diff options
| -rw-r--r-- | src/elab_env.sml | 39 | ||||
| -rw-r--r-- | tests/type_class.ur | 14 |
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 |