-(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
-e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
-contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
-
-let generalize_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
- terms ~status:((proof,goal) as status)
-=
- let module C = Cic in
- let module P = PrimitiveTactics in
- let module T = Tacticals in
- let _,metasenv,_,_ = proof in
- let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- let typ =
- match terms with
- [] -> assert false
- | he::tl ->
- (* We need to check that all the convertibility of all the terms *)
- List.iter
- (function t ->
- if not (CicReduction.are_convertible context he t) then
- raise AllSelectedTermsMustBeConvertible
- ) tl ;
- (CicTypeChecker.type_of_aux' metasenv context he)
+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 status = (uri,metasenv,pbo,pty),goal in
+ let term =
+ match term with
+ None -> None
+ | Some term -> Some (CicMetaSubst.apply_subst subst term) in
+ let u,typ,term =
+ let context_of_t,t =
+ match terms_with_context, term with
+ [], None ->
+ raise
+ UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
+ | _, Some t -> context,t
+ | (context_of_t,t)::_, None -> context_of_t,t
+ 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