From 541baf317c36923cf701598669a4f5e3ef012028 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 20 Feb 2021 13:25:26 +0300 Subject: [PATCH 01/10] Add simple syntax based on bound --- rzk/package.yaml | 4 +- rzk/rzk.cabal | 20 +- rzk/src/Rzk/Debug/Trace.hs | 49 +- rzk/src/Rzk/Simple/Evaluator.hs | 121 +++++ rzk/src/Rzk/Simple/Parser.hs | 609 ++++++++++++++++++++++ rzk/src/Rzk/Simple/Pretty.hs | 187 +++++++ rzk/src/Rzk/Simple/Syntax/Term.hs | 165 ++++++ rzk/src/Rzk/Simple/Syntax/Term/Example.hs | 5 + rzk/src/Rzk/Simple/Syntax/Var.hs | 44 ++ 9 files changed, 1154 insertions(+), 50 deletions(-) create mode 100644 rzk/src/Rzk/Simple/Evaluator.hs create mode 100644 rzk/src/Rzk/Simple/Parser.hs create mode 100644 rzk/src/Rzk/Simple/Pretty.hs create mode 100644 rzk/src/Rzk/Simple/Syntax/Term.hs create mode 100644 rzk/src/Rzk/Simple/Syntax/Term/Example.hs create mode 100644 rzk/src/Rzk/Simple/Syntax/Var.hs diff --git a/rzk/package.yaml b/rzk/package.yaml index c1b3b62d2..2e0356466 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -24,12 +24,14 @@ ghc-options: dependencies: - base >= 4.7 && < 5 -- attoparsec +- bound +- deriving-compat - mtl - text - parsers - trifecta - unordered-containers +- prettyprinter - prettyprinter-ansi-terminal - ansi-terminal diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index db5317cda..87059f614 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -4,7 +4,7 @@ cabal-version: 1.12 -- -- see: https://github.com/sol/hpack -- --- hash: e760f59aaadc2bd161f827d734c81167c3e8e0790d0530ac586b799327784473 +-- hash: 377d77461ef09bbb3140b2714aef9a45be530905fd1e4b0dccbea665ac85bc38 name: rzk version: 0.1.0.0 @@ -31,6 +31,12 @@ library Rzk.Evaluator Rzk.Parser.Text Rzk.Pretty.Text + Rzk.Simple.Evaluator + Rzk.Simple.Parser + Rzk.Simple.Pretty + Rzk.Simple.Syntax.Term + Rzk.Simple.Syntax.Term.Example + Rzk.Simple.Syntax.Var Rzk.Syntax.Decl Rzk.Syntax.Module Rzk.Syntax.Term @@ -43,10 +49,12 @@ library ghc-options: -Wall -fno-warn-type-defaults -O2 build-depends: ansi-terminal - , attoparsec , base >=4.7 && <5 + , bound + , deriving-compat , mtl , parsers + , prettyprinter , prettyprinter-ansi-terminal , text , trifecta @@ -62,10 +70,12 @@ executable rzk ghc-options: -Wall -fno-warn-type-defaults -O2 -threaded -rtsopts -with-rtsopts=-N build-depends: ansi-terminal - , attoparsec , base >=4.7 && <5 + , bound + , deriving-compat , mtl , parsers + , prettyprinter , prettyprinter-ansi-terminal , rzk , text @@ -83,10 +93,12 @@ test-suite rzk-test ghc-options: -Wall -fno-warn-type-defaults -O2 -threaded -rtsopts -with-rtsopts=-N build-depends: ansi-terminal - , attoparsec , base >=4.7 && <5 + , bound + , deriving-compat , mtl , parsers + , prettyprinter , prettyprinter-ansi-terminal , rzk , text diff --git a/rzk/src/Rzk/Debug/Trace.hs b/rzk/src/Rzk/Debug/Trace.hs index 994bc335c..362f7fb22 100644 --- a/rzk/src/Rzk/Debug/Trace.hs +++ b/rzk/src/Rzk/Debug/Trace.hs @@ -4,9 +4,6 @@ {-# LANGUAGE TypeApplications #-} module Rzk.Debug.Trace where -import Data.IORef -import System.IO.Unsafe - import Data.Typeable import qualified Debug.Trace import System.Console.ANSI @@ -16,58 +13,20 @@ import Rzk.Pretty.Text () import Rzk.Syntax.Term import Rzk.Syntax.Var --- trace :: String -> b -> b --- trace = const id --- --- traceShow :: Show a => a -> b -> b --- traceShow = const id - -__GLOBAL_DEBUG_SCOPE_LEVEL :: IORef Int -__GLOBAL_DEBUG_SCOPE_LEVEL = unsafePerformIO (newIORef (-1)) - -incrementScope :: IO Int -incrementScope = do - modifyIORef __GLOBAL_DEBUG_SCOPE_LEVEL (+1) - readIORef __GLOBAL_DEBUG_SCOPE_LEVEL - -decrementScope :: IO Int -decrementScope = do - modifyIORef __GLOBAL_DEBUG_SCOPE_LEVEL (subtract 1) - readIORef __GLOBAL_DEBUG_SCOPE_LEVEL - -getScope :: IO Int -getScope = readIORef __GLOBAL_DEBUG_SCOPE_LEVEL - -scoped :: a -> a -scoped x = unsafePerformIO incrementScope `seq` x `seq` unsafePerformIO decrementScope `seq` x -{-# NOINLINE scoped #-} - -indentWithScope :: String -> String -indentWithScope s = replicate (unsafePerformIO getScope) '-' <> s -{-# NOINLINE indentWithScope #-} - -trace :: String -> a -> a -trace s x = scoped (Debug.Trace.trace (indentWithScope s) x) -{-# NOINLINE trace #-} - -traceShow :: Show a => a -> b -> b -traceShow x = trace (show x) -{-# NOINLINE traceShow #-} - unsafeTraceShowCoerce :: forall b a c. Show b => a -> c -> c -unsafeTraceShowCoerce = traceShow . (unsafeCoerce :: a -> b) +unsafeTraceShowCoerce = Debug.Trace.traceShow . (unsafeCoerce :: a -> b) traceShowCast :: forall b a c. (Typeable a, Typeable b, Show b) => String -> a -> c -> c -traceShowCast fallback = trace . maybe fallback show . (cast :: a -> Maybe b) +traceShowCast fallback = Debug.Trace.trace . maybe fallback show . (cast :: a -> Maybe b) traceShowCast' :: forall b a c. (Typeable a, Typeable b, Show b) => b -> a -> c -> c traceShowCast' fallback = traceShowCast @b (show fallback) traceShowCast_ :: forall b a c. (Typeable a, Typeable b, Show b) => a -> c -> c -traceShowCast_ = maybe id traceShow . (cast :: a -> Maybe b) +traceShowCast_ = maybe id Debug.Trace.traceShow . (cast :: a -> Maybe b) traceShowTag :: Show a => String -> a -> b -> b -traceShowTag tag x = trace (colored [SetColor Foreground Dull White] ("[" <> tag <> "] ") <> show x) +traceShowTag tag x = Debug.Trace.trace (colored [SetColor Foreground Dull White] ("[" <> tag <> "] ") <> show x) traceTerm :: String -> Term Var -> a -> a traceTerm = traceShowTag diff --git a/rzk/src/Rzk/Simple/Evaluator.hs b/rzk/src/Rzk/Simple/Evaluator.hs new file mode 100644 index 000000000..75a67ad7c --- /dev/null +++ b/rzk/src/Rzk/Simple/Evaluator.hs @@ -0,0 +1,121 @@ +{-# LANGUAGE LambdaCase #-} +module Rzk.Simple.Evaluator where + +import Bound +import Rzk.Simple.Syntax.Term + +nfScoped :: Scope b (Term var) a -> Scope b (Term var) a +nfScoped = Scope . nf . unscope + +nf :: Term var a -> Term var a +nf = \case + App t1 t2 -> + case whnf t1 of + Lambda _a _phi body -> nf (instantiate1 t2 body) + t1' -> App (nf t1') (nf t2) + + First t -> + case whnf t of + Pair t1 _t2 -> nf t1 + t' -> nf t' + Second t -> + case whnf t of + Pair _t1 t2 -> nf t2 + t' -> nf t' + + IdJ tA a tC d x p -> + case whnf p of + Refl{} -> nf d + p' -> IdJ (nf tA) (nf a) (nf tC) (nf d) (nf x) (nf p') + + e@Variable{} -> e + e@Universe -> e + + ExtensionType tC psi tA phi a -> + ExtensionType (nf tC) (nfScoped psi) (nfScoped tA) (nfScoped phi) (nfScoped a) + Pi t' -> Pi (nf t') + Lambda a phi body + -> Lambda (fmap nf a) (fmap nfScoped phi) (nfScoped body) + + Sigma t' -> Sigma (nf t') + Pair t1 t2 -> Pair (nf t1) (nf t2) + + IdType a x y -> IdType (nf a) (nf x) (nf y) + Refl a x -> Refl (fmap nf a) (nf x) + + Cube -> Cube + CubeUnit -> CubeUnit + CubeUnitStar -> CubeUnitStar + + CubeProd t1 t2 -> CubeProd (nf t1) (nf t2) + + Tope -> Tope + TopeTop -> TopeTop + TopeBottom -> TopeBottom + TopeOr t1 t2 -> TopeOr (nf t1) (nf t2) + TopeAnd t1 t2 -> TopeAnd (nf t1) (nf t2) + TopeEQ t1 t2 -> TopeEQ (nf t1) (nf t2) + + RecBottom -> RecBottom + RecOr psi phi t1 t2 -> RecOr (nf psi) (nf phi) (nf t1) (nf t2) + + Cube2 -> Cube2 + Cube2_0 -> Cube2_0 + Cube2_1 -> Cube2_1 + + TopeLEQ t1 t2 -> TopeLEQ (nf t1) (nf t2) + +whnf :: Term var a -> Term var a +whnf = \case + App t1 t2 -> + case whnf t1 of + Lambda _a _phi body -> whnf (instantiate1 t2 body) + t1' -> App t1' t2 + + First t -> + case whnf t of + Pair t1 _t2 -> nf t1 + t' -> t' + Second t -> + case whnf t of + Pair _t1 t2 -> nf t2 + t' -> t' + + e@Variable{} -> e + e@Universe -> e + + ExtensionType tC psi tA phi a -> + ExtensionType (nf tC) (nfScoped psi) (nfScoped tA) (nfScoped phi) (nfScoped a) + Pi t' -> Pi (nf t') + e@Lambda{} -> e + + Sigma t' -> Sigma (nf t') + Pair t1 t2 -> Pair (nf t1) (nf t2) + + IdType a x y -> IdType (nf a) (nf x) (nf y) + Refl a x -> Refl (fmap nf a) (nf x) + IdJ tA a tC d x p -> IdJ (nf tA) (nf a) (nf tC) (nf d) (nf x) (nf p) + + Cube -> Cube + CubeUnit -> CubeUnit + CubeUnitStar -> CubeUnitStar + + CubeProd t1 t2 -> CubeProd (nf t1) (nf t2) + + Tope -> Tope + TopeTop -> TopeTop + TopeBottom -> TopeBottom + TopeOr t1 t2 -> TopeOr (nf t1) (nf t2) + TopeAnd t1 t2 -> TopeAnd (nf t1) (nf t2) + TopeEQ t1 t2 -> TopeEQ (nf t1) (nf t2) + + RecBottom -> RecBottom + RecOr psi phi t1 t2 -> RecOr (nf psi) (nf phi) (nf t1) (nf t2) + + + Cube2 -> Cube2 + Cube2_0 -> Cube2_0 + Cube2_1 -> Cube2_1 + + TopeLEQ t1 t2 -> TopeLEQ (nf t1) (nf t2) + diff --git a/rzk/src/Rzk/Simple/Parser.hs b/rzk/src/Rzk/Simple/Parser.hs new file mode 100644 index 000000000..acb809678 --- /dev/null +++ b/rzk/src/Rzk/Simple/Parser.hs @@ -0,0 +1,609 @@ +{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-unused-do-bind #-} +{-# LANGUAGE ApplicativeDo #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeSynonymInstances #-} +module Rzk.Simple.Parser where + +import Bound.Name +import Control.Applicative +import Data.Char (isPrint, isSpace) +import qualified Data.HashSet as HashSet +import Data.String (IsString (..)) +import Data.Text (Text) +import qualified Data.Text as Text +import Data.Text.Prettyprint.Doc.Render.Terminal (putDoc) +import System.IO.Unsafe + +import Text.Parser.Expression +import Text.Parser.Token +import Text.Parser.Token.Style (emptyIdents) +import Text.Trifecta + +import Rzk.Simple.Syntax.Term +import Rzk.Simple.Syntax.Var + +type RzkParser = Unlined Parser + +-- ** Term + +rzkVar :: RzkParser Var +rzkVar = Var <$> rzkIdent + +rzkTerm :: RzkParser (Term Var Var) +rzkTerm = "term" + buildExpressionParser rzkOperatorTable rzkTerm' + +rzkTerm' :: RzkParser (Term Var Var) +rzkTerm' = "simple term" + try rzkTermPiType + <|> rzkTermPiShape + <|> try rzkTermPair + <|> parens rzkTerm + <|> try rzkTermLambda + <|> try rzkTermLambdaShape + <|> rzkTermSigmaType + <|> rzkTermRefl + <|> rzkTermIdJ + <|> rzkTermRecOr + <|> rzkTermFirst + <|> rzkTermSecond + <|> rzkTermExtensionType + <|> rzkTermExtensionTypeFromCube + -- constants + <|> Universe <$ (symbol "U" <|> symbol "𝒰") + <|> Cube <$ symbol "CUBE" + <|> CubeUnitStar <$ (symbol "*_1" <|> symbol "⋆") + <|> Cube2 <$ (symbol "2" <|> symbol "𝟚") + <|> Cube2_0 <$ symbol "0_2" + <|> Cube2_1 <$ symbol "1_2" + <|> CubeUnit <$ (symbol "1" <|> symbol "πŸ™") + <|> Tope <$ symbol "TOPE" + <|> TopeTop <$ (symbol "TOP" <|> symbol "⊀") + <|> TopeBottom <$ (symbol "BOT" <|> symbol "βŠ₯") + <|> RecBottom <$ (symbol "recBOT" <|> symbol "recβŠ₯") + <|> rzkTermVar + +rzkTermVar :: RzkParser (Term Var Var) +rzkTermVar = "variable" + (Variable <$> (Var <$> rzkIdent)) + +rzkTermColonType :: RzkParser (Term Var Var, Term Var Var) +rzkTermColonType = do + term <- rzkTerm + colon + type_ <- rzkTerm + return (term, type_) + +rzkTermColonType' :: RzkParser (Term Var Var, Maybe (Term Var Var)) +rzkTermColonType' = try withType <|> withoutType + where + withType = fmap Just <$> rzkTermColonType + withoutType = (\t -> (t, Nothing)) <$> rzkTerm + +rzkVarColonType' :: RzkParser (Var, Maybe (Term Var Var)) +rzkVarColonType' = try withType <|> withoutType + where + withType = fmap Just <$> parens rzkVarColonType + withoutType = (\x -> (Var x, Nothing)) <$> rzkIdent + +rzkVarColonType :: RzkParser (Var, Term Var Var) +rzkVarColonType = do + x <- Var <$> rzkIdent + colon + type_ <- rzkTerm + return (x, type_) + +rzkTermPiType :: RzkParser (Term Var Var) +rzkTermPiType = "dependent function type" do + (var, a) <- parens rzkVarColonType + symbol "->" <|> symbol "β†’" + t <- rzkTerm + return (Pi (Lambda (Just a) Nothing (abstract1Name var t))) + +rzkTermPiShape :: RzkParser (Term Var Var) +rzkTermPiShape = "dependent function type (from a shape)" do + symbol "{" + (var, i) <- rzkVarColonType' + symbol "|" + phi <- rzkTerm + symbol "}" + symbol "->" <|> symbol "β†’" + a <- rzkTerm + return (Pi (Lambda i (Just (abstract1Name var phi)) (abstract1Name var a))) + +rzkTermLambda :: RzkParser (Term Var Var) +rzkTermLambda = "lambda abstraction (anonymous function from a type)" do + symbol "Ξ»" <|> symbol "\\" + (x, a) <- rzkVarColonType' + symbol "->" <|> symbol "β†’" + t <- rzkTerm + return (Lambda a Nothing (abstract1Name x t)) + +rzkTermLambdaShape :: RzkParser (Term Var Var) +rzkTermLambdaShape = "lambda abstraction (anonymous function from a shape)" do + symbol "Ξ»" <|> symbol "\\" + symbol "{" + (t, i) <- rzkVarColonType + symbol "|" + phi <- rzkTerm + symbol "}" + symbol "->" <|> symbol "β†’" + a <- rzkTerm + return (Lambda (Just i) (Just (abstract1Name t phi)) (abstract1Name t a)) + +rzkTermSigmaType :: RzkParser (Term Var Var) +rzkTermSigmaType = "dependent sum type" do + symbol "βˆ‘" <|> symbol "Sigma" + (x, a) <- parens rzkVarColonType + symbol "," + t <- rzkTerm + return (Sigma (Lambda (Just a) Nothing (abstract1Name x t))) + +rzkTermRefl :: RzkParser (Term Var Var) +rzkTermRefl = do + symbol "refl_{" + (x, a) <- rzkTermColonType' + symbol "}" + return (Refl a x) + +rzkTermIdJ :: RzkParser (Term Var Var) +rzkTermIdJ = do + symbol "idJ" + symbol "(" + tA <- rzkTerm <* comma + a <- rzkTerm <* comma + tC <- rzkTerm <* comma + d <- rzkTerm <* comma + x <- rzkTerm <* comma + p <- rzkTerm + symbol ")" + return (IdJ tA a tC d x p) + +rzkTermRecOr :: RzkParser (Term Var Var) +rzkTermRecOr = do + symbol "recOR" <|> symbol "rec∨" + symbol "(" + psi <- rzkTerm <* comma + phi <- rzkTerm <* comma + a <- rzkTerm <* comma + b <- rzkTerm + symbol ")" + return (RecOr psi phi a b) + +rzkTermFirst :: RzkParser (Term Var Var) +rzkTermFirst = do + (symbol "first" <|> symbol "π₁") "π₁" + First <$> rzkTerm + +rzkTermSecond :: RzkParser (Term Var Var) +rzkTermSecond = do + (symbol "second" <|> symbol "Ο€β‚‚") "Ο€β‚‚" + Second <$> rzkTerm + +rzkTermExtensionTypeFromCube :: RzkParser (Term Var Var) +rzkTermExtensionTypeFromCube = between (symbol "<(") (symbol ">") $ do + t <- rzkVar + symbol ":" + cI <- rzkTerm + symbol ")" + symbol "->" <|> symbol "β†’" + tA <- rzkTerm + mphi_a <- optional $ do + symbol "[" + phi <- rzkTerm + symbol "|->" + a <- rzkTerm + symbol "]" + return (phi, a) + let (phi, a) = case mphi_a of + Just x -> x + Nothing -> (TopeBottom, RecBottom) + return (ExtensionType cI (abstract1Name t TopeTop) (abstract1Name t tA) (abstract1Name t phi) (abstract1Name t a)) + + +rzkTermExtensionType :: RzkParser (Term Var Var) +rzkTermExtensionType = between (symbol "<{") (symbol ">") $ do + t <- rzkVar + symbol ":" + cI <- rzkTerm + symbol "|" + psi <- rzkTerm + symbol "}" + symbol "->" <|> symbol "β†’" + tA <- rzkTerm + mphi_a <- optional $ do + symbol "[" + phi <- rzkTerm + symbol "|->" + a <- rzkTerm + symbol "]" + return (phi, a) + let (phi, a) = case mphi_a of + Just x -> x + Nothing -> (TopeBottom, RecBottom) + return (ExtensionType cI (abstract1Name t psi) (abstract1Name t tA) (abstract1Name t phi) (abstract1Name t a)) + +-- firstP :: Parser (Term Var Var) +-- firstP = do +-- "first" <|> "π₁" +-- skipSpace +-- First <$> termParens True +-- +-- secondP :: Parser (Term Var Var) +-- secondP = do +-- "second" <|> "Ο€β‚‚" +-- skipSpace +-- Second <$> termParens True + +rzkTermPair :: RzkParser (Term Var Var) +rzkTermPair = parens (Pair <$> rzkTerm <* comma <*> rzkTerm) + +rzkTermApp :: RzkParser (Term Var Var) +rzkTermApp = do + t1 <- rzkTerm + t2 <- rzkTerm + return (App t1 t2) + +rzkOperator :: RzkParser a -> RzkParser a +rzkOperator op = op -- <* skipMany (satisfy isSpace) + +rzkOperatorTable :: OperatorTable RzkParser (Term Var Var) +rzkOperatorTable = + [ [ Infix (pure App) AssocLeft ] + , [ Infix (CubeProd <$ rzkOperator (symbol "*" <|> symbol "Γ—")) AssocLeft ] + , [ Infix (TopeEQ <$ rzkOperator (symbol "===" <|> symbol "≑")) AssocNone + , Infix (TopeLEQ <$ rzkOperator (symbol "<=" <|> symbol "≀")) AssocNone ] + , [ Infix (TopeAnd <$ rzkOperator (symbol "/\\" <|> symbol "∧")) AssocLeft ] + , [ Infix (TopeOr <$ rzkOperator (symbol "\\/" <|> symbol "∨")) AssocLeft ] + , [ Infix (rzkOperator $ do + { symbol "=_{" ; + t <- rzkTerm ; + symbol "}" ; + return (IdType t) + }) AssocNone] + ] + +-- ** Identifiers + +rzkIdent :: RzkParser Text +rzkIdent = Text.pack <$> ident rzkIdentStyle + +rzkIdentStyle :: IdentifierStyle RzkParser +rzkIdentStyle = (emptyIdents @RzkParser) + { _styleStart = satisfy isIdentChar + , _styleLetter = satisfy isIdentChar + , _styleReserved = HashSet.fromList + [ "data", "where", "let" + , "if", "then", "else" + , ":", ":=", "." + , "\\", "->" + , "=_", "=_{" + , "*" + , "/\\" + , "\\/" + , "<=" + , "===" + , "=>", "β‡’" + , "U" + , "recBOT" + , "BOT" + , "TOP" + , "CUBE" + , "TOPE" + , "βˆ‘", "Sigma" + , "refl_", "refl_{" + , "```" + , "<", ">" , "|->", "|" + ] + } + +-- ** Char predicates + +isIdentChar :: Char -> Bool +isIdentChar c = isPrint c && not (isSpace c) && not (isDelim c) + +isDelim :: Char -> Bool +isDelim c = c `elem` ("()[]{}," :: String) + +-- * Orphan 'IsString' instances + +instance IsString (Term Var Var) where + fromString = unsafeParseTerm + +unsafeParseTerm :: String -> Term Var Var +unsafeParseTerm = unsafeParseString rzkTerm + +unsafeParseString :: RzkParser a -> String -> a +unsafeParseString parser input = + case parseString (runUnlined parser) mempty input of + Success x -> x + Failure errInfo -> unsafePerformIO $ do + putDoc (_errDoc errInfo <> "\n") + error "Parser error while attempting unsafeParseString" + +-- +-- module_ :: Parser (Module Var) +-- module_ = do +-- moduleDecls <- decl `Atto.sepBy` (skipSpace >> Atto.many1 Atto.endOfLine) +-- return Module{..} +-- +-- decl :: Parser (Decl Var) +-- decl = do +-- declName <- var +-- skipSpace >> ":" >> skipSpace +-- declType <- term +-- Atto.skipSpace >> ":=" >> skipSpace +-- declBody <- term +-- return Decl{..} +-- +-- term :: Parser (Term Var Var) +-- term = termParens False +-- +-- termParens :: Bool -> Parser (Term Var Var) +-- termParens useParens +-- = termParens' useParens +-- <|> parens (termParens useParens) +-- +-- termParens' :: Bool -> Parser (Term Var Var) +-- termParens' useParens +-- = parens' idType +-- <|> parens' firstP <|> parens' secondP +-- <|> parens' idJ +-- <|> parens' recOr +-- <|> parens' cubeProd +-- <|> parens' constrainedType +-- <|> refl +-- <|> recBottom +-- <|> cubeU <|> topeU <|> universe +-- <|> topeTop <|> topeBottom +-- <|> cubeUnit <|> cubeUnitStar +-- <|> parens' piApp +-- <|> piType <|> sigmaType +-- <|> pair +-- <|> parens' piLambda +-- <|> parens' topeOr -- FIXME: slow +-- <|> parens' topeAnd -- FIXME: slow +-- <|> parens' topeEQ -- FIXME: slow +-- <|> hole <|> (Variable <$> var) +-- where +-- parens' = if useParens then parens else id +-- +-- parseTuple :: Parser [Term Var Var] +-- parseTuple +-- = "(" *> skipSpace *> Atto.sepBy1 term (skipSpace *> "," <* skipSpace) <* skipSpace <* ")" +-- +-- cubeU :: Parser (Term var) +-- cubeU = Cube <$ "CUBE" +-- +-- topeU :: Parser (Term var) +-- topeU = Tope <$ "TOPE" +-- +-- cubeUnit :: Parser (Term var) +-- cubeUnit = CubeUnit <$ "1" +-- +-- cubeUnitStar :: Parser (Term var) +-- cubeUnitStar = CubeUnit <$ ("*_1" <|> "⋆") +-- +-- cubeProd :: Parser (Term Var Var) +-- cubeProd = do +-- i <- termParens True +-- skipSpace +-- "Γ—" <|> "*" +-- skipSpace +-- j <- termParens True +-- return (CubeProd i j) +-- +-- topeTop :: Parser (Term var) +-- topeTop = TopeTop <$ ("TOP" <|> "⊀") +-- +-- topeBottom :: Parser (Term var) +-- topeBottom = TopeBottom <$ ("BOT" <|> "βŠ₯") +-- +-- topeOr :: Parser (Term Var Var) +-- topeOr = do +-- phi <- termParens True +-- skipSpace +-- "\\/" <|> "∨" +-- skipSpace +-- psi <- termParens True +-- return (TopeOr phi psi) +-- +-- topeAnd :: Parser (Term Var Var) +-- topeAnd = do +-- phi <- termParens True +-- skipSpace +-- "/\\" <|> "∧" +-- skipSpace +-- psi <- termParens True +-- return (TopeAnd phi psi) +-- +-- topeEQ :: Parser (Term Var Var) +-- topeEQ = do +-- t <- termParens True +-- skipSpace +-- "===" <|> "≑" +-- skipSpace +-- s <- termParens True +-- return (TopeEQ t s) +-- +-- recBottom :: Parser (Term Var Var) +-- recBottom = RecBottom <$ ("recBOT" <|> "recβŠ₯") +-- +-- recOr :: Parser (Term Var Var) +-- recOr = do +-- "recOR" <|> "rec∨" +-- [psi, phi, a, b] <- parseTuple +-- return (RecOr psi phi a b) +-- +-- constrainedType :: Parser (Term Var Var) +-- constrainedType = do +-- phi <- termParens True +-- skipSpace +-- "=>" +-- skipSpace +-- a <- term +-- return (ConstrainedType phi a) +-- +-- parens :: Parser a -> Parser a +-- parens p = "(" *> skipSpace *> p <* skipSpace <* ")" +-- +-- piType :: Parser (Term Var Var) +-- piType = do +-- "{" +-- skipSpace +-- x <- var "variable identifier" +-- skipSpace +-- ":" +-- skipSpace +-- a <- term "type" +-- skipSpace +-- "}" +-- skipSpace +-- "->" <|> "β†’" +-- skipSpace +-- b <- term "type" +-- return (Pi (Lambda x a b)) +-- +-- piLambda :: Parser (Term Var Var) +-- piLambda = do +-- "Ξ»" <|> "\\" +-- skipSpace +-- "(" +-- skipSpace +-- x <- var "variable identifier" +-- skipSpace +-- ":" +-- skipSpace +-- a <- term "type" +-- skipSpace +-- ")" +-- skipSpace +-- "->" <|> "β†’" +-- skipSpace +-- t <- term "term" +-- return (Lambda x a t) +-- +-- piApp :: Parser (Term Var Var) +-- piApp = do +-- t1 <- termParens True +-- skipSpace +-- t2 <- termParens True +-- return (App t1 t2) +-- +-- sigmaType :: Parser (Term Var Var) +-- sigmaType = do +-- "Sigma" <|> "βˆ‘" +-- skipSpace +-- "(" +-- skipSpace +-- x <- var "variable identifier" +-- skipSpace +-- ":" +-- skipSpace +-- a <- term "type" +-- skipSpace +-- ")" +-- skipSpace +-- "," +-- skipSpace +-- b <- term "type" +-- return (Sigma (Lambda x a b)) +-- +-- pair :: Parser (Term Var Var) +-- pair = do +-- "(" +-- skipSpace +-- f <- term +-- skipSpace +-- "," +-- skipSpace +-- s <- term +-- skipSpace +-- ")" +-- return (Pair f s) +-- +-- firstP :: Parser (Term Var Var) +-- firstP = do +-- "first" <|> "π₁" +-- skipSpace +-- First <$> termParens True +-- +-- secondP :: Parser (Term Var Var) +-- secondP = do +-- "second" <|> "Ο€β‚‚" +-- skipSpace +-- Second <$> termParens True +-- +-- idType :: Parser (Term Var Var) +-- idType = do +-- x <- termParens True +-- skipSpace +-- "=_{" +-- skipSpace +-- a <- termParens False +-- skipSpace +-- "}" +-- skipSpace +-- y <- termParens True +-- return (IdType a x y) +-- +-- refl :: Parser (Term Var Var) +-- refl = do +-- "refl_{" +-- skipSpace +-- x <- term +-- skipSpace +-- ":" +-- skipSpace +-- a <- term +-- skipSpace +-- "}" +-- return (Refl a x) +-- +-- idJ :: Parser (Term Var Var) +-- idJ = do +-- "idJ" +-- [tA, a, tC, d, x, p] <- parseTuple +-- return (IdJ tA a tC d x p) +-- +-- universe :: Parser (Term Var Var) +-- universe = do +-- "U" <|> "𝒰" +-- return Universe +-- +-- hole :: Parser (Term Var Var) +-- hole = Hole <$> ("?" >> var) +-- +-- var :: Parser Var +-- var = do +-- first <- Atto.satisfy (Atto.inClass (letters <> "_")) +-- rest <- Atto.takeWhile (Atto.inClass (letters <> digits <> digitsSub <> "_")) +-- return (Var (Text.cons first rest)) +-- where +-- digits = "0123456789" +-- digitsSub = "β‚€β‚β‚‚β‚ƒβ‚„β‚…β‚†β‚‡β‚ˆβ‚‰" +-- +-- letters = latinSmall <> latinCapital <> greekSmall +-- latinSmall = "abcdefghijklmnopqrstuvwxyz" +-- latinCapital = "ABCDEFGHIJKLMNOPQRSTUVWXYZ" +-- greekSmall = "Ξ±Ξ²Ξ³Ξ΄Ξ΅ΞΆΞ·ΞΈΞΉΞΊΞ»ΞΌΞ½ΞΎΞΏΟ€ΟΟ‚ΟƒΟ„Ο…Ο†Ο‡ΟˆΟ‰" \\ "Ξ»" +-- +-- unsafeParse :: String -> Parser a -> Text -> a +-- unsafeParse name parser input = +-- case Atto.parseOnly (parser <* Atto.endOfInput) input of +-- Right t -> t +-- Left err -> error $ unlines +-- [ "Failed parsing " <> name +-- , " " <> Text.unpack input +-- , "Parsing error was:" +-- , err +-- ] +-- +-- skipSpace :: Parser () +-- skipSpace = Atto.skipWhile (Atto.inClass " \t") + +() :: Parsing m => String -> m a -> m a +() = flip () diff --git a/rzk/src/Rzk/Simple/Pretty.hs b/rzk/src/Rzk/Simple/Pretty.hs new file mode 100644 index 000000000..507c40eda --- /dev/null +++ b/rzk/src/Rzk/Simple/Pretty.hs @@ -0,0 +1,187 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +module Rzk.Simple.Pretty where + +import Bound.Scope (instantiate1) +import Data.Text.Prettyprint.Doc +import Data.Text.Prettyprint.Doc.Render.Terminal + +import Rzk.Simple.Syntax.Term +import Rzk.Simple.Syntax.Var + +data TypeOfTerm + = TermVariable + | TypeVariable + | TopeVariable + | CubeVariable + + | TermConstructor + | TypeConstructor + | TopeConstructor + | CubeConstructor + + | TermEliminator + | TypeEliminator + | TopeEliminator + | CubeEliminator + + | SomeTerm + | SomeType + | SomeTope + | SomeCube + + | Reserved + +highlightUsingAnsiStyle :: TypeOfTerm -> AnsiStyle +highlightUsingAnsiStyle = \case + TermVariable -> color White + TypeVariable -> color White + TopeVariable -> color White + CubeVariable -> color White + + TermConstructor -> color Green <> bold + TypeConstructor -> color Green <> bold + TopeConstructor -> color Green <> bold + CubeConstructor -> color Green <> bold + + TermEliminator -> color Magenta <> bold + TypeEliminator -> color Magenta <> bold + TopeEliminator -> color Magenta <> bold + CubeEliminator -> color Magenta <> bold + + SomeTerm -> mempty + SomeType -> mempty + SomeTope -> mempty + SomeCube -> mempty + + Reserved -> color Cyan + +ppTermANSI :: Show a => [Doc TypeOfTerm] -> Term var a -> Doc AnsiStyle +ppTermANSI vars = reAnnotate highlightUsingAnsiStyle . ppTerm vars . fmap viaShow + +ppTermParens :: [Doc TypeOfTerm] -> Term var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppTermParens vars = \case + t@Variable{} -> ppTerm vars t + t@Universe -> ppTerm vars t + t@Refl{} -> ppTerm vars t + t@Cube{} -> ppTerm vars t + t@CubeUnit{} -> ppTerm vars t + t@CubeUnitStar{} -> ppTerm vars t + t@Tope{} -> ppTerm vars t + t@TopeTop{} -> ppTerm vars t + t@TopeBottom{} -> ppTerm vars t + t@RecBottom{} -> ppTerm vars t + t@Cube2{} -> ppTerm vars t + t@Cube2_0{} -> ppTerm vars t + t@Cube2_1{} -> ppTerm vars t + t -> parens (ppTerm vars t) + +ppReserved :: Doc TypeOfTerm -> Doc TypeOfTerm +ppReserved = annotate Reserved + +ppTermCon :: Doc TypeOfTerm -> Doc TypeOfTerm +ppTermCon = annotate TermConstructor + +ppTypeCon :: Doc TypeOfTerm -> Doc TypeOfTerm +ppTypeCon = annotate TypeConstructor + +ppTopeCon :: Doc TypeOfTerm -> Doc TypeOfTerm +ppTopeCon = annotate TopeConstructor + +ppCubeCon :: Doc TypeOfTerm -> Doc TypeOfTerm +ppCubeCon = annotate CubeConstructor + +ppTermElim :: Doc TypeOfTerm -> Doc TypeOfTerm +ppTermElim = annotate TermEliminator + +ppTypeElim :: Doc TypeOfTerm -> Doc TypeOfTerm +ppTypeElim = annotate TypeEliminator + +ppTopeElim :: Doc TypeOfTerm -> Doc TypeOfTerm +ppTopeElim = annotate TopeEliminator + +ppCubeElim :: Doc TypeOfTerm -> Doc TypeOfTerm +ppCubeElim = annotate CubeEliminator + +ppScoped :: [Doc TypeOfTerm] -> Scope1Term var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppScoped [] = error "Not enough fresh variables!" +ppScoped (x:vars) = ppTerm vars . instantiate1 (Variable x) + +ppVar :: Doc TypeOfTerm -> Doc TypeOfTerm +ppVar = annotate TermVariable + +ppTypeVar :: Doc TypeOfTerm -> Doc TypeOfTerm +ppTypeVar = annotate TypeVariable + +ppTopeVar :: Doc TypeOfTerm -> Doc TypeOfTerm +ppTopeVar = annotate TopeVariable + +ppCubeVar :: Doc TypeOfTerm -> Doc TypeOfTerm +ppCubeVar = annotate CubeVariable + +ppElimWithArgs :: [Doc TypeOfTerm] -> Doc TypeOfTerm -> [Term var (Doc TypeOfTerm)] -> Doc TypeOfTerm +ppElimWithArgs vars elim args + = elim <> parens (hsep (punctuate comma (map (ppTerm vars) args))) + +ppTerm :: [Doc TypeOfTerm] -> Term var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppTerm vars = \case + Variable x -> ppVar x + App t1 t2 -> ppTerm vars t1 <+> ppTermParens vars t2 + First t -> ppTermElim "π₁" <+> ppTermParens vars t + Second t -> ppTermElim "Ο€β‚‚" <+> ppTermParens vars t + Universe -> ppTypeCon "𝒰 " + Pi (Lambda (Just a) Nothing m) -> + parens (ppTypeVar var <+> ":" <+> ppTerm vars a) <+> "β†’ " <+> ppScoped vars m + Pi (Lambda (Just a) (Just phi) m) -> + braces (ppTypeVar var <+> ":" <+> ppTerm vars a <+> "|" <+> ppScoped vars phi) <+> "β†’ " <+> ppScoped vars m + Pi t -> "Pi " <> ppTermParens vars t + Lambda (Just a) Nothing m + -> ppReserved "Ξ»" <> parens (ppVar var <+> ":" <+> ppTerm vars a) <+> "β†’ " <> ppScoped vars m + Lambda Nothing Nothing m + -> ppReserved "Ξ»" <> ppVar var <> " β†’ " <> ppScoped vars m + Lambda (Just a) (Just phi) m + -> ppReserved "Ξ»" <> braces (ppVar var <+> ":" <+> ppTerm vars a <+> "|" <+> ppScoped vars phi) <+> "β†’" <+> ppScoped vars m + Lambda Nothing (Just phi) m + -> ppReserved "Ξ»" <> braces (ppVar var <+> "|" <+> ppScoped vars phi) <+> "β†’" <+> ppScoped vars m + + Sigma (Lambda (Just a) Nothing m) + -> ppReserved "βˆ‘" <+> parens (ppTypeVar var <+> ":" <+> ppTerm vars a) <> comma <+> ppScoped vars m + Sigma t -> ppReserved "βˆ‘" <> ppTermParens vars t + Pair t1 t2 -> parens (ppTerm vars t1 <> comma <+> ppTerm vars t2) + + IdType a x y -> ppTermParens vars x <> " =_{" <> ppTerm vars a <> "} " <> ppTermParens vars y + Refl (Just a) x -> ppTermCon "refl" <> "_{" <> ppTerm vars x <> " : " <> ppTerm vars a <> "}" + Refl Nothing x -> ppTermCon "refl" <> "_{" <> ppTerm vars x <> "}" + IdJ tA a tC d x p -> ppElimWithArgs vars (ppTermElim "idJ") [tA, a, tC, d, x, p] + + Cube -> ppTypeCon "CUBE" + CubeUnit -> ppCubeCon "πŸ™" + CubeUnitStar -> ppTermCon "⋆" + CubeProd i j -> ppTermParens vars i <> " Γ— " <> ppTermParens vars j + + Tope -> ppTypeCon "TOPE" + TopeTop -> ppTopeCon "⊀" + TopeBottom -> ppTopeCon "βŠ₯" + TopeOr psi phi -> ppTermParens vars psi <> " ∨ " <> ppTermParens vars phi + TopeAnd psi phi -> ppTermParens vars psi <> " ∧ " <> ppTermParens vars phi + TopeEQ x y -> ppTermParens vars x <> " ≑ " <> ppTermParens vars y + + RecBottom -> ppTermCon "recβŠ₯" + RecOr psi phi a_psi a_phi + -> ppElimWithArgs vars (ppTermCon "rec∨") [psi, phi, a_psi, a_phi] + + ExtensionType cI psi tA phi a -> + "γ€ˆ" <> braces (ppCubeVar var <+> ":" <+> ppTerm vars cI <+> "|" <+> ppScoped vars psi) <+> "β†’" <+> ppScoped vars tA <> brackets (ppScoped vars phi <+> "↦" <+> ppScoped vars a) <> "〉" + + Cube2 -> ppCubeCon "𝟚" + Cube2_0 -> ppTermCon "0" + Cube2_1 -> ppTermCon "1" + TopeLEQ t s -> ppTermParens vars t <+> ppTopeCon "≀" <+> ppTermParens vars s + where + var:_ = vars + +pp :: Show a => Term var a -> IO () +pp t = putDoc (ppTermANSI vars t' <> "\n") + where + vars = (viaShow . Var) <$> zipWith appendIndexText [0..] (repeat "x") + t' = viaShow <$> t diff --git a/rzk/src/Rzk/Simple/Syntax/Term.hs b/rzk/src/Rzk/Simple/Syntax/Term.hs new file mode 100644 index 000000000..ae28e723e --- /dev/null +++ b/rzk/src/Rzk/Simple/Syntax/Term.hs @@ -0,0 +1,165 @@ +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE TemplateHaskell #-} +module Rzk.Simple.Syntax.Term where + +import Bound +import Bound.Name +import Control.Monad (ap) +import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, + deriveShow1) +import Data.Functor.Classes + +type Scope1 var = Scope (Name var ()) + +type Scope1Term var a = Scope1 var (Term var) a + +-- | This is a (probably unevaluated) term out of context. +data Term var a + = Variable a + -- ^ Term variable \(x_i\) or type variable \(A_i\) or cube variable \(t_i\) or tope variable \(\phi_i\). + + | Universe + -- ^ Universe type \(\mathcal{U}\). + -- Saying \(A \mathbf{type}\) is equivalent to saying \(A : \mathcal{U}\). + + | Pi (Term var a) + -- ^ Dependent product type former \(\prod_{x : A} B(x)\). + -- The term argument represents type family \(B : A \to \mathcal{U}\). + | Lambda (Maybe (Term var a)) (Maybe (Scope1Term var a)) (Scope1Term var a) + -- ^ \(\lambda\)-abstraction ("lambda abstraction"). + -- @Lambda x a Nothing m@ represents a term of the form \(\lambda (x : A). M\) + -- while @Lambda t i (Just phi) m@ represents \(\lambda \{t : I | \phi\}. M\) + | App (Term var a) (Term var a) + -- ^ Application of one term to another \((M N)\). + + | Sigma (Term var a) + -- ^ Dependent sum type former \(\sum_{x : A} B(x)\). + -- The term argument represents type family \(B : A \to \mathcal{U}\). + | Pair (Term var a) (Term var a) + -- ^ A (dependent) pair of terms. + -- @Pair x y@ represents a term of the form \((x, y)\). + | First (Term var a) + -- ^ Project the first element of a pair: \(\pi_1 p\). + | Second (Term var a) + -- ^ Project the second element of a pair: \(\pi_2 p\). + + | IdType (Term var a) (Term var a) (Term var a) + -- ^ Identity type former \(x =_A y\) (corresponding to term @IdType a x y@). + | Refl (Maybe (Term var a)) (Term var a) + -- ^ Trivial inhabitant of \(x =_A x\) for any type \(A\) and \(x : A\). + -- @Refl a x@ corresponds to \(x =_a x\). + | IdJ (Term var a) (Term var a) (Term var a) (Term var a) (Term var a) (Term var a) + -- ^ Path induction (for identity types). + -- For any type \(A\) and \(a : A\), type family + -- \(C : \prod_{x : A} ((a =_A x) \to \mathcal{U})\) + -- and \(d : C(a,\mathsf{refl}_a)\) + -- and \(x : A\) + -- and \(p : a =_A x\) + -- we have \(\mathcal{J}(A, a, C, d, x, p) : C(x, p)\). + + | Cube + -- ^ Cube "universe". Technically, it is not a type, but it is treated as such syntactically. + + | CubeUnit + -- ^ Unit cube: \(\mathbf{1}\;\mathsf{cube}\). + | CubeUnitStar + -- ^ The only point in the unit cube: \(\star : \mathbf{1}\). + + | CubeProd (Term var a) (Term var a) + -- ^ Product of cubes: \(I \times J\). + + | Tope + -- ^ Tope "universe". Like cubes, this is not a type. + | TopeTop + -- ^ Top tope (no constraints on cube): \(\top\;\mathsf{tope}\) + | TopeBottom + -- ^ Bottom tope (cube contrained to empty space): \(\bot\;\mathsf{tope}\) + | TopeOr (Term var a) (Term var a) + -- ^ Tope disjuction (union of shapes): \(\psi \lor \phi\;\mathsf{tope}\) + | TopeAnd (Term var a) (Term var a) + -- ^ Tope conjunction (intersection of shapes): \(\psi \land \phi\;\mathsf{tope}\) + | TopeEQ (Term var a) (Term var a) + -- ^ Equality tope (diagonals): \(t \equiv s \;\mathsf{tope}\). + -- Note that it can involve projections as well, e.g. \(\pi_1 t \equiv \pi_2 t\). + + | RecBottom + -- ^ Bottom tope eliminator: \(\mathsf{rec}_\bot : A\). + | RecOr (Term var a) (Term var a) (Term var a) (Term var a) + -- ^ Tope disjunction eliminator: \(\mathsf{rec}^{\psi,\phi}_\lor(a_\psi, a_\phi)\). + + | ExtensionType + (Term var a) (Scope1Term var a) (Scope1Term var a) (Scope1Term var a) (Scope1Term var a) + -- ^ Extension type \( \left\langle \prod_{t : I | psi} A(t) \rvert^{\phi}_{a(t)} \right\rangle \) corresponding to @ExtensionType t cI psi tA phi a@. + + | Cube2 + -- ^ Directed interval cube: \(\mathbb{2}\). + | Cube2_0 + -- ^ Start of directed interval: \(0 : \mathbb{2}\). + | Cube2_1 + -- ^ End of directed interval: \(1 : \mathbb{2}\). + + | TopeLEQ (Term var a) (Term var a) + -- ^ Inequality tope: \(t \leq s\). + + deriving (Functor, Foldable) + +instance Applicative (Term var) where + pure = Variable + (<*>) = ap + +instance Monad (Term var) where + return = Variable + t >>= f = + case t of + Variable x -> f x + Universe -> Universe + + ExtensionType tC psi tA phi a -> + ExtensionType (tC >>= f) (psi >>>= f) (tA >>>= f) (phi >>>= f) (a >>>= f) + Pi t' -> Pi (t' >>= f) + Lambda a phi body + -> Lambda (fmap (>>= f) a) (fmap (>>>= f) phi) (body >>>= f) + App t1 t2 -> App (t1 >>= f) (t2 >>= f) + + Sigma t' -> Sigma (t' >>= f) + Pair t1 t2 -> Pair (t1 >>= f) (t2 >>= f) + First t' -> First (t' >>= f) + Second t' -> Second (t' >>= f) + + IdType a x y -> IdType (a >>= f) (x >>= f) (y >>= f) + Refl a x -> Refl (fmap (>>= f) a) (x >>= f) + IdJ tA a tC d x p -> IdJ (tA >>= f) (a >>= f) (tC >>= f) (d >>= f) (x >>= f) (p >>= f) + + Cube -> Cube + CubeUnit -> CubeUnit + CubeUnitStar -> CubeUnitStar + + CubeProd t1 t2 -> CubeProd (t1 >>= f) (t2 >>= f) + + Tope -> Tope + TopeTop -> TopeTop + TopeBottom -> TopeBottom + TopeOr t1 t2 -> TopeOr (t1 >>= f) (t2 >>= f) + TopeAnd t1 t2 -> TopeAnd (t1 >>= f) (t2 >>= f) + TopeEQ t1 t2 -> TopeEQ (t1 >>= f) (t2 >>= f) + + RecBottom -> RecBottom + RecOr psi phi t1 t2 -> RecOr (psi >>= f) (phi >>= f) (t1 >>= f) (t2 >>= f) + + + Cube2 -> Cube2 + Cube2_0 -> Cube2_0 + Cube2_1 -> Cube2_1 + + TopeLEQ t1 t2 -> TopeLEQ (t1 >>= f) (t2 >>= f) + +deriveEq1 ''Term +deriveOrd1 ''Term +deriveRead1 ''Term +deriveShow1 ''Term + +instance (Eq var, Eq a) => Eq (Term var a) where (==) = eq1 +instance (Ord var, Ord a) => Ord (Term var a) where compare = compare1 +instance (Show var, Show a) => Show (Term var a) where showsPrec = showsPrec1 +instance (Read var, Read a) => Read (Term var a) where readsPrec = readsPrec1 diff --git a/rzk/src/Rzk/Simple/Syntax/Term/Example.hs b/rzk/src/Rzk/Simple/Syntax/Term/Example.hs new file mode 100644 index 000000000..6c12ad249 --- /dev/null +++ b/rzk/src/Rzk/Simple/Syntax/Term/Example.hs @@ -0,0 +1,5 @@ +module Rzk.Simple.Syntax.Term.Example where + +import Rzk.Simple.Syntax.Term + + diff --git a/rzk/src/Rzk/Simple/Syntax/Var.hs b/rzk/src/Rzk/Simple/Syntax/Var.hs new file mode 100644 index 000000000..3d944ff17 --- /dev/null +++ b/rzk/src/Rzk/Simple/Syntax/Var.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +module Rzk.Simple.Syntax.Var where + +import Data.Char (chr, ord) +import Data.Coerce (coerce) +import Data.String (IsString (..)) +import Data.Text (Text) +import qualified Data.Text as Text + +-- | Standard type of variables. +newtype Var = Var { getVar :: Text } + deriving (Eq, IsString) + +instance Show Var where show = Text.unpack . getVar + +appendIndexText :: Int -> Text -> Text +appendIndexText n s = s <> index + where + digitToSub c = chr ((ord c - ord '0') + ord 'β‚€') + index = Text.pack (map digitToSub (show n)) + +-- | Increment index for a variable. +-- +-- >>> incVarIndex "x" +-- x₁ +incVarIndex :: Var -> Var +incVarIndex = coerce incIndexText + +-- | Increment the subscript number at the end of the indentifier. +-- +-- >>> Var (incIndexText "x") +-- x₁ +-- >>> Var (incIndexText "x₁₉") +-- xβ‚‚β‚€ +incIndexText :: Text -> Text +incIndexText s = name <> newIndex + where + digitsSub = "β‚€β‚β‚‚β‚ƒβ‚„β‚…β‚†β‚‡β‚ˆβ‚‰" :: String + isDigitSub = (`elem` digitsSub) + digitFromSub c = chr ((ord c - ord 'β‚€') + ord '0') + digitToSub c = chr ((ord c - ord '0') + ord 'β‚€') + (name, index) = Text.break isDigitSub s + oldIndexN = read ('0' : map digitFromSub (Text.unpack index)) -- FIXME: read + newIndex = Text.pack (map digitToSub (show (oldIndexN + 1))) From 5cebbde4b2d6eb05ad6c28660f35f3bfe6e7735f Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 20 Feb 2021 14:03:24 +0300 Subject: [PATCH 02/10] Fix pretty-printer for binders and add Show instance for Term Var Var --- rzk/src/Rzk/Simple/Pretty.hs | 53 ++++++++++++++++++++++++------------ 1 file changed, 36 insertions(+), 17 deletions(-) diff --git a/rzk/src/Rzk/Simple/Pretty.hs b/rzk/src/Rzk/Simple/Pretty.hs index 507c40eda..28f2f67be 100644 --- a/rzk/src/Rzk/Simple/Pretty.hs +++ b/rzk/src/Rzk/Simple/Pretty.hs @@ -1,14 +1,20 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} module Rzk.Simple.Pretty where import Bound.Scope (instantiate1) +import qualified Data.Text.Lazy as Text import Data.Text.Prettyprint.Doc import Data.Text.Prettyprint.Doc.Render.Terminal import Rzk.Simple.Syntax.Term import Rzk.Simple.Syntax.Var +instance {-# OVERLAPPING #-} Show (Term Var Var) where + show = Text.unpack . renderLazy . layoutPretty defaultLayoutOptions . ppTermANSIviaShow + data TypeOfTerm = TermVariable | TypeVariable @@ -59,22 +65,32 @@ highlightUsingAnsiStyle = \case ppTermANSI :: Show a => [Doc TypeOfTerm] -> Term var a -> Doc AnsiStyle ppTermANSI vars = reAnnotate highlightUsingAnsiStyle . ppTerm vars . fmap viaShow +ppTermLeft :: [Doc TypeOfTerm] -> Term var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppTermLeft vars = \case + t@Lambda{} -> parens (ppTerm vars t) + t@Pi{} -> parens (ppTerm vars t) + t@Sigma{} -> parens (ppTerm vars t) + t -> ppTerm vars t + ppTermParens :: [Doc TypeOfTerm] -> Term var (Doc TypeOfTerm) -> Doc TypeOfTerm ppTermParens vars = \case - t@Variable{} -> ppTerm vars t - t@Universe -> ppTerm vars t - t@Refl{} -> ppTerm vars t - t@Cube{} -> ppTerm vars t - t@CubeUnit{} -> ppTerm vars t - t@CubeUnitStar{} -> ppTerm vars t - t@Tope{} -> ppTerm vars t - t@TopeTop{} -> ppTerm vars t - t@TopeBottom{} -> ppTerm vars t - t@RecBottom{} -> ppTerm vars t - t@Cube2{} -> ppTerm vars t - t@Cube2_0{} -> ppTerm vars t - t@Cube2_1{} -> ppTerm vars t - t -> parens (ppTerm vars t) + t@Lambda{} -> ppTerm vars t + t@Pi{} -> ppTerm vars t + t@Sigma{} -> ppTerm vars t + t@Variable{} -> ppTerm vars t + t@Universe -> ppTerm vars t + t@Refl{} -> ppTerm vars t + t@Cube{} -> ppTerm vars t + t@CubeUnit{} -> ppTerm vars t + t@CubeUnitStar{} -> ppTerm vars t + t@Tope{} -> ppTerm vars t + t@TopeTop{} -> ppTerm vars t + t@TopeBottom{} -> ppTerm vars t + t@RecBottom{} -> ppTerm vars t + t@Cube2{} -> ppTerm vars t + t@Cube2_0{} -> ppTerm vars t + t@Cube2_1{} -> ppTerm vars t + t -> parens (ppTerm vars t) ppReserved :: Doc TypeOfTerm -> Doc TypeOfTerm ppReserved = annotate Reserved @@ -126,7 +142,7 @@ ppElimWithArgs vars elim args ppTerm :: [Doc TypeOfTerm] -> Term var (Doc TypeOfTerm) -> Doc TypeOfTerm ppTerm vars = \case Variable x -> ppVar x - App t1 t2 -> ppTerm vars t1 <+> ppTermParens vars t2 + App t1 t2 -> ppTermLeft vars t1 <+> ppTermParens vars t2 First t -> ppTermElim "π₁" <+> ppTermParens vars t Second t -> ppTermElim "Ο€β‚‚" <+> ppTermParens vars t Universe -> ppTypeCon "𝒰 " @@ -180,8 +196,11 @@ ppTerm vars = \case where var:_ = vars -pp :: Show a => Term var a -> IO () -pp t = putDoc (ppTermANSI vars t' <> "\n") +ppTermANSIviaShow :: Show a => Term var a -> Doc AnsiStyle +ppTermANSIviaShow t = ppTermANSI vars t' where vars = (viaShow . Var) <$> zipWith appendIndexText [0..] (repeat "x") t' = viaShow <$> t + +pp :: Show a => Term var a -> IO () +pp t = putDoc (ppTermANSIviaShow t <> "\n") From d4eb1176b3662429937f4327a1bc2ad18fe73ba3 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 20 Feb 2021 14:03:40 +0300 Subject: [PATCH 03/10] Fix whnf --- rzk/src/Rzk/Simple/Evaluator.hs | 73 ++++++++++++++++----------------- 1 file changed, 36 insertions(+), 37 deletions(-) diff --git a/rzk/src/Rzk/Simple/Evaluator.hs b/rzk/src/Rzk/Simple/Evaluator.hs index 75a67ad7c..19fdacb9d 100644 --- a/rzk/src/Rzk/Simple/Evaluator.hs +++ b/rzk/src/Rzk/Simple/Evaluator.hs @@ -81,41 +81,40 @@ whnf = \case Pair _t1 t2 -> nf t2 t' -> t' - e@Variable{} -> e - e@Universe -> e - - ExtensionType tC psi tA phi a -> - ExtensionType (nf tC) (nfScoped psi) (nfScoped tA) (nfScoped phi) (nfScoped a) - Pi t' -> Pi (nf t') - e@Lambda{} -> e - - Sigma t' -> Sigma (nf t') - Pair t1 t2 -> Pair (nf t1) (nf t2) - - IdType a x y -> IdType (nf a) (nf x) (nf y) - Refl a x -> Refl (fmap nf a) (nf x) - IdJ tA a tC d x p -> IdJ (nf tA) (nf a) (nf tC) (nf d) (nf x) (nf p) - - Cube -> Cube - CubeUnit -> CubeUnit - CubeUnitStar -> CubeUnitStar - - CubeProd t1 t2 -> CubeProd (nf t1) (nf t2) - - Tope -> Tope - TopeTop -> TopeTop - TopeBottom -> TopeBottom - TopeOr t1 t2 -> TopeOr (nf t1) (nf t2) - TopeAnd t1 t2 -> TopeAnd (nf t1) (nf t2) - TopeEQ t1 t2 -> TopeEQ (nf t1) (nf t2) - - RecBottom -> RecBottom - RecOr psi phi t1 t2 -> RecOr (nf psi) (nf phi) (nf t1) (nf t2) - - - Cube2 -> Cube2 - Cube2_0 -> Cube2_0 - Cube2_1 -> Cube2_1 - - TopeLEQ t1 t2 -> TopeLEQ (nf t1) (nf t2) + IdJ tA a tC d x p -> + case whnf p of + Refl{} -> whnf d + p' -> IdJ tA a tC d x p' + + t@Variable{} -> t + t@Universe -> t + t@Lambda{} -> t + t@ExtensionType{} -> t + t@Pi{} -> t + t@Sigma{} -> t + t@Pair{} -> t + + t@IdType{} -> t + t@Refl{} -> t + + t@Cube -> t + t@CubeUnit -> t + t@CubeUnitStar -> t + t@CubeProd{} -> t + + t@Tope -> t + t@TopeTop -> t + t@TopeBottom -> t + + t@TopeOr{} -> t + t@TopeAnd{} -> t + t@TopeEQ{} -> t + + t@RecBottom -> t + t@RecOr{} -> t + + t@Cube2 -> t + t@Cube2_0 -> t + t@Cube2_1 -> t + t@TopeLEQ{} -> t From 618e88448291313c83fbbb21fcff4d1a4f8a289f Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 20 Feb 2021 18:14:25 +0300 Subject: [PATCH 04/10] Add annotations and make nf/whnf work with definitions --- rzk/src/Rzk/Simple/Evaluator.hs | 293 +++++++++++++++---------- rzk/src/Rzk/Simple/Parser.hs | 342 +++--------------------------- rzk/src/Rzk/Simple/Pretty.hs | 19 +- rzk/src/Rzk/Simple/Syntax/Term.hs | 54 ++--- rzk/src/Rzk/Simple/Syntax/Var.hs | 13 +- 5 files changed, 256 insertions(+), 465 deletions(-) diff --git a/rzk/src/Rzk/Simple/Evaluator.hs b/rzk/src/Rzk/Simple/Evaluator.hs index 19fdacb9d..f05327350 100644 --- a/rzk/src/Rzk/Simple/Evaluator.hs +++ b/rzk/src/Rzk/Simple/Evaluator.hs @@ -1,120 +1,183 @@ -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} module Rzk.Simple.Evaluator where +import qualified Data.MemoTrie as MemoTrie + import Bound +import Control.Monad.Trans (lift) +import Data.Hashable (Hashable) +import qualified Data.HashMap.Strict as HashMap import Rzk.Simple.Syntax.Term -nfScoped :: Scope b (Term var) a -> Scope b (Term var) a -nfScoped = Scope . nf . unscope - -nf :: Term var a -> Term var a -nf = \case - App t1 t2 -> - case whnf t1 of - Lambda _a _phi body -> nf (instantiate1 t2 body) - t1' -> App (nf t1') (nf t2) - - First t -> - case whnf t of - Pair t1 _t2 -> nf t1 - t' -> nf t' - Second t -> - case whnf t of - Pair _t1 t2 -> nf t2 - t' -> nf t' - - IdJ tA a tC d x p -> - case whnf p of - Refl{} -> nf d - p' -> IdJ (nf tA) (nf a) (nf tC) (nf d) (nf x) (nf p') - - e@Variable{} -> e - e@Universe -> e - - ExtensionType tC psi tA phi a -> - ExtensionType (nf tC) (nfScoped psi) (nfScoped tA) (nfScoped phi) (nfScoped a) - Pi t' -> Pi (nf t') - Lambda a phi body - -> Lambda (fmap nf a) (fmap nfScoped phi) (nfScoped body) - - Sigma t' -> Sigma (nf t') - Pair t1 t2 -> Pair (nf t1) (nf t2) - - IdType a x y -> IdType (nf a) (nf x) (nf y) - Refl a x -> Refl (fmap nf a) (nf x) - - Cube -> Cube - CubeUnit -> CubeUnit - CubeUnitStar -> CubeUnitStar - - CubeProd t1 t2 -> CubeProd (nf t1) (nf t2) - - Tope -> Tope - TopeTop -> TopeTop - TopeBottom -> TopeBottom - TopeOr t1 t2 -> TopeOr (nf t1) (nf t2) - TopeAnd t1 t2 -> TopeAnd (nf t1) (nf t2) - TopeEQ t1 t2 -> TopeEQ (nf t1) (nf t2) - - RecBottom -> RecBottom - RecOr psi phi t1 t2 -> RecOr (nf psi) (nf phi) (nf t1) (nf t2) - - Cube2 -> Cube2 - Cube2_0 -> Cube2_0 - Cube2_1 -> Cube2_1 - - TopeLEQ t1 t2 -> TopeLEQ (nf t1) (nf t2) - -whnf :: Term var a -> Term var a -whnf = \case - App t1 t2 -> - case whnf t1 of - Lambda _a _phi body -> whnf (instantiate1 t2 body) - t1' -> App t1' t2 - - First t -> - case whnf t of - Pair t1 _t2 -> nf t1 - t' -> t' - Second t -> - case whnf t of - Pair _t1 t2 -> nf t2 - t' -> t' - - IdJ tA a tC d x p -> - case whnf p of - Refl{} -> whnf d - p' -> IdJ tA a tC d x p' - - t@Variable{} -> t - t@Universe -> t - t@Lambda{} -> t - t@ExtensionType{} -> t - t@Pi{} -> t - t@Sigma{} -> t - t@Pair{} -> t - - t@IdType{} -> t - t@Refl{} -> t - - t@Cube -> t - t@CubeUnit -> t - t@CubeUnitStar -> t - t@CubeProd{} -> t - - t@Tope -> t - t@TopeTop -> t - t@TopeBottom -> t - - t@TopeOr{} -> t - t@TopeAnd{} -> t - t@TopeEQ{} -> t - - t@RecBottom -> t - t@RecOr{} -> t - - t@Cube2 -> t - t@Cube2_0 -> t - t@Cube2_1 -> t - t@TopeLEQ{} -> t - +data EvalContext ann var a b = EvalContext + { definitionOf :: a -> Either b (Term ann var a) + } + +emptyEvalContext :: EvalContext ann var a a +emptyEvalContext = EvalContext + { definitionOf = Left + } + +mkEvalContext + :: (Eq a, Hashable a) + => (a -> b) + -> [(a, Term ann var a)] + -> EvalContext ann var a b +mkEvalContext convert dict = EvalContext + { definitionOf = \x -> + case HashMap.lookup x definitions of + Nothing -> Left (convert x) + Just t -> Right t + } + where + definitions = HashMap.fromList dict + +nfWith :: forall ann var a. EvalContext ann var a a -> Term ann var a -> Term ann var a +nfWith context@EvalContext{..} = nf' + where + whnf' = whnfWith context + + -- definitionOf' + -- :: Var x (Term ann var a) + -- -> Either (Var x (Term ann var a)) (Term ann var (Var x (Term ann var a))) + definitionOf' = \case + B b -> Left (B b) + F (Variable y) -> + case definitionOf y of + Left z -> Left (F (pure z)) + Right t -> Right (pure (F t)) + F t -> Right (F . pure <$> t) + + -- nfScoped :: Scope x (Term ann var) a -> Scope x (Term ann var) b + nfScoped = Scope . nfWith context' . unscope + where + -- context' :: EvalContext ann var (Var x (Term ann var a)) (Var x (Term ann var b)) + context' = context { definitionOf = definitionOf' } + + nf' = \case + t@(Variable x) -> + case definitionOf x of + Left y -> Variable y + Right t' -> nf' t' + Annotated ann t -> Annotated ann (nf' t) + App t1 t2 -> + case whnf' t1 of + Lambda _a _phi body -> nf' (instantiate1 t2 body) + t1' -> App (nf' t1') (nf' t2) + + First t -> + case whnf' t of + Pair t1 _t2 -> nf' t1 + t' -> nf' t' + Second t -> + case whnf' t of + Pair _t1 t2 -> nf' t2 + t' -> nf' t' + + IdJ tA a tC d x p -> + case whnf' p of + Refl{} -> nf' d + p' -> IdJ (nf' tA) (nf' a) (nf' tC) (nf' d) (nf' x) (nf' p') + + e@Universe -> e + + ExtensionType tC psi tA phi a -> + ExtensionType (nf' tC) (nfScoped psi) (nfScoped tA) (nfScoped phi) (nfScoped a) + Pi t' -> Pi (nf' t') + Lambda a phi body + -> Lambda (fmap nf' a) (fmap nfScoped phi) (nfScoped body) + + Sigma t' -> Sigma (nf' t') + Pair t1 t2 -> Pair (nf' t1) (nf' t2) + + IdType a x y -> IdType (nf' a) (nf' x) (nf' y) + Refl a x -> Refl (fmap nf' a) (nf' x) + + Cube -> Cube + CubeUnit -> CubeUnit + CubeUnitStar -> CubeUnitStar + + CubeProd t1 t2 -> CubeProd (nf' t1) (nf' t2) + + Tope -> Tope + TopeTop -> TopeTop + TopeBottom -> TopeBottom + TopeOr t1 t2 -> TopeOr (nf' t1) (nf' t2) + TopeAnd t1 t2 -> TopeAnd (nf' t1) (nf' t2) + TopeEQ t1 t2 -> TopeEQ (nf' t1) (nf' t2) + + RecBottom -> RecBottom + RecOr psi phi t1 t2 -> RecOr (nf' psi) (nf' phi) (nf' t1) (nf' t2) + + Cube2 -> Cube2 + Cube2_0 -> Cube2_0 + Cube2_1 -> Cube2_1 + + TopeLEQ t1 t2 -> TopeLEQ (nf' t1) (nf' t2) + +whnfWith :: EvalContext ann var a a -> Term ann var a -> Term ann var a +whnfWith EvalContext{..} = whnf' + where + whnf' = \case + t@(Variable x) -> + case definitionOf x of + Left z -> pure z + Right t' -> whnf' t' + Annotated ann t -> Annotated ann (whnf' t) + App t1 t2 -> + case whnf' t1 of + Lambda _a _phi body -> whnf' (instantiate1 t2 body) + t1' -> App t1' t2 + + First t -> + case whnf' t of + Pair t1 _t2 -> whnf' t1 + t' -> t' + Second t -> + case whnf' t of + Pair _t1 t2 -> whnf' t2 + t' -> t' + + IdJ tA a tC d x p -> + case whnf' p of + Refl{} -> whnf' d + p' -> IdJ tA a tC d x p' + + t@Universe -> t + t@Lambda{} -> t + t@ExtensionType{} -> t + t@Pi{} -> t + t@Sigma{} -> t + t@Pair{} -> t + + t@IdType{} -> t + t@Refl{} -> t + + t@Cube -> t + t@CubeUnit -> t + t@CubeUnitStar -> t + t@CubeProd{} -> t + + t@Tope -> t + t@TopeTop -> t + t@TopeBottom -> t + + t@TopeOr{} -> t + t@TopeAnd{} -> t + t@TopeEQ{} -> t + + t@RecBottom -> t + t@RecOr{} -> t + + t@Cube2 -> t + t@Cube2_0 -> t + t@Cube2_1 -> t + t@TopeLEQ{} -> t + +nf :: Term ann var a -> Term ann var a +nf = nfWith emptyEvalContext + +whnf :: Term ann var a -> Term ann var a +whnf = whnfWith emptyEvalContext diff --git a/rzk/src/Rzk/Simple/Parser.hs b/rzk/src/Rzk/Simple/Parser.hs index acb809678..87e397e2e 100644 --- a/rzk/src/Rzk/Simple/Parser.hs +++ b/rzk/src/Rzk/Simple/Parser.hs @@ -25,18 +25,23 @@ import Text.Trifecta import Rzk.Simple.Syntax.Term import Rzk.Simple.Syntax.Var -type RzkParser = Unlined Parser +type RzkParser = Parser -- ** Term +parseSpanned :: RzkParser (Term Span Var Var) -> RzkParser (Term Span Var Var) +parseSpanned parser = annotateWithSpan <$> spanned parser + where + annotateWithSpan (t :~ span') = Annotated span' t + rzkVar :: RzkParser Var rzkVar = Var <$> rzkIdent -rzkTerm :: RzkParser (Term Var Var) +rzkTerm :: RzkParser (Term Span Var Var) rzkTerm = "term" buildExpressionParser rzkOperatorTable rzkTerm' -rzkTerm' :: RzkParser (Term Var Var) +rzkTerm' :: RzkParser (Term Span Var Var) rzkTerm' = "simple term" try rzkTermPiType <|> rzkTermPiShape @@ -66,44 +71,44 @@ rzkTerm' = "simple term" <|> RecBottom <$ (symbol "recBOT" <|> symbol "recβŠ₯") <|> rzkTermVar -rzkTermVar :: RzkParser (Term Var Var) +rzkTermVar :: RzkParser (Term Span Var Var) rzkTermVar = "variable" (Variable <$> (Var <$> rzkIdent)) -rzkTermColonType :: RzkParser (Term Var Var, Term Var Var) +rzkTermColonType :: RzkParser (Term Span Var Var, Term Span Var Var) rzkTermColonType = do term <- rzkTerm colon type_ <- rzkTerm return (term, type_) -rzkTermColonType' :: RzkParser (Term Var Var, Maybe (Term Var Var)) +rzkTermColonType' :: RzkParser (Term Span Var Var, Maybe (Term Span Var Var)) rzkTermColonType' = try withType <|> withoutType where withType = fmap Just <$> rzkTermColonType withoutType = (\t -> (t, Nothing)) <$> rzkTerm -rzkVarColonType' :: RzkParser (Var, Maybe (Term Var Var)) +rzkVarColonType' :: RzkParser (Var, Maybe (Term Span Var Var)) rzkVarColonType' = try withType <|> withoutType where withType = fmap Just <$> parens rzkVarColonType withoutType = (\x -> (Var x, Nothing)) <$> rzkIdent -rzkVarColonType :: RzkParser (Var, Term Var Var) +rzkVarColonType :: RzkParser (Var, Term Span Var Var) rzkVarColonType = do x <- Var <$> rzkIdent colon type_ <- rzkTerm return (x, type_) -rzkTermPiType :: RzkParser (Term Var Var) +rzkTermPiType :: RzkParser (Term Span Var Var) rzkTermPiType = "dependent function type" do (var, a) <- parens rzkVarColonType symbol "->" <|> symbol "β†’" t <- rzkTerm return (Pi (Lambda (Just a) Nothing (abstract1Name var t))) -rzkTermPiShape :: RzkParser (Term Var Var) +rzkTermPiShape :: RzkParser (Term Span Var Var) rzkTermPiShape = "dependent function type (from a shape)" do symbol "{" (var, i) <- rzkVarColonType' @@ -114,7 +119,7 @@ rzkTermPiShape = "dependent function type (from a shape)" do a <- rzkTerm return (Pi (Lambda i (Just (abstract1Name var phi)) (abstract1Name var a))) -rzkTermLambda :: RzkParser (Term Var Var) +rzkTermLambda :: RzkParser (Term Span Var Var) rzkTermLambda = "lambda abstraction (anonymous function from a type)" do symbol "Ξ»" <|> symbol "\\" (x, a) <- rzkVarColonType' @@ -122,7 +127,7 @@ rzkTermLambda = "lambda abstraction (anonymous function from a type)" do t <- rzkTerm return (Lambda a Nothing (abstract1Name x t)) -rzkTermLambdaShape :: RzkParser (Term Var Var) +rzkTermLambdaShape :: RzkParser (Term Span Var Var) rzkTermLambdaShape = "lambda abstraction (anonymous function from a shape)" do symbol "Ξ»" <|> symbol "\\" symbol "{" @@ -134,7 +139,7 @@ rzkTermLambdaShape = "lambda abstraction (anonymous function from a shape)" a <- rzkTerm return (Lambda (Just i) (Just (abstract1Name t phi)) (abstract1Name t a)) -rzkTermSigmaType :: RzkParser (Term Var Var) +rzkTermSigmaType :: RzkParser (Term Span Var Var) rzkTermSigmaType = "dependent sum type" do symbol "βˆ‘" <|> symbol "Sigma" (x, a) <- parens rzkVarColonType @@ -142,14 +147,14 @@ rzkTermSigmaType = "dependent sum type" do t <- rzkTerm return (Sigma (Lambda (Just a) Nothing (abstract1Name x t))) -rzkTermRefl :: RzkParser (Term Var Var) +rzkTermRefl :: RzkParser (Term Span Var Var) rzkTermRefl = do symbol "refl_{" (x, a) <- rzkTermColonType' symbol "}" return (Refl a x) -rzkTermIdJ :: RzkParser (Term Var Var) +rzkTermIdJ :: RzkParser (Term Span Var Var) rzkTermIdJ = do symbol "idJ" symbol "(" @@ -162,7 +167,7 @@ rzkTermIdJ = do symbol ")" return (IdJ tA a tC d x p) -rzkTermRecOr :: RzkParser (Term Var Var) +rzkTermRecOr :: RzkParser (Term Span Var Var) rzkTermRecOr = do symbol "recOR" <|> symbol "rec∨" symbol "(" @@ -173,17 +178,17 @@ rzkTermRecOr = do symbol ")" return (RecOr psi phi a b) -rzkTermFirst :: RzkParser (Term Var Var) +rzkTermFirst :: RzkParser (Term Span Var Var) rzkTermFirst = do (symbol "first" <|> symbol "π₁") "π₁" First <$> rzkTerm -rzkTermSecond :: RzkParser (Term Var Var) +rzkTermSecond :: RzkParser (Term Span Var Var) rzkTermSecond = do (symbol "second" <|> symbol "Ο€β‚‚") "Ο€β‚‚" Second <$> rzkTerm -rzkTermExtensionTypeFromCube :: RzkParser (Term Var Var) +rzkTermExtensionTypeFromCube :: RzkParser (Term Span Var Var) rzkTermExtensionTypeFromCube = between (symbol "<(") (symbol ">") $ do t <- rzkVar symbol ":" @@ -204,7 +209,7 @@ rzkTermExtensionTypeFromCube = between (symbol "<(") (symbol ">") $ do return (ExtensionType cI (abstract1Name t TopeTop) (abstract1Name t tA) (abstract1Name t phi) (abstract1Name t a)) -rzkTermExtensionType :: RzkParser (Term Var Var) +rzkTermExtensionType :: RzkParser (Term Span Var Var) rzkTermExtensionType = between (symbol "<{") (symbol ">") $ do t <- rzkVar symbol ":" @@ -226,22 +231,22 @@ rzkTermExtensionType = between (symbol "<{") (symbol ">") $ do Nothing -> (TopeBottom, RecBottom) return (ExtensionType cI (abstract1Name t psi) (abstract1Name t tA) (abstract1Name t phi) (abstract1Name t a)) --- firstP :: Parser (Term Var Var) +-- firstP :: Parser (Term Span Var Var) -- firstP = do -- "first" <|> "π₁" -- skipSpace -- First <$> termParens True -- --- secondP :: Parser (Term Var Var) +-- secondP :: Parser (Term Span Var Var) -- secondP = do -- "second" <|> "Ο€β‚‚" -- skipSpace -- Second <$> termParens True -rzkTermPair :: RzkParser (Term Var Var) +rzkTermPair :: RzkParser (Term Span Var Var) rzkTermPair = parens (Pair <$> rzkTerm <* comma <*> rzkTerm) -rzkTermApp :: RzkParser (Term Var Var) +rzkTermApp :: RzkParser (Term Span Var Var) rzkTermApp = do t1 <- rzkTerm t2 <- rzkTerm @@ -250,7 +255,7 @@ rzkTermApp = do rzkOperator :: RzkParser a -> RzkParser a rzkOperator op = op -- <* skipMany (satisfy isSpace) -rzkOperatorTable :: OperatorTable RzkParser (Term Var Var) +rzkOperatorTable :: OperatorTable RzkParser (Term Span Var Var) rzkOperatorTable = [ [ Infix (pure App) AssocLeft ] , [ Infix (CubeProd <$ rzkOperator (symbol "*" <|> symbol "Γ—")) AssocLeft ] @@ -310,300 +315,19 @@ isDelim c = c `elem` ("()[]{}," :: String) -- * Orphan 'IsString' instances -instance IsString (Term Var Var) where +instance IsString (Term Span Var Var) where fromString = unsafeParseTerm -unsafeParseTerm :: String -> Term Var Var +unsafeParseTerm :: String -> Term Span Var Var unsafeParseTerm = unsafeParseString rzkTerm unsafeParseString :: RzkParser a -> String -> a unsafeParseString parser input = - case parseString (runUnlined parser) mempty input of + case parseString parser mempty input of Success x -> x Failure errInfo -> unsafePerformIO $ do putDoc (_errDoc errInfo <> "\n") error "Parser error while attempting unsafeParseString" --- --- module_ :: Parser (Module Var) --- module_ = do --- moduleDecls <- decl `Atto.sepBy` (skipSpace >> Atto.many1 Atto.endOfLine) --- return Module{..} --- --- decl :: Parser (Decl Var) --- decl = do --- declName <- var --- skipSpace >> ":" >> skipSpace --- declType <- term --- Atto.skipSpace >> ":=" >> skipSpace --- declBody <- term --- return Decl{..} --- --- term :: Parser (Term Var Var) --- term = termParens False --- --- termParens :: Bool -> Parser (Term Var Var) --- termParens useParens --- = termParens' useParens --- <|> parens (termParens useParens) --- --- termParens' :: Bool -> Parser (Term Var Var) --- termParens' useParens --- = parens' idType --- <|> parens' firstP <|> parens' secondP --- <|> parens' idJ --- <|> parens' recOr --- <|> parens' cubeProd --- <|> parens' constrainedType --- <|> refl --- <|> recBottom --- <|> cubeU <|> topeU <|> universe --- <|> topeTop <|> topeBottom --- <|> cubeUnit <|> cubeUnitStar --- <|> parens' piApp --- <|> piType <|> sigmaType --- <|> pair --- <|> parens' piLambda --- <|> parens' topeOr -- FIXME: slow --- <|> parens' topeAnd -- FIXME: slow --- <|> parens' topeEQ -- FIXME: slow --- <|> hole <|> (Variable <$> var) --- where --- parens' = if useParens then parens else id --- --- parseTuple :: Parser [Term Var Var] --- parseTuple --- = "(" *> skipSpace *> Atto.sepBy1 term (skipSpace *> "," <* skipSpace) <* skipSpace <* ")" --- --- cubeU :: Parser (Term var) --- cubeU = Cube <$ "CUBE" --- --- topeU :: Parser (Term var) --- topeU = Tope <$ "TOPE" --- --- cubeUnit :: Parser (Term var) --- cubeUnit = CubeUnit <$ "1" --- --- cubeUnitStar :: Parser (Term var) --- cubeUnitStar = CubeUnit <$ ("*_1" <|> "⋆") --- --- cubeProd :: Parser (Term Var Var) --- cubeProd = do --- i <- termParens True --- skipSpace --- "Γ—" <|> "*" --- skipSpace --- j <- termParens True --- return (CubeProd i j) --- --- topeTop :: Parser (Term var) --- topeTop = TopeTop <$ ("TOP" <|> "⊀") --- --- topeBottom :: Parser (Term var) --- topeBottom = TopeBottom <$ ("BOT" <|> "βŠ₯") --- --- topeOr :: Parser (Term Var Var) --- topeOr = do --- phi <- termParens True --- skipSpace --- "\\/" <|> "∨" --- skipSpace --- psi <- termParens True --- return (TopeOr phi psi) --- --- topeAnd :: Parser (Term Var Var) --- topeAnd = do --- phi <- termParens True --- skipSpace --- "/\\" <|> "∧" --- skipSpace --- psi <- termParens True --- return (TopeAnd phi psi) --- --- topeEQ :: Parser (Term Var Var) --- topeEQ = do --- t <- termParens True --- skipSpace --- "===" <|> "≑" --- skipSpace --- s <- termParens True --- return (TopeEQ t s) --- --- recBottom :: Parser (Term Var Var) --- recBottom = RecBottom <$ ("recBOT" <|> "recβŠ₯") --- --- recOr :: Parser (Term Var Var) --- recOr = do --- "recOR" <|> "rec∨" --- [psi, phi, a, b] <- parseTuple --- return (RecOr psi phi a b) --- --- constrainedType :: Parser (Term Var Var) --- constrainedType = do --- phi <- termParens True --- skipSpace --- "=>" --- skipSpace --- a <- term --- return (ConstrainedType phi a) --- --- parens :: Parser a -> Parser a --- parens p = "(" *> skipSpace *> p <* skipSpace <* ")" --- --- piType :: Parser (Term Var Var) --- piType = do --- "{" --- skipSpace --- x <- var "variable identifier" --- skipSpace --- ":" --- skipSpace --- a <- term "type" --- skipSpace --- "}" --- skipSpace --- "->" <|> "β†’" --- skipSpace --- b <- term "type" --- return (Pi (Lambda x a b)) --- --- piLambda :: Parser (Term Var Var) --- piLambda = do --- "Ξ»" <|> "\\" --- skipSpace --- "(" --- skipSpace --- x <- var "variable identifier" --- skipSpace --- ":" --- skipSpace --- a <- term "type" --- skipSpace --- ")" --- skipSpace --- "->" <|> "β†’" --- skipSpace --- t <- term "term" --- return (Lambda x a t) --- --- piApp :: Parser (Term Var Var) --- piApp = do --- t1 <- termParens True --- skipSpace --- t2 <- termParens True --- return (App t1 t2) --- --- sigmaType :: Parser (Term Var Var) --- sigmaType = do --- "Sigma" <|> "βˆ‘" --- skipSpace --- "(" --- skipSpace --- x <- var "variable identifier" --- skipSpace --- ":" --- skipSpace --- a <- term "type" --- skipSpace --- ")" --- skipSpace --- "," --- skipSpace --- b <- term "type" --- return (Sigma (Lambda x a b)) --- --- pair :: Parser (Term Var Var) --- pair = do --- "(" --- skipSpace --- f <- term --- skipSpace --- "," --- skipSpace --- s <- term --- skipSpace --- ")" --- return (Pair f s) --- --- firstP :: Parser (Term Var Var) --- firstP = do --- "first" <|> "π₁" --- skipSpace --- First <$> termParens True --- --- secondP :: Parser (Term Var Var) --- secondP = do --- "second" <|> "Ο€β‚‚" --- skipSpace --- Second <$> termParens True --- --- idType :: Parser (Term Var Var) --- idType = do --- x <- termParens True --- skipSpace --- "=_{" --- skipSpace --- a <- termParens False --- skipSpace --- "}" --- skipSpace --- y <- termParens True --- return (IdType a x y) --- --- refl :: Parser (Term Var Var) --- refl = do --- "refl_{" --- skipSpace --- x <- term --- skipSpace --- ":" --- skipSpace --- a <- term --- skipSpace --- "}" --- return (Refl a x) --- --- idJ :: Parser (Term Var Var) --- idJ = do --- "idJ" --- [tA, a, tC, d, x, p] <- parseTuple --- return (IdJ tA a tC d x p) --- --- universe :: Parser (Term Var Var) --- universe = do --- "U" <|> "𝒰" --- return Universe --- --- hole :: Parser (Term Var Var) --- hole = Hole <$> ("?" >> var) --- --- var :: Parser Var --- var = do --- first <- Atto.satisfy (Atto.inClass (letters <> "_")) --- rest <- Atto.takeWhile (Atto.inClass (letters <> digits <> digitsSub <> "_")) --- return (Var (Text.cons first rest)) --- where --- digits = "0123456789" --- digitsSub = "β‚€β‚β‚‚β‚ƒβ‚„β‚…β‚†β‚‡β‚ˆβ‚‰" --- --- letters = latinSmall <> latinCapital <> greekSmall --- latinSmall = "abcdefghijklmnopqrstuvwxyz" --- latinCapital = "ABCDEFGHIJKLMNOPQRSTUVWXYZ" --- greekSmall = "Ξ±Ξ²Ξ³Ξ΄Ξ΅ΞΆΞ·ΞΈΞΉΞΊΞ»ΞΌΞ½ΞΎΞΏΟ€ΟΟ‚ΟƒΟ„Ο…Ο†Ο‡ΟˆΟ‰" \\ "Ξ»" --- --- unsafeParse :: String -> Parser a -> Text -> a --- unsafeParse name parser input = --- case Atto.parseOnly (parser <* Atto.endOfInput) input of --- Right t -> t --- Left err -> error $ unlines --- [ "Failed parsing " <> name --- , " " <> Text.unpack input --- , "Parsing error was:" --- , err --- ] --- --- skipSpace :: Parser () --- skipSpace = Atto.skipWhile (Atto.inClass " \t") - () :: Parsing m => String -> m a -> m a () = flip () diff --git a/rzk/src/Rzk/Simple/Pretty.hs b/rzk/src/Rzk/Simple/Pretty.hs index 28f2f67be..5cbf6e581 100644 --- a/rzk/src/Rzk/Simple/Pretty.hs +++ b/rzk/src/Rzk/Simple/Pretty.hs @@ -12,7 +12,7 @@ import Data.Text.Prettyprint.Doc.Render.Terminal import Rzk.Simple.Syntax.Term import Rzk.Simple.Syntax.Var -instance {-# OVERLAPPING #-} Show (Term Var Var) where +instance {-# OVERLAPPING #-} Show (Term ann Var Var) where show = Text.unpack . renderLazy . layoutPretty defaultLayoutOptions . ppTermANSIviaShow data TypeOfTerm @@ -62,17 +62,17 @@ highlightUsingAnsiStyle = \case Reserved -> color Cyan -ppTermANSI :: Show a => [Doc TypeOfTerm] -> Term var a -> Doc AnsiStyle +ppTermANSI :: Show a => [Doc TypeOfTerm] -> Term ann var a -> Doc AnsiStyle ppTermANSI vars = reAnnotate highlightUsingAnsiStyle . ppTerm vars . fmap viaShow -ppTermLeft :: [Doc TypeOfTerm] -> Term var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppTermLeft :: [Doc TypeOfTerm] -> Term ann var (Doc TypeOfTerm) -> Doc TypeOfTerm ppTermLeft vars = \case t@Lambda{} -> parens (ppTerm vars t) t@Pi{} -> parens (ppTerm vars t) t@Sigma{} -> parens (ppTerm vars t) t -> ppTerm vars t -ppTermParens :: [Doc TypeOfTerm] -> Term var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppTermParens :: [Doc TypeOfTerm] -> Term ann var (Doc TypeOfTerm) -> Doc TypeOfTerm ppTermParens vars = \case t@Lambda{} -> ppTerm vars t t@Pi{} -> ppTerm vars t @@ -119,7 +119,7 @@ ppTopeElim = annotate TopeEliminator ppCubeElim :: Doc TypeOfTerm -> Doc TypeOfTerm ppCubeElim = annotate CubeEliminator -ppScoped :: [Doc TypeOfTerm] -> Scope1Term var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppScoped :: [Doc TypeOfTerm] -> Scope1Term ann var (Doc TypeOfTerm) -> Doc TypeOfTerm ppScoped [] = error "Not enough fresh variables!" ppScoped (x:vars) = ppTerm vars . instantiate1 (Variable x) @@ -135,12 +135,13 @@ ppTopeVar = annotate TopeVariable ppCubeVar :: Doc TypeOfTerm -> Doc TypeOfTerm ppCubeVar = annotate CubeVariable -ppElimWithArgs :: [Doc TypeOfTerm] -> Doc TypeOfTerm -> [Term var (Doc TypeOfTerm)] -> Doc TypeOfTerm +ppElimWithArgs :: [Doc TypeOfTerm] -> Doc TypeOfTerm -> [Term ann var (Doc TypeOfTerm)] -> Doc TypeOfTerm ppElimWithArgs vars elim args = elim <> parens (hsep (punctuate comma (map (ppTerm vars) args))) -ppTerm :: [Doc TypeOfTerm] -> Term var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppTerm :: [Doc TypeOfTerm] -> Term ann var (Doc TypeOfTerm) -> Doc TypeOfTerm ppTerm vars = \case + Annotated _ann t -> ppTerm vars t -- ignore annotations Variable x -> ppVar x App t1 t2 -> ppTermLeft vars t1 <+> ppTermParens vars t2 First t -> ppTermElim "π₁" <+> ppTermParens vars t @@ -196,11 +197,11 @@ ppTerm vars = \case where var:_ = vars -ppTermANSIviaShow :: Show a => Term var a -> Doc AnsiStyle +ppTermANSIviaShow :: Show a => Term ann var a -> Doc AnsiStyle ppTermANSIviaShow t = ppTermANSI vars t' where vars = (viaShow . Var) <$> zipWith appendIndexText [0..] (repeat "x") t' = viaShow <$> t -pp :: Show a => Term var a -> IO () +pp :: Show a => Term ann var a -> IO () pp t = putDoc (ppTermANSIviaShow t <> "\n") diff --git a/rzk/src/Rzk/Simple/Syntax/Term.hs b/rzk/src/Rzk/Simple/Syntax/Term.hs index ae28e723e..d4469c4eb 100644 --- a/rzk/src/Rzk/Simple/Syntax/Term.hs +++ b/rzk/src/Rzk/Simple/Syntax/Term.hs @@ -12,44 +12,45 @@ import Data.Functor.Classes type Scope1 var = Scope (Name var ()) -type Scope1Term var a = Scope1 var (Term var) a +type Scope1Term ann var a = Scope1 var (Term ann var) a -- | This is a (probably unevaluated) term out of context. -data Term var a - = Variable a +data Term ann var a + = Annotated ann (Term ann var a) + | Variable a -- ^ Term variable \(x_i\) or type variable \(A_i\) or cube variable \(t_i\) or tope variable \(\phi_i\). | Universe -- ^ Universe type \(\mathcal{U}\). -- Saying \(A \mathbf{type}\) is equivalent to saying \(A : \mathcal{U}\). - | Pi (Term var a) + | Pi (Term ann var a) -- ^ Dependent product type former \(\prod_{x : A} B(x)\). -- The term argument represents type family \(B : A \to \mathcal{U}\). - | Lambda (Maybe (Term var a)) (Maybe (Scope1Term var a)) (Scope1Term var a) + | Lambda (Maybe (Term ann var a)) (Maybe (Scope1Term ann var a)) (Scope1Term ann var a) -- ^ \(\lambda\)-abstraction ("lambda abstraction"). -- @Lambda x a Nothing m@ represents a term of the form \(\lambda (x : A). M\) -- while @Lambda t i (Just phi) m@ represents \(\lambda \{t : I | \phi\}. M\) - | App (Term var a) (Term var a) + | App (Term ann var a) (Term ann var a) -- ^ Application of one term to another \((M N)\). - | Sigma (Term var a) + | Sigma (Term ann var a) -- ^ Dependent sum type former \(\sum_{x : A} B(x)\). -- The term argument represents type family \(B : A \to \mathcal{U}\). - | Pair (Term var a) (Term var a) + | Pair (Term ann var a) (Term ann var a) -- ^ A (dependent) pair of terms. -- @Pair x y@ represents a term of the form \((x, y)\). - | First (Term var a) + | First (Term ann var a) -- ^ Project the first element of a pair: \(\pi_1 p\). - | Second (Term var a) + | Second (Term ann var a) -- ^ Project the second element of a pair: \(\pi_2 p\). - | IdType (Term var a) (Term var a) (Term var a) + | IdType (Term ann var a) (Term ann var a) (Term ann var a) -- ^ Identity type former \(x =_A y\) (corresponding to term @IdType a x y@). - | Refl (Maybe (Term var a)) (Term var a) + | Refl (Maybe (Term ann var a)) (Term ann var a) -- ^ Trivial inhabitant of \(x =_A x\) for any type \(A\) and \(x : A\). -- @Refl a x@ corresponds to \(x =_a x\). - | IdJ (Term var a) (Term var a) (Term var a) (Term var a) (Term var a) (Term var a) + | IdJ (Term ann var a) (Term ann var a) (Term ann var a) (Term ann var a) (Term ann var a) (Term ann var a) -- ^ Path induction (for identity types). -- For any type \(A\) and \(a : A\), type family -- \(C : \prod_{x : A} ((a =_A x) \to \mathcal{U})\) @@ -66,7 +67,7 @@ data Term var a | CubeUnitStar -- ^ The only point in the unit cube: \(\star : \mathbf{1}\). - | CubeProd (Term var a) (Term var a) + | CubeProd (Term ann var a) (Term ann var a) -- ^ Product of cubes: \(I \times J\). | Tope @@ -75,21 +76,21 @@ data Term var a -- ^ Top tope (no constraints on cube): \(\top\;\mathsf{tope}\) | TopeBottom -- ^ Bottom tope (cube contrained to empty space): \(\bot\;\mathsf{tope}\) - | TopeOr (Term var a) (Term var a) + | TopeOr (Term ann var a) (Term ann var a) -- ^ Tope disjuction (union of shapes): \(\psi \lor \phi\;\mathsf{tope}\) - | TopeAnd (Term var a) (Term var a) + | TopeAnd (Term ann var a) (Term ann var a) -- ^ Tope conjunction (intersection of shapes): \(\psi \land \phi\;\mathsf{tope}\) - | TopeEQ (Term var a) (Term var a) + | TopeEQ (Term ann var a) (Term ann var a) -- ^ Equality tope (diagonals): \(t \equiv s \;\mathsf{tope}\). -- Note that it can involve projections as well, e.g. \(\pi_1 t \equiv \pi_2 t\). | RecBottom -- ^ Bottom tope eliminator: \(\mathsf{rec}_\bot : A\). - | RecOr (Term var a) (Term var a) (Term var a) (Term var a) + | RecOr (Term ann var a) (Term ann var a) (Term ann var a) (Term ann var a) -- ^ Tope disjunction eliminator: \(\mathsf{rec}^{\psi,\phi}_\lor(a_\psi, a_\phi)\). | ExtensionType - (Term var a) (Scope1Term var a) (Scope1Term var a) (Scope1Term var a) (Scope1Term var a) + (Term ann var a) (Scope1Term ann var a) (Scope1Term ann var a) (Scope1Term ann var a) (Scope1Term ann var a) -- ^ Extension type \( \left\langle \prod_{t : I | psi} A(t) \rvert^{\phi}_{a(t)} \right\rangle \) corresponding to @ExtensionType t cI psi tA phi a@. | Cube2 @@ -99,19 +100,20 @@ data Term var a | Cube2_1 -- ^ End of directed interval: \(1 : \mathbb{2}\). - | TopeLEQ (Term var a) (Term var a) + | TopeLEQ (Term ann var a) (Term ann var a) -- ^ Inequality tope: \(t \leq s\). deriving (Functor, Foldable) -instance Applicative (Term var) where +instance Applicative (Term ann var) where pure = Variable (<*>) = ap -instance Monad (Term var) where +instance Monad (Term ann var) where return = Variable t >>= f = case t of + Annotated ann t' -> Annotated ann (t' >>= f) Variable x -> f x Universe -> Universe @@ -159,7 +161,7 @@ deriveOrd1 ''Term deriveRead1 ''Term deriveShow1 ''Term -instance (Eq var, Eq a) => Eq (Term var a) where (==) = eq1 -instance (Ord var, Ord a) => Ord (Term var a) where compare = compare1 -instance (Show var, Show a) => Show (Term var a) where showsPrec = showsPrec1 -instance (Read var, Read a) => Read (Term var a) where readsPrec = readsPrec1 +instance (Eq ann, Eq var, Eq a) => Eq (Term ann var a) where (==) = eq1 +instance (Ord ann, Ord var, Ord a) => Ord (Term ann var a) where compare = compare1 +instance (Show ann, Show var, Show a) => Show (Term ann var a) where showsPrec = showsPrec1 +instance (Read ann, Read var, Read a) => Read (Term ann var a) where readsPrec = readsPrec1 diff --git a/rzk/src/Rzk/Simple/Syntax/Var.hs b/rzk/src/Rzk/Simple/Syntax/Var.hs index 3d944ff17..0c1aa4b36 100644 --- a/rzk/src/Rzk/Simple/Syntax/Var.hs +++ b/rzk/src/Rzk/Simple/Syntax/Var.hs @@ -1,15 +1,16 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} module Rzk.Simple.Syntax.Var where -import Data.Char (chr, ord) -import Data.Coerce (coerce) -import Data.String (IsString (..)) -import Data.Text (Text) -import qualified Data.Text as Text +import Data.Char (chr, ord) +import Data.Coerce (coerce) +import Data.Hashable (Hashable) +import Data.String (IsString (..)) +import Data.Text (Text) +import qualified Data.Text as Text -- | Standard type of variables. newtype Var = Var { getVar :: Text } - deriving (Eq, IsString) + deriving (Eq, Ord, Hashable, IsString) instance Show Var where show = Text.unpack . getVar From 9b0f9a03cfaff355a9caf2bd3a53534102f7118c Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 20 Feb 2021 19:22:22 +0300 Subject: [PATCH 05/10] Add evaluationg with memoization of WHNF --- rzk/package.yaml | 3 +- rzk/rzk.cabal | 14 +- rzk/src/Rzk/Simple/Evaluator.hs | 366 ++++++++++++++++-------------- rzk/src/Rzk/Simple/Syntax/Term.hs | 9 +- 4 files changed, 217 insertions(+), 175 deletions(-) diff --git a/rzk/package.yaml b/rzk/package.yaml index 2e0356466..a0941a551 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -4,7 +4,7 @@ github: "fizruk/rzk" license: BSD3 author: "Nikolai Kudasov" maintainer: "nickolay.kudasov@gmail.com" -copyright: "2020 Nikolai Kudasov" +copyright: "2020-2021 Nikolai Kudasov" extra-source-files: - README.md @@ -34,6 +34,7 @@ dependencies: - prettyprinter - prettyprinter-ansi-terminal - ansi-terminal +- hashable library: source-dirs: src diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index 87059f614..ff8e5e640 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -4,7 +4,7 @@ cabal-version: 1.12 -- -- see: https://github.com/sol/hpack -- --- hash: 377d77461ef09bbb3140b2714aef9a45be530905fd1e4b0dccbea665ac85bc38 +-- hash: 19633eb32342102057b2c107aed4c10bb65d863dc5e13269ee3dd4e7f9928628 name: rzk version: 0.1.0.0 @@ -48,10 +48,12 @@ library src ghc-options: -Wall -fno-warn-type-defaults -O2 build-depends: - ansi-terminal + MemoTrie + , ansi-terminal , base >=4.7 && <5 , bound , deriving-compat + , hashable , mtl , parsers , prettyprinter @@ -69,10 +71,12 @@ executable rzk app ghc-options: -Wall -fno-warn-type-defaults -O2 -threaded -rtsopts -with-rtsopts=-N build-depends: - ansi-terminal + MemoTrie + , ansi-terminal , base >=4.7 && <5 , bound , deriving-compat + , hashable , mtl , parsers , prettyprinter @@ -92,10 +96,12 @@ test-suite rzk-test test ghc-options: -Wall -fno-warn-type-defaults -O2 -threaded -rtsopts -with-rtsopts=-N build-depends: - ansi-terminal + MemoTrie + , ansi-terminal , base >=4.7 && <5 , bound , deriving-compat + , hashable , mtl , parsers , prettyprinter diff --git a/rzk/src/Rzk/Simple/Evaluator.hs b/rzk/src/Rzk/Simple/Evaluator.hs index f05327350..b4202f7f8 100644 --- a/rzk/src/Rzk/Simple/Evaluator.hs +++ b/rzk/src/Rzk/Simple/Evaluator.hs @@ -1,183 +1,217 @@ -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} module Rzk.Simple.Evaluator where -import qualified Data.MemoTrie as MemoTrie - import Bound +import Control.Applicative (liftA2) +import Control.Monad.Identity +import Control.Monad.Reader (ReaderT, asks, runReaderT) +import Control.Monad.State import Control.Monad.Trans (lift) import Data.Hashable (Hashable) +import Data.HashMap.Strict (HashMap) import qualified Data.HashMap.Strict as HashMap import Rzk.Simple.Syntax.Term -data EvalContext ann var a b = EvalContext - { definitionOf :: a -> Either b (Term ann var a) - } - -emptyEvalContext :: EvalContext ann var a a -emptyEvalContext = EvalContext - { definitionOf = Left - } - -mkEvalContext - :: (Eq a, Hashable a) - => (a -> b) - -> [(a, Term ann var a)] - -> EvalContext ann var a b -mkEvalContext convert dict = EvalContext - { definitionOf = \x -> - case HashMap.lookup x definitions of - Nothing -> Left (convert x) - Just t -> Right t - } - where - definitions = HashMap.fromList dict - -nfWith :: forall ann var a. EvalContext ann var a a -> Term ann var a -> Term ann var a -nfWith context@EvalContext{..} = nf' +class Monad m => MonadLookup k v m where + lookupM :: k -> m (Maybe v) + +instance MonadLookup k v Identity where + lookupM = const (return Nothing) + +newtype ForgetLookupT m a = ForgetLookupT { runForgetLookupT :: m a } + deriving (Functor, Applicative, Monad) + +instance Monad m => MonadLookup k v (ForgetLookupT m) where + lookupM = const (return Nothing) + +newtype HashMapLookupT k v m a + = HashMapLookupT { runHashMapLookupT :: ReaderT (HashMap k v) m a } + deriving (Functor, Applicative, Monad) + +instance (Eq k, Hashable k, Monad m) => MonadLookup k v (HashMapLookupT k v m) where + lookupM = HashMapLookupT . asks . HashMap.lookup + +data Thunk a + = Unevaluated a + | Evaluating + | Evaluated a + +newtype WhnfHashMapLookupT ann var a m b + = WhnfHashMapLookupT { runWhnfHashMapLookupT :: StateT (HashMap a (Thunk (Term ann var a))) m b } + deriving (Functor, Applicative, Monad) + +instance (Eq a, Hashable a, Monad m) => MonadLookup a (Term ann var a) (WhnfHashMapLookupT ann var a m) where + lookupM x = WhnfHashMapLookupT $ do + gets (HashMap.lookup x) >>= \case + Nothing -> return Nothing + Just (Unevaluated t) -> do + modify (HashMap.insert x Evaluating) + t' <- runWhnfHashMapLookupT (whnfM t) + modify (HashMap.insert x (Evaluated t')) + return (Just t') + Just (Evaluated t) -> return (Just t) + Just Evaluating -> error "unable to evaluate self-referencing value" + +nfM + :: MonadLookup a (Term ann var a) m + => Term ann var a -> m (Term ann var a) +nfM = nf' where - whnf' = whnfWith context - - -- definitionOf' - -- :: Var x (Term ann var a) - -- -> Either (Var x (Term ann var a)) (Term ann var (Var x (Term ann var a))) - definitionOf' = \case - B b -> Left (B b) - F (Variable y) -> - case definitionOf y of - Left z -> Left (F (pure z)) - Right t -> Right (pure (F t)) - F t -> Right (F . pure <$> t) - - -- nfScoped :: Scope x (Term ann var) a -> Scope x (Term ann var) b - nfScoped = Scope . nfWith context' . unscope + nfScoped + :: MonadLookup a (Term ann var a) m + => Scope b (Term ann var) a -> m (Scope b (Term ann var) a) + nfScoped = fmap Scope . nfScoped' . unscope where - -- context' :: EvalContext ann var (Var x (Term ann var a)) (Var x (Term ann var b)) - context' = context { definitionOf = definitionOf' } + nfScoped' f = runForgetLookupT (nfM f) >>= traverse (traverse nfM) + nf' :: MonadLookup a (Term ann var a) m => Term ann var a -> m (Term ann var a) nf' = \case - t@(Variable x) -> - case definitionOf x of - Left y -> Variable y - Right t' -> nf' t' - Annotated ann t -> Annotated ann (nf' t) - App t1 t2 -> - case whnf' t1 of - Lambda _a _phi body -> nf' (instantiate1 t2 body) - t1' -> App (nf' t1') (nf' t2) - - First t -> - case whnf' t of - Pair t1 _t2 -> nf' t1 - t' -> nf' t' - Second t -> - case whnf' t of - Pair _t1 t2 -> nf' t2 - t' -> nf' t' - - IdJ tA a tC d x p -> - case whnf' p of - Refl{} -> nf' d - p' -> IdJ (nf' tA) (nf' a) (nf' tC) (nf' d) (nf' x) (nf' p') - - e@Universe -> e - - ExtensionType tC psi tA phi a -> - ExtensionType (nf' tC) (nfScoped psi) (nfScoped tA) (nfScoped phi) (nfScoped a) - Pi t' -> Pi (nf' t') - Lambda a phi body - -> Lambda (fmap nf' a) (fmap nfScoped phi) (nfScoped body) - - Sigma t' -> Sigma (nf' t') - Pair t1 t2 -> Pair (nf' t1) (nf' t2) - - IdType a x y -> IdType (nf' a) (nf' x) (nf' y) - Refl a x -> Refl (fmap nf' a) (nf' x) - - Cube -> Cube - CubeUnit -> CubeUnit - CubeUnitStar -> CubeUnitStar - - CubeProd t1 t2 -> CubeProd (nf' t1) (nf' t2) - - Tope -> Tope - TopeTop -> TopeTop - TopeBottom -> TopeBottom - TopeOr t1 t2 -> TopeOr (nf' t1) (nf' t2) - TopeAnd t1 t2 -> TopeAnd (nf' t1) (nf' t2) - TopeEQ t1 t2 -> TopeEQ (nf' t1) (nf' t2) - - RecBottom -> RecBottom - RecOr psi phi t1 t2 -> RecOr (nf' psi) (nf' phi) (nf' t1) (nf' t2) - - Cube2 -> Cube2 - Cube2_0 -> Cube2_0 - Cube2_1 -> Cube2_1 - - TopeLEQ t1 t2 -> TopeLEQ (nf' t1) (nf' t2) - -whnfWith :: EvalContext ann var a a -> Term ann var a -> Term ann var a -whnfWith EvalContext{..} = whnf' + t@(Variable x) -> lookupM x >>= \case + Nothing -> return t + Just t' -> nf' t' + Annotated ann t -> Annotated ann <$> nf' t + App t1 t2 -> whnfM t1 >>= \case + Lambda _a _phi body -> nf' (instantiate1 t2 body) + t1' -> App <$> nf' t1' <*> nf' t2 + + First t -> whnfM t >>= \case + Pair t1 _t2 -> nf' t1 + t' -> nf' t' + Second t -> whnfM t >>= \case + Pair _t1 t2 -> nf' t2 + t' -> nf' t' + + IdJ tA a tC d x p -> whnfM p >>= \case + Refl{} -> nf' d + p' -> IdJ <$> nf' tA <*> nf' a <*> nf' tC <*> nf' d <*> nf' x <*> nf' p' + + e@Universe -> return e + + ExtensionType tC psi tA phi a -> ExtensionType + <$> nf' tC + <*> nfScoped psi + <*> nfScoped tA + <*> nfScoped phi + <*> nfScoped a + + Pi t' -> Pi <$> nf' t' + Lambda a phi body -> Lambda + <$> traverse nf' a + <*> traverse nfScoped phi + <*> nfScoped body + + Sigma t' -> Sigma <$> nf' t' + Pair t1 t2 -> Pair <$> nf' t1 <*> nf' t2 + + IdType a x y -> IdType <$> nf' a <*> nf' x <*> nf' y + Refl a x -> Refl <$> traverse nf' a <*> nf' x + + Cube -> return Cube + CubeUnit -> return CubeUnit + CubeUnitStar -> return CubeUnitStar + + CubeProd t1 t2 -> CubeProd <$> nf' t1 <*> nf' t2 + + Tope -> return Tope + TopeTop -> return TopeTop + TopeBottom -> return TopeBottom + TopeOr t1 t2 -> TopeOr <$> nf' t1 <*> nf' t2 + TopeAnd t1 t2 -> TopeAnd <$> nf' t1 <*> nf' t2 + TopeEQ t1 t2 -> TopeEQ <$> nf' t1 <*> nf' t2 + + RecBottom -> return RecBottom + RecOr psi phi t1 t2 -> RecOr <$> nf' psi <*> nf' phi <*> nf' t1 <*> nf' t2 + + Cube2 -> return Cube2 + Cube2_0 -> return Cube2_0 + Cube2_1 -> return Cube2_1 + + TopeLEQ t1 t2 -> TopeLEQ <$> nf' t1 <*> nf' t2 + +whnfM + :: MonadLookup a (Term ann var a) m + => Term ann var a -> m (Term ann var a) +whnfM = whnfM where - whnf' = \case - t@(Variable x) -> - case definitionOf x of - Left z -> pure z - Right t' -> whnf' t' - Annotated ann t -> Annotated ann (whnf' t) - App t1 t2 -> - case whnf' t1 of - Lambda _a _phi body -> whnf' (instantiate1 t2 body) - t1' -> App t1' t2 - - First t -> - case whnf' t of - Pair t1 _t2 -> whnf' t1 - t' -> t' - Second t -> - case whnf' t of - Pair _t1 t2 -> whnf' t2 - t' -> t' - - IdJ tA a tC d x p -> - case whnf' p of - Refl{} -> whnf' d - p' -> IdJ tA a tC d x p' - - t@Universe -> t - t@Lambda{} -> t - t@ExtensionType{} -> t - t@Pi{} -> t - t@Sigma{} -> t - t@Pair{} -> t - - t@IdType{} -> t - t@Refl{} -> t - - t@Cube -> t - t@CubeUnit -> t - t@CubeUnitStar -> t - t@CubeProd{} -> t - - t@Tope -> t - t@TopeTop -> t - t@TopeBottom -> t - - t@TopeOr{} -> t - t@TopeAnd{} -> t - t@TopeEQ{} -> t - - t@RecBottom -> t - t@RecOr{} -> t - - t@Cube2 -> t - t@Cube2_0 -> t - t@Cube2_1 -> t - t@TopeLEQ{} -> t + whnfM = \case + t@(Variable x) -> lookupM x >>= \case + Nothing -> return t + Just t' -> whnfM t' + Annotated ann t -> Annotated ann <$> whnfM t + App t1 t2 -> whnfM t1 >>= \case + Lambda _a _phi body -> whnfM (instantiate1 t2 body) + t1' -> return (App t1' t2) + + First t -> whnfM t >>= \case + Pair t1 _t2 -> whnfM t1 + t' -> return t' + Second t -> whnfM t >>= \case + Pair _t1 t2 -> whnfM t2 + t' -> return t' + + IdJ tA a tC d x p -> whnfM p >>= \case + Refl{} -> whnfM d + p' -> return (IdJ tA a tC d x p') + + t@Universe -> return t + t@Lambda{} -> return t + t@ExtensionType{} -> return t + t@Pi{} -> return t + t@Sigma{} -> return t + t@Pair{} -> return t + + t@IdType{} -> return t + t@Refl{} -> return t + + t@Cube -> return t + t@CubeUnit -> return t + t@CubeUnitStar -> return t + t@CubeProd{} -> return t + + t@Tope -> return t + t@TopeTop -> return t + t@TopeBottom -> return t + + t@TopeOr{} -> return t + t@TopeAnd{} -> return t + t@TopeEQ{} -> return t + + t@RecBottom -> return t + t@RecOr{} -> return t + + t@Cube2 -> return t + t@Cube2_0 -> return t + t@Cube2_1 -> return t + t@TopeLEQ{} -> return t nf :: Term ann var a -> Term ann var a -nf = nfWith emptyEvalContext +nf = runIdentity . nfM whnf :: Term ann var a -> Term ann var a -whnf = whnfWith emptyEvalContext +whnf = runIdentity . whnfM + +nfWith :: (Eq a, Hashable a) => [(a, Term ann var a)] -> Term ann var a -> Term ann var a +nfWith definitions = runIdentity . flip runReaderT defs . runHashMapLookupT . nfM + where + defs = HashMap.fromList definitions + +whnfWith :: (Eq a, Hashable a) => [(a, Term ann var a)] -> Term ann var a -> Term ann var a +whnfWith definitions = runIdentity . flip runReaderT defs . runHashMapLookupT . whnfM + where + defs = HashMap.fromList definitions + +nfWith' :: (Eq a, Hashable a) => [(a, Term ann var a)] -> Term ann var a -> Term ann var a +nfWith' definitions = runIdentity . flip evalStateT defs . runWhnfHashMapLookupT . nfM + where + defs = Unevaluated <$> HashMap.fromList definitions + +whnfWith' :: (Eq a, Hashable a) => [(a, Term ann var a)] -> Term ann var a -> Term ann var a +whnfWith' definitions = runIdentity . flip evalStateT defs . runWhnfHashMapLookupT . whnfM + where + defs = Unevaluated <$> HashMap.fromList definitions diff --git a/rzk/src/Rzk/Simple/Syntax/Term.hs b/rzk/src/Rzk/Simple/Syntax/Term.hs index d4469c4eb..d6e8bb090 100644 --- a/rzk/src/Rzk/Simple/Syntax/Term.hs +++ b/rzk/src/Rzk/Simple/Syntax/Term.hs @@ -1,6 +1,7 @@ -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE TemplateHaskell #-} module Rzk.Simple.Syntax.Term where import Bound @@ -103,7 +104,7 @@ data Term ann var a | TopeLEQ (Term ann var a) (Term ann var a) -- ^ Inequality tope: \(t \leq s\). - deriving (Functor, Foldable) + deriving (Functor, Foldable, Traversable) instance Applicative (Term ann var) where pure = Variable From 8036adf5f49ec93b1b07ed7e26a84ccedd19d2f3 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 20 Feb 2021 19:47:23 +0300 Subject: [PATCH 06/10] Add evaluationg with memoization of WHNF --- rzk/src/Rzk/Simple/Evaluator.hs | 126 +++++++++++++++++--------------- 1 file changed, 69 insertions(+), 57 deletions(-) diff --git a/rzk/src/Rzk/Simple/Evaluator.hs b/rzk/src/Rzk/Simple/Evaluator.hs index b4202f7f8..d76de004e 100644 --- a/rzk/src/Rzk/Simple/Evaluator.hs +++ b/rzk/src/Rzk/Simple/Evaluator.hs @@ -7,16 +7,18 @@ {-# LANGUAGE ScopedTypeVariables #-} module Rzk.Simple.Evaluator where -import Bound -import Control.Applicative (liftA2) +import Bound.Scope +import Control.Monad.Except import Control.Monad.Identity import Control.Monad.Reader (ReaderT, asks, runReaderT) import Control.Monad.State -import Control.Monad.Trans (lift) import Data.Hashable (Hashable) import Data.HashMap.Strict (HashMap) import qualified Data.HashMap.Strict as HashMap import Rzk.Simple.Syntax.Term +import Rzk.Simple.Syntax.Var + +import Text.Trifecta (Span, Spanned (..)) class Monad m => MonadLookup k v m where lookupM :: k -> m (Maybe v) @@ -58,6 +60,18 @@ instance (Eq a, Hashable a, Monad m) => MonadLookup a (Term ann var a) (WhnfHash Just (Evaluated t) -> return (Just t) Just Evaluating -> error "unable to evaluate self-referencing value" +data UndefinedError k = UndefinedError k + deriving (Show) + +newtype EnsureDefinedT k m a = EnsureDefinedT { runEnsureDefinedT :: ExceptT (UndefinedError k) m a } + deriving (Functor, Applicative, Monad) + +instance (MonadLookup k v m) => MonadLookup k v (EnsureDefinedT k m) where + lookupM x = EnsureDefinedT $ do + lift (lookupM x) >>= \case + Nothing -> throwError (UndefinedError x) + Just t -> return (Just t) + nfM :: MonadLookup a (Term ann var a) m => Term ann var a -> m (Term ann var a) @@ -137,58 +151,56 @@ nfM = nf' whnfM :: MonadLookup a (Term ann var a) m => Term ann var a -> m (Term ann var a) -whnfM = whnfM - where - whnfM = \case - t@(Variable x) -> lookupM x >>= \case - Nothing -> return t - Just t' -> whnfM t' - Annotated ann t -> Annotated ann <$> whnfM t - App t1 t2 -> whnfM t1 >>= \case - Lambda _a _phi body -> whnfM (instantiate1 t2 body) - t1' -> return (App t1' t2) - - First t -> whnfM t >>= \case - Pair t1 _t2 -> whnfM t1 - t' -> return t' - Second t -> whnfM t >>= \case - Pair _t1 t2 -> whnfM t2 - t' -> return t' - - IdJ tA a tC d x p -> whnfM p >>= \case - Refl{} -> whnfM d - p' -> return (IdJ tA a tC d x p') - - t@Universe -> return t - t@Lambda{} -> return t - t@ExtensionType{} -> return t - t@Pi{} -> return t - t@Sigma{} -> return t - t@Pair{} -> return t - - t@IdType{} -> return t - t@Refl{} -> return t - - t@Cube -> return t - t@CubeUnit -> return t - t@CubeUnitStar -> return t - t@CubeProd{} -> return t - - t@Tope -> return t - t@TopeTop -> return t - t@TopeBottom -> return t - - t@TopeOr{} -> return t - t@TopeAnd{} -> return t - t@TopeEQ{} -> return t - - t@RecBottom -> return t - t@RecOr{} -> return t - - t@Cube2 -> return t - t@Cube2_0 -> return t - t@Cube2_1 -> return t - t@TopeLEQ{} -> return t +whnfM = \case + t@(Variable x) -> lookupM x >>= \case + Nothing -> return t + Just t' -> whnfM t' + Annotated ann t -> Annotated ann <$> whnfM t + App t1 t2 -> whnfM t1 >>= \case + Lambda _a _phi body -> whnfM (instantiate1 t2 body) + t1' -> return (App t1' t2) + + First t -> whnfM t >>= \case + Pair t1 _t2 -> whnfM t1 + t' -> return t' + Second t -> whnfM t >>= \case + Pair _t1 t2 -> whnfM t2 + t' -> return t' + + IdJ tA a tC d x p -> whnfM p >>= \case + Refl{} -> whnfM d + p' -> return (IdJ tA a tC d x p') + + t@Universe -> return t + t@Lambda{} -> return t + t@ExtensionType{} -> return t + t@Pi{} -> return t + t@Sigma{} -> return t + t@Pair{} -> return t + + t@IdType{} -> return t + t@Refl{} -> return t + + t@Cube -> return t + t@CubeUnit -> return t + t@CubeUnitStar -> return t + t@CubeProd{} -> return t + + t@Tope -> return t + t@TopeTop -> return t + t@TopeBottom -> return t + + t@TopeOr{} -> return t + t@TopeAnd{} -> return t + t@TopeEQ{} -> return t + + t@RecBottom -> return t + t@RecOr{} -> return t + + t@Cube2 -> return t + t@Cube2_0 -> return t + t@Cube2_1 -> return t + t@TopeLEQ{} -> return t nf :: Term ann var a -> Term ann var a nf = runIdentity . nfM @@ -211,7 +223,7 @@ nfWith' definitions = runIdentity . flip evalStateT defs . runWhnfHashMapLookupT where defs = Unevaluated <$> HashMap.fromList definitions -whnfWith' :: (Eq a, Hashable a) => [(a, Term ann var a)] -> Term ann var a -> Term ann var a -whnfWith' definitions = runIdentity . flip evalStateT defs . runWhnfHashMapLookupT . whnfM +whnfWith' :: (Eq a, Hashable a) => [(a, Term ann var a)] -> Term ann var a -> Either (UndefinedError a) (Term ann var a) +whnfWith' definitions = runIdentity . flip evalStateT defs . runWhnfHashMapLookupT . runExceptT . runEnsureDefinedT . whnfM where defs = Unevaluated <$> HashMap.fromList definitions From 089f3d275fb321067ff677ae5fbccf98dc7a83d3 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sun, 21 Feb 2021 23:50:13 +0300 Subject: [PATCH 07/10] Add AnnotatedTerm and use annotation to report nicer undefined variable errors --- rzk/rzk.cabal | 13 +- rzk/src/Rzk/Simple/Evaluator.hs | 283 +++++++++++++++++------------- rzk/src/Rzk/Simple/Parser.hs | 162 +++++++++-------- rzk/src/Rzk/Simple/Pretty.hs | 80 +++++---- rzk/src/Rzk/Simple/Syntax/Term.hs | 189 +++++++++++++------- rzk/src/Rzk/Simple/Syntax/Var.hs | 14 +- 6 files changed, 437 insertions(+), 304 deletions(-) diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index ff8e5e640..f99793433 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -4,7 +4,7 @@ cabal-version: 1.12 -- -- see: https://github.com/sol/hpack -- --- hash: 19633eb32342102057b2c107aed4c10bb65d863dc5e13269ee3dd4e7f9928628 +-- hash: 2ae15fb94b314d3beeb9cfdc7449e6c7550bf4ce4406e88e3910951feac7f9b5 name: rzk version: 0.1.0.0 @@ -13,7 +13,7 @@ homepage: https://github.com/fizruk/rzk#readme bug-reports: https://github.com/fizruk/rzk/issues author: Nikolai Kudasov maintainer: nickolay.kudasov@gmail.com -copyright: 2020 Nikolai Kudasov +copyright: 2020-2021 Nikolai Kudasov license: BSD3 build-type: Simple extra-source-files: @@ -48,8 +48,7 @@ library src ghc-options: -Wall -fno-warn-type-defaults -O2 build-depends: - MemoTrie - , ansi-terminal + ansi-terminal , base >=4.7 && <5 , bound , deriving-compat @@ -71,8 +70,7 @@ executable rzk app ghc-options: -Wall -fno-warn-type-defaults -O2 -threaded -rtsopts -with-rtsopts=-N build-depends: - MemoTrie - , ansi-terminal + ansi-terminal , base >=4.7 && <5 , bound , deriving-compat @@ -96,8 +94,7 @@ test-suite rzk-test test ghc-options: -Wall -fno-warn-type-defaults -O2 -threaded -rtsopts -with-rtsopts=-N build-depends: - MemoTrie - , ansi-terminal + ansi-terminal , base >=4.7 && <5 , bound , deriving-compat diff --git a/rzk/src/Rzk/Simple/Evaluator.hs b/rzk/src/Rzk/Simple/Evaluator.hs index d76de004e..f858cdcd1 100644 --- a/rzk/src/Rzk/Simple/Evaluator.hs +++ b/rzk/src/Rzk/Simple/Evaluator.hs @@ -5,20 +5,31 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} module Rzk.Simple.Evaluator where +import qualified Bound import Bound.Scope import Control.Monad.Except import Control.Monad.Identity -import Control.Monad.Reader (ReaderT, asks, runReaderT) +import Control.Monad.Reader (ReaderT, asks, + runReaderT) import Control.Monad.State -import Data.Hashable (Hashable) -import Data.HashMap.Strict (HashMap) -import qualified Data.HashMap.Strict as HashMap +import Data.Hashable (Hashable) +import Data.HashMap.Strict (HashMap) +import qualified Data.HashMap.Strict as HashMap import Rzk.Simple.Syntax.Term import Rzk.Simple.Syntax.Var -import Text.Trifecta (Span, Spanned (..)) +import Text.Trifecta (Span, Spanned (..)) +import qualified Text.Trifecta as Trifecta + +import qualified Data.Text.Lazy as Text +import Data.Text.Prettyprint.Doc (Doc, + defaultLayoutOptions, + layoutPretty) +import Data.Text.Prettyprint.Doc.Render.Terminal (AnsiStyle, + renderLazy) class Monad m => MonadLookup k v m where lookupM :: k -> m (Maybe v) @@ -45,10 +56,10 @@ data Thunk a | Evaluated a newtype WhnfHashMapLookupT ann var a m b - = WhnfHashMapLookupT { runWhnfHashMapLookupT :: StateT (HashMap a (Thunk (Term ann var a))) m b } + = WhnfHashMapLookupT { runWhnfHashMapLookupT :: StateT (HashMap a (Thunk (AnnotatedTerm ann var a))) m b } deriving (Functor, Applicative, Monad) -instance (Eq a, Hashable a, Monad m) => MonadLookup a (Term ann var a) (WhnfHashMapLookupT ann var a m) where +instance (Eq a, Hashable a, Monad m) => MonadLookup a (AnnotatedTerm ann var a) (WhnfHashMapLookupT ann var a m) where lookupM x = WhnfHashMapLookupT $ do gets (HashMap.lookup x) >>= \case Nothing -> return Nothing @@ -63,6 +74,10 @@ instance (Eq a, Hashable a, Monad m) => MonadLookup a (Term ann var a) (WhnfHash data UndefinedError k = UndefinedError k deriving (Show) +ppUndefinedError :: UndefinedError SpannedVar -> Doc AnsiStyle +ppUndefinedError (UndefinedError (SpannedVar (x :~ span))) + = Trifecta.prettyRendering (Trifecta.render (Trifecta.Fixit span "undefined variable")) + newtype EnsureDefinedT k m a = EnsureDefinedT { runEnsureDefinedT :: ExceptT (UndefinedError k) m a } deriving (Functor, Applicative, Monad) @@ -72,158 +87,182 @@ instance (MonadLookup k v m) => MonadLookup k v (EnsureDefinedT k m) where Nothing -> throwError (UndefinedError x) Just t -> return (Just t) +newtype BoundedVarLookupT m a = BoundedVarLookupT { runBoundedVarLookupT :: m a } + deriving (Functor, Applicative, Monad) + +instance MonadLookup k (AnnotatedTerm ann var k) m + => MonadLookup (Bound.Var b k) (AnnotatedTerm ann var (Bound.Var b k)) (BoundedVarLookupT m) where + lookupM x = BoundedVarLookupT $ do + case x of + Bound.B b -> return Nothing + Bound.F y -> fmap (fmap (fmap Bound.F)) (lookupM y) + +nfScopedM + :: MonadLookup a (AnnotatedTerm ann var a) m + => Scope b (AnnotatedTerm ann var) a -> m (Scope b (AnnotatedTerm ann var) a) +nfScopedM = fmap toScope . runBoundedVarLookupT . nfM . fromScope + nfM - :: MonadLookup a (Term ann var a) m - => Term ann var a -> m (Term ann var a) -nfM = nf' - where - nfScoped - :: MonadLookup a (Term ann var a) m - => Scope b (Term ann var) a -> m (Scope b (Term ann var) a) - nfScoped = fmap Scope . nfScoped' . unscope - where - nfScoped' f = runForgetLookupT (nfM f) >>= traverse (traverse nfM) - - nf' :: MonadLookup a (Term ann var a) m => Term ann var a -> m (Term ann var a) - nf' = \case - t@(Variable x) -> lookupM x >>= \case - Nothing -> return t - Just t' -> nf' t' - Annotated ann t -> Annotated ann <$> nf' t - App t1 t2 -> whnfM t1 >>= \case - Lambda _a _phi body -> nf' (instantiate1 t2 body) - t1' -> App <$> nf' t1' <*> nf' t2 - - First t -> whnfM t >>= \case - Pair t1 _t2 -> nf' t1 - t' -> nf' t' - Second t -> whnfM t >>= \case - Pair _t1 t2 -> nf' t2 - t' -> nf' t' - - IdJ tA a tC d x p -> whnfM p >>= \case - Refl{} -> nf' d - p' -> IdJ <$> nf' tA <*> nf' a <*> nf' tC <*> nf' d <*> nf' x <*> nf' p' - - e@Universe -> return e - - ExtensionType tC psi tA phi a -> ExtensionType - <$> nf' tC - <*> nfScoped psi - <*> nfScoped tA - <*> nfScoped phi - <*> nfScoped a - - Pi t' -> Pi <$> nf' t' - Lambda a phi body -> Lambda - <$> traverse nf' a - <*> traverse nfScoped phi - <*> nfScoped body - - Sigma t' -> Sigma <$> nf' t' - Pair t1 t2 -> Pair <$> nf' t1 <*> nf' t2 - - IdType a x y -> IdType <$> nf' a <*> nf' x <*> nf' y - Refl a x -> Refl <$> traverse nf' a <*> nf' x - - Cube -> return Cube - CubeUnit -> return CubeUnit - CubeUnitStar -> return CubeUnitStar - - CubeProd t1 t2 -> CubeProd <$> nf' t1 <*> nf' t2 - - Tope -> return Tope - TopeTop -> return TopeTop - TopeBottom -> return TopeBottom - TopeOr t1 t2 -> TopeOr <$> nf' t1 <*> nf' t2 - TopeAnd t1 t2 -> TopeAnd <$> nf' t1 <*> nf' t2 - TopeEQ t1 t2 -> TopeEQ <$> nf' t1 <*> nf' t2 - - RecBottom -> return RecBottom - RecOr psi phi t1 t2 -> RecOr <$> nf' psi <*> nf' phi <*> nf' t1 <*> nf' t2 - - Cube2 -> return Cube2 - Cube2_0 -> return Cube2_0 - Cube2_1 -> return Cube2_1 - - TopeLEQ t1 t2 -> TopeLEQ <$> nf' t1 <*> nf' t2 + :: MonadLookup a (AnnotatedTerm ann var a) m + => AnnotatedTerm ann var a -> m (AnnotatedTerm ann var a) +nfM (AnnotatedTerm ann tt) = fmap (appendAnnotation ann) $ case tt of + t@(Variable x) -> lookupM x >>= \case + Nothing -> return (unannotated t) + Just t' -> nfM t' + App t1 t2 -> whnfM t1 >>= \case + AnnotatedTerm _ (Lambda _a _phi body) -> nfM (instantiate1 t2 body) + t1' -> unannotated <$> (App <$> nfM t1' <*> nfM t2) + + First t -> whnfM t >>= \case + AnnotatedTerm _ (Pair t1 _t2) -> nfM t1 + t' -> nfM t' + Second t -> whnfM t >>= \case + AnnotatedTerm _ (Pair _t1 t2) -> nfM t2 + t' -> nfM t' + + IdJ tA a tC d x p -> whnfM p >>= \case + AnnotatedTerm _ Refl{} -> nfM d + p' -> unannotated <$> + (IdJ <$> nfM tA <*> nfM a <*> nfM tC <*> nfM d <*> nfM x <*> nfM p') + + t@Universe -> return (unannotated t) + + ExtensionType tC psi tA phi a -> fmap unannotated $ ExtensionType + <$> nfM tC + <*> nfScopedM psi + <*> nfScopedM tA + <*> nfScopedM phi + <*> nfScopedM a + + Pi t' -> fmap unannotated $ Pi <$> nfM t' + Lambda a phi body -> fmap unannotated $ Lambda + <$> traverse nfM a + <*> traverse nfScopedM phi + <*> nfScopedM body + + Sigma t' -> fmap unannotated $ Sigma <$> nfM t' + Pair t1 t2 -> fmap unannotated $ Pair <$> nfM t1 <*> nfM t2 + + IdType a x y -> fmap unannotated $ IdType <$> nfM a <*> nfM x <*> nfM y + Refl a x -> fmap unannotated $ Refl <$> traverse nfM a <*> nfM x + + Cube -> return (unannotated Cube) + CubeUnit -> return (unannotated CubeUnit) + CubeUnitStar -> return (unannotated CubeUnitStar) + + CubeProd t1 t2 -> fmap unannotated $ CubeProd <$> nfM t1 <*> nfM t2 + + Tope -> return (unannotated Tope) + TopeTop -> return (unannotated TopeTop) + TopeBottom -> return (unannotated TopeBottom) + TopeOr t1 t2 -> fmap unannotated $ TopeOr <$> nfM t1 <*> nfM t2 + TopeAnd t1 t2 -> fmap unannotated $ TopeAnd <$> nfM t1 <*> nfM t2 + TopeEQ t1 t2 -> fmap unannotated $ TopeEQ <$> nfM t1 <*> nfM t2 + + RecBottom -> return (unannotated RecBottom) + RecOr psi phi t1 t2 -> fmap unannotated $ RecOr <$> nfM psi <*> nfM phi <*> nfM t1 <*> nfM t2 + + Cube2 -> return (unannotated Cube2) + Cube2_0 -> return (unannotated Cube2_0) + Cube2_1 -> return (unannotated Cube2_1) + + TopeLEQ t1 t2 -> fmap unannotated $ TopeLEQ <$> nfM t1 <*> nfM t2 whnfM - :: MonadLookup a (Term ann var a) m - => Term ann var a -> m (Term ann var a) -whnfM = \case + :: MonadLookup a (AnnotatedTerm ann var a) m + => AnnotatedTerm ann var a -> m (AnnotatedTerm ann var a) +whnfM (AnnotatedTerm ann tt) = fmap (appendAnnotation ann) $ case tt of t@(Variable x) -> lookupM x >>= \case - Nothing -> return t + Nothing -> return (unannotated t) Just t' -> whnfM t' - Annotated ann t -> Annotated ann <$> whnfM t App t1 t2 -> whnfM t1 >>= \case - Lambda _a _phi body -> whnfM (instantiate1 t2 body) - t1' -> return (App t1' t2) + AnnotatedTerm _ (Lambda _a _phi body) -> whnfM (instantiate1 t2 body) + t1' -> return (unannotated (App t1' t2)) First t -> whnfM t >>= \case - Pair t1 _t2 -> whnfM t1 + AnnotatedTerm _ (Pair t1 _t2) -> whnfM t1 t' -> return t' Second t -> whnfM t >>= \case - Pair _t1 t2 -> whnfM t2 + AnnotatedTerm _ (Pair _t1 t2) -> whnfM t2 t' -> return t' IdJ tA a tC d x p -> whnfM p >>= \case - Refl{} -> whnfM d - p' -> return (IdJ tA a tC d x p') + AnnotatedTerm _ Refl{} -> whnfM d + p' -> return (unannotated (IdJ tA a tC d x p')) - t@Universe -> return t - t@Lambda{} -> return t - t@ExtensionType{} -> return t - t@Pi{} -> return t - t@Sigma{} -> return t - t@Pair{} -> return t + t@Universe -> return (unannotated t) + t@Lambda{} -> return (unannotated t) + t@ExtensionType{} -> return (unannotated t) + t@Pi{} -> return (unannotated t) + t@Sigma{} -> return (unannotated t) + t@Pair{} -> return (unannotated t) - t@IdType{} -> return t - t@Refl{} -> return t + t@IdType{} -> return (unannotated t) + t@Refl{} -> return (unannotated t) - t@Cube -> return t - t@CubeUnit -> return t - t@CubeUnitStar -> return t - t@CubeProd{} -> return t + t@Cube -> return (unannotated t) + t@CubeUnit -> return (unannotated t) + t@CubeUnitStar -> return (unannotated t) + t@CubeProd{} -> return (unannotated t) - t@Tope -> return t - t@TopeTop -> return t - t@TopeBottom -> return t + t@Tope -> return (unannotated t) + t@TopeTop -> return (unannotated t) + t@TopeBottom -> return (unannotated t) - t@TopeOr{} -> return t - t@TopeAnd{} -> return t - t@TopeEQ{} -> return t + t@TopeOr{} -> return (unannotated t) + t@TopeAnd{} -> return (unannotated t) + t@TopeEQ{} -> return (unannotated t) - t@RecBottom -> return t - t@RecOr{} -> return t + t@RecBottom -> return (unannotated t) + t@RecOr{} -> return (unannotated t) - t@Cube2 -> return t - t@Cube2_0 -> return t - t@Cube2_1 -> return t - t@TopeLEQ{} -> return t + t@Cube2 -> return (unannotated t) + t@Cube2_0 -> return (unannotated t) + t@Cube2_1 -> return (unannotated t) + t@TopeLEQ{} -> return (unannotated t) -nf :: Term ann var a -> Term ann var a +nf :: AnnotatedTerm ann var a -> AnnotatedTerm ann var a nf = runIdentity . nfM -whnf :: Term ann var a -> Term ann var a +whnf :: AnnotatedTerm ann var a -> AnnotatedTerm ann var a whnf = runIdentity . whnfM -nfWith :: (Eq a, Hashable a) => [(a, Term ann var a)] -> Term ann var a -> Term ann var a +nfWith :: (Eq a, Hashable a) => [(a, AnnotatedTerm ann var a)] -> AnnotatedTerm ann var a -> AnnotatedTerm ann var a nfWith definitions = runIdentity . flip runReaderT defs . runHashMapLookupT . nfM where defs = HashMap.fromList definitions -whnfWith :: (Eq a, Hashable a) => [(a, Term ann var a)] -> Term ann var a -> Term ann var a +whnfWith :: (Eq a, Hashable a) => [(a, AnnotatedTerm ann var a)] -> AnnotatedTerm ann var a -> AnnotatedTerm ann var a whnfWith definitions = runIdentity . flip runReaderT defs . runHashMapLookupT . whnfM where defs = HashMap.fromList definitions -nfWith' :: (Eq a, Hashable a) => [(a, Term ann var a)] -> Term ann var a -> Term ann var a +nfWith' :: (Eq a, Hashable a) => [(a, AnnotatedTerm ann var a)] -> AnnotatedTerm ann var a -> AnnotatedTerm ann var a nfWith' definitions = runIdentity . flip evalStateT defs . runWhnfHashMapLookupT . nfM where defs = Unevaluated <$> HashMap.fromList definitions -whnfWith' :: (Eq a, Hashable a) => [(a, Term ann var a)] -> Term ann var a -> Either (UndefinedError a) (Term ann var a) +whnfWith' :: (Eq a, Hashable a) => [(a, AnnotatedTerm ann var a)] -> AnnotatedTerm ann var a -> Either (UndefinedError a) (AnnotatedTerm ann var a) whnfWith' definitions = runIdentity . flip evalStateT defs . runWhnfHashMapLookupT . runExceptT . runEnsureDefinedT . whnfM where defs = Unevaluated <$> HashMap.fromList definitions + +withSpannedVars :: AnnotatedTerm Span var Var -> AnnotatedTerm Span var SpannedVar +withSpannedVars = mapWithAnnotation $ \[span] var -> SpannedVar (var :~ span) + +-- | +-- >>> zero = "\\s -> \\z -> z" :: AnnotatedTerm Span SpannedVar SpannedVar +-- >>> n3 = "\\s -> \\z -> s (s (s z))" :: AnnotatedTerm Span SpannedVar SpannedVar +-- >>> unsafeNfWith [("0", zero), ("3", n3)] "3 3" +-- Ξ»xβ‚€ β†’ Ξ»x₁ β†’ xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ (xβ‚€ x₁)))))))))))))))))))))))))) +unsafeNfWith + :: [(SpannedVar, AnnotatedTerm ann SpannedVar SpannedVar)] + -> AnnotatedTerm ann SpannedVar SpannedVar + -> AnnotatedTerm ann SpannedVar SpannedVar +unsafeNfWith definitions t = + case eval t of + Left err -> error ("\n" <> Text.unpack (renderLazy (layoutPretty defaultLayoutOptions (ppUndefinedError err)))) + Right res -> res + where + eval = runIdentity . flip evalStateT defs . runWhnfHashMapLookupT . runExceptT . runEnsureDefinedT . nfM + defs = Unevaluated <$> HashMap.fromList definitions diff --git a/rzk/src/Rzk/Simple/Parser.hs b/rzk/src/Rzk/Simple/Parser.hs index 87e397e2e..b08f07180 100644 --- a/rzk/src/Rzk/Simple/Parser.hs +++ b/rzk/src/Rzk/Simple/Parser.hs @@ -29,86 +29,97 @@ type RzkParser = Parser -- ** Term -parseSpanned :: RzkParser (Term Span Var Var) -> RzkParser (Term Span Var Var) -parseSpanned parser = annotateWithSpan <$> spanned parser +parseAnnotated :: RzkParser (Term Span SpannedVar SpannedVar) -> RzkParser (AnnotatedTerm Span SpannedVar SpannedVar) +parseAnnotated parser = annotateWithSpan <$> spanned parser where - annotateWithSpan (t :~ span') = Annotated span' t + annotateWithSpan (t :~ span) = AnnotatedTerm [span] t -rzkVar :: RzkParser Var -rzkVar = Var <$> rzkIdent +parseAnnotatedOp + :: RzkParser (AnnotatedTerm Span SpannedVar SpannedVar -> AnnotatedTerm Span SpannedVar SpannedVar -> Term Span SpannedVar SpannedVar) + -> RzkParser (AnnotatedTerm Span SpannedVar SpannedVar -> AnnotatedTerm Span SpannedVar SpannedVar -> AnnotatedTerm Span SpannedVar SpannedVar) +parseAnnotatedOp parser = annotateWithSpan <$> spanned parser + where + annotateWithSpan (f :~ span) x y = AnnotatedTerm [span] (f x y) + +rzkVar :: RzkParser SpannedVar +rzkVar = SpannedVar <$> spanned (Var <$> rzkIdent) -rzkTerm :: RzkParser (Term Span Var Var) +rzkTerm :: RzkParser (AnnotatedTerm Span SpannedVar SpannedVar) rzkTerm = "term" buildExpressionParser rzkOperatorTable rzkTerm' -rzkTerm' :: RzkParser (Term Span Var Var) +rzkTerm' :: RzkParser (AnnotatedTerm Span SpannedVar SpannedVar) rzkTerm' = "simple term" - try rzkTermPiType - <|> rzkTermPiShape - <|> try rzkTermPair + parseAnnotated ( + try rzkTermPiType + <|> rzkTermPiShape + <|> try rzkTermPair + ) <|> parens rzkTerm - <|> try rzkTermLambda - <|> try rzkTermLambdaShape - <|> rzkTermSigmaType - <|> rzkTermRefl - <|> rzkTermIdJ - <|> rzkTermRecOr - <|> rzkTermFirst - <|> rzkTermSecond - <|> rzkTermExtensionType - <|> rzkTermExtensionTypeFromCube - -- constants - <|> Universe <$ (symbol "U" <|> symbol "𝒰") - <|> Cube <$ symbol "CUBE" - <|> CubeUnitStar <$ (symbol "*_1" <|> symbol "⋆") - <|> Cube2 <$ (symbol "2" <|> symbol "𝟚") - <|> Cube2_0 <$ symbol "0_2" - <|> Cube2_1 <$ symbol "1_2" - <|> CubeUnit <$ (symbol "1" <|> symbol "πŸ™") - <|> Tope <$ symbol "TOPE" - <|> TopeTop <$ (symbol "TOP" <|> symbol "⊀") - <|> TopeBottom <$ (symbol "BOT" <|> symbol "βŠ₯") - <|> RecBottom <$ (symbol "recBOT" <|> symbol "recβŠ₯") - <|> rzkTermVar - -rzkTermVar :: RzkParser (Term Span Var Var) + <|> parseAnnotated ( + try rzkTermLambda + <|> try rzkTermLambdaShape + <|> rzkTermSigmaType + <|> rzkTermRefl + <|> rzkTermIdJ + <|> rzkTermRecOr + <|> rzkTermFirst + <|> rzkTermSecond + <|> rzkTermExtensionType + <|> rzkTermExtensionTypeFromCube + -- constants + <|> Universe <$ (symbol "U" <|> symbol "𝒰") + <|> Cube <$ symbol "CUBE" + <|> CubeUnitStar <$ (symbol "*_1" <|> symbol "⋆") + <|> Cube2 <$ (symbol "2" <|> symbol "𝟚") + <|> Cube2_0 <$ symbol "0_2" + <|> Cube2_1 <$ symbol "1_2" + <|> CubeUnit <$ (symbol "1" <|> symbol "πŸ™") + <|> Tope <$ symbol "TOPE" + <|> TopeTop <$ (symbol "TOP" <|> symbol "⊀") + <|> TopeBottom <$ (symbol "BOT" <|> symbol "βŠ₯") + <|> RecBottom <$ (symbol "recBOT" <|> symbol "recβŠ₯") + <|> rzkTermVar + ) + +rzkTermVar :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermVar = "variable" - (Variable <$> (Var <$> rzkIdent)) + (Variable <$> rzkVar) -rzkTermColonType :: RzkParser (Term Span Var Var, Term Span Var Var) +rzkTermColonType :: RzkParser (AnnotatedTerm Span SpannedVar SpannedVar, AnnotatedTerm Span SpannedVar SpannedVar) rzkTermColonType = do term <- rzkTerm colon type_ <- rzkTerm return (term, type_) -rzkTermColonType' :: RzkParser (Term Span Var Var, Maybe (Term Span Var Var)) +rzkTermColonType' :: RzkParser (AnnotatedTerm Span SpannedVar SpannedVar, Maybe (AnnotatedTerm Span SpannedVar SpannedVar)) rzkTermColonType' = try withType <|> withoutType where withType = fmap Just <$> rzkTermColonType withoutType = (\t -> (t, Nothing)) <$> rzkTerm -rzkVarColonType' :: RzkParser (Var, Maybe (Term Span Var Var)) +rzkVarColonType' :: RzkParser (SpannedVar, Maybe (AnnotatedTerm Span SpannedVar SpannedVar)) rzkVarColonType' = try withType <|> withoutType where withType = fmap Just <$> parens rzkVarColonType - withoutType = (\x -> (Var x, Nothing)) <$> rzkIdent + withoutType = (\x -> (x, Nothing)) <$> rzkVar -rzkVarColonType :: RzkParser (Var, Term Span Var Var) +rzkVarColonType :: RzkParser (SpannedVar, AnnotatedTerm Span SpannedVar SpannedVar) rzkVarColonType = do - x <- Var <$> rzkIdent + x <- rzkVar colon type_ <- rzkTerm return (x, type_) -rzkTermPiType :: RzkParser (Term Span Var Var) +rzkTermPiType :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermPiType = "dependent function type" do (var, a) <- parens rzkVarColonType symbol "->" <|> symbol "β†’" t <- rzkTerm - return (Pi (Lambda (Just a) Nothing (abstract1Name var t))) + return (Pi (unannotated (Lambda (Just a) Nothing (abstract1Name var t)))) -rzkTermPiShape :: RzkParser (Term Span Var Var) +rzkTermPiShape :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermPiShape = "dependent function type (from a shape)" do symbol "{" (var, i) <- rzkVarColonType' @@ -117,9 +128,9 @@ rzkTermPiShape = "dependent function type (from a shape)" do symbol "}" symbol "->" <|> symbol "β†’" a <- rzkTerm - return (Pi (Lambda i (Just (abstract1Name var phi)) (abstract1Name var a))) + return (Pi (unannotated (Lambda i (Just (abstract1Name var phi)) (abstract1Name var a)))) -rzkTermLambda :: RzkParser (Term Span Var Var) +rzkTermLambda :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermLambda = "lambda abstraction (anonymous function from a type)" do symbol "Ξ»" <|> symbol "\\" (x, a) <- rzkVarColonType' @@ -127,7 +138,7 @@ rzkTermLambda = "lambda abstraction (anonymous function from a type)" do t <- rzkTerm return (Lambda a Nothing (abstract1Name x t)) -rzkTermLambdaShape :: RzkParser (Term Span Var Var) +rzkTermLambdaShape :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermLambdaShape = "lambda abstraction (anonymous function from a shape)" do symbol "Ξ»" <|> symbol "\\" symbol "{" @@ -139,22 +150,22 @@ rzkTermLambdaShape = "lambda abstraction (anonymous function from a shape)" a <- rzkTerm return (Lambda (Just i) (Just (abstract1Name t phi)) (abstract1Name t a)) -rzkTermSigmaType :: RzkParser (Term Span Var Var) +rzkTermSigmaType :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermSigmaType = "dependent sum type" do symbol "βˆ‘" <|> symbol "Sigma" (x, a) <- parens rzkVarColonType symbol "," t <- rzkTerm - return (Sigma (Lambda (Just a) Nothing (abstract1Name x t))) + return (Sigma (unannotated (Lambda (Just a) Nothing (abstract1Name x t)))) -rzkTermRefl :: RzkParser (Term Span Var Var) +rzkTermRefl :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermRefl = do symbol "refl_{" (x, a) <- rzkTermColonType' symbol "}" return (Refl a x) -rzkTermIdJ :: RzkParser (Term Span Var Var) +rzkTermIdJ :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermIdJ = do symbol "idJ" symbol "(" @@ -167,7 +178,7 @@ rzkTermIdJ = do symbol ")" return (IdJ tA a tC d x p) -rzkTermRecOr :: RzkParser (Term Span Var Var) +rzkTermRecOr :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermRecOr = do symbol "recOR" <|> symbol "rec∨" symbol "(" @@ -178,17 +189,17 @@ rzkTermRecOr = do symbol ")" return (RecOr psi phi a b) -rzkTermFirst :: RzkParser (Term Span Var Var) +rzkTermFirst :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermFirst = do (symbol "first" <|> symbol "π₁") "π₁" First <$> rzkTerm -rzkTermSecond :: RzkParser (Term Span Var Var) +rzkTermSecond :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermSecond = do (symbol "second" <|> symbol "Ο€β‚‚") "Ο€β‚‚" Second <$> rzkTerm -rzkTermExtensionTypeFromCube :: RzkParser (Term Span Var Var) +rzkTermExtensionTypeFromCube :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermExtensionTypeFromCube = between (symbol "<(") (symbol ">") $ do t <- rzkVar symbol ":" @@ -205,11 +216,11 @@ rzkTermExtensionTypeFromCube = between (symbol "<(") (symbol ">") $ do return (phi, a) let (phi, a) = case mphi_a of Just x -> x - Nothing -> (TopeBottom, RecBottom) - return (ExtensionType cI (abstract1Name t TopeTop) (abstract1Name t tA) (abstract1Name t phi) (abstract1Name t a)) + Nothing -> (unannotated TopeBottom, unannotated RecBottom) + return (ExtensionType cI (abstract1Name t (unannotated TopeTop)) (abstract1Name t tA) (abstract1Name t phi) (abstract1Name t a)) -rzkTermExtensionType :: RzkParser (Term Span Var Var) +rzkTermExtensionType :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermExtensionType = between (symbol "<{") (symbol ">") $ do t <- rzkVar symbol ":" @@ -228,25 +239,25 @@ rzkTermExtensionType = between (symbol "<{") (symbol ">") $ do return (phi, a) let (phi, a) = case mphi_a of Just x -> x - Nothing -> (TopeBottom, RecBottom) + Nothing -> (unannotated TopeBottom, unannotated RecBottom) return (ExtensionType cI (abstract1Name t psi) (abstract1Name t tA) (abstract1Name t phi) (abstract1Name t a)) --- firstP :: Parser (Term Span Var Var) +-- firstP :: Parser (Term Span SpannedVar SpannedVar) -- firstP = do -- "first" <|> "π₁" -- skipSpace -- First <$> termParens True -- --- secondP :: Parser (Term Span Var Var) +-- secondP :: Parser (Term Span SpannedVar SpannedVar) -- secondP = do -- "second" <|> "Ο€β‚‚" -- skipSpace -- Second <$> termParens True -rzkTermPair :: RzkParser (Term Span Var Var) +rzkTermPair :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermPair = parens (Pair <$> rzkTerm <* comma <*> rzkTerm) -rzkTermApp :: RzkParser (Term Span Var Var) +rzkTermApp :: RzkParser (Term Span SpannedVar SpannedVar) rzkTermApp = do t1 <- rzkTerm t2 <- rzkTerm @@ -255,15 +266,15 @@ rzkTermApp = do rzkOperator :: RzkParser a -> RzkParser a rzkOperator op = op -- <* skipMany (satisfy isSpace) -rzkOperatorTable :: OperatorTable RzkParser (Term Span Var Var) +rzkOperatorTable :: OperatorTable RzkParser (AnnotatedTerm Span SpannedVar SpannedVar) rzkOperatorTable = - [ [ Infix (pure App) AssocLeft ] - , [ Infix (CubeProd <$ rzkOperator (symbol "*" <|> symbol "Γ—")) AssocLeft ] - , [ Infix (TopeEQ <$ rzkOperator (symbol "===" <|> symbol "≑")) AssocNone - , Infix (TopeLEQ <$ rzkOperator (symbol "<=" <|> symbol "≀")) AssocNone ] - , [ Infix (TopeAnd <$ rzkOperator (symbol "/\\" <|> symbol "∧")) AssocLeft ] - , [ Infix (TopeOr <$ rzkOperator (symbol "\\/" <|> symbol "∨")) AssocLeft ] - , [ Infix (rzkOperator $ do + [ [ Infix (parseAnnotatedOp $ pure App) AssocLeft ] + , [ Infix (parseAnnotatedOp $ CubeProd <$ rzkOperator (symbol "*" <|> symbol "Γ—")) AssocLeft ] + , [ Infix (parseAnnotatedOp $ TopeEQ <$ rzkOperator (symbol "===" <|> symbol "≑")) AssocNone + , Infix (parseAnnotatedOp $ TopeLEQ <$ rzkOperator (symbol "<=" <|> symbol "≀")) AssocNone ] + , [ Infix (parseAnnotatedOp $ TopeAnd <$ rzkOperator (symbol "/\\" <|> symbol "∧")) AssocLeft ] + , [ Infix (parseAnnotatedOp $ TopeOr <$ rzkOperator (symbol "\\/" <|> symbol "∨")) AssocLeft ] + , [ Infix (parseAnnotatedOp $ rzkOperator $ do { symbol "=_{" ; t <- rzkTerm ; symbol "}" ; @@ -315,10 +326,13 @@ isDelim c = c `elem` ("()[]{}," :: String) -- * Orphan 'IsString' instances -instance IsString (Term Span Var Var) where +instance IsString (AnnotatedTerm Span SpannedVar SpannedVar) where fromString = unsafeParseTerm -unsafeParseTerm :: String -> Term Span Var Var +instance IsString SpannedVar where + fromString = unsafeParseString rzkVar + +unsafeParseTerm :: String -> AnnotatedTerm Span SpannedVar SpannedVar unsafeParseTerm = unsafeParseString rzkTerm unsafeParseString :: RzkParser a -> String -> a diff --git a/rzk/src/Rzk/Simple/Pretty.hs b/rzk/src/Rzk/Simple/Pretty.hs index 5cbf6e581..e2b652d85 100644 --- a/rzk/src/Rzk/Simple/Pretty.hs +++ b/rzk/src/Rzk/Simple/Pretty.hs @@ -12,9 +12,12 @@ import Data.Text.Prettyprint.Doc.Render.Terminal import Rzk.Simple.Syntax.Term import Rzk.Simple.Syntax.Var -instance {-# OVERLAPPING #-} Show (Term ann Var Var) where +instance {-# OVERLAPPING #-} Show (AnnotatedTerm ann var Var) where show = Text.unpack . renderLazy . layoutPretty defaultLayoutOptions . ppTermANSIviaShow +instance {-# OVERLAPPING #-} Show (AnnotatedTerm ann var SpannedVar) where + show = Text.unpack . renderLazy . layoutPretty defaultLayoutOptions . ppTermANSIviaShow . fmap unSpanVar + data TypeOfTerm = TermVariable | TypeVariable @@ -62,35 +65,35 @@ highlightUsingAnsiStyle = \case Reserved -> color Cyan -ppTermANSI :: Show a => [Doc TypeOfTerm] -> Term ann var a -> Doc AnsiStyle +ppTermANSI :: Show a => [Doc TypeOfTerm] -> AnnotatedTerm ann var a -> Doc AnsiStyle ppTermANSI vars = reAnnotate highlightUsingAnsiStyle . ppTerm vars . fmap viaShow -ppTermLeft :: [Doc TypeOfTerm] -> Term ann var (Doc TypeOfTerm) -> Doc TypeOfTerm -ppTermLeft vars = \case - t@Lambda{} -> parens (ppTerm vars t) - t@Pi{} -> parens (ppTerm vars t) - t@Sigma{} -> parens (ppTerm vars t) - t -> ppTerm vars t - -ppTermParens :: [Doc TypeOfTerm] -> Term ann var (Doc TypeOfTerm) -> Doc TypeOfTerm -ppTermParens vars = \case - t@Lambda{} -> ppTerm vars t - t@Pi{} -> ppTerm vars t - t@Sigma{} -> ppTerm vars t - t@Variable{} -> ppTerm vars t - t@Universe -> ppTerm vars t - t@Refl{} -> ppTerm vars t - t@Cube{} -> ppTerm vars t - t@CubeUnit{} -> ppTerm vars t - t@CubeUnitStar{} -> ppTerm vars t - t@Tope{} -> ppTerm vars t - t@TopeTop{} -> ppTerm vars t - t@TopeBottom{} -> ppTerm vars t - t@RecBottom{} -> ppTerm vars t - t@Cube2{} -> ppTerm vars t - t@Cube2_0{} -> ppTerm vars t - t@Cube2_1{} -> ppTerm vars t - t -> parens (ppTerm vars t) +ppTermLeft :: [Doc TypeOfTerm] -> AnnotatedTerm ann var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppTermLeft vars t@(AnnotatedTerm _ann tt) = case tt of + Lambda{} -> parens (ppTerm vars t) + Pi{} -> parens (ppTerm vars t) + Sigma{} -> parens (ppTerm vars t) + _ -> ppTerm vars t + +ppTermParens :: [Doc TypeOfTerm] -> AnnotatedTerm ann var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppTermParens vars t@(AnnotatedTerm _ann tt) = case tt of + Lambda{} -> ppTerm vars t + Pi{} -> ppTerm vars t + Sigma{} -> ppTerm vars t + Variable{} -> ppTerm vars t + Universe -> ppTerm vars t + Refl{} -> ppTerm vars t + Cube{} -> ppTerm vars t + CubeUnit{} -> ppTerm vars t + CubeUnitStar{} -> ppTerm vars t + Tope{} -> ppTerm vars t + TopeTop{} -> ppTerm vars t + TopeBottom{} -> ppTerm vars t + RecBottom{} -> ppTerm vars t + Cube2{} -> ppTerm vars t + Cube2_0{} -> ppTerm vars t + Cube2_1{} -> ppTerm vars t + _ -> parens (ppTerm vars t) ppReserved :: Doc TypeOfTerm -> Doc TypeOfTerm ppReserved = annotate Reserved @@ -119,9 +122,9 @@ ppTopeElim = annotate TopeEliminator ppCubeElim :: Doc TypeOfTerm -> Doc TypeOfTerm ppCubeElim = annotate CubeEliminator -ppScoped :: [Doc TypeOfTerm] -> Scope1Term ann var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppScoped :: [Doc TypeOfTerm] -> Scope1AnnotatedTerm ann var (Doc TypeOfTerm) -> Doc TypeOfTerm ppScoped [] = error "Not enough fresh variables!" -ppScoped (x:vars) = ppTerm vars . instantiate1 (Variable x) +ppScoped (x:vars) = ppTerm vars . instantiate1 (unannotated (Variable x)) ppVar :: Doc TypeOfTerm -> Doc TypeOfTerm ppVar = annotate TermVariable @@ -135,21 +138,20 @@ ppTopeVar = annotate TopeVariable ppCubeVar :: Doc TypeOfTerm -> Doc TypeOfTerm ppCubeVar = annotate CubeVariable -ppElimWithArgs :: [Doc TypeOfTerm] -> Doc TypeOfTerm -> [Term ann var (Doc TypeOfTerm)] -> Doc TypeOfTerm +ppElimWithArgs :: [Doc TypeOfTerm] -> Doc TypeOfTerm -> [AnnotatedTerm ann var (Doc TypeOfTerm)] -> Doc TypeOfTerm ppElimWithArgs vars elim args = elim <> parens (hsep (punctuate comma (map (ppTerm vars) args))) -ppTerm :: [Doc TypeOfTerm] -> Term ann var (Doc TypeOfTerm) -> Doc TypeOfTerm -ppTerm vars = \case - Annotated _ann t -> ppTerm vars t -- ignore annotations +ppTerm :: [Doc TypeOfTerm] -> AnnotatedTerm ann var (Doc TypeOfTerm) -> Doc TypeOfTerm +ppTerm vars (AnnotatedTerm _ann tt) = case tt of Variable x -> ppVar x App t1 t2 -> ppTermLeft vars t1 <+> ppTermParens vars t2 First t -> ppTermElim "π₁" <+> ppTermParens vars t Second t -> ppTermElim "Ο€β‚‚" <+> ppTermParens vars t Universe -> ppTypeCon "𝒰 " - Pi (Lambda (Just a) Nothing m) -> + Pi (AnnotatedTerm _ann (Lambda (Just a) Nothing m)) -> parens (ppTypeVar var <+> ":" <+> ppTerm vars a) <+> "β†’ " <+> ppScoped vars m - Pi (Lambda (Just a) (Just phi) m) -> + Pi (AnnotatedTerm _ann (Lambda (Just a) (Just phi) m)) -> braces (ppTypeVar var <+> ":" <+> ppTerm vars a <+> "|" <+> ppScoped vars phi) <+> "β†’ " <+> ppScoped vars m Pi t -> "Pi " <> ppTermParens vars t Lambda (Just a) Nothing m @@ -161,7 +163,7 @@ ppTerm vars = \case Lambda Nothing (Just phi) m -> ppReserved "Ξ»" <> braces (ppVar var <+> "|" <+> ppScoped vars phi) <+> "β†’" <+> ppScoped vars m - Sigma (Lambda (Just a) Nothing m) + Sigma (AnnotatedTerm _ann (Lambda (Just a) Nothing m)) -> ppReserved "βˆ‘" <+> parens (ppTypeVar var <+> ":" <+> ppTerm vars a) <> comma <+> ppScoped vars m Sigma t -> ppReserved "βˆ‘" <> ppTermParens vars t Pair t1 t2 -> parens (ppTerm vars t1 <> comma <+> ppTerm vars t2) @@ -197,11 +199,11 @@ ppTerm vars = \case where var:_ = vars -ppTermANSIviaShow :: Show a => Term ann var a -> Doc AnsiStyle +ppTermANSIviaShow :: Show a => AnnotatedTerm ann var a -> Doc AnsiStyle ppTermANSIviaShow t = ppTermANSI vars t' where vars = (viaShow . Var) <$> zipWith appendIndexText [0..] (repeat "x") t' = viaShow <$> t -pp :: Show a => Term ann var a -> IO () +pp :: Show a => AnnotatedTerm ann var a -> IO () pp t = putDoc (ppTermANSIviaShow t <> "\n") diff --git a/rzk/src/Rzk/Simple/Syntax/Term.hs b/rzk/src/Rzk/Simple/Syntax/Term.hs index d6e8bb090..935ff81f2 100644 --- a/rzk/src/Rzk/Simple/Syntax/Term.hs +++ b/rzk/src/Rzk/Simple/Syntax/Term.hs @@ -1,7 +1,9 @@ -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE UndecidableInstances #-} module Rzk.Simple.Syntax.Term where import Bound @@ -10,48 +12,59 @@ import Control.Monad (ap) import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1) import Data.Functor.Classes +import Data.Functor.Compose type Scope1 var = Scope (Name var ()) -type Scope1Term ann var a = Scope1 var (Term ann var) a +type Scope1AnnotatedTerm ann var = Scope1 var (AnnotatedTerm ann var) + +data AnnotatedTerm ann var a = AnnotatedTerm + { getAnnotation :: [ann] + , getTerm :: Term ann var a + } deriving (Functor, Foldable, Traversable) + +appendAnnotation :: [ann] -> AnnotatedTerm ann var a -> AnnotatedTerm ann var a +appendAnnotation x (AnnotatedTerm y t) = AnnotatedTerm (x <> y) t + +unannotated :: Term ann var a -> AnnotatedTerm ann var a +unannotated = AnnotatedTerm mempty -- | This is a (probably unevaluated) term out of context. data Term ann var a - = Annotated ann (Term ann var a) - | Variable a + = Variable a -- ^ Term variable \(x_i\) or type variable \(A_i\) or cube variable \(t_i\) or tope variable \(\phi_i\). | Universe -- ^ Universe type \(\mathcal{U}\). -- Saying \(A \mathbf{type}\) is equivalent to saying \(A : \mathcal{U}\). - | Pi (Term ann var a) + | Pi (AnnotatedTerm ann var a) -- ^ Dependent product type former \(\prod_{x : A} B(x)\). -- The term argument represents type family \(B : A \to \mathcal{U}\). - | Lambda (Maybe (Term ann var a)) (Maybe (Scope1Term ann var a)) (Scope1Term ann var a) + | Lambda (Maybe (AnnotatedTerm ann var a)) (Maybe (Scope1AnnotatedTerm ann var a)) (Scope1AnnotatedTerm ann var a) -- ^ \(\lambda\)-abstraction ("lambda abstraction"). -- @Lambda x a Nothing m@ represents a term of the form \(\lambda (x : A). M\) -- while @Lambda t i (Just phi) m@ represents \(\lambda \{t : I | \phi\}. M\) - | App (Term ann var a) (Term ann var a) + | App (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) -- ^ Application of one term to another \((M N)\). - | Sigma (Term ann var a) + | Sigma (AnnotatedTerm ann var a) -- ^ Dependent sum type former \(\sum_{x : A} B(x)\). -- The term argument represents type family \(B : A \to \mathcal{U}\). - | Pair (Term ann var a) (Term ann var a) + | Pair (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) -- ^ A (dependent) pair of terms. -- @Pair x y@ represents a term of the form \((x, y)\). - | First (Term ann var a) + | First (AnnotatedTerm ann var a) -- ^ Project the first element of a pair: \(\pi_1 p\). - | Second (Term ann var a) + | Second (AnnotatedTerm ann var a) -- ^ Project the second element of a pair: \(\pi_2 p\). - | IdType (Term ann var a) (Term ann var a) (Term ann var a) + | IdType (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) -- ^ Identity type former \(x =_A y\) (corresponding to term @IdType a x y@). - | Refl (Maybe (Term ann var a)) (Term ann var a) + | Refl (Maybe (AnnotatedTerm ann var a)) (AnnotatedTerm ann var a) -- ^ Trivial inhabitant of \(x =_A x\) for any type \(A\) and \(x : A\). -- @Refl a x@ corresponds to \(x =_a x\). - | IdJ (Term ann var a) (Term ann var a) (Term ann var a) (Term ann var a) (Term ann var a) (Term ann var a) + | IdJ (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) -- ^ Path induction (for identity types). -- For any type \(A\) and \(a : A\), type family -- \(C : \prod_{x : A} ((a =_A x) \to \mathcal{U})\) @@ -68,7 +81,7 @@ data Term ann var a | CubeUnitStar -- ^ The only point in the unit cube: \(\star : \mathbf{1}\). - | CubeProd (Term ann var a) (Term ann var a) + | CubeProd (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) -- ^ Product of cubes: \(I \times J\). | Tope @@ -77,21 +90,21 @@ data Term ann var a -- ^ Top tope (no constraints on cube): \(\top\;\mathsf{tope}\) | TopeBottom -- ^ Bottom tope (cube contrained to empty space): \(\bot\;\mathsf{tope}\) - | TopeOr (Term ann var a) (Term ann var a) + | TopeOr (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) -- ^ Tope disjuction (union of shapes): \(\psi \lor \phi\;\mathsf{tope}\) - | TopeAnd (Term ann var a) (Term ann var a) + | TopeAnd (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) -- ^ Tope conjunction (intersection of shapes): \(\psi \land \phi\;\mathsf{tope}\) - | TopeEQ (Term ann var a) (Term ann var a) + | TopeEQ (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) -- ^ Equality tope (diagonals): \(t \equiv s \;\mathsf{tope}\). -- Note that it can involve projections as well, e.g. \(\pi_1 t \equiv \pi_2 t\). | RecBottom -- ^ Bottom tope eliminator: \(\mathsf{rec}_\bot : A\). - | RecOr (Term ann var a) (Term ann var a) (Term ann var a) (Term ann var a) + | RecOr (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) -- ^ Tope disjunction eliminator: \(\mathsf{rec}^{\psi,\phi}_\lor(a_\psi, a_\phi)\). | ExtensionType - (Term ann var a) (Scope1Term ann var a) (Scope1Term ann var a) (Scope1Term ann var a) (Scope1Term ann var a) + (AnnotatedTerm ann var a) (Scope1AnnotatedTerm ann var a) (Scope1AnnotatedTerm ann var a) (Scope1AnnotatedTerm ann var a) (Scope1AnnotatedTerm ann var a) -- ^ Extension type \( \left\langle \prod_{t : I | psi} A(t) \rvert^{\phi}_{a(t)} \right\rangle \) corresponding to @ExtensionType t cI psi tA phi a@. | Cube2 @@ -101,61 +114,66 @@ data Term ann var a | Cube2_1 -- ^ End of directed interval: \(1 : \mathbb{2}\). - | TopeLEQ (Term ann var a) (Term ann var a) + | TopeLEQ (AnnotatedTerm ann var a) (AnnotatedTerm ann var a) -- ^ Inequality tope: \(t \leq s\). deriving (Functor, Foldable, Traversable) -instance Applicative (Term ann var) where - pure = Variable +instance Applicative (AnnotatedTerm ann var) where + pure = return (<*>) = ap -instance Monad (Term ann var) where - return = Variable - t >>= f = +instance Monad (AnnotatedTerm ann var) where + return = unannotated . Variable + AnnotatedTerm ann t >>= f = appendAnnotation ann $ case t of - Annotated ann t' -> Annotated ann (t' >>= f) Variable x -> f x - Universe -> Universe + _ -> unannotated $ case t of + Universe -> Universe - ExtensionType tC psi tA phi a -> - ExtensionType (tC >>= f) (psi >>>= f) (tA >>>= f) (phi >>>= f) (a >>>= f) - Pi t' -> Pi (t' >>= f) - Lambda a phi body - -> Lambda (fmap (>>= f) a) (fmap (>>>= f) phi) (body >>>= f) - App t1 t2 -> App (t1 >>= f) (t2 >>= f) + ExtensionType tC psi tA phi a -> + ExtensionType (tC >>= f) (psi >>>= f) (tA >>>= f) (phi >>>= f) (a >>>= f) + Pi t' -> Pi (t' >>= f) + Lambda a phi body + -> Lambda (fmap (>>= f) a) (fmap (>>>= f) phi) (body >>>= f) + App t1 t2 -> App (t1 >>= f) (t2 >>= f) - Sigma t' -> Sigma (t' >>= f) - Pair t1 t2 -> Pair (t1 >>= f) (t2 >>= f) - First t' -> First (t' >>= f) - Second t' -> Second (t' >>= f) + Sigma t' -> Sigma (t' >>= f) + Pair t1 t2 -> Pair (t1 >>= f) (t2 >>= f) + First t' -> First (t' >>= f) + Second t' -> Second (t' >>= f) - IdType a x y -> IdType (a >>= f) (x >>= f) (y >>= f) - Refl a x -> Refl (fmap (>>= f) a) (x >>= f) - IdJ tA a tC d x p -> IdJ (tA >>= f) (a >>= f) (tC >>= f) (d >>= f) (x >>= f) (p >>= f) + IdType a x y -> IdType (a >>= f) (x >>= f) (y >>= f) + Refl a x -> Refl (fmap (>>= f) a) (x >>= f) + IdJ tA a tC d x p -> IdJ (tA >>= f) (a >>= f) (tC >>= f) (d >>= f) (x >>= f) (p >>= f) - Cube -> Cube - CubeUnit -> CubeUnit - CubeUnitStar -> CubeUnitStar + Cube -> Cube + CubeUnit -> CubeUnit + CubeUnitStar -> CubeUnitStar - CubeProd t1 t2 -> CubeProd (t1 >>= f) (t2 >>= f) + CubeProd t1 t2 -> CubeProd (t1 >>= f) (t2 >>= f) - Tope -> Tope - TopeTop -> TopeTop - TopeBottom -> TopeBottom - TopeOr t1 t2 -> TopeOr (t1 >>= f) (t2 >>= f) - TopeAnd t1 t2 -> TopeAnd (t1 >>= f) (t2 >>= f) - TopeEQ t1 t2 -> TopeEQ (t1 >>= f) (t2 >>= f) + Tope -> Tope + TopeTop -> TopeTop + TopeBottom -> TopeBottom + TopeOr t1 t2 -> TopeOr (t1 >>= f) (t2 >>= f) + TopeAnd t1 t2 -> TopeAnd (t1 >>= f) (t2 >>= f) + TopeEQ t1 t2 -> TopeEQ (t1 >>= f) (t2 >>= f) - RecBottom -> RecBottom - RecOr psi phi t1 t2 -> RecOr (psi >>= f) (phi >>= f) (t1 >>= f) (t2 >>= f) + RecBottom -> RecBottom + RecOr psi phi t1 t2 -> RecOr (psi >>= f) (phi >>= f) (t1 >>= f) (t2 >>= f) - Cube2 -> Cube2 - Cube2_0 -> Cube2_0 - Cube2_1 -> Cube2_1 + Cube2 -> Cube2 + Cube2_0 -> Cube2_0 + Cube2_1 -> Cube2_1 - TopeLEQ t1 t2 -> TopeLEQ (t1 >>= f) (t2 >>= f) + TopeLEQ t1 t2 -> TopeLEQ (t1 >>= f) (t2 >>= f) + +deriveEq1 ''AnnotatedTerm +deriveOrd1 ''AnnotatedTerm +deriveRead1 ''AnnotatedTerm +deriveShow1 ''AnnotatedTerm deriveEq1 ''Term deriveOrd1 ''Term @@ -166,3 +184,54 @@ instance (Eq ann, Eq var, Eq a) => Eq (Term ann var a) where (==) = eq1 instance (Ord ann, Ord var, Ord a) => Ord (Term ann var a) where compare = compare1 instance (Show ann, Show var, Show a) => Show (Term ann var a) where showsPrec = showsPrec1 instance (Read ann, Read var, Read a) => Read (Term ann var a) where readsPrec = readsPrec1 + +mapWithAnnotation :: ([ann] -> a -> b) -> AnnotatedTerm ann var a -> AnnotatedTerm ann var b +mapWithAnnotation f = go + where + goScope = Scope . fmap (fmap go) . unscope + + go (AnnotatedTerm ann tt) = AnnotatedTerm ann $ + case tt of + Variable x -> Variable (f ann x) + + Universe -> Universe + + ExtensionType tC psi tA phi a -> + ExtensionType (go tC) (goScope psi) (goScope tA) (goScope phi) (goScope a) + Pi t' -> Pi (go t') + Lambda a phi body + -> Lambda (fmap go a) (fmap goScope phi) (goScope body) + App t1 t2 -> App (go t1) (go t2) + + Sigma t' -> Sigma (go t') + Pair t1 t2 -> Pair (go t1) (go t2) + First t' -> First (go t') + Second t' -> Second (go t') + + IdType a x y -> IdType (go a) (go x) (go y) + Refl a x -> Refl (fmap go a) (go x) + IdJ tA a tC d x p -> IdJ (go tA) (go a) (go tC) (go d) (go x) (go p) + + Cube -> Cube + CubeUnit -> CubeUnit + CubeUnitStar -> CubeUnitStar + + CubeProd t1 t2 -> CubeProd (go t1) (go t2) + + Tope -> Tope + TopeTop -> TopeTop + TopeBottom -> TopeBottom + TopeOr t1 t2 -> TopeOr (go t1) (go t2) + TopeAnd t1 t2 -> TopeAnd (go t1) (go t2) + TopeEQ t1 t2 -> TopeEQ (go t1) (go t2) + + RecBottom -> RecBottom + RecOr psi phi t1 t2 -> RecOr (go psi) (go phi) (go t1) (go t2) + + + Cube2 -> Cube2 + Cube2_0 -> Cube2_0 + Cube2_1 -> Cube2_1 + + TopeLEQ t1 t2 -> TopeLEQ (go t1) (go t2) + diff --git a/rzk/src/Rzk/Simple/Syntax/Var.hs b/rzk/src/Rzk/Simple/Syntax/Var.hs index 0c1aa4b36..675a77ce3 100644 --- a/rzk/src/Rzk/Simple/Syntax/Var.hs +++ b/rzk/src/Rzk/Simple/Syntax/Var.hs @@ -3,15 +3,27 @@ module Rzk.Simple.Syntax.Var where import Data.Char (chr, ord) import Data.Coerce (coerce) -import Data.Hashable (Hashable) +import Data.Function (on) +import Data.Hashable (Hashable (..)) import Data.String (IsString (..)) import Data.Text (Text) import qualified Data.Text as Text +import Text.Trifecta (Spanned (..)) -- | Standard type of variables. newtype Var = Var { getVar :: Text } deriving (Eq, Ord, Hashable, IsString) +newtype SpannedVar = SpannedVar { getSpannedVar :: Spanned Var } + deriving (Show) + +unSpanVar :: SpannedVar -> Var +unSpanVar (SpannedVar (var :~ _span)) = var + +instance Eq SpannedVar where (==) = (==) `on` unSpanVar +instance Ord SpannedVar where compare = compare `on` unSpanVar +instance Hashable SpannedVar where hashWithSalt salt = hashWithSalt salt . unSpanVar + instance Show Var where show = Text.unpack . getVar appendIndexText :: Int -> Text -> Text From f92dcb4451b9e738ab1dbbfd92ed02b7f28641d6 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 26 Feb 2021 00:53:24 +0300 Subject: [PATCH 08/10] Add a formulation of simple terms with typechecking using free monads with scoping --- rzk/package.yaml | 3 + rzk/rzk.cabal | 13 +- rzk/src/Rzk/Free/Syntax/Term.hs | 133 +++++++++ rzk/src/Rzk/Free/Syntax/Term2.hs | 459 +++++++++++++++++++++++++++++++ 4 files changed, 607 insertions(+), 1 deletion(-) create mode 100644 rzk/src/Rzk/Free/Syntax/Term.hs create mode 100644 rzk/src/Rzk/Free/Syntax/Term2.hs diff --git a/rzk/package.yaml b/rzk/package.yaml index a0941a551..9ea9baddd 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -35,6 +35,9 @@ dependencies: - prettyprinter-ansi-terminal - ansi-terminal - hashable +- free +- bifunctors +- transformers library: source-dirs: src diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index f99793433..3d941f41d 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -4,7 +4,7 @@ cabal-version: 1.12 -- -- see: https://github.com/sol/hpack -- --- hash: 2ae15fb94b314d3beeb9cfdc7449e6c7550bf4ce4406e88e3910951feac7f9b5 +-- hash: 2c2185c92acedbd2a2f0c0f42a8dea0210179f8f285811228b6ad651b51df31c name: rzk version: 0.1.0.0 @@ -29,6 +29,8 @@ library Rzk Rzk.Debug.Trace Rzk.Evaluator + Rzk.Free.Syntax.Term + Rzk.Free.Syntax.Term2 Rzk.Parser.Text Rzk.Pretty.Text Rzk.Simple.Evaluator @@ -50,14 +52,17 @@ library build-depends: ansi-terminal , base >=4.7 && <5 + , bifunctors , bound , deriving-compat + , free , hashable , mtl , parsers , prettyprinter , prettyprinter-ansi-terminal , text + , transformers , trifecta , unordered-containers default-language: Haskell2010 @@ -72,8 +77,10 @@ executable rzk build-depends: ansi-terminal , base >=4.7 && <5 + , bifunctors , bound , deriving-compat + , free , hashable , mtl , parsers @@ -81,6 +88,7 @@ executable rzk , prettyprinter-ansi-terminal , rzk , text + , transformers , trifecta , unordered-containers default-language: Haskell2010 @@ -96,8 +104,10 @@ test-suite rzk-test build-depends: ansi-terminal , base >=4.7 && <5 + , bifunctors , bound , deriving-compat + , free , hashable , mtl , parsers @@ -105,6 +115,7 @@ test-suite rzk-test , prettyprinter-ansi-terminal , rzk , text + , transformers , trifecta , unordered-containers default-language: Haskell2010 diff --git a/rzk/src/Rzk/Free/Syntax/Term.hs b/rzk/src/Rzk/Free/Syntax/Term.hs new file mode 100644 index 000000000..2d1b82107 --- /dev/null +++ b/rzk/src/Rzk/Free/Syntax/Term.hs @@ -0,0 +1,133 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} +module Rzk.Free.Syntax.Term where + +import Bound +import Bound.Name +import Control.Monad (ap) +import Data.Void + +newtype Scope' term a b = Scope' { unscope' :: Scope b term a } + +unscopeVoid :: Monad term => Scope' term a Void -> term a +unscopeVoid = instantiate absurd . unscope' + +abstractVoid :: Monad term => term a -> Scope' term a Void +abstractVoid = Scope' . abstract (const Nothing) + +class Functor1 term where + fmap1 :: (forall x. scope x -> scope' x) -> term scope -> term scope' + +data FreeScoped term a + = PureScoped a + | FreeScoped (term (Scope' (FreeScoped term) a)) + +deriving instance + ( Show a + , Show (term (Scope' (FreeScoped term) a)) + ) => Show (FreeScoped term a) + +instance Functor1 term => Functor (FreeScoped term) where + fmap f (PureScoped x) = PureScoped (f x) + fmap f (FreeScoped t) = FreeScoped (fmap1 (Scope' . fmap f . unscope') t) + +instance Functor1 term => Applicative (FreeScoped term) where + pure = return + (<*>) = ap + +instance Functor1 term => Monad (FreeScoped term) where + return = PureScoped + PureScoped x >>= f = f x + FreeScoped t >>= f = FreeScoped (fmap1 (Scope' . (>>>= f) . unscope') t) + +data TermF bound scope + = LambdaF (scope (Name bound ())) + | AppF (scope Void) (scope Void) + +deriving instance + ( Show (scope (Name bound ())) + , Show (scope Void) + ) => Show (TermF bound scope) + +instance Functor1 (TermF bound) where + fmap1 k (LambdaF body) = LambdaF (k body) + fmap1 k (AppF t1 t2) = AppF (k t1) (k t2) + +type Term bound = FreeScoped (TermF bound) + +type Scope1Term bound = Scope (Name bound ()) (Term bound) + +-- * Pattern synonyms for 'Term' + +pattern Variable :: a -> Term b a +pattern Variable x = PureScoped x + +isApp :: Term b a -> Maybe (Term b a, Term b a) +isApp (FreeScoped (AppF t1 t2)) = Just (unscopeVoid t1, unscopeVoid t2) +isApp _ = Nothing + +pattern App :: Term b a -> Term b a -> Term b a +pattern App t1 t2 <- (isApp -> Just (t1, t2)) where + App t1 t2 = FreeScoped (AppF (abstractVoid t1) (abstractVoid t2)) + +pattern Lambda :: Scope1Term b a -> Term b a +pattern Lambda body = FreeScoped (LambdaF (Scope' body)) + +{-# COMPLETE Variable, App, Lambda #-} + +-- * Smart constructors for binders + +lam :: Eq a => a -> Term a a -> Term a a +lam x body = Lambda (abstract1Name x body) + +-- * Evaluation + +whnf :: Term b a -> Term b a +whnf = \case + App t1 t2 -> + case whnf t1 of + Lambda body -> instantiate1 t2 body + t1' -> App t1' t2 + t@Variable{} -> t + t@Lambda{} -> t + +nf :: Term b a -> Term b a +nf = \case + App t1 t2 -> + case whnf t1 of + Lambda body -> nf (instantiate1 t2 body) + t1' -> App (nf t1') (nf t2) + Lambda body -> Lambda (nfScope body) + t@Variable{} -> t + where + nfScope = toScope . nf . fromScope + +-- * Pretty-printing + +parens :: String -> String +parens s = "(" <> s <> ")" + +ppTerm :: [String] -> Term b String -> String +ppTerm vars = \case + Variable x -> x + App t1 t2 -> ppTermFun vars t1 <> " " <> ppTermArg vars t2 + Lambda body -> + let z:zs = vars + in "\\" <> z <> "." <> ppTerm zs (instantiate1 (Variable z) body) + +ppTermFun :: [String] -> Term b String -> String +ppTermFun vars = \case + t@Lambda{} -> parens (ppTerm vars t) + t -> ppTerm vars t + +ppTermArg :: [String] -> Term b String -> String +ppTermArg vars = \case + t@Variable{} -> ppTerm vars t + t -> parens (ppTerm vars t) + diff --git a/rzk/src/Rzk/Free/Syntax/Term2.hs b/rzk/src/Rzk/Free/Syntax/Term2.hs new file mode 100644 index 000000000..7b1c026ca --- /dev/null +++ b/rzk/src/Rzk/Free/Syntax/Term2.hs @@ -0,0 +1,459 @@ +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE UndecidableInstances #-} +module Rzk.Free.Syntax.Term2 where + +import Bound +import Bound.Name +import Control.Monad (ap, liftM) +import Control.Monad.Identity (Identity (..)) +import Control.Monad.Trans (lift) +import Data.Bifoldable +import Data.Bifunctor +import Data.Bifunctor.TH +import Data.Bitraversable + +-- * Free monad transformer with scoping + +data FreeScopedF term scope subterm a + = PureScopedF a + | FreeScopedF (term scope subterm) + deriving (Eq, Show, Functor, Foldable, Traversable) + +newtype FreeScopedT b term m a = FreeScopedT + { runFreeScopedT :: m (FreeScopedF term (Scope b (FreeScopedT b term m) a) (FreeScopedT b term m a) a) + } + +instance (Bifoldable term, Foldable m) => Foldable (FreeScopedT b term m) where + foldMap f (FreeScopedT m) = foldMap f' m + where + f' (PureScopedF x) = f x + f' (FreeScopedF t) = bifoldMap (foldMap f) (foldMap f) t + +instance (Bitraversable term, Traversable m, Monad m) + => Traversable (FreeScopedT b term m) where + traverse f (FreeScopedT m) = FreeScopedT <$> traverse f' m + where + f' (PureScopedF x) = PureScopedF <$> f x + f' (FreeScopedF t) = FreeScopedF <$> bitraverse (traverse f) (traverse f) t + +instance (Bifunctor term, Monad m) => Functor (FreeScopedT b term m) where + fmap f (FreeScopedT m) = FreeScopedT (liftM f' m) + where + f' (PureScopedF x) = PureScopedF (f x) + f' (FreeScopedF t) = FreeScopedF (bimap (fmap f) (fmap f) t) + +instance (Bifunctor term, Monad m) => Applicative (FreeScopedT b term m) where + pure = return + (<*>) = ap + +instance (Bifunctor term, Monad m) => Monad (FreeScopedT b term m) where + return = FreeScopedT . return . PureScopedF + FreeScopedT m >>= f = FreeScopedT (m >>= f') + where + f' (PureScopedF x) = runFreeScopedT (f x) + f' (FreeScopedF t) = return (FreeScopedF (bimap (>>>= f) (>>= f) t)) + +hoistFreeScopedT + :: (Monad m, Bifunctor term) + => (forall x. m x -> n x) -> FreeScopedT b term m a -> FreeScopedT b term n a +hoistFreeScopedT phi (FreeScopedT m) = FreeScopedT (phi (liftM f' m)) + where + f' (PureScopedF x) = PureScopedF x + f' (FreeScopedF t) = FreeScopedF (bimap hoistFreeScopedT' (hoistFreeScopedT phi) t) + + hoistFreeScopedT' = Scope . hoistFreeScopedT phi . fmap (fmap (hoistFreeScopedT phi)) . unscope + +transFreeScopedT + :: (Monad m, Bifunctor term) + => (forall x y. term x y -> term' x y) + -> FreeScopedT b term m a -> FreeScopedT b term' m a +transFreeScopedT phi (FreeScopedT m) = FreeScopedT (liftM f' m) + where + f' (PureScopedF x) = PureScopedF x + f' (FreeScopedF t) = FreeScopedF (phi (bimap transFreeScopedT' (transFreeScopedT phi) t)) + + transFreeScopedT' = Scope . transFreeScopedT phi . fmap (fmap (transFreeScopedT phi)) . unscope + +wrapFreeScopedT + :: Monad m + => term (Scope b (FreeScopedT b term m) a) (FreeScopedT b term m a) + -> FreeScopedT b term m a +wrapFreeScopedT = FreeScopedT . return . FreeScopedF + +-- * Free monad with scoping + +type FreeScoped b term = FreeScopedT b term Identity + +pattern PureScoped :: a -> FreeScoped b term a +pattern PureScoped x = FreeScopedT (Identity (PureScopedF x)) + +pattern FreeScoped + :: term (Scope b (FreeScoped b term) a) (FreeScoped b term a) + -> FreeScoped b term a +pattern FreeScoped t = FreeScopedT (Identity (FreeScopedF t)) + +-- data FreeScoped b term a +-- = PureScoped a +-- | FreeScoped (term (Scope b (FreeScoped b term) a) (FreeScoped b term a)) +-- +-- instance Bifunctor term => Functor (FreeScoped b term) where +-- fmap f (PureScoped x) = PureScoped (f x) +-- fmap f (FreeScoped t) = FreeScoped (bimap (fmap f) (fmap f) t) +-- +-- instance Bifunctor term => Applicative (FreeScoped b term) where +-- pure = return +-- (<*>) = ap +-- +-- instance Bifunctor term => Monad (FreeScoped b term) where +-- return = PureScoped +-- PureScoped x >>= f = f x +-- FreeScoped t >>= f = FreeScoped (bimap (>>>= f) (>>= f) t) + +-- * Term bifunctor to provide nodes + +data TermF bound scope term + = LambdaF scope + | AppF term term + | UniverseF + | PiF term scope + deriving (Show, Functor, Foldable, Traversable) + +deriveBifunctor ''TermF +deriveBifoldable ''TermF +deriveBitraversable ''TermF + +data TypedTermF bound scope term = TypedTermF + { typeF :: term + , termF :: TermF bound scope term + } deriving (Show, Functor, Foldable, Traversable) + +deriveBifunctor ''TypedTermF +deriveBifoldable ''TypedTermF +deriveBitraversable ''TypedTermF + +-- * Annotations + +data Annotated ann a = Annotated + { annotation :: ann + , value :: a + } deriving (Show, Functor, Foldable, Traversable) + +deriveBifunctor ''Annotated +deriveBifoldable ''Annotated +deriveBitraversable ''Annotated + +instance Monoid ann => Applicative (Annotated ann) where + pure = return + (<*>) = ap + +instance Monoid ann => Monad (Annotated ann) where + return = Annotated mempty + Annotated ann x >>= f = reAnnotate (ann <>) (f x) + +reAnnotate :: (a -> b) -> Annotated a x -> Annotated b x +reAnnotate = first + +-- * Term + +-- | Generic term. +type GTerm bound = FreeScopedT (Name bound ()) + +-- | Term without annotations. +type Term bound = GTerm bound (TermF bound) Identity + +-- | A typed term without annotations. +type TypedTerm bound = GTerm bound (TypedTermF bound) Identity + +-- | Term with annotations at every node. +type ATerm ann bound = GTerm bound (TermF bound) (Annotated ann) + +-- | Typed term with annotations at every node. +type ATypedTerm ann bound = GTerm bound (TypedTermF bound) (Annotated ann) + +-- | Scoped term. +type Scope1Term bound = Scope (Name bound ()) (Term bound) + +-- | Scoped typed term. +type Scope1TypedTerm bound = Scope (Name bound ()) (TypedTerm bound) + +-- | Scoped 'ATerm'. +type Scope1ATerm ann bound = Scope (Name bound ()) (ATerm ann bound) + +-- | Scoped annotated typed term. +type Scope1ATypedTerm ann bound = Scope (Name bound ()) (ATypedTerm ann bound) + +type ATermF ann b a = FreeScopedF (TermF b) (Scope1ATerm ann b a) (ATerm ann b a) a + +type ATermF' ann b a = TermF (Scope1ATerm ann b a) (ATerm ann b a) a + +-- ** Patterns + +pattern Variable :: a -> Term b a +pattern Variable x = PureScoped x + +pattern App :: Term b a -> Term b a -> Term b a +pattern App t1 t2 = FreeScoped (AppF t1 t2) + +pattern Lambda :: Scope1Term b a -> Term b a +pattern Lambda body = FreeScoped (LambdaF body) + +pattern Universe :: Term b a +pattern Universe = FreeScoped UniverseF + +pattern Pi :: Term b a -> Scope1Term b a -> Term b a +pattern Pi a b = FreeScoped (PiF a b) + +{-# COMPLETE Variable, App, Lambda, Universe, Pi #-} + +-- *** Patterns for typed terms + +pattern VariableT :: a -> TypedTerm b a +pattern VariableT x = PureScoped x + +pattern Typed :: TypedTerm b a -> TermF b (Scope1TypedTerm b a) (TypedTerm b a) -> TypedTerm b a +pattern Typed t term = FreeScoped (TypedTermF t term) + +pattern AppT :: TypedTerm b a -> TypedTerm b a -> TypedTerm b a -> TypedTerm b a +pattern AppT t t1 t2 = FreeScoped (TypedTermF t (AppF t1 t2)) + +pattern LambdaT :: TypedTerm b a -> Scope1TypedTerm b a -> TypedTerm b a +pattern LambdaT t body = FreeScoped (TypedTermF t (LambdaF body)) + +pattern UniverseT :: TypedTerm b a -> TypedTerm b a +pattern UniverseT t = FreeScoped (TypedTermF t UniverseF) + +pattern PiT :: TypedTerm b a -> TypedTerm b a -> Scope1TypedTerm b a -> TypedTerm b a +pattern PiT t a b = FreeScoped (TypedTermF t (PiF a b)) + +{-# COMPLETE VariableT, AppT, LambdaT, UniverseT, PiT #-} +{-# COMPLETE VariableT, Typed #-} + +-- ** With annotations + +pattern ATerm :: ann -> ATermF ann b a -> ATerm ann b a +pattern ATerm ann f = FreeScopedT (Annotated ann f) + +pattern AppA :: ann -> ATerm ann b a -> ATerm ann b a -> ATerm ann b a +pattern AppA ann t1 t2 = FreeScopedT (Annotated ann (FreeScopedF (AppF t1 t2))) + +pattern LambdaA :: ann -> Scope1ATerm ann b a -> ATerm ann b a +pattern LambdaA ann body = FreeScopedT (Annotated ann (FreeScopedF (LambdaF body))) + +pattern UniverseA :: ann -> ATerm ann b a +pattern UniverseA ann = FreeScopedT (Annotated ann (FreeScopedF UniverseF)) + +pattern PiA :: ann -> ATerm ann b a -> Scope1ATerm ann b a -> ATerm ann b a +pattern PiA ann a b = FreeScopedT (Annotated ann (FreeScopedF (PiF a b))) + +{-# COMPLETE Variable, AppA, LambdaA, UniverseA, PiA #-} + +-- ** Smart binding constructors + +lam :: Eq a => a -> Term a a -> Term a a +lam x body = Lambda (abstract1Name x body) + +-- * Evaluation + +whnf :: Term b a -> Term b a +whnf = \case + App t1 t2 -> + case whnf t1 of + Lambda body -> instantiate1 t2 body + t1' -> App t1' t2 + t@Variable{} -> t + t@Lambda{} -> t + t@Universe{} -> t + t@Pi{} -> t + +nf :: Term b a -> Term b a +nf = \case + App t1 t2 -> + case whnf t1 of + Lambda body -> nf (instantiate1 t2 body) + t1' -> App (nf t1') (nf t2) + Lambda body -> Lambda (nfScope body) + Pi a b -> Pi (nf a) (nfScope b) + t@Variable{} -> t + t@Universe{} -> t + where + nfScope = toScope . nf . fromScope + +-- * Pretty-printing + +parens :: String -> String +parens s = "(" <> s <> ")" + +ppTerm :: [String] -> Term b String -> String +ppTerm vars = \case + Universe -> "U" + Variable x -> x + App t1 t2 -> ppTermFun vars t1 <> " " <> ppTermArg vars t2 + Lambda body -> + let z:zs = vars + in "\\" <> z <> "." <> ppTerm zs (instantiate1 (Variable z) body) + Pi a b -> + let z:zs = vars + in parens (z <> " : " <> ppTerm vars a) <> " -> " <> ppTerm zs (instantiate1 (Variable z) b) + +ppTermFun :: [String] -> Term b String -> String +ppTermFun vars = \case + t@Lambda{} -> parens (ppTerm vars t) + t -> ppTerm vars t + +ppTermArg :: [String] -> Term b String -> String +ppTermArg vars = \case + t@Variable{} -> ppTerm vars t + t -> parens (ppTerm vars t) + +ppTypedTerm :: [String] -> TypedTerm b String -> String +ppTypedTerm vars = \case + VariableT x -> x + AppT t t1 t2 -> parens (ppTypedTerm vars t1) <> " " <> parens (ppTypedTerm vars t2) <> " : " <> ppTerm vars (untyped t) + LambdaT t body -> + let z:zs = vars + in "(\\" <> z <> "." <> ppTypedTerm zs (instantiate1 (VariableT z) body) <> ") : " <> ppTerm vars (untyped t) + UniverseT k -> "U" <> " : " <> ppTerm vars (untyped k) + PiT k a b -> + let z:zs = vars + in parens (z <> " : " <> ppTerm vars (untyped a)) <> " -> " <> ppTypedTerm zs (instantiate1 (VariableT z) b) + <> " : " <> ppTerm vars (untyped k) + +-- * Typecheck + +universeT :: TypedTerm b a +universeT = UniverseT universeT + +untyped :: TypedTerm b a -> Term b a +untyped = transFreeScopedT termF + +typecheckScope :: TypedTerm b a -> (a -> TypedTerm b a) -> Scope1Term b a -> Scope1Term b a -> Scope1TypedTerm b a +typecheckScope typeOfBoundVar typeOfFreeVar term expectedType + = toScope (typecheck typeOfVar (fromScope term) (fromScope expectedType)) + where + typeOfVar (B (Name _ ())) = F <$> typeOfBoundVar + typeOfVar (F x) = F <$> typeOfFreeVar x + +infer :: (a -> TypedTerm b a) -> Term b a -> TypedTerm b a +infer typeOfFreeVar = \case + Universe -> universeT + Pi a b -> + let a' = typecheck typeOfFreeVar a Universe + b' = typecheckScope a' typeOfFreeVar b (toScope Universe) + in PiT universeT a' b' + App t1 t2 -> + case infer typeOfFreeVar t1 of + t1'@(Typed (PiT _ a b) _) -> + let t2' = typecheck typeOfFreeVar t2 (untyped a) -- FIXME: why make a untyped? + in AppT (instantiate1 t2' b) t1' t2' + t1'@(VariableT x) -> + case typeOfFreeVar x of + PiT _ a b -> + let t2' = typecheck typeOfFreeVar t2 (untyped a) -- FIXME: why make a untyped? + in AppT (instantiate1 t2' b) t1' t2' + _ -> error "not a function!" + _ -> error "not a function!" + Lambda _body -> error "can't infer Lambda" + Variable x -> VariableT x + +typecheck :: (a -> TypedTerm b a) -> Term b a -> Term b a -> TypedTerm b a +typecheck typeOfFreeVar term expectedType = case (term, expectedType) of + (Universe, Universe) -> universeT + (Lambda body, Pi a b) -> + let a' = typecheck typeOfFreeVar a Universe + b' = typecheckScope a' typeOfFreeVar b (toScope Universe) + body' = typecheckScope a' typeOfFreeVar body b -- FIXME: why make b' untyped? + in LambdaT (PiT universeT a' b') body' + (Variable x, _) -> VariableT x + _ -> infer typeOfFreeVar term -- FIXME: unify inferred type with expected + +typecheckClosed :: Term b a -> Term b a -> TypedTerm b a +typecheckClosed = typecheck (error "expected closed term, but free vars found!") + +inferClosed :: Term b a -> TypedTerm b a +inferClosed = infer (error "expected closed term, but free vars found!") + +zero :: Term String String +zero = lam "s" (lam "z" (Variable "z")) + +nat :: Int -> Term String String +nat n = lam "s" (lam "z" (iterate (App (Variable "s")) (Variable "z") !! n)) + +(-->) :: Term b a -> Term b a -> Term b a +a --> b = Pi a (lift b) + +natT :: Term b a +natT = (Universe --> Universe) --> (Universe --> Universe) + +-- newtype AType b a = AType { getAType :: Maybe (ATerm (AType b) b a) } +-- deriving (Functor, Foldable, Traversable) +-- +-- type Scope1AType b a = Scope1ATerm (AType b) b a +-- +-- instance Applicative (AType b) where +-- pure = return +-- (<*>) = ap +-- +-- instance Monad (AType b) where +-- return x = AType (Just (return x)) +-- AType Nothing >>= _ = AType Nothing +-- AType (Just t) >>= f = AType (fmap join (traverse (getAType . f) t)) +-- +-- instance Alternative (AType b) where +-- empty = mzero +-- (<|>) = mplus +-- +-- instance MonadPlus (AType b) where +-- mzero = AType Nothing +-- AType Nothing `mplus` t = t +-- t `mplus` _ = t +-- +-- type TypedTerm b a = ATerm (AType b) b a +-- +-- type TypedTermF b a = ATermF (AType b) b a +-- type TypedTermF' b a = ATermF' (AType b) b a +-- +-- type Scope1TypedTerm b a = Scope1ATerm (AType b) b a +-- +-- pattern (:::) :: TypedTermF b a -> AType b (TypedTermF b a) -> TypedTerm b a +-- pattern term ::: ty = ATerm ty term +-- +-- typecheck :: Term b a -> AType b a -> TypeChecker (TypedTerm b a) +-- typecheck term expectedType = +-- case (term, expectedType) of +-- (Variable x, _) -> PureScopedF x ::: expectedTypeF +-- (Universe, AType (Just (UniverseA _))) -> FreeScopedF UniverseF ::: expectedTypeF +-- (Lambda body, AType (Just (PiA _ a b))) -> +-- case typecheckScope body (AType (Just a)) b of +-- body' -> FreeScopedF (LambdaF body') ::: expectedTypeF +-- _ -> error "can't typecheck" +-- where +-- expectedTypeF = fmap PureScopedF expectedType +-- +-- typecheckScope :: Scope1Term b a -> AType b a -> Scope1AType b a -> Scope1TypedTerm b a +-- typecheckScope term argType bodyType +-- = toScope $ (fromScope term `typecheck` AType (Just (fromScope bodyType))) +-- +-- +-- +-- pattern AppT :: AType b (TypedTermF b a) -> TypedTerm b a -> TypedTerm b a -> AType b a +-- pattern AppT kind t1 t2 = AType (Just (FreeScopedT (Annotated kind (FreeScopedF (AppF t1 t2))))) +-- +-- pattern LambdaT :: c -> Scope1AType b a -> AType b a +-- pattern LambdaT kind body = AType (Just (FreeScopedT (Annotated kind (FreeScopedF (LambdaF body))))) +-- +-- pattern UniverseT :: c -> AType b a +-- pattern UniverseT kind = AType (Just (FreeScopedT (Annotated kind (FreeScopedF UniverseF)))) +-- +-- pattern PiT :: c -> TypedTerm b a -> Scope1AType b a -> AType b a +-- pattern PiT kind a b = AType (Just (FreeScopedT (Annotated kind (FreeScopedF (PiF a b))))) +-- +-- {-# COMPLETE Variable, AppA, LambdaA, UniverseA, PiA #-} +-- From c9fc7fb549978f28af8304243e27afd3f4bf8793 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 26 Feb 2021 09:33:38 +0300 Subject: [PATCH 09/10] Add unification and basic inference for lambdas --- rzk/src/Rzk/Free/Syntax/Term2.hs | 150 +++++++++++++++++++++++++------ 1 file changed, 125 insertions(+), 25 deletions(-) diff --git a/rzk/src/Rzk/Free/Syntax/Term2.hs b/rzk/src/Rzk/Free/Syntax/Term2.hs index 7b1c026ca..39c8f8653 100644 --- a/rzk/src/Rzk/Free/Syntax/Term2.hs +++ b/rzk/src/Rzk/Free/Syntax/Term2.hs @@ -20,6 +20,8 @@ import Data.Bifunctor import Data.Bifunctor.TH import Data.Bitraversable +import Unsafe.Coerce (unsafeCoerce) + -- * Free monad transformer with scoping data FreeScopedF term scope subterm a @@ -260,6 +262,9 @@ pattern PiA ann a b = FreeScopedT (Annotated ann (FreeScopedF (PiF a b))) lam :: Eq a => a -> Term a a -> Term a a lam x body = Lambda (abstract1Name x body) +piType :: Eq a => a -> Term a a -> Term a a -> Term a a +piType x a b = Pi a (abstract1Name x b) + -- * Evaluation whnf :: Term b a -> Term b a @@ -286,6 +291,30 @@ nf = \case where nfScope = toScope . nf . fromScope +whnfT :: TypedTerm b a -> TypedTerm b a +whnfT = \case + AppT t t1 t2 -> + case whnfT t1 of + LambdaT _ body -> instantiate1 t2 body + t1' -> AppT t t1' t2 + t@VariableT{} -> t + t@LambdaT{} -> t + t@UniverseT{} -> t + t@PiT{} -> t + +nfT :: TypedTerm b a -> TypedTerm b a +nfT = \case + AppT t t1 t2 -> + case whnfT t1 of + LambdaT _ body -> nfT (instantiate1 t2 body) + t1' -> AppT (nfT t) (nfT t1') (nfT t2) + LambdaT t body -> LambdaT (nfT t) (nfScopeT body) + PiT _ a b -> PiT universeT (nfT a) (nfScopeT b) + t@VariableT{} -> t + t@UniverseT{} -> t + where + nfScopeT = toScope . nfT . fromScope + -- * Pretty-printing parens :: String -> String @@ -313,18 +342,24 @@ ppTermArg vars = \case t@Variable{} -> ppTerm vars t t -> parens (ppTerm vars t) +ppTypedTermWithSig :: [String] -> TypedTerm b String -> String +ppTypedTermWithSig vars t + = ppTypedTerm vars t <> " : " <> ppTypedTerm vars (typeOf (error "don't know types of free vars") t) + ppTypedTerm :: [String] -> TypedTerm b String -> String ppTypedTerm vars = \case VariableT x -> x - AppT t t1 t2 -> parens (ppTypedTerm vars t1) <> " " <> parens (ppTypedTerm vars t2) <> " : " <> ppTerm vars (untyped t) - LambdaT t body -> + AppT _ t1 t2 -> parens (ppTypedTerm vars t1) <> " " <> parens (ppTypedTerm vars t2) + LambdaT (PiT _ a _) body -> + let z:zs = vars + in "\\(" <> z <> " : " <> ppTypedTerm vars a <> ")." <> ppTypedTerm zs (instantiate1 (VariableT z) body) + LambdaT _ body -> let z:zs = vars - in "(\\" <> z <> "." <> ppTypedTerm zs (instantiate1 (VariableT z) body) <> ") : " <> ppTerm vars (untyped t) - UniverseT k -> "U" <> " : " <> ppTerm vars (untyped k) - PiT k a b -> + in "\\" <> z <> "." <> ppTypedTerm zs (instantiate1 (VariableT z) body) + UniverseT _ -> "U" + PiT _ a b -> let z:zs = vars - in parens (z <> " : " <> ppTerm vars (untyped a)) <> " -> " <> ppTypedTerm zs (instantiate1 (VariableT z) b) - <> " : " <> ppTerm vars (untyped k) + in parens (z <> " : " <> ppTypedTerm vars a) <> " -> " <> ppTypedTerm zs (instantiate1 (VariableT z) b) -- * Typecheck @@ -334,50 +369,103 @@ universeT = UniverseT universeT untyped :: TypedTerm b a -> Term b a untyped = transFreeScopedT termF -typecheckScope :: TypedTerm b a -> (a -> TypedTerm b a) -> Scope1Term b a -> Scope1Term b a -> Scope1TypedTerm b a +typecheckScope + :: Eq a + => TypedTerm b a -> (a -> TypedTerm b a) -> Scope1Term b a -> Scope1TypedTerm b a -> Scope1TypedTerm b a typecheckScope typeOfBoundVar typeOfFreeVar term expectedType = toScope (typecheck typeOfVar (fromScope term) (fromScope expectedType)) where typeOfVar (B (Name _ ())) = F <$> typeOfBoundVar typeOfVar (F x) = F <$> typeOfFreeVar x -infer :: (a -> TypedTerm b a) -> Term b a -> TypedTerm b a +typeOfScoped :: Eq a => TypedTerm b a -> (a -> TypedTerm b a) -> Scope1TypedTerm b a -> Scope1TypedTerm b a +typeOfScoped typeOfBoundVar typeOfFreeVar = toScope . typeOf typeOfVar . fromScope + where + typeOfVar (B (Name _ ())) = F <$> typeOfBoundVar + typeOfVar (F x) = F <$> typeOfFreeVar x + +typeOf :: (a -> TypedTerm b a) -> TypedTerm b a -> TypedTerm b a +typeOf _ (Typed t _) = t +typeOf typeOfFreeVar (VariableT x) = typeOfFreeVar x + +inferScoped :: Eq a => TypedTerm b a -> (a -> TypedTerm b a) -> Scope1Term b a -> Scope1TypedTerm b a +inferScoped typeOfBoundVar typeOfFreeVar = toScope . infer typeOfVar . fromScope + where + typeOfVar (B (Name _ ())) = F <$> typeOfBoundVar + typeOfVar (F x) = F <$> typeOfFreeVar x + +infer :: Eq a => (a -> TypedTerm b a) -> Term b a -> TypedTerm b a infer typeOfFreeVar = \case Universe -> universeT Pi a b -> - let a' = typecheck typeOfFreeVar a Universe - b' = typecheckScope a' typeOfFreeVar b (toScope Universe) + let a' = typecheck typeOfFreeVar a universeT + b' = typecheckScope a' typeOfFreeVar b (toScope universeT) in PiT universeT a' b' + App (Lambda body) arg -> + case infer typeOfFreeVar arg of + arg' -> + let typeOfArg = typeOf typeOfFreeVar arg' + body' = inferScoped typeOfArg typeOfFreeVar body + typeOfBody = typeOfScoped arg' typeOfFreeVar body' + typeOfResult = instantiate1 arg' typeOfBody + in AppT typeOfResult (LambdaT (PiT universeT typeOfArg typeOfBody) body') arg' App t1 t2 -> case infer typeOfFreeVar t1 of t1'@(Typed (PiT _ a b) _) -> - let t2' = typecheck typeOfFreeVar t2 (untyped a) -- FIXME: why make a untyped? + let t2' = typecheck typeOfFreeVar t2 a in AppT (instantiate1 t2' b) t1' t2' t1'@(VariableT x) -> case typeOfFreeVar x of PiT _ a b -> - let t2' = typecheck typeOfFreeVar t2 (untyped a) -- FIXME: why make a untyped? + let t2' = typecheck typeOfFreeVar t2 a in AppT (instantiate1 t2' b) t1' t2' _ -> error "not a function!" _ -> error "not a function!" Lambda _body -> error "can't infer Lambda" Variable x -> VariableT x -typecheck :: (a -> TypedTerm b a) -> Term b a -> Term b a -> TypedTerm b a +typecheck :: Eq a => (a -> TypedTerm b a) -> Term b a -> TypedTerm b a -> TypedTerm b a typecheck typeOfFreeVar term expectedType = case (term, expectedType) of - (Universe, Universe) -> universeT - (Lambda body, Pi a b) -> - let a' = typecheck typeOfFreeVar a Universe - b' = typecheckScope a' typeOfFreeVar b (toScope Universe) - body' = typecheckScope a' typeOfFreeVar body b -- FIXME: why make b' untyped? - in LambdaT (PiT universeT a' b') body' + (Universe, UniverseT{}) -> universeT + (Lambda body, PiT _ a b) -> + LambdaT expectedType (typecheckScope a typeOfFreeVar body b) (Variable x, _) -> VariableT x - _ -> infer typeOfFreeVar term -- FIXME: unify inferred type with expected + _ -> + case infer typeOfFreeVar term of + Typed ty x -> Typed (unify typeOfFreeVar ty expectedType) x + term'@(VariableT x) -> unify typeOfFreeVar (typeOfFreeVar x) expectedType `seq` term' + +unifyScoped + :: Eq a + => TypedTerm b a -> (a -> TypedTerm b a) -> Scope1TypedTerm b a -> Scope1TypedTerm b a -> Scope1TypedTerm b a +unifyScoped typeOfBoundVar typeOfFreeVar l r + = toScope (unify typeOfVar (fromScope l) (fromScope r)) + where + typeOfVar (B (Name _ ())) = F <$> typeOfBoundVar + typeOfVar (F x) = F <$> typeOfFreeVar x -typecheckClosed :: Term b a -> Term b a -> TypedTerm b a +unify :: Eq a => (a -> TypedTerm b a) -> TypedTerm b a -> TypedTerm b a -> TypedTerm b a +unify typeOfFreeVar = go + where + go l r = go' (whnfT l) (whnfT r) + + go' (UniverseT _) (UniverseT _) = universeT + go' (PiT _ a b) (PiT _ c d) = + let ac = go a c + in PiT universeT ac (unifyScoped ac typeOfFreeVar b d) + go' (AppT t a b) (AppT t' c d) = AppT (go t t') (go a c) (go b d) + go' (LambdaT (PiT _ a b) x) (LambdaT (PiT _ c d) y) = + let ac = go a c + in LambdaT (PiT universeT ac (unifyScoped ac typeOfFreeVar b d)) (unifyScoped ac typeOfFreeVar x y) + go' (VariableT x) (VariableT y) + | x == y = VariableT x + | otherwise = error "can't unify different variables" + go' l r = error ("can't unify terms:\n" <> ppTypedTerm ["x", "y", "z"] (unsafeCoerce l) <> "\nand\n" <> ppTypedTerm ["x", "y", "z"] (unsafeCoerce r)) + +typecheckClosed :: Eq a => Term b a -> TypedTerm b a -> TypedTerm b a typecheckClosed = typecheck (error "expected closed term, but free vars found!") -inferClosed :: Term b a -> TypedTerm b a +inferClosed :: Eq a => Term b a -> TypedTerm b a inferClosed = infer (error "expected closed term, but free vars found!") zero :: Term String String @@ -389,8 +477,20 @@ nat n = lam "s" (lam "z" (iterate (App (Variable "s")) (Variable "z") !! n)) (-->) :: Term b a -> Term b a -> Term b a a --> b = Pi a (lift b) -natT :: Term b a -natT = (Universe --> Universe) --> (Universe --> Universe) +natT :: Eq a => TypedTerm b a +natT = mkType $ (Universe --> Universe) --> (Universe --> Universe) + +mkType :: Eq a => Term b a -> TypedTerm b a +mkType t = typecheckClosed t universeT + +idfun :: Term String String +idfun = lam "x" (Variable "x") + +-- | +-- >>> putStrLn $ ppTypedTermWithSig ["x", "y", "z"] (F.typecheckClosed idfun idfunT) +-- \(x : U).x : (x : U) -> (\(y : U).y) (U) +idfunT :: TypedTerm String String +idfunT = mkType $ Universe --> App idfun Universe -- newtype AType b a = AType { getAType :: Maybe (ATerm (AType b) b a) } -- deriving (Functor, Foldable, Traversable) From dbe49ae698e33f56c795cbc63575403742caf707 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 26 Feb 2021 10:02:49 +0300 Subject: [PATCH 10/10] Add unit types with type-based computation rule --- rzk/src/Rzk/Free/Syntax/Term2.hs | 100 ++++++++++++++++++++++++------- 1 file changed, 77 insertions(+), 23 deletions(-) diff --git a/rzk/src/Rzk/Free/Syntax/Term2.hs b/rzk/src/Rzk/Free/Syntax/Term2.hs index 39c8f8653..68329f0d0 100644 --- a/rzk/src/Rzk/Free/Syntax/Term2.hs +++ b/rzk/src/Rzk/Free/Syntax/Term2.hs @@ -126,6 +126,8 @@ data TermF bound scope term | AppF term term | UniverseF | PiF term scope + | UnitTypeF + | UnitF deriving (Show, Functor, Foldable, Traversable) deriveBifunctor ''TermF @@ -213,7 +215,13 @@ pattern Universe = FreeScoped UniverseF pattern Pi :: Term b a -> Scope1Term b a -> Term b a pattern Pi a b = FreeScoped (PiF a b) -{-# COMPLETE Variable, App, Lambda, Universe, Pi #-} +pattern Unit :: Term b a +pattern Unit = FreeScoped UnitF + +pattern UnitType :: Term b a +pattern UnitType = FreeScoped UnitTypeF + +{-# COMPLETE Variable, App, Lambda, Universe, Pi, Unit, UnitType #-} -- *** Patterns for typed terms @@ -224,18 +232,24 @@ pattern Typed :: TypedTerm b a -> TermF b (Scope1TypedTerm b a) (TypedTerm b a) pattern Typed t term = FreeScoped (TypedTermF t term) pattern AppT :: TypedTerm b a -> TypedTerm b a -> TypedTerm b a -> TypedTerm b a -pattern AppT t t1 t2 = FreeScoped (TypedTermF t (AppF t1 t2)) +pattern AppT t t1 t2 = Typed t (AppF t1 t2) pattern LambdaT :: TypedTerm b a -> Scope1TypedTerm b a -> TypedTerm b a -pattern LambdaT t body = FreeScoped (TypedTermF t (LambdaF body)) +pattern LambdaT t body = Typed t (LambdaF body) pattern UniverseT :: TypedTerm b a -> TypedTerm b a -pattern UniverseT t = FreeScoped (TypedTermF t UniverseF) +pattern UniverseT t = Typed t UniverseF pattern PiT :: TypedTerm b a -> TypedTerm b a -> Scope1TypedTerm b a -> TypedTerm b a -pattern PiT t a b = FreeScoped (TypedTermF t (PiF a b)) +pattern PiT t a b = Typed t (PiF a b) + +pattern UnitT :: TypedTerm b a -> TypedTerm b a +pattern UnitT t = Typed t UnitF -{-# COMPLETE VariableT, AppT, LambdaT, UniverseT, PiT #-} +pattern UnitTypeT :: TypedTerm b a -> TypedTerm b a +pattern UnitTypeT t = Typed t UnitTypeF + +{-# COMPLETE VariableT, AppT, LambdaT, UniverseT, PiT, UnitT, UnitTypeT #-} {-# COMPLETE VariableT, Typed #-} -- ** With annotations @@ -277,6 +291,8 @@ whnf = \case t@Lambda{} -> t t@Universe{} -> t t@Pi{} -> t + t@Unit{} -> t + t@UnitType{} -> t nf :: Term b a -> Term b a nf = \case @@ -288,32 +304,58 @@ nf = \case Pi a b -> Pi (nf a) (nfScope b) t@Variable{} -> t t@Universe{} -> t + t@Unit{} -> t + t@UnitType{} -> t where nfScope = toScope . nf . fromScope -whnfT :: TypedTerm b a -> TypedTerm b a -whnfT = \case +whnfT :: (a -> TypedTerm b a) -> TypedTerm b a -> TypedTerm b a +whnfT typeOfFreeVar = \case AppT t t1 t2 -> - case whnfT t1 of + case whnfT typeOfFreeVar t1 of LambdaT _ body -> instantiate1 t2 body + Typed t1Type _ | PiT _ _ b <- whnfT typeOfFreeVar t1Type, UnitTypeT _ <- fromScope b + -> UnitT (UnitTypeT universeT) + VariableT x | PiT _ _ b <- whnfT typeOfFreeVar (typeOfFreeVar x), UnitTypeT _ <- fromScope b + -> UnitT (UnitTypeT universeT) t1' -> AppT t t1' t2 t@VariableT{} -> t t@LambdaT{} -> t t@UniverseT{} -> t t@PiT{} -> t + t@UnitT{} -> t + t@UnitTypeT{} -> t -nfT :: TypedTerm b a -> TypedTerm b a -nfT = \case - AppT t t1 t2 -> - case whnfT t1 of - LambdaT _ body -> nfT (instantiate1 t2 body) - t1' -> AppT (nfT t) (nfT t1') (nfT t2) - LambdaT t body -> LambdaT (nfT t) (nfScopeT body) - PiT _ a b -> PiT universeT (nfT a) (nfScopeT b) - t@VariableT{} -> t - t@UniverseT{} -> t +whnfTClosed :: TypedTerm b a -> TypedTerm b a +whnfTClosed = whnfT (error "a free variable in a closed term!") + +nfT :: (a -> TypedTerm b a) -> TypedTerm b a -> TypedTerm b a +nfT typeOfFreeVar = nfT' where - nfScopeT = toScope . nfT . fromScope + nfT' = \case + AppT t t1 t2 -> + case whnfT typeOfFreeVar t1 of + LambdaT _ body -> nfT' (instantiate1 t2 body) + Typed t1Type _ | PiT _ _ b <- whnfT typeOfFreeVar t1Type, UnitTypeT _ <- fromScope b + -> UnitT (UnitTypeT universeT) + VariableT x | PiT _ _ b <- whnfT typeOfFreeVar (typeOfFreeVar x), UnitTypeT _ <- fromScope b + -> UnitT (UnitTypeT universeT) + t1' -> AppT (nfT' t) (nfT' t1') (nfT' t2) + LambdaT t@(PiT _ a _) body -> LambdaT (nfT' t) (nfScopeT a body) + LambdaT _ _ -> error "impossible type of Lambda" + PiT _ a b -> PiT universeT (nfT' a) (nfScopeT a b) + t@VariableT{} -> t + t@UniverseT{} -> t + t@UnitT{} -> t + t@UnitTypeT{} -> t + where + nfScopeT typeOfBoundVar = toScope . nfT typeOfVar . fromScope + where + typeOfVar (B (Name _ ())) = F <$> typeOfBoundVar + typeOfVar (F x) = F <$> typeOfFreeVar x + +nfTClosed :: TypedTerm b a -> TypedTerm b a +nfTClosed = nfT (error "a free variable in a closed term!") -- * Pretty-printing @@ -331,6 +373,8 @@ ppTerm vars = \case Pi a b -> let z:zs = vars in parens (z <> " : " <> ppTerm vars a) <> " -> " <> ppTerm zs (instantiate1 (Variable z) b) + Unit -> "unit" + UnitType -> "UNIT" ppTermFun :: [String] -> Term b String -> String ppTermFun vars = \case @@ -360,6 +404,8 @@ ppTypedTerm vars = \case PiT _ a b -> let z:zs = vars in parens (z <> " : " <> ppTypedTerm vars a) <> " -> " <> ppTypedTerm zs (instantiate1 (VariableT z) b) + UnitT _ -> "unit" + UnitTypeT _ -> "UNIT" -- * Typecheck @@ -421,14 +467,16 @@ infer typeOfFreeVar = \case in AppT (instantiate1 t2' b) t1' t2' _ -> error "not a function!" _ -> error "not a function!" - Lambda _body -> error "can't infer Lambda" + term@(Lambda _body) -> error $ "can't infer Lambda: " <> ppTerm ["x", "y", "z"] (unsafeCoerce term) + Unit -> UnitT (UnitTypeT universeT) + UnitType -> UnitTypeT universeT Variable x -> VariableT x typecheck :: Eq a => (a -> TypedTerm b a) -> Term b a -> TypedTerm b a -> TypedTerm b a typecheck typeOfFreeVar term expectedType = case (term, expectedType) of - (Universe, UniverseT{}) -> universeT (Lambda body, PiT _ a b) -> LambdaT expectedType (typecheckScope a typeOfFreeVar body b) + (Lambda _, _) -> error "lambda is expected to be a non-function type?!" (Variable x, _) -> VariableT x _ -> case infer typeOfFreeVar term of @@ -447,7 +495,7 @@ unifyScoped typeOfBoundVar typeOfFreeVar l r unify :: Eq a => (a -> TypedTerm b a) -> TypedTerm b a -> TypedTerm b a -> TypedTerm b a unify typeOfFreeVar = go where - go l r = go' (whnfT l) (whnfT r) + go l r = go' (whnfT typeOfFreeVar l) (whnfT typeOfFreeVar r) go' (UniverseT _) (UniverseT _) = universeT go' (PiT _ a b) (PiT _ c d) = @@ -483,6 +531,12 @@ natT = mkType $ (Universe --> Universe) --> (Universe --> Universe) mkType :: Eq a => Term b a -> TypedTerm b a mkType t = typecheckClosed t universeT +ex1 :: Term String String +ex1 = lam "f" (lam "x" (App (Variable "f") (Variable "x"))) + +ex1Type :: TypedTerm String String +ex1Type = mkType $ piType "f" (Universe --> UnitType) (Universe --> UnitType) + idfun :: Term String String idfun = lam "x" (Variable "x")