Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experiments

1 files changed, 18 insertions, 0 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 2f630021..048fbb15 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -70,6 +70,14 @@ let mk_lit_exp lit_aux = mk_exp (E_lit (mk_lit lit_aux))
 
 let mk_funcl id pat body = FCL_aux (FCL_Funcl (id, pat, body), no_annot)
 
+let mk_qi_nc nc = QI_aux (QI_const nc, Parse_ast.Unknown)
+
+let mk_qi_id bk kid =
+  let kopt =
+    KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (bk, Parse_ast.Unknown)], Parse_ast.Unknown), kid), Parse_ast.Unknown)
+  in
+  QI_aux (QI_id kopt, Parse_ast.Unknown)
+
 let mk_fundef funcls =
   let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in
   let effect_opt = Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown) in
@@ -155,6 +163,8 @@ let range_typ nexp1 nexp2 =
 let bool_typ = mk_id_typ (mk_id "bool")
 let string_typ = mk_id_typ (mk_id "string")
 let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)]))
+let tuple_typ typs = mk_typ (Typ_tup typs)
+let function_typ typ1 typ2 eff = mk_typ (Typ_fn (typ1, typ2, eff))
 
 let vector_typ n m ord typ =
   mk_typ (Typ_app (mk_id "vector",
@@ -173,6 +183,7 @@ let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
 let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
 let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown)
 
+let nc_set kid ints = mk_nc (NC_nat_set_bounded (kid, ints))
 let nc_eq n1 n2 = mk_nc (NC_fixed (n1, n2))
 let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2))
 let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
@@ -210,6 +221,7 @@ and map_exp_annot_aux f = function
   | E_tuple xs -> E_tuple (List.map (map_exp_annot f) xs)
   | E_if (cond, t, e) -> E_if (map_exp_annot f cond, map_exp_annot f t, map_exp_annot f e)
   | E_for (v, e1, e2, e3, o, e4) -> E_for (v, map_exp_annot f e1, map_exp_annot f e2, map_exp_annot f e3, o, map_exp_annot f e4)
+  | E_loop (loop_type, e1, e2) -> E_loop (loop_type, map_exp_annot f e1, map_exp_annot f e2)
   | E_vector exps -> E_vector (List.map (map_exp_annot f) exps)
   | E_vector_indexed (iexps, opt_default) ->
      E_vector_indexed (List.map (fun (i, exp) -> (i, map_exp_annot f exp)) iexps, map_opt_default_annot f opt_default)
@@ -297,6 +309,10 @@ let string_of_id = function
 let id_of_kid = function
   | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
 
+let kid_of_id = function
+  | Id_aux (Id v, l) -> Kid_aux (Var ("'" ^ v), l)
+  | Id_aux (DeIid v, _) -> assert false
+
 let string_of_kid = function
   | Kid_aux (Var v, _) -> v
 
@@ -461,6 +477,8 @@ let rec string_of_exp (E_aux (exp, _)) =
      ^ " by " ^ string_of_exp u ^ " order " ^ string_of_order ord
      ^ ") { "
      ^ string_of_exp body
+  | E_loop (While, cond, body) -> "while " ^ string_of_exp cond ^ " do " ^ string_of_exp body
+  | E_loop (Until, cond, body) -> "repeat " ^ string_of_exp body ^ " until " ^ string_of_exp cond
   | E_assert (test, msg) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")"
   | E_exit exp -> "exit " ^ string_of_exp exp
   | E_throw exp -> "throw " ^ string_of_exp exp