Library Ltac2.Constr


Require Import Ltac2.Init.

Ltac2 @ external type : constr -> constr := "coq-core.plugins.ltac2" "constr_type".
Return the type of a term

Ltac2 @ external equal : constr -> constr -> bool := "coq-core.plugins.ltac2" "constr_equal".
Strict syntactic equality: only up to α-conversion and evar expansion

Module Unsafe.

Low-level access to kernel terms. Use with care!

Ltac2 Type case.

Ltac2 Type case_invert := [
| NoInvert
| CaseInvert (constr array)
].

Ltac2 Type kind := [
| Rel (int)
| Var (ident)
| Meta (meta)
| Evar (evar, constr array)
| Sort (sort)
| Cast (constr, cast, constr)
| Prod (binder, constr)
| Lambda (binder, constr)
| LetIn (binder, constr, constr)
| App (constr, constr array)
| Constant (constant, instance)
| Ind (inductive, instance)
| Constructor (constructor, instance)
| Case (case, constr, case_invert, constr, constr array)
| Fix (int array, int, binder array, constr array)
| CoFix (int, binder array, constr array)
| Proj (projection, constr)
| Uint63 (uint63)
| Float (float)
| Array (instance, constr array, constr, constr)
].

Ltac2 @ external kind : constr -> kind := "coq-core.plugins.ltac2" "constr_kind".

Ltac2 @ external make : kind -> constr := "coq-core.plugins.ltac2" "constr_make".

Ltac2 @ external check : constr -> constr result := "coq-core.plugins.ltac2" "constr_check".
Checks that a constr generated by unsafe means is indeed safe in the current environment, and returns it, or the error otherwise. Panics if not focused.

Ltac2 @ external liftn : int -> int -> constr -> constr := "coq-core.plugins.ltac2" "constr_liftn".
liftn n k c lifts by n indices greater than or equal to k in c Note that with respect to substitution calculi's terminology, n is the shift and k is the lift.

Ltac2 @ external substnl : constr list -> int -> constr -> constr := "coq-core.plugins.ltac2" "constr_substnl".
substnl [r₁;...;rₙ] k c substitutes in parallel Rel(k+1); ...; Rel(k+n) with r₁;...;rₙ in c.

Ltac2 @ external closenl : ident list -> int -> constr -> constr := "coq-core.plugins.ltac2" "constr_closenl".
closenl [x₁;...;xₙ] k c abstracts over variables x₁;...;xₙ and replaces them with Rel(k); ...; Rel(k+n-1) in c. If two names are identical, the one of least index is kept.

Ltac2 @ external closedn : int -> constr -> bool := "coq-core.plugins.ltac2" "constr_closedn".
closedn n c is true iff c is a closed term under n binders

Ltac2 is_closed (c : constr) : bool := closedn 0 c.
is_closed c is true iff c is a closed term (contains no Rels)

Ltac2 @ external occur_between : int -> int -> constr -> bool := "coq-core.plugins.ltac2" "constr_occur_between".
occur_between n m c returns true iff Rel p occurs in term c for n <= p < n+m

Ltac2 occurn (n : int) (c : constr) : bool := occur_between n 1 c.
occurn n c returns true iff Rel n occurs in term c

Ltac2 @ external case : inductive -> case := "coq-core.plugins.ltac2" "constr_case".
Generate the case information for a given inductive type.

Ltac2 @ external constructor : inductive -> int -> constructor := "coq-core.plugins.ltac2" "constr_constructor".
Generate the i-th constructor for a given inductive type. Indexing starts at 0. Panics if there is no such constructor.

Module Case.
  Ltac2 @ external equal : case -> case -> bool := "coq-core.plugins.ltac2" "constr_case_equal".
Checks equality of the inductive and relevance components of the case info. When comparing the inductives, those obtained through module aliases or Include are not considered equal by this function.

End Case.

End Unsafe.

Module Binder.

Ltac2 Type relevance := [ Relevant | Irrelevant ].

Ltac2 @ external make : ident option -> constr -> binder := "coq-core.plugins.ltac2" "constr_binder_make".
Create a binder given the name and the type of the bound variable. Fails if the type is not a type in the current goal.

Ltac2 @ external unsafe_make : ident option -> relevance -> constr -> binder := "coq-core.plugins.ltac2" "constr_binder_unsafe_make".
Create a binder given the name and the type and relevance of the bound variable.

Ltac2 @ external name : binder -> ident option := "coq-core.plugins.ltac2" "constr_binder_name".
Retrieve the name of a binder.

Ltac2 @ external type : binder -> constr := "coq-core.plugins.ltac2" "constr_binder_type".
Retrieve the type of a binder.

End Binder.

Module Cast.

  Ltac2 @ external default : cast := "coq-core.plugins.ltac2" "constr_cast_default".
  Ltac2 @ external vm : cast := "coq-core.plugins.ltac2" "constr_cast_vm".
  Ltac2 @ external native : cast := "coq-core.plugins.ltac2" "constr_cast_native".

  Ltac2 @ external equal : cast -> cast -> bool := "coq-core.plugins.ltac2" "constr_cast_equal".

End Cast.

Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "coq-core.plugins.ltac2" "constr_in_context".
On a focused goal Γ ⊢ A, in_context id c tac evaluates tac in a focused goal Γ, id : c ⊢ ?X and returns fun (id : c) => t where t is the proof built by the tactic.

Ltac2 @ external pretype : preterm -> constr := "coq-core.plugins.ltac2" "constr_pretype".
Pretype the provided preterm. Assumes the goal to be focussed.

Ltac2 is_evar(c: constr) :=
  match Unsafe.kind c with
  | Unsafe.Evar _ _ => true
  | _ => false
  end.

Ltac2 @ external has_evar : constr -> bool := "coq-core.plugins.ltac2" "constr_has_evar".

Ltac2 is_var(c: constr) :=
  match Unsafe.kind c with
  | Unsafe.Var _ => true
  | _ => false
  end.

Ltac2 is_fix(c: constr) :=
  match Unsafe.kind c with
  | Unsafe.Fix _ _ _ _ => true
  | _ => false
  end.

Ltac2 is_cofix(c: constr) :=
  match Unsafe.kind c with
  | Unsafe.CoFix _ _ _ => true
  | _ => false
  end.

Ltac2 is_ind(c: constr) :=
  match Unsafe.kind c with
  | Unsafe.Ind _ _ => true
  | _ => false
  end.

Ltac2 is_constructor(c: constr) :=
  match Unsafe.kind c with
  | Unsafe.Constructor _ _ => true
  | _ => false
  end.

Ltac2 is_proj(c: constr) :=
  match Unsafe.kind c with
  | Unsafe.Proj _ _ => true
  | _ => false
  end.

Ltac2 is_const(c: constr) :=
  match Unsafe.kind c with
  | Unsafe.Constant _ _ => true
  | _ => false
  end.