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

Commit 296c77dc authored by Adam Nelson's avatar Adam Nelson
Browse files

Rearrange helper files, add syntax sugar

- Split up DefineUtils into separate files following the HOL convention
  (e.g., fooScript + fooLib)
- sumMonadTheory merged into monadsTheory, which now contains list and
  option monads as well
- List and option monads used to clean up code throughout the project
- Extra unicode symbols/operators in syntaxSugarTheory
parent 87ce7ba5
......@@ -3,7 +3,7 @@ struct
open HolKernel Parse Term boolLib bossLib
open listTheory llistTheory optionTheory pred_setTheory finite_mapTheory sptreeTheory
open listSyntax stringSyntax sptreeSyntax
open sumMonadTheory uvmTypesTheory uvmMemoryTheory
open monadsTheory uvmTypesTheory uvmMemoryTheory
val lhdtl_lunfold = prove(
``LHD (LUNFOLD f x) = OPTION_MAP SND (f x)
......
open HolKernel bossLib
signature extraTactics =
sig
val pair_case_tac : tactic
val multi_case_tac : tactic
val rw_assums : thm list -> tactic
end
structure extraTactics :> extraTactics =
struct
open HolKernel boolLib bossLib
open Parse
open Term
val pair_case_tac =
qpat_assum `_ (_: α # β) = _` (fn a =>
let val v = concl a |> lhs |> dest_comb |> #2 in
if pairSyntax.is_pair v then NO_TAC else Cases_on `^v`
end) ORELSE
qpat_assum `_ = _ (_: α # β)` (fn a =>
let val v = concl a |> rhs |> dest_comb |> #2 in
if pairSyntax.is_pair v then NO_TAC else Cases_on `^v`
end)
fun multi_case_tac x =
(REPEAT ((BasicProvers.FULL_CASE_TAC ORELSE pair_case_tac) >> fs[] >> rw[])) x
fun rw_assums xs =
POP_ASSUM_LIST (map_every (assume_tac o REWRITE_RULE xs) o rev)
end
open HolKernel bossLib
signature DefineUtils =
signature monadsLib =
sig
val pair_case_tac : tactic
val multi_case_tac : tactic
val rw_assums : thm list -> tactic
val define_sum : string * string * hol_type * string * hol_type -> unit
val define_num_newtype : string * string -> unit
val define_monad : string * (hol_type -> hol_type) * term * term -> unit
end
structure DefineUtils :> DefineUtils =
structure monadsLib :> monadsLib =
struct
open HolKernel boolLib bossLib
open Parse
open Term
val num_infixes_defined: bool ref = ref false
val monad_infixes_defined: bool ref = ref false
val pair_case_tac =
qpat_assum `_ (_: α # β) = _` (fn a =>
let val v = concl a |> lhs |> dest_comb |> #2 in
if pairSyntax.is_pair v then NO_TAC else Cases_on `^v`
end) ORELSE
qpat_assum `_ = _ (_: α # β)` (fn a =>
let val v = concl a |> rhs |> dest_comb |> #2 in
if pairSyntax.is_pair v then NO_TAC else Cases_on `^v`
end)
fun multi_case_tac x =
(REPEAT ((BasicProvers.FULL_CASE_TAC ORELSE pair_case_tac) >> fs[] >> rw[])) x
fun rw_assums xs =
POP_ASSUM_LIST (map_every (assume_tac o REWRITE_RULE xs) o rev)
fun define_sum(name : string, inl : string, inl_ty : hol_type, inr : string,
inr_ty : hol_type) : unit =
let
......@@ -41,42 +24,6 @@ struct
})
end
fun define_num_newtype(type_name : string, ctor_name : string) : unit =
let
val _ = Datatype[QUOTE type_name, QUOTE " = ", QUOTE ctor_name, QUOTE " num"]
val ty = mk_type(type_name, [])
val ctor = mk_const(ctor_name, mk_type("num", []) --> ty)
val suc_name = type_name ^ "_suc"
val lt_name = type_name ^ "_lt"
val dest_name = type_name ^ "_dest"
val suc_def = Define(QUOTE suc_name::` x = case x of ^ctor n => ^ctor (SUC n)`)
val lt_def = Define(QUOTE lt_name::` x y = case x of ^ctor m => case y of ^ctor n => m < n`)
val dest_def = Define(QUOTE dest_name::` (^ctor n) = n`)
val suc = mk_const(suc_name, ty --> ty)
val lt = mk_const(lt_name, ty --> ty --> mk_type("bool", []))
val _ = Q.store_thm(type_name ^ "_lt_suc[simp]",
`x. ^lt x (^suc x)`,
Cases >> rw[suc_def, lt_def])
val _ = Q.store_thm(type_name ^ "_lt_trans",
`x y z. ^lt x y ^lt y z ^lt x z`,
Cases >> Cases >> Cases >> rw[lt_def])
val _ = Q.store_thm(type_name ^ "_lt_equiv[simp]",
`x y. ^lt x y m n. (x = ^ctor m) (y = ^ctor n) m < n`,
Cases >> Cases >> rw[lt_def])
in
(* Define "precedes" (U+227A = ≺) and "predeces or equivalent" (U+227C = ≼) operators,
* which are different Unicode chars from < and ≤. These new symbols are required for
* overloaded comparisons because ≤ is not defined as an overload. *)
if not (!num_infixes_defined) then (
set_fixity "≺" (Infix(NONASSOC, 450));
set_fixity "≼" (Infix(NONASSOC, 450));
num_infixes_defined := true
) else ();
overload_on("≺", ``^lt``);
overload_on("≼", ``λl r. (^lt l r) (l = r)``)
(* TeX_notation {hol="≺", TeX=("\\ensuremath{\\prec}", 1)}; *)
end
fun QDefine(quoted : string frag list) =
let fun unquote (QUOTE s) = QUOTE s
| unquote (ANTIQUOTE s) = QUOTE s
......@@ -144,6 +91,9 @@ struct
overload_on("ap", Term [QUOTE ap_name]);
overload_on("<$>", Term [QUOTE lift_name]);
overload_on("APPLICATIVE_FAPPLY", Term [QUOTE ap_name])
(* (* FIXME: This doesn't quite work. It makes the __monad_sequence terms appear. *)
; Unicode.unicode_version{tmnm="__monad_assign", u=UnicodeChars.leftarrow}
*)
end
end
open HolKernel Parse boolLib bossLib;
open sumSyntax
open DefineUtils
open monadsLib
(* A monad for sum types, roughly equivalent to Haskell's `Either` monad. It
favors the left side of a sum type (although `bind_right` can be used to bind
over the right side instead). Also contains several utility functions for sum
types.
(* Monads for options, lists, and sum types.
The sum type monad is roughly equivalent to Haskell's `Either` monad. It
favors the left side of a sum type, although `bind_right` can be used to bind
over the right side instead.
*)
val _ = new_theory "sumMonad"
val _ = new_theory "monads"
val _ = define_monad("option", (fn a => mk_type("option", [a])),
``SOME``, ``OPTION_BIND``)
val _ = define_monad("list", (fn a => mk_type("list", [a])),
``combin$C CONS []``, ``LIST_BIND``)
val _ = define_monad("left", (fn a => mk_sum(a, mk_vartype "'right")),
``INL``, ``λx fn. sum_CASE x fn INR``)
(*
val return_left_INL = store_thm("return_left_INL[simp]",
``return_left x = INL x``,
simp[definition "return_left_def"])
*)
(* Utility functions and theorems for the sum monad. *)
val bind_left_INR_simp = store_thm("bind_left_INR_simp[simp]",
``bind_left (INR x) f = INR x``, simp[])
......
......@@ -4,7 +4,7 @@ struct
open listSyntax
open numSyntax
open sumSyntax
open sumMonadTheory
open monadsTheory
open uvmTypesTheory
open uvmErrorsTheory
open uvmValuesTheory
......@@ -86,7 +86,7 @@ struct
foldl
(fn ((arg, ty), acc) => list_mk_comb(
mk_thy_const{
Thy="sumMonad",
Thy="monads",
Name="ap_left",
Ty=type_of acc --> type_of arg --> or_error ty
}, [acc, arg]))
......
open HolKernel bossLib
signature syntaxSugarLib =
sig
val prefix_op : string -> unit
val define_num_newtype : string * string * string -> unit
end
structure syntaxSugarLib :> syntaxSugarLib =
struct
open HolKernel boolLib bossLib
open Parse
open Term
(* Quickly generate prefix operators *)
fun prefix_op optr =
add_rule {term_name = optr,
fixity = Prefix 780,
pp_elements = [TOK optr],
paren_style = OnlyIfNecessary,
block_style = (AroundEachPhrase, (PP.CONSISTENT, 0))}
(* Superscript "modifier" letters *)
exception NoSuperscript of string
fun sup "a" = "ᵃ"
| sup "b" = "ᵇ"
| sup "c" = "ᶜ"
| sup "d" = "ᵈ"
| sup "e" = "ᵉ"
| sup "f" = "ᶠ"
| sup "g" = "ᵍ"
| sup "i" = "ⁱ"
| sup "k" = "ᵏ"
| sup "l" = "ˡ"
| sup "m" = "ᵐ"
| sup "n" = "ⁿ"
| sup "o" = "ᵒ"
| sup "p" = "ᵖ"
| sup "s" = "ˢ"
| sup "t" = "ᵗ"
| sup "u" = "ᵘ"
| sup "v" = "ᵛ"
| sup "x" = "ˣ"
| sup "z" = "ᶻ"
| sup letter = raise NoSuperscript letter
(* Defines a newtype wrapper for a numeric ID, complete with Unicode operators
for less/less-eq, construction, and destructuring.
*)
fun define_num_newtype(type_name : string, ctor_name : string, letter : string) : unit =
let
val _ = Datatype[QUOTE type_name, QUOTE " = ", QUOTE ctor_name, QUOTE " num"]
val ty = mk_type(type_name, [])
val ctor = mk_const(ctor_name, mk_type("num", []) --> ty)
val suc_name = type_name ^ "_suc"
val lt_name = type_name ^ "_lt"
val dest_name = type_name ^ "_dest"
val suc_def = Define(QUOTE suc_name::` x = case x of ^ctor n => ^ctor (SUC n)`)
val lt_def = Define(QUOTE lt_name::` x y = case x of ^ctor m => case y of ^ctor n => m < n`)
val dest_def = Define(QUOTE dest_name::` (^ctor n) = n`)
val suc = mk_const(suc_name, ty --> ty)
val lt = mk_const(lt_name, ty --> ty --> mk_type("bool", []))
val dest = mk_const(dest_name, ty --> mk_type("num", []))
val _ = Q.store_thm(type_name ^ "_lt_suc[simp]",
`x. ^lt x (^suc x)`,
Cases >> rw[suc_def, lt_def])
val _ = Q.store_thm(type_name ^ "_lt_trans",
`x y z. ^lt x y ^lt y z ^lt x z`,
Cases >> Cases >> Cases >> rw[lt_def])
val _ = Q.store_thm(type_name ^ "_lt_equiv[simp]",
`x y. ^lt x y m n. (x = ^ctor m) (y = ^ctor n) m < n`,
Cases >> Cases >> rw[lt_def])
val ctor_sym = sup letter ^ "#"
val _ = TeX_notation{
hol=ctor_sym,
TeX=("\\ensuremath{{}^{" ^ letter ^ "}\\#}", 1)
}
in
(* Define "precedes" (U+227A = ≺) and "predeces or equivalent" (U+227C = ≼) operators,
* which are different Unicode chars from < and ≤. These new symbols are required for
* overloaded comparisons because ≤ is not defined as an overload. *)
overload_on("≺", lt);
overload_on("≼", ``λl r. (^lt l r) (l = r)``);
overload_on("suc", suc);
overload_on("⍽", dest);
prefix_op(ctor_sym);
overload_on(ctor_sym, ctor)
end
end
open HolKernel Parse boolLib bossLib
open listTheory
open syntaxSugarLib
val _ = new_theory "syntaxSugar"
val _ = ParseExtras.tight_equality()
val _ = app prefix_op ["%", "∁", "⍽", "✔", "✘"]
val _ = set_fixity "≺" (Infix(NONASSOC, 450))
val _ = set_fixity "≼" (Infix(NONASSOC, 450))
val _ = overload_on("∁", ``COMPL``)
val _ = Unicode.unicode_version{tmnm="CONS", u="∷"}
val _ = TeX_notation {hol="%", TeX=("\\%", 1)}
(* For some reason HOL doesn't define this symbol by default... *)
val _ = TeX_notation{hol="⊌", TeX=("\\ensuremath{\\uplus}", 1)}
val _ = export_theory()
......@@ -4,8 +4,7 @@ open ParserHelpers
open TypeParser
open ValueParser
open CodeParser
open wordsTheory
open sumMonadTheory
open monadsTheory
open uvmTypesTheory
open uvmValuesTheory
open uvmMemoryTheory
......
......@@ -2,7 +2,7 @@ open HolKernel Parse boolLib bossLib
open ParserHelpers
open TypeParser
open sumMonadTheory
open monadsTheory
open uvmTypesTheory
val _ = new_theory "typesTest"
......
......@@ -4,7 +4,7 @@ open ParserHelpers
open TypeParser
open ValueParser
open wordsTheory
open sumMonadTheory
open monadsTheory
open uvmTypesTheory
open uvmValuesTheory
open uvmMemoryTheory
......
......@@ -2,7 +2,9 @@ open HolKernel Parse boolLib bossLib
open uvmTypesTheory
open stringTheory
open DefineUtils
open monadsTheory
open monadsLib
open syntaxSugarTheory
val _ = new_theory "uvmErrors"
......@@ -32,6 +34,9 @@ val _ = define_sum("errorM",
"OK", ``:α``,
"Fail", ``:(β, γ) gen_uvm_error``)
val _ = overload_on("✔", ``OK``)
val _ = overload_on("✘", ``Fail``)
val assert_def = Define`
assert (cond : bool) (err : (α, β) gen_uvm_error) : (one, α, β) errorM =
if cond then OK () else Fail err
......
......@@ -4,8 +4,8 @@ open uvmTypesTheory
open uvmValuesTheory
open uvmErrorsTheory
open uvmMemoryTheory
open sumMonadTheory
open DefineUtils
open monadsTheory
open extraTactics
open alistTheory
open finite_mapTheory
......@@ -542,7 +542,7 @@ val map_terminst_def = Define`
val var_list_def = Define `var_list (Var s) = [s] var_list _ = []`
val new_stack_clause_vars_def = Define`
new_stack_clause_vars (PassValues vs) = LIST_BIND vs (var_list o FST)
new_stack_clause_vars (PassValues vs) = vs >>= var_list o FST
new_stack_clause_vars (ThrowExc e) = var_list e
`
......@@ -597,7 +597,7 @@ val expr_types_def = Define`
by the instruction.
*)
val inst_vars_def = Define`
inst_vars (Assign vs e) = (LIST_BIND (expr_vars e) var_list, nub vs)
inst_vars (Assign vs e) = (expr_vars e >>= var_list, nub vs)
inst_vars (Load v _ _ src _) = ([src], [v])
inst_vars (Store src _ _ dst _) = (var_list src, [dst])
inst_vars (CmpXchg v1 v2 _ _ _ _ _ loc exp des) =
......@@ -660,22 +660,22 @@ val comminst_types_def = Define`
*)
val terminst_vars_def = Define`
terminst_vars (inst : terminst) : ssavar list # ssavar list =
let dest_vars dest = LIST_BIND (SND dest) var_list in
let dest_vars dest = SND dest >>= var_list in
let rd_vars rd =
dest_vars rd.normal_dest ++
option_CASE rd.exceptional_dest [] dest_vars in
case inst of
| Ret vals => [], nub (LIST_BIND vals var_list)
| Ret vals => [], nub (vals >>= var_list)
| Throw v => [], nub (var_list v)
| Call vs cd rd =>
left_list cd.name,
nub (vs ++ LIST_BIND cd.args var_list ++ rd_vars rd)
| TailCall cd => left_list cd.name, nub (LIST_BIND cd.args var_list)
nub (vs ++ (cd.args >>= var_list) ++ rd_vars rd)
| TailCall cd => left_list cd.name, nub (cd.args >>= var_list)
| Branch1 dst => [], nub (dest_vars dst)
| Branch2 cond dst1 dst2 => var_list cond, nub (dest_vars dst1 ++ dest_vars dst2)
| Switch _ cond def_dst branches =>
var_list cond,
nub (dest_vars def_dst ++ LIST_BIND branches (dest_vars o SND))
nub (dest_vars def_dst ++ (branches >>= dest_vars o SND))
| Watchpoint NONE _ rd => [], nub (rd_vars rd)
| Watchpoint (SOME (id, dst)) _ rd => [], nub (dest_vars dst ++ rd_vars rd)
| WPBranch id dst1 dst2 => [], nub (dest_vars dst1 ++ dest_vars dst2)
......@@ -721,8 +721,8 @@ val _ = Datatype`
val block_vars_def = Define`
block_vars (block : bblock) : ssavar list =
nub (MAP FST block.args ++
option_CASE block.exc [] (λe. [e]) ++
LIST_BIND block.body inst_all_vars ++
option_CASE block.exc [] return ++
(block.body >>= inst_all_vars) ++
terminst_all_vars block.exit ++
block.keepalives)
`
......@@ -731,7 +731,7 @@ val block_types_def = Define`
block_types (block : bblock) : (ssavar # uvm_type) list =
block.args ++
option_CASE block.exc [] (λe. [(e, Ref (Type Void))]) ++
LIST_BIND block.body inst_types ++
(block.body >>= inst_types) ++
terminst_types block.exit
`
......
......@@ -4,8 +4,9 @@ open uvmMemoryTheory
open uvmIRTheory
open uvmValuesTheory
open uvmErrorsTheory
open sumMonadTheory
open DefineUtils
open monadsTheory
open monadsLib
open syntaxSugarTheory
open alistTheory
open combinTheory
......@@ -16,11 +17,10 @@ open pairTheory
open pred_setTheory
open sptreeTheory
open lcsymtacs
open monadsyntax
val _ = new_theory "uvmInstructionSemantics"
val _ = add_monadsyntax()
val _ = reveal "C" (* The C (flip) combinator is used in this theory *)
val _ = monadsyntax.add_monadsyntax()
val _ = reveal "C"
(* reg_reader is a reader monad over a memory region. It provides syntax sugar
for operations on a thread's registers. *)
......@@ -127,7 +127,7 @@ val eval_expr_def = Define`
| SUB => return $-
| MUL => return $*
| _ => K (Fail (NotImplemented "most binops"));
C CONS [] <$> K (int_binop op v1 v2)
return <$> K (int_binop op v1 v2)
od
eval_expr ssa (CmpOp op _ v1 v2) = (
if (op = EQ op = NE) then do
......@@ -189,14 +189,14 @@ val eval_expr_def = Define`
assert_type_eq ty (type_of_value v) "EXTRACTELEMENT array/vector";
assert_type_eq ity (type_of_value i) "EXTRACTELEMENT index";
off <- get_int_as_num "EXTRACTELEMENT index" i;
C CONS [] <$> value_offset_get v off
return <$> value_offset_get v off
od
∧ eval_expr get (InsertElement ty ity v1 i v2) = do
v1 <- get v1; i <- get i; v2 <- get v2;
assert_type_eq ty (type_of_value v1) "INSERTELEMENT array/vector";
assert_type_eq ity (type_of_value i) "INSERTELEMENT index";
off <- get_int_as_num "INSERTELEMENT index" i;
C CONS [] <$> value_offset_update v1 off v2
return <$> value_offset_update v1 off v2
od*)
(* TODO: ShuffleVector *)
eval_expr _ (ShuffleVector _ _ _ _ _) =
......@@ -227,7 +227,7 @@ val eval_expr_def = Define`
rv <- HD (getc ssa ref);
ia <- K (get_iref_addr rv);
case ia.ty of
| Hybrid fts _ => C CONS [] <$> K (get_field_iref rv (LENGTH fts))
| Hybrid fts _ => return <$> K (get_field_iref rv (LENGTH fts))
| _ => K (Fail (InvalidIR "GETVARPARTIREF of non-hybrid"))
od
`
......@@ -235,16 +235,16 @@ val eval_expr_def = Define`
(* μVM instructions are split up into operations before they are executed. *)
val compile_inst_def = Define`
compile_inst (ssa : ssa_map) (Assign vs e) : opn list =
[Nm (CURRY ZIP (LIST_BIND vs (MAP FST o ssa)) <$> eval_expr ssa e)]
[Nm (CURRY ZIP (vs >>= MAP FST o ssa) <$> eval_expr ssa e)]
compile_inst (ssa : ssa_map) (Load dst _ _ src ord) : opn list =
(let lds = MAP2 (λs d. Ld (s >>= K o get_iref_addr) (FST d))
(get ssa src) (ssa dst) in
case ord of
| NOT_ATOMIC => lds
| RELAXED => lds
| CONSUME => LIST_BIND lds (λld. [ld; Rec])
| ACQUIRE => LIST_BIND lds (λld. [ld; Rec])
| SEQ_CST => LIST_BIND lds (λld. [Com; Rec; ld; Rec])
| CONSUME => do ld <- lds; [ld; Rec] od
| ACQUIRE => do ld <- lds; [ld; Rec] od
| SEQ_CST => do ld <- lds; [Com; Rec; ld; Rec] od
| _ => [Nm (K (Fail (InvalidIR "unsupported memory order for LOAD")))])
compile_inst ssa (Store src _ _ dst ord) =
(let sts = MAP2
......@@ -253,8 +253,8 @@ val compile_inst_def = Define`
case ord of
| NOT_ATOMIC => sts
| RELAXED => sts
| RELEASE => LIST_BIND sts (λst. [Com; st])
| SEQ_CST => LIST_BIND sts (λst. [Com; st])
| RELEASE => do st <- sts; [Com; st] od
| SEQ_CST => do st <- sts; [Com; st] od
| _ => [St (K (Fail (InvalidIR "unsupported memory order for STORE")))])
compile_inst _ (CmpXchg _ _ _ _ _ _ _ _ _ _) =
[Nm (K (Fail (NotImplemented "CMPXCHG")))]
......@@ -278,7 +278,7 @@ val compile_inst_def = Define`
val compile_terminst_def = Define`
compile_terminst (lbl : block_label -> num) (ssa : ssa_map) (Ret vs) =
[Cmd (DoPopStack o NOR <$> sequence (LIST_BIND vs (getc ssa)))]
[Cmd (DoPopStack o NOR <$> sequence (vs >>= getc ssa))]
compile_terminst _ ssa (Throw v) =
[Cmd (DoPopStack o EXC [] <$> HD (getc ssa v))]
compile_terminst lbl ssa (Call dsts cdata rdata) = (
......@@ -303,12 +303,12 @@ val compile_terminst_def = Define`
| INR name => return name in
let jmps = (λn e. SOME <|
nor_jump := (lbl (FST rdata.normal_dest), n);
exc_jump := OPTION_MAP (λed. lbl (FST ed), e) rdata.exceptional_dest
exc_jump := (λed. lbl (FST ed), e) <$> rdata.exceptional_dest
|>) <$> (FLAT <$> mapM get_dst (SND rdata.normal_dest))
<*> (FLAT <$> mapM get_dst (option_CASE rdata.exceptional_dest [] SND)) in
[Cmd (DoPushStack <$> fname
<*> return cdata.signature
<*> sequence (LIST_BIND cdata.args (getc ssa))
<*> sequence (cdata.args >>= getc ssa)
<*> jmps)])
compile_terminst _ ssa (TailCall cdata) =
(let fname =
......@@ -322,10 +322,10 @@ val compile_terminst_def = Define`
| INR name => return name in
[Cmd (DoPushStack <$> fname
<*> return cdata.signature
<*> sequence (LIST_BIND cdata.args (getc ssa))
<*> sequence (cdata.args >>= getc ssa)
<*> return NONE)])
compile_terminst lbl ssa (Branch1 (b, vs)) =
[Cmd (DoJump <$> return (lbl b) <*> sequence (LIST_BIND vs (getc ssa)))]
[Cmd (DoJump <$> return (lbl b) <*> sequence (vs >>= getc ssa))]
compile_terminst lbl ssa (Branch2 p d1 d2) =
[Cmd (HD (getc ssa p) >>= K o get_int1_as_bool >>= λis1.
let compile_dest = lbl ## C LIST_BIND (getc ssa) in
......@@ -334,7 +334,7 @@ val compile_terminst_def = Define`
compile_terminst lbl ssa (Switch _ p default cases) =
[Cmd (HD (getc ssa p) >>= λpv.
let (b, vs) = (lbl ## I) (option_CASE (ALOOKUP cases pv) default I) in
DoJump <$> return b <*> sequence (LIST_BIND vs (getc ssa)))]
DoJump <$> return b <*> sequence (vs >>= getc ssa))]
compile_terminst _ _ (Watchpoint _ _ _) =
[Cmd (K (Fail (NotImplemented "WATCHPOINT")))]
compile_terminst _ _ (WPBranch _ _ _) =
......@@ -356,9 +356,13 @@ val compile_block_def = Define`
let (cs, ssas, _) = FOLDL alloc_cells ([], FEMPTY, 0) (block_types block) in
<|
regs := cs;
exc_param := OPTION_BIND block.exc (OPTION_MAP (FST o HD) o FLOOKUP ssas);
exc_param := do
ssa <- block.exc;
regs <- FLOOKUP ssas ssa;
return (FST (HD regs))
od;
opns :=
LIST_BIND block.body (compile_inst (FAPPLY ssas)) ++
(block.body >>= compile_inst (FAPPLY ssas)) ++
compile_terminst lbl (FAPPLY ssas) block.exit