(* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements
* (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
-let rec min acc = function
+let rec min acc skipped = function
| c::tl ->
- if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
- | [] -> acc
+ if List.exists (lb c) (tl@acc)
+ then min acc (c::skipped) tl else min (c::acc) skipped tl
+ | [] -> acc, skipped
+;;
+
+
+let sort l =
+ let low, high = min [] [] l in low @ high
;;
let meets metasenv subst context (grow_left,left) (grow_right,right) =
in
List.map
(fun (c,uo1,uo2) ->
- let metasenv, uo1 =
- if grow_left then saturate metasenv uo1 else metasenv, None in
- let metasenv, uo2 =
- if grow_right then saturate metasenv uo2 else metasenv, None in
+ let metasenv, uo1 = saturate metasenv uo1 in
+ let metasenv, uo2 = saturate metasenv uo2 in
c,metasenv, uo1, uo2)
- (min [] (intersect (grow left) (grow right)))
+ (sort (intersect
+ (if grow_left then grow left else [left,None])
+ (if grow_right then grow right else [right,None])))
;;
(* EOF *)