mirror of
https://github.com/anoma/juvix.git
synced 2025-01-06 06:53:33 +03:00
Merge branch 'jan' into qtt
This commit is contained in:
Jan Mas Rovira
commit
18ec026605
81
app/Main.hs
81
app/Main.hs
@ -2,7 +2,8 @@
|
||||
|
||||
module Main (main) where
|
||||
|
||||
import Data.Aeson (defaultOptions)
|
||||
import Control.Monad.Extra
|
||||
import qualified MiniJuvix.Syntax.Concrete.Language as M
|
||||
import qualified MiniJuvix.Syntax.Concrete.Parser as M
|
||||
import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi as M
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (Options (_optShowNameId))
|
||||
@ -11,6 +12,8 @@ import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M
|
||||
import MiniJuvix.Utils.Prelude
|
||||
import Options.Applicative
|
||||
import Options.Applicative.Help.Pretty
|
||||
import System.IO.Error
|
||||
import Text.Show.Pretty
|
||||
|
||||
data Command
|
||||
= Scope ScopeOptions
|
||||
@ -23,6 +26,24 @@ data ScopeOptions = ScopeOptions
|
||||
}
|
||||
|
||||
data ParseOptions = ParseOptions
|
||||
{ _parseInputFile :: FilePath,
|
||||
_parseNoPrettyShow :: Bool
|
||||
}
|
||||
|
||||
parseParse :: Parser ParseOptions
|
||||
parseParse = do
|
||||
_parseInputFile <-
|
||||
argument
|
||||
str
|
||||
( metavar "MINIJUVIX_FILE"
|
||||
<> help "Path to a .mjuvix file"
|
||||
)
|
||||
_parseNoPrettyShow <-
|
||||
switch
|
||||
( long "no-pretty-show"
|
||||
<> help "Disable formatting of the Haskell AST"
|
||||
)
|
||||
pure ParseOptions {..}
|
||||
|
||||
parseScope :: Parser ScopeOptions
|
||||
parseScope = do
|
||||
@ -49,28 +70,46 @@ parseScope = do
|
||||
|
||||
pure ScopeOptions {..}
|
||||
|
||||
parseParse :: Parser ParseOptions
|
||||
parseParse = pure ParseOptions
|
||||
|
||||
descr :: ParserInfo Command
|
||||
descr =
|
||||
info
|
||||
(parseCommand <**> helper)
|
||||
( fullDesc
|
||||
<> progDesc "The MiniJuvix compiler."
|
||||
<> headerDoc (Just $ dullblue $ bold $ underline "MiniJuvix help")
|
||||
<> headerDoc (Just headDoc)
|
||||
<> footerDoc (Just foot)
|
||||
)
|
||||
where
|
||||
headDoc :: Doc
|
||||
headDoc = dullblue $ bold $ underline "MiniJuvix help"
|
||||
foot :: Doc
|
||||
foot = bold "maintainers: " <> "jan@heliax.dev; jonathan@heliax.dev"
|
||||
|
||||
parseCommand :: Parser Command
|
||||
parseCommand =
|
||||
subparser
|
||||
( command "parse" (info (Parse <$> parseParse) (progDesc "Parse some .mjuvix files"))
|
||||
<> command "scope" (info (Scope <$> parseScope) (progDesc "Parse and scope some .mjuvix files"))
|
||||
)
|
||||
hsubparser $
|
||||
mconcat
|
||||
[ commandParse,
|
||||
commandScope
|
||||
]
|
||||
where
|
||||
commandParse :: Mod CommandFields Command
|
||||
commandParse = command "parse" minfo
|
||||
where
|
||||
minfo :: ParserInfo Command
|
||||
minfo =
|
||||
info
|
||||
(Parse <$> parseParse)
|
||||
(progDesc "Parse a .mjuvix file")
|
||||
|
||||
commandScope :: Mod CommandFields Command
|
||||
commandScope = command "scope" minfo
|
||||
where
|
||||
minfo :: ParserInfo Command
|
||||
minfo =
|
||||
info
|
||||
(Scope <$> parseScope)
|
||||
(progDesc "Parse and scope a .mjuvix file")
|
||||
|
||||
mkPrettyOptions :: ScopeOptions -> M.Options
|
||||
mkPrettyOptions ScopeOptions {..} =
|
||||
@ -78,21 +117,21 @@ mkPrettyOptions ScopeOptions {..} =
|
||||
{ _optShowNameId = _scopeShowIds
|
||||
}
|
||||
|
||||
parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop)
|
||||
parseModuleIO = fromRightIO id . M.runModuleParserIO
|
||||
|
||||
fromRightIO :: (e -> Text) -> IO (Either e r) -> IO r
|
||||
fromRightIO pp = eitherM (ioError . userError . unpack . pp) return
|
||||
|
||||
go :: Command -> IO ()
|
||||
go c = case c of
|
||||
Scope opts@ScopeOptions {..} -> do
|
||||
res <- M.runModuleParserIO _scopeInputFile
|
||||
case res of
|
||||
Left err -> print err
|
||||
Right m -> do
|
||||
print m
|
||||
putStrLn "\n\n"
|
||||
s <- M.scopeCheck _scopeInputFile [m]
|
||||
case s of
|
||||
Left err -> print err
|
||||
Right [r] -> M.printTopModule (mkPrettyOptions opts) r
|
||||
Right _ -> error "impossible"
|
||||
Parse _ -> putStrLn "not implemented"
|
||||
m <- parseModuleIO _scopeInputFile
|
||||
s <- fromRightIO show $ M.scopeCheck1 _scopeInputFile m
|
||||
M.printTopModule (mkPrettyOptions opts) s
|
||||
Parse ParseOptions {..} -> do
|
||||
m <- parseModuleIO _parseInputFile
|
||||
if _parseNoPrettyShow then print m else pPrint m
|
||||
|
||||
main :: IO ()
|
||||
main = execParser descr >>= go
|
||||
|
||||
@ -21,8 +21,10 @@ dependencies:
|
||||
- base == 4.15.*
|
||||
- bytestring == 0.10.*
|
||||
- containers == 0.6.*
|
||||
- directory == 1.3.*
|
||||
- extra == 1.7.*
|
||||
- filepath == 1.4.*
|
||||
- hashable == 1.3.*
|
||||
- megaparsec == 9.2.*
|
||||
- microlens-platform == 0.4.*
|
||||
- parser-combinators == 1.3.*
|
||||
@ -31,7 +33,6 @@ dependencies:
|
||||
- prettyprinter == 1.7.*
|
||||
- prettyprinter-ansi-terminal == 1.1.*
|
||||
- process == 1.6.*
|
||||
- relude == 1.0.*
|
||||
- semirings == 0.6.*
|
||||
- singletons == 3.0.*
|
||||
- Stream == 0.4.*
|
||||
@ -78,6 +79,7 @@ executables:
|
||||
dependencies:
|
||||
- MiniJuvix
|
||||
- optparse-applicative == 0.16.*
|
||||
- pretty-show == 1.10.*
|
||||
|
||||
tests:
|
||||
MiniJuvix-test:
|
||||
|
||||
@ -25,7 +25,7 @@ stylize a = case a of
|
||||
KNameInductive -> colorDull Green
|
||||
KNameAxiom -> colorDull Red
|
||||
KNameLocalModule -> mempty
|
||||
KNameFunction -> mempty
|
||||
KNameFunction -> colorDull Yellow
|
||||
KNameLocal -> mempty
|
||||
AnnDelimiter -> mempty
|
||||
AnnDelimiter -> colorDull White
|
||||
AnnKeyword -> colorDull Blue
|
||||
|
||||
@ -3,9 +3,7 @@ module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base where
|
||||
import Data.Singletons
|
||||
import MiniJuvix.Syntax.Concrete.Language
|
||||
import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
|
||||
import MiniJuvix.Utils.Prelude hiding (Reader, asks, runReader)
|
||||
import Polysemy
|
||||
import Polysemy.Reader
|
||||
import MiniJuvix.Utils.Prelude
|
||||
import Prettyprinter hiding (braces, parens)
|
||||
|
||||
data Ann
|
||||
@ -353,11 +351,13 @@ ppLambda Lambda {..} = do
|
||||
ppFunctionClause :: forall r. Members '[Reader Options] r => FunctionClause 'Scoped -> Sem r (Doc Ann)
|
||||
ppFunctionClause FunctionClause {..} = do
|
||||
clauseOwnerFunction' <- ppSSymbol clauseOwnerFunction
|
||||
clausePatterns' <- hsep <$> mapM ppPattern clausePatterns
|
||||
clausePatterns' <- case nonEmpty clausePatterns of
|
||||
Nothing -> return Nothing
|
||||
Just ne -> Just . hsep . toList <$> mapM ppPattern ne
|
||||
clauseBody' <- ppExpression clauseBody
|
||||
clauseWhere' <- sequence $ ppWhereBlock <$> clauseWhere
|
||||
return $
|
||||
clauseOwnerFunction' <+> clausePatterns' <+> kwAssignment <+> clauseBody'
|
||||
clauseOwnerFunction' <+?> clausePatterns' <+> kwAssignment <+> clauseBody'
|
||||
<+?> (((line <> kwWhere) <+>) <$> clauseWhere')
|
||||
where
|
||||
ppWhereBlock :: WhereBlock 'Scoped -> Sem r (Doc Ann)
|
||||
@ -438,7 +438,7 @@ ppPattern = goAtom
|
||||
ppPatternPostfixApp PatternPostfixApp {..} = do
|
||||
patPostfixConstructor' <- ppSName patPostfixConstructor
|
||||
patPostfixParameter' <- goAtom patPostfixParameter
|
||||
return $ patPostfixConstructor' <+> patPostfixParameter'
|
||||
return $ patPostfixParameter' <+> patPostfixConstructor'
|
||||
|
||||
ppExpressionAtom :: forall r. Members '[Reader Options] r => Expression -> Sem r (Doc Ann)
|
||||
ppExpressionAtom e = do
|
||||
|
||||
@ -8,7 +8,6 @@ module MiniJuvix.Syntax.Concrete.Scoped.Scoper where
|
||||
import qualified Control.Monad.Combinators.Expr as P
|
||||
import qualified Data.HashMap.Strict as HashMap
|
||||
import qualified Data.HashSet as HashSet
|
||||
import Data.Stream (Stream)
|
||||
import qualified Data.Stream as Stream
|
||||
import qualified Data.Text as Text
|
||||
import Lens.Micro.Platform
|
||||
@ -17,12 +16,7 @@ import MiniJuvix.Syntax.Concrete.Language
|
||||
import MiniJuvix.Syntax.Concrete.Parser (runModuleParserIO)
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Name (NameKind (KNameConstructor))
|
||||
import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
|
||||
import MiniJuvix.Utils.Prelude hiding (Reader, State, ask, asks, evalState, get, gets, local, modify, put, runReader, runState)
|
||||
import Polysemy
|
||||
import Polysemy.Error hiding (fromEither)
|
||||
import Polysemy.NonDet
|
||||
import Polysemy.Reader
|
||||
import Polysemy.State
|
||||
import MiniJuvix.Utils.Prelude
|
||||
import System.FilePath
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
@ -68,7 +62,6 @@ data SymbolEntry = SymbolEntry
|
||||
data Scope = Scope
|
||||
{ _scopePath :: S.AbsModulePath,
|
||||
_scopeFixities :: HashMap Symbol Fixity,
|
||||
_scopeUsedFixities :: HashSet Symbol,
|
||||
_scopeSymbols :: HashMap Symbol SymbolInfo,
|
||||
_scopeModules :: HashMap QualifiedName ModuleScopeInfo,
|
||||
_scopeBindGroup :: HashMap Symbol LocalVariable
|
||||
@ -92,8 +85,7 @@ data ScopeError
|
||||
= ErrParser Text
|
||||
| Err
|
||||
| ErrInfixParser String
|
||||
| ErrPattern String
|
||||
| ErrPatternUnfold
|
||||
| ErrInfixPattern String
|
||||
| ErrAlreadyDefined Symbol
|
||||
| ErrLacksTypeSig Symbol
|
||||
| ErrImportCycle TopModulePath
|
||||
@ -122,7 +114,10 @@ data ScopeState = ScopeState
|
||||
|
||||
makeLenses ''ScopeState
|
||||
|
||||
scopeCheck :: FilePath -> [Module 'Parsed 'ModuleTop] -> IO (Either ScopeError [Module 'Scoped 'ModuleTop])
|
||||
scopeCheck1 :: FilePath -> Module 'Parsed 'ModuleTop -> IO (Either ScopeError (Module 'Scoped 'ModuleTop))
|
||||
scopeCheck1 root m = fmap head <$> scopeCheck root (pure m)
|
||||
|
||||
scopeCheck :: FilePath -> NonEmpty (Module 'Parsed 'ModuleTop) -> IO (Either ScopeError (NonEmpty (Module 'Scoped 'ModuleTop)))
|
||||
scopeCheck root modules =
|
||||
runM $
|
||||
runError $
|
||||
@ -170,14 +165,7 @@ freshSymbol _nameKind _nameConcrete = do
|
||||
getFixity :: Sem r S.NameFixity
|
||||
getFixity
|
||||
| S.canHaveFixity _nameKind = do
|
||||
mfix <- HashMap.lookup _nameConcrete <$> gets _scopeFixities
|
||||
case mfix of
|
||||
Nothing -> return S.NoFixity
|
||||
Just fixity -> do
|
||||
-- deleting the fixity so we know it has been used
|
||||
modify (over scopeFixities (HashMap.delete _nameConcrete))
|
||||
modify (over scopeUsedFixities (HashSet.insert _nameConcrete))
|
||||
return (S.SomeFixity fixity)
|
||||
maybe S.NoFixity S.SomeFixity . HashMap.lookup _nameConcrete <$> gets _scopeFixities
|
||||
| otherwise = return S.NoFixity
|
||||
|
||||
reserveSymbolOf ::
|
||||
@ -355,11 +343,7 @@ checkOperatorSyntaxDef OperatorSyntaxDef {..} = do
|
||||
checkNotDefined :: Sem r ()
|
||||
checkNotDefined =
|
||||
whenM
|
||||
( orM
|
||||
[ HashSet.member opSymbol <$> gets _scopeUsedFixities,
|
||||
HashMap.member opSymbol <$> gets _scopeFixities
|
||||
]
|
||||
)
|
||||
(HashMap.member opSymbol <$> gets _scopeFixities)
|
||||
(throw (ErrDuplicateFixity opSymbol))
|
||||
|
||||
checkTypeSignature ::
|
||||
@ -453,7 +437,6 @@ checkTopModule m@(Module path stmts) = do
|
||||
Scope
|
||||
{ _scopePath = getTopModulePath m,
|
||||
_scopeFixities = mempty,
|
||||
_scopeUsedFixities = mempty,
|
||||
_scopeSymbols = mempty,
|
||||
_scopeModules = mempty,
|
||||
_scopeBindGroup = mempty
|
||||
@ -485,6 +468,10 @@ checkLocalModule Module {..} = do
|
||||
moduleBody = moduleBody'
|
||||
}
|
||||
|
||||
-- | checks if there is an infix declaration without a binding.
|
||||
checkOrphanFixities :: Members '[Error ScopeError, State Scope] r => Sem r ()
|
||||
checkOrphanFixities = undefined
|
||||
|
||||
checkOpenModule ::
|
||||
forall r.
|
||||
Members '[Error ScopeError, State Scope] r =>
|
||||
@ -1180,7 +1167,7 @@ makePatternTable = do
|
||||
|
||||
parsePrePatTerm ::
|
||||
forall r.
|
||||
Members '[Reader (ParsePat Pattern), Embed ParsePat, NonDet] r =>
|
||||
Members '[Reader (ParsePat Pattern), Embed ParsePat] r =>
|
||||
Sem r Pattern
|
||||
parsePrePatTerm = do
|
||||
pPat <- ask
|
||||
@ -1257,9 +1244,9 @@ mkPatternParser table = embed @ParsePat pPattern
|
||||
pPattern :: ParsePat Pattern
|
||||
pPattern = P.makeExprParser pTerm table
|
||||
pTerm :: ParsePat Pattern
|
||||
pTerm = runM (runNonDet parseTermRec) >>= maybe mzero pure
|
||||
pTerm = runM parseTermRec
|
||||
where
|
||||
parseTermRec :: Sem '[NonDet, Embed ParsePat] Pattern
|
||||
parseTermRec :: Sem '[Embed ParsePat] Pattern
|
||||
parseTermRec = runReader pPattern parsePrePatTerm
|
||||
|
||||
parsePatternSection ::
|
||||
@ -1270,7 +1257,7 @@ parsePatternSection sec = do
|
||||
parser = runM (mkPatternParser tbl) <* P.eof
|
||||
res = P.parse parser filePath [sec]
|
||||
case res of
|
||||
Left err -> throw (ErrPattern (show err))
|
||||
Left err -> throw (ErrInfixPattern (show err))
|
||||
Right r -> return r
|
||||
where
|
||||
filePath = "tmp"
|
||||
|
||||
@ -6,7 +6,7 @@ module MiniJuvix.Syntax.Core where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import MiniJuvix.Utils.Prelude
|
||||
import MiniJuvix.Utils.Prelude hiding (Local)
|
||||
import Numeric.Natural (Natural)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -1,40 +0,0 @@
|
||||
module MiniJuvix.Typing.Error
|
||||
( Error (..),
|
||||
CheckingError (..),
|
||||
CommonError (..),
|
||||
)
|
||||
where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import MiniJuvix.Utils.Prelude
|
||||
import qualified Text.Show
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data CommonError
|
||||
= MissingVariable
|
||||
| QuantityError
|
||||
deriving stock (Show)
|
||||
|
||||
data CheckingError
|
||||
= ExpectUniverseType
|
||||
| ExpectPiType
|
||||
| ExpectTensorType
|
||||
| ExpectSumType
|
||||
deriving stock (Show)
|
||||
|
||||
-- ! TODO add the other possible cases..
|
||||
|
||||
data InferingError = InferingError
|
||||
deriving stock (Show)
|
||||
|
||||
data ErasingError = ErasingError
|
||||
deriving stock (Show)
|
||||
|
||||
data Error
|
||||
= CheckError CheckingError
|
||||
| InferError InferingError
|
||||
| ErasureError ErasingError
|
||||
| CommonError
|
||||
deriving stock (Show)
|
||||
@ -1,61 +0,0 @@
|
||||
module MiniJuvix.Typing.Typechecking () where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
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
|
||||
@ -1,62 +0,0 @@
|
||||
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
|
||||
@ -1,35 +1,106 @@
|
||||
{-
|
||||
* 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
|
||||
( module MiniJuvix.Utils.Prelude,
|
||||
module Data.List.Extra,
|
||||
module Control.Monad.Extra,
|
||||
module Relude,
|
||||
module Data.Char,
|
||||
module Data.Either.Extra,
|
||||
module Data.Function,
|
||||
module Data.List.Extra,
|
||||
module Data.Maybe,
|
||||
module Data.String,
|
||||
module Data.Text.Encoding,
|
||||
module GHC.Real,
|
||||
module Data.Tuple.Extra,
|
||||
module Data.Void,
|
||||
module GHC.Enum,
|
||||
module System.Directory,
|
||||
module System.FilePath,
|
||||
module Data.Singletons,
|
||||
module Data.Hashable,
|
||||
module GHC.Generics,
|
||||
module Data.Bool,
|
||||
module Data.List.NonEmpty,
|
||||
module Data.Traversable,
|
||||
module Data.Monoid,
|
||||
module Polysemy,
|
||||
module Polysemy.Reader,
|
||||
module Polysemy.State,
|
||||
module Polysemy.Error,
|
||||
module Polysemy.Embed,
|
||||
module Text.Show,
|
||||
module Data.Eq,
|
||||
module Data.Ord,
|
||||
module Data.Semigroup,
|
||||
module Data.Stream,
|
||||
module GHC.Num,
|
||||
module Data.Word,
|
||||
module Data.Functor,
|
||||
module Data.Int,
|
||||
module System.IO,
|
||||
module Control.Applicative,
|
||||
module Data.Foldable,
|
||||
Data,
|
||||
Text,
|
||||
pack,
|
||||
unpack,
|
||||
strip,
|
||||
HashMap,
|
||||
ByteString,
|
||||
HashSet,
|
||||
IsString (..),
|
||||
Alternative (..),
|
||||
)
|
||||
where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Control.Monad.Extra (maybeM)
|
||||
import Control.Applicative
|
||||
import Control.Monad.Extra
|
||||
import Data.Bool
|
||||
import Data.ByteString.Lazy (ByteString)
|
||||
import Data.Char
|
||||
import qualified Data.Char as Char
|
||||
import Data.List.Extra (groupSortOn, unsnoc)
|
||||
import Data.Data
|
||||
import Data.Either.Extra
|
||||
import Data.Eq
|
||||
import Data.Foldable
|
||||
import Data.Function
|
||||
import Data.Functor
|
||||
import Data.HashMap.Strict (HashMap)
|
||||
import Data.HashSet (HashSet)
|
||||
import Data.Hashable
|
||||
import Data.Int
|
||||
import Data.List.Extra hiding (head, last)
|
||||
import Data.List.NonEmpty (NonEmpty (..), head, last, nonEmpty)
|
||||
import qualified Data.List.NonEmpty as NonEmpty
|
||||
import Relude hiding
|
||||
( Type,
|
||||
one,
|
||||
)
|
||||
import Data.Maybe
|
||||
import Data.Monoid
|
||||
import Data.Ord
|
||||
import Data.Semigroup (Semigroup, (<>))
|
||||
import Data.Singletons
|
||||
import Data.Stream (Stream)
|
||||
import Data.String
|
||||
import Data.Text (Text, pack, strip, unpack)
|
||||
import Data.Text.Encoding
|
||||
import Data.Traversable
|
||||
import Data.Tuple.Extra
|
||||
import Data.Void
|
||||
import Data.Word
|
||||
import GHC.Enum
|
||||
import qualified GHC.Err as Err
|
||||
import GHC.Generics (Generic)
|
||||
import GHC.Num
|
||||
import GHC.Real
|
||||
import GHC.Stack.Types
|
||||
import Polysemy
|
||||
import Polysemy.Embed
|
||||
import Polysemy.Error hiding (fromEither)
|
||||
import Polysemy.Reader
|
||||
import Polysemy.State
|
||||
import System.Directory
|
||||
import System.FilePath
|
||||
import System.IO
|
||||
import Text.Show (Show)
|
||||
import qualified Text.Show as Show
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Logical connectives
|
||||
@ -89,6 +160,9 @@ traverseM f = fmap join . traverse f
|
||||
-- String related util functions.
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
show :: (Show a, IsString str) => a -> str
|
||||
show = fromString . Show.show
|
||||
|
||||
toUpperFirst :: String -> String
|
||||
toUpperFirst [] = []
|
||||
toUpperFirst (x : xs) = Char.toUpper x : xs
|
||||
@ -103,13 +177,6 @@ class Monoid m => Semiring m where
|
||||
one :: m
|
||||
times :: m -> m -> m
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Maybe
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
fromMaybeM :: Monad m => m a -> m (Maybe a) -> m a
|
||||
fromMaybeM n = maybeM n pure
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- NonEmpty
|
||||
--------------------------------------------------------------------------------
|
||||
@ -118,8 +185,11 @@ nonEmptyUnsnoc :: NonEmpty a -> (Maybe (NonEmpty a), a)
|
||||
nonEmptyUnsnoc e = (NonEmpty.nonEmpty (NonEmpty.init e), NonEmpty.last e)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Tuple
|
||||
-- Errors
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
mapFirst :: (a -> b) -> (a, d) -> (b, d)
|
||||
mapFirst f (a, b) = (f a, b)
|
||||
error :: HasCallStack => Text -> a
|
||||
error = Err.error . unpack
|
||||
|
||||
undefined :: HasCallStack => a
|
||||
undefined = Err.error "undefined"
|
||||
|
||||
@ -2,7 +2,8 @@ module MiniJuvix.Utils.Version (getVersion) where
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
import Control.Exception (IOException, try)
|
||||
import Control.Exception (IOException)
|
||||
import qualified Control.Exception as Exception
|
||||
import qualified Data.List as List
|
||||
import Data.Version (Version (versionTags))
|
||||
import MiniJuvix.Utils.Prelude
|
||||
@ -12,7 +13,7 @@ import System.Process (readProcessWithExitCode)
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
tryIO :: IO a -> IO (Either IOException a)
|
||||
tryIO = try
|
||||
tryIO = Exception.try
|
||||
|
||||
commitInfo :: IO (Maybe String)
|
||||
commitInfo = do
|
||||
|
||||
@ -54,11 +54,6 @@ inductive Empty {};
|
||||
-- An inductive type named Unit with only one constructor.
|
||||
inductive Unit { tt : Unit; };
|
||||
|
||||
inductive Nat' : Type
|
||||
{ zero : Nat' ;
|
||||
suc : Nat' -> Nat' ;
|
||||
};
|
||||
|
||||
-- The use of the type `Type` below is optional.
|
||||
-- The following declaration is equivalent to Nat'.
|
||||
|
||||
@ -86,8 +81,8 @@ inductive Fin (n : Nat) {
|
||||
-- The type of sized vectors.
|
||||
inductive Vec (n : Nat) (A : Type)
|
||||
{
|
||||
zero : Vec Nat.zero A;
|
||||
succ : A -> Vec n A -> Vec (Nat.succ n) A;
|
||||
zero : Vec zero A;
|
||||
succ : A -> Vec n A -> Vec (succ n) A;
|
||||
};
|
||||
|
||||
-- * Indexed inductive type declarations.
|
||||
@ -151,8 +146,8 @@ f' := \ {zero ↦ a ; -- We can use lambda abstractions to pattern match
|
||||
-- signature is missing.
|
||||
|
||||
g : Nat -> A;
|
||||
g Nat.zero := a;
|
||||
g (Nat.suc t) := a';
|
||||
g zero := a;
|
||||
g (suc t) := a';
|
||||
|
||||
-- For pattern-matching, the symbol `_` is the wildcard pattern as in
|
||||
-- Haskell or Agda. The following function definition is equivalent to
|
||||
@ -176,8 +171,8 @@ neg := A -> Empty;
|
||||
-- An equivalent type for sized vectors.
|
||||
|
||||
Vec' : Nat -> Type -> Type;
|
||||
Vec' Nat.zero A := Unit;
|
||||
Vec' (Nat.suc n) A := A -> Vec' n A;
|
||||
Vec' zero A := Unit;
|
||||
Vec' (suc n) A := A -> Vec' n A;
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Fixity notation similarly as in Agda or Haskell.
|
||||
@ -185,8 +180,8 @@ Vec' (Nat.suc n) A := A -> Vec' n A;
|
||||
|
||||
infixl 10 + ;
|
||||
+ : Nat → Nat → Nat ;
|
||||
+ Nat.zero m := m;
|
||||
+ (Nat.suc n) m := Nat.suc (n + m) ;
|
||||
+ zero m := m;
|
||||
+ (suc n) m := suc (n + m) ;
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Quantities for variables.
|
||||
|
||||
Loading…
Reference in New Issue
Block a user