Fixed left/right context distinction in inductive types.

[helm.git] / matita / components / grafite_engine / grafiteEngine.ml

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index b6f5b14e607725534592176ff0eee5b5b319af35..a4942aa07f690017643a88e21ba859a6c77107cf 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -275,25 +275,47 @@ let index_obj_for_auto status (uri, height, _, _, kind) =
    NCicLibrary.dump_obj status (record_index_obj data)
 ;; 
 
-let index_eq uri status =
+(*
+module EmptyC = 
+  struct
+    let metasenv = []
+    let subst = []
+    let context = []
+  end
+*)
+
+let index_eq print uri (status:#NCic.status) =
   let eq_status = status#eq_cache in
-  let eq_status = NCicParamod.index_obj status eq_status uri in
-    status#set_eq_cache eq_status
+  let eq_status,clause = NCicParamod.index_obj status eq_status uri in
+  if print then
+   ((*let module NCicBlob =
+    struct
+     include NCicBlob.NCicBlob(EmptyC)
+     let pp t = status#ppterm ~metasenv:[] ~subst:[] ~context:[] t
+    end in
+   let module Pp = Pp.Pp(NCicBlob) in*)
+   (match clause with
+     | Some (*clause*) (_,Terms.Equation (_,_,_,o),_,_) ->
+        HLog.debug ("Indexed with orientation: " ^ Pp.string_of_comparison o);
+        (*HLog.debug ("Indexed as:" ^ Pp.pp_unit_clause clause)*)
+     | _ -> HLog.debug "Not indexed (i.e. pruned)")) ;
+  status#set_eq_cache eq_status
 ;;
 
 let record_index_eq =
  let basic_index_eq uri
    ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference 
    ~alias_only status
-   = if not alias_only then index_eq (NCicLibrary.refresh_uri uri) status else
-     status
+   = if not alias_only then index_eq false (NCicLibrary.refresh_uri uri) status 
+     else
+      status
  in
   GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
 ;;
 
 let index_eq_for_auto status uri =
  if NnAuto.is_a_fact_obj status uri then
-   let newstatus = index_eq uri status in
+   let newstatus = index_eq true uri status in
      if newstatus#eq_cache == status#eq_cache then status 
      else
        ((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*)
@@ -612,7 +634,16 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                   (*HLog.warn "error in generating projection/eliminator";*)
                   status
              ) status boxml in             
-           let _,_,_,_,nobj = obj in 
+           let _,_,_,_,nobj = obj in
+           (* attempting to generate an inversion principle on the maximum
+            * universe can take a long time to fail: this code removes maximal
+            * sorts from the universe list *)
+           let universes = NCicEnvironment.get_universes () in
+           let max_univ = List.fold_left max [] universes in
+           let universes = 
+             List.filter (fun x -> NCicEnvironment.universe_lt x max_univ)
+               universes
+           in
            let status = match nobj with
                NCic.Inductive (is_ind,leftno,itl,_) ->
                  List.fold_left (fun status it ->      
@@ -632,12 +663,13 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                                     ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
                            | _ -> status))
                        (* XXX *)
-                      with _ -> (*HLog.warn "error in generating inversion principle"; *)
+                      with
+                         Sys.Break as exn -> raise exn
+                       | _ -> (*HLog.warn "error in generating inversion principle"; *)
                                 let status = status#set_ng_mode `CommandMode in status)
                   status
                   (NCic.Prop::
-                    List.map (fun s -> NCic.Type s)
-                    (NCicEnvironment.get_universes ())))) status itl
+                    List.map (fun s -> NCic.Type s) universes))) status itl
               | _ -> status
            in
            let status = match nobj with
@@ -685,7 +717,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                                     ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
                            | _ -> status))
                        (* XXX *)
-                      with _ -> (*HLog.warn "error in generating discrimination principle"; *)
+                      with
+                         Sys.Break as exn -> raise exn
+                       | _ -> (*HLog.warn "error in generating discrimination principle"; *)
                                 let status = status#set_ng_mode `CommandMode in
                                 status)
                   status' itl
@@ -881,8 +915,13 @@ let rec eval_executable ~include_paths opts status (text,prefix_len,ex) =
        let status =
         List.fold_left 
           (fun status tac ->
+            let time0 = Unix.gettimeofday () in
             let status = eval_ng_tac (text,prefix_len,tac) status in
-            subst_metasenv_and_fix_names status)
+            let time3 = Unix.gettimeofday () in
+            HLog.debug ("... eval_ng_tac done in " ^ string_of_float (time3 -. time0) ^ "s");
+            let status = subst_metasenv_and_fix_names status in
+            let time3 = Unix.gettimeofday () in
+            HLog.debug ("... subst_metasenv_and_fix_names done in " ^ string_of_float (time3 -. time0) ^ "s"); status)
           status tacl
        in
         status