From e0f9a9d921e6e505c86ef3e798690784f7abd511 Mon Sep 17 00:00:00 2001
From: adamc
Date: Thu, 23 Oct 2008 11:38:31 -0400
Subject: Add newline at end of file
---
src/compiler.sml | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/compiler.sml b/src/compiler.sml
index 2ddcfb4d..df4ee48d 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -555,6 +555,7 @@ fun compile job =
val s = TextIOPP.openOut {dst = outf, wid = 80}
in
Print.fprint s (CjrPrint.p_file CjrEnv.empty file);
+ TextIO.output1 (outf, #"\n");
TextIO.closeOut outf;
case #sql job of
--
cgit v1.2.3
From 833f4d2e0474ec3ff772107b52711289c4b648cf Mon Sep 17 00:00:00 2001
From: Adam Chlipala
Date: Thu, 23 Oct 2008 11:59:48 -0400
Subject: Counter demo
---
demo/counter.ur | 7 +++++++
demo/counter.urp | 2 ++
demo/counter.urs | 1 +
demo/prose | 8 ++++++--
4 files changed, 16 insertions(+), 2 deletions(-)
create mode 100644 demo/counter.ur
create mode 100644 demo/counter.urp
create mode 100644 demo/counter.urs
diff --git a/demo/counter.ur b/demo/counter.ur
new file mode 100644
index 00000000..b11fc936
--- /dev/null
+++ b/demo/counter.ur
@@ -0,0 +1,7 @@
+fun counter n = return
+ Current counter: {[n]}
+ Increment
+ Decrement
+
+
+fun main () = counter 0
diff --git a/demo/counter.urp b/demo/counter.urp
new file mode 100644
index 00000000..d22312c9
--- /dev/null
+++ b/demo/counter.urp
@@ -0,0 +1,2 @@
+
+counter
diff --git a/demo/counter.urs b/demo/counter.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/counter.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
diff --git a/demo/prose b/demo/prose
index 7f9f6bb0..8fedc557 100644
--- a/demo/prose
+++ b/demo/prose
@@ -44,12 +44,16 @@ rec.urp
Crafting webs of interlinked pages is easy, using recursion.
+counter.urp
+
+
It is also easy to pass state around via functions, in the style commonly associated with "continuation-based" web servers. As is usual for such systems, all state is stored on the client side. In this case, it is encoded in URLs.
+
+
In the implementation of Counter.counter, we see the notation {[...]}, which uses type classes to inject values of different types (int in this case) into XML. It's probably worth stating explicitly that XML fragments are not strings, so that the type-checker will enforce that our final piece of XML is valid.
+
form.urp
Here we see a basic form. The type system tracks which form inputs we include, and it enforces that the form handler function expects a record containing exactly those fields, with exactly the proper types.
-
In the implementation of handler, we see the notation {[...]}, which uses type classes to inject values of different types (string and bool in this case) into XML. It's probably worth stating explicitly that XML fragments are not strings, so that the type-checker will enforce that our final piece of XML is valid.
-
listShop.urp
This example shows off algebraic datatypes, parametric polymorphism, and functors.
--
cgit v1.2.3
From 0fa422bfaf3931aacff958cb73d44ebfa4191f4a Mon Sep 17 00:00:00 2001
From: Adam Chlipala
Date: Thu, 23 Oct 2008 12:58:35 -0400
Subject: Fix nasty de Bruijn substitution bug; TcSum demo
---
demo/prose | 4 ++
demo/tcSum.ur | 9 +++++
demo/tcSum.urp | 2 +
demo/tcSum.urs | 1 +
lib/basis.urs | 1 +
src/core_env.sml | 14 +++----
src/monoize.sml | 20 ++++++++--
src/reduce.sml | 115 ++++++++++++++++++++++++++++++-------------------------
8 files changed, 103 insertions(+), 63 deletions(-)
create mode 100644 demo/tcSum.ur
create mode 100644 demo/tcSum.urp
create mode 100644 demo/tcSum.urs
diff --git a/demo/prose b/demo/prose
index 8fedc557..19e9df0f 100644
--- a/demo/prose
+++ b/demo/prose
@@ -100,3 +100,7 @@ An unusual part of the third argument is the syntax [t1 ~ t2] within a
The general syntax for constant row types is [Name1 = t1, ..., NameN = tN], and there is a shorthand version [Name1, ..., NameN] for records of Units.
With sum defined, it is easy to make some sample calls. The form of the code for main does not make it apparent, but the compiler must "reverse engineer" the appropriate {Unit} from the {Type} available from the context at each call to sum.
+
+tcSum.urp
+
+
It's easy to adapt the last example to use type classes, such that we can sum the fields of records based on any numeric type.
diff --git a/demo/tcSum.ur b/demo/tcSum.ur
new file mode 100644
index 00000000..53679116
--- /dev/null
+++ b/demo/tcSum.ur
@@ -0,0 +1,9 @@
+fun sum (t ::: Type) (_ : num t) (fs ::: {Unit}) (x : $(mapUT t fs)) =
+ foldUR [t] [fn _ => t]
+ (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] n acc => n + acc)
+ zero [fs] x
+
+fun main () = return
+ {[sum {A = 0, B = 1}]}
+ {[sum {C = 2.1, D = 3.2, E = 4.3}]}
+
diff --git a/demo/tcSum.urp b/demo/tcSum.urp
new file mode 100644
index 00000000..8b36efc0
--- /dev/null
+++ b/demo/tcSum.urp
@@ -0,0 +1,2 @@
+
+tcSum
diff --git a/demo/tcSum.urs b/demo/tcSum.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/tcSum.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
diff --git a/lib/basis.urs b/lib/basis.urs
index a539f05e..a8c81353 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -20,6 +20,7 @@ val eq_string : eq string
val eq_bool : eq bool
class num
+val zero : t ::: Type -> num t -> t
val neg : t ::: Type -> num t -> t -> t
val plus : t ::: Type -> num t -> t -> t -> t
val minus : t ::: Type -> num t -> t -> t -> t
diff --git a/src/core_env.sml b/src/core_env.sml
index a4b48b8d..b399f62f 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -82,13 +82,13 @@ val liftConInExp =
val subConInExp =
U.Exp.mapB {kind = fn k => k,
con = fn (xn, rep) => fn c =>
- case c of
- CRel xn' =>
- (case Int.compare (xn', xn) of
- EQUAL => #1 rep
- | GREATER => CRel (xn' - 1)
- | LESS => c)
- | _ => c,
+ case c of
+ CRel xn' =>
+ (case Int.compare (xn', xn) of
+ EQUAL => #1 rep
+ | GREATER => CRel (xn' - 1)
+ | LESS => c)
+ | _ => c,
exp = fn _ => fn e => e,
bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
| (ctx, _) => ctx}
diff --git a/src/monoize.sml b/src/monoize.sml
index cacf3d6d..6a12306b 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -104,7 +104,8 @@ fun monoType env =
let
val t = mt env dtmap t
in
- (L'.TRecord [("Neg", (L'.TFun (t, t), loc)),
+ (L'.TRecord [("Zero", t),
+ ("Neg", (L'.TFun (t, t), loc)),
("Plus", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
("Minus", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
("Times", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
@@ -491,14 +492,16 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
(dummyExp, fm))
fun numTy t =
- (L'.TRecord [("Neg", (L'.TFun (t, t), loc)),
+ (L'.TRecord [("Zero", t),
+ ("Neg", (L'.TFun (t, t), loc)),
("Plus", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
("Minus", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
("Times", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
("Div", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
("Mod", (L'.TFun (t, (L'.TFun (t, t), loc)), loc))], loc)
- fun numEx (t, neg, plus, minus, times, dv, md) =
- ((L'.ERecord [("Neg", neg, (L'.TFun (t, t), loc)),
+ fun numEx (t, zero, neg, plus, minus, times, dv, md) =
+ ((L'.ERecord [("Zero", (L'.EPrim zero, loc), t),
+ ("Neg", neg, (L'.TFun (t, t), loc)),
("Plus", plus, (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
("Minus", minus, (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
("Times", times, (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
@@ -595,6 +598,13 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
(L'.EBinop ("!strcmp", (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc),
fm)
+ | L.ECApp ((L.EFfi ("Basis", "zero"), _), t) =>
+ let
+ val t = monoType env t
+ in
+ ((L'.EAbs ("r", numTy t, t,
+ (L'.EField ((L'.ERel 0, loc), "Zero"), loc)), loc), fm)
+ end
| L.ECApp ((L.EFfi ("Basis", "neg"), _), t) =>
let
val t = monoType env t
@@ -647,6 +657,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
(L'.EBinop (s, (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc)
in
numEx ((L'.TFfi ("Basis", "int"), loc),
+ Prim.Int (Int64.fromInt 0),
(L'.EAbs ("x", (L'.TFfi ("Basis", "int"), loc),
(L'.TFfi ("Basis", "int"), loc),
(L'.EUnop ("-", (L'.ERel 0, loc)), loc)), loc),
@@ -666,6 +677,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
(L'.EBinop (s, (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc)
in
numEx ((L'.TFfi ("Basis", "float"), loc),
+ Prim.Float 0.0,
(L'.EAbs ("x", (L'.TFfi ("Basis", "float"), loc),
(L'.TFfi ("Basis", "float"), loc),
(L'.EUnop ("-", (L'.ERel 0, loc)), loc)), loc),
diff --git a/src/reduce.sml b/src/reduce.sml
index 0250175f..927c8ff1 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -36,6 +36,7 @@ structure U = CoreUtil
val liftConInCon = E.liftConInCon
val subConInCon = E.subConInCon
+val liftConInExp = E.liftConInExp
val liftExpInExp =
U.Exp.mapB {kind = fn k => k,
@@ -63,6 +64,7 @@ val subExpInExp =
| LESS => e)
| _ => e,
bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
+ | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
| (ctx, _) => ctx}
val liftConInExp = E.liftConInExp
@@ -106,58 +108,67 @@ fun con env c =
and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env
fun exp env e =
- case e of
- ENamed n =>
- (case E.lookupENamed env n of
- (_, _, SOME e', _) => #1 e'
- | _ => e)
-
- | ECApp ((EApp ((EApp ((ECApp ((EFold ks, _), ran), _), f), _), i), _), (CRecord (k, xcs), loc)) =>
- (case xcs of
- [] => #1 i
- | (n, v) :: rest =>
- #1 (reduceExp env (EApp ((ECApp ((ECApp ((ECApp (f, n), loc), v), loc), (CRecord (k, rest), loc)), loc),
- (ECApp ((EApp ((EApp ((ECApp ((EFold ks, loc), ran), loc), f), loc), i), loc),
- (CRecord (k, rest), loc)), loc)), loc)))
-
- | EApp ((EAbs (_, _, _, e1), loc), e2) =>
- #1 (reduceExp env (subExpInExp (0, e2) e1))
- | ECApp ((ECAbs (_, _, e1), loc), c) =>
- #1 (reduceExp env (subConInExp (0, c) e1))
-
- | EField ((ERecord xes, _), (CName x, _), _) =>
- (case List.find (fn ((CName x', _), _, _) => x' = x
- | _ => false) xes of
- SOME (_, e, _) => #1 e
- | NONE => e)
- | EWith (r as (_, loc), x, e, {rest = (CRecord (k, xts), _), field}) =>
- let
- fun fields (remaining, passed) =
- case remaining of
- [] => []
- | (x, t) :: rest =>
- (x,
- (EField (r, x, {field = t,
- rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
- t) :: fields (rest, (x, t) :: passed)
- in
- #1 (reduceExp env (ERecord ((x, e, field) :: fields (xts, [])), loc))
- end
- | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) =>
- let
- fun fields (remaining, passed) =
- case remaining of
- [] => []
- | (x, t) :: rest =>
- (x,
- (EField (r, x, {field = t,
- rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
- t) :: fields (rest, (x, t) :: passed)
- in
- #1 (reduceExp env (ERecord (fields (xts, [])), loc))
- end
-
- | _ => e
+ let
+ (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan))]*)
+
+ val r = case e of
+ ENamed n =>
+ (case E.lookupENamed env n of
+ (_, _, SOME e', _) => #1 e'
+ | _ => e)
+
+ | ECApp ((EApp ((EApp ((ECApp ((EFold ks, _), ran), _), f), _), i), _), (CRecord (k, xcs), loc)) =>
+ (case xcs of
+ [] => #1 i
+ | (n, v) :: rest =>
+ #1 (reduceExp env (EApp ((ECApp ((ECApp ((ECApp (f, n), loc), v), loc), (CRecord (k, rest), loc)), loc),
+ (ECApp ((EApp ((EApp ((ECApp ((EFold ks, loc), ran), loc), f), loc), i), loc),
+ (CRecord (k, rest), loc)), loc)), loc)))
+
+ | EApp ((EAbs (_, _, _, e1), loc), e2) =>
+ #1 (reduceExp env (subExpInExp (0, e2) e1))
+ | ECApp ((ECAbs (_, _, e1), loc), c) =>
+ #1 (reduceExp env (subConInExp (0, c) e1))
+
+ | EField ((ERecord xes, _), (CName x, _), _) =>
+ (case List.find (fn ((CName x', _), _, _) => x' = x
+ | _ => false) xes of
+ SOME (_, e, _) => #1 e
+ | NONE => e)
+ | EWith (r as (_, loc), x, e, {rest = (CRecord (k, xts), _), field}) =>
+ let
+ fun fields (remaining, passed) =
+ case remaining of
+ [] => []
+ | (x, t) :: rest =>
+ (x,
+ (EField (r, x, {field = t,
+ rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
+ t) :: fields (rest, (x, t) :: passed)
+ in
+ #1 (reduceExp env (ERecord ((x, e, field) :: fields (xts, [])), loc))
+ end
+ | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) =>
+ let
+ fun fields (remaining, passed) =
+ case remaining of
+ [] => []
+ | (x, t) :: rest =>
+ (x,
+ (EField (r, x, {field = t,
+ rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
+ t) :: fields (rest, (x, t) :: passed)
+ in
+ #1 (reduceExp env (ERecord (fields (xts, [])), loc))
+ end
+
+ | _ => e
+ in
+ (*Print.prefaces "exp'" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan)),
+ ("r", CorePrint.p_exp env (r, ErrorMsg.dummySpan))];*)
+
+ r
+ end
and reduceExp env = U.Exp.mapB {kind = kind, con = con, exp = exp, bind = bind} env
--
cgit v1.2.3
From a2495d384c7747a079cb0f4bc31f44d626391068 Mon Sep 17 00:00:00 2001
From: Adam Chlipala
Date: Thu, 23 Oct 2008 14:03:12 -0400
Subject: Metaform demos, minus prose
---
demo/metaform.ur | 28 ++++++++++++++++++++++++++++
demo/metaform.urs | 6 ++++++
demo/metaform1.ur | 3 +++
demo/metaform1.urp | 3 +++
demo/metaform1.urs | 1 +
demo/metaform2.ur | 12 ++++++++++++
demo/metaform2.urp | 3 +++
demo/metaform2.urs | 1 +
demo/prose | 4 ++++
lib/top.ur | 20 ++++++++++++++++++++
lib/top.urs | 12 ++++++++++++
src/cjr_print.sml | 3 ++-
12 files changed, 95 insertions(+), 1 deletion(-)
create mode 100644 demo/metaform.ur
create mode 100644 demo/metaform.urs
create mode 100644 demo/metaform1.ur
create mode 100644 demo/metaform1.urp
create mode 100644 demo/metaform1.urs
create mode 100644 demo/metaform2.ur
create mode 100644 demo/metaform2.urp
create mode 100644 demo/metaform2.urs
diff --git a/demo/metaform.ur b/demo/metaform.ur
new file mode 100644
index 00000000..ae1197f4
--- /dev/null
+++ b/demo/metaform.ur
@@ -0,0 +1,28 @@
+functor Make (M : sig
+ con fs :: {Unit}
+ val names : $(mapUT string fs)
+ end) = struct
+
+ fun handler values = return
+ {foldURX2 [string] [string] [body]
+ (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] name value =>
+
{[name]} = {[value]}
+ )
+ [M.fs] M.names values}
+
+
+ fun main () = return
+
+
+
+end
diff --git a/demo/metaform.urs b/demo/metaform.urs
new file mode 100644
index 00000000..7a3fa62e
--- /dev/null
+++ b/demo/metaform.urs
@@ -0,0 +1,6 @@
+functor Make (M : sig
+ con fs :: {Unit}
+ val names : $(mapUT string fs)
+ end) : sig
+ val main : unit -> transaction page
+end
diff --git a/demo/metaform1.ur b/demo/metaform1.ur
new file mode 100644
index 00000000..c6a4664d
--- /dev/null
+++ b/demo/metaform1.ur
@@ -0,0 +1,3 @@
+open Metaform.Make(struct
+ val names = {A = "Tic", B = "Tac", C = "Toe"}
+ end)
diff --git a/demo/metaform1.urp b/demo/metaform1.urp
new file mode 100644
index 00000000..7f04b9b7
--- /dev/null
+++ b/demo/metaform1.urp
@@ -0,0 +1,3 @@
+
+metaform
+metaform1
diff --git a/demo/metaform1.urs b/demo/metaform1.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/metaform1.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
diff --git a/demo/metaform2.ur b/demo/metaform2.ur
new file mode 100644
index 00000000..430a42f0
--- /dev/null
+++ b/demo/metaform2.ur
@@ -0,0 +1,12 @@
+structure MM = Metaform.Make(struct
+ val names = {X = "x", Y = "y"}
+ end)
+
+fun diversion () = return
+ Welcome to the diversion.
+
+
+fun main () = return
+
+
diff --git a/demo/metaform2.urp b/demo/metaform2.urp
new file mode 100644
index 00000000..debc0448
--- /dev/null
+++ b/demo/metaform2.urp
@@ -0,0 +1,3 @@
+
+metaform
+metaform2
diff --git a/demo/metaform2.urs b/demo/metaform2.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/metaform2.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
diff --git a/demo/prose b/demo/prose
index 19e9df0f..4fb07673 100644
--- a/demo/prose
+++ b/demo/prose
@@ -104,3 +104,7 @@ An unusual part of the third argument is the syntax [t1 ~ t2] within a
tcSum.urp
It's easy to adapt the last example to use type classes, such that we can sum the fields of records based on any numeric type.
+
+metaform1.urp
+
+metaform2.urp
diff --git a/lib/top.ur b/lib/top.ur
index ab506c80..91cab991 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -36,6 +36,26 @@ fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
f [nm] [rest] r.nm (acc (r -- nm)))
(fn _ => i)
+fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type)
+ (f : nm :: Name -> rest :: {Unit}
+ -> fn [[nm] ~ rest] =>
+ tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
+ (i : tr []) =
+ fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r]
+ (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
+ [[nm] ~ rest] r1 r2 =>
+ f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+ (fn _ _ => i)
+
+fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit})
+ (f : nm :: Name -> rest :: {Unit}
+ -> fn [[nm] ~ rest] =>
+ tf1 -> tf2 -> xml ctx [] []) =
+ foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+ (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc =>
+ {f [nm] [rest] v1 v2}{acc})
+
+
fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
(f : nm :: Name -> t :: Type -> rest :: {Type}
-> fn [[nm] ~ rest] =>
diff --git a/lib/top.urs b/lib/top.urs
index abdb7477..29a1acf1 100644
--- a/lib/top.urs
+++ b/lib/top.urs
@@ -29,6 +29,18 @@ val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
tf -> tr rest -> tr ([nm] ++ rest))
-> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r
+val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
+ -> (nm :: Name -> rest :: {Unit}
+ -> fn [[nm] ~ rest] =>
+ tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
+ -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
+
+val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
+ -> (nm :: Name -> rest :: {Unit}
+ -> fn [[nm] ~ rest] =>
+ tf1 -> tf2 -> xml ctx [] [])
+ -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
+
val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
-> (nm :: Name -> t :: Type -> rest :: {Type}
-> fn [[nm] ~ rest] =>
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index f2af999b..089f98a1 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -1466,7 +1466,8 @@ fun p_file env (ds, ps) =
let
fun unurlify' rf t =
case t of
- TFfi (m, t) => string ("uw_" ^ ident m ^ "_unurlify" ^ capitalize t ^ "(ctx, &request)")
+ TFfi ("Basis", "unit") => string ("uw_unit_v")
+ | TFfi (m, t) => string ("uw_" ^ ident m ^ "_unurlify" ^ capitalize t ^ "(ctx, &request)")
| TRecord 0 => string "uw_unit_v"
| TRecord i =>
--
cgit v1.2.3
From da7b52ba28367cf2b31476e77e1a26e53e4765e4 Mon Sep 17 00:00:00 2001
From: Adam Chlipala
Date: Thu, 23 Oct 2008 17:35:10 -0400
Subject: Fix bug with bringing functor argument instances into scope; Ref
demo, minus prose
---
demo/prose | 2 ++
demo/ref.ur | 28 +++++++++++++++
demo/ref.urp | 4 +++
demo/ref.urs | 1 +
demo/refFun.ur | 27 ++++++++++++++
demo/refFun.urs | 10 ++++++
src/elab_env.sml | 105 ++++++++++++++++++++++++++++++++++++++-----------------
7 files changed, 145 insertions(+), 32 deletions(-)
create mode 100644 demo/ref.ur
create mode 100644 demo/ref.urp
create mode 100644 demo/ref.urs
create mode 100644 demo/refFun.ur
create mode 100644 demo/refFun.urs
diff --git a/demo/prose b/demo/prose
index 4fb07673..05bafd11 100644
--- a/demo/prose
+++ b/demo/prose
@@ -108,3 +108,5 @@ tcSum.urp
metaform1.urp
metaform2.urp
+
+ref.urp
diff --git a/demo/ref.ur b/demo/ref.ur
new file mode 100644
index 00000000..089529e3
--- /dev/null
+++ b/demo/ref.ur
@@ -0,0 +1,28 @@
+structure IR = RefFun.Make(struct
+ type t = int
+ val inj = _
+ end)
+
+structure SR = RefFun.Make(struct
+ type t = string
+ val inj = _
+ end)
+
+fun main () =
+ ir <- IR.new 3;
+ ir' <- IR.new 7;
+ sr <- SR.new "hi";
+
+ () <- IR.write ir' 10;
+
+ iv <- IR.read ir;
+ iv' <- IR.read ir';
+ sv <- SR.read sr;
+
+ () <- IR.delete ir;
+ () <- IR.delete ir';
+ () <- SR.delete sr;
+
+ return
+ {[iv]}, {[iv']}, {[sv]}
+
diff --git a/demo/ref.urp b/demo/ref.urp
new file mode 100644
index 00000000..c00e5406
--- /dev/null
+++ b/demo/ref.urp
@@ -0,0 +1,4 @@
+database dbname=test
+
+refFun
+ref
diff --git a/demo/ref.urs b/demo/ref.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/ref.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
diff --git a/demo/refFun.ur b/demo/refFun.ur
new file mode 100644
index 00000000..d58acee5
--- /dev/null
+++ b/demo/refFun.ur
@@ -0,0 +1,27 @@
+functor Make(M : sig
+ type data
+ val inj : sql_injectable data
+ end) = struct
+
+ type ref = int
+
+ sequence s
+ table t : { Id : int, Data : M.data }
+
+ fun new d =
+ id <- nextval s;
+ () <- dml (INSERT INTO t (Id, Data) VALUES ({id}, {d}));
+ return id
+
+ fun read r =
+ o <- oneOrNoRows (SELECT t.Data FROM t WHERE t.Id = {r});
+ return (case o of
+ None => error You already deleted that ref!
+ | Some r => r.T.Data)
+
+ fun write r d =
+ dml (UPDATE t SET Data = {d} WHERE Id = {r})
+
+ fun delete r =
+ dml (DELETE FROM t WHERE Id = {r})
+end
diff --git a/demo/refFun.urs b/demo/refFun.urs
new file mode 100644
index 00000000..bcecc8d3
--- /dev/null
+++ b/demo/refFun.urs
@@ -0,0 +1,10 @@
+functor Make(M : sig
+ type data
+ val inj : sql_injectable data
+ end) : sig
+ type ref
+ val new : M.data -> transaction ref
+ val read : ref -> transaction M.data
+ val write : ref -> M.data -> transaction unit
+ val delete : ref -> transaction unit
+end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 958d369c..edda9f38 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -159,10 +159,11 @@ val empty_class = {
ground = KM.empty
}
-fun printClasses cs = CM.appi (fn (cn, {ground = km}) =>
- (print (cn2s cn ^ ":");
- KM.appi (fn (ck, _) => print (" " ^ ck2s ck)) km;
- print "\n")) cs
+fun printClasses cs = (print "Classes:\n";
+ CM.appi (fn (cn, {ground = km}) =>
+ (print (cn2s cn ^ ":");
+ KM.appi (fn (ck, _) => print (" " ^ ck2s ck)) km;
+ print "\n")) cs)
type env = {
renameC : kind var' SM.map,
@@ -743,34 +744,74 @@ fun enrichClasses env classes (m1, ms) sgn =
| SgiClassAbs xn => found xn
| SgiClass (x, n, _) => found (x, n)
- | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) =>
- (case IM.find (newClasses, f) of
- NONE => default ()
- | SOME fx =>
- case class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a) of
- NONE => default ()
- | SOME ck =>
- let
- val cn = ClProj (m1, ms, fx)
-
- val classes =
- case CM.find (classes, cn) of
- NONE => classes
- | SOME class =>
- let
- val class = {
- ground = KM.insert (#ground class, ck,
- (EModProj (m1, ms, x), #2 sgn))
- }
- in
- CM.insert (classes, cn, class)
- end
- in
- (classes,
- newClasses,
- fmap,
- env)
- end)
+ | SgiVal (x, n, (CApp (f, a), _)) =>
+ let
+ fun unravel c =
+ case #1 c of
+ CUnif (_, _, _, ref (SOME c)) => unravel c
+ | CNamed n =>
+ ((case lookupCNamed env n of
+ (_, _, SOME c) => unravel c
+ | _ => c)
+ handle UnboundNamed _ => c)
+ | _ => c
+
+ val nc =
+ case f of
+ (CNamed f, _) => IM.find (newClasses, f)
+ | _ => NONE
+ in
+ case nc of
+ NONE =>
+ (case (class_name_in (unravel f),
+ class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a)) of
+ (SOME cn, SOME ck) =>
+ let
+ val classes =
+ case CM.find (classes, cn) of
+ NONE => classes
+ | SOME class =>
+ let
+ val class = {
+ ground = KM.insert (#ground class, ck,
+ (EModProj (m1, ms, x), #2 sgn))
+ }
+ in
+ CM.insert (classes, cn, class)
+ end
+ in
+ (classes,
+ newClasses,
+ fmap,
+ env)
+ end
+ | _ => default ())
+ | SOME fx =>
+ case class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a) of
+ NONE => default ()
+ | SOME ck =>
+ let
+ val cn = ClProj (m1, ms, fx)
+
+ val classes =
+ case CM.find (classes, cn) of
+ NONE => classes
+ | SOME class =>
+ let
+ val class = {
+ ground = KM.insert (#ground class, ck,
+ (EModProj (m1, ms, x), #2 sgn))
+ }
+ in
+ CM.insert (classes, cn, class)
+ end
+ in
+ (classes,
+ newClasses,
+ fmap,
+ env)
+ end
+ end
| SgiVal _ => default ()
| _ => default ()
end)
--
cgit v1.2.3
From c083f2b0659545c9a0f36faf1a56239f4efc8df2 Mon Sep 17 00:00:00 2001
From: Adam Chlipala
Date: Thu, 23 Oct 2008 17:52:04 -0400
Subject: Prose for Ref and Metaform
---
demo/prose | 13 ++++++++++++-
demo/refFun.ur | 1 +
2 files changed, 13 insertions(+), 1 deletion(-)
diff --git a/demo/prose b/demo/prose
index 05bafd11..e447aee3 100644
--- a/demo/prose
+++ b/demo/prose
@@ -76,6 +76,12 @@ sql.urp
+ref.urp
+
+
This example shows how to mix the module system with SQL to implement a kind of "abstract data type." The functor RefFun.Make takes in a type belonging to the type class of those types that may be included in SQL. The functor output includes an abstract type ref, along with operations for working with refs via transactions. In the functor implementation, we see that ref is implemented as int, treated as primary keys of a SQL table.
+
+
The functor creates a new encapsulated SQL sequence and table on each call. These local relations show up in the automatically-generated SQL file that should be run to prepare the database for use, but they are invisible from client code. We could change the functor to create different SQL relations, without needing to change client code.
+
sum.urp
Metaprogramming is one of the most important facilities of Ur. This example shows how to write a function that is able to sum up the fields of records of integers, no matter which set of fields the particular record has.
@@ -107,6 +113,11 @@ tcSum.urp
metaform1.urp
+
We can use metaprogramming with row types to build HTML forms (and their handlers) generically. The functor Metaform.Make takes in a unit row fs and a value-level record names assigning string names to the fields of fs. The functor implementation builds a form handler with a library function foldURX2, which runs over two value-level records in parallel, building an XML fragment.
+
+
The form itself is generated using the more primitive foldUR. We see the type xml form [] (mapUT string cols) as the result of the fold. This is the type of XML fragments that are suitable for inclusion in forms, require no form fields to be defined on entry, and themselves define form fields whose names and types are given by mapUT string cols. The useMore function "weakens" the type of an XML fragment, so that it "pretends" to require additional fields as input. This weakening is necessary to accommodate the general typing rule for concatenating bits of XML.
+
The functor use in Metaform1 is trivial. The compiler infers the value of the structure member fs from the type of the value provided for names.
+
metaform2.urp
-ref.urp
+
This example showcases code reuse by applying the same functor as in the last example. The Metaform2 module mixes pages from the functor with some new pages of its own.
diff --git a/demo/refFun.ur b/demo/refFun.ur
index d58acee5..a090b297 100644
--- a/demo/refFun.ur
+++ b/demo/refFun.ur
@@ -24,4 +24,5 @@ functor Make(M : sig
fun delete r =
dml (DELETE FROM t WHERE Id = {r})
+
end
--
cgit v1.2.3
From fbde7928c43149e02806949343783dc6e885ab0f Mon Sep 17 00:00:00 2001
From: Adam Chlipala
Date: Thu, 23 Oct 2008 18:18:51 -0400
Subject: Crud demo
---
demo/crud.ur | 178 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
demo/crud.urs | 26 +++++++++
demo/crud1.ur | 12 ++++
demo/crud1.urp | 5 ++
demo/prose | 31 ++++++++++
demo/ref.urp | 1 +
demo/sql.urp | 1 +
7 files changed, 254 insertions(+)
create mode 100644 demo/crud.ur
create mode 100644 demo/crud.urs
create mode 100644 demo/crud1.ur
create mode 100644 demo/crud1.urp
diff --git a/demo/crud.ur b/demo/crud.ur
new file mode 100644
index 00000000..472de6d4
--- /dev/null
+++ b/demo/crud.ur
@@ -0,0 +1,178 @@
+con colMeta = fn t_formT :: (Type * Type) => {
+ Nam : string,
+ Show : t_formT.1 -> xbody,
+ Widget : nm :: Name -> xml form [] [nm = t_formT.2],
+ WidgetPopulated : nm :: Name -> t_formT.1 -> xml form [] [nm = t_formT.2],
+ Parse : t_formT.2 -> t_formT.1,
+ Inject : sql_injectable t_formT.1
+ }
+con colsMeta = fn cols :: {(Type * Type)} => $(Top.mapT2T colMeta cols)
+
+fun default (t ::: Type) (sh : show t) (rd : read t) (inj : sql_injectable t)
+ name : colMeta (t, string) =
+ {Nam = name,
+ Show = txt,
+ Widget = fn nm :: Name => ,
+ WidgetPopulated = fn (nm :: Name) n =>
+ ,
+ Parse = readError,
+ Inject = _}
+
+val int = default
+val float = default
+val string = default
+
+fun bool name = {Nam = name,
+ Show = txt,
+ Widget = fn nm :: Name => ,
+ WidgetPopulated = fn (nm :: Name) b =>
+ ,
+ Parse = fn x => x,
+ Inject = _}
+
+functor Make(M : sig
+ con cols :: {(Type * Type)}
+ constraint [Id] ~ cols
+ val tab : sql_table ([Id = int] ++ mapT2T fstTT cols)
+
+ val title : string
+
+ val cols : colsMeta cols
+ end) = struct
+
+ open constraints M
+ val tab = M.tab
+
+ sequence seq
+
+ fun list () =
+ rows <- queryX (SELECT * FROM tab AS T)
+ (fn (fs : {T : $([Id = int] ++ mapT2T fstTT M.cols)}) =>
+
+
+
+ and main () =
+ ls <- list ();
+ return
+ {cdata M.title}
+
+
+
{cdata M.title}
+
+ {ls}
+
+
+end
diff --git a/demo/crud.urs b/demo/crud.urs
new file mode 100644
index 00000000..33090421
--- /dev/null
+++ b/demo/crud.urs
@@ -0,0 +1,26 @@
+con colMeta = fn t_formT :: (Type * Type) =>
+ {Nam : string,
+ Show : t_formT.1 -> xbody,
+ Widget : nm :: Name -> xml form [] [nm = t_formT.2],
+ WidgetPopulated : nm :: Name -> t_formT.1
+ -> xml form [] [nm = t_formT.2],
+ Parse : t_formT.2 -> t_formT.1,
+ Inject : sql_injectable t_formT.1}
+con colsMeta = fn cols :: {(Type * Type)} => $(mapT2T colMeta cols)
+
+val int : string -> colMeta (int, string)
+val float : string -> colMeta (float, string)
+val string : string -> colMeta (string, string)
+val bool : string -> colMeta (bool, bool)
+
+functor Make(M : sig
+ con cols :: {(Type * Type)}
+ constraint [Id] ~ cols
+ val tab : sql_table ([Id = int] ++ mapT2T fstTT cols)
+
+ val title : string
+
+ val cols : colsMeta cols
+ end) : sig
+ val main : unit -> transaction page
+end
diff --git a/demo/crud1.ur b/demo/crud1.ur
new file mode 100644
index 00000000..3849e822
--- /dev/null
+++ b/demo/crud1.ur
@@ -0,0 +1,12 @@
+table t1 : {Id : int, A : int, B : string, C : float, D : bool}
+
+open Crud.Make(struct
+ val tab = t1
+
+ val title = "Crud1"
+
+ val cols = {A = Crud.int "A",
+ B = Crud.string "B",
+ C = Crud.float "C",
+ D = Crud.bool "D"}
+ end)
diff --git a/demo/crud1.urp b/demo/crud1.urp
new file mode 100644
index 00000000..bfc2d14e
--- /dev/null
+++ b/demo/crud1.urp
@@ -0,0 +1,5 @@
+database dbname=test
+sql crud1.sql
+
+crud
+crud1
diff --git a/demo/prose b/demo/prose
index e447aee3..6b7ddf29 100644
--- a/demo/prose
+++ b/demo/prose
@@ -121,3 +121,34 @@ metaform1.urp
metaform2.urp
This example showcases code reuse by applying the same functor as in the last example. The Metaform2 module mixes pages from the functor with some new pages of its own.
+
+crud1.urp
+
+
This example pulls together much of what we have seen so far. It involves a generic "admin interface" builder. That is, we have the Crud.Make functor, which takes in a description of a table and outputs a sub-application for viewing and editing that table.
+
+
The signature of Crud.Make is based around a type function colMeta, which describes which supporting values we need for each column. This function is declared with the keyword con, which stands for "constructor," the general class of "compile-time things" that includes types. An argument to colMeta has kind (Type * Type), which means that it must be a type-level tuple. The first type is how the column is represented in SQL, and the second is how we represent it in HTML forms. In order, the components of the resulting record give:
+
+
+
A display name
+
A way of pretty-printing values of the column
+
A way of generating an HTML form widget to input this column
+
A way of generating an HTML form widget with an initial value specified
+
A way of parsing values of the column from strings
+
A type class witness, showing that the SQL representation can really be included in SQL
+
+
+
The function colsMeta lifts colMeta over type-level records of type pairs. The Crud module also defines reasonable default colMeta values for some primitive types.
+
+
The functor signature tells us (in order) that an input must contain:
+
+
+
A type pair record cols
+
A proof that cols does not contain a field named Id
+
A SQL table tab with an Id field of type int and other fields whose names and types are read off of cols
+
A display title for the admin interface
+
A record of meta-data for the columns
+
+
+
Looking at crud1.ur, we see that a use of the functor is almost trivial. Only the value components of the argument structure must be provided. The column row type is inferred, and the disjointness constraint is proved automatically.
+
+
We won't go into detail on the implementation of Crud.Make. The types of the functions used there can be found in the signatures of the built-in Basis module and the Top module from the standard library. The signature of the first and the signature and implementation of the second can be found in the lib directory of the Ur/Web distribution.
diff --git a/demo/ref.urp b/demo/ref.urp
index c00e5406..a6bb1de3 100644
--- a/demo/ref.urp
+++ b/demo/ref.urp
@@ -1,4 +1,5 @@
database dbname=test
+sql ref.sql
refFun
ref
diff --git a/demo/sql.urp b/demo/sql.urp
index 1b8bb5a4..7894da95 100644
--- a/demo/sql.urp
+++ b/demo/sql.urp
@@ -1,3 +1,4 @@
database dbname=test
+sql sql.sql
sql
--
cgit v1.2.3
From 9569ae99c75cb74aeeb6fa02e6eec9eff2c7669f Mon Sep 17 00:00:00 2001
From: Adam Chlipala
Date: Thu, 23 Oct 2008 18:45:10 -0400
Subject: Crud2 demo
---
demo/crud2.sql | 6 ++++++
demo/crud2.ur | 34 ++++++++++++++++++++++++++++++++++
demo/crud2.urp | 5 +++++
demo/prose | 4 ++++
lib/basis.urs | 3 ++-
lib/top.ur | 2 ++
lib/top.urs | 2 ++
src/monoize.sml | 9 +++++++++
8 files changed, 64 insertions(+), 1 deletion(-)
create mode 100644 demo/crud2.sql
create mode 100644 demo/crud2.ur
create mode 100644 demo/crud2.urp
diff --git a/demo/crud2.sql b/demo/crud2.sql
new file mode 100644
index 00000000..88568f2a
--- /dev/null
+++ b/demo/crud2.sql
@@ -0,0 +1,6 @@
+CREATE TABLE uw_Crud2_t(uw_id int8 NOT NULL, uw_nam text NOT NULL,
+ uw_ready bool NOT NULL);
+
+ CREATE SEQUENCE uw_Crud2_Crud_Make_seq;
+
+
\ No newline at end of file
diff --git a/demo/crud2.ur b/demo/crud2.ur
new file mode 100644
index 00000000..1db376d4
--- /dev/null
+++ b/demo/crud2.ur
@@ -0,0 +1,34 @@
+table t : {Id : int, Nam : string, Ready : bool}
+
+open Crud.Make(struct
+ val tab = t
+
+ val title = "Are you ready?"
+
+ val cols = {Nam = Crud.string "Name",
+ Ready = {Nam = "Ready",
+ Show = (fn b => if b then
+ Ready!
+ else
+ Not ready),
+ Widget = (fn (nm :: Name) =>
+
+ ),
+ WidgetPopulated = (fn (nm :: Name) b =>
+
+ ),
+ Parse = (fn s =>
+ case s of
+ "Ready" => True
+ | "Not ready" => False
+ | _ => error Invalid ready/not ready),
+ Inject = _
+ }
+ }
+ end)
diff --git a/demo/crud2.urp b/demo/crud2.urp
new file mode 100644
index 00000000..d552e1a7
--- /dev/null
+++ b/demo/crud2.urp
@@ -0,0 +1,5 @@
+database dbname=test
+sql crud2.sql
+
+crud
+crud2
diff --git a/demo/prose b/demo/prose
index 6b7ddf29..3b9d9ebb 100644
--- a/demo/prose
+++ b/demo/prose
@@ -152,3 +152,7 @@ crud1.urp
Looking at crud1.ur, we see that a use of the functor is almost trivial. Only the value components of the argument structure must be provided. The column row type is inferred, and the disjointness constraint is proved automatically.
We won't go into detail on the implementation of Crud.Make. The types of the functions used there can be found in the signatures of the built-in Basis module and the Top module from the standard library. The signature of the first and the signature and implementation of the second can be found in the lib directory of the Ur/Web distribution.
+
+crud2.urp
+
+
This example shows another application of Crud.Make. We mix one standard column with one customized column. We write an underscore for the Inject field of meta-data, since the type class facility can infer that witness.
diff --git a/lib/basis.urs b/lib/basis.urs
index a8c81353..fce29ff9 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -18,6 +18,7 @@ val eq_int : eq int
val eq_float : eq float
val eq_string : eq string
val eq_bool : eq bool
+val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
class num
val zero : t ::: Type -> num t -> t
@@ -365,7 +366,7 @@ val radioOption : unit -> tag [Value = string] radio [] [] []
con select = [Select]
val select : formTag string select []
-val option : unit -> tag [Value = string] select [] [] []
+val option : unit -> tag [Value = string, Selected = bool] select [] [] []
val submit : ctx ::: {Unit} -> use ::: {Type}
-> fn [[Form] ~ ctx] =>
diff --git a/lib/top.ur b/lib/top.ur
index 91cab991..0bc345de 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -1,3 +1,5 @@
+fun not b = if b then False else True
+
con idT (t :: Type) = t
con record (t :: {Type}) = $t
con fstTT (t :: (Type * Type)) = t.1
diff --git a/lib/top.urs b/lib/top.urs
index 29a1acf1..22cebb16 100644
--- a/lib/top.urs
+++ b/lib/top.urs
@@ -1,3 +1,5 @@
+val not : bool -> bool
+
con idT = fn t :: Type => t
con record = fn t :: {Type} => $t
con fstTT = fn t :: (Type * Type) => t.1
diff --git a/src/monoize.sml b/src/monoize.sml
index 6a12306b..5fda4fa1 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -597,6 +597,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
(L'.TFfi ("Basis", "bool"), loc),
(L'.EBinop ("!strcmp", (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc),
fm)
+ | L.ECApp ((L.EFfi ("Basis", "mkEq"), _), t) =>
+ let
+ val t = monoType env t
+ val b = (L'.TFfi ("Basis", "bool"), loc)
+ val dom = (L'.TFun (t, (L'.TFun (t, b), loc)), loc)
+ in
+ ((L'.EAbs ("f", dom, dom,
+ (L'.ERel 0, loc)), loc), fm)
+ end
| L.ECApp ((L.EFfi ("Basis", "zero"), _), t) =>
let
--
cgit v1.2.3
From d27809108ef5ce4ed389cd39562e0dabb4a38c75 Mon Sep 17 00:00:00 2001
From: Adam Chlipala
Date: Fri, 24 Oct 2008 16:13:53 -0400
Subject: Stop including functors in paths
---
src/corify.sml | 37 ++++++++++++++-----------------------
1 file changed, 14 insertions(+), 23 deletions(-)
diff --git a/src/corify.sml b/src/corify.sml
index 09af27d0..89d1e63f 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -109,9 +109,9 @@ structure St : sig
val lookupStrByName : string * t -> t
val lookupStrByNameOpt : string * t -> t option
- val bindFunctor : t -> string list -> string -> int -> string -> int -> L.str -> t
- val lookupFunctorById : t -> int -> string list * string * int * L.str
- val lookupFunctorByName : string * t -> string list * string * int * L.str
+ val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
+ val lookupFunctorById : t -> int -> string * int * L.str
+ val lookupFunctorByName : string * t -> string * int * L.str
end = struct
datatype flattening =
@@ -120,7 +120,7 @@ datatype flattening =
constructors : L'.patCon SM.map,
vals : int SM.map,
strs : flattening SM.map,
- funs : (string list * string * int * L.str) SM.map}
+ funs : (string * int * L.str) SM.map}
| FFfi of {mod : string,
vals : L'.con SM.map,
constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map}
@@ -131,7 +131,7 @@ type t = {
constructors : L'.patCon IM.map,
vals : int IM.map,
strs : flattening IM.map,
- funs : (string list * string * int * L.str) IM.map,
+ funs : (string * int * L.str) IM.map,
current : flattening,
nested : flattening list
}
@@ -405,21 +405,21 @@ fun lookupStrByNameOpt (m, {basis, current = FNormal {strs, ...}, ...} : t) =
fun bindFunctor ({basis, cons, constructors, vals, strs, funs,
current = FNormal {name, cons = mcons, constructors = mconstructors,
vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
- mods x n xa na str =
+ x n xa na str =
{basis = basis,
cons = cons,
constructors = constructors,
vals = vals,
strs = strs,
- funs = IM.insert (funs, n, (mods, xa, na, str)),
+ funs = IM.insert (funs, n, (xa, na, str)),
current = FNormal {name = name,
cons = mcons,
constructors = mconstructors,
vals = mvals,
strs = mstrs,
- funs = SM.insert (mfuns, x, (mods, xa, na, str))},
+ funs = SM.insert (mfuns, x, (xa, na, str))},
nested = nested}
- | bindFunctor _ _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
+ | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
fun lookupFunctorById ({funs, ...} : t) n =
case IM.find (funs, n) of
@@ -696,7 +696,7 @@ fun corifyDecl mods ((d, loc : EM.span), st) =
| L.DSgn _ => ([], st)
| L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
- ([], St.bindFunctor st (x :: mods) x n xa na str)
+ ([], St.bindFunctor st x n xa na str)
| L.DStr (x, n, _, (L.StrProj (str, x'), _)) =>
let
@@ -706,9 +706,9 @@ fun corifyDecl mods ((d, loc : EM.span), st) =
SOME st' => St.bindStr st x n st'
| NONE =>
let
- val (mods', x', n', str') = St.lookupFunctorByName (x', inner)
+ val (x', n', str') = St.lookupFunctorByName (x', inner)
in
- St.bindFunctor st mods' x n x' n' str'
+ St.bindFunctor st x n x' n' str'
end
in
([], st)
@@ -957,20 +957,11 @@ and corifyStr mods ((str, _), st) =
| L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str)
| _ => raise Fail "Corify of fancy functor application [2]"
- val (fmods, xa, na, body) = unwind str1
+ val (xa, na, body) = unwind str1
val (ds1, {inner = inner', outer}) = corifyStr mods (str2, st)
- val mods' = case #1 str2 of
- L.StrConst _ => fmods @ mods
- | _ =>
- let
- val ast = unwind' str2
- in
- fmods @ St.name ast
- end
-
- val (ds2, {inner, outer}) = corifyStr mods' (body, St.bindStr outer xa na inner')
+ val (ds2, {inner, outer}) = corifyStr mods (body, St.bindStr outer xa na inner')
in
(ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer})
end
--
cgit v1.2.3
From 4f82b8197a0e0b520882c0173f321bd948fc7b50 Mon Sep 17 00:00:00 2001
From: Adam Chlipala
Date: Fri, 24 Oct 2008 16:47:18 -0400
Subject: Transactions seem to be working
---
.hgignore | 2 ++
src/c/driver.c | 56 ++++++++++++++++++++++++++++++++++++++++-
src/cjr_print.sml | 75 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
tests/aborter.sql | 3 +++
tests/aborter.ur | 5 ++++
tests/aborter.urp | 4 +++
6 files changed, 144 insertions(+), 1 deletion(-)
create mode 100644 tests/aborter.sql
create mode 100644 tests/aborter.ur
create mode 100644 tests/aborter.urp
diff --git a/.hgignore b/.hgignore
index f6368700..8c3417d4 100644
--- a/.hgignore
+++ b/.hgignore
@@ -24,3 +24,5 @@ src/config.sml
demo/out/*.html
demo/demo.*
+
+*.sql
diff --git a/src/c/driver.c b/src/c/driver.c
index 09478270..db982d96 100644
--- a/src/c/driver.c
+++ b/src/c/driver.c
@@ -51,6 +51,24 @@ static pthread_cond_t queue_cond = PTHREAD_COND_INITIALIZER;
#define MAX_RETRIES 5
+int uw_db_begin(uw_context);
+int uw_db_commit(uw_context);
+int uw_db_rollback(uw_context);
+
+static int try_rollback(uw_context ctx) {
+ int r = uw_db_rollback(ctx);
+
+ if (r) {
+ printf("Error running SQL ROLLBACK\n");
+ uw_reset(ctx);
+ uw_write(ctx, "HTTP/1.1 500 Internal Server Error\n\r");
+ uw_write(ctx, "Content-type: text/plain\r\n\r\n");
+ uw_write(ctx, "Error running SQL ROLLBACK\n");
+ }
+
+ return r;
+}
+
static void *worker(void *data) {
int me = *(int *)data, retries_left = MAX_RETRIES;
uw_context ctx = uw_init(1024, 0);
@@ -116,6 +134,7 @@ static void *worker(void *data) {
*back = 0;
if (s = strstr(buf, "\r\n\r\n")) {
+ failure_kind fk;
char *cmd, *path, path_copy[uw_bufsize+1], *inputs;
*s = 0;
@@ -169,7 +188,20 @@ static void *worker(void *data) {
printf("Serving URI %s....\n", path);
while (1) {
- failure_kind fk;
+ if (uw_db_begin(ctx)) {
+ printf("Error running SQL BEGIN\n");
+ if (retries_left)
+ --retries_left;
+ else {
+ fk = FATAL;
+ uw_reset(ctx);
+ uw_write(ctx, "HTTP/1.1 500 Internal Server Error\n\r");
+ uw_write(ctx, "Content-type: text/plain\r\n\r\n");
+ uw_write(ctx, "Error running SQL BEGIN\n");
+
+ break;
+ }
+ }
uw_write(ctx, "HTTP/1.1 200 OK\r\n");
uw_write(ctx, "Content-type: text/html\r\n\r\n");
@@ -179,6 +211,17 @@ static void *worker(void *data) {
fk = uw_begin(ctx, path_copy);
if (fk == SUCCESS) {
uw_write(ctx, "