added something for remove_vector_string_patterns that for a give pattern-match expression produces one without vector_concat patterns, plus a list of variable bindings for slices of the vector. Not finished yet

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*)