@@ -30,6 +30,7 @@ declare_config_elab elabCutsatConfig Grind.CutsatConfig
3030declare_config_elab elabGrobnerConfig Grind.GrobnerConfig
3131
3232open Command Term in
33+ open Lean.Parser.Command.GrindCnstr in
3334@[builtin_command_elab Lean.Parser.Command.grindPattern]
3435def elabGrindPattern : CommandElab := fun stx => do
3536 match stx with
@@ -38,41 +39,92 @@ def elabGrindPattern : CommandElab := fun stx => do
3839 | `(local grind_pattern $thmName:ident => $terms,* $[$cnstrs?:grindPatternCnstrs]?) => go thmName terms cnstrs? .local
3940 | _ => throwUnsupportedSyntax
4041where
42+ findLHS (xs : Array Expr) (lhs : Syntax) : TermElabM (LocalDecl × Nat) := do
43+ let lhsId := lhs.getId
44+ let mut i := 0
45+ for x in xs do
46+ let xDecl ← x.fvarId!.getDecl
47+ if xDecl.userName == lhsId then
48+ return (xDecl, xs.size - i - 1 )
49+ i := i + 1
50+ throwErrorAt lhs "invalid constraint, `{lhsId}` is not local variable of the theorem"
51+
52+ elabCnstrRHS (xs : Array Expr) (rhs : Syntax) (expectedType : Expr) : TermElabM Grind.CnstrRHS := do
53+ /-
54+ **Note** : We need better sanity checking here.
55+ We must check whether the type of `rhs` is type correct with respect to
56+ an arbitrary instantiation of `xs`. That is, we should use meta-variables
57+ in the check. It is incorrect to use `xDecl.type`. For example, suppose the
58+ type of `xDecl` is `α → β` where `α` and `β` are variables in `xs` occurring before
59+ `xDecl`, and `rhsExpr` is `some : ?m → ?m`. The types `α → β =?= ?m → ?m` are
60+ not definitionally equal, but `?α → ?β =?= ?m → ?m` are.
61+ -/
62+ let rhsExpr ← Term.elabTerm rhs expectedType
63+ Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true )
64+ let rhsExpr ← instantiateMVars rhsExpr
65+ if rhsExpr.hasSyntheticSorry then
66+ throwErrorAt rhs "invalid constraint, rhs contains a synthetic `sorry`"
67+ let rhsExpr := rhsExpr.eta
68+ let { paramNames := levelNames, mvars, expr := rhs } ← abstractMVars rhsExpr
69+ let numMVars := mvars.size
70+ let rhs := rhs.abstract xs
71+ return { levelNames, numMVars, expr := rhs }
72+
73+ elabProp (xs : Array Expr) (term : Syntax) : TermElabM Expr := do
74+ let e ← Term.elabTermAndSynthesize term (Expr.sort 0 )
75+ let e ← instantiateMVars e
76+ if e.hasSyntheticSorry then
77+ throwErrorAt term "invalid proposition, it contains a synthetic `sorry`"
78+ if e.hasMVar then
79+ throwErrorAt term "invalid proposition, it contains metavariables{indentExpr e}"
80+ return e.abstract xs
81+
82+ elabNotDefEq (xs : Array Expr) (lhs rhs : Syntax) : TermElabM Grind.EMatchTheoremConstraint := do
83+ let (localDecl, lhsBVarIdx) ← findLHS xs lhs
84+ let rhs ← elabCnstrRHS xs rhs localDecl.type
85+ return .notDefEq lhsBVarIdx rhs
86+
87+ elabDefEq (xs : Array Expr) (lhs rhs : Syntax) : TermElabM Grind.EMatchTheoremConstraint := do
88+ let (localDecl, lhsBVarIdx) ← findLHS xs lhs
89+ let rhs ← elabCnstrRHS xs rhs localDecl.type
90+ return .defEq lhsBVarIdx rhs
91+
4192 elabCnstrs (xs : Array Expr) (cnstrs? : Option (TSyntax ``Parser.Command.grindPatternCnstrs))
4293 : TermElabM (List (Grind.EMatchTheoremConstraint)) := do
4394 let some cnstrs := cnstrs? | return []
4495 let cnstrs := cnstrs.raw[1 ].getArgs
4596 cnstrs.toList.mapM fun cnstr => do
46- -- **Note** : Hack because syntax matching is not working. Fix after another update stage0
47- let lhs := cnstr[0 ]
48- let rhs := cnstr[2 ]
49- let lhsId := lhs.getId
50- let mut i := 0
51- for x in xs do
52- let xDecl ← x.fvarId!.getDecl
53- if xDecl.userName == lhsId then
54- let bvarIdx := xs.size - i - 1
55- /-
56- **Note** : We need better sanity checking here.
57- We must check whether the type of `rhs` is type correct with respect to
58- an arbitrary instantiation of `xs`. That is, we should use meta-variables
59- in the check. It is incorrect to use `xDecl.type`. For example, suppose the
60- type of `xDecl` is `α → β` where `α` and `β` are variables in `xs` occurring before
61- `xDecl`, and `rhsExpr` is `some : ?m → ?m`. The types `α → β =?= ?m → ?m` are
62- not definitionally equal, but `?α → ?β =?= ?m → ?m` are.
63- -/
64- let rhsExpr ← Term.elabTerm rhs xDecl.type
65- Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true )
66- let rhsExpr ← instantiateMVars rhsExpr
67- if rhsExpr.hasSyntheticSorry then
68- throwErrorAt rhs "invalid constraint, rhs contains a synthetic `sorry`"
69- let rhsExpr := rhsExpr.eta
70- let { paramNames := levelNames, mvars, expr := rhs } ← abstractMVars rhsExpr
71- let numMVars := mvars.size
72- let rhs := rhs.abstract xs
73- return { bvarIdx, levelNames, numMVars, rhs }
74- i := i + 1
75- throwErrorAt lhs "invalid constraint, `{lhsId}` is not local variable of the theorem"
97+ let kind := cnstr.getKind
98+ if kind == ``notDefEq then
99+ elabNotDefEq xs cnstr[0 ] cnstr[2 ]
100+ else if kind == ``defEq then
101+ elabDefEq xs cnstr[0 ] cnstr[2 ]
102+ else if kind == ``genLt then
103+ let (_, lhs) ← findLHS xs cnstr[1 ]
104+ return .genLt lhs cnstr[3 ].toNat
105+ else if kind == ``sizeLt then
106+ let (_, lhs) ← findLHS xs cnstr[1 ]
107+ return .sizeLt lhs cnstr[3 ].toNat
108+ else if kind == ``depthLt then
109+ let (_, lhs) ← findLHS xs cnstr[1 ]
110+ return .depthLt lhs cnstr[3 ].toNat
111+ else if kind == ``maxInsts then
112+ return .maxInsts cnstr[1 ].toNat
113+ else if kind == ``isValue then
114+ let (_, lhs) ← findLHS xs cnstr[1 ]
115+ return .isValue lhs false
116+ else if kind == ``isStrictValue then
117+ let (_, lhs) ← findLHS xs cnstr[1 ]
118+ return .isValue lhs true
119+ else if kind == ``isGround then
120+ let (_, lhs) ← findLHS xs cnstr[1 ]
121+ return .isGround lhs
122+ else if kind == ``Parser.Command.GrindCnstr.check then
123+ return .check (← elabProp xs cnstr[1 ])
124+ else if kind == ``Parser.Command.GrindCnstr.guard then
125+ return .guard (← elabProp xs cnstr[1 ])
126+ else
127+ throwErrorAt cnstr "unexpected constraint"
76128
77129 go (thmName : TSyntax `ident) (terms : Syntax.TSepArray `term "," )
78130 (cnstrs? : Option (TSyntax ``Parser.Command.grindPatternCnstrs))
0 commit comments