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

1 files changed, 74 insertions, 74 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 3f02fc88..934b1ec0 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -76,30 +76,30 @@ type base_effect =
  | BE_aux of base_effect_aux * l
 
 
-type id_aux =  (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
-
-
 type effect_aux =  (* effect set, of kind Effects *)
  | Effect_var of kid
  | Effect_set of list base_effect (* effect set *)
 
 
+type id_aux =  (* Identifier *)
+ | Id of x
+ | DeIid of x (* remove infix status *)
+
+
 type order_aux =  (* vector order specifications, of kind Order *)
  | Ord_var of kid (* variable *)
  | Ord_inc (* increasing (little-endian) *)
  | Ord_dec (* decreasing (big-endian) *)
 
 
-type id = 
- | Id_aux of id_aux * l
-
-
 type effect = 
  | Effect_aux of effect_aux * l
 
 
+type id = 
+ | Id_aux of id_aux * l
+
+
 type order = 
  | Ord_aux of order_aux * l
 
@@ -156,6 +156,10 @@ type lit_aux =  (* Literal constant *)
  | L_string of string (* string constant *)
 
 
+type typquant = 
+ | TypQ_aux of typquant_aux * l
+
+
 type typ_aux =  (* Type expressions, of kind $Type$ *)
  | Typ_wild (* Unspecified type *)
  | Typ_id of id (* Defined type *)
@@ -177,10 +181,6 @@ and typ_arg =
  | Typ_arg_aux of typ_arg_aux * l
 
 
-type typquant = 
- | TypQ_aux of typquant_aux * l
-
-
 type lit = 
  | L_aux of lit_aux * l
 
@@ -221,7 +221,14 @@ type reg_id_aux 'a =
  | RI_id of id
 
 
-type exp_aux 'a =  (* Expression *)
+type letbind_aux 'a =  (* Let binding *)
+ | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *)
+ | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *)
+
+and letbind 'a = 
+ | LB_aux of (letbind_aux 'a) * annot 'a
+
+and exp_aux 'a =  (* Expression *)
  | E_block of list (exp 'a) (* block *)
  | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *)
  | E_id of id (* identifier *)
@@ -290,20 +297,16 @@ and pexp_aux 'a =  (* Pattern match *)
 and pexp 'a = 
  | Pat_aux of (pexp_aux 'a) * annot 'a
 
-and letbind_aux 'a =  (* Let binding *)
- | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *)
- | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *)
-
-and letbind 'a = 
- | LB_aux of (letbind_aux 'a) * annot 'a
-
 
 type reg_id 'a = 
  | RI_aux of (reg_id_aux 'a) * annot 'a
 
 
-type tannot_opt_aux =  (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
+type alias_spec_aux 'a =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
+ | AL_subreg of (reg_id 'a) * id
+ | AL_bit of (reg_id 'a) * (exp 'a)
+ | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a)
+ | AL_concat of (reg_id 'a) * (reg_id 'a)
 
 
 type rec_opt_aux =  (* Optional recursive annotation for functions *)
@@ -311,15 +314,19 @@ type rec_opt_aux =  (* Optional recursive annotation for functions *)
  | Rec_rec (* recursive *)
 
 
+type funcl_aux 'a =  (* Function clause *)
+ | FCL_Funcl of id * (pat 'a) * (exp 'a)
+
+
+type tannot_opt_aux =  (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
+
+
 type effect_opt_aux =  (* Optional effect annotation for functions *)
  | Effect_opt_pure (* sugar for empty effect set *)
  | Effect_opt_effect of effect
 
 
-type funcl_aux 'a =  (* Function clause *)
- | FCL_Funcl of id * (pat 'a) * (exp 'a)
-
-
 type name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
  | Name_sect_none
  | Name_sect_some of string
@@ -330,27 +337,24 @@ type type_union_aux =  (* Type union constructors *)
  | Tu_ty_id of typ * id
 
 
-type alias_spec_aux 'a =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
- | AL_subreg of (reg_id 'a) * id
- | AL_bit of (reg_id 'a) * (exp 'a)
- | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a)
- | AL_concat of (reg_id 'a) * (reg_id 'a)
-
-
-type tannot_opt = 
- | Typ_annot_opt_aux of tannot_opt_aux * l
+type alias_spec 'a = 
+ | AL_aux of (alias_spec_aux 'a) * annot 'a
 
 
 type rec_opt = 
  | Rec_aux of rec_opt_aux * l
 
 
-type effect_opt = 
- | Effect_opt_aux of effect_opt_aux * l
+type funcl 'a = 
+ | FCL_aux of (funcl_aux 'a) * annot 'a
 
 
-type funcl 'a = 
- | FCL_aux of (funcl_aux 'a) * l
+type tannot_opt = 
+ | Typ_annot_opt_aux of tannot_opt_aux * l
+
+
+type effect_opt = 
+ | Effect_opt_aux of effect_opt_aux * l
 
 
 type name_scm_opt = 
@@ -361,10 +365,6 @@ type type_union =
  | Tu_aux of type_union_aux * l
 
 
-type alias_spec 'a = 
- | AL_aux of (alias_spec_aux 'a) * annot 'a
-
-
 type index_range_aux =  (* index specification, for bitfields in register types *)
  | BF_single of integer (* single index *)
  | BF_range of integer * integer (* index range *)
@@ -374,20 +374,14 @@ and index_range =
  | BF_aux of index_range_aux * l
 
 
-type fundef_aux 'a =  (* Function definition *)
- | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
-
-
-type val_spec_aux 'a =  (* 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 dec_spec_aux 'a =  (* Register declarations *)
+ | DEC_reg of typ * id
+ | DEC_alias of id * (alias_spec 'a)
+ | DEC_typ_alias of typ * id * (alias_spec 'a)
 
 
-type default_spec_aux 'a =  (* Default kinding or typing assumption *)
- | DT_kind of base_kind * kid
- | DT_order of order
- | DT_typ of typschm * id
+type fundef_aux 'a =  (* Function definition *)
+ | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
 
 
 type scattered_def_aux 'a =  (* Function and type union definitions that can be spread across
@@ -399,12 +393,6 @@ type scattered_def_aux 'a =  (* Function and type union definitions that can be
  | SD_scattered_end of id (* scattered definition end *)
 
 
-type dec_spec_aux 'a =  (* Register declarations *)
- | DEC_reg of typ * id
- | DEC_alias of id * (alias_spec 'a)
- | DEC_typ_alias of typ * id * (alias_spec 'a)
-
-
 type type_def_aux 'a =  (* Type definition body *)
  | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
  | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
@@ -413,30 +401,42 @@ type type_def_aux 'a =  (* Type definition body *)
  | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
-type fundef 'a = 
- | FD_aux of (fundef_aux 'a) * annot 'a
+type default_spec_aux 'a =  (* Default kinding or typing assumption *)
+ | DT_kind of base_kind * kid
+ | DT_order of order
+ | DT_typ of typschm * id
 
 
-type val_spec 'a = 
- | VS_aux of (val_spec_aux 'a) * annot 'a
+type val_spec_aux 'a =  (* 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 default_spec 'a = 
- | DT_aux of (default_spec_aux 'a) * l
+type dec_spec 'a = 
+ | DEC_aux of (dec_spec_aux 'a) * annot 'a
 
 
-type scattered_def 'a = 
- | SD_aux of (scattered_def_aux 'a) * annot 'a
+type fundef 'a = 
+ | FD_aux of (fundef_aux 'a) * annot 'a
 
 
-type dec_spec 'a = 
- | DEC_aux of (dec_spec_aux 'a) * annot 'a
+type scattered_def 'a = 
+ | SD_aux of (scattered_def_aux 'a) * annot 'a
 
 
 type type_def 'a = 
  | TD_aux of (type_def_aux 'a) * annot 'a
 
 
+type default_spec 'a = 
+ | DT_aux of (default_spec_aux 'a) * l
+
+
+type val_spec 'a = 
+ | VS_aux of (val_spec_aux 'a) * annot 'a
+
+
 type def 'a =  (* Top-level definition *)
  | DEF_type of (type_def 'a) (* type definition *)
  | DEF_fundef of (fundef 'a) (* function definition *)
@@ -589,10 +589,10 @@ let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should
 
 
 
-type E = env
+type I = inf
 
 
-type I = inf
+type E = env