ml output passing simple test suite, except for register aliases

Known todo:
Write library functions in ocaml
Properly upper-case/lower-case the first letter of names to conform to ocaml requirements
Handle register aliases
Turn id reads to dereferences for local ref variables

3 files changed, 51 insertions, 35 deletions

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 1d3947cd..c28ea02a 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1200,7 +1200,7 @@ let star_sp = star ^^ space
 
 let doc_id_ocaml (Id_aux(i,_)) =
   match i with
-  | Id("bit") -> string "bool" 
+  | Id("bit") -> string "int" 
   | Id i -> string i
   | DeIid x ->
       (* add an extra space through empty to avoid a closing-comment
@@ -1223,7 +1223,7 @@ let doc_typ_ocaml, doc_atomic_typ_ocaml =
       Typ_arg_aux(Typ_arg_nexp m, _);
       Typ_arg_aux (Typ_arg_order ord, _);
       Typ_arg_aux (Typ_arg_typ typ, _)]) ->
-      parens (atomic_typ typ) ^^ (string "list")
+    string "value"
   | Typ_app(Id_aux (Id "range", _), [
     Typ_arg_aux(Typ_arg_nexp n, _);
     Typ_arg_aux(Typ_arg_nexp m, _);]) ->
@@ -1316,10 +1316,10 @@ let doc_exp_ocaml, doc_let_ocaml =
       group (parens (string "vector_append ") ^^ (exp l) ^^ space ^^ (exp r))
     | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r)
     | E_if(c,t,E_aux(E_block [], _)) ->
-      string "if" ^^ space ^^ string "to_bool" ^^  (exp c) ^/^
+      string "if" ^^ space ^^ string "to_bool" ^^  parens (exp c) ^/^
       string "then" ^^ space ^^ (exp t)
     | E_if(c,t,e) ->
-      string "if" ^^ space ^^ string "to_bool" ^^ group (exp c) ^/^
+      string "if" ^^ space ^^ string "to_bool" ^^ parens (exp c) ^/^
       string "then" ^^ space ^^ group (exp t) ^/^
       string "else" ^^ space ^^ group (exp e)
     | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
@@ -1361,7 +1361,7 @@ let doc_exp_ocaml, doc_let_ocaml =
       let call = match annot with
         | Base(_,External (Some n),_,_,_) -> string n
         | _ -> doc_id_ocaml f in
-      doc_unop call (parens (separate_map comma exp args))
+      parens (doc_unop call (parens (separate_map comma exp args)))
     | E_vector_access(v,e) ->
       let call = (match annot with
           | Base((_,t),_,_,_,_) ->
@@ -1371,12 +1371,12 @@ let doc_exp_ocaml, doc_let_ocaml =
           | _ -> (string "vector_access")) in
       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))
+      parens ((string "vector_subrange") ^^ space ^^ (exp v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2))
     | E_field((E_aux(_,(_,fannot)) as fexp),id) ->
       (match fannot with
        | Base((_,{t= Tapp("register",_)}),_,_,_,_) |
          Base((_,{t= Tabbrev(_,{t=Tapp("register",_)})}),_,_,_,_)->
-        parens ((string "get_register_field") ^^ space ^^ exp fexp ^^ space ^^
+        parens ((string "get_register_field") ^^ space ^^ (exp fexp) ^^ space ^^
                 (string "\"") ^^ (doc_id id) ^^ string "\"")
       | _ -> exp fexp ^^ dot ^^ doc_id id)
     | E_block [] -> string "()"
@@ -1450,7 +1450,7 @@ let doc_exp_ocaml, doc_let_ocaml =
       match annot with
       | Base((_,t),External(Some name),_,_,_) -> string name
       | _ -> doc_id_ocaml id in
-    separate space [call; parens (separate_map semi exp [e1;e2])]
+    separate space [call; parens (separate_map comma 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*)
@@ -1533,7 +1533,6 @@ let doc_typdef_ocaml (TD_aux(td,_)) = match td with
         (concat [string "type"; space; doc_id_ocaml id;])
         (enums_doc)
   | TD_register(id,n1,n2,rs) ->
-    (*TODO: not sure*)
     let doc_rid (r,id) = separate comma_sp [string "\"" ^^ doc_id id ^^ string "\""; doc_range_ocaml r;] in
     let doc_rids = group (separate_map (break 1) doc_rid rs) in
     match n1,n2 with
@@ -1599,6 +1598,6 @@ let doc_def_ocaml def = group (match def with
 let doc_defs_ocaml (Defs(defs)) =
   separate_map hardline doc_def_ocaml defs
 let pp_defs_ocaml f d top_line opens =
-  print f ((string top_line) ^^ hardline ^^
-           (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^^ 
+  print f (string "(*" ^^ (string top_line) ^^ string "*)" ^/^
+           (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^/^ 
            (doc_defs_ocaml d))
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 7c89a8ac..9fba79a5 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -561,6 +561,13 @@ let rewrite_exp_lift_assign_intro rewriters nmap ((E_aux (exp,(l,annot))) as ful
       | 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
+       rewrap (E_internal_let(le', e', E_aux(E_block [], (l, simple_annot {t=Tid "unit"}))))
+     | _ -> rewrite_base full_exp)         
   | _ -> rewrite_base full_exp
 
 let rewrite_defs_exp_lift_assign defs = rewrite_defs_base
diff --git a/src/type_check.ml b/src/type_check.ml
index 694317f5..9f97c482 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -612,10 +612,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       (*let _ = Printf.eprintf "Type checking cast: cast_t is %s constraints after checking e are %s\n" 
         (t_to_string cast_t) (constraints_to_string cs) in*)
       let t',cs2,ef',e' = type_coerce (Expr l) d_env Require true false b_env u e' cast_t in
-      (*let _ = Printf.eprintf "Type checking cast: after first coerce with u at %s, and final t' %s is and constraints are %s\n" 
+      (*let _ = Printf.eprintf "Type checking cast: after first coerce with u %s, t' %s is and constraints are %s\n" 
         (t_to_string u) (t_to_string t') (constraints_to_string cs2) in*)
       let t',cs3,ef'',e'' = type_coerce (Expr l) d_env Guarantee false false b_env cast_t e' expect_t in 
-      (*let _ = Printf.eprintf "Type checking cast: after second coerce expect_t is %s, t' %s is and constraints are %s\n" (t_to_string expect_t) (t_to_string t') (constraints_to_string cs3) in*)
+      (*let _ = Printf.eprintf "Type checking cast: after second coerce expect_t %s, t' %s and constraints are %s\n" 
+        (t_to_string expect_t) (t_to_string t') (constraints_to_string cs3) in*)
       (e'',t',t_env,cs_a@cs@cs2@cs3,bounds,union_effects ef' (union_effects ef'' ef))
     | E_app(id,parms) -> 
       let i = id_to_string id in
@@ -626,7 +627,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         | parms -> 
           (match check_exp envs imp_param p_typ (E_aux (E_tuple parms,(l,NoTyp))) with
           | ((E_aux(E_tuple parms',tannot')),arg_t,t_env,cs',_,ef_p) -> parms',arg_t,cs',ef_p
-          | _ -> raise (Reporting_basic.err_unreachable l "check_exp, given a tuple and a tuple type, didn't return a tuple"))) 
+          | _ ->
+            raise (Reporting_basic.err_unreachable l
+                     "check_exp, given a tuple and a tuple type, didn't return a tuple"))) 
       in
       let coerce_parms arg_t parms expect_arg_t =
         (match parms with
@@ -678,12 +681,15 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       | Some(Base(tp,Default,_,_,_)) ->
         typ_error l ("Function " ^ i ^ " must be specified, not just declared as a default, before use")
       | Some(Base((params,t),tag,cs,ef,bounds)) ->
-        (*let _ = Printf.eprintf "Going to check a function call %s with unsubstituted types %s and constraints %s \n" i (t_to_string t) (constraints_to_string cs) in*)
+        (*let _ = Printf.eprintf "Going to check a function call %s with unsubstituted types %s and constraints %s \n"
+          i (t_to_string t) (constraints_to_string cs) in*)
         let t,cs,ef,_ = subst params false t cs ef in
         (match t.t with
         | Tfn(arg,ret,imp,ef') ->
           (*let _ = Printf.eprintf "Checking funcation call of %s\n" i in
-          let _ = Printf.eprintf "Substituted types and constraints are %s and %s\n" (t_to_string t) (constraints_to_string cs) in*)
+          let _ = Printf.eprintf "Substituted types and constraints are %s and %s\n" 
+            (t_to_string t) (constraints_to_string cs) in*)
+          let ret,_ = get_abbrev d_env ret in 
           let parms,arg_t,cs_p,ef_p = check_parms arg parms in
           (*let _ = Printf.eprintf "Checked parms of %s\n" i in*)
           let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' parms in
@@ -705,26 +711,30 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
             ("No function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t))
           | [Base((params,t),tag,cs,ef,bounds)] ->
             (match t.t with
-              | Tfn(arg,ret,imp,ef') ->
-                let args',arg_ef',arg_cs' = coerce_parms arg_t args arg in
-                let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' args' in
-                (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,nob,
-                 union_effects ef_r (union_effects ef_p (union_effects (union_effects arg_ef' arg_ef) ef')))
-              | _ -> raise (Reporting_basic.err_unreachable l "Overloaded variant not a function"))
+             | Tfn(arg,ret,imp,ef') ->
+               let ret,_ = get_abbrev d_env ret in
+               let args',arg_ef',arg_cs' = coerce_parms arg_t args arg in
+               let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' args' in
+               (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,nob,
+                union_effects ef_r (union_effects ef_p (union_effects (union_effects arg_ef' arg_ef) ef')))
+             | _ -> raise (Reporting_basic.err_unreachable l "Overloaded variant not a function"))
           | variants' ->
             (match select_overload_variant d_env false true variants' expect_t with
-              | [] ->
-                typ_error l ("No function found with name " ^ i ^ ", expecting parameters " ^ (t_to_string arg_t) ^ " and returning " ^ (t_to_string expect_t))
-              | [Base((params,t),tag,cs,ef,bounds)] ->
-                (match t.t with
-                  |Tfn(arg,ret,imp,ef') ->
-                    let args',arg_ef',arg_cs' = coerce_parms arg_t args arg in 
-                    let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' args' in
-                    (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,nob,
-                     union_effects ef_r (union_effects ef_p (union_effects (union_effects arg_ef arg_ef') ef')))
-                 | _ -> raise (Reporting_basic.err_unreachable l "Overloaded variant not a function"))
-              | _ -> 
-                typ_error l ("More than one definition of " ^ i ^ " found with type " ^ (t_to_string arg_t) ^ " -> " ^ (t_to_string expect_t) ^ ". A cast may be required")))
+             | [] ->
+               typ_error l ("No function found with name " ^ i ^ ", expecting parameters " ^
+                            (t_to_string arg_t) ^ " and returning " ^ (t_to_string expect_t))
+             | [Base((params,t),tag,cs,ef,bounds)] ->
+               (match t.t with
+                |Tfn(arg,ret,imp,ef') ->
+                  let ret,_ = get_abbrev d_env ret in
+                  let args',arg_ef',arg_cs' = coerce_parms arg_t args arg in 
+                  let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' args' in
+                  (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,nob,
+                   union_effects ef_r (union_effects ef_p (union_effects (union_effects arg_ef arg_ef') ef')))
+                | _ -> raise (Reporting_basic.err_unreachable l "Overloaded variant not a function"))
+             | _ -> 
+               typ_error l ("More than one definition of " ^ i ^ " found with type " ^
+                            (t_to_string arg_t) ^ " -> " ^ (t_to_string expect_t) ^ ". A cast may be required")))
       | _ -> typ_error l ("Unbound function " ^ i))
     | E_app_infix(lft,op,rht) -> 
       let i = id_to_string op in
@@ -1271,7 +1281,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
     | E_exit e ->
       let (e',t',_,_,_,_) = check_exp envs imp_param (new_t ()) e in
       (E_aux (E_exit e',(l,(simple_annot expect_t))),expect_t,t_env,[],nob,pure_e)
-    | E_internal_cast _ | E_internal_exp _ | E_internal_exp_user _ -> 
+    | E_internal_cast _ | E_internal_exp _ | E_internal_exp_user _ | E_internal_let _ -> 
       raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
                     
 and check_block envs imp_param expect_t exps:((tannot exp) list * tannot * nexp_range list * t * effect) =