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

7 files changed, 163 insertions, 165 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
 
 
 
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 *)
diff --git a/language/l2.ott b/language/l2.ott
index 4ee9cd65..d65f1cb0 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -767,7 +767,7 @@ effect_opt :: 'Effect_opt_' ::=
 
 funcl :: 'FCL_' ::=
   {{ com Function clause }}
-  {{ aux _ l }} {{ auxparam 'a }}
+  {{ aux _ annot }} {{ auxparam 'a }}
   | id pat = exp                   :: :: Funcl
 
 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index d26f6b84..0c080553 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -646,7 +646,7 @@ let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) :
 let to_ast_funcl (names,k_env,def_ord) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (tannot funcl) =
   match fcl with
   | Parse_ast.FCL_Funcl(id,pat,exp) -> 
-    FCL_aux(FCL_Funcl(to_ast_id id, to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp),l)
+    FCL_aux(FCL_Funcl(to_ast_id id, to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp),(l,NoTyp))
 
 let to_ast_fundef  (names,k_env,def_ord) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef) : (tannot fundef) envs_out = 
   match fd with
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index 52361911..74e5fd4c 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -38,11 +38,9 @@ end
 
 let rec extract_effects_of_pat id execute = match execute with
   | [] -> []
-  | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) _) _) exp) _ :: executes ->
+  | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) _) _) _) (_,(Just(_,_,_,Effect_aux(Effect_set efs) _))) :: executes ->
     if i = id 
-    then match exp with
-      | E_aux e (_,Just(_,_,_,Effect_aux (Effect_set efs) _)) -> efs
-      | _ -> [] end
+    then efs
     else extract_effects_of_pat id executes
   | _::executes -> extract_effects_of_pat id executes
 end
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index a4581162..faa75224 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -528,9 +528,9 @@ let pp_lem_effects_opt ppf (Effect_opt_aux(e,l)) =
   | Effect_opt_pure -> fprintf ppf "(Effect_opt_aux Effect_opt_pure %a)" pp_lem_l l
   | Effect_opt_effect e -> fprintf ppf "(Effect_opt_aux (Effect_opt_effect %a) %a)" pp_lem_effects e pp_lem_l l
 
-let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),l)) =
-  fprintf ppf "@[<0>(FCL_aux (%a %a %a %a) %a)@]@\n" 
-    kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp pp_lem_l l
+let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),(l,annot))) =
+  fprintf ppf "@[<0>(FCL_aux (%a %a %a %a) (%a,%a))@]@\n" 
+    kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot
 
 let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) =
   let pp_funcls ppf funcl = fprintf ppf "%a %a" pp_lem_funcl funcl kwd ";" in
diff --git a/src/type_check.ml b/src/type_check.ml
index 8bdede1d..5421b1b8 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1576,7 +1576,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
               | Rec_aux(Rec_nonrec,_) -> false
 	      | Rec_aux(Rec_rec,_) -> true in
   let Some(id) = List.fold_right 
-    (fun (FCL_aux((FCL_Funcl(id,pat,exp)),l)) id' ->
+    (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) id' ->
       match id' with
 	| Some(id') -> if id' = id_to_string id then Some(id') 
 	  else typ_error l ("Function declaration expects all definitions to have the same name, " 
@@ -1593,20 +1593,20 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       t,p_t,Base((ids,{t=Tfn(p_t,t,IP_none,ef)}),Emp_global,constraints,ef) in
   let check t_env imp_param =
     List.split
-      (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),l)) ->
+      (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) ->
 	let (pat',t_env',cs_p,t') = check_pattern (Env(d_env,t_env)) Emp_local param_t pat in
 	(*let _ = Printf.printf "about to check that %s and %s are consistent\n!" (t_to_string t') (t_to_string param_t) in*)
 	let exp',_,_,cs_e,ef = 
 	  check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env t_env')) imp_param ret_t exp in
 	(*let _ = Printf.printf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
 	let cs = [CondCons(Fun l,cs_p,cs_e)] in
-	(FCL_aux((FCL_Funcl(id,pat',exp')),l),(cs,ef))) funcls) in
-  let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),l)) = 
+	(FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,cs,ef)))),(cs,ef))) funcls) in
+  let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),annot)) = 
     let pat' = match pat with
       | P_lit (L_aux (L_unit,l')) -> P_aux(P_id (Id_aux (Id var, l')), t)
       | P_tup pats -> P_aux(P_tup ((P_aux (P_id (Id_aux (Id var, l)), t))::pats), t)
       | _ ->  P_aux(P_tup [(P_aux (P_id (Id_aux (Id var,l)), t));(P_aux(pat,t))], t)
-    in (FCL_aux ((FCL_Funcl(id,pat',exp)),l))
+    in (FCL_aux ((FCL_Funcl(id,pat',exp)),annot))
   in
   match (in_env,tannot) with
     | Some(Base( (params,u),Spec,constraints,eft)), Base( (p',t),_,c',eft') ->