X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=f76b8b02a802e80a406e1d9b8321c47b5e2b9087;hb=b6ceb877c05d27705ef163488aee38e60a86886c;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..f76b8b02a 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,60 @@ 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 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 + ~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 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 @@ -326,7 +380,7 @@ let index_eq_for_auto status uri = ;; let inject_constraint = - let basic_eval_add_constraint (u1,u2) + let basic_eval_add_constraint (acyclic,u1,u2) ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status = @@ -336,7 +390,7 @@ let inject_constraint = (* NCicLibrary.add_constraint adds the constraint to the NCicEnvironment * and also to the storage (for undo/redo). During inclusion of compiled * files the storage must not be touched. *) - NCicEnvironment.add_lt_constraint u1 u2; + NCicEnvironment.add_lt_constraint acyclic u1 u2; status else status @@ -344,9 +398,9 @@ let inject_constraint = GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint ;; -let eval_add_constraint status u1 u2 = - let status = NCicLibrary.add_constraint status u1 u2 in - NCicLibrary.dump_obj status (inject_constraint (u1,u2)) +let eval_add_constraint status acyclic u1 u2 = + let status = NCicLibrary.add_constraint status acyclic u1 u2 in + NCicLibrary.dump_obj status (inject_constraint (acyclic,u1,u2)) ;; let eval_ng_tac tac = @@ -427,6 +481,7 @@ let eval_ng_tac tac = NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l) |GrafiteAst.NRepeat (_,tac) -> NTactics.repeat_tac (f f (text, prefix_len, tac)) + |GrafiteAst.Assume (_,id,t) -> Declarative.assume id t in aux aux tac (* trick for non uniform recursion call *) ;; @@ -495,6 +550,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 @@ -504,15 +567,18 @@ 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 = 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 = @@ -533,17 +599,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) @@ -582,6 +646,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 + let status = eval_extract_ocaml_obj status obj in (try let index_obj = index && match obj_kind with @@ -598,6 +664,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 @@ -608,7 +677,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 +698,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = else nstatus with - | MultiPassDisambiguator.DisambiguationError _ + | MultiPassDisambiguator.DisambiguationError _ -> + 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 +810,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 +818,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 = extract_uris status nuris in eval_alias status (mode,aliases) with MultiPassDisambiguator.DisambiguationError _-> HLog.warn ("error in generating coercion: "^name); @@ -813,14 +885,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 `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 | _ -> 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 +906,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 +920,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 @@ -868,8 +940,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) | _ -> assert false) - | GrafiteAst.NUnivConstraint (loc,u1,u2) -> - eval_add_constraint status [`Type,u1] [`Type,u2] + | GrafiteAst.NUnivConstraint (loc,acyclic,u1,u2) -> + eval_add_constraint status acyclic [`Type,u1] [`Type,u2] (* ex lexicon commands *) | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) -> let cic_appl_pattern =