From 25bcc95b13244cd26154ff04b565f6b9d386408f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Sep 2020 14:39:22 -0700 Subject: [PATCH] feat: construct `brecOn` application TODO: replace recursive application with `below` argument --- src/Lean/Elab/PreDefinition/Structural.lean | 70 ++++++++++++++++++--- 1 file changed, 60 insertions(+), 10 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean index 7bdc2cdb2c..ca61d3037e 100644 --- a/src/Lean/Elab/PreDefinition/Structural.lean +++ b/src/Lean/Elab/PreDefinition/Structural.lean @@ -26,10 +26,14 @@ runST fun _ => do (_, numFixed) ← visitor.run xs.size; pure numFixed structure RecArgInfo := /- `fixedParams ++ ys` are the arguments of the function we are trying to justify termination using structural recursion. -/ (fixedParams : Array Expr) -(ys : Array Expr) -- recursion arguments -(pos : Nat) -- position in `ys` of the argument we are recursing on -(indicesPos : Array Nat) -- position in `ys` of the inductive datatype indices we are recursing on -(reflexive : Bool) -- true if we are recursing over a reflexive inductive datatype +(ys : Array Expr) -- recursion arguments +(pos : Nat) -- position in `ys` of the argument we are recursing on +(indicesPos : Array Nat) -- position in `ys` of the inductive datatype indices we are recursing on +(indName : Name) -- inductive datatype name of the argument we are recursing on +(indLevels : List Level) -- inductice datatype universe levels of the argument we are recursing on +(indParams : Array Expr) -- inductive datatype parameters of the argument we are recursing on +(indIndices : Array Expr) -- inductive datatype indices of the argument we are recursing on, it is equal to `indicesPos.map fun i => ys.get! i` +(reflexive : Bool) -- true if we are recursing over a reflexive inductive datatype private def getIndexMinPos (xs : Array Expr) (indices : Array Expr) : Nat := indices.foldl @@ -103,7 +107,13 @@ private partial def findRecArgAux? {α} (numFixed : Nat) (xs : Array Expr) (k? : findRecArgAux? (i+1) | none => do let indicesPos := indIndices.map fun index => match ys.indexOf index with | some i => i.val | none => unreachable!; - a? ← k? { fixedParams := fixedParams, ys := ys, pos := i - fixedParams.size, indicesPos := indicesPos, reflexive := indInfo.isReflexive }; + a? ← k? { fixedParams := fixedParams, ys := ys, pos := i - fixedParams.size, + indicesPos := indicesPos, + indName := indInfo.name, + indLevels := us, + indParams := indParams, + indIndices := indIndices, + reflexive := indInfo.isReflexive }; match a? with | some a => pure a | none => findRecArgAux? (i+1) @@ -113,15 +123,55 @@ private partial def findRecArgAux? {α} (numFixed : Nat) (xs : Array Expr) (k? : @[inline] private def findRecArg? {α} (numFixed : Nat) (xs : Array Expr) (k? : RecArgInfo → TermElabM (Option α)) : TermElabM (Option α) := findRecArgAux? numFixed xs k? numFixed +private def replaceRecApps? (argInfo : RecArgInfo) (below : Expr) (value : Expr) : TermElabM (Option Expr) := +-- TODO +pure value + +private def mkBRecOn? (argInfo : RecArgInfo) (value : Expr) : TermElabM (Option Expr) := do +type ← inferType value; +let type := type.headBeta; +let major := argInfo.ys.get! argInfo.pos; +let otherArgs := argInfo.ys.filter fun y => y != major && !argInfo.indIndices.contains y; +motive ← mkForallFVars otherArgs type; +brecOnUniv ← getDecLevel motive; +motive ← mkLambdaFVars (argInfo.indIndices.push major) motive; +trace `Elab.definition.structural fun _ => "brecOn motive: " ++ motive; +let brecOn := Lean.mkConst (mkBRecOnFor argInfo.indName) (brecOnUniv :: argInfo.indLevels); +let brecOn := mkAppN brecOn argInfo.indParams; +let brecOn := mkApp brecOn motive; +let brecOn := mkAppN brecOn argInfo.indIndices; +let brecOn := mkApp brecOn major; +brecOnType ← inferType brecOn; +trace `Elab.definition.structural fun _ => "brecOn " ++ brecOn; +trace `Elab.definition.structural fun _ => "brecOnType " ++ brecOnType; +forallBoundedTelescope brecOnType (some 1) fun F _ => do + let F := F.get! 0; + FType ← inferType F; + let numIndices := argInfo.indIndices.size; + forallBoundedTelescope FType (some $ numIndices + 1 /- major -/ + 1 /- below -/) fun Fargs _ => do + let indicesNew := Fargs.extract 0 numIndices; + let majorNew := Fargs.get! numIndices; + let below := Fargs.get! (numIndices+1); + let valueNew := value.replaceFVars argInfo.indIndices indicesNew; + let valueNew := valueNew.replaceFVar major majorNew; + valueNew? ← replaceRecApps? argInfo below valueNew; + match valueNew? with + | none => pure none + | some valueNew => do + Farg ← mkLambdaFVars Fargs valueNew; + let brecOn := mkApp brecOn Farg; + pure $ mkAppN brecOn otherArgs + private def elimRecursion? (preDef : PreDefinition) : TermElabM (Option PreDefinition) := -lambdaLetTelescope preDef.value fun xs value => do +lambdaTelescope preDef.value fun xs value => do trace `Elab.definition.structural fun _ => preDef.declName ++ " " ++ xs ++ " :=\n" ++ value; let numFixed := getFixedPrefix preDef.declName xs value; findRecArg? numFixed xs fun argInfo => do - -- TODO - trace `Elab.definition.structural fun _ => - "try " ++ argInfo.fixedParams ++ " " ++ argInfo.ys ++ " " ++ toString argInfo.pos ++ ", " ++ toString argInfo.indicesPos; - pure none + some valueNew ← mkBRecOn? argInfo value | pure none; + valueNew ← mkLambdaFVars xs valueNew; + trace `Elab.definition.structural fun _ => "result: " ++ valueNew; + -- pure $ some { preDef with value := valueNew } + throwError "WIP" def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Bool := if preDefs.size != 1 then