switch to TParsecT

TParsec.ipkg

@@ -12,6 +12,7 @@ modules = Relation.Indexed
 
         , TParsec
         , TParsec.Success
+        , TParsec.Result
         , TParsec.Types
         , TParsec.Combinators
         , TParsec.Combinators.Chars

src/Examples/Arithmetic.idr

@@ -56,11 +56,11 @@ mutual
 -- `Toks p` in the monad `mn` to produce respectively values of type `Expr`,
 -- `Term`, and `Factor`.
 
-record Language (p : Parameters) (mn : Type -> Type) (n : Nat) where
+record Language (mn : Type -> Type) (p : Parameters mn) (n : Nat) where
   constructor MkLanguage
-  _expr   : Parser p mn Expr n
-  _term   : Parser p mn Term n
-  _factor : Parser p mn Factor n
+  _expr   : Parser mn p Expr n
+  _term   : Parser mn p Term n
+  _factor : Parser mn p Factor n
 
 -- We are now ready to build a `Language toks mn n` for all `n` by recursion.
 -- We have a few constraints which arise directly from the combinators we are
@@ -70,12 +70,12 @@ record Language (p : Parameters) (mn : Type -> Type) (n : Nat) where
 -- In particular, this means that we can make sure that the first character
 -- of the input string is a specific `Char` e.g. '+'.
 
-language : (Alternative mn, Monad mn, Instrumented p mn, Inspect (Toks p) (Tok p), Eq (Tok p), Subset Char (Tok p)) => All (Language p mn)
+language : (Alternative mn, Monad mn, Inspect (Toks p) (Tok p), Eq (Tok p), Subset Char (Tok p)) => All (Language mn p)
 language {p} {mn} =
 
   -- The value of type `Language` is build as a fixpoint.
   -- We can use the variable `rec` bound here to perform a recursive call.
-  fix (Language p mn) $ \rec =>
+  fix (Language mn p) $ \rec =>
 
   -- We start by writing the parsers recognizing basic operations on numbers:
   -- * `alt` is used to take the union of two grammars
@@ -135,5 +135,5 @@ language {p} {mn} =
 -- `_expr Arithmetic.language` on `"1+3"` produces the abstract syntax tree
 -- `EAdd (EEmb (TEmb (FLit 1))) (TEmb (FLit 3))`. Which it does.
 
-test : parse {p = unInstr Char (SizedList Char)} {mn = Maybe} "1+3" (_expr Arithmetic.language)
+test : parseType {mn=TParsecU} {p=Types.chars} "1+3" (_expr Arithmetic.language)
 test = MkSingleton (EAdd (EEmb (TEmb (FLit 1))) (TEmb (FLit 3)))

src/Examples/NList.idr

@@ -11,7 +11,7 @@ NList a  Z    = a
 NList a (S n) = List (NList a n)
 
 Parser' : Type -> Nat -> Type
-Parser' = Parser (unInstr Char (SizedList Char)) Maybe
+Parser' = Parser TParsecU chars
 
 NList' : All (Parser' a) -> (n : Nat) -> All (Parser' (NList a n))
 NList' a  Z    = a
@@ -22,17 +22,17 @@ NList' a (S n) = parens $ map DList.toList (chainl1 (map wrap (NList' a n)) (cma
 nnats : (n : Nat) -> All (Parser' (NList Nat n))
 nnats = NList' decimalNat
 
-test : parse "((1,2,3),(4,5,6))" (nnats 2)
+test : parseType "((1,2,3),(4,5,6))" (nnats 2)
 test = MkSingleton [[1, 2, 3], [4, 5, 6]]
 
-test2 : parse "((1,2,3),(4,5,6),(7,8,9,10))" (nnats 2)
+test2 : parseType "((1,2,3),(4,5,6),(7,8,9,10))" (nnats 2)
 test2 = MkSingleton [[1, 2, 3], [4, 5, 6], [7, 8, 9, 10]]
 
-test3 : parse "((1),(2))" (nnats 2)
+test3 : parseType "((1),(2))" (nnats 2)
 test3 = MkSingleton [[1], [2]]
 
-test4 : parse "((1,2))" (nnats 2)
+test4 : parseType "((1,2))" (nnats 2)
 test4 = MkSingleton [[1, 2]]
 
-test5 : parse "(((1,2),(3,4)),((5,6),(7,8)))" (nnats 3)
+test5 : parseType "(((1,2),(3,4)),((5,6),(7,8)))" (nnats 3)
 test5 = MkSingleton [[[1, 2], [3, 4]], [[5, 6], [7, 8]]]

src/Examples/Parentheses.idr

@@ -29,14 +29,8 @@ Tokenizer PAR where
     toPAR ']' = [RSQU]
     toPAR _ = [] -- ignoring other characters as noise
 
-SizedInput PAR (SizedList PAR) where
-  sizedInput = MkSizedList
-
-Params : Parameters
-Params = unInstr PAR (SizedList PAR)
-
 Parser' : Type -> Nat -> Type
-Parser' = Parser Params Maybe
+Parser' = Parser TParsecU (sizedtok PAR)
 
 PAR' : All (Parser' ())
 PAR' = fix _ $ \rec => 
@@ -48,5 +42,5 @@ PAR' = fix _ $ \rec =>
 
 ---- test
 
-test : parse "hel[{(lo({((wor))ld})wan)t}som{e()[n]o}i(s)e]?" PAR'
+test : parseType "hel[{(lo({((wor))ld})wan)t}som{e()[n]o}i(s)e]?" PAR'
 test = MkSingleton ()

src/Examples/RegExp.idr

@@ -79,14 +79,8 @@ Tokenizer TOK where
     toTOKs ('|' :: cs)        = OR     :: toTOKs cs
     toTOKs (c :: cs)          = CHAR c :: toTOKs cs
 
-SizedInput TOK (SizedList TOK) where
-  sizedInput = MkSizedList    
-
-Params : Parameters
-Params = unInstr TOK (SizedList TOK)
-
 Parser' : Type -> Nat -> Type
-Parser' = Parser Params Maybe
+Parser' = Parser TParsecU (sizedtok TOK)
 
 -- workarounds for #4504
 exactTOK : TOK -> All (Parser' TOK)   
@@ -101,21 +95,21 @@ range = map (uncurry $ \c => maybe (Single c) (Interval c))
 
 regexp : All (Parser' RegExp)
 regexp = fix _ $ \rec => 
-           let parens   = between (exactTOK LPAR) (exactTOK RPAR)
-               parensm  = betweenm (exactTOK LPAR) (exactTOK RPAR)
-               ranges   = Combinators.app ((cmap Bracket (exactTOK OPEN)) `alt` (cmap (BracketNot . NEList.toList) (exactTOK NOPEN)))
-                              ((nelist range) `land` (exact CLOSE))
-               literals = Combinators.map (foldrf (Conj . literal) literal) (nelist (maybeTOK isCHAR))
-               base     = alts [ranges, cmap (BracketNot []) (exactTOK ANY), literals, parens rec]
-               star     = map (\(r,m) => maybe r (const $ Star r) m) (base `andopt` exact STAR)
-               disj     = chainr1 star (Disj `cmap` exactTOK OR)
+           let parens    = between (exactTOK LPAR) (exactTOK RPAR)
+               parensopt = betweenopt (exactTOK LPAR) (exactTOK RPAR)
+               ranges    = Combinators.app ((cmap Bracket (exactTOK OPEN)) `alt` (cmap (BracketNot . NEList.toList) (exactTOK NOPEN)))
+                               ((nelist range) `land` (exact CLOSE))
+               literals  = Combinators.map (foldrf (Conj . literal) literal) (nelist (maybeTOK isCHAR))
+               base      = alts [ranges, cmap (BracketNot []) (exactTOK ANY), literals, parens rec]
+               star      = map (\(r,m) => maybe r (const $ Star r) m) (base `andopt` exact STAR)
+               disj      = chainr1 star (Disj `cmap` exactTOK OR)
               in 
-           map (foldr1 Conj) (nelist (parensm disj))
+           map (foldr1 Conj) (nelist (parensopt disj))
 
 ---- test
 
 TestT : Type 
-TestT = parse "[a..zA..Z0..9-]*\\.agd(a|ai)" regexp
+TestT = parseType "[a..zA..Z0..9-]*\\.agd(a|ai)" regexp
 
 test : TestT
 test = MkSingleton (Conj (Star (Bracket (MkNEList (Interval 'a' 'z') [Interval 'A' 'Z', Interval '0' '9', Single '-']))) 

src/Examples/STLC.idr

@@ -39,7 +39,7 @@ import TParsec.Running
 -- Arithmetic example for a most-general-type approach).
 
 Parser' : Type -> Nat -> Type
-Parser' = Parser (unInstr Char (SizedList Char)) Maybe
+Parser' = Parser TParsecU chars
 
 -- Parsing Types
 -------------------------------------------------------------------------------
@@ -99,7 +99,7 @@ type =
 -- user gives a proof of `Singleton v`. The only such proof is `MkSingleton v`.
 
 Test : Type
-Test = parse "'a -> ('b -> 'c) -> 'd" type
+Test = parseType "'a -> ('b -> 'c) -> 'd" type
 
 test : Test
 test = MkSingleton (ARR (K "a") (ARR (ARR (K "b") (K "c")) (K "d")))
@@ -228,7 +228,7 @@ language = fix _ $ \rec =>
 -- produces the right output.
 
 Test2 : Type
-Test2 = parse "\\ x . (\\ y . y : 'a -> 'a) x" (val language)
+Test2 = parseType "\\ x . (\\ y . y : 'a -> 'a) x" (val language)
 
 test2 : Test2
 test2 = MkSingleton (Lam "x" (Emb (App (Cut (Lam "y" (Emb (Var "y"))) (ARR (K "a") (K "a")))

src/TParsec.idr

@@ -5,8 +5,8 @@ import public Relation.Indexed
 import public Induction.Nat
 import public Data.Inspect
 import public TParsec.Success
+import public TParsec.Result
 import public TParsec.Types
-import public TParsec.Instruments
 import public TParsec.Combinators
 import public TParsec.Combinators.Chars
 import public TParsec.Combinators.Numbers