From 1db5cc5ea86ce20792853ddcc1547a793cac5fde Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Tue, 8 Oct 2024 21:56:14 -0500 Subject: [PATCH] add test case without live variables This currently breaks, but functions as a starting point --- Qpf/Macro/Data/View.lean | 21 ++++++++------------- Test.lean | 1 + Test/NoLiveVars.lean | 14 ++++++++++++++ 3 files changed, 23 insertions(+), 13 deletions(-) create mode 100644 Test/NoLiveVars.lean diff --git a/Qpf/Macro/Data/View.lean b/Qpf/Macro/Data/View.lean index fe00c4b..81a65a7 100644 --- a/Qpf/Macro/Data/View.lean +++ b/Qpf/Macro/Data/View.lean @@ -232,19 +232,14 @@ instance : ToString (DataView) := ⟨ specifications -/ 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 - 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" - - -- TODO: remove once dead variables are fully supported - if !view.deadBinders.isEmpty then - dbg_trace "Dead variables are not fully supported yet" - + -- 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 + -- 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" -- 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 diff --git a/Test.lean b/Test.lean index 6003607..b4edc82 100644 --- a/Test.lean +++ b/Test.lean @@ -9,3 +9,4 @@ import Test.Tree -- import Test.Variable import Test.WithBindersInCtor import Test.Wrap +import Test.NoLiveVariables diff --git a/Test/NoLiveVars.lean b/Test/NoLiveVars.lean new file mode 100644 index 0000000..5aefc07 --- /dev/null +++ b/Test/NoLiveVars.lean @@ -0,0 +1,14 @@ +import Qpf + +/-! +Tests to assert we can have (`co`)`data` types without +any live variables +-/ + +namespace Qpf.Test.NoLiveVars + +data Data (α : Type) where + | dat : α → Data α + +codata Codata (α : Type) where + | dat : α → Codata α → Codata α