From: Claudio Sacerdoti Coen Date: Tue, 3 Dec 2002 17:47:30 +0000 (+0000) Subject: Typing of intros_tac improved. It now has a parameter that is a fresh-names X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9597e7e79ce0606671f8aa170951d119419780ad;p=helm.git Typing of intros_tac improved. It now has a parameter that is a fresh-names generator. --- diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 07a94a9b1..c08183beb 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -1002,7 +1002,9 @@ let assumption_tac ~status:(proof,goal)= (* !!!!! fix !!!!!!!!!! *) let contradiction_tac ~status:(proof,goal)= Tacticals.then_ - ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*) + (*inutile sia questo che quello prima della chiamata*) + ~start: + (PrimitiveTactics.intros_tac ~mknames:(function () -> "boh")) ~continuation:(Tacticals.then_ ~start:(VariousTactics.elim_type_tac ~term:_False) ~continuation:(assumption_tac)) @@ -1044,7 +1046,8 @@ theoreme,so let's parse our thesis *) let proof,gl = Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) - ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp) + ~continuation: + (PrimitiveTactics.intros_tac ~mknames:(function () -> fhyp)) ~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 8b3f025aa..eba2d571f 100644 --- a/helm/gTopLevel/primitiveTactics.ml +++ b/helm/gTopLevel/primitiveTactics.ml @@ -37,7 +37,7 @@ exception WrongUriToVariable of string (* and [bo] = Lambda/LetIn [context].(Meta [newmeta]) *) (* So, lambda_abstract is the core of the implementation of *) (* the Intros tactic. *) -let lambda_abstract context newmeta ty name = +let lambda_abstract context newmeta ty mknames = let module C = Cic in let rec collect_context context = function @@ -46,8 +46,7 @@ let lambda_abstract context newmeta ty name = let n' = match n with C.Name _ -> n -(*CSC: generatore di nomi? Chiedere il nome? *) - | C.Anonymous -> C.Name name + | C.Anonymous -> C.Name (mknames ()) in let (context',ty,bo) = collect_context ((Some (n',(C.Decl s)))::context) t @@ -306,13 +305,13 @@ let apply_tac ~term ~status = with CicUnification.UnificationFailed as e -> raise (Fail (Printexc.to_string e)) -let intros_tac ~name ~status:(proof, goal) = +let intros_tac ~mknames ~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 name in + let (context',ty',bo') = lambda_abstract context newmeta ty mknames in let (newproof, _) = subst_meta_in_proof proof metano bo' [newmeta,context',ty'] in @@ -508,7 +507,7 @@ let elim_simpl_intros_tac ~term = ~continuation: (Tacticals.then_ ~start:(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) - ~continuation:(intros_tac ~name:"FOO")) + ~continuation:(intros_tac ~mknames:(function () -> "FOO"))) ;; diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli index b23e4005f..1fa97805a 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: - name: string -> ProofEngineTypes.tactic + mknames: (unit -> string) -> 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 dbf04c393..173c1c59d 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -138,11 +138,10 @@ let perforate context term ty = (*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 + 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 = @@ -174,7 +173,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 ~name:(fresh_name ())) + apply_tactic (PrimitiveTactics.intros_tac ~mknames:fresh_name) 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/variousTactics.ml b/helm/gTopLevel/variousTactics.ml index 35122025c..95b74ab99 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 ~name:"FOO") + ~start: (P.intros_tac ~mknames:(function () -> "FOO")) ~continuation:( T.then_ ~start: (elim_type_tac ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )) @@ -495,7 +495,8 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) = (* quale uguaglianza usare, eq o eqT ? *) ~continuations:[ T.then_ - ~start:(P.intros_tac ~name:"dummy_for_replace") + ~start: + (P.intros_tac ~mknames:(function () ->"dummy_for_replace")) ~continuation:(T.then_ ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *) ~continuation:(ProofEngineStructuralRules.clear