git.iko.soy/Idris-dev
on master help sign in
Case tree building considers heterogeneous types

Previously, arguments with different types in each cases could have led to run-time failure (or non-reduction at compile-time) since branching takes only the constructor tag into account. Now the case tree compiler orders the patterns so that this can no longer happen. Fixes #1080 Fixes #771

commitcfe250a3ce9ea199db9f71dc61339605939ce608 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 20 Apr 2014, 16:22 (13 years ago) parente07c13d
6 files changed+96−1
compare with master
unifiedsplit
idris.cabal+3 src/Idris/Core/CaseTree.hs+19−1 test/reg040/expected+4 test/reg040/ott.idr+42 test/reg040/run+5 test/reg040/showu.idr+23
idris.cabal+3
@@ -230,6 +230,9 @@ Extra-source-files:
230230 test/reg039/run
231231 test/reg039/*.idr
232232 test/reg039/expected
233+ test/reg040/run
234+ test/reg040/*.idr
235+ test/reg040/expected
233236
234237 test/basic001/run
235238 test/basic001/*.idr
src/Idris/Core/CaseTree.hs+19−1
@@ -10,6 +10,7 @@ import Idris.Core.TT
1010import Control.Monad.State
1111import Data.Maybe
1212import Data.List hiding (partition)
13+import qualified Data.List(partition)
1314import Debug.Trace
1415
1516data CaseDef = CaseDef [Name] !SC [Term]
@@ -417,8 +418,15 @@ order :: [(Name, Bool)] -> [Clause] -> ([Name], [Clause])
417418order [] cs = ([], cs)
418419order ns' [] = (map fst ns', [])
419420order 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
420427 -- 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
422430 (getNOrder pats', zipWith rebuild pats' cs)
423431 where
424432 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))
426434
427435 rebuild patnames clause = (map snd patnames, snd clause)
428436
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+
429447 -- this compares (+isInaccessible, -numberOfCases)
430448 moreDistinct xs ys = compare (snd . fst . head $ xs, numNames [] (map snd ys))
431449 (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