diff options
Diffstat (limited to 'src/Inky/Parser.idr')
| -rw-r--r-- | src/Inky/Parser.idr | 698 |
1 files changed, 489 insertions, 209 deletions
diff --git a/src/Inky/Parser.idr b/src/Inky/Parser.idr index 1ad48d8..c44e7bd 100644 --- a/src/Inky/Parser.idr +++ b/src/Inky/Parser.idr @@ -1,21 +1,27 @@ module Inky.Parser +import public Data.List.Quantifiers +import public Data.Nat + import Control.WellFounded import Data.Bool +import Data.DPair import Data.List -import Data.List.Elem import Data.List1 -import Data.Nat import Data.So +import Data.String.Extra import Inky.Context +import Inky.Thinning import Text.Lexer +export +Interpolation Bounds where + interpolate bounds = "\{show (1 + bounds.startLine)}:\{show bounds.startCol}--\{show (1 + bounds.endLine)}:\{show bounds.endCol}" -- Parser Expressions ---------------------------------------------------------- -export -infixl 3 <**>, **>, <** -infixr 2 <||> +export infixl 3 <**>, **>, <** +export infixr 2 <||> public export linUnless : Bool -> Context a -> Context a @@ -23,124 +29,272 @@ linUnless False ctx = [<] linUnless True ctx = ctx public export -data Parser : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> Type -> Type where - Var : (f : a -> b) -> Var free (nil, a) -> Parser i nil locked free b - Fail : (msg : String) -> Parser i False locked free a - Empty : (x : a) -> Parser i True locked free a - Lit : (text : i) -> (x : String -> a) -> Parser i False locked free a - (<**>) : - {nil1, nil2 : Bool} -> - Parser i nil1 locked free (a -> b) -> - Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) a -> - Parser i (nil1 && nil2) locked free b - (<|>) : - {nil1, nil2 : Bool} -> - Parser i nil1 locked free a -> Parser i nil2 locked free a -> - So (not (nil1 && nil2)) => - Parser i (nil1 || nil2) locked free a +linUnlessLin : (0 a : Type) -> (b : Bool) -> linUnless {a} b [<] = [<] +linUnlessLin a False = Refl +linUnlessLin a True = Refl + +public export +data Parser : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> Type -> Type + +public export +data ParserChain : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> List Type -> Type + +data Parser where + Var : Var free (nil, a) -> Parser i nil locked free a + Lit : (text : i) -> Parser i False locked free String + Seq : + ParserChain i nil locked free as -> + Parser i nil locked free (HList as) + OneOf : + {nils : List Bool} -> + All (\nil => Parser i nil locked free a) nils -> + {auto 0 prf : length (filter Basics.id nils) `LTE` 1} -> + Parser i (any Basics.id nils) locked free a Fix : (0 x : String) -> - (f : a -> b) -> Parser i nil (locked :< (x :- (nil, a))) free a -> - Parser i nil locked free b + Parser i nil locked free a + Map : (a -> b) -> Parser i nil locked free a -> Parser i nil locked free b + WithBounds : Parser i nil locked free a -> Parser i nil locked free (WithBounds a) + +data ParserChain where + Nil : ParserChain i True locked free [] + (::) : + {nil1, nil2 : Bool} -> + Parser i nil1 locked free a -> + ParserChain i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) as -> + ParserChain i (nil1 && nil2) locked free (a :: as) %name Parser p, q +%name ParserChain ps, qs + +-- Weakening ------------------------------------------------------------------- public export -Functor (Parser i nil locked free) where - map f (Var g x) = Var (f . g) x - map f (Fail msg) = Fail msg - map f (Empty x) = Empty (f x) - map f (Lit text g) = Lit text (f . g) - map f ((<**>) {nil1 = True} p q) = map (f .) p <**> q - map f ((<**>) {nil1 = False} p q) = map (f .) p <**> q - map f (p <|> q) = map f p <|> map f q - map f (Fix x g p) = Fix x (f . g) p +rename : + locked1 `Thins` locked2 -> + free1 `Thins` free2 -> + {auto len : Length locked2} -> + Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a +public export +renameChain : + locked1 `Thins` locked2 -> + free1 `Thins` free2 -> + {auto len : Length locked2} -> + ParserChain i nil locked1 free1 a -> ParserChain i nil locked2 free2 a +public export +renameAll : + locked1 `Thins` locked2 -> + free1 `Thins` free2 -> + {auto len : Length locked2} -> + All.All (\nil => Parser i nil locked1 free1 a) nils -> + All.All (\nil => Parser i nil locked2 free2 a) nils + +rename f g (Var i) = Var (index g i) +rename f g (Lit text) = Lit text +rename f g (Seq ps) = Seq (renameChain f g ps) +rename f g (OneOf ps) = OneOf (renameAll f g ps) +rename f g (Fix x p) = Fix x (rename (Keep f) g p) +rename f g (Map h p) = Map h (rename f g p) +rename f g (WithBounds p) = WithBounds (rename f g p) + +renameChain f g [] = [] +renameChain f g ((::) {nil1 = False} p ps) = rename f g p :: renameChain Id (append g f) ps +renameChain f g ((::) {nil1 = True} p ps) = rename f g p :: renameChain f g ps + +renameAll f g [] = [] +renameAll f g (p :: ps) = rename f g p :: renameAll f g ps public export -Applicative (Parser i True locked free) where - pure = Empty - (<*>) = (<**>) +weaken : + (len1 : Length free2) -> + {auto len2 : Length locked} -> + Parser i nil (free2 ++ locked) free1 a -> Parser i nil locked (free1 ++ free2) a +public export +weakenChain : + (len1 : Length free2) -> + {auto len2 : Length locked} -> + ParserChain i nil (free2 ++ locked) free1 a -> ParserChain i nil locked (free1 ++ free2) a +public export +weakenAll : + (len1 : Length free2) -> + {auto len2 : Length locked} -> + All.All (\nil => Parser i nil (free2 ++ locked) free1 a) nils -> + All.All (\nil => Parser i nil locked (free1 ++ free2) a) nils + +weaken len1 (Var x) = Var (wknL x) +weaken len1 (Lit text) = Lit text +weaken len1 (Seq ps) = Seq (weakenChain len1 ps) +weaken len1 (OneOf ps) = OneOf (weakenAll len1 ps) +weaken len1 (Fix x p) = Fix x (weaken len1 p) +weaken len1 (Map f p) = Map f (weaken len1 p) +weaken len1 (WithBounds p) = WithBounds (weaken len1 p) + +weakenChain len1 [] = [] +weakenChain len1 ((::) {nil1 = False} p ps) = weaken len1 p :: renameChain Id (assoc len2) ps +weakenChain len1 ((::) {nil1 = True} p ps) = weaken len1 p :: weakenChain len1 ps + +weakenAll len1 [] = [] +weakenAll len1 (p :: ps) = weaken len1 p :: weakenAll len1 ps -- Typing ---------------------------------------------------------------------- -export +-- Lists are sufficient, as we assume each symbol appears once. +-- TODO: switch to some efficient tree? + +public export peek : (env : All (const (List i)) free) -> Parser i nil locked free a -> List i -peek env (Var f x) = indexAll x env -peek env (Fail msg) = [] -peek env (Empty x) = [] -peek env (Lit text x) = [text] -peek env ((<**>) {nil1 = False} p q) = peek env p -peek env ((<**>) {nil1 = True} p q) = peek env p ++ peek env q -peek env (p <|> q) = peek env p ++ peek env q -peek env (Fix x f p) = peek env p +public export +peekChain : + (env : All (const (List i)) free) -> + ParserChain i nil locked free a -> List i +public export +peekAll : + (env : All (const (List i)) free) -> + All.All (\nil => Parser i nil locked free a) nils -> + All.All (const $ List i) nils -export +peek env (Var x) = indexAll x env +peek env (Lit text) = [text] +peek env (Seq ps) = peekChain env ps +peek env (OneOf ps) = concat (forget $ peekAll env ps) +peek env (Fix x p) = peek env p +peek env (Map f p) = peek env p +peek env (WithBounds p) = peek env p + +peekChain env [] = [] +peekChain env ((::) {nil1 = False} p ps) = peek env p +peekChain env ((::) {nil1 = True} p ps) = peek env p ++ peekChain env ps + +peekAll env [] = [] +peekAll env (p :: ps) = peek env p :: peekAll env ps + +public export follow : (penv1 : All (const (List i)) locked) -> (penv2 : All (const (List i)) free) -> (fenv1 : All (const (List i)) locked) -> (fenv2 : All (const (List i)) free) -> Parser i nil locked free a -> List i -follow penv1 penv2 fenv1 fenv2 (Var f x) = indexAll x fenv2 -follow penv1 penv2 fenv1 fenv2 (Fail msg) = empty -follow penv1 penv2 fenv1 fenv2 (Empty x) = empty -follow penv1 penv2 fenv1 fenv2 (Lit text x) = empty -follow penv1 penv2 fenv1 fenv2 ((<**>) {nil1 = False} p q) = - follow [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) q -follow penv1 penv2 fenv1 fenv2 ((<**>) {nil1 = True} p q) = - peek penv2 q ++ - follow penv1 penv2 fenv1 fenv2 p ++ - follow penv1 penv2 fenv1 fenv2 q -follow penv1 penv2 fenv1 fenv2 (p <|> q) = - follow penv1 penv2 fenv1 fenv2 p ++ - follow penv1 penv2 fenv1 fenv2 q -follow penv1 penv2 fenv1 fenv2 (Fix x f p) = +public export +followChain : + (penv1 : All (const (List i)) locked) -> + (penv2 : All (const (List i)) free) -> + (fenv1 : All (const (List i)) locked) -> + (fenv2 : All (const (List i)) free) -> + ParserChain i nil locked free a -> List i +public export +followAll : + (penv1 : All (const (List i)) locked) -> + (penv2 : All (const (List i)) free) -> + (fenv1 : All (const (List i)) locked) -> + (fenv2 : All (const (List i)) free) -> + All.All (\nil => Parser i nil locked free a) nils -> List i + +follow penv1 penv2 fenv1 fenv2 (Var x) = indexAll x fenv2 +follow penv1 penv2 fenv1 fenv2 (Lit text) = [] +follow penv1 penv2 fenv1 fenv2 (Seq ps) = followChain penv1 penv2 fenv1 fenv2 ps +follow penv1 penv2 fenv1 fenv2 (OneOf ps) = followAll penv1 penv2 fenv1 fenv2 ps +follow penv1 penv2 fenv1 fenv2 (Fix x p) = -- Conjecture: The fix point converges after one step -- Proof: -- - we always add information -- - no step depends on existing information follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- empty)) fenv2 p +follow penv1 penv2 fenv1 fenv2 (Map f p) = follow penv1 penv2 fenv1 fenv2 p +follow penv1 penv2 fenv1 fenv2 (WithBounds p) = follow penv1 penv2 fenv1 fenv2 p + +followChain penv1 penv2 fenv1 fenv2 [] = [] +followChain penv1 penv2 fenv1 fenv2 ((::) {nil1 = False, nil2} p ps) = + (if nil2 + then peekChain (penv2 ++ penv1) ps ++ follow penv1 penv2 fenv1 fenv2 p + else []) ++ + followChain [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ps +followChain penv1 penv2 fenv1 fenv2 ((::) {nil1 = True, nil2} p ps) = + (if nil2 + then peekChain penv2 ps ++ follow penv1 penv2 fenv1 fenv2 p + else []) ++ + followChain penv1 penv2 fenv1 fenv2 ps + +followAll penv1 penv2 fenv1 fenv2 [] = [] +followAll penv1 penv2 fenv1 fenv2 (p :: ps) = + follow penv1 penv2 fenv1 fenv2 p ++ + followAll penv1 penv2 fenv1 fenv2 ps -export -WellTyped : - Eq i => - (penv1 : All (const (List i)) locked) -> - (penv2 : All (const (List i)) free) -> - (fenv1 : All (const (List i)) locked) -> - (fenv2 : All (const (List i)) free) -> - Parser i nil locked free a -> Type -WellTyped penv1 penv2 fenv1 fenv2 (Var f x) = () -WellTyped penv1 penv2 fenv1 fenv2 (Fail msg) = () -WellTyped penv1 penv2 fenv1 fenv2 (Empty x) = () -WellTyped penv1 penv2 fenv1 fenv2 (Lit text x) = () -WellTyped penv1 penv2 fenv1 fenv2 ((<**>) {nil1 = False} p q) = - let set1 = follow penv1 penv2 fenv1 fenv2 p in - let set2 = peek (penv2 ++ penv1) q in - ( WellTyped penv1 penv2 fenv1 fenv2 p - , WellTyped [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) q - , So (not $ any (`elem` set2) set1) - ) -WellTyped penv1 penv2 fenv1 fenv2 ((<**>) {nil1 = True} p q) = - let set1 = follow penv1 penv2 fenv1 fenv2 p in - let set2 = peek penv2 q in - ( WellTyped penv1 penv2 fenv1 fenv2 p - , WellTyped penv1 penv2 fenv1 fenv2 q - , So (not $ any (`elem` set2) set1) - ) -WellTyped penv1 penv2 fenv1 fenv2 (p <|> q) = - let set1 = peek penv2 p in - let set2 = peek penv2 q in - ( WellTyped penv1 penv2 fenv1 fenv2 p - , WellTyped penv1 penv2 fenv1 fenv2 q - , So (not $ any (`elem` set2) set1) - ) -WellTyped penv1 penv2 fenv1 fenv2 (Fix x f p) = - let fst = peek penv2 p in - let flw = follow (penv1 :< (x :- fst)) penv2 (fenv1 :< (x :- empty)) fenv2 p in - WellTyped (penv1 :< (x :- fst)) penv2 (fenv1 :< (x :- flw)) fenv2 p +public export +all' : (a -> Bool) -> List a -> Bool +all' f [] = True +all' f (x :: xs) = f x && all' f xs + +allTrue : (xs : List a) -> all' (const True) xs = True +allTrue [] = Refl +allTrue (x :: xs) = allTrue xs + +public export +disjoint : Eq a => List (List a) -> Bool +disjoint [] = True +disjoint (xs :: xss) = all' (\ys => all' (\x => not (x `elem` ys)) xs) xss && disjoint xss + +namespace WellTyped + public export + wellTyped : + (e : Eq i) -> + (penv1 : All (const (List i)) locked) -> + (penv2 : All (const (List i)) free) -> + (fenv1 : All (const (List i)) locked) -> + (fenv2 : All (const (List i)) free) -> + Parser i nil locked free a -> + Bool + public export + wellTypedChain : + (e : Eq i) -> + (penv1 : All (const (List i)) locked) -> + (penv2 : All (const (List i)) free) -> + (fenv1 : All (const (List i)) locked) -> + (fenv2 : All (const (List i)) free) -> + ParserChain i nil locked free a -> + Bool + public export + allWellTyped : + (e : Eq i) -> + (penv1 : All (const (List i)) locked) -> + (penv2 : All (const (List i)) free) -> + (fenv1 : All (const (List i)) locked) -> + (fenv2 : All (const (List i)) free) -> + All.All (\nil => Parser i nil locked free a) nils -> + Bool + + wellTyped e penv1 penv2 fenv1 fenv2 (Var i) = True + wellTyped e penv1 penv2 fenv1 fenv2 (Lit txt) = True + wellTyped e penv1 penv2 fenv1 fenv2 (Seq ps) = wellTypedChain e penv1 penv2 fenv1 fenv2 ps + wellTyped e penv1 penv2 fenv1 fenv2 (OneOf {nils, prf} ps) = + disjoint (forget $ peekAll penv2 ps) && allWellTyped e penv1 penv2 fenv1 fenv2 ps + wellTyped e penv1 penv2 fenv1 fenv2 (Fix x p) = + wellTyped e + (penv1 :< (x :- peek penv2 p)) + penv2 + (fenv1 :< (x :- follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- [])) fenv2 p)) + fenv2 + p + wellTyped e penv1 penv2 fenv1 fenv2 (Map f p) = wellTyped e penv1 penv2 fenv1 fenv2 p + wellTyped e penv1 penv2 fenv1 fenv2 (WithBounds p) = wellTyped e penv1 penv2 fenv1 fenv2 p + + wellTypedChain e penv1 penv2 fenv1 fenv2 [] = True + wellTypedChain e penv1 penv2 fenv1 fenv2 ((::) {nil1 = False} p ps) = + disjoint [follow penv1 penv2 fenv1 fenv2 p, peekChain (penv2 ++ penv1) ps] && + wellTyped e penv1 penv2 fenv1 fenv2 p && + wellTypedChain e [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ps + wellTypedChain e penv1 penv2 fenv1 fenv2 ((::) {nil1 = True} p ps) = + disjoint [follow penv1 penv2 fenv1 fenv2 p, peekChain penv2 ps] && + wellTyped e penv1 penv2 fenv1 fenv2 p && + wellTypedChain e penv1 penv2 fenv1 fenv2 ps + + allWellTyped e penv1 penv2 fenv1 fenv2 [] = True + allWellTyped e penv1 penv2 fenv1 fenv2 (p :: ps) = + wellTyped e penv1 penv2 fenv1 fenv2 p && + allWellTyped e penv1 penv2 fenv1 fenv2 ps -- Parsing Function ------------------------------------------------------------ @@ -168,8 +322,10 @@ wknSmallerL (Strict prf) _ = ofSmaller prf wknSmallerL (Lax prf) _ = Lax prf wknSmallerR : (b1 : Bool) -> SmallerX b2 xs ys -> SmallerX (b1 || b2) xs ys -wknSmallerR b1 (Strict prf) = rewrite orFalseNeutral b1 in ofSmaller prf -wknSmallerR b1 (Lax prf) = rewrite orTrueTrue b1 in Lax prf +wknSmallerR b1 (Strict prf) = + if b1 then ofSmaller prf else ofSmaller prf +wknSmallerR b1 (Lax prf) = + if b1 then Lax prf else Lax prf forget : SmallerX b xs ys -> SmallerX True xs ys forget = wknSmallerR True @@ -180,6 +336,16 @@ toSmaller {xs = []} {ys = (y :: ys)} (Strict prf) = LTESucc LTEZero toSmaller {xs = (x :: xs)} {ys = []} (Strict prf) impossible toSmaller {xs = (x :: xs)} {ys = (y :: ys)} (Strict (LTESucc prf)) = LTESucc (toSmaller (Strict prf)) +anyCons : (b : Bool) -> (bs : List Bool) -> any Basics.id (b :: bs) = b || any Basics.id bs +anyCons b [] = sym (orFalseNeutral b) +anyCons b (b' :: bs) = + trans (anyCons (b || b') bs) $ + trans (sym $ orAssociative b b' (any id bs)) + (cong (b ||) (sym $ anyCons b' bs)) + +anyTrue : (bs : List Bool) -> any Basics.id (True :: bs) = True +anyTrue = anyCons True + -- Return Type namespace M @@ -203,39 +369,146 @@ namespace M wknR b1 (Err msg) = Err msg wknR b1 (Ok res ys prf) = Ok res ys (wknSmallerR b1 prf) + export + anyL : + (b : Bool) -> {0 bs : List Bool} -> + M xs (any Basics.id bs) a -> M xs (any Basics.id (b :: bs)) a + anyL b m = rewrite anyCons b bs in wknR b m + + export + anyR : (bs : List Bool) -> M xs b a -> M xs (any Basics.id (b :: bs)) a + anyR bs m = rewrite anyCons b bs in wknL m (any id bs) + -- The Big Function +data FirstNil : List Bool -> Type where + Here : FirstNil (True :: bs) + There : FirstNil bs -> FirstNil (False :: bs) + +findNil : (nils : List Bool) -> Maybe (FirstNil nils) +findNil [] = Nothing +findNil (False :: bs) = There <$> findNil bs +findNil (True :: bs) = Just Here + +memberOf : Eq a => (x : a) -> All.All (const $ List a) xs -> Maybe (Any (const ()) xs) +memberOf x [] = Nothing +memberOf x (xs :: xss) = + if x `elem` xs + then Just (Here ()) + else There <$> (x `memberOf` xss) + parser : - Eq i => Interpolation i => + (e : Eq i) => Interpolation i => (p : Parser i nil locked free a) -> (penv1 : _) -> (penv2 : _) -> (fenv1 : _) -> (fenv2 : _) -> - {auto 0 wf : WellTyped penv1 penv2 fenv1 fenv2 p} -> + {auto 0 wf : So (wellTyped e penv1 penv2 fenv1 fenv2 p)} -> (xs : List (WithBounds (Token i))) -> All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked -> All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free -> M xs nil a -parser (Var f x) penv1 penv2 fenv1 fenv2 xs env1 env2 = - f <$> indexAll x env2 xs (Lax reflexive) -parser (Fail msg) penv1 penv2 fenv1 fenv2 xs env1 env2 = - Err msg -parser (Empty x) penv1 penv2 fenv1 fenv2 xs env1 env2 = - Ok x xs (Lax reflexive) -parser (Lit text f) penv1 penv2 fenv1 fenv2 xs env1 env2 = +parserChain : + (e : Eq i) => Interpolation i => + (ps : ParserChain i nil locked free as) -> + (penv1 : _) -> + (penv2 : _) -> + (fenv1 : _) -> + (fenv2 : _) -> + {auto 0 wf : So (wellTypedChain e penv1 penv2 fenv1 fenv2 ps)} -> + (xs : List (WithBounds (Token i))) -> + All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked -> + All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free -> + M xs nil (HList as) +parserNil : + (e : Eq i) => Interpolation i => + (at : FirstNil nils) -> + (ps : All (\nil => Parser i nil locked free a) nils) -> + (penv1 : _) -> + (penv2 : _) -> + (fenv1 : _) -> + (fenv2 : _) -> + {auto 0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)} -> + (xs : List (WithBounds (Token i))) -> + All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked -> + All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free -> + M xs (any Basics.id nils) a +parserOneOf : + (e : Eq i) => Interpolation i => + {nils : List Bool} -> + (at : Any (const ()) nils) -> + (ps : All (\nil => Parser i nil locked free a) nils) -> + (penv1 : _) -> + (penv2 : _) -> + (fenv1 : _) -> + (fenv2 : _) -> + {auto 0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)} -> + (xs : List1 (WithBounds (Token i))) -> + All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys (forget xs)) -> uncurry (M ys) x) locked -> + All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys (forget xs)) -> uncurry (M ys) x) free -> + M (forget xs) (any Basics.id nils) a + +parser (Var x) penv1 penv2 fenv1 fenv2 xs env1 env2 = + indexAll x env2 xs (Lax reflexive) +parser (Lit text) penv1 penv2 fenv1 fenv2 xs env1 env2 = case xs of [] => Err "expected \{text}, got end of file" y :: ys => if y.val.kind == text - then Ok (f y.val.text) ys (Strict reflexive) - else Err "\{show y.bounds}: expected \{text}, got \{y.val.kind}" -parser ((<**>) {nil1 = False, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 = + then Ok y.val.text ys (Strict reflexive) + else Err "\{y.bounds}: expected \{text}, got \{y.val.kind}" +parser (Seq ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = + parserChain ps penv1 penv2 fenv1 fenv2 xs env1 env2 +parser (OneOf {nils} ps) penv1 penv2 fenv1 fenv2 [] env1 env2 {wf} = + let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in + case findNil nils of + Nothing => Err "unexpected end of input" + Just at => parserNil at ps penv1 penv2 fenv1 fenv2 [] env1 env2 +parser (OneOf {nils} ps) penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 {wf = wf} = + let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in + let sets = peekAll penv2 ps in + case x.val.kind `memberOf` sets of + Just at => parserOneOf at ps penv1 penv2 fenv1 fenv2 (x ::: xs) env1 env2 + Nothing => case findNil nils of + Nothing => + Err + "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") $ concat $ forget sets}; got \{x.val.kind}" + Just at => parserNil at ps penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 +parser (Fix {a, nil} x p) penv1 penv2 fenv1 fenv2 xs env1 env2 = + let f = parser p _ _ _ _ {wf} in + let + res : M xs nil a + res = + sizeInd {P = \ys => (0 prf : SmallerX True ys xs) -> M ys nil a} + (\ys, rec, lte => + f ys + ( mapProperty (\f, zs, 0 prf => f zs $ transX prf lte) env1 + :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte))) + ) + (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2)) + xs + (Lax reflexive) + in + res +parser (Map f p) penv1 penv2 fenv1 fenv2 xs env1 env2 = + f <$> parser p penv1 penv2 fenv1 fenv2 xs env1 env2 +parser (WithBounds p) penv1 penv2 fenv1 fenv2 xs env1 env2 = + case xs of + [] => irrelevantBounds <$> parser p penv1 penv2 fenv1 fenv2 [] env1 env2 + (x :: xs) => + (\y => MkBounded y x.isIrrelevant x.bounds) <$> + parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 + +parserChain [] penv1 penv2 fenv1 fenv2 xs env1 env2 = Ok [] xs (Lax reflexive) +parserChain ((::) {nil1 = False, nil2} p ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = + let 0 wfs = soAnd wf in + let 0 wfs' = soAnd (snd wfs) in case parser p penv1 penv2 fenv1 fenv2 xs env1 env2 of Err msg => Err msg - Ok f ys lt => + Ok x ys lt => case - parser q [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) + parserChain ps [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ys [<] ( mapProperty (\f, zs, 0 prf => f zs $ forget $ transX prf lt) env2 @@ -243,122 +516,102 @@ parser ((<**>) {nil1 = False, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 = ) of Err msg => Err msg - Ok x zs prf => Ok (f x) zs (rewrite sym $ andFalseFalse nil2 in transX prf lt) -parser ((<**>) {nil1 = True, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 = + Ok y zs prf => Ok (x :: y) zs (rewrite sym $ andFalseFalse nil2 in transX prf lt) +parserChain ((::) {nil1 = True, nil2} p ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = + let 0 wfs = soAnd wf in + let 0 wfs' = soAnd (snd wfs) in case parser p penv1 penv2 fenv1 fenv2 xs env1 env2 of Err msg => Err msg - Ok f ys lte => + Ok x ys lte => case - parser q penv1 penv2 fenv1 fenv2 + parserChain ps penv1 penv2 fenv1 fenv2 ys (mapProperty (\f, zs, prf => f zs $ transX prf lte) env1) (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2) of Err msg => Err msg - Ok x zs prf => Ok (f x) zs (rewrite sym $ andTrueNeutral nil2 in transX prf lte) -parser ((<|>) {nil1, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 = - case xs of - [] => - if nil1 - then parser p penv1 penv2 fenv1 fenv2 [] env1 env2 - else if nil2 - then parser q penv1 penv2 fenv1 fenv2 [] env1 env2 - else Err "unexpected end of input" - x :: xs => - if elem x.val.kind (peek penv2 p) - then wknL (parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2) nil2 - else if elem x.val.kind (peek penv2 q) - then wknR nil1 (parser q penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2) - else if nil1 - then parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 - else if nil2 - then parser q penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 - else Err "\{show x.bounds}: unexpected \{x.val.kind}" -parser (Fix {a, b, nil} x f p) penv1 penv2 fenv1 fenv2 xs env1 env2 = - let g = parser p _ _ _ _ {wf} in - let - res : M xs nil a - res = - sizeInd {P = \ys => (0 prf : SmallerX True ys xs) -> M ys nil a} - (\ys, rec, lte => - g ys - ( mapProperty (\f, zs, 0 prf => f zs $ transX prf lte) env1 - :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte))) - ) - (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2)) - xs - (Lax reflexive) - in - f <$> res + Ok y zs prf => Ok (x :: y) zs (rewrite sym $ andTrueNeutral nil2 in transX prf lte) + +parserNil {nils = True :: nils} Here (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = + let 0 wfs = soAnd wf in + rewrite anyTrue nils in + parser p penv1 penv2 fenv1 fenv2 xs env1 env2 +parserNil (There at) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = + let 0 wfs = soAnd {a = wellTyped e penv1 penv2 fenv1 fenv2 p} wf in + parserNil at ps penv1 penv2 fenv1 fenv2 xs env1 env2 + +parserOneOf {nils = nil :: nils} (Here ()) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = + let 0 wfs = soAnd wf in + anyR nils (parser p penv1 penv2 fenv1 fenv2 (forget xs) env1 env2) +parserOneOf {nils = nil :: nils} (There at) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = + let 0 wfs = soAnd {a = wellTyped e penv1 penv2 fenv1 fenv2 p} wf in + anyL nil (parserOneOf at ps penv1 penv2 fenv1 fenv2 xs env1 env2) export parse : - Eq i => Interpolation i => + (e : Eq i) => Interpolation i => (p : Parser i nil [<] [<] a) -> - {auto 0 wf : WellTyped [<] [<] [<] [<] p} -> + {auto 0 wf : So (wellTyped e [<] [<] [<] [<] p)} -> (xs : List (WithBounds (Token i))) -> M xs nil a parse p xs = parser p [<] [<] [<] [<] xs [<] [<] --- Weakening ------------------------------------------------------------------- +-- Functor --------------------------------------------------------------------- public export -rename : - (len1 : Length locked1) -> - (len2 : Length locked2) -> - (forall x. Var locked1 x -> Var locked2 x) -> - (forall x. Var free1 x -> Var free2 x) -> - Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a -rename len1 len2 ren1 ren2 (Var f x) = Var f (ren2 x) -rename len1 len2 ren1 ren2 (Fail msg) = Fail msg -rename len1 len2 ren1 ren2 (Empty x) = Empty x -rename len1 len2 ren1 ren2 (Lit text x) = Lit text x -rename len1 len2 ren1 ren2 ((<**>) {nil1 = False} p q) = - rename len1 len2 ren1 ren2 p <**> - rename Z Z id (either (wknL {len = len2} . ren2) (wknR . ren1) . split) q -rename len1 len2 ren1 ren2 ((<**>) {nil1 = True} p q) = - rename len1 len2 ren1 ren2 p <**> rename len1 len2 ren1 ren2 q -rename len1 len2 ren1 ren2 (p <|> q) = - rename len1 len2 ren1 ren2 p <|> rename len1 len2 ren1 ren2 q -rename len1 len2 ren1 ren2 (Fix x f p) = - Fix x f (rename (S len1) (S len2) (lift {len = S Z} ren1) ren2 p) +(++) : + {nil2 : Bool} -> + ParserChain i nil1 locked free as -> + ParserChain i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) bs -> + ParserChain i (nil1 && nil2) locked free (as ++ bs) +[] ++ qs = qs +((::) {nil1 = False, nil2} p ps) ++ qs = + p :: + ( ps + ++ rewrite linUnlessLin (Bool, Type) nil2 in + rewrite linUnlessLin (Bool, Type) (not nil2) in + qs) +((::) {nil1 = True, nil2} p ps) ++ qs = p :: (ps ++ qs) public export -weaken : - (len1 : Length free2) -> - {auto len2 : Length locked} -> - Parser i nil (free2 ++ locked) free1 a -> Parser i nil locked (free1 ++ free2) a -weaken len1 (Var f x) = Var f (wknL x) -weaken len1 (Fail msg) = Fail msg -weaken len1 (Empty x) = Empty x -weaken len1 (Lit text x) = Lit text x -weaken len1 ((<**>) {nil1 = False} p q) = - weaken len1 p <**> - rename Z Z - id - ( either (wknL . wknL) (either (wknL . wknR) wknR . split) - . split {len = lengthAppend len1 len2} - ) - q -weaken len1 ((<**>) {nil1 = True} p q) = weaken len1 p <**> weaken len1 q -weaken len1 (p <|> q) = weaken len1 p <|> weaken len1 q -weaken len1 (Fix x f p) = Fix x f (weaken len1 p) - -public export -shift : - {auto len1 : Length locked1} -> - (len2 : Length locked2) -> - (len3 : Length free2) -> - Parser i nil locked1 free1 a -> Parser i nil (locked1 ++ locked2) (free1 ++ free2) a -shift len2 len3 = rename len1 (lengthAppend len1 len2) wknL wknL +(<**>) : + {nil1, nil2 : Bool} -> + Parser i nil1 locked free a -> + Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b -> + Parser i (nil1 && nil2) locked free (a, b) +p <**> Seq ps = Map (\(x :: xs) => (x, xs)) $ Seq (p :: ps) +-- HACK: andTrueNeutral isn't public, so do a full case split. +(<**>) {nil1 = True, nil2 = True} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] +(<**>) {nil1 = True, nil2 = False} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] +(<**>) {nil1 = False, nil2 = True} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] +(<**>) {nil1 = False, nil2 = False} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] + +public export +Functor (Parser i nil locked free) where + map f (Map g p) = Map (f . g) p + map f p = Map f p + +public export +Applicative (Parser i True locked free) where + pure x = map (const x) (Seq []) + p <*> q = map (\(f, x) => f x) (p <**> q) -- Combinator ------------------------------------------------------------------ public export +(<|>) : + {nil1, nil2 : Bool} -> + Parser i nil1 locked free a -> + Parser i nil2 locked free a -> + {auto 0 prf : length (filter Basics.id [nil1, nil2]) `LTE` 1} -> + Parser i (nil1 || nil2) locked free a +p <|> q = OneOf [p, q] + +public export (<||>) : {nil1, nil2 : Bool} -> Parser i nil1 locked free a -> Parser i nil2 locked free b -> - So (not (nil1 && nil2)) => + {auto 0 prf : length (filter Basics.id [nil1, nil2]) `LTE` 1} -> Parser i (nil1 || nil2) locked free (Either a b) p <||> q = Left <$> p <|> Right <$> q @@ -368,7 +621,7 @@ public export Parser i nil1 locked free a -> Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b -> Parser i (nil1 && nil2) locked free b -p **> q = (\_ => id) <$> p <**> q +p **> q = snd <$> (p <**> q) public export (<**) : @@ -376,11 +629,24 @@ public export Parser i nil1 locked free a -> Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b -> Parser i (nil1 && nil2) locked free a -p <** q = const <$> p <**> q +p <** q = fst <$> (p <**> q) public export match : TokenKind i => (kind : i) -> Parser i False locked free (TokType kind) -match kind = Lit kind (tokValue kind) +match kind = Map (tokValue kind) $ Lit kind + +public export +enclose : + {b1, b2, b3 : Bool} -> + (left : Parser i b1 locked free ()) -> + (right : + Parser i b3 + (linUnless b2 (linUnless b1 locked)) + ((free ++ linUnless (not b1) locked) ++ linUnless (not b2) (linUnless b1 locked)) + ()) -> + Parser i b2 (linUnless b1 locked) (free ++ linUnless (not b1) locked) a -> + Parser i (b1 && b2 && b3 && True) locked free a +enclose left right p = (\[_, x, _] => x) <$> Seq {as = [(), a, ()]} [left, p, right] public export option : Parser i False locked free a -> Parser i True locked free (Maybe a) @@ -392,15 +658,29 @@ plus : Parser i False locked free a -> Parser i False locked free (List1 a) plus p = - Fix "plus" id - ( (:::) <$> shift (S Z) Z p - <**> maybe [] forget <$> option (Var id (%% "plus"))) + Fix "plus" + ( uncurry (:::) + <$> (rename (Drop Id) Id p <**> maybe [] forget <$> option (Var $ %% "plus"))) public export star : {auto len : Length locked} -> Parser i False locked free a -> Parser i True locked free (List a) -star p = - Fix "star" id - (maybe [] id <$> option ((::) <$> shift (S Z) Z p <**> Var id (%% "star"))) +star p = maybe [] forget <$> option (plus p) + +public export +sepBy1 : + {auto len : Length locked} -> + (sep : Parser i False locked free ()) -> + Parser i False locked free a -> + Parser i False locked free (List1 a) +sepBy1 sep p = uncurry (:::) <$> (p <**> star (weaken len sep **> weaken len p)) + +public export +sepBy : + {auto len : Length locked} -> + (sep : Parser i False locked free ()) -> + Parser i False locked free a -> + Parser i True locked free (List a) +sepBy sep p = maybe [] forget <$> option (sepBy1 sep p) |