summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-02 18:51:25 +0100
committerSon Ho2021-11-02 18:51:25 +0100
commitec39b172441fa3739635e55ea8ebbc170c53f3f2 (patch)
tree3d4e1894b6e9b3f4a99929c47307145c8cc357f1
parent09bfbde5ebdc60cef109b570b6c6f567a5b516b0 (diff)
Setup the project
Diffstat (limited to '')
-rw-r--r--Makefile5
-rw-r--r--dune-project1
-rw-r--r--src/dune2
-rw-r--r--src/main.ml110
4 files changed, 118 insertions, 0 deletions
diff --git a/Makefile b/Makefile
new file mode 100644
index 00000000..c44454e9
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,5 @@
+all:
+ dune build src/main.exe && dune exec src/main.exe
+
+doc:
+ dune build @doc
diff --git a/dune-project b/dune-project
new file mode 100644
index 00000000..c2e46604
--- /dev/null
+++ b/dune-project
@@ -0,0 +1 @@
+(lang dune 2.8)
diff --git a/src/dune b/src/dune
new file mode 100644
index 00000000..6ab09aa4
--- /dev/null
+++ b/src/dune
@@ -0,0 +1,2 @@
+(executable
+ (name main)) \ No newline at end of file
diff --git a/src/main.ml b/src/main.ml
new file mode 100644
index 00000000..45bb2057
--- /dev/null
+++ b/src/main.ml
@@ -0,0 +1,110 @@
+exception IntegerOverflow of unit
+
+(** Signature for a module describing an identifier.
+
+ We often need identifiers (for definitions, variables, etc.) and in
+ order to make sure we don't mix them, we use a generative functor
+ (see [IdGen]).
+*)
+module type Id = sig
+ type id
+
+ type 'a vector
+
+ val zero : id
+
+ val incr : id -> id
+
+ val to_string : id -> string
+end
+
+(** Generative functor for identifiers.
+
+ See [Id].
+*)
+module IdGen () : Id = struct
+ type id = int
+
+ type 'a vector = 'a list (* TODO: use a map *)
+
+ let zero = 0
+
+ let incr x =
+ (* Identifiers should never overflow (because max_int is a really big
+ * value - but we really want to make sure we detect overflows if
+ * they happen *)
+ if x == max_int then raise (IntegerOverflow ()) else x + 1
+
+ let to_string = string_of_int
+end
+
+type name = string list
+(** A name such as: `std::collections::vector` *)
+
+module TypeVarId = IdGen ()
+
+module TypeDefId = IdGen ()
+
+module VariantId = IdGen ()
+
+module FieldId = IdGen ()
+
+module RegionVarId = IdGen ()
+
+type type_var = {
+ index : TypeVarId.id; (** Unique index identifying the variable *)
+ name : string; (** Variable name *)
+}
+
+type region_var = {
+ index : RegionVarId.id; (** Unique index identifying the region *)
+ name : string option; (** Region name *)
+}
+
+(** A region.
+
+ Regions are used in function signatures (in which case we use region variable
+ ids) and in symbolic variables and projections (in which case we use region
+ ids).
+ *)
+type 'rid region =
+ | Static (** Static region *)
+ | Var of 'rid (** Non-static region *)
+
+(** The type of erased regions.
+
+ We could use unit, but having a dedicated type makes things more explicit.
+ *)
+type erased_region = Erased
+
+(* TODO *)
+type rty = unit
+
+type field = { name : string; ty : rty }
+
+type variant = { name : string; fields : field FieldId.vector }
+
+type type_def_kind =
+ | Struct of field FieldId.vector
+ | Enum of variant VariantId.vector
+
+type type_def = {
+ def_id : TypeDefId.id;
+ name : name;
+ region_params : region_var RegionVarId.vector;
+ type_params : type_var TypeVarId.vector;
+ kind : type_def_kind;
+}
+
+module Id0 = IdGen ()
+
+module Id1 = IdGen ()
+
+let x0 = Id0.zero
+
+let x1 = Id0.incr x0
+
+let () =
+ let _ = print_endline "Hello, world!" in
+ let _ = print_endline (Id0.to_string x1) in
+ ()