X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=00160ac81b0ad885d47fe7477ce5f94f3a3f93c5;hb=f3f6b451707a3feb8245717e3fa7ca25df0ce8ef;hp=b122366c1ea77d3d9ffb831cb7bd9651da0ba9e6;hpb=0fde70bd19b8fdfa72b807b9713a02ad1bd91b5b;p=helm.git diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index b122366c1..00160ac81 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -27,10 +27,6 @@ exception Drop (* mo file name, ma file name *) -exception IncludedFileNotCompiled of string * string -exception Macro of - GrafiteAst.loc * - (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a @@ -39,95 +35,6 @@ type options = { do_heavy_checks: bool ; } -let concat_nuris uris nuris = - match uris,nuris with - | `New uris, `New nuris -> `New (nuris@uris) - | _ -> assert false -;; -(** create a ProofEngineTypes.mk_fresh_name_type function which uses given - * names as long as they are available, then it fallbacks to name generation - * using FreshNamesGenerator module *) -let namer_of names = - let len = List.length names in - let count = ref 0 in - fun metasenv context name ~typ -> - if !count < len then begin - let name = match List.nth names !count with - | Some s -> Cic.Name s - | None -> Cic.Anonymous - in - incr count; - name - end else - FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ - -type eval_ast = - {ea_go: - 'term 'lazy_term 'reduction 'obj 'ident. - - disambiguate_command: - (GrafiteTypes.status -> - (('term,'obj) GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> - - disambiguate_macro: - (GrafiteTypes.status -> - (('term,'lazy_term) GrafiteAst.macro) disambiguator_input -> - Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) -> - - ?do_heavy_checks:bool -> - GrafiteTypes.status -> - (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) - disambiguator_input -> - GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] - } - -type 'a eval_command = - {ec_go: 'term 'obj. - disambiguate_command: - (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> - options -> GrafiteTypes.status -> - (('term,'obj) GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] - } - -type 'a eval_comment = - {ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident. - disambiguate_command: - (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> - options -> GrafiteTypes.status -> - (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input -> - GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] - } - -type 'a eval_executable = - {ee_go: 'term 'lazy_term 'reduction 'obj 'ident. - - disambiguate_command: - (GrafiteTypes.status -> - (('term,'obj) GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> - - disambiguate_macro: - (GrafiteTypes.status -> - (('term,'lazy_term) GrafiteAst.macro) disambiguator_input -> - Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) -> - - options -> - GrafiteTypes.status -> - (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input -> - GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] - } - -type 'a eval_from_moo = - { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status } - -let coercion_moo_statement_of (uri,arity, saturations,_) = - GrafiteAst.Coercion - (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations) - let basic_eval_unification_hint (t,n) status = NCicUnifHint.add_user_provided_hint status t n ;; @@ -139,10 +46,8 @@ let inject_unification_hint = = let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) in - NCicLibrary.Serializer.register#run "unification_hints" - object(_ : 'a NCicLibrary.register_type) - method run = basic_eval_unification_hint - end + GrafiteTypes.Serializer.register#run "unification_hints" + basic_eval_unification_hint ;; let eval_unification_hint status t n = @@ -153,7 +58,7 @@ let eval_unification_hint status t n = let status = basic_eval_unification_hint (t,n) status in let dump = inject_unification_hint (t,n)::status#dump in let status = status#set_dump dump in - status,`New [] + status,[] ;; let basic_index_obj l status = @@ -176,10 +81,7 @@ let record_index_obj = (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v) l) in - NCicLibrary.Serializer.register#run "index_obj" - object(_ : 'a NCicLibrary.register_type) - method run = aux - end + GrafiteTypes.Serializer.register#run "index_obj" aux ;; let compute_keys status uri height kind = @@ -260,10 +162,7 @@ let record_index_eq = ~refresh_uri_in_term = index_eq (NCicLibrary.refresh_uri uri) in - NCicLibrary.Serializer.register#run "index_eq" - object(_ : 'a NCicLibrary.register_type) - method run = basic_index_eq - end + GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq ;; let index_eq_for_auto status uri = @@ -292,68 +191,14 @@ let inject_constraint = let u2 = refresh_uri_in_universe u2 in basic_eval_add_constraint (u1,u2) in - NCicLibrary.Serializer.register#run "constraints" - object(_:'a NCicLibrary.register_type) - method run = basic_eval_add_constraint - end + GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint ;; let eval_add_constraint status u1 u2 = let status = basic_eval_add_constraint (u1,u2) status in let dump = inject_constraint (u1,u2)::status#dump in let status = status#set_dump dump in - status,`Old [] -;; - -let add_coercions_of_lemmas lemmas status = - let moo_content = - HExtlib.filter_map - (fun uri -> - match CoercDb.is_a_coercion (Cic.Const (uri,[])) with - | None -> None - | Some (_,tgt,_,sat,_) -> - let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in - Some (coercion_moo_statement_of (uri,arity,sat,0))) - lemmas - in - let status = GrafiteTypes.add_moo_content moo_content status in - status#set_coercions (CoercDb.dump ()), - lemmas - -let eval_coercion status ~add_composites uri arity saturations = - let uri = - try CicUtil.uri_of_term uri - with Invalid_argument _ -> - raise (Invalid_argument "coercion can only be constants/constructors") - in - let status, lemmas = - GrafiteSync.add_coercion ~add_composites - ~pack_coercion_obj:CicRefine.pack_coercion_obj - status uri arity saturations status#baseuri in - let moo_content = coercion_moo_statement_of (uri,arity,saturations,0) in - let status = GrafiteTypes.add_moo_content [moo_content] status in - add_coercions_of_lemmas lemmas status - -let eval_prefer_coercion status c = - let uri = - try CicUtil.uri_of_term c - with Invalid_argument _ -> - raise (Invalid_argument "coercion can only be constants/constructors") - in - let status = GrafiteSync.prefer_coercion status uri in - let moo_content = GrafiteAst.PreferCoercion (HExtlib.dummy_floc,c) in - let status = GrafiteTypes.add_moo_content [moo_content] status in - status, `Old [] - -let eval_ng_punct (_text, _prefix_len, punct) = - match punct with - | GrafiteAst.Dot _ -> NTactics.dot_tac - | GrafiteAst.Semicolon _ -> fun x -> x - | GrafiteAst.Branch _ -> NTactics.branch_tac ~force:false - | GrafiteAst.Shift _ -> NTactics.shift_tac - | GrafiteAst.Pos (_,l) -> NTactics.pos_tac l - | GrafiteAst.Wildcard _ -> NTactics.wildcard_tac - | GrafiteAst.Merge _ -> NTactics.merge_tac + status,[] ;; let eval_ng_tac tac = @@ -484,7 +329,6 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = | _ -> obj_kind in let obj = uri,height,[],[],obj_kind in - prerr_endline ("pp new obj \n"^NCicPp.ppobj obj); let old_status = status in let status = NCicLibrary.add_obj status obj in let index_obj = @@ -522,7 +366,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let uris = uri::List.rev uris_rev in *) let status = status#set_ng_mode `CommandMode in - let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in + let status = LexiconSync.add_aliases_for_objs status [uri] in let status,uris = List.fold_left (fun (status,uris) boxml -> @@ -534,16 +378,17 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = if nstatus#ng_mode <> `CommandMode then begin (*HLog.warn "error in generating projection/eliminator";*) + assert(status#ng_mode = `CommandMode); status, uris end else - nstatus, concat_nuris uris nuris + nstatus, uris@nuris with | MultiPassDisambiguator.DisambiguationError _ | NCicTypeChecker.TypeCheckerFailure _ -> (*HLog.warn "error in generating projection/eliminator";*) status,uris - ) (status,`New [] (* uris *)) boxml in + ) (status,[] (* uris *)) boxml in let _,_,_,_,nobj = obj in let status = match nobj with NCic.Inductive (is_ind,leftno,[it],_) -> @@ -560,7 +405,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let _,_,menv,_,_ = invobj in fst (match menv with [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) - | _ -> status,`New [])) + | _ -> status,[])) (* XXX *) with _ -> (*HLog.warn "error in generating inversion principle"; *) let status = status#set_ng_mode `CommandMode in status) @@ -584,14 +429,14 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = try let metasenv,subst,status,t = GrafiteDisambiguate.disambiguate_nterm None status [] [] [] - ("",0,CicNotationPt.Ident (name,None)) in + ("",0,NotationPt.Ident (name,None)) in assert (metasenv = [] && subst = []); let status, nuris = NCicCoercDeclaration. basic_eval_and_record_ncoercion_from_t_cpos_arity status (name,t,cpos,arity) in - let uris = concat_nuris nuris uris in + let uris = nuris@uris in status, uris with MultiPassDisambiguator.DisambiguationError _-> HLog.warn ("error in generating coercion: "^name); @@ -650,7 +495,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = (match nmenv with [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) - | _ -> status,`New []) + | _ -> status,[]) | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") @@ -668,7 +513,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = (match menv with [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | _ -> prerr_endline ("Discriminator: non empty metasenv"); - status, `New []) *) + status, []) *) | GrafiteAst.NInverter (loc, name, indty, selection, sort) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") @@ -704,57 +549,34 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = eval_add_constraint status [`Type,u1] [`Type,u2] ;; -let rec eval_command = {ec_go = fun ~disambiguate_command opts status -(text,prefix_len,cmd) -> - let status,cmd = disambiguate_command status (text,prefix_len,cmd) in +let eval_comment opts status (text,prefix_len,c) = status, [] + +let rec eval_command opts status (text,prefix_len,cmd) = let status,uris = match cmd with - | GrafiteAst.PreferCoercion (loc, coercion) -> - eval_prefer_coercion status coercion - | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) -> - let res,uris = - eval_coercion status ~add_composites uri arity saturations - in - res,`Old uris - | GrafiteAst.Default (loc, what, uris) as cmd -> - LibraryObjects.set_default what uris; - GrafiteTypes.add_moo_content [cmd] status,`Old [] - | GrafiteAst.Drop loc -> raise Drop - | GrafiteAst.Include (loc, mode, new_or_old, baseuri) -> - (* Old Include command is not recursive; new one is *) - let status = - if new_or_old = `OldAndNew then - let moopath_rw, moopath_r = - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true, - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:false in - let moopath = - if Sys.file_exists moopath_r then moopath_r else - if Sys.file_exists moopath_rw then moopath_rw else - raise (IncludedFileNotCompiled (moopath_rw,baseuri)) - in - eval_from_moo.efm_go status moopath - else - status - in - let status = - NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) - status in + | GrafiteAst.Include (loc, fname, mode, _) -> + let include_paths = assert false in + let never_include = assert false in + let mode = assert false in + let baseuri = assert false in let status = - GrafiteTypes.add_moo_content - [GrafiteAst.Include (loc,mode,`New,baseuri)] status + let _root, buri, fullpath, _rrelpath = + Librarian.baseuri_of_script ~include_paths fname in + if never_include then raise (GrafiteParser.NoInclusionPerformed fullpath) + else + LexiconEngine.eval_command status (LexiconAst.Include (loc,buri,mode,fullpath)) in - status,`Old [] - | GrafiteAst.Print (_,_) -> status,`Old [] - | GrafiteAst.Set (loc, name, value) -> status, `Old [] -(* GrafiteTypes.set_option status name value,[] *) - | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false + let status,obj = + GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) + status in + let status = status#set_dump (obj::status#dump) in + status,[] + | GrafiteAst.Print (_,_) -> status,[] + | GrafiteAst.Set (loc, name, value) -> status, [] in status,uris -} and eval_executable = {ee_go = fun ~disambiguate_command -~disambiguate_macro opts status (text,prefix_len,ex) -> +and eval_executable opts status (text,prefix_len,ex) = match ex with | GrafiteAst.NTactic (_(*loc*), tacl) -> if status#ng_mode <> `ProofMode then @@ -767,50 +589,19 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status subst_metasenv_and_fix_names status) status tacl in - status,`New [] + status,[] | GrafiteAst.Command (_, cmd) -> - eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd) + eval_command opts status (text,prefix_len,cmd) | GrafiteAst.NCommand (_, cmd) -> eval_ncommand opts status (text,prefix_len,cmd) - | GrafiteAst.Macro (loc, macro) -> - raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro))) | GrafiteAst.NMacro (loc, macro) -> raise (NMacro (loc,macro)) -} and eval_from_moo = {efm_go = fun status fname -> - let ast_of_cmd cmd = - ("",0,GrafiteAst.Executable (HExtlib.dummy_floc, - GrafiteAst.Command (HExtlib.dummy_floc, - cmd))) - in - let moo = GrafiteMarshal.load_moo fname in - List.fold_left - (fun status ast -> - let ast = ast_of_cmd ast in - let status,lemmas = - eval_ast.ea_go - ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd) - ~disambiguate_macro:(fun _ _ -> assert false) - status ast - in - assert (lemmas=`Old []); - status) - status moo -} and eval_ast = {ea_go = fun ~disambiguate_command -~disambiguate_macro ?(do_heavy_checks=false) status -(text,prefix_len,st) --> +and eval_ast ?(do_heavy_checks=false) status (text,prefix_len,st) = let opts = { do_heavy_checks = do_heavy_checks ; } in match st with | GrafiteAst.Executable (_,ex) -> - eval_executable.ee_go ~disambiguate_command - ~disambiguate_macro opts status (text,prefix_len,ex) + eval_executable opts status (text,prefix_len,ex) | GrafiteAst.Comment (_,c) -> - eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c) -} and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) -> - status, `Old [] -} + eval_comment opts status (text,prefix_len,c) ;; - - -let eval_ast = eval_ast.ea_go