diff options
Diffstat (limited to 'src/ast_util.ml')
| -rw-r--r-- | src/ast_util.ml | 18 |
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 |