X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=dbc134319424b94f1397903077ebc1e38e68772c;hb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;hp=15e77f0940417eb6c5368e99798434706c12ea15;hpb=f5c28fbe41e4754af1c161e7b4176ae053199cc7;p=helm.git

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index 15e77f094..dbc134319 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) ]
 ;;
 
@@ -442,8 +461,7 @@ 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 =
@@ -452,8 +470,7 @@ let change_tac ~where ~with_what =
     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,29 +490,24 @@ type indtyinfo = {
         rightno: int;
         leftno: int;
         consno: int;
-        lefts: NCic.term list;
-        rights: NCic.term list;
         reference: NReference.reference;
-        term: NCic.term
  }
 ;;
 
 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, 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
-  let status,what = term_of_cic_term status what (ctx_of goalty) in
   indtyref := Some { 
-    rightno = rightno; leftno = leftno; consno = consno;
-    lefts = lefts; rights = rights; reference = r; term = what
+    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 ->
@@ -525,8 +537,8 @@ let elim_tac ~what:(txt,len,what) ~where =
           (match !sort with NCic.Sort x -> x | _ -> assert false))
      in
      let eliminator = 
-       let what = (HExtlib.unopt !indtyinfo).term in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ]
+       let _,_,w = what in
+       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;
@@ -542,6 +554,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
@@ -596,13 +609,9 @@ let cases_tac ~what:(txt,len,what) ~where =
   atomic_tac 
    (block_tac [
       analyze_indty_tac ~what indtyinfo;
-      (fun s ->
-        select_tac 
-         ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true
-         s);
-      (fun s ->
-        distribute_tac
-         (cases ~what:("",0,Ast.NCic (HExtlib.unopt !indtyinfo).term)) s); ])
+      (fun s -> select_tac 
+       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s);
+      distribute_tac (cases ~what) ])
 ;;
 
 let case1_tac name =
@@ -636,7 +645,7 @@ let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
   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
@@ -695,8 +704,8 @@ let inversion_tac ~what:(txt,len,what) ~where =
           (match !sort with NCic.Sort x -> x | _ -> assert false))
      in
      let eliminator = 
-       let what = (HExtlib.unopt !indtyinfo).term in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ]
+       let _,_,w = what in
+       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;