path: root/contrib/funind/tacinv.ml4

(*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 rec split3 l = 
  List.fold_right (fun (e1,e2,e3) (a,b,c) -> (e1::a),(e2::b),(e3::c)) 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

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

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

(* Take two terms with same structure and return a map of deBruijn from the
   first to the second. Only DeBruijn should be different between the two
   terms. *)
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
  | Const c1, Const c2  when c1=c2 -> Smap.empty
  | Ind c1, Ind c2 when c1=c2 -> Smap.empty
  | Rel i, Rel j when i=j -> Smap.empty
  | Rel i, Rel j -> 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) when Array.length args = Array.length argsb ->
     build_rel_map_list (Array.to_list args) (Array.to_list argsb)
  | _,_ -> 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 *)

(* This is the type of the argument of [proofPrinc] *)

type mimickinfo =
    {
     concl: constr; (* conclusion voulue, cad (xi:ti)gl, ou gl est le but a
                       prouver, et xi:ti correspondent aux arguments donnés à
                       la tactique.  On enlèvera un produit à chaque fois
                       qu'on rencontrera un binder, sans lift ou pop.
                       Initialement: une seule conclusion, puis specifique à
                       chaque branche. *)
     absconcl: constr array; (* conclusions patternisées pour pouvoir être
                                appliquées = un predicat pour chaque fixpt
                                mutuel. *)
     mimick: constr; (* le terme qu'on imite. On plongera  dedans au fur et
                        à mesure, sans lift ni pop. *)
     env: env; (* The global typing environment, we will add thing in it when
                  going inside the term (push_rel, push_rec_types) *)
     sigma: Evd.evar_map; 
     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)). *)
     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).  *)
     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 *)
     lst_vars: (constr*(name*constr)) list ; (* Variables rencontrées jusque là *)
     lst_eqs: (Term.constr * (Term.constr * Term.constr * Term.constr)) list ; 
                                   (* liste d'équations engendrées au cours du
                                      parcours, cette liste grandit à chaque
                                      case, et il faut lifter le tout à chaque
                                      binder *)
     lst_recs: constr list ; (* appels récursifs rencontrés jusque là *)
    }

(* This is the return type of [proofPrinc] *)
type 'a funind = (* 'A = CONTR  OU  CONSTR ARRAY *)
    {

     princ:'a; (* le (ou les) principe(s) demandé(s), 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. *)
     evarlist: (constr*Term.types) list; (* [(ev1,tev1);(ev2,tev2)...]]
                                            l'ensemble des meta variables
                                            correspondant à des trous. [evi]
                                            est la meta variable, [tevi] est
                                            son type. *)
     hypnum: (int*int*int) list; (* [[(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. *)
     mutfixmetas: constr array ; (* un tableau de meta variables correspondant
                                    à chacun des prédicats mutuellement
                                    récursifs construits. *)
     conclarray: types array; (* un tableau contenant les conclusions
                                 respectives de chacun des prédicats
                                 mutuellement récursifs. Permet de finir la
                                 construction du principe. *)
     params:(constr*name*constr) list; (* [[(metavar,param,tparam)..]] la
                                          liste des paramètres (les lambdas
                                          au-dessus du fix) du fixpoint si
                                          fixpoint il y a, le paramètre est
                                          une meta var, dont on stocke le nom
                                          et le type. TODO: utiliser la
                                          structure adequat? *)
    }



let empty_funind_constr =
    {
     princ = mkProp;
     evarlist = [];
     hypnum = [];
     mutfixmetas = [||];
     conclarray = [||];
     params = []
    }

let empty_funind_array =
    { empty_funind_constr with
     princ = [||];
    }

(* Replace the calls to the function (recursive calls) by calls to the
   corresponding constant  *)
let replace_reccalls mi b =
 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
 !res
 


(* collects all information of match branches stored in [l] *)
let rec collect_cases l =
 match l with
  | [||] -> empty_funind_array
  | arr -> 
     let x = arr.(0) in
     let resrec = collect_cases (Array.sub arr 1 (Array.length arr - 1)) in
     { x with
      princ= Array.append [|x.princ|] resrec.princ;
      evarlist = x.evarlist@resrec.evarlist;
      hypnum = x.hypnum@resrec.hypnum;
     }

let collect_pred l = 
 let l1,l2,l3 = split3 l in
 Array.of_list l1 , Array.of_list l2 , Array.of_list l3


(* [build_pred n tarr] builds the right predicates for each element of [tarr]
   (of type: [type array] of size [n]). Return the list of triples: 
   (?i , 
   fun (x1:t1) ... (xn:tn) => (?i x1...xn) ,
   forall (x1:t1) ... (xn:tn), (?i x1...xn)),
   where ti's are deduced from elements of tarr, which are of the form:
   t1 -> t2 -> ... -> tn -> <nevermind>. *)
let rec build_pred n tarr =
 if n >= Array.length tarr (* 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) tarr


let heq_prefix = "H_eq_"

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

(* the main function, build the principle by exploring the term and reproduce
   the same structure. *)
let rec proofPrinc mi: constr funind =
 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 evararr,newabsconcl,pisarr = collect_pred (build_pred 0 tarr) in
     let newenv = push_rec_types (narr,tarr,carr) mi.env in
     let anme',aappel_rec,llevar,llposeq = 
      collect_fix mi 0 iarr narr carr pisarr newabsconcl newenv in
     let anme = Array.map (fun nme -> newname_append nme "_ind") anme' in
     { 
      princ = mkFix((iarr,i),(anme, pisarr,aappel_rec));
      evarlist= pop1_levar llevar; (* llevar are put outside the fix, so we pop 1 *)
      hypnum = llposeq;
      mutfixmetas = evararr;
      conclarray = pisarr;
      params = []
     }
  (* <pcase> Cases b of arrPt end.*)
  | Case (cinfo, pcase, b, arrPt) -> 
     let prod_pcase,_ = decompose_lam pcase in
     let _nmeb,_ = List.hd prod_pcase in
     let newb'= apply_leqtrpl_t b mi.lst_eqs in
     let type_of_b = Typing.type_of mi.env mi.sigma b in
     (* Replace the recursive calls to the function by calls to the constant *)
     let newb = replace_reccalls mi newb' in     
     let cases = collect_cases (Array.mapi (fold_proof mi b type_of_b newb) arrPt) in
     (* the match (case) annotation must be transformed, see [build_pcase] below *)
     let newpcase = build_pcase mi pcase b type_of_b newb in
     let trm' = mkCase (cinfo,newpcase,newb, cases.princ) in
    { cases with
     princ = if mi.doeqs then mkApp (trm',[|(mkRefl type_of_b newb)|]) else trm';
     params = [] (* FIX: fix parms here (fixpt inside a match)*)
    }


  | 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 newlst_var = (* if this lambda is a param, then don't add it here *)
      if mi.fix then (mkRel 1,(nme,typ)) :: lift1_lvars mi.lst_vars
      else (*(mkRel 1,(nme,typ)) :: *) lift1_lvars mi.lst_vars 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);
      lst_vars = newlst_var ; lst_eqs = lift1_leqs mi.lst_eqs;
      lst_recs = lift1L mi.lst_recs} in
     let resrec = proofPrinc newmi in
     (* are we inside a fixpoint or a case? then this is a normal lambda *)
     if mi.fix 
     then { resrec with princ = mkLambda (nme,typ,resrec.princ) ; params = [] }
     else (* otherwise this is a parameter *)
       let metav = mknewmeta() in
       let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in
       { resrec with
        princ = substmeta resrec.princ;
        evarlist = List.map (fun (ev,tev) -> ev, substmeta tev) resrec.evarlist;
        conclarray = Array.map substmeta resrec.conclarray;
        params = (metav,nme,typ) :: resrec.params
       }


  | 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 mi.lst_vars) in
     let varnames = List.map snd mi.lst_vars in
     let nb_vars = List.length varnames in
     let nb_eqs = List.length mi.lst_eqs in
     let _eqrels = List.map fst mi.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 = mi.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
     { empty_funind_constr with
      princ = conclrecs;
      evarlist = [ newmeta , typeofhole ];
      hypnum = [ nb_vars , List.length terms_recs , nb_eqs ];
      conclarray = mi.absconcl;
     }

     
(* C'est un peu compliqué ici: en cas de type inductif vraiment dépendant
   l'annotation de type du case [pcase] contient des lambdas supplémentaires
   en tête. Je les récupère dans la variable [suppllam_pcase]. Le problème est
   que la conclusion de l'annotation du nouveauacse doit faire référence à ces
   variables plutôt qu'à celle de l'exterieur. Ce qui suit permet de changer
   les reference de newpcase' pour pointer vers les lambda du piquant. On
   procède comme suit: on repère les rels qui pointent à l'interieur de
   l'annotation dans la fonction initiale et on les relie à celle du type
   voulu pour le case, pour ça ([build_rel_map]) on parcourt en même temps le
   dernier lambda du piquant ([typ]) (qui contient le type de l'argument du
   case) et le type attendu pour le case ([type_of_b]) et on construit un
   map. Ensuite on remplace les rels correspondant dans la preuve construite
   en suivant le map. *)
     
and build_pcase mi pcase b type_of_b newb =
     let prod_pcase,_ = decompose_lam pcase in
     let nme,typ = List.hd 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 typeof_case'' = substitterm 0 (lift 1 b) (mkRel 1) (lift 1 mi.concl) in
     let suppllam_pcase = List.tl prod_pcase in
     let suppllam_pcasel = List.length suppllam_pcase  in
     let rel_smap = 
      if suppllam_pcasel=0 then Smap.empty else (* FIX: is this test necessary ? *)
        build_rel_map (lift suppllam_pcasel type_of_b) typ in
     let newpcase''' =  
      Smap.fold (fun e e' acc -> substitterm 0 e (lift 1 e') acc)
       rel_smap typeof_case'' in
     let neweq = mkEq (lift (suppllam_pcasel + 1) type_of_b) 
      (lift (suppllam_pcasel + 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 newpcase' = mkLambda (newname_append nme "_ind" ,typ, newpcase'') in
     (* ajout des lambdas supplémentaires (type dépendant) du piquant. *)
     lamn suppllam_pcasel suppllam_pcase newpcase'


(* [fold_proof mi b typeofb newb l n] rend le resultat de l'appel recursif sur
   cstr (correpsondant au ième elt de [arrPt] ci-dessus et donc au ième
   constructeur de [typeofb]), appele avec les bons arguments: [mi.concl]
   devient [(DUMMY1:t1;...;DUMMY:tn)concl'], ou [n] est le nombre d'arguments
   du constructeur considéré, et [concl'] est [mi.concl] ou l'on a réécrit [b]
   en ($c_n$ [rel1]...). *)
and fold_proof mi b type_of_b newb i cstr = 
 let new_lst_recs = mi.lst_recs @ hdMatchSub_cpl b mi.fonc in
 (* 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 i 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 mi.lst_eqs neweq in
 let new_lsteqs = (mkRel (-nargs),(type_of_b,newb, popn nargs cstr_appl))::lsteqs_rew in
 let a',a'' = decompose_lam_n nargs cstr 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; 
  lst_eqs= new_lsteqs; lst_recs = new_lst_recs} in
 proofPrinc newmi 


and collect_fix mi n iarr narr carr pisarr newabsconcl newenv =
 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;
    lst_vars=lift1_lvars mi.lst_vars; lst_eqs=lift1_leqs mi.lst_eqs; 
    lst_recs= lift1L mi.lst_recs;} in
   let resrec = proofPrinc newmi  in
   let lnme,lappel_rec,llevar,llposeq = 
    collect_fix mi (n+1) iarr narr carr pisarr newabsconcl newenv in
   Array.append [|nme|] lnme , Array.append [|resrec.princ|] lappel_rec
    , (resrec.evarlist@llevar) , (resrec.hypnum@llposeq)

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 ; 
 lst_vars = []; lst_eqs = []; lst_recs = []} in
 proofPrinc mi

(* 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 (str "Cannot rewrite"))
      )) gl)


(* 
       (fun hyp gl -> 
        let _ = prstr ("nthhyp= "^ string_of_int i) in
        if isConst hyp && ((name_of_const hyp)==heq_prefix) then
          let _ = prstr "YES\n" in
          rewriteLR hyp gl 
        else 
          let _ = prstr "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,_ = destApp 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 pr = 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 pr.params)) in
 (* we apply args of the fix now, the parameters will be applied later *)
 let princ_proof_applied_args = 
  applistc pr.princ (listsuf (List.length pr.params) listargs') in
 (* parameters are still there so patternify must not take them -> lift *)
 let princ_proof_applied_lift = 
  lift (List.length pr.evarlist) princ_proof_applied_args in
 let princ_applied_hyps'' = patternify (List.rev pr.evarlist)
  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 pr.mutfixmetas > 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 pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*) 
    (substit_red 0 (pr.mutfixmetas.(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 pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*) 
    List.map (fun (x,y) -> x,substit_red 0 (pr.mutfixmetas.(0)) gl_abstr y) pr.evarlist 
  else pr.evarlist
 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 pr.params 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 pr.params listargs' y) newlevar') in
(*
 (* replace params metavar by abstracted variables *)
  let princ_proof_params = npatternify (List.rev pr.params) princ_applied_hyps in
 (* we apply now the real parameters *)
 let princ_proof_applied = 
  applistc princ_proof_params (listpref (List.length pr.params) 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 pr.hypnum

(* 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"




(* 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 =  *)
 let _ = prstr "Recherche du principe... lancement de invfun_proof\n" in
 let pr = 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 pr.evarlist) pr.princ in
 let princ_proof_hyps = 
  patternify (List.rev pr.evarlist) 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 pr.mutfixmetas = 0 (* Is there a Fixpoint? *)
	then (* No Fixpoint *)
   princ_replace_params pr.params (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 pr.mutfixmetas pr.conclarray 0 princ_proof_hyps in
   princ_replace_params pr.params princ_rpl


    
(* Declaration of the functional scheme. *)
let declareFunScheme f fname mutflist =
 let _ = prstr "Recherche du perincipe...\n" in
 let id_to_cstr id = 
  try constr_of_id (Global.env()) id 
  with
     Not_found -> error (string_of_id id ^ " not found in the environment") in
 let flist = if mutflist=[] then [f] else mutflist in
 let fcstrlist = Array.of_list (List.map id_to_cstr flist) in
 let idf = id_to_cstr f in
 let scheme = buildFunscheme idf fcstrlist in
  let _ = prstr "Principe:" in
  let _ = prconstr scheme in
 let ce = { 
  const_entry_body = scheme;
  const_entry_type = None;
  const_entry_opaque = false;
  const_entry_boxed = true } in
 let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition Scheme)) in
 ()



TACTIC EXTEND functional_induction
  [ "old" "functional" "induction" constr(c)  ne_constr_list(l) ] 
     -> [ invfun_verif c l true ]
END

VERNAC COMMAND EXTEND FunctionalScheme
 [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" 
    ident(c) "with" ne_ident_list(l) ] 
  -> [ declareFunScheme c na l ]
| [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (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: ***
*)