mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-25 05:43:19 +03:00
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)
This commit is contained in:
parent
25843793c7
commit
b0d640fa55
@ -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"
|
||||
|
@ -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'
|
||||
|
@ -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
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user