diff options
| author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2018-12-20 16:56:21 +0000 |
|---|---|---|
| committer | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2019-01-02 13:12:17 +0000 |
| commit | dc6f48b574c4215e46b79612a01d0c203698e3f8 (patch) | |
| tree | d0571af4450fc17b9ac629d057a02569a0b5e01b | |
| parent | cd6d793698133a6282e7d380a393cc9ee48dd464 (diff) | |
| download | sail-riscv-dc6f48b574c4215e46b79612a01d0c203698e3f8.zip sail-riscv-dc6f48b574c4215e46b79612a01d0c203698e3f8.tar.gz sail-riscv-dc6f48b574c4215e46b79612a01d0c203698e3f8.tar.bz2 | |
Note Coq externals for min/max_nat, add workaround for Coq issue
| -rw-r--r-- | prelude.sail | 4 | ||||
| -rw-r--r-- | riscv_extras.v | 10 |
2 files changed, 12 insertions, 2 deletions
diff --git a/prelude.sail b/prelude.sail index 20951af..c0e93e9 100644 --- a/prelude.sail +++ b/prelude.sail @@ -956,11 +956,11 @@ val lor_int = "lor_int" : (int, int) -> int val land_int = "land_int" : (int, int) -> int val lxor_int = "lxor_int" : (int, int) -> int -val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat +val min_nat = {ocaml: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat val min_int = {ocaml: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int -val max_nat = {ocaml: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat +val max_nat = {ocaml: "max_int", lem: "max", coq: "max_nat", c: "max_int"} : (nat, nat) -> nat val max_int = {ocaml: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int diff --git a/riscv_extras.v b/riscv_extras.v index 820e3f3..6de320d 100644 --- a/riscv_extras.v +++ b/riscv_extras.v @@ -132,3 +132,13 @@ Definition prerr_string (_:string) : unit := tt. Definition putchar {T} (_:T) : unit := tt. Require DecimalString. Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). + +(* The constraint solver can do this itself, but a Coq bug puts + anonymous_subproof into the term instead of an actual subproof. *) +Lemma n_leading_spaces_fact {w__0} : + w__0 >= 0 -> exists ex17629_ : Z, 1 + w__0 = 1 + ex17629_ /\ 0 <= ex17629_. +intro. +exists w__0. +omega. +Qed. +Hint Resolve n_leading_spaces_fact : sail. |