lambdapi 2.2.0 · OCaml Package

Implementation of the rewrite tactic.

val log_rewr : 'a Lplib.Base.outfmt -> 'a

type eq_config = {

symb_P : Core.Term.sym;
(*
Encoding of propositions.
*)
symb_T : Core.Term.sym;
(*
Encoding of types.
*)
symb_eq : Core.Term.sym;
(*
Equality proposition.
*)
symb_eqind : Core.Term.sym;
(*
Induction principle on equality.
*)
symb_refl : Core.Term.sym;
(*
Reflexivity of equality.
*)

}

Equality configuration.

val get_eq_config : Core.Sig_state.t -> Common.Pos.popt -> eq_config

get_eq_config ss pos returns the current configuration for equality, used by tactics such as “rewrite” or “reflexivity”.

val get_eq_data : 
  eq_config ->
  Common.Pos.popt ->
  Core.Term.term ->
  (Core.Term.term * Core.Term.term * Core.Term.term) * Core.Term.tvar array

get_eq_data pos cfg a returns ((a,l,r),[v1;..;vn]) if a ≡ Π v1:A1, .., Π vn:An, P (eq a l r) and fails otherwise.

type to_subst = Core.Term.tvar array * Core.Term.term

Type of a term with the free variables that need to be substituted. It is usually used to store the LHS of a proof of equality, together with the variables that were quantified over.

val matches : Core.Term.term -> Core.Term.term -> bool

matches p t instantiates the TRef's of p so that p gets equal to t and returns true if all TRef's of p could be instantiated, and false otherwise.

val matching_subs : to_subst -> Core.Term.term -> Core.Term.term array option

matching_subs (xs,p) t attempts to match the pattern p containing the variables xs) with the term t. If successful, it returns Some ts where ts is an array of terms such that substituting xs by the corresponding elements of ts in p yields t.

val find_subst : to_subst -> Core.Term.term -> Core.Term.term array option

find_subst (xs,p) t tries to find the first instance of a subterm of t matching p. If successful, the function returns the array of terms by which xs must substituted.

val find_subterm_matching : Core.Term.term -> Core.Term.term -> bool

find_subterm_matching p t tries to find a subterm of t that matches p by instantiating the TRef's of p. In case of success, the function returns true.

val bind_pattern : Core.Term.term -> Core.Term.term -> Core.Term.tbinder

bind_pattern p t replaces in the term t every occurence of the pattern p by a fresh variable, and returns the binder on this variable.

val swap : 
  eq_config ->
  Core.Term.term ->
  Core.Term.term ->
  Core.Term.term ->
  Core.Term.term ->
  Core.Term.term

swap cfg a r l t returns a term of type P (eq a l r) from a term t of type P (eq a r l).

val replace_wild_by_tref : Core.Term.term -> Core.Term.term

replace_wild_by_tref t substitutes every wildcard of t by a fresh TRef.

val rewrite : 
  Core.Sig_state.t ->
  Core.Term.problem ->
  Common.Pos.popt ->
  Proof.goal_typ ->
  bool ->
  (Core.Term.term, Core.Term.tbinder) Parsing.Syntax.rw_patt option ->
  Core.Term.term ->
  Core.Term.term

rewrite ss p pos gt l2r pat t generates a term for the refine tactic representing the application of the rewrite tactic to the goal type gt. Every occurrence of the first instance of the left-hand side is replaced by the right-hand side of the obtained proof (or the reverse if l2r is false). pat is an optional SSReflect pattern. t is the equational lemma that is appied. It handles the full set of SSReflect patterns.

package lambdapi