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