Add type annotations to funcls to track effects and constraints from one function-clause

1 files changed, 77 insertions, 77 deletions

diff --git a/language/l2.ml b/language/l2.ml
index bdbec809..ab0e7b66 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -150,6 +150,20 @@ typquant_aux =  (* type quantifiers and constraints *)
 
 
 type 
+lit_aux =  (* Literal constant *)
+   L_unit (* $() : _$ *)
+ | L_zero (* $_ : _$ *)
+ | L_one (* $_ : _$ *)
+ | L_true (* $_ : _$ *)
+ | L_false (* $_ : _$ *)
+ | L_num of int (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* constant representing undefined values *)
+ | L_string of string (* string constant *)
+
+
+type 
 typquant = 
    TypQ_aux of typquant_aux * l
 
@@ -177,32 +191,13 @@ and typ_arg =
 
 
 type 
-lit_aux =  (* Literal constant *)
-   L_unit (* $() : _$ *)
- | L_zero (* $_ : _$ *)
- | L_one (* $_ : _$ *)
- | L_true (* $_ : _$ *)
- | L_false (* $_ : _$ *)
- | L_num of int (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_undef (* constant representing undefined values *)
- | L_string of string (* string constant *)
-
-
-type 
-typschm_aux =  (* type scheme *)
-   TypSchm_ts of typquant * typ
-
-
-type 
 lit = 
    L_aux of lit_aux * l
 
 
 type 
-typschm = 
-   TypSchm_aux of typschm_aux * l
+typschm_aux =  (* type scheme *)
+   TypSchm_ts of typquant * typ
 
 
 type 
@@ -231,6 +226,11 @@ and 'a fpat =
 
 
 type 
+typschm = 
+   TypSchm_aux of typschm_aux * l
+
+
+type 
 'a reg_id_aux = 
    RI_id of id
 
@@ -319,12 +319,6 @@ type
 
 
 type 
-name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of string
-
-
-type 
 type_union_aux =  (* Type union constructors *)
    Tu_id of id
  | Tu_ty_id of typ * id
@@ -336,9 +330,8 @@ tannot_opt_aux =  (* Optional type annotation for functions *)
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+'a funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * 'a pat * 'a exp
 
 
 type 
@@ -348,8 +341,15 @@ effect_opt_aux =  (* Optional effect annotation for functions *)
 
 
 type 
-'a funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * 'a pat * 'a exp
+name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of string
+
+
+type 
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
 
 
 type 
@@ -361,28 +361,28 @@ type
 
 
 type 
-name_scm_opt = 
-   Name_sect_aux of name_scm_opt_aux * l
+type_union = 
+   Tu_aux of type_union_aux * l
 
 
 type 
-type_union = 
-   Tu_aux of type_union_aux * l
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
 
 
 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 *)
+'a funcl = 
+   FCL_aux of 'a funcl_aux * 'a annot
 
-and index_range = 
-   BF_aux of index_range_aux * l
+
+type 
+effect_opt = 
+   Effect_opt_aux of effect_opt_aux * l
 
 
 type 
-tannot_opt = 
-   Typ_annot_opt_aux of tannot_opt_aux * l
+name_scm_opt = 
+   Name_sect_aux of name_scm_opt_aux * l
 
 
 type 
@@ -391,13 +391,13 @@ rec_opt =
 
 
 type 
-effect_opt = 
-   Effect_opt_aux of effect_opt_aux * l
-
+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 *)
 
-type 
-'a funcl = 
-   FCL_aux of 'a funcl_aux * l
+and index_range = 
+   BF_aux of index_range_aux * l
 
 
 type 
@@ -406,6 +406,16 @@ type
 
 
 type 
+'a scattered_def_aux =  (* Function and type union definitions that can be spread across
+         a file. Each one must end in $_$ *)
+   SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
+ | SD_scattered_funcl of 'a funcl (* scattered function definition clause *)
+ | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
+ | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
+ | SD_scattered_end of id (* scattered definition end *)
+
+
+type 
 'a type_def_aux =  (* Type definition body *)
    TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
  | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
@@ -415,18 +425,6 @@ type
 
 
 type 
-'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
-
-
-type 
-'a val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
-
-
-type 
 'a default_spec_aux =  (* Default kinding or typing assumption *)
    DT_kind of base_kind * kid
  | DT_order of order
@@ -434,13 +432,8 @@ type
 
 
 type 
-'a scattered_def_aux =  (* Function and type union definitions that can be spread across
-         a file. Each one must end in $_$ *)
-   SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
- | SD_scattered_funcl of 'a funcl (* scattered function definition clause *)
- | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
- | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
- | SD_scattered_end of id (* scattered definition end *)
+'a fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
 
 
 type 
@@ -451,18 +444,20 @@ type
 
 
 type 
-'a type_def = 
-   TD_aux of 'a type_def_aux * 'a annot
+'a val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
+ | VS_extern_no_rename of typschm * id
+ | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a scattered_def = 
+   SD_aux of 'a scattered_def_aux * 'a annot
 
 
 type 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
 
 
 type 
@@ -471,8 +466,8 @@ type
 
 
 type 
-'a scattered_def = 
-   SD_aux of 'a scattered_def_aux * 'a annot
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
 
 
 type 
@@ -481,6 +476,11 @@ type
 
 
 type 
+'a val_spec = 
+   VS_aux of 'a val_spec_aux * 'a annot
+
+
+type 
 'a def =  (* Top-level definition *)
    DEF_type of 'a type_def (* type definition *)
  | DEF_fundef of 'a fundef (* function definition *)