|
| 1 | +/- |
| 2 | +Copyright (c) 2021 Microsoft Corporation. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Leonardo de Moura |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +prelude |
| 9 | +public import Lean.Meta.Basic |
| 10 | +public import Lean.Meta.Match.MatcherInfo |
| 11 | +import Lean.Meta.Match.NamedPatterns |
| 12 | +import Lean.Meta.MatchUtil |
| 13 | +import Lean.Meta.AppBuilder |
| 14 | + |
| 15 | +public section |
| 16 | + |
| 17 | +/-! |
| 18 | +This module has telescope functions for macher alts. They are primariliy used |
| 19 | +in `Match.MatchEqs`, but also in `MatcherApp.Transform`, hence the sparate module. |
| 20 | +-/ |
| 21 | + |
| 22 | +namespace Lean.Meta.Match |
| 23 | +/-- |
| 24 | + Similar to `forallTelescopeReducing`, but |
| 25 | +
|
| 26 | + 1. Eliminates arguments for named parameters and the associated equation proofs. |
| 27 | +
|
| 28 | + 2. Instantiate the `Unit` parameter of an otherwise argumentless alternative. |
| 29 | +
|
| 30 | + It does not handle the equality parameters associated with the `h : discr` notation. |
| 31 | +
|
| 32 | + The continuation `k` takes four arguments `ys args mask type`. |
| 33 | + - `ys` are variables for the hypotheses that have not been eliminated. |
| 34 | + - `args` are the arguments for the alternative `alt` that has type `altType`. `ys.size <= args.size` |
| 35 | + - `mask[i]` is true if the hypotheses has not been eliminated. `mask.size == args.size`. |
| 36 | + - `type` is the resulting type for `altType`. |
| 37 | +
|
| 38 | + We use the `mask` to build the splitter proof. See `mkSplitterProof`. |
| 39 | +
|
| 40 | + This can be used to use the alternative of a match expression in its splitter. |
| 41 | +-/ |
| 42 | +public partial def forallAltVarsTelescope (altType : Expr) (altInfo : AltParamInfo) |
| 43 | + (k : (patVars : Array Expr) → (args : Array Expr) → (mask : Array Bool) → (type : Expr) → MetaM α) : MetaM α := do |
| 44 | + assert! altInfo.numOverlaps = 0 |
| 45 | + if altInfo.hasUnitThunk then |
| 46 | + let type ← whnfForall altType |
| 47 | + let type ← Match.unfoldNamedPattern type |
| 48 | + let type ← instantiateForall type #[mkConst ``Unit.unit] |
| 49 | + k #[] #[mkConst ``Unit.unit] #[false] type |
| 50 | + else |
| 51 | + go #[] #[] #[] 0 altType |
| 52 | +where |
| 53 | + go (ys : Array Expr) (args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) : MetaM α := do |
| 54 | + let type ← whnfForall type |
| 55 | + |
| 56 | + if i < altInfo.numFields then |
| 57 | + let Expr.forallE n d b .. := type |
| 58 | + | throwError "expecting {altInfo.numFields} parameters, but found type{indentExpr altType}" |
| 59 | + |
| 60 | + let d ← Match.unfoldNamedPattern d |
| 61 | + withLocalDeclD n d fun y => do |
| 62 | + let typeNew := b.instantiate1 y |
| 63 | + if let some (_, lhs, rhs) ← matchEq? d then |
| 64 | + if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then |
| 65 | + let some j := ys.finIdxOf? lhs | unreachable! |
| 66 | + let ys := ys.eraseIdx j |
| 67 | + let some k := args.idxOf? lhs | unreachable! |
| 68 | + let mask := mask.set! k false |
| 69 | + let args := args.map fun arg => if arg == lhs then rhs else arg |
| 70 | + let arg ← mkEqRefl rhs |
| 71 | + let typeNew := typeNew.replaceFVar lhs rhs |
| 72 | + return ← withReplaceFVarId lhs.fvarId! rhs do |
| 73 | + withReplaceFVarId y.fvarId! arg do |
| 74 | + go ys (args.push arg) (mask.push false) (i+1) typeNew |
| 75 | + go (ys.push y) (args.push y) (mask.push true) (i+1) typeNew |
| 76 | + else |
| 77 | + let type ← Match.unfoldNamedPattern type |
| 78 | + k ys args mask type |
| 79 | + |
| 80 | + isNamedPatternProof (type : Expr) (h : Expr) : Bool := |
| 81 | + Option.isSome <| type.find? fun e => |
| 82 | + if let some e := Match.isNamedPattern? e then |
| 83 | + e.appArg! == h |
| 84 | + else |
| 85 | + false |
| 86 | + |
| 87 | + |
| 88 | +/-- |
| 89 | + Extension of `forallAltTelescope` that continues further: |
| 90 | +
|
| 91 | + Equality parameters associated with the `h : discr` notation are replaced with `rfl` proofs. |
| 92 | + Recall that this kind of parameter always occurs after the parameters corresponding to pattern |
| 93 | + variables. |
| 94 | +
|
| 95 | + The continuation `k` takes four arguments `ys args mask type`. |
| 96 | + - `ys` are variables for the hypotheses that have not been eliminated. |
| 97 | + - `eqs` are variables for equality hypotheses associated with discriminants annotated with `h : discr`. |
| 98 | + - `args` are the arguments for the alternative `alt` that has type `altType`. `ys.size <= args.size` |
| 99 | + - `mask[i]` is true if the hypotheses has not been eliminated. `mask.size == args.size`. |
| 100 | + - `type` is the resulting type for `altType`. |
| 101 | +
|
| 102 | + We use the `mask` to build the splitter proof. See `mkSplitterProof`. |
| 103 | +
|
| 104 | + This can be used to use the alternative of a match expression in its splitter. |
| 105 | +-/ |
| 106 | +public partial def forallAltTelescope (altType : Expr) (altInfo : AltParamInfo) (numDiscrEqs : Nat) |
| 107 | + (k : (ys : Array Expr) → (eqs : Array Expr) → (args : Array Expr) → (mask : Array Bool) → (type : Expr) → MetaM α) |
| 108 | + : MetaM α := do |
| 109 | + forallAltVarsTelescope altType altInfo fun ys args mask altType => do |
| 110 | + go ys #[] args mask 0 altType |
| 111 | +where |
| 112 | + go (ys : Array Expr) (eqs : Array Expr) (args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) : MetaM α := do |
| 113 | + let type ← whnfForall type |
| 114 | + if i < numDiscrEqs then |
| 115 | + let Expr.forallE n d b .. := type |
| 116 | + | throwError "expecting {numDiscrEqs} equalities, but found type{indentExpr altType}" |
| 117 | + let arg ← if let some (_, _, rhs) ← matchEq? d then |
| 118 | + mkEqRefl rhs |
| 119 | + else if let some (_, _, _, rhs) ← matchHEq? d then |
| 120 | + mkHEqRefl rhs |
| 121 | + else |
| 122 | + throwError "unexpected match alternative type{indentExpr altType}" |
| 123 | + withLocalDeclD n d fun eq => do |
| 124 | + let typeNew := b.instantiate1 eq |
| 125 | + go ys (eqs.push eq) (args.push arg) (mask.push false) (i+1) typeNew |
| 126 | + else |
| 127 | + let type ← unfoldNamedPattern type |
| 128 | + k ys eqs args mask type |
0 commit comments