1 (* Copyright (C) 2004-2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
32 (* lexicon file name * ma file name *)
33 exception IncludedFileNotCompiled of string * string
34 exception MetadataNotFound of string (* file name *)
37 aliases: L.alias_spec DisambiguateTypes.Environment.t;
38 multi_aliases: L.alias_spec list DisambiguateTypes.Environment.t;
39 lexicon_content_rev: LexiconMarshal.lexicon;
40 notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
43 let dump_aliases out msg status =
44 out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
45 DisambiguateTypes.Environment.iter
46 (fun _ x -> out (LexiconAstPp.pp_alias x))
49 let initial_status = {
50 aliases = DisambiguateTypes.Environment.empty;
51 multi_aliases = DisambiguateTypes.Environment.empty;
52 lexicon_content_rev = [];
56 let add_lexicon_content cmds status =
57 let content = status.lexicon_content_rev in
64 | L.Notation _ -> cmd :: (List.filter ((<>) cmd) acc)
65 | L.Interpretation _ -> if List.exists ((=) cmd) acc then acc else cmd::acc)
69 prerr_endline ("new lexicon content: " ^
70 String.concat "; " (List.map LexiconAstPp.pp_command content')
73 { status with lexicon_content_rev = content' }
75 let set_proof_aliases mode status new_aliases =
76 if mode = L.WithoutPreferences then
79 let commands_of_aliases =
81 (fun _,alias -> L.Alias (HExtlib.dummy_floc, alias))
84 List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
85 status.aliases new_aliases in
87 List.fold_left (fun acc (d,c) ->
88 DisambiguateTypes.Environment.cons L.description_of_alias
90 status.multi_aliases new_aliases
93 { status with multi_aliases = multi_aliases ; aliases = aliases}
95 if new_aliases = [] then
99 add_lexicon_content (commands_of_aliases new_aliases) new_status
104 let rec eval_command ?(mode=L.WithPreferences) status cmd =
106 let bmode = match mode with L.WithPreferences -> true | _ -> false in
107 Printf.eprintf "Include preferences: %b\n" bmode;
111 | L.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
112 let rec disambiguate =
114 CicNotationPt.ApplPattern l ->
115 CicNotationPt.ApplPattern (List.map disambiguate l)
116 | CicNotationPt.VarPattern id
119 (function (CicNotationPt.IdentArg (_,id')) -> id'=id) args)
121 let item = DisambiguateTypes.Id id in
123 match DisambiguateTypes.Environment.find item status.aliases with
124 L.Ident_alias (_, uri) ->
126 CicNotationPt.NRefPattern
127 (NReference.reference_of_string uri)
129 NReference.IllFormedReference _ ->
130 CicNotationPt.UriPattern (UriManager.uri_of_string uri))
133 prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^
134 (DisambiguateTypes.string_of_domain_item item));
135 dump_aliases prerr_endline "" status;
141 (loc, dsc, (symbol, args), disambiguate cic_appl_pattern)
144 let notation_ids' = CicNotation.process_notation cmd in
146 { status with notation_ids = notation_ids' @ status.notation_ids } in
148 | L.Include (loc, baseuri, mode, fullpath) ->
149 let lexiconpath_rw, lexiconpath_r =
150 LibraryMisc.lexicon_file_of_baseuri
151 ~must_exist:false ~writable:true ~baseuri,
152 LibraryMisc.lexicon_file_of_baseuri
153 ~must_exist:false ~writable:false ~baseuri
156 if Sys.file_exists lexiconpath_rw then lexiconpath_rw else
157 if Sys.file_exists lexiconpath_r then lexiconpath_r else
158 raise (IncludedFileNotCompiled (lexiconpath_rw,fullpath))
160 let lexicon = LexiconMarshal.load_lexicon lexiconpath in
161 let status = List.fold_left (eval_command ~mode) status lexicon in
163 | L.Alias (loc, spec) ->
165 (*CSC: Warning: this code should be factorized with the corresponding
166 code in DisambiguatePp *)
168 | L.Ident_alias (id,uri) ->
169 [DisambiguateTypes.Id id,spec]
170 | L.Symbol_alias (symb, instance, desc) ->
171 [DisambiguateTypes.Symbol (symb,instance),spec]
172 | L.Number_alias (instance,desc) ->
173 [DisambiguateTypes.Num instance,spec]
175 set_proof_aliases mode status diff
176 | L.Interpretation (_, dsc, (symbol, _), _) as stm ->
177 let status = add_lexicon_content [stm] status in
180 [DisambiguateTypes.Symbol (symbol, 0),
181 L.Symbol_alias (symbol,0,dsc)]
183 DisambiguateChoices.Choice_not_found msg ->
184 prerr_endline (Lazy.force msg);
187 let status = set_proof_aliases mode status diff in
189 | L.Notation _ as stm ->
190 add_lexicon_content [stm] status
192 let eval_command status cmd =
193 if !debug then dump_aliases prerr_endline "before eval_command" status;
194 let status = eval_command ?mode:None status cmd in
195 if !debug then dump_aliases prerr_endline "after eval_command" status;
198 let set_proof_aliases status aliases =
199 if !debug then dump_aliases prerr_endline "before set_proof_aliases" status;
200 let status = set_proof_aliases L.WithPreferences status aliases in
201 if !debug then dump_aliases prerr_endline "after set_proof_aliases" status;