X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=5086eb845c6424574c565f8471ecc96b216bac14;hb=21679cd1397d9c51519dbe439c29c1683b91ec64;hp=9fbcd94729d34b7700c226cea4446fe018e0a66f;hpb=f7da48c844105a52a705872dfa0d4104de010c82;p=helm.git diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 9fbcd9472..5086eb845 100644 --- 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 @@ -627,6 +663,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = | _ -> status) else status in + (* purge tinycals stack *) + let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in + let status = status#set_stack ninitial_stack in (* try index_eq uri status @@ -658,7 +697,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 +817,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 +884,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