Source

ocaml-lib / term.ml


(* useful code for representing idents and terms as integers *)
(* --------------------------------------------------------- *)

let cpt : int ref = ref 0

type id = int (* >0 for terms, <0 for idents *)

let h_s2id : (string,id) Hashtbl.t = Hashtbl.create 100
    
let h_id2s : (id,string) Hashtbl.t = Hashtbl.create 100

let exists s = Hashtbl.mem h_s2id s

let s2id s =
  try Hashtbl.find h_s2id s
  with Not_found ->
    incr cpt;
    let id = !cpt in
    Hashtbl.add h_s2id s id;
    Hashtbl.add h_id2s id s;
    id

let id2s id = (* may raise Not_found *)
  Hashtbl.find h_id2s id


(** Utility code for the representation and managing of taxonomic relations over terms. *)

(* type of data associated to a term *)
type t = {
    mutable sufs : int LSet.t;  (* list of sufficient conditions *)
    mutable necs : int LSet.t  (* list of necessary conditions *)
  }

(* dictionary of terms *)
let tbl : (int,t) Hashtbl.t = Hashtbl.create 1000

(* Invariants
   - a term absent from tbl has all fields equal to []
*)

(* get data about a term *)
let get : int -> t =
  fun id ->
    try Hashtbl.find tbl id
    with Not_found ->
      let data = {sufs = LSet.empty (); necs = LSet.empty ()} in
      Hashtbl.add tbl id data;
      data

let get_sufs : int -> int list =
  fun id ->
    try (Hashtbl.find tbl id).sufs
    with Not_found ->  LSet.empty ()

let get_necs : int -> int list =
  fun id ->
    try (Hashtbl.find tbl id).necs
    with Not_found -> LSet.empty ()

(* add a necessary condition *)
let add : int -> int -> unit =
  fun id nec ->
    let data = get id in
    data.necs <- LSet.add nec data.necs;
    let data2 = get nec in
    data2.sufs <- LSet.add id data2.sufs

(* delete a necessary condition *)
let remove : int -> int -> unit =
  fun id nec ->
    (try
      let data = Hashtbl.find tbl id in
      data.necs <- LSet.remove nec data.necs
    with Not_found -> ());
    (try
      let data2 = Hashtbl.find tbl nec in
      data2.sufs <- LSet.remove id data2.sufs
    with Not_found -> ())

(* rename a term/ident *)
let rename : int -> string -> unit =
  fun id s ->
    assert (not (Hashtbl.mem h_s2id s));
    let old_s = Hashtbl.find h_id2s id in
    Hashtbl.remove h_s2id old_s;
    Hashtbl.add h_s2id s id;
    Hashtbl.replace h_id2s id s

(* load and save *)

type data = {
    cpt : int;
    id2s : (id * string) list;
    tbl : (int * t) list;
  }

let init () =
  cpt := 0;
  Hashtbl.clear h_id2s;
  Hashtbl.clear h_s2id;
  Hashtbl.clear tbl

let load (t : data) =
  init ();
  cpt := t.cpt;
  List.iter
    (fun (id,s) ->
      Hashtbl.add h_id2s id s;
      Hashtbl.add h_s2id s id)
    t.id2s;
  List.iter
    (fun (id,x) ->
      Hashtbl.add tbl id x)
    t.tbl

let save () =
  let t = {
    cpt = !cpt;
    id2s = Hashtbl.fold (fun id s l -> (id,s)::l) h_id2s [];
    tbl = Hashtbl.fold (fun id x l -> (id,x)::l) tbl [];
  } in
  (t : data)