diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/anf.ml | 4 | ||||
| -rw-r--r-- | src/ast_util.ml | 25 | ||||
| -rw-r--r-- | src/ast_util.mli | 1 | ||||
| -rw-r--r-- | src/constant_fold.ml | 4 | ||||
| -rw-r--r-- | src/initial_check.ml | 8 | ||||
| -rw-r--r-- | src/interpreter.ml | 10 | ||||
| -rw-r--r-- | src/monomorphise.ml | 22 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 4 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 4 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 4 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 2 | ||||
| -rw-r--r-- | src/rewriter.ml | 53 | ||||
| -rw-r--r-- | src/rewriter.mli | 28 | ||||
| -rw-r--r-- | src/rewrites.ml | 25 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 4 | ||||
| -rw-r--r-- | src/type_check.ml | 20 |
16 files changed, 91 insertions, 127 deletions
@@ -569,7 +569,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = let aval, wrap = to_aval (anf field_exp) in wrap (mk_aexp (AE_field (aval, id, typ_of exp))) - | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) -> + | E_record_update (exp, fexps) -> let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = let aval, wrap = to_aval (anf exp) in (id, aval), wrap @@ -679,7 +679,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in wrap (mk_aexp (AE_val (AV_tuple (List.map fst avals)))) - | E_record (FES_aux (FES_Fexps (fexps, _), _)) -> + | E_record fexps -> let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = let aval, wrap = to_aval (anf exp) in (id, aval), wrap diff --git a/src/ast_util.ml b/src/ast_util.ml index ffe4c90e..48750ab7 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -393,7 +393,6 @@ let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown let mk_typquant qis = TypQ_aux (TypQ_tq qis, Parse_ast.Unknown) let mk_fexp id exp = FE_aux (FE_Fexp (id, exp), no_annot) -let mk_fexps fexps = FES_aux (FES_Fexps (fexps, false), no_annot) let mk_effect effs = Effect_aux (Effect_set (List.map (fun be_aux -> BE_aux (be_aux, Parse_ast.Unknown)) effs), Parse_ast.Unknown) @@ -461,8 +460,8 @@ and map_exp_annot_aux f = function | E_vector_append (exp1, exp2) -> E_vector_append (map_exp_annot f exp1, map_exp_annot f exp2) | E_list xs -> E_list (List.map (map_exp_annot f) xs) | E_cons (exp1, exp2) -> E_cons (map_exp_annot f exp1, map_exp_annot f exp2) - | E_record fexps -> E_record (map_fexps_annot f fexps) - | E_record_update (exp, fexps) -> E_record_update (map_exp_annot f exp, map_fexps_annot f fexps) + | E_record fexps -> E_record (List.map (map_fexp_annot f) fexps) + | E_record_update (exp, fexps) -> E_record_update (map_exp_annot f exp, List.map (map_fexp_annot f) fexps) | E_field (exp, id) -> E_field (map_exp_annot f exp, id) | E_case (exp, cases) -> E_case (map_exp_annot f exp, List.map (map_pexp_annot f) cases) | E_try (exp, cases) -> E_try (map_exp_annot f exp, List.map (map_pexp_annot f) cases) @@ -482,7 +481,6 @@ and map_opt_default_annot f (Def_val_aux (df, annot)) = Def_val_aux (map_opt_def and map_opt_default_annot_aux f = function | Def_val_empty -> Def_val_empty | Def_val_dec exp -> Def_val_dec (map_exp_annot f exp) -and map_fexps_annot f (FES_aux (FES_Fexps (fexps, b), annot)) = FES_aux (FES_Fexps (List.map (map_fexp_annot f) fexps, b), f annot) and map_fexp_annot f (FE_aux (FE_Fexp (id, exp), annot)) = FE_aux (FE_Fexp (id, map_exp_annot f exp), f annot) and map_pexp_annot f (Pat_aux (pexp, annot)) = Pat_aux (map_pexp_annot_aux f pexp, f annot) and map_pexp_annot_aux f = function @@ -770,9 +768,9 @@ let rec string_of_exp (E_aux (exp, _)) = | E_throw exp -> "throw " ^ string_of_exp exp | E_cons (x, xs) -> string_of_exp x ^ " :: " ^ string_of_exp xs | E_list xs -> "[|" ^ string_of_list ", " string_of_exp xs ^ "|]" - | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) -> + | E_record_update (exp, fexps) -> "{ " ^ string_of_exp exp ^ " with " ^ string_of_list "; " string_of_fexp fexps ^ " }" - | E_record (FES_aux (FES_Fexps (fexps, _), _)) -> + | E_record fexps -> "{ " ^ string_of_list "; " string_of_fexp fexps ^ " }" | E_var (lexp, binding, exp) -> "var " ^ string_of_lexp lexp ^ " = " ^ string_of_exp binding ^ " in " ^ string_of_exp exp | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")" @@ -1290,8 +1288,8 @@ let rec subst id value (E_aux (e_aux, annot) as exp) = | E_list exps -> E_list (List.map (subst id value) exps) | E_cons (exp1, exp2) -> E_cons (subst id value exp1, subst id value exp2) - | E_record fexps -> E_record (subst_fexps id value fexps) - | E_record_update (exp, fexps) -> E_record_update (subst id value exp, subst_fexps id value fexps) + | E_record fexps -> E_record (List.map (subst_fexp id value) fexps) + | E_record_update (exp, fexps) -> E_record_update (subst id value exp, List.map (subst_fexp id value) fexps) | E_field (exp, id') -> E_field (subst id value exp, id') | E_case (exp, pexps) -> @@ -1336,10 +1334,6 @@ and subst_pexp id value (Pat_aux (pexp_aux, annot)) = in Pat_aux (pexp_aux, annot) - -and subst_fexps id value (FES_aux (FES_Fexps (fexps, flag), annot)) = - FES_aux (FES_Fexps (List.map (subst_fexp id value) fexps, flag), annot) - and subst_fexp id value (FE_aux (FE_Fexp (id', exp), annot)) = FE_aux (FE_Fexp (id', subst id value exp), annot) @@ -1493,8 +1487,8 @@ let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, ann E_vector_append (locate f exp1, locate f exp2) | E_list exps -> E_list (List.map (locate f) exps) | E_cons (exp1, exp2) -> E_cons (locate f exp1, locate f exp2) - | E_record fexps -> E_record (locate_fexps f fexps) - | E_record_update (exp, fexps) -> E_record_update (locate f exp, locate_fexps f fexps) + | E_record fexps -> E_record (List.map (locate_fexp f) fexps) + | E_record_update (exp, fexps) -> E_record_update (locate f exp, List.map (locate_fexp f) fexps) | E_field (exp, id) -> E_field (locate f exp, locate_id f id) | E_case (exp, cases) -> E_case (locate f exp, List.map (locate_pexp f) cases) | E_let (letbind, exp) -> E_let (locate_letbind f letbind, locate f exp) @@ -1538,9 +1532,6 @@ and locate_lexp : 'a. (l -> l) -> 'a lexp -> 'a lexp = fun f (LEXP_aux (lexp_aux in LEXP_aux (lexp_aux, (f l, annot)) -and locate_fexps : 'a. (l -> l) -> 'a fexps -> 'a fexps = fun f (FES_aux (FES_Fexps (fexps, semi), (l, annot))) -> - FES_aux (FES_Fexps (List.map (locate_fexp f) fexps, semi), (f l, annot)) - and locate_fexp : 'a. (l -> l) -> 'a fexp -> 'a fexp = fun f (FE_aux (FE_Fexp (id, exp), (l, annot))) -> FE_aux (FE_Fexp (locate_id f id, locate f exp), (f l, annot)) diff --git a/src/ast_util.mli b/src/ast_util.mli index b7979e88..b6bce7c5 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -89,7 +89,6 @@ val mk_qi_id : kind_aux -> kid -> quant_item val mk_qi_nc : n_constraint -> quant_item val mk_qi_kopt : kinded_id -> quant_item val mk_fexp : id -> unit exp -> unit fexp -val mk_fexps : (unit fexp) list -> unit fexps val mk_letbind : unit pat -> unit exp -> unit letbind val unaux_exp : 'a exp -> 'a exp_aux diff --git a/src/constant_fold.ml b/src/constant_fold.ml index 0e34ed5b..b86f4ea5 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -72,7 +72,7 @@ and exp_of_value = | V_bool false -> mk_lit_exp L_false | V_string str -> mk_lit_exp (L_string str) | V_record ctors -> - mk_exp (E_record (FES_aux (FES_Fexps (List.map fexp_of_ctor (StringMap.bindings ctors), false), no_annot))) + mk_exp (E_record (List.map fexp_of_ctor (StringMap.bindings ctors))) | V_vector vs -> mk_exp (E_vector (List.map exp_of_value vs)) | V_tuple vs -> @@ -110,7 +110,7 @@ let rec is_constant (E_aux (e_aux, _)) = match e_aux with | E_lit _ -> true | E_vector exps -> List.for_all is_constant exps - | E_record (FES_aux (FES_Fexps (fexps, _), _)) -> List.for_all is_constant_fexp fexps + | E_record fexps -> List.for_all is_constant_fexp fexps | E_cast (_, exp) -> is_constant exp | E_tuple exps -> List.for_all is_constant exps | _ -> false diff --git a/src/initial_check.ml b/src/initial_check.ml index d1efb374..aa3a7136 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -595,14 +595,14 @@ and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.Pat_aux(pex | Parse_ast.Pat_when(pat,guard,exp) -> Pat_aux (Pat_when (to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord guard, to_ast_exp k_env def_ord exp), (l, ())) -and to_ast_fexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps : Parse_ast.exp list) : unit fexps option = +and to_ast_fexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps : Parse_ast.exp list) : unit fexp list option = match exps with - | [] -> Some(FES_aux(FES_Fexps([],false), (Parse_ast.Unknown,()))) + | [] -> Some [] | fexp::exps -> let maybe_fexp,maybe_error = to_ast_record_try k_env def_ord fexp in (match maybe_fexp,maybe_error with | Some(fexp),None -> (match (to_ast_fexps fail_on_error k_env def_ord exps) with - | Some(FES_aux(FES_Fexps(fexps,_),l)) -> Some(FES_aux(FES_Fexps(fexp::fexps,false),l)) + | Some(fexps) -> Some(fexp::fexps) | _ -> None) | None,Some(l,msg) -> if fail_on_error @@ -1138,7 +1138,7 @@ let generate_undefineds vs_ids (Defs defs) = [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) pat - (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]] + (mk_exp (E_record (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields)))]] | TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in let body = diff --git a/src/interpreter.ml b/src/interpreter.ml index 03877600..194812ca 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -401,13 +401,13 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | _ -> failwith ("Couldn't find id " ^ string_of_id id) end - | E_record (FES_aux (FES_Fexps (fexps, flag), fes_annot)) -> + | E_record fexps -> let evaluated, unevaluated = Util.take_drop is_value_fexp fexps in begin match unevaluated with | FE_aux (FE_Fexp (id, exp), fe_annot) :: fexps -> step exp >>= fun exp' -> - wrap (E_record (FES_aux (FES_Fexps (evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps, flag), fes_annot))) + wrap (E_record (evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps)) | [] -> List.map value_of_fexp fexps |> List.fold_left (fun record (field, v) -> StringMap.add field v record) StringMap.empty @@ -418,13 +418,13 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_record_update (exp, fexps) when not (is_value exp) -> step exp >>= fun exp' -> wrap (E_record_update (exp', fexps)) - | E_record_update (record, FES_aux (FES_Fexps (fexps, flag), fes_annot)) -> + | E_record_update (record, fexps) -> let evaluated, unevaluated = Util.take_drop is_value_fexp fexps in begin match unevaluated with | FE_aux (FE_Fexp (id, exp), fe_annot) :: fexps -> step exp >>= fun exp' -> - wrap (E_record_update (record, FES_aux (FES_Fexps (evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps, flag), fes_annot))) + wrap (E_record_update (record, evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps)) | [] -> List.map value_of_fexp fexps |> List.fold_left (fun record (field, v) -> StringMap.add field v record) (coerce_record (value_of_exp record)) @@ -444,7 +444,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_assign (LEXP_aux (LEXP_field (lexp, id), ul), exp) -> let open Type_check in let lexp_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp lexp)) in - let exp' = E_aux (E_record_update (lexp_exp, FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), ul)], false), ul)), ul) in + let exp' = E_aux (E_record_update (lexp_exp, [FE_aux (FE_Fexp (id, exp), ul)]), ul) in wrap (E_assign (lexp, exp')) | E_assign (LEXP_aux (LEXP_vector (vec, n), lexp_annot), exp) -> let open Type_check in diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 6a262df6..7626971e 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -615,8 +615,8 @@ let nexp_subst_fns substs = | E_vector_append (e1,e2) -> re (E_vector_append (s_exp e1,s_exp e2)) | E_list es -> re (E_list (List.map s_exp es)) | E_cons (e1,e2) -> re (E_cons (s_exp e1,s_exp e2)) - | E_record fes -> re (E_record (s_fexps fes)) - | E_record_update (e,fes) -> re (E_record_update (s_exp e, s_fexps fes)) + | E_record fes -> re (E_record (List.map s_fexp fes)) + | E_record_update (e,fes) -> re (E_record_update (s_exp e, List.map s_fexp fes)) | E_field (e,id) -> re (E_field (s_exp e,id)) | E_case (e,cases) -> re (E_case (s_exp e, List.map s_pexp cases)) | E_let (lb,e) -> re (E_let (s_letbind lb, s_exp e)) @@ -629,8 +629,6 @@ let nexp_subst_fns substs = | E_internal_return e -> re (E_internal_return (s_exp e)) | E_throw e -> re (E_throw (s_exp e)) | E_try (e,cases) -> re (E_try (s_exp e, List.map s_pexp cases)) - and s_fexps (FES_aux (FES_Fexps (fes,flag), (l,annot))) = - FES_aux (FES_Fexps (List.map s_fexp fes, flag), (l,s_tannot annot)) and s_fexp (FE_aux (FE_Fexp (id,e), (l,annot))) = FE_aux (FE_Fexp (id,s_exp e),(l,s_tannot annot)) and s_pexp = function @@ -954,7 +952,7 @@ let referenced_vars exp = { (compute_exp_alg IdSet.empty IdSet.union) with e_ref = (fun id -> IdSet.singleton id, E_ref id) } exp) -let assigned_vars_in_fexps (FES_aux (FES_Fexps (fes,_), _)) = +let assigned_vars_in_fexps fes = List.fold_left (fun vs (FE_aux (FE_Fexp (_,e),_)) -> IdSet.union vs (assigned_vars e)) IdSet.empty @@ -1460,8 +1458,8 @@ let split_defs all_errors splits defs = | E_internal_value _ -> raise (Reporting.err_unreachable l __POS__ ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp)) - and const_prop_fexps ref_vars substs assigns (FES_aux (FES_Fexps (fes,flag), annot)) = - FES_aux (FES_Fexps (List.map (const_prop_fexp ref_vars substs assigns) fes, flag), annot) + and const_prop_fexps ref_vars substs assigns fes = + List.map (const_prop_fexp ref_vars substs assigns) fes and const_prop_fexp ref_vars substs assigns (FE_aux (FE_Fexp (id,e), annot)) = FE_aux (FE_Fexp (id,fst (const_prop_exp ref_vars substs assigns e)),annot) and const_prop_pexp ref_vars substs assigns = function @@ -1995,8 +1993,8 @@ let split_defs all_errors splits defs = | E_vector_append (e1,e2) -> re (E_vector_append (map_exp e1,map_exp e2)) | E_list es -> re (E_list (List.map map_exp es)) | E_cons (e1,e2) -> re (E_cons (map_exp e1,map_exp e2)) - | E_record fes -> re (E_record (map_fexps fes)) - | E_record_update (e,fes) -> re (E_record_update (map_exp e, map_fexps fes)) + | E_record fes -> re (E_record (List.map map_fexp fes)) + | E_record_update (e,fes) -> re (E_record_update (map_exp e, List.map map_fexp fes)) | E_field (e,id) -> re (E_field (map_exp e,id)) | E_case (e,cases) -> re (E_case (map_exp e, List.concat (List.map map_pexp cases))) | E_let (lb,e) -> re (E_let (map_letbind lb, map_exp e)) @@ -2009,8 +2007,6 @@ let split_defs all_errors splits defs = | E_var (le,e1,e2) -> re (E_var (map_lexp le, map_exp e1, map_exp e2)) | E_internal_plet (p,e1,e2) -> re (E_internal_plet (check_single_pat p, map_exp e1, map_exp e2)) | E_internal_return e -> re (E_internal_return (map_exp e)) - and map_fexps (FES_aux (FES_Fexps (fes,flag), annot)) = - FES_aux (FES_Fexps (List.map map_fexp fes, flag), annot) and map_fexp (FE_aux (FE_Fexp (id,e), annot)) = FE_aux (FE_Fexp (id,map_exp e),annot) and map_pexp = function @@ -3087,11 +3083,11 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = | E_vector_update_subrange (e1,e2,e3,e4) -> let ds, assigns, r = non_det [e1;e2;e3;e4] in (merge_deps ds, assigns, r) - | E_record (FES_aux (FES_Fexps (fexps,_),_)) -> + | E_record fexps -> let es = List.map (function (FE_aux (FE_Fexp (_,e),_)) -> e) fexps in let ds, assigns, r = non_det es in (merge_deps ds, assigns, r) - | E_record_update (e,FES_aux (FES_Fexps (fexps,_),_)) -> + | E_record_update (e,fexps) -> let es = List.map (function (FE_aux (FE_Fexp (_,e),_)) -> e) fexps in let ds, assigns, r = non_det (e::es) in (merge_deps ds, assigns, r) diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index cf681ae5..f3a3fa54 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -242,9 +242,9 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = | E_if (c, t, e) -> separate space [string "if"; ocaml_atomic_exp ctx c; string "then"; ocaml_atomic_exp ctx t; string "else"; ocaml_atomic_exp ctx e] - | E_record (FES_aux (FES_Fexps (fexps, _), _)) -> + | E_record fexps -> enclose lbrace rbrace (group (separate_map (semi ^^ break 1) (ocaml_fexp ctx) fexps)) - | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) -> + | E_record_update (exp, fexps) -> enclose lbrace rbrace (separate space [ocaml_atomic_exp ctx exp; string "with"; separate_map (semi ^^ space) (ocaml_fexp ctx) fexps]) diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 4b466326..7cc61507 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1370,7 +1370,7 @@ let doc_exp, doc_let = if aexp_needed then parens epp else epp | E_tuple exps -> parens (align (group (separate_map (comma ^^ break 1) expN exps))) - | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> + | E_record fexps -> let recordtyp = match destruct_tannot annot with | Some (env, Typ_aux (Typ_id tid,_), _) | Some (env, Typ_aux (Typ_app (tid, _), _), _) -> @@ -1381,7 +1381,7 @@ let doc_exp, doc_let = (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,_),_))) -> + | E_record_update(e, fexps) -> let recordtyp, env = match destruct_tannot annot with | Some (env, Typ_aux (Typ_id tid,_), _) | Some (env, Typ_aux (Typ_app (tid, _), _), _) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 53b703bf..be790a1c 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -825,7 +825,7 @@ let doc_exp_lem, doc_let_lem = | E_cast(typ,e) -> expV aexp_needed e | E_tuple exps -> parens (align (group (separate_map (comma ^^ break 1) expN exps))) - | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> + | E_record fexps -> let recordtyp = match destruct_tannot annot with | Some (env, Typ_aux (Typ_id tid,_), _) | Some (env, Typ_aux (Typ_app (tid, _), _), _) -> @@ -835,7 +835,7 @@ let doc_exp_lem, doc_let_lem = 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,_),_))) -> + | E_record_update(e, fexps) -> let recordtyp = match destruct_tannot annot with | Some (env, Typ_aux (Typ_id tid,_), _) | Some (env, Typ_aux (Typ_app (tid, _), _), _) diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index fe533f00..b1efd11d 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -453,7 +453,7 @@ and doc_atomic_exp (E_aux (e_aux, _) as exp) = brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4]) | E_internal_value v -> string (Value.string_of_value v |> Util.green |> Util.clear) | _ -> parens (doc_exp exp) -and doc_fexps (FES_aux (FES_Fexps (fexps, _), _)) = +and doc_fexps fexps = separate_map (comma ^^ space) doc_fexp fexps and doc_fexp (FE_aux (FE_Fexp (id, exp), _)) = separate space [doc_id id; equals; doc_exp exp] diff --git a/src/rewriter.ml b/src/rewriter.ml index 082d9850..77070025 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -64,11 +64,10 @@ type 'a rewriters = { rewrite_defs : 'a rewriters -> 'a defs -> 'a defs; } - let effect_of_fpat (FP_aux (_,(_,a))) = effect_of_annot a let effect_of_lexp (LEXP_aux (_,(_,a))) = effect_of_annot a let effect_of_fexp (FE_aux (_,(_,a))) = effect_of_annot a -let effect_of_fexps (FES_aux (FES_Fexps (fexps,_),_)) = +let effect_of_fexps fexps = List.fold_left union_effects no_effect (List.map effect_of_fexp fexps) let effect_of_opt_default (Def_val_aux (_,(_,a))) = effect_of_annot a (* The typechecker does not seem to annotate pexps themselves *) @@ -295,16 +294,14 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) = | E_vector_append (v1,v2) -> rewrap (E_vector_append (rewrite v1,rewrite v2)) | E_list exps -> rewrap (E_list (List.map rewrite exps)) | E_cons(h,t) -> rewrap (E_cons (rewrite h,rewrite t)) - | E_record (FES_aux (FES_Fexps(fexps, bool),fannot)) -> + | E_record fexps -> rewrap (E_record - (FES_aux (FES_Fexps - (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> - FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot))) - | E_record_update (re,(FES_aux (FES_Fexps(fexps, bool),fannot))) -> + (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> + FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps)) + | E_record_update (re, fexps) -> rewrap (E_record_update ((rewrite re), - (FES_aux (FES_Fexps - (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> - FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot)))) + (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> + FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps))) | E_field(exp,id) -> rewrap (E_field(rewrite exp,id)) | E_case (exp,pexps) -> rewrap (E_case (rewrite exp, List.map (rewrite_pexp rewriters) pexps)) @@ -475,9 +472,9 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg = ; fP_Fpat = (fun (id,pat) -> FP_Fpat (id,pat)) } -type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, +type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux, 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, - 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg = + 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg = { e_block : 'exp list -> 'exp_aux ; e_nondet : 'exp list -> 'exp_aux ; e_id : id -> 'exp_aux @@ -498,8 +495,8 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_vector_append : 'exp * 'exp -> 'exp_aux ; e_list : 'exp list -> 'exp_aux ; e_cons : 'exp * 'exp -> 'exp_aux - ; e_record : 'fexps -> 'exp_aux - ; e_record_update : 'exp * 'fexps -> 'exp_aux + ; e_record : 'fexp list -> 'exp_aux + ; e_record_update : 'exp * 'fexp list -> 'exp_aux ; e_field : 'exp * id -> 'exp_aux ; e_case : 'exp * 'pexp list -> 'exp_aux ; e_try : 'exp * 'pexp list -> 'exp_aux @@ -528,8 +525,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; lEXP_aux : 'lexp_aux * 'a annot -> 'lexp ; fE_Fexp : id * 'exp -> 'fexp_aux ; fE_aux : 'fexp_aux * 'a annot -> 'fexp - ; fES_Fexps : 'fexp list * bool -> 'fexps_aux - ; fES_aux : 'fexps_aux * 'a annot -> 'fexps ; def_val_empty : 'opt_default_aux ; def_val_dec : 'exp -> 'opt_default_aux ; def_val_aux : 'opt_default_aux * 'a annot -> 'opt_default @@ -567,8 +562,8 @@ let rec fold_exp_aux alg = function | E_vector_append (e1,e2) -> alg.e_vector_append (fold_exp alg e1, fold_exp alg e2) | E_list es -> alg.e_list (List.map (fold_exp alg) es) | E_cons (e1,e2) -> alg.e_cons (fold_exp alg e1, fold_exp alg e2) - | E_record fexps -> alg.e_record (fold_fexps alg fexps) - | E_record_update (e,fexps) -> alg.e_record_update (fold_exp alg e, fold_fexps alg fexps) + | E_record fexps -> alg.e_record (List.map (fold_fexp alg) fexps) + | E_record_update (e,fexps) -> alg.e_record_update (fold_exp alg e, List.map (fold_fexp alg) fexps) | E_field (e,id) -> alg.e_field (fold_exp alg e, id) | E_case (e,pexps) -> alg.e_case (fold_exp alg e, List.map (fold_pexp alg) pexps) | E_try (e,pexps) -> alg.e_try (fold_exp alg e, List.map (fold_pexp alg) pexps) @@ -602,8 +597,6 @@ and fold_lexp alg (LEXP_aux (lexp_aux,annot)) = alg.lEXP_aux (fold_lexp_aux alg lexp_aux, annot) and fold_fexp_aux alg (FE_Fexp (id,e)) = alg.fE_Fexp (id, fold_exp alg e) and fold_fexp alg (FE_aux (fexp_aux,annot)) = alg.fE_aux (fold_fexp_aux alg fexp_aux,annot) -and fold_fexps_aux alg (FES_Fexps (fexps,b)) = alg.fES_Fexps (List.map (fold_fexp alg) fexps, b) -and fold_fexps alg (FES_aux (fexps_aux,annot)) = alg.fES_aux (fold_fexps_aux alg fexps_aux, annot) and fold_opt_default_aux alg = function | Def_val_empty -> alg.def_val_empty | Def_val_dec e -> alg.def_val_dec (fold_exp alg e) @@ -674,8 +667,6 @@ let id_exp_alg = ; lEXP_aux = (fun (lexp,annot) -> LEXP_aux (lexp,annot)) ; fE_Fexp = (fun (id,e) -> FE_Fexp (id,e)) ; fE_aux = (fun (fexp,annot) -> FE_aux (fexp,annot)) - ; fES_Fexps = (fun (fexps,b) -> FES_Fexps (fexps,b)) - ; fES_aux = (fun (fexp,annot) -> FES_aux (fexp,annot)) ; def_val_empty = Def_val_empty ; def_val_dec = (fun e -> Def_val_dec e) ; def_val_aux = (fun (defval,aux) -> Def_val_aux (defval,aux)) @@ -742,8 +733,12 @@ let compute_exp_alg bot join = ; e_vector_append = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_vector_append (e1,e2))) ; e_list = split_join (fun es -> E_list es) ; e_cons = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_cons (e1,e2))) - ; e_record = (fun (vs,fexps) -> (vs, E_record fexps)) - ; e_record_update = (fun ((v1,e1),(vf,fexp)) -> (join v1 vf, E_record_update (e1,fexp))) + ; e_record = (fun fexps -> + let vs, fexps = List.split fexps in + (join_list vs, E_record fexps)) + ; e_record_update = (fun ((v1,e1),fexps) -> + let (vps,fexps) = List.split fexps in + (join_list (v1::vps), E_record_update (e1,fexps))) ; e_field = (fun ((v1,e1),id) -> (v1, E_field (e1,id))) ; e_case = (fun ((v1,e1),pexps) -> let (vps,pexps) = List.split pexps in @@ -783,10 +778,6 @@ let compute_exp_alg bot join = ; lEXP_aux = (fun ((vl,lexp),annot) -> (vl, LEXP_aux (lexp,annot))) ; fE_Fexp = (fun (id,(v,e)) -> (v, FE_Fexp (id,e))) ; fE_aux = (fun ((vf,fexp),annot) -> (vf, FE_aux (fexp,annot))) - ; fES_Fexps = (fun (fexps,b) -> - let (vs,fexps) = List.split fexps in - (join_list vs, FES_Fexps (fexps,b))) - ; fES_aux = (fun ((vf,fexp),annot) -> (vf, FES_aux (fexp,annot))) ; def_val_empty = (bot, Def_val_empty) ; def_val_dec = (fun (v,e) -> (v, Def_val_dec e)) ; def_val_aux = (fun ((v,defval),aux) -> (v, Def_val_aux (defval,aux))) @@ -843,8 +834,8 @@ let pure_exp_alg bot join = ; e_vector_append = (fun (v1,v2) -> join v1 v2) ; e_list = join_list ; e_cons = (fun (v1,v2) -> join v1 v2) - ; e_record = (fun vs -> vs) - ; e_record_update = (fun (v1,vf) -> join v1 vf) + ; e_record = (fun vs -> join_list vs) + ; e_record_update = (fun (v1,vf) -> join_list (v1::vf)) ; e_field = (fun (v1,id) -> v1) ; e_case = (fun (v1,vps) -> join_list (v1::vps)) ; e_try = (fun (v1,vps) -> join_list (v1::vps)) @@ -873,8 +864,6 @@ let pure_exp_alg bot join = ; lEXP_aux = (fun (vl,annot) -> vl) ; fE_Fexp = (fun (id,v) -> v) ; fE_aux = (fun (vf,annot) -> vf) - ; fES_Fexps = (fun (vs,b) -> join_list vs) - ; fES_aux = (fun (vf,annot) -> vf) ; def_val_empty = bot ; def_val_dec = (fun v -> v) ; def_val_aux = (fun (v,aux) -> v) diff --git a/src/rewriter.mli b/src/rewriter.mli index 15e704df..9da94a99 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -107,7 +107,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg = (* fold over pat_aux expressions *) (* the type of interpretations of expressions *) -type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, +type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux, 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg = { e_block : 'exp list -> 'exp_aux @@ -130,8 +130,8 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_vector_append : 'exp * 'exp -> 'exp_aux ; e_list : 'exp list -> 'exp_aux ; e_cons : 'exp * 'exp -> 'exp_aux - ; e_record : 'fexps -> 'exp_aux - ; e_record_update : 'exp * 'fexps -> 'exp_aux + ; e_record : 'fexp list -> 'exp_aux + ; e_record_update : 'exp * 'fexp list -> 'exp_aux ; e_field : 'exp * id -> 'exp_aux ; e_case : 'exp * 'pexp list -> 'exp_aux ; e_try : 'exp * 'pexp list -> 'exp_aux @@ -160,8 +160,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; lEXP_aux : 'lexp_aux * 'a annot -> 'lexp ; fE_Fexp : id * 'exp -> 'fexp_aux ; fE_aux : 'fexp_aux * 'a annot -> 'fexp - ; fES_Fexps : 'fexp list * bool -> 'fexps_aux - ; fES_aux : 'fexps_aux * 'a annot -> 'fexps ; def_val_empty : 'opt_default_aux ; def_val_dec : 'exp -> 'opt_default_aux ; def_val_aux : 'opt_default_aux * 'a annot -> 'opt_default @@ -177,34 +175,34 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, val fold_pat : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg -> 'a pat -> 'pat (* fold over expressions *) -val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, +val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux, 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp -val fold_letbind : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, +val fold_letbind : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux, 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a letbind -> 'letbind -val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, +val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux, 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp -val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, +val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux, 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp -val fold_funcl : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, +val fold_funcl : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux, 'opt_default_aux,'opt_default,'a pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a funcl -> 'a funcl -val fold_function : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, +val fold_function : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux, 'opt_default_aux,'opt_default, 'a pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a fundef -> 'a fundef val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg val id_exp_alg : ('a,'a exp,'a exp_aux,'a lexp,'a lexp_aux,'a fexp, - 'a fexp_aux,'a fexps,'a fexps_aux, + 'a fexp_aux, 'a opt_default_aux,'a opt_default,'a pexp,'a pexp_aux, 'a letbind_aux,'a letbind, 'a pat,'a pat_aux,'a fpat,'a fpat_aux) exp_alg @@ -214,7 +212,7 @@ val compute_pat_alg : 'b -> ('b -> 'b -> 'b) -> val compute_exp_alg : 'b -> ('b -> 'b -> 'b) -> ('a,('b * 'a exp),('b * 'a exp_aux),('b * 'a lexp),('b * 'a lexp_aux),('b * 'a fexp), - ('b * 'a fexp_aux),('b * 'a fexps),('b * 'a fexps_aux), + ('b * 'a fexp_aux), ('b * 'a opt_default_aux),('b * 'a opt_default),('b * 'a pexp),('b * 'a pexp_aux), ('b * 'a letbind_aux),('b * 'a letbind), ('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) exp_alg @@ -224,7 +222,7 @@ val pure_pat_alg : 'b -> ('b -> 'b -> 'b) -> ('a,'b,'b,'b,'b) pat_alg val pure_exp_alg : 'b -> ('b -> 'b -> 'b) -> ('a,'b,'b,'b,'b,'b, 'b,'b,'b, - 'b,'b,'b,'b, + 'b,'b, 'b,'b, 'b,'b,'b,'b) exp_alg @@ -248,6 +246,4 @@ val fix_eff_pexp : tannot pexp -> tannot pexp val fix_eff_fexp : tannot fexp -> tannot fexp -val fix_eff_fexps : tannot fexps -> tannot fexps - val fix_eff_opt_default : tannot opt_default -> tannot opt_default diff --git a/src/rewrites.ml b/src/rewrites.ml index 2734e91f..8c1311a0 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -513,8 +513,8 @@ let rewrite_sizeof (Defs defs) = ; e_vector_append = (fun ((e1,e1'),(e2,e2')) -> (E_vector_append (e1,e2), E_vector_append (e1',e2'))) ; e_list = (fun es -> let (es, es') = List.split es in (E_list es, E_list es')) ; e_cons = (fun ((e1,e1'),(e2,e2')) -> (E_cons (e1,e2), E_cons (e1',e2'))) - ; e_record = (fun (fexps, fexps') -> (E_record fexps, E_record fexps')) - ; e_record_update = (fun ((e1,e1'),(fexp,fexp')) -> (E_record_update (e1,fexp), E_record_update (e1',fexp'))) + ; e_record = (fun fexps -> let (fexps, fexps') = List.split fexps in (E_record fexps, E_record fexps')) + ; e_record_update = (fun ((e1,e1'),fexps) -> let (fexps, fexps') = List.split fexps in (E_record_update (e1,fexps), E_record_update (e1',fexps'))) ; e_field = (fun ((e1,e1'),id) -> (E_field (e1,id), E_field (e1',id))) ; e_case = (fun ((e1,e1'),pexps) -> let (pexps, pexps') = List.split pexps in (E_case (e1,pexps), E_case (e1',pexps'))) ; e_try = (fun ((e1,e1'),pexps) -> let (pexps, pexps') = List.split pexps in (E_try (e1,pexps), E_try (e1',pexps'))) @@ -543,8 +543,6 @@ let rewrite_sizeof (Defs defs) = ; lEXP_aux = (fun ((lexp,lexp'),annot) -> (LEXP_aux (lexp,annot), LEXP_aux (lexp',annot))) ; fE_Fexp = (fun (id,(e,e')) -> (FE_Fexp (id,e), FE_Fexp (id,e'))) ; fE_aux = (fun ((fexp,fexp'),annot) -> (FE_aux (fexp,annot), FE_aux (fexp',annot))) - ; fES_Fexps = (fun (fexps,b) -> let (fexps, fexps') = List.split fexps in (FES_Fexps (fexps,b), FES_Fexps (fexps',b))) - ; fES_aux = (fun ((fexp,fexp'),annot) -> (FES_aux (fexp,annot), FES_aux (fexp',annot))) ; def_val_empty = (Def_val_empty, Def_val_empty) ; def_val_dec = (fun (e,e') -> (Def_val_dec e, Def_val_dec e')) ; def_val_aux = (fun ((defval,defval'),aux) -> (Def_val_aux (defval,aux), Def_val_aux (defval',aux))) @@ -1173,7 +1171,7 @@ let rec pat_to_exp ((P_aux (pat,(l,annot))) as p_aux) = | P_id id -> rewrap (E_id id) | P_app (id,pats) -> rewrap (E_app (id, List.map pat_to_exp pats)) | P_record (fpats,b) -> - rewrap (E_record (FES_aux (FES_Fexps (List.map fpat_to_fexp fpats,b),(l,annot)))) + rewrap (E_record (List.map fpat_to_fexp fpats)) | P_vector pats -> rewrap (E_vector (List.map pat_to_exp pats)) | P_vector_concat pats -> begin let empty_vec = E_aux (E_vector [], (l,())) in @@ -1728,8 +1726,8 @@ let rec rewrite_lexp_to_rhs ((LEXP_aux(lexp,((l,_) as annot))) as le) = let env = env_of_annot lannot in match Env.expand_synonyms env (typ_of_annot lannot) with | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env -> - let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in - (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), lannot)))) + let field_update exp = FE_aux (FE_Fexp (id, exp), annot) in + (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, [field_update exp]), lannot)))) | _ -> raise (Reporting.err_unreachable l __POS__ ("Unsupported lexp: " ^ string_of_lexp le)) end | _ -> raise (Reporting.err_unreachable l __POS__ ("Unsupported lexp: " ^ string_of_lexp le)) @@ -2590,7 +2588,7 @@ let rewrite_defs_letbind_effects = and value_optdefault (Def_val_aux (o,_)) = match o with | Def_val_empty -> true | Def_val_dec e -> value e - and value_fexps (FES_aux (FES_Fexps (fexps,_),_)) = + and value_fexps fexps = List.fold_left (fun b (FE_aux (FE_Fexp (_,e),_)) -> b && value e) true fexps in @@ -2621,11 +2619,6 @@ let rewrite_defs_letbind_effects = and n_pexpL (newreturn : bool) (pexps : 'a pexp list) (k : 'a pexp list -> 'a exp) : 'a exp = mapCont (n_pexp newreturn) pexps k - and n_fexps (fexps : 'a fexps) (k : 'a fexps -> 'a exp) : 'a exp = - let (FES_aux (FES_Fexps (fexps_aux,b),annot)) = fexps in - n_fexpL fexps_aux (fun fexps_aux -> - k (fix_eff_fexps (FES_aux (FES_Fexps (fexps_aux,b),annot)))) - and n_opt_default (opt_default : 'a opt_default) (k : 'a opt_default -> 'a exp) : 'a exp = let (Def_val_aux (opt_default,annot)) = opt_default in match opt_default with @@ -2774,11 +2767,11 @@ let rewrite_defs_letbind_effects = n_exp_name exp2 (fun exp2 -> k (rewrap (E_cons (exp1,exp2))))) | E_record fexps -> - n_fexps fexps (fun fexps -> + n_fexpL fexps (fun fexps -> k (rewrap (E_record fexps))) | E_record_update (exp1,fexps) -> n_exp_name exp1 (fun exp1 -> - n_fexps fexps (fun fexps -> + n_fexpL fexps (fun fexps -> k (rewrap (E_record_update (exp1,fexps))))) | E_field (exp1,id) -> n_exp_name exp1 (fun exp1 -> @@ -4155,7 +4148,7 @@ and fexps_of_mfpats mfpats flag annot = let fexp_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) = FE_aux (FE_Fexp (id, exp_of_mpat mpat), annot) in - FES_aux (FES_Fexps (List.map fexp_of_mfpat mfpats, flag), annot) + List.map fexp_of_mfpat mfpats and pat_of_mpat (MP_aux (mpat, annot)) = match mpat with diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index fa68c6f2..180b96b2 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -210,11 +210,11 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset. | E_vector_update(v,i,e) -> list_fv bound used set [v;i;e] | E_vector_update_subrange(v,i1,i2,e) -> list_fv bound used set [v;i1;i2;e] | E_vector_append(e1,e2) | E_cons(e1,e2) -> list_fv bound used set [e1;e2] - | E_record (FES_aux(FES_Fexps(fexps,_),_)) -> + | E_record fexps -> let used = Nameset.union (free_type_names_tannot consider_var tannot) used in List.fold_right (fun (FE_aux(FE_Fexp(_,e),_)) (b,u,s) -> fv_of_exp consider_var b u s e) fexps (bound,used,set) - | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> + | E_record_update(e, fexps) -> let b,u,s = fv_of_exp consider_var bound used set e in List.fold_right (fun (FE_aux(FE_Fexp(_,e),_)) (b,u,s) -> fv_of_exp consider_var b u s e) fexps (b,u,s) diff --git a/src/type_check.ml b/src/type_check.ml index d39ce27d..435c5cd8 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2293,7 +2293,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ annot_exp (E_list checked_xs) typ | None -> typ_error l ("List " ^ string_of_exp exp ^ " must have list type, got " ^ string_of_typ typ) end - | E_record_update (exp, FES_aux (FES_Fexps (fexps, flag), (l, ()))), _ -> + | E_record_update (exp, fexps), _ -> (* TODO: this could also infer exp - also fix code duplication with E_record below *) let checked_exp = crule check_exp env exp typ in let rectyp_id = match Env.expand_synonyms env typ with @@ -2308,8 +2308,8 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ let checked_exp = crule check_exp env exp field_typ' in FE_aux (FE_Fexp (field, checked_exp), (l, None)) in - annot_exp (E_record_update (checked_exp, FES_aux (FES_Fexps (List.map check_fexp fexps, flag), (l, None)))) typ - | E_record (FES_aux (FES_Fexps (fexps, flag), (l, ()))), _ -> + annot_exp (E_record_update (checked_exp, List.map check_fexp fexps)) typ + | E_record fexps, _ -> (* TODO: check record fields are total *) let rectyp_id = match Env.expand_synonyms env typ with | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env -> @@ -2323,7 +2323,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ let checked_exp = crule check_exp env exp field_typ' in FE_aux (FE_Fexp (field, checked_exp), (l, None)) in - annot_exp (E_record (FES_aux (FES_Fexps (List.map check_fexp fexps, flag), (l, None)))) typ + annot_exp (E_record (List.map check_fexp fexps)) typ | E_let (LB_aux (letbind, (let_loc, _)), exp), _ -> begin match letbind with @@ -3165,7 +3165,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = annot_exp (E_tuple inferred_exps) (mk_typ (Typ_tup (List.map typ_of inferred_exps))) | E_assign (lexp, bind) -> fst (bind_assignment env lexp bind) - | E_record_update (exp, FES_aux (FES_Fexps (fexps, flag), (l, ()))) -> + | E_record_update (exp, fexps) -> let inferred_exp = irule infer_exp env exp in let typ = typ_of inferred_exp in let rectyp_id = match Env.expand_synonyms env typ with @@ -3180,7 +3180,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let inferred_exp = crule check_exp env exp field_typ' in FE_aux (FE_Fexp (field, inferred_exp), (l, None)) in - annot_exp (E_record_update (inferred_exp, FES_aux (FES_Fexps (List.map check_fexp fexps, flag), (l, None)))) typ + annot_exp (E_record_update (inferred_exp, List.map check_fexp fexps)) typ | E_cast (typ, exp) -> let checked_exp = crule check_exp env exp typ in annot_exp (E_cast (typ, checked_exp)) typ @@ -3857,14 +3857,14 @@ and propagate_exp_effect_aux = function let p_cases = List.map propagate_pexp_effect cases in let case_eff = List.fold_left union_effects no_effect (List.map snd p_cases) in E_case (p_exp, List.map fst p_cases), union_effects (effect_of p_exp) case_eff - | E_record_update (exp, FES_aux (FES_Fexps (fexps, flag), (l, _))) -> + | E_record_update (exp, fexps) -> let p_exp = propagate_exp_effect exp in let p_fexps = List.map propagate_fexp_effect fexps in - E_record_update (p_exp, FES_aux (FES_Fexps (List.map fst p_fexps, flag), (l, None))), + E_record_update (p_exp, List.map fst p_fexps), List.fold_left union_effects no_effect (effect_of p_exp :: List.map snd p_fexps) - | E_record (FES_aux (FES_Fexps (fexps, flag), (l, _))) -> + | E_record fexps -> let p_fexps = List.map propagate_fexp_effect fexps in - E_record (FES_aux (FES_Fexps (List.map fst p_fexps, flag), (l, None))), + E_record (List.map fst p_fexps), List.fold_left union_effects no_effect (List.map snd p_fexps) | E_try (exp, cases) -> let p_exp = propagate_exp_effect exp in |