cfe250a · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -230,6 +230,9 @@ Extra-source-files:

230 test/reg039/run

231 test/reg039/*.idr

232 test/reg039/expected

233+ test/reg040/run

234+ test/reg040/*.idr

235+ test/reg040/expected

233

236

234 test/basic001/run

237 test/basic001/run

235 test/basic001/*.idr

238 test/basic001/*.idr

src/Idris/Core/CaseTree.hs+19−1

@@ -10,6 +10,7 @@ import Idris.Core.TT

10import Control.Monad.State

11import Data.Maybe

12import Data.List hiding (partition)

13+import qualified Data.List(partition)

13import Debug.Trace

14import Debug.Trace

14

15

15data CaseDef = CaseDef [Name] !SC [Term]

16data CaseDef = CaseDef [Name] !SC [Term]

@@ -417,8 +418,15 @@ order :: [(Name, Bool)] -> [Clause] -> ([Name], [Clause])

417order [] cs = ([], cs)

418order [] cs = ([], cs)

418order ns' [] = (map fst ns', [])

419order ns' [] = (map fst ns', [])

419order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))

420order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))

421+ -- only sort the arguments where there is no clash in

422+ -- constructor tags between families, and no constructor/constant

423+ -- clash, because otherwise we can't reliable make the

424+ -- case distinction on evaluation

425+ (patnames_ord, patnames_rest)

426+ = Data.List.partition (noClash . map snd) patnames

420 -- note: sortBy . reverse is not nonsense because sortBy is stable

427 -- note: sortBy . reverse is not nonsense because sortBy is stable

421− pats' = transpose (sortBy moreDistinct (reverse patnames)) in

428+ pats' = transpose (sortBy moreDistinct (reverse patnames_ord)

429+ ++ patnames_rest) in

422 (getNOrder pats', zipWith rebuild pats' cs)

430 (getNOrder pats', zipWith rebuild pats' cs)

423 where

431 where

424 getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs)

432 getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs)

@@ -426,6 +434,16 @@ order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))

426

434

427 rebuild patnames clause = (map snd patnames, snd clause)

435 rebuild patnames clause = (map snd patnames, snd clause)

428

436

437+ noClash [] = True

438+ noClash (p : ps) = not (any (clashPat p) ps) && noClash ps

439+

440+ clashPat (PCon _ _ _) (PConst _) = True

441+ clashPat (PConst _) (PCon _ _ _) = True

442+ clashPat (PCon _ _ _) (PSuc _) = True

443+ clashPat (PSuc _) (PCon _ _ _) = True

444+ clashPat (PCon n i _) (PCon n' i' _) | i == i' = n /= n'

445+ clashPat _ _ = False

446+

429 -- this compares (+isInaccessible, -numberOfCases)

447 -- this compares (+isInaccessible, -numberOfCases)

430 moreDistinct xs ys = compare (snd . fst . head $ xs, numNames [] (map snd ys))

448 moreDistinct xs ys = compare (snd . fst . head $ xs, numNames [] (map snd ys))

431 (snd . fst . head $ ys, numNames [] (map snd xs))

449 (snd . fst . head $ ys, numNames [] (map snd xs))

test/reg040/expectednew file+4

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

1+Type checking ./ott.idr

2+?prf : (x : Bool) ->

3+(x1 : Bool) -> (El (EQ two x two x1)) -> El (EQ two x two x1)

4+Z

test/reg040/ott.idrnew file+42

@@ -0,0 +1,42 @@

1+module OTT

2+

3+mutual

4+

5+ data U : Type where

6+ u : U

7+ zero : U

8+ one : U

9+ two : U

10+ pi : (s : U) -> (t : El s -> U) -> U

11+

12+ El : U -> Type

13+ El u = U

14+ El zero = _|_

15+ El one = ()

16+ El two = Bool

17+ El (pi s t) = (x : El s) -> El (t x)

18+

19+infixr 10 ~>

20+(~>) : U -> U -> U

21+s ~> t = pi s $ const t

22+

23+syntax "<|" [s] "|>" = El s

24+syntax [x] "==" [y] "in" [s] = EQ s x s y

25+

26+%assert_total

27+EQ : (s : U) -> <| s |> -> (t : U) -> <| t |> -> U

28+EQ u u u u = one

29+EQ u zero u zero = one

30+EQ u one u one = one

31+EQ u two u two = one

32+EQ u (pi s t) u (pi s' t') = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ u (t x) u (t' y)

33+EQ zero x zero y = one

34+EQ one x one y = one

35+EQ two True two True = one

36+EQ two False two False = one

37+EQ (pi s t) f (pi s' t') g = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)

38+EQ _ _ _ _ = zero

39+

40+example : <| id == id in (two ~> two) |>

41+example = ?prf

42+

test/reg040/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+echo "example" | idris $@ --quiet ott.idr

3+idris $@ showu.idr -o reg040

4+./reg040

5+rm -f reg040 *.ibc

test/reg040/showu.idrnew file+23

@@ -0,0 +1,23 @@

1+module Main

2+

3+%default total

4+

5+data U : Type where

6+ BOOL : U

7+ NAT : U

8+ PAIR : U -> U -> U

9+

10+interpU : U -> Type

11+interpU BOOL = Bool

12+interpU NAT = Nat

13+interpU (PAIR x y) = (interpU x, interpU y)

14+

15+showU : (u : U) -> interpU u -> String

16+showU BOOL True = "Yes"

17+showU BOOL False = "No"

18+showU NAT Z = "Z"

19+showU NAT (S x) = "S of " ++ showU NAT x

20+showU (PAIR tx ty) (x , y) = "(" ++ showU tx x ++ "," ++ showU ty y ++ ")"

21+

22+main : IO ()

23+main = putStrLn $ showU NAT 0