2856967 · Idris-dev · git.iko.soy

src/Core/CaseTree.hs+2−1

compare with master

unifiedsplit

@@ -158,7 +158,8 @@ data Phase = CompileTime | RunTime

158-- Generate a simple case tree

159-- Work Left to Right at Compile Time

160

161−simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] -> TC CaseDef

161+simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] ->

162+ TC CaseDef

162simpleCase tc cover phase fc []

163simpleCase tc cover phase fc []

163 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []

164 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []

164simpleCase tc cover phase fc cs

165simpleCase tc cover phase fc cs

src/Idris/ElabDecls.hs+3−2

@@ -320,7 +320,6 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

320 else stripCollapsed pats

321

322 logLvl 5 $ "Patterns:\n" ++ show pats

323− logLvl 5 $ "Optimised patterns:\n" ++ show optpats

324

323

325 let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats

324 let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats

326 tree@(CaseDef scargs sc _) <- tclift $

325 tree@(CaseDef scargs sc _) <- tclift $

@@ -339,6 +338,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

339 else return []

338 else return []

340 let pcover = null pmissing

339 let pcover = null pmissing

341 pdef' <- applyOpts optpdef

340 pdef' <- applyOpts optpdef

341+ logLvl 5 $ "Optimised patterns:\n" ++ show pdef'

342 ist <- get

343-- let wf = wellFounded ist n sc

344 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

400

401 getLHS (_, l, _) = l

402

403− simpl rt ctxt (Right (x, y)) = Right (x, simplify ctxt rt [] y)

403+ simpl rt ctxt (Right (x, y)) = Right (normalise ctxt [] x,

404+ simplify ctxt rt [] y)

404 simpl rt ctxt t = t

405 simpl rt ctxt t = t

405

406

406 sameLength ((_, x, _) : xs)

407 sameLength ((_, x, _) : xs)

test/reg005/expectednew file+1

@@ -0,0 +1 @@

1+1f4o1b4a1r1b3a1z

test/reg005/reg005.idrnew file+50

@@ -0,0 +1,50 @@

1+module Main

2+

3+rep : (n : Nat) -> Char -> Vect Char n

4+rep O x = []

5+rep (S k) x = x :: rep k x

6+

7+data RLE : Vect Char n -> Set where

8+ REnd : RLE []

9+ RChar : {xs : Vect Char k} ->

10+ (n : Nat) -> (x : Char) -> RLE xs ->

11+ RLE (rep (S n) x ++ xs)

12+

13+eq : (x : Char) -> (y : Char) -> Maybe (x = y)

14+eq x y = if x == y then Just ?eqCharOK else Nothing

15+

16+------------

17+

18+rle : (xs : Vect Char n) -> RLE xs

19+rle [] = REnd

20+rle (x :: xs) with (rle xs)

21+ rle (x :: []) | REnd = RChar O x REnd

22+ rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)

23+ rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just p

24+ = RChar (S n) x rs

25+ rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing

26+ = RChar O x (RChar n y rs)

27+

28+compress : Vect Char n -> String

29+compress xs with (rle xs)

30+ compress Nil | REnd = ""

31+ compress (rep (S n) x ++ xs) | RChar n x rs

32+ = let ni : Int = cast (S n) in

33+ show ni ++ show x ++ compress xs

34+

35+compressString : String -> String

36+compressString xs = compress (fromList (unpack xs))

37+

38+main : IO ()

39+main = putStrLn (compressString "foooobaaaarbaaaz")

40+

41+

42+

43+---------- Proofs ----------

44+

45+Main.eqCharOK = proof {

46+ intros;

47+ refine believe_me;

48+ exact x = x;

49+}

50+

test/reg005/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris $@ reg005.idr -o reg005

3+./reg005

4+rm -f reg005 *.ibc