package term-indexing

You can search for identifiers within the package.

in-package search v0.2.0

term-indexing
- Term_indexing
  - Int_option
  - Intf
    
    Hashed
    
    Map
    
    Pattern
    
    Signature
    
    Subst
    
    Unification
    
    Term
    
    Term_core
    
    Term_index
  - Make
    
    Index
    
    P
    
    Path
    
    Pattern
    
    Subst
    
    Unification
    
    Term
  - Path
  - Pattern
    
    Make
    
    P
    
    T
    
    Make_raw
    
    P
    
    T
    
    Make_with_hash_consing
    
    P
    
    T
  - Subst
    
    Make
    
    M
    
    P
    
    T
    
    Unification
  - Term
    
    Default_map
    
    Make_hash_consed
    
    M
    
    P
  - Term_index
    
    IRef
    
    IS
    
    Make
    
    Internal_for_tests
    
    P
    
    S
    
    Unification
    
    T

Legend:
Library
Module
Module type
Parameter
Class
Class type

exception Invalid_pattern

type focused =

| Focused

val _focused : focused

type unfocused =

| Unfocused

val _unfocused : unfocused

type 'f focus_tag =

| Focused_tag : focused focus_tag
| Unfocused_tag : unfocused focus_tag

type ('f1, 'f2, 'f) join =

| UU : (unfocused, unfocused, unfocused) join
| FU : (focused, unfocused, focused) join
| UF : (unfocused, focused, focused) join
| FF : (focused, focused, focused) join

type (_, _) pattern_desc =

| Patt_prim : 'p prim_pred * ('p, 'f) pattern_list -> ('p, 'f) pattern_desc
| Patt_var : int -> ('p, unfocused) pattern_desc
| Patt_any : ('p, unfocused) pattern_desc
| Patt_focus : ('p, unfocused) pattern -> ('p, focused) pattern_desc

and ('p, 'f) pattern = {

patt_desc : ('p, 'f) pattern_desc;
patt_uid : int;

}

and (_, _) pattern_list =

| Patt_list_empty : ('p, unfocused) pattern_list
| Patt_list_any : ('p, unfocused) pattern_list
| Patt_list_cons : ('p, 'f1) pattern * ('p, 'f2) pattern_list * ('f1, 'f2, 'f) join -> ('p, 'f) pattern_list

and 'p prim_pred =

| Patt_prim_equal of 'p
| Patt_pred of 'p -> bool

val get_focus : 'f. ('p, 'f) pattern -> 'f focus_tag

val get_focus_list : 'f. ('p, 'f) pattern_list -> 'f focus_tag

module Make_raw
  (P : Intf.Signature)
  (T : Intf.Term with type prim = P.t and type t = P.t Term.term) : 
  sig ... end

module Make
  (P : Intf.Signature)
  (T : Intf.Term with type prim = P.t and type t = P.t Term.term) : 
  Intf.Pattern
    with type prim = P.t
     and type path = Path.t
     and type term = P.t Term.term

module Make_with_hash_consing
  (P : Intf.Signature)
  (T : Intf.Term with type prim = P.t and type t = P.t Term.term) : 
  sig ... end