summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--demo/prose12
-rw-r--r--demo/sql.ur52
-rw-r--r--demo/sql.urp3
-rw-r--r--demo/sql.urs1
-rw-r--r--lib/basis.urs2
-rw-r--r--src/demo.sml16
-rw-r--r--src/monoize.sml6
-rw-r--r--src/termination.sml50
8 files changed, 120 insertions, 22 deletions
diff --git a/demo/prose b/demo/prose
index 5035108c..a863f6c5 100644
--- a/demo/prose
+++ b/demo/prose
@@ -59,3 +59,15 @@ listShop.urp
<p>The <tt>ListFun</tt> module defines a functor for building list editing sub-applications. An argument to the functor <tt>Make</tt> must give the type to be stored in the lists, along with marshaling and unmarshaling functions. In return, the functor returns an entry point function.</p>
<p>The <tt>ListShop</tt> modules ties everything together by instantiating <tt>ListFun.Make</tt> with structures for integers and strings. <tt>show</tt> and <tt>read</tt> can be used for marshaling and unmarshaling in both cases because they are type-class-generic.</p>
+
+sql.urp
+
+<p>We see a simple example of accessing a SQL database. The project file specifies the database to connect to.</p>
+
+<p>A <tt>table</tt> declaration declares a SQL table with rows of a particular record type. We can use embedded SQL syntax in a way that leads to all of our queries and updates being type-checked. Indeed, Ur/Web makes strong guarantees that it is impossible to execute invalid SQL queries or make bad assumptions about the types of tables for marshaling and unmarshaling (which happen implicitly).</p>
+
+<p>The <tt>list</tt> function implements an HTML table view of all rows in the SQL table. The <tt>queryX</tt> function takes two arguments: a SQL query and a function for generating XML fragments from query result rows. The query is run, and the fragments for the rows are concatenated together.</p>
+
+<p>Other functions demonstrate use of the <tt>dml</tt> function, for building a transaction from a SQL DML command. It is easy to insert antiquoted Ur code into queries and DML commands, and the type-checker catches mistakes in the types of the expressions that we insert.</p>
+
+<p>
diff --git a/demo/sql.ur b/demo/sql.ur
new file mode 100644
index 00000000..9e9effff
--- /dev/null
+++ b/demo/sql.ur
@@ -0,0 +1,52 @@
+table t : { A : int, B : float, C : string, D : bool }
+
+fun list () =
+ rows <- queryX (SELECT * FROM t)
+ (fn row => <xml><tr>
+ <td>{[row.T.A]}</td> <td>{[row.T.B]}</td> <td>{[row.T.C]}</td> <td>{[row.T.D]}</td>
+ <td><a link={delete row.T.A}>[delete]</a></td>
+ </tr></xml>);
+ return <xml>
+ <table border=1>
+ <tr> <th>A</th> <th>B</th> <th>C</th> <th>D</th> </tr>
+ {rows}
+ </table>
+
+ <br/><hr/><br/>
+
+ <form>
+ <table>
+ <tr> <th>A:</th> <td><textbox{#A}/></td> </tr>
+ <tr> <th>B:</th> <td><textbox{#B}/></td> </tr>
+ <tr> <th>C:</th> <td><textbox{#C}/></td> </tr>
+ <tr> <th>D:</th> <td><checkbox{#D}/></td> </tr>
+ <tr> <th/> <td><submit action={add} value="Add Row"/></td> </tr>
+ </table>
+ </form>
+ </xml>
+
+and add r =
+ () <- dml (INSERT INTO t (A, B, C, D)
+ VALUES ({readError r.A}, {readError r.B}, {r.C}, {r.D}));
+ xml <- list ();
+ return <xml><body>
+ <p>Row added.</p>
+
+ {xml}
+ </body></xml>
+
+and delete a =
+ () <- dml (DELETE FROM t
+ WHERE t.A = {a});
+ xml <- list ();
+ return <xml><body>
+ <p>Row deleted.</p>
+
+ {xml}
+ </body></xml>
+
+fun main () =
+ xml <- list ();
+ return <xml><body>
+ {xml}
+ </body></xml>
diff --git a/demo/sql.urp b/demo/sql.urp
new file mode 100644
index 00000000..1b8bb5a4
--- /dev/null
+++ b/demo/sql.urp
@@ -0,0 +1,3 @@
+database dbname=test
+
+sql
diff --git a/demo/sql.urs b/demo/sql.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/sql.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
diff --git a/lib/basis.urs b/lib/basis.urs
index 53c4529d..a539f05e 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -339,6 +339,8 @@ val font : bodyTag [Size = int, Face = string]
val h1 : bodyTag []
val li : bodyTag []
+val hr : bodyTag []
+
val a : bodyTag [Link = transaction page]
val form : ctx ::: {Unit} -> bind ::: {Type}
diff --git a/src/demo.sml b/src/demo.sml
index 80506576..5ed9da2a 100644
--- a/src/demo.sml
+++ b/src/demo.sml
@@ -271,6 +271,15 @@ fun make {prefix, dirname} =
fun highlight () =
doit (fn (src, html) =>
let
+ val dirty =
+ let
+ val srcSt = Posix.FileSys.stat src
+ val htmlSt = Posix.FileSys.stat html
+ in
+ Time.> (Posix.FileSys.ST.mtime srcSt,
+ Posix.FileSys.ST.mtime htmlSt)
+ end handle OS.SysErr _ => true
+
val cmd = "emacs --eval \"(progn "
^ "(global-font-lock-mode t) "
^ "(add-to-list 'load-path \\\""
@@ -287,8 +296,11 @@ fun make {prefix, dirname} =
^ "\\\") "
^ "(kill-emacs))\""
in
- print (">>> " ^ cmd ^ "\n");
- ignore (OS.Process.system cmd)
+ if dirty then
+ (print (">>> " ^ cmd ^ "\n");
+ ignore (OS.Process.system cmd))
+ else
+ ()
end)
in
if OS.Path.base file = "demo" then
diff --git a/src/monoize.sml b/src/monoize.sml
index 36ae4a08..cacf3d6d 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -1535,7 +1535,8 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
val s = (L'.EPrim (Prim.String (String.concat ["<", tag])), loc)
in
- foldl (fn ((x, e, t), (s, fm)) =>
+ foldl (fn (("Action", _, _), acc) => acc
+ | ((x, e, t), (s, fm)) =>
case t of
(L'.TFfi ("Basis", "bool"), _) =>
let
@@ -1567,7 +1568,6 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
case x of
"Href" => urlifyExp
| "Link" => urlifyExp
- | "Action" => urlifyExp
| _ => attrifyExp
val xp = " " ^ lowercaseFirst x ^ "=\""
@@ -1633,7 +1633,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
end
in
case tag of
- "submit" => ((L'.EPrim (Prim.String "<input type=\"submit\"/>"), loc), fm)
+ "submit" => normal ("input type=\"submit\"", NONE)
| "textbox" =>
(case targs of
diff --git a/src/termination.sml b/src/termination.sml
index e2337e54..1bae7592 100644
--- a/src/termination.sml
+++ b/src/termination.sml
@@ -31,6 +31,7 @@ open Elab
structure E = ElabEnv
structure IM = IntBinaryMap
+structure IS = IntBinarySet
datatype pedigree =
Func of int
@@ -118,7 +119,7 @@ fun declOk' env (d, loc) =
| (_, PRecord xps) => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps
end
- fun exp (penv, calls) e =
+ fun exp parent (penv, calls) e =
let
val default = (Rabble, calls)
@@ -157,7 +158,7 @@ fun declOk' env (d, loc) =
if checkName x then
calls
else
- #2 (exp (penv, calls) e)) calls xets
+ #2 (exp parent (penv, calls) e)) calls xets
in
(Rabble, [Rabble], calls)
end
@@ -165,7 +166,7 @@ fun declOk' env (d, loc) =
| EApp (e1, e2) =>
let
val (p1, ps, calls) = combiner calls e1
- val (p2, calls) = exp (penv, calls) e2
+ val (p2, calls) = exp parent (penv, calls) e2
val p = case p1 of
Rabble => Rabble
@@ -191,7 +192,7 @@ fun declOk' env (d, loc) =
end
| _ =>
let
- val (p, calls) = exp (penv, calls) e
+ val (p, calls) = exp parent (penv, calls) e
in
(*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)];
print (p2s p ^ "\n");*)
@@ -205,7 +206,7 @@ fun declOk' env (d, loc) =
[] => raise Fail "Termination: Empty ps"
| f :: ps =>
case f of
- Func i => (i, ps) :: calls
+ Func i => (parent, i, ps) :: calls
| _ => calls
in
(p, calls)
@@ -227,27 +228,27 @@ fun declOk' env (d, loc) =
| EApp _ => apps ()
| EAbs (_, _, _, e) =>
let
- val (_, calls) = exp (Rabble :: penv, calls) e
+ val (_, calls) = exp parent (Rabble :: penv, calls) e
in
(Rabble, calls)
end
| ECApp _ => apps ()
| ECAbs (_, _, _, e) =>
let
- val (_, calls) = exp (penv, calls) e
+ val (_, calls) = exp parent (penv, calls) e
in
(Rabble, calls)
end
| ERecord xets =>
let
- val calls = foldl (fn ((_, e, _), calls) => #2 (exp (penv, calls) e)) calls xets
+ val calls = foldl (fn ((_, e, _), calls) => #2 (exp parent (penv, calls) e)) calls xets
in
(Rabble, calls)
end
| EField (e, x, _) =>
let
- val (p, calls) = exp (penv, calls) e
+ val (p, calls) = exp parent (penv, calls) e
val p =
case p of
Subarg (i, j, (TRecord (CRecord (_, xts), _), _)) =>
@@ -260,14 +261,14 @@ fun declOk' env (d, loc) =
end
| ECut (e, _, _) =>
let
- val (_, calls) = exp (penv, calls) e
+ val (_, calls) = exp parent (penv, calls) e
in
(Rabble, calls)
end
| EWith (e1, _, e2, _) =>
let
- val (_, calls) = exp (penv, calls) e1
- val (_, calls) = exp (penv, calls) e2
+ val (_, calls) = exp parent (penv, calls) e1
+ val (_, calls) = exp parent (penv, calls) e2
in
(Rabble, calls)
end
@@ -275,12 +276,12 @@ fun declOk' env (d, loc) =
| ECase (e, pes, _) =>
let
- val (p, calls) = exp (penv, calls) e
+ val (p, calls) = exp parent (penv, calls) e
val calls = foldl (fn ((pt, e), calls) =>
let
val penv = pat penv (p, pt)
- val (_, calls) = exp (penv, calls) e
+ val (_, calls) = exp parent (penv, calls) e
in
calls
end) calls pes
@@ -289,7 +290,7 @@ fun declOk' env (d, loc) =
end
| EError => (Rabble, calls)
- | EUnif (ref (SOME e)) => exp (penv, calls) e
+ | EUnif (ref (SOME e)) => exp parent (penv, calls) e
| EUnif (ref NONE) => (Rabble, calls)
end
@@ -301,20 +302,35 @@ fun declOk' env (d, loc) =
unravel (e, j + 1, Arg (i, j, t) :: penv)
| ECAbs (_, _, _, e) =>
unravel (e, j, penv)
- | _ => (j, #2 (exp (penv, calls) e))
+ | _ => (j, #2 (exp f (penv, calls) e))
in
unravel (e, 0, [])
end
val (ns, calls) = ListUtil.foldliMap doVali [] vis
+ fun isRecursive (from, to, _) =
+ let
+ fun search (at, soFar) =
+ at = from
+ orelse List.exists (fn (from', to', _) =>
+ from' = at
+ andalso not (IS.member (soFar, to'))
+ andalso search (to', IS.add (soFar, to')))
+ calls
+ in
+ search (to, IS.empty)
+ end
+
+ val calls = List.filter isRecursive calls
+
fun search (ns, choices) =
case ns of
[] =>
let
val choices = rev choices
in
- List.all (fn (f, args) =>
+ List.all (fn (_, f, args) =>
let
val recArg = List.nth (choices, f)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 11:59:37 +0000