Mercurial > urweb

comparison lib/ur/top.ur @ 629:e68de2a5506b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Top.Fold.concat elaborates
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 13:46:08 -0500
parents 12b73f3c108e
children 6a6eb9882d57
comparison
equal deleted inserted replaced
628:12b73f3c108e 629:e68de2a5506b
1 (** Row folding *) 1 (** Row folding *)
2 2
3 con folder = K ==> fn r :: {K} => 3 con folder = K ==> fn r :: {K} =>
4 tf :: ({K} -> Type) 4 tf :: ({K} -> Type)
5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r 5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r
6 -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) 6 -> [[nm] ~ r] => tf ([nm = v] ++ r))
7 -> tf [] -> tf r 7 -> tf [] -> tf r
8 8
9 structure Folder = struct 9 structure Folder = struct
10 fun nil K (tf :: {K} -> Type) 10 fun nil K (tf :: {K} -> Type)
11 (f : nm :: Name -> v :: K -> r :: {K} -> tf r 11 (f : nm :: Name -> v :: K -> r :: {K} -> tf r
12 -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) 12 -> [[nm] ~ r] => tf ([nm = v] ++ r))
13 (i : tf []) = i 13 (i : tf []) = i
14 14
15 fun cons K (r ::: {K}) (nm :: Name) (v :: K) [[nm] ~ r] (fold : folder r) 15 fun cons K (r ::: {K}) (nm :: Name) (v :: K) [[nm] ~ r] (fold : folder r)
16 (tf :: {K} -> Type) 16 (tf :: {K} -> Type)
17 (f : nm :: Name -> v :: K -> r :: {K} -> tf r 17 (f : nm :: Name -> v :: K -> r :: {K} -> tf r
18 -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) 18 -> [[nm] ~ r] => tf ([nm = v] ++ r))
19 (i : tf []) = f [nm] [v] [r] (fold [tf] f i) 19 (i : tf []) = f [nm] [v] [r] (fold [tf] f i) !
20 20
21 fun concat K (r1 ::: {K}) (r2 ::: {K}) [r1 ~ r2] 21 fun concat K (r1 ::: {K}) (r2 ::: {K}) [r1 ~ r2]
22 (f1 : folder r1) (f2 : folder r2) 22 (f1 : folder r1) (f2 : folder r2)
23 (tf :: {K} -> Type) 23 (tf :: {K} -> Type)
24 (f : nm :: Name -> v :: K -> r :: {K} -> tf r 24 (f : nm :: Name -> v :: K -> r :: {K} -> tf r
25 -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) 25 -> [[nm] ~ r] => tf ([nm = v] ++ r))
26 (i : tf []) = 26 (i : tf []) =
27 f1 [fn r1' [r1' ~ r2] => tf (r1' ++ r2)] 0 27 f1 [fn r1' => [r1' ~ r2] => tf (r1' ++ r2)]
28 (*(fn (nm :: Name) (v :: K) (r1' :: {K}) (acc : fn [r1' ~ r2] => tf (r1' ++ r2)) 28 (fn (nm :: Name) (v :: K) (r1' :: {K}) (acc : [r1' ~ r2] => tf (r1' ++ r2))
29 [[nm] ~ r1'] [[nm = v] ++ r1' ~ r2] => 29 [[nm] ~ r1'] [[nm = v] ++ r1' ~ r2] =>
30 f [nm] [v] [r1' ++ r2] acc) 30 f [nm] [v] [r1' ++ r2] acc !)
31 (f2 [tf] f i)*) 31 (fn [[] ~ r2] => f2 [tf] f i) !
32 end 32 end
33 33
34 34
35 fun not b = if b then False else True 35 fun not b = if b then False else True
36 36
57 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) = 57 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) =
58 cdata (show v) 58 cdata (show v)
59 59
60 fun foldUR (tf :: Type) (tr :: {Unit} -> Type) 60 fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
61 (f : nm :: Name -> rest :: {Unit} 61 (f : nm :: Name -> rest :: {Unit}
62 -> fn [[nm] ~ rest] => 62 -> [[nm] ~ rest] =>
63 tf -> tr rest -> tr ([nm] ++ rest)) 63 tf -> tr rest -> tr ([nm] ++ rest))
64 (i : tr []) (r ::: {Unit}) (fold : folder r)= 64 (i : tr []) (r ::: {Unit}) (fold : folder r)=
65 fold [fn r :: {Unit} => $(mapUT tf r) -> tr r] 65 fold [fn r :: {Unit} => $(mapUT tf r) -> tr r]
66 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc 66 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
67 [[nm] ~ rest] r => 67 [[nm] ~ rest] r =>
68 f [nm] [rest] r.nm (acc (r -- nm))) 68 f [nm] [rest] ! r.nm (acc (r -- nm)))
69 (fn _ => i) 69 (fn _ => i)
70 70
71 fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type) 71 fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type)
72 (f : nm :: Name -> rest :: {Unit} 72 (f : nm :: Name -> rest :: {Unit}
73 -> fn [[nm] ~ rest] => 73 -> [[nm] ~ rest] =>
74 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) 74 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
75 (i : tr []) (r ::: {Unit}) (fold : folder r) = 75 (i : tr []) (r ::: {Unit}) (fold : folder r) =
76 fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r] 76 fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r]
77 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc 77 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
78 [[nm] ~ rest] r1 r2 => 78 [[nm] ~ rest] r1 r2 =>
79 f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) 79 f [nm] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
80 (fn _ _ => i) 80 (fn _ _ => i)
81 81
82 fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit}) 82 fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit})
83 (f : nm :: Name -> rest :: {Unit} 83 (f : nm :: Name -> rest :: {Unit}
84 -> fn [[nm] ~ rest] => 84 -> [[nm] ~ rest] =>
85 tf1 -> tf2 -> xml ctx [] []) = 85 tf1 -> tf2 -> xml ctx [] []) =
86 foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []] 86 foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
87 (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc => 87 (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc =>
88 <xml>{f [nm] [rest] v1 v2}{acc}</xml>) 88 <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>)
89 <xml/> 89 <xml/>
90 90
91 fun foldR K (tf :: K -> Type) (tr :: {K} -> Type) 91 fun foldR K (tf :: K -> Type) (tr :: {K} -> Type)
92 (f : nm :: Name -> t :: K -> rest :: {K} 92 (f : nm :: Name -> t :: K -> rest :: {K}
93 -> fn [[nm] ~ rest] => 93 -> [[nm] ~ rest] =>
94 tf t -> tr rest -> tr ([nm = t] ++ rest)) 94 tf t -> tr rest -> tr ([nm = t] ++ rest))
95 (i : tr []) (r ::: {K}) (fold : folder r) = 95 (i : tr []) (r ::: {K}) (fold : folder r) =
96 fold [fn r :: {K} => $(map tf r) -> tr r] 96 fold [fn r :: {K} => $(map tf r) -> tr r]
97 (fn (nm :: Name) (t :: K) (rest :: {K}) (acc : _ -> tr rest) 97 (fn (nm :: Name) (t :: K) (rest :: {K}) (acc : _ -> tr rest)
98 [[nm] ~ rest] r => 98 [[nm] ~ rest] r =>
99 f [nm] [t] [rest] r.nm (acc (r -- nm))) 99 f [nm] [t] [rest] ! r.nm (acc (r -- nm)))
100 (fn _ => i) 100 (fn _ => i)
101 101
102 fun foldR2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (tr :: {K} -> Type) 102 fun foldR2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (tr :: {K} -> Type)
103 (f : nm :: Name -> t :: K -> rest :: {K} 103 (f : nm :: Name -> t :: K -> rest :: {K}
104 -> fn [[nm] ~ rest] => 104 -> [[nm] ~ rest] =>
105 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 105 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
106 (i : tr []) (r ::: {K}) (fold : folder r) = 106 (i : tr []) (r ::: {K}) (fold : folder r) =
107 fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r] 107 fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
108 (fn (nm :: Name) (t :: K) (rest :: {K}) 108 (fn (nm :: Name) (t :: K) (rest :: {K})
109 (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => 109 (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
110 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) 110 f [nm] [t] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
111 (fn _ _ => i) 111 (fn _ _ => i)
112 112
113 fun foldRX K (tf :: K -> Type) (ctx :: {Unit}) 113 fun foldRX K (tf :: K -> Type) (ctx :: {Unit})
114 (f : nm :: Name -> t :: K -> rest :: {K} 114 (f : nm :: Name -> t :: K -> rest :: {K}
115 -> fn [[nm] ~ rest] => 115 -> [[nm] ~ rest] =>
116 tf t -> xml ctx [] []) = 116 tf t -> xml ctx [] []) =
117 foldR [tf] [fn _ => xml ctx [] []] 117 foldR [tf] [fn _ => xml ctx [] []]
118 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] r acc => 118 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] r acc =>
119 <xml>{f [nm] [t] [rest] r}{acc}</xml>) 119 <xml>{f [nm] [t] [rest] ! r}{acc}</xml>)
120 <xml/> 120 <xml/>
121 121
122 fun foldRX2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit}) 122 fun foldRX2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit})
123 (f : nm :: Name -> t :: K -> rest :: {K} 123 (f : nm :: Name -> t :: K -> rest :: {K}
124 -> fn [[nm] ~ rest] => 124 -> [[nm] ~ rest] =>
125 tf1 t -> tf2 t -> xml ctx [] []) = 125 tf1 t -> tf2 t -> xml ctx [] []) =
126 foldR2 [tf1] [tf2] [fn _ => xml ctx [] []] 126 foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
127 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] 127 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest]
128 r1 r2 acc => 128 r1 r2 acc =>
129 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) 129 <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>)
130 <xml/> 130 <xml/>
131 131
132 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) 132 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
133 (q : sql_query tables exps) [tables ~ exps] 133 (q : sql_query tables exps) [tables ~ exps]
134 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) 134 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
146 r <- f fs; 146 r <- f fs;
147 return <xml>{acc}{r}</xml>) 147 return <xml>{acc}{r}</xml>)
148 <xml/> 148 <xml/>
149 149
150 fun oneOrNoRows (tables ::: {{Type}}) (exps ::: {Type}) 150 fun oneOrNoRows (tables ::: {{Type}}) (exps ::: {Type})
151 (q : sql_query tables exps) [tables ~ exps] = 151 [tables ~ exps]
152 (q : sql_query tables exps) =
152 query q 153 query q
153 (fn fs _ => return (Some fs)) 154 (fn fs _ => return (Some fs))
154 None 155 None
155 156
156 fun oneRow (tables ::: {{Type}}) (exps ::: {Type}) 157 fun oneRow (tables ::: {{Type}}) (exps ::: {Type})
157 (q : sql_query tables exps) [tables ~ exps] = 158 [tables ~ exps] (q : sql_query tables exps) =
158 o <- oneOrNoRows q; 159 o <- oneOrNoRows q;
159 return (case o of 160 return (case o of
160 None => error <xml>Query returned no rows</xml> 161 None => error <xml>Query returned no rows</xml>
161 | Some r => r) 162 | Some r => r)
162 163