From 898a2c9e9c11d5455e9b27069327530db568570d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jan 2003 10:19:55 +0000 Subject: [PATCH] Optional callbacks have been added to tactics that need to introduce new fresh names directly (i.e. without calling other tactics that need fresh names). The default behaviour is _MUCH_ nicer than the previous dummy one and is fully functional. Corollary 1: all the code of tactics.cma is now reentrant. Corollary 2: the user can be asked the fresh name if it is requested by a top-level tactic. --- helm/gTopLevel/gTopLevel.ml | 27 +++++++++++-- helm/gTopLevel/proofEngine.ml | 11 ++++-- helm/gTopLevel/proofEngine.mli | 9 +++-- helm/ocaml/tactics/eliminationTactics.ml | 6 ++- helm/ocaml/tactics/eliminationTactics.mli | 7 ++-- helm/ocaml/tactics/equalityTactics.ml | 11 +++--- helm/ocaml/tactics/fourierR.ml | 2 +- helm/ocaml/tactics/negationTactics.ml | 2 +- helm/ocaml/tactics/primitiveTactics.ml | 40 +++++++++++++------ helm/ocaml/tactics/primitiveTactics.mli | 9 +++-- helm/ocaml/tactics/proofEngineHelpers.ml | 47 ++++++++++++++++++----- helm/ocaml/tactics/proofEngineHelpers.mli | 6 ++- helm/ocaml/tactics/proofEngineTypes.ml | 3 ++ helm/ocaml/tactics/variousTactics.ml | 30 +++++++-------- 14 files changed, 145 insertions(+), 65 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 396c968fd..a94472bf2 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1658,6 +1658,22 @@ let new_inductive () = ("

" ^ Printexc.to_string e ^ "

") ; ;; +let mk_fresh_name_callback context name ~typ = + let fresh_name = + match ProofEngineHelpers.mk_fresh_name context name ~typ with + Cic.Name fresh_name -> fresh_name + | Cic.Anonymous -> assert false + in + match + GToolbox.input_string ~title:"Enter a fresh hypothesis name" ~text:fresh_name + ("Enter a fresh name for the hypothesis " ^ + CicPp.pp typ + (List.map (function None -> None | Some (n,_) -> Some n) context)) + with + Some fresh_name' -> Cic.Name fresh_name' + | None -> raise NoChoice +;; + let new_proof () = let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in @@ -1758,7 +1774,10 @@ let new_proof () = refresh_sequent notebook ; refresh_proof output ; !save_set_sensitive true ; - inputt#reset + inputt#reset ; + ProofEngine.intros ~mk_fresh_name_callback () ; + refresh_sequent notebook ; + refresh_proof output with RefreshSequentException e -> output_html outputhtml @@ -2138,7 +2157,7 @@ let call_tactic_with_hypothesis_input tactic () = ;; -let intros = call_tactic ProofEngine.intros;; +let intros = call_tactic (ProofEngine.intros ~mk_fresh_name_callback);; let exact = call_tactic_with_input ProofEngine.exact;; let apply = call_tactic_with_input ProofEngine.apply;; let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;; @@ -2149,9 +2168,9 @@ let simpl = call_tactic_with_goal_input ProofEngine.simpl;; let fold_whd = call_tactic_with_input ProofEngine.fold_whd;; let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;; let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;; -let cut = call_tactic_with_input ProofEngine.cut;; +let cut = call_tactic_with_input (ProofEngine.cut ~mk_fresh_name_callback);; let change = call_tactic_with_input_and_goal_input ProofEngine.change;; -let letin = call_tactic_with_input ProofEngine.letin;; +let letin = call_tactic_with_input (ProofEngine.letin ~mk_fresh_name_callback);; let ring = call_tactic ProofEngine.ring;; let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;; let clear = call_tactic_with_hypothesis_input ProofEngine.clear;; diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index e333ec3b8..99e6a081c 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -165,9 +165,12 @@ 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 -let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term) -let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term) +let intros ?mk_fresh_name_callback () = + apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ()) +let cut ?mk_fresh_name_callback term = + apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback term) +let letin ?mk_fresh_name_callback term = + apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback term) let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term) let elim_intros_simpl term = apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term) @@ -232,7 +235,7 @@ let absurd term = apply_tactic (NegationTactics.absurd_tac ~term) let contradiction () = apply_tactic NegationTactics.contradiction_tac let decompose ~uris_choice_callback term = - apply_tactic (EliminationTactics.decompose_tac ~term ~uris_choice_callback) + apply_tactic (EliminationTactics.decompose_tac ~uris_choice_callback term) (* let decide_equality () = apply_tactic VariousTactics.decide_equality_tac diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index deb8483ac..c845c2b1e 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -46,9 +46,12 @@ val simpl_in_scratch : Cic.term -> Cic.term -> Cic.term (* "primitive" tactics *) val can_apply : Cic.term -> bool val apply : Cic.term -> unit -val intros : unit -> unit -val cut : Cic.term -> unit -val letin : Cic.term -> unit +val intros : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit -> unit +val cut : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> unit +val letin : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> unit val exact : Cic.term -> unit val elim_intros_simpl : Cic.term -> unit val change : goal_input:Cic.term -> input:Cic.term -> unit diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index ae947f5ec..73d1771ff 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -49,7 +49,7 @@ let elim_type_tac ~term ~status = let module P = PrimitiveTactics in let module T = Tacticals in T.thens - ~start: (P.cut_tac ~term) + ~start: (P.cut_tac term) ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ] ~status ;; @@ -96,7 +96,9 @@ let cic_textual_parser_uri_of_string uri' = _ -> raise (IllFormedUri uri') ;; -let decompose_tac ~term ~uris_choice_callback ~status:((proof,goal) as status) = +let decompose_tac ?(uris_choice_callback=(function l -> l)) term + ~status:((proof,goal) as status) += let module C = Cic in let module R = CicReduction in let module P = PrimitiveTactics in diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli index 5e132c496..92d9eee01 100644 --- a/helm/ocaml/tactics/eliminationTactics.mli +++ b/helm/ocaml/tactics/eliminationTactics.mli @@ -25,9 +25,10 @@ val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic +(* The default callback always decomposes the term as much as possible *) val decompose_tac: - term:Cic.term -> - uris_choice_callback: + ?uris_choice_callback: ((UriManager.uri * int * (UriManager.uri * Cic.term) list) list -> (UriManager.uri * int * (UriManager.uri * Cic.term) list) list) -> - ProofEngineTypes.tactic + Cic.term -> + ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 79b5b1dbe..29df82c08 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -162,12 +162,11 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) = then T.thens ~start:( P.cut_tac - ~term:( - C.Appl [ - (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; (* quale uguaglianza usare, eq o eqT ? *) - wty ; - what ; - with_what])) + (C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; (* quale uguaglianza usare, eq o eqT ? *) + wty ; + what ; + with_what])) ~continuations:[ T.then_ ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *) diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index 370b5db50..bd4eeae3e 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -1049,7 +1049,7 @@ theoreme,so let's parse our thesis *) let proof,gl = Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) - ~continuation:PrimitiveTactics.intros_tac + ~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/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml index 28e5ceeb5..25c29918f 100644 --- a/helm/ocaml/tactics/negationTactics.ml +++ b/helm/ocaml/tactics/negationTactics.ml @@ -44,7 +44,7 @@ let contradiction_tac ~status = let module T = Tacticals in try T.then_ - ~start: P.intros_tac + ~start:(P.intros_tac ()) ~continuation:( T.then_ ~start: diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index ccd8ccfe0..8abaae1b8 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -37,13 +37,13 @@ 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 mknames = +let lambda_abstract context newmeta ty mk_fresh_name = let module C = Cic in let rec collect_context context = function C.Cast (te,_) -> collect_context context te | C.Prod (n,s,t) -> - let n' = C.Name (mknames n) in + let n' = mk_fresh_name context n ~typ:s in let (context',ty,bo) = collect_context ((Some (n',(C.Decl s)))::context) t in @@ -112,7 +112,10 @@ let eta_expand metasenv context t arg = let argty = T.type_of_aux' metasenv context arg in - (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg]) + let fresh_name = + ProofEngineHelpers.mk_fresh_name context (Cic.Name "Heta") ~typ:argty + in + (C.Appl [C.Lambda (fresh_name,argty,aux 0 t) ; arg]) (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *) let classify_metas newmeta in_subst_domain subst_in metasenv = @@ -301,35 +304,43 @@ let apply_tac ~term ~status = with CicUnification.UnificationFailed as e -> raise (Fail (Printexc.to_string e)) -let intros_tac ~status:(proof, goal) = +let intros_tac + ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name) () + ~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 (ProofEngineHelpers.fresh_name) + lambda_abstract context newmeta ty mk_fresh_name_callback in let (newproof, _) = subst_meta_in_proof proof metano bo' [newmeta,context',ty'] in (newproof, [newmeta]) -let cut_tac ~term ~status:(proof, goal) = +let cut_tac + ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name) + term ~status:(proof, goal) += let module C = Cic in let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let newmeta1 = new_meta ~proof in let newmeta2 = newmeta1 + 1 in + let fresh_name = + mk_fresh_name_callback context (Cic.Name "Hcut") ~typ:term in let context_for_newmeta1 = - (Some (C.Name "dummy_for_cut",C.Decl term))::context in + (Some (fresh_name,C.Decl term))::context in let irl1 = identity_relocation_list_for_metavariable context_for_newmeta1 in let irl2 = identity_relocation_list_for_metavariable context in let newmeta1ty = CicSubstitution.lift 1 ty in let bo' = C.Appl - [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ; + [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ; C.Meta (newmeta2,irl2)] in let (newproof, _) = @@ -338,18 +349,23 @@ let cut_tac ~term ~status:(proof, goal) = in (newproof, [newmeta1 ; newmeta2]) -let letin_tac ~term ~status:(proof, goal) = +let letin_tac + ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name) + term ~status:(proof, goal) += let module C = Cic in let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let _ = CicTypeChecker.type_of_aux' metasenv context term in let newmeta = new_meta ~proof in + let fresh_name = + mk_fresh_name_callback context (Cic.Name "Hletin") ~typ:term in let context_for_newmeta = - (Some (C.Name "dummy_for_letin",C.Def term))::context in + (Some (fresh_name,C.Def term))::context in let irl = identity_relocation_list_for_metavariable context_for_newmeta in let newmetaty = CicSubstitution.lift 1 ty in - let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta (newmeta,irl)) in + let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in let (newproof, _) = subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] @@ -505,7 +521,7 @@ let elim_intros_simpl_tac ~term = Tacticals.then_ ~start:(elim_tac ~term) ~continuation: (Tacticals.thens - ~start:intros_tac + ~start:(intros_tac ()) ~continuations: [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None]) ;; diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli index dad385339..bef3bb2e8 100644 --- a/helm/ocaml/tactics/primitiveTactics.mli +++ b/helm/ocaml/tactics/primitiveTactics.mli @@ -28,11 +28,14 @@ val apply_tac: val exact_tac: term: Cic.term -> ProofEngineTypes.tactic val intros_tac: - ProofEngineTypes.tactic + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit -> + ProofEngineTypes.tactic val cut_tac: - term: Cic.term -> ProofEngineTypes.tactic + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> + ProofEngineTypes.tactic val letin_tac: - term: Cic.term -> ProofEngineTypes.tactic + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> + ProofEngineTypes.tactic val elim_intros_simpl_tac: term: Cic.term -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 74b6fcdac..84eaa2559 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -23,16 +23,43 @@ * 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 +(* mk_fresh_name context name typ *) +(* returns an identifier which is fresh in the context *) +(* and that resembles [name] as much as possible. *) +(* [typ] will be the type of the variable *) +let mk_fresh_name context name ~typ = + let module C = Cic in + let basename = + match name with + C.Anonymous -> + (*CSC: great space for improvements here *) + (try + (match CicTypeChecker.type_of_aux' [] context typ with + C.Sort C.Prop -> "H" + | C.Sort C.Set -> "x" + | _ -> "H" + ) + with _ -> + "H" + ) + | C.Name name -> + Str.global_replace (Str.regexp "[0-9]*$") "" name + in + let already_used name = + List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context + in + if not (already_used basename) then + C.Name basename + else + let rec try_next n = + let name' = basename ^ string_of_int n in + if already_used name' then + try_next (n+1) + else + C.Name name' + in + try_next 1 +;; (* identity_relocation_list_for_metavariable i canonical_context *) (* returns the identity relocation list, which is the list [1 ; ... ; n] *) diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index de0b37596..a1e4d21b6 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -23,7 +23,11 @@ * http://cs.unibo.it/helm/. *) -val fresh_name : Cic.name -> string +(* mk_fresh_name context name typ *) +(* returns an identifier which is fresh in the context *) +(* and that resembles [name] as much as possible. *) +(* [typ] will be the type of the variable *) +val mk_fresh_name : ProofEngineTypes.mk_fresh_name_type (* identity_relocation_list_for_metavariable i canonical_context *) (* returns the identity relocation list, which is the list [1 ; ... ; n] *) diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index f5e75fc47..974e6893c 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -39,3 +39,6 @@ type tactic = status:(proof * goal) -> proof * goal list (** tactic failure *) exception Fail of string + (** constraint: the returned value will always be constructed by Cic.Name **) +type mk_fresh_name_type = + Cic.context -> Cic.name -> typ:Cic.term -> Cic.name diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 5f6dade40..f0a3070f7 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -103,17 +103,17 @@ let generalize_tac ~term ~status:((proof,goal) as status) = in *) T.thens - ~start:(P.cut_tac - ~term:( - C.Prod( - (C.Name "dummy_for_gen"), - (CicTypeChecker.type_of_aux' metasenv context term), - (ProofEngineReduction.replace_lifting_csc 1 - ~equality:(==) - ~what:term - ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *) - ~where:ty) - ))) + ~start: + (P.cut_tac + (C.Prod( + (C.Name "dummy_for_gen"), + (CicTypeChecker.type_of_aux' metasenv context term), + (ProofEngineReduction.replace_lifting_csc 1 + ~equality:(==) + ~what:term + ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *) + ~where:ty) + ))) ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac] ~status ;; @@ -153,9 +153,9 @@ let compare_tac ~term ~status:((proof, goal) as status) = ] in T.thens - ~start:(P.cut_tac ~term:term') + ~start:(P.cut_tac term') ~continuations:[ - T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; + T.then_ ~start:(P.intros_tac ()) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; decide_equality_tac] | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> let term' = (* (t1=t2) \/ ~(t1=t2) *) @@ -170,9 +170,9 @@ let compare_tac ~term ~status:((proof, goal) as status) = ] in T.thens - ~start:(P.cut_tac ~term:term') + ~start:(P.cut_tac term') ~continuations:[ - T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; + T.then_ ~start:(P.intros_tac ()) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; decide_equality_tac] | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality") ;; -- 2.39.2