summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-03-26 15:54:04 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-03-26 15:54:04 -0400
commitb80bc0fde66898326c077f7a3aa47151d7f9e755 (patch)
treeddd45517e0df460b44d219633cdb5645f5d29bf8
parent88f948c12e78d9e3e75eb28864ade3395e5c6c86 (diff)
Enforce termination of type class instances
-rw-r--r--src/elab_env.sml39
-rw-r--r--tests/type_class.ur14
2 files changed, 48 insertions, 5 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 9f64a8c2..de33ec56 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -182,6 +182,7 @@ fun compare x =
fn () => String.compare (x1, x2)))
end
+structure CS = BinarySetFn(CK)
structure CM = BinaryMapFn(CK)
datatype class_key =
@@ -697,8 +698,8 @@ fun rule_in c =
case #1 c of
TFun (hyp, c) =>
(case class_pair_in hyp of
- NONE => NONE
- | SOME p => clauses (c, p :: hyps))
+ SOME (p as (_, CkRel _)) => clauses (c, p :: hyps)
+ | _ => NONE)
| _ =>
case class_pair_in c of
NONE => NONE
@@ -730,6 +731,32 @@ fun rule_in c =
| _ => quantifiers (c, 0)
end
+fun inclusion (classes : class CM.map, init, inclusions, f, e : exp) =
+ let
+ fun search (f, fs) =
+ if f = init then
+ NONE
+ else if CS.member (fs, f) then
+ SOME fs
+ else
+ let
+ val fs = CS.add (fs, f)
+ in
+ case CM.find (classes, f) of
+ NONE => SOME fs
+ | SOME {inclusions = fs', ...} =>
+ CM.foldli (fn (f', _, fs) =>
+ case fs of
+ NONE => NONE
+ | SOME fs => search (f', fs)) (SOME fs) fs'
+ end
+ in
+ case search (f, CS.empty) of
+ SOME _ => CM.insert (inclusions, f, e)
+ | NONE => (ErrorMsg.errorAt (#2 e) "Type class inclusion would create a cycle";
+ inclusions)
+ end
+
fun pushENamedAs (env : env) x n t =
let
val classes = #classes env
@@ -749,7 +776,7 @@ fun pushENamedAs (env : env) x n t =
inclusions = #inclusions class}
| Inclusion f' =>
{ground = #ground class,
- inclusions = CM.insert (#inclusions class, f', e)}
+ inclusions = inclusion (classes, f, #inclusions class, f', e)}
in
CM.insert (classes, f, class)
end
@@ -1113,7 +1140,8 @@ fun enrichClasses env classes (m1, ms) sgn =
inclusions = #inclusions class}
| Inclusion f' =>
{ground = #ground class,
- inclusions = CM.insert (#inclusions class,
+ inclusions = inclusion (classes, cn,
+ #inclusions class,
globalizeN f', e)}
in
CM.insert (classes, cn, class)
@@ -1146,7 +1174,8 @@ fun enrichClasses env classes (m1, ms) sgn =
inclusions = #inclusions class}
| Inclusion f' =>
{ground = #ground class,
- inclusions = CM.insert (#inclusions class,
+ inclusions = inclusion (classes, cn,
+ #inclusions class,
globalizeN f', e)}
in
CM.insert (classes, cn, class)
diff --git a/tests/type_class.ur b/tests/type_class.ur
index a41ccdc8..8c77bbad 100644
--- a/tests/type_class.ur
+++ b/tests/type_class.ur
@@ -10,10 +10,16 @@ structure M : sig
val option_default : t ::: Type -> default t -> default (option t)
val pair_default : a ::: Type -> b ::: Type -> default a -> default b -> default (pair a b)
+ (*val uh_oh : t ::: Type -> default t -> default t*)
+
class awesome
val awesome_default : t ::: Type -> awesome t -> default t
val float_awesome : awesome float
+
+ val oh_my : t ::: Type -> awesome (option t) -> awesome (option t)
+
+ val awesome : t ::: Type -> awesome t -> t
end = struct
class default t = t
fun get (t ::: Type) (x : t) = x
@@ -24,10 +30,16 @@ end = struct
fun option_default (t ::: Type) (x : t) = Some x
fun pair_default (a ::: Type) (b ::: Type) (x : a) (y : b) = Pair (x, y)
+ (*fun uh_oh (t ::: Type) (x : t) = x*)
+
class awesome t = t
fun awesome_default (t ::: Type) (x : t) = x
val float_awesome = 1.23
+
+ fun oh_my (t ::: Type) (x : option t) = x
+
+ fun awesome (t ::: Type) (x : t) = x
end
open M
@@ -49,6 +61,8 @@ fun show_option (t ::: Type) (_ : show t) : show (option t) =
None => "None"
| Some y => show y)
+(*val x : option float = awesome*)
+
fun show_pair (a ::: Type) (b ::: Type) (_ : show a) (_ : show b) : show (pair a b) =
mkShow (fn x =>
case x of