From 272d9565ef7f48baa0982a291c7fde8497ab0cd9 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 5 Dec 2018 20:49:38 +0000 Subject: Re-factor initial check Mostly this is to change how we desugar types in order to make us more flexible with what we can parse as a valid constraint as type. Previously the structure of the initial check forced some awkward limitations on what was parseable due to how the parse AST is set up. As part of this, I've taken the de-scattering of scattered functions out of the initial check, and moved it to a re-writing step after type-checking, where I think it logically belongs. This doesn't change much right now, but opens up some more possibilities in the future: Since scattered functions are now typechecked normally, any future module system for Sail would be able to handle them specially, and the Latex documentation backend can now document scattered functions explicitly, rather than relying on hackish 'de-scattering' logic to present documentation as the functions originally appeared. This has one slight breaking change which is that union clauses must appear before their uses in scattered functions, so union ast = Foo : unit function clause execute(Foo()) is ok, but function clause execute(Foo()) union ast = Foo : unit is not. Previously this worked because the de-scattering moved union clauses upwards before type-checking, but as this now happens after type-checking they must appear in the correct order. This doesn't occur in ARM, RISC-V, MIPS, but did appear in Cheri and I submitted a pull request to re-order the places where it happens. --- src/initial_check.ml | 1458 ++++++++++++++++++++------------------------------ 1 file changed, 585 insertions(+), 873 deletions(-) (limited to 'src/initial_check.ml') diff --git a/src/initial_check.ml b/src/initial_check.ml index aa3a7136..926e993a 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -51,1006 +51,718 @@ open Ast open Util open Ast_util +open Printf module Big_int = Nat_big_num +module P = Parse_ast + (* See mli file for details on what these flags do *) let opt_undefined_gen = ref false let opt_fast_undefined = ref false let opt_magic_hash = ref false let opt_enum_casts = ref false -module Envmap = Finite_map.Fmap_map(String) -module Nameset' = Set.Make(String) -module Nameset = struct - include Nameset' - let pp ppf nameset = - Format.fprintf ppf "{@[%a@]}" - (Pp.lst ",@ " Pp.pp_str) - (Nameset'.elements nameset) -end - -type kind = { mutable k : k_aux } -and k_aux = - | K_Typ - | K_Nat - | K_Ord - | K_Efct - | K_Val - | K_Lam of kind list * kind - | K_infer - -let rec kind_to_string kind = match kind.k with - | K_Nat -> "Nat" - | K_Typ -> "Type" - | K_Ord -> "Order" - | K_Efct -> "Effect" - | K_infer -> "Infer" - | K_Val -> "Val" - | K_Lam (kinds,kind) -> "Lam [" ^ string_of_list ", " kind_to_string kinds ^ "] -> " ^ (kind_to_string kind) - -(*Envs is a tuple of used names (currently unused), map from id to kind, default order for vector types and literal vectors *) -type envs = Nameset.t * kind Envmap.t * order -type 'a envs_out = 'a * envs - -let id_to_string (Id_aux(id,l)) = - match id with | Id(x) | DeIid(x) -> x - -let var_to_string (Kid_aux(Var v,l)) = v - -let typquant_to_quantkinds k_env typquant = - match typquant with - | TypQ_aux(tq,_) -> - (match tq with - | TypQ_no_forall -> [] - | TypQ_tq(qlist) -> - List.fold_right - (fun (QI_aux(qi,_)) rst -> - match qi with - | QI_const _ -> rst - | QI_id(ki) -> begin - match ki with - | KOpt_aux(KOpt_none(v),l) | KOpt_aux(KOpt_kind(_,v),l) -> - (match Envmap.apply k_env (var_to_string v) with - | Some(typ) -> typ::rst - | None -> raise (Reporting.err_unreachable l __POS__ "Envmap didn't get an entry during typschm processing")) - end) - qlist - []) - -let typ_error l msg opt_id opt_var opt_kind = - raise (Reporting.err_typ - l - (msg ^ - (match opt_id, opt_var, opt_kind with - | Some(id),None,Some(kind) -> (id_to_string id) ^ " of " ^ (kind_to_string kind) - | Some(id),None,None -> ": " ^ (id_to_string id) - | None,Some(v),Some(kind) -> (var_to_string v) ^ " of " ^ (kind_to_string kind) - | None,Some(v),None -> ": " ^ (var_to_string v) - | None,None,Some(kind) -> " " ^ (kind_to_string kind) - | _ -> ""))) +type ctx = { + kinds : kind_aux KBindings.t; + type_constructors : (kind_aux list) Bindings.t; + scattereds : ctx Bindings.t; + } let string_of_parse_id_aux = function - | Parse_ast.Id v -> v - | Parse_ast.DeIid v -> v + | P.Id v -> v + | P.DeIid v -> v -let string_of_parse_id (Parse_ast.Id_aux(id, l)) = string_of_parse_id_aux id +let string_of_parse_id (P.Id_aux (id, l)) = string_of_parse_id_aux id let string_contains str char = try (ignore (String.index str char); true) with | Not_found -> false -let to_ast_id (Parse_ast.Id_aux(id, l)) = - if string_contains (string_of_parse_id_aux id) '#' && not (!opt_magic_hash) - then typ_error l "Identifier contains hash character" None None None - else Id_aux ((match id with - | Parse_ast.Id(x) -> Id(x) - | Parse_ast.DeIid(x) -> DeIid(x)), - l) - -let to_ast_var (Parse_ast.Kid_aux(Parse_ast.Var v,l)) = Kid_aux(Var v,l) +let to_ast_var (P.Kid_aux (P.Var v, l)) = Kid_aux (Var v, l) -let to_ast_kind (Parse_ast.K_aux(k,l')) = +let to_ast_kind (P.K_aux (k, l)) = match k with - | Parse_ast.K_type -> K_aux(K_type,l'), { k = K_Typ} - | Parse_ast.K_int -> K_aux(K_int,l'), { k = K_Nat } - | Parse_ast.K_order -> K_aux(K_order,l'), { k = K_Ord } - -let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) : Ast.typ = - (* let _ = Printf.eprintf "to_ast_typ\n" in*) - match t with - | Parse_ast.ATyp_aux(t,l) -> - Typ_aux( (match t with - | Parse_ast.ATyp_id(id) -> Typ_id (to_ast_id id) - | Parse_ast.ATyp_var(v) -> - let v = to_ast_var v in - let mk = Envmap.apply k_env (var_to_string v) in - (match mk with - | Some(k) -> (match k.k with - | K_Typ -> Typ_var v - | K_infer -> k.k <- K_Typ; Typ_var v - | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k)) - | None -> typ_error l "Encountered an unbound variable" None (Some v) None) - | Parse_ast.ATyp_fn(arg,ret,efct) -> - begin match arg with - | Parse_ast.ATyp_aux (Parse_ast.ATyp_tup args, _) -> - Typ_fn (List.map (to_ast_typ k_env def_ord) args, - (to_ast_typ k_env def_ord ret), - (to_ast_effects k_env efct)) - | _ -> Typ_fn ([to_ast_typ k_env def_ord arg], - (to_ast_typ k_env def_ord ret), - (to_ast_effects k_env efct)) - end - | Parse_ast.ATyp_bidir (typ1, typ2) -> Typ_bidir ( (to_ast_typ k_env def_ord typ1), - (to_ast_typ k_env def_ord typ2)) - | Parse_ast.ATyp_tup(typs) -> Typ_tup( List.map (to_ast_typ k_env def_ord) typs) - | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_tb",il), [ b; r; ord ; ti]) -> - let make_r bot top = - match bot,top with - | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant b,_),Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,l) -> - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.add (Big_int.sub t b) (Big_int.of_int 1)),l) - | bot,(Parse_ast.ATyp_aux(_,l) as top) -> - Parse_ast.ATyp_aux((Parse_ast.ATyp_sum - ((Parse_ast.ATyp_aux - (Parse_ast.ATyp_sum (top, - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.of_int 1),Parse_ast.Unknown)), - Parse_ast.Unknown)), - (Parse_ast.ATyp_aux ((Parse_ast.ATyp_neg bot),Parse_ast.Unknown)))), l) in - let base = to_ast_nexp k_env b in - let rise = match def_ord with - | Ord_aux(Ord_inc,dl) -> to_ast_nexp k_env (make_r b r) - | Ord_aux(Ord_dec,dl) -> to_ast_nexp k_env (make_r r b) - | _ -> raise (Reporting.err_unreachable l __POS__ "Default order not inc or dec") in - Typ_app(Id_aux(Id "vector",il), - [Typ_arg_aux (Typ_arg_nexp base,Parse_ast.Unknown); - Typ_arg_aux (Typ_arg_nexp rise,Parse_ast.Unknown); - Typ_arg_aux (Typ_arg_order def_ord,Parse_ast.Unknown); - Typ_arg_aux (Typ_arg_typ (to_ast_typ k_env def_ord ti), Parse_ast.Unknown);]) - | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_r",il), [b;r;ord;ti]) -> - let make_sub_one t = - match t with - | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.sub t (Big_int.of_int 1)),l) - | t -> (Parse_ast.ATyp_aux - (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.negate (Big_int.of_int 1)),Parse_ast.Unknown)), - Parse_ast.Unknown)) in - let (base,rise) = match def_ord with - | Ord_aux(Ord_inc,dl) -> (to_ast_nexp k_env b), (to_ast_nexp k_env r) - | Ord_aux(Ord_dec,dl) -> (to_ast_nexp k_env (make_sub_one r)), (to_ast_nexp k_env r) - | _ -> raise (Reporting.err_unreachable l __POS__ "Default order not inc or dec") in - Typ_app(Id_aux(Id "vector",il), - [Typ_arg_aux (Typ_arg_nexp base,Parse_ast.Unknown); - Typ_arg_aux (Typ_arg_nexp rise,Parse_ast.Unknown); - Typ_arg_aux (Typ_arg_order def_ord,Parse_ast.Unknown); - Typ_arg_aux (Typ_arg_typ (to_ast_typ k_env def_ord ti), Parse_ast.Unknown);]) - | Parse_ast.ATyp_app (Parse_ast.Id_aux (Parse_ast.Id "int", il), [n]) -> - Typ_app(Id_aux(Id "atom", il), [Typ_arg_aux (Typ_arg_nexp (to_ast_nexp k_env n), Parse_ast.Unknown)]) - | Parse_ast.ATyp_app(pid,typs) -> - let id = to_ast_id pid in - let k = Envmap.apply k_env (id_to_string id) in - (match k with - | Some({k = K_Lam(args,t)}) -> - if ((List.length args) = (List.length typs)) - then - Typ_app(id,(List.map2 (fun k a -> (to_ast_typ_arg k_env def_ord k a)) args typs)) - else typ_error l "Type constructor given incorrect number of arguments" (Some id) None None - | None -> typ_error l "Required a type constructor, encountered an unbound identifier" (Some id) None None - | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None None) - | Parse_ast.ATyp_exist (kids, nc, atyp) -> - let kids = List.map to_ast_var kids in - let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in - let exist_typ = to_ast_typ k_env def_ord atyp in - Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ) - | Parse_ast.ATyp_with (atyp, nc) -> - let exist_typ = to_ast_typ k_env def_ord atyp in - let kids = KidSet.elements (tyvars_of_typ exist_typ) in - let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in - Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ) - | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None - ), l) - -and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp = - match n with - | Parse_ast.ATyp_aux(t,l) -> - (match t with - | Parse_ast.ATyp_id i -> Nexp_aux (Nexp_id (to_ast_id i), l) - | Parse_ast.ATyp_var v -> Nexp_aux (Nexp_var (to_ast_var v), l) - | Parse_ast.ATyp_constant i -> Nexp_aux (Nexp_constant i, l) - | Parse_ast.ATyp_sum (t1, t2) -> - let n1 = to_ast_nexp k_env t1 in - let n2 = to_ast_nexp k_env t2 in - Nexp_aux (Nexp_sum (n1, n2), l) - | Parse_ast.ATyp_exp t1 -> Nexp_aux(Nexp_exp(to_ast_nexp k_env t1),l) - | Parse_ast.ATyp_neg t1 -> Nexp_aux(Nexp_neg(to_ast_nexp k_env t1),l) - | Parse_ast.ATyp_times (t1, t2) -> - let n1 = to_ast_nexp k_env t1 in - let n2 = to_ast_nexp k_env t2 in - Nexp_aux (Nexp_times (n1, n2), l) - | Parse_ast.ATyp_minus (t1, t2) -> - let n1 = to_ast_nexp k_env t1 in - let n2 = to_ast_nexp k_env t2 in - Nexp_aux (Nexp_minus (n1, n2), l) - | Parse_ast.ATyp_app (id, ts) -> - let nexps = List.map (to_ast_nexp k_env) ts in - Nexp_aux (Nexp_app (to_ast_id id, nexps), l) - | _ -> typ_error l "Required an item of kind Nat, encountered an illegal form for this kind" None None None) - -and to_ast_order (k_env : kind Envmap.t) (def_ord : order) (o: Parse_ast.atyp) : Ast.order = - match o with - | Parse_ast.ATyp_aux(t,l) -> - (match t with - | Parse_ast.ATyp_var(v) -> - let v = to_ast_var v in - let mk = Envmap.apply k_env (var_to_string v) in - (match mk with - | Some(k) -> (match k.k with - | K_Ord -> Ord_aux(Ord_var v, l) - | K_infer -> k.k <- K_Ord; Ord_aux(Ord_var v,l) - | _ -> typ_error l "Required a variable with kind Order, encountered " None (Some v) (Some k)) - | None -> typ_error l "Encountered an unbound variable" None (Some v) None) - | Parse_ast.ATyp_inc -> Ord_aux(Ord_inc,l) - | Parse_ast.ATyp_dec -> Ord_aux(Ord_dec,l) - | Parse_ast.ATyp_default_ord -> def_ord - | _ -> typ_error l "Required an item of kind Order, encountered an illegal form for this kind" None None None - ) - -and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect = - match e with - | Parse_ast.ATyp_aux(t,l) -> - Effect_aux( (match t with - | Parse_ast.ATyp_var(v) -> - let v = to_ast_var v in - let mk = Envmap.apply k_env (var_to_string v) in - (match mk with - | Some k -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k) - | None -> typ_error l "Encountered an unbound variable" None (Some v) None) - | Parse_ast.ATyp_set(effects) -> - Effect_set( List.map - (fun efct -> match efct with - | Parse_ast.BE_aux(e,l) -> - BE_aux((match e with - | Parse_ast.BE_barr -> BE_barr - | Parse_ast.BE_rreg -> BE_rreg - | Parse_ast.BE_wreg -> BE_wreg - | Parse_ast.BE_rmem -> BE_rmem - | Parse_ast.BE_rmemt -> BE_rmemt - | Parse_ast.BE_wmem -> BE_wmem - | Parse_ast.BE_wmv -> BE_wmv - | Parse_ast.BE_wmvt -> BE_wmvt - | Parse_ast.BE_eamem -> BE_eamem - | Parse_ast.BE_exmem -> BE_exmem - | Parse_ast.BE_depend -> BE_depend - | Parse_ast.BE_undef -> BE_undef - | Parse_ast.BE_unspec -> BE_unspec - | Parse_ast.BE_nondet -> BE_nondet - | Parse_ast.BE_escape -> BE_escape - | Parse_ast.BE_config -> BE_config),l)) - effects) - | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None None - ), l) - -and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg : Parse_ast.atyp) : Ast.typ_arg = - let l = (match arg with Parse_ast.ATyp_aux(_,l) -> l) in - Typ_arg_aux ( - (match kind.k with - | K_Typ -> Typ_arg_typ (to_ast_typ k_env def_ord arg) - | K_Nat -> Typ_arg_nexp (to_ast_nexp k_env arg) - | K_Ord -> Typ_arg_order (to_ast_order k_env def_ord arg) - | _ -> raise (Reporting.err_unreachable l __POS__ ("To_ast_typ_arg received Lam kind or infer kind: " ^ kind_to_string kind))), - l) + | P.K_type -> K_aux (K_type, l) + | P.K_int -> K_aux (K_int, l) + | P.K_order -> K_aux (K_order, l) -and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint = - match c with - | Parse_ast.NC_aux(nc,l) -> - NC_aux( (match nc with - | Parse_ast.NC_equal(t1,t2) -> - let n1 = to_ast_nexp k_env t1 in - let n2 = to_ast_nexp k_env t2 in - NC_equal(n1,n2) - | Parse_ast.NC_not_equal(t1,t2) -> - let n1 = to_ast_nexp k_env t1 in - let n2 = to_ast_nexp k_env t2 in - NC_not_equal(n1,n2) - | Parse_ast.NC_bounded_ge(t1,t2) -> - let n1 = to_ast_nexp k_env t1 in - let n2 = to_ast_nexp k_env t2 in - NC_bounded_ge(n1,n2) - | Parse_ast.NC_bounded_le(t1,t2) -> - let n1 = to_ast_nexp k_env t1 in - let n2 = to_ast_nexp k_env t2 in - NC_bounded_le(n1,n2) - | Parse_ast.NC_set(id,bounds) -> - NC_set(to_ast_var id, bounds) - | Parse_ast.NC_or (nc1, nc2) -> - NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2) - | Parse_ast.NC_and (nc1, nc2) -> - NC_and (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2) - | Parse_ast.NC_true -> NC_true - | Parse_ast.NC_false -> NC_false - ), l) - -(* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *) -let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant * kind Envmap.t * kind Envmap.t = - let opt_kind_to_ast k_env local_names local_env (Parse_ast.KOpt_aux(ki,l)) = - let v, key, kind, ktyp = - match ki with - | Parse_ast.KOpt_none(v) -> - let v = to_ast_var v in - let key = var_to_string v in - let kind,ktyp = if (Envmap.in_dom key k_env) then None,(Envmap.apply k_env key) else None,(Some{ k = K_infer }) in - v,key,kind, ktyp - | Parse_ast.KOpt_kind(k,v) -> - let v = to_ast_var v in - let key = var_to_string v in - let kind,ktyp = to_ast_kind k in - v,key,Some(kind),Some(ktyp) - in - if (Nameset.mem key local_names) - then typ_error l "Encountered duplicate name in type scheme" None (Some v) None - else - let local_names = Nameset.add key local_names in - let kopt,k_env,k_env_local = (match kind,ktyp with - | Some(k),Some(kt) -> KOpt_kind(k,v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt)) - | None, Some(kt) -> KOpt_none(v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt)) - | _ -> raise (Reporting.err_unreachable l __POS__ "Envmap in dom is true but apply gives None")) in - KOpt_aux(kopt,l),k_env,local_names,k_env_local +let to_ast_id (P.Id_aux(id, l)) = + if string_contains (string_of_parse_id_aux id) '#' && not (!opt_magic_hash) then + raise (Reporting.err_general l "Identifier contains hash character and -dmagic_hash is unset") + else + Id_aux ((match id with + | P.Id x -> Id x + | P.DeIid x -> DeIid x), + l) + +let to_ast_var (P.Kid_aux(P.Var v,l)) = Kid_aux(Var v,l) + +let to_ast_effects = function + | P.ATyp_aux (P.ATyp_set effects, l) -> + let to_effect (P.BE_aux (e, l)) = + BE_aux ((match e with + | P.BE_barr -> BE_barr + | P.BE_rreg -> BE_rreg + | P.BE_wreg -> BE_wreg + | P.BE_rmem -> BE_rmem + | P.BE_rmemt -> BE_rmemt + | P.BE_wmem -> BE_wmem + | P.BE_wmv -> BE_wmv + | P.BE_wmvt -> BE_wmvt + | P.BE_eamem -> BE_eamem + | P.BE_exmem -> BE_exmem + | P.BE_depend -> BE_depend + | P.BE_undef -> BE_undef + | P.BE_unspec -> BE_unspec + | P.BE_nondet -> BE_nondet + | P.BE_escape -> BE_escape + | P.BE_config -> BE_config), + l) + in + Effect_aux (Effect_set (List.map to_effect effects), l) + | P.ATyp_aux (_, l) -> + raise (Reporting.err_typ l "Invalid effect set") + +(* Used for error messages involving lists of kinds *) +let format_kind_aux_list = function + | [kind] -> string_of_kind_aux kind + | kinds -> "(" ^ Util.string_of_list ", " string_of_kind_aux kinds ^ ")" + +let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) = + let aux = match aux with + | P.ATyp_id id -> Typ_id (to_ast_id id) + | P.ATyp_var v -> Typ_var (to_ast_var v) + | P.ATyp_fn (from_typ, to_typ, effects) -> + let from_typs = match from_typ with + | P.ATyp_aux (P.ATyp_tup typs, _) -> + List.map (to_ast_typ ctx) typs + | _ -> [to_ast_typ ctx from_typ] + in + Typ_fn (from_typs, to_ast_typ ctx to_typ, to_ast_effects effects) + | P.ATyp_bidir (typ1, typ2) -> Typ_bidir (to_ast_typ ctx typ1, to_ast_typ ctx typ2) + | P.ATyp_tup typs -> Typ_tup (List.map (to_ast_typ ctx) typs) + | P.ATyp_app (P.Id_aux (P.Id "int", il), [n]) -> + Typ_app (Id_aux (Id "atom", il), [to_ast_typ_arg ctx n K_int]) + | P.ATyp_app (id, args) -> + let id = to_ast_id id in + begin match Bindings.find_opt id ctx.type_constructors with + | None -> raise (Reporting.err_typ l (sprintf "Could not find type constructor %s" (string_of_id id))) + | Some kinds when List.length args <> List.length kinds -> + raise (Reporting.err_typ l (sprintf "%s : %s -> Type expected %d arguments, given %d" + (string_of_id id) (format_kind_aux_list kinds) + (List.length kinds) (List.length args))) + | Some kinds -> + Typ_app (id, List.map2 (to_ast_typ_arg ctx) args kinds) + end + | P.ATyp_exist (kids, nc, atyp) -> + let kids = List.map to_ast_var kids in + let ctx = { ctx with kinds = List.fold_left (fun kinds kid -> KBindings.add kid K_int kinds) ctx.kinds kids } in + Typ_exist (kids, to_ast_constraint ctx nc, to_ast_typ ctx atyp) + | _ -> raise (Reporting.err_typ l "Invalid type") in - match tq with - | Parse_ast.TypQ_aux(tqa,l) -> - (match tqa with - | Parse_ast.TypQ_no_forall -> TypQ_aux(TypQ_no_forall,l), k_env, Envmap.empty - | Parse_ast.TypQ_tq(qlist) -> - let rec to_ast_q_items k_env local_names local_env = function - | [] -> [],k_env,local_env - | q::qs -> (match q with - | Parse_ast.QI_aux(qi,l) -> - (match qi with - | Parse_ast.QI_const(n_const) -> - let c = QI_aux(QI_const(to_ast_nexp_constraint k_env n_const),l) in - let qis,k_env,local_env = to_ast_q_items k_env local_names local_env qs in - (c::qis),k_env,local_env - | Parse_ast.QI_id(kid) -> - let kid,k_env,local_names,local_env = opt_kind_to_ast k_env local_names local_env kid in - let c = QI_aux(QI_id(kid),l) in - let qis,k_env,local_env = to_ast_q_items k_env local_names local_env qs in - (c::qis),k_env,local_env)) - in - let lst,k_env,local_env = to_ast_q_items k_env Nameset.empty Envmap.empty qlist in - TypQ_aux(TypQ_tq(lst),l), k_env, local_env) - -let to_ast_typschm (k_env:kind Envmap.t) (def_ord:order) (tschm:Parse_ast.typschm) :Ast.typschm * kind Envmap.t * kind Envmap.t = - match tschm with - | Parse_ast.TypSchm_aux(ts,l) -> - (match ts with | Parse_ast.TypSchm_ts(tquant,t) -> - let tq,k_env,local_env = to_ast_typquant k_env tquant in - let typ = to_ast_typ k_env def_ord t in - TypSchm_aux(TypSchm_ts(tq,typ),l),k_env,local_env) - -let to_ast_lit (Parse_ast.L_aux(lit,l)) : lit = - L_aux( - (match lit with - | Parse_ast.L_unit -> L_unit - | Parse_ast.L_zero -> L_zero - | Parse_ast.L_one -> L_one - | Parse_ast.L_true -> L_true - | Parse_ast.L_false -> L_false - | Parse_ast.L_undef -> L_undef - | Parse_ast.L_num(i) -> L_num(i) - | Parse_ast.L_hex(h) -> L_hex(h) - | Parse_ast.L_bin(b) -> L_bin(b) - | Parse_ast.L_real r -> L_real r - | Parse_ast.L_string(s) -> L_string(s)) - ,l) - -let rec to_ast_typ_pat (Parse_ast.ATyp_aux (typ_aux, l)) = - match typ_aux with - | Parse_ast.ATyp_wild -> TP_aux (TP_wild, l) - | Parse_ast.ATyp_var kid -> TP_aux (TP_var (to_ast_var kid), l) - | Parse_ast.ATyp_app (Parse_ast.Id_aux (Parse_ast.Id "int", il), typs) -> - TP_aux (TP_app (Id_aux (Id "atom", il), List.map to_ast_typ_pat typs), l) - | Parse_ast.ATyp_app (f, typs) -> - TP_aux (TP_app (to_ast_id f, List.map to_ast_typ_pat typs), l) - | _ -> typ_error l "Unexpected type in type pattern" None None None - -let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pat,l) : Parse_ast.pat) : unit pat = - P_aux( - (match pat with - | Parse_ast.P_lit(lit) -> P_lit(to_ast_lit lit) - | Parse_ast.P_wild -> P_wild - | Parse_ast.P_or(pat1, pat2) -> - P_or (to_ast_pat k_env def_ord pat1, to_ast_pat k_env def_ord pat2) - | Parse_ast.P_var (pat, Parse_ast.ATyp_aux (Parse_ast.ATyp_id id, _)) -> - P_as (to_ast_pat k_env def_ord pat, to_ast_id id) - | Parse_ast.P_typ(typ,pat) -> P_typ(to_ast_typ k_env def_ord typ,to_ast_pat k_env def_ord pat) - | Parse_ast.P_id(id) -> P_id(to_ast_id id) - | Parse_ast.P_var (pat, typ) -> P_var (to_ast_pat k_env def_ord pat, to_ast_typ_pat typ) - | Parse_ast.P_app(id, []) -> P_id (to_ast_id id) - | Parse_ast.P_app(id, pats) -> - if List.length pats == 1 && string_of_parse_id id = "~" - then P_not (to_ast_pat k_env def_ord (List.hd pats)) - else P_app(to_ast_id id, List.map (to_ast_pat k_env def_ord) pats) - | Parse_ast.P_record(fpats,_) -> - P_record(List.map - (fun (Parse_ast.FP_aux(Parse_ast.FP_Fpat(id,fp),l)) -> - FP_aux(FP_Fpat(to_ast_id id, to_ast_pat k_env def_ord fp),(l,()))) - fpats, false) - | Parse_ast.P_vector(pats) -> P_vector(List.map (to_ast_pat k_env def_ord) pats) - | Parse_ast.P_vector_concat(pats) -> P_vector_concat(List.map (to_ast_pat k_env def_ord) pats) - | Parse_ast.P_tup(pats) -> P_tup(List.map (to_ast_pat k_env def_ord) pats) - | Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env def_ord) pats) - | Parse_ast.P_cons(pat1, pat2) -> P_cons (to_ast_pat k_env def_ord pat1, to_ast_pat k_env def_ord pat2) - | Parse_ast.P_string_append pats -> P_string_append (List.map (to_ast_pat k_env def_ord) pats) - ), (l,())) + Typ_aux (aux, l) + +and to_ast_typ_arg ctx (ATyp_aux (_, l) as atyp) = function + | K_type -> Typ_arg_aux (Typ_arg_typ (to_ast_typ ctx atyp), l) + | K_int -> Typ_arg_aux (Typ_arg_nexp (to_ast_nexp ctx atyp), l) + | K_order -> Typ_arg_aux (Typ_arg_order (to_ast_order ctx atyp), l) + +and to_ast_nexp ctx (P.ATyp_aux (aux, l)) = + let aux = match aux with + | P.ATyp_id id -> Nexp_id (to_ast_id id) + | P.ATyp_var v -> Nexp_var (to_ast_var v) + | P.ATyp_constant c -> Nexp_constant c + | P.ATyp_sum (t1, t2) -> Nexp_sum (to_ast_nexp ctx t1, to_ast_nexp ctx t2) + | P.ATyp_exp t1 -> Nexp_exp (to_ast_nexp ctx t1) + | P.ATyp_neg t1 -> Nexp_neg (to_ast_nexp ctx t1) + | P.ATyp_times (t1, t2) -> Nexp_times (to_ast_nexp ctx t1, to_ast_nexp ctx t2) + | P.ATyp_minus (t1, t2) -> Nexp_minus (to_ast_nexp ctx t1, to_ast_nexp ctx t2) + | P.ATyp_app (id, ts) -> Nexp_app (to_ast_id id, List.map (to_ast_nexp ctx) ts) + | _ -> raise (Reporting.err_typ l "Invalid numeric expression in type") + in + Nexp_aux (aux, l) +and to_ast_order ctx (P.ATyp_aux (aux, l)) = + match aux with + | ATyp_var v -> Ord_aux (Ord_var (to_ast_var v), l) + | ATyp_inc -> Ord_aux (Ord_inc, l) + | ATyp_dec -> Ord_aux (Ord_dec, l) + | _ -> raise (Reporting.err_typ l "Invalid order in type") + +and to_ast_constraint ctx (P.NC_aux (nc, l)) = + let nc = match nc with + | P.NC_equal (t1, t2) -> + NC_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2) + | P.NC_not_equal (t1, t2) -> + NC_not_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2) + | P.NC_bounded_ge (t1,t2) -> + NC_bounded_ge (to_ast_nexp ctx t1, to_ast_nexp ctx t2) + | P.NC_bounded_le(t1,t2) -> + NC_bounded_le (to_ast_nexp ctx t1, to_ast_nexp ctx t2) + | P.NC_set(id,bounds) -> + NC_set(to_ast_var id, bounds) + | P.NC_or (nc1, nc2) -> + NC_or (to_ast_constraint ctx nc1, to_ast_constraint ctx nc2) + | P.NC_and (nc1, nc2) -> + NC_and (to_ast_constraint ctx nc1, to_ast_constraint ctx nc2) + | P.NC_true -> NC_true + | P.NC_false -> NC_false + in + NC_aux (nc, l) -let rec to_ast_letbind (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.LB_aux(lb,l) : Parse_ast.letbind) : unit letbind = +let to_ast_quant_item ctx (P.QI_aux (aux, l)) = + match aux with + | P.QI_const nc -> QI_aux (QI_const (to_ast_constraint ctx nc), l), ctx + | P.QI_id (KOpt_aux (aux, kopt_l)) -> + let aux, ctx = match aux with + | P.KOpt_none v -> + let v = to_ast_var v in + KOpt_none v, { ctx with kinds = KBindings.add v K_int ctx.kinds } + | P.KOpt_kind (k, v) -> + let v = to_ast_var v in + let k = to_ast_kind k in + KOpt_kind (k, v), { ctx with kinds = KBindings.add v (unaux_kind k) ctx.kinds } + in + QI_aux (QI_id (KOpt_aux (aux, kopt_l)), l), ctx + +let to_ast_typquant ctx (P.TypQ_aux (aux, l)) = + match aux with + | P.TypQ_no_forall -> TypQ_aux (TypQ_no_forall, l), ctx + | P.TypQ_tq quants -> + let quants, ctx = + List.fold_left (fun (qis, ctx) qi -> let qi', ctx = to_ast_quant_item ctx qi in qi' :: qis, ctx) ([], ctx) quants + in + TypQ_aux (TypQ_tq (List.rev quants), l), ctx + +let to_ast_typschm ctx (P.TypSchm_aux (P.TypSchm_ts (typq, typ), l)) = + let typq, ctx = to_ast_typquant ctx typq in + let typ = to_ast_typ ctx typ in + TypSchm_aux (TypSchm_ts (typq, typ), l), ctx + +let to_ast_lit (P.L_aux (lit, l)) = + L_aux ((match lit with + | P.L_unit -> L_unit + | P.L_zero -> L_zero + | P.L_one -> L_one + | P.L_true -> L_true + | P.L_false -> L_false + | P.L_undef -> L_undef + | P.L_num i -> L_num i + | P.L_hex h -> L_hex h + | P.L_bin b -> L_bin b + | P.L_real r -> L_real r + | P.L_string s -> L_string s) + ,l) + +let rec to_ast_typ_pat (P.ATyp_aux (aux, l)) = + match aux with + | P.ATyp_wild -> TP_aux (TP_wild, l) + | P.ATyp_var kid -> TP_aux (TP_var (to_ast_var kid), l) + | P.ATyp_app (P.Id_aux (P.Id "int", il), typs) -> + TP_aux (TP_app (Id_aux (Id "atom", il), List.map to_ast_typ_pat typs), l) + | P.ATyp_app (f, typs) -> + TP_aux (TP_app (to_ast_id f, List.map to_ast_typ_pat typs), l) + | _ -> raise (Reporting.err_typ l "Unexpected type in type pattern") + +let rec to_ast_pat ctx (P.P_aux (pat, l)) = + P_aux ((match pat with + | P.P_lit lit -> P_lit (to_ast_lit lit) + | P.P_wild -> P_wild + | P.P_or (pat1, pat2) -> + P_or (to_ast_pat ctx pat1, to_ast_pat ctx pat2) + | P.P_var (pat, P.ATyp_aux (P.ATyp_id id, _)) -> + P_as (to_ast_pat ctx pat, to_ast_id id) + | P.P_typ (typ, pat) -> P_typ (to_ast_typ ctx typ, to_ast_pat ctx pat) + | P.P_id id -> P_id (to_ast_id id) + | P.P_var (pat, typ) -> P_var (to_ast_pat ctx pat, to_ast_typ_pat typ) + | P.P_app (id, []) -> P_id (to_ast_id id) + | P.P_app (id, pats) -> + if List.length pats == 1 && string_of_parse_id id = "~" + then P_not (to_ast_pat ctx (List.hd pats)) + else P_app (to_ast_id id, List.map (to_ast_pat ctx) pats) + | P.P_record(fpats,_) -> + P_record(List.map + (fun (P.FP_aux(P.FP_Fpat(id,fp),l)) -> + FP_aux(FP_Fpat(to_ast_id id, to_ast_pat ctx fp),(l,()))) + fpats, false) + | P.P_vector(pats) -> P_vector(List.map (to_ast_pat ctx) pats) + | P.P_vector_concat(pats) -> P_vector_concat(List.map (to_ast_pat ctx) pats) + | P.P_tup(pats) -> P_tup(List.map (to_ast_pat ctx) pats) + | P.P_list(pats) -> P_list(List.map (to_ast_pat ctx) pats) + | P.P_cons(pat1, pat2) -> P_cons (to_ast_pat ctx pat1, to_ast_pat ctx pat2) + | P.P_string_append pats -> P_string_append (List.map (to_ast_pat ctx) pats) + ), (l,())) + +let rec to_ast_letbind ctx (P.LB_aux(lb,l) : P.letbind) : unit letbind = LB_aux( (match lb with - | Parse_ast.LB_val(pat,exp) -> - LB_val(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp) + | P.LB_val(pat,exp) -> + LB_val(to_ast_pat ctx pat, to_ast_exp ctx exp) ), (l,())) -and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit exp = +and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) = E_aux( (match exp with - | Parse_ast.E_block(exps) -> - (match to_ast_fexps false k_env def_ord exps with + | P.E_block(exps) -> + (match to_ast_fexps false ctx exps with | Some(fexps) -> E_record(fexps) - | None -> E_block(List.map (to_ast_exp k_env def_ord) exps)) - | Parse_ast.E_nondet(exps) -> E_nondet(List.map (to_ast_exp k_env def_ord) exps) - | Parse_ast.E_id(id) -> E_id(to_ast_id id) - | Parse_ast.E_ref(id) -> E_ref(to_ast_id id) - | Parse_ast.E_lit(lit) -> E_lit(to_ast_lit lit) - | Parse_ast.E_cast(typ,exp) -> E_cast(to_ast_typ k_env def_ord typ, to_ast_exp k_env def_ord exp) - | Parse_ast.E_app(f,args) -> - (match List.map (to_ast_exp k_env def_ord) args with + | None -> E_block(List.map (to_ast_exp ctx) exps)) + | P.E_nondet(exps) -> E_nondet(List.map (to_ast_exp ctx) exps) + | P.E_id(id) -> E_id(to_ast_id id) + | P.E_ref(id) -> E_ref(to_ast_id id) + | P.E_lit(lit) -> E_lit(to_ast_lit lit) + | P.E_cast(typ,exp) -> E_cast(to_ast_typ ctx typ, to_ast_exp ctx exp) + | P.E_app(f,args) -> + (match List.map (to_ast_exp ctx) args with | [] -> E_app(to_ast_id f, []) | exps -> E_app(to_ast_id f, exps)) - | Parse_ast.E_app_infix(left,op,right) -> - E_app_infix(to_ast_exp k_env def_ord left, to_ast_id op, to_ast_exp k_env def_ord right) - | Parse_ast.E_tuple(exps) -> E_tuple(List.map (to_ast_exp k_env def_ord) exps) - | Parse_ast.E_if(e1,e2,e3) -> E_if(to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2, to_ast_exp k_env def_ord e3) - | Parse_ast.E_for(id,e1,e2,e3,atyp,e4) -> - E_for(to_ast_id id,to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2, - to_ast_exp k_env def_ord e3,to_ast_order k_env def_ord atyp, to_ast_exp k_env def_ord e4) - | Parse_ast.E_loop (Parse_ast.While, e1, e2) -> E_loop (While, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2) - | Parse_ast.E_loop (Parse_ast.Until, e1, e2) -> E_loop (Until, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2) - | Parse_ast.E_vector(exps) -> E_vector(List.map (to_ast_exp k_env def_ord) exps) - | Parse_ast.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp k_env def_ord vexp, to_ast_exp k_env def_ord exp) - | Parse_ast.E_vector_subrange(vex,exp1,exp2) -> - E_vector_subrange(to_ast_exp k_env def_ord vex, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) - | Parse_ast.E_vector_update(vex,exp1,exp2) -> - E_vector_update(to_ast_exp k_env def_ord vex, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) - | Parse_ast.E_vector_update_subrange(vex,e1,e2,e3) -> - E_vector_update_subrange(to_ast_exp k_env def_ord vex, to_ast_exp k_env def_ord e1, - to_ast_exp k_env def_ord e2, to_ast_exp k_env def_ord e3) - | Parse_ast.E_vector_append(e1,e2) -> E_vector_append(to_ast_exp k_env def_ord e1,to_ast_exp k_env def_ord e2) - | Parse_ast.E_list(exps) -> E_list(List.map (to_ast_exp k_env def_ord) exps) - | Parse_ast.E_cons(e1,e2) -> E_cons(to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2) - | Parse_ast.E_record fexps -> - (match to_ast_fexps true k_env def_ord fexps with + | P.E_app_infix(left,op,right) -> + E_app_infix(to_ast_exp ctx left, to_ast_id op, to_ast_exp ctx right) + | P.E_tuple(exps) -> E_tuple(List.map (to_ast_exp ctx) exps) + | P.E_if(e1,e2,e3) -> E_if(to_ast_exp ctx e1, to_ast_exp ctx e2, to_ast_exp ctx e3) + | P.E_for(id,e1,e2,e3,atyp,e4) -> + E_for(to_ast_id id,to_ast_exp ctx e1, to_ast_exp ctx e2, + to_ast_exp ctx e3,to_ast_order ctx atyp, to_ast_exp ctx e4) + | P.E_loop (P.While, e1, e2) -> E_loop (While, to_ast_exp ctx e1, to_ast_exp ctx e2) + | P.E_loop (P.Until, e1, e2) -> E_loop (Until, to_ast_exp ctx e1, to_ast_exp ctx e2) + | P.E_vector(exps) -> E_vector(List.map (to_ast_exp ctx) exps) + | P.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp ctx vexp, to_ast_exp ctx exp) + | P.E_vector_subrange(vex,exp1,exp2) -> + E_vector_subrange(to_ast_exp ctx vex, to_ast_exp ctx exp1, to_ast_exp ctx exp2) + | P.E_vector_update(vex,exp1,exp2) -> + E_vector_update(to_ast_exp ctx vex, to_ast_exp ctx exp1, to_ast_exp ctx exp2) + | P.E_vector_update_subrange(vex,e1,e2,e3) -> + E_vector_update_subrange(to_ast_exp ctx vex, to_ast_exp ctx e1, + to_ast_exp ctx e2, to_ast_exp ctx e3) + | P.E_vector_append(e1,e2) -> E_vector_append(to_ast_exp ctx e1,to_ast_exp ctx e2) + | P.E_list(exps) -> E_list(List.map (to_ast_exp ctx) exps) + | P.E_cons(e1,e2) -> E_cons(to_ast_exp ctx e1, to_ast_exp ctx e2) + | P.E_record fexps -> + (match to_ast_fexps true ctx fexps with | Some fexps -> E_record fexps | None -> raise (Reporting.err_unreachable l __POS__ "to_ast_fexps with true returned none")) - | Parse_ast.E_record_update(exp,fexps) -> - (match to_ast_fexps true k_env def_ord fexps with - | Some(fexps) -> E_record_update(to_ast_exp k_env def_ord exp, fexps) + | P.E_record_update(exp,fexps) -> + (match to_ast_fexps true ctx fexps with + | Some(fexps) -> E_record_update(to_ast_exp ctx exp, fexps) | _ -> raise (Reporting.err_unreachable l __POS__ "to_ast_fexps with true returned none")) - | Parse_ast.E_field(exp,id) -> E_field(to_ast_exp k_env def_ord exp, to_ast_id id) - | Parse_ast.E_case(exp,pexps) -> E_case(to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps) - | Parse_ast.E_try (exp, pexps) -> E_try (to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps) - | Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env def_ord leb, to_ast_exp k_env def_ord exp) - | Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp) - | Parse_ast.E_var(lexp,exp1,exp2) -> E_var(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) - | Parse_ast.E_sizeof(nexp) -> E_sizeof(to_ast_nexp k_env nexp) - | Parse_ast.E_constraint nc -> E_constraint (to_ast_nexp_constraint k_env nc) - | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env def_ord exp) - | Parse_ast.E_throw exp -> E_throw (to_ast_exp k_env def_ord exp) - | Parse_ast.E_return exp -> E_return(to_ast_exp k_env def_ord exp) - | Parse_ast.E_assert(cond,msg) -> E_assert(to_ast_exp k_env def_ord cond, to_ast_exp k_env def_ord msg) + | P.E_field(exp,id) -> E_field(to_ast_exp ctx exp, to_ast_id id) + | P.E_case(exp,pexps) -> E_case(to_ast_exp ctx exp, List.map (to_ast_case ctx) pexps) + | P.E_try (exp, pexps) -> E_try (to_ast_exp ctx exp, List.map (to_ast_case ctx) pexps) + | P.E_let(leb,exp) -> E_let(to_ast_letbind ctx leb, to_ast_exp ctx exp) + | P.E_assign(lexp,exp) -> E_assign(to_ast_lexp ctx lexp, to_ast_exp ctx exp) + | P.E_var(lexp,exp1,exp2) -> E_var(to_ast_lexp ctx lexp, to_ast_exp ctx exp1, to_ast_exp ctx exp2) + | P.E_sizeof(nexp) -> E_sizeof(to_ast_nexp ctx nexp) + | P.E_constraint nc -> E_constraint (to_ast_constraint ctx nc) + | P.E_exit exp -> E_exit(to_ast_exp ctx exp) + | P.E_throw exp -> E_throw (to_ast_exp ctx exp) + | P.E_return exp -> E_return(to_ast_exp ctx exp) + | P.E_assert(cond,msg) -> E_assert(to_ast_exp ctx cond, to_ast_exp ctx msg) | _ -> raise (Reporting.err_unreachable l __POS__ "Unparsable construct in to_ast_exp") ), (l,())) -and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp = +and to_ast_lexp ctx (P.E_aux(exp,l) : P.exp) : unit lexp = let lexp = match exp with - | Parse_ast.E_id id -> LEXP_id (to_ast_id id) - | Parse_ast.E_deref exp -> LEXP_deref (to_ast_exp k_env def_ord exp) - | Parse_ast.E_cast (typ, Parse_ast.E_aux (Parse_ast.E_id id, l')) -> - LEXP_cast (to_ast_typ k_env def_ord typ, to_ast_id id) - | Parse_ast.E_tuple tups -> - let ltups = List.map (to_ast_lexp k_env def_ord) tups in + | P.E_id id -> LEXP_id (to_ast_id id) + | P.E_deref exp -> LEXP_deref (to_ast_exp ctx exp) + | P.E_cast (typ, P.E_aux (P.E_id id, l')) -> + LEXP_cast (to_ast_typ ctx typ, to_ast_id id) + | P.E_tuple tups -> + let ltups = List.map (to_ast_lexp ctx) tups in let is_ok_in_tup (LEXP_aux (le, (l, _))) = match le with | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_vector_concat _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> () | LEXP_memory _ | LEXP_deref _ -> - typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None + raise (Reporting.err_typ l "only identifiers, fields, and vectors may be set in a tuple") in List.iter is_ok_in_tup ltups; LEXP_tup ltups - | Parse_ast.E_app ((Parse_ast.Id_aux (f, l') as f'), args) -> + | P.E_app ((P.Id_aux (f, l') as f'), args) -> begin match f with - | Parse_ast.Id(id) -> - (match List.map (to_ast_exp k_env def_ord) args with + | P.Id(id) -> + (match List.map (to_ast_exp ctx) args with | [E_aux (E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory (to_ast_id f', []) | [E_aux (E_tuple exps,_)] -> LEXP_memory (to_ast_id f', exps) | args -> LEXP_memory(to_ast_id f', args)) - | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None + | _ -> raise (Reporting.err_typ l' "memory call on lefthand side of assignment must begin with an id") end - | Parse_ast.E_vector_append (exp1, exp2) -> - LEXP_vector_concat (to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2) - | Parse_ast.E_vector_access (vexp, exp) -> LEXP_vector (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp) - | Parse_ast.E_vector_subrange (vexp, exp1, exp2) -> - LEXP_vector_range (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) - | Parse_ast.E_field (fexp, id) -> LEXP_field (to_ast_lexp k_env def_ord fexp, to_ast_id id) - | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None + | P.E_vector_append (exp1, exp2) -> + LEXP_vector_concat (to_ast_lexp ctx exp1 :: to_ast_lexp_vector_concat ctx exp2) + | P.E_vector_access (vexp, exp) -> LEXP_vector (to_ast_lexp ctx vexp, to_ast_exp ctx exp) + | P.E_vector_subrange (vexp, exp1, exp2) -> + LEXP_vector_range (to_ast_lexp ctx vexp, to_ast_exp ctx exp1, to_ast_exp ctx exp2) + | P.E_field (fexp, id) -> LEXP_field (to_ast_lexp ctx fexp, to_ast_id id) + | _ -> raise (Reporting.err_typ l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment") in LEXP_aux (lexp, (l, ())) -and to_ast_lexp_vector_concat k_env def_ord (Parse_ast.E_aux (exp_aux, l) as exp) = +and to_ast_lexp_vector_concat ctx (P.E_aux (exp_aux, l) as exp) = match exp_aux with - | Parse_ast.E_vector_append (exp1, exp2) -> - to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2 - | _ -> [to_ast_lexp k_env def_ord exp] + | P.E_vector_append (exp1, exp2) -> + to_ast_lexp ctx exp1 :: to_ast_lexp_vector_concat ctx exp2 + | _ -> [to_ast_lexp ctx exp] -and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : unit pexp = +and to_ast_case ctx (P.Pat_aux(pex,l) : P.pexp) : unit pexp = match pex with - | Parse_ast.Pat_exp(pat,exp) -> Pat_aux(Pat_exp(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp),(l,())) - | Parse_ast.Pat_when(pat,guard,exp) -> - Pat_aux (Pat_when (to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord guard, to_ast_exp k_env def_ord exp), (l, ())) + | P.Pat_exp(pat,exp) -> Pat_aux(Pat_exp(to_ast_pat ctx pat, to_ast_exp ctx exp),(l,())) + | P.Pat_when(pat,guard,exp) -> + Pat_aux (Pat_when (to_ast_pat ctx pat, to_ast_exp ctx guard, to_ast_exp ctx exp), (l, ())) -and to_ast_fexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps : Parse_ast.exp list) : unit fexp list option = +and to_ast_fexps (fail_on_error:bool) ctx (exps : P.exp list) : unit fexp list option = match exps with | [] -> Some [] - | fexp::exps -> let maybe_fexp,maybe_error = to_ast_record_try k_env def_ord fexp in + | fexp::exps -> let maybe_fexp,maybe_error = to_ast_record_try ctx fexp in (match maybe_fexp,maybe_error with | Some(fexp),None -> - (match (to_ast_fexps fail_on_error k_env def_ord exps) with + (match (to_ast_fexps fail_on_error ctx exps) with | Some(fexps) -> Some(fexp::fexps) | _ -> None) | None,Some(l,msg) -> if fail_on_error - then typ_error l msg None None None + then raise (Reporting.err_typ l msg) else None | _ -> None) -and to_ast_record_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp,l):Parse_ast.exp): unit fexp option * (l * string) option = +and to_ast_record_try ctx (P.E_aux(exp,l):P.exp): unit fexp option * (l * string) option = match exp with - | Parse_ast.E_app_infix(left,op,r) -> + | P.E_app_infix(left,op,r) -> (match left, op with - | Parse_ast.E_aux(Parse_ast.E_id(id),li), Parse_ast.Id_aux(Parse_ast.Id("="),leq) -> - Some(FE_aux(FE_Fexp(to_ast_id id, to_ast_exp k_env def_ord r), (l,()))),None - | Parse_ast.E_aux(_,li) , Parse_ast.Id_aux(Parse_ast.Id("="),leq) -> + | P.E_aux(P.E_id(id),li), P.Id_aux(P.Id("="),leq) -> + Some(FE_aux(FE_Fexp(to_ast_id id, to_ast_exp ctx r), (l,()))),None + | P.E_aux(_,li) , P.Id_aux(P.Id("="),leq) -> None,Some(li,"Expected an identifier to begin this field assignment") - | Parse_ast.E_aux(Parse_ast.E_id(id),li), Parse_ast.Id_aux(_,leq) -> + | P.E_aux(P.E_id(id),li), P.Id_aux(_,leq) -> None,Some(leq,"Expected a field assignment to be identifier = expression") - | Parse_ast.E_aux(_,li),Parse_ast.Id_aux(_,leq) -> + | P.E_aux(_,li),P.Id_aux(_,leq) -> None,Some(l,"Expected a field assignment to be identifier = expression")) | _ -> - None,Some(l, "Expected a field assignment to be identifier = expression") + None,Some(l, "Expected a field assignment to be identifier = expression") + +type 'a ctx_out = 'a * ctx -let to_ast_default (names, k_env, default_order) (default : Parse_ast.default_typing_spec) : default_spec envs_out = +let to_ast_default ctx (default : P.default_typing_spec) : default_spec ctx_out = match default with - | Parse_ast.DT_aux(Parse_ast.DT_order(k,o),l) -> - let k,k_typ = to_ast_kind k in - (match (k,o) with - | (K_aux(K_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_inc,lo)) -> - let default_order = Ord_aux(Ord_inc,lo) in - DT_aux(DT_order default_order,l),(names,k_env,default_order) - | (K_aux(K_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_dec,lo)) -> - let default_order = Ord_aux(Ord_dec,lo) in - DT_aux(DT_order default_order,l),(names,k_env,default_order) - | _ -> typ_error l "Inc and Dec must have kind Order" None None None) - -let to_ast_spec (names,k_env,default_order) (val_:Parse_ast.val_spec) : (unit val_spec) envs_out = + | P.DT_aux(P.DT_order(k,o),l) -> + let k = to_ast_kind k in + match (k,o) with + | K_aux(K_order, _), P.ATyp_aux(P.ATyp_inc,lo) -> + let default_order = Ord_aux(Ord_inc,lo) in + DT_aux(DT_order default_order,l),ctx + | K_aux(K_order, _), P.ATyp_aux(P.ATyp_dec,lo) -> + let default_order = Ord_aux(Ord_dec,lo) in + DT_aux(DT_order default_order,l),ctx + | _ -> raise (Reporting.err_typ l "Inc and Dec must have kind Order") + +let to_ast_spec ctx (val_:P.val_spec) : (unit val_spec) ctx_out = match val_ with - | Parse_ast.VS_aux(vs,l) -> + | P.VS_aux(vs,l) -> (match vs with - | Parse_ast.VS_val_spec(ts,id,ext,is_cast) -> - let typsch,_,_ = to_ast_typschm k_env default_order ts in - VS_aux(VS_val_spec(typsch,to_ast_id id,ext,is_cast),(l,())),(names,k_env,default_order)) + | P.VS_val_spec(ts,id,ext,is_cast) -> + let typschm, _ = to_ast_typschm ctx ts in + VS_aux(VS_val_spec(typschm,to_ast_id id,ext,is_cast),(l,())),ctx) -let to_ast_namescm (Parse_ast.Name_sect_aux(ns,l)) = +let to_ast_namescm (P.Name_sect_aux(ns,l)) = Name_sect_aux( (match ns with - | Parse_ast.Name_sect_none -> Name_sect_none - | Parse_ast.Name_sect_some(s) -> Name_sect_some(s) + | P.Name_sect_none -> Name_sect_none + | P.Name_sect_some(s) -> Name_sect_some(s) ),l) -let rec to_ast_range (Parse_ast.BF_aux(r,l)) = (* TODO add check that ranges are sensible for some definition of sensible *) +let rec to_ast_range (P.BF_aux(r,l)) = (* TODO add check that ranges are sensible for some definition of sensible *) BF_aux( (match r with - | Parse_ast.BF_single(i) -> BF_single(i) - | Parse_ast.BF_range(i1,i2) -> BF_range(i1,i2) - | Parse_ast.BF_concat(ir1,ir2) -> BF_concat( to_ast_range ir1, to_ast_range ir2)), + | P.BF_single(i) -> BF_single(i) + | P.BF_range(i1,i2) -> BF_range(i1,i2) + | P.BF_concat(ir1,ir2) -> BF_concat( to_ast_range ir1, to_ast_range ir2)), l) -let to_ast_type_union k_env default_order (Parse_ast.Tu_aux (Parse_ast.Tu_ty_id (atyp, id), l)) = - let typ = to_ast_typ k_env default_order atyp in +let to_ast_type_union ctx (P.Tu_aux (P.Tu_ty_id (atyp, id), l)) = + let typ = to_ast_typ ctx atyp in Tu_aux (Tu_ty_id (typ, to_ast_id id), l) -let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (unit type_def) envs_out = - match td with - | Parse_ast.TD_aux(td,l) -> - (match td with - | Parse_ast.TD_abbrev(id,name_scm_opt,typschm) -> - let id = to_ast_id id in - let key = id_to_string id in - let typschm,k_env,_ = to_ast_typschm k_env def_ord typschm in - let td_abrv = TD_aux(TD_abbrev(id,to_ast_namescm name_scm_opt,typschm),(l,())) in - let typ = (match typschm with - | TypSchm_aux(TypSchm_ts(tq,typ), _) -> - begin match (typquant_to_quantkinds k_env tq) with - | [] -> {k = K_Typ} - | typs -> {k= K_Lam(typs,{k=K_Typ})} - end) in - td_abrv,(names,Envmap.insert k_env (key,typ),def_ord) - | Parse_ast.TD_record(id,name_scm_opt,typq,fields,_) -> - let id = to_ast_id id in - let key = id_to_string id in - let typq,k_env,_ = to_ast_typquant k_env typq in - let fields = List.map (fun (atyp,id) -> (to_ast_typ k_env def_ord atyp),(to_ast_id id)) fields in (* Add check that all arms have unique names locally *) - let td_rec = TD_aux(TD_record(id,to_ast_namescm name_scm_opt,typq,fields,false),(l,())) in - let typ = (match (typquant_to_quantkinds k_env typq) with - | [ ] -> {k = K_Typ} - | typs -> {k = K_Lam(typs,{k=K_Typ})}) in - td_rec, (names,Envmap.insert k_env (key,typ), def_ord) - | Parse_ast.TD_variant(id,name_scm_opt,typq,arms,_) -> - let id = to_ast_id id in - let key = id_to_string id in - let typq,k_env,_ = to_ast_typquant k_env typq in - let arms = List.map (to_ast_type_union k_env def_ord) arms in (* Add check that all arms have unique names *) - let td_var = TD_aux(TD_variant(id,to_ast_namescm name_scm_opt,typq,arms,false),(l,())) in - let typ = (match (typquant_to_quantkinds k_env typq) with - | [ ] -> {k = K_Typ} - | typs -> {k = K_Lam(typs,{k=K_Typ})}) in - td_var, (names,Envmap.insert k_env (key,typ), def_ord) - | Parse_ast.TD_enum(id,name_scm_opt,enums,_) -> - let id = to_ast_id id in - let key = id_to_string id in - let enums = List.map to_ast_id enums in - let keys = List.map id_to_string enums in - let td_enum = TD_aux(TD_enum(id,to_ast_namescm name_scm_opt,enums,false),(l,())) in (* Add check that all enums have unique names *) - let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in - td_enum, (names,k_env,def_ord) - | Parse_ast.TD_bitfield(id,typ,ranges) -> - let id = to_ast_id id in - let key = id_to_string id in - let typ = to_ast_typ k_env def_ord typ in - let ranges = List.map (fun (id, range) -> (to_ast_id id, to_ast_range range)) ranges in - TD_aux(TD_bitfield(id,typ,ranges),(l,())), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord)) - -let to_ast_kdef (names, k_env, def_ord) (td:Parse_ast.kind_def) : unit kind_def = +let kopt_kind (KOpt_aux (aux, l)) = + match aux with + | KOpt_none _ -> K_aux (K_int, gen_loc l) + | KOpt_kind (k, _) -> k + +let add_constructor id typq ctx = + let kinds = List.map (fun kopt -> unaux_kind (kopt_kind kopt)) (quant_kopts typq) in + { ctx with type_constructors = Bindings.add id kinds ctx.type_constructors } + +let to_ast_typedef ctx (P.TD_aux (aux, l) : P.type_def) : unit type_def ctx_out = + let aux, ctx = match aux with + | P.TD_abbrev (id, namescm_opt, P.TypSchm_aux (P.TypSchm_ts (typq, typ), l)) -> + let id = to_ast_id id in + let typq, typq_ctx = to_ast_typquant ctx typq in + let typ = to_ast_typ typq_ctx typ in + TD_abbrev (id, to_ast_namescm namescm_opt, TypSchm_aux (TypSchm_ts (typq, typ), l)), + add_constructor id typq ctx + + | P.TD_record (id, namescm_opt, typq, fields, _) -> + let id = to_ast_id id in + let typq, typq_ctx = to_ast_typquant ctx typq in + let fields = List.map (fun (atyp, id) -> to_ast_typ typq_ctx atyp, to_ast_id id) fields in + TD_record (id, to_ast_namescm namescm_opt, typq, fields, false), + add_constructor id typq ctx + + | P.TD_variant (id, namescm_opt, typq, arms, _) -> + let id = to_ast_id id in + let typq, typq_ctx = to_ast_typquant ctx typq in + let arms = List.map (to_ast_type_union typq_ctx) arms in + TD_variant (id, to_ast_namescm namescm_opt, typq, arms, false), + add_constructor id typq ctx + + | P.TD_enum (id, namescm_opt, enums, _) -> + let id = to_ast_id id in + let enums = List.map to_ast_id enums in + TD_enum (id, to_ast_namescm namescm_opt, enums, false), + { ctx with type_constructors = Bindings.add id [] ctx.type_constructors } + + | P.TD_bitfield (id, typ, ranges) -> + let id = to_ast_id id in + let typ = to_ast_typ ctx typ in + let ranges = List.map (fun (id, range) -> (to_ast_id id, to_ast_range range)) ranges in + TD_bitfield (id, typ, ranges), + { ctx with type_constructors = Bindings.add id [] ctx.type_constructors } + in + TD_aux (aux, (l, ())), ctx + +let to_ast_kdef ctx (td:P.kind_def) : unit kind_def = match td with - | Parse_ast.KD_aux (Parse_ast.KD_nabbrev (kind, id, name_scm_opt, atyp), l) -> + | P.KD_aux (P.KD_nabbrev (kind, id, name_scm_opt, atyp), l) -> let id = to_ast_id id in - let (kind, k) = to_ast_kind kind in - KD_aux (KD_nabbrev (kind, id, to_ast_namescm name_scm_opt, to_ast_nexp k_env atyp), (l, ())) + let kind = to_ast_kind kind in + KD_aux (KD_nabbrev (kind, id, to_ast_namescm name_scm_opt, to_ast_nexp ctx atyp), (l, ())) -let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt = +let to_ast_rec (P.Rec_aux(r,l): P.rec_opt) : rec_opt = Rec_aux((match r with - | Parse_ast.Rec_nonrec -> Rec_nonrec - | Parse_ast.Rec_rec -> Rec_rec + | P.Rec_nonrec -> Rec_nonrec + | P.Rec_rec -> Rec_rec ),l) -let to_ast_tannot_opt (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.Typ_annot_opt_aux(tp,l)):tannot_opt * kind Envmap.t * kind Envmap.t= +let to_ast_tannot_opt ctx (P.Typ_annot_opt_aux(tp,l)) : tannot_opt ctx_out = match tp with - | Parse_ast.Typ_annot_opt_none -> - Typ_annot_opt_aux (Typ_annot_opt_none, l), k_env, Envmap.empty - | Parse_ast.Typ_annot_opt_some(tq,typ) -> - let typq,k_env,k_local = to_ast_typquant k_env tq in - Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env def_ord typ),l),k_env,k_local + | P.Typ_annot_opt_none -> + Typ_annot_opt_aux (Typ_annot_opt_none, l), ctx + | P.Typ_annot_opt_some(tq,typ) -> + let typq, ctx = to_ast_typquant ctx tq in + Typ_annot_opt_aux (Typ_annot_opt_some(typq,to_ast_typ ctx typ),l),ctx -let to_ast_typschm_opt (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.TypSchm_opt_aux(aux,l)) : tannot_opt * kind Envmap.t * kind Envmap.t = +let to_ast_typschm_opt ctx (P.TypSchm_opt_aux(aux,l)) : tannot_opt ctx_out = match aux with - | Parse_ast.TypSchm_opt_none -> - Typ_annot_opt_aux (Typ_annot_opt_none, l), k_env, Envmap.empty - | Parse_ast.TypSchm_opt_some (Parse_ast.TypSchm_aux (Parse_ast.TypSchm_ts (tq, typ), l)) -> - let typq, k_env, k_local = to_ast_typquant k_env tq in - Typ_annot_opt_aux (Typ_annot_opt_some (typq, to_ast_typ k_env def_ord typ), l), k_env, k_local + | P.TypSchm_opt_none -> + Typ_annot_opt_aux (Typ_annot_opt_none, l), ctx + | P.TypSchm_opt_some (P.TypSchm_aux (P.TypSchm_ts (tq, typ), l)) -> + let typq, ctx = to_ast_typquant ctx tq in + Typ_annot_opt_aux (Typ_annot_opt_some (typq, to_ast_typ ctx typ), l), ctx - -let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) : effect_opt = +let to_ast_effects_opt (P.Effect_opt_aux(e,l)) : effect_opt = match e with - | Parse_ast.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l) - | Parse_ast.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects k_env typ),l) + | P.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l) + | P.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects typ),l) -let to_ast_funcl (names,k_env,def_ord) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (unit funcl) = - (*let _ = Printf.eprintf "to_ast_funcl\n" in*) +let to_ast_funcl ctx (P.FCL_aux(fcl,l) : P.funcl) : (unit funcl) = match fcl with - | Parse_ast.FCL_Funcl(id,pexp) -> - FCL_aux(FCL_Funcl(to_ast_id id, to_ast_case k_env def_ord pexp),(l,())) + | P.FCL_Funcl(id,pexp) -> + FCL_aux(FCL_Funcl(to_ast_id id, to_ast_case ctx pexp),(l,())) -let to_ast_fundef (names,k_env,def_ord) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef) : (unit fundef) envs_out = +let to_ast_fundef ctx (P.FD_aux(fd,l):P.fundef) : unit fundef = match fd with - | Parse_ast.FD_function(rec_opt,tannot_opt,effects_opt,funcls) -> - (*let _ = Printf.eprintf "to_ast_fundef\n" in*) - let tannot_opt, k_env,_ = to_ast_tannot_opt k_env def_ord tannot_opt in - FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, def_ord)) funcls), (l,())), (names,k_env,def_ord) + | P.FD_function(rec_opt,tannot_opt,effects_opt,funcls) -> + let tannot_opt, ctx = to_ast_tannot_opt ctx tannot_opt in + FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt effects_opt, List.map (to_ast_funcl ctx) funcls), (l,())) -let rec to_ast_mpat k_env def_ord (Parse_ast.MP_aux(mpat,l)) = +let rec to_ast_mpat ctx (P.MP_aux(mpat,l)) = MP_aux( (match mpat with - | Parse_ast.MP_lit(lit) -> MP_lit(to_ast_lit lit) - | Parse_ast.MP_id(id) -> MP_id(to_ast_id id) - | Parse_ast.MP_as (mpat, id) -> MP_as (to_ast_mpat k_env def_ord mpat, to_ast_id id) - | Parse_ast.MP_app(id,mpats) -> + | P.MP_lit(lit) -> MP_lit(to_ast_lit lit) + | P.MP_id(id) -> MP_id(to_ast_id id) + | P.MP_as (mpat, id) -> MP_as (to_ast_mpat ctx mpat, to_ast_id id) + | P.MP_app(id,mpats) -> if mpats = [] then MP_id (to_ast_id id) - else MP_app(to_ast_id id, List.map (to_ast_mpat k_env def_ord) mpats) - | Parse_ast.MP_record(mfpats,_) -> + else MP_app(to_ast_id id, List.map (to_ast_mpat ctx) mpats) + | P.MP_record(mfpats,_) -> MP_record(List.map - (fun (Parse_ast.MFP_aux(Parse_ast.MFP_mpat(id,mfp),l)) -> - MFP_aux(MFP_mpat(to_ast_id id, to_ast_mpat k_env def_ord mfp),(l,()))) + (fun (P.MFP_aux(P.MFP_mpat(id,mfp),l)) -> + MFP_aux(MFP_mpat(to_ast_id id, to_ast_mpat ctx mfp),(l,()))) mfpats, false) - | Parse_ast.MP_vector(mpats) -> MP_vector(List.map (to_ast_mpat k_env def_ord) mpats) - | Parse_ast.MP_vector_concat(mpats) -> MP_vector_concat(List.map (to_ast_mpat k_env def_ord) mpats) - | Parse_ast.MP_tup(mpats) -> MP_tup(List.map (to_ast_mpat k_env def_ord) mpats) - | Parse_ast.MP_list(mpats) -> MP_list(List.map (to_ast_mpat k_env def_ord) mpats) - | Parse_ast.MP_cons(pat1, pat2) -> MP_cons (to_ast_mpat k_env def_ord pat1, to_ast_mpat k_env def_ord pat2) - | Parse_ast.MP_string_append pats -> MP_string_append (List.map (to_ast_mpat k_env def_ord) pats) - | Parse_ast.MP_typ (mpat, typ) -> MP_typ (to_ast_mpat k_env def_ord mpat, to_ast_typ k_env def_ord typ) + | P.MP_vector(mpats) -> MP_vector(List.map (to_ast_mpat ctx) mpats) + | P.MP_vector_concat(mpats) -> MP_vector_concat(List.map (to_ast_mpat ctx) mpats) + | P.MP_tup(mpats) -> MP_tup(List.map (to_ast_mpat ctx) mpats) + | P.MP_list(mpats) -> MP_list(List.map (to_ast_mpat ctx) mpats) + | P.MP_cons(pat1, pat2) -> MP_cons (to_ast_mpat ctx pat1, to_ast_mpat ctx pat2) + | P.MP_string_append pats -> MP_string_append (List.map (to_ast_mpat ctx) pats) + | P.MP_typ (mpat, typ) -> MP_typ (to_ast_mpat ctx mpat, to_ast_typ ctx typ) ), (l,())) - -let to_ast_mpexp (names,k_env,def_ord) (Parse_ast.MPat_aux(mpexp, l)) = +let to_ast_mpexp ctx (P.MPat_aux(mpexp, l)) = match mpexp with - | Parse_ast.MPat_pat mpat -> MPat_aux (MPat_pat (to_ast_mpat k_env def_ord mpat), (l, ())) - | Parse_ast.MPat_when (mpat, exp) -> MPat_aux (MPat_when (to_ast_mpat k_env def_ord mpat, to_ast_exp k_env def_ord exp), (l, ())) + | P.MPat_pat mpat -> MPat_aux (MPat_pat (to_ast_mpat ctx mpat), (l, ())) + | P.MPat_when (mpat, exp) -> MPat_aux (MPat_when (to_ast_mpat ctx mpat, to_ast_exp ctx exp), (l, ())) -let to_ast_mapcl (names,k_env,def_ord) (Parse_ast.MCL_aux(mapcl, l)) = +let to_ast_mapcl ctx (P.MCL_aux(mapcl, l)) = match mapcl with - | Parse_ast.MCL_bidir (mpexp1, mpexp2) -> MCL_aux (MCL_bidir (to_ast_mpexp (names,k_env,def_ord) mpexp1, to_ast_mpexp (names,k_env,def_ord) mpexp2), (l, ())) - | Parse_ast.MCL_forwards (mpexp, exp) -> MCL_aux (MCL_forwards (to_ast_mpexp (names,k_env,def_ord) mpexp, to_ast_exp k_env def_ord exp), (l, ())) - | Parse_ast.MCL_backwards (mpexp, exp) -> MCL_aux (MCL_backwards (to_ast_mpexp (names,k_env,def_ord) mpexp, to_ast_exp k_env def_ord exp), (l, ())) + | P.MCL_bidir (mpexp1, mpexp2) -> MCL_aux (MCL_bidir (to_ast_mpexp ctx mpexp1, to_ast_mpexp ctx mpexp2), (l, ())) + | P.MCL_forwards (mpexp, exp) -> MCL_aux (MCL_forwards (to_ast_mpexp ctx mpexp, to_ast_exp ctx exp), (l, ())) + | P.MCL_backwards (mpexp, exp) -> MCL_aux (MCL_backwards (to_ast_mpexp ctx mpexp, to_ast_exp ctx exp), (l, ())) -let to_ast_mapdef (names,k_env,def_ord) (Parse_ast.MD_aux(md,l):Parse_ast.mapdef) : (unit mapdef) envs_out = +let to_ast_mapdef ctx (P.MD_aux(md,l):P.mapdef) : unit mapdef = match md with - | Parse_ast.MD_mapping(id, typschm_opt, mapcls) -> - let tannot_opt, k_env, _ = to_ast_typschm_opt k_env def_ord typschm_opt in - MD_aux(MD_mapping(to_ast_id id, tannot_opt, List.map (to_ast_mapcl (names,k_env,def_ord)) mapcls), (l,())), (names,k_env,def_ord) - -type def_progress = - No_def - | Def_place_holder of id * Parse_ast.l - | Finished of unit def - -type partial_def = ((unit def) * bool) ref * kind Envmap.t - -let rec def_in_progress (id : id) (partial_defs : (id * partial_def) list) : partial_def option = - match partial_defs with - | [] -> None - | (n,pd)::defs -> - (match n,id with - | Id_aux(Id(n),_), Id_aux(Id(i),_) -> if (n = i) then Some(pd) else def_in_progress id defs - | _,_ -> def_in_progress id defs) - -let to_ast_alias_spec k_env def_ord (Parse_ast.E_aux(e,le)) = - AL_aux( - (match e with - | Parse_ast.E_field(Parse_ast.E_aux(Parse_ast.E_id id,li), field) -> - AL_subreg(RI_aux(RI_id (to_ast_id id),(li,())),to_ast_id field) - | Parse_ast.E_vector_access(Parse_ast.E_aux(Parse_ast.E_id id,li),range) -> - AL_bit(RI_aux(RI_id (to_ast_id id),(li,())),to_ast_exp k_env def_ord range) - | Parse_ast.E_vector_subrange(Parse_ast.E_aux(Parse_ast.E_id id,li),base,stop) -> - AL_slice(RI_aux(RI_id (to_ast_id id),(li,())),to_ast_exp k_env def_ord base,to_ast_exp k_env def_ord stop) - | Parse_ast.E_vector_append(Parse_ast.E_aux(Parse_ast.E_id first,lf), - Parse_ast.E_aux(Parse_ast.E_id second,ls)) -> - AL_concat(RI_aux(RI_id (to_ast_id first),(lf,())), - RI_aux(RI_id (to_ast_id second),(ls,()))) - | _ -> raise (Reporting.err_unreachable le __POS__ "Found an expression not supported by parser in to_ast_alias_spec") - ), (le,())) - -let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) = - DEC_aux( - (match regdec with - | Parse_ast.DEC_reg(typ,id) -> - DEC_reg(to_ast_typ k_env def_ord typ,to_ast_id id) - | Parse_ast.DEC_config(id,typ,exp) -> - DEC_config(to_ast_id id,to_ast_typ k_env def_ord typ,to_ast_exp k_env def_ord exp) - | Parse_ast.DEC_alias(id,e) -> - DEC_alias(to_ast_id id,to_ast_alias_spec k_env def_ord e) - | Parse_ast.DEC_typ_alias(typ,id,e) -> - DEC_typ_alias(to_ast_typ k_env def_ord typ,to_ast_id id,to_ast_alias_spec k_env def_ord e) - ),(l,())) + | P.MD_mapping(id, typschm_opt, mapcls) -> + let tannot_opt, ctx = to_ast_typschm_opt ctx typschm_opt in + MD_aux(MD_mapping(to_ast_id id, tannot_opt, List.map (to_ast_mapcl ctx) mapcls), (l,())) + +let to_ast_alias_spec ctx (P.E_aux(e, l)) = + AL_aux((match e with + | P.E_field (P.E_aux (P.E_id id, li), field) -> + AL_subreg (RI_aux (RI_id (to_ast_id id), (li, ())), to_ast_id field) + | P.E_vector_access (P.E_aux (P.E_id id, li), range) -> + AL_bit (RI_aux (RI_id (to_ast_id id), (li, ())), to_ast_exp ctx range) + | P.E_vector_subrange(P.E_aux(P.E_id id,li),base,stop) -> + AL_slice (RI_aux (RI_id (to_ast_id id), (li,())), to_ast_exp ctx base, to_ast_exp ctx stop) + | P.E_vector_append (P.E_aux (P.E_id first, lf), P.E_aux (P.E_id second, ls)) -> + AL_concat (RI_aux (RI_id (to_ast_id first), (lf, ())), + RI_aux (RI_id (to_ast_id second), (ls, ()))) + | _ -> raise (Reporting.err_unreachable l __POS__ "Found an expression not supported by parser in to_ast_alias_spec") + ), (l, ())) + +let to_ast_dec ctx (P.DEC_aux(regdec,l)) = + DEC_aux((match regdec with + | P.DEC_reg (typ, id) -> + DEC_reg (to_ast_typ ctx typ, to_ast_id id) + | P.DEC_config (id, typ, exp) -> + DEC_config (to_ast_id id, to_ast_typ ctx typ, to_ast_exp ctx exp) + | P.DEC_alias (id,e) -> + DEC_alias (to_ast_id id, to_ast_alias_spec ctx e) + | P.DEC_typ_alias (typ,id,e) -> + DEC_typ_alias (to_ast_typ ctx typ, to_ast_id id, to_ast_alias_spec ctx e) + ),(l,())) + +let to_ast_scattered ctx (P.SD_aux (aux, l)) = + let aux, ctx = match aux with + | P.SD_function (rec_opt, tannot_opt, effect_opt, id) -> + let tannot_opt, _ = to_ast_tannot_opt ctx tannot_opt in + let effect_opt = to_ast_effects_opt effect_opt in + SD_function (to_ast_rec rec_opt, tannot_opt, effect_opt, to_ast_id id), ctx + | P.SD_funcl funcl -> + SD_funcl (to_ast_funcl ctx funcl), ctx + | P.SD_variant (id, namescm_opt, typq) -> + let id = to_ast_id id in + let typq, typq_ctx = to_ast_typquant ctx typq in + SD_variant (id, to_ast_namescm namescm_opt, typq), + add_constructor id typq { ctx with scattereds = Bindings.add id typq_ctx ctx.scattereds } + | P.SD_unioncl (id, tu) -> + let id = to_ast_id id in + begin match Bindings.find_opt id ctx.scattereds with + | Some typq_ctx -> + let tu = to_ast_type_union typq_ctx tu in + SD_unioncl (id, tu), ctx + | None -> raise (Reporting.err_typ l ("No scattered union declaration found for " ^ string_of_id id)) + end + | P.SD_end id -> SD_end (to_ast_id id), ctx + | P.SD_mapping (id, tannot_opt) -> + let id = to_ast_id id in + let tannot_opt, _ = to_ast_tannot_opt ctx tannot_opt in + SD_mapping (id, tannot_opt), ctx + | P.SD_mapcl (id, mapcl) -> + let id = to_ast_id id in + let mapcl = to_ast_mapcl ctx mapcl in + SD_mapcl (id, mapcl), ctx + in + SD_aux (aux, (l, ())), ctx let to_ast_prec = function - | Parse_ast.Infix -> Infix - | Parse_ast.InfixL -> InfixL - | Parse_ast.InfixR -> InfixR + | P.Infix -> Infix + | P.InfixL -> InfixL + | P.InfixR -> InfixR -let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out * (id * partial_def) list = - let envs = (names,k_env,def_ord) in +let to_ast_def ctx def : unit def ctx_out = match def with - | Parse_ast.DEF_overload(id,ids) -> - ((Finished(DEF_overload(to_ast_id id, List.map to_ast_id ids))),envs),partial_defs - | Parse_ast.DEF_fixity (prec, n, op) -> - ((Finished(DEF_fixity (to_ast_prec prec, n, to_ast_id op)),envs),partial_defs) - | Parse_ast.DEF_kind(k_def) -> - let kd = to_ast_kdef envs k_def in - ((Finished(DEF_kind(kd))),envs),partial_defs - | Parse_ast.DEF_type(t_def) -> - let td,envs = to_ast_typedef envs t_def in - ((Finished(DEF_type(td))),envs),partial_defs - | Parse_ast.DEF_fundef(f_def) -> - let fd,envs = to_ast_fundef envs f_def in - ((Finished(DEF_fundef(fd))),envs),partial_defs - | Parse_ast.DEF_mapdef(m_def) -> - let md, envs = to_ast_mapdef envs m_def in - ((Finished(DEF_mapdef(md))),envs),partial_defs - | Parse_ast.DEF_val(lbind) -> - let lb = to_ast_letbind k_env def_ord lbind in - ((Finished(DEF_val(lb))),envs),partial_defs - | Parse_ast.DEF_spec(val_spec) -> - let vs,envs = to_ast_spec envs val_spec in - ((Finished(DEF_spec(vs))),envs),partial_defs - | Parse_ast.DEF_default(typ_spec) -> - let default,envs = to_ast_default envs typ_spec in - ((Finished(DEF_default(default))),envs),partial_defs - | Parse_ast.DEF_reg_dec(dec) -> - let d = to_ast_dec envs dec in - ((Finished(DEF_reg_dec(d))),envs),partial_defs - | Parse_ast.DEF_pragma (pragma, arg, l) -> - ((Finished(DEF_pragma (pragma, arg, l))), envs), partial_defs - | Parse_ast.DEF_internal_mutrec _ -> + | P.DEF_overload (id, ids) -> + DEF_overload (to_ast_id id, List.map to_ast_id ids), ctx + | P.DEF_fixity (prec, n, op) -> + DEF_fixity (to_ast_prec prec, n, to_ast_id op), ctx + | P.DEF_kind k_def -> + let kd = to_ast_kdef ctx k_def in + DEF_kind kd, ctx + | P.DEF_type(t_def) -> + let td, ctx = to_ast_typedef ctx t_def in + DEF_type td, ctx + | P.DEF_fundef(f_def) -> + let fd = to_ast_fundef ctx f_def in + DEF_fundef fd, ctx + | P.DEF_mapdef(m_def) -> + let md = to_ast_mapdef ctx m_def in + DEF_mapdef md, ctx + | P.DEF_val(lbind) -> + let lb = to_ast_letbind ctx lbind in + DEF_val lb, ctx + | P.DEF_spec(val_spec) -> + let vs,ctx = to_ast_spec ctx val_spec in + DEF_spec vs, ctx + | P.DEF_default(typ_spec) -> + let default,ctx = to_ast_default ctx typ_spec in + DEF_default default, ctx + | P.DEF_reg_dec dec -> + let d = to_ast_dec ctx dec in + DEF_reg_dec d, ctx + | P.DEF_pragma (pragma, arg, l) -> + DEF_pragma (pragma, arg, l), ctx + | P.DEF_internal_mutrec _ -> (* Should never occur because of remove_mutrec *) - typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None - | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,l)) -> - (match sd with - | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) -> - let rec_opt = to_ast_rec rec_opt in - let unit,k_env',k_local = to_ast_tannot_opt k_env def_ord tannot_opt in - let effects_opt = to_ast_effects_opt k_env' effects_opt in - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> let partial_def = ref ((DEF_fundef(FD_aux(FD_function(rec_opt,unit,effects_opt,[]),(l,())))),false) in - (No_def,envs),((id,(partial_def,k_local))::partial_defs) - | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None) - | Parse_ast.SD_scattered_mapping (id, tannot_opt) -> - let id = to_ast_id id in - let unit, k_env ,k_local = to_ast_tannot_opt k_env def_ord tannot_opt in - (match (def_in_progress id partial_defs) with - | None -> let partial_def = ref ((DEF_mapdef(MD_aux(MD_mapping(id, unit, []), (l, ())))), false) in - (No_def,envs),((id,(partial_def,k_local))::partial_defs) - | Some(d,k) -> typ_error l "Scattered mapping definition header name already in use by scattered definition" (Some id) None None) - - | Parse_ast.SD_scattered_mapcl (id, mapcl) -> - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered mapping definition clause does not match any existing mapping definition headers" (Some id) None None - | Some (d, k) -> - (match !d with - | DEF_mapdef(MD_aux(MD_mapping(_,tannot_opt, mcls),ml)),false -> - let (MCL_aux (mapcl_aux, _)) = to_ast_mapcl (names,k_env,def_ord) mapcl in - d := DEF_mapdef(MD_aux(MD_mapping(id, tannot_opt, mcls @ [MCL_aux (mapcl_aux, (l, ()))]), ml)), false; - (No_def,envs),partial_defs - | _, true -> typ_error l "Scattered mapping definition clause extends ended definition" (Some id) None None - | _ -> typ_error l "Scattered mapping definition doesn't match existing definition header" (Some id) None None)) - - | Parse_ast.SD_scattered_funcl(funcl) -> - (match funcl with - | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_),_) -> - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered function definition clause does not match any existing function definition headers" (Some id) None None - | Some(d,k) -> - (* let _ = Printf.eprintf "SD_scattered_funcl processing\n" in - let _ = Envmap.iter (fun v' k -> P rintf.eprintf "%s -> %s\n" v' (kind_to_string k)) k in - let _ = Envmap.iter (fun v' k -> Prin tf.eprintf "%s -> %s\n" v' (kind_to_string k) ) (Envmap.union k k_env) in *) - (match !d with - | DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),false -> - let (FCL_aux (funcl_aux, _)) = to_ast_funcl (names,Envmap.union k k_env,def_ord) funcl in - d:= DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[FCL_aux (funcl_aux, (l, ()))]),fl)),false; - (No_def,envs),partial_defs - | _,true -> typ_error l "Scattered function definition clauses extends ended definition" (Some id) None None - | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None))) - | Parse_ast.SD_scattered_variant(id,naming_scheme_opt,typquant) -> - let id = to_ast_id id in - let name = to_ast_namescm naming_scheme_opt in - let typq, k_env',_ = to_ast_typquant k_env typquant in - let kind = (match (typquant_to_quantkinds k_env' typq) with - | [ ] -> {k = K_Typ} - | typs -> {k = K_Lam(typs,{k=K_Typ})}) in - (match (def_in_progress id partial_defs) with - | None -> let partial_def = ref ((DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,())))),false) in - (Def_place_holder(id,l),(names,Envmap.insert k_env ((id_to_string id),kind),def_ord)),(id,(partial_def,k_env'))::partial_defs - | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None) - | Parse_ast.SD_scattered_unioncl(id,tu) -> - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None - | Some(d,k) -> - (match !d with - | DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)), false -> - d:= DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_ast_type_union k def_ord tu],false),tl)),false; - (No_def,envs),partial_defs - | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None - | _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None)) - | Parse_ast.SD_scattered_end(id) -> - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None - | Some(d,k) -> - (match !d with - | (DEF_type(_) as def),false -> - d:= (def,true); - (No_def,envs),partial_defs - | (DEF_fundef(_) as def),false -> - d:= (def,true); - ((Finished def), envs),partial_defs - | (DEF_mapdef(_) as def),false -> - d := (def,true); - ((Finished def), envs),partial_defs - | _, true -> - typ_error l "Scattered definition ended multiple times" (Some id) None None - | _ -> raise (Reporting.err_unreachable l __POS__ "Something in partial_defs other than fundef and type")))) - -let rec to_ast_defs_helper envs partial_defs = function - | [] -> ([],envs,partial_defs) - | d::ds -> let ((d', envs), partial_defs) = to_ast_def envs partial_defs d in - let (defs,envs,partial_defs) = to_ast_defs_helper envs partial_defs ds in - (match d' with - | Finished def -> (def::defs,envs, partial_defs) - | No_def -> defs,envs,partial_defs - | Def_place_holder(id,l) -> - (match (def_in_progress id partial_defs) with - | None -> - raise - (Reporting.err_unreachable l __POS__ "Id stored in place holder not retrievable from partial defs") - | Some(d,k) -> - if (snd !d) - then (fst !d) :: defs, envs, partial_defs - else typ_error l "Scattered type definition never ended" (Some id) None None)) + raise (Reporting.err_unreachable P.Unknown __POS__ + "Internal mutual block found when processing scattered defs") + | P.DEF_scattered sdef -> + let sdef, ctx = to_ast_scattered ctx sdef in + DEF_scattered sdef, ctx let rec remove_mutrec = function | [] -> [] - | Parse_ast.DEF_internal_mutrec fundefs :: defs -> - List.map (fun fdef -> Parse_ast.DEF_fundef fdef) fundefs @ remove_mutrec defs + | P.DEF_internal_mutrec fundefs :: defs -> + List.map (fun fdef -> P.DEF_fundef fdef) fundefs @ remove_mutrec defs | def :: defs -> def :: remove_mutrec defs -let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (def_ord : order) (Parse_ast.Defs(defs)) = +let to_ast ctx (P.Defs(defs)) = let defs = remove_mutrec defs in - let defs,(_,k_env,def_ord),partial_defs = to_ast_defs_helper (default_names,kind_env,def_ord) [] defs in - List.iter - (fun (id,(d,k)) -> - (match !d with - | (d,false) -> typ_error Parse_ast.Unknown "Scattered definition never ended" (Some id) None None - | (_, true) -> ())) - partial_defs; - (Defs defs),k_env,def_ord - -let initial_kind_env = - Envmap.from_list [ - ("bool", {k = K_Typ}); - ("nat", {k = K_Typ}); - ("int", {k = K_Typ}); - ("uint8", {k = K_Typ}); - ("uint16", {k= K_Typ}); - ("uint32", {k=K_Typ}); - ("uint64", {k=K_Typ}); - ("unit", {k = K_Typ}); - ("bit", {k = K_Typ}); - ("string", {k = K_Typ}); - ("real", {k = K_Typ}); - ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})}); - ("reg", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); - ("register", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); - ("range", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) }); - ("vector", {k = K_Lam( [{k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ); - ("atom", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); - ("option", { k = K_Lam( [{k=K_Typ}], {k=K_Typ}) }); - ("implicit", {k = K_Lam( [{k = K_Nat}], {k=K_Typ})} ); - ("itself", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); - ] - -let exp_of_string order str = + let defs, ctx = + List.fold_left (fun (defs, ctx) def -> let def, ctx = to_ast_def ctx def in (def :: defs, ctx)) ([], ctx) defs + in + Defs (List.rev defs), ctx + +let initial_ctx = { + type_constructors = + List.fold_left (fun m (k, v) -> Bindings.add (mk_id k) v m) Bindings.empty + [ ("bool", []); + ("nat", []); + ("int", []); + ("unit", []); + ("bit", []); + ("string", []); + ("real", []); + ("list", [K_type]); + ("register", [K_type]); + ("range", [K_int; K_int]); + ("vector", [K_int; K_order; K_type]); + ("atom", [K_int]); + ("implicit", [K_int]); + ("itself", [K_int]); + ]; + kinds = KBindings.empty; + scattereds = Bindings.empty; + } + +let exp_of_string str = let exp = Parser.exp_eof Lexer.token (Lexing.from_string str) in - to_ast_exp initial_kind_env order exp + to_ast_exp initial_ctx exp -let typschm_of_string order str = +let typschm_of_string str = let typschm = Parser.typschm_eof Lexer.token (Lexing.from_string str) in - let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in + let typschm, _ = to_ast_typschm initial_ctx typschm in typschm -let extern_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> Some (string_of_id id)), false)) -let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> None), false)) +let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> Some (string_of_id id)), false)) +let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> None), false)) let val_spec_ids (Defs defs) = let val_spec_id (VS_aux (vs_aux, _)) = @@ -1089,7 +801,7 @@ let have_undefined_builtins = ref false let generate_undefineds vs_ids (Defs defs) = let gen_vs id str = - if (IdSet.mem id vs_ids) then [] else [extern_of_string dec_ord id str] + if (IdSet.mem id vs_ids) then [] else [extern_of_string id str] in let undefined_builtins = if !have_undefined_builtins then @@ -1124,7 +836,7 @@ let generate_undefineds vs_ids (Defs defs) = 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 + let typschm = typschm_of_string ("unit -> " ^ string_of_id id ^ " effect {undef}") in [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) (mk_pat (P_lit (mk_lit L_unit))) @@ -1152,7 +864,7 @@ let generate_undefineds vs_ids (Defs defs) = | Tu_aux (Tu_ty_id (typ, id), _) -> (id, [typ]) in let record_arg_typs m (_,typs) = - let m' = + let m' = List.fold_left (fun m typ -> TypMap.add typ (1 + try TypMap.find typ m with Not_found -> 0) m) TypMap.empty typs in TypMap.merge (fun _ x y -> match x,y with Some m, Some n -> Some (max m n) @@ -1208,7 +920,7 @@ let generate_initialize_registers vs_ids (Defs defs) = 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}"; + [val_spec_of_string (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)))]] @@ -1273,11 +985,11 @@ let generate_enum_functions vs_ids (Defs defs) = in Defs (gen_enums defs) -let incremental_k_env = ref initial_kind_env +let incremental_ctx = ref initial_ctx let process_ast order defs = - let ast, k_env, _= to_ast Nameset.empty !incremental_k_env order defs in - incremental_k_env := k_env; + let ast, ctx = to_ast !incremental_ctx defs in + incremental_ctx := ctx; let vs_ids = val_spec_ids ast in if not !opt_undefined_gen then generate_enum_functions vs_ids ast @@ -1289,4 +1001,4 @@ let process_ast order defs = let ast_of_def_string order str = let def = Parser.def_eof Lexer.token (Lexing.from_string str) in - process_ast order (Parse_ast.Defs [def]) + process_ast order (P.Defs [def]) -- cgit v1.2.3