From b0d640fa55d73d9884f2edb7dfebfe330bf768fe Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 8 Mar 2020 20:10:08 +0000 Subject: [PATCH] Some tiny updates Most importantly: Case operators should not be inlined indiscriminately, because that might duplicate work (e.g. via a variable pattern for the scrutinee, where the variable is used more than once) --- src/Compiler/Scheme/Common.idr | 5 ++++- src/TTImp/Elab/Case.idr | 1 - src/Text/Parser/Core.idr | 4 ++-- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index 28fe903..db3726a 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/src/Compiler/Scheme/Common.idr @@ -237,7 +237,10 @@ schConstant : (String -> String) -> Constant -> String schConstant _ (I x) = show x schConstant _ (BI x) = show x schConstant schString (Str x) = schString x -schConstant _ (Ch x) = "#\\" ++ cast x +schConstant _ (Ch x) + = if (the Int (cast x) >= 32 && the Int (cast x) < 127) + then "#\\" ++ cast x + else "(integer->char " ++ show (the Int (cast x)) ++ ")" schConstant _ (Db x) = show x schConstant _ WorldVal = "#f" schConstant _ IntType = "#t" diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index 17e48f7..ad04ca1 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -202,7 +202,6 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected = maybe (App fc applyEnv scrtm) (const applyEnv) splitOn - setFlag fc casen Inline let alts' = map (updateClause casen splitOn nest env) alts log 2 $ "Generated alts: " ++ show alts' diff --git a/src/Text/Parser/Core.idr b/src/Text/Parser/Core.idr index 2929b95..622a25e 100644 --- a/src/Text/Parser/Core.idr +++ b/src/Text/Parser/Core.idr @@ -31,7 +31,7 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where Grammar tok c1 a -> (a -> Grammar tok c2 b) -> Grammar tok (c1 || c2) b Alt : {c1, c2 : Bool} -> - Grammar tok c1 ty -> Grammar tok c2 ty -> + Grammar tok c1 ty -> Lazy (Grammar tok c2 ty) -> Grammar tok (c1 && c2) ty ||| Sequence two grammars. If either consumes some input, the sequence is @@ -69,7 +69,7 @@ join {c1 = True} p = SeqEat p id export (<|>) : {c1,c2 : Bool} -> Grammar tok c1 ty -> - Grammar tok c2 ty -> + Lazy (Grammar tok c2 ty) -> Grammar tok (c1 && c2) ty (<|>) = Alt