matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module ET = RolesTypes
  13
  14 let raise_error e =
  15   raise (ET.Error e)
  16
  17 let list_union error compare l1 l2 =
  18   let rec aux l1 l2 = match l1 with
  19   | []       -> l2
  20   | hd1::tl1 -> match l2 with
  21   | []       -> l1
  22   | hd2::tl2 ->
  23     let b = compare (snd hd1) (snd hd2) in
  24     if b > 0 then hd2 :: aux l1 tl2
  25     else if b < 0 then hd1 :: aux tl1 l2
  26     else raise_error (error (snd hd1))
  27   in
  28   aux l1 l2
  29
  30 let list_compare compare l1 l2 =
  31   let rec aux l1 l2 = match l1 with
  32   | []       ->
  33     if l2 = [] then 0 else -1
  34   | hd1::tl1 -> match l2 with
  35   | []       -> 1
  36   | hd2::tl2 ->
  37     let b = compare hd1 hd2 in
  38     if b = 0 then aux tl1 tl2 else b
  39   in
  40   aux l1 l2
  41
  42 let rec list_nth n = function
  43   | []         -> raise_error ET.ENoEntry
  44   | (_,hd)::tl -> if n = 0 then hd else list_nth (pred n) tl
  45
  46 let rec list_select n = function
  47   | []         -> raise_error ET.ENoEntry
  48   | (b,hd)::tl -> if n = 0 then (not b,hd)::tl else (b,hd)::list_select (pred n) tl
  49
  50 let rec list_select_all = function
  51   | []         -> []
  52   | (b,hd)::tl -> (not b,hd)::list_select_all tl
  53
  54 let rec list_split = function
  55   | []                -> [], []
  56   | (b,a) as hd :: tl ->
  57     let fs,ts = list_split tl in
  58     if fst hd then fs,((false,a)::ts)
  59     else (hd::fs),ts
  60
  61 let rec list_find_selected r = function
  62   | []         -> r
  63   | (b,hd)::tl ->
  64     begin match b, r with
  65     | false, _      -> list_find_selected r tl
  66     | true , None   -> list_find_selected (Some hd) tl
  67     | true , Some _ -> raise_error (ET.EWrongSelect)
  68     end
  69
  70 let rec list_exists compare = function
  71   | []        -> false
  72   | (_,a)::tl ->
  73     let b = compare a in
  74     if b <= 0 then b = 0 else
  75     list_exists compare tl
  76
  77 let rec list_count s c = function
  78   | []         -> s, c
  79   | (b, _)::tl -> list_count (s + if b then 1 else 0) (succ c) tl
  80
  81 let string_of_version v =
  82   String.concat "." (List.map string_of_int v)
  83
  84 let version_of_string s =
  85   List.map int_of_string (String.split_on_char '.' s)
  86
  87 let compare_versions v1 v2 =
  88   list_compare compare v1 v2
  89
  90 let string_of_name n =
  91   String.concat "_" n
  92
  93 let name_of_string s =
  94   String.split_on_char '_' s
  95
  96 let compare_names n1 n2 =
  97   list_compare compare n1 n2
  98
  99 let names_union ns1 ns2 =
 100   let error n = ET.ENameClash n in
 101   list_union error compare_names ns1 ns2
 102
 103 let rec match_names oi ni os ns =
 104   match os, ns with
 105   | _         , []        -> None
 106   | []        , _         -> None
 107   | (_,o)::otl,(_,n)::ntl ->
 108     let b = compare_names (snd o) n in
 109     if b > 0 then match_names oi (succ ni) os ntl else
 110     if b < 0 then match_names (succ oi) ni otl ns else
 111     Some (oi, ni)
 112
 113 let string_of_obj (v,n) =
 114   Printf.sprintf "%s/%s" (string_of_version v) (string_of_name n)
 115
 116 let obj_of_string s =
 117   match String.split_on_char '/' s with
 118   | [sv;sn] -> version_of_string sv, name_of_string sn
 119   | _       -> failwith "obj_of_string"
 120
 121 let compare_objs (v1,n1) (v2,n2) =
 122   let b = compare_versions v1 v2 in
 123   if b = 0 then compare_names n1 n2 else b
 124
 125 let objs_union os1 os2 =
 126   let error o = ET.EObjClash o in
 127   list_union error compare_objs os1 os2
 128
 129 let rec rev_objs_of_names v os = function
 130   | []        -> os
 131   | (b,n)::tl -> rev_objs_of_names v ((b,(v,n))::os) tl
 132
 133 let rec get_tops v = function
 134   | []        -> [], []
 135   | (_,r)::tl ->
 136     let ds, ts = get_tops v tl in
 137     if compare_versions v r.ET.v = 0 then begin
 138       if r.ET.n = [] then objs_union r.ET.o ds, ts else
 139       let tops = rev_objs_of_names v [] r.ET.n in
 140       ds, objs_union (List.rev tops) ts
 141     end else
 142       ds, ts
 143
 144 let obj_of_role r =
 145   let n = match r.ET.n with
 146     | []        -> []
 147     | (_,n):: _ -> n
 148   in
 149   r.ET.v, n
 150
 151 let string_of_role r =
 152   string_of_obj (obj_of_role r)
 153
 154 let compare_roles r1 r2 =
 155   compare_objs (obj_of_role r1) (obj_of_role r2)
 156
 157 let roles_union rs1 rs2 =
 158   let error r = ET.ERoleClash r in
 159   list_union error compare_roles rs1 rs2
 160
 161 let roles_expand_all rs =
 162   let map (b, r) = r.ET.x <- not r.ET.x in
 163   List.iter map rs
 164
 165 let rec roles_expand n = function
 166   | []        -> ()
 167   | (_,r)::tl ->
 168     if n = 0 then r.ET.x <- not r.ET.x else
 169     roles_expand (pred n) tl
 170
 171 let exists_role_deleted v r =
 172   let o = v, [] in
 173   let compare r = compare_objs o (obj_of_role r) in
 174   list_exists compare r
 175
 176 let roles_split s rs =
 177   let rec aux rs os ns = function
 178   | []           -> List.rev rs, os, ns
 179   | (b, r) :: tl ->
 180     if compare_versions s r.ET.v <> 0 then aux ((b, r)::rs) os ns tl else
 181     if b then aux rs (objs_union os r.ET.o) (names_union ns r.ET.n) tl else
 182     let ro, so = list_split r.ET.o in
 183     let rn, sn = list_split r.ET.n in
 184     if ro = [] && rn = [] then aux rs (objs_union os so) (names_union ns sn) tl else begin
 185       r.ET.o <- ro; r.ET.o <- ro;
 186       aux ((b, r)::rs) (objs_union os so) (names_union ns sn) tl
 187     end
 188   in
 189   aux [] [] [] rs
 190
 191 let new_status = {
 192   ET.m = false; ET.r = []; ET.s = []; ET.t = []; ET.w = [];
 193 }
 194
 195 let string_of_pointer = string_of_version
 196
 197 let pointer_of_string = version_of_string
 198
 199 let list_visit before each visit after string_of p l =
 200   let ptr p = string_of_pointer (List.rev p) in
 201   let rec aux i = function
 202     | []         -> ()
 203     | (b, x)::tl ->
 204       each (ptr (i::p)) b (string_of x);
 205       visit (i::p) x;
 206       aux (succ i) tl
 207   in
 208   let s, c = list_count 0 0 l in
 209   let count = Printf.sprintf "%u/%u" s c in
 210   before (ptr p) count;
 211   aux 0 l;
 212   after ()
 213
 214 let string_of_error = function
 215   | ET.EWrongExt x         ->
 216     Printf.sprintf "unknown input file type %S" x
 217   | ET.EStage v            ->
 218     Printf.sprintf "current stage %S" (string_of_version v)
 219   | ET.ENoStage            ->
 220     Printf.sprintf "current stage not defined"
 221   | ET.EWaiting            ->
 222     Printf.sprintf "current stage not finished"
 223   | ET.ENameClash n        ->
 224     Printf.sprintf "name clash %S" (string_of_name n)
 225   | ET.EObjClash o         ->
 226     Printf.sprintf "object clash %S" (string_of_obj o)
 227   | ET.ERoleClash r        ->
 228     Printf.sprintf "role clash %S" (string_of_role r)
 229   | ET.ENoEntry            ->
 230     Printf.sprintf "entry not found"
 231   | ET.EWrongSelect        ->
 232     Printf.sprintf "selected role is not unique"
 233   | ET.EWrongVersion       ->
 234     Printf.sprintf "selected role is not in the current stage"
 235   | ET.ETops               ->
 236     Printf.sprintf "top objects already computed"
 237   | ET.EWrongRequest (r,a) ->
 238     Printf.sprintf "unknown request \"%s=%s\"" r a