diff options
| -rw-r--r-- | proofs/tactic_debug.ml | 23 | ||||
| -rw-r--r-- | proofs/tactic_debug.mli | 3 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 55 |
3 files changed, 26 insertions, 55 deletions
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 1e2111639..316aa0ee5 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -18,7 +18,6 @@ open Printer type debug_info = | DebugOn of int | DebugOff - | Exit (* Prints the goal if it exists *) let db_pr_goal = function @@ -49,7 +48,7 @@ let rec db_print_error = function hov 0 (str "Uncaught exception ") (* Prints the state and waits for an instruction *) -let debug_prompt level goalopt tac_ast f exit = +let debug_prompt level goalopt tac_ast f = db_pr_goal goalopt; msg (str "Going to execute:" ++ fnl () ++ (pr_raw_tactic tac_ast) ++ fnl ()); (* str "Commands: <Enter>=Continue, s=Skip, x=Exit" >];*) @@ -63,34 +62,32 @@ let debug_prompt level goalopt tac_ast f exit = match inst with | "" -> DebugOn (level+1) | "s" -> DebugOff - | "x" -> Exit + | "x" -> raise Sys.Break | "h" -> begin help (); prompt () end | _ -> prompt () in - match prompt () with - | Exit -> exit () - | d -> - try f d - with e when Logic.catchable_exception e -> - ppnl (str "Level " ++ int level ++ str ": " ++ db_print_error e); - raise e + let d = prompt () in + try f d + with e when e <> Sys.Break -> + ppnl (str "Level " ++ int level ++ str ": " ++ db_print_error e); + raise e (* Prints a constr *) let db_constr debug env c = - if debug <> DebugOff & debug <> Exit then + if debug <> DebugOff then msgnl (str "Evaluated term --> " ++ prterm_env env c) (* Prints a matched hypothesis *) let db_matched_hyp debug env (id,c) = - if debug <> DebugOff & debug <> Exit then + if debug <> DebugOff then msgnl (str "Matched hypothesis --> " ++ str (Names.string_of_id id^": ") ++ prterm_env env c) (* Prints the matched conclusion *) let db_matched_concl debug env c = - if debug <> DebugOff & debug <> Exit then + if debug <> DebugOff then msgnl (str "Matched goal --> " ++ prterm_env env c) diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 1bb8a7f42..9b542c784 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -20,11 +20,10 @@ open Term type debug_info = | DebugOn of int | DebugOff - | Exit (* Prints the state and waits *) val debug_prompt : int -> goal sigma option -> Tacexpr.raw_tactic_expr -> - (debug_info -> 'a) -> (unit -> 'a) -> 'a + (debug_info -> 'a) -> 'a (* Prints a constr *) val db_constr : debug_info -> Environ.env -> constr -> unit diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 787ef7701..b3656c419 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -99,19 +99,7 @@ let constr_of_VConstr_context = function anomalylabstrm "constr_of_VConstr_context" (str "Not a Constr_context tactic_arg") -(* -(* Gives identifiers and makes the possible injection constr -> ident *) -let make_ids ast = function - | Identifier id -> id - | Constr c -> - (try destVar c with - | Invalid_argument "destVar" -> - anomalylabstrm "make_ids" - (str "This term cannot be reduced to an identifier" ++ fnl () ++ - print_ast ast)) - | _ -> anomalylabstrm "make_ids" (str "Not an identifier") -*) - +(* Displays a value *) let pr_value env = function | VVoid -> str "()" | VInteger n -> int n @@ -1079,7 +1067,7 @@ let rec val_interp ist gl tac = | TacLetIn (l,u) -> let addlfun = letin_interp ist gl l in val_interp { ist with lfun=addlfun@ist.lfun } gl u - | TacMatchContext (lr,lmr) -> match_context_interp ist gl lr lmr + | TacMatchContext (lr,lmr) -> match_context_interp ist gl lr lmr | TacMatch (c,lmr) -> match_interp ist gl c lmr | TacArg a -> tacarg_interp ist gl a (* Delayed evaluation *) @@ -1088,14 +1076,12 @@ let rec val_interp ist gl tac = in match ist.debug with | DebugOn n -> - debug_prompt n (Some gl) tac - (fun v -> value_interp {ist with debug=v}) - (fun () -> VTactic tclIDTAC) + debug_prompt n (Some gl) tac (fun v -> value_interp {ist with debug=v}) | _ -> value_interp ist and eval_tactic ist = function | TacAtom (loc,t) -> fun gl -> - (try (interp_atomic ist gl t) gl + (try interp_atomic ist gl t gl with e -> Stdpp.raise_with_loc loc e) | TacFun (it,body) -> assert false | TacLetRecIn (lrc,u) -> assert false @@ -1407,32 +1393,21 @@ and genarg_interp ist goal x = (* Interprets the Match expressions *) and match_interp ist g constr lmr = let rec apply_sub_match ist nocc (id,c) csr mt = - try + try let (lm,ctxt) = sub_match nocc c csr in let lctxt = give_context ctxt id in - eval_with_fail - (val_interp { ist with lfun=lctxt@ist.lfun; lmatch=lm@ist.lmatch}) - mt g - with - | NextOccurrence n -> raise No_match - | (FailError _) as e -> raise e - | e when is_match_catchable e -> - apply_sub_match ist (nocc + 1) (id,c) csr mt + val_interp {ist with lfun=lctxt@ist.lfun; lmatch=lm@ist.lmatch} g mt + with | NextOccurrence _ -> raise No_match in let rec apply_match ist csr = function | (All t)::_ -> - (try - eval_with_fail (val_interp ist) t g - with - | (FailError _) as e -> raise e - | e when is_match_catchable e -> apply_match ist csr []) + (try val_interp ist g t + with e when is_match_catchable e -> apply_match ist csr []) | (Pat ([],Term c,mt))::tl -> (try - eval_with_fail (val_interp - { ist with lmatch=(apply_matching c csr)@ist.lmatch }) mt g - with - | (FailError _) as e -> raise e - | e when is_match_catchable e -> apply_match ist csr tl) + val_interp + { ist with lmatch=(apply_matching c csr)@ist.lmatch } g mt + with e when is_match_catchable e -> apply_match ist csr tl) | (Pat ([],Subterm (id,c),mt))::tl -> (try apply_sub_match ist 0 (id,c) csr mt @@ -1447,8 +1422,8 @@ and match_interp ist g constr lmr = apply_match ist csr ilr (* Interprets tactic expressions : returns a "tactic" *) -and tactic_interp ist tac g = - try tactic_of_value (val_interp ist g tac) g +and tactic_interp ist tac gl = + try tactic_of_value (val_interp ist gl tac) gl with | NotTactic -> errorlabstrm "Tacinterp.tac_interp" (str "Must be a command or must give a tactic value") @@ -1571,7 +1546,7 @@ and interp_atomic ist gl = function tactic_of_value (val_interp { ist with lfun=lfun } gl body) gl (* Interprets tactic arguments *) -let interp_tacarg sign ast = (*unvarg*) (val_interp sign ast) +let interp_tacarg sign ast = val_interp sign ast (* Initial call for interpretation *) let tac_interp lfun lmatch debug t = |