Mercurial > urweb

comparison lib/ur/top.urs @ 623:588b9d16b00a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents 8998114760c1
children f4f2b09a533a
comparison
equal deleted inserted replaced
622:d64533157f40 623:588b9d16b00a
1 (** Row folding *)
2
3 con folder = K ==> fn r :: {K} =>
4 tf :: ({K} -> Type)
5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r
6 -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
7 -> tf [] -> tf r
8
9
1 val not : bool -> bool 10 val not : bool -> bool
2 11
3 con idT = fn t :: Type => t 12 con idT = fn t :: Type => t
4 con record = fn t :: {Type} => $t 13 con record = fn t :: {Type} => $t
5 con fstTT = fn t :: (Type * Type) => t.1 14 con fstTT = fn t :: (Type * Type) => t.1
23 32
24 val foldUR : tf :: Type -> tr :: ({Unit} -> Type) 33 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
25 -> (nm :: Name -> rest :: {Unit} 34 -> (nm :: Name -> rest :: {Unit}
26 -> fn [[nm] ~ rest] => 35 -> fn [[nm] ~ rest] =>
27 tf -> tr rest -> tr ([nm] ++ rest)) 36 tf -> tr rest -> tr ([nm] ++ rest))
28 -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r 37 -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf r) -> tr r
29 38
30 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type) 39 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
31 -> (nm :: Name -> rest :: {Unit} 40 -> (nm :: Name -> rest :: {Unit}
32 -> fn [[nm] ~ rest] => 41 -> fn [[nm] ~ rest] =>
33 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) 42 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
34 -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r 43 -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
35 44
36 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit} 45 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
37 -> (nm :: Name -> rest :: {Unit} 46 -> (nm :: Name -> rest :: {Unit}
38 -> fn [[nm] ~ rest] => 47 -> fn [[nm] ~ rest] =>
39 tf1 -> tf2 -> xml ctx [] []) 48 tf1 -> tf2 -> xml ctx [] [])
40 -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] [] 49 -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
41 50
42 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) 51 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
43 -> (nm :: Name -> t :: Type -> rest :: {Type} 52 -> (nm :: Name -> t :: K -> rest :: {K}
44 -> fn [[nm] ~ rest] => 53 -> fn [[nm] ~ rest] =>
45 tf t -> tr rest -> tr ([nm = t] ++ rest)) 54 tf t -> tr rest -> tr ([nm = t] ++ rest))
46 -> tr [] -> r :: {Type} -> $(map tf r) -> tr r 55 -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
47 56
48 val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) 57 val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
49 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 58 -> tr :: ({K} -> Type)
59 -> (nm :: Name -> t :: K -> rest :: {K}
60 -> fn [[nm] ~ rest] =>
61 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
62 -> tr []
63 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
64
65 val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit}
66 -> (nm :: Name -> t :: K -> rest :: {K}
67 -> fn [[nm] ~ rest] =>
68 tf t -> xml ctx [] [])
69 -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
70
71 val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
72 -> (nm :: Name -> t :: K -> rest :: {K}
50 -> fn [[nm] ~ rest] => 73 -> fn [[nm] ~ rest] =>
51 tf t -> tr rest -> tr ([nm = t] ++ rest)) 74 tf1 t -> tf2 t -> xml ctx [] [])
52 -> tr [] -> r :: {(Type * Type)} -> $(map tf r) -> tr r 75 -> r ::: {K} -> folder r
53 76 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
54 val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type)
55 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
56 -> fn [[nm] ~ rest] =>
57 tf t -> tr rest -> tr ([nm = t] ++ rest))
58 -> tr [] -> r :: {(Type * Type * Type)} -> $(map tf r) -> tr r
59
60 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
61 -> tr :: ({Type} -> Type)
62 -> (nm :: Name -> t :: Type -> rest :: {Type}
63 -> fn [[nm] ~ rest] =>
64 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
65 -> tr []
66 -> r :: {Type} -> $(map tf1 r) -> $(map tf2 r) -> tr r
67
68 val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
69 -> tr :: ({(Type * Type)} -> Type)
70 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
71 -> fn [[nm] ~ rest] =>
72 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
73 -> tr [] -> r :: {(Type * Type)}
74 -> $(map tf1 r) -> $(map tf2 r) -> tr r
75
76 val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
77 -> tr :: ({(Type * Type * Type)} -> Type)
78 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
79 -> fn [[nm] ~ rest] =>
80 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
81 -> tr [] -> r :: {(Type * Type * Type)}
82 -> $(map tf1 r) -> $(map tf2 r) -> tr r
83
84 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
85 -> (nm :: Name -> t :: Type -> rest :: {Type}
86 -> fn [[nm] ~ rest] =>
87 tf t -> xml ctx [] [])
88 -> r :: {Type} -> $(map tf r) -> xml ctx [] []
89
90 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
91 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
92 -> fn [[nm] ~ rest] =>
93 tf t -> xml ctx [] [])
94 -> r :: {(Type * Type)} -> $(map tf r) -> xml ctx [] []
95
96 val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit}
97 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
98 -> fn [[nm] ~ rest] =>
99 tf t -> xml ctx [] [])
100 -> r :: {(Type * Type * Type)} -> $(map tf r) -> xml ctx [] []
101
102 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
103 -> (nm :: Name -> t :: Type -> rest :: {Type}
104 -> fn [[nm] ~ rest] =>
105 tf1 t -> tf2 t -> xml ctx [] [])
106 -> r :: {Type}
107 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
108
109 val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
110 -> ctx :: {Unit}
111 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
112 -> fn [[nm] ~ rest] =>
113 tf1 t -> tf2 t -> xml ctx [] [])
114 -> r :: {(Type * Type)}
115 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
116
117
118 val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
119 -> ctx :: {Unit}
120 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
121 -> fn [[nm] ~ rest] =>
122 tf1 t -> tf2 t -> xml ctx [] [])
123 -> r :: {(Type * Type * Type)}
124 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
125 77
126 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} 78 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
127 -> sql_query tables exps 79 -> sql_query tables exps
128 -> fn [tables ~ exps] => 80 -> fn [tables ~ exps] =>
129 ($(exps ++ map (fn fields :: {Type} => $fields) tables) 81 ($(exps ++ map (fn fields :: {Type} => $fields) tables)