packages feed

morte 1.6.20 → 1.7.2

raw patch · 7 files changed

Files

bench/Main.hs view
@@ -2,8 +2,9 @@  import Control.Exception (throwIO) import Criterion.Main (Benchmark, defaultMain, env, bgroup, bench, nf)+import Data.Void (Void) import Filesystem.Path.CurrentOS (FilePath)-import Morte.Core (Expr, X)+import Morte.Core (Expr) import Paths_morte (getDataFileName) import Prelude hiding (FilePath) @@ -13,7 +14,7 @@ import qualified Morte.Import              as Morte import qualified Morte.Parser              as Morte -readMorteFile :: FilePath -> IO (Expr X)+readMorteFile :: FilePath -> IO (Expr Void) readMorteFile filename = do     str <- getDataFileName (Filesystem.encodeString filename)     text <- Text.readFile str@@ -37,7 +38,7 @@         x2 <- readMorteFile "bench/src/concat.mt"         return (x0, x1, x2) -benchExpr :: FilePath -> Expr X -> Benchmark+benchExpr :: FilePath -> Expr Void -> Benchmark benchExpr path expr = bgroup (Filesystem.encodeString path)     [ bench "normalize" (nf Morte.normalize expr)     , bench "equality"  (nf (expr ==)       expr)
morte.cabal view
@@ -1,5 +1,5 @@ Name: morte-Version: 1.6.20+Version: 1.7.2 Cabal-Version: >=1.8.0.2 Build-Type: Simple License: BSD3@@ -36,10 +36,10 @@         base                 >= 4        && < 5   ,         array                >= 0.4.0.0  && < 0.6 ,         binary               >= 0.7.0.0  && < 0.9 ,-        containers           >= 0.5.0.0  && < 0.6 ,+        containers           >= 0.5.0.0  && < 0.7 ,         deepseq              >= 1.3.0    && < 1.5 ,-        Earley               >= 0.10.1.0 && < 0.13,-        http-client          >= 0.5.0    && < 0.6 ,+        Earley               >= 0.10.1.0 && < 0.14,+        http-client          >= 0.5.0    && < 0.7 ,         http-client-tls      >= 0.2.0    && < 0.4 ,         microlens            >= 0.2.0.0  && < 0.5 ,         microlens-mtl        >= 0.1.3.1  && < 0.2 ,@@ -63,7 +63,7 @@     Main-Is: Main.hs     Build-Depends:         base                 >= 4     && < 5    ,-        code-page            >= 0.1.1 && < 0.2  ,+        code-page            >= 0.1.1 && < 0.3  ,         formatting                              ,         morte                                   ,         optparse-applicative             < 0.15 ,@@ -90,9 +90,9 @@     Build-Depends:         base             >= 4        && < 5   ,         mtl              >= 2.2      && < 2.3 ,-        QuickCheck       >= 2.8.1    && < 2.12,+        QuickCheck       >= 2.8.1    && < 2.14,         system-filepath  >= 0.3.1    && < 0.5 ,-        tasty            >= 0.11     && < 1.2 ,+        tasty            >= 0.11     && < 1.3 ,         tasty-hunit      >= 0.9      && < 0.11,         tasty-quickcheck >= 0.8.4    && < 0.11,         transformers     >= 0.2.0.0  && < 0.6 ,
src/Morte/Core.hs view
@@ -51,7 +51,6 @@     Var(..),     Const(..),     Path(..),-    X(..),     Expr(..),     Context, @@ -78,7 +77,6 @@ #endif import Control.DeepSeq (NFData(..)) import Control.Exception (Exception)-import Control.Monad (mzero) import Data.Binary (Binary(..), Get, Put) import Data.Foldable import Data.Monoid ((<>))@@ -87,6 +85,7 @@ import Data.Text.Lazy.Builder (Builder) import Data.Traversable import Data.Typeable (Typeable)+import Data.Void (Void, absurd) import Data.Word (Word8) import Filesystem.Path.CurrentOS (FilePath) import Formatting.Buildable (Buildable(..))@@ -225,27 +224,6 @@         txt = Text.fromStrict (either id id (Filesystem.toText file))     build (URL  str ) = build str <> " " -{-| Like `Data.Void.Void`, except with an `NFData` instance in order to avoid-    orphan instances--}-newtype X = X { absurd :: forall a . a }--instance Eq X where-    _ == _ = True--instance Show X where-    show = absurd--instance NFData X where-    rnf x = seq x ()--instance Buildable X where-    build = absurd--instance Binary X where-    get = mzero-    put = absurd- -- | Syntax tree for expressions data Expr a     -- | > Const c        ~  c@@ -441,10 +419,10 @@ -- | The specific type error data TypeMessage     = UnboundVariable-    | InvalidInputType (Expr X)-    | InvalidOutputType (Expr X)+    | InvalidInputType (Expr Void)+    | InvalidOutputType (Expr Void)     | NotAFunction-    | TypeMismatch (Expr X) (Expr X)+    | TypeMismatch (Expr Void) (Expr Void)     | Untyped Const     deriving (Show) @@ -481,8 +459,8 @@  -- | A structured type error that includes context data TypeError = TypeError-    { context     :: Context (Expr X)-    , current     :: Expr X+    { context     :: Context (Expr Void)+    , current     :: Expr Void     , typeMessage :: TypeMessage     } deriving (Typeable) @@ -564,7 +542,7 @@     is not necessary for just type-checking.  If you actually care about the     returned type then you may want to `normalize` it afterwards. -}-typeWith :: Context (Expr X) -> Expr X -> Either TypeError (Expr X)+typeWith :: Context (Expr Void) -> Expr Void -> Either TypeError (Expr Void) typeWith ctx e = case e of     Const c     -> fmap Const (axiom c)     Var (V x n) -> case Context.lookup x n ctx of@@ -609,7 +587,7 @@     expression must be closed (i.e. no free variables), otherwise type-checking     will fail. -}-typeOf :: Expr X -> Either TypeError (Expr X)+typeOf :: Expr Void -> Either TypeError (Expr Void) typeOf = typeWith Context.empty  -- | Reduce an expression to weak-head normal form
src/Morte/Import.hs view
@@ -90,12 +90,13 @@ import Data.Traversable (traverse) #endif import Data.Typeable (Typeable)+import Data.Void (Void) import Filesystem.Path ((</>), FilePath) import Filesystem as Filesystem import Formatting.Buildable (build) import Lens.Micro (Lens') import Lens.Micro.Mtl (zoom)-import Morte.Core (Expr, Path(..), X(..))+import Morte.Core (Expr, Path(..)) import Network.HTTP.Client (Manager) import Prelude hiding (FilePath) @@ -181,7 +182,7 @@  data Status = Status     { _stack   :: [Path]-    , _cache   :: Map Path (Expr X)+    , _cache   :: Map Path (Expr Void)     , _manager :: Maybe Manager     } @@ -191,7 +192,7 @@ stack :: Lens' Status [Path] stack k s = fmap (\x -> s { _stack = x }) (k (_stack s)) -cache :: Lens' Status (Map Path (Expr X))+cache :: Lens' Status (Map Path (Expr Void)) cache k s = fmap (\x -> s { _cache = x }) (k (_cache s))  manager :: Lens' Status (Maybe Manager)@@ -362,7 +363,7 @@         Right expr -> return expr  -- | Load a `Path` as a \"static\" expression (with all imports resolved)-loadStatic :: Path -> StateT Status IO (Expr X)+loadStatic :: Path -> StateT Status IO (Expr Void) loadStatic path = do     paths <- zoom stack State.get @@ -428,7 +429,7 @@     -- ^ Starting path     -> Expr Path     -- ^ Expression to resolve-    -> IO (Expr X)+    -> IO (Expr Void) load here expr =     State.evalStateT (fmap join (traverse loadStatic expr)) status   where
src/Morte/Tutorial.hs view
@@ -451,7 +451,7 @@ > r      : *  -- The result type of all three case branches > t      : T String Int Bool >-> matchT String Int Bool r t+> matchT String Int Bool t r >     (                                ...)  -- Branch if you match `A` >     (\(s : String) ->                ...)  -- Branch if you match `B` >     (\(i : Int   ) -> \(b : Bool) -> ...)  -- Branch if you match `C`@@ -1057,7 +1057,7 @@     Morte using the rules for existential quantification given in the previous     section: -> (forall (x : *) -> (forall (s : *) -> s -> (s -> StreamF a s) -> x) -> x+> forall (x : *) -> (forall (s : *) -> s -> (s -> StreamF a s) -> x) -> x      See the next section for some example @Stream@ code. -}@@ -1604,7 +1604,7 @@ > --     ninetynine = nine * ten + nine > -- > --     main_ :: IO U-> --     main_ = getLine >>= putStrLn+> --     main_ = replicateM_ ninetynine (getLine >>= putStrLn) >  > -- "Free" variables > (   \(String : *   )@@ -2045,7 +2045,7 @@ > > λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero)) -    Take care that you must have whitespace after the hashtag import.  If you+    Take care that you must have whitespace after the file name import.  If you     were to write:  > $ morte@@ -2065,7 +2065,7 @@     @Zero))@.  This causes a parsing failure because @morte@ can no longer find     the program's closing parentheses. -    When you use imports, each hashtag is replaced with the expression from that+    When you use imports, each file name is replaced with the expression from that     file, so it would be as if you wrote the following really long expression:  > $ morte@@ -2124,9 +2124,8 @@     design feature of Boehm-Berarducci encoding known as \"representability\".      The <https://github.com/Gabriel439/Haskell-Morte-Library Morte repository>-    provides a simple Prelude of utilities that you can try out.  For example,-    if you @cd@ to the @local@ directory of the repository, you can run-    expressions like:+    provides a simple Prelude of utilities that you can try out.  If you @cd@+    to the @Prelude@ directory of the repository, you can run expressions like:  > $ morte > ./id ./Bool ./Bool/True@@ -2224,12 +2223,6 @@ >  > λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True  -    In fact, the @remote@ directory in the @morte@ repository does exactly this,-    mirroring the structure of the @local@ directory except all the files are-    just references to network-hosted expressions.  If you @cd@ to the @remote@-    directory all of the above examples will still work, except this time when-    you compile the examples they will download the expressions from the server.-     Remote expressions can reference other remote expressions, and the compiler     will track down and resolve all of these references, taking care to avoid     cycles.  This means that you can host code on the network that references
test/ClosedWellTyped.hs view
@@ -7,6 +7,7 @@ import Control.Applicative hiding (Const) import Control.Monad (guard) import Data.Text.Lazy (Text)+import Data.Void (Void) import Control.Monad.State.Lazy (MonadState, StateT) import Control.Monad.Trans.Class (lift) import Morte.Core@@ -17,11 +18,11 @@ import qualified Data.Text.Lazy           as Text import qualified Test.QuickCheck          as QuickCheck -newtype ClosedWellTyped = ClosedWellTyped { unClosedWellTyped :: Expr X }+newtype ClosedWellTyped = ClosedWellTyped { unClosedWellTyped :: Expr Void }     deriving Show  data Env = Env-    { bindings :: [(Var, Expr X)]+    { bindings :: [(Var, Expr Void)]     , uniques  :: [Text]     } @@ -47,10 +48,10 @@     , uniques  = map (Text.pack . show) [1..n]     } -extend :: Var -> Expr X -> M ()+extend :: Var -> Expr Void -> M () extend x t = State.modify (\env -> env { bindings = (x, t) : bindings env }) -select :: [(Int, M (Expr X, Expr X), Env -> Bool)] -> M (Expr X, Expr X)+select :: [(Int, M (Expr Void, Expr Void), Env -> Bool)] -> M (Expr Void, Expr Void) select wgps = do     env <- State.get     m   <- liftGen (QuickCheck.frequency (do@@ -70,11 +71,11 @@ moreThan :: Int -> [a] -> Bool moreThan n = not . null . drop n -piFilter :: Expr X -> Expr X -> Bool+piFilter :: Expr Void -> Expr Void -> Bool piFilter t (Pi _ _A _) = _A == t piFilter _  _          = False -closed :: M (Expr X, Expr X)+closed :: M (Expr Void, Expr Void) closed =     select         [ (20, typeOrKind                       , \_ -> True          )@@ -82,7 +83,7 @@         , (30, app                              , moreThan 1 . uniques)         ] -termOrType :: M (Expr X, Expr X)+termOrType :: M (Expr Void, Expr Void) termOrType =     select         [ ( 5, type_                            , moreThan 0 . uniques )@@ -93,7 +94,7 @@                 ||  (moreThan 0 (bindings e) && moreThan 0 (uniques e)) )         ] -typeOrKind :: M (Expr X, Expr X)+typeOrKind :: M (Expr Void, Expr Void) typeOrKind =     select         [ (15, return (Const Star,Const Box)   , \_ -> True                      )@@ -101,7 +102,7 @@         , (15, pi (scope typeOrKind) typeOrKind, moreThan 0            . uniques )         ] -varWith :: (Expr X -> Bool) -> M (Expr X, Expr X)+varWith :: (Expr Void -> Bool) -> M (Expr Void, Expr Void) varWith f = do     bEnv <- State.gets bindings     liftGen (QuickCheck.elements (do@@ -109,10 +110,10 @@         guard (f y)         return (Var x, y) )) -var :: M (Expr X, Expr X)+var :: M (Expr Void, Expr Void) var = varWith (\_ -> True) -type_ :: M (Expr X, Expr X)+type_ :: M (Expr Void, Expr Void) type_ =     select         [ (20, varWith (== Const Star)     , matching (Const Star) . bindings)@@ -126,9 +127,9 @@     State.put (env { uniques = xs })     return x -lam :: M (Expr X, Expr X)-    -> M (Expr X, Expr X)-    -> M (Expr X, Expr X)+lam :: M (Expr Void, Expr Void)+    -> M (Expr Void, Expr Void)+    -> M (Expr Void, Expr Void) lam _AGen bGen = do     x <- fresh     (_A, _) <- _AGen@@ -136,9 +137,9 @@     (b, bType) <- bGen     return (Lam x _A b, Pi x _A bType) -pi  :: M (Expr X, Expr X)-    -> M (Expr X, Expr X)-    -> M (Expr X, Expr X)+pi  :: M (Expr Void, Expr Void)+    -> M (Expr Void, Expr Void)+    -> M (Expr Void, Expr Void) pi _AGen _BGen = do     x <- fresh     (_A, _) <- _AGen@@ -146,11 +147,11 @@     (_B, _BType) <- _BGen     return (Pi x _A _B, _BType) -app :: M (Expr X, Expr X)+app :: M (Expr Void, Expr Void) app = do     (_N, _A       ) <- scope termOrType     let genA = return (_A, Const Star)-    (f , Pi x _ _B) <- do+    ~(f , Pi x _ _B) <- do         scope             (select                 [ (40, lam genA termOrType  , moreThan 0              . uniques )
test/Main.hs view
@@ -7,8 +7,9 @@ import Control.Exception (throwIO) import ClosedWellTyped (ClosedWellTyped(..)) import Data.Text.Lazy (Text)+import Data.Void (Void) import Filesystem.Path (FilePath)-import Morte.Core (Expr, X)+import Morte.Core (Expr) import Paths_morte (getDataFileName) import Prelude hiding (FilePath) import Test.Tasty (TestTree)@@ -54,7 +55,7 @@             ]         ] -typeChecks :: Expr X -> Bool+typeChecks :: Expr Void -> Bool typeChecks expr = case Morte.typeOf expr of     Right _ -> True     Left  _ -> False