diff options
author | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-30 16:56:19 +0000 |
---|---|---|
committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-30 16:56:19 +0000 |
commit | 2c13632cd7296072ab5271fc047cda720f23686c (patch) | |
tree | bd6ed3886cee140c56ffdf88e83cab3d6208909e | |
parent | cae025c40c270a23ffef489d855346dd86944aa6 (diff) |
Tactiques utilisateur + debugger
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@786 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | proofs/tacinterp.ml | 344 | ||||
-rw-r--r-- | proofs/tacinterp.mli | 23 | ||||
-rw-r--r-- | proofs/tactic_debug.ml | 47 | ||||
-rw-r--r-- | proofs/tactic_debug.mli | 21 |
4 files changed, 301 insertions, 134 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 014dda7e7..98f2b3554 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -3,6 +3,7 @@ open Astterm open Closure +open Dyn (* open Generic *) open Libobject open Pattern @@ -14,6 +15,7 @@ open Util open Names open Proof_type open Tacmach +open Tactic_debug open Macros open Coqast open Ast @@ -80,7 +82,33 @@ let rec constr_list goalopt = function (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = enamed_declarations * Environ.env * (string * value) list * - (int * constr) list * goal sigma option + (int * constr) list * goal sigma option * debug_info + +(* For user tactics *) +let ((ocamlIn : (unit -> Coqast.t) -> Dyn.t), + (ocamlOut : Dyn.t -> (unit -> Coqast.t))) = create "ocaml" + +(* To provide the tactic expressions *) +let loc = (0,0) +let tacticIn t = Dynamic (loc,ocamlIn t) + +(* References for dynamic interpretation of user tactics. They are all + initialized with dummy values *) +let r_evc = ref Evd.empty +let r_env = ref Environ.empty_env +let r_lfun = ref [] +let r_lmatch = ref [] +let r_goalopt = ref None +let r_debug = ref DebugOn + +(* Updates the references with the current environment *) +let env_update (evc,env,lfun,lmatch,goalopt,debug) = + r_evc := evc; + r_env := env; + r_lfun := lfun; + r_lmatch := lmatch; + r_goalopt := goalopt; + r_debug := debug (* Table of interpretation functions *) let interp_tab = @@ -362,75 +390,88 @@ let rec make_subs_list = function | e::tl -> make_subs_list tl | [] -> [] +(* Debug reference *) +let debug =ref DebugOff + +(* Sets the debugger mode *) +let set_debug pos = debug := pos + +(* Gives the state of debug *) +let get_debug () = !debug + (* Interprets any expression *) -let rec val_interp (evc,env,lfun,lmatch,goalopt) ast = +let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast = (* mSGNL [<print_ast ast>]; *) (* mSGNL [<print_ast (Termast.ast_of_constr false (Pretty.assumptions_for_print []) c)>] *) + let value_interp debug = match ast with | Node(_,"APP",l) -> - let fv = val_interp (evc,env,lfun,lmatch,goalopt) (List.hd l) - and largs = List.map (val_interp (evc,env,lfun,lmatch,goalopt)) (List.tl - l) in - app_interp evc env lfun lmatch goalopt fv largs ast + let fv = val_interp (evc,env,lfun,lmatch,goalopt,debug) (List.hd l) + and largs = List.map (val_interp (evc,env,lfun,lmatch,goalopt,debug)) + (List.tl l) in + app_interp (evc,env,lfun,lmatch,goalopt,debug) fv largs ast | Node(_,"FUN",l) -> VFun (lfun,read_fun (List.hd l),List.nth l 1) - | Node(_,"REC",l) -> rec_interp evc env lfun lmatch goalopt ast l + | Node(_,"REC",l) -> + rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast l | Node(_,"LET",[Node(_,"LETDECL",l);u]) -> - let addlfun=let_interp evc env lfun lmatch goalopt ast l in - val_interp (evc,env,(lfun@addlfun),lmatch,goalopt) u + let addlfun=let_interp (evc,env,lfun,lmatch,goalopt,debug) ast l in + val_interp (evc,env,(lfun@addlfun),lmatch,goalopt,debug) u | Node(_,"MATCHCONTEXT",lmr) -> - match_context_interp evc env lfun lmatch goalopt ast lmr + match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr | Node(_,"MATCH",lmr) -> - match_interp evc env lfun lmatch goalopt ast lmr + match_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr | Node(_,"IDTAC",[]) -> VTactic tclIDTAC | Node(_,"FAIL",[]) -> VTactic (tclFAIL 0) | Node(_,"FAIL",[n]) -> VTactic (tclFAIL (num_of_ast n)) | Node(_,"TACTICLIST",l) -> - VTactic (interp_semi_list tclIDTAC lfun lmatch l) + VTactic (interp_semi_list tclIDTAC lfun lmatch debug l) | Node(_,"DO",[n;tac]) -> - VTactic (tclDO (num_of_ast n) (tac_interp lfun lmatch tac)) + VTactic (tclDO (num_of_ast n) (tac_interp lfun lmatch debug tac)) | Node(_,"TRY",[tac]) -> - VTactic (tclTRY (tac_interp lfun lmatch tac)) + VTactic (tclTRY (tac_interp lfun lmatch debug tac)) | Node(_,"INFO",[tac]) -> - VTactic (tclINFO (tac_interp lfun lmatch tac)) + VTactic (tclINFO (tac_interp lfun lmatch debug tac)) | Node(_,"REPEAT",[tac]) -> - VTactic (tclREPEAT (tac_interp lfun lmatch tac)) + VTactic (tclREPEAT (tac_interp lfun lmatch debug tac)) | Node(_,"ORELSE",[tac1;tac2]) -> - VTactic (tclORELSE (tac_interp lfun lmatch tac1) (tac_interp lfun lmatch - tac2)) + VTactic (tclORELSE (tac_interp lfun lmatch debug tac1) + (tac_interp lfun lmatch debug tac2)) | Node(_,"FIRST",l) -> - VTactic (tclFIRST (List.map (tac_interp lfun lmatch) l)) + VTactic (tclFIRST (List.map (tac_interp lfun lmatch debug) l)) | Node(_,"TCLSOLVE",l) -> - VTactic (tclSOLVE (List.map (tac_interp lfun lmatch) l)) + VTactic (tclSOLVE (List.map (tac_interp lfun lmatch debug) l)) | Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) -> - val_interp (evc,env,lfun,lmatch,goalopt) (Node(loc0,"APP",[Node(loc1, - "PRIM-TACTIC",[Node(loc1,s,[])])]@l)) + val_interp (evc,env,lfun,lmatch,goalopt,debug) + (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l)) | Node(_,"PRIM-TACTIC",[Node(loc,opn,[])]) -> VFTactic ([],(interp_atomic loc opn)) | Node(_,"VOID",[]) -> VVoid | Nvar(_,s) -> - (try (unrec (List.assoc s (List.rev lfun))) + (try (unrec (List.assoc s lfun)) with | Not_found -> (try (lookup s) with | Not_found -> VArg (Identifier (id_of_string s)))) | Str(_,s) -> VArg (Quoted_string s) | Num(_,n) -> VArg (Integer n) - | Node(_,"COMMAND",[c]) -> com_interp (evc,env,lfun,lmatch,goalopt) c + | Node(_,"COMMAND",[c]) -> + com_interp (evc,env,lfun,lmatch,goalopt,debug) c | Node(_,"CASTEDCOMMAND",[c]) -> - cast_com_interp (evc,env,lfun,lmatch,goalopt) c + cast_com_interp (evc,env,lfun,lmatch,goalopt,debug) c | Node(_,"CASTEDOPENCOMMAND",[c]) -> - cast_opencom_interp (evc,env,lfun,lmatch,goalopt) c + cast_opencom_interp (evc,env,lfun,lmatch,goalopt,debug) c | Node(_,"BINDINGS",astl) -> - VArg (Cbindings (List.map (bind_interp evc env lfun lmatch goalopt) - astl)) + VArg (Cbindings (List.map (bind_interp + (evc,env,lfun,lmatch,goalopt,debug)) astl)) | Node(_,"REDEXP",[Node(_,redname,args)]) -> - VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt) + VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug) (redname,args))) | Node(_,"CLAUSE",cl) -> VArg (Clause (List.map (fun ast -> id_of_Identifier (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt) ast))) cl)) - | Node(_,"TACTIC",[ast]) -> VArg (Tac (tac_interp lfun lmatch ast)) + (evc,env,lfun,lmatch,goalopt,debug) ast))) cl)) + | Node(_,"TACTIC",[ast]) -> + VArg (Tac (tac_interp lfun lmatch debug ast)) (*Remains to treat*) | Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) -> VArg ((Fixexp (id_of_string s,n,c))) @@ -438,34 +479,45 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt) ast = VArg ((Cofixexp (id_of_string s,c))) (*End of Remains to treat*) | Node(_,"INTROPATTERN", [ast]) -> - VArg ((Intropattern (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt) - ast))) + VArg ((Intropattern (cvt_intro_pattern + (evc,env,lfun,lmatch,goalopt,debug) ast))) | Node(_,"LETPATTERNS",astl) -> VArg (Letpatterns (List.fold_left (cvt_letpattern - (evc,env,lfun,lmatch,goalopt)) (None,[]) astl)) + (evc,env,lfun,lmatch,goalopt,debug)) (None,[]) astl)) | Node(loc,s,l) -> (try - ((look_for_interp s) (evc,env,lfun,lmatch,goalopt) ast) + ((look_for_interp s) (evc,env,lfun,lmatch,goalopt,debug) ast) with Not_found -> - val_interp (evc,env,lfun,lmatch,goalopt) + val_interp (evc,env,lfun,lmatch,goalopt,debug) (Node(dummy_loc,"APPTACTIC",[ast]))) + + | Dynamic(_,t) -> + env_update (evc,env,lfun,lmatch,goalopt,debug); + let f = (ocamlOut t) in + Obj.magic (val_interp (evc,env,lfun,lmatch,goalopt,debug) (f ())) | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",[<'sTR - "Unrecognizable ast: "; print_ast ast>]) + "Unrecognizable ast: "; print_ast ast>]) in + if debug = DebugOn then + match debug_prompt goalopt ast with + | Exit -> VTactic tclIDTAC + | v -> value_interp v + else + value_interp debug (* Interprets an application node *) -and app_interp evc env lfun lmatch goalopt fv largs ast = +and app_interp (evc,env,lfun,lmatch,goalopt,debug) fv largs ast = match fv with | VFTactic(l,f) -> VFTactic(l@(List.map unvarg largs),f) | VFun(olfun,var,body) -> let (newlfun,lvar,lval)=head_with_value (var,largs) in if lvar=[] then if lval=[] then - val_interp (evc,env,(olfun@newlfun),lmatch,goalopt) body + val_interp (evc,env,(olfun@newlfun),lmatch,goalopt,debug) body else - app_interp evc env lfun lmatch goalopt (val_interp (evc,env, - (olfun@newlfun),lmatch,goalopt) body) lval ast + app_interp (evc,env,lfun,lmatch,goalopt,debug) (val_interp (evc,env, + (olfun@newlfun),lmatch,goalopt,debug) body) lval ast else VFun(olfun@newlfun,lvar,body) | _ -> @@ -473,7 +525,7 @@ and app_interp evc env lfun lmatch goalopt fv largs ast = "Illegal application: "; print_ast ast>]) (* Interprets recursive expressions *) -and rec_interp evc env lfun lmatch goalopt ast = function +and rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function | [Node(_,"RECCLAUSE",_)] as l -> let (name,var,body) = List.hd (read_rec_clauses l) and ve = ref VVoid in @@ -491,24 +543,24 @@ and rec_interp evc env lfun lmatch goalopt ast = function var,body))) lrc in begin List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve; - val_interp (evc,env,(lfun@lve),lmatch,goalopt) u + val_interp (evc,env,(lfun@lve),lmatch,goalopt,debug) u end | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",[<'sTR "Rec not well formed: "; print_ast ast>]) (* Interprets the clauses of a let *) -and let_interp evc env lfun lmatch goalopt ast = function +and let_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function | [] -> [] | Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl -> - (id,val_interp (evc,env,lfun,lmatch,goalopt) t)::(let_interp evc env lfun - lmatch goalopt ast tl) + (id,val_interp (evc,env,lfun,lmatch,goalopt,debug) t):: + (let_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl) | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",[<'sTR "Let not well formed: "; print_ast ast>]) (* Interprets the Match Context expressions *) -and match_context_interp evc env lfun lmatch goalopt ast lmr = +and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr = let goal = (match goalopt with | None -> @@ -521,10 +573,11 @@ and match_context_interp evc env lfun lmatch goalopt ast lmr = let (lgoal,ctxt) = sub_match nocc c csr in let lctxt = give_context ctxt id in if mhyps = [] then - eval_with_fail (val_interp (evc,env,lctxt@lfun,lgoal@lmatch,Some goal)) - mt goal + eval_with_fail (val_interp + (evc,env,lctxt@lfun,lgoal@lmatch,Some goal,debug)) mt goal else - apply_hyps_context evc env (lctxt@lfun) lmatch goal mt lgoal mhyps hyps + apply_hyps_context evc env (lctxt@lfun) lmatch goal debug mt lgoal + mhyps hyps with | (FailError _) as e -> raise e | NextOccurrence _ -> raise No_match @@ -533,26 +586,33 @@ and match_context_interp evc env lfun lmatch goalopt ast lmr = hyps in let rec apply_match_context evc env lfun lmatch goal = function | (All t)::tl -> - (try eval_with_fail (val_interp (evc,env,lfun,lmatch,Some goal)) t goal - with No_match -> apply_match_context evc env lfun lmatch goal tl) + (try + eval_with_fail (val_interp (evc,env,lfun,lmatch,Some goal,debug)) t + goal + with No_match | _ -> apply_match_context evc env lfun lmatch goal tl) | (Pat (mhyps,mgoal,mt))::tl -> - let hyps = make_hyps (pf_hyps goal) + let hyps = make_hyps (List.rev (pf_hyps goal)) and concl = pf_concl goal in (match mgoal with | Term mg -> (try (let lgoal = apply_matching mg concl in + begin + db_matched_concl debug env concl; if mhyps = [] then - eval_with_fail (val_interp (evc,env,lfun,lgoal@lmatch,Some goal)) - mt goal + eval_with_fail (val_interp + (evc,env,lfun,lgoal@lmatch,Some goal,debug)) mt goal else - apply_hyps_context evc env lfun lmatch goal mt lgoal mhyps hyps) - with | No_match -> apply_match_context evc env lfun lmatch goal tl) + apply_hyps_context evc env lfun lmatch goal debug mt lgoal mhyps + hyps + end) + with | No_match | _ -> + apply_match_context evc env lfun lmatch goal tl) | Subterm (id,mg) -> (try apply_goal_sub evc env lfun lmatch goal 0 (id,mg) concl mt mhyps hyps with - | No_match -> apply_match_context evc env lfun lmatch goal tl)) + | No_match | _ -> apply_match_context evc env lfun lmatch goal tl)) | _ -> errorlabstrm "Tacinterp.apply_match_context" [<'sTR "No matching clauses for Match Context">] in @@ -560,24 +620,26 @@ and match_context_interp evc env lfun lmatch goalopt ast lmr = (constr_list goalopt lfun) lmr) (* Tries to match the hypotheses in a Match Context *) -and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps - hyps = +and apply_hyps_context evc env lfun_glob lmatch_glob goal debug mt lgmatch + mhyps hyps = let rec apply_hyps_context_rec evc env lfun_glob lmatch_glob goal 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 lmatch hd lhyps_mhyp noccopt in + begin + db_matched_hyp debug env hyp_match; (try if tl = [] then eval_with_fail (val_interp (evc,env,(lfun@lid@lc@lfun_glob), - (lmatch@lm@lmatch_glob),Some goal)) mt goal + (lmatch@lm@lmatch_glob),Some goal,debug)) 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 evc env lfun_glob lmatch_glob goal mt - (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None + (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None with | (FailError _) as e -> raise e | _ -> @@ -589,6 +651,7 @@ and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun lmatch mhyps (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1)))) + end | [] -> anomalylabstrm "apply_hyps_context_rec" [<'sTR "Empty list should not occur" >] in @@ -596,90 +659,101 @@ and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps hyps hyps None (* Interprets the Match expressions *) -and match_interp evc env lfun lmatch goalopt ast lmr = - let rec apply_sub_match evc env lfun lmatch goalopt nocc (id,c) csr mt = +and match_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr = + let rec apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) nocc (id,c) csr + mt = match goalopt with | None -> (try let (lm,ctxt) = sub_match nocc c csr in let lctxt = give_context ctxt id in - val_interp (evc,env,lctxt@lfun,lm@lmatch,goalopt) mt + val_interp (evc,env,lctxt@lfun,lm@lmatch,goalopt,debug) mt with | NextOccurrence _ -> raise No_match) | Some g -> (try let (lm,ctxt) = sub_match nocc c csr in let lctxt = give_context ctxt id in - eval_with_fail (val_interp (evc,env,lctxt@lfun,lm@lmatch,goalopt)) mt g + eval_with_fail (val_interp + (evc,env,lctxt@lfun,lm@lmatch,goalopt,debug)) mt g with | NextOccurrence n -> raise No_match | (FailError _) as e -> raise e | _ -> - apply_sub_match evc env lfun lmatch goalopt (nocc + 1) (id,c) csr mt) + apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) (nocc + 1) (id,c) + csr mt) in - let rec apply_match evc env lfun lmatch goalopt csr = function - | (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t + let rec apply_match (evc,env,lfun,lmatch,goalopt,debug) csr = function + | (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt,debug) t | (Pat ([],mp,mt))::tl -> (match mp with | Term c -> (try - val_interp (evc,env,lfun,(apply_matching c csr)@lmatch,goalopt) mt - with | No_match -> apply_match evc env lfun lmatch goalopt csr tl) + val_interp + (evc,env,lfun,(apply_matching c csr)@lmatch,goalopt,debug) mt + with | No_match -> + apply_match (evc,env,lfun,lmatch,goalopt,debug) csr tl) | Subterm (id,c) -> - (try apply_sub_match evc env lfun lmatch goalopt 0 (id,c) csr mt - with | No_match -> apply_match evc env lfun lmatch goalopt csr tl)) + (try + apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) 0 (id,c) csr mt + with | No_match -> + apply_match (evc,env,lfun,lmatch,goalopt,debug) csr tl)) | _ -> errorlabstrm "Tacinterp.apply_match" [<'sTR "No matching clauses for Match">] in - let csr = constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - (List.hd lmr))) + let csr = + constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug) + (List.hd lmr))) and ilr = read_match_rule evc env (constr_list goalopt lfun) (List.tl lmr) in - apply_match evc env lfun lmatch goalopt csr ilr + apply_match (evc,env,lfun,lmatch,goalopt,debug) csr ilr (* Interprets tactic expressions *) -and tac_interp lfun lmatch ast g = +and tac_interp lfun lmatch debug ast g = let evc = project g and env = pf_env g in - match (val_interp (evc,env,lfun,lmatch,(Some g)) ast) with + match (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) with | VTactic tac -> (tac g) | VFTactic (largs,f) -> (f largs g) | VRTactic res -> res | _ -> - errorlabstrm "Tacinterp.interp_rec" [<'sTR + errorlabstrm "Tacinterp.tac_interp" [<'sTR "Interpretation gives a non-tactic value">] (* Interprets a primitive tactic *) and interp_atomic loc opn args = vernac_tactic(opn,args) (* Interprets sequences of tactics *) -and interp_semi_list acc lfun lmatch = function +and interp_semi_list acc lfun lmatch debug = function | (Node(_,"TACLIST",seq))::l -> - interp_semi_list (tclTHENS acc (List.map (tac_interp lfun lmatch) seq)) - lfun lmatch l + interp_semi_list (tclTHENS acc (List.map (tac_interp lfun lmatch debug) + seq)) lfun lmatch debug l | t::l -> - interp_semi_list (tclTHEN acc (tac_interp lfun lmatch t)) lfun lmatch l + interp_semi_list (tclTHEN acc (tac_interp lfun lmatch debug t)) lfun lmatch + debug l | [] -> acc (* Interprets bindings for tactics *) -and bind_interp evc env lfun lmatch goalopt = function +and bind_interp (evc,env,lfun,lmatch,goalopt,debug) = function | Node(_,"BINDING", [Num(_,n);Node(loc,"COMMAND",[c])]) -> - (NoDep n,constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - (Node(loc,"COMMAND",[c]))))) + (NoDep n,constr_of_Constr (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt,debug) (Node(loc,"COMMAND",[c]))))) | Node(_,"BINDING", [Nvar(loc0,s); Node(loc1,"COMMAND",[c])]) -> - (Dep (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - (Nvar(loc0,s))))),constr_of_Constr (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt) (Node(loc1,"COMMAND",[c]))))) + (Dep (id_of_Identifier (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt,debug) + (Nvar(loc0,s))))),constr_of_Constr (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt,debug) (Node(loc1,"COMMAND",[c]))))) | Node(_,"BINDING", [Node(loc,"COMMAND",[c])]) -> - (Com,constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - (Node(loc,"COMMAND",[c]))))) + (Com,constr_of_Constr (unvarg + (val_interp (evc,env,lfun,lmatch,goalopt,debug) + (Node(loc,"COMMAND",[c]))))) | x -> errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding"; print_ast x>] (* Interprets a COMMAND expression (in case of failure, returns Command) *) -and com_interp (evc,env,lfun,lmatch,goalopt) = function +and com_interp (evc,env,lfun,lmatch,goalopt,debug) = function | Node(_,"EVAL",[c;rtc]) -> - let redexp = unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - rtc)) in + let redexp = unredexp (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt,debug) rtc)) in VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr_gen evc env (constr_list goalopt lfun) lmatch c None))) @@ -694,19 +768,18 @@ and com_interp (evc,env,lfun,lmatch,goalopt) = function errorlabstrm "com_interp" [<'sTR "Unbound context identifier"; print_ast ast>]) | c -> -(* try*) VArg (Constr (interp_constr_gen evc env (constr_list goalopt lfun) lmatch c None)) -(* with e when Logic.catchable_exception e -> VArg (Command c)*) (* Interprets a CASTEDCOMMAND expression *) -and cast_com_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with +and cast_com_interp (evc,env,lfun,lmatch,goalopt,debug) com = + match goalopt with | Some gl -> (match com with | Node(_,"EVAL",[c;rtc]) -> - let redexp = unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - rtc)) in + let redexp = unredexp (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt,debug) rtc)) in VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr_gen evc env (constr_list goalopt lfun) lmatch c (Some (pf_concl gl))))) | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast -> @@ -724,20 +797,19 @@ and cast_com_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with errorlabstrm "cast_com_interp" [<'sTR "Unbound context identifier"; print_ast ast>]) | c -> -(* try*) VArg (Constr (interp_constr_gen evc env (constr_list goalopt lfun) - lmatch c (Some (pf_concl gl)))) -(* with e when Logic.catchable_exception e -> VArg (Command c)*) ) + lmatch c (Some (pf_concl gl))))) | None -> errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">] (* Interprets a CASTEDOPENCOMMAND expression *) -and cast_opencom_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with +and cast_opencom_interp (evc,env,lfun,lmatch,goalopt,debug) com = + match goalopt with | Some gl -> (match com with | Node(_,"EVAL",[c;rtc]) -> - let redexp = unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - rtc)) in + let redexp = unredexp (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt,debug) rtc)) in VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr_gen evc env (constr_list goalopt lfun) lmatch c (Some (pf_concl gl))))) | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast -> @@ -755,37 +827,36 @@ and cast_opencom_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with errorlabstrm "cast_opencom_interp" [<'sTR "Unbound context identifier"; print_ast ast>]) | c -> -(* try*) VArg (OpenConstr (interp_openconstr_gen evc env (constr_list goalopt lfun) - lmatch c (Some (pf_concl gl)))) -(* with e when Logic.catchable_exception e -> VArg (Command c)*) ) + lmatch c (Some (pf_concl gl))))) | None -> errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">] -and cvt_pattern (evc,env,lfun,lmatch,goalopt) = function +and cvt_pattern (evc,env,lfun,lmatch,goalopt,debug) = function | Node(_,"PATTERN", Node(loc,"COMMAND",[com])::nums) -> let occs = List.map num_of_ast nums and csr = constr_of_Constr (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt) (Node(loc,"COMMAND",[com])))) in + (evc,env,lfun,lmatch,goalopt,debug) (Node(loc,"COMMAND",[com])))) in let jdt = Typing.unsafe_machine env evc csr in (occs, jdt.Environ.uj_val, body_of_type jdt.Environ.uj_type) | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern") -and cvt_unfold (evc,env,lfun,lmatch,goalopt) = function +and cvt_unfold (evc,env,lfun,lmatch,goalopt,debug) = function | Node(_,"UNFOLD", com::nums) -> (List.map num_of_ast nums,glob_nvar (id_of_Identifier (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt) com)))) + (evc,env,lfun,lmatch,goalopt,debug) com)))) | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold") (* Interprets the arguments of Fold *) -and cvt_fold (evc,env,lfun,lmatch,goalopt) = function +and cvt_fold (evc,env,lfun,lmatch,goalopt,debug) = function | Node(_,"COMMAND",[c]) as ast -> - constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) ast)) + constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug) + ast)) | arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold") (* Interprets the reduction flags *) -and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf = +and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf = let rec add_flag red = function | [] -> red | Node(_,"Beta",[])::lf -> add_flag (red_add red BETA) lf @@ -794,12 +865,12 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf = | Node(loc,"Unf",l)::lf -> let idl= List.map (fun v -> glob_nvar (id_of_Identifier (unvarg - (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l + (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l in add_flag (red_add red (CONST idl)) lf | Node(loc,"UnfBut",l)::lf -> let idl= List.map (fun v -> glob_nvar (id_of_Identifier (unvarg - (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l + (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l in add_flag (red_add red (CONSTBUT idl)) lf | _ -> add_flag (red_add red DELTA) lf) | Node(_,"Iota",[])::lf -> add_flag (red_add red IOTA) lf @@ -812,40 +883,47 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf = add_flag no_red lf; (* Interprets a reduction expression *) -and redexp_of_ast (evc,env,lfun,lmatch,goalopt) = function +and redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug) = function | ("Red", []) -> Red false | ("Hnf", []) -> Hnf | ("Simpl", []) -> Simpl | ("Unfold", ul) -> - Unfold (List.map (cvt_unfold (evc,env,lfun,lmatch,goalopt)) ul) - | ("Fold", cl) -> Fold (List.map (cvt_fold (evc,env,lfun,lmatch,goalopt)) cl) - | ("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf) - | ("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf) + Unfold (List.map (cvt_unfold (evc,env,lfun,lmatch,goalopt,debug)) ul) + | ("Fold", cl) -> + Fold (List.map (cvt_fold (evc,env,lfun,lmatch,goalopt,debug)) cl) + | ("Cbv",lf) -> + Cbv(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf) + | ("Lazy",lf) -> + Lazy(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf) | ("Pattern",lp) -> - Pattern (List.map (cvt_pattern (evc,env,lfun,lmatch,goalopt)) lp) + Pattern (List.map (cvt_pattern (evc,env,lfun,lmatch,goalopt,debug)) lp) | (s,_) -> invalid_arg ("malformed reduction-expression: "^s) (* Interprets the patterns of Intro *) -and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt) = function +and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug) = function | Node(_,"IDENTIFIER", [Nvar(loc,s)]) -> - IdPat (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - (Nvar (loc,s))))) + IdPat (id_of_Identifier (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt,debug) (Nvar (loc,s))))) | Node(_,"DISJPATTERN", l) -> - DisjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) + DisjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug)) + l) | Node(_,"CONJPATTERN", l) -> - ConjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) + ConjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug)) + l) | Node(_,"LISTPATTERN", l) -> - ListPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l) + ListPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug)) + l) | x -> errorlabstrm "cvt_intro_pattern" [<'sTR "Not the expected form for an introduction pattern!"; print_ast x>] (* Interprets a pattern of Let *) -and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l) = function +and cvt_letpattern (evc,env,lfun,lmatch,goalopt,debug) (o,l) = function | Node(_,"HYPPATTERN", Nvar(loc,s)::nums) -> - (o,(id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) - (Nvar (loc,s)))),List.map num_of_ast nums)::l) + (o,(id_of_Identifier (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt,debug) + (Nvar (loc,s)))),List.map num_of_ast nums)::l) | Node(_,"CCLPATTERN", nums) -> if o <> None then error "\"Goal\" occurs twice" @@ -857,7 +935,7 @@ and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l) = function let interp_tacarg sign ast = unvarg (val_interp sign ast) (* Initial call for interpretation *) -let interp = tac_interp [] [] +let interp = fun ast -> tac_interp [] [] !debug ast let is_just_undef_macro ast = match ast with diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 746c89f08..ee5d67966 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -2,10 +2,12 @@ (* $Id$ *) (*i*) +open Dyn open Pp open Names open Proof_type open Tacmach +open Tactic_debug open Term (*i*) @@ -25,7 +27,26 @@ val constr_of_Constr : tactic_arg -> constr (* Signature for interpretation: [val_interp] and interpretation functions *) type interp_sign = enamed_declarations * Environ.env * (string * value) list * - (int * constr) list * goal sigma option + (int * constr) list * goal sigma option * debug_info + +(* To provide the tactic expressions *) +val loc : Coqast.loc +val tacticIn : (unit -> Coqast.t) -> Coqast.t + +(* References for dynamic interpretation of user tactics. They are all + initialized with dummy values *) +val r_evc : enamed_declarations ref +val r_env : Environ.env ref +val r_lfun : (string * value) list ref +val r_lmatch : (int * constr) list ref +val r_goalopt : goal sigma option ref +val r_debug : debug_info ref + +(* Sets the debugger mode *) +val set_debug : debug_info -> unit + +(* Gives the state of debug *) +val get_debug : unit -> debug_info (* Adds a Tactic Definition in the table *) val add_tacdef : string -> value -> unit diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml new file mode 100644 index 000000000..d9c5d528a --- /dev/null +++ b/proofs/tactic_debug.ml @@ -0,0 +1,47 @@ +open Ast +open Pp +open Printer + +(* This module intends to be a beginning of debugger for tactic expressions. + Currently, it is quite simple and we can hope to have, in the future, a more + complete panel of commands dedicated to a proof assistant framework *) + +(* Debug information *) +type debug_info = + | DebugOn + | DebugOff + | Exit + +(* Prints the goal if it exists *) +let db_pr_goal = function + | None -> mSGNL [< 'sTR "No goal" >] + | Some g -> + mSGNL [<'sTR ("Goal:"); 'fNL; Proof_trees.pr_goal (Tacmach.sig_it g) >] + +(* Prints the state and waits for an instruction *) +let debug_prompt goalopt tac_ast = + db_pr_goal goalopt; + mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL; 'fNL; + 'sTR "----<Enter>=Continue----s=Skip----x=Exit----" >]; + let rec prompt () = + mSG [<'fNL; 'sTR "TcDebug> " >]; + flush stdout; + let inst = read_line () in + mSGNL [<>]; + match inst with + | "" -> DebugOn + | "s" -> DebugOff + | "x" -> Exit + | _ -> prompt () in + prompt () + +(* Prints a matched hypothesis *) +let db_matched_hyp debug env (id,c) = + if debug = DebugOn then + mSGNL [< 'sTR "Matched hypothesis --> "; 'sTR (id^": "); + prterm_env env c >] + +(* Prints the matched conclusion *) +let db_matched_concl debug env c = + if debug = DebugOn then + mSGNL [< 'sTR "Matched goal --> "; prterm_env env c >] diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli new file mode 100644 index 000000000..26ab1a947 --- /dev/null +++ b/proofs/tactic_debug.mli @@ -0,0 +1,21 @@ +open Proof_type +open Term + +(* This module intends to be a beginning of debugger for tactic expressions. + Currently, it is quite simple and we can hope to have, in the future, a more + complete panel of commands dedicated to a proof assistant framework *) + +(* Debug information *) +type debug_info = + | DebugOn + | DebugOff + | Exit + +(* Prints the state and waits *) +val debug_prompt : goal sigma option -> Coqast.t -> debug_info + +(* Prints a matched hypothesis *) +val db_matched_hyp : debug_info -> Environ.env -> string * constr -> unit + +(* Prints the matched conclusion *) +val db_matched_concl : debug_info -> Environ.env -> constr -> unit |