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 e1631c1b96aab0f767158c8e6333403581cf8021..066d7b865e929faeb285a99dcc108df5c78a007a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
@@ -15,20 +15,20 @@ let raise_error e =
   raise (ET.Error e)
 
 let list_union error compare l1 l2 =
-  let rec aux l1 l2 = match l1 with 
+  let rec aux l1 l2 = match l1 with
   | []       -> l2
   | hd1::tl1 -> match l2 with
   | []       -> l1
   | hd2::tl2 ->
     let b = compare (snd hd1) (snd hd2) in
     if b > 0 then hd2 :: aux l1 tl2
-    else if b < 0 then hd1 :: aux tl1 l2 
+    else if b < 0 then hd1 :: aux tl1 l2
     else raise_error (error (snd hd1))
   in
   aux l1 l2
 
 let list_compare compare l1 l2 =
-  let rec aux l1 l2 = match l1 with 
+  let rec aux l1 l2 = match l1 with
   | []       ->
     if l2 = [] then 0 else -1
   | hd1::tl1 -> match l2 with
@@ -51,12 +51,31 @@ let rec list_toggle_all = function
   | []         -> []
   | (b,hd)::tl -> (not b,hd)::list_toggle_all tl
 
+let rec list_split = function
+  | []                -> [], []
+  | (b,a) as hd :: tl ->
+    let fs,ts = list_split tl in
+    if fst hd then fs,((false,a)::ts)
+    else (hd::fs),ts
+
+let rec list_select r = function
+  | []         -> r
+  | (b,hd)::tl ->
+    begin match b, r with
+    | false, _      -> list_select r tl
+    | true , None   -> list_select (Some hd) tl
+    | true , Some _ -> raise_error (ET.EWrongSelect)
+    end
+
 let string_of_version v =
   String.concat "." (List.map string_of_int v)
 
 let version_of_string s =
   List.map int_of_string (String.split_on_char '.' s)
 
+let compare_versions v1 v2 =
+  list_compare compare v1 v2
+
 let string_of_name n =
   String.concat "_" n
 
@@ -66,14 +85,43 @@ let name_of_string s =
 let compare_names n1 n2 =
   list_compare compare n1 n2
 
+let names_union ns1 ns2 =
+  let error n = ET.ENameClash n in
+  list_union error compare_names ns1 ns2
+
 let string_of_obj (v,n) =
-  Printf.sprintf "%s/%s" (string_of_version v) (string_of_name n) 
+  Printf.sprintf "%s/%s" (string_of_version v) (string_of_name n)
 
 let obj_of_string s =
   match String.split_on_char '/' s with
-  | [sv;sn] -> version_of_string sv, name_of_string sn 
+  | [sv;sn] -> version_of_string sv, name_of_string sn
   | _       -> failwith "obj_of_string"
 
+let compare_objs (v1,n1) (v2,n2) =
+  let b = compare_versions v1 v2 in
+  if b = 0 then compare_names n1 n2 else b
+
+let objs_union os1 os2 =
+  let error o = ET.EObjClash o in
+  list_union error compare_objs os1 os2
+
+let obj_of_role r =
+  let n = match r.ET.n with
+    | []        -> []
+    | (_,n):: _ -> n
+  in
+  r.ET.v, n
+
+let string_of_role r =
+  string_of_obj (obj_of_role r)
+
+let compare_roles r1 r2 =
+  compare_objs (obj_of_role r1) (obj_of_role r2)
+
+let roles_union rs1 rs2 =
+  let error r = ET.ERoleClash r in
+  list_union error compare_roles rs1 rs2
+
 let new_status = {
   ET.r = []; ET.s = []; ET.t = []; ET.w = [];
 }
@@ -81,15 +129,23 @@ let new_status = {
 let pointer_of_string = version_of_string
 
 let string_of_error = function
-  | ET.EExt x       ->
+  | ET.EExt x        ->
     Printf.sprintf "unknown input file type %S" x
-  | ET.EStage v     ->
+  | ET.EStage v      ->
     Printf.sprintf "current stage %S" (string_of_version v)
-  | ET.ENoStage     ->
+  | ET.ENoStage      ->
     Printf.sprintf "current stage not defined"
-  | ET.ENews        ->
+  | ET.ENews         ->
     Printf.sprintf "current stage not finished"
-  | ET.ENameClash n ->
+  | ET.ENameClash n  ->
     Printf.sprintf "name clash %S" (string_of_name n)
-  | ET.ENoEntry     ->
+  | ET.EObjClash o   ->
+    Printf.sprintf "object clash %S" (string_of_obj o)
+  | ET.ERoleClash r  ->
+    Printf.sprintf "role clash %S" (string_of_role r)
+  | ET.ENoEntry      ->
     Printf.sprintf "entry not found"
+  | ET.EWrongSelect  ->
+    Printf.sprintf "selected role is not unique"
+  | ET.EWrongVersion ->
+    Printf.sprintf "selected role is not in the current stage"