diff options
| author | Jon French | 2018-12-28 15:12:00 +0000 |
|---|---|---|
| committer | Jon French | 2018-12-28 15:12:00 +0000 |
| commit | b59fba68e535f39b6285ec7f4f693107b6e34148 (patch) | |
| tree | 3135513ac4b23f96b41f3d521990f1ce91206c99 /lib/vector_inc.sail | |
| parent | 9f6a95882e1d3d057bcb83d098ba1b63925a4d1f (diff) | |
| parent | 2c887e7d01331d3165120695594eac7a2650ec03 (diff) | |
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'lib/vector_inc.sail')
| -rw-r--r-- | lib/vector_inc.sail | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail index b8e1b91f..daba99be 100644 --- a/lib/vector_inc.sail +++ b/lib/vector_inc.sail @@ -65,7 +65,7 @@ val bitvector_access = { lem: "access_vec_inc", coq: "access_vec_inc", c: "vector_access" -} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit +} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit val plain_vector_access = { ocaml: "access", @@ -83,7 +83,7 @@ val bitvector_update = { lem: "update_vec_inc", coq: "update_vec_inc", c: "vector_update" -} : forall 'n, 'n >= 0. (bits('n), int, bit) -> bits('n) +} : forall 'n 'm, 0 <= 'm < 'n. (bits('n), atom('m), bit) -> bits('n) val plain_vector_update = { ocaml: "update", @@ -91,7 +91,7 @@ val plain_vector_update = { lem: "update_list_inc", coq: "update_list_inc", c: "vector_update" -} : forall 'n ('a : Type). (vector('n, inc, 'a), int, 'a) -> vector('n, inc, 'a) +} : forall 'n 'm ('a : Type), 0 <= 'm < 'n. (vector('n, inc, 'a), atom('m), 'a) -> vector('n, inc, 'a) overload vector_update = {bitvector_update, plain_vector_update} @@ -123,7 +123,7 @@ val vector_update_subrange = { lem: "update_subrange_vec_inc", c: "vector_update_subrange", coq: "update_subrange_vec_inc" -} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) +} : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) // Some ARM specific builtins |