structure BundleParser :> BundleParser = struct open HolKernel TypeBase Parse Term UIRLexer open boolLib open finite_mapSyntax open listSyntax open pairSyntax open stringSyntax open sumSyntax open uvmErrorsTheory open uvmIRTheory open ParserHelpers open TypeParser open ValueParser open CodeParser val decls : string list = [ "typedef", "const", "global", "funcsig", "funcdecl", "funcdef" ] val ty_env = mk_type("environment", []) val ty_bundle = ty_env --> or_error ty_env val ty_gln = mk_type("global_name", []) val ty_tyn = mk_type("type_name", []) val ty_sign = mk_type("sig_name", []) val ty_constn = mk_type("const_name", []) val t_env = mk_var("env", ty_env) (* Attempts to look up a member of one of the finite map fields of an ``:environment``. Assumes that t_env is already present in the current scope. Returns a term of type ``:^vty or_error``. *) fun get_env_member (field_name : string) (kty : hol_type) (vty : hol_type) (key : term) : term = infer_comb("expect", [ infer_comb("FLOOKUP", [ infer_comb("environment_" ^ field_name, [t_env], mk_fmap_ty(kty, vty)), key ], mk_type("option", [vty])), infer_comb("InvalidIR", (* TODO: Include key in error message *) [fromMLstring (field_name ^ " lookup failed")], ty_err) ], or_error vty) fun get_env_type (name : string) : term = get_env_member "types" ty_tyn ty_type (infer_comb("TypeName", [fromMLstring name], ty_tyn)) fun get_env_funcsig (name : string) : term = get_env_member "funcsigs" ty_sign ty_sig (infer_comb("SigName", [fromMLstring name], ty_sign)) fun get_env_const (name : string) : term = mk_lift( mk_thy_const{Thy="pair", Name="SND", Ty=mk_prod(ty_type, ty_val) --> ty_val}, get_env_member "constants" ty_constn (mk_prod(ty_type, ty_val)) (infer_comb("ConstName", [fromMLstring name], ty_constn))) fun add_env_member (field_name : string) (kty : hol_type) (vty : hol_type) (key : term) (value : term) : term = let val t_f = mk_var("f", mk_fmap_ty(kty, vty)) in infer_comb("environment_" ^ field_name ^ "_fupd", [ mk_abs(t_f, infer_comb("FUPDATE", [t_f, mk_pair(key, value)], mk_fmap_ty(kty, vty))), t_env ], ty_env) end fun add_env_type (name : string) (t : term) : term = add_env_member "types" ty_tyn ty_type (infer_comb("TypeName", [fromMLstring name], ty_tyn)) t fun add_env_funcsig (name : string) (s : term) : term = add_env_member "funcsigs" ty_sign ty_sig (infer_comb("SigName", [fromMLstring name], ty_sign)) s fun add_env_const (name : string) (ty : term) (value : term) : term = add_env_member "constants" ty_constn (mk_prod(ty_type, ty_val)) (infer_comb("ConstName", [fromMLstring name], ty_constn)) (mk_pair(ty, value)) val free_env_context = { get_type = get_env_type, get_funcsig = get_env_funcsig, get_global = get_env_const } type bundle = { types : term list, globals : term list, functions : term list } val empty_bundle : bundle = { types = [], globals = [], functions = [] } fun parse_decl (lines : uir_token list list, {types, globals, functions} : bundle) : bundle = let val env = free_env_context val (header::other_lines) = filter (fn l => l <> []) lines in case header of Decl "typedef"::SSA (Global, name)::Eq::rhs => if other_lines = [] then let val ty = mk_var("ty", ty_type) val def = mk_abs(t_env, mk_lift(mk_abs(ty, add_env_type name ty), parse_type env rhs)) in {types = types @ [def], globals = globals, functions = functions} end else raise ParseError "non-declaration line after .typedef" | Decl "funcsig"::SSA (Global, name)::Eq::rhs => if other_lines = [] then let val fs = mk_var("fs", ty_sig) val def = mk_abs(t_env, mk_lift(mk_abs(fs, add_env_funcsig name fs), parse_funcsig env rhs)) in {types = types @ [def], globals = globals, functions = functions} end else raise ParseError "non-declaration line after .funcsig" | Decl "const"::SSA (Global, name)::Type ty::Eq::rhs => (* TODO: Support multi-line constants (for structs, arrays, etc.) *) if other_lines = [] then let val ty' = mk_var("ty'", ty_type) val const = mk_var("const", ty_val) val def = mk_abs(t_env, mk_bind(parse_type env ty, mk_abs(ty', mk_lift( mk_abs(const, add_env_const name ty' const), beta_conv(mk_comb(parse_value rhs, ty')))))) in {types = types, globals = globals @ [def], functions = functions} end else raise ParseError "non-declaration line after .const" | [Decl "global", SSA (Global, name), Type ty] => let val t_ty = mk_var("ty", ty_type) val t_gln = infer_comb("Global", [fromMLstring name], ty_gln) val ty_gl = mk_prod(ty_gln, ty_type) val t_gls = mk_var("gls", ty_list ty_gl) val def = mk_abs(t_env, mk_lift( mk_abs(t_ty, infer_comb("environment_globals_fupd", [ mk_abs(t_gls, infer_comb("CONS", [mk_pair(t_gln, t_ty), t_gls], ty_list ty_gl)), add_env_const name t_ty (infer_comb("RefV", [t_ty, mk_some(infer_comb("GlobalAddr", [t_gln], ty_addr))], ty_val)) ], ty_env)), parse_type env ty)) in {types = types, globals = globals @ [def], functions = functions} end | [Decl "funcdecl", SSA (Global, name), Type fsig] => (* TODO: funcdecl *) raise ParseError "funcdecl not yet supported" | [Decl "funcdef", SSA (Global, name), Word "VERSION", SSA (Local, v), Type fsig, OpenBrace] => if exists (fn l => l = [CloseBrace]) other_lines then if List.last other_lines = [CloseBrace] then let val r = mk_const("REF", mk_type("ref_type", [])) val ty_fno = mk_type("option", [ty_funcn]) val fsig' = parse_funcsig env fsig val ty = mk_var("ty", ty_type) val fr = mk_var("fr", ty_val) val fref = mk_abs(t_env, list_mk_lift( list_mk_abs([ty, fr], add_env_const name ty fr), [ mk_lift(infer_comb("FuncRef", [r], ty_sig --> ty_type), fsig'), list_mk_lift( infer_comb("FuncRefV", [r], ty_sig --> ty_fno --> ty_val), [fsig', mk_return(infer_comb("SOME", [ infer_comb("Func", [fromMLstring name], ty_funcn)], ty_fno))])])) val fdef = mk_abs(t_env, mk_lift( infer_comb("generate_function", [t_env, fromMLstring name], mk_type("function", []) --> ty_env), parse_func env fsig' (List.take(other_lines, length other_lines - 1)))) in {types = types, globals = globals @ [fref], functions = functions @ [fdef]} end else raise ParseError "non-declaration line after .funcdef's }" else raise ParseError "unclosed { in .funcdef" | Decl d::_ => if exists (fn x => x = d) decls then raise ParseError ("invalid parameters for ." ^ d) else raise ParseError ("." ^ d ^ " is not a toplevel declaration") | _ => raise ParseError "expected toplevel declaration" end fun uir_bundle (quotation : 'a frag list) : term = let val ty_bind = or_error ty_env --> ty_bundle --> or_error ty_env val str = unquote_all quotation val lines = map tokenize (String.tokens (fn x => x = #"\n") str) val decl_blocks = split_by_header (fn (Decl _::_) => true | _ => false) (filter (fn l => l <> []) lines) val {types, globals, functions} = foldl parse_decl empty_bundle decl_blocks in mk_abs(t_env, list_mk_comb( mk_thy_const{ Thy="list", Name="FOLDL", Ty=ty_bind --> or_error ty_env --> ty_list ty_bundle --> or_error ty_env }, [ mk_thy_const{Thy="sumMonad", Name="bind_left", Ty=ty_bind}, mk_return t_env, mk_list(types @ globals @ functions, ty_bundle) ])) end end