Add: pragma support

app/Commands/Repl.hs

@@ -375,7 +375,8 @@ runTransformations shouldDisambiguate ts n = runCoreInfoTableBuilderArtifacts $
                 _identifierArgsNum = 0,
                 _identifierType = Core.mkDynamic',
                 _identifierIsExported = False,
-                _identifierBuiltin = Nothing
+                _identifierBuiltin = Nothing,
+                _identifierPragmas = mempty
               }
       Core.registerIdent name idenInfo
       return sym

src/Juvix/Compiler/Abstract/Language.hs

@@ -30,7 +30,8 @@ type TopModuleName = Name
 data Module = Module
   { _moduleName :: Name,
     _moduleExamples :: [Example],
-    _moduleBody :: ModuleBody
+    _moduleBody :: ModuleBody,
+    _modulePragmas :: Pragmas
   }
   deriving stock (Eq, Show)
 
@@ -59,7 +60,8 @@ data FunctionDef = FunctionDef
     _funDefExamples :: [Example],
     _funDefClauses :: NonEmpty FunctionClause,
     _funDefBuiltin :: Maybe BuiltinFunction,
-    _funDefTerminating :: Bool
+    _funDefTerminating :: Bool,
+    _funDefPragmas :: Pragmas
   }
   deriving stock (Eq, Show)
 
@@ -194,21 +196,24 @@ data InductiveDef = InductiveDef
     _inductiveType :: Expression,
     _inductiveExamples :: [Example],
     _inductiveConstructors :: [InductiveConstructorDef],
-    _inductivePositive :: Bool
+    _inductivePositive :: Bool,
+    _inductivePragmas :: Pragmas
   }
   deriving stock (Eq, Show)
 
 data InductiveConstructorDef = InductiveConstructorDef
   { _constructorName :: ConstrName,
     _constructorExamples :: [Example],
-    _constructorType :: Expression
+    _constructorType :: Expression,
+    _constructorPragmas :: Pragmas
   }
   deriving stock (Eq, Show)
 
 data AxiomDef = AxiomDef
   { _axiomName :: AxiomName,
     _axiomBuiltin :: Maybe BuiltinAxiom,
-    _axiomType :: Expression
+    _axiomType :: Expression,
+    _axiomPragmas :: Pragmas
   }
   deriving stock (Eq, Show)
 

src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs

@@ -7,7 +7,6 @@ where
 import Data.HashMap.Strict qualified as HashMap
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Abstract.Data.InfoTableBuilder
-import Juvix.Compiler.Abstract.Language (FunctionDef (_funDefExamples))
 import Juvix.Compiler.Abstract.Language qualified as Abstract
 import Juvix.Compiler.Abstract.Translation.FromConcrete.Data.Context
 import Juvix.Compiler.Builtins
@@ -29,30 +28,34 @@ unsupported msg = error $ msg <> "Scoped to Abstract: not yet supported"
 fromConcrete :: (Members '[Error JuvixError, Builtins, NameIdGen] r) => Scoper.ScoperResult -> Sem r AbstractResult
 fromConcrete _resultScoper =
   mapError (JuvixError @ScoperError) $ do
-    (_resultTable, _resultModules) <- runInfoTableBuilder (evalState (ModulesCache mempty) (mapM goTopModule ms))
+    (_resultTable, _resultModules) <-
+      runInfoTableBuilder $
+        runReader @Pragmas mempty $
+          evalState (ModulesCache mempty) $
+            mapM goTopModule ms
     let _resultExports = _resultScoper ^. Scoper.resultExports
     return AbstractResult {..}
   where
     ms = _resultScoper ^. Scoper.resultModules
 
 fromConcreteExpression :: (Members '[Error JuvixError, NameIdGen] r) => Scoper.Expression -> Sem r Abstract.Expression
-fromConcreteExpression = mapError (JuvixError @ScoperError) . ignoreInfoTableBuilder . goExpression
+fromConcreteExpression = mapError (JuvixError @ScoperError) . ignoreInfoTableBuilder . runReader @Pragmas mempty . goExpression
 
 goTopModule ::
-  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r) =>
+  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
   Module 'Scoped 'ModuleTop ->
   Sem r Abstract.TopModule
 goTopModule = goModule
 
 goLocalModule ::
-  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r) =>
+  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
   Module 'Scoped 'ModuleLocal ->
   Sem r Abstract.LocalModule
 goLocalModule = goModule
 
 goModule ::
   forall r t.
-  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r, SingI t) =>
+  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r, SingI t) =>
   Module 'Scoped t ->
   Sem r Abstract.Module
 goModule m = case sing :: SModuleIsTop t of
@@ -70,20 +73,27 @@ goModule m = case sing :: SModuleIsTop t of
   where
     goModule' :: Module 'Scoped t -> Sem r Abstract.Module
     goModule' Module {..} = do
-      body' <- goModuleBody _moduleBody
+      pragmas' <- goPragmas _modulePragmas
+      body' <- local (const pragmas') (goModuleBody _moduleBody)
       examples' <- goExamples _moduleDoc
       return
         Abstract.Module
           { _moduleName = name',
             _moduleBody = body',
-            _moduleExamples = examples'
+            _moduleExamples = examples',
+            _modulePragmas = pragmas'
           }
       where
         name' :: Abstract.Name
         name' = case sing :: SModuleIsTop t of
           SModuleTop -> goSymbol (S.topModulePathName _modulePath)
           SModuleLocal -> goSymbol _modulePath
 
+goPragmas :: Member (Reader Pragmas) r => Maybe ParsedPragmas -> Sem r Pragmas
+goPragmas p = do
+  p' <- ask
+  return $ p' <> p ^. _Just . withLocParam . withSourceValue
+
 goName :: S.Name -> Abstract.Name
 goName name =
   set Abstract.namePretty prettyStr (goSymbol (S.nameUnqualify name))
@@ -104,7 +114,7 @@ goSymbol s =
 
 goModuleBody ::
   forall r.
-  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r) =>
+  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
   [Statement 'Scoped] ->
   Sem r Abstract.ModuleBody
 goModuleBody ss' = do
@@ -138,7 +148,7 @@ goModuleBody ss' = do
 
 goStatement ::
   forall r.
-  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r) =>
+  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
   Indexed (Statement 'Scoped) ->
   Sem r (Maybe (Indexed Abstract.Statement))
 goStatement (Indexed idx s) =
@@ -154,7 +164,7 @@ goStatement (Indexed idx s) =
 
 goOpenModule ::
   forall r.
-  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache] r) =>
+  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
   OpenModule 'Scoped ->
   Sem r (Maybe Abstract.Statement)
 goOpenModule o
@@ -167,15 +177,15 @@ goOpenModule o
   | otherwise = return Nothing
 
 goLetFunctionDef ::
-  (Members '[InfoTableBuilder, Error ScoperError] r) =>
+  (Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError] r) =>
   TypeSignature 'Scoped ->
   [FunctionClause 'Scoped] ->
   Sem r Abstract.FunctionDef
 goLetFunctionDef = goFunctionDefHelper
 
 goFunctionDefHelper ::
   forall r.
-  (Members '[InfoTableBuilder, Error ScoperError] r) =>
+  (Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError] r) =>
   TypeSignature 'Scoped ->
   [FunctionClause 'Scoped] ->
   Sem r Abstract.FunctionDef
@@ -185,6 +195,7 @@ goFunctionDefHelper sig@TypeSignature {..} clauses = do
       _funDefBuiltin = (^. withLocParam) <$> _sigBuiltin
   _funDefTypeSig <- goExpression _sigType
   _funDefExamples <- goExamples _sigDoc
+  _funDefPragmas <- goPragmas _sigPragmas
   _funDefClauses <- case (_sigBody, nonEmpty clauses) of
     (Nothing, Nothing) -> throw (ErrLacksFunctionClause (LacksFunctionClause sig))
     (Just {}, Just clauses') -> throw (ErrDuplicateFunctionClause (DuplicateFunctionClause sig (head clauses')))
@@ -204,7 +215,7 @@ goFunctionDefHelper sig@TypeSignature {..} clauses = do
 
 goTopFunctionDef ::
   forall r.
-  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) =>
   TypeSignature 'Scoped ->
   [FunctionClause 'Scoped] ->
   Sem r Abstract.FunctionDef
@@ -215,7 +226,7 @@ goTopFunctionDef sig clauses = do
 
 goExamples ::
   forall r.
-  (Members '[Error ScoperError, InfoTableBuilder] r) =>
+  (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
   Maybe (Judoc 'Scoped) ->
   Sem r [Abstract.Example]
 goExamples = mapM goExample . maybe [] judocExamples
@@ -230,7 +241,7 @@ goExamples = mapM goExample . maybe [] judocExamples
           }
 
 goFunctionClause ::
-  (Members '[Error ScoperError, InfoTableBuilder] r) =>
+  (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
   FunctionClause 'Scoped ->
   Sem r Abstract.FunctionClause
 goFunctionClause FunctionClause {..} = do
@@ -244,7 +255,7 @@ goFunctionClause FunctionClause {..} = do
       }
 
 goInductiveParameters ::
-  (Members '[Error ScoperError, InfoTableBuilder] r) =>
+  (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
   InductiveParameters 'Scoped ->
   Sem r [Abstract.FunctionParameter]
 goInductiveParameters InductiveParameters {..} = do
@@ -325,13 +336,16 @@ registerBuiltinAxiom d = \case
   BuiltinIntPrint -> registerIntPrint d
 
 goInductive ::
-  (Members '[InfoTableBuilder, Builtins, Error ScoperError] r) =>
+  (Members '[InfoTableBuilder, Reader Pragmas, Builtins, Error ScoperError] r) =>
   InductiveDef 'Scoped ->
   Sem r Abstract.InductiveDef
 goInductive ty@InductiveDef {..} = do
   _inductiveParameters' <- concatMapM goInductiveParameters _inductiveParameters
   _inductiveType' <- mapM goExpression _inductiveType
-  _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors
+  _inductivePragmas' <- goPragmas _inductivePragmas
+  _inductiveConstructors' <-
+    local (const _inductivePragmas') $
+      mapM goConstructorDef _inductiveConstructors
   _inductiveExamples' <- goExamples _inductiveDoc
   let loc = getLoc _inductiveName
       indDef =
@@ -342,6 +356,7 @@ goInductive ty@InductiveDef {..} = do
             _inductiveType = fromMaybe (Abstract.ExpressionUniverse (smallUniverse loc)) _inductiveType',
             _inductiveConstructors = toList _inductiveConstructors',
             _inductiveExamples = _inductiveExamples',
+            _inductivePragmas = _inductivePragmas',
             _inductivePositive = isJust (ty ^. inductivePositive)
           }
   whenJust ((^. withLocParam) <$> _inductiveBuiltin) (registerBuiltinInductive indDef)
@@ -350,22 +365,24 @@ goInductive ty@InductiveDef {..} = do
   return (inductiveInfo ^. inductiveInfoDef)
 
 goConstructorDef ::
-  (Members [Error ScoperError, InfoTableBuilder] r) =>
+  (Members [Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
   InductiveConstructorDef 'Scoped ->
   Sem r Abstract.InductiveConstructorDef
 goConstructorDef InductiveConstructorDef {..} = do
   ty' <- goExpression _constructorType
   examples' <- goExamples _constructorDoc
+  pragmas' <- goPragmas _constructorPragmas
   return
     Abstract.InductiveConstructorDef
       { _constructorType = ty',
         _constructorExamples = examples',
-        _constructorName = goSymbol _constructorName
+        _constructorName = goSymbol _constructorName,
+        _constructorPragmas = pragmas'
       }
 
 goExpression ::
   forall r.
-  (Members [Error ScoperError, InfoTableBuilder] r) =>
+  (Members [Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
   Expression ->
   Sem r Abstract.Expression
 goExpression = \case
@@ -433,7 +450,7 @@ goExpression = \case
       r' <- goExpression r
       return (Abstract.Application l'' r' Explicit)
 
-goCase :: forall r. (Members '[Error ScoperError, InfoTableBuilder] r) => Case 'Scoped -> Sem r Abstract.Case
+goCase :: forall r. (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => Case 'Scoped -> Sem r Abstract.Case
 goCase c = do
   _caseExpression <- goExpression (c ^. caseExpression)
   _caseBranches <- mapM goBranch (c ^. caseBranches)
@@ -446,7 +463,7 @@ goCase c = do
       _caseBranchExpression <- goExpression (b ^. caseBranchExpression)
       return Abstract.CaseBranch {..}
 
-goLambda :: forall r. (Members '[Error ScoperError, InfoTableBuilder] r) => Lambda 'Scoped -> Sem r Abstract.Lambda
+goLambda :: forall r. (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => Lambda 'Scoped -> Sem r Abstract.Lambda
 goLambda l = Abstract.Lambda <$> mapM goClause (l ^. lambdaClauses)
   where
     goClause :: LambdaClause 'Scoped -> Sem r Abstract.LambdaClause
@@ -458,7 +475,7 @@ goLambda l = Abstract.Lambda <$> mapM goClause (l ^. lambdaClauses)
 goUniverse :: Universe -> Universe
 goUniverse = id
 
-goFunction :: (Members '[Error ScoperError, InfoTableBuilder] r) => Function 'Scoped -> Sem r Abstract.Function
+goFunction :: (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => Function 'Scoped -> Sem r Abstract.Function
 goFunction f = do
   params <- goFunctionParameters (f ^. funParameters)
   ret <- goExpression (f ^. funReturn)
@@ -467,7 +484,7 @@ goFunction f = do
       foldr (\param acc -> Abstract.ExpressionFunction $ Abstract.Function param acc) ret (NonEmpty.tail params)
 
 goFunctionParameters ::
-  (Members '[Error ScoperError, InfoTableBuilder] r) =>
+  (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
   FunctionParameters 'Scoped ->
   Sem r (NonEmpty Abstract.FunctionParameter)
 goFunctionParameters (FunctionParameters {..}) = do
@@ -553,14 +570,16 @@ goPattern p = case p of
   PatternWildcard i -> return (Abstract.PatternWildcard i)
   PatternEmpty {} -> return Abstract.PatternEmpty
 
-goAxiom :: (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef
+goAxiom :: (Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef
 goAxiom a = do
   _axiomType' <- goExpression (a ^. axiomType)
+  _axiomPragmas' <- goPragmas (a ^. axiomPragmas)
   let axiom =
         Abstract.AxiomDef
           { _axiomType = _axiomType',
             _axiomBuiltin = (^. withLocParam) <$> a ^. axiomBuiltin,
-            _axiomName = goSymbol (a ^. axiomName)
+            _axiomName = goSymbol (a ^. axiomName),
+            _axiomPragmas = _axiomPragmas'
           }
   whenJust (a ^. axiomBuiltin) (registerBuiltinAxiom axiom . (^. withLocParam))
   registerAxiom' axiom

src/Juvix/Compiler/Concrete/Data/ParsedInfoTableBuilder.hs

@@ -4,6 +4,7 @@ module Juvix.Compiler.Concrete.Data.ParsedInfoTableBuilder
     registerDelimiter,
     registerKeyword,
     registerJudocText,
+    registerPragmas,
     registerSpaceSpan,
     registerModule,
     moduleVisited,
@@ -55,6 +56,14 @@ registerJudocText i =
         _parsedTag = ParsedTagJudoc
       }
 
+registerPragmas :: Member InfoTableBuilder r => Interval -> Sem r ()
+registerPragmas i =
+  registerItem
+    ParsedItem
+      { _parsedLoc = i,
+        _parsedTag = ParsedTagComment
+      }
+
 registerLiteral :: Member InfoTableBuilder r => LiteralLoc -> Sem r LiteralLoc
 registerLiteral l =
   l