← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/syntax/Syntax.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:
examples/outdated-and-incorrect/syntax/Syntax.agda
1
 
 
2
 
{-  An agda file contains a single module. The module name should correspond to
3
 
    the name and path of the file. The path is relative to the project root. In
4
 
    this case the project root is the root of Agda II. Modules can be
5
 
    parameterised, but in this case we choose not to parameterise the top-level
6
 
    module.
7
 
-}
8
 
 
9
 
module examples.syntax.Syntax where
10
 
 
11
 
  -- It is recommended that the body of the top-level module is indented by a
12
 
  -- small amount, but this is not enforced in the syntax.
13
 
 
14
 
  -- You can have modules inside modules. The name of a sub-module isn't
15
 
  -- qualified.
16
 
  module Expressions (X : Set)(x1, x2 : X) where
17
 
 
18
 
    -- There are three forms of sorts. Set = Set0.
19
 
    postulate A1 : Set
20
 
              A2 : Set3
21
 
              A3 : Prop
22
 
 
23
 
    -- Independent function space.
24
 
    fun1 : X -> X
25
 
    fun1 x = x
26
 
 
27
 
    -- Implicit independent function space. This is mostly included for
28
 
    -- symmetry, I can't come up with an example when this would be useful.
29
 
    fun2 : {X} -> X
30
 
    fun2 {x} = x
31
 
 
32
 
    -- Dependent function space.
33
 
    fun3 : (A:Set) -> A -> A
34
 
    fun3 A x = x
35
 
 
36
 
    -- Implicit dependent function space. 'A' is implicit so we don't have to
37
 
    -- write it out in the function definition.
38
 
    fun4 : {A:Set} -> A -> A
39
 
    fun4 x = x
40
 
 
41
 
    -- You can also write independent functions using the dependent function
42
 
    -- space syntax. Not that you'd ever want to.
43
 
    fun5 : (_:X) -> X
44
 
    fun5 x = x
45
 
 
46
 
    -- Lambdas can be domain free.
47
 
    const1 : {A, B : Set} -> A -> B -> A
48
 
    const1 = \x y -> x
49
 
 
50
 
    -- Or completely typed.
51
 
    const2 = \{A:Set}{B:Set}(x:A)(y:B) -> x -- inferable, no type needed
52
 
 
53
 
    -- You cannot mix typed and untyped arguments in the same lambda.
54
 
    const3 : {A, B : Set} -> A -> B -> A
55
 
    const3 = \{A}{B} -> \(x:A)(y:B) -> x
56
 
 
57
 
    -- You can have wildcards in lambdas
58
 
    const4 : {A, B : Set} -> A -> B -> A
59
 
    const4 = \x _ -> x
60
 
 
61
 
    -- Implicit arguments can be omitted in applications.
62
 
    x = const1 x1 x2
63
 
 
64
 
    -- Or made explicit.
65
 
    x' = const1 {X} {X} x1 x2
66
 
 
67
 
    -- Infix operators can be bound by lambdas. See ComplexDeclarations for
68
 
    -- more information about infix operators.
69
 
    dup : {A:Set} -> (A -> A -> A) -> A -> A
70
 
    dup = \(+) x -> x + x
71
 
 
72
 
  -- The two basic declarations are function definitions and datatype
73
 
  -- declarations.
74
 
  module BasicDeclarations (X : Set) where
75
 
 
76
 
    -- The most common declaration is the function definition. It consists of
77
 
    -- two parts; a type signature and a set of function clauses. Type
78
 
    -- signatures have the form 'id : type', no telescopes are allowed at this
79
 
    -- point. This can be discussed.
80
 
    id : X -> X
81
 
    id x = x
82
 
 
83
 
    -- You can omit the type signature if the type can be inferred.
84
 
    id' = id
85
 
 
86
 
    -- Datatypes are introduced with the data keyword.
87
 
    data Bool : Set where
88
 
      false : Bool
89
 
      true  : Bool
90
 
 
91
 
    -- The parameters to the datatype (A in this case) are in scope in the
92
 
    -- types of the constructors. At the moment inductive families are not
93
 
    -- supported.
94
 
    data List (A : Set) : Set where
95
 
      nil  : List A
96
 
      (::) : A -> List A -> List A
97
 
 
98
 
    -- When using a constructor as a function, the parameters are hidden
99
 
    -- arguments.
100
 
    singleton : X -> List X
101
 
    singleton x = x :: nil
102
 
 
103
 
    singleton' : X -> List X
104
 
    singleton' x = (::) {X} x (nil {X})
105
 
 
106
 
    -- You can pattern match over elements of a datatype when defining
107
 
    -- functions (and only then).
108
 
    null : (A : Set) -> List A -> Bool
109
 
    null A nil     = true
110
 
    null A (x::xs) = false
111
 
 
112
 
    -- Patterns can be nested (and functions can be recursive).
113
 
    and : List Bool -> Bool
114
 
    and nil         = true
115
 
    and (true::xs)  = and xs
116
 
    and (false::xs) = false
117
 
 
118
 
    -- Functions can be defined in an infix style. When doing this it must be
119
 
    -- clear what name is being defined without looking at fixities. Hence we
120
 
    -- could never remove the parenthesis around x::xs in the second clause.
121
 
    (++) : List X -> List X -> List X
122
 
    nil     ++ ys = ys
123
 
    (x::xs) ++ ys = x :: (xs ++ ys)
124
 
 
125
 
    -- You can also use a combination of infix and prefix.
126
 
    (@) : {A, B, C : Set} -> (B -> C) -> (A -> B) -> A -> C
127
 
    (f @ g) x = f (g x)
128
 
 
129
 
  -- Declarations can appear in many different contexts and not all
130
 
  -- declarations are allowed everywhere.
131
 
  module ComplexDeclarations (X : Set) where
132
 
 
133
 
    -- You can introduce new constants with the postulate declaration. A
134
 
    -- postulate declaration takes a list of type signatures.
135
 
    postulate A : Set
136
 
              a : A
137
 
 
138
 
    -- Let's introduce some datatypes so we have something to work with. At the
139
 
    -- same time we illustrate that layout is optional.
140
 
    data Nat  : Set where { zero : Nat;   suc  : Nat -> Nat }
141
 
    data Bool : Set where { false : Bool; true : Bool }
142
 
 
143
 
    {- We can declare the fixity of infix symbols. The fixity is tied to a
144
 
       particular binding of a name. The binding doesn't have to be in scope
145
 
       directly (as in the example below), but it should be possible to bring
146
 
       it into scope by moving the fixity declaration further down in the
147
 
       current block (but never inside things).
148
 
 
149
 
       The following wouldn't be allowed:
150
 
 
151
 
         infixl 15 +
152
 
         mutual
153
 
           (+) : Nat -> Nat -> Nat
154
 
           ..
155
 
 
156
 
       There are three forms: infix, infixl and infixr, for non-associative,
157
 
       left associative and right associative respectively. The number is the
158
 
       precedence level.
159
 
    -}
160
 
 
161
 
    infixl 15 +, `plus`
162
 
 
163
 
    (+) : Nat -> Nat -> Nat
164
 
    n + zero  = zero
165
 
    n + suc m = suc (n + m)
166
 
 
167
 
    plus = (+)
168
 
 
169
 
    -- The following code is to stress test the handling of infix applications.
170
 
 
171
 
    infixl 10 @
172
 
    infixl 11 @@
173
 
    infixr 10 #
174
 
    infixr 11 ##
175
 
    postulate
176
 
      (@)  : Nat -> Nat -> Nat
177
 
      (#)  : Nat -> Nat -> Nat
178
 
      (@@) : Nat -> Nat -> Nat
179
 
      (##) : Nat -> Nat -> Nat
180
 
 
181
 
    z = zero
182
 
 
183
 
    test1 = z @ (z # z)
184
 
    test2 = (z @ z) # z
185
 
    test3 = z # (z @ z)
186
 
    test4 = (z # z) @ z
187
 
    test5 = z ## z # z ## z # z
188
 
    test6 = z @@ z @ z @@ z @ z
189
 
    test7 = z # z @@ z @@ z # z
190
 
 
191
 
    -- Mutually recursive definition are introduced using the 'mutual' keyword.
192
 
    -- A mutual block can contain function definitions, datatypes
193
 
    -- (induction-recursion) and fixity declarations.
194
 
    mutual
195
 
      even : Nat -> Bool
196
 
      even zero     = true
197
 
      even (suc n)  = odd n
198
 
 
199
 
      odd : Nat -> Bool
200
 
      odd zero      = false
201
 
      odd (suc n)   = even n
202
 
 
203
 
    -- If a function is declared abstract the definition of the function is not
204
 
    -- visible outside the module. For an abstract datatype the constructors
205
 
    -- are hidden. Definitions that can appear in an abstract block are:
206
 
    -- function definitions, data declarations, fixity declarations, mutual
207
 
    -- blocks, open and name space declarations (see NameSpaces).
208
 
    abstract
209
 
      data Stack : Set where
210
 
        nil  : Stack
211
 
        cons : A -> Stack -> Stack
212
 
 
213
 
      empty : Stack
214
 
      empty = nil
215
 
 
216
 
      push : A -> Stack -> Stack
217
 
      push = cons
218
 
 
219
 
    -- Local declarations are introduces either with a let or in a where
220
 
    -- clause. A where clause is attached to a function clause. Everything that
221
 
    -- can appear in an abstract block can appear in a local declaration, plus
222
 
    -- abstract blocks. Local functions can be recursive.
223
 
    foo : (A : Set) -> A -> A
224
 
    foo A x = let f : Local -> A
225
 
                  f (local y) = y
226
 
              in  f (local x)
227
 
      where
228
 
        data Local : Set where
229
 
          local : A -> Local
230
 
 
231
 
    -- You can declare things to be private to the current module. This means
232
 
    -- that they cannot be accessed outside the module (but they're still
233
 
    -- visible inside the module and its submodules). The only things that
234
 
    -- cannot appear in a private block are other private blocks and import
235
 
    -- statements.
236
 
    private
237
 
      bar : X -> X
238
 
      bar x = x
239
 
 
240
 
    -- Private declarations can go inside mutual and abstract blocks.
241
 
    mutual
242
 
      private f : Nat -> Nat
243
 
              f zero    = zero
244
 
              f (suc n) = g n
245
 
 
246
 
      g : Nat -> Nat
247
 
      g n = f n
248
 
 
249
 
    abstract
250
 
      Nat' : Set
251
 
      Nat' = Nat
252
 
 
253
 
      private h : Nat' -> Nat
254
 
              h n = n
255
 
 
256
 
 
257
 
  -- A name space is something that contains names. You can create new
258
 
  -- name spaces and bring names from a name space into scope.
259
 
  module NameSpaces where
260
 
 
261
 
    -- To access definitions from a module in a different file, you have to
262
 
    -- 'import' this module. Only top-level modules (which have their own
263
 
    -- files) can be imported.
264
 
 
265
 
    -- If the imported module is not parameterised a name space with the same
266
 
    -- name as the module is created.
267
 
    import examples.syntax.ModuleA
268
 
 
269
 
    -- We can now refer to things from ModuleA using the created name
270
 
    -- space.  Note that no unqualified names were brought into scope
271
 
    -- (except, perhaps, the name of the name space). [To bring
272
 
    -- unqualified names into scope we have to use the 'open'
273
 
    -- declaration.]
274
 
    FunnyNat = examples.syntax.ModuleA.Nat
275
 
 
276
 
    -- If the name of an imported module clashes with a local module we might
277
 
    -- have to rename the module we are importing
278
 
    import examples.syntax.ModuleA as A
279
 
    import examples.syntax.ModuleA as A' using (Nat)
280
 
 
281
 
    Nat1 = A.Nat
282
 
    Nat2 = A'.Nat
283
 
 
284
 
    {- You can't project from a parameterised module. It has to be
285
 
       instantiated first. The only thing that happens when importing
286
 
       is that the module name 'examples.syntax.ModuleB' is brought
287
 
       into scope (and the type checker goes away and type checks this
288
 
       module).
289
 
    -}
290
 
    import examples.syntax.ModuleB
291
 
 
292
 
    -- To instantiate ModuleB we need something to instantiate it with.
293
 
    postulate X    : Set
294
 
              (==) : X -> X -> Prop
295
 
              refl : (x : X) -> x == x
296
 
 
297
 
    -- To instantiate a module you create a new module and define it as the
298
 
    -- instantiation in question.
299
 
    module B = examples.syntax.ModuleB X (==) refl
300
 
 
301
 
    -- Now the module B contains all the names from ModuleB.
302
 
    XList = B.List
303
 
    And   = B./\    -- qualified operators are not infix symbols
304
 
 
305
 
    dummyX = B.SubModule.dummy  -- submodules of ModuleB are also in scope
306
 
 
307
 
    -- This of course works for non-parameterised modules as well.
308
 
    module B' = B
309
 
 
310
 
    -- And you can create parameterised modules this way.
311
 
    module BX ((==) : X -> X -> Prop)(refl : (x : X) -> x == x) = B X (==) refl
312
 
 
313
 
    -- To bring names from a module into scope you use an open declaration.
314
 
    open examples.syntax.ModuleA
315
 
 
316
 
    two : FunnyNat
317
 
    two = eval (plus (suc zero) (suc zero))
318
 
 
319
 
    {- In all three declarations (import, module instantiation and open) you
320
 
       can give modifiers that affect the names which are imported. There are
321
 
       three modifiers:
322
 
 
323
 
        using (x1;..;xn)                only import x1,..,xn
324
 
        hiding (x1;..;xn)               import everything but x1,..,xn
325
 
        renaming (x1 to y1;..;xn to yn) import x1,..,xn but call them y1,..,yn
326
 
 
327
 
      Restrictions:
328
 
        - a modifier can appear only once
329
 
        - 'using' and 'hiding' cannot appear together
330
 
        - imported names must be distinct (e.g. you cannot rename to a name
331
 
          that is already being imported).
332
 
    -}
333
 
 
334
 
    -- B1 only contains True and False
335
 
    module B1 = B using (True; False)
336
 
 
337
 
    -- B2 contains True, False and And where And = B./\
338
 
    module B2 = B using (True; False) renaming (/\ to And)
339
 
 
340
 
    -- B3 contains everything from B except reflEqList and eqList, plus ===
341
 
    -- where (===) = B.eqList.
342
 
    module B3 = B hiding (reflEqList) renaming (eqList to ===)
343
 
 
344
 
    -- When referring to sub modules you have to be explicitly about it being
345
 
    -- a module
346
 
    module B4 = B renaming (module SubModule to Sub)
347
 
 
348
 
    dummy : X
349
 
    dummy = B4.Sub.dummy
350
 
 
351
 
  -- There are two kinds of meta variables; question marks and underscores.
352
 
  -- Question marks are used for interaction and underscores for implicit
353
 
  -- arguments.
354
 
  module MetaVariables where
355
 
 
356
 
    postulate X : Set
357
 
              x : X
358
 
 
359
 
    -- There are two ways of writing a question mark: ? and {! ... !}
360
 
    -- The type checker will not complain about unsolved question marks (unless
361
 
    -- you claim you are done).
362
 
    incomplete : {A:Set} -> A -> A
363
 
    incomplete x = ?
364
 
 
365
 
    incomplete' : {A:Set} -> A -> A
366
 
    incomplete' x = {! you can put anything in here,
367
 
                       even {! nested holes !}
368
 
                    !}
369
 
 
370
 
    -- Underscores should always be solvable locally. Internally underscores
371
 
    -- are inserted for implicit arguments, but there are cases where you would
372
 
    -- like to write them explicitly. For instance, if you want to give one but
373
 
    -- not all implicit arguments to a function explicitly.
374
 
    underscore : ({A,B,C:Set} -> (A -> A) -> B -> C) -> X
375
 
    underscore f = f {_} {X} {_} (\y -> y) x
376
 
 
377
 
    -- Note that '_' is not an identifier character. The current use of
378
 
    -- underscore is not the real reason for this. The idea is rather that
379
 
    -- underscore will be used for subscripts.
380
 
    id : (A : Set) -> A -> A
381
 
    id A x = x
382
 
 
383
 
    x' = id_x -- this means id _ x
384
 
 
385
 
  -- The parser supports four types of literals. The syntax is the same as in
386
 
  -- Haskell (since that meant I could steal the lexer for them from ghc).
387
 
  module Literals where
388
 
 
389
 
    -- We haven't decided how to handle built-in types.
390
 
    postulate Integer : Set
391
 
              Char    : Set
392
 
              String  : Set
393
 
              Float   : Set
394
 
 
395
 
    fortyTwo : Integer
396
 
    fortyTwo = 42
397
 
 
398
 
    helloWorld : String
399
 
    helloWorld = "Hello World!"
400
 
 
401
 
    escape : Char
402
 
    escape = '\ESC'
403
 
 
404
 
    pi : Float
405
 
    pi = 3.141592
406
 
 
407
 
  -- There are few things that the parser doesn't implement.
408
 
 
409
 
    {- Fancy case. I haven't been able to come up with a nice syntax for the
410
 
       fancy case statement.  The difficulty is that we should make it clear
411
 
       what arguments to the elimination rule will appear as patterns (the
412
 
       targets). Suggestions are welcome.
413
 
 
414
 
       Also I'm not sure that we want the fancy case. It would be better to
415
 
       have a good way of doing actual pattern matching on inductive families.
416
 
    -}
417
 
 
418
 
    {- Relative imports. You might want to be able to say
419
 
 
420
 
        import .ModuleA
421
 
 
422
 
       to import the module 'current.directory.ModuleA'. Easy to implement but
423
 
       I'm not sure it's that painful to write the complete name (not a problem
424
 
       in Haskell for instance). Drawbacks: it looks kind of funny and it adds
425
 
       an extra bit of syntax to remember.
426
 
    -}
427