From: Claudio Sacerdoti Coen Date: Thu, 23 Jun 2005 12:17:55 +0000 (+0000) Subject: Tactic generalize ported to patterns and activated in matita. X-Git-Tag: INDEXING_NO_PROOFS~96 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1416af941615fa434b71c0adda461d5bcac65f89;p=helm.git Tactic generalize ported to patterns and activated in matita. --- diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 6ad30c794..c130cc933 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -47,6 +47,7 @@ type ('term, 'ident) tactic = | Exists of loc | Fold of loc * reduction_kind * 'term | Fourier of loc + | Generalize of loc * 'term * ('term, 'ident) pattern | Goal of loc * int (* change current goal, argument is goal number 1-based *) | Injection of loc * 'ident | Intros of loc * int option * 'ident list diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 902a1d661..35a27ff24 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -68,6 +68,7 @@ let rec count_tactic current_size tac = | Fold (_, kind, term) -> countterm (current_size + 5) term | Fourier _ -> current_size + 7 + | Generalize (_,term,pattern) -> assert false (* TODO *) | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n))) | Injection (_, ident) -> current_size + 10 + (String.length ident) | Intros (_, num, idents) -> @@ -191,6 +192,7 @@ and big_tactic2box = function Box.Text([],string_of_kind kind)]); Box.indent(ast2astBox term)]) | Fourier _ -> Box.Text([],"fourier") + | Generalize _ -> assert false (* TODO *) | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n) | Injection (_, ident) -> Box.V([],[Box.Text([],"transitivity"); diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 2cc4d0c65..86d10c877 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -80,6 +80,8 @@ let rec pp_tactic = function | Exists _ -> "exists" | Fold (_, kind, term) -> sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term_ast term) + | Generalize (_, term, pattern) -> + sprintf "generalize %s %s" (pp_term_ast term) (pp_pattern pattern) | Goal (_, n) -> "goal " ^ string_of_int n | Fourier _ -> "fourier" | Injection (_, ident) -> "injection " ^ ident diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 5eb66704f..b656fe58c 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -34,7 +34,7 @@ val fold : val fourier : ProofEngineTypes.tactic val generalize : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - Cic.term list -> ProofEngineTypes.tactic + term:Cic.term -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic val set_goal : int -> ProofEngineTypes.tactic val injection : term:Cic.term -> ProofEngineTypes.tactic val intros : diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index c10060324..233cc321f 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -64,35 +64,52 @@ let assumption_tac = (* ANCORA DA DEBUGGARE *) exception AllSelectedTermsMustBeConvertible;; +exception CannotGeneralizeInHypotheses;; (* 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 = FreshNamesGenerator.mk_fresh_name ~subst:[]) terms + ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + ~term pattern = let module PET = ProofEngineTypes in - let generalize_tac mk_fresh_name_callback terms status = + let generalize_tac mk_fresh_name_callback ~term (hyps_pat,concl_pat) status = + if hyps_pat <> [] then raise CannotGeneralizeInHypotheses ; let (proof, goal) = status in let module C = Cic in let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in - let typ,_ = - match terms with - [] -> assert false - | he::tl -> - (* We need to check that all the convertibility of all the terms *) - let u = List.fold_left ( (* TASSI: FIXME *) - fun u t -> - let b,u1 = CicReduction.are_convertible context he t u in - if not b then - raise AllSelectedTermsMustBeConvertible - else - u1) CicUniv.empty_ugraph tl in - (CicTypeChecker.type_of_aux' metasenv context he u) + let terms = + let path = + match concl_pat with + None -> Cic.Implicit (Some `Hole) + | Some path -> path in + let roots = CicUtil.select ~term:ty ~context:path in + List.fold_left + (fun acc (i, r) -> + ProofEngineHelpers.find_subterms + ~eq:ProofEngineReduction.alpha_equivalence ~wanted:term r @ acc + ) [] roots + in + let typ = + let typ,u = + CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in + (* We need to check that all the convertibility of all the terms *) + ignore ( + (* TASSI: FIXME *) + List.fold_left + (fun u t -> + let b,u1 = CicReduction.are_convertible context term t u in + if not b then + raise AllSelectedTermsMustBeConvertible + else + u1 + ) u terms) ; + typ in PET.apply_tactic (T.thens @@ -107,10 +124,12 @@ let generalize_tac ~with_what:(List.map (function _ -> C.Rel 1) terms) ~where:ty) ))) - ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]) + ~continuations: + [(P.apply_tac ~term:(C.Appl [C.Rel 1; CicSubstitution.lift 1 term])) ; + T.id_tac]) status in - PET.mk_tactic (generalize_tac mk_fresh_name_callback terms) + PET.mk_tactic (generalize_tac mk_fresh_name_callback ~term pattern) ;; let set_goal n = diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index eefdd9846..2c891b036 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -29,9 +29,9 @@ exception AllSelectedTermsMustBeConvertible;; val assumption_tac: ProofEngineTypes.tactic val generalize_tac: - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list -> + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + term:Cic.term -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic (* change the current goal to those referred by the given meta number *) val set_goal: int -> ProofEngineTypes.tactic -