Bug fixed: composite coercions were not extracted.

[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 9fbcd94729d34b7700c226cea4446fe018e0a66f..54850f1126b707ca0d765809fea7573d0fe4b0e9 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -286,6 +286,15 @@ let basic_extract_obj obj status =
   | exn -> prerr_endline ("EXTRACTION FAILURE: " ^ Printexc.to_string exn); assert false
 ;;
 
+let basic_extract_ocaml_obj obj status =
+ try
+  let status  = OcamlExtraction.print_ocaml_of_obj status obj in
+  let infos,status = status#get_info in
+   status,infos
+ with
+  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
@@ -298,11 +307,28 @@ let inject_extract_obj =
   GrafiteTypes.Serializer.register#run "extraction" basic_extract_obj
 ;;
 
+let inject_extract_ocaml_obj =
+ let basic_extract_ocaml_obj info
+   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+   ~alias_only status
+ =
+  let info= OcamlExtractionTable.refresh_uri_in_info ~refresh_uri_in_reference ~refresh_uri:NCicLibrary.refresh_uri info in
+   status#set_ocaml_extraction_db
+    (OcamlExtractionTable.register_infos status#ocaml_extraction_db info)
+ in
+  GrafiteTypes.Serializer.register#run "ocaml_extraction" basic_extract_ocaml_obj
+;;
+
 let eval_extract_obj status obj = 
  let status,infos = basic_extract_obj obj status in
   NCicLibrary.dump_obj status (inject_extract_obj infos)
 ;;
 
+let eval_extract_ocaml_obj status obj = 
+ let status,infos = basic_extract_ocaml_obj obj status in
+  NCicLibrary.dump_obj status (inject_extract_ocaml_obj infos)
+;;
+
 (*
 module EmptyC = 
   struct
@@ -523,6 +549,14 @@ let compute_relevance status uri =
       NCic.Inductive (ind,leftno,tys,attrs)
 ;;
 
+let extract_uris status uris =
+ List.fold_left
+  (fun status uri ->
+    let obj = NCicEnvironment.get_checked_obj status uri in
+     let status = eval_extract_obj status obj in
+      eval_extract_ocaml_obj status obj
+  ) status uris
+;;
 
 let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
   match cmd with
@@ -532,8 +566,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
      let baseuri = NUri.uri_of_string baseuri in
      (* MATITA 1.0: keep WithoutPreferences? *)
      let alias_only = (mode = GrafiteAst.OnlyPreferences) in
+     let status =
       GrafiteTypes.Serializer.require
-       ~alias_only ~baseuri ~fname:fullpath status
+       ~alias_only ~baseuri ~fname:fullpath status in
+     OcamlExtraction.print_open status
+      (NCicLibrary.get_transitively_included status)
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
   | GrafiteAst.NCoercion (loc, name, compose, None) ->
      let status, t, ty, source, target =
@@ -561,17 +598,15 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        in
        status, o_t, NotationPt.NCic ty, source, target
      in
-     let status, composites =
-      NCicCoercDeclaration.eval_ncoercion status name compose t ty source
-       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)
+      let cmd = 
+       GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target))
+      in
+      eval_ncommand ~include_paths opts status (text,prefix_len,cmd)
   | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) ->
      let status, composites =
       NCicCoercDeclaration.eval_ncoercion status name compose t ty source
        target in
+     let status = extract_uris status composites in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
       eval_alias status (mode,aliases)
@@ -611,6 +646,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
         let status = eval_extract_obj status obj in
+        let status = eval_extract_ocaml_obj status obj in
        (try
         let index_obj = index &&
          match obj_kind with
@@ -658,7 +694,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                 else
                   nstatus
                with
-               | MultiPassDisambiguator.DisambiguationError _ as e ->
+               | MultiPassDisambiguator.DisambiguationError _ ->
                   HLog.warn "error in disambiguating projection/eliminator";
                   status
                | NCicTypeChecker.TypeCheckerFailure _ ->
@@ -778,13 +814,7 @@ 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
+                 let status = extract_uris status nuris in
                   eval_alias status (mode,aliases)
                with MultiPassDisambiguator.DisambiguationError _-> 
                  HLog.warn ("error in generating coercion: "^name);
@@ -851,7 +881,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       else
         let status = status#set_ng_mode `ProofMode in
         let metasenv,subst,status,indty =
-          GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] (text,prefix_len,indty) in
+          GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] [] (text,prefix_len,indty) in
         let indtyno, (_,_,tys,_,_),leftno = match indty with
             NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) ->
               indtyno, NCicEnvironment.get_checked_indtys status r, leftno