X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=9fbcd94729d34b7700c226cea4446fe018e0a66f;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=a4942aa07f690017643a88e21ba859a6c77107cf;hpb=789be8e12d78acc622fc9a115c592fa42b8fa3d1;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index a4942aa07..9fbcd9472 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -55,7 +55,7 @@ let inject_unification_hint =
 
 let eval_unification_hint status t n = 
  let metasenv,subst,status,t =
-  GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
+  GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst status subst [] t in
  let status = basic_eval_unification_hint (t,n) status in
@@ -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
@@ -512,7 +540,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        let o_t = NotationPt.Ident (name,None) in
        let metasenv,subst, status,t =
          GrafiteDisambiguate.disambiguate_nterm 
-           status None [] [] [] ("",0,o_t) in
+           status `XTNone [] [] [] ("",0,o_t) in
        assert( metasenv = [] && subst = []);
        let ty = NCicTypeChecker.typeof status [] [] [] t in
        let source, target =
@@ -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
@@ -608,7 +637,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        (*prerr_endline (status#ppobj obj);*)
            let boxml = NCicElim.mk_elims status obj in
            let boxml = boxml @ NCicElim.mk_projections status obj in
-           let status = status#set_ng_mode `CommandMode in
+	   let status = status#set_ng_mode `CommandMode in
            let xxaliases = GrafiteDisambiguate.aliases_for_objs status [uri] in
            let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
            let status = eval_alias status (mode,xxaliases) in
@@ -629,9 +658,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                 else
                   nstatus
                with
-               | MultiPassDisambiguator.DisambiguationError _
+               | MultiPassDisambiguator.DisambiguationError _ as e ->
+                  HLog.warn "error in disambiguating projection/eliminator";
+                  status
                | NCicTypeChecker.TypeCheckerFailure _ ->
-                  (*HLog.warn "error in generating projection/eliminator";*)
+                  HLog.warn "error in typechecking projection/eliminator";
                   status
              ) status boxml in             
            let _,_,_,_,nobj = obj in
@@ -739,7 +770,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              (fun status (name,cpos,arity) ->
                try
                  let metasenv,subst,status,t =
-                  GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+                  GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] []
                    ("",0,NotationPt.Ident (name,None)) in
                  assert (metasenv = [] && subst = []);
                  let status, nuris = 
@@ -747,6 +778,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);
@@ -813,14 +851,14 @@ 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 None [] [] [] (text,prefix_len,indty) in
+          GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] (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
           | _ -> 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
@@ -834,7 +872,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       let metasenv,subst,status,sort = match sort with
         | None -> [],[],status,NCic.Sort NCic.Prop
         | Some s ->
-           GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+           GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] []
             (text,prefix_len,s) 
       in
       assert (metasenv = []);
@@ -848,7 +886,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              (status#ppterm ~metasenv ~subst ~context:[] sort))) in
       let status = status#set_ng_mode `ProofMode in
       let metasenv,subst,status,indty =
-       GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
+       GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] subst
         (text,prefix_len,indty) in
       let indtyno,(_,leftno,tys,_,_) =
        match indty with