X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=e96790860618ea0f2d7dbd5174d3ed3ad49397eb;hb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;hp=f3c4c5a22c2f350f5c2810a71cadf26566bb63eb;hpb=f68f58e17f9be1d3760dd79064fb950d1aa885e1;p=helm.git diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index f3c4c5a22..e96790860 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -25,9 +25,7 @@ (* $Id$ *) -exception Drop (* mo file name, ma file name *) -exception IncludedFileNotCompiled of string * string exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a @@ -36,62 +34,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 -;; - -type eval_ast = - {ea_go: - 'term 'lazy_term 'reduction 'obj 'ident. - - disambiguate_command: - (GrafiteTypes.status -> - (GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * GrafiteAst.command) -> - - ?do_heavy_checks:bool -> - GrafiteTypes.status -> - 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 -> GrafiteAst.command disambiguator_input -> - GrafiteTypes.status * GrafiteAst.command) -> - options -> GrafiteTypes.status -> - 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 -> GrafiteAst.command disambiguator_input -> - GrafiteTypes.status * GrafiteAst.command) -> - options -> GrafiteTypes.status -> 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 -> - GrafiteAst.command disambiguator_input -> - GrafiteTypes.status * GrafiteAst.command) -> - - options -> - GrafiteTypes.status -> 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 basic_eval_unification_hint (t,n) status = NCicUnifHint.add_user_provided_hint status t n ;; @@ -103,10 +45,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 = @@ -117,7 +57,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 = @@ -140,10 +80,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 = @@ -224,10 +161,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 = @@ -256,17 +190,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,`New [] + status,[] ;; let eval_ng_tac tac = @@ -360,8 +291,18 @@ let subst_metasenv_and_fix_names status = ;; -let rec eval_ncommand opts status (text,prefix_len,cmd) = +let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = match cmd with + | GrafiteAst.Include (loc, mode, fname) -> + let _root, baseuri, _fullpath, _rrelpath = + Librarian.baseuri_of_script ~include_paths fname in + let status,obj = + GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) + status in + let status = status#set_dump (obj::status#dump) in + assert false (* mode must be passed to GrafiteTypes.Serializer.require + somehow *) + status,[] | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n | GrafiteAst.NCoercion (loc, name, t, ty, source, target) -> NCicCoercDeclaration.eval_ncoercion status name t ty source target @@ -397,7 +338,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 = @@ -435,28 +375,29 @@ 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 -> try let nstatus,nuris = - eval_ncommand opts status + eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml)) in 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],_) -> @@ -472,8 +413,9 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = is_ind it leftno outsort status status#baseuri in let _,_,menv,_,_ = invobj in fst (match menv with - [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) - | _ -> status,`New [])) + [] -> eval_ncommand ~include_paths opts status + ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + | _ -> status,[])) (* XXX *) with _ -> (*HLog.warn "error in generating inversion principle"; *) let status = status#set_ng_mode `CommandMode in status) @@ -504,7 +446,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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); @@ -546,7 +488,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let status = status#set_stack ninitial_stack in let status = subst_metasenv_and_fix_names status in let status = status#set_ng_mode `ProofMode in - eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | GrafiteAst.NObj (loc,obj) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") @@ -562,8 +504,8 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let status = status#set_ng_mode `ProofMode in (match nmenv with [] -> - eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) - | _ -> status,`New []) + eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + | _ -> status,[]) | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") @@ -579,9 +521,9 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let status,obj = NDestructTac.mk_discriminator it status in let _,_,menv,_,_ = obj in (match menv with - [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + [] -> eval_ncommand ~include_paths 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") @@ -611,46 +553,99 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let _,_,menv,_,_ = obj in (match menv with [] -> - eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | _ -> assert false) | GrafiteAst.NUnivConstraint (loc,u1,u2) -> 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 status,uris = - match cmd with - | GrafiteAst.Include (loc, baseuri) -> + (* ex lexicon commands *) + | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) -> + let rec disambiguate = + function + NotationPt.ApplPattern l -> + NotationPt.ApplPattern (List.map disambiguate l) + | NotationPt.VarPattern id + when not + (List.exists + (function (NotationPt.IdentArg (_,id')) -> id'=id) args) + -> + let item = DisambiguateTypes.Id id in + begin try + match DisambiguateTypes.Environment.find item status#lstatus.LexiconTypes.aliases with + GrafiteAst.Ident_alias (_, uri) -> + NotationPt.NRefPattern (NReference.reference_of_string uri) + | _ -> assert false + with Not_found -> + prerr_endline + ("LexiconEngine.eval_command: domain item not found: " ^ + (DisambiguateTypes.string_of_domain_item item)); + LexiconEngine.dump_aliases prerr_endline "" status; + raise + (Failure + ((DisambiguateTypes.string_of_domain_item item) ^ " not found")) + end + | p -> p + in + let cic_appl_pattern = disambiguate cic_appl_pattern in let status = - 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)) + Interpretations.add_interpretation status + dsc (symbol, args) cic_appl_pattern in + let mode = assert false in (* VEDI SOTTO *) + let diff = + [DisambiguateTypes.Symbol (symbol, 0), + GrafiteAst.Symbol_alias (symbol,0,dsc)] in + let status = LexiconEngine.set_proof_aliases status mode diff in + assert false (* MANCA SALVATAGGIO SU DISCO CHE DEVE TENERE IN CONTO + IL MODE WithPreference/WithOutPreferences*) + | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) -> + let l1 = + CicNotationParser.check_l1_pattern + l1 (dir = Some `RightToLeft) precedence associativity in - eval_from_moo.efm_go status moopath - in let status = - NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) - status in + if dir <> Some `RightToLeft then + CicNotationParser.extend status l1 + (fun env loc -> + NotationPt.AttributedTerm + (`Loc loc,TermContentPres.instantiate_level2 env l2)) + else status + in let status = - GrafiteTypes.add_moo_content - [GrafiteAst.Include (loc,baseuri)] status + if dir <> Some `LeftToRight then + let status = TermContentPres.add_pretty_printer status l2 l1 in + status + else + status in - status,`New [] - | GrafiteAst.Print (_,_) -> status,`New [] - | GrafiteAst.Set (loc, name, value) -> status, `New [] + assert false (* MANCA SALVATAGGIO SU DISCO *) + status + | GrafiteAst.Alias (loc, spec) -> + let diff = + (*CSC: Warning: this code should be factorized with the corresponding + code in DisambiguatePp *) + match spec with + | GrafiteAst.Ident_alias (id,uri) -> + [DisambiguateTypes.Id id,spec] + | GrafiteAst.Symbol_alias (symb, instance, desc) -> + [DisambiguateTypes.Symbol (symb,instance),spec] + | GrafiteAst.Number_alias (instance,desc) -> + [DisambiguateTypes.Num instance,spec] + in + let mode = assert false in (* VEDI SOPRA *) + LexiconEngine.set_proof_aliases status mode diff; + assert false (* MANCA SALVATAGGIO SU DISCO *) +;; + +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.Print (_,_) -> status,[] + | GrafiteAst.Set (loc, name, value) -> status, [] in status,uris -} and eval_executable = {ee_go = fun ~disambiguate_command - opts status (text,prefix_len,ex) -> +and eval_executable ~include_paths opts status (text,prefix_len,ex) = match ex with | GrafiteAst.NTactic (_(*loc*), tacl) -> if status#ng_mode <> `ProofMode then @@ -663,47 +658,20 @@ 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) + eval_ncommand ~include_paths opts status (text,prefix_len,cmd) | 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) - status ast - in - assert (lemmas=`New []); - status) - status moo -} and eval_ast = {ea_go = fun ~disambiguate_command -?(do_heavy_checks=false) status -(text,prefix_len,st) --> +and eval_ast ~include_paths ?(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 - opts status (text,prefix_len,ex) + eval_executable ~include_paths 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, `New [] -} + eval_comment opts status (text,prefix_len,c) ;; - - -let eval_ast = eval_ast.ea_go