Source

ocaml-lib / term.old.ml

Full commit
(*
   Useful code for representation and managing of terms.
   To be used by logic modules 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 def : Syntax.t_list;  (* definition of the term *)
    mutable sub : string LSet.t;  (* names of terms used in def *)
    mutable sup : string LSet.t;  (* names of terms using the term *)
  }

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

(* Invariants
   - every term that has been used once must be in tbl (even if undefined)
*)

(* get data about a term *)
let get : string -> t =
  fun name ->
    try Hashtbl.find tbl name
    with Not_found ->
      let data = {version = 0; def = [BackSlash; Term name]; sub = []; sup = []} in
      Hashtbl.add tbl name data; data

(* add a sup-term *)
let add_sup : string -> string -> unit =
  fun name sup ->
    let data = get name in
    data.sup <- sup::data.sup

(* delete a sup-term *)
let del_sup : string -> string -> unit =
  fun name sup ->
    let data = get name in
    data.sup <- List.filter ((<>) sup) data.sup

(* get all names depending on a given name *)
let rec all_dep : string -> string LSet.t =
  fun name ->
    let data = get name in
    List.fold_left (fun res sup -> LSet.union res (all_dep sup)) [name] data.sup

(* test occurence of name in def of an other term *)
let rec occur : string -> string -> bool =
  fun name in_name -> in_name = name or
    List.exists (occur name) (get in_name).sub

(* corrects the new definition of a term *)

exception Cycle  (* raised when a cycle is detected in a definition *)

let rec define_pp : string -> Syntax.t_list -> string list -> Syntax.t_list -> Syntax.t_list * string LSet.t =
  fun name def0 sub0 -> function
      [] -> [], []
    | Term t::tokens ->
	if t = name
	then let def1, sub1 = define_pp name def0 sub0 tokens in def0 @ def1, LSet.union sub0 sub1
	else if occur name t
	then raise Cycle
	else let def1, sub1 = define_pp name def0 sub0 tokens in Term t::def1, LSet.union sub1 [t]
    | token::tokens -> let def1, sub1 = define_pp name def0 sub0 tokens in token::def1, sub1

(* define or re-define a term *)
let define : string -> Syntax.t_list -> unit =
  fun name def ->
   let data = get name in
   let def1, sub1 = define_pp name data.def data.sub def in
   if def1 <> data.def then data.version <- data.version + 1;
   data.def <- def1;
   List.iter (fun n -> del_sup n name) data.sub;
   data.sub <- sub1;
   List.iter (fun n -> add_sup n name) data.sub

(* parse a term *)
let rec parse_term : (string -> int -> Syntax.t_stream -> 'a) -> (Syntax.t_stream -> 'a) -> Syntax.t_stream -> 'a =
  fun p_def p_undef -> parser
      [<'LeftPar; x = parse_term p; 'RightPar>] -> x
    | [<'Term name; s>] ->
	let data = get name in
	p name data.version [<'LeftPar; Stream.of_list data.def; 'RightPar; s>]

(* parse an atom *)
let parse_atom : Syntax.t_stream -> string = parser
    [<'BackSlash; 'Term name>] -> name

(* print a term *)
let print_term : string -> int -> Syntax.t_list -> Syntax.t_list =
  fun name version l_old ->
    let data = get name in
    if data.version = version
    then [Term name]
    else l_old

(* print an atom *)
let print_atom : string -> Syntax.t_list =
  fun name -> [BackSlash; Term name]