1--
2-- Copyright 2016, NICTA
3--
4-- This software may be distributed and modified according to the terms of
5-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
6-- See "LICENSE_GPLv2.txt" for details.
7--
8-- @TAG(NICTA_GPL)
9--
10
11type A = {f1 : X, f2 : Y, f3: Z}
12
13type X
14type Y
15type Z
16
17type B = (A take (..)) put (f1)
18-- type C = A take .. put (f1)
19-- type D = A take (.., f1) put (f1)
20-- type E = A take (f1, ..) put f1
21
22foo : () -> {f1 : X, f2 : Y, f3 : Z} take (f2, f3)
23bar : B -> ()
24
25x : () -> ()
26x () = bar (foo ())
27
28-- type C = A put (f2)
29-- type D = A take (f1, f2) put (f3)
30
31-- type E = ((A take (f2)) put (f1)) take (f2)
32
33type F = (A take (f1, f2)) put (..)
34
35id : all (a). a -> a
36id x = x
37
38test : F -> A
39test y = id[A] y
40