X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconEngine.ml;h=22d9b2f33a703ce7357f598cd16af11a62626220;hb=c04f852241510515f06e3bec8eb79acac6e4952e;hp=34e314edcd128b13ae820f1e393ea5df5801c49f;hpb=b95be966e385957a25f26a41f45e0116955264ae;p=helm.git diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index 34e314edc..22d9b2f33 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -25,15 +25,19 @@ (* $Id$ *) -exception IncludedFileNotCompiled of string (* file name *) +let out = ref ignore + +let set_callback f = out := f + +(* lexicon file name * ma file name *) +exception IncludedFileNotCompiled of string * string exception MetadataNotFound of string (* file name *) type status = { - aliases: DisambiguateTypes.environment; (** disambiguation aliases *) - multi_aliases: DisambiguateTypes.multiple_environment; + aliases: LexiconAst.alias_spec DisambiguateTypes.Environment.t; + multi_aliases: LexiconAst.alias_spec list DisambiguateTypes.Environment.t; lexicon_content_rev: LexiconMarshal.lexicon; notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) - metadata: LibraryNoDb.metadata list; } let initial_status = { @@ -41,81 +45,90 @@ let initial_status = { multi_aliases = DisambiguateTypes.Environment.empty; lexicon_content_rev = []; notation_ids = []; - metadata = []; } let add_lexicon_content cmds status = let content = status.lexicon_content_rev in let content' = List.fold_right - (fun cmd acc -> cmd :: (List.filter ((<>) cmd) acc)) + (fun cmd acc -> + match cmd with + | LexiconAst.Alias _ + | LexiconAst.Include _ + | LexiconAst.Notation _ -> cmd :: (List.filter ((<>) cmd) acc) + | LexiconAst.Interpretation _ -> if List.exists ((=) cmd) acc then acc else cmd::acc) cmds content in (* prerr_endline ("new lexicon content: " ^ String.concat " " (List.map LexiconAstPp.pp_command content')); *) { status with lexicon_content_rev = content' } -let add_metadata new_metadata status = - if Helm_registry.get_bool "db.nodb" then - let metadata = status.metadata in - let metadata' = - List.fold_left - (fun acc m -> - match m with - | LibraryNoDb.Dependency buri -> - if List.exists (LibraryNoDb.eq_metadata m) metadata - then acc - else m :: acc) - metadata new_metadata - in - { status with metadata = metadata' } - else - status - let set_proof_aliases mode status new_aliases = if mode = LexiconAst.WithoutPreferences then status else let commands_of_aliases = List.map - (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias)) - in - let deps_of_aliases = - HExtlib.filter_map - (function - | LexiconAst.Ident_alias (_, suri) -> - let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in - Some (LibraryNoDb.Dependency buri) - | _ -> None) + (fun _,alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias)) in let aliases = List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) status.aliases new_aliases in let multi_aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc) - status.multi_aliases new_aliases in + List.fold_left (fun acc (d,c) -> + DisambiguateTypes.Environment.cons LexiconAst.description_of_alias + d c acc) + status.multi_aliases new_aliases + in let new_status = { status with multi_aliases = multi_aliases ; aliases = aliases} in if new_aliases = [] then new_status else - let aliases = - DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases - in let status = - add_lexicon_content (commands_of_aliases aliases) new_status + add_lexicon_content (commands_of_aliases new_aliases) new_status in - let status = add_metadata (deps_of_aliases aliases) status in status let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = + let cmd = + match cmd with + | LexiconAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) -> + let rec disambiguate = + function + CicNotationPt.ApplPattern l -> + CicNotationPt.ApplPattern (List.map disambiguate l) + | CicNotationPt.VarPattern id + when not + (List.exists + (function (CicNotationPt.IdentArg (_,id')) -> id'=id) args) + -> + let item = DisambiguateTypes.Id id in + (try + let uri = + match DisambiguateTypes.Environment.find item status.aliases with + LexiconAst.Ident_alias (_, uri)-> UriManager.uri_of_string uri + | _ -> assert false + in + CicNotationPt.UriPattern uri + with Not_found -> + prerr_endline ("Domain item not found: " ^ + (DisambiguateTypes.string_of_domain_item item)); + assert false) + | p -> p + in + LexiconAst.Interpretation + (loc, dsc, (symbol, args), disambiguate cic_appl_pattern) + | _-> cmd + in + !out cmd; let notation_ids' = CicNotation.process_notation cmd in let status = { status with notation_ids = notation_ids' @ status.notation_ids } in match cmd with - | LexiconAst.Include (loc, baseuri, mode) -> + | LexiconAst.Include (loc, baseuri, mode, fullpath) -> let lexiconpath_rw, lexiconpath_r = LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~writable:true ~baseuri, @@ -125,56 +138,39 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = let lexiconpath = if Sys.file_exists lexiconpath_rw then lexiconpath_rw else if Sys.file_exists lexiconpath_r then lexiconpath_r else - raise (IncludedFileNotCompiled lexiconpath_rw) + raise (IncludedFileNotCompiled (lexiconpath_rw,fullpath)) in let lexicon = LexiconMarshal.load_lexicon lexiconpath in let status = List.fold_left (eval_command ~mode) status lexicon in - if Helm_registry.get_bool "db.nodb" then - let metadatapath_rw, metadatapath_r = - LibraryMisc.metadata_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true, - LibraryMisc.metadata_file_of_baseuri - ~must_exist:false ~baseuri ~writable:false - in - let metadatapath = - if Sys.file_exists metadatapath_rw then metadatapath_rw else - if Sys.file_exists metadatapath_r then metadatapath_r else - raise (MetadataNotFound metadatapath_rw) - in - add_metadata (LibraryNoDb.load_metadata ~fname:metadatapath) status - else - status + status | LexiconAst.Alias (loc, spec) -> let diff = (*CSC: Warning: this code should be factorized with the corresponding code in DisambiguatePp *) match spec with | LexiconAst.Ident_alias (id,uri) -> - [DisambiguateTypes.Id id, - (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))] + [DisambiguateTypes.Id id,spec] | LexiconAst.Symbol_alias (symb, instance, desc) -> - [DisambiguateTypes.Symbol (symb,instance), - DisambiguateChoices.lookup_symbol_by_dsc symb desc] + [DisambiguateTypes.Symbol (symb,instance),spec] | LexiconAst.Number_alias (instance,desc) -> - [DisambiguateTypes.Num instance, - DisambiguateChoices.lookup_num_by_dsc desc] + [DisambiguateTypes.Num instance,spec] in set_proof_aliases mode status diff - | LexiconAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm -> + | LexiconAst.Interpretation (_, dsc, (symbol, _), _) as stm -> let status = add_lexicon_content [stm] status in - let uris = - List.map - (fun uri -> LibraryNoDb.Dependency (UriManager.buri_of_uri uri)) - (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern) - in let diff = - [DisambiguateTypes.Symbol (symbol, 0), - DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] + try + [DisambiguateTypes.Symbol (symbol, 0), + LexiconAst.Symbol_alias (symbol,0,dsc)] + with + DisambiguateChoices.Choice_not_found msg -> + prerr_endline (Lazy.force msg); + assert false in let status = set_proof_aliases mode status diff in - let status = add_metadata uris status in status - | LexiconAst.Notation _ as stm -> add_lexicon_content [stm] status + | LexiconAst.Notation _ as stm -> + add_lexicon_content [stm] status let eval_command = eval_command ?mode:None