X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FvariousTactics.ml;h=fd383cf99dbe76ee977c3c7fa50a52b7aaf73566;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=bc7b52200fccd8b99961dd3a80f534b1cc849a4e;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/tactics/variousTactics.ml b/helm/software/components/tactics/variousTactics.ml index bc7b52200..fd383cf99 100644 --- a/helm/software/components/tactics/variousTactics.ml +++ b/helm/software/components/tactics/variousTactics.ml @@ -38,23 +38,17 @@ let assumption_tac = let module R = CicReduction in let module S = CicSubstitution in let module PT = PrimitiveTactics in - let _,metasenv,_,_ = proof in + let _,metasenv,_,_,_, _ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let rec find n = function hd::tl -> (match hd with (Some (_, C.Decl t)) when fst (R.are_convertible context (S.lift n t) ty - CicUniv.empty_ugraph) -> n - | (Some (_, C.Def (_,Some ty'))) when + CicUniv.oblivion_ugraph) -> n + | (Some (_, C.Def (_,ty'))) when fst (R.are_convertible context (S.lift n ty') ty - CicUniv.empty_ugraph) -> n - | (Some (_, C.Def (t,None))) -> - let ty_t, u = (* TASSI: FIXME *) - CicTypeChecker.type_of_aux' metasenv context (S.lift n t) - CicUniv.empty_ugraph in - let b,_ = R.are_convertible context ty_t ty u in - if b then n else find (n+1) tl + CicUniv.oblivion_ugraph) -> n | _ -> find (n+1) tl ) | [] -> raise (PET.Fail (lazy "Assumption: No such assumption")) @@ -62,130 +56,3 @@ let assumption_tac = in PET.mk_tactic assumption_tac ;; - -(* ANCORA DA DEBUGGARE *) - -exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;; -exception TheSelectedTermsMustLiveInTheGoalContext -exception AllSelectedTermsMustBeConvertible;; -exception GeneralizationInHypothesesNotImplementedYet;; - -let generalize_tac - ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) - pattern - = - let module PET = ProofEngineTypes in - let generalize_tac mk_fresh_name_callback - ~pattern:(term,hyps_pat,concl_pat) status - = - if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet; - let (proof, goal) = status in - let module C = Cic in - let module P = PrimitiveTactics in - let module T = Tacticals in - let uri,metasenv,pbo,pty = proof in - let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in - let subst,metasenv,u,selected_hyps,terms_with_context = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph - ~conjecture ~pattern in - let context = CicMetaSubst.apply_subst_context subst context in - let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in - let pbo = CicMetaSubst.apply_subst subst pbo in - let pty = CicMetaSubst.apply_subst subst pty in - let term = - match term with - None -> None - | Some term -> - Some (fun context metasenv ugraph -> - let term, metasenv, ugraph = term context metasenv ugraph in - CicMetaSubst.apply_subst subst term, - CicMetaSubst.apply_subst_metasenv subst metasenv, - ugraph) - in - let u,typ,term, metasenv' = - let context_of_t, (t, metasenv, u) = - match terms_with_context, term with - [], None -> - raise - UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly - | [], Some t -> context, t context metasenv u - | (context_of_t, _)::_, Some t -> - context_of_t, t context_of_t metasenv u - | (context_of_t, t)::_, None -> context_of_t, (t, metasenv, u) - in - let t,subst,metasenv' = - try - CicMetaSubst.delift_rels [] metasenv - (List.length context_of_t - List.length context) t - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - raise TheSelectedTermsMustLiveInTheGoalContext - in - (*CSC: I am not sure about the following two assertions; - maybe I need to propagate the new subst and metasenv *) - assert (subst = []); - assert (metasenv' = metasenv); - let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in - u,typ,t,metasenv - in - (* We need to check: - 1. whether they live in the context of the goal; - if they do they are also well-typed since they are closed subterms - of a well-typed term in the well-typed context of the well-typed - term - 2. whether they are convertible - *) - ignore ( - List.fold_left - (fun u (context_of_t,t) -> - (* 1 *) - let t,subst,metasenv'' = - try - CicMetaSubst.delift_rels [] metasenv' - (List.length context_of_t - List.length context) t - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - raise TheSelectedTermsMustLiveInTheGoalContext in - (*CSC: I am not sure about the following two assertions; - maybe I need to propagate the new subst and metasenv *) - assert (subst = []); - assert (metasenv'' = metasenv'); - (* 2 *) - let b,u1 = CicReduction.are_convertible ~subst context term t u in - if not b then - raise AllSelectedTermsMustBeConvertible - else - u1 - ) u terms_with_context) ; - let status = (uri,metasenv',pbo,pty),goal in - let proof,goals = - PET.apply_tactic - (T.thens - ~start: - (P.cut_tac - (C.Prod( - (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ), - typ, - (ProofEngineReduction.replace_lifting_csc 1 - ~equality:(==) - ~what:(List.map snd terms_with_context) - ~with_what:(List.map (function _ -> C.Rel 1) terms_with_context) - ~where:ty) - ))) - ~continuations: - [(P.apply_tac ~term:(C.Appl [C.Rel 1; CicSubstitution.lift 1 term])) ; - T.id_tac]) - status - in - let _,metasenv'',_,_ = proof in - (* CSC: the following is just a bad approximation since a meta - can be closed and then re-opened! *) - (proof, - goals @ - (List.filter - (fun j -> List.exists (fun (i,_,_) -> i = j) metasenv'') - (ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv - ~newmetasenv:metasenv'))) - in - PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern) -;;