X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=15e20277f6f1ad5cb6d132c76686671f14512716;hb=3d981fb10ebc350bc3fc693f0a433d51fc35715a;hp=b1e0f4c8538061afb2a78648406c3c285f24699f;hpb=48a9ef28943252488e7138a8f570eef965744ee3;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index b1e0f4c85..15e20277f 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,75 @@ let index_obj_for_auto status (uri, height, _, _, kind) =
    NCicLibrary.dump_obj status (record_index_obj data)
 ;; 
 
-let index_eq uri status =
+let basic_extract_obj obj status =
+ try
+  ignore (Helm_registry.get "extract_haskell");
+  let status,(msg,infos) = NCicExtraction.haskell_of_obj status obj in
+   prerr_endline msg;
+   status,infos
+ with
+    Helm_registry.Key_not_found _ -> status,NCicExtraction.empty_info
+  | exn -> prerr_endline ("EXTRACTION FAILURE: " ^ Printexc.to_string exn); assert false
+;;
+
+let inject_extract_obj =
+ let basic_extract_obj info
+   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+   ~alias_only status
+ =
+  let info= NCicExtraction.refresh_uri_in_info ~refresh_uri_in_reference info in
+   status#set_extraction_db
+    (NCicExtraction.register_infos status#extraction_db info)
+ in
+  GrafiteTypes.Serializer.register#run "extraction" basic_extract_obj
+;;
+
+let eval_extract_obj status obj = 
+ let status,infos = basic_extract_obj obj status in
+  NCicLibrary.dump_obj status (inject_extract_obj infos)
+;;
+
+(*
+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 +545,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 +610,8 @@ 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
+        let status = eval_extract_obj status obj in
+       (try
         let index_obj = index &&
          match obj_kind with
             NCic.Constant (_,_,_,_,(_,`Example,_))
@@ -563,7 +622,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 +634,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
@@ -587,7 +647,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                try
                 let nstatus =
                  eval_ncommand ~include_paths opts status
-                  ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
+                  ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml,true))
                 in
                 if nstatus#ng_mode <> `CommandMode then
                   begin
@@ -603,7 +663,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 +692,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 +746,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
@@ -704,6 +776,13 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
                       status (name,true,t,cpos,arity) in
                  let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
+                 let status =
+                  List.fold_left
+                   (fun status uri ->
+                     let obj = NCicEnvironment.get_checked_obj status uri in
+                      eval_extract_obj status obj
+                   ) status nuris
+                 in
                   eval_alias status (mode,aliases)
                with MultiPassDisambiguator.DisambiguationError _-> 
                  HLog.warn ("error in generating coercion: "^name);
@@ -746,7 +825,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        let status = subst_metasenv_and_fix_names status in
        let status = status#set_ng_mode `ProofMode in
        eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
-  | GrafiteAst.NObj (loc,obj) ->
+  | GrafiteAst.NObj (loc,obj,index) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")
      else
@@ -761,7 +840,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       let status = status#set_ng_mode `ProofMode in
       (match nmenv with
           [] ->
-           eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,true))
+           eval_ncommand ~include_paths opts status
+             ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,index))
         | _ -> status)
   | GrafiteAst.NDiscriminator (loc, indty) ->
       if status#ng_mode <> `CommandMode then
@@ -776,7 +856,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
           | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
         let (_,ind_name,_,_ as it) = List.nth tys indtyno in
         let status,obj =  
-          NDestructTac.mk_discriminator ~use_jmeq:true (ind_name ^ "_jmdiscr")
+          NDestructTac.mk_discriminator ~use_jmeq:true ~force:true (ind_name ^ "_jmdiscr")
            it leftno status status#baseuri in
         let _,_,menv,_,_ = obj in
           (match menv with
@@ -871,8 +951,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