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 string_of_version v =
  55   String.concat "." (List.map string_of_int v)
  56
  57 let version_of_string s =
  58   List.map int_of_string (String.split_on_char '.' s)
  59
  60 let string_of_name n =
  61   String.concat "_" n
  62
  63 let name_of_string s =
  64   String.split_on_char '_' s
  65
  66 let compare_names n1 n2 =
  67   list_compare compare n1 n2
  68
  69 let string_of_obj (v,n) =
  70   Printf.sprintf "%s/%s" (string_of_version v) (string_of_name n)
  71
  72 let obj_of_string s =
  73   match String.split_on_char '/' s with
  74   | [sv;sn] -> version_of_string sv, name_of_string sn
  75   | _       -> failwith "obj_of_string"
  76
  77 let new_status = {
  78   ET.r = []; ET.s = []; ET.t = []; ET.w = [];
  79 }
  80
  81 let pointer_of_string = version_of_string
  82
  83 let string_of_error = function
  84   | ET.EExt x       ->
  85     Printf.sprintf "unknown input file type %S" x
  86   | ET.EStage v     ->
  87     Printf.sprintf "current stage %S" (string_of_version v)
  88   | ET.ENoStage     ->
  89     Printf.sprintf "current stage not defined"
  90   | ET.ENews        ->
  91     Printf.sprintf "current stage not finished"
  92   | ET.ENameClash n ->
  93     Printf.sprintf "name clash %S" (string_of_name n)
  94   | ET.ENoEntry     ->
  95     Printf.sprintf "entry not found"