From 679187ae0a4e291afc0d74372a698fa1278bb35c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Oct 2020 09:11:16 -0700 Subject: [PATCH] chore: move to new frontend --- src/Lean/Meta/RecursorInfo.lean | 234 +++++++++++++++----------------- 1 file changed, 107 insertions(+), 127 deletions(-) diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index 2704e4c306..09fa5d72e9 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -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 ]', where 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 ]', where 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