From fbcc27ca1bd3801beac0338e657b933d6a9c8f95 Mon Sep 17 00:00:00 2001 From: Jon French Date: Thu, 27 Dec 2018 12:19:44 +0000 Subject: refactor val-spec AST to store externs as an assoc-list rather than a function (preparing for marshalling) --- language/sail.ott | 4 ++-- src/ast_util.ml | 10 ++++++++++ src/ast_util.mli | 3 +++ src/initial_check.ml | 12 ++++++------ src/ocaml_backend.ml | 4 ++-- src/parse_ast.ml | 2 +- src/parser.mly | 22 +++++++++++----------- src/pretty_print_coq.ml | 4 ++-- src/pretty_print_lem.ml | 2 +- src/pretty_print_sail.ml | 4 +--- src/rewrites.ml | 16 ++++++++-------- src/type_check.ml | 22 +++++++++++----------- 12 files changed, 58 insertions(+), 47 deletions(-) diff --git a/language/sail.ott b/language/sail.ott index 59d51d68..5c8b6a01 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -943,8 +943,8 @@ val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::= val_spec_aux :: 'VS_' ::= {{ com value type specification }} - {{ ocaml VS_val_spec of typschm * id * (string -> string option) * bool }} - {{ lem VS_val_spec of typschm * id * (string -> maybe string) * bool }} + {{ ocaml VS_val_spec of typschm * id * (string * string) list * bool }} + {{ lem VS_val_spec of typschm * id * list (string * string) * bool }} | val typschm id :: S :: val_spec {{ com specify the type of an upcoming definition }} {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }} diff --git a/src/ast_util.ml b/src/ast_util.ml index 9966742e..3d13c5c3 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -1488,3 +1488,13 @@ and locate_fexps : 'a. l -> 'a fexps -> 'a fexps = fun l (FES_aux (FES_Fexps (fe and locate_fexp : 'a. l -> 'a fexp -> 'a fexp = fun l (FE_aux (FE_Fexp (id, exp), (_, annot))) -> FE_aux (FE_Fexp (locate_id l id, locate l exp), (l, annot)) + + +let extern_assoc backend exts = + try + try + Some (List.assoc backend exts) + with Not_found -> + Some (List.assoc "_" exts) + with Not_found -> + None diff --git a/src/ast_util.mli b/src/ast_util.mli index ea287190..54f18ae8 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -366,3 +366,6 @@ val locate_pat : l -> 'a pat -> 'a pat val locate_lexp : l -> 'a lexp -> 'a lexp val locate_typ : l -> typ -> typ + + +val extern_assoc : string -> (string * string) list -> string option diff --git a/src/initial_check.ml b/src/initial_check.ml index 36513ba1..36c60f2e 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -1078,8 +1078,8 @@ let typschm_of_string order str = let (typschm, _, _) = to_ast_typschm initial_kind_env order 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 order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, [("_", 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, [], false)) let val_spec_ids (Defs defs) = let val_spec_id (VS_aux (vs_aux, _)) = @@ -1154,7 +1154,7 @@ let generate_undefineds vs_ids (Defs defs) = let undefined_td = function | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in - [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false)); + [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, [], false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) (mk_pat (P_lit (mk_lit L_unit))) (if !opt_fast_undefined && List.length ids > 0 then @@ -1164,7 +1164,7 @@ let generate_undefineds vs_ids (Defs defs) = [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]] | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in - [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); + [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) pat (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]] @@ -1212,7 +1212,7 @@ let generate_undefineds vs_ids (Defs defs) = (mk_exp (E_app (mk_id "internal_pick", [mk_exp (E_list (List.map (make_constr typ_to_var) constr_args))]))) letbinds in - [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); + [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) pat body]] @@ -1248,7 +1248,7 @@ let generate_enum_functions vs_ids (Defs defs) = let rec gen_enums = function | DEF_type (TD_aux (TD_enum (id, _, elems, _), _)) as enum :: defs -> let enum_val_spec name quants typ = - mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, (fun _ -> None), !opt_enum_casts)) + mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, [], !opt_enum_casts)) in let range_constraint kid = nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1))) in diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 4828398f..2a1fae15 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -615,8 +615,8 @@ let ocaml_typedef ctx (TD_aux (td_aux, _)) = | _ -> failwith "Unsupported typedef" let get_externs (Defs defs) = - let extern_id (VS_aux (VS_val_spec (typschm, id, ext, _), _)) = - match ext "ocaml" with + let extern_id (VS_aux (VS_val_spec (typschm, id, exts, _), _)) = + match Ast_util.extern_assoc "ocaml" exts with | None -> [] | Some ext -> [(id, mk_id ext)] in diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 3317c196..db8f9939 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -488,7 +488,7 @@ type_def_aux = (* Type definition body *) type val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id * (string -> string option) * bool + VS_val_spec of typschm * id * (string * string) list * bool type diff --git a/src/parser.mly b/src/parser.mly index 070dee50..b2df5176 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -1316,31 +1316,31 @@ let_def: externs: | id Colon String - { ([(string_of_id $1, $3)], None) } + { [(string_of_id $1, $3)] } | Under Colon String - { ([], Some $3) } + { [("_", $3)] } | id Colon String Comma externs - { cons_fst (string_of_id $1, $3) $5 } + { (string_of_id $1, $3) :: $5 } val_spec_def: | Doc val_spec_def { doc_vs $1 $2 } | Val id Colon typschm - { mk_vs (VS_val_spec ($4, $2, (fun _ -> None), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($4, $2, [], false)) $startpos $endpos } | Val Cast id Colon typschm - { mk_vs (VS_val_spec ($5, $3, (fun _ -> None), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($5, $3, [], true)) $startpos $endpos } | Val id Eq String Colon typschm - { mk_vs (VS_val_spec ($6, $2, (fun _ -> Some $4), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($6, $2, [], false)) $startpos $endpos } | Val Cast id Eq String Colon typschm - { mk_vs (VS_val_spec ($7, $3, (fun _ -> Some $5), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($7, $3, [("_", $5)], true)) $startpos $endpos } | Val String Colon typschm - { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), (fun _ -> Some $2), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), [("_", $2)], false)) $startpos $endpos } | Val Cast String Colon typschm - { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), (fun _ -> Some $3), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), [("_", $3)], true)) $startpos $endpos } | Val id Eq Lcurly externs Rcurly Colon typschm - { mk_vs (VS_val_spec ($8, $2, (fun backend -> (assoc_opt backend $5)), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($8, $2, $5, false)) $startpos $endpos } | Val Cast id Eq Lcurly externs Rcurly Colon typschm - { mk_vs (VS_val_spec ($9, $3, (fun backend -> (assoc_opt backend $6)), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($9, $3, $6, true)) $startpos $endpos } register_def: | Register id Colon typ diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index f1726ce4..ccbde5cd 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -2235,8 +2235,8 @@ let find_exc_typ defs = let find_unimplemented defs = let adjust_def unimplemented = function - | DEF_spec (VS_aux (VS_val_spec (_,id,ext,_),_)) -> begin - match ext "coq" with + | DEF_spec (VS_aux (VS_val_spec (_,id,exts,_),_)) -> begin + match Ast_util.extern_assoc "coq" exts with | Some _ -> unimplemented | None -> IdSet.add id unimplemented end diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 68825c8f..ba2b797b 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1349,7 +1349,7 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = let doc_spec_lem (VS_aux (valspec,annot)) = match valspec with - | VS_val_spec (typschm,id,ext,_) when ext "lem" = None -> + | VS_val_spec (typschm,id,exts,_) when Ast_util.extern_assoc "lem" exts = None -> (* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in if contains_t_pp_var typ then empty else *) doc_docstring_lem annot ^^ diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 0b0a8305..179ef208 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -538,9 +538,7 @@ let doc_typdef (TD_aux(td,_)) = match td with let doc_spec (VS_aux (v, annot)) = let doc_extern ext = - let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^ - utf8string ("\"" ^ String.escaped id ^ "\"")) (ext b) in - let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"; "smt"; "interpreter"; "c"]) in + let docs = List.map (fun (backend, rep) -> string (backend ^ ":") ^^ space ^^ utf8string ("\"" ^ String.escaped rep ^ "\"")) ext in if docs = [] then empty else equals ^^ space ^^ braces (separate (comma ^^ space) docs) in match v with diff --git a/src/rewrites.ml b/src/rewrites.ml index c470d906..f1d22720 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2212,7 +2212,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) = in let val_spec = VS_aux (VS_val_spec - (mk_typschm typquant fun_typ, id, (fun _ -> None), false), + (mk_typschm typquant fun_typ, id, [], false), (Parse_ast.Unknown, empty_tannot)) in let fundef = FD_aux (FD_function (r_o, t_o, e_o, funcls), fdannot) in @@ -3152,7 +3152,7 @@ let construct_toplevel_string_append_func env f_id pat = ), unk)] in let fun_typ = (mk_typ (Typ_fn ([string_typ], option_typ, no_effect))) in - let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, (fun _ -> None), false), unkt) in + let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, [], false), unkt) in let new_val_spec, env = Type_check.check_val_spec env new_val_spec in let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in @@ -4345,10 +4345,10 @@ let rewrite_defs_realise_mappings (Defs defs) = let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), l) in let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), l) in - let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in - let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in - let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in - let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, [], false), (Parse_ast.Unknown,())) in + let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, [], false), (Parse_ast.Unknown,())) in + let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, [], false), (Parse_ast.Unknown,())) in + let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, [], false), (Parse_ast.Unknown,())) in let forwards_spec, env = Type_check.check_val_spec env forwards_spec in let backwards_spec, env = Type_check.check_val_spec env backwards_spec in @@ -4382,7 +4382,7 @@ let rewrite_defs_realise_mappings (Defs defs) = let string_defs = begin if subtype_check env typ1 string_typ && subtype_check env string_typ typ1 then let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in - let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in @@ -4392,7 +4392,7 @@ let rewrite_defs_realise_mappings (Defs defs) = else if subtype_check env typ2 string_typ && subtype_check env string_typ typ2 then let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in - let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in diff --git a/src/type_check.ml b/src/type_check.ml index cf1d8ef9..16690696 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -392,7 +392,7 @@ module Env : sig val add_overloads : id -> id list -> t -> t val get_overloads : id -> t -> id list val is_extern : id -> t -> string -> bool - val add_extern : id -> (string -> string option) -> t -> t + val add_extern : id -> (string * string) list -> t -> t val get_extern : id -> t -> string -> string val get_default_order : t -> order val set_default_order : order_aux -> t -> t @@ -459,7 +459,7 @@ end = struct enums : IdSet.t Bindings.t; records : (typquant * (typ * id) list) Bindings.t; accessors : (typquant * typ) Bindings.t; - externs : (string -> string option) Bindings.t; + externs : (string * string) list Bindings.t; smt_ops : string Bindings.t; constraint_synonyms : (kid list * n_constraint) Bindings.t; casts : id list; @@ -1073,7 +1073,7 @@ end = struct | Not_found -> typ_error (id_loc id) ("No register binding found for " ^ string_of_id id) let is_extern id env backend = - try not (Bindings.find id env.externs backend = None) with + try not (Ast_util.extern_assoc backend (Bindings.find id env.externs) = None) with | Not_found -> false (* Bindings.mem id env.externs *) @@ -1082,7 +1082,7 @@ end = struct let get_extern id env backend = try - match Bindings.find id env.externs backend with + match Ast_util.extern_assoc backend (Bindings.find id env.externs) with | Some ext -> ext | None -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id) with @@ -4353,7 +4353,7 @@ let mk_val_spec env typq typ id = | Typ_aux (Typ_fn (_,_,eff),_) -> eff | _ -> no_effect in - DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, (fun _ -> None), false), (Parse_ast.Unknown, Some ((env,typ,eff),None)))) + DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, [], false), (Parse_ast.Unknown, Some ((env,typ,eff),None)))) let check_tannotopt env typq ret_typ = function | Typ_annot_opt_aux (Typ_annot_opt_none, _) -> () @@ -4449,16 +4449,16 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md let check_val_spec env (VS_aux (vs, (l, _))) = let annotate vs typ eff = DEF_spec (VS_aux (vs, (l, Some ((env, typ, eff), None)))) in let vs, id, typq, typ, env = match vs with - | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, ext_opt, is_cast) -> + | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, exts, is_cast) -> typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm)); - let env = match (ext_opt "smt", ext_opt "#") with + let env = match (Ast_util.extern_assoc "smt" exts, Ast_util.extern_assoc "#" exts) with | Some op, None -> Env.add_smt_op id op env | _, _ -> env in - let env = Env.add_extern id ext_opt env in + let env = Env.add_extern id exts env in let env = if is_cast then Env.add_cast id env else env in let typq, typ = expand_bind_synonyms ts_l env (typq, typ) in - let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in + let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, exts, is_cast) in (vs, id, typq, typ, env) in let eff = @@ -4626,13 +4626,13 @@ let initial_env = (* |> Env.add_val_spec (mk_id "int") * (TypQ_aux (TypQ_no_forall, Parse_ast.Unknown), Typ_aux (Typ_bidir (int_typ, string_typ), Parse_ast.Unknown)) *) - |> Env.add_extern (mk_id "size_itself_int") (fun _ -> Some "size_itself_int") + |> Env.add_extern (mk_id "size_itself_int") [("_", "size_itself_int")] |> Env.add_val_spec (mk_id "size_itself_int") (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)), Parse_ast.Unknown)],Parse_ast.Unknown), function_typ [app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]] (atom_typ (nvar (mk_kid "n"))) no_effect) - |> Env.add_extern (mk_id "make_the_value") (fun _ -> Some "make_the_value") + |> Env.add_extern (mk_id "make_the_value") [("_", "make_the_value")] |> Env.add_val_spec (mk_id "make_the_value") (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)), Parse_ast.Unknown)],Parse_ast.Unknown), -- cgit v1.2.3