+let close env new' given =
+ let new_pos, new_table, min_weight =
+ List.fold_left
+ (fun (l, t, w) e ->
+ let ew, _, _, _, _ = e in
+ (Positive, e)::l, Indexing.index t e, min ew w)
+ ([], Indexing.empty, 1000000) (snd new')
+ in
+ List.fold_left
+ (fun (n,p) (s,c) ->
+ let neg,pos = infer env s c (new_pos,new_table) in
+ neg@n,pos@p)
+ ([],[]) given
+;;
+
+let is_commutative_law eq =
+ let w, proof, (eq_ty, left, right, order), metas, args = snd eq in
+ match left,right with
+ Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1],
+ Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
+ f1 = f2 && a1 = b2 && a2 = b1
+ | _ -> false
+;;
+
+let prova env new' active =
+ let given = List.filter is_commutative_law (fst active) in
+ let _ =
+ debug_print
+ (lazy
+ (Printf.sprintf "symmetric:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e))
+ (given)))))) in
+ close env new' given
+;;
+