Make sure literals are normalise on LHS

The hack (optimisation?) to normalise integer literals when below some
threshold is fine on the RHS, but on the LHS causes problems since we
need them in normal form for pattern matching. Fixes #112

Makefile

@@ -47,7 +47,7 @@ endif
 export SCHEME
 
 
-.PHONY: all idris2-exec ${TARGET} support support-clean clean distclean
+.PHONY: all idris2-exec ${TARGET} testbin support support-clean clean distclean
 
 all: support ${TARGET} testbin libs
 

src/TTImp/Elab/App.idr

@@ -649,11 +649,12 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
     isPrimName (p :: ps) fn
         = dropNS fn == p || isPrimName ps fn
 
-    boundSafe : Constant -> Bool
-    boundSafe (BI x) = abs x < 100 -- only do this for relatively small bounds.
+    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!
-    boundSafe _ = True
+    boundSafe _ _ = True
 
     -- If the term is an application of a primitive conversion (fromInteger etc)
     -- and it's applied to a constant, fully normalise the term.
@@ -665,7 +666,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
         = if isPrimName prims !(getFullName n)
              then case reverse expargs of
                        (IPrimVal _ c :: _) =>
-                          if boundSafe c
+                          if boundSafe c (elabMode elabinfo)
                              then do defs <- get Ctxt
                                      tm <- normalise defs env (fst res)
                                      pure (tm, snd res)

tests/Main.idr

@@ -85,7 +85,7 @@ idrisTests
        -- Miscellaneous regressions
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
-       "reg015", "reg016", "reg017", "reg018", "reg019",
+       "reg015", "reg016", "reg017", "reg018", "reg019", "reg020",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008",

tests/Makefile

@@ -5,9 +5,7 @@ INTERACTIVE ?= --interactive
 test:
 	./build/exec/runtests $(IDRIS2) $(INTERACTIVE) --only $(only)
 
-testbin: build/exec/runtests
-
-build/exec/runtests:
+testbin:
 	${IDRIS2_BOOT} --build tests.ipkg
 
 clean:

tests/idris2/reg020/expected

@@ -0,0 +1,7 @@
+1/1: Building matchlits (matchlits.idr)
+Main> Main.test1 : Int -> Int
+test1 256 = 42
+test1 64 = 43
+test1 1234567890 = 44
+test1 _ = 0
+Main> Bye for now!

tests/idris2/reg020/input

@@ -0,0 +1,2 @@
+:printdef test1
+:q

tests/idris2/reg020/matchlits.idr

@@ -0,0 +1,5 @@
+test1 : Int -> Int
+test1 0x100 = 42
+test1 0o100 = 43
+test1 1234567890 = 44
+test1 _         = 0

tests/idris2/reg020/run

@@ -0,0 +1,3 @@
+$1 matchlits.idr --no-banner < input
+
+rm -rf build