(*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 rec listsuf i l = if i<=0 then l else listsuf (i-1) (List.tl l)
let rec listpref i l = if i<=0 then [] else List.hd l :: listpref (i-1) (List.tl l)

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)
(* Operations on names *)
let id_of_name = function
    Anonymous -> id_of_string "H"
  | Name id   -> id;;
let string_of_name nme = string_of_id (id_of_name nme)
 (*end debugging *)

(* Interpretation of constr's *)
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,g)= 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, g

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 pop1_levar levars = List.map (function ev,tev -> ev, popn 1 tev) levars


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
     let tlift = lift (List.length ltypes') t in
     let res = 
      patternify ltypes' (mkLambda (newname_append nme "rec", tlift, c')) nme in
     res

let rec npatternify ltypes c =
 match ltypes with
  | [] -> c
  | (mv,nme,t)::ltypes' -> 
     let c'= substitterm 0 mv (mkRel 1) c in
(*      let _ = prconstr c' in *)
     let tlift = lift (List.length ltypes') t in
     let res = 
      npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in
(*      let _ = prconstr res in *)
     res

(* fait une application (c m1 m2...mn, où mi est une evar, on rend également
   la liste des evar munies de leur type) *)
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 
 let res = mkAppRel c ltyp (List.length ltyp) in
 res


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) *)
     fix: bool (* did I already went through a fix or case constr? lambdas
                  found before a case or a fix are treated as parameters of
                  the induction principle *)
    }

(*
  \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..|],
  [(param,tparam)..]]

 *)

(* This could be the return type of [proofPrinc], but not yet *)
type funind =
    {
     princ:constr;
     evarlist: (constr*Term.types) list;
     hypnum: (int*int*int) list;
     mutfixmetas: constr array ;
     conclarray: types array;
     params:(constr*name*constr) list
    }

(* 
  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 (suivant qu'on utilise le principe pour
  faire refine ou functional scheme). Il y 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.

  \item[[(param,tparam)..]] est la liste des paramètres (les lambda au-dessus
  du fix) du fixpoint si fixpoint il y a.

  \end{itemize}
*)
let heq_prefix = "H_eq_"

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

let rec proofPrinc mi lst_vars lst_eqs lst_recs:
 constr * (constr*Term.types) list * (int*int*int) list 
 * constr array * types array * (constr*name*constr) list =
 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;fix=true} in
        let appel_rec,levar,lposeq,_,evarrarr,parms = 
         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
     (* llevar are put outside the fix, so one level of rel must be removed *)
     mkFix((iarr,i),(anme, pisarr,aappel_rec))
      , (pop1_levar 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 heq_prefix,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 heq_prefix,lift nargs neweq,lift 1 b'')
       else b'' in
      let newconcl = prodn nargs b' newb'' in
      let newmi = {mi with mimick=newmimick; concl=newconcl; fix=true} in
      let a,b,c,d,e,p = proofPrinc newmi lst_vars new_lsteqs new_lst_recs in
      a,b,c,d,e,p
      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,[] (* fix parms here (fix inside case)*)
      
  | 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 newlst_var = (* if this lambda is a param, then don't add it here *)
      if mi.fix then (mkRel 1,(nme,typ)) :: lift1_lvars lst_vars
      else (*(mkRel 1,(nme,typ)) :: *) lift1_lvars lst_vars in
     let rec_call,levar,lposeq,evararr,absc,parms =
      proofPrinc newmi newlst_var (lift1_leqs lst_eqs) (lift1L lst_recs) in
     (* are we inside a fixpoint or a case? then this is a normal lambda *)
     if mi.fix then mkLambda (nme,typ,rec_call) , levar, lposeq,evararr,absc,[]
     else (* otherwise this is a parameter *)
       let metav = mknewmeta() in
       let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in
       let newrec_call = substmeta rec_call in
       let newlevar = List.map (fun (ev,tev) -> ev, substmeta tev) levar in
       let newabsc = Array.map substmeta absc in
       newrec_call,newlevar,lposeq,evararr,newabsc,((metav,nme, typ)::parms)

  | 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 avec ceux trouves dans u (ie
        mi.mimick). *)
     (* 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


(* 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 mi = {concl=pis; absconcl=gl_abstr; mimick=def_fonc; env=env;
 sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false} in
 let princ_proof,levar,lposeq,evararr,absc,parms = proofPrinc mi [] [] [] in
 princ_proof,levar,lposeq,evararr,absc,parms

(* Do intros [i] times, then do rewrite on all introduced hyps which are called
   like [heq_prefix], 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 (String.length heq_prefix)
         with _ -> "" (* different than [heq_prefix] *) in
        if sub=heq_prefix 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)==heq_prefix) 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*)



(* TODO: ne plus mettre les sous-but à l'exterieur, mais à l'intérieur (le bug
   de refine est normalement resolu). Ca permettra 2 choses: d'une part que
   les preuves soient plus simple, et d'autre part de fabriquer un terme de
   refine qui pourra s'aapliquer SANS FAIRE LES INTROS AVANT, ce qui est bcp
   mieux car fonctionne comme induction et plus comme inversion (pas de perte
   de connexion entre les hypothèse et les variables). *)

(*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
 (* 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 _ = resetmeta() in
 let princ_proof,levar, lposeq,evararr,_,parms = 
  invfun_proof [|fonc|] def_fonc [||] pis (pf_env gl) (project gl) in
 (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *)
 let gl_abstr' = add_lambdas (pf_concl gl) gl listargs' in
 (* apply parameters immediately *)
 let gl_abstr = 
  applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev parms)) in
 (* we apply args of the fix now, the parameters will be applied later *)
 let princ_proof_applied_args = 
  applistc princ_proof (listsuf (List.length parms) listargs') in
 (* parameters are still there so patternify must not take them -> lift *)
 let princ_proof_applied_lift = 
  lift (List.length levar) princ_proof_applied_args in
 let princ_applied_hyps'' = patternify (List.rev levar)
  princ_proof_applied_lift (Name (id_of_string "Hyp"))  in
 (* if there was a fix, we will not add "Q" as in funscheme, so we make a pop,
    TODO: find were we made the lift in proofPrinc instead and supress it here,
    and add lift in funscheme. *)
 let princ_applied_hyps' = 
  if Array.length evararr > 0 then popn 1 princ_applied_hyps''
  else princ_applied_hyps'' in 
 (* if there is was fix, we have to replace the meta representing the
    predicate of the goal by the abstracted goal itself. *)
 let princ_applied_hyps = 
  if Array.length evararr > 0 then (* mutual Fixpoint not treated in the tactic *) 
    (substit_red 0 (evararr.(0)) gl_abstr princ_applied_hyps')
  else princ_applied_hyps' (* No Fixpoint *) in
 let _ = prNamedConstr "princ_applied_hyps" princ_applied_hyps in
 (* Same thing inside levar *)
 let newlevar' = 
  if Array.length evararr > 0 then (* mutual Fixpoint not treated in the tactic *) 
    List.map (fun (x,y) -> x,substit_red 0 (evararr.(0)) gl_abstr y) levar 
  else levar
 in
 (* replace params metavar by real args *)
 let rec replace_parms lparms largs t = 
  match lparms, largs with
     [], _ -> t
   | ((p,_,_)::lp), (a::la) -> let t'= substitterm 0 p a t in replace_parms lp la t'
   | _, _ -> error "problem with number of args." in
 let princ_proof_applied = replace_parms parms listargs' princ_applied_hyps in
 let _ = prNamedLConstr "levar:" (List.map fst newlevar') in
 let _ = prNamedLConstr "levar types:" (List.map snd newlevar') in
 let _ = prNamedConstr "princ_proof_applied" princ_proof_applied in
 (* replace also in levar *)
 let newlevar = 
  List.rev (List.map (fun (x,y) -> x, replace_parms parms listargs' y) newlevar') in
(*
 (* replace params metavar by abstracted variables *)
  let princ_proof_params = npatternify (List.rev parms) princ_applied_hyps in
 (* we apply now the real parameters *)
 let princ_proof_applied = 
  applistc princ_proof_params (listpref (List.length parms) listargs') in
*)
 let princ_applied_evars = apply_levars princ_proof_applied newlevar in
 let open_princ_proof_applied = princ_applied_evars in
 let _ = prNamedConstr "princ_applied_evars" (snd princ_applied_evars) in
 let _ = prNamedLConstr "evars" (List.map snd (fst princ_applied_evars)) in
 let listargs_ids = List.map destVar (List.filter isVar listargs') in
 (* debug: impression du but*)
(*  let lgl = Evd.to_list (sig_sig gl) in *)
(*  let _ = prNamedLConstr "\ngl= " (List.map (fun x -> (snd x).evar_concl) lgl) in *)
(*  let _ = prstr "fin gl \n\n" 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 _ = resetmeta() 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,parms = 
  invfun_proof mutflist def_fonc [||] pis (Global.env()) Evd.empty in
 (* parameters are still there (unboud rel), and patternify must not take them
  -> lift*)
 let princ_proof_lift = lift (List.length levar) princ_proof in
 let princ_proof_hyps = 
  patternify (List.rev levar) princ_proof_lift (Name (id_of_string "Hyp"))  in
 let rec princ_replace_metas ev abs i t = 
  if i>= Array.length ev then t
  else (* fix? *)
    princ_replace_metas ev abs (i+1)
     (mkLambda (
      (Name (id_of_string ("Q"^(string_of_int i)))),
      prod_change_concl (lift 0 abs.(i)) mkthesort,
      (substitterm 0 ev.(i) (mkRel 1) (lift 0 t))))
 in
 let rec princ_replace_params params t = 
  List.fold_left (
   fun acc (ev,nam,typ) -> 
    mkLambda (Name (id_of_name nam) , typ, 
    substitterm 0 ev (mkRel 1) (lift 0 acc)))
   t (List.rev params) in
 if Array.length evararr = 0 (* Is there a Fixpoint? *)
	then (* No Fixpoint *)
   princ_replace_params parms (mkLambda ((Name (id_of_string "Q")), 
		 prod_change_concl ftyp mkthesort,
   (substitterm 0 gl (mkRel 1) princ_proof_hyps)))
	else (* there is a fix -> add parameters + replace metas *)
   let princ_rpl = princ_replace_metas evararr absc 0 princ_proof_hyps in
   princ_replace_params parms princ_rpl


    
(* 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" ne_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 ***
***  test-tactic: "../../bin/coqtop -translate -q -batch -load-vernac-source ../../test-suite/success/Funind.v" ***
*** End: ***
*)