From dc26b607f828fdf4d1dffbb007e213263ffbef97 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 7 Apr 2009 17:23:10 +0000
Subject: [PATCH] - select_tac honors the hypotheses pattern when required to
 generalize them - clear [names] - initial generalize tac implementation

---
 .../components/ng_tactics/nTactics.ml         | 105 ++++++++++++------
 1 file changed, 68 insertions(+), 37 deletions(-)

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 250d50ce3..1d3a4aeff 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -18,6 +18,7 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 open Continuationals.Stack
 open NTacStatus
+module Ast = CicNotationPt
 
 let dot_tac status =
   let new_gstatus = 
@@ -211,10 +212,42 @@ let distribute_tac tac status =
        { gstatus = stack; istatus = sn }
 ;;
 
+let exact t status goal =
+ let goalty = get_goalty status goal in
+ let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
+ instantiate status goal t
+;;
+
+let exact_tac t = distribute_tac (exact t) ;;
+
+let find_in_context name context =
+  let rec aux acc = function
+    | [] -> raise Not_found
+    | (hd,_) :: tl when hd = name -> acc
+    | _ :: tl ->  aux (acc + 1) tl
+  in
+  aux 1 context
+;;
 
-let select ~where status goal = 
+let clear names status goal =
+ let goalty = get_goalty status goal in
+ let js =
+   List.map 
+     (fun name -> 
+        try find_in_context name (ctx_of goalty)
+        with Not_found -> 
+          fail (lazy ("hypothesis '" ^ name ^ "' not found"))) 
+     names
+ in
+ let n,h,metasenv,subst,o = status.pstatus in
+ let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
+  { status with pstatus = n,h,metasenv,subst,o }
+;;
+
+let clear_tac names = distribute_tac (clear names);;
+
+let select ~where:(wanted,_,where) status goal = 
  let goalty = get_goalty status goal in
- let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in
  let path = 
    match where with None -> NCic.Implicit `Term | Some where -> where 
  in
@@ -227,14 +260,31 @@ let select ~where status goal =
 
 let select_tac ~where = distribute_tac (select ~where) ;;
 
-let exact t status goal =
- let goalty = get_goalty status goal in
- let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
- instantiate status goal t
+let select_tac ~where move_down_hyps = 
+ let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
+ let path = 
+  match where with None -> NCic.Implicit `Term | Some where -> where in
+ if not move_down_hyps then
+  select_tac ~where:(wanted,hyps,Some path)
+ else
+  let path = 
+   List.fold_left
+     (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
+     path (List.rev hyps)
+  in
+   let generalize_tac =
+    distribute_tac
+     (exec (exact_tac 
+         ("",0,Ast.Appl 
+           (Ast.Implicit :: List.map (fun (name,_) -> Ast.Ident (name,None)) 
+             hyps))))
+   in
+   block_tac [ 
+     generalize_tac; 
+     select_tac ~where:(wanted,[],Some path);
+     clear_tac (List.map fst hyps) ]
 ;;
 
-let exact_tac t = distribute_tac (exact t) ;;
-
 let reopen status =
  let n,h,metasenv,subst,o = status.pstatus in
  let subst, newm = 
@@ -287,7 +337,7 @@ let change_tac ~where ~with_what = distribute_tac (change ~where ~with_what) ;;
 
 let elim_tac ~what ~where status =
  block_tac
-   [ select_tac ~where;
+   [ select_tac ~where true;
      distribute_tac (fun status goal ->
        let goalty = get_goalty status goal in
        let _,_,w = what in
@@ -296,42 +346,21 @@ let elim_tac ~what ~where status =
        let _ty_what = typeof status (ctx_of what) what in 
        (* check inductive... find eliminator *)
        let holes = [ 
-         CicNotationPt.Implicit;CicNotationPt.Implicit;CicNotationPt.Implicit]
+         Ast.Implicit;Ast.Implicit;Ast.Implicit]
        in
        let eliminator = 
-         CicNotationPt.Appl(CicNotationPt.Ident("nat_ind",None)::holes @ [ w ])
+         Ast.Appl(Ast.Ident("nat_ind",None)::holes @ [ w ])
        in
        exec (apply_tac ("",0,eliminator)) status goal) ] 
    status
 ;;
 
-let find_in_context name context =
-  let rec aux acc = function
-    | [] -> raise Not_found
-    | (hd,_) :: tl when hd = name -> acc
-    | _ :: tl ->  aux (acc + 1) tl
-  in
-  aux 1 context
-;;
-
-let clear name status goal =
- let goalty = get_goalty status goal in
- let j =
-  try find_in_context name (ctx_of goalty)
-  with Not_found -> fail (lazy ("hypothesis '" ^ name ^ "' not found")) in
- let n,h,metasenv,subst,o = status.pstatus in
- let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal [j] in
-  { status with pstatus = n,h,metasenv,subst,o }
-;;
-
-let clear_tac name = distribute_tac (clear name);;
-
 let intro_tac name =
  block_tac
   [ exact_tac
-    ("",0,(CicNotationPt.Binder (`Lambda,
-     (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)));
-    if name = "_" then clear_tac name else fun x -> x ]
+    ("",0,(Ast.Binder (`Lambda,
+     (Ast.Ident (name,None),None),Ast.Implicit)));
+     if name = "_" then clear_tac [name] else fun x -> x ]
 ;;
 
 let cases ~what status goal =
@@ -349,12 +378,14 @@ let cases ~what status goal =
 ;;
 
 let cases_tac ~what ~where = 
-  block_tac [ select_tac ~where ; distribute_tac (cases ~what) ]
+        block_tac [ select_tac ~where true ; distribute_tac (cases ~what) ]
 ;;
 
 let case1_tac name =
+ let name = if name = "_" then "_clearme" else name in
  block_tac [ intro_tac name; 
              cases_tac 
               ~where:("",0,(None,[],None)) 
-              ~what:("",0,CicNotationPt.Ident (name,None)) ]
+              ~what:("",0,Ast.Ident (name,None));
+              if name = "_clearme" then clear_tac ["_clearme"] else fun x -> x ]
 ;;
-- 
2.39.2