summaryrefslogtreecommitdiff
path: root/src/rewriter.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/rewriter.ml')
-rw-r--r--src/rewriter.ml116
1 files changed, 60 insertions, 56 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 4fad78e7..9e28f6f5 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -6,59 +6,61 @@ type 'a exp = 'a Ast.exp
type 'a emap = 'a Envmap.t
type envs = Type_check.envs
-let rec partial_assoc (v: 'a) (ls : ('a *'b) list ) : 'b option = match ls with
+let rec partial_assoc (eq: 'a -> 'a -> bool) (v: 'a) (ls : ('a *'b) list ) : 'b option = match ls with
| [] -> None
- | (v1,v2)::ls -> if v1 = v then Some v2 else partial_assoc v ls
+ | (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 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
- match nexp.nexp with
- | Nconst i -> E_aux (E_lit (L_aux (L_num (int_of_big_int i),l)), (l,simple_annot typ))
- | Nadd (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "+",l)),rewrite n2),
- (l, (tag_annot typ (External (Some "add")))))
- | Nmult (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "*",l)),rewrite n2),
- (l, tag_annot typ (External (Some "multiply"))))
- | Nsub (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "-",l)),rewrite n2),
- (l, tag_annot typ (External (Some "minus"))))
- | N2n (n, _) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 2,l)), (l, simple_annot (mk_atom_typ n_two))),
- (Id_aux (Id "**",l)),
- rewrite n), (l, tag_annot typ (External (Some "power"))))
- | Npow(n,i) -> E_aux (E_app_infix
- (rewrite n, (Id_aux (Id "**",l)),
- E_aux (E_lit (L_aux (L_num i,l)),
- (l, simple_annot (mk_atom_typ {nexp = Nconst (big_int_of_int i)})))),
- (l, tag_annot typ (External (Some "power"))))
- | Nneg(n) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 0,l)), (l, simple_annot (mk_atom_typ n_zero))),
- (Id_aux (Id "-",l)),
- rewrite n),
- (l, tag_annot typ (External (Some "minus"))))
- | Nvar v ->
- match program_vars with
- | None -> assert false
- | Some program_vars ->
- (match partial_assoc v program_vars with
- | None ->
- (*TODO these need to generate an error as it's a place where there's insufficient specification.
- But, for now I need to permit this to make power.sail compile, and most errors are in trap
- or vectors *)
- (*let _ = Printf.printf "unbound variable here %s\n" v in *)
- E_aux (E_id (Id_aux (Id v,l)),(l,simple_annot typ))
- | Some(None,ev) ->
- (*let _ = Printf.printf "var case of nvar rewrite, %s\n" ev in*)
- E_aux (E_id (Id_aux (Id ev,l)), (l, simple_annot typ))
- | Some(Some f,ev) ->
- E_aux (E_app ((Id_aux (Id f,l)), [ (E_aux (E_id (Id_aux (Id ev,l)), (l,simple_annot typ)))]),
- (l, tag_annot typ (External (Some f)))))
+ let actual_rewrite_n nexp =
+ match nexp.nexp with
+ | Nconst i -> E_aux (E_lit (L_aux (L_num (int_of_big_int i),l)), (l,simple_annot typ))
+ | Nadd (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "+",l)),rewrite n2),
+ (l, (tag_annot typ (External (Some "add")))))
+ | Nmult (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "*",l)),rewrite n2),
+ (l, tag_annot typ (External (Some "multiply"))))
+ | Nsub (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "-",l)),rewrite n2),
+ (l, tag_annot typ (External (Some "minus"))))
+ | N2n (n, _) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 2,l)), (l, simple_annot (mk_atom_typ n_two))),
+ (Id_aux (Id "**",l)),
+ rewrite n), (l, tag_annot typ (External (Some "power"))))
+ | Npow(n,i) -> E_aux (E_app_infix
+ (rewrite n, (Id_aux (Id "**",l)),
+ E_aux (E_lit (L_aux (L_num i,l)),
+ (l, simple_annot (mk_atom_typ {nexp = Nconst (big_int_of_int i)})))),
+ (l, tag_annot typ (External (Some "power"))))
+ | Nneg(n) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 0,l)), (l, simple_annot (mk_atom_typ n_zero))),
+ (Id_aux (Id "-",l)),
+ rewrite n),
+ (l, tag_annot typ (External (Some "minus"))))
+ | Nvar v -> (*TODO these need to generate an error as it's a place where there's insufficient specification.
+ But, for now I need to permit this to make power.sail compile, and most errors are in trap
+ or vectors *)
+ (*let _ = Printf.eprintf "unbound variable here %s\n" v in *)
+ E_aux (E_id (Id_aux (Id v,l)),(l,simple_annot typ)) in
+ match program_vars with
+ | None -> actual_rewrite_n nexp
+ | Some program_vars ->
+ (match partial_assoc nexp_eq_check nexp program_vars with
+ | None -> actual_rewrite_n nexp
+ | Some(None,ev) ->
+ (*let _ = Printf.eprintf "var case of rewrite, %s\n" ev in*)
+ E_aux (E_id (Id_aux (Id ev,l)), (l, simple_annot typ))
+ | Some(Some f,ev) ->
+ E_aux (E_app ((Id_aux (Id f,l)), [ (E_aux (E_id (Id_aux (Id ev,l)), (l,simple_annot typ)))]),
+ (l, tag_annot typ (External (Some f)))))
-let rec match_to_program_vars vs bounds =
- match vs with
+let rec match_to_program_vars ns bounds =
+ match ns with
| [] -> []
- | v::vs -> match find_var_from_nvar v bounds with
- | None -> match_to_program_vars vs bounds
- | Some(augment,ev) -> (v,(augment,ev))::(match_to_program_vars vs bounds)
+ | n::ns -> match find_var_from_nexp n bounds with
+ | 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)
let rec rewrite_exp (E_aux (exp,(l,annot))) =
let rewrap e = E_aux (e,(l,annot)) in
@@ -128,34 +130,36 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) =
| _ -> new_exp)
| _ -> new_exp))
| E_internal_exp (l,impl) ->
- (*let _ = Printf.printf "Rewriting internal expression\n" in*)
(match impl with
| Base((_,t),_,_,_,bounds) ->
+ (*let _ = Printf.eprintf "Rewriting internal expression, with type %s\n" (t_to_string t) in *)
match t.t with
(*Old case; should possibly be removed*)
| Tapp("register",[TA_typ {t= Tapp("vector",[ _; TA_nexp r;_;_])}])
| Tapp("vector", [_;TA_nexp r;_;_]) ->
- let vars = get_all_nvar r in
- (match vars with
+ (*let _ = Printf.eprintf "vector case with %s, bounds are %s\n" (n_to_string r) (bounds_to_string bounds) in*)
+ let nexps = expand_nexp r in
+ (match (match_to_program_vars nexps bounds) with
| [] -> rewrite_nexp_to_exp None l r
- | vars -> rewrite_nexp_to_exp (Some (match_to_program_vars vars bounds)) l r)
+ | map -> rewrite_nexp_to_exp (Some map) l r)
| Tapp("implicit", [TA_nexp i]) ->
- (*let _ = Printf.printf "Implicit case with %s\n" (n_to_string i) in*)
- let vars = get_all_nvar i in
- (match vars with
+ (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*)
+ let nexps = expand_nexp i in
+ (match (match_to_program_vars nexps bounds) with
| [] -> rewrite_nexp_to_exp None l i
- | vars -> rewrite_nexp_to_exp (Some (match_to_program_vars vars bounds)) l i))
+ | map -> rewrite_nexp_to_exp (Some map) l i))
| 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" (t_to_string tu) (t_to_string ti) in*)
match (tu.t,ti.t) with
| (Tapp("implicit", [TA_nexp u]),Tapp("implicit",[TA_nexp i])) ->
- let vars = get_all_nvar i in
- (match vars with
+ (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*)
+ let nexps = expand_nexp i in
+ (match (match_to_program_vars nexps bounds) with
| [] -> rewrite_nexp_to_exp None l i
(*add u to program_vars env; for now it will work out properly by accident*)
- | vars -> rewrite_nexp_to_exp (Some (match_to_program_vars vars bounds)) l i))
+ | map -> rewrite_nexp_to_exp (Some map) l i))
and rewrite_let (LB_aux(letbind,(l,annot))) = match letbind with
| LB_val_explicit (typschm, pat,exp) ->
@@ -175,7 +179,7 @@ and rewrite_lexp (LEXP_aux(lexp,(l,annot))) =
let rewrite_fun (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,annot))) =
let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),(l,annot))) =
- (*let _ = Printf.printf "Rewriting function %s\n" (match id with (Id_aux (Id i,_)) -> i) in*)
+ (*let _ = Printf.eprintf "Rewriting function %s\n" (match id with (Id_aux (Id i,_)) -> i) in*)
(FCL_aux (FCL_Funcl (id,pat,rewrite_exp exp),(l,annot)))
in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,annot))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 16:09:53 +0000