diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 3 | ||||
| -rw-r--r-- | lib/coq/Sail2_string.v | 22 |
2 files changed, 22 insertions, 3 deletions
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 12c1a9d9..a0ef467e 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -127,6 +127,3 @@ Definition projT1_m {rv e} {P:Z -> Prop} (x: monad rv {x : Z & P x} e) : monad r Definition derive_m {rv e} {P Q:Z -> Prop} (x : monad rv {x : Z & P x} e) `{forall x, ArithFact (P x) -> ArithFact (Q x)} : monad rv {x : Z & (ArithFact (Q x))} e := x >>= fun y => returnm (build_ex (projT1 y)). - -Definition memea {rv e} {T:Type} (_:T) (_:Z) : monad rv unit e := returnm tt. -Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt. diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v index 1208e00e..c8bf5f9f 100644 --- a/lib/coq/Sail2_string.v +++ b/lib/coq/Sail2_string.v @@ -138,3 +138,25 @@ Definition hex_bits_28_matches_prefix s := hex_bits_n_matches_prefix 28 s. Definition hex_bits_32_matches_prefix s := hex_bits_n_matches_prefix 32 s. Definition hex_bits_33_matches_prefix s := hex_bits_n_matches_prefix 33 s. +Local Definition zero : N := Ascii.N_of_ascii "0". +Local Fixpoint string_of_N (limit : nat) (n : N) (acc : string) : string := +match limit with +| O => acc +| S limit' => + let (d,m) := N.div_eucl n 10 in + let acc := String (Ascii.ascii_of_N (m + zero)) acc in + if N.ltb 0 d then string_of_N limit' d acc else acc +end. +Local Fixpoint pos_limit p := +match p with +| xH => S O +| xI p | xO p => S (pos_limit p) +end. +Definition string_of_int (z : Z) : string := +match z with +| Z0 => "0" +| Zpos p => string_of_N (pos_limit p) (Npos p) "" +| Zneg p => String "-" (string_of_N (pos_limit p) (Npos p) "") +end. + + |