ScopedTerm (u.c73734534e52e3c7e3a6ab4ddda12c49.elpi.3.4.5.doc.elpi.compiler.Elpi_compiler.Compiler

module SimpleTerm : sig ... end

type 'scope w_ty_loc = {

scope : 'scope;
name : F.t;
ty : TypeAssignment.t MutableOnce.t;
loc : Elpi_util.Util.Loc.t;

}

val pp_w_ty_loc : 
  'scope. (Ppx_deriving_runtime.Format.formatter ->
            'scope ->
            Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  'scope w_ty_loc ->
  Ppx_deriving_runtime.unit

val show_w_ty_loc : 
  'scope. (Ppx_deriving_runtime.Format.formatter ->
            'scope ->
            Ppx_deriving_runtime.unit) ->
  'scope w_ty_loc ->
  Ppx_deriving_runtime.string

type const = Scope.t w_ty_loc

val pp_const : 
  Ppx_deriving_runtime.Format.formatter ->
  const ->
  Ppx_deriving_runtime.unit

val show_const : const -> Ppx_deriving_runtime.string

type uvar = unit w_ty_loc

val pp_uvar : 
  Ppx_deriving_runtime.Format.formatter ->
  uvar ->
  Ppx_deriving_runtime.unit

val show_uvar : uvar -> Ppx_deriving_runtime.string

type binder = string w_ty_loc

val pp_binder : 
  Ppx_deriving_runtime.Format.formatter ->
  binder ->
  Ppx_deriving_runtime.unit

val show_binder : binder -> Ppx_deriving_runtime.string

val mk_w_ty_loc : 
  ?ty:TypeAssignment.t MutableOnce.t ->
  scope:'a ->
  F.t ->
  loc:Elpi_util.Util.Loc.t ->
  'a w_ty_loc

val mk_global_const : 
  ?ty:TypeAssignment.t MutableOnce.t ->
  ?escape_ns:bool ->
  loc:Elpi_util.Util.Loc.t ->
  F.t ->
  const

val mk_bound_const : 
  ?ty:TypeAssignment.t MutableOnce.t ->
  lang:Scope.language ->
  F.t ->
  loc:Elpi_util.Util.Loc.t ->
  Scope.t w_ty_loc

val mk_uvar : 
  ?ty:TypeAssignment.t MutableOnce.t ->
  F.t ->
  loc:Elpi_util.Util.Loc.t ->
  unit w_ty_loc

val mk_binder : 
  ?ty:TypeAssignment.t MutableOnce.t ->
  lang:'a ->
  F.t ->
  loc:Elpi_util.Util.Loc.t ->
  'a w_ty_loc

val bind_const : binder -> const

val const_of_symb : 
  types:TypingEnv.t ->
  Symbol.t ->
  loc:Elpi_util.Util.Loc.t ->
  const

val clone_const : ?clone_scope:('a -> 'a) -> 'a w_ty_loc -> 'a w_ty_loc

type spill_info =

| NoInfo
| Main of int
| Phantom of int

val pp_spill_info : 
  Ppx_deriving_runtime.Format.formatter ->
  spill_info ->
  Ppx_deriving_runtime.unit

val show_spill_info : spill_info -> Ppx_deriving_runtime.string

type t_ =

| Impl of SimpleTerm.impl_kind * Elpi_util.Util.Loc.t * t * t
| Discard of {
1. mutable heapify : bool;
}
| UVar of uvar * t list
| App of const * t list
| Lam of binder option * ScopedTypeExpression.e option * t
| CData of Elpi_util.Util.CData.t
| Spill of t * spill_info ref
| Cast of t * ScopedTypeExpression.e

and t = {

}

val pp_t_ : 
  Ppx_deriving_runtime.Format.formatter ->
  t_ ->
  Ppx_deriving_runtime.unit

val show_t_ : t_ -> Ppx_deriving_runtime.string

val pp : 
  Ppx_deriving_runtime.Format.formatter ->
  t ->
  Ppx_deriving_runtime.unit

val show : t -> Ppx_deriving_runtime.string

val mkGlobalApp : 
  ?ty:TypeAssignment.t MutableOnce.t ->
  ?escape_ns:bool ->
  loc:Elpi_util.Util.Loc.t ->
  F.t ->
  t list ->
  t_

val mkBoundApp : 
  ?ty:TypeAssignment.t MutableOnce.t ->
  lang:Scope.language ->
  loc:Elpi_util.Util.Loc.t ->
  F.t ->
  t list ->
  t_

val mkUVar : 
  ?ty:TypeAssignment.t MutableOnce.t ->
  loc:Elpi_util.Util.Loc.t ->
  F.t ->
  t list ->
  t_

val type_of : t -> TypeAssignment.ty

val lam : int

val app : int

val lvl_of : t_ -> int

val get_lam_name : (F.t * 'a) option -> F.t

val mk_empty_lam_type : 
  (F.t * Elpi_util.Util.Loc.t * 'a) option ->
  'a w_ty_loc option

val build_infix_constant : const -> Elpi_util.Util.Loc.t -> t

val is_infix_constant : F.t -> bool

val intersperse : (Elpi_util.Util.Loc.t -> t) -> t list -> t list

val pretty_lam : 
  Format.formatter ->
  binder option ->
  ScopedTypeExpression.e option ->
  t ->
  unit

val pretty : Format.formatter -> t -> unit

val pretty_ : Format.formatter -> t_ -> unit

val pretty_parens : lvl:int -> Format.formatter -> t -> unit

val pretty_parens_lam : lvl:int -> Format.formatter -> t -> unit

val equal : TypingEnv.t -> ?types:bool -> t -> t -> bool

val compare : 'a -> 'b -> 'c

val in_scoped_term : t -> Elpi_util.Util.CData.t

val out_scoped_term : Elpi_util.Util.CData.t -> t

val is_scoped_term : Elpi_util.Util.CData.t -> bool

val of_simple_term : loc:Elpi_util.Util.Loc.t -> SimpleTerm.t_ -> t_

val of_simple_term_loc : SimpleTerm.t -> t

val unlock : t -> t_

val fresh : unit -> F.t

val rename : Scope.language -> F.t -> F.t -> t_ -> t_

val rename_loc : Scope.language -> F.t -> F.t -> t -> t

val clone_loc : loc:Elpi_util.Util.Loc.t -> t -> t

val clone : loc:Elpi_util.Util.Loc.t -> t_ -> t_

val beta : t -> t list -> t_

module QTerm : sig ... end

val is_var : t_ -> bool