summaryrefslogtreecommitdiff
path: root/contrib/funind
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind')
-rw-r--r--contrib/funind/tacinv.ml4853
-rw-r--r--contrib/funind/tacinvutils.ml277
-rw-r--r--contrib/funind/tacinvutils.mli79
3 files changed, 1209 insertions, 0 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
new file mode 100644
index 00000000..d2ae12d6
--- /dev/null
+++ b/contrib/funind/tacinv.ml4
@@ -0,0 +1,853 @@
+(*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 *)
+
+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
+
+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. *)
+ (* 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 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
+
+ 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
+
+ (* 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
+
+
+(*
+ (* 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 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 _ = 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: ***
+*)
+
+
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
new file mode 100644
index 00000000..758071ba
--- /dev/null
+++ b/contrib/funind/tacinvutils.ml
@@ -0,0 +1,277 @@
+(* tacinvutils.ml *)
+(*s utilities *)
+
+(*i*)
+open Names
+open Util
+open Term
+open Termops
+open Coqlib
+open Pp
+open Printer
+open Inductiveops
+open Environ
+open Declarations
+open Nameops
+open Evd
+open Sign
+open Reductionops
+(*i*)
+
+(*s printing of constr -- debugging *)
+
+let msg x = () ;; let prterm c = str "" (* comment this to see debug msgs *)
+ (* uncomment this to see debugging *)
+let prconstr c = msg (str" " ++ prterm c ++ str"\n")
+let prlistconstr lc = List.iter prconstr lc
+let prstr s = msg(str s)
+
+let prchr () = msg (str" (ret) \n")
+let prNamedConstr s c =
+ begin
+ msg(str "");
+ msg(str(s^"==>\n ") ++ prterm c ++ str "\n<==\n");
+ msg(str "");
+ end
+
+let prNamedLConstr_aux lc =
+ List.iter (prNamedConstr "#>") lc
+
+let prNamedLConstr s lc =
+ begin
+ prstr s;
+ prNamedLConstr_aux lc
+ end
+
+
+(* FIXME: ref 1, pas bon, si? *)
+let evarcpt = ref 0
+let metacpt = ref 0
+let mknewexist ()=
+ begin
+ evarcpt := !evarcpt+1;
+ !evarcpt,[||]
+ end
+
+let resetexist ()= evarcpt := 0
+
+let mknewmeta ()=
+ begin
+ metacpt := !metacpt+1;
+ mkMeta (!metacpt)
+ end
+
+let resetmeta () = metacpt := 0
+
+let rec mkevarmap_from_listex lex =
+ match lex with
+ | [] -> Evd.empty
+ | ((ex,_),typ)::lex' ->
+ let info ={
+ evar_concl = typ;
+ evar_hyps = empty_named_context;
+ evar_body = Evar_empty} in
+ Evd.add (mkevarmap_from_listex lex') ex info
+
+let mkEq typ c1 c2 =
+ mkApp (build_coq_eq(),[| typ; c1; c2|])
+
+let mkRefl typ c1 =
+ mkApp ((build_coq_eq_data()).refl, [| typ; c1|])
+
+let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
+
+
+(* 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)
+let name_of_string str = Name (id_of_string str)
+let newname_append nme str =
+ Name(id_of_string ((string_of_id (id_of_name nme))^str))
+
+(* Substitutions in constr *)
+
+let compare_constr_nosub t1 t2 =
+ if compare_constr (fun _ _ -> false) t1 t2
+ then true
+ else false
+
+let rec compare_constr' t1 t2 =
+ if compare_constr_nosub t1 t2
+ then true
+ else (compare_constr (compare_constr') t1 t2)
+
+let rec substitterm prof t by_t in_u =
+ if (compare_constr' (lift prof t) in_u)
+ then (lift prof by_t)
+ else map_constr_with_binders succ
+ (fun i -> substitterm i t by_t) prof in_u
+
+
+let apply_eqtrpl eq t =
+ let r,(tb,b,by_t) = eq in
+ substitterm 0 b by_t t
+
+let apply_eqtrpl_lt lt eq = List.map (apply_eqtrpl eq) lt
+
+let apply_leqtrpl_t t leq =
+ List.fold_left (fun x y -> apply_eqtrpl y x) t leq
+
+
+let apply_refl_term eq t =
+ let _,arr = destApplication eq in
+ let reli= (Array.get arr 1) in
+ let by_t= (Array.get arr 2) in
+ substitterm 0 reli by_t t
+
+let apply_eq_leqtrpl leq eq =
+ List.map
+ (function (r,(tb,b,t)) ->
+ r,(tb,
+ (if isRel b then b else (apply_refl_term eq b)), apply_refl_term eq t))
+ leq
+
+
+
+(* [(a b c) a] -> true *)
+let constr_head_match u t=
+ if isApp u
+ then
+ let uhd,args= destApplication u in
+ uhd=t
+ else false
+
+(* My operations on constr *)
+let lift1L l = (List.map (lift 1) l)
+let mkArrow_lift t1 t2 = mkArrow t1 (lift 1 t2)
+let mkProd_liftc nme c1 c2 = mkProd (nme,c1,(lift 1 c2))
+(* prod_it_lift x [a1 a2 ...] *)
+let prod_it_lift ini lcpl =
+ List.fold_right (function a,b -> (fun c -> mkProd_liftc a b c)) ini lcpl;;
+
+let prod_it_anonym_lift trm lst = List.fold_right mkArrow_lift lst trm
+
+let lam_it_anonymous trm lst =
+ List.fold_right
+ (fun elt res -> mkLambda(Name(id_of_string "Hrec"),elt,res)) lst trm
+
+let lambda_id id typeofid cstr =
+ let cstr' = mkNamedLambda (id_of_string "FUNX") typeofid cstr in
+ substitterm 0 id (mkRel 0) cstr'
+
+let prod_id id typeofid cstr =
+ let cstr' = mkNamedProd (id_of_string "FUNX") typeofid cstr in
+ substitterm 0 id (mkRel 0) cstr'
+
+
+
+
+
+let nth_dep_constructor indtype n =
+ let sigma = Evd.empty and env = Global.env() in
+ let indtypedef = find_rectype env sigma indtype in
+ let indfam,_ = dest_ind_type indtypedef in
+ let arr_cstr_summary = get_constructors env indfam in
+ let cstr_sum = Array.get arr_cstr_summary n in
+ build_dependent_constructor cstr_sum, cstr_sum.cs_nargs
+
+
+let rec buildrefl_from_eqs eqs =
+ match eqs with
+ | [] -> []
+ | cstr::eqs' ->
+ let eq,args = destApplication cstr in
+ (mkRefl (Array.get args 0) (Array.get args 2))
+ :: (buildrefl_from_eqs eqs')
+
+
+
+
+(* list of occurrences of a term inside another, no imbricated
+ occurrence are considered (ie we stop looking inside a termthat is
+ an occurrence). *)
+let rec hdMatchSub u t=
+ if constr_head_match u t then
+ u::(fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
+ []
+ u)
+ else
+ fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
+ []
+ u
+
+(* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *)
+let hdMatchSub_cpl u (d,f) =
+ let res = ref [] in
+ begin
+ for i = d to f do res := (hdMatchSub u (mkRel i)) @ !res done;
+ !res
+ end
+
+
+(* destApplication raises an exception if [t] is not an application *)
+let exchange_hd_prod subst_hd t =
+ let (hd,args)= destApplication t in mkApp (subst_hd,args)
+
+(* substitute t by by_t in head of products inside in_u, reduces each
+ product found *)
+let rec substit_red prof t by_t in_u =
+ if constr_head_match in_u (lift prof t)
+ then
+ let _ = prNamedConstr "in_u" in_u in
+ let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in
+ let _ = prNamedConstr "xx " x in
+ let _ = prstr "\n\n" in
+ x
+ else
+ map_constr_with_binders succ (fun i u -> substit_red i t by_t u)
+ prof in_u
+
+(* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each
+ reli by tarr.(f-i). *)
+let exchange_reli_arrayi tarr (d,f) t =
+ let hd,args= destApplication t in
+ let i = destRel hd in
+ whd_beta (mkApp (tarr.(f-i) ,args))
+
+let exchange_reli_arrayi_L tarr (d,f) =
+ List.map (exchange_reli_arrayi tarr (d,f))
+
+
+(* expand all letins in a term, before building the principle. *)
+let rec expand_letins mimick =
+ match kind_of_term mimick with
+ | LetIn(nme,cstr1, typ, cstr) ->
+ let cstr' = substitterm 0 (mkRel 1) (lift 1 cstr1) cstr in
+ expand_letins (pop cstr')
+ | x -> map_constr expand_letins mimick
+
+
+(* Valeur d'une constante, or identity *)
+let def_of_const t =
+ match kind_of_term t with
+ | Const sp ->
+ (try
+ match Global.lookup_constant sp with
+ {const_body=Some c} -> force c
+ |_ -> assert false
+ with _ -> assert false)
+ | _ -> t
+
+(* nom d'une constante. Must be a constante. x*)
+let name_of_const t =
+ match (kind_of_term t) with
+ Const cst -> Names.string_of_label (Names.label cst)
+ |_ -> assert false
+ ;;
+
+
+(*i
+*** Local Variables:
+*** compile-command: "make -k tacinvutils.cmo"
+*** test-tactic: "../../bin/coqtop -translate -q -batch -load-vernac-source ../../test-suite/success/Funind.v"
+*** End:
+i*)
+
diff --git a/contrib/funind/tacinvutils.mli b/contrib/funind/tacinvutils.mli
new file mode 100644
index 00000000..2fc37b2c
--- /dev/null
+++ b/contrib/funind/tacinvutils.mli
@@ -0,0 +1,79 @@
+(* tacinvutils.ml *)
+(*s utilities *)
+
+(*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 Evd
+(*i*)
+
+(* printing debugging *)
+val prconstr: constr -> unit
+val prlistconstr: constr list -> unit
+val prNamedConstr:string -> constr -> unit
+val prNamedLConstr:string -> constr list -> unit
+val prstr: string -> unit
+
+
+val mknewmeta: unit -> constr
+val mknewexist: unit -> existential
+val resetmeta: unit -> unit (* safe *)
+val resetexist: unit -> unit (* be careful with this one *)
+val mkevarmap_from_listex: (Term.existential * Term.types) list -> evar_map
+val mkEq: types -> constr -> constr -> constr
+(* let mkEq typ c1 c2 = mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) *)
+val mkRefl: types -> constr -> constr
+val buildrefl_from_eqs: constr list -> constr list
+(* typ c1 = mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"), [| typ; c1|]) *)
+
+val nth_dep_constructor: constr -> int -> (constr*int)
+
+val prod_it_lift: (name*constr) list -> constr -> constr
+val prod_it_anonym_lift: constr -> constr list -> constr
+val lam_it_anonymous: constr -> constr list -> constr
+val lift1L: (constr list) -> constr list
+val popn: int -> constr -> constr
+val lambda_id: constr -> constr -> constr -> constr
+val prod_id: constr -> constr -> constr -> constr
+
+
+val name_of_string : string -> name
+val newname_append: name -> string -> name
+
+val apply_eqtrpl: constr*(constr*constr*constr) -> constr -> constr
+val substitterm: int -> constr -> constr -> constr -> constr
+val apply_leqtrpl_t:
+ constr -> (constr*(constr*constr*constr)) list -> constr
+val apply_eq_leqtrpl:
+ (constr*(constr*constr*constr)) list -> constr -> (constr*(constr*constr*constr)) list
+(* val apply_leq_lt: constr list -> constr list -> constr list *)
+
+val hdMatchSub: constr -> constr -> constr list
+val hdMatchSub_cpl: constr -> int*int -> constr list
+val exchange_hd_prod: constr -> constr -> constr
+val exchange_reli_arrayi_L: constr array -> int*int -> constr list -> constr list
+val substit_red: int -> constr -> constr -> constr -> constr
+val expand_letins: constr -> constr
+
+val def_of_const: constr -> constr
+val name_of_const: constr -> string
+(*i
+ Local Variables:
+ compile-command: "make -k tacinvutils.cmi"
+ End:
+i*)
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 20:05:29 +0000