diff options
| -rw-r--r-- | src/pretty_print.ml | 86 | ||||
| -rw-r--r-- | src/rewriter.ml | 39 | ||||
| -rw-r--r-- | src/rewriter.mli | 1 |
3 files changed, 97 insertions, 29 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 0ca8a582..9e050ba0 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1296,13 +1296,22 @@ let doc_pat_ocaml, doc_atomic_pat_ocaml = let doc_exp_ocaml, doc_let_ocaml = let rec exp (E_aux (e, (_,annot))) = match e with - | E_assign(le,e) -> - (*TODO: Check the type, if le is a ref cell, then do this. - if le is a register or a memory function (external), then call out - if le is a register or a memory function (internal), then replace with call - if le isn't immediately a ref cell, then maybe have a function to cope? - *) - doc_op coloneq (doc_lexp le) (exp e) + | E_assign((LEXP_aux(le_act,tannot) as le),e) -> + (match annot with + | Base(_,(Emp_local | Emp_set),_,_,_) -> + (match le_act with + | LEXP_id _ | LEXP_cast _ -> + (*Setting local variable fully *) + doc_op coloneq (doc_lexp_ocaml le) (exp e) + | LEXP_vector _ -> + doc_op (string "<-") (doc_lexp_ocaml le) (exp e) + | LEXP_vector_range _ -> + group ((string "set_vector_range") ^^ space ^^ (doc_lexp_ocaml le) ^^ space ^^ (exp e))) + | _ -> + (match le_act with + | LEXP_vector _ | LEXP_vector_range _ | LEXP_cast _ | LEXP_field _ -> + (doc_lexp_rwrite le e) + | LEXP_memory _ -> (doc_lexp_fcall le e))) | E_vector_append(l,r) -> group (parens (string "vector_append ") ^^ (exp l) ^^ space ^^ (exp r)) | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r) @@ -1340,7 +1349,12 @@ let doc_exp_ocaml, doc_let_ocaml = parens (call ^^ space ^^ exp v ^^ space ^^ exp e) | E_vector_subrange(v,e1,e2) -> parens ((string "vector_subrange") ^^ space ^^ exp v ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) - | E_field(fexp,id) -> exp fexp ^^ dot ^^ doc_id id + | E_field((E_aux(_,(_,fannot)) as fexp),id) -> + (match fannot with + | Base((_,{t= Tapp("register",_)}),External _,_,_,_) -> + parens ((string "get_register_field") ^^ space ^^ exp fexp ^^ space ^^ + (string "\"") ^^ (doc_id id) ^^ string "\"") + | _ -> exp fexp ^^ dot ^^ doc_id id) | E_block [] -> string "()" | E_block exps | E_nondet exps -> let exps_doc = separate_map (semi ^^ hardline) exp exps in @@ -1412,6 +1426,13 @@ let doc_exp_ocaml, doc_let_ocaml = | Base((_,t),External(Some name),_,_,_) -> string name | _ -> doc_id_ocaml id in separate space [call; parens (separate_map semi exp [e1;e2])] + | E_internal_let(lexp, eq_exp, in_exp) -> + separate space [string "let"; + doc_lexp_ocaml lexp; (*Rewriter/typecheck should ensure this is only cast or id*) + equals; + exp eq_exp; + string "in"; + exp in_exp] and let_exp (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> @@ -1426,19 +1447,33 @@ let doc_exp_ocaml, doc_let_ocaml = and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id id) (exp e) and doc_case (Pat_aux(Pat_exp(pat,e),_)) = - doc_op arrow (separate space [pipe; doc_atomic_pat pat]) (group (exp e)) + doc_op arrow (separate space [pipe; doc_atomic_pat_ocaml pat]) (group (exp e)) - (* lexps are parsed as eq_exp - we need to duplicate the precedence - * structure for them *) - and doc_lexp ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with - (*TODO: in the case of vector and memory and field, need to lift these up to rewrite them differently. *) - | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma exp args) - | LEXP_vector(v,e) -> doc_lexp v ^^ brackets (exp e) + and doc_lexp_ocaml ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with + | LEXP_vector(v,e) -> parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml v) ^^ dot ^^ parens (exp e) | LEXP_vector_range(v,e1,e2) -> - doc_lexp v ^^ brackets (exp e1 ^^ dotdot ^^ exp e2) - | LEXP_field(v,id) -> doc_lexp v ^^ dot ^^ doc_id id + parens ((string "vector_subrange") ^^ space ^^ doc_lexp_ocaml v ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) + | LEXP_field(v,id) -> doc_lexp_ocaml v ^^ dot ^^ doc_id id | LEXP_id id -> doc_id_ocaml id - | LEXP_cast(typ,id) -> (*prefix 2 1 (parens (doc_typ typ)) *) (doc_id_ocaml id) + | LEXP_cast(typ,id) -> (doc_id_ocaml id) + + and doc_lexp_rwrite ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = + match lexp with + | LEXP_vector(v,e) -> + doc_op (string "<-") + (group (parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml v)) ^^ dot ^^ parens (exp e)) + (exp e_new_v) + | LEXP_vector_range(v,e1,e2) -> + parens ((string "set_vector_subrange") ^^ space ^^ + doc_lexp_ocaml v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) + | LEXP_field(v,id) -> + parens ((string "set_register_field") ^^ space ^^ doc_lexp_ocaml v ^^ space ^^string "\"" ^^ doc_id id ^^ + string "\"" ^^ space ^^ exp e_new_v) + | LEXP_id id -> doc_id_ocaml id + | LEXP_cast(typ,id) -> (doc_id_ocaml id) + + and doc_lexp_fcall ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = match lexp with + | LEXP_memory(id,args) -> doc_id_ocaml id ^^ parens (separate_map comma exp (args@[e_new_v])) (* expose doc_exp and doc_let *) in exp, let_exp @@ -1481,8 +1516,6 @@ let doc_typdef_ocaml (TD_aux(td,_)) = match td with let doc_rec_ocaml (Rec_aux(r,_)) = match r with | Rec_nonrec -> empty - (* include trailing space because caller doesn't know if we return - * empty *) | Rec_rec -> string "rec" ^^ space let doc_tannot_opt_ocaml (Typ_annot_opt_aux(t,_)) = match t with @@ -1502,11 +1535,14 @@ let doc_fundef_ocaml (FD_aux(FD_function(r, typa, efa, fcls),_)) = separate space [(string "let"); (doc_rec_ocaml r); (doc_id_ocaml id); (doc_pat_ocaml pat); equals; (doc_exp_ocaml exp)] | _ -> let id = get_id fcls in - let sep = hardline ^^ pipe ^^ space in - let clauses = separate_map sep doc_funcl fcls in - separate space [string "let"; - doc_rec_ocaml r; - clauses] + let sep = hardline ^^ pipe ^^ space in + let clauses = separate_map sep doc_funcl fcls in + separate space [string "let"; + doc_rec_ocaml r; + doc_id_ocaml id; + equals; + (string "function"); + clauses] (*Aliases should be removed by here; registers not sure about*) (*let doc_dec (DEC_aux (reg,_)) = diff --git a/src/rewriter.ml b/src/rewriter.ml index e7048e8c..de865be2 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -117,7 +117,7 @@ let rewrite_pat rewriters nmap (P_aux (pat,(l,annot))) = 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) -> rewrap (P_typ(typ,rewrite pat)) + | P_typ(typ,pat) -> 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, @@ -311,8 +311,6 @@ let rewrite_defs (Defs defs) = rewrite_defs_base rewrite_def = rewrite_def; rewrite_defs = rewrite_defs_base} (Defs defs) - -(* signature of patterns *) type ('pat,'pat_aux,'fpat,'fpat_aux,'annot) pat_alg = { p_lit : lit -> 'pat_aux ; p_wild : 'pat_aux @@ -486,4 +484,37 @@ let remove_vector_concat_pat pat = let pat = fold_pat remove_vector_concats pat in (pat,decls) - + + + +(*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 rewrite_rec = rewriters.rewrite_exp rewriters nmap in + let rewrite_base = rewrite_exp rewriters nmap 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 + [(E_aux (E_internal_let(le', e', E_aux(E_block exps', (l, simple_annot {t=Tid "unit"}))), + (l, simple_annot t)))] + | e::exps -> (rewrite_rec e)::(walker exps) + in + rewrap (E_block (walker exps)) + | _ -> rewrite_base full_exp + +let rewrite_defs_ocaml defs = rewrite_defs_base + {rewrite_exp = rewrite_exp_lift_assign_intro; + 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 diff --git a/src/rewriter.mli b/src/rewriter.mli index 419be937..a28eed4a 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -17,3 +17,4 @@ type 'a rewriters = { rewrite_exp : 'a rewriters -> nexp_map option -> 'a exp -> val rewrite_exp : tannot rewriters -> nexp_map option -> tannot exp -> tannot exp val rewrite_defs : tannot defs -> tannot defs +val rewrite_defs_ocaml : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for ocaml out*) |