+++ /dev/null
-(* 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
-
projects / helm.git / blobdiff