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