From 49e90642022f41461fac575bfb663e161dd2505f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 15 Nov 2020 14:22:05 -0800 Subject: [PATCH] refactor: add `MatcherInfo.lean` --- src/Lean/Meta/Match/Match.lean | 99 +----------------------- src/Lean/Meta/Match/MatcherInfo.lean | 111 +++++++++++++++++++++++++++ 2 files changed, 112 insertions(+), 98 deletions(-) create mode 100644 src/Lean/Meta/Match/MatcherInfo.lean diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index ed774bd01b..7d15d62f0a 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -10,6 +10,7 @@ import Lean.Meta.Check import Lean.Meta.Closure import Lean.Meta.Tactic.Cases import Lean.Meta.GeneralizeTelescope +import Lean.Meta.Match.MatcherInfo import Lean.Meta.Match.MVarRenaming import Lean.Meta.Match.CaseValues import Lean.Meta.Match.CaseArraySizes @@ -767,56 +768,6 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := withIn else liftM $ throwNonSupported p -/-- -A "matcher" auxiliary declaration has the following structure: -- `numParams` parameters -- motive -- `numDiscrs` discriminators (aka major premises) -- `altNumParams.size` alternatives (aka minor premises) where alternative `i` has `altNumParams[i]` parameters -- `uElimPos?` is `some pos` when the matcher can eliminate in different universe levels, and - `pos` is the position of the universe level parameter that specifies the elimination universe. - It is `none` if the matcher only eliminates into `Prop`. -/ -structure MatcherInfo := - (numParams : Nat) - (numDiscrs : Nat) - (altNumParams : Array Nat) - (uElimPos? : Option Nat) - -def MatcherInfo.numAlts (matcherInfo : MatcherInfo) : Nat := - matcherInfo.altNumParams.size - -namespace Extension - -structure Entry := - (name : Name) - (info : MatcherInfo) - -structure State := - (map : SMap Name MatcherInfo := {}) - -instance : Inhabited State := ⟨{}⟩ - -def State.addEntry (s : State) (e : Entry) : State := { s with map := s.map.insert e.name e.info } -def State.switch (s : State) : State := { s with map := s.map.switch } - -builtin_initialize extension : SimplePersistentEnvExtension Entry State ← - registerSimplePersistentEnvExtension { - name := `matcher, - addEntryFn := State.addEntry, - addImportedFn := fun es => (mkStateFromImportedEntries State.addEntry {} es).switch - } - -def addMatcherInfo (env : Environment) (matcherName : Name) (info : MatcherInfo) : Environment := - extension.addEntry env { name := matcherName, info := info } - -def getMatcherInfo? (env : Environment) (declName : Name) : Option MatcherInfo := - (extension.getState env).map.find? declName - -end Extension - -def addMatcherInfo (matcherName : Name) (info : MatcherInfo) : MetaM Unit := - modifyEnv fun env => Extension.addMatcherInfo env matcherName info - private def getUElimPos? (matcherLevels : List Level) (uElim : Level) : MetaM (Option Nat) := if uElim == levelZero then pure none @@ -887,54 +838,6 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss : end Match -export Match (MatcherInfo) - -def getMatcherInfo? (declName : Name) : MetaM (Option MatcherInfo) := do - let env ← getEnv - pure $ Match.Extension.getMatcherInfo? env declName - -def isMatcher (declName : Name) : MetaM Bool := do - let info? ← getMatcherInfo? declName - pure info?.isSome - -structure MatcherApp := - (matcherName : Name) - (matcherLevels : Array Level) - (uElimPos? : Option Nat) - (params : Array Expr) - (motive : Expr) - (discrs : Array Expr) - (altNumParams : Array Nat) - (alts : Array Expr) - (remaining : Array Expr) - -def matchMatcherApp? (e : Expr) : MetaM (Option MatcherApp) := - match e.getAppFn with - | Expr.const declName declLevels _ => do - let some info ← getMatcherInfo? declName | pure none - let args := e.getAppArgs - if args.size < info.numParams + 1 + info.numDiscrs + info.numAlts then pure none - else - pure $ some { - matcherName := declName, - matcherLevels := declLevels.toArray, - uElimPos? := info.uElimPos?, - params := args.extract 0 info.numParams, - motive := args.get! info.numParams, - discrs := args.extract (info.numParams + 1) (info.numParams + 1 + info.numDiscrs), - altNumParams := info.altNumParams, - alts := args.extract (info.numParams + 1 + info.numDiscrs) (info.numParams + 1 + info.numDiscrs + info.numAlts), - remaining := args.extract (info.numParams + 1 + info.numDiscrs + info.numAlts) args.size - } - | _ => pure none - -def MatcherApp.toExpr (matcherApp : MatcherApp) : Expr := - let result := mkAppN (mkConst matcherApp.matcherName matcherApp.matcherLevels.toList) matcherApp.params - let result := mkApp result matcherApp.motive - let result := mkAppN result matcherApp.discrs - let result := mkAppN result matcherApp.alts - mkAppN result matcherApp.remaining - /- Auxiliary function for MatcherApp.addArg -/ private partial def updateAlts (typeNew : Expr) (altNumParams : Array Nat) (alts : Array Expr) (i : Nat) : MetaM (Array Nat × Array Expr) := do if h : i < alts.size then diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean new file mode 100644 index 0000000000..48bb230b7f --- /dev/null +++ b/src/Lean/Meta/Match/MatcherInfo.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +import Lean.Meta.Basic + +namespace Lean.Meta +namespace Match + +/-- +A "matcher" auxiliary declaration has the following structure: +- `numParams` parameters +- motive +- `numDiscrs` discriminators (aka major premises) +- `altNumParams.size` alternatives (aka minor premises) where alternative `i` has `altNumParams[i]` parameters +- `uElimPos?` is `some pos` when the matcher can eliminate in different universe levels, and + `pos` is the position of the universe level parameter that specifies the elimination universe. + It is `none` if the matcher only eliminates into `Prop`. -/ +structure MatcherInfo := + (numParams : Nat) + (numDiscrs : Nat) + (altNumParams : Array Nat) + (uElimPos? : Option Nat) + +def MatcherInfo.numAlts (matcherInfo : MatcherInfo) : Nat := + matcherInfo.altNumParams.size + +namespace Extension + +structure Entry := + (name : Name) + (info : MatcherInfo) + +structure State := + (map : SMap Name MatcherInfo := {}) + +instance : Inhabited State := ⟨{}⟩ + +def State.addEntry (s : State) (e : Entry) : State := { s with map := s.map.insert e.name e.info } +def State.switch (s : State) : State := { s with map := s.map.switch } + +builtin_initialize extension : SimplePersistentEnvExtension Entry State ← + registerSimplePersistentEnvExtension { + name := `matcher, + addEntryFn := State.addEntry, + addImportedFn := fun es => (mkStateFromImportedEntries State.addEntry {} es).switch + } + +def addMatcherInfo (env : Environment) (matcherName : Name) (info : MatcherInfo) : Environment := + extension.addEntry env { name := matcherName, info := info } + +def getMatcherInfo? (env : Environment) (declName : Name) : Option MatcherInfo := + (extension.getState env).map.find? declName + +end Extension + +def addMatcherInfo (matcherName : Name) (info : MatcherInfo) : MetaM Unit := + modifyEnv fun env => Extension.addMatcherInfo env matcherName info + +end Match + +export Match (MatcherInfo) + +def getMatcherInfo? (declName : Name) : MetaM (Option MatcherInfo) := do + let env ← getEnv + pure $ Match.Extension.getMatcherInfo? env declName + +def isMatcher (declName : Name) : MetaM Bool := do + let info? ← getMatcherInfo? declName + pure info?.isSome + +structure MatcherApp := + (matcherName : Name) + (matcherLevels : Array Level) + (uElimPos? : Option Nat) + (params : Array Expr) + (motive : Expr) + (discrs : Array Expr) + (altNumParams : Array Nat) + (alts : Array Expr) + (remaining : Array Expr) + +def matchMatcherApp? (e : Expr) : MetaM (Option MatcherApp) := + match e.getAppFn with + | Expr.const declName declLevels _ => do + let some info ← getMatcherInfo? declName | pure none + let args := e.getAppArgs + if args.size < info.numParams + 1 + info.numDiscrs + info.numAlts then pure none + else + pure $ some { + matcherName := declName, + matcherLevels := declLevels.toArray, + uElimPos? := info.uElimPos?, + params := args.extract 0 info.numParams, + motive := args.get! info.numParams, + discrs := args.extract (info.numParams + 1) (info.numParams + 1 + info.numDiscrs), + altNumParams := info.altNumParams, + alts := args.extract (info.numParams + 1 + info.numDiscrs) (info.numParams + 1 + info.numDiscrs + info.numAlts), + remaining := args.extract (info.numParams + 1 + info.numDiscrs + info.numAlts) args.size + } + | _ => pure none + +def MatcherApp.toExpr (matcherApp : MatcherApp) : Expr := + let result := mkAppN (mkConst matcherApp.matcherName matcherApp.matcherLevels.toList) matcherApp.params + let result := mkApp result matcherApp.motive + let result := mkAppN result matcherApp.discrs + let result := mkAppN result matcherApp.alts + mkAppN result matcherApp.remaining + +end Lean.Meta