test script for removal of unneeded arguments

Load removeNonAug.

Inductive list (A : Type) (Aᵗ : A -> Type) : list A -> Type :=
    nil : list A A []
  | cons : forall H : A,
            A H -> forall H0 : list A, list A A H0 -> list A A (H :: H0).

Inductive bool : bool -> Set :=
  true : bool true | false : bool false.
Inductive nat : nat -> Set :=
    O : nat 0
  | S : forall H : nat, nat H -> nat (S H).

Definition vec := VectorDef.t.

Inductive
vec (A : Type) (A : A -> Type)
  : forall H : nat, nat H -> vec A H -> Type :=
    vecnil : vec A A 0 O (@Vector.nil A)
  | veccons : forall H : A,
               A H ->
               forall (n : nat) (n : nat n)
                 (H0 : vec A n),
               vec A A n n H0 ->
               vec A A (S n) (S n nᵗ)
                    (@Vector.cons A H n H0).

(* Inductive *)
(* vecᵗ' (A : Type) (Aᵗ : A -> Type) *)
(*   : forall H : nat, vec A H -> Type := *)
(*     vecnilᵗ' : vecᵗ' A Aᵗ 0 (@Vector.nil A) *)
(*   | vecconsᵗ' : forall H : A, *)
(*                Aᵗ H -> *)
(*                forall (n : nat) *)
(*                (1* (nᵗ : natᵗ n) *1) *)
(*                  (H0 : vec A n), *)
(*                vecᵗ' A Aᵗ n H0 -> *)
(*                vecᵗ' A Aᵗ (S n) *)
(*                     (@Vector.cons A H n H0). *)

(*
Print vecᵗ.

Inductive
vecᵗ (A : Type) (Aᵗ : A -> Type)
  : forall H : nat, natᵗ H -> vec A H -> Type :=
    vecnilᵗ : vecᵗ A Aᵗ 0 Oᵗ (Vector.nil A)
  | vecconsᵗ : forall H : A,
               Aᵗ H ->
               forall (n : nat) (nᵗ : natᵗ n) (H0 : vec A n),
               vecᵗ A Aᵗ n nᵗ H0 ->
               vecᵗ A Aᵗ (S n) (Sᵗ n nᵗ) (Vector.cons A H n H0)
               *)


(* MetaCoq Run (cleanInd "vecᵗ" >>= tmMsg). *)
(* MetaCoq Run (cleanInd listᵗ >>= tmMsg). *)

(* Print vecᵗ0. *)
(* Print listᵗ0. *)

Print tmMkInductive.
Print mutual_inductive_entry.
Search mutual_inductive_entry.
Print mutual_inductive_body.
Print context_decl.

MetaCoq Run (tmQuoteInductive "vecᵗ" >>= tmPrint).

Compute (removeArgList (tApp (tRel 0) [tRel 1;tRel 2;tRel 3]) [1]).

About print_term.
Search global_env_ext.

(* MetaCoq Run ( *)
(* xp <- removeNonAugmentable <*)
(*   , forall H : nat, natᵗ H -> vec A H -> Type *)
(* y <- tmEval all (xp);; *)
(* tmPrint y;; *)
(* tmMsg (print_term (empty_ext  true y.1)). *)

(* MetaCoq Run ( *)
(* x <- removeNonAugmentable *)
(*   <*)
(* forall(A : Type) (Aᵗ : A -> Type), *)
(*                forall H : A, *)
(*                Aᵗ H -> *)
(*                forall (n : nat) (nᵗ : natᵗ n) *)
(*                  (H0 : vec A n), *)
(*                vecᵗ A Aᵗ n nᵗ H0 -> *)
(*                vecᵗ A Aᵗ (S n) (Sᵗ n nᵗ) *)
(*                     (@Vector.cons A H n H0) *)
(*   *)
(* y <- tmEval all (x);; *)
(* tmPrint y;; *)
(* tmMsg (print_term (empty_ext  true y.1);; *)
(* tmMsg "";; *)
(* tmMsg "";; *)
(* tmMsg "";; *)
(* y2 <- tmEval all (removeArgList (y.1) 3);; *)
(* tmPrint y2;; *)
(* tmMsg (print_term (empty_ext  true y2) *)
(* ). *)

(*
1. remove Parameter after non augmentable inductive
2. delete parameter in recursive call

should the function look inside the arguments?
TODO: find examples like (T -> nat) or (nat -> T) in an argument
*)