From 1149000fb184c1d3863a4ad91f5da2d86a1e768b Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 17 Mar 2022 17:41:08 +0000 Subject: [PATCH] [ perf ] only normalise primitives on small strings on the RHS --- src/TTImp/Elab/App.idr | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 066c729b8..0b9f8578c 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -836,12 +836,13 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp boundSafe : Constant -> ElabMode -> Bool boundSafe _ (InLHS _) = True -- always need to expand on LHS - boundSafe (BI x) _ = abs x < 100 -- only do this for relatively small bounds. - -- Once it gets too big, we might be making the term - -- bigger than it would have been without evaluating! + -- only do this for relatively small bounds. + -- Once it gets too big, we might be making the term + -- bigger than it would have been without evaluating! + boundSafe (BI x) _ = abs x < 100 + boundSafe (Str str) _ = length str < 10 boundSafe _ _ = True - updateElabInfo : List Name -> ElabMode -> Name -> List RawImp -> ElabInfo -> Core ElabInfo -- If it's a primitive function applied to a constant on the LHS, treat it