diff --git a/lib/Quox/Lexer.idr b/lib/Quox/Lexer.idr index 163f065..cd1bfd5 100644 --- a/lib/Quox/Lexer.idr +++ b/lib/Quox/Lexer.idr @@ -4,8 +4,9 @@ import Quox.CharExtra import Quox.Name import Data.String.Extra import Data.SortedMap -import Text.Lexer -import Text.Lexer.Tokenizer +import public Data.List.Elem +import public Text.Lexer +import public Text.Lexer.Tokenizer import Derive.Prelude %hide TT.Name @@ -25,7 +26,7 @@ data Token = R String | I Name | N Nat | S String | T String | TYPE Nat %runElab derive "Token" [Eq, Ord, Show] -- token or whitespace -private +public export 0 TokenW : Type TokenW = Maybe Token @@ -41,70 +42,51 @@ record Error where %runElab derive "Error" [Eq, Ord, Show] +private skip : Lexer -> Tokenizer TokenW skip t = match t $ const Nothing -export -syntaxChars : List Char -syntaxChars = ['(', ')', '[', ']', '{', '}', '`', '"', '\'', ',', '.'] +private +match : Lexer -> (String -> Token) -> Tokenizer TokenW +match t f = Tokenizer.match t (Just . f) +%hide Tokenizer.match -export -isSymStart, isSymCont : Char -> Bool + +export %inline +syntaxChars : List Char +syntaxChars = ['(', ')', '[', ']', '{', '}', '"', '\'', ',', '.', ';'] + +private +stra, isSymCont : Char -> Bool isSymStart c = not (c `elem` syntaxChars) && isSymChar c isSymCont c = c == '\'' || isSymStart c -export -idStart, idCont, idEnd, idContEnd, symStart, symCont : Lexer +private +idStart, idCont, idEnd, idContEnd : Lexer idStart = pred isIdStart idCont = pred isIdCont idEnd = pred $ \c => c `elem` unpack "?!#" idContEnd = idCont <|> idEnd + +private +symStart, symCont : Lexer symStart = pred isSymStart symCont = pred isSymCont -private %inline -resVal : String -> a -> Maybe Token -resVal str = const $ Just $ R str - -export -resWordL, resSymL, syntaxL : String -> Lexer -resWordL str = exact str <+> reject idContEnd -resSymL str = exact str <+> reject symCont -syntaxL str = exact str - -export -resWord, resSym, syntax : String -> Tokenizer TokenW -resWord str = match (resWordL str) (resVal str) -resSym str = match (resSymL str) (resVal str) -syntax str = match (syntaxL str) (resVal str) - --- return value contains unicode version -export -uresWord, uresSym, usyntax : (unicode, ascii : String) -> Tokenizer TokenW -uresWord u a = match (resWordL u <|> resWordL a) (resVal u) -uresSym u a = match (resSymL u <|> resSymL a) (resVal u) -usyntax u a = match (exact u <|> exact a) (resVal u) - -export -alphaName, symName, baseNameL : Lexer -alphaName = idStart <+> many idCont <+> many idEnd -symName = symStart <+> many symCont -baseNameL = symName <|> alphaName - -export -baseName : Tokenizer BaseName -baseName = match baseNameL UN +private +baseNameL : Lexer +baseNameL = idStart <+> many idCont <+> many idEnd + <|> symStart <+> many symCont private -toName : String -> Name -toName = fromList . split (== '.') +nameL : Lexer +nameL = baseNameL <+> many (is '.' <+> baseNameL) -export +private name : Tokenizer TokenW -name = match (baseNameL <+> many (is '.' <+> baseNameL)) - (Just . I . toName . normalizeNfc) +name = match nameL $ I . fromList . split (== '.') . normalizeNfc --- [todo] escapes other than \" and (accidentally) \\ +||| [todo] escapes other than `\"` and (accidentally) `\\` export fromStringLit : String -> String fromStringLit = pack . go . unpack . drop 1 . dropLast 1 where @@ -114,18 +96,18 @@ fromStringLit = pack . go . unpack . drop 1 . dropLast 1 where go ('\\' :: c :: cs) = c :: go cs go (c :: cs) = c :: go cs -export +private string : Tokenizer TokenW -string = match stringLit (Just . S . fromStringLit) +string = match stringLit (S . fromStringLit) -export +private nat : Tokenizer TokenW -nat = match (some (range '0' '9')) (Just . N . cast) +nat = match (some (range '0' '9')) (N . cast) -export +private tag : Tokenizer TokenW -tag = match (is '`' <+> baseNameL) (Just . T . drop 1) - <|> match (is '`' <+> stringLit) (Just . T . fromStringLit . drop 1) +tag = match (is '\'' <+> nameL) (T . drop 1) + <|> match (is '\'' <+> stringLit) (T . fromStringLit . drop 1) @@ -140,38 +122,115 @@ subToNat : String -> Nat subToNat = cast . pack . map fromSub . unpack -export +private universe : Tokenizer TokenW universe = universeWith "★" <|> universeWith "Type" where universeWith : String -> Tokenizer TokenW universeWith pfx = let len = length pfx in match (exact pfx <+> some (range '0' '9')) - (Just . TYPE . cast . drop len) <|> + (TYPE . cast . drop len) <|> match (exact pfx <+> some (range '₀' '₉')) - (Just . TYPE . subToNat . drop len) + (TYPE . subToNat . drop len) -export +private %inline choice : (xs : List (Tokenizer a)) -> (0 _ : NonEmpty xs) => Tokenizer a choice (t :: ts) = foldl (\a, b => a <|> b) t ts +namespace Res + ||| description of a reserved symbol + ||| @ W a reserved word (must not be followed by letters, digits, etc) + ||| @ S a reserved symbol (must not be followed by symbolic chars) + ||| @ X a character that doesn't show up in names (brackets, etc) + public export + data Res1 = W String | S String | X Char + %runElab derive "Res1" [Eq, Ord, Show] + + ||| description of a token that might have unicode & ascii-only aliases + public export + data Res = Only Res1 | Or Res1 Res1 + %runElab derive "Res" [Eq, Ord, Show] + + public export + S1, W1 : String -> Res + S1 = Only . S + W1 = Only . W + + public export + X1 : Char -> Res + X1 = Only . X + +public export +resString1 : Res1 -> String +resString1 (X x) = singleton x +resString1 (W w) = w +resString1 (S s) = s + +||| return the representative string for a token description. if there are +||| two, then it's the first one, which should be the full-unicode one +public export +resString : Res -> String +resString (Only r) = resString1 r +resString (r `Or` _) = resString1 r + +private +resTokenizer1 : Res1 -> String -> Tokenizer TokenW +resTokenizer1 r str = + let res : String -> Token := const $ R str in + case r of W w => match (exact w <+> reject idContEnd) res + S s => match (exact s <+> reject symCont) res + X x => match (is x) res + +||| match a reserved token +export +resTokenizer : Res -> Tokenizer TokenW +resTokenizer (Only r) = resTokenizer1 r (resString1 r) +resTokenizer (r `Or` s) = + resTokenizer1 r (resString1 r) <|> resTokenizer1 s (resString1 r) + +||| reserved words & symbols. +||| the tokens recognised by ``a `Or` b`` will be `R a`. e.g. `=>` in the input +||| (if not part of a longer name) will be returned as `R "⇒"`. +public export +reserved : List Res +reserved = + [X1 '(', X1 ')', X1 '[', X1 ']', X1 '{', X1 '}', X1 ',', X1 ';', + S1 "@", + S1 ":", + S "⇒" `Or` S "=>", + S "→" `Or` S "->", + S "×" `Or` S "**", + S "≡" `Or` S "==", + S "∷" `Or` S "::", + S "·" `Or` X '.', + W1 "case", + W1 "case1", + W "caseω" `Or` W "case#", + W1 "return", + W1 "of", + W1 "_", + W1 "Eq", + W "λ" `Or` W "fun", + W "δ" `Or` W "dfun", + W "ω" `Or` S "#", + S "★" `Or` W "Type"] + +||| `IsReserved str` is true if `R str` might actually show up in +||| the token stream +public export +IsReserved : String -> Type +IsReserved str = str `Elem` map resString reserved + export tokens : Tokenizer TokenW tokens = choice $ map skip [pred isWhitespace, lineComment (exact "--" <+> reject symCont), blockComment (exact "{-") (exact "-}")] <+> - map syntax ["(", ")", "[", "]", ",", "{", "}", "."] <+> - [match (exact "`{" <+> reject (is '-')) (resVal "`{")] <+> - map resSym ["@", ":"] <+> - map (uncurry uresSym) - [("·", "%"), ("→","->"), ("×", "**"), ("≡", "=="), ("∷", "::")] <+> - map resWord ["case", "case1", "caseω", "return", "of", "_"] <+> - map (uncurry uresWord) [("λ","fun"), ("δ","dfun"), ("caseω", "case#")] <+> - [resWord "ω", match (resSymL "#") (resVal "ω"), - universe, resSym "★", match (resWordL "Type") (resVal "★")] <+> + [universe] <+> -- ★ᵢ takes precedence over bare ★ + map resTokenizer reserved <+> [nat, string, tag, name] export diff --git a/lib/Quox/Parser.idr b/lib/Quox/Parser.idr new file mode 100644 index 0000000..f2252ab --- /dev/null +++ b/lib/Quox/Parser.idr @@ -0,0 +1,326 @@ +module Quox.Parser + +import public Quox.Syntax.Qty.Three +import public Quox.Syntax +import public Quox.Lexer + +import Data.Fin +import Data.Vect +import public Text.Parser + +import Derive.Prelude +%hide TT.Name + +%default total +%language ElabReflection + + +public export +0 Grammar : Bool -> Type -> Type +Grammar = Core.Grammar () Token +%hide Core.Grammar + + +public export +0 BName : Type +BName = Maybe BaseName + +public export +0 PUniverse : Type +PUniverse = Nat + +public export +0 PQty : Type +PQty = Three + +namespace PDim + public export + data PDim = K DimConst | V BaseName + %runElab derive "PDim" [Eq, Ord, Show] + +namespace PTerm + mutual + ||| terms out of the parser with BVs and bidirectionality still tangled up + public export + data PTerm = + TYPE Nat + + | Pi PQty BName PTerm PTerm + | Lam BName PTerm + | (:@) PTerm PTerm + + | Sig BName PTerm PTerm + | Pair PTerm PTerm + | Case PQty PTerm (BName, PTerm) (PCaseBody) + + | Enum (List TagVal) + | Tag TagVal + + | Eq (BName, PTerm) PTerm PTerm + | DLam BName PTerm + | (:%) PTerm PDim + + | V Name + | (:#) PTerm PTerm + + public export + data PCaseBody = + CasePair (BName, BName) PTerm + | CaseEnum (List (TagVal, PTerm)) + + %runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show] + +private +data PArg = T PTerm | D PDim +%runElab derive "PArg" [Eq, Ord, Show] + + +private +apply : PTerm -> List PArg -> PTerm +apply = foldl $ \f, x => case x of T x => f :@ x; D p => f :% p + +private +annotate : PTerm -> Maybe PTerm -> PTerm +annotate s a = maybe s (s :#) a + + +export +res : (str : String) -> (0 _ : IsReserved str) => Grammar True () +res str = terminal "expecting \"\{str}\"" $ + \x => guard $ x == R str + +export +resC : (str : String) -> (0 _ : IsReserved str) => Grammar True () +resC str = do res str; commit + + +parameters {default True commit : Bool} + private + maybeCommit : Grammar False () + maybeCommit = when commit Core.commit + + export + betweenR : {c : Bool} -> (op, cl : String) -> + (0 _ : IsReserved op) => (0 _ : IsReserved cl) => + Grammar c a -> Grammar True a + betweenR o c p = res o *> maybeCommit *> p <* res c <* maybeCommit + + export + parens, bracks, braces : {c : Bool} -> Grammar c a -> Grammar True a + parens = betweenR "(" ")" + bracks = betweenR "[" "]" + braces = betweenR "{" "}" + + +export +commaSep : {c : Bool} -> Grammar c a -> Grammar False (List a) +commaSep = sepEndBy (res ",") + -- don't commit because of the possible terminating "," + +export +semiSep : {c : Bool} -> Grammar c a -> Grammar False (List a) +semiSep = sepEndBy (res ";") + +export +commaSep1 : {c : Bool} -> Grammar c a -> Grammar c (List1 a) +commaSep1 = sepEndBy1 (res ",") + +export +darr : Grammar True () +darr = resC "⇒" + + +export +name : Grammar True Name +name = terminal "expecting name" $ + \case I i => Just i; _ => Nothing + +export +baseName : Grammar True BaseName +baseName = terminal "expecting unqualified name" $ + \case I i => guard (null i.mods) $> i.base + _ => Nothing + +export +nat : Grammar True Nat +nat = terminal "expecting natural number" $ + \case N n => pure n; _ => Nothing + +export +string : Grammar True String +string = terminal "expecting string literal" $ + \case S s => pure s; _ => Nothing + +export +tag : Grammar True String +tag = terminal "expecting tag constructor" $ + \case T t => pure t; _ => Nothing + +export +bareTag : Grammar True String +bareTag = string <|> [|toDots name|] + +export +universe : Grammar True PUniverse +universe = terminal "expecting type universe" $ + \case TYPE u => Just u; _ => Nothing + +export +bname : Grammar True BName +bname = Nothing <$ res "_" + <|> [|Just baseName|] + +export +zeroOne : (zero, one : a) -> Grammar True a +zeroOne zero one = terminal "expecting zero or one" $ + \case N 0 => Just zero; N 1 => Just one; _ => Nothing + + +export covering +qty : Grammar True PQty +qty = zeroOne Zero One + <|> Any <$ res "ω" + <|> parens qty + +private covering +qtys : Grammar False (List PQty) +qtys = option [] [|toList $ some qty <* res "·"|] + +export +dimConst : Grammar True DimConst +dimConst = zeroOne Zero One + +export covering +dim : Grammar True PDim +dim = [|V baseName|] + <|> [|K dimConst|] + <|> parens dim + +private +0 PBinderHead : Nat -> Type +PBinderHead n = (Vect n PQty, BName, PTerm) + +private +toVect : List a -> (n ** Vect n a) +toVect [] = (_ ** []) +toVect (x :: xs) = (_ ** x :: snd (toVect xs)) + +private +0 MakeBinder : Nat -> Type +MakeBinder n = (String, PBinderHead n -> PTerm -> PTerm) + +private +makePi : MakeBinder 1 +makePi = ("→", \([pi], x, s) => Pi pi x s) + +private +makeSig : MakeBinder 0 +makeSig = ("×", \([], x, s) => Sig x s) + +private +plural : Nat -> a -> a -> a +plural 1 s p = s +plural _ s p = p + +private +makeBinder : {m, n : Nat} -> MakeBinder m -> PBinderHead n -> PTerm -> + Grammar False PTerm +makeBinder (str, f) h t = + case decEq m n of + Yes Refl => pure $ f h t + No _ => fatalError + "'\{str}' expects \{show m} quantit\{plural m "y" "ies"}, got \{show n}" + +private +binderInfix : Grammar True (n ** MakeBinder n) +binderInfix = res "→" $> (1 ** makePi) + <|> res "×" $> (0 ** makeSig) + +private +lamIntro : Grammar True (BName -> PTerm -> PTerm) +lamIntro = Lam <$ resC "λ" + <|> DLam <$ resC "δ" + +private covering +caseIntro : Grammar True PQty +caseIntro = resC "case1" $> One + <|> resC "caseω" $> Any + <|> resC "case" *> qty <* resC "·" + +private +optNameBinder : Grammar False BName +optNameBinder = [|join $ optional $ bname <* darr|] + +mutual + export covering + term : Grammar True PTerm + term = lamTerm + <|> caseTerm + <|> bindTerm + <|> [|annotate infixEqTerm (optional $ resC "∷" *> term)|] + + private covering + lamTerm : Grammar True PTerm + lamTerm = flip . foldr <$> lamIntro <*> some bname <* darr <*> term + + private covering + caseTerm : Grammar True PTerm + caseTerm = + [|Case caseIntro term + (resC "return" *> optBinderTerm) + (resC "of" *> braces caseBody)|] + + private covering + caseBody : Grammar False PCaseBody + caseBody = [|CasePair (pairPat <* darr) (term <* optSemi)|] + <|> [|CaseEnum $ semiSep [|MkPair tag (darr *> term)|]|] + where + optSemi = ignore $ optional $ res ";" + pairPat = parens [|MkPair bname (resC "," *> bname)|] + + private covering + bindTerm : Grammar True PTerm + bindTerm = do + bnd <- binderHead + inf <- binderInfix + body <- term + makeBinder (snd inf) (snd bnd) body + + private covering + infixEqTerm : Grammar True PTerm + infixEqTerm = do + l <- appTerm + rty <- optional [|MkPair (resC "≡" *> term) (resC ":" *> appTerm)|] + pure $ maybe l (\rty => Eq (Nothing, snd rty) l (fst rty)) rty + + private covering + appTerm : Grammar True PTerm + appTerm = resC "★" *> [|TYPE nat|] + <|> resC "Eq" *> [|Eq (bracks optBinderTerm) aTerm aTerm|] + <|> [|apply aTerm (many appArg)|] + + private covering + appArg : Grammar True PArg + appArg = [|D $ resC "@" *> dim|] + <|> [|T aTerm|] + + private covering + aTerm : Grammar True PTerm + aTerm = [|Enum $ braces $ commaSep bareTag|] + <|> [|TYPE universe|] + <|> [|V name|] + <|> [|Tag tag|] + <|> foldr1 Pair <$> parens (commaSep1 term) + + private covering + binderHead : Grammar True (n ** PBinderHead n) + binderHead = parens {commit = False} $ do + qs <- [|toVect qtys|] + name <- bname + resC ":" + ty <- term + pure (_ ** (qs.snd, name, ty)) + + private covering + optBinderTerm : Grammar True (BName, PTerm) + optBinderTerm = [|MkPair optNameBinder term|] diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr index b923d4c..4e50f88 100644 --- a/lib/Quox/Syntax/Term/Base.idr +++ b/lib/Quox/Syntax/Term/Base.idr @@ -96,7 +96,7 @@ mutual ||| pair destruction ||| ||| `CasePair 𝜋 𝑒 ([𝑟], 𝐴) ([𝑥, 𝑦], 𝑡)` is - ||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦). 𝑡 }` + ||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }` CasePair : (qty : q) -> (pair : Elim q d n) -> (ret : ScopeTerm q d n) -> (body : ScopeTermN 2 q d n) -> diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index a57899d..0da58c8 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -11,10 +11,11 @@ import Data.Vect private %inline -typeD, arrowD, timesD, lamD, eqndD, dlamD, annD : +typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD : Pretty.HasEnv m => m (Doc HL) typeD = hlF Syntax $ ifUnicode "★" "Type" arrowD = hlF Syntax $ ifUnicode "→" "->" +darrowD = hlF Syntax $ ifUnicode "⇒" "=>" timesD = hlF Syntax $ ifUnicode "×" "**" lamD = hlF Syntax $ ifUnicode "λ" "fun" eqndD = hlF Syntax $ ifUnicode "≡" "==" @@ -22,11 +23,10 @@ dlamD = hlF Syntax $ ifUnicode "δ" "dfun" annD = hlF Syntax $ ifUnicode "∷" "::" private %inline -eqD, colonD, commaD, dotD, caseD, returnD, ofD : Doc HL +eqD, colonD, commaD, caseD, returnD, ofD : Doc HL eqD = hl Syntax "Eq" colonD = hl Syntax ":" commaD = hl Syntax "," -dotD = hl Delim "." caseD = hl Syntax "case" ofD = hl Syntax "of" returnD = hl Syntax "return" @@ -48,7 +48,7 @@ prettyArm : PrettyHL a => Pretty.HasEnv m => BinderSort -> List BaseName -> Doc HL -> a -> m (Doc HL) prettyArm sort xs pat body = do body <- withPrec Outer $ unders sort xs $ prettyM body - pure $ hang 2 $ sep [pat <+> dotD, body] + pure $ hang 2 $ sep [pat <++> !darrowD, body] export prettyLams : PrettyHL a => Pretty.HasEnv m => @@ -96,7 +96,7 @@ prettyCase pi elim r ret arms = do -- [fixme] put delimiters around tags that aren't simple names export prettyTag : TagVal -> Doc HL -prettyTag t = hl Tag $ "`" <+> fromString t +prettyTag t = hl Tag $ "'" <+> fromString t parameters (showSubsts : Bool) @@ -117,7 +117,7 @@ parameters (showSubsts : Bool) let GotPairs {init, last, _} = getPairs' [< s] t in prettyTuple $ toList $ init :< last prettyM (Enum tags) = - pure $ delims "`{" "}" . aseparate comma $ map prettyTag $ + pure $ delims "{" "}" . aseparate comma $ map prettyTag $ Prelude.toList tags prettyM (Tag t) = pure $ prettyTag t diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 484d0da..a778b2f 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -35,4 +35,5 @@ modules = Quox.Name, Quox.Typing, Quox.Typechecker, - Quox.Lexer + Quox.Lexer, + Quox.Parser diff --git a/tests/Tests.idr b/tests/Tests.idr index aaebd75..bdd5124 100644 --- a/tests/Tests.idr +++ b/tests/Tests.idr @@ -5,6 +5,7 @@ import Tests.Reduce import Tests.Equal import Tests.Typechecker import Tests.Lexer +import Tests.Parser import System @@ -13,7 +14,8 @@ allTests = [ Reduce.tests, Equal.tests, Typechecker.tests, - Lexer.tests + Lexer.tests, + Parser.tests ] main : IO () diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index b944a88..ce289ed 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -122,31 +122,31 @@ tests = "equality & subtyping" :- [ ], "lambda" :- [ - testEq "λ x. [x] = λ x. [x]" $ + testEq "λ x ⇒ [x] = λ x ⇒ [x]" $ equalT empty (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0) (["x"] :\\ BVT 0), - testEq "λ x. [x] <: λ x. [x]" $ + testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $ subT empty (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0) (["x"] :\\ BVT 0), - testEq "λ x. [x] = λ y. [y]" $ + testEq "λ x ⇒ [x] = λ y ⇒ [y]" $ equalT empty (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0) (["y"] :\\ BVT 0), - testEq "λ x. [x] <: λ y. [y]" $ + testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $ equalT empty (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0) (["y"] :\\ BVT 0), - testNeq "λ x y. [x] ≠ λ x y. [y]" $ + testNeq "λ x y ⇒ [x] ≠ λ x y ⇒ [y]" $ equalT empty (Arr One (FT "A") $ Arr One (FT "A") (FT "A")) (["x", "y"] :\\ BVT 1) (["x", "y"] :\\ BVT 0), - testEq "λ x. [a] = λ x. [a] (Y vs N)" $ + testEq "λ x ⇒ [a] = λ x ⇒ [a] (Y vs N)" $ equalT empty (Arr Zero (FT "B") (FT "A")) (Lam $ SY ["x"] $ FT "a") (Lam $ SN $ FT "a"), - testEq "λ x. [f [x]] = [f] (η)" $ + testEq "λ x ⇒ [f [x]] = [f] (η)" $ equalT empty (Arr One (FT "A") (FT "A")) (["x"] :\\ E (F "f" :@ BVT 0)) (FT "f") @@ -169,7 +169,7 @@ tests = "equality & subtyping" :- [ refl a x = (DLam $ S ["_"] $ N x) :# (Eq0 a x x) in [ - note #""refl [A] x" is an abbreviation for "(δ i. x) ∷ (x ≡ x : A)""#, + note #""refl [A] x" is an abbreviation for "(δ i ⇒ x) ∷ (x ≡ x : A)""#, note "binds before ∥ are globals, after it are BVs", testEq "refl [A] a = refl [A] a" $ equalE empty (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")), @@ -237,11 +237,11 @@ tests = "equality & subtyping" :- [ equalT empty (FT "A") (CloT (BVT 1) (F "a" ::: F "b" ::: id)) (FT "b"), - testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A (N)" $ + testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A (N)" $ equalT empty (Arr Zero (FT "B") (FT "A")) (CloT (Lam $ S ["y"] $ N $ BVT 0) (F "a" ::: id)) (Lam $ S ["y"] $ N $ FT "a"), - testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A (Y)" $ + testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A (Y)" $ equalT empty (Arr Zero (FT "B") (FT "A")) (CloT (["y"] :\\ BVT 1) (F "a" ::: id)) (["y"] :\\ FT "a") @@ -250,7 +250,7 @@ tests = "equality & subtyping" :- [ "term d-closure" :- [ testEq "★₀‹𝟎› = ★₀ : ★₁" $ equalTD 1 empty (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0), - testEq "(δ i. a)‹𝟎› = (δ i. a) : (a ≡ a : A)" $ + testEq "(δ i ⇒ a)‹𝟎› = (δ i ⇒ a) : (a ≡ a : A)" $ equalTD 1 empty (Eq0 (FT "A") (FT "a") (FT "a")) (DCloT (["i"] :\\% FT "a") (K Zero ::: id)) @@ -315,24 +315,24 @@ tests = "equality & subtyping" :- [ equalE empty (F "f" :@ FT "a") (F "f" :@ FT "a"), testEq "f [a] <: f [a]" $ subE empty (F "f" :@ FT "a") (F "f" :@ FT "a"), - testEq "(λ x. [x] ∷ A ⊸ A) a = ([a ∷ A] ∷ A) (β)" $ + testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = ([a ∷ A] ∷ A) (β)" $ equalE empty (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") (E (FT "a" :# FT "A") :# FT "A"), - testEq "(λ x. [x] ∷ A ⊸ A) a = a (βυ)" $ + testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = a (βυ)" $ equalE empty (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") (F "a"), - testEq "(λ g. [g [a]] ∷ ⋯)) [f] = (λ y. [f [y]] ∷ ⋯) [a] (β↘↙)" $ + testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] = (λ y ⇒ [f [y]] ∷ ⋯) [a] (β↘↙)" $ let a = FT "A"; a2a = (Arr One a a) in equalE empty (((["g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f") (((["y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"), - testEq "(λ x. [x] ∷ A ⊸ A) a <: a" $ + testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $ subE empty (((["x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a") (F "a"), - note "id : A ⊸ A ≔ λ x. [x]", + note "id : A ⊸ A ≔ λ x ⇒ [x]", testEq "id [a] = a" $ equalE empty (F "id" :@ FT "a") (F "a"), testEq "id [a] <: a" $ subE empty (F "id" :@ FT "a") (F "a") ], @@ -340,13 +340,13 @@ tests = "equality & subtyping" :- [ todo "dim application", "annotation" :- [ - testEq "(λ x. f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $ + testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $ equalE empty ((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A")) (FT "f" :# Arr One (FT "A") (FT "A")), testEq "[f] ∷ A ⊸ A = f" $ equalE empty (FT "f" :# Arr One (FT "A") (FT "A")) (F "f"), - testEq "(λ x. f [x]) ∷ A ⊸ A = f" $ + testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = f" $ equalE empty ((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A")) (F "f") diff --git a/tests/Tests/Lexer.idr b/tests/Tests/Lexer.idr index 209eab7..4eaa00a 100644 --- a/tests/Tests/Lexer.idr +++ b/tests/Tests/Lexer.idr @@ -2,7 +2,6 @@ module Tests.Lexer import Quox.Name import Quox.Lexer -import Text.Lexer.Tokenizer import TAP @@ -31,19 +30,14 @@ denewline = pack . map (\case '\n' => '␤'; c => c) . unpack private lexes : String -> List Token -> Test -lexes str toks = test "｢\{denewline str}｣" {e = Failure} $ - case lex str of - Left err => throwError $ LexError err - Right res => - let res = map val res in - unless (toks == res) $ throwError $ WrongLex toks res +lexes str toks = test "｢\{denewline str}｣" $ do + res <- bimap LexError (map val) $ lex str + unless (toks == res) $ throwError $ WrongLex toks res private lexFail : String -> Test -lexFail str = test "｢\{denewline str}｣ # fails" {e = Failure} $ - case lex str of - Left err => pure () - Right res => throwError $ ExpectedFail $ map val res +lexFail str = test "｢\{denewline str}｣ # fails" $ + either (const $ Right ()) (Left . ExpectedFail . map val) $ lex str export tests : Test @@ -68,8 +62,13 @@ tests = "lexer" :- [ lexes "dfun" [R "δ"], lexes "funky" [I "funky"], lexes "δελτα" [I "δελτα"], + lexes "★★" [I "★★"], + lexes "Types" [I "Types"], lexes "a.b.c.d.e" [I $ MakeName [< "a","b","c","d"] "e"], lexes "normalïse" [I "normalïse"], + lexes "map#" [I "map#"], + lexes "write!" [I "write!"], + lexes "uhh??!?!?!?" [I "uhh??!?!?!?"], -- ↑ replace i + combining ¨ with precomposed ï todo "check for reserved words in a qname", @@ -80,16 +79,17 @@ tests = "lexer" :- [ lexes "**" [R "×"], lexes "***" [I "***"], lexes "+**" [I "+**"], + lexes "+#" [I "+#"], lexes "+.+.+" [I $ MakeName [< "+", "+"] "+"], lexes "a.+" [I $ MakeName [< "a"] "+"], lexes "+.a" [I $ MakeName [< "+"] "a"], lexes "+a" [I "+", I "a"], - lexes "x." [I "x", R "."], - lexes "&." [I "&", R "."], - lexes ".x" [R ".", I "x"], - lexes "a.b.c." [I $ MakeName [< "a", "b"] "c", R "."], + lexes "x." [I "x", R "·"], + lexes "&." [I "&", R "·"], + lexes ".x" [R "·", I "x"], + lexes "a.b.c." [I $ MakeName [< "a", "b"] "c", R "·"], lexes "case" [R "case"], lexes "caseω" [R "caseω"], @@ -103,29 +103,27 @@ tests = "lexer" :- [ lexes "a_" [I "a_"], lexes "a'" [I "a'"], - lexes "+'" [I "+'"], - lexFail "'+" + lexes "+'" [I "+'"] ], "syntax characters" :- [ lexes "()" [R "(", R ")"], lexes "(a)" [R "(", I "a", R ")"], lexes "(^)" [R "(", I "^", R ")"], - lexes "`{a,b}" [R "`{", I "a", R ",", I "b", R "}"], - lexes "`{+,-}" [R "`{", I "+", R ",", I "-", R "}"], - lexFail "` {}", - -- [todo] should this be lexed as "`{", "-", "mid", etc? - lexFail "`{-mid token comment-}{}" + lexes "{a,b}" [R "{", I "a", R ",", I "b", R "}"], + lexes "{+,-}" [R "{", I "+", R ",", I "-", R "}"] ], "tags" :- [ - lexes "`a" [T "a"], - lexes "`abc" [T "abc"], - lexes "`+" [T "+"], - lexes "`$$$" [T "$$$"], - lexes #"`"multi word tag""# [T "multi word tag"], - lexFail "`", - lexFail "``" + lexes #" 'a "# [T "a"], + lexes #" 'abc "# [T "abc"], + lexes #" '+ "# [T "+"], + lexes #" '$$$ "# [T "$$$"], + lexes #" 'tag.with.dots "# [T "tag.with.dots"], + lexes #" '"multi word tag" "# [T "multi word tag"], + lexes #" '"" "# [T ""], + lexFail #" ' "#, + lexFail #" '' "# ], "strings" :- [ diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr new file mode 100644 index 0000000..f1b4c1c --- /dev/null +++ b/tests/Tests/Parser.idr @@ -0,0 +1,241 @@ +module Tests.Parser + +import Quox.Parser +import Data.List +import Data.String +import TAP + +public export +data Failure = + LexError Lexer.Error + | ParseError (List1 (ParsingError Token)) + | WrongResult String + | ExpectedFail String + +export +ToInfo Failure where + toInfo (LexError err) = + [("type", "LexError"), ("info", show err)] + toInfo (ParseError errs) = + ("type", "ParseError") :: + map (bimap show show) ([1 .. length errs] `zip` toList errs) + toInfo (WrongResult got) = + [("type", "WrongResult"), ("got", got)] + toInfo (ExpectedFail got) = + [("type", "ExpectedFail"), ("got", got)] + + +parameters {c : Bool} {auto _ : Show a} (grm : Grammar c a) + (inp : String) + parameters {default (ltrim inp) label : String} + parsesWith : (a -> Bool) -> Test + parsesWith p = test label $ do + toks <- mapFst LexError $ lex inp + (res, _) <- mapFst ParseError $ parse (grm <* eof) toks + unless (p res) $ Left $ WrongResult $ show res + + parses : Test + parses = parsesWith $ const True + + parsesAs : Eq a => a -> Test + parsesAs exp = parsesWith (== exp) + + parameters {default "\{ltrim inp} # fails" label : String} + parseFails : Test + parseFails = test label $ do + toks <- mapFst LexError $ lex inp + either (const $ Right ()) (Left . ExpectedFail . show . fst) $ + parse (grm <* eof) toks + + +export +tests : Test +tests = "parser" :- [ + "bound names" :- [ + parsesAs bname "_" Nothing, + parsesAs bname "F" (Just "F"), + parseFails bname "a.b.c" + ], + + "names" :- [ + parsesAs name "x" + (MakeName [<] $ UN "x"), + parsesAs name "Data.String.length" + (MakeName [< "Data", "String"] $ UN "length"), + parseFails name "_" + ], + + "dimensions" :- [ + parsesAs dim "0" (K Zero), + parsesAs dim "1" (K One), + parsesAs dim "ι" (V "ι"), + parsesAs dim "(0)" (K Zero), + parseFails dim "M.x", + parseFails dim "_" + ], + + "quantities" :- [ + parsesAs qty "0" Zero, + parsesAs qty "1" One, + parsesAs qty "ω" Any, + parsesAs qty "#" Any, + parsesAs qty "(#)" Any, + parseFails qty "anythingElse", + parseFails qty "_" + ], + + "enum types" :- [ + parsesAs term #"{}"# (Enum []), + parsesAs term #"{a}"# (Enum ["a"]), + parsesAs term #"{a,}"# (Enum ["a"]), + parsesAs term #"{a.b.c.d}"# (Enum ["a.b.c.d"]), + parsesAs term #"{"hel lo"}"# (Enum ["hel lo"]), + parsesAs term #"{a, b}"# (Enum ["a", "b"]), + parsesAs term #"{a, b,}"# (Enum ["a", "b"]), + parsesAs term #"{a, b, ","}"# (Enum ["a", "b", ","]), + parseFails term #"{,}"# + ], + + "tags" :- [ + parsesAs term #" 'a "# (Tag "a"), + parsesAs term #" 'abc "# (Tag "abc"), + parsesAs term #" '"abc" "# (Tag "abc"), + parsesAs term #" '"a b c" "# (Tag "a b c"), + parsesAs term #" 'a b c "# (Tag "a" :@ V "b" :@ V "c") + {label = "'a b c # application to two args"} + ], + + "universes" :- [ + parsesAs term "★₀" (TYPE 0), + parsesAs term "★1" (TYPE 1), + parsesAs term "★ 2" (TYPE 2), + parsesAs term "Type₃" (TYPE 3), + parsesAs term "Type4" (TYPE 4), + parsesAs term "Type 100" (TYPE 100), + parsesAs term "(Type 1000)" (TYPE 1000), + parseFails term "Type", + parseFails term "★" + ], + + "applications" :- [ + parsesAs term "f" (V "f"), + parsesAs term "f.x.y" (V $ MakeName [< "f", "x"] $ UN "y"), + parsesAs term "f x" (V "f" :@ V "x"), + parsesAs term "f x y" (V "f" :@ V "x" :@ V "y"), + parsesAs term "(f x) y" (V "f" :@ V "x" :@ V "y"), + parsesAs term "f (g x)" (V "f" :@ (V "g" :@ V "x")), + parsesAs term "f (g x) y" (V "f" :@ (V "g" :@ V "x") :@ V "y"), + parsesAs term "f @p" (V "f" :% V "p"), + parsesAs term "f x @p y" (V "f" :@ V "x" :% V "p" :@ V "y") + ], + + "annotations" :- [ + parsesAs term "f :: A" (V "f" :# V "A"), + parsesAs term "f ∷ A" (V "f" :# V "A"), + parsesAs term "f x y ∷ A B C" + ((V "f" :@ V "x" :@ V "y") :# + (V "A" :@ V "B" :@ V "C")), + parsesAs term "Type 0 ∷ Type 1 ∷ Type 2" + (TYPE 0 :# (TYPE 1 :# TYPE 2)) + ], + + "binders" :- [ + parsesAs term "(1·x : A) → B x" $ + Pi One (Just "x") (V "A") (V "B" :@ V "x"), + parsesAs term "(1.x : A) -> B x" $ + Pi One (Just "x") (V "A") (V "B" :@ V "x"), + parsesAs term "(ω·x : A) → B x" $ + Pi Any (Just "x") (V "A") (V "B" :@ V "x"), + parsesAs term "(#.x : A) -> B x" $ + Pi Any (Just "x") (V "A") (V "B" :@ V "x"), + parseFails term "(x : A) → B x", + parseFails term "(1 ω·x : A) → B x", + parsesAs term "(x : A) × B x" $ + Sig (Just "x") (V "A") (V "B" :@ V "x"), + parsesAs term "(x : A) ** B x" $ + Sig (Just "x") (V "A") (V "B" :@ V "x"), + parseFails term "(1·x : A) × B x" + ], + + "lambdas" :- [ + parsesAs term "λ x ⇒ x" $ Lam (Just "x") (V "x"), + parsesAs term "λ x ⇒ x" $ Lam (Just "x") (V "x"), + parsesAs term "fun x => x" $ Lam (Just "x") (V "x"), + parsesAs term "δ i ⇒ x @i" $ DLam (Just "i") (V "x" :% V "i"), + parsesAs term "dfun i => x @i" $ DLam (Just "i") (V "x" :% V "i"), + parsesAs term "λ x y z ⇒ x z y" $ + Lam (Just "x") $ Lam (Just "y") $ Lam (Just "z") $ + V "x" :@ V "z" :@ V "y" + ], + + "pairs" :- [ + parsesAs term "(x, y)" $ + Pair (V "x") (V "y"), + parsesAs term "(x, y, z)" $ + Pair (V "x") (Pair (V "y") (V "z")), + parsesAs term "((x, y), z)" $ + Pair (Pair (V "x") (V "y")) (V "z"), + parsesAs term "(f x, g @y)" $ + Pair (V "f" :@ V "x") (V "g" :% V "y"), + parsesAs term "((x : A) × B, (0·x : C) → D)" $ + Pair (Sig (Just "x") (V "A") (V "B")) + (Pi Zero (Just "x") (V "C") (V "D")), + parsesAs term "(λ x ⇒ x, δ i ⇒ e @i)" $ + Pair (Lam (Just "x") (V "x")) + (DLam (Just "i") (V "e" :% V "i")), + parsesAs term "(x,)" (V "x"), -- i GUESS + parseFails term "(,y)", + parseFails term "(x,,y)" + ], + + "equality type" :- [ + parsesAs term "Eq [i ⇒ A] s t" $ + Eq (Just "i", V "A") (V "s") (V "t"), + parsesAs term "Eq [i ⇒ A B (C @i)] (f x y) (g y z)" $ + Eq (Just "i", V "A" :@ V "B" :@ (V "C" :% V "i")) + (V "f" :@ V "x" :@ V "y") (V "g" :@ V "y" :@ V "z"), + parsesAs term "Eq [A] s t" $ + Eq (Nothing, V "A") (V "s") (V "t"), + parsesAs term "s ≡ t : A" $ + Eq (Nothing, V "A") (V "s") (V "t"), + parsesAs term "s == t : A" $ + Eq (Nothing, V "A") (V "s") (V "t"), + parsesAs term "f x y ≡ g y z : A B C" $ + Eq (Nothing, V "A" :@ V "B" :@ V "C") + (V "f" :@ V "x" :@ V "y") (V "g" :@ V "y" :@ V "z"), + parseFails term "Eq", + parseFails term "Eq s t", + parseFails term "s ≡ t", + parseFails term "≡" + ], + + "case" :- [ + parsesAs term + "case1 f s return x ⇒ A x of { (l, r) ⇒ add l r }" $ + Case One (V "f" :@ V "s") + (Just "x", V "A" :@ V "x") + (CasePair (Just "l", Just "r") + (V "add" :@ V "l" :@ V "r")), + parsesAs term + "case1 f s return x ⇒ A x of { (l, r) ⇒ add l r; }" $ + Case One (V "f" :@ V "s") + (Just "x", V "A" :@ V "x") + (CasePair (Just "l", Just "r") + (V "add" :@ V "l" :@ V "r")), + parsesAs term + "case 1 · f s return x ⇒ A x of { (l, r) ⇒ add l r }" $ + Case One (V "f" :@ V "s") + (Just "x", V "A" :@ V "x") + (CasePair (Just "l", Just "r") + (V "add" :@ V "l" :@ V "r")), + parsesAs term + "case1 t return A of { 'x ⇒ p; 'y ⇒ q; 'z ⇒ r }" $ + Case One (V "t") + (Nothing, V "A") + (CaseEnum [("x", V "p"), ("y", V "q"), ("z", V "r")]), + parsesAs term "caseω t return A of {}" $ + Case Any (V "t") (Nothing, V "A") (CaseEnum []), + parsesAs term "case# t return A of {}" $ + Case Any (V "t") (Nothing, V "A") (CaseEnum []) + ] +] diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr index ae6379e..16fde76 100644 --- a/tests/Tests/Typechecker.idr +++ b/tests/Tests/Typechecker.idr @@ -207,14 +207,14 @@ tests = "typechecker" :- [ ], "enum types" :- [ - testTC "0 · `{} ⇐ ★₀" $ check_ (ctx [<]) szero (enum []) (TYPE 0), - testTC "0 · `{} ⇐ ★₃" $ check_ (ctx [<]) szero (enum []) (TYPE 3), - testTC "0 · `{a,b,c} ⇐ ★₀" $ + testTC "0 · {} ⇐ ★₀" $ check_ (ctx [<]) szero (enum []) (TYPE 0), + testTC "0 · {} ⇐ ★₃" $ check_ (ctx [<]) szero (enum []) (TYPE 3), + testTC "0 · {a,b,c} ⇐ ★₀" $ check_ (ctx [<]) szero (enum ["a", "b", "c"]) (TYPE 0), - testTC "0 · `{a,b,c} ⇐ ★₃" $ + testTC "0 · {a,b,c} ⇐ ★₃" $ check_ (ctx [<]) szero (enum ["a", "b", "c"]) (TYPE 3), - testTCFail "1 · `{} ⇍ ★₀" $ check_ (ctx [<]) sone (enum []) (TYPE 0), - testTC "0=1 ⊢ 1 · `{} ⇐ ★₀" $ check_ (ctx01 [<]) sone (enum []) (TYPE 0) + testTCFail "1 · {} ⇍ ★₀" $ check_ (ctx [<]) sone (enum []) (TYPE 0), + testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ (ctx01 [<]) sone (enum []) (TYPE 0) ], "free vars" :- [ @@ -229,7 +229,7 @@ tests = "typechecker" :- [ note "(fail) runtime-relevant type", testTCFail "1 · A ⇏ ★₀" $ infer_ (ctx [<]) sone (F "A"), - note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x. δ _. x)", + note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)", testTC "1 · refl ⇒ ⋯" $ inferAs (ctx [<]) sone (F "refl") reflTy, testTC "1 · [refl] ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy ], @@ -248,21 +248,21 @@ tests = "typechecker" :- [ "lambda" :- [ note "linear & unrestricted identity", - testTC "1 · (λ x. x) ⇐ A ⊸ A" $ + testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $ check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")), - testTC "1 · (λ x. x) ⇐ A → A" $ + testTC "1 · (λ x ⇒ x) ⇐ A → A" $ check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")), note "(fail) zero binding used relevantly", - testTCFail "1 · (λ x. x) ⇍ A ⇾ A" $ + testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $ check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")), note "(but ok in overall erased context)", - testTC "0 · (λ x. x) ⇐ A ⇾ A" $ + testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $ check_ (ctx [<]) szero (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")), - testTC "1 · (λ A x. refl A x) ⇐ ⋯ # (type of refl)" $ + testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $ check_ (ctx [<]) sone (["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0])) reflTy, - testTC "1 · (λ A x. δ i. x) ⇐ ⋯ # (def. and type of refl)" $ + testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $ check_ (ctx [<]) sone reflDef reflTy ], @@ -272,59 +272,59 @@ tests = "typechecker" :- [ testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $ checkQ (ctx [< FT "A"]) sone (Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any], - testTC "1 · (a, δ i. a) ⇐ (x : A) × (x ≡ a)" $ + testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $ check_ (ctx [<]) sone (Pair (FT "a") (["i"] :\\% FT "a")) (Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a")) ], "unpairing" :- [ - testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r). f2 l r) ⇒ B ⊳ 1·x" $ + testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $ inferAsQ (ctx [< FT "A" `And` FT "A"]) sone (CasePair One (BV 0) (SN $ FT "B") (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (FT "B") [< One], - testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r). f2 l r) ⇒ B ⊳ ω·x" $ + testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $ inferAsQ (ctx [< FT "A" `And` FT "A"]) sone (CasePair Any (BV 0) (SN $ FT "B") (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (FT "B") [< Any], - testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r). f2 l r) ⇒ B ⊳ 0·x" $ + testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $ inferAsQ (ctx [< FT "A" `And` FT "A"]) szero (CasePair Any (BV 0) (SN $ FT "B") (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (FT "B") [< Zero], - testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r). f2 l r) ⇏" $ + testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $ infer_ (ctx [< FT "A" `And` FT "A"]) sone (CasePair Zero (BV 0) (SN $ FT "B") (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])), - testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r). l) ⇒ A ⊳ ω·x" $ + testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $ inferAsQ (ctx [< FT "A" `And` FT "B"]) sone (CasePair Any (BV 0) (SN $ FT "A") (SY ["l", "r"] $ BVT 1)) (FT "A") [< Any], - testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r). l) ⇒ A ⊳ 0·x" $ + testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $ inferAsQ (ctx [< FT "A" `And` FT "B"]) szero (CasePair One (BV 0) (SN $ FT "A") (SY ["l", "r"] $ BVT 1)) (FT "A") [< Zero], - testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r). l) ⇏" $ + testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $ infer_ (ctx [< FT "A" `And` FT "B"]) sone (CasePair One (BV 0) (SN $ FT "A") (SY ["l", "r"] $ BVT 1)), note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A", - note " ≔ (λ A B p. caseω p return A of (x, y). x)", + note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)", testTC "0 · ‹type of fst› ⇐ ★₂" $ check_ (ctx [<]) szero fstTy (TYPE 2), testTC "1 · ‹def of fst› ⇐ ‹type of fst›" $ check_ (ctx [<]) sone fstDef fstTy, note "snd : (0·A : ★₁) → (0·B : A ↠ ★₁) → (ω·p : (x : A) × B x) → B (fst A B p)", - note " ≔ (λ A B p. caseω p return p. B (fst A B p) of (x, y). y)", + note " ≔ (λ A B p ⇒ caseω p return p ⇒ B (fst A B p) of (x, y) ⇒ y)", testTC "0 · ‹type of snd› ⇐ ★₂" $ check_ (ctx [<]) szero sndTy (TYPE 2), testTC "1 · ‹def of snd› ⇐ ‹type of snd›" $ check_ (ctx [<]) sone sndDef sndTy, - testTC "0 · snd ★₀ (λ x. x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x. x) p" $ + testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $ inferAs (ctx [<]) szero (F "snd" :@@ [TYPE 0, ["x"] :\\ BVT 0]) (Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $ @@ -332,27 +332,27 @@ tests = "typechecker" :- [ ], "enums" :- [ - testTC "1 · `a ⇐ `{a}" $ + testTC "1 · `a ⇐ {a}" $ check_ (ctx [<]) sone (Tag "a") (enum ["a"]), - testTC "1 · `a ⇐ `{a, b, c}" $ + testTC "1 · `a ⇐ {a, b, c}" $ check_ (ctx [<]) sone (Tag "a") (enum ["a", "b", "c"]), - testTCFail "1 · `a ⇍ `{b, c}" $ + testTCFail "1 · `a ⇍ {b, c}" $ check_ (ctx [<]) sone (Tag "a") (enum ["b", "c"]), - testTC "0=1 ⊢ 1 · `a ⇐ `{b, c}" $ + testTC "0=1 ⊢ 1 · `a ⇐ {b, c}" $ check_ (ctx01 [<]) sone (Tag "a") (enum ["b", "c"]) ], "equalities" :- [ - testTC "1 · (δ i. a) ⇐ a ≡ a" $ + testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $ check_ (ctx [<]) sone (DLam $ SN $ FT "a") (Eq0 (FT "A") (FT "a") (FT "a")), - testTC "0 · (λ p q. δ i. p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ + testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ check_ (ctx [<]) szero (["p","q"] :\\ ["i"] :\\% BVT 1) (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)), - testTC "0 · (λ p q. δ i. q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ + testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ check_ (ctx [<]) szero (["p","q"] :\\ ["i"] :\\% BVT 0) (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ @@ -363,8 +363,8 @@ tests = "typechecker" :- [ "misc" :- [ note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x", note "⊢", - note "1 · λ x y xy. δ i. p (xy i)", - note " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i. P (xy i)] (p x) (p y)", + note "1 · λ x y xy ⇒ δ i ⇒ p (xy i)", + note " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)", testTC "cong" $ check_ (ctx [<]) sone (["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0))) @@ -376,7 +376,7 @@ tests = "typechecker" :- [ note "0·A : Type, 0·P : ω·A → Type,", note "ω·p q : (1·x : A) → P x", note "⊢", - note "1 · λ eq. δ i. λ x. eq x i", + note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i", note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q", testTC "funext" $ check_ (ctx [<]) sone diff --git a/tests/quox-tests.ipkg b/tests/quox-tests.ipkg index 95eac27..5d91630 100644 --- a/tests/quox-tests.ipkg +++ b/tests/quox-tests.ipkg @@ -9,4 +9,6 @@ modules = TypingImpls, Tests.Reduce, Tests.Equal, - Tests.Typechecker + Tests.Typechecker, + Tests.Lexer, + Tests.Parser