12 år sedan · 3767869c7f
--- a/UrWeb/bench.ur
+++ b/UrWeb/bench.ur
@@ -0,0 +1,114 @@
 
				+open Json
			
 
				+
			
 
				+fun addHeaders () =
			
 
				+  n <- now;
			
 
				+  setHeader (blessResponseHeader "Date") (timef "%a, %d %b %Y %H:%M:%S GMT" n);
			
 
				+  setHeader (blessResponseHeader "Server") "Ur/Web"
			
 
				+
			
 
				+
			
 
				+val hello = "Hello, World!"
			
 
				+fun plaintext () =
			
 
				+  addHeaders ();
			
 
				+  returnBlob (textBlob hello) (blessMime "text/plain")
			
 
				+
			
 
				+
			
 
				+type json_t = {Message : string}
			
 
				+fun json () =
			
 
				+  let
			
 
				+    val json_conversion : json json_t = json_record {Message = "message"}
			
 
				+    val hello_json : json_t = {Message = hello}
			
 
				+  in
			
 
				+    addHeaders ();
			
 
				+    returnBlob (textBlob (toJson hello_json)) (blessMime "application/json")
			
 
				+  end
			
 
				+
			
 
				+table world : {Id : int, RandomNumber : int} PRIMARY KEY Id
			
 
				+type world_t = {Id : int, RandomNumber : int}
			
 
				+val world_conversion : json world_t = json_record {Id = "id", RandomNumber = "randomNumber"}
			
 
				+fun world_find n =
			
 
				+  oneRow1 (SELECT World.Id, World.RandomNumber FROM world WHERE World.Id = {[n]})
			
 
				+
			
 
				+fun clamp n =
			
 
				+  (mod n 10000) + 1
			
 
				+
			
 
				+fun db () =
			
 
				+  addHeaders ();
			
 
				+  n <- rand;
			
 
				+  row <- world_find (clamp n);
			
 
				+  returnBlob (textBlob (toJson row)) (blessMime "application/json")
			
 
				+
			
 
				+fun parseQueries oqs =
			
 
				+  let
			
 
				+    val qt = case oqs of
			
 
				+        None => Some ("queries", "1")
			
 
				+      | Some qs => String.split (show qs) #"="
			
 
				+    val on = case qt of
			
 
				+        None => Some 1
			
 
				+      | Some ("queries", x) => read x
			
 
				+      | Some _ => Some 1
			
 
				+  in
			
 
				+    case on of
			
 
				+      None => 1
			
 
				+    | Some x => if x > 500 then 500
			
 
				+                else if x < 1 then 1
			
 
				+                else x
			
 
				+  end
			
 
				+
			
 
				+fun range n acc =
			
 
				+  case n of
			
 
				+      0 => acc
			
 
				+    | _ => range (n-1) (n :: acc)
			
 
				+
			
 
				+fun queries oqs =
			
 
				+  addHeaders ();
			
 
				+  let
			
 
				+    val rq = range (parseQueries oqs) []
			
 
				+  in
			
 
				+    rands <- List.mapM (fn _ => rand) rq;
			
 
				+    rows <- List.mapM (fn r => world_find (clamp r)) rands;
			
 
				+    returnBlob (textBlob (toJson rows)) (blessMime "application/json")
			
 
				+  end
			
 
				+
			
 
				+table fortune : {Id : int, Message : string} PRIMARY KEY Id
			
 
				+type fortune_t = {Id : int, Message : string}
			
 
				+fun fortunes () =
			
 
				+  addHeaders ();
			
 
				+  fs <- queryL1 (SELECT Fortune.Id, Fortune.Message FROM fortune);
			
 
				+  let
			
 
				+    val fortune_conversion : json fortune_t = json_record {Id = "id", Message = "message"}
			
 
				+    val new_fortune : fortune_t = {Id = 0, Message = "Additional fortune added at request time"}
			
 
				+    val fs' = List.sort (fn x y => x.Message > y.Message ) (new_fortune :: fs)
			
 
				+    val tabled = List.mapX (fn row =>
			
 
				+      <xml>
			
 
				+        <tr><td>{[row.Id]}</td><td>{[row.Message]}</td></tr>
			
 
				+      </xml>) fs'
			
 
				+  in
			
 
				+    return <xml>
			
 
				+             <head><title>Fortunes</title></head>
			
 
				+             <body><table>
			
 
				+               <tr><th>id</th><th>message</th></tr>
			
 
				+               {tabled}
			
 
				+             </table></body>
			
 
				+           </xml>
			
 
				+  end
			
 
				+
			
 
				+fun updates oqs =
			
 
				+  addHeaders ();
			
 
				+  let
			
 
				+    fun map2 f ls1 ls2 =
			
 
				+      case (ls1, ls2) of
			
 
				+        ([], []) => []
			
 
				+      | (x1 :: ls1, x2 :: ls2) => (f x1 x2) :: map2 f ls1 ls2
			
 
				+      | _ => error <xml>map2: Unequal list lengths</xml>
			
 
				+    val rq = range (parseQueries oqs) []
			
 
				+  in
			
 
				+    rands <- List.mapM (fn _ => rand) rq;
			
 
				+    rows <- List.mapM (fn r => world_find (clamp r)) rands;
			
 
				+    rands' <- List.mapM (fn _ => rand) rq;
			
 
				+    let
			
 
				+      val rows' = map2 (fn x y => x -- #RandomNumber ++ {RandomNumber = clamp y}) rows rands'
			
 
				+    in
			
 
				+      u <- List.mapM (fn r => dml (UPDATE world SET RandomNumber = {[r.RandomNumber]} WHERE Id = {[r.Id]})) rows';
			
 
				+      returnBlob (textBlob (toJson rows')) (blessMime "application/json")
			
 
				+    end
			
 
				+  end
			
--- a/UrWeb/bench.urp
+++ b/UrWeb/bench.urp
@@ -0,0 +1,12 @@
 
				+library meta
			
 
				+database dbname=hello_world user=benchmarkdbuser password=benchmarkdbpass host=localhost
			
 
				+rewrite url Bench/*
			
 
				+allow responseHeader Date
			
 
				+allow responseHeader Server
			
 
				+allow mime application/json
			
 
				+allow mime text/plain
			
 
				+safeGet updates
			
 
				+
			
 
				+$/list
			
 
				+$/string
			
 
				+bench
			
--- a/UrWeb/bench.urs
+++ b/UrWeb/bench.urs
@@ -0,0 +1,6 @@
 
				+val json : unit -> transaction page
			
 
				+val plaintext : unit -> transaction page
			
 
				+val db : unit -> transaction page
			
 
				+val queries: option queryString -> transaction page
			
 
				+val fortunes: unit -> transaction page
			
 
				+val updates: option queryString -> transaction page
			
--- a/UrWeb/fortune.sql
+++ b/UrWeb/fortune.sql
@@ -0,0 +1,14 @@
 
				+CREATE TABLE uw_Bench_fortune(uw_id int8 NOT NULL, uw_message text NOT NULL,
			
 
				+  PRIMARY KEY (uw_id));
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (11, '<script>alert("This should not be displayed in a browser alert box.")</script>');
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (4, 'A bad random number generator: 1, 1, 1, 1, 1, 4.33e+67, 1, 1, 1');
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (5, 'A computer program does what you tell it to do, not what you want it to do.');
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (2, 'A computer scientist is someone who fixes things that aren''t broken.');
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (8, 'A list is only as strong as its weakest link. — Donald Knuth');
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (3, 'After enough decimal places, nobody gives a damn.');
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (7, 'Any program that runs right is obsolete.');
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (10, 'Computers make very fast, very accurate mistakes.');
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (6, 'Emacs is a nice operating system, but I prefer UNIX. — Tom Christaensen');
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (9, 'Feature: A bug with seniority.');
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (1, 'fortune: No such file or directory');
			
 
				+INSERT INTO uw_Bench_fortune (uw_id, uw_message) VALUES (12, 'フレームワークのベンチマーク');
			
--- a/UrWeb/meta/LICENSE
+++ b/UrWeb/meta/LICENSE
@@ -0,0 +1,25 @@
 
				+Copyright (c) 2009-2010, Adam Chlipala
			
 
				+All rights reserved.
			
 
				+
			
 
				+Redistribution and use in source and binary forms, with or without
			
 
				+modification, are permitted provided that the following conditions are met:
			
 
				+
			
 
				+- Redistributions of source code must retain the above copyright notice,
			
 
				+  this list of conditions and the following disclaimer.
			
 
				+- Redistributions in binary form must reproduce the above copyright notice,
			
 
				+  this list of conditions and the following disclaimer in the documentation
			
 
				+  and/or other materials provided with the distribution.
			
 
				+- The names of contributors may not be used to endorse or promote products
			
 
				+  derived from this software without specific prior written permission.
			
 
				+
			
 
				+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
			
 
				+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
			
 
				+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
			
 
				+ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
			
 
				+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
			
 
				+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
			
 
				+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
			
 
				+INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
			
 
				+CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
			
 
				+ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
			
 
				+POSSIBILITY OF SUCH DAMAGE.
			
--- a/UrWeb/meta/eq.ur
+++ b/UrWeb/meta/eq.ur
@@ -0,0 +1,76 @@
 
				+con eq = K ==> fn (t1 :: K) (t2 :: K) => f :: (K -> Type) -> f t1 -> f t2
			
 
				+
			
 
				+val refl [K] [t ::: K] : eq t t = fn [f :: (K -> Type)] x => x
			
 
				+
			
 
				+fun sym [K] [t1 ::: K] [t2 ::: K] (e : eq t1 t2) : eq t2 t1 =
			
 
				+    e [fn t => eq t t1] refl
			
 
				+
			
 
				+fun trans [K] [t1 ::: K] [t2 ::: K] [t3 ::: K] (e1 : eq t1 t2) (e2 : eq t2 t3) : eq t1 t3 =
			
 
				+    (sym e1) [fn t => eq t t3] e2
			
 
				+
			
 
				+fun cast [K] [t1 ::: K] [t2 ::: K] (e : eq t1 t2) = e
			
 
				+
			
 
				+fun fold [K] [tf :: {K} -> Type] [r ::: {K}]
			
 
				+         (f : pre :: {K} -> nm :: Name -> v :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+          eq r (pre ++ [nm = v] ++ post) -> tf post -> tf ([nm = v] ++ post))
			
 
				+    (i : tf []) (fl : folder r) : tf r =
			
 
				+    @@Top.fold [fn post => pre :: {K} -> [pre ~ post] => eq r (pre ++ post) -> tf post]
			
 
				+     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
			
 
				+                      (acc : pre :: {K} -> [pre ~ rest] => eq r (pre ++ rest) -> tf rest)
			
 
				+                      [pre :: {K}] [pre ~ [nm = t] ++ rest] pf =>
			
 
				+         f [pre] [nm] [t] [rest] pf (acc [[nm = t] ++ pre] pf))
			
 
				+     (fn [pre :: {K}] [pre ~ []] _ => i) [r] fl [[]] ! refl
			
 
				+
			
 
				+fun foldUR [tr :: Type] [tf :: {Unit} -> Type] [r ::: {Unit}]
			
 
				+    (f : pre :: {Unit} -> nm :: Name -> post :: {Unit} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+     eq r (pre ++ [nm] ++ post) -> tr -> tf post -> tf ([nm] ++ post))
			
 
				+    (i : tf []) (fl : folder r) (r : $(mapU tr r)) : tf r =
			
 
				+    @@fold [fn r' => $(mapU tr r') -> tf r'] [r]
			
 
				+      (fn [pre :: {Unit}] [nm :: Name] [u :: Unit] [post :: {Unit}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r =>
			
 
				+          f [pre] [nm] [post] pf r.nm (acc (r -- nm)))
			
 
				+      (fn _ => i) fl r
			
 
				+
			
 
				+fun foldR [K] [tr :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
			
 
				+    (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+     eq r (pre ++ [nm = t] ++ post) -> tr t -> tf post -> tf ([nm = t] ++ post))
			
 
				+    (i : tf []) (fl : folder r) (r : $(map tr r)) : tf r =
			
 
				+    @@fold [fn r' => $(map tr r') -> tf r'] [r]
			
 
				+      (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r =>
			
 
				+          f [pre] [nm] [t] [post] pf r.nm (acc (r -- nm)))
			
 
				+      (fn _ => i) fl r
			
 
				+
			
 
				+fun foldR2 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
			
 
				+    (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+     eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tf post -> tf ([nm = t] ++ post))
			
 
				+    (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) : tf r =
			
 
				+    @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> tf r'] [r]
			
 
				+      (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 =>
			
 
				+          f [pre] [nm] [t] [post] pf r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
			
 
				+      (fn _ _ => i) fl r1 r2
			
 
				+
			
 
				+fun foldR3 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
			
 
				+    (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+     eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tf post -> tf ([nm = t] ++ post))
			
 
				+    (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) : tf r =
			
 
				+    @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> tf r'] [r]
			
 
				+      (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 =>
			
 
				+          f [pre] [nm] [t] [post] pf r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
			
 
				+      (fn _ _ _ => i) fl r1 r2 r3
			
 
				+
			
 
				+fun foldR4 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tr4 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
			
 
				+    (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+     eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tr4 t -> tf post -> tf ([nm = t] ++ post))
			
 
				+    (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) (r4 : $(map tr4 r)) : tf r =
			
 
				+    @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> $(map tr4 r') -> tf r'] [r]
			
 
				+      (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 r4 =>
			
 
				+          f [pre] [nm] [t] [post] pf r1.nm r2.nm r3.nm r4.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm) (r4 -- nm)))
			
 
				+      (fn _ _ _ _ => i) fl r1 r2 r3 r4
			
 
				+
			
 
				+fun mp [K] [tr :: K -> Type] [tf :: K -> Type] [r ::: {K}]
			
 
				+       (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] =>
			
 
				+        eq r ([nm = t] ++ rest) -> tr t -> tf t)
			
 
				+    (fl : folder r) (r : $(map tr r)) : $(map tf r) =
			
 
				+  @@foldR [tr] [fn r => $(map tf r)] [r]
			
 
				+      (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf r acc =>
			
 
				+          {nm = f [nm] [t] [pre ++ post] pf r} ++ acc)
			
 
				+      {} fl r
			
--- a/UrWeb/meta/eq.urs
+++ b/UrWeb/meta/eq.urs
@@ -0,0 +1,44 @@
 
				+(** A constructor equality predicate *)
			
 
				+
			
 
				+con eq :: K --> K -> K -> Type
			
 
				+
			
 
				+val refl : K --> t ::: K -> eq t t
			
 
				+val sym : K --> t1 ::: K -> t2 ::: K -> eq t1 t2 -> eq t2 t1
			
 
				+val trans : K --> t1 ::: K -> t2 ::: K -> t3 ::: K -> eq t1 t2 -> eq t2 t3 -> eq t1 t3
			
 
				+
			
 
				+val cast : K --> t1 ::: K -> t2 ::: K -> eq t1 t2 -> f :: (K -> Type) -> f t1 -> f t2
			
 
				+
			
 
				+val fold : K --> tf :: ({K} -> Type) -> r ::: {K}
			
 
				+           -> (pre :: {K} -> nm :: Name -> v :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+               eq r (pre ++ [nm = v] ++ post) -> tf post -> tf ([nm = v] ++ post))
			
 
				+           -> tf [] -> folder r -> tf r
			
 
				+
			
 
				+val foldUR : tr :: Type -> tf :: ({Unit} -> Type) -> r ::: {Unit}
			
 
				+           -> (pre :: {Unit} -> nm :: Name -> post :: {Unit} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+               eq r (pre ++ [nm] ++ post) -> tr -> tf post -> tf ([nm] ++ post))
			
 
				+           -> tf [] -> folder r -> $(mapU tr r) -> tf r
			
 
				+
			
 
				+val foldR : K --> tr :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
			
 
				+           -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+               eq r (pre ++ [nm = t] ++ post) -> tr t -> tf post -> tf ([nm = t] ++ post))
			
 
				+           -> tf [] -> folder r -> $(map tr r) -> tf r
			
 
				+
			
 
				+val foldR2 : K --> tr1 :: (K -> Type) -> tr2 :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
			
 
				+             -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+                 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tf post -> tf ([nm = t] ++ post))
			
 
				+             -> tf [] -> folder r -> $(map tr1 r) -> $(map tr2 r) -> tf r
			
 
				+
			
 
				+val foldR3 : K --> tr1 :: (K -> Type) -> tr2 :: (K -> Type) -> tr3 :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
			
 
				+             -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+                 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tf post -> tf ([nm = t] ++ post))
			
 
				+             -> tf [] -> folder r -> $(map tr1 r) -> $(map tr2 r) -> $(map tr3 r) -> tf r
			
 
				+
			
 
				+val foldR4 : K --> tr1 :: (K -> Type) -> tr2 :: (K -> Type) -> tr3 :: (K -> Type) -> tr4 :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
			
 
				+             -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
			
 
				+                 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tr4 t -> tf post -> tf ([nm = t] ++ post))
			
 
				+             -> tf [] -> folder r -> $(map tr1 r) -> $(map tr2 r) -> $(map tr3 r) -> $(map tr4 r) -> tf r
			
 
				+
			
 
				+val mp : K --> tr :: (K -> Type) -> tf :: (K -> Type) -> r ::: {K}
			
 
				+         -> (nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] =>
			
 
				+             eq r ([nm = t] ++ rest) -> tr t -> tf t)
			
 
				+         -> folder r -> $(map tr r) -> $(map tf r)
			
--- a/UrWeb/meta/html.ur
+++ b/UrWeb/meta/html.ur
@@ -0,0 +1,144 @@
 
				+open Parse
			
 
				+
			
 
				+con attribute = fn t => {Nam : string,
			
 
				+                         Parse : string -> option t}
			
 
				+
			
 
				+con tag = fn ts => {Nam : string,
			
 
				+                    Attributes : $(map attribute ts),
			
 
				+                    Folder : folder ts,
			
 
				+                    Construct : ctx ::: {Unit} -> [[Body] ~ ctx] => $ts
			
 
				+                                -> xml ([Body] ++ ctx) [] [] -> xml ([Body] ++ ctx) [] []}
			
 
				+
			
 
				+fun tag [use] [ignore] [use ~ ignore] (fl : folder use) (name : string) (attrs : $(map attribute use))
			
 
				+        (construct : ctx ::: {Unit} -> [[Body] ~ ctx] => Basis.tag (use ++ ignore) ([Body] ++ ctx) ([Body] ++ ctx) [] []) =
			
 
				+    {Nam = name,
			
 
				+     Attributes = attrs,
			
 
				+     Folder = fl,
			
 
				+     Construct = fn [ctx] [[Body] ~ ctx] (ats : $use) (inner : xml ([Body] ++ ctx) [] []) =>
			
 
				+                    Basis.tag null None noStyle None ats construct inner}
			
 
				+
			
 
				+fun simpleTag [ignore] name (bt : bodyTag ignore) : tag [] =
			
 
				+    @@tag [[]] [ignore] ! _ name {} (fn [ctx] [[Body] ~ ctx] => bt ())
			
 
				+
			
 
				+fun simpleTag' [use] [ignore] [use ~ ignore] (fl : folder use)
			
 
				+               name (bt : bodyTag (use ++ ignore)) (ats : $(map attribute use)) : tag use =
			
 
				+    @@tag [use] [ignore] ! fl name ats (fn [ctx] [[Body] ~ ctx] => bt ())
			
 
				+
			
 
				+fun url name = {Nam = name,
			
 
				+                Parse = checkUrl}
			
 
				+
			
 
				+datatype error a =
			
 
				+         Good of a
			
 
				+       | Bad of string
			
 
				+
			
 
				+fun format [tags] (fl : folder tags) (tags : $(map tag tags)) [ctx] [[Body] ~ ctx] s =
			
 
				+    let
			
 
				+        fun loop s : error (xml ([Body] ++ ctx) [] [] * string) =
			
 
				+            case String.msplit {Haystack = s, Needle = "&<"} of
			
 
				+                None => Good (cdata s, "")
			
 
				+              | Some (pre, ch, post) =>
			
 
				+                case ch of
			
 
				+                    #"&" =>
			
 
				+                    (case String.split post #";" of
			
 
				+                         None => Bad "No ';' after '&'"
			
 
				+                       | Some (code, post) =>
			
 
				+                         let
			
 
				+                             val xml = 
			
 
				+                                 case code of
			
 
				+                                     "lt" => <xml>&lt;</xml>
			
 
				+                                   | "gt" => <xml>&gt;</xml>
			
 
				+                                   | "amp" => <xml>&amp;</xml>
			
 
				+                                   | _ => <xml/>
			
 
				+                         in
			
 
				+                             case loop post of
			
 
				+                                 Good (after, post) => Good (<xml>{[pre]}{xml}{after}</xml>, post)
			
 
				+                               | x => x
			
 
				+                         end)
			
 
				+                  | _ =>
			
 
				+                    if String.length post > 0 && String.sub post 0 = #"/" then
			
 
				+                        case String.split post #"\x3E" of
			
 
				+                            None => Bad "No '>' after '</'"
			
 
				+                          | Some (_, post) => Good (<xml>{[pre]}</xml>, post)
			
 
				+                    else
			
 
				+                        case String.msplit {Haystack = post, Needle = " >"} of
			
 
				+                            None => Bad "No '>' after '<'"
			
 
				+                          | Some (tname, ch, post) =>
			
 
				+                            @foldR [tag] [fn _ => unit -> error (xml ([Body] ++ ctx) [] [] * string)]
			
 
				+                            (fn [nm :: Name] [ts :: {Type}] [r :: {{Type}}] [[nm] ~ r] (meta : tag ts) acc () =>
			
 
				+                                if meta.Nam = tname then
			
 
				+                                    let
			
 
				+                                        fun doAttrs (ch, post, ats : $(map option ts)) =
			
 
				+                                            if String.length post > 0 && Char.isSpace (String.sub post 0) then
			
 
				+                                                doAttrs (ch, String.substring post {Start = 1,
			
 
				+                                                                                    Len = String.length post - 1},
			
 
				+                                                         ats)
			
 
				+                                            else 
			
 
				+                                                case ch of
			
 
				+                                                    #"\x3E" => Good (ats, post)
			
 
				+                                                  | _ =>
			
 
				+                                                    case String.split post #"=" of
			
 
				+                                                        None =>
			
 
				+                                                        (case String.split post #"\x3E" of
			
 
				+                                                             None => Bad "No tag ender '\x3E'"
			
 
				+                                                           | Some (_, post) => Good (ats, post))
			
 
				+                                                      | Some (aname, post) =>
			
 
				+                                                        if String.length post >= 1 && String.sub post 0 = #"\"" then
			
 
				+                                                            case String.split (String.substring post
			
 
				+                                                                                                {Start = 1,
			
 
				+                                                                                                 Len = String.length post
			
 
				+                                                                                                       - 1})
			
 
				+                                                                              #"\"" of
			
 
				+                                                                None => Bad "No '\"' to end attribute value"
			
 
				+                                                              | Some (aval, post) =>
			
 
				+                                                                let
			
 
				+                                                                    val ats =
			
 
				+                                                                        @map2 [attribute] [option] [option]
			
 
				+                                                                         (fn [t] meta v =>
			
 
				+                                                                             if aname = meta.Nam then
			
 
				+                                                                                 meta.Parse aval
			
 
				+                                                                             else
			
 
				+                                                                                 v)
			
 
				+                                                                         meta.Folder meta.Attributes ats
			
 
				+                                                                in
			
 
				+                                                                    doAttrs (#" ", post, ats)
			
 
				+                                                                end
			
 
				+                                                        else
			
 
				+                                                            Bad "Attribute value doesn't begin with quote"
			
 
				+                                    in
			
 
				+                                        case doAttrs (ch, post, @map0 [option] (fn [t :: Type] => None)
			
 
				+                                                                 meta.Folder) of
			
 
				+                                            Good (ats, post) =>
			
 
				+                                            let
			
 
				+                                                val ats =
			
 
				+                                                    @map2 [attribute] [option] [ident]
			
 
				+                                                     (fn [t] meta v =>
			
 
				+                                                         case v of
			
 
				+                                                             None => error <xml>Missing attribute {[meta.Nam]}
			
 
				+                                                               for {[tname]}</xml>
			
 
				+                                                           | Some v => v)
			
 
				+                                                     meta.Folder meta.Attributes ats
			
 
				+                                            in
			
 
				+                                                case loop post of
			
 
				+                                                    Good (inner, post) =>
			
 
				+                                                    (case loop post of
			
 
				+                                                         Good (after, post) =>
			
 
				+                                                         Good (<xml>{[pre]}{meta.Construct [ctx] !
			
 
				+                                                                                           ats inner}{after}</xml>, post)
			
 
				+                                                       | x => x)
			
 
				+                                                  | x => x
			
 
				+                                            end
			
 
				+                                          | Bad s => Bad s
			
 
				+                                    end
			
 
				+                                else
			
 
				+                                    acc ())
			
 
				+                            (fn () => Bad ("Unknown HTML tag " ^ tname)) fl tags ()
			
 
				+    in
			
 
				+        case loop s of
			
 
				+            Bad msg => Failure msg
			
 
				+          | Good (xml, _) => Success xml
			
 
				+    end
			
 
				+
			
 
				+val b = simpleTag "b" @@b
			
 
				+val i = simpleTag "i" @@i
			
 
				+val a = simpleTag' "a" @@a {Href = url "href"}
			
 
				+
			
--- a/UrWeb/meta/html.urs
+++ b/UrWeb/meta/html.urs
@@ -0,0 +1,29 @@
 
				+(** Safe HTML parsing *)
			
 
				+
			
 
				+con attribute = fn t => {Nam : string,
			
 
				+                         Parse : string -> option t}
			
 
				+
			
 
				+con tag = fn ts => {Nam : string,
			
 
				+                    Attributes : $(map attribute ts),
			
 
				+                    Folder : folder ts,
			
 
				+                    Construct : ctx ::: {Unit} -> [[Body] ~ ctx] => $ts
			
 
				+                                -> xml ([Body] ++ ctx) [] [] -> xml ([Body] ++ ctx) [] []}
			
 
				+
			
 
				+val tag : use ::: {Type} -> ignore ::: {Type} -> [use ~ ignore] => folder use -> string
			
 
				+          -> $(map attribute use)
			
 
				+          -> (ctx ::: {Unit} -> [[Body] ~ ctx] => Basis.tag (use ++ ignore) ([Body] ++ ctx) ([Body] ++ ctx) [] [])
			
 
				+          -> tag use
			
 
				+
			
 
				+val simpleTag : ignore ::: {Type} -> string -> bodyTag ignore -> tag []
			
 
				+val simpleTag' : use ::: {Type} -> ignore ::: {Type} -> [use ~ ignore] => folder use
			
 
				+    -> string -> bodyTag (use ++ ignore) -> $(map attribute use) -> tag use
			
 
				+
			
 
				+val url : string -> attribute url
			
 
				+
			
 
				+val format : tags ::: {{Type}} -> folder tags -> $(map tag tags)
			
 
				+             -> ctx ::: {Unit} -> [[Body] ~ ctx] => string
			
 
				+             -> Parse.parse (xml ([Body] ++ ctx) [] [])
			
 
				+
			
 
				+val b : tag []
			
 
				+val i : tag []
			
 
				+val a : tag [Href = url]
			
--- a/UrWeb/meta/incl.ur
+++ b/UrWeb/meta/incl.ur
@@ -0,0 +1,40 @@
 
				+con incl' = K ==> fn (r1 :: {K}) (r2 :: {K}) (r' :: {K}) =>
			
 
				+                     [r1 ~ r'] => {Expose : f :: ({K} -> Type) -> f r2 -> f (r1 ++ r'),
			
 
				+                                   Hide : f :: ({K} -> Type) -> f (r1 ++ r') -> f r2}
			
 
				+
			
 
				+con incl = K ==> fn (r1 :: {K}) (r2 :: {K}) =>
			
 
				+                    tp :: Type -> (r' :: {K} -> [r1 ~ r'] => incl' r1 r2 r' -> tp) -> tp
			
 
				+
			
 
				+fun incl [K] [r1 :: {K}] [r2 :: {K}] [r1 ~ r2] =
			
 
				+ fn [tp :: Type] (f : r' :: {K} -> [r1 ~ r'] => incl' r1 (r1 ++ r2) r' -> tp) =>
			
 
				+    f [r2] (fn [r1 ~ r2] => {Expose = fn [f :: ({K} -> Type)] x => x,
			
 
				+                             Hide = fn [f :: ({K} -> Type)] x => x})
			
 
				+    
			
 
				+fun proj [r1 ::: {Type}] [r2 ::: {Type}] (i : incl r1 r2) (r : $r2) =
			
 
				+    i [$r1] (fn [r' :: {Type}] [r1 ~ r'] (i' : incl' r1 r2 r') =>
			
 
				+                i'.Expose [fn r => $r] r --- r')
			
 
				+
			
 
				+fun inv1 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
			
 
				+         [f :: Name -> K -> {K} -> Type]
			
 
				+         (i : incl ([nm = t] ++ r) r')
			
 
				+         (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) =
			
 
				+    i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
			
 
				+                      i'.Hide [f nm t] (f [nm] [t] [r ++ r'']))
			
 
				+
			
 
				+fun inv2 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
			
 
				+         (i : incl ([nm = t] ++ r) r') =
			
 
				+    i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
			
 
				+                   fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) =>
			
 
				+                      f [[nm = t] ++ r''] (fn [r ~ [nm = t] ++ r''] =>
			
 
				+                                              {Expose = fn [f :: ({K} -> Type)] (x : f r') => i'.Expose [f] x,
			
 
				+                                               Hide = fn [f :: ({K} -> Type)] x => i'.Hide [f] x}))
			
 
				+
			
 
				+fun fold [K] [tf :: {K} -> Type] [r ::: {K}]
			
 
				+         (f : nm :: Name -> v :: K -> r' :: {K}
			
 
				+              -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r'))
			
 
				+         (i : tf []) (fl : folder r) =
			
 
				+    @Top.fold [fn r' => incl r' r -> tf r']
			
 
				+     (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i =>
			
 
				+         f [nm] [v] [r'] i (acc (inv2 [nm] [v] [r'] [r] i)))
			
 
				+     (fn _ => i)
			
 
				+     fl (incl [r] [[]])
			
--- a/UrWeb/meta/incl.urs
+++ b/UrWeb/meta/incl.urs
@@ -0,0 +1,22 @@
 
				+(** A record inclusion predicate *)
			
 
				+
			
 
				+con incl :: K --> {K} -> {K} -> Type
			
 
				+
			
 
				+val incl : K --> r1 :: {K} -> r2 :: {K} -> [r1 ~ r2] => incl r1 (r1 ++ r2)
			
 
				+val proj : r1 ::: {Type} -> r2 ::: {Type} -> incl r1 r2 -> $r2 -> $r1
			
 
				+
			
 
				+val inv1 : K --> nm :: Name -> t :: K -> r :: {K} -> r' :: {K}
			
 
				+           -> [[nm] ~ r] =>
			
 
				+    f :: (Name -> K -> {K} -> Type)
			
 
				+    -> incl ([nm = t] ++ r) r'
			
 
				+    -> (nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r))
			
 
				+    -> f nm t r'
			
 
				+val inv2 : K --> nm :: Name -> t :: K -> r :: {K} -> r' :: {K}
			
 
				+           -> [[nm] ~ r] =>
			
 
				+    incl ([nm = t] ++ r) r' -> incl r r'
			
 
				+
			
 
				+val fold : K --> tf :: ({K} -> Type) -> r ::: {K}
			
 
				+           -> (nm :: Name -> v :: K -> r' :: {K}
			
 
				+               -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r'))
			
 
				+           -> tf []
			
 
				+           -> folder r -> tf r
			
--- a/UrWeb/meta/json.ur
+++ b/UrWeb/meta/json.ur
@@ -0,0 +1,339 @@
 
				+con json a = {ToJson : a -> string,
			
 
				+              FromJson : string -> a * string}
			
 
				+
			
 
				+fun mkJson [a] (x : {ToJson : a -> string,
			
 
				+                     FromJson : string -> a * string}) = x
			
 
				+
			
 
				+fun skipSpaces s =
			
 
				+    let
			
 
				+        val len = String.length s
			
 
				+
			
 
				+        fun skip i =
			
 
				+            if i >= len then
			
 
				+                ""
			
 
				+            else
			
 
				+                let
			
 
				+                    val ch = String.sub s i
			
 
				+                in
			
 
				+                    if Char.isSpace ch then
			
 
				+                        skip (i+1)
			
 
				+                    else
			
 
				+                        String.substring s {Start = i, Len = len-i}
			
 
				+                end
			
 
				+    in
			
 
				+        skip 0
			
 
				+    end
			
 
				+
			
 
				+fun toJson [a] (j : json a) : a -> string = j.ToJson
			
 
				+fun fromJson' [a] (j : json a) : string -> a * string = j.FromJson
			
 
				+
			
 
				+fun fromJson [a] (j : json a) (s : string) : a =
			
 
				+    let
			
 
				+        val (v, s') = j.FromJson (skipSpaces s)
			
 
				+    in
			
 
				+        if String.all Char.isSpace s' then
			
 
				+            v
			
 
				+        else
			
 
				+            error <xml>Extra content at end of JSON record: {[s']}</xml>
			
 
				+    end
			
 
				+
			
 
				+fun escape s =
			
 
				+    let
			
 
				+        val len = String.length s
			
 
				+
			
 
				+        fun esc i =
			
 
				+            if i >= len then
			
 
				+                "\""
			
 
				+            else
			
 
				+                let
			
 
				+                    val ch = String.sub s i
			
 
				+                in
			
 
				+                    (if ch = #"\"" || ch = #"\\" then
			
 
				+                         "\\" ^ String.str ch
			
 
				+                     else
			
 
				+                         String.str ch) ^ esc (i+1)
			
 
				+                end
			
 
				+    in
			
 
				+        "\"" ^ esc 0
			
 
				+    end
			
 
				+
			
 
				+fun unescape s =
			
 
				+    let
			
 
				+        val len = String.length s
			
 
				+
			
 
				+        fun findEnd i =
			
 
				+            if i >= len then
			
 
				+                error <xml>JSON unescape: string ends before quote: {[s]}</xml>
			
 
				+            else
			
 
				+                let
			
 
				+                    val ch = String.sub s i
			
 
				+                in
			
 
				+                    case ch of
			
 
				+                        #"\"" => i
			
 
				+                      | #"\\" =>
			
 
				+                        if i+1 >= len then
			
 
				+                            error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
			
 
				+                        else
			
 
				+                            findEnd (i+2)
			
 
				+                      | _ => findEnd (i+1)
			
 
				+                end
			
 
				+
			
 
				+        val last = findEnd 1
			
 
				+
			
 
				+        fun unesc i =
			
 
				+            if i >= last then
			
 
				+                ""
			
 
				+            else
			
 
				+                let
			
 
				+                    val ch = String.sub s i
			
 
				+                in
			
 
				+                    case ch of
			
 
				+                        #"\\" =>
			
 
				+                        if i+1 >= len then
			
 
				+                            error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
			
 
				+                        else
			
 
				+                            String.str (String.sub s (i+1)) ^ unesc (i+2)
			
 
				+                      | _ => String.str ch ^ unesc (i+1)
			
 
				+                end
			
 
				+    in
			
 
				+        if len = 0 || String.sub s 0 <> #"\"" then
			
 
				+            error <xml>JSON unescape: String doesn't start with double quote: {[s]}</xml>
			
 
				+        else
			
 
				+            (unesc 1, String.substring s {Start = last+1, Len = len-last-1})
			
 
				+    end
			
 
				+
			
 
				+val json_string = {ToJson = escape,
			
 
				+                   FromJson = unescape}
			
 
				+
			
 
				+fun numIn [a] (_ : read a) s : a * string =
			
 
				+    let
			
 
				+        val len = String.length s
			
 
				+
			
 
				+        fun findEnd i =
			
 
				+            if i >= len then
			
 
				+                i
			
 
				+            else
			
 
				+                let
			
 
				+                    val ch = String.sub s i
			
 
				+                in
			
 
				+                    if Char.isDigit ch || ch = #"-" || ch = #"." || ch = #"E" || ch = #"e" then
			
 
				+                        findEnd (i+1)
			
 
				+                    else
			
 
				+                        i
			
 
				+                end
			
 
				+
			
 
				+        val last = findEnd 0
			
 
				+    in
			
 
				+        (readError (String.substring s {Start = 0, Len = last}), String.substring s {Start = last, Len = len-last})
			
 
				+    end
			
 
				+
			
 
				+fun json_num [a] (_ : show a) (_ : read a) : json a = {ToJson = show,
			
 
				+                                                       FromJson = numIn}
			
 
				+
			
 
				+val json_int = json_num
			
 
				+val json_float = json_num
			
 
				+
			
 
				+val json_bool = {ToJson = fn b => if b then "true" else "false",
			
 
				+                 FromJson = fn s => if String.isPrefix {Full = s, Prefix = "true"} then
			
 
				+                                        (True, String.substring s {Start = 4, Len = String.length s - 4})
			
 
				+                                    else if String.isPrefix {Full = s, Prefix = "false"} then
			
 
				+                                        (False, String.substring s {Start = 5, Len = String.length s - 5})
			
 
				+                                    else
			
 
				+                                        error <xml>JSON: bad boolean string: {[s]}</xml>}
			
 
				+
			
 
				+fun json_option [a] (j : json a) : json (option a) =
			
 
				+    {ToJson = fn v => case v of
			
 
				+                          None => "null"
			
 
				+                        | Some v => j.ToJson v,
			
 
				+     FromJson = fn s => if String.isPrefix {Full = s, Prefix = "null"} then
			
 
				+                            (None, String.substring s {Start = 4, Len = String.length s - 4})
			
 
				+                        else
			
 
				+                            let
			
 
				+                                val (v, s') = j.FromJson s
			
 
				+                            in
			
 
				+                                (Some v, s')
			
 
				+                            end}
			
 
				+
			
 
				+fun json_list [a] (j : json a) : json (list a) =
			
 
				+    let
			
 
				+        fun toJ' (ls : list a) : string =
			
 
				+            case ls of
			
 
				+                [] => ""
			
 
				+              | x :: ls => "," ^ toJson j x ^ toJ' ls
			
 
				+
			
 
				+        fun toJ (x : list a) : string =
			
 
				+            case x of
			
 
				+                [] => "[]"
			
 
				+              | x :: [] => "[" ^ toJson j x ^ "]"
			
 
				+              | x :: ls => "[" ^ toJson j x ^ toJ' ls ^ "]"
			
 
				+
			
 
				+        fun fromJ (s : string) : list a * string =
			
 
				+            let
			
 
				+                fun fromJ' (s : string) : list a * string =
			
 
				+                    if String.length s = 0 then
			
 
				+                        error <xml>JSON list doesn't end with ']'</xml>
			
 
				+                    else
			
 
				+                        let
			
 
				+                            val ch = String.sub s 0
			
 
				+                        in
			
 
				+                            case ch of
			
 
				+                                #"]" => ([], String.substring s {Start = 1, Len = String.length s - 1})
			
 
				+                              | _ =>
			
 
				+                                let
			
 
				+                                    val (x, s') = j.FromJson s
			
 
				+                                    val s' = skipSpaces s'
			
 
				+                                    val s' = if String.length s' = 0 then
			
 
				+                                                 error <xml>JSON list doesn't end with ']'</xml>
			
 
				+                                             else if String.sub s' 0 = #"," then
			
 
				+                                                 skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
			
 
				+                                             else
			
 
				+                                                 s'
			
 
				+
			
 
				+                                    val (ls, s'') = fromJ' s'
			
 
				+                                in
			
 
				+                                    (x :: ls, s'')
			
 
				+                                end
			
 
				+                        end
			
 
				+            in
			
 
				+                if String.length s = 0 || String.sub s 0 <> #"[" then
			
 
				+                    error <xml>JSON list doesn't start with '[': {[s]}</xml>
			
 
				+                else
			
 
				+                    fromJ' (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1}))
			
 
				+            end
			
 
				+    in
			
 
				+        {ToJson = toJ,
			
 
				+         FromJson = fromJ}
			
 
				+    end
			
 
				+
			
 
				+fun json_record [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json $ts =
			
 
				+    {ToJson = fn r => "{" ^ @foldR3 [json] [fn _ => string] [ident] [fn _ => string]
			
 
				+                             (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc =>
			
 
				+                                 escape name ^ ":" ^ j.ToJson v ^ (case acc of
			
 
				+                                                                       "" => ""
			
 
				+                                                                     | _ => "," ^ acc))
			
 
				+                             "" fl jss names r ^ "}",
			
 
				+     FromJson = fn s =>
			
 
				+                   let
			
 
				+                       fun fromJ s (r : $(map option ts)) : $(map option ts) * string =
			
 
				+                           if String.length s = 0 then
			
 
				+                               error <xml>JSON object doesn't end in brace</xml>
			
 
				+                           else if String.sub s 0 = #"}" then
			
 
				+                               (r, String.substring s {Start = 1, Len = String.length s - 1})
			
 
				+                           else let
			
 
				+                                   val (name, s') = unescape s
			
 
				+                                   val s' = skipSpaces s'
			
 
				+                                   val s' = if String.length s' = 0 || String.sub s' 0 <> #":" then
			
 
				+                                                error <xml>No colon after JSON object field name</xml>
			
 
				+                                            else
			
 
				+                                                skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
			
 
				+
			
 
				+                                   val (r, s') = @foldR2 [json] [fn _ => string] [fn ts => $(map option ts) -> $(map option ts) * string]
			
 
				+                                                  (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name' acc r =>
			
 
				+                                                      if name = name' then
			
 
				+                                                          let
			
 
				+                                                              val (v, s') = j.FromJson s'
			
 
				+                                                          in
			
 
				+                                                              (r -- nm ++ {nm = Some v}, s')
			
 
				+                                                          end
			
 
				+                                                      else
			
 
				+                                                          let
			
 
				+                                                              val (r', s') = acc (r -- nm)
			
 
				+                                                          in
			
 
				+                                                              (r' ++ {nm = r.nm}, s')
			
 
				+                                                          end)
			
 
				+                                                  (fn _ => error <xml>Unknown JSON object field name {[name]}</xml>)
			
 
				+                                                  fl jss names r
			
 
				+
			
 
				+                                   val s' = skipSpaces s'
			
 
				+                                   val s' = if String.length s' <> 0 && String.sub s' 0 = #"," then
			
 
				+                                                skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
			
 
				+                                            else
			
 
				+                                                s'
			
 
				+                               in
			
 
				+                                   fromJ s' r
			
 
				+                               end
			
 
				+                   in
			
 
				+                       if String.length s = 0 || String.sub s 0 <> #"{" then
			
 
				+                           error <xml>JSON record doesn't begin with brace</xml>
			
 
				+                       else
			
 
				+                           let
			
 
				+                               val (r, s') = fromJ (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1}))
			
 
				+                                                   (@map0 [option] (fn [t ::_] => None) fl)
			
 
				+                           in
			
 
				+                               (@map2 [option] [fn _ => string] [ident] (fn [t] (v : option t) name =>
			
 
				+                                                                            case v of
			
 
				+                                                                                None => error <xml>Missing JSON object field {[name]}</xml>
			
 
				+                                                                              | Some v => v) fl r names, s')
			
 
				+                           end
			
 
				+                   end}
			
 
				+
			
 
				+fun json_variant [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json (variant ts) =
			
 
				+    {ToJson = fn r => let val jnames = @map2 [json] [fn _ => string] [fn x => json x * string]
			
 
				+                                     (fn [t] (j : json t) (name : string) => (j, name)) fl jss names
			
 
				+                      in @Variant.destrR [ident] [fn x => json x * string]
			
 
				+                          (fn [p ::_] (v : p) (j : json p, name : string) =>
			
 
				+                            "{" ^ escape name ^ ":" ^ j.ToJson v ^ "}") fl r jnames
			
 
				+                      end,
			
 
				+     FromJson = fn s =>
			
 
				+                   if String.length s = 0 || String.sub s 0 <> #"{" then
			
 
				+                       error <xml>JSON variant doesn't begin with brace</xml>
			
 
				+                   else
			
 
				+                       let
			
 
				+                           val (name, s') = unescape (skipSpaces (String.suffix s 1))
			
 
				+                           val s' = skipSpaces s'
			
 
				+                           val s' = if String.length s' = 0 || String.sub s' 0 <> #":" then
			
 
				+                                        error <xml>No colon after JSON object field name</xml>
			
 
				+                                    else
			
 
				+                                        skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
			
 
				+
			
 
				+                           val (r, s') = (@foldR2 [json] [fn _ => string]
			
 
				+                                            [fn ts => ts' :: {Type} -> [ts ~ ts'] => variant (ts ++ ts') * string]
			
 
				+                                            (fn [nm ::_] [t ::_] [rest ::_] [[nm] ~ rest] (j : json t) name'
			
 
				+                                             (acc : ts' :: {Type} -> [rest ~ ts'] => variant (rest ++ ts') * string) [fwd ::_] [[nm = t] ++ rest ~ fwd] =>
			
 
				+                                                if name = name'
			
 
				+                                                    then
			
 
				+                                                        let val (v, s') = j.FromJson s'
			
 
				+                                                        in (make [nm] v, s')
			
 
				+                                                        end
			
 
				+                                                    else acc [fwd ++ [nm = t]]
			
 
				+                                            )
			
 
				+                                            (fn [fwd ::_] [[] ~ fwd] => error <xml>Unknown JSON object variant name {[name]}</xml>)
			
 
				+                                            fl jss names) [[]] !
			
 
				+
			
 
				+                           val s' = skipSpaces s'
			
 
				+                           val s' = if String.length s' <> 0 && String.sub s' 0 = #"," then
			
 
				+                                        skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
			
 
				+                                    else
			
 
				+                                        s'
			
 
				+                       in
			
 
				+                           if String.length s' = 0 then
			
 
				+                               error <xml>JSON object doesn't end in brace</xml>
			
 
				+                           else if String.sub s' 0 = #"}" then
			
 
				+                               (r, String.substring s' {Start = 1, Len = String.length s' - 1})
			
 
				+                           else error <xml>Junk after JSON value in object</xml>
			
 
				+                       end
			
 
				+                   }
			
 
				+
			
 
				+val json_unit : json unit = json_record {} {}
			
 
				+
			
 
				+functor Recursive (M : sig
			
 
				+                       con t :: Type -> Type
			
 
				+                       val json_t : a ::: Type -> json a -> json (t a)
			
 
				+                   end) = struct
			
 
				+    open M
			
 
				+
			
 
				+    datatype r = Rec of t r
			
 
				+
			
 
				+    fun rTo (Rec x) = (json_t {ToJson = rTo,
			
 
				+                               FromJson = fn _ => error <xml>Tried to FromJson in ToJson!</xml>}).ToJson x
			
 
				+
			
 
				+    fun rFrom s =
			
 
				+        let
			
 
				+            val (x, s') = (json_t {ToJson = fn _ => error <xml>Tried to ToJson in FromJson!</xml>,
			
 
				+                                   FromJson = rFrom}).FromJson s
			
 
				+        in
			
 
				+            (Rec x, s')
			
 
				+        end
			
 
				+
			
 
				+    val json_r = {ToJson = rTo, FromJson = rFrom}
			
 
				+end
			
--- a/UrWeb/meta/json.urs
+++ b/UrWeb/meta/json.urs
@@ -0,0 +1,31 @@
 
				+(** The JSON text-based serialization format *)
			
 
				+
			
 
				+class json
			
 
				+
			
 
				+val toJson : a ::: Type -> json a -> a -> string
			
 
				+val fromJson : a ::: Type -> json a -> string -> a
			
 
				+val fromJson' : a ::: Type -> json a -> string -> a * string
			
 
				+
			
 
				+val mkJson : a ::: Type -> {ToJson : a -> string,
			
 
				+                            FromJson : string -> a * string} -> json a
			
 
				+
			
 
				+val json_string : json string
			
 
				+val json_int : json int
			
 
				+val json_float : json float
			
 
				+val json_bool : json bool
			
 
				+val json_option : a ::: Type -> json a -> json (option a)
			
 
				+val json_list : a ::: Type -> json a -> json (list a)
			
 
				+
			
 
				+val json_record : ts ::: {Type} -> folder ts -> $(map json ts) -> $(map (fn _ => string) ts) -> json $ts
			
 
				+val json_variant : ts ::: {Type} -> folder ts -> $(map json ts) -> $(map (fn _ => string) ts) -> json (variant ts)
			
 
				+
			
 
				+val json_unit : json unit
			
 
				+
			
 
				+functor Recursive (M : sig
			
 
				+                       con t :: Type -> Type
			
 
				+                       val json_t : a ::: Type -> json a -> json (t a)
			
 
				+                   end) : sig
			
 
				+    datatype r = Rec of M.t r
			
 
				+
			
 
				+    val json_r : json r
			
 
				+end
			
--- a/UrWeb/meta/lib.urp
+++ b/UrWeb/meta/lib.urp
@@ -0,0 +1,12 @@
 
				+$/char
			
 
				+$/string
			
 
				+$/option
			
 
				+incl
			
 
				+mem
			
 
				+eq
			
 
				+record
			
 
				+variant
			
 
				+json
			
 
				+sql
			
 
				+parse
			
 
				+html
			
--- a/UrWeb/meta/mem.ur
+++ b/UrWeb/meta/mem.ur
@@ -0,0 +1,38 @@
 
				+con mem' = K ==> fn (nm :: Name) (t :: K) (r :: {K}) (r' :: {K}) =>
			
 
				+    [[nm] ~ r'] => {Expose : f :: ({K} -> Type) -> f r -> f ([nm = t] ++ r'),
			
 
				+                    Hide : f :: ({K} -> Type) -> f ([nm = t] ++ r') -> f r}
			
 
				+
			
 
				+con mem = K ==> fn (nm :: Name) (t :: K) (r :: {K}) =>
			
 
				+                   tp :: Type -> (r' :: {K} -> [[nm] ~ r'] => mem' nm t r r' -> tp) -> tp
			
 
				+
			
 
				+fun mem [K] [nm :: Name] [t :: K] [r :: {K}] [[nm] ~ r] =
			
 
				+    fn [tp :: Type] (f : r' :: {K} -> [[nm] ~ r'] => mem' nm t ([nm = t] ++ r) r' -> tp) =>
			
 
				+       f [r] (fn [[nm] ~ r] => {Expose = fn [f :: {K} -> Type] x => x,
			
 
				+                                Hide = fn [f :: {K} -> Type] x => x})
			
 
				+
			
 
				+fun mp [K] [K2] [f :: K -> K2] [nm ::: Name] [t ::: K] [r ::: {K}] (m : mem nm t r) =
			
 
				+    m [mem nm (f t) (map f r)] (fn [r' :: {K}] [[nm] ~ r'] (m' : mem' nm t r r') =>
			
 
				+                                fn [tp :: Type] (f : r' :: {K2} -> [[nm] ~ r'] =>
			
 
				+                                                 mem' nm (f t) (map f r) r' -> tp) =>
			
 
				+                                   f [map f r'] (fn [[nm] ~ map f r'] =>
			
 
				+                                                    {Expose = fn [f' :: {K2} -> Type] x =>
			
 
				+                                                                 m'.Expose [fn r => f' (map f r)] x,
			
 
				+                                                     Hide = fn [f' :: {K2} -> Type] x =>
			
 
				+                                                               m'.Hide [fn r => f' (map f r)] x}))
			
 
				+
			
 
				+fun proj [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) =
			
 
				+    m [t] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') =>
			
 
				+              (m'.Expose [fn r => $r] r).nm)
			
 
				+
			
 
				+fun replace [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) (v : t) =
			
 
				+    m [$r] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') =>
			
 
				+               m'.Hide [fn r => $r] (m'.Expose [fn r => $r] r -- nm ++ {nm = v}))
			
 
				+
			
 
				+fun fold [K] [tf :: ({K} -> Type)] [r ::: {K}]
			
 
				+    (f : nm :: Name -> v :: K -> r' :: {K} -> [[nm] ~ r']
			
 
				+     => mem nm v r -> tf r' -> tf ([nm = v] ++ r'))
			
 
				+    (i : tf []) (fl : folder r) =
			
 
				+    @@Incl.fold [tf] [r]
			
 
				+      (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] (i : Incl.incl ([nm = v] ++ r') r) acc =>
			
 
				+          f [nm] [v] [r'] (Incl.inv1 [nm] [v] [r'] [r] [mem] i mem) acc)
			
 
				+      i fl
			
--- a/UrWeb/meta/mem.urs
+++ b/UrWeb/meta/mem.urs
@@ -0,0 +1,15 @@
 
				+(** A record membership predicate *)
			
 
				+
			
 
				+con mem :: K --> Name -> K -> {K} -> Type
			
 
				+
			
 
				+val mem : K --> nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => mem nm t ([nm = t] ++ r)
			
 
				+val mp : K --> K2 --> f :: (K -> K2) -> nm ::: Name -> t ::: K -> r ::: {K} -> mem nm t r -> mem nm (f t) (map f r)
			
 
				+
			
 
				+val proj : nm ::: Name -> t ::: Type -> r ::: {Type} -> mem nm t r -> $r -> t
			
 
				+val replace : nm ::: Name -> t ::: Type -> r ::: {Type} -> mem nm t r -> $r -> t -> $r
			
 
				+
			
 
				+val fold : K --> tf :: ({K} -> Type) -> r ::: {K}
			
 
				+           -> (nm :: Name -> v :: K -> r' :: {K} -> [[nm] ~ r']
			
 
				+               => mem nm v r -> tf r' -> tf ([nm = v] ++ r'))
			
 
				+           -> tf []
			
 
				+           -> folder r -> tf r
			
--- a/UrWeb/meta/parse.ur
+++ b/UrWeb/meta/parse.ur
@@ -0,0 +1,5 @@
 
				+(** Datatypes for describing parse results *)
			
 
				+
			
 
				+datatype parse a =
			
 
				+         Success of a
			
 
				+       | Failure of string
			
--- a/UrWeb/meta/record.ur
+++ b/UrWeb/meta/record.ur
@@ -0,0 +1,18 @@
 
				+fun numFields [r ::: {Type}] (fl : folder r) (r : $r) : int =
			
 
				+    @fold [fn _ => int] (fn [nm ::_] [u ::_] [r ::_] [[nm] ~ r] acc => acc+1) 0 fl
			
 
				+
			
 
				+fun mem [a ::: Type] [ns ::: {Unit}] (_ : eq a) (fl : folder ns) (x : a) (r : $(mapU a ns)) : bool =
			
 
				+    @foldUR [a] [fn _ => bool]
			
 
				+     (fn [nm ::_] [r ::_] [[nm] ~ r] y acc =>
			
 
				+         acc || x = y)
			
 
				+     False fl r
			
 
				+
			
 
				+fun equal [ts ::: {Type}] (eqs : $(map eq ts)) (fl : folder ts) (r1 : $ts) (r2 : $ts) : bool =
			
 
				+    @foldR3 [eq] [ident] [ident] [fn _ => bool]
			
 
				+     (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] isEq x y acc =>
			
 
				+         acc && @eq isEq x y)
			
 
				+     True fl eqs r1 r2
			
 
				+
			
 
				+fun ap [K] [tf1 :: K -> Type] [tf2 :: K -> Type]
			
 
				+       [r ::: {K}] (fl : folder r) (fs : $(map (fn t => tf1 t -> tf2 t) r)) (xs : $(map tf1 r))
			
 
				+  = @map2 [fn t => tf1 t -> tf2 t] [fn t => tf1 t] [tf2] (fn [t] f x => f x) fl fs xs
			
--- a/UrWeb/meta/record.urs
+++ b/UrWeb/meta/record.urs
@@ -0,0 +1,14 @@
 
				+val numFields : r ::: {Type} -> folder r -> $r -> int
			
 
				+
			
 
				+val mem : a ::: Type -> ns ::: {Unit} -> eq a -> folder ns -> a -> $(mapU a ns) -> bool
			
 
				+(* Is a value found in a record? *)
			
 
				+
			
 
				+val equal : ts ::: {Type} -> $(map eq ts) -> folder ts -> $ts -> $ts -> bool
			
 
				+(* Are two records equal? *)
			
 
				+
			
 
				+(* Analogous to applicative ap e.g. <*>, of type [f (a -> b) -> f a -> f b] *)
			
 
				+val ap : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
			
 
				+         -> r ::: {K} -> folder r
			
 
				+         -> $(map (fn t => tf1 t -> tf2 t) r)
			
 
				+         -> $(map tf1 r)
			
 
				+         -> $(map tf2 r)
			
--- a/UrWeb/meta/sql.ur
+++ b/UrWeb/meta/sql.ur
@@ -0,0 +1,75 @@
 
				+fun sqexps [env] [fields] (fl : folder fields) (inj : $(map sql_injectable fields)) (r : $fields) =
			
 
				+    @map2 [sql_injectable] [ident] [sql_exp env [] []]
			
 
				+     (fn [t] => @sql_inject)
			
 
				+     fl inj r
			
 
				+
			
 
				+fun selector [tn :: Name] [fs] [ofs] [fs ~ ofs] (fl : folder fs) (m : $(map sql_injectable fs)) (r : $fs)
			
 
				+    : sql_exp [tn = ofs ++ fs] [] [] bool =
			
 
				+    @foldR2 [sql_injectable] [ident]
			
 
				+     [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool]
			
 
				+     (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
			
 
				+                      (inj : sql_injectable t) (v : t)
			
 
				+                      (exp : rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool)
			
 
				+                      [rest :: {Type}] [rest ~ [nm = t] ++ key] =>
			
 
				+         (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest]}))
			
 
				+     (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE))
			
 
				+     fl m r [_] !
			
 
				+
			
 
				+fun joiner [tn1 :: Name] [tn2 :: Name] [fs] [ofs1] [ofs2] [[tn1] ~ [tn2]] [fs ~ ofs1] [fs ~ ofs2]
			
 
				+           (fl : folder fs) : sql_exp [tn1 = ofs1 ++ fs, tn2 = ofs2 ++ fs] [] [] bool =
			
 
				+    @fold
			
 
				+     [fn key => rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key] => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool]
			
 
				+     (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
			
 
				+                      (exp : rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key]
			
 
				+                       => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool)
			
 
				+                      [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ [nm = t] ++ key] [rest2 ~ [nm = t] ++ key] =>
			
 
				+         (WHERE {{tn1}}.{nm} = {{tn2}}.{nm} AND {exp [[nm = t] ++ rest1] [[nm = t] ++ rest2]}))
			
 
				+     (fn [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ []] [rest2 ~ []] => (WHERE TRUE))
			
 
				+     fl [_] [_] ! !
			
 
				+
			
 
				+fun insertIfMissing [keyCols ::: {Type}] [otherCols ::: {Type}] [otherKeys ::: {{Unit}}]
			
 
				+                    [keyCols ~ otherCols] [[Pkey] ~ otherKeys]
			
 
				+                    (kfl : folder keyCols) (kinj : $(map sql_injectable keyCols))
			
 
				+                    (ofl : folder otherCols) (oinj : $(map sql_injectable otherCols))
			
 
				+                    (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
			
 
				+                    (vs : $(keyCols ++ otherCols))
			
 
				+    : transaction bool =
			
 
				+    alreadyThere <- oneRowE1 (SELECT COUNT( * ) > 0
			
 
				+                              FROM t
			
 
				+                              WHERE {@selector [#T] ! kfl kinj (vs --- _)});
			
 
				+    if alreadyThere then
			
 
				+        return False
			
 
				+    else
			
 
				+        dml (insert t (@sqexps kfl kinj (vs --- _)
			
 
				+                        ++ @sqexps ofl oinj (vs --- _)));
			
 
				+        return True
			
 
				+
			
 
				+fun deleteByKey [keyCols ::: {Type}] [otherCols ::: {Type}] [otherKeys ::: {{Unit}}]
			
 
				+    [keyCols ~ otherCols] [[Pkey] ~ otherKeys]
			
 
				+    (kfl : folder keyCols) (kinj : $(map sql_injectable keyCols))
			
 
				+    (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
			
 
				+    (vs : $keyCols) =
			
 
				+    dml (delete t (@selector [#T] ! kfl kinj vs))
			
 
				+
			
 
				+fun lookup [keyCols ::: {Type}] [otherCols ::: {Type}] [otherKeys ::: {{Unit}}]
			
 
				+           [keyCols ~ otherCols] [[Pkey] ~ otherKeys]
			
 
				+           (kfl : folder keyCols) (kinj : $(map sql_injectable keyCols))
			
 
				+           (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
			
 
				+           (vs : $keyCols)
			
 
				+    : transaction (option $otherCols) =
			
 
				+      oneOrNoRows1 (SELECT t.{{otherCols}}
			
 
				+                    FROM t
			
 
				+                    WHERE {@selector [#T] ! kfl kinj (vs --- _)})
			
 
				+
			
 
				+fun listify [lead :: Name] [cols ::: {Type}] [rest ::: {{Type}}] [[lead] ~ rest]
			
 
				+    (fl : folder cols) (eqs : $(map eq cols)) (q : sql_query [] [] ([lead = cols] ++ rest) []) =
			
 
				+    query q
			
 
				+    (fn r acc =>
			
 
				+        return (case acc of
			
 
				+                    [] => (r.lead, (r -- lead) :: []) :: []
			
 
				+                  | (key, ls) :: acc' =>
			
 
				+                    if @Record.equal eqs fl r.lead key then
			
 
				+                        (key, (r -- lead) :: ls) :: acc'
			
 
				+                    else
			
 
				+                        (r.lead, (r -- lead) :: []) :: acc))
			
 
				+    []
			
--- a/UrWeb/meta/sql.urs
+++ b/UrWeb/meta/sql.urs
@@ -0,0 +1,47 @@
 
				+(** Common metaprogramming patterns for SQL syntax construction *)
			
 
				+
			
 
				+val sqexps : env ::: {{Type}} -> fields ::: {Type} -> folder fields -> $(map sql_injectable fields)
			
 
				+             -> $fields -> $(map (sql_exp env [] []) fields)
			
 
				+(* Convert a record of Ur values into a record of SQL expressions *)
			
 
				+
			
 
				+val selector : tn :: Name -> fs ::: {Type} -> ofs ::: {Type} -> [fs ~ ofs]
			
 
				+               => folder fs -> $(map sql_injectable fs) -> $fs
			
 
				+               -> sql_exp [tn = ofs ++ fs] [] [] bool
			
 
				+(* Build a boolean SQL expression expressing equality of some fields of a table
			
 
				+ * row with a record of Ur values *)
			
 
				+
			
 
				+val joiner : tn1 :: Name -> tn2 :: Name -> fs ::: {Type} -> ofs1 ::: {Type} -> ofs2 ::: {Type}
			
 
				+             -> [[tn1] ~ [tn2]] => [fs ~ ofs1] => [fs ~ ofs2]
			
 
				+               => folder fs
			
 
				+               -> sql_exp [tn1 = ofs1 ++ fs, tn2 = ofs2 ++ fs] [] [] bool
			
 
				+(* Declare equality of same-named columns from two tables. *)
			
 
				+
			
 
				+val insertIfMissing : keyCols ::: {Type} -> otherCols ::: {Type} -> otherKeys ::: {{Unit}}
			
 
				+                      -> [keyCols ~ otherCols] => [[Pkey] ~ otherKeys]
			
 
				+                      => folder keyCols -> $(map sql_injectable keyCols)
			
 
				+                      -> folder otherCols -> $(map sql_injectable otherCols)
			
 
				+                      -> sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys)
			
 
				+                      -> $(keyCols ++ otherCols)
			
 
				+                      -> transaction bool
			
 
				+(* Insert a row into an SQL table if its key isn't already present, returning [False] iff the key was already present *)
			
 
				+
			
 
				+val deleteByKey : keyCols ::: {Type} -> otherCols ::: {Type} -> otherKeys ::: {{Unit}}
			
 
				+                  -> [keyCols ~ otherCols] => [[Pkey] ~ otherKeys]
			
 
				+                  => folder keyCols -> $(map sql_injectable keyCols)
			
 
				+                  -> sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys)
			
 
				+                  -> $keyCols
			
 
				+                  -> transaction {}
			
 
				+(* Delete a row from a table by matching its primary key against a given record. *)
			
 
				+
			
 
				+val lookup : keyCols ::: {Type} -> otherCols ::: {Type} -> otherKeys ::: {{Unit}}
			
 
				+             -> [keyCols ~ otherCols] => [[Pkey] ~ otherKeys]
			
 
				+             => folder keyCols -> $(map sql_injectable keyCols)
			
 
				+             -> sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys)
			
 
				+             -> $keyCols -> transaction (option $otherCols)
			
 
				+(* Get the further columns associated with a table key. *)
			
 
				+
			
 
				+val listify : lead :: Name -> cols ::: {Type} -> rest ::: {{Type}} -> [[lead] ~ rest]
			
 
				+              => folder cols -> $(map eq cols)
			
 
				+              -> sql_query [] [] ([lead = cols] ++ rest) []
			
 
				+              -> transaction (list ($cols * list $(map (fn ts => $ts) rest)))
			
 
				+(* Shrink a set of table rows by summarizing into lists, keyed off of a lead table *)
			
--- a/UrWeb/meta/variant.ur
+++ b/UrWeb/meta/variant.ur
@@ -0,0 +1,145 @@
 
				+fun read [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) : t =
			
 
				+    match v
			
 
				+    (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> t) r)]
			
 
				+     (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> _) [r'::_] [[nm = u] ++ us ~ r'] r =>
			
 
				+         {nm = fn () => r.nm} ++ cs [[nm = u] ++ r'] r)
			
 
				+     (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r)
			
 
				+
			
 
				+fun write [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) (x : t) : $(mapU t r) =
			
 
				+    match v
			
 
				+    (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> $(mapU t (r ++ r'))) r)]
			
 
				+      (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us]
			
 
				+          (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> $(mapU ({} -> $(mapU t (us ++ r'))) us))
			
 
				+          [r'::_] [[nm = u] ++ us ~ r'] r =>
			
 
				+          {nm = fn () => r -- nm ++ {nm = x}} ++ cs [[nm = u] ++ r'] r)
			
 
				+      (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r)
			
 
				+
			
 
				+fun search [r] [t] (f : variant (mapU {} r) -> option t) (fl : folder r) : option t =
			
 
				+    @fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t]
			
 
				+    (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
			
 
				+                     (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t)
			
 
				+                     [r' ::_] [[nm] ++ r ~ r'] f' =>
			
 
				+        case f' (make [nm] {}) of
			
 
				+            None => acc [[nm] ++ r'] f'
			
 
				+          | v => v)
			
 
				+    (fn [r' ::_] [[] ~ r'] _ => None) fl [[]] ! f
			
 
				+
			
 
				+fun find [r] (f : variant (mapU {} r) -> bool) (fl : folder r) : option (variant (mapU {} r)) =
			
 
				+    @search (fn v => if f v then Some v else None) fl
			
 
				+
			
 
				+fun test [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ([nm = t] ++ ts))
			
 
				+          (v : variant ([nm = t] ++ ts)) : option t =
			
 
				+    match v ({nm = Some}
			
 
				+                 ++ (@map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl -- nm))
			
 
				+
			
 
				+fun testLess [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ts) (v : variant ([nm = t] ++ ts)) : option t =
			
 
				+    match v ({nm = Some}
			
 
				+                 ++ @map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl)
			
 
				+
			
 
				+fun weaken [r1 ::: {Type}] [r2 ::: {Type}] [r1 ~ r2] (fl : folder r1) (v : variant r1) : variant (r1 ++ r2) =
			
 
				+    match v
			
 
				+    (@fold [fn r => r' :: {Type} -> [r ~ r'] => $(map (fn t => t -> variant (r ++ r')) r)]
			
 
				+      (fn [nm :: Name] [t ::_] [r ::_] [[nm] ~ r] (acc : r' :: {Type} -> [r ~ r'] => $(map (fn t => t -> variant (r ++ r')) r)) [r'::_] [[nm = t] ++ r ~ r'] =>
			
 
				+          {nm = make [nm]} ++ acc [[nm = t] ++ r'])
			
 
				+      (fn [r'::_] [[] ~ r'] => {}) fl [r2] !)
			
 
				+
			
 
				+fun eq [r] (fl : folder r) (v1 : variant (mapU {} r)) (v2 : variant (mapU {} r)) : bool =
			
 
				+    match v1
			
 
				+    (@fold [fn r => r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)]
			
 
				+     (fn [nm ::_] [u ::_] [r ::_] [[nm] ~ r]
			
 
				+         (acc : r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r))
			
 
				+         [r' ::_] [[nm] ++ r ~ r'] (fl' : folder ([nm] ++ r ++ r')) v =>
			
 
				+         {nm = fn () => Option.isSome (@test [nm] ! (@Folder.mp fl') v)}
			
 
				+             ++ @acc [[nm] ++ r'] ! fl' v)
			
 
				+     (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! fl v2)
			
 
				+
			
 
				+fun fold [r] [t] (fl : folder r) (f : variant (mapU {} r) -> t -> t) : t -> t =
			
 
				+    @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t]
			
 
				+    (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
			
 
				+                     (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t)
			
 
				+                     [r' ::_] [[nm] ++ r ~ r'] f' acc' =>
			
 
				+        f' (make [nm] {}) (acc [[nm] ++ r'] f' acc'))
			
 
				+    (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f
			
 
				+
			
 
				+fun mp [r ::: {Unit}] [t ::: Type] (fl : folder r) (f : variant (mapU {} r) -> t) : $(mapU t r) =
			
 
				+    @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t) -> $(mapU t r)]
			
 
				+    (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
			
 
				+                     (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t) -> $(mapU t r))
			
 
				+                     [r' ::_] [[nm] ++ r ~ r'] f' =>
			
 
				+        {nm = f' (make [nm] {})} ++ acc [[nm] ++ r'] f')
			
 
				+    (fn [r' ::_] [[] ~ r'] _ => {}) fl [[]] ! f
			
 
				+
			
 
				+fun foldR [tr] [r] [t] (fl : folder r) (f : variant (mapU {} r) -> tr -> t -> t) (record : $(mapU tr r)) : t -> t =
			
 
				+    @Top.foldUR [tr] [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t]
			
 
				+    (fn [nm :: Name] [r ::_] [[nm] ~ r] (v : tr)
			
 
				+                     (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t)
			
 
				+                     [r' ::_] [[nm] ++ r ~ r'] f' acc' =>
			
 
				+        f' (make [nm] {}) v (acc [[nm] ++ r'] f' acc'))
			
 
				+    (fn [r' ::_] [[] ~ r'] _ x => x) fl record [[]] ! f
			
 
				+
			
 
				+fun appR [m] (_ : monad m) [tr] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> m {}) (record : $(mapU tr r)) : m {} =
			
 
				+    @foldR fl (fn var this acc => f var this; acc) record (return ())
			
 
				+
			
 
				+fun mapR [tr] [t] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> t) (record : $(mapU tr r)) : $(mapU t r) =
			
 
				+    @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)]
			
 
				+    (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
			
 
				+                     (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t) -> $(mapU tr r) -> $(mapU t r))
			
 
				+                     [r' ::_] [[nm] ++ r ~ r'] f' vs =>
			
 
				+        {nm = f' (make [nm] {}) vs.nm} ++ acc [[nm] ++ r'] f' (vs -- nm))
			
 
				+    (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! f record
			
 
				+
			
 
				+fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type]
			
 
				+    (f : p :: K -> f p -> fr p -> t)
			
 
				+    [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t =
			
 
				+    match v
			
 
				+    (@Top.mp [fr] [fn p => f p -> t]
			
 
				+     (fn [p] (m : fr p) (v : f p) => f [p] v m)
			
 
				+     fl r)
			
 
				+
			
 
				+fun destr2R [K] [f1 :: K -> Type] [f2 :: K -> Type] [fr :: K -> Type] [t ::: Type]
			
 
				+    (f : p :: K -> f1 p -> f2 p -> fr p -> t)
			
 
				+    [r ::: {K}] (fl : folder r) (v1 : variant (map f1 r)) (v2 : variant (map f2 r)) (r : $(map fr r)) : option t =
			
 
				+    match v1
			
 
				+    (@Top.foldR [fr] [fn r => others :: {K} -> [others ~ r] =>
			
 
				+                     folder (r ++ others)
			
 
				+                     -> variant (map f2 (r ++ others))
			
 
				+                     -> $(map (fn p => f1 p -> option t) r)]
			
 
				+     (fn [nm ::_] [p ::_] [r ::_] [[nm] ~ r] (meta : fr p)
			
 
				+         (acc : others :: {K} -> [others ~ r] =>
			
 
				+          folder (r ++ others)
			
 
				+          -> variant (map f2 (r ++ others))
			
 
				+          -> $(map (fn p => f1 p -> option t) r))
			
 
				+         [others :: {K}] [others ~ [nm = p] ++ r]
			
 
				+         (fl : folder ([nm = p] ++ r ++ others))
			
 
				+         (v2 : variant (map f2 ([nm = p] ++ r ++ others))) =>
			
 
				+         {nm = fn x1 => match v2
			
 
				+                        ({nm = fn x2 => Some (f [p] x1 x2 meta)}
			
 
				+                             ++ (@map0 [fn p => f2 p -> option t] (fn [p' ::_] _ => None) fl -- nm))}
			
 
				+             ++ @acc [[nm = p] ++ others] ! fl v2)
			
 
				+     (fn [others ::_] [others ~ []] _ _ => {})
			
 
				+     fl r [[]] ! fl v2)
			
 
				+
			
 
				+fun testEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts]
			
 
				+    (pf : Eq.eq r ([nm = t] ++ ts)) (fl : folder r) (v : variant (map f r)) : option (f t) =
			
 
				+  @test [nm] ! (@Folder.mp (@Eq.cast pf [folder] fl))
			
 
				+   (Eq.cast pf [fn r => variant (map f r)] v)
			
 
				+
			
 
				+fun makeEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts]
			
 
				+    (pf : Eq.eq r ([nm = t] ++ ts)) (x : f t) : variant (map f r) =
			
 
				+  Eq.cast (Eq.sym pf) [fn r => variant (map f r)] (make [nm] x)
			
 
				+
			
 
				+con variantMake ts' ts = $(map (fn t => t -> variant ts') ts)
			
 
				+con mkLabelsAccum r = s :: {Type} -> [r ~ s] => variantMake (r ++ s) r
			
 
				+fun mkLabels [ts ::: {Type}] (fl : folder ts) : variantMake ts ts
			
 
				+  = @Top.fold [mkLabelsAccum]
			
 
				+          (fn [nm::_] [v::_] [r::_] [[nm] ~ r]
			
 
				+              (k : mkLabelsAccum r)
			
 
				+              [s::_] [[nm = v] ++ r ~ s] => k [[nm = v] ++ s] ++ {nm = make [nm]})
			
 
				+          (fn [s::_] [[] ~ s] => {}) fl [[]] !
			
 
				+
			
 
				+con type_case ts t a = (a -> variant ts) -> a -> t
			
 
				+
			
 
				+fun declareCase [ts] [t] [a] (f : (a -> variant ts) -> a -> t) : type_case ts t a = f
			
 
				+fun typeCase [ts] [t] (v : variant ts) (dstrs : $(map (type_case ts t) ts)) (fl : folder ts) : t
			
 
				+(* Ur/Web not clever enough to calculate these folders, it seems *)
			
 
				+  = match v (@Record.ap [fn a => a -> variant ts] [fn a => a -> t] fl dstrs (@mkLabels fl))
			
--- a/UrWeb/meta/variant.urs
+++ b/UrWeb/meta/variant.urs
@@ -0,0 +1,83 @@
 
				+(** Derived functions dealing with polymorphic variants *)
			
 
				+
			
 
				+val read : r ::: {Unit} -> t ::: Type -> folder r -> $(mapU t r) -> variant (mapU {} r) -> t
			
 
				+val write : r ::: {Unit} -> t ::: Type -> folder r -> $(mapU t r) -> variant (mapU {} r) -> t -> $(mapU t r)
			
 
				+
			
 
				+val search : r ::: {Unit} -> t ::: Type -> (variant (mapU {} r) -> option t) -> folder r -> option t
			
 
				+val find : r ::: {Unit} -> (variant (mapU {} r) -> bool) -> folder r -> option (variant (mapU {} r))
			
 
				+
			
 
				+val test : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ([nm = t] ++ ts)
			
 
				+                                                                    -> variant ([nm = t] ++ ts) -> option t
			
 
				+val testLess : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ts -> variant ([nm = t] ++ ts) -> option t
			
 
				+
			
 
				+val weaken : r1 ::: {Type} -> r2 ::: {Type} -> [r1 ~ r2] => folder r1
			
 
				+             -> variant r1 -> variant (r1 ++ r2)
			
 
				+
			
 
				+val testEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
			
 
				+    Eq.eq r ([nm = t] ++ ts)
			
 
				+    -> folder r
			
 
				+    -> variant (map f r) -> option (f t)
			
 
				+
			
 
				+val eq : r ::: {Unit} -> folder r -> variant (mapU {} r) -> variant (mapU {} r) -> bool
			
 
				+
			
 
				+val makeEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
			
 
				+    Eq.eq r ([nm = t] ++ ts)
			
 
				+    -> f t
			
 
				+    -> variant (map f r)
			
 
				+
			
 
				+val mp : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t) -> $(mapU t r)
			
 
				+
			
 
				+val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t
			
 
				+
			
 
				+val foldR : tr ::: Type -> r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> tr -> t -> t) -> $(mapU tr r) -> t -> t
			
 
				+
			
 
				+val appR : m ::: (Type -> Type) -> monad m
			
 
				+           -> tr ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> m {}) -> $(mapU tr r) -> m {}
			
 
				+
			
 
				+val mapR : tr ::: Type -> t ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)
			
 
				+
			
 
				+val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
			
 
				+             -> (p :: K -> f p -> fr p -> t)
			
 
				+             -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t
			
 
				+
			
 
				+val destr2R : K --> f1 :: (K -> Type) -> f2 :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
			
 
				+             -> (p :: K -> f1 p -> f2 p -> fr p -> t)
			
 
				+             -> r ::: {K} -> folder r -> variant (map f1 r) -> variant (map f2 r) -> $(map fr r) -> option t
			
 
				+
			
 
				+(* Metaprogrammed type-directed case-match.
			
 
				+
			
 
				+This uses a combination of type classes and metaprogramming to make
			
 
				+it easy to write case-matches on very large variants with many
			
 
				+similar elements.  Here's how you use it:
			
 
				+
			
 
				+    1. For every type in the variant, write a local typeclass function
			
 
				+       which reduces it to t, and register as such using the 'declareCase'
			
 
				+       function in the module you created.
			
 
				+
			
 
				+            let val empty = declareCase (fn _ (_ : int) => True)
			
 
				+
			
 
				+       These functions also take an initial argument, which has
			
 
				+       type [a -> variant ts]; e.g. you can use this to create
			
 
				+       a new copy of the variant with different values!
			
 
				+       Make sure you specify type signatures on the argument [t]
			
 
				+       so that we can identify who this typeclass is for.  (If you
			
 
				+       use type classes to construct the return value, you may
			
 
				+       also need to declare the return type explicitly.)
			
 
				+
			
 
				+    2. Do the match using 'typeCase':
			
 
				+
			
 
				+            typeCase t
			
 
				+
			
 
				+       If you need to override specific constructors, use this idiom:
			
 
				+
			
 
				+            @typeCase t (_ ++ {
			
 
				+                YourConstr = declareCase (fn _ _ => ...)
			
 
				+            }) _
			
 
				+
			
 
				+How does it work?  Very simple: it uses local typeclasses + Ur/Web's
			
 
				+support for automatically instantiating records of typeclasses.
			
 
				+*)
			
 
				+
			
 
				+class type_case :: {Type} -> Type -> Type -> Type
			
 
				+val declareCase : ts ::: {Type} -> t ::: Type -> a ::: Type -> ((a -> variant ts) -> a -> t) -> type_case ts t a
			
 
				+val typeCase : ts ::: {Type} -> t ::: Type -> variant ts -> $(map (type_case ts t) ts) -> folder ts -> t
			
--- a/UrWeb/world.sql
+++ b/UrWeb/world.sql
@@ -0,0 +1,3 @@
 
				+CREATE TABLE uw_Bench_world AS SELECT uw_id::int8, trunc(random()*9999+1)::int8 AS uw_randomnumber FROM generate_series(1,10000) AS uw_id;
			
 
				+ALTER TABLE uw_Bench_world ADD PRIMARY KEY (uw_id);
			
 
				+ALTER TABLE uw_Bench_world ALTER COLUMN uw_randomnumber SET NOT NULL;