From 1a7a84d29e2b2d49e96bd064e77fbb65cef2d3e1 Mon Sep 17 00:00:00 2001 From: Michael Morgan Date: Wed, 17 Jan 2018 15:01:46 -0600 Subject: [PATCH] inline upgradeRes in doParse --- libs/contrib/Text/Parser/Core.idr | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/libs/contrib/Text/Parser/Core.idr b/libs/contrib/Text/Parser/Core.idr index fa98255715..04c0f2dd39 100644 --- a/libs/contrib/Text/Parser/Core.idr +++ b/libs/contrib/Text/Parser/Core.idr @@ -235,20 +235,16 @@ shorter : (more : List tok) -> .(ys : List tok) -> shorter more [] = lteRefl shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs)) -upgradeRes : {c : Bool} -> {xs : List tok} -> - outerST -> - ParseResult innerST xs c ty -> - ParseResult outerST xs c (ty, innerST) -upgradeRes state (Failure com msg xs) = Failure com msg xs -upgradeRes state (EmptyRes inner com val xs) = EmptyRes state com (val, inner) xs -upgradeRes state (NonEmptyRes inner com val xs) = NonEmptyRes state com (val, inner) xs - doParse : {c : Bool} -> (state : st) -> (commit : Bool) -> (xs : List tok) -> (act : GrammarT st tok c ty) -> ParseResult st xs c ty doParse state com xs act with (sizeAccessible xs) - doParse state com xs (Run sub init) | sml = upgradeRes state (doParse init com xs sub | sml) + doParse state com xs (Run sub init) | sml + = case (doParse init com xs sub | sml) of + Failure com' msg xs' => Failure com' msg xs' + EmptyRes inner com' val xs' => EmptyRes state com' (val, inner) xs' + NonEmptyRes inner com' val xs' => NonEmptyRes state com' (val, inner) xs' doParse state com xs Get | sml = EmptyRes state com state xs doParse state com xs (Put newState) | sml = EmptyRes newState com () xs doParse state com xs (Empty val) | sml = EmptyRes state com val xs