X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=a4942aa07f690017643a88e21ba859a6c77107cf;hb=526b5e543ec56038010eba48b4a78094bcff5fa2;hp=c5e2919599146b82fb559213a1ce199249658347;hpb=f5b9e1d5511a13ca5bb424c149781087aa0c8e31;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index c5e291959..a4942aa07 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -62,7 +62,7 @@ let eval_unification_hint status t n =
   NCicLibrary.dump_obj status (inject_unification_hint (t,n))
 ;;
 
-let basic_index_obj l status =
+let basic_index_obj l (status:#NCic.status) =
   status#set_auto_cache 
     (List.fold_left
       (fun t (ks,v) -> 
@@ -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));*)
@@ -495,19 +517,26 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        let ty = NCicTypeChecker.typeof status [] [] [] t in
        let source, target =
          let clean = function
-         | NCic.Appl (NCic.Const _ as r :: l) -> 
-             NotationPt.Appl (NotationPt.NCic r ::
-               List.map (fun _ -> NotationPt.Implicit `JustOne)l)
-         | NCic.Const _ as r -> NotationPt.NCic r
-         | _ -> assert false in
+           | NCic.Appl (NCic.Const _ as r :: l) -> 
+               NotationPt.Appl (NotationPt.NCic r ::
+                 List.map (fun _ -> NotationPt.Implicit `JustOne)l)
+           | NCic.Const _ as r -> NotationPt.NCic r
+           | NCic.Sort _ as r -> NotationPt.NCic r (* FG: missing case *)
+	   | _ -> assert false
+	 in
          let rec aux = function
-         | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest
-         | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt
-         | _ -> assert false in aux ty in
-       status, o_t, NotationPt.NCic ty, source, target in
+           | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest
+           | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt
+           | _ -> assert false
+	 in
+	 aux ty
+       in
+       status, o_t, NotationPt.NCic ty, source, target
+     in
      let status, composites =
       NCicCoercDeclaration.eval_ncoercion status name compose t ty source
-       target in
+       target
+     in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
       eval_alias status (mode,aliases)
@@ -553,6 +582,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
         let obj = uri,height,[],[],obj_kind in
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
+       (try
         let index_obj = index &&
          match obj_kind with
             NCic.Constant (_,_,_,_,(_,`Example,_))
@@ -563,7 +593,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
          if index_obj then
           let status = index_obj_for_auto status obj in
            (try index_eq_for_auto status uri
-           with _ -> status)
+           with
+              Sys.Break as exn -> raise exn
+            | _ -> status)
          else
           status in
 (*
@@ -573,7 +605,6 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
 	in *)
 (*         prerr_endline (status#ppobj obj); *)
         HLog.message ("New object: " ^ NUri.string_of_uri uri);
-         (try
        (*prerr_endline (status#ppobj obj);*)
            let boxml = NCicElim.mk_elims status obj in
            let boxml = boxml @ NCicElim.mk_projections status obj in
@@ -603,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 ->      
@@ -623,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
@@ -676,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
@@ -872,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