packages feed

lambda-cube 0.1.0.0 → 0.2.0.0

raw patch · 47 files changed

+925/−584 lines, 47 filesdep +syb

Dependencies added: syb

Files

+ CHANGELOG.md view
@@ -0,0 +1,27 @@+# 0.2.0.0++## Main updates++- New top-level module for each lambda calculus is added.  +  It make easier to use one specific lambda calculus under a qualified name.+- Quasiquoter now supports splicing-in.+- Change the type of elaborator and type checker for composability.  +  Currently they are less type-safe. However, monad to make them type-safe will be added in the future.++## 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.++# 0.1.0.0++The first release including support for following 4 lambda calculi.++- Simply Typed Lambda Calculus+- System F+- System F omega underbar+- System F omega
lambda-cube.cabal view
@@ -5,16 +5,17 @@ -- see: https://github.com/sol/hpack  name:           lambda-cube-version:        0.1.0.0+version:        0.2.0.0 synopsis:       Haskell implementation of (some of) lambda cube calculi description:    Haskell implementation of the following 4 lambda calculi:+                .                 1. Simply typed lambda calculus                 2. System F                 3. System F omega underbar                 4. System F omega category:       Utilities-homepage:       https://github.com/Ailrun/LambdaCube#readme-bug-reports:    https://github.com/Ailrun/LambdaCube/issues+homepage:       https://github.com/Ailrun/lambda-cube#readme+bug-reports:    https://github.com/Ailrun/lambda-cube/issues author:         Junyoung Clare Jang maintainer:     jjc9310@gmail.com copyright:      2021 Junyoung Clare Jang@@ -22,46 +23,59 @@ license-file:   LICENSE build-type:     Simple extra-source-files:+    CHANGELOG.md     README.md  source-repository head   type: git-  location: https://github.com/Ailrun/LambdaCube+  location: https://github.com/Ailrun/lambda-cube  library   exposed-modules:       LambdaCube.Common.Parser       LambdaCube.Common.PrettyPrinter+      LambdaCube.STLC       LambdaCube.STLC.Ast       LambdaCube.STLC.Elaborator       LambdaCube.STLC.Evaluator+      LambdaCube.STLC.Lifter       LambdaCube.STLC.Normalizer       LambdaCube.STLC.Parser       LambdaCube.STLC.PrettyPrinter+      LambdaCube.STLC.Substitution       LambdaCube.STLC.TH       LambdaCube.STLC.TypeChecker+      LambdaCube.SystemF       LambdaCube.SystemF.Ast       LambdaCube.SystemF.Elaborator       LambdaCube.SystemF.Evaluator+      LambdaCube.SystemF.Lifter       LambdaCube.SystemF.Normalizer       LambdaCube.SystemF.Parser       LambdaCube.SystemF.PrettyPrinter+      LambdaCube.SystemF.Substitution       LambdaCube.SystemF.TH       LambdaCube.SystemF.TypeChecker+      LambdaCube.SystemFw       LambdaCube.SystemFw.Ast       LambdaCube.SystemFw.Elaborator       LambdaCube.SystemFw.Evaluator+      LambdaCube.SystemFw.Lifter       LambdaCube.SystemFw.Normalizer       LambdaCube.SystemFw.Parser       LambdaCube.SystemFw.PrettyPrinter+      LambdaCube.SystemFw.Substitution       LambdaCube.SystemFw.TH       LambdaCube.SystemFw.TypeChecker+      LambdaCube.SystemFw_       LambdaCube.SystemFw_.Ast       LambdaCube.SystemFw_.Elaborator       LambdaCube.SystemFw_.Evaluator+      LambdaCube.SystemFw_.Lifter       LambdaCube.SystemFw_.Normalizer       LambdaCube.SystemFw_.Parser       LambdaCube.SystemFw_.PrettyPrinter+      LambdaCube.SystemFw_.Substitution       LambdaCube.SystemFw_.TH       LambdaCube.SystemFw_.TypeChecker   other-modules:@@ -116,8 +130,9 @@   build-depends:       base >=4.12 && <5     , megaparsec >=9.0.1 && <9.1+    , syb     , template-haskell-    , text+    , text >=1.2.4.0   default-language: Haskell2010  test-suite lambda-cube-test
src/LambdaCube/Common/Parser.hs view
@@ -21,7 +21,7 @@ rightArrow = lex $ string "->" atsignBackslash = lex $ string "@\\" -backslash, atsign, sharp, colon, dot, openParenthesis, closeParenthesis, exclamationMark, comma, asterisk :: Parser Char+backslash, atsign, sharp, colon, dot, openParenthesis, closeParenthesis, exclamationMark, comma, asterisk, dollarsign :: Parser Char backslash        = lex $ char '\\' atsign           = lex $ char '@' sharp            = lex $ char '#'@@ -32,6 +32,7 @@ exclamationMark  = lex $ char '!' comma            = lex $ char ',' asterisk         = lex $ char '*'+dollarsign       = lex $ char '$'  identifier :: Parser Text identifier = lex $ (Text.pack .) . (:) <$> letterChar <*> many alphaNumChar
+ src/LambdaCube/STLC.hs view
@@ -0,0 +1,22 @@+module LambdaCube.STLC+  ( module LambdaCube.STLC.Ast+  , module LambdaCube.STLC.Elaborator+  , module LambdaCube.STLC.Lifter+  , module LambdaCube.STLC.Normalizer+  , module LambdaCube.STLC.Parser+  , module LambdaCube.STLC.PrettyPrinter+  , module LambdaCube.STLC.Substitution+  , module LambdaCube.STLC.TH+  , module LambdaCube.STLC.TypeChecker+  ) where++import LambdaCube.STLC.Ast++import LambdaCube.STLC.Elaborator+import LambdaCube.STLC.Lifter+import LambdaCube.STLC.Normalizer+import LambdaCube.STLC.Parser+import LambdaCube.STLC.PrettyPrinter+import LambdaCube.STLC.Substitution+import LambdaCube.STLC.TH+import LambdaCube.STLC.TypeChecker
src/LambdaCube/STLC/Ast.hs view
@@ -1,39 +1,48 @@ module LambdaCube.STLC.Ast where +import           Data.Data                  (Data) 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 LCType ExtLCTerm+  | ExtLCLam Text ExtLCType ExtLCTerm   | ExtLCApp ExtLCTerm ExtLCTerm-  deriving stock (Eq, Show, Lift)+  | ExtLCMVar String+  deriving stock (Eq, Show, Data, Lift) infixl 6 `ExtLCApp`  data LCType   = LCBase   | LCArr LCType LCType-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixr 5 `LCArr`  data LCTerm   = LCVar Int   | LCLam LCType LCTerm   | LCApp LCTerm LCTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixl 6 `LCApp`  data LCValue   = LCValLam LCType LCTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift)  data LCNormalTerm   = LCNormLam LCType LCNormalTerm   | LCNormNeut LCNeutralTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift)  data LCNeutralTerm   = LCNeutVar Int   | LCNeutApp LCNeutralTerm LCNormalTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixl 6 `LCNeutApp`
src/LambdaCube/STLC/Elaborator.hs view
@@ -4,13 +4,21 @@ import qualified Data.Text           as Text import           LambdaCube.STLC.Ast -elaborate :: ExtLCTerm -> Either String LCTerm+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-      = Right $ LCVar idx+      = LCVar idx       | otherwise-      = Left $ "Variable " <> Text.unpack v <> " is not in scope"-    go l (ExtLCLam v t b) = LCLam t <$> go (v : l) b-    go l (ExtLCApp f a) = LCApp <$> go l f <*> go l a+      = error $ "Variable " <> Text.unpack v <> " is not in scope"+    go l (ExtLCLam v t b) = LCLam (elaborateType t) $ go (v : l) b+    go l (ExtLCApp f a) = go l f `LCApp` go l a+    go _ (ExtLCMVar _) = error "invalid TemplateHaskell code splicer"
src/LambdaCube/STLC/Evaluator.hs view
@@ -1,16 +1,7 @@ module LambdaCube.STLC.Evaluator where  import           LambdaCube.STLC.Ast--liftLCValue :: LCValue -> LCTerm-liftLCValue (LCValLam t b) = LCLam t b--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) = go m f `LCApp` go m a+import           LambdaCube.STLC.Substitution  evaluate :: LCTerm -> LCValue evaluate = go
+ src/LambdaCube/STLC/Lifter.hs view
@@ -0,0 +1,14 @@+module LambdaCube.STLC.Lifter where++import           LambdaCube.STLC.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++liftLCNeutral :: LCNeutralTerm -> LCTerm+liftLCNeutral (LCNeutVar n) = LCVar n+liftLCNeutral (LCNeutApp f a) = liftLCNeutral f `LCApp` liftLCNormal a
src/LambdaCube/STLC/Normalizer.hs view
@@ -1,23 +1,7 @@ module LambdaCube.STLC.Normalizer where  import           LambdaCube.STLC.Ast--substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm-substituteNormal n nv = go n-  where-    go m (LCNormLam t b)   = LCNormLam t $ go (m + 1) b-    go m (LCNormNeut neut) = substituteNeutral m nv neut--substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm-substituteNeutral n nv = go n-  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   -> substituteNormal 0 a' b-        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'-      where-        a' = substituteNormal m nv a+import           LambdaCube.STLC.Substitution  normalize :: LCTerm -> LCNormalTerm normalize = go@@ -26,7 +10,7 @@     go (LCLam t b) = LCNormLam t $ go b     go (LCApp f a) =       case go f of-        LCNormLam t b   -> LCNormLam t $ substituteNormal 0 a' b+        LCNormLam t b   -> LCNormLam t $ substituteNormalInNormal 0 a' b         LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'       where         a' = go a
src/LambdaCube/STLC/Parser.hs view
@@ -2,6 +2,7 @@  import           Data.Foldable            (Foldable (foldl')) import           Data.Functor             (($>))+import qualified Data.Text                as Text import           LambdaCube.Common.Parser import           LambdaCube.STLC.Ast import           Text.Megaparsec@@ -10,7 +11,7 @@ pTopLC = topParser pLC  pLC :: Parser ExtLCTerm-pLC = pLam <|> pApp+pLC = pLam<|> pApp  pLam :: Parser ExtLCTerm pLam =@@ -23,10 +24,22 @@ pApp = foldl' ExtLCApp <$> pATerm <*> many pATerm  pATerm :: Parser ExtLCTerm-pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC+pATerm = pVar <|> pMVar <|> parenthesized pLC -pType :: Parser LCType-pType = foldr1 LCArr <$> sepBy1 pAType rightArrow+pVar :: Parser ExtLCTerm+pVar = ExtLCVar <$> identifier -pAType :: Parser LCType-pAType = (sharp $> LCBase) <|> parenthesized pType+pMVar :: Parser ExtLCTerm+pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)++pType :: Parser ExtLCType+pType = foldr1 ExtLCArr <$> sepBy1 pAType rightArrow++pAType :: Parser ExtLCType+pAType = pBase <|> pMTVar <|> parenthesized pType++pBase :: Parser ExtLCType+pBase = sharp $> ExtLCBase++pMTVar :: Parser ExtLCType+pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)
src/LambdaCube/STLC/PrettyPrinter.hs view
@@ -9,22 +9,22 @@ import           LambdaCube.Common.PrettyPrinter import           LambdaCube.STLC.Ast -prettyType :: LCType -> Text-prettyType = prettyTypePrec 0+prettyUnnamedType :: LCType -> Text+prettyUnnamedType = prettyUnnamedTypePrec 0 -prettyTerm :: LCTerm -> Text-prettyTerm = prettyTermPrec 0+prettyUnnamedTerm :: LCTerm -> Text+prettyUnnamedTerm = prettyUnnamedTermPrec 0 -prettyTypePrec :: Int -> LCType -> Text-prettyTypePrec = go+prettyUnnamedTypePrec :: Int -> LCType -> Text+prettyUnnamedTypePrec = go   where     go _ LCBase      = "#"     go p (LCArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b] -prettyTermPrec :: Int -> LCTerm -> Text-prettyTermPrec = go+prettyUnnamedTermPrec :: Int -> LCTerm -> Text+prettyUnnamedTermPrec = go   where-    pTP = prettyTypePrec+    pTP = prettyUnnamedTypePrec      go _ (LCVar n)   = Text.pack $ show n     go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
+ src/LambdaCube/STLC/Substitution.hs view
@@ -0,0 +1,28 @@+module LambdaCube.STLC.Substitution where++import           LambdaCube.STLC.Ast+import           LambdaCube.STLC.Lifter++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) = go m f `LCApp` go m a++substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm+substituteNormalInNormal n nv = go n+  where+    go m (LCNormLam t b)   = LCNormLam t $ go (m + 1) b+    go m (LCNormNeut neut) = substituteNormalInNeutral m nv neut++substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm+substituteNormalInNeutral n nv = go n+  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'+      where+        a' = substituteNormalInNormal m nv a
src/LambdaCube/STLC/TH.hs view
@@ -1,43 +1,45 @@-module LambdaCube.STLC.TH where+module LambdaCube.STLC.TH+  ( lc+  ) where -import           Control.Monad              ((<=<))+import           Data.Data                  (Data)+import           Data.Generics              (extQ)+import           Data.Text                  (Text) import qualified Data.Text                  as Text import           LambdaCube.STLC.Ast-import           LambdaCube.STLC.Elaborator 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), Q, lift, location)+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 -stlc :: QuasiQuoter-stlc =+lc :: QuasiQuoter+lc =   QuasiQuoter-    { quoteExp = lift <=< stlcQuoteExp+    { quoteExp = expLc     , quotePat = undefined     , quoteType = undefined     , quoteDec = undefined     } -stlcQuoteExp :: String -> Q ExtLCTerm-stlcQuoteExp str = do+expLc :: String -> ExpQ+expLc str = do   l <- location   case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of-    Right e  -> pure e+    Right e  -> dataToExpQ converter e     Left err -> fail $ PE.errorBundlePretty err+  where+    converter :: Data b => b -> Maybe ExpQ+    converter =+      const Nothing+      `extQ` quotedMVar+      `extQ` quotedMTVar+      `extQ` (Just . lift :: Text -> Maybe ExpQ) -elaboratedStlc :: QuasiQuoter-elaboratedStlc =-  QuasiQuoter-    { quoteExp = lift <=< elaboratedStlcQuoteExp-    , quotePat = undefined-    , quoteType = undefined-    , quoteDec = undefined-    }+    quotedMVar (ExtLCMVar x) = Just . varE $ mkName x+    quotedMVar _             = Nothing -elaboratedStlcQuoteExp :: String -> Q LCTerm-elaboratedStlcQuoteExp str = do-  e <- stlcQuoteExp str-  case elaborate e of-    Right e' -> pure e'-    Left err -> fail err+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x+    quotedMTVar _              = Nothing
src/LambdaCube/STLC/TypeChecker.hs view
@@ -3,15 +3,14 @@ import           Data.List           (uncons) import           LambdaCube.STLC.Ast -infer :: LCTerm -> Maybe LCType+infer :: LCTerm -> LCType infer = go []   where-    go l (LCVar n) = fmap fst . uncons $ drop n l-    go l (LCLam t b) = LCArr t <$> go (t : l) b+    go l (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n l+    go l (LCLam t b) = t `LCArr` go (t : l) b     go l (LCApp f a)-      | Just (LCArr at' rt) <- go l f-      , Just at <- go l a-      , at == at'-      = Just rt+      | LCArr at rt <- go l f+      , at == go l a+      = rt       | otherwise-      = Nothing+      = error "Function argument type mismatch"
+ src/LambdaCube/SystemF.hs view
@@ -0,0 +1,22 @@+module LambdaCube.SystemF+  ( module LambdaCube.SystemF.Ast+  , module LambdaCube.SystemF.Elaborator+  , module LambdaCube.SystemF.Lifter+  , module LambdaCube.SystemF.Normalizer+  , module LambdaCube.SystemF.Parser+  , module LambdaCube.SystemF.PrettyPrinter+  , module LambdaCube.SystemF.Substitution+  , module LambdaCube.SystemF.TH+  , module LambdaCube.SystemF.TypeChecker+  ) where++import LambdaCube.SystemF.Ast++import LambdaCube.SystemF.Elaborator+import LambdaCube.SystemF.Lifter+import LambdaCube.SystemF.Normalizer+import LambdaCube.SystemF.Parser+import LambdaCube.SystemF.PrettyPrinter+import LambdaCube.SystemF.Substitution+import LambdaCube.SystemF.TH+import LambdaCube.SystemF.TypeChecker
src/LambdaCube/SystemF/Ast.hs view
@@ -1,5 +1,6 @@ module LambdaCube.SystemF.Ast where +import           Data.Data                  (Data) import           Data.Text                  (Text) import           Language.Haskell.TH.Syntax (Lift) @@ -8,7 +9,8 @@   | ExtLCTVar Text   | ExtLCArr ExtLCType ExtLCType   | ExtLCUniv Text ExtLCType-  deriving stock (Eq, Show, Lift)+  | ExtLCMTVar String+  deriving stock (Eq, Show, Data, Lift) infixr 5 `ExtLCArr`  data ExtLCTerm@@ -17,7 +19,8 @@   | ExtLCApp ExtLCTerm ExtLCTerm   | ExtLCTLam Text ExtLCTerm   | ExtLCTApp ExtLCTerm ExtLCType-  deriving stock (Eq, Show, Lift)+  | ExtLCMVar String+  deriving stock (Eq, Show, Data, Lift) infixl 6 `ExtLCApp` infixl 6 `ExtLCTApp` @@ -26,7 +29,7 @@   | LCTVar Int   | LCArr LCType LCType   | LCUniv LCType-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixr 5 `LCArr`  data LCTerm@@ -35,25 +38,25 @@   | LCApp LCTerm LCTerm   | LCTLam LCTerm   | LCTApp LCTerm LCType-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixl 6 `LCApp` infixl 6 `LCTApp`  data LCValue   = LCValLam LCType LCTerm   | LCValTLam LCTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift)  data LCNormalTerm   = LCNormLam LCType LCNormalTerm   | LCNormTLam LCNormalTerm   | LCNormNeut LCNeutralTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift)  data LCNeutralTerm   = LCNeutVar Int   | LCNeutApp LCNeutralTerm LCNormalTerm   | LCNeutTApp LCNeutralTerm LCType-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixl 6 `LCNeutApp` infixl 6 `LCNeutTApp`
src/LambdaCube/SystemF/Elaborator.hs view
@@ -5,27 +5,29 @@ import qualified Data.Text              as Text import           LambdaCube.SystemF.Ast -elaborate :: ExtLCTerm -> Either String LCTerm+elaborate :: ExtLCTerm -> LCTerm elaborate = go [] []   where     go _  vl (ExtLCVar x)       | Just n <- x `elemIndex` vl-      = Right $ LCVar n+      = LCVar n       | otherwise-      = Left $ "Term variable " <> Text.unpack x <> " is not in scope"-    go tl vl (ExtLCLam x t b) = LCLam <$> typeElaborate tl t <*> go tl (x : vl) b-    go tl vl (ExtLCApp f a) = LCApp <$> go tl vl f <*> go tl vl a-    go tl vl (ExtLCTLam x b) = LCTLam <$> go (x : tl) vl b-    go tl vl (ExtLCTApp f t) = LCTApp <$> go tl vl f <*> typeElaborate tl t+      = 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 (ExtLCTApp f t) = go tl vl f `LCTApp` elaborateType tl t+    go _  _  (ExtLCMVar _) = error "invalid TemplateHaskell code splicer" -typeElaborate :: [Text] -> ExtLCType -> Either String LCType-typeElaborate = go+elaborateType :: [Text] -> ExtLCType -> LCType+elaborateType = go   where-    go _ ExtLCBase = Right LCBase+    go _ ExtLCBase = LCBase     go l (ExtLCTVar x)       | Just n <- x `elemIndex` l-      = Right $ LCTVar n+      = LCTVar n       | otherwise-      = Left  $ "Type variable " <> Text.unpack x <> " is not in scope"-    go l (ExtLCArr a b) = LCArr <$> go l a <*> go l b-    go l (ExtLCUniv x a) = LCUniv <$> go (x : l) a+      = error $ "Type variable " <> Text.unpack x <> " 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 _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"
src/LambdaCube/SystemF/Evaluator.hs view
@@ -1,20 +1,7 @@ module LambdaCube.SystemF.Evaluator where  import           LambdaCube.SystemF.Ast-import           LambdaCube.SystemF.TypeChecker (substituteType)--liftLCValue :: LCValue -> LCTerm-liftLCValue (LCValLam t b) = LCLam t b-liftLCValue (LCValTLam b)  = LCTLam b--substitute :: Int -> LCValue -> LCTerm -> LCTerm-substitute 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)  = 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+import           LambdaCube.SystemF.Substitution  evaluate :: LCTerm -> LCValue evaluate = go@@ -24,7 +11,7 @@     go (LCApp f a)       | LCValLam _ b <- go f       , v <- go a-      = go $ substitute 0 v b+      = go $ substituteValue 0 v b       | otherwise       = error "Did you really type check this?"     go (LCTLam b) = LCValTLam b
+ src/LambdaCube/SystemF/Lifter.hs view
@@ -0,0 +1,17 @@+module LambdaCube.SystemF.Lifter where++import           LambdaCube.SystemF.Ast++liftLCValue :: LCValue -> LCTerm+liftLCValue (LCValLam t b) = LCLam t b+liftLCValue (LCValTLam b)  = LCTLam b++liftLCNormal :: LCNormalTerm -> LCTerm+liftLCNormal (LCNormLam t b) = LCLam t $ liftLCNormal b+liftLCNormal (LCNormTLam b)  = LCTLam $ 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 (LCNeutTApp f t) = liftLCNeutral f `LCTApp` t
src/LambdaCube/SystemF/Normalizer.hs view
@@ -1,59 +1,7 @@ module LambdaCube.SystemF.Normalizer where  import           LambdaCube.SystemF.Ast-import           LambdaCube.SystemF.TypeChecker (substituteTypeInType)--substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm-substituteNormal n v = go n-  where-    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b-    go m (LCNormTLam b)  = LCNormTLam $ go m b-    go m (LCNormNeut nt) = substituteNeutral m v nt--substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm-substituteNeutral n v = go n-  where-    go m e@(LCNeutVar l)-      | m == l = v-      | otherwise = LCNormNeut e-    go m (LCNeutApp f a) =-      case go m f of-        LCNormLam _ b -> substituteNormal 0 a' b-        LCNormTLam _  -> error "Did you really type check this?"-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'-      where-        a' = substituteNormal m v a-    go m (LCNeutTApp f t) =-      case go m f of-        LCNormLam _ _ -> error "Did you really type check this?"-        LCNormTLam b  -> substituteTypeNormal 0 t b-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t--substituteTypeNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm-substituteTypeNormal n v = go n-  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) = substituteTypeNeutral m v nt--substituteTypeNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm-substituteTypeNeutral n v = go n-  where-    go _ e@(LCNeutVar _) = LCNormNeut e-    go m (LCNeutApp f a) =-      case go m f of-        LCNormLam _ b -> substituteNormal 0 a' b-        LCNormTLam _  -> error "Did you really type check this?"-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'-      where-        a' = substituteTypeNormal m v a-    go m (LCNeutTApp f t) =-      case go m f of-        LCNormLam _ _ -> error "Did you really type check this?"-        LCNormTLam b  -> substituteTypeNormal 0 t' b-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t'-      where-        t' = substituteTypeInType m v t+import           LambdaCube.SystemF.Substitution  normalize :: LCTerm -> LCNormalTerm normalize = go@@ -63,7 +11,7 @@     go (LCTLam b) = LCNormTLam $ go b     go (LCApp f a) =       case go f of-        LCNormLam _ b   -> substituteNormal 0 a' b+        LCNormLam _ b   -> substituteNormalInNormal 0 a' b         LCNormTLam _    -> error "Did you really type check this?"         LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'       where@@ -71,5 +19,5 @@     go (LCTApp f t) =       case go f of         LCNormLam _ _   -> error "Did you really type check this?"-        LCNormTLam b    -> substituteTypeNormal 0 t b+        LCNormTLam b    -> substituteTypeInNormal 0 t b         LCNormNeut neut -> LCNormNeut $ neut `LCNeutTApp` t
src/LambdaCube/SystemF/Parser.hs view
@@ -7,6 +7,7 @@ import           LambdaCube.Common.Parser import           LambdaCube.SystemF.Ast import           Text.Megaparsec+import qualified Data.Text as Text  pTopLC :: Parser ExtLCTerm pTopLC = topParser pLC@@ -38,8 +39,14 @@     else flip ExtLCApp <$> pATerm  pATerm :: Parser ExtLCTerm-pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC+pATerm = pVar <|> pMVar <|> parenthesized pLC +pVar :: Parser ExtLCTerm+pVar = ExtLCVar <$> identifier++pMVar :: Parser ExtLCTerm+pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)+ pType :: Parser ExtLCType pType = pUniv <|> pArr @@ -53,4 +60,13 @@ pArr = foldr1 ExtLCArr <$> sepBy1 pAType rightArrow  pAType :: Parser ExtLCType-pAType = (sharp $> ExtLCBase) <|> (ExtLCTVar <$> identifier) <|> parenthesized pType+pAType = pBase <|> pTVar <|> pMTVar <|> parenthesized pType++pBase :: Parser ExtLCType+pBase = sharp $> ExtLCBase++pTVar :: Parser ExtLCType+pTVar = ExtLCTVar <$> identifier++pMTVar :: Parser ExtLCType+pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)
src/LambdaCube/SystemF/PrettyPrinter.hs view
@@ -9,24 +9,24 @@ import           LambdaCube.Common.PrettyPrinter import           LambdaCube.SystemF.Ast -prettyType :: LCType -> Text-prettyType = prettyTypePrec 0+prettyUnnamedType :: LCType -> Text+prettyUnnamedType = prettyUnnamedTypePrec 0 -prettyTerm :: LCTerm -> Text-prettyTerm = prettyTermPrec 0+prettyUnnamedTerm :: LCTerm -> Text+prettyUnnamedTerm = prettyUnnamedTermPrec 0 -prettyTypePrec :: Int -> LCType -> Text-prettyTypePrec = go+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] -prettyTermPrec :: Int -> LCTerm -> Text-prettyTermPrec = go+prettyUnnamedTermPrec :: Int -> LCTerm -> Text+prettyUnnamedTermPrec = go   where-    pTP = prettyTypePrec+    pTP = prettyUnnamedTypePrec      go _ (LCVar i)    = Text.pack $ show i     go p (LCLam t b)  = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
+ src/LambdaCube/SystemF/Substitution.hs view
@@ -0,0 +1,82 @@+module LambdaCube.SystemF.Substitution where++import           LambdaCube.SystemF.Ast+import           LambdaCube.SystemF.Lifter++substituteType :: Int -> LCType -> LCTerm -> LCTerm+substituteType n v = go n+  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++substituteTypeInType :: Int -> LCType -> LCType -> LCType+substituteTypeInType n v = go n+  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++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)  = 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++substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm+substituteNormalInNormal n v = go n+  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++substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm+substituteNormalInNeutral n v = go n+  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+        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+        LCNormLam _ _ -> error "Did you really type check this?"+        LCNormTLam b  -> substituteTypeInNormal 0 t b+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t++substituteTypeInNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm+substituteTypeInNormal n v = go n+  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++substituteTypeInNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm+substituteTypeInNeutral n v = go n+  where+    go _ e@(LCNeutVar _) = LCNormNeut e+    go m (LCNeutApp f a) =+      case go m f of+        LCNormLam _ b -> substituteNormalInNormal 0 a' 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+        LCNormLam _ _ -> error "Did you really type check this?"+        LCNormTLam b  -> substituteTypeInNormal 0 t' b+        LCNormNeut nt -> LCNormNeut $ nt `LCNeutTApp` t'+      where+        t' = substituteTypeInType m v t
src/LambdaCube/SystemF/TH.hs view
@@ -1,44 +1,45 @@-module LambdaCube.SystemF.TH where+module LambdaCube.SystemF.TH+  ( lc+  ) where -import           Control.Monad                 ((<=<))-import qualified Data.Text                     as Text+import           Data.Data                  (Data)+import           Data.Generics              (extQ)+import           Data.Text                  (Text)+import qualified Data.Text                  as Text import           LambdaCube.SystemF.Ast-import           LambdaCube.SystemF.Elaborator import           LambdaCube.SystemF.Parser-import           Language.Haskell.TH.Quote     (QuasiQuoter (..))-import           Language.Haskell.TH.Syntax    (Loc (loc_start), Q, lift,-                                                location)-import qualified Text.Megaparsec               as P-import qualified Text.Megaparsec.Error         as PE+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 -systemF :: QuasiQuoter-systemF =+lc :: QuasiQuoter+lc =   QuasiQuoter-    { quoteExp = lift <=< systemFQuoteExp+    { quoteExp = expLc     , quotePat = undefined     , quoteType = undefined     , quoteDec = undefined     } -systemFQuoteExp :: String -> Q ExtLCTerm-systemFQuoteExp str = do+expLc :: String -> ExpQ+expLc str = do   l <- location   case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of-    Right e  -> pure e+    Right e  -> dataToExpQ converter e     Left err -> fail $ PE.errorBundlePretty err+  where+    converter :: Data b => b -> Maybe ExpQ+    converter =+      const Nothing+      `extQ` quotedMVar+      `extQ` quotedMTVar+      `extQ` (Just . lift :: Text -> Maybe ExpQ) -elaboratedSystemF :: QuasiQuoter-elaboratedSystemF =-  QuasiQuoter-    { quoteExp = lift <=< elaboratedSystemFQuoteExp-    , quotePat = undefined-    , quoteType = undefined-    , quoteDec = undefined-    }+    quotedMVar (ExtLCMVar x) = Just . varE $ mkName x+    quotedMVar _             = Nothing -elaboratedSystemFQuoteExp :: String -> Q LCTerm-elaboratedSystemFQuoteExp str = do-  e <- systemFQuoteExp str-  case elaborate e of-    Right e' -> pure e'-    Left err -> fail err+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x+    quotedMTVar _              = Nothing
src/LambdaCube/SystemF/TypeChecker.hs view
@@ -1,40 +1,23 @@ module LambdaCube.SystemF.TypeChecker where -import           Data.List              (uncons)+import           Data.List                       (uncons) import           LambdaCube.SystemF.Ast--substituteType :: Int -> LCType -> LCTerm -> LCTerm-substituteType n v = go n-  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--substituteTypeInType :: Int -> LCType -> LCType -> LCType-substituteTypeInType n v = go n-  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+import           LambdaCube.SystemF.Substitution -infer :: LCTerm -> Maybe LCType+infer :: LCTerm -> LCType infer = go []   where-    go tl (LCVar n) = fmap fst . uncons $ drop n tl-    go tl (LCLam t b) = LCArr t <$> go (t : tl) b+    go tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl+    go tl (LCLam t b) = t `LCArr` go (t : tl) b     go tl (LCApp f a)-      | Just (LCArr at' rt) <- go tl f-      , Just at <- go tl a-      , at == at'-      = Just rt+      | LCArr at rt <- go tl f+      , at == go tl a+      = rt       | otherwise-      = Nothing-    go tl (LCTLam b) = LCUniv <$> go tl b+      = error "Function argument type mismatch"+    go tl (LCTLam b) = LCUniv $ go tl b     go tl (LCTApp f t)-      | Just (LCUniv rt) <- go tl f-      = Just $ substituteTypeInType 0 t rt+      | LCUniv rt <- go tl f+      = substituteTypeInType 0 t rt       | otherwise-      = Nothing+      = error "Function argument type mismatch"
+ src/LambdaCube/SystemFw.hs view
@@ -0,0 +1,22 @@+module LambdaCube.SystemFw+  ( module LambdaCube.SystemFw.Ast+  , module LambdaCube.SystemFw.Elaborator+  , module LambdaCube.SystemFw.Lifter+  , module LambdaCube.SystemFw.Normalizer+  , module LambdaCube.SystemFw.Parser+  , module LambdaCube.SystemFw.PrettyPrinter+  , module LambdaCube.SystemFw.Substitution+  , module LambdaCube.SystemFw.TH+  , module LambdaCube.SystemFw.TypeChecker+  ) where++import LambdaCube.SystemFw.Ast++import LambdaCube.SystemFw.Elaborator+import LambdaCube.SystemFw.Lifter+import LambdaCube.SystemFw.Normalizer+import LambdaCube.SystemFw.Parser+import LambdaCube.SystemFw.PrettyPrinter+import LambdaCube.SystemFw.Substitution+import LambdaCube.SystemFw.TH+import LambdaCube.SystemFw.TypeChecker
src/LambdaCube/SystemFw/Ast.hs view
@@ -1,16 +1,25 @@ module LambdaCube.SystemFw.Ast where +import           Data.Data                  (Data) import           Data.Text                  (Text) import           Language.Haskell.TH.Syntax (Lift) +data ExtLCKind+  = ExtLCStar+  | ExtLCKArr ExtLCKind ExtLCKind+  | ExtLCMKVar String+  deriving stock (Eq, Show, Data, Lift)+infixr 5 `ExtLCKArr`+ data ExtLCType   = ExtLCBase   | ExtLCTVar Text   | ExtLCArr ExtLCType ExtLCType-  | ExtLCUniv Text LCKind ExtLCType-  | ExtLCTTLam Text LCKind ExtLCType+  | ExtLCUniv Text ExtLCKind ExtLCType+  | ExtLCTTLam Text ExtLCKind ExtLCType   | ExtLCTTApp ExtLCType ExtLCType-  deriving stock (Eq, Show, Lift)+  | ExtLCMTVar String+  deriving stock (Eq, Show, Data, Lift) infixr 5 `ExtLCArr` infixl 6 `ExtLCTTApp` @@ -18,16 +27,17 @@   = ExtLCVar Text   | ExtLCLam Text ExtLCType ExtLCTerm   | ExtLCApp ExtLCTerm ExtLCTerm-  | ExtLCTLam Text LCKind ExtLCTerm+  | ExtLCTLam Text ExtLCKind ExtLCTerm   | ExtLCTApp ExtLCTerm ExtLCType-  deriving stock (Eq, Show, Lift)+  | ExtLCMVar String+  deriving stock (Eq, Show, Data, Lift) infixl 6 `ExtLCApp` infixl 6 `ExtLCTApp`  data LCKind   = LCStar   | LCKArr LCKind LCKind-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixr 5 `LCKArr`  data LCType@@ -37,7 +47,7 @@   | LCUniv LCKind LCType   | LCTTLam LCKind LCType   | LCTTApp LCType LCType-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixr 5 `LCArr` infixl 6 `LCTTApp` @@ -47,25 +57,25 @@   | LCApp LCTerm LCTerm   | LCTLam LCKind LCTerm   | LCTApp LCTerm LCType-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixl 6 `LCApp` infixl 6 `LCTApp`  data LCValue   = LCValLam LCType LCTerm   | LCValTLam LCKind LCTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift)  data LCNormalTerm   = LCNormLam LCType LCNormalTerm   | LCNormTLam LCKind LCNormalTerm   | LCNormNeut LCNeutralTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift)  data LCNeutralTerm   = LCNeutVar Int   | LCNeutApp LCNeutralTerm LCNormalTerm   | LCNeutTApp LCNeutralTerm LCType-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixl 6 `LCNeutApp` infixl 6 `LCNeutTApp`
src/LambdaCube/SystemFw/Elaborator.hs view
@@ -5,29 +5,38 @@ import qualified Data.Text               as Text import           LambdaCube.SystemFw.Ast -elaborate :: ExtLCTerm -> Either String LCTerm+elaborate :: ExtLCTerm -> LCTerm elaborate = go [] []   where     go _  vl (ExtLCVar x)       | Just n <- x `elemIndex` vl-      = Right $ LCVar n+      = LCVar n       | otherwise-      = Left $ "Term variable " <> Text.unpack x <> " is not in scope"-    go tl vl (ExtLCLam x t b) = LCLam <$> typeElaborate tl t <*> go tl (x : vl) b-    go tl vl (ExtLCApp f a) = LCApp <$> go tl vl f <*> go tl vl a-    go tl vl (ExtLCTLam x k b) = LCTLam k <$> go (x : tl) vl b-    go tl vl (ExtLCTApp f t) = LCTApp <$> go tl vl f <*> typeElaborate tl t+      = 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 (ExtLCTApp f t) = go tl vl f `LCTApp` elaborateType tl t+    go _  _  (ExtLCMVar _) = error "invalid TemplateHaskell code splicer" -typeElaborate :: [Text] -> ExtLCType -> Either String LCType-typeElaborate = go+elaborateType :: [Text] -> ExtLCType -> LCType+elaborateType = go   where-    go _ ExtLCBase = Right LCBase+    go _ ExtLCBase = LCBase     go l (ExtLCTVar x)       | Just n <- x `elemIndex` l-      = Right $ LCTVar n+      = LCTVar n       | otherwise-      = Left  $ "Type variable " <> Text.unpack x <> " is not in scope"-    go l (ExtLCArr a b) = LCArr <$> go l a <*> go l b-    go l (ExtLCUniv x k a) = LCUniv k <$> go (x : l) a-    go l (ExtLCTTLam x k b) = LCTTLam k <$> go (x : l) b-    go l (ExtLCTTApp f a) = LCTTApp <$> go l f <*> go l a+      = error $ "Type variable " <> Text.unpack x <> " 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 (ExtLCTTApp f a) = go l f `LCTTApp` go l a+    go _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"++elaborateKind :: ExtLCKind -> LCKind+elaborateKind = go+  where+    go ExtLCStar = LCStar+    go (ExtLCKArr a b) = go a `LCKArr` go b+    go (ExtLCMKVar _) = error "invalid TemplateHaskell code splicer"
src/LambdaCube/SystemFw/Evaluator.hs view
@@ -1,20 +1,7 @@ module LambdaCube.SystemFw.Evaluator where  import           LambdaCube.SystemFw.Ast-import           LambdaCube.SystemFw.TypeChecker (substituteType)--liftLCValue :: LCValue -> LCTerm-liftLCValue (LCValLam t b)  = LCLam t b-liftLCValue (LCValTLam k b) = LCTLam k b--substitute :: Int -> LCValue -> LCTerm -> LCTerm-substitute 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)  = 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+import           LambdaCube.SystemFw.Substitution  evaluate :: LCTerm -> LCValue evaluate = go@@ -24,7 +11,7 @@     go (LCApp f a)       | LCValLam _ b <- go f       , v <- go a-      = go $ substitute 0 v b+      = go $ substituteValue 0 v b       | otherwise       = error "Did you really type check this?"     go (LCTLam k b) = LCValTLam k b
+ src/LambdaCube/SystemFw/Lifter.hs view
@@ -0,0 +1,17 @@+module LambdaCube.SystemFw.Lifter where++import           LambdaCube.SystemFw.Ast++liftLCValue :: LCValue -> LCTerm+liftLCValue (LCValLam t b)  = LCLam t b+liftLCValue (LCValTLam k b) = LCTLam k b++liftLCNormal :: LCNormalTerm -> LCTerm+liftLCNormal (LCNormLam t b)  = LCLam t $ liftLCNormal b+liftLCNormal (LCNormTLam k b) = LCTLam k $ 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 (LCNeutTApp f t) = liftLCNeutral f `LCTApp` t
src/LambdaCube/SystemFw/Normalizer.hs view
@@ -1,59 +1,7 @@ module LambdaCube.SystemFw.Normalizer where  import           LambdaCube.SystemFw.Ast-import           LambdaCube.SystemFw.TypeChecker (substituteTypeInType)--substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm-substituteNormal n v = go n-  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)  = substituteNeutral m v nt--substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm-substituteNeutral n v = go n-  where-    go m e@(LCNeutVar l)-      | m == l = v-      | otherwise = LCNormNeut e-    go m (LCNeutApp f a) =-      case go m f of-        LCNormLam _ b  -> substituteNormal 0 a' b-        LCNormTLam _ _ -> error "Did you really type check this?"-        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'-      where-        a' = substituteNormal m v a-    go m (LCNeutTApp f t) =-      case go m f of-        LCNormLam _ _  -> error "Did you really type check this?"-        LCNormTLam _ b -> substituteTypeNormal 0 t b-        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t--substituteTypeNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm-substituteTypeNormal n v = go n-  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)  = substituteTypeNeutral m v nt--substituteTypeNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm-substituteTypeNeutral n v = go n-  where-    go _ e@(LCNeutVar _) = LCNormNeut e-    go m (LCNeutApp f a) =-      case go m f of-        LCNormLam _ b  -> substituteNormal 0 a' b-        LCNormTLam _ _ -> error "Did you really type check this?"-        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutApp` a'-      where-        a' = substituteTypeNormal m v a-    go m (LCNeutTApp f t) =-      case go m f of-        LCNormLam _ _  -> error "Did you really type check this?"-        LCNormTLam _ b -> substituteTypeNormal 0 t' b-        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t'-      where-        t' = substituteTypeInType m v t+import           LambdaCube.SystemFw.Substitution  normalize :: LCTerm -> LCNormalTerm normalize = go@@ -63,7 +11,7 @@     go (LCTLam k b) = LCNormTLam k $ go b     go (LCApp f a) =       case go f of-        LCNormLam _ b   -> substituteNormal 0 a' b+        LCNormLam _ b   -> substituteNormalInNormal 0 a' b         LCNormTLam _ _  -> error "Did you really type check this?"         LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'       where@@ -71,5 +19,5 @@     go (LCTApp f t) =       case go f of         LCNormLam _ _   -> error "Did you really type check this?"-        LCNormTLam _ b  -> substituteTypeNormal 0 t b+        LCNormTLam _ b  -> substituteTypeInNormal 0 t b         LCNormNeut neut -> LCNormNeut $ neut `LCNeutTApp` t
src/LambdaCube/SystemFw/Parser.hs view
@@ -4,6 +4,7 @@ import           Data.Function            ((&)) import           Data.Functor             (($>)) import           Data.Maybe               (isJust)+import qualified Data.Text                as Text import           LambdaCube.Common.Parser import           LambdaCube.SystemFw.Ast import           Text.Megaparsec@@ -39,8 +40,14 @@     else flip ExtLCApp <$> pATerm  pATerm :: Parser ExtLCTerm-pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC+pATerm = pVar <|> pMVar <|> parenthesized pLC +pVar :: Parser ExtLCTerm+pVar = ExtLCVar <$> identifier++pMVar :: Parser ExtLCTerm+pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)+ pType :: Parser ExtLCType pType = pTTLam <|> pUniv <|> pArr @@ -65,10 +72,25 @@ pTTApp = foldl' ExtLCTTApp <$> pAType <*> many pAType  pAType :: Parser ExtLCType-pAType = (sharp $> ExtLCBase) <|> (ExtLCTVar <$> identifier) <|> parenthesized pType+pAType = pBase <|> pTVar <|> pMTVar <|> parenthesized pType -pKind :: Parser LCKind-pKind = foldr1 LCKArr <$> sepBy1 pAKind rightArrow+pBase :: Parser ExtLCType+pBase = sharp $> ExtLCBase -pAKind :: Parser LCKind-pAKind = (asterisk $> LCStar) <|> parenthesized pKind+pTVar :: Parser ExtLCType+pTVar = ExtLCTVar <$> identifier++pMTVar :: Parser ExtLCType+pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)++pKind :: Parser ExtLCKind+pKind = foldr1 ExtLCKArr <$> sepBy1 pAKind rightArrow++pAKind :: Parser ExtLCKind+pAKind = pStar <|> pMKVar <|> parenthesized pKind++pStar :: Parser ExtLCKind+pStar = asterisk $> ExtLCStar++pMKVar :: Parser ExtLCKind+pMKVar = ExtLCMKVar <$> (dollarsign *> fmap Text.unpack identifier)
src/LambdaCube/SystemFw/PrettyPrinter.hs view
@@ -9,25 +9,25 @@ import           LambdaCube.Common.PrettyPrinter import           LambdaCube.SystemFw.Ast -prettyKind :: LCKind -> Text-prettyKind = prettyKindPrec 0+prettyUnnamedKind :: LCKind -> Text+prettyUnnamedKind = prettyUnnamedKindPrec 0 -prettyType :: LCType -> Text-prettyType = prettyTypePrec 0+prettyUnnamedType :: LCType -> Text+prettyUnnamedType = prettyUnnamedTypePrec 0 -prettyTerm :: LCTerm -> Text-prettyTerm = prettyTermPrec 0+prettyUnnamedTerm :: LCTerm -> Text+prettyUnnamedTerm = prettyUnnamedTermPrec 0 -prettyKindPrec :: Int -> LCKind -> Text-prettyKindPrec = go+prettyUnnamedKindPrec :: Int -> LCKind -> Text+prettyUnnamedKindPrec = go   where     go _ LCStar       = "*"     go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b] -prettyTypePrec :: Int -> LCType -> Text-prettyTypePrec = go+prettyUnnamedTypePrec :: Int -> LCType -> Text+prettyUnnamedTypePrec = go   where-    pKP = prettyKindPrec+    pKP = prettyUnnamedKindPrec      go _ LCBase        = "#"     go _ (LCTVar i)    = Text.pack $ show i@@ -36,11 +36,11 @@     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] -prettyTermPrec :: Int -> LCTerm -> Text-prettyTermPrec = go+prettyUnnamedTermPrec :: Int -> LCTerm -> Text+prettyUnnamedTermPrec = go   where-    pKP = prettyKindPrec-    pTP = prettyTypePrec+    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]
+ src/LambdaCube/SystemFw/Substitution.hs view
@@ -0,0 +1,84 @@+module LambdaCube.SystemFw.Substitution where++import           LambdaCube.SystemFw.Ast+import           LambdaCube.SystemFw.Lifter++substituteType :: Int -> LCType -> LCTerm -> LCTerm+substituteType n v = go n+  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++substituteTypeInType :: Int -> LCType -> LCType -> LCType+substituteTypeInType n v = go n+  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++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)  = 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++substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm+substituteNormalInNormal n v = go n+  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++substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm+substituteNormalInNeutral n v = go n+  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+        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+        LCNormLam _ _  -> error "Did you really type check this?"+        LCNormTLam _ b -> substituteTypeInNormal 0 t b+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t++substituteTypeInNormal :: Int -> LCType -> LCNormalTerm -> LCNormalTerm+substituteTypeInNormal n v = go n+  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++substituteTypeInNeutral :: Int -> LCType -> LCNeutralTerm -> LCNormalTerm+substituteTypeInNeutral n v = go n+  where+    go _ e@(LCNeutVar _) = LCNormNeut e+    go m (LCNeutApp f a) =+      case go m f of+        LCNormLam _ b  -> substituteNormalInNormal 0 a' 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+        LCNormLam _ _  -> error "Did you really type check this?"+        LCNormTLam _ b -> substituteTypeInNormal 0 t' b+        LCNormNeut nt  -> LCNormNeut $ nt `LCNeutTApp` t'+      where+        t' = substituteTypeInType m v t
src/LambdaCube/SystemFw/TH.hs view
@@ -1,44 +1,49 @@-module LambdaCube.SystemFw.TH where+module LambdaCube.SystemFw.TH+  ( lc+  ) where -import           Control.Monad                  ((<=<))-import qualified Data.Text                      as Text+import           Data.Data                  (Data)+import           Data.Generics              (extQ)+import           Data.Text                  (Text)+import qualified Data.Text                  as Text import           LambdaCube.SystemFw.Ast-import           LambdaCube.SystemFw.Elaborator import           LambdaCube.SystemFw.Parser-import           Language.Haskell.TH.Quote      (QuasiQuoter (..))-import           Language.Haskell.TH.Syntax     (Loc (loc_start), Q, lift,-                                                 location)-import qualified Text.Megaparsec                as P-import qualified Text.Megaparsec.Error          as PE+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 -systemFw :: QuasiQuoter-systemFw =+lc :: QuasiQuoter+lc =   QuasiQuoter-    { quoteExp = lift <=< systemFwQuoteExp+    { quoteExp = expLc     , quotePat = undefined     , quoteType = undefined     , quoteDec = undefined     } -systemFwQuoteExp :: String -> Q ExtLCTerm-systemFwQuoteExp str = do+expLc :: String -> ExpQ+expLc str = do   l <- location   case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of-    Right e  -> pure e+    Right e  -> dataToExpQ converter e     Left err -> fail $ PE.errorBundlePretty err+  where+    converter :: Data b => b -> Maybe ExpQ+    converter =+      const Nothing+      `extQ` quotedMVar+      `extQ` quotedMTVar+      `extQ` quotedMKVar+      `extQ` (Just . lift :: Text -> Maybe ExpQ) -elaboratedSystemFw :: QuasiQuoter-elaboratedSystemFw =-  QuasiQuoter-    { quoteExp = lift <=< elaboratedSystemFwQuoteExp-    , quotePat = undefined-    , quoteType = undefined-    , quoteDec = undefined-    }+    quotedMVar (ExtLCMVar x) = Just . varE $ mkName x+    quotedMVar _             = Nothing -elaboratedSystemFwQuoteExp :: String -> Q LCTerm-elaboratedSystemFwQuoteExp str = do-  e <- systemFwQuoteExp str-  case elaborate e of-    Right e' -> pure e'-    Left err -> fail err+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x+    quotedMTVar _              = Nothing++    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x+    quotedMKVar _              = Nothing
src/LambdaCube/SystemFw/TypeChecker.hs view
@@ -1,26 +1,8 @@ module LambdaCube.SystemFw.TypeChecker where -import           Data.List               (uncons)+import           Data.List                        (uncons) import           LambdaCube.SystemFw.Ast--substituteType :: Int -> LCType -> LCTerm -> LCTerm-substituteType n v = go n-  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--substituteTypeInType :: Int -> LCType -> LCType -> LCType-substituteTypeInType n v = go n-  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+import           LambdaCube.SystemFw.Substitution  reduceType :: LCType -> LCType reduceType = go@@ -37,50 +19,47 @@       | otherwise       = error "Did you really kind check this?" -infer :: LCTerm -> Maybe LCType+infer :: LCTerm -> LCType infer = go []   where-    go tl (LCVar n) = fmap fst . uncons $ drop n tl+    go tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl     go tl (LCLam t b)-      | Just LCStar <- inferKind t-      = LCArr v <$> go (v : tl) b+      | LCStar <- inferKind t+      = v `LCArr` go (v : tl) b       | otherwise-      = Nothing+      = error "Function argument kind mismatch"       where         v = reduceType t     go tl (LCApp f a)-      | Just (LCArr at' rt) <- go tl f-      , Just at <- go tl a-      , at == at'-      = Just rt+      | LCArr at rt <- go tl f+      , at == go tl a+      = rt       | otherwise-      = Nothing-    go tl (LCTLam k b) = LCUniv k <$> go tl b+      = error "Function argument type mismatch"+    go tl (LCTLam k b) = LCUniv k $ go tl b     go tl (LCTApp f t)-      | Just (LCUniv tk' rt) <- go tl f-      , Just tk <- inferKind t-      , tk == tk'-      = Just $ substituteTypeInType 0 t rt+      | LCUniv tk rt <- go tl f+      , tk == inferKind t+      = substituteTypeInType 0 t rt       | otherwise-      = Nothing+      = error "Function argument kind mismatch" -inferKind :: LCType -> Maybe LCKind+inferKind :: LCType -> LCKind inferKind = go []   where-    go _  LCBase = Just LCStar-    go kl (LCTVar n) = fmap fst . uncons $ drop n kl+    go _  LCBase = LCStar+    go kl (LCTVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n kl     go kl (LCArr a b)-      | Just LCStar <- go kl a-      , Just LCStar <- go kl b-      = Just LCStar+      | LCStar <- go kl a+      , LCStar <- go kl b+      = LCStar       | otherwise-      = Nothing+      = error "Arrow kind mismatch"     go kl (LCUniv k a) = go (k : kl) a-    go kl (LCTTLam k b) = LCKArr k <$> go (k : kl) b+    go kl (LCTTLam k b) = LCKArr k $ go (k : kl) b     go kl (LCTTApp f a)-      | Just (LCKArr ak' rk) <- go kl f-      , Just ak <- go kl a-      , ak == ak'-      = Just rk+      | LCKArr ak rk <- go kl f+      , ak == go kl a+      = rk       | otherwise-      = Nothing+      = error "Function argument kind mismatch"
+ src/LambdaCube/SystemFw_.hs view
@@ -0,0 +1,22 @@+module LambdaCube.SystemFw_+  ( module LambdaCube.SystemFw_.Ast+  , module LambdaCube.SystemFw_.Elaborator+  , module LambdaCube.SystemFw_.Lifter+  , module LambdaCube.SystemFw_.Normalizer+  , module LambdaCube.SystemFw_.Parser+  , module LambdaCube.SystemFw_.PrettyPrinter+  , module LambdaCube.SystemFw_.Substitution+  , module LambdaCube.SystemFw_.TH+  , module LambdaCube.SystemFw_.TypeChecker+  ) where++import LambdaCube.SystemFw_.Ast++import LambdaCube.SystemFw_.Elaborator+import LambdaCube.SystemFw_.Lifter+import LambdaCube.SystemFw_.Normalizer+import LambdaCube.SystemFw_.Parser+import LambdaCube.SystemFw_.PrettyPrinter+import LambdaCube.SystemFw_.Substitution+import LambdaCube.SystemFw_.TH+import LambdaCube.SystemFw_.TypeChecker
src/LambdaCube/SystemFw_/Ast.hs view
@@ -1,15 +1,24 @@ module LambdaCube.SystemFw_.Ast where +import           Data.Data                  (Data) import           Data.Text                  (Text) import           Language.Haskell.TH.Syntax (Lift) +data ExtLCKind+  = ExtLCStar+  | ExtLCKArr ExtLCKind ExtLCKind+  | ExtLCMKVar String+  deriving stock (Eq, Show, Data, Lift)+infixr 5 `ExtLCKArr`+ data ExtLCType   = ExtLCBase   | ExtLCTVar Text   | ExtLCArr ExtLCType ExtLCType-  | ExtLCTTLam Text LCKind ExtLCType+  | ExtLCTTLam Text ExtLCKind ExtLCType   | ExtLCTTApp ExtLCType ExtLCType-  deriving stock (Eq, Show, Lift)+  | ExtLCMTVar String+  deriving stock (Eq, Show, Data, Lift) infixr 5 `ExtLCArr` infixl 6 `ExtLCTTApp` @@ -17,13 +26,14 @@   = ExtLCVar Text   | ExtLCLam Text ExtLCType ExtLCTerm   | ExtLCApp ExtLCTerm ExtLCTerm-  deriving stock (Eq, Show, Lift)+  | ExtLCMVar String+  deriving stock (Eq, Show, Data, Lift) infixl 6 `ExtLCApp`  data LCKind   = LCStar   | LCKArr LCKind LCKind-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixr 5 `LCKArr`  data LCType@@ -32,7 +42,7 @@   | LCArr LCType LCType   | LCTTLam LCKind LCType   | LCTTApp LCType LCType-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixr 5 `LCArr` infixl 6 `LCTTApp` @@ -40,20 +50,20 @@   = LCVar Int   | LCLam LCType LCTerm   | LCApp LCTerm LCTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixl 6 `LCApp`  data LCValue   = LCValLam LCType LCTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift)  data LCNormalTerm   = LCNormLam LCType LCNormalTerm   | LCNormNeut LCNeutralTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift)  data LCNeutralTerm   = LCNeutVar Int   | LCNeutApp LCNeutralTerm LCNormalTerm-  deriving stock (Eq, Show, Lift)+  deriving stock (Eq, Show, Data, Lift) infixl 6 `LCNeutApp`
src/LambdaCube/SystemFw_/Elaborator.hs view
@@ -4,26 +4,35 @@ import qualified Data.Text                as Text import           LambdaCube.SystemFw_.Ast -elaborate :: ExtLCTerm -> Either String LCTerm+elaborate :: ExtLCTerm -> LCTerm elaborate = go []   where     go l (ExtLCVar x)       | Just n <- x `elemIndex` l-      = Right $ LCVar n+      = LCVar n       | otherwise-      = Left $ "Term variable " <> Text.unpack x <> " is not in scope"-    go l (ExtLCLam x t b) = LCLam <$> typeElaborate t <*> go (x : l) b-    go l (ExtLCApp f a) = LCApp <$> go l f <*> go l a+      = error $ "Term 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" -typeElaborate :: ExtLCType -> Either String LCType-typeElaborate = go []+elaborateType :: ExtLCType -> LCType+elaborateType = go []   where-    go _ ExtLCBase = Right LCBase+    go _ ExtLCBase = LCBase     go l (ExtLCTVar x)       | Just n <- x `elemIndex` l-      = Right $ LCTVar n+      = LCTVar n       | otherwise-      = Left  $ "Type variable " <> Text.unpack x <> " is not in scope"-    go l (ExtLCArr a b) = LCArr <$> go l a <*> go l b-    go l (ExtLCTTLam x k b) = LCTTLam k <$> go (x : l) b-    go l (ExtLCTTApp f a) = LCTTApp <$> go l f <*> go l a+      = error $ "Type variable " <> Text.unpack x <> " 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 (ExtLCTTApp f a) = go l f `LCTTApp` go l a+    go _ (ExtLCMTVar _) = error "invalid TemplateHaskell code splicer"++elaborateKind :: ExtLCKind -> LCKind+elaborateKind = go+  where+    go ExtLCStar = LCStar+    go (ExtLCKArr a b) = go a `LCKArr` go b+    go (ExtLCMKVar _) = error "invalid TemplateHaskell code splicer"
src/LambdaCube/SystemFw_/Evaluator.hs view
@@ -1,16 +1,7 @@ module LambdaCube.SystemFw_.Evaluator where  import           LambdaCube.SystemFw_.Ast--liftLCValue :: LCValue -> LCTerm-liftLCValue (LCValLam t b) = LCLam t b--substitute :: Int -> LCValue -> LCTerm -> LCTerm-substitute 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 (substitute (m + 1) v b)-    go m (LCApp f a) = LCApp (go m f) (go m a)+import           LambdaCube.SystemFw_.Substitution  evaluate :: LCTerm -> LCValue evaluate = go@@ -20,6 +11,6 @@     go (LCApp f a)       | LCValLam _ b <- go f       , v <- go a-      = go (substitute 0 v b)+      = go (substituteValue 0 v b)       | otherwise       = error "Did you really type check this?"
+ src/LambdaCube/SystemFw_/Lifter.hs view
@@ -0,0 +1,14 @@+module LambdaCube.SystemFw_.Lifter where++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++liftLCNeutral :: LCNeutralTerm -> LCTerm+liftLCNeutral (LCNeutVar n)    = LCVar n+liftLCNeutral (LCNeutApp f a)  = liftLCNeutral f `LCApp` liftLCNormal a
src/LambdaCube/SystemFw_/Normalizer.hs view
@@ -1,24 +1,8 @@ module LambdaCube.SystemFw_.Normalizer where  import           LambdaCube.SystemFw_.Ast-import           LambdaCube.SystemFw_.TypeChecker (reduceType)--substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm-substituteNormal n v = go n-  where-    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b-    go m (LCNormNeut nt) = substituteNeutral m v nt--substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm-substituteNeutral n v = go n-  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 -> substituteNormal 0 a' b-        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'-      where-        a' = substituteNormal m v a+import           LambdaCube.SystemFw_.Substitution+import           LambdaCube.SystemFw_.TypeChecker  (reduceType)  normalize :: LCTerm -> LCNormalTerm normalize = go@@ -27,7 +11,7 @@     go (LCLam t b) = LCNormLam (reduceType t) $ go b     go (LCApp f a) =       case go f of-        LCNormLam _ b   -> substituteNormal 0 a' b+        LCNormLam _ b   -> substituteNormalInNormal 0 a' b         LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'       where         a' = go a
src/LambdaCube/SystemFw_/Parser.hs view
@@ -2,6 +2,7 @@  import           Data.Foldable            (Foldable (foldl')) import           Data.Functor             (($>))+import qualified Data.Text                as Text import           LambdaCube.Common.Parser import           LambdaCube.SystemFw_.Ast import           Text.Megaparsec@@ -23,8 +24,14 @@ pApp = foldl' ExtLCApp <$> pATerm <*> many pATerm  pATerm :: Parser ExtLCTerm-pATerm = (ExtLCVar <$> identifier) <|> parenthesized pLC+pATerm = pVar <|> pMVar <|> parenthesized pLC +pVar :: Parser ExtLCTerm+pVar = ExtLCVar <$> identifier++pMVar :: Parser ExtLCTerm+pMVar = ExtLCMVar <$> (dollarsign *> fmap Text.unpack identifier)+ pType :: Parser ExtLCType pType = pTTLam <|> pArr @@ -42,10 +49,25 @@ pTTApp = foldl' ExtLCTTApp <$> pAType <*> many pAType  pAType :: Parser ExtLCType-pAType = (sharp $> ExtLCBase) <|> (ExtLCTVar <$> identifier) <|> parenthesized pType+pAType = pBase <|> pTVar <|> pMTVar <|> parenthesized pType -pKind :: Parser LCKind-pKind = foldr1 LCKArr <$> sepBy1 pAKind rightArrow+pBase :: Parser ExtLCType+pBase = sharp $> ExtLCBase -pAKind :: Parser LCKind-pAKind = (asterisk $> LCStar) <|> parenthesized pKind+pTVar :: Parser ExtLCType+pTVar = ExtLCTVar <$> identifier++pMTVar :: Parser ExtLCType+pMTVar = ExtLCMTVar <$> (dollarsign *> fmap Text.unpack identifier)++pKind :: Parser ExtLCKind+pKind = foldr1 ExtLCKArr <$> sepBy1 pAKind rightArrow++pAKind :: Parser ExtLCKind+pAKind = pStar <|> pMKVar <|> parenthesized pKind++pStar :: Parser ExtLCKind+pStar = asterisk $> ExtLCStar++pMKVar :: Parser ExtLCKind+pMKVar = ExtLCMKVar <$> (dollarsign *> fmap Text.unpack identifier)
src/LambdaCube/SystemFw_/PrettyPrinter.hs view
@@ -9,25 +9,25 @@ import           LambdaCube.Common.PrettyPrinter import           LambdaCube.SystemFw_.Ast -prettyKind :: LCKind -> Text-prettyKind = prettyKindPrec 0+prettyUnnamedKind :: LCKind -> Text+prettyUnnamedKind = prettyUnnamedKindPrec 0 -prettyType :: LCType -> Text-prettyType = prettyTypePrec 0+prettyUnnamedType :: LCType -> Text+prettyUnnamedType = prettyUnnamedTypePrec 0 -prettyTerm :: LCTerm -> Text-prettyTerm = prettyTermPrec 0+prettyUnnamedTerm :: LCTerm -> Text+prettyUnnamedTerm = prettyUnnamedTermPrec 0 -prettyKindPrec :: Int -> LCKind -> Text-prettyKindPrec = go+prettyUnnamedKindPrec :: Int -> LCKind -> Text+prettyUnnamedKindPrec = go   where     go _ LCStar       = "*"     go p (LCKArr a b) = wrapIfSpaced (p > 0) [go 1 a, "->", go 0 b] -prettyTypePrec :: Int -> LCType -> Text-prettyTypePrec = go+prettyUnnamedTypePrec :: Int -> LCType -> Text+prettyUnnamedTypePrec = go   where-    pKP = prettyKindPrec+    pKP = prettyUnnamedKindPrec      go _ LCBase        = "#"     go _ (LCTVar i)    = Text.pack $ show i@@ -35,10 +35,10 @@     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] -prettyTermPrec :: Int -> LCTerm -> Text-prettyTermPrec = go+prettyUnnamedTermPrec :: Int -> LCTerm -> Text+prettyUnnamedTermPrec = go   where-    pTP = prettyTypePrec+    pTP = prettyUnnamedTypePrec      go _ (LCVar i)   = Text.pack $ show i     go p (LCLam t b) = wrapIfSpaced (p > 0) ["\\ :", pTP 0 t, ".", go 0 b]
+ src/LambdaCube/SystemFw_/Substitution.hs view
@@ -0,0 +1,37 @@+module LambdaCube.SystemFw_.Substitution where++import           LambdaCube.SystemFw_.Ast+import           LambdaCube.SystemFw_.Lifter++substituteTypeInType :: Int -> LCType -> LCType -> LCType+substituteTypeInType n v = go n+  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 (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)++substituteNormalInNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm+substituteNormalInNormal n v = go n+  where+    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b+    go m (LCNormNeut nt) = substituteNormalInNeutral m v nt++substituteNormalInNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm+substituteNormalInNeutral n v = go n+  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
src/LambdaCube/SystemFw_/TH.hs view
@@ -1,44 +1,49 @@-module LambdaCube.SystemFw_.TH where+module LambdaCube.SystemFw_.TH+  ( lc+  ) where -import           Control.Monad                   ((<=<))-import qualified Data.Text                       as Text+import           Data.Data                   (Data)+import           Data.Generics               (extQ)+import           Data.Text                   (Text)+import qualified Data.Text                   as Text import           LambdaCube.SystemFw_.Ast-import           LambdaCube.SystemFw_.Elaborator import           LambdaCube.SystemFw_.Parser-import           Language.Haskell.TH.Quote       (QuasiQuoter (..))-import           Language.Haskell.TH.Syntax      (Loc (loc_start), Q, lift,-                                                  location)-import qualified Text.Megaparsec                 as P-import qualified Text.Megaparsec.Error           as PE+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 -systemFw_ :: QuasiQuoter-systemFw_ =+lc :: QuasiQuoter+lc =   QuasiQuoter-    { quoteExp = lift <=< systemFw_QuoteExp+    { quoteExp = expLc     , quotePat = undefined     , quoteType = undefined     , quoteDec = undefined     } -systemFw_QuoteExp :: String -> Q ExtLCTerm-systemFw_QuoteExp str = do+expLc :: String -> ExpQ+expLc str = do   l <- location   case P.parse pTopLC ("<quote at " <> show (loc_start l) <> ">") (Text.pack str) of-    Right e  -> pure e+    Right e  -> dataToExpQ converter e     Left err -> fail $ PE.errorBundlePretty err+  where+    converter :: Data b => b -> Maybe ExpQ+    converter =+      const Nothing+      `extQ` quotedMVar+      `extQ` quotedMTVar+      `extQ` quotedMKVar+      `extQ` (Just . lift :: Text -> Maybe ExpQ) -elaboratedSystemFw_ :: QuasiQuoter-elaboratedSystemFw_ =-  QuasiQuoter-    { quoteExp = lift <=< elaboratedSystemFw_QuoteExp-    , quotePat = undefined-    , quoteType = undefined-    , quoteDec = undefined-    }+    quotedMVar (ExtLCMVar x) = Just . varE $ mkName x+    quotedMVar _             = Nothing -elaboratedSystemFw_QuoteExp :: String -> Q LCTerm-elaboratedSystemFw_QuoteExp str = do-  e <- systemFw_QuoteExp str-  case elaborate e of-    Right e' -> pure e'-    Left err -> fail err+    quotedMTVar (ExtLCMTVar x) = Just . varE $ mkName x+    quotedMTVar _              = Nothing++    quotedMKVar (ExtLCMKVar x) = Just . varE $ mkName x+    quotedMKVar _              = Nothing
src/LambdaCube/SystemFw_/TypeChecker.hs view
@@ -1,16 +1,8 @@ module LambdaCube.SystemFw_.TypeChecker where -import           Data.List                (uncons)+import           Data.List                         (uncons) import           LambdaCube.SystemFw_.Ast--substituteTypeInType :: Int -> LCType -> LCType -> LCType-substituteTypeInType n v = go n-  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 (LCTTLam k b) = LCTTLam k $ go (m + 1) b-    go m (LCTTApp f a) = go m f `LCTTApp` go m a+import           LambdaCube.SystemFw_.Substitution  reduceType :: LCType -> LCType reduceType = go@@ -26,41 +18,39 @@       | otherwise       = error "Did you really kind check this?" -infer :: LCTerm -> Maybe LCType+infer :: LCTerm -> LCType infer = go []   where-    go tl (LCVar n) = fmap fst . uncons $ drop n tl+    go tl (LCVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n tl     go tl (LCLam t b)-      | Just LCStar <- inferKind t-      = LCArr v <$> go (v : tl) b+      | LCStar <- inferKind t+      = v `LCArr` go (v : tl) b       | otherwise-      = Nothing+      = error "Function argument kind mismatch"       where         v = reduceType t     go tl (LCApp f a)-      | Just (LCArr at' rt) <- go tl f-      , Just at <- go tl a-      , at == at'-      = Just rt+      | LCArr at rt <- go tl f+      , at == go tl a+      = rt       | otherwise-      = Nothing+      = error "Function argument type mismatch" -inferKind :: LCType -> Maybe LCKind+inferKind :: LCType -> LCKind inferKind = go []   where-    go _  LCBase = Just LCStar-    go kl (LCTVar n) = fmap fst . uncons $ drop n kl+    go _  LCBase = LCStar+    go kl (LCTVar n) = maybe (error "Out-of-scope variable") fst . uncons $ drop n kl     go kl (LCArr a b)-      | Just LCStar <- go kl a-      , Just LCStar <- go kl b-      = Just LCStar+      | LCStar <- go kl a+      , LCStar <- go kl b+      = LCStar       | otherwise-      = Nothing-    go kl (LCTTLam k b) = LCKArr k <$> go (k : kl) b+      = error "Arrow kind mismatch"+    go kl (LCTTLam k b) = k `LCKArr` go (k : kl) b     go kl (LCTTApp f a)-      | Just (LCKArr ak' rk) <- go kl f-      , Just ak <- go kl a-      , ak == ak'-      = Just rk+      | LCKArr ak rk <- go kl f+      , ak == go kl a+      = rk       | otherwise-      = Nothing+      = error "Function argument kind mismatch"