← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/fail/PatternSynonymsErrorLocation.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/fail/PatternSynonymsErrorLocation.agda
1
 
{-# OPTIONS --type-in-type #-}
2
 
 
3
 
module PatternSynonymsErrorLocation where
4
 
 
5
 
data _≡_ {A : Set}(a : A) : A -> Set where
6
 
  refl : a ≡ a
7
 
 
8
 
infixr 2 _,_
9
 
 
10
 
record Unit : Set where
11
 
 
12
 
data Sigma (A : Set)(B : A -> Set) : Set where
13
 
  _,_ : (fst : A) -> B fst -> Sigma A B
14
 
 
15
 
Prod : (A B : Set) -> Set
16
 
Prod A B = Sigma A \ _ -> B
17
 
 
18
 
data Empty : Set where
19
 
 
20
 
data ListTag : Set where nil cons : ListTag
21
 
 
22
 
{-# NO_TERMINATION_CHECK #-}
23
 
List : (A : Set) -> Set
24
 
List A = Sigma ListTag T where
25
 
  T : ListTag -> Set
26
 
  T nil  = Unit
27
 
  T cons = Sigma A \ _ -> List A
28
 
 
29
 
infix 5 _∷_
30
 
 
31
 
pattern []       = nil , _
32
 
pattern _∷_ x xs = cons , x , xs
33
 
 
34
 
data TyTag : Set where base arr : TyTag
35
 
 
36
 
{-# NO_TERMINATION_CHECK #-}
37
 
Ty : Set
38
 
Ty = Sigma TyTag T where
39
 
  T : TyTag -> Set
40
 
  T base = Unit
41
 
  T arr  = Sigma Ty \ _ -> Ty  -- Prod Ty Ty
42
 
 
43
 
infix 10 _⇒_
44
 
 
45
 
pattern ★       = base , _
46
 
pattern _⇒_ A B = arr , A , B
47
 
 
48
 
Context = List Ty
49
 
 
50
 
data NatTag : Set where zero succ : NatTag
51
 
 
52
 
Var : (Gamma : Context)(C : Ty) -> Set
53
 
Var []           C = Empty
54
 
Var (cons , A , Gamma) C =  Sigma NatTag T
55
 
  where T : NatTag -> Set
56
 
        T zero = A ≡ C
57
 
        T succ = Var Gamma C
58
 
 
59
 
pattern vz   = zero , refl
60
 
pattern vs x = succ , x
61
 
 
62
 
idVar : (Gamma : Context)(C : Ty)(x : Var Gamma C) -> Var Gamma C
63
 
idVar [] _ ()
64
 
idVar (A ∷ Gamma) C vz         = vz
65
 
idVar (A ∷ Gamma) C (vs x)     = vs (idVar Gamma C x)