From 6ec246c70b05bb310ee5364c3774ea69b0fc9e57 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 7 Apr 2009 21:55:14 +0000
Subject: [PATCH] - more progress towards generalize, but I am stuck now - elim
 completed (up to saturation)

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

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 1d3a4aeff..f967a2ac4 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -20,6 +20,8 @@ open Continuationals.Stack
 open NTacStatus
 module Ast = CicNotationPt
 
+let id_tac status = status;;
+
 let dot_tac status =
   let new_gstatus = 
     match status.gstatus with
@@ -244,7 +246,14 @@ let clear names status goal =
   { status with pstatus = n,h,metasenv,subst,o }
 ;;
 
-let clear_tac names = distribute_tac (clear names);;
+let clear_tac names =
+ if names = [] then id_tac else distribute_tac (clear names)
+;;
+
+let generalize0_tac args =
+ if args = [] then id_tac
+ else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
+;;
 
 let select ~where:(wanted,_,where) status goal = 
  let goalty = get_goalty status goal in
@@ -258,33 +267,33 @@ let select ~where:(wanted,_,where) status goal =
  instantiate status goal instance
 ;;
 
-let select_tac ~where = distribute_tac (select ~where) ;;
+let select0_tac ~where = distribute_tac (select ~where) ;;
 
 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)
+  select0_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);
+     generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
+     select0_tac ~where:(wanted,[],Some path);
      clear_tac (List.map fst hyps) ]
 ;;
 
+(*
+let generalize_tac ~where = 
+ block_tac [ select_tac ~where true ; generalize0_tac ???? ]
+;;
+*)
+
+
 let reopen status =
  let n,h,metasenv,subst,o = status.pstatus in
  let subst, newm = 
@@ -340,16 +349,23 @@ let elim_tac ~what ~where status =
    [ select_tac ~where true;
      distribute_tac (fun status goal ->
        let goalty = get_goalty status goal in
+       let goalsort = typeof status (ctx_of goalty) goalty in
        let _,_,w = what in
        let status, what = 
          disambiguate status what None (ctx_of goalty) in
-       let _ty_what = typeof status (ctx_of what) what in 
-       (* check inductive... find eliminator *)
-       let holes = [ 
-         Ast.Implicit;Ast.Implicit;Ast.Implicit]
-       in
+       let ty_what = typeof status (ctx_of what) what in 
+       let NReference.Ref (uri,_),consno,lefts,rights =
+        analyse_indty status ty_what in
+       let name = NUri.name_of_uri uri ^
+        match term_of_cic_term goalsort (ctx_of goalsort) with
+           NCic.Sort NCic.Prop -> "_ind"
+         | NCic.Sort _ -> "_rect"
+         | _ -> assert false in
+       let leftno = List.length rights in
+       let rightno = List.length rights in
+       let holes=HExtlib.mk_list Ast.Implicit (leftno + 1 + consno + rightno) in
        let eliminator = 
-         Ast.Appl(Ast.Ident("nat_ind",None)::holes @ [ w ])
+         Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
        in
        exec (apply_tac ("",0,eliminator)) status goal) ] 
    status
@@ -360,14 +376,14 @@ let intro_tac name =
   [ exact_tac
     ("",0,(Ast.Binder (`Lambda,
      (Ast.Ident (name,None),None),Ast.Implicit)));
-     if name = "_" then clear_tac [name] else fun x -> x ]
+     if name = "_" then clear_tac [name] else id_tac ]
 ;;
 
 let cases ~what status goal =
  let gty = get_goalty status goal in
  let status, what = disambiguate status what None (ctx_of gty) in
  let ty = typeof status (ctx_of what) what in
- let ref, consno, left, right = analyse_indty status ty in
+ let ref, consno, _, _ = analyse_indty status ty in
  let t =
   NCic.Match (ref,NCic.Implicit `Term, term_of_cic_term what (ctx_of gty),
     HExtlib.mk_list (NCic.Implicit `Term) consno)
@@ -387,5 +403,5 @@ let case1_tac name =
              cases_tac 
               ~where:("",0,(None,[],None)) 
               ~what:("",0,Ast.Ident (name,None));
-              if name = "_clearme" then clear_tac ["_clearme"] else fun x -> x ]
+              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 ;;
-- 
2.39.2