summaryrefslogtreecommitdiff
path: root/demo
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-23 17:35:10 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-23 17:35:10 -0400
commitda7b52ba28367cf2b31476e77e1a26e53e4765e4 (patch)
tree5de8de2f16499f80ffe6cd1cb7bc2afb6ca851d4 /demo
parenta2495d384c7747a079cb0f4bc31f44d626391068 (diff)
Fix bug with bringing functor argument instances into scope; Ref demo, minus prose
Diffstat (limited to 'demo')
-rw-r--r--demo/prose2
-rw-r--r--demo/ref.ur28
-rw-r--r--demo/ref.urp4
-rw-r--r--demo/ref.urs1
-rw-r--r--demo/refFun.ur27
-rw-r--r--demo/refFun.urs10
6 files changed, 72 insertions, 0 deletions
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 <xml><body>
+ {[iv]}, {[iv']}, {[sv]}
+ </body></xml>
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 <xml>You already deleted that ref!</xml>
+ | 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