← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to test/succeed/PruningNonMillerPattern.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
test/succeed/PruningNonMillerPattern.agda
1
 
module PruningNonMillerPattern where
2
 
 
3
 
data _≡_ {A : Set}(a : A) : A -> Set where
4
 
  refl : a ≡ a
5
 
 
6
 
data Nat : Set where
7
 
  zero : Nat
8
 
  suc  : Nat -> Nat
9
 
 
10
 
test : let X : Nat -> Nat -> Nat
11
 
           X = _
12
 
           Y : Nat -> Nat -> Nat
13
 
           Y = _
14
 
       in  (C : Set) ->
15
 
           (({x y : Nat} -> X x x ≡ suc (Y x y)) ->
16
 
            ({x y : Nat} -> Y x x ≡ x)           ->
17
 
            ({x y : Nat} -> X (Y x y) y ≡ X x x) -> C) -> C
18
 
test C k = k refl refl refl
19
 
{- none of these equations is immediately solvable.  However,
20
 
   from 1. we deduce that Y does not depend on its second argument, thus
21
 
   from 2. we solve Y x y = x, and then
22
 
   eqn. 3. simplifies to X x y = X x x, thus, X does not depend on its second arg,
23
 
   we can then solve using 1.  X x y = suc x
24
 
-}
25
 
 
26
 
test' : let X : Nat -> Nat -> Nat
27
 
            X = _
28
 
            Y : Nat -> Nat -> Nat
29
 
            Y = _
30
 
        in  (C : Set) ->
31
 
            (({x y : Nat} -> X x (suc x) ≡ suc (Y x y)) ->  -- non-pattern lhs
32
 
             ({x y : Nat} -> Y x x ≡ x)           ->
33
 
             ({x y : Nat} -> X (Y x y) y ≡ X x x) -> C) -> C
34
 
test' C k = k refl refl refl
35
 
 
36
 
 
37
 
data Sing {A : Set} : A → Set where
38
 
  sing : (x : A) -> Sing x
39
 
 
40
 
test2 : let X : Nat -> Nat -> Nat
41
 
            X = _
42
 
            Y : Nat → Set -> Nat
43
 
            Y = _
44
 
        in  (C : Set) ->
45
 
            (({x y : Nat} -> X x x ≡ suc (Y x (Sing (suc y)))) ->
46
 
             ({x y : Nat} -> Y x (Sing x) ≡ x)           ->
47
 
             ({x y : Nat} -> X (Y x (Sing y)) y ≡ X x x) -> C) -> C
48
 
test2 C k = k refl refl refl
49
 
 
50
 
T : Nat → Set
51
 
T zero    = Nat
52
 
T (suc _) = Nat → Nat
53
 
 
54
 
test3 : let X : Nat -> Nat -> Nat
55
 
            X = _
56
 
            Y : Nat → Set -> Nat
57
 
            Y = _
58
 
        in  (C : Set) ->
59
 
            (({x y : Nat} -> X x x ≡ suc (Y x (T y -> T y))) ->
60
 
             ({x y : Nat} -> Y x (Sing x) ≡ x)           ->
61
 
             ({x y : Nat} -> X (Y x (Sing y)) y ≡ X x x) -> C) -> C
62
 
test3 C k = k refl refl refl
63
 
 
64
 
test4 : let X : Nat -> Nat -> Nat
65
 
            X = _
66
 
            Y : Nat → (Nat → Nat) -> Nat
67
 
            Y = _
68
 
        in  (C : Set) ->
69
 
            ((∀ {x : Nat} {y : Nat → Nat} -> X x x ≡ suc (Y x (λ k → y zero))) ->
70
 
             (∀ {x : Nat} {y : Nat → Nat} -> Y x (λ k → y zero) ≡ x)           ->
71
 
             (∀ {x : Nat} {y : Nat } -> X (Y x (λ k → y)) y ≡ X x x) -> C) -> C
72
 
test4 C k = k refl refl refl
73
 
 
74
 
test5 : let X : Nat -> Nat -> Nat
75
 
            X = _
76
 
            Y : Nat -> .Nat -> Nat
77
 
            Y = _
78
 
        in  (C : Set) ->
79
 
            (({x y : Nat} -> X x (suc x) ≡ suc (Y x (suc y))) ->  -- non-pattern lhs
80
 
             ({x y : Nat} -> Y x x ≡ x)           ->
81
 
             ({x y : Nat} -> X (Y x (suc y)) y ≡ X x x) -> C) -> C
82
 
test5 C k = k refl refl refl