]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/lexicon/lexiconEngine.ml
- matitacLib: better handling of the callbacks for the dump operation
[helm.git] / helm / software / components / lexicon / lexiconEngine.ml
1 (* Copyright (C) 2004-2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 module L = LexiconAst
29
30 let debug = ref true
31
32 (* lexicon file name * ma file name *)
33 exception IncludedFileNotCompiled of string * string 
34 exception MetadataNotFound of string        (* file name *)
35
36 type status = {
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 *)
41 }
42
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))
47       status.aliases
48    
49 let initial_status = {
50   aliases = DisambiguateTypes.Environment.empty;
51   multi_aliases = DisambiguateTypes.Environment.empty;
52   lexicon_content_rev = [];
53   notation_ids = [];
54 }
55
56 let add_lexicon_content cmds status =
57   let content = status.lexicon_content_rev in
58   let content' =
59     List.fold_right
60      (fun cmd acc -> 
61         match cmd with
62         | L.Alias _ 
63         | L.Include _ 
64         | L.Notation _ -> cmd :: (List.filter ((<>) cmd) acc)
65         | L.Interpretation _ -> if List.exists ((=) cmd) acc then acc else cmd::acc)
66      cmds content
67   in
68 (*   
69   prerr_endline ("new lexicon content: " ^ 
70      String.concat "; " (List.map LexiconAstPp.pp_command content')
71   );
72 *)
73   { status with lexicon_content_rev = content' }
74
75 let set_proof_aliases mode status new_aliases =
76  if mode = L.WithoutPreferences then
77    status 
78  else
79    let commands_of_aliases =
80      List.map
81       (fun _,alias -> L.Alias (HExtlib.dummy_floc, alias))
82    in
83    let aliases =
84     List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
85      status.aliases new_aliases in
86    let multi_aliases =
87     List.fold_left (fun acc (d,c) -> 
88       DisambiguateTypes.Environment.cons L.description_of_alias 
89          d c acc)
90      status.multi_aliases new_aliases
91    in
92    let new_status =
93      { status with multi_aliases = multi_aliases ; aliases = aliases}
94    in
95    if new_aliases = [] then
96      new_status
97    else
98      let status = 
99        add_lexicon_content (commands_of_aliases new_aliases) new_status 
100      in
101      status
102
103
104 let rec eval_command ?(mode=L.WithPreferences) status cmd =
105 (*
106  let bmode = match mode with L.WithPreferences -> true | _ -> false in
107  Printf.eprintf "Include preferences: %b\n" bmode;
108 *) 
109  let cmd =
110   match cmd with
111   | L.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
112      let rec disambiguate =
113       function
114          CicNotationPt.ApplPattern l ->
115           CicNotationPt.ApplPattern (List.map disambiguate l)
116        | CicNotationPt.VarPattern id
117           when not
118            (List.exists
119             (function (CicNotationPt.IdentArg (_,id')) -> id'=id) args)
120           ->
121            let item = DisambiguateTypes.Id id in
122             begin try
123               let uri =
124                match DisambiguateTypes.Environment.find item status.aliases with
125                   L.Ident_alias (_, uri)-> UriManager.uri_of_string uri
126                 | _ -> assert false
127               in
128                CicNotationPt.UriPattern uri
129              with Not_found -> 
130               prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^ 
131                (DisambiguateTypes.string_of_domain_item item));
132               dump_aliases prerr_endline "" status;
133               assert false
134             end
135        | p -> p
136      in
137       L.Interpretation
138        (loc, dsc, (symbol, args), disambiguate cic_appl_pattern)
139   | _-> cmd
140  in
141  let notation_ids' = CicNotation.process_notation cmd in
142  let status =
143    { status with notation_ids = notation_ids' @ status.notation_ids } in
144   match cmd with
145   | L.Include (loc, baseuri, mode, fullpath) ->
146      let lexiconpath_rw, lexiconpath_r = 
147        LibraryMisc.lexicon_file_of_baseuri 
148          ~must_exist:false ~writable:true ~baseuri,
149        LibraryMisc.lexicon_file_of_baseuri 
150          ~must_exist:false ~writable:false ~baseuri
151      in
152      let lexiconpath = 
153        if Sys.file_exists lexiconpath_rw then lexiconpath_rw else
154          if Sys.file_exists lexiconpath_r then lexiconpath_r else
155           raise (IncludedFileNotCompiled (lexiconpath_rw,fullpath))
156      in
157      let lexicon = LexiconMarshal.load_lexicon lexiconpath in
158      let status = List.fold_left (eval_command ~mode) status lexicon in
159      status
160   | L.Alias (loc, spec) -> 
161      let diff =
162       (*CSC: Warning: this code should be factorized with the corresponding
163              code in DisambiguatePp *)
164       match spec with
165       | L.Ident_alias (id,uri) -> 
166          [DisambiguateTypes.Id id,spec]
167       | L.Symbol_alias (symb, instance, desc) ->
168          [DisambiguateTypes.Symbol (symb,instance),spec]
169       | L.Number_alias (instance,desc) ->
170          [DisambiguateTypes.Num instance,spec]
171      in
172       set_proof_aliases mode status diff
173   | L.Interpretation (_, dsc, (symbol, _), _) as stm ->
174       let status = add_lexicon_content [stm] status in
175       let diff =
176        try
177         [DisambiguateTypes.Symbol (symbol, 0),
178           L.Symbol_alias (symbol,0,dsc)]
179        with
180         DisambiguateChoices.Choice_not_found msg ->
181           prerr_endline (Lazy.force msg);
182           assert false
183       in
184       let status = set_proof_aliases mode status diff in
185       status
186   | L.Notation _ as stm ->
187       add_lexicon_content [stm] status
188
189 let eval_command status cmd = 
190    if !debug then dump_aliases prerr_endline "before eval_command" status;
191    let status = eval_command ?mode:None status cmd in
192    if !debug then dump_aliases prerr_endline "after eval_command" status;
193    status
194
195 let set_proof_aliases status aliases =
196    if !debug then dump_aliases prerr_endline "before set_proof_aliases" status;
197    let status = set_proof_aliases L.WithPreferences status aliases in
198    if !debug then dump_aliases prerr_endline "after set_proof_aliases" status;
199    status