diff options
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 23 | ||||
| -rw-r--r-- | contrib/funind/tacinvutils.ml | 53 |
2 files changed, 37 insertions, 39 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index b358ff39..1500e1ae 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -157,11 +157,9 @@ let rec npatternify ltypes c = | [] -> 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 @@ -510,15 +508,15 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs: | 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 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 - + 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. *) @@ -573,7 +571,6 @@ let invfun_proof fonc def_fonc gl_abstr pis env sigma = 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 = @@ -596,12 +593,12 @@ let rec iterintro i = (* (fun hyp gl -> - let _ = print_string ("nthhyp= "^ string_of_int i) in + let _ = prstr ("nthhyp= "^ string_of_int i) in if isConst hyp && ((name_of_const hyp)==heq_prefix) then - let _ = print_string "YES\n" in + let _ = prstr "YES\n" in rewriteLR hyp gl else - let _ = print_string "NO\n" in + let _ = prstr "NO\n" in tclIDTAC gl) *) @@ -818,9 +815,9 @@ let buildFunscheme fonc mutflist = (* 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 flist = if mutflist=[] then [f] else mutflist in + let fcstrlist = Array.of_list (List.map constr_of flist) in + let scheme = buildFunscheme (constr_of f) fcstrlist in let _ = prstr "Principe:" in let _ = prconstr scheme in let ce = { diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index 6e086d95..a125b9a7 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -21,7 +21,7 @@ open Reductionops (*s printing of constr -- debugging *) (* comment this line to see debug msgs *) -let msg x = () ;; let prterm c = str "" +let msg x = () ;; let prterm c = str "" (* uncomment this to see debugging *) let prconstr c = msg (str" " ++ prterm c ++ str"\n") let prlistconstr lc = List.iter prconstr lc @@ -194,52 +194,53 @@ let rec 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). *) +(* list of occurrences of a term inside another *) +(* Cofix will be wrong, not sure Fix is correct too *) 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 subres = + match kind_of_term u with + | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> hdMatchSub (lift 1 cstr) t + | Fix (_,(lna,tl,bl)) -> + Array.fold_left + (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) t) + [] bl + | LetIn _ -> assert false + (* Correct? *) + | _ -> fold_constr (fun l cstr -> l @ hdMatchSub cstr t) [] u + in + if constr_head_match u t then u :: subres else subres + (* 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 + 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) + 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 + let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in + x else - map_constr_with_binders succ (fun i u -> substit_red i t by_t u) - prof in_u + 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 res = whd_beta (mkApp (tarr.(f-i) ,args)) in + res let exchange_reli_arrayi_L tarr (d,f) = List.map (exchange_reli_arrayi tarr (d,f)) |