1. bug fixed in generalize_pattern: a lazy const_tac should have been

   relocated. The interesting case is

   generalize in match a in \vdash %

   where a occurs in the goal under at least one binder

2. pattern for cases partially implemented. It is now possible to perform
   a case on the hypotheses as long as the conclusion and hypothesis patterns
   are trivial (i.e. %)

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index fc9ea8c5d8964c3ad5b0c647eaf234b59c1b2ecd..2290c4d0ba05cc8483f7cce957e059731cbe990b 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -66,7 +66,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | ApplyS of loc * 'term * 'term auto_params
   | Assumption of loc
   | AutoBatch of loc * 'term auto_params
-  | Cases of loc * 'term * 'ident intros_spec
+  | Cases of loc * 'term * ('term, 'lazy_term, 'ident) pattern *
+             'ident intros_spec
   | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
   | Clear of loc * 'ident list
   | ClearBody of loc * 'ident

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 9fa1d05b62e5fdfaddac84da415b57845e51b310..84facde66203a3e9ac62ba4c1afe4c1b5120f3c0 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -119,7 +119,8 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   | AutoBatch (_,params) -> "autobatch " ^ 
       pp_auto_params ~term_pp params
   | Assumption _ -> "assumption"
-  | Cases (_, term, specs) -> Printf.sprintf "cases " ^ term_pp term ^
+  | Cases (_, term, pattern, specs) -> Printf.sprintf "cases " ^ term_pp term ^
+      pp_tactic_pattern pattern ^
       pp_intros_specs "names " specs 
   | Change (_, where, with_what) ->
       Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 3746403d951ea382e8360c2fcd2f933dc0f1cc07..8813e498bed94ae6425757af2e4d88ed1c025794 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -89,9 +89,9 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.AutoBatch (_,params) ->
       Tactics.auto ~params ~dbd:(LibraryDb.instance ()) 
        ~universe:status.GrafiteTypes.universe
-  | GrafiteAst.Cases (_, what, (howmany, names)) ->
+  | GrafiteAst.Cases (_, what, pattern, (howmany, names)) ->
       Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
-        what
+        ~pattern what
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 73e71c815f764e2f9a3f79933d4300c9c13da102..71460415a293dcad0ef759aadc0d6a304668c507 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -216,9 +216,10 @@ let rec disambiguate_tactic
     | GrafiteAst.AutoBatch (loc,params) ->
         let metasenv, params = disambiguate_auto_params metasenv params in
         metasenv,GrafiteAst.AutoBatch (loc,params)
-    | GrafiteAst.Cases (loc, what, idents) ->
+    | GrafiteAst.Cases (loc, what, pattern, idents) ->
         let metasenv,what = disambiguate_term context metasenv what in
-        metasenv,GrafiteAst.Cases (loc, what, idents)
+       let pattern = disambiguate_pattern pattern in
+        metasenv,GrafiteAst.Cases (loc, what, pattern, idents)
     | GrafiteAst.Change (loc, pattern, with_what) -> 
         let with_what = disambiguate_lazy_term with_what in
         let pattern = disambiguate_pattern pattern in

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 6fcb9dba4f0a8e83620b84534f68523ef2d1cd07..6ce615091a5203602f6195221d48e2b0b62f4911 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -177,8 +177,13 @@ EXTEND
     | IDENT "autobatch";  params = auto_params ->
         GrafiteAst.AutoBatch (loc,params)
     | IDENT "cases"; what = tactic_term;
+      pattern = OPT pattern_spec;
       specs = intros_spec ->
-        GrafiteAst.Cases (loc, what, specs)
+        let pattern = match pattern with
+           | None         -> None, [], Some Ast.UserInput
+           | Some pattern -> pattern   
+        in
+        GrafiteAst.Cases (loc, what, pattern, specs)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
     | IDENT "clearbody"; id = IDENT ->

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 7b58517f6883af1927618721852bbd387a0ef75b..db8fe4376686468c076b1ab41995a9c0e5ff5af2 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -743,7 +743,7 @@ let generalize_pattern_tac pattern =
     List.map
      (fun id ->
        let rel,_ = ProofEngineHelpers.find_hyp id context in
-        id,(Some (PET.const_lazy_term rel), [], Some (ProofEngineTypes.hole))
+        id,(Some (fun ctx m u -> CicSubstitution.lift (List.length ctx - List.length context) rel,m,u), [], Some (ProofEngineTypes.hole))
      ) generalize_hyps in
    let tactics =
     List.map
@@ -886,14 +886,27 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
     PET.mk_tactic reorder_pattern
 ;;
 
-let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
- let cases_tac ~term (proof, goal) =
+let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ?(pattern = PET.conclusion_pattern None) term =
+ let cases_tac pattern (proof, goal) =
   let module TC = CicTypeChecker in
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
   let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  let pattern = pattern_after_generalize_pattern_tac pattern in
+  let _cpattern =
+   match pattern with 
+     | None, [], Some cpattern ->
+        let rec is_hole =
+         function
+            Cic.Implicit (Some `Hole) -> true
+          | Cic.Prod (Cic.Anonymous,so,tgt) -> is_hole so && is_hole tgt
+          | _ -> false
+        in
+         if not (is_hole cpattern) then
+          raise (PET.Fail (lazy "not implemented"))
+     | _ -> raise (PET.Fail (lazy "not implemented")) in    
   let termty,_ = TC.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
   let termty = CicReduction.whd context termty in
   let (termty,metasenv',arguments,fresh_meta) =
@@ -1016,7 +1029,16 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
     in
     proof'', patched_new_goals
   in
-  PET.mk_tactic (cases_tac ~term)
+   let reorder_pattern ((proof, goal) as status) =
+     let _,metasenv,_,_,_,_ = proof in
+     let conjecture = CicUtil.lookup_meta goal metasenv in
+     let _,context,_ = conjecture in
+     let pattern = ProofEngineHelpers.sort_pattern_hyps context pattern in
+      PET.apply_tactic
+       (Tacticals.then_ ~start:(generalize_pattern_tac pattern)
+         ~continuation:(PET.mk_tactic (cases_tac pattern))) status
+   in
+    PET.mk_tactic reorder_pattern
 ;;
 
 

diff --git a/helm/software/components/tactics/primitiveTactics.mli b/helm/software/components/tactics/primitiveTactics.mli
index 95ba654f50815965c1925d7a5dce63a05c043861..0ca91fe2c56128549f9789f46aeed4344f72a269 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.mli
+++ b/helm/software/components/tactics/primitiveTactics.mli
@@ -93,7 +93,8 @@ val elim_intros_tac:
 val cases_intros_tac:
   ?howmany:int ->
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  Cic.term -> ProofEngineTypes.tactic 
+  ?pattern:ProofEngineTypes.lazy_pattern -> Cic.term ->
+  ProofEngineTypes.tactic 
 
 (* FG *)
 

diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index 08b32e5714ccb2e4e49a09c13d02cb7e6beaed11..a0aa32b3c268a51dc3b8ec505ff14db730faff63 100644 (file)
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -14,6 +14,7 @@ val auto :
 val cases_intros :
   ?howmany:int ->
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  ?pattern:ProofEngineTypes.lazy_pattern ->
   Cic.term -> ProofEngineTypes.tactic
 val change :
   ?with_cast:bool ->