Commits

Sébastien Ferré  committed 5e81073

Initial revision

  • Participants
  • Parent commits 9f556cc

Comments (0)

Files changed (1)

+(*
+   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
+