mirror of
https://github.com/anoma/juvix.git
synced 2024-11-23 16:25:37 +03:00
w.i.p. adding ideal modules to cabal. Check compilation.
This commit is contained in:
Jonathan Prieto-Cubides
parent
99704af773
commit
fa5c8d77d4
@ -32,7 +32,7 @@
|
||||
# OTHER HINTS
|
||||
# --------------------------------------------------------------------------------
|
||||
|
||||
- warn: {name: Use explicit module export list}
|
||||
# - warn: {name: Use explicit module export list}
|
||||
|
||||
# --------------------------------------------------------------------------------
|
||||
# HINTS
|
||||
@ -52,6 +52,8 @@
|
||||
# --------------------------------------------------------------------------------
|
||||
|
||||
- ignore: {within: [MiniJuvix.Syntax.Core, MiniJuvix.Syntax.Eval]}
|
||||
- ignore: {within: [MiniJuvix.Monad]}
|
||||
- ignore: {within: [MiniJuvix.Pretty]}
|
||||
- ignore: {name: Use let, within: [Test.All]}
|
||||
- ignore: {name: Use String}
|
||||
- ignore: {name: Use String}
|
||||
- ignore: {name: Avoid restricted flags}
|
||||
@ -29,8 +29,18 @@ library
|
||||
MiniJuvix.Utils.Prelude
|
||||
MiniJuvix.Utils.Pretty
|
||||
MiniJuvix.Utils.Parser
|
||||
MiniJuvix.Parsing.ADT
|
||||
MiniJuvix.Parsing.Error
|
||||
MiniJuvix.Parsing.Location
|
||||
MiniJuvix.Parsing.Parser
|
||||
MiniJuvix.Desugaring.Error
|
||||
MiniJuvix.Typing.Typechecking
|
||||
MiniJuvix.Typing.Utils
|
||||
MiniJuvix.Typing.Error
|
||||
MiniJuvix.Error
|
||||
MiniJuvix.Pretty
|
||||
MiniJuvix.Pipeline
|
||||
MiniJuvix.Monad
|
||||
|
||||
hs-source-dirs: src
|
||||
other-modules: Paths_MiniJuvix
|
||||
|
||||
@ -2,4 +2,10 @@ module MiniJuvix.Desugaring.Error where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data DesugaringError
|
||||
import MiniJuvix.Utils.Prelude
|
||||
import qualified Text.Show
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data DesugaringError = DesugaringError
|
||||
deriving stock (Show)
|
||||
|
||||
@ -1,30 +1,35 @@
|
||||
module MiniJuvix.Error
|
||||
( ErrorType (..),
|
||||
ErrorLocation (..),
|
||||
ErrorReport (..),
|
||||
printErrors,
|
||||
)
|
||||
where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import qualified Data.List as List
|
||||
import qualified Data.Set as Set
|
||||
import MiniJuvix.Desugaring.Error (DesugaringError)
|
||||
import MiniJuvix.Parsing.Error
|
||||
import MiniJuvix.Pretty
|
||||
import MiniJuvix.Typing.Error (TypingError (..))
|
||||
import MiniJuvix.Typing.Error
|
||||
import MiniJuvix.Utils.Prelude
|
||||
import qualified Text.Show
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data ErrorType
|
||||
= PError ParsingError
|
||||
| DError DesugaringError
|
||||
| TError TypingError
|
||||
| CError CheckingError
|
||||
| UnknownError
|
||||
|
||||
instance Show ErrorType where
|
||||
show e = case e of
|
||||
PError pe -> show pe
|
||||
DError de -> show de
|
||||
TError te -> show pe
|
||||
CError te -> show te
|
||||
UnknownError -> show "UnknownError"
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
@ -49,15 +54,18 @@ type ErrorDescription = Text
|
||||
|
||||
type ErrorScope = Maybe Scope
|
||||
|
||||
data Error = Error
|
||||
{ _errorType :: ErrorType,
|
||||
_errorLoc :: ErrorLocation,
|
||||
_errorText :: ErrorDescription,
|
||||
_errorParentScopes :: [ErrorScope]
|
||||
}
|
||||
deriving stock (Eq, Show)
|
||||
data ErrorReport
|
||||
= ErrorReport
|
||||
{ _errorType :: ErrorType,
|
||||
_errorLoc :: ErrorLocation,
|
||||
_errorText :: ErrorDescription,
|
||||
_errorParentScopes :: [ErrorScope]
|
||||
}
|
||||
|
||||
instance Show ErrorReport where
|
||||
show _ = undefined
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
printErrors :: Set Error -> IO ()
|
||||
printErrors = printList . L.sort . S.toList
|
||||
printErrors :: Set ErrorReport -> IO ()
|
||||
printErrors = printList . Set.toList
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
|
||||
module MiniJuvix.Monad where
|
||||
@ -7,27 +7,25 @@ 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 :: ExceptT e (ReaderT r (StateT s m)) a}
|
||||
deriving anyclass (Functor, Applicative, Monad)
|
||||
-- newtype MiniJuvixT e r s m a
|
||||
-- = 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
|
||||
-- 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
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
-- 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
|
||||
@ -51,4 +49,4 @@ runMiniJuvix m = runMiniJuvixT m [] S.empty
|
||||
|
||||
-- -- | Retrieves the environment within a MiniJuvixT.
|
||||
-- ask :: Monad m => MiniJuvixT e r s m r
|
||||
-- ask = MiniJuvixT (lift R.ask)
|
||||
-- ask = MiniJuvixT (lift R.ask)
|
||||
|
||||
@ -1,9 +1,8 @@
|
||||
-- {-# LANGUAGE DeriveAnyClass #-}
|
||||
-- {-# LANGUAGE TypeFamilies #-}
|
||||
-- {-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
-- | Adapted from heliaxdev/Juvix/library/StandardLibrary/src/Juvix/
|
||||
module MiniJuvix.Parsing.ADT where
|
||||
module MiniJuvix.Parsing.ADT
|
||||
(
|
||||
)
|
||||
where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
||||
@ -1,15 +1,24 @@
|
||||
-- | Adapted from https://github.com/heliaxdev/juvix/
|
||||
module MiniJuvix.Parsing.Error
|
||||
( Error (..),
|
||||
ParsingError (..),
|
||||
)
|
||||
where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import safe MiniJuvix.Utils.Prelude (FilePath)
|
||||
--------------------------------------------------------------------------------
|
||||
import safe MiniJuvix.Utils.Prelude
|
||||
import qualified Text.Show
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data ParsingError
|
||||
|
||||
instance Show ParsingError where
|
||||
show = undefined
|
||||
|
||||
data Error = NoHeaderErr FilePath | ParseError ParsingError
|
||||
|
||||
instance Show Error where
|
||||
show = undefined
|
||||
|
||||
@ -1,14 +1,17 @@
|
||||
{-# OPTIONS_GHC -Wno-partial-fields #-}
|
||||
|
||||
-- | Adapted from https://github.com/heliaxdev/juvix/
|
||||
module MiniJuvix.Parsing.Location
|
||||
(noLoc,location,mkLocated)
|
||||
where
|
||||
module MiniJuvix.Parsing.Location
|
||||
( noLoc,
|
||||
location,
|
||||
mkLocated,
|
||||
)
|
||||
where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import MiniJuvix.Utils.Parser (Parser)
|
||||
import MiniJuvix.Utils.Prelude
|
||||
|
||||
import qualified Text.Megaparsec as P
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
@ -19,7 +22,7 @@ data Loc
|
||||
deriving stock (Eq, Show, Ord)
|
||||
|
||||
data Located a = Located {located :: Loc, locVal :: a}
|
||||
deriving stock Show
|
||||
deriving stock (Show)
|
||||
|
||||
instance Functor Located where
|
||||
fmap f (Located l v) = Located l (f v)
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@ -1,10 +1,10 @@
|
||||
module MiniJuvix.Pipeline
|
||||
( -- * Compiler configuration-related data structures
|
||||
CompilerMode (..),
|
||||
Config (..),
|
||||
WriteToFsBehavior (..),
|
||||
Pass (..),
|
||||
Backend (..),
|
||||
Mode (..),
|
||||
)
|
||||
where
|
||||
|
||||
@ -15,7 +15,7 @@ import MiniJuvix.Utils.Prelude (Eq, FilePath, Maybe, Ord, Show, Text)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data CompilerMode
|
||||
data Mode
|
||||
= ReplMode
|
||||
| CheckMode Config FilePath
|
||||
| CompileMode Config FilePath
|
||||
@ -32,25 +32,23 @@ data Config
|
||||
data Pass
|
||||
= Parsing
|
||||
| Desugaring
|
||||
| Typechecking
|
||||
| Checking
|
||||
| Compiling
|
||||
deriving stock Show
|
||||
deriving stock (Show)
|
||||
|
||||
data Backend = LLVM
|
||||
deriving (Eq, Ord, Show)
|
||||
deriving stock (Eq, Ord, Show)
|
||||
|
||||
data WriteToFsBehavior = OverwriteTargetFiles | WriteIfDoesNotExist
|
||||
|
||||
-- runAndLogErrs :: MiniJuvix a -> IO ()
|
||||
-- runAndLogErrs m = runMiniJuvix m >>= \(_, errs) -> logErrs errs
|
||||
-- run' :: MiniJuvix a -> IO ()
|
||||
-- run' m = runMiniJuvix m >>= \(_, errs) -> logErrors errs
|
||||
|
||||
-- runTestWith :: FilePath -> Config -> IO ()
|
||||
-- runTestWith filePath config = case _configPass config of
|
||||
-- Parsing -> undefined
|
||||
-- Desugaring -> undefined
|
||||
-- Typechecking -> runAndLogErrs $ depAnalPass filePath >>= parsePass >>= checkPass
|
||||
-- Checking -> run' $ filePath >>= parsingPass >>= checkingPass
|
||||
-- Compiling -> undefined
|
||||
|
||||
|
||||
runMiniJuvix ::
|
||||
runMiniJuvix = ?
|
||||
-- runMiniJuvix :: MiniJuvix a -> IO ()
|
||||
-- runMiniJuvix = undefined
|
||||
|
||||
@ -17,6 +17,7 @@ import MiniJuvix.Utils.Pretty
|
||||
ascii,
|
||||
color,
|
||||
hardlines,
|
||||
printList,
|
||||
render,
|
||||
unicode,
|
||||
)
|
||||
@ -87,8 +88,5 @@ instance Pretty Neutral where
|
||||
instance Pretty Binding where
|
||||
pretty _ = undefined
|
||||
|
||||
instance Pretty TypingEnv where
|
||||
pretty _ = undefined
|
||||
|
||||
instance Pretty TypingContext where
|
||||
pretty _ = undefined
|
||||
|
||||
@ -1,28 +1,28 @@
|
||||
{-# OPTIONS_GHC -fno-warn-missing-export-lists #-}
|
||||
{-# OPTIONS_GHC -fno-warn-unused-matches #-}
|
||||
{-# OPTIONS_GHC -fno-warn-unused-imports #-}
|
||||
{-# OPTIONS_GHC -fno-warn-unused-matches #-}
|
||||
|
||||
module MiniJuvix.Syntax.Core where
|
||||
|
||||
import Numeric.Natural (Natural)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import MiniJuvix.Utils.Prelude
|
||||
import Numeric.Natural (Natural)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Quantity (a.k.a. Usage)
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data Quantity = Zero
|
||||
| One
|
||||
| Many
|
||||
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
|
||||
@ -34,36 +34,38 @@ 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
|
||||
@ -74,21 +76,23 @@ 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
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -96,25 +100,40 @@ instance Eq Variable where
|
||||
-- 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 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
|
||||
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)
|
||||
@ -126,16 +145,16 @@ data InferableTerm = Var Variable
|
||||
|
||||
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
|
||||
@ -145,23 +164,29 @@ 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
|
||||
@ -171,5 +196,4 @@ termEq (Inferable x) (Inferable y) = x == y
|
||||
termEq _ _ = False
|
||||
|
||||
instance Eq Term where
|
||||
(==) = termEq
|
||||
|
||||
(==) = termEq
|
||||
|
||||
@ -1,5 +1,4 @@
|
||||
{-# 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
|
||||
|
||||
@ -10,68 +9,98 @@ import MiniJuvix.Utils.Prelude
|
||||
-- Values and neutral terms
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
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 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)
|
||||
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)
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
module MiniJuvix.Typing.Erasure () where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -8,28 +8,33 @@ where
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import MiniJuvix.Utils.Prelude
|
||||
import qualified Text.Show
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data CommonError
|
||||
= MissingVariable
|
||||
| QuantityError
|
||||
| UnknownError String
|
||||
deriving stock (Show)
|
||||
|
||||
data CheckingError
|
||||
= ExpectUniverseType
|
||||
| ExpectPiType
|
||||
| ExpectTensorType
|
||||
| ExpectSumType
|
||||
deriving stock (Show)
|
||||
|
||||
-- ! TODO add the other possible cases..
|
||||
|
||||
data InferingError
|
||||
data InferingError = InferingError
|
||||
deriving stock (Show)
|
||||
|
||||
data ErasingError
|
||||
data ErasingError = ErasingError
|
||||
deriving stock (Show)
|
||||
|
||||
data Error
|
||||
= CheckError CheckingError
|
||||
| InferError InferingError
|
||||
| ErasureError ErasingError
|
||||
| CommonError
|
||||
deriving stock (Show)
|
||||
|
||||
@ -24,11 +24,10 @@ where
|
||||
|
||||
import qualified Data.Char as Char
|
||||
import Relude hiding
|
||||
( one,
|
||||
( Type,
|
||||
one,
|
||||
)
|
||||
|
||||
import safe Relude.Container
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Logical connectives
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -8,11 +8,13 @@ module MiniJuvix.Utils.Pretty
|
||||
hardlines,
|
||||
format,
|
||||
annotateSpecialSymbol,
|
||||
printList,
|
||||
)
|
||||
where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import qualified Data.List as List
|
||||
import MiniJuvix.Utils.Prelude
|
||||
import Prettyprinter hiding
|
||||
( Doc,
|
||||
@ -113,3 +115,6 @@ annotateSpecialSymbol b s = annotate (Term.color (color s)) (format b s)
|
||||
|
||||
class Pretty a where
|
||||
pretty :: Bool -> a -> Doc
|
||||
|
||||
printList :: [a] -> IO ()
|
||||
printList = undefined
|
||||
|
||||
Loading…
Reference in New Issue
Block a user