elpi 1.20.0 · OCaml Package

module Pp : sig ... end

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

val embed_query : 
  mk_Arg:
    (Elpi__.Data.State.t ->
      name:string ->
      args:Elpi__.Data.Term.term list ->
      Elpi__.Data.State.t * Elpi__.Data.Term.term) ->
  depth:int ->
  Elpi__.Data.State.t ->
  'a Elpi__.Data.Query.t ->
  Elpi__.Data.State.t
  * Elpi__.Data.Term.term
  * Elpi__.Data.Conversion.extra_goal list

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

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

val deref_uv : 
  ?avoid:Elpi__.Data.Term.uvar_body ->
  from:int ->
  to_:int ->
  int ->
  Elpi__.Data.Term.term ->
  Elpi__.Data.Term.term

val deref_appuv : 
  ?avoid:Elpi__.Data.Term.uvar_body ->
  from:int ->
  to_:int ->
  Elpi__.Data.Term.term list ->
  Elpi__.Data.Term.term ->
  Elpi__.Data.Term.term

val deref_head : depth:int -> Elpi__.Data.Term.term -> Elpi__.Data.Term.term

val eta_contract_flex : 
  depth:int ->
  Elpi__.Data.Term.term ->
  Elpi__.Data.Term.term option

val is_flex : 
  depth:int ->
  Elpi__.Data.Term.term ->
  Elpi__.Data.Term.uvar_body option

val expand_uv : 
  depth:int ->
  Elpi__.Data.Term.uvar_body ->
  lvl:int ->
  ano:int ->
  Elpi__.Data.Term.term

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

val lp_list_to_list : 
  depth:int ->
  Elpi__.Data.Term.term ->
  Elpi__.Data.Term.term list

val list_to_lp_list : Elpi__.Data.Term.term list -> Elpi__.Data.Term.term

val split_conj : 
  depth:int ->
  Elpi__.Data.Term.term ->
  Elpi__.Data.Term.term list

val mkinterval : int -> int -> int -> Elpi__.Data.Term.term list

val mkConst : int -> Elpi__.Data.Term.term

val mkAppL : int -> Elpi__.Data.Term.term list -> Elpi__.Data.Term.term

val mkAppArg : 
  int ->
  int ->
  Elpi__.Data.Term.term list ->
  Elpi__.Data.Term.term

val move : 
  argsdepth:int ->
  Elpi__.Data.Term.term array ->
  ?avoid:Elpi__.Data.Term.uvar_body ->
  from:int ->
  to_:int ->
  Elpi__.Data.Term.term ->
  Elpi__.Data.Term.term

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

val subst : 
  depth:int ->
  Elpi__.Data.Term.term list ->
  Elpi__.Data.Term.term ->
  Elpi__.Data.Term.term

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

val full_deref : depth:int -> Elpi__.Data.Term.term -> Elpi__.Data.Term.term

val lex_insertion : int list -> int list -> int

module CompileTime : sig ... end

package elpi