]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/grafite_parser/grafiteDisambiguate.ml
abstracted pretty printers over inner pretty printing units (terms, lazy terms, and...
[helm.git] / helm / ocaml / grafite_parser / grafiteDisambiguate.ml
1 (* Copyright (C) 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 open GrafiteTypes
27
28 let singleton = function
29   | [x], _ -> x
30   | _ -> assert false
31
32   (** @param term not meaningful when context is given *)
33 let disambiguate_term ?context status_ref goal term =
34   let status = !status_ref in
35   let context =
36     match context with
37     | Some c -> c
38     | None -> GrafiteTypes.get_proof_context status goal
39   in
40   let (diff, metasenv, cic, _) =
41     singleton
42       (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
43         ~aliases:status.aliases ~universe:(Some status.multi_aliases)
44         ~context ~metasenv:(GrafiteTypes.get_proof_metasenv status) term)
45   in
46   let status = GrafiteTypes.set_metasenv metasenv status in
47   let status = MatitaSync.set_proof_aliases status diff in
48   status_ref := status;
49   cic
50   
51   (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
52    * rationale: lazy_term will be invoked in different context to obtain a term,
53    * each invocation will disambiguate the term and can add aliases. Once all
54    * disambiguations have been performed, the first returned function can be
55    * used to obtain the resulting aliases *)
56 let disambiguate_lazy_term status_ref term =
57   (fun context metasenv ugraph ->
58     let status = !status_ref in
59     let (diff, metasenv, cic, ugraph) =
60       singleton
61         (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
62           ~initial_ugraph:ugraph ~aliases:status.aliases
63           ~universe:(Some status.multi_aliases) ~context ~metasenv term)
64     in
65     let status = GrafiteTypes.set_metasenv metasenv status in
66     let status = MatitaSync.set_proof_aliases status diff in
67     status_ref := status;
68     cic, metasenv, ugraph)
69
70 let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
71   let interp path = Disambiguate.interpretate_path [] path in
72   let goal_path = interp goal_path in
73   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
74   let wanted =
75    match wanted with
76       None -> None
77     | Some wanted ->
78        let wanted = disambiguate_lazy_term status_ref wanted in
79        Some wanted
80   in
81   (wanted, hyp_paths ,goal_path)
82
83 let disambiguate_reduction_kind aliases_ref = function
84   | `Unfold (Some t) ->
85       let t = disambiguate_lazy_term aliases_ref t in
86       `Unfold (Some t)
87   | `Normalize
88   | `Reduce
89   | `Simpl
90   | `Unfold None
91   | `Whd as kind -> kind
92   
93 let disambiguate_tactic status goal tactic =
94   let status_ref = ref status in
95   let tactic =
96     match tactic with
97     | GrafiteAst.Absurd (loc, term) -> 
98         let cic = disambiguate_term status_ref goal term in
99         GrafiteAst.Absurd (loc, cic)
100     | GrafiteAst.Apply (loc, term) ->
101         let cic = disambiguate_term status_ref goal term in
102         GrafiteAst.Apply (loc, cic)
103     | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
104     | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
105         GrafiteAst.Auto (loc,depth,width,paramodulation,full)
106     | GrafiteAst.Change (loc, pattern, with_what) -> 
107         let with_what = disambiguate_lazy_term status_ref with_what in
108         let pattern = disambiguate_pattern status_ref pattern in
109         GrafiteAst.Change (loc, pattern, with_what)
110     | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id)
111     | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id)
112     | GrafiteAst.Compare (loc,term) ->
113         let term = disambiguate_term status_ref goal term in
114         GrafiteAst.Compare (loc,term)
115     | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n)
116     | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc
117     | GrafiteAst.Cut (loc, ident, term) -> 
118         let cic = disambiguate_term status_ref goal term in
119         GrafiteAst.Cut (loc, ident, cic)
120     | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc
121     | GrafiteAst.Decompose (loc, types, what, names) ->
122         let disambiguate types = function
123            | GrafiteAst.Type _   -> assert false
124            | GrafiteAst.Ident id ->
125               (match disambiguate_term status_ref goal
126                 (CicNotationPt.Ident (id, None))
127               with
128               | Cic.MutInd (uri, tyno, _) ->
129                   (GrafiteAst.Type (uri, tyno) :: types)
130               | _ -> raise (MatitaDisambiguator.DisambiguationError (0,[[None,lazy "Decompose works only on inductive types"]])))
131         in
132         let types = List.fold_left disambiguate [] types in
133         GrafiteAst.Decompose (loc, types, what, names)
134     | GrafiteAst.Discriminate (loc,term) ->
135         let term = disambiguate_term status_ref goal term in
136         GrafiteAst.Discriminate(loc,term)
137     | GrafiteAst.Exact (loc, term) -> 
138         let cic = disambiguate_term status_ref goal term in
139         GrafiteAst.Exact (loc, cic)
140     | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
141         let what = disambiguate_term status_ref goal what in
142         let using = disambiguate_term status_ref goal using in
143         GrafiteAst.Elim (loc, what, Some using, depth, idents)
144     | GrafiteAst.Elim (loc, what, None, depth, idents) ->
145         let what = disambiguate_term status_ref goal what in
146         GrafiteAst.Elim (loc, what, None, depth, idents)
147     | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
148         let what = disambiguate_term status_ref goal what in
149         let using = disambiguate_term status_ref goal using in
150         GrafiteAst.ElimType (loc, what, Some using, depth, idents)
151     | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
152         let what = disambiguate_term status_ref goal what in
153         GrafiteAst.ElimType (loc, what, None, depth, idents)
154     | GrafiteAst.Exists loc -> GrafiteAst.Exists loc 
155     | GrafiteAst.Fail loc -> GrafiteAst.Fail loc
156     | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
157         let pattern = disambiguate_pattern status_ref pattern in
158         let term = disambiguate_lazy_term status_ref term in
159         let red_kind = disambiguate_reduction_kind status_ref red_kind in
160         GrafiteAst.Fold (loc, red_kind, term, pattern)
161     | GrafiteAst.FwdSimpl (loc, hyp, names) ->
162        GrafiteAst.FwdSimpl (loc, hyp, names)  
163     | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc
164     | GrafiteAst.Generalize (loc,pattern,ident) ->
165         let pattern = disambiguate_pattern status_ref pattern in
166         GrafiteAst.Generalize (loc,pattern,ident)
167     | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g)
168     | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc
169     | GrafiteAst.Injection (loc, term) ->
170         let term = disambiguate_term status_ref goal term in
171         GrafiteAst.Injection (loc,term)
172     | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names)
173     | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
174        let f term to_what =
175           let term = disambiguate_term status_ref goal term in
176           term :: to_what
177        in
178        let to_what = List.fold_right f to_what [] in 
179        let what = disambiguate_term status_ref goal what in
180        GrafiteAst.LApply (loc, depth, to_what, what, ident)
181     | GrafiteAst.Left loc -> GrafiteAst.Left loc
182     | GrafiteAst.LetIn (loc, term, name) ->
183         let term = disambiguate_term status_ref goal term in
184         GrafiteAst.LetIn (loc,term,name)
185     | GrafiteAst.Reduce (loc, red_kind, pattern) ->
186         let pattern = disambiguate_pattern status_ref pattern in
187         let red_kind = disambiguate_reduction_kind status_ref red_kind in
188         GrafiteAst.Reduce(loc, red_kind, pattern)
189     | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc
190     | GrafiteAst.Replace (loc, pattern, with_what) -> 
191         let pattern = disambiguate_pattern status_ref pattern in
192         let with_what = disambiguate_lazy_term status_ref with_what in
193         GrafiteAst.Replace (loc, pattern, with_what)
194     | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
195         let term = disambiguate_term status_ref goal t in
196         let pattern = disambiguate_pattern status_ref pattern in
197         GrafiteAst.Rewrite (loc, dir, term, pattern)
198     | GrafiteAst.Right loc -> GrafiteAst.Right loc
199     | GrafiteAst.Ring loc -> GrafiteAst.Ring loc
200     | GrafiteAst.Split loc -> GrafiteAst.Split loc
201     | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc
202     | GrafiteAst.Transitivity (loc, term) -> 
203         let cic = disambiguate_term status_ref goal term in
204         GrafiteAst.Transitivity (loc, cic)
205   in
206   status_ref, tactic
207
208 let disambiguate_obj status obj =
209   let uri =
210    match obj with
211     | CicNotationPt.Inductive (_,(name,_,_,_)::_)
212     | CicNotationPt.Record (_,name,_,_) ->
213        Some (UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ".ind"))
214     | CicNotationPt.Inductive _ -> assert false
215     | CicNotationPt.Theorem _ -> None in
216   let (diff, metasenv, cic, _) =
217     singleton
218       (MatitaDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
219         ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
220   in
221   let proof_status =
222     match status.proof_status with
223     | No_proof -> Intermediate metasenv
224     | Incomplete_proof _
225     | Proof _ ->
226        raise (GrafiteTypes.Command_error "imbricated proofs not allowed")
227     | Intermediate _ -> assert false
228   in
229   let status = { status with proof_status = proof_status } in
230   let status = MatitaSync.set_proof_aliases status diff in
231   status, cic
232   
233 let disambiguate_command status =
234   function
235   | GrafiteAst.Alias _
236   | GrafiteAst.Default _
237   | GrafiteAst.Drop _
238   | GrafiteAst.Dump _
239   | GrafiteAst.Include _
240   | GrafiteAst.Interpretation _
241   | GrafiteAst.Notation _
242   | GrafiteAst.Qed _
243   | GrafiteAst.Render _
244   | GrafiteAst.Set _ as cmd ->
245       status,cmd
246   | GrafiteAst.Coercion (loc, term, add_composites) ->
247       let status_ref = ref status in
248       let term = disambiguate_term ~context:[] status_ref ~-1 term in
249       !status_ref, GrafiteAst.Coercion (loc,term,add_composites)
250   | GrafiteAst.Obj (loc,obj) ->
251       let status,obj = disambiguate_obj status obj in
252       status, GrafiteAst.Obj (loc,obj)