update in binaries for λδ

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

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
index 066d7b865e929faeb285a99dcc108df5c78a007a..ae8dc9fe0beea34def9771f3e81085da6ce0d14e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
@@ -67,6 +67,17 @@ let rec list_select r = function
     | true , Some _ -> raise_error (ET.EWrongSelect)
     end
 
+let rec list_exists compare = function
+  | []        -> false
+  | (_,a)::tl ->
+    let b = compare a in
+    if b <= 0 then b = 0 else
+    list_exists compare tl
+
+let rec list_count s c = function
+  | []         -> s, c
+  | (b, _)::tl -> list_count (s + if b then 1 else 0) (succ c) tl
+
 let string_of_version v =
   String.concat "." (List.map string_of_int v)
 
@@ -105,6 +116,10 @@ let objs_union os1 os2 =
   let error o = ET.EObjClash o in
   list_union error compare_objs os1 os2
 
+let rec rev_objs_of_names v os = function
+  | []        -> os
+  | (b,n)::tl -> rev_objs_of_names v ((b,(v,n))::os) tl
+
 let obj_of_role r =
   let n = match r.ET.n with
     | []        -> []
@@ -122,20 +137,62 @@ let roles_union rs1 rs2 =
   let error r = ET.ERoleClash r in
   list_union error compare_roles rs1 rs2
 
+let exists_role_deleted v r =
+  let o = v, [] in
+  let compare r = compare_objs o (obj_of_role r) in
+  list_exists compare r
+
+let rec get_tops v = function
+  | []        -> [], []
+  | (_,r)::tl ->
+    let ds, ts = get_tops v tl in
+    if compare_versions v r.ET.v = 0 then begin
+      if r.ET.n = [] then objs_union r.ET.o ds, ts else
+      let tops = rev_objs_of_names v [] r.ET.n in
+      ds, objs_union (List.rev tops) ts
+    end else
+      ds, ts
+
+let rec match_names oi ni os ns =
+  match os, ns with
+  | _         , []        -> None
+  | []        , _         -> None
+  | (_,o)::otl,(_,n)::ntl ->
+    let b = compare_names (snd o) n in
+    if b > 0 then match_names oi (succ ni) os ntl else
+    if b < 0 then match_names (succ oi) ni otl ns else
+    Some (oi, ni)
+
 let new_status = {
   ET.r = []; ET.s = []; ET.t = []; ET.w = [];
 }
 
+let string_of_pointer = string_of_version 
+
 let pointer_of_string = version_of_string
 
+let list_visit before each after string_of p l =
+  let ptr p = string_of_pointer (List.rev p) in
+  let rec aux i = function
+    | []         -> ()
+    | (b, x)::tl ->
+      each (ptr (i::p)) b (string_of x);
+      aux (succ i) tl
+  in
+  let s, c = list_count 0 0 l in
+  let count = Printf.sprintf "%u/%u" s c in
+  before (ptr p) count;
+  aux 0 l;
+  after ()
+
 let string_of_error = function
-  | ET.EExt x        ->
+  | ET.EWrongExt x   ->
     Printf.sprintf "unknown input file type %S" x
   | ET.EStage v      ->
     Printf.sprintf "current stage %S" (string_of_version v)
   | ET.ENoStage      ->
     Printf.sprintf "current stage not defined"
-  | ET.ENews         ->
+  | ET.EWaiting      ->
     Printf.sprintf "current stage not finished"
   | ET.ENameClash n  ->
     Printf.sprintf "name clash %S" (string_of_name n)
@@ -149,3 +206,5 @@ let string_of_error = function
     Printf.sprintf "selected role is not unique"
   | ET.EWrongVersion ->
     Printf.sprintf "selected role is not in the current stage"
+  | ET.ETops         ->
+    Printf.sprintf "top objects already computed"