diff options
| author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-11-25 17:56:10 +0000 |
|---|---|---|
| committer | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-11-25 17:56:10 +0000 |
| commit | 1a653fc6207b8cb20204af6b2ccabab48a020945 (patch) | |
| tree | ace99ff81dfb2fd7acd7bf056a197de4605f34c5 /handwritten_support | |
| parent | 0e42c867fba498746405d2b878a12fd4d143c5d8 (diff) | |
| download | sail-riscv-1a653fc6207b8cb20204af6b2ccabab48a020945.zip sail-riscv-1a653fc6207b8cb20204af6b2ccabab48a020945.tar.gz sail-riscv-1a653fc6207b8cb20204af6b2ccabab48a020945.tar.bz2 | |
Fix RV32 Lem build
Diffstat (limited to 'handwritten_support')
| -rw-r--r-- | handwritten_support/0.11/mem_metadata.lem | 4 | ||||
| -rw-r--r-- | handwritten_support/mem_metadata.lem | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/handwritten_support/0.11/mem_metadata.lem b/handwritten_support/0.11/mem_metadata.lem index 24bcecb..8a8c070 100644 --- a/handwritten_support/0.11/mem_metadata.lem +++ b/handwritten_support/0.11/mem_metadata.lem @@ -6,11 +6,11 @@ open import Sail2_operators_mwords open import Sail2_prompt_monad open import Sail2_prompt -val write_ram : forall 'rv 'e 'n. Size 'n => write_kind -> mword ty64 -> integer -> mword 'n -> unit -> monad 'rv bool 'e +val write_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => write_kind -> mword 'a -> integer -> mword 'n -> unit -> monad 'rv bool 'e let write_ram wk addr width data meta = write_mem wk () addr width data -val read_ram : forall 'rv 'e 'n. Size 'n => read_kind -> mword ty64 -> integer -> bool -> monad 'rv (mword 'n * unit) 'e +val read_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => read_kind -> mword 'a -> integer -> bool -> monad 'rv (mword 'n * unit) 'e let read_ram rk addr width read_tag = read_mem rk () addr width >>= (fun (data : mword 'n) -> return (data, ())) diff --git a/handwritten_support/mem_metadata.lem b/handwritten_support/mem_metadata.lem index 24bcecb..8a8c070 100644 --- a/handwritten_support/mem_metadata.lem +++ b/handwritten_support/mem_metadata.lem @@ -6,11 +6,11 @@ open import Sail2_operators_mwords open import Sail2_prompt_monad open import Sail2_prompt -val write_ram : forall 'rv 'e 'n. Size 'n => write_kind -> mword ty64 -> integer -> mword 'n -> unit -> monad 'rv bool 'e +val write_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => write_kind -> mword 'a -> integer -> mword 'n -> unit -> monad 'rv bool 'e let write_ram wk addr width data meta = write_mem wk () addr width data -val read_ram : forall 'rv 'e 'n. Size 'n => read_kind -> mword ty64 -> integer -> bool -> monad 'rv (mword 'n * unit) 'e +val read_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => read_kind -> mword 'a -> integer -> bool -> monad 'rv (mword 'n * unit) 'e let read_ram rk addr width read_tag = read_mem rk () addr width >>= (fun (data : mword 'n) -> return (data, ())) |