Module Data.TermSource

Sourcetype 'unification_def stuck_goal_kind = ..
Sourceval pp_stuck_goal_kind : 'a -> 'b -> 'c -> unit
Sourceval show_stuck_goal_kind : 'a -> 'b -> string
Sourceval equal_stuck_goal_kind : 'a -> 'b -> 'b -> bool
Sourcetype stuck_goal_kind +=
  1. | Unification of 'unification_def
Sourcetype ttype =
  1. | TConst of Elpi_util.Util.constant
  2. | TApp of Elpi_util.Util.constant * ttype * ttype list
  3. | TPred of bool * (Elpi_util.Util.Mode.t * ttype) list
  4. | TArr of ttype * ttype
  5. | TCData of Elpi_util.Util.CData.t
  6. | TLam of ttype
Sourceval compare_ttype : ttype -> ttype -> Ppx_deriving_runtime.int
Sourcetype builtin_predicate =
  1. | Cut
  2. | And
  3. | Impl
  4. | ImplBang
  5. | RImpl
  6. | Pi
  7. | Sigma
  8. | Eq
  9. | Match
  10. | Findall
  11. | Delay
  12. | Host of Elpi_util.Util.constant
Sourceval builtin_predicates : builtin_predicate list
Sourceval builtin_predicate_max : int
Sourceval func_of_builtin_predicate : (Elpi_util.Util.constant -> F.t) -> builtin_predicate -> F.t
Sourceval show_builtin_predicate : ?table:'a -> (?table:'a -> Elpi_util.Util.constant -> string) -> builtin_predicate -> string
Sourceval const_of_builtin_predicate : builtin_predicate -> Elpi_util.Util.constant
Sourceval is_builtin_predicate : int -> bool
Sourceval builtin_predicate_of_const : int -> builtin_predicate
Sourcetype term =
  1. | Const of Elpi_util.Util.constant
  2. | Lam of term
  3. | App of Elpi_util.Util.constant * term * term list
  4. | Cons of term * term
  5. | Nil
  6. | Discard
  7. | Builtin of builtin_predicate * term list
  8. | CData of Elpi_util.Util.CData.t
  9. | UVar of uvar * int
  10. | AppUVar of uvar * term list
  11. | Arg of int * int
  12. | AppArg of int * term list
Sourceand uvar = {
  1. vardepth : int;
  2. mutable contents : term;
  3. mutable uid_private : int;
}
Sourceval compare_term : term -> term -> Ppx_deriving_runtime.int
Sourceval compare_uvar : uvar -> uvar -> Ppx_deriving_runtime.int
Sourceval cons2tcons : ?loc:Elpi_util.Util.Loc.t -> term -> ttype
Sourceval uvar_id : uvar -> int
Sourceval uvar_is_a_blocker : uvar -> bool
Sourceval uvar_isnt_a_blocker : uvar -> bool
Sourceval uvar_set_blocker : uvar -> unit
Sourceval uvar_unset_blocker : uvar -> unit
Sourcetype clause = {
  1. depth : int;
  2. args : term list;
  3. hyps : term list;
  4. vars : int;
  5. mode : Elpi_util.Util.Mode.hos;
  6. loc : Elpi_util.Util.Loc.t option;
  7. mutable timestamp : int list;
}
Sourceval compare_clause : clause -> clause -> Ppx_deriving_runtime.int
Sourcetype grafting_time = int list
Sourceval compare_times : times -> times -> Ppx_deriving_runtime.int
Sourcetype stuck_goal = {
  1. mutable blockers : blockers;
  2. kind : unification_def stuck_goal_kind;
}
Sourceand blockers = uvar list
Sourceand unification_def = {
  1. adepth : int;
  2. env : term array;
  3. bdepth : int;
  4. a : term;
  5. b : term;
  6. matching : bool;
}
Sourceand clause_src = {
  1. hdepth : int;
  2. hsrc : term;
}
Sourceand prolog_prog = {
  1. src : clause_src list;
  2. index : index;
}
Sourceand clause_list = clause Bl.t
Sourceand first_lvl_idx = {
  1. idx : second_lvl_idx Ptmap.t;
  2. time : int;
  3. times : times;
}
Sourceand second_lvl_idx =
  1. | TwoLevelIndex of {
    1. mode : Elpi_util.Util.Mode.hos;
    2. argno : int;
    3. all_clauses : clause_list;
    4. flex_arg_clauses : clause_list;
    5. arg_idx : clause_list Ptmap.t;
    }
  2. | BitHash of {
    1. mode : Elpi_util.Util.Mode.hos;
    2. args : int list;
    3. args_idx : clause_list Ptmap.t;
    }
  3. | IndexWithDiscriminationTree of {
    1. mode : Elpi_util.Util.Mode.hos;
    2. arg_depths : int list;
    3. args_idx : clause Discrimination_tree.t;
    }
Sourceval stop : bool ref
Sourceval close_index : index -> index
Sourcetype constraints = stuck_goal list
Sourcetype hyps = clause_src list
Sourcetype suspended_goal = {
  1. context : hyps;
  2. goal : int * term;
  3. blockers : blockers;
}
Sourceval mkLam : term -> term
Sourceval mkApp : Elpi_util.Util.constant -> term -> term list -> term
Sourceval mkCons : term -> term -> term
Sourceval mkNil : term
Sourceval mkDiscard : term
Sourceval mkBuiltin : builtin_predicate -> term list -> term
Sourceval mkUVar : uvar -> int -> term
Sourceval mkAppUVar : uvar -> term list -> term
Sourceval mkArg : int -> int -> term
Sourceval mkAppArg : int -> term list -> term
Sourcemodule C : sig ... end
Sourceval oref : depth:int -> term -> uvar
Sourceval (!!) : uvar -> term
Sourcetype env = term array
Sourceval empty_env : 'a array