Added more ideas to implement

MiniJuvix.cabal

@@ -24,33 +24,34 @@ source-repository head
 
 library
     exposed-modules:
-        MiniJuvix.Pipeline
-        MiniJuvix.Error
+        -- MiniJuvix.Pipeline
+        -- MiniJuvix.Error
         MiniJuvix.Pretty
-        MiniJuvix.Monad
-        MiniJuvix.Parsing.ADT
-        MiniJuvix.Parsing.Parser
-        MiniJuvix.Parsing.Location
-        MiniJuvix.Parsing.Error
-        MiniJuvix.Desugaring.Error
-        MiniJuvix.Syntax.Sugared
-        MiniJuvix.Syntax.Desugared
+        -- MiniJuvix.Monad
+        -- MiniJuvix.Parsing.ADT
+        -- MiniJuvix.Parsing.Parser
+        -- MiniJuvix.Parsing.Location
+        -- MiniJuvix.Parsing.Error
+        -- MiniJuvix.Desugaring.Error
+        -- MiniJuvix.Syntax.Sugared
+        -- MiniJuvix.Syntax.Desugared
         MiniJuvix.Syntax.Core
         MiniJuvix.Syntax.Eval
         MiniJuvix.Utils.Prelude
         MiniJuvix.Utils.Pretty
-        MiniJuvix.Utils.Parser
-        MiniJuvix.Utils.Parser.Lexer
-        MiniJuvix.Utils.Parser.Token
-        MiniJuvix.Utils.NameSymbol
-        MiniJuvix.Utils.File
-        MiniJuvix.Utils.Monad
-        MiniJuvix.Typing
-        MiniJuvix.Typing.Coverage
-        MiniJuvix.Typing.Erasure
-        MiniJuvix.Typing.Scopechecking
-        MiniJuvix.Typing.Termination
+        -- MiniJuvix.Utils.Parser
+        -- MiniJuvix.Utils.Parser.Lexer
+        -- MiniJuvix.Utils.Parser.Token
+        -- MiniJuvix.Utils.NameSymbol
+        -- MiniJuvix.Utils.File
+        -- MiniJuvix.Utils.Monad
+        -- MiniJuvix.Typing
+        -- MiniJuvix.Typing.Coverage
+        -- MiniJuvix.Typing.Erasure
+        -- MiniJuvix.Typing.Scopechecking
+        -- MiniJuvix.Typing.Termination
         MiniJuvix.Typing.Typechecking
+        MiniJuvix.Typing.Utils
         MiniJuvix.Typing.Error
 
 

src/MiniJuvix/Desugaring/Error.hs

@@ -1,3 +1,5 @@
 module MiniJuvix.Desugaring.Error where
 
-data DesugaringError
+--------------------------------------------------------------------------------
+
+data DesugaringError

src/MiniJuvix/Error.hs

@@ -8,9 +8,9 @@ where
 
 import MiniJuvix.Desugaring.Error (DesugaringError)
 import MiniJuvix.Parsing.Error (ParsingError)
+import MiniJuvix.Pretty
 import MiniJuvix.Typing.Error (TypingError (..))
 import MiniJuvix.Utils.Prelude
-import MiniJuvix.Pretty
 
 --------------------------------------------------------------------------------
 
@@ -38,7 +38,6 @@ type Loc = (String, Row, Col)
 newtype ErrorLocation = ErrorLocation (Maybe (Loc, Loc))
   deriving stock (Eq, Ord, Show)
 
-
 {- TODO: I don't know yet how to deal with scope. But the errors
 should be printed with some information about the enviroment.
 -}
@@ -47,17 +46,19 @@ data Scope
 --------------------------------------------------------------------------------
 
 type ErrorDescription = Text
+
 type ErrorScope = Maybe Scope
 
-data Error = Error
-  { _errorType :: ErrorType,
-    _errorLoc :: ErrorLocation,
-    _errorText :: ErrorDescription,
-    _errorParentScopes :: [ErrorScope]
-  }
+data Error
+  = Error
+      { _errorType :: ErrorType,
+        _errorLoc :: ErrorLocation,
+        _errorText :: ErrorDescription,
+        _errorParentScopes :: [ErrorScope]
+      }
   deriving stock (Eq, Show)
 
 --------------------------------------------------------------------------------
 
 logErrs :: Set Error -> IO ()
-logErrs = printList . L.sort  . S.toList
+logErrs = printList . L.sort . S.toList

src/MiniJuvix/Monad.hs

@@ -1,12 +1,9 @@
 module MiniJuvix.Monad where
 
-
-newtype MiniJuvixT e r s m a 
+newtype MiniJuvixT e r s m a
   = MiniJuvixT {unMgT :: E.ExceptT e (R.ReaderT r (St.StateT s m)) a}
   deriving (Functor, Applicative, Monad)
 
 instance MonadIO m => MonadIO (MiniJuvixT e r s m) where
   liftIO = MiniJuvixT . liftIO
-
-
--- type MiniJuvix = MiniJuvixT () [Name] (S.Set Err) IO
+-- type MiniJuvix = MiniJuvixT () [Name] (S.Set Err) IO

src/MiniJuvix/Parsing/ADT.hs

@@ -1,8 +1,8 @@
--- | Adapted from https://github.com/heliaxdev/juvix/
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 
+-- | Adapted from https://github.com/heliaxdev/juvix/
 module MiniJuvix.Parsing.ADT where
 
 --------------------------------------------------------------------------------
@@ -12,6 +12,7 @@ import qualified Data.Aeson as A
 --------------------------------------------------------------------------------
 
 type ConstructorName = NameSymb
+
 type NameSymb = NonEmpty Symbol
 
 type ModuleName = NameSymb
@@ -47,14 +48,15 @@ data InfixDeclar
 -- Types
 --------------------------------------------------------------------------------
 
-data Type = Typ
-  -- Was a usage but can't alias for now
-  { typeUsage :: Maybe Expression,
-    typeName' :: !Symbol,
-    typeArgs :: [Symbol],
-    typeForm :: Data
-    -- TODO: To support Empty type this should be 'Maybe Data'
-  }
+data Type
+  = Typ
+      -- Was a usage but can't alias for now
+      { typeUsage :: Maybe Expression,
+        typeName' :: !Symbol,
+        typeArgs :: [Symbol],
+        typeForm :: Data
+        -- TODO: To support Empty type this should be 'Maybe Data'
+      }
   deriving (Show, Read, Eq, Generic)
 
 -- | 'Data' is the data declaration in the Juvix language
@@ -72,17 +74,19 @@ data Data
 -- Arrows
 --------------------------------------------------------------------------------
 
-data NamedType = NamedType'
-  { nameRefineName :: !Name,
-    namedRefineRefine :: Expression
-  }
+data NamedType
+  = NamedType'
+      { nameRefineName :: !Name,
+        namedRefineRefine :: Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
 -- TODO ∷ change TypeName to TypeNameModule
-data TypeRefine = TypeRefine
-  { typeRefineName :: Expression,
-    typeRefineRefinement :: Expression
-  }
+data TypeRefine
+  = TypeRefine
+      { typeRefineName :: Expression,
+        typeRefineRefinement :: Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
 --------------------------------------------------------------------------------
@@ -122,10 +126,11 @@ data Adt
   | Product Product
   deriving (Show, Read, Eq, Generic)
 
-data Sum = S
-  { sumConstructor :: !Symbol,
-    sumValue :: !(Maybe Product)
-  }
+data Sum
+  = S
+      { sumConstructor :: !Symbol,
+        sumValue :: !(Maybe Product)
+      }
   deriving (Show, Read, Eq, Generic)
 
 -- For when a product is without a sum only a record can apply a sum
@@ -136,27 +141,30 @@ data Product
   | ADTLike [Expression]
   deriving (Show, Read, Eq, Generic)
 
-data Record = Record''
-  { recordFields :: NonEmpty NameType,
-    recordFamilySignature :: Maybe Expression
-  }
+data Record
+  = Record''
+      { recordFields :: NonEmpty NameType,
+        recordFamilySignature :: Maybe Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
-data NameType = NameType'
-  { nameTypeSignature :: Expression,
-    nameTypeName :: !Name,
-    nameTypeUsage :: Maybe Expression
-  }
+data NameType
+  = NameType'
+      { nameTypeSignature :: Expression,
+        nameTypeName :: !Name,
+        nameTypeUsage :: Maybe Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
 --------------------------------------------------------------------------------
 -- Effect Handlers
 --------------------------------------------------------------------------------
 
-data Effect = Eff
-  { effName :: Symbol,
-    effOps :: [Signature]
-  }
+data Effect
+  = Eff
+      { effName :: Symbol,
+        effOps :: [Signature]
+      }
   deriving (Show, Read, Eq, Generic)
 
 data Operation = Op (FunctionLike Expression)
@@ -186,18 +194,20 @@ newtype Module
   = Mod (FunctionLike (NonEmpty TopLevel))
   deriving (Show, Read, Eq, Generic)
 
-data ModuleE = ModE
-  { moduleEBindings :: FunctionLike (NonEmpty TopLevel),
-    moduleEBody :: Expression
-  }
+data ModuleE
+  = ModE
+      { moduleEBindings :: FunctionLike (NonEmpty TopLevel),
+        moduleEBody :: Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
 -- 'FunctionLike' is the generic version for both modules and functions
-data FunctionLike a = Like
-  { functionLikedName :: Symbol,
-    functionLikeArgs :: [Arg],
-    functionLikeBody :: GuardBody a
-  }
+data FunctionLike a
+  = Like
+      { functionLikedName :: Symbol,
+        functionLikeArgs :: [Arg],
+        functionLikeBody :: GuardBody a
+      }
   deriving (Show, Read, Eq, Generic)
 
 -- 'GuardBody' determines if a form is a guard or a body
@@ -210,10 +220,11 @@ newtype ModuleOpen
   = Open ModuleName
   deriving (Show, Read, Eq, Generic)
 
-data ModuleOpenExpr = OpenExpress
-  { moduleOpenExprModuleN :: ModuleName,
-    moduleOpenExprExpr :: Expression
-  }
+data ModuleOpenExpr
+  = OpenExpress
+      { moduleOpenExprModuleN :: ModuleName,
+        moduleOpenExprExpr :: Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
 -- Very similar to name, but match instead of symbol
@@ -226,23 +237,25 @@ newtype Cond a
   = C (NonEmpty (CondLogic a))
   deriving (Show, Read, Eq, Generic)
 
-data CondLogic a = CondExpression
-  { condLogicPred :: Expression,
-    condLogicBody :: a
-  }
+data CondLogic a
+  = CondExpression
+      { condLogicPred :: Expression,
+        condLogicBody :: a
+      }
   deriving (Show, Read, Eq, Generic)
 
 --------------------------------------------------------------------------------
 -- Signatures
 --------------------------------------------------------------------------------
 
-data Signature = Sig
-  { signatureName :: Symbol,
-    -- Was a usage but can't alias for now
-    signatureUsage :: Maybe Expression,
-    signatureArrowType :: Expression,
-    signatureConstraints :: [Expression]
-  }
+data Signature
+  = Sig
+      { signatureName :: Symbol,
+        -- Was a usage but can't alias for now
+        signatureUsage :: Maybe Expression,
+        signatureArrowType :: Expression,
+        signatureConstraints :: [Expression]
+      }
   deriving (Show, Read, Eq, Generic)
 
 --------------------------------------------------------------------------------
@@ -296,12 +309,13 @@ data Tuple
   = TupleLit [Expression]
   deriving (Show, Read, Eq, Generic)
 
-data ArrowExp = Arr'
-  { arrowExpLeft :: Expression,
-    -- Was a usage but can't alias for now
-    arrowExpUsage :: Expression,
-    arrowExpRight :: Expression
-  }
+data ArrowExp
+  = Arr'
+      { arrowExpLeft :: Expression,
+        -- Was a usage but can't alias for now
+        arrowExpUsage :: Expression,
+        arrowExpRight :: Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
 data Constant
@@ -318,26 +332,30 @@ newtype String'
   = Sho Text
   deriving (Show, Read, Eq, Generic)
 
-newtype Block = Bloc
-  {blockExpr :: Expression}
+newtype Block
+  = Bloc
+      {blockExpr :: Expression}
   deriving (Show, Read, Eq, Generic)
 
-data Lambda = Lamb
-  { lambdaArgs :: NonEmpty MatchLogic,
-    lambdaBody :: Expression
-  }
+data Lambda
+  = Lamb
+      { lambdaArgs :: NonEmpty MatchLogic,
+        lambdaBody :: Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
-data Application = App
-  { applicationName :: Expression,
-    applicationArgs :: NonEmpty Expression
-  }
+data Application
+  = App
+      { applicationName :: Expression,
+        applicationArgs :: NonEmpty Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
-data EffApp = Via
-  { effappHand :: Expression,
-    effappArg :: Expression
-  }
+data EffApp
+  = Via
+      { effappHand :: Expression,
+        effappArg :: Expression
+      }
   deriving (Show, Read, Generic, Eq)
 
 -- Was a newtype but extensible adds fields
@@ -346,10 +364,11 @@ newtype Do
   deriving (Show, Read, Eq, Generic)
 
 -- promote this to a match!!!
-data DoBody = DoBody
-  { doBodyName :: Maybe Symbol,
-    doBodyExpr :: Computation -- computation as in effect
-  }
+data DoBody
+  = DoBody
+      { doBodyName :: Maybe Symbol,
+        doBodyExpr :: Computation -- computation as in effect
+      }
   deriving (Show, Read, Eq, Generic)
 
 data Computation
@@ -357,68 +376,77 @@ data Computation
   | DoPure DoPure
   deriving (Show, Read, Eq, Generic)
 
-data DoOp = DoOp'
-  { opName :: Expression,
-    opArgs :: NonEmpty Expression
-  }
+data DoOp
+  = DoOp'
+      { opName :: Expression,
+        opArgs :: NonEmpty Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
-data DoPure = DoPure'
-  { pureArg :: Expression
-  }
+data DoPure
+  = DoPure'
+      { pureArg :: Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
 -- TODO ∷ we need includes in here as well!
 -- Was a newtype but extensible adds fields
-newtype ExpRecord = ExpressionRecord
-  { expRecordFields :: NonEmpty (NameSet Expression)
-  }
+newtype ExpRecord
+  = ExpressionRecord
+      { expRecordFields :: NonEmpty (NameSet Expression)
+      }
   deriving (Show, Read, Eq, Generic)
 
 --------------------------------------------------------------------------------
 -- Symbol Binding
 --------------------------------------------------------------------------------
 
-data Let = Let'
-  { letBindings :: FunctionLike Expression,
-    letBody :: Expression
-  }
+data Let
+  = Let'
+      { letBindings :: FunctionLike Expression,
+        letBody :: Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
-data LetType = LetType''
-  { letTypeBindings :: Type,
-    letTypeBody :: Expression
-  }
+data LetType
+  = LetType''
+      { letTypeBindings :: Type,
+        letTypeBody :: Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
-data Infix = Inf
-  { infixLeft :: Expression,
-    infixOp :: NameSymb,
-    infixRight :: Expression
-  }
+data Infix
+  = Inf
+      { infixLeft :: Expression,
+        infixOp :: NameSymb,
+        infixRight :: Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
 --------------------------------------------------------------------------------
 -- Matching
 --------------------------------------------------------------------------------
 
-data Match = Match''
-  { matchOn :: Expression,
-    matchBindigns :: NonEmpty MatchL
-  }
+data Match
+  = Match''
+      { matchOn :: Expression,
+        matchBindigns :: NonEmpty MatchL
+      }
   deriving (Show, Read, Eq, Generic)
 
-data MatchL = MatchL
-  { matchLPattern :: MatchLogic,
-    matchLBody :: Expression
-  }
+data MatchL
+  = MatchL
+      { matchLPattern :: MatchLogic,
+        matchLBody :: Expression
+      }
   deriving (Show, Read, Eq, Generic)
 
 -- TODO ∷ add literals to the match
-data MatchLogic = MatchLogic
-  { matchLogicContents :: MatchLogicStart,
-    matchLogicNamed :: Maybe Symbol
-  }
+data MatchLogic
+  = MatchLogic
+      { matchLogicContents :: MatchLogicStart,
+        matchLogicNamed :: Maybe Symbol
+      }
   deriving (Show, Read, Eq, Generic)
 
 data MatchLogicStart

src/MiniJuvix/Parsing/Error.hs

@@ -1,15 +1,17 @@
 -- | Adapted from https://github.com/heliaxdev/juvix/
-module MiniJuvix.Parsing.Error 
-  (ParsingError
-  , Error)
-  where
+module MiniJuvix.Parsing.Error
+  ( ParsingError,
+    Error,
+  )
+where
 
 --------------------------------------------------------------------------------
 
 import MiniJuvix.Utils.Prelude
+
 --------------------------------------------------------------------------------
 
 data ParsingError
 
-data Error = NoHeaderErr FilePath | ParseError ParserError
-  deriving (Show)
+data Error = NoHeaderErr FilePath | ParseError ParsingError
+  deriving stock (Show)

src/MiniJuvix/Parsing/Location.hs

@@ -1,11 +1,10 @@
 -- | Adapted from https://github.com/heliaxdev/juvix/
-
 module MiniJuvix.Parsing.Location where
 
 --------------------------------------------------------------------------------
 
-import MiniJuvix.Utils.Prelude
 import MiniJuvix.Utils.Parser (Parser)
+import MiniJuvix.Utils.Prelude
 import qualified Text.Megaparsec as P
 
 --------------------------------------------------------------------------------

src/MiniJuvix/Parsing/Parser.hs

@@ -1,6 +1,6 @@
--- | Adapted from https://github.com/heliaxdev/juvix/
 {-# LANGUAGE ApplicativeDo #-}
 
+-- | Adapted from https://github.com/heliaxdev/juvix/
 module Juvix.Frontend.Parser
   ( parse,
     prettyParse,
@@ -318,8 +318,7 @@ nameSetMany' :: Parser a -> Parser (NonEmpty (Types.NameSet a))
 nameSetMany' parser =
   J.curly $ do
     x <- J.sepBy1H (nameSetSN parser) (skipLiner J.comma)
-    if
-        | length x == 1 && isPunned x ->
+    if  | length x == 1 && isPunned x ->
           x <$ skipLiner J.comma
         | otherwise ->
           x <$ P.optional (skipLiner J.comma)
@@ -449,9 +448,9 @@ product =
 record :: Parser Types.Record
 record = do
   names <-
-    spaceLiner $
-      J.curly $
-        J.sepBy1HFinal nameTypeSN (skipLiner J.comma)
+    spaceLiner
+      $ J.curly
+      $ J.sepBy1HFinal nameTypeSN (skipLiner J.comma)
   familySignature <- P.optional (skipLiner J.colon *> expression)
   pure (Types.Record'' names familySignature)
 
@@ -760,8 +759,7 @@ doPureParser = do
 infixSymbolGen :: Parser Symbol -> Parser Symbol
 infixSymbolGen p = do
   symb <- p
-  if
-      | Set.member symb J.reservedSymbols -> fail "symbol is reserved word"
+  if  | Set.member symb J.reservedSymbols -> fail "symbol is reserved word"
       | otherwise -> pure symb
 
 infixSymbolDot :: Parser (NonEmpty Symbol)
@@ -795,8 +793,7 @@ prefixSymbolGen startParser = do
   rest <- P.takeWhileP (Just "Valid Middle Symbol") J.validMiddleSymbol
   -- Slow O(n) call, could maybe peek ahead instead, then parse it all at once?
   let new = ByteString.cons start rest
-  if
-      | Set.member new J.reservedWords -> fail "symbol is reserved operator"
+  if  | Set.member new J.reservedWords -> fail "symbol is reserved operator"
       | otherwise -> pure (internText $ Encoding.decodeUtf8 new)
 
 symbolEndGen :: ByteString -> Parser ()
@@ -887,11 +884,11 @@ arrowExp =
 
 refine :: Expr.Operator Parser Types.Expression
 refine =
-  Expr.Postfix $
-    P.try $
-      do
-        refine <- spaceLiner (J.curly expressionSN)
-        pure (\p -> Types.RefinedE (Types.TypeRefine p refine))
+  Expr.Postfix
+    $ P.try
+    $ do
+      refine <- spaceLiner (J.curly expressionSN)
+      pure (\p -> Types.RefinedE (Types.TypeRefine p refine))
 
 -- For Do!
 table :: Semigroup a => [[Expr.Operator Parser a]]
@@ -1012,4 +1009,3 @@ parseSingleFile file = do
 _fileNameToModuleName :: FilePath -> NameSymbol.T
 _fileNameToModuleName =
   NameSymbol.fromSymbol . intern . toUpperFirst . FilePath.takeBaseName
-

src/MiniJuvix/Pipeline.hs

@@ -10,8 +10,6 @@ where
 
 --------------------------------------------------------------------------------
 
---------------------------------------------------------------------------------
-
 import MiniJuvix.Error
 import MiniJuvix.Utils.Prelude (Eq, FilePath, Maybe, Ord, Show, Text)
 
@@ -22,12 +20,13 @@ data CompilerMode
   | BuildMode Config FilePath
   | TestMode Config FilePath
 
-data Config = Config
-  { _configPass :: Pass,
-    _configBackend :: Backend,
-    _configOutputDirectory :: Maybe FilePath,
-    _configWriteToFsBehavior :: WriteToFsBehavior
-  }
+data Config
+  = Config
+      { _configPass :: Pass,
+        _configBackend :: Backend,
+        _configOutputDirectory :: Maybe FilePath,
+        _configWriteToFsBehavior :: WriteToFsBehavior
+      }
 
 data Pass
   = Parsing
@@ -40,13 +39,12 @@ data Backend = LLVM
   deriving (Eq, Ord, Show)
 
 data WriteToFsBehavior = OverwriteTargetFiles | WriteIfDoesNotExist
-
-runAndLogErrs :: MiniJuvix a -> IO ()
-runAndLogErrs m = runMiniJuvix m >>= \(_, errs) -> logErrs errs
+-- runAndLogErrs :: MiniJuvix a -> IO ()
+-- runAndLogErrs m = runMiniJuvix m >>= \(_, errs) -> logErrs errs
 
 -- runTestWith :: FilePath -> Config -> IO ()
 -- runTestWith filePath config = case _configPass config of
---   Parsing -> undefined 
+--   Parsing -> undefined
 --   Desugaring -> undefined
 --   Typechecking -> runAndLogErrs $ depAnalPass filePath >>= parsePass >>= checkPass
---   Compiling -> undefined
+--   Compiling -> undefined

src/MiniJuvix/Pretty.hs

@@ -1,36 +1,52 @@
-module MiniJuvix.Print 
-  (module MiniJuvix.Utils.Pretty
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module MiniJuvix.Pretty
+  ( module MiniJuvix.Utils.Pretty,
   )
-  where
+where
 
 --------------------------------------------------------------------------------
 
+import MiniJuvix.Syntax.Core
+import MiniJuvix.Syntax.Eval
+import MiniJuvix.Typing.Utils
+import MiniJuvix.Utils.Prelude
 import MiniJuvix.Utils.Pretty
+  ( Doc,
+    Pretty (..),
+    ascii,
+    color,
+    hardlines,
+    render,
+    unicode,
+  )
+import qualified MiniJuvix.Utils.Pretty as PP
+import qualified Prettyprinter.Render.Terminal as Term
 
 --------------------------------------------------------------------------------
 
 instance Pretty Text where
-  pretty = const PP.pretty
+  pretty = undefined -- const PP.pretty
 
 instance Pretty Int where
-  pretty = const PP.pretty
+  pretty = undefined -- const PP.pretty
 
 instance Pretty Quantity where
-  pretty _ Zero = annotate (Term.color Term.Magenta) (PP.pretty "0")
-  pretty _ One = annotate (Term.color Term.Magenta) (PP.pretty "1")
-  pretty b Many = annotateSpecialSymbol b ManyQuantitySymbol
+  pretty _ Zero = undefined --  annotate (Term.color Term.Magenta) (PP.pretty "0")
+  pretty _ One = undefined --  annotate (Term.color Term.Magenta) (PP.pretty "1")
+  pretty b Many = undefined --  annotateSpecialSymbol b ManyQuantitySymbol
 
 instance Pretty Relevance where
-  pretty _ Relevant = PP.pretty "!"
-  pretty _ Irrelevant = PP.pretty "-"
+  pretty _ Relevant = undefined -- PP.pretty "!"
+  pretty _ Irrelevant = undefined -- PP.pretty "-"
 
 instance Pretty Name where
-  pretty _ (Global n) = PP.pretty n
-  pretty _ (Local n _) = PP.pretty n
+  pretty _ (Global n) = undefined -- PP.pretty n
+  pretty _ (Local n _) = undefined -- PP.pretty n
 
 instance Pretty Variable where
-  pretty _ (Bound idx) = PP.pretty idx
-  pretty b (Free name) = pretty b name
+  pretty _ (Bound idx) = undefined -- PP.pretty idx
+  pretty b (Free name) = undefined -- pretty b name
 
 instance Pretty Term where
   pretty b (Checkable t) = pretty b t
@@ -66,4 +82,7 @@ instance Pretty Value where
   pretty _ = undefined
 
 instance Pretty Neutral where
-  pretty _ = undefined
+  pretty _ = undefined
+
+instance Pretty TypingEnv where
+  pretty _ = undefined

src/MiniJuvix/Syntax/Eval.agda

@@ -102,7 +102,6 @@ data Neutral where
 
 valueToTerm : Value → Term
 valueToTerm v = Checkable Unit -- TODO
-
 {-# COMPILE AGDA2HS valueToTerm #-}
 
 --------------------------------------------------------------------------------

src/MiniJuvix/Typing.hs

@@ -0,0 +1,3 @@
+module MiniJuvix.Typing where
+
+--------------------------------------------------------------------------------

src/MiniJuvix/Typing/Coverage.hs

@@ -1,3 +1,3 @@
 module MiniJuvix.Typing.Coverage () where
 
---------------------------------------------------------------------------------
+--------------------------------------------------------------------------------

src/MiniJuvix/Typing/Error.hs

@@ -1,17 +1,35 @@
-module MiniJuvix.Typing.Error 
-  (TypingError(..))
-  where
+module MiniJuvix.Typing.Error
+  ( Error (..),
+    CheckingError (..),
+    CommonError (..),
+  )
+where
 
 --------------------------------------------------------------------------------
 
--- Specific error related to an algorithm
+import MiniJuvix.Utils.Prelude
+
+--------------------------------------------------------------------------------
+
+data CommonError
+  = MissingVariable
+  | QuantityError
+  | UnknownError String
+
 data CheckingError
+  = ExpectUniverseType
+  | ExpectPiType
+  | ExpectTensorType
+  | ExpectSumType
+
+-- ! TODO add the other possible cases..
+
 data InferingError
+
 data ErasingError
 
-
-data TypingError
+data Error
   = CheckError CheckingError
   | InferError InferingError
   | ErasureError ErasingError
-  | UnknownTypingError
+  | CommonError

src/MiniJuvix/Typing/Scopechecking.hs

@@ -4,5 +4,3 @@ module MiniJuvix.Typing.Scopechecking
 where
 
 --------------------------------------------------------------------------------
-
---------------------------------------------------------------------------------

src/MiniJuvix/Typing/Termination.hs

@@ -1 +1,3 @@
 module MiniJuvix.Typing.Termination where
+
+--------------------------------------------------------------------------------

src/MiniJuvix/Typing/Typechecking.hs

@@ -1,5 +1,52 @@
-module MiniJuvix.Typing.Typechecking where
-  
--- check 
+module MiniJuvix.Typing.Typechecking () where
 
--- infer 
+--------------------------------------------------------------------------------
+
+import MiniJuvix.Syntax.Core
+import MiniJuvix.Syntax.Eval
+import MiniJuvix.Typing.Error
+import MiniJuvix.Typing.Utils (Binding, Quantities, TypingContext, TypingContextM)
+import MiniJuvix.Utils.Prelude
+
+--------------------------------------------------------------------------------
+
+type TypingResult = Either Error
+
+{- Let's try to have support Andy's notation. Γ |-  (x :q M) -| Δ
+   where Γ is the given context, x is a variable of quantity q of type
+   M, and Δ is the leftovers of quantities for each variable in Γ.
+-}
+
+type LeftOvers = Quantities
+
+type Judgment = TypingContextM TypingResult LeftOvers
+
+-- This should be equivalent to have 0Γ.
+type ZeroJudgment = TypingContextM TypingResult ()
+
+extendLocalContext :: String -> Binding -> Judgment -> Judgment
+extendLocalContext = undefined
+
+type Type = Value
+
+--------------------------------------------------------------------------------
+-- Type checking
+--------------------------------------------------------------------------------
+
+check :: Relevance -> Term -> Type -> TypingResult (Type, LeftOvers)
+check = undefined
+
+check' :: Relevance -> CheckableTerm -> Type -> TypingResult (Type, LeftOvers)
+check' = undefined
+
+--------------------------------------------------------------------------------
+-- Type inference
+--------------------------------------------------------------------------------
+
+-- | infer the type of a term and check that context has appropriate
+-- resources available for the term.
+infer :: TypingContext -> Quantity -> Term -> TypingResult (Type, LeftOvers)
+infer = undefined
+
+infer' :: TypingContext -> Quantity -> InferableTerm -> TypingResult (Type, LeftOvers)
+infer' = undefined

src/MiniJuvix/Typing/Utils.hs

@@ -0,0 +1,64 @@
+module MiniJuvix.Typing.Utils
+  ( Binding (..),
+    Context,
+    TypingContextM,
+    weakenGlobal,
+    weakenLocal,
+    Quantities,
+    checkResources,
+    TypingContext (..),
+  )
+where
+
+--------------------------------------------------------------------------------
+
+import MiniJuvix.Syntax.Core (Name, Quantity)
+import MiniJuvix.Syntax.Eval (Value)
+import MiniJuvix.Utils.Prelude
+import qualified MiniJuvix.Utils.Prelude as Map
+
+--------------------------------------------------------------------------------
+
+{-
+  Γ  ⊢ let Δ in (x :^q M)
+
+  On the left side of the turnstile, we have the global context (Γ).
+  On the right side of the turnstile, we have the local context (Δ). A
+  context, regardless its kind, consists of triples, each consisting
+  of a variable, its quantity, and its type.
+-}
+
+data Binding
+  = Binding
+      { varName :: Name,
+        varQuantity :: Quantity,
+        varType :: Value
+      }
+
+type Context = [Binding]
+
+data TypingContext
+  = TypingContext
+      { globalEnv :: Context,
+        localEnv :: Context
+      }
+
+type TypingContextM = ReaderT TypingContext
+
+weakenGlobal :: Binding -> TypingContext -> TypingContext
+weakenGlobal var ctxt = ctxt {globalEnv = var : globalEnv ctxt}
+
+weakenLocal :: Binding -> TypingContext -> TypingContext
+weakenLocal var ctxt = ctxt {localEnv = var : localEnv ctxt}
+
+-- a.k.a. Resources
+type Quantities = Map.Map Name Quantity
+
+checkResources ::
+  Context ->
+  Quantity ->
+  Maybe [(Binding, Quantity)]
+checkResources = undefined
+
+mergeResources :: Quantities -> Quantities -> Quantities
+mergeResources = undefined

src/MiniJuvix/Utils/NameSymbol.hs

@@ -1,8 +1,7 @@
-module MiniJuvix.Utils.NameSymbol 
-  (
-    fromString
+module MiniJuvix.Utils.NameSymbol
+  ( fromString,
   )
-  where
+where
 
 --------------------------------------------------------------------------------
 -- Adapted from https://github.com/heliaxdev/juvix/library/StandardLibrary
@@ -11,9 +10,10 @@ module MiniJuvix.Utils.NameSymbol
 -- import Data.String (IsString (..))
 -- import qualified Data.Text as Text
 
-import MiniJuvix.Utils.Prelude
 import qualified MiniJuvix.Utils.Parser.Token as Tok
+import MiniJuvix.Utils.Prelude
 import qualified MiniJuvix.Utils.Pretty as PP
+
 -- import qualified Prelude (foldr1)
 
 --------------------------------------------------------------------------------
@@ -141,4 +141,4 @@ type instance PP.Ann T = ()
 instance PP.PrettySyntax T
 
 instance PP.PrettyText T where
-  prettyT = PP.text . textify . toSymbol
+  prettyT = PP.text . textify . toSymbol

src/MiniJuvix/Utils/Parser.hs

@@ -1,7 +1,8 @@
 module MiniJuvix.Utils.Parser
-  (Parser
-  , ParserError)
-  where
+  ( Parser,
+    ParserError,
+  )
+where
 
 import Protolude
 import qualified Text.Megaparsec as P

src/MiniJuvix/Utils/Parser/Lexer.hs

@@ -1,5 +1,4 @@
 -- | Adapted from https://github.com/heliaxdev/juvix/
-
 module MiniJuvix.Utils.Parser.Lexer
   ( spacer,
     spaceLiner,

src/MiniJuvix/Utils/Pretty.hs

@@ -6,15 +6,14 @@ module MiniJuvix.Utils.Pretty
     color,
     render,
     hardlines,
+    format,
+    annotateSpecialSymbol,
+    printList,
   )
 where
 
 --------------------------------------------------------------------------------
 
---------------------------------------------------------------------------------
-
-import MiniJuvix.Syntax.Core
-import MiniJuvix.Syntax.Eval
 import MiniJuvix.Utils.Prelude
 import Prettyprinter hiding
   ( Doc,
@@ -26,6 +25,7 @@ import qualified Prettyprinter.Render.Terminal as Term
 --------------------------------------------------------------------------------
 -- See https://hackage.haskell.org/package/prettyprinter-1.7.1/docs/Prettyprinter.html
 --     https://hackage.haskell.org/package/prettyprinter-ansi-terminal
+-- to know why we decide to have the def. below.
 
 type Doc = PP.Doc Term.AnsiStyle
 
@@ -114,6 +114,3 @@ annotateSpecialSymbol b s = annotate (Term.color (color s)) (format b s)
 
 class Pretty a where
   pretty :: Bool -> a -> Doc
-
-printList :: Pretty a => [a] -> IO ()
-printList = printDoc . vsep . punctuate line . map p