To protect your data, the CISO officer has suggested users to enable GitLab 2FA as soon as possible.

Commit 87ce7ba5 authored by Adam Nelson's avatar Adam Nelson
Browse files

Tests pass again with RISC-V code!

- Parser updated to work with code changes
- Lots of bug fixes to get tests to pass (previous commit didn't even
  execute basic instructions properly)
- Improved pretty printing and EVAL
parent 59737ac5
......@@ -3,7 +3,7 @@ open HolKernel
signature EvalUtils =
sig
val add_extra_eval_thms : unit -> unit
(*
val to_env : term -> term
val start_at : string -> term frag list -> term -> term
......@@ -19,6 +19,5 @@ sig
val take_step : term frag list -> term -> term
val take_steps : term frag list -> term -> term
*)
end
structure EvalUtils :> EvalUtils =
struct
open HolKernel Parse Term boolLib bossLib
open listTheory llistTheory optionTheory pred_setTheory finite_mapTheory uvmMemoryTheory listSyntax stringSyntax
val map_keys_register_fupdate = prove(
``MAP_KEYS (Register (Thread n)) (fm |+ (k, v)) =
MAP_KEYS (Register (Thread n)) fm |+ (Register (Thread n) k, v)``,
simp[INJ_DEF, MAP_KEYS_FUPDATE])
val reduce_o_f_if = prove(
``f x s y y'. (f o_f if x s then y else y') = (if s x then f o_f y else f o_f y')``,
rw[IN_APP])
open listTheory llistTheory optionTheory pred_setTheory finite_mapTheory sptreeTheory
open listSyntax stringSyntax sptreeSyntax
open sumMonadTheory uvmTypesTheory uvmMemoryTheory
val lhdtl_lunfold = prove(
``LHD (LUNFOLD f x) = OPTION_MAP SND (f x)
......@@ -18,44 +11,44 @@ struct
rw[] >> rw[Once LUNFOLD, LHDTL_CONS_THM] >>
Cases_on `f x` >> simp[OPTION_MAP_DEF] >> Cases_on `x'` >> simp[])
fun add_extra_eval_thms() : unit =
fun add_extra_eval_thms() : unit = (
sptreeSyntax.temp_add_sptree_printer();
computeLib.add_funs[
SING, CHOICE_SING,
SING, CHOICE_SING, EMPTY_DEF, IN_APP, INSERT_applied,
OPTION_MAP_DEF, OPTION_MAP2_DEF, OPTION_BIND_def, OPTION_CHOICE_def,
in_app_symbolic_only, lhdtl_lunfold,
lhdtl_lunfold, prefix_type_cases,
bind_left_monad_left_id, bind_left_monad_right_id, bind_left_monad_assoc]
)
(*
fun parens q = [QUOTE "("] @ q @ [QUOTE ")"]
fun to_env (bundle : term) : term =
EVAL ``^bundle empty_env`` |> concl |> rhs
fun start_at (func_name : string) (args : term frag list) (env : term) : term =
let val func_name' = fromMLstring func_name in
EVAL(Term(`^env >>= λe. init_sched_state <|env:=e;main:=Func ^func_name';args:=` @ parens args @ `|>`))
|> concl |> rhs
end
Term(`
^env >>= λenv.
new_sched_state env (Func ^(fromMLstring func_name)) >>=
start_with_args ` @ parens args) |> EVAL |> concl |> rhs
fun run_schedule (schedule : term frag list) (state : term) : term =
EVAL(Term(`^state >>= run_schedule` @ parens schedule)) |> concl |> rhs
Term(`^state >>= run_schedule` @ parens schedule) |> EVAL |> concl |> rhs
fun run_finite_schedule (schedule : term frag list) (state : term) : term =
EVAL(Term(`^state >>= run_finite_schedule` @ parens schedule)) |> concl |> rhs
Term(`^state >>= run_finite_schedule` @ parens schedule) |> EVAL |> concl |> rhs
fun expect_result (expected : term frag list) (state : term) : thm =
let val actual = EVAL(``^state >>= get_return_values``) |> concl |> rhs
let val actual = EVAL ``^state >>= get_return_values`` |> concl |> rhs
in prove(Term(parens expected @ ` = ^actual`), simp[]) end
fun expect_global_value (name : string) (value : term frag list) (state : term) : thm =
let val actual = EVAL(``^state >>= get_global_value ^(fromMLstring name)``) |> concl |> rhs
let val actual = EVAL ``^state >>= get_global_value ^(fromMLstring name)`` |> concl |> rhs
in prove(Term(parens value @ ` = ^actual`), simp[]) end
fun take_step (step : term frag list) (state : term) : term =
EVAL(Term(`^state >>= take_step` @ parens step)) |> concl |> rhs
Term(`^state >>= take_step` @ parens step) |> EVAL |> concl |> rhs
fun take_steps (steps : term frag list) (state : term) : term =
EVAL(Term(`^state >>= take_steps` @ parens steps)) |> concl |> rhs
*)
Term(`^state >>= take_steps` @ parens steps) |> EVAL |> concl |> rhs
end
......@@ -21,7 +21,6 @@ struct
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", [])
......@@ -56,10 +55,8 @@ struct
(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)))
get_env_member "constants" ty_constn ty_or_const
(infer_comb("ConstName", [fromMLstring name], ty_constn))
fun add_env_member (field_name : string)
(kty : hol_type)
......@@ -82,9 +79,11 @@ struct
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))
fun add_env_const (name : string) (ty : term) (values : term) : term =
add_env_member "constants" ty_constn ty_or_const
(infer_comb("ConstName", [fromMLstring name], ty_constn))
(list_mk_comb(t_Const, [ty, infer_comb("HD", [values], ty_val),
infer_comb("TL", [values], ty_list ty_val)]))
val free_env_context = {
get_type = get_env_type,
......@@ -95,73 +94,69 @@ struct
type bundle = {
types : term list,
globals : term list,
functions : term list
functions : term list,
gn : int
}
val empty_bundle : bundle = {
types = [], globals = [], functions = []
types = [], globals = [], functions = [], gn = 0
}
fun parse_decl (lines : uir_token list list,
{types, globals, functions} : bundle)
{types, globals, functions, gn} : bundle)
: bundle =
let
val env = free_env_context
val (header::other_lines) = filter (fn l => l <> []) lines
in
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}
let val ty = mk_var("ty", ty_type)
val def = parse_type env rhs
|> curry mk_lift (mk_abs(ty, add_env_type name ty))
|> curry mk_abs t_env in
{types = types @ [def], globals = globals, functions = functions, gn = gn}
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}
let val fs = mk_var("fs", ty_sig)
val def = parse_funcsig env rhs
|> curry mk_lift(mk_abs(fs, add_env_funcsig name fs))
|> curry mk_abs t_env in
{types = types @ [def], globals = globals, functions = functions, gn = gn}
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}
let val ty' = mk_var("ty'", ty_type)
val const = mk_var("const", ty_list ty_val)
val def = mk_comb(parse_value rhs, ty') |> beta_conv
|> curry mk_lift (mk_abs(const, add_env_const name ty' const))
|> curry mk_abs ty'
|> curry mk_bind (parse_type env ty)
|> curry mk_abs t_env in
{types = types, globals = globals @ [def], functions = functions, gn = gn}
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}
let val global = mk_const("Global", mk_type("alloc", []))
val t_gln = fromMLstring name
val ty_gl = mk_prod(ty_str, ty_type)
val def = parse_type env ty
|> curry mk_lift (
let val t_ty = mk_var("ty", ty_type)
val t_gls = mk_var("gls", ty_list ty_gl) in
infer_comb("environment_globals_fupd", [
infer_comb("CONS", [mk_pair(t_gln, t_ty), t_gls], ty_list ty_gl)
|> curry mk_abs t_gls,
infer_comb("RefV", [t_ty, mk_some(mk_pair(global, mk_num gn))], ty_val)
|> mk_singleton
|> add_env_const name t_ty], ty_env)
|> curry mk_abs t_ty
end)
|> curry mk_abs t_env in
{types = types, globals = globals @ [def], functions = functions, gn = gn + 1}
end
| [Decl "funcdecl", SSA (Global, name), Type fsig] =>
(* TODO: funcdecl *)
......@@ -169,25 +164,28 @@ struct
| [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]}
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 fref =
[mk_lift(infer_comb("FuncRef", [r], ty_sig --> ty_type), fsig'),
infer_comb("FuncRefV", [r,
infer_comb("OUTL", [fsig'], ty_sig),
infer_comb("Func", [fromMLstring name], ty_funcn) |> mk_some
], ty_val) |> mk_singleton |> mk_return]
|> curry list_mk_lift (
let val fr = mk_var("fr", ty_list ty_val)
val ty = mk_var("ty", ty_type) in
list_mk_abs([ty, fr], add_env_const name ty fr)
end)
|> curry mk_abs t_env
val fdef =
List.take(other_lines, length other_lines - 1)
|> parse_func env fsig'
|> curry mk_lift (infer_comb("generate_function",
[t_env, fromMLstring name], mk_type("function", []) --> ty_env))
|> curry mk_abs t_env in
{types = types, globals = globals @ [fref], functions = functions @ [fdef], gn = gn}
end
else raise ParseError "non-declaration line after .funcdef's }"
else raise ParseError "unclosed { in .funcdef"
......@@ -201,36 +199,27 @@ struct
end
fun uir_bundle_s (str : string) : term =
let
val ty_bind = or_error ty_env --> ty_bundle --> or_error ty_env
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)
]))
let val ty_bind = or_error ty_env --> ty_bundle --> or_error ty_env
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, gn} =
foldl parse_decl empty_bundle decl_blocks in
mk_abs(t_env, infer_comb("FOLDL",
[``bind_left : ^(ty_antiq ty_bind)``,
mk_return t_env,
mk_list(types @ globals @ functions, ty_bundle)],
or_error ty_env))
end
fun uir_bundle (quotation : 'a frag list) : term =
uir_bundle_s (unquote_all quotation)
fun load_uir_file (filename : string) : term =
let
val stream = TextIO.openIn filename
fun read() = case TextIO.inputLine stream of
SOME s => s ^ read()
| NONE => ""
in
let val stream = TextIO.openIn filename
fun read() = case TextIO.inputLine stream of
SOME s => s ^ read()
| NONE => "" in
uir_bundle_s (read())
handle ParseError e => raise ParseError ("[" ^ filename ^ "] " ^ e)
end
......
......@@ -4,7 +4,7 @@ signature CodeParser =
sig
val ty_ssa : hol_type
val ty_blabel : hol_type
val or_const : hol_type -> hol_type
val ty_or_const : hol_type
val t_Var : term
val t_Const : term
......
......@@ -55,11 +55,11 @@ struct
val ty_ssa = mk_type("ssavar", [])
val ty_blabel = mk_type("block_label", [])
val ty_ci = mk_type("comminst", [ty_ssa])
fun or_const ty = ``:^ty or_const``
val ty_ci = mk_type("comminst", [])
val ty_or_const = mk_type("ssa_or_const", [])
val t_Var = mk_const("INL", ty_ssa --> or_const ty_ssa)
val t_Const = mk_const("INR", ty_val --> or_const ty_ssa)
val t_Var = mk_const("Var", ty_ssa --> ty_or_const)
val t_Const = mk_const("Const", ty_type --> ty_val --> ty_list ty_val --> ty_or_const)
val t_SSA = mk_const("SSA", ty_str --> ty_ssa)
fun mk_ssa s = mk_comb(t_SSA, fromMLstring s)
fun mk_some x =
......@@ -76,10 +76,10 @@ struct
end
(* Reads an SSA variable, replacing global variables with constants using the
given context. Returns a term of type ``:ssavar or_const or_error``.
given context. Returns a term of type ``:ssa_or_const or_error``.
*)
fun ssa_var _ (Local, v) = mk_return(mk_comb(t_Var, mk_ssa v))
| ssa_var (env : env_context) (Global, v) = mk_lift(t_Const, #get_global env v)
| ssa_var (env : env_context) (Global, v) = #get_global env v
fun parse_mem_order (ord : string) : term =
if exists (fn x => x = ord) mem_orders then
......@@ -90,8 +90,8 @@ struct
fun parse_new_stack_clause (env : env_context) (tokens : uir_token list)
: (term * uir_token list) =
let
val ty = mk_type("new_stack_clause", [or_const ty_ssa])
val ty_pair = mk_prod(or_const ty_ssa, ty_type)
val ty = mk_type("new_stack_clause", [ty_or_const])
val ty_pair = mk_prod(ty_or_const, ty_type)
in
case tokens of
Word "PASS_VALUES" :: Type tys :: Parens vals :: rest =>
......@@ -100,13 +100,13 @@ struct
map (fn (ty, v) =>
case v of
SSA v => list_mk_lift(
mk_const(",", or_const ty_ssa --> ty_type --> ty_pair),
mk_const(",", ty_or_const --> ty_type --> ty_pair),
[ssa_var env v, ty])
| _ => raise ParseError "PASS_VALUES expected SSA arguments")
(ListPair.zipEq(parse_type_list env tys, vals)),
ty_pair)), rest)
| Word "THROW_EXC" :: SSA exc :: rest =>
(mk_lift(mk_const("ThrowExc", or_const ty_ssa --> ty),
(mk_lift(mk_const("ThrowExc", ty_or_const --> ty),
ssa_var env exc), rest)
| _ => raise ParseError "expected newStackClause (PASS_VALUES or THROW_EXC)"
end
......@@ -143,20 +143,23 @@ struct
| _ => raise ParseError(inst ^ " lhs contains non-SSA-var")
(* Parses a list of tokens into a Mu IR instruction. Returns a term of type
``:ssavar instruction or_error``.
``:instruction or_error``.
*)
fun parse_inst (env : env_context) (tokens : uir_token list) : term =
let
val ty_inst = mk_type("instruction", [ty_ssa])
val ty_expr = mk_type("expression", [or_const ty_ssa])
val ty_inst = mk_type("instruction", [])
val ty_expr = mk_type("expression", [])
val t_ref = mk_return(mk_const("REF", ty_reft))
val t_ptr = mk_return(mk_const("PTR", ty_reft))
val t_na = mk_return(mk_const("NOT_ATOMIC", mk_type("memory_order", [])))
val t_void = mk_return(mk_const("Void", ty_type))
val t_null = mk_return(infer_comb("INR", [infer_comb("RefV", [
mk_const("Void", ty_type),
mk_const("NONE", ``:addr option``)
], ty_val)], ``:ssavar or_const``))
val t_null = mk_return(list_mk_comb(t_Const, [
``Ref (Type Void)``,
infer_comb("RefV", [
mk_const("Void", ty_type),
mk_const("NONE", ``:addr option``)
], ty_val),
mk_list([], ty_val)]))
fun two_tys tys =
let
val (t1, rest) = take_one_type tys
......@@ -360,40 +363,38 @@ struct
let
fun param (SSA v) = ssa_var env v
| param _ = raise ParseError "expected SSA variable"
fun params vs = mk_sequence(map param vs, or_const ty_ssa)
val ty_dest = ``:ssavar destination``
fun params vs = mk_sequence(map param vs, ty_or_const)
val ty_dest = ``:destination``
val ty_destopt = mk_type("option", [ty_dest])
val x = mk_var("x", ty_list (or_const ty_ssa))
val x = mk_var("x", ty_list ty_or_const)
fun dest label vs = mk_lift(
mk_abs(x, mk_pair(infer_comb("BlockLabel",
[fromMLstring label], ty_blabel), x)),
params vs)
fun calldata(fsig, callee, args) =
let val fsig' = parse_funcsig env fsig in
lift_record(mk_type("calldata", [ty_ssa]), [
("name", mk_bind(
ssa_var env callee,
mk_const("get_callee",
or_const ty_ssa --> or_error (mk_sum(ty_ssa, ty_funcn))))),
("signature", fsig'),
("args", params args),
("convention",
mk_return(mk_const("Mu", mk_type("callconvention", []))))
])
let val ty_f = ty_or_const --> or_error(mk_sum(ty_ssa, ty_funcn))
val name = mk_bind(ssa_var env callee, mk_const("get_callee", ty_f))
val conv = mk_return(mk_const("Mu", mk_type("callconvention", [])))
in lift_record(mk_type("calldata", []), [
("name", name),
("signature", parse_funcsig env fsig),
("args", params args),
("convention", conv)
])
end
fun exc_clause [SSA (Local, l1), Parens a1, SSA (Local, l2), Parens a2] =
lift_record(mk_type("resumption_data", [ty_ssa]), [
lift_record(mk_type("resumption_data", []), [
("normal_dest", dest l1 a1),
("exceptional_dest", mk_lift(
mk_const("SOME", ty_dest --> ty_destopt), dest l2 a2))
])
| exc_clause [SSA (Local, l1), Parens a1] =
lift_record(mk_type("resumption_data", [ty_ssa]), [
lift_record(mk_type("resumption_data", []), [
("normal_dest", dest l1 a1),
("exceptional_dest", mk_return(mk_const("NONE", ty_destopt)))
])
| exc_clause _ = raise ParseError "invalid syntax for EXC clause"
val ty_inst = mk_type("terminst", [ty_ssa])
val ty_inst = mk_type("terminst", [])
in case tokens of
[Word "RET", Parens vs] => ir_ap("Ret", [params vs], ty_inst)
| [Word "THROW", v] => ir_ap("Throw", [param v], ty_inst)
......@@ -419,7 +420,7 @@ struct
SSA (Local, l1), Parens a1, SSA (Local, l2), Parens a2] =>
let val ty_int1 = mk_return(mk_comb(
mk_const("Int", ty_num --> ty_type),
lift_num ty_num Arbnum.one))
mk_num 1))
in ir_ap("Branch2",
[ssa_var env cond, dest l1 a1, dest l2 a2],
ty_inst)
......@@ -497,10 +498,10 @@ struct
mk_lift(mk_abs(x, mk_pair(mk_ssa v, x)), parse_type env t)::accum)
| get_args [] accum = List.rev accum
| get_args _ _ = raise ParseError "expected <type> %arg in block args"
val inst_ty = mk_type("instruction", [ty_ssa])
val inst_ty = mk_type("instruction", [])
in case header of
[SSA (Local, label), Parens arg_tokens, Colon] =>
(label, lift_record(mk_type("bblock", [ty_ssa]), [
(label, lift_record(mk_type("bblock", []), [
("args",
mk_sequence(get_args arg_tokens [], mk_prod(ty_ssa, ty_type))),
("body",
......@@ -511,7 +512,7 @@ struct
("keepalives", mk_return(mk_list([], ty_ssa)))
]))
| [SSA (Local, label), Parens arg_tokens, Brackets [SSA (Local, exc)], Colon] =>
(label, lift_record(mk_type("bblock", [ty_ssa]), [
(label, lift_record(mk_type("bblock", []), [
("args",
mk_sequence(get_args arg_tokens [], mk_prod(ty_ssa, ty_type))),
("body",
......@@ -528,30 +529,20 @@ struct
let
val block_tokens = split_by_header (fn l => List.last l = Colon)
(filter (fn l => l <> []) lines)
val ty_bb = mk_type("bblock", [ty_ssa])
val ty_bb = mk_type("bblock", [])
val ty_lb = mk_prod(ty_blabel, ty_bb)
val ty_bbmap = mk_fmap_ty(ty_blabel, ty_bb)
val t_b = mk_var("b", ty_bb)
val blocks = mk_sequence(
map (fn block => let val (l, b) = parse_block env block in mk_lift(
mk_abs(t_b,
mk_pair(infer_comb("BlockLabel", [fromMLstring l], ty_blabel), t_b)),
b)
end)
block_tokens,
map (fn (l, b) =>
mk_lift(mk_abs(t_b,
mk_pair(infer_comb("BlockLabel", [fromMLstring l], ty_blabel),
t_b)), b))
(map (parse_block env) block_tokens),
ty_lb)
in
lift_record(mk_type("function", []), [
("signature", fsig),
("entry_block", mk_lift(mk_const("FST", ty_lb --> ty_blabel),
mk_lift(mk_const("HD", ty_list ty_lb --> ty_lb),
blocks))),
("blocks", mk_lift(
infer_comb("FOLDL", [
mk_const("FUPDATE", ty_bbmap --> ty_lb --> ty_bbmap),
mk_const("FEMPTY", ty_bbmap)],
ty_list ty_lb --> ty_bbmap),
blocks))
("blocks", blocks)
])
end
......
......@@ -30,6 +30,8 @@ sig
val mk_bind : term * term -> term
val mk_sequence : term list * hol_type -> term
val mk_lift : term * term -> term
val mk_num : int -> term
val mk_singleton : term -> term
val list_mk_lift : term * term list -> term
val lift_record : hol_type * (string * term) list -> term
val ty_pat : string -> term list -> term
......
structure ParserHelpers :> ParserHelpers =
struct
open HolKernel Term Parse TypeBase
open sumSyntax
open listSyntax
open numSyntax
open sumSyntax
open sumMonadTheory
open uvmTypesTheory
open uvmErrorsTheory
......@@ -30,7 +31,7 @@ struct
val ty_type = mk_type("uvm_type", [])