diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/prompt.lem | 8 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 1 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 60 |
3 files changed, 37 insertions, 32 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 8e1e1f67..3efdd163 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -83,7 +83,7 @@ type reg_name = * specifies a part of the field, indexed w.r.t. the register as a whole *) | Reg_f_slice of string * nat * direction * string * slice * slice -type outcome 'a = +type outcome 'e 'a = (* Request to read memory, value is location to read followed by registers that location depended * on when mode.track_values, integer is size to read, followed by registers that were used in * computing that size *) @@ -123,14 +123,14 @@ type outcome 'a = (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally * provide a handler. *) - | Escape (* currently without handlers *) (* of maybe (unit -> outcome 'a) *) + | Escape 'e (* currently without handlers *) (* of maybe (unit -> outcome 'a) *) (* Stop for incremental stepping, function can be used to display function call data *) | Done of 'a -type M 'a = outcome 'a +type M 'e 'a = outcome 'e 'a -val return : forall 'a. 'a -> M 'a +val return : forall 'e 'a. 'a -> M 'e 'a let return a = Done a val (>>=) : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index d2364397..ace65b3b 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -4,6 +4,7 @@ open import Vector open import Arch type i = integer +type number = integer let length l = integerFromNat (length l) diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index f79f8eff..b5b0c37f 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -3,7 +3,7 @@ open import Vector open import Arch (* 'a is result type, 'e is error type *) -type M 's 'e 'a = 's -> (either 'a 'e * 's) +type State 's 'e 'a = 's -> (either 'a 'e * 's) type memstate = map integer (list bit) @@ -21,25 +21,27 @@ let rec ints_aux acc x = let ints = ints_aux [] -val return : forall 's 'e 'a. 'a -> M 's 'e 'a +val return : forall 's 'e 'a. 'a -> State 's 'e 'a let return a s = (Left a,s) -val bind : forall 's 'e 'a 'b. M 's 'e 'a -> ('a -> M 's 'e 'b) -> M 's 'e 'b +val bind : forall 's 'e 'a 'b. State 's 'e 'a -> ('a -> State 's 'e 'b) -> State 's 'e 'b let bind m f s = match m s with | (Left a,s') -> f a s' | (Right error,s') -> (Right error,s') end -val exit : forall 's 'e 'a. 'e -> M 's 'e 'a +val exit : forall 's 'e. 'e -> State 's 'e unit let exit e s = (Right e,s) let (>>=) = bind + +val (>>): forall 's 'e 'a 'b. State 's 'e 'a -> State 's 'e 'b -> State 's 'e 'b let (>>) m n = m >>= fun _ -> n -val read_writeEA : forall 'e. unit -> M state 'e (integer * integer) +val read_writeEA : forall 'e. unit -> State state 'e (integer * integer) let read_writeEA () s = (Left s.writeEA,s) -val write_writeEA : forall 'e. integer -> integer -> M state 'e unit +val write_writeEA : forall 'e. integer -> integer -> State state 'e unit let write_writeEA addr l s = (Left (), <| s with writeEA = (addr,l) |>) val byte_chunks : forall 'a. integer -> list 'a -> list (list 'a) @@ -63,46 +65,46 @@ let read_memstate s addr = findWithDefault addr (replicate 8 Undef) s val write_memstate : memstate -> (integer * list bit) -> memstate let write_memstate s (addr,bits) = Map.insert addr bits s -val read_memory : forall 'e. integer -> integer -> M state 'e (vector bit) +val read_memory : forall 'e. integer -> integer -> State state 'e (vector bit) let read_memory addr l s = let bytes = List.map (compose (read_memstate s.memstate) ((+) addr)) (ints l) in (Left (V (foldl (++) [] bytes) 0 defaultDir),s) -val write_memory : forall 'e. integer -> integer -> vector bit -> M state 'e unit +val write_memory : forall 'e. integer -> integer -> vector bit -> State state 'e unit let write_memory addr l (V bits _ _) s = let addrs = List.map ((+) addr) (ints l) in let bytes = byte_chunks l bits in (Left (), <| s with memstate = foldl write_memstate s.memstate (zip addrs bytes) |>) -val read_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> M state 'e (vector bit) +val read_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> State state 'e (vector bit) let read_reg_range reg i j s = let v = slice (read_regstate s reg) i j in (Left v,s) -val read_reg_bit : forall 'e. register -> integer (*nat*) -> M state 'e bit +val read_reg_bit : forall 'e. register -> integer (*nat*) -> State state 'e bit let read_reg_bit reg i s = let v = access (read_regstate s reg) i in (Left v,s) -val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bit -> M state 'e unit +val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bit -> State state 'e unit let write_reg_range reg i j v s = let v' = update (read_regstate s reg) i j v in let s' = write_regstate s reg v' in (Left (),s') -val write_reg_bit : forall 'e. register -> integer (*nat*) -> bit -> M state 'e unit +val write_reg_bit : forall 'e. register -> integer (*nat*) -> bit -> State state 'e unit let write_reg_bit reg i bit s = let v = read_regstate s reg in let v' = update_pos v i bit in let s' = write_regstate s reg v' in (Left (),s') -val read_reg : forall 'e. register -> M state 'e (vector bit) +val read_reg : forall 'e. register -> State state 'e (vector bit) let read_reg reg s = let v = read_regstate s reg in (Left v,s) -val write_reg : forall 'e. register -> vector bit -> M state 'e unit +val write_reg : forall 'e. register -> vector bit -> State state 'e unit let write_reg reg v s = let s' = write_regstate s reg v in (Left (),s') @@ -128,45 +130,45 @@ let rec foreach_dec (i,stop,by) vars body = else ((),vars) -val foreachM_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) -let rec foreachM_inc (i,stop,by) vars body = +val foreachState_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (unit * 'vars) +let rec foreachState_inc (i,stop,by) vars body = if i <= stop then body i vars >>= fun (_,vars) -> - foreachM_inc (i + by,stop,by) vars body + foreachState_inc (i + by,stop,by) vars body else return ((),vars) -val foreachM_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) -let rec foreachM_dec (i,stop,by) vars body = +val foreachState_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (unit * 'vars) +let rec foreachState_dec (i,stop,by) vars body = if i >= stop then body i vars >>= fun (_,vars) -> - foreachM_dec (i - by,stop,by) vars body + foreachState_dec (i - by,stop,by) vars body else return ((),vars) -val read_reg_field : forall 'e. register -> register_field -> M state 'e (vector bit) +val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bit) let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfield) -val write_reg_field : forall 'e. register -> register_field -> vector bit -> M state 'e unit +val write_reg_field : forall 'e. register -> register_field -> vector bit -> State state 'e unit let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield) -val read_reg_bitfield : forall 'e. register -> register_bitfield -> M state 'e bit +val read_reg_bitfield : forall 'e. register -> register_bitfield -> State state 'e bit let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit) -val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> M state 'e unit +val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> State state 'e unit let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit) val write_reg_field_range : forall 'e. register -> register_field -> integer -> integer -> - vector bit -> M state 'e unit + vector bit -> State state 'e unit let write_reg_field_range reg rfield i j v = let (i',j') = field_indices rfield in write_reg_range reg i' j' v val write_reg_field_bit : forall 'e. register -> register_field -> integer -> - bit -> M state 'e unit + bit -> State state 'e unit let write_reg_field_bit reg rfield i v = let (i',_) = field_indices rfield in write_reg_bit reg (i + i') v @@ -190,3 +192,5 @@ let read_two_regs r1 r2 = read_reg r1 >>= fun v1 -> read_reg r2 >>= fun v2 -> return (v1 ^^ v2) + +type M 'e 'a = State state 'e 'a |