package elpi

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

Install

Dune Dependency

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

Authors

  1. C
    Claudio Sacerdoti Coen
  2. E
    Enrico Tassi

Maintainers

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

Sources

elpi-2.0.7.tbz
sha256=80233ebd92babd696148ed553238961ec7b6de6bf157045aae1c7090840aeded
sha512=00c9ec01fabde9db1de4a58cb37480035e6f926d83b8360553419bcb99e9199f0720dde975f97ac9942ce528884d3d59d025cfbd471f12d57547429f15684d49

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

Module Elpi_runtime.DataSource

Sourcemodule Fmt = Format
Sourcemodule Term : sig ... end
include module type of struct include Term end
Sourcetype 'unification_def stuck_goal_kind = 'unification_def Term.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 arg_mode = Elpi_util.Util.arg_mode =
  1. | Input
  2. | Output
Sourceval compare_arg_mode : arg_mode -> arg_mode -> Ppx_deriving_runtime.int
Sourcetype mode_aux = Elpi_util.Util.mode_aux =
  1. | Fo of arg_mode
  2. | Ho of arg_mode * mode
Sourceand mode = mode_aux list
Sourceval compare_mode_aux : mode_aux -> mode_aux -> Ppx_deriving_runtime.int
Sourceval compare_mode : mode -> mode -> Ppx_deriving_runtime.int
Sourcetype ttype = Term.ttype =
  1. | TConst of Elpi_util.Util.constant
  2. | TApp of Elpi_util.Util.constant * ttype * ttype list
  3. | TPred of bool * (arg_mode * 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 term = Term.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 Elpi_util.Util.constant * 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 = Term.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 = Term.clause = {
  1. depth : int;
  2. args : term list;
  3. hyps : term list;
  4. vars : int;
  5. mode : mode;
  6. loc : Elpi_util.Util.Loc.t option;
  7. mutable timestamp : int list;
}
Sourceval compare_clause : clause -> clause -> Ppx_deriving_runtime.int
Sourceval get_arg_mode : mode_aux -> arg_mode
Sourceval to_mode : bool -> mode_aux
Sourcetype grafting_time = int list
Sourceval compare_times : times -> times -> Ppx_deriving_runtime.int
Sourcetype stuck_goal = Term.stuck_goal = {
  1. mutable blockers : blockers;
  2. kind : unification_def stuck_goal_kind;
}
Sourceand blockers = uvar_body list
Sourceand unification_def = Term.unification_def = {
  1. adepth : int;
  2. env : term array;
  3. bdepth : int;
  4. a : term;
  5. b : term;
  6. matching : bool;
}
Sourceand clause_src = Term.clause_src = {
  1. hdepth : int;
  2. hsrc : term;
}
Sourceand prolog_prog = Term.prolog_prog = {
  1. src : clause_src list;
  2. index : index;
}
Sourceand clause_list = clause Bl.t
Sourceand first_lvl_idx = Term.first_lvl_idx = {
  1. idx : second_lvl_idx Ptmap.t;
  2. time : int;
  3. times : times;
}
Sourceand second_lvl_idx = Term.second_lvl_idx =
  1. | TwoLevelIndex of {
    1. mode : mode;
    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 : mode;
    2. args : int list;
    3. args_idx : clause_list Ptmap.t;
    }
  3. | IndexWithDiscriminationTree of {
    1. mode : mode;
    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 = Term.suspended_goal = {
  1. context : hyps;
  2. goal : int * term;
}
Sourcetype indexing = Term.indexing =
  1. | MapOn of int
  2. | Hash of int list
  3. | DiscriminationTree of int list

Used to index the parameters of a predicate P

  • MapOn N -> N-th argument at depth 1 (head symbol only)
  • Hash L -> L is the list of depths given by the urer for the parameters of P. Indexing is done by hashing all the parameters with a non zero depth and comparing it with the hashing of the parameters of the query
  • DiscriminationTree L -> we use the same logic of Hash, except we use DiscriminationTree to discriminate clauses
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 : Elpi_util.Util.constant -> 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 = Term.C
Sourceval oref : term -> uvar_body
Sourceval (!!) : uvar_body -> term
Sourcetype env = term array
Sourceval empty_env : 'a array
Sourcemodule State : sig ... end
Sourceval elpi_state_descriptor : State.descriptor
Sourcemodule Global_symbols : sig ... end
Sourceval dummy : term
Sourceval dummy_uvar_body : uvar_body
Sourcemodule CHR : sig ... end
Sourcetype clause_w_info = {
  1. clloc : Elpi_util.Util.CData.t;
  2. clargsname : string list;
  3. clbody : clause;
}
Sourceexception No_clause
Sourceexception No_more_steps
Sourcemodule Conversion : sig ... end
Sourcemodule ContextualConversion : sig ... end
Sourceval while_compiling : bool State.component
Sourcemodule HoasHooks : sig ... end
Sourcemodule CalcHooks : sig ... end
Sourcemodule BuiltInPredicate : sig ... end
Sourcetype symbol_table = {
  1. mutable c2s : string Elpi_util.Util.Constants.Map.t;
  2. c2t : (Elpi_util.Util.constant, term) Elpi_util.Util.Hashtbl.t;
  3. mutable frozen_constants : int;
}
Sourcetype executable = {
  1. compiled_program : prolog_prog;
  2. chr : CHR.t;
  3. initial_depth : int;
  4. initial_goal : term;
  5. initial_runtime_state : State.t;
  6. symbol_table : symbol_table;
  7. builtins : BuiltInPredicate.builtin_table;
  8. assignments : term Elpi_util.Util.StrMap.t;
}
Sourcetype pp_ctx = {
  1. uv_names : (string Elpi_util.Util.IntMap.t * int) ref;
  2. table : symbol_table;
}
Sourcetype solution = {
  1. assignments : term Elpi_util.Util.StrMap.t;
  2. constraints : constraints;
  3. state : State.t;
  4. pp_ctx : pp_ctx;
  5. state_for_relocation : int * symbol_table;
}
Sourcetype 'a outcome =
  1. | Success of solution
  2. | Failure
  3. | NoMoreSteps
Sourceexception CannotDeclareClauseForBuiltin of Elpi_util.Util.Loc.t option * Elpi_util.Util.constant
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