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_toggle n = function
  47   | []         -> raise_error ET.ENoEntry
  48   | (b,hd)::tl -> if n = 0 then (not b,hd)::tl else (b,hd)::list_toggle (pred n) tl
  49
  50 let rec list_toggle_all = function
  51   | []         -> []
  52   | (b,hd)::tl -> (not b,hd)::list_toggle_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_select r = function
  62   | []         -> r
  63   | (b,hd)::tl ->
  64     begin match b, r with
  65     | false, _      -> list_select r tl
  66     | true , None   -> list_select (Some hd) tl
  67     | true , Some _ -> raise_error (ET.EWrongSelect)
  68     end
  69
  70 let string_of_version v =
  71   String.concat "." (List.map string_of_int v)
  72
  73 let version_of_string s =
  74   List.map int_of_string (String.split_on_char '.' s)
  75
  76 let compare_versions v1 v2 =
  77   list_compare compare v1 v2
  78
  79 let string_of_name n =
  80   String.concat "_" n
  81
  82 let name_of_string s =
  83   String.split_on_char '_' s
  84
  85 let compare_names n1 n2 =
  86   list_compare compare n1 n2
  87
  88 let names_union ns1 ns2 =
  89   let error n = ET.ENameClash n in
  90   list_union error compare_names ns1 ns2
  91
  92 let string_of_obj (v,n) =
  93   Printf.sprintf "%s/%s" (string_of_version v) (string_of_name n)
  94
  95 let obj_of_string s =
  96   match String.split_on_char '/' s with
  97   | [sv;sn] -> version_of_string sv, name_of_string sn
  98   | _       -> failwith "obj_of_string"
  99
 100 let compare_objs (v1,n1) (v2,n2) =
 101   let b = compare_versions v1 v2 in
 102   if b = 0 then compare_names n1 n2 else b
 103
 104 let objs_union os1 os2 =
 105   let error o = ET.EObjClash o in
 106   list_union error compare_objs os1 os2
 107
 108 let obj_of_role r =
 109   let n = match r.ET.n with
 110     | []        -> []
 111     | (_,n):: _ -> n
 112   in
 113   r.ET.v, n
 114
 115 let string_of_role r =
 116   string_of_obj (obj_of_role r)
 117
 118 let compare_roles r1 r2 =
 119   compare_objs (obj_of_role r1) (obj_of_role r2)
 120
 121 let roles_union rs1 rs2 =
 122   let error r = ET.ERoleClash r in
 123   list_union error compare_roles rs1 rs2
 124
 125 let new_status = {
 126   ET.r = []; ET.s = []; ET.t = []; ET.w = [];
 127 }
 128
 129 let pointer_of_string = version_of_string
 130
 131 let string_of_error = function
 132   | ET.EExt x        ->
 133     Printf.sprintf "unknown input file type %S" x
 134   | ET.EStage v      ->
 135     Printf.sprintf "current stage %S" (string_of_version v)
 136   | ET.ENoStage      ->
 137     Printf.sprintf "current stage not defined"
 138   | ET.ENews         ->
 139     Printf.sprintf "current stage not finished"
 140   | ET.ENameClash n  ->
 141     Printf.sprintf "name clash %S" (string_of_name n)
 142   | ET.EObjClash o   ->
 143     Printf.sprintf "object clash %S" (string_of_obj o)
 144   | ET.ERoleClash r  ->
 145     Printf.sprintf "role clash %S" (string_of_role r)
 146   | ET.ENoEntry      ->
 147     Printf.sprintf "entry not found"
 148   | ET.EWrongSelect  ->
 149     Printf.sprintf "selected role is not unique"
 150   | ET.EWrongVersion ->
 151     Printf.sprintf "selected role is not in the current stage"