package elpi

  1. Overview
  2. Docs
ELPI - Embeddable λProlog Interpreter

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (9)

Authors

  1. C
    Claudio Sacerdoti Coen
  2. E
    Enrico Tassi

Maintainers

  1. E
    Enrico Tassi <enrico.tassi@inria.fr>

Sources

elpi-3.0.1.tbz
sha256=af8074c67e94095b25556e1d1e2aaaf0d04c19f373e38919cb8f0a0d6786aae7
sha512=774612085cd3ff267bfd1aa35b7dd2629cde066f9d2393185e28f21d2c86a24c2e36ef1293dee1b2cba37636b6deb6dc6e688cebdb4e2aaff922e06de15dba0a

doc/elpi.runtime/Elpi_runtime/Data/Term/index.html

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_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_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 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_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 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_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