diff options
Diffstat (limited to 'kvx/lib/PseudoAsmblock.v')
| -rw-r--r-- | kvx/lib/PseudoAsmblock.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kvx/lib/PseudoAsmblock.v b/kvx/lib/PseudoAsmblock.v index 336e315c..b33ea1bd 100644 --- a/kvx/lib/PseudoAsmblock.v +++ b/kvx/lib/PseudoAsmblock.v @@ -27,10 +27,16 @@ Module Pregmap := EMap(PregEq). Definition regset := Pregmap.t val. +Module AsmNotations. + (* Declare Scope asm. *) Notation "a # b" := (a b) (at level 1, only parsing) : asm. Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. +Open Scope asm. + +End AsmNotations. +Import AsmNotations. Definition to_Machrs (rs: regset): Mach.regset := fun (r:mreg) => rs r. @@ -44,7 +50,6 @@ Definition set_from_Machrs (mrs: Mach.regset) (rs: regset): regset := end. Local Open Scope option_monad_scope. -Local Open Scope asm. Record state: Type := State { _rs: regset; _m: mem }. Definition outcome := option state. |