From e4af7c3090c93a129e99dd75f2a20d5a9d2f6920 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 27 Jul 2018 18:50:31 +0100 Subject: Make type annotations abstract in type_check.mli Rather than exporting the implementation of type annotations as type tannot = (Env.t * typ * effect) option we leave it abstract as type tannot Some additional functions have been added to type_check.mli to work with these abstract type annotations. Most use cases where the type was constructed explicitly can be handled by using either mk_tannot or empty_tannot. For pattern matching on a tannot there is a function val destruct_tannot : tannot -> (Env.t * typ * effect) option Note that it is specifically not guaranteed that using mk_tannot on the elements returned by destruct_tannot re-constructs the same tannot, as destruct_tannot is only used to give the old view of a type annotation, and we may add additional information that will not be returned by destruct_tannot. --- src/anf.ml | 2 +- src/ast_util.ml | 5 -- src/ast_util.mli | 1 - src/interpreter.ml | 3 +- src/monomorphise.ml | 141 +++++++++++++++++++++++--------------------- src/pretty_print_coq.ml | 18 +++--- src/pretty_print_lem.ml | 22 +++---- src/rewriter.ml | 42 ++++++------- src/rewrites.ml | 152 ++++++++++++++++++++++++++---------------------- src/spec_analysis.ml | 3 +- src/state.ml | 6 +- src/type_check.ml | 19 ++++++ src/type_check.mli | 20 ++++++- 13 files changed, 243 insertions(+), 191 deletions(-) diff --git a/src/anf.ml b/src/anf.ml index d0803d4f..97565b2b 100644 --- a/src/anf.ml +++ b/src/anf.ml @@ -660,7 +660,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") | E_let (LB_aux (LB_val (pat, binding), _), body) -> - anf (E_aux (E_case (binding, [Pat_aux (Pat_exp (pat, body), (Parse_ast.Unknown, None))]), exp_annot)) + anf (E_aux (E_case (binding, [Pat_aux (Pat_exp (pat, body), (Parse_ast.Unknown, empty_tannot))]), exp_annot)) | E_tuple exps -> let aexps = List.map anf exps in diff --git a/src/ast_util.ml b/src/ast_util.ml index 781069eb..3c6cbeb2 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -633,11 +633,6 @@ and string_of_n_constraint = function | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" -let string_of_annot = function - | Some (_, typ, eff) -> - "Some (_, " ^ string_of_typ typ ^ ", " ^ string_of_effect eff ^ ")" - | None -> "None" - let string_of_quant_item_aux = function | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> "(" ^ string_of_kid kid ^ " :: " ^ string_of_kind k ^ ")" diff --git a/src/ast_util.mli b/src/ast_util.mli index 083b81e0..545e669d 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -209,7 +209,6 @@ val string_of_nexp : nexp -> string val string_of_typ : typ -> string val string_of_typ_arg : typ_arg -> string val string_of_typ_pat : typ_pat -> string -val string_of_annot : ('a * typ * effect) option -> string val string_of_n_constraint : n_constraint -> string val string_of_quant_item : quant_item -> string val string_of_typquant : typquant -> string diff --git a/src/interpreter.ml b/src/interpreter.ml index e4f7faf0..9a1d0ed2 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -135,7 +135,7 @@ let is_false = function | (E_aux (E_internal_value (V_bool b), _)) -> b == false | _ -> false -let exp_of_value v = (E_aux (E_internal_value v, (Parse_ast.Unknown, None))) +let exp_of_value v = (E_aux (E_internal_value v, (Parse_ast.Unknown, Type_check.empty_tannot))) let value_of_exp = function | (E_aux (E_internal_value v, _)) -> v | _ -> failwith "value_of_exp coerction failed" @@ -589,7 +589,6 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) = | LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id)) and pattern_match env (P_aux (p_aux, _) as pat) value = - (* print_endline ("Matching: " ^ string_of_pat pat ^ " with " ^ string_of_value value |> Util.yellow |> Util.clear); *) match p_aux with | P_lit lit -> eq_value (value_of_lit lit) value, Bindings.empty | P_wild -> true, Bindings.empty diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 9acb6052..3e7ef970 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -175,8 +175,8 @@ let pat_id_is_variable env id = let rec is_value (E_aux (e,(l,annot))) = let is_constructor id = - match annot with - | None -> + match destruct_tannot annot with + | None -> (Reporting_basic.print_err false true l "Monomorphisation" ("Missing type information for identifier " ^ string_of_id id); false) (* Be conservative if we have no info *) @@ -485,9 +485,13 @@ let reduce_nexp subst ne = let typ_of_args args = match args with - | [E_aux (E_tuple args,(_,Some (_,Typ_aux (Typ_exist _,_),_)))] -> - let tys = List.map Type_check.typ_of args in - Typ_aux (Typ_tup tys,Unknown) + | [(E_aux (E_tuple args, (_, tannot)) as exp)] -> + begin match destruct_tannot tannot with + | Some (_,Typ_aux (Typ_exist _,_),_) -> + let tys = List.map Type_check.typ_of args in + Typ_aux (Typ_tup tys,Unknown) + | _ -> Type_check.typ_of exp + end | [exp] -> Type_check.typ_of exp | _ -> @@ -541,9 +545,10 @@ let nexp_subst_fns substs = (* let s_typschm (TypSchm_aux (TypSchm_ts (q,t),l)) = TypSchm_aux (TypSchm_ts (q,s_t t),l) in hopefully don't need this anyway *)(* let s_typschm tsh = tsh in*) - let s_tannot = function - | None -> None - | Some (env,t,eff) -> Some (env,s_t t,eff) (* TODO: what about env? *) + let s_tannot tannot = + match destruct_tannot tannot with + | None -> empty_tannot + | Some (env,t,eff) -> mk_tannot env (s_t t) eff (* TODO: what about env? *) in let rec s_pat (P_aux (p,(l,annot))) = let re p = P_aux (p,(l,s_tannot annot)) in @@ -706,7 +711,8 @@ let fabricate_nexp_exist env l typ kids nc typ' = | _ -> raise (Reporting_basic.err_general l ("Undefined value at unsupported type " ^ string_of_typ typ)) -let fabricate_nexp l = function +let fabricate_nexp l tannot = + match destruct_tannot tannot with | None -> nint 32 | Some (env,typ,_) -> match Type_check.destruct_exist env typ with @@ -725,10 +731,6 @@ let atom_typ_kid kid = function let reduce_cast typ exp l annot = let env = env_of_annot (l,annot) in - let replace_typ typ = function - | Some (env,_,eff) -> Some (env,typ,eff) - | None -> None - in let typ' = Env.base_typ_of env typ in match exp, destruct_exist env typ' with | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' -> @@ -831,11 +833,10 @@ let try_app (l,ann) (id,args) = | _ -> None else if is_id "slice" then match args with - | [E_aux (E_lit (L_aux ((L_hex _| L_bin _),_) as lit), - (_,Some (vec_env,vec_typ,_))); + | [E_aux (E_lit (L_aux ((L_hex _| L_bin _),_) as lit), annot); E_aux (E_lit L_aux (L_num i,_), _); E_aux (E_lit L_aux (L_num len,_), _)] -> - (match Env.base_typ_of vec_env vec_typ with + (match Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) with | Typ_aux (Typ_app (_,[_;Typ_arg_aux (Typ_arg_order ord,_);_]),_) -> (match slice_lit lit i len ord with | Some lit' -> Some (E_aux (E_lit lit',(l,ann))) @@ -996,7 +997,7 @@ let rec freshen_pat_bindings p = (mkp (P_not r), vs) | P_as (p,_) -> aux p | P_typ (typ,p) -> let p',vs = aux p in mkp (P_typ (typ,p')),vs - | P_id id -> let id' = freshen_id id in mkp (P_id id'),[id,E_aux (E_id id',(Generated Unknown,None))] + | P_id id -> let id' = freshen_id id in mkp (P_id id'),[id,E_aux (E_id id',(Generated Unknown,empty_tannot))] | P_var (p,_) -> aux p | P_app (id,args) -> let args',vs = List.split (List.map aux args) in @@ -1031,7 +1032,7 @@ let rec freshen_pat_bindings p = let stop_at_false_assertions e = let dummy_value_of_typ typ = let l = Generated Unknown in - E_aux (E_exit (E_aux (E_lit (L_aux (L_unit,l)),(l,None))),(l,None)) + E_aux (E_exit (E_aux (E_lit (L_aux (L_unit,l)),(l,empty_tannot))),(l,empty_tannot)) in let rec nc_false (NC_aux (nc,_)) = match nc with @@ -1130,7 +1131,7 @@ let apply_pat_choices choices = | choice,max,subst -> (match List.nth cases choice with | Pat_aux (Pat_exp (p,E_aux (e,_)),_) -> - let dummyannot = (Generated Unknown,None) in + let dummyannot = (Generated Unknown,empty_tannot) in (* TODO: use a proper substitution *) List.fold_left (fun e (id,e') -> E_let (LB_aux (LB_val (P_aux (P_id id, dummyannot),e'),dummyannot),E_aux (e,dummyannot))) e subst @@ -1386,7 +1387,7 @@ let split_defs all_errors splits defs = re (E_let (LB_aux (LB_val (p,e'), annot), e2')) assigns in if is_value e' && not (is_value e) then - match can_match ref_vars e' [Pat_aux (Pat_exp (p,e2),(Unknown,None))] substs assigns with + match can_match ref_vars e' [Pat_aux (Pat_exp (p,e2),(Unknown,empty_tannot))] substs assigns with | None -> plain () | Some (e'',bindings,kbindings) -> let e'' = nexp_subst_exp (kbindings_from_list kbindings) e'' in @@ -1490,9 +1491,9 @@ let split_defs all_errors splits defs = | Some (eff,_) when not (is_pure eff) -> None | Some (_,fcls) -> let arg = match args with - | [] -> E_aux (E_lit (L_aux (L_unit,Generated l)),(Generated l,None)) + | [] -> E_aux (E_lit (L_aux (L_unit,Generated l)),(Generated l,empty_tannot)) | [e] -> e - | _ -> E_aux (E_tuple args,(Generated l,None)) in + | _ -> E_aux (E_tuple args,(Generated l,empty_tannot)) in let cases = List.map (function | FCL_aux (FCL_Funcl (_,pexp), ann) -> pexp) fcls in @@ -1576,7 +1577,7 @@ let split_defs all_errors splits defs = | L_undef -> let nexp = fabricate_nexp l annot in let typ = subst_src_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in - DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,None))),(l,None))], + DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))], [kid,nexp]) | _ -> (Reporting_basic.print_err false true lit_l "Monomorphisation" @@ -1622,7 +1623,7 @@ let split_defs all_errors splits defs = let kids = equal_kids (env_of_annot p_id_annot) kid in let ksubst = KidSet.fold (fun k b -> KBindings.add k nexp b) kids KBindings.empty in let typ = subst_src_typ ksubst (typ_of_annot p_id_annot) in - DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,None))], + DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))], KBindings.bindings ksubst) | P_aux (_,(l',_)) -> (Reporting_basic.print_err false true l' "Monomorphisation" @@ -2180,22 +2181,23 @@ and sizes_of_typarg (Typ_arg_aux (ta,_)) = -> KidSet.empty | Typ_arg_typ typ -> sizes_of_typ typ -let sizes_of_annot = function - | _,None -> KidSet.empty - | _,Some (env,typ,_) -> sizes_of_typ (Env.base_typ_of env typ) +let sizes_of_annot (l, tannot) = + match destruct_tannot tannot with + | None -> KidSet.empty + | Some (env,typ,_) -> sizes_of_typ (Env.base_typ_of env typ) let change_parameter_pat i = function | P_aux (P_id var, (l,_)) | P_aux (P_typ (_,P_aux (P_id var, (l,_))),_) -> - P_aux (P_id var, (l,None)), ([var],[]) + P_aux (P_id var, (l,empty_tannot)), ([var],[]) | P_aux (P_lit lit,(l,_)) -> let var = mk_id ("p#" ^ string_of_int i) in - let annot = (Generated l, None) in + let annot = (Generated l, empty_tannot) in let test : tannot exp = E_aux (E_app_infix (E_aux (E_app (mk_id "size_itself_int",[E_aux (E_id var,annot)]),annot), mk_id "==", E_aux (E_lit lit,annot)), annot) in - P_aux (P_id var, (l,None)), ([],[test]) + P_aux (P_id var, (l,empty_tannot)), ([],[test]) | P_aux (_,(l,_)) -> raise (Reporting_basic.err_unreachable l "Expected variable pattern") @@ -2214,7 +2216,7 @@ let var_maybe_used_in_exp exp var = let add_var_rebind unconditional exp var = if unconditional || var_maybe_used_in_exp exp var then let l = Generated Unknown in - let annot = (l,None) in + let annot = (l,empty_tannot) in E_aux (E_let (LB_aux (LB_val (P_aux (P_id var,annot), E_aux (E_app (mk_id "size_itself_int",[E_aux (E_id var,annot)]),annot)),annot),exp),annot) else exp @@ -2241,8 +2243,8 @@ let replace_with_the_value bound_nexps (E_aux (_,(l,_)) as exp) = let nexp = replace_size nexp in E_aux (E_cast (wrap (Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown), [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated Unknown)), - E_aux (E_app (Id_aux (Id "make_the_value",Generated Unknown),[exp]),(Generated l,None))), - (Generated l,None)) + E_aux (E_app (Id_aux (Id "make_the_value",Generated Unknown),[exp]),(Generated l,empty_tannot))), + (Generated l,empty_tannot)) in match typ with | Typ_aux (Typ_app (Id_aux (Id "range",_), @@ -2310,7 +2312,8 @@ let rewrite_size_parameters env (Defs defs) = print_endline ("Nexp map for " ^ string_of_id id); List.iter (fun (nexp, i) -> print_endline (" " ^ string_of_nexp nexp ^ " -> " ^ string_of_int i)) nexp_list in *) - let parameters_for = function + let parameters_for tannot = + match destruct_tannot tannot with | Some (env,typ,_) -> begin match Env.base_typ_of env typ with | Typ_aux (Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp size,_);_;_]),_) @@ -2361,7 +2364,7 @@ in *) P_aux (P_tup pats,(l,_)) -> let pats, vars_guards = mapat_extra change_parameter_pat to_change pats in let vars, new_guards = List.split vars_guards in - P_aux (P_tup pats,(l,None)), vars, new_guards + P_aux (P_tup pats,(l,empty_tannot)), vars, new_guards | P_aux (_,(l,_)) -> begin if IntSet.is_empty to_change then pat, [], [] @@ -2373,7 +2376,7 @@ in *) let vars, new_guards = List.concat vars, List.concat new_guards in let body = List.fold_left (add_var_rebind true) body vars in let merge_guards g1 g2 : tannot exp = - E_aux (E_app_infix (g1, mk_id "&", g2),(Generated Unknown,None)) in + E_aux (E_app_infix (g1, mk_id "&", g2),(Generated Unknown,empty_tannot)) in let guard = match guard, new_guards with | None, [] -> None | None, (h::t) -> Some (List.fold_left merge_guards h t) @@ -2403,7 +2406,7 @@ in *) let guard = match guard with | None -> None | Some exp -> Some (fold_exp { id_exp_alg with e_app = rewrite_e_app } exp) in - FCL_aux (FCL_Funcl (id,construct_pexp (pat,guard,body,(pl,None))),(l,None)) + FCL_aux (FCL_Funcl (id,construct_pexp (pat,guard,body,(pl,empty_tannot))),(l,empty_tannot)) in let rewrite_letbind lb = let rewrite_e_app (id,args) = @@ -2417,7 +2420,7 @@ in *) let rewrite_def = function | DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,funcls),(l,_))) -> (* TODO rewrite tannopt? *) - DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,List.map rewrite_funcl funcls),(l,None))) + DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,List.map rewrite_funcl funcls),(l,empty_tannot))) | DEF_val lb -> DEF_val (rewrite_letbind lb) | DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,annot))) as spec -> begin @@ -2433,7 +2436,7 @@ in *) | _ -> replace_type env typ in TypSchm_aux (TypSchm_ts (tq,typ),l) in - DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,None))) + DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,empty_tannot))) | _ -> spec | exception Not_found -> spec end @@ -2740,11 +2743,11 @@ let kids_bound_by_pat pat = let open Rewriter in fst (fold_pat ({ (compute_pat_alg KidSet.empty KidSet.union) with p_aux = - (function ((s,(P_var (P_aux (_,(_,Some (_,typ,_))),tpat) as p)), (_,Some (env,_,_) as ann)) -> - let kids = tyvars_of_typ typ in - let new_kids = KidSet.filter (fun kid -> not (is_kid_in_env env kid)) kids in + (function ((s,(P_var (P_aux (_, annot'),tpat) as p)), annot) when not (is_empty_tannot (snd annot')) -> + let kids = tyvars_of_typ (typ_of_annot annot') in + let new_kids = KidSet.filter (fun kid -> not (is_kid_in_env (env_of_annot annot) kid)) kids in let tpat_kids = kids_bound_by_typ_pat tpat in - KidSet.union s (KidSet.union new_kids tpat_kids), P_aux (p, ann) + KidSet.union s (KidSet.union new_kids tpat_kids), P_aux (p, annot) | ((s,p),ann) -> s, P_aux (p,ann)) }) pat) @@ -2853,20 +2856,20 @@ let mk_subrange_pattern vannot vstart vend = let end_len = Big_int.pred (Big_int.sub len vend) in (* Wrap pat in its type; in particular the type checker won't manage P_wild in the middle of a P_vector_concat *) - let pat = P_aux (P_typ (pat_typ_of pat, pat),(Generated (pat_loc pat),None)) in + let pat = P_aux (P_typ (pat_typ_of pat, pat),(Generated (pat_loc pat),empty_tannot)) in let pats = if Big_int.greater end_len Big_int.zero then [pat;P_aux (P_typ (vector_typ (nconstant end_len) ord typ, - P_aux (P_wild,(dummyl,None))),(dummyl,None))] + P_aux (P_wild,(dummyl,empty_tannot))),(dummyl,empty_tannot))] else [pat] in let pats = if Big_int.greater vstart Big_int.zero then (P_aux (P_typ (vector_typ (nconstant vstart) ord typ, - P_aux (P_wild,(dummyl,None))),(dummyl,None)))::pats + P_aux (P_wild,(dummyl,empty_tannot))),(dummyl,empty_tannot)))::pats else pats in let pats = if ord' = Ord_inc then pats else List.rev pats in - P_aux (P_vector_concat pats,(Generated (fst vannot),None))) + P_aux (P_vector_concat pats,(Generated (fst vannot),empty_tannot))) | _ -> None (* If the expression matched on in a case expression is a function argument, @@ -3161,7 +3164,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = in let r = (* Check for bitvector types with parametrised sizes *) - match annot with + match destruct_tannot annot with | None -> r | Some (tenv,typ,_) -> let typ = Env.base_typ_of tenv typ in @@ -3209,7 +3212,7 @@ and analyse_lexp fn_id env assigns deps (LEXP_aux (lexp,(l,_))) = then assigns, empty else Bindings.add id deps assigns, empty | LEXP_memory (id,es) -> - let _, assigns, r = analyse_exp fn_id env assigns (E_aux (E_tuple es,(Unknown,None))) in + let _, assigns, r = analyse_exp fn_id env assigns (E_aux (E_tuple es,(Unknown,empty_tannot))) in assigns, r | LEXP_tup lexps | LEXP_vector_concat lexps -> @@ -3353,7 +3356,7 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions = (* When there's no argument to case split on for a kid, we'll add a case expression instead *) let env = pat_env_of pat in - let split = default_split (Some (env,int_typ,no_effect)) (KidSet.singleton kid) in + let split = default_split (mk_tannot env int_typ no_effect) (KidSet.singleton kid) in let extra_splits = ExtraSplits.singleton (fn_id, fn_l) (KBindings.singleton kid split) in KBindings.add kid (Have (ArgSplits.empty, extra_splits)) kid_deps @@ -3585,7 +3588,7 @@ let add_extra_splits extras (Defs defs) = KBindings.fold (fun kid detail (exp,split_list) -> let nexp = Nexp_aux (Nexp_var kid,l) in let var = fresh_sz_var () in - let size_annot = Some (env_of e,atom_typ nexp,no_effect) in + let size_annot = mk_tannot (env_of e) (atom_typ nexp) no_effect in let loc = match Analysis.translate_loc l with | Some l -> l | None -> @@ -3666,7 +3669,7 @@ let rewrite_app env typ (id,args) = E_aux (E_cast (midtyp, E_aux (E_app (mk_id "subrange_subrange_concat", [vector1; start1; end1; vector2; start2; end2]), - (Unknown,None))),(Unknown,None))]) + (Unknown,empty_tannot))),(Unknown,empty_tannot))]) | [E_aux (E_app (append, [e1; E_aux (E_app (slice1, @@ -3685,7 +3688,7 @@ let rewrite_app env typ (id,args) = E_aux (E_cast (midtyp, E_aux (E_app (mk_id "slice_slice_concat", [vector1; start1; length1; vector2; start2; length2]), - (Unknown,None))),(Unknown,None))]) + (Unknown,empty_tannot))),(Unknown,empty_tannot))]) (* variable-range @ variable-range *) | [E_aux (E_app (subrange1, @@ -3697,7 +3700,7 @@ let rewrite_app env typ (id,args) = E_cast (typ, E_aux (E_app (mk_id "subrange_subrange_concat", [vector1; start1; end1; vector2; start2; end2]), - (Unknown,None))) + (Unknown,empty_tannot))) (* variable-slice @ variable-slice *) | [E_aux (E_app (slice1, @@ -3708,7 +3711,7 @@ let rewrite_app env typ (id,args) = not (is_constant length1 || is_constant length2) -> E_cast (typ, E_aux (E_app (mk_id "slice_slice_concat", - [vector1; start1; length1; vector2; start2; length2]),(Unknown,None))) + [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot))) | [E_aux (E_app (append1, [e1; @@ -3726,8 +3729,8 @@ let rewrite_app env typ (id,args) = [e1; E_aux (E_cast (midtyp, E_aux (E_app (mk_id "slice_zeros_concat", - [vector1; start1; length1; length2]),(Unknown,None))),(Unknown,None))]), - (Unknown,None))) + [vector1; start1; length1; length2]),(Unknown,empty_tannot))),(Unknown,empty_tannot))]), + (Unknown,empty_tannot))) | _ -> E_app (id,args) @@ -3819,7 +3822,7 @@ let rewrite_app env typ (id,args) = let (_,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in E_cast (vector_typ nlen order bittyp, E_aux (E_app (mk_id "sext_slice", [vector1; start1; length1]), - (Unknown,None))) + (Unknown,empty_tannot))) end | _ -> E_app (id,args) @@ -3840,8 +3843,12 @@ let rewrite_app env typ (id,args) = else E_app (id,args) let rewrite_aux = function - | (E_app (id,args),((_,Some (env,ty,_)) as annot)) -> - E_aux (rewrite_app env ty (id,args),annot) + | E_app (id,args), (l, tannot) -> + begin match destruct_tannot tannot with + | Some (env, ty, _) -> + E_aux (rewrite_app env ty (id,args), (l, tannot)) + | None -> E_aux (E_app (id, args), (l, tannot)) + end | exp,annot -> E_aux (exp,annot) let mono_rewrite defs = @@ -3880,8 +3887,8 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ = in let at_least_one = ref None in let rec aux (Typ_aux (src_t,src_l) as src_typ) (Typ_aux (tar_t,tar_l) as tar_typ) = - let src_ann = Some (env,src_typ,no_effect) in - let tar_ann = Some (env,tar_typ,no_effect) in + let src_ann = mk_tannot env src_typ no_effect in + let tar_ann = mk_tannot env tar_typ no_effect in match src_t, tar_t with | Typ_tup typs, Typ_tup typs' -> let ps,es = List.split (List.map2 aux typs typs') in @@ -3905,7 +3912,7 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ = E_aux (E_app (Id_aux (Id "bitvector_cast", genunk), [E_aux (E_id var, (genunk, src_ann))]), (genunk, tar_ann))), (genunk, tar_ann)) - | _ -> + | _ -> let var = fresh () in P_aux (P_id var,(Generated src_l,src_ann)), E_aux (E_id var,(Generated src_l,tar_ann)) @@ -3920,13 +3927,13 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ = let pat, e' = aux src_typ' target_typ' in match !at_least_one with | Some one_target_typ -> begin - let src_ann = Some (env,src_typ,no_effect) in - let tar_ann = Some (env,target_typ,no_effect) in + let src_ann = mk_tannot env src_typ no_effect in + let tar_ann = mk_tannot env target_typ no_effect in match src_typ' with (* Simple case with just the bitvector; don't need to pull apart value *) | Typ_aux (Typ_app _,_) -> (fun var exp -> - let exp_ann = Some (env,typ_of exp,effect_of exp) in + let exp_ann = mk_tannot env (typ_of exp) (effect_of exp) in E_aux (E_let (LB_aux (LB_val (P_aux (P_typ (one_target_typ, P_aux (P_id var,(genunk,tar_ann))),(genunk,tar_ann)), E_aux (E_app (Id_aux (Id "bitvector_cast",genunk), [E_aux (E_id var,(genunk,src_ann))]),(genunk,tar_ann))),(genunk,tar_ann)), @@ -3937,7 +3944,7 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ = (Generated exp_l,tar_ann))) | _ -> (fun var exp -> - let exp_ann = Some (env,typ_of exp,effect_of exp) in + let exp_ann = mk_tannot env (typ_of exp) (effect_of exp) in E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id var,(genunk,src_ann))),(genunk,src_ann)), E_aux (E_let (LB_aux (LB_val (P_aux (P_id var,(genunk,tar_ann)),e'),(genunk,tar_ann)), exp),(genunk,exp_ann))),(genunk,exp_ann))), diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index ebb703db..713cfb34 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1066,7 +1066,7 @@ let doc_exp_lem, doc_let_lem = raise (Reporting_basic.err_unreachable l "E_vector_subrange should have been rewritten before pretty-printing") | E_field((E_aux(_,(l,fannot)) as fexp),id) -> - (match fannot with + (match destruct_tannot fannot with | Some(env, (Typ_aux (Typ_id tid, _)), _) | Some(env, (Typ_aux (Typ_app (tid, _), _)), _) when Env.is_record tid env -> @@ -1115,23 +1115,23 @@ let doc_exp_lem, doc_let_lem = | E_tuple exps -> parens (align (group (separate_map (comma ^^ break 1) expN exps))) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> - let recordtyp = match annot with + let recordtyp = match destruct_tannot annot with | Some (env, Typ_aux (Typ_id tid,_), _) | Some (env, Typ_aux (Typ_app (tid, _), _), _) -> (* when Env.is_record tid env -> *) tid - | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in + | _ -> raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in let epp = enclose_record (align (separate_map (semi_sp ^^ break 1) (doc_fexp ctxt recordtyp) fexps)) in if aexp_needed then parens epp else epp | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> - let recordtyp, env = match annot with + let recordtyp, env = match destruct_tannot annot with | Some (env, Typ_aux (Typ_id tid,_), _) | Some (env, Typ_aux (Typ_app (tid, _), _), _) when Env.is_record tid env -> tid, env - | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in + | _ -> raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in if List.length fexps > 1 then let _,fields = Env.get_record recordtyp env in let var, let_pp = @@ -1464,8 +1464,8 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with let args_of_typ l env typs = let arg i typ = let id = mk_id ("arg" ^ string_of_int i) in - (P_aux (P_id id, (l, Some (env, typ, no_effect))), typ), - E_aux (E_id id, (l, Some (env, typ, no_effect))) in + (P_aux (P_id id, (l, mk_tannot env typ no_effect)), typ), + E_aux (E_id id, (l, mk_tannot env typ no_effect)) in List.split (List.mapi arg typs) let rec untuple_args_pat typ (P_aux (paux, ((l, _) as annot)) as pat) = @@ -1479,12 +1479,12 @@ let rec untuple_args_pat typ (P_aux (paux, ((l, _) as annot)) as pat) = let identity = (fun body -> body) in match paux, tup_typs with | P_tup [], _ -> - let annot = (l, Some (Env.empty, unit_typ, no_effect)) in + let annot = (l, mk_tannot Env.empty unit_typ no_effect) in [P_aux (P_lit (mk_lit L_unit), annot), unit_typ], identity | P_tup pats, Some typs -> List.combine pats typs, identity | P_tup pats, _ -> raise (Reporting_basic.err_unreachable l "Tuple pattern against non-tuple type") | P_wild, Some typs -> - let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))), typ in + let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)), typ in List.map wild typs, identity | P_typ (_, pat), _ -> untuple_args_pat typ pat | P_as _, Some typs | P_id _, Some typs -> diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index a4d446d3..75284418 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -740,7 +740,7 @@ let doc_exp_lem, doc_let_lem = "Unexpected number of arguments for early_return builtin") end | _ -> - begin match annot with + begin match destruct_tannot annot with | Some (env, _, _) when Env.is_union_constructor f env -> let epp = match args with @@ -751,7 +751,7 @@ let doc_exp_lem, doc_let_lem = parens (separate_map comma (expV false) args) in wrap_parens (align epp) | _ -> - let call, is_extern = match annot with + let call, is_extern = match destruct_tannot annot with | Some (env, _, _) when Env.is_extern f env "lem" -> string (Env.get_extern f env "lem"), true | _ -> doc_id_lem f, false in @@ -774,7 +774,7 @@ let doc_exp_lem, doc_let_lem = "E_vector_subrange should have been rewritten before pretty-printing") | E_field((E_aux(_,(l,fannot)) as fexp),id) -> let ft = typ_of_annot (l,fannot) in - (match fannot with + (match destruct_tannot fannot with | Some(env, (Typ_aux (Typ_id tid, _)), _) | Some(env, (Typ_aux (Typ_app (tid, _), _)), _) when Env.is_record tid env -> @@ -806,22 +806,22 @@ let doc_exp_lem, doc_let_lem = | E_tuple exps -> parens (align (group (separate_map (comma ^^ break 1) expN exps))) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> - let recordtyp = match annot with + let recordtyp = match destruct_tannot annot with | Some (env, Typ_aux (Typ_id tid,_), _) | Some (env, Typ_aux (Typ_app (tid, _), _), _) -> (* when Env.is_record tid env -> *) tid - | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in + | _ -> raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in wrap_parens (anglebars (space ^^ (align (separate_map (semi_sp ^^ break 1) (doc_fexp ctxt recordtyp) fexps)) ^^ space)) | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> - let recordtyp = match annot with + let recordtyp = match destruct_tannot annot with | Some (env, Typ_aux (Typ_id tid,_), _) | Some (env, Typ_aux (Typ_app (tid, _), _), _) when Env.is_record tid env -> tid - | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in + | _ -> raise (report l ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in @@ -1211,8 +1211,8 @@ let args_of_typ l env typ = | typ -> [typ] in let arg i typ = let id = mk_id ("arg" ^ string_of_int i) in - P_aux (P_id id, (l, Some (env, typ, no_effect))), - E_aux (E_id id, (l, Some (env, typ, no_effect))) in + P_aux (P_id id, (l, mk_tannot env typ no_effect)), + E_aux (E_id id, (l, mk_tannot env typ no_effect)) in List.split (List.mapi arg typs) let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) = @@ -1221,11 +1221,11 @@ let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) = let identity = (fun body -> body) in match paux, taux with | P_tup [], _ -> - let annot = (l, Some (Env.empty, unit_typ, no_effect)) in + let annot = (l, mk_tannot Env.empty unit_typ no_effect) in [P_aux (P_lit (mk_lit L_unit), annot)], identity | P_tup pats, _ -> pats, identity | P_wild, Typ_tup typs -> - let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))) in + let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)) in List.map wild typs, identity | P_typ (_, pat), _ -> untuple_args_pat pat | P_as _, Typ_tup _ | P_id _, Typ_tup _ -> diff --git a/src/rewriter.ml b/src/rewriter.ml index f072f91f..01ff62b1 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -81,7 +81,7 @@ let effect_of_pexp (Pat_aux (pexp,(_,a))) = union_effects eff (effect_of_annot a) let effect_of_lb (LB_aux (_,(_,a))) = effect_of_annot a -let simple_annot l typ = (gen_loc l, Some (initial_env, typ, no_effect)) +let simple_annot l typ = (gen_loc l, mk_tannot initial_env typ no_effect) let lookup_generated_kid env kid = @@ -138,7 +138,7 @@ let fun_app_effects id env = with | _ -> no_effect -let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with +let fix_eff_exp (E_aux (e,((l,_) as annot))) = match destruct_tannot (snd annot) with | Some (env, typ, eff) -> let effsum = match e with | E_block es -> union_eff_exps es @@ -180,11 +180,11 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with | E_internal_return e1 -> effect_of e1 | E_internal_value v -> no_effect in - E_aux (e, (l, Some (env, typ, effsum))) + E_aux (e, (l, mk_tannot env typ effsum)) | None -> - E_aux (e, (l, None)) + E_aux (e, (l, empty_tannot)) -let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with +let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match destruct_tannot (snd annot) with | Some (env, typ, eff) -> let effsum = union_effects eff (match lexp with | LEXP_id _ -> no_effect @@ -200,45 +200,45 @@ let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with union_effects (effect_of_lexp lexp) (union_effects (effect_of e1) (effect_of e2)) | LEXP_field (lexp,_) -> effect_of_lexp lexp) in - LEXP_aux (lexp, (l, Some (env, typ, effsum))) + LEXP_aux (lexp, (l, mk_tannot env typ effsum)) | None -> - LEXP_aux (lexp, (l, None)) + LEXP_aux (lexp, (l, empty_tannot)) -let fix_eff_fexp (FE_aux (fexp,((l,_) as annot))) = match snd annot with +let fix_eff_fexp (FE_aux (fexp,((l,_) as annot))) = match destruct_tannot (snd annot) with | Some (env, typ, eff) -> let effsum = union_effects eff (match fexp with | FE_Fexp (_,e) -> effect_of e) in - FE_aux (fexp, (l, Some (env, typ, effsum))) + FE_aux (fexp, (l, mk_tannot env typ effsum)) | None -> - FE_aux (fexp, (l, None)) + FE_aux (fexp, (l, empty_tannot)) let fix_eff_fexps fexps = fexps (* FES_aux have no effect information *) -let fix_eff_opt_default (Def_val_aux (opt_default,((l,_) as annot))) = match snd annot with +let fix_eff_opt_default (Def_val_aux (opt_default,((l,_) as annot))) = match destruct_tannot (snd annot) with | Some (env, typ, eff) -> let effsum = union_effects eff (match opt_default with | Def_val_empty -> no_effect | Def_val_dec e -> effect_of e) in - Def_val_aux (opt_default, (l, Some (env, typ, effsum))) + Def_val_aux (opt_default, (l, mk_tannot env typ effsum)) | None -> - Def_val_aux (opt_default, (l, None)) + Def_val_aux (opt_default, (l, empty_tannot)) -let fix_eff_pexp (Pat_aux (pexp,((l,_) as annot))) = match snd annot with +let fix_eff_pexp (Pat_aux (pexp,((l,_) as annot))) = match destruct_tannot (snd annot) with | Some (env, typ, eff) -> let effsum = match pexp with | Pat_exp (_,e) -> effect_of e | Pat_when (_,e,e') -> union_effects (effect_of e) (effect_of e') in - Pat_aux (pexp, (l, Some (env, typ, effsum))) + Pat_aux (pexp, (l, mk_tannot env typ effsum)) | None -> - Pat_aux (pexp, (l, None)) + Pat_aux (pexp, (l, empty_tannot)) -let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match snd annot with +let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match destruct_tannot (snd annot) with | Some (env, typ, eff) -> let effsum = match lb with | LB_val (_,e) -> effect_of e in - LB_aux (lb, (l, Some (env, typ, effsum))) + LB_aux (lb, (l, mk_tannot env typ effsum)) | None -> - LB_aux (lb, (l, None)) + LB_aux (lb, (l, empty_tannot)) let explode s = let rec exp i l = if i < 0 then l else exp (i - 1) (s.[i] :: l) in @@ -287,7 +287,7 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) = let rewrite = rewriters.rewrite_pat rewriters in match pat with | P_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) -> - let ps = List.map (fun p -> P_aux (P_lit p, (l, Some (pat_env_of orig_pat, bit_typ, no_effect)))) + let ps = List.map (fun p -> P_aux (P_lit p, (l, mk_tannot (pat_env_of orig_pat) bit_typ no_effect))) (vector_string_to_bit_list l lit) in rewrap (P_vector ps) | P_lit _ | P_wild | P_id _ | P_var _ -> rewrap pat @@ -313,7 +313,7 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) = | E_block exps -> rewrap (E_block (List.map rewrite exps)) | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps)) | E_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) -> - let es = List.map (fun p -> E_aux (E_lit p, (l, Some (env_of orig_exp, bit_typ, no_effect)))) + let es = List.map (fun p -> E_aux (E_lit p, (l, mk_tannot (env_of orig_exp) bit_typ no_effect))) (vector_string_to_bit_list l lit) in rewrap (E_vector es) | E_id _ | E_lit _ -> rewrap exp diff --git a/src/rewrites.ml b/src/rewrites.ml index 5a903a40..5ed174ea 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -83,11 +83,11 @@ let get_loc_exp (E_aux (_,(l,_))) = l let gen_vs (id, spec) = Initial_check.extern_of_string dec_ord (mk_id id) spec -let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, Some (env, typ, effect))) +let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, mk_tannot env typ effect)) let annot_exp e_aux l env typ = annot_exp_effect e_aux l env typ no_effect -let annot_pat p_aux l env typ = P_aux (p_aux, (l, Some (env, typ, no_effect))) +let annot_pat p_aux l env typ = P_aux (p_aux, (l, mk_tannot env typ no_effect)) let annot_letbind (p_aux, exp) l env typ = - LB_aux (LB_val (annot_pat p_aux l env typ, exp), (l, Some (env, typ, effect_of exp))) + LB_aux (LB_val (annot_pat p_aux l env typ, exp), (l, mk_tannot env typ (effect_of exp))) let simple_num l n = E_aux ( E_lit (L_aux (L_num n, gen_loc l)), @@ -141,7 +141,7 @@ let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with | LEXP_vector_range (lexp,_,_) | LEXP_field (lexp,_) -> lexp_is_local_intro lexp env -let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with +let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match destruct_tannot annot with | Some (_, _, eff) -> effectful_effs eff | _ -> false @@ -238,18 +238,22 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = Typ_arg_aux (Typ_arg_order ord, l) in - let rewrite_annot = function - | (l, Some (env, typ, eff)) -> (l, Some (env, rewrite_typ env typ, eff)) - | (l, None) -> (l, None) + let rewrite_annot (l, tannot) = + match destruct_tannot tannot with + | Some (env, typ, eff) -> l, replace_typ (rewrite_typ env typ) tannot + | None -> l, empty_tannot in let rewrite_def rewriters = function - | DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), (l, Some (env, typ, eff)))) -> + | DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), (l, tannot))) when not (is_empty_tannot tannot) -> + let env = env_of_annot (l, tannot) in + let typ = typ_of_annot (l, tannot) in + let eff = effect_of_annot tannot in let typschm = match typschm with | TypSchm_aux (TypSchm_ts (tq, typ), l) -> TypSchm_aux (TypSchm_ts (tq, rewrite_typ env typ), l) in - let a = rewrite_annot (l, Some (env, typ, eff)) in + let a = rewrite_annot (l, mk_tannot env typ eff) in DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), a)) | d -> Rewriter.rewrite_def rewriters d in @@ -262,8 +266,11 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = let rewrite_bitvector_exps defs = let e_aux = function - | (E_vector es, ((l, Some (env, typ, eff)) as a)) when is_bitvector_typ typ -> - begin + | (E_vector es, ((l, tannot) as a)) when not (is_empty_tannot tannot) -> + let env = env_of_annot (l, tannot) in + let typ = typ_of_annot (l, tannot) in + let eff = effect_of_annot tannot in + if is_bitvector_typ typ then try let len = mk_lit_exp (L_num (Big_int.of_int (List.length es))) in let es = mk_exp (E_list (List.map strip_exp es)) in @@ -271,7 +278,8 @@ let rewrite_bitvector_exps defs = check_exp env exp typ with | _ -> E_aux (E_vector es, a) - end + else + E_aux (E_vector es, a) | (e_aux, a) -> E_aux (e_aux, a) in let rewrite_exp _ = fold_exp { id_exp_alg with e_aux = e_aux } in @@ -285,7 +293,7 @@ let rewrite_bitvector_exps defs = variables in scope. *) let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = let extract_typ_var l env nexp (id, (_, typ)) = - let var = E_aux (E_id id, (l, Some (env, typ, no_effect))) in + let var = E_aux (E_id id, (l, mk_tannot env typ no_effect)) in match destruct_atom_nexp env typ with | Some size when prove env (nc_eq size nexp) -> Some var (* AA: This next case is a bit of a hack... is there a more @@ -294,12 +302,12 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = scope. *) | Some size when prove env (nc_eq (nsum size (nint 1)) nexp) -> let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in - Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect)))) + Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, mk_tannot env (atom_typ (nsum size (nint 1))) no_effect))) | _ -> begin match destruct_vector env typ with | Some (len, _, _) when prove env (nc_eq len nexp) -> - Some (E_aux (E_app (mk_id "length", [var]), (l, Some (env, atom_typ len, no_effect)))) + Some (E_aux (E_app (mk_id "length", [var]), (l, mk_tannot env (atom_typ len) no_effect))) | _ -> None end in @@ -318,12 +326,12 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = let env = env_of orig_exp in match e_aux with | E_sizeof (Nexp_aux (Nexp_constant c, _) as nexp) -> - E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect))) + E_aux (E_lit (L_aux (L_num c, l)), (l, mk_tannot env (atom_typ nexp) no_effect)) | E_sizeof nexp -> begin match nexp_simp (rewrite_nexp_ids (env_of orig_exp) nexp) with | Nexp_aux (Nexp_constant c, _) -> - E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect))) + E_aux (E_lit (L_aux (L_num c, l)), (l, mk_tannot env (atom_typ nexp) no_effect)) | _ -> let locals = Env.get_locals env in let exps = Bindings.bindings locals @@ -428,7 +436,7 @@ let rewrite_sizeof (Defs defs) = let uvar = try Some (KBindings.find (orig_kid kid) inst) with Not_found -> None in match uvar with | Some (U_nexp nexp) -> - let sizeof = E_aux (E_sizeof nexp, (l, Some (env, atom_typ nexp, no_effect))) in + let sizeof = E_aux (E_sizeof nexp, (l, mk_tannot env (atom_typ nexp) no_effect)) in (try rewrite_trivial_sizeof_exp sizeof with | Type_error (l, err) -> raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))) @@ -554,11 +562,11 @@ let rewrite_sizeof (Defs defs) = let ptyp' = Typ_aux (Typ_tup (kid_typs @ typs), l) in (match pat with | P_tup pats -> - P_aux (P_tup (kid_pats @ pats), (l, Some (penv, ptyp', peff))) - | P_wild -> P_aux (pat, (l, Some (penv, ptyp', peff))) + P_aux (P_tup (kid_pats @ pats), (l, mk_tannot penv ptyp' peff)) + | P_wild -> P_aux (pat, (l, mk_tannot penv ptyp' peff)) | P_typ (Typ_aux (Typ_tup typs, l), pat) -> P_aux (P_typ (Typ_aux (Typ_tup (kid_typs @ typs), l), - rewrite_pat pat), (l, Some (penv, ptyp', peff))) + rewrite_pat pat), (l, mk_tannot penv ptyp' peff)) | P_as (_, id) | P_id id -> (* adding parameters here would change the type of id; we should remove the P_as/P_id here and add a let-binding to the body *) @@ -569,7 +577,7 @@ let rewrite_sizeof (Defs defs) = "unexpected pattern while rewriting function parameters for sizeof expressions")) | ptyp -> let ptyp' = Typ_aux (Typ_tup (kid_typs @ [ptyp]), l) in - P_aux (P_tup (kid_pats @ [paux]), (l, Some (penv, ptyp', peff))) in + P_aux (P_tup (kid_pats @ [paux]), (l, mk_tannot penv ptyp' peff)) in let pat,guard,exp,pannot = destruct_pexp pexp in let pat' = rewrite_pat pat in let guard' = match guard with @@ -907,7 +915,7 @@ let remove_vector_concat_pat pat = let typ = Env.base_typ_of env (typ_of_annot annot) in let eff = effect_of_annot (snd annot) in let (l,_) = annot in - let wild _ = P_aux (P_wild,(gen_loc l, Some (env, bit_typ, eff))) in + let wild _ = P_aux (P_wild,(gen_loc l, mk_tannot env bit_typ eff)) in if is_vector_typ typ then match p, vector_typ_args_of typ with | P_vector ps,_ -> acc @ ps @@ -1136,7 +1144,7 @@ let subst_id_pat pat (id1,id2) = fold_pat {id_pat_alg with p_id = p_id} pat let subst_id_exp exp (id1,id2) = - Ast_util.subst (Id_aux (id1,Parse_ast.Unknown)) (E_aux (E_id (Id_aux (id2,Parse_ast.Unknown)),(Parse_ast.Unknown,None))) exp + Ast_util.subst (Id_aux (id1,Parse_ast.Unknown)) (E_aux (E_id (Id_aux (id2,Parse_ast.Unknown)),(Parse_ast.Unknown,empty_tannot))) exp let rec pat_to_exp (P_aux (pat,(l,annot))) = let rewrap e = E_aux (e,(l,annot)) in @@ -1370,7 +1378,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = let rannot = simple_annot l typ in let elem = access_bit_exp rootid l typ idx in let e = annot_pat (P_id id) l env bit_typ in - let letbind = LB_aux (LB_val (e,elem), (l, Some (env, bit_typ, no_effect))) in + let letbind = LB_aux (LB_val (e,elem), (l, mk_tannot env bit_typ no_effect)) in let letexp = (fun body -> let (E_aux (_,(_,bannot))) = body in if IdSet.mem id (find_used_vars body) @@ -1614,7 +1622,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) = if (effectful e) then let e = rewrite_rec e in let (E_aux (_,(el,eannot))) = e in - let pat_e' = fresh_id_pat "p__" (el, Some (env_of e, typ_of e, no_effect)) in + let pat_e' = fresh_id_pat "p__" (el, mk_tannot (env_of e) (typ_of e) no_effect) in let exp_e' = pat_to_exp pat_e' in let letbind_e = LB_aux (LB_val (pat_e',e), (el,eannot)) in let exp' = case_exp exp_e' (typ_of full_exp) clauses in @@ -1631,7 +1639,7 @@ let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fd (pat,guard,exp,annot) in let cs = rewrite_guarded_clauses l (List.map clause funcls) in List.map (fun (pat,exp,annot) -> - FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Parse_ast.Unknown,None))),annot)) cs + FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Parse_ast.Unknown,empty_tannot))),annot)) cs | _ -> funcls (* TODO is the empty list possible here? *) in FD_aux (FD_function(r,t,e,funcls),(l,fdannot)) @@ -1681,14 +1689,15 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f | E_block exps -> let rec walker exps = match exps with | [] -> [] - | (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps - when lexp_is_local_intro le env && not (lexp_is_effectful le) -> - let (le', re') = rewrite_lexp_to_rhs le in - let e' = re' (rewrite_base e) in - let exps' = walker exps in - let effects = union_eff_exps exps' in - let block = E_aux (E_block exps', (l, Some (env, unit_typ, effects))) in - [fix_eff_exp (E_aux (E_var(le', e', block), annot))] + | (E_aux(E_assign(le,e), (l, tannot)) as exp)::exps + when not (is_empty_tannot tannot) && lexp_is_local_intro le (env_of_annot (l, tannot)) && not (lexp_is_effectful le) -> + let env = env_of_annot (l, tannot) in + let (le', re') = rewrite_lexp_to_rhs le in + let e' = re' (rewrite_base e) in + let exps' = walker exps in + let effects = union_eff_exps exps' in + let block = E_aux (E_block exps', (l, mk_tannot env unit_typ effects)) in + [fix_eff_exp (E_aux (E_var(le', e', block), annot))] (*| ((E_aux(E_if(c,t,e),(l,annot))) as exp)::exps -> let vars_t = introduced_variables t in let vars_e = introduced_variables e in @@ -1919,7 +1928,7 @@ let rewrite_defs_early_return (Defs defs) = let annot = match List.map get_return_pexp pes with | Pat_aux (Pat_exp (_, E_aux (_, annot)), _) :: _ -> annot | Pat_aux (Pat_when (_, _, E_aux (_, annot)), _) :: _ -> annot - | [] -> (Parse_ast.Unknown, None) in + | [] -> (Parse_ast.Unknown, empty_tannot) in if List.for_all is_return_pexp pes then E_return (E_aux (E_case (e, List.map get_return_pexp pes), annot)) else E_case (e, pes) in @@ -1945,12 +1954,15 @@ let rewrite_defs_early_return (Defs defs) = let full_exp = propagate_exp_effect (E_aux (exp, (l, annot))) in let env = env_of full_exp in match full_exp with - | E_aux (E_return exp, (l, Some (env, typ, eff))) -> + | E_aux (E_return exp, (l, tannot)) when not (is_empty_tannot tannot) -> (* Add escape effect annotation, since we use the exception mechanism of the state monad to implement early return in the Lem backend *) - let annot' = Some (env, typ, union_effects eff (mk_effect [BE_escape])) in - let exp' = add_e_cast (typ_of exp) exp in - E_aux (E_app (mk_id "early_return", [exp']), (l, annot')) + let typ = typ_of_annot (l, tannot) in + let env = env_of_annot (l, tannot) in + let eff = effect_of_annot tannot in + let tannot' = mk_tannot env typ (union_effects eff (mk_effect [BE_escape])) in + let exp' = add_e_cast (typ_of exp) exp in + E_aux (E_app (mk_id "early_return", [exp']), (l, tannot')) | _ -> full_exp in (* Make sure that all final leaves of an expression (e.g. all branches of @@ -1998,10 +2010,10 @@ let rewrite_defs_early_return (Defs defs) = (if is_return exp' then get_return exp' else exp) else exp in - let a = match a with - | (l, Some (env, typ, eff)) -> - (l, Some (env, typ, union_effects eff (effect_of exp))) - | _ -> a in + let a = match destruct_tannot (snd a) with + | Some (env, typ, eff) -> + (fst a, mk_tannot env typ (union_effects eff (effect_of exp))) + | _ -> a in FCL_aux (FCL_Funcl (id, construct_pexp (pat, guard, exp, pannot)), a) in let rewrite_fun_early_return rewriters @@ -2016,14 +2028,14 @@ let rewrite_defs_early_return (Defs defs) = { rewriters_base with rewrite_fun = rewrite_fun_early_return } (Defs (early_ret_spec @ defs)) -let swaptyp typ (l,tannot) = match tannot with - | Some (env, typ', eff) -> (l, Some (env, typ, eff)) +let swaptyp typ (l,tannot) = match destruct_tannot tannot with + | Some (env, typ', eff) -> (l, mk_tannot env typ eff) | _ -> raise (Reporting_basic.err_unreachable l "swaptyp called with empty type annotation") let is_funcl_rec (FCL_aux (FCL_Funcl (id, pexp), _)) = let pat,guard,exp,pannot = destruct_pexp pexp in let exp = match guard with None -> exp - | Some exp' -> E_aux (E_block [exp';exp],(Parse_ast.Unknown,None)) in + | Some exp' -> E_aux (E_block [exp';exp],(Parse_ast.Unknown,empty_tannot)) in fst (fold_exp { (compute_exp_alg false (||) ) with e_app = (fun (f, es) -> @@ -2126,7 +2138,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) = let val_spec = VS_aux (VS_val_spec (mk_typschm typquant fun_typ, id, (fun _ -> None), false), - (Parse_ast.Unknown, None)) + (Parse_ast.Unknown, empty_tannot)) in let fundef = FD_aux (FD_function (r_o, t_o, e_o, funcls), fdannot) in [DEF_spec val_spec; DEF_fundef fundef] @ defs @@ -2173,13 +2185,17 @@ let rewrite_fix_val_specs (Defs defs) = let e_aux val_specs (exp, (l, annot)) = match fix_eff_exp (E_aux (exp, (l, annot))) with - | E_aux (E_app_infix (_, f, _) as exp, (l, Some (env, typ, eff))) - | E_aux (E_app (f, _) as exp, (l, Some (env, typ, eff))) -> + | E_aux (E_app_infix (_, f, _) as exp, (l, tannot)) + | E_aux (E_app (f, _) as exp, (l, tannot)) + when not (is_empty_tannot tannot) -> + let env = env_of_annot (l, tannot) in + let typ = typ_of_annot (l, tannot) in + let eff = effect_of_annot tannot in let vs = find_vs env val_specs f in (* The (updated) environment is used later by fix_eff_exp to look up the actual effects of a function call *) let env = Env.update_val_spec f vs env in - E_aux (exp, (l, Some (env, typ, union_effects eff (eff_of_vs vs)))) + E_aux (exp, (l, mk_tannot env typ (union_effects eff (eff_of_vs vs)))) | e_aux -> e_aux in @@ -2567,7 +2583,7 @@ let rewrite_defs_remove_blocks = let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp = (* body is a function : E_id variable -> actual body *) let (E_aux (_,(l,annot))) = v in - match annot with + match destruct_tannot annot with | Some (env, typ, eff) when is_unit_typ typ -> let body = body (annot_exp (E_lit (mk_lit L_unit)) l env unit_typ) in let body_typ = try typ_of body with _ -> unit_typ in @@ -2964,7 +2980,7 @@ let fresh_stringappend_id () = id let unk = Parse_ast.Unknown -let unkt = (Parse_ast.Unknown, None) +let unkt = (Parse_ast.Unknown, empty_tannot) let construct_bool_match env (match_on : tannot exp) (pexp : tannot pexp) : tannot exp = let true_exp = annot_exp (E_lit (mk_lit L_true)) unk env bool_typ in @@ -3384,13 +3400,13 @@ let rewrite_defs_pat_lits rewrite_lit = match !guards with | [] -> pexp | (g :: gs) -> - let guard_annot = (fst annot, Some (env_of exp, bool_typ, no_effect)) in + let guard_annot = (fst annot, mk_tannot (env_of exp) bool_typ no_effect) in Pat_aux (Pat_when (pat, List.fold_left (fun g g' -> E_aux (E_app (mk_id "and_bool", [g; g']), guard_annot)) g gs, exp), annot) end | Pat_when (pat, guard, exp) -> begin let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat } pat in - let guard_annot = (fst annot, Some (env_of exp, bool_typ, no_effect)) in + let guard_annot = (fst annot, mk_tannot (env_of exp) bool_typ no_effect) in Pat_aux (Pat_when (pat, List.fold_left (fun g g' -> E_aux (E_app (mk_id "and_bool", [g; g']), guard_annot)) guard !guards, exp), annot) end in @@ -3562,7 +3578,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let env = env_of_annot annot in let typ = typ_of e1 in let eff = union_eff_exps [c;e1;e2] in - let v = E_aux (E_if (c,e1,e2), (gen_loc el, Some (env, typ, eff))) in + let v = E_aux (E_if (c,e1,e2), (gen_loc el, mk_tannot env typ eff)) in Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats)) | E_case (e1,ps) | E_try (e1, ps) -> let is_case = match expaux with E_case _ -> true | _ -> false in @@ -3587,7 +3603,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let rewrite_pexp (Pat_aux (pexp, (l, _))) = match pexp with | Pat_exp (pat, exp) -> let exp = rewrite_var_updates (add_vars overwrite exp vars) in - let pannot = (l, Some (env_of exp, typ_of exp, effect_of exp)) in + let pannot = (l, mk_tannot (env_of exp) (typ_of exp) (effect_of exp)) in Pat_aux (Pat_exp (pat, exp), pannot) | Pat_when _ -> raise (Reporting_basic.err_unreachable l @@ -3689,9 +3705,10 @@ let remove_reference_types exp = | Typ_arg_aux (Typ_arg_typ t, a) -> Typ_arg_aux (Typ_arg_typ (rewrite_t t), a) | _ -> t_arg in - let rec rewrite_annot = function - | (l, None) -> (l, None) - | (l, Some (env, typ, eff)) -> (l, Some (env, rewrite_t typ, eff)) in + let rec rewrite_annot (l, tannot) = + match destruct_tannot tannot with + | None -> l, empty_tannot + | Some (_, typ, _) -> l, replace_typ (rewrite_t typ) tannot in map_exp_annot rewrite_annot exp @@ -3715,7 +3732,7 @@ let rewrite_defs_remove_superfluous_letbinds = when Id.compare id id' = 0 && small exp1 -> let (E_aux (_,e1annot)) = exp1 in E_aux (E_internal_return (exp1),e1annot) - | _ -> E_aux (exp,annot) + | _ -> E_aux (exp,annot) end | _ -> E_aux (exp,annot) in @@ -3729,7 +3746,6 @@ let rewrite_defs_remove_superfluous_letbinds = ; rewrite_def = rewrite_def ; rewrite_defs = rewrite_defs_base } - let rewrite_defs_remove_superfluous_returns = @@ -3808,12 +3824,12 @@ let merge_funcls (Defs defs) = | (FCL_aux (FCL_Funcl (id,_),(l,_)))::_ -> let var = mk_id "merge#var" in let l_g = Parse_ast.Generated l in - let ann_g : _ * tannot = (l_g,None) in + let ann_g : _ * tannot = (l_g,empty_tannot) in let clauses = List.map (fun (FCL_aux (FCL_Funcl (_,pexp),_)) -> pexp) fcls in FD_aux (FD_function (r,t,e,[ FCL_aux (FCL_Funcl (id,Pat_aux (Pat_exp (P_aux (P_id var,ann_g), E_aux (E_case (E_aux (E_id var,ann_g),clauses),ann_g)),ann_g)), - (l,None))]),ann) + (l,empty_tannot))]),ann) in let merge_in_def = function | DEF_fundef f -> DEF_fundef (merge_function f) @@ -4261,11 +4277,11 @@ let rewrite_case (e,ann) = (fst ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in let l = Parse_ast.Generated Parse_ast.Unknown in - let p = P_aux (P_wild, (l, None)) in - let ann' = Some (env, typ_of_annot ann, mk_effect [BE_escape]) in + let p = P_aux (P_wild, (l, empty_tannot)) in + let ann' = mk_tannot env (typ_of_annot ann) (mk_effect [BE_escape]) in (* TODO: use an expression that specifically indicates a failed pattern match *) - let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,None))),(l,ann')) in - E_aux (E_case (e1,cases@[Pat_aux (Pat_exp (p,b),(l,None))]),ann) + let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in + E_aux (E_case (e1,cases@[Pat_aux (Pat_exp (p,b),(l,empty_tannot))]),ann) end | _ -> E_aux (e,ann) diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 9481d6b1..b459610d 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -105,7 +105,8 @@ and free_type_names_t_args consider_var targs = nameset_bigunion (List.map (free_type_names_t_arg consider_var) targs) -let rec free_type_names_tannot consider_var = function +let rec free_type_names_tannot consider_var tannot = + match Type_check.destruct_tannot tannot with | None -> mt | Some (_, t, _) -> free_type_names_t consider_var t diff --git a/src/state.ml b/src/state.ml index 245d450c..70e53a52 100644 --- a/src/state.ml +++ b/src/state.ml @@ -69,9 +69,9 @@ let find_registers defs = List.fold_left (fun acc def -> match def with - | DEF_reg_dec (DEC_aux(DEC_reg (typ, id), annot)) -> - let env = match annot with - | (_, Some (env, _, _)) -> env + | DEF_reg_dec (DEC_aux(DEC_reg (typ, id), (_, tannot))) -> + let env = match destruct_tannot tannot with + | Some (env, _, _) -> env | _ -> Env.empty in (Env.expand_synonyms env typ, id) :: acc diff --git a/src/type_check.ml b/src/type_check.ml index 28e0f930..0c0fc212 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1953,6 +1953,25 @@ let subtype_check env typ1 typ2 = of these type annotations. *) type tannot = (Env.t * typ * effect) option +let mk_tannot env typ effect = Some (env, typ, effect) + +let empty_tannot = None +let is_empty_tannot = function + | None -> true + | Some _ -> false + +let destruct_tannot tannot = tannot + +let string_of_tannot tannot = + match destruct_tannot tannot with + | Some (_, typ, eff) -> + "Some (_, " ^ string_of_typ typ ^ ", " ^ string_of_effect eff ^ ")" + | None -> "None" + +let replace_typ typ = function + | Some (env, _, eff) -> Some (env, typ, eff) + | None -> None + let infer_lit env (L_aux (lit_aux, l) as lit) = match lit_aux with | L_unit -> unit_typ diff --git a/src/type_check.mli b/src/type_check.mli index 286c2be9..aa9d6385 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -220,7 +220,23 @@ val dvector_typ : Env.t -> nexp -> typ -> typ val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ (** The type of type annotations *) -type tannot = (Env.t * typ * effect) option +type tannot + +(** The canonical view of a type annotation is that it is a tuple + containing an environment (env), a type (typ), and an effect such + that check_X env (strip_X X) typ succeeds, where X is typically exp + (i.e an expression). Note that it is specifically not guaranteed + that calling destruct_tannot followed by mk_tannot returns an + identical type annotation. *) +val destruct_tannot : tannot -> (Env.t * typ * effect) option +val mk_tannot : Env.t -> typ -> effect -> tannot + +val empty_tannot : tannot +val is_empty_tannot : tannot -> bool + +val destruct_tannot : tannot -> (Env.t * typ * effect) option +val string_of_tannot : tannot -> string (* For debugging only *) +val replace_typ : typ -> tannot -> tannot (** {2 Removing type annotations} *) @@ -270,7 +286,7 @@ val check_case : Env.t -> typ -> unit pexp -> typ -> tannot pexp val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t -val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t +val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t val prove : Env.t -> n_constraint -> bool -- cgit v1.2.3