X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=fd336910ea4a899e3d5fcdc15870bffd929afb12;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=4bb46fc4c011c491abfd316271b6e2b968137413;hpb=a3ed9ca5ff6563d05d2940727e4fa335fdaaeb0f;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 4bb46fc4c..fd336910e 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception Bad_pattern of string
+exception Bad_pattern of string Lazy.t
 
 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
   CicMkImplicit.new_meta metasenv []
@@ -46,9 +46,10 @@ let subst_meta_in_proof proof meta term newmetasenv =
          List.map
           (function
               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
-            | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
+            | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def (subst_in s,None))
             | None -> None
-            | Some (_,Cic.Def (_,Some _)) -> assert false
+            | Some (n,Cic.Def (bo,Some ty)) ->
+               Some (n,Cic.Def (subst_in bo,Some (subst_in ty)))
           ) canonical_context
         in
          i,canonical_context',(subst_in ty)
@@ -92,8 +93,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
                  None -> None
                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
                | Some (i,Cic.Def (t,None))  ->
-                  Some (i,Cic.Def ((subst_in t),None))
-               | Some (_,Cic.Def (_,Some _))  -> assert false
+                  Some (i,Cic.Def (subst_in t,None))
+               | Some (i,Cic.Def (bo,Some ty)) ->
+                  Some (i,Cic.Def (subst_in bo,Some (subst_in ty)))
              ) canonical_context
            in
             (m,canonical_context',subst_in ty)::i
@@ -227,6 +229,12 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
   let add_ctx context name entry =
       (Some (name, entry)) :: context
   in
+  let map2 error_msg f l1 l2 = 
+    try 
+      List.map2 f l1 l2 
+    with
+    | Invalid_argument _ -> raise (Bad_pattern (lazy error_msg))
+  in
   let rec aux context where term =
     match (where, term) with
     | Cic.Implicit (Some `Hole), t -> [context,t]
@@ -234,7 +242,7 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
     | Cic.Implicit None,_ -> []
     | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) ->
         List.concat
-          (List.map2
+          (map2 "wrong number of argument in explicit substitution"
             (fun t1 t2 ->
               (match (t1, t2) with
                   Some t1, Some t2 -> aux context t1 t2
@@ -271,7 +279,7 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
         List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
        in
         List.concat
-          (List.map2
+          (map2 "wrong number of mutually recursive functions"
             (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> 
               aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
             funs1 funs2)
@@ -280,17 +288,18 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
         List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
        in
         List.concat
-          (List.map2
+          (map2 "wrong number of mutually co-recursive functions"
             (fun (_, ty1, bo1) (_, ty2, bo2) ->
               aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
             funs1 funs2)
     | x,y -> 
         raise (Bad_pattern 
-                (Printf.sprintf "Pattern %s versus term %s" 
+                (lazy (Printf.sprintf "Pattern %s versus term %s" 
                   (CicPp.ppterm x)
-                  (CicPp.ppterm y)))
+                  (CicPp.ppterm y))))
   and auxs context terms1 terms2 =  (* as aux for list of terms *)
-    List.concat (List.map2 (fun t1 t2 -> aux context t1 t2) terms1 terms2)
+    List.concat (map2 "wrong number of arguments in application"
+      (fun t1 t2 -> aux context t1 t2) terms1 terms2)
   in
    let context_len = List.length context in
    let roots = aux context where term in
@@ -302,12 +311,10 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
             [] -> [],metasenv,ugraph,[]
           | (context',where)::tl ->
              let subst,metasenv,ugraph,tl' = find_in_roots tl in
-             let context'_len = List.length context' in
              let subst,metasenv,ugraph,found =
-              let wanted =
-               CicSubstitution.lift (context'_len - context_len) wanted
-              in
-               find_subterms ~subst ~metasenv ~ugraph ~wanted ~context where
+              let wanted, metasenv, ugraph = wanted context' metasenv ugraph in
+               find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context'
+                where
              in
               subst,metasenv,ugraph,found @ tl'
         in
@@ -450,7 +457,7 @@ let pattern_of ?(equality=(==)) ~term terms =
   in
    snd (aux term)
 
-exception Fail of string
+exception Fail of string Lazy.t
 
   (** select metasenv conjecture pattern
   * select all subterms of [conjecture] matching [pattern].
@@ -462,7 +469,10 @@ exception Fail of string
   * with their context conclusion. Note: in the result the list of hypothesis
   * has an entry for each entry in the context and in the same order.
   * Of course the list of terms (with their context) associated to the
-  * hypothesis name may be empty. *)
+  * hypothesis name may be empty. 
+  *
+  * @raise Bad_pattern
+  * *)
   let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
        ~pattern:(what,hyp_patterns,goal_pattern)
   =
@@ -484,30 +494,12 @@ exception Fail of string
             | None ->
                subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
             | Some pat ->
-               try
-                let what =
-                 match what with
-                    None -> None
-                  | Some what ->
-                     let what,subst',metasenv' =
-                      CicMetaSubst.delift_rels [] metasenv
-                       (context_len - List.length context) what
-                     in
-                      assert (subst' = []);
-                      assert (metasenv' = metasenv);
-                      Some what in
                 let subst,metasenv,ugraph,terms =
                  select_in_term ~metasenv ~context ~ugraph ~term
                   ~pattern:(what,pat)
                 in
                  subst,metasenv,ugraph,((Some (`Decl terms))::res),
-                  (entry::context)
-               with
-                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
-                 raise
-                  (Fail
-                    ("The term the user wants to convert is not closed " ^
-                     "in the context of the position of the substitution.")))
+                  (entry::context))
         | Some (name,Cic.Def (bo, ty)) ->
             (match find_pattern_for name with
             | None ->
@@ -515,18 +507,6 @@ exception Fail of string
                 subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res),
                  (entry::context)
             | Some pat -> 
-               try
-                let what =
-                 match what with
-                    None -> None
-                  | Some what ->
-                     let what,subst',metasenv' =
-                      CicMetaSubst.delift_rels [] metasenv
-                       (context_len - List.length context) what
-                     in
-                      assert (subst' = []);
-                      assert (metasenv' = metasenv);
-                      Some what in
                 let subst,metasenv,ugraph,terms_bo =
                  select_in_term ~metasenv ~context ~ugraph ~term:bo
                   ~pattern:(what,pat) in
@@ -541,28 +521,24 @@ exception Fail of string
                       subst,metasenv,ugraph,Some res
                 in
                  subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res),
-                  (entry::context)
-               with
-                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
-                 raise
-                  (Fail
-                    ("The term the user wants to convert is not closed " ^
-                     "in the context of the position of the substitution.")))
+                  (entry::context))
       ) context (subst,metasenv,ugraph,[],[]))
     in
      subst,metasenv,ugraph,res
    in
     subst,metasenv,ugraph,context_terms, ty_terms
 
-(** locate_in_term what where
-* [what] must be a physical pointer to a subterm of [where]
-* It returns the context of [what] in [where] *)
-let locate_in_term what ~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
+* [context] must be the context of [where]
+*)
+let locate_in_term ?(equality=(fun _ -> (==))) what ~where context =
   let add_ctx context name entry =
-      (Some (name, entry)) :: context
-  in
+      (Some (name, entry)) :: context in
   let rec aux context where =
-   if what == where then context
+   if equality context what where then [context,where]
    else
     match where with
     | Cic.Implicit _
@@ -603,20 +579,49 @@ let locate_in_term what ~where =
   and auxs context tl =  (* as aux for list of terms *)
     List.concat (List.map (fun t -> aux context t) tl)
   in
-   aux [] where
+   aux context where
 
+(** locate_in_conjecture 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
+* [context] must be the context of [where]
+*)
+let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) =
+ 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 context' = entry::context in
+          context',res
+      | Some (_, Cic.Def (bo,ty)) ->
+         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
+         let context' = entry::context in
+          context',res
+   ) context ([],[])
+ in
+  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  *)
-(* which there is new a META for each hypothesis, a list of arguments for the *)
-(* new applications and the index of the last new META introduced. The nth    *)
-(* argument in the list of arguments is just the nth new META.                *)
-let saturate_term newmeta metasenv context ty =
+(* saturate_term newmeta metasenv context ty goal_arity                       *)
+(* Given a type [ty] (a backbone), it returns its suffix of length            *)
+(* [goal_arity] head and a new metasenv in which there is new a META for each *)
+(* hypothesis, a list of arguments for the new applications and the index of  *)
+(* the last new META introduced. The nth argument in the list of arguments is *)
+(* just the nth new META.                                                     *)
+let saturate_term newmeta metasenv context ty goal_arity =
  let module C = Cic in
  let module S = CicSubstitution in
+ assert (goal_arity >= 0);
   let rec aux newmeta ty =
-   let ty' = ty in
-   match ty' with
+   match ty with
       C.Cast (he,_) -> aux newmeta he
 (* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
       (* If the expected type is a Type, then also Set is OK ==>
@@ -641,22 +646,31 @@ let saturate_term newmeta metasenv context ty =
          CicMkImplicit.identity_relocation_list_for_metavariable context
        in
         let newargument = C.Meta (newmeta,irl) in
-         let (res,newmetasenv,arguments,lastmeta) =
+         let res,newmetasenv,arguments,lastmeta,prod_no =
           aux (newmeta + 1) (S.subst newargument t)
          in
-         let s' = CicReduction.normalize ~delta:false context s in
-          res,(newmeta,context,s')::newmetasenv,newargument::arguments,lastmeta
-          (** NORMALIZE RATIONALE 
-           * we normalize the target only NOW since we may be in this case:
-           * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k  
-           * and we want a mesasenv with ?1:A1 and ?2:A2 and not
-           * ?1, ?2, ?3 (that is the one we whould get if we start from the
-           * beta-normalized A1 -> A2 -> A3 -> P **)
-    | t -> (CicReduction.normalize ~delta:false context t),[],[],newmeta
+          if prod_no + 1 = goal_arity then
+           let head = CicReduction.normalize ~delta:false context ty in
+            head,[],[],lastmeta,goal_arity + 1
+          else
+           (** NORMALIZE RATIONALE 
+            * we normalize the target only NOW since we may be in this case:
+            * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k  
+            * and we want a mesasenv with ?1:A1 and ?2:A2 and not
+            * ?1, ?2, ?3 (that is the one we whould get if we start from the
+            * beta-normalized A1 -> A2 -> A3 -> P **)
+           let s' = CicReduction.normalize ~delta:false context s in
+            res,(newmeta,context,s')::newmetasenv,newargument::arguments,
+             lastmeta,prod_no + 1
+    | t ->
+       let head = CicReduction.normalize ~delta:false context t in
+        match CicReduction.whd context head with
+           C.Prod _ as head' -> aux newmeta head'
+         | _ -> head,[],[],newmeta,0
   in
    (* WARNING: here we are using the invariant that above the most *)
    (* recente new_meta() there are no used metas.                  *)
-   let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
+   let res,newmetasenv,arguments,lastmeta,_ = aux newmeta ty in
     res,metasenv @ newmetasenv,arguments,lastmeta
 
 let lookup_type metasenv context hyp =
@@ -666,6 +680,6 @@ let lookup_type metasenv context hyp =
       | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
          p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
       | _ :: tail -> aux (succ p) tail
-      | [] -> raise (ProofEngineTypes.Fail "lookup_type: not premise in the current goal")
+      | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal"))
    in
    aux 1 context