Improved ocaml backend to the point where the hexapod spec produces syntactically correct ocaml

6 files changed, 63 insertions, 9 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 0ba5617f..5740a3c7 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -77,6 +77,8 @@ let mk_fundef funcls =
   DEF_fundef
    (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), no_annot))
 
+let mk_letbind pat exp = LB_aux (LB_val_implicit (pat, exp), no_annot)
+
 let mk_val_spec vs_aux =
   DEF_spec (VS_aux (vs_aux, no_annot))
 
@@ -441,6 +443,8 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_cast (typ, exp) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_exp exp
   | E_vector vec -> "[" ^ string_of_list ", " string_of_exp vec ^ "]"
   | E_vector_access (v, n) -> string_of_exp v ^ "[" ^ string_of_exp n ^ "]"
+  | E_vector_update (v, n, exp) -> "[" ^ string_of_exp v ^ " with " ^ string_of_exp n ^ " = " ^ string_of_exp exp ^ "]"
+  | E_vector_update_subrange (v, n, m, exp) -> "[" ^ string_of_exp v ^ " with " ^ string_of_exp n ^ " .. " ^ string_of_exp m ^ " = " ^ string_of_exp exp ^ "]"
   | E_vector_subrange (v, n1, n2) -> string_of_exp v ^ "[" ^ string_of_exp n1 ^ " .. " ^ string_of_exp n2 ^ "]"
   | E_vector_append (v1, v2) -> string_of_exp v1 ^ " : " ^ string_of_exp v2
   | E_if (cond, then_branch, else_branch) ->
@@ -468,6 +472,8 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_comment _ -> "INTERNAL COMMENT"
   | E_comment_struc _ -> "INTERNAL COMMENT STRUC"
   | E_internal_let _ -> "INTERNAL LET"
+  | E_internal_return _ -> "INTERNAL RETURN"
+  | E_internal_plet _ -> "INTERNAL PLET"
   | _ -> "INTERNAL"
 and string_of_fexp (FE_aux (FE_Fexp (field, exp), _)) =
   string_of_id field ^ " = " ^ string_of_exp exp
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 95afa232..6a150872 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -60,6 +60,7 @@ val mk_val_spec : val_spec_aux -> unit def
 val mk_typschm : typquant -> typ -> typschm
 val mk_fexp : id -> unit exp -> unit fexp
 val mk_fexps : (unit fexp) list -> unit fexps
+val mk_letbind : unit pat -> unit exp -> unit letbind
 
 val unaux_exp : 'a exp -> 'a exp_aux
 
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index e73d98c1..8c8b8103 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -40,6 +40,7 @@ let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) =
   match typ_aux with
   | Typ_id id when Id.compare id (mk_id "string") = 0 -> string "string"
   | Typ_id id -> zencode ctx id
+  | Typ_app (id, []) -> zencode ctx id
   | Typ_app (id, typs) -> parens (separate_map (string " * ") (ocaml_typ_arg ctx) typs) ^^ space ^^ zencode ctx id
   | Typ_tup typs -> parens (separate_map (string " * ") (ocaml_typ ctx) typs)
   | Typ_fn (typ1, typ2, _) -> separate space [ocaml_typ ctx typ1; string "->"; ocaml_typ ctx typ2]
@@ -56,6 +57,7 @@ let ocaml_typquant typq =
     | QI_aux (QI_const _, _) -> failwith "Ocaml type quantifiers should no longer contain constraints"
   in
   match quant_items typq with
+  | [] -> empty
   | [qi] -> ocaml_qi qi
   | qis -> parens (separate_map (string " * ") ocaml_qi qis)
 
@@ -104,7 +106,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
                                       string "then"; ocaml_atomic_exp ctx t;
                                       string "else"; ocaml_atomic_exp ctx e]
   | E_record (FES_aux (FES_Fexps (fexps, _), _)) ->
-     enclose lbrace rbrace (separate_map (semi ^^ space) (ocaml_fexp ctx) fexps)
+     enclose lbrace rbrace (group (separate_map (semi ^^ break 1) (ocaml_fexp ctx) fexps))
   | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) ->
      enclose lbrace rbrace (separate space [ocaml_atomic_exp ctx exp;
                                             string "with";
@@ -116,7 +118,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
      separate space [string "let"; string "ref"; ocaml_atomic_lexp ctx lexp;
                      equals; ocaml_exp ctx exp1; string "in"]
      ^/^ ocaml_exp ctx exp2
-  | E_lit _ | E_list _ | E_id _ -> ocaml_atomic_exp ctx exp
+  | E_lit _ | E_list _ | E_id _ | E_tuple _ -> ocaml_atomic_exp ctx exp
   | _ -> string ("EXP(" ^ string_of_exp exp ^ ")")
 and ocaml_letbind ctx (LB_aux (lb_aux, _)) =
   match lb_aux with
@@ -145,11 +147,12 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
   | E_id id ->
      begin
        match Env.lookup_id id (env_of exp) with
-       | Local (Immutable, _) | Unbound -> zencode ctx id
+       | Local (Immutable, _) | Unbound | Enum _ -> zencode ctx id
        | Register _ | Local (Mutable, _) -> bang ^^ zencode ctx id
-       | _ -> assert false
+       | _ -> failwith ("Union constructor: " ^ zencode_string (string_of_id id))
      end
   | E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps)
+  | E_tuple exps -> parens (separate_map (comma ^^ space) (ocaml_exp ctx) exps)
   | _ -> parens (ocaml_exp ctx exp)
 and ocaml_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) =
   match lexp_aux with
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 15933653..8f1ac9f7 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -2216,7 +2216,7 @@ let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = match lex
     let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
     (lexp, E_aux (E_field (access, id), annot),
     (fun exp -> rexp (E_aux (E_record_update (access, field_update exp), annot))))
-  | _ -> raise (Reporting_basic.err_unreachable l "unsupported lexp")
+  | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le))
 
 (*Expects to be called after rewrite_defs; thus the following should not appear:
   internal_exp of any form
@@ -2590,6 +2590,44 @@ let rewrite_simple_types (Defs defs) =
   let defs = Defs (List.map simple_def defs) in
   rewrite_defs_base simple_defs defs
 
+let rewrite_tuple_assignments defs =
+  let assign_tuple e_aux annot =
+    let env = env_of_annot annot in
+    match e_aux with
+    | E_assign (LEXP_aux (LEXP_tup lexps, _), exp) ->
+       let (_, ids) = List.fold_left (fun (n, ids) _ -> (n + 1, ids @ [mk_id ("tup__" ^ string_of_int n)])) (0, []) lexps in
+       let block_assign i lexp = mk_exp (E_assign (strip_lexp lexp, mk_exp (E_id (mk_id ("tup__" ^ string_of_int i))))) in
+       let block = mk_exp (E_block (List.mapi block_assign lexps)) in
+       let letbind = mk_letbind (mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))) (strip_exp exp) in
+       let let_exp = mk_exp (E_let (letbind, block)) in
+       check_exp env let_exp unit_typ
+    | _ -> E_aux (e_aux, annot)
+  in
+  let assign_exp = {
+      id_exp_alg with
+      e_aux = (fun (e_aux, annot) -> assign_tuple e_aux annot)
+    } in
+  let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in
+  rewrite_defs_base assign_defs defs
+
+let rewrite_simple_assignments defs =
+  let assign_e_aux e_aux annot =
+    let env = env_of_annot annot in
+    match e_aux with
+    | E_assign (lexp, exp) ->
+       print_endline ("REWRITE: " ^ string_of_exp (E_aux (e_aux, annot)));
+       let (lexp, _, rhs) = rewrite_local_lexp lexp in
+       let assign = mk_exp (E_assign (strip_lexp lexp, strip_exp (rhs exp))) in
+       check_exp env assign unit_typ
+    | _ -> E_aux (e_aux, annot)
+  in
+  let assign_exp = {
+      id_exp_alg with
+      e_aux = (fun (e_aux, annot) -> assign_e_aux e_aux annot)
+    } in
+  let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in
+  rewrite_defs_base assign_defs defs
+
 let rewrite_defs_remove_blocks =
   let letbind_wild v body =
     let (E_aux (_,(l,tannot))) = v in
@@ -2911,14 +2949,14 @@ let rewrite_defs_letbind_effects  =
 
 let rewrite_defs_effectful_let_expressions =
 
-  let e_let (lb,body) = 
+  let e_let (lb,body) =
     match lb with
     | LB_aux (LB_val_explicit (_,pat,exp'),annot')
     | LB_aux (LB_val_implicit (pat,exp'),annot') ->
        if effectful exp'
        then E_internal_plet (pat,exp',body)
        else E_let (lb,body) in
-                             
+
   let e_internal_let = fun (lexp,exp1,exp2) ->
     match lexp with
     | LEXP_aux (LEXP_id id,annot)
@@ -2932,7 +2970,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
@@ -3332,7 +3370,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
@@ -3377,6 +3415,8 @@ let rewrite_defs_lem =[
 let rewrite_defs_ocaml = [
     (* top_sort_defs; *)
   rewrite_undefined;
+  rewrite_tuple_assignments;
+  rewrite_simple_assignments;
   rewrite_defs_remove_vector_concat;
   rewrite_constraint;
   rewrite_trivial_sizeof;
diff --git a/src/type_check.ml b/src/type_check.ml
index 43eb4e36..4eb0688b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1794,6 +1794,7 @@ let irule r env exp =
 
 let strip_exp : 'a exp -> unit exp = function exp -> map_exp_annot (fun (l, _) -> (l, ())) exp
 let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) -> (l, ())) pat
+let strip_lexp : 'a lexp -> unit lexp = function lexp -> map_lexp_annot (fun (l, _) -> (l, ())) lexp
 
 let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ_aux, _) as typ) : tannot exp =
   let annot_exp_effect exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in
@@ -2536,6 +2537,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      let else_branch' = crule check_exp (add_constraints (List.map nc_negate constrs) (add_flows false flows env)) else_branch (typ_of then_branch') in
      annot_exp (E_if (cond', then_branch', else_branch')) (typ_of then_branch')
   | E_vector_access (v, n) -> infer_exp env (E_aux (E_app (mk_id "vector_access", [v; n]), (l, ())))
+  | E_vector_update (v, n, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update", [v; n; exp]), (l, ())))
+  | E_vector_update_subrange (v, n, m, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update_subrange", [v; n; m; exp]), (l, ())))
   | E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "append", [v1; v2]), (l, ())))
   | E_vector_subrange (v, n, m) -> infer_exp env (E_aux (E_app (mk_id "vector_subrange", [v; n; m]), (l, ())))
   | E_vector [] -> typ_error l "Cannot infer type of empty vector"
diff --git a/src/type_check.mli b/src/type_check.mli
index 401862cf..857e0019 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -174,6 +174,7 @@ type tannot = (Env.t * typ * effect) option
 (* Strip the type annotations from an expression. *)
 val strip_exp : 'a exp -> unit exp
 val strip_pat : 'a pat -> unit pat
+val strip_lexp : 'a lexp -> unit lexp
 
 (* Check an expression has some type. Returns a fully annotated
    version of the expression, where each subexpression is annotated