From 3d853e394b5bb5aa0862b56cfbb068aef8d2458a Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 21 Sep 2017 16:12:12 +0100 Subject: Simplify AST by removing LB_val_explicit and replace LB_val_implicit with just LB_val in AST also rename functions in rewriter.ml appropriately. --- src/ast.ml | 3 +- src/ast_util.ml | 9 ++-- src/initial_check.ml | 7 +-- src/monomorphise.ml | 19 +++---- src/ocaml_backend.ml | 2 +- src/parse_ast.ml | 3 +- src/parser.mly | 7 +-- src/parser2.mly | 2 +- src/pretty_print_lem.ml | 3 +- src/pretty_print_lem_ast.ml | 6 +-- src/pretty_print_ocaml.ml | 6 +-- src/pretty_print_sail.ml | 12 +---- src/rewriter.ml | 125 ++++++++++++++------------------------------ src/rewriter.mli | 3 +- src/spec_analysis.ml | 7 +-- src/type_check.ml | 27 ++++------ 16 files changed, 72 insertions(+), 169 deletions(-) (limited to 'src') diff --git a/src/ast.ml b/src/ast.ml index 930af68f..bf9b11aa 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -374,8 +374,7 @@ and 'a pexp = Pat_aux of 'a pexp_aux * 'a annot and 'a letbind_aux = (* Let binding *) - LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *) - | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *) + LB_val of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *) and 'a letbind = LB_aux of 'a letbind_aux * 'a annot diff --git a/src/ast_util.ml b/src/ast_util.ml index a39e570b..c57f2a12 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -85,7 +85,7 @@ let mk_fundef funcls = DEF_fundef (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), no_annot)) -let mk_letbind pat exp = LB_aux (LB_val_implicit (pat, exp), no_annot) +let mk_letbind pat exp = LB_aux (LB_val (pat, exp), no_annot) let mk_val_spec vs_aux = DEF_spec (VS_aux (vs_aux, no_annot)) @@ -280,8 +280,7 @@ and map_pat_annot_aux f = function and map_fpat_annot f (FP_aux (FP_Fpat (id, pat), annot)) = FP_aux (FP_Fpat (id, map_pat_annot f pat), f annot) and map_letbind_annot f (LB_aux (lb, annot)) = LB_aux (map_letbind_annot_aux f lb, f annot) and map_letbind_annot_aux f = function - | LB_val_explicit (typschm, pat, exp) -> LB_val_explicit (typschm, map_pat_annot f pat, map_exp_annot f exp) - | LB_val_implicit (pat, exp) -> LB_val_implicit (map_pat_annot f pat, map_exp_annot f exp) + | LB_val (pat, exp) -> LB_val (map_pat_annot f pat, map_exp_annot f exp) and map_lexp_annot f (LEXP_aux (lexp, annot)) = LEXP_aux (map_lexp_annot_aux f lexp, f annot) and map_lexp_annot_aux f = function | LEXP_id id -> LEXP_id id @@ -526,9 +525,7 @@ and string_of_lexp (LEXP_aux (lexp, _)) = | _ -> "LEXP" and string_of_letbind (LB_aux (lb, l)) = match lb with - | LB_val_implicit (pat, exp) -> string_of_pat pat ^ " = " ^ string_of_exp exp - | LB_val_explicit (typschm, pat, exp) -> - string_of_typschm typschm ^ " " ^ string_of_pat pat ^ " = " ^ string_of_exp exp + | LB_val (pat, exp) -> string_of_pat pat ^ " = " ^ string_of_exp exp let rec string_of_index_range (BF_aux (ir, _)) = match ir with diff --git a/src/initial_check.ml b/src/initial_check.ml index 7b618867..89da69e0 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -439,11 +439,8 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa let rec to_ast_letbind (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.LB_aux(lb,l) : Parse_ast.letbind) : unit letbind = LB_aux( (match lb with - | Parse_ast.LB_val_explicit(typschm,pat,exp) -> - let typsch, k_env, _ = to_ast_typschm k_env def_ord typschm in - LB_val_explicit(typsch,to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp) - | Parse_ast.LB_val_implicit(pat,exp) -> - LB_val_implicit(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp) + | Parse_ast.LB_val(pat,exp) -> + LB_val(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp) ), (l,())) and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit exp = diff --git a/src/monomorphise.ml b/src/monomorphise.ml index e97632ec..e419370e 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -363,9 +363,7 @@ let nexp_subst_fns substs refinements = Pat_aux (Pat_when ((*s_pat*) p, s_exp e1, s_exp e2),(l,(*s_tannot*) annot)) and s_letbind (LB_aux (lb,(l,annot))) = match lb with - | LB_val_explicit (tysch,p,e) -> - LB_aux (LB_val_explicit ((*s_typschm*) tysch,(*s_pat*) p,s_exp e), (l,(*s_tannot*) annot)) - | LB_val_implicit (p,e) -> LB_aux (LB_val_implicit ((*s_pat*) p,s_exp e), (l,(*s_tannot*) annot)) + | LB_val (p,e) -> LB_aux (LB_val ((*s_pat*) p,s_exp e), (l,(*s_tannot*) annot)) and s_lexp (LEXP_aux (e,(l,annot))) = let re e = LEXP_aux (e,(l,(*s_tannot*) annot)) in match e with @@ -460,8 +458,7 @@ and deexist_pexp (Pat_aux (pe,(l,annot))) = | Pat_when (p,e1,e2) -> Pat_aux (Pat_when ((*Type_check.strip_pat*) p,deexist_exp e1,deexist_exp e2),(l,annot)) and deexist_letbind (LB_aux (lb,(l,annot))) = match lb with (* TODO, drop tysc if there's an exist? Do they even appear here? *) - | LB_val_explicit (tysc,p,e) -> LB_aux (LB_val_explicit (tysc,(*Type_check.strip_pat*) p,deexist_exp e),(l,annot)) - | LB_val_implicit (p,e) -> LB_aux (LB_val_implicit ((*Type_check.strip_pat*) p,deexist_exp e),(l,annot)) + | LB_val (p,e) -> LB_aux (LB_val ((*Type_check.strip_pat*) p,deexist_exp e),(l,annot)) and deexist_lexp (LEXP_aux (le,(l,annot))) = let re le = LEXP_aux (le,(l,annot)) in match le with @@ -759,11 +756,8 @@ let split_defs splits defs = Pat_aux (Pat_when (p, const_prop_exp substs' e1, const_prop_exp substs' e2),l) and const_prop_letbind substs (LB_aux (lb,annot)) = match lb with - | LB_val_explicit (tysch,p,e) -> - (LB_aux (LB_val_explicit (tysch,p,const_prop_exp substs e), annot), - remove_bound substs p) - | LB_val_implicit (p,e) -> - (LB_aux (LB_val_implicit (p,const_prop_exp substs e), annot), + | LB_val (p,e) -> + (LB_aux (LB_val (p,const_prop_exp substs e), annot), remove_bound substs p) and const_prop_lexp substs ((LEXP_aux (e,annot)) as le) = let re e = LEXP_aux (e,annot) in @@ -817,7 +811,7 @@ let split_defs splits defs = let lg = Generated l in let id = match subi with Id_aux (i,l) -> Id_aux (i,lg) in let p = P_aux (P_id id, subannot) in - E_aux (E_let (LB_aux (LB_val_implicit (p,sube),(lg,annot)), exp),(lg,annot)) + E_aux (E_let (LB_aux (LB_val (p,sube),(lg,annot)), exp),(lg,annot)) else let substs = isubst_from_list [subst] in let () = nexp_substs := [] in @@ -1090,8 +1084,7 @@ let split_defs splits defs = ) patnsubsts) and map_letbind (LB_aux (lb,annot)) = match lb with - | LB_val_explicit (tysch,p,e) -> LB_aux (LB_val_explicit (tysch,check_single_pat p,map_exp e), annot) - | LB_val_implicit (p,e) -> LB_aux (LB_val_implicit (check_single_pat p,map_exp e), annot) + | LB_val (p,e) -> LB_aux (LB_val (check_single_pat p,map_exp e), annot) and map_lexp ((LEXP_aux (e,annot)) as le) = let re e = LEXP_aux (e,annot) in match e with diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 2509f8ef..301d53fb 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -141,7 +141,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = | _ -> string ("EXP(" ^ string_of_exp exp ^ ")") and ocaml_letbind ctx (LB_aux (lb_aux, _)) = match lb_aux with - | LB_val_implicit (pat, exp) -> separate space [ocaml_pat ctx pat; equals; ocaml_atomic_exp ctx exp] + | LB_val (pat, exp) -> separate space [ocaml_pat ctx pat; equals; ocaml_atomic_exp ctx exp] | _ -> failwith "Ocaml: Explicit letbind found" and ocaml_pexps ctx = function | [pexp] -> ocaml_pexp ctx pexp diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 1036fab8..cd5edce6 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -318,8 +318,7 @@ and pexp = Pat_aux of pexp_aux * l and letbind_aux = (* Let binding *) - LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *) - | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) + LB_val of pat * exp (* value binding, implicit type (pat must be total) *) and letbind = LB_aux of letbind_aux * l diff --git a/src/parser.mly b/src/parser.mly index c756cf74..70a6d132 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -999,12 +999,7 @@ patsexp: letbind: | Let_ atomic_pat Eq exp - { lbloc (LB_val_implicit($2,$4)) } - | Let_ typquant atomic_typ atomic_pat Eq exp - { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,$6)) } -/* This introduces one shift reduce conflict, that basically points out that an atomic_pat with a type declared is the Same as this - | Let_ Lparen typ Rparen atomic_pat Eq exp - { assert false (* lbloc (LB_val_explicit((mk_typschm (mk_typqn ()) $2 2 2),$3,$5)) *)} */ + { lbloc (LB_val($2,$4)) } funcl: | id atomic_pat Eq exp diff --git a/src/parser2.mly b/src/parser2.mly index 02a8f09c..7ee98f41 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -836,7 +836,7 @@ block: %inline letbind: | pat Eq exp - { LB_aux (LB_val_implicit ($1, $3), loc $startpos $endpos) } + { LB_aux (LB_val ($1, $3), loc $startpos $endpos) } atomic_exp: | atomic_exp Colon atomic_typ diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index a247b973..7f04c495 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -948,8 +948,7 @@ let doc_exp_lem, doc_let_lem = raise (Reporting_basic.err_unreachable l "unsupported internal expression encountered while pretty-printing") and let_exp sequential mwords early_ret (LB_aux(lb,_)) = match lb with - | LB_val_explicit(_,pat,e) - | LB_val_implicit(pat,e) -> + | LB_val(pat,e) -> prefix 2 1 (separate space [string "let"; doc_pat_lem sequential mwords true pat; equals]) (top_exp sequential mwords early_ret false e) diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 48ec37b8..f0f25795 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -349,10 +349,8 @@ let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p) let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) = let print_lb ppf lb = match lb with - | LB_val_explicit(ts,pat,exp) -> - fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp - | LB_val_implicit(pat,exp) -> - fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat pp_lem_exp exp in + | LB_val(pat,exp) -> + fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val" pp_lem_pat pat pp_lem_exp exp in fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot and pp_lem_exp ppf (E_aux(e,(l,annot))) = diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml index d94879ee..0b7ca48f 100644 --- a/src/pretty_print_ocaml.ml +++ b/src/pretty_print_ocaml.ml @@ -439,11 +439,7 @@ let doc_exp_ocaml, doc_let_ocaml = "internal expression should have been rewritten before pretty-printing") | E_comment _ | E_comment_struc _ -> empty (* TODO Should we output comments? *) and let_exp (LB_aux(lb,_)) = match lb with - | LB_val_explicit(ts,pat,e) -> - prefix 2 1 - (separate space [string "let"; doc_pat_ocaml pat; equals]) - (top_exp false e) - | LB_val_implicit(pat,e) -> + | LB_val(pat,e) -> prefix 2 1 (separate space [string "let"; doc_pat_ocaml pat; equals]) (top_exp false e) diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 8101d45f..546f229f 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -341,17 +341,7 @@ let doc_exp, doc_let = separate space [string "internal let"; doc_lexp lexp; equals; exp exp1; string "in"; exp exp2] | _ -> failwith ("Cannot print: " ^ Ast_util.string_of_exp expr) and let_exp (LB_aux(lb,_)) = match lb with - | LB_val_explicit(ts,pat,e) -> - (match ts with - | TypSchm_aux (TypSchm_ts (TypQ_aux (TypQ_no_forall,_),_),_) -> - prefix 2 1 - (separate space [string "let"; parens (doc_typscm_atomic ts); doc_atomic_pat pat; equals]) - (atomic_exp e) - | _ -> - prefix 2 1 - (separate space [string "let"; doc_typscm_atomic ts; doc_atomic_pat pat; equals]) - (atomic_exp e)) - | LB_val_implicit(pat,e) -> + | LB_val(pat,e) -> prefix 2 1 (separate space [string "let"; doc_atomic_pat pat; equals]) (atomic_exp e) diff --git a/src/rewriter.ml b/src/rewriter.ml index ad4b88c4..2f743e45 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -212,8 +212,7 @@ let fix_eff_pexp (Pat_aux (pexp,((l,_) as annot))) = match snd annot with let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match snd annot with | Some (env, typ, eff) -> let effsum = match lb with - | LB_val_explicit (_,_,e) -> effect_of e - | LB_val_implicit (_,e) -> effect_of e in + | LB_val (_,e) -> effect_of e in LB_aux (lb, (l, Some (env, typ, effsum))) | None -> LB_aux (lb, (l, None)) @@ -533,11 +532,8 @@ let rewrite_let rewriters (LB_aux(letbind,(l,annot))) = | None -> Some(m,s) (*Shouldn't happen*) | Some new_m -> Some(new_m,s) in*) match letbind with - | LB_val_explicit (typschm, pat,exp) -> - LB_aux(LB_val_explicit (typschm,rewriters.rewrite_pat rewriters pat, - rewriters.rewrite_exp rewriters exp),(l,annot)) - | LB_val_implicit ( pat, exp) -> - LB_aux(LB_val_implicit (rewriters.rewrite_pat rewriters pat, + | LB_val ( pat, exp) -> + LB_aux(LB_val (rewriters.rewrite_pat rewriters pat, rewriters.rewrite_exp rewriters exp),(l,annot)) let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) = @@ -732,8 +728,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; pat_exp : 'pat * 'exp -> 'pexp_aux ; pat_when : 'pat * 'exp * 'exp -> 'pexp_aux ; pat_aux : 'pexp_aux * 'a annot -> 'pexp - ; lB_val_explicit : typschm * 'pat * 'exp -> 'letbind_aux - ; lB_val_implicit : 'pat * 'exp -> 'letbind_aux + ; lB_val : 'pat * 'exp -> 'letbind_aux ; lB_aux : 'letbind_aux * 'a annot -> 'letbind ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg } @@ -810,8 +805,7 @@ and fold_pexp_aux alg = function | Pat_when (pat,e,e') -> alg.pat_when (fold_pat alg.pat_alg pat, fold_exp alg e, fold_exp alg e') and fold_pexp alg (Pat_aux (pexp_aux,annot)) = alg.pat_aux (fold_pexp_aux alg pexp_aux, annot) and fold_letbind_aux alg = function - | LB_val_explicit (t,pat,e) -> alg.lB_val_explicit (t,fold_pat alg.pat_alg pat, fold_exp alg e) - | LB_val_implicit (pat,e) -> alg.lB_val_implicit (fold_pat alg.pat_alg pat, fold_exp alg e) + | LB_val (pat,e) -> alg.lB_val (fold_pat alg.pat_alg pat, fold_exp alg e) and fold_letbind alg (LB_aux (letbind_aux,annot)) = alg.lB_aux (fold_letbind_aux alg letbind_aux, annot) let id_exp_alg = @@ -871,8 +865,7 @@ let id_exp_alg = ; pat_exp = (fun (pat,e) -> (Pat_exp (pat,e))) ; pat_when = (fun (pat,e,e') -> (Pat_when (pat,e,e'))) ; pat_aux = (fun (pexp,a) -> (Pat_aux (pexp,a))) - ; lB_val_explicit = (fun (typ,pat,e) -> LB_val_explicit (typ,pat,e)) - ; lB_val_implicit = (fun (pat,e) -> LB_val_implicit (pat,e)) + ; lB_val = (fun (pat,e) -> LB_val (pat,e)) ; lB_aux = (fun (lb,annot) -> LB_aux (lb,annot)) ; pat_alg = id_pat_alg } @@ -972,8 +965,7 @@ let compute_exp_alg bot join = ; pat_exp = (fun ((vp,pat),(v,e)) -> (join vp v, Pat_exp (pat,e))) ; pat_when = (fun ((vp,pat),(v,e),(v',e')) -> (join_list [vp;v;v'], Pat_when (pat,e,e'))) ; pat_aux = (fun ((v,pexp),a) -> (v, Pat_aux (pexp,a))) - ; lB_val_explicit = (fun (typ,(vp,pat),(v,e)) -> (join vp v, LB_val_explicit (typ,pat,e))) - ; lB_val_implicit = (fun ((vp,pat),(v,e)) -> (join vp v, LB_val_implicit (pat,e))) + ; lB_val = (fun ((vp,pat),(v,e)) -> (join vp v, LB_val (pat,e))) ; lB_aux = (fun ((vl,lb),annot) -> (vl,LB_aux (lb,annot))) ; pat_alg = compute_pat_alg bot join } @@ -1199,8 +1191,7 @@ let rewrite_sizeof (Defs defs) = ; pat_exp = (fun (pat,(e,e')) -> (Pat_exp (pat,e), Pat_exp (pat,e'))) ; pat_when = (fun (pat,(e1,e1'),(e2,e2')) -> (Pat_when (pat,e1,e2), Pat_when (pat,e1',e2'))) ; pat_aux = (fun ((pexp,pexp'),a) -> (Pat_aux (pexp,a), Pat_aux (pexp',a))) - ; lB_val_explicit = (fun (typ,pat,(e,e')) -> (LB_val_explicit (typ,pat,e), LB_val_explicit (typ,pat,e'))) - ; lB_val_implicit = (fun (pat,(e,e')) -> (LB_val_implicit (pat,e), LB_val_implicit (pat,e'))) + ; lB_val = (fun (pat,(e,e')) -> (LB_val (pat,e), LB_val (pat,e'))) ; lB_aux = (fun ((lb,lb'),annot) -> (LB_aux (lb,annot), LB_aux (lb',annot))) ; pat_alg = id_pat_alg } in @@ -1272,12 +1263,9 @@ let rewrite_sizeof (Defs defs) = | DEF_val (LB_aux (lb, annot)) -> begin let lb' = match lb with - | LB_val_explicit (typschm, pat, exp) -> - let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in - LB_val_explicit (typschm, pat, exp') - | LB_val_implicit (pat, exp) -> + | LB_val (pat, exp) -> let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in - LB_val_implicit (pat, exp') in + LB_val (pat, exp') in (params_map, defs @ [DEF_val (LB_aux (lb', annot))]) end | def -> @@ -1425,7 +1413,7 @@ let remove_vector_concat_pat pat = match typ_opt with | Some typ -> P_aux (P_typ (typ, P_aux (P_id child,cannot)), cannot) | None -> P_aux (P_id child,cannot) in - let letbind = fix_eff_lb (LB_aux (LB_val_implicit (id_pat,subv),cannot)) in + let letbind = fix_eff_lb (LB_aux (LB_val (id_pat,subv),cannot)) in (letbind, (fun body -> fix_eff_exp (E_aux (E_let (letbind,body), simple_annot l (typ_of body)))), (rootname,childname)) in @@ -1608,13 +1596,9 @@ let rewrite_exp_remove_vector_concat_pat rewriters (E_aux (exp,(l,annot)) as ful let (pat,_,decls) = remove_vector_concat_pat pat in Pat_aux (Pat_when (pat, decls (rewrite_rec guard), decls (rewrite_rec body)),annot') in rewrap (E_case (rewrite_rec e, List.map aux ps)) - | E_let (LB_aux (LB_val_explicit (typ,pat,v),annot'),body) -> + | E_let (LB_aux (LB_val (pat,v),annot'),body) -> let (pat,_,decls) = remove_vector_concat_pat pat in - rewrap (E_let (LB_aux (LB_val_explicit (typ,pat,rewrite_rec v),annot'), - decls (rewrite_rec body))) - | E_let (LB_aux (LB_val_implicit (pat,v),annot'),body) -> - let (pat,_,decls) = remove_vector_concat_pat pat in - rewrap (E_let (LB_aux (LB_val_implicit (pat,rewrite_rec v),annot'), + rewrap (E_let (LB_aux (LB_val (pat,rewrite_rec v),annot'), decls (rewrite_rec body))) | exp -> rewrite_base full_exp @@ -1638,14 +1622,10 @@ let rewrite_defs_remove_vector_concat (Defs defs) = let rewrite_def d = let d = rewriters.rewrite_def rewriters d in match d with - | DEF_val (LB_aux (LB_val_explicit (t,pat,exp),a)) -> + | DEF_val (LB_aux (LB_val (pat,exp),a)) -> let (pat,letbinds,_) = remove_vector_concat_pat pat in let defvals = List.map (fun lb -> DEF_val lb) letbinds in - [DEF_val (LB_aux (LB_val_explicit (t,pat,exp),a))] @ defvals - | DEF_val (LB_aux (LB_val_implicit (pat,exp),a)) -> - let (pat,letbinds,_) = remove_vector_concat_pat pat in - let defvals = List.map (fun lb -> DEF_val lb) letbinds in - [DEF_val (LB_aux (LB_val_implicit (pat,exp),a))] @ defvals + [DEF_val (LB_aux (LB_val (pat,exp),a))] @ defvals | d -> [d] in Defs (List.flatten (List.map rewrite_def defs)) @@ -1918,7 +1898,7 @@ let remove_bitvector_pat pat = let rannot = simple_annot l typ in let elem = access_bit_exp (rootid,rannot) l idx in let e = P_aux (P_id id, simple_annot l bit_typ) in - let letbind = LB_aux (LB_val_implicit (e,elem), simple_annot l bit_typ) in + let letbind = LB_aux (LB_val (e,elem), simple_annot l bit_typ) in let letexp = (fun body -> let (E_aux (_,(_,bannot))) = body in E_aux (E_let (letbind,body), (Parse_ast.Generated l, bannot))) in @@ -2049,13 +2029,9 @@ let rewrite_exp_remove_bitvector_pat rewriters (E_aux (exp,(l,annot)) as full_ex | Some guard' -> Pat_aux (Pat_when (pat', bitwise_and_exp guard guard', body'), annot') | None -> Pat_aux (Pat_when (pat', guard, body'), annot')) in rewrap (E_case (e, List.map rewrite_pexp ps)) - | E_let (LB_aux (LB_val_explicit (typ,pat,v),annot'),body) -> - let (pat,(_,decls,_)) = remove_bitvector_pat pat in - rewrap (E_let (LB_aux (LB_val_explicit (typ,pat,rewrite_rec v),annot'), - decls (rewrite_rec body))) - | E_let (LB_aux (LB_val_implicit (pat,v),annot'),body) -> + | E_let (LB_aux (LB_val (pat,v),annot'),body) -> let (pat,(_,decls,_)) = remove_bitvector_pat pat in - rewrap (E_let (LB_aux (LB_val_implicit (pat,rewrite_rec v),annot'), + rewrap (E_let (LB_aux (LB_val (pat,rewrite_rec v),annot'), decls (rewrite_rec body))) | _ -> rewrite_base full_exp @@ -2086,14 +2062,10 @@ let rewrite_defs_remove_bitvector_pats (Defs defs) = let rewrite_def d = let d = rewriters.rewrite_def rewriters d in match d with - | DEF_val (LB_aux (LB_val_explicit (t,pat,exp),a)) -> + | DEF_val (LB_aux (LB_val (pat,exp),a)) -> let (pat',(_,_,letbinds)) = remove_bitvector_pat pat in let defvals = List.map (fun lb -> DEF_val lb) letbinds in - [DEF_val (LB_aux (LB_val_explicit (t,pat',exp),a))] @ defvals - | DEF_val (LB_aux (LB_val_implicit (pat,exp),a)) -> - let (pat',(_,_,letbinds)) = remove_bitvector_pat pat in - let defvals = List.map (fun lb -> DEF_val lb) letbinds in - [DEF_val (LB_aux (LB_val_implicit (pat',exp),a))] @ defvals + [DEF_val (LB_aux (LB_val (pat',exp),a))] @ defvals | d -> [d] in (* FIXME See above in rewrite_sizeof *) (* fst (check initial_env ( *) @@ -2124,7 +2096,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) = 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 exp_e' = pat_to_exp pat_e' in - let letbind_e = LB_aux (LB_val_implicit (pat_e',e), (el,eannot)) 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 rewrap (E_let (letbind_e, exp')) else case_exp e (typ_of full_exp) clauses @@ -2599,7 +2571,7 @@ let rewrite_defs_remove_blocks = let annot_pat = (simple_annot l (typ_of v)) in let annot_lb = (Parse_ast.Generated l, tannot) in let annot_let = (Parse_ast.Generated l, Some (env_of body, typ_of body, union_eff_exps [v;body])) in - E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in + E_aux (E_let (LB_aux (LB_val (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in let rec f l = function | [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)), (simple_annot l unit_typ)) @@ -2636,7 +2608,7 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp = let annot_let = (Parse_ast.Generated l, Some (env, typ_of body, union_eff_exps [v;body])) in let pat = P_aux (P_wild,annot_pat) in - E_aux (E_let (LB_aux (LB_val_implicit (pat,v),annot_lb),body),annot_let) + E_aux (E_let (LB_aux (LB_val (pat,v),annot_lb),body),annot_let) | Some (env, typ, eff) -> let id = fresh_id "w__" l in let annot_pat = simple_annot l (typ_of v) in @@ -2647,7 +2619,7 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp = let annot_let = (Parse_ast.Generated l, Some (env, typ_of body, union_eff_exps [v;body])) in let pat = P_aux (P_id id,annot_pat) in - E_aux (E_let (LB_aux (LB_val_implicit (pat,v),annot_lb),body),annot_let) + E_aux (E_let (LB_aux (LB_val (pat,v),annot_lb),body),annot_let) | None -> raise (Reporting_basic.err_unreachable l "no type information") @@ -2711,12 +2683,9 @@ let rewrite_defs_letbind_effects = and n_lb (lb : 'a letbind) (k : 'a letbind -> 'a exp) : 'a exp = let (LB_aux (lb,annot)) = lb in match lb with - | LB_val_explicit (typ,pat,exp1) -> - n_exp exp1 (fun exp1 -> - k (fix_eff_lb (LB_aux (LB_val_explicit (typ,pat,exp1),annot)))) - | LB_val_implicit (pat,exp1) -> + | LB_val (pat,exp1) -> n_exp exp1 (fun exp1 -> - k (fix_eff_lb (LB_aux (LB_val_implicit (pat,exp1),annot)))) + k (fix_eff_lb (LB_aux (LB_val (pat,exp1),annot)))) and n_lexp (lexp : 'a lexp) (k : 'a lexp -> 'a exp) : 'a exp = let (LEXP_aux (lexp_aux,annot)) = lexp in @@ -2901,10 +2870,8 @@ let rewrite_defs_letbind_effects = let rewrap lb = DEF_val (LB_aux (lb, annot)) in begin match lb with - | LB_val_implicit (pat, exp) -> - rewrap (LB_val_implicit (pat, n_exp_term (effectful exp) exp)) - | LB_val_explicit (ts, pat, exp) -> - rewrap (LB_val_explicit (ts, pat, n_exp_term (effectful exp) exp)) + | LB_val (pat, exp) -> + rewrap (LB_val (pat, n_exp_term (effectful exp) exp)) end | DEF_fundef fdef -> DEF_fundef (rewrite_fun rewriters fdef) | d -> d in @@ -2928,13 +2895,12 @@ let rewrite_defs_effectful_let_expressions = let e_let (lb,body) = match lb with - | LB_aux (LB_val_implicit (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _) + | LB_aux (LB_val (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _) when lexp_is_local le (env_of_annot annot) && not (lexp_is_effectful le) -> (* Rewrite assignments to local variables into let bindings *) let (lhs, rhs) = rewrite_local_lexp le in - E_let (LB_aux (LB_val_implicit (pat_of_local_lexp lhs, rhs exp), annot), body) - | LB_aux (LB_val_explicit (_,pat,exp'),annot') - | LB_aux (LB_val_implicit (pat,exp'),annot') -> + E_let (LB_aux (LB_val (pat_of_local_lexp lhs, rhs exp), annot), body) + | LB_aux (LB_val (pat,exp'),annot') -> if effectful exp' then E_internal_plet (pat,exp',body) else E_let (lb,body) in @@ -2946,7 +2912,7 @@ let rewrite_defs_effectful_let_expressions = if effectful exp1 then E_internal_plet (P_aux (P_id id,annot),exp1,exp2) else - let lb = LB_aux (LB_val_implicit (P_aux (P_id id,annot), exp1), annot) in + let lb = LB_aux (LB_val (P_aux (P_id id,annot), exp1), annot) in E_let (lb, exp2) | _ -> failwith "E_internal_let with unexpected lexp" in @@ -3206,20 +3172,13 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | E_let (lb,body) -> let body = rewrite_var_updates body in let (eff,lb) = match lb with - | LB_aux (LB_val_implicit (pat,v),lbannot) -> + | LB_aux (LB_val (pat,v),lbannot) -> (match rewrite v pat with | Added_vars (v,pat) -> let (E_aux (_,(l,_))) = v in let lbannot = (simple_annot l (typ_of v)) in - (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot)) - | Same_vars v -> (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot))) - | LB_aux (LB_val_explicit (typ,pat,v),lbannot) -> - (match rewrite v pat with - | Added_vars (v,pat) -> - let (E_aux (_,(l,_))) = v in - let lbannot = (simple_annot l (typ_of v)) in - (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot)) - | Same_vars v -> (effect_of v,LB_aux (LB_val_explicit (typ,pat,v),lbannot))) in + (effect_of v,LB_aux (LB_val (pat,v),lbannot)) + | Same_vars v -> (effect_of v,LB_aux (LB_val (pat,v),lbannot))) in let tannot = Some (env_of_annot annot, typ_of body, union_effects eff (effect_of body)) in E_aux (E_let (lb,body),(Parse_ast.Generated l,tannot)) | E_internal_let (lexp,v,body) -> @@ -3235,7 +3194,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let bodyeff = effect_of body in let pat = P_aux (P_id id, (simple_annot l vtyp)) in let lbannot = (Parse_ast.Generated l, Some (env, vtyp, veff)) in - let lb = LB_aux (LB_val_implicit (pat,v),lbannot) in + let lb = LB_aux (LB_val (pat,v),lbannot) in let exp = E_aux (E_let (lb,body),(Parse_ast.Generated l, Some (bodyenv, bodytyp, union_effects veff bodyeff))) in rewrite_var_updates exp | E_internal_plet (pat,v,body) -> @@ -3290,21 +3249,15 @@ let rewrite_defs_remove_superfluous_letbinds = | E_let (lb,exp2) -> begin match lb,exp2 with (* 'let x = EXP1 in x' can be replaced with 'EXP1' *) - | LB_aux (LB_val_explicit (_,P_aux (P_id (Id_aux (id,_)),_),exp1),_), - E_aux (E_id (Id_aux (id',_)),_) - | LB_aux (LB_val_explicit (_,P_aux (P_id (Id_aux (id,_)),_),exp1),_), - E_aux (E_cast (_,E_aux (E_id (Id_aux (id',_)),_)),_) - | LB_aux (LB_val_implicit (P_aux (P_id (Id_aux (id,_)),_),exp1),_), + | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_), E_aux (E_id (Id_aux (id',_)),_) - | LB_aux (LB_val_implicit (P_aux (P_id (Id_aux (id,_)),_),exp1),_), + | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_), E_aux (E_cast (_,E_aux (E_id (Id_aux (id',_)),_)),_) when id = id' -> exp1 (* "let x = EXP1 in return x" can be replaced with 'return (EXP1)', at least when EXP1 is 'small' enough *) - | LB_aux (LB_val_explicit (_,P_aux (P_id (Id_aux (id,_)),_),exp1),_), - E_aux (E_internal_return (E_aux (E_id (Id_aux (id',_)),_)),_) - | LB_aux (LB_val_implicit (P_aux (P_id (Id_aux (id,_)),_),exp1),_), + | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_), E_aux (E_internal_return (E_aux (E_id (Id_aux (id',_)),_)),_) when id = id' && small exp1 -> let (E_aux (_,e1annot)) = exp1 in diff --git a/src/rewriter.mli b/src/rewriter.mli index 645ecbf4..32974bd0 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -142,8 +142,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; pat_exp : 'pat * 'exp -> 'pexp_aux ; pat_when : 'pat * 'exp * 'exp -> 'pexp_aux ; pat_aux : 'pexp_aux * 'a annot -> 'pexp - ; lB_val_explicit : typschm * 'pat * 'exp -> 'letbind_aux - ; lB_val_implicit : 'pat * 'exp -> 'letbind_aux + ; lB_val : 'pat * 'exp -> 'letbind_aux ; lB_aux : 'letbind_aux * 'a annot -> 'letbind ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg } diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index e04b7d33..3f3df45a 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -358,12 +358,7 @@ and fv_of_pes consider_var bound used set pes = fv_of_pes consider_var bound us_e set_e pes and fv_of_let consider_var bound used set (LB_aux(lebind,_)) = match lebind with - | LB_val_explicit(typsch,pat,exp) -> - let bound_t,us_t = fv_of_typschm consider_var bound used typsch in - let bound_p, us_p = pat_bindings consider_var (Nameset.union bound bound_t) used pat in - let _,us_e,set_e = fv_of_exp consider_var (Nameset.union bound bound_t) used set exp in - (Nameset.union bound_t bound_p),Nameset.union us_t (Nameset.union us_p us_e),set_e - | LB_val_implicit(pat,exp) -> + | LB_val(pat,exp) -> let bound_p, us_p = pat_bindings consider_var bound used pat in let _,us_e,set_e = fv_of_exp consider_var bound used set exp in bound_p,Nameset.union us_p us_e,set_e diff --git a/src/type_check.ml b/src/type_check.ml index 5813b081..bfd336d9 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1946,15 +1946,14 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | E_let (LB_aux (letbind, (let_loc, _)), exp), _ -> begin match letbind with - | LB_val_explicit (typschm, pat, bind) -> assert false - | LB_val_implicit (P_aux (P_typ (ptyp, _), _) as pat, bind) -> + | LB_val (P_aux (P_typ (ptyp, _), _) as pat, bind) -> let checked_bind = crule check_exp env bind ptyp in let tpat, env = bind_pat env pat ptyp in - annot_exp (E_let (LB_aux (LB_val_implicit (tpat, checked_bind), (let_loc, None)), crule check_exp env exp typ)) typ - | LB_val_implicit (pat, bind) -> + annot_exp (E_let (LB_aux (LB_val (tpat, checked_bind), (let_loc, None)), crule check_exp env exp typ)) typ + | LB_val (pat, bind) -> let inferred_bind = irule infer_exp env bind in let tpat, env = bind_pat env pat (typ_of inferred_bind) in - annot_exp (E_let (LB_aux (LB_val_implicit (tpat, inferred_bind), (let_loc, None)), crule check_exp env exp typ)) typ + annot_exp (E_let (LB_aux (LB_val (tpat, inferred_bind), (let_loc, None)), crule check_exp env exp typ)) typ end | E_app_infix (x, op, y), _ when List.length (Env.get_overloads (deinfix op) env) > 0 -> check_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) typ @@ -2965,15 +2964,10 @@ and propagate_letbind_effect (LB_aux (lb, (l, annot))) = | Some (typq, typ, eff) -> LB_aux (p_lb, (l, Some (typq, typ, eff))), eff | None -> LB_aux (p_lb, (l, None)), eff and propagate_letbind_effect_aux = function - | LB_val_explicit (typschm, pat, exp) -> + | LB_val (pat, exp) -> let p_pat = propagate_pat_effect pat in let p_exp = propagate_exp_effect exp in - LB_val_explicit (typschm, p_pat, p_exp), - union_effects (effect_of_pat p_pat) (effect_of p_exp) - | LB_val_implicit (pat, exp) -> - let p_pat = propagate_pat_effect pat in - let p_exp = propagate_exp_effect exp in - LB_val_implicit (p_pat, p_exp), + LB_val (p_pat, p_exp), union_effects (effect_of_pat p_pat) (effect_of p_exp) and propagate_lexp_effect (LEXP_aux (lexp, annot)) = @@ -3010,15 +3004,14 @@ and propagate_lexp_effect_aux = function let check_letdef env (LB_aux (letbind, (l, _))) = begin match letbind with - | LB_val_explicit (typschm, pat, bind) -> assert false - | LB_val_implicit (P_aux (P_typ (typ_annot, pat), _), bind) -> + | LB_val (P_aux (P_typ (typ_annot, pat), _), bind) -> let checked_bind = crule check_exp env (strip_exp bind) typ_annot in let tpat, env = bind_pat env (strip_pat pat) typ_annot in - [DEF_val (LB_aux (LB_val_implicit (P_aux (P_typ (typ_annot, tpat), (l, Some (env, typ_annot, no_effect))), checked_bind), (l, None)))], env - | LB_val_implicit (pat, bind) -> + [DEF_val (LB_aux (LB_val (P_aux (P_typ (typ_annot, tpat), (l, Some (env, typ_annot, no_effect))), checked_bind), (l, None)))], env + | LB_val (pat, bind) -> let inferred_bind = irule infer_exp env (strip_exp bind) in let tpat, env = bind_pat env (strip_pat pat) (typ_of inferred_bind) in - [DEF_val (LB_aux (LB_val_implicit (tpat, inferred_bind), (l, None)))], env + [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], env end let check_funcl env (FCL_aux (FCL_Funcl (id, pat, exp), (l, _))) typ = -- cgit v1.2.3