Small clean up of ott files, start of environments for formal representation of kind and type system

3 files changed, 69 insertions, 57 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 3ef45b12..db3d83a5 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -217,14 +217,7 @@ typschm =
 
 
 type 
-'a letbind_aux =  (* Let binding *)
-   LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
- | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
-
-and 'a letbind = 
-   LB_aux of 'a letbind_aux * 'a annot
-
-and 'a exp_aux =  (* Expression *)
+'a exp_aux =  (* Expression *)
    E_block of ('a exp) list (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
  | E_lit of lit (* literal constant *)
@@ -279,16 +272,12 @@ and 'a pexp_aux =  (* Pattern match *)
 and 'a pexp = 
    Pat_aux of 'a pexp_aux * 'a annot
 
+and 'a letbind_aux =  (* Let binding *)
+   LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
+ | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
 
-type 
-naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of string
-
-
-type 
-'a funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * 'a pat * 'a exp
+and 'a letbind = 
+   LB_aux of 'a letbind_aux * 'a annot
 
 
 type 
@@ -298,6 +287,11 @@ rec_opt_aux =  (* Optional recursive annotation for functions *)
 
 
 type 
+'a funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * 'a pat * 'a exp
+
+
+type 
 'a tannot_opt_aux =  (* Optional type annotation for functions *)
    Typ_annot_opt_some of typquant * typ
 
@@ -309,18 +303,14 @@ type
 
 
 type 
-index_range_aux =  (* index specification, for bitfields in register types *)
-   BF_single of int (* single index *)
- | BF_range of int * int (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
-
-and index_range = 
-   BF_aux of index_range_aux * l
+naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of string
 
 
 type 
-naming_scheme_opt = 
-   Name_sect_aux of naming_scheme_opt_aux * l
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
 
 
 type 
@@ -329,11 +319,6 @@ type
 
 
 type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
-
-
-type 
 'a tannot_opt = 
    Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
 
@@ -344,17 +329,18 @@ type
 
 
 type 
-'a val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
+index_range_aux =  (* index specification, for bitfields in register types *)
+   BF_single of int (* single index *)
+ | BF_range of int * int (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
+
+and index_range = 
+   BF_aux of index_range_aux * l
 
 
 type 
-'a type_def_aux =  (* Type definition body *)
-   TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
- | TD_record of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* union type definition *)
- | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
+naming_scheme_opt = 
+   Name_sect_aux of naming_scheme_opt_aux * l
 
 
 type 
@@ -363,24 +349,33 @@ type
 
 
 type 
+'a val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
+
+
+type 
 'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
    DT_kind of base_kind * id
  | DT_typ of typschm * id
 
 
 type 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
+'a type_def_aux =  (* Type definition body *)
+   TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
+ | TD_record of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
+ | TD_variant of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* union type definition *)
+ | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
 
 
 type 
-'a type_def = 
-   TD_aux of 'a type_def_aux * 'a annot
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a val_spec = 
+   VS_aux of 'a val_spec_aux * 'a annot
 
 
 type 
@@ -389,6 +384,22 @@ type
 
 
 type 
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
+
+
+type 
+k =  (* Internal kinds *)
+   Ki_typ
+ | Ki_nat
+ | Ki_ord
+ | Ki_efct
+ | Ki_val (* Representing values, for use in identifier checks *)
+ | Ki_ctor of (k) list * k
+ | Ki_infer (* Representing an unknown kind, inferred by context *)
+
+
+type 
 'a def_aux =  (* Top-level definition *)
    DEF_type of 'a type_def (* type definition *)
  | DEF_fundef of 'a fundef (* function definition *)
@@ -409,11 +420,6 @@ type
 
 
 type 
-'a def = 
-   DEF_aux of 'a def_aux * 'a annot
-
-
-type 
 'a typ_lib_aux =  (* library types and syntactic sugar for them *)
    Typ_lib_unit (* unit type with value $()$ *)
  | Typ_lib_bool (* booleans $_$ and $_$ *)
@@ -432,13 +438,13 @@ type
 
 
 type 
-'a ctor_def = 
-   CT_aux of 'a ctor_def_aux * 'a annot
+'a def = 
+   DEF_aux of 'a def_aux * 'a annot
 
 
 type 
-'a defs =  (* Definition sequence *)
-   Defs of ('a def) list
+'a ctor_def = 
+   CT_aux of 'a ctor_def_aux * 'a annot
 
 
 type 
@@ -446,4 +452,10 @@ type
    Typ_lib_aux of 'a typ_lib_aux * l
 
 
+type 
+'a defs =  (* Definition sequence *)
+   Defs of ('a def) list
+
+(** definitions *)
+
 
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index f527c402..23957118 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -62,7 +62,7 @@ kind_aux =  (* kinds *)
 
 
 type 
-atyp_aux =  (* expression of all kinds *)
+atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *)
    ATyp_id of id (* identifier *)
  | ATyp_constant of int (* constant *)
  | ATyp_times of atyp * atyp (* product *)
@@ -73,7 +73,7 @@ atyp_aux =  (* expression of all kinds *)
  | ATyp_efid of id
  | ATyp_set of (efct) list (* effect set *)
  | ATyp_wild (* Unspecified type *)
- | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code) *)
+ | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *)
  | ATyp_tup of (atyp) list (* Tuple type *)
  | ATyp_app of id * (atyp) list (* type constructor application *)
 
diff --git a/src/type_internal.mli b/src/type_internal.mli
index f53ac9dd..9aa5b9d9 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -33,7 +33,7 @@ and nexp_aux =
   | Nadd of nexp * nexp
   | Nmult of nexp * nexp
   | N2n of nexp
-  | Nneg of nexp (* Unary minus for representing new vector sizes after vector slicing *)
+  | Nneg of nexp (* Unary minus for representing new sizes after slicing *)
   | Nuvar of n_uvar
 and effect = { mutable effect : effect_aux }
 and effect_aux =