diff options
author | Jonathan Protzenko | 2023-01-27 16:59:38 -0800 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | 1d6742c059cf53e73c9bc66cec7ac1f857830e78 (patch) | |
tree | c1d1058b9fee9f12e9410b0a8930941728b2695c /backends/lean | |
parent | 8f27b1e64ef3dab9a314df4794ae8c361a8ef3dd (diff) |
WIP lots of stuff
Diffstat (limited to 'backends/lean')
-rw-r--r-- | backends/lean/primitives.lean | 35 |
1 files changed, 30 insertions, 5 deletions
diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean index 3b1d39fc..dc2314fc 100644 --- a/backends/lean/primitives.lean +++ b/backends/lean/primitives.lean @@ -1,3 +1,5 @@ +import Lean + ------------- -- PRELUDE -- ------------- @@ -10,14 +12,14 @@ inductive error where | arrayOutOfBounds: error | maximumSizeExceeded: error | panic: error -deriving Repr +deriving Repr, BEq open error inductive result (α : Type u) where | ret (v: α): result α | fail (e: error): result α -deriving Repr +deriving Repr, BEq open result @@ -48,7 +50,9 @@ instance : Pure result where def massert (b:Bool) : result Unit := if b then return () else fail assertionFailure --- Machine integers +---------------------- +-- MACHINE INTEGERS -- +---------------------- -- NOTE: we reuse the USize type from prelude.lean, because at least we know -- it's defined in an idiomatic style that is going to make proofs easy (and @@ -123,13 +127,16 @@ macro_rules #eval UInt32.ofNatCore 0 (by intlit) -- Test behavior... -#eval USize.checked_sub 10 20 +#eval assert! USize.checked_sub 10 20 == fail integerOverflow; 0 + #eval USize.checked_sub 20 10 -- NOTE: compare with concrete behavior here, which I do not think we want #eval USize.sub 0 1 #eval UInt8.add 255 255 --- Vectors +------------- +-- VECTORS -- +------------- def vec (α : Type u) := { l : List α // List.length l < USize.size } @@ -176,3 +183,21 @@ def vec_push_back (α : Type u) (v : vec α) (x : α) : { res: result (vec α) / -- TODO: strengthen post-condition above and do a demo to show that we can -- safely eliminate the `fail` case return (vec_len Nat x) + +-------------------- +-- ASSERT COMMAND -- +-------------------- + +open Lean Elab Command Term Meta + +syntax (name := assert) "#assert" term: command + +@[command_elab assert] +def assertImpl : CommandElab := fun (stx: Syntax) => do + logInfo "Hello World" + +def ignore (a: Prop) (x: a) := () + +#eval ignore (2 == 2) (by simp) + +#assert (2 == 2) |