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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index a8e32886371030ea1bc9fe13a567108fcd139019..0b61e9595778354639878ca264fc85b832eb8076 100644 (file)
--- 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 b9112deed25c0f90da430502ec168f504a367782..895a799dceb871e74ae5230871b2e110f8d62317 100644 (file)
--- 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 a5541ab03d4d39265dbd25b79880c6b17900d7aa..bb060305627691c553f2664473c0b8f35ca39237 100644 (file)
--- 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 e28e1425d8fd69270ba896bcf1c703a1cc2f0b58..a7c0e5b543cb6fe23f51dd9be8b1f81c39779cab 100644 (file)
--- 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 58dafd1a674441e25a8a933dc82a031fef1a5fea..6e532a807478f3f28f4c11898e4ed1afb6ea7c48 100644 (file)
--- 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 40a9e6c80067ffd81d34cdb4c8a771d89eacd8f8..d50707f7344f898068df21d29809a9f22729f6d7 100644 (file)
--- 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 dbec3fb72b0d9532b2fa016bd7737749c62dd573..153cb6f285df4b647c0b8874178c7d9e394805f1 100644 (file)
--- 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 6d524093569a91663c8f57ec091286a756e31350..9d5bc475398251f61a38a77ba1930a50138cbe9a 100644 (file)
--- 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 f792666c296790f78e61d07d3aeb9f112a145896..35576326eb2dbc2f6ffa1e0f4b7adb6744908acc 100644 (file)
--- 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
+