+*)
+
+
+let backward_simplify_active env (new_neg, new_pos) active =
+ let new_pos = List.map (fun e -> Positive, e) new_pos in
+ let active =
+ List.fold_right
+ (fun (s, equality) res ->
+ match forward_simplify env ~active:new_pos (s, equality) with
+ | None -> res
+ | Some e -> e::res)
+ active []
+ in
+ let find eq1 where =
+ List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
+ in
+ List.fold_right
+ (fun (s, eq) res ->
+ if (is_identity env eq) || (find eq res) then
+ res
+ else
+ (s, eq)::res)
+ active []
+;;
+
+
+let backward_simplify_passive env (new_neg, new_pos) passive =
+ let new_pos = List.map (fun e -> Positive, e) new_pos in
+ let (nl, ns), (pl, ps) = passive in
+ let f sign equality (resl, ress, newn) =
+ match forward_simplify env ~active:new_pos (sign, equality) with
+ | None -> resl, EqualitySet.remove equality ress, newn
+ | Some (s, e) ->
+ if equality = e then
+ equality::resl, ress, newn
+ else
+ let ress = EqualitySet.remove equality ress in
+ resl, ress, e::newn
+ in
+ let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
+ and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
+ match newn, newp with
+ | [], [] -> ((nl, ns), (pl, ps)), None
+ | _, _ -> ((nl, ns), (pl, ps)), Some (newn, newp)
+;;
+
+
+let backward_simplify env ?(active=[]) ?passive new' =
+ let active = backward_simplify_active env new' active in
+ match passive with
+ | None ->
+ active, (([], EqualitySet.empty), ([], EqualitySet.empty)), None
+ | Some passive ->
+ let passive, new' =
+ backward_simplify_passive env new' passive in
+ active, passive, new'
+;;