diff --git a/Qpf/Macro/Comp.lean b/Qpf/Macro/Comp.lean index 65ce150..9be1eae 100644 --- a/Qpf/Macro/Comp.lean +++ b/Qpf/Macro/Comp.lean @@ -267,6 +267,7 @@ partial def elabQpf {arity : Nat} (vars : Vector Q(Type u) arity) (target : Q(Ty structure QpfCompositionBodyView where + (ref : Syntax := .missing) (type? : Option Syntax := none) (target : Term) (liveBinders deadBinders : Array Syntax) @@ -288,7 +289,7 @@ def elabQpfCompositionBody (view: QpfCompositionBodyView) : liveBinders := {view.liveBinders} deadBinders := {view.deadBinders} " - runTermElabM fun _ => do + runTermElabM fun _ => withRef view.ref do let u : Level ← if let some typeStx := view.type? then let type ← elabTerm typeStx (some <| .sort <|<- mkFreshLevelMVar) diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean index 680b1aa..6d92e14 100644 --- a/Qpf/Macro/Data.lean +++ b/Qpf/Macro/Data.lean @@ -332,7 +332,7 @@ structure MkShapeResult where (effects : CommandElabM Unit) open Parser in -def mkShape (view: DataView) : TermElabM MkShapeResult := do +def mkShape (view : DataView) : TermElabM MkShapeResult := do -- If the original declId was `MyType`, we want to register the shape type under `MyType.Shape` let (declName, declId, shortDeclName) ← addSuffixToDeclId view.declId "Shape" @@ -399,7 +399,7 @@ open Elab.Term Parser.Term in `IsPolynomial F`, and return that instance (if it exists). -/ def isPolynomial (view : DataView) (F: Term) : CommandElabM (Option Term) := do - runTermElabM fun _ => do + runTermElabM fun _ => withRef view.ref do elabBinders view.deadBinders fun _deadVars => do let inst_func ← `(MvFunctor $F:term) let inst_func ← elabTerm inst_func none @@ -459,17 +459,20 @@ def mkType (view : DataView) (base : Term × Term × Term) : CommandElabM Unit : abbrev $baseIdent:ident $view.deadBinders:bracketedBinder* : TypeFun $(quote <| arity + 1) := $base + -- instance foo : MvFunctor.{0,0} ($baseApplied) := $functor + instance foo : MvFunctor.{1,1} ($baseApplied) := $functor instance $baseFunctorIdent:ident : MvFunctor ($baseApplied) := $functor instance $baseQPFIdent:ident : MvQPF ($baseApplied) := $q - abbrev $uncurriedIdent:ident $view.deadBinders:bracketedBinder* : TypeFun $(quote arity) := $fix_or_cofix $base + abbrev $uncurriedIdent:ident $view.deadBinders:bracketedBinder* : TypeFun $(quote arity) := + $fix_or_cofix $base - abbrev $(view.declId) $view.deadBinders:bracketedBinder* - := TypeFun.curried $uncurriedApplied + abbrev $(view.declId) $view.deadBinders:bracketedBinder* := + TypeFun.curried $uncurriedApplied ) - trace[QPF] "elabData.cmd = {cmd}" - elabCommand cmd + withRef view.ref <| + cmd.raw.getArgs.forM elabDeclaration @@ -541,28 +544,29 @@ def elabData : CommandElab := fun stx => do let modifiers ← elabModifiers stx[0] let decl := stx[1] let view ← dataSyntaxToView modifiers decl + withRef view.ref do + let (nonRecView, ⟨r, shape, _P, eff⟩) ← runTermElabM fun _ => withRef view.ref do + let (nonRecView, _rho) ← makeNonRecursive view; + trace[QPF] "nonRecView: {nonRecView}" + pure (nonRecView, ←mkShape nonRecView) + + /- Execute the `ComandElabM` side-effects prescribed by `mkShape` -/ + let _ ← eff + + /- Composition pipeline -/ + let base ← elabQpfCompositionBody { + liveBinders := nonRecView.liveBinders, + deadBinders := nonRecView.deadBinders, + ref := view.ref, + type? := none, + target := ←`( + $(mkIdent shape):ident $r.expr:term* + ) + } + trace[QPF] "base = {base}" - let (nonRecView, ⟨r, shape, _P, eff⟩) ← runTermElabM fun _ => do - let (nonRecView, _rho) ← makeNonRecursive view; - trace[QPF] "nonRecView: {nonRecView}" - pure (nonRecView, ←mkShape nonRecView) - - /- Execute the `ComandElabM` side-effects prescribed by `mkShape` -/ - let _ ← eff - - /- Composition pipeline -/ - let base ← elabQpfCompositionBody { - liveBinders := nonRecView.liveBinders, - deadBinders := nonRecView.deadBinders, - type? := none, - target := ←`( - $(mkIdent shape):ident $r.expr:term* - ) - } - trace[QPF] "base = {base}" - - mkType view base - mkConstructors view shape + mkType view base + mkConstructors view shape end Data.Command diff --git a/Qpf/Macro/Data/View.lean b/Qpf/Macro/Data/View.lean index 6c78c9a..9e8256f 100644 --- a/Qpf/Macro/Data/View.lean +++ b/Qpf/Macro/Data/View.lean @@ -2,7 +2,7 @@ import Lean import Qpf.Macro.Common open Lean -open Meta Elab Elab.Command +open Meta Elab Elab.Command open Parser.Term (bracketedBinder) open Parser.Command (declId) @@ -14,7 +14,7 @@ inductive DataCommand where | Codata deriving BEq, Inhabited -namespace DataCommand +namespace DataCommand def fromSyntax : Syntax → CommandElabM DataCommand | Syntax.atom _ "data" => pure .Data @@ -62,13 +62,13 @@ def DataView.asInductive (view : DataView) : InductiveView := { ref := view.ref declId := view.declId - modifiers := view.modifiers - shortDeclName := view.shortDeclName - declName := view.declName - levelNames := view.levelNames - binders := view.binders - type? := view.type? - ctors := view.ctors + modifiers := view.modifiers + shortDeclName := view.shortDeclName + declName := view.declName + levelNames := view.levelNames + binders := view.binders + type? := view.type? + ctors := view.ctors derivingClasses := view.derivingClasses -- TODO: find out what these computed fields are, add support for them in `data`/`codata` computedFields := #[] @@ -108,7 +108,7 @@ def DataView.addDeclNameSuffix (view : DataView) (suffix : String) : DataView def DataView.getExpectedType (view : DataView) : Term := Syntax.mkApp (mkIdent view.shortDeclName) ( (Macro.getBinderIdents view.binders.getArgs false) - ) + ) /-- Returns the fully applied, explicit (`@`) form of the type to be defined -/ def DataView.getExplicitExpectedType (view : DataView) : CommandElabM Term @@ -158,16 +158,17 @@ instance : ToString (DataView) := ⟨ -/ +open Elab Term /-- Raises (hopefully) more informative errors when `data` or `codata` are used with unsupported specifications -/ -def DataView.doSanityChecks (view : DataView) : CommandElabM Unit := do - if view.liveBinders.isEmpty then +def DataView.doSanityChecks (view : DataView) : CommandElabM Unit := do + if view.liveBinders.isEmpty then if view.deadBinders.isEmpty then if view.command == .Codata then throwError "Due to a bug, codatatype without any parameters don't quite work yet. Please try adding parameters to your type" - else + else throwError "Trying to define a datatype without variables, you probably want an `inductive` type instead" else throwErrorAt view.binders "You should mark some variables as live by removing the type ascription (they will be automatically inferred as `Type _`), or if you don't have variables of type `Type _`, you probably want an `inductive` type" @@ -179,8 +180,15 @@ def DataView.doSanityChecks (view : DataView) : CommandElabM Unit := do -- TODO: make this more intelligent. In particular, allow types like `Type`, `Type 3`, or `Type u` -- and only throw an error if the user tries to define a family of types + match view.type? with - | some t => throwErrorAt t "Unexpected type; type will be automatically inferred. Note that inductive families are not supported due to inherent limitations of QPFs" + | some t_stx => + let t : Expr ← runTermElabM <| fun _ => + elabTerm t_stx none + if t.isType then + pure () + else + throwErrorAt t_stx "Unexpected type; type will be automatically inferred. Note that inductive families are not supported due to inherent limitations of QPFs" | none => pure () @@ -193,7 +201,7 @@ def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM Data let (binders, type?) := expandOptDeclSig decl[2] - let declId : TSyntax ``declId := ⟨decl[1]⟩ + let declId : TSyntax ``declId := ⟨decl[1]⟩ let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers addDeclarationRanges declName decl let ctors ← decl[4].getArgs.mapM fun ctor => withRef ctor do diff --git a/Test/Arrow.lean b/Test/Arrow.lean index a0bfc31..c12a3a6 100644 --- a/Test/Arrow.lean +++ b/Test/Arrow.lean @@ -1,16 +1,42 @@ import Qpf +universe u v w + /-- info: MvQPF.Arrow ?α : CurriedTypeFun 1 -/ #guard_msgs in #check MvQPF.Arrow ?α -data Arrow (α : Type _) β +data Arrow (α : Type) β : Type u | mk : (α → β) → Arrow α β /-- info: Arrow : Type → CurriedTypeFun 1 -/ #guard_msgs in #check (Arrow : Type → Type → Type) --- Types generated by `data` are not as polymorphic as they could/should be, --- so the following does not yet work: --- `#check (Arrow : Type 1 → Type 1 → Type 1)` +/-- info: Arrow.Shape : Type u → Type v → Type w → Type w -/ +#guard_msgs in #check (Arrow.Shape : Type u → Type v → Type w → Type w) + +/-- info: Arrow.Base : Type → TypeFun 2 -/ +#guard_msgs in #check (Arrow.Base : Type → TypeFun.{u, u} 2) + +#synth MvFunctor (Arrow.Base.{0} _) +-- ^^^ This works +#synth MvFunctor (Arrow.Base.{1} _) +-- ^^^ but this already does not, which explains the issues below +-- If we add instance foo : MvFunctor.{1,1} ($baseApplied) := $functor to Qpf/Macro/Data.lean explicitely, +-- it seems to work but it produces a weird type error. + +-- #synth MvQPF (Arrow.Base _ : TypeFun.{0} 2) +-- -- ^^^ We know that the `Base` is a QPF for universe 0 +-- +-- #synth MvQPF (Arrow.Base _ : TypeFun.{1} 2) +-- -- ^^^ But, somehow we can't synthesize this fact for higher universes +-- +-- #check (Arrow.Uncurried : Type → TypeFun.{1} 1) +-- -- ^^^ Which, presumably, is why `Uncurried` is *not* polymorphic +-- +-- +-- +-- /-- info: Arrow : Type → CurriedTypeFun 1 -/ +-- #guard_msgs in +-- #check (Arrow : Type → Type u → Type u)