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 hd1 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 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_apply prop map n = function
  43   | []       -> false
  44   | hd :: tl ->
  45     if prop n hd then begin map hd; true end
  46     else list_apply prop map (succ n) tl
  47
  48 let list_nth map n l =
  49   let prop m _ = m = n in
  50   if list_apply prop map 0 l then () else raise_error ET.ENoEntry
  51
  52 let list_split prop map l =
  53   let lt, lf = List.partition prop l in
  54   List.iter map lt; lf, lt
  55
  56 let rec list_count p s c = function
  57   | []      -> s, c
  58   | x :: tl -> list_count p (s + if p x then 1 else 0) (succ c) tl
  59
  60 (* stage *)
  61
  62 let string_of_stage v =
  63   String.concat "." (List.map string_of_int v)
  64
  65 let stage_of_string s =
  66   List.map int_of_string (String.split_on_char '.' s)
  67
  68 let stage_compare v1 v2 =
  69   list_compare compare v1 v2
  70
  71 (* name *)
  72
  73 let string_of_name n =
  74   String.concat "_" n
  75
  76 let name_of_string s =
  77   String.split_on_char '_' s
  78
  79 let name_compare n1 n2 =
  80   list_compare compare n1 n2
  81
  82 (* nobj *)
  83
  84 let string_of_nobj n =
  85   string_of_name n.ET.nn
  86
  87 let nobj_of_string s = {
  88   ET.nb = false; ET.nn = name_of_string s;
  89 }
  90
  91 let key_of_nobj n = string_of_nobj n
  92
  93 let nobj_selected n = n.ET.nb
  94
  95 let nobj_select n =
  96   n.ET.nb <- not n.ET.nb
  97
  98 let nobj_compare n1 n2 =
  99   name_compare n1.ET.nn n2.ET.nn
 100
 101 let nobj_union ns1 ns2 =
 102   let error n = ET.ENClash n in
 103   list_union error nobj_compare ns1 ns2
 104
 105 (* oobj *)
 106
 107 let string_of_oobj o =
 108   Printf.sprintf "%s/%s" (string_of_stage o.ET.os) (string_of_name o.ET.on)
 109
 110 let oobj_of_string s =
 111   match String.split_on_char '/' s with
 112   | [ss;sn] -> {ET.ob = false; ET.os = stage_of_string ss; ET.on = name_of_string sn}
 113   | _       -> failwith "oobj_of_string"
 114
 115 let key_of_oobj o = string_of_name o.ET.on
 116
 117 let oobj_selected o = o.ET.ob
 118
 119 let oobj_select o =
 120   o.ET.ob <- not o.ET.ob
 121
 122 let oobj_compare o1 o2 =
 123   let b = stage_compare o1.ET.os o2.ET.os in
 124   if b = 0 then name_compare o1.ET.on o2.ET.on else b
 125
 126 let oobj_union os1 os2 =
 127   let error o = ET.EOClash o in
 128   list_union error oobj_compare os1 os2
 129
 130 let oobj_of_nobj v n =
 131   {ET.ob = n.ET.nb; ET.os = v; ET.on = n.ET.nn}
 132
 133 let rec oobj_match oi ni os ns =
 134   match os, ns with
 135   | _       , []       -> None
 136   | []      , _        -> None
 137   | o :: otl, n :: ntl ->
 138     let b = name_compare o.ET.on n.ET.nn in
 139     if b > 0 then oobj_match oi (succ ni) os ntl else
 140     if b < 0 then oobj_match (succ oi) ni otl ns else
 141     Some (oi, ni)
 142
 143 (* robj *)
 144
 145 let oobj_of_robj r =
 146   let n = match r.ET.rn with
 147     | []     -> []
 148     | n :: _ -> n.ET.nn
 149   in
 150   {ET.ob = r.ET.rb; ET.os = r.ET.rs; ET.on = n}
 151
 152 let string_of_robj r =
 153   string_of_oobj (oobj_of_robj r)
 154
 155 let key_of_robj r = key_of_oobj (oobj_of_robj r)
 156
 157 let robj_selected r = r.ET.rb
 158
 159 let robj_select r =
 160   r.ET.rb <- not r.ET.rb
 161
 162 let robj_expand r =
 163   r.ET.rx <- not r.ET.rx
 164
 165 let robj_compare r1 r2 =
 166   oobj_compare (oobj_of_robj r1) (oobj_of_robj r2)
 167
 168 let robj_union rs1 rs2 =
 169   let error r = ET.ERClash r in
 170   list_union error robj_compare rs1 rs2
 171
 172 let rec robj_tops v = function
 173   | []      -> [], []
 174   | r :: tl ->
 175     let ds, ts = robj_tops v tl in
 176     if stage_compare v r.ET.rs = 0 then begin
 177       if r.ET.rn = [] then oobj_union r.ET.ro ds, ts else
 178       let tops = List.rev_map (oobj_of_nobj v) r.ET.rn in
 179       ds, oobj_union (List.rev tops) ts
 180     end else
 181       ds, ts
 182
 183 let robj_split s rs =
 184   let rec aux rs os ns = function
 185   | []      -> List.rev rs, os, ns
 186   | r :: tl ->
 187     if stage_compare s r.ET.rs <> 0 then aux (r :: rs) os ns tl else
 188     if r.ET.rb then aux rs (oobj_union os r.ET.ro) (nobj_union ns r.ET.rn) tl else
 189     let ro, so = list_split oobj_selected oobj_select r.ET.ro in
 190     let rn, sn = list_split nobj_selected nobj_select r.ET.rn in
 191     if ro = [] && rn = [] then aux rs (oobj_union os so) (nobj_union ns sn) tl else begin
 192       r.ET.ro <- ro; r.ET.rn <- rn;
 193       aux (r :: rs) (oobj_union os so) (nobj_union ns sn) tl
 194     end
 195   in
 196   aux [] [] [] rs
 197
 198 (* status *)
 199
 200 let new_status = {
 201   ET.sm = false; ET.sr = []; ET.ss = []; ET.so = []; ET.sn = [];
 202 }
 203
 204 (* pointer *)
 205
 206 let string_of_pointer = string_of_stage
 207
 208 let pointer_of_string = stage_of_string
 209
 210 let list_visit before each visit after selected key_of string_of p l =
 211   let ptr p = string_of_pointer (List.rev p) in
 212   let rec aux i = function
 213     | []      -> ()
 214     | x :: tl ->
 215       each (ptr p) (ptr (i::p)) (selected x) (key_of x) (string_of x);
 216       visit (i::p) x;
 217       aux (succ i) tl
 218   in
 219   let s, c = list_count selected 0 0 l in
 220   let count = Printf.sprintf "%u/%u" s c in
 221   before (ptr p) count;
 222   aux 0 l;
 223   after ()
 224
 225 (* error *)
 226
 227 let string_of_error = function
 228   | ET.EWrongExt x         ->
 229     Printf.sprintf "unknown input file type %S" x
 230   | ET.EStage v            ->
 231     Printf.sprintf "current stage %S" (string_of_stage v)
 232   | ET.ENoStage            ->
 233     Printf.sprintf "current stage not defined"
 234   | ET.EWaiting            ->
 235     Printf.sprintf "current stage not finished"
 236   | ET.ENClash n           ->
 237     Printf.sprintf "name clash %S" (string_of_nobj n)
 238   | ET.EOClash o           ->
 239     Printf.sprintf "object clash %S" (string_of_oobj o)
 240   | ET.ERClash r           ->
 241     Printf.sprintf "role clash %S" (string_of_robj r)
 242   | ET.ENoEntry            ->
 243     Printf.sprintf "entry not found"
 244   | ET.EWrongSelect        ->
 245     Printf.sprintf "selected role is not unique"
 246   | ET.EWrongVersion       ->
 247     Printf.sprintf "selected role is not in the current stage"
 248   | ET.ETops               ->
 249     Printf.sprintf "top objects already computed"
 250   | ET.EWrongRequest (r,a) ->
 251     Printf.sprintf "unknown request \"%s=%s\"" r a