diff --git a/src/Lean/Compiler/LCNF.lean b/src/Lean/Compiler/LCNF.lean index 61168d6189..7b8a7d070c 100644 --- a/src/Lean/Compiler/LCNF.lean +++ b/src/Lean/Compiler/LCNF.lean @@ -12,8 +12,6 @@ import Lean.Compiler.InlineAttrs import Lean.Compiler.InferType import Lean.Compiler.Util --- TODO: port file to the new LCNF format - namespace Lean.Compiler /-! # Lean Compiler Normal Form (LCNF) @@ -225,11 +223,8 @@ where etaIfUnderApplied e arity do visitAppDefault e.getAppFn e.getAppArgs --- TODO: stopped here - visitQuotLift (e : Expr) : M Expr := do - throwError "wip {e}" -/- let arity := 6 + let arity := 6 etaIfUnderApplied e arity do let mut args := e.getAppArgs let α := args[0]! @@ -237,56 +232,53 @@ where let f ← visitChild args[3]! let q ← visitChild args[5]! let .const _ [u, _] := e.getAppFn | unreachable! - let invq ← mkAuxLetDecl (mkApp3 (.const ``Quot.lcInv [u]) α r q) + let invq ← withRoot false <| mkAuxLetDecl (mkApp3 (.const ``Quot.lcInv [u]) α r q) let r := mkApp f invq mkOverApplication r args arity --/ visitEqRec (e : Expr) : M Expr := - throwError "wip {e}" -/- let arity := 6 etaIfUnderApplied e arity do let args := e.getAppArgs let f := e.getAppFn - let type ← inferType (mkAppN f args[:arity]) + let recType ← liftMetaM do toLCNFType (← Meta.inferType (mkAppN f args[:arity])) let minor := if e.isAppOf ``Eq.rec || e.isAppOf ``Eq.ndrec then args[3]! else args[5]! - let cast ← mkLcCast (← visitChild minor) type + let minor ← visit minor + let minorType ← inferType minor + let cast ← if compatibleTypes minorType recType then + -- Recall that many types become compatible after LCNF conversion + -- Example: `Fin 10` and `Fin n` + pure minor + else + mkLcCast (← withRoot false <| mkAuxLetDecl minor) recType mkOverApplication cast args arity --/ visitFalseRec (e : Expr) : M Expr := - throwError "wip {e}" -/- let arity := 2 etaIfUnderApplied e arity do - mkAuxLetDecl (← mkLcUnreachable (← inferType e)) --/ + let type ← liftMetaM do toLCNFType (← Meta.inferType e) + mkAuxLetDecl (← mkLcUnreachable type) visitAndRec (e : Expr) : M Expr := - throwError "wip {e}" -/- let arity := 5 etaIfUnderApplied e arity do let args := e.getAppArgs - let ha := mkLcProof args[0]! + let ha := mkLcProof args[0]! -- We should not use `lcErased` here since we use it to create a pre-LCNF Expr. let hb := mkLcProof args[1]! let minor := if e.isAppOf ``And.rec then args[3]! else args[4]! let minor := minor.beta #[ha, hb] + trace[Meta.debug] "minor: {minor}" visit (mkAppN minor args[arity:]) --/ visitNoConfusion (e : Expr) : M Expr := do - throwError "wip {e}" -/- let .const declName _ := e.getAppFn | unreachable! let typeName := declName.getPrefix let .inductInfo inductVal ← getConstInfo typeName | unreachable! let arity := inductVal.numParams + inductVal.numIndices + 1 /- motive -/ + 2 /- lhs/rhs-/ + 1 /- equality -/ etaIfUnderApplied e arity do let args := e.getAppArgs - let lhs ← whnf args[inductVal.numParams + inductVal.numIndices + 1]! - let rhs ← whnf args[inductVal.numParams + inductVal.numIndices + 2]! + let lhs ← liftMetaM do Meta.whnf args[inductVal.numParams + inductVal.numIndices + 1]! + let rhs ← liftMetaM do Meta.whnf args[inductVal.numParams + inductVal.numIndices + 2]! let lhs := lhs.toCtorIfLit let rhs := rhs.toCtorIfLit match lhs.isConstructorApp? (← getEnv), rhs.isConstructorApp? (← getEnv) with @@ -301,7 +293,6 @@ where mkAuxLetDecl (← mkLcUnreachable (← inferType e)) | _, _ => throwError "code generator failed, unsupported occurrence of `{declName}`" --/ expandNoConfusionMajor (major : Expr) (numFields : Nat) : M Expr := do match numFields with @@ -309,7 +300,6 @@ where | n+1 => if let .lam _ d b _ := major then let proof := mkLcProof d - trace[Meta.debug] "proof: {proof}" expandNoConfusionMajor (b.instantiate1 proof) n else expandNoConfusionMajor (← etaExpandN major (n+1)) (n+1) @@ -393,7 +383,7 @@ where | .fvar .. | .sort .. | .forallE .. => return e -- Do nothing | _ => if isLCProof e then - return e + return mkConst ``lcErased let type ← liftMetaM <| Meta.inferType e if (← liftMetaM <| Meta.isProp type) then /- We replace proofs with `lcProof` applications. -/ diff --git a/src/Lean/Compiler/Main.lean b/src/Lean/Compiler/Main.lean index 6b01b3403e..ad786bc16e 100644 --- a/src/Lean/Compiler/Main.lean +++ b/src/Lean/Compiler/Main.lean @@ -31,8 +31,9 @@ where def checkpoint (step : Name) (decls : Array Decl) : CoreM Unit := do trace[Meta.debug] "After {step}" for decl in decls do - trace[Meta.debug] "{decl.name} := {decl.value}" - decl.check + withOptions (fun opts => opts.setBool `pp.motives.pi false) do + trace[Meta.debug] "{decl.name} := {decl.value}" + decl.check def compile (declNames : Array Name) : CoreM Unit := do let declNames ← declNames.filterM shouldGenerateCode diff --git a/tests/lean/run/lcnf1.lean b/tests/lean/run/lcnf1.lean index b084414cb2..e4f03b7a12 100644 --- a/tests/lean/run/lcnf1.lean +++ b/tests/lean/run/lcnf1.lean @@ -2,39 +2,30 @@ import Lean open Lean -set_option trace.Meta.debug true -set_option pp.proofs true -set_option pp.funBinderTypes true -set_option pp.letVarTypes true --- set_option pp.explicit true --- set_option pp.match false #eval Compiler.compile #[``List.map] -#exit #eval Compiler.compile #[``Lean.Elab.Term.synthesizeInstMVarCore] -#check @Eq.rec - -#exit #eval Compiler.compile #[``Eq.ndrec] +def g1 (x : Nat) (h : Nat = Int) : Int := + (h ▸ x) + 1 + +#eval Compiler.compile #[``g1] + def f (h : False) (x : Nat) : Nat := (h.rec : Nat → Nat) x -#check @False.casesOn - #eval Compiler.compile #[``f] def g (as : Array (Nat → Nat)) (h : i < as.size ∧ q) : Nat := h.casesOn (fun _ _ => as[i]) i -set_option pp.notation false in #eval Compiler.compile #[``g] def f2 {r : Nat → Nat → Prop} (q : Quot r) : Nat := (q.lift (·+·) sorry : Nat → Nat) 2 -#print Quot.lift #eval Compiler.compile #[``f2] inductive Vec (α : Type u) : Nat → Type u @@ -51,3 +42,8 @@ def Vec.head : Vec α (n+1) → α #eval Compiler.compile #[``Vec.zip] #eval Compiler.compile #[``Vec.zip.match_1] + +#eval Compiler.compile #[``Lean.Elab.Term.reportStuckSyntheticMVar] + +set_option trace.Meta.debug true +#eval Compiler.compile #[``Lean.Elab.Term.synthesizeSyntheticMVars]