package elpi

  1. Overview
  2. Docs
package elpi
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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 pp_ttype : Ppx_deriving_runtime.Format.formatter -> ttype -> Ppx_deriving_runtime.unit
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 pp_builtin_predicate : Ppx_deriving_runtime.Format.formatter -> builtin_predicate -> Ppx_deriving_runtime.unit
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_body * int * int
  10. | AppUVar of uvar_body * int * term list
  11. | Arg of int * int
  12. | AppArg of int * term list
Sourceand uvar_body = {
  1. mutable contents : term;
  2. mutable uid_private : int;
}
Sourceval pp_term : Ppx_deriving_runtime.Format.formatter -> term -> Ppx_deriving_runtime.unit
Sourceval pp_uvar_body : Ppx_deriving_runtime.Format.formatter -> uvar_body -> Ppx_deriving_runtime.unit
Sourceval show_uvar_body : uvar_body -> Ppx_deriving_runtime.string
Sourceval compare_term : term -> term -> Ppx_deriving_runtime.int
Sourceval compare_uvar_body : uvar_body -> uvar_body -> Ppx_deriving_runtime.int
Sourceval cons2tcons : ?loc:Elpi_util.Util.Loc.t -> term -> ttype
Sourceval uvar_id : uvar_body -> int
Sourceval uvar_is_a_blocker : uvar_body -> bool
Sourceval uvar_isnt_a_blocker : uvar_body -> bool
Sourceval uvar_set_blocker : uvar_body -> unit
Sourceval uvar_unset_blocker : uvar_body -> 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 pp_clause : Ppx_deriving_runtime.Format.formatter -> clause -> Ppx_deriving_runtime.unit
Sourceval compare_clause : clause -> clause -> Ppx_deriving_runtime.int
Sourcetype grafting_time = int list
Sourceval pp_grafting_time : Ppx_deriving_runtime.Format.formatter -> grafting_time -> Ppx_deriving_runtime.unit
Sourceval pp_times : Ppx_deriving_runtime.Format.formatter -> times -> Ppx_deriving_runtime.unit
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_body 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 pp_stuck_goal : Ppx_deriving_runtime.Format.formatter -> stuck_goal -> Ppx_deriving_runtime.unit
Sourceval pp_blockers : Ppx_deriving_runtime.Format.formatter -> blockers -> Ppx_deriving_runtime.unit
Sourceval pp_unification_def : Ppx_deriving_runtime.Format.formatter -> unification_def -> Ppx_deriving_runtime.unit
Sourceval pp_clause_src : Ppx_deriving_runtime.Format.formatter -> clause_src -> Ppx_deriving_runtime.unit
Sourceval pp_prolog_prog : Ppx_deriving_runtime.Format.formatter -> prolog_prog -> Ppx_deriving_runtime.unit
Sourceval pp_clause_list : Ppx_deriving_runtime.Format.formatter -> clause_list -> Ppx_deriving_runtime.unit
Sourceval pp_index : Ppx_deriving_runtime.Format.formatter -> index -> Ppx_deriving_runtime.unit
Sourceval pp_first_lvl_idx : Ppx_deriving_runtime.Format.formatter -> index -> Ppx_deriving_runtime.unit
Sourceval pp_second_lvl_idx : Ppx_deriving_runtime.Format.formatter -> second_lvl_idx -> Ppx_deriving_runtime.unit
Sourceval stop : bool Stdlib.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_body -> int -> int -> term
Sourceval mkAppUVar : uvar_body -> int -> term list -> term
Sourceval mkArg : int -> int -> term
Sourceval mkAppArg : int -> term list -> term
Sourcemodule C : sig ... end
Sourceval oref : term -> uvar_body
Sourceval (!!) : uvar_body -> term
Sourcetype env = term array
Sourceval empty_env : 'a array
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct