[ Juvix.Parser w.i.p ] fixing cabal compilation.

.hlint.yaml

@@ -8,7 +8,7 @@
 
 - extensions:
   - default: false
-  - name: [DeriveFunctor, OverloadedStrings]
+  - name: [DeriveFunctor, GeneralizedNewtypeDeriving, OverloadedStrings]
   - name: [MultiWayIf, PatternGuards, RecordWildCards]
   - name: [ScopedTypeVariables]
   - name: [ConstraintKinds, RankNTypes, TypeFamilies]
@@ -16,7 +16,7 @@
 
 - flags:
   - default: false
-  - {name: [-Wno-incomplete-patterns, -Wno-overlapping-patterns]}
+  - {name: [-Wno-incomplete-patterns, -Wno-overlapping-patterns , Wno-partial-fields]}
 
 - modules:
   # if you import Data.Set qualified, it must be as 'Set'
@@ -52,5 +52,6 @@
 # --------------------------------------------------------------------------------
 
 - ignore: {within: [MiniJuvix.Syntax.Core, MiniJuvix.Syntax.Eval]}
+- ignore: {within: [MiniJuvix.Pretty]}
 - ignore: {name: Use let, within: [Test.All]}
 - ignore: {name: Use String}

MiniJuvix.cabal

@@ -24,43 +24,20 @@ source-repository head
 
 library
     exposed-modules:
-        -- 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.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.Typing.Typechecking
-        MiniJuvix.Typing.Utils
-        MiniJuvix.Typing.Error
-
+        MiniJuvix.Utils.Parser
+        MiniJuvix.Parsing.Error
+        MiniJuvix.Parsing.Location
 
     hs-source-dirs:     src
     other-modules:      Paths_MiniJuvix
     default-language:   Haskell2010
     default-extensions:
-        NoImplicitPrelude DerivingStrategies StandaloneDeriving
-        MultiParamTypeClasses
+        NoImplicitPrelude Safe DerivingStrategies StandaloneDeriving
+        MultiParamTypeClasses OverloadedStrings
 
     ghc-options:
         -Wall -Wcompat -Widentities -Wincomplete-uni-patterns
@@ -70,15 +47,18 @@ library
     build-depends:
         aeson >=2.0 && <=2.1,
         base >=4.14 && <=4.16,
+        bytestring >=0.11 && <=0.12,
+        capability >=0.5 && <=0.6,
+        containers >=0.6 && <=0.7,
         filepath >=1.4 && <=1.5,
         megaparsec >=9.2 && <=9.3,
         prettyprinter >=1.7 && <=1.8,
         prettyprinter-ansi-terminal >=1.1 && <=1.2,
         process >=1.6 && <=1.7,
-        protolude >=0.3 && <=0.4,
+        relude >=1.0 && <=1.1,
         semirings >=0.6 && <=0.7,
-        text >=1.2 && <=1.3,
-        unordered-containers >=0.2 && <=0.3
+        unordered-containers >=0.2 && <=0.3,
+        word8 >=0.1 && <=0.2
 
     if impl(ghc >=8.0)
         ghc-options: -Wredundant-constraints
@@ -101,9 +81,7 @@ executable MiniJuvix
         -Wincomplete-record-updates -threaded -rtsopts -with-rtsopts=-N
         -fwrite-ide-info -hiedir=.hie
 
-    build-depends:
-        base >=4.14 && <=4.16,
-        optparse-applicative >=0.16 && <=0.17
+    build-depends:    base >=4.14 && <=4.16
 
     if impl(ghc >=8.0)
         ghc-options: -Wredundant-constraints
@@ -126,9 +104,7 @@ test-suite MiniJuvix-test
         -Wall -Wcompat -Widentities -Wincomplete-uni-patterns
         -Wincomplete-record-updates -threaded -rtsopts -with-rtsopts=-N
 
-    build-depends:
-        base >=4.14 && <=4.16,
-        MiniJuvix -any
+    build-depends:    MiniJuvix -any
 
     if impl(ghc >=8.0)
         ghc-options: -Wredundant-constraints

notes/README.md

@@ -1,12 +1,20 @@
 Tools used so far:
 
 - cabal-edit
-- hlint
+- hlint and checkout
+  https://github.com/kowainik/relude/blob/main/.hlint.yaml for a
+  complex configuration and better hints.
 - stan
 - summoner
 - ghcup
 - `implicit-hie` generates `hie.yaml`.
 
+- For a good prelude, I tried with Protolude, but it seems a bit
+  abandoned, and it doesn't have support the new Haskell versions.
+  Relude just offered the same, and it is better documented. Let us
+  give it a shot. NoImplicitPrelude plus base-noprelude.
+  https://kowainik.github.io/projects/relude
+
 - For Pretty printer, we will use the package
   https://hackage.haskell.org/package/prettyprinter, which supports
   nice annotations and colors using Ansi-terminal subpackage:
@@ -23,8 +31,10 @@ Tools used so far:
   During elaboration different kind of evaluation strategies may be
   needed.
     - top vs. local scope. 
-- On equality type-checking, see [abstract](https://github.com/anjapetkovic/anjapetkovic.github.io/blob/master/talks/2021-06-17-TYPES2021/abstract.pdf)
-- To document the code, see https://kowainik.github.io/posts/haddock-tips
+- On equality type-checking, see
+  [abstract](https://github.com/anjapetkovic/anjapetkovic.github.io/blob/master/talks/2021-06-17-TYPES2021/abstract.pdf)
+- To document the code, see
+  https://kowainik.github.io/posts/haddock-tips
 
 Initial task order for Minijuvix indicated between parenthesis:
 1. Parser (3.)
@@ -34,8 +44,29 @@ Initial task order for Minijuvix indicated between parenthesis:
 
 - On deriving stuff using Standalone Der.
 See https://kowainik.github.io/posts/deriving.
-- To avoid boilerplate in the cabal file, one could use [common stanzas](https://vrom911.github.io/blog/common-stanzas). At the moment, I'm using cabal-edit to keep the bounds and this tool does not support stanzas. So be it.
+- To avoid boilerplate in the cabal file, one could use [common
+  stanzas](https://vrom911.github.io/blog/common-stanzas). At the
+  moment, I'm using cabal-edit to keep the bounds and this tool does
+  not support stanzas. So be it.
+
 - Using MultiParamTypeClasses to allow me deriving multi instances in one line. 
 
-- TODO: make a `ref.bib` listing all the repositories and the source-code from where I took code,
-inspiration, whatever thing.
+- TODO: make a `ref.bib` listing all the repositories and the
+  source-code from where I took code, inspiration, whatever thing.
+
+- The haskell library https://hackage.haskell.org/package/capability
+  seems to be a right choice. Still, I need to check the details. I
+  will use Juvix Prelude.
+
+- Let us use qualified imports to prevent namespace pollution,
+  as much as possible. Checkout:
+  - https://www.haskell.org/onlinereport/haskell2010/haskellch5.html
+  - https://ro-che.info/articles/2019-01-26-haskell-module-system-p2
+  - https://mmhaskell.com/blog/2017/5/8/4-steps-to-a-better-imports-list.
+
+- TODO: https://kowainik.github.io/posts/2018-09-09-dhall-to-hlint So
+  far, I have proposed a hlint file, it's clean, but for refactoring,
+  seems to me, the link above shows a better approach.
+
+- Let us use the Safe pragma.
+  https://stackoverflow.com/questions/61655158/haskell-safe-and-trustworthy-extensions

src/MiniJuvix/Error.hs

@@ -7,7 +7,7 @@ where
 --------------------------------------------------------------------------------
 
 import MiniJuvix.Desugaring.Error (DesugaringError)
-import MiniJuvix.Parsing.Error (ParsingError)
+import MiniJuvix.Parsing.Error
 import MiniJuvix.Pretty
 import MiniJuvix.Typing.Error (TypingError (..))
 import MiniJuvix.Utils.Prelude
@@ -49,16 +49,15 @@ 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
+printErrors :: Set Error -> IO ()
+printErrors = printList . L.sort . S.toList

src/MiniJuvix/Monad.hs

@@ -1,9 +1,54 @@
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
 module MiniJuvix.Monad where
 
+--------------------------------------------------------------------------------
+
+import MiniJuvix.Utils.Prelude
+import qualified MiniJuvix.Utils.Prelude.Set as S
+
+--------------------------------------------------------------------------------
+
 newtype MiniJuvixT e r s m a
-  = MiniJuvixT {unMgT :: E.ExceptT e (R.ReaderT r (St.StateT s m)) a}
-  deriving (Functor, Applicative, Monad)
+  = MiniJuvixT {unMgT :: ExceptT e (ReaderT r (StateT s m)) a}
+  deriving anyclass (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] (Set Error) IO
+
+runMiniJuvixT :: MiniJuvixT e r s m a -> r -> s -> m (Either e a, s)
+runMiniJuvixT mgm r s =
+  (`St.runStateT` s) . (`R.runReaderT` r) . E.runExceptT $ unMgT mgm
+
+runMiniJuvix :: MiniJuvix a -> IO (Either () a, S.Set Err)
+runMiniJuvix m = runMiniJuvixT m [] S.empty
+
+-- -- | Retrieves the state within a MiniJuvixT.
+-- get :: Monad m => MiniJuvixT e r s m s
+-- get = MiniJuvixT (lift (lift St.get))
+
+-- -- | Modifies the state within a MiniJuvixT using the provided function.
+-- modify :: Monad m => (s -> s) -> MiniJuvixT e r s m ()
+-- modify f = MiniJuvixT (lift (lift (St.modify f)))
+
+-- -- | Throws an exception within a MiniJuvixT.
+-- throwE :: Monad m => e -> MiniJuvixT e s r m a
+-- throwE = MiniJuvixT . E.throwE
+
+-- -- | Catches an exception within a MiniJuvixT.
+-- catchE ::
+--   Monad m =>
+--   MiniJuvixT e r s m a ->
+--   (e -> MiniJuvixT e r s m a) ->
+--   MiniJuvixT e r s m a
+-- catchE me f = MiniJuvixT (unMgT me `E.catchE` (unMgT . f))
+
+-- -- | Retrieves the environment within a MiniJuvixT.
+-- ask :: Monad m => MiniJuvixT e r s m r
+-- ask = MiniJuvixT (lift R.ask)

src/MiniJuvix/Parsing/ADT.hs

@@ -1,467 +1,468 @@
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE UndecidableInstances #-}
+-- {-# LANGUAGE DeriveAnyClass #-}
+-- {-# LANGUAGE TypeFamilies #-}
+-- {-# LANGUAGE UndecidableInstances #-}
 
--- | Adapted from https://github.com/heliaxdev/juvix/
+-- |  Adapted from heliaxdev/Juvix/library/StandardLibrary/src/Juvix/
 module MiniJuvix.Parsing.ADT where
 
 --------------------------------------------------------------------------------
 
-import qualified Data.Aeson as A
+-- import qualified Data.Aeson as A
+import MiniJuvix.Utils.Prelude
 
 --------------------------------------------------------------------------------
 
-type ConstructorName = NameSymb
-
-type NameSymb = NonEmpty Symbol
-
-type ModuleName = NameSymb
-
-data TopLevel
-  = Type Type
-  | ModuleOpen ModuleOpen
-  | Signature Signature
-  | Module Module
-  | Function Function
-  | Effect Effect
-  | Handler Handler
-  | Declaration Declaration
-  | TypeClass
-  | TypeClassInstance
-  deriving (Show, Read, Eq, Generic)
-
---------------------------------------------------------------------------------
--- Declarations
---------------------------------------------------------------------------------
-
-newtype Declaration
-  = Infixivity InfixDeclar
-  deriving (Show, Read, Eq, Generic)
-
-data InfixDeclar
-  = NonAssoc Symbol Natural
-  | AssocL Symbol Natural
-  | AssocR Symbol Natural
-  deriving (Show, Read, Eq, Generic)
-
---------------------------------------------------------------------------------
--- 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'
-      }
-  deriving (Show, Read, Eq, Generic)
-
--- | 'Data' is the data declaration in the Juvix language
-data Data
-  = Arrowed
-      { dataArrow :: Expression,
-        dataAdt' :: Adt
-      }
-  | NonArrowed
-      { dataAdt :: Adt
-      }
-  deriving (Show, Read, Eq, Generic)
-
---------------------------------------------------------------------------------
--- Arrows
---------------------------------------------------------------------------------
-
-data NamedType
-  = NamedType'
-      { nameRefineName :: !Name,
-        namedRefineRefine :: Expression
-      }
-  deriving (Show, Read, Eq, Generic)
-
--- TODO ∷ change TypeName to TypeNameModule
-data TypeRefine
-  = TypeRefine
-      { typeRefineName :: Expression,
-        typeRefineRefinement :: Expression
-      }
-  deriving (Show, Read, Eq, Generic)
-
---------------------------------------------------------------------------------
--- Types Misc
---------------------------------------------------------------------------------
-
-data Name
-  = Implicit !Symbol
-  | Concrete !Symbol
-  deriving (Show, Read, Eq, Generic)
-
-data ArrowSymbol
-  = ArrowUse Usage.T
-  | -- Was a usage but can't alias for now
-    ArrowExp Expression
-  deriving (Show, Read, Eq, Generic)
-
--- TODO ∷ finish this type!
-newtype UniverseExpression
-  = UniverseExpression Symbol
-  deriving (Show, Read, Eq, Generic)
-
---------------------------------------------------------------------------------
--- ADTs
---------------------------------------------------------------------------------
-
--- The types for ADT are not the most constraining, however are setup
--- to have the least amount of boilerplate in the latter stages as
--- possible a Sum of length one should not have a record
--- [type Address = Foo {abc : Int}]
--- this form should be considered illegal unless we wish to permit
--- named records along with unnamed records. Ι suspect in the future
--- this will instead be used for Enum Subsets with refined information
-
-data Adt
-  = Sum (NonEmpty Sum)
-  | Product Product
-  deriving (Show, Read, Eq, Generic)
-
-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
--- of only one is a named product
-data Product
-  = Record !Record
-  | Arrow Expression
-  | ADTLike [Expression]
-  deriving (Show, Read, Eq, Generic)
-
-data Record
-  = Record''
-      { recordFields :: NonEmpty NameType,
-        recordFamilySignature :: Maybe Expression
-      }
-  deriving (Show, Read, Eq, Generic)
-
-data NameType
-  = NameType'
-      { nameTypeSignature :: Expression,
-        nameTypeName :: !Name,
-        nameTypeUsage :: Maybe Expression
-      }
-  deriving (Show, Read, Eq, Generic)
-
---------------------------------------------------------------------------------
--- Effect Handlers
---------------------------------------------------------------------------------
-
-data Effect
-  = Eff
-      { effName :: Symbol,
-        effOps :: [Signature]
-      }
-  deriving (Show, Read, Eq, Generic)
-
-data Operation = Op (FunctionLike Expression)
-  deriving (Show, Read, Eq, Generic)
-
---  A 'Handler', as implemented here, is a set of functions that implement
--- (at least) one `Effect` interface.
--- However, Handlers are NOT scoped, meaning that they can't be defined
--- defined within another function. We CAN fix that, but it requires
--- us to make some choices, it's wise to have Witch up and running first.
-data Handler
-  = Hand Symbol [Operation]
-  deriving (Show, Read, Eq, Generic)
-
---------------------------------------------------------------------------------
--- Functions and Modules
---------------------------------------------------------------------------------
-
--- | 'Function' is a normal signature with a name arguments and a body
--- that may or may not have a guard before it
-newtype Function
-  = Func (FunctionLike Expression)
-  deriving (Show, Read, Eq, Generic)
-
--- 'Module' is like function, however it allows multiple top levels
-newtype Module
-  = Mod (FunctionLike (NonEmpty TopLevel))
-  deriving (Show, Read, Eq, Generic)
-
-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
-      }
-  deriving (Show, Read, Eq, Generic)
-
--- 'GuardBody' determines if a form is a guard or a body
-data GuardBody a
-  = Body a
-  | Guard (Cond a)
-  deriving (Show, Read, Eq, Generic)
-
-newtype ModuleOpen
-  = Open ModuleName
-  deriving (Show, Read, Eq, Generic)
-
-data ModuleOpenExpr
-  = OpenExpress
-      { moduleOpenExprModuleN :: ModuleName,
-        moduleOpenExprExpr :: Expression
-      }
-  deriving (Show, Read, Eq, Generic)
-
--- Very similar to name, but match instead of symbol
-data Arg
-  = ImplicitA MatchLogic
-  | ConcreteA MatchLogic
-  deriving (Show, Read, Eq, Generic)
-
-newtype Cond a
-  = C (NonEmpty (CondLogic a))
-  deriving (Show, Read, Eq, Generic)
-
-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]
-      }
-  deriving (Show, Read, Eq, Generic)
-
---------------------------------------------------------------------------------
--- Expression
---------------------------------------------------------------------------------
-
--- TODO ∷ add <expression> : <expression> <refine>?
--- to the parser
-data Expression
-  = Cond (Cond Expression)
-  | Constant Constant
-  | Let Let
-  | ModuleE ModuleE
-  | LetType LetType
-  | Match Match
-  | Name NameSymb
-  | OpenExpr ModuleOpenExpr
-  | Lambda Lambda
-  | Application Application
-  | Primitive Primitive
-  | List List
-  | Tuple Tuple
-  | Block Block
-  | Infix Infix
-  | ExpRecord ExpRecord
-  | RecordDec Record
-  | Do Do
-  | EffApp EffApp
-  | -- Added due to merge
-    ArrowE ArrowExp
-  | NamedTypeE NamedType
-  | RefinedE TypeRefine
-  | UniverseName UniverseExpression
-  | Parened Expression
-  | DeclarationE DeclarationExpression
-  deriving (Show, Read, Eq, Generic)
-
-data DeclarationExpression
-  = DeclareExpression Declaration Expression
-  deriving (Show, Read, Eq, Generic)
-
-data Primitive
-  = Prim NameSymb
-  deriving (Show, Read, Eq, Generic)
-
-data List
-  = ListLit [Expression]
-  deriving (Show, Read, Eq, Generic)
-
-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
-      }
-  deriving (Show, Read, Eq, Generic)
-
-data Constant
-  = Number Numb
-  | String String'
-  deriving (Show, Read, Eq, Generic)
-
-data Numb
-  = Integer' Integer
-  | Double' Double
-  deriving (Show, Read, Eq, Generic)
-
-newtype String'
-  = Sho Text
-  deriving (Show, Read, Eq, Generic)
-
-newtype Block
-  = Bloc
-      {blockExpr :: Expression}
-  deriving (Show, Read, Eq, Generic)
-
-data Lambda
-  = Lamb
-      { lambdaArgs :: NonEmpty MatchLogic,
-        lambdaBody :: Expression
-      }
-  deriving (Show, Read, Eq, Generic)
-
-data Application
-  = App
-      { applicationName :: Expression,
-        applicationArgs :: NonEmpty Expression
-      }
-  deriving (Show, Read, Eq, Generic)
-
-data EffApp
-  = Via
-      { effappHand :: Expression,
-        effappArg :: Expression
-      }
-  deriving (Show, Read, Generic, Eq)
-
--- Was a newtype but extensible adds fields
-newtype Do
-  = Do'' (NonEmpty DoBody)
-  deriving (Show, Read, Eq, Generic)
-
--- promote this to a match!!!
-data DoBody
-  = DoBody
-      { doBodyName :: Maybe Symbol,
-        doBodyExpr :: Computation -- computation as in effect
-      }
-  deriving (Show, Read, Eq, Generic)
-
-data Computation
-  = DoOp DoOp
-  | DoPure DoPure
-  deriving (Show, Read, Eq, Generic)
-
-data DoOp
-  = DoOp'
-      { opName :: Expression,
-        opArgs :: NonEmpty Expression
-      }
-  deriving (Show, Read, Eq, Generic)
-
-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)
-      }
-  deriving (Show, Read, Eq, Generic)
-
---------------------------------------------------------------------------------
--- Symbol Binding
---------------------------------------------------------------------------------
-
-data Let
-  = Let'
-      { letBindings :: FunctionLike Expression,
-        letBody :: Expression
-      }
-  deriving (Show, Read, Eq, Generic)
-
-data LetType
-  = LetType''
-      { letTypeBindings :: Type,
-        letTypeBody :: Expression
-      }
-  deriving (Show, Read, Eq, Generic)
-
-data Infix
-  = Inf
-      { infixLeft :: Expression,
-        infixOp :: NameSymb,
-        infixRight :: Expression
-      }
-  deriving (Show, Read, Eq, Generic)
-
---------------------------------------------------------------------------------
--- Matching
---------------------------------------------------------------------------------
-
-data Match
-  = Match''
-      { matchOn :: Expression,
-        matchBindigns :: NonEmpty MatchL
-      }
-  deriving (Show, Read, Eq, Generic)
-
-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
-      }
-  deriving (Show, Read, Eq, Generic)
-
-data MatchLogicStart
-  = MatchCon ConstructorName [MatchLogic]
-  | MatchName Symbol
-  | MatchConst Constant
-  | MatchRecord (NonEmpty (NameSet MatchLogic))
-  deriving (Show, Read, Eq, Generic)
-
-data NameSet t
-  = Punned NameSymb
-  | NonPunned NameSymb t
-  deriving (Show, Read, Eq, Generic)
-
-data Header topLevel
-  = Header NameSymb [topLevel]
-  | NoHeader [topLevel]
-  deriving (Show, Read, Eq, Generic)
+-- type ConstructorName = NameSymb
+
+-- type NameSymb = NonEmpty Symbol
+
+-- type ModuleName = NameSymb
+
+-- data TopLevel
+--   = Type Type
+--   | ModuleOpen ModuleOpen
+--   | Signature Signature
+--   | Module Module
+--   | Function Function
+--   | Effect Effect
+--   | Handler Handler
+--   | Declaration Declaration
+--   | TypeClass
+--   | TypeClassInstance
+--   deriving stock (Show, Read, Eq)
+
+-- --------------------------------------------------------------------------------
+-- -- Declarations
+-- --------------------------------------------------------------------------------
+
+-- newtype Declaration
+--   = Infixivity InfixDeclar
+--   deriving stock (Show, Read, Eq)
+
+-- data InfixDeclar
+--   = NonAssoc Symbol Natural
+--   | AssocL Symbol Natural
+--   | AssocR Symbol Natural
+--   deriving stock (Show, Read, Eq)
+
+-- --------------------------------------------------------------------------------
+-- -- 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'
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- -- | 'Data' is the data declaration in the Juvix language
+-- data Data
+--   = Arrowed
+--       { dataArrow :: Expression,
+--         dataAdt' :: Adt
+--       }
+--   | NonArrowed
+--       { dataAdt :: Adt
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- --------------------------------------------------------------------------------
+-- -- Arrows
+-- --------------------------------------------------------------------------------
+
+-- data NamedType
+--   = NamedType'
+--       { nameRefineName :: !Name,
+--         namedRefineRefine :: Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- -- TODO ∷ change TypeName to TypeNameModule
+-- data TypeRefine
+--   = TypeRefine
+--       { typeRefineName :: Expression,
+--         typeRefineRefinement :: Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- --------------------------------------------------------------------------------
+-- -- Types Misc
+-- --------------------------------------------------------------------------------
+
+-- data Name
+--   = Implicit !Symbol
+--   | Concrete !Symbol
+--   deriving stock (Show, Read, Eq)
+
+-- data ArrowSymbol
+--   = ArrowUse Usage.T
+--   | -- Was a usage but can't alias for now
+--     ArrowExp Expression
+--   deriving stock (Show, Read, Eq)
+
+-- -- TODO ∷ finish this type!
+-- newtype UniverseExpression
+--   = UniverseExpression Symbol
+--   deriving stock (Show, Read, Eq)
+
+-- --------------------------------------------------------------------------------
+-- -- ADTs
+-- --------------------------------------------------------------------------------
+
+-- -- The types for ADT are not the most constraining, however are setup
+-- -- to have the least amount of boilerplate in the latter stages as
+-- -- possible a Sum of length one should not have a record
+-- -- [type Address = Foo {abc : Int}]
+-- -- this form should be considered illegal unless we wish to permit
+-- -- named records along with unnamed records. Ι suspect in the future
+-- -- this will instead be used for Enum Subsets with refined information
+
+-- data Adt
+--   = Sum (NonEmpty Sum)
+--   | Product Product
+--   deriving stock (Show, Read, Eq)
+
+-- data Sum
+--   = S
+--       { sumConstructor :: !Symbol,
+--         sumValue :: !(Maybe Product)
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- -- For when a product is without a sum only a record can apply a sum
+-- -- of only one is a named product
+-- data Product
+--   = Record !Record
+--   | Arrow Expression
+--   | ADTLike [Expression]
+--   deriving stock (Show, Read, Eq)
+
+-- data Record
+--   = Record''
+--       { recordFields :: NonEmpty NameType,
+--         recordFamilySignature :: Maybe Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- data NameType
+--   = NameType'
+--       { nameTypeSignature :: Expression,
+--         nameTypeName :: !Name,
+--         nameTypeUsage :: Maybe Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- --------------------------------------------------------------------------------
+-- -- Effect Handlers
+-- --------------------------------------------------------------------------------
+
+-- data Effect
+--   = Eff
+--       { effName :: Symbol,
+--         effOps :: [Signature]
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- data Operation = Op (FunctionLike Expression)
+--   deriving stock (Show, Read, Eq)
+
+-- --  A 'Handler', as implemented here, is a set of functions that implement
+-- -- (at least) one `Effect` interface.
+-- -- However, Handlers are NOT scoped, meaning that they can't be defined
+-- -- defined within another function. We CAN fix that, but it requires
+-- -- us to make some choices, it's wise to have Witch up and running first.
+-- data Handler
+--   = Hand Symbol [Operation]
+--   deriving stock (Show, Read, Eq)
+
+-- --------------------------------------------------------------------------------
+-- -- Functions and Modules
+-- --------------------------------------------------------------------------------
+
+-- -- | 'Function' is a normal signature with a name arguments and a body
+-- -- that may or may not have a guard before it
+-- newtype Function
+--   = Func (FunctionLike Expression)
+--   deriving stock (Show, Read, Eq)
+
+-- -- 'Module' is like function, however it allows multiple top levels
+-- newtype Module
+--   = Mod (FunctionLike (NonEmpty TopLevel))
+--   deriving stock (Show, Read, Eq)
+
+-- data ModuleE
+--   = ModE
+--       { moduleEBindings :: FunctionLike (NonEmpty TopLevel),
+--         moduleEBody :: Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- -- 'FunctionLike' is the generic version for both modules and functions
+-- data FunctionLike a
+--   = Like
+--       { functionLikedName :: Symbol,
+--         functionLikeArgs :: [Arg],
+--         functionLikeBody :: GuardBody a
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- -- 'GuardBody' determines if a form is a guard or a body
+-- data GuardBody a
+--   = Body a
+--   | Guard (Cond a)
+--   deriving stock (Show, Read, Eq)
+
+-- newtype ModuleOpen
+--   = Open ModuleName
+--   deriving stock (Show, Read, Eq)
+
+-- data ModuleOpenExpr
+--   = OpenExpress
+--       { moduleOpenExprModuleN :: ModuleName,
+--         moduleOpenExprExpr :: Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- -- Very similar to name, but match instead of symbol
+-- data Arg
+--   = ImplicitA MatchLogic
+--   | ConcreteA MatchLogic
+--   deriving stock (Show, Read, Eq)
+
+-- newtype Cond a
+--   = C (NonEmpty (CondLogic a))
+--   deriving stock (Show, Read, Eq)
+
+-- data CondLogic a
+--   = CondExpression
+--       { condLogicPred :: Expression,
+--         condLogicBody :: a
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- --------------------------------------------------------------------------------
+-- -- Signatures
+-- --------------------------------------------------------------------------------
+
+-- data Signature
+--   = Sig
+--       { signatureName :: Symbol,
+--         -- Was a usage but can't alias for now
+--         signatureUsage :: Maybe Expression,
+--         signatureArrowType :: Expression,
+--         signatureConstraints :: [Expression]
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- --------------------------------------------------------------------------------
+-- -- Expression
+-- --------------------------------------------------------------------------------
+
+-- -- TODO ∷ add <expression> : <expression> <refine>?
+-- -- to the parser
+-- data Expression
+--   = Cond (Cond Expression)
+--   | Constant Constant
+--   | Let Let
+--   | ModuleE ModuleE
+--   | LetType LetType
+--   | Match Match
+--   | Name NameSymb
+--   | OpenExpr ModuleOpenExpr
+--   | Lambda Lambda
+--   | Application Application
+--   | Primitive Primitive
+--   | List List
+--   | Tuple Tuple
+--   | Block Block
+--   | Infix Infix
+--   | ExpRecord ExpRecord
+--   | RecordDec Record
+--   | Do Do
+--   | EffApp EffApp
+--   | -- Added due to merge
+--     ArrowE ArrowExp
+--   | NamedTypeE NamedType
+--   | RefinedE TypeRefine
+--   | UniverseName UniverseExpression
+--   | Parened Expression
+--   | DeclarationE DeclarationExpression
+--   deriving stock (Show, Read, Eq)
+
+-- data DeclarationExpression
+--   = DeclareExpression Declaration Expression
+--   deriving stock (Show, Read, Eq)
+
+-- data Primitive
+--   = Prim NameSymb
+--   deriving stock (Show, Read, Eq)
+
+-- data List
+--   = ListLit [Expression]
+--   deriving stock (Show, Read, Eq)
+
+-- data Tuple
+--   = TupleLit [Expression]
+--   deriving stock (Show, Read, Eq)
+
+-- data ArrowExp
+--   = Arr'
+--       { arrowExpLeft :: Expression,
+--         -- Was a usage but can't alias for now
+--         arrowExpUsage :: Expression,
+--         arrowExpRight :: Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- data Constant
+--   = Number Numb
+--   | String String'
+--   deriving stock (Show, Read, Eq)
+
+-- data Numb
+--   = Integer' Integer
+--   | Double' Double
+--   deriving stock (Show, Read, Eq)
+
+-- newtype String'
+--   = Sho Text
+--   deriving stock (Show, Read, Eq)
+
+-- newtype Block
+--   = Bloc
+--       {blockExpr :: Expression}
+--   deriving stock (Show, Read, Eq)
+
+-- data Lambda
+--   = Lamb
+--       { lambdaArgs :: NonEmpty MatchLogic,
+--         lambdaBody :: Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- data Application
+--   = App
+--       { applicationName :: Expression,
+--         applicationArgs :: NonEmpty Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- data EffApp
+--   = Via
+--       { effappHand :: Expression,
+--         effappArg :: Expression
+--       }
+--   deriving (Show, Read, Generic, Eq)
+
+-- -- Was a newtype but extensible adds fields
+-- newtype Do
+--   = Do'' (NonEmpty DoBody)
+--   deriving stock (Show, Read, Eq)
+
+-- -- promote this to a match!!!
+-- data DoBody
+--   = DoBody
+--       { doBodyName :: Maybe Symbol,
+--         doBodyExpr :: Computation -- computation as in effect
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- data Computation
+--   = DoOp DoOp
+--   | DoPure DoPure
+--   deriving stock (Show, Read, Eq)
+
+-- data DoOp
+--   = DoOp'
+--       { opName :: Expression,
+--         opArgs :: NonEmpty Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- data DoPure
+--   = DoPure'
+--       { pureArg :: Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- -- TODO ∷ we need includes in here as well!
+-- -- Was a newtype but extensible adds fields
+-- newtype ExpRecord
+--   = ExpressionRecord
+--       { expRecordFields :: NonEmpty (NameSet Expression)
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- --------------------------------------------------------------------------------
+-- -- Symbol Binding
+-- --------------------------------------------------------------------------------
+
+-- data Let
+--   = Let'
+--       { letBindings :: FunctionLike Expression,
+--         letBody :: Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- data LetType
+--   = LetType''
+--       { letTypeBindings :: Type,
+--         letTypeBody :: Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- data Infix
+--   = Inf
+--       { infixLeft :: Expression,
+--         infixOp :: NameSymb,
+--         infixRight :: Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- --------------------------------------------------------------------------------
+-- -- Matching
+-- --------------------------------------------------------------------------------
+
+-- data Match
+--   = Match''
+--       { matchOn :: Expression,
+--         matchBindigns :: NonEmpty MatchL
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- data MatchL
+--   = MatchL
+--       { matchLPattern :: MatchLogic,
+--         matchLBody :: Expression
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- -- TODO ∷ add literals to the match
+-- data MatchLogic
+--   = MatchLogic
+--       { matchLogicContents :: MatchLogicStart,
+--         matchLogicNamed :: Maybe Symbol
+--       }
+--   deriving stock (Show, Read, Eq)
+
+-- data MatchLogicStart
+--   = MatchCon ConstructorName [MatchLogic]
+--   | MatchName Symbol
+--   | MatchConst Constant
+--   | MatchRecord (NonEmpty (NameSet MatchLogic))
+--   deriving stock (Show, Read, Eq)
+
+-- data NameSet t
+--   = Punned NameSymb
+--   | NonPunned NameSymb t
+--   deriving stock (Show, Read, Eq)
+
+-- data Header topLevel
+--   = Header NameSymb [topLevel]
+--   | NoHeader [topLevel]
+--   deriving stock (Show, Read, Eq)

src/MiniJuvix/Parsing/Error.hs

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

src/MiniJuvix/Parsing/Location.hs

@@ -1,10 +1,14 @@
+{-# OPTIONS_GHC -Wno-partial-fields #-}
 -- | Adapted from https://github.com/heliaxdev/juvix/
-module MiniJuvix.Parsing.Location where
+module MiniJuvix.Parsing.Location 
+  (noLoc,location,mkLocated)
+  where
 
 --------------------------------------------------------------------------------
 
 import MiniJuvix.Utils.Parser (Parser)
 import MiniJuvix.Utils.Prelude
+
 import qualified Text.Megaparsec as P
 
 --------------------------------------------------------------------------------
@@ -12,10 +16,10 @@ import qualified Text.Megaparsec as P
 data Loc
   = NoLoc
   | Loc {line :: Int, col :: Int}
-  deriving (Eq, Show, Ord, Generic)
+  deriving stock (Eq, Show, Ord)
 
 data Located a = Located {located :: Loc, locVal :: a}
-  deriving (Generic, Show)
+  deriving stock Show
 
 instance Functor Located where
   fmap f (Located l v) = Located l (f v)
@@ -33,9 +37,9 @@ noLoc = Located NoLoc
 location :: Parser Loc
 location = do
   srcPos <- P.getSourcePos
-  let line = P.unPos $ P.sourceLine srcPos
-      col = P.unPos $ P.sourceColumn srcPos
-  pure $ Loc line col
+  let r = P.unPos $ P.sourceLine srcPos
+      c = P.unPos $ P.sourceColumn srcPos
+  pure $ Loc r c
 
 mkLocated :: Parser a -> Parser (Located a)
 mkLocated p = Located <$> location <*> p

src/MiniJuvix/Pipeline.hs

@@ -17,7 +17,8 @@ import MiniJuvix.Utils.Prelude (Eq, FilePath, Maybe, Ord, Show, Text)
 
 data CompilerMode
   = ReplMode
-  | BuildMode Config FilePath
+  | CheckMode Config FilePath
+  | CompileMode Config FilePath
   | TestMode Config FilePath
 
 data Config
@@ -33,12 +34,13 @@ data Pass
   | Desugaring
   | Typechecking
   | Compiling
-  deriving stock (Show)
+  deriving stock Show
 
 data Backend = LLVM
   deriving (Eq, Ord, Show)
 
 data WriteToFsBehavior = OverwriteTargetFiles | WriteIfDoesNotExist
+
 -- runAndLogErrs :: MiniJuvix a -> IO ()
 -- runAndLogErrs m = runMiniJuvix m >>= \(_, errs) -> logErrs errs
 
@@ -46,5 +48,9 @@ data WriteToFsBehavior = OverwriteTargetFiles | WriteIfDoesNotExist
 -- runTestWith filePath config = case _configPass config of
 --   Parsing -> undefined
 --   Desugaring -> undefined
---   Typechecking -> runAndLogErrs $ depAnalPass filePath >>= parsePass >>= checkPass
+  -- Typechecking -> runAndLogErrs $ depAnalPass filePath >>= parsePass >>= checkPass
 --   Compiling -> undefined
+
+
+runMiniJuvix :: 
+runMiniJuvix = ?

src/MiniJuvix/Pretty.hs

@@ -48,10 +48,6 @@ instance Pretty Variable where
   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
-  pretty b (Inferable t) = pretty b t
-
 instance Pretty CheckableTerm where
   pretty _ = prettyCheckable
 
@@ -78,11 +74,21 @@ prettyInferrable (App m n) = undefined
 prettyInferrable (TensorTypeElim q x _ _ t _ _) = undefined
 prettyInferrable (SumTypeElim q b x y c z s t) = undefined
 
+instance Pretty Term where
+  pretty b (Checkable t) = pretty b t
+  pretty b (Inferable t) = pretty b t
+
 instance Pretty Value where
   pretty _ = undefined
 
 instance Pretty Neutral where
   pretty _ = undefined
 
+instance Pretty Binding where
+  pretty _ = undefined
+
 instance Pretty TypingEnv where
   pretty _ = undefined
+
+instance Pretty TypingContext where
+  pretty _ = undefined

src/MiniJuvix/Syntax/Core.agda

@@ -18,16 +18,20 @@ open import Agda.Builtin.Equality
 --------------------------------------------------------------------------------
 
 {-# FOREIGN AGDA2HS
-{-# OPTIONS_GHC -fno-warn-missing-export-lists -fno-warn-unused-matches #-}
+{-# OPTIONS_GHC -fno-warn-missing-export-lists #-}
+{-# OPTIONS_GHC -fno-warn-unused-matches #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
 #-}
 
 {-# FOREIGN AGDA2HS
+--------------------------------------------------------------------------------
+
 import MiniJuvix.Utils.Prelude
-#-}
 
 --------------------------------------------------------------------------------
 -- Quantity (a.k.a. Usage)
 --------------------------------------------------------------------------------
+#-}
 
 data Quantity : Set where
   Zero One Many : Quantity
@@ -162,7 +166,9 @@ instance
 
 -- TODO: May I want to have Instances of Ord, Functor, Applicative, Monad?
 
+{-# FOREIGN AGDA2HS
 --------------------------------------------------------------------------------
+#-}
 
 {- 
 Core syntax follows the pattern design for bidirectional typing
@@ -183,9 +189,11 @@ Jargon:
   principal connective.
 -}
 
+{-# FOREIGN AGDA2HS
 --------------------------------------------------------------------------------
 -- Type-checkable terms.
 --------------------------------------------------------------------------------
+#-}
 
 data CheckableTerm : Set
 data InferableTerm : Set
@@ -230,9 +238,11 @@ data CheckableTerm where
 
 {-# COMPILE AGDA2HS CheckableTerm #-}
 
+{-# FOREIGN AGDA2HS
 --------------------------------------------------------------------------------
 -- Type-inferable terms (a.k.a terms that synthesise)
 --------------------------------------------------------------------------------
+#-}
 
 data InferableTerm where
   -- | Variables, typing rule Var⇒. 
@@ -276,9 +286,11 @@ data InferableTerm where
     → InferableTerm
 {-# COMPILE AGDA2HS InferableTerm #-}
 
+{-# FOREIGN AGDA2HS
 --------------------------------------------------------------------------------
 -- Term Equality
 --------------------------------------------------------------------------------
+#-}
 
 checkEq : CheckableTerm → CheckableTerm → Bool
 inferEq : InferableTerm → InferableTerm → Bool
@@ -302,7 +314,6 @@ checkEq (Inferred x) (Inferred y) = inferEq x y
 checkEq _ _ = false
 {-# COMPILE AGDA2HS checkEq #-}
 
-
 inferEq (Var x) (Var y) = x == y
 inferEq (Ann x₁ y₁) (Ann x₂ y₂) = checkEq x₁ x₂ &&  checkEq y₁ y₂
 inferEq (App x₁ y₁) (App x₂ y₂) =  inferEq x₁ x₂ &&  checkEq y₁ y₂
@@ -324,7 +335,6 @@ instance
   InferableTermEq ._==_ = inferEq
 {-# COMPILE AGDA2HS InferableTermEq #-}
 
-
 data Term : Set where
   Checkable : CheckableTerm → Term  -- terms with a type checkable.
   Inferable : InferableTerm → Term  -- terms that which types can be inferred.

src/MiniJuvix/Syntax/Core.hs

@@ -1,20 +1,28 @@
-{-# OPTIONS_GHC -fno-warn-missing-export-lists -fno-warn-unused-matches #-}
+{-# OPTIONS_GHC -fno-warn-missing-export-lists #-}
+{-# OPTIONS_GHC -fno-warn-unused-matches #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
 
 module MiniJuvix.Syntax.Core where
 
-import MiniJuvix.Utils.Prelude
 import Numeric.Natural (Natural)
 
-data Quantity
-  = Zero
-  | One
-  | Many
+--------------------------------------------------------------------------------
+
+import MiniJuvix.Utils.Prelude
+
+--------------------------------------------------------------------------------
+-- Quantity (a.k.a. Usage)
+--------------------------------------------------------------------------------
+
+data Quantity = Zero
+              | One
+              | Many
 
 instance Eq Quantity where
-  Zero == Zero = True
-  One == One = True
-  Many == Many = True
-  _ == _ = False
+    Zero == Zero = True
+    One == One = True
+    Many == Many = True
+    _ == _ = False
 
 compareQuantity :: Quantity -> Quantity -> Ordering
 compareQuantity Zero Zero = EQ
@@ -26,38 +34,36 @@ compareQuantity _ One = GT
 compareQuantity Many Many = EQ
 
 instance Ord Quantity where
-  compare = compareQuantity
-  x < y = compareQuantity x y == LT
-  x > y = compareQuantity x y == GT
-  x <= y = compareQuantity x y /= GT
-  x >= y = compareQuantity x y /= LT
-  max x y = if compareQuantity x y == LT then y else x
-  min x y = if compareQuantity x y == GT then y else x
+    compare = compareQuantity
+    x < y = compareQuantity x y == LT
+    x > y = compareQuantity x y == GT
+    x <= y = compareQuantity x y /= GT
+    x >= y = compareQuantity x y /= LT
+    max x y = if compareQuantity x y == LT then y else x
+    min x y = if compareQuantity x y == GT then y else x
 
 instance Semigroup Quantity where
-  Zero <> _ = Zero
-  One <> m = m
-  Many <> Zero = Zero
-  Many <> One = Many
-  Many <> Many = Many
+    Zero <> _ = Zero
+    One <> m = m
+    Many <> Zero = Zero
+    Many <> One = Many
+    Many <> Many = Many
 
 instance Monoid Quantity where
-  mempty = Zero
+    mempty = Zero
 
 instance Semiring Quantity where
-  one = One
-  times Zero _ = Zero
-  times One m = m
-  times Many Zero = Zero
-  times Many One = Many
-  times Many Many = Many
+    one = One
+    times Zero _ = Zero
+    times One m = m
+    times Many Zero = Zero
+    times Many One = Many
+    times Many Many = Many
 
-data Relevance
-  = Relevant
-  | Irrelevant
+data Relevance = Relevant
+               | Irrelevant
 
 deriving stock instance Eq Relevance
-
 deriving stock instance Ord Relevance
 
 relevancy :: Quantity -> Relevance
@@ -68,71 +74,68 @@ type Index = Natural
 
 type BindingName = String
 
-data Name
-  = Global String
-  | Local BindingName Index
+data Name = Global String
+          | Local BindingName Index
 
 instance Eq Name where
-  Global x == Global y = x == y
-  Local x1 y1 == Local x2 y2 = x1 == x2 && y1 == y2
-  _ == _ = False
+    Global x == Global y = x == y
+    Local x1 y1 == Local x2 y2 = x1 == x2 && y1 == y2
+    _ == _ = False
 
-data Variable
-  = Bound Index
-  | Free Name
+data Variable = Bound Index
+              | Free Name
 
 instance Eq Variable where
-  Bound x == Bound y = x == y
-  Free x == Free y = x == y
-  _ == _ = False
+    Bound x == Bound y = x == y
+    Free x == Free y = x == y
+    _ == _ = False
 
-data CheckableTerm
-  = UniverseType
-  | PiType Quantity BindingName CheckableTerm CheckableTerm
-  | Lam BindingName CheckableTerm
-  | TensorType Quantity BindingName CheckableTerm CheckableTerm
-  | TensorIntro CheckableTerm CheckableTerm
-  | UnitType
-  | Unit
-  | SumType CheckableTerm CheckableTerm
-  | Inl CheckableTerm
-  | Inr CheckableTerm
-  | Inferred InferableTerm
+--------------------------------------------------------------------------------
 
-data InferableTerm
-  = Var Variable
-  | Ann CheckableTerm CheckableTerm
-  | App InferableTerm CheckableTerm
-  | TensorTypeElim
-      Quantity
-      BindingName
-      BindingName
-      BindingName
-      InferableTerm
-      CheckableTerm
-      CheckableTerm
-  | SumTypeElim
-      Quantity
-      BindingName
-      InferableTerm
-      BindingName
-      CheckableTerm
-      BindingName
-      CheckableTerm
-      CheckableTerm
+--------------------------------------------------------------------------------
+-- Type-checkable terms.
+--------------------------------------------------------------------------------
+
+data CheckableTerm = UniverseType
+                   | PiType Quantity BindingName CheckableTerm CheckableTerm
+                   | Lam BindingName CheckableTerm
+                   | TensorType Quantity BindingName CheckableTerm CheckableTerm
+                   | TensorIntro CheckableTerm CheckableTerm
+                   | UnitType
+                   | Unit
+                   | SumType CheckableTerm CheckableTerm
+                   | Inl CheckableTerm
+                   | Inr CheckableTerm
+                   | Inferred InferableTerm
+
+data InferableTerm = Var Variable
+                   | Ann CheckableTerm CheckableTerm
+                   | App InferableTerm CheckableTerm
+                   | TensorTypeElim Quantity BindingName BindingName BindingName
+                                    InferableTerm CheckableTerm CheckableTerm
+                   | SumTypeElim Quantity BindingName InferableTerm BindingName
+                                 CheckableTerm BindingName CheckableTerm CheckableTerm
+
+--------------------------------------------------------------------------------
+-- Type-inferable terms (a.k.a terms that synthesise)
+--------------------------------------------------------------------------------
+
+--------------------------------------------------------------------------------
+-- Term Equality
+--------------------------------------------------------------------------------
 
 checkEq :: CheckableTerm -> CheckableTerm -> Bool
 checkEq UniverseType UniverseType = True
-checkEq (PiType q₁ _ a₁ b₁) (PiType q₂ _ a₂ b₂) =
-  q₁ == q₂ && checkEq a₁ a₂ && checkEq b₁ b₂
-checkEq (TensorType q₁ _ a₁ b₁) (TensorType q₂ _ a₂ b₂) =
-  q₁ == q₂ && checkEq a₁ a₂ && checkEq b₁ b₂
-checkEq (TensorIntro x₁ y₁) (TensorIntro x₂ y₂) =
-  checkEq x₁ x₂ && checkEq y₁ y₂
+checkEq (PiType q₁ _ a₁ b₁) (PiType q₂ _ a₂ b₂)
+  = q₁ == q₂ && checkEq a₁ a₂ && checkEq b₁ b₂
+checkEq (TensorType q₁ _ a₁ b₁) (TensorType q₂ _ a₂ b₂)
+  = q₁ == q₂ && checkEq a₁ a₂ && checkEq b₁ b₂
+checkEq (TensorIntro x₁ y₁) (TensorIntro x₂ y₂)
+  = checkEq x₁ x₂ && checkEq y₁ y₂
 checkEq UnitType UnitType = True
 checkEq Unit Unit = True
-checkEq (SumType x₁ y₁) (SumType x₂ y₂) =
-  checkEq x₁ x₂ && checkEq y₁ y₂
+checkEq (SumType x₁ y₁) (SumType x₂ y₂)
+  = checkEq x₁ x₂ && checkEq y₁ y₂
 checkEq (Inl x) (Inl y) = checkEq x y
 checkEq (Inr x) (Inr y) = checkEq x y
 checkEq (Inferred x) (Inferred y) = inferEq x y
@@ -142,29 +145,23 @@ inferEq :: InferableTerm -> InferableTerm -> Bool
 inferEq (Var x) (Var y) = x == y
 inferEq (Ann x₁ y₁) (Ann x₂ y₂) = checkEq x₁ x₂ && checkEq y₁ y₂
 inferEq (App x₁ y₁) (App x₂ y₂) = inferEq x₁ x₂ && checkEq y₁ y₂
-inferEq
-  (TensorTypeElim q₁ _ _ _ a₁ b₁ c₁)
-  (TensorTypeElim q₂ _ _ _ a₂ b₂ c₂) =
-    q₁ == q₂ && inferEq a₁ a₂ && checkEq b₁ b₂ && checkEq c₁ c₂
-inferEq
-  (SumTypeElim q₁ _ x₁ _ a₁ _ b₁ c₁)
-  (SumTypeElim q₂ _ x₂ _ a₂ _ b₂ c₂) =
-    q₁ == q₂
-      && inferEq x₁ x₂
-      && checkEq a₁ a₂
-      && checkEq b₁ b₂
-      && checkEq c₁ c₂
+inferEq (TensorTypeElim q₁ _ _ _ a₁ b₁ c₁)
+  (TensorTypeElim q₂ _ _ _ a₂ b₂ c₂)
+  = q₁ == q₂ && inferEq a₁ a₂ && checkEq b₁ b₂ && checkEq c₁ c₂
+inferEq (SumTypeElim q₁ _ x₁ _ a₁ _ b₁ c₁)
+  (SumTypeElim q₂ _ x₂ _ a₂ _ b₂ c₂)
+  = q₁ == q₂ &&
+      inferEq x₁ x₂ && checkEq a₁ a₂ && checkEq b₁ b₂ && checkEq c₁ c₂
 inferEq _ _ = False
 
 instance Eq CheckableTerm where
-  (==) = checkEq
+    (==) = checkEq
 
 instance Eq InferableTerm where
-  (==) = inferEq
+    (==) = inferEq
 
-data Term
-  = Checkable CheckableTerm
-  | Inferable InferableTerm
+data Term = Checkable CheckableTerm
+          | Inferable InferableTerm
 
 termEq :: Term -> Term -> Bool
 termEq (Checkable (Inferred x)) (Inferable y) = x == y
@@ -174,4 +171,5 @@ termEq (Inferable x) (Inferable y) = x == y
 termEq _ _ = False
 
 instance Eq Term where
-  (==) = termEq
+    (==) = termEq
+

src/MiniJuvix/Syntax/Eval.agda

@@ -20,9 +20,11 @@ import MiniJuvix.Syntax.Core
 import MiniJuvix.Utils.Prelude
 #-}
 
+{-# FOREIGN AGDA2HS
 --------------------------------------------------------------------------------
 -- Values and neutral terms
 --------------------------------------------------------------------------------
+#-}
 
 {-
   We are interested in a normal form for posibbly open terms. This

src/MiniJuvix/Syntax/Eval.hs

@@ -1,102 +1,77 @@
-{-# OPTIONS_GHC -fno-warn-missing-export-lists -fno-warn-unused-matches #-}
+{-# OPTIONS_GHC
+  -fno-warn-missing-export-lists -fno-warn-unused-matches #-}
 
 module MiniJuvix.Syntax.Eval where
 
 import MiniJuvix.Syntax.Core
 import MiniJuvix.Utils.Prelude
 
-data Value
-  = IsUniverse
-  | IsPiType Quantity BindingName Value (Value -> Value)
-  | IsLam BindingName (Value -> Value)
-  | IsTensorType Quantity BindingName Value (Value -> Value)
-  | IsTensorIntro Value Value
-  | IsUnitType
-  | IsUnit
-  | IsSumType Value Value
-  | IsInl Value
-  | IsInr Value
-  | IsNeutral Neutral
+--------------------------------------------------------------------------------
+-- Values and neutral terms
+--------------------------------------------------------------------------------
 
-data Neutral
-  = IsFree Name
-  | IsApp Neutral Value
-  | IsTensorTypeElim
-      Quantity
-      BindingName
-      BindingName
-      BindingName
-      Neutral
-      (Value -> Value -> Value)
-      (Value -> Value)
-  | NSumElim
-      Quantity
-      BindingName
-      Neutral
-      BindingName
-      (Value -> Value)
-      BindingName
-      (Value -> Value)
-      (Value -> Value)
+data Value = IsUniverse
+           | IsPiType Quantity BindingName Value (Value -> Value)
+           | IsLam BindingName (Value -> Value)
+           | IsTensorType Quantity BindingName Value (Value -> Value)
+           | IsTensorIntro Value Value
+           | IsUnitType
+           | IsUnit
+           | IsSumType Value Value
+           | IsInl Value
+           | IsInr Value
+           | IsNeutral Neutral
+
+data Neutral = IsFree Name
+             | IsApp Neutral Value
+             | IsTensorTypeElim Quantity BindingName BindingName BindingName
+                                Neutral (Value -> Value -> Value) (Value -> Value)
+             | NSumElim Quantity BindingName Neutral BindingName
+                        (Value -> Value) BindingName (Value -> Value) (Value -> Value)
 
 valueToTerm :: Value -> Term
 valueToTerm v = Checkable Unit
 
 substCheckableTerm ::
-  CheckableTerm -> Index -> InferableTerm -> CheckableTerm
+                   CheckableTerm -> Index -> InferableTerm -> CheckableTerm
 substCheckableTerm UniverseType x m = UniverseType
-substCheckableTerm (PiType q y a b) x m =
-  PiType
-    q
-    y
-    (substCheckableTerm a x m)
-    (substCheckableTerm b (x + 1) m)
-substCheckableTerm (Lam y n) x m =
-  Lam y (substCheckableTerm n (x + 1) m)
-substCheckableTerm (TensorType q y s t) x m =
-  TensorType
-    q
-    y
-    (substCheckableTerm s x m)
-    (substCheckableTerm t (x + 1) m)
-substCheckableTerm (TensorIntro p1 p2) x m =
-  TensorIntro
-    (substCheckableTerm p1 x m)
-    (substCheckableTerm p2 x m)
+substCheckableTerm (PiType q y a b) x m
+  = PiType q y (substCheckableTerm a x m)
+      (substCheckableTerm b (x + 1) m)
+substCheckableTerm (Lam y n) x m
+  = Lam y (substCheckableTerm n (x + 1) m)
+substCheckableTerm (TensorType q y s t) x m
+  = TensorType q y (substCheckableTerm s x m)
+      (substCheckableTerm t (x + 1) m)
+substCheckableTerm (TensorIntro p1 p2) x m
+  = TensorIntro (substCheckableTerm p1 x m)
+      (substCheckableTerm p2 x m)
 substCheckableTerm UnitType x m = UnitType
 substCheckableTerm Unit x m = Unit
-substCheckableTerm (SumType a b) x m =
-  SumType (substCheckableTerm a x m) (substCheckableTerm b x m)
+substCheckableTerm (SumType a b) x m
+  = SumType (substCheckableTerm a x m) (substCheckableTerm b x m)
 substCheckableTerm (Inl n) x m = Inl (substCheckableTerm n x m)
 substCheckableTerm (Inr n) x m = Inr (substCheckableTerm n x m)
-substCheckableTerm (Inferred n) x m =
-  Inferred (substInferableTerm n x m)
+substCheckableTerm (Inferred n) x m
+  = Inferred (substInferableTerm n x m)
 
 substInferableTerm ::
-  InferableTerm -> Index -> InferableTerm -> InferableTerm
-substInferableTerm (Var (Bound y)) x m =
-  if x == y then m else Var (Bound y)
+                   InferableTerm -> Index -> InferableTerm -> InferableTerm
+substInferableTerm (Var (Bound y)) x m
+  = if x == y then m else Var (Bound y)
 substInferableTerm (Var (Free y)) x m = Var (Free y)
-substInferableTerm (Ann y a) x m =
-  Ann (substCheckableTerm y x m) (substCheckableTerm a x m)
-substInferableTerm (App f t) x m =
-  App (substInferableTerm f x m) (substCheckableTerm t x m)
-substInferableTerm (TensorTypeElim q z u v n a b) x m =
-  TensorTypeElim
-    q
-    z
-    u
-    v
-    (substInferableTerm n x m)
-    (substCheckableTerm a (x + 2) m)
-    (substCheckableTerm b (x + 1) m)
-substInferableTerm (SumTypeElim q z esum u r1 v r2 ann) x m =
-  SumTypeElim
-    q
-    z
-    (substInferableTerm esum x m)
-    u
-    (substCheckableTerm r1 (x + 1) m)
-    v
-    (substCheckableTerm r2 (x + 1) m)
-    (substCheckableTerm ann (x + 1) m)
+substInferableTerm (Ann y a) x m
+  = Ann (substCheckableTerm y x m) (substCheckableTerm a x m)
+substInferableTerm (App f t) x m
+  = App (substInferableTerm f x m) (substCheckableTerm t x m)
+substInferableTerm (TensorTypeElim q z u v n a b) x m
+  = TensorTypeElim q z u v (substInferableTerm n x m)
+      (substCheckableTerm a (x + 2) m)
+      (substCheckableTerm b (x + 1) m)
+substInferableTerm (SumTypeElim q z esum u r1 v r2 ann) x m
+  = SumTypeElim q z (substInferableTerm esum x m) u
+      (substCheckableTerm r1 (x + 1) m)
+      v
+      (substCheckableTerm r2 (x + 1) m)
+      (substCheckableTerm ann (x + 1) m)
+

src/MiniJuvix/Typing/Erasure.hs

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

src/MiniJuvix/Utils/NameSymbol.hs

@@ -1,144 +0,0 @@
-module MiniJuvix.Utils.NameSymbol
-  ( fromString,
-  )
-where
-
---------------------------------------------------------------------------------
--- Adapted from https://github.com/heliaxdev/juvix/library/StandardLibrary
-
--- import qualified Data.List.NonEmpty as NonEmpty
--- import Data.String (IsString (..))
--- import qualified Data.Text as Text
-
-import qualified MiniJuvix.Utils.Parser.Token as Tok
-import MiniJuvix.Utils.Prelude
-import qualified MiniJuvix.Utils.Pretty as PP
-
--- import qualified Prelude (foldr1)
-
---------------------------------------------------------------------------------
-
-type T = NonEmpty Symbol
-
-type Base = Symbol
-
-type Mod = [Symbol]
-
-class Name a where
-  toSym :: a -> Symbol
-  fromSym :: Symbol -> a
-
-instance Name T where
-  toSym = toSymbol
-  fromSym = fromSymbol
-
-instance Name Symbol where
-  toSym x = x
-  fromSym x = x
-
-toNonEmptySymbol :: T -> NonEmpty Symbol
-toNonEmptySymbol = identity
-
-toSymbol :: T -> Symbol
-toSymbol =
-  Prelude.foldr1 (\x acc -> x <> "." <> acc)
-
-fromSymbol :: Symbol -> T
-fromSymbol =
-  NonEmpty.fromList . fmap internText . handleInfix . Text.splitOn "." . textify
-
-fromText :: Text -> T
-fromText = fromSymbol . internText
-
--- TODO ∷ make this a fold!?
-handleInfix :: [Text] -> [Text]
-handleInfix [] = []
-handleInfix (x : xs) = rec' (x : xs) ""
-  where
-    rec' ("" : xs) currentInfixSymbol =
-      rec' xs (Text.snoc currentInfixSymbol '.')
-    rec' (x : xs) build
-      -- case 1)
-      | Tok.validInfixSymbol (Tok.charToWord8 (Text.head x)) =
-        rec' xs (build <> Text.cons '.' x)
-      | Text.null build =
-        x : rec' xs build
-      | otherwise =
-        -- case 3)
-        -- we must tail x, as we add an extra .
-        -- at the start of every infix symbol.
-        -- we do this because even a symbol like
-        -- "-" triggers case 1) which adds a '.'
-        -- to the front even when it shouldn't!
-        -- this is the correct behavior IFF we
-        -- are in the middle of a infix symbol!
-        Text.tail build : x : xs
-    rec' [] "" =
-      []
-    rec' [] acc =
-      -- see case 3)
-      [Text.tail acc]
-
-instance IsString T where
-  fromString = fromSymbol . intern
-
-prefixOf :: T -> T -> Bool
-prefixOf smaller larger =
-  case takePrefixOfInternal smaller larger of
-    Just _ -> True
-    Nothing -> False
-
-takePrefixOf :: T -> T -> Maybe T
-takePrefixOf smaller larger =
-  case takePrefixOfInternal smaller larger of
-    Just [] -> Nothing
-    Nothing -> Nothing
-    Just (x : xs) -> Just (x :| xs)
-
-takePrefixOfInternal :: T -> T -> Maybe [Symbol]
-takePrefixOfInternal (s :| smaller) (b :| bigger)
-  | b == s = recurse smaller bigger
-  | otherwise = Nothing
-  where
-    recurse [] ys = Just ys
-    recurse _ [] = Nothing
-    recurse (x : xs) (y : ys)
-      | x == y = recurse xs ys
-      | otherwise = Nothing
-
-cons :: Symbol -> T -> T
-cons = NonEmpty.cons
-
-append :: T -> T -> T
-append = (<>)
-
-hd :: T -> Symbol
-hd = NonEmpty.head
-
-qualify :: Foldable t => t Symbol -> T -> T
-qualify m n = foldr cons n m
-
-qualify1 :: Foldable t => t Symbol -> Base -> T
-qualify1 m b = qualify m (b :| [])
-
-qualified :: T -> Bool
-qualified (_ :| xs) = not $ null xs
-
-split :: T -> (Mod, Base)
-split n = (NonEmpty.init n, NonEmpty.last n)
-
-mod :: T -> Mod
-mod = fst . split
-
-base :: T -> Base
-base = snd . split
-
-applyBase :: (Base -> Base) -> T -> T
-applyBase f n = let (m, b) = split n in qualify1 m (f b)
-
-type instance PP.Ann T = ()
-
-instance PP.PrettySyntax T
-
-instance PP.PrettyText T where
-  prettyT = PP.text . textify . toSymbol

src/MiniJuvix/Utils/Parser.hs

@@ -1,11 +1,79 @@
+-- | Adapted from heliaxdev/Juvix/library/StandardLibrary/src/Juvix/Parser*
 module MiniJuvix.Utils.Parser
   ( Parser,
     ParserError,
+
+    -- * Tokens
+    charToWord8,
+    wordToChr,
+    validUpperSymbol,
+    validStartSymbol',
+    dash,
+    percent,
+    slash,
+    newLine,
+    backtick,
+    hat,
+    asterisk,
+    amper,
+    bang,
+    question,
+    dot,
+    at,
+    equals,
+    pipe,
+    doubleQuote,
+    quote,
+    backSlash,
+    closeBracket,
+    openBracket,
+    closeCurly,
+    openCurly,
+    closeParen,
+    openParen,
+    hash,
+    comma,
+    semi,
+    colon,
+    space,
+    under,
+    validStartSymbol,
+    validMiddleSymbol,
+    validInfixSymbol,
+    endOfLine,
+    reservedWords,
+    reservedSymbols,
+
+    -- * Lexing
+    emptyCheck,
+    spacer,
+    spaceLiner,
+    skipLiner,
+    eatSpaces,
+    between,
+    parens,
+    brackets,
+    curly,
+    many1H,
+    sepBy1HFinal,
+    sepBy1,
+    sepBy1H,
+    maybeParend,
+    integer,
   )
 where
 
-import Protolude
+--------------------------------------------------------------------------------
+
+import qualified Data.ByteString.Char8 as Char8
+import qualified Data.Word8 as Word8
+import qualified GHC.Unicode as Unicode
+import MiniJuvix.Utils.Prelude
+import qualified MiniJuvix.Utils.Prelude as Set
 import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Byte as P
+
+--------------------------------------------------------------------------------
 
 type Parser = P.Parsec Void ByteString
 
@@ -14,3 +82,221 @@ type Parser = P.Parsec Void ByteString
 -- Custom error component Type of input stream
 
 type ParserError = P.ParseErrorBundle ByteString Void
+
+--------------------------------------------------------------------------------
+-- Tokens
+--------------------------------------------------------------------------------
+
+charToWord8 :: Char -> Word8
+charToWord8 = fromIntegral . ord
+{-# INLINE charToWord8 #-}
+
+wordToChr :: Integral a => a -> Char
+wordToChr = chr . fromIntegral
+
+-- Hopefully this is fast!
+validStartSymbol' :: Integral a => a -> Bool
+validStartSymbol' = Unicode.isAlpha . wordToChr
+
+-- Unicode.isUpper 'İ' = True!
+validUpperSymbol :: Integral a => a -> Bool
+validUpperSymbol = Unicode.isUpper . wordToChr
+
+dash :: Word8
+dash = charToWord8 '-'
+
+under :: Word8
+under = charToWord8 '_'
+
+space :: Word8
+space = charToWord8 ' '
+
+colon :: Word8
+colon = charToWord8 ':'
+
+semi :: Word8
+semi = charToWord8 ';'
+
+comma :: Word8
+comma = charToWord8 ','
+
+hash :: Word8
+hash = charToWord8 '#'
+
+openParen :: Word8
+openParen = charToWord8 '('
+
+closeParen :: Word8
+closeParen = charToWord8 ')'
+
+openCurly :: Word8
+openCurly = charToWord8 '{'
+
+closeCurly :: Word8
+closeCurly = charToWord8 '}'
+
+openBracket :: Word8
+openBracket = charToWord8 '['
+
+closeBracket :: Word8
+closeBracket = charToWord8 ']'
+
+backSlash :: Word8
+backSlash = charToWord8 '\\'
+
+quote :: Word8
+quote = charToWord8 '\''
+
+doubleQuote :: Word8
+doubleQuote = charToWord8 '\"'
+
+pipe :: Word8
+pipe = charToWord8 '|'
+
+equals :: Word8
+equals = charToWord8 '='
+
+at :: Word8
+at = charToWord8 '@'
+
+dot :: Word8
+dot = charToWord8 '.'
+
+question :: Word8
+question = charToWord8 '?'
+
+bang :: Word8
+bang = charToWord8 '!'
+
+amper :: Word8
+amper = charToWord8 '&'
+
+asterisk :: Word8
+asterisk = charToWord8 '*'
+
+hat :: Word8
+hat = charToWord8 '^'
+
+backtick :: Word8
+backtick = charToWord8 '`'
+
+newLine :: Word8
+newLine = charToWord8 '\n'
+
+slash :: Word8
+slash = charToWord8 '/'
+
+percent :: Word8
+percent = charToWord8 '%'
+
+validStartSymbol :: Word8 -> Bool
+validStartSymbol w =
+  validStartSymbol' w || w == under
+
+validInfixSymbol :: Word8 -> Bool
+validInfixSymbol w =
+  Unicode.isSymbol (wordToChr w)
+    || w == asterisk
+    || w == hat
+    || w == dash
+    || w == amper
+    || w == colon
+    || w == slash
+    || w == percent
+    || w == dot
+
+validMiddleSymbol :: Word8 -> Bool
+validMiddleSymbol w =
+  validStartSymbol w
+    || Word8.isDigit w
+    || w == dash
+    || w == bang
+    || w == question
+    || w == percent
+
+-- check for \r or \n
+endOfLine :: (Eq a, Num a) => a -> Bool
+endOfLine w = w == 13 || w == 10
+
+-- Reserved words and symbols.
+
+reservedWords :: (Ord a, IsString a) => Set a
+reservedWords =
+  Set.fromList
+    [ "let",
+      "val",
+      "type",
+      "case",
+      "in",
+      "open",
+      "if",
+      "cond",
+      "end",
+      "of",
+      "begin",
+      "sig", -- TODO: we might removed this from the language.
+      "mod",
+      "declare",
+      "where",
+      "via",
+      "handler",
+      "effect"
+    ]
+
+reservedSymbols :: (Ord a, IsString a) => Set a
+reservedSymbols = Set.fromList ["=", "|", "", "--"]
+
+--------------------------------------------------------------------------------
+-- Lexing
+--------------------------------------------------------------------------------
+
+emptyCheck :: Word8 -> Bool
+emptyCheck x = Word8.isSpace x || x == newLine
+
+spacer :: Parser p -> Parser p
+spacer p = P.takeWhileP (Just "spacer") Word8.isSpace *> p
+
+spaceLiner :: Parser p -> Parser p
+spaceLiner p = do
+  p <* P.takeWhileP (Just "space liner") emptyCheck
+
+skipLiner :: Word8 -> Parser ()
+skipLiner p = spaceLiner (P.skipCount 1 (P.char p))
+
+eatSpaces :: Parser p -> Parser p
+eatSpaces p = P.takeWhileP (Just "eat spaces") emptyCheck *> p
+
+between :: Word8 -> Parser p -> Word8 -> Parser p
+between x p end = skipLiner x *> spaceLiner p <* P.satisfy (== end)
+
+parens :: Parser p -> Parser p
+parens p = between openParen p closeParen
+
+brackets :: Parser p -> Parser p
+brackets p = between openBracket p closeBracket
+
+curly :: Parser p -> Parser p
+curly p = between openCurly p closeCurly
+
+many1H :: Parser a -> Parser (NonEmpty a)
+many1H = fmap fromList . P.some
+
+-- | 'sepBy1HFinal' is like 'sepBy1H' but also tries to parse a last separator
+sepBy1HFinal :: Parser a -> Parser s -> Parser (NonEmpty a)
+sepBy1HFinal parse sep = sepBy1H parse sep <* P.optional sep
+
+sepBy1 :: Parser a -> Parser s -> Parser [a]
+sepBy1 p sep = liftA2 (:) p (many (P.try $ sep *> p))
+
+sepBy1H :: Parser a -> Parser s -> Parser (NonEmpty a)
+sepBy1H parse sep = fromList <$> sepBy1 parse sep
+
+maybeParend :: Parser a -> Parser a
+maybeParend p = p <|> parens p
+
+integer :: Parser Integer
+integer = do
+  digits <- P.takeWhileP (Just "digits") Word8.isDigit
+  case Char8.readInteger digits of
+    Just (x, _) -> pure x
+    Nothing -> fail "didn't parse an int"

src/MiniJuvix/Utils/Parser/Lexer.hs

@@ -1,83 +0,0 @@
--- | Adapted from https://github.com/heliaxdev/juvix/
-module MiniJuvix.Utils.Parser.Lexer
-  ( spacer,
-    spaceLiner,
-    skipLiner,
-    parens,
-    brackets,
-    between,
-    curly,
-    many1H,
-    sepBy1H,
-    sepBy1HFinal,
-    maybeParend,
-    emptyCheck,
-    eatSpaces,
-    integer,
-  )
-where
-
---------------------------------------------------------------------------------
-
--- import qualified Data.ByteString.Char8 as Char8
--- import qualified Data.List.NonEmpty as NonEmpty
--- import Data.Word8 (isDigit, isSpace)
--- import Juvix.Library
--- import Juvix.Library.Parser.Internal (Parser)
--- import qualified Juvix.Library.Parser.Token as Tok
--- import qualified Text.Megaparsec as P
--- import qualified Text.Megaparsec.Byte as P
--- import Prelude (fail)
-
---------------------------------------------------------------------------------
-
-emptyCheck :: Word8 -> Bool
-emptyCheck x = isSpace x || x == Tok.newLine
-
-spacer :: Parser p -> Parser p
-spacer p = P.takeWhileP (Just "spacer") isSpace *> p
-
-spaceLiner :: Parser p -> Parser p
-spaceLiner p = do
-  p <* P.takeWhileP (Just "space liner") emptyCheck
-
-eatSpaces :: Parser p -> Parser p
-eatSpaces p = P.takeWhileP (Just "eat spaces") emptyCheck *> p
-
-between :: Word8 -> Parser p -> Word8 -> Parser p
-between fst p end = skipLiner fst *> spaceLiner p <* P.satisfy (== end)
-
-parens :: Parser p -> Parser p
-parens p = between Tok.openParen p Tok.closeParen
-
-brackets :: Parser p -> Parser p
-brackets p = between Tok.openBracket p Tok.closeBracket
-
-curly :: Parser p -> Parser p
-curly p = between Tok.openCurly p Tok.closeCurly
-
-many1H :: Parser a -> Parser (NonEmpty a)
-many1H = fmap NonEmpty.fromList . P.some
-
--- | 'sepBy1HFinal' is like 'sepBy1H' but also tries to parse a last separator
-sepBy1HFinal :: Parser a -> Parser s -> Parser (NonEmpty a)
-sepBy1HFinal parse sep = sepBy1H parse sep <* P.optional sep
-
-sepBy1 :: Parser a -> Parser s -> Parser [a]
-sepBy1 p sep = liftA2 (:) p (many (P.try $ sep *> p))
-
-sepBy1H :: Parser a -> Parser s -> Parser (NonEmpty a)
-sepBy1H parse sep = NonEmpty.fromList <$> sepBy1 parse sep
-
-skipLiner :: Word8 -> Parser ()
-skipLiner p = spaceLiner (P.skipCount 1 (P.char p))
-
-maybeParend :: Parser a -> Parser a
-maybeParend p = p <|> parens p
-
-integer :: Parser Integer
-integer = do
-  digits <- P.takeWhileP (Just "digits") isDigit
-  case Char8.readInteger digits of
-    Just (x, _) -> pure x
-    Nothing -> fail $ "didn't parse an int"

src/MiniJuvix/Utils/Parser/Token.hs

@@ -1,209 +0,0 @@
-module MiniJuvix.Utils.Parser.Token
-  ( charToWord8,
-    wordToChr,
-    dash,
-    under,
-    space,
-    colon,
-    semi,
-    comma,
-    hash,
-    backSlash,
-    quote,
-    doubleQuote,
-    pipe,
-    equals,
-    at,
-    question,
-    dot,
-    bang,
-    amper,
-    times,
-    exp,
-    backtick,
-    div,
-    percent,
-    newLine,
-    openBracket,
-    closeBracket,
-    openParen,
-    closeParen,
-    openCurly,
-    closeCurly,
-    validStartSymbol,
-    validMiddleSymbol,
-    validInfixSymbol,
-    validUpperSymbol,
-    reservedSymbols,
-    reservedWords,
-    endOfLine,
-  )
-where
-
---------------------------------------------------------------------------------
-
--- import qualified Data.Set as Set
--- import Data.Word8 (isDigit)
-import qualified GHC.Unicode as Unicode
-import MiniJuvix.Utils.Prelude hiding (div, exp, hash, maybe, option, takeWhile)
-
---------------------------------------------------------------------------------
-
-charToWord8 :: Char -> Word8
-charToWord8 = fromIntegral . ord
-{-# INLINE charToWord8 #-}
-
-wordToChr :: Integral a => a -> Char
-wordToChr = chr . fromIntegral
-
--- Hopefully this is fast!
-validStartSymbol' :: Integral a => a -> Bool
-validStartSymbol' = Unicode.isAlpha . wordToChr
-
--- Unicode.isUpper 'İ' = True!
-validUpperSymbol :: Integral a => a -> Bool
-validUpperSymbol = Unicode.isUpper . wordToChr
-
-dash :: Word8
-dash = charToWord8 '-'
-
-under :: Word8
-under = charToWord8 '_'
-
-space :: Word8
-space = charToWord8 ' '
-
-colon :: Word8
-colon = charToWord8 ':'
-
-semi :: Word8
-semi = charToWord8 ';'
-
-comma :: Word8
-comma = charToWord8 ','
-
-hash :: Word8
-hash = charToWord8 '#'
-
-openParen :: Word8
-openParen = charToWord8 '('
-
-closeParen :: Word8
-closeParen = charToWord8 ')'
-
-openCurly :: Word8
-openCurly = charToWord8 '{'
-
-closeCurly :: Word8
-closeCurly = charToWord8 '}'
-
-openBracket :: Word8
-openBracket = charToWord8 '['
-
-closeBracket :: Word8
-closeBracket = charToWord8 ']'
-
-backSlash :: Word8
-backSlash = charToWord8 '\\'
-
-quote :: Word8
-quote = charToWord8 '\''
-
-doubleQuote :: Word8
-doubleQuote = charToWord8 '\"'
-
-pipe :: Word8
-pipe = charToWord8 '|'
-
-equals :: Word8
-equals = charToWord8 '='
-
-at :: Word8
-at = charToWord8 '@'
-
-dot :: Word8
-dot = charToWord8 '.'
-
-question :: Word8
-question = charToWord8 '?'
-
-bang :: Word8
-bang = charToWord8 '!'
-
-amper :: Word8
-amper = charToWord8 '&'
-
-times :: Word8
-times = charToWord8 '*'
-
-exp :: Word8
-exp = charToWord8 '^'
-
-backtick :: Word8
-backtick = charToWord8 '`'
-
-newLine :: Word8
-newLine = charToWord8 '\n'
-
-div :: Word8
-div = charToWord8 '/'
-
-percent :: Word8
-percent = charToWord8 '%'
-
-validStartSymbol :: Word8 -> Bool
-validStartSymbol w =
-  validStartSymbol' w || w == under
-
-validInfixSymbol :: Word8 -> Bool
-validInfixSymbol w =
-  Unicode.isSymbol (wordToChr w)
-    || w == times
-    || w == exp
-    || w == dash
-    || w == amper
-    || w == colon
-    || w == div
-    || w == percent
-    || w == dot
-
-validMiddleSymbol :: Word8 -> Bool
-validMiddleSymbol w =
-  validStartSymbol w
-    || isDigit w
-    || w == dash
-    || w == bang
-    || w == question
-    || w == percent
-
--- check for \r or \n
-endOfLine :: (Eq a, Num a) => a -> Bool
-endOfLine w = w == 13 || w == 10
-
-reservedWords :: (Ord a, IsString a) => Set a
-reservedWords =
-  Set.fromList
-    [ "let",
-      "val",
-      "type",
-      "case",
-      "in",
-      "open",
-      "if",
-      "cond",
-      "end",
-      "of",
-      "begin",
-      "sig",
-      "mod",
-      "declare",
-      "where",
-      "via",
-      "handler",
-      "effect"
-    ]
-
-reservedSymbols :: (Ord a, IsString a) => Set a
-reservedSymbols =
-  Set.fromList
-    ["=", "|", "", "--"]

src/MiniJuvix/Utils/Prelude.hs

@@ -1,691 +1,92 @@
+{-# LANGUAGE RankNTypes #-}
+
+{-
+* This Predude is =Protolude= except with a few changes
+  + _Additions_
+    * ∨   :: Serves as an or function
+    * ∧   :: Serves as an and function
+    * |<< :: Serves as a map function
+    * >>| :: Serves as the flip map function
+  + _Changes_
+    * The Capability library is imported and replaces the standard
+      =MTL= constructs in =Protolude=
+    * We don't import the Semiring typeclass from =Protolude=.
+-}
+
+-- | Adapted from heliaxdev/Juvix/library/StandardLibrary/src/Juvix/Library.hs
 module MiniJuvix.Utils.Prelude
-  ( String,
-    module Protolude,
-    Semiring (..),
+  ( module MiniJuvix.Utils.Prelude,
+    module Relude,
   )
 where
 
 --------------------------------------------------------------------------------
 
-import Protolude
-  ( ($),
-    -- Type,
-
-    -- type (:+:)(..),
-    -- type (:*:)(..),
-    -- type (:.:)(..),
-
-    ($!),
-    ($!!),
-    ($>),
-    (%),
-    (&),
-    (&&),
-    (&&^),
-    (++),
-    (.),
-    (<$!>),
-    (<$>),
-    (<&&>),
-    (<&>),
-    (<**>),
-    (<<$>>),
-    (<<*>>),
-    (<=<),
-    (<||>),
-    (=<<),
-    (>=>),
-    All (..),
-    -- type (:~:)(..),
-    -- type (==),
-
-    AllocationLimitExceeded (..),
-    Alt (..),
-    Alternative (..),
-    Any (..),
-    Ap (..),
-    Applicative (..),
-    ArithException (..),
-    ArrayException (..),
-    AssertionFailed (..),
-    Associativity (..),
-    Async (..),
-    AsyncException (..),
-    Bifunctor (..),
-    Bits (..),
-    BlockedIndefinitelyOnMVar (..),
-    BlockedIndefinitelyOnSTM (..),
-    Bool (..),
-    Bounded (..),
-    ByteString,
-    C1,
-    CallStack,
-    Chan,
-    Char,
-    CmpNat,
-    Coercible,
-    Coercion (..),
-    CompactionFailed (..),
-    Complex (..),
-    Concurrently (..),
-    Const (..),
-    Constraint,
-    Constructor (..),
-    ConvertText (..),
-    D1,
-    Datatype (..),
-    Deadlock (..),
-    Double (..),
-    Down (..),
-    Dual (..),
-    Either (..),
-    Endo (..),
-    Enum (..),
-    Eq (..),
-    ErrorCall (..),
-    Except,
-    ExceptT (..),
-    Exception (..),
-    ExitCode (..),
-    FatalError (..),
-    FilePath,
-    FiniteBits (..),
-    First (..),
-    Fixity (..),
-    FixityI (..),
-    Float (..),
-    Floating (..),
-    Foldable (..),
-    Fractional (..),
-    FunPtr,
-    Functor (..),
-    Generic (..),
-    Generic1,
-    Handle,
-    Handler (..),
-    HasCallStack,
-    HasField (..),
-    Hashable (..),
-    IO,
-    IOException,
-    IOMode (..),
-    Identity (..),
-    Int,
-    Int16,
-    Int32,
-    Int64,
-    Int8,
-    IntMap,
-    IntPtr,
-    IntSet,
-    Integer,
-    Integral (..),
-    IsLabel (..),
-    IsString,
-    K1 (..),
-    KnownNat,
-    KnownSymbol,
-    LByteString,
-    LText,
-    Last (..),
-    Location (..),
-    M1 (..),
-    MVar,
-    Map,
-    MaskingState (..),
-    Maybe (..),
-    Meta (..),
-    Monad (..),
-    MonadError (..),
-    MonadFail,
-    MonadIO (..),
-    MonadPlus (..),
-    MonadReader (..),
-    MonadState (..),
-    Monoid (..),
-    NFData (..),
-    Nat,
-    NestedAtomically (..),
-    NoMethodError (..),
-    NonEmpty (..),
-    NonTermination (..),
-    Num (..),
-    OnDecodeError,
-    OnError,
-    Option (..),
-    Ord (..),
-    Ordering (..),
-    PatternMatchFail (..),
-    Print (..),
-    Product (..),
-    Proxy (..),
-    Ptr,
-    QSem,
-    QSemN,
-    Ratio,
-    Rational,
-    Read,
-    Reader,
-    ReaderT (..),
-    Real (..),
-    RealFloat (..),
-    RealFrac (..),
-    Rec0,
-    RecConError (..),
-    RecSelError (..),
-    RecUpdError (..),
-    S1,
-    ST,
-    STM,
-    Selector (..),
-    Semigroup (..),
-    Seq,
-    Set,
-    Show,
-    SomeAsyncException (..),
-    SomeException (..),
-    SomeNat (..),
-    SomeSymbol (..),
-    SrcLoc (..),
-    StablePtr,
-    State,
-    StateT (..),
-    StaticPtr,
-    Storable,
-    Sum (..),
-    Symbol,
-    Text,
-    ThreadId,
-    Traversable (..),
-    TypeError (..),
-    TypeRep,
-    Typeable,
-    U1 (..),
-    URec,
-    UnicodeException,
-    V1,
-    Void,
-    Word,
-    Word16,
-    Word32,
-    Word64,
-    Word8,
-    WordPtr,
-    WrappedMonoid,
-    ZipList (..),
-    (^),
-    (^%^),
-    (^^),
-    (^^%^^),
-    absurd,
-    addMVarFinalizer,
-    all,
-    allowInterrupt,
-    and,
-    any,
-    ap,
-    appendFile,
-    applyN,
-    asTypeOf,
-    asks,
-    asum,
-    async,
-    asyncBound,
-    asyncExceptionFromException,
-    asyncExceptionToException,
-    asyncOn,
-    atDef,
-    atMay,
-    atomically,
-    bitDefault,
-    bool,
-    boundedEnumFrom,
-    boundedEnumFromThen,
-    bracket,
-    bracketOnError,
-    bracket_,
-    break,
-    byteSwap16,
-    byteSwap32,
-    byteSwap64,
-    callStack,
-    cancel,
-    cancelWith,
-    cast,
-    castWith,
-    catMaybes,
-    catch,
-    catchE,
-    catchJust,
-    catchSTM,
-    catches,
-    check,
-    chr,
-    cis,
-    coerceWith,
-    comparing,
-    concat,
-    concatMap,
-    concatMapM,
-    concurrently,
-    conjugate,
-    const,
-    currentCallStack,
-    curry,
-    cycle,
-    cycle1,
-    decodeUtf8,
-    decodeUtf8',
-    decodeUtf8With,
-    deepseq,
-    denominator,
-    die,
-    diff,
-    digitToInt,
-    divZeroError,
-    drop,
-    dropWhile,
-    dupChan,
-    either,
-    eitherA,
-    encodeUtf8,
-    eqT,
-    evalState,
-    evalStateT,
-    evaluate,
-    even,
-    execState,
-    execStateT,
-    exitFailure,
-    exitSuccess,
-    exitWith,
-    filter,
-    filterM,
-    finally,
-    find,
-    fix,
-    fixST,
-    flip,
-    fmapDefault,
-    foldM,
-    foldM_,
-    foldMapDefault,
-    foldl1May,
-    foldl1May',
-    foldlM,
-    foldr1May,
-    foldrM,
-    for,
-    forM,
-    forM_,
-    for_,
-    force,
-    foreach,
-    forever,
-    forkFinally,
-    forkIO,
-    forkIOWithUnmask,
-    forkOS,
-    forkOSWithUnmask,
-    forkOn,
-    forkOnWithUnmask,
-    fromIntegral,
-    fromLeft,
-    fromMaybe,
-    fromRight,
-    fromStrict,
-    fst,
-    gcast,
-    gcastWith,
-    gcd,
-    gcdInt',
-    gcdWord',
-    genericDrop,
-    genericLength,
-    genericReplicate,
-    genericSplitAt,
-    genericTake,
-    getArgs,
-    getCallStack,
-    getChanContents,
-    getContents,
-    getLine,
-    getMaskingState,
-    getNumCapabilities,
-    getStackTrace,
-    gets,
-    group,
-    groupBy,
-    guard,
-    guardM,
-    guarded,
-    guardedA,
-    handle,
-    handleJust,
-    hashUsing,
-    head,
-    headDef,
-    headMay,
-    hush,
-    identity,
-    ifM,
-    ignore,
-    imagPart,
-    infinity,
-    initDef,
-    initMay,
-    initSafe,
-    inits,
-    intToDigit,
-    integralEnumFrom,
-    integralEnumFromThen,
-    integralEnumFromThenTo,
-    integralEnumFromTo,
-    interact,
-    intercalate,
-    interruptible,
-    intersperse,
-    ioError,
-    isAlpha,
-    isAlphaNum,
-    isAscii,
-    isControl,
-    isCurrentThreadBound,
-    isDigit,
-    isEmptyMVar,
-    isHexDigit,
-    isJust,
-    isLeft,
-    isLetter,
-    isLower,
-    isNothing,
-    isPrefixOf,
-    isPrint,
-    isRight,
-    isSpace,
-    isUpper,
-    iterate,
-    join,
-    killThread,
-    lastDef,
-    lastMay,
-    lcm,
-    leftToMaybe,
-    lefts,
-    lenientDecode,
-    lift,
-    liftA,
-    liftA3,
-    liftAA2,
-    liftIO1,
-    liftIO2,
-    liftM,
-    liftM',
-    liftM2,
-    liftM2',
-    liftM3,
-    liftM4,
-    liftM5,
-    lines,
-    link,
-    link2,
-    list,
-    listToMaybe,
-    magnitude,
-    map,
-    mapAccumL,
-    mapAccumR,
-    mapAndUnzipM,
-    mapExcept,
-    mapExceptT,
-    mapException,
-    mapM_,
-    mapMaybe,
-    mask,
-    mask_,
-    maxInt,
-    maximumBy,
-    maximumDef,
-    maximumMay,
-    maybe,
-    maybeEmpty,
-    maybeToEither,
-    maybeToLeft,
-    maybeToList,
-    maybeToRight,
-    mfilter,
-    minInt,
-    minimumBy,
-    minimumDef,
-    minimumMay,
-    mkPolar,
-    mkWeakMVar,
-    mkWeakThreadId,
-    modify,
-    modifyMVar,
-    modifyMVarMasked,
-    modifyMVarMasked_,
-    modifyMVar_,
-    msum,
-    mtimesDefault,
-    myThreadId,
-    natVal,
-    newChan,
-    newEmptyMVar,
-    newMVar,
-    newQSem,
-    newQSemN,
-    nonEmpty,
-    not,
-    notANumber,
-    notElem,
-    notImplemented,
-    note,
-    numerator,
-    numericEnumFrom,
-    numericEnumFromThen,
-    numericEnumFromThenTo,
-    numericEnumFromTo,
-    odd,
-    on,
-    onException,
-    openFile,
-    option,
-    optional,
-    or,
-    orAlt,
-    orElse,
-    orEmpty,
-    ord,
-    ordNub,
-    otherwise,
-    overflowError,
-    panic,
-    partitionEithers,
-    pass,
-    permutations,
-    phase,
-    polar,
-    poll,
-    popCountDefault,
-    prettyCallStack,
-    prettySrcLoc,
-    print,
-    product,
-    purer,
-    putByteString,
-    putErrText,
-    putLByteString,
-    putLText,
-    putMVar,
-    putText,
-    race,
-    race_,
-    ratioPrec,
-    ratioPrec1,
-    ratioZeroDenominatorError,
-    readChan,
-    readEither,
-    readFile,
-    readMVar,
-    readMaybe,
-    reads,
-    realPart,
-    realToFrac,
-    reduce,
-    repeat,
-    replace,
-    replicate,
-    replicateM,
-    replicateM_,
-    repr,
-    retry,
-    reverse,
-    rightToMaybe,
-    rights,
-    rtsSupportsBoundThreads,
-    runExcept,
-    runExceptT,
-    runInBoundThread,
-    runInUnboundThread,
-    runReader,
-    runST,
-    runState,
-    scanl,
-    scanl',
-    scanr,
-    seq,
-    sequenceA_,
-    sequence_,
-    setNumCapabilities,
-    show,
-    showStackTrace,
-    signalQSem,
-    signalQSemN,
-    snd,
-    someNatVal,
-    someSymbolVal,
-    sort,
-    sortBy,
-    sortOn,
-    splitAt,
-    stderr,
-    stdin,
-    stdout,
-    stimesIdempotent,
-    stimesIdempotentMonoid,
-    stimesMonoid,
-    strictDecode,
-    subsequences,
-    subtract,
-    sum,
-    swap,
-    swapMVar,
-    sym,
-    symbolVal,
-    tailDef,
-    tailMay,
-    tailSafe,
-    tails,
-    take,
-    takeMVar,
-    takeWhile,
-    testBitDefault,
-    threadCapability,
-    threadDelay,
-    threadWaitRead,
-    threadWaitReadSTM,
-    threadWaitWrite,
-    threadWaitWriteSTM,
-    throwE,
-    throwIO,
-    throwSTM,
-    throwTo,
-    toIntegralSized,
-    toLower,
-    toStrict,
-    toTitle,
-    toUpper,
-    toUtf8,
-    toUtf8Lazy,
-    trace,
-    traceIO,
-    traceId,
-    traceM,
-    traceShow,
-    traceShowId,
-    traceShowM,
-    trans,
-    transpose,
-    traverse_,
-    try,
-    tryIO,
-    tryJust,
-    tryPutMVar,
-    tryReadMVar,
-    tryTakeMVar,
-    typeOf,
-    typeRep,
-    uncons,
-    uncurry,
-    undefined,
-    underflowError,
-    unfoldr,
-    uninterruptibleMask,
-    uninterruptibleMask_,
-    unless,
-    unlessM,
-    unlines,
-    unsnoc,
-    until,
-    unwords,
-    unzip,
-    vacuous,
-    void,
-    wait,
-    waitAny,
-    waitAnyCancel,
-    waitAnyCatch,
-    waitAnyCatchCancel,
-    waitBoth,
-    waitCatch,
-    waitEither,
-    waitEitherCancel,
-    waitEitherCatch,
-    waitEitherCatchCancel,
-    waitEither_,
-    waitQSem,
-    waitQSemN,
-    when,
-    whenM,
-    withAsync,
-    withAsyncBound,
-    withAsyncOn,
-    withExcept,
-    withExceptT,
-    withFile,
-    withFrozenCallStack,
-    withMVar,
-    withMVarMasked,
-    withState,
-    witness,
-    words,
-    writeChan,
-    writeFile,
-    writeList2Chan,
-    yield,
-    zero,
-    zip,
-    zipWith,
-    zipWithM,
-    zipWithM_,
-    (||),
-    (||^),
+import qualified Data.Char as Char
+import Relude hiding
+  ( one,
   )
-import Protolude.Base ()
-import Prelude (String)
+
+import safe Relude.Container
 
 --------------------------------------------------------------------------------
+-- Logical connectives
+--------------------------------------------------------------------------------
+
+(∨) :: Bool -> Bool -> Bool
+(∨) = (||)
+
+infixr 2 ∨
+
+(∧) :: Bool -> Bool -> Bool
+(∧) = (&&)
+
+infixr 3 ∧
+
+--------------------------------------------------------------------------------
+-- High-level syntax sugar.
+--------------------------------------------------------------------------------
+
+-- Lift a map.
+(|<<) ::
+  forall a b f.
+  (Functor f) =>
+  (a -> b) ->
+  -----------
+  f a ->
+  f b
+(|<<) = fmap
+
+infixr 1 |<<
+
+-- Apply a lifted map.
+(>>|) :: forall a b f. (Functor f) => f a -> (a -> b) -> f b
+(>>|) = flip fmap
+
+infixl 1 >>|
+
+-- Postfix funciton application.
+(|>) :: a -> (a -> b) -> b
+(|>) = (&)
+
+infixl 1 |>
+
+--------------------------------------------------------------------------------
+
+traverseM ::
+  (Monad m, Traversable m, Applicative f) =>
+  (a1 -> f (m a2)) ->
+  m a1 ->
+  f (m a2)
+traverseM f = fmap join . traverse f
+
+--------------------------------------------------------------------------------
+-- String related util functions.
+--------------------------------------------------------------------------------
+
+toUpperFirst :: String -> String
+toUpperFirst [] = []
+toUpperFirst (x : xs) = Char.toUpper x : xs
 
 --------------------------------------------------------------------------------
 -- Semiring

src/MiniJuvix/Utils/Pretty.hs

@@ -8,7 +8,6 @@ module MiniJuvix.Utils.Pretty
     hardlines,
     format,
     annotateSpecialSymbol,
-    printList,
   )
 where