diff options
Diffstat (limited to 'src/rewriter.ml')
| -rw-r--r-- | src/rewriter.ml | 1778 |
1 files changed, 1245 insertions, 533 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index d26879e9..166c31f0 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -9,6 +9,7 @@ (* Robert Norton-Wright *) (* Christopher Pulte *) (* Peter Sewell *) +(* Thomas Bauereiss *) (* *) (* All rights reserved. *) (* *) @@ -42,19 +43,15 @@ open Big_int open Ast -open Type_internal +open Ast_util +open Type_check open Spec_analysis -type typ = Type_internal.t -type 'a exp = 'a Ast.exp -type 'a emap = 'a Envmap.t -type envs = Type_check.envs -type 'a namemap = (typ * 'a exp) emap type 'a rewriters = { - rewrite_exp : 'a rewriters -> (nexp_map * 'a namemap) option -> 'a exp -> 'a exp; - rewrite_lexp : 'a rewriters -> (nexp_map * 'a namemap) option -> 'a lexp -> 'a lexp; - rewrite_pat : 'a rewriters -> (nexp_map * 'a namemap) option -> 'a pat -> 'a pat; - rewrite_let : 'a rewriters -> (nexp_map * 'a namemap) option -> 'a letbind -> 'a letbind; + rewrite_exp : 'a rewriters -> 'a exp -> 'a exp; + rewrite_lexp : 'a rewriters -> 'a lexp -> 'a lexp; + rewrite_pat : 'a rewriters -> 'a pat -> 'a pat; + rewrite_let : 'a rewriters -> 'a letbind -> 'a letbind; rewrite_fun : 'a rewriters -> 'a fundef -> 'a fundef; rewrite_def : 'a rewriters -> 'a def -> 'a def; rewrite_defs : 'a rewriters -> 'a defs -> 'a defs; @@ -63,6 +60,23 @@ type 'a rewriters = { let (>>) f g = fun x -> g(f(x)) +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,_),_)) = + 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 +let effect_of_pexp (Pat_aux (_,(_,a))) = effect_of_annot a +let effect_of_lb (LB_aux (_,(_,a))) = effect_of_annot a + +let get_loc_exp (E_aux (_,(l,_))) = l + +let simple_annot l typ = (Parse_ast.Generated l, Some (Env.empty, typ, no_effect)) +let simple_num l n = E_aux ( + E_lit (L_aux (L_num n, Parse_ast.Generated l)), + simple_annot (Parse_ast.Generated l) + (atom_typ (Nexp_aux (Nexp_constant n, Parse_ast.Generated l)))) + let fresh_name_counter = ref 0 let fresh_name () = @@ -72,151 +86,162 @@ let fresh_name () = let reset_fresh_name_counter () = fresh_name_counter := 0 -let get_effsum_annot (_,t) = match t with - | Base (_,_,_,_,effs,_) -> effs - | NoTyp -> failwith "no effect information" - | _ -> failwith "get_effsum_annot doesn't support Overload" - -let get_localeff_annot (_,t) = match t with - | Base (_,_,_,eff,_,_) -> eff - | NoTyp -> failwith "no effect information" - | _ -> failwith "get_localeff_annot doesn't support Overload" - -let get_type_annot (_,t) = match t with - | Base((_,t),_,_,_,_,_) -> t - | NoTyp -> failwith "no type information" - | _ -> failwith "get_type_annot doesn't support Overload" - -let get_type (E_aux (_,a)) = get_type_annot a - -let union_effs effs = - List.fold_left (fun acc eff -> union_effects acc eff) pure_e effs - -let get_effsum_exp (E_aux (_,a)) = get_effsum_annot a -let get_effsum_fpat (FP_aux (_,a)) = get_effsum_annot a -let get_effsum_lexp (LEXP_aux (_,a)) = get_effsum_annot a -let get_effsum_fexp (FE_aux (_,a)) = get_effsum_annot a -let get_effsum_fexps (FES_aux (FES_Fexps (fexps,_),_)) = - union_effs (List.map get_effsum_fexp fexps) -let get_effsum_opt_default (Def_val_aux (_,a)) = get_effsum_annot a -let get_effsum_pexp (Pat_aux (_,a)) = get_effsum_annot a -let get_effsum_lb (LB_aux (_,a)) = get_effsum_annot a - -let eff_union_exps es = - union_effs (List.map get_effsum_exp es) - -let fix_effsum_exp (E_aux (e,(l,annot))) = - let (Base (t,tag,nexps,eff,_,bounds)) = annot in - let effsum = match e with - | E_block es -> eff_union_exps es - | E_nondet es -> eff_union_exps es +let fresh_id pre l = + let current = fresh_name () in + Id_aux (Id (pre ^ string_of_int current), Parse_ast.Generated l) + +let fresh_id_exp pre ((l,annot)) = + let id = fresh_id pre l in + E_aux (E_id id, (Parse_ast.Generated l, annot)) + +let fresh_id_pat pre ((l,annot)) = + let id = fresh_id pre l in + P_aux (P_id id, (Parse_ast.Generated l, annot)) + +let union_eff_exps es = + List.fold_left union_effects no_effect (List.map effect_of es) + +let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with +| Some (env, typ, eff) -> + let effsum = union_effects eff (match e with + | E_block es -> union_eff_exps es + | E_nondet es -> union_eff_exps es | E_id _ - | E_lit _ -> pure_e - | E_cast (_,e) -> get_effsum_exp e + | E_lit _ -> no_effect + | E_cast (_,e) -> effect_of e | E_app (_,es) - | E_tuple es -> eff_union_exps es - | E_app_infix (e1,_,e2) -> eff_union_exps [e1;e2] - | E_if (e1,e2,e3) -> eff_union_exps [e1;e2;e3] - | E_for (_,e1,e2,e3,_,e4) -> eff_union_exps [e1;e2;e3;e4] - | E_vector es -> eff_union_exps es + | E_tuple es -> union_eff_exps es + | E_app_infix (e1,_,e2) -> union_eff_exps [e1;e2] + | E_if (e1,e2,e3) -> union_eff_exps [e1;e2;e3] + | E_for (_,e1,e2,e3,_,e4) -> union_eff_exps [e1;e2;e3;e4] + | E_vector es -> union_eff_exps es | E_vector_indexed (ies,opt_default) -> let (_,es) = List.split ies in - union_effs (get_effsum_opt_default opt_default :: List.map get_effsum_exp es) - | E_vector_access (e1,e2) -> eff_union_exps [e1;e2] - | E_vector_subrange (e1,e2,e3) -> eff_union_exps [e1;e2;e3] - | E_vector_update (e1,e2,e3) -> eff_union_exps [e1;e2;e3] - | E_vector_update_subrange (e1,e2,e3,e4) -> eff_union_exps [e1;e2;e3;e4] - | E_vector_append (e1,e2) -> eff_union_exps [e1;e2] - | E_list es -> eff_union_exps es - | E_cons (e1,e2) -> eff_union_exps [e1;e2] - | E_record fexps -> get_effsum_fexps fexps - | E_record_update(e,fexps) -> union_effs ((get_effsum_exp e)::[(get_effsum_fexps fexps)]) - | E_field (e,_) -> get_effsum_exp e - | E_case (e,pexps) -> union_effs (get_effsum_exp e :: List.map get_effsum_pexp pexps) - | E_let (lb,e) -> union_effs [get_effsum_lb lb;get_effsum_exp e] - | E_assign (lexp,e) -> union_effs [get_effsum_lexp lexp;get_effsum_exp e] - | E_exit e -> get_effsum_exp e - | E_return e -> get_effsum_exp e - | E_sizeof _ | E_sizeof_internal _ -> pure_e - | E_assert (c,m) -> pure_e - | E_comment _ | E_comment_struc _ -> pure_e - | E_internal_cast (_,e) -> get_effsum_exp e - | E_internal_exp _ -> pure_e - | E_internal_exp_user _ -> pure_e - | E_internal_let (lexp,e1,e2) -> union_effs [get_effsum_lexp lexp; - get_effsum_exp e1;get_effsum_exp e2] - | E_internal_plet (_,e1,e2) -> union_effs [get_effsum_exp e1;get_effsum_exp e2] - | E_internal_return e1 -> get_effsum_exp e1 + union_effects (effect_of_opt_default opt_default) (union_eff_exps es) + | E_vector_access (e1,e2) -> union_eff_exps [e1;e2] + | E_vector_subrange (e1,e2,e3) -> union_eff_exps [e1;e2;e3] + | E_vector_update (e1,e2,e3) -> union_eff_exps [e1;e2;e3] + | E_vector_update_subrange (e1,e2,e3,e4) -> union_eff_exps [e1;e2;e3;e4] + | E_vector_append (e1,e2) -> union_eff_exps [e1;e2] + | E_list es -> union_eff_exps es + | E_cons (e1,e2) -> union_eff_exps [e1;e2] + | E_record fexps -> effect_of_fexps fexps + | E_record_update(e,fexps) -> + union_effects (effect_of e) (effect_of_fexps fexps) + | E_field (e,_) -> effect_of e + | E_case (e,pexps) -> + List.fold_left union_effects (effect_of e) (List.map effect_of_pexp pexps) + | E_let (lb,e) -> union_effects (effect_of_lb lb) (effect_of e) + | E_assign (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e) + | E_exit e -> effect_of e + | E_return e -> effect_of e + | E_sizeof _ | E_sizeof_internal _ -> no_effect + | E_assert (c,m) -> no_effect + | E_comment _ | E_comment_struc _ -> no_effect + | E_internal_cast (_,e) -> effect_of e + | E_internal_exp _ -> no_effect + | E_internal_exp_user _ -> no_effect + | E_internal_let (lexp,e1,e2) -> + union_effects (effect_of_lexp lexp) + (union_effects (effect_of e1) (effect_of e2)) + | E_internal_plet (_,e1,e2) -> union_effects (effect_of e1) (effect_of e2) + | E_internal_return e1 -> effect_of e1) in - E_aux (e,(l,(Base (t,tag,nexps,eff,union_effects eff effsum,bounds)))) - -let fix_effsum_lexp (LEXP_aux (lexp,(l,annot))) = - let (Base (t,tag,nexps,eff,_,bounds)) = annot in - let effsum = match lexp with - | LEXP_id _ -> pure_e - | LEXP_cast _ -> pure_e - | LEXP_memory (_,es) -> eff_union_exps es - | LEXP_vector (lexp,e) -> union_effs [get_effsum_lexp lexp;get_effsum_exp e] - | LEXP_vector_range (lexp,e1,e2) -> union_effs [get_effsum_lexp lexp;get_effsum_exp e1; - get_effsum_exp e2] - | LEXP_field (lexp,_) -> get_effsum_lexp lexp in - LEXP_aux (lexp,(l,(Base (t,tag,nexps,eff,union_effects eff effsum,bounds)))) - -let fix_effsum_fexp (FE_aux (fexp,(l,annot))) = - let (Base (t,tag,nexps,eff,_,bounds)) = annot in - let effsum = match fexp with - | FE_Fexp (_,e) -> get_effsum_exp e in - FE_aux (fexp,(l,(Base (t,tag,nexps,eff,union_effects eff effsum,bounds)))) - -let fix_effsum_fexps fexps = fexps (* FES_aux have no effect information *) - -let fix_effsum_opt_default (Def_val_aux (opt_default,(l,annot))) = - let (Base (t,tag,nexps,eff,_,bounds)) = annot in - let effsum = match opt_default with - | Def_val_empty -> pure_e - | Def_val_dec e -> get_effsum_exp e in - Def_val_aux (opt_default,(l,(Base (t,tag,nexps,eff,union_effects eff effsum,bounds)))) - -let fix_effsum_pexp (Pat_aux (pexp,(l,annot))) = - let (Base (t,tag,nexps,eff,_,bounds)) = annot in - let effsum = match pexp with - | Pat_exp (_,e) -> get_effsum_exp e in - Pat_aux (pexp,(l,(Base (t,tag,nexps,eff,union_effects eff effsum,bounds)))) - -let fix_effsum_lb (LB_aux (lb,(l,annot))) = - let (Base (t,tag,nexps,eff,_,bounds)) = annot in - let effsum = match lb with - | LB_val_explicit (_,_,e) -> get_effsum_exp e - | LB_val_implicit (_,e) -> get_effsum_exp e in - LB_aux (lb,(l,(Base (t,tag,nexps,eff,union_effects eff effsum,bounds)))) - -let effectful_effs {effect = Eset effs} = - List.exists - (fun (BE_aux (be,_)) -> - match be with - | BE_nondet | BE_unspec | BE_undef | BE_lset -> false - | _ -> true - ) effs - -let effectful eaux = effectful_effs (get_effsum_exp eaux) - -let updates_vars_effs {effect = Eset effs} = - List.exists - (fun (BE_aux (be,_)) -> - match be with - | BE_lset -> true - | _ -> false - ) effs - -let updates_vars eaux = updates_vars_effs (get_effsum_exp eaux) - - -let rec partial_assoc (eq: 'a -> 'a -> bool) (v: 'a) (ls : ('a *'b) list ) : 'b option = match ls with + E_aux (e, (l, Some (env, typ, effsum))) +| None -> + E_aux (e, (l, None)) + +let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with +| Some (env, typ, eff) -> + let effsum = union_effects eff (match lexp with + | LEXP_id _ -> no_effect + | LEXP_cast _ -> no_effect + | LEXP_memory (_,es) -> union_eff_exps es + | LEXP_vector (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e) + | LEXP_vector_range (lexp,e1,e2) -> + 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))) +| None -> + LEXP_aux (lexp, (l, None)) + +let fix_eff_fexp (FE_aux (fexp,((l,_) as annot))) = match 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))) +| None -> + FE_aux (fexp, (l, None)) + +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 +| 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))) +| None -> + Def_val_aux (opt_default, (l, None)) + +let fix_eff_pexp (Pat_aux (pexp,((l,_) as annot))) = match snd annot with +| Some (env, typ, eff) -> + let effsum = union_effects eff (match pexp with + | Pat_exp (_,e) -> effect_of e) in + Pat_aux (pexp, (l, Some (env, typ, effsum))) +| None -> + Pat_aux (pexp, (l, None)) + +let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match snd annot with +| Some (env, typ, eff) -> + let effsum = union_effects eff (match lb with + | LB_val_explicit (_,_,e) -> effect_of e + | LB_val_implicit (_,e) -> effect_of e) in + LB_aux (lb, (l, Some (env, typ, effsum))) +| None -> + LB_aux (lb, (l, None)) + +let effectful_effs = function + | Effect_aux (Effect_set effs, _) -> + List.exists + (fun (BE_aux (be,_)) -> + match be with + | BE_nondet | BE_unspec | BE_undef | BE_lset -> false + | _ -> true + ) effs + | _ -> true + +let effectful eaux = effectful_effs (effect_of eaux) + +let updates_vars_effs = function + | Effect_aux (Effect_set effs, _) -> + List.exists + (fun (BE_aux (be,_)) -> + match be with + | BE_lset -> true + | _ -> false + ) effs + | _ -> true + +let updates_vars eaux = updates_vars_effs (effect_of eaux) + +let id_to_string (Id_aux(id,l)) = + match id with + | Id(s) -> s + | DeIid(s) -> s + + +(*let rec partial_assoc (eq: 'a -> 'a -> bool) (v: 'a) (ls : ('a *'b) list ) : 'b option = match ls with | [] -> None | (v1,v2)::ls -> if (eq v1 v) then Some v2 else partial_assoc eq v ls let mk_atom_typ i = {t=Tapp("atom",[TA_nexp i])} +let simple_num l n : tannot exp = + let typ = simple_annot (mk_atom_typ (mk_c (big_int_of_int n))) in + E_aux (E_lit (L_aux (L_num n,l)), (l,typ)) + let rec rewrite_nexp_to_exp program_vars l nexp = let rewrite n = rewrite_nexp_to_exp program_vars l n in let typ = mk_atom_typ nexp in @@ -266,7 +291,7 @@ let rec match_to_program_vars ns bounds = | None -> match_to_program_vars ns bounds | Some(augment,ev) -> (*let _ = Printf.eprintf "adding n %s to program var %s\n" (n_to_string n) ev in*) - (n,(augment,ev))::(match_to_program_vars ns bounds) + (n,(augment,ev))::(match_to_program_vars ns bounds)*) let explode s = let rec exp i l = if i < 0 then l else exp (i - 1) (s.[i] :: l) in @@ -303,17 +328,17 @@ let vector_string_to_bit_list l lit = | '1' -> L_aux (L_one,Parse_ast.Generated l) | _ -> raise (Reporting_basic.err_unreachable (Parse_ast.Generated l) "binary had non-zero or one")) s_bin -let rewrite_pat rewriters nmap (P_aux (pat,(l,annot))) = +let rewrite_pat rewriters (P_aux (pat,(l,annot))) = let rewrap p = P_aux (p,(l,annot)) in - let rewrite = rewriters.rewrite_pat rewriters nmap in + 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,(Parse_ast.Generated l,simple_annot {t = Tid "bit"}))) + let ps = List.map (fun p -> P_aux (P_lit p, simple_annot l bit_typ)) (vector_string_to_bit_list l lit) in rewrap (P_vector ps) | P_lit _ | P_wild | P_id _ -> rewrap pat - | P_as(pat,id) -> rewrap (P_as( rewrite pat, id)) - | P_typ(typ,pat) -> rewrite pat + | P_as(pat,id) -> rewrap (P_as(rewrite pat, id)) + | P_typ(typ,pat) -> rewrap (P_typ(typ, rewrite pat)) | P_app(id ,pats) -> rewrap (P_app(id, List.map rewrite pats)) | P_record(fpats,_) -> rewrap (P_record(List.map (fun (FP_aux(FP_Fpat(id,pat),pannot)) -> FP_aux(FP_Fpat(id, rewrite pat), pannot)) fpats, @@ -323,16 +348,17 @@ let rewrite_pat rewriters nmap (P_aux (pat,(l,annot))) = | P_vector_concat pats -> rewrap (P_vector_concat (List.map rewrite pats)) | P_tup pats -> rewrap (P_tup (List.map rewrite pats)) | P_list pats -> rewrap (P_list (List.map rewrite pats)) + | P_cons (pat1, pat2) -> rewrap (P_cons (rewrite pat1, rewrite pat2)) -let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = +let rewrite_exp rewriters (E_aux (exp,(l,annot))) = let rewrap e = E_aux (e,(l,annot)) in - let rewrite = rewriters.rewrite_exp rewriters nmap in + let rewrite = rewriters.rewrite_exp rewriters in match exp with | E_comment _ | E_comment_struc _ -> rewrap 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 ,(Parse_ast.Generated l,simple_annot {t = Tid "bit"}))) + let es = List.map (fun p -> E_aux (E_lit p, simple_annot l bit_typ)) (vector_string_to_bit_list l lit) in rewrap (E_vector es) | E_id _ | E_lit _ -> rewrap exp @@ -374,15 +400,17 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = rewrap (E_case (rewrite exp, (List.map (fun (Pat_aux (Pat_exp(p,e),pannot)) -> - Pat_aux (Pat_exp(rewriters.rewrite_pat rewriters nmap p,rewrite e),pannot)) pexps))) - | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite body)) - | E_assign (lexp,exp) -> rewrap (E_assign(rewriters.rewrite_lexp rewriters nmap lexp,rewrite exp)) + Pat_aux (Pat_exp(rewriters.rewrite_pat rewriters p,rewrite e),pannot)) pexps))) + | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters letbind,rewrite body)) + | E_assign (lexp,exp) -> rewrap (E_assign(rewriters.rewrite_lexp rewriters lexp,rewrite exp)) | E_sizeof n -> rewrap (E_sizeof n) | E_exit e -> rewrap (E_exit (rewrite e)) | E_return e -> rewrap (E_return (rewrite e)) | E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2)) - | E_internal_cast ((l,casted_annot),exp) -> - let new_exp = rewrite exp in + | E_internal_cast (casted_annot,exp) -> + rewrap (E_internal_cast (casted_annot, rewrite exp)) + (* check_exp (env_of exp) (strip_exp exp) (typ_of_annot casted_annot) *) + (*let new_exp = rewrite exp in (*let _ = Printf.eprintf "Removing an internal_cast with %s\n" (tannot_to_string casted_annot) in*) (match casted_annot,exp with | Base((_,t),_,_,_,_,_),E_aux(ec,(ecl,Base((_,exp_t),_,_,_,_,_))) -> @@ -403,7 +431,7 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"),Parse_ast.Generated l)), Parse_ast.Generated l),new_exp)) | _ -> new_exp)) - | _ -> new_exp) + | _ -> new_exp | Base((_,t),_,_,_,_,_),_ -> (*let _ = Printf.eprintf "Considering removing an internal cast where the remaining type is %s\n%!" (t_to_string t) in*) @@ -417,9 +445,9 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = Parse_ast.Generated l), new_exp)) | _ -> new_exp) | _ -> new_exp) - | _ -> (*let _ = Printf.eprintf "Not a base match?\n" in*) new_exp) - | E_internal_exp (l,impl) -> - (match impl with + | _ -> (*let _ = Printf.eprintf "Not a base match?\n" in*) new_exp*) + (*| E_internal_exp (l,impl) -> + match impl with | Base((_,t),_,_,_,_,bounds) -> (*let _ = Printf.eprintf "Rewriting internal expression, with type %s, and bounds %s\n" (t_to_string t) (bounds_to_string bounds) in*) @@ -445,8 +473,8 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given unexpected types " ^ (t_to_string t)))) - | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given none Base annot"))) - | E_sizeof_internal (l,impl) -> + | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given none Base annot"))*) + (*| E_sizeof_internal (l,impl) -> (match impl with | Base((_,t),_,_,_,_,bounds) -> let bounds = match nmap with | None -> bounds | Some (nm,_) -> add_map_to_bounds nm bounds in @@ -458,8 +486,8 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = | [] -> rewrite_nexp_to_exp None l n | map -> rewrite_nexp_to_exp (Some map) l n) | _ -> raise (Reporting_basic.err_unreachable l ("Sizeof internal had non-atom type " ^ (t_to_string t)))) - | _ -> raise (Reporting_basic.err_unreachable l ("Sizeof internal had none base annot"))) - | E_internal_exp_user ((l,user_spec),(_,impl)) -> + | _ -> raise (Reporting_basic.err_unreachable l ("Sizeof internal had none base annot"))*) + (*| E_internal_exp_user ((l,user_spec),(_,impl)) -> (match (user_spec,impl) with | (Base((_,tu),_,_,_,_,_), Base((_,ti),_,_,_,_,bounds)) -> (*let _ = Printf.eprintf "E_interal_user getting rewritten two types are %s and %s\n" @@ -476,13 +504,14 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given unexpected types " ^ (t_to_string tu) ^ ", " ^ (t_to_string ti)))) - | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot"))) + | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot")))*) | E_internal_let _ -> raise (Reporting_basic.err_unreachable l "Internal let found before it should have been introduced") | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced") | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l " Internal plet found before it should have been introduced") + | _ -> rewrap exp -let rewrite_let rewriters map (LB_aux(letbind,(l,annot))) = - let local_map = get_map_tannot annot in +let rewrite_let rewriters (LB_aux(letbind,(l,annot))) = + (*let local_map = get_map_tannot annot in let map = match map,local_map with | None,None -> None @@ -490,47 +519,47 @@ let rewrite_let rewriters map (LB_aux(letbind,(l,annot))) = | Some(m,s), None -> Some(m,s) | Some(m,s), Some m' -> match merge_option_maps (Some m) local_map with | None -> Some(m,s) (*Shouldn't happen*) - | Some new_m -> Some(new_m,s) in + | 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 map pat, - rewriters.rewrite_exp rewriters map exp),(l,annot)) + 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 map pat, - rewriters.rewrite_exp rewriters map exp),(l,annot)) + LB_aux(LB_val_implicit (rewriters.rewrite_pat rewriters pat, + rewriters.rewrite_exp rewriters exp),(l,annot)) -let rewrite_lexp rewriters map (LEXP_aux(lexp,(l,annot))) = +let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) = let rewrap le = LEXP_aux(le,(l,annot)) in match lexp with | LEXP_id _ | LEXP_cast _ -> rewrap lexp - | LEXP_tup tupls -> rewrap (LEXP_tup (List.map (rewriters.rewrite_lexp rewriters map) tupls)) - | LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map (rewriters.rewrite_exp rewriters map) exps)) + | LEXP_tup tupls -> rewrap (LEXP_tup (List.map (rewriters.rewrite_lexp rewriters) tupls)) + | LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map (rewriters.rewrite_exp rewriters) exps)) | LEXP_vector (lexp,exp) -> - rewrap (LEXP_vector (rewriters.rewrite_lexp rewriters map lexp,rewriters.rewrite_exp rewriters map exp)) + rewrap (LEXP_vector (rewriters.rewrite_lexp rewriters lexp,rewriters.rewrite_exp rewriters exp)) | LEXP_vector_range (lexp,exp1,exp2) -> - rewrap (LEXP_vector_range (rewriters.rewrite_lexp rewriters map lexp, - rewriters.rewrite_exp rewriters map exp1, - rewriters.rewrite_exp rewriters map exp2)) - | LEXP_field (lexp,id) -> rewrap (LEXP_field (rewriters.rewrite_lexp rewriters map lexp,id)) + rewrap (LEXP_vector_range (rewriters.rewrite_lexp rewriters lexp, + rewriters.rewrite_exp rewriters exp1, + rewriters.rewrite_exp rewriters exp2)) + | LEXP_field (lexp,id) -> rewrap (LEXP_field (rewriters.rewrite_lexp rewriters lexp,id)) let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),(l,annot))) = let _ = reset_fresh_name_counter () in (*let _ = Printf.eprintf "Rewriting function %s, pattern %s\n" (match id with (Id_aux (Id i,_)) -> i) (Pretty_print.pat_to_string pat) in*) - let map = get_map_tannot fdannot in + (*let map = get_map_tannot fdannot in let map = match map with | None -> None - | Some m -> Some(m, Envmap.empty) in - (FCL_aux (FCL_Funcl (id,rewriters.rewrite_pat rewriters map pat, - rewriters.rewrite_exp rewriters map exp),(l,annot))) + | Some m -> Some(m, Envmap.empty) in*) + (FCL_aux (FCL_Funcl (id,rewriters.rewrite_pat rewriters pat, + rewriters.rewrite_exp rewriters exp),(l,annot))) in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) let rewrite_def rewriters d = match d with - | DEF_type _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ -> d + | DEF_type _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ -> d | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef) - | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters None letbind) + | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind) | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter") let rewrite_defs_base rewriters (Defs defs) = @@ -538,32 +567,40 @@ let rewrite_defs_base rewriters (Defs defs) = | [] -> [] | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds) in Defs (rewrite defs) + +let rewriters_base = + {rewrite_exp = rewrite_exp; + rewrite_pat = rewrite_pat; + rewrite_let = rewrite_let; + rewrite_lexp = rewrite_lexp; + rewrite_fun = rewrite_fun; + rewrite_def = rewrite_def; + rewrite_defs = rewrite_defs_base} -let rewrite_defs (Defs defs) = rewrite_defs_base - {rewrite_exp = rewrite_exp; - rewrite_pat = rewrite_pat; - rewrite_let = rewrite_let; - rewrite_lexp = rewrite_lexp; - rewrite_fun = rewrite_fun; - rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_base} (Defs defs) +let rewrite_defs (Defs defs) = rewrite_defs_base rewriters_base (Defs defs) +module Envmap = Finite_map.Fmap_map(String) -let rec introduced_variables (E_aux (exp,(l,annot))) = +(* TODO: This seems to only consider a single assignment (or possibly two, in + separate branches of an if-expression). Hence, it seems the result is always + at most one variable. Is this intended? + It is only used below when pulling out local variables inside if-expressions + into the outer scope, which seems dubious. I comment it out for now. *) +(*let rec introduced_variables (E_aux (exp,(l,annot))) = match exp with | E_cast (typ, exp) -> introduced_variables exp | E_if (c,t,e) -> Envmap.intersect (introduced_variables t) (introduced_variables e) | E_assign (lexp,exp) -> introduced_vars_le lexp exp | _ -> Envmap.empty -and introduced_vars_le (LEXP_aux(lexp,(l,annot))) exp = +and introduced_vars_le (LEXP_aux(lexp,annot)) exp = match lexp with | LEXP_id (Id_aux (Id id,_)) | LEXP_cast(_,(Id_aux (Id id,_))) -> (match annot with | Base((_,t),Emp_intro,_,_,_,_) -> Envmap.insert Envmap.empty (id,(t,exp)) | _ -> Envmap.empty) - | _ -> Envmap.empty + | _ -> Envmap.empty*) type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg = { p_lit : lit -> 'pat_aux @@ -656,6 +693,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_case : 'exp * 'pexp list -> 'exp_aux ; e_let : 'letbind * 'exp -> 'exp_aux ; e_assign : 'lexp * 'exp -> 'exp_aux + ; e_sizeof : nexp -> 'exp_aux ; e_exit : 'exp -> 'exp_aux ; e_return : 'exp -> 'exp_aux ; e_assert : 'exp * 'exp -> 'exp_aux @@ -720,6 +758,7 @@ let rec fold_exp_aux alg = function | E_case (e,pexps) -> alg.e_case (fold_exp alg e, List.map (fold_pexp alg) pexps) | E_let (letbind,e) -> alg.e_let (fold_letbind alg letbind, fold_exp alg e) | E_assign (lexp,e) -> alg.e_assign (fold_lexp alg lexp, fold_exp alg e) + | E_sizeof nexp -> alg.e_sizeof nexp | E_exit e -> alg.e_exit (fold_exp alg e) | E_return e -> alg.e_return (fold_exp alg e) | E_assert(e1,e2) -> alg.e_assert (fold_exp alg e1, fold_exp alg e2) @@ -784,6 +823,7 @@ let id_exp_alg = ; e_case = (fun (e1,pexps) -> E_case (e1,pexps)) ; e_let = (fun (lb,e2) -> E_let (lb,e2)) ; e_assign = (fun (lexp,e2) -> E_assign (lexp,e2)) + ; e_sizeof = (fun nexp -> E_sizeof nexp) ; e_exit = (fun e1 -> E_exit (e1)) ; e_return = (fun e1 -> E_return e1) ; e_assert = (fun (e1,e2) -> E_assert(e1,e2)) @@ -816,7 +856,281 @@ let id_exp_alg = ; lB_aux = (fun (lb,annot) -> LB_aux (lb,annot)) ; pat_alg = id_pat_alg } - + +(* Folding algorithms for not only rewriting patterns/expressions, but also + computing some additional value. Usage: Pass default value (bot) and a + binary join operator as arguments, and specify the non-default cases of + rewriting/computation by overwriting fields of the record. + See rewrite_sizeof for examples. *) +let compute_pat_alg bot join = + let join_list vs = List.fold_left join bot vs in + let split_join f ps = let (vs,ps) = List.split ps in (join_list vs, f ps) in + { p_lit = (fun lit -> (bot, P_lit lit)) + ; p_wild = (bot, P_wild) + ; p_as = (fun ((v,pat),id) -> (v, P_as (pat,id))) + ; p_typ = (fun (typ,(v,pat)) -> (v, P_typ (typ,pat))) + ; p_id = (fun id -> (bot, P_id id)) + ; p_app = (fun (id,ps) -> split_join (fun ps -> P_app (id,ps)) ps) + ; p_record = (fun (ps,b) -> split_join (fun ps -> P_record (ps,b)) ps) + ; p_vector = split_join (fun ps -> P_vector ps) + ; p_vector_indexed = (fun ps -> + let (is,ps) = List.split ps in + let (vs,ps) = List.split ps in + (join_list vs, P_vector_indexed (List.combine is ps))) + ; p_vector_concat = split_join (fun ps -> P_vector_concat ps) + ; p_tup = split_join (fun ps -> P_tup ps) + ; p_list = split_join (fun ps -> P_list ps) + ; p_aux = (fun ((v,pat),annot) -> (v, P_aux (pat,annot))) + ; fP_aux = (fun ((v,fpat),annot) -> (v, FP_aux (fpat,annot))) + ; fP_Fpat = (fun (id,(v,pat)) -> (v, FP_Fpat (id,pat))) + } + +let compute_exp_alg bot join = + let join_list vs = List.fold_left join bot vs in + let split_join f es = let (vs,es) = List.split es in (join_list vs, f es) in + { e_block = split_join (fun es -> E_block es) + ; e_nondet = split_join (fun es -> E_nondet es) + ; e_id = (fun id -> (bot, E_id id)) + ; e_lit = (fun lit -> (bot, E_lit lit)) + ; e_cast = (fun (typ,(v,e)) -> (v, E_cast (typ,e))) + ; e_app = (fun (id,es) -> split_join (fun es -> E_app (id,es)) es) + ; e_app_infix = (fun ((v1,e1),id,(v2,e2)) -> (join v1 v2, E_app_infix (e1,id,e2))) + ; e_tuple = split_join (fun es -> E_tuple es) + ; e_if = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_if (e1,e2,e3))) + ; e_for = (fun (id,(v1,e1),(v2,e2),(v3,e3),order,(v4,e4)) -> + (join_list [v1;v2;v3;v4], E_for (id,e1,e2,e3,order,e4))) + ; e_vector = split_join (fun es -> E_vector es) + ; e_vector_indexed = (fun (es,(v2,opt2)) -> + let (is,es) = List.split es in + let (vs,es) = List.split es in + (join_list (vs @ [v2]), E_vector_indexed (List.combine is es,opt2))) + ; e_vector_access = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_vector_access (e1,e2))) + ; e_vector_subrange = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_vector_subrange (e1,e2,e3))) + ; e_vector_update = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_vector_update (e1,e2,e3))) + ; e_vector_update_subrange = (fun ((v1,e1),(v2,e2),(v3,e3),(v4,e4)) -> (join_list [v1;v2;v3;v4], E_vector_update_subrange (e1,e2,e3,e4))) + ; 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_field = (fun ((v1,e1),id) -> (v1, E_field (e1,id))) + ; e_case = (fun ((v1,e1),pexps) -> + let (vps,pexps) = List.split pexps in + (join_list (v1::vps), E_case (e1,pexps))) + ; e_let = (fun ((vl,lb),(v2,e2)) -> (join vl v2, E_let (lb,e2))) + ; e_assign = (fun ((vl,lexp),(v2,e2)) -> (join vl v2, E_assign (lexp,e2))) + ; e_sizeof = (fun nexp -> (bot, E_sizeof nexp)) + ; e_exit = (fun (v1,e1) -> (v1, E_exit (e1))) + ; e_return = (fun (v1,e1) -> (v1, E_return e1)) + ; e_assert = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_assert(e1,e2)) ) + ; e_internal_cast = (fun (a,(v1,e1)) -> (v1, E_internal_cast (a,e1))) + ; e_internal_exp = (fun a -> (bot, E_internal_exp a)) + ; e_internal_exp_user = (fun (a1,a2) -> (bot, E_internal_exp_user (a1,a2))) + ; e_internal_let = (fun ((vl, lexp), (v2,e2), (v3,e3)) -> + (join_list [vl;v2;v3], E_internal_let (lexp,e2,e3))) + ; e_internal_plet = (fun ((vp,pat), (v1,e1), (v2,e2)) -> + (join_list [vp;v1;v2], E_internal_plet (pat,e1,e2))) + ; e_internal_return = (fun (v,e) -> (v, E_internal_return e)) + ; e_aux = (fun ((v,e),annot) -> (v, E_aux (e,annot))) + ; lEXP_id = (fun id -> (bot, LEXP_id id)) + ; lEXP_memory = (fun (id,es) -> split_join (fun es -> LEXP_memory (id,es)) es) + ; lEXP_cast = (fun (typ,id) -> (bot, LEXP_cast (typ,id))) + ; lEXP_tup = split_join (fun tups -> LEXP_tup tups) + ; lEXP_vector = (fun ((vl,lexp),(v2,e2)) -> (join vl v2, LEXP_vector (lexp,e2))) + ; lEXP_vector_range = (fun ((vl,lexp),(v2,e2),(v3,e3)) -> + (join_list [vl;v2;v3], LEXP_vector_range (lexp,e2,e3))) + ; lEXP_field = (fun ((vl,lexp),id) -> (vl, LEXP_field (lexp,id))) + ; 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))) + ; pat_exp = (fun ((vp,pat),(v,e)) -> (join vp v, Pat_exp (pat,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_aux = (fun ((vl,lb),annot) -> (vl,LB_aux (lb,annot))) + ; pat_alg = compute_pat_alg bot join + } + + +(* Rewrite sizeof expressions with type-level variables to + term-level expressions + + For each type-level variable used in a sizeof expressions whose value cannot + be directly extracted from existing parameters of the surrounding function, + a further parameter is added; calls to the function are rewritten + accordingly (possibly causing further rewriting in the calling function) *) +let rewrite_sizeof (Defs defs) = + let sizeof_frees exp = + fst (fold_exp + { (compute_exp_alg KidSet.empty KidSet.union) with + e_sizeof = (fun nexp -> (nexp_frees nexp, E_sizeof nexp)) } + exp) in + + (* Collect nexps whose values can be obtained directly from a pattern bind *) + let nexps_from_params pat = + fst (fold_pat + { (compute_pat_alg [] (@)) with + p_aux = (fun ((v,pat),((l,_) as annot)) -> + let v' = match pat with + | P_id id | P_as (_, id) -> + let (Typ_aux (typ,_) as typ_aux) = typ_of_annot annot in + (match typ with + | Typ_app (atom, [Typ_arg_aux (Typ_arg_nexp nexp, _)]) + when string_of_id atom = "atom" -> + [nexp, E_id id] + | Typ_app (vector, _) when string_of_id vector = "vector" -> + let (_,len,_,_) = vector_typ_args_of typ_aux in + let exp = E_app + (Id_aux (Id "length", Parse_ast.Generated l), + [E_aux (E_id id, annot)]) in + [len, exp] + | _ -> []) + | _ -> [] in + (v @ v', P_aux (pat,annot)))} pat) in + + (* Substitute collected values in sizeof expressions *) + let rec e_sizeof nmap (Nexp_aux (nexp, l) as nexp_aux) = + try snd (List.find (fun (nexp,_) -> nexp_identical nexp nexp_aux) nmap) + with + | Not_found -> + let binop nexp1 op nexp2 = E_app_infix ( + E_aux (e_sizeof nmap nexp1, simple_annot l (atom_typ nexp1)), + Id_aux (Id op, Parse_ast.Unknown), + E_aux (e_sizeof nmap nexp2, simple_annot l (atom_typ nexp2)) + ) in + (match nexp with + | Nexp_constant i -> E_lit (L_aux (L_num i, l)) + | Nexp_times (nexp1, nexp2) -> binop nexp1 "*" nexp2 + | Nexp_sum (nexp1, nexp2) -> binop nexp1 "+" nexp2 + | Nexp_minus (nexp1, nexp2) -> binop nexp1 "-" nexp2 + | _ -> E_sizeof nexp_aux) in + + (* Rewrite calls to functions which have had parameters added to pass values + of type-level variables; these are added as sizeof expressions first, and + then further rewritten as above. *) + let e_app_aux param_map (exp, ((l,_) as annot)) = + let full_exp = E_aux (exp, annot) in + match exp with + | E_app (f, args) -> + if Bindings.mem f param_map then + (* Retrieve instantiation of the type variables of the called function + for the given parameters in the current environment *) + let inst = instantiation_of full_exp in + let kid_exp kid = begin + match KBindings.find kid inst with + | U_nexp nexp -> E_aux (E_sizeof nexp, simple_annot l (atom_typ nexp)) + | _ -> + raise (Reporting_basic.err_unreachable l + ("failed to infer nexp for type variable " ^ string_of_kid kid ^ + " of function " ^ string_of_id f)) + end in + let kid_exps = List.map kid_exp (KidSet.elements (Bindings.find f param_map)) in + E_aux (E_app (f, kid_exps @ args), annot) + else full_exp + | _ -> full_exp in + + let rewrite_sizeof_fun params_map + (FD_aux (FD_function (rec_opt,tannot,eff,funcls),((l,_) as annot))) = + let rewrite_funcl_body (FCL_aux (FCL_Funcl (id,pat,exp), annot)) (funcls,nvars) = + let body_env = env_of exp in + let body_typ = typ_of exp in + let nmap = nexps_from_params pat in + (* first rewrite calls to other functions... *) + let exp' = fold_exp { id_exp_alg with e_aux = e_app_aux params_map } exp in + (* ... then rewrite sizeof expressions in current function body *) + let exp'' = fold_exp { id_exp_alg with e_sizeof = e_sizeof nmap } exp' in + (FCL_aux (FCL_Funcl (id,pat,exp''), annot) :: funcls, + KidSet.union nvars (sizeof_frees exp'')) in + let (funcls, nvars) = List.fold_right rewrite_funcl_body funcls ([], KidSet.empty) in + (* Add a parameter for each remaining free type-level variable in a + sizeof expression *) + let kid_typ kid = atom_typ (nvar kid) in + let kid_annot kid = simple_annot l (kid_typ kid) in + let kid_pat kid = + P_aux (P_typ (kid_typ kid, + P_aux (P_id (Id_aux (Id (string_of_kid kid), l)), + kid_annot kid)), kid_annot kid) in + let kid_eaux kid = E_id (Id_aux (Id (string_of_kid kid), l)) in + let kid_typs = List.map kid_typ (KidSet.elements nvars) in + let kid_pats = List.map kid_pat (KidSet.elements nvars) in + let kid_nmap = List.map (fun kid -> (nvar kid, kid_eaux kid)) (KidSet.elements nvars) in + let rewrite_funcl_params (FCL_aux (FCL_Funcl (id, pat, exp), annot) as funcl) = + let rec rewrite_pat (P_aux (pat,(l,_)) as paux) = + if KidSet.is_empty nvars then paux else + match pat_typ_of paux with + | Typ_aux (Typ_tup _, _) -> + (match pat with + | P_tup pats -> + P_aux (P_tup (kid_pats @ pats), (l, None)) + | P_wild -> paux + | 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, None)) + | 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 *) + raise (Reporting_basic.err_todo l + "rewriting as- or id-patterns for sizeof expressions not yet implemented") + | _ -> + raise (Reporting_basic.err_unreachable l + "unexpected pattern while rewriting function parameters for sizeof expressions")) + | _ -> P_aux (P_tup (kid_pats @ [paux]), (l, None)) in + let exp' = fold_exp { id_exp_alg with e_sizeof = e_sizeof kid_nmap } exp in + FCL_aux (FCL_Funcl (id, rewrite_pat pat, exp'), annot) in + let funcls = List.map rewrite_funcl_params funcls in + (nvars, FD_aux (FD_function (rec_opt,tannot,eff,funcls),annot)) in + + let rewrite_sizeof_fundef (params_map, defs) = function + | DEF_fundef fd -> + let (nvars, fd') = rewrite_sizeof_fun params_map fd in + let params_map' = + if KidSet.is_empty nvars then params_map + else Bindings.add (id_of_fundef fd) nvars params_map in + (params_map', defs @ [DEF_fundef fd']) + | def -> + (params_map, defs @ [def]) in + + let rewrite_sizeof_valspec params_map def = + let rewrite_typschm (TypSchm_aux (TypSchm_ts (tq, typ), l) as ts) id = + if Bindings.mem id params_map then + let kid_typs = List.map (fun kid -> atom_typ (nvar kid)) + (KidSet.elements (Bindings.find id params_map)) in + let typ' = match typ with + | Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, declared_eff), vl) -> + let vtyp_arg' = begin + match vtyp_arg with + | Typ_aux (Typ_tup typs, vl) -> + Typ_aux (Typ_tup (kid_typs @ typs), vl) + | _ -> Typ_aux (Typ_tup (kid_typs @ [vtyp_arg]), vl) + end in + Typ_aux (Typ_fn (vtyp_arg', vtyp_ret, declared_eff), vl) + | _ -> raise (Reporting_basic.err_typ l + "val spec with non-function type") in + TypSchm_aux (TypSchm_ts (tq, typ'), l) + else ts in + match def with + | DEF_spec (VS_aux (VS_val_spec (typschm, id), a)) -> + DEF_spec (VS_aux (VS_val_spec (rewrite_typschm typschm id, id), a)) + | DEF_spec (VS_aux (VS_extern_no_rename (typschm, id), a)) -> + DEF_spec (VS_aux (VS_extern_no_rename (rewrite_typschm typschm id, id), a)) + | DEF_spec (VS_aux (VS_extern_spec (typschm, id, e), a)) -> + DEF_spec (VS_aux (VS_extern_spec (rewrite_typschm typschm id, id, e), a)) + | DEF_spec (VS_aux (VS_cast_spec (typschm, id), a)) -> + DEF_spec (VS_aux (VS_cast_spec (rewrite_typschm typschm id, id), a)) + | _ -> def in + + let (params_map, defs) = List.fold_left rewrite_sizeof_fundef + (Bindings.empty, []) defs in + let defs = List.map (rewrite_sizeof_valspec params_map) defs in + fst (check initial_env (Defs defs)) + let remove_vector_concat_pat pat = @@ -830,12 +1144,10 @@ let remove_vector_concat_pat pat = ) } in - let pat = remove_typed_patterns pat in + (* let pat = remove_typed_patterns pat in *) + + let fresh_id_v = fresh_id "v__" in - let fresh_name l = - let current = fresh_name () in - Id_aux (Id ("v__" ^ string_of_int current), Parse_ast.Generated l) in - (* expects that P_typ elements have been removed from AST, that the length of all vectors involved is known, that we don't have indexed vectors *) @@ -860,7 +1172,7 @@ let remove_vector_concat_pat pat = | P_vector_concat pats -> (if contained_in_p_as then P_aux (pat,annot) - else P_aux (P_as (P_aux (pat,annot),fresh_name l),annot)) + else P_aux (P_as (P_aux (pat,annot),fresh_id_v l),annot)) | _ -> P_aux (pat,annot) ) ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot)) @@ -872,10 +1184,11 @@ let remove_vector_concat_pat pat = (* introduce names for all unnamed child nodes of P_vector_concat *) let name_vector_concat_elements = let p_vector_concat pats = - let aux ((P_aux (p,((l,_) as a))) as pat) = match p with - | P_vector _ -> P_aux (P_as (pat,fresh_name l),a) + let rec aux ((P_aux (p,((l,_) as a))) as pat) = match p with + | P_vector _ -> P_aux (P_as (pat,fresh_id_v l),a) | P_id id -> P_aux (P_id id,a) | P_as (p,id) -> P_aux (P_as (p,id),a) + | P_typ (typ, pat) -> P_aux (P_typ (typ, aux pat),a) | P_wild -> P_aux (P_wild,a) | _ -> raise @@ -886,7 +1199,7 @@ let remove_vector_concat_pat pat = let pat = fold_pat name_vector_concat_elements pat in - + let rec tag_last = function | x :: xs -> let is_last = xs = [] in (x,is_last) :: tag_last xs @@ -903,102 +1216,78 @@ let remove_vector_concat_pat pat = pat_alg = *) (* build a let-expression of the form "let child = root[i..j] in body" *) - let letbind_vec (rootid,rannot) (child,cannot) (i,j) = + let letbind_vec typ_opt (rootid,rannot) (child,cannot) (i,j) = let (l,_) = cannot in let (Id_aux (Id rootname,_)) = rootid in let (Id_aux (Id childname,_)) = child in - let simple_num n : tannot exp = - let typ = simple_annot (mk_atom_typ (mk_c (big_int_of_int n))) in - E_aux (E_lit (L_aux (L_num n,l)), (l,typ)) in - - let vlength_info (Base ((_,{t = Tapp("vector",[_;TA_nexp nexp;_;_])}),_,_,_,_,_)) = - nexp in - - let root : tannot exp = E_aux (E_id rootid,rannot) in - let index_i = simple_num i in - let index_j : tannot exp = match j with - | Some j -> simple_num j - | None -> - let length_root_nexp = vlength_info (snd rannot) in - let length_app_exp : tannot exp = - let typ = mk_atom_typ length_root_nexp in - let annot = (l,tag_annot typ (External (Some "length"))) in - E_aux (E_app (Id_aux (Id "length",l),[root]),annot) in - let minus = Id_aux (Id "-",l) in - let one_exp : tannot exp = - let typ = (mk_atom_typ (mk_c unit_big_int)) in - let annot = (l,simple_annot typ) in - E_aux (E_lit (L_aux (L_num 1,l)),annot) in - - let typ = mk_atom_typ (mk_sub length_root_nexp (mk_c unit_big_int)) in - let annot = (l,tag_annot typ (External (Some "minus"))) in - let exp : tannot exp = - E_aux (E_app_infix(length_app_exp,minus,one_exp),annot) in - exp in - - let subv = E_aux (E_app (Id_aux (Id "slice_raw",Unknown), - [root;index_i;index_j]),cannot) in - - let typ = (Parse_ast.Generated l,simple_annot {t = Tid "unit"}) in + let root = E_aux (E_id rootid, rannot) in + let index_i = simple_num l i in + let index_j = simple_num l j in - let letbind = LB_val_implicit (P_aux (P_id child,cannot),subv) in - (LB_aux (letbind,typ), - (fun body -> E_aux (E_let (LB_aux (letbind,cannot),body),typ)), + let subv = fix_eff_exp (E_aux (E_vector_subrange (root, index_i, index_j), cannot)) in + + let id_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 + (letbind, + (fun body -> fix_eff_exp (E_aux (E_let (letbind,body), simple_annot l (typ_of body)))), (rootname,childname)) in let p_aux = function | ((P_as (P_aux (P_vector_concat pats,rannot'),rootid),decls),rannot) -> - let aux (pos,pat_acc,decl_acc) (P_aux (p,cannot),is_last) = match cannot with - | (_,Base((_,{t = Tapp ("vector",[_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_)) - | (_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector",[_;TA_nexp {nexp = Nconst length};_;_])})}),_,_,_,_,_)) -> - let length = int_of_big_int length in + let rtyp = Env.base_typ_of (env_of_annot rannot') (typ_of_annot rannot') in + let (start,last_idx) = (match vector_typ_args_of rtyp with + | (Nexp_aux (Nexp_constant start,_), Nexp_aux (Nexp_constant length,_), ord, _) -> + (start, if is_order_inc ord then start + length - 1 else start - length + 1) + | _ -> + raise (Reporting_basic.err_unreachable (fst rannot') + ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern"))) in + let rec aux typ_opt (pos,pat_acc,decl_acc) (P_aux (p,cannot),is_last) = + let ctyp = Env.base_typ_of (env_of_annot cannot) (typ_of_annot cannot) in + let (_,length,ord,_) = vector_typ_args_of ctyp in + (*)| (_,length,ord,_) ->*) + let (pos',index_j) = match length with + | Nexp_aux (Nexp_constant i,_) -> + if is_order_inc ord then (pos+i, pos+i-1) + else (pos-i, pos-i+1) + | Nexp_aux (_,l) -> + if is_last then (pos,last_idx) + else + raise + (Reporting_basic.err_unreachable + l ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern")) in (match p with (* if we see a named vector pattern, remove the name and remember to declare it later *) | P_as (P_aux (p,cannot),cname) -> - let (lb,decl,info) = letbind_vec (rootid,rannot) (cname,cannot) (pos,Some(pos+length-1)) in - (pos + length, pat_acc @ [P_aux (p,cannot)], decl_acc @ [((lb,decl),info)]) + let (lb,decl,info) = letbind_vec typ_opt (rootid,rannot) (cname,cannot) (pos,index_j) in + (pos', pat_acc @ [P_aux (p,cannot)], decl_acc @ [((lb,decl),info)]) (* if we see a P_id variable, remember to declare it later *) | P_id cname -> - let (lb,decl,info) = letbind_vec (rootid,rannot) (cname,cannot) (pos,Some(pos+length-1)) in - (pos + length, pat_acc @ [P_aux (P_id cname,cannot)], decl_acc @ [((lb,decl),info)]) + let (lb,decl,info) = letbind_vec typ_opt (rootid,rannot) (cname,cannot) (pos,index_j) in + (pos', pat_acc @ [P_aux (P_id cname,cannot)], decl_acc @ [((lb,decl),info)]) + | P_typ (typ, pat) -> aux (Some typ) (pos,pat_acc,decl_acc) (pat, is_last) (* normal vector patterns are fine *) - | _ -> (pos + length, pat_acc @ [P_aux (p,cannot)],decl_acc) ) + | _ -> (pos', pat_acc @ [P_aux (p,cannot)],decl_acc) ) (* non-vector patterns aren't *) - | (l,Base((_,{t = Tapp ("vector",[_;_;_;_])}),_,_,_,_,_)) - | (l,Base((_,{t = Tabbrev (_,{t = Tapp ("vector",[_;_;_;_])})}),_,_,_,_,_)) -> - if is_last then - match p with - (* if we see a named vector pattern, remove the name and remember to - declare it later *) - | P_as (P_aux (p,cannot),cname) -> - let (lb,decl,info) = letbind_vec (rootid,rannot) (cname,cannot) (pos,None) in - (pos, pat_acc @ [P_aux (p,cannot)], decl_acc @ [((lb,decl),info)]) - (* if we see a P_id variable, remember to declare it later *) - | P_id cname -> - let (lb,decl,info) = letbind_vec (rootid,rannot) (cname,cannot) (pos,None) in - (pos, pat_acc @ [P_aux (P_id cname,cannot)], decl_acc @ [((lb,decl),info)]) - (* normal vector patterns are fine *) - | _ -> (pos, pat_acc @ [P_aux (p,cannot)],decl_acc) - else + (*)| _ -> raise (Reporting_basic.err_unreachable - l ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern")) - | (l,Base((_,t),_,_,_,_,_)) -> - raise - (Reporting_basic.err_unreachable - l ("unname_vector_concat_elements: Non-vector in vector-concat pattern:" ^ - t_to_string t) - ) in + (fst cannot) + ("unname_vector_concat_elements: Non-vector in vector-concat pattern:" ^ + string_of_typ (typ_of_annot cannot)) + )*) in let pats_tagged = tag_last pats in - let (_,pats',decls') = List.fold_left aux (0,[],[]) pats_tagged in + let (_,pats',decls') = List.fold_left (aux None) (start,[],[]) pats_tagged in (* abuse P_vector_concat as a P_vector_const pattern: it has the of patterns as an argument but they're meant to be consed together *) (P_aux (P_as (P_aux (P_vector_concat pats',rannot'),rootid),rannot), decls @ decls') | ((p,decls),annot) -> (P_aux (p,annot),decls) in - + { p_lit = (fun lit -> (P_lit lit,[])) ; p_wild = (P_wild,[]) ; p_as = (fun ((pat,decls),id) -> (P_as (pat,id),decls)) @@ -1079,41 +1368,28 @@ let remove_vector_concat_pat pat = let remove_vector_concats = let p_vector_concat ps = let aux acc (P_aux (p,annot),is_last) = + let env = env_of_annot annot in + let typ = Env.base_typ_of env (typ_of_annot annot) in + let eff = effect_of_annot (snd annot) in let (l,_) = annot in - match p,annot with - | P_vector ps,_ -> acc @ ps - | P_id _,(_,Base((_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_)) - | P_id _,(_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector",[_;TA_nexp {nexp = Nconst length};_;_])})}),_,_,_,_,_)) - | P_wild,(_,Base((_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_)) - | P_wild,(_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])})}),_,_,_,_,_)) -> - let wild _ = P_aux (P_wild,(Parse_ast.Generated l,simple_annot {t = Tid "bit"})) in - acc @ (List.map wild (range 0 ((int_of_big_int length) - 1))) - | P_id _,(_,Base((_,{t = Tapp ("vector", _)}),_,_,_,_,_)) - | P_id _,(_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector",_)})}),_,_,_,_,_)) - | P_wild,(_,Base((_,{t = Tapp ("vector", _)}),_,_,_,_,_)) - | P_wild,(_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector", _)})}),_,_,_,_,_)) - when is_last -> - let wild _ = P_aux (P_wild,(Parse_ast.Generated l,simple_annot {t = Tid "bit"})) in - acc @ [P_aux(P_wild,annot)] - | P_lit _,(l,_) -> - raise (Reporting_basic.err_unreachable l "remove_vector_concats: P_lit pattern in vector-concat pattern") - | _,(l,Base((_,t),_,_,_,_,_)) -> - raise (Reporting_basic.err_unreachable l ("remove_vector_concats: Non-vector in vector-concat pattern " ^ - t_to_string t)) in + let wild _ = P_aux (P_wild,(Parse_ast.Generated l, Some (env, bit_typ, eff))) in + if is_vector_typ typ then + match p, vector_typ_args_of typ with + | P_vector ps,_ -> acc @ ps + | _, (_,Nexp_aux (Nexp_constant length,_),_,_) -> + acc @ (List.map wild (range 0 (length - 1))) + | _, _ -> + (*if is_last then*) acc @ [wild 0] + else raise + (Reporting_basic.err_unreachable l + ("remove_vector_concats: Non-vector in vector-concat pattern " ^ + string_of_typ (typ_of_annot annot))) in let has_length (P_aux (p,annot)) = - match p,annot with - | P_vector _,_ -> true - | P_id _,(_,Base((_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_)) - | P_id _,(_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector",[_;TA_nexp {nexp = Nconst length};_;_])})}),_,_,_,_,_)) - | P_wild,(_,Base((_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_)) - | P_wild,(_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])})}),_,_,_,_,_)) -> - true - | P_id _,(_,Base((_,{t = Tapp ("vector", _)}),_,_,_,_,_)) - | P_id _,(_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector",_)})}),_,_,_,_,_)) - | P_wild,(_,Base((_,{t = Tapp ("vector", _)}),_,_,_,_,_)) - | P_wild,(_,Base((_,{t = Tabbrev (_,{t = Tapp ("vector", _)})}),_,_,_,_,_)) -> - false in + let typ = Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) in + match vector_typ_args_of typ with + | (_,Nexp_aux (Nexp_constant length,_),_,_) -> true + | _ -> false in let ps_tagged = tag_last ps in let ps' = List.fold_left aux [] ps_tagged in @@ -1135,16 +1411,16 @@ let remove_vector_concat_pat pat = (pat,letbinds,decls) (* assumes there are no more E_internal expressions *) -let rewrite_exp_remove_vector_concat_pat rewriters nmap (E_aux (exp,(l,annot)) as full_exp) = +let rewrite_exp_remove_vector_concat_pat rewriters (E_aux (exp,(l,annot)) as full_exp) = let rewrap e = E_aux (e,(l,annot)) in - let rewrite_rec = rewriters.rewrite_exp rewriters nmap in - let rewrite_base = rewrite_exp rewriters nmap in + let rewrite_rec = rewriters.rewrite_exp rewriters in + let rewrite_base = rewrite_exp rewriters in match exp with | E_case (e,ps) -> let aux (Pat_aux (Pat_exp (pat,body),annot')) = let (pat,_,decls) = remove_vector_concat_pat pat in - Pat_aux (Pat_exp (pat,decls (rewrite_rec body)),annot') in - rewrap (E_case (rewrite_rec e,List.map aux ps)) + Pat_aux (Pat_exp (pat, 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) -> let (pat,_,decls) = remove_vector_concat_pat pat in rewrap (E_let (LB_aux (LB_val_explicit (typ,pat,rewrite_rec v),annot'), @@ -1158,11 +1434,20 @@ let rewrite_exp_remove_vector_concat_pat rewriters nmap (E_aux (exp,(l,annot)) a let rewrite_fun_remove_vector_concat_pat rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),(l,annot))) = - let (pat,_,decls) = remove_vector_concat_pat pat in - (FCL_aux (FCL_Funcl (id,pat,rewriters.rewrite_exp rewriters None (decls exp)),(l,annot))) + let (pat',_,decls) = remove_vector_concat_pat pat in + let exp' = decls (rewriters.rewrite_exp rewriters exp) in + (FCL_aux (FCL_Funcl (id,pat',exp'),(l,annot))) in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) -let rewrite_defs_remove_vector_concat_pat rewriters (Defs defs) = +let rewrite_defs_remove_vector_concat (Defs defs) = + let rewriters = + {rewrite_exp = rewrite_exp_remove_vector_concat_pat; + rewrite_pat = rewrite_pat; + rewrite_let = rewrite_let; + rewrite_lexp = rewrite_lexp; + rewrite_fun = rewrite_fun_remove_vector_concat_pat; + rewrite_def = rewrite_def; + rewrite_defs = rewrite_defs_base} in let rewrite_def d = let d = rewriters.rewrite_def rewriters d in match d with @@ -1174,41 +1459,464 @@ let rewrite_defs_remove_vector_concat_pat rewriters (Defs defs) = 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 - | d -> [rewriters.rewrite_def rewriters d] in + | d -> [d] in Defs (List.flatten (List.map rewrite_def defs)) -let rewrite_defs_remove_vector_concat defs = rewrite_defs_base - {rewrite_exp = rewrite_exp_remove_vector_concat_pat; +let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with +| P_lit _ | P_wild | P_id _ -> false +| P_as (pat,_) | P_typ (_,pat) -> contains_bitvector_pat pat +| P_vector _ | P_vector_concat _ | P_vector_indexed _ -> + let typ = Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) in + is_bitvector_typ typ +| P_app (_,pats) | P_tup pats | P_list pats -> + List.exists contains_bitvector_pat pats +| P_record (fpats,_) -> + List.exists (fun (FP_aux (FP_Fpat (_,pat),_)) -> contains_bitvector_pat pat) fpats + +let remove_bitvector_pat pat = + + (* first introduce names for bitvector patterns *) + let name_bitvector_roots = + { p_lit = (fun lit -> P_lit lit) + ; p_typ = (fun (typ,p) -> P_typ (typ,p false)) + ; p_wild = P_wild + ; p_as = (fun (pat,id) -> P_as (pat true,id)) + ; p_id = (fun id -> P_id id) + ; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps)) + ; p_record = (fun (fpats,b) -> P_record (fpats, b)) + ; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps)) + ; p_vector_indexed = (fun ps -> P_vector_indexed (List.map (fun (i,p) -> (i,p false)) ps)) + ; p_vector_concat = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps)) + ; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps)) + ; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps)) + ; p_aux = + (fun (pat,annot) contained_in_p_as -> + let env = env_of_annot annot in + let t = Env.base_typ_of env (typ_of_annot annot) in + let (l,_) = annot in + match pat, is_bitvector_typ t, contained_in_p_as with + | P_vector _, true, false + | P_vector_indexed _, true, false -> + P_aux (P_as (P_aux (pat,annot),fresh_id "b__" l), annot) + | _ -> P_aux (pat,annot) + ) + ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot)) + ; fP_Fpat = (fun (id,p) -> FP_Fpat (id,p false)) + } in + let pat = (fold_pat name_bitvector_roots pat) false in + + (* Then collect guard expressions testing whether the literal bits of a + bitvector pattern match those of a given bitvector, and collect let + bindings for the bits bound by P_id or P_as patterns *) + + (* Helper functions for generating guard expressions *) + let access_bit_exp (rootid,rannot) l idx = + let root : tannot exp = E_aux (E_id rootid,rannot) in + E_aux (E_vector_access (root,simple_num l idx), simple_annot l bit_typ) in + + let test_bit_exp rootid l t idx exp = + let rannot = simple_annot l t in + let elem = access_bit_exp (rootid,rannot) l idx in + let eqid = Id_aux (Id "eq", Parse_ast.Generated l) in + let eqannot = simple_annot l bool_typ in + let eqexp : tannot exp = E_aux (E_app(eqid,[elem;exp]), eqannot) in + Some (eqexp) in + + let test_subvec_exp rootid l typ i j lits = + let (start, length, ord, _) = vector_typ_args_of typ in + let length' = nconstant (List.length lits) in + let start' = + if is_order_inc ord then nconstant 0 + else nminus length' (nconstant 1) in + let typ' = vector_typ start' length' ord bit_typ in + let subvec_exp = + match start, length with + | Nexp_aux (Nexp_constant s, _), Nexp_aux (Nexp_constant l, _) + when s = i && l = List.length lits -> + E_id rootid + | _ -> + (*if vec_start t = i && vec_length t = List.length lits + then E_id rootid + else*) E_vector_subrange ( + E_aux (E_id rootid, simple_annot l typ), + simple_num l i, + simple_num l j) in + E_aux (E_app( + Id_aux (Id "eq_vec", Parse_ast.Generated l), + [E_aux (subvec_exp, simple_annot l typ'); + E_aux (E_vector lits, simple_annot l typ')]), + simple_annot l bool_typ) in + + let letbind_bit_exp rootid l typ idx id = + 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 letexp = (fun body -> + let (E_aux (_,(_,bannot))) = body in + E_aux (E_let (letbind,body), (Parse_ast.Generated l, bannot))) in + (letexp, letbind) in + + (* Helper functions for composing guards *) + let bitwise_and exp1 exp2 = + let (E_aux (_,(l,_))) = exp1 in + let andid = Id_aux (Id "bool_and", Parse_ast.Generated l) in + E_aux (E_app(andid,[exp1;exp2]), simple_annot l bool_typ) in + + let compose_guards guards = + List.fold_right (Util.option_binop bitwise_and) guards None in + + let flatten_guards_decls gd = + let (guards,decls,letbinds) = Util.split3 gd in + (compose_guards guards, (List.fold_right (@@) decls), List.flatten letbinds) in + + (* Collect guards and let bindings *) + let guard_bitvector_pat = + let collect_guards_decls ps rootid t = + let (start,_,ord,_) = vector_typ_args_of t in + let rec collect current (guards,dls) idx ps = + let idx' = if is_order_inc ord then idx + 1 else idx - 1 in + (match ps with + | pat :: ps' -> + (match pat with + | P_aux (P_lit lit, (l,annot)) -> + let e = E_aux (E_lit lit, (Parse_ast.Generated l, annot)) in + let current' = (match current with + | Some (l,i,j,lits) -> Some (l,i,idx,lits @ [e]) + | None -> Some (l,idx,idx,[e])) in + collect current' (guards, dls) idx' ps' + | P_aux (P_as (pat',id), (l,annot)) -> + let dl = letbind_bit_exp rootid l t idx id in + collect current (guards, dls @ [dl]) idx (pat' :: ps') + | _ -> + let dls' = (match pat with + | P_aux (P_id id, (l,annot)) -> + dls @ [letbind_bit_exp rootid l t idx id] + | _ -> dls) in + let guards' = (match current with + | Some (l,i,j,lits) -> + guards @ [Some (test_subvec_exp rootid l t i j lits)] + | None -> guards) in + collect None (guards', dls') idx' ps') + | [] -> + let guards' = (match current with + | Some (l,i,j,lits) -> + guards @ [Some (test_subvec_exp rootid l t i j lits)] + | None -> guards) in + (guards',dls)) in + let (guards,dls) = match start with + | Nexp_aux (Nexp_constant s, _) -> + collect None ([],[]) s ps + | _ -> + let (P_aux (_, (l,_))) = pat in + raise (Reporting_basic.err_unreachable l + "guard_bitvector_pat called on pattern with non-constant start index") in + let (decls,letbinds) = List.split dls in + (compose_guards guards, List.fold_right (@@) decls, letbinds) in + + let collect_guards_decls_indexed ips rootid t = + let rec guard_decl (idx,pat) = (match pat with + | P_aux (P_lit lit, (l,annot)) -> + let exp = E_aux (E_lit lit, (l,annot)) in + (test_bit_exp rootid l t idx exp, (fun b -> b), []) + | P_aux (P_as (pat',id), (l,annot)) -> + let (guard,decls,letbinds) = guard_decl (idx,pat') in + let (letexp,letbind) = letbind_bit_exp rootid l t idx id in + (guard, decls >> letexp, letbind :: letbinds) + | P_aux (P_id id, (l,annot)) -> + let (letexp,letbind) = letbind_bit_exp rootid l t idx id in + (None, letexp, [letbind]) + | _ -> (None, (fun b -> b), [])) in + let (guards,decls,letbinds) = Util.split3 (List.map guard_decl ips) in + (compose_guards guards, List.fold_right (@@) decls, List.flatten letbinds) in + + { p_lit = (fun lit -> (P_lit lit, (None, (fun b -> b), []))) + ; p_wild = (P_wild, (None, (fun b -> b), [])) + ; p_as = (fun ((pat,gdls),id) -> (P_as (pat,id), gdls)) + ; p_typ = (fun (typ,(pat,gdls)) -> (P_typ (typ,pat), gdls)) + ; p_id = (fun id -> (P_id id, (None, (fun b -> b), []))) + ; p_app = (fun (id,ps) -> let (ps,gdls) = List.split ps in + (P_app (id,ps), flatten_guards_decls gdls)) + ; p_record = (fun (ps,b) -> let (ps,gdls) = List.split ps in + (P_record (ps,b), flatten_guards_decls gdls)) + ; p_vector = (fun ps -> let (ps,gdls) = List.split ps in + (P_vector ps, flatten_guards_decls gdls)) + ; p_vector_indexed = (fun p -> let (is,p) = List.split p in + let (ps,gdls) = List.split p in + let ps = List.combine is ps in + (P_vector_indexed ps, flatten_guards_decls gdls)) + ; p_vector_concat = (fun ps -> let (ps,gdls) = List.split ps in + (P_vector_concat ps, flatten_guards_decls gdls)) + ; p_tup = (fun ps -> let (ps,gdls) = List.split ps in + (P_tup ps, flatten_guards_decls gdls)) + ; p_list = (fun ps -> let (ps,gdls) = List.split ps in + (P_list ps, flatten_guards_decls gdls)) + ; p_aux = (fun ((pat,gdls),annot) -> + let env = env_of_annot annot in + let t = Env.base_typ_of env (typ_of_annot annot) in + (match pat, is_bitvector_typ t with + | P_as (P_aux (P_vector ps, _), id), true -> + (P_aux (P_id id, annot), collect_guards_decls ps id t) + | P_as (P_aux (P_vector_indexed ips, _), id), true -> + (P_aux (P_id id, annot), collect_guards_decls_indexed ips id t) + | _, _ -> (P_aux (pat,annot), gdls))) + ; fP_aux = (fun ((fpat,gdls),annot) -> (FP_aux (fpat,annot), gdls)) + ; fP_Fpat = (fun (id,(pat,gdls)) -> (FP_Fpat (id,pat), gdls)) + } in + fold_pat guard_bitvector_pat pat + +let remove_wildcards pre (P_aux (_,(l,_)) as pat) = + fold_pat + {id_pat_alg with + p_aux = function + | (P_wild,(l,annot)) -> P_aux (P_id (fresh_id pre l),(l,annot)) + | (p,annot) -> P_aux (p,annot) } + pat + +(* Check if one pattern subsumes the other, and if so, calculate a + substitution of variables that are used in the same position. + TODO: Check somewhere that there are no variable clashes (the same variable + name used in different positions of the patterns) + *) +let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = + let rewrap p = P_aux (p,annot1) in + let subsumes_list s pats1 pats2 = + if List.length pats1 = List.length pats2 + then + let subs = List.map2 s pats1 pats2 in + List.fold_right + (fun p acc -> match p, acc with + | Some subst, Some substs -> Some (subst @ substs) + | _ -> None) + subs (Some []) + else None in + match p1, p2 with + | P_lit (L_aux (lit1,_)), P_lit (L_aux (lit2,_)) -> + if lit1 = lit2 then Some [] else None + | P_as (pat1,_), _ -> subsumes_pat pat1 pat2 + | _, P_as (pat2,_) -> subsumes_pat pat1 pat2 + | P_typ (_,pat1), _ -> subsumes_pat pat1 pat2 + | _, P_typ (_,pat2) -> subsumes_pat pat1 pat2 + | P_id (Id_aux (id1,_) as aid1), P_id (Id_aux (id2,_) as aid2) -> + if id1 = id2 then Some [] + else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound && + Env.lookup_id aid2 (env_of_annot annot2) = Unbound + then Some [(id2,id1)] else None + | P_id id1, _ -> + if Env.lookup_id id1 (env_of_annot annot1) = Unbound then Some [] else None + | P_wild, _ -> Some [] + | P_app (Id_aux (id1,l1),args1), P_app (Id_aux (id2,_),args2) -> + if id1 = id2 then subsumes_list subsumes_pat args1 args2 else None + | P_record (fps1,b1), P_record (fps2,b2) -> + if b1 = b2 then subsumes_list subsumes_fpat fps1 fps2 else None + | P_vector pats1, P_vector pats2 + | P_vector_concat pats1, P_vector_concat pats2 + | P_tup pats1, P_tup pats2 + | P_list pats1, P_list pats2 -> + subsumes_list subsumes_pat pats1 pats2 + | P_vector_indexed ips1, P_vector_indexed ips2 -> + let (is1,ps1) = List.split ips1 in + let (is2,ps2) = List.split ips2 in + if is1 = is2 then subsumes_list subsumes_pat ps1 ps2 else None + | _ -> None +and subsumes_fpat (FP_aux (FP_Fpat (id1,pat1),_)) (FP_aux (FP_Fpat (id2,pat2),_)) = + if id1 = id2 then subsumes_pat pat1 pat2 else None + +let equiv_pats pat1 pat2 = + match subsumes_pat pat1 pat2, subsumes_pat pat2 pat1 with + | Some _, Some _ -> true + | _, _ -> false + +let subst_id_pat pat (id1,id2) = + let p_id (Id_aux (id,l)) = (if id = id1 then P_id (Id_aux (id2,l)) else P_id (Id_aux (id,l))) in + fold_pat {id_pat_alg with p_id = p_id} pat + +let subst_id_exp exp (id1,id2) = + (* TODO Don't substitute bound occurrences inside let expressions etc *) + let e_id (Id_aux (id,l)) = (if id = id1 then E_id (Id_aux (id2,l)) else E_id (Id_aux (id,l))) in + fold_exp {id_exp_alg with e_id = e_id} exp + +let rec pat_to_exp (P_aux (pat,(l,annot))) = + let rewrap e = E_aux (e,(l,annot)) in + match pat with + | P_lit lit -> rewrap (E_lit lit) + | P_wild -> raise (Reporting_basic.err_unreachable l + "pat_to_exp given wildcard pattern") + | P_as (pat,id) -> rewrap (E_id id) + | P_typ (_,pat) -> pat_to_exp pat + | 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)))) + | P_vector pats -> rewrap (E_vector (List.map pat_to_exp pats)) + | P_vector_concat pats -> raise (Reporting_basic.err_unreachable l + "pat_to_exp not implemented for P_vector_concat") + (* We assume that vector concatenation patterns have been transformed + away already *) + | P_tup pats -> rewrap (E_tuple (List.map pat_to_exp pats)) + | P_list pats -> rewrap (E_list (List.map pat_to_exp pats)) + | P_vector_indexed ipats -> raise (Reporting_basic.err_unreachable l + "pat_to_exp not implemented for P_vector_indexed") (* TODO *) +and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) = + FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot)) + +let case_exp e t cs = + let pexp (pat,body,annot) = Pat_aux (Pat_exp (pat,body),annot) in + let ps = List.map pexp cs in + (* let efr = union_effs (List.map effect_of_pexp ps) in *) + fix_eff_exp (E_aux (E_case (e,ps), (get_loc_exp e, Some (env_of e, t, no_effect)))) + +let rewrite_guarded_clauses l cs = + let rec group clauses = + let add_clause (pat,cls,annot) c = (pat,cls @ [c],annot) in + let rec group_aux current acc = (function + | ((pat,guard,body,annot) as c) :: cs -> + let (current_pat,_,_) = current in + (match subsumes_pat current_pat pat with + | Some substs -> + let pat' = List.fold_left subst_id_pat pat substs in + let guard' = (match guard with + | Some exp -> Some (List.fold_left subst_id_exp exp substs) + | None -> None) in + let body' = List.fold_left subst_id_exp body substs in + let c' = (pat',guard',body',annot) in + group_aux (add_clause current c') acc cs + | None -> + let pat = remove_wildcards "g__" pat in + group_aux (pat,[c],annot) (acc @ [current]) cs) + | [] -> acc @ [current]) in + let groups = match clauses with + | ((pat,guard,body,annot) as c) :: cs -> + group_aux (remove_wildcards "g__" pat, [c], annot) [] cs + | _ -> + raise (Reporting_basic.err_unreachable l + "group given empty list in rewrite_guarded_clauses") in + List.map (fun cs -> if_pexp cs) groups + and if_pexp (pat,cs,annot) = (match cs with + | c :: _ -> + (* fix_eff_pexp (pexp *) + let body = if_exp pat cs in + let pexp = fix_eff_pexp (Pat_aux (Pat_exp (pat,body),annot)) in + let (Pat_aux (Pat_exp (_,_),annot)) = pexp in + (pat, body, annot) + | [] -> + raise (Reporting_basic.err_unreachable l + "if_pexp given empty list in rewrite_guarded_clauses")) + and if_exp current_pat = (function + | (pat,guard,body,annot) :: ((pat',guard',body',annot') as c') :: cs -> + (match guard with + | Some exp -> + let else_exp = + if equiv_pats current_pat pat' + then if_exp current_pat (c' :: cs) + else case_exp (pat_to_exp current_pat) (typ_of body') (group (c' :: cs)) in + fix_eff_exp (E_aux (E_if (exp,body,else_exp), simple_annot (fst annot) (typ_of body))) + | None -> body) + | [(pat,guard,body,annot)] -> body + | [] -> + raise (Reporting_basic.err_unreachable l + "if_exp given empty list in rewrite_guarded_clauses")) in + group cs + +let rewrite_exp_remove_bitvector_pat rewriters (E_aux (exp,(l,annot)) as full_exp) = + let rewrap e = E_aux (e,(l,annot)) in + let rewrite_rec = rewriters.rewrite_exp rewriters in + let rewrite_base = rewrite_exp rewriters in + match exp with + | E_case (e,ps) + when List.exists (fun (Pat_aux (Pat_exp (pat,_),_)) -> contains_bitvector_pat pat) ps -> + let clause (Pat_aux (Pat_exp (pat,body),annot')) = + let (pat',(guard,decls,_)) = remove_bitvector_pat pat in + let body' = decls (rewrite_rec body) in + (pat',guard,body',annot') in + let clauses = rewrite_guarded_clauses l (List.map clause ps) in + 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,eannot) in + let exp_e' = pat_to_exp pat_e' in + (* let fresh = fresh_id "p__" el in + let exp_e' = E_aux (E_id fresh, gen_annot l (get_type e) pure_e) in + let pat_e' = P_aux (P_id fresh, gen_annot l (get_type e) pure_e) in *) + let letbind_e = LB_aux (LB_val_implicit (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 + | 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) -> + let (pat,(_,decls,_)) = remove_bitvector_pat pat in + rewrap (E_let (LB_aux (LB_val_implicit (pat,rewrite_rec v),annot'), + decls (rewrite_rec body))) + | _ -> rewrite_base full_exp + +let rewrite_fun_remove_bitvector_pat + rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = + let _ = reset_fresh_name_counter () in + (* TODO Can there be clauses with different id's in one FD_function? *) + let funcls = match funcls with + | (FCL_aux (FCL_Funcl(id,_,_),_) :: _) -> + let clause (FCL_aux (FCL_Funcl(_,pat,exp),annot)) = + let (pat,(guard,decls,_)) = remove_bitvector_pat pat in + let exp = decls (rewriters.rewrite_exp rewriters exp) in + (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,pat,exp),annot)) cs + | _ -> funcls (* TODO is the empty list possible here? *) in + FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot)) + +let rewrite_defs_remove_bitvector_pats (Defs defs) = + let rewriters = + {rewrite_exp = rewrite_exp_remove_bitvector_pat; rewrite_pat = rewrite_pat; rewrite_let = rewrite_let; rewrite_lexp = rewrite_lexp; - rewrite_fun = rewrite_fun_remove_vector_concat_pat; + rewrite_fun = rewrite_fun_remove_bitvector_pat; rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_remove_vector_concat_pat} defs - + rewrite_defs = rewrite_defs_base } in + 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)) -> + 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 + | d -> [d] in + Defs (List.flatten (List.map rewrite_def defs)) + + (*Expects to be called after rewrite_defs; thus the following should not appear: internal_exp of any form lit vectors in patterns or expressions *) -let rewrite_exp_lift_assign_intro rewriters nmap ((E_aux (exp,(l,annot))) as full_exp) = - let rewrap e = E_aux (e,(l,annot)) in - let rewrap_effects e effsum = - let (Base (t,tag,nexps,eff,_,bounds)) = annot in - E_aux (e,(l,Base (t,tag,nexps,eff,effsum,bounds))) in - let rewrite_rec = rewriters.rewrite_exp rewriters nmap in - let rewrite_base = rewrite_exp rewriters nmap in +let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as full_exp) = + let rewrap e = E_aux (e,annot) in + let rewrap_effects e eff = + E_aux (e, (l,Some (env_of_annot annot, typ_of_annot annot, eff))) in + let rewrite_rec = rewriters.rewrite_exp rewriters in + let rewrite_base = rewrite_exp rewriters in match exp with | E_block exps -> let rec walker exps = match exps with | [] -> [] - | (E_aux(E_assign(le,e), (l, Base((_,t),Emp_intro,_,_,_,_))))::exps -> - let le' = rewriters.rewrite_lexp rewriters nmap le in - let e' = rewrite_base e in - let exps' = walker exps in - let effects = eff_union_exps exps' in - [E_aux (E_internal_let(le', e', E_aux(E_block exps', (l, simple_annot_efr {t=Tid "unit"} effects))), - (l, simple_annot_efr t (eff_union_exps (e::exps'))))] - | ((E_aux(E_if(c,t,e),(l,annot))) as exp)::exps -> + | (E_aux(E_assign((LEXP_aux ((LEXP_id id | LEXP_cast (_,id)),_)) as le,e), + ((l, Some (env,typ,eff)) as annot)) as exp)::exps -> + (match Env.lookup_id id env with + | Unbound -> + let le' = rewriters.rewrite_lexp rewriters le in + let e' = 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_internal_let(le', e', block), annot))] + | _ -> (rewrite_rec exp)::(walker exps)) + (*| ((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 let new_vars = Envmap.intersect vars_t vars_e in @@ -1249,43 +1957,34 @@ let rewrite_exp_lift_assign_intro rewriters nmap ((E_aux (exp,(l,annot))) as ful set_exp, E_aux (E_block res, (Parse_ast.Generated l, (simple_annot_efr unit_t effects)))), (Parse_ast.Generated l, simple_annot_efr unit_t unioneffs))],unioneffs))) - (E_aux(E_if(c',t',e'),(Parse_ast.Generated l, annot))::exps',eff_union_exps (c'::t'::e'::exps')) new_vars) + (E_aux(E_if(c',t',e'),(Parse_ast.Generated l, annot))::exps',eff_union_exps (c'::t'::e'::exps')) new_vars)*) | e::exps -> (rewrite_rec e)::(walker exps) in rewrap (E_block (walker exps)) - | E_assign(le,e) -> - (match annot with - | Base((_,t),Emp_intro,_,_,_,_) -> - let le' = rewriters.rewrite_lexp rewriters nmap le in - let e' = rewrite_base e in - let effects = get_effsum_exp e' in - (match le' with - | LEXP_aux(_, (_,Base(_,Emp_intro,_,_,_,_))) -> - rewrap_effects - (E_internal_let(le', e', E_aux(E_block [], (l, simple_annot_efr unit_t effects)))) - effects - | LEXP_aux(_, (_,Base(_,_,_,_,efr,_))) -> - let effects' = union_effects effects efr in - E_aux((E_assign(le', e')),(l, tag_annot_efr unit_t Emp_set effects')) - | _ -> assert false) + | E_assign(((LEXP_aux ((LEXP_id id | LEXP_cast (_,id)),lannot)) as le),e) -> + let le' = rewriters.rewrite_lexp rewriters le in + let e' = rewrite_base e in + let effects = effect_of e' in + (match Env.lookup_id id (env_of_annot annot) with + | Unbound -> + rewrap_effects + (E_internal_let(le', e', E_aux(E_block [], simple_annot l unit_typ))) + effects + | Local _ -> + let effects' = union_effects effects (effect_of_annot (snd lannot)) in + let annot' = Some (env_of_annot annot, unit_typ, effects') in + E_aux((E_assign(le', e')),(l, annot')) | _ -> rewrite_base full_exp) | _ -> rewrite_base full_exp -let rewrite_lexp_lift_assign_intro rewriters map ((LEXP_aux(lexp,(l,annot))) as le) = - let rewrap le = LEXP_aux(le,(l,annot)) in - let rewrite_base = rewrite_lexp rewriters map in - match lexp with - | LEXP_id (Id_aux (Id i, _)) | LEXP_cast (_,(Id_aux (Id i,_))) -> - (match annot with - | Base((p,t),Emp_intro,cs,e1,e2,bs) -> - (match map with - | Some(_,s) -> - (match Envmap.apply s i with - | None -> rewrap lexp - | Some _ -> - let ls = BE_aux(BE_lset,l) in - LEXP_aux(lexp,(l,(Base((p,t),Emp_set,cs,add_effect ls e1, add_effect ls e2,bs))))) - | _ -> rewrap lexp) +let rewrite_lexp_lift_assign_intro rewriters ((LEXP_aux(lexp,annot)) as le) = + let rewrap le = LEXP_aux(le,annot) in + let rewrite_base = rewrite_lexp rewriters in + match lexp, annot with + | (LEXP_id id | LEXP_cast (_,id)), (l, Some (env, typ, eff)) -> + (match Env.lookup_id id env with + | Unbound | Local _ -> + LEXP_aux (lexp, (l, Some (env, typ, union_effects eff (mk_effect [BE_lset])))) | _ -> rewrap lexp) | _ -> rewrite_base le @@ -1298,16 +1997,16 @@ let rewrite_defs_exp_lift_assign defs = rewrite_defs_base rewrite_fun = rewrite_fun; rewrite_def = rewrite_def; rewrite_defs = rewrite_defs_base} defs - -let rewrite_exp_separate_ints rewriters nmap ((E_aux (exp,(l,annot))) as full_exp) = - let tparms,t,tag,nexps,eff,cum_eff,bounds = match annot with + +(*let rewrite_exp_separate_ints rewriters ((E_aux (exp,((l,_) as annot))) as full_exp) = + (*let tparms,t,tag,nexps,eff,cum_eff,bounds = match annot with | Base((tparms,t),tag,nexps,eff,cum_eff,bounds) -> tparms,t,tag,nexps,eff,cum_eff,bounds - | _ -> [],unit_t,Emp_local,[],pure_e,pure_e,nob in - let rewrap e = E_aux (e,(l,annot)) in - let rewrap_effects e effsum = - E_aux (e,(l,Base ((tparms,t),tag,nexps,eff,effsum,bounds))) in - let rewrite_rec = rewriters.rewrite_exp rewriters nmap in - let rewrite_base = rewrite_exp rewriters nmap in + | _ -> [],unit_t,Emp_local,[],pure_e,pure_e,nob in*) + let rewrap e = E_aux (e,annot) in + (*let rewrap_effects e effsum = + E_aux (e,(l,Base ((tparms,t),tag,nexps,eff,effsum,bounds))) in*) + let rewrite_rec = rewriters.rewrite_exp rewriters in + let rewrite_base = rewrite_exp rewriters in match exp with | E_lit (L_aux (((L_num _) as lit),_)) -> (match (is_within_machine64 t nexps) with @@ -1344,25 +2043,25 @@ let rewrite_defs_separate_numbs defs = rewrite_defs_base rewrite_lexp = rewrite_lexp; (*will likely need a new one?*) rewrite_fun = rewrite_fun; rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_base} defs + rewrite_defs = rewrite_defs_base} defs*) -let rewrite_defs_ocaml defs = - let defs_sorted = top_sort_defs defs in - let defs_vec_concat_removed = rewrite_defs_remove_vector_concat defs_sorted in - let defs_lifted_assign = rewrite_defs_exp_lift_assign defs_vec_concat_removed in -(* let defs_separate_nums = rewrite_defs_separate_numbs defs_lifted_assign in *) - defs_lifted_assign +let rewrite_defs_ocaml = + top_sort_defs >> + rewrite_defs_remove_vector_concat >> + rewrite_sizeof >> + rewrite_defs_exp_lift_assign (* >> + rewrite_defs_separate_numbs *) let rewrite_defs_remove_blocks = let letbind_wild v body = - let (E_aux (_,(l,_))) = v in - let annot_pat = (Parse_ast.Generated l,simple_annot (get_type v)) in - let annot_lb = (Parse_ast.Generated l,simple_annot_efr (get_type v) (get_effsum_exp v)) in - let annot_let = (Parse_ast.Generated l,simple_annot_efr (get_type body) (eff_union_exps [v;body])) in + let (E_aux (_,(l,tannot))) = v in + 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 let rec f l = function - | [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)), (Parse_ast.Generated l,simple_annot ({t = Tid "unit"}))) + | [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)), (simple_annot l unit_typ)) | [e] -> e (* check with Kathy if that annotation is fine *) | e :: es -> letbind_wild e (f l es) in @@ -1373,7 +2072,7 @@ let rewrite_defs_remove_blocks = let alg = { id_exp_alg with e_aux = e_aux } in rewrite_defs_base - {rewrite_exp = (fun _ _ -> fold_exp alg) + {rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp @@ -1384,36 +2083,32 @@ let rewrite_defs_remove_blocks = -let fresh_id ((l,_) as annot) = - let current = fresh_name () in - let id = Id_aux (Id ("w__" ^ string_of_int current), Parse_ast.Generated l) in - let annot_var = (Parse_ast.Generated l,simple_annot (get_type_annot annot)) in - E_aux (E_id id, annot_var) - let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp = (* body is a function : E_id variable -> actual body *) - match get_type v with - | {t = Tid "unit"} -> - let (E_aux (_,(l,annot))) = v in - let e = E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(Parse_ast.Generated l,simple_annot unit_t)) in + let (E_aux (_,(l,annot))) = v in + match annot with + | Some (env, Typ_aux (Typ_id tid, _), eff) when string_of_id tid = "unit" -> + let e = E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(simple_annot l unit_typ)) in let body = body e in - let annot_pat = (Parse_ast.Generated l,simple_annot unit_t) in + let annot_pat = simple_annot l unit_typ in let annot_lb = annot_pat in - let annot_let = (Parse_ast.Generated l,simple_annot_efr (get_type body) (eff_union_exps [v;body])) in + 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) - | _ -> - let (E_aux (_,((l,_) as annot))) = v in - let ((E_aux (E_id id,_)) as e_id) = fresh_id annot in + | Some (env, typ, eff) -> + let id = fresh_id "w__" l in + let annot_pat = simple_annot l (typ_of v) in + let e_id = E_aux (E_id id, (Parse_ast.Generated l, Some (env, typ, no_effect))) in let body = body e_id in - - let annot_pat = (Parse_ast.Generated l,simple_annot (get_type v)) in + let annot_lb = annot_pat in - let annot_let = (Parse_ast.Generated l,simple_annot_efr (get_type body) (eff_union_exps [v;body])) in + 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) + | None -> + raise (Reporting_basic.err_unreachable l "no type information") let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list -> 'a exp) : 'a exp = @@ -1424,7 +2119,7 @@ let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list let rewrite_defs_letbind_effects = let rec value ((E_aux (exp_aux,_)) as exp) = - not (effectful exp) && not (updates_vars exp) + not (effectful exp || updates_vars exp) and value_optdefault (Def_val_aux (o,_)) = match o with | Def_val_empty -> true | Def_val_dec e -> value e @@ -1436,7 +2131,7 @@ let rewrite_defs_letbind_effects = n_exp exp (fun exp -> if value exp then k exp else letbind exp k) and n_exp_pure (exp : 'a exp) (k : 'a exp -> 'a exp) : 'a exp = - n_exp exp (fun exp -> if not (effectful exp || updates_vars exp) then k exp else letbind exp k) + n_exp exp (fun exp -> if value exp then k exp else letbind exp k) and n_exp_nameL (exps : 'a exp list) (k : 'a exp list -> 'a exp) : 'a exp = mapCont n_exp_name exps k @@ -1444,14 +2139,14 @@ let rewrite_defs_letbind_effects = and n_fexp (fexp : 'a fexp) (k : 'a fexp -> 'a exp) : 'a exp = let (FE_aux (FE_Fexp (id,exp),annot)) = fexp in n_exp_name exp (fun exp -> - k (fix_effsum_fexp (FE_aux (FE_Fexp (id,exp),annot)))) + k (fix_eff_fexp (FE_aux (FE_Fexp (id,exp),annot)))) and n_fexpL (fexps : 'a fexp list) (k : 'a fexp list -> 'a exp) : 'a exp = mapCont n_fexp fexps k and n_pexp (newreturn : bool) (pexp : 'a pexp) (k : 'a pexp -> 'a exp) : 'a exp = let (Pat_aux (Pat_exp (pat,exp),annot)) = pexp in - k (fix_effsum_pexp (Pat_aux (Pat_exp (pat,n_exp_term newreturn exp), annot))) + k (fix_eff_pexp (Pat_aux (Pat_exp (pat,n_exp_term newreturn exp), annot))) and n_pexpL (newreturn : bool) (pexps : 'a pexp list) (k : 'a pexp list -> 'a exp) : 'a exp = mapCont (n_pexp newreturn) pexps k @@ -1459,7 +2154,7 @@ let rewrite_defs_letbind_effects = 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_effsum_fexps (FES_aux (FES_Fexps (fexps_aux,b),annot)))) + 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 @@ -1467,17 +2162,17 @@ let rewrite_defs_letbind_effects = | Def_val_empty -> k (Def_val_aux (Def_val_empty,annot)) | Def_val_dec exp -> n_exp_name exp (fun exp -> - k (fix_effsum_opt_default (Def_val_aux (Def_val_dec exp,annot)))) + k (fix_eff_opt_default (Def_val_aux (Def_val_dec exp,annot)))) 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_effsum_lb (LB_aux (LB_val_explicit (typ,pat,exp1),annot)))) + k (fix_eff_lb (LB_aux (LB_val_explicit (typ,pat,exp1),annot)))) | LB_val_implicit (pat,exp1) -> n_exp exp1 (fun exp1 -> - k (fix_effsum_lb (LB_aux (LB_val_implicit (pat,exp1),annot)))) + k (fix_eff_lb (LB_aux (LB_val_implicit (pat,exp1),annot)))) and n_lexp (lexp : 'a lexp) (k : 'a lexp -> 'a exp) : 'a exp = let (LEXP_aux (lexp_aux,annot)) = lexp in @@ -1485,27 +2180,28 @@ let rewrite_defs_letbind_effects = | LEXP_id _ -> k lexp | LEXP_memory (id,es) -> n_exp_nameL es (fun es -> - k (fix_effsum_lexp (LEXP_aux (LEXP_memory (id,es),annot)))) + k (fix_eff_lexp (LEXP_aux (LEXP_memory (id,es),annot)))) | LEXP_cast (typ,id) -> - k (fix_effsum_lexp (LEXP_aux (LEXP_cast (typ,id),annot))) + k (fix_eff_lexp (LEXP_aux (LEXP_cast (typ,id),annot))) | LEXP_vector (lexp,e) -> n_lexp lexp (fun lexp -> n_exp_name e (fun e -> - k (fix_effsum_lexp (LEXP_aux (LEXP_vector (lexp,e),annot))))) + k (fix_eff_lexp (LEXP_aux (LEXP_vector (lexp,e),annot))))) | LEXP_vector_range (lexp,e1,e2) -> n_lexp lexp (fun lexp -> n_exp_name e1 (fun e1 -> n_exp_name e2 (fun e2 -> - k (fix_effsum_lexp (LEXP_aux (LEXP_vector_range (lexp,e1,e2),annot)))))) + k (fix_eff_lexp (LEXP_aux (LEXP_vector_range (lexp,e1,e2),annot)))))) | LEXP_field (lexp,id) -> n_lexp lexp (fun lexp -> - k (fix_effsum_lexp (LEXP_aux (LEXP_field (lexp,id),annot)))) + k (fix_eff_lexp (LEXP_aux (LEXP_field (lexp,id),annot)))) and n_exp_term (newreturn : bool) (exp : 'a exp) : 'a exp = - let (E_aux (_,(l,_))) = exp in + let (E_aux (_,(l,tannot))) = exp in let exp = if newreturn then - E_aux (E_internal_return exp,(Parse_ast.Generated l,simple_annot_efr (get_type exp) (get_effsum_exp exp))) + let typ = typ_of exp in + E_aux (E_internal_return exp, simple_annot l typ) else exp in (* n_exp_term forces an expression to be translated into a form @@ -1515,7 +2211,7 @@ let rewrite_defs_letbind_effects = and n_exp (E_aux (exp_aux,annot) as exp : 'a exp) (k : 'a exp -> 'a exp) : 'a exp = - let rewrap e = fix_effsum_exp (E_aux (e,annot)) in + let rewrap e = fix_eff_exp (E_aux (e,annot)) in match exp_aux with | E_block es -> failwith "E_block should have been removed till now" @@ -1602,7 +2298,7 @@ let rewrite_defs_letbind_effects = | E_case (exp1,pexps) -> let newreturn = List.fold_left - (fun b (Pat_aux (_,(_,Base (_,_,_,_,effs,_)))) -> b || effectful_effs effs) + (fun b (Pat_aux (_,(_,annot))) -> b || effectful_effs (effect_of_annot annot)) false pexps in n_exp_name exp1 (fun exp1 -> n_pexpL newreturn pexps (fun pexps -> @@ -1648,8 +2344,8 @@ let rewrite_defs_letbind_effects = let rewrite_fun _ (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),fdannot)) = let newreturn = List.fold_left - (fun b (FCL_aux (FCL_Funcl(id,pat,exp),annot)) -> - b || effectful_effs (get_localeff_annot annot)) false funcls in + (fun b (FCL_aux (FCL_Funcl(id,pat,exp),(_,annot))) -> + b || effectful_effs (effect_of_annot annot)) false funcls in let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),annot)) = let _ = reset_fresh_name_counter () in FCL_aux (FCL_Funcl (id,pat,n_exp_term newreturn exp),annot) @@ -1685,7 +2381,7 @@ let rewrite_defs_effectful_let_expressions = let alg = { id_exp_alg with e_let = e_let; e_internal_let = e_internal_let } in rewrite_defs_base - {rewrite_exp = (fun _ _ -> fold_exp alg) + {rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp @@ -1742,6 +2438,7 @@ let find_updated_vars exp = ; e_case = (fun (e1,pexps) -> e1 @@ lapp2 pexps) ; e_let = (fun (lb,e2) -> lb @@ e2) ; e_assign = (fun ((ids,acc),e2) -> ([],ids) @@ acc @@ e2) + ; e_sizeof = (fun nexp -> ([],[])) ; e_exit = (fun e1 -> ([],[])) ; e_return = (fun e1 -> e1) ; e_assert = (fun (e1,e2) -> ([],[])) @@ -1764,8 +2461,10 @@ let find_updated_vars exp = ; lEXP_field = (fun ((ids,acc),_) -> (None,ids,acc)) ; lEXP_aux = (function - | ((Some id,ids,acc),((_,Base (_,(Emp_set | Emp_intro),_,_,_,_)) as annot)) -> - ((id,annot) :: ids,acc) + | ((Some id,ids,acc),(annot)) -> + (match Env.lookup_id id (env_of_annot annot) with + | Unbound | Local _ -> ((id,annot) :: ids,acc) + | _ -> (ids,acc)) | ((_,ids,acc),_) -> (ids,acc) ) ; fE_Fexp = (fun (_,e) -> e) @@ -1784,29 +2483,33 @@ let find_updated_vars exp = } exp in dedup eqidtyp updates -let swaptyp t (l,(Base ((t_params,_),tag,nexps,eff,effsum,bounds))) = - (l,Base ((t_params,t),tag,nexps,eff,effsum,bounds)) +let swaptyp typ (l,tannot) = match tannot with + | Some (env, typ', eff) -> (l, Some (env, typ, eff)) + | _ -> raise (Reporting_basic.err_unreachable l "swaptyp called with empty type annotation") let mktup l es = match es with - | [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(Parse_ast.Generated l,simple_annot unit_t)) + | [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(simple_annot l unit_typ)) | [e] -> e - | _ -> + | e :: _ -> let effs = - List.fold_left (fun acc e -> union_effects acc (get_effsum_exp e)) {effect = Eset []} es in - let typs = List.map get_type es in - E_aux (E_tuple es,(Parse_ast.Generated l,simple_annot_efr {t = Ttup typs} effs)) + List.fold_left (fun acc e -> union_effects acc (effect_of e)) no_effect es in + let typ = mk_typ (Typ_tup (List.map typ_of es)) in + E_aux (E_tuple es,(Parse_ast.Generated l, Some (env_of e, typ, effs))) let mktup_pat l es = match es with - | [] -> P_aux (P_wild,(Parse_ast.Generated l,simple_annot unit_t)) + | [] -> P_aux (P_wild,(simple_annot l unit_typ)) | [E_aux (E_id id,_) as exp] -> - P_aux (P_id id,(Parse_ast.Generated l,simple_annot (get_type exp))) + P_aux (P_id id,(simple_annot l (typ_of exp))) | _ -> - let typs = List.map get_type es in - let pats = List.map (fun (E_aux (E_id id,_) as exp) -> - P_aux (P_id id,(Parse_ast.Generated l,simple_annot (get_type exp)))) es in - P_aux (P_tup pats,(Parse_ast.Generated l,simple_annot {t = Ttup typs})) + let typ = mk_typ (Typ_tup (List.map typ_of es)) in + let pats = List.map (function + | (E_aux (E_id id,_) as exp) -> + P_aux (P_id id,(simple_annot l (typ_of exp))) + | exp -> + P_aux (P_wild,(simple_annot l (typ_of exp)))) es in + P_aux (P_tup pats,(simple_annot l typ)) type 'a updated_term = @@ -1819,36 +2522,48 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = match expaux with | E_let (lb,exp) -> let exp = add_vars overwrite exp vars in - E_aux (E_let (lb,exp),swaptyp (get_type exp) annot) + E_aux (E_let (lb,exp),swaptyp (typ_of exp) annot) | E_internal_let (lexp,exp1,exp2) -> let exp2 = add_vars overwrite exp2 vars in - E_aux (E_internal_let (lexp,exp1,exp2), swaptyp (get_type exp2) annot) + E_aux (E_internal_let (lexp,exp1,exp2), swaptyp (typ_of exp2) annot) | E_internal_plet (pat,exp1,exp2) -> let exp2 = add_vars overwrite exp2 vars in - E_aux (E_internal_plet (pat,exp1,exp2), swaptyp (get_type exp2) annot) + E_aux (E_internal_plet (pat,exp1,exp2), swaptyp (typ_of exp2) annot) | E_internal_return exp2 -> let exp2 = add_vars overwrite exp2 vars in - E_aux (E_internal_return exp2,swaptyp (get_type exp2) annot) + E_aux (E_internal_return exp2,swaptyp (typ_of exp2) annot) | _ -> (* after rewrite_defs_letbind_effects there cannot be terms that have effects/update local variables in "tail-position": check n_exp_term and where it is used. *) if overwrite then - let () = if get_type exp = {t = Tid "unit"} then () - else failwith "nono" in - vars + match typ_of exp with + | Typ_aux (Typ_id (Id_aux (Id "unit", _)), _) -> vars + | _ -> raise (Reporting_basic.err_unreachable l + "add_vars: trying to overwrite a non-unit expression in tail-position") else - E_aux (E_tuple [exp;vars],swaptyp {t = Ttup [get_type exp;get_type vars]} annot) in + let typ' = Typ_aux (Typ_tup [typ_of exp;typ_of vars], Parse_ast.Generated l) in + E_aux (E_tuple [exp;vars],swaptyp typ' annot) in let rewrite (E_aux (expaux,((el,_) as annot))) (P_aux (_,(pl,pannot)) as pat) = - let overwrite = match get_type_annot annot with - | {t = Tid "unit"} -> true + let overwrite = match typ_of_annot annot with + | Typ_aux (Typ_id (Id_aux (Id "unit", _)), _) -> true | _ -> false in match expaux with | E_for(id,exp1,exp2,exp3,order,exp4) -> + (* Translate for loops into calls to one of the foreach combinators. + The loop body becomes a function of the loop variable and any + mutable local variables that are updated inside the loop. + Since the foreach* combinators are higher-order functions, + they cannot be represented faithfully in the AST. The following + code abuses the parameters of an E_app node, embedding the loop body + function as an expression followed by the list of variables it + expects. In (Lem) pretty-printing, this turned into an anonymous + function and passed to foreach*. *) let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (find_updated_vars exp4) in let vartuple = mktup el vars in let exp4 = rewrite_var_updates (add_vars overwrite exp4 vartuple) in + let (E_aux (_,(_,annot4))) = exp4 in let fname = match effectful exp4,order with | false, Ord_aux (Ord_inc,_) -> "foreach_inc" | false, Ord_aux (Ord_dec,_) -> "foreach_dec" @@ -1856,13 +2571,15 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | true, Ord_aux (Ord_dec,_) -> "foreachM_dec" in let funcl = Id_aux (Id fname,Parse_ast.Generated el) in let loopvar = - let (bf,tf) = match get_type exp1 with + (* Don't bother with creating a range type annotation, since the + Lem pretty-printing does not use it. *) + (* let (bf,tf) = match typ_of exp1 with | {t = Tapp ("atom",[TA_nexp f])} -> (TA_nexp f,TA_nexp f) | {t = Tapp ("reg", [TA_typ {t = Tapp ("atom",[TA_nexp f])}])} -> (TA_nexp f,TA_nexp f) | {t = Tapp ("range",[TA_nexp bf;TA_nexp tf])} -> (TA_nexp bf,TA_nexp tf) | {t = Tapp ("reg", [TA_typ {t = Tapp ("range",[TA_nexp bf;TA_nexp tf])}])} -> (TA_nexp bf,TA_nexp tf) | {t = Tapp (name,_)} -> failwith (name ^ " shouldn't be here") in - let (bt,tt) = match get_type exp2 with + let (bt,tt) = match typ_of exp2 with | {t = Tapp ("atom",[TA_nexp t])} -> (TA_nexp t,TA_nexp t) | {t = Tapp ("atom",[TA_typ {t = Tapp ("atom", [TA_nexp t])}])} -> (TA_nexp t,TA_nexp t) | {t = Tapp ("range",[TA_nexp bt;TA_nexp tt])} -> (TA_nexp bt,TA_nexp tt) @@ -1870,14 +2587,14 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | {t = Tapp (name,_)} -> failwith (name ^ " shouldn't be here") in let t = {t = Tapp ("range",match order with | Ord_aux (Ord_inc,_) -> [bf;tt] - | Ord_aux (Ord_dec,_) -> [tf;bt])} in - E_aux (E_id id,(Parse_ast.Generated el,simple_annot t)) in + | Ord_aux (Ord_dec,_) -> [tf;bt])} in *) + E_aux (E_id id, simple_annot l int_typ) in let v = E_aux (E_app (funcl,[loopvar;mktup el [exp1;exp2;exp3];exp4;vartuple]), - (Parse_ast.Generated el,simple_annot_efr (get_type exp4) (get_effsum_exp exp4))) in + (Parse_ast.Generated el, annot4)) in let pat = if overwrite then mktup_pat el vars else P_aux (P_tup [pat; mktup_pat pl vars], - (Parse_ast.Generated pl,simple_annot (get_type v))) in + simple_annot pl (typ_of v)) in Added_vars (v,pat) | E_if (c,e1,e2) -> let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) @@ -1889,12 +2606,14 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let e1 = rewrite_var_updates (add_vars overwrite e1 vartuple) in let e2 = rewrite_var_updates (add_vars overwrite e2 vartuple) in (* after rewrite_defs_letbind_effects c has no variable updates *) - let t = get_type e1 in - let v = E_aux (E_if (c,e1,e2), (Parse_ast.Generated el,simple_annot_efr t (eff_union_exps [e1;e2]))) in + let env = env_of_annot annot in + let typ = typ_of e1 in + let eff = union_eff_exps [e1;e2] in + let v = E_aux (E_if (c,e1,e2), (Parse_ast.Generated el, Some (env, typ, eff))) in let pat = if overwrite then mktup_pat el vars else P_aux (P_tup [pat; mktup_pat pl vars], - (Parse_ast.Generated pl,simple_annot (get_type v))) in + (simple_annot pl (typ_of v))) in Added_vars (v,pat) | E_case (e1,ps) -> (* after rewrite_defs_letbind_effects e1 needs no rewriting *) @@ -1909,48 +2628,53 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let vartuple = mktup el vars in let typ = let (Pat_aux (Pat_exp (_,first),_)) = List.hd ps in - get_type first in + typ_of first in let (ps,typ,effs) = let f (acc,typ,effs) (Pat_aux (Pat_exp (p,e),pannot)) = - let etyp = get_type e in - let () = assert (simple_annot etyp = simple_annot typ) in + let etyp = typ_of e in + let () = assert (string_of_typ etyp = string_of_typ typ) in let e = rewrite_var_updates (add_vars overwrite e vartuple) in - let pannot = (Parse_ast.Generated pl,simple_annot (get_type e)) in - let effs = union_effects effs (get_effsum_exp e) in + let pannot = simple_annot pl (typ_of e) in + let effs = union_effects effs (effect_of e) in let pat' = Pat_aux (Pat_exp (p,e),pannot) in (acc @ [pat'],typ,effs) in - List.fold_left f ([],typ,{effect = Eset []}) ps in - let v = E_aux (E_case (e1,ps), (Parse_ast.Generated pl,simple_annot_efr typ effs)) in + List.fold_left f ([],typ,no_effect) ps in + let v = E_aux (E_case (e1,ps), (Parse_ast.Generated pl, Some (env_of_annot annot, typ, effs))) in let pat = if overwrite then mktup_pat el vars else P_aux (P_tup [pat; mktup_pat pl vars], - (Parse_ast.Generated pl,simple_annot (get_type v))) in + (simple_annot pl (typ_of v))) in Added_vars (v,pat) | E_assign (lexp,vexp) -> - let {effect = Eset effs} = get_effsum_annot annot in + let effs = match effect_of_annot (snd annot) with + | Effect_aux (Effect_set effs, _) -> effs + | _ -> + raise (Reporting_basic.err_unreachable l + "assignment without effects annotation") in if not (List.exists (function BE_aux (BE_lset,_) -> true | _ -> false) effs) then Same_vars (E_aux (E_assign (lexp,vexp),annot)) else (match lexp with | LEXP_aux (LEXP_id id,annot) -> - let pat = P_aux (P_id id,(Parse_ast.Generated pl,simple_annot (get_type vexp))) in + let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in Added_vars (vexp,pat) | LEXP_aux (LEXP_cast (_,id),annot) -> - let pat = P_aux (P_id id,(Parse_ast.Generated pl,simple_annot (get_type vexp))) in + let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in Added_vars (vexp,pat) | LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i),((l1,_) as annot)) -> - let eid = E_aux (E_id id,(Parse_ast.Generated l2,simple_annot (get_type_annot annot2))) in + let eid = E_aux (E_id id, simple_annot l2 (typ_of_annot annot2)) in let vexp = E_aux (E_vector_update (eid,i,vexp), - (Parse_ast.Generated l1,simple_annot (get_type_annot annot))) in - let pat = P_aux (P_id id,(Parse_ast.Generated pl,simple_annot (get_type vexp))) in + simple_annot l1 (typ_of_annot annot)) in + let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in Added_vars (vexp,pat) | LEXP_aux (LEXP_vector_range (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i,j), ((l,_) as annot)) -> - let eid = E_aux (E_id id,(Parse_ast.Generated l2,simple_annot (get_type_annot annot2))) in + let eid = E_aux (E_id id, simple_annot l2 (typ_of_annot annot2)) in let vexp = E_aux (E_vector_update_subrange (eid,i,j,vexp), - (Parse_ast.Generated l,simple_annot (get_type_annot annot))) in - let pat = P_aux (P_id id,(Parse_ast.Generated pl,simple_annot (get_type vexp))) in - Added_vars (vexp,pat)) + simple_annot l (typ_of_annot annot)) in + let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in + Added_vars (vexp,pat) + | _ -> Same_vars (E_aux (E_assign (lexp,vexp),annot))) | _ -> (* after rewrite_defs_letbind_effects this expression is pure and updates no variables: check n_exp_term and where it's used. *) @@ -1964,27 +2688,33 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = (match rewrite v pat with | Added_vars (v,pat) -> let (E_aux (_,(l,_))) = v in - let lbannot = (Parse_ast.Generated l,simple_annot (get_type v)) in - (get_effsum_exp v,LB_aux (LB_val_implicit (pat,v),lbannot)) - | Same_vars v -> (get_effsum_exp v,LB_aux (LB_val_implicit (pat,v),lbannot))) + 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 = (Parse_ast.Generated l,simple_annot (get_type v)) in - (get_effsum_exp v,LB_aux (LB_val_implicit (pat,v),lbannot)) - | Same_vars v -> (get_effsum_exp v,LB_aux (LB_val_explicit (typ,pat,v),lbannot))) in - let typ = simple_annot_efr (get_type body) (union_effects eff (get_effsum_exp body)) in - E_aux (E_let (lb,body),(Parse_ast.Generated l,typ)) + 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 + 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) -> (* Rewrite E_internal_let into E_let and call recursively *) let id = match lexp with | LEXP_aux (LEXP_id id,_) -> id | LEXP_aux (LEXP_cast (_,id),_) -> id in - let pat = P_aux (P_id id, (Parse_ast.Generated l,simple_annot (get_type v))) in - let lbannot = (Parse_ast.Generated l,simple_annot_efr (get_type v) (get_effsum_exp v)) in + let env = env_of_annot annot in + let vtyp = typ_of v in + let veff = effect_of v in + let bodyenv = env_of body in + let bodytyp = typ_of body in + 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 exp = E_aux (E_let (lb,body),(Parse_ast.Generated l,simple_annot_efr (get_type body) (eff_union_exps [v;body]))) 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) -> failwith "rewrite_var_updates: E_internal_plet shouldn't be introduced yet" @@ -2003,42 +2733,23 @@ let replace_memwrite_e_assign exp = let remove_reference_types exp = - let rec rewrite_t {t = t_aux} = {t = rewrite_t_aux t_aux} + let rec rewrite_t (Typ_aux (t_aux,a)) = (Typ_aux (rewrite_t_aux t_aux,a)) and rewrite_t_aux t_aux = match t_aux with - | Tapp ("reg",[TA_typ {t = t_aux2}]) -> rewrite_t_aux t_aux2 - | Tapp (name,t_args) -> Tapp (name,List.map rewrite_t_arg t_args) - | Tfn (t1,t2,imp,e) -> Tfn (rewrite_t t1,rewrite_t t2,imp,e) - | Ttup ts -> Ttup (List.map rewrite_t ts) - | Tabbrev (t1,t2) -> Tabbrev (rewrite_t t1,rewrite_t t2) - | Toptions (t1,t2) -> - let t2 = match t2 with Some t2 -> Some (rewrite_t t2) | None -> None in - Toptions (rewrite_t t1,t2) - | Tuvar t_uvar -> Tuvar t_uvar (*(rewrite_t_uvar t_uvar) *) + | Typ_app (Id_aux (Id "reg",_), [Typ_arg_aux (Typ_arg_typ (Typ_aux (t_aux2, _)), _)]) -> + rewrite_t_aux t_aux2 + | Typ_app (name,t_args) -> Typ_app (name,List.map rewrite_t_arg t_args) + | Typ_fn (t1,t2,eff) -> Typ_fn (rewrite_t t1,rewrite_t t2,eff) + | Typ_tup ts -> Typ_tup (List.map rewrite_t ts) | _ -> t_aux -(* and rewrite_t_uvar t_uvar = - t_uvar.subst <- (match t_uvar.subst with None -> None | Some t -> Some (rewrite_t t)) *) and rewrite_t_arg t_arg = match t_arg with - | TA_typ t -> TA_typ (rewrite_t t) + | 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 - | NoTyp -> NoTyp - | Base ((tparams,t),tag,nexprs,effs,effsum,bounds) -> - Base ((tparams,rewrite_t t),tag,nexprs,effs,effsum,bounds) - | Overload (tannot1,b,tannots) -> - Overload (rewrite_annot tannot1,b,List.map rewrite_annot tannots) in - - - fold_exp - { id_exp_alg with - e_aux = (fun (e,(l,annot)) -> E_aux (e,(l,rewrite_annot annot))) - ; lEXP_aux = (fun (lexp,(l,annot)) -> LEXP_aux (lexp,(l,rewrite_annot annot))) - ; fE_aux = (fun (fexp,(l,annot)) -> FE_aux (fexp,(l,(rewrite_annot annot)))) - ; fES_aux = (fun (fexp,(l,annot)) -> FES_aux (fexp,(l,rewrite_annot annot))) - ; pat_aux = (fun (pexp,(l,annot)) -> Pat_aux (pexp,(l,rewrite_annot annot))) - ; lB_aux = (fun (lb,(l,annot)) -> LB_aux (lb,(l,rewrite_annot annot))) - } - exp + | (l, None) -> (l, None) + | (l, Some (env, typ, eff)) -> (l, Some (env, rewrite_t typ, eff)) in + + map_exp_annot rewrite_annot exp @@ -2082,7 +2793,7 @@ let rewrite_defs_remove_superfluous_letbinds = let alg = { id_exp_alg with e_aux = e_aux } in rewrite_defs_base - { rewrite_exp = (fun _ _ -> fold_exp alg) + { rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp @@ -2094,9 +2805,9 @@ let rewrite_defs_remove_superfluous_letbinds = let rewrite_defs_remove_superfluous_returns = - let has_unittype e = - let {t = t} = get_type e in - t = Tid "unit" in + let has_unittype e = match typ_of e with + | Typ_aux (Typ_id (Id_aux (Id "unit", _)), _) -> true + | _ -> false in let e_aux (exp,annot) = match exp with | E_internal_plet (pat,exp1,exp2) -> @@ -2119,7 +2830,7 @@ let rewrite_defs_remove_superfluous_returns = let alg = { id_exp_alg with e_aux = e_aux } in rewrite_defs_base - {rewrite_exp = (fun _ _ -> fold_exp alg) + {rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp @@ -2130,7 +2841,7 @@ let rewrite_defs_remove_superfluous_returns = let rewrite_defs_remove_e_assign = - let rewrite_exp _ _ e = + let rewrite_exp _ e = replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in rewrite_defs_base { rewrite_exp = rewrite_exp @@ -2146,6 +2857,8 @@ let rewrite_defs_remove_e_assign = let rewrite_defs_lem = top_sort_defs >> rewrite_defs_remove_vector_concat >> + rewrite_defs_remove_bitvector_pats >> + rewrite_sizeof >> rewrite_defs_exp_lift_assign >> rewrite_defs_remove_blocks >> rewrite_defs_letbind_effects >> @@ -2154,4 +2867,3 @@ let rewrite_defs_lem = rewrite_defs_remove_superfluous_letbinds >> rewrite_defs_remove_superfluous_returns - |