Additional tests for ocaml backend

6 files changed, 32 insertions, 8 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index d7b69c4f..0cea64a1 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1022,6 +1022,8 @@ let generate_undefineds vs_ids (Defs defs) =
   in
   let undefined_tu = function
     | Tu_aux (Tu_id id, _) -> mk_exp (E_id id)
+    | Tu_aux (Tu_ty_id (Typ_aux (Typ_tup typs, _), id), _) ->
+       mk_exp (E_app (id, List.map (fun _ -> mk_lit_exp L_undef) typs))
     | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef]))
   in
   let undefined_td = function
diff --git a/src/lexer2.mll b/src/lexer2.mll
index 312183fa..e24de0d0 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -147,6 +147,7 @@ let kw_table =
      ("type",		         (fun x -> Typedef));
      ("undefined",               (fun x -> Undefined));
      ("union",			 (fun x -> Union));
+     ("newtype",                 (fun x -> Newtype));
      ("with",                    (fun x -> With));
      ("val",                     (fun x -> Val));
      ("repeat",                  (fun _ -> Repeat));
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index f753b907..89220356 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -146,6 +146,7 @@ let ocaml_typ_id ctx = function
   | id when Id.compare id (mk_id "real") = 0 -> string "Num.num"
   | id when Id.compare id (mk_id "exception") = 0 -> string "exn"
   | id when Id.compare id (mk_id "register") = 0 -> string "ref"
+  | id when Id.compare id (mk_id "ref") = 0 -> string "ref"
   | id -> zencode ctx id
 
 let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) =
@@ -278,7 +279,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
      (string "let rec loop () =" ^//^ loop_body)
      ^/^ string "in"
      ^/^ string "loop ()"
-  | E_lit _ | E_list _ | E_id _ | E_tuple _ -> ocaml_atomic_exp ctx exp
+  | E_lit _ | E_list _ | E_id _ | E_tuple _ | E_ref _ -> ocaml_atomic_exp ctx exp
   | E_for (id, exp_from, exp_to, exp_step, ord, exp_body) ->
      let loop_var = separate space [string "let"; zencode ctx id; equals; string "ref"; ocaml_atomic_exp ctx exp_from; string "in"] in
      let loop_mod =
@@ -326,6 +327,7 @@ and ocaml_fexp ctx (FE_aux (FE_Fexp (id, exp), _)) =
 and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
   match exp_aux with
   | E_lit lit -> ocaml_lit lit
+  | E_ref id -> zencode ctx id
   | E_id id ->
      begin
        match Env.lookup_id id (env_of exp) with
@@ -362,10 +364,13 @@ and ocaml_assignment ctx (LEXP_aux (lexp_aux, _) as lexp) exp =
           separate space [zencode ctx id; string ":="; traced_exp]
        | _ -> separate space [zencode ctx id; string ":="; ocaml_exp ctx exp]
      end
+  | LEXP_deref ref_exp ->
+     separate space [ocaml_atomic_exp ctx ref_exp; string ":="; ocaml_exp ctx exp]
   | _ -> string ("LEXP<" ^ string_of_lexp lexp ^ ">")
 and ocaml_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) =
   match lexp_aux with
   | LEXP_cast _ | LEXP_id _ -> ocaml_atomic_lexp ctx lexp
+  | LEXP_deref exp -> ocaml_exp ctx exp
   | _ -> string ("LEXP<" ^ string_of_lexp lexp ^ ">")
 and ocaml_atomic_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) =
   match lexp_aux with
@@ -550,6 +555,9 @@ let ocaml_string_of_abbrev ctx id typq typ =
   separate space [string "let"; ocaml_string_of id; parens (arg ^^ space ^^ colon ^^ space ^^ zencode ctx id); equals]
   ^//^ ocaml_string_typ typ arg
 
+let ocaml_string_of_variant ctx id typq cases =
+  separate space [string "let"; ocaml_string_of id; string "_"; equals; string "\"VARIANT\""]
+
 let ocaml_typedef ctx (TD_aux (td_aux, _)) =
   match td_aux with
   | TD_record (id, _, typq, fields, _) ->
@@ -561,8 +569,10 @@ let ocaml_typedef ctx (TD_aux (td_aux, _)) =
   | TD_variant (id, _, _, cases, _) when string_of_id id = "exception" ->
      ocaml_exceptions ctx cases
   | TD_variant (id, _, typq, cases, _) ->
-     separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals]
-     ^//^ ocaml_cases ctx cases
+     (separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals]
+      ^//^ ocaml_cases ctx cases)
+     ^^ ocaml_def_end
+     ^^ ocaml_string_of_variant ctx id typq cases
   | TD_enum (id, _, ids, _) ->
      (separate space [string "type"; zencode ctx id; equals]
       ^//^ (bar ^^ space ^^ ocaml_enum ctx ids))
diff --git a/src/parser2.mly b/src/parser2.mly
index 34ab8732..521da6f8 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -154,7 +154,7 @@ let rec desugar_rchain chain s e =
 %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
 %token Enum Else False Forall Foreach Overload Function_ If_ In Inc Let_ Int Order Cast
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
-%token Undefined Union With Val Constraint Throw Try Catch Exit
+%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Record Mutual Var Ref
 
@@ -962,8 +962,12 @@ atomic_exp:
     { mk_exp (E_cast ($3, $1)) $startpos $endpos }
   | lit
     { mk_exp (E_lit $1) $startpos $endpos }
+  | id MinusGt id Unit
+    { mk_exp (E_app (prepend_id "_mod_" $3, [mk_exp (E_ref $1) $startpos($1) $endpos($1)])) $startpos $endpos }
   | id MinusGt id Lparen exp_list Rparen
     { mk_exp (E_app (prepend_id "_mod_" $3, mk_exp (E_ref $1) $startpos($1) $endpos($1) :: $5)) $startpos $endpos }
+  | atomic_exp Dot id Unit
+    { mk_exp (E_app (prepend_id "_mod_" $3, [$1])) $startpos $endpos }
   | atomic_exp Dot id Lparen exp_list Rparen
     { mk_exp (E_app (prepend_id "_mod_" $3, $1 :: $5)) $startpos $endpos }
   | atomic_exp Dot id
@@ -1054,6 +1058,10 @@ type_def:
     { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos }
   | Enum id Eq Lcurly enum Rcurly
     { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos }
+  | Newtype id Eq type_union
+    { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos }
+  | Newtype id typquant Eq type_union
+    { mk_td (TD_variant ($2, mk_namesectn, $3, [$5], false)) $startpos $endpos }
   | Union id Eq Lcurly type_unions Rcurly
     { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
   | Union id typquant Eq Lcurly type_unions Rcurly
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 87baa746..9b97b88b 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1354,7 +1354,7 @@ let id_is_unbound id env = match Env.lookup_id id env with
   | _ -> false
 
 let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
-  | LEXP_memory _ -> false
+  | LEXP_memory _ | LEXP_deref _ -> false
   | LEXP_id id
   | LEXP_cast (_, id) -> id_is_local_var id env
   | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps
@@ -1363,7 +1363,7 @@ let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
   | LEXP_field (lexp,_) -> lexp_is_local lexp env
 
 let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with
-  | LEXP_memory _ -> false
+  | LEXP_memory _ | LEXP_deref _ -> false
   | LEXP_id id
   | LEXP_cast (_, id) -> id_is_unbound id env
   | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps
@@ -1378,7 +1378,7 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
 let rec rewrite_lexp_to_rhs (do_rewrite : tannot lexp -> bool) ((LEXP_aux(lexp,((l,_) as annot))) as le) =
   if do_rewrite le then
     match lexp with
-    | LEXP_id _ | LEXP_cast (_, _) | LEXP_tup _ -> (le, (fun exp -> exp))
+    | LEXP_id _ | LEXP_cast (_, _) | LEXP_tup _ | LEXP_deref _ -> (le, (fun exp -> exp))
     | LEXP_vector (lexp, e) ->
        let (lhs, rhs) = rewrite_lexp_to_rhs do_rewrite lexp in
        (lhs, (fun exp -> rhs (E_aux (E_vector_update (lexp_to_exp lexp, e, exp), annot))))
diff --git a/src/type_check.ml b/src/type_check.ml
index d3967e7d..0c1d55ce 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -450,7 +450,8 @@ end = struct
 
   let add_overloads id ids env =
     typ_print ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]");
-    { env with overloads = Bindings.add id ids env.overloads }
+    let existing = try Bindings.find id env.overloads with Not_found -> [] in
+    { env with overloads = Bindings.add id (existing @ ids) env.overloads }
 
   let add_smt_op id str env =
     typ_print ("Adding smt binding " ^ string_of_id id ^ " to " ^ str);
@@ -2496,6 +2497,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
         subtyp l env typ vtyp; annot_lexp (LEXP_deref inferred_exp) typ, env
      | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "register" ->
         subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env
+     | _ ->
+        typ_error l (string_of_typ typ  ^ " must be a ref or register type in (*" ^ string_of_exp exp ^ ")")
      end
   | LEXP_id v ->
      begin match Env.lookup_id v env with