X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=7937e8b4b4ddbb739ed6fb27bafa82a0b3f7f7ea;hb=916c558005ed665c62699a7a4c5347870c8a3efb;hp=3be17c5e7eca608993a2304e663b9670643f9ec6;hpb=8d7287519cc51145fcac0ee603ba136dc749857d;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 3be17c5e7..7937e8b4b 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -274,9 +274,6 @@ let select0_tac ~where:(wanted,hyps,where) ~job  =
    let path = 
      match where with None -> NCic.Implicit `Term | Some where -> where 
    in
-   let status, newgoalty = 
-     select_term status ~found ~postprocess goalty (wanted,path) 
-   in
    let status, newgoalctx =
       List.fold_right
        (fun (name,d as entry) (status,ctx) ->
@@ -299,6 +296,16 @@ let select0_tac ~where:(wanted,hyps,where) ~job  =
           Not_found -> status, entry::ctx
        ) (ctx_of goalty) (status,[])
    in
+   let status, newgoalty = 
+     select_term status ~found ~postprocess goalty (wanted,path) in
+   (* WARNING: the next two lines simply change the context of newgoalty
+      from the old to the new one. Otherwise mk_meta will do that herself,
+      calling relocate that calls delift. However, newgoalty is now
+      ?[out_scope] and thus the delift would trigger the special unification
+      case, which is wrong now :-( *)
+   let status,newgoalty = term_of_cic_term status newgoalty (ctx_of goalty) in
+   let newgoalty = mk_cic_term newgoalctx newgoalty in
+
    let status, instance = 
      mk_meta status newgoalctx (`Decl newgoalty) 
    in
@@ -363,23 +370,11 @@ let change_tac ~where ~with_what =
   select0_tac ~where ~job:(`ChangeWith change)
 ;;
 
-let letin_tac ~where:(_,_,(m,hyp,gp)) ~what:(_,_,w) name =
-  assert(m = None);
-  let where = Some w, [], 
-     match gp with 
-     | None -> Some Ast.Implicit
-     | Some where -> 
-         Some 
-          (List.fold_left 
-           (fun t _ -> 
-              Ast.Binder(`Pi,(Ast.Ident("_",None),Some Ast.UserInput),t)) 
-           where hyp)
-  in
-  block_tac [
-   generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyp);
-   exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
-   change_tac ~where:("",0,where) ~with_what:("",0,Ast.Ident (name,None))
-  ]
+let letin_tac ~where ~what:(_,_,w) name =
+ block_tac [
+  select_tac ~where ~job:(`Substexpand 1) true;
+  exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
+ ]
 ;;
 
 let apply_tac = exact_tac;;
@@ -494,46 +489,55 @@ let case1_tac name =
              cases_tac 
               ~where:("",0,(None,[],None)) 
               ~what:("",0,Ast.Ident (name,None));
-              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
+             if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 ;;
 
-let assert_tac (hyps,concl) = distribute_tac (fun status goal ->
+let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
  let gty = get_goalty status goal in
- let status,concl = disambiguate status concl None (ctx_of gty) in
- let status,concl = term_of_cic_term status concl (ctx_of gty) in
+ let eq status ctx t1 t2 =
+  let status,t1 = disambiguate status t1 None ctx 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);
+  assert (t1=t2);
+  status
+ in
  let status,gty' = term_of_cic_term status gty (ctx_of gty) in
- assert (concl=gty');
+ let status = eq status (ctx_of gty) concl gty' in
  let status,_ =
   List.fold_right2
    (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
-     assert (id1=id2);
+     assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false));
      match e1,e2 with
         `Decl t1, NCic.Decl t2 ->
-          let status,t1 = disambiguate status t1 None ctx 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
-          assert (t1=t2);
+          let status = eq status ctx t1 t2 in
           status,item::ctx
       | `Def (b1,t1), NCic.Def (b2,t2) ->
-          let status,t1 = disambiguate status t1 None ctx in
-          let status,t1 = apply_subst status ctx t1 in
-          let status,t1 = term_of_cic_term status t1 ctx in
-          let status,b1 = disambiguate status b1 None ctx in
-          let status,b1 = apply_subst status ctx b1 in
-          let status,b1 = term_of_cic_term status b1 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
-          let b2 = mk_cic_term ctx b2 in
-          let status,b2 = apply_subst status ctx b2 in
-          let status,b2 = term_of_cic_term status b2 ctx in
-          assert (t1=t2 && b1=b2);
+          let status = eq status ctx t1 t2 in
+          let status = eq status ctx b1 b2 in
           status,item::ctx
       | _ -> assert false
    ) hyps (ctx_of gty) (status,[])
  in
   exec id_tac status goal)
 ;;
+
+let assert_tac seqs status =
+ match status.gstatus with
+  | [] -> assert false
+  | (g,_,_,_) :: s ->
+     assert (List.length g = List.length seqs);
+     (match seqs with
+         [] -> id_tac
+       | [seq] -> assert0_tac seq
+       | _ ->
+         block_tac
+          (branch_tac::
+          HExtlib.list_concat ~sep:[shift_tac]
+            (List.map (fun seq -> [assert0_tac seq]) seqs)@
+          [merge_tac])
+     ) status
+;;