ScopedTerm (p.elpi.3.1.0.doc.elpi.compiler.Elpi_compiler.Compiler

Sourcemodule SimpleTerm : sig ... end

Sourcetype 'scope const = {

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

}

val pp_const : 
  'scope. (Ppx_deriving_runtime.Format.formatter ->
            'scope ->
            Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  'scope const ->
  Ppx_deriving_runtime.unit

Source

val show_const : 
  'scope. (Ppx_deriving_runtime.Format.formatter ->
            'scope ->
            Ppx_deriving_runtime.unit) ->
  'scope const ->
  Ppx_deriving_runtime.string

Source

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

Source

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

Sourceval bind_const : string const -> Scope.t const

Sourceval mk_global_const : name:F.t -> loc:Elpi_util.Util.Loc.t -> Scope.t const

Source

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

Sourceval clone_const : ?clone_scope:('a -> 'a) -> 'a const -> 'a const

Sourcetype spill_info =

| NoInfo
| Main of int
| Phantom of int

Source

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

Sourceval show_spill_info : spill_info -> Ppx_deriving_runtime.string

Sourcetype t_ =

| Impl of SimpleTerm.impl_kind * Elpi_util.Util.Loc.t * t * t
| Discard
| Var of Scope.t const * t list
| App of Scope.t const * t list
| Lam of Scope.language const option * ScopedTypeExpression.e option * t
| CData of Elpi_util.Util.CData.t
| Spill of t * spill_info ref
| Cast of t * ScopedTypeExpression.e

Sourceand t = {

}

Source

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

Sourceval show_t_ : t_ -> Ppx_deriving_runtime.string

Source

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

Sourceval show : t -> Ppx_deriving_runtime.string

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

Source

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

Sourceval build_infix_constant : Scope.t 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

Source

val pretty_lam : 
  Format.formatter ->
  Scope.language const 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:bool -> 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