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.
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_______________________________________________________________ *)
12 module ET = RolesTypes
17 let rec list_map_filter map l = function
20 begin match map hd with
21 | None -> list_map_filter map l tl
22 | Some x -> list_map_filter map (x :: l) tl
25 let list_union error compare l1 l2 =
26 let rec aux l1 l2 = match l1 with
28 | hd1::tl1 -> match l2 with
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)
38 let list_compare compare l1 l2 =
39 let rec aux l1 l2 = match l1 with
41 if l2 = [] then 0 else -1
42 | hd1::tl1 -> match l2 with
45 let b = compare hd1 hd2 in
46 if b = 0 then aux tl1 tl2 else b
50 let rec list_apply prop map n = function
53 if prop n hd then begin map hd; true end
54 else list_apply prop map (succ n) tl
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
60 let list_split prop map l =
61 let lt, lf = List.partition prop l in
62 List.iter map lt; lf, lt
64 let rec list_count p s c = function
66 | x :: tl -> list_count p (s + if p x then 1 else 0) (succ c) tl
70 let string_of_stage v =
71 String.concat "." (List.map string_of_int v)
73 let stage_of_string s =
74 list_map_filter int_of_string_opt [] (String.split_on_char '.' s)
76 let stage_compare v1 v2 =
77 list_compare compare v1 v2
81 let string_of_name n =
84 let name_of_string s =
85 String.split_on_char '_' s
87 let name_compare n1 n2 =
88 list_compare compare n1 n2
92 let string_of_nobj n =
93 string_of_name n.ET.nn
95 let nobj_of_string s = {
96 ET.nb = false; ET.nn = name_of_string s;
99 let key_of_nobj n = string_of_nobj n
101 let nobj_selected n = n.ET.nb
104 n.ET.nb <- not n.ET.nb
106 let nobj_compare n1 n2 =
107 name_compare n1.ET.nn n2.ET.nn
109 let nobj_union ns1 ns2 =
110 let error n = ET.ENClash n in
111 list_union error nobj_compare ns1 ns2
115 let string_of_oobj o =
116 Printf.sprintf "%s/%s" (string_of_stage o.ET.os) (string_of_name o.ET.on)
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"
123 let key_of_oobj o = string_of_name o.ET.on
125 let oobj_selected o = o.ET.ob
128 o.ET.ob <- not o.ET.ob
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
134 let oobj_union os1 os2 =
135 let error o = ET.EOClash o in
136 list_union error oobj_compare os1 os2
138 let oobj_of_nobj v n =
139 {ET.ob = n.ET.nb; ET.os = v; ET.on = n.ET.nn}
141 let rec oobj_match oi ni os ns =
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
154 let n = match r.ET.rn with
158 {ET.ob = r.ET.rb; ET.os = r.ET.rs; ET.on = n}
160 let string_of_robj r =
161 string_of_oobj (oobj_of_robj r)
163 let key_of_robj r = key_of_oobj (oobj_of_robj r)
165 let robj_selected r = r.ET.rb
168 r.ET.rb <- not r.ET.rb
171 r.ET.rx <- not r.ET.rx
173 let robj_compare r1 r2 =
174 oobj_compare (oobj_of_robj r1) (oobj_of_robj r2)
176 let robj_union rs1 rs2 =
177 let error r = ET.ERClash r in
178 list_union error robj_compare rs1 rs2
180 let rec robj_tops v = function
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
191 let robj_split s rs =
192 let rec aux rs os ns = function
193 | [] -> List.rev rs, os, ns
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
209 ET.sm = false; ET.sr = []; ET.ss = []; ET.so = []; ET.sn = [];
214 let string_of_pointer p =
216 | ET.One i -> string_of_int i
217 | ET.Many is -> String.concat "," (List.map string_of_int is)
219 String.concat "." (List.map map p)
221 let pointer_of_string s =
223 match list_map_filter int_of_string_opt [] (String.split_on_char ',' s) with
225 | [i] -> Some (ET.One i)
226 | is -> Some (ET.Many is)
228 list_map_filter map [] (String.split_on_char '.' s)
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
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
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);
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;
255 let string_of_error = function
257 Printf.sprintf "unknown input file type %S" x
259 Printf.sprintf "current stage %S" (string_of_stage v)
261 Printf.sprintf "current stage not defined"
263 Printf.sprintf "current stage not finished"
265 Printf.sprintf "name clash %S" (string_of_nobj n)
267 Printf.sprintf "object clash %S" (string_of_oobj o)
269 Printf.sprintf "role clash %S" (string_of_robj r)
271 Printf.sprintf "entry not found"
273 Printf.sprintf "selected role is not unique"
274 | ET.EWrongVersion ->
275 Printf.sprintf "selected role is not in the current stage"
277 Printf.sprintf "top objects already computed"
278 | ET.EWrongRequest (r,a) ->
279 Printf.sprintf "unknown request \"%s=%s\"" r a