1 (* Copyright (C) 2004, 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/
26 open Disambiguate_struct
27 open Disambiguate_types
30 let debug_print = if debug then prerr_endline else ignore
32 type interpretation_domain = Domain.t
33 type domain_and_interpretation = interpretation_domain * interpretation
35 let string_of_interpretation_domain_item = function
37 | Symbol (s, i) -> "SYMBOL " ^ s ^ " " ^ string_of_int i
38 | Num (s, i) -> "NUM " ^ s ^ " " ^ string_of_int i
40 let descr_of_domain_item = function
45 let rec build_natural =
47 | 0 -> HelmLibraryObjects.Datatypes.zero
48 | n -> Cic.Appl [ HelmLibraryObjects.Datatypes.succ; (build_natural (n - 1)) ]
50 exception Invalid_choice
52 let symbol_choices: (string, interpretation_codomain_item list) Hashtbl.t = Hashtbl.create 1023
54 Hashtbl.add symbol_choices "eq"
55 [ ("Leibnitz's equality",
60 | _ -> raise Invalid_choice
63 Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
67 let add_symbol_choice = Hashtbl.add symbol_choices
68 let add_symbol_choices symbol = List.iter (add_symbol_choice symbol)
74 let num = int_of_string num in
79 let add_num_choice choice =
80 num_choices := choice :: !num_choices
83 | Ok of Cic.term * Cic.metasenv
87 let refine metasenv context term =
88 let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in
90 let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in
93 | CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
94 (* TODO remove this case as soon as refine is fully implemented *)
96 let term' = CicTypeChecker.type_of_aux' metasenv context term in
99 | CicRefine.Uncertain _ ->
100 debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
103 debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
110 let indtyuri_of_uri uri =
111 let index_sharp = String.index uri '#' in
112 let index_num = index_sharp + 3 in
113 (UriManager.uri_of_string (String.sub uri 0 index_sharp),
114 int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1)
116 let indconuri_of_uri uri =
117 let index_sharp = String.index uri '#' in
118 let index_div = String.rindex uri '/' in
119 let index_con = index_div + 1 in
120 (UriManager.uri_of_string (String.sub uri 0 index_sharp),
122 (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1,
124 (String.sub uri index_con (String.length uri - index_con)))
126 (* TODO move it to Cic *)
127 let term_of_uri uri =
130 (* TODO explicit substitutions? *)
131 let len = String.length uri in
132 if String.sub uri (len - 4) 4 = ".con" then
133 Cic.Const (uri_of_string uri, [])
134 else if String.sub uri (len - 4) 4 = ".var" then
135 Cic.Var (uri_of_string uri, [])
139 let uri',typeno = indtyuri_of_uri uri in
140 Cic.MutInd (uri', typeno, [])
142 | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ ->
143 (* Constructor of an Inductive Type *)
144 let uri',typeno,consno = indconuri_of_uri uri in
145 Cic.MutConstruct (uri', typeno, consno, []))
147 | Invalid_argument _ -> raise (UriManager.IllFormedUri uri)
149 module Make (C: Callbacks) =
151 exception NoWellTypedInterpretation
153 let choices_of_id mqi_handle id =
154 let query = MQueryGenerator.locate id in
155 let result = MQueryInterpreter.execute mqi_handle query in
159 MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
161 C.output_html (`Msg (`T "Locate query:"));
162 MQueryUtil.text_of_query
163 (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
165 C.output_html (`Msg (`T "Result:"));
166 MQueryUtil.text_of_result
167 (fun s -> C.output_html (`Msg (`T s))) "" result;
171 [UriManager.string_of_uri (C.input_or_locate_uri
172 ~title:("URI matching \"" ^ id ^ "\" unknown."))]
175 C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
176 ~ok:"Try every selection." ~enable_button_for_non_vars:true
177 ~title:"Ambiguous input." ~id
178 ~msg: ("Ambiguous input \"" ^ id ^
179 "\". Please, choose one or more interpretations:")
182 List.map (fun uri -> (uri, term_of_uri uri)) uris'
184 let disambiguate_input
185 mqi_handle context metasenv parser_dom parser_mk_term
186 (current_dom, current_interpretation)
188 debug_print "NEW DISAMBIGUATE INPUT";
189 let todo_dom = Domain.diff parser_dom current_dom in
190 (* (1) for each item in todo_dom we get the associated list of choices *)
191 let id_choices = Hashtbl.create 1023 in
196 (* pairs <description, term> *)
197 let choices = choices_of_id mqi_handle id in
199 "CHOICES_OF_ID di %s ha restituito %d scelte"
200 id (List.length choices));
201 Hashtbl.add id_choices id choices
203 (Domain.filter (function Id _ -> true | _ -> false) todo_dom)
205 (* (2) lookup function for any item (Id/Symbol/Num) *)
206 let lookup_choices item =
210 let choices = Hashtbl.find id_choices id in
211 List.map (fun (descr, term) -> (descr, fun _ _ -> term)) choices
212 | Symbol (symb, _) -> Hashtbl.find symbol_choices symb
215 (fun (descr, f) -> (descr, let term = f num in fun _ _ -> term))
217 with Not_found -> assert false
219 (* (3) test an interpretation filling with meta uninterpreted identifiers
221 let test_interpretation current_interpretation todo_dom =
222 let filled_interpretation =
224 (fun item' interpretation ->
227 "Implicit", fun _ _ -> Cic.Implicit
230 todo_dom current_interpretation
232 let term' = parser_mk_term filled_interpretation in
233 refine metasenv context term'
235 (* (4) build all possible interpretations *)
236 let rec aux current_interpretation todo_dom =
237 if Domain.is_empty todo_dom then
238 match test_interpretation current_interpretation Domain.empty with
239 | Ok (term, metasenv) -> [ current_interpretation, term, metasenv ]
240 | Ko | Uncertain -> []
242 let item = Domain.choose todo_dom in
243 debug_print (sprintf "CHOOSED ITEM: %s"
244 (string_of_interpretation_domain_item item));
245 let remaining_dom = Domain.remove item todo_dom in
246 let choices = lookup_choices item in
247 let rec filter = function
249 | codomain_item :: tl ->
250 let new_interpretation =
255 current_interpretation item'
257 (match test_interpretation new_interpretation remaining_dom with
258 | Ok (term, metasenv) ->
259 (if Domain.is_empty remaining_dom then
260 [ new_interpretation, term, metasenv ]
262 aux new_interpretation remaining_dom)
265 (if Domain.is_empty remaining_dom then
268 aux new_interpretation remaining_dom)
274 let (choosed_interpretation, choosed_term, choosed_metasenv) =
275 match aux current_interpretation todo_dom with
276 | [] -> raise NoWellTypedInterpretation
278 debug_print "UNA SOLA SCELTA";
281 debug_print "PIU' SCELTE";
284 (fun (interpretation, _, _) ->
287 let description = fst (interpretation domain_item) in
289 match interpretation domain_item with
290 | None -> assert false
291 | Some (descr, _) -> descr
294 (descr_of_domain_item domain_item, description))
295 (Domain.elements parser_dom))
298 let choosed = C.interactive_interpretation_choice choices in
301 (Domain.union current_dom todo_dom, choosed_interpretation),
302 choosed_metasenv, choosed_term
306 let apply_interp (interp: interpretation) item = snd (interp item)
308 let interpretate ~context ~interp ast =
309 let rec aux loc context = function
310 | Ast.LocatedTerm (loc, term) -> aux loc context term
311 | Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
312 | Ast.Appl_symbol (symb, args) ->
313 let cic_args = List.map (aux loc context) args in
314 apply_interp interp (Symbol (symb, 0)) interp cic_args
315 | Ast.Binder (binder_kind, var, typ, body) ->
316 let cic_type = aux_option loc context typ in
317 let cic_body = aux loc (Some var :: context) body in
318 (match binder_kind with
319 | `Lambda -> Cic.Lambda (var, cic_type, cic_body)
320 | `Pi | `Forall -> Cic.Prod (var, cic_type, cic_body)
322 apply_interp interp (Symbol ("exists", 0)) interp
323 [ cic_type; Cic.Lambda (var, cic_type, cic_body) ])
324 | Ast.Case (term, indty_ident, outtype, branches) ->
325 let cic_term = aux loc context term in
326 let cic_outtype = aux_option loc context outtype in
327 let do_branch (pat, term) =
328 let rec do_branch' context = function
329 | [] -> aux loc context term
331 let cic_body = do_branch' (Some (Cic.Name hd) :: context) tl in
332 Cic.Lambda (Cic.Name hd, Cic.Implicit, cic_body)
335 | _ :: tl -> (* ignoring constructor *) do_branch' context tl
338 let (indtype_uri, indtype_no) =
339 match apply_interp interp (Id indty_ident) interp [] with
340 | Cic.MutInd (uri, tyno, _) -> uri, tyno
341 | _ -> Parser.fail loc ("Not an inductive type: " ^ indty_ident)
343 Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
344 (List.map do_branch branches))
345 | Ast.LetIn (var, def, body) ->
346 let cic_def = aux loc context def in
347 let name = Cic.Name var in
348 let cic_body = aux loc (Some name :: context) body in
349 Cic.LetIn (name, cic_def, cic_body)
350 | Ast.LetRec (kind, defs, body) ->
352 List.fold_left (fun acc (var, _, _, _) -> Some (Cic.Name var) :: acc)
355 let cic_body = aux loc context' body in
358 (fun (var, body, typ, decr_idx) ->
359 let cic_body = aux loc context' body in
360 let cic_type = aux_option loc context typ in
361 (var, decr_idx, cic_type, cic_body))
364 let counter = ref 0 in
365 let build_term funs =
366 (* this is the body of the fold_right function below. Rationale: Fix
367 * and CoFix cases differs only in an additional index in the
368 * indcutiveFun list, see Cic.term *)
371 (fun (var, _, _, _) cic ->
373 Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
376 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
378 (fun (var, _, _, _) cic ->
379 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
381 List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
382 | Ast.Ident (name, subst) ->
383 let rec find acc e = function
384 | [] -> raise Not_found
385 | Some (Cic.Name hd) :: tl when e = hd -> acc
386 | _ :: tl -> find (acc + 1) e tl
389 let index = find 1 name context in
391 Parser.fail loc "Explicit substitutions not allowed here";
394 apply_interp interp (Id name) interp [])
395 | Ast.Num num -> apply_interp interp (Num (num, 0)) interp []
396 | Ast.Meta (index, subst) ->
399 (function None -> None | Some term -> Some (aux loc context term))
402 Cic.Meta (index, cic_subst)
403 | Ast.Sort `Prop -> Cic.Sort Cic.Prop
404 | Ast.Sort `Set -> Cic.Sort Cic.Set
405 | Ast.Sort `Type -> Cic.Sort Cic.Type
406 | Ast.Sort `CProp -> Cic.Sort Cic.CProp
407 and aux_option loc context = function
408 | None -> Cic.Implicit
409 | Some term -> aux loc context term
412 | Ast.LocatedTerm (loc, term) -> aux loc context term