From ec39b172441fa3739635e55ea8ebbc170c53f3f2 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 2 Nov 2021 18:51:25 +0100 Subject: Setup the project --- Makefile | 5 +++ dune-project | 1 + src/dune | 2 ++ src/main.ml | 110 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 118 insertions(+) create mode 100644 Makefile create mode 100644 dune-project create mode 100644 src/dune create mode 100644 src/main.ml 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 + () -- cgit v1.2.3