aboutsummaryrefslogtreecommitdiffhomepage
path: root/demo
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-10-05 16:36:38 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-10-05 16:36:38 -0400
commit78e557c3b405113b62bc945382415895860a5825 (patch)
tree4bb99b24aa10939567424dd11c6c414094f8fe4f /demo
parentd795d3e7d07b8770335b414fd1b0d32af41016c5 (diff)
Better location calculation for record unification error messages; infer kind arguments to module-projected variables
Diffstat (limited to 'demo')
-rw-r--r--demo/more/orm.ur29
-rw-r--r--demo/more/orm.urp2
-rw-r--r--demo/more/orm.urs19
3 files changed, 50 insertions, 0 deletions
diff --git a/demo/more/orm.ur b/demo/more/orm.ur
new file mode 100644
index 00000000..9abc0234
--- /dev/null
+++ b/demo/more/orm.ur
@@ -0,0 +1,29 @@
+con link = fn t :: Type => unit
+
+con meta = fn col :: Type => {
+ Link : link col,
+ Inj : sql_injectable col
+ }
+
+functor Table(M : sig
+ con cols :: {Type}
+ val cols : $(map meta cols)
+ constraint [Id] ~ cols
+ val folder : folder cols
+ end) = struct
+ type id = int
+ val inj = _
+ val id : meta id = {Link = (),
+ Inj = inj}
+
+ sequence s
+ table t : ([Id = id] ++ M.cols)
+
+ fun create (r : $M.cols) =
+ id <- nextval s;
+ dml (insert t ({Id = sql_inject id}
+ ++ map2 [meta] [Top.id] [sql_exp [] [] []]
+ (fn [t ::: Type] (meta : meta t) (v : t) => @sql_inject meta.Inj v)
+ [_] M.folder M.cols r));
+ return id
+end
diff --git a/demo/more/orm.urp b/demo/more/orm.urp
new file mode 100644
index 00000000..7380983a
--- /dev/null
+++ b/demo/more/orm.urp
@@ -0,0 +1,2 @@
+
+orm
diff --git a/demo/more/orm.urs b/demo/more/orm.urs
new file mode 100644
index 00000000..8fab3ae8
--- /dev/null
+++ b/demo/more/orm.urs
@@ -0,0 +1,19 @@
+con link :: Type -> Type
+
+con meta = fn col :: Type => {
+ Link : link col,
+ Inj : sql_injectable col
+ }
+
+functor Table(M : sig
+ con cols :: {Type}
+ val cols : $(map meta cols)
+ constraint [Id] ~ cols
+ val folder : folder cols
+ end) : sig
+ type id
+ val inj : sql_injectable id
+ val id : meta id
+
+ val create : $M.cols -> transaction id
+end