made executable again

[helm.git] / helm / software / components / tactics / metadataQuery.ml

diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml
index 443ae973fe2c7b0c86d288ab08015c482db471a9..6db568cb4ab9ad60516bc30f1a0d366e4e6a7b1f 100644 (file)
--- a/helm/software/components/tactics/metadataQuery.ml
+++ b/helm/software/components/tactics/metadataQuery.ml
@@ -51,11 +51,11 @@ let signature_of_hypothesis context metasenv =
             try 
               let ty,_ = 
                 CicTypeChecker.type_of_aux' 
-                  metasenv current_ctx t CicUniv.empty_ugraph 
+                  metasenv current_ctx t CicUniv.oblivion_ugraph 
               in
               let sort,_ = 
                 CicTypeChecker.type_of_aux' 
-                  metasenv current_ctx ty CicUniv.empty_ugraph 
+                  metasenv current_ctx ty CicUniv.oblivion_ugraph 
               in
               let set = Constr.UriManagerSet.union set(Constr.constants_of ty)in
               match sort with
@@ -109,19 +109,19 @@ let filter_uris_backward ~dbd ~facts signature uris =
     intersect uris siguris 
 
 let compare_goal_list proof goal1 goal2 =
-  let _,metasenv,_,_ = proof in
+  let _,metasenv, _subst, _,_, _ = proof in
   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
   let ty_sort1,_ = 
-    CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph 
+    CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph 
   in
   let ty_sort2,_ = 
-    CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph 
+    CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.oblivion_ugraph 
   in
   let prop1 =
     let b,_ = 
       CicReduction.are_convertible 
-       ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph 
+       ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.oblivion_ugraph 
     in
       if b then 0
       else 1
@@ -129,7 +129,7 @@ let compare_goal_list proof goal1 goal2 =
   let prop2 =
     let b,_ = 
       CicReduction.are_convertible 
-       ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph 
+       ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.oblivion_ugraph 
     in 
       if b then 0
       else 1
@@ -150,7 +150,7 @@ let close_with_types s metasenv context =
     (fun e bag -> 
       let t = CicUtil.term_of_uri e in
       let ty, _ = 
-        CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph  
+        CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph  
       in
       Constr.UriManagerSet.union bag (Constr.constants_of ty)) 
     s s
@@ -162,7 +162,7 @@ let close_with_constructors s metasenv context =
       match t with
          Cic.MutInd (uri,_,_)  
        | Cic.MutConstruct (uri,_,_,_) ->  
-           (match fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+           (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
                 Cic.InductiveDefinition(tl,_,_,_) ->
                   snd
                     (List.fold_left
@@ -171,6 +171,8 @@ let close_with_constructors s metasenv context =
                             List.fold_left 
                               (fun (j,s) _ -> 
                                  let curi = UriManager.uri_of_uriref uri i (Some j) in
+(*                                     prerr_endline ("adding " ^
+ *                                     (UriManager.string_of_uri curi)); *)
                                    j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
                             (i+1,s)) (0,bag) tl)
               | _ -> assert false)
@@ -194,8 +196,8 @@ let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
 let cmatch' = Constr.cmatch'
 
 (* used only by te old auto *)
-let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
- let (_, metasenv, _, _) = proof in
+let signature_of_goal ~(dbd:HSql.dbd) ((proof, goal) as _status) =
+ let (_, metasenv, _subst, _, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
  let set = signature_of_hypothesis context metasenv in
@@ -215,7 +217,7 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
 let is_predicate u = 
     let ty, _ = 
       try CicTypeChecker.type_of_aux' [] []
-        (CicUtil.term_of_uri u) CicUniv.empty_ugraph
+        (CicUtil.term_of_uri u) CicUniv.oblivion_ugraph
       with CicTypeChecker.TypeCheckerFailure _ -> assert false
     in
     let rec check_last_pi = function
@@ -229,7 +231,7 @@ let is_predicate u =
 let only constants uri =
   prerr_endline (UriManager.string_of_uri uri);
   let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
-  let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+  let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
   let consts = Constr.constants_of ty in
 (*
   prerr_endline ("XXX " ^ UriManager.string_of_uri uri);
@@ -260,7 +262,7 @@ let types_for_equality metasenv goal =
       (fun (i,acc) _ ->         
         let ty, _ = 
            CicTypeChecker.type_of_aux' 
-             metasenv context (Cic.Rel i) CicUniv.empty_ugraph in
+             metasenv context (Cic.Rel i) CicUniv.oblivion_ugraph in
         let newty = types_of_equality ty in
           (i+1,Constr.SetSet.union newty acc)) 
       (1,all) context
@@ -272,10 +274,13 @@ let signature_of metasenv goal =
   let ty_set = Constr.constants_of ty in
   let hyp_set = signature_of_hypothesis context metasenv in
   let set = Constr.UriManagerSet.union ty_set hyp_set in
-    close_with_types set metasenv context
+    close_with_types
+     (close_with_constructors (close_with_types set metasenv context)
+       metasenv context)
+    metasenv context
 
 
-let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
+let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let ty_set = Constr.constants_of ty in
   let hyp_set = signature_of_hypothesis context metasenv in
@@ -288,20 +293,20 @@ let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
   let uris =
     Constr.UriManagerSet.fold
       (fun u acc -> 
-         prerr_endline ("processing "^(UriManager.string_of_uri u));
+         debug_print (lazy ("processing "^(UriManager.string_of_uri u)));
          let set_for_sigmatch = 
           Constr.UriManagerSet.remove u all_constants_closed in
         if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
           (* equality has a special treatment *)
-           (prerr_endline "special treatment";
+           (debug_print (lazy "special treatment");
           let tfe =
             Constr.SetSet.elements (types_for_equality metasenv goal) 
           in
             List.fold_left 
               (fun acc l ->
                  let tyl = Constr.UriManagerSet.elements l in
-                  prerr_endline ("tyl: "^(String.concat "\n" 
-                       (List.map UriManager.string_of_uri tyl)));
+                  debug_print (lazy ("tyl: "^(String.concat "\n" 
+                       (List.map UriManager.string_of_uri tyl))));
                  let set_for_sigmatch =
                    Constr.UriManagerSet.diff set_for_sigmatch l in
                  let uris =
@@ -310,7 +315,7 @@ let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
                    acc @ uris) 
               acc tfe)
         else
-           (prerr_endline "normal treatment";
+           (debug_print (lazy "normal treatment");
            let uris =
              sigmatch ~dbd ~facts:false ~where:`Statement 
                (Some (u,[]),set_for_sigmatch)
@@ -334,7 +339,7 @@ let filter_out_predicate set ctx menv =
   Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set  
 ;;
 
-let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
+let equations_for_goal ~(dbd:HSql.dbd) ?signature ((proof, goal) as _status) =
 (*
   let to_string set =
     "{\n" ^
@@ -344,7 +349,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
     ^ "\n}"
   in
 *)
- let (_, metasenv, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = 
    match signature with 
@@ -393,8 +398,8 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
    (*        else raise Goal_is_not_an_equation *)
 
 let experimental_hint 
-  ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
-  let (_, metasenv, _, _) = proof in
+  ~(dbd:HSql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
+  let (_, metasenv, _subst, _, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
     match signature with
@@ -424,7 +429,8 @@ let experimental_hint
       | Some (main,_) -> 
           let ty, _ = 
             CicTypeChecker.type_of_aux' 
-              metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
+              metasenv context (CicUtil.term_of_uri main)
+              CicUniv.oblivion_ugraph
           in
           Constr.constants_of ty
     in
@@ -475,10 +481,10 @@ let experimental_hint
     (aux uris)
 
 let new_experimental_hint 
-  ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
+  ~(dbd:HSql.dbd) ?(facts=false) ?signature ~universe
   ((proof, goal) as status)
 =
-  let (_, metasenv, _, _) = proof in
+  let (_, metasenv,  _subst, _, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
     match signature with