X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=e318bd87c562c31547208b944565c1200a1cee1c;hb=fd648e40eb2c9c5b29cfa4408459511a74898d1d;hp=d26de444714f312904017658a0fe7739dd82ea7b;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index d26de4447..e318bd87c 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -72,7 +72,11 @@ let eta_expand metasenv context t arg = | C.Var (uri,exp_named_subst) -> let exp_named_subst' = aux_exp_named_subst n exp_named_subst in C.Var (uri,exp_named_subst') - | C.Meta _ + | C.Meta (i,l) -> + let l' = + List.map (function None -> None | Some t -> Some (aux n t)) l + in + C.Meta (i, l') | C.Sort _ | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty) @@ -326,7 +330,9 @@ let apply_tac ~term (proof, goal) = in let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in let (newproof, newmetasenv''') = - let subst_in = CicMetaSubst.apply_subst ((metano,bo')::subst) in + let subst_in = + CicMetaSubst.apply_subst ((metano,(context, bo'))::subst) + in subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv'' in @@ -453,7 +459,7 @@ let elim_tac ~term = let module U = UriManager in let module R = CicReduction in let module C = Cic in - let (curi,metasenv,_,_) = proof in + let (curi,metasenv,proofbo,proofty) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let termty = T.type_of_aux' metasenv context term in let uri,exp_named_subst,typeno,args = @@ -484,95 +490,43 @@ let elim_tac ~term = in let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in let ety = T.type_of_aux' metasenv context eliminator_ref in - let newmeta = new_meta_of_proof ~proof in - let (econclusion,newmetas,arguments,lastmeta) = - new_metasenv_for_apply newmeta proof context ety + let rec find_args_no = + function + C.Prod (_,_,t) -> 1 + find_args_no t + | C.Cast (s,_) -> find_args_no s + | C.LetIn (_,_,t) -> 0 + find_args_no t + | _ -> 0 in - (* Here we assume that we have only one inductive hypothesis to *) - (* eliminate and that it is the last hypothesis of the theorem. *) - (* A better approach would be fingering the hypotheses in some *) - (* way. *) - let meta_of_corpse = - let (_,canonical_context,_) = - CicUtil.lookup_meta (lastmeta - 1) newmetas + let args_no = find_args_no ety in + let term_to_refine = + let rec make_tl base_case = + function + 0 -> [base_case] + | n -> (C.Implicit None)::(make_tl base_case (n - 1)) in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable - canonical_context - in - Cic.Meta (lastmeta - 1, irl) + C.Appl (eliminator_ref :: make_tl term (args_no - 1)) in - let newmetasenv = newmetas @ metasenv in - let subst1,newmetasenv' = - CicUnification.fo_unif newmetasenv context term meta_of_corpse - in - let ueconclusion = CicMetaSubst.apply_subst subst1 econclusion in - (* The conclusion of our elimination principle is *) - (* (?i farg1 ... fargn) *) - (* The conclusion of our goal is ty. So, we can *) - (* eta-expand ty w.r.t. farg1 .... fargn to get *) - (* a new ty equal to (P farg1 ... fargn). Now *) - (* ?i can be instantiated with P and we are ready *) - (* to refine the term. *) - let emeta, fargs = - match ueconclusion with - C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs - | C.Meta (emeta,_) -> emeta,[] - | _ -> raise NotTheRightEliminatorShape + let metasenv', term_to_refine' = + CicMkImplicit.expand_implicits metasenv [] context term_to_refine in + let refined_term,_,metasenv'' = + CicRefine.type_of_aux' metasenv' context term_to_refine' + in + let new_goals = + ProofEngineHelpers.compare_metasenvs + ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in - let ty' = CicMetaSubst.apply_subst subst1 ty in - let eta_expanded_ty = - (*CSC: newmetasenv' era metasenv ??????????? *) - List.fold_left (eta_expand newmetasenv' context) ty' fargs + let proof' = curi,metasenv'',proofbo,proofty in + let proof'', new_goals' = + apply_tactic (apply_tac ~term:refined_term) (proof',goal) in - let subst2,newmetasenv'' = - (*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite - da subst1!!!! Dovrei rimuoverle o sono innocue?*) - CicUnification.fo_unif - newmetasenv' context ueconclusion eta_expanded_ty + (* The apply_tactic can have closed some of the new_goals *) + let patched_new_goals = + let (_,metasenv''',_,_) = proof'' in + List.filter + (function i -> List.exists (function (j,_,_) -> j=i) metasenv''' + ) new_goals @ new_goals' in - let in_subst_domain i = - let eq_to_i = function (j,_) -> i=j in - List.exists eq_to_i subst1 || - List.exists eq_to_i subst2 - in - (* When unwinding the META that corresponds to the elimination *) - (* predicate (which is emeta), we must also perform one-step *) - (* beta-reduction. apply_subst doesn't need the context. Hence *) - (* the underscore. *) - let apply_subst _ t = - let t' = CicMetaSubst.apply_subst subst1 t in - CicMetaSubst.apply_subst_reducing - (Some (emeta,List.length fargs)) subst2 t' - in - let old_uninstantiatedmetas,new_uninstantiatedmetas = - classify_metas newmeta in_subst_domain apply_subst - newmetasenv'' - in - let arguments' = List.map (apply_subst context) arguments in - let bo' = Cic.Appl (eliminator_ref::arguments') in - let newmetasenv''' = - new_uninstantiatedmetas@old_uninstantiatedmetas - in - let (newproof, newmetasenv'''') = - (* When unwinding the META that corresponds to the *) - (* elimination predicate (which is emeta), we must *) - (* also perform one-step beta-reduction. *) - (* The only difference w.r.t. apply_subst is that *) - (* we also substitute metano with bo'. *) - (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *) - (*CSC: no? *) - let apply_subst' t = - let t' = CicMetaSubst.apply_subst subst1 t in - CicMetaSubst.apply_subst_reducing - (Some (emeta,List.length fargs)) - ((metano,bo')::subst2) t' - in - subst_meta_and_metasenv_in_proof - proof metano apply_subst' newmetasenv''' - in - (newproof, - List.map (function (i,_,_) -> i) new_uninstantiatedmetas) + proof'', patched_new_goals in mk_tactic (elim_tac ~term) ;;