Huge reorganization of matita and ocaml.

[helm.git] / helm / ocaml / tactics / proofEngineHelpers.ml

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 51405f5fdfa7269f58c3b780b16484eb7b67e85d..bb6390bdcdb2c3d231674520882fc41c585c44f0 100644 (file)
--- 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
@@ -224,14 +226,12 @@ 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 
     with
-    | Invalid_argument _ -> raise (Bad_pattern error_msg)
+    | Invalid_argument _ -> raise (Bad_pattern (lazy error_msg))
   in
   let rec aux context where term =
     match (where, term) with
@@ -292,15 +292,18 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
             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 (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
+   let roots =
+     match where with
+     | None -> []
+     | Some where -> aux context where term
+   in
     match wanted with
        None -> [],metasenv,ugraph,roots
      | Some wanted ->
@@ -455,7 +458,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].
@@ -472,15 +475,15 @@ exception Fail of string
   * @raise Bad_pattern
   * *)
   let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
-       ~pattern:(what,hyp_patterns,goal_pattern)
+       ~(pattern: (Cic.term, Cic.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
    let subst,metasenv,ugraph,ty_terms =
     select_in_term ~metasenv ~context ~ugraph ~term:ty
      ~pattern:(what,goal_pattern) in
-   let context_len = List.length context in
    let subst,metasenv,ugraph,context_terms =
     let subst,metasenv,ugraph,res,_ =
      (List.fold_right
@@ -494,7 +497,7 @@ exception Fail of string
             | 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
             | 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
@@ -678,6 +681,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