diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 120 | ||||
| -rw-r--r-- | src/ast_util.mli | 61 | ||||
| -rw-r--r-- | src/initial_check.ml | 69 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 285 | ||||
| -rw-r--r-- | src/parse_ast.ml | 1 | ||||
| -rw-r--r-- | src/rewriter.ml | 25 | ||||
| -rw-r--r-- | src/sail.ml | 5 | ||||
| -rw-r--r-- | src/type_check.ml | 113 | ||||
| -rw-r--r-- | src/type_check.mli | 50 |
9 files changed, 558 insertions, 171 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 82367e9e..0ba5617f 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -51,6 +51,8 @@ let no_annot = (Parse_ast.Unknown, ()) let inc_ord = Ord_aux (Ord_inc, Parse_ast.Unknown) let dec_ord = Ord_aux (Ord_dec, Parse_ast.Unknown) +let mk_id str = Id_aux (Id str, Parse_ast.Unknown) + let mk_nc nc_aux = NC_aux (nc_aux, Parse_ast.Unknown) let mk_nexp nexp_aux = Nexp_aux (nexp_aux, Parse_ast.Unknown) @@ -60,6 +62,8 @@ let unaux_exp (E_aux (exp_aux, _)) = exp_aux let mk_pat pat_aux = P_aux (pat_aux, no_annot) +let mk_lexp lexp_aux = LEXP_aux (lexp_aux, no_annot) + let mk_lit lit_aux = L_aux (lit_aux, Parse_ast.Unknown) let mk_lit_exp lit_aux = mk_exp (E_lit (mk_lit lit_aux)) @@ -76,6 +80,122 @@ let mk_fundef funcls = let mk_val_spec vs_aux = DEF_spec (VS_aux (vs_aux, no_annot)) +let kopt_kid (KOpt_aux (kopt_aux, _)) = + match kopt_aux with + | KOpt_none kid | KOpt_kind (_, kid) -> kid + +let is_nat_kopt = function + | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), _), _) -> true + | KOpt_aux (KOpt_none _, _) -> true + | _ -> false + +let is_order_kopt = function + | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), _), _) -> true + | _ -> false + +let is_typ_kopt = function + | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), _), _) -> true + | _ -> false + +let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l) +and nexp_simp_aux = function + | Nexp_minus (Nexp_aux (Nexp_sum (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 -> + nexp_simp_aux n1 + | Nexp_sum (Nexp_aux (Nexp_minus (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 -> + nexp_simp_aux n1 + | Nexp_sum (n1, n2) -> + begin + let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in + let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in + match n1_simp, n2_simp with + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 + c2) + | _, Nexp_neg n2 -> Nexp_minus (n1, n2) + | _, _ -> Nexp_sum (n1, n2) + end + | Nexp_times (n1, n2) -> + begin + let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in + let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in + match n1_simp, n2_simp with + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 * c2) + | _, _ -> Nexp_times (n1, n2) + end + | Nexp_minus (n1, n2) -> + begin + let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in + let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in + match n1_simp, n2_simp with + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 - c2) + | _, _ -> Nexp_minus (n1, n2) + end + | nexp -> nexp + +let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown) +let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) +let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown) +let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown) + +let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown) + +let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown) + +let int_typ = mk_id_typ (mk_id "int") +let nat_typ = mk_id_typ (mk_id "nat") +let unit_typ = mk_id_typ (mk_id "unit") +let bit_typ = mk_id_typ (mk_id "bit") +let real_typ = mk_id_typ (mk_id "real") +let app_typ id args = mk_typ (Typ_app (id, args)) +let atom_typ nexp = + mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))])) +let range_typ nexp1 nexp2 = + mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp1)); + mk_typ_arg (Typ_arg_nexp (nexp_simp 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 vector_typ n m ord typ = + mk_typ (Typ_app (mk_id "vector", + [mk_typ_arg (Typ_arg_nexp (nexp_simp n)); + mk_typ_arg (Typ_arg_nexp (nexp_simp m)); + mk_typ_arg (Typ_arg_order ord); + mk_typ_arg (Typ_arg_typ typ)])) + +let exc_typ = mk_id_typ (mk_id "exception") + +let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown) +let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown) +let nsum n1 n2 = Nexp_aux (Nexp_sum (n1, n2), Parse_ast.Unknown) +let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown) +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_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) +let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown) +let nc_lt n1 n2 = nc_lteq n1 (nsum n2 (nconstant 1)) +let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nconstant 1)) +let nc_and nc1 nc2 = mk_nc (NC_and (nc1, nc2)) +let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2)) +let nc_true = mk_nc NC_true +let nc_false = mk_nc NC_false + +let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown) + +let mk_fexp id exp = FE_aux (FE_Fexp (id, exp), no_annot) +let mk_fexps fexps = FES_aux (FES_Fexps (fexps, false), no_annot) + +let mk_effect effs = + Effect_aux (Effect_set (List.map (fun be_aux -> BE_aux (be_aux, Parse_ast.Unknown)) effs), Parse_ast.Unknown) + +let no_effect = mk_effect [] + +let quant_items : typquant -> quant_item list = function + | TypQ_aux (TypQ_tq qis, _) -> qis + | TypQ_aux (TypQ_no_forall, _) -> [] + let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f annot) and map_exp_annot_aux f = function | E_block xs -> E_block (List.map (map_exp_annot f) xs) diff --git a/src/ast_util.mli b/src/ast_util.mli index 7580404d..95afa232 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -44,21 +44,82 @@ open Ast +val mk_id : string -> id +val mk_kid : string -> kid +val mk_ord : order_aux -> order val mk_nc : n_constraint_aux -> n_constraint val mk_nexp : nexp_aux -> nexp val mk_exp : unit exp_aux -> unit exp val mk_pat : unit pat_aux -> unit pat +val mk_lexp : unit lexp_aux -> unit lexp val mk_lit : lit_aux -> lit val mk_lit_exp : lit_aux -> unit exp val mk_funcl : id -> unit pat -> unit exp -> unit funcl val mk_fundef : (unit funcl) list -> unit def 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 unaux_exp : 'a exp -> 'a exp_aux val inc_ord : order val dec_ord : order +(* Utilites for working with kinded_ids *) +val kopt_kid : kinded_id -> kid +val is_nat_kopt : kinded_id -> bool +val is_order_kopt : kinded_id -> bool +val is_typ_kopt : kinded_id -> bool + +(* Some handy utility functions for constructing types. *) +val mk_typ : typ_aux -> typ +val mk_typ_arg : typ_arg_aux -> typ_arg +val mk_id_typ : id -> typ + +(* Sail builtin types. *) +val int_typ : typ +val nat_typ : typ +val atom_typ : nexp -> typ +val range_typ : nexp -> nexp -> typ +val bit_typ : typ +val bool_typ : typ +val app_typ : id -> typ_arg list -> typ +val unit_typ : typ +val string_typ : typ +val real_typ : typ +val vector_typ : nexp -> nexp -> order -> typ -> typ +val list_typ : typ -> typ +val exc_typ : typ + +val no_effect : effect +val mk_effect : base_effect_aux list -> effect + +val nexp_simp : nexp -> nexp + +(* Utilities for building n-expressions *) +val nconstant : int -> nexp +val nminus : nexp -> nexp -> nexp +val nsum : nexp -> nexp -> nexp +val ntimes : nexp -> nexp -> nexp +val npow2 : nexp -> nexp +val nvar : kid -> nexp +val nid : id -> nexp (* NOTE: Nexp_id's don't do anything currently *) + +(* Numeric constraint builders *) +val nc_eq : nexp -> nexp -> n_constraint +val nc_neq : nexp -> nexp -> n_constraint +val nc_lteq : nexp -> nexp -> n_constraint +val nc_gteq : nexp -> nexp -> n_constraint +val nc_lt : nexp -> nexp -> n_constraint +val nc_gt : nexp -> nexp -> n_constraint +val nc_and : n_constraint -> n_constraint -> n_constraint +val nc_or : n_constraint -> n_constraint -> n_constraint +val nc_true : n_constraint +val nc_false : n_constraint + +val quant_items : typquant -> quant_item list + (* Functions to map over the annotations in sub-expressions *) val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp val map_pat_annot : ('a annot -> 'b annot) -> 'a pat -> 'b pat diff --git a/src/initial_check.ml b/src/initial_check.ml index 8e5fd35f..74faba25 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -1012,6 +1012,8 @@ let typschm_of_string order str = let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in typschm +let val_spec_of_string order id str = mk_val_spec (VS_extern_no_rename (typschm_of_string order str, id)) + let val_spec_ids (Defs defs) = let val_spec_id (VS_aux (vs_aux, _)) = match vs_aux with @@ -1027,14 +1029,56 @@ let val_spec_ids (Defs defs) = in IdSet.of_list (vs_ids defs) +let quant_item_param = function + | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))] + | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [prepend_id "typ_" (id_of_kid (kopt_kid kopt))] + | _ -> [] +let quant_item_typ = function + | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [atom_typ (nvar (kopt_kid kopt))] + | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ (Typ_var (kopt_kid kopt))] + | _ -> [] +let quant_item_arg = function + | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [mk_typ_arg (Typ_arg_nexp (nvar (kopt_kid kopt)))] + | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kopt))))] + | _ -> [] +let undefined_typschm id typq = + let qis = quant_items typq in + if qis = [] then + mk_typschm typq (mk_typ (Typ_fn (unit_typ, mk_typ (Typ_id id), mk_effect [BE_undef]))) + else + let arg_typ = mk_typ (Typ_tup (List.concat (List.map quant_item_typ qis))) in + let ret_typ = app_typ id (List.concat (List.map quant_item_arg qis)) in + mk_typschm typq (mk_typ (Typ_fn (arg_typ, ret_typ, mk_effect [BE_undef]))) + let generate_undefineds vs_ids (Defs defs) = + let gen_vs id str = + if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str] + in + let undefined_builtins = List.concat + [gen_vs (mk_id "internal_pick") "forall 'a:Type. list('a) -> 'a effect {undef}"; + gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}"; + gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}"; + gen_vs (mk_id "undefined_int") "unit -> int effect {undef}"; + gen_vs (mk_id "undefined_string") "unit -> string effect {undef}"; + gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; + (* FIXME: How to handle inc/dec order correctly? *) + gen_vs (mk_id "undefined_vector") "forall 'n 'm 'a:Type. (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}"; + gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"] + in let undefined_td = function | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id)); mk_fundef [mk_funcl (prepend_id "undefined_" id) (mk_pat (P_lit (mk_lit L_unit))) - (mk_exp (E_lit (mk_lit L_undef)))]] + (mk_exp (E_app (mk_id "internal_pick", + [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]] + | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> + let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in + [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id)); + mk_fundef [mk_funcl (prepend_id "undefined_" id) + pat + (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]] | _ -> [] in let rec undefined_defs = function @@ -1044,9 +1088,28 @@ let generate_undefineds vs_ids (Defs defs) = def :: undefined_defs defs | [] -> [] in - Defs (undefined_defs defs) + Defs (undefined_builtins @ undefined_defs defs) + +let rec get_registers = function + | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) :: defs -> (typ, id) :: get_registers defs + | def :: defs -> get_registers defs + | [] -> [] + +let generate_initialize_registers vs_ids (Defs defs) = + let regs = get_registers defs in + let initialize_registers = + if IdSet.mem (mk_id "initialize_registers") vs_ids || regs = [] then [] + else + [val_spec_of_string dec_ord (mk_id "initialize_registers") "unit -> unit effect {undef, wreg}"; + mk_fundef [mk_funcl (mk_id "initialize_registers") + (mk_pat (P_lit (mk_lit L_unit))) + (mk_exp (E_block (List.map (fun (typ, id) -> mk_exp (E_assign (mk_lexp (LEXP_cast (typ, id)), mk_lit_exp L_undef))) regs)))]] + in + Defs (defs @ initialize_registers) + let process_ast order defs = let (ast, _, _) = to_ast Nameset.empty initial_kind_env order defs in let vs_ids = val_spec_ids ast in - generate_undefineds vs_ids ast + let ast = generate_undefineds vs_ids ast in + generate_initialize_registers vs_ids ast diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml new file mode 100644 index 00000000..60622aba --- /dev/null +++ b/src/ocaml_backend.ml @@ -0,0 +1,285 @@ +open Ast +open Ast_util +open PPrint +open Type_check + +type ctx = + { register_inits : tannot exp list; + externs : id Bindings.t + } + +let empty_ctx = + { register_inits = []; + externs = Bindings.empty + } + +let zchar c = + let zc c = "z" ^ String.make 1 c in + if Char.code c <= 41 then zc (Char.chr (Char.code c + 16)) + else if Char.code c <= 47 then zc (Char.chr (Char.code c + 23)) + else if Char.code c <= 57 then String.make 1 c + else if Char.code c <= 64 then zc (Char.chr (Char.code c + 13)) + else if Char.code c <= 90 then String.make 1 c + else if Char.code c <= 94 then zc (Char.chr (Char.code c - 13)) + else if Char.code c <= 95 then "_" + else if Char.code c <= 96 then zc (Char.chr (Char.code c - 13)) + else if Char.code c <= 121 then String.make 1 c + else if Char.code c <= 122 then "zz" + else if Char.code c <= 126 then zc (Char.chr (Char.code c - 39)) + else raise (Invalid_argument "zchar") + +let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (Util.string_to_list str)) + +let zencode ctx id = + try string (string_of_id (Bindings.find id ctx.externs)) with + | Not_found -> string (zencode_string (string_of_id id)) + +let zencode_kid kid = string ("'" ^ zencode_string (string_of_id (id_of_kid kid))) + +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, 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] + | Typ_var kid -> zencode_kid kid + | Typ_exist _ | Typ_wild -> assert false +and ocaml_typ_arg ctx (Typ_arg_aux (typ_arg_aux, _) as typ_arg) = + match typ_arg_aux with + | Typ_arg_typ typ -> ocaml_typ ctx typ + | _ -> failwith ("OCaml: unexpected type argument " ^ string_of_typ_arg typ_arg) + +let ocaml_typquant typq = + let ocaml_qi = function + | QI_aux (QI_id kopt, _) -> zencode_kid (kopt_kid kopt) + | QI_aux (QI_const _, _) -> failwith "Ocaml type quantifiers should no longer contain constraints" + in + match quant_items typq with + | [qi] -> ocaml_qi qi + | qis -> parens (separate_map (string " * ") ocaml_qi qis) + +let ocaml_lit (L_aux (lit_aux, _)) = + match lit_aux with + | L_unit -> string "()" + | L_zero -> string "B0" + | L_one -> string "B1" + | L_true -> string "true" + | L_false -> string "false" + | L_num n -> string (string_of_int n) + | L_undef -> failwith "undefined should have been re-written prior to ocaml backend" + | L_string str -> dquotes (string (String.escaped str)) + | _ -> string "LIT" + +let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) = + match pat_aux with + | P_id id -> zencode ctx id + | P_lit lit -> ocaml_lit lit + | P_typ (_, pat) -> ocaml_pat ctx pat + | P_tup pats -> parens (separate_map (comma ^^ space) (ocaml_pat ctx) pats) + | P_list pats -> brackets (separate_map (semi ^^ space) (ocaml_pat ctx) pats) + | P_wild -> string "_" + | P_as (pat, id) -> separate space [ocaml_pat ctx pat; string "as"; zencode ctx id] + | _ -> string ("PAT<" ^ string_of_pat pat ^ ">") + +let begin_end doc = group (string "begin" ^^ nest 2 (break 1 ^^ doc) ^/^ string "end") + +let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = + match exp_aux with + | E_app (f, [x]) -> zencode ctx f ^^ space ^^ ocaml_atomic_exp ctx x + | E_app (f, xs) -> zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs) + | E_return exp -> separate space [string "r.return"; ocaml_atomic_exp ctx exp] + | E_assert (exp, _) -> separate space [string "assert"; ocaml_atomic_exp ctx exp] + | E_cast (_, exp) -> ocaml_exp ctx exp + | E_block [exp] -> ocaml_exp ctx exp + | E_block [] -> string "()" + | E_block exps -> begin_end (ocaml_block ctx exps) + | E_field (exp, id) -> ocaml_atomic_exp ctx exp ^^ dot ^^ zencode ctx id + | E_exit exp -> string "failwith" ^^ space ^^ dquotes (string (String.escaped (string_of_exp exp))) + | E_case (exp, pexps) -> + begin_end (separate space [string "match"; ocaml_atomic_exp ctx exp; string "with"] + ^/^ ocaml_pexps ctx pexps) + | E_assign (lexp, exp) -> separate space [ocaml_lexp ctx lexp; string ":="; ocaml_exp ctx exp] + | E_if (c, t, e) -> separate space [string "if"; ocaml_atomic_exp ctx c; + 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) + | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) -> + enclose lbrace rbrace (separate space [ocaml_atomic_exp ctx exp; + string "with"; + separate_map (semi ^^ space) (ocaml_fexp ctx) fexps]) + | E_let (lb, exp) -> + separate space [string "let"; ocaml_letbind ctx lb; string "in"] + ^/^ ocaml_exp ctx exp + | E_internal_let (lexp, exp1, exp2) -> + 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 + | _ -> string ("EXP(" ^ string_of_exp exp ^ ")") +and ocaml_letbind ctx (LB_aux (lb_aux, _)) = + match lb_aux with + | LB_val_implicit (pat, exp) -> separate space [ocaml_pat ctx pat; equals; ocaml_atomic_exp ctx exp] + | _ -> failwith "Ocaml: Explicit letbind found" +and ocaml_pexps ctx = function + | [pexp] -> ocaml_pexp ctx pexp + | pexp :: pexps -> ocaml_pexp ctx pexp ^/^ ocaml_pexps ctx pexps + | [] -> empty +and ocaml_pexp ctx = function + | Pat_aux (Pat_exp (pat, exp), _) -> + separate space [bar; ocaml_pat ctx pat; string "->"] + ^//^ group (ocaml_exp ctx exp) + | Pat_aux (Pat_when (pat, wh, exp), _) -> + separate space [bar; ocaml_pat ctx pat; string "when"; ocaml_atomic_exp ctx exp; string "->"] + ^//^ group (ocaml_exp ctx exp) +and ocaml_block ctx = function + | [exp] -> ocaml_exp ctx exp + | exp :: exps -> ocaml_exp ctx exp ^^ semi ^/^ ocaml_block ctx exps + | _ -> assert false +and ocaml_fexp ctx (FE_aux (FE_Fexp (id, exp), _)) = + separate space [zencode ctx id; equals; ocaml_exp ctx exp] +and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) = + match exp_aux with + | E_lit lit -> ocaml_lit lit + | E_id id -> + begin + match Env.lookup_id id (env_of exp) with + | Local (Immutable, _) | Unbound -> zencode ctx id + | Register _ | Local (Mutable, _) -> bang ^^ zencode ctx id + | _ -> assert false + end + | E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps) + | _ -> parens (ocaml_exp ctx exp) +and ocaml_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) = + match lexp_aux with + | LEXP_cast _ | LEXP_id _ -> ocaml_atomic_lexp ctx lexp + | _ -> string ("LEXP<" ^ string_of_lexp lexp ^ ">") +and ocaml_atomic_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) = + match lexp_aux with + | LEXP_cast (_, id) -> zencode ctx id + | LEXP_id id -> zencode ctx id + | _ -> parens (ocaml_lexp ctx lexp) + +let rec get_initialize_registers = function + | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _, E_aux (E_block inits, _)), _)]), _)) :: defs + when Id.compare id (mk_id "initialize_registers") = 0 -> + inits + | _ :: defs -> get_initialize_registers defs + | [] -> [] + +let initial_value_for id inits = + let find_reg = function + | E_aux (E_assign (LEXP_aux (LEXP_cast (_, reg_id), _), init), _) -> Some init + | _ -> None + in + match Util.option_first find_reg inits with + | Some init -> init + | None -> failwith ("No assignment to register ^ " ^ string_of_id id ^ " in initialize_registers") + +let ocaml_dec_spec ctx (DEC_aux (reg, _)) = + match reg with + | DEC_reg (typ, id) -> + separate space [string "let"; zencode ctx id; colon; + parens (ocaml_typ ctx typ); string "ref"; equals; + string "ref"; parens (ocaml_exp ctx (initial_value_for id ctx.register_inits))] + | _ -> failwith "Unsupported register declaration" + +let ocaml_funcls ctx = function + | [] -> failwith "Ocaml: empty function" + | [FCL_aux (FCL_Funcl (id, pat, exp),_)] -> + separate space [string "let"; zencode ctx id; ocaml_pat ctx pat; equals; string "with_return (fun r ->"] + ^//^ ocaml_exp ctx exp + ^^ rparen + | _ -> string "MBF" (* failwith "Ocaml: multi-body function should have been re-written by now" *) + +let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) = + ocaml_funcls ctx funcls + +let rec ocaml_fields ctx = + let ocaml_field typ id = + separate space [zencode ctx id; colon; ocaml_typ ctx typ] + in + function + | [(typ, id)] -> ocaml_field typ id + | (typ, id) :: fields -> ocaml_field typ id ^^ semi ^/^ ocaml_fields ctx fields + | [] -> empty + +let rec ocaml_cases ctx = + let ocaml_case = function + | Tu_aux (Tu_id id, _) -> separate space [bar; zencode ctx id] + | Tu_aux (Tu_ty_id (typ, id), _) -> separate space [bar; zencode ctx id; string "of"; ocaml_typ ctx typ] + in + function + | [tu] -> ocaml_case tu + | tu :: tus -> ocaml_case tu ^/^ ocaml_cases ctx tus + | [] -> empty + +let rec ocaml_enum ctx = function + | [id] -> zencode ctx id + | id :: ids -> zencode ctx id ^/^ ocaml_enum ctx ids + | [] -> empty + +let ocaml_typedef ctx (TD_aux (td_aux, _)) = + match td_aux with + | TD_record (id, _, typq, fields, _) -> + (separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals; lbrace] + ^//^ ocaml_fields ctx fields) + ^/^ rbrace + | TD_variant (id, _, typq, cases, _) -> + separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals] + ^//^ ocaml_cases ctx cases + | TD_enum (id, _, ids, _) -> + separate space [string "type"; zencode ctx id; equals] + ^//^ ocaml_enum ctx ids + | TD_abbrev (id, _, TypSchm_aux (TypSchm_ts (typq, typ), _)) -> + separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals; ocaml_typ ctx typ] + +let get_externs (Defs defs) = + let extern_id (VS_aux (vs_aux, _)) = + match vs_aux with + | VS_val_spec (typschm, id) -> [] + | VS_extern_no_rename (typschm, id) -> [(id, id)] + | VS_extern_spec (typschm, id, name) -> [(id, mk_id name)] + | VS_cast_spec (typschm, id) -> [] + in + let rec extern_ids = function + | DEF_spec vs :: defs -> extern_id vs :: extern_ids defs + | def :: defs -> extern_ids defs + | [] -> [] + in + List.fold_left (fun exts (id, name) -> Bindings.add id name exts) Bindings.empty (List.concat (extern_ids defs)) + +let ocaml_def_end = string ";;" ^^ twice hardline + +let ocaml_def ctx def = match def with + | DEF_reg_dec ds -> group (ocaml_dec_spec ctx ds) ^^ ocaml_def_end + | DEF_fundef fd -> group (ocaml_fundef ctx fd) ^^ ocaml_def_end + | DEF_type td -> group (ocaml_typedef ctx td) ^^ ocaml_def_end + | _ -> empty + +let ocaml_defs (Defs defs) = + let ctx = { register_inits = get_initialize_registers defs; + externs = get_externs (Defs defs) + } + in + let empty_reg_init = + if ctx.register_inits = [] + then + separate space [string "let"; zencode ctx (mk_id "initialize_registers"); string "()"; equals; string "()"] + ^^ ocaml_def_end + else empty + in + (string "open Sail_lib" ^^ ocaml_def_end) + ^^ concat (List.map (ocaml_def ctx) defs) + ^^ empty_reg_init + +let ocaml_main ctx spec = + concat [separate space [string "open"; string spec] ^^ ocaml_def_end; + separate space [string "let"; string "()"; equals] + ^//^ (zencode ctx (mk_id "initialize_registers") ^^ string "()" ^^ semi + ^/^ zencode ctx (mk_id "main") ^^ string "()") + ] + +let ocaml_pp_defs f defs = + ToChannel.pretty 1. 80 f (ocaml_defs defs) diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 3951ab51..b259611d 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -288,6 +288,7 @@ exp_aux = (* Expression *) | E_try of exp * pexp list | E_return of exp | E_assert of exp * exp + | E_internal_let of exp * exp * exp and exp = E_aux of exp_aux * l diff --git a/src/rewriter.ml b/src/rewriter.ml index eb2a0bdf..f099427d 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -1040,6 +1040,8 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = let rec rewrite_e_aux split_sizeof (E_aux (e_aux, (l, _)) as orig_exp) = let env = env_of orig_exp in match e_aux with + | E_sizeof (Nexp_aux (Nexp_constant c, _) as nexp) -> + E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect))) | E_sizeof nexp -> begin match simplify_nexp (rewrite_nexp_ids (env_of orig_exp) nexp) with @@ -2467,7 +2469,7 @@ let rewrite_overload_cast (Defs defs) = let remove_cast_vs (VS_aux (vs_aux, annot)) = match vs_aux with | VS_val_spec (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot) - | VS_extern_no_rename (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot) + | VS_extern_no_rename (typschm, id) -> VS_aux (VS_extern_no_rename (typschm, id), annot) | VS_extern_spec (typschm, id, e) -> VS_aux (VS_extern_spec (typschm, id, e), annot) | VS_cast_spec (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot) in @@ -2489,6 +2491,11 @@ let rewrite_undefined = mk_exp (E_app (prepend_id "undefined_" id, [mk_lit_exp L_unit])) | Typ_app (id, args) -> mk_exp (E_app (prepend_id "undefined_" id, List.concat (List.map undefined_of_typ_args args))) + | Typ_var kid -> + (* FIXME: bit of a hack, need to add a restriction to how + polymorphic undefined can be in the type checker to + guarantee this always works. *) + mk_exp (E_id (prepend_id "typ_" (id_of_kid kid))) | Typ_fn _ -> assert false and undefined_of_typ_args (Typ_arg_aux (typ_arg_aux, _) as typ_arg) = match typ_arg_aux with @@ -2499,7 +2506,6 @@ let rewrite_undefined = let rewrite_e_aux (E_aux (e_aux, _) as exp) = match e_aux with | E_lit (L_aux (L_undef, l)) -> - print_endline ("Undefined: " ^ string_of_typ (typ_of exp)); check_exp (env_of exp) (undefined_of_typ (typ_of exp)) (typ_of exp) | _ -> exp in @@ -2527,10 +2533,15 @@ let rewrite_simple_types (Defs defs) = Typ_id (mk_id "int") | Typ_app (id, [_; _]) when Id.compare id (mk_id "range") = 0 -> Typ_id (mk_id "int") + | Typ_app (id, args) -> Typ_app (id, List.concat (List.map simple_typ_arg args)) | Typ_fn (typ1, typ2, effs) -> Typ_fn (simple_typ typ1, simple_typ typ2, effs) | Typ_tup typs -> Typ_tup (List.map simple_typ typs) | Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux typ | typ_aux -> typ_aux + and simple_typ_arg (Typ_arg_aux (typ_arg_aux, l)) = + match typ_arg_aux with + | Typ_arg_typ typ -> [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)] + | _ -> [] in let simple_typschm (TypSchm_aux (TypSchm_ts (typq, typ), annot)) = TypSchm_aux (TypSchm_ts (simple_typquant typq, simple_typ typ), annot) @@ -2538,7 +2549,7 @@ let rewrite_simple_types (Defs defs) = let simple_vs (VS_aux (vs_aux, annot)) = match vs_aux with | VS_val_spec (typschm, id) -> VS_aux (VS_val_spec (simple_typschm typschm, id), annot) - | VS_extern_no_rename (typschm, id) -> VS_aux (VS_val_spec (simple_typschm typschm, id), annot) + | VS_extern_no_rename (typschm, id) -> VS_aux (VS_extern_no_rename (simple_typschm typschm, id), annot) | VS_extern_spec (typschm, id, e) -> VS_aux (VS_extern_spec (simple_typschm typschm, id, e), annot) | VS_cast_spec (typschm, id) -> VS_aux (VS_cast_spec (simple_typschm typschm, id), annot) in @@ -3366,10 +3377,10 @@ let rewrite_defs_ocaml = [ rewrite_defs_remove_vector_concat; rewrite_constraint; rewrite_trivial_sizeof; - (* rewrite_sizeof; *) - (* rewrite_simple_types; *) - (* rewrite_overload_cast; *) - (* rewrite_defs_exp_lift_assign; *) + rewrite_sizeof; + rewrite_simple_types; + rewrite_overload_cast; + rewrite_defs_exp_lift_assign; (* rewrite_defs_exp_lift_assign *) (* rewrite_defs_separate_numbs *) ] diff --git a/src/sail.ml b/src/sail.ml index 081a414f..0f84db9f 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -158,10 +158,13 @@ let main() = else ()); (if !(opt_print_ocaml) then let ast_ocaml = rewrite_ast_ocaml ast in - Pretty_print_sail.pp_defs stdout ast_ocaml; + (* Pretty_print_sail.pp_defs stdout ast_ocaml; *) + Ocaml_backend.ocaml_pp_defs stdout ast_ocaml; + (* if !(opt_libs_ocaml) = [] then output "" (Ocaml_out None) [out_name,ast_ocaml] else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [out_name,ast_ocaml] + *) else ()); (if !(opt_print_lem) then let ast_lem = rewrite_ast_lem ast in diff --git a/src/type_check.ml b/src/type_check.ml index 14c91247..43eb4e36 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -91,74 +91,6 @@ let orig_kid (Kid_aux (Var v, l) as kid) = with | Not_found -> kid -let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown) -let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) -let mk_id str = Id_aux (Id str, Parse_ast.Unknown) -let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown) -let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown) - -let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown) - -let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown) - -let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l) -and nexp_simp_aux = function - | Nexp_minus (Nexp_aux (Nexp_sum (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 -> - nexp_simp_aux n1 - | Nexp_sum (Nexp_aux (Nexp_minus (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 -> - nexp_simp_aux n1 - | Nexp_sum (n1, n2) -> - begin - let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in - let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in - match n1_simp, n2_simp with - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 + c2) - | _, Nexp_neg n2 -> Nexp_minus (n1, n2) - | _, _ -> Nexp_sum (n1, n2) - end - | Nexp_times (n1, n2) -> - begin - let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in - let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in - match n1_simp, n2_simp with - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 * c2) - | _, _ -> Nexp_times (n1, n2) - end - | Nexp_minus (n1, n2) -> - begin - let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in - let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in - typ_debug ("SIMP: " ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2); - match n1_simp, n2_simp with - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 - c2) - | _, _ -> Nexp_minus (n1, n2) - end - | nexp -> nexp - -let int_typ = mk_id_typ (mk_id "int") -let nat_typ = mk_id_typ (mk_id "nat") -let unit_typ = mk_id_typ (mk_id "unit") -let bit_typ = mk_id_typ (mk_id "bit") -let real_typ = mk_id_typ (mk_id "real") -let app_typ id args = mk_typ (Typ_app (id, args)) -let atom_typ nexp = - mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))])) -let range_typ nexp1 nexp2 = - mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp1)); - mk_typ_arg (Typ_arg_nexp (nexp_simp 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 vector_typ n m ord typ = - mk_typ (Typ_app (mk_id "vector", - [mk_typ_arg (Typ_arg_nexp (nexp_simp n)); - mk_typ_arg (Typ_arg_nexp (nexp_simp m)); - mk_typ_arg (Typ_arg_order ord); - mk_typ_arg (Typ_arg_typ typ)])) - -let exc_typ = mk_id_typ (mk_id "exception") - let is_range (Typ_aux (typ_aux, _)) = match typ_aux with | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)]) @@ -173,25 +105,6 @@ let is_list (Typ_aux (typ_aux, _)) = when string_of_id f = "list" -> Some typ | _ -> None -let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown) -let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown) -let nsum n1 n2 = Nexp_aux (Nexp_sum (n1, n2), Parse_ast.Unknown) -let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown) -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_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) -let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown) -let nc_lt n1 n2 = nc_lteq n1 (nsum n2 (nconstant 1)) -let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nconstant 1)) -let nc_and nc1 nc2 = mk_nc (NC_and (nc1, nc2)) -let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2)) -let nc_true = mk_nc NC_true -let nc_false = mk_nc NC_false - let mk_lit l = E_aux (E_lit (L_aux (l, Parse_ast.Unknown)), (Parse_ast.Unknown, ())) let rec nc_negate (NC_aux (nc, _)) = @@ -211,10 +124,6 @@ let rec nc_negate (NC_aux (nc, _)) = (* Utilities for constructing effect sets *) -let mk_effect effs = - Effect_aux (Effect_set (List.map (fun be_aux -> BE_aux (be_aux, Parse_ast.Unknown)) effs), Parse_ast.Unknown) - -let no_effect = mk_effect [] module BESet = Set.Make(BE) @@ -246,10 +155,6 @@ let string_of_index_sort = function ^ string_of_list " & " (fun (x, y) -> string_of_nexp x ^ " <= " ^ string_of_nexp y) constraints ^ "}" -let quant_items : typquant -> quant_item list = function - | TypQ_aux (TypQ_tq qis, _) -> qis - | TypQ_aux (TypQ_no_forall, _) -> [] - let quant_split typq = let qi_kopt = function | QI_aux (QI_id kopt, _) -> [kopt] @@ -262,23 +167,6 @@ let quant_split typq = let qis = quant_items typq in List.concat (List.map qi_kopt qis), List.concat (List.map qi_nc qis) -let kopt_kid (KOpt_aux (kopt_aux, _)) = - match kopt_aux with - | KOpt_none kid | KOpt_kind (_, kid) -> kid - -let is_nat_kopt = function - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), _), _) -> true - | KOpt_aux (KOpt_none _, _) -> true - | _ -> false - -let is_order_kopt = function - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), _), _) -> true - | _ -> false - -let is_typ_kopt = function - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), _), _) -> true - | _ -> false - (**************************************************************************) (* 1. Substitutions *) (**************************************************************************) @@ -768,6 +656,7 @@ end = struct end let add_register id typ env = + wf_typ env typ; if Bindings.mem id env.registers then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound") else diff --git a/src/type_check.mli b/src/type_check.mli index 6fef1e9b..401862cf 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -153,68 +153,22 @@ val add_typquant : typquant -> Env.t -> Env.t not of this form. *) val orig_kid : kid -> kid -(* Some handy utility functions for constructing types. *) -val mk_typ : typ_aux -> typ -val mk_typ_arg : typ_arg_aux -> typ_arg -val mk_id : string -> id -val mk_id_typ : id -> typ - -val no_effect : effect -val mk_effect : base_effect_aux list -> effect - val union_effects : effect -> effect -> effect val equal_effects : effect -> effect -> bool -val nconstant : int -> nexp -val nminus : nexp -> nexp -> nexp -val nsum : nexp -> nexp -> nexp -val ntimes : nexp -> nexp -> nexp -val npow2 : nexp -> nexp -val nvar : kid -> nexp -val nid : id -> nexp (* NOTE: Nexp_id's don't do anything currently *) - -(* Numeric constraint builders *) -val nc_eq : nexp -> nexp -> n_constraint -val nc_neq : nexp -> nexp -> n_constraint -val nc_lteq : nexp -> nexp -> n_constraint -val nc_gteq : nexp -> nexp -> n_constraint -val nc_lt : nexp -> nexp -> n_constraint -val nc_gt : nexp -> nexp -> n_constraint -val nc_and : n_constraint -> n_constraint -> n_constraint -val nc_or : n_constraint -> n_constraint -> n_constraint -val nc_true : n_constraint -val nc_false : n_constraint - (* Negate a n_constraint. Note that there's no NC_not constructor, so this flips all the inequalites a the n_constraint leaves and uses de-morgans to switch and to or and vice versa. *) val nc_negate : n_constraint -> n_constraint -val is_nat_kopt : kinded_id -> bool -val is_order_kopt : kinded_id -> bool -val is_typ_kopt : kinded_id -> bool - -(* Sail builtin types. *) -val int_typ : typ -val nat_typ : typ -val atom_typ : nexp -> typ -val range_typ : nexp -> nexp -> typ -val bit_typ : typ -val bool_typ : typ -val unit_typ : typ -val string_typ : typ -val real_typ : typ -val vector_typ : nexp -> nexp -> order -> typ -> typ -val list_typ : typ -> typ -val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ -val exc_typ : typ - (* Vector with default order. *) val dvector_typ : Env.t -> nexp -> nexp -> typ -> typ (* Vector of specific length with default order, i.e. lvector_typ env n bit_typ = bit[n]. *) val lvector_typ : Env.t -> nexp -> typ -> typ +val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ + type tannot = (Env.t * typ * effect) option (* Strip the type annotations from an expression. *) |