packages feed

lambda-cube 0.2.0.0 → 0.3.0.0

raw patch · 56 files changed

+1775/−502 lines, 56 filesdep +tastydep +tasty-hspecdep −QuickCheckdep ~text

Dependencies added: tasty, tasty-hspec

Dependencies removed: QuickCheck

Dependency ranges changed: text

Files

CHANGELOG.md view
@@ -1,3 +1,26 @@+# Unreleased++# 0.3.0.0++## Main updates++- Type/Kind level quasiquoter are added.+- Evaluators are added to the top-level modules.+- STLC and System F omega are tested with various examples.+- Identifiers now accepts `_`.++## Bug fixed++- Substitutions are fixed with valid shifting.+- STLC normalizer is fixed with valid beta-reduction.+- Fix type inference for System F and System F omega.++## Breaking changes++- Names of quasiquoters are changed.+- The order of arguments for substitution are changed.+- Non-Ast modules now have explicit export lists.+ # 0.2.0.0  ## Main updates@@ -10,12 +33,12 @@  ## Breaking changes -- Move lifters and substitutions into dedicated modules.-- Rename pretty printers.-- Rename elaborators.-- Rename quasiquoter.-- Remove elaborated quasiquoter.-- Change the type of elaborator and type checker.+- Lifters and substitutions into dedicated modules are moved.+- Pretty printers are renamed.+- Elaborators are renamed.+- Quasiquoter are renamed.+- Elaborated quasiquoters are remove.+- The types of elaborators and type checkers are changed.  # 0.1.0.0
lambda-cube.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           lambda-cube-version:        0.2.0.0+version:        0.3.0.0 synopsis:       Haskell implementation of (some of) lambda cube calculi description:    Haskell implementation of the following 4 lambda calculi:                 .@@ -34,6 +34,7 @@   exposed-modules:       LambdaCube.Common.Parser       LambdaCube.Common.PrettyPrinter+      LambdaCube.Common.TH       LambdaCube.STLC       LambdaCube.STLC.Ast       LambdaCube.STLC.Elaborator@@ -137,8 +138,13 @@  test-suite lambda-cube-test   type: exitcode-stdio-1.0-  main-is: Spec.hs+  main-is: Test.hs   other-modules:+      LambdaCube.STLCTest+      LambdaCube.STLCTestExample+      LambdaCube.SystemFwTest+      LambdaCube.SystemFwTestExample+      LambdaCube.TestUtil       Paths_lambda_cube   hs-source-dirs:       test@@ -188,8 +194,10 @@       TypeSynonymInstances   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-deriving-strategies -Wmissing-home-modules -Wmonomorphism-restriction -Wpartial-fields -Wredundant-constraints -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N   build-depends:-      QuickCheck-    , base+      base     , hspec     , lambda-cube+    , tasty+    , tasty-hspec+    , text   default-language: Haskell2010
src/LambdaCube/Common/Parser.hs view
@@ -1,6 +1,27 @@ {-# LANGUAGE OverloadedStrings #-}-module LambdaCube.Common.Parser where+module LambdaCube.Common.Parser+  ( Parser +  , topParser+  , parenthesized+  , identifier++  , rightArrow+  , atsignBackslash++  , backslash+  , atsign+  , sharp+  , colon+  , dot+  , openParenthesis+  , closeParenthesis+  , exclamationMark+  , comma+  , asterisk+  , dollarsign+  ) where+ import           Prelude              hiding (lex)  import           Data.Text            (Text)@@ -17,6 +38,9 @@ parenthesized :: Parser a -> Parser a parenthesized = between openParenthesis closeParenthesis +identifier :: Parser Text+identifier = lex $ (Text.pack .) . (:) <$> letterChar <*> many (alphaNumChar <|> char '_')+ rightArrow, atsignBackslash :: Parser Text rightArrow = lex $ string "->" atsignBackslash = lex $ string "@\\"@@ -33,9 +57,6 @@ comma            = lex $ char ',' asterisk         = lex $ char '*' dollarsign       = lex $ char '$'--identifier :: Parser Text-identifier = lex $ (Text.pack .) . (:) <$> letterChar <*> many alphaNumChar  lex :: Parser a -> Parser a lex = (<* space)
src/LambdaCube/Common/PrettyPrinter.hs view
@@ -1,18 +1,24 @@ {-# LANGUAGE OverloadedStrings #-}-module LambdaCube.Common.PrettyPrinter where+module LambdaCube.Common.PrettyPrinter+  ( wrapIfSpaced+  , wrapIf+  , wrap +  , spaced+  ) where+ import           Data.Text (Text) import qualified Data.Text as Text  wrapIfSpaced :: Bool -> [Text] -> Text wrapIfSpaced b = wrapIf b . spaced -wrap :: Text -> Text-wrap t = "(" <> t <> ")"- wrapIf :: Bool -> Text -> Text wrapIf True  = wrap wrapIf False = id++wrap :: Text -> Text+wrap t = "(" <> t <> ")"  spaced :: [Text] -> Text spaced = Text.intercalate " "
+ src/LambdaCube/Common/TH.hs view
@@ -0,0 +1,25 @@+module LambdaCube.Common.TH+  ( qExpBase++  , converterBase+  ) where++import           Data.Data                  (Data)+import           Data.Generics              (extQ)+import           Data.Text                  (Text)+import qualified Data.Text                  as Text+import           LambdaCube.Common.Parser+import           Language.Haskell.TH.Lib    (ExpQ)+import           Language.Haskell.TH.Syntax (dataToExpQ, lift, loc_start,+                                             location)+import qualified Text.Megaparsec            as P++qExpBase :: Data a => Parser a -> (forall b. Data b => b -> Maybe ExpQ) -> String -> ExpQ+qExpBase p conv str = do+  l <- location+  case P.parse p ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of+    Right e  -> dataToExpQ conv e+    Left err -> fail $ P.errorBundlePretty err++converterBase :: Data b => b -> Maybe ExpQ+converterBase = const Nothing `extQ` (Just . lift :: Text -> Maybe ExpQ)
src/LambdaCube/STLC.hs view
@@ -1,6 +1,7 @@ module LambdaCube.STLC   ( module LambdaCube.STLC.Ast   , module LambdaCube.STLC.Elaborator+  , module LambdaCube.STLC.Evaluator   , module LambdaCube.STLC.Lifter   , module LambdaCube.STLC.Normalizer   , module LambdaCube.STLC.Parser@@ -13,6 +14,7 @@ import LambdaCube.STLC.Ast  import LambdaCube.STLC.Elaborator+import LambdaCube.STLC.Evaluator import LambdaCube.STLC.Lifter import LambdaCube.STLC.Normalizer import LambdaCube.STLC.Parser
src/LambdaCube/STLC/Ast.hs view
@@ -4,13 +4,6 @@ import           Data.Text                  (Text) import           Language.Haskell.TH.Syntax (Lift) -data ExtLCType-  = ExtLCBase-  | ExtLCArr ExtLCType ExtLCType-  | ExtLCMTVar String-  deriving stock (Eq, Show, Data, Lift)-infixr 5 `ExtLCArr`- data ExtLCTerm   = ExtLCVar Text   | ExtLCLam Text ExtLCType ExtLCTerm@@ -19,11 +12,12 @@   deriving stock (Eq, Show, Data, Lift) infixl 6 `ExtLCApp` -data LCType-  = LCBase-  | LCArr LCType LCType+data ExtLCType+  = ExtLCBase+  | ExtLCArr ExtLCType ExtLCType+  | ExtLCMTVar String   deriving stock (Eq, Show, Data, Lift)-infixr 5 `LCArr`+infixr 5 `ExtLCArr`  data LCTerm   = LCVar Int@@ -31,6 +25,12 @@   | LCApp LCTerm LCTerm   deriving stock (Eq, Show, Data, Lift) infixl 6 `LCApp`++data LCType+  = LCBase+  | LCArr LCType LCType+  deriving stock (Eq, Show, Data, Lift)+infixr 5 `LCArr`  data LCValue   = LCValLam LCType LCTerm
src/LambdaCube/STLC/Elaborator.hs view
@@ -1,24 +1,27 @@-module LambdaCube.STLC.Elaborator where+module LambdaCube.STLC.Elaborator+  ( elaborate+  , elaborateType+  ) where  import           Data.List           (elemIndex) import qualified Data.Text           as Text import           LambdaCube.STLC.Ast -elaborateType :: ExtLCType -> LCType-elaborateType = go-  where-    go ExtLCBase = LCBase-    go (ExtLCArr a b) = go a `LCArr` go b-    go (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"- elaborate :: ExtLCTerm -> LCTerm elaborate = go []   where-    go l (ExtLCVar v)-      | Just idx <- v `elemIndex` l+    go l (ExtLCVar x)+      | Just idx <- x `elemIndex` l       = LCVar idx       | otherwise-      = error $ "Variable " <> Text.unpack v <> " is not in scope"-    go l (ExtLCLam v t b) = LCLam (elaborateType t) $ go (v : l) b+      = error $ "Variable " <> Text.unpack x <> " is not in scope"+    go l (ExtLCLam x t b) = LCLam (elaborateType t) $ go (x : l) b     go l (ExtLCApp f a) = go l f `LCApp` go l a     go _ (ExtLCMVar _) = error "invalid TemplateHaskell code splicer"++elaborateType :: ExtLCType -> LCType+elaborateType = go+  where+    go ExtLCBase = LCBase+    go (ExtLCArr a b) = go a `LCArr` go b+    go (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
src/LambdaCube/STLC/Evaluator.hs view
@@ -1,4 +1,6 @@-module LambdaCube.STLC.Evaluator where+module LambdaCube.STLC.Evaluator+  ( evaluate+  ) where  import           LambdaCube.STLC.Ast import           LambdaCube.STLC.Substitution@@ -11,4 +13,4 @@     go (LCApp f a)       | LCValLam _ b <- go f       , v <- go a-      = go $ substituteValue 0 v b+      = go $ substituteValue v 0 b
src/LambdaCube/STLC/Lifter.hs view
@@ -1,4 +1,7 @@-module LambdaCube.STLC.Lifter where+module LambdaCube.STLC.Lifter+  ( liftLCValue+  , liftLCNormal+  ) where  import           LambdaCube.STLC.Ast @@ -10,5 +13,5 @@ liftLCNormal (LCNormNeut nt) = liftLCNeutral nt  liftLCNeutral :: LCNeutralTerm -> LCTerm-liftLCNeutral (LCNeutVar n) = LCVar n+liftLCNeutral (LCNeutVar x) = LCVar x liftLCNeutral (LCNeutApp f a) = liftLCNeutral f `LCApp` liftLCNormal a
src/LambdaCube/STLC/Normalizer.hs view
@@ -1,4 +1,6 @@-module LambdaCube.STLC.Normalizer where+module LambdaCube.STLC.Normalizer+  ( normalize+  ) where  import           LambdaCube.STLC.Ast import           LambdaCube.STLC.Substitution@@ -6,11 +8,11 @@ normalize :: LCTerm -> LCNormalTerm normalize = go   where-    go (LCVar n) = LCNormNeut $ LCNeutVar n+    go (LCVar x) = LCNormNeut $ LCNeutVar x     go (LCLam t b) = LCNormLam t $ go b     go (LCApp f a) =       case go f of-        LCNormLam t b   -> LCNormLam t $ substituteNormalInNormal 0 a' b-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'+        LCNormLam _ b -> substituteNormalInNormal a' 0 b+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'       where         a' = go a
src/LambdaCube/STLC/Parser.hs view
@@ -1,4 +1,7 @@-module LambdaCube.STLC.Parser where+module LambdaCube.STLC.Parser+  ( pTopTerm+  , pTopType+  ) where  import           Data.Foldable            (Foldable (foldl')) import           Data.Functor             (($>))@@ -7,30 +10,33 @@ import           LambdaCube.STLC.Ast import           Text.Megaparsec -pTopLC :: Parser ExtLCTerm-pTopLC = topParser pLC+pTopTerm :: Parser ExtLCTerm+pTopTerm = topParser pTerm -pLC :: Parser ExtLCTerm-pLC = pLam<|> pApp+pTerm :: Parser ExtLCTerm+pTerm = pLam <|> pApp  pLam :: Parser ExtLCTerm pLam =   ExtLCLam   <$> (backslash *> identifier)   <*> (colon *> pType)-  <*> (dot *> pLC)+  <*> (dot *> pTerm)  pApp :: Parser ExtLCTerm pApp = foldl' ExtLCApp <$> pATerm <*> many pATerm  pATerm :: Parser ExtLCTerm-pATerm = pVar <|> pMVar <|> parenthesized pLC+pATerm = pVar <|> pMVar <|> parenthesized pTerm  pVar :: Parser ExtLCTerm pVar = ExtLCVar <$> identifier  pMVar :: Parser ExtLCTerm pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)++pTopType :: Parser ExtLCType+pTopType = topParser pType  pType :: Parser ExtLCType pType = foldr1 ExtLCArr <$> sepBy1 pAType rightArrow
src/LambdaCube/STLC/PrettyPrinter.hs view
@@ -2,30 +2,41 @@   TODO: Use real pretty printer library -} {-# LANGUAGE OverloadedStrings #-}-module LambdaCube.STLC.PrettyPrinter where+module LambdaCube.STLC.PrettyPrinter+  ( prettyUnnamedTerm+  , prettyShowUnnamedTerm+  , prettyUnnamedType+  , prettyShowUnnamedType+  ) where  import           Data.Text                       (Text) import qualified Data.Text                       as Text import           LambdaCube.Common.PrettyPrinter import           LambdaCube.STLC.Ast -prettyUnnamedType :: LCType -> Text-prettyUnnamedType = prettyUnnamedTypePrec 0- prettyUnnamedTerm :: LCTerm -> Text prettyUnnamedTerm = prettyUnnamedTermPrec 0 -prettyUnnamedTypePrec :: Int -> LCType -> Text-prettyUnnamedTypePrec = go-  where-    go _ LCBase      = "#"-    go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]+prettyShowUnnamedTerm :: LCTerm -> String+prettyShowUnnamedTerm = Text.unpack . prettyUnnamedTerm +prettyUnnamedType :: LCType -> Text+prettyUnnamedType = prettyUnnamedTypePrec 0++prettyShowUnnamedType :: LCType -> String+prettyShowUnnamedType = Text.unpack . prettyUnnamedType+ prettyUnnamedTermPrec :: Int -> LCTerm -> Text prettyUnnamedTermPrec = go   where     pTP = prettyUnnamedTypePrec -    go _ (LCVar n)   = Text.pack $ show n+    go _ (LCVar x)   = Text.pack $ show x     go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]     go p (LCApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]++prettyUnnamedTypePrec :: Int -> LCType -> Text+prettyUnnamedTypePrec = go+  where+    go _ LCBase      = "#"+    go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
src/LambdaCube/STLC/Substitution.hs view
@@ -1,28 +1,70 @@-module LambdaCube.STLC.Substitution where+{-# LANGUAGE ViewPatterns #-}+module LambdaCube.STLC.Substitution+  ( substituteValue+  , substituteNormalInNormal+  ) where  import           LambdaCube.STLC.Ast import           LambdaCube.STLC.Lifter -substituteValue :: Int -> LCValue -> LCTerm -> LCTerm-substituteValue n v = go n+substituteValue :: LCValue -> Int -> LCTerm -> LCTerm+substituteValue v = substDefValue (v, 0)++substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm+substituteNormalInNormal v = substDefNormalInNormal (v, 0)++substDefValue :: (LCValue, Int) -> Int -> LCTerm -> LCTerm+substDefValue = go   where-    go m e@(LCVar l) = if m == l then liftLCValue v else e-    go m (LCLam t b) = LCLam t $ go (m + 1) b-    go m (LCApp f a) = go m f `LCApp` go m a+    go dv     x (LCVar ((== x) -> True))  = shiftValue dv+    go _      x e@(LCVar ((< x) -> True)) = e+    go _      _ (LCVar y)                 = LCVar $ y - 1+    go (v, s) x (LCLam t b)               = LCLam t $ go (v, s + 1) (x + 1) b+    go dv     x (LCApp f a)               = go dv x f `LCApp` go dv x a -substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm-substituteNormalInNormal n nv = go n+substDefNormalInNormal :: (LCNormalTerm, Int) -> Int -> LCNormalTerm -> LCNormalTerm+substDefNormalInNormal = go   where-    go m (LCNormLam t b)   = LCNormLam t $ go (m + 1) b-    go m (LCNormNeut neut) = substituteNormalInNeutral m nv neut+    go (v, s) x (LCNormLam t b) = LCNormLam t $ go (v, s + 1) (x + 1) b+    go dv     x (LCNormNeut nt) = substDefNormalInNeutral dv x nt -substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm-substituteNormalInNeutral n nv = go n+substDefNormalInNeutral :: (LCNormalTerm, Int) -> Int -> LCNeutralTerm -> LCNormalTerm+substDefNormalInNeutral dv x = go   where-    go m e@(LCNeutVar l) = if m == l then nv else LCNormNeut e-    go m (LCNeutApp f a) =-      case go m f of-        LCNormLam _ b   -> substituteNormalInNormal 0 a' b-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'+    go (LCNeutVar ((== x) -> True)) = shiftNormal dv+    go e@(LCNeutVar ((< x) -> True)) = LCNormNeut e+    go (LCNeutVar y) = LCNormNeut . LCNeutVar $ y - 1+    go (LCNeutApp f a) =+      case go f of+        LCNormLam _ b -> substituteNormalInNormal a' 0 b+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'       where-        a' = substituteNormalInNormal m nv a+        a' = substDefNormalInNormal dv x a++shift :: (LCTerm, Int) -> LCTerm+shift = shiftMin 0++shiftMin :: Int -> (LCTerm, Int) -> LCTerm+shiftMin n' (v, s) = go n' v+  where+    go n (LCVar x)   = LCVar $ if x < n then x else x + s+    go n (LCLam t b) = LCLam t $ go (n + 1) b+    go n (LCApp f a) = go n f `LCApp` go n a++shiftValue :: (LCValue, Int) -> LCTerm+shiftValue (v, s) = shift (liftLCValue v, s)++shiftNormal :: (LCNormalTerm, Int) -> LCNormalTerm+shiftNormal = shiftNormalMin 0++shiftNormalMin :: Int -> (LCNormalTerm, Int) -> LCNormalTerm+shiftNormalMin n' (v, s) = go n' v+  where+    go n (LCNormLam t b) = LCNormLam t $ go (n + 1) b+    go n (LCNormNeut nt) = LCNormNeut $ shiftNeutralMin n (nt, s)++shiftNeutralMin :: Int -> (LCNeutralTerm, Int) -> LCNeutralTerm+shiftNeutralMin n (v, s) = go v+  where+    go (LCNeutVar x)   = LCNeutVar $ if x < n then x else x + s+    go (LCNeutApp f a) = go f `LCNeutApp` shiftNormalMin n (a, s)
src/LambdaCube/STLC/TH.hs view
@@ -1,45 +1,57 @@ module LambdaCube.STLC.TH-  ( lc+  ( qTerm+  , qType   ) where  import           Data.Data                  (Data) import           Data.Generics              (extQ)-import           Data.Text                  (Text)-import qualified Data.Text                  as Text+import           LambdaCube.Common.TH import           LambdaCube.STLC.Ast import           LambdaCube.STLC.Parser import           Language.Haskell.TH.Lib    (ExpQ, varE) import           Language.Haskell.TH.Quote  (QuasiQuoter (..))-import           Language.Haskell.TH.Syntax (Loc (loc_start), dataToExpQ, lift,-                                             location, mkName)-import qualified Text.Megaparsec            as P-import qualified Text.Megaparsec.Error      as PE+import           Language.Haskell.TH.Syntax (mkName) -lc :: QuasiQuoter-lc =+qTerm :: QuasiQuoter+qTerm =   QuasiQuoter-    { quoteExp = expLc+    { quoteExp = qExpTerm     , quotePat = undefined     , quoteType = undefined     , quoteDec = undefined     } -expLc :: String -> ExpQ-expLc str = do-  l <- location-  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of-    Right e  -> dataToExpQ converter e-    Left err -> fail $ PE.errorBundlePretty err+qExpTerm :: String -> ExpQ+qExpTerm = qExpBase pTopTerm converter   where     converter :: Data b => b -> Maybe ExpQ     converter =-      const Nothing+      converterBase       `extQ` quotedMVar       `extQ` quotedMTVar-      `extQ` (Just . lift :: Text -> Maybe ExpQ)      quotedMVar (ExtLCMVar x) = Just . varE $ mkName x     quotedMVar _             = Nothing++    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x+    quotedMTVar _              = Nothing++qType :: QuasiQuoter+qType =+  QuasiQuoter+    { quoteExp = qExpType+    , quotePat = undefined+    , quoteType = undefined+    , quoteDec = undefined+    }++qExpType :: String -> ExpQ+qExpType = qExpBase pTopType converter+  where+    converter :: Data b => b -> Maybe ExpQ+    converter =+      converterBase+      `extQ` quotedMTVar      quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x     quotedMTVar _              = Nothing
src/LambdaCube/STLC/TypeChecker.hs view
@@ -1,4 +1,6 @@-module LambdaCube.STLC.TypeChecker where+module LambdaCube.STLC.TypeChecker+  ( infer+  ) where  import           Data.List           (uncons) import           LambdaCube.STLC.Ast@@ -6,7 +8,7 @@ infer :: LCTerm -> LCType infer = go []   where-    go l (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n l+    go l (LCVar x) = maybe (error "Out-of-scope variable") fst . uncons $ drop x l     go l (LCLam t b) = t `LCArr` go (t : l) b     go l (LCApp f a)       | LCArr at rt <- go l f
src/LambdaCube/SystemF.hs view
@@ -1,6 +1,7 @@ module LambdaCube.SystemF   ( module LambdaCube.SystemF.Ast   , module LambdaCube.SystemF.Elaborator+  , module LambdaCube.SystemF.Evaluator   , module LambdaCube.SystemF.Lifter   , module LambdaCube.SystemF.Normalizer   , module LambdaCube.SystemF.Parser@@ -13,6 +14,7 @@ import LambdaCube.SystemF.Ast  import LambdaCube.SystemF.Elaborator+import LambdaCube.SystemF.Evaluator import LambdaCube.SystemF.Lifter import LambdaCube.SystemF.Normalizer import LambdaCube.SystemF.Parser
src/LambdaCube/SystemF/Ast.hs view
@@ -4,15 +4,6 @@ import           Data.Text                  (Text) import           Language.Haskell.TH.Syntax (Lift) -data ExtLCType-  = ExtLCBase-  | ExtLCTVar Text-  | ExtLCArr ExtLCType ExtLCType-  | ExtLCUniv Text ExtLCType-  | ExtLCMTVar String-  deriving stock (Eq, Show, Data, Lift)-infixr 5 `ExtLCArr`- data ExtLCTerm   = ExtLCVar Text   | ExtLCLam Text ExtLCType ExtLCTerm@@ -24,13 +15,14 @@ infixl 6 `ExtLCApp` infixl 6 `ExtLCTApp` -data LCType-  = LCBase-  | LCTVar Int-  | LCArr LCType LCType-  | LCUniv LCType+data ExtLCType+  = ExtLCBase+  | ExtLCTVar Text+  | ExtLCArr ExtLCType ExtLCType+  | ExtLCUniv Text ExtLCType+  | ExtLCMTVar String   deriving stock (Eq, Show, Data, Lift)-infixr 5 `LCArr`+infixr 5 `ExtLCArr`  data LCTerm   = LCVar Int@@ -41,6 +33,14 @@   deriving stock (Eq, Show, Data, Lift) infixl 6 `LCApp` infixl 6 `LCTApp`++data LCType+  = LCBase+  | LCTVar Int+  | LCArr LCType LCType+  | LCUniv LCType+  deriving stock (Eq, Show, Data, Lift)+infixr 5 `LCArr`  data LCValue   = LCValLam LCType LCTerm
src/LambdaCube/SystemF/Elaborator.hs view
@@ -1,4 +1,7 @@-module LambdaCube.SystemF.Elaborator where+module LambdaCube.SystemF.Elaborator+  ( elaborate+  , elaborateType+  ) where  import           Data.List              (elemIndex) import           Data.Text              (Text)@@ -15,7 +18,7 @@       = error $ "Term variable " <> Text.unpack x <> " is not in scope"     go tl vl (ExtLCLam x t b) = LCLam (elaborateType tl t) $ go tl (x : vl) b     go tl vl (ExtLCApp f a) = go tl vl f `LCApp` go tl vl a-    go tl vl (ExtLCTLam x b) = LCTLam $ go (x : tl) vl b+    go tl vl (ExtLCTLam p b) = LCTLam $ go (p : tl) vl b     go tl vl (ExtLCTApp f t) = go tl vl f `LCTApp` elaborateType tl t     go _  _  (ExtLCMVar _) = error "invalid TemplateHaskell code splicer" @@ -23,11 +26,11 @@ elaborateType = go   where     go _ ExtLCBase = LCBase-    go l (ExtLCTVar x)-      | Just n <- x `elemIndex` l+    go l (ExtLCTVar p)+      | Just n <- p `elemIndex` l       = LCTVar n       | otherwise-      = error $ "Type variable " <> Text.unpack x <> " is not in scope"+      = error $ "Type variable " <> Text.unpack p <> " is not in scope"     go l (ExtLCArr a b) = go l a `LCArr` go l b-    go l (ExtLCUniv x a) = LCUniv $ go (x : l) a+    go l (ExtLCUniv p a) = LCUniv $ go (p : l) a     go _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
src/LambdaCube/SystemF/Evaluator.hs view
@@ -1,4 +1,6 @@-module LambdaCube.SystemF.Evaluator where+module LambdaCube.SystemF.Evaluator+  ( evaluate+  ) where  import           LambdaCube.SystemF.Ast import           LambdaCube.SystemF.Substitution@@ -11,12 +13,12 @@     go (LCApp f a)       | LCValLam _ b <- go f       , v <- go a-      = go $ substituteValue 0 v b+      = go $ substituteValue v 0 b       | otherwise       = error "Did you really type check this?"     go (LCTLam b) = LCValTLam b     go (LCTApp f t)       | LCValTLam b <- go f-      = go $ substituteType 0 t b+      = go $ substituteType t 0 b       | otherwise       = error "Did you really type check this?"
src/LambdaCube/SystemF/Lifter.hs view
@@ -1,4 +1,7 @@-module LambdaCube.SystemF.Lifter where+module LambdaCube.SystemF.Lifter+  ( liftLCValue+  , liftLCNormal+  ) where  import           LambdaCube.SystemF.Ast @@ -12,6 +15,6 @@ liftLCNormal (LCNormNeut nt) = liftLCNeutral nt  liftLCNeutral :: LCNeutralTerm -> LCTerm-liftLCNeutral (LCNeutVar n)    = LCVar n+liftLCNeutral (LCNeutVar x)    = LCVar x liftLCNeutral (LCNeutApp f a)  = liftLCNeutral f `LCApp` liftLCNormal a liftLCNeutral (LCNeutTApp f t) = liftLCNeutral f `LCTApp` t
src/LambdaCube/SystemF/Normalizer.hs view
@@ -6,18 +6,18 @@ normalize :: LCTerm -> LCNormalTerm normalize = go   where-    go (LCVar n) = LCNormNeut $ LCNeutVar n+    go (LCVar x) = LCNormNeut $ LCNeutVar x     go (LCLam t b) = LCNormLam t $ go b     go (LCTLam b) = LCNormTLam $ go b     go (LCApp f a) =       case go f of-        LCNormLam _ b   -> substituteNormalInNormal 0 a' b-        LCNormTLam _    -> error "Did you really type check this?"-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'+        LCNormLam _ b -> substituteNormalInNormal a' 0 b+        LCNormTLam _  -> error "Did you really type check this?"+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'       where         a' = go a     go (LCTApp f t) =       case go f of-        LCNormLam _ _   -> error "Did you really type check this?"-        LCNormTLam b    -> substituteTypeInNormal 0 t b-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutTApp` t+        LCNormLam _ _ -> error "Did you really type check this?"+        LCNormTLam b  -> substituteTypeInNormal t 0 b+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t
src/LambdaCube/SystemF/Parser.hs view
@@ -1,4 +1,7 @@-module LambdaCube.SystemF.Parser where+module LambdaCube.SystemF.Parser+  ( pTopTerm+  , pTopType+  ) where  import           Data.Foldable            (Foldable (foldl')) import           Data.Function            ((&))@@ -9,24 +12,24 @@ import           Text.Megaparsec import qualified Data.Text as Text -pTopLC :: Parser ExtLCTerm-pTopLC = topParser pLC+pTopTerm :: Parser ExtLCTerm+pTopTerm = topParser pTerm -pLC :: Parser ExtLCTerm-pLC = pTLam <|> pLam <|> pApp+pTerm :: Parser ExtLCTerm+pTerm = pTLam <|> pLam <|> pApp  pTLam :: Parser ExtLCTerm pTLam =   ExtLCTLam   <$> (atsignBackslash *> identifier <* colon <* asterisk)-  <*> (dot *> pLC)+  <*> (dot *> pTerm)  pLam :: Parser ExtLCTerm pLam =   ExtLCLam   <$> (backslash *> identifier)   <*> (colon *> pType)-  <*> (dot *> pLC)+  <*> (dot *> pTerm)  pApp :: Parser ExtLCTerm pApp = foldl' (&) <$> pATerm <*> many pAppArg@@ -39,13 +42,16 @@     else flip ExtLCApp <$> pATerm  pATerm :: Parser ExtLCTerm-pATerm = pVar <|> pMVar <|> parenthesized pLC+pATerm = pVar <|> pMVar <|> parenthesized pTerm  pVar :: Parser ExtLCTerm pVar = ExtLCVar <$> identifier  pMVar :: Parser ExtLCTerm pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)++pTopType :: Parser ExtLCType+pTopType = topParser pType  pType :: Parser ExtLCType pType = pUniv <|> pArr
src/LambdaCube/SystemF/PrettyPrinter.hs view
@@ -2,34 +2,45 @@   TODO: Use real pretty printer library -} {-# LANGUAGE OverloadedStrings #-}-module LambdaCube.SystemF.PrettyPrinter where+module LambdaCube.SystemF.PrettyPrinter+  ( prettyUnnamedTerm+  , prettyShowUnnamedTerm+  , prettyUnnamedType+  , prettyShowUnnamedType+  ) where  import           Data.Text                       (Text) import qualified Data.Text                       as Text import           LambdaCube.Common.PrettyPrinter import           LambdaCube.SystemF.Ast -prettyUnnamedType :: LCType -> Text-prettyUnnamedType = prettyUnnamedTypePrec 0- prettyUnnamedTerm :: LCTerm -> Text prettyUnnamedTerm = prettyUnnamedTermPrec 0 -prettyUnnamedTypePrec :: Int -> LCType -> Text-prettyUnnamedTypePrec = go-  where-    go _ LCBase      = "#"-    go _ (LCTVar i)  = Text.pack $ show i-    go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]-    go p (LCUniv b)  = wrapIfSpaced (p > 0) ["! : * ,", go 0 b]+prettyShowUnnamedTerm :: LCTerm -> String+prettyShowUnnamedTerm = Text.unpack . prettyUnnamedTerm +prettyUnnamedType :: LCType -> Text+prettyUnnamedType = prettyUnnamedTypePrec 0++prettyShowUnnamedType :: LCType -> String+prettyShowUnnamedType = Text.unpack . prettyUnnamedType+ prettyUnnamedTermPrec :: Int -> LCTerm -> Text prettyUnnamedTermPrec = go   where     pTP = prettyUnnamedTypePrec -    go _ (LCVar i)    = Text.pack $ show i+    go _ (LCVar x)    = Text.pack $ show x     go p (LCLam t b)  = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]     go p (LCApp f a)  = wrapIfSpaced (p > 1) [go 1 f, go 2 a]     go p (LCTLam b)   = wrapIfSpaced (p > 0) ["@\\ : * .", go 0 b]     go p (LCTApp f t) = wrapIfSpaced (p > 1) [go 1 f, "@" <> pTP 1 t]++prettyUnnamedTypePrec :: Int -> LCType -> Text+prettyUnnamedTypePrec = go+  where+    go _ LCBase      = "#"+    go _ (LCTVar p)  = Text.pack $ show p+    go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]+    go p (LCUniv b)  = wrapIfSpaced (p > 0) ["! : * ,", go 0 b]
src/LambdaCube/SystemF/Substitution.hs view
@@ -1,82 +1,153 @@-module LambdaCube.SystemF.Substitution where+{-# LANGUAGE ViewPatterns #-}+module LambdaCube.SystemF.Substitution+  ( substituteType+  , substituteTypeInType+  , substituteValue+  , substituteNormalInNormal+  , substituteTypeInNormal +  , shiftType+  ) where+ import           LambdaCube.SystemF.Ast import           LambdaCube.SystemF.Lifter -substituteType :: Int -> LCType -> LCTerm -> LCTerm-substituteType n v = go n+substituteType :: LCType -> Int -> LCTerm -> LCTerm+substituteType v = substDefType (v, 0)++substituteTypeInType :: LCType -> Int -> LCType -> LCType+substituteTypeInType v = substDefTypeInType (v, 0)++substituteValue :: LCValue -> Int -> LCTerm -> LCTerm+substituteValue v = substDefValue (v, 0, 0)++substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm+substituteNormalInNormal v = substDefNormalInNormal (v, 0, 0)++substituteTypeInNormal :: LCType -> Int -> LCNormalTerm -> LCNormalTerm+substituteTypeInNormal v = substDefTypeInNormal (v, 0)++substDefType :: (LCType, Int) -> Int -> LCTerm -> LCTerm+substDefType = go   where-    go _ e@(LCVar _)  = e-    go m (LCLam t b)  = LCLam (substituteTypeInType m v t) $ go m b-    go m (LCApp f a)  = go m f `LCApp` go m a-    go m (LCTLam b)   = LCTLam $ go (m + 1) b-    go m (LCTApp f t) = go m f `LCTApp` substituteTypeInType m v t+    go _      _ e@(LCVar _)  = e+    go dv     p (LCLam t b)  = LCLam (substDefTypeInType dv p t) $ go dv p b+    go dv     p (LCApp f a)  = go dv p f `LCApp` go dv p a+    go (v, r) p (LCTLam b)   = LCTLam $ go (v, r + 1) (p + 1) b+    go dv     p (LCTApp f t) = go dv p f `LCTApp` substDefTypeInType dv p t -substituteTypeInType :: Int -> LCType -> LCType -> LCType-substituteTypeInType n v = go n+substDefTypeInType :: (LCType, Int) -> Int -> LCType -> LCType+substDefTypeInType = go   where-    go _ LCBase       = LCBase-    go m e@(LCTVar l) = if m == l then v else e-    go m (LCArr a b)  = go m a `LCArr` go m b-    go m (LCUniv a)   = LCUniv $ go (m + 1) a+    go _      _ LCBase                     = LCBase+    go dv     p (LCTVar ((== p) -> True))  = shiftType dv+    go _      p e@(LCTVar ((< p) -> True)) = e+    go _      _ (LCTVar q)                 = LCTVar $ q - 1+    go dv     p (LCArr a b)                = go dv p a `LCArr` go dv p b+    go (v, r) p (LCUniv a)                 = LCUniv $ go (v, r + 1) (p + 1) a -substituteValue :: Int -> LCValue -> LCTerm -> LCTerm-substituteValue n v = go n+substDefValue :: (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm+substDefValue = go   where-    go m e@(LCVar l)  = if m == l then liftLCValue v else e-    go m (LCLam t b)  = LCLam t $ go (m + 1) b-    go m (LCApp f a)  = go m f `LCApp` go m a-    go m (LCTLam b)   = LCTLam $ go m b-    go m (LCTApp f t) = go m f `LCTApp` t+    go dv        x (LCVar ((== x) -> True))  = shiftValue dv+    go _         x e@(LCVar ((< x) -> True)) = e+    go _         _ (LCVar y)                 = LCVar $ y - 1+    go (v, r, s) x (LCLam t b)               = LCLam t $ go (v, r, s + 1) (x + 1) b+    go dv        x (LCApp f a)               = go dv x f `LCApp` go dv x a+    go (v, r, s) x (LCTLam b)                = LCTLam $ go (v, r + 1, s) x b+    go dv        x (LCTApp f t)              = go dv x f `LCTApp` t -substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm-substituteNormalInNormal n v = go n+substDefNormalInNormal :: (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm+substDefNormalInNormal = go   where-    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b-    go m (LCNormTLam b)  = LCNormTLam $ go m b-    go m (LCNormNeut nt) = substituteNormalInNeutral m v nt+    go (v, r, s) x (LCNormLam t b) = LCNormLam t $ go (v, r, s + 1) (x + 1) b+    go (v, r, s) x (LCNormTLam b)  = LCNormTLam $ go (v, r + 1, s) x b+    go dv        x (LCNormNeut nt) = substDefNormalInNeutral dv x nt -substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm-substituteNormalInNeutral n v = go n+substDefNormalInNeutral :: (LCNormalTerm, Int, Int) -> Int -> LCNeutralTerm -> LCNormalTerm+substDefNormalInNeutral dv x = go   where-    go m e@(LCNeutVar l)-      | m == l = v-      | otherwise = LCNormNeut e-    go m (LCNeutApp f a) =-      case go m f of-        LCNormLam _ b -> substituteNormalInNormal 0 a' b+    go (LCNeutVar ((== x) -> True)) = shiftNormal dv+    go e@(LCNeutVar ((< x) -> True)) = LCNormNeut e+    go (LCNeutVar y) = LCNormNeut . LCNeutVar $ y - 1+    go (LCNeutApp f a) =+      case go f of+        LCNormLam _ b -> substituteNormalInNormal a' 0 b         LCNormTLam _  -> error "Did you really type check this?"         LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'       where-        a' = substituteNormalInNormal m v a-    go m (LCNeutTApp f t) =-      case go m f of+        a' = substDefNormalInNormal dv x a+    go (LCNeutTApp f t) =+      case go f of         LCNormLam _ _ -> error "Did you really type check this?"-        LCNormTLam b  -> substituteTypeInNormal 0 t b+        LCNormTLam b  -> substituteTypeInNormal t 0 b         LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t -substituteTypeInNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm-substituteTypeInNormal n v = go n+substDefTypeInNormal :: (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm+substDefTypeInNormal = go   where-    go m (LCNormLam t b) = LCNormLam (substituteTypeInType m v t) $ go m b-    go m (LCNormTLam b)  = LCNormTLam $ go (m + 1) b-    go m (LCNormNeut nt) = substituteTypeInNeutral m v nt+    go dv     p (LCNormLam t b) = LCNormLam (substDefTypeInType dv p t) $ go dv p b+    go (v, r) p (LCNormTLam b)  = LCNormTLam $ go (v, r + 1) (p + 1) b+    go dv     p (LCNormNeut nt) = substDefTypeInNeutral dv p nt -substituteTypeInNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm-substituteTypeInNeutral n v = go n+substDefTypeInNeutral :: (LCType, Int) -> Int -> LCNeutralTerm -> LCNormalTerm+substDefTypeInNeutral dv p = go   where-    go _ e@(LCNeutVar _) = LCNormNeut e-    go m (LCNeutApp f a) =-      case go m f of-        LCNormLam _ b -> substituteNormalInNormal 0 a' b+    go e@(LCNeutVar _) = LCNormNeut e+    go (LCNeutApp f a) =+      case go f of+        LCNormLam _ b -> substituteNormalInNormal a' 0 b         LCNormTLam _  -> error "Did you really type check this?"         LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'       where-        a' = substituteTypeInNormal m v a-    go m (LCNeutTApp f t) =-      case go m f of+        a' = substDefTypeInNormal dv p a+    go (LCNeutTApp f t) =+      case go f of         LCNormLam _ _ -> error "Did you really type check this?"-        LCNormTLam b  -> substituteTypeInNormal 0 t' b+        LCNormTLam b  -> substituteTypeInNormal t' 0 b         LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t'       where-        t' = substituteTypeInType m v t+        t' = substDefTypeInType dv p t++shift :: (LCTerm, Int, Int) -> LCTerm+shift = shiftMin 0 0++shiftMin :: Int -> Int -> (LCTerm, Int, Int) -> LCTerm+shiftMin m' n' (v, r, s) = go m' n' v+  where+    go _ n (LCVar x)    = LCVar $ if x < n then x else x + s+    go m n (LCLam t b)  = LCLam (shiftTypeMin m (t, r)) $ go m (n + 1) b+    go m n (LCApp f a)  = go m n f `LCApp` go m n a+    go m n (LCTLam b)   = LCTLam $ go (m + 1) n b+    go m n (LCTApp f t) = go m n f `LCTApp` shiftTypeMin m (t, r)++shiftType :: (LCType, Int) -> LCType+shiftType = shiftTypeMin 0++shiftTypeMin :: Int -> (LCType, Int) -> LCType+shiftTypeMin m' (v, r) = go m' v+  where+    go _ LCBase      = LCBase+    go m (LCTVar p)  = LCTVar $ if p < m then p else p + r+    go m (LCArr a b) = go m a `LCArr` go m b+    go m (LCUniv a)  = LCUniv $ go (m + 1) a++shiftValue :: (LCValue, Int, Int) -> LCTerm+shiftValue (v, r, s) = shift (liftLCValue v, r, s)++shiftNormal :: (LCNormalTerm, Int, Int) -> LCNormalTerm+shiftNormal = shiftNormalMin 0 0++shiftNormalMin :: Int -> Int -> (LCNormalTerm, Int, Int) -> LCNormalTerm+shiftNormalMin m' n' (v, r, s) = go m' n' v+  where+    go m n (LCNormLam t b) = LCNormLam (shiftTypeMin m (t, r)) $ go m (n + 1) b+    go m n (LCNormTLam b)  = LCNormTLam $ go (m + 1) n b+    go m n (LCNormNeut nt) = LCNormNeut $ shiftNeutralMin m n (nt, r, s)++shiftNeutralMin :: Int -> Int -> (LCNeutralTerm, Int, Int) -> LCNeutralTerm+shiftNeutralMin m n (v, r, s) = go v+  where+    go (LCNeutVar x)    = LCNeutVar $ if x < n then x else x + s+    go (LCNeutApp f a)  = go f `LCNeutApp` shiftNormalMin m n (a, r, s)+    go (LCNeutTApp f t) = go f `LCNeutTApp` shiftTypeMin m (t, r)
src/LambdaCube/SystemF/TH.hs view
@@ -1,45 +1,57 @@ module LambdaCube.SystemF.TH-  ( lc+  ( qTerm+  , qType   ) where  import           Data.Data                  (Data) import           Data.Generics              (extQ)-import           Data.Text                  (Text)-import qualified Data.Text                  as Text+import           LambdaCube.Common.TH import           LambdaCube.SystemF.Ast import           LambdaCube.SystemF.Parser import           Language.Haskell.TH.Lib    (ExpQ, varE) import           Language.Haskell.TH.Quote  (QuasiQuoter (..))-import           Language.Haskell.TH.Syntax (Loc (loc_start), dataToExpQ, lift,-                                             location, mkName)-import qualified Text.Megaparsec            as P-import qualified Text.Megaparsec.Error      as PE+import           Language.Haskell.TH.Syntax (mkName) -lc :: QuasiQuoter-lc =+qTerm :: QuasiQuoter+qTerm =   QuasiQuoter-    { quoteExp = expLc+    { quoteExp = qExpTerm     , quotePat = undefined     , quoteType = undefined     , quoteDec = undefined     } -expLc :: String -> ExpQ-expLc str = do-  l <- location-  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of-    Right e  -> dataToExpQ converter e-    Left err -> fail $ PE.errorBundlePretty err+qExpTerm :: String -> ExpQ+qExpTerm = qExpBase pTopTerm converter   where     converter :: Data b => b -> Maybe ExpQ     converter =-      const Nothing+      converterBase       `extQ` quotedMVar       `extQ` quotedMTVar-      `extQ` (Just . lift :: Text -> Maybe ExpQ)      quotedMVar (ExtLCMVar x) = Just . varE $ mkName x     quotedMVar _             = Nothing++    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x+    quotedMTVar _              = Nothing++qType :: QuasiQuoter+qType =+  QuasiQuoter+    { quoteExp = qExpType+    , quotePat = undefined+    , quoteType = undefined+    , quoteDec = undefined+    }++qExpType :: String -> ExpQ+qExpType = qExpBase pTopType converter+  where+    converter :: Data b => b -> Maybe ExpQ+    converter =+      converterBase+      `extQ` quotedMTVar      quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x     quotedMTVar _              = Nothing
src/LambdaCube/SystemF/TypeChecker.hs view
@@ -1,4 +1,6 @@-module LambdaCube.SystemF.TypeChecker where+module LambdaCube.SystemF.TypeChecker+  ( infer+  ) where  import           Data.List                       (uncons) import           LambdaCube.SystemF.Ast@@ -7,7 +9,7 @@ infer :: LCTerm -> LCType infer = go []   where-    go tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl+    go tl (LCVar x) = maybe (error "Out-of-scope variable") fst . uncons $ drop x tl     go tl (LCLam t b) = t `LCArr` go (t : tl) b     go tl (LCApp f a)       | LCArr at rt <- go tl f@@ -15,9 +17,9 @@       = rt       | otherwise       = error "Function argument type mismatch"-    go tl (LCTLam b) = LCUniv $ go tl b+    go tl (LCTLam b) = LCUniv $ go (fmap (shiftType . (, 1)) tl) b     go tl (LCTApp f t)       | LCUniv rt <- go tl f-      = substituteTypeInType 0 t rt+      = substituteTypeInType t 0 rt       | otherwise       = error "Function argument type mismatch"
src/LambdaCube/SystemFw.hs view
@@ -1,6 +1,7 @@ module LambdaCube.SystemFw   ( module LambdaCube.SystemFw.Ast   , module LambdaCube.SystemFw.Elaborator+  , module LambdaCube.SystemFw.Evaluator   , module LambdaCube.SystemFw.Lifter   , module LambdaCube.SystemFw.Normalizer   , module LambdaCube.SystemFw.Parser@@ -13,6 +14,7 @@ import LambdaCube.SystemFw.Ast  import LambdaCube.SystemFw.Elaborator+import LambdaCube.SystemFw.Evaluator import LambdaCube.SystemFw.Lifter import LambdaCube.SystemFw.Normalizer import LambdaCube.SystemFw.Parser
src/LambdaCube/SystemFw/Ast.hs view
@@ -4,12 +4,16 @@ import           Data.Text                  (Text) import           Language.Haskell.TH.Syntax (Lift) -data ExtLCKind-  = ExtLCStar-  | ExtLCKArr ExtLCKind ExtLCKind-  | ExtLCMKVar String+data ExtLCTerm+  = ExtLCVar Text+  | ExtLCLam Text ExtLCType ExtLCTerm+  | ExtLCApp ExtLCTerm ExtLCTerm+  | ExtLCTLam Text ExtLCKind ExtLCTerm+  | ExtLCTApp ExtLCTerm ExtLCType+  | ExtLCMVar String   deriving stock (Eq, Show, Data, Lift)-infixr 5 `ExtLCKArr`+infixl 6 `ExtLCApp`+infixl 6 `ExtLCTApp`  data ExtLCType   = ExtLCBase@@ -23,22 +27,22 @@ infixr 5 `ExtLCArr` infixl 6 `ExtLCTTApp` -data ExtLCTerm-  = ExtLCVar Text-  | ExtLCLam Text ExtLCType ExtLCTerm-  | ExtLCApp ExtLCTerm ExtLCTerm-  | ExtLCTLam Text ExtLCKind ExtLCTerm-  | ExtLCTApp ExtLCTerm ExtLCType-  | ExtLCMVar String+data ExtLCKind+  = ExtLCStar+  | ExtLCKArr ExtLCKind ExtLCKind+  | ExtLCMKVar String   deriving stock (Eq, Show, Data, Lift)-infixl 6 `ExtLCApp`-infixl 6 `ExtLCTApp`+infixr 5 `ExtLCKArr` -data LCKind-  = LCStar-  | LCKArr LCKind LCKind+data LCTerm+  = LCVar Int+  | LCLam LCType LCTerm+  | LCApp LCTerm LCTerm+  | LCTLam LCKind LCTerm+  | LCTApp LCTerm LCType   deriving stock (Eq, Show, Data, Lift)-infixr 5 `LCKArr`+infixl 6 `LCApp`+infixl 6 `LCTApp`  data LCType   = LCBase@@ -51,15 +55,11 @@ infixr 5 `LCArr` infixl 6 `LCTTApp` -data LCTerm-  = LCVar Int-  | LCLam LCType LCTerm-  | LCApp LCTerm LCTerm-  | LCTLam LCKind LCTerm-  | LCTApp LCTerm LCType+data LCKind+  = LCStar+  | LCKArr LCKind LCKind   deriving stock (Eq, Show, Data, Lift)-infixl 6 `LCApp`-infixl 6 `LCTApp`+infixr 5 `LCKArr`  data LCValue   = LCValLam LCType LCTerm
src/LambdaCube/SystemFw/Elaborator.hs view
@@ -1,4 +1,8 @@-module LambdaCube.SystemFw.Elaborator where+module LambdaCube.SystemFw.Elaborator+  ( elaborate+  , elaborateType+  , elaborateKind+  ) where  import           Data.List               (elemIndex) import           Data.Text               (Text)@@ -15,7 +19,7 @@       = error $ "Term variable " <> Text.unpack x <> " is not in scope"     go tl vl (ExtLCLam x t b) = LCLam (elaborateType tl t) $ go tl (x : vl) b     go tl vl (ExtLCApp f a) = go tl vl f `LCApp` go tl vl a-    go tl vl (ExtLCTLam x k b) = LCTLam (elaborateKind k) $ go (x : tl) vl b+    go tl vl (ExtLCTLam p k b) = LCTLam (elaborateKind k) $ go (p : tl) vl b     go tl vl (ExtLCTApp f t) = go tl vl f `LCTApp` elaborateType tl t     go _  _  (ExtLCMVar _) = error "invalid TemplateHaskell code splicer" @@ -23,14 +27,14 @@ elaborateType = go   where     go _ ExtLCBase = LCBase-    go l (ExtLCTVar x)-      | Just n <- x `elemIndex` l+    go l (ExtLCTVar p)+      | Just n <- p `elemIndex` l       = LCTVar n       | otherwise-      = error $ "Type variable " <> Text.unpack x <> " is not in scope"+      = error $ "Type variable " <> Text.unpack p <> " is not in scope"     go l (ExtLCArr a b) = go l a `LCArr` go l b-    go l (ExtLCUniv x k a) = LCUniv (elaborateKind k) $ go (x : l) a-    go l (ExtLCTTLam x k b) = LCTTLam (elaborateKind k) $ go (x : l) b+    go l (ExtLCUniv p k a) = LCUniv (elaborateKind k) $ go (p : l) a+    go l (ExtLCTTLam p k b) = LCTTLam (elaborateKind k) $ go (p : l) b     go l (ExtLCTTApp f a) = go l f `LCTTApp` go l a     go _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
src/LambdaCube/SystemFw/Evaluator.hs view
@@ -1,4 +1,6 @@-module LambdaCube.SystemFw.Evaluator where+module LambdaCube.SystemFw.Evaluator+  ( evaluate+  ) where  import           LambdaCube.SystemFw.Ast import           LambdaCube.SystemFw.Substitution@@ -11,12 +13,12 @@     go (LCApp f a)       | LCValLam _ b <- go f       , v <- go a-      = go $ substituteValue 0 v b+      = go $ substituteValue v 0 b       | otherwise       = error "Did you really type check this?"     go (LCTLam k b) = LCValTLam k b     go (LCTApp f t)       | LCValTLam _ b <- go f-      = go $ substituteType 0 t b+      = go $ substituteType t 0 b       | otherwise       = error "Did you really type check this?"
src/LambdaCube/SystemFw/Lifter.hs view
@@ -1,4 +1,7 @@-module LambdaCube.SystemFw.Lifter where+module LambdaCube.SystemFw.Lifter+  ( liftLCValue+  , liftLCNormal+  ) where  import           LambdaCube.SystemFw.Ast @@ -12,6 +15,6 @@ liftLCNormal (LCNormNeut nt)  = liftLCNeutral nt  liftLCNeutral :: LCNeutralTerm -> LCTerm-liftLCNeutral (LCNeutVar n)    = LCVar n+liftLCNeutral (LCNeutVar x)    = LCVar x liftLCNeutral (LCNeutApp f a)  = liftLCNeutral f `LCApp` liftLCNormal a liftLCNeutral (LCNeutTApp f t) = liftLCNeutral f `LCTApp` t
src/LambdaCube/SystemFw/Normalizer.hs view
@@ -1,4 +1,6 @@-module LambdaCube.SystemFw.Normalizer where+module LambdaCube.SystemFw.Normalizer+  ( normalize+  ) where  import           LambdaCube.SystemFw.Ast import           LambdaCube.SystemFw.Substitution@@ -6,18 +8,18 @@ normalize :: LCTerm -> LCNormalTerm normalize = go   where-    go (LCVar n) = LCNormNeut $ LCNeutVar n+    go (LCVar x) = LCNormNeut $ LCNeutVar x     go (LCLam t b) = LCNormLam t $ go b     go (LCTLam k b) = LCNormTLam k $ go b     go (LCApp f a) =       case go f of-        LCNormLam _ b   -> substituteNormalInNormal 0 a' b-        LCNormTLam _ _  -> error "Did you really type check this?"-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'+        LCNormLam _ b  -> substituteNormalInNormal a' 0 b+        LCNormTLam _ _ -> error "Did you really type check this?"+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'       where         a' = go a     go (LCTApp f t) =       case go f of-        LCNormLam _ _   -> error "Did you really type check this?"-        LCNormTLam _ b  -> substituteTypeInNormal 0 t b-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutTApp` t+        LCNormLam _ _  -> error "Did you really type check this?"+        LCNormTLam _ b -> substituteTypeInNormal t 0 b+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t
src/LambdaCube/SystemFw/Parser.hs view
@@ -1,4 +1,8 @@-module LambdaCube.SystemFw.Parser where+module LambdaCube.SystemFw.Parser+  ( pTopTerm+  , pTopType+  , pTopKind+  ) where  import           Data.Foldable            (Foldable (foldl')) import           Data.Function            ((&))@@ -9,25 +13,25 @@ import           LambdaCube.SystemFw.Ast import           Text.Megaparsec -pTopLC :: Parser ExtLCTerm-pTopLC = topParser pLC+pTopTerm :: Parser ExtLCTerm+pTopTerm = topParser pTerm -pLC :: Parser ExtLCTerm-pLC = pTLam <|> pLam <|> pApp+pTerm :: Parser ExtLCTerm+pTerm = pTLam <|> pLam <|> pApp  pTLam :: Parser ExtLCTerm pTLam =   ExtLCTLam   <$> (atsignBackslash *> identifier)   <*> (colon *> pKind)-  <*> (dot *> pLC)+  <*> (dot *> pTerm)  pLam :: Parser ExtLCTerm pLam =   ExtLCLam   <$> (backslash *> identifier)   <*> (colon *> pType)-  <*> (dot *> pLC)+  <*> (dot *> pTerm)  pApp :: Parser ExtLCTerm pApp = foldl' (&) <$> pATerm <*> many pAppArg@@ -40,7 +44,7 @@     else flip ExtLCApp <$> pATerm  pATerm :: Parser ExtLCTerm-pATerm = pVar <|> pMVar <|> parenthesized pLC+pATerm = pVar <|> pMVar <|> parenthesized pTerm  pVar :: Parser ExtLCTerm pVar = ExtLCVar <$> identifier@@ -48,6 +52,9 @@ pMVar :: Parser ExtLCTerm pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier) +pTopType :: Parser ExtLCType+pTopType = topParser pType+ pType :: Parser ExtLCType pType = pTTLam <|> pUniv <|> pArr @@ -82,6 +89,9 @@  pMTVar :: Parser ExtLCType pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)++pTopKind :: Parser ExtLCKind+pTopKind = topParser pKind  pKind :: Parser ExtLCKind pKind = foldr1 ExtLCKArr <$> sepBy1 pAKind rightArrow
src/LambdaCube/SystemFw/PrettyPrinter.hs view
@@ -2,28 +2,50 @@   TODO: Use real pretty printer library -} {-# LANGUAGE OverloadedStrings #-}-module LambdaCube.SystemFw.PrettyPrinter where+module LambdaCube.SystemFw.PrettyPrinter+  ( prettyUnnamedTerm+  , prettyShowUnnamedTerm+  , prettyUnnamedType+  , prettyShowUnnamedType+  , prettyUnnamedKind+  , prettyShowUnnamedKind+  ) where  import           Data.Text                       (Text) import qualified Data.Text                       as Text import           LambdaCube.Common.PrettyPrinter import           LambdaCube.SystemFw.Ast -prettyUnnamedKind :: LCKind -> Text-prettyUnnamedKind = prettyUnnamedKindPrec 0+prettyUnnamedTerm :: LCTerm -> Text+prettyUnnamedTerm = prettyUnnamedTermPrec 0 +prettyShowUnnamedTerm :: LCTerm -> String+prettyShowUnnamedTerm = Text.unpack . prettyUnnamedTerm+ prettyUnnamedType :: LCType -> Text prettyUnnamedType = prettyUnnamedTypePrec 0 -prettyUnnamedTerm :: LCTerm -> Text-prettyUnnamedTerm = prettyUnnamedTermPrec 0+prettyShowUnnamedType :: LCType -> String+prettyShowUnnamedType = Text.unpack . prettyUnnamedType -prettyUnnamedKindPrec :: Int -> LCKind -> Text-prettyUnnamedKindPrec = go+prettyUnnamedKind :: LCKind -> Text+prettyUnnamedKind = prettyUnnamedKindPrec 0++prettyShowUnnamedKind :: LCKind -> String+prettyShowUnnamedKind = Text.unpack . prettyUnnamedKind++prettyUnnamedTermPrec :: Int -> LCTerm -> Text+prettyUnnamedTermPrec = go   where-    go _ LCStar       = "*"-    go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]+    pKP = prettyUnnamedKindPrec+    pTP = prettyUnnamedTypePrec +    go _ (LCVar i)    = Text.pack $ show i+    go p (LCLam t b)  = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]+    go p (LCApp f a)  = wrapIfSpaced (p > 1) [go 1 f, go 2 a]+    go p (LCTLam k b) = wrapIfSpaced (p > 0) ["@\\ :", pKP 0 k, ".", go 0 b]+    go p (LCTApp f t) = wrapIfSpaced (p > 1) [go 1 f, "@" <> pTP 1 t]+ prettyUnnamedTypePrec :: Int -> LCType -> Text prettyUnnamedTypePrec = go   where@@ -36,14 +58,8 @@     go p (LCTTLam k b) = wrapIfSpaced (p > 0) ["\\ :", pKP 0 k, ".", go 0 b]     go p (LCTTApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a] -prettyUnnamedTermPrec :: Int -> LCTerm -> Text-prettyUnnamedTermPrec = go+prettyUnnamedKindPrec :: Int -> LCKind -> Text+prettyUnnamedKindPrec = go   where-    pKP = prettyUnnamedKindPrec-    pTP = prettyUnnamedTypePrec--    go _ (LCVar i)    = Text.pack $ show i-    go p (LCLam t b)  = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]-    go p (LCApp f a)  = wrapIfSpaced (p > 1) [go 1 f, go 2 a]-    go p (LCTLam k b) = wrapIfSpaced (p > 0) ["@\\ :", pKP 0 k, ".", go 0 b]-    go p (LCTApp f t) = wrapIfSpaced (p > 1) [go 1 f, "@" <> pTP 1 t]+    go _ LCStar       = "*"+    go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
src/LambdaCube/SystemFw/Substitution.hs view
@@ -1,84 +1,154 @@-module LambdaCube.SystemFw.Substitution where+{-# LANGUAGE ViewPatterns #-}+module LambdaCube.SystemFw.Substitution+  ( substituteType+  , substituteTypeInType+  , substituteValue+  , substituteNormalInNormal+  , substituteTypeInNormal +  , shiftType+  ) where+ import           LambdaCube.SystemFw.Ast import           LambdaCube.SystemFw.Lifter -substituteType :: Int -> LCType -> LCTerm -> LCTerm-substituteType n v = go n+substituteType :: LCType -> Int -> LCTerm -> LCTerm+substituteType v = substDefType (v, 0)++substituteTypeInType :: LCType -> Int -> LCType -> LCType+substituteTypeInType v = substDefTypeInType (v, 0)++substituteValue :: LCValue -> Int -> LCTerm -> LCTerm+substituteValue v = substDefValue (v, 0, 0)++substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm+substituteNormalInNormal v = substDefNormalInNormal (v, 0, 0)++substituteTypeInNormal :: LCType -> Int -> LCNormalTerm -> LCNormalTerm+substituteTypeInNormal v = substDefTypeInNormal (v, 0)++substDefType :: (LCType, Int) -> Int -> LCTerm -> LCTerm+substDefType = go   where-    go _ e@(LCVar _)  = e-    go m (LCLam t b)  = LCLam (substituteTypeInType m v t) $ go m b-    go m (LCApp f a)  = go m f `LCApp` go m a-    go m (LCTLam k b) = LCTLam k $ go (m + 1) b-    go m (LCTApp f t) = go m f `LCTApp` substituteTypeInType m v t+    go _      _ e@(LCVar _)  = e+    go dv     p (LCLam t b)  = LCLam (substDefTypeInType dv p t) $ go dv p b+    go dv     p (LCApp f a)  = go dv p f `LCApp` go dv p a+    go (v, r) p (LCTLam k b) = LCTLam k $ go (v, r + 1) (p + 1) b+    go dv     p (LCTApp f t) = go dv p f `LCTApp` substDefTypeInType dv p t -substituteTypeInType :: Int -> LCType -> LCType -> LCType-substituteTypeInType n v = go n+substDefTypeInType :: (LCType, Int) -> Int -> LCType -> LCType+substDefTypeInType = go   where-    go _ LCBase        = LCBase-    go m e@(LCTVar l)  = if m == l then v else e-    go m (LCArr a b)   = go m a `LCArr` go m b-    go m (LCUniv k a)  = LCUniv k $ go (m + 1) a-    go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b-    go m (LCTTApp f a) = go m f `LCTTApp` go m a+    go _      _ LCBase                     = LCBase+    go dv     p (LCTVar ((== p) -> True))  = shiftType dv+    go _      p e@(LCTVar ((< p) -> True)) = e+    go _      _ (LCTVar q)                 = LCTVar $ q - 1+    go dv     p (LCArr a b)                = go dv p a `LCArr` go dv p b+    go (v, r) p (LCUniv k a)               = LCUniv k $ go (v, r + 1) (p + 1) a+    go (v, r) p (LCTTLam k b)              = LCTTLam k $ go (v, r + 1) (p + 1) b+    go dv     p (LCTTApp f a)              = go dv p f `LCTTApp` go dv p a -substituteValue :: Int -> LCValue -> LCTerm -> LCTerm-substituteValue n v = go n+substDefValue :: (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm+substDefValue = go   where-    go m e@(LCVar l)  = if m == l then liftLCValue v else e-    go m (LCLam t b)  = LCLam t $ go (m + 1) b-    go m (LCApp f a)  = go m f `LCApp` go m a-    go m (LCTLam k b) = LCTLam k $ go m b-    go m (LCTApp f t) = go m f `LCTApp` t+    go dv        x (LCVar ((== x) -> True))  = shiftValue dv+    go _         x e@(LCVar ((< x) -> True)) = e+    go _         _ (LCVar y)                 = LCVar $ y - 1+    go (v, r, s) x (LCLam t b)  = LCLam t $ go (v, r, s + 1) (x + 1) b+    go dv        x (LCApp f a)  = go dv x f `LCApp` go dv x a+    go (v, r, s) x (LCTLam k b) = LCTLam k $ go (v, r + 1, s) x b+    go dv        x (LCTApp f t) = go dv x f `LCTApp` t -substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm-substituteNormalInNormal n v = go n+substDefNormalInNormal :: (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm+substDefNormalInNormal = go   where-    go m (LCNormLam t b)  = LCNormLam t $ go (m + 1) b-    go m (LCNormTLam k b) = LCNormTLam k $ go m b-    go m (LCNormNeut nt)  = substituteNormalInNeutral m v nt+    go (v, r, s) x (LCNormLam t b)  = LCNormLam t $ go (v, r, s + 1) (x + 1) b+    go (v, r, s) x (LCNormTLam k b) = LCNormTLam k $ go (v, r + 1, s) x b+    go dv        x (LCNormNeut nt)  = substDefNormalInNeutral dv x nt -substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm-substituteNormalInNeutral n v = go n+substDefNormalInNeutral :: (LCNormalTerm, Int, Int) -> Int -> LCNeutralTerm -> LCNormalTerm+substDefNormalInNeutral dv x = go   where-    go m e@(LCNeutVar l)-      | m == l = v-      | otherwise = LCNormNeut e-    go m (LCNeutApp f a) =-      case go m f of-        LCNormLam _ b  -> substituteNormalInNormal 0 a' b+    go (LCNeutVar ((== x) -> True)) = shiftNormal dv+    go e@(LCNeutVar ((< x) -> True)) = LCNormNeut e+    go (LCNeutVar y) = LCNormNeut . LCNeutVar $ y - 1+    go (LCNeutApp f a) =+      case go f of+        LCNormLam _ b  -> substituteNormalInNormal a' 0 b         LCNormTLam _ _ -> error "Did you really type check this?"         LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'       where-        a' = substituteNormalInNormal m v a-    go m (LCNeutTApp f t) =-      case go m f of+        a' = substDefNormalInNormal dv x a+    go (LCNeutTApp f t) =+      case go f of         LCNormLam _ _  -> error "Did you really type check this?"-        LCNormTLam _ b -> substituteTypeInNormal 0 t b+        LCNormTLam _ b -> substituteTypeInNormal t 0 b         LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t -substituteTypeInNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm-substituteTypeInNormal n v = go n+substDefTypeInNormal :: (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm+substDefTypeInNormal = go   where-    go m (LCNormLam t b)  = LCNormLam (substituteTypeInType m v t) $ go m b-    go m (LCNormTLam k b) = LCNormTLam k $ go (m + 1) b-    go m (LCNormNeut nt)  = substituteTypeInNeutral m v nt+    go dv     p (LCNormLam t b)  = LCNormLam (substDefTypeInType dv p t) $ go dv p b+    go (v, r) p (LCNormTLam k b) = LCNormTLam k $ go (v, r + 1) (p + 1) b+    go dv     p (LCNormNeut nt)  = substDefTypeInNeutral dv p nt -substituteTypeInNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm-substituteTypeInNeutral n v = go n+substDefTypeInNeutral :: (LCType, Int) -> Int -> LCNeutralTerm -> LCNormalTerm+substDefTypeInNeutral dv p = go   where-    go _ e@(LCNeutVar _) = LCNormNeut e-    go m (LCNeutApp f a) =-      case go m f of-        LCNormLam _ b  -> substituteNormalInNormal 0 a' b+    go e@(LCNeutVar _) = LCNormNeut e+    go (LCNeutApp f a) =+      case go f of+        LCNormLam _ b  -> substituteNormalInNormal a' 0 b         LCNormTLam _ _ -> error "Did you really type check this?"         LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'       where-        a' = substituteTypeInNormal m v a-    go m (LCNeutTApp f t) =-      case go m f of+        a' = substDefTypeInNormal dv p a+    go (LCNeutTApp f t) =+      case go f of         LCNormLam _ _  -> error "Did you really type check this?"-        LCNormTLam _ b -> substituteTypeInNormal 0 t' b+        LCNormTLam _ b -> substituteTypeInNormal t' 0 b         LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t'       where-        t' = substituteTypeInType m v t+        t' = substDefTypeInType dv p t++shift :: (LCTerm, Int, Int) -> LCTerm+shift (v, r, s) = go 0 0 v+  where+    go _ n (LCVar x)    = LCVar $ if x < n then x else x + s+    go m n (LCLam t b)  = LCLam (shiftTypeMin m (t, r)) $ go m (n + 1) b+    go m n (LCApp f a)  = go m n f `LCApp` go m n a+    go m n (LCTLam k b) = LCTLam k $ go (m + 1) n b+    go m n (LCTApp f t) = go m n f `LCTApp` shiftTypeMin m (t, r)++shiftType :: (LCType, Int) -> LCType+shiftType = shiftTypeMin 0++shiftTypeMin :: Int -> (LCType, Int) -> LCType+shiftTypeMin m' (v, r) = go m' v+  where+    go _ LCBase        = LCBase+    go m (LCTVar p)    = LCTVar $ if p < m then p else p + r+    go m (LCArr a b)   = go m a `LCArr` go m b+    go m (LCUniv k a)  = LCUniv k $ go (m + 1) a+    go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b+    go m (LCTTApp f a) = go m f `LCTTApp` go m a++shiftValue :: (LCValue, Int, Int) -> LCTerm+shiftValue (v, r, s) = shift (liftLCValue v, r, s)++shiftNormal :: (LCNormalTerm, Int, Int) -> LCNormalTerm+shiftNormal = shiftNormalMin 0 0++shiftNormalMin :: Int -> Int -> (LCNormalTerm, Int, Int) -> LCNormalTerm+shiftNormalMin m' n' (v, r, s) = go m' n' v+  where+    go m n (LCNormLam t b)  = LCNormLam (shiftTypeMin m (t, r)) $ go m (n + 1) b+    go m n (LCNormTLam k b) = LCNormTLam k $ go (m + 1) n b+    go m n (LCNormNeut nt)  = LCNormNeut $ shiftNeutralMin m n (nt, r, s)++shiftNeutralMin :: Int -> Int -> (LCNeutralTerm, Int, Int) -> LCNeutralTerm+shiftNeutralMin m n (v, r, s) = go v+  where+    go (LCNeutVar x)    = LCNeutVar $ if x < n then x else x + s+    go (LCNeutApp f a)  = go f `LCNeutApp` shiftNormalMin m n (a, r, s)+    go (LCNeutTApp f t) = go f `LCNeutTApp` shiftTypeMin m (t, r)
src/LambdaCube/SystemFw/TH.hs view
@@ -1,49 +1,86 @@ module LambdaCube.SystemFw.TH-  ( lc+  ( qTerm+  , qType+  , qKind   ) where  import           Data.Data                  (Data) import           Data.Generics              (extQ)-import           Data.Text                  (Text)-import qualified Data.Text                  as Text+import           LambdaCube.Common.TH import           LambdaCube.SystemFw.Ast import           LambdaCube.SystemFw.Parser import           Language.Haskell.TH.Lib    (ExpQ, varE) import           Language.Haskell.TH.Quote  (QuasiQuoter (..))-import           Language.Haskell.TH.Syntax (Loc (loc_start), dataToExpQ, lift,-                                             location, mkName)-import qualified Text.Megaparsec            as P-import qualified Text.Megaparsec.Error      as PE+import           Language.Haskell.TH.Syntax (mkName) -lc :: QuasiQuoter-lc =+qTerm :: QuasiQuoter+qTerm =   QuasiQuoter-    { quoteExp = expLc+    { quoteExp = qExpTerm     , quotePat = undefined     , quoteType = undefined     , quoteDec = undefined     } -expLc :: String -> ExpQ-expLc str = do-  l <- location-  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of-    Right e  -> dataToExpQ converter e-    Left err -> fail $ PE.errorBundlePretty err+qExpTerm :: String -> ExpQ+qExpTerm = qExpBase pTopTerm converter   where     converter :: Data b => b -> Maybe ExpQ     converter =-      const Nothing+      converterBase       `extQ` quotedMVar       `extQ` quotedMTVar       `extQ` quotedMKVar-      `extQ` (Just . lift :: Text -> Maybe ExpQ)      quotedMVar (ExtLCMVar x) = Just . varE $ mkName x     quotedMVar _             = Nothing      quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x     quotedMTVar _              = Nothing++    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x+    quotedMKVar _              = Nothing++qType :: QuasiQuoter+qType =+  QuasiQuoter+    { quoteExp = qExpType+    , quotePat = undefined+    , quoteType = undefined+    , quoteDec = undefined+    }++qExpType :: String -> ExpQ+qExpType = qExpBase pTopType converter+  where+    converter :: Data b => b -> Maybe ExpQ+    converter =+      converterBase+      `extQ` quotedMTVar+      `extQ` quotedMKVar++    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x+    quotedMTVar _              = Nothing++    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x+    quotedMKVar _              = Nothing++qKind :: QuasiQuoter+qKind =+  QuasiQuoter+    { quoteExp = qExpKind+    , quotePat = undefined+    , quoteType = undefined+    , quoteDec = undefined+    }++qExpKind :: String -> ExpQ+qExpKind = qExpBase pTopKind converter+  where+    converter :: Data b => b -> Maybe ExpQ+    converter =+      converterBase+      `extQ` quotedMKVar      quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x     quotedMKVar _              = Nothing
src/LambdaCube/SystemFw/TypeChecker.hs view
@@ -1,5 +1,10 @@-module LambdaCube.SystemFw.TypeChecker where+module LambdaCube.SystemFw.TypeChecker+  ( reduceType +  , infer+  , inferKind+  ) where+ import           Data.List                        (uncons) import           LambdaCube.SystemFw.Ast import           LambdaCube.SystemFw.Substitution@@ -15,37 +20,39 @@     go (LCTTApp f a)       | LCTTLam _ b <- go f       , v <- go a-      = go $ substituteTypeInType 0 v b+      = go $ substituteTypeInType v 0 b       | otherwise       = error "Did you really kind check this?"  infer :: LCTerm -> LCType-infer = go []+infer = go [] []   where-    go tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl-    go tl (LCLam t b)-      | LCStar <- inferKind t-      = v `LCArr` go (v : tl) b+    go _  tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl+    go kl tl (LCLam t b)+      | LCStar <- inferKind kl t+      = v `LCArr` go kl (v : tl) b       | otherwise       = error "Function argument kind mismatch"       where         v = reduceType t-    go tl (LCApp f a)-      | LCArr at rt <- go tl f-      , at == go tl a+    go kl tl (LCApp f a)+      | LCArr at rt <- go kl tl f+      , at == go kl tl a       = rt       | otherwise       = error "Function argument type mismatch"-    go tl (LCTLam k b) = LCUniv k $ go tl b-    go tl (LCTApp f t)-      | LCUniv tk rt <- go tl f-      , tk == inferKind t-      = substituteTypeInType 0 t rt+    go kl tl (LCTLam k b) = LCUniv k $ go (k : kl) (fmap (shiftType . (, 1)) tl) b+    go kl tl (LCTApp f t)+      | LCUniv tk rt <- go kl tl f+      , tk == inferKind kl t+      = substituteTypeInType v 0 rt       | otherwise       = error "Function argument kind mismatch"+      where+        v = reduceType t -inferKind :: LCType -> LCKind-inferKind = go []+inferKind :: [LCKind] -> LCType -> LCKind+inferKind = go   where     go _  LCBase = LCStar     go kl (LCTVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n kl
src/LambdaCube/SystemFw_.hs view
@@ -1,6 +1,7 @@ module LambdaCube.SystemFw_   ( module LambdaCube.SystemFw_.Ast   , module LambdaCube.SystemFw_.Elaborator+  , module LambdaCube.SystemFw_.Evaluator   , module LambdaCube.SystemFw_.Lifter   , module LambdaCube.SystemFw_.Normalizer   , module LambdaCube.SystemFw_.Parser@@ -13,6 +14,7 @@ import LambdaCube.SystemFw_.Ast  import LambdaCube.SystemFw_.Elaborator+import LambdaCube.SystemFw_.Evaluator import LambdaCube.SystemFw_.Lifter import LambdaCube.SystemFw_.Normalizer import LambdaCube.SystemFw_.Parser
src/LambdaCube/SystemFw_/Ast.hs view
@@ -4,12 +4,13 @@ import           Data.Text                  (Text) import           Language.Haskell.TH.Syntax (Lift) -data ExtLCKind-  = ExtLCStar-  | ExtLCKArr ExtLCKind ExtLCKind-  | ExtLCMKVar String+data ExtLCTerm+  = ExtLCVar Text+  | ExtLCLam Text ExtLCType ExtLCTerm+  | ExtLCApp ExtLCTerm ExtLCTerm+  | ExtLCMVar String   deriving stock (Eq, Show, Data, Lift)-infixr 5 `ExtLCKArr`+infixl 6 `ExtLCApp`  data ExtLCType   = ExtLCBase@@ -22,19 +23,19 @@ infixr 5 `ExtLCArr` infixl 6 `ExtLCTTApp` -data ExtLCTerm-  = ExtLCVar Text-  | ExtLCLam Text ExtLCType ExtLCTerm-  | ExtLCApp ExtLCTerm ExtLCTerm-  | ExtLCMVar String+data ExtLCKind+  = ExtLCStar+  | ExtLCKArr ExtLCKind ExtLCKind+  | ExtLCMKVar String   deriving stock (Eq, Show, Data, Lift)-infixl 6 `ExtLCApp`+infixr 5 `ExtLCKArr` -data LCKind-  = LCStar-  | LCKArr LCKind LCKind+data LCTerm+  = LCVar Int+  | LCLam LCType LCTerm+  | LCApp LCTerm LCTerm   deriving stock (Eq, Show, Data, Lift)-infixr 5 `LCKArr`+infixl 6 `LCApp`  data LCType   = LCBase@@ -46,12 +47,11 @@ infixr 5 `LCArr` infixl 6 `LCTTApp` -data LCTerm-  = LCVar Int-  | LCLam LCType LCTerm-  | LCApp LCTerm LCTerm+data LCKind+  = LCStar+  | LCKArr LCKind LCKind   deriving stock (Eq, Show, Data, Lift)-infixl 6 `LCApp`+infixr 5 `LCKArr`  data LCValue   = LCValLam LCType LCTerm
src/LambdaCube/SystemFw_/Elaborator.hs view
@@ -1,4 +1,8 @@-module LambdaCube.SystemFw_.Elaborator where+module LambdaCube.SystemFw_.Elaborator+  ( elaborate+  , elaborateType+  , elaborateKind+  ) where  import           Data.List                (elemIndex) import qualified Data.Text                as Text@@ -20,13 +24,13 @@ elaborateType = go []   where     go _ ExtLCBase = LCBase-    go l (ExtLCTVar x)-      | Just n <- x `elemIndex` l+    go l (ExtLCTVar p)+      | Just n <- p `elemIndex` l       = LCTVar n       | otherwise-      = error $ "Type variable " <> Text.unpack x <> " is not in scope"+      = error $ "Type variable " <> Text.unpack p <> " is not in scope"     go l (ExtLCArr a b) = go l a `LCArr` go l b-    go l (ExtLCTTLam x k b) = LCTTLam (elaborateKind k) $ go (x : l) b+    go l (ExtLCTTLam p k b) = LCTTLam (elaborateKind k) $ go (p : l) b     go l (ExtLCTTApp f a) = go l f `LCTTApp` go l a     go _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
src/LambdaCube/SystemFw_/Evaluator.hs view
@@ -1,4 +1,6 @@-module LambdaCube.SystemFw_.Evaluator where+module LambdaCube.SystemFw_.Evaluator+  ( evaluate+  ) where  import           LambdaCube.SystemFw_.Ast import           LambdaCube.SystemFw_.Substitution@@ -11,6 +13,6 @@     go (LCApp f a)       | LCValLam _ b <- go f       , v <- go a-      = go (substituteValue 0 v b)+      = go $ substituteValue v 0 b       | otherwise       = error "Did you really type check this?"
src/LambdaCube/SystemFw_/Lifter.hs view
@@ -1,14 +1,17 @@-module LambdaCube.SystemFw_.Lifter where+module LambdaCube.SystemFw_.Lifter+  ( liftLCValue+  , liftLCNormal+  ) where -import LambdaCube.SystemFw_.Ast+import           LambdaCube.SystemFw_.Ast  liftLCValue :: LCValue -> LCTerm liftLCValue (LCValLam t b) = LCLam t b  liftLCNormal :: LCNormalTerm -> LCTerm-liftLCNormal (LCNormLam t b)  = LCLam t $ liftLCNormal b-liftLCNormal (LCNormNeut nt)  = liftLCNeutral nt+liftLCNormal (LCNormLam t b) = LCLam t $ liftLCNormal b+liftLCNormal (LCNormNeut nt) = liftLCNeutral nt  liftLCNeutral :: LCNeutralTerm -> LCTerm-liftLCNeutral (LCNeutVar n)    = LCVar n-liftLCNeutral (LCNeutApp f a)  = liftLCNeutral f `LCApp` liftLCNormal a+liftLCNeutral (LCNeutVar x)   = LCVar x+liftLCNeutral (LCNeutApp f a) = liftLCNeutral f `LCApp` liftLCNormal a
src/LambdaCube/SystemFw_/Normalizer.hs view
@@ -1,4 +1,6 @@-module LambdaCube.SystemFw_.Normalizer where+module LambdaCube.SystemFw_.Normalizer+  ( normalize+  ) where  import           LambdaCube.SystemFw_.Ast import           LambdaCube.SystemFw_.Substitution@@ -7,11 +9,11 @@ normalize :: LCTerm -> LCNormalTerm normalize = go   where-    go (LCVar n) = LCNormNeut $ LCNeutVar n+    go (LCVar x) = LCNormNeut $ LCNeutVar x     go (LCLam t b) = LCNormLam (reduceType t) $ go b     go (LCApp f a) =       case go f of-        LCNormLam _ b   -> substituteNormalInNormal 0 a' b-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'+        LCNormLam _ b -> substituteNormalInNormal a' 0 b+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'       where         a' = go a
src/LambdaCube/SystemFw_/Parser.hs view
@@ -1,4 +1,8 @@-module LambdaCube.SystemFw_.Parser where+module LambdaCube.SystemFw_.Parser+  ( pTopTerm+  , pTopType+  , pTopKind+  ) where  import           Data.Foldable            (Foldable (foldl')) import           Data.Functor             (($>))@@ -7,24 +11,24 @@ import           LambdaCube.SystemFw_.Ast import           Text.Megaparsec -pTopLC :: Parser ExtLCTerm-pTopLC = topParser pLC+pTopTerm :: Parser ExtLCTerm+pTopTerm = topParser pTerm -pLC :: Parser ExtLCTerm-pLC = pLam <|> pApp+pTerm :: Parser ExtLCTerm+pTerm = pLam <|> pApp  pLam :: Parser ExtLCTerm pLam =   ExtLCLam   <$> (backslash *> identifier)   <*> (colon *> pType)-  <*> (dot *> pLC)+  <*> (dot *> pTerm)  pApp :: Parser ExtLCTerm pApp = foldl' ExtLCApp <$> pATerm <*> many pATerm  pATerm :: Parser ExtLCTerm-pATerm = pVar <|> pMVar <|> parenthesized pLC+pATerm = pVar <|> pMVar <|> parenthesized pTerm  pVar :: Parser ExtLCTerm pVar = ExtLCVar <$> identifier@@ -32,6 +36,9 @@ pMVar :: Parser ExtLCTerm pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier) +pTopType :: Parser ExtLCType+pTopType = topParser pType+ pType :: Parser ExtLCType pType = pTTLam <|> pArr @@ -59,6 +66,9 @@  pMTVar :: Parser ExtLCType pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)++pTopKind :: Parser ExtLCKind+pTopKind = topParser pKind  pKind :: Parser ExtLCKind pKind = foldr1 ExtLCKArr <$> sepBy1 pAKind rightArrow
src/LambdaCube/SystemFw_/PrettyPrinter.hs view
@@ -2,44 +2,60 @@   TODO: Use real pretty printer library -} {-# LANGUAGE OverloadedStrings #-}-module LambdaCube.SystemFw_.PrettyPrinter where+module LambdaCube.SystemFw_.PrettyPrinter+  ( prettyUnnamedTerm+  , prettyShowUnnamedTerm+  , prettyUnnamedType+  , prettyShowUnnamedType+  , prettyUnnamedKind+  , prettyShowUnnamedKind+  ) where  import           Data.Text                       (Text) import qualified Data.Text                       as Text import           LambdaCube.Common.PrettyPrinter import           LambdaCube.SystemFw_.Ast -prettyUnnamedKind :: LCKind -> Text-prettyUnnamedKind = prettyUnnamedKindPrec 0+prettyUnnamedTerm :: LCTerm -> Text+prettyUnnamedTerm = prettyUnnamedTermPrec 0 +prettyShowUnnamedTerm :: LCTerm -> String+prettyShowUnnamedTerm = Text.unpack . prettyUnnamedTerm+ prettyUnnamedType :: LCType -> Text prettyUnnamedType = prettyUnnamedTypePrec 0 -prettyUnnamedTerm :: LCTerm -> Text-prettyUnnamedTerm = prettyUnnamedTermPrec 0+prettyShowUnnamedType :: LCType -> String+prettyShowUnnamedType = Text.unpack . prettyUnnamedType -prettyUnnamedKindPrec :: Int -> LCKind -> Text-prettyUnnamedKindPrec = go+prettyUnnamedKind :: LCKind -> Text+prettyUnnamedKind = prettyUnnamedKindPrec 0++prettyShowUnnamedKind :: LCKind -> String+prettyShowUnnamedKind = Text.unpack . prettyUnnamedKind++prettyUnnamedTermPrec :: Int -> LCTerm -> Text+prettyUnnamedTermPrec = go   where-    go _ LCStar       = "*"-    go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]+    pTP = prettyUnnamedTypePrec +    go _ (LCVar x)   = Text.pack $ show x+    go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]+    go p (LCApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]+ prettyUnnamedTypePrec :: Int -> LCType -> Text prettyUnnamedTypePrec = go   where     pKP = prettyUnnamedKindPrec      go _ LCBase        = "#"-    go _ (LCTVar i)    = Text.pack $ show i+    go _ (LCTVar p)    = Text.pack $ show p     go p (LCArr a b)   = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]     go p (LCTTLam k b) = wrapIfSpaced (p > 0) ["\\ :", pKP 0 k, ".", go 0 b]     go p (LCTTApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a] -prettyUnnamedTermPrec :: Int -> LCTerm -> Text-prettyUnnamedTermPrec = go+prettyUnnamedKindPrec :: Int -> LCKind -> Text+prettyUnnamedKindPrec = go   where-    pTP = prettyUnnamedTypePrec--    go _ (LCVar i)   = Text.pack $ show i-    go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]-    go p (LCApp f a) = wrapIfSpaced (p > 1) [go 1 f, go 2 a]+    go _ LCStar       = "*"+    go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b]
src/LambdaCube/SystemFw_/Substitution.hs view
@@ -1,37 +1,94 @@-module LambdaCube.SystemFw_.Substitution where+{-# LANGUAGE ViewPatterns #-}+module LambdaCube.SystemFw_.Substitution+  ( substituteTypeInType+  , substituteValue+  , substituteNormalInNormal+  ) where  import           LambdaCube.SystemFw_.Ast import           LambdaCube.SystemFw_.Lifter -substituteTypeInType :: Int -> LCType -> LCType -> LCType-substituteTypeInType n v = go n+substituteTypeInType :: LCType -> Int -> LCType -> LCType+substituteTypeInType v = substDefTypeInType (v, 0)++substituteValue :: LCValue -> Int -> LCTerm -> LCTerm+substituteValue v = substDefValue (v, 0)++substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm+substituteNormalInNormal v = substDefNormalInNormal (v, 0)++substDefTypeInType :: (LCType, Int) -> Int -> LCType -> LCType+substDefTypeInType = go   where+    go _      _ LCBase                     = LCBase+    go dv     p (LCTVar ((== p) -> True))  = shiftType dv+    go _      p e@(LCTVar ((< p) -> True)) = e+    go _      _ (LCTVar q)                 = LCTVar $ q - 1+    go dv     p (LCArr a b)                = go dv p a `LCArr` go dv p b+    go (v, r) p (LCTTLam k b)              = LCTTLam k $ go (v, r + 1) (p + 1) b+    go dv     p (LCTTApp f a)              = go dv p f `LCTTApp` go dv p a++substDefValue :: (LCValue, Int) -> Int -> LCTerm -> LCTerm+substDefValue = go+  where+    go dv     x (LCVar ((== x) -> True))  = shiftValue dv+    go _      x e@(LCVar ((< x) -> True)) = e+    go _      _ (LCVar y)                 = LCVar $ y - 1+    go (v, s) x (LCLam t b)               = LCLam t $ go (v, s + 1) (x + 1) b+    go dv     x (LCApp f a)               = go dv x f `LCApp` go dv x a++substDefNormalInNormal :: (LCNormalTerm, Int) -> Int -> LCNormalTerm -> LCNormalTerm+substDefNormalInNormal = go+  where+    go (v, s) x (LCNormLam t b) = LCNormLam t $ go (v, s + 1) (x + 1) b+    go dv     x (LCNormNeut nt) = substDefNormalInNeutral dv x nt++substDefNormalInNeutral :: (LCNormalTerm, Int) -> Int -> LCNeutralTerm -> LCNormalTerm+substDefNormalInNeutral dv x = go+  where+    go (LCNeutVar ((== x) -> True)) = shiftNormal dv+    go e@(LCNeutVar ((< x) -> True)) = LCNormNeut e+    go (LCNeutVar y) = LCNormNeut . LCNeutVar $ y - 1+    go (LCNeutApp f a) =+      case go f of+        LCNormLam _ b -> substituteNormalInNormal a' 0 b+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'+      where+        a' = substDefNormalInNormal dv x a++shift :: (LCTerm, Int) -> LCTerm+shift (v, s) = go 0 v+  where+    go n (LCVar x)   = LCVar $ if x < n then x else x + s+    go n (LCLam t b) = LCLam t $ go (n + 1) b+    go n (LCApp f a) = go n f `LCApp` go n a++shiftType :: (LCType, Int) -> LCType+shiftType = shiftTypeMin 0++shiftTypeMin :: Int -> (LCType, Int) -> LCType+shiftTypeMin m' (v, r) = go m' v+  where     go _ LCBase        = LCBase-    go m e@(LCTVar l)  = if m == l then v else e+    go m (LCTVar p)    = LCTVar $ if p < m then p else p + r     go m (LCArr a b)   = go m a `LCArr` go m b     go m (LCTTLam k b) = LCTTLam k $ go (m + 1) b     go m (LCTTApp f a) = go m f `LCTTApp` go m a -substituteValue :: Int -> LCValue -> LCTerm -> LCTerm-substituteValue n v = go n-  where-    go m e@(LCVar l) = if m == l then liftLCValue v else e-    go m (LCLam t b) = LCLam t (go (m + 1) b)-    go m (LCApp f a) = LCApp (go m f) (go m a)+shiftValue :: (LCValue, Int) -> LCTerm+shiftValue (v, s) = shift (liftLCValue v, s) -substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm-substituteNormalInNormal n v = go n+shiftNormal :: (LCNormalTerm, Int) -> LCNormalTerm+shiftNormal = shiftNormalMin 0++shiftNormalMin :: Int -> (LCNormalTerm, Int) -> LCNormalTerm+shiftNormalMin n' (v, s) = go n' v   where-    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b-    go m (LCNormNeut nt) = substituteNormalInNeutral m v nt+    go n (LCNormLam t b) = LCNormLam t $ go (n + 1) b+    go n (LCNormNeut nt) = LCNormNeut $ shiftNeutralMin n (nt, s) -substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm-substituteNormalInNeutral n v = go n+shiftNeutralMin :: Int -> (LCNeutralTerm, Int) -> LCNeutralTerm+shiftNeutralMin n (v, s) = go v   where-    go m e@(LCNeutVar l) = if m == l then v else LCNormNeut e-    go m (LCNeutApp f a) =-      case go m f of-        LCNormLam _ b -> substituteNormalInNormal 0 a' b-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'-      where-        a' = substituteNormalInNormal m v a+    go (LCNeutVar x)   = LCNeutVar $ if x < n then x else x + s+    go (LCNeutApp f a) = go f `LCNeutApp` shiftNormalMin n (a, s)
src/LambdaCube/SystemFw_/TH.hs view
@@ -1,49 +1,86 @@ module LambdaCube.SystemFw_.TH-  ( lc+  ( qTerm+  , qType+  , qKind   ) where  import           Data.Data                   (Data) import           Data.Generics               (extQ)-import           Data.Text                   (Text)-import qualified Data.Text                   as Text+import           LambdaCube.Common.TH import           LambdaCube.SystemFw_.Ast import           LambdaCube.SystemFw_.Parser import           Language.Haskell.TH.Lib     (ExpQ, varE) import           Language.Haskell.TH.Quote   (QuasiQuoter (..))-import           Language.Haskell.TH.Syntax  (Loc (loc_start), dataToExpQ, lift,-                                              location, mkName)-import qualified Text.Megaparsec             as P-import qualified Text.Megaparsec.Error       as PE+import           Language.Haskell.TH.Syntax  (mkName) -lc :: QuasiQuoter-lc =+qTerm :: QuasiQuoter+qTerm =   QuasiQuoter-    { quoteExp = expLc+    { quoteExp = qExpTerm     , quotePat = undefined     , quoteType = undefined     , quoteDec = undefined     } -expLc :: String -> ExpQ-expLc str = do-  l <- location-  case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of-    Right e  -> dataToExpQ converter e-    Left err -> fail $ PE.errorBundlePretty err+qExpTerm :: String -> ExpQ+qExpTerm = qExpBase pTopTerm converter   where     converter :: Data b => b -> Maybe ExpQ     converter =-      const Nothing+      converterBase       `extQ` quotedMVar       `extQ` quotedMTVar       `extQ` quotedMKVar-      `extQ` (Just . lift :: Text -> Maybe ExpQ)      quotedMVar (ExtLCMVar x) = Just . varE $ mkName x     quotedMVar _             = Nothing      quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x     quotedMTVar _              = Nothing++    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x+    quotedMKVar _              = Nothing++qType :: QuasiQuoter+qType =+  QuasiQuoter+    { quoteExp = qExpType+    , quotePat = undefined+    , quoteType = undefined+    , quoteDec = undefined+    }++qExpType :: String -> ExpQ+qExpType = qExpBase pTopType converter+  where+    converter :: Data b => b -> Maybe ExpQ+    converter =+      converterBase+      `extQ` quotedMTVar+      `extQ` quotedMKVar++    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x+    quotedMTVar _              = Nothing++    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x+    quotedMKVar _              = Nothing++qKind :: QuasiQuoter+qKind =+  QuasiQuoter+    { quoteExp = qExpKind+    , quotePat = undefined+    , quoteType = undefined+    , quoteDec = undefined+    }++qExpKind :: String -> ExpQ+qExpKind = qExpBase pTopKind converter+  where+    converter :: Data b => b -> Maybe ExpQ+    converter =+      converterBase+      `extQ` quotedMKVar      quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x     quotedMKVar _              = Nothing
src/LambdaCube/SystemFw_/TypeChecker.hs view
@@ -1,5 +1,10 @@-module LambdaCube.SystemFw_.TypeChecker where+module LambdaCube.SystemFw_.TypeChecker+  ( reduceType +  , infer+  , inferKind+  ) where+ import           Data.List                         (uncons) import           LambdaCube.SystemFw_.Ast import           LambdaCube.SystemFw_.Substitution@@ -14,7 +19,7 @@     go (LCTTApp f a)       | LCTTLam _ b <- go f       , v <- go a-      = go $ substituteTypeInType 0 v b+      = go $ substituteTypeInType v 0 b       | otherwise       = error "Did you really kind check this?"
+ test/LambdaCube/STLCTest.hs view
@@ -0,0 +1,168 @@+{-# LANGUAGE QuasiQuotes #-}+module LambdaCube.STLCTest+  ( tests+  ) where++import qualified Control.Exception+import           Control.Monad              (forM_, void)+import qualified Data.Text                  as Text+import           LambdaCube.STLC+import           LambdaCube.STLCTestExample+import           LambdaCube.TestUtil+import           Test.Hspec+import           Test.Tasty+import           Test.Tasty.Hspec           (testSpec)++newtype TestLCType = TestLCType LCType+  deriving newtype (Eq)++instance Show TestLCType where+  show (TestLCType ty) = Text.unpack $ prettyUnnamedType ty++newtype TestLCTerm = TestLCTerm LCTerm+  deriving newtype (Eq)++instance Show TestLCTerm where+  show (TestLCTerm tm) = Text.unpack $ prettyUnnamedTerm tm++tests :: IO TestTree+tests = testSpec "STLC tests" spec++spec :: Spec+spec = do+  describe "STLC infer" inferSpec+  describe "STLC evaluate" evaluateSpec+  describe "STLC normalize" normalizeSpec++inferSpec :: SpecWith ()+inferSpec = forM_ inferSpecCases $ \(mkTitle, extTm, extTy) -> do+  let+    tm = elaborate extTm+    ty = elaborateType extTy+  it (mkTitle tm ty) $ do+    TestLCType (infer tm) `shouldBe` TestLCType ty++inferSpecCases :: [(LCTerm -> LCType -> String, ExtLCTerm, ExtLCType)]+inferSpecCases =+  [ ( const2 "infer lcBaseId should be lcBaseArr"+    , lcBaseId+    , lcBaseArr+    )+  , ( makeDefaultInferTitle+    , [qTerm| \x : # . $lcBaseArrId $lcBaseId x |]+    , lcBaseArr+    )+  , ( makeDefaultInferTitle+    , [qTerm| \x : $lcBaseArr . \y : $lcBaseArr . \z : # . x (y z) |]+    , [qType| $lcBaseArr -> $lcBaseArr -> $lcBaseArr |]+    )+  , ( makeDefaultInferTitle+    , [qTerm| \abc : # . (\fdd : $lcBaseArr . fdd abc) |]+    , [qType| # -> $lcBaseArr -> # |]+    )+  , ( const2 "infer pcn3 should be pcnTy"+    , lcPCN3+    , lcPCNTy+    )+  , ( const2 "infer lcPCNAdd should be (lcPCNTy -> lcPCNTy -> lcPCNTy)"+    , lcPCNAdd+    , [qType| $lcPCNTy -> $lcPCNTy -> $lcPCNTy |]+    )+  , ( const2 "infer (lcPCNAdd lcPCN1 lcPCN2) should be lcPCNTy"+    , [qTerm| $lcPCNAdd $lcPCN1 $lcPCN2 |]+    , [qType| $lcPCNTy |]+    )+  , ( const2 "infer lcPCNMul should be (lcPCNTy -> lcPCNTy -> lcPCNTy)"+    , lcPCNMul+    , [qType| $lcPCNTy -> $lcPCNTy -> $lcPCNTy |]+    )+  , ( const2 "infer (lcPCNMul lcPCN0) should be (lcPCNTy -> lcPCNTy)"+    , [qTerm| $lcPCNMul $lcPCN0 |]+    , [qType| $lcPCNTy -> $lcPCNTy |]+    )+  ]++evaluateSpec :: SpecWith ()+evaluateSpec = forM_ evaluateSpecCases $ \(mkTitle, extTm, extResTm) -> do+  let+    tm = elaborate extTm+    resTm = elaborate extResTm+  it (mkTitle tm resTm) $ do+    void . Control.Exception.evaluate $ infer tm+    void . Control.Exception.evaluate $ infer resTm+    TestLCTerm (liftLCValue (evaluate tm)) `shouldBe` TestLCTerm (liftLCValue (evaluate resTm))++evaluateSpecCases :: [(LCTerm -> LCTerm -> String, ExtLCTerm, ExtLCTerm)]+evaluateSpecCases =+  [ ( makeDefaultEvaluateTitle+    , [qTerm| (\abc : $lcBaseArr . (\fdd : $lcBaseArr -> $lcBaseArr . fdd abc)) $lcBaseId |]+    , [qTerm| \fdd : $lcBaseArr -> $lcBaseArr . fdd $lcBaseId |]+    )+  , ( const2 "evaluate (lcBaseArrId lcBaseId) should be lcBaseId"+    , [qTerm| $lcBaseArrId $lcBaseId |]+    , lcBaseId+    )+  , ( const2 "evaluate (lcBaseArrId (lcBaseArrId lcBaseId)) should be lcBaseId"+    , [qTerm| $lcBaseArrId ($lcBaseArrId $lcBaseId) |]+    , lcBaseId+    )+  , ( const2 "evaluate (lcPCNAdd lcPCN1 lcPCN2) should be lcPCN3 with unnormalized parts"+    , [qTerm| $lcPCNAdd $lcPCN1 $lcPCN2 |]+    , [qTerm| \s : $lcBaseArr . \z : # . $lcPCN1 s ($lcPCN2 s z) |]+    )+  ]++normalizeSpec :: SpecWith ()+normalizeSpec = forM_ normalizeSpecCases $ \(mkTitle, extTm, extResTm) -> do+  let+    tm = elaborate extTm+    resTm = elaborate extResTm+  it (mkTitle tm resTm) $ do+    void . Control.Exception.evaluate $ infer tm+    void . Control.Exception.evaluate $ infer resTm+    TestLCTerm (liftLCNormal (normalize tm)) `shouldBe` TestLCTerm (liftLCNormal (normalize resTm))++normalizeSpecCases :: [(LCTerm -> LCTerm -> String, ExtLCTerm, ExtLCTerm)]+normalizeSpecCases =+  [ ( makeDefaultNormalizeTitle+    , [qTerm| (\abc : $lcBaseArr . (\fdd : $lcBaseArr -> $lcBaseArr . fdd abc)) $lcBaseId |]+    , [qTerm| \fdd : $lcBaseArr -> $lcBaseArr . fdd $lcBaseId |]+    )+  , ( const2 "normalize (lcBaseArrId lcBaseId) should be lcBaseId"+    , [qTerm| $lcBaseArrId $lcBaseId |]+    , lcBaseId+    )+  , ( const2 "normalize (lcBaseArrId (lcBaseArrId lcBaseId)) should be lcBaseId"+    , [qTerm| $lcBaseArrId ($lcBaseArrId $lcBaseId) |]+    , lcBaseId+    )+  , ( const2 "normalize (lcPCNAdd lcPCN1 lcPCN2) should be lcPCN3"+    , [qTerm| $lcPCNAdd $lcPCN0 $lcPCN1 |]+    , lcPCN1+    )+  , ( const2 "normalize (lcPCN4 lcBaseId) should be lcBaseId"+    , [qTerm| $lcPCN4 $lcBaseId |]+    , lcBaseId+    )+  ]++makeDefaultInferTitle :: LCTerm -> LCType -> String+makeDefaultInferTitle tm ty =+  makeDefaultTitle+  "infer"+  (prettyShowUnnamedTerm tm)+  (prettyShowUnnamedType ty)++makeDefaultEvaluateTitle :: LCTerm -> LCTerm -> String+makeDefaultEvaluateTitle tm resTm =+  makeDefaultTitle+  "evaluate"+  (prettyShowUnnamedTerm tm)+  (prettyShowUnnamedTerm resTm)++makeDefaultNormalizeTitle :: LCTerm -> LCTerm -> String+makeDefaultNormalizeTitle tm resTm =+  makeDefaultTitle+  "normalize"+  (prettyShowUnnamedTerm tm)+  (prettyShowUnnamedTerm resTm)
+ test/LambdaCube/STLCTestExample.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE QuasiQuotes #-}+module LambdaCube.STLCTestExample where++import           LambdaCube.STLC++lcBaseId, lcBaseArrId :: ExtLCTerm+lcBaseId = [qTerm| \x : # . x |]+lcBaseArrId = [qTerm| \x : $lcBaseArr . x |]++lcBaseArr :: ExtLCType+lcBaseArr = [qType| # -> # |]++------------------------------------------------------------+-- Pseudo Church Numeral examples+------------------------------------------------------------++lcPCN0, lcPCN1, lcPCN2, lcPCN3, lcPCN4, lcPCN5 :: ExtLCTerm+lcPCN0 = [qTerm| \s : $lcBaseArr . $lcBaseId |]+lcPCN1 = [qTerm| \s : $lcBaseArr . \z : # . s z |]+lcPCN2 = [qTerm| \s : $lcBaseArr . \z : # . s (s z) |]+lcPCN3 = [qTerm| \s : $lcBaseArr . \z : # . s (s (s z)) |]+lcPCN4 = [qTerm| \s : $lcBaseArr . \z : # . s (s (s (s z))) |]+lcPCN5 = [qTerm| \s : $lcBaseArr . \z : # . s (s (s (s (s z)))) |]++lcPCNAdd, lcPCNMul :: ExtLCTerm+lcPCNAdd =+  [qTerm|+     \n : $lcPCNTy . \m : $lcPCNTy .+     \s : $lcBaseArr . \z : # . n s (m s z)+  |]+lcPCNMul =+  [qTerm|+     \n : $lcPCNTy . \m : $lcPCNTy .+     \s : $lcBaseArr . \z : # . n (m s) z+  |]++lcPCNTy :: ExtLCType+lcPCNTy = [qType| $lcBaseArr -> $lcBaseArr |]
+ test/LambdaCube/SystemFwTest.hs view
@@ -0,0 +1,282 @@+{-# LANGUAGE QuasiQuotes #-}+module LambdaCube.SystemFwTest where++import qualified Control.Exception+import           Control.Monad                  (forM_, void)+import qualified Data.Text                      as Text+import           LambdaCube.SystemFw+import           LambdaCube.SystemFwTestExample+import           LambdaCube.TestUtil+import           Test.Hspec+import           Test.Tasty+import           Test.Tasty.Hspec               (testSpec)++newtype TestLCType = TestLCType LCType+  deriving newtype (Eq)++instance Show TestLCType where+  show (TestLCType ty) = Text.unpack $ prettyUnnamedType ty++newtype TestLCTerm = TestLCTerm LCTerm+  deriving newtype (Eq)++instance Show TestLCTerm where+  show (TestLCTerm tm) = Text.unpack $ prettyUnnamedTerm tm++tests :: IO TestTree+tests = testSpec "SystemFw tests" spec++spec :: Spec+spec = do+  describe "SystemFw infer" inferSpec+  describe "SystemFw evaluate" evaluateSpec+  describe "SystemFw normalize" normalizeSpec++inferSpec :: SpecWith ()+inferSpec = forM_ inferSpecCases $ \(mkTitle, extTm, extTy) -> do+  let+    tm = elaborate extTm+    ty = elaborateType [] extTy+  it (mkTitle tm ty) $ do+    TestLCType (infer tm) `shouldBe` TestLCType (reduceType ty)++inferSpecCases :: [(LCTerm -> LCType -> String, ExtLCTerm, ExtLCType)]+inferSpecCases =+  [ ( const2 "infer lcBaseId should be lcBaseArr"+    , lcBaseId+    , lcBaseArr+    )+  , ( makeDefaultInferTitle+    , [qTerm| \x : # . $lcBaseArrId $lcBaseId x |]+    , lcBaseArr+    )+  , ( makeDefaultInferTitle+    , [qTerm| \x : $lcBaseArr . \y : $lcBaseArr . \z : # . x (y z) |]+    , [qType| $lcBaseArr -> $lcBaseArr -> $lcBaseArr |]+    )+  , ( makeDefaultInferTitle+    , [qTerm| \abc : # . (\fdd : $lcBaseArr . fdd abc) |]+    , [qType| # -> $lcBaseArr -> # |]+    )+  , ( const2 "infer lcId should be (! a : * , a -> a)"+    , lcId+    , [qType| ! a : * , a -> a |]+    )+  , ( const2 "infer pCN3 should be pCNTy"+    , lcCN3+    , lcCNTy+    )+  , ( const2 "infer lcCNSucc should be (lcCNTy -> lcCNTy)"+    , [qTerm| $lcCNSucc |]+    , [qType| $lcCNTy -> $lcCNTy |]+    )+  , ( const2 "infer lcCNAdd should be (lcCNTy -> lcCNTy -> lcCNTy)"+    , lcCNAdd+    , [qType| $lcCNTy -> $lcCNTy -> $lcCNTy |]+    )+  , ( const2 "infer (lcCNAdd lcCN1 lcCN2) should be lcCNTy"+    , [qTerm| $lcCNAdd $lcCN1 $lcCN2 |]+    , [qType| $lcCNTy |]+    )+  , ( const2 "infer lcCNMul should be (lcCNTy -> lcCNTy -> lcCNTy)"+    , lcCNMul+    , [qType| $lcCNTy -> $lcCNTy -> $lcCNTy |]+    )+  , ( const2 "infer (lcCNMul lcCN0) should be (lcCNTy -> lcCNTy)"+    , [qTerm| $lcCNMul $lcCN0 |]+    , [qType| $lcCNTy -> $lcCNTy |]+    )+  , ( const2 "infer lcCNPred should be (lcCNTy -> lcCNTy)"+    , [qTerm| $lcCNPred |]+    , [qType| $lcCNTy -> $lcCNTy |]+    )+  , ( const2 "infer lcCNPredDef should be (lcCNTy -> lcCNTy -> lcCNTy)"+    , [qTerm| $lcCNPredDef |]+    , [qType| $lcCNTy -> $lcCNTy -> $lcCNTy |]+    )+  , ( const2 "infer lcCNMinus should be (lcCNTy -> lcCNTy -> lcCNTy)"+    , [qTerm| $lcCNMinus |]+    , [qType| $lcCNTy -> $lcCNTy -> $lcCNTy |]+    )+  , ( const2 "infer lcCNIs0 should be (lcCNTy -> lcCBTy)"+    , [qTerm| $lcCNIs0 |]+    , [qType| $lcCNTy -> $lcCBTy |]+    )+  , ( const2 "infer lcCLNil should be (!e : * , lcCLTy e)"+    , [qTerm| $lcCLNil |]+    , [qType| !e : * , $lcCLTy e |]+    )+  , ( const2 "infer lcCLCons should be (!e : * , e -> lcCLTy e -> lcCLTy e)"+    , [qTerm| $lcCLCons |]+    , [qType| !e : * , e -> $lcCLTy e -> $lcCLTy e |]+    )+  , ( const2 "infer lcCL_CN_0_1_2 should be (lcCLTy lcCNTy)"+    , [qTerm| $lcCL_CN_0_1_2 |]+    , [qType| $lcCLTy $lcCNTy |]+    )+  , ( const2 "infer lcCLHeadDef should be (!e : * , e -> lcCLTy e -> e)"+    , [qTerm| $lcCLHeadDef |]+    , [qType| !e : * , e -> $lcCLTy e -> e |]+    )+  , ( const2 "infer lcCLTail should be (!e : * , lcCLTy e -> lcCLTy e)"+    , [qTerm| $lcCLTail |]+    , [qType| !e : * , $lcCLTy e -> $lcCLTy e |]+    )+  , ( const2 "infer lcCLTailDef should be (!e : * , lcCLTy e -> lcCLTy e -> lcCLTy e)"+    , [qTerm| $lcCLTailDef |]+    , [qType| !e : * , $lcCLTy e -> $lcCLTy e -> $lcCLTy e |]+    )+  ]++evaluateSpec :: SpecWith ()+evaluateSpec = forM_ evaluateSpecCases $ \(mkTitle, extTm, extResTm) -> do+  let+    tm = elaborate extTm+    resTm = elaborate extResTm+  it (mkTitle tm resTm) $ do+    void . Control.Exception.evaluate $ infer tm+    void . Control.Exception.evaluate $ infer resTm+    TestLCTerm (liftLCValue (evaluate tm)) `shouldBe` TestLCTerm (liftLCValue (evaluate resTm))++evaluateSpecCases :: [(LCTerm -> LCTerm -> String, ExtLCTerm, ExtLCTerm)]+evaluateSpecCases =+  [ ( makeDefaultEvaluateTitle+    , [qTerm| (\abc : $lcBaseArr . (\fdd : $lcBaseArr -> $lcBaseArr . fdd abc)) $lcBaseId |]+    , [qTerm| \fdd : $lcBaseArr -> $lcBaseArr . fdd $lcBaseId |]+    )+  , ( const2 "evaluate (lcBaseArrId lcBaseId) should be lcBaseId"+    , [qTerm| $lcBaseArrId $lcBaseId |]+    , lcBaseId+    )+  , ( const2 "evaluate (lcBaseArrId (lcBaseArrId lcBaseId)) should be lcBaseId"+    , [qTerm| $lcBaseArrId ($lcBaseArrId $lcBaseId) |]+    , lcBaseId+    )+  , ( const2 "evaluate (lcCNAdd lcCN1 lcCN2) should be lcCN3 with unnormalized parts"+    , [qTerm| $lcCNAdd $lcCN1 $lcCN2 |]+    , [qTerm| @\r : * . \s : r -> r . \z : r . $lcCN1 @r s ($lcCN2 @r s z) |]+    )+  , ( const2 "evaluate (lcCNSucc lcCN1) should be lcCN2 with unnormalized parts"+    , [qTerm| $lcCNSucc $lcCN1 |]+    , [qTerm| @\r : * . \s : r -> r . \z : r . s ($lcCN1 @r s z) |]+    )+  , ( const2 "evaluate (lcCNPredDef lcCN5 lcCN1) should be lcCN0"+    , [qTerm| $lcCNPredDef $lcCN5 $lcCN1 |]+    , [qTerm| $lcCN0 |]+    )+  , ( const2 "evaluate (lcCNPredDef lcCN5 lcCN0) should be lcCN5"+    , [qTerm| $lcCNPredDef $lcCN5 $lcCN0 |]+    , [qTerm| $lcCN5 |]+    )+  , ( const2 "evaluate (lcCNIs0 lcCN0) should be lcCBTrue"+    , [qTerm| $lcCNIs0 $lcCN0 |]+    , [qTerm| $lcCBTrue |]+    )+  , ( const2 "evaluate (lcCNIs0 lcCN2) should be lcCBFalse"+    , [qTerm| $lcCNIs0 $lcCN2 |]+    , [qTerm| $lcCBFalse |]+    )+  , ( const2 "evaluate (lcCLHeadDef @lcCNTy lcCN3 lcCL_CN_0_1_2) should be lcCN0"+    , [qTerm| $lcCLHeadDef @$lcCNTy $lcCN3 $lcCL_CN_0_1_2 |]+    , [qTerm| $lcCN0 |]+    )+  , ( const2 "evaluate (lcCLTailDef lcCL_CN_0_1_2 (lcCLTailDef lcCL_CN_0_1_2 lcCL_CN_0)) should be lcCL_CN_0_1_2"+    , [qTerm| $lcCLTailDef @$lcCNTy $lcCL_CN_0_1_2 ($lcCLTailDef @$lcCNTy $lcCL_CN_0_1_2 $lcCL_CN_0) |]+    , [qTerm| $lcCL_CN_0_1_2 |]+    )+  ]++normalizeSpec :: SpecWith ()+normalizeSpec = forM_ normalizeSpecCases $ \(mkTitle, extTm, extResTm) -> do+  let+    tm = elaborate extTm+    resTm = elaborate extResTm+  it (mkTitle tm resTm) $ do+    void . Control.Exception.evaluate $ infer tm+    void . Control.Exception.evaluate $ infer resTm+    TestLCTerm (liftLCNormal (normalize tm)) `shouldBe` TestLCTerm (liftLCNormal (normalize resTm))++normalizeSpecCases :: [(LCTerm -> LCTerm -> String, ExtLCTerm, ExtLCTerm)]+normalizeSpecCases =+  [ ( makeDefaultNormalizeTitle+    , [qTerm| (\abc : $lcBaseArr . (\fdd : $lcBaseArr -> $lcBaseArr . fdd abc)) $lcBaseId |]+    , [qTerm| \fdd : $lcBaseArr -> $lcBaseArr . fdd $lcBaseId |]+    )+  , ( const2 "normalize (lcBaseArrId lcBaseId) should be lcBaseId"+    , [qTerm| $lcBaseArrId $lcBaseId |]+    , lcBaseId+    )+  , ( const2 "normalize (lcBaseArrId (lcBaseArrId lcBaseId)) should be lcBaseId"+    , [qTerm| $lcBaseArrId ($lcBaseArrId $lcBaseId) |]+    , lcBaseId+    )+  , ( const2 "normalize (lcCNAdd lcCN1 lcCN2) should be lcCN3"+    , [qTerm| $lcCNAdd $lcCN0 $lcCN1 |]+    , lcCN1+    )+  , ( const2 "normalize (lcCN4 lcBaseId) should be lcBaseId"+    , [qTerm| $lcCN4 @# $lcBaseId |]+    , lcBaseId+    )+  , ( const2 "normalize (lcCNPred lcCN4) should be lcCN3"+    , [qTerm| $lcCNPred $lcCN4 |]+    , lcCN3+    )+  , ( const2 "normalize (lcCNMinus lcCN5 lcCN3) should be lcCN2"+    , [qTerm| $lcCNMinus $lcCN5 $lcCN3 |]+    , lcCN2+    )+  , ( const2 "normalize (lcCNIs0 lcCN0) should be lcCBTrue"+    , [qTerm| $lcCNIs0 $lcCN0 |]+    , [qTerm| $lcCBTrue |]+    )+  , ( const2 "normalize (lcCNIs0 lcCN2) should be lcCBFalse"+    , [qTerm| $lcCNIs0 $lcCN2 |]+    , [qTerm| $lcCBFalse |]+    )+  , ( const2 "normalize (lcCLHeadDef lcCN3 lcCL_CN_0_1_2) should be lcCN0"+    , [qTerm| $lcCLHeadDef @$lcCNTy $lcCN3 $lcCL_CN_0_1_2 |]+    , [qTerm| $lcCN0 |]+    )+  , ( const2 "normalize (lcCLHeadDef lcCN3 (lcCLTail lcCL_CN_0_1_2)) should be lcCN1"+    , [qTerm| $lcCLHeadDef @$lcCNTy $lcCN3 ($lcCLTail @$lcCNTy $lcCL_CN_0_1_2) |]+    , [qTerm| $lcCN1 |]+    )+  , ( const2 "normalize (lcCLHeadDef lcCN3 (lcCLTail (lcCLTail lcCL_CN_0_1_2))) should be lcCN2"+    , [qTerm| $lcCLHeadDef @$lcCNTy $lcCN3 ($lcCLTail @$lcCNTy ($lcCLTail @$lcCNTy $lcCL_CN_0_1_2)) |]+    , [qTerm| $lcCN2 |]+    )+  , ( const2 "normalize (lcCLTail (lcCLTail (lcCLTail lcCL_CN_0_1_2))) should be lcCLNil"+    , [qTerm| $lcCLTail @$lcCNTy ($lcCLTail @$lcCNTy ($lcCLTail @$lcCNTy $lcCL_CN_0_1_2)) |]+    , [qTerm| $lcCLNil @$lcCNTy |]+    )+  , ( const2 "normalize (lcCLTailDef lcCL_CN_0_1_2 lcCL_CN_0) should be lcCLNil"+    , [qTerm| $lcCLTailDef @$lcCNTy $lcCL_CN_0_1_2 $lcCL_CN_0 |]+    , [qTerm| $lcCLNil @$lcCNTy |]+    )+  , ( const2 "normalize (lcCLTailDef lcCL_CN_0_1_2 (lcCLTailDef lcCL_CN_0_1_2 lcCL_CN_0)) should be lcCL_CN_0_1_2"+    , [qTerm| $lcCLTailDef @$lcCNTy $lcCL_CN_0_1_2 ($lcCLTailDef @$lcCNTy $lcCL_CN_0_1_2 $lcCL_CN_0) |]+    , [qTerm| $lcCL_CN_0_1_2 |]+    )+  ]++makeDefaultInferTitle :: LCTerm -> LCType -> String+makeDefaultInferTitle tm ty =+  makeDefaultTitle+  "infer"+  (prettyShowUnnamedTerm tm)+  (prettyShowUnnamedType ty)++makeDefaultEvaluateTitle :: LCTerm -> LCTerm -> String+makeDefaultEvaluateTitle tm resTm =+  makeDefaultTitle+  "evaluate"+  (prettyShowUnnamedTerm tm)+  (prettyShowUnnamedTerm resTm)++makeDefaultNormalizeTitle :: LCTerm -> LCTerm -> String+makeDefaultNormalizeTitle tm resTm =+  makeDefaultTitle+  "normalize"+  (prettyShowUnnamedTerm tm)+  (prettyShowUnnamedTerm resTm)
+ test/LambdaCube/SystemFwTestExample.hs view
@@ -0,0 +1,184 @@+{-# LANGUAGE QuasiQuotes #-}+module LambdaCube.SystemFwTestExample where++import           LambdaCube.SystemFw++lcBaseId, lcBaseArrId :: ExtLCTerm+lcBaseId = [qTerm| \x : # . x |]+lcBaseArrId = [qTerm| \x : $lcBaseArr . x |]++lcBaseArr :: ExtLCType+lcBaseArr = [qType| # -> # |]++lcId :: ExtLCTerm+lcId = [qTerm| @\a : * . \x : a . x |]++------------------------------------------------------------+-- Church Pair examples+------------------------------------------------------------++lcCPPair :: ExtLCTerm+lcCPPair = [qTerm| @\a : * . @\b : * . \x : a . \y : b . @\r : * . \f : a -> b -> r . f x y |]++lcCPFst :: ExtLCTerm+lcCPFst = [qTerm| @\a : * . @\b : * . \p : $lcCPTy a b . p @a (\x : a . \y : b . x) |]++lcCPSnd :: ExtLCTerm+lcCPSnd = [qTerm| @\a : * . @\b : * . \p : $lcCPTy a b . p @b (\x : a . \y : b . y) |]++lcCPTy :: ExtLCType+lcCPTy = [qType| \a : * . \b : * . !r : * , (a -> b -> r) -> r |]++------------------------------------------------------------+-- Church Boolean examples+------------------------------------------------------------++lcCBTrue, lcCBFalse :: ExtLCTerm+lcCBTrue = [qTerm| @\r : * . \t : r . \f : r . t |]+lcCBFalse = [qTerm| @\r : * . \t : r . \f : r . f |]++lcCBIf :: ExtLCTerm+lcCBIf = [qTerm| \b : $lcCBTy . b |]++lcCBAnd, lcCBOr :: ExtLCTerm+lcCBAnd = [qTerm| \b1 : $lcCBTy . \b2 : $lcCBTy . @\r : * . \t : r . \f : r . b1 @r (b2 @r t f) f |]+lcCBOr = [qTerm| \b1 : $lcCBTy . \b2 : $lcCBTy . @\r : * . \t : r . \f : r . b1 @r t (b2 @r t f) |]++lcCBNot :: ExtLCTerm+lcCBNot = [qTerm| \b : $lcCBTy . @\r : * . \t : r . \f : r . b @r f t |]++lcCBTy :: ExtLCType+lcCBTy = [qType| !r : * , r -> r -> r |]++------------------------------------------------------------+-- Church Numeral examples+------------------------------------------------------------++lcCN1, lcCN2, lcCN3, lcCN4, lcCN5 :: ExtLCTerm+lcCN1 = [qTerm| @\r : * . \s : r -> r . \z : r . s z |]+lcCN2 = [qTerm| @\r : * . \s : r -> r . \z : r . s (s z) |]+lcCN3 = [qTerm| @\r : * . \s : r -> r . \z : r . s (s (s z)) |]+lcCN4 = [qTerm| @\r : * . \s : r -> r . \z : r . s (s (s (s z))) |]+lcCN5 = [qTerm| @\r : * . \s : r -> r . \z : r . s (s (s (s (s z)))) |]++lcCN0, lcCNSucc :: ExtLCTerm+lcCN0 = [qTerm| @\r : * . \s : r -> r . \z : r . z |]+lcCNSucc = [qTerm| \n : $lcCNTy . @\r : * . \s : r -> r . \z : r . s (n @r s z) |]++lcCNPred, lcCNPredDef :: ExtLCTerm+lcCNPred =+  [qTerm|+     \n : $lcCNTy .+     @\r : * . \s : r -> r . \z : r .+     n+     @((r -> r) -> r)+     (\p : (r -> r) -> r . \g : r -> r . g (p s))+     (\p : r -> r . z)+     (\p : r . p)+  |]+lcCNPredDef =+  [qTerm|+     \d : $lcCNTy .+     \n : $lcCNTy .+     n+     @(($lcCNTy -> $lcCNTy -> $lcCNTy) -> $lcCNTy)+     (\p : ($lcCNTy -> $lcCNTy -> $lcCNTy) -> $lcCNTy .+      \g : $lcCNTy -> $lcCNTy -> $lcCNTy .+      (\x : $lcCNTy . g ($lcCNSucc x) x) (p (\x : $lcCNTy . \y : $lcCNTy . x)))+     (\g : $lcCNTy -> $lcCNTy -> $lcCNTy . g $lcCN0 d)+     (\x : $lcCNTy . \y : $lcCNTy . y)+  |]++lcCNAdd, lcCNMul, lcCNMinus :: ExtLCTerm+lcCNAdd =+  [qTerm|+     \n : $lcCNTy . \m : $lcCNTy .+     @\r : * . \s : r -> r . \z : r . n @r s (m @r s z)+  |]+lcCNMul =+  [qTerm|+     \n : $lcCNTy . \m : $lcCNTy .+     @\r : * . \s : r -> r . \z : r . n @r (m @r s) z+  |]+lcCNMinus =+  [qTerm|+     \n : $lcCNTy . \m : $lcCNTy . m @$lcCNTy $lcCNPred n+  |]++lcCNIs0 :: ExtLCTerm+lcCNIs0 =+  [qTerm|+     \n : $lcCNTy . n @$lcCBTy (\x : $lcCBTy . $lcCBFalse) $lcCBTrue+  |]++lcCNTy :: ExtLCType+lcCNTy = [qType| !r : * , (r -> r) -> r -> r |]++------------------------------------------------------------+-- Church List examples+------------------------------------------------------------++lcCL_CN_0, lcCL_CN_0_1, lcCL_CN_0_1_2 :: ExtLCTerm+lcCL_CN_0 =+  [qTerm|+    $lcCLCons @$lcCNTy $lcCN0+    ($lcCLNil @$lcCNTy)+  |]+lcCL_CN_0_1 =+  [qTerm|+    $lcCLCons @$lcCNTy $lcCN0+    ($lcCLCons @$lcCNTy $lcCN1+    ($lcCLNil @$lcCNTy))+  |]+lcCL_CN_0_1_2 =+  [qTerm|+    $lcCLCons @$lcCNTy $lcCN0+    ($lcCLCons @$lcCNTy $lcCN1+    ($lcCLCons @$lcCNTy $lcCN2+    ($lcCLNil @$lcCNTy)))+  |]++lcCLNil, lcCLCons :: ExtLCTerm+lcCLNil = [qTerm| @\e : * . @\r : * . \c : e -> r -> r . \n : r . n |]+lcCLCons =+  [qTerm|+    @\e : * .+    \h : e . \t : $lcCLTy e .+    @\r : * . \c : e -> r -> r . \n : r . c h (t @r c n)+  |]++lcCLLength :: ExtLCTerm+lcCLLength = [qTerm| @\e : * . \l : $lcCLTy e . l @$lcCNTy (\h : e . \t : $lcCNTy . $lcCNSucc t) $lcCN0 |]++lcCLHeadDef :: ExtLCTerm+lcCLHeadDef = [qTerm| @\e : * . \d : e . \l : $lcCLTy e . l @e (\h : e . \t : e . h) d |]++lcCLTail, lcCLTailDef :: ExtLCTerm+lcCLTail =+  [qTerm|+    @\e : * .+    \l : $lcCLTy e .+    @\r : * . \c : e -> r -> r . \n : r .+    l+    @((e -> r -> r) -> r)+    (\h : e . \t : (e -> r -> r) -> r . \g : e -> r -> r . g h (t c))+    (\t : e -> r -> r . n)+    (\h : e . \t : r . t)+  |]+lcCLTailDef =+  [qTerm|+    @\e : * .+    \d : $lcCLTy e .+    \l : $lcCLTy e .+    l+    @(($lcCLTy e -> $lcCLTy e -> $lcCLTy e) -> $lcCLTy e)+    (\h : e .+     \t : ($lcCLTy e -> $lcCLTy e -> $lcCLTy e) -> $lcCLTy e .+     \g : $lcCLTy e -> $lcCLTy e -> $lcCLTy e .+     (\x : $lcCLTy e . g ($lcCLCons @e h x) x) (t (\x : $lcCLTy e . \y : $lcCLTy e . x)))+    (\g : $lcCLTy e -> $lcCLTy e -> $lcCLTy e . g ($lcCLNil @e) d)+    (\x : $lcCLTy e . \y : $lcCLTy e . y)+  |]++lcCLTy :: ExtLCType+lcCLTy = [qType| \e : * . !r : * , (e -> r -> r) -> r -> r |]
+ test/LambdaCube/TestUtil.hs view
@@ -0,0 +1,15 @@+module LambdaCube.TestUtil where++const2 :: a -> b -> c -> a+const2 x _ _ = x++makeDefaultTitle :: String -> String -> String -> String+makeDefaultTitle fName left right =+  concat+  [ fName+  , " ("+  , left+  , ") should be ("+  , right+  , ")"+  ]
− test/Spec.hs 
@@ -1,1 +0,0 @@-{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
+ test/Test.hs view
@@ -0,0 +1,16 @@+module Main+  ( main+  ) where++import qualified LambdaCube.STLCTest     as STLC+import qualified LambdaCube.SystemFwTest as SystemFw+import           Test.Tasty++main :: IO ()+main = do+  testsForSTLC <- STLC.tests+  testsForSystemFw <- SystemFw.tests+  defaultMain $ testGroup "tests"+    [ testsForSTLC+    , testsForSystemFw+    ]