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 (* $Id: disambiguate.ml 9178 2008-11-12 12:09:52Z tassi $ *)
30 open DisambiguateTypes
33 module Ast = CicNotationPt
35 let debug_print _ = ();;
37 let refine_term metasenv context uri term ugraph ~localization_tbl =
38 (* if benchmark then incr actual_refinements; *)
40 debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
42 let term', _, metasenv',ugraph1 =
43 NCicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
44 (Disambiguate.Ok (term', metasenv')),ugraph1
47 let rec process_exn loc =
49 HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
50 | CicRefine.Uncertain msg ->
51 debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
52 Disambiguate.Uncertain (loc,msg),ugraph
53 | CicRefine.RefineFailure msg ->
54 debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
55 (CicPp.ppterm term) (Lazy.force msg)));
56 Disambiguate.Ko (loc,msg),ugraph
61 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
63 snd (Environment.find item env) env num args
65 failwith ("Domain item not found: " ^
66 (DisambiguateTypes.string_of_domain_item item))
68 (* TODO move it to Cic *)
69 let find_in_context name context =
70 let rec aux acc = function
71 | [] -> raise Not_found
72 | Cic.Name hd :: tl when hd = name -> acc
73 | _ :: tl -> aux (acc + 1) tl
77 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
80 (* create_dummy_ids shouldbe used only for interpretating patterns *)
82 let rec aux ~localize loc context = function
83 | CicNotationPt.AttributedTerm (`Loc loc, term) ->
84 let res = aux ~localize loc context term in
85 if localize then Cic.CicHash.add localization_tbl res loc;
87 | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
88 | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
89 let cic_args = List.map (aux ~localize loc context) args in
90 resolve env (Symbol (symb, i)) ~args:cic_args ()
91 | CicNotationPt.Appl terms ->
92 Cic.Appl (List.map (aux ~localize loc context) terms)
93 | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
94 let cic_type = aux_option ~localize loc context (Some `Type) typ in
95 let cic_name = CicNotationUtil.cic_name_of_name var in
96 let cic_body = aux ~localize loc (cic_name :: context) body in
97 (match binder_kind with
98 | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
100 | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
102 resolve env (Symbol ("exists", 0))
103 ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
104 | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
105 let cic_term = aux ~localize loc context term in
106 let cic_outtype = aux_option ~localize loc context None outtype in
107 let do_branch ((head, _, args), term) =
108 let rec do_branch' context = function
109 | [] -> aux ~localize loc context term
110 | (name, typ) :: tl ->
111 let cic_name = CicNotationUtil.cic_name_of_name name in
112 let cic_body = do_branch' (cic_name :: context) tl in
115 | None -> Cic.Implicit (Some `Type)
116 | Some typ -> aux ~localize loc context typ
118 Cic.Lambda (cic_name, typ, cic_body)
120 do_branch' context args
122 let indtype_uri, indtype_no =
123 if create_dummy_ids then
124 (UriManager.uri_of_string "cic:/fake_indty.con", 0)
126 match indty_ident with
127 | Some (indty_ident, _) ->
128 (match resolve env (Id indty_ident) () with
129 | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
131 raise (Disambiguate.Try_again (lazy "The type of the term to be matched
134 raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
136 let rec fst_constructor =
138 (Ast.Pattern (head, _, _), _) :: _ -> head
139 | (Ast.Wildcard, _) :: tl -> fst_constructor tl
140 | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))
142 (match resolve env (Id (fst_constructor branches)) () with
143 | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
144 (indtype_uri, indtype_no)
146 raise (Disambiguate.Try_again (lazy "The type of the term to be matched
149 raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
152 if create_dummy_ids then
155 Ast.Wildcard,term -> ("wildcard",None,[]), term
157 raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
160 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
161 Cic.InductiveDefinition (il,_,leftsno,_) ->
164 List.nth il indtype_no
165 with _ -> assert false
167 let rec count_prod t =
168 match CicReduction.whd [] t with
169 Cic.Prod (_, _, t) -> 1 + (count_prod t)
172 let rec sort branches cl =
175 let rec analyze unused unrecognized useless =
178 if unrecognized != [] then
179 raise (DisambiguateTypes.Invalid_choice
182 ("Unrecognized constructors: " ^
183 String.concat " " unrecognized)))
184 else if useless > 0 then
185 raise (DisambiguateTypes.Invalid_choice
188 ("The last " ^ string_of_int useless ^
189 "case" ^ if useless > 1 then "s are" else " is" ^
193 | (Ast.Wildcard,_)::tl when not unused ->
194 analyze true unrecognized useless tl
195 | (Ast.Pattern (head,_,_),_)::tl when not unused ->
196 analyze unused (head::unrecognized) useless tl
197 | _::tl -> analyze unused unrecognized (useless + 1) tl
199 analyze false [] 0 branches
201 let rec find_and_remove =
205 (DisambiguateTypes.Invalid_choice
206 (Some loc, lazy ("Missing case: " ^ name)))
207 | ((Ast.Wildcard, _) as branch :: _) as branches ->
209 | (Ast.Pattern (name',_,_),_) as branch :: tl
213 let found,rest = find_and_remove tl in
216 let branch,tl = find_and_remove branches in
218 Ast.Pattern (name,y,args),term ->
219 if List.length args = count_prod ty - leftsno then
220 ((name,y,args),term)::sort tl cltl
223 (DisambiguateTypes.Invalid_choice
225 lazy ("Wrong number of arguments for " ^ name)))
226 | Ast.Wildcard,term ->
232 (`Lambda, (CicNotationPt.Ident ("_", None), None),
235 (("wildcard",None,[]),
236 mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
241 Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
242 (List.map do_branch branches))
243 | CicNotationPt.Cast (t1, t2) ->
244 let cic_t1 = aux ~localize loc context t1 in
245 let cic_t2 = aux ~localize loc context t2 in
246 Cic.Cast (cic_t1, cic_t2)
247 | CicNotationPt.LetIn ((name, typ), def, body) ->
248 let cic_def = aux ~localize loc context def in
249 let cic_name = CicNotationUtil.cic_name_of_name name in
252 | None -> Cic.Implicit (Some `Type)
253 | Some t -> aux ~localize loc context t
255 let cic_body = aux ~localize loc (cic_name :: context) body in
256 Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
257 | CicNotationPt.LetRec (kind, defs, body) ->
260 (fun acc (_, (name, _), _, _) ->
261 CicNotationUtil.cic_name_of_name name :: acc)
265 let unlocalized_body = aux ~localize:false loc context' body in
266 match unlocalized_body with
267 Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
268 | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
273 let t',subst,metasenv =
274 CicMetaSubst.delift_rels [] [] (List.length defs) t
277 assert (metasenv=[]);
280 (* We can avoid the LetIn. But maybe we need to recompute l'
281 so that it is localized *)
284 CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
285 (* since we avoid the letin, the context has no
287 let l' = List.map (aux ~localize loc context) l in
293 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
295 `AddLetIn (aux ~localize loc context' body)
297 `AddLetIn unlocalized_body)
300 `AddLetIn (aux ~localize loc context' body)
302 `AddLetIn unlocalized_body
306 (fun (params, (name, typ), body, decr_idx) ->
307 let add_binders kind t =
309 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
312 aux ~localize loc context' (add_binders `Lambda body) in
314 aux_option ~localize loc context (Some `Type)
315 (HExtlib.map_option (add_binders `Pi) typ) in
317 match CicNotationUtil.cic_name_of_name name with
319 CicNotationPt.fail loc
320 "Recursive functions cannot be anonymous"
321 | Cic.Name name -> name
323 (name, decr_idx, cic_type, cic_body))
328 `Inductive -> Cic.Fix (n,inductiveFuns)
330 let coinductiveFuns =
332 (fun (name, _, typ, body) -> name, typ, body)
335 Cic.CoFix (n,coinductiveFuns)
337 let counter = ref ~-1 in
338 let build_term funs (var,_,ty,_) t =
340 Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
343 `AvoidLetInNoAppl n ->
344 let n' = List.length inductiveFuns - n in
346 | `AvoidLetIn (n,l) ->
347 let n' = List.length inductiveFuns - n in
348 Cic.Appl (fix_or_cofix n'::l)
349 | `AddLetIn cic_body ->
350 List.fold_right (build_term inductiveFuns) inductiveFuns
352 | CicNotationPt.Ident _
353 | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
354 | CicNotationPt.Ident (name, subst)
355 | CicNotationPt.Uri (name, subst) as ast ->
356 let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
358 if is_uri ast then raise Not_found;(* don't search the env for URIs *)
359 let index = find_in_context name context in
360 if subst <> None then
361 CicNotationPt.fail loc "Explicit substitutions not allowed here";
365 if is_uri ast then (* we have the URI, build the term out of it *)
367 CicUtil.term_of_uri (UriManager.uri_of_string name)
368 with UriManager.IllFormedUri _ ->
369 CicNotationPt.fail loc "Ill formed URI"
371 resolve env (Id name) ()
375 List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
382 List.assoc s ids_to_uris, aux ~localize loc context term
384 raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
386 | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
390 | Cic.Const (uri, []) ->
391 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
392 let uris = CicUtil.params_of_obj o in
393 Cic.Const (uri, mk_subst uris)
394 | Cic.Var (uri, []) ->
395 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
396 let uris = CicUtil.params_of_obj o in
397 Cic.Var (uri, mk_subst uris)
398 | Cic.MutInd (uri, i, []) ->
400 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
401 let uris = CicUtil.params_of_obj o in
402 Cic.MutInd (uri, i, mk_subst uris)
404 CicEnvironment.Object_not_found _ ->
405 (* if we are here it is probably the case that during the
406 definition of a mutual inductive type we have met an
407 occurrence of the type in one of its constructors.
408 However, the inductive type is not yet in the environment
410 (*here the explicit_named_substituion is assumed to be of length 0 *)
411 Cic.MutInd (uri,i,[]))
412 | Cic.MutConstruct (uri, i, j, []) ->
413 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
414 let uris = CicUtil.params_of_obj o in
415 Cic.MutConstruct (uri, i, j, mk_subst uris)
416 | Cic.Meta _ | Cic.Implicit _ as t ->
418 debug_print (lazy (sprintf
419 "Warning: %s must be instantiated with _[%s] but we do not enforce it"
423 (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
428 raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
430 CicEnvironment.CircularDependency _ ->
431 raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
432 | CicNotationPt.Implicit -> Cic.Implicit None
433 | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
434 | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
435 | CicNotationPt.Meta (index, subst) ->
440 | Some term -> Some (aux ~localize loc context term))
443 Cic.Meta (index, cic_subst)
444 | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
445 | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
446 | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
447 | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
448 | CicNotationPt.Symbol (symbol, instance) ->
449 resolve env (Symbol (symbol, instance)) ()
450 | _ -> assert false (* god bless Bologna *)
451 and aux_option ~localize loc context annotation = function
452 | None -> Cic.Implicit annotation
453 | Some term -> aux ~localize loc context term
455 aux ~localize:true HExtlib.dummy_floc context ast
457 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
462 let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
463 interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
468 let domain_of_term ~context =
469 let context = List.map (fun x -> Cic.Name (fst x)) context in
470 Disambiguate.domain_of_ast_term ~context
473 module Make (C : DisambiguateTypes.Callbacks) = struct
474 module Disambiguator = Disambiguate.Make(C)
476 let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
477 ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
478 (text,prefix_len,term) =
480 if fresh_instances then CicNotationUtil.freshen_term term else term
482 let localization_tbl = Cic.CicHash.create 503 in
483 Disambiguator.disambiguate_thing
484 ~dbd ~context ~metasenv ~initial_ugraph ~aliases
485 ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
486 ~domain_of_thing:domain_of_term
487 ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
488 ~refine_thing:refine_term (text,prefix_len,term)