auto destructs while introducing in the context

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 323777d18846e895eabfcaaeff3ae7e3e6c2ecfa..93078df257ab9aadfc781cbdd8e07d06f1decec1 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -166,7 +166,7 @@ let fast_height_of_term t =
    | NCic.Rel _
    | NCic.Sort _ -> ()
    | NCic.Implicit _ -> assert false
-   | NCic.Const nref as t -> 
+   | NCic.Const nref -> 
 (*
                    prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[]
                    ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref));            
@@ -284,6 +284,7 @@ let index_local_equations eq_cache status =
   let open_goal = List.hd open_goals in
   let ngty = get_goalty status open_goal in
   let ctx = ctx_of ngty in
+  let ctx = apply_subst_context ~fix_projections:true status ctx in
   let c = ref 0 in
   List.fold_left 
     (fun eq_cache _ ->
@@ -293,6 +294,7 @@ let index_local_equations eq_cache status =
            let ty = NCicTypeChecker.typeof [] [] ctx t in
            if is_a_fact status (mk_cic_term ctx ty) then
              (debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
+              debug_print(lazy("riprovo " ^ (ppterm status (mk_cic_term ctx ty))));
               NCicParamod.forward_infer_step eq_cache t ty)
            else 
              (debug_print (lazy ("not a fact: " ^ (NCicPp.ppterm ctx [] [] ty)));
@@ -519,7 +521,7 @@ let saturate_to_ref metasenv subst ctx nref ty =
       | NCic.Const(NReference.Ref (_,NReference.Def _) as nre) 
          when nre<>nref ->
          let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in 
-           aux metasenv ty (args@moreargs)
+           aux metasenv bo (args@moreargs)
       | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl) 
          when nre<>nref ->
          let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in
@@ -641,6 +643,7 @@ let all_keys_of_cic_type metasenv subst context ty =
 let all_keys_of_type status t =
  let _,_,metasenv,subst,_ = status#obj in
  let context = ctx_of t in
+ let status, t = apply_subst status context t in
  let keys =
   all_keys_of_cic_type metasenv subst context
    (snd (term_of_cic_term status t context))
@@ -660,6 +663,7 @@ let keys_of_type status orig_ty =
   (* Here we are dropping the metasenv (in the status), but this should not
      raise any exception (hopefully...) *)
   let _, ty, _ = saturate ~delta:max_int status orig_ty in
+  let _, ty = apply_subst status (ctx_of ty) ty in
   let keys =
 (*
     let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
@@ -772,7 +776,7 @@ let search_in_th gty th =
    | [] -> (* Ncic_termSet.elements *) acc
    | (_::tl) as k ->
        try 
-         let idx = List.assq k th in
+         let idx = List.assoc(*q*) k th in
          let acc = Ncic_termSet.union acc 
            (InvRelDiscriminationTree.retrieve_unifiables idx gty)
          in
@@ -897,7 +901,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
     else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status 
     else (* smart = 2: both *)
       try NTactics.apply_tac ("",0,t) status 
-      with Error _ as exc -> 
+      with Error _ -> 
         smart_apply_auto ("",0,t) eq_cache status 
   in
 (*
@@ -1202,10 +1206,22 @@ let rec guess_name name ctx =
 
 let is_prod status = 
   let _, ctx, gty = current_goal status in
+  let status, gty = apply_subst status ctx gty in
   let _, raw_gty = term_of_cic_term status gty ctx in
   match raw_gty with
-    | NCic.Prod (name,_,_) -> Some (guess_name name ctx)
-    | _ -> None
+    | NCic.Prod (name,src,_) ->
+        let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
+        (match snd (term_of_cic_term status src ctx) with
+        | NCic.Const(NReference.Ref (_,NReference.Ind _) as r) 
+        | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
+            let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys r in
+            (match itys with
+            | [_,_,_,[_;_]] 
+            | [_,_,_,[_]] 
+            | [_,_,_,[]] -> `Inductive (guess_name name ctx)         
+            | _ -> `Some (guess_name name ctx))
+        | _ -> `Some (guess_name name ctx))
+    | _ -> `None
 
 let intro ~depth status facts name =
   let status = NTactics.intro_tac name status in
@@ -1219,26 +1235,36 @@ let intro ~depth status facts name =
 ;;
 
 let rec intros_facts ~depth status facts =
+  if List.length (head_goals status#stack) <> 1 then status, facts else
   match is_prod status with
-    | Some(name) ->
+    | `Some(name) ->
         let status,facts =
           intro ~depth status facts name
         in intros_facts ~depth status facts 
+    | `Inductive name ->
+          let status = NTactics.case1_tac name status in
+          intros_facts ~depth status facts
     | _ -> status, facts
 ;; 
 
-let rec intros ~depth status cache =
+let intros ~depth status cache =
     match is_prod status with
-      | Some _ ->
+      | `Inductive _
+      | `Some _ ->
          let trace = cache.trace in
           let status,facts =
             intros_facts ~depth status cache.facts 
           in 
+          if head_goals status#stack = [] then 
+            let status = NTactics.merge_tac status in
+            [(0,Ast.Ident("__intros",None)),status], cache
+          else
             (* we reindex the equation from scratch *)
-          let unit_eq = 
-            index_local_equations status#eq_cache status in
-          status, init_cache ~facts ~unit_eq () ~trace
-      | _ -> status, cache
+            let unit_eq = index_local_equations status#eq_cache status in
+            let status = NTactics.merge_tac status in
+            [(0,Ast.Ident("__intros",None)),status], 
+            init_cache ~facts ~unit_eq () ~trace
+      | _ -> [],cache
 ;;
 
 let reduce ~whd ~depth status g = 
@@ -1264,6 +1290,9 @@ let reduce ~whd ~depth status g =
 ;;
 
 let do_something signature flags status g depth gty cache =
+  let l0, cache = intros ~depth status cache in
+  if l0 <> [] then l0, cache
+  else
   (* whd *)
   let l = (*reduce ~whd:true ~depth status g @*) reduce ~whd:true ~depth status g in
   (* if l <> [] then l,cache else *)
@@ -1537,7 +1566,6 @@ auto_main flags signature cache depth status: unit =
          raise (Gaveup IntSet.empty)
         else 
         let status = NTactics.branch_tac ~force:true status in
-        let status, cache = intros ~depth status cache in
         let g,gctx, gty = current_goal status in
         let ctx,ty = close status g in
         let closegty = mk_cic_term ctx ty in
@@ -1565,7 +1593,9 @@ auto_main flags signature cache depth status: unit =
              debug_print (~depth:depth) 
                (lazy ("Case: " ^ CicNotationPp.pp_term t));
              let depth,cache =
-              if t=Ast.Ident("__whd",None) then depth, cache 
+              if t=Ast.Ident("__whd",None) || 
+                  t=Ast.Ident("__intros",None) 
+               then depth, cache 
               else depth+1,loop_cache in 
             let cache = add_to_trace ~depth cache t in
             try