Composite coercions are now extracted too.

[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 bd0fd6ceac3faa2b7afa82011b96396bb88a4983..5891698404d4661e9b4f83fa631b539f684f6055 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -275,6 +275,34 @@ let index_obj_for_auto status (uri, height, _, _, kind) =
    NCicLibrary.dump_obj status (record_index_obj data)
 ;; 
 
+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
@@ -582,6 +610,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
+        let status = eval_extract_obj status obj in
        (try
         let index_obj = index &&
          match obj_kind with
@@ -634,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 ->      
@@ -654,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
@@ -707,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
@@ -735,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);
@@ -903,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