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 subst context uri term _ ~localization_tbl =
39 debug_print (lazy (sprintf "TEST_INTERPRETATION: %s"
40 (NCicPp.ppterm ~metasenv ~subst ~context term)));
43 try NCicUntrusted.NCicHash.find localization_tbl t
44 with Not_found -> assert false
46 let metasenv, subst, term, _ =
47 NCicRefiner.typeof metasenv subst context term None ~localise
49 Disambiguate.Ok (term, metasenv, subst, ())
51 | NCicRefiner.Uncertain (msg) ->
52 debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force msg) ^ "] " ^
53 NCicPp.ppterm ~metasenv ~subst ~context term)) ;
54 Disambiguate.Uncertain (loc,msg)
55 | NCicRefiner.RefineFailure (msg) ->
56 debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s"
57 (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force msg))));
58 Disambiguate.Ko (loc,msg,())
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 :: _ when hd = name -> acc
73 | _ :: tl -> aux (acc + 1) tl
78 ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl
80 (* create_dummy_ids shouldbe used only for interpretating patterns *)
83 let rec aux ~localize loc context = function
84 | CicNotationPt.AttributedTerm (`Loc loc, term) ->
85 let res = aux ~localize loc context term in
86 if localize then NCic.NCicHash.add localization_tbl res loc;
88 | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
89 | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
90 let cic_args = List.map (aux ~localize loc context) args in
91 resolve env (Symbol (symb, i)) ~args:cic_args ()
92 | CicNotationPt.Appl terms ->
93 NCic.Appl (List.map (aux ~localize loc context) terms)
94 | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
95 let cic_type = aux_option ~localize loc context (Some `Type) typ in
96 let cic_name = CicNotationUtil.cic_name_of_name var in
97 let cic_body = aux ~localize loc (cic_name :: context) body in
98 (match binder_kind with
99 | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
101 | `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
103 resolve env (Symbol ("exists", 0))
104 ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ())
105 | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
106 let cic_term = aux ~localize loc context term in
107 let cic_outtype = aux_option ~localize loc context None outtype in
108 let do_branch ((_, _, args), term) =
109 let rec do_branch' context = function
110 | [] -> aux ~localize loc context term
111 | (name, typ) :: tl ->
112 let cic_name = CicNotationUtil.cic_name_of_name name in
113 let cic_body = do_branch' (cic_name :: context) tl in
116 | None -> NCic.Implicit (Some `Type)
117 | Some typ -> aux ~localize loc context typ
119 NCic.Lambda (cic_name, typ, cic_body)
121 do_branch' context args
123 let indtype_uri, indtype_no =
124 if create_dummy_ids then
125 (UriManager.uri_of_string "cic:/fake_indty.con", 0)
127 match indty_ident with
128 | Some (indty_ident, _) ->
129 (match resolve env (Id indty_ident) () with
130 | NCic.MutInd (uri, tyno, _) -> (uri, tyno)
132 raise (Disambiguate.Try_again (lazy "The type of the term to be matched
135 raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
137 let rec fst_constructor =
139 (Ast.Pattern (head, _, _), _) :: _ -> head
140 | (Ast.Wildcard, _) :: tl -> fst_constructor tl
141 | [] -> 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"))
143 (match resolve env (Id (fst_constructor branches)) () with
144 | NCic.MutConstruct (indtype_uri, indtype_no, _, _) ->
145 (indtype_uri, indtype_no)
147 raise (Disambiguate.Try_again (lazy "The type of the term to be matched
150 raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
153 if create_dummy_ids then
156 Ast.Wildcard,term -> ("wildcard",None,[]), term
158 raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
161 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
162 NCic.InductiveDefinition (il,_,leftsno,_) ->
165 List.nth il indtype_no
166 with _ -> assert false
168 let rec count_prod t =
169 match CicReduction.whd [] t with
170 NCic.Prod (_, _, t) -> 1 + (count_prod t)
173 let rec sort branches cl =
176 let rec analyze unused unrecognized useless =
179 if unrecognized != [] then
180 raise (DisambiguateTypes.Invalid_choice
183 ("Unrecognized constructors: " ^
184 String.concat " " unrecognized)))
185 else if useless > 0 then
186 raise (DisambiguateTypes.Invalid_choice
189 ("The last " ^ string_of_int useless ^
190 "case" ^ if useless > 1 then "s are" else " is" ^
194 | (Ast.Wildcard,_)::tl when not unused ->
195 analyze true unrecognized useless tl
196 | (Ast.Pattern (head,_,_),_)::tl when not unused ->
197 analyze unused (head::unrecognized) useless tl
198 | _::tl -> analyze unused unrecognized (useless + 1) tl
200 analyze false [] 0 branches
202 let rec find_and_remove =
206 (DisambiguateTypes.Invalid_choice
207 (Some loc, lazy ("Missing case: " ^ name)))
208 | ((Ast.Wildcard, _) as branch :: _) as branches ->
210 | (Ast.Pattern (name',_,_),_) as branch :: tl
214 let found,rest = find_and_remove tl in
217 let branch,tl = find_and_remove branches in
219 Ast.Pattern (name,y,args),term ->
220 if List.length args = count_prod ty - leftsno then
221 ((name,y,args),term)::sort tl cltl
224 (DisambiguateTypes.Invalid_choice
226 lazy ("Wrong number of arguments for " ^ name)))
227 | Ast.Wildcard,term ->
233 (`Lambda, (CicNotationPt.Ident ("_", None), None),
236 (("wildcard",None,[]),
237 mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
242 NCic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
243 (List.map do_branch branches))
244 | CicNotationPt.Cast (t1, t2) ->
245 let cic_t1 = aux ~localize loc context t1 in
246 let cic_t2 = aux ~localize loc context t2 in
247 NCic.Cast (cic_t1, cic_t2)
248 | CicNotationPt.LetIn ((name, typ), def, body) ->
249 let cic_def = aux ~localize loc context def in
250 let cic_name = CicNotationUtil.cic_name_of_name name in
253 | None -> NCic.Implicit (Some `Type)
254 | Some t -> aux ~localize loc context t
256 let cic_body = aux ~localize loc (cic_name :: context) body in
257 NCic.LetIn (cic_name, cic_def, cic_typ, cic_body)
258 | CicNotationPt.LetRec (kind, defs, body) ->
261 (fun acc (_, (name, _), _, _) ->
262 CicNotationUtil.cic_name_of_name name :: acc)
266 let unlocalized_body = aux ~localize:false loc context' body in
267 match unlocalized_body with
268 NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
269 | NCic.Appl (NCic.Rel n::l) when n <= List.length defs ->
274 let t',subst,metasenv =
275 CicMetaSubst.delift_rels [] [] (List.length defs) t
278 assert (metasenv=[]);
281 (* We can avoid the LetIn. But maybe we need to recompute l'
282 so that it is localized *)
285 CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
286 (* since we avoid the letin, the context has no
288 let l' = List.map (aux ~localize loc context) l in
294 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
296 `AddLetIn (aux ~localize loc context' body)
298 `AddLetIn unlocalized_body)
301 `AddLetIn (aux ~localize loc context' body)
303 `AddLetIn unlocalized_body
307 (fun (params, (name, typ), body, decr_idx) ->
308 let add_binders kind t =
310 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
313 aux ~localize loc context' (add_binders `Lambda body) in
315 aux_option ~localize loc context (Some `Type)
316 (HExtlib.map_option (add_binders `Pi) typ) in
318 match CicNotationUtil.cic_name_of_name name with
320 CicNotationPt.fail loc
321 "Recursive functions cannot be anonymous"
322 | NCic.Name name -> name
324 (name, decr_idx, cic_type, cic_body))
329 `Inductive -> NCic.Fix (n,inductiveFuns)
331 let coinductiveFuns =
333 (fun (name, _, typ, body) -> name, typ, body)
336 NCic.CoFix (n,coinductiveFuns)
338 let counter = ref ~-1 in
339 let build_term _ (var,_,ty,_) t =
341 NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t)
344 `AvoidLetInNoAppl n ->
345 let n' = List.length inductiveFuns - n in
347 | `AvoidLetIn (n,l) ->
348 let n' = List.length inductiveFuns - n in
349 NCic.Appl (fix_or_cofix n'::l)
350 | `AddLetIn cic_body ->
351 List.fold_right (build_term inductiveFuns) inductiveFuns
353 | CicNotationPt.Ident _
354 | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
355 | CicNotationPt.Ident (name, subst)
356 | CicNotationPt.Uri (name, subst) as ast ->
357 let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
359 if is_uri ast then raise Not_found;(* don't search the env for URIs *)
360 let index = find_in_context name context in
361 if subst <> None then
362 CicNotationPt.fail loc "Explicit substitutions not allowed here";
366 if is_uri ast then (* we have the URI, build the term out of it *)
368 CicUtil.term_of_uri (UriManager.uri_of_string name)
369 with UriManager.IllFormedUri _ ->
370 CicNotationPt.fail loc "Ill formed URI"
372 resolve env (Id name) ()
376 List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
383 List.assoc s ids_to_uris, aux ~localize loc context term
385 raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
387 | None -> List.map (fun uri -> uri, NCic.Implicit None) uris)
391 | NCic.Const (uri, []) ->
392 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
393 let uris = CicUtil.params_of_obj o in
394 NCic.Const (uri, mk_subst uris)
395 | NCic.Var (uri, []) ->
396 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
397 let uris = CicUtil.params_of_obj o in
398 NCic.Var (uri, mk_subst uris)
399 | NCic.MutInd (uri, i, []) ->
401 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
402 let uris = CicUtil.params_of_obj o in
403 NCic.MutInd (uri, i, mk_subst uris)
405 CicEnvironment.Object_not_found _ ->
406 (* if we are here it is probably the case that during the
407 definition of a mutual inductive type we have met an
408 occurrence of the type in one of its constructors.
409 However, the inductive type is not yet in the environment
411 (*here the explicit_named_substituion is assumed to be of length 0 *)
412 NCic.MutInd (uri,i,[]))
413 | NCic.MutConstruct (uri, i, j, []) ->
414 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
415 let uris = CicUtil.params_of_obj o in
416 NCic.MutConstruct (uri, i, j, mk_subst uris)
417 | NCic.Meta _ | NCic.Implicit _ as t ->
419 debug_print (lazy (sprintf
420 "Warning: %s must be instantiated with _[%s] but we do not enforce it"
424 (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
429 raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
431 CicEnvironment.CircularDependency _ ->
432 raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
433 | CicNotationPt.Implicit -> NCic.Implicit None
434 | CicNotationPt.UserInput -> NCic.Implicit (Some `Hole)
435 | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
436 | CicNotationPt.Meta (index, subst) ->
441 | Some term -> Some (aux ~localize loc context term))
444 NCic.Meta (index, cic_subst)
445 | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
446 | CicNotationPt.Sort `Set -> NCic.Sort NCic.Set
447 | CicNotationPt.Sort (`Type u) -> NCic.Sort (NCic.Type u)
448 | CicNotationPt.Sort (`CProp u) -> NCic.Sort (NCic.CProp u)
449 | CicNotationPt.Symbol (symbol, instance) ->
450 resolve env (Symbol (symbol, instance)) ()
451 | _ -> assert false (* god bless Bologna *)
452 and aux_option ~localize loc context annotation = function
453 | None -> NCic.Implicit annotation
454 | Some term -> aux ~localize loc context term
456 aux ~localize:true HExtlib.dummy_floc context ast
458 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
461 let context = List.map (function None -> NCic.Anonymous | Some (n,_) -> n) context in
462 interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
466 let domain_of_term ~context =
467 let context = List.map (fun x -> NCic.Name (fst x)) context in
468 Disambiguate.domain_of_ast_term ~context
471 module Make (C : DisambiguateTypes.Callbacks) = struct
472 module Disambiguator = Disambiguate.Make(C)
474 let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
475 ?(initial_ugraph = ()) ~aliases ~universe
476 (text,prefix_len,term)
479 if fresh_instances then CicNotationUtil.freshen_term term else term
481 let localization_tbl = NCic.NCicHash.create 503 in
482 Disambiguator.disambiguate_thing
483 ~dbd ~context ~metasenv ~initial_ugraph ~aliases
484 ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
485 ~domain_of_thing:domain_of_term
486 ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
487 ~refine_thing:refine_term (text,prefix_len,term)