Refactor so that scoped and unscoped expressions are different data t…

…ypes (#841)

* Refactor so that scoped and unscoped expressions are different data types

* More fixes to NoThunks

* Fix unit tests

vehicle-syntax/src/Vehicle/Syntax/AST.hs

@@ -8,7 +8,6 @@ import Vehicle.Syntax.AST.Binder as X
 import Vehicle.Syntax.AST.Decl as X
 import Vehicle.Syntax.AST.Expr as X
 import Vehicle.Syntax.AST.Instances.NoThunks ()
-import Vehicle.Syntax.AST.Meta as X
 import Vehicle.Syntax.AST.Name as X
 import Vehicle.Syntax.AST.Prog as X
 import Vehicle.Syntax.AST.Provenance as X

vehicle-syntax/src/Vehicle/Syntax/AST/Binder.hs

@@ -165,7 +165,10 @@ mapBinderNamingForm f Binder {..} =
       ..
     }
 
-mkDefaultBinder :: Name -> expr -> GenericBinder expr
-mkDefaultBinder name = Binder mempty displayForm Explicit Relevant
-  where
-    displayForm = BinderDisplayForm (OnlyName name) True
+mkDefaultBinderDisplayForm :: Maybe Name -> BinderDisplayForm
+mkDefaultBinderDisplayForm = \case
+  Just name -> BinderDisplayForm (OnlyName name) True
+  Nothing -> BinderDisplayForm OnlyType True
+
+mkDefaultBinder :: expr -> Maybe Name -> GenericBinder expr
+mkDefaultBinder typ name = Binder mempty (mkDefaultBinderDisplayForm name) Explicit Relevant typ

vehicle-syntax/src/Vehicle/Syntax/AST/Decl.hs

@@ -4,11 +4,9 @@ import Control.DeepSeq (NFData)
 import Data.Serialize (Serialize)
 import GHC.Generics (Generic)
 import Prettyprinter (Pretty (..))
-import Vehicle.Syntax.AST.Expr
 import Vehicle.Syntax.AST.Name
 import Vehicle.Syntax.AST.Provenance
 import Vehicle.Syntax.AST.Type
-import Vehicle.Syntax.Builtin
 
 --------------------------------------------------------------------------------
 -- Declarations
@@ -30,8 +28,6 @@ data GenericDecl expr
       expr -- Body of the definition.
   deriving (Eq, Show, Functor, Foldable, Traversable, Generic)
 
-type Decl var builtin = GenericDecl (Expr var builtin)
-
 instance (NFData expr) => NFData (GenericDecl expr)
 
 instance (Serialize expr) => Serialize (GenericDecl expr)
@@ -116,7 +112,7 @@ data DefAbstractSort
   = NetworkDef
   | DatasetDef
   | ParameterDef ParameterSort
-  | PostulateDef (Maybe (Expr Name Builtin)) (Maybe (Expr Name Builtin))
+  | PostulateDef
   deriving (Eq, Show, Generic)
 
 instance NFData DefAbstractSort
@@ -140,7 +136,7 @@ isExternalResourceSort = \case
 
 convertToPostulate :: GenericDecl expr -> GenericDecl expr
 convertToPostulate d =
-  DefAbstract (provenanceOf d) (identifierOf d) (PostulateDef Nothing Nothing) (typeOf d)
+  DefAbstract (provenanceOf d) (identifierOf d) PostulateDef (typeOf d)
 
 --------------------------------------------------------------------------------
 -- Annotations options

vehicle-syntax/src/Vehicle/Syntax/AST/Expr.hs

@@ -1,63 +1,41 @@
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+{-# HLINT ignore "Use list literal" #-}
 module Vehicle.Syntax.AST.Expr
   ( -- * Generic expressions
     Arg,
     Binder,
+    Decl,
+    Prog,
     Expr
       ( Universe,
         App,
         Pi,
         Builtin,
-        BoundVar,
-        FreeVar,
+        Var,
         Hole,
-        Meta,
         Let,
         Lam
       ),
     Type,
-    UniverseLevel (..),
-    Telescope,
 
     -- * Utilities
     isTypeSynonym,
-    isPi,
     mkHole,
     normAppList,
-    getFreeVarApp,
-    getBuiltinApp,
-    pattern TypeUniverse,
     pattern BuiltinExpr,
   )
 where
 
-import Control.DeepSeq (NFData)
-import Data.Hashable (Hashable)
 import Data.List.NonEmpty (NonEmpty (..))
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Serialize (Serialize)
 import GHC.Generics (Generic)
-import Prettyprinter (Pretty (..), (<+>))
 import Vehicle.Syntax.AST.Arg
 import Vehicle.Syntax.AST.Binder
-import Vehicle.Syntax.AST.Meta (MetaID)
-import Vehicle.Syntax.AST.Name (Identifier, Name)
+import Vehicle.Syntax.AST.Decl (GenericDecl)
+import Vehicle.Syntax.AST.Name (Name)
+import Vehicle.Syntax.AST.Prog (GenericProg)
 import Vehicle.Syntax.AST.Provenance (HasProvenance (..), Provenance, fillInProvenance)
-import Vehicle.Syntax.Prelude ()
-
---------------------------------------------------------------------------------
--- Universes
-
-newtype UniverseLevel = UniverseLevel Int
-  deriving (Eq, Ord, Show, Generic)
-
-instance NFData UniverseLevel
-
-instance Hashable UniverseLevel
-
-instance Serialize UniverseLevel
-
-instance Pretty UniverseLevel where
-  pretty (UniverseLevel l) = "Type" <+> pretty l
+import Vehicle.Syntax.Builtin (Builtin)
 
 --------------------------------------------------------------------------------
 -- Expressions
@@ -69,40 +47,31 @@ instance Pretty UniverseLevel where
 --
 -- Names are parameterised over so that they can store
 -- either the user assigned names or deBruijn indices.
-data Expr var builtin
+data Expr
   = -- | A universe, used to type types.
     Universe
       Provenance
-      UniverseLevel
   | -- | Application of one term to another. Doesn't have provenance as it has no syntax in the grammar.
     UnsafeApp
-      (Expr var builtin) -- Function.
-      (NonEmpty (Arg var builtin)) -- Arguments.
+      Expr -- Function.
+      (NonEmpty Arg) -- Arguments.
   | -- | Dependent product (subsumes both functions and universal quantification).
     Pi
       Provenance
-      (Binder var builtin) -- The bound name
-      (Expr var builtin) -- (Dependent) result type.
+      Binder -- The bound name
+      Expr -- (Dependent) result type.
   | -- | Terms consisting of constants that are built into the language.
     Builtin
       Provenance
-      builtin -- Builtin name.
-  | -- | Variables that are bound locally by other expressions
-    BoundVar
+      Builtin -- Builtin name.
+  | -- | Variables in the program.
+    Var
       Provenance
-      var -- Variable name.
-  | -- | Variables that refer to other declarations
-    FreeVar
-      Provenance
-      Identifier -- Declaration name
+      Name -- Variable name.
   | -- | A hole in the program.
     Hole
       Provenance
       Name -- Hole name.
-  | -- | Unsolved meta variables.
-    Meta
-      Provenance
-      MetaID -- Meta variable number.
   | -- | Let expressions. We have these in the core syntax because we want to
     -- cross compile them to various backends.
     --
@@ -111,106 +80,83 @@ data Expr var builtin
     -- operations concisely much easier.
     Let
       Provenance
-      (Expr var builtin) -- Bound expression body.
-      (Binder var builtin) -- Bound expression name.
-      (Expr var builtin) -- Expression body.
+      Expr -- Bound expression body.
+      Binder -- Bound expression name.
+      Expr -- Expression body.
   | -- | Lambda expressions (i.e. anonymous functions).
     Lam
       Provenance
-      (Binder var builtin) -- Bound expression name.
-      (Expr var builtin) -- Expression body.
-  deriving (Eq, Show, Functor, Foldable, Traversable, Generic)
+      Binder -- Bound expression name.
+      Expr -- Expression body.
+  deriving (Eq, Show, Generic)
+
+--------------------------------------------------------------------------------
+-- The AST datatypes specialised to the Expr type
+
+type Type = Expr
+
+type Binder = GenericBinder Expr
+
+type Arg = GenericArg Expr
+
+type Decl = GenericDecl Expr
+
+type Prog = GenericProg Expr
 
 --------------------------------------------------------------------------------
 -- Safe applications
 
 -- | Smart constructor for applications with possibly no arguments.
-normAppList :: Expr var builtin -> [Arg var builtin] -> Expr var builtin
+normAppList :: Expr -> [Arg] -> Expr
 normAppList f [] = f
 normAppList f (x : xs) = App f (x :| xs)
 
 -- | Smart constructor for applications.
-normApp :: Expr var builtin -> NonEmpty (Arg var builtin) -> Expr var builtin
+normApp :: Expr -> NonEmpty Arg -> Expr
 normApp (UnsafeApp f xs) ys = UnsafeApp f (xs <> ys)
 normApp f xs = UnsafeApp f xs
 
 -- | Safe pattern synonym for applications.
-pattern App :: Expr var builtin -> NonEmpty (Arg var builtin) -> Expr var builtin
+pattern App :: Expr -> NonEmpty Arg -> Expr
 pattern App f xs <- UnsafeApp f xs
   where
     App f xs = normApp f xs
 
-{-# COMPLETE Universe, App, Pi, Builtin, BoundVar, FreeVar, Hole, Meta, Let, Lam #-}
+{-# COMPLETE Universe, App, Pi, Builtin, Var, Hole, Let, Lam #-}
 
 --------------------------------------------------------------------------------
 -- Instances
 
-instance (NFData var, NFData builtin) => NFData (Expr var builtin)
-
-instance (Serialize var, Serialize builtin) => Serialize (Expr var builtin)
-
-instance HasProvenance (Expr var builtin) where
+instance HasProvenance Expr where
   provenanceOf = \case
-    Universe p _ -> p
+    Universe p -> p
     Hole p _ -> p
-    Meta p _ -> p
     App e xs -> fillInProvenance (provenanceOf e :| provenanceOf xs : [])
     Pi p _ _ -> p
     Builtin p _ -> p
-    BoundVar p _ -> p
-    FreeVar p _ -> p
+    Var p _ -> p
     Let p _ _ _ -> p
     Lam p _ _ -> p
 
---------------------------------------------------------------------------------
--- The AST datatypes specialised to the Expr type
-
-type Type = Expr
-
-type Binder var builtin = GenericBinder (Expr var builtin)
-
-type Arg var builtin = GenericArg (Expr var builtin)
-
-type Telescope var builtin = [Binder var builtin]
-
 --------------------------------------------------------------------------------
 -- Utilities
 
-mkHole :: Provenance -> Name -> Expr var builtin
+mkHole :: Provenance -> Name -> Expr
 mkHole p name = Hole p ("_" <> name)
 
 -- | Tests if a definition's type indicates that the definition is a type
 -- synonym.
-isTypeSynonym :: Type var builtin -> Bool
+isTypeSynonym :: Type -> Bool
 isTypeSynonym = \case
   Universe {} -> True
   Pi _ _ res -> isTypeSynonym res
   _ -> False
 
-isPi :: Type var builtin -> Bool
-isPi Pi {} = True
-isPi _ = False
-
-pattern TypeUniverse :: Provenance -> Int -> Expr var builtin
-pattern TypeUniverse p l = Universe p (UniverseLevel l)
-
 pattern BuiltinExpr ::
   Provenance ->
-  builtin ->
-  NonEmpty (Arg var builtin) ->
-  Expr var builtin
+  Builtin ->
+  NonEmpty Arg ->
+  Expr
 pattern BuiltinExpr p b args <- App (Builtin p b) args
   where
     BuiltinExpr p b args = App (Builtin p b) args
-
-getBuiltinApp :: Expr var builtin -> Maybe (Provenance, builtin, [Arg var builtin])
-getBuiltinApp = \case
-  Builtin p b -> Just (p, b, [])
-  App (Builtin p b) args -> Just (p, b, NonEmpty.toList args)
-  _ -> Nothing
-
-getFreeVarApp :: Expr var builtin -> Maybe (Provenance, Identifier, [Arg var builtin])
-getFreeVarApp = \case
-  FreeVar p b -> Just (p, b, [])
-  App (FreeVar p b) args -> Just (p, b, NonEmpty.toList args)
-  _ -> Nothing

vehicle-syntax/src/Vehicle/Syntax/AST/Instances/NoThunks.hs

@@ -7,7 +7,6 @@ import Vehicle.Syntax.AST.Arg
 import Vehicle.Syntax.AST.Binder
 import Vehicle.Syntax.AST.Decl
 import Vehicle.Syntax.AST.Expr
-import Vehicle.Syntax.AST.Meta
 import Vehicle.Syntax.AST.Name
 import Vehicle.Syntax.AST.Prog
 import Vehicle.Syntax.AST.Provenance
@@ -67,11 +66,7 @@ instance NoThunks DefAbstractSort
 instance NoThunks Annotation
 
 -- Vehicle.Syntax.AST.Expr
-instance NoThunks UniverseLevel
-instance (NoThunks var, NoThunks builtin) => NoThunks (Expr var builtin)
-
--- Vehicle.Syntax.AST.Meta
-instance NoThunks MetaID
+instance NoThunks Expr
 
 -- Vehicle.Syntax.AST.Name
 instance NoThunks Module

vehicle-syntax/src/Vehicle/Syntax/AST/Prog.hs

@@ -4,7 +4,6 @@ import Control.DeepSeq (NFData)
 import Data.Serialize (Serialize)
 import GHC.Generics (Generic)
 import Vehicle.Syntax.AST.Decl (GenericDecl)
-import Vehicle.Syntax.AST.Expr (Expr)
 
 --------------------------------------------------------------------------------
 -- Programs
@@ -15,8 +14,6 @@ newtype GenericProg expr
     Main [GenericDecl expr]
   deriving (Eq, Show, Functor, Foldable, Traversable, Generic)
 
-type Prog var builtin = GenericProg (Expr var builtin)
-
 instance (NFData expr) => NFData (GenericProg expr)
 
 instance (Serialize expr) => Serialize (GenericProg expr)