Debugger plus informatif

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3675 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 138 insertions, 83 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index fdafe9a64..3f9ad2fd7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -253,13 +253,14 @@ let lookup_genarg_interp id =
   try Gmap.find id !extragenargtab
   with Not_found -> failwith ("No interpretation function found for entry "^id)
 
-
 (* Unboxes VRec *)
 let unrec = function
   | VRec v -> !v
   | a -> a
 
-(************* GLOBALIZE ************)
+(*****************)
+(* Globalization *)
+(*****************)
 
 (* We have identifier <| global_reference <| constr *)
 
@@ -369,7 +370,7 @@ let glob_induction_arg ist = function
   | ElimOnAnonHyp n as x -> x
   | ElimOnIdent (_loc,id) as x -> ElimOnIdent (loc,id)
 
-(* Globalize a reduction expression *)
+(* Globalizes a reduction expression *)
 let glob_evaluable_or_metanum ist = function
   | AN qid -> AN (glob_reference ist qid)
   | MetaNum (_loc,n) -> MetaNum (loc,glob_metanum ist loc n)
@@ -457,7 +458,8 @@ let extract_let_names lrc =
 (* Globalizes tactics *)
 let rec glob_atomic lf (_,_,_,_ as ist) = function
   (* Basic tactics *)
-  | TacIntroPattern l -> TacIntroPattern (List.map (glob_intro_pattern lf ist) l)
+  | TacIntroPattern l ->
+      TacIntroPattern (List.map (glob_intro_pattern lf ist) l)
   | TacIntrosUntil hyp -> TacIntrosUntil (glob_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,ido') ->
       TacIntroMove (option_app (glob_ident lf ist) ido,
@@ -493,7 +495,8 @@ let rec glob_atomic lf (_,_,_,_ as ist) = function
   | TacTrivial l -> TacTrivial l
   | TacAuto (n,l) -> TacAuto (n,l)
   | TacAutoTDB n -> TacAutoTDB n
-  | TacDestructHyp (b,(_loc,_ as id)) -> TacDestructHyp(b,(loc,glob_hyp ist id))
+  | TacDestructHyp (b,(_loc,_ as id)) ->
+      TacDestructHyp(b,(loc,glob_hyp ist id))
   | TacDestructConcl -> TacDestructConcl
   | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
   | TacDAuto (n,p) -> TacDAuto (n,p)
@@ -524,7 +527,8 @@ let rec glob_atomic lf (_,_,_,_ as ist) = function
   (* Context management *)
   | TacClear l -> TacClear (List.map (glob_hyp_or_metanum ist) l)
   | TacClearBody l -> TacClearBody (List.map (glob_hyp_or_metanum ist) l)
-  | TacMove (dep,id1,id2) -> TacMove (dep,glob_lochyp ist id1,glob_lochyp ist id2)
+  | TacMove (dep,id1,id2) ->
+    TacMove (dep,glob_lochyp ist id1,glob_lochyp ist id2)
   | TacRename (id1,id2) -> TacRename (glob_lochyp ist id1, glob_lochyp ist id2)
 
   (* Constructors *)
@@ -568,11 +572,13 @@ and glob_tactic_seq (lfun,lmeta,sigma,env as ist) = function
       let lrc = List.map (fun (n,b) -> (n,glob_tactic_fun ist b)) lrc in
       lfun, TacLetRecIn (lrc,glob_tactic ist u)
   | TacLetIn (l,u) ->
-      let l = List.map (fun (n,c,b) -> (n,option_app (glob_constr_may_eval ist) c,glob_tacarg !strict_check ist b)) l in
+      let l = List.map (fun (n,c,b) -> (n,option_app (glob_constr_may_eval ist)
+              c,glob_tacarg !strict_check ist b)) l in
       let ist' = ((extract_let_names l)@lfun,lmeta,sigma,env) in
       lfun, TacLetIn (l,glob_tactic ist' u)
   | TacLetCut l ->
-      let f (n,c,t) = (n,glob_constr_may_eval ist c,glob_tacarg !strict_check ist t) in
+      let f (n,c,t) = (n,glob_constr_may_eval ist c,glob_tacarg !strict_check
+                      ist t) in
       lfun, TacLetCut (List.map f l)
   | TacMatchContext (lr,lmr) ->
       lfun, TacMatchContext(lr, glob_match_rule ist lmr)
@@ -657,7 +663,8 @@ and glob_genarg ist x =
   | ConstrArgType ->
       in_gen rawwit_constr (glob_constr ist (out_gen rawwit_constr x))
   | ConstrMayEvalArgType ->
-      in_gen rawwit_constr_may_eval (glob_constr_may_eval ist (out_gen rawwit_constr_may_eval x))
+      in_gen rawwit_constr_may_eval (glob_constr_may_eval ist
+      (out_gen rawwit_constr_may_eval x))
   | QuantHypArgType ->
       in_gen rawwit_quant_hyp
         (glob_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
@@ -677,8 +684,7 @@ and glob_genarg ist x =
   | PairArgType _ -> app_pair (glob_genarg ist) (glob_genarg ist) x
   | ExtraArgType s -> x
 
-
-(************* END GLOBALIZE ************)
+(**** End Globalization ****)
 
 (* Associates variables with values and gives the remaining variables and
    values *)
@@ -733,9 +739,10 @@ let rec read_match_rule evc env lfun = function
 (* For Match Context and Match *)
 exception No_match
 exception Not_coherent_metas
+exception Eval_fail
 
 let is_match_catchable = function
-  | No_match | FailError _ -> true
+  | No_match | Eval_fail | FailError _ -> true
   | e -> Logic.catchable_exception e
 
 (* Verifies if the matched list is coherent with respect to lcm *)
@@ -755,14 +762,23 @@ let apply_matching pat csr =
      PatternMatchingFailure -> raise No_match
 
 (* Tries to match one hypothesis pattern with a list of hypotheses *)
-let apply_one_mhyp_context gl lmatch mhyp lhyps noccopt =
+let apply_one_mhyp_context ist env gl lmatch mhyp lhyps noccopt =
   let get_pattern = function
     | Hyp (_,pat) -> pat
     | NoHypId pat -> pat
   and get_id_couple id = function
+    | Hyp((_,idpat),_) -> [idpat,VIdentifier id]
+    | NoHypId _ -> [] 
+  and get_info_pattern = function
+    | Hyp((_,idpat),pat) -> (Some idpat,pat)
+    | NoHypId pat -> (None,pat) in
+
+(*=======
     | Hyp((_,idpat),_) -> [idpat,VConstr (mkVar id)]
     | NoHypId _ -> [] in
-  let rec apply_one_mhyp_context_rec mhyp lhyps_acc nocc = function
+>>>>>>> 1.28*)
+
+  let rec apply_one_mhyp_context_rec ist env mhyp lhyps_acc nocc = function
     | (id,hyp)::tl ->
       (match (get_pattern mhyp) with
       | Term t ->
@@ -771,7 +787,7 @@ let apply_one_mhyp_context gl lmatch mhyp lhyps noccopt =
             verify_metas_coherence gl lmatch (Pattern.matches t hyp) in
           (get_id_couple id mhyp,[],lmeta,tl,(id,hyp),None)
          with | PatternMatchingFailure | Not_coherent_metas ->
-          apply_one_mhyp_context_rec mhyp (lhyps_acc@[id,hyp]) 0 tl)
+          apply_one_mhyp_context_rec ist env mhyp (lhyps_acc@[id,hyp]) 0 tl)
       | Subterm (ic,t) ->
         (try
           let (lm,ctxt) = sub_match nocc t hyp in
@@ -780,15 +796,37 @@ let apply_one_mhyp_context gl lmatch mhyp lhyps noccopt =
             ic,lmeta,tl,(id,hyp),Some nocc)
          with
         | NextOccurrence _ ->
-          apply_one_mhyp_context_rec mhyp (lhyps_acc@[id,hyp]) 0 tl
+          apply_one_mhyp_context_rec ist env mhyp (lhyps_acc@[id,hyp]) 0 tl
         | Not_coherent_metas ->
-          apply_one_mhyp_context_rec mhyp lhyps_acc (nocc + 1) ((id,hyp)::tl)))
-    | [] -> raise No_match in
+          apply_one_mhyp_context_rec ist env mhyp lhyps_acc (nocc + 1)
+                                     ((id,hyp)::tl)))
+    | [] ->
+      begin
+        db_hyp_pattern_failure ist.debug env (get_info_pattern mhyp);
+        raise No_match
+      end in
   let nocc =
     match noccopt with
     | None -> 0
     | Some n -> n in
-  apply_one_mhyp_context_rec mhyp [] nocc lhyps
+  apply_one_mhyp_context_rec ist env mhyp [] nocc lhyps
+
+(* Gets the identifier of the pattern if it exists *)
+let get_id_pattern = function
+  | [] -> None
+  | [(id,_)] -> Some id
+  | _ -> assert false
+
+(*
+let coerce_to_qualid loc = function
+  | Constr c when isVar c -> make_short_qualid (destVar c)
+  | Constr c -> 
+      (try qualid_of_sp (sp_of_global (Global.env()) (reference_of_constr c))
+      with Not_found -> invalid_arg_loc (loc, "Not a reference"))
+  | Identifier id -> make_short_qualid id
+  | Qualid qid -> qid
+  | _ -> invalid_arg_loc (loc, "Not a reference")
+*)
 
 let constr_to_id loc c =
   if isVar c then destVar c
@@ -884,6 +922,9 @@ let hyp_or_metanum_interp ist gl = function
   | AN id -> eval_variable ist gl (dummy_loc,id)
   | MetaNum (loc,n) -> constr_to_id loc (List.assoc n ist.lmatch)
 
+(* To avoid to move to much simple functions in the big recursive block *)
+let forward_vcontext_interp = ref (fun ist v -> failwith "not implemented")
+
 let interp_pure_qualid is_applied env (loc,qid) =
   try VConstr (constr_of_reference (find_reference env qid))
   with Not_found ->
@@ -1072,12 +1113,12 @@ let rec val_interp ist gl tac =
     | TacArg a -> tacarg_interp ist gl a
     (* Delayed evaluation *)
     | t -> VTactic (eval_tactic ist t)
-
- in
+  in 
   match ist.debug with
-    | DebugOn n ->
-	debug_prompt n (Some gl) tac (fun v -> value_interp {ist with debug=v})
-    | _ -> value_interp ist
+  | DebugOn | Run _ ->
+    let debug = debug_prompt gl ist.debug tac in
+    value_interp {ist with debug=debug}
+  | _ -> value_interp ist
 
 and eval_tactic ist = function
   | TacAtom (loc,t) -> fun gl ->
@@ -1176,7 +1217,7 @@ and eval_with_fail interp tac goal =
     | a -> a)
   with | FailError lvl ->
     if lvl = 0 then
-      raise No_match
+      raise Eval_fail
     else
       raise (FailError (lvl - 1))
 
@@ -1200,7 +1241,6 @@ and letin_interp ist gl = function
       let v = tacarg_interp ist gl t in
       check_is_value v;
       (id,v):: (letin_interp ist gl tl)
-
   | ((loc,id),Some com,tce)::tl ->
     let typ = interp_may_eval pf_interp_constr ist gl com
     and v = tacarg_interp ist gl tce in
@@ -1248,14 +1288,9 @@ and letcut_interp ist = function
     and exat = h_exact csr in
     tclTHENSV cutt [|tclTHEN (introduction id) (letcut_interp ist tl);exat|] gl
 
-(*      let lic = mkLetIn (Name id,csr,typ,ccl) in
-      let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in
-      tclTHEN ntac (tclTHEN (introduction id)
-      (letcut_interp ist tl))*)
-
 (* Interprets the Match Context expressions *)
-and match_context_interp ist goal lr lmr =
-  let rec apply_goal_sub ist nocc (id,c) csr mt mhyps hyps =
+and match_context_interp ist g lr lmr =
+  let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps =
     try
       let (lgoal,ctxt) = sub_match nocc c csr in
       let lctxt = give_context ctxt id in
@@ -1264,18 +1299,23 @@ and match_context_interp ist goal lr lmr =
           (val_interp {ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch})
           mt goal
       else
-        apply_hyps_context ist goal mt lgoal mhyps hyps
+        apply_hyps_context ist env goal mt lgoal mhyps hyps
     with
     | (FailError _) as e -> raise e
     | NextOccurrence _ -> raise No_match
     | e when e = No_match or Logic.catchable_exception e ->
-      apply_goal_sub ist (nocc + 1) (id,c) csr mt mhyps hyps in
-  let rec apply_match_context ist = function
+      apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
+  let rec apply_match_context ist env goal nrs lex lpt = 
+    begin
+    if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex);
+    match lpt with
     | (All t)::tl ->
-      (try
-         eval_with_fail (val_interp ist) t goal
-       with No_match | FailError _ -> apply_match_context ist tl
-	 | e when Logic.catchable_exception e -> apply_match_context ist tl)
+      begin
+        db_mc_pattern_success ist.debug;
+        try eval_with_fail (val_interp ist) t goal
+         with e when is_match_catchable e ->
+           apply_match_context ist env goal (nrs+1) (List.tl lex) tl
+      end
     | (Pat (mhyps,mgoal,mt))::tl ->
       let hyps = make_hyps (pf_hyps goal) in
       let hyps = if lr then List.rev hyps else hyps in
@@ -1288,63 +1328,77 @@ and match_context_interp ist goal lr lmr =
             begin
             db_matched_concl ist.debug (pf_env goal) concl;
             if mhyps = [] then
-              eval_with_fail
-		(val_interp {ist with lmatch=lgoal@ist.lmatch}) mt goal
+            begin
+              db_mc_pattern_success ist.debug;
+              eval_with_fail (val_interp
+                {ist with lmatch=lgoal@ist.lmatch}) mt goal
+            end
             else
-              apply_hyps_context ist goal mt lgoal mhyps hyps
+              apply_hyps_context ist env goal mt lgoal mhyps hyps
             end)
-        with e when is_match_catchable e -> apply_match_context ist tl)
+        with 
+        | e when is_match_catchable e ->
+          begin 
+            (match e with
+            | No_match -> db_matching_failure ist.debug
+            | Eval_fail -> db_eval_failure ist.debug
+            | _ -> db_logic_failure ist.debug e);
+            apply_match_context ist env goal (nrs+1) (List.tl lex) tl
+          end)
       |	Subterm (id,mg) ->
-        (try
-          apply_goal_sub ist 0 (id,mg) concl mt mhyps hyps
-        with e when is_match_catchable e ->
-	  apply_match_context ist tl))
+        (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps
+         with e when is_match_catchable e ->
+           apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
     | _ ->
-      errorlabstrm "Tacinterp.apply_match_context" (str
-        "No matching clauses for Match Context")
-
-  in
-  let env = pf_env goal in
-  apply_match_context ist 
-    (read_match_rule (project goal) env (constr_list ist env) lmr)
+      errorlabstrm "Tacinterp.apply_match_context"
+        (v 0 (str "No matching clauses for Match Context" ++
+        (if ist.debug=DebugOff then
+           fnl() ++ str "(use \"Debug On\" for more info)"
+         else mt())))
+    end in
+  let env = pf_env g in
+  apply_match_context ist env g 0 lmr
+    (read_match_rule (project g) env (constr_list ist env) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
-and apply_hyps_context ist goal mt lgmatch mhyps hyps =
-  let rec apply_hyps_context_rec mt lfun lmatch mhyps lhyps_mhyp
+and apply_hyps_context ist env goal mt lgmatch mhyps hyps =
+  let rec apply_hyps_context_rec ist mt lfun lmatch mhyps lhyps_mhyp
     lhyps_rest noccopt =
     match mhyps with
       | hd::tl ->
         let (lid,lc,lm,newlhyps,hyp_match,noccopt) =
-          apply_one_mhyp_context goal lmatch hd lhyps_mhyp noccopt in
+          apply_one_mhyp_context ist env goal lmatch hd lhyps_mhyp noccopt in
         begin
-        db_matched_hyp ist.debug (pf_env goal) hyp_match;
-        (try
-        if tl = [] then
-            eval_with_fail
-              (val_interp {ist with lfun=lfun@lid@lc@ist.lfun;
-                                    lmatch=lmatch@lm@ist.lmatch})
-              mt goal
-        else
-          let nextlhyps =
-            List.fold_left (fun l e -> if e = hyp_match then l else l@[e]) []
-              lhyps_rest in
-          apply_hyps_context_rec mt
-            (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
-         with
-        | (FailError _) as e -> raise e
-	|  e when is_match_catchable e -> 
-          (match noccopt with
-          | None ->
-            apply_hyps_context_rec mt lfun
-              lmatch mhyps newlhyps lhyps_rest None
-          | Some nocc ->
-            apply_hyps_context_rec mt ist.lfun ist.lmatch mhyps
-              (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1))))
+          db_matched_hyp ist.debug (pf_env goal) hyp_match
+                         (get_id_pattern lid);
+          (try
+          if tl = [] then
+          begin
+            db_mc_pattern_success ist.debug;
+            eval_with_fail (val_interp {ist with lfun=lfun@lid@lc@ist.lfun;
+                                        lmatch=lmatch@lm@ist.lmatch}) mt goal
+          end
+          else
+            let nextlhyps =
+              List.fold_left (fun l e -> if e = hyp_match then l else l@[e]) []
+                lhyps_rest in
+            apply_hyps_context_rec ist mt
+              (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
+           with
+           | (FailError _) as e -> raise e
+	   | e when is_match_catchable e -> 
+             (match noccopt with
+             | None ->
+               apply_hyps_context_rec ist mt lfun
+                 lmatch mhyps newlhyps lhyps_rest None
+             | Some nocc ->
+               apply_hyps_context_rec ist mt ist.lfun ist.lmatch mhyps
+                 (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1))))
         end
       |	[] ->
         anomalylabstrm "apply_hyps_context_rec" (str
           "Empty list should not occur") in
-  apply_hyps_context_rec mt [] lgmatch mhyps hyps hyps None
+  apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None
 
   (* Interprets extended tactic generic arguments *)
 and genarg_interp ist goal x =
@@ -1517,7 +1571,8 @@ and interp_atomic ist gl = function
 
   (* Conversion *)
   | TacReduce (r,cl) ->
-      h_reduce (pf_redexp_interp ist gl r) (List.map (interp_hyp_location ist gl) cl)
+      h_reduce (pf_redexp_interp ist gl r) (List.map
+               (interp_hyp_location ist gl) cl)
   | TacChange (occl,c,cl) ->
       h_change (option_app (pf_pattern_interp ist gl) occl)
         (pf_constr_interp ist gl c) (List.map (interp_hyp_location ist gl) cl)