diff options
| -rw-r--r-- | backends/lean/primitives.lean | 27 | ||||
| -rw-r--r-- | compiler/Extract.ml | 2 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Hashmap/Funs.lean | 4 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Hashmap/Primitives.lean | 31 |
4 files changed, 51 insertions, 13 deletions
diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean index b68df5f0..d86c0423 100644 --- a/backends/lean/primitives.lean +++ b/backends/lean/primitives.lean @@ -83,12 +83,13 @@ def massert (b:Bool) : result Unit := -- and -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean -- which both contain a fair amount of reasoning already! -def USize.checked_sub (n: USize) (m: Nat): result USize := +def USize.checked_sub (n: USize) (m: USize): result USize := -- NOTE: the test USize.toNat n - m >= 0 seems to always succeed? - if USize.toNat n >= m then + if n >= m then let n' := USize.toNat n - let r := USize.ofNatCore (n' - m) (by - have h: n' - m <= n' := by + let m' := USize.toNat n + let r := USize.ofNatCore (n' - m') (by + have h: n' - m' <= n' := by apply Nat.sub_le_of_le_add case h => rewrite [ Nat.add_comm ]; apply Nat.le_add_left apply Nat.lt_of_le_of_lt h @@ -102,6 +103,24 @@ def USize.checked_sub (n: USize) (m: Nat): result USize := def USize.checked_mul (n: USize) (m: USize): result USize := sorry def USize.checked_div (n: USize) (m: USize): result USize := sorry +-- One needs to perform a little bit of reasoning in order to successfully +-- inject constants into USize, so we provide a general-purpose macro + +syntax "intlit" : tactic + +macro_rules + | `(tactic| intlit) => `(tactic| + match USize.size, usize_size_eq with + | _, Or.inl rfl => decide + | _, Or.inr rfl => decide) + +-- This is how the macro is expected to be used +#eval USize.ofNatCore 0 (by intlit) + +-- Also works for other integer types (at the expense of a needless disjunction) +#eval UInt32.ofNatCore 0 (by intlit) + +-- Test behavior... #eval USize.checked_sub 10 20 #eval USize.checked_sub 20 10 -- NOTE: compare with concrete behavior here, which I do not think we want diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 6bda6376..9496fcf9 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -573,7 +573,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) F.pp_print_string fmt (int_name sv.int_ty); F.pp_print_string fmt ".ofNatCore "; Z.pp_print fmt sv.value; - F.pp_print_string fmt (" (by simp))")) + F.pp_print_string fmt (" (by intlit))")) | Bool b -> let b = if b then "true" else "false" in F.pp_print_string fmt b diff --git a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean b/tests/lean/hashmap_on_disk/Hashmap/Funs.lean index a4f2e3e0..c67a37ff 100644 --- a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean +++ b/tests/lean/hashmap_on_disk/Hashmap/Funs.lean @@ -15,10 +15,10 @@ def hashmap_hash_map_allocate_slots_loop_fwd (T : Type) (slots : vec (hashmap_list_t T)) (n : USize) : result (vec (hashmap_list_t T)) := - if n > (USize.ofNatCore 0 (by simp)) + if n > (USize.ofNatCore 0 (by intlit)) then do let slots0: vec (hashmap_list_t T) <- @vec_push_back (hashmap_list_t T) slots HashmapListNil - let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by simp)) + let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 else ret slots termination_by hashmap_hash_map_allocate_slots_loop_fwd _ _ n => n diff --git a/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean b/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean index 83de98db..d86c0423 100644 --- a/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean @@ -22,12 +22,12 @@ deriving Repr open result -- TODO: is there automated syntax for these discriminators? -def is_ret (α: Type) (r: result α): Bool := +def is_ret {α: Type} (r: result α): Bool := match r with | result.ret _ => true | result.fail _ => false -def eval_global (α: Type) (x: result α) (h: is_ret α x): α := +def eval_global {α: Type} (x: result α) (h: is_ret x): α := match x with | result.fail _ => by contradiction | result.ret x => x @@ -83,12 +83,13 @@ def massert (b:Bool) : result Unit := -- and -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean -- which both contain a fair amount of reasoning already! -def USize.checked_sub (n: USize) (m: Nat): result USize := +def USize.checked_sub (n: USize) (m: USize): result USize := -- NOTE: the test USize.toNat n - m >= 0 seems to always succeed? - if USize.toNat n >= m then + if n >= m then let n' := USize.toNat n - let r := USize.ofNatCore (n' - m) (by - have h: n' - m <= n' := by + let m' := USize.toNat n + let r := USize.ofNatCore (n' - m') (by + have h: n' - m' <= n' := by apply Nat.sub_le_of_le_add case h => rewrite [ Nat.add_comm ]; apply Nat.le_add_left apply Nat.lt_of_le_of_lt h @@ -102,6 +103,24 @@ def USize.checked_sub (n: USize) (m: Nat): result USize := def USize.checked_mul (n: USize) (m: USize): result USize := sorry def USize.checked_div (n: USize) (m: USize): result USize := sorry +-- One needs to perform a little bit of reasoning in order to successfully +-- inject constants into USize, so we provide a general-purpose macro + +syntax "intlit" : tactic + +macro_rules + | `(tactic| intlit) => `(tactic| + match USize.size, usize_size_eq with + | _, Or.inl rfl => decide + | _, Or.inr rfl => decide) + +-- This is how the macro is expected to be used +#eval USize.ofNatCore 0 (by intlit) + +-- Also works for other integer types (at the expense of a needless disjunction) +#eval UInt32.ofNatCore 0 (by intlit) + +-- Test behavior... #eval USize.checked_sub 10 20 #eval USize.checked_sub 20 10 -- NOTE: compare with concrete behavior here, which I do not think we want |