update in binaries for λδ

[helm.git] / matita / matita / contribs / lambdadelta / bin / roles / rolesEngine.ml

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
index 4a3a92cb5b3ccc9e34cc2cadf324fc46813423d2..73cca4e6618da4ab5499a2cccbbedac16a3ae12b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
@@ -67,6 +67,15 @@ let add_tops v =
   end;
   if ts <> [] then st.ET.t <- ts
 
+let rec add_matching () =
+  match EU.match_names 0 0 st.ET.t st.ET.w with
+  | None          -> ()
+  | Some  (ti,wi) ->
+    toggle_entry [1;ti];
+    toggle_entry [2;wi];
+    add_role ();
+    add_matching ()
+
 let read_waiting fname =
   if st.ET.s = [] then EU.raise_error ET.ENoStage else
   let ich = Scanf.Scanning.open_in fname in
@@ -90,3 +99,10 @@ let write_status () =
   let och = open_out fname in
   EO.out_status och st;
   close_out och
+
+let print_status () =
+  EO.out_status stdout st
+
+let visit_status before_t each_t after_t before_w each_w after_w =
+  EU.list_visit before_t each_t after_t EU.string_of_obj [1] st.ET.t;
+  EU.list_visit before_w each_w after_w EU.string_of_name [2] st.ET.w