Switch to pulling all Ur/Web infrastructure from Ubuntu (#3823)

* Ur/Web needs Ubuntu package 'mlton'

* All Ur/Web infrastructure now pulled from Ubuntu

* Remove unused Ur/Web library

* Load other Ur/Web standard-library modules

* Try removing more explicit apt dependencies of urweb

* Switch Ur/Web to Ubuntu 18.04

frameworks/Ur/urweb/bench.urp

@@ -1,4 +1,3 @@
-library meta
 database dbname=hello_world user=benchmarkdbuser password=benchmarkdbpass host=localhost
 rewrite all Bench/*
 allow responseHeader Date
@@ -9,5 +8,8 @@ safeGet updates
 noMangleSql
 html5
 
+$/char
+$/string
 $/list
+$/json
 bench

frameworks/Ur/urweb/meta/LICENSE

@@ -1,25 +0,0 @@
-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.

frameworks/Ur/urweb/meta/eq.ur

@@ -1,76 +0,0 @@
-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

frameworks/Ur/urweb/meta/eq.urs

@@ -1,44 +0,0 @@
-(** 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)

frameworks/Ur/urweb/meta/html.ur

@@ -1,144 +0,0 @@
-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"}
-

frameworks/Ur/urweb/meta/html.urs

@@ -1,29 +0,0 @@
-(** 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]

frameworks/Ur/urweb/meta/incl.ur

@@ -1,40 +0,0 @@
-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] [[]])

frameworks/Ur/urweb/meta/incl.urs

@@ -1,22 +0,0 @@
-(** 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

frameworks/Ur/urweb/meta/json.ur

@@ -1,337 +0,0 @@
-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
-        fun esc s =
-            case s of
-                "" => "\""
-              | _ =>
-                let
-                    val ch = String.sub s 0
-                in
-                    (if ch = #"\"" || ch = #"\\" then
-                         "\\" ^ String.str ch
-                     else
-                         String.str ch) ^ esc (String.suffix s 1)
-                end
-    in
-        "\"" ^ esc s
-    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 => "," ^ 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

frameworks/Ur/urweb/meta/json.urs

@@ -1,31 +0,0 @@
-(** 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

frameworks/Ur/urweb/meta/lib.urp

@@ -1,12 +0,0 @@
-$/char
-$/string
-$/option
-incl
-mem
-eq
-record
-variant
-json
-sql
-parse
-html

frameworks/Ur/urweb/meta/mem.ur

@@ -1,38 +0,0 @@
-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

frameworks/Ur/urweb/meta/mem.urs

@@ -1,15 +0,0 @@
-(** 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

frameworks/Ur/urweb/meta/parse.ur

@@ -1,5 +0,0 @@
-(** Datatypes for describing parse results *)
-
-datatype parse a =
-         Success of a
-       | Failure of string

frameworks/Ur/urweb/meta/record.ur

@@ -1,18 +0,0 @@
-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

frameworks/Ur/urweb/meta/record.urs

@@ -1,14 +0,0 @@
-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)

frameworks/Ur/urweb/meta/sql.ur

@@ -1,75 +0,0 @@
-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))
-    []

frameworks/Ur/urweb/meta/sql.urs

@@ -1,47 +0,0 @@
-(** 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 *)

frameworks/Ur/urweb/meta/variant.ur

@@ -1,145 +0,0 @@
-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))

frameworks/Ur/urweb/meta/variant.urs

@@ -1,83 +0,0 @@
-(** 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

frameworks/Ur/urweb/urweb-mysql.dockerfile

@@ -1,24 +1,9 @@
-FROM ubuntu:16.04
+FROM ubuntu:18.04
 
 ADD ./ /urweb
 WORKDIR /urweb
 
-ENV URWEB_VERSION=20160621
-ENV COMPILER=/urweb/urweb-build
-
-RUN apt update -yqq && apt install -yqq make wget mlton libssl-dev libpq-dev libmysqlclient-dev
-
-RUN mkdir -p $COMPILER && \
-    wget -q http://www.impredicative.com/ur/urweb-$URWEB_VERSION.tgz && \
-    tar xf urweb-$URWEB_VERSION.tgz && \
-    cd urweb-$URWEB_VERSION && \
-    ./configure --prefix=$COMPILER && \
-    make && \
-    make install
-
-ENV URWEB_HOME=${COMPILER}
-ENV LD_LIBRARY_PATH=${COMPILER}/lib
-ENV PATH=${COMPILER}/bin:${PATH}
+RUN apt update -yqq && apt install -yqq urweb
 
 RUN urweb -dbms mysql -db "dbname=hello_world user=benchmarkdbuser password=benchmarkdbpass host=tfb-database" bench
 

frameworks/Ur/urweb/urweb.dockerfile

@@ -1,24 +1,9 @@
-FROM ubuntu:16.04
+FROM ubuntu:18.04
 
 ADD ./ /urweb
 WORKDIR /urweb
 
-ENV URWEB_VERSION=20160621
-ENV COMPILER=/urweb/urweb-build
-
-RUN apt update -yqq && apt install -yqq build-essential wget mlton libssl-dev libpq-dev libmysqlclient-dev
-
-RUN mkdir -p $COMPILER && \
-    wget -q http://www.impredicative.com/ur/urweb-$URWEB_VERSION.tgz && \
-    tar xf urweb-$URWEB_VERSION.tgz && \
-    cd urweb-$URWEB_VERSION && \
-    ./configure --prefix=$COMPILER && \
-    make && \
-    make install
-
-ENV URWEB_HOME=${COMPILER}
-ENV LD_LIBRARY_PATH=${COMPILER}/lib
-ENV PATH=${COMPILER}/bin:${PATH}
+RUN apt update -yqq && apt install -yqq urweb
 
 RUN urweb -db "dbname=hello_world user=benchmarkdbuser password=benchmarkdbpass host=tfb-database" bench