diff options
| author | Son Ho | 2023-07-12 15:41:29 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-12 15:41:29 +0200 |
| commit | 59e4a06480b5365f48dc68de80f44841f94094ed (patch) | |
| tree | 00644dda183bff958381183939f4eb54d97ed242 /backends/lean/Base/Arith | |
| parent | a18d899a2c2b9bdd36f4a5a4b70472c12a835a96 (diff) | |
Improve the handling of arithmetic bounds
Diffstat (limited to 'backends/lean/Base/Arith')
| -rw-r--r-- | backends/lean/Base/Arith/Arith.lean | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean index 3557d350..20420f36 100644 --- a/backends/lean/Base/Arith/Arith.lean +++ b/backends/lean/Base/Arith/Arith.lean @@ -339,13 +339,17 @@ def scalarTac : Tactic.TacticM Unit := do let add (e : Expr) : Tactic.TacticM Unit := do let ty ← inferType e let _ ← Utils.addDeclTac (← mkFreshUserName `h) e ty (asLet := false) - add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Usize []]) add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []]) add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []]) add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []]) -- Reveal the concrete bounds - TODO: not too sure about that. -- Maybe we should reveal the "concrete" bounds (after normalization) - Utils.simpAt [``Scalar.max, ``Scalar.min, ``Scalar.cMin, ``Scalar.cMax] [] [] .wildcard + Utils.simpAt [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax, + ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min, + ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max, + ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min, + ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max + ] [] [] .wildcard -- Apply the integer tactic intTac |