2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
17 exception RefineFailure of string Lazy.t;;
18 exception Uncertain of string Lazy.t;;
19 exception AssertFailure of string Lazy.t;;
21 (* for internal use only; the integer is the number of surplus arguments *)
22 exception MoreArgsThanExpected of int * exn;;
24 let insert_coercions = ref true
25 let pack_coercions = ref true
30 if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
32 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
34 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
37 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
38 in profiler_eat_prods2.HExtlib.profile foo ()
40 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
41 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
44 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
46 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
49 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
50 in profiler_eat_prods.HExtlib.profile foo ()
52 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
53 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
56 let profiler = HExtlib.profile "CicRefine.fo_unif"
58 let fo_unif_subst subst context metasenv t1 t2 ugraph =
61 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
62 in profiler.HExtlib.profile foo ()
64 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
65 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
68 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
71 RefineFailure msg -> RefineFailure (f msg)
72 | Uncertain msg -> Uncertain (f msg)
73 | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
74 | Sys.Break -> raise exn
75 | _ -> prerr_endline (Printexc.to_string exn); assert false
79 Cic.CicHash.find localization_tbl t
81 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
84 raise (HExtlib.Localized (loc,exn'))
86 let relocalize localization_tbl oldt newt =
88 let infos = Cic.CicHash.find localization_tbl oldt in
89 Cic.CicHash.remove localization_tbl oldt;
90 Cic.CicHash.add localization_tbl newt infos;
98 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
99 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
102 let exp_impl metasenv subst context =
105 let (metasenv', idx) =
106 CicMkImplicit.mk_implicit_type metasenv subst context in
108 CicMkImplicit.identity_relocation_list_for_metavariable context in
109 metasenv', Cic.Meta (idx, irl)
111 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
112 metasenv', Cic.Meta (idx, [])
114 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
116 CicMkImplicit.identity_relocation_list_for_metavariable context in
117 metasenv', Cic.Meta (idx, irl)
121 let is_a_double_coercion t =
122 let rec subst_nth n x l =
125 | 0, _::tl -> x :: tl
126 | n, hd::tl -> hd :: subst_nth (n-1) x tl
128 let imp = Cic.Implicit None in
129 let dummyres = false,imp, imp,imp,imp in
132 (match CoercGraph.coerced_arg l1 with
133 | Some (Cic.Appl l2, pos1) ->
134 (match CoercGraph.coerced_arg l2 with
136 true, List.hd l1, List.hd l2, x,
137 Cic.Appl (subst_nth (pos1 + 1)
138 (Cic.Appl (subst_nth (pos2+1) imp l2)) l1)
144 let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
146 let len = List.length tlbody_and_type in
149 CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
150 " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
151 ") is here applied to " ^ string_of_int len ^
152 " arguments but here it can handle only up to " ^
153 string_of_int (len - residuals) ^ " arguments")
155 enrich localization_tbl he ~f:(fun _-> msg) exn
158 let mk_prod_of_metas metasenv context subst args =
159 let rec mk_prod metasenv context' = function
161 let (metasenv, idx) =
162 CicMkImplicit.mk_implicit_type metasenv subst context'
165 CicMkImplicit.identity_relocation_list_for_metavariable context'
167 metasenv,Cic.Meta (idx, irl)
169 let (metasenv, idx) =
170 CicMkImplicit.mk_implicit_type metasenv subst context'
173 CicMkImplicit.identity_relocation_list_for_metavariable context'
175 let meta = Cic.Meta (idx,irl) in
177 (* The name must be fresh for context. *)
178 (* Nevertheless, argty is well-typed only in context. *)
179 (* Thus I generate a name (name_hint) in context and *)
180 (* then I generate a name --- using the hint name_hint *)
181 (* --- that is fresh in context'. *)
183 FreshNamesGenerator.mk_fresh_name ~subst metasenv
184 (CicMetaSubst.apply_subst_context subst context)
186 ~typ:(CicMetaSubst.apply_subst subst argty)
188 FreshNamesGenerator.mk_fresh_name ~subst
189 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
191 let metasenv,target =
192 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
194 metasenv,Cic.Prod (name,meta,target)
196 mk_prod metasenv context args
199 let rec type_of_constant uri ugraph =
200 let module C = Cic in
201 let module R = CicReduction in
202 let module U = UriManager in
203 let _ = CicTypeChecker.typecheck uri in
206 CicEnvironment.get_cooked_obj ugraph uri
207 with Not_found -> assert false
210 C.Constant (_,_,ty,_,_) -> ty,u
211 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
215 (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
217 and type_of_variable uri ugraph =
218 let module C = Cic in
219 let module R = CicReduction in
220 let module U = UriManager in
221 let _ = CicTypeChecker.typecheck uri in
224 CicEnvironment.get_cooked_obj ugraph uri
225 with Not_found -> assert false
228 C.Variable (_,_,ty,_,_) -> ty,u
232 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
234 and type_of_mutual_inductive_defs uri i ugraph =
235 let module C = Cic in
236 let module R = CicReduction in
237 let module U = UriManager in
238 let _ = CicTypeChecker.typecheck uri in
241 CicEnvironment.get_cooked_obj ugraph uri
242 with Not_found -> assert false
245 C.InductiveDefinition (dl,_,_,_) ->
246 let (_,_,arity,_) = List.nth dl i in
251 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
253 and type_of_mutual_inductive_constr uri i j ugraph =
254 let module C = Cic in
255 let module R = CicReduction in
256 let module U = UriManager in
257 let _ = CicTypeChecker.typecheck uri in
260 CicEnvironment.get_cooked_obj ugraph uri
261 with Not_found -> assert false
264 C.InductiveDefinition (dl,_,_,_) ->
265 let (_,_,_,cl) = List.nth dl i in
266 let (_,ty) = List.nth cl (j-1) in
272 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
275 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
277 (* the check_branch function checks if a branch of a case is refinable.
278 It returns a pair (outype_instance,args), a subst and a metasenv.
279 outype_instance is the expected result of applying the case outtype
281 The problem is that outype is in general unknown, and we should
282 try to synthesize it from the above information, that is in general
283 a second order unification problem. *)
285 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
286 let module C = Cic in
287 let module R = CicReduction in
288 match R.whd ~subst context expectedtype with
290 (n,context,actualtype, [term]), subst, metasenv, ugraph
291 | C.Appl (C.MutInd (_,_,_)::tl) ->
292 let (_,arguments) = split tl left_args_no in
293 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
294 | C.Prod (_,so,de) ->
295 (* we expect that the actual type of the branch has the due
297 (match R.whd ~subst context actualtype with
298 C.Prod (name',so',de') ->
299 let subst, metasenv, ugraph1 =
300 fo_unif_subst subst context metasenv so so' ugraph in
302 (match CicSubstitution.lift 1 term with
303 C.Appl l -> C.Appl (l@[C.Rel 1])
304 | t -> C.Appl [t ; C.Rel 1]) in
305 (* we should also check that the name variable is anonymous in
306 the actual type de' ?? *)
308 ((Some (name',(C.Decl so)))::context)
309 metasenv subst left_args_no de' term' de ugraph1
310 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
311 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
313 and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
316 let rec type_of_aux subst metasenv context t ugraph =
317 let module C = Cic in
318 let module S = CicSubstitution in
319 let module U = UriManager in
320 let (t',_,_,_,_) as res =
325 match List.nth context (n - 1) with
326 Some (_,C.Decl ty) ->
327 t,S.lift n ty,subst,metasenv, ugraph
328 | Some (_,C.Def (_,ty)) ->
329 t,S.lift n ty,subst,metasenv, ugraph
331 enrich localization_tbl t
332 (RefineFailure (lazy "Rel to hidden hypothesis"))
335 enrich localization_tbl t
336 (RefineFailure (lazy "Not a closed term")))
337 | C.Var (uri,exp_named_subst) ->
338 let exp_named_subst',subst',metasenv',ugraph1 =
339 check_exp_named_subst
340 subst metasenv context exp_named_subst ugraph
342 let ty_uri,ugraph1 = type_of_variable uri ugraph in
344 CicSubstitution.subst_vars exp_named_subst' ty_uri
346 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
349 let (canonical_context, term,ty) =
350 CicUtil.lookup_subst n subst
352 let l',subst',metasenv',ugraph1 =
353 check_metasenv_consistency n subst metasenv context
354 canonical_context l ugraph
356 (* trust or check ??? *)
357 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
358 subst', metasenv', ugraph1
359 (* type_of_aux subst metasenv
360 context (CicSubstitution.subst_meta l term) *)
361 with CicUtil.Subst_not_found _ ->
362 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
363 let l',subst',metasenv', ugraph1 =
364 check_metasenv_consistency n subst metasenv context
365 canonical_context l ugraph
367 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
368 subst', metasenv',ugraph1)
369 | C.Sort (C.Type tno) ->
370 let tno' = CicUniv.fresh() in
372 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
373 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
375 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
376 | C.Sort (C.CProp tno) ->
377 let tno' = CicUniv.fresh() in
379 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
380 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
382 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
383 | C.Sort (C.Prop|C.Set) ->
384 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
385 | C.Implicit infos ->
386 let metasenv',t' = exp_impl metasenv subst context infos in
387 type_of_aux subst metasenv' context t' ugraph
389 let ty',_,subst',metasenv',ugraph1 =
390 type_of_aux subst metasenv context ty ugraph
392 let te',inferredty,subst'',metasenv'',ugraph2 =
393 type_of_aux subst' metasenv' context te ugraph1
395 let (te', ty'), subst''',metasenv''',ugraph3 =
396 coerce_to_something true localization_tbl te' inferredty ty'
397 subst'' metasenv'' context ugraph2
399 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
400 | C.Prod (name,s,t) ->
401 let s',sort1,subst',metasenv',ugraph1 =
402 type_of_aux subst metasenv context s ugraph
404 let s',sort1,subst', metasenv',ugraph1 =
405 coerce_to_sort localization_tbl
406 s' sort1 subst' context metasenv' ugraph1
408 let context_for_t = ((Some (name,(C.Decl s')))::context) in
409 let t',sort2,subst'',metasenv'',ugraph2 =
410 type_of_aux subst' metasenv'
411 context_for_t t ugraph1
413 let t',sort2,subst'',metasenv'',ugraph2 =
414 coerce_to_sort localization_tbl
415 t' sort2 subst'' context_for_t metasenv'' ugraph2
417 let sop,subst''',metasenv''',ugraph3 =
418 sort_of_prod localization_tbl subst'' metasenv''
419 context (name,s') t' (sort1,sort2) ugraph2
421 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
422 | C.Lambda (n,s,t) ->
423 let s',sort1,subst',metasenv',ugraph1 =
424 type_of_aux subst metasenv context s ugraph
426 let s',sort1,subst',metasenv',ugraph1 =
427 coerce_to_sort localization_tbl
428 s' sort1 subst' context metasenv' ugraph1
430 let context_for_t = ((Some (n,(C.Decl s')))::context) in
431 let t',type2,subst'',metasenv'',ugraph2 =
432 type_of_aux subst' metasenv' context_for_t t ugraph1
434 C.Lambda (n,s',t'),C.Prod (n,s',type2),
435 subst'',metasenv'',ugraph2
436 | C.LetIn (n,s,ty,t) ->
437 (* only to check if s is well-typed *)
438 let s',ty',subst',metasenv',ugraph1 =
439 type_of_aux subst metasenv context s ugraph in
440 let ty,_,subst',metasenv',ugraph1 =
441 type_of_aux subst' metasenv' context ty ugraph1 in
442 let subst',metasenv',ugraph1 =
444 fo_unif_subst subst' context metasenv'
448 enrich localization_tbl s' exn
451 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
452 context ^ " has type " ^
453 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
454 context ^ " but is here used with type " ^
455 CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
458 let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
460 let t',inferredty,subst'',metasenv'',ugraph2 =
461 type_of_aux subst' metasenv'
462 context_for_t t ugraph1
464 (* One-step LetIn reduction.
465 * Even faster than the previous solution.
466 * Moreover the inferred type is closer to the expected one.
468 C.LetIn (n,s',ty,t'),
469 CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
470 subst'',metasenv'',ugraph2
471 | C.Appl (he::((_::_) as tl)) ->
472 let he',hetype,subst',metasenv',ugraph1 =
473 type_of_aux subst metasenv context he ugraph
475 let tlbody_and_type,subst'',metasenv'',ugraph2 =
476 typeof_list subst' metasenv' context ugraph1 tl
478 let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
479 eat_prods true subst'' metasenv'' context
480 he' hetype tlbody_and_type ugraph2
482 let newappl = (C.Appl (coerced_he::coerced_args)) in
483 avoid_double_coercion
484 context subst''' metasenv''' ugraph3 newappl applty
485 | C.Appl _ -> assert false
486 | C.Const (uri,exp_named_subst) ->
487 let exp_named_subst',subst',metasenv',ugraph1 =
488 check_exp_named_subst subst metasenv context
489 exp_named_subst ugraph in
490 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
492 CicSubstitution.subst_vars exp_named_subst' ty_uri
494 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
495 | C.MutInd (uri,i,exp_named_subst) ->
496 let exp_named_subst',subst',metasenv',ugraph1 =
497 check_exp_named_subst subst metasenv context
498 exp_named_subst ugraph
500 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
502 CicSubstitution.subst_vars exp_named_subst' ty_uri in
503 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
504 | C.MutConstruct (uri,i,j,exp_named_subst) ->
505 let exp_named_subst',subst',metasenv',ugraph1 =
506 check_exp_named_subst subst metasenv context
507 exp_named_subst ugraph
510 type_of_mutual_inductive_constr uri i j ugraph1
513 CicSubstitution.subst_vars exp_named_subst' ty_uri
515 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
517 | C.MutCase (uri, i, outtype, term, pl) ->
518 (* first, get the inductive type (and noparams)
519 * in the environment *)
520 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
521 let _ = CicTypeChecker.typecheck uri in
522 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
524 C.InductiveDefinition (l,expl_params,parsno,_) ->
525 List.nth l i , expl_params, parsno, u
527 enrich localization_tbl t
529 (lazy ("Unkown mutual inductive definition " ^
530 U.string_of_uri uri)))
532 if List.length constructors <> List.length pl then
533 enrich localization_tbl t
535 (lazy "Wrong number of cases")) ;
536 let rec count_prod t =
537 match CicReduction.whd ~subst context t with
538 C.Prod (_, _, t) -> 1 + (count_prod t)
541 let no_args = count_prod arity in
542 (* now, create a "generic" MutInd *)
543 let metasenv,left_args =
544 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
546 let metasenv,right_args =
547 let no_right_params = no_args - no_left_params in
548 if no_right_params < 0 then assert false
549 else CicMkImplicit.n_fresh_metas
550 metasenv subst context no_right_params
552 let metasenv,exp_named_subst =
553 CicMkImplicit.fresh_subst metasenv subst context expl_params in
556 C.MutInd (uri,i,exp_named_subst)
559 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
561 (* check consistency with the actual type of term *)
562 let term',actual_type,subst,metasenv,ugraph1 =
563 type_of_aux subst metasenv context term ugraph in
564 let expected_type',_, subst, metasenv,ugraph2 =
565 type_of_aux subst metasenv context expected_type ugraph1
567 let actual_type = CicReduction.whd ~subst context actual_type in
568 let subst,metasenv,ugraph3 =
570 fo_unif_subst subst context metasenv
571 expected_type' actual_type ugraph2
574 enrich localization_tbl term' exn
577 CicMetaSubst.ppterm_in_context ~metasenv subst term'
578 context ^ " has type " ^
579 CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
580 context ^ " but is here used with type " ^
581 CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
584 let rec instantiate_prod t =
588 match CicReduction.whd ~subst context t with
590 instantiate_prod (CicSubstitution.subst he t') tl
593 let arity_instantiated_with_left_args =
594 instantiate_prod arity left_args in
595 (* TODO: check if the sort elimination
596 * is allowed: [(I q1 ... qr)|B] *)
597 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
599 (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
601 if left_args = [] then
602 (C.MutConstruct (uri,i,j,exp_named_subst))
605 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
607 let p',actual_type,subst,metasenv,ugraph1 =
608 type_of_aux subst metasenv context p ugraph
610 let constructor',expected_type, subst, metasenv,ugraph2 =
611 type_of_aux subst metasenv context constructor ugraph1
613 let outtypeinstance,subst,metasenv,ugraph3 =
615 check_branch 0 context metasenv subst
616 no_left_params actual_type constructor' expected_type
620 enrich localization_tbl constructor'
623 CicMetaSubst.ppterm_in_context metasenv subst p'
624 context ^ " has type " ^
625 CicMetaSubst.ppterm_in_context metasenv subst actual_type
626 context ^ " but is here used with type " ^
627 CicMetaSubst.ppterm_in_context metasenv subst expected_type
631 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
632 pl ([],List.length pl,[],subst,metasenv,ugraph3)
635 (* we are left to check that the outype matches his instances.
636 The easy case is when the outype is specified, that amount
637 to a trivial check. Otherwise, we should guess a type from
641 let outtype,outtypety, subst, metasenv,ugraph4 =
642 type_of_aux subst metasenv context outtype ugraph4 in
645 (let candidate,ugraph5,metasenv,subst =
646 let exp_name_subst, metasenv =
648 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
650 let uris = CicUtil.params_of_obj o in
652 fun uri (acc,metasenv) ->
653 let metasenv',new_meta =
654 CicMkImplicit.mk_implicit metasenv subst context
657 CicMkImplicit.identity_relocation_list_for_metavariable
660 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
664 match left_args,right_args with
665 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
667 let rec mk_right_args =
670 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
672 let right_args_no = List.length right_args in
673 let lifted_left_args =
674 List.map (CicSubstitution.lift right_args_no) left_args
676 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
677 (lifted_left_args @ mk_right_args right_args_no))
680 FreshNamesGenerator.mk_fresh_name ~subst metasenv
681 context Cic.Anonymous ~typ:ty
683 match outtypeinstances with
685 let extended_context =
686 let rec add_right_args =
688 Cic.Prod (name,ty,t) ->
689 Some (name,Cic.Decl ty)::(add_right_args t)
692 (Some (fresh_name,Cic.Decl ty))::
694 (add_right_args arity_instantiated_with_left_args))@
697 let metasenv,new_meta =
698 CicMkImplicit.mk_implicit metasenv subst extended_context
701 CicMkImplicit.identity_relocation_list_for_metavariable
704 let rec add_lambdas b =
706 Cic.Prod (name,ty,t) ->
707 Cic.Lambda (name,ty,(add_lambdas b t))
708 | _ -> Cic.Lambda (fresh_name, ty, b)
711 add_lambdas (Cic.Meta (new_meta,irl))
712 arity_instantiated_with_left_args
714 (Some candidate),ugraph4,metasenv,subst
715 | (constructor_args_no,_,instance,_)::tl ->
717 let instance',subst,metasenv =
718 CicMetaSubst.delift_rels subst metasenv
719 constructor_args_no instance
721 let candidate,ugraph,metasenv,subst =
723 fun (candidate_oty,ugraph,metasenv,subst)
724 (constructor_args_no,_,instance,_) ->
725 match candidate_oty with
726 | None -> None,ugraph,metasenv,subst
729 let instance',subst,metasenv =
730 CicMetaSubst.delift_rels subst metasenv
731 constructor_args_no instance
733 let subst,metasenv,ugraph =
734 fo_unif_subst subst context metasenv
737 candidate_oty,ugraph,metasenv,subst
739 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
740 | RefineFailure _ | Uncertain _ ->
741 None,ugraph,metasenv,subst
742 ) (Some instance',ugraph4,metasenv,subst) tl
745 | None -> None, ugraph,metasenv,subst
747 let rec add_lambdas n b =
749 Cic.Prod (name,ty,t) ->
750 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
752 Cic.Lambda (fresh_name, ty,
753 CicSubstitution.lift (n + 1) t)
756 (add_lambdas 0 t arity_instantiated_with_left_args),
757 ugraph,metasenv,subst
758 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
759 None,ugraph4,metasenv,subst
762 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
764 let subst,metasenv,ugraph =
766 fo_unif_subst subst context metasenv
767 candidate outtype ugraph5
769 exn -> assert false(* unification against a metavariable *)
771 C.MutCase (uri, i, outtype, term', pl'),
772 CicReduction.head_beta_reduce
773 (CicMetaSubst.apply_subst subst
774 (Cic.Appl (outtype::right_args@[term']))),
775 subst,metasenv,ugraph)
776 | _ -> (* easy case *)
777 let tlbody_and_type,subst,metasenv,ugraph4 =
778 typeof_list subst metasenv context ugraph4 (right_args @ [term'])
780 let _,_,_,subst,metasenv,ugraph4 =
781 eat_prods false subst metasenv context
782 outtype outtypety tlbody_and_type ugraph4
784 let _,_, subst, metasenv,ugraph5 =
785 type_of_aux subst metasenv context
786 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
788 let (subst,metasenv,ugraph6) =
790 (fun (subst,metasenv,ugraph)
791 p (constructor_args_no,context,instance,args)
796 CicSubstitution.lift constructor_args_no outtype
798 C.Appl (outtype'::args)
800 CicReduction.head_beta_reduce ~delta:false
801 ~upto:(List.length args) appl
804 fo_unif_subst subst context metasenv instance instance'
808 enrich localization_tbl p exn
811 CicMetaSubst.ppterm_in_context ~metasenv subst p
812 context ^ " has type " ^
813 CicMetaSubst.ppterm_in_context ~metasenv subst instance'
814 context ^ " but is here used with type " ^
815 CicMetaSubst.ppterm_in_context ~metasenv subst instance
817 (subst,metasenv,ugraph5) pl' outtypeinstances
819 C.MutCase (uri, i, outtype, term', pl'),
820 CicReduction.head_beta_reduce
821 (CicMetaSubst.apply_subst subst
822 (C.Appl(outtype::right_args@[term']))),
823 subst,metasenv,ugraph6)
825 let fl_ty',subst,metasenv,types,ugraph1,len =
827 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
828 let ty',_,subst',metasenv',ugraph1 =
829 type_of_aux subst metasenv context ty ugraph
831 fl @ [ty'],subst',metasenv',
832 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
833 :: types, ugraph, len+1
834 ) ([],subst,metasenv,[],ugraph,0) fl
836 let context' = types@context in
837 let fl_bo',subst,metasenv,ugraph2 =
839 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
840 let bo',ty_of_bo,subst,metasenv,ugraph1 =
841 type_of_aux subst metasenv context' bo ugraph in
842 let expected_ty = CicSubstitution.lift len ty in
843 let subst',metasenv',ugraph' =
845 fo_unif_subst subst context' metasenv
846 ty_of_bo expected_ty ugraph1
849 enrich localization_tbl bo exn
852 CicMetaSubst.ppterm_in_context ~metasenv subst bo
853 context' ^ " has type " ^
854 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
855 context' ^ " but is here used with type " ^
856 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
859 fl @ [bo'] , subst',metasenv',ugraph'
860 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
862 let ty = List.nth fl_ty' i in
863 (* now we have the new ty in fl_ty', the new bo in fl_bo',
864 * and we want the new fl with bo' and ty' injected in the right
867 let rec map3 f l1 l2 l3 =
870 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
873 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
876 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
878 let fl_ty',subst,metasenv,types,ugraph1,len =
880 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
881 let ty',_,subst',metasenv',ugraph1 =
882 type_of_aux subst metasenv context ty ugraph
884 fl @ [ty'],subst',metasenv',
885 Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
886 types, ugraph1, len+1
887 ) ([],subst,metasenv,[],ugraph,0) fl
889 let context' = types@context in
890 let fl_bo',subst,metasenv,ugraph2 =
892 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
893 let bo',ty_of_bo,subst,metasenv,ugraph1 =
894 type_of_aux subst metasenv context' bo ugraph in
895 let expected_ty = CicSubstitution.lift len ty in
896 let subst',metasenv',ugraph' =
898 fo_unif_subst subst context' metasenv
899 ty_of_bo expected_ty ugraph1
902 enrich localization_tbl bo exn
905 CicMetaSubst.ppterm_in_context ~metasenv subst bo
906 context' ^ " has type " ^
907 CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
908 context' ^ " but is here used with type " ^
909 CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
912 fl @ [bo'],subst',metasenv',ugraph'
913 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
915 let ty = List.nth fl_ty' i in
916 (* now we have the new ty in fl_ty', the new bo in fl_bo',
917 * and we want the new fl with bo' and ty' injected in the right
920 let rec map3 f l1 l2 l3 =
923 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
926 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
929 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
931 relocalize localization_tbl t t';
934 (* check_metasenv_consistency checks that the "canonical" context of a
935 metavariable is consitent - up to relocation via the relocation list l -
936 with the actual context *)
937 and check_metasenv_consistency
938 metano subst metasenv context canonical_context l ugraph
940 let module C = Cic in
941 let module R = CicReduction in
942 let module S = CicSubstitution in
943 let lifted_canonical_context =
947 | (Some (n,C.Decl t))::tl ->
948 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
949 | None::tl -> None::(aux (i+1) tl)
950 | (Some (n,C.Def (t,ty)))::tl ->
954 (S.subst_meta l (S.lift i t),
955 S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
957 aux 1 canonical_context
961 (fun (l,subst,metasenv,ugraph) t ct ->
964 l @ [None],subst,metasenv,ugraph
965 | Some t,Some (_,C.Def (ct,_)) ->
966 (*CSC: the following optimization is to avoid a possibly
967 expensive reduction that can be easily avoided and
968 that is quite frequent. However, this is better
969 handled using levels to control reduction *)
974 match List.nth context (n - 1) with
975 Some (_,C.Def (te,_)) -> S.lift n te
981 let subst',metasenv',ugraph' =
983 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
984 * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
985 fo_unif_subst subst context metasenv optimized_t ct ugraph
986 with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
988 l @ [Some t],subst',metasenv',ugraph'
989 | Some t,Some (_,C.Decl ct) ->
990 let t',inferredty,subst',metasenv',ugraph1 =
991 type_of_aux subst metasenv context t ugraph
993 let subst'',metasenv'',ugraph2 =
996 subst' context metasenv' inferredty ct ugraph1
997 with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
999 l @ [Some t'], subst'',metasenv'',ugraph2
1001 raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
1003 Invalid_argument _ ->
1007 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1008 (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1009 (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1011 and check_exp_named_subst metasubst metasenv context tl ugraph =
1012 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
1014 [] -> [],metasubst,metasenv,ugraph
1016 let ty_uri,ugraph1 = type_of_variable uri ugraph in
1018 CicSubstitution.subst_vars substs ty_uri in
1019 (* CSC: why was this code here? it is wrong
1020 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1021 Cic.Variable (_,Some bo,_,_) ->
1023 (RefineFailure (lazy
1024 "A variable with a body can not be explicit substituted"))
1025 | Cic.Variable (_,None,_,_) -> ()
1028 (RefineFailure (lazy
1029 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1032 let t',typeoft,metasubst',metasenv',ugraph2 =
1033 type_of_aux metasubst metasenv context t ugraph1 in
1034 let subst = uri,t' in
1035 let metasubst'',metasenv'',ugraph3 =
1038 metasubst' context metasenv' typeoft typeofvar ugraph2
1040 raise (RefineFailure (lazy
1041 ("Wrong Explicit Named Substitution: " ^
1042 CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1043 " not unifiable with " ^
1044 CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1046 (* FIXME: no mere tail recursive! *)
1047 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1048 check_exp_named_subst_aux
1049 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1051 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1053 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1056 and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1059 let module C = Cic in
1060 let context_for_t2 = (Some (name,C.Decl s))::context in
1061 let t1'' = CicReduction.whd ~subst context t1 in
1062 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1063 match (t1'', t2'') with
1064 | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
1065 (* different than Coq manual!!! *)
1066 C.Sort s2,subst,metasenv,ugraph
1067 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1068 let t' = CicUniv.fresh() in
1070 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1071 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1072 C.Sort (C.Type t'),subst,metasenv,ugraph2
1074 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1075 | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
1076 let t' = CicUniv.fresh() in
1078 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1079 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1080 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1082 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1083 | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
1084 let t' = CicUniv.fresh() in
1086 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1087 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1088 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1090 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1091 | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
1092 let t' = CicUniv.fresh() in
1094 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1095 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1096 C.Sort (C.Type t'),subst,metasenv,ugraph2
1098 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1099 | (C.Sort _,C.Sort (C.Type t1)) ->
1100 C.Sort (C.Type t1),subst,metasenv,ugraph
1101 | (C.Sort _,C.Sort (C.CProp t1)) ->
1102 C.Sort (C.CProp t1),subst,metasenv,ugraph
1103 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1104 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1105 (* TODO how can we force the meta to become a sort? If we don't we
1106 * break the invariant that refine produce only well typed terms *)
1107 (* TODO if we check the non meta term and if it is a sort then we
1108 * are likely to know the exact value of the result e.g. if the rhs
1109 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1110 let (metasenv,idx) =
1111 CicMkImplicit.mk_implicit_sort metasenv subst in
1112 let (subst, metasenv,ugraph1) =
1114 fo_unif_subst subst context_for_t2 metasenv
1115 (C.Meta (idx,[])) t2'' ugraph
1116 with _ -> assert false (* unification against a metavariable *)
1118 t2'',subst,metasenv,ugraph1
1121 enrich localization_tbl s
1125 "%s is supposed to be a type, but its type is %s"
1126 (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1127 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1129 enrich localization_tbl t
1133 "%s is supposed to be a type, but its type is %s"
1134 (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1135 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1137 and avoid_double_coercion context subst metasenv ugraph t ty =
1138 if not !pack_coercions then
1139 t,ty,subst,metasenv,ugraph
1141 let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1143 let source_carr = CoercGraph.source_of c2 in
1144 let tgt_carr = CicMetaSubst.apply_subst subst ty in
1145 (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1147 | CoercGraph.SomeCoercion candidates ->
1149 HExtlib.list_findopt
1150 (function (metasenv,last,c) ->
1152 | c when not (CoercGraph.is_composite c) ->
1153 debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1156 let subst,metasenv,ugraph =
1157 fo_unif_subst subst context metasenv last head ugraph in
1158 debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1163 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1164 let newt,_,subst,metasenv,ugraph =
1165 type_of_aux subst metasenv context c ugraph in
1166 debug_print (lazy "tipa...");
1167 let subst, metasenv, ugraph =
1168 (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1169 fo_unif_subst subst context metasenv newt t ugraph
1171 debug_print (lazy "unifica...");
1172 Some (newt, ty, subst, metasenv, ugraph)
1174 | RefineFailure s | Uncertain s when not !pack_coercions->
1175 debug_print s; debug_print (lazy "stop\n");None
1176 | RefineFailure s | Uncertain s ->
1177 debug_print s;debug_print (lazy "goon\n");
1179 let old_pack_coercions = !pack_coercions in
1180 pack_coercions := false; (* to avoid diverging *)
1181 let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1182 type_of_aux subst metasenv context c1_c2_implicit ugraph
1184 pack_coercions := old_pack_coercions;
1186 is_a_double_coercion refined_c1_c2_implicit
1192 match refined_c1_c2_implicit with
1193 | Cic.Appl l -> HExtlib.list_last l
1196 let subst, metasenv, ugraph =
1197 try fo_unif_subst subst context metasenv
1199 with RefineFailure s| Uncertain s->
1200 debug_print s;assert false
1202 let subst, metasenv, ugraph =
1203 fo_unif_subst subst context metasenv
1204 refined_c1_c2_implicit t ugraph
1206 Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1208 | RefineFailure s | Uncertain s ->
1209 pack_coercions := true;debug_print s;None
1210 | exn -> pack_coercions := true; raise exn))
1213 (match selected with
1217 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1218 t, ty, subst, metasenv, ugraph)
1219 | _ -> t, ty, subst, metasenv, ugraph)
1221 t, ty, subst, metasenv, ugraph
1223 and typeof_list subst metasenv context ugraph l =
1224 let tlbody_and_type,subst,metasenv,ugraph =
1226 (fun x (res,subst,metasenv,ugraph) ->
1227 let x',ty,subst',metasenv',ugraph1 =
1228 type_of_aux subst metasenv context x ugraph
1230 (x', ty)::res,subst',metasenv',ugraph1
1231 ) l ([],subst,metasenv,ugraph)
1233 tlbody_and_type,subst,metasenv,ugraph
1236 allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1238 (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1239 let fix_arity n metasenv context subst he hetype ugraph =
1240 let hetype = CicMetaSubst.apply_subst subst hetype in
1241 (* instead of a dummy functional type we may create the real product
1242 * using args_bo_and_ty, but since coercions lookup ignores the
1243 * actual ariety we opt for the simple solution *)
1244 let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
1245 match CoercGraph.look_for_coercion metasenv subst context hetype fty with
1246 | CoercGraph.NoCoercion -> []
1247 | CoercGraph.NotHandled ->
1248 raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1249 | CoercGraph.SomeCoercionToTgt candidates
1250 | CoercGraph.SomeCoercion candidates ->
1252 (fun (metasenv,last,coerc) ->
1254 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1256 let subst,metasenv,ugraph =
1257 fo_unif_subst subst context metasenv last he ugraph in
1258 debug_print (lazy ("New head: "^ pp coerc));
1260 CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1263 debug_print (lazy (" has type: "^ pp tty));
1264 Some (coerc,tty,subst,metasenv,ugraph)
1266 | Uncertain _ | RefineFailure _
1267 | HExtlib.Localized (_,Uncertain _)
1268 | HExtlib.Localized (_,RefineFailure _) -> None
1269 | exn -> assert false)
1272 (* aux function to process the type of the head and the args in parallel *)
1273 let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1275 | [] -> newargs,subst,metasenv,he,hetype,ugraph
1276 | (hete, hety)::tl as args ->
1277 match (CicReduction.whd ~subst context hetype) with
1278 | Cic.Prod (n,s,t) ->
1279 let arg,subst,metasenv,ugraph =
1280 coerce_to_something allow_coercions localization_tbl
1281 hete hety s subst metasenv context ugraph in
1283 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1284 ugraph (newargs@[arg]) tl
1287 match he, newargs with
1289 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1290 | _ -> Cic.Appl (he::List.map fst newargs)
1292 (*{{{*) debug_print (lazy
1294 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1295 "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1296 "\n but is applyed to: " ^ String.concat ";"
1297 (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1298 let possible_fixes =
1299 fix_arity (List.length args) metasenv context subst he hetype
1302 HExtlib.list_findopt
1303 (fun (he,hetype,subst,metasenv,ugraph) ->
1304 (* {{{ *)debug_print (lazy ("Try fix: "^
1305 CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1306 debug_print (lazy (" of type: "^
1307 CicMetaSubst.ppterm_in_context
1308 ~metasenv subst hetype context)); (* }}} *)
1310 Some (eat_prods_and_args
1311 metasenv subst context he hetype ugraph [] args)
1313 | RefineFailure _ | Uncertain _
1314 | HExtlib.Localized (_,RefineFailure _)
1315 | HExtlib.Localized (_,Uncertain _) -> None)
1321 (MoreArgsThanExpected
1322 (List.length args, RefineFailure (lazy "")))
1324 (* first we check if we are in the simple case of a meta closed term *)
1325 let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1326 if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1327 (* this optimization is to postpone fix_arity (the most common case)*)
1328 subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1330 (* this (says CSC) is also useful to infer dependent types *)
1331 let pristinemenv = metasenv in
1332 let metasenv,hetype' =
1333 mk_prod_of_metas metasenv context subst args_bo_and_ty
1336 let subst,metasenv,ugraph =
1337 fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1339 subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1340 with RefineFailure _ | Uncertain _ ->
1341 subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1343 let coerced_args,subst,metasenv,he,t,ugraph =
1346 metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1348 MoreArgsThanExpected (residuals,exn) ->
1349 more_args_than_expected localization_tbl metasenv
1350 subst he context hetype' residuals args_bo_and_ty exn
1352 he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1354 and coerce_to_something
1355 allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1357 let module CS = CicSubstitution in
1358 let module CR = CicReduction in
1359 let cs_subst = CS.subst ~avoid_beta_redexes:true in
1360 let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1361 debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1363 CoercGraph.look_for_coercion metasenv subst context infty expty
1366 | CoercGraph.NoCoercion
1367 | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
1368 "coerce_atom_to_something fails since no coercions found"))
1369 | CoercGraph.NotHandled when
1370 not (CicUtil.is_meta_closed infty) ||
1371 not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
1372 "coerce_atom_to_something fails since carriers have metas"))
1373 | CoercGraph.NotHandled -> raise (RefineFailure (lazy
1374 "coerce_atom_to_something fails since no coercions found"))
1375 | CoercGraph.SomeCoercion candidates ->
1376 debug_print (lazy (string_of_int (List.length candidates) ^
1377 " candidates found"));
1378 let uncertain = ref false in
1382 (fun (metasenv,last,c) ->
1384 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1385 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1387 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1388 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1390 debug_print (lazy ("FO_UNIF_SUBST: " ^
1391 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1392 let subst,metasenv,ugraph =
1393 fo_unif_subst subst context metasenv last t ugraph
1395 let newt,newhety,subst,metasenv,ugraph =
1396 type_of_aux subst metasenv context c ugraph in
1397 let newt, newty, subst, metasenv, ugraph =
1398 avoid_double_coercion context subst metasenv ugraph newt expty
1400 let subst,metasenv,ugraph =
1401 fo_unif_subst subst context metasenv newhety expty ugraph in
1402 Some ((newt,newty), subst, metasenv, ugraph)
1404 | Uncertain _ -> uncertain := true; None
1405 | RefineFailure _ -> None)
1410 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1418 | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1419 | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1421 let rec coerce_to_something_aux
1422 t infty expty subst metasenv context ugraph
1425 let subst, metasenv, ugraph =
1426 fo_unif_subst subst context metasenv infty expty ugraph
1428 (t, expty), subst, metasenv, ugraph
1429 with (Uncertain _ | RefineFailure _ as exn)
1430 when allow_coercions && !insert_coercions ->
1431 let whd = CicReduction.whd ~delta:false in
1432 let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1433 let infty = clean infty subst context in
1434 let expty = clean expty subst context in
1435 let t = clean t subst context in
1436 (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1437 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1438 CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1439 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1440 let (coerced,_),subst,metasenv,_ as result =
1441 match infty, expty, t with
1442 | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1443 (*{{{*) debug_print (lazy "FIX");
1445 [name,i,_(* infty *),bo] ->
1447 Some (Cic.Name name,Cic.Decl expty)::context in
1448 let (rel1, _), subst, metasenv, ugraph =
1449 coerce_to_something_aux (Cic.Rel 1)
1450 (CS.lift 1 expty) (CS.lift 1 infty) subst
1451 metasenv context_bo ugraph in
1452 let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1453 let (bo,_), subst, metasenv, ugraph =
1454 coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1456 metasenv context_bo ugraph
1458 (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1459 | _ -> assert false (* not implemented yet *)) (*}}}*)
1460 | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1461 (*{{{*) debug_print (lazy "CASE");
1462 (* {{{ helper functions *)
1463 let get_cl_and_left_p uri tyno outty ugraph =
1464 match CicEnvironment.get_obj ugraph uri with
1465 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1468 match CicReduction.whd ~delta:false ctx t with
1469 | Cic.Prod (name,src,tgt) ->
1470 let ctx = Some (name, Cic.Decl src) :: ctx in
1476 let rec skip_lambda_delifting t n =
1479 | Cic.Lambda (_,_,t),n ->
1480 skip_lambda_delifting
1481 (CS.subst (Cic.Implicit None) t) (n - 1)
1484 let get_l_r_p n = function
1485 | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1486 | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1487 HExtlib.split_nth n args
1490 let _, _, ty, cl = List.nth tl tyno in
1491 let pis = count_pis ty in
1492 let rno = pis - leftno in
1493 let t = skip_lambda_delifting outty rno in
1494 let left_p, _ = get_l_r_p leftno t in
1495 let instantiale_with_left cl =
1499 (fun t p -> match t with
1500 | Cic.Prod (_,_,t) ->
1506 let cl = instantiale_with_left (List.map snd cl) in
1507 cl, left_p, leftno, rno, ugraph
1510 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1513 let rec mkr n = function
1514 | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1517 CicReplace.replace_lifting
1518 ~equality:(fun _ -> CicUtil.alpha_equivalence)
1520 ~what:(matched::right_p)
1521 ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1525 | Cic.Lambda (name, src, tgt),_ ->
1526 Cic.Lambda (name, src,
1527 keep_lambdas_and_put_expty
1528 (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1529 (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1532 let eq_uri, eq, eq_refl =
1533 match LibraryObjects.eq_URI () with
1534 | None -> HLog.warn "no default equality"; raise exn
1535 | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1538 metasenv subst context uri tyno cty outty mty m leftno i
1540 let rec aux context outty par k mty m = function
1541 | Cic.Prod (name, src, tgt) ->
1544 (Some (name, Cic.Decl src) :: context)
1545 (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1546 (CS.lift 1 mty) (CS.lift 1 m) tgt
1548 Cic.Prod (name, src, t), k
1551 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1552 if par <> [] then Cic.Appl (k::par) else k
1554 Cic.Prod (Cic.Name "p",
1555 Cic.Appl [eq; mty; m; k],
1557 (CR.head_beta_reduce ~delta:false
1558 (Cic.Appl [outty;k])))),k
1559 | Cic.Appl (Cic.MutInd _::pl) ->
1560 let left_p,right_p = HExtlib.split_nth leftno pl in
1561 let has_rights = right_p <> [] in
1563 let k = Cic.MutConstruct (uri,tyno,i,[]) in
1564 Cic.Appl (k::left_p@par)
1568 CicTypeChecker.type_of_aux' ~subst metasenv context k
1569 CicUniv.oblivion_ugraph
1571 | Cic.Appl (Cic.MutInd _::args),_ ->
1572 snd (HExtlib.split_nth leftno args)
1574 with CicTypeChecker.TypeCheckerFailure _-> assert false
1577 CR.head_beta_reduce ~delta:false
1578 (Cic.Appl (outty ::right_p @ [k])),k
1580 Cic.Prod (Cic.Name "p",
1581 Cic.Appl [eq; mty; m; k],
1583 (CR.head_beta_reduce ~delta:false
1584 (Cic.Appl (outty ::right_p @ [k]))))),k
1587 aux context outty [] 1 mty m cty
1589 let add_lambda_for_refl_m pbo rno mty m k cty =
1590 (* k lives in the right context *)
1591 if rno <> 0 then pbo else
1592 let rec aux mty m = function
1593 | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1594 Cic.Lambda (name,src,
1595 (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1597 Cic.Lambda (Cic.Name "p",
1598 Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1602 let add_pi_for_refl_m new_outty mty m rno =
1603 if rno <> 0 then new_outty else
1604 let rec aux m mty = function
1605 | Cic.Lambda (name, src, tgt) ->
1606 Cic.Lambda (name, src,
1607 aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1610 (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1614 in (* }}} end helper functions *)
1615 (* constructors types with left params already instantiated *)
1616 let outty = CicMetaSubst.apply_subst subst outty in
1617 let cl, left_p, leftno,rno,ugraph =
1618 get_cl_and_left_p uri tyno outty ugraph
1623 CicTypeChecker.type_of_aux' ~subst metasenv context m
1624 CicUniv.oblivion_ugraph
1626 | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
1627 | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
1628 snd (HExtlib.split_nth leftno args), mty
1630 with CicTypeChecker.TypeCheckerFailure _ ->
1631 raise (AssertFailure(lazy "already ill-typed matched term"))
1634 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1637 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1638 ~metasenv subst new_outty context));
1639 let _,pl,subst,metasenv,ugraph =
1641 (fun cty pbo (i, acc, s, menv, ugraph) ->
1642 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1643 * (new_)outty right_par (K_i left_par k_par) *)
1645 add_params menv s context uri tyno
1646 cty outty mty m leftno i in
1648 (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1649 ~metasenv subst infty_pbo context));
1650 let expty_pbo, k = (* k is (K_i left_par k_par) *)
1651 add_params menv s context uri tyno
1652 cty new_outty mty m leftno i in
1654 (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1655 ~metasenv subst expty_pbo context));
1656 let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1658 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1659 ~metasenv subst pbo context));
1660 let (pbo, _), subst, metasenv, ugraph =
1661 coerce_to_something_aux pbo infty_pbo expty_pbo
1662 s menv context ugraph
1665 (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1666 ~metasenv subst pbo context));
1667 (i-1, pbo::acc, subst, metasenv, ugraph))
1668 cl pl (List.length pl, [], subst, metasenv, ugraph)
1670 let new_outty = add_pi_for_refl_m new_outty mty m rno in
1672 (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1673 ~metasenv subst new_outty context));
1676 let refl_m=Cic.Appl[eq_refl;mty;m]in
1677 Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1679 Cic.MutCase(uri,tyno,new_outty,m,pl)
1681 (t, expty), subst, metasenv, ugraph (*}}}*)
1682 | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1683 (*{{{*) debug_print (lazy "LAM");
1685 FreshNamesGenerator.mk_fresh_name
1686 ~subst metasenv context ~typ:src2 Cic.Anonymous
1688 let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1689 (* contravariant part: the argument of f:src->ty *)
1690 let (rel1, _), subst, metasenv, ugraph =
1691 coerce_to_something_aux
1692 (Cic.Rel 1) (CS.lift 1 src2)
1693 (CS.lift 1 src) subst metasenv context_src2 ugraph
1695 (* covariant part: the result of f(c x); x:src2; (c x):src *)
1698 | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1699 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1701 (* we fix the possible dependency problem in the source ty *)
1702 let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1703 let (bo, _), subst, metasenv, ugraph =
1704 coerce_to_something_aux
1705 bo ty ty2 subst metasenv context_src2 ugraph
1707 let coerced = Cic.Lambda (name_t,src2, bo) in
1708 (coerced, expty), subst, metasenv, ugraph (*}}}*)
1710 (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1711 ~metasenv subst infty context ^ " ==> " ^
1712 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1713 coerce_atom_to_something
1714 t infty expty subst metasenv context ugraph (*}}}*)
1716 debug_print (lazy ("COERCE TO SOMETHING END: "^
1717 CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1721 coerce_to_something_aux t infty expty subst metasenv context ugraph
1722 with Uncertain _ | RefineFailure _ as exn ->
1725 CicMetaSubst.ppterm_in_context metasenv subst t context ^
1726 " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1727 infty context ^ " but is here used with type " ^
1728 CicMetaSubst.ppterm_in_context metasenv subst expty context)
1730 enrich localization_tbl ~f t exn
1732 and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1733 match CicReduction.whd ~delta:false ~subst context infty with
1734 | Cic.Meta _ | Cic.Sort _ ->
1735 t,infty, subst, metasenv, ugraph
1737 debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1738 ~metasenv subst src context));
1739 let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1741 let (t, ty_t), subst, metasenv, ugraph =
1742 coerce_to_something true
1743 localization_tbl t src tgt subst metasenv context ugraph
1745 debug_print (lazy ("COERCE TO SORT END: "^
1746 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1747 t, ty_t, subst, metasenv, ugraph
1748 with HExtlib.Localized (_, exn) ->
1750 lazy ("(7)The term " ^
1751 CicMetaSubst.ppterm_in_context ~metasenv subst t context
1752 ^ " is not a type since it has type " ^
1753 CicMetaSubst.ppterm_in_context ~metasenv subst src context
1754 ^ " that is not a sort")
1756 enrich localization_tbl ~f t exn
1759 (* eat prods ends here! *)
1761 let t',ty,subst',metasenv',ugraph1 =
1762 type_of_aux [] metasenv context t ugraph
1764 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1765 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1766 (* Andrea: ho rimesso qui l'applicazione della subst al
1767 metasenv dopo che ho droppato l'invariante che il metsaenv
1768 e' sempre istanziato *)
1769 let substituted_metasenv =
1770 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1772 (* substituted_t,substituted_ty,substituted_metasenv *)
1773 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1775 if clean_dummy_dependent_types then
1776 FreshNamesGenerator.clean_dummy_dependent_types substituted_t
1777 else substituted_t in
1779 if clean_dummy_dependent_types then
1780 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
1781 else substituted_ty in
1782 let cleaned_metasenv =
1783 if clean_dummy_dependent_types then
1785 (function (n,context,ty) ->
1786 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1791 | Some (n, Cic.Decl t) ->
1793 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1794 | Some (n, Cic.Def (bo,ty)) ->
1795 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1796 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
1798 Some (n, Cic.Def (bo',ty'))
1802 ) substituted_metasenv
1804 substituted_metasenv
1806 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1809 let undebrujin uri typesno tys t =
1812 (fun (name,_,_,_) (i,t) ->
1813 (* here the explicit_named_substituion is assumed to be *)
1815 let t' = Cic.MutInd (uri,i,[]) in
1816 let t = CicSubstitution.subst t' t in
1818 ) tys (typesno - 1,t))
1820 let map_first_n n start f g l =
1821 let rec aux acc k l =
1824 | [] -> raise (Invalid_argument "map_first_n")
1825 | hd :: tl -> f hd k (aux acc (k+1) tl)
1831 (*CSC: this is a very rough approximation; to be finished *)
1832 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1833 let subst,metasenv,ugraph,tys =
1835 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1836 let subst,metasenv,ugraph,cl =
1838 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1839 let rec aux ctx k subst = function
1840 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1841 let subst,metasenv,ugraph,tl =
1843 (subst,metasenv,ugraph,[])
1844 (fun t n (subst,metasenv,ugraph,acc) ->
1845 let subst,metasenv,ugraph =
1847 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1849 subst,metasenv,ugraph,(t::acc))
1850 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1853 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1854 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1855 subst,metasenv,ugraph,t
1856 | Cic.Prod (name,s,t) ->
1857 let ctx = (Some (name,Cic.Decl s))::ctx in
1858 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1859 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1863 (lazy "not well formed constructor type"))
1865 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1866 subst,metasenv,ugraph,(name,ty) :: acc)
1867 cl (subst,metasenv,ugraph,[])
1869 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1870 tys ([],metasenv,ugraph,[])
1872 let substituted_tys =
1874 (fun (name,ind,arity,cl) ->
1876 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1878 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1881 metasenv,ugraph,substituted_tys
1883 let typecheck metasenv uri obj ~localization_tbl =
1884 let ugraph = CicUniv.oblivion_ugraph in
1886 Cic.Constant (name,Some bo,ty,args,attrs) ->
1887 (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
1888 since type_of_aux' destroys localization information (which are
1889 preserved by type_of_aux *)
1892 Cic.CicHash.find localization_tbl bo
1894 HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
1896 let bo',boty,metasenv,ugraph =
1897 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1898 let ty',_,metasenv,ugraph =
1899 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1900 let subst,metasenv,ugraph =
1902 fo_unif_subst [] [] metasenv boty ty' ugraph
1905 | Uncertain _ as exn ->
1908 CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
1910 CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
1911 " but is here used with type " ^
1912 CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
1916 RefineFailure _ -> RefineFailure msg
1917 | Uncertain _ -> Uncertain msg
1920 raise (HExtlib.Localized (loc exn',exn'))
1922 let bo' = CicMetaSubst.apply_subst subst bo' in
1923 let ty' = CicMetaSubst.apply_subst subst ty' in
1924 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1925 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1926 | Cic.Constant (name,None,ty,args,attrs) ->
1927 let ty',_,metasenv,ugraph =
1928 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1930 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1931 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1932 assert (metasenv' = metasenv);
1933 (* Here we do not check the metasenv for correctness *)
1934 let bo',boty,metasenv,ugraph =
1935 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1936 let ty',sort,metasenv,ugraph =
1937 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1941 (* instead of raising Uncertain, let's hope that the meta will become
1944 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1946 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1947 let bo' = CicMetaSubst.apply_subst subst bo' in
1948 let ty' = CicMetaSubst.apply_subst subst ty' in
1949 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1950 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1951 | Cic.Variable _ -> assert false (* not implemented *)
1952 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1953 (*CSC: this code is greately simplified and many many checks are missing *)
1954 (*CSC: e.g. the constructors are not required to build their own types, *)
1955 (*CSC: the arities are not required to have as type a sort, etc. *)
1956 let uri = match uri with Some uri -> uri | None -> assert false in
1957 let typesno = List.length tys in
1958 (* first phase: we fix only the types *)
1959 let metasenv,ugraph,tys =
1961 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1962 let ty',_,metasenv,ugraph =
1963 (* clean_dummy_dependent_types: false to avoid cleaning the names
1964 of the left products, that must be identical to those of the
1965 constructors; however, non-left products should probably be
1967 type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
1968 metasenv [] ty ugraph
1970 metasenv,ugraph,(name,b,ty',cl)::res
1971 ) tys (metasenv,ugraph,[]) in
1973 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1974 (* second phase: we fix only the constructors *)
1975 let saved_menv = metasenv in
1976 let metasenv,ugraph,tys =
1978 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1979 let metasenv,ugraph,cl' =
1981 (fun (name,ty) (metasenv,ugraph,res) ->
1983 CicTypeChecker.debrujin_constructor
1984 ~cb:(relocalize localization_tbl) uri typesno [] ty in
1985 let ty',_,metasenv,ugraph =
1986 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1987 let ty' = undebrujin uri typesno tys ty' in
1988 metasenv@saved_menv,ugraph,(name,ty')::res
1989 ) cl (metasenv,ugraph,[])
1991 metasenv,ugraph,(name,b,ty,cl')::res
1992 ) tys (metasenv,ugraph,[]) in
1993 (* third phase: we check the positivity condition *)
1994 let metasenv,ugraph,tys =
1995 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1997 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
2000 (* sara' piu' veloce che raffinare da zero? mah.... *)
2001 let pack_coercion metasenv ctx t =
2002 let module C = Cic in
2003 let rec merge_coercions ctx =
2004 let aux = (fun (u,t) -> u,merge_coercions ctx t) in
2006 | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
2007 | C.Meta (n,subst) ->
2010 (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
2013 | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
2014 | C.Prod (name,so,dest) ->
2015 let ctx' = (Some (name,C.Decl so))::ctx in
2016 C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
2017 | C.Lambda (name,so,dest) ->
2018 let ctx' = (Some (name,C.Decl so))::ctx in
2019 C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
2020 | C.LetIn (name,so,ty,dest) ->
2021 let ctx' = Some (name,(C.Def (so,ty)))::ctx in
2023 (name, merge_coercions ctx so, merge_coercions ctx ty,
2024 merge_coercions ctx' dest)
2026 let l = List.map (merge_coercions ctx) l in
2028 let b,_,_,_,_ = is_a_double_coercion t in
2030 let ugraph = CicUniv.oblivion_ugraph in
2031 let old_insert_coercions = !insert_coercions in
2032 insert_coercions := false;
2033 let newt, _, menv, _ =
2035 type_of_aux' metasenv ctx t ugraph
2036 with RefineFailure _ | Uncertain _ ->
2039 insert_coercions := old_insert_coercions;
2040 if metasenv <> [] || menv = [] then
2043 (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2046 | C.Var (uri,exp_named_subst) ->
2047 let exp_named_subst = List.map aux exp_named_subst in
2048 C.Var (uri, exp_named_subst)
2049 | C.Const (uri,exp_named_subst) ->
2050 let exp_named_subst = List.map aux exp_named_subst in
2051 C.Const (uri, exp_named_subst)
2052 | C.MutInd (uri,tyno,exp_named_subst) ->
2053 let exp_named_subst = List.map aux exp_named_subst in
2054 C.MutInd (uri,tyno,exp_named_subst)
2055 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2056 let exp_named_subst = List.map aux exp_named_subst in
2057 C.MutConstruct (uri,tyno,consno,exp_named_subst)
2058 | C.MutCase (uri,tyno,out,te,pl) ->
2059 let pl = List.map (merge_coercions ctx) pl in
2060 C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2061 | C.Fix (fno, fl) ->
2064 (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2069 (fun (name,idx,ty,bo) ->
2070 (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2074 | C.CoFix (fno, fl) ->
2077 (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2082 (fun (name,ty,bo) ->
2083 (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2088 merge_coercions ctx t
2091 let pack_coercion_metasenv conjectures = conjectures (*
2093 TASSI: this code war written when coercions were a toy,
2094 now packing coercions involves unification thus
2095 the metasenv may change, and this pack coercion
2096 does not handle that.
2098 let module C = Cic in
2100 (fun (i, ctx, ty) ->
2106 Some (name, C.Decl t) ->
2107 Some (name, C.Decl (pack_coercion conjectures ctx t))
2108 | Some (name, C.Def (t,None)) ->
2109 Some (name,C.Def (pack_coercion conjectures ctx t,None))
2110 | Some (name, C.Def (t,Some ty)) ->
2111 Some (name, C.Def (pack_coercion conjectures ctx t,
2112 Some (pack_coercion conjectures ctx ty)))
2118 ((i,ctx,pack_coercion conjectures ctx ty))
2123 let pack_coercion_obj obj = obj (*
2125 TASSI: this code war written when coercions were a toy,
2126 now packing coercions involves unification thus
2127 the metasenv may change, and this pack coercion
2128 does not handle that.
2130 let module C = Cic in
2132 | C.Constant (id, body, ty, params, attrs) ->
2136 | Some body -> Some (pack_coercion [] [] body)
2138 let ty = pack_coercion [] [] ty in
2139 C.Constant (id, body, ty, params, attrs)
2140 | C.Variable (name, body, ty, params, attrs) ->
2144 | Some body -> Some (pack_coercion [] [] body)
2146 let ty = pack_coercion [] [] ty in
2147 C.Variable (name, body, ty, params, attrs)
2148 | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2149 let conjectures = pack_coercion_metasenv conjectures in
2150 let body = pack_coercion conjectures [] body in
2151 let ty = pack_coercion conjectures [] ty in
2152 C.CurrentProof (name, conjectures, body, ty, params, attrs)
2153 | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2156 (fun (name, ind, arity, cl) ->
2157 let arity = pack_coercion [] [] arity in
2159 List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2161 (name, ind, arity, cl))
2164 C.InductiveDefinition (indtys, params, leftno, attrs) *)
2169 let type_of_aux' metasenv context term =
2172 type_of_aux' metasenv context term in
2174 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2176 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2179 | RefineFailure msg as e ->
2180 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2182 | Uncertain msg as e ->
2183 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2187 let profiler2 = HExtlib.profile "CicRefine"
2189 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2190 profiler2.HExtlib.profile
2191 (type_of_aux' ?localization_tbl metasenv context term) ugraph
2193 let typecheck ~localization_tbl metasenv uri obj =
2194 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2196 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2197 (* vim:set foldmethod=marker: *)