From c81aabcc14e59ffc65e68a07cce53c3336ef136e Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 12 Mar 2023 18:28:37 +0100 Subject: [PATCH] more parser/FromParser stuff - top level semicolons optional - type optional [the def will need to be an elim] - `load` statement - namespaces --- lib/Quox/Context.idr | 8 + lib/Quox/Name.idr | 79 +++++--- lib/Quox/Parser.idr | 280 +-------------------------- lib/Quox/Parser/FromParser.idr | 212 +++++++++++++++++++++ lib/Quox/{ => Parser}/Lexer.idr | 10 +- lib/Quox/Parser/Parser.idr | 328 ++++++++++++++++++++++++++++++++ lib/Quox/Parser/Syntax.idr | 240 +++++------------------ lib/quox-lib.ipkg | 4 +- tests/Tests/FromPTerm.idr | 31 ++- tests/Tests/Parser.idr | 62 +++--- 10 files changed, 716 insertions(+), 538 deletions(-) create mode 100644 lib/Quox/Parser/FromParser.idr rename lib/Quox/{ => Parser}/Lexer.idr (97%) create mode 100644 lib/Quox/Parser/Parser.idr diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr index d481a1d..a2cd868 100644 --- a/lib/Quox/Context.idr +++ b/lib/Quox/Context.idr @@ -6,6 +6,7 @@ import Quox.Pretty import Data.DPair import Data.Nat import Data.SnocList +import Data.Vect import Control.Monad.Identity %default total @@ -64,6 +65,13 @@ public export tel1 . [<] = tel1 tel1 . (tel2 :< s) = (tel1 . tel2) :< s +export +(<><) : Telescope' a from to -> Vect n a -> Telescope' a from (n + to) +(<><) tel [] = tel +(<><) tel (x :: xs) {n = S n} = + rewrite plusSuccRightSucc n to in + (tel :< x) <>< xs + public export getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) -> diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr index 372c9f1..20d16d8 100644 --- a/lib/Quox/Name.idr +++ b/lib/Quox/Name.idr @@ -13,50 +13,85 @@ import Derive.Prelude public export data BaseName = UN String -- user-given name +| Unused -- "_" %runElab derive "BaseName" [Eq, Ord] -export -Show BaseName where - show (UN x) = x - - export baseStr : BaseName -> String baseStr (UN x) = x +baseStr Unused = "_" -export -FromString BaseName where - fromString = UN +export Show BaseName where show = baseStr +export FromString BaseName where fromString = UN + + +public export +Mods : Type +Mods = SnocList String public export record Name where constructor MakeName - mods : SnocList String + mods : Mods base : BaseName %runElab derive "Name" [Eq, Ord] -export -Show Name where - show (MakeName mods base) = - concat $ intersperse "." $ toList $ mods :< show base - -export -FromString Name where - fromString x = MakeName [<] (fromString x) - public export %inline unq : BaseName -> Name unq = MakeName [<] +||| add some namespaces to the beginning of a name +public export %inline +addMods : Mods -> Name -> Name +addMods ms = {mods $= (ms <+>)} + + +public export +PBaseName : Type +PBaseName = String + +public export +record PName where + constructor MakePName + mods : Mods + base : String +%runElab derive "PName" [Eq, Ord] + +export %inline +fromPName : PName -> Name +fromPName p = MakeName p.mods $ UN p.base + +export %inline +toPName : Name -> PName +toPName p = MakePName p.mods $ baseStr p.base + +export +Show PName where + show (MakePName mods base) = concat $ intersperse "." $ toList $ mods :< base + +export Show Name where show = show . toPName + +export FromString PName where fromString = MakePName [<] + +export FromString Name where fromString = fromPName . fromString + + +export +toDotsP : PName -> String +toDotsP x = fastConcat $ cast $ map (<+> ".") x.mods :< x.base export toDots : Name -> String toDots x = fastConcat $ cast $ map (<+> ".") x.mods :< baseStr x.base export -fromList : List1 String -> Name -fromList (x ::: xs) = go [<] x xs where - go : SnocList String -> String -> List String -> Name - go mods x [] = MakeName mods (UN x) +fromListP : List1 String -> PName +fromListP (x ::: xs) = go [<] x xs where + go : SnocList String -> String -> List String -> PName + go mods x [] = MakePName mods x go mods x (y :: ys) = go (mods :< x) y ys + +export %inline +fromList : List1 String -> Name +fromList = fromPName . fromListP diff --git a/lib/Quox/Parser.idr b/lib/Quox/Parser.idr index 9276178..b9806fa 100644 --- a/lib/Quox/Parser.idr +++ b/lib/Quox/Parser.idr @@ -1,280 +1,6 @@ module Quox.Parser -import public Quox.Lexer import public Quox.Parser.Syntax - -import Data.Fin -import Data.Vect -import public Text.Parser - -%default total - - -public export -0 Grammar : Bool -> Type -> Type -Grammar = Core.Grammar () Token -%hide Core.Grammar - - -export -res : (str : String) -> (0 _ : IsReserved str) => Grammar True () -res str = terminal "expecting \"\{str}\"" $ - \x => guard $ x == Reserved 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 Name i => Just i; _ => Nothing - -export -baseName : Grammar True BaseName -baseName = terminal "expecting unqualified name" $ - \case Name i => guard (null i.mods) $> i.base - _ => Nothing - -export -nat : Grammar True Nat -nat = terminal "expecting natural number" $ - \case Nat n => pure n; _ => Nothing - -export -string : Grammar True String -string = terminal "expecting string literal" $ - \case Str s => pure s; _ => Nothing - -export -tag : Grammar True String -tag = terminal "expecting tag constructor" $ - \case Tag 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 Nat 0 => Just zero; Nat 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 -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 _ => - let q = if m == 1 then "quantity" else "quantities" in - fatalError "'\{str}' expects \{show m} \{q}, 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)|] - where - annotate : PTerm -> Maybe PTerm -> PTerm - annotate s a = maybe s (s :#) a - - 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)|] - where - data PArg = TermArg PTerm | DimArg PDim - - appArg : Grammar True PArg - appArg = [|DimArg $ resC "@" *> dim|] - <|> [|TermArg aTerm|] - - apply : PTerm -> List PArg -> PTerm - apply = foldl apply1 where - apply1 : PTerm -> PArg -> PTerm - apply1 f (TermArg x) = f :@ x - apply1 f (DimArg p) = f :% p - - 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.fst ** (qs.snd, name, ty)) - - private covering - optBinderTerm : Grammar True (BName, PTerm) - optBinderTerm = [|MkPair optNameBinder term|] - - -export covering -defIntro : Grammar True PQty -defIntro = Zero <$ resC "def0" - <|> Any <$ resC "defω" - <|> resC "def" *> option Any (qty <* resC "·") - -export covering -definition : Grammar True PDefinition -definition = - [|MkPDef defIntro name (resC ":" *> term) (resC "≔" *> term)|] <* resC ";" - -export covering -input : Grammar False (List PDefinition) -input = many definition +import public Quox.Parser.Lexer +import public Quox.Parser.Parser +import public Quox.Parser.FromParser diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr new file mode 100644 index 0000000..136c0ca --- /dev/null +++ b/lib/Quox/Parser/FromParser.idr @@ -0,0 +1,212 @@ +||| take freshly-parsed input, translate it to core, and check it +module Quox.Parser.FromParser + +import Quox.Parser.Syntax +import Quox.Typechecker +import Data.List + +import public Control.Monad.Either +import public Control.Monad.State +import public Control.Monad.Reader + + +public export +data FromParserError = + AnnotationNeeded PTerm + | DuplicatesInEnum (List TagVal) + | DimNotInScope PBaseName + | QtyNotGlobal PQty + | DimNameInTerm PBaseName + +public export +interface LoadFile m where + loadFile : (file : String) -> m PTopLevel + +public export +0 CanError : (Type -> Type) -> Type +CanError = MonadError FromParserError + +public export +0 HasNamespace : (Type -> Type) -> Type +HasNamespace = MonadReader Mods + +public export +0 HasSeenFiles : (Type -> Type) -> Type +HasSeenFiles = MonadState (SortedSet String) + +public export +0 FromParser : (Type -> Type) -> Type +FromParser m = (CanError m, HasNamespace m, HasSeenFiles m) + + + +parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a) + (xs : Context' BName n) + private + fromBaseName : PBaseName -> m a + fromBaseName x = maybe (f $ MakePName [<] x) b $ Context.find (== Just x) xs + + private + fromName : PName -> m a + fromName x = if null x.mods then fromBaseName x.base else f x + +export +fromPDimWith : CanError m => + Context' BName d -> PDim -> m (Dim d) +fromPDimWith ds (K e) = pure $ K e +fromPDimWith ds (V i) = + fromBaseName (pure . B) (const $ throwError $ DimNotInScope i) ds i + +private +avoidDim : CanError m => Context' BName d -> PName -> m (Term q d n) +avoidDim ds x = + fromName (const $ throwError $ DimNameInTerm x.base) + (pure . FT . fromPName) ds x + + +mutual + export + fromPTermWith : CanError m => + Context' BName d -> Context' BName n -> + PTerm -> m (Term Three d n) + fromPTermWith ds ns t0 = case t0 of + TYPE k => + pure $ TYPE $ k + + Pi pi x s t => + Pi pi <$> fromPTermWith ds ns s + <*> fromPTermTScope ds ns [x] t + + Lam x s => + Lam <$> fromPTermTScope ds ns [x] s + + s :@ t => + map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t + + Sig x s t => + Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [x] t + + Pair s t => + Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t + + Case pi pair (r, ret) (CasePair (x, y) body) => + map E $ Base.CasePair pi + <$> fromPTermElim ds ns pair + <*> fromPTermTScope ds ns [r] ret + <*> fromPTermTScope ds ns [x, y] body + + Case pi tag (r, ret) (CaseEnum arms) => + map E $ Base.CaseEnum pi + <$> fromPTermElim ds ns tag + <*> fromPTermTScope ds ns [r] ret + <*> assert_total fromPTermEnumArms ds ns arms + + Enum strs => + let set = SortedSet.fromList strs in + if length strs == length (SortedSet.toList set) then + pure $ Enum set + else + throwError $ DuplicatesInEnum strs + + Tag str => pure $ Tag str + + Eq (i, ty) s t => + Eq <$> fromPTermDScope ds ns [i] ty + <*> fromPTermWith ds ns s + <*> fromPTermWith ds ns t + + DLam i s => + DLam <$> fromPTermDScope ds ns [i] s + + s :% p => + map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p + + V x => + fromName (pure . E . B) (avoidDim ds) ns x + + s :# a => + map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a + + private + fromPTermEnumArms : CanError m => + Context' BName d -> Context' BName n -> + List (TagVal, PTerm) -> m (CaseEnumArms Three d n) + fromPTermEnumArms ds ns = + map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns) + + private + fromPTermElim : CanError m => + Context' BName d -> Context' BName n -> + PTerm -> m (Elim Three d n) + fromPTermElim ds ns e = + case !(fromPTermWith ds ns e) of + E e => pure e + _ => throwError $ AnnotationNeeded e + + -- [todo] use SN if the var is named but still unused + private + fromPTermTScope : {s : Nat} -> CanError m => + Context' BName d -> Context' BName n -> + Vect s BName -> + PTerm -> m (ScopeTermN s Three d n) + fromPTermTScope ds ns xs t = + if all isNothing xs then + SN <$> fromPTermWith ds ns t + else + SY (map (maybe Unused UN) xs) <$> fromPTermWith ds (ns <>< xs) t + + private + fromPTermDScope : {s : Nat} -> CanError m => + Context' BName d -> Context' BName n -> + Vect s BName -> + PTerm -> m (DScopeTermN s Three d n) + fromPTermDScope ds ns xs t = + if all isNothing xs then + SN <$> fromPTermWith ds ns t + else + SY (map (maybe Unused UN) xs) <$> fromPTermWith (ds <>< xs) ns t + + +export %inline +fromPTerm : CanError m => PTerm -> m (Term Three 0 0) +fromPTerm = fromPTermWith [<] [<] + + +export +globalPQty : CanError m => (q : PQty) -> m (IsGlobal q) +globalPQty pi = case isGlobal pi of + Yes y => pure y + No n => throwError $ QtyNotGlobal pi + + + +-- -- [todo] extend substitutions so they can do this injection. that's the sort of +-- -- thing they are for. +-- export +-- fromPDefinition : FromParser m => PDefinition -> m (Name, Definition Three) +-- fromPDefinition (MkPDef {name, qty, type, term}) = +-- pure (addMods !ask $ fromPName name, MkDef' { +-- qty, qtyGlobal = !(globalPQty qty), +-- type = T $ inject !(fromPTerm type), +-- term = Just $ T $ inject !(fromPTerm term) +-- }) + + +-- export +-- fromPDecl : FromParser m => PDecl -> m (List (Name, Definition Three)) +-- fromPDecl (PDef def) = singleton <$> fromPDefinition def +-- fromPDecl (PNs ns) = local (<+> ns.name) $ +-- concat <$> assert_total traverse fromPDecl ns.decls + + +-- export covering +-- fromPTopLevel : (FromParser m, LoadFile m) => +-- PTopLevel -> m (List (Name, Definition Three)) +-- fromPTopLevel (PD decl) = fromPDecl decl +-- fromPTopLevel (PLoad file) = +-- if contains file !get then +-- pure [] +-- else do +-- modify $ insert file +-- t <- loadFile file +-- fromPTopLevel t diff --git a/lib/Quox/Lexer.idr b/lib/Quox/Parser/Lexer.idr similarity index 97% rename from lib/Quox/Lexer.idr rename to lib/Quox/Parser/Lexer.idr index 8144571..9c38a00 100644 --- a/lib/Quox/Lexer.idr +++ b/lib/Quox/Parser/Lexer.idr @@ -1,4 +1,4 @@ -module Quox.Lexer +module Quox.Parser.Lexer import Quox.CharExtra import Quox.Name @@ -25,7 +25,7 @@ import Derive.Prelude public export data Token = Reserved String - | Name Name + | Name PName | Nat Nat | Str String | Tag String @@ -91,7 +91,7 @@ nameL = baseNameL <+> many (is '.' <+> baseNameL) private name : Tokenizer TokenW -name = match nameL $ Name . fromList . split (== '.') . normalizeNfc +name = match nameL $ Name . fromListP . split (== '.') . normalizeNfc ||| [todo] escapes other than `\"` and (accidentally) `\\` export @@ -228,7 +228,9 @@ reserved = Word1 "def", Word1 "def0", Word "defω" `Or` Word "def#", - Sym "≔" `Or` Sym ":="] + Sym "≔" `Or` Sym ":=", + Word1 "load", + Word1 "namespace"] ||| `IsReserved str` is true if `Reserved str` might actually show up in ||| the token stream diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr new file mode 100644 index 0000000..cc61f64 --- /dev/null +++ b/lib/Quox/Parser/Parser.idr @@ -0,0 +1,328 @@ +module Quox.Parser.Parser + +import public Quox.Parser.Lexer +import public Quox.Parser.Syntax + +import Data.Fin +import Data.Vect +import public Text.Parser + +%default total + + +public export +0 Grammar : Bool -> Type -> Type +Grammar = Core.Grammar () Token +%hide Core.Grammar + + +export +res : (str : String) -> (0 _ : IsReserved str) => Grammar True () +res str = terminal "expecting \"\{str}\"" $ + \x => guard $ x == Reserved 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 PName +name = terminal "expecting name" $ + \case Name i => Just i; _ => Nothing + +export +mods : Grammar True Mods +mods = name <&> \n => n.mods :< n.base + +export +baseName : Grammar True String +baseName = terminal "expecting unqualified name" $ + \case Name i => guard (null i.mods) $> i.base + _ => Nothing + +export +nat : Grammar True Nat +nat = terminal "expecting natural number" $ + \case Nat n => pure n; _ => Nothing + +export +string : Grammar True String +string = terminal "expecting string literal" $ + \case Str s => pure s; _ => Nothing + +export +tag : Grammar True String +tag = terminal "expecting tag constructor" $ + \case Tag t => pure t; _ => Nothing + +export +bareTag : Grammar True String +bareTag = string <|> [|toDotsP 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 Nat 0 => Just zero; Nat 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 +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 _ => + let q = if m == 1 then "quantity" else "quantities" in + fatalError "'\{str}' expects \{show m} \{q}, 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)|] + where + annotate : PTerm -> Maybe PTerm -> PTerm + annotate s a = maybe s (s :#) a + + 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)|] + where + data PArg = TermArg PTerm | DimArg PDim + + appArg : Grammar True PArg + appArg = [|DimArg $ resC "@" *> dim|] + <|> [|TermArg aTerm|] + + apply : PTerm -> List PArg -> PTerm + apply = foldl apply1 where + apply1 : PTerm -> PArg -> PTerm + apply1 f (TermArg x) = f :@ x + apply1 f (DimArg p) = f :% p + + 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.fst ** (qs.snd, name, ty)) + + private covering + optBinderTerm : Grammar True (BName, PTerm) + optBinderTerm = [|MkPair optNameBinder term|] + + +export covering +defIntro : Grammar True PQty +defIntro = Zero <$ resC "def0" + <|> Any <$ resC "defω" + <|> resC "def" *> option Any (qty <* resC "·") + +export covering +definition : Grammar True PDefinition +definition = + [|MkPDef defIntro name + (optional (resC ":" *> term)) + (resC "≔" *> term)|] + +export +load : Grammar True String +load = resC "load" *> string + +mutual + export covering + namespace_ : Grammar True PNamespace + namespace_ = + [|MkPNamespace (resC "namespace" *> mods) (braces $ many decl)|] + + export covering + decl : Grammar True PDecl + decl = [|PDef definition|] + <|> [|PNs namespace_|] + +export covering +topLevel : Grammar True PTopLevel +topLevel = [|PLoad load|] + <|> [|PD decl|] + +export covering +input : Grammar False (List PTopLevel) +input = skipSemis *> many (topLevel <* skipSemis) + where skipSemis = ignore $ many $ resC ";" + + +public export +data Error = + LexError Lexer.Error + | ParseError (List1 (ParsingError Token)) +%hide Lexer.Error + +export +lexParseWith : {c : Bool} -> Grammar c a -> String -> Either Error a +lexParseWith grm input = do + toks <- mapFst LexError $ lex input + bimap ParseError fst $ parse (grm <* eof) toks + +export covering %inline +lexParseInput : String -> Either Error (List PTopLevel) +lexParseInput = lexParseWith input + +export covering %inline +lexParseTerm : String -> Either Error PTerm +lexParseTerm = lexParseWith term diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr index c3cee48..aaf13dd 100644 --- a/lib/Quox/Parser/Syntax.idr +++ b/lib/Quox/Parser/Syntax.idr @@ -4,8 +4,6 @@ import public Quox.Syntax import public Quox.Syntax.Qty.Three import public Quox.Definition -import public Control.Monad.Either - import Derive.Prelude %hide TT.Name @@ -15,7 +13,7 @@ import Derive.Prelude public export 0 BName : Type -BName = Maybe BaseName +BName = Maybe String public export 0 PUniverse : Type @@ -27,7 +25,7 @@ PQty = Three namespace PDim public export - data PDim = K DimConst | V BaseName + data PDim = K DimConst | V PBaseName %name PDim p, q %runElab derive "PDim" [Eq, Ord, Show] @@ -53,7 +51,7 @@ namespace PTerm | DLam BName PTerm | (:%) PTerm PDim - | V Name + | V PName | (:#) PTerm PTerm %name PTerm s, t @@ -70,15 +68,35 @@ public export record PDefinition where constructor MkPDef qty : PQty - name : Name - type : PTerm + name : PName + type : Maybe PTerm term : PTerm %name PDefinition def %runElab derive "PDefinition" [Eq, Ord, Show] +mutual + public export + record PNamespace where + constructor MkPNamespace + name : Mods + decls : List PDecl + %name PNamespace ns + + public export + data PDecl = + PDef PDefinition + | PNs PNamespace + %name PDecl decl +%runElab deriveMutual ["PNamespace", "PDecl"] [Eq, Ord, Show] + +public export +data PTopLevel = PD PDecl | PLoad String +%name PTopLevel t +%runElab derive "PTopLevel" [Eq, Ord, Show] + export -toPDimWith : Context' BaseName d -> Dim d -> PDim +toPDimWith : Context' PBaseName d -> Dim d -> PDim toPDimWith ds (K e) = K e toPDimWith ds (B i) = V $ ds !!! i @@ -90,27 +108,30 @@ toPDim = toPDimWith [<] mutual namespace Term export - toPTermWith : Context' BaseName d -> Context' BaseName n -> + toPTermWith : Context' PBaseName d -> Context' PBaseName n -> Term Three d n -> PTerm toPTermWith ds ns t = let Element t _ = pushSubsts t in toPTermWith' ds ns t private - toPTermWith' : Context' BaseName d -> Context' BaseName n -> + toPTermWith' : Context' PBaseName d -> Context' PBaseName n -> (t : Term Three d n) -> (0 _ : NotClo t) => PTerm toPTermWith' ds ns s = case s of TYPE l => TYPE l Pi qty arg (S [x] res) => - Pi qty (Just x) (toPTermWith ds ns arg) - (toPTermWith ds (ns :< x) res.term) + Pi qty (Just $ show x) + (toPTermWith ds ns arg) + (toPTermWith ds (ns :< baseStr x) res.term) Lam (S [x] body) => - Lam (Just x) $ toPTermWith ds (ns :< x) body.term + Lam (Just $ show x) $ + toPTermWith ds (ns :< baseStr x) body.term Sig fst (S [x] snd) => - Sig (Just x) (toPTermWith ds ns fst) - (toPTermWith ds (ns :< x) snd.term) + Sig (Just $ show x) + (toPTermWith ds ns fst) + (toPTermWith ds (ns :< baseStr x) snd.term) Pair fst snd => Pair (toPTermWith ds ns fst) (toPTermWith ds ns snd) Enum cases => @@ -118,40 +139,40 @@ mutual Tag tag => Tag tag Eq (S [i] ty) l r => - Eq (Just i, toPTermWith (ds :< i) ns ty.term) + Eq (Just $ show i, toPTermWith (ds :< baseStr i) ns ty.term) (toPTermWith ds ns l) (toPTermWith ds ns r) DLam (S [i] body) => - DLam (Just i) $ toPTermWith (ds :< i) ns body.term + DLam (Just $ show i) $ toPTermWith (ds :< baseStr i) ns body.term E e => toPTermWith ds ns e namespace Elim export - toPTermWith : Context' BaseName d -> Context' BaseName n -> + toPTermWith : Context' PBaseName d -> Context' PBaseName n -> Elim Three d n -> PTerm toPTermWith ds ns e = let Element e _ = pushSubsts e in toPTermWith' ds ns e private - toPTermWith' : Context' BaseName d -> Context' BaseName n -> + toPTermWith' : Context' PBaseName d -> Context' PBaseName n -> (e : Elim Three d n) -> (0 _ : NotClo e) => PTerm toPTermWith' ds ns e = case e of F x => - V x + V $ toPName x B i => - V $ unq $ ns !!! i + V $ MakePName [<] $ ns !!! i fun :@ arg => toPTermWith ds ns fun :@ toPTermWith ds ns arg CasePair qty pair (S [r] ret) (S [x, y] body) => Case qty (toPTermWith ds ns pair) - (Just r, toPTermWith ds (ns :< r) ret.term) - (CasePair (Just x, Just y) $ - toPTermWith ds (ns :< x :< y) body.term) + (Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term) + (CasePair (Just $ show x, Just $ show y) $ + toPTermWith ds (ns :< baseStr x :< baseStr y) body.term) CaseEnum qty tag (S [r] ret) arms => Case qty (toPTermWith ds ns tag) - (Just r, toPTermWith ds (ns :< r) ret.term) + (Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term) (CaseEnum $ mapSnd (toPTermWith ds ns) <$> SortedMap.toList arms) fun :% arg => toPTermWith ds ns fun :% toPDimWith ds arg @@ -167,172 +188,3 @@ namespace Elim export toPTerm : Elim Three 0 0 -> PTerm toPTerm = toPTermWith [<] [<] - - - -public export -data FromPTermError = - AnnotationNeeded PTerm - | DuplicatesInEnum (List TagVal) - | DimNotInScope Name - | QtyNotGlobal PQty - | DimNameInTerm Name - -public export -FromPTerm : (Type -> Type) -> Type -FromPTerm m = MonadError FromPTermError m - -private -extendVect : Telescope' a from to -> Vect n a -> Telescope' a from (n + to) -extendVect tel [] = tel -extendVect tel (x :: xs) {n = S n} = - rewrite plusSuccRightSucc n to in - extendVect (tel :< x) xs - - -parameters {auto _ : FromPTerm m} (b : Var n -> m a) (f : Name -> m a) - (xs : Context' BName n) - private - fromBaseName : BaseName -> m a - fromBaseName x = maybe (f $ unq x) b $ Context.find (== Just x) xs - - fromName : Name -> m a - fromName x = if null x.mods then fromBaseName x.base else f x - -export -fromPDimWith : FromPTerm m => - Context' BName d -> PDim -> m (Dim d) -fromPDimWith ds (K e) = pure $ K e -fromPDimWith ds (V i) = fromBaseName (pure . B) (throwError . DimNotInScope) ds i - -private -avoidDim : FromPTerm m => Context' BName d -> Name -> m (Term q d n) -avoidDim ds x = - fromName (const $ throwError $ DimNameInTerm x) (pure . FT) ds x - - -mutual - export - fromPTermWith : FromPTerm m => - Context' BName d -> Context' BName n -> - PTerm -> m (Term Three d n) - fromPTermWith ds ns t0 = case t0 of - TYPE k => - pure $ TYPE $ k - - Pi pi x s t => - Pi pi <$> fromPTermWith ds ns s - <*> fromPTermTScope ds ns [x] t - - Lam x s => - Lam <$> fromPTermTScope ds ns [x] s - - s :@ t => - map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t - - Sig x s t => - Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [x] t - - Pair s t => - Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t - - Case pi pair (r, ret) (CasePair (x, y) body) => - map E $ Base.CasePair pi - <$> fromPTermElim ds ns pair - <*> fromPTermTScope ds ns [r] ret - <*> fromPTermTScope ds ns [x, y] body - - Case pi tag (r, ret) (CaseEnum arms) => - map E $ Base.CaseEnum pi - <$> fromPTermElim ds ns tag - <*> fromPTermTScope ds ns [r] ret - <*> assert_total fromPTermEnumArms ds ns arms - - Enum strs => - let set = SortedSet.fromList strs in - if length strs == length (SortedSet.toList set) then - pure $ Enum set - else - throwError $ DuplicatesInEnum strs - - Tag str => pure $ Tag str - - Eq (i, ty) s t => - Eq <$> fromPTermDScope ds ns [i] ty - <*> fromPTermWith ds ns s - <*> fromPTermWith ds ns t - - DLam i s => - DLam <$> fromPTermDScope ds ns [i] s - - s :% p => - map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p - - V x => - fromName (pure . E . B) (avoidDim ds) ns x - - s :# a => - map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a - - private - fromPTermEnumArms : FromPTerm m => - Context' BName d -> Context' BName n -> - List (TagVal, PTerm) -> m (CaseEnumArms Three d n) - fromPTermEnumArms ds ns = - map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns) - - private - fromPTermElim : FromPTerm m => - Context' BName d -> Context' BName n -> - PTerm -> m (Elim Three d n) - fromPTermElim ds ns e = - case !(fromPTermWith ds ns e) of - E e => pure e - _ => throwError $ AnnotationNeeded e - - -- [todo] use SN if the var is named but still unused - private - fromPTermTScope : {s : Nat} -> FromPTerm m => - Context' BName d -> Context' BName n -> - Vect s BName -> - PTerm -> m (ScopeTermN s Three d n) - fromPTermTScope ds ns xs t = - if all isNothing xs then - SN <$> fromPTermWith ds ns t - else - SY (map (fromMaybe "_") xs) <$> fromPTermWith ds (extendVect ns xs) t - - private - fromPTermDScope : {s : Nat} -> FromPTerm m => - Context' BName d -> Context' BName n -> - Vect s BName -> - PTerm -> m (DScopeTermN s Three d n) - fromPTermDScope ds ns xs t = - if all isNothing xs then - SN <$> fromPTermWith ds ns t - else - SY (map (fromMaybe "_") xs) <$> fromPTermWith (extendVect ds xs) ns t - - -export %inline -fromPTerm : FromPTerm m => PTerm -> m (Term Three 0 0) -fromPTerm = fromPTermWith [<] [<] - - -export -globalPQty : FromPTerm m => (q : PQty) -> m (IsGlobal q) -globalPQty pi = case isGlobal pi of - Yes y => pure y - No n => throwError $ QtyNotGlobal pi - - --- [todo] extend substitutions so they can do this injection. that's the sort of --- thing they are for. -export -fromPDefinition : FromPTerm m => PDefinition -> m (Name, Definition Three) -fromPDefinition (MkPDef {name, qty, type, term}) = - pure (name, MkDef' { - qty, qtyGlobal = !(globalPQty qty), - type = T $ inject !(fromPTerm type), - term = Just $ T $ inject !(fromPTerm term) - }) diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 2134fa4..c5e851b 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -33,6 +33,8 @@ modules = Quox.Name, Quox.Typing, Quox.Typechecker, - Quox.Lexer, + Quox.Parser.Lexer, Quox.Parser.Syntax, + Quox.Parser.Parser, + Quox.Parser.FromParser, Quox.Parser diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr index 01d62b0..3991f7c 100644 --- a/tests/Tests/FromPTerm.idr +++ b/tests/Tests/FromPTerm.idr @@ -3,30 +3,29 @@ module Tests.FromPTerm import Quox.Parser.Syntax import Quox.Parser import TermImpls +import Tests.Parser as TParser import TAP import Derive.Prelude %language ElabReflection +%hide TParser.Failure +%hide TParser.ExpectedFail + public export data Failure = - LexError Lexer.Error - | ParseError (List1 (ParsingError Token)) - | FromPTermError FromPTermError + ParseError (Parser.Error) + | FromParserError FromParserError | WrongResult String | ExpectedFail String -%runElab derive "Syntax.FromPTermError" [Show] +%runElab derive "FromParser.FromParserError" [Show] 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 (FromPTermError err) = - [("type", "FromPTermError"), + toInfo (ParseError err) = toInfo err + toInfo (FromParserError err) = + [("type", "FromParserError"), ("got", show err)] toInfo (WrongResult got) = [("type", "WrongResult"), ("got", got)] @@ -35,14 +34,13 @@ ToInfo Failure where parameters {c : Bool} {auto _ : Show b} - (grm : Grammar c a) (fromP : a -> Either FromPTermError b) + (grm : Grammar c a) (fromP : a -> Either FromParserError b) (inp : String) parameters {default (ltrim inp) label : String} parsesWith : (b -> Bool) -> Test parsesWith p = test label $ do - toks <- mapFst LexError $ lex inp - (pres, _) <- mapFst ParseError $ parse (grm <* eof) toks - res <- mapFst FromPTermError $ fromP pres + pres <- mapFst ParseError $ lexParseWith grm inp + res <- mapFst FromParserError $ fromP pres unless (p res) $ Left $ WrongResult $ show res parses : Test @@ -54,8 +52,7 @@ parameters {c : Bool} {auto _ : Show b} parameters {default "\{ltrim inp} # fails" label : String} parseFails : Test parseFails = test label $ do - toks <- mapFst LexError $ lex inp - (pres, _) <- mapFst ParseError $ parse (grm <* eof) toks + pres <- mapFst ParseError $ lexParseWith grm inp either (const $ Right ()) (Left . ExpectedFail . show) $ fromP pres diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index f1c71d3..0aac535 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -7,18 +7,22 @@ import TAP public export data Failure = - LexError Lexer.Error - | ParseError (List1 (ParsingError Token)) + ParseError Parser.Error | WrongResult String | ExpectedFail String export -ToInfo Failure where +ToInfo Parser.Error where toInfo (LexError err) = [("type", "LexError"), ("info", show err)] toInfo (ParseError errs) = ("type", "ParseError") :: map (bimap show show) ([1 .. length errs] `zip` toList errs) + +export +ToInfo Failure where + toInfo (ParseError err) = + toInfo err toInfo (WrongResult got) = [("type", "WrongResult"), ("got", got)] toInfo (ExpectedFail got) = @@ -30,8 +34,7 @@ parameters {c : Bool} {auto _ : Show a} (grm : Grammar c a) 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 + res <- mapFst ParseError $ lexParseWith grm inp unless (p res) $ Left $ WrongResult $ show res parses : Test @@ -43,9 +46,8 @@ parameters {c : Bool} {auto _ : Show a} (grm : Grammar c a) 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 + either (const $ Right ()) (Left . ExpectedFail . show) $ + lexParseWith grm inp export @@ -59,9 +61,9 @@ tests = "parser" :- [ "names" :- [ parsesAs name "x" - (MakeName [<] $ UN "x"), + (MakePName [<] "x"), parsesAs name "Data.String.length" - (MakeName [< "Data", "String"] $ UN "length"), + (MakePName [< "Data", "String"] "length"), parseFails name "_" ], @@ -119,7 +121,7 @@ tests = "parser" :- [ "applications" :- [ parsesAs term "f" (V "f"), - parsesAs term "f.x.y" (V $ MakeName [< "f", "x"] $ UN "y"), + parsesAs term "f.x.y" (V $ MakePName [< "f", "x"] "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"), @@ -240,22 +242,36 @@ tests = "parser" :- [ ], "definitions" :- [ - parsesAs definition "defω x : (_: {a}) × {b} ≔ ('a, 'b);" $ - MkPDef Any "x" (Sig Nothing (Enum ["a"]) (Enum ["b"])) + parsesAs definition "defω x : (_: {a}) × {b} ≔ ('a, 'b)" $ + MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"])) (Pair (Tag "a") (Tag "b")), - parsesAs definition "def# x : (_: {a}) ** {b} ≔ ('a, 'b);" $ - MkPDef Any "x" (Sig Nothing (Enum ["a"]) (Enum ["b"])) + parsesAs definition "defω x : (_: {a}) × {b} ≔ ('a, 'b)" $ + MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"])) (Pair (Tag "a") (Tag "b")), - parsesAs definition "def ω·x : (_: {a}) × {b} ≔ ('a, 'b);" $ - MkPDef Any "x" (Sig Nothing (Enum ["a"]) (Enum ["b"])) + parsesAs definition "def# x : (_: {a}) ** {b} ≔ ('a, 'b)" $ + MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"])) (Pair (Tag "a") (Tag "b")), - parsesAs definition "def x : (_: {a}) × {b} ≔ ('a, 'b);" $ - MkPDef Any "x" (Sig Nothing (Enum ["a"]) (Enum ["b"])) + parsesAs definition "def ω·x : (_: {a}) × {b} ≔ ('a, 'b)" $ + MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"])) (Pair (Tag "a") (Tag "b")), - parsesAs definition "def0 A : ★₀ ≔ {a, b, c};" $ - MkPDef Zero "A" (TYPE 0) (Enum ["a", "b", "c"]), + parsesAs definition "def x : (_: {a}) × {b} ≔ ('a, 'b)" $ + MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"])) + (Pair (Tag "a") (Tag "b")), + parsesAs definition "def0 A : ★₀ ≔ {a, b, c}" $ + MkPDef Zero "A" (Just $ TYPE 0) (Enum ["a", "b", "c"]) + ], + + "top level" :- [ parsesAs input "def0 A : ★₀ ≔ {}; def0 B : ★₁ ≔ A;" $ - [MkPDef Zero "A" (TYPE 0) (Enum []), - MkPDef Zero "B" (TYPE 1) (V "A")] + [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []), + PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")], + parsesAs input "def0 A : ★₀ ≔ {} def0 B : ★₁ ≔ A" $ + [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []), + PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")], + parsesAs input "def0 A : ★₀ ≔ {};;; def0 B : ★₁ ≔ A" $ + [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []), + PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")], + parsesAs input "" [] {label = "[empty input]"}, + parsesAs input ";;;;;;;;;;;;;;;;;;;;;;;;;;" [] ] ]