package logtk

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Some helpers

package logtk

logtk
- Logtk
- LogtkCache
  - Dummy
    
    X
  - Dummy2
    
    X
    
    Y
  - EQ
  - HASH
  - LRU
    
    X
  - Linear
    
    X
  - Linear2
    
    X
    
    Y
  - Replacing
    
    X
  - Replacing2
    
    X
    
    Y
  - S
  - S2
- LogtkCnf
- LogtkComparison
  - PARTIAL_ORD
- LogtkCongruence
  - FO
  - HO
  - Make
    
    T
  - S
  - TERM
- LogtkDBEnv
- LogtkDtree
  - Default
  - Make
    
    E
- LogtkFOTerm
  - AC
    
    A
  - AC_SPEC
  - Classic
  - Map
  - Pos
  - Seq
  - Set
  - T2LogtkCache
  - TLogtkCache
  - TPTP
    
    Arith
  - Tbl
- LogtkFastFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFeatureVector
  - Make
    
    C
    
    Feature
- LogtkFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFormula
  - FO
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Make
    
    Base
    
    Map
    
    MyT
    
    Seq
    
    Set
    
    TPTP
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Map
    
    From
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
    
    To
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - S
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - TERM
    
    Seq
    
    Set
    
    TPTP
- LogtkFormulaShape
- LogtkHORewriting
  - Seq
- LogtkHOTerm
  - LogtkCache
  - Map
  - Pos
  - Seq
  - Set
  - TPTP
  - Tbl
  - any_visitor
  - id_visitor
- LogtkHashcons
  - HashedLogtkType
  - Make
    
    H
    
    X
  - S
    
    H
- LogtkIArray
  - Seq
- LogtkIndex
  - BasicEquation
  - CLAUSE
  - EQUATION
  - LEAF
  - MakeLeaf
    
    X
  - SUBSUMPTION_IDX
    
    C
  - TERM_IDX
    
    Leaf
  - UNIT_IDX
    
    E
- LogtkInterfaces
  - EQ
  - GROUP
  - HASH
  - ITER
  - MONOID
  - ORD
  - PRINT
  - PRINT1
  - PRINT_DE_BRUIJN
  - PRINT_OVERLOAD
- LogtkLambda
- LogtkLazyGraph
  - Dot
  - Full
  - Heap
  - Infix
  - Mutable
- LogtkLazyList
- LogtkMultiset
  - Make
    
    Seq
    
    X
  - S
    
    Seq
- LogtkNPDtree
  - Make
    
    E
  - MakeTerm
    
    Leaf
    
    X
- LogtkOptions
- LogtkOrdering
  - Default
  - Make
    
    P
    
    Constr
    
    Seq
- LogtkOrdering_intf
  - S
    
    Prec
    
    Constr
    
    Seq
- LogtkParseLocation
- LogtkPartialOrder
  - ELEMENT
  - Make
    
    E
- LogtkPartialOrder_intf
  - S
- LogtkPosition
  - Build
- LogtkPrecedence
  - Constr
  - Default
    
    Constr
    
    Seq
  - Make
    
    Constr
    
    Seq
    
    Sym
  - SYMBOL
  - Seq
- LogtkPrecedence_intf
  - S
    
    Constr
    
    Seq
- LogtkPrologTerm
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
  - id_visitor
  - visitor
- LogtkRewriting
  - FormRW
  - MakeOrdered
    
    E
  - MakeTRS
    
    I
    
    E
  - ORDERED
    
    E
  - SIG_TRS
  - TRS
- LogtkScopedTerm
  - DB
  - Kind
  - Map
  - Pos
  - Seq
  - Set
  - Tbl
- LogtkSignature
  - SMap
  - Seq
  - TPTP
    
    Arith
- LogtkSkolem
- LogtkSourced
- LogtkSubsts
  - FO
  - Form
  - HO
  - Renaming
  - SPECIALIZED
  - Ty
- LogtkSymbol
  - ArithOp
  - Base
  - Map
  - Seq
  - Set
  - TPTP
    
    Arith
  - Tbl
- LogtkTransform
  - DAG
    
    Form
  - FORM
  - FormDag
    
    Form
  - MakeDAG
    
    Form
- LogtkType
  - Conv
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
- LogtkTypeInference
  - Closure
  - Ctx
  - FO
  - HO
  - S
- LogtkTypedPrologTerm
  - Map
  - Seq
  - Set
  - Subst
  - Tbl
  - Visitor
- LogtkUnif
  - FO
  - Form
  - HO
  - NARY
  - Nary
  - Ty
  - UNARY
  - Unary
- LogtkUtil
  - Exn
  - Flag
  - Section

Legend:
Library
Module
Module type
Parameter
Class
Class type

Some helpers

Time facilities

val get_total_time : unit -> float

time elapsed since start of program

val get_start_time : unit -> float

time at which the program started

Misc

module Section : sig ... end

Debug section

val set_debug : int -> unit

Set debug level of Section.root

val get_debug : unit -> int

Set debug level of Section.root

Current debug level for Section.root

val need_cleanup : bool Pervasives.ref

Current debug level for Section.root

Cleanup line before printing?

val debug : 
  ?section:Section.t ->
  int ->
  ('a, Buffer.t, unit, unit) Pervasives.format4 ->
  'a

Print a debug message, with the given section and verbosity level. The message might be dropped if its level is too high. NOTE: non-thread safe

val debugf : 
  ?section:Section.t ->
  int ->
  ('a, Format.formatter, unit, unit) Pervasives.format4 ->
  'a

Same as debug but using Format. Makes multi-line printing easier.

val pp_pos : Lexing.position -> string

val set_memory_limit : int -> unit

Limit the amount of memory available to the process (in MB)

val set_time_limit : int -> unit

Limit the CPU time available to the process (in seconds)

OCaml Stack

requires ocaml >= 4.01

since 0.8

module Exn : sig ... end

profiling facilities

type profiler

val enable_profiling : bool Pervasives.ref

Enable/disable profiling

val mk_profiler : string -> profiler

Enable/disable profiling

Create a named profiler

val enter_prof : profiler -> unit

Create a named profiler

Enter the profiler

val exit_prof : profiler -> unit

Enter the profiler

Exit the profiler

val yield_prof : profiler -> unit

Exit the profiler

Yield control to sub-call

Runtime statistics

type stat

val mk_stat : string -> stat

val print_global_stats : unit -> unit

val incr_stat : stat -> unit

val add_stat : stat -> int -> unit

Flags as integers

module Flag : sig ... end

LogtkOrdering utils

val lexicograph : ('a -> 'b -> int) -> 'a list -> 'b list -> int

lexicographic order on lists l1,l2 which elements are ordered by f

val lexicograph_combine : int list -> int

combine comparisons by lexicographic order

val opposite_order : ('a -> 'b -> int) -> 'a -> 'b -> int

the opposite order, that sorts elements the opposite way

String utils

val str_sub : sub:string -> int -> string -> int -> bool

Equality from the given start position

val str_split : by:string -> string -> string list

val str_find : ?start:int -> sub:string -> string -> int

Find sub in the string, returns its first index or -1

val str_repeat : string -> int -> string

The same char, repeated n times

val str_prefix : pre:string -> string -> bool

str_prefix ~pre s returns true iff pre is a prefix of s

Exceptions

val finally : h:(unit -> unit) -> f:(unit -> 'a) -> 'a

finally h f calls f () and returns its result. If it raises, the same exception is raised; in any case, h () is called after f () terminates.

File utils

val with_lock_file : string -> (unit -> 'a) -> 'a

perform the action with a lock on the given file

val with_input : string -> (Pervasives.in_channel -> 'a) -> 'a option

Open the given file for reading, and returns the result of the action applied to the input channel

val with_output : string -> (Pervasives.out_channel -> 'a) -> 'a option

Open the given file for writing, and returns the result of the action applied to the output channel

val slurp : Pervasives.in_channel -> string

Read the whole filedescriptor into a string

type 'a or_error = [

| `Error of string
| `Ok of 'a

]

val popen : cmd:string -> input:string -> string or_error

Run the given command cmd with the given input, wait for it to terminate, and return its stdout.

Printing utils

val sprintf : ('a, Buffer.t, unit, string) Pervasives.format4 -> 'a

print into a string

val fprintf : 
  Pervasives.out_channel ->
  ('a, Buffer.t, unit, unit) Pervasives.format4 ->
  'a

val printf : ('a, Buffer.t, unit, unit) Pervasives.format4 -> 'a

val eprintf : ('a, Buffer.t, unit, unit) Pervasives.format4 -> 'a

val on_buffer : (Buffer.t -> 'a -> unit) -> 'a -> string

val pp_pair : 
  ?sep:string ->
  (Buffer.t -> 'a -> unit) ->
  (Buffer.t -> 'b -> unit) ->
  Buffer.t ->
  ('a * 'b) ->
  unit

val pp_opt : (Buffer.t -> 'a -> unit) -> Buffer.t -> 'a option -> unit

val pp_list : 
  ?sep:string ->
  (Buffer.t -> 'a -> unit) ->
  Buffer.t ->
  'a list ->
  unit

print a list of items using the printing function

val pp_array : 
  ?sep:string ->
  (Buffer.t -> 'a -> unit) ->
  Buffer.t ->
  'a array ->
  unit

print an array of items with printing function

val pp_arrayi : 
  ?sep:string ->
  (Buffer.t -> int -> 'a -> unit) ->
  Buffer.t ->
  'a array ->
  unit

print an array, giving the printing function both index and item

val pp_seq : 
  ?sep:string ->
  (Buffer.t -> 'a -> unit) ->
  Buffer.t ->
  'a Sequence.t ->
  unit

Print the sequence