feat: add addAndCompilePartial

src/Lean/Elab.lean

@@ -23,3 +23,6 @@ import Lean.Elab.StructInst
 import Lean.Elab.Inductive
 import Lean.Elab.Structure
 import Lean.Elab.Print
+import Lean.Elab.MutualDef
+import Lean.Elab.PreDefinition
+import Lean.Elab.MkInhabitant

src/Lean/Elab/MkInhabitant.lean

@@ -3,28 +3,11 @@ 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.Util.ReplaceExpr
-import Lean.Compiler.ImplementedByAttr
 import Lean.Meta.AppBuilder
-import Lean.Meta.Basic
 
 namespace Lean
-namespace Meta
-
-private def mkUnsafeNameFor (n : Name) := n ++ `_unsafe
-
-private def addUnsafeDecls (ds : List DefinitionVal) : MetaM Unit := do
-let ds := ds.map fun d =>
-  { d with
-    name  := mkUnsafeNameFor d.name,
-    value := d.value.replace fun e => match e with
-      | Expr.const constName us _ =>
-        if ds.any fun d => d.name == constName then
-          some $ mkConst (mkUnsafeNameFor constName) us
-        else
-          none
-      | _ => none };
-addAndCompile (Declaration.mutualDefnDecl ds)
+namespace Elab
+open Meta
 
 private def mkInhabitant? (type : Expr) : MetaM (Option Expr) :=
 catch
@@ -52,7 +35,9 @@ private def mkFnInhabitantAux? (xs : Array Expr) : Nat → Expr → MetaM (Optio
 private def mkFnInhabitant? (xs : Array Expr) (type : Expr) : MetaM (Option Expr) :=
 mkFnInhabitantAux? xs xs.size type
 
-private def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr := do
+/- TODO: add a global IO.Ref to let users customize/extend this procedure -/
+
+def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr := do
 val? ← mkInhabitant? type;
 match val? with
 | some val => mkLambdaFVars xs val
@@ -66,16 +51,5 @@ match x? with
 | some val => pure val
 | none => throwError ("failed to compile partial definition '" ++ declName ++ "', failed to show that type is inhabited")
 
-private def addOpaqueConstants (ds : List DefinitionVal) : MetaM Unit := do
-ds.forM fun d =>
-  forallTelescopeReducing d.type fun xs type => do
-    inh ← mkInhabitantFor d.name xs type;
-    addAndCompile $ Declaration.opaqueDecl { name := d.name, lparams := d.lparams, type := d.type, value := inh, isUnsafe := false };
-    setImplementedBy d.name (mkUnsafeNameFor d.name)
-
-def addPartialDecls (ds : List DefinitionVal) : MetaM Unit := do
-addUnsafeDecls ds;
-addOpaqueConstants ds
-
-end Meta
+end Elab
 end Lean

src/Lean/Elab/PreDefinition.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Util.SCC
+import Lean.Elab.MkInhabitant
 import Lean.Elab.Term
 import Lean.Elab.DefView
 
@@ -87,7 +88,7 @@ pure $ preDefs.map fun preDef =>
 private def applyAttributesOf (preDefs : Array PreDefinition) (applicationTime : AttributeApplicationTime) : TermElabM Unit := do
 preDefs.forM fun preDef => applyAttributes preDef.declName preDef.modifiers.attrs applicationTime
 
-private def addAndCompileNonRec (preDef : PreDefinition) : TermElabM Unit := do
+private def addNonRecAux (preDef : PreDefinition) (compile : Bool) : TermElabM Unit := do
 env ← getEnv;
 let decl :=
   match preDef.kind with
@@ -107,11 +108,18 @@ let decl :=
 ensureNoUnassignedMVars decl;
 addDecl decl;
 applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking;
-compileDecl decl;
+when compile $
+  compileDecl decl;
 applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation;
 pure ()
 
-private def addAndCompileAsUnsafe (preDefs : Array PreDefinition) : TermElabM Unit := do
+private def addAndCompileNonRec (preDef : PreDefinition) : TermElabM Unit := do
+addNonRecAux preDef true
+
+private def addNonRec (preDef : PreDefinition) : TermElabM Unit := do
+addNonRecAux preDef false
+
+private def addAndCompileUnsafe (preDefs : Array PreDefinition) : TermElabM Unit := do
 let decl := Declaration.mutualDefnDecl $ preDefs.toList.map fun preDef => {
     name     := preDef.declName,
     lparams  := preDef.lparams,
@@ -127,6 +135,28 @@ compileDecl decl;
 applyAttributesOf preDefs AttributeApplicationTime.afterCompilation;
 pure ()
 
+private def addAndCompileUnsafeRec (preDefs : Array PreDefinition) : TermElabM Unit := do
+addAndCompileUnsafe $ preDefs.map fun preDef =>
+  { preDef with
+    declName  := Compiler.mkUnsafeRecName preDef.declName,
+    value     := preDef.value.replace fun e => match e with
+      | Expr.const declName us _ =>
+        if preDefs.any fun preDef => preDef.declName == declName then
+          some $ mkConst (Compiler.mkUnsafeRecName declName) us
+        else
+          none
+      | _ => none,
+    modifiers := {} }
+
+private def addAndCompilePartial (preDefs : Array PreDefinition) : TermElabM Unit := do
+preDefs.forM fun preDef =>
+  forallTelescopeReducing preDef.type fun xs type => do
+    inh ← liftM $ mkInhabitantFor preDef.declName xs type;
+    addNonRec { preDef with
+      kind  := DefKind.«opaque»,
+      value := inh };
+addAndCompileUnsafeRec preDefs
+
 private def isNonRecursive (preDef : PreDefinition) : Bool :=
 Option.isNone $ preDef.value.find? fun c => match c with
   | Expr.const declName _ _ => preDef.declName == declName
@@ -148,10 +178,13 @@ preDefs.forM fun preDef => trace `Elab.definition.body fun _ => preDef.declName
 (partitionPreDefs preDefs).forM fun preDefs => do
   if preDefs.size == 1 && isNonRecursive (preDefs.get! 0) then
     addAndCompileNonRec (preDefs.get! 0)
-  else do
-    trace `Elab.definition.scc fun _ => toString $ preDefs.map fun preDef => preDef.declName;
+  else if preDefs.any fun preDef => preDef.modifiers.isUnsafe then
+    addAndCompileUnsafe preDefs
+  else if preDefs.any fun preDef => preDef.modifiers.isPartial then
+    addAndCompilePartial preDefs
+  else
     -- TODO
-    addAndCompileAsUnsafe preDefs
+    throwError "WIP"
 
 end Elab
 end Lean

src/Lean/Meta.lean

@@ -21,5 +21,4 @@ import Lean.Meta.RecursorInfo
 import Lean.Meta.GeneralizeTelescope
 import Lean.Meta.EqnCompiler
 import Lean.Meta.ReduceEval
-import Lean.Meta.Partial
 import Lean.Meta.Closure

tests/lean/run/partial1.lean

@@ -0,0 +1,13 @@
+new_frontend
+
+partial def reverse {α} (as : List α) : List α :=
+let rec loop : List α → List α → List α
+  | [],    r => r
+  | a::as, r => loop as (a::r);
+loop as []
+
+#eval reverse [3, 2, 1]
+#eval reverse [1, 2, 3, 4]
+#print reverse
+#print reverse.loop
+#print reverse.loop._unsafe_rec

tests/lean/run/typeclass_diamond.lean

@@ -33,5 +33,8 @@ set_option ppOld false
 
 #synth Top Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ
 
+#exit
+
+-- TODO: we should not consider the auxiliary local `tst : ...`
 def tst : Top Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ :=
 inferInstance