Module `Elpi_runtime.Runtime`Source

Sourcemodule Pp : sig ... end

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

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

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

Sourceval deref_uv : ?avoid:Data.uvar -> to_:int -> Data.uvar -> int -> Data.term

val deref_appuv : 
  ?avoid:Data.uvar ->
  to_:int ->
  Data.uvar ->
  Data.term list ->
  Data.term

val deref_apparg : 
  ?avoid:Data.uvar ->
  from:int ->
  to_:int ->
  Data.term ->
  Data.term list ->
  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 option

Sourceval expand_uv : depth:int -> Data.uvar -> ano:int -> Data.term

Sourceval expand_appuv : depth:int -> Data.uvar -> 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

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

Sourceval hmove : ?avoid:Data.uvar -> from:int -> to_:int -> Data.term -> Data.term

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

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

Install