Normalise LHS before compilation

...otherwise in some situations the forcing optimisation may lead
to uncompilable code

src/Core/CaseTree.hs

@@ -158,7 +158,8 @@ data Phase = CompileTime | RunTime
 -- Generate a simple case tree
 -- Work Left to Right at Compile Time 
 
-simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] -> TC CaseDef
+simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] -> 
+              TC CaseDef
 simpleCase tc cover phase fc [] 
                  = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []
 simpleCase tc cover phase fc cs 

src/Idris/ElabDecls.hs

@@ -320,7 +320,6 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
                        else stripCollapsed pats
 
          logLvl 5 $ "Patterns:\n" ++ show pats
-         logLvl 5 $ "Optimised patterns:\n" ++ show optpats
 
          let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats
          tree@(CaseDef scargs sc _) <- tclift $ 
@@ -339,6 +338,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
                     else return []
          let pcover = null pmissing
          pdef' <- applyOpts optpdef 
+         logLvl 5 $ "Optimised patterns:\n" ++ show pdef'
          ist <- get
 --          let wf = wellFounded ist n sc
          let tot = if pcover || AssertTotal `elem` opts
@@ -400,7 +400,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
     
     getLHS (_, l, _) = l
 
-    simpl rt ctxt (Right (x, y)) = Right (x, simplify ctxt rt [] y)
+    simpl rt ctxt (Right (x, y)) = Right (normalise ctxt [] x, 
+                                          simplify ctxt rt [] y)
     simpl rt ctxt t = t
 
     sameLength ((_, x, _) : xs) 

test/reg005/expected

@@ -0,0 +1 @@
+1f4o1b4a1r1b3a1z

test/reg005/reg005.idr

@@ -0,0 +1,50 @@
+module Main
+
+rep : (n : Nat) -> Char -> Vect Char n
+rep O     x = []
+rep (S k) x = x :: rep k x
+
+data RLE : Vect Char n -> Set where
+     REnd  : RLE []
+     RChar : {xs : Vect Char k} ->
+             (n : Nat) -> (x : Char) -> RLE xs -> 
+             RLE (rep (S n) x ++ xs)
+
+eq : (x : Char) -> (y : Char) -> Maybe (x = y)
+eq x y = if x == y then Just ?eqCharOK else Nothing
+
+------------
+
+rle : (xs : Vect Char n) -> RLE xs
+rle [] = REnd
+rle (x :: xs) with (rle xs)
+   rle (x :: [])            | REnd = RChar O x REnd 
+   rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)
+     rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just p 
+           = RChar (S n) x rs
+     rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing 
+           = RChar O x (RChar n y rs)
+
+compress : Vect Char n -> String
+compress xs with (rle xs)
+  compress Nil                 | REnd         = ""
+  compress (rep (S n) x ++ xs) | RChar n x rs 
+         = let ni : Int = cast (S n) in
+               show ni ++ show x ++ compress xs
+
+compressString : String -> String
+compressString xs = compress (fromList (unpack xs))
+
+main : IO ()
+main = putStrLn (compressString "foooobaaaarbaaaz")
+
+
+
+---------- Proofs ----------
+
+Main.eqCharOK = proof {
+  intros;
+  refine believe_me;
+  exact x = x;
+}
+

test/reg005/run

@@ -0,0 +1,4 @@
+#!/bin/bash
+idris $@ reg005.idr -o reg005
+./reg005
+rm -f reg005 *.ibc