From 02e4b62028411bc107ba63eff87b8d996baae695 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Tue, 30 Sep 2014 16:52:38 +0100 Subject: Add type annotations to funcls to track effects and constraints from one function-clause --- language/l2.lem | 148 ++++++++++++++--------------- language/l2.ml | 154 +++++++++++++++---------------- language/l2.ott | 2 +- src/initial_check.ml | 2 +- src/lem_interp/instruction_extractor.lem | 6 +- src/pretty_print.ml | 6 +- src/type_check.ml | 10 +- 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 @@ -149,6 +149,20 @@ typquant_aux = (* type quantifiers and constraints *) | TypQ_no_forall (* sugar, omitting quantifier 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 @@ -176,33 +190,14 @@ and typ_arg = Typ_arg_aux of typ_arg_aux * l -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 @@ -230,6 +225,11 @@ and 'a fpat = FP_aux of 'a fpat_aux * 'a annot +type +typschm = + TypSchm_aux of typschm_aux * l + + type 'a reg_id_aux = RI_id of id @@ -318,12 +318,6 @@ type RI_aux of 'a reg_id_aux * 'a annot -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 @@ -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 @@ -405,6 +405,16 @@ type AL_aux of 'a alias_spec_aux * 'a annot +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 *) @@ -414,18 +424,6 @@ type | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) -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 @@ -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 @@ -480,6 +475,11 @@ type DEC_aux of 'a dec_spec_aux * 'a annot +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 *) 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') -> -- cgit v1.2.3