Allow Identifiers to store a list of Modules rather than a single one (#839)

* Allow Identifiers to store a list of Modules rather than a single one

* Fix rogue print statements

* Fix pattern synonym

* Fix formatting error

* Fix nothunks

Author: MatthewDaggitt

tasty-golden-executable/src/Test/Tasty/Golden/Executable/Error.hs

@@ -88,7 +88,6 @@ instance Exception ProducedFilesError
 
 handleProducedFilesError :: ProducedFilesError -> IO Result
 handleProducedFilesError ProducedFilesError {..} = do
-  print stdoutDiff
   let message =
         unlines . catMaybes $
           [ case stderrDiff of

tasty-golden-executable/src/Test/Tasty/Golden/Executable/Runner.hs

@@ -412,8 +412,6 @@ acceptTestProduced testProduces (IgnoreFiles testIgnores) = do
           NonEmpty.prependList
             otherTestSpecsBefore
             $ NonEmpty.appendList (NonEmpty.singleton acceptTestSpec) otherTestSpecsAfter
-    liftIO $ putStrLn "Hi2"
-    liftIO $ print acceptTestSpecsList
     let acceptTestSpecs = TestSpecs acceptTestSpecsList
     lift $ writeTestSpecsFile (testDirectory </> testSpecsFileName) acceptTestSpecs
   -- Remove the outdated .golden files:

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

@@ -75,6 +75,7 @@ instance NoThunks MetaID
 
 -- Vehicle.Syntax.AST.Name
 instance NoThunks Module
+instance NoThunks ModulePath
 instance NoThunks Identifier
 
 -- Vehicle.Syntax.AST.Prog

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

@@ -7,7 +7,7 @@ import Data.Serialize (Serialize)
 import Data.Serialize.Text ()
 import Data.Text (Text)
 import GHC.Generics (Generic)
-import Prettyprinter (Pretty (..))
+import Prettyprinter (Pretty (..), concatWith, dot, surround)
 
 --------------------------------------------------------------------------------
 -- Definition
@@ -20,6 +20,7 @@ type Name = Text
 data Module
   = User
   | StdLib
+  | Record Name
   deriving (Eq, Ord, Show, Generic)
 
 instance NFData Module
@@ -36,15 +37,37 @@ instance Pretty Module where
   pretty = \case
     User -> "User"
     StdLib -> "StdLib"
+    Record name -> pretty name
+
+newtype ModulePath = ModulePath
+  { modules :: [Module]
+  }
+  deriving (Eq, Ord, Show, Generic)
+
+instance NFData ModulePath
+
+instance Hashable ModulePath
+
+instance ToJSON ModulePath
+
+instance FromJSON ModulePath
+
+instance Serialize ModulePath
+
+instance Pretty ModulePath where
+  pretty (ModulePath m) = concatWith (surround dot) (fmap pretty m)
 
 --------------------------------------------------------------------------------
 -- Identifiers
 
-data Identifier = Identifier Module Name
+data Identifier = Identifier
+  { modulePath :: ModulePath,
+    identifierName :: Name
+  }
   deriving (Eq, Ord, Show, Generic)
 
 instance Pretty Identifier where
-  pretty (Identifier m s) = pretty m <> "." <> pretty s
+  pretty (Identifier m s) = pretty m <> dot <> pretty s
 
 instance NFData Identifier
 
@@ -61,11 +84,14 @@ instance Serialize Identifier
 class HasIdentifier a where
   identifierOf :: a -> Identifier
 
-moduleOf :: Identifier -> Module
-moduleOf (Identifier m _) = m
+stdlibIdentifier :: Name -> Identifier
+stdlibIdentifier = Identifier (ModulePath [StdLib])
+
+isUserIdent :: Identifier -> Bool
+isUserIdent ident = User `elem` modules (modulePath ident)
 
-identifierName :: Identifier -> Name
-identifierName (Identifier _ n) = n
+changeName :: Identifier -> Name -> Identifier
+changeName Identifier {..} newName = Identifier {identifierName = newName, ..}
 
 --------------------------------------------------------------------------------
 -- Names

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

@@ -18,8 +18,8 @@ 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.Name (Module (..))
+import Prettyprinter (Pretty (..), squotes, (<+>))
+import System.FilePath (takeFileName)
 import Vehicle.Syntax.Parse.Token
 
 --------------------------------------------------------------------------------
@@ -96,10 +96,13 @@ expandRange (l, r) (Range {..}) =
 
 data Provenance = Provenance
   { range :: Range,
-    modul :: Module
+    file :: FilePath
   }
   deriving (Generic)
 
+noProvenance :: Provenance
+noProvenance = Provenance mempty "unknown"
+
 instance Show Provenance where
   show = const ""
 
@@ -114,9 +117,19 @@ instance Hashable Provenance where
 
 instance Serialize Provenance
 
+instance Pretty Provenance where
+  pretty (Provenance origin file) = "file" <+> squotes (pretty (takeFileName file)) <+> "at" <+> pretty origin
+
+instance Semigroup Provenance where
+  Provenance origin1 owner1 <> Provenance origin2 _owner2 =
+    Provenance (origin1 <> origin2) owner1
+
+instance Monoid Provenance where
+  mempty = noProvenance
+
 -- | Get the provenance for a single token.
-tkProvenance :: (IsToken a) => Module -> a -> Provenance
-tkProvenance modl tk = Provenance (Range start end) modl
+tkProvenance :: (IsToken a) => a -> FilePath -> Provenance
+tkProvenance tk = Provenance (Range start end)
   where
     start = tkPosition tk
     end = Position (posLine start) (posColumn start + tkLength tk)
@@ -126,29 +139,14 @@ fillInProvenance provenances = do
   let (starts, ends) = NonEmpty.unzip (fmap getPositions provenances)
   let start = minimum starts
   let end = maximum ends
-  Provenance (Range start end) (modul $ NonEmpty.head provenances)
+  Provenance (Range start end) (file $ NonEmpty.head provenances)
   where
     getPositions :: Provenance -> (Position, Position)
     getPositions (Provenance (Range start end) _) = (start, end)
 
 expandProvenance :: (Int, Int) -> Provenance -> Provenance
 expandProvenance w (Provenance range o) = Provenance (expandRange w range) o
 
-instance Pretty Provenance where
-  pretty (Provenance origin modl) = case modl of
-    User -> pretty origin
-    StdLib -> pretty modl <> "," <+> pretty origin
-
-instance Semigroup Provenance where
-  Provenance origin1 owner1 <> Provenance origin2 _owner2 =
-    Provenance (origin1 <> origin2) owner1
-
-noProvenance :: Provenance
-noProvenance = Provenance mempty User
-
-instance Monoid Provenance where
-  mempty = Provenance mempty User
-
 --------------------------------------------------------------------------------
 -- Type-classes
 

vehicle-syntax/src/Vehicle/Syntax/BNFC/Elaborate/External.hs

@@ -12,7 +12,7 @@ where
 
 import Control.Monad (foldM_)
 import Control.Monad.Except (MonadError (..), throwError)
-import Control.Monad.Reader (MonadReader (..), runReaderT)
+import Control.Monad.Reader (runReaderT)
 import Data.Bitraversable (bitraverse)
 import Data.Either (partitionEithers)
 import Data.List (find)
@@ -28,6 +28,8 @@ import Prettyprinter
 import Vehicle.Syntax.AST qualified as V
 import Vehicle.Syntax.BNFC.Utils
   ( MonadElab,
+    ParseLocation,
+    getModule,
     mkProvenance,
     tokArrow,
     tokDot,
@@ -61,10 +63,10 @@ newtype UnparsedExpr = UnparsedExpr B.Expr
 -- types and definitions.
 partiallyElabProg ::
   (MonadError ParseError m) =>
-  V.Module ->
+  ParseLocation ->
   B.Prog ->
   m PartiallyParsedProg
-partiallyElabProg modl (B.Main decls) = flip runReaderT modl $ do
+partiallyElabProg file (B.Main decls) = flip runReaderT file $ do
   V.Main <$> partiallyElabDecls decls
 
 partiallyElabDecls :: (MonadElab m) => [B.Decl] -> m [PartiallyParsedDecl]
@@ -303,10 +305,10 @@ getTypeOption = \case
 
 elaborateDecl ::
   (MonadError ParseError m) =>
-  V.Module ->
+  ParseLocation ->
   PartiallyParsedDecl ->
   m (V.Decl V.Name V.Builtin)
-elaborateDecl modl decl = flip runReaderT modl $ case decl of
+elaborateDecl file decl = flip runReaderT file $ case decl of
   V.DefAbstract p n r t -> V.DefAbstract p n r <$> elabDeclType t
   V.DefFunction p n b t e -> V.DefFunction p n b <$> elabDeclType t <*> elabDeclBody e
 
@@ -330,10 +332,10 @@ elabDeclBody (UnparsedExpr expr) = case expr of
 
 elaborateExpr ::
   (MonadError ParseError m) =>
-  V.Module ->
+  ParseLocation ->
   UnparsedExpr ->
   m (V.Expr V.Name V.Builtin)
-elaborateExpr modl (UnparsedExpr expr) = runReaderT (elabExpr expr) modl
+elaborateExpr file (UnparsedExpr expr) = runReaderT (elabExpr expr) file
 
 elabExpr :: (MonadElab m) => B.Expr -> m (V.Expr V.Name V.Builtin)
 elabExpr = \case
@@ -391,7 +393,7 @@ elabExpr = \case
   B.HasMap tk -> builtinTypeClass V.HasMap tk []
   B.HasFold tk -> builtinTypeClass V.HasFold tk []
   -- NOTE: we reverse the arguments to make it well-typed.
-  B.Ann e tk t -> freeVar (V.Identifier V.StdLib "typeAnn") tk [t, e]
+  B.Ann e tk t -> elabExpr (B.App (B.App (B.Var (B.Name (tkLocation tk, "typeAnn"))) (B.ExplicitArg t)) (B.ExplicitArg e))
 
 elabArg :: (MonadElab m) => B.Arg -> m (V.Arg V.Name V.Builtin)
 elabArg = \case
@@ -401,7 +403,7 @@ elabArg = \case
 
 elabName :: (MonadElab m) => B.Name -> m V.Identifier
 elabName n = do
-  modl <- ask
+  modl <- getModule
   return $ V.Identifier modl $ tkSymbol n
 
 elabBasicBinder :: (MonadElab m) => Bool -> B.BasicBinder -> m (V.Binder V.Name V.Builtin)
@@ -493,11 +495,6 @@ op2 mk t e1 e2 = do
   let p = V.fillInProvenance (tProv :| [V.provenanceOf ce1, V.provenanceOf ce2])
   return $ mk p ce1 ce2
 
-freeVar :: (MonadElab m, IsToken token) => V.Identifier -> token -> [B.Expr] -> m (V.Expr V.Name V.Builtin)
-freeVar b t args = do
-  tProv <- mkProvenance t
-  app (V.FreeVar tProv b) <$> traverse elabExpr args
-
 builtin :: (MonadElab m, IsToken token) => V.Builtin -> token -> [B.Expr] -> m (V.Expr V.Name V.Builtin)
 builtin b t args = do
   tProv <- mkProvenance t
@@ -603,9 +600,9 @@ elabQuantifierIn ::
   m (V.Expr V.Name V.Builtin)
 elabQuantifierIn tk q binder container body = do
   p <- mkProvenance tk
-  let quantBuiltin = V.FreeVar p $ case q of
-        V.Forall -> V.Identifier V.StdLib "forallIn"
-        V.Exists -> V.Identifier V.StdLib "existsIn"
+  let quantBuiltin = V.BoundVar p $ case q of
+        V.Forall -> "forallIn"
+        V.Exists -> "existsIn"
 
   binder' <- elabNameBinder False binder
   container' <- elabExpr container
@@ -627,7 +624,7 @@ elabForeach ::
   m (V.Expr V.Name V.Builtin)
 elabForeach tk binder body = do
   p <- mkProvenance tk
-  let foreachBuiltin = V.FreeVar p (V.Identifier V.StdLib "foreachIndex")
+  let foreachBuiltin = V.BoundVar p "foreachIndex"
 
   binder' <- elabNameBinder False binder
   body' <- elabExpr body

vehicle-syntax/src/Vehicle/Syntax/BNFC/Utils.hs

@@ -3,26 +3,32 @@
 module Vehicle.Syntax.BNFC.Utils where
 
 import Control.Monad.Except (MonadError)
-import Control.Monad.Reader (MonadReader (..))
+import Control.Monad.Reader (MonadReader (..), asks)
 import Data.Text (Text, pack)
-import Vehicle.Syntax.AST.Name (Module)
+import Vehicle.Syntax.AST.Name (ModulePath)
 import Vehicle.Syntax.AST.Provenance
 import Vehicle.Syntax.External.Abs qualified as B
 import Vehicle.Syntax.Parse.Error (ParseError (..))
 import Vehicle.Syntax.Parse.Token (IsToken, mkToken)
 
 type MonadElab m =
   ( MonadError ParseError m,
-    MonadReader Module m
+    MonadReader ParseLocation m
   )
 
 pattern InferableOption :: Text
 pattern InferableOption = "infer"
 
+type ParseLocation = (ModulePath, FilePath)
+
+getModule :: (MonadElab m) => m ModulePath
+getModule = asks fst
+
+getFile :: (MonadElab m) => m FilePath
+getFile = asks snd
+
 mkProvenance :: (MonadElab m, IsToken tk) => tk -> m Provenance
-mkProvenance tk = do
-  modl <- ask
-  return $ tkProvenance modl tk
+mkProvenance tk = tkProvenance tk <$> getFile
 
 tokType :: Int -> B.Expr
 tokType l = B.Type (mkToken B.TokType ("Type" <> pack (show l)))

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

@@ -3,6 +3,7 @@ module Vehicle.Syntax.Parse
     UnparsedExpr,
     PartiallyParsedProg,
     PartiallyParsedDecl,
+    ParseLocation,
     readAndParseProg,
     parseDecl,
     parseExpr,
@@ -14,6 +15,7 @@ import Control.Monad.Except (MonadError (..))
 import Data.Text (Text)
 import Vehicle.Syntax.AST
 import Vehicle.Syntax.BNFC.Elaborate.External
+import Vehicle.Syntax.BNFC.Utils (ParseLocation)
 import Vehicle.Syntax.Builtin
 import Vehicle.Syntax.External.Abs qualified as External (Expr, Prog)
 import Vehicle.Syntax.External.Layout as External (resolveLayout)
@@ -24,14 +26,14 @@ import Vehicle.Syntax.Parse.Error (ParseError (..))
 --------------------------------------------------------------------------------
 -- Interface
 
-readAndParseProg :: (MonadError ParseError m) => Module -> Text -> m PartiallyParsedProg
+readAndParseProg :: (MonadError ParseError m) => ParseLocation -> Text -> m PartiallyParsedProg
 readAndParseProg modul txt =
   castBNFCError (partiallyElabProg modul) (parseExternalProg txt)
 
-parseDecl :: (MonadError ParseError m) => Module -> PartiallyParsedDecl -> m (Decl Name Builtin)
+parseDecl :: (MonadError ParseError m) => ParseLocation -> PartiallyParsedDecl -> m (Decl Name Builtin)
 parseDecl = elaborateDecl
 
-parseExpr :: (MonadError ParseError m) => Module -> UnparsedExpr -> m (Expr Name Builtin)
+parseExpr :: (MonadError ParseError m) => ParseLocation -> UnparsedExpr -> m (Expr Name Builtin)
 parseExpr = elaborateExpr
 
 readExpr :: (MonadError ParseError m) => Text -> m UnparsedExpr

vehicle-syntax/vehicle-syntax.cabal

@@ -166,6 +166,7 @@ library
     , cereal-text    >=0.1   && <1
     , containers     >=0.5   && <1
     , deepseq        >=1.4   && <2
+    , filepath       >=1.4   && <2
     , hashable       >=1.3   && <2
     , mtl            >=2.2   && <3
     , prettyprinter  >=1.7   && <2

vehicle/src/Vehicle/Backend/Agda/Compile.hs

@@ -911,7 +911,7 @@ pattern TensorType ::
   Expr Name Builtin
 pattern TensorType p tElem tDims <-
   App
-    (FreeVar p (Identifier StdLib "Tensor"))
+    (FreeVar p TensorIdent)
     [ RelevantExplicitArg _ tElem,
       IrrelevantExplicitArg _ tDims
       ]