Library Ltac2.Constr


Require Import Ltac2.Init.

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

Ltac2 @ external equal : constr -> constr -> bool := "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 := "ltac2" "constr_kind".

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

Ltac2 @ external check : constr -> constr result := "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 := "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 := "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 := "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 := "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 := "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 := "ltac2" "constr_case".
Generate the case information for a given inductive type.

Ltac2 @ external constructor : inductive -> int -> constructor := "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 := "ltac2" "constr_case_equal".
End Case.

End Unsafe.

Module Binder.

Ltac2 Type relevance := [ Relevant | Irrelevant ].

Ltac2 @ external make : ident option -> constr -> binder := "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 := "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 := "ltac2" "constr_binder_name".
Retrieve the name of a binder.

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

End Binder.

Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "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 := "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 := "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.