Sébastien Ferré avatar Sébastien Ferré committed 320a2d3

Removed deprecated files (belonging to Camelis)

Comments (0)

Files changed (9)

lexer.mll

-{
-open Tokens
-
-let norm_string : string -> string =
-  fun s ->
-    let r = ref 0 in
-    let w = ref 0 in
-    let l = String.length s in
-    while !r < l do
-      let c = s.[!r] in
-      if c = '\\'
-      then begin
-	incr r;
-	match s.[!r] with
-	| 'n' -> s.[!w] <- '\n'
-	| 't' -> s.[!w] <- '\t'
-	| '0'..'9' as c' ->
-	    (try
-	      s.[!w] <- Char.chr (int_of_string (String.sub s !r 3));
-	      incr r;
-	      incr r;
-	    with _ ->
-	      s.[!w] <- c')
-	| c' -> s.[!w] <- c' end
-      else s.[!w] <- c;
-      incr r;
-      incr w
-    done;
-    String.sub s 0 !w;;
-
-} 
-
-let skip_char = [' ' '\t' '\n']
-let ident_char = ['A'-'Z' 'a'-'z' '0'-'9' '_']
-let digit = ['0'-'9']
-let special_char = ['~' '@' '#' '$' '%' '^' '&' '*' '-' '+' '=' '|' '\\' '/' '>' '<']
-
-rule token = parse
-| skip_char { token lexbuf }
-| "\\\n" { token lexbuf }
-| '`' { BackQuote }
-| '!' { Exclam }
-| '(' { LeftPar }
-| ')' { RightPar }
-| '{' { LeftAcc }
-| '}' { RightAcc }
-| '[' { LeftBra }
-| ']' { RightBra }
-| '?' { Interro }
-| ',' { Comma }
-| '.' { Dot }
-| ':' { Colon }
-| ';' { SemiColon }
-| '"' { DoubleQuote }
-| '\'' { Quote }
-| '0'
-    { Nat 0 }
-| '-' '0'
-    { MinusNat 0 }
-| ['1'-'9'] digit*
-    { Nat (int_of_string (Lexing.lexeme lexbuf)) }
-| '-' ['1'-'9'] digit*
-    { MinusNat (- (int_of_string (Lexing.lexeme lexbuf))) }
-| ['A'-'Z' 'a'-'z' '_'] ident_char *
-    { Symbol (Lexing.lexeme lexbuf) }
-| special_char +
-    { Symbol (Lexing.lexeme lexbuf) }
-| '`' _ '`'
-    { Char ((norm_string (Lexing.lexeme lexbuf)).[1]) }
-| '"' [^ '\\' '"']* ('\\' _ [^ '\\' '"']*)* '"'
-  { let s = Lexing.lexeme lexbuf in String (norm_string (String.sub s 1 (String.length s - 2))) }
-| '\'' [^ '\\' '\'']* ('\\' _ [^ '\\' '\'']*)* '\''
-  { let s = Lexing.lexeme lexbuf in Symbol (norm_string (String.sub s 1 (String.length s - 2))) }
-| eof { raise Eof }

logdag.ml

-
-(** The first input signature of the functor {!Logdag.Make} specifying various paramters. *)
-module type PARAM =
-  sig
-    val dbname : string (** File name of the Dbm database. Files {i dbname}[.dir] and {i dbname}[.pag] are created if necessary. *)
-    val max_mem : float  (** Number of bytes beyond which nodes are removed from memory. *)
-    val node_chunk : int  (** Number of nodes that are removed from memory when more than [max_mem] is used. *) 
-    val log_file : string option  (** Optional filename for printing a log of internal messages. *)
-  end
-
-(** The second input signature of the functor {!Logdag.Make} specifying the logic. *)
-module type LOG =
-  sig
-    type t  (** Abstract type of formulas. *)
-    val top : unit -> t  (** Most general formula. *)
-    val entails : t -> t -> bool  (** Entailment relation {e is more specific than} of the logic. *)
-    val parse : Syntax.t_stream -> t  (** Parsing of formulas from token streams. *)
-    val print : t -> Syntax.t_list  (** Printing of formulas to token lists. *)
-    val gen : t -> t -> t list -> t list  (** Dichotomic operator for generating new features. *)
-    val simpl : t -> t Stream.t  (** Simplifications of a formula. *)
-  end
-
-(** The signature of implementations of logical diagrams. *)
-module type T =
-  sig
-    module Log : LOG
-    (** The logic module passed as a parameter. *)
-
-    val some_log : bool
-    (** True if a log file is open. *)
-
-    val log_fmt : Format.formatter
-    (** The formatter associated to the log file when it exists. *)
-
-    val db : Dbm.t
-    (** The database used for persistency and swapping. *)
-
-    type nid = int
-    (** Type of node ids. This type is also used for identifying objects: the id of an object is the id of its description node. *)
-
-    val nil : nid
-    (** Nil id referencing no node. *)
-
-    val top : nid
-    (** Id of the most general node. *)
-
-(*
-    (** Module for the representation of extents (sets of objects). *)
-    module Ext :
-      sig
-        type t  (** Abstract type of extents. *)
-        val empty : t  (** The empty extent. *)
-        val is_empty : t -> bool  (** [is_empty ext] tests whether [ext] is empty. *)
-        val cardinal : t -> int  (** [cardinal ext] returns the size of the extent [ext]. *)
-        val mem : nid -> t -> bool  (** [mem o ext] tests whether [o] belongs to [ext]. *)
-        val contains : t -> t -> bool  (** [contains ext1 ext2] tests whether [ext1] contains [ext2]. *)
-        val add : nid -> t -> t  (** [add o ext] returns the addition of [o] to [ext]. *)
-        val remove : nid -> t -> t  (** [remove o ext] returns the removal of [o] from [ext]. *)
-        val union : t -> t -> t  (** [union ext1 ext2] returns the set union of [ext1] and [ext2]. *)
-        val union_r : t list -> t  (** [union_r exts] returns the union of all extents in [exts]. *)
-        val inter : t -> t -> t  (** [inter ext1 ext2] returns the set intersection of [ext1] and [ext2]. *)
-        val inter_r : t list -> t  (** [inter_r exts] returns the intersection of all extents in [exts].
-                                       @raise Invalid_argument if [exts] is the empty list. *)
-        val subtract : t -> t -> t  (** [subtract ext1 ext2] returns the set subtraction of [ext1] and [ext2]. *)
-        val inter_difsym : t -> t -> t * t * t
-          (** [inter_difsym ext1 ext2] returns the extent triplet [(subtract ext1 ext2, inter ext1 ext2, subtract ext2 ext1)]. *)
-        val iter : (nid -> unit) -> t -> unit
-          (** Iteration on the objects of an extent (see [List.iter]). Objects visited from low ids to high ids. *)
-        val fold_left : ('a -> nid -> 'a) -> 'a -> t -> 'a
-          (** Folding on an extent from low ids to high ids (see List.fold_left). *)
-        val fold_right : (nid -> 'a -> 'a) -> t -> 'a -> 'a
-          (** Folding on an extent from high ids to low ids (see List.fold_right). *)
-      end
-*)
-
-    type node
-    (** Abstract type of nodes.
-
-       {e Warning}: values of this type are relevant at the time they are
-	retrieved, but are not guarenteed to remain consistent after changes are
-	made. *)
-
-    val feat : node -> Log.t
-    (** [feat node] gets the formula label of [node]. *)
-
-    val ext : node -> Ext.t
-    (** [ext node] gets the extent label of [node]. *)
-
-    val inf : node -> nid LSet.t
-    (** [inf node] gets the inferior (more specific) neighbours of [node]. *)
-
-    val sup : node -> nid LSet.t
-    (** [sup node] gets the superior (more general) neighbours of [node]. *)
-
-    val is_obj : node -> bool
-    (** [is_obj node] test whether [node] is labeled by an object. *)
-
-    val get : nid -> node
-    (** [get nid] retrieves a node from its id [nid]. If the node is not yet in memory, it is loaded from the database.
-        @raise Not_found when the node [nid] does not exist in the diagram. *)
-
-    val insert : Log.t -> bool -> nid * bool
-    (** [insert f obj] returns the node id whose formula label is
-	logically equivalent to [f]. If such a node does not yet exist in the
-	diagram, it is inserted and the second result is [true]; otherwise the second result is [false]. 
-        If [obj] is true, then a new object is
-	associated to this node, and extents of existing nodes are updated
-	accordingly. *)
-
-    val remove : nid -> unit
-    (** [remove nid] removes the node identified by [nid] from the diagram (both in memory and the database). *)
-
-    val fold : (nid * node Lazy.t -> 'a -> 'a * nid list) -> nid * node Lazy.t -> 'a -> 'a
-    (** [fold f_next (nid,node) e] computes a result through a traversal of
-	the diagram. The starting node is specified by [(nid,node)], where
-	[node] is the lazy evaluation of [get nid]. The application [f_next (nid,node)
-	res] to the current node [(nid,node)] and the current result [res]
-	returns a pair [(res',next_nids)], where [res'] is the new result, and
-	[next_nids] are the ids of the next nodes to be visited. The traversal
-	order is not specified, but each node is ensured to be visited at most
-	once. *)
-
-    val first : pred_next:(bool -> nid * node Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> 'a list
-    (** [first ~pred_next ~start:(nid,node)] looks for the first nodes encountered in
-	a traversal of the diagram, and satisfying some condition {e
-	pred}. The traversal is defined similarly to [fold] (starting point,
-	and next nodes). The first result of an application of [pred_next] is
-	[None] if {e pred} is not satisfied, and [Some] {i v} otherwise, {i v}
-	being the value returned as a result instead of the node itself. The
-	first parameter can be used for optimization as, when it is false,
-	[None] can be returned in all cases. *)
-
-    val last : pred_next:(nid * node Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> 'a list
-    (** [last ~pred_next ~start:(nid,node)] looks for the last nodes encountered in
-	a traversal of the diagram, and satisfying some condition {e
-	pred}. The traversal is defined similarly to [fold] (starting point,
-	and next nodes). The first result of an application of [pred_next] is
-	[None] if {e pred} is not satisfied, and [Some] {i v} otherwise, {i v}
-	being the value returned as a result instead of the node itself. *)
-
-    val glbs : pred:(nid * node Lazy.t -> bool) -> (nid * node Lazy.t) list -> (nid * node Lazy.t) list
-    (** [glbs ~pred nodes] returns the {e glbs} (greatest lower bounds) of the nodes [nodes] among the nodes satisfying [pred]. *)
-
-    val lubs : pred:(nid * node Lazy.t -> int -> 'a option) -> suppmin:int -> (nid * node Lazy.t) list -> 'a list
-    (** [lubs ~pred ~suppmin nodes] returns the [suppmin]-approximate {e lubs}
-	(least upper bounds) of the nodes [nodes] among the nodes satisfying
-	[pred]. A node is a [suppmin]-approximate lub if it has at least
-	[suppmin] more specific nodes in [nodes]. The second argument of
-	[pred] is the support of the node (number of more specific nodes in
-	[nodes]). *)
-
-  end
-
-module Make (Param : PARAM) (Log : LOG) : T =
-  struct
-    module Log = Log
-
-    open Format
-
-    let some_log = match Param.log_file with None -> false | Some _ -> true
-    let log_fmt = match Param.log_file with None -> Format.err_formatter | Some name -> formatter_of_out_channel (open_out name)
-
-    type nid = int
-
-    module Nval =
-      struct
-        type t = float
-        let init () = Common.utime ()
-        let update v = Common.prof "Logdag.Nval.update" (fun () -> Common.utime ())
-        let better v1 v2 = v1 >= v2
-      end
-
-    type node = {
-	mutable feat : Log.t;  (* formula describing the node, and description of local object if some *)
-	mutable ext : Ext.t;  (* object idents of the extent *)
-	mutable sup : nid LSet.t;  (* list of parent nodes *)
-	mutable inf : nid LSet.t;  (* list of child nodes *)
-        mutable v : Nval.t  (* value w.r.t. swapping *)
-      }
-
-    let nil = 0
-    let node_nil = {
-        feat = Log.top ();
-        ext = Ext.empty;
-        inf = LSet.empty ();
-        sup = LSet.empty ();
-        v = Nval.init ()
-      }
-
-    let top = 1
-
-    let db = Dbm.opendbm Param.dbname [Dbm.Dbm_create; Dbm.Dbm_rdwr] 0o664
-    let _ = at_exit (fun () -> Dbm.close db)
-
-    let db_mod : Dbm.t Cache.db_mod = {
-        Cache.find = Dbm.find;
-        Cache.replace = Dbm.replace;
-        Cache.remove = Dbm.remove
-      }
-
-    let cache_cpt = Cache.create db_mod db "cpt" 1
-    let _ =
-      if not (Cache.mem cache_cpt 0)
-      then Cache.add cache_cpt 0 (ref (top+1))
-
-    let cpt () = Cache.get cache_cpt 0
-
-
-    let cache_nid = Cache.create db_mod db "nid" Param.node_chunk
-    let _ =
-      if not (Cache.mem cache_nid top)
-      then Cache.add cache_nid top node_nil
-
-    let get_worst_chunk () =
-      let rec insert x =
-        function
-        | [] -> [x]
-        | y::ys ->
-           if Nval.better x y
-           then x::y::ys
-           else y::insert x ys in
-      let _, worst_chunk =
-        Cache.fold
-          (fun nid node (n,l) ->
-             let n', l' = n+1, insert (node.v,nid) l in
-             if n' <= Param.node_chunk
-             then n', l'
-             else n, List.tl l')
-          cache_nid (0,[]) in
-      List.map snd worst_chunk
-
-    let unget_cpt = ref 0
-
-    let unget_chunk () = Common.prof "Logdag.unget_chunk" (fun () ->
-      if (unget_cpt := !unget_cpt+1 mod Param.node_chunk; !unget_cpt = 0) & Common.heap_size () > Param.max_mem
-      then begin
-        if some_log then pp_print_string log_fmt "Logdag: swapping nodes on disk\n";
-        let keys = get_worst_chunk () in
-        List.iter (Cache.unget cache_nid) keys;
-        Gc.major () end)
-
-    let get nid = Common.prof "Logdag.get" (fun () ->
-      unget_chunk ();
-      let node = Cache.get cache_nid nid in
-      node.v <- Nval.update node.v;
-      node)
-
-    let create node =
-      unget_chunk ();
-      let cpt = cpt () in
-      let nid = !cpt in
-      incr cpt;
-      Cache.add cache_nid nid node;
-      nid
-
-    let delete nid = Cache.remove cache_nid nid
-
-
-    let feat node = node.feat
-
-    let ext node = node.ext
-
-    let inf node = node.inf
-
-    let sup node = node.sup
-
-    let is_obj node = LSet.is_empty node.inf & node.ext <> Ext.empty
-
-    let rec fold : (nid * node Lazy.t -> 'a -> 'a * nid list) -> nid * node Lazy.t -> 'a -> 'a =
-      fun f_next (nid,node) init ->
-        let m = Array.make !(cpt ()) `Unknown
-        in fold2 m f_next (nid,node) init
-    and fold2 m f_next (nid,node) init =
-      if m.(nid) = `Unknown
-      then begin
-        m.(nid) <- `Good;
-        let res0, nids = f_next (nid,node) init in
-        List.fold_left
-	  (fun res n -> fold2 m f_next (n,lazy (get n)) res)
-	  res0
-	  nids end
-      else init
-
-    let rec first : pred_next:(bool -> nid * node Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> 'a list =
-      fun ~pred_next ~start ->
-	let m = Array.make !(cpt ()) `Unknown
-	in List.map snd (
-          List.fold_left
-	    (fun res nid -> first2 m pred_next (nid,lazy (get nid)) true res)
-	    [] (snd (pred_next false start)))
-    and first2 m pred_next (nid,node) above res =
-	if m.(nid) = `Unknown then
-	  let x, nids = pred_next above (nid,node) in
-	  let good = above & (x <> None) in
-	  m.(nid) <- if good then `Good else `Bad;
-	  List.fold_left
-	    (fun res n -> first2 m pred_next (n,lazy (get n)) (above & not good) res)
-	    (match x with None -> res | Some v -> if good then ((nid, v)::res) else res)
-	    nids
-	else if m.(nid) = `Good & not above then begin
-	  m.(nid) <- `Bad;
-	  List.filter (fun (n,v) -> n != nid) res end 
-	else res
-
-    let rec last : pred_next:(nid * node Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> 'a list =
-      fun ~pred_next ~start ->
-	let m = Array.make !(cpt ()) `Unknown in
-	snd (new_last m pred_next start [])
-    and new_last m pred_next (nid,node) res =
-	let x, nids = pred_next (nid,node) in
-	let last, res1 = List.fold_left
-	    (fun (last,res) n ->
-	      if m.(n) = `Good then (false,res) (* node is not a last one *)
-	      else if m.(n) = `Bad then (last,res) (* node may be a last one *)
-	      else (* m.(n) = `Unknown *)
-		let last',res' = new_last m pred_next (n,lazy (get n)) res in
-		last & last', res')
-	    (true,res)
-	    nids in
-	if not last
-	then begin m.(nid) <- `Good; (false,res1) end
-	else match x with
-	| None -> begin m.(nid) <- `Bad; (true,res1) end
-	| Some v -> begin m.(nid) <- `Good; (false,v::res1) end
-
-    let glbs : pred:(nid * node Lazy.t -> bool) -> (nid * node Lazy.t) list -> (nid * node Lazy.t) list =
-      fun ~pred -> function
-	| [] -> [(top,lazy (get top))]
-	| [nidnode] when pred nidnode -> [nidnode]
-	| nidnodes ->
-	    let m = Array.make !(cpt ()) 0 in
-	    let lnodes = List.length nidnodes in
-	    List.iter
-	      (fun (nid,node) ->
-		fold (fun (n,nd) res -> m.(n) <- m.(n)+1; (), (Lazy.force nd).inf) (nid,node) ())
-	      nidnodes;
-	    first
-	      (fun above (nid,node) ->
-		(if above & m.(nid) >= lnodes & pred (nid,node) then Some (nid,node) else None), (Lazy.force node).inf)
-	      (nil, lazy {node_nil with inf = List.map fst nidnodes})
-
-    let rec lubs : pred:(nid * node Lazy.t -> int -> 'a option) -> suppmin:int -> (nid * node Lazy.t) list -> 'a list =
-      fun ~pred ~suppmin -> function
-	| [] -> raise (Invalid_argument "LogDag.Make.lubs : the list is empty") 
-	| nidnodes -> Common.prof "Logdag.lubs" (fun () ->
-	    let m = Array.make !(cpt ()) 0 in
-	    let l = List.length nidnodes in
-	    let supp = min suppmin l in
-	    List.iter
-	      (fun (nid,node) ->
-		fold (fun (n,nd) res -> m.(n) <- m.(n)+1; (), (Lazy.force nd).sup) (nid,node) ())
-	      (if supp=l then List.tl nidnodes else nidnodes);
-            let smin = if supp=l then supp-1 else supp in
-	    first
-	      (fun _ (nid,node) ->
-                let s = m.(nid) in
-		(if s >= smin then pred (nid,node) s else None),
-		(Lazy.force node).sup)
-	      (if supp=l then (List.hd nidnodes) else (nil,lazy {node_nil with sup = List.map fst nidnodes})))
-
-
-    let locate : Log.t -> bool -> nid * node =
-      fun feat obj ->
-	let sup =
-	  last
-	    ~pred_next:(fun (nid,node) ->
-	       if not (is_obj (Lazy.force node)) & Log.entails feat (Lazy.force node).feat
-	       then Some (nid,node), (Lazy.force node).inf
-	       else None, [])
-	    ~start:(top,lazy (get top)) in
-	match sup with
-	| [(nid,node)] when not obj & Log.entails (Lazy.force node).feat feat ->
-	     (Lazy.force node).feat <- feat;  (* the old formula is replaced by the new equivalent one *)
-	     nid, Lazy.force node  (* the searched node already exists *)
-	| nodes ->  (* the searched node must be inserted *)
-	     let inf, ext =
-	       if obj
-               then LSet.empty (), Ext.empty
-               else
-                 let inf = glbs (fun (nid,node) -> Log.entails (Lazy.force node).feat feat) nodes in
-                 inf, List.fold_left Ext.union Ext.empty (List.map (fun (nid,node) -> (Lazy.force node).ext) inf) in
-	     let new_node = {
-		feat = feat;
-		ext = ext;
-		sup = LSet.of_list (List.map fst sup);
-		inf = LSet.of_list (List.map fst inf);
-                v = Nval.init ()} in
-	     nil, new_node
-
-    let connect : nid -> node -> bool -> unit =
-      fun nid node obj ->
-	List.iter
-	  (fun n ->
-             let nd = get n in
-             nd.inf <- LSet.add nid (LSet.subtract nd.inf node.inf))
-	  node.sup;
-	List.iter
-	  (fun n ->
-             let nd = get n in
-             nd.sup <- LSet.add nid (LSet.subtract nd.sup node.sup))
-	  node.inf;
-        if obj
-        then
-	  fold
-	    (fun (n,nd) () ->
-               let nd_val = Lazy.force nd in
-               nd_val.ext <- Ext.add nid nd_val.ext; (), nd_val.sup)
-	    (nid,lazy node)
-	    ()
-
-    let insert feat obj = Common.prof "Logdag.insert" (fun () ->
-      let nid, node = locate feat obj in
-      if nid = nil
-      then begin
-        let nid = create node in
-        connect nid node obj;
-        nid, true end
-      else begin
-        nid, false end)
-
-    let rec disconnect nid =
-      let node = get nid in
-      if is_obj node
-      then
-	fold
-	  (fun (n,nd) () ->
-             let nd_val = Lazy.force nd in
-             nd_val.ext <- Ext.remove nid nd_val.ext; (), nd_val.sup)
-	  (nid,lazy node)
-	  ();
-      List.iter (fun n -> let nd = get n in nd.inf <- LSet.remove nid nd.inf) node.sup;
-      List.iter (fun n -> let nd = get n in nd.sup <- LSet.remove nid nd.sup) node.inf;
-      let mup = Array.make !(cpt ()) false in
-      fold
-        (fun (n,nd) () -> (mup.(n) <- true), (Lazy.force nd).sup)
-        (nil,lazy {node_nil with sup = node.inf})
-        ();
-      let mdown = Array.make !(cpt ()) false in
-      let tbl = Hashtbl.create (2 * LSet.cardinal node.inf) in
-      List.iter (fun n -> Hashtbl.add tbl n node.sup) node.inf;
-      List.iter
-	(fun n ->
-           let nd = get n in
-           List.iter (fun n' -> mdown.(n') <- false) node.inf;
-           fold
-             (fun (n',nd') () -> (mdown.(n') <- true), if mup.(n') then (Lazy.force nd').inf else [])
-             (n,lazy (get n))
-             ();
-           let inf_old, inf_new = List.partition (fun n' -> mdown.(n')) node.inf in
-	   nd.inf <- LSet.union nd.inf inf_new;
-           List.iter (fun n' -> Hashtbl.replace tbl n' (LSet.remove n (Hashtbl.find tbl n'))) inf_old)
-        node.sup;
-      List.iter
-        (fun n ->
-           let nd = get n in
-           nd.sup <- LSet.union nd.sup (Hashtbl.find tbl n))
-        node.inf
-
-    let remove nid =
-      if nid <> top
-      then begin
-        try disconnect nid with Not_found -> ();
-        delete nid end
-
-  end

logdag.mli

-(**
-Logical DAG (Directed Acyclic Graphs) with objects.
-
-Object descriptions and features represented by formulas are
-represented as a DAG. The nodes are labeled by a logical formula, and
-a set of objects (extent). The nodes are ordered according to the
-entailment relation of the logic. This logic is specified as a
-functorial parameter.
-
-The nodes are persistent in a Dbm database, and can be partially
-represented in memory, thus allowing for very large DAGs.
-*)
-
-(** The first input signature of the functor {!Logdag.Make} specifying various paramters. *)
-module type PARAM =
-  sig
-    val dbname : string (** File name of the Dbm database. Files {i dbname}[.dir] and {i dbname}[.pag] are created if necessary. *)
-    val max_mem : float  (** Number of bytes beyond which nodes are removed from memory. *)
-    val node_chunk : int  (** Number of nodes that are removed from memory when more than [max_mem] is used. *) 
-    val log_file : string option  (** Optional filename for printing a log of internal messages. *)
-  end
-
-(** The second input signature of the functor {!Logdag.Make} specifying the logic. *)
-module type LOG =
-  sig
-    type t  (** Abstract type of formulas. *)
-    val top : unit -> t  (** Most general formula. *)
-    val entails : t -> t -> bool  (** Entailment relation {e is more specific than} of the logic. *)
-    val parse : Syntax.t_stream -> t  (** Parsing of formulas from token streams. *)
-    val print : t -> Syntax.t_list  (** Printing of formulas to token lists. *)
-    val gen : t -> t -> t list -> t list  (** Dichotomic operator for generating new features. *)
-    val simpl : t -> t Stream.t  (** Simplifications of a formula. *)
-  end
-
-(** The signature of implementations of logical diagrams. *)
-module type T =
-  sig
-    module Log : LOG
-    (** The logic module passed as a parameter. *)
-
-    val some_log : bool
-    (** True if a log file is open. *)
-
-    val log_fmt : Format.formatter
-    (** The formatter associated to the log file when it exists. *)
-
-    val db : Dbm.t
-    (** The database used for persistency and swapping. *)
-
-    type nid = int
-    (** Type of node ids. This type is also used for identifying objects: the id of an object is the id of its description node. *)
-
-    val nil : nid
-    (** Nil id referencing no node. *)
-
-    val top : nid
-    (** Id of the most general node. *)
-
-    type node
-    (** Abstract type of nodes.
-
-       {e Warning}: values of this type are relevant at the time they are
-	retrieved, but are not guarenteed to remain consistent after changes are
-	made. *)
-
-    val feat : node -> Log.t
-    (** [feat node] gets the formula label of [node]. *)
-
-    val ext : node -> Ext.t
-    (** [ext node] gets the extent label of [node]. *)
-
-    val inf : node -> nid LSet.t
-    (** [inf node] gets the inferior (more specific) neighbours of [node]. *)
-
-    val sup : node -> nid LSet.t
-    (** [sup node] gets the superior (more general) neighbours of [node]. *)
-
-    val is_obj : node -> bool
-    (** [is_obj node] test whether [node] is labeled by an object. *)
-
-    val get : nid -> node
-    (** [get nid] retrieves a node from its id [nid]. If the node is not yet in memory, it is loaded from the database.
-        @raise Not_found when the node [nid] does not exist in the diagram. *)
-
-    val insert : Log.t -> bool -> nid * bool
-    (** [insert f obj] returns the node id whose formula label is
-	logically equivalent to [f]. If such a node does not yet exist in the
-	diagram, it is inserted and the second result is [true]; otherwise the second result is [false]. 
-        If [obj] is true, then a new object is
-	associated to this node, and extents of existing nodes are updated
-	accordingly. *)
-
-    val remove : nid -> unit
-    (** [remove nid] removes the node identified by [nid] from the diagram (both in memory and the database). *)
-
-    val fold : (nid * node Lazy.t -> 'a -> 'a * nid list) -> nid * node Lazy.t -> 'a -> 'a
-    (** [fold f_next (nid,node) e] computes a result through a traversal of
-	the diagram. The starting node is specified by [(nid,node)], where
-	[node] is the lazy evaluation of [get nid]. The application [f_next (nid,node)
-	res] to the current node [(nid,node)] and the current result [res]
-	returns a pair [(res',next_nids)], where [res'] is the new result, and
-	[next_nids] are the ids of the next nodes to be visited. The traversal
-	order is not specified, but each node is ensured to be visited at most
-	once. *)
-
-    val first : pred_next:(bool -> nid * node Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> 'a list
-    (** [first ~pred_next ~start:(nid,node)] looks for the first nodes encountered in
-	a traversal of the diagram, and satisfying some condition {e
-	pred}. The traversal is defined similarly to [fold] (starting point,
-	and next nodes). The first result of an application of [pred_next] is
-	[None] if {e pred} is not satisfied, and [Some] {i v} otherwise, {i v}
-	being the value returned as a result instead of the node itself. The
-	first parameter can be used for optimization as, when it is false,
-	[None] can be returned in all cases. *)
-
-    val last : pred_next:(nid * node Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> 'a list
-    (** [last ~pred_next ~start:(nid,node)] looks for the last nodes encountered in
-	a traversal of the diagram, and satisfying some condition {e
-	pred}. The traversal is defined similarly to [fold] (starting point,
-	and next nodes). The first result of an application of [pred_next] is
-	[None] if {e pred} is not satisfied, and [Some] {i v} otherwise, {i v}
-	being the value returned as a result instead of the node itself. *)
-
-    val glbs : pred:(nid * node Lazy.t -> bool) -> (nid * node Lazy.t) list -> (nid * node Lazy.t) list
-    (** [glbs ~pred nodes] returns the {e glbs} (greatest lower bounds) of the nodes [nodes] among the nodes satisfying [pred]. *)
-
-    val lubs : pred:(nid * node Lazy.t -> int -> 'a option) -> suppmin:int -> (nid * node Lazy.t) list -> 'a list
-    (** [lubs ~pred ~suppmin nodes] returns the [suppmin]-approximate {e lubs}
-	(least upper bounds) of the nodes [nodes] among the nodes satisfying
-	[pred]. A node is a [suppmin]-approximate lub if it has at least
-	[suppmin] more specific nodes in [nodes]. The second argument of
-	[pred] is the support of the node (number of more specific nodes in
-	[nodes]). *)
-
-  end
-
-(** Functor building an implementation of logical DAGs. *)
-module Make (Param : PARAM) (Log : LOG) : T
 .SUFFIXES: .mll .ml .mli .cmo .cmi
 
 # Make all
-all: common.cmo threads_common.cmo unicode.cmo tokens.cmo lexer.cmo syntax.cmo bintree.cmo lSet.cmo cis.cmi cis.cmo iterator.cmo intmap.cmo intset.cmo intrel.cmo intrel2.cmo intreln.cmo text_index.cmo setset.cmo term.cmo cache.cmi cache.cmo ext.cmo suffix_tree.cmo index.cmo seq.cmo logdag.cmi logdag.cmo persindex.cmo genid.cmo persintset.cmo persintset.cmo stringset.cmo seqset.cmo
+all: common.cmo threads_common.cmo unicode.cmo bintree.cmo lSet.cmo cis.cmi cis.cmo iterator.cmo intmap.cmo intset.cmo intrel.cmo intrel2.cmo intreln.cmo text_index.cmo setset.cmo cache.cmi cache.cmo ext.cmo suffix_tree.cmo index.cmo seq.cmo persindex.cmo genid.cmo persintset.cmo persintset.cmo stringset.cmo seqset.cmo
 	echo
 
 # archiving

syntax.ml

-(** Syntax utility functions. *)
-
-(* analyse lexicale g�n�rique *)
-
-type t_stream = Tokens.t Stream.t
-
-type t_list = Tokens.t list
-
-type decimal = int * int (* fraction and exponent *)
-
-open Tokens
-
-(* forbidden idents in syntax of logics *)
-let keywords = ["thing";"nothing";"and";"or";"not";"except";"implies";"if";"then";"else";"some";"every";"only";"something";"the";"of";"by";"with";"is";"trans";"opt";"co";"share";"a";"an";"this";"that";"whose"]
-
-let not_PP t = not (Tokens.is_PP t)
-(*
-function
-  | PP_tilda | PP_space | PP_cut | PP_break _ | PP_newline -> false
-  | _ -> true
-*)
-
-let rec length = function
-  | [] -> 0
-  | x::xs -> (if not_PP x then 1 else 0) + length xs
-
-(* deprecated -> moved into logics *)
-(*
-let rec get_terms : t_list -> string list =
-  function
-      [] -> []
-    | Term name::l -> name::get_terms l
-    | _::l -> get_terms l
-*)
-
-let from_channel : in_channel -> t_stream =
-  fun ch ->
-    let lexbuf = Lexing.from_channel ch in
-    Stream.from (fun _ ->
-      try Some (Lexer.token lexbuf)
-      with Eof -> None)
-
-let from_string : string -> t_stream =
-  fun s ->
-    let lexbuf = Lexing.from_string s in
-    Stream.from (fun _ ->
-      try Some (Lexer.token lexbuf)
-      with Eof -> None)
-
-let rec list_of_stream s =
-  try
-    let x = Stream.next s in
-    x::list_of_stream s
-  with _ -> []
-
-let list_of_string s =
-  list_of_stream (from_string s)
-
-let rec of_list : t_list -> t_stream =
-  fun toks -> Stream.of_list (List.filter not_PP toks)
-
-(* get the string representation of the token *)
-type space_of_token = Sep | PonctL | PonctR | Op | Word
-
-open Format
-
-(*
-let rec power10 : int -> float =
-      function
-      | 0 -> 1.
-      | p -> if p > 0
-             then power10 (p-1) *. 10.
-             else power10 (p+1) /. 10.
-*)
-
-let string_escaped : string -> string =
-  fun s ->
-    let l1 = String.length s in
-    let buf = Buffer.create (2 * l1) in
-    for i=0 to l1-1 do
-      if s.[i] = '"' then Buffer.add_string buf "\\\""
-      else if s.[i] = '\\' then Buffer.add_string buf "\\\\"
-      else if s.[i] = '\n' then Buffer.add_string buf "\\n"
-      else if s.[i] = '\t' then Buffer.add_string buf "\\t"
-      else Buffer.add_char buf s.[i]
-    done;
-    Buffer.contents buf
-
-let term_escaped : string -> string =
-  fun s ->
-    let l1 = String.length s in
-    let buf = Buffer.create (2 * l1) in
-    for i=0 to l1-1 do
-      if s.[i] = '\'' then Buffer.add_string buf "\\\'"
-      else if s.[i] = '\\' then Buffer.add_string buf "\\\\"
-      else Buffer.add_char buf s.[i]
-    done;
-    Buffer.contents buf
-
-let pp_print_token : formatter -> Tokens.t -> Tokens.t -> unit =
-  fun ff pred -> function
-    | BackQuote -> pp_print_string ff "`"
-    | Exclam -> pp_print_string ff "!"
-    | LeftPar -> pp_print_string ff "("
-    | RightPar -> pp_print_string ff ")"
-    | LeftAcc -> pp_print_string ff "{"
-    | RightAcc -> pp_print_string ff "}"
-    | LeftBra -> pp_print_string ff "["
-    | RightBra -> pp_print_string ff "]"
-    | Interro -> pp_print_string ff "?"
-    | Comma -> pp_print_string ff ","
-    | Dot -> pp_print_string ff "."
-    | Colon -> pp_print_string ff ":"
-    | SemiColon -> pp_print_string ff ";"
-    | DoubleQuote -> pp_print_string ff "\""
-    | Quote -> pp_print_string ff "'"
-    | Nat n ->
-	(match pred with
-	| Nat 0 | MinusNat 0 -> ()
-	| Nat _ | MinusNat _ | Symbol _ -> pp_print_string ff " "
-	| _ -> ());
-	pp_print_int ff n
-    | MinusNat n ->
-	(match pred with
-	| Nat 0 | MinusNat 0 -> ()
-	| Nat _ | MinusNat _ | Symbol _ -> pp_print_string ff " "
-	| _ -> ());
-	pp_print_string ff "-"; pp_print_int ff n
-    | String s ->
-	pp_print_string ff ("\"" ^ string_escaped s ^ "\"")
-    | Char c ->
-	pp_print_string ff ("`" ^ Char.escaped c ^ "`")
-    | Symbol s ->
-	( match pred with
-	| Nat _ | MinusNat _ | Symbol _ -> pp_print_string ff " "
-	| _ -> ());
-	if Tokens.symbol_needs_quotes s
-	then pp_print_string ff ("'" ^ term_escaped s ^ "'")
-	else pp_print_string ff s
-    | PP_tilda -> pp_print_string ff " "
-    | PP_space -> pp_print_space ff ()
-    | PP_cut -> pp_print_cut ff ()
-    | PP_break (spaces,offset) -> pp_print_break ff spaces offset
-    | PP_newline -> pp_print_newline ff ()
-
-
-let rec pp_print_tokens : formatter -> t_list -> unit =
-  fun ff toks -> pp_print_tokens2 ff PP_newline toks
-and pp_print_tokens2 ff pred =
-  function
-    | [] -> ()
-    | tok::toks ->
-	pp_print_token ff pred tok;
-	pp_print_tokens2 ff tok toks
-
-let stringizer : t_list -> string =
-  fun toks ->
-    pp_print_tokens Format.str_formatter (List.map (fun tok -> if not_PP tok then tok else PP_tilda) toks);
-    Format.flush_str_formatter ()
-
-let print_tokens : t_list -> unit =
-  fun toks ->
-    pp_print_tokens Format.std_formatter toks
-
-let print_string : string -> unit =
-  fun s ->
-    pp_print_string Format.std_formatter s 
-
-let print_int : int -> unit =
-  fun n ->
-    pp_print_int Format.std_formatter n
-
-
-(* fonctions generiques pour le printing *)
-(* ------------------------------------- *)
-
-(* printing a signed integer to tokens *)
-let toks_of_int : int -> t_list =
-  fun n ->
-    let s = string_of_int n in
-    list_of_stream (from_string s)
-
-let float_of_decimal : decimal -> float =
-  fun (frac,expo) ->
-    float_of_string (string_of_int frac ^ "e" ^ string_of_int expo)
-
-let toks_of_decimal : decimal -> t_list =
-  fun (frac,expo) ->
-    let sign, abs_frac =
-      if frac < 0
-      then "-", -frac
-      else "", frac in
-    let s_abs_frac = string_of_int abs_frac in
-    let l = String.length s_abs_frac in
-    let s =
-      if expo > 0 then 
-	sign ^ s_abs_frac ^ ".e" ^ string_of_int expo
-      else if expo = 0 then
-	sign ^ s_abs_frac ^ "."
-      else if expo >= (-l + 1) && expo <= (-1) then
-	sign ^ String.sub s_abs_frac 0 (l - (-expo)) ^ "." ^ String.sub s_abs_frac (l - (-expo)) (-expo)
-      else if expo = -l then
-	sign ^ "0." ^ s_abs_frac
-      else if expo <= -l then
-	sign ^ "0." ^ s_abs_frac ^ "e" ^ string_of_int (expo + l)
-      else assert false in
-    list_of_stream (from_string s)
-
-(*
-let toks_of_float : (int * int) -> t_list =
-  fun (f,p) ->
-    let sm = if f=0. then "" else string_of_int (int_of_float ((abs_float f) *. (power10 (-p)))) in
-    let l = String.length sm in
-    let e = let x = (p+l) mod 3 in if x >= 0 then x else x+3 in
-    let exp e = if e = 0 then "" else "e" ^ string_of_int e in
-    let s =
-      (if f < 0. then "-" else "") ^
-      if e = 1 then
-	if l >= 1 & p+l+2 <> 0 then String.sub sm 0 1 ^ "." ^ String.sub sm 1 (l-1) ^ exp (p+l-1)
-	else "0.00" ^ sm ^ exp (p + l + 2)
-      else if e = 2 then
-        if l >= 2 & p+l+1 <> 0 then String.sub sm 0 2 ^ "." ^ String.sub sm 2 (l-2) ^ exp (p+l-2)
-        else "0.0" ^ sm ^ exp (p + l + 1)
-      else
-        if l >= 3 & p+l <> 0 then String.sub sm 0 3 ^ "." ^ String.sub sm 3 (l-3) ^ exp (p+l-3)
-        else "0." ^ sm ^ exp (p + l) in
-    list_of_stream (from_string s)
-*)
-
-(* messages d'erreur syntaxique *)
-
-let error_RightPar = "Syntax error: a closing parenthesis is missing."
-let error_RightBra = "Syntax error: a closing bracket is missing."
-
-(* add parenthesis around the given t_list if op (precedence) is above the ctx (precedence) *)
-
-let add_par : int -> int -> t_list -> t_list =
-  fun ctx op l -> if op > ctx then LeftPar::(l @ [RightPar]) else l
-
-(* fonctions generiques pour le parsing *)
-(* ------------------------------------ *)
-
-(* parsing a signed integer *)
-let parse_int : t_stream -> int = parser
-  | [<'Nat n>] -> n
-  | [<'MinusNat n>] -> (- n)
-
-(* get the fraction and exponent (integers) of a float number from its writing *)
-let decimal_of_sfloat : string -> decimal =
-  fun s ->
-      let l = String.length s in
-      let i_e, p =
-        try
-          let i_e = String.index s 'e' in
-          i_e,
-          int_of_string (String.sub s (i_e+1) (l-(i_e+1)))
-        with Not_found -> l, 0 in
-      let i_dot, frac, expo =
-        try 
-	  let i_dot = String.index s '.' in
-	  i_dot,
-	  int_of_string (String.sub s 0 i_dot ^ String.sub s (i_dot+1) (i_e - i_dot - 1)),
-	  p - (i_e - i_dot - 1)
-	with Not_found ->
-	  i_e,
-	  int_of_string (String.sub s 0 i_e),
-	  p in
-      frac, expo
-
-(* parsing a float *)
-let rec parse_decimal : t_stream -> decimal = parser
-  | [<s = parse_decimal0>] -> decimal_of_sfloat s (*float_of_string s, prec_of_sfloat s*)
-and parse_decimal0 = parser
-(*  | [<'Dot; m2 = parse_decimal_decimal; s = parse_decimal4>] -> "." ^ m2 ^ s *)
-  | [<'Nat m1; s = parse_decimal2>] -> string_of_int m1 ^ s
-  | [<'MinusNat m1; s = parse_decimal2>] -> "-" ^ string_of_int m1 ^ s
-(*  | [<'Symbol "-"; 'Dot; m2 = parse_decimal_decimal; s = parse_decimal4>] -> "-." ^ m2 ^ s *)
-and parse_decimal2 = parser
-  | [<'Dot; s = parse_decimal3>] -> "." ^ s
-  | [<exp = parse_decimal4>] -> "." ^ exp
-and parse_decimal3 = parser
-  | [<m2 = parse_decimal_decimal; s = parse_decimal4>] -> m2 ^ s
-  | [<e = parse_decimal_e; s = parse_decimal5>] -> e ^ s
-  | [<exp = parse_decimal_exp>] -> exp
-  | [<>] -> ""
-and parse_decimal4 = parser
-  | [<e = parse_decimal_e; s = parse_decimal5>] -> e ^ s
-  | [<exp = parse_decimal_exp>] -> exp
-  | [<>] -> ""
-and parse_decimal5 = parser
-  | [<p = parse_decimal_decimal>] -> p
-  | [<p = parse_decimal_minus_decimal>] -> p
-and parse_decimal_decimal = parser
-  | [<'Nat 0; d = parse_decimal_decimal2>] -> "0" ^ d
-  | [<'Nat d>] -> string_of_int d
-and parse_decimal_minus_decimal = parser
-  | [<'MinusNat 0; d = parse_decimal_decimal2>] -> "-0" ^ d
-  | [<'MinusNat d>] -> "-" ^ string_of_int d
-and parse_decimal_decimal2 = parser
-  | [<'Nat 0; d = parse_decimal_decimal2>] -> "0" ^ d
-  | [<'Nat d>] -> string_of_int d
-  | [<>] -> ""
-and parse_decimal_e = parser
-  | [<'Symbol "e">] -> "e"
-  | [<'Symbol "E">] -> "e"
-and parse_decimal_exp = parser
-  | [<'Symbol exp when Str.string_match (Str.regexp "e[0-9]+$") exp 0>] -> exp
-  | [<'Symbol exp when Str.string_match (Str.regexp "E[0-9]+$") exp 0>] -> exp
-
-(* parsing a number *)
-type num = Int of int | Float of decimal
-
-let rec parse_num : t_stream -> num = parser
-  | [<i, s = parse_num0>] ->
-      if i
-      then Int (int_of_string s)
-      else Float (decimal_of_sfloat s) (*float_of_string s, prec_of_sfloat s*)
-and parse_num0 = parser
-(*  | [<'Dot; m2 = parse_num_decimal; s = parse_num4>] -> false, "." ^ m2 ^ s *)
-  | [<'Nat m1; i,s = parse_num2>] -> i, string_of_int m1 ^ s
-  | [<'MinusNat m1; i,s = parse_num2>] -> i, "-" ^ string_of_int m1 ^ s
-(*  | [<'Symbol "-"; 'Dot; m2 = parse_num_decimal; s = parse_num4>] -> false, "-." ^ m2 ^ s *)
-and parse_num2 = parser
-  | [<'Dot; s = parse_num3>] -> false, "." ^ s
-  | [<exp = parse_num4>] -> if exp = "" then true, "" else false, ("." ^ exp)
-  | [<>] -> true, ""
-and parse_num3 = parser
-  | [<m2 = parse_num_decimal; s = parse_num4>] -> m2 ^ s
-  | [<e = parse_num_e; s = parse_num5>] -> e ^ s
-  | [<exp = parse_num_exp>] -> exp
-  | [<>] -> ""
-and parse_num4 = parser
-  | [<e = parse_num_e; s = parse_num5>] -> e ^ s
-  | [<exp = parse_num_exp>] -> exp
-  | [<>] -> ""
-and parse_num5 = parser
-  | [<p = parse_num_decimal>] -> p
-  | [<p = parse_num_minus_decimal>] -> p
-and parse_num_decimal = parser
-  | [<'Nat 0; d = parse_num_decimal2>] -> "0" ^ d
-  | [<'Nat d>] -> string_of_int d
-and parse_num_minus_decimal = parser
-  | [<'MinusNat 0; d = parse_num_decimal2>] -> "-0" ^ d
-  | [<'MinusNat d>] -> "-" ^ string_of_int d
-and parse_num_decimal2 = parser
-  | [<'Nat 0; d = parse_num_decimal2>] -> "0" ^ d
-  | [<'Nat d>] -> string_of_int d
-  | [<>] -> ""
-and parse_num_e = parser
-  | [<'Symbol "e">] -> "e"
-  | [<'Symbol "E">] -> "e"
-and parse_num_exp = parser
-  | [<'Symbol exp when Str.string_match (Str.regexp "e[0-9]+$") exp 0>] -> exp
-  | [<'Symbol exp when Str.string_match (Str.regexp "E[0-9]+$") exp 0>] -> exp
-
-
-(* parsing of a list of tokens *)
-let rec parse_tokens : t_list -> t_stream -> unit =
-fun toks str ->
-  match List.filter not_PP toks with
-  | [] -> (match str with parser [<>] -> ())
-  | tok::toks -> (match str with parser [<'t when t = tok; _ = parse_tokens toks ?? "Syntax error: '"^stringizer toks^"' expected after '"^stringizer [tok]^"'">] -> ())
-
-(* parsing of an optional list of tokens *)
-let rec parse_tokens_opt : t_list option -> t_stream -> unit =
-fun toks_opt str ->
-  match toks_opt with
-  | None -> raise Stream.Failure
-  | Some toks ->
-      match List.filter not_PP toks with
-      | [] -> (match str with parser [<>] -> ())
-      | tok::toks -> (match str with parser [<'t when t = tok; _ = parse_tokens toks ?? "Syntax error: '"^stringizer toks^"' expected after '"^stringizer [tok]^"'">] -> ())
-
-(* parsing of a list of tokens and something else *)
-let rec parse_tokens_and : t_list -> (t_stream -> 'a) -> t_stream -> 'a =
-fun toks p str ->
-  match List.filter not_PP toks with
-  | [] -> (match str with parser [<x = p>] -> x)
-  | tok::toks -> (match str with parser [<'t when t = tok; x = parse_tokens_and toks p ?? "Syntax error: '"^stringizer toks^"' expected after '"^stringizer [tok]^"'">] -> x)
-
-(* parsing an indefinite number of pattern given some parser *)
-let rec parse_star p = parser
-  | [<x = p; xs = parse_star p>] -> x::xs
-  | [<>] -> []
-
-let parse_plus p = parser
-  | [<x = p; xs = parse_star p>] -> x::xs
-
-(* optional parsing *)
-let parse_opt : (t_stream -> 'a) -> 'a -> (t_stream -> 'a) =
-  fun p e -> parser
-    | [<x = p>] -> x
-    | [<>] -> e
-
-
-(* parsing options *)
-
-let wrong_option s n = "Syntax error: option -"^n^" expected instead of -"^s
-let wrong_option_name n = "Syntax error in some option: '"^n^"' expected after '-'"
-
-let parse_option_bool n = parser
-| [<'Symbol "-"; 'Symbol s ?? wrong_option_name n>] -> s=n or raise (Stream.Error (wrong_option s n))
-| [<>] -> false
-
-let parse_option_int ?(default=0) n = parser
-| [<'Symbol "-"; 'Symbol s when s=n ?? wrong_option_name n; i = parse_int ?? "Syntax error: integer expected after option -"^n>] -> i
-| [<>] -> default
-
-let parse_option_float ? (default=0.) n = parser
-| [<'Symbol "-"; 'Symbol s when s=n ?? wrong_option_name n; dec = parse_decimal ?? "Syntax error: float expected after option -"^n>] -> float_of_decimal dec
-| [<>] -> default
-
-let parse_option_string ?(default="") n = parser
-| [<'Symbol "-"; 'Symbol s when s=n ?? wrong_option_name n; 'String s2 ?? "Syntax error: string expected after opion -"^n>] -> s2
-| [<>] -> default
-
-
-(* parsing of proposition-like language, where operations and atoms are parameterized *)
-
-type 'a spec_prop = { 
-    all : string; none : string; a : string; an : string; o : string; n :  string;
-    taut : 'a; cont : 'a; neg : 'a -> 'a; conj : 'a -> 'a -> 'a; disj : 'a -> 'a -> 'a;
-      atom : t_stream -> 'a
-  } 
-
-let wrong_prop spec s = "Syntax error: '(', '" ^ spec.n ^ "', '" ^ spec.all ^ "', '" ^ spec.none ^ "' or atom expected after '" ^ s ^ "'"
-let wrong_term spec s = "Syntax error: '(', '" ^ spec.n ^ "' or atom expected after '" ^ s ^ "'"
-let wrong_fact spec s = "Syntax error: '(', '" ^ spec.n ^ "' or atom expected after '" ^ s ^ "'"
-
-let rec parse_prop spec = parser
-  | [<q = parse_term spec; f = parse_suite spec>] -> f q
-and parse_suite spec = parser
-  | [<'Tokens.Symbol s when s = spec.o; q = parse_prop spec ?? wrong_prop spec s>] -> (fun q' -> spec.disj q' q)
-  | [<>] -> (fun q' -> q')
-and parse_term spec = parser
-  | [<q = parse_fact spec; f = parse_term_suite spec>] -> f q
-and parse_term_suite spec = parser
-    [<'Tokens.Symbol s when s = spec.a; q = parse_term spec ?? wrong_term spec s>] -> (fun q' -> spec.conj q' q)
-  | [<'Tokens.Symbol s when s = spec.an; q = parse_fact spec ?? wrong_fact spec s>] -> (fun q' -> spec.conj q' (spec.neg q))
-  | [<>] -> (fun q' -> q')
-and parse_fact spec = parser
-  | [<'Tokens.LeftPar; q = parse_prop spec ?? wrong_prop spec "("; 'Tokens.RightPar ?? "Syntax error: missing ')' after proposition">] -> q
-  | [<'Tokens.Symbol s when s = spec.all >] -> spec.taut
-  | [<'Tokens.Symbol s when s = spec.none>] -> spec.cont
-  | [<'Tokens.Symbol s when s = spec.n; q = parse_fact spec ?? wrong_fact spec s>] -> spec.neg q
-  | [<a = spec.atom>] -> a
-
-(* generic functions about strings *)
-(* ------------------------------- *)
-
-let rec split (normalize, separator, stopword) (s : string) = 
-      split2 (normalize, separator, stopword) s 0 "" []
-and split2 (normalize, separator, stopword) s i w ws =
-      if i>=String.length s then addword (normalize, separator, stopword) w ws
-      else if separator s.[i] then split2 (normalize, separator, stopword) s (i+1) "" (addword (normalize, separator, stopword) w ws)
-      else split2 (normalize, separator, stopword) s (i+1) (w ^ String.make 1 s.[i]) ws
-and addword (normalize, separator, stopword) w ws =
-      if w = "" or stopword (normalize w) then ws else w::ws
-

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)

term.old.ml

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

token.ml

-(** Tokens and utility functions. *)
-
-exception Eof
-
-type t =
-    BackQuote | Tilda | Exclam | At | Sharp | Dollar | Percent | Hat | Et | Star
-  | LeftPar | RightPar | Minus | Plus | Equal | LeftAcc | RightAcc | LeftBra | RightBra
-  | Pipe | BackSlash | Slash | Interro | LT | GT | Comma | Dot | Colon | SemiColon
-  | DoubleQuote | Quote
-  | Ident of string
-  | Nat of int
-  | Char of char | String of string | Term of string
-  | PP_tilda | PP_space | PP_cut | PP_break of int * int | PP_newline
-
-(* predicate filtering PP_* tokens *)
-let is_PP = function PP_tilda | PP_space | PP_cut | PP_break _ | PP_newline -> true | _ -> false
-
-(* get the precision of a float number from its writing *)
-let prec_of_sfloat : string -> int =
-  fun s ->
-      let l = String.length s in
-      let i_dot =
-        try String.index s '.'
-        with Not_found -> try String.index s 'e' - 1
-        with Not_found -> l - 1 in
-      let i_e,p =
-        try
-          let i_e = String.index s 'e' in
-          i_e,
-          match s.[i_e+1] with
-          | '+' -> int_of_string (String.sub s (i_e+2) (l-(i_e+2)))
-          | _ -> int_of_string (String.sub s (i_e+1) (l-(i_e+1)))
-        with Not_found -> l, 0 in
-      p - (i_e - (i_dot+1))

tokens.ml

-(** Tokens and utility functions. *)
-
-exception Eof
-
-type t =
-  | Quote | DoubleQuote | BackQuote
-  | Comma | Colon | SemiColon | Dot | Interro | Exclam
-  | LeftPar | RightPar | LeftAcc | RightAcc | LeftBra | RightBra
-  | Nat of int | MinusNat of int
-  | Char of char
-  | String of string
-  | Symbol of string
-  | PP_tilda | PP_space | PP_cut | PP_break of int * int | PP_newline
-
-(* predicate filtering PP_* tokens *)
-let is_PP = function PP_tilda | PP_space | PP_cut | PP_break _ | PP_newline -> true | _ -> false
-
-(* predicate for testing whether a symbol needs quotes *)
-let symbol_needs_quotes s =
-  let is_ident = Str.string_match (Str.regexp "^[A-Za-z_][A-Za-z0-9_]*$") s 0 in
-  let is_op = Str.string_match (Str.regexp "^[-~@#$%^&*+=|\\/><]+$") s 0 in
-  not (is_ident || is_op)
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.