summaryrefslogtreecommitdiff
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
parenta2495d384c7747a079cb0f4bc31f44d626391068 (diff)
Fix bug with bringing functor argument instances into scope; Ref demo, minus prose
-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
-rw-r--r--src/elab_env.sml105
7 files changed, 145 insertions, 32 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
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)