Source

ocaml-lib / term.ml

(*
   Useful code for representation and managing of terms.
   To be used by logic modules, Node and Context.
*)

open Token

(* type of data associated to a term *)
type t = {
    mutable version : int;  (* version number of the definition of the term *)
    mutable sufs : Syntax.t_list list;  (* list of sufficient conditions *)
    mutable necs : Syntax.t_list list;  (* list of necessary conditions *)
(*    mutable sub : string list;  (* names of terms used in sufs and necs *) *)
    mutable dep : string list;  (* names of terms using the term *)
  }

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

(* load and save *)

let init () =
  Hashtbl.clear !tbl

let load ch =
  tbl := (input_value ch : (string,t) Hashtbl.t)

let save ch =
  output_value ch (!tbl : (string,t) Hashtbl.t)

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

(* get data about a term *)
let get : string -> t =
  fun name ->
    try Hashtbl.find !tbl name
    with Not_found ->
      let data = {version = 0; sufs = []; necs = []; dep = []} in
      Hashtbl.add !tbl name data; data

let get_sufs : string -> Syntax.t_list list =
  fun name -> (get name).sufs

let get_necs : string -> Syntax.t_list list =
  fun name -> (get name).necs


(* add a dep-term *)
let add_dep : string -> string -> unit =
  fun name dep ->
    let data = get name in
    if not (List.mem dep data.dep) then data.dep <- dep::data.dep

(* get all names depending on a given name *)
let rec all_dep : string -> string list =
  fun name -> all_dep2 name []
and all_dep2 : string -> string list -> string list =
  fun name deps ->
    if List.mem name deps
    then deps
    else
      let data = get name in
      List.fold_left (fun res dep -> all_dep2 dep res) (name::deps) data.dep

(* add a sufficient condition *)
let add_suf : string -> Syntax.t_list -> unit =
  fun name suf ->
    let data = get name in
    let sub_names = Syntax.get_terms suf in
    data.sufs <- suf::data.sufs;
    List.iter (fun sub -> add_dep sub name) sub_names

(* add a necessary condition *)
let add_nec : string -> Syntax.t_list -> unit =
  fun name nec ->
    let data = get name in
    let sub_names = Syntax.get_terms nec in
    data.necs <- nec::data.necs;
    List.iter (fun sub -> add_dep sub name) sub_names