1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture

   generalized to return the list of matched terms
2. unfold generalized to unfold several occurrences at once

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index da3a730fb7831212b17c5f6ab09b012fefe78e2a..f329780633b423d2d0d626fdfd6ad18cb4b34156 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -126,7 +126,7 @@ let tactic_of_ast = function
       | `Normalize -> Tactics.normalize ~pattern
       | `Reduce -> Tactics.reduce ~pattern  
       | `Simpl -> Tactics.simpl ~pattern 
-      | `Unfold what -> Tactics.unfold ~pattern ?what
+      | `Unfold what -> Tactics.unfold ~pattern what
       | `Whd -> Tactics.whd ~pattern)
   | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
   | GrafiteAst.Replace (_, pattern, with_what) ->

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index efda8cd7638e209fb4d580a9b6cf2bc9e8484e98..3cb9c8c0b2ba3d4a6ff69dbc11459bd12395d127 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -254,8 +254,12 @@ object (self)
       match term with
       | `Term t ->
           let context' =
+           match
             ProofEngineHelpers.locate_in_conjecture t
               (dummy_goal, context, conclusion)
+           with
+              [context,_] -> context
+            | _ -> assert false (* since it uses physical equality *)
           in
           dummy_goal, context', t
       | `Hyp context -> dummy_goal, context, Cic.Rel 1

diff --git a/helm/matita/tests/unfold.ma b/helm/matita/tests/unfold.ma
index ff68d5fd1e8cbb111bb13fda979665d60b49809e..c91ff18636999638c233c9844a8481c1b3a6f776 100644 (file)
--- a/helm/matita/tests/unfold.ma
+++ b/helm/matita/tests/unfold.ma
@@ -21,9 +21,10 @@ lemma lem: \forall n. S (n + n) = (S n) + n.
  intro; reflexivity.
 qed.
 
-theorem trivial: \forall n. S (myplus n n) = (S n) + n.
- unfold myplus.
+theorem trivial: \forall n. S (myplus n n) = myplus (S n) n.
+ unfold myplus in \vdash \forall _.(? ? ? %).
  intro.
+ unfold myplus.
  rewrite > lem.
  reflexivity.
 qed.
\ No newline at end of file

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index b9ee8bb8fc8d72eb00e231ad0b9f531d6b6cd9ad..22b6c8487a8348d74a80f896c501a26f3263aba1 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -554,23 +554,17 @@ exception Fail of string
    in
     subst,metasenv,ugraph,context_terms, ty_terms
 
-exception TermNotFound
-exception TermFoundMultipleTimes
-
 (** locate_in_term equality what where context
 * [what] must match a subterm of [where] according to [equality]
-* It returns the matched term together with its context in [where]
+* It returns the matched terms together with their contexts in [where]
 * [equality] defaults to physical equality
 * [context] must be the context of [where]
-* It may raise TermNotFound or TermFoundMultipleTimes
 *)
 let locate_in_term ?(equality=(==))what ~where context =
-  let (@@) (l1,l2) (l1',l2') = l1 @ l1', l2 @ l2' in
-  let list_concat l = List.fold_right (@@) l ([],[]) in
   let add_ctx context name entry =
       (Some (name, entry)) :: context in
   let rec aux context where =
-   if equality what where then context,[where]
+   if equality what where then [context,where]
    else
     match where with
     | Cic.Implicit _
@@ -580,83 +574,67 @@ let locate_in_term ?(equality=(==))what ~where context =
     | Cic.Var _
     | Cic.Const _
     | Cic.MutInd _
-    | Cic.MutConstruct _ -> [],[]
-    | Cic.Cast (te, ty) -> aux context te @@ aux context ty
+    | Cic.MutConstruct _ -> []
+    | Cic.Cast (te, ty) -> aux context te @ aux context ty
     | Cic.Prod (name, s, t)
     | Cic.Lambda (name, s, t) ->
-        aux context s @@ aux (add_ctx context name (Cic.Decl s)) t
+        aux context s @ aux (add_ctx context name (Cic.Decl s)) t
     | Cic.LetIn (name, s, t) -> 
-        aux context s @@ aux (add_ctx context name (Cic.Def (s,None))) t
+        aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t
     | Cic.Appl tl -> auxs context tl
     | Cic.MutCase (_, _, out, t, pat) ->
-        aux context out @@ aux context t @@ auxs context pat
+        aux context out @ aux context t @ auxs context pat
     | Cic.Fix (_, funs) ->
        let tys =
         List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
        in
-        list_concat
+        List.concat
           (List.map
             (fun (_, _, ty, bo) -> 
-              aux context ty @@ aux (tys @ context) bo)
+              aux context ty @ aux (tys @ context) bo)
             funs)
     | Cic.CoFix (_, funs) ->
        let tys =
         List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
        in
-        list_concat
+        List.concat
           (List.map
             (fun (_, ty, bo) ->
-              aux context ty @@ aux (tys @ context) bo)
+              aux context ty @ aux (tys @ context) bo)
             funs)
   and auxs context tl =  (* as aux for list of terms *)
-    list_concat (List.map (fun t -> aux context t) tl)
+    List.concat (List.map (fun t -> aux context t) tl)
   in
-   match aux context where with
-      context,[] -> raise TermNotFound
-    | context,[t] -> context,t
-    | context,_ -> raise TermFoundMultipleTimes
+   aux context where
 
-(** locate_in_term equality what where
-* [what] must be a subterm of [where] according to [equality]
-* It returns the context of [what] in [where]
+(** locate_in_term equality what where context
+* [what] must match a subterm of [where] according to [equality]
+* It returns the matched terms together with their contexts in [where]
 * [equality] defaults to physical equality
-* It may raise TermNotFound or TermFoundMultipleTimes
+* [context] must be the context of [where]
 *)
 let locate_in_conjecture ?(equality=(==)) what (_,context,ty) =
- let (@@) (l1,l2) =
-  function
-     None -> l1,l2
-   | Some (l1',t) -> l1 @ l1', l2 @ [t] in
- let locate_in_term what ~where context =
-  try
-   Some (locate_in_term ~equality what ~where context)
-  with
-     TermNotFound -> None in
  let context,res =
   List.fold_right
    (fun entry (context,res) ->
      match entry with
         None -> entry::context, res
       | Some (_, Cic.Decl ty) ->
-         let res = res @@ locate_in_term what ~where:ty context in
+         let res = res @ locate_in_term what ~where:ty context in
          let context' = entry::context in
           context',res
       | Some (_, Cic.Def (bo,ty)) ->
-         let res = res @@ locate_in_term what ~where:bo context in
+         let res = res @ locate_in_term what ~where:bo context in
          let res =
           match ty with
              None -> res
            | Some ty ->
-              res @@ locate_in_term what ~where:ty context in
+              res @ locate_in_term what ~where:ty context in
          let context' = entry::context in
           context',res
-   ) context ([],([],[]))
+   ) context ([],[])
  in
- let res = res @@ locate_in_term what ~where:ty context in
-  match res with
-     context,[] -> raise TermNotFound
-   | context,[_] -> context
-   | context,_ -> raise TermFoundMultipleTimes
+  res @ locate_in_term what ~where:ty context
 
 (* saturate_term newmeta metasenv context ty                                  *)
 (* Given a type [ty] (a backbone), it returns its head and a new metasenv in  *)

diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli
index 574a9441318fd8c03f909dfe12d06011ff5ee563..859f1f4bac35096d0844f15c7718fef3577be179 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.mli
+++ b/helm/ocaml/tactics/proofEngineHelpers.mli
@@ -80,29 +80,25 @@ val select:
   ] option list *
   (Cic.context * Cic.term) list
 
-exception TermNotFound
-exception TermFoundMultipleTimes
-
 (** locate_in_term equality what where context
 * [what] must match a subterm of [where] according to [equality]
-* It returns the matched term together with its context in [where]
+* It returns the matched terms together with their contexts in [where]
 * [equality] defaults to physical equality
 * [context] must be the context of [where]
-* It may raise TermNotFound or TermFoundMultipleTimes
 *)
 val locate_in_term:
  ?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> where:Cic.term ->
-  Cic.context -> Cic.context * Cic.term
+  Cic.context -> (Cic.context * Cic.term) list
 
-(** locate_in_conjecture equality what where
+(** locate_in_term equality what where context
 * [what] must match a subterm of [where] according to [equality]
-* It returns the context of [what] in [where]
+* It returns the matched terms together with their contexts in [where]
 * [equality] defaults to physical equality
-* It may raise TermNotFound or TermFoundMultipleTimes
+* [context] must be the context of [where]
 *)
 val locate_in_conjecture:
  ?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> Cic.conjecture ->
-  Cic.context
+  (Cic.context * Cic.term) list
 
 (* saturate_term newmeta metasenv context ty                                  *)
 (* Given a type [ty] (a backbone), it returns its head and a new metasenv in  *)

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 8d42450685d2ec18287ad1deb1d299b43ea2f157..d04acd181ba2c7c621b00ec2f479f2089aaafebe 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -933,24 +933,26 @@ let unfold ?what context where =
    | Cic.Appl (he::tl) -> hd_delta_beta context tl he
    | t -> cannot_delta_expand t
  in
- let context, where' =
+ let context_and_matched_term_list =
   match what with
-     None -> context, where
+     None -> [context, where]
    | Some what ->
-      try
+      let res =
        ProofEngineHelpers.locate_in_term
         ~equality:first_is_the_expandable_head_of_second
         what ~where context
-      with
-       ProofEngineHelpers.TermNotFound ->
+      in
+       if res = [] then
         raise
          (ProofEngineTypes.Fail
            ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
+       else
+        res
  in
-  let reduced_term = hd_delta_beta context [] where' in
-   match what with
-      None -> reduced_term
-    | Some what ->
-       replace ~equality:first_is_the_expandable_head_of_second
-        ~what:[what] ~with_what:[reduced_term] ~where
+  let reduced_terms =
+   List.map
+    (function (context,where) -> hd_delta_beta context [] where)
+    context_and_matched_term_list in
+  let whats = List.map snd context_and_matched_term_list in
+   replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
 ;;

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 492b265cb5b3e97e0a26077b402104bb673430e5..f5c82a9fe7da0be3f2702d90c5733a99cc3c6f4d 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -79,7 +79,7 @@ let simpl_tac ~pattern =
 let reduce_tac ~pattern =
  mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
 
-let unfold_tac ?what ~pattern =
+let unfold_tac what ~pattern =
  mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what)
   ~pattern);;
   

diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli
index 6ef80512b8173ec4fd8b776181078530e45c9c0a..56b80c06a6a2256fbfdf6f5aee5ce53ff235aa4a 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.mli
+++ b/helm/ocaml/tactics/reductionTactics.mli
@@ -29,7 +29,7 @@ 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 unfold_tac:
- ?what:Cic.term -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
+ Cic.term option -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 
 val change_tac:
   pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic 

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 4780a82fb32ba51fdcb998adc6a73dc980d0acc4..77e3f8ac545f176a1ac99488be6df6607bbf847f 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -79,6 +79,6 @@ val split : ProofEngineTypes.tactic
 val symmetry : ProofEngineTypes.tactic
 val transitivity : term:Cic.term -> ProofEngineTypes.tactic
 val unfold :
-  ?what:Cic.term ->
+  Cic.term option ->
   pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic