From 7e079a966810b07efa51a9e279df003a8920ab16 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 26 Apr 2023 02:47:42 +0200 Subject: [PATCH] add file locations to Parser.Syntax they're immediately thrown away currently. but one step at a time --- lib/Quox/Loc.idr | 63 +++++ lib/Quox/Parser/FromParser.idr | 197 ++++++------- lib/Quox/Parser/Parser.idr | 460 +++++++++++++++++------------- lib/Quox/Parser/Syntax.idr | 256 ++++++++--------- lib/quox-lib.ipkg | 1 + tests/Tests/FromPTerm.idr | 9 +- tests/Tests/Parser.idr | 503 ++++++++++++++++++--------------- 7 files changed, 822 insertions(+), 667 deletions(-) create mode 100644 lib/Quox/Loc.idr diff --git a/lib/Quox/Loc.idr b/lib/Quox/Loc.idr new file mode 100644 index 0000000..4b65199 --- /dev/null +++ b/lib/Quox/Loc.idr @@ -0,0 +1,63 @@ +||| file locations +module Quox.Loc + +import Text.Bounded +import Derive.Prelude + +%default total +%language ElabReflection + +public export +FileName : Type +FileName = String + +public export +record Loc' where + constructor L + fname : FileName + startLine, startCol, endLine, endCol : Int +%name Loc' loc +%runElab derive "Loc'" [Eq, Ord, Show] + +public export +Loc : Type +Loc = Maybe Loc' + +export +makeLoc : FileName -> Bounds -> Loc +makeLoc fname (MkBounds {startLine, startCol, endLine, endCol}) = + Just $ L {fname, startLine, startCol, endLine, endCol} + +export +onlyStart : Loc -> Loc +onlyStart Nothing = Nothing +onlyStart (Just (L fname sl sc _ _)) = Just $ L fname sl sc sl sc + +export +onlyEnd : Loc -> Loc +onlyEnd Nothing = Nothing +onlyEnd (Just (L fname _ _ el ec)) = Just $ L fname el ec el ec + + +export +extend : Loc -> Bounds -> Loc +extend Nothing _ = Nothing +extend (Just (L fname sl1 sc1 el1 ec1)) (MkBounds sl2 sc2 el2 ec2) = + let (sl, sc) = (sl1, sc1) `min` (sl2, sc2) + (el, ec) = (el1, ec1) `max` (el2, ec2) + in + Just $ L fname sl sc el ec + +export +extend' : Loc -> Maybe Bounds -> Loc +extend' l b = maybe l (extend l) b + + +public export +interface Located a where (.loc) : a -> Loc + +export +(.bounds) : Loc -> Maybe Bounds +(Just (L {fname, startLine, startCol, endLine, endCol})).bounds = + Just $ MkBounds {startLine, startCol, endLine, endCol} +(Nothing).bounds = Nothing diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index 91b3dfb..47d97da 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -23,15 +23,15 @@ import public Quox.Parser.FromParser.Error as Quox.Parser.FromParser public export -0 NDefinition : Type +NDefinition : Type NDefinition = (Name, Definition) public export -0 IncludePath : Type +IncludePath : Type IncludePath = List String public export -0 SeenFiles : Type +SeenFiles : Type SeenFiles = SortedSet String @@ -39,26 +39,29 @@ public export data StateTag = NS | SEEN public export -0 FromParserPure : List (Type -> Type) +FromParserPure : List (Type -> Type) FromParserPure = [Except Error, StateL DEFS Definitions, StateL NS Mods] public export -0 FromParserEff : List (Type -> Type) +FromParserEff : List (Type -> Type) FromParserEff = [Except Error, StateL DEFS Definitions, StateL NS Mods, Reader IncludePath, StateL SEEN SeenFiles, IO] public export -0 FromParser : Type -> Type +FromParser : Type -> Type FromParser = Eff FromParserEff +-- [todo] put the locs in the core ast, obv + parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a) - (xs : Context' BName n) + (xs : Context' PatVar n) private fromBaseName : PBaseName -> m a - fromBaseName x = maybe (f $ MakePName [<] x) b $ Context.find (== Just x) xs + fromBaseName x = maybe (f $ MakePName [<] x) b $ + Context.find (\y => y.name == Just x) xs private fromName : PName -> m a @@ -66,14 +69,14 @@ parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a) export fromPDimWith : Has (Except Error) fs => - Context' BName d -> PDim -> Eff fs (Dim d) -fromPDimWith ds (K e) = pure $ K e -fromPDimWith ds (V i) = + Context' PatVar d -> PDim -> Eff fs (Dim d) +fromPDimWith ds (K e _) = pure $ K e +fromPDimWith ds (V i _) = fromBaseName (pure . B) (const $ throw $ DimNotInScope i) ds i private avoidDim : Has (Except Error) fs => - Context' BName d -> PName -> Eff fs Name + Context' PatVar d -> PName -> Eff fs Name avoidDim ds x = fromName (const $ throw $ DimNameInTerm x.base) (pure . fromPName) ds x @@ -88,97 +91,112 @@ resolveName ns x = | _ => throw $ TermNotInScope x resolveName ns x +export +fromPatVar : PatVar -> BaseName +fromPatVar (Unused _) = Unused +fromPatVar (PV x _) = UN x + +export +fromPQty : PQty -> Qty +fromPQty (PQ q _) = q + +export +fromPTagVal : PTagVal -> TagVal +fromPTagVal (PT t _) = t + + mutual export - fromPTermWith : Context' BName d -> Context' BName n -> + fromPTermWith : Context' PatVar d -> Context' PatVar n -> PTerm -> Eff FromParserPure (Term d n) fromPTermWith ds ns t0 = case t0 of - TYPE k => - pure $ TYPE $ k + TYPE k _ => + pure $ TYPE k - Pi pi x s t => - Pi pi <$> fromPTermWith ds ns s - <*> fromPTermTScope ds ns [< x] t + Pi pi x s t _ => + Pi (fromPQty pi) + <$> fromPTermWith ds ns s + <*> fromPTermTScope ds ns [< x] t - Lam x s => + Lam x s _ => Lam <$> fromPTermTScope ds ns [< x] s - s :@ t => + App s t _ => map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t - Sig x s t => + Sig x s t _ => Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [< x] t - Pair s t => + Pair s t _ => Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t - Case pi pair (r, ret) (CasePair (x, y) body) => - map E $ CasePair pi + Case pi pair (r, ret) (CasePair (x, y) body _) _ => + map E $ CasePair (fromPQty 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 $ CaseEnum pi + Case pi tag (r, ret) (CaseEnum arms _) _ => + map E $ CaseEnum (fromPQty pi) <$> fromPTermElim ds ns tag <*> fromPTermTScope ds ns [< r] ret <*> assert_total fromPTermEnumArms ds ns arms - Nat => pure Nat - Zero => pure Zero - Succ n => [|Succ $ fromPTermWith ds ns n|] + Nat _ => pure Nat + Zero _ => pure Zero + Succ n _ => [|Succ $ fromPTermWith ds ns n|] - Case pi nat (r, ret) (CaseNat zer (s, pi', ih, suc)) => - map E $ CaseNat pi pi' + Case pi nat (r, ret) (CaseNat zer (s, pi', ih, suc) _) _ => + map E $ CaseNat (fromPQty pi) (fromPQty pi') <$> fromPTermElim ds ns nat <*> fromPTermTScope ds ns [< r] ret <*> fromPTermWith ds ns zer <*> fromPTermTScope ds ns [< s, ih] suc - Enum strs => + Enum strs _ => let set = SortedSet.fromList strs in if length strs == length (SortedSet.toList set) then pure $ Enum set else throw $ DuplicatesInEnum strs - Tag str => pure $ Tag str + Tag str _ => pure $ Tag str - Eq (i, ty) s t => + Eq (i, ty) s t _ => Eq <$> fromPTermDScope ds ns [< i] ty <*> fromPTermWith ds ns s <*> fromPTermWith ds ns t - DLam i s => + DLam i s _ => DLam <$> fromPTermDScope ds ns [< i] s - BOX q ty => BOX q <$> fromPTermWith ds ns ty + DApp s p _ => + map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p - Box val => Box <$> fromPTermWith ds ns val + BOX q ty _ => BOX (fromPQty q) <$> fromPTermWith ds ns ty - Case pi box (r, ret) (CaseBox b body) => - map E $ CaseBox pi + Box val _ => Box <$> fromPTermWith ds ns val + + Case pi box (r, ret) (CaseBox b body _) _ => + map E $ CaseBox (fromPQty pi) <$> fromPTermElim ds ns box <*> fromPTermTScope ds ns [< r] ret <*> fromPTermTScope ds ns [< b] body - s :% p => - map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p - - V x => + V x _ => fromName (pure . E . B) (resolveName !(getAt NS) <=< avoidDim ds) ns x - s :# a => + Ann s a _ => map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a - Coe (i, ty) p q val => + Coe (i, ty) p q val _ => map E $ Coe <$> fromPTermDScope ds ns [< i] ty <*> fromPDimWith ds p <*> fromPDimWith ds q <*> fromPTermWith ds ns val - Comp (i, ty) p q val r (j0, val0) (j1, val1) => + Comp (i, ty) p q val r (j0, val0) (j1, val1) _ => map E $ CompH' <$> fromPTermDScope ds ns [< i] ty <*> fromPDimWith ds p @@ -189,46 +207,42 @@ mutual <*> fromPTermDScope ds ns [< j1] val1 private - fromPTermEnumArms : Context' BName d -> Context' BName n -> - List (TagVal, PTerm) -> + fromPTermEnumArms : Context' PatVar d -> Context' PatVar n -> + List (PTagVal, PTerm) -> Eff FromParserPure (CaseEnumArms d n) fromPTermEnumArms ds ns = - map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns) + map SortedMap.fromList . + traverse (bitraverse (pure . fromPTagVal) (fromPTermWith ds ns)) private - fromPTermElim : Context' BName d -> Context' BName n -> + fromPTermElim : Context' PatVar d -> Context' PatVar n -> PTerm -> Eff FromParserPure (Elim d n) fromPTermElim ds ns e = case !(fromPTermWith ds ns e) of E e => pure e - t => let ctx = MkNameContexts (map name ds) (map name ns) in + t => let ctx = MkNameContexts (map fromPatVar ds) (map fromPatVar ns) in throw $ AnnotationNeeded ctx t - where - name : BName -> BaseName - name = maybe Unused UN -- [todo] use SN if the var is named but still unused private - fromPTermTScope : {s : Nat} -> Context' BName d -> Context' BName n -> - SnocVect s BName -> PTerm -> + fromPTermTScope : {s : Nat} -> Context' PatVar d -> Context' PatVar n -> + SnocVect s PatVar -> PTerm -> Eff FromParserPure (ScopeTermN s d n) fromPTermTScope ds ns xs t = - if all isNothing xs then + if all isUnused xs then SN <$> fromPTermWith ds ns t else - ST (fromSnocVect $ map (maybe Unused UN) xs) - <$> fromPTermWith ds (ns ++ xs) t + ST (fromSnocVect $ map fromPatVar xs) <$> fromPTermWith ds (ns ++ xs) t private - fromPTermDScope : {s : Nat} -> Context' BName d -> Context' BName n -> - SnocVect s BName -> PTerm -> + fromPTermDScope : {s : Nat} -> Context' PatVar d -> Context' PatVar n -> + SnocVect s PatVar -> PTerm -> Eff FromParserPure (DScopeTermN s d n) fromPTermDScope ds ns xs t = - if all isNothing xs then + if all isUnused xs then SN <$> fromPTermWith ds ns t else - DST (fromSnocVect $ map (maybe Unused UN) xs) - <$> fromPTermWith (ds ++ xs) ns t + DST (fromSnocVect $ map fromPatVar xs) <$> fromPTermWith (ds ++ xs) ns t export %inline @@ -237,30 +251,26 @@ fromPTerm = fromPTermWith [<] [<] export -globalPQty : Has (Except Error) fs => - (q : Qty) -> Eff fs (So $ isGlobal q) +globalPQty : (q : Qty) -> Eff [Except Error] (So $ isGlobal q) globalPQty pi = case choose $ isGlobal pi of Left y => pure y Right _ => throw $ QtyNotGlobal pi export -fromPBaseNameNS : Has (StateL NS Mods) fs => PBaseName -> Eff fs Name +fromPBaseNameNS : PBaseName -> Eff [StateL NS Mods] Name fromPBaseNameNS name = pure $ addMods !(getAt NS) $ fromPBaseName name private -injTC : (Has (StateL DEFS Definitions) fs, Has (Except Error) fs) => - TC a -> Eff fs a +injTC : TC a -> Eff FromParserPure a injTC act = rethrow $ mapFst WrapTypeError $ runTC !(getAt DEFS) act export covering -fromPDef : (Has (StateL DEFS Definitions) fs, - Has (StateL NS Mods) fs, - Has (Except Error) fs) => - PDefinition -> Eff fs NDefinition -fromPDef (MkPDef qty pname ptype pterm) = do - name <- fromPBaseNameNS pname - qtyGlobal <- globalPQty qty +fromPDef : PDefinition -> Eff FromParserPure NDefinition +fromPDef (MkPDef qty pname ptype pterm _) = do + name <- lift $ fromPBaseNameNS pname + let qty = fromPQty qty + qtyGlobal <- lift $ globalPQty qty let gqty = Element qty qtyGlobal let sqty = globalToSubj gqty type <- lift $ traverse fromPTerm ptype @@ -280,21 +290,18 @@ fromPDef (MkPDef qty pname ptype pterm) = do pure (name, def) export covering -fromPDecl : (Has (StateL DEFS Definitions) fs, - Has (StateL NS Mods) fs, - Has (Except Error) fs) => - PDecl -> Eff fs (List NDefinition) +fromPDecl : PDecl -> Eff FromParserPure (List NDefinition) fromPDecl (PDef def) = singleton <$> fromPDef def fromPDecl (PNs ns) = localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls +public export +LoadFile : List (Type -> Type) +LoadFile = [IO, StateL SEEN SeenFiles, Reader IncludePath, Except Error] + export covering -loadFile : (Has IO fs, - Has (StateL SEEN SeenFiles) fs, - Has (Reader IncludePath) fs, - Has (Except Error) fs) => - String -> Eff fs (Maybe String) +loadFile : String -> Eff LoadFile (Maybe String) loadFile file = if contains file !(getAt SEEN) then pure Nothing @@ -305,27 +312,21 @@ loadFile file = Right res => modifyAt SEEN (insert file) $> Just res Left err => throw $ LoadError ifile err -parameters {auto _ : (Has IO fs, - Has (StateL SEEN SeenFiles) fs, - Has (Reader IncludePath) fs, - Has (Except Error) fs, - Has (StateL DEFS Definitions) fs, - Has (StateL NS Mods) fs)} - mutual +mutual export covering - loadProcessFile : String -> Eff fs (List NDefinition) + loadProcessFile : String -> FromParser (List NDefinition) loadProcessFile file = - case !(loadFile file) of + case !(lift $ loadFile file) of Just inp => do - tl <- either (throw . WrapParseError file) pure $ lexParseInput inp + tl <- either (throw . WrapParseError file) pure $ lexParseInput file inp concat <$> traverse fromPTopLevel tl Nothing => pure [] ||| populates the `defs` field of the state export covering - fromPTopLevel : PTopLevel -> Eff fs (List NDefinition) - fromPTopLevel (PD decl) = fromPDecl decl - fromPTopLevel (PLoad file) = loadProcessFile file + fromPTopLevel : PTopLevel -> FromParser (List NDefinition) + fromPTopLevel (PD decl) = lift $ fromPDecl decl + fromPTopLevel (PLoad file _) = loadProcessFile file export fromParserPure : Definitions -> diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index 952fd76..b65c9d9 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -26,12 +26,27 @@ data Error = %hide Lexer.Error %runElab derive "Error" [Show] + 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 +withLoc : {c : Bool} -> FileName -> (Grammar c (Loc -> a)) -> Grammar c a +withLoc fname act = bounds act <&> \res => + if res.isIrrelevant then res.val Nothing + else res.val $ makeLoc fname res.bounds + +export +defLoc : FileName -> (Loc -> a) -> Grammar False a +defLoc fname f = position <&> f . makeLoc fname + +export +unused : FileName -> Grammar False PatVar +unused fname = defLoc fname Unused + ||| reserved token, like punctuation or keywords etc export @@ -114,26 +129,33 @@ dimConst = terminalMatchN "dimension constant" ||| quantity (0, 1, or ω) export -qty : Grammar True Qty -qty = terminalMatchN "quantity" +qtyVal : Grammar True Qty +qtyVal = terminalMatchN "quantity" [(`(Nat 0), `(Zero)), (`(Nat 1), `(One)), (`(Reserved "ω"), `(Any))] +||| quantity (0, 1, or ω) +export +qty : FileName -> Grammar True PQty +qty fname = withLoc fname [|PQ qtyVal|] + + ||| pattern var (unqualified name or _) export -patVar : Grammar True BName -patVar = [|Just baseName|] <|> Nothing <$ res "_" +patVar : FileName -> Grammar True PatVar +patVar fname = withLoc fname $ + [|PV baseName|] <|> Unused <$ res "_" ||| dimension (without `@` prefix) export -dim : Grammar True PDim -dim = [|K dimConst|] <|> [|V baseName|] +dim : FileName -> Grammar True PDim +dim fname = withLoc fname $ [|K dimConst|] <|> [|V baseName|] ||| dimension argument (with @) export -dimArg : Grammar True PDim -dimArg = resC "@" *> mustWork dim +dimArg : FileName -> Grammar True PDim +dimArg fname = do resC "@"; mustWork $ dim fname delim : (o, c : String) -> (0 _ : IsReserved o) => (0 _ : IsReserved c) => @@ -168,313 +190,369 @@ enumType = delimSep "{" "}" "," bareTag ||| e.g. `case` or `case 1.` export -caseIntro : Grammar True Qty -caseIntro = - Zero <$ res "case0" - <|> One <$ res "case1" - <|> Any <$ res "caseω" - <|> delim "case" "." qty +caseIntro : FileName -> Grammar True PQty +caseIntro fname = + withLoc fname (PQ Zero <$ res "case0") + <|> withLoc fname (PQ One <$ res "case1") + <|> withLoc fname (PQ Any <$ res "caseω") + <|> delim "case" "." (qty fname) export -qtyPatVar : Grammar True (Qty, BName) -qtyPatVar = [|(,) qty (needRes "." *> patVar)|] +qtyPatVar : FileName -> Grammar True (PQty, PatVar) +qtyPatVar fname = [|(,) (qty fname) (needRes "." *> patVar fname)|] +export +ptag : FileName -> Grammar True PTagVal +ptag fname = withLoc fname $ [|PT tag|] + public export data PCasePat = - PPair BName BName - | PTag TagVal - | PZero - | PSucc BName Qty BName - | PBox BName + PPair PatVar PatVar Loc + | PTag PTagVal Loc + | PZero Loc + | PSucc PatVar PQty PatVar Loc + | PBox PatVar Loc %runElab derive "PCasePat" [Eq, Ord, Show] +export +Located PCasePat where + (PPair _ _ loc).loc = loc + (PTag _ loc).loc = loc + (PZero loc).loc = loc + (PSucc _ _ _ loc).loc = loc + (PBox _ loc).loc = loc + ||| either `zero` or `0` export zeroPat : Grammar True () zeroPat = resC "zero" <|> terminal "expected '0'" (guard . (== Nat 0)) export -casePat : Grammar True PCasePat -casePat = - delim "(" ")" [|PPair patVar (needRes "," *> patVar)|] - <|> [|PTag tag|] +casePat : FileName -> Grammar True PCasePat +casePat fname = withLoc fname $ + delim "(" ")" [|PPair (patVar fname) (needRes "," *> patVar fname)|] + <|> [|PTag (ptag fname)|] <|> PZero <$ zeroPat - <|> do p <- resC "succ" *> patVar - ih <- option (Zero, Nothing) $ resC "," *> qtyPatVar + <|> do p <- resC "succ" *> patVar fname + ih <- resC "," *> qtyPatVar fname + <|> [|(,) (defLoc fname $ PQ Zero) (unused fname)|] pure $ PSucc p (fst ih) (snd ih) - <|> delim "[" "]" [|PBox patVar|] + <|> delim "[" "]" [|PBox (patVar fname)|] <|> fatalError "invalid pattern" +export covering +term : FileName -> Grammar True PTerm +-- defined after all the subterm parsers export covering -term : Grammar True PTerm - -export covering -typeLine : Grammar True (BName, PTerm) -typeLine = do +typeLine : FileName -> Grammar True (PatVar, PTerm) +typeLine fname = do resC "[" mustWork $ do - i <- option Nothing $ patVar <* resC "⇒" - t <- term <* needRes "]" + i <- patVar fname <* resC "⇒" <|> unused fname + t <- term fname <* needRes "]" pure (i, t) ||| box term `[t]` or type `[π.A]` export covering -boxTerm : Grammar True PTerm -boxTerm = do +boxTerm : FileName -> Grammar True PTerm +boxTerm fname = withLoc fname $ do res "["; commit - q <- optional $ qty <* res "." - t <- mustWork $ term <* needRes "]" + q <- optional $ qty fname <* res "." + t <- mustWork $ term fname <* needRes "]" pure $ maybe (Box t) (\q => BOX q t) q ||| tuple term like `(a, b)`, or parenthesised single term. ||| allows terminating comma. more than two elements are nested on the right: ||| `(a, b, c, d) = (a, (b, (c, d)))`. export covering -tupleTerm : Grammar True PTerm -tupleTerm = foldr1 Pair <$> delimSep1 "(" ")" "," term +tupleTerm : FileName -> Grammar True PTerm +tupleTerm fname = withLoc fname $ do + terms <- delimSep1 "(" ")" "," $ term fname + pure $ \loc => foldr1 (\s, t => Pair s t loc) terms ||| argument/atomic term: single-token terms, or those with delimiters e.g. ||| `[t]` export covering -termArg : Grammar True PTerm -termArg = [|TYPE universe1|] - <|> [|Enum enumType|] - <|> [|Tag tag|] - <|> boxTerm - <|> Nat <$ res "ℕ" - <|> Zero <$ res "zero" - <|> [|fromNat nat|] - <|> [|V qname|] - <|> tupleTerm +termArg : FileName -> Grammar True PTerm +termArg fname = withLoc fname $ + [|TYPE universe1|] + <|> [|Enum enumType|] + <|> [|Tag tag|] + <|> const <$> boxTerm fname + <|> Nat <$ res "ℕ" + <|> Zero <$ res "zero" + <|> [|fromNat nat|] + <|> [|V qname|] + <|> const <$> tupleTerm fname export covering -coeTerm : Grammar True PTerm -coeTerm = resC "coe" *> mustWork [|Coe typeLine dimArg dimArg termArg|] +coeTerm : FileName -> Grammar True PTerm +coeTerm fname = withLoc fname $ do + resC "coe" + mustWork [|Coe (typeLine fname) (dimArg fname) (dimArg fname) + (termArg fname)|] + +public export +CompBranch : Type +CompBranch = (DimConst, PatVar, PTerm) export covering -compBranch : Grammar True (DimConst, BName, PTerm) -compBranch = [|(,,) dimConst patVar (needRes "⇒" *> term)|] +compBranch : FileName -> Grammar True CompBranch +compBranch fname = [|(,,) dimConst (patVar fname) (needRes "⇒" *> term fname)|] + +private +checkCompTermBody : (PatVar, PTerm) -> PDim -> PDim -> PTerm -> PDim -> + CompBranch -> CompBranch -> Bounds -> + Grammar False (Loc -> PTerm) +checkCompTermBody a p q s r (e0, s0) (e1, s1) bounds = + case (e0, e1) of + (Zero, One) => pure $ Comp a p q s r s0 s1 + (One, Zero) => pure $ Comp a p q s r s1 s0 + (_, _) => + fatalLoc bounds "body of 'comp' needs one 0 case and one 1 case" export covering -compTerm : Grammar True PTerm -compTerm = do +compTerm : FileName -> Grammar True PTerm +compTerm fname = withLoc fname $ do resC "comp" mustWork $ do - a <- typeLine - p <- dimArg; q <- dimArg - s <- termArg; r <- dimArg - needRes "{" - s0 <- compBranch; needRes ";" - s1 <- compBranch; optRes ";" - needRes "}" - case (fst s0, fst s1) of - (Zero, One) => pure $ Comp a p q s r (snd s0) (snd s1) - (One, Zero) => pure $ Comp a p q s r (snd s1) (snd s0) - (_, _) => - fatalError "body of 'comp' needs one 0 case and one 1 case" + a <- typeLine fname + p <- dimArg fname; q <- dimArg fname + s <- termArg fname; r <- dimArg fname + bodyStart <- bounds $ needRes "{" + s0 <- compBranch fname; needRes ";" + s1 <- compBranch fname; optRes ";" + bodyEnd <- bounds $ needRes "}" + let body = bounds $ mergeBounds bodyStart bodyEnd + checkCompTermBody a p q s r s0 s1 body export covering -splitUniverseTerm : Grammar True PTerm -splitUniverseTerm = resC "★" *> mustWork [|TYPE nat|] +splitUniverseTerm : FileName -> Grammar True PTerm +splitUniverseTerm fname = withLoc fname $ resC "★" *> mustWork [|TYPE nat|] export covering -eqTerm : Grammar True PTerm -eqTerm = resC "Eq" *> mustWork [|Eq typeLine termArg termArg|] +eqTerm : FileName -> Grammar True PTerm +eqTerm fname = withLoc fname $ + resC "Eq" *> mustWork [|Eq (typeLine fname) (termArg fname) (termArg fname)|] export covering -succTerm : Grammar True PTerm -succTerm = resC "succ" *> mustWork [|Succ termArg|] +succTerm : FileName -> Grammar True PTerm +succTerm fname = withLoc fname $ + resC "succ" *> mustWork [|Succ (termArg fname)|] ||| a dimension argument with an `@` prefix, or ||| a term argument with no prefix export covering -anyArg : Grammar True (Either PDim PTerm) -anyArg = dimArg <||> termArg +anyArg : FileName -> Grammar True (Either PDim PTerm) +anyArg fname = dimArg fname <||> termArg fname export covering -normalAppTerm : Grammar True PTerm -normalAppTerm = foldl ap <$> termArg <*> many anyArg -where ap : PTerm -> Either PDim PTerm -> PTerm - ap f (Left p) = f :% p - ap f (Right s) = f :@ s +normalAppTerm : FileName -> Grammar True PTerm +normalAppTerm fname = withLoc fname $ do + head <- termArg fname + args <- many $ anyArg fname + pure $ \loc => foldl (ap loc) head args +where ap : Loc -> PTerm -> Either PDim PTerm -> PTerm + ap loc f (Left p) = DApp f p loc + ap loc f (Right s) = App f s loc ||| application term `f x @y z`, or other terms that look like application ||| like `succ` or `coe`. export covering -appTerm : Grammar True PTerm -appTerm = coeTerm - <|> compTerm - <|> splitUniverseTerm - <|> eqTerm - <|> succTerm - <|> normalAppTerm +appTerm : FileName -> Grammar True PTerm +appTerm fname = + coeTerm fname + <|> compTerm fname + <|> splitUniverseTerm fname + <|> eqTerm fname + <|> succTerm fname + <|> normalAppTerm fname export covering -infixEqTerm : Grammar True PTerm -infixEqTerm = do - l <- appTerm; commit - rest <- optional $ res "≡" *> [|(,) term (needRes ":" *> appTerm)|] - pure $ maybe l (\rest => Eq (Nothing, snd rest) l (fst rest)) rest +infixEqTerm : FileName -> Grammar True PTerm +infixEqTerm fname = withLoc fname $ do + l <- appTerm fname; commit + rest <- optional $ + res "≡" *> [|(,) (term fname) (needRes ":" *> appTerm fname)|] + let u = Unused $ onlyStart l.loc + pure $ \loc => maybe l (\rest => Eq (u, snd rest) l (fst rest) loc) rest export covering -annTerm : Grammar True PTerm -annTerm = do - tm <- infixEqTerm; commit - ty <- optional $ res "∷" *> term - pure $ maybe tm (tm :#) ty +annTerm : FileName -> Grammar True PTerm +annTerm fname = withLoc fname $ do + tm <- infixEqTerm fname; commit + ty <- optional $ res "∷" *> term fname + pure $ \loc => maybe tm (\ty => Ann tm ty loc) ty export covering -lamTerm : Grammar True PTerm -lamTerm = do +lamTerm : FileName -> Grammar True PTerm +lamTerm fname = withLoc fname $ do k <- DLam <$ res "δ" <|> Lam <$ res "λ" mustWork $ do - xs <- some patVar; needRes "⇒" - body <- term; commit - pure $ foldr k body xs + xs <- some $ patVar fname; needRes "⇒" + body <- term fname; commit + pure $ \loc => foldr (\x, s => k x s loc) body xs -- [todo] fix the backtracking in e.g. (F x y z × B) export covering -properBinders : Grammar True (List1 BName, PTerm) -properBinders = do +properBinders : FileName -> Grammar True (List1 PatVar, PTerm) +properBinders fname = do res "(" - xs <- some patVar; resC ":" - t <- term; needRes ")" + xs <- some $ patVar fname; resC ":" + t <- term fname; needRes ")" pure (xs, t) export covering -piTerm : Grammar True PTerm -piTerm = do - q <- qty; resC "." - dom <- piBinder; needRes "→" - cod <- term; commit - pure $ foldr (\x => Pi q x (snd dom)) cod (fst dom) +piTerm : FileName -> Grammar True PTerm +piTerm fname = withLoc fname $ do + q <- qty fname; resC "." + dom <- piBinder; needRes "→" + cod <- term fname; commit + pure $ \loc => foldr (\x, t => Pi q x (snd dom) t loc) cod (fst dom) where - piBinder : Grammar True (List1 BName, PTerm) - piBinder = properBinders <|> [|(singleton Nothing,) termArg|] + piBinder : Grammar True (List1 PatVar, PTerm) + piBinder = properBinders fname + <|> [|(,) [|singleton $ unused fname|] (termArg fname)|] export covering -sigmaTerm : Grammar True PTerm -sigmaTerm = - (properBinders >>= continueDep) - <|> (annTerm >>= continueNondep) +sigmaTerm : FileName -> Grammar True PTerm +sigmaTerm fname = + (properBinders fname >>= continueDep) + <|> (annTerm fname >>= continueNondep) where - continueDep : (List1 BName, PTerm) -> Grammar True PTerm - continueDep (names, dom) = do - cod <- needRes "×" *> sigmaTerm - pure $ foldr (\x => Sig x dom) cod names - continueNondep : PTerm -> Grammar False PTerm - continueNondep dom = do - rest <- optional $ resC "×" *> sepBy1 (res "×") annTerm - Core.pure $ foldr1 (Sig Nothing) $ dom ::: maybe [] forget rest + continueDep : (List1 PatVar, PTerm) -> Grammar True PTerm + continueDep (names, fst) = withLoc fname $ do + snd <- needRes "×" *> sigmaTerm fname + pure $ \loc => foldr (\x, snd => Sig x fst snd loc) snd names + cross : PTerm -> PTerm -> PTerm + cross l r = let loc = extend' l.loc r.loc.bounds in + Sig (Unused $ onlyStart l.loc) l r loc + + continueNondep : PTerm -> Grammar False PTerm + continueNondep fst = do + rest <- optional $ resC "×" *> sepBy1 (res "×") (annTerm fname) + pure $ foldr1 cross $ fst ::: maybe [] toList rest public export PCaseArm : Type PCaseArm = (PCasePat, PTerm) +export covering +caseArm : FileName -> Grammar True PCaseArm +caseArm fname = [|(,) (casePat fname) (needRes "⇒" *> term fname)|] + export -checkCaseArms : List PCaseArm -> Grammar False PCaseBody -checkCaseArms [] = - pure $ CaseEnum [] -checkCaseArms ((PPair x y, rhs) :: rest) = do - let [] = rest | _ => fatalError "unexpected pattern after pair" - pure $ CasePair (x, y) rhs -checkCaseArms ((PTag tag, rhs1) :: rest) = do +checkCaseArms : Loc -> List PCaseArm -> Grammar False PCaseBody +checkCaseArms loc [] = pure $ CaseEnum [] loc +checkCaseArms loc ((PPair x y _, rhs) :: rest) = + if null rest then pure $ CasePair (x, y) rhs loc + else fatalError "unexpected pattern after pair" +checkCaseArms loc ((PTag tag _, rhs1) :: rest) = do let rest = for rest $ \case - (PTag tag, rhs) => Just (tag, rhs) - _ => Nothing + (PTag tag _, rhs) => Just (tag, rhs) + _ => Nothing maybe (fatalError "expected all patterns to be tags") - (pure . CaseEnum . ((tag, rhs1) ::)) rest -checkCaseArms ((PZero, rhs1) :: rest) = do - let [(PSucc p q ih, rhs2)] = rest + (\rest => pure $ CaseEnum ((tag, rhs1) :: rest) loc) rest +checkCaseArms loc ((PZero _, rhs1) :: rest) = do + let [(PSucc p q ih _, rhs2)] = rest | _ => fatalError "expected succ pattern after zero" - pure $ CaseNat rhs1 (p, q, ih, rhs2) -checkCaseArms ((PSucc p q ih, rhs1) :: rest) = do - let [(PZero, rhs2)] = rest + pure $ CaseNat rhs1 (p, q, ih, rhs2) loc +checkCaseArms loc ((PSucc p q ih _, rhs1) :: rest) = do + let [(PZero _, rhs2)] = rest | _ => fatalError "expected zero pattern after succ" - pure $ CaseNat rhs2 (p, q, ih, rhs1) -checkCaseArms ((PBox x, rhs) :: rest) = do - let [] = rest | _ => fatalError "unexpected pattern after box" - pure $ CaseBox x rhs + pure $ CaseNat rhs2 (p, q, ih, rhs1) loc +checkCaseArms loc ((PBox x _, rhs) :: rest) = + if null rest then pure $ CaseBox x rhs loc + else fatalError "unexpected pattern after box" export covering -caseArm : Grammar True PCaseArm -caseArm = [|(,) casePat (needRes "⇒" *> term)|] +caseBody : FileName -> Grammar True PCaseBody +caseBody fname = do + body <- bounds $ delimSep "{" "}" ";" $ caseArm fname + let loc = makeLoc fname body.bounds + checkCaseArms loc body.val export covering -caseBody : Grammar True PCaseBody -caseBody = delimSep "{" "}" ";" caseArm >>= checkCaseArms +caseReturn : FileName -> Grammar True (PatVar, PTerm) +caseReturn fname = do + x <- patVar fname <* resC "⇒" <|> unused fname + ret <- term fname + pure (x, ret) export covering -caseTerm : Grammar True PTerm -caseTerm = do - qty <- caseIntro; commit - head <- mustWork term; needRes "return" - ret <- mustWork [|(,) (option Nothing $ patVar <* resC "⇒") term|] - needRes "of" - body <- mustWork caseBody +caseTerm : FileName -> Grammar True PTerm +caseTerm fname = withLoc fname $ do + qty <- caseIntro fname; commit + head <- mustWork $ term fname; needRes "return" + ret <- mustWork $ caseReturn fname; needRes "of" + body <- mustWork $ caseBody fname pure $ Case qty head ret body +-- export covering +-- term : FileName -> Grammar True PTerm +term fname = lamTerm fname + <|> caseTerm fname + <|> piTerm fname + <|> sigmaTerm fname -term = lamTerm - <|> caseTerm - <|> piTerm - <|> sigmaTerm +export covering +decl : FileName -> Grammar True PDecl ||| `def` alone means `defω` export -defIntro : Grammar True Qty -defIntro = Zero <$ resC "def0" - <|> Any <$ resC "defω" - <|> resC "def" *> option Any (qty <* needRes ".") - +defIntro : FileName -> Grammar True PQty +defIntro fname = + withLoc fname (PQ Zero <$ resC "def0") + <|> withLoc fname (PQ Any <$ resC "defω") + <|> do pos <- bounds $ resC "def" + let any = PQ Any $ makeLoc fname pos.bounds + option any $ qty fname <* needRes "." export covering -decl : Grammar True PDecl - -export covering -definition : Grammar True PDefinition -definition = do - qty <- defIntro +definition : FileName -> Grammar True PDefinition +definition fname = withLoc fname $ do + qty <- defIntro fname name <- baseName - type <- optional $ resC ":" *> mustWork term - term <- needRes "=" *> mustWork term + type <- optional $ resC ":" *> mustWork (term fname) + term <- needRes "=" *> mustWork (term fname) optRes ";" - pure $ MkPDef {qty, name, type, term} + pure $ MkPDef qty name type term export covering -namespace_ : Grammar True PNamespace -namespace_ = do +namespace_ : FileName -> Grammar True PNamespace +namespace_ fname = withLoc fname $ do ns <- resC "namespace" *> qname; needRes "{" decls <- nsInner; optRes ";" pure $ MkPNamespace (ns.mods :< ns.base) decls where nsInner : Grammar True (List PDecl) nsInner = [] <$ resC "}" - <|> [|(decl <* commit) :: nsInner|] + <|> [|(decl fname <* commit) :: nsInner|] -decl = [|PDef definition|] <|> [|PNs namespace_|] +decl fname = [|PDef $ definition fname|] <|> [|PNs $ namespace_ fname|] export covering -load : Grammar True String -load = resC "load" *> mustWork strLit <* optRes ";" +load : FileName -> Grammar True PTopLevel +load fname = withLoc fname $ + resC "load" *> mustWork [|PLoad strLit|] <* optRes ";" export covering -topLevel : Grammar True PTopLevel -topLevel = [|PLoad load|] <|> [|PD decl|] +topLevel : FileName -> Grammar True PTopLevel +topLevel fname = load fname <|> [|PD $ decl fname|] export covering -input : Grammar False (List PTopLevel) -input = [] <$ eof - <|> [|(topLevel <* commit) :: input|] +input : FileName -> Grammar False (List PTopLevel) +input fname = [] <$ eof + <|> [|(topLevel fname <* commit) :: input fname|] export covering -lexParseTerm : String -> Either Error PTerm -lexParseTerm = lexParseWith term +lexParseTerm : FileName -> String -> Either Error PTerm +lexParseTerm = lexParseWith . term export covering -lexParseInput : String -> Either Error (List PTopLevel) -lexParseInput = lexParseWith input +lexParseInput : FileName -> String -> Either Error (List PTopLevel) +lexParseInput = lexParseWith . input diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr index 0c33ff5..c5a8648 100644 --- a/lib/Quox/Parser/Syntax.idr +++ b/lib/Quox/Parser/Syntax.idr @@ -1,5 +1,6 @@ module Quox.Parser.Syntax +import public Quox.Loc import public Quox.Syntax import public Quox.Definition @@ -11,81 +12,148 @@ import Derive.Prelude public export -BName : Type -BName = Maybe String +data PatVar = Unused Loc | PV PBaseName Loc +%name PatVar v +%runElab derive "PatVar" [Eq, Ord, Show] + +export +Located PatVar where + (Unused loc).loc = loc + (PV _ loc).loc = loc + +export +(.name) : PatVar -> Maybe PBaseName +(Unused _).name = Nothing +(PV nm _).name = Just nm + +export +isUnused : PatVar -> Bool +isUnused (Unused {}) = True +isUnused _ = False + public export -PUniverse : Type -PUniverse = Nat +data PQty = PQ Qty Loc +%name PQty qty +%runElab derive "PQty" [Eq, Ord, Show] + +export Located PQty where (PQ _ loc).loc = loc namespace PDim public export - data PDim = K DimConst | V PBaseName + data PDim = K DimConst Loc | V PBaseName Loc %name PDim p, q %runElab derive "PDim" [Eq, Ord, Show] +export +Located PDim where + (K _ loc).loc = loc + (V _ loc).loc = loc + +public export +data PTagVal = PT TagVal Loc +%name PTagVal tag +%runElab derive "PTagVal" [Eq, Ord, Show] + + namespace PTerm mutual ||| terms out of the parser with BVs and bidirectionality still tangled up public export data PTerm = - TYPE Nat + TYPE Universe Loc - | Pi Qty BName PTerm PTerm - | Lam BName PTerm - | (:@) PTerm PTerm + | Pi PQty PatVar PTerm PTerm Loc + | Lam PatVar PTerm Loc + | App PTerm PTerm Loc - | Sig BName PTerm PTerm - | Pair PTerm PTerm - | Case Qty PTerm (BName, PTerm) PCaseBody + | Sig PatVar PTerm PTerm Loc + | Pair PTerm PTerm Loc + | Case PQty PTerm (PatVar, PTerm) PCaseBody Loc - | Enum (List TagVal) - | Tag TagVal + | Enum (List TagVal) Loc + | Tag TagVal Loc - | Eq (BName, PTerm) PTerm PTerm - | DLam BName PTerm - | (:%) PTerm PDim + | Eq (PatVar, PTerm) PTerm PTerm Loc + | DLam PatVar PTerm Loc + | DApp PTerm PDim Loc - | Nat - | Zero | Succ PTerm + | Nat Loc + | Zero Loc | Succ PTerm Loc - | BOX Qty PTerm - | Box PTerm + | BOX PQty PTerm Loc + | Box PTerm Loc - | V PName - | (:#) PTerm PTerm + | V PName Loc + | Ann PTerm PTerm Loc - | Coe (BName, PTerm) PDim PDim PTerm - | Comp (BName, PTerm) PDim PDim PTerm PDim (BName, PTerm) (BName, PTerm) + | Coe (PatVar, PTerm) PDim PDim PTerm Loc + | Comp (PatVar, PTerm) PDim PDim PTerm PDim + (PatVar, PTerm) (PatVar, PTerm) Loc %name PTerm s, t public export data PCaseBody = - CasePair (BName, BName) PTerm - | CaseEnum (List (TagVal, PTerm)) - | CaseNat PTerm (BName, Qty, BName, PTerm) - | CaseBox BName PTerm + CasePair (PatVar, PatVar) PTerm Loc + | CaseEnum (List (PTagVal, PTerm)) Loc + | CaseNat PTerm (PatVar, PQty, PatVar, PTerm) Loc + | CaseBox PatVar PTerm Loc %name PCaseBody body %runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show] +export +Located PTerm where + (TYPE _ loc).loc = loc + (Pi _ _ _ _ loc).loc = loc + (Lam _ _ loc).loc = loc + (App _ _ loc).loc = loc + (Sig _ _ _ loc).loc = loc + (Pair _ _ loc).loc = loc + (Case _ _ _ _ loc).loc = loc + (Enum _ loc).loc = loc + (Tag _ loc).loc = loc + (Eq _ _ _ loc).loc = loc + (DLam _ _ loc).loc = loc + (DApp _ _ loc).loc = loc + (Nat loc).loc = loc + (Zero loc).loc = loc + (Succ _ loc).loc = loc + (BOX _ _ loc).loc = loc + (Box _ loc).loc = loc + (V _ loc).loc = loc + (Ann _ _ loc).loc = loc + (Coe _ _ _ _ loc).loc = loc + (Comp _ _ _ _ _ _ _ loc).loc = loc + +export +Located PCaseBody where + (CasePair _ _ loc).loc = loc + (CaseEnum _ loc).loc = loc + (CaseNat _ _ loc).loc = loc + (CaseBox _ _ loc).loc = loc + public export record PDefinition where constructor MkPDef - qty : Qty + qty : PQty name : PBaseName type : Maybe PTerm term : PTerm + loc_ : Loc %name PDefinition def %runElab derive "PDefinition" [Eq, Ord, Show] +export Located PDefinition where def.loc = def.loc_ + mutual public export record PNamespace where constructor MkPNamespace name : Mods decls : List PDecl + loc_ : Loc %name PNamespace ns public export @@ -95,125 +163,25 @@ mutual %name PDecl decl %runElab deriveMutual ["PNamespace", "PDecl"] [Eq, Ord, Show] +export Located PNamespace where ns.loc = ns.loc_ + +export +Located PDecl where + (PDef def).loc = def.loc + (PNs ns).loc = ns.loc + public export -data PTopLevel = PD PDecl | PLoad String +data PTopLevel = PD PDecl | PLoad String Loc %name PTopLevel t %runElab derive "PTopLevel" [Eq, Ord, Show] - export -toPDimWith : Context' PBaseName d -> Dim d -> PDim -toPDimWith ds (K e) = K e -toPDimWith ds (B i) = V $ ds !!! i +Located PTopLevel where + (PD decl).loc = decl.loc + (PLoad _ loc).loc = loc -export -toPDim : Dim 0 -> PDim -toPDim = toPDimWith [<] public export -fromNat : Nat -> PTerm -fromNat 0 = Zero -fromNat (S k) = Succ $ fromNat k - - -{- -mutual - namespace Term - export - toPTermWith : Context' PBaseName d -> Context' PBaseName n -> - Term d n -> PTerm - toPTermWith ds ns t = - let Element t _ = pushSubsts t in - toPTermWith' ds ns t - - private - toPTermWith' : Context' PBaseName d -> Context' PBaseName n -> - (t : Term 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 $ show x) - (toPTermWith ds ns arg) - (toPTermWith ds (ns :< baseStr x) res.term) - Lam (S [< x] body) => - Lam (Just $ show x) $ - toPTermWith ds (ns :< baseStr x) body.term - Sig fst (S [< x] snd) => - 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 => - Enum $ SortedSet.toList cases - Tag tag => - Tag tag - Eq (S [< i] ty) l r => - 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 $ show i) $ toPTermWith (ds :< baseStr i) ns body.term - Nat => Nat - Zero => Zero - Succ n => Succ $ toPTermWith ds ns n - BOX q ty => BOX q $ toPTermWith ds ns ty - Box val => Box $ toPTermWith ds ns val - E e => - toPTermWith ds ns e - - namespace Elim - export - toPTermWith : Context' PBaseName d -> Context' PBaseName n -> - Elim d n -> PTerm - toPTermWith ds ns e = - let Element e _ = pushSubsts e in - toPTermWith' ds ns e - - private - toPTermWith' : Context' PBaseName d -> Context' PBaseName n -> - (e : Elim d n) -> (0 _ : NotClo e) => - PTerm - toPTermWith' ds ns e = case e of - F x => - V $ toPName x - B 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 $ 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 $ baseStr r, toPTermWith ds (ns :< baseStr r) ret.term) - (CaseEnum $ mapSnd (toPTermWith ds ns) <$> SortedMap.toList arms) - CaseNat qtyNat qtyIH nat (S [< r] ret) zer (S [< p, ih] suc) => - Case qtyNat (toPTermWith ds ns nat) - (Just $ baseStr r, toPTermWith ds (ns :< baseStr r) ret.term) - (CaseNat (toPTermWith ds ns zer) - (Just $ baseStr p, qtyIH, Just $ baseStr ih, - toPTermWith ds (ns :< baseStr p :< baseStr ih) suc.term)) - CaseBox qty box (S [< r] ret) (S [< b] body) => - Case qty (toPTermWith ds ns box) - (Just $ baseStr r, toPTermWith ds (ns :< baseStr r) ret.term) - (CaseBox (Just $ baseStr b) $ - toPTermWith ds (ns :< baseStr b) body.term) - fun :% arg => - toPTermWith ds ns fun :% toPDimWith ds arg - tm :# ty => - toPTermWith ds ns tm :# toPTermWith ds ns ty - -namespace Term - export - toPTerm : Term 0 0 -> PTerm - toPTerm = toPTermWith [<] [<] - -namespace Elim - export - toPTerm : Elim 0 0 -> PTerm - toPTerm = toPTermWith [<] [<] --} +fromNat : Nat -> Loc -> PTerm +fromNat 0 loc = Zero loc +fromNat (S k) loc = Succ (fromNat k loc) loc diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index d9574e1..55749e0 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -14,6 +14,7 @@ modules = Quox.EffExtra, Quox.Decidable, Quox.No, + Quox.Loc, Quox.OPE, Quox.Pretty, Quox.Syntax, diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr index 0507a8e..c453b05 100644 --- a/tests/Tests/FromPTerm.idr +++ b/tests/Tests/FromPTerm.idr @@ -37,12 +37,13 @@ ToInfo Failure where parameters {c : Bool} {auto _ : Show b} - (grm : Grammar c a) (fromP : a -> Either FromParser.Error b) + (grm : FileName -> Grammar c a) + (fromP : a -> Either FromParser.Error b) (inp : String) parameters {default (ltrim inp) label : String} parsesWith : (b -> Bool) -> Test parsesWith p = test label $ do - pres <- mapFst ParseError $ lexParseWith grm inp + pres <- mapFst ParseError $ lexParseWith (grm "‹test›") inp res <- mapFst FromParser $ fromP pres unless (p res) $ Left $ WrongResult $ show res @@ -55,11 +56,11 @@ parameters {c : Bool} {auto _ : Show b} parameters {default "\{ltrim inp} # fails" label : String} parseFails : Test parseFails = test label $ do - pres <- mapFst ParseError $ lexParseWith grm inp + pres <- mapFst ParseError $ lexParseWith (grm "‹test›") inp either (const $ Right ()) (Left . ExpectedFail . show) $ fromP pres -FromString BName where fromString = Just . fromString +FromString PatVar where fromString x = PV x Nothing runFromParser : {default empty defs : Definitions} -> Eff FromParserPure a -> Either FromParser.Error a diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index 0889997..54d22b5 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -4,6 +4,9 @@ import Quox.Parser import Data.List import Data.String import TAP +import Language.Reflection + +%language ElabReflection public export data Failure = @@ -29,204 +32,227 @@ ToInfo Failure where [("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 - res <- mapFst ParseError $ lexParseWith grm inp - unless (p res) $ Left $ WrongResult $ show res +parameters {auto _ : (Show a, Eq a)} {c : Bool} (grm : FileName -> Grammar c a) + parsesWith : String -> (a -> Bool) -> Test + parsesWith inp p = test (ltrim inp) $ do + res <- mapFst ParseError $ lexParseWith (grm "‹test›") inp + unless (p res) $ Left $ WrongResult $ show res - parses : Test - parses = parsesWith $ const True + parsesAs : String -> a -> Test + parsesAs inp exp = parsesWith inp (== exp) - parsesAs : Eq a => a -> Test - parsesAs exp = parsesWith (== exp) + %macro + parseMatch : String -> TTImp -> Elab Test + parseMatch inp pat = + parsesWith inp <$> check `(\case ~(pat) => True; _ => False) - parameters {default "\{ltrim inp} # fails" label : String} - parseFails : Test - parseFails = test label $ do - either (const $ Right ()) (Left . ExpectedFail . show) $ - lexParseWith grm inp + parseFails : String -> Test + parseFails inp = test "\{ltrim inp} # fails" $ do + either (const $ Right ()) (Left . ExpectedFail . show) $ + lexParseWith (grm "‹test›") inp export tests : Test tests = "parser" :- [ "pattern vars" :- [ - parsesAs patVar "_" Nothing, - parsesAs patVar "F" (Just "F"), + parseMatch patVar "_" `(Unused _), + parseMatch patVar "F" `(PV "F" _), parseFails patVar "a.b.c" ], "names" :- [ - parsesAs qname "x" + parsesAs (const qname) "x" (MakePName [<] "x"), - parsesAs qname "Data.String.length" + parsesAs (const qname) "Data.String.length" (MakePName [< "Data", "String"] "length"), - parseFails qname "_" + parseFails (const qname) "_" ], "dimensions" :- [ - parsesAs dim "0" (K Zero), - parsesAs dim "1" (K One), - parsesAs dim "𝑖" (V "𝑖"), + parseMatch dim "0" `(K Zero _), + parseMatch dim "1" `(K One _), + parseMatch dim "𝑖" `(V "𝑖" _), parseFails dim "M.x", parseFails dim "_" ], "quantities" :- [ - parsesAs qty "0" Zero, - parsesAs qty "1" One, - parsesAs qty "ω" Any, - parsesAs qty "#" Any, + parseMatch qty "0" `(PQ Zero _), + parseMatch qty "1" `(PQ One _), + parseMatch qty "ω" `(PQ Any _), + parseMatch qty "#" `(PQ 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", ","]), + parseMatch term #"{}"# `(Enum [] _), + parseMatch term #"{a}"# `(Enum ["a"] _), + parseMatch term #"{a,}"# `(Enum ["a"] _), + parseMatch term #"{a.b.c.d}"# `(Enum ["a.b.c.d"] _), + parseMatch term #"{"hel lo"}"# `(Enum ["hel lo"] _), + parseMatch term #"{a, b}"# `(Enum ["a", "b"] _), + parseMatch term #"{a, b,}"# `(Enum ["a", "b"] _), + parseMatch 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"} + parseMatch term #" 'a "# `(Tag "a" _), + parseMatch term #" 'abc "# `(Tag "abc" _), + parseMatch term #" '"abc" "# `(Tag "abc" _), + parseMatch term #" '"a b c" "# `(Tag "a b c" _), + note "application to two arguments", + parseMatch term #" 'a b c "# + `(App (App (Tag "a" _) (V "b" _) _) (V "c" _) _) ], "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), + parseMatch term "★₀" `(TYPE 0 _), + parseMatch term "★1" `(TYPE 1 _), + parseMatch term "★ 2" `(TYPE 2 _), + parseMatch term "Type₃" `(TYPE 3 _), + parseMatch term "Type4" `(TYPE 4 _), + parseMatch term "Type 100" `(TYPE 100 _), + parseMatch term "(Type 1000)" `(TYPE 1000 _), parseFails term "Type", parseFails term "★" ], "applications" :- [ - parsesAs term "f" (V "f"), - 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"), - 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") + parseMatch term "f" + `(V "f" _), + parseMatch term "f.x.y" + `(V (MakePName [< "f", "x"] "y") _), + parseMatch term "f x" + `(App (V "f" _) (V "x" _) _), + parseMatch term "f x y" + `(App (App (V "f" _) (V "x" _) _) (V "y" _) _), + parseMatch term "(f x) y" + `(App (App (V "f" _) (V "x" _) _) (V "y" _) _), + parseMatch term "f (g x)" + `(App (V "f" _) (App (V "g" _) (V "x" _) _) _), + parseMatch term "f (g x) y" + `(App (App (V "f" _) (App (V "g" _) (V "x" _) _) _) (V "y" _) _), + parseMatch term "f @p" + `(DApp (V "f" _) (V "p" _) _), + parseMatch term "f x @p y" + `(App (DApp (App (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)) + parseMatch term "f :: A" + `(Ann (V "f" _) (V "A" _) _), + parseMatch term "f ∷ A" + `(Ann (V "f" _) (V "A" _) _), + parseMatch term "f x y ∷ A B C" + `(Ann (App (App (V "f" _) (V "x" _) _) (V "y" _) _) + (App (App (V "A" _) (V "B" _) _) (V "C" _) _) _), + parseMatch term "Type 0 ∷ Type 1 ∷ Type 2" + `(Ann (TYPE 0 _) (Ann (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"), - parsesAs term "1.(x y : A) -> B x" $ - Pi One (Just "x") (V "A") $ Pi One (Just "y") (V "A") (V "B" :@ V "x"), + parseMatch term "1.(x : A) → B x" + `(Pi (PQ One _) (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _), + parseMatch term "1.(x : A) -> B x" + `(Pi (PQ One _) (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _), + parseMatch term "ω.(x : A) → B x" + `(Pi (PQ Any _) (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _), + parseMatch term "#.(x : A) -> B x" + `(Pi (PQ Any _) (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _), + parseMatch term "1.(x y : A) -> B x" + `(Pi (PQ One _) (PV "x" _) (V "A" _) + (Pi (PQ One _) (PV "y" _) (V "A" _) + (App (V "B" _) (V "x" _) _) _) _), parseFails term "(x : A) → B x", - parsesAs term "1.A → B" - (Pi One Nothing (V "A") (V "B")), - parsesAs term "1.(List A) → List B" - (Pi One Nothing (V "List" :@ V "A") (V "List" :@ V "B")), + parseMatch term "1.A → B" + `(Pi (PQ One _) (Unused _) (V "A" _) (V "B" _) _), + parseMatch term "1.(List A) → List B" + `(Pi (PQ One _) (Unused _) + (App (V "List" _) (V "A" _) _) + (App (V "List" _) (V "B" _) _) _), parseFails term "1.List A → List B", - 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"), - parsesAs term "(x y : A) × B x" $ - Sig (Just "x") (V "A") $ Sig (Just "y") (V "A") (V "B" :@ V "x"), + parseMatch term "(x : A) × B x" + `(Sig (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _), + parseMatch term "(x : A) ** B x" + `(Sig (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _), + parseMatch term "(x y : A) × B" $ + `(Sig (PV "x" _) (V "A" _) (Sig (PV "y" _) (V "A" _) (V "B" _) _) _), parseFails term "1.(x : A) × B x", - parsesAs term "A × B" $ - Sig Nothing (V "A") (V "B"), - parsesAs term "A ** B" $ - Sig Nothing (V "A") (V "B"), - parsesAs term "A × B × C" $ - Sig Nothing (V "A") (Sig Nothing (V "B") (V "C")), - parsesAs term "(A × B) × C" $ - Sig Nothing (Sig Nothing (V "A") (V "B")) (V "C") + parseMatch term "A × B" + `(Sig (Unused _) (V "A" _) (V "B" _) _), + parseMatch term "A ** B" + `(Sig (Unused _) (V "A" _) (V "B" _) _), + parseMatch term "A × B × C" $ + `(Sig (Unused _) (V "A" _) (Sig (Unused _) (V "B" _) (V "C" _) _) _), + parseMatch term "(A × B) × C" $ + `(Sig (Unused _) (Sig (Unused _) (V "A" _) (V "B" _) _) (V "C" _) _) ], "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" + parseMatch term "λ x ⇒ x" + `(Lam (PV "x" _) (V "x" _) _), + parseMatch term "fun x => x" + `(Lam (PV "x" _) (V "x" _) _), + parseMatch term "δ i ⇒ x @i" + `(DLam (PV "i" _) (DApp (V "x" _) (V "i" _) _) _), + parseMatch term "dfun i => x @i" + `(DLam (PV "i" _) (DApp (V "x" _) (V "i" _) _) _), + parseMatch term "λ x y z ⇒ x z y" + `(Lam (PV "x" _) + (Lam (PV "y" _) + (Lam (PV "z" _) + (App (App (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 + parseMatch term "(x, y)" + `(Pair (V "x" _) (V "y" _) _), + parseMatch term "(x, y, z)" + `(Pair (V "x" _) (Pair (V "y" _) (V "z" _) _) _), + parseMatch term "((x, y), z)" + `(Pair (Pair (V "x" _) (V "y" _) _) (V "z" _) _), + parseMatch term "(f x, g @y)" + `(Pair (App (V "f" _) (V "x" _) _) (DApp (V "g" _) (V "y" _) _) _), + parseMatch term "((x : A) × B, 0.(x : C) → D)" + `(Pair (Sig (PV "x" _) (V "A" _) (V "B" _) _) + (Pi (PQ Zero _) (PV "x" _) (V "C" _) (V "D" _) _) _), + parseMatch term "(λ x ⇒ x, δ i ⇒ e @i)" + `(Pair (Lam (PV "x" _) (V "x" _) _) + (DLam (PV "i" _) (DApp (V "e" _) (V "i" _) _) _) _), + parseMatch 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"), - parsesAs term "(A × B) ≡ (A' × B') : ★₁" $ - Eq (Nothing, TYPE 1) - (Sig Nothing (V "A") (V "B")) (Sig Nothing (V "A'") (V "B'")), + parseMatch term "Eq [i ⇒ A] s t" + `(Eq (PV "i" _, V "A" _) (V "s" _) (V "t" _) _), + parseMatch term "Eq [i ⇒ A (B @i)] (f x) (g y)" + `(Eq (PV "i" _, App (V "A" _) (DApp (V "B" _) (V "i" _) _) _) + (App (V "f" _) (V "x" _) _) + (App (V "g" _) (V "y" _) _) _), + parseMatch term "Eq [A] s t" + `(Eq (Unused _, V "A" _) (V "s" _) (V "t" _) _), + parseMatch term "s ≡ t : A" + `(Eq (Unused _, V "A" _) (V "s" _) (V "t" _) _), + parseMatch term "s == t : A" + `(Eq (Unused _, V "A" _) (V "s" _) (V "t" _) _), + parseMatch term "f x ≡ g y : A B" + `(Eq (Unused _, App (V "A" _) (V "B" _) _) + (App (V "f" _) (V "x" _) _) + (App (V "g" _) (V "y" _) _) _), + parseMatch term "(A × B) ≡ (A' × B') : ★₁" + `(Eq (Unused _, TYPE 1 _) + (Sig (Unused _) (V "A" _) (V "B" _) _) + (Sig (Unused _) (V "A'" _) (V "B'" _) _) _), note "A × (B ≡ A' × B' : ★₁)", - parsesAs term "A × B ≡ A' × B' : ★₁" $ - Sig Nothing (V "A") $ - Eq (Nothing, TYPE 1) - (V "B") (Sig Nothing (V "A'") (V "B'")), + parseMatch term "A × B ≡ A' × B' : ★₁" + `(Sig (Unused _) (V "A" _) + (Eq (Unused _, TYPE 1 _) + (V "B" _) (Sig (Unused _) (V "A'" _) (V "B'" _) _) _) _), parseFails term "Eq", parseFails term "Eq s t", parseFails term "s ≡ t", @@ -234,127 +260,144 @@ tests = "parser" :- [ ], "naturals" :- [ - parsesAs term "ℕ" Nat, - parsesAs term "Nat" Nat, - parsesAs term "zero" Zero, - parsesAs term "succ n" (Succ $ V "n"), - parsesAs term "3" (fromNat 3), - parsesAs term "succ (succ 5)" (fromNat 7), + parseMatch term "ℕ" `(Nat _), + parseMatch term "Nat" `(Nat _), + parseMatch term "zero" `(Zero _), + parseMatch term "succ n" `(Succ (V "n" _) _), + parseMatch term "3" + `(Succ (Succ (Succ (Zero _) _) _) _), + parseMatch term "succ (succ 1)" + `(Succ (Succ (Succ (Zero _) _) _) _), parseFails term "succ succ 5", parseFails term "succ" ], "box" :- [ - parsesAs term "[1.ℕ]" $ BOX One Nat, - parsesAs term "[ω. ℕ × ℕ]" $ BOX Any (Sig Nothing Nat Nat), - parsesAs term "[a]" $ Box (V "a"), - parsesAs term "[0]" $ Box Zero, - parsesAs term "[1]" $ Box (Succ Zero) + parseMatch term "[1.ℕ]" + `(BOX (PQ One _) (Nat _) _), + parseMatch term "[ω. ℕ × ℕ]" + `(BOX (PQ Any _) (Sig (Unused _) (Nat _) (Nat _) _) _), + parseMatch term "[a]" + `(Box (V "a" _) _), + parseMatch term "[0]" + `(Box (Zero _) _), + parseMatch term "[1]" + `(Box (Succ (Zero _) _) _) ], "coe" :- [ - parsesAs term "coe [A] @p @q x" $ - Coe (Nothing, V "A") (V "p") (V "q") (V "x"), - parsesAs term "coe [i ⇒ A] @p @q x" $ - Coe (Just "i", V "A") (V "p") (V "q") (V "x"), + parseMatch term "coe [A] @p @q x" + `(Coe (Unused _, V "A" _) (V "p" _) (V "q" _) (V "x" _) _), + parseMatch term "coe [i ⇒ A] @p @q x" + `(Coe (PV "i" _, V "A" _) (V "p" _) (V "q" _) (V "x" _) _), parseFails term "coe [A] @p @q", parseFails term "coe A @p @q x", parseFails term "coe [i ⇒ A] @p q x" ], "comp" :- [ - parsesAs term "comp [A] @p @q s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }" $ - Comp (Nothing, V "A") (V "p") (V "q") (V "s") (V "r") - (Just "𝑗", V "s₀") (Just "𝑘", V "s₁"), - parsesAs term "comp [A] @p @q s @r { 1 𝑗 ⇒ s₀; 0 𝑘 ⇒ s₁; }" $ - Comp (Nothing, V "A") (V "p") (V "q") (V "s") (V "r") - (Just "𝑘", V "s₁") (Just "𝑗", V "s₀"), + parseMatch term "comp [A] @p @q s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }" + `(Comp (Unused _, V "A" _) (V "p" _) (V "q" _) (V "s" _) (V "r" _) + (PV "𝑗" _, V "s₀" _) (PV "𝑘" _, V "s₁" _) _), + parseMatch term "comp [A] @p @q s @r { 1 𝑗 ⇒ s₀; 0 𝑘 ⇒ s₁; }" + `(Comp (Unused _, V "A" _) (V "p" _) (V "q" _) (V "s" _) (V "r" _) + (PV "𝑘" _, V "s₁" _) (PV "𝑗" _, V "s₀" _) _), parseFails term "comp [A] @p @q s @r { 1 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁; }", parseFails term "comp [A] @p @q s @r { 0 𝑗 ⇒ s₀ }", parseFails term "comp [A] @p @q s @r { }" ], "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 []), - parsesAs term "caseω n return A of { 0 ⇒ a; succ n' ⇒ b }" $ - Case Any (V "n") (Nothing, V "A") $ - CaseNat (V "a") (Just "n'", Zero, Nothing, V "b"), - parsesAs term "caseω n return ℕ of { succ _, 1.ih ⇒ ih; zero ⇒ 0; }" $ - Case Any (V "n") (Nothing, Nat) $ - CaseNat Zero (Nothing, One, Just "ih", V "ih"), + parseMatch term + "case1 f s return x ⇒ A x of { (l, r) ⇒ r l }" + `(Case (PQ One _) (App (V "f" _) (V "s" _) _) + (PV "x" _, App (V "A" _) (V "x" _) _) + (CasePair (PV "l" _, PV "r" _) + (App (V "r" _) (V "l" _) _) _) _), + parseMatch term + "case1 f s return x => A x of { (l, r) ⇒ r l; }" + `(Case (PQ One _) (App (V "f" _) (V "s" _) _) + (PV "x" _, App (V "A" _) (V "x" _) _) + (CasePair (PV "l" _, PV "r" _) + (App (V "r" _) (V "l" _) _) _) _), + parseMatch term + "case 1 . f s return x ⇒ A x of { (l, r) ⇒ r l }" + `(Case (PQ One _) (App (V "f" _) (V "s" _) _) + (PV "x" _, App (V "A" _) (V "x" _) _) + (CasePair (PV "l" _, PV "r" _) + (App (V "r" _) (V "l" _) _) _) _), + parseMatch term + "case1 t return A of { 'x ⇒ p; 'y ⇒ q; 'z ⇒ r }" + `(Case (PQ One _) (V "t" _) + (Unused _, V "A" _) + (CaseEnum [(PT "x" _, V "p" _), + (PT "y" _, V "q" _), + (PT "z" _, V "r" _)] _) _), + parseMatch term "caseω t return A of {}" + `(Case (PQ Any _) (V "t" _) (Unused _, V "A" _) (CaseEnum [] _) _), + parseMatch term "case# t return A of {}" + `(Case (PQ Any _) (V "t" _) (Unused _, V "A" _) (CaseEnum [] _) _), + parseMatch term "caseω n return A of { 0 ⇒ a; succ n' ⇒ b }" + `(Case (PQ Any _) (V "n" _) (Unused _, V "A" _) + (CaseNat (V "a" _) (PV "n'" _, PQ Zero _, Unused _, V "b" _) _) _), + parseMatch term "caseω n return ℕ of { succ _, 1.ih ⇒ ih; zero ⇒ 0; }" + `(Case (PQ Any _) (V "n" _) (Unused _, Nat _) + (CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" _) _) _), parseFails term "caseω n return A of { zero ⇒ a }", parseFails term "caseω n return ℕ of { succ ⇒ 5 }" ], "definitions" :- [ - 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" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"])) - (Pair (Tag "a") (Tag "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" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"])) - (Pair (Tag "a") (Tag "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" (Just $ TYPE 0) (Enum ["a", "b", "c"]) + parseMatch definition "defω x : {a} × {b} = ('a, 'b);" + `(MkPDef (PQ Any _) "x" + (Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _)) + (Pair (Tag "a" _) (Tag "b" _) _) _), + parseMatch definition "def# x : {a} ** {b} = ('a, 'b)" + `(MkPDef (PQ Any _) "x" + (Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _)) + (Pair (Tag "a" _) (Tag "b" _) _) _), + parseMatch definition "def ω.x : {a} × {b} = ('a, 'b)" + `(MkPDef (PQ Any _) "x" + (Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _)) + (Pair (Tag "a" _) (Tag "b" _) _) _), + parseMatch definition "def x : {a} × {b} = ('a, 'b)" + `(MkPDef (PQ Any _) "x" + (Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _)) + (Pair (Tag "a" _) (Tag "b" _) _) _), + parseMatch definition "def0 A : ★₀ = {a, b, c}" + `(MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) + (Enum ["a", "b", "c"] _) _) ], "top level" :- [ - 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]"}, + parseMatch input "def0 A : ★₀ = {}; def0 B : ★₁ = A;" + `([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _, + PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" _) _]), + parseMatch input "def0 A : ★₀ = {} def0 B : ★₁ = A" $ + `([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _, + PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" _) _]), + note "empty input", + parsesAs input "" [], parseFails input ";;;;;;;;;;;;;;;;;;;;;;;;;;", - parsesAs input "namespace a {}" [PD $ PNs $ MkPNamespace [< "a"] []], - parsesAs input "namespace a.b.c {}" - [PD $ PNs $ MkPNamespace [< "a", "b", "c"] []], - parsesAs input "namespace a {namespace b {}}" - [PD $ PNs $ MkPNamespace [< "a"] [PNs $ MkPNamespace [< "b"] []]], - parsesAs input "namespace a {def x = 't ∷ {t}}" - [PD $ PNs $ MkPNamespace [< "a"] - [PDef $ MkPDef Any "x" Nothing (Tag "t" :# Enum ["t"])]], - parsesAs input "namespace a {def x = 't ∷ {t}} def y = a.x" - [PD $ PNs $ MkPNamespace [< "a"] - [PDef $ MkPDef Any "x" Nothing (Tag "t" :# Enum ["t"])], - PD $ PDef $ MkPDef Any "y" Nothing (V $ MakePName [< "a"] "x")], - parsesAs input #" load "a.quox"; def b = a.b "# - [PLoad "a.quox", - PD $ PDef $ MkPDef Any "b" Nothing (V $ MakePName [< "a"] "b")] + parseMatch input "namespace a {}" + `([PD $ PNs $ MkPNamespace [< "a"] [] _]), + parseMatch input "namespace a.b.c {}" + `([PD $ PNs $ MkPNamespace [< "a", "b", "c"] [] _]), + parseMatch input "namespace a {namespace b {}}" + `([PD $ PNs $ MkPNamespace [< "a"] [PNs $ MkPNamespace [< "b"] [] _] _]), + parseMatch input "namespace a {def x = 't ∷ {t}}" + `([PD $ PNs $ MkPNamespace [< "a"] + [PDef $ MkPDef (PQ Any _) "x" Nothing + (Ann (Tag "t" _) (Enum ["t"] _) _) _] _]), + parseMatch input "namespace a {def x = 't ∷ {t}} def y = a.x" + `([PD $ PNs $ MkPNamespace [< "a"] + [PDef $ MkPDef (PQ Any _) "x" Nothing + (Ann (Tag "t" _) (Enum ["t"] _) _) _] _, + PD $ PDef $ MkPDef (PQ Any _) "y" Nothing + (V (MakePName [< "a"] "x") _) _]), + parseMatch input #" load "a.quox"; def b = a.b "# + `([PLoad "a.quox" _, + PD $ PDef $ MkPDef (PQ Any _) "b" Nothing + (V (MakePName [< "a"] "b") _) _]) ] ]