frontend.mli

open Constrexpr
open Names

(*
 * Identify an algebraic ornament between two types
 * Define the components of the corresponding equivalence
 * If the appropriate option is set, prove that these form an equivalence
 *)
val find_ornament : ?hints:string list -> Id.t option -> constr_expr -> constr_expr -> int option -> unit          

(*
 * Save a user-supplied equivalence between two types.
 * The boolean denotes a custom kind of equivalence (that is, not one of
 * the supported kinds, like the supported algebraic ornaments and so on).
 * If only one of two functions is supplied, automatically invert for
 * non-custom equivalences.
 * If the appropriate option is set, prove that these form an equivalence
 * for non-custom ornaments.
 *)
val save_ornament :
  constr_expr ->
  constr_expr ->
  constr_expr option ->
  constr_expr option ->
  bool ->
  unit
                                                                   
(*
 * Lift the supplied function along an ornament between the supplied types
 * Define the lifted version
 *)
val lift_by_ornament : ?suffix:bool -> ?opaques:Libnames.qualid list -> ?hints:string list -> Id.t -> constr_expr -> constr_expr -> constr_expr -> bool -> unit

(*
  * Lift each module element (constant and inductive definitions) along the given
  * ornament, defining a new module with all the transformed module elements.
  *)
val lift_module_by_ornament : ?opaques:Libnames.qualid list -> ?hints:string list -> Id.t -> constr_expr -> constr_expr -> Libnames.qualid -> unit

(*
 * Lift (transform) and then decompile for tactic suggestions
 *)
val repair : ?suffix:bool -> ?opaques:Libnames.qualid list -> ?hints:string list -> Id.t -> constr_expr -> constr_expr -> constr_expr -> bool -> unit

(*
 * Whole module lift (transform) and decompile for tactic suggestions
 *)
val repair_module : ?opaques:Libnames.qualid list -> ?hints:string list -> Id.t -> constr_expr -> constr_expr -> Libnames.qualid -> unit
                                             
(*
 * Unpack sigma types in the functional signature of a constant.
 *
 * This transformation assumes that the input constant was generated by
 * ornamental lifting.
 *)
val do_unpack_constant : Id.t -> Libnames.qualid -> unit

(*
 * Add terms to or remove terms from the globally opaque lifting cache
 * at a particular ornament
 *)
val add_lifting_opaques :
  constr_expr -> constr_expr -> Libnames.qualid list -> unit
val remove_lifting_opaques :
  constr_expr -> constr_expr ->  Libnames.qualid list -> unit

(*
 * Manual configuration
 *)
val configure_manual :
  constr_expr -> (* A *)
  constr_expr -> (* B *)
  (Libnames.qualid list) * (Libnames.qualid list) -> (* DepConstr *)
  (Libnames.qualid * Libnames.qualid) -> (* DepElim *)
  (Libnames.qualid * Libnames.qualid) -> (* Eta *)
  (Libnames.qualid list) * (Libnames.qualid list) -> (* Iota *)
  unit