1 files changed, 61 insertions, 0 deletions
diff --git a/lib/coq/State_lifting.v b/lib/coq/State_lifting.v
new file mode 100644
index 00000000..8342b04c
--- /dev/null
+++ b/lib/coq/State_lifting.v
@@ -0,0 +1,61 @@
+Require Import Sail.Values.
+Require Import Sail.Prompt_monad.
+Require Import Sail.Prompt.
+Require Import Sail.State_monad.
+Import ListNotations.
+
+(* Lifting from prompt monad to state monad *)
+(*val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e*)
+Fixpoint liftState {Regval Regs A E} (ra : register_accessors Regs Regval) (m : monad Regval A E) : monadS Regs A E :=
+ match m with
+  | (Done a)                   => returnS a
+  | (Read_mem rk a sz k)       => bindS (read_mem_bytesS rk a sz)       (fun v => liftState ra (k v))
+  | (Read_memt rk a sz k)      => bindS (read_memt_bytesS rk a sz)      (fun v => liftState ra (k v))
+  | (Write_mem wk a sz v k)    => bindS (write_mem_bytesS wk a sz v)    (fun v => liftState ra (k v))
+  | (Write_memt wk a sz v t k) => bindS (write_memt_bytesS wk a sz v t) (fun v => liftState ra (k v))
+  | (Read_reg r k)             => bindS (read_regvalS ra r)             (fun v => liftState ra (k v))
+  | (Excl_res k)               => bindS (excl_resultS tt)               (fun v => liftState ra (k v))
+  | (Choose _ k)               => bindS (choose_boolS tt)               (fun v => liftState ra (k v))
+  | (Write_reg r v k)          => seqS (write_regvalS ra r v)           (liftState ra k)
+  | (Write_ea _ _ _ k)         => liftState ra k
+  | (Footprint k)              => liftState ra k
+  | (Barrier _ k)              => liftState ra k
+  | (Print _ k)                => liftState ra k (* TODO *)
+  | (Fail descr)               => failS descr
+  | (Exception e)              => throwS e
+end.
+
+Local Open Scope bool_scope.
+
+(*val emitEventS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> event 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)*)
+Definition emitEventS {Regval Regs} `{forall (x y : Regval), Decidable (x = y)} (ra : register_accessors Regs Regval) (e : event Regval) (s : sequential_state Regs) : option (sequential_state Regs) :=
+match e with
+  | E_read_mem _ addr sz v =>
+     option_bind (get_mem_bytes addr sz s) (fun '(v', _) =>
+     if generic_eq v' v then Some s else None)
+  | E_read_memt _ addr sz (v, tag) =>
+     option_bind (get_mem_bytes addr sz s) (fun '(v', tag') =>
+     if generic_eq v' v && generic_eq tag' tag then Some s else None)
+  | E_write_mem _ addr sz v success =>
+     if success then Some (put_mem_bytes addr sz v B0 s) else None
+  | E_write_memt _ addr sz v tag success =>
+     if success then Some (put_mem_bytes addr sz v tag s) else None
+  | E_read_reg r v =>
+     let (read_reg, _) := ra in
+     option_bind (read_reg r s.(ss_regstate)) (fun v' =>
+     if generic_eq v' v then Some s else None)
+  | E_write_reg r v =>
+     let (_, write_reg) := ra in
+     option_bind (write_reg r v s.(ss_regstate)) (fun rs' =>
+     Some {| ss_regstate := rs'; ss_memstate := s.(ss_memstate); ss_tagstate := s.(ss_tagstate) |})
+  | _ => Some s
+end.
+
+Local Close Scope bool_scope.
+
+(*val runTraceS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> trace 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)*)
+Fixpoint runTraceS {Regval Regs} `{forall (x y : Regval), Decidable (x = y)} (ra : register_accessors Regs Regval) (t : trace Regval) (s : sequential_state Regs) : option (sequential_state Regs) :=
+match t with
+  | [] => Some s
+  | e :: t' => option_bind (emitEventS ra e s) (runTraceS ra t')
+end.