Library Ltac2.Constr


Require Import Ltac2.Init.
Require Ltac2.Ind Ltac2.Array.

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 Binder.

Ltac2 Type relevance_var.
Ltac2 Type relevance := [ Relevant | Irrelevant | RelevanceVar (relevance_var) ].

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.

Ltac2 @ external relevance : binder -> relevance := "coq-core.plugins.ltac2" "constr_binder_relevance".
Retrieve the relevance of a binder.

End Binder.

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 * Binder.relevance), case_invert, constr, constr array)
| Fix (int array, int, binder array, constr array)
| CoFix (int, binder array, constr array)
| Proj (projection, Binder.relevance, constr)
| Uint63 (uint63)
| Float (float)
| Array (instance, constr array, constr, constr)
].

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

Ltac2 rec kind_nocast c :=
  match kind c with
  | Cast c _ _ => kind_nocast c
  | k => k
  end.

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 constructor (ind : inductive) (i : int) : constructor :=
  Ind.get_constructor (Ind.data ind) i.
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 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.

Open recursion combinators

Local Ltac2 iter_invert (f : constr -> unit) (ci : case_invert) : unit :=
  match ci with
  | NoInvert => ()
  | CaseInvert indices => Array.iter f indices
  end.

iter f c iters f on the immediate subterms of c; it is not recursive and the order with which subterms are processed is not specified
Ltac2 iter (f : constr -> unit) (c : constr) : unit :=
  match kind c with
  | Rel _ | Meta _ | Var _ | Sort _ | Constant _ _ | Ind _ _
  | Constructor _ _ | Uint63 _ | Float _ => ()
  | Cast c _ t => f c; f t
  | Prod b c => f (Binder.type b); f c
  | Lambda b c => f (Binder.type b); f c
  | LetIn b t c => f (Binder.type b); f t; f c
  | App c l => f c; Array.iter f l
  | Evar _ l => Array.iter f l
  | Case _ x iv y bl =>
      match x with (x,_) => f x end;
      iter_invert f iv;
      f y;
      Array.iter f bl
  | Proj _p _ c => f c
  | Fix _ _ tl bl =>
      Array.iter (fun b => f (Binder.type b)) tl;
      Array.iter f bl
  | CoFix _ tl bl =>
      Array.iter (fun b => f (Binder.type b)) tl;
      Array.iter f bl
  | Array _u t def ty =>
      f ty; Array.iter f t; f def
  end.

iter_with_binders g f n c iters f n on the immediate subterms of c; it carries an extra data n (typically a lift index) which is processed by g (which typically add 1 to n) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified
Ltac2 iter_with_binders (g : 'a -> binder -> 'a) (f : 'a -> constr -> unit) (n : 'a) (c : constr) : unit :=
  match kind c with
  | Rel _ | Meta _ | Var _ | Sort _ | Constant _ _ | Ind _ _
  | Constructor _ _ | Uint63 _ | Float _ => ()
  | Cast c _ t => f n c; f n t
  | Prod b c => f n (Binder.type b); f (g n b) c
  | Lambda b c => f n (Binder.type b); f (g n b) c
  | LetIn b t c => f n (Binder.type b); f n t; f (g n b) c
  | App c l => f n c; Array.iter (f n) l
  | Evar _ l => Array.iter (f n) l
  | Case _ x iv y bl =>
      match x with (x,_) => f n x end;
      iter_invert (f n) iv;
      f n y;
      Array.iter (f n) bl
  | Proj _p _ c => f n c
  | Fix _ _ tl bl =>
      Array.iter (fun b => f n (Binder.type b)) tl;
      let n := Array.fold_left g n tl in
      Array.iter (f n) bl
  | CoFix _ tl bl =>
      Array.iter (fun b => f n (Binder.type b)) tl;
      let n := Array.fold_left g n tl in
      Array.iter (f n) bl
  | Array _u t def ty =>
      f n ty;
      Array.iter (f n) t;
      f n def
  end.

Local Ltac2 binder_map (f : constr -> constr) (b : binder) : binder :=
  Binder.unsafe_make (Binder.name b) (Binder.relevance b) (f (Binder.type b)).

Local Ltac2 map_invert (f : constr -> constr) (iv : case_invert) : case_invert :=
  match iv with
  | NoInvert => NoInvert
  | CaseInvert indices => CaseInvert (Array.map f indices)
  end.

map f c maps f on the immediate subterms of c; it is not recursive and the order with which subterms are processed is not specified
Ltac2 map (f : constr -> constr) (c : constr) : constr :=
  match kind c with
  | Rel _ | Meta _ | Var _ | Sort _ | Constant _ _ | Ind _ _
  | Constructor _ _ | Uint63 _ | Float _ => c
  | Cast c k t =>
      let c := f c
      with t := f t in
      make (Cast c k t)
  | Prod b c =>
      let b := binder_map f b
      with c := f c in
      make (Prod b c)
  | Lambda b c =>
      let b := binder_map f b
      with c := f c in
      make (Lambda b c)
  | LetIn b t c =>
      let b := binder_map f b
      with t := f t
      with c := f c in
      make (LetIn b t c)
  | App c l =>
      let c := f c
      with l := Array.map f l in
      make (App c l)
  | Evar e l =>
      let l := Array.map f l in
      make (Evar e l)
  | Case info x iv y bl =>
      let x := match x with (x,x') => (f x, x') end
      with iv := map_invert f iv
      with y := f y
      with bl := Array.map f bl in
      make (Case info x iv y bl)
  | Proj p r c =>
      let c := f c in
      make (Proj p r c)
  | Fix structs which tl bl =>
      let tl := Array.map (binder_map f) tl
      with bl := Array.map f bl in
      make (Fix structs which tl bl)
  | CoFix which tl bl =>
      let tl := Array.map (binder_map f) tl
      with bl := Array.map f bl in
      make (CoFix which tl bl)
  | Array u t def ty =>
      let ty := f ty
      with t := Array.map f t
      with def := f def in
      make (Array u t def ty)
  end.

End Unsafe.

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.

Module Pretype.
  Module Flags.
    Ltac2 Type t.

    Ltac2 @ external constr_flags : t := "coq-core.plugins.ltac2" "constr_flags".
The flags used by constr:().

    Ltac2 @external set_use_coercions : bool -> t -> t
      := "coq-core.plugins.ltac2" "pretype_flags_set_use_coercions".
Use coercions during pretyping. true in constr_flags.

    Ltac2 @external set_use_typeclasses : bool -> t -> t
      := "coq-core.plugins.ltac2" "pretype_flags_set_use_typeclasses".
Run typeclass inference at the end of pretyping and when needed according to flag "Typeclass Resolution For Conversion". true in constr_flags.

    Ltac2 @external set_allow_evars : bool -> t -> t
      := "coq-core.plugins.ltac2" "pretype_flags_set_allow_evars".
Allow pretyping to produce new unresolved evars. false in constr_flags.

    Ltac2 @external set_nf_evars : bool -> t -> t
      := "coq-core.plugins.ltac2" "pretype_flags_set_nf_evars".
Evar-normalize the result of pretyping. This should not impact anything other than performance. true in constr_flags.

    Ltac2 Notation open_constr_flags_with_tc :=
      set_nf_evars false (set_allow_evars true constr_flags).

    Ltac2 Notation open_constr_flags_no_tc :=
      set_use_typeclasses false open_constr_flags_with_tc.
The flags used by open_constr:() and its alias '.

    #[deprecated(since="8.20", note="use open_constr_flags_with_tc (or no_tc as desired)")]
    Ltac2 Notation open_constr_flags := open_constr_flags_with_tc.
  End Flags.

  Ltac2 Type expected_type.

  Ltac2 @ external expected_istype : expected_type
    := "coq-core.plugins.ltac2" "expected_istype".

  Ltac2 @ external expected_oftype : constr -> expected_type
    := "coq-core.plugins.ltac2" "expected_oftype".

  Ltac2 @ external expected_without_type_constraint : expected_type
    := "coq-core.plugins.ltac2" "expected_without_type_constraint".

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

Ltac2 pretype (c : preterm) : constr :=
  Pretype.pretype Pretype.Flags.constr_flags Pretype.expected_without_type_constraint c.
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.

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

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

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