summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
commit6497f27021fec4e01f2182014f2bb1989b4707f9 (patch)
tree473be7e63895a42966970ab6a70998113bc1bd59 /contrib
parent6b649aba925b6f7462da07599fe67ebb12a3460e (diff)
Imported Upstream version 8.0pl2upstream/8.0pl2
Diffstat (limited to 'contrib')
-rw-r--r--contrib/funind/tacinv.ml461
-rw-r--r--contrib/funind/tacinvutils.ml7
-rw-r--r--contrib/interface/xlate.ml12
3 files changed, 51 insertions, 29 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index d2ae12d6..b358ff39 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -68,6 +68,7 @@ let id_of_name = function
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 =
@@ -163,6 +164,8 @@ let rec npatternify ltypes c =
(* 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
@@ -373,7 +376,8 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs:
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,[]
+ mkFix((iarr,i),(anme, pisarr,aappel_rec))
+ , (pop1_levar llevar) , llposeq,evararr,pisarr,[]
(* <pcase> Cases b of arrPt end.*)
| Case(cinfo, pcase, b, arrPt) ->
@@ -495,7 +499,7 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs:
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 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)
@@ -510,7 +514,8 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs:
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. *)
+ 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
@@ -539,9 +544,6 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs:
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 =
@@ -619,7 +621,7 @@ let invfun_basic open_princ_proof_applied listargs_ids gl dorew lposeq =
(tclTHEN
(* Refine on the right term (following the sheme of the
given function) *)
- (fun gl -> refine open_princ_proof_applied gl)
+ (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))))
@@ -689,20 +691,17 @@ let invfun c l dorew gl =
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
-
+ 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,
@@ -710,14 +709,20 @@ let invfun c l dorew gl =
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
-
+ 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')
+ (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
@@ -725,8 +730,12 @@ let invfun c l dorew gl =
| ((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
@@ -734,12 +743,15 @@ let invfun c l dorew gl =
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 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
@@ -750,8 +762,7 @@ let invfun_verif c l dorew gl =
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))
+ with UserError (x,y) -> raise (UserError (x,y))
else error "wrong number of arguments for the function"
@@ -790,7 +801,7 @@ let buildFunscheme fonc mutflist =
in
let rec princ_replace_params params t =
List.fold_left (
- fun acc ev,nam,typ ->
+ 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
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 758071ba..6e086d95 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -20,7 +20,8 @@ open Reductionops
(*s printing of constr -- debugging *)
-let msg x = () ;; let prterm c = str "" (* comment this to see debug msgs *)
+(* comment this line to see debug msgs *)
+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
@@ -67,6 +68,10 @@ let rec mkevarmap_from_listex lex =
match lex with
| [] -> Evd.empty
| ((ex,_),typ)::lex' ->
+(* let _ = prstr "mkevarmap" in
+ let _ = prstr ("evar n. " ^ string_of_int ex ^ " ") in
+ let _ = prstr "OF TYPE: " in
+ let _ = prconstr typ in*)
let info ={
evar_concl = typ;
evar_hyps = empty_named_context;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ed51b9cb..50f5b947 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -884,7 +884,7 @@ and xlate_tac =
| _ -> assert false)
| _ -> assert false)
| TacExtend (_, "refine", [c]) ->
- CT_refine (xlate_formula (out_gen rawwit_casted_open_constr c))
+ CT_refine (xlate_formula (snd (out_gen rawwit_casted_open_constr c)))
| TacExtend (_,"absurd",[c]) ->
CT_absurd (xlate_formula (out_gen rawwit_constr c))
| TacExtend (_,"contradiction",[opt_c]) ->
@@ -1230,11 +1230,16 @@ and coerce_genarg_to_TARG x =
| TacticArgType ->
let t = xlate_tactic (out_gen rawwit_tactic x) in
CT_coerce_TACTIC_COM_to_TARG t
+ | OpenConstrArgType ->
+ CT_coerce_SCOMMENT_CONTENT_to_TARG
+ (CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
+ (snd (out_gen
+ rawwit_open_constr x))))
| CastedOpenConstrArgType ->
CT_coerce_SCOMMENT_CONTENT_to_TARG
(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
- (out_gen
- rawwit_casted_open_constr x)))
+ (snd (out_gen
+ rawwit_casted_open_constr x))))
| ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
| BindingsArgType -> xlate_error "TODO: generic with bindings"
| RedExprArgType -> xlate_error "TODO: generic red expr"
@@ -1324,6 +1329,7 @@ let coerce_genarg_to_VARG x =
| TacticArgType ->
let t = xlate_tactic (out_gen rawwit_tactic x) in
CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
+ | OpenConstrArgType -> xlate_error "TODO: generic open constr"
| CastedOpenConstrArgType -> xlate_error "TODO: generic open constr"
| ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
| BindingsArgType -> xlate_error "TODO: generic with bindings"