From 4dad47b93729b5108a7de190faeb25fcf16aba5d Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 12 Dec 2005 15:59:58 +0000 Subject: [PATCH] changed pattern datatype: - now the goal_pattern (third component) is optional, instead of using Cic.Implicit without annotation to denote non-specified pattern - now the patter is polymorph over terms and lazy terms --- helm/ocaml/tactics/equalityTactics.ml | 25 ++++++++++++++--------- helm/ocaml/tactics/equalityTactics.mli | 7 ++++--- helm/ocaml/tactics/proofEngineHelpers.ml | 19 +++++++++-------- helm/ocaml/tactics/proofEngineHelpers.mli | 2 +- helm/ocaml/tactics/proofEngineTypes.ml | 7 +++++-- helm/ocaml/tactics/proofEngineTypes.mli | 7 +++++-- helm/ocaml/tactics/reductionTactics.mli | 14 ++++++------- helm/ocaml/tactics/tactics.mli | 25 +++++++++++++---------- helm/ocaml/tactics/variousTactics.mli | 3 ++- 9 files changed, 64 insertions(+), 45 deletions(-) diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index a8e328863..0b61e9595 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -let rec rewrite_tac ~direction ~pattern equality = +let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality = let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status = let module C = Cic in @@ -41,14 +41,14 @@ let rec rewrite_tac ~direction ~pattern equality = PET.apply_tactic (Tacticals.then_ (rewrite_tac ~direction - ~pattern:(None,[he],Cic.Implicit None) equality) + ~pattern:(None,[he],None) equality) (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) equality) ) status - | [_] as hyps_pat when concl_pat <> Cic.Implicit None -> + | [_] as hyps_pat when concl_pat <> None -> PET.apply_tactic (Tacticals.then_ (rewrite_tac ~direction - ~pattern:(None,hyps_pat,Cic.Implicit None) equality) + ~pattern:(None,hyps_pat,None) equality) (rewrite_tac ~direction ~pattern:(None,[],concl_pat) equality) ) status | _ -> @@ -83,11 +83,11 @@ let rec rewrite_tac ~direction ~pattern equality = ProofEngineStructuralRules.clearbody name; ReductionTactics.change_tac ~pattern: - (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None) + (None,[name,Cic.Implicit (Some `Hole)], None) (ProofEngineTypes.const_lazy_term typ); ProofEngineStructuralRules.clear dummy ]), - pat,gty + Some pat,gty | _::_ -> assert false in let if_right_to_left do_not_change a b = @@ -130,7 +130,11 @@ let rec rewrite_tac ~direction ~pattern equality = let lifted_conjecture = metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in let lifted_pattern = - Some (fun _ m u -> lifted_t1, m, u),[],CicSubstitution.lift 1 concl_pat + let lifted_concl_pat = + match concl_pat with + | None -> None + | Some term -> Some (CicSubstitution.lift 1 term) in + Some (fun _ m u -> lifted_t1, m, u),[],lifted_concl_pat in let subst,metasenv',ugraph,_,selected_terms_with_context = ProofEngineHelpers.select @@ -195,8 +199,9 @@ let rewrite_simpl_tac ~direction ~pattern equality = ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~direction ~pattern equality) ;; -let replace_tac ~pattern ~with_what = - let replace_tac ~pattern:(wanted,hyps_pat,concl_pat) ~with_what status = +let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = + let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status = + let _wanted, hyps_pat, concl_pat = pattern in let (proof, goal) = status in let module C = Cic in let module U = UriManager in @@ -259,7 +264,7 @@ let replace_tac ~pattern ~with_what = let rec aux n whats status = match whats with [] -> ProofEngineTypes.apply_tactic T.id_tac status - | (what,pattern)::tl -> + | (what,lazy_pattern)::tl -> let what = CicSubstitution.lift n what in let with_what = CicSubstitution.lift n with_what in let ty_of_with_what = CicSubstitution.lift n ty_of_with_what in diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli index b9112deed..895a799dc 100644 --- a/helm/ocaml/tactics/equalityTactics.mli +++ b/helm/ocaml/tactics/equalityTactics.mli @@ -25,13 +25,14 @@ val rewrite_tac: direction:[`LeftToRight | `RightToLeft] -> - pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic + val rewrite_simpl_tac: direction:[`LeftToRight | `RightToLeft] -> - pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic val replace_tac: - pattern:ProofEngineTypes.pattern -> + pattern:ProofEngineTypes.lazy_pattern -> with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic val reflexivity_tac: ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index a5541ab03..bb0603056 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -226,9 +226,7 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t = find subst metasenv ugraph context wanted t let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = - let add_ctx context name entry = - (Some (name, entry)) :: context - in + let add_ctx context name entry = (Some (name, entry)) :: context in let map2 error_msg f l1 l2 = try List.map2 f l1 l2 @@ -301,7 +299,11 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = List.concat (map2 "wrong number of arguments in application" (fun t1 t2 -> aux context t1 t2) terms1 terms2) in - let roots = aux context where term in + let roots = + match where with + | None -> [] + | Some where -> aux context where term + in match wanted with None -> [],metasenv,ugraph,roots | Some wanted -> @@ -473,8 +475,9 @@ exception Fail of string Lazy.t * @raise Bad_pattern * *) let select ~metasenv ~ugraph ~conjecture:(_,context,ty) - ~pattern:(what,hyp_patterns,goal_pattern) + ~(pattern: (Cic.term, ProofEngineTypes.lazy_term) ProofEngineTypes.pattern) = + let what, hyp_patterns, goal_pattern = pattern in let find_pattern_for name = try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns)) with Not_found -> None in @@ -494,7 +497,7 @@ exception Fail of string Lazy.t | Some pat -> let subst,metasenv,ugraph,terms = select_in_term ~metasenv ~context ~ugraph ~term - ~pattern:(what,pat) + ~pattern:(what, Some pat) in subst,metasenv,ugraph,((Some (`Decl terms))::res), (entry::context)) @@ -507,14 +510,14 @@ exception Fail of string Lazy.t | Some pat -> let subst,metasenv,ugraph,terms_bo = select_in_term ~metasenv ~context ~ugraph ~term:bo - ~pattern:(what,pat) in + ~pattern:(what, Some pat) in let subst,metasenv,ugraph,terms_ty = match ty with None -> subst,metasenv,ugraph,None | Some ty -> let subst,metasenv,ugraph,res = select_in_term ~metasenv ~context ~ugraph ~term:ty - ~pattern:(what,pat) + ~pattern:(what, Some pat) in subst,metasenv,ugraph,Some res in diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index e28e1425d..a7c0e5b54 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -76,7 +76,7 @@ val select: metasenv:Cic.metasenv -> ugraph:CicUniv.universe_graph -> conjecture:Cic.conjecture -> - pattern:ProofEngineTypes.pattern -> + pattern:ProofEngineTypes.lazy_pattern -> Cic.substitution * Cic.metasenv * CicUniv.universe_graph * [ `Decl of (Cic.context * Cic.term) list | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list option diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index 58dafd1a6..6e532a807 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -72,7 +72,10 @@ type lazy_reduction = let const_lazy_reduction red = (fun _ metasenv ugraph -> red, metasenv, ugraph) -type pattern = lazy_term option * (string * Cic.term) list * Cic.term +type ('term, 'lazy_term) pattern = + 'lazy_term option * (string * 'term) list * 'term option + +type lazy_pattern = (Cic.term, lazy_term) pattern let conclusion_pattern t = let t' = @@ -80,7 +83,7 @@ let conclusion_pattern t = | None -> None | Some t -> Some (fun _ m u -> t, m, u) in - t',[],Cic.Implicit (Some `Hole) + t',[],Some (Cic.Implicit (Some `Hole)) (** tactic failure *) exception Fail of string Lazy.t diff --git a/helm/ocaml/tactics/proofEngineTypes.mli b/helm/ocaml/tactics/proofEngineTypes.mli index 40a9e6c80..d50707f73 100644 --- a/helm/ocaml/tactics/proofEngineTypes.mli +++ b/helm/ocaml/tactics/proofEngineTypes.mli @@ -59,10 +59,13 @@ type lazy_reduction = val const_lazy_reduction: reduction -> lazy_reduction (** what, hypothesis patterns, conclusion pattern *) -type pattern = lazy_term option * (string * Cic.term) list * Cic.term +type ('term, 'lazy_term) pattern = + 'lazy_term option * (string * 'term) list * 'term option + +type lazy_pattern = (Cic.term, lazy_term) pattern (** conclusion_pattern [t] returns the pattern (t,[],%) *) -val conclusion_pattern : Cic.term option -> pattern +val conclusion_pattern : Cic.term option -> lazy_pattern (** tactic failure *) exception Fail of string Lazy.t diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli index dbec3fb72..153cb6f28 100644 --- a/helm/ocaml/tactics/reductionTactics.mli +++ b/helm/ocaml/tactics/reductionTactics.mli @@ -23,25 +23,25 @@ * http://cs.unibo.it/helm/. *) -val simpl_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic -val reduce_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic -val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic -val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic +val simpl_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic +val reduce_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic +val whd_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic +val normalize_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic (* The default of term is the thesis of the goal to be prooved *) val unfold_tac: ProofEngineTypes.lazy_term option -> - pattern:ProofEngineTypes.pattern -> + pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val change_tac: - pattern:ProofEngineTypes.pattern -> + pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic val fold_tac: reduction:ProofEngineTypes.lazy_reduction -> term:ProofEngineTypes.lazy_term -> - pattern:ProofEngineTypes.pattern -> + pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 6d5240935..9d5bc4753 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -8,7 +8,7 @@ val auto : ?paramodulation:string -> ?full:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic val change : - pattern:ProofEngineTypes.pattern -> + pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic val clear : hyp:string -> ProofEngineTypes.tactic val clearbody : hyp:string -> ProofEngineTypes.tactic @@ -39,14 +39,14 @@ val fail : ProofEngineTypes.tactic val fold : reduction:ProofEngineTypes.lazy_reduction -> term:ProofEngineTypes.lazy_term -> - pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val fourier : ProofEngineTypes.tactic val fwd_simpl : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic val generalize : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ProofEngineTypes.pattern -> ProofEngineTypes.tactic + ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val id : ProofEngineTypes.tactic val injection : term:Cic.term -> ProofEngineTypes.tactic val intros : @@ -61,26 +61,29 @@ val left : ProofEngineTypes.tactic val letin : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> ProofEngineTypes.tactic -val normalize : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic -val reduce : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic +val normalize : + pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic +val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val reflexivity : ProofEngineTypes.tactic val replace : - pattern:ProofEngineTypes.pattern -> + pattern:ProofEngineTypes.lazy_pattern -> with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic val rewrite : direction:[ `LeftToRight | `RightToLeft ] -> - pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.lazy_pattern -> + Cic.term -> ProofEngineTypes.tactic val rewrite_simpl : direction:[ `LeftToRight | `RightToLeft ] -> - pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.lazy_pattern -> + Cic.term -> ProofEngineTypes.tactic val right : ProofEngineTypes.tactic val ring : ProofEngineTypes.tactic val set_goal : int -> ProofEngineTypes.tactic -val simpl : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic +val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic val unfold : ProofEngineTypes.lazy_term option -> - pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic -val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic +val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index f792666c2..35576326e 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -30,5 +30,6 @@ val assumption_tac: ProofEngineTypes.tactic val generalize_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ProofEngineTypes.pattern -> + ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic + -- 2.39.2