diff options
| -rw-r--r-- | dev/include | 4 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 58 | ||||
| -rw-r--r-- | proofs/tacinterp.mli | 13 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 44 |
5 files changed, 54 insertions, 67 deletions
diff --git a/dev/include b/dev/include index 2a841e458..ce923477b 100644 --- a/dev/include +++ b/dev/include @@ -24,4 +24,6 @@ #install_printer (* readable_constraints *) prevc;; #install_printer (* walking_constraints *) prwc;; #install_printer (* clenv *) prclenv;; -#install_printer (* env *) ppenv;;
\ No newline at end of file +#install_printer (* env *) ppenv;; + +#install_printer (* tactic *) pptac;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 71347c695..51334029e 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -79,6 +79,8 @@ let pp_universes u = pP [< 'sTR"[" ; pr_universes u ; 'sTR"]" >] let ppenv e = pP (pr_rel_context e (rel_context e)) +let pptac = (fun x -> pP(gentacpr x)) + let cnt = ref 0 let constr_display csr = diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index a68566d72..05d7df746 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -41,7 +41,7 @@ type value = | VTactic of tactic | VFTactic of tactic_arg list * (tactic_arg list->tactic) | VRTactic of (goal list sigma * validation) - | VContext of (goal sigma -> value) + | VContext of (interp_sign -> goal sigma -> value) | VArg of tactic_arg | VFun of (identifier * value) list * identifier option list * Coqast.t | VVoid @@ -146,31 +146,16 @@ let interp_openconstr ist c ocl = (constr_list ist.goalopt ist.lfun) ist.lmatch c ocl (* For user tactics *) -let ((ocamlIn : (unit -> Coqast.t) -> Dyn.t), - (ocamlOut : Dyn.t -> (unit -> Coqast.t))) = create "ocaml" +(*let ((ocamlIn : (unit -> Coqast.t) -> Dyn.t), + (ocamlOut : Dyn.t -> (unit -> Coqast.t))) = create "ocaml"*) + +let ((ocamlIn : (interp_sign -> Coqast.t) -> Dyn.t), + (ocamlOut : Dyn.t -> (interp_sign -> 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 ist = - r_evc := ist.evc; - r_env := ist.env; - r_lfun := ist.lfun; - r_lmatch := ist.lmatch; - r_goalopt := ist.goalopt; - r_debug := ist.debug - (* Table of interpretation functions *) let interp_tab = (Hashtbl.create 17 : (string , interp_sign -> Coqast.t -> value) Hashtbl.t) @@ -510,7 +495,7 @@ let rec val_interp ist ast = | Nvar(_,s) -> (try (unrec (List.assoc s ist.lfun)) with | Not_found -> - (try (vcontext_interp ist.goalopt (lookup s)) + (try (vcontext_interp ist (lookup s)) with | Not_found -> VArg (Identifier s))) | Node(_,"QUALIDARG",[Nvar(_,s)]) -> (try (make_qid (unrec (List.assoc s ist.lfun))) @@ -547,13 +532,15 @@ let rec val_interp ist ast = with Not_found -> val_interp ist (Node(dummy_loc,"APPTACTIC",[ast]))) - | Dynamic(_,t) -> - env_update ist; - let f = (ocamlOut t) in - Obj.magic (val_interp ist (f ())) + | Dynamic(_,t) -> + if (tag t) = "ocaml" then + let f = (ocamlOut t) in val_interp ist (f ist) + else + anomaly_loc (Ast.loc ast, "Tacinterp.val_interp", + [<'sTR "Unknown dynamic ast: "; print_ast ast>]) | _ -> anomaly_loc (Ast.loc ast, "Tacinterp.val_interp", - [<'sTR "Unrecognizable ast: "; print_ast ast>]) in + [<'sTR "Unrecognizable ast: "; print_ast ast>]) in if ist.debug = DebugOn then match debug_prompt ist.goalopt ast with | Exit -> VTactic tclIDTAC @@ -772,12 +759,17 @@ and match_context_interp ist ast lmr = errorlabstrm "Tacinterp.apply_match_context" [<'sTR "No matching clauses for Match Context">] in let app_wo_goal = - (fun goal -> + (fun ist goal -> + apply_match_context ist goal + (read_match_context_rule ist.evc ist.env + (constr_list ist.goalopt ist.lfun) lmr)) in + +(* (fun goal -> let evc = project goal and env = pf_env goal in apply_match_context ist goal (read_match_context_rule ist.evc ist.env - (constr_list ist.goalopt ist.lfun) lmr)) in + (constr_list ist.goalopt ist.lfun) lmr)) in*) (* (fun ist goal -> apply_match_context ist goal @@ -785,7 +777,7 @@ and match_context_interp ist ast lmr = (match ist.goalopt with | None -> VContext app_wo_goal - | Some g -> app_wo_goal g) + | Some g -> app_wo_goal ist g) (* apply_match_context evc env lfun lmatch goal (read_match_context_rule evc env (constr_list goalopt lfun) lmr)*) @@ -831,11 +823,11 @@ and apply_hyps_context ist mt lgmatch mhyps hyps = apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None (* Interprets a VContext value *) -and vcontext_interp goalopt = function +and vcontext_interp ist = function | (VContext f) as v -> - (match goalopt with + (match ist.goalopt with | None -> v - | Some g -> f g) + | Some g -> f ist g) | v -> v (* Interprets the Match expressions *) diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 41b105f7b..85dc1e2fb 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -23,7 +23,7 @@ type value = | VTactic of tactic | VFTactic of tactic_arg list * (tactic_arg list -> tactic) | VRTactic of (goal list sigma * validation) - | VContext of (goal sigma -> value) + | VContext of (interp_sign -> goal sigma -> value) | VArg of tactic_arg | VFun of (identifier * value) list * identifier option list * Coqast.t | VVoid @@ -43,16 +43,7 @@ val constr_of_Constr : tactic_arg -> constr (* 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 : (identifier * value) list ref -val r_lmatch : (int * constr) list ref -val r_goalopt : goal sigma option ref -val r_debug : debug_info ref +val tacticIn : (interp_sign -> Coqast.t) -> Coqast.t (* Sets the debugger mode *) val set_debug : debug_info -> unit diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 599644927..ab96c8759 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -21,41 +21,41 @@ open Tacinterp open Tactics open Util -let is_empty () = - if (is_empty_type (List.assoc 1 !r_lmatch)) then +let is_empty ist = + if (is_empty_type (List.assoc 1 ist.lmatch)) then <:tactic<ElimType ?1;Assumption>> else failwith "is_empty" -let is_unit () = - if (is_unit_type (List.assoc 1 !r_lmatch)) then +let is_unit ist = + if (is_unit_type (List.assoc 1 ist.lmatch)) then <:tactic<Idtac>> else failwith "is_unit" -let is_conj () = - if (is_conjunction (List.assoc 1 !r_lmatch)) then +let is_conj ist = + if (is_conjunction (List.assoc 1 ist.lmatch)) then <:tactic<Idtac>> else failwith "is_conj" -let is_disj () = - if (is_disjunction (List.assoc 1 !r_lmatch)) then +let is_disj ist = + if (is_disjunction (List.assoc 1 ist.lmatch)) then <:tactic<Idtac>> else failwith "is_disj" -let not_dep_intros () = +let not_dep_intros ist = <:tactic< Repeat Match Context With | [|- ?1 -> ?2 ] -> Intro>> -let init_intros () = - (tclORELSE (tclTHEN (intros_until_n_wored 1) (interp (not_dep_intros ()))) - intros) +let init_intros = + (tclORELSE (tclTHEN (intros_until_n_wored 1) + (interp (tacticIn not_dep_intros))) intros) -let axioms () = +let axioms ist = let t_is_unit = tacticIn is_unit and t_is_empty = tacticIn is_empty in <:tactic< @@ -64,7 +64,7 @@ let axioms () = |[ _:?1 |- ?] -> $t_is_empty |[ _:?1 |- ?1] -> Assumption>> -let simplif () = +let simplif ist = let t_is_unit = tacticIn is_unit and t_is_conj = tacticIn is_conj and t_is_disj = tacticIn is_disj @@ -86,7 +86,7 @@ let simplif () = $t_is_unit;Cut ?2;[Intro;Clear id|Intros;Apply id;Constructor;Fail] | [|- (?1 ? ?)] -> $t_is_conj;Split);$t_not_dep_intros)>> -let rec tauto_main () = +let rec tauto_main ist = let t_axioms = tacticIn axioms and t_simplif = tacticIn simplif and t_is_disj = tacticIn is_disj @@ -104,7 +104,7 @@ let rec tauto_main () = Orelse (Intro;$t_tauto_main)>> -let rec intuition_main () = +let rec intuition_main ist = let t_axioms = tacticIn axioms and t_simplif = tacticIn simplif and t_intuition_main = tacticIn intuition_main in @@ -133,17 +133,17 @@ let reduction = Tacticals.onAllClauses (fun ido -> compute ido) let tauto g = try - (tclTHEN (init_intros ()) + (tclTHEN init_intros (tclORELSE - (tclTHEN reduction_not_iff (interp (tauto_main ()))) - (tclTHEN reduction (interp (tauto_main ()))))) g + (tclTHEN reduction_not_iff (interp (tacticIn tauto_main))) + (tclTHEN reduction (interp (tacticIn tauto_main))))) g with UserError _ -> errorlabstrm "tauto" [< 'sTR "Tauto failed" >] let intuition = - tclTHEN (init_intros ()) + tclTHEN init_intros (tclORELSE - (tclTHEN reduction_not_iff (interp (intuition_main ()))) - (tclTHEN reduction (interp (intuition_main ())))) + (tclTHEN reduction_not_iff (interp (tacticIn intuition_main))) + (tclTHEN reduction (interp (tacticIn intuition_main)))) let _ = hide_atomic_tactic "Tauto" tauto let _ = hide_atomic_tactic "Intuition" intuition |