(*i camlp4deps: "parsing/grammar.cma" i*)

(*s FunInv Tactic: inversion following the shape of a function.  *)
(* Use:
   \begin{itemize}
   \item The Tacinv directory must be in the path (-I <path> option)
   \item use the bytecode version of coqtop or coqc (-byte option), or make a
         coqtop 
   \item Do [Require Tacinv] to be able to use it.
   \item For syntax see Tacinv.v
   \end{itemize}
*)


(*i*)
open Termops
open Equality
open Names
open Pp
open Tacmach
open Proof_type
open Tacinterp
open Tactics
open Tacticals
open Term
open Util
open Printer
open Reductionops
open Inductiveops
open Coqlib
open Refine
open Typing
open Declare
open Decl_kinds
open Safe_typing
open Vernacinterp
open Evd
open Environ
open Entries
open Setoid_replace
open Tacinvutils
(*i*)

module Smap = Map.Make(struct type t = constr let compare = compare end)
let smap_to_list m = Smap.fold (fun c cb l -> (c,cb)::l) m []
let merge_smap m1 m2 = Smap.fold (fun c cb m -> Smap.add c cb m) m1 m2

let mkthesort = mkProp (* would like to put Type here, but with which index? *)

(*  this is the prefix used to name equality hypothesis generated by
    case analysis*)
let equality_hyp_string = "_eg_"

(* bug de refine: on doit ssavoir sur quelle hypothese on se trouve. valeur
   initiale au debut de l'appel a la fonction proofPrinc: 1. *)
let nthhyp = ref 1
 (*debugging*)
 (* let rewrules = ref [] *)
 (*debugging*)
let debug i = prstr ("DEBUG "^ string_of_int i ^"\n")
let pr2constr = (fun c1 c2 -> prconstr c1; prstr " <---> "; prconstr c2)
 (*end debugging *)

let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c

let rec collect_cases l =
 match l with
  | [||] -> [||],[],[],[||],[||]
  | arr -> 
     let (a,c,d,f,e)= arr.(0) in
     let aa,lc,ld,_,_ = 
      collect_cases (Array.sub arr 1 ((Array.length arr)-1)) in
     Array.append [|a|] aa , (c@lc) , (d@ld) , f , e

let rec collect_pred l =
 match l with
  | [] -> [],[],[]
  | (e1,e2,e3)::l' -> let a,b,c = collect_pred l' in (e1::a),(e2::b),(e3::c)


(*s specific manipulations on constr *)
let lift1_leqs leq=
 List.map 
  (function (r,(typofg,g,d)) 
      -> lift 1 r, (lift 1 typofg, lift 1 g , lift 1 d)) leq

let lift1_relleqs leq= List.map (function (r,x) -> lift 1 r,x) leq

(* WARNING: In the types, we don't lift the rels in the type. This is
   intentional. Use with care. *)
let lift1_lvars lvars= List.map 
 (function x,(nme,c) -> lift 1 x, (nme, (*lift 1*) c)) lvars


let rec add_n_dummy_prod t n = 
 if n<=0 then t
 else add_n_dummy_prod (mkNamedProd (id_of_string "DUMMY") mkthesort t) (n-1)

(* [add_lambdas t gl [csr1;csr2...]] returns [[x1:type of csr1]
   [x2:type of csr2] t [csr <- x1 ...]], names of abstracted variables
   are not specified *)
let rec add_lambdas t gl lcsr =
 match lcsr with
  | [] -> t
  | csr::lcsr' -> 
     let hyp_csr,hyptyp = csr,(pf_type_of gl csr) in
     lambda_id hyp_csr hyptyp (add_lambdas t gl lcsr')

(* [add_pis t gl [csr1;csr2...]] returns ([x1] :type of [csr1]
   [x2]:type of csr2) [t]*)
let rec add_pis t gl lcsr =
 match lcsr with
  | [] -> t
  | csr::lcsr' -> 
     let hyp_csr,hyptyp = csr,(pf_type_of gl csr) in
     prod_id hyp_csr hyptyp (add_pis t gl lcsr')

let mkProdEg teq eql eqr concl =
 mkProd (name_of_string "eg", mkEq teq eql eqr, lift 1 concl)

let eqs_of_beqs x = 
 List.map (function (_,(a,b,c)) -> (Anonymous, mkEq a b c)) x


let rec eqs_of_beqs_named_aux s i l =
 match l with 
  | [] -> []
  | (r,(a,b,c))::l' -> 
     (Name(id_of_string (s^ string_of_int i)), mkEq a b c)
     ::eqs_of_beqs_named_aux s (i-1) l'


let eqs_of_beqs_named s l = eqs_of_beqs_named_aux s (List.length l) l

let rec patternify ltypes c nme =
 match ltypes with
  | [] -> c
  | (mv,t)::ltypes' -> 
     let c'= substitterm 0 mv (mkRel 1) c in
     patternify ltypes' (mkLambda (newname_append nme "rec", t, c')) nme

let rec apply_levars c lmetav =
 match lmetav with
  | [] -> [],c
  | (i,typ) :: lmetav' -> 
     let levars,trm = apply_levars c lmetav' in
     let exkey = mknewexist() in
     ((exkey,typ)::levars),  applistc trm [mkEvar exkey]
      (* EXPERIMENT le refine est plus long si on met un cast:
         ((exkey,typ)::levars), mkCast ((applistc trm [mkEvar exkey]),typ) *)


let prod_change_concl c newconcl = 
 let lv,_ = decompose_prod c in prod_it  newconcl lv

let lam_change_concl c newconcl = 
 let lv,_ = decompose_prod c in lam_it newconcl lv


let rec mkAppRel c largs n =
 match largs with
  | [] -> c
  | arg::largs' -> 
     let newc = mkApp (c,[|(mkRel n)|]) in mkAppRel newc largs' (n-1)

let applFull c typofc =
 let lv,t = decompose_prod typofc in 
 let ltyp = List.map fst lv in mkAppRel c  ltyp ((List.length ltyp))


let rec build_rel_map typ type_of_b = 
 match (kind_of_term typ), (kind_of_term type_of_b) with
    Evar _ , Evar _  -> Smap.empty
  | Rel i, Rel j -> if i=j then Smap.empty 
    else Smap.add typ type_of_b Smap.empty
  | Prod (name,c1,c2), Prod (nameb,c1b,c2b) -> 
     let map1 = build_rel_map c1 c1b in
     let map2 = build_rel_map (pop c2) (pop c2b) in
     merge_smap map1 map2
  | App (f,args), App (fb,argsb) ->
     (try build_rel_map_list (Array.to_list args) (Array.to_list argsb)
     with Invalid_argument _ -> 
      failwith ("Could not generate case annotation. "^ 
      "Two application with different length"))
  | Const c1, Const c2 -> if c1=c2 then Smap.empty
    else failwith ("Could not generate case annotation. "^ 
    "Two different constants in a case annotation.")
  | Ind c1, Ind c2 -> if c1=c2 then Smap.empty
    else failwith ("Could not generate case annotation. "^ 
    "Two different constants in a case annotation.")
  | _,_ -> failwith ("Could not generate case annotation. "^
    "Incompatibility between annotation and actual type")
and build_rel_map_list ltyp ltype_of_b =
 List.fold_left2 (fun a b c -> merge_smap a (build_rel_map b c))
  Smap.empty ltyp ltype_of_b


(*s Use (and proof) of the principle *)

(*
  \begin {itemize}
  \item [concl] ([constr]): conclusions, cad (xi:ti)gl, ou gl est le but a
  prouver, et xi:ti correspondent aux arguments donnés à la tactique.  On
  enlève un produit à chaque fois qu'on rencontre un binder, sans lift ou pop.
  Initialement: une seule conclusion, puis specifique a chaque branche.
  \item[absconcl] ([constr array]): les conclusions (un predicat pour chaque
  fixp. mutuel) patternisées pour  pouvoir être appliquées.
  \item [mimick] ([constr]): le terme qu'on imite. On plonge  dedans au fur et
  à mesure, sans lift ni pop.
  \item [nmefonc] ([constr array]): la constante correspondant à la fonction
  appelée, permet de remplacer les appels recursifs par des appels à la
  constante correspondante (non pertinent (et inutile) si on permet l'appel de
  la tactique sur une terme donné directement (au lieu d'une constante comme
  pour l'instant)).
  \item [fonc] ([int*int]) : bornes des indices des variable correspondant aux
  appels récursifs (plusieurs car fixp.  mutuels), utile pour reconnaître les
  appels récursifs (ATTENTION: initialement vide, reste vide tant qu'on n'est
  pas dans un fix).  
  \end{itemize}
*)

type mimickinfo =
    {
     concl: constr;
     absconcl: constr array;
     mimick: constr;
     env: env;
     sigma: Evd.evar_map;
     nmefonc: constr array;
     fonc: int * int;
     doeqs: bool (* this reference is to toggle building of equalities during
                    the building of the principle (default is true) *)
    }

(*
  \begin{itemize}
  \item [lst_vars] ([(constr*(name*constr)) list]): liste des variables
  rencontrées jusqu'à maintenant.
  \item [lst_eqs] ([constr list]): liste d'équations engendrées au cours du
  parcours, cette liste grandit à chaque case, et il faut lifter le tout à
  chaque binder.
  \item [lst_recs] ([constr list]): listes des appels récursifs rencontrés
  jusque là.
  \end{itemize}

  Cette fonction rends un nuplet de la forme:

  [t,
  [(ev1,tev1);(ev2,tev2)..],
  [(i1,j1,k1);(i2,j2,k2)..],
  [|c1;c2..|],
  [|typ1;typ2..|]]

  où:

  \begin{itemize} 

  \item[t] est le principe demandé, il contient des meta variables représentant
  soit des trous à prouver plus tard, soit les conclusions à compléter avant de
  rendre le terme (plusieurs conclusions si plusieurs fonction mutuellement
  récursives) voir la suite.

  \item[[(ev1,tev1);(ev2,tev2)...]] est l'ensemble des méta variables
  correspondant à des trous. [evi] est la meta variable, [tevi] est son type.

  \item[(in,jn,kn)] sont les nombres respectivement de variables, d'équations,
  et d'hypothèses de récurrence pour le but n. Permet de faire le bon nombre
  d'intros et des rewrite au bons endroits dans la suite.

  \item[[|c1;c2...|]] est un tableau de meta variables correspondant à chacun
  des prédicats mutuellement récursifs construits.

  \item[|typ1;typ2...|] est un tableau contenant les conclusions respectives de
  chacun des prédicats mutuellement récursifs. Permet de finir la construction
  du principe.

  \end{itemize}
*)

type kind_of_hyp = Var | Eq  (*| Rec*)

let rec proofPrinc (mi:mimickinfo) lst_vars lst_eqs lst_recs:
 constr * (constr*Term.types) list * (int*int*int) list 
 * constr array * types array =
 match kind_of_term mi.mimick with
    (* Fixpoint: we reproduce the Fix, fonc becomes (1,nbofmutf) to point on
       the name of recursive calls *) 
  | Fix((iarr,i),(narr,tarr,carr)) -> 

     (* We construct the right predicates for each mutual fixpt *)     
     let rec build_pred n =
      if n >= Array.length iarr then []
      else
        let ftyp = Array.get tarr n in
        let gl = mknewmeta() in
        let gl_app = applFull gl ftyp in
        let pis = prod_change_concl ftyp gl_app in
        let gl_abstr = lam_change_concl ftyp gl_app in
        (gl,gl_abstr,pis):: build_pred (n+1) in
     
     let evarl,predl,pisl = collect_pred (build_pred 0) in
     let newabsconcl = Array.of_list predl in
     let evararr = Array.of_list evarl in
     let pisarr = Array.of_list pisl in
     
     let newenv = push_rec_types (narr,tarr,carr) mi.env in

     let rec collect_fix n =
      if n >= Array.length iarr then [],[],[],[]
      else
        let nme = Array.get narr n in
        let c = Array.get carr n in
        (* rappelle sur le sous-terme, on ajoute un niveau de
           profondeur (lift) parce que Fix est un binder. *)
        let newmi = {mi with concl=(pisarr.(n)); absconcl=newabsconcl;
        mimick=c; fonc=(1,((Array.length iarr)));env=newenv} in
        let appel_rec,levar,lposeq,_,evarrarr = 
         proofPrinc newmi (lift1_lvars lst_vars) 
          (lift1_leqs lst_eqs) (lift1L lst_recs) in
        let lnme,lappel_rec,llevar,llposeq = collect_fix (n+1) in
        (nme::lnme),(appel_rec::lappel_rec),(levar@llevar), (lposeq@llposeq) in
     let lnme,lappel_rec,llevar,llposeq =collect_fix  0 in
     let lnme' = List.map (fun nme -> newname_append nme   "_ind") lnme in
     let anme = Array.of_list lnme' in
     let aappel_rec = Array.of_list lappel_rec in
     mkFix((iarr,i),(anme, pisarr,aappel_rec)),llevar,llposeq,evararr,pisarr

  (* <pcase> Cases b of arrPt end.*)
  | Case(cinfo, pcase, b, arrPt) -> 

     let prod_pcase,_ = decompose_lam pcase in
     let nmeb,lastprod_pcase = List.hd prod_pcase in
     let b'= apply_leqtrpl_t b lst_eqs in
     let type_of_b = Typing.type_of mi.env mi.sigma b in
     let new_lst_recs = lst_recs @ hdMatchSub_cpl b mi.fonc in
     (* Replace the calls to the function (recursive calls) by calls to the
        corresponding constant:  *)
     let d,f = mi.fonc in 
     let res = ref b' in
     let _ = for i = d to f do 
       res := substitterm 0 (mkRel i) mi.nmefonc.(f-i) !res done in
     let newb = !res in

     (* [fold_proof t l n] rend le resultat de l'appel recursif sur les
        elements de la liste l (correpsondant a arrPt), appele avec les bons
        arguments: [concl] devient [(DUMMY1:t1;...;DUMMY:tn)concl'], ou [n]
        est le nombre d'arguments du constructeur considéré (FIX: Hormis les
        parametres!!), et [concl'] est concl ou l'on a réécrit [b] en ($c_n$
        [rel1]...).*)

     let rec fold_proof nth_construct eltPt' =  
      (* mise a jour de concl pour l'interieur du case, concl'= concl[b <- C x3
         x2 x1... ], sans quoi les annotations ne sont plus coherentes *)
      let cstr_appl,nargs = nth_dep_constructor type_of_b nth_construct in
      let concl'' = 
       substitterm 0 (lift nargs b) cstr_appl (lift nargs mi.concl) in
      let neweq = mkEq type_of_b newb (popn nargs cstr_appl) in
      let concl_dummy = add_n_dummy_prod concl'' nargs in
      let lsteqs_rew = apply_eq_leqtrpl lst_eqs neweq in
      let new_lsteqs = 
       (mkRel (0-nargs),(type_of_b,newb, popn nargs cstr_appl))::lsteqs_rew in
      let a',a'' = decompose_lam_n nargs eltPt' in
      let newa'' = 
       if mi.doeqs 
       then mkLambda (name_of_string "_eq_",lift nargs neweq,lift 1 a'') 
       else a'' in
      let newmimick = lamn nargs a' newa'' in
      let b',b'' = decompose_prod_n nargs concl_dummy in
      let newb'' = 
       if mi.doeqs 
       then mkProd (name_of_string "_eq_",lift nargs neweq,lift 1 b'')
       else b'' in
      let newconcl = prodn nargs b' newb'' in
      let newmi = {mi with mimick=newmimick; concl=newconcl} in
      let a,b,c,d,e = proofPrinc newmi lst_vars new_lsteqs new_lst_recs in
      a,b,c,d,e
      in
     
     let arrPt_proof,levar,lposeq,evararr,absc = 
      collect_cases (Array.mapi fold_proof arrPt) in
     let prod_pcase,concl_pcase = decompose_lam pcase in
     let nme,typ = List.hd prod_pcase in
     let suppllam_pcase = List.tl prod_pcase in
     (* je remplace b par rel1 (apres avoir lifte un coup) dans la
        future annotation du futur case: ensuite je mettrai un lambda devant *)
     let typesofeqs' = eqs_of_beqs_named equality_hyp_string lst_eqs in
     (*      let typesofeqs = prod_it_lift typesofeqs' mi.concl in *)
     let typesofeqs = mi.concl in
     let typeof_case'' = 
      substitterm 0 (lift 1 b) (mkRel 1) (lift 1 typesofeqs) in
     
     (* C'est un peu compliqué ici: en cas de type inductif vraiment dépendant
        le piquant du case [pcase] contient des lambdas supplémentaires en tête
        je les ai dans la variable [suppllam_pcase]. Le problème est que la
        conclusion du piquant doit faire référence à ces variables plutôt qu'à
        celle de l'exterieur. Ce qui suit permet de changer les reference de
        newpacse' pour pointer vers les lambda du piquant. On procède comme
        suit: on repère les rels qui pointent à l'interieur du piquant dans la
        fonction imitée, pour ça on parcourt le dernier lambda du piquant (qui
        contient le type de l'argument du case), et on remplace les rels
        correspondant dans la preuve construite. *)
     
     (* typ vient du piquant, type_of_b vient du typage de b.*)
     
     let rel_smap = 
      if List.length suppllam_pcase=0 then Smap.empty else
        build_rel_map (lift (List.length suppllam_pcase) type_of_b) typ in
     let rel_map = smap_to_list rel_smap in
     let rec substL l c =
      match l with
         [] -> c
       | ((e,e') ::l') -> substL l' (substitterm 0 e (lift 1 e') c) in
     let newpcase' = substL rel_map typeof_case'' in
     let neweq = mkEq (lift (List.length suppllam_pcase + 1) type_of_b) 
      (lift (List.length suppllam_pcase + 1) newb) (mkRel 1) in
     let newpcase = 
      if mi.doeqs then
        mkProd (name_of_string "eg", neweq, lift 1 newpcase') else newpcase'
     in
     (* construction du dernier lambda du piquant. *)
     let typeof_case' = mkLambda (newname_append nme "_ind" ,typ, newpcase) in
     (* ajout des lambdas supplémentaires (type dépendant) du piquant. *)
     let typeof_case = 
      lamn (List.length suppllam_pcase) suppllam_pcase typeof_case' in 
     let trm' = mkCase (cinfo,typeof_case,newb, arrPt_proof) in
     let trm = 
      if mi.doeqs then mkApp (trm',[|(mkRefl type_of_b newb)|]) 
      else trm' in
     trm,levar,lposeq,evararr,absc
      
  | Lambda(nme, typ, cstr) ->
     let _, _, cconcl = destProd mi.concl in
     let d,f=mi.fonc in
     let newenv = push_rel (nme,None,typ) mi.env in
     let newmi = {mi with concl=cconcl; mimick=cstr; env=newenv;
      fonc=((if d > 0 then d+1 else 0),(if f > 0 then f+1 else 0))} in
     let rec_call,levar,lposeq,evararr,absc =
      proofPrinc newmi ((mkRel 1,(nme,typ)):: lift1_lvars lst_vars)
       (lift1_leqs lst_eqs) (lift1L lst_recs) in
     mkLambda (nme,typ,rec_call) , levar, lposeq,evararr,absc

  | LetIn(nme,cstr1, typ, cstr) ->
     failwith ("I don't deal with let ins yet. "^
				 "Please expand them before applying this function.")

  | u -> 
     let varrels = List.rev (List.map fst lst_vars) in
     let varnames = List.map snd lst_vars in
     let nb_vars = (List.length varnames) in
     let nb_eqs = (List.length lst_eqs) in
     let eqrels = List.map fst lst_eqs in
     (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs
        trouvés dans les let in et les Cases. *)
     (* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *)
     let terms_recs = lst_recs @ (hdMatchSub_cpl mi.mimick mi.fonc)  in
     
     (*c construction du terme: application successive des variables, des
       egalites et des appels rec, a la variable existentielle correspondant a
       l'hypothese de recurrence en cours. *)
     (* d'abord, on fabrique les types des appels recursifs en replacant le nom
        de des fonctions par les predicats dans [terms_recs]: [(f_i t u v)]
        devient [(P_i t u v)] *)
     (* TODO optimiser ici: *)
     let appsrecpred = exchange_reli_arrayi_L mi.absconcl mi.fonc terms_recs in
     let typeofhole''  = prod_it_anonym_lift mi.concl appsrecpred in
     let typeofhole    = prodn nb_vars varnames typeofhole'' in
		   
     (* Un bug de refine m'oblige à mettre ici un H (meta variable à ce point,
        mais remplacé par H avant le refine) au lieu d'un '?', je mettrai les
        '?'  à la fin comme ça [(([H1,H2,H3...] ...) ? ? ?)] *)

     let newmeta = mknewmeta() in
     let concl_with_var = applistc newmeta varrels in
     let conclrecs = applistc concl_with_var terms_recs in
     conclrecs,[newmeta,typeofhole], [nb_vars,(List.length terms_recs)
      ,nb_eqs],[||],mi.absconcl



let mkevarmap_aux ex = let x,y = ex in	(mkevarmap_from_listex x),y

(* Interpretation of constr's *)
let constr_of_Constr c = Constrintern.interp_constr Evd.empty (Global.env()) c


(* TODO: deal with any term, not only a constant. *)
let interp_fonc_tacarg fonctac gl =
 (* [fonc] is the constr corresponding to fontact not unfolded,
    if [fonctac] is a (qualified) name then this is a [const] ?. *)
(*  let fonc = constr_of_Constr fonctac in *)
 (* TODO: replace the [with _ -> ] by something more precise in
    the following. *)
 (* [def_fonc] is the definition of fonc. TODO: We should do this only
    if [fonc] is a const, and take [fonc] otherwise.*)
 try fonctac, pf_const_value gl (destConst fonctac)
 with _ -> failwith ("don't know how to deal with this function "
 ^"(DEBUG:is it a constante?)")




(* [invfun_proof fonc  def_fonc  gl_abstr pis]  builds  the principle,
   following  the shape  of   [def_fonc],    [fonc]  is the      constant
   corresponding to [def_func] (or a reduced form of  it ?), gl_abstr and
   pis are the goal to be proved, of the form [x,y...]g and (x.y...)g.

   This function calls the big function proofPrinc. *)

let invfun_proof fonc def_fonc gl_abstr pis env sigma =
 let _ = resetmeta() in
 let mi = {concl=pis; absconcl=gl_abstr; mimick=def_fonc; env=env;
 sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true} in
 let princ_proof,levar,lposeq,evararr,absc = proofPrinc mi [] [] [] in
 princ_proof,levar,lposeq,evararr,absc

(* Do intros [i] times, then do rewrite on all introduced hyps which are called
   ["_eq_xx"], FIX: have another filter than the name. *)
let rec iterintro i = 
 if i<=0 then tclIDTAC else 
   tclTHEN
    (tclTHEN 
     intro
     (iterintro (i-1)))
    (fun gl -> 
     (tclREPEAT 
      (tclNTH_HYP i
       (fun hyp -> 
        let hypname = (string_of_id (destVar hyp)) in
        let sub = 
         try String.sub hypname 0 4 with _ -> "" (* different than "_eq_" *) in
        if sub="_eq_" then rewriteLR hyp else tclFAIL 0 "Cannot rewrite")
      )) gl)


(* 
       (fun hyp gl -> 
        let _ = print_string ("nthhyp= "^ string_of_int i) in
        if isConst hyp && ((name_of_const hyp)=="_eq_") then
          let _ = print_string "YES\n" in
          rewriteLR hyp gl 
        else 
          let _ = print_string "NO\n" in
          tclIDTAC gl)
 *)
    
(* [invfun_basic C listargs_ids gl dorew lposeq] builds the tactic
   which:
   \begin{itemize}
   \item Do refine on C (the induction principle),
   \item try to Clear listargs_ids
   \item if boolean dorew is true, then intro all new hypothesis, and
   try rewrite on those hypothesis that are equalities.
   \end{itemize}
*)

let invfun_basic open_princ_proof_applied listargs_ids gl dorew lposeq =
 (tclTHEN_i
  (tclTHEN
   (tclTHEN
    (* Refine on the right term (following the sheme of the
       given function) *)
    (fun gl -> refine open_princ_proof_applied  gl)
    (* Clear the hypothesis given as arguments of the tactic
       (because they are generalized) *)
    (tclTHEN simpl_in_concl (tclTRY (clear listargs_ids))))
   (* Now we introduce the created hypothesis, and try rewrite on
      equalities due to case analysis *)
   (fun gl ->  (tclIDTAC gl)))
		(fun i gl -> 
   if not dorew then tclIDTAC gl
   else
     (* d,m,f correspond respectively to vars, induction hyps and
        equalities*)
     let d,m,f = List.nth lposeq (i-1) in
     tclTHEN (iterintro (d)) (tclDO m (tclTRY intro)) gl)
 )
 gl




(* This function trys to reduce instanciated arguments, provided they
   are of the form [(C t u v...)] where [C] is a constructor, and
   provided that the argument is not the argument of a fixpoint (i.e. the
   argument corresponds to a simple lambda) . *)
let rec applistc_iota cstr lcstr env sigma = 
 match lcstr with
  | [] -> cstr,[]
  | arg::lcstr' -> 
     let arghd = 
      if isApp arg then let x,_ = destApplication arg in x else arg in
     if isConstruct arghd (* of the form [(C ...)]*)
     then 
        applistc_iota (Tacred.nf env sigma (nf_beta (applistc cstr [arg])))
         lcstr' env sigma
     else 
       try 
        let nme,typ,suite = destLambda cstr in
        let c, l = applistc_iota suite lcstr' env sigma in
        mkLambda (nme,typ,c), arg::l
       with _ -> cstr,arg::lcstr' (* the arg does not correspond to a lambda*)




(*s Tactic that makes induction and case analysis following the shape
  of a function (idf) given with arguments (listargs) *)
let invfun c l dorew gl = 
(* \begin{itemize}
    \item [fonc] = the constant corresponding to the function
    (necessary for equalities of the form [(f x1 x2 ...)=...] where
    [f] is the recursive function).
    \item [def_fonc] = body of the function, where let ins have
    been expanded. *)
 let fonc, def_fonc' = interp_fonc_tacarg c gl in
 let def_fonc'',listargs' = 
  applistc_iota def_fonc' l (pf_env gl) (project gl)  in
 let def_fonc = expand_letins def_fonc'' in
 (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *)
 let gl_abstr = (add_lambdas (pf_concl gl) gl listargs') in
 (* quantifies on previously generalized arguments. 
    [(x1:T1)...g[arg1 <- x1 ...]] *)
 let pis = add_pis (pf_concl gl) gl listargs' in
 (* princ_proof builds the principle *)
 let princ_proof,levar, lposeq,evararr,_ = 
  invfun_proof [|fonc|] def_fonc [||] pis (pf_env gl) (project gl) in
 (* We do not consider mutual fixpt here *)
 let princ_proof_applied = applistc princ_proof listargs' in
 let princ_applied_hyps' = patternify (List.rev levar) 
  princ_proof_applied (Name (id_of_string "Hyp"))  in
 let princ_applied_hyps = 
  if Array.length evararr > 0 then (* Fixpoint? *)
    substit_red 0 (evararr.(0)) gl_abstr princ_applied_hyps'
  else princ_applied_hyps' (* No Fixpoint *) in
(* let _ = prconstr princ_applied_hyps' in *)
 let princ_applied_evars = apply_levars princ_applied_hyps levar in
 let open_princ_proof_applied = princ_applied_evars in
 let listargs_ids = List.map destVar (List.filter isVar listargs') in
 invfun_basic (mkevarmap_aux open_princ_proof_applied) listargs_ids 
  gl dorew lposeq

(* function must be a constant, all arguments must be given. *)
let invfun_verif c l dorew gl =
 if not (isConst c) then error "given function is not a constant"
 else 
   let x,_ = decompose_prod (pf_type_of gl c) in
   if List.length x = List.length l then 
     try invfun c l dorew gl
     with 
        UserError (x,y) -> raise (UserError (x,y))
   else error "wrong number of arguments for the function"


TACTIC EXTEND FunctionalInduction
  [ "Functional" "Induction" constr(c)  ne_constr_list(l) ] 
     -> [ invfun_verif c l true ]
END



(* Construction of the functional scheme. *)
let buildFunscheme fonc mutflist =
 let def_fonc = expand_letins (def_of_const fonc) in
 let ftyp = type_of (Global.env ()) Evd.empty fonc in
 let gl = mknewmeta() in
 let gl_app = applFull gl ftyp in
 let pis = prod_change_concl ftyp gl_app in
 (* Here we call the function invfun_proof, that effectively 
    builds the scheme *)
 let princ_proof,levar,_,evararr,absc = 
  invfun_proof mutflist def_fonc [||] pis (Global.env()) Evd.empty in
 let lst_hyps = List.map snd levar in
 let princ_proof_hyps = 
  patternify (List.rev levar) princ_proof (Name (id_of_string "Hyp"))  in
 let rec princ_replace_metas ev abs i t = 
  if i>= Array.length ev then t
  else
    princ_replace_metas ev abs (i+1)
     (mkLambda (
      (Name (id_of_string ("Q"^(string_of_int i)))),
      prod_change_concl (lift 1 abs.(i)) mkthesort,
      (substitterm 0 ev.(i) (mkRel (1)) (lift 1 t))))
 in
 if Array.length evararr = 0 (* Is there a Fixpoint? *)
	then (* No Fixpoint *)
		 (mkLambda ((Name (id_of_string ("Q"))), 
		 prod_change_concl ftyp mkthesort,
   (substitterm 0 gl (mkRel 1) princ_proof_hyps)))
	else
   princ_replace_metas evararr absc 0 princ_proof_hyps

    
(* Declaration of the functional scheme. *)
let declareFunScheme f fname mutflist =
 let scheme = 
   buildFunscheme (constr_of f) 
    (Array.of_list (List.map constr_of (f::mutflist))) in
  let _ = prstr "Principe:" in
  let _ = prconstr scheme in
 let ce = { 
  const_entry_body = scheme;
  const_entry_type = None;
  const_entry_opaque = false } in
 let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition)) in
 ()



VERNAC COMMAND EXTEND FunctionalScheme
 [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" 
    constr(c) "with" constr_list(l) ]
  -> [ declareFunScheme c na l ]
| [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" constr(c) ]
  -> [ declareFunScheme c na [] ]
END

 



(* 
*** Local Variables: ***
*** compile-command: "make -C ../.. contrib/funind/tacinv.cmo" ***
*** tab-width: 1 ***
*** tuareg-default-indent:1 ***
*** tuareg-begin-indent:1 ***
*** tuareg-let-indent:1 ***
*** tuareg-match-indent:-1 ***
*** tuareg-try-indent:1 ***
*** tuareg-with-indent:1 ***
*** tuareg-if-then-else-inden:1 ***
*** fill-column: 78 ***
*** indent-tabs-mode: nil ***
*** End: ***
*)