80 lines
3.1 KiB
Text
80 lines
3.1 KiB
Text
/-
|
|
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.Elab.PreDefinition.Basic
|
|
import Lean.Elab.PreDefinition.Structural
|
|
import Lean.Elab.PreDefinition.WF
|
|
new_frontend
|
|
namespace Lean.Elab
|
|
open Meta
|
|
open Term
|
|
|
|
private def addAndCompilePartial (preDefs : Array PreDefinition) : TermElabM Unit := do
|
|
for preDef in preDefs do
|
|
trace[Elab.definition]! msg!"processing {preDef.declName}"
|
|
forallTelescope preDef.type fun xs type => do
|
|
let inh ← liftM $ mkInhabitantFor preDef.declName xs type
|
|
trace[Elab.definition]! msg!"inhabitant for {preDef.declName}"
|
|
addNonRec { preDef with
|
|
kind := DefKind.«opaque»,
|
|
value := inh }
|
|
addAndCompileUnsafeRec preDefs
|
|
|
|
private def isNonRecursive (preDef : PreDefinition) : Bool :=
|
|
Option.isNone $ preDef.value.find? fun
|
|
| Expr.const declName _ _ => preDef.declName == declName
|
|
| _ => false
|
|
|
|
private def partitionPreDefs (preDefs : Array PreDefinition) : Array (Array PreDefinition) :=
|
|
let getPreDef := fun declName => (preDefs.find? fun preDef => preDef.declName == declName).get!
|
|
let vertices := preDefs.toList.map (·.declName)
|
|
let successorsOf := fun declName => (getPreDef declName).value.foldConsts [] fun declName successors =>
|
|
if preDefs.any fun preDef => preDef.declName == declName then
|
|
declName :: successors
|
|
else
|
|
successors
|
|
let sccs := SCC.scc vertices successorsOf
|
|
sccs.toArray.map fun scc => scc.toArray.map getPreDef
|
|
|
|
private def collectMVarsAtPreDef (preDef : PreDefinition) : StateRefT CollectMVars.State MetaM Unit := do
|
|
collectMVars preDef.value
|
|
collectMVars preDef.type
|
|
|
|
private def getMVarsAtPreDef (preDef : PreDefinition) : MetaM (Array MVarId) := do
|
|
let (_, s) ← (collectMVarsAtPreDef preDef).run {}
|
|
pure s.result
|
|
|
|
private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM Unit := do
|
|
let pendingMVarIds ← liftMetaM $ getMVarsAtPreDef preDef
|
|
if ← logUnassignedUsingErrorInfos pendingMVarIds then
|
|
throwAbort
|
|
|
|
def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := do
|
|
for preDef in preDefs do
|
|
trace[Elab.definition.body]! msg!"{preDef.declName} : {preDef.type} :=\n{preDef.value}"
|
|
for preDef in preDefs do
|
|
ensureNoUnassignedMVarsAtPreDef preDef
|
|
for preDefs in partitionPreDefs preDefs do
|
|
trace[Elab.definition.scc]! "{preDefs.map (·.declName)}"
|
|
if preDefs.size == 1 && isNonRecursive preDefs[0] then
|
|
let preDef := preDefs[0]
|
|
if preDef.modifiers.isNoncomputable then
|
|
addNonRec preDef
|
|
else
|
|
addAndCompileNonRec preDef
|
|
else if preDefs.any (·.modifiers.isUnsafe) then
|
|
addAndCompileUnsafe preDefs
|
|
else if preDefs.any (·.modifiers.isPartial) then
|
|
addAndCompilePartial preDefs
|
|
else
|
|
mapError
|
|
(orelseMergeErrors
|
|
(structuralRecursion preDefs)
|
|
(WFRecursion preDefs))
|
|
(fun msg =>
|
|
let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
|
|
msg!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
|
|
|
|
end Lean.Elab
|