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 6ad30c7943e4f7d6ab0c4ba03920880035c624a0..c130cc933081bdbf03f766a73feabe7fb2d42e42 100644 (file)
--- 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 902a1d661eeabda075b9e8c1cc760b97610625f0..35a27ff24785fa17640b023ebc5d374efd95a076 100644 (file)
--- 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 2cc4d0c658fc735306b45b6ebbed2a86c210f18c..86d10c87730294bf0db4e097c4ec442dec47f3e4 100644 (file)
--- 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 5eb66704f7fe61f2d76cc379709ef49c7e1ecc19..b656fe58cc6af392219b12843d3f42c4cd6d6670 100644 (file)
--- 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 c1006032471a7d6fffc86959dcedca987c4a05bf..233cc321f4b5112006201d1609d294d59588274d 100644 (file)
--- 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 eefdd9846aad150c578a8ea34ad83087000b6d85..2c891b036b75e635a38242383c61e8530f62c162 100644 (file)
--- 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
-