matita/matita/virtuals.ml

   1 type symbol = Glib.unichar
   2 type tag = string
   3
   4 let virtual_to_symbol = Hashtbl.create 503;;
   5 let tag_to_data = Hashtbl.create 503;;
   6
   7 let add_virtual names symbol tags =
   8   List.iter
   9     (fun name ->
  10        if Hashtbl.mem virtual_to_symbol name then
  11          HLog.error
  12           (Printf.sprintf "name %s already used for virtual %s" name
  13           (Glib.Utf8.from_unichar (Hashtbl.find virtual_to_symbol name)))
  14        else
  15          Hashtbl.add virtual_to_symbol name symbol)
  16        names;
  17   List.iter
  18     (fun tag ->
  19        try
  20         let l = Hashtbl.find tag_to_data tag in
  21         let l = (names,symbol) :: l in
  22         Hashtbl.replace tag_to_data tag l
  23        with Not_found ->
  24         Hashtbl.add tag_to_data tag [names,symbol])
  25     tags;
  26 ;;
  27
  28 let get_all_virtuals () =
  29   let l = ref [] in
  30   Hashtbl.iter
  31     (fun k v -> l := (k,v) :: !l;)
  32     tag_to_data;
  33   !l
  34 ;;
  35
  36 exception Not_a_virtual
  37
  38 let rec symbol_of_virtual str =
  39   if str = "" then raise Not_a_virtual
  40   else
  41     try str, Hashtbl.find virtual_to_symbol str
  42     with Not_found ->
  43      symbol_of_virtual (String.sub str 1 (String.length str - 1))
  44 ;;
  45
  46 let classes = Hashtbl.create 503;;
  47
  48 let add_eqclass l =
  49   List.iter (fun x ->
  50     assert(not (Hashtbl.mem classes x));
  51     Hashtbl.add classes x l) l
  52 ;;
  53
  54 let similar_symbols symbol =
  55   try Hashtbl.find classes symbol
  56   with Not_found -> []
  57 ;;
  58
  59 let get_all_eqclass () =
  60   let rc = ref [] in
  61   Hashtbl.iter
  62     (fun k v ->
  63       if not (List.mem v !rc) then
  64         rc := v :: !rc)
  65     classes;
  66   !rc
  67 ;;
  68