chore: move to new frontend
This commit is contained in:
Leonardo de Moura
parent
60091a49cd
commit
679187ae0a
1 changed files with 107 additions and 127 deletions
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -7,8 +8,7 @@ import Lean.AuxRecursor
|
|||
import Lean.Util.FindExpr
|
||||
import Lean.Meta.ExprDefEq
|
||||
|
||||
namespace Lean
|
||||
namespace Meta
|
||||
namespace Lean.Meta
|
||||
|
||||
def casesOnSuffix := "casesOn"
|
||||
def recOnSuffix := "recOn"
|
||||
|
|
@ -54,8 +54,8 @@ else if info.firstIndexPos ≤ pos && pos ≤ info.majorPos then false
|
|||
else true
|
||||
|
||||
def numMinors (info : RecursorInfo) : Nat :=
|
||||
let r := info.numArgs;
|
||||
let r := r - info.motivePos - 1;
|
||||
let r := info.numArgs
|
||||
let r := r - info.motivePos - 1
|
||||
r - (info.majorPos + 1 - info.firstIndexPos)
|
||||
|
||||
instance : HasToString RecursorInfo :=
|
||||
|
|
@ -80,14 +80,14 @@ instance : HasToString RecursorInfo :=
|
|||
end RecursorInfo
|
||||
|
||||
private def mkRecursorInfoForKernelRec (declName : Name) (val : RecursorVal) : MetaM RecursorInfo := do
|
||||
ival ← getConstInfoInduct val.getInduct;
|
||||
let numLParams := ival.lparams.length;
|
||||
let univLevelPos := (List.range numLParams).map RecursorUnivLevelPos.majorType;
|
||||
let univLevelPos := if val.lparams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos;
|
||||
let produceMotive := List.replicate val.nminors true;
|
||||
let paramsPos := (List.range val.nparams).map some;
|
||||
let indicesPos := (List.range val.nindices).map (fun pos => val.nparams + pos);
|
||||
let numArgs := val.nindices + val.nparams + val.nminors + val.nmotives + 1;
|
||||
let ival ← getConstInfoInduct val.getInduct
|
||||
let numLParams := ival.lparams.length
|
||||
let univLevelPos := (List.range numLParams).map RecursorUnivLevelPos.majorType
|
||||
let univLevelPos := if val.lparams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos
|
||||
let produceMotive := List.replicate val.nminors true
|
||||
let paramsPos := (List.range val.nparams).map some
|
||||
let indicesPos := (List.range val.nindices).map fun pos => val.nparams + pos
|
||||
let numArgs := val.nindices + val.nparams + val.nminors + val.nmotives + 1
|
||||
pure {
|
||||
recursorName := declName,
|
||||
typeName := val.getInduct,
|
||||
|
|
@ -105,30 +105,29 @@ pure {
|
|||
private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat) : MetaM (Option Nat) :=
|
||||
if majorPos?.isSome then pure majorPos?
|
||||
else do
|
||||
env ← getEnv;
|
||||
let env ← getEnv
|
||||
if !isAuxRecursor env declName then pure none
|
||||
else match declName with
|
||||
| Name.str p s _ =>
|
||||
if s != recOnSuffix && s != casesOnSuffix && s != brecOnSuffix then
|
||||
pure none
|
||||
else do
|
||||
val ← getConstInfoRec (mkRecFor p);
|
||||
let val ← getConstInfoRec (mkRecFor p)
|
||||
pure $ some (val.nparams + val.nindices + (if s == casesOnSuffix then 1 else val.nmotives))
|
||||
| _ => pure none
|
||||
|
||||
private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Expr) : MetaM Unit :=
|
||||
unless (motive.isFVar && motiveArgs.all Expr.isFVar) $ throwError
|
||||
("invalid user defined recursor '" ++ toString declName ++ "', result type must be of the form (C t), " ++
|
||||
"where C is a bound variable, and t is a (possibly empty) sequence of bound variables")
|
||||
private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Expr) : MetaM Unit := do
|
||||
unless motive.isFVar && motiveArgs.all Expr.isFVar do
|
||||
throwError! "invalid user defined recursor '{declName}', result type must be of the form (C t), where C is a bound variable, and t is a (possibly empty) sequence of bound variables"
|
||||
|
||||
/- Compute number of parameters for (user-defined) recursor.
|
||||
We assume a parameter is anything that occurs before the motive -/
|
||||
private partial def getNumParams (xs : Array Expr) (motive : Expr) : Nat → Nat
|
||||
| i =>
|
||||
if h : i < xs.size then
|
||||
let x := xs.get ⟨i, h⟩;
|
||||
let x := xs.get ⟨i, h⟩
|
||||
if motive == x then i
|
||||
else getNumParams (i+1)
|
||||
else getNumParams xs motive (i+1)
|
||||
else
|
||||
i
|
||||
|
||||
|
|
@ -137,121 +136,107 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
|
|||
match majorPos? with
|
||||
| some majorPos =>
|
||||
if h : majorPos < xs.size then
|
||||
let major := xs.get ⟨majorPos, h⟩;
|
||||
let depElim := motiveArgs.contains major;
|
||||
let major := xs.get ⟨majorPos, h⟩
|
||||
let depElim := motiveArgs.contains major
|
||||
pure (major, majorPos, depElim)
|
||||
else throwError
|
||||
("invalid major premise position for user defined recursor, recursor has only " ++ toString xs.size ++ " arguments")
|
||||
else throwError! "invalid major premise position for user defined recursor, recursor has only {xs.size} arguments"
|
||||
| none => do
|
||||
when motiveArgs.isEmpty $ throwError
|
||||
("invalid user defined recursor, '" ++ toString declName ++ "' does not support dependent elimination, " ++
|
||||
"and position of the major premise was not specified " ++
|
||||
"(solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)");
|
||||
let major := motiveArgs.back;
|
||||
if motiveArgs.isEmpty then
|
||||
throwError! "invalid user defined recursor, '{declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)"
|
||||
let major := motiveArgs.back
|
||||
match xs.getIdx? major with
|
||||
| some majorPos => pure (major, majorPos, true)
|
||||
| none => throwError ("ill-formed recursor '" ++ toString declName ++ "'")
|
||||
| none => throwError! "ill-formed recursor '{declName}'"
|
||||
|
||||
private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) (Iargs : Array Expr) : MetaM (List (Option Nat)) := do
|
||||
paramsPos ← numParams.foldM
|
||||
(fun i (paramsPos : Array (Option Nat)) => do
|
||||
let x := xs.get! i;
|
||||
j? ← Iargs.findIdxM? $ fun Iarg => isDefEq Iarg x;
|
||||
match j? with
|
||||
| some j => pure $ paramsPos.push (some j)
|
||||
| none => do
|
||||
localDecl ← getLocalDecl x.fvarId!;
|
||||
if localDecl.binderInfo.isInstImplicit then
|
||||
pure $ paramsPos.push none
|
||||
else
|
||||
throwError
|
||||
("invalid user defined recursor '" ++ toString declName ++ "' , type of the major premise does not contain the recursor parameter"))
|
||||
#[];
|
||||
let paramsPos := #[]
|
||||
for i in [:numParams] do
|
||||
let x := xs[i]
|
||||
match (← Iargs.findIdxM? fun Iarg => isDefEq Iarg x) with
|
||||
| some j => paramsPos := paramsPos.push (some j)
|
||||
| none => do
|
||||
let localDecl ← getLocalDecl x.fvarId!
|
||||
if localDecl.binderInfo.isInstImplicit then
|
||||
paramsPos := paramsPos.push none
|
||||
else
|
||||
throwError!"invalid user defined recursor '{declName}', type of the major premise does not contain the recursor parameter"
|
||||
pure paramsPos.toList
|
||||
|
||||
private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndices : Nat) (Iargs : Array Expr) : MetaM (List Nat) := do
|
||||
indicesPos ← numIndices.foldM
|
||||
(fun i (indicesPos : Array Nat) => do
|
||||
let i := majorPos - numIndices + i;
|
||||
let x := xs.get! i;
|
||||
-- trace! `Meta ("getIndicesPos " ++ toString i ++ ": " ++ x);
|
||||
j? ← Iargs.findIdxM? $ fun Iarg => isDefEq Iarg x;
|
||||
match j? with
|
||||
| some j => pure $ indicesPos.push j
|
||||
| none => throwError
|
||||
("invalid user defined recursor '" ++ toString declName ++ "' , type of the major premise does not contain the recursor index"))
|
||||
#[];
|
||||
let indicesPos := #[]
|
||||
for i in [:numIndices] do
|
||||
let i := majorPos - numIndices + i
|
||||
let x := xs[i]
|
||||
match (← Iargs.findIdxM? fun Iarg => isDefEq Iarg x) with
|
||||
| some j => indicesPos := indicesPos.push j
|
||||
| none => throwError! "invalid user defined recursor '{declName}', type of the major premise does not contain the recursor index"
|
||||
pure indicesPos.toList
|
||||
|
||||
private def getMotiveLevel (declName : Name) (motiveResultType : Expr) : MetaM Level :=
|
||||
match motiveResultType with
|
||||
| Expr.sort u@(Level.zero _) _ => pure u
|
||||
| Expr.sort u@(Level.param _ _) _ => pure u
|
||||
| _ => throwError
|
||||
("invalid user defined recursor '" ++ toString declName ++ "' , motive result sort must be Prop or (Sort u) where u is a universe level parameter")
|
||||
| _ =>
|
||||
throwError! "invalid user defined recursor '{declName}', motive result sort must be Prop or (Sort u) where u is a universe level parameter"
|
||||
|
||||
private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl : Level) (Ilevels : List Level) : MetaM (List RecursorUnivLevelPos) := do
|
||||
let Ilevels := Ilevels.toArray;
|
||||
univLevelPos ← lparams.foldlM
|
||||
(fun (univLevelPos : Array RecursorUnivLevelPos) p =>
|
||||
if motiveLvl == mkLevelParam p then
|
||||
pure $ univLevelPos.push RecursorUnivLevelPos.motive
|
||||
else
|
||||
match Ilevels.findIdx? $ fun u => u == mkLevelParam p with
|
||||
| some i => pure $ univLevelPos.push $ RecursorUnivLevelPos.majorType i
|
||||
| none => throwError
|
||||
("invalid user defined recursor '" ++ toString declName ++ "' , major premise type does not contain universe level parameter '" ++ toString p ++ "'"))
|
||||
#[];
|
||||
let Ilevels := Ilevels.toArray
|
||||
let univLevelPos := #[]
|
||||
for p in lparams do
|
||||
if motiveLvl == mkLevelParam p then
|
||||
univLevelPos := univLevelPos.push RecursorUnivLevelPos.motive
|
||||
else
|
||||
match Ilevels.findIdx? fun u => u == mkLevelParam p with
|
||||
| some i => univLevelPos := univLevelPos.push (RecursorUnivLevelPos.majorType i)
|
||||
| none =>
|
||||
throwError! "invalid user defined recursor '{declName}', major premise type does not contain universe level parameter '{p}'"
|
||||
pure univLevelPos.toList
|
||||
|
||||
private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices majorPos : Nat) (motive : Expr) : MetaM (List Bool × Bool) := do
|
||||
(produceMotive, rec) ← xs.size.foldM
|
||||
(fun i (p : Array Bool × Bool) =>
|
||||
if i < numParams + 1 then pure p -- skip parameters and motive
|
||||
else if majorPos - numIndices ≤ i && i ≤ majorPos then pure p -- skip indices and major premise
|
||||
else do -- process minor premise
|
||||
let (produceMotive, rec) := p;
|
||||
let x := xs.get! i;
|
||||
xType ← inferType x;
|
||||
forallTelescopeReducing xType $ fun minorArgs minorResultType => minorResultType.withApp $ fun res _ => do
|
||||
-- trace! `Meta ("xType: " ++ xType ++ ", motive: " ++ motive ++ ", " ++ minorArgs ++ ", " ++ res);
|
||||
let produceMotive := produceMotive.push (res == motive);
|
||||
rec ← if rec then pure rec else minorArgs.anyM $ fun minorArg => do {
|
||||
minorArgType ← inferType minorArg;
|
||||
pure $ (minorArgType.find? $ fun e => e == motive).isSome
|
||||
};
|
||||
pure (produceMotive, rec))
|
||||
(#[], false);
|
||||
pure (produceMotive.toList, rec)
|
||||
let produceMotive := #[]
|
||||
let recursor := false
|
||||
for i in [:xs.size] do
|
||||
if i < numParams + 1 then
|
||||
continue --skip parameters and motive
|
||||
if majorPos - numIndices ≤ i && i ≤ majorPos then
|
||||
continue -- skip indices and major premise
|
||||
-- process minor premise
|
||||
let x := xs[i]
|
||||
let xType ← inferType x
|
||||
(produceMotive, recursor) ← forallTelescopeReducing xType fun minorArgs minorResultType => minorResultType.withApp fun res _ => do
|
||||
let produceMotive := produceMotive.push (res == motive)
|
||||
let recursor ← if recursor then pure recursor else minorArgs.anyM fun minorArg => do
|
||||
let minorArgType ← inferType minorArg
|
||||
pure (minorArgType.find? fun e => e == motive).isSome
|
||||
pure (produceMotive, recursor)
|
||||
pure (produceMotive.toList, recursor)
|
||||
|
||||
private def checkMotiveResultType (declName : Name) (motiveArgs : Array Expr) (motiveResultType : Expr) (motiveTypeParams : Array Expr) : MetaM Unit :=
|
||||
when (!motiveResultType.isSort || motiveArgs.size != motiveTypeParams.size) $ throwError
|
||||
("invalid user defined recursor '" ++ toString declName ++ "', motive must have a type of the form "
|
||||
++ "(C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), "
|
||||
++ "(i : B A) is a (possibly empty) telescope (aka indices), and I is a constant")
|
||||
private def checkMotiveResultType (declName : Name) (motiveArgs : Array Expr) (motiveResultType : Expr) (motiveTypeParams : Array Expr) : MetaM Unit := do
|
||||
if !motiveResultType.isSort || motiveArgs.size != motiveTypeParams.size then
|
||||
throwError! "invalid user defined recursor '{declName}', motive must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant"
|
||||
|
||||
private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) : MetaM RecursorInfo := do
|
||||
let declName := cinfo.name;
|
||||
majorPos? ← getMajorPosIfAuxRecursor? declName majorPos?;
|
||||
forallTelescopeReducing cinfo.type $ fun xs type => type.withApp $ fun motive motiveArgs => do
|
||||
checkMotive declName motive motiveArgs;
|
||||
let numParams := getNumParams xs motive 0;
|
||||
(major, majorPos, depElim) ← getMajorPosDepElim declName majorPos? xs motive motiveArgs;
|
||||
let numIndices := if depElim then motiveArgs.size - 1 else motiveArgs.size;
|
||||
when (majorPos < numIndices) $ throwError
|
||||
("invalid user defined recursor '" ++ toString declName ++ "', indices must occur before major premise");
|
||||
majorType ← inferType major;
|
||||
majorType.withApp $ fun I Iargs =>
|
||||
let declName := cinfo.name
|
||||
let majorPos? ← getMajorPosIfAuxRecursor? declName majorPos?
|
||||
forallTelescopeReducing cinfo.type fun xs type => type.withApp fun motive motiveArgs => do
|
||||
checkMotive declName motive motiveArgs
|
||||
let numParams := getNumParams xs motive 0
|
||||
let (major, majorPos, depElim) ← getMajorPosDepElim declName majorPos? xs motive motiveArgs
|
||||
let numIndices := if depElim then motiveArgs.size - 1 else motiveArgs.size
|
||||
if majorPos < numIndices then
|
||||
throwError! "invalid user defined recursor '{declName}', indices must occur before major premise"
|
||||
let majorType ← inferType major
|
||||
majorType.withApp fun I Iargs =>
|
||||
match I with
|
||||
| Expr.const Iname Ilevels _ => do
|
||||
paramsPos ← getParamsPos declName xs numParams Iargs;
|
||||
indicesPos ← getIndicesPos declName xs majorPos numIndices Iargs;
|
||||
motiveType ← inferType motive;
|
||||
forallTelescopeReducing motiveType $ fun motiveTypeParams motiveResultType => do
|
||||
checkMotiveResultType declName motiveArgs motiveResultType motiveTypeParams;
|
||||
motiveLvl ← getMotiveLevel declName motiveResultType;
|
||||
univLevelPos ← getUnivLevelPos declName cinfo.lparams motiveLvl Ilevels;
|
||||
(produceMotive, recursive) ← getProduceMotiveAndRecursive xs numParams numIndices majorPos motive;
|
||||
let paramsPos ← getParamsPos declName xs numParams Iargs
|
||||
let indicesPos ← getIndicesPos declName xs majorPos numIndices Iargs
|
||||
let motiveType ← inferType motive
|
||||
forallTelescopeReducing motiveType fun motiveTypeParams motiveResultType => do
|
||||
checkMotiveResultType declName motiveArgs motiveResultType motiveTypeParams
|
||||
let motiveLvl ← getMotiveLevel declName motiveResultType
|
||||
let univLevelPos ← getUnivLevelPos declName cinfo.lparams motiveLvl Ilevels
|
||||
let (produceMotive, recursive) ← getProduceMotiveAndRecursive xs numParams numIndices majorPos motive
|
||||
pure {
|
||||
recursorName := declName,
|
||||
typeName := Iname,
|
||||
|
|
@ -264,15 +249,13 @@ forallTelescopeReducing cinfo.type $ fun xs type => type.withApp $ fun motive mo
|
|||
indicesPos := indicesPos,
|
||||
numArgs := xs.size
|
||||
}
|
||||
| _ => throwError
|
||||
("invalid user defined recursor '" ++ toString declName
|
||||
++ "', type of the major premise must be of the form (I ...), where I is a constant")
|
||||
| _ => throwError! "invalid user defined recursor '{declName}', type of the major premise must be of the form (I ...), where I is a constant"
|
||||
|
||||
private def syntaxToMajorPos (stx : Syntax) : Except String Nat :=
|
||||
match stx with
|
||||
| Syntax.node _ args =>
|
||||
if args.size == 0 then Except.error "unexpected kind of argument"
|
||||
else match (args.get! 0).isNatLit? with
|
||||
else match args[0].isNatLit? with
|
||||
| some idx =>
|
||||
if idx == 0 then Except.error "major premise position must be greater than 0"
|
||||
else pure (idx - 1)
|
||||
|
|
@ -280,30 +263,27 @@ match stx with
|
|||
| _ => Except.error "unexpected kind of argument"
|
||||
|
||||
private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
|
||||
cinfo ← getConstInfo declName;
|
||||
let cinfo ← getConstInfo declName
|
||||
match cinfo with
|
||||
| ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
|
||||
| _ => mkRecursorInfoAux cinfo majorPos?
|
||||
|
||||
def mkRecursorAttr : IO (ParametricAttribute Nat) :=
|
||||
registerParametricAttribute `recursor "user defined recursor, numerical parameter specifies position of the major premise"
|
||||
(fun _ stx => ofExcept $ syntaxToMajorPos stx)
|
||||
(fun declName majorPos => do
|
||||
liftM $ (mkRecursorInfoCore declName (some majorPos)).run';
|
||||
pure ())
|
||||
|
||||
@[init mkRecursorAttr] constant recursorAttribute : ParametricAttribute Nat := arbitrary _
|
||||
initialize recursorAttribute : ParametricAttribute Nat ←
|
||||
registerParametricAttribute `recursor "user defined recursor, numerical parameter specifies position of the major premise"
|
||||
(fun _ stx => ofExcept $ syntaxToMajorPos stx)
|
||||
(fun declName majorPos => do
|
||||
(mkRecursorInfoCore declName (some majorPos)).run'
|
||||
pure ())
|
||||
|
||||
def getMajorPos? (env : Environment) (declName : Name) : Option Nat :=
|
||||
recursorAttribute.getParam env declName
|
||||
|
||||
def mkRecursorInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
|
||||
cinfo ← getConstInfo declName;
|
||||
let cinfo ← getConstInfo declName
|
||||
match cinfo with
|
||||
| ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
|
||||
| _ => match majorPos? with
|
||||
| none => do env ← getEnv; mkRecursorInfoAux cinfo (getMajorPos? env declName)
|
||||
| none => do mkRecursorInfoAux cinfo (getMajorPos? (← getEnv) declName)
|
||||
| _ => mkRecursorInfoAux cinfo majorPos?
|
||||
|
||||
end Meta
|
||||
end Lean
|
||||
end Lean.Meta
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue