From b896cfcc6ed52bec8519694e0f0428c5266cb6b0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 6 Dec 2002 13:36:07 +0000 Subject: [PATCH] The fresh_name generator has been moved to ProofEngineHelpers. intros_tac now directly uses it ==> no more ~mkname arguments. The generator has been "improved" so that it does not generate any more two equal names. The drawback is that every identifier is augmented with a nonce. --- helm/gTopLevel/fourierR.ml | 13 ++++++------- helm/gTopLevel/primitiveTactics.ml | 14 ++++++-------- helm/gTopLevel/primitiveTactics.mli | 2 +- helm/gTopLevel/proofEngine.ml | 10 +--------- helm/gTopLevel/proofEngineHelpers.ml | 11 +++++++++++ helm/gTopLevel/proofEngineHelpers.mli | 2 ++ helm/gTopLevel/variousTactics.ml | 5 ++--- 7 files changed, 29 insertions(+), 28 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 9076ae70f..bb1c2febf 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -1004,8 +1004,7 @@ let assumption_tac ~status:(proof,goal)= let contradiction_tac ~status:(proof,goal)= Tacticals.then_ (*inutile sia questo che quello prima della chiamata*) - ~start: - (PrimitiveTactics.intros_tac ~mknames:(function () -> "boh")) + ~start:PrimitiveTactics.intros_tac ~continuation:(Tacticals.then_ ~start:(VariousTactics.elim_type_tac ~term:_False) ~continuation:(assumption_tac)) @@ -1045,11 +1044,11 @@ theoreme,so let's parse our thesis *) (* now let's change our thesis applying the th and put it with hp *) - let proof,gl = Tacticals.then_ - ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) - ~continuation: - (PrimitiveTactics.intros_tac ~mknames:(function () -> fhyp)) - ~status:(s_proof,s_goal) in + let proof,gl = + Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) + ~continuation:PrimitiveTactics.intros_tac + ~status:(s_proof,s_goal) in let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml index eba2d571f..9a037d754 100644 --- a/helm/gTopLevel/primitiveTactics.ml +++ b/helm/gTopLevel/primitiveTactics.ml @@ -43,11 +43,7 @@ let lambda_abstract context newmeta ty mknames = function C.Cast (te,_) -> collect_context context te | C.Prod (n,s,t) -> - let n' = - match n with - C.Name _ -> n - | C.Anonymous -> C.Name (mknames ()) - in + let n' = C.Name (mknames n) in let (context',ty,bo) = collect_context ((Some (n',(C.Decl s)))::context) t in @@ -305,13 +301,15 @@ let apply_tac ~term ~status = with CicUnification.UnificationFailed as e -> raise (Fail (Printexc.to_string e)) -let intros_tac ~mknames ~status:(proof, goal) = +let intros_tac ~status:(proof, goal) = let module C = Cic in let module R = CicReduction in let (_,metasenv,_,_) = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let newmeta = new_meta ~proof in - let (context',ty',bo') = lambda_abstract context newmeta ty mknames in + let (context',ty',bo') = + lambda_abstract context newmeta ty (ProofEngineHelpers.fresh_name) + in let (newproof, _) = subst_meta_in_proof proof metano bo' [newmeta,context',ty'] in @@ -507,7 +505,7 @@ let elim_simpl_intros_tac ~term = ~continuation: (Tacticals.then_ ~start:(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) - ~continuation:(intros_tac ~mknames:(function () -> "FOO"))) + ~continuation:intros_tac) ;; diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli index 1fa97805a..59a714c78 100644 --- a/helm/gTopLevel/primitiveTactics.mli +++ b/helm/gTopLevel/primitiveTactics.mli @@ -28,7 +28,7 @@ val apply_tac: val exact_tac: term: Cic.term -> ProofEngineTypes.tactic val intros_tac: - mknames: (unit -> string) -> ProofEngineTypes.tactic + ProofEngineTypes.tactic val cut_tac: term: Cic.term -> ProofEngineTypes.tactic val letin_tac: diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 73e2aa177..7b4c68ab5 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -136,13 +136,6 @@ let perforate context term ty = (* Some easy tactics. *) (************************************************************) -(*CSC: generatore di nomi? Chiedere il nome? *) -let fresh_name = - let next_fresh_index = ref 0 in - function () -> - incr next_fresh_index ; - "fresh_name" ^ string_of_int !next_fresh_index - (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *) let reduction_tactic_in_scratch reduction_function term ty = let metasenv = @@ -172,8 +165,7 @@ let simpl_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.simpl let can_apply term = can_apply_tactic (PrimitiveTactics.apply_tac ~term) let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term) -let intros () = - apply_tactic (PrimitiveTactics.intros_tac ~mknames:fresh_name) +let intros () = apply_tactic PrimitiveTactics.intros_tac let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term) let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term) let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term) diff --git a/helm/gTopLevel/proofEngineHelpers.ml b/helm/gTopLevel/proofEngineHelpers.ml index d191340ea..74b6fcdac 100644 --- a/helm/gTopLevel/proofEngineHelpers.ml +++ b/helm/gTopLevel/proofEngineHelpers.ml @@ -23,6 +23,17 @@ * http://cs.unibo.it/helm/. *) +(*CSC: generatore di nomi? Chiedere il nome? *) +let fresh_name = + let next_fresh_index = ref 0 in + function + Cic.Anonymous -> + incr next_fresh_index ; + "fresh_name" ^ string_of_int !next_fresh_index + | Cic.Name name -> + incr next_fresh_index ; + name ^ string_of_int !next_fresh_index + (* identity_relocation_list_for_metavariable i canonical_context *) (* returns the identity relocation list, which is the list [1 ; ... ; n] *) (* where n = List.length [canonical_context] *) diff --git a/helm/gTopLevel/proofEngineHelpers.mli b/helm/gTopLevel/proofEngineHelpers.mli index c5593235c..de0b37596 100644 --- a/helm/gTopLevel/proofEngineHelpers.mli +++ b/helm/gTopLevel/proofEngineHelpers.mli @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +val fresh_name : Cic.name -> string + (* identity_relocation_list_for_metavariable i canonical_context *) (* returns the identity relocation list, which is the list [1 ; ... ; n] *) (* where n = List.length [canonical_context] *) diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml index 95b74ab99..fc6897baf 100644 --- a/helm/gTopLevel/variousTactics.ml +++ b/helm/gTopLevel/variousTactics.ml @@ -189,7 +189,7 @@ let contradiction_tac ~status = let module P = PrimitiveTactics in let module T = Tacticals in T.then_ - ~start: (P.intros_tac ~mknames:(function () -> "FOO")) + ~start:P.intros_tac ~continuation:( T.then_ ~start: (elim_type_tac ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )) @@ -495,8 +495,7 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) = (* quale uguaglianza usare, eq o eqT ? *) ~continuations:[ T.then_ - ~start: - (P.intros_tac ~mknames:(function () ->"dummy_for_replace")) + ~start:P.intros_tac ~continuation:(T.then_ ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *) ~continuation:(ProofEngineStructuralRules.clear -- 2.39.2