(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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)
| String (pstring)
| 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 [Rel]s) *)

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 _ | String _ => ()
  | 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 _ | String _ => ()
  | 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 _ | String _ => 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).

    Local Ltac2 open_constr_flags_with_tc_kn () := open_constr_flags_with_tc.
    (** Code generation uses this as using the notation is not convenient. *)

    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.