X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Flexicon%2FlexiconEngine.ml;fp=helm%2Focaml%2Flexicon%2FlexiconEngine.ml;h=aec759c964d64d3b3d00f9ea92d87c73d42a5445;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hp=0000000000000000000000000000000000000000;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953;p=helm.git diff --git a/helm/ocaml/lexicon/lexiconEngine.ml b/helm/ocaml/lexicon/lexiconEngine.ml new file mode 100644 index 000000000..aec759c96 --- /dev/null +++ b/helm/ocaml/lexicon/lexiconEngine.ml @@ -0,0 +1,150 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id$ *) + +exception IncludedFileNotCompiled of string (* file name *) +exception MetadataNotFound of string (* file name *) + +type status = { + aliases: DisambiguateTypes.environment; (** disambiguation aliases *) + multi_aliases: DisambiguateTypes.multiple_environment; + lexicon_content_rev: LexiconMarshal.lexicon; + notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) + metadata: LibraryNoDb.metadata list; +} + +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)) + 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 status new_aliases = + 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) + 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 + 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 in + let status = add_metadata (deps_of_aliases aliases) status in + status + +let rec eval_command status cmd = + let notation_ids' = CicNotation.process_notation cmd in + let status = + { status with notation_ids = notation_ids' @ status.notation_ids } in + let basedir = Helm_registry.get "matita.basedir" in + match cmd with + | LexiconAst.Include (loc, baseuri) -> + let lexiconpath = LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri in + if not (Sys.file_exists lexiconpath) then + raise (IncludedFileNotCompiled lexiconpath); + let lexicon = LexiconMarshal.load_lexicon lexiconpath in + let status = List.fold_left eval_command status lexicon in + if Helm_registry.get_bool "db.nodb" then + let metadatapath = LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in + if not (Sys.file_exists metadatapath) then + raise (MetadataNotFound metadatapath) + else + add_metadata (LibraryNoDb.load_metadata ~fname:metadatapath) status + else + 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)))] + | LexiconAst.Symbol_alias (symb, instance, desc) -> + [DisambiguateTypes.Symbol (symb,instance), + DisambiguateChoices.lookup_symbol_by_dsc symb desc] + | LexiconAst.Number_alias (instance,desc) -> + [DisambiguateTypes.Num instance, + DisambiguateChoices.lookup_num_by_dsc desc] + in + set_proof_aliases status diff + | LexiconAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) 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] + in + let status = set_proof_aliases status diff in + let status = add_metadata uris status in + status + | LexiconAst.Notation _ as stm -> add_lexicon_content [stm] status +