diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 1 | ||||
| -rw-r--r-- | src/ast_util.mli | 1 | ||||
| -rw-r--r-- | src/c_backend.ml | 8 | ||||
| -rw-r--r-- | src/initial_check.ml | 1458 | ||||
| -rw-r--r-- | src/initial_check.mli | 6 | ||||
| -rw-r--r-- | src/isail.ml | 6 | ||||
| -rw-r--r-- | src/monomorphise.ml | 4 | ||||
| -rw-r--r-- | src/parse_ast.ml | 14 | ||||
| -rw-r--r-- | src/parser.mly | 22 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 13 | ||||
| -rw-r--r-- | src/process_file.ml | 1 | ||||
| -rw-r--r-- | src/process_file.mli | 1 | ||||
| -rw-r--r-- | src/rewrites.ml | 5 | ||||
| -rw-r--r-- | src/sail.ml | 1 | ||||
| -rw-r--r-- | src/scattered.ml | 141 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 19 | ||||
| -rw-r--r-- | src/type_check.ml | 50 |
17 files changed, 824 insertions, 927 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 48750ab7..e9153f7a 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -436,6 +436,7 @@ let quant_map_items f = function let unaux_nexp (Nexp_aux (nexp, _)) = nexp let unaux_order (Ord_aux (ord, _)) = ord let unaux_typ (Typ_aux (typ, _)) = typ +let unaux_kind (K_aux (k, _)) = k 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 diff --git a/src/ast_util.mli b/src/ast_util.mli index b6bce7c5..19fc017d 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -96,6 +96,7 @@ val unaux_pat : 'a pat -> 'a pat_aux val unaux_nexp : nexp -> nexp_aux val unaux_order : order -> order_aux val unaux_typ : typ -> typ_aux +val unaux_kind : kind -> kind_aux val untyp_pat : 'a pat -> 'a pat * typ option val uncast_exp : 'a exp -> 'a exp * typ option diff --git a/src/c_backend.ml b/src/c_backend.ml index 2f57a802..fa21f96d 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -3328,8 +3328,8 @@ let instrument_tracing ctx = | cdef -> cdef let bytecode_ast ctx rewrites (Defs defs) = - let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in - let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in + let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in + let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit effect {escape}" in let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in @@ -3370,8 +3370,8 @@ let compile_ast ctx c_includes (Defs defs) = let ctx = { ctx with recursive_functions = recursive_functions } in c_debug (lazy (Util.string_of_list ", " string_of_id (IdSet.elements recursive_functions))); - let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in - let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in + let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in + let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit effect {escape}" in let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in let cdefs = List.concat (List.rev chunks) in 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]) diff --git a/src/initial_check.mli b/src/initial_check.mli index e6b29216..32def316 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -87,7 +87,7 @@ val process_ast : order -> Parse_ast.defs -> unit defs val val_spec_ids : 'a defs -> IdSet.t -val extern_of_string : order -> id -> string -> unit def -val val_spec_of_string : order -> id -> string -> unit def +val extern_of_string : id -> string -> unit def +val val_spec_of_string : id -> string -> unit def -val exp_of_string : order -> string -> unit exp +val exp_of_string : string -> unit exp diff --git a/src/isail.ml b/src/isail.ml index 83bff3f3..195e5940 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -266,7 +266,7 @@ let handle_input' input = Value.output_close (); exit 0 | ":i" | ":infer" -> - let exp = Initial_check.exp_of_string dec_ord arg in + let exp = Initial_check.exp_of_string arg in let exp = Type_check.infer_exp !interactive_env exp in pretty_sail stdout (doc_typ (Type_check.typ_of exp)); print_newline () @@ -370,7 +370,7 @@ let handle_input' input = Initial_check.have_undefined_builtins := false | ":exec" -> let open Bytecode_interpreter in - let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord arg) in + let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string arg) in let anf = Anf.anf exp in let ctx = C_backend.initial_ctx !interactive_env in let ctyp = C_backend.ctyp_of_typ ctx (Type_check.typ_of exp) in @@ -383,7 +383,7 @@ let handle_input' input = | Expression str -> (* An expression in normal mode is type checked, then puts us in evaluation mode. *) - let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord str) in + let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string str) in current_mode := Evaluation (eval_frame (Step (lazy "", !interactive_state, return exp, []))); print_program () | Empty -> () diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 7626971e..41a27be7 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2096,8 +2096,8 @@ let split_defs all_errors splits defs = in let map_scattered_def sd = match sd with - | SD_aux (SD_scattered_funcl fcl, annot) -> - List.map (fun fcl' -> SD_aux (SD_scattered_funcl fcl', annot)) (map_funcl fcl) + | SD_aux (SD_funcl fcl, annot) -> + List.map (fun fcl' -> SD_aux (SD_funcl fcl', annot)) (map_funcl fcl) | _ -> [sd] in let map_def d = diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 38854d48..79d90635 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -494,13 +494,13 @@ dec_spec_aux = (* Register declarations *) type scattered_def_aux = (* Function and type union definitions that can be spread across a file. Each one must end in $_$ *) - SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) - | SD_scattered_funcl of funcl (* scattered function definition clause *) - | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) - | SD_scattered_unioncl of id * type_union (* scattered union definition member *) - | SD_scattered_mapping of id * tannot_opt - | SD_scattered_mapcl of id * mapcl - | SD_scattered_end of id (* scattered definition end *) + SD_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) + | SD_funcl of funcl (* scattered function definition clause *) + | SD_variant of id * name_scm_opt * typquant (* scattered union definition header *) + | SD_unioncl of id * type_union (* scattered union definition member *) + | SD_mapping of id * tannot_opt + | SD_mapcl of id * mapcl + | SD_end of id (* scattered definition end *) type diff --git a/src/parser.mly b/src/parser.mly index fd6c9373..73259210 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -1395,22 +1395,22 @@ default_def: { mk_default (DT_order ($2, mk_typ ATyp_dec $startpos($3) $endpos)) $startpos $endpos } scattered_def: - | Union id typquant - { mk_sd (SD_scattered_variant($2, mk_namesectn, $3)) $startpos $endpos } + | Union id typaram + { mk_sd (SD_variant($2, mk_namesectn, $3)) $startpos $endpos } | Union id - { mk_sd (SD_scattered_variant($2, mk_namesectn, mk_typqn)) $startpos $endpos } + { mk_sd (SD_variant($2, mk_namesectn, mk_typqn)) $startpos $endpos } | Function_ id - { mk_sd (SD_scattered_function(mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos } + { mk_sd (SD_function(mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos } | Mapping id - { mk_sd (SD_scattered_mapping ($2, mk_tannotn)) $startpos $endpos } + { mk_sd (SD_mapping ($2, mk_tannotn)) $startpos $endpos } | Mapping id Colon funcl_typ - { mk_sd (SD_scattered_mapping ($2, $4)) $startpos $endpos } + { mk_sd (SD_mapping ($2, $4)) $startpos $endpos } scattered_clause: | Doc Function_ Clause funcl - { mk_sd_doc (SD_scattered_funcl $4) $1 $startpos($2) $endpos } + { mk_sd_doc (SD_funcl $4) $1 $startpos($2) $endpos } | Function_ Clause funcl - { mk_sd (SD_scattered_funcl $3) $startpos $endpos } + { mk_sd (SD_funcl $3) $startpos $endpos } def: @@ -1437,11 +1437,11 @@ def: | scattered_clause { DEF_scattered $1 } | Union Clause id Eq type_union - { DEF_scattered (mk_sd (SD_scattered_unioncl ($3, $5)) $startpos $endpos) } + { DEF_scattered (mk_sd (SD_unioncl ($3, $5)) $startpos $endpos) } | Mapping Clause id Eq mapcl - { DEF_scattered (mk_sd (SD_scattered_mapcl ($3, $5)) $startpos $endpos) } + { DEF_scattered (mk_sd (SD_mapcl ($3, $5)) $startpos $endpos) } | End id - { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) } + { DEF_scattered (mk_sd (SD_end $2) $startpos $endpos) } | default_def { DEF_default $1 } | Constant id Eq typ diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index b1efd11d..f9908c71 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -613,13 +613,18 @@ let doc_kind_def (KD_aux (KD_nabbrev (_, id, _, nexp), _)) = let rec doc_scattered (SD_aux (sd_aux, _)) = match sd_aux with - | SD_scattered_function (_, _, _, id) -> + | SD_function (_, _, _, id) -> string "scattered" ^^ space ^^ string "function" ^^ space ^^ doc_id id - | SD_scattered_funcl funcl -> + | SD_funcl funcl -> string "function" ^^ space ^^ string "clause" ^^ space ^^ doc_funcl funcl - | SD_scattered_end id -> + | SD_end id -> string "end" ^^ space ^^ doc_id id - | _ -> string "SCATTERED" + | SD_variant (id, _, TypQ_aux (TypQ_no_forall, _)) -> + string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id + | SD_variant (id, _, TypQ_aux (TypQ_tq quants, _)) -> + string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id ^^ doc_param_quants quants + | SD_unioncl (id, tu) -> + separate space [string "union clause"; doc_id id; equals; doc_union tu] let rec doc_def def = group (match def with | DEF_default df -> doc_default df diff --git a/src/process_file.ml b/src/process_file.ml index c3d0be0e..ca013077 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -388,7 +388,6 @@ let rewrite rewriters defs = raise (Reporting.err_typ l (Type_error.string_of_type_error err)) let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)] -let rewrite_undefined bitvectors = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined bitvectors x)] let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_coq let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml diff --git a/src/process_file.mli b/src/process_file.mli index 1ebb3014..1d4d629a 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -56,7 +56,6 @@ val convert_ast : Ast.order -> Parse_ast.defs -> unit Ast.defs val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs val check_ast: Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs -val rewrite_undefined: bool -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_coq : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs diff --git a/src/rewrites.ml b/src/rewrites.ml index 8c1311a0..0ead9670 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -82,7 +82,7 @@ let fresh_id_pat pre ((l,annot)) = let get_loc_exp (E_aux (_,(l,_))) = l -let gen_vs (id, spec) = Initial_check.extern_of_string dec_ord (mk_id id) spec +let gen_vs (id, spec) = Initial_check.extern_of_string (mk_id id) spec let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, mk_tannot env typ effect)) let annot_exp e_aux l env typ = annot_exp_effect e_aux l env typ no_effect @@ -4277,7 +4277,8 @@ let rewrite_defs_realise_mappings (Defs defs) = let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in let effect_pure = (Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown)) in - let env = match mapcls with + (* We need to make sure we get the environment for the last mapping clause *) + let env = match List.rev mapcls with | MCL_aux (_, mapcl_annot) :: _ -> env_of_annot mapcl_annot | _ -> Type_check.typ_error l "mapping with no clauses?" in diff --git a/src/sail.ml b/src/sail.ml index b9a18417..73173946 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -282,6 +282,7 @@ let load_files type_envs files = let (ast, type_envs) = check_ast type_envs ast in Profile.finish "type checking" t; + let ast = Scattered.descatter ast in let ast = rewrite_ast ast in let out_name = match !opt_file_out with diff --git a/src/scattered.ml b/src/scattered.ml new file mode 100644 index 00000000..be304dc8 --- /dev/null +++ b/src/scattered.ml @@ -0,0 +1,141 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util + +let funcl_id (FCL_aux (FCL_Funcl (id, _), _)) = id + +let rec last_scattered_funcl id = function + | DEF_scattered (SD_aux (SD_funcl funcl, _)) :: _ + when Id.compare (funcl_id funcl) id = 0 -> false + | _ :: defs -> last_scattered_funcl id defs + | [] -> true + +let rec last_scattered_mapcl id = function + | DEF_scattered (SD_aux (SD_mapcl (mid, _), _)) :: _ + when Id.compare mid id = 0 -> false + | _ :: defs -> last_scattered_mapcl id defs + | [] -> true + +(* Nothing cares about these and the AST should be changed *) +let fake_effect_opt l = Effect_opt_aux (Effect_opt_pure, gen_loc l) +let fake_rec_opt l = Rec_aux (Rec_rec, gen_loc l) + +let no_tannot_opt l = Typ_annot_opt_aux (Typ_annot_opt_none, gen_loc l) + +let rec get_union_clauses id = function + | DEF_scattered (SD_aux (SD_unioncl (uid, tu), _)) :: defs when Id.compare id uid = 0 -> + tu :: get_union_clauses id defs + | def :: defs -> + get_union_clauses id defs + | [] -> [] + +let rec filter_union_clauses id = function + | DEF_scattered (SD_aux (SD_unioncl (uid, tu), _)) :: defs when Id.compare id uid = 0 -> + filter_union_clauses id defs + | def :: defs -> + def :: filter_union_clauses id defs + | [] -> [] + +let rec descatter' funcls mapcls = function + (* For scattered functions we collect all the seperate function + clauses until we find the last one, then we turn that function + clause into a DEF_fundef containing all the clauses. *) + | DEF_scattered (SD_aux (SD_funcl funcl, (l, _))) :: defs + when last_scattered_funcl (funcl_id funcl) defs -> + let clauses = match Bindings.find_opt (funcl_id funcl) funcls with + | Some clauses -> List.rev (funcl :: clauses) + | None -> [funcl] + in + DEF_fundef (FD_aux (FD_function (fake_rec_opt l, no_tannot_opt l, fake_effect_opt l, clauses), + (gen_loc l, Type_check.empty_tannot))) + :: descatter' funcls mapcls defs + + | DEF_scattered (SD_aux (SD_funcl funcl, _)) :: defs -> + let id = funcl_id funcl in + begin match Bindings.find_opt id funcls with + | Some clauses -> descatter' (Bindings.add id (funcl :: clauses) funcls) mapcls defs + | None -> descatter' (Bindings.add id [funcl] funcls) mapcls defs + end + + (* Scattered mappings are handled the same way as scattered functions *) + | DEF_scattered (SD_aux (SD_mapcl (id, mapcl), (l, tannot))) :: defs + when last_scattered_mapcl id defs -> + let clauses = match Bindings.find_opt id mapcls with + | Some clauses -> List.rev (mapcl :: clauses) + | None -> [mapcl] + in + DEF_mapdef (MD_aux (MD_mapping (id, no_tannot_opt l, clauses), + (gen_loc l, tannot))) + :: descatter' funcls mapcls defs + + | DEF_scattered (SD_aux (SD_mapcl (id, mapcl), _)) :: defs -> + begin match Bindings.find_opt id mapcls with + | Some clauses -> descatter' funcls (Bindings.add id (mapcl :: clauses) mapcls) defs + | None -> descatter' funcls (Bindings.add id [mapcl] mapcls) defs + end + + (* For scattered unions, when we find a union declaration we + immediately grab all the future clauses and turn it into a + regular union declaration. *) + | DEF_scattered (SD_aux (SD_variant (id, namescm, typq), (l, _))) :: defs -> + let tus = get_union_clauses id defs in + DEF_type (TD_aux (TD_variant (id, namescm, typq, tus, false), (gen_loc l, Type_check.empty_tannot))) + :: descatter' funcls mapcls (filter_union_clauses id defs) + + (* Therefore we should never see SD_unioncl... *) + | DEF_scattered (SD_aux (SD_unioncl _, (l, _))) :: defs -> + raise (Reporting.err_unreachable l __POS__ "Found union clause during de-scattering") + + | def :: defs -> def :: descatter' funcls mapcls defs + | [] -> [] + +let descatter (Defs defs) = Defs (descatter' Bindings.empty Bindings.empty defs) diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 180b96b2..9453e999 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -386,17 +386,17 @@ let rec find_scattered_of name = function | [] -> [] | DEF_scattered (SD_aux(sda,_) as sd):: defs -> (match sda with - | SD_scattered_function(_,_,_,id) - | SD_scattered_funcl(FCL_aux(FCL_Funcl(id,_),_)) - | SD_scattered_unioncl(id,_) -> + | SD_function(_,_,_,id) + | SD_funcl(FCL_aux(FCL_Funcl(id,_),_)) + | SD_unioncl(id,_) -> if name = string_of_id id then [sd] else [] | _ -> [])@ (find_scattered_of name defs) | _::defs -> find_scattered_of name defs -let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd,_)) = match sd with - | SD_scattered_function(_,tannot_opt,_,id) -> +let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd,(l, _))) = match sd with + | SD_function(_,tannot_opt,_,id) -> let b,ns = (match tannot_opt with | Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ),_) -> let bindings = if consider_var then typq_bindings typq else mt in @@ -404,7 +404,7 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd | Typ_annot_opt_aux(Typ_annot_opt_none, _) -> mt, mt) in init_env (string_of_id id),ns - | SD_scattered_funcl (FCL_aux(FCL_Funcl(id,pexp),_)) -> + | SD_funcl (FCL_aux(FCL_Funcl(id,pexp),_)) -> begin match pexp with | Pat_aux(Pat_exp (pat,exp),_) -> @@ -423,7 +423,7 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd | _ -> mt in scattered_binds, exp_ns end - | SD_scattered_variant (id,_,_) -> + | SD_variant (id,_,_) -> let name = string_of_id id in let uses = if consider_scatter_as_one @@ -435,12 +435,12 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd Nameset.remove name pieces_uses else mt in init_env name, uses - | SD_scattered_unioncl(id, type_union) -> + | SD_unioncl(id, type_union) -> let typ_name = string_of_id id in let b = init_env typ_name in let (b,r) = typ_variants consider_var b [type_union] in (Nameset.remove typ_name b, Nameset.add typ_name r) - | SD_scattered_end id -> + | SD_end id -> let name = string_of_id id in let uses = if consider_scatter_as_one (*Note: if this is a function ending, the dec is included *) @@ -450,6 +450,7 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd (List.map (fv_of_scattered consider_var false []) scattered_defs) (init_env name) else init_env name in init_env (name ^ "/end"), uses + | _ -> raise (Reporting.err_unreachable l __POS__ "Tried to find free variables for scattered mapping clause") let fv_of_rd consider_var (DEC_aux (d, annot)) = (* When we get the free variables of a register, we have to ensure diff --git a/src/type_check.ml b/src/type_check.ml index 435c5cd8..f204a558 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -235,6 +235,9 @@ module Env : sig val add_local : id -> mut * typ -> t -> t val get_locals : t -> (mut * typ) Bindings.t val add_variant : id -> typquant * type_union list -> t -> t + val add_scattered_variant : id -> typquant -> t -> t + val add_variant_clause : id -> type_union -> t -> t + val get_variant : id -> t -> typquant * type_union list val add_mapping : id -> typquant * typ * typ -> t -> t val add_union_id : id -> typquant * typ -> t -> t val add_flow : id -> (typ -> typ) -> t -> t @@ -916,10 +919,22 @@ end = struct end let add_variant id variant env = - begin - typ_print (lazy (adding ^ "variant " ^ string_of_id id)); - { env with variants = Bindings.add id variant env.variants } - end + typ_print (lazy (adding ^ "variant " ^ string_of_id id)); + { env with variants = Bindings.add id variant env.variants } + + let add_scattered_variant id typq env = + typ_print (lazy (adding ^ "scattered variant " ^ string_of_id id)); + { env with variants = Bindings.add id (typq, []) env.variants } + + let add_variant_clause id tu env = + match Bindings.find_opt id env.variants with + | Some (typq, tus) -> { env with variants = Bindings.add id (typq, tus @ [tu]) env.variants } + | None -> typ_error (id_loc id) ("scattered union " ^ string_of_id id ^ " not found") + + let get_variant id env = + match Bindings.find_opt id env.variants with + | Some (typq, tus) -> typq, tus + | None -> typ_error (id_loc id) ("union " ^ string_of_id id ^ " not found") let add_union_id id bind env = begin @@ -4339,7 +4354,6 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md else typ_error l ("Mapping not pure (or escape only): " ^ string_of_effect eff ^ " found") - (* Checking a val spec simply adds the type as a binding in the context. We have to destructure the various kinds of val specs, but the difference is irrelevant for the typechecker. *) @@ -4355,7 +4369,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) = let env = Env.add_extern id ext_opt env in let env = if is_cast then Env.add_cast id env else env in let typq, typ = - if !opt_expand_valspec then + if !opt_expand_valspec then expand_bind_synonyms ts_l env (typq, typ) else (typq, typ) @@ -4473,6 +4487,28 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t = typ_error l "Bad bitfield type" end +and check_scattered : 'a. Env.t -> 'a scattered_def -> (tannot def) list * Env.t = + fun env (SD_aux (sdef, (l, _))) -> + match sdef with + | SD_function _ | SD_end _ | SD_mapping _ -> [], env + | SD_variant (id, namescm, typq) -> + [DEF_scattered (SD_aux (SD_variant (id, namescm, typq), (l, None)))], Env.add_scattered_variant id typq env + | SD_unioncl (id, tu) -> + [DEF_scattered (SD_aux (SD_unioncl (id, tu), (l, None)))], + let env = Env.add_variant_clause id tu env in + let typq, _ = Env.get_variant id env in + check_type_union env id typq tu + | SD_funcl (FCL_aux (FCL_Funcl (id, _), (l, _)) as funcl) -> + let typq, typ = Env.get_val_spec id env in + let funcl_env = add_typquant l typq env in + let funcl = check_funcl funcl_env funcl typ in + [DEF_scattered (SD_aux (SD_funcl funcl, (l, None)))], env + | SD_mapcl (id, mapcl) -> + let typq, typ = Env.get_val_spec id env in + let mapcl_env = add_typquant l typq env in + let mapcl = check_mapcl mapcl_env mapcl typ in + [DEF_scattered (SD_aux (SD_mapcl (id, mapcl), (l, None)))], env + and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t = fun env def -> let cd_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Case") in @@ -4503,7 +4539,7 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t = | DEF_pragma (pragma, arg, l) -> [DEF_pragma (pragma, arg, l)], env | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err () | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err () - | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Scattered given to type checker") + | DEF_scattered sdef -> check_scattered env sdef and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t = fun env (Defs defs) -> |