← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/fail/Productivity.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/Productivity.agda
1
 
module Productivity (char : Set) where
2
 
 
3
 
  open import Imports.Coinduction
4
 
 
5
 
  infix  50 _⋆ _+
6
 
  infixl 40 _⊛_
7
 
  infixl 30 _∣_
8
 
 
9
 
  data P : Set where
10
 
    ε   : P
11
 
    sym : char -> P
12
 
    _⊛_ : ∞ P -> ∞ P -> P
13
 
    _∣_ : ∞ P -> ∞ P -> P
14
 
 
15
 
  mutual
16
 
 
17
 
    _⋆ : P -> P
18
 
    p ⋆ = ♯ ε ∣ ♯ (p +)
19
 
 
20
 
    _+ : P -> P
21
 
    p + = ♯ p ⊛ ♯ (p ⋆)
22
 
 
23
 
  _sepBy_ : P -> P -> P
24
 
  p sepBy sep = ♯ p ⊛ ♯ ((♯ sep ⊛ ♯ p) ⋆)
25
 
 
26
 
  postulate
27
 
    addOp  : P
28
 
    mulOp  : P
29
 
    number : P
30
 
    openP  : char
31
 
    closeP : char
32
 
 
33
 
  -- Not guarded:
34
 
 
35
 
  mutual
36
 
    expr   = term sepBy addOp
37
 
    term   = factor sepBy mulOp
38
 
    factor = ♯ number ∣ ♯ (♯ (♯ sym openP ⊛ ♯ expr) ⊛ ♯ sym closeP)
39
 
 
40
 
  -- Guarded and incomprehensible:
41
 
 
42
 
  mutual
43
 
    expr₁ = ♯ term₁ ⊛ ♯ expr₂
44
 
    expr₂ = ♯ ε ∣ ♯ expr₃
45
 
    expr₃ = ♯ (♯ addOp ⊛ ♯ term₁) ⊛ ♯ expr₂
46
 
 
47
 
    term₁ = ♯ factor₁ ⊛ ♯ term₂
48
 
    term₂ = ♯ ε ∣ ♯ term₃
49
 
    term₃ = ♯ (♯ mulOp ⊛ ♯ factor₁) ⊛ ♯ term₂
50
 
 
51
 
    factor₁ = ♯ number ∣ ♯ (♯ (♯ sym openP ⊛ ♯ expr₁) ⊛ ♯ sym closeP)