Runtime (p.elpi.3.0.0.doc.elpi.runtime.Elpi

Sourcemodule Pp : sig ... end

val pp_stuck_goal : 
  ?pp_ctx:Data.pp_ctx ->
  Elpi_runtime.Data.Fmt.formatter ->
  Data.stuck_goal ->
  unit

Source

val execute_once : 
  ?max_steps:int ->
  ?delay_outside_fragment:bool ->
  Data.executable ->
  'a Data.outcome

Source

val execute_loop : 
  ?delay_outside_fragment:bool ->
  Data.executable ->
  more:(unit -> bool) ->
  pp:(float -> 'a Data.outcome -> unit) ->
  unit

Source

val deref_uv : 
  ?avoid:Data.uvar_body ->
  from:Elpi_util.Util.constant ->
  to_:Elpi_util.Util.constant ->
  int ->
  Data.term ->
  Data.term

Source

val deref_appuv : 
  ?avoid:Data.uvar_body ->
  from:Elpi_util.Util.constant ->
  to_:Elpi_util.Util.constant ->
  Data.term list ->
  Data.term ->
  Data.term

Sourceval deref_head : depth:int -> Data.term -> Data.term

Sourceval eta_contract_flex : depth:int -> Data.term -> Data.term option

Sourceval is_flex : depth:int -> Data.term -> Data.uvar_body option

Sourceval expand_uv : depth:int -> Data.uvar_body -> lvl:int -> ano:int -> Data.term

Source

val expand_appuv : 
  depth:int ->
  Data.uvar_body ->
  lvl:int ->
  args:Data.term list ->
  Data.term

Sourceval lp_list_to_list : depth:int -> Data.term -> Data.term list

Sourceval list_to_lp_list : Data.term list -> Data.term

Sourceval split_conj : depth:int -> Data.term -> Data.term list

Sourceval mkinterval : int -> int -> int -> Data.term list

Sourceval mkConst : Elpi_util.Util.constant -> Data.term

Sourceval mkAppL : Elpi_util.Util.constant -> Data.term list -> Data.term

Sourceval mkAppArg : int -> int -> Data.term list -> Data.term

Source

val move : 
  argsdepth:int ->
  Data.env ->
  ?avoid:Data.uvar_body ->
  from:int ->
  to_:int ->
  Data.term ->
  Data.term

Source

val hmove : 
  ?avoid:Data.uvar_body ->
  from:int ->
  to_:int ->
  Data.term ->
  Data.term

Sourceval subst : depth:int -> Data.term list -> Data.term -> Data.term

Source

val get_suspended_goal : 
  Data.blockers ->
  'a Data.stuck_goal_kind ->
  Data.suspended_goal option

Sourceval full_deref : depth:int -> Data.term -> Data.term

Sourceval lex_insertion : int list -> int list -> int

Sourcemodule CompileTime : sig ... end

Sourcemodule Indexing : sig ... end