package elpi

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

Install 

dune-project
 Dependency

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

Authors

  1. C
    Claudio Sacerdoti Coen
  2. E
    Enrico Tassi

Maintainers

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

Sources

elpi-2.0.6.tbz
sha256=b515185d0674557ae3219059d6c91dce2794b30c38ad23447b98a4fa22a99375
sha512=48490035f8dc103de9c0f2bf4e3a3ea6db2bda8670efe87bc2402a3b47e5c510452a5ae406be65a83fe16dd410c374894142bbee477681e50fc0dde4b8153d3c

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