Mercurial > urweb
comparison lib/ur/top.urs @ 1480:aa0c6382aa57
top.urs: More comments
author | Robin Green <greenrd@greenrd.org> |
---|---|
date | Tue, 28 Jun 2011 11:55:57 +0100 |
parents | 44f78d6fec29 |
children | 9253765d7724 |
comparison
equal
deleted
inserted
replaced
1479:f561025bb68e | 1480:aa0c6382aa57 |
---|---|
19 end | 19 end |
20 | 20 |
21 | 21 |
22 val not : bool -> bool | 22 val not : bool -> bool |
23 | 23 |
24 (* Type-level identity function *) | |
24 con id = K ==> fn t :: K => t | 25 con id = K ==> fn t :: K => t |
26 | |
27 (* Type-level function which yields the value-level record | |
28 described by the given type-level record *) | |
25 con record = fn t :: {Type} => $t | 29 con record = fn t :: {Type} => $t |
30 | |
26 con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1 | 31 con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1 |
27 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2 | 32 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2 |
28 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1 | 33 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1 |
29 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2 | 34 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2 |
30 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3 | 35 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3 |
31 | 36 |
37 (* Convert a record of n Units into a type-level record where | |
38 each field has the same value (which describes a uniformly | |
39 typed record) *) | |
32 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f) | 40 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f) |
33 | 41 |
42 (* Existential type former *) | |
34 con ex :: K --> (K -> Type) -> Type | 43 con ex :: K --> (K -> Type) -> Type |
35 | 44 |
45 (* Introduction of existential type *) | |
36 val ex_intro : K --> tf :: (K -> Type) -> choice :: K -> tf choice -> ex tf | 46 val ex_intro : K --> tf :: (K -> Type) -> choice :: K -> tf choice -> ex tf |
47 | |
48 (* Eliminator for existential type *) | |
37 val ex_elim : K --> tf ::: (K -> Type) -> ex tf -> res ::: Type -> (choice :: K -> tf choice -> res) -> res | 49 val ex_elim : K --> tf ::: (K -> Type) -> ex tf -> res ::: Type -> (choice :: K -> tf choice -> res) -> res |
38 | 50 |
51 (* Composition of ordinary (value-level) functions *) | |
39 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type | 52 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type |
40 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) | 53 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) |
41 | 54 |
42 val show_option : t ::: Type -> show t -> show (option t) | 55 val show_option : t ::: Type -> show t -> show (option t) |
43 val read_option : t ::: Type -> read t -> read (option t) | 56 val read_option : t ::: Type -> read t -> read (option t) |
44 | 57 |
45 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t | 58 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t |
46 -> xml ctx use [] | 59 -> xml ctx use [] |
47 | 60 |
61 (* Given a polymorphic type (tf) and a means of constructing | |
62 "default" values of tf applied to arbitrary arguments, | |
63 constructs records consisting of those "default" values *) | |
48 val map0 : K --> tf :: (K -> Type) | 64 val map0 : K --> tf :: (K -> Type) |
49 -> (t :: K -> tf t) | 65 -> (t :: K -> tf t) |
50 -> r ::: {K} -> folder r -> $(map tf r) | 66 -> r ::: {K} -> folder r -> $(map tf r) |
67 | |
68 (* Given two polymorphic types (tf1 and tf2) and a means of | |
69 converting from tf1 t to tf2 t for arbitrary t, | |
70 converts records of tf1's to records of tf2's *) | |
51 val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) | 71 val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) |
52 -> (t ::: K -> tf1 t -> tf2 t) | 72 -> (t ::: K -> tf1 t -> tf2 t) |
53 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) | 73 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) |
74 | |
75 (* Two-argument conversion form of mp *) | |
54 val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type) | 76 val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type) |
55 -> (t ::: K -> tf1 t -> tf2 t -> tf t) | 77 -> (t ::: K -> tf1 t -> tf2 t -> tf t) |
56 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r) | 78 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r) |
79 | |
80 (* Three-argument conversion form of mp *) | |
57 val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type) | 81 val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type) |
58 -> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) | 82 -> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) |
59 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r) | 83 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r) |
60 | 84 |
85 (* Fold along a uniformly (homogenously) typed record *) | |
61 val foldUR : tf :: Type -> tr :: ({Unit} -> Type) | 86 val foldUR : tf :: Type -> tr :: ({Unit} -> Type) |
62 -> (nm :: Name -> rest :: {Unit} | 87 -> (nm :: Name -> rest :: {Unit} |
63 -> [[nm] ~ rest] => | 88 -> [[nm] ~ rest] => |
64 tf -> tr rest -> tr ([nm] ++ rest)) | 89 tf -> tr rest -> tr ([nm] ++ rest)) |
65 -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf r) -> tr r | 90 -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf r) -> tr r |
66 | 91 |
92 (* Fold (generalized safe zip) along two equal-length uniformly-typed records *) | |
67 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type) | 93 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type) |
68 -> (nm :: Name -> rest :: {Unit} | 94 -> (nm :: Name -> rest :: {Unit} |
69 -> [[nm] ~ rest] => | 95 -> [[nm] ~ rest] => |
70 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) | 96 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) |
71 -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r | 97 -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r |
72 | 98 |
99 (* Fold along a heterogenously-typed record *) | |
73 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type) | 100 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type) |
74 -> (nm :: Name -> t :: K -> rest :: {K} | 101 -> (nm :: Name -> t :: K -> rest :: {K} |
75 -> [[nm] ~ rest] => | 102 -> [[nm] ~ rest] => |
76 tf t -> tr rest -> tr ([nm = t] ++ rest)) | 103 tf t -> tr rest -> tr ([nm = t] ++ rest)) |
77 -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r | 104 -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r |
78 | 105 |
106 (* Fold (generalized safe zip) along two heterogenously-typed records *) | |
79 val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) | 107 val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) |
80 -> tr :: ({K} -> Type) | 108 -> tr :: ({K} -> Type) |
81 -> (nm :: Name -> t :: K -> rest :: {K} | 109 -> (nm :: Name -> t :: K -> rest :: {K} |
82 -> [[nm] ~ rest] => | 110 -> [[nm] ~ rest] => |
83 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) | 111 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) |
84 -> tr [] | 112 -> tr [] |
85 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r | 113 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r |
86 | 114 |
115 (* Fold (generalized safe zip) along three heterogenously-typed records *) | |
87 val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) | 116 val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) |
88 -> tr :: ({K} -> Type) | 117 -> tr :: ({K} -> Type) |
89 -> (nm :: Name -> t :: K -> rest :: {K} | 118 -> (nm :: Name -> t :: K -> rest :: {K} |
90 -> [[nm] ~ rest] => | 119 -> [[nm] ~ rest] => |
91 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest)) | 120 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest)) |
92 -> tr [] | 121 -> tr [] |
93 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r | 122 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r |
94 | 123 |
124 (* Generate some XML by mapping over a uniformly-typed record *) | |
95 val mapUX : tf :: Type -> ctx :: {Unit} | 125 val mapUX : tf :: Type -> ctx :: {Unit} |
96 -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => | 126 -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => |
97 tf -> xml ctx [] []) | 127 tf -> xml ctx [] []) |
98 -> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] [] | 128 -> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] [] |
99 | 129 |
130 (* Generate some XML by mapping over a heterogenously-typed record *) | |
100 val mapX : K --> tf :: (K -> Type) -> ctx :: {Unit} | 131 val mapX : K --> tf :: (K -> Type) -> ctx :: {Unit} |
101 -> (nm :: Name -> t :: K -> rest :: {K} | 132 -> (nm :: Name -> t :: K -> rest :: {K} |
102 -> [[nm] ~ rest] => | 133 -> [[nm] ~ rest] => |
103 tf t -> xml ctx [] []) | 134 tf t -> xml ctx [] []) |
104 -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] | 135 -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] |