mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-18 02:44:12 +00:00
Compare commits
2 Commits
replace
...
std_comman
| Author | SHA1 | Date | |
|---|---|---|---|
|
c8a9b249ac | ||
|
|
2b485c0dc3 |
@@ -207,28 +207,6 @@ the first matching constructor, or else fails.
|
||||
-/
|
||||
syntax (name := constructor) "constructor" : tactic
|
||||
|
||||
/--
|
||||
Applies the second constructor when
|
||||
the goal is an inductive type with exactly two constructors, or fails otherwise.
|
||||
```
|
||||
example : True ∨ False := by
|
||||
left
|
||||
trivial
|
||||
```
|
||||
-/
|
||||
syntax (name := left) "left" : tactic
|
||||
|
||||
/--
|
||||
Applies the second constructor when
|
||||
the goal is an inductive type with exactly two constructors, or fails otherwise.
|
||||
```
|
||||
example {p q : Prop} (h : q) : p ∨ q := by
|
||||
right
|
||||
exact h
|
||||
```
|
||||
-/
|
||||
syntax (name := right) "right" : tactic
|
||||
|
||||
/--
|
||||
* `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`,
|
||||
or else fails.
|
||||
@@ -398,7 +376,7 @@ syntax locationWildcard := " *"
|
||||
A hypothesis location specification consists of 1 or more hypothesis references
|
||||
and optionally `⊢` denoting the goal.
|
||||
-/
|
||||
syntax locationHyp := (ppSpace colGt term:max)+ patternIgnore(ppSpace (atomic("|" noWs "-") <|> "⊢"))?
|
||||
syntax locationHyp := (ppSpace colGt term:max)+ ppSpace patternIgnore( atomic("|" noWs "-") <|> "⊢")?
|
||||
|
||||
/--
|
||||
Location specifications are used by many tactics that can operate on either the
|
||||
@@ -894,53 +872,6 @@ The tactic `nomatch h` is shorthand for `exact nomatch h`.
|
||||
macro "nomatch " es:term,+ : tactic =>
|
||||
`(tactic| exact nomatch $es:term,*)
|
||||
|
||||
/--
|
||||
Acts like `have`, but removes a hypothesis with the same name as
|
||||
this one if possible. For example, if the state is:
|
||||
|
||||
```lean
|
||||
f : α → β
|
||||
h : α
|
||||
⊢ goal
|
||||
```
|
||||
|
||||
Then after `replace h := f h` the state will be:
|
||||
|
||||
```lean
|
||||
f : α → β
|
||||
h : β
|
||||
⊢ goal
|
||||
```
|
||||
|
||||
whereas `have h := f h` would result in:
|
||||
|
||||
```lean
|
||||
f : α → β
|
||||
h† : α
|
||||
h : β
|
||||
⊢ goal
|
||||
```
|
||||
|
||||
This can be used to simulate the `specialize` and `apply at` tactics of Coq.
|
||||
-/
|
||||
syntax (name := replace) "replace" haveDecl : tactic
|
||||
|
||||
/--
|
||||
`repeat' tac` runs `tac` on all of the goals to produce a new list of goals,
|
||||
then runs `tac` again on all of those goals, and repeats until `tac` fails on all remaining goals.
|
||||
-/
|
||||
syntax (name := repeat') "repeat' " tacticSeq : tactic
|
||||
|
||||
/--
|
||||
`repeat1' tac` applies `tac` to main goal at least once. If the application succeeds,
|
||||
the tactic is applied recursively to the generated subgoals until it eventually fails.
|
||||
-/
|
||||
syntax (name := repeat1') "repeat1' " tacticSeq : tactic
|
||||
|
||||
/-- `and_intros` applies `And.intro` until it does not make progress. -/
|
||||
syntax "and_intros" : tactic
|
||||
macro_rules | `(tactic| and_intros) => `(tactic| repeat' refine And.intro ?_ ?_)
|
||||
|
||||
end Tactic
|
||||
|
||||
namespace Attr
|
||||
|
||||
@@ -41,26 +41,4 @@ macro_rules
|
||||
| `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) =>
|
||||
expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
|
||||
|
||||
/--
|
||||
`iterate n tac` runs `tac` exactly `n` times.
|
||||
`iterate tac` runs `tac` repeatedly until failure.
|
||||
|
||||
`iterate`'s argument is a tactic sequence,
|
||||
so multiple tactics can be run using `iterate n (tac₁; tac₂; ⋯)` or
|
||||
```lean
|
||||
iterate n
|
||||
tac₁
|
||||
tac₂
|
||||
⋯
|
||||
```
|
||||
-/
|
||||
syntax "iterate" (ppSpace num)? ppSpace tacticSeq : tactic
|
||||
macro_rules
|
||||
| `(tactic| iterate $seq:tacticSeq) =>
|
||||
`(tactic| try ($seq:tacticSeq); iterate $seq:tacticSeq)
|
||||
| `(tactic| iterate $n $seq:tacticSeq) =>
|
||||
match n.1.toNat with
|
||||
| 0 => `(tactic| skip)
|
||||
| n+1 => `(tactic| ($seq:tacticSeq); iterate $(quote n) $seq:tacticSeq)
|
||||
|
||||
end Lean.Parser.Tactic
|
||||
|
||||
@@ -25,13 +25,9 @@ def leanMainFn := "_lean_main"
|
||||
|
||||
namespace LLVM
|
||||
-- TODO(bollu): instantiate target triple and find out what size_t is.
|
||||
def size_tType (llvmctx : LLVM.Context) : BaseIO (LLVM.LLVMType llvmctx) :=
|
||||
def size_tType (llvmctx : LLVM.Context) : IO (LLVM.LLVMType llvmctx) :=
|
||||
LLVM.i64Type llvmctx
|
||||
|
||||
-- TODO(bollu): instantiate target triple and find out what unsigned is.
|
||||
def unsignedType (llvmctx : LLVM.Context) : BaseIO (LLVM.LLVMType llvmctx) :=
|
||||
LLVM.i32Type llvmctx
|
||||
|
||||
-- Helper to add a function if it does not exist, and to return the function handle if it does.
|
||||
def getOrAddFunction (m : LLVM.Module ctx) (name : String) (type : LLVM.LLVMType ctx) : BaseIO (LLVM.Value ctx) := do
|
||||
match (← LLVM.getNamedFunction m name) with
|
||||
@@ -100,15 +96,6 @@ def getDecl (n : Name) : M llvmctx Decl := do
|
||||
| some d => pure d
|
||||
| none => throw s!"unknown declaration {n}"
|
||||
|
||||
def constInt8 (n : Nat) : M llvmctx (LLVM.Value llvmctx) := do
|
||||
LLVM.constInt8 llvmctx (UInt64.ofNat n)
|
||||
|
||||
def constInt64 (n : Nat) : M llvmctx (LLVM.Value llvmctx) := do
|
||||
LLVM.constInt64 llvmctx (UInt64.ofNat n)
|
||||
|
||||
def constIntSizeT (n : Nat) : M llvmctx (LLVM.Value llvmctx) := do
|
||||
LLVM.constIntSizeT llvmctx (UInt64.ofNat n)
|
||||
|
||||
def constIntUnsigned (n : Nat) : M llvmctx (LLVM.Value llvmctx) := do
|
||||
LLVM.constIntUnsigned llvmctx (UInt64.ofNat n)
|
||||
|
||||
@@ -175,14 +162,14 @@ def callLeanUnsignedToNatFn (builder : LLVM.Builder llvmctx)
|
||||
let retty ← LLVM.voidPtrType llvmctx
|
||||
let f ← getOrCreateFunctionPrototype mod retty "lean_unsigned_to_nat" argtys
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
let nv ← constIntUnsigned n
|
||||
let nv ← LLVM.constInt32 llvmctx (UInt64.ofNat n)
|
||||
LLVM.buildCall2 builder fnty f #[nv] name
|
||||
|
||||
def callLeanMkStringFromBytesFn (builder : LLVM.Builder llvmctx)
|
||||
(strPtr nBytes : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
|
||||
let fnName := "lean_mk_string_from_bytes"
|
||||
let retty ← LLVM.voidPtrType llvmctx
|
||||
let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
|
||||
let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.i64Type llvmctx]
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
LLVM.buildCall2 builder fnty fn #[strPtr, nBytes] name
|
||||
@@ -231,9 +218,9 @@ def callLeanAllocCtor (builder : LLVM.Builder llvmctx)
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
|
||||
let tag ← constIntUnsigned tag
|
||||
let num_objs ← constIntUnsigned num_objs
|
||||
let scalar_sz ← constIntUnsigned scalar_sz
|
||||
let tag ← LLVM.constInt32 llvmctx (UInt64.ofNat tag)
|
||||
let num_objs ← LLVM.constInt32 llvmctx (UInt64.ofNat num_objs)
|
||||
let scalar_sz ← LLVM.constInt32 llvmctx (UInt64.ofNat scalar_sz)
|
||||
LLVM.buildCall2 builder fnty fn #[tag, num_objs, scalar_sz] name
|
||||
|
||||
def callLeanCtorSet (builder : LLVM.Builder llvmctx)
|
||||
@@ -241,7 +228,7 @@ def callLeanCtorSet (builder : LLVM.Builder llvmctx)
|
||||
let fnName := "lean_ctor_set"
|
||||
let retty ← LLVM.voidType llvmctx
|
||||
let voidptr ← LLVM.voidPtrType llvmctx
|
||||
let unsigned ← LLVM.unsignedType llvmctx
|
||||
let unsigned ← LLVM.size_tType llvmctx
|
||||
let argtys := #[voidptr, unsigned, voidptr]
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
@@ -261,7 +248,7 @@ def callLeanAllocClosureFn (builder : LLVM.Builder llvmctx)
|
||||
(f arity nys : LLVM.Value llvmctx) (retName : String := "") : M llvmctx (LLVM.Value llvmctx) := do
|
||||
let fnName := "lean_alloc_closure"
|
||||
let retty ← LLVM.voidPtrType llvmctx
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.unsignedType llvmctx]
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.size_tType llvmctx]
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
LLVM.buildCall2 builder fnty fn #[f, arity, nys] retName
|
||||
@@ -270,7 +257,7 @@ def callLeanClosureSetFn (builder : LLVM.Builder llvmctx)
|
||||
(closure ix arg : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do
|
||||
let fnName := "lean_closure_set"
|
||||
let retty ← LLVM.voidType llvmctx
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.voidPtrType llvmctx]
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.voidPtrType llvmctx]
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
let _ ← LLVM.buildCall2 builder fnty fn #[closure, ix, arg] retName
|
||||
@@ -298,7 +285,7 @@ def callLeanCtorRelease (builder : LLVM.Builder llvmctx)
|
||||
(closure i : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do
|
||||
let fnName := "lean_ctor_release"
|
||||
let retty ← LLVM.voidType llvmctx
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx]
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
let _ ← LLVM.buildCall2 builder fnty fn #[closure, i] retName
|
||||
@@ -307,7 +294,7 @@ def callLeanCtorSetTag (builder : LLVM.Builder llvmctx)
|
||||
(closure i : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do
|
||||
let fnName := "lean_ctor_set_tag"
|
||||
let retty ← LLVM.voidType llvmctx
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.i8Type llvmctx]
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
let _ ← LLVM.buildCall2 builder fnty fn #[closure, i] retName
|
||||
@@ -360,31 +347,6 @@ def builderAppendBasicBlock (builder : LLVM.Builder llvmctx) (name : String) : M
|
||||
let fn ← builderGetInsertionFn builder
|
||||
LLVM.appendBasicBlockInContext llvmctx fn name
|
||||
|
||||
/--
|
||||
Add an alloca to the first BB of the current function. The builders final position
|
||||
will be the end of the BB that we came from.
|
||||
|
||||
If it is possible to put an alloca in the first BB this approach is to be preferred
|
||||
over putting it in other BBs. This is because mem2reg only inspects allocas in the first BB,
|
||||
leading to missed optimizations for allocas in other BBs.
|
||||
-/
|
||||
def buildPrologueAlloca (builder : LLVM.Builder llvmctx) (ty : LLVM.LLVMType llvmctx) (name : @&String := "") : M llvmctx (LLVM.Value llvmctx) := do
|
||||
let origBB ← LLVM.getInsertBlock builder
|
||||
|
||||
let fn ← builderGetInsertionFn builder
|
||||
if (← LLVM.countBasicBlocks fn) == 0 then
|
||||
throw "Attempt to obtain first BB of function without BBs"
|
||||
|
||||
let entryBB ← LLVM.getEntryBasicBlock fn
|
||||
match ← LLVM.getFirstInstruction entryBB with
|
||||
| some instr => LLVM.positionBuilderBefore builder instr
|
||||
| none => LLVM.positionBuilderAtEnd builder entryBB
|
||||
|
||||
let alloca ← LLVM.buildAlloca builder ty name
|
||||
LLVM.positionBuilderAtEnd builder origBB
|
||||
return alloca
|
||||
|
||||
|
||||
def buildWhile_ (builder : LLVM.Builder llvmctx) (name : String)
|
||||
(condcodegen : LLVM.Builder llvmctx → M llvmctx (LLVM.Value llvmctx))
|
||||
(bodycodegen : LLVM.Builder llvmctx → M llvmctx Unit) : M llvmctx Unit := do
|
||||
@@ -466,7 +428,7 @@ def buildIfThenElse_ (builder : LLVM.Builder llvmctx) (name : String) (brval :
|
||||
-- Recall that lean uses `i8` for booleans, not `i1`, so we need to compare with `true`.
|
||||
def buildLeanBoolTrue? (builder : LLVM.Builder llvmctx)
|
||||
(b : LLVM.Value llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx) := do
|
||||
LLVM.buildICmp builder LLVM.IntPredicate.NE b (← constInt8 0) name
|
||||
LLVM.buildICmp builder LLVM.IntPredicate.NE b (← LLVM.constInt8 llvmctx 0) name
|
||||
|
||||
def emitFnDeclAux (mod : LLVM.Module llvmctx)
|
||||
(decl : Decl) (cppBaseName : String) (isExternal : Bool) : M llvmctx (LLVM.Value llvmctx) := do
|
||||
@@ -551,8 +513,8 @@ def emitArgSlot_ (builder : LLVM.Builder llvmctx)
|
||||
| Arg.var x => emitLhsSlot_ x
|
||||
| _ => do
|
||||
let slotty ← LLVM.voidPtrType llvmctx
|
||||
let slot ← buildPrologueAlloca builder slotty "irrelevant_slot"
|
||||
let v ← callLeanBox builder (← constIntSizeT 0) "irrelevant_val"
|
||||
let slot ← LLVM.buildAlloca builder slotty "irrelevant_slot"
|
||||
let v ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "irrelevant_val"
|
||||
let _ ← LLVM.buildStore builder v slot
|
||||
return (slotty, slot)
|
||||
|
||||
@@ -574,7 +536,7 @@ def emitCtorSetArgs (builder : LLVM.Builder llvmctx)
|
||||
ys.size.forM fun i => do
|
||||
let zv ← emitLhsVal builder z
|
||||
let (_yty, yv) ← emitArgVal builder ys[i]!
|
||||
let iv ← constIntUnsigned i
|
||||
let iv ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat i)
|
||||
callLeanCtorSet builder zv iv yv
|
||||
emitLhsSlotStore builder z zv
|
||||
pure ()
|
||||
@@ -583,7 +545,7 @@ def emitCtor (builder : LLVM.Builder llvmctx)
|
||||
(z : VarId) (c : CtorInfo) (ys : Array Arg) : M llvmctx Unit := do
|
||||
let (_llvmty, slot) ← emitLhsSlot_ z
|
||||
if c.size == 0 && c.usize == 0 && c.ssize == 0 then do
|
||||
let v ← callLeanBox builder (← constIntSizeT c.cidx) "lean_box_outv"
|
||||
let v ← callLeanBox builder (← constIntUnsigned c.cidx) "lean_box_outv"
|
||||
let _ ← LLVM.buildStore builder v slot
|
||||
else do
|
||||
let v ← emitAllocCtor builder c
|
||||
@@ -595,7 +557,7 @@ def emitInc (builder : LLVM.Builder llvmctx)
|
||||
let xv ← emitLhsVal builder x
|
||||
if n != 1
|
||||
then do
|
||||
let nv ← constIntSizeT n
|
||||
let nv ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat n)
|
||||
callLeanRefcountFn builder (kind := RefcountKind.inc) (checkRef? := checkRef?) (delta := nv) xv
|
||||
else callLeanRefcountFn builder (kind := RefcountKind.inc) (checkRef? := checkRef?) xv
|
||||
|
||||
@@ -709,7 +671,7 @@ def emitPartialApp (builder : LLVM.Builder llvmctx) (z : VarId) (f : FunId) (ys
|
||||
|
||||
def emitApp (builder : LLVM.Builder llvmctx) (z : VarId) (f : VarId) (ys : Array Arg) : M llvmctx Unit := do
|
||||
if ys.size > closureMaxArgs then do
|
||||
let aargs ← buildPrologueAlloca builder (← LLVM.arrayType (← LLVM.voidPtrType llvmctx) (UInt64.ofNat ys.size)) "aargs"
|
||||
let aargs ← LLVM.buildAlloca builder (← LLVM.arrayType (← LLVM.voidPtrType llvmctx) (UInt64.ofNat ys.size)) "aargs"
|
||||
for i in List.range ys.size do
|
||||
let (yty, yv) ← emitArgVal builder ys[i]!
|
||||
let aslot ← LLVM.buildInBoundsGEP2 builder yty aargs #[← constIntUnsigned 0, ← constIntUnsigned i] s!"param_{i}_slot"
|
||||
@@ -718,7 +680,7 @@ def emitApp (builder : LLVM.Builder llvmctx) (z : VarId) (f : VarId) (ys : Array
|
||||
let retty ← LLVM.voidPtrType llvmctx
|
||||
let args := #[← emitLhsVal builder f, ← constIntUnsigned ys.size, aargs]
|
||||
-- '1 + ...'. '1' for the fn and 'args' for the arguments
|
||||
let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.voidPtrType llvmctx]
|
||||
let argtys := #[← LLVM.voidPtrType llvmctx]
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
let zv ← LLVM.buildCall2 builder fnty fn args
|
||||
@@ -760,18 +722,18 @@ def emitFullApp (builder : LLVM.Builder llvmctx)
|
||||
def emitLit (builder : LLVM.Builder llvmctx)
|
||||
(z : VarId) (t : IRType) (v : LitVal) : M llvmctx (LLVM.Value llvmctx) := do
|
||||
let llvmty ← toLLVMType t
|
||||
let zslot ← buildPrologueAlloca builder llvmty
|
||||
let zslot ← LLVM.buildAlloca builder llvmty
|
||||
addVartoState z zslot llvmty
|
||||
let zv ← match v with
|
||||
| LitVal.num v => emitNumLit builder t v
|
||||
| LitVal.str v =>
|
||||
let zero ← constIntUnsigned 0
|
||||
let zero ← LLVM.constIntUnsigned llvmctx 0
|
||||
let str_global ← LLVM.buildGlobalString builder v
|
||||
-- access through the global, into the 0th index of the array
|
||||
let strPtr ← LLVM.buildInBoundsGEP2 builder
|
||||
(← LLVM.opaquePointerTypeInContext llvmctx)
|
||||
str_global #[zero] ""
|
||||
let nbytes ← constIntSizeT v.utf8ByteSize
|
||||
let nbytes ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat (v.utf8ByteSize))
|
||||
callLeanMkStringFromBytesFn builder strPtr nbytes ""
|
||||
LLVM.buildStore builder zv zslot
|
||||
return zslot
|
||||
@@ -795,7 +757,7 @@ def callLeanCtorGetUsize (builder : LLVM.Builder llvmctx)
|
||||
(x i : LLVM.Value llvmctx) (retName : String) : M llvmctx (LLVM.Value llvmctx) := do
|
||||
let fnName := "lean_ctor_get_usize"
|
||||
let retty ← LLVM.size_tType llvmctx
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx]
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
LLVM.buildCall2 builder fnty fn #[x, i] retName
|
||||
@@ -822,7 +784,7 @@ def emitSProj (builder : LLVM.Builder llvmctx)
|
||||
| IRType.uint32 => pure ("lean_ctor_get_uint32", ← LLVM.i32Type llvmctx)
|
||||
| IRType.uint64 => pure ("lean_ctor_get_uint64", ← LLVM.i64Type llvmctx)
|
||||
| _ => throw s!"Invalid type for lean_ctor_get: '{t}'"
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx]
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let xval ← emitLhsVal builder x
|
||||
let offset ← emitOffset builder n offset
|
||||
@@ -929,7 +891,7 @@ def emitReset (builder : LLVM.Builder llvmctx) (z : VarId) (n : Nat) (x : VarId)
|
||||
(fun builder => do
|
||||
let xv ← emitLhsVal builder x
|
||||
callLeanDecRef builder xv
|
||||
let box0 ← callLeanBox builder (← constIntSizeT 0) "box0"
|
||||
let box0 ← callLeanBox builder (← constIntUnsigned 0) "box0"
|
||||
emitLhsSlotStore builder z box0
|
||||
return ShouldForwardControlFlow.yes
|
||||
)
|
||||
@@ -950,7 +912,7 @@ def emitReuse (builder : LLVM.Builder llvmctx)
|
||||
emitLhsSlotStore builder z xv
|
||||
if updtHeader then
|
||||
let zv ← emitLhsVal builder z
|
||||
callLeanCtorSetTag builder zv (← constInt8 c.cidx)
|
||||
callLeanCtorSetTag builder zv (← constIntUnsigned c.cidx)
|
||||
return ShouldForwardControlFlow.yes
|
||||
)
|
||||
emitCtorSetArgs builder z ys
|
||||
@@ -973,7 +935,7 @@ def emitVDecl (builder : LLVM.Builder llvmctx) (z : VarId) (t : IRType) (v : Exp
|
||||
|
||||
def declareVar (builder : LLVM.Builder llvmctx) (x : VarId) (t : IRType) : M llvmctx Unit := do
|
||||
let llvmty ← toLLVMType t
|
||||
let alloca ← buildPrologueAlloca builder llvmty "varx"
|
||||
let alloca ← LLVM.buildAlloca builder llvmty "varx"
|
||||
addVartoState x alloca llvmty
|
||||
|
||||
partial def declareVars (builder : LLVM.Builder llvmctx) (f : FnBody) : M llvmctx Unit := do
|
||||
@@ -999,7 +961,7 @@ def emitTag (builder : LLVM.Builder llvmctx) (x : VarId) (xType : IRType) : M ll
|
||||
def emitSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : Arg) : M llvmctx Unit := do
|
||||
let fnName := "lean_ctor_set"
|
||||
let retty ← LLVM.voidType llvmctx
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx , ← LLVM.voidPtrType llvmctx]
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.voidPtrType llvmctx]
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
let _ ← LLVM.buildCall2 builder fnty fn #[← emitLhsVal builder x, ← constIntUnsigned i, (← emitArgVal builder y).2]
|
||||
@@ -1007,7 +969,7 @@ def emitSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : Arg) : M
|
||||
def emitUSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : VarId) : M llvmctx Unit := do
|
||||
let fnName := "lean_ctor_set_usize"
|
||||
let retty ← LLVM.voidType llvmctx
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.size_tType llvmctx]
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.size_tType llvmctx]
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
let _ ← LLVM.buildCall2 builder fnty fn #[← emitLhsVal builder x, ← constIntUnsigned i, (← emitLhsVal builder y)]
|
||||
@@ -1046,7 +1008,7 @@ def emitSSet (builder : LLVM.Builder llvmctx) (x : VarId) (n : Nat) (offset : Na
|
||||
| IRType.uint32 => pure ("lean_ctor_set_uint32", ← LLVM.i32Type llvmctx)
|
||||
| IRType.uint64 => pure ("lean_ctor_set_uint64", ← LLVM.i64Type llvmctx)
|
||||
| _ => throw s!"invalid type for 'lean_ctor_set': '{t}'"
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, setty]
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, setty]
|
||||
let retty ← LLVM.voidType llvmctx
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
|
||||
let xv ← emitLhsVal builder x
|
||||
@@ -1064,12 +1026,12 @@ def emitDel (builder : LLVM.Builder llvmctx) (x : VarId) : M llvmctx Unit := do
|
||||
let _ ← LLVM.buildCall2 builder fnty fn #[xv]
|
||||
|
||||
def emitSetTag (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) : M llvmctx Unit := do
|
||||
let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.i8Type llvmctx]
|
||||
let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
|
||||
let retty ← LLVM.voidType llvmctx
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty "lean_ctor_set_tag" argtys
|
||||
let xv ← emitLhsVal builder x
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
let _ ← LLVM.buildCall2 builder fnty fn #[xv, ← constInt8 i]
|
||||
let _ ← LLVM.buildCall2 builder fnty fn #[xv, ← constIntUnsigned i]
|
||||
|
||||
def ensureHasDefault' (alts : Array Alt) : Array Alt :=
|
||||
if alts.any Alt.isDefault then alts
|
||||
@@ -1095,7 +1057,7 @@ partial def emitCase (builder : LLVM.Builder llvmctx)
|
||||
match alt with
|
||||
| Alt.ctor c b =>
|
||||
let destbb ← builderAppendBasicBlock builder s!"case_{xType}_{c.name}_{c.cidx}"
|
||||
LLVM.addCase switch (← constIntSizeT c.cidx) destbb
|
||||
LLVM.addCase switch (← constIntUnsigned c.cidx) destbb
|
||||
LLVM.positionBuilderAtEnd builder destbb
|
||||
emitFnBody builder b
|
||||
| Alt.default b =>
|
||||
@@ -1179,14 +1141,14 @@ def emitFnArgs (builder : LLVM.Builder llvmctx)
|
||||
-- pv := *(argsi) = *(args + i)
|
||||
let pv ← LLVM.buildLoad2 builder llvmty argsi
|
||||
-- slot for arg[i] which is always void* ?
|
||||
let alloca ← buildPrologueAlloca builder llvmty s!"arg_{i}"
|
||||
let alloca ← LLVM.buildAlloca builder llvmty s!"arg_{i}"
|
||||
LLVM.buildStore builder pv alloca
|
||||
addVartoState params[i]!.x alloca llvmty
|
||||
else
|
||||
let n ← LLVM.countParams llvmfn
|
||||
for i in (List.range n.toNat) do
|
||||
let llvmty ← toLLVMType params[i]!.ty
|
||||
let alloca ← buildPrologueAlloca builder llvmty s!"arg_{i}"
|
||||
let alloca ← LLVM.buildAlloca builder llvmty s!"arg_{i}"
|
||||
let arg ← LLVM.getParam llvmfn (UInt64.ofNat i)
|
||||
let _ ← LLVM.buildStore builder arg alloca
|
||||
addVartoState params[i]!.x alloca llvmty
|
||||
@@ -1338,7 +1300,7 @@ def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
|
||||
let ginit?v ← LLVM.buildLoad2 builder ginit?ty ginit?slot "init_v"
|
||||
buildIfThen_ builder "isGInitialized" ginit?v
|
||||
(fun builder => do
|
||||
let box0 ← callLeanBox builder (← constIntSizeT 0) "box0"
|
||||
let box0 ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "box0"
|
||||
let out ← callLeanIOResultMKOk builder box0 "retval"
|
||||
let _ ← LLVM.buildRet builder out
|
||||
pure ShouldForwardControlFlow.no)
|
||||
@@ -1356,7 +1318,7 @@ def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
|
||||
callLeanDecRef builder res
|
||||
let decls := getDecls env
|
||||
decls.reverse.forM (emitDeclInit builder initFn)
|
||||
let box0 ← callLeanBox builder (← constIntSizeT 0) "box0"
|
||||
let box0 ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "box0"
|
||||
let out ← callLeanIOResultMKOk builder box0 "retval"
|
||||
let _ ← LLVM.buildRet builder out
|
||||
|
||||
@@ -1470,15 +1432,15 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
|
||||
#endif
|
||||
-/
|
||||
let inty ← LLVM.voidPtrType llvmctx
|
||||
let inslot ← buildPrologueAlloca builder (← LLVM.pointerType inty) "in"
|
||||
let inslot ← LLVM.buildAlloca builder (← LLVM.pointerType inty) "in"
|
||||
let resty ← LLVM.voidPtrType llvmctx
|
||||
let res ← buildPrologueAlloca builder (← LLVM.pointerType resty) "res"
|
||||
let res ← LLVM.buildAlloca builder (← LLVM.pointerType resty) "res"
|
||||
if usesLeanAPI then callLeanInitialize builder else callLeanInitializeRuntimeModule builder
|
||||
/- We disable panic messages because they do not mesh well with extracted closed terms.
|
||||
See issue #534. We can remove this workaround after we implement issue #467. -/
|
||||
callLeanSetPanicMessages builder (← LLVM.constFalse llvmctx)
|
||||
let world ← callLeanIOMkWorld builder
|
||||
let resv ← callModInitFn builder (← getModName) (← constInt8 1) world ((← getModName).toString ++ "_init_out")
|
||||
let resv ← callModInitFn builder (← getModName) (← LLVM.constInt8 llvmctx 1) world ((← getModName).toString ++ "_init_out")
|
||||
let _ ← LLVM.buildStore builder resv res
|
||||
|
||||
callLeanSetPanicMessages builder (← LLVM.constTrue llvmctx)
|
||||
@@ -1491,21 +1453,21 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
|
||||
callLeanDecRef builder resv
|
||||
callLeanInitTaskManager builder
|
||||
if xs.size == 2 then
|
||||
let inv ← callLeanBox builder (← constIntSizeT 0) "inv"
|
||||
let inv ← callLeanBox builder (← LLVM.constInt (← LLVM.size_tType llvmctx) 0) "inv"
|
||||
let _ ← LLVM.buildStore builder inv inslot
|
||||
let ity ← LLVM.size_tType llvmctx
|
||||
let islot ← buildPrologueAlloca builder ity "islot"
|
||||
let islot ← LLVM.buildAlloca builder ity "islot"
|
||||
let argcval ← LLVM.getParam main 0
|
||||
let argvval ← LLVM.getParam main 1
|
||||
LLVM.buildStore builder argcval islot
|
||||
buildWhile_ builder "argv"
|
||||
(condcodegen := fun builder => do
|
||||
let iv ← LLVM.buildLoad2 builder ity islot "iv"
|
||||
let i_gt_1 ← LLVM.buildICmp builder LLVM.IntPredicate.UGT iv (← constIntSizeT 1) "i_gt_1"
|
||||
let i_gt_1 ← LLVM.buildICmp builder LLVM.IntPredicate.UGT iv (← constIntUnsigned 1) "i_gt_1"
|
||||
return i_gt_1)
|
||||
(bodycodegen := fun builder => do
|
||||
let iv ← LLVM.buildLoad2 builder ity islot "iv"
|
||||
let iv_next ← LLVM.buildSub builder iv (← constIntSizeT 1) "iv.next"
|
||||
let iv_next ← LLVM.buildSub builder iv (← constIntUnsigned 1) "iv.next"
|
||||
LLVM.buildStore builder iv_next islot
|
||||
let nv ← callLeanAllocCtor builder 1 2 0 "nv"
|
||||
let argv_i_next_slot ← LLVM.buildGEP2 builder (← LLVM.voidPtrType llvmctx) argvval #[iv_next] "argv.i.next.slot"
|
||||
@@ -1547,7 +1509,7 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
|
||||
pure ShouldForwardControlFlow.no
|
||||
else do
|
||||
callLeanDecRef builder resv
|
||||
let _ ← LLVM.buildRet builder (← constInt64 0)
|
||||
let _ ← LLVM.buildRet builder (← LLVM.constInt64 llvmctx 0)
|
||||
pure ShouldForwardControlFlow.no
|
||||
|
||||
)
|
||||
@@ -1555,7 +1517,7 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
|
||||
let resv ← LLVM.buildLoad2 builder resty res "resv"
|
||||
callLeanIOResultShowError builder resv
|
||||
callLeanDecRef builder resv
|
||||
let _ ← LLVM.buildRet builder (← constInt64 1)
|
||||
let _ ← LLVM.buildRet builder (← LLVM.constInt64 llvmctx 1)
|
||||
pure ShouldForwardControlFlow.no)
|
||||
-- at the merge
|
||||
let _ ← LLVM.buildUnreachable builder
|
||||
@@ -1630,8 +1592,6 @@ def emitLLVM (env : Environment) (modName : Name) (filepath : String) : IO Unit
|
||||
let some fn ← LLVM.getNamedFunction emitLLVMCtx.llvmmodule name
|
||||
| throw <| IO.Error.userError s!"ERROR: linked module must have function from runtime module: '{name}'"
|
||||
LLVM.setLinkage fn LLVM.Linkage.internal
|
||||
if let some err ← LLVM.verifyModule emitLLVMCtx.llvmmodule then
|
||||
throw <| .userError err
|
||||
LLVM.writeBitcodeToFile emitLLVMCtx.llvmmodule filepath
|
||||
LLVM.disposeModule emitLLVMCtx.llvmmodule
|
||||
| .error err => throw (IO.Error.userError err)
|
||||
|
||||
@@ -182,18 +182,6 @@ opaque createBuilderInContext (ctx : Context) : BaseIO (Builder ctx)
|
||||
@[extern "lean_llvm_append_basic_block_in_context"]
|
||||
opaque appendBasicBlockInContext (ctx : Context) (fn : Value ctx) (name : @&String) : BaseIO (BasicBlock ctx)
|
||||
|
||||
@[extern "lean_llvm_count_basic_blocks"]
|
||||
opaque countBasicBlocks (fn : Value ctx) : BaseIO UInt64
|
||||
|
||||
@[extern "lean_llvm_get_entry_basic_block"]
|
||||
opaque getEntryBasicBlock (fn : Value ctx) : BaseIO (BasicBlock ctx)
|
||||
|
||||
@[extern "lean_llvm_get_first_instruction"]
|
||||
opaque getFirstInstruction (bb : BasicBlock ctx) : BaseIO (Option (Value ctx))
|
||||
|
||||
@[extern "lean_llvm_position_builder_before"]
|
||||
opaque positionBuilderBefore (builder : Builder ctx) (instr : Value ctx) : BaseIO Unit
|
||||
|
||||
@[extern "lean_llvm_position_builder_at_end"]
|
||||
opaque positionBuilderAtEnd (builder : Builder ctx) (bb : BasicBlock ctx) : BaseIO Unit
|
||||
|
||||
@@ -338,9 +326,6 @@ opaque disposeTargetMachine (tm : TargetMachine ctx) : BaseIO Unit
|
||||
@[extern "lean_llvm_dispose_module"]
|
||||
opaque disposeModule (m : Module ctx) : BaseIO Unit
|
||||
|
||||
@[extern "lean_llvm_verify_module"]
|
||||
opaque verifyModule (m : Module ctx) : BaseIO (Option String)
|
||||
|
||||
@[extern "lean_llvm_create_string_attribute"]
|
||||
opaque createStringAttribute (key : String) (value : String) : BaseIO (Attribute ctx)
|
||||
|
||||
@@ -454,11 +439,6 @@ def constInt32 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : B
|
||||
def constInt64 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) :=
|
||||
constInt' ctx 64 value signExtend
|
||||
|
||||
def constIntSizeT (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) :=
|
||||
-- TODO: make this stick to the actual size_t of the target machine
|
||||
constInt' ctx 64 value signExtend
|
||||
|
||||
def constIntUnsigned (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) :=
|
||||
-- TODO: make this stick to the actual unsigned of the target machine
|
||||
constInt' ctx 32 value signExtend
|
||||
constInt' ctx 64 value signExtend
|
||||
end LLVM
|
||||
|
||||
@@ -656,40 +656,35 @@ unsafe def elabEvalUnsafe : CommandElab
|
||||
return e
|
||||
-- Evaluate using term using `MetaEval` class.
|
||||
let elabMetaEval : CommandElabM Unit := do
|
||||
-- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
|
||||
-- we don't polute the environment with auxliary declarations.
|
||||
-- We have special support for `CommandElabM` to ensure `#eval` can be used to execute commands
|
||||
-- that modify `CommandElabM` state not just the `Environment`.
|
||||
let act : Sum (CommandElabM Unit) (Environment → Options → IO (String × Except IO.Error Environment)) ←
|
||||
runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do
|
||||
let e ← elabEvalTerm
|
||||
let eType ← instantiateMVars (← inferType e)
|
||||
if eType.isAppOfArity ``CommandElabM 1 then
|
||||
let mut stx ← Term.exprToSyntax e
|
||||
unless (← isDefEq eType.appArg! (mkConst ``Unit)) do
|
||||
stx ← `($stx >>= fun v => IO.println (repr v))
|
||||
let act ← Lean.Elab.Term.evalTerm (CommandElabM Unit) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) stx
|
||||
pure <| Sum.inl act
|
||||
else
|
||||
let e ← mkRunMetaEval e
|
||||
addAndCompile e
|
||||
let act ← evalConst (Environment → Options → IO (String × Except IO.Error Environment)) declName
|
||||
pure <| Sum.inr act
|
||||
match act with
|
||||
| .inl act => act
|
||||
| .inr act =>
|
||||
let (out, res) ← act (← getEnv) (← getOptions)
|
||||
logInfoAt tk out
|
||||
match res with
|
||||
| Except.error e => throwError e.toString
|
||||
| Except.ok env => setEnv env; pure ()
|
||||
-- act? is `some act` if elaborated `term` has type `CommandElabM α`
|
||||
let act? ← runTermElabM fun _ => Term.withDeclName declName do
|
||||
let e ← elabEvalTerm
|
||||
let eType ← instantiateMVars (← inferType e)
|
||||
if eType.isAppOfArity ``CommandElabM 1 then
|
||||
let mut stx ← Term.exprToSyntax e
|
||||
unless (← isDefEq eType.appArg! (mkConst ``Unit)) do
|
||||
stx ← `($stx >>= fun v => IO.println (repr v))
|
||||
let act ← Lean.Elab.Term.evalTerm (CommandElabM Unit) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) stx
|
||||
pure <| some act
|
||||
else
|
||||
let e ← mkRunMetaEval e
|
||||
let env ← getEnv
|
||||
let opts ← getOptions
|
||||
let act ← try addAndCompile e; evalConst (Environment → Options → IO (String × Except IO.Error Environment)) declName finally setEnv env
|
||||
let (out, res) ← act env opts -- we execute `act` using the environment
|
||||
logInfoAt tk out
|
||||
match res with
|
||||
| Except.error e => throwError e.toString
|
||||
| Except.ok env => do setEnv env; pure none
|
||||
let some act := act? | return ()
|
||||
act
|
||||
-- Evaluate using term using `Eval` class.
|
||||
let elabEval : CommandElabM Unit := runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do
|
||||
let elabEval : CommandElabM Unit := runTermElabM fun _ => Term.withDeclName declName do
|
||||
-- fall back to non-meta eval if MetaEval hasn't been defined yet
|
||||
-- modify e to `runEval e`
|
||||
let e ← mkRunEval (← elabEvalTerm)
|
||||
addAndCompile e
|
||||
let act ← evalConst (IO (String × Except IO.Error Unit)) declName
|
||||
let env ← getEnv
|
||||
let act ← try addAndCompile e; evalConst (IO (String × Except IO.Error Unit)) declName finally setEnv env
|
||||
let (out, res) ← liftM (m := IO) act
|
||||
logInfoAt tk out
|
||||
match res with
|
||||
@@ -727,8 +722,6 @@ opaque elabEval : CommandElab
|
||||
match stx with
|
||||
| `($doc:docComment add_decl_doc $id) =>
|
||||
let declName ← resolveGlobalConstNoOverloadWithInfo id
|
||||
unless ((← getEnv).getModuleIdxFor? declName).isNone do
|
||||
throwError "invalid 'add_decl_doc', declaration is in an imported module"
|
||||
if let .none ← findDeclarationRangesCore? declName then
|
||||
-- this is only relevant for declarations added without a declaration range
|
||||
-- in particular `Quot.mk` et al which are added by `init_quot`
|
||||
|
||||
@@ -524,14 +524,14 @@ private def updateResultingUniverse (views : Array InductiveView) (numParams : N
|
||||
register_builtin_option bootstrap.inductiveCheckResultingUniverse : Bool := {
|
||||
defValue := true,
|
||||
group := "bootstrap",
|
||||
descr := "by default the `inductive`/`structure` commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into `Prop`. In the `Init` package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator"
|
||||
descr := "by default the `inductive/structure commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into `Prop`. In the `Init` package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator"
|
||||
}
|
||||
|
||||
def checkResultingUniverse (u : Level) : TermElabM Unit := do
|
||||
if bootstrap.inductiveCheckResultingUniverse.get (← getOptions) then
|
||||
let u ← instantiateLevelMVars u
|
||||
if !u.isZero && !u.isNeverZero then
|
||||
throwError "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'){indentD u}"
|
||||
throwError "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'{indentD u}"
|
||||
|
||||
private def checkResultingUniverses (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
|
||||
let u := (← instantiateLevelMVars (← getResultingUniverse indTypes)).normalize
|
||||
|
||||
@@ -25,5 +25,3 @@ import Lean.Elab.Tactic.Calc
|
||||
import Lean.Elab.Tactic.Congr
|
||||
import Lean.Elab.Tactic.Guard
|
||||
import Lean.Elab.Tactic.RCases
|
||||
import Lean.Elab.Tactic.Repeat
|
||||
import Lean.Elab.Tactic.Change
|
||||
|
||||
@@ -3,7 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
import Lean.Meta.Tactic.Apply
|
||||
import Lean.Meta.Tactic.Assumption
|
||||
import Lean.Meta.Tactic.Contradiction
|
||||
import Lean.Meta.Tactic.Refl
|
||||
@@ -12,7 +11,6 @@ import Lean.Elab.Open
|
||||
import Lean.Elab.SetOption
|
||||
import Lean.Elab.Tactic.Basic
|
||||
import Lean.Elab.Tactic.ElabTerm
|
||||
import Lean.Elab.Do
|
||||
|
||||
namespace Lean.Elab.Tactic
|
||||
open Meta
|
||||
@@ -325,12 +323,6 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
|
||||
@[builtin_tactic Lean.Parser.Tactic.substVars] def evalSubstVars : Tactic := fun _ =>
|
||||
liftMetaTactic fun mvarId => return [← substVars mvarId]
|
||||
|
||||
/--
|
||||
`subst_eq` repeatedly substitutes according to the equality proof hypotheses in the context,
|
||||
replacing the left side of the equality with the right, until no more progress can be made.
|
||||
-/
|
||||
elab "subst_eqs" : tactic => Elab.Tactic.liftMetaTactic1 (·.substEqs)
|
||||
|
||||
/--
|
||||
Searches for a metavariable `g` s.t. `tag` is its exact name.
|
||||
If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name.
|
||||
@@ -476,24 +468,4 @@ where
|
||||
| none => throwIllFormedSyntax
|
||||
| some ms => IO.sleep ms.toUInt32
|
||||
|
||||
@[builtin_tactic left] def evalLeft : Tactic := fun _stx => do
|
||||
liftMetaTactic (fun g => g.nthConstructor `left 0 (some 2))
|
||||
|
||||
@[builtin_tactic right] def evalRight : Tactic := fun _stx => do
|
||||
liftMetaTactic (fun g => g.nthConstructor `right 1 (some 2))
|
||||
|
||||
@[builtin_tactic replace] def evalReplace : Tactic := fun stx => do
|
||||
match stx with
|
||||
| `(tactic| replace $decl:haveDecl) =>
|
||||
withMainContext do
|
||||
let vars ← Elab.Term.Do.getDoHaveVars <| mkNullNode #[.missing, decl]
|
||||
let origLCtx ← getLCtx
|
||||
evalTactic $ ← `(tactic| have $decl:haveDecl)
|
||||
let mut toClear := #[]
|
||||
for fv in vars do
|
||||
if let some ldecl := origLCtx.findFromUserName? fv.getId then
|
||||
toClear := toClear.push ldecl.fvarId
|
||||
liftMetaTactic1 (·.tryClearMany toClear)
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
end Lean.Elab.Tactic
|
||||
|
||||
@@ -1,51 +0,0 @@
|
||||
/-
|
||||
Copyright (c) 2023 Kyle Miller. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Kyle Miller
|
||||
-/
|
||||
import Lean.Meta.Tactic.Replace
|
||||
import Lean.Elab.Tactic.Location
|
||||
|
||||
namespace Lean.Elab.Tactic
|
||||
open Meta
|
||||
/-!
|
||||
# Implementation of the `change` tactic
|
||||
-/
|
||||
|
||||
/-- `change` can be used to replace the main goal or its hypotheses with
|
||||
different, yet definitionally equal, goal or hypotheses.
|
||||
|
||||
For example, if `n : Nat` and the current goal is `⊢ n + 2 = 2`, then
|
||||
```lean
|
||||
change _ + 1 = _
|
||||
```
|
||||
changes the goal to `⊢ n + 1 + 1 = 2`.
|
||||
|
||||
The tactic also applies to hypotheses. If `h : n + 2 = 2` and `h' : n + 3 = 4`
|
||||
are hypotheses, then
|
||||
```lean
|
||||
change _ + 1 = _ at h h'
|
||||
```
|
||||
changes their types to be `h : n + 1 + 1 = 2` and `h' : n + 2 + 1 = 4`.
|
||||
|
||||
Change is like `refine` in that every placeholder needs to be solved for by unification,
|
||||
but using named placeholders or `?_` results in `change` to creating new goals.
|
||||
|
||||
The tactic `show e` is interchangeable with `change e`, where the pattern `e` is applied to
|
||||
the main goal. -/
|
||||
@[builtin_tactic change] elab_rules : tactic
|
||||
| `(tactic| change $newType:term $[$loc:location]?) => do
|
||||
withLocation (expandOptLocation (Lean.mkOptionalNode loc))
|
||||
(atLocal := fun h => do
|
||||
let hTy ← h.getType
|
||||
-- This is a hack to get the new type to elaborate in the same sort of way that
|
||||
-- it would for a `show` expression for the goal.
|
||||
let mvar ← mkFreshExprMVar none
|
||||
let (_, mvars) ← elabTermWithHoles
|
||||
(← `(term | show $newType from $(← Term.exprToSyntax mvar))) hTy `change
|
||||
liftMetaTactic fun mvarId => do
|
||||
return (← mvarId.changeLocalDecl h (← inferType mvar)) :: mvars)
|
||||
(atTarget := evalTactic <| ← `(tactic| refine_lift show $newType from ?_))
|
||||
(failed := fun _ => throwError "change tactic failed")
|
||||
|
||||
end Lean.Elab.Tactic
|
||||
@@ -1,25 +0,0 @@
|
||||
/-
|
||||
Copyright (c) 2022 Mario Carneiro. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mario Carneiro, Scott Morrison
|
||||
-/
|
||||
import Lean.Meta.Tactic.Repeat
|
||||
import Lean.Elab.Tactic.Basic
|
||||
|
||||
namespace Lean.Elab.Tactic
|
||||
|
||||
@[builtin_tactic repeat']
|
||||
def evalRepeat' : Tactic := fun stx => do
|
||||
match stx with
|
||||
| `(tactic| repeat' $tac:tacticSeq) =>
|
||||
setGoals (← Meta.repeat' (evalTacticAtRaw tac) (← getGoals))
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[builtin_tactic repeat1']
|
||||
def evalRepeat1' : Tactic := fun stx => do
|
||||
match stx with
|
||||
| `(tactic| repeat1' $tac:tacticSeq) =>
|
||||
setGoals (← Meta.repeat1' (evalTacticAtRaw tac) (← getGoals))
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
end Lean.Elab.Tactic
|
||||
@@ -1,7 +1,7 @@
|
||||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura, Jannis Limperg, Scott Morrison
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
import Lean.Meta.WHNF
|
||||
import Lean.Meta.Transform
|
||||
@@ -450,18 +450,6 @@ def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreCon
|
||||
let keys ← mkPath e config
|
||||
return d.insertCore keys v
|
||||
|
||||
/--
|
||||
Inserts a value into a discrimination tree,
|
||||
but only if its key is not of the form `#[*]` or `#[=, *, *, *]`.
|
||||
-/
|
||||
def insertIfSpecific [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) : MetaM (DiscrTree α) := do
|
||||
let keys ← mkPath e config
|
||||
return if keys == #[Key.star] || keys == #[Key.const `Eq 3, Key.star, Key.star, Key.star] then
|
||||
d
|
||||
else
|
||||
d.insertCore keys v
|
||||
|
||||
|
||||
private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) := do
|
||||
let e ← reduceDT e root config
|
||||
unless root do
|
||||
@@ -688,124 +676,4 @@ where
|
||||
| .arrow => visitNonStar .other #[] (← visitNonStar k args (← visitStar result))
|
||||
| _ => visitNonStar k args (← visitStar result)
|
||||
|
||||
namespace Trie
|
||||
|
||||
-- `Inhabited` instance to allow `partial` definitions below.
|
||||
private local instance [Monad m] : Inhabited (σ → β → m σ) := ⟨fun s _ => pure s⟩
|
||||
|
||||
/--
|
||||
Monadically fold the keys and values stored in a `Trie`.
|
||||
-/
|
||||
partial def foldM [Monad m] (initialKeys : Array Key)
|
||||
(f : σ → Array Key → α → m σ) : (init : σ) → Trie α → m σ
|
||||
| init, Trie.node vs children => do
|
||||
let s ← vs.foldlM (init := init) fun s v => f s initialKeys v
|
||||
children.foldlM (init := s) fun s (k, t) =>
|
||||
t.foldM (initialKeys.push k) f s
|
||||
|
||||
/--
|
||||
Fold the keys and values stored in a `Trie`.
|
||||
-/
|
||||
@[inline]
|
||||
def fold (initialKeys : Array Key) (f : σ → Array Key → α → σ) (init : σ) (t : Trie α) : σ :=
|
||||
Id.run <| t.foldM initialKeys (init := init) fun s k a => return f s k a
|
||||
|
||||
/--
|
||||
Monadically fold the values stored in a `Trie`.
|
||||
-/
|
||||
partial def foldValuesM [Monad m] (f : σ → α → m σ) : (init : σ) → Trie α → m σ
|
||||
| init, node vs children => do
|
||||
let s ← vs.foldlM (init := init) f
|
||||
children.foldlM (init := s) fun s (_, c) => c.foldValuesM (init := s) f
|
||||
|
||||
/--
|
||||
Fold the values stored in a `Trie`.
|
||||
-/
|
||||
@[inline]
|
||||
def foldValues (f : σ → α → σ) (init : σ) (t : Trie α) : σ :=
|
||||
Id.run <| t.foldValuesM (init := init) f
|
||||
|
||||
/--
|
||||
The number of values stored in a `Trie`.
|
||||
-/
|
||||
partial def size : Trie α → Nat
|
||||
| Trie.node vs children =>
|
||||
children.foldl (init := vs.size) fun n (_, c) => n + size c
|
||||
|
||||
end Trie
|
||||
|
||||
|
||||
/--
|
||||
Monadically fold over the keys and values stored in a `DiscrTree`.
|
||||
-/
|
||||
@[inline]
|
||||
def foldM [Monad m] (f : σ → Array Key → α → m σ) (init : σ)
|
||||
(t : DiscrTree α) : m σ :=
|
||||
t.root.foldlM (init := init) fun s k t => t.foldM #[k] (init := s) f
|
||||
|
||||
/--
|
||||
Fold over the keys and values stored in a `DiscrTree`
|
||||
-/
|
||||
@[inline]
|
||||
def fold (f : σ → Array Key → α → σ) (init : σ) (t : DiscrTree α) : σ :=
|
||||
Id.run <| t.foldM (init := init) fun s keys a => return f s keys a
|
||||
|
||||
/--
|
||||
Monadically fold over the values stored in a `DiscrTree`.
|
||||
-/
|
||||
@[inline]
|
||||
def foldValuesM [Monad m] (f : σ → α → m σ) (init : σ) (t : DiscrTree α) :
|
||||
m σ :=
|
||||
t.root.foldlM (init := init) fun s _ t => t.foldValuesM (init := s) f
|
||||
|
||||
/--
|
||||
Fold over the values stored in a `DiscrTree`.
|
||||
-/
|
||||
@[inline]
|
||||
def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ :=
|
||||
Id.run <| t.foldValuesM (init := init) f
|
||||
|
||||
/--
|
||||
Check for the presence of a value satisfying a predicate.
|
||||
-/
|
||||
@[inline]
|
||||
def containsValueP [BEq α] (t : DiscrTree α) (f : α → Bool) : Bool :=
|
||||
t.foldValues (init := false) fun r a => r || f a
|
||||
|
||||
/--
|
||||
Extract the values stored in a `DiscrTree`.
|
||||
-/
|
||||
@[inline]
|
||||
def values (t : DiscrTree α) : Array α :=
|
||||
t.foldValues (init := #[]) fun as a => as.push a
|
||||
|
||||
/--
|
||||
Extract the keys and values stored in a `DiscrTree`.
|
||||
-/
|
||||
@[inline]
|
||||
def toArray (t : DiscrTree α) : Array (Array Key × α) :=
|
||||
t.fold (init := #[]) fun as keys a => as.push (keys, a)
|
||||
|
||||
/--
|
||||
Get the number of values stored in a `DiscrTree`. O(n) in the size of the tree.
|
||||
-/
|
||||
@[inline]
|
||||
def size (t : DiscrTree α) : Nat :=
|
||||
t.root.foldl (init := 0) fun n _ t => n + t.size
|
||||
|
||||
variable {m : Type → Type} [Monad m]
|
||||
|
||||
/-- Apply a monadic function to the array of values at each node in a `DiscrTree`. -/
|
||||
partial def Trie.mapArraysM (t : DiscrTree.Trie α) (f : Array α → m (Array β)) :
|
||||
m (DiscrTree.Trie β) :=
|
||||
match t with
|
||||
| .node vs children =>
|
||||
return .node (← f vs) (← children.mapM fun (k, t') => do pure (k, ← t'.mapArraysM f))
|
||||
|
||||
/-- Apply a monadic function to the array of values at each node in a `DiscrTree`. -/
|
||||
def mapArraysM (d : DiscrTree α) (f : Array α → m (Array β)) : m (DiscrTree β) := do
|
||||
pure { root := ← d.root.mapM (fun t => t.mapArraysM f) }
|
||||
|
||||
/-- Apply a function to the array of values at each node in a `DiscrTree`. -/
|
||||
def mapArrays (d : DiscrTree α) (f : Array α → Array β) : DiscrTree β :=
|
||||
Id.run <| d.mapArraysM fun A => pure (f A)
|
||||
end Lean.Meta.DiscrTree
|
||||
|
||||
@@ -22,12 +22,10 @@ import Lean.Meta.Tactic.Simp
|
||||
import Lean.Meta.Tactic.AuxLemma
|
||||
import Lean.Meta.Tactic.SplitIf
|
||||
import Lean.Meta.Tactic.Split
|
||||
import Lean.Meta.Tactic.TryThis
|
||||
import Lean.Meta.Tactic.Cleanup
|
||||
import Lean.Meta.Tactic.Unfold
|
||||
import Lean.Meta.Tactic.Rename
|
||||
import Lean.Meta.Tactic.LinearArith
|
||||
import Lean.Meta.Tactic.AC
|
||||
import Lean.Meta.Tactic.Refl
|
||||
import Lean.Meta.Tactic.Congr
|
||||
import Lean.Meta.Tactic.Repeat
|
||||
import Lean.Meta.Tactic.Congr
|
||||
@@ -1,7 +1,7 @@
|
||||
/-
|
||||
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura, Siddhartha Gadgil
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
import Lean.Util.FindMVar
|
||||
import Lean.Meta.SynthInstance
|
||||
@@ -230,25 +230,4 @@ def _root_.Lean.MVarId.exfalso (mvarId : MVarId) : MetaM MVarId :=
|
||||
mvarId.assign (mkApp2 (mkConst ``False.elim [u]) target mvarIdNew)
|
||||
return mvarIdNew.mvarId!
|
||||
|
||||
/--
|
||||
Apply the `n`-th constructor of the target type,
|
||||
checking that it is an inductive type,
|
||||
and that there are the expected number of constructors.
|
||||
-/
|
||||
def _root_.Lean.MVarId.nthConstructor
|
||||
(name : Name) (idx : Nat) (expected? : Option Nat := none) (goal : MVarId) :
|
||||
MetaM (List MVarId) := do
|
||||
goal.withContext do
|
||||
goal.checkNotAssigned name
|
||||
matchConstInduct (← goal.getType').getAppFn
|
||||
(fun _ => throwTacticEx name goal "target is not an inductive datatype")
|
||||
fun ival us => do
|
||||
if let some e := expected? then unless ival.ctors.length == e do
|
||||
throwTacticEx name goal
|
||||
s!"{name} tactic works for inductive types with exactly {e} constructors"
|
||||
if h : idx < ival.ctors.length then
|
||||
goal.apply <| mkConst ival.ctors[idx] us
|
||||
else
|
||||
throwTacticEx name goal s!"index {idx} out of bounds, only {ival.ctors.length} constructors"
|
||||
|
||||
end Lean.Meta
|
||||
|
||||
@@ -1,64 +0,0 @@
|
||||
/-
|
||||
Copyright (c) 2022 Mario Carneiro. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mario Carneiro, Scott Morrison
|
||||
-/
|
||||
import Lean.Meta.Basic
|
||||
|
||||
namespace Lean.Meta
|
||||
/--
|
||||
Implementation of `repeat'` and `repeat1'`.
|
||||
|
||||
`repeat'Core f` runs `f` on all of the goals to produce a new list of goals,
|
||||
then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
|
||||
or until `maxIters` total calls to `f` have occurred.
|
||||
|
||||
Returns a boolean indicating whether `f` succeeded at least once, and
|
||||
all the remaining goals (i.e. those on which `f` failed).
|
||||
-/
|
||||
def repeat'Core [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
|
||||
(f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) :
|
||||
m (Bool × List MVarId) := do
|
||||
let (progress, acc) ← go maxIters false goals [] #[]
|
||||
pure (progress, (← acc.filterM fun g => not <$> g.isAssigned).toList)
|
||||
where
|
||||
/-- Auxiliary for `repeat'Core`. `repeat'Core.go f maxIters progress goals stk acc` evaluates to
|
||||
essentially `acc.toList ++ repeat' f (goals::stk).join maxIters`: that is, `acc` are goals we will
|
||||
not revisit, and `(goals::stk).join` is the accumulated todo list of subgoals. -/
|
||||
go : Nat → Bool → List MVarId → List (List MVarId) → Array MVarId → m (Bool × Array MVarId)
|
||||
| _, p, [], [], acc => pure (p, acc)
|
||||
| n, p, [], goals::stk, acc => go n p goals stk acc
|
||||
| n, p, g::goals, stk, acc => do
|
||||
if ← g.isAssigned then
|
||||
go n p goals stk acc
|
||||
else
|
||||
match n with
|
||||
| 0 => pure <| (p, acc.push g ++ goals |> stk.foldl .appendList)
|
||||
| n+1 =>
|
||||
match ← observing? (f g) with
|
||||
| some goals' => go n true goals' (goals::stk) acc
|
||||
| none => go n p goals stk (acc.push g)
|
||||
termination_by n p goals stk _ => (n, stk, goals)
|
||||
|
||||
/--
|
||||
`repeat' f` runs `f` on all of the goals to produce a new list of goals,
|
||||
then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
|
||||
or until `maxIters` total calls to `f` have occurred.
|
||||
Always succeeds (returning the original goals if `f` fails on all of them).
|
||||
-/
|
||||
def repeat' [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
|
||||
(f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) : m (List MVarId) :=
|
||||
repeat'Core f goals maxIters <&> (·.2)
|
||||
|
||||
/--
|
||||
`repeat1' f` runs `f` on all of the goals to produce a new list of goals,
|
||||
then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
|
||||
or until `maxIters` total calls to `f` have occurred.
|
||||
Fails if `f` does not succeed at least once.
|
||||
-/
|
||||
def repeat1' [Monad m] [MonadError m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
|
||||
(f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) : m (List MVarId) := do
|
||||
let (.true, goals) ← repeat'Core f goals maxIters | throwError "repeat1' made no progress"
|
||||
pure goals
|
||||
|
||||
end Lean.Meta
|
||||
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
import Lean.Util.ForEachExpr
|
||||
import Lean.Elab.InfoTree.Main
|
||||
import Lean.Meta.AppBuilder
|
||||
import Lean.Meta.MatchUtil
|
||||
import Lean.Meta.Tactic.Util
|
||||
@@ -140,54 +139,29 @@ def _root_.Lean.MVarId.change (mvarId : MVarId) (targetNew : Expr) (checkDefEq :
|
||||
def change (mvarId : MVarId) (targetNew : Expr) (checkDefEq := true) : MetaM MVarId := mvarId.withContext do
|
||||
mvarId.change targetNew checkDefEq
|
||||
|
||||
/-- Runs the continuation `k` after temporarily reverting some variables from the local context of a metavariable (identified by `mvarId`), then reintroduces local variables as specified by `k`.
|
||||
|
||||
The argument `fvarIds` is an array of `fvarIds` to revert in the order specified. An error is thrown if they cannot be reverted in order.
|
||||
|
||||
Once the local variables have been reverted, `k` is passed `mvarId` along with an array of local variables that were reverted. This array always has `fvarIds` as a prefix, but it may contain additional variables that were reverted due to dependencies. `k` returns a value, a goal, an array of _link variables_.
|
||||
|
||||
Once `k` has completed, one variable is introduced for each link variable returned by `k`. If the returned variable is `none`, the variable is just introduced. If it is `some fv`, the variable is introduced and then linked as an alias of `fv` in the info tree. For example, having `k` return `fvars.map .some` as the link variables causes all reverted variables to be introduced and linked.
|
||||
|
||||
Returns the value returned by `k` along with the resulting goal.
|
||||
-/
|
||||
def _root_.Lean.MVarId.withReverted (mvarId : MVarId) (fvarIds : Array FVarId)
|
||||
(k : MVarId → Array FVarId → MetaM (α × Array (Option FVarId) × MVarId))
|
||||
(clearAuxDeclsInsteadOfRevert := false) : MetaM (α × MVarId) := do
|
||||
let (xs, mvarId) ← mvarId.revert fvarIds true clearAuxDeclsInsteadOfRevert
|
||||
let (r, xs', mvarId) ← k mvarId xs
|
||||
let (ys, mvarId) ← mvarId.introNP xs'.size
|
||||
mvarId.withContext do
|
||||
for x? in xs', y in ys do
|
||||
if let some x := x? then
|
||||
Elab.pushInfoLeaf (.ofFVarAliasInfo { id := y, baseId := x, userName := ← y.getUserName })
|
||||
return (r, mvarId)
|
||||
|
||||
/--
|
||||
Replaces the type of the free variable `fvarId` with `typeNew`.
|
||||
|
||||
If `checkDefEq` is `true` then an error is thrown if `typeNew` is not definitionally
|
||||
equal to the type of `fvarId`. Otherwise this function assumes `typeNew` and the type
|
||||
of `fvarId` are definitionally equal.
|
||||
|
||||
This function is the same as `Lean.MVarId.changeLocalDecl` but makes sure to push substitution
|
||||
information into the info tree.
|
||||
Replace the type of the free variable `fvarId` with `typeNew`.
|
||||
If `checkDefEq = false`, this method assumes that `typeNew` is definitionally equal to `fvarId` type.
|
||||
If `checkDefEq = true`, throw an error if `typeNew` is not definitionally equal to `fvarId` type.
|
||||
-/
|
||||
def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr)
|
||||
(checkDefEq := true) : MetaM MVarId := do
|
||||
def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do
|
||||
mvarId.checkNotAssigned `changeLocalDecl
|
||||
let (_, mvarId) ← mvarId.withReverted #[fvarId] fun mvarId fvars => mvarId.withContext do
|
||||
let (xs, mvarId) ← mvarId.revert #[fvarId] true
|
||||
mvarId.withContext do
|
||||
let numReverted := xs.size
|
||||
let target ← mvarId.getType
|
||||
let check (typeOld : Expr) : MetaM Unit := do
|
||||
if checkDefEq then
|
||||
unless ← isDefEq typeNew typeOld do
|
||||
throwTacticEx `changeLocalDecl mvarId
|
||||
m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
|
||||
let finalize (targetNew : Expr) := do
|
||||
return ((), fvars.map .some, ← mvarId.replaceTargetDefEq targetNew)
|
||||
match ← mvarId.getType with
|
||||
| .forallE n d b bi => do check d; finalize (.forallE n typeNew b bi)
|
||||
| .letE n t v b ndep => do check t; finalize (.letE n typeNew v b ndep)
|
||||
| _ => throwTacticEx `changeLocalDecl mvarId "unexpected auxiliary target"
|
||||
return mvarId
|
||||
unless (← isDefEq typeNew typeOld) do
|
||||
throwTacticEx `changeHypothesis mvarId m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
|
||||
let finalize (targetNew : Expr) : MetaM MVarId := do
|
||||
let mvarId ← mvarId.replaceTargetDefEq targetNew
|
||||
let (_, mvarId) ← mvarId.introNP numReverted
|
||||
pure mvarId
|
||||
match target with
|
||||
| .forallE n d b c => do check d; finalize (mkForall n c typeNew b)
|
||||
| .letE n t v b _ => do check t; finalize (mkLet n typeNew v b)
|
||||
| _ => throwTacticEx `changeHypothesis mvarId "unexpected auxiliary target"
|
||||
|
||||
@[deprecated MVarId.changeLocalDecl]
|
||||
def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do
|
||||
|
||||
@@ -12,13 +12,9 @@ import Lean.Meta.Tactic.Simp.SimpCongrTheorems
|
||||
namespace Lean.Meta
|
||||
namespace Simp
|
||||
|
||||
/-- The result of simplifying some expression `e`. -/
|
||||
structure Result where
|
||||
/-- The simplified version of `e` -/
|
||||
expr : Expr
|
||||
/-- A proof that `$e = $expr`, where the simplified expression is on the RHS.
|
||||
If `none`, the proof is assumed to be `refl`. -/
|
||||
proof? : Option Expr := none
|
||||
proof? : Option Expr := none -- If none, proof is assumed to be `refl`
|
||||
/-- Save the field `dischargeDepth` at `Simp.Context` because it impacts the simplifier result. -/
|
||||
dischargeDepth : UInt32 := 0
|
||||
/-- If `cache := true` the result is cached. -/
|
||||
|
||||
@@ -1,585 +0,0 @@
|
||||
/-
|
||||
Copyright (c) 2021 Gabriel Ebner. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Gabriel Ebner, Mario Carneiro, Thomas Murrills
|
||||
-/
|
||||
import Lean.Server.CodeActions
|
||||
import Lean.Widget.UserWidget
|
||||
import Lean.Data.Json.Elab
|
||||
|
||||
/-- Gets the LSP range from a `String.Range`. -/
|
||||
def Lean.FileMap.utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
|
||||
{ start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
|
||||
|
||||
|
||||
/-!
|
||||
# "Try this" support
|
||||
|
||||
This implements a mechanism for tactics to print a message saying `Try this: <suggestion>`,
|
||||
where `<suggestion>` is a link to a replacement tactic. Users can either click on the link
|
||||
in the suggestion (provided by a widget), or use a code action which applies the suggestion.
|
||||
-/
|
||||
namespace Lean.Meta.Tactic.TryThis
|
||||
|
||||
open Lean Elab PrettyPrinter Meta Server RequestM
|
||||
|
||||
/-! # Raw widget -/
|
||||
|
||||
/--
|
||||
This is a widget which is placed by `TryThis.addSuggestion` and `TryThis.addSuggestions`.
|
||||
|
||||
When placed by `addSuggestion`, it says `Try this: <replacement>`
|
||||
where `<replacement>` is a link which will perform the replacement.
|
||||
|
||||
When placed by `addSuggestions`, it says:
|
||||
```
|
||||
Try these:
|
||||
```
|
||||
* `<replacement1>`
|
||||
* `<replacement2>`
|
||||
* `<replacement3>`
|
||||
* ...
|
||||
|
||||
where `<replacement*>` is a link which will perform the replacement.
|
||||
-/
|
||||
@[widget_module] def tryThisWidget : Widget.Module where
|
||||
javascript := "
|
||||
import * as React from 'react';
|
||||
import { EditorContext } from '@leanprover/infoview';
|
||||
const e = React.createElement;
|
||||
export default function ({ pos, suggestions, range, header, isInline, style }) {
|
||||
const editorConnection = React.useContext(EditorContext)
|
||||
const defStyle = style || {
|
||||
className: 'link pointer dim',
|
||||
style: { color: 'var(--vscode-textLink-foreground)' }
|
||||
}
|
||||
|
||||
// Construct the children of the HTML element for a given suggestion.
|
||||
function makeSuggestion({ suggestion, preInfo, postInfo, style }) {
|
||||
function onClick() {
|
||||
editorConnection.api.applyEdit({
|
||||
changes: { [pos.uri]: [{ range, newText: suggestion }] }
|
||||
})
|
||||
}
|
||||
return [
|
||||
preInfo,
|
||||
e('span', { onClick, title: 'Apply suggestion', ...style || defStyle }, suggestion),
|
||||
postInfo
|
||||
]
|
||||
}
|
||||
|
||||
// Choose between an inline 'Try this'-like display and a list-based 'Try these'-like display.
|
||||
let inner = null
|
||||
if (isInline) {
|
||||
inner = e('div', { className: 'ml1' },
|
||||
e('pre', { className: 'font-code pre-wrap' }, header, makeSuggestion(suggestions[0])))
|
||||
} else {
|
||||
inner = e('div', { className: 'ml1' },
|
||||
e('pre', { className: 'font-code pre-wrap' }, header),
|
||||
e('ul', { style: { paddingInlineStart: '20px' } }, suggestions.map(s =>
|
||||
e('li', { className: 'font-code pre-wrap' }, makeSuggestion(s)))))
|
||||
}
|
||||
return e('details', { open: true },
|
||||
e('summary', { className: 'mv2 pointer' }, 'Suggestions'),
|
||||
inner)
|
||||
}"
|
||||
|
||||
/-! # Code action -/
|
||||
|
||||
/-- A packet of information about a "Try this" suggestion
|
||||
that we store in the infotree for the associated code action to retrieve. -/
|
||||
structure TryThisInfo : Type where
|
||||
/-- The textual range to be replaced by one of the suggestions. -/
|
||||
range : Lsp.Range
|
||||
/--
|
||||
A list of suggestions for the user to choose from.
|
||||
Each suggestion may optionally come with an override for the code action title.
|
||||
-/
|
||||
suggestionTexts : Array (String × Option String)
|
||||
/-- The prefix to display before the code action for a "Try this" suggestion if no custom code
|
||||
action title is provided. If not provided, `"Try this: "` is used. -/
|
||||
codeActionPrefix? : Option String
|
||||
deriving TypeName
|
||||
|
||||
/--
|
||||
This is a code action provider that looks for `TryThisInfo` nodes and supplies a code action to
|
||||
apply the replacement.
|
||||
-/
|
||||
@[code_action_provider] def tryThisProvider : CodeActionProvider := fun params snap => do
|
||||
let doc ← readDoc
|
||||
pure <| snap.infoTree.foldInfo (init := #[]) fun _ctx info result => Id.run do
|
||||
let .ofCustomInfo { stx, value } := info | result
|
||||
let some { range, suggestionTexts, codeActionPrefix? } :=
|
||||
value.get? TryThisInfo | result
|
||||
let some stxRange := stx.getRange? | result
|
||||
let stxRange := doc.meta.text.utf8RangeToLspRange stxRange
|
||||
unless stxRange.start.line ≤ params.range.end.line do return result
|
||||
unless params.range.start.line ≤ stxRange.end.line do return result
|
||||
let mut result := result
|
||||
for h : i in [:suggestionTexts.size] do
|
||||
let (newText, title?) := suggestionTexts[i]'h.2
|
||||
let title := title?.getD <| (codeActionPrefix?.getD "Try this: ") ++ newText
|
||||
result := result.push {
|
||||
eager.title := title
|
||||
eager.kind? := "quickfix"
|
||||
-- Only make the first option preferred
|
||||
eager.isPreferred? := if i = 0 then true else none
|
||||
eager.edit? := some <| .ofTextEdit doc.versionedIdentifier { range, newText }
|
||||
}
|
||||
result
|
||||
|
||||
/-! # Formatting -/
|
||||
|
||||
/-- Yields `(indent, column)` given a `FileMap` and a `String.Range`, where `indent` is the number
|
||||
of spaces by which the line that first includes `range` is initially indented, and `column` is the
|
||||
column `range` starts at in that line. -/
|
||||
def getIndentAndColumn (map : FileMap) (range : String.Range) : Nat × Nat :=
|
||||
let start := map.source.findLineStart range.start
|
||||
let body := map.source.findAux (· ≠ ' ') range.start start
|
||||
((body - start).1, (range.start - start).1)
|
||||
|
||||
/-- Replace subexpressions like `?m.1234` with `?_` so it can be copy-pasted. -/
|
||||
partial def replaceMVarsByUnderscores [Monad m] [MonadQuotation m]
|
||||
(s : Syntax) : m Syntax :=
|
||||
s.replaceM fun s => do
|
||||
let `(?$id:ident) := s | pure none
|
||||
if id.getId.hasNum || id.getId.isInternal then `(?_) else pure none
|
||||
|
||||
/-- Delaborate `e` into syntax suitable for use by `refine`. -/
|
||||
def delabToRefinableSyntax (e : Expr) : MetaM Term :=
|
||||
return ⟨← replaceMVarsByUnderscores (← delab e)⟩
|
||||
|
||||
/--
|
||||
An option allowing the user to customize the ideal input width. Defaults to 100.
|
||||
This option controls output format when
|
||||
the output is intended to be copied back into a lean file -/
|
||||
register_option format.inputWidth : Nat := {
|
||||
/- The default maximum width of an ideal line in source code. -/
|
||||
defValue := 100
|
||||
descr := "ideal input width"
|
||||
}
|
||||
|
||||
/-- Get the input width specified in the options -/
|
||||
def getInputWidth (o : Options) : Nat := format.inputWidth.get o
|
||||
|
||||
/-! # `Suggestion` data -/
|
||||
|
||||
-- TODO: we could also support `Syntax` and `Format`
|
||||
/-- Text to be used as a suggested replacement in the infoview. This can be either a `TSyntax kind`
|
||||
for a single `kind : SyntaxNodeKind` or a raw `String`.
|
||||
|
||||
Instead of using constructors directly, there are coercions available from these types to
|
||||
`SuggestionText`. -/
|
||||
inductive SuggestionText where
|
||||
/-- `TSyntax kind` used as suggested replacement text in the infoview. Note that while `TSyntax`
|
||||
is in general parameterized by a list of `SyntaxNodeKind`s, we only allow one here; this
|
||||
unambiguously guides pretty-printing. -/
|
||||
| tsyntax {kind : SyntaxNodeKind} : TSyntax kind → SuggestionText
|
||||
/-- A raw string to be used as suggested replacement text in the infoview. -/
|
||||
| string : String → SuggestionText
|
||||
deriving Inhabited
|
||||
|
||||
instance : ToMessageData SuggestionText where
|
||||
toMessageData
|
||||
| .tsyntax stx => stx
|
||||
| .string s => s
|
||||
|
||||
instance {kind : SyntaxNodeKind} : CoeHead (TSyntax kind) SuggestionText where
|
||||
coe := .tsyntax
|
||||
|
||||
instance : Coe String SuggestionText where
|
||||
coe := .string
|
||||
|
||||
namespace SuggestionText
|
||||
|
||||
/-- Pretty-prints a `SuggestionText` as a `Format`. If the `SuggestionText` is some `TSyntax kind`,
|
||||
we use the appropriate pretty-printer; strings are coerced to `Format`s as-is. -/
|
||||
def pretty : SuggestionText → CoreM Format
|
||||
| .tsyntax (kind := kind) stx => ppCategory kind stx
|
||||
| .string text => return text
|
||||
|
||||
/- Note that this is essentially `return (← s.pretty).prettyExtra w indent column`, but we
|
||||
special-case strings to avoid converting them to `Format`s and back, which adds indentation after each newline. -/
|
||||
/-- Pretty-prints a `SuggestionText` as a `String` and wraps with respect to the pane width,
|
||||
indentation, and column, via `Format.prettyExtra`. If `w := none`, then
|
||||
`w := getInputWidth (← getOptions)` is used. Raw `String`s are returned as-is. -/
|
||||
def prettyExtra (s : SuggestionText) (w : Option Nat := none)
|
||||
(indent column : Nat := 0) : CoreM String :=
|
||||
match s with
|
||||
| .tsyntax (kind := kind) stx => do
|
||||
let w ← match w with | none => do pure <| getInputWidth (← getOptions) | some n => pure n
|
||||
return (← ppCategory kind stx).pretty w indent column
|
||||
| .string text => return text
|
||||
|
||||
end SuggestionText
|
||||
|
||||
/--
|
||||
Style hooks for `Suggestion`s. See `SuggestionStyle.error`, `.warning`, `.success`, `.value`,
|
||||
and other definitions here for style presets. This is an arbitrary `Json` object, with the following
|
||||
interesting fields:
|
||||
* `title`: the hover text in the suggestion link
|
||||
* `className`: the CSS classes applied to the link
|
||||
* `style`: A `Json` object with additional inline CSS styles such as `color` or `textDecoration`.
|
||||
-/
|
||||
def SuggestionStyle := Json deriving Inhabited, ToJson
|
||||
|
||||
/-- Style as an error. By default, decorates the text with an undersquiggle; providing the argument
|
||||
`decorated := false` turns this off. -/
|
||||
def SuggestionStyle.error (decorated := true) : SuggestionStyle :=
|
||||
let style := if decorated then
|
||||
json% {
|
||||
-- The VS code error foreground theme color (`--vscode-errorForeground`).
|
||||
color: "var(--vscode-errorForeground)",
|
||||
textDecoration: "underline wavy var(--vscode-editorError-foreground) 1pt"
|
||||
}
|
||||
else json% { color: "var(--vscode-errorForeground)" }
|
||||
json% { className: "pointer dim", style: $style }
|
||||
|
||||
/-- Style as a warning. By default, decorates the text with an undersquiggle; providing the
|
||||
argument `decorated := false` turns this off. -/
|
||||
def SuggestionStyle.warning (decorated := true) : SuggestionStyle :=
|
||||
if decorated then
|
||||
json% {
|
||||
-- The `.gold` CSS class, which the infoview uses when e.g. building a file.
|
||||
className: "gold pointer dim",
|
||||
style: { textDecoration: "underline wavy var(--vscode-editorWarning-foreground) 1pt" }
|
||||
}
|
||||
else json% { className: "gold pointer dim" }
|
||||
|
||||
/-- Style as a success. -/
|
||||
def SuggestionStyle.success : SuggestionStyle :=
|
||||
-- The `.information` CSS class, which the infoview uses on successes.
|
||||
json% { className: "information pointer dim" }
|
||||
|
||||
/-- Style the same way as a hypothesis appearing in the infoview. -/
|
||||
def SuggestionStyle.asHypothesis : SuggestionStyle :=
|
||||
json% { className: "goal-hyp pointer dim" }
|
||||
|
||||
/-- Style the same way as an inaccessible hypothesis appearing in the infoview. -/
|
||||
def SuggestionStyle.asInaccessible : SuggestionStyle :=
|
||||
json% { className: "goal-inaccessible pointer dim" }
|
||||
|
||||
/-- Draws the color from a red-yellow-green color gradient with red at `0.0`, yellow at `0.5`, and
|
||||
green at `1.0`. Values outside the range `[0.0, 1.0]` are clipped to lie within this range.
|
||||
|
||||
With `showValueInHoverText := true` (the default), the value `t` will be included in the `title` of
|
||||
the HTML element (which appears on hover). -/
|
||||
def SuggestionStyle.value (t : Float) (showValueInHoverText := true) : SuggestionStyle :=
|
||||
let t := min (max t 0) 1
|
||||
json% {
|
||||
className: "pointer dim",
|
||||
-- interpolates linearly from 0º to 120º with 95% saturation and lightness
|
||||
-- varying around 50% in HSL space
|
||||
style: { color: $(s!"hsl({(t * 120).round} 95% {60 * ((t - 0.5)^2 + 0.75)}%)") },
|
||||
title: $(if showValueInHoverText then s!"Apply suggestion ({t})" else "Apply suggestion")
|
||||
}
|
||||
|
||||
/-- Holds a `suggestion` for replacement, along with `preInfo` and `postInfo` strings to be printed
|
||||
immediately before and after that suggestion, respectively. It also includes an optional
|
||||
`MessageData` to represent the suggestion in logs; by default, this is `none`, and `suggestion` is
|
||||
used. -/
|
||||
structure Suggestion where
|
||||
/-- Text to be used as a replacement via a code action. -/
|
||||
suggestion : SuggestionText
|
||||
/-- Optional info to be printed immediately before replacement text in a widget. -/
|
||||
preInfo? : Option String := none
|
||||
/-- Optional info to be printed immediately after replacement text in a widget. -/
|
||||
postInfo? : Option String := none
|
||||
/-- Optional style specification for the suggestion. If `none` (the default), the suggestion is
|
||||
styled as a text link. Otherwise, the suggestion can be styled as:
|
||||
* a status: `.error`, `.warning`, `.success`
|
||||
* a hypothesis name: `.asHypothesis`, `.asInaccessible`
|
||||
* a variable color: `.value (t : Float)`, which draws from a red-yellow-green gradient, with red
|
||||
at `0.0` and green at `1.0`.
|
||||
|
||||
See `SuggestionStyle` for details. -/
|
||||
style? : Option SuggestionStyle := none
|
||||
/-- How to represent the suggestion as `MessageData`. This is used only in the info diagnostic.
|
||||
If `none`, we use `suggestion`. Use `toMessageData` to render a `Suggestion` in this manner. -/
|
||||
messageData? : Option MessageData := none
|
||||
/-- How to construct the text that appears in the lightbulb menu from the suggestion text. If
|
||||
`none`, we use `fun ppSuggestionText => "Try this: " ++ ppSuggestionText`. Only the pretty-printed
|
||||
`suggestion : SuggestionText` is used here. -/
|
||||
toCodeActionTitle? : Option (String → String) := none
|
||||
deriving Inhabited
|
||||
|
||||
/-- Converts a `Suggestion` to `Json` in `CoreM`. We need `CoreM` in order to pretty-print syntax.
|
||||
|
||||
This also returns a `String × Option String` consisting of the pretty-printed text and any custom
|
||||
code action title if `toCodeActionTitle?` is provided.
|
||||
|
||||
If `w := none`, then `w := getInputWidth (← getOptions)` is used.
|
||||
-/
|
||||
def Suggestion.toJsonAndInfoM (s : Suggestion) (w : Option Nat := none) (indent column : Nat := 0) :
|
||||
CoreM (Json × String × Option String) := do
|
||||
let text ← s.suggestion.prettyExtra w indent column
|
||||
let mut json := [("suggestion", (text : Json))]
|
||||
if let some preInfo := s.preInfo? then json := ("preInfo", preInfo) :: json
|
||||
if let some postInfo := s.postInfo? then json := ("postInfo", postInfo) :: json
|
||||
if let some style := s.style? then json := ("style", toJson style) :: json
|
||||
return (Json.mkObj json, text, s.toCodeActionTitle?.map (· text))
|
||||
|
||||
/- If `messageData?` is specified, we use that; otherwise (by default), we use `toMessageData` of
|
||||
the suggestion text. -/
|
||||
instance : ToMessageData Suggestion where
|
||||
toMessageData s := s.messageData?.getD (toMessageData s.suggestion)
|
||||
|
||||
instance : Coe SuggestionText Suggestion where
|
||||
coe t := { suggestion := t }
|
||||
|
||||
/-- Delaborate `e` into a suggestion suitable for use by `refine`. -/
|
||||
def delabToRefinableSuggestion (e : Expr) : MetaM Suggestion :=
|
||||
return { suggestion := ← delabToRefinableSyntax e, messageData? := e }
|
||||
|
||||
/-! # Widget hooks -/
|
||||
|
||||
/-- Core of `addSuggestion` and `addSuggestions`. Whether we use an inline display for a single
|
||||
element or a list display is controlled by `isInline`. -/
|
||||
private def addSuggestionCore (ref : Syntax) (suggestions : Array Suggestion)
|
||||
(header : String) (isInline : Bool) (origSpan? : Option Syntax := none)
|
||||
(style? : Option SuggestionStyle := none)
|
||||
(codeActionPrefix? : Option String := none) : CoreM Unit := do
|
||||
if let some range := (origSpan?.getD ref).getRange? then
|
||||
let map ← getFileMap
|
||||
-- FIXME: this produces incorrect results when `by` is at the beginning of the line, i.e.
|
||||
-- replacing `tac` in `by tac`, because the next line will only be 2 space indented
|
||||
-- (less than `tac` which starts at column 3)
|
||||
let (indent, column) := getIndentAndColumn map range
|
||||
let suggestions ← suggestions.mapM (·.toJsonAndInfoM (indent := indent) (column := column))
|
||||
let suggestionTexts := suggestions.map (·.2)
|
||||
let suggestions := suggestions.map (·.1)
|
||||
let ref := Syntax.ofRange <| ref.getRange?.getD range
|
||||
let range := map.utf8RangeToLspRange range
|
||||
pushInfoLeaf <| .ofCustomInfo {
|
||||
stx := ref
|
||||
value := Dynamic.mk
|
||||
{ range, suggestionTexts, codeActionPrefix? : TryThisInfo }
|
||||
}
|
||||
Widget.savePanelWidgetInfo (hash tryThisWidget.javascript) ref
|
||||
(props := return json% {
|
||||
suggestions: $suggestions,
|
||||
range: $range,
|
||||
header: $header,
|
||||
isInline: $isInline,
|
||||
style: $style?
|
||||
})
|
||||
|
||||
/-- Add a "try this" suggestion. This has three effects:
|
||||
|
||||
* An info diagnostic is displayed saying `Try this: <suggestion>`
|
||||
* A widget is registered, saying `Try this: <suggestion>` with a link on `<suggestion>` to apply
|
||||
the suggestion
|
||||
* A code action is added, which will apply the suggestion.
|
||||
|
||||
The parameters are:
|
||||
* `ref`: the span of the info diagnostic
|
||||
* `s`: a `Suggestion`, which contains
|
||||
* `suggestion`: the replacement text;
|
||||
* `preInfo?`: an optional string shown immediately after the replacement text in the widget
|
||||
message (only)
|
||||
* `postInfo?`: an optional string shown immediately after the replacement text in the widget
|
||||
message (only)
|
||||
* `style?`: an optional `Json` object used as the value of the `style` attribute of the
|
||||
suggestion text's element (not the whole suggestion element).
|
||||
* `messageData?`: an optional message to display in place of `suggestion` in the info diagnostic
|
||||
(only). The widget message uses only `suggestion`. If `messageData?` is `none`, we simply use
|
||||
`suggestion` instead.
|
||||
* `toCodeActionTitle?`: an optional function `String → String` describing how to transform the
|
||||
pretty-printed suggestion text into the code action text which appears in the lightbulb menu.
|
||||
If `none`, we simply prepend `"Try This: "` to the suggestion text.
|
||||
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
|
||||
If not provided it defaults to `ref`.
|
||||
* `header`: a string that begins the display. By default, it is `"Try this: "`.
|
||||
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
|
||||
suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
|
||||
-/
|
||||
def addSuggestion (ref : Syntax) (s : Suggestion) (origSpan? : Option Syntax := none)
|
||||
(header : String := "Try this: ") (codeActionPrefix? : Option String := none) : MetaM Unit := do
|
||||
logInfoAt ref m!"{header}{s}"
|
||||
addSuggestionCore ref #[s] header (isInline := true) origSpan?
|
||||
(codeActionPrefix? := codeActionPrefix?)
|
||||
|
||||
/-- Add a list of "try this" suggestions as a single "try these" suggestion. This has three effects:
|
||||
|
||||
* An info diagnostic is displayed saying `Try these: <list of suggestions>`
|
||||
* A widget is registered, saying `Try these: <list of suggestions>` with a link on each
|
||||
`<suggestion>` to apply the suggestion
|
||||
* A code action for each suggestion is added, which will apply the suggestion.
|
||||
|
||||
The parameters are:
|
||||
* `ref`: the span of the info diagnostic
|
||||
* `suggestions`: an array of `Suggestion`s, which each contain
|
||||
* `suggestion`: the replacement text;
|
||||
* `preInfo?`: an optional string shown immediately after the replacement text in the widget
|
||||
message (only)
|
||||
* `postInfo?`: an optional string shown immediately after the replacement text in the widget
|
||||
message (only)
|
||||
* `style?`: an optional `Json` object used as the value of the `style` attribute of the
|
||||
suggestion text's element (not the whole suggestion element).
|
||||
* `messageData?`: an optional message to display in place of `suggestion` in the info diagnostic
|
||||
(only). The widget message uses only `suggestion`. If `messageData?` is `none`, we simply use
|
||||
`suggestion` instead.
|
||||
* `toCodeActionTitle?`: an optional function `String → String` describing how to transform the
|
||||
pretty-printed suggestion text into the code action text which appears in the lightbulb menu.
|
||||
If `none`, we simply prepend `"Try This: "` to the suggestion text.
|
||||
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
|
||||
If not provided it defaults to `ref`.
|
||||
* `header`: a string that precedes the list. By default, it is `"Try these:"`.
|
||||
* `style?`: a default style for all suggestions which do not have a custom `style?` set.
|
||||
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
|
||||
suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
|
||||
used.
|
||||
-/
|
||||
def addSuggestions (ref : Syntax) (suggestions : Array Suggestion)
|
||||
(origSpan? : Option Syntax := none) (header : String := "Try these:")
|
||||
(style? : Option SuggestionStyle := none)
|
||||
(codeActionPrefix? : Option String := none) : MetaM Unit := do
|
||||
if suggestions.isEmpty then throwErrorAt ref "no suggestions available"
|
||||
let msgs := suggestions.map toMessageData
|
||||
let msgs := msgs.foldl (init := MessageData.nil) (fun msg m => msg ++ m!"\n• " ++ m)
|
||||
logInfoAt ref m!"{header}{msgs}"
|
||||
addSuggestionCore ref suggestions header (isInline := false) origSpan? style? codeActionPrefix?
|
||||
|
||||
private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion := do
|
||||
let stx ← delabToRefinableSyntax e
|
||||
let mvars ← getMVars e
|
||||
let suggestion ← if mvars.isEmpty then `(tactic| exact $stx) else `(tactic| refine $stx)
|
||||
let messageData? := if mvars.isEmpty then m!"exact {e}" else m!"refine {e}"
|
||||
let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else
|
||||
let mut str := "\nRemaining subgoals:"
|
||||
for g in mvars do
|
||||
-- TODO: use a MessageData.ofExpr instead of rendering to string
|
||||
let e ← PrettyPrinter.ppExpr (← instantiateMVars (← g.getType))
|
||||
str := str ++ Format.pretty ("\n⊢ " ++ e)
|
||||
pure str
|
||||
pure { suggestion, postInfo?, messageData? }
|
||||
|
||||
/-- Add an `exact e` or `refine e` suggestion.
|
||||
|
||||
The parameters are:
|
||||
* `ref`: the span of the info diagnostic
|
||||
* `e`: the replacement expression
|
||||
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
|
||||
If not provided it defaults to `ref`.
|
||||
* `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after
|
||||
`Remaining subgoals:`
|
||||
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
|
||||
suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
|
||||
-/
|
||||
def addExactSuggestion (ref : Syntax) (e : Expr)
|
||||
(origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
|
||||
(codeActionPrefix? : Option String := none): MetaM Unit := do
|
||||
addSuggestion ref (← addExactSuggestionCore addSubgoalsMsg e)
|
||||
(origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
|
||||
|
||||
/-- Add `exact e` or `refine e` suggestions.
|
||||
|
||||
The parameters are:
|
||||
* `ref`: the span of the info diagnostic
|
||||
* `es`: the array of replacement expressions
|
||||
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
|
||||
If not provided it defaults to `ref`.
|
||||
* `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after
|
||||
`Remaining subgoals:`
|
||||
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
|
||||
suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
|
||||
used.
|
||||
-/
|
||||
def addExactSuggestions (ref : Syntax) (es : Array Expr)
|
||||
(origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
|
||||
(codeActionPrefix? : Option String := none) : MetaM Unit := do
|
||||
let suggestions ← es.mapM <| addExactSuggestionCore addSubgoalsMsg
|
||||
addSuggestions ref suggestions (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
|
||||
|
||||
/-- Add a term suggestion.
|
||||
|
||||
The parameters are:
|
||||
* `ref`: the span of the info diagnostic
|
||||
* `e`: the replacement expression
|
||||
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
|
||||
If not provided it defaults to `ref`.
|
||||
* `header`: a string which precedes the suggestion. By default, it's `"Try this: "`.
|
||||
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
|
||||
suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
|
||||
-/
|
||||
def addTermSuggestion (ref : Syntax) (e : Expr)
|
||||
(origSpan? : Option Syntax := none) (header : String := "Try this: ")
|
||||
(codeActionPrefix? : Option String := none) : MetaM Unit := do
|
||||
addSuggestion ref (← delabToRefinableSuggestion e) (origSpan? := origSpan?) (header := header)
|
||||
(codeActionPrefix? := codeActionPrefix?)
|
||||
|
||||
/-- Add term suggestions.
|
||||
|
||||
The parameters are:
|
||||
* `ref`: the span of the info diagnostic
|
||||
* `es`: an array of the replacement expressions
|
||||
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
|
||||
If not provided it defaults to `ref`.
|
||||
* `header`: a string which precedes the list of suggestions. By default, it's `"Try these:"`.
|
||||
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
|
||||
suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
|
||||
used.
|
||||
-/
|
||||
def addTermSuggestions (ref : Syntax) (es : Array Expr)
|
||||
(origSpan? : Option Syntax := none) (header : String := "Try these:")
|
||||
(codeActionPrefix? : Option String := none) : MetaM Unit := do
|
||||
addSuggestions ref (← es.mapM delabToRefinableSuggestion)
|
||||
(origSpan? := origSpan?) (header := header) (codeActionPrefix? := codeActionPrefix?)
|
||||
|
||||
open Lean Elab Elab.Tactic PrettyPrinter Meta
|
||||
|
||||
/-- Add a suggestion for `have h : t := e`. -/
|
||||
def addHaveSuggestion (ref : Syntax) (h? : Option Name) (t? : Option Expr) (e : Expr)
|
||||
(origSpan? : Option Syntax := none) : TermElabM Unit := do
|
||||
let estx ← delabToRefinableSyntax e
|
||||
let prop ← isProp (← inferType e)
|
||||
let tac ← if let some t := t? then
|
||||
let tstx ← delabToRefinableSyntax t
|
||||
if prop then
|
||||
match h? with
|
||||
| some h => `(tactic| have $(mkIdent h) : $tstx := $estx)
|
||||
| none => `(tactic| have : $tstx := $estx)
|
||||
else
|
||||
`(tactic| let $(mkIdent (h?.getD `_)) : $tstx := $estx)
|
||||
else
|
||||
if prop then
|
||||
match h? with
|
||||
| some h => `(tactic| have $(mkIdent h) := $estx)
|
||||
| none => `(tactic| have := $estx)
|
||||
else
|
||||
`(tactic| let $(mkIdent (h?.getD `_)) := $estx)
|
||||
addSuggestion ref tac origSpan?
|
||||
|
||||
open Lean.Parser.Tactic
|
||||
open Lean.Syntax
|
||||
|
||||
/-- Add a suggestion for `rw [h₁, ← h₂] at loc`. -/
|
||||
def addRewriteSuggestion (ref : Syntax) (rules : List (Expr × Bool))
|
||||
(type? : Option Expr := none) (loc? : Option Expr := none)
|
||||
(origSpan? : Option Syntax := none) :
|
||||
TermElabM Unit := do
|
||||
let rules_stx := TSepArray.ofElems <| ← rules.toArray.mapM fun ⟨e, symm⟩ => do
|
||||
let t ← delabToRefinableSyntax e
|
||||
if symm then `(rwRule| ← $t:term) else `(rwRule| $t:term)
|
||||
let tac ← do
|
||||
let loc ← loc?.mapM fun loc => do `(location| at $(← delab loc):term)
|
||||
`(tactic| rw [$rules_stx,*] $(loc)?)
|
||||
|
||||
-- We don't simply write `let mut tacMsg := m!"{tac}"` here
|
||||
-- but instead rebuild it, so that there are embedded `Expr`s in the message,
|
||||
-- thus giving more information in the hovers.
|
||||
-- Perhaps in future we will have a better way to attach elaboration information to
|
||||
-- `Syntax` embedded in a `MessageData`.
|
||||
let mut tacMsg :=
|
||||
let rulesMsg := MessageData.sbracket <| MessageData.joinSep
|
||||
(rules.map fun ⟨e, symm⟩ => (if symm then "← " else "") ++ m!"{e}") ", "
|
||||
if let some loc := loc? then
|
||||
m!"rw {rulesMsg} at {loc}"
|
||||
else
|
||||
m!"rw {rulesMsg}"
|
||||
let mut extraMsg := ""
|
||||
if let some type := type? then
|
||||
tacMsg := tacMsg ++ m!"\n-- {type}"
|
||||
extraMsg := extraMsg ++ s!"\n-- {← PrettyPrinter.ppExpr type}"
|
||||
addSuggestion ref (s := { suggestion := tac, postInfo? := extraMsg, messageData? := tacMsg })
|
||||
origSpan?
|
||||
@@ -18,7 +18,6 @@ Lean's IR.
|
||||
#include "runtime/string_ref.h"
|
||||
|
||||
#ifdef LEAN_LLVM
|
||||
#include "llvm-c/Analysis.h"
|
||||
#include "llvm-c/BitReader.h"
|
||||
#include "llvm-c/BitWriter.h"
|
||||
#include "llvm-c/Core.h"
|
||||
@@ -1425,74 +1424,3 @@ extern "C" LEAN_EXPORT lean_object *llvm_is_declaration(size_t ctx, size_t globa
|
||||
return lean_io_result_mk_ok(lean_box(is_bool));
|
||||
#endif // LEAN_LLVM
|
||||
}
|
||||
|
||||
extern "C" LEAN_EXPORT lean_object *lean_llvm_verify_module(size_t ctx, size_t mod,
|
||||
lean_object * /* w */) {
|
||||
#ifndef LEAN_LLVM
|
||||
lean_always_assert(
|
||||
false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
|
||||
"the LLVM backend function."));
|
||||
#else
|
||||
char* msg = NULL;
|
||||
LLVMBool broken = LLVMVerifyModule(lean_to_Module(mod), LLVMReturnStatusAction, &msg);
|
||||
if (broken) {
|
||||
return lean_io_result_mk_ok(lean::mk_option_some(lean_mk_string(msg)));
|
||||
} else {
|
||||
return lean_io_result_mk_ok(lean::mk_option_none());
|
||||
}
|
||||
#endif // LEAN_LLVM
|
||||
}
|
||||
|
||||
extern "C" LEAN_EXPORT lean_object *lean_llvm_count_basic_blocks(size_t ctx, size_t fn_val,
|
||||
lean_object * /* w */) {
|
||||
#ifndef LEAN_LLVM
|
||||
lean_always_assert(
|
||||
false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
|
||||
"the LLVM backend function."));
|
||||
#else
|
||||
LLVMValueRef fn_ref = lean_to_Value(fn_val);
|
||||
return lean_io_result_mk_ok(lean_box_uint64((uint64_t)LLVMCountBasicBlocks(fn_ref)));
|
||||
#endif // LEAN_LLVM
|
||||
}
|
||||
|
||||
extern "C" LEAN_EXPORT lean_object *lean_llvm_get_entry_basic_block(size_t ctx, size_t fn_val,
|
||||
lean_object * /* w */) {
|
||||
#ifndef LEAN_LLVM
|
||||
lean_always_assert(
|
||||
false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
|
||||
"the LLVM backend function."));
|
||||
#else
|
||||
LLVMValueRef fn_ref = lean_to_Value(fn_val);
|
||||
LLVMBasicBlockRef bb_ref = LLVMGetEntryBasicBlock(fn_ref);
|
||||
return lean_io_result_mk_ok(lean_box_usize(BasicBlock_to_lean(bb_ref)));
|
||||
#endif // LEAN_LLVM
|
||||
}
|
||||
|
||||
extern "C" LEAN_EXPORT lean_object *lean_llvm_get_first_instruction(size_t ctx, size_t bb,
|
||||
lean_object * /* w */) {
|
||||
#ifndef LEAN_LLVM
|
||||
lean_always_assert(
|
||||
false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
|
||||
"the LLVM backend function."));
|
||||
#else
|
||||
LLVMBasicBlockRef bb_ref = lean_to_BasicBlock(bb);
|
||||
LLVMValueRef instr_ref = LLVMGetFirstInstruction(bb_ref);
|
||||
if (instr_ref == NULL) {
|
||||
return lean_io_result_mk_ok(lean::mk_option_none());
|
||||
} else {
|
||||
return lean_io_result_mk_ok(lean::mk_option_some(lean_box_usize(Value_to_lean(instr_ref))));
|
||||
}
|
||||
#endif // LEAN_LLVM
|
||||
}
|
||||
|
||||
extern "C" LEAN_EXPORT lean_object *lean_llvm_position_builder_before(
|
||||
size_t ctx, size_t builder, size_t instr, lean_object * /* w */) {
|
||||
#ifndef LEAN_LLVM
|
||||
lean_always_assert(
|
||||
false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
|
||||
"the LLVM backend function."));
|
||||
#else
|
||||
LLVMPositionBuilderBefore(lean_to_Builder(builder), lean_to_Value(instr));
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
#endif // LEAN_LLVM
|
||||
}
|
||||
|
||||
@@ -102,6 +102,3 @@ def printRangesTest : MetaM Unit := do
|
||||
printRanges `g.foo
|
||||
|
||||
#eval printRangesTest
|
||||
|
||||
/-- no dice -/
|
||||
add_decl_doc Nat.add
|
||||
|
||||
@@ -189,4 +189,3 @@ g.foo :=
|
||||
charUtf16 := 44,
|
||||
endPos := { line := 42, column := 47 },
|
||||
endCharUtf16 := 47 } }
|
||||
docStr.lean:106:0-107:20: error: invalid 'add_decl_doc', declaration is in an imported module
|
||||
|
||||
@@ -1,23 +0,0 @@
|
||||
import Lean
|
||||
|
||||
#eval match true with | true => false | false => true
|
||||
|
||||
open Lean Elab Command Meta
|
||||
#eval show CommandElabM Unit from do
|
||||
match ([] : List Nat) with
|
||||
| [] =>
|
||||
liftCoreM <| addDecl <| Declaration.defnDecl {
|
||||
name := `foo
|
||||
type := Lean.mkConst ``Bool
|
||||
levelParams := []
|
||||
value := Lean.mkConst ``true
|
||||
hints := .opaque
|
||||
safety := .safe
|
||||
}
|
||||
| _ => return ()
|
||||
|
||||
#check foo
|
||||
-- The auxiliary declarations created to elaborate the commands above
|
||||
-- should not leak into the environment
|
||||
#check _eval.match_1 -- Should fail
|
||||
#check _eval.match_2 -- Should fail
|
||||
@@ -1,4 +0,0 @@
|
||||
false
|
||||
foo : Bool
|
||||
evalLeak.lean:22:7-22:20: error: unknown identifier '_eval.match_1'
|
||||
evalLeak.lean:23:7-23:20: error: unknown identifier '_eval.match_2'
|
||||
@@ -63,5 +63,3 @@ def foo : a b c d e f g a b c d e f g h where
|
||||
#eval fmt `(calc
|
||||
1 = 1 := rfl
|
||||
1 = 1 := rfl)
|
||||
|
||||
#eval fmt `(by rw [] at h)
|
||||
|
||||
@@ -70,4 +70,3 @@ def foo✝ : a✝ b✝ c✝ d✝ e✝ f✝ g✝ a✝ b✝ c✝ d✝ e✝ f✝ g
|
||||
calc
|
||||
1 = 1 := rfl✝
|
||||
1 = 1 := rfl✝
|
||||
by rw [] at h✝
|
||||
|
||||
@@ -24,17 +24,6 @@
|
||||
"label": "format.indent",
|
||||
"kind": 10,
|
||||
"detail": "(2), indentation"},
|
||||
{"textEdit":
|
||||
{"replace":
|
||||
{"start": {"line": 1, "character": 11},
|
||||
"end": {"line": 1, "character": 17}},
|
||||
"newText": "format.inputWidth",
|
||||
"insert":
|
||||
{"start": {"line": 1, "character": 11},
|
||||
"end": {"line": 1, "character": 17}}},
|
||||
"label": "format.inputWidth",
|
||||
"kind": 10,
|
||||
"detail": "(100), ideal input width"},
|
||||
{"textEdit":
|
||||
{"replace":
|
||||
{"start": {"line": 1, "character": 11},
|
||||
@@ -96,17 +85,6 @@
|
||||
"label": "format.indent",
|
||||
"kind": 10,
|
||||
"detail": "(2), indentation"},
|
||||
{"textEdit":
|
||||
{"replace":
|
||||
{"start": {"line": 4, "character": 11},
|
||||
"end": {"line": 4, "character": 20}},
|
||||
"newText": "format.inputWidth",
|
||||
"insert":
|
||||
{"start": {"line": 4, "character": 11},
|
||||
"end": {"line": 4, "character": 20}}},
|
||||
"label": "format.inputWidth",
|
||||
"kind": 10,
|
||||
"detail": "(100), ideal input width"},
|
||||
{"textEdit":
|
||||
{"replace":
|
||||
{"start": {"line": 4, "character": 11},
|
||||
@@ -250,17 +228,6 @@
|
||||
"label": "format.indent",
|
||||
"kind": 10,
|
||||
"detail": "(2), indentation"},
|
||||
{"textEdit":
|
||||
{"replace":
|
||||
{"start": {"line": 13, "character": 11},
|
||||
"end": {"line": 13, "character": 17}},
|
||||
"newText": "format.inputWidth",
|
||||
"insert":
|
||||
{"start": {"line": 13, "character": 11},
|
||||
"end": {"line": 13, "character": 17}}},
|
||||
"label": "format.inputWidth",
|
||||
"kind": 10,
|
||||
"detail": "(100), ideal input width"},
|
||||
{"textEdit":
|
||||
{"replace":
|
||||
{"start": {"line": 13, "character": 11},
|
||||
@@ -322,17 +289,6 @@
|
||||
"label": "format.indent",
|
||||
"kind": 10,
|
||||
"detail": "(2), indentation"},
|
||||
{"textEdit":
|
||||
{"replace":
|
||||
{"start": {"line": 16, "character": 11},
|
||||
"end": {"line": 16, "character": 18}},
|
||||
"newText": "format.inputWidth",
|
||||
"insert":
|
||||
{"start": {"line": 16, "character": 11},
|
||||
"end": {"line": 16, "character": 18}}},
|
||||
"label": "format.inputWidth",
|
||||
"kind": 10,
|
||||
"detail": "(100), ideal input width"},
|
||||
{"textEdit":
|
||||
{"replace":
|
||||
{"start": {"line": 16, "character": 11},
|
||||
|
||||
@@ -1,7 +0,0 @@
|
||||
example (hp : p) (hq : q) (hr : r) : (p ∧ q) ∧ (q ∧ (r ∧ p)) := by
|
||||
and_intros
|
||||
· exact hp
|
||||
· exact hq
|
||||
· exact hq
|
||||
· exact hr
|
||||
· exact hp
|
||||
@@ -1,76 +0,0 @@
|
||||
private axiom test_sorry : ∀ {α}, α
|
||||
|
||||
example : n + 2 = m := by
|
||||
change n + 1 + 1 = _
|
||||
guard_target =ₛ n + 1 + 1 = m
|
||||
exact test_sorry
|
||||
|
||||
example (h : n + 2 = m) : False := by
|
||||
change _ + 1 = _ at h
|
||||
guard_hyp h :ₛ n + 1 + 1 = m
|
||||
exact test_sorry
|
||||
|
||||
example : n + 2 = m := by
|
||||
fail_if_success change true
|
||||
fail_if_success change _ + 3 = _
|
||||
fail_if_success change _ * _ = _
|
||||
change (_ : Nat) + _ = _
|
||||
exact test_sorry
|
||||
|
||||
-- `change ... at ...` allows placeholders to mean different things at different hypotheses
|
||||
example (h : n + 3 = m) (h' : n + 2 = m) : False := by
|
||||
change _ + 1 = _ at h h'
|
||||
guard_hyp h :ₛ n + 2 + 1 = m
|
||||
guard_hyp h' :ₛ n + 1 + 1 = m
|
||||
exact test_sorry
|
||||
|
||||
-- `change ... at ...` preserves dependencies
|
||||
example (p : n + 2 = m → Type) (h : n + 2 = m) (x : p h) : false := by
|
||||
change _ + 1 = _ at h
|
||||
guard_hyp x :ₛ p h
|
||||
exact test_sorry
|
||||
|
||||
noncomputable example : Nat := by
|
||||
fail_if_success change Type 1
|
||||
exact test_sorry
|
||||
|
||||
def foo (a b c : Nat) := if a < b then c else 0
|
||||
|
||||
example : foo 1 2 3 = 3 := by
|
||||
change (if _ then _ else _) = _
|
||||
change ite _ _ _ = _
|
||||
change (if _ < _ then _ else _) = _
|
||||
change _ = (if true then 3 else 4)
|
||||
rfl
|
||||
|
||||
example (h : foo 1 2 3 = 4) : True := by
|
||||
change ite _ _ _ = _ at h
|
||||
guard_hyp h :ₛ ite (1 < 2) 3 0 = 4
|
||||
trivial
|
||||
|
||||
example (h : foo 1 2 3 = 4) : True := by
|
||||
change (if _ then _ else _) = _ at h
|
||||
guard_hyp h : (if 1 < 2 then 3 else 0) = 4
|
||||
trivial
|
||||
|
||||
example (α : Type) [LT α] (x : α) (h : x < x) : x < id x := by
|
||||
change _ < _ -- can defer LT typeclass lookup, just like `show`
|
||||
change _ < _ at h -- can defer LT typeclass lookup at h too
|
||||
guard_target =ₛ x < id x
|
||||
change _ < x
|
||||
guard_target =ₛ x < x
|
||||
exact h
|
||||
|
||||
-- This example shows using named and anonymous placeholders to create a new goal.
|
||||
example (x y : Nat) (h : x = y) : True := by
|
||||
change (if 1 < 2 then x else ?z + ?_) = y at h
|
||||
rotate_left
|
||||
· exact 4
|
||||
· exact 37
|
||||
guard_hyp h : (if 1 < 2 then x else 4 + 37) = y
|
||||
· trivial
|
||||
|
||||
example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 := by
|
||||
intro x y z -- `z` was previously erroneously marked as unused
|
||||
change _ at y
|
||||
exact z.2
|
||||
@@ -1,46 +0,0 @@
|
||||
/-
|
||||
Copyright (c) 2022 Arthur Paulino. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Arthur Paulino
|
||||
-/
|
||||
|
||||
example (h : Int) : Nat := by
|
||||
replace h : Nat := 0
|
||||
exact h
|
||||
|
||||
example (h : Nat) : Nat := by
|
||||
have h : Int := 0
|
||||
assumption -- original `h` is not absent but...
|
||||
|
||||
example (h : Nat) : Nat := by
|
||||
replace h : Int := 0
|
||||
fail_if_success assumption -- original `h` is absent now
|
||||
replace h : Nat := 0
|
||||
exact h
|
||||
|
||||
-- tests with `this`
|
||||
|
||||
example : Nat := by
|
||||
have : Int := 0
|
||||
replace : Nat := 0
|
||||
assumption
|
||||
|
||||
example : Nat := by
|
||||
have : Nat := 0
|
||||
have : Int := 0
|
||||
assumption -- original `this` is not absent but...
|
||||
|
||||
example : Nat := by
|
||||
have : Nat := 0
|
||||
replace : Int := 0
|
||||
fail_if_success assumption -- original `this` is absent now
|
||||
replace : Nat := 0
|
||||
assumption
|
||||
|
||||
-- trying to replace the type of a variable when the goal depends on it
|
||||
|
||||
example {a : Nat} : a = a := by
|
||||
replace a : Int := 0
|
||||
have : Nat := by assumption -- old `a` is not gone
|
||||
have : Int := by exact a -- new `a` is of type `Int`
|
||||
simp
|
||||
@@ -65,7 +65,7 @@ Try this: simp only [bla, h] at *
|
||||
| Sum.inl (y, z) => y + z
|
||||
| Sum.inr val => 0
|
||||
[Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
|
||||
Try this: simp only [bla, h] at h'
|
||||
Try this: simp only [bla, h] at h'
|
||||
[Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
|
||||
| Sum.inl (y, z) => y + z
|
||||
| Sum.inr val => 0
|
||||
|
||||
@@ -4,7 +4,7 @@ structure resulting type
|
||||
Type ?u
|
||||
recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the structure resulting universe level
|
||||
S6 : Sort (max w₁ w₂) → Type w₂ → Sort (max w₁ (w₂ + 1))
|
||||
univInference.lean:45:0-46:17: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u')
|
||||
univInference.lean:45:0-46:17: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
|
||||
max u v
|
||||
univInference.lean:65:2-65:22: error: failed to compute resulting universe level of inductive datatype, constructor 'Induct.S4.mk' has type
|
||||
{α : Sort u} → {β : Sort v} → α → β → S4 α β
|
||||
@@ -13,7 +13,7 @@ parameter 'a' has type
|
||||
inductive type resulting type
|
||||
Type ?u
|
||||
recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the inductive type resulting universe level
|
||||
univInference.lean:73:0-74:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u')
|
||||
univInference.lean:73:0-74:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
|
||||
max u v
|
||||
univInference.lean:81:0-82:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u')
|
||||
univInference.lean:81:0-82:22: error: invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
|
||||
max u v
|
||||
|
||||
Reference in New Issue
Block a user