package elpi

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

Install 

dune-project
 Dependency

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

Authors

  1. C
    Claudio Sacerdoti Coen
  2. E
    Enrico Tassi

Maintainers

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

Sources

elpi-3.7.1.tbz
sha256=0109f44fd6c08f5eed01c559765dcf4e3e2b8b47c25d026f0153757459f5f466
sha512=62fb7bce9d8d0505458b9686a9ab112f4f988ab6e2051bb623d53308f175abd72ed74c8962e5469380ec989b80c58a77b31c8bbfb7e8b2b60953b11b436f6647

doc/elpi.compiler/Elpi_compiler/Compiler_data/ScopedTerm/index.html

Module Compiler_data.ScopedTermSource

Sourcemodule SimpleTerm : sig ... end
Sourcetype 'scope w_ty_loc = {
  1. scope : 'scope;
  2. name : F.t;
  3. ty : TypeAssignment.t MutableOnce.t;
  4. loc : Elpi_util.Util.Loc.t;
}
Sourcetype const = Scope.t w_ty_loc
Sourcetype uvar = unit w_ty_loc
Sourcetype binder = string w_ty_loc
Sourceval mk_w_ty_loc : ?ty:??? -> scope:'a -> F.t -> loc:Elpi_util.Util.Loc.t -> 'a w_ty_loc
Sourceval mk_global_const : ?ty:??? -> ?escape_ns:??? -> loc:Elpi_util.Util.Loc.t -> F.t -> const
Sourceval mk_bound_const : ?ty:??? -> lang:Scope.language -> F.t -> loc:Elpi_util.Util.Loc.t -> Scope.t w_ty_loc
Sourceval mk_uvar : ?ty:??? -> F.t -> loc:Elpi_util.Util.Loc.t -> unit w_ty_loc
Sourceval mk_binder : ?ty:??? -> lang:'a -> F.t -> loc:Elpi_util.Util.Loc.t -> 'a w_ty_loc
Sourceval bind_const : binder -> const
Sourceval const_of_symb : types:TypingEnv.t -> Symbol.t -> loc:Elpi_util.Util.Loc.t -> const
Sourceval clone_const : ?clone_scope:??? -> 'a w_ty_loc -> 'a w_ty_loc
Sourcetype spill_info =
  1. | NoInfo
  2. | Main of int
  3. | Phantom of int
Sourcetype t_ =
  1. | Impl of SimpleTerm.impl_kind * Elpi_util.Util.Loc.t * t * t
  2. | Discard of {
    1. mutable heapify : bool;
    }
  3. | UVar of uvar * t list
  4. | App of const * t list
  5. | Lam of binder option * ScopedTypeExpression.e option * t
  6. | CData of Elpi_util.Util.CData.t
  7. | Spill of t * spill_info ref
  8. | Cast of t * ScopedTypeExpression.e
Sourceval pp_t_ : Ppx_deriving_runtime.Format.formatter -> t_ -> Ppx_deriving_runtime.unit
Sourceval show_t_ : t_ -> Ppx_deriving_runtime.string
Sourceval mkGlobalApp : ?ty:??? -> ?escape_ns:??? -> loc:Elpi_util.Util.Loc.t -> F.t -> t list -> t_
Sourceval mkBoundApp : ?ty:??? -> lang:Scope.language -> loc:Elpi_util.Util.Loc.t -> F.t -> t list -> t_
Sourceval mkUVar : ?ty:??? -> loc:Elpi_util.Util.Loc.t -> F.t -> t list -> t_
Sourceval type_of : t -> TypeAssignment.ty
Sourceval lam : int
Sourceval app : int
Sourceval lvl_of : t_ -> int
Sourceval get_lam_name : (F.t * 'a) option -> F.t
Sourceval mk_empty_lam_type : (F.t * Elpi_util.Util.Loc.t * 'a) option -> 'a w_ty_loc option
Sourceval build_infix_constant : const -> Elpi_util.Util.Loc.t -> t
Sourceval is_infix_constant : F.t -> bool
Sourceval intersperse : (Elpi_util.Util.Loc.t -> t) -> t list -> t list
Sourceval pretty_lam : Format.formatter -> binder option -> ScopedTypeExpression.e option -> t -> unit
Sourceval pretty : Format.formatter -> t -> unit
Sourceval pretty_ : Format.formatter -> t_ -> unit
Sourceval pretty_parens : lvl:int -> Format.formatter -> t -> unit
Sourceval pretty_parens_lam : lvl:int -> Format.formatter -> t -> unit
Sourceval equal : TypingEnv.t -> ?types:??? -> t -> t -> bool
Sourceval compare : 'a -> 'b -> 'c
Sourceval in_scoped_term : t -> Elpi_util.Util.CData.t
Sourceval out_scoped_term : Elpi_util.Util.CData.t -> t
Sourceval is_scoped_term : Elpi_util.Util.CData.t -> bool
Sourceval of_simple_term : loc:Elpi_util.Util.Loc.t -> SimpleTerm.t_ -> t_
Sourceval of_simple_term_loc : SimpleTerm.t -> t
Sourceval unlock : t -> t_
Sourceval fresh : unit -> F.t
Sourceval rename : Scope.language -> F.t -> F.t -> t_ -> t_
Sourceval rename_loc : Scope.language -> F.t -> F.t -> t -> t
Sourceval clone_loc : loc:Elpi_util.Util.Loc.t -> t -> t
Sourceval clone : loc:Elpi_util.Util.Loc.t -> t_ -> t_
Sourceval beta : t -> t list -> t_
Sourcemodule QTerm : sig ... end
Sourceval is_var : t_ -> bool