X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=6241a3ea6baa7f13b25a9f2105b443e0ea018624;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=331945819395f95db65665d46236b6b1629abb0f;hpb=53a5acbe28212706be9c684d612aee1ccb165587;p=helm.git

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index 331945819..6241a3ea6 100644
--- a/matita/components/ng_tactics/nTactics.ml
+++ b/matita/components/ng_tactics/nTactics.ml
@@ -202,11 +202,25 @@ let compare_statuses ~past ~present =
    (e.g. the tactic could perform a global analysis of the set of goals)
 *)
 
+(* CSC: potential bug here: the new methods still use the instance variables
+   of the old status and not the instance variables of the new one *)
+let change_stack_type (status : 'a #NTacStatus.status) (stack: 'b) : 'b NTacStatus.status =
+ let o =
+  object
+   inherit ['b] NTacStatus.status status#obj stack
+   method ppterm = status#ppterm
+   method ppcontext = status#ppcontext
+   method ppsubst = status#ppsubst
+   method ppobj = status#ppobj
+   method ppmetasenv = status#ppmetasenv
+  end
+ in
+  o#set_pstatus status
+;;
+
 let exec tac (low_status : #lowtac_status) g =
   let stack = [ [0,Open g], [], [], `NoTag ] in
-  let status =
-   (new NTacStatus.status low_status#obj stack)#set_pstatus low_status
-  in
+  let status = change_stack_type low_status stack in
   let status = tac status in
    (low_status#set_pstatus status)#set_obj status#obj
 ;;
@@ -236,7 +250,7 @@ let distribute_tac tac (status : #tac_status) =
             in
             aux s go gc loc_tl
       in
-      let s0 = (new NTacStatus.status status#obj ())#set_pstatus status in
+      let s0 = change_stack_type status () in
       let s0, go0, gc0 = s0, [], [] in
       let sn, gon, gcn = aux s0 go0 gc0 g in
       debug_print (lazy ("opened: "
@@ -261,10 +275,13 @@ let repeat_tac t s =
 
 
 let try_tac tac status =
+ let try_tac status =
   try
     tac status
   with NTacStatus.Error _ ->
     status
+ in
+  atomic_tac try_tac status
 ;;
 
 let first_tac tacl status =
@@ -315,7 +332,7 @@ let clear_tac names =
      names
    in
    let n,h,metasenv,subst,o = status#obj in
-   let metasenv,subst,_,_ = NCicMetaSubst.restrict metasenv subst goal js in
+   let metasenv,subst,_,_ = NCicMetaSubst.restrict status metasenv subst goal js in
     status#set_obj (n,h,metasenv,subst,o))
 ;;
 
@@ -324,7 +341,7 @@ let generalize0_tac args =
  else exact_tac ("",0,Ast.Appl (Ast.Implicit `JustOne :: args))
 ;;
 
-let select0_tac ~where:(wanted,hyps,where) ~job  =
+let select0_tac ~where ~job  =
  let found, postprocess = 
    match job with
    | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno
@@ -332,6 +349,8 @@ let select0_tac ~where:(wanted,hyps,where) ~job  =
    | `ChangeWith f -> f,(fun s t -> s, t)
  in
  distribute_tac (fun status goal ->
+   let wanted,hyps,where =
+    GrafiteDisambiguate.disambiguate_npattern status where in
    let goalty = get_goalty status goal in
    let path = 
      match where with None -> NCic.Implicit `Term | Some where -> where 
@@ -371,24 +390,24 @@ let select0_tac ~where:(wanted,hyps,where) ~job  =
    let status, instance = 
      mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
    in
-   instantiate status goal instance)
+   instantiate ~refine:false status goal instance) 
 ;;
 
-let select_tac ~where ~job 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
+let select_tac ~where:((txt,txtlen,(wanted,hyps,path)) as where) ~job
+ move_down_hyps
+=
  if not move_down_hyps then
-  select0_tac ~where:(wanted,hyps,Some path) ~job
+  select0_tac ~where ~job
  else
   let path = 
    List.fold_left
-     (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
-     path (List.rev hyps)
+    (fun path (name,ty) ->
+      NotationPt.Binder (`Forall, (NotationPt.Ident (name,None),Some ty),path))
+    (match path with Some x -> x | None -> NotationPt.UserInput) (List.rev hyps)
   in
    block_tac [ 
      generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
-     select0_tac ~where:(wanted,[],Some path) ~job;
+     select0_tac ~where:(txt,txtlen,(wanted,[],Some path)) ~job;
      clear_tac (List.map fst hyps) ]
 ;;
 
@@ -405,7 +424,7 @@ let generalize_tac ~where =
                _,_,(None,_,_)  -> fail (lazy "No term to generalize")
              | txt,txtlen,(Some what,_,_) ->
                 let status, what =
-                 disambiguate status (ctx_of goalty) (txt,txtlen,what) None
+                 disambiguate status (ctx_of goalty) (txt,txtlen,what) `XTNone
                 in
                  status,what,[]
            )
@@ -442,18 +461,17 @@ let reduce_tac ~reduction ~where =
         whd status
          ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
   in
-  let where = GrafiteDisambiguate.disambiguate_npattern where in
-  select0_tac ~where ~job:(`ChangeWith change)
+  select_tac ~where ~job:(`ChangeWith change) false
 ;;
 
 let change_tac ~where ~with_what =
   let change status t = 
-    let status, ww = disambiguate status (ctx_of t) with_what  None in
+(* FG: `XTSort could be used when we change the whole goal *)    
+    let status, ww = disambiguate status (ctx_of t) with_what `XTNone in
     let status = unify status (ctx_of t) t ww in
     status, ww
   in
-  let where = GrafiteDisambiguate.disambiguate_npattern where in
-  select0_tac ~where ~job:(`ChangeWith change)
+  select_tac ~where ~job:(`ChangeWith change) false
 ;;
 
 let letin_tac ~where ~what:(_,_,w) name =
@@ -473,8 +491,6 @@ type indtyinfo = {
         rightno: int;
         leftno: int;
         consno: int;
-        lefts: NCic.term list;
-        rights: NCic.term list;
         reference: NReference.reference;
  }
 ;;
@@ -482,18 +498,17 @@ type indtyinfo = {
 let ref_of_indtyinfo iti = iti.reference;;
 
 let analyze_indty_tac ~what indtyref =
- distribute_tac (fun status goal ->
+ distribute_tac (fun (status as orig_status) goal ->
   let goalty = get_goalty status goal in
-  let status, what = disambiguate status (ctx_of goalty) what None in
+  let status, what = disambiguate status (ctx_of goalty) what `XTInd in
   let status, ty_what = typeof status (ctx_of what) what in 
   let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
   let leftno = List.length lefts in
   let rightno = List.length rights in
   indtyref := Some { 
-    rightno = rightno; leftno = leftno; consno = consno;
-    lefts = lefts; rights = rights; reference = r;
+    rightno = rightno; leftno = leftno; consno = consno; reference = r;
   };
-  exec id_tac status goal)
+  exec id_tac orig_status goal)
 ;;
 
 let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
@@ -540,6 +555,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
      `LeftToRight -> "eq" ^ suffix ^ "_r"
    | `RightToLeft -> "eq" ^ suffix
  in
+ let what = Ast.Appl [what; Ast.Implicit `Vector] in
   block_tac
    [ select_tac ~where ~job:(`Substexpand 2) true;
      exact_tac
@@ -577,14 +593,14 @@ let intros_tac ?names_ref names s =
 
 let cases ~what status goal =
  let gty = get_goalty status goal in
- let status, what = disambiguate status (ctx_of gty) what None in
+ let status, what = disambiguate status (ctx_of gty) what `XTInd in
  let status, ty = typeof status (ctx_of what) what in
  let status, (ref, consno, _, _) = analyse_indty status ty in
  let status, what = term_of_cic_term status what (ctx_of gty) in
  let t =
   NCic.Match (ref,NCic.Implicit `Term, what,
     HExtlib.mk_list (NCic.Implicit `Term) consno)
- in
+ in 
  instantiate status goal (mk_cic_term (ctx_of gty) t)
 ;;
 
@@ -609,9 +625,9 @@ let case1_tac name =
 ;;
 
 let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal ->
-  if num < 1 then fail (lazy "constructor numbers begin with 1");
   let gty = get_goalty status goal in
-  let status, (r,_,_,_) = analyse_indty status gty in
+  let status, (r,consno,_,_) = analyse_indty status gty in
+  if num < 1 || num > consno then fail (lazy "Non existant constructor");
   let ref = NReference.mk_constructor num r in
   let t = 
     if args = [] then Ast.NRef ref else
@@ -624,13 +640,13 @@ let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal ->
 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
  let gty = get_goalty status goal in
  let eq status ctx t1 t2 =
-  let status,t1 = disambiguate status ctx t1 None in
+  let status,t1 = disambiguate status ctx t1 `XTSort in
   let status,t1 = apply_subst status ctx t1 in
   let status,t1 = term_of_cic_term status t1 ctx in
   let t2 = mk_cic_term ctx t2 in
   let status,t2 = apply_subst status ctx t2 in
   let status,t2 = term_of_cic_term status t2 ctx in
-  prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
+  prerr_endline ("COMPARING: " ^ status#ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ status#ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
   assert (t1=t2);
   status
  in
@@ -690,7 +706,7 @@ let inversion_tac ~what:(txt,len,what) ~where =
      in
      let eliminator = 
        let _,_,w = what in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ; Ast.Implicit `Vector]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;