1 (* Copyright (C) 2000, 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://cs.unibo.it/helm/.
28 exception RefineFailure of string Lazy.t;;
29 exception Uncertain of string Lazy.t;;
30 exception AssertFailure of string Lazy.t;;
32 let insert_coercions = ref true
34 let debug_print = fun _ -> ()
36 let profiler = HExtlib.profile "CicRefine.fo_unif"
38 let fo_unif_subst subst context metasenv t1 t2 ugraph =
41 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
42 in profiler.HExtlib.profile foo ()
44 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
45 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
48 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
51 RefineFailure msg -> RefineFailure (f msg)
52 | Uncertain msg -> Uncertain (f msg)
53 | _ -> assert false in
56 Cic.CicHash.find localization_tbl t
58 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
61 raise (HExtlib.Localized (loc,exn'))
63 let relocalize localization_tbl oldt newt =
65 let infos = Cic.CicHash.find localization_tbl oldt in
66 Cic.CicHash.remove localization_tbl oldt;
67 Cic.CicHash.add localization_tbl newt infos;
75 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
76 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
79 let exp_impl metasenv subst context =
82 let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
83 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
84 metasenv', Cic.Meta (idx, irl)
86 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
87 metasenv', Cic.Meta (idx, [])
89 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
90 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
91 metasenv', Cic.Meta (idx, irl)
96 let rec type_of_constant uri ugraph =
98 let module R = CicReduction in
99 let module U = UriManager in
100 let _ = CicTypeChecker.typecheck uri in
103 CicEnvironment.get_cooked_obj ugraph uri
104 with Not_found -> assert false
107 C.Constant (_,_,ty,_,_) -> ty,u
108 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
111 (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
113 and type_of_variable uri ugraph =
114 let module C = Cic in
115 let module R = CicReduction in
116 let module U = UriManager in
117 let _ = CicTypeChecker.typecheck uri in
120 CicEnvironment.get_cooked_obj ugraph uri
121 with Not_found -> assert false
124 C.Variable (_,_,ty,_,_) -> ty,u
128 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
130 and type_of_mutual_inductive_defs uri i ugraph =
131 let module C = Cic in
132 let module R = CicReduction in
133 let module U = UriManager in
134 let _ = CicTypeChecker.typecheck uri in
137 CicEnvironment.get_cooked_obj ugraph uri
138 with Not_found -> assert false
141 C.InductiveDefinition (dl,_,_,_) ->
142 let (_,_,arity,_) = List.nth dl i in
147 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
149 and type_of_mutual_inductive_constr uri i j ugraph =
150 let module C = Cic in
151 let module R = CicReduction in
152 let module U = UriManager in
153 let _ = CicTypeChecker.typecheck uri in
156 CicEnvironment.get_cooked_obj ugraph uri
157 with Not_found -> assert false
160 C.InductiveDefinition (dl,_,_,_) ->
161 let (_,_,_,cl) = List.nth dl i in
162 let (_,ty) = List.nth cl (j-1) in
168 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
171 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
173 (* the check_branch function checks if a branch of a case is refinable.
174 It returns a pair (outype_instance,args), a subst and a metasenv.
175 outype_instance is the expected result of applying the case outtype
177 The problem is that outype is in general unknown, and we should
178 try to synthesize it from the above information, that is in general
179 a second order unification problem. *)
181 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
182 let module C = Cic in
183 (* let module R = CicMetaSubst in *)
184 let module R = CicReduction in
185 match R.whd ~subst context expectedtype with
187 (n,context,actualtype, [term]), subst, metasenv, ugraph
188 | C.Appl (C.MutInd (_,_,_)::tl) ->
189 let (_,arguments) = split tl left_args_no in
190 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
191 | C.Prod (name,so,de) ->
192 (* we expect that the actual type of the branch has the due
194 (match R.whd ~subst context actualtype with
195 C.Prod (name',so',de') ->
196 let subst, metasenv, ugraph1 =
197 fo_unif_subst subst context metasenv so so' ugraph in
199 (match CicSubstitution.lift 1 term with
200 C.Appl l -> C.Appl (l@[C.Rel 1])
201 | t -> C.Appl [t ; C.Rel 1]) in
202 (* we should also check that the name variable is anonymous in
203 the actual type de' ?? *)
205 ((Some (name,(C.Decl so)))::context)
206 metasenv subst left_args_no de' term' de ugraph1
207 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
208 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
210 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
213 let rec type_of_aux subst metasenv context t ugraph =
214 let module C = Cic in
215 let module S = CicSubstitution in
216 let module U = UriManager in
217 let (t',_,_,_,_) as res =
222 match List.nth context (n - 1) with
223 Some (_,C.Decl ty) ->
224 t,S.lift n ty,subst,metasenv, ugraph
225 | Some (_,C.Def (_,Some ty)) ->
226 t,S.lift n ty,subst,metasenv, ugraph
227 | Some (_,C.Def (bo,None)) ->
229 (* if it is in the context it must be already well-typed*)
230 CicTypeChecker.type_of_aux' ~subst metasenv context
233 t,ty,subst,metasenv,ugraph
235 enrich localization_tbl t
236 (RefineFailure (lazy "Rel to hidden hypothesis"))
239 enrich localization_tbl t
240 (RefineFailure (lazy "Not a close term")))
241 | C.Var (uri,exp_named_subst) ->
242 let exp_named_subst',subst',metasenv',ugraph1 =
243 check_exp_named_subst
244 subst metasenv context exp_named_subst ugraph
246 let ty_uri,ugraph1 = type_of_variable uri ugraph in
248 CicSubstitution.subst_vars exp_named_subst' ty_uri
250 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
253 let (canonical_context, term,ty) =
254 CicUtil.lookup_subst n subst
256 let l',subst',metasenv',ugraph1 =
257 check_metasenv_consistency n subst metasenv context
258 canonical_context l ugraph
260 (* trust or check ??? *)
261 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
262 subst', metasenv', ugraph1
263 (* type_of_aux subst metasenv
264 context (CicSubstitution.subst_meta l term) *)
265 with CicUtil.Subst_not_found _ ->
266 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
267 let l',subst',metasenv', ugraph1 =
268 check_metasenv_consistency n subst metasenv context
269 canonical_context l ugraph
271 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
272 subst', metasenv',ugraph1)
273 | C.Sort (C.Type tno) ->
274 let tno' = CicUniv.fresh() in
275 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
276 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
278 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
279 | C.Implicit infos ->
280 let metasenv',t' = exp_impl metasenv subst context infos in
281 type_of_aux subst metasenv' context t' ugraph
283 let ty',_,subst',metasenv',ugraph1 =
284 type_of_aux subst metasenv context ty ugraph
286 let te',inferredty,subst'',metasenv'',ugraph2 =
287 type_of_aux subst' metasenv' context te ugraph1
290 let subst''',metasenv''',ugraph3 =
291 fo_unif_subst subst'' context metasenv''
292 inferredty ty' ugraph2
294 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
297 enrich localization_tbl te'
300 CicMetaSubst.ppterm_in_context subst'' te'
301 context ^ " has type " ^
302 CicMetaSubst.ppterm_in_context subst'' inferredty
303 context ^ " but is here used with type " ^
304 CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
306 | C.Prod (name,s,t) ->
307 let carr t subst context = CicMetaSubst.apply_subst subst t in
308 let coerce_to_sort in_source tgt_sort t type_to_coerce
309 subst context metasenv uragph
311 if not !insert_coercions then
312 t,type_to_coerce,subst,metasenv,ugraph
314 let coercion_src = carr type_to_coerce subst context in
315 match coercion_src with
317 t,type_to_coerce,subst,metasenv,ugraph
318 | Cic.Meta _ as meta ->
319 t, meta, subst, metasenv, ugraph
320 | Cic.Cast _ as cast ->
321 t, cast, subst, metasenv, ugraph
323 let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
324 let search = CoercGraph.look_for_coercion in
325 let boh = search coercion_src coercion_tgt in
327 | CoercGraph.NoCoercion
328 | CoercGraph.NotHandled _ ->
329 enrich localization_tbl t
332 CicMetaSubst.ppterm_in_context subst t context ^
333 " is not a type since it has type " ^
334 CicMetaSubst.ppterm_in_context
335 subst coercion_src context ^ " that is not a sort")))
336 | CoercGraph.NotMetaClosed ->
337 enrich localization_tbl t
340 CicMetaSubst.ppterm_in_context subst t context ^
341 " is not a type since it has type " ^
342 CicMetaSubst.ppterm_in_context
343 subst coercion_src context ^ " that is not a sort")))
344 | CoercGraph.SomeCoercion c ->
345 let newt, tty, subst, metasenv, ugraph =
346 avoid_double_coercion
347 subst metasenv ugraph
348 (Cic.Appl[c;t]) coercion_tgt
350 newt, tty, subst, metasenv, ugraph)
352 let s',sort1,subst',metasenv',ugraph1 =
353 type_of_aux subst metasenv context s ugraph
355 let s',sort1,subst', metasenv',ugraph1 =
356 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
357 s' sort1 subst' context metasenv' ugraph1
359 let context_for_t = ((Some (name,(C.Decl s')))::context) in
360 let t',sort2,subst'',metasenv'',ugraph2 =
361 type_of_aux subst' metasenv'
362 context_for_t t ugraph1
364 let t',sort2,subst'',metasenv'',ugraph2 =
365 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
366 t' sort2 subst'' context_for_t metasenv'' ugraph2
368 let sop,subst''',metasenv''',ugraph3 =
369 sort_of_prod subst'' metasenv''
370 context (name,s') (sort1,sort2) ugraph2
372 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
373 | C.Lambda (n,s,t) ->
375 let s',sort1,subst',metasenv',ugraph1 =
376 type_of_aux subst metasenv context s ugraph in
377 let s',sort1,subst',metasenv',ugraph1 =
378 if not !insert_coercions then
379 s',sort1, subst', metasenv', ugraph1
381 match CicReduction.whd ~subst:subst' context sort1 with
382 | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
384 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
385 let search = CoercGraph.look_for_coercion in
386 let boh = search coercion_src coercion_tgt in
388 | CoercGraph.SomeCoercion c ->
389 let newt, tty, subst', metasenv', ugraph1 =
390 avoid_double_coercion
391 subst' metasenv' ugraph1
392 (Cic.Appl[c;s']) coercion_tgt
394 newt, tty, subst', metasenv', ugraph1
395 | CoercGraph.NoCoercion
396 | CoercGraph.NotHandled _ ->
397 enrich localization_tbl s'
400 CicMetaSubst.ppterm_in_context subst s' context ^
401 " is not a type since it has type " ^
402 CicMetaSubst.ppterm_in_context
403 subst coercion_src context ^ " that is not a sort")))
404 | CoercGraph.NotMetaClosed ->
405 enrich localization_tbl s'
408 CicMetaSubst.ppterm_in_context subst s' context ^
409 " is not a type since it has type " ^
410 CicMetaSubst.ppterm_in_context
411 subst coercion_src context ^ " that is not a sort")))
413 let context_for_t = ((Some (n,(C.Decl s')))::context) in
414 let t',type2,subst'',metasenv'',ugraph2 =
415 type_of_aux subst' metasenv' context_for_t t ugraph1
417 C.Lambda (n,s',t'),C.Prod (n,s',type2),
418 subst'',metasenv'',ugraph2
420 (* only to check if s is well-typed *)
421 let s',ty,subst',metasenv',ugraph1 =
422 type_of_aux subst metasenv context s ugraph
424 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
426 let t',inferredty,subst'',metasenv'',ugraph2 =
427 type_of_aux subst' metasenv'
428 context_for_t t ugraph1
430 (* One-step LetIn reduction.
431 * Even faster than the previous solution.
432 * Moreover the inferred type is closer to the expected one.
434 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
435 subst'',metasenv'',ugraph2
436 | C.Appl (he::((_::_) as tl)) ->
437 let he',hetype,subst',metasenv',ugraph1 =
438 type_of_aux subst metasenv context he ugraph
440 let tlbody_and_type,subst'',metasenv'',ugraph2 =
442 (fun x (res,subst,metasenv,ugraph) ->
443 let x',ty,subst',metasenv',ugraph1 =
444 type_of_aux subst metasenv context x ugraph
446 (x', ty)::res,subst',metasenv',ugraph1
447 ) tl ([],subst',metasenv',ugraph1)
449 let tl',applty,subst''',metasenv''',ugraph3 =
450 eat_prods true subst'' metasenv'' context
451 hetype tlbody_and_type ugraph2
453 avoid_double_coercion
454 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
455 | C.Appl _ -> assert false
456 | C.Const (uri,exp_named_subst) ->
457 let exp_named_subst',subst',metasenv',ugraph1 =
458 check_exp_named_subst subst metasenv context
459 exp_named_subst ugraph in
460 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
462 CicSubstitution.subst_vars exp_named_subst' ty_uri
464 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
465 | C.MutInd (uri,i,exp_named_subst) ->
466 let exp_named_subst',subst',metasenv',ugraph1 =
467 check_exp_named_subst subst metasenv context
468 exp_named_subst ugraph
470 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
472 CicSubstitution.subst_vars exp_named_subst' ty_uri in
473 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
474 | C.MutConstruct (uri,i,j,exp_named_subst) ->
475 let exp_named_subst',subst',metasenv',ugraph1 =
476 check_exp_named_subst subst metasenv context
477 exp_named_subst ugraph
480 type_of_mutual_inductive_constr uri i j ugraph1
483 CicSubstitution.subst_vars exp_named_subst' ty_uri
485 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
487 | C.MutCase (uri, i, outtype, term, pl) ->
488 (* first, get the inductive type (and noparams)
489 * in the environment *)
490 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
491 let _ = CicTypeChecker.typecheck uri in
492 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
494 C.InductiveDefinition (l,expl_params,parsno,_) ->
495 List.nth l i , expl_params, parsno, u
497 enrich localization_tbl t
499 (lazy ("Unkown mutual inductive definition " ^
500 U.string_of_uri uri)))
502 let rec count_prod t =
503 match CicReduction.whd ~subst context t with
504 C.Prod (_, _, t) -> 1 + (count_prod t)
507 let no_args = count_prod arity in
508 (* now, create a "generic" MutInd *)
509 let metasenv,left_args =
510 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
512 let metasenv,right_args =
513 let no_right_params = no_args - no_left_params in
514 if no_right_params < 0 then assert false
515 else CicMkImplicit.n_fresh_metas
516 metasenv subst context no_right_params
518 let metasenv,exp_named_subst =
519 CicMkImplicit.fresh_subst metasenv subst context expl_params in
522 C.MutInd (uri,i,exp_named_subst)
525 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
527 (* check consistency with the actual type of term *)
528 let term',actual_type,subst,metasenv,ugraph1 =
529 type_of_aux subst metasenv context term ugraph in
530 let expected_type',_, subst, metasenv,ugraph2 =
531 type_of_aux subst metasenv context expected_type ugraph1
533 let actual_type = CicReduction.whd ~subst context actual_type in
534 let subst,metasenv,ugraph3 =
536 fo_unif_subst subst context metasenv
537 expected_type' actual_type ugraph2
540 enrich localization_tbl term' exn
543 CicMetaSubst.ppterm_in_context subst term'
544 context ^ " has type " ^
545 CicMetaSubst.ppterm_in_context subst actual_type
546 context ^ " but is here used with type " ^
547 CicMetaSubst.ppterm_in_context subst expected_type' context))
549 let rec instantiate_prod t =
553 match CicReduction.whd ~subst context t with
555 instantiate_prod (CicSubstitution.subst he t') tl
558 let arity_instantiated_with_left_args =
559 instantiate_prod arity left_args in
560 (* TODO: check if the sort elimination
561 * is allowed: [(I q1 ... qr)|B] *)
562 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
564 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
566 if left_args = [] then
567 (C.MutConstruct (uri,i,j,exp_named_subst))
570 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
572 let p',actual_type,subst,metasenv,ugraph1 =
573 type_of_aux subst metasenv context p ugraph
575 let constructor',expected_type, subst, metasenv,ugraph2 =
576 type_of_aux subst metasenv context constructor ugraph1
578 let outtypeinstance,subst,metasenv,ugraph3 =
579 check_branch 0 context metasenv subst no_left_params
580 actual_type constructor' expected_type ugraph2
583 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
584 ([],1,[],subst,metasenv,ugraph3) pl
587 (* we are left to check that the outype matches his instances.
588 The easy case is when the outype is specified, that amount
589 to a trivial check. Otherwise, we should guess a type from
593 let outtype,outtypety, subst, metasenv,ugraph4 =
594 type_of_aux subst metasenv context outtype ugraph4 in
597 (let candidate,ugraph5,metasenv,subst =
598 let exp_name_subst, metasenv =
600 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
602 let uris = CicUtil.params_of_obj o in
604 fun uri (acc,metasenv) ->
605 let metasenv',new_meta =
606 CicMkImplicit.mk_implicit metasenv subst context
609 CicMkImplicit.identity_relocation_list_for_metavariable
612 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
616 match left_args,right_args with
617 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
619 let rec mk_right_args =
622 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
624 let right_args_no = List.length right_args in
625 let lifted_left_args =
626 List.map (CicSubstitution.lift right_args_no) left_args
628 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
629 (lifted_left_args @ mk_right_args right_args_no))
632 FreshNamesGenerator.mk_fresh_name ~subst metasenv
633 context Cic.Anonymous ~typ:ty
635 match outtypeinstances with
637 let extended_context =
638 let rec add_right_args =
640 Cic.Prod (name,ty,t) ->
641 Some (name,Cic.Decl ty)::(add_right_args t)
644 (Some (fresh_name,Cic.Decl ty))::
646 (add_right_args arity_instantiated_with_left_args))@
649 let metasenv,new_meta =
650 CicMkImplicit.mk_implicit metasenv subst extended_context
653 CicMkImplicit.identity_relocation_list_for_metavariable
656 let rec add_lambdas b =
658 Cic.Prod (name,ty,t) ->
659 Cic.Lambda (name,ty,(add_lambdas b t))
660 | _ -> Cic.Lambda (fresh_name, ty, b)
663 add_lambdas (Cic.Meta (new_meta,irl))
664 arity_instantiated_with_left_args
666 (Some candidate),ugraph4,metasenv,subst
667 | (constructor_args_no,_,instance,_)::tl ->
669 let instance',subst,metasenv =
670 CicMetaSubst.delift_rels subst metasenv
671 constructor_args_no instance
673 let candidate,ugraph,metasenv,subst =
675 fun (candidate_oty,ugraph,metasenv,subst)
676 (constructor_args_no,_,instance,_) ->
677 match candidate_oty with
678 | None -> None,ugraph,metasenv,subst
681 let instance',subst,metasenv =
682 CicMetaSubst.delift_rels subst metasenv
683 constructor_args_no instance
685 let subst,metasenv,ugraph =
686 fo_unif_subst subst context metasenv
689 candidate_oty,ugraph,metasenv,subst
691 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
692 | CicUnification.UnificationFailure _
693 | CicUnification.Uncertain _ ->
694 None,ugraph,metasenv,subst
695 ) (Some instance',ugraph4,metasenv,subst) tl
698 | None -> None, ugraph,metasenv,subst
700 let rec add_lambdas n b =
702 Cic.Prod (name,ty,t) ->
703 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
705 Cic.Lambda (fresh_name, ty,
706 CicSubstitution.lift (n + 1) t)
709 (add_lambdas 0 t arity_instantiated_with_left_args),
710 ugraph,metasenv,subst
711 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
712 None,ugraph4,metasenv,subst
715 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
717 let subst,metasenv,ugraph =
718 fo_unif_subst subst context metasenv
719 candidate outtype ugraph5
721 C.MutCase (uri, i, outtype, term', pl'),
722 CicReduction.head_beta_reduce
723 (CicMetaSubst.apply_subst subst
724 (Cic.Appl (outtype::right_args@[term']))),
725 subst,metasenv,ugraph)
726 | _ -> (* easy case *)
727 let tlbody_and_type,subst,metasenv,ugraph4 =
729 (fun x (res,subst,metasenv,ugraph) ->
730 let x',ty,subst',metasenv',ugraph1 =
731 type_of_aux subst metasenv context x ugraph
733 (x', ty)::res,subst',metasenv',ugraph1
734 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
736 let _,_,subst,metasenv,ugraph4 =
737 eat_prods false subst metasenv context
738 outtypety tlbody_and_type ugraph4
740 let _,_, subst, metasenv,ugraph5 =
741 type_of_aux subst metasenv context
742 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
744 let (subst,metasenv,ugraph6) =
746 (fun (subst,metasenv,ugraph)
747 (constructor_args_no,context,instance,args) ->
751 CicSubstitution.lift constructor_args_no outtype
753 C.Appl (outtype'::args)
755 CicReduction.whd ~subst context appl
757 fo_unif_subst subst context metasenv
758 instance instance' ugraph)
759 (subst,metasenv,ugraph5) outtypeinstances
761 C.MutCase (uri, i, outtype, term', pl'),
762 CicReduction.head_beta_reduce
763 (CicMetaSubst.apply_subst subst
764 (C.Appl(outtype::right_args@[term]))),
765 subst,metasenv,ugraph6)
767 let fl_ty',subst,metasenv,types,ugraph1 =
769 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
770 let ty',_,subst',metasenv',ugraph1 =
771 type_of_aux subst metasenv context ty ugraph
773 fl @ [ty'],subst',metasenv',
774 Some (C.Name n,(C.Decl ty')) :: types, ugraph
775 ) ([],subst,metasenv,[],ugraph) fl
777 let len = List.length types in
778 let context' = types@context in
779 let fl_bo',subst,metasenv,ugraph2 =
781 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
782 let bo',ty_of_bo,subst,metasenv,ugraph1 =
783 type_of_aux subst metasenv context' bo ugraph
785 let subst',metasenv',ugraph' =
786 fo_unif_subst subst context' metasenv
787 ty_of_bo (CicSubstitution.lift len ty) ugraph1
789 fl @ [bo'] , subst',metasenv',ugraph'
790 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
792 let ty = List.nth fl_ty' i in
793 (* now we have the new ty in fl_ty', the new bo in fl_bo',
794 * and we want the new fl with bo' and ty' injected in the right
797 let rec map3 f l1 l2 l3 =
800 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
803 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
806 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
808 let fl_ty',subst,metasenv,types,ugraph1 =
810 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
811 let ty',_,subst',metasenv',ugraph1 =
812 type_of_aux subst metasenv context ty ugraph
814 fl @ [ty'],subst',metasenv',
815 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
816 ) ([],subst,metasenv,[],ugraph) fl
818 let len = List.length types in
819 let context' = types@context in
820 let fl_bo',subst,metasenv,ugraph2 =
822 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
823 let bo',ty_of_bo,subst,metasenv,ugraph1 =
824 type_of_aux subst metasenv context' bo ugraph
826 let subst',metasenv',ugraph' =
827 fo_unif_subst subst context' metasenv
828 ty_of_bo (CicSubstitution.lift len ty) ugraph1
830 fl @ [bo'],subst',metasenv',ugraph'
831 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
833 let ty = List.nth fl_ty' i in
834 (* now we have the new ty in fl_ty', the new bo in fl_bo',
835 * and we want the new fl with bo' and ty' injected in the right
838 let rec map3 f l1 l2 l3 =
841 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
844 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
847 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
849 relocalize localization_tbl t t';
852 and avoid_double_coercion subst metasenv ugraph t ty =
854 | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when
855 CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
856 let source_carr = CoercGraph.source_of c2 in
857 let tgt_carr = CicMetaSubst.apply_subst subst ty in
858 (match CoercGraph.look_for_coercion source_carr tgt_carr
860 | CoercGraph.SomeCoercion c ->
861 Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph
862 | _ -> assert false) (* the composite coercion must exist *)
863 | _ -> t, ty, subst, metasenv, ugraph
865 (* check_metasenv_consistency checks that the "canonical" context of a
866 metavariable is consitent - up to relocation via the relocation list l -
867 with the actual context *)
868 and check_metasenv_consistency
869 metano subst metasenv context canonical_context l ugraph
871 let module C = Cic in
872 let module R = CicReduction in
873 let module S = CicSubstitution in
874 let lifted_canonical_context =
878 | (Some (n,C.Decl t))::tl ->
879 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
880 | (Some (n,C.Def (t,None)))::tl ->
881 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
882 | None::tl -> None::(aux (i+1) tl)
883 | (Some (n,C.Def (t,Some ty)))::tl ->
885 C.Def ((S.subst_meta l (S.lift i t)),
886 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
888 aux 1 canonical_context
892 (fun (l,subst,metasenv,ugraph) t ct ->
895 l @ [None],subst,metasenv,ugraph
896 | Some t,Some (_,C.Def (ct,_)) ->
897 let subst',metasenv',ugraph' =
899 fo_unif_subst subst context metasenv t ct ugraph
900 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 subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
902 l @ [Some t],subst',metasenv',ugraph'
903 | Some t,Some (_,C.Decl ct) ->
904 let t',inferredty,subst',metasenv',ugraph1 =
905 type_of_aux subst metasenv context t ugraph
907 let subst'',metasenv'',ugraph2 =
910 subst' context metasenv' inferredty ct ugraph1
911 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 subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
913 l @ [Some t'], subst'',metasenv'',ugraph2
915 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 subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
917 Invalid_argument _ ->
921 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
922 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
923 (CicMetaSubst.ppcontext subst canonical_context))))
925 and check_exp_named_subst metasubst metasenv context tl ugraph =
926 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
928 [] -> [],metasubst,metasenv,ugraph
930 let ty_uri,ugraph1 = type_of_variable uri ugraph in
932 CicSubstitution.subst_vars substs ty_uri in
933 (* CSC: why was this code here? it is wrong
934 (match CicEnvironment.get_cooked_obj ~trust:false uri with
935 Cic.Variable (_,Some bo,_,_) ->
938 "A variable with a body can not be explicit substituted"))
939 | Cic.Variable (_,None,_,_) -> ()
943 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
946 let t',typeoft,metasubst',metasenv',ugraph2 =
947 type_of_aux metasubst metasenv context t ugraph1 in
948 let subst = uri,t' in
949 let metasubst'',metasenv'',ugraph3 =
952 metasubst' context metasenv' typeoft typeofvar ugraph2
954 raise (RefineFailure (lazy
955 ("Wrong Explicit Named Substitution: " ^
956 CicMetaSubst.ppterm metasubst' typeoft ^
957 " not unifiable with " ^
958 CicMetaSubst.ppterm metasubst' typeofvar)))
960 (* FIXME: no mere tail recursive! *)
961 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
962 check_exp_named_subst_aux
963 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
965 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
967 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
970 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
971 let module C = Cic in
972 let context_for_t2 = (Some (name,C.Decl s))::context in
973 let t1'' = CicReduction.whd ~subst context t1 in
974 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
975 match (t1'', t2'') with
976 (C.Sort s1, C.Sort s2)
977 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
978 (* different than Coq manual!!! *)
979 C.Sort s2,subst,metasenv,ugraph
980 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
981 let t' = CicUniv.fresh() in
982 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
983 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
984 C.Sort (C.Type t'),subst,metasenv,ugraph2
985 | (C.Sort _,C.Sort (C.Type t1)) ->
986 C.Sort (C.Type t1),subst,metasenv,ugraph
987 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
988 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
989 (* TODO how can we force the meta to become a sort? If we don't we
990 * brake the invariant that refine produce only well typed terms *)
991 (* TODO if we check the non meta term and if it is a sort then we
992 * are likely to know the exact value of the result e.g. if the rhs
993 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
995 CicMkImplicit.mk_implicit_sort metasenv subst in
996 let (subst, metasenv,ugraph1) =
997 fo_unif_subst subst context_for_t2 metasenv
998 (C.Meta (idx,[])) t2'' ugraph
1000 t2'',subst,metasenv,ugraph1
1006 ("Two sorts were expected, found %s " ^^
1007 "(that reduces to %s) and %s (that reduces to %s)")
1008 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1009 (CicPp.ppterm t2''))))
1012 allow_coercions subst metasenv context hetype tlbody_and_type ugraph
1014 let rec mk_prod metasenv context =
1017 let (metasenv, idx) =
1018 CicMkImplicit.mk_implicit_type metasenv subst context
1021 CicMkImplicit.identity_relocation_list_for_metavariable context
1023 metasenv,Cic.Meta (idx, irl)
1025 let (metasenv, idx) =
1026 CicMkImplicit.mk_implicit_type metasenv subst context
1029 CicMkImplicit.identity_relocation_list_for_metavariable context
1031 let meta = Cic.Meta (idx,irl) in
1033 (* The name must be fresh for context. *)
1034 (* Nevertheless, argty is well-typed only in context. *)
1035 (* Thus I generate a name (name_hint) in context and *)
1036 (* then I generate a name --- using the hint name_hint *)
1037 (* --- that is fresh in (context'@context). *)
1039 (* Cic.Name "pippo" *)
1040 FreshNamesGenerator.mk_fresh_name ~subst metasenv
1041 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
1042 (CicMetaSubst.apply_subst_context subst context)
1044 ~typ:(CicMetaSubst.apply_subst subst argty)
1046 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
1047 FreshNamesGenerator.mk_fresh_name ~subst
1048 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
1050 let metasenv,target =
1051 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
1053 metasenv,Cic.Prod (name,meta,target)
1055 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
1056 let (subst, metasenv,ugraph1) =
1058 fo_unif_subst subst context metasenv hetype hetype' ugraph
1060 debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
1061 (CicPp.ppterm hetype)
1062 (CicPp.ppterm hetype')
1063 (CicMetaSubst.ppmetasenv [] metasenv)
1064 (CicMetaSubst.ppsubst subst)));
1068 let rec eat_prods metasenv subst context hetype ugraph =
1070 | [] -> [],metasenv,subst,hetype,ugraph
1071 | (hete, hety)::tl ->
1074 let arg,subst,metasenv,ugraph1 =
1076 let subst,metasenv,ugraph1 =
1077 fo_unif_subst subst context metasenv hety s ugraph
1079 hete,subst,metasenv,ugraph1
1080 with exn when allow_coercions && !insert_coercions ->
1081 (* we search a coercion from hety to s *)
1082 let coer, tgt_carr =
1083 let carr t subst context =
1084 CicMetaSubst.apply_subst subst t
1086 let c_hety = carr hety subst context in
1087 let c_s = carr s subst context in
1088 CoercGraph.look_for_coercion c_hety c_s, c_s
1091 | CoercGraph.NoCoercion
1092 | CoercGraph.NotHandled _ ->
1093 enrich localization_tbl hete
1095 (lazy ("The term " ^
1096 CicMetaSubst.ppterm_in_context subst hete
1097 context ^ " has type " ^
1098 CicMetaSubst.ppterm_in_context subst hety
1099 context ^ " but is here used with type " ^
1100 CicMetaSubst.ppterm_in_context subst s context
1101 (* "\nReason: " ^ Lazy.force e*))))
1102 | CoercGraph.NotMetaClosed ->
1103 enrich localization_tbl hete
1105 (lazy ("The term " ^
1106 CicMetaSubst.ppterm_in_context subst hete
1107 context ^ " has type " ^
1108 CicMetaSubst.ppterm_in_context subst hety
1109 context ^ " but is here used with type " ^
1110 CicMetaSubst.ppterm_in_context subst s context
1111 (* "\nReason: " ^ Lazy.force e*))))
1112 | CoercGraph.SomeCoercion c ->
1113 let newt, _, subst, metasenv, ugraph =
1114 avoid_double_coercion
1115 subst metasenv ugraph
1116 (Cic.Appl[c;hete]) tgt_carr
1118 newt, subst, metasenv, ugraph)
1120 enrich localization_tbl hete
1122 (lazy ("The term " ^
1123 CicMetaSubst.ppterm_in_context subst hete
1124 context ^ " has type " ^
1125 CicMetaSubst.ppterm_in_context subst hety
1126 context ^ " but is here used with type " ^
1127 CicMetaSubst.ppterm_in_context subst s context
1128 (* "\nReason: " ^ Lazy.force e*)))) exn
1130 let coerced_args,metasenv',subst',t',ugraph2 =
1131 eat_prods metasenv subst context
1132 (CicSubstitution.subst arg t) ugraph1 tl
1134 arg::coerced_args,metasenv',subst',t',ugraph2
1138 let coerced_args,metasenv,subst,t,ugraph2 =
1139 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1141 coerced_args,t,subst,metasenv,ugraph2
1144 (* eat prods ends here! *)
1146 let t',ty,subst',metasenv',ugraph1 =
1147 type_of_aux [] metasenv context t ugraph
1149 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1150 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1151 (* Andrea: ho rimesso qui l'applicazione della subst al
1152 metasenv dopo che ho droppato l'invariante che il metsaenv
1153 e' sempre istanziato *)
1154 let substituted_metasenv =
1155 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1157 (* substituted_t,substituted_ty,substituted_metasenv *)
1158 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1160 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1162 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1163 let cleaned_metasenv =
1165 (function (n,context,ty) ->
1166 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1171 | Some (n, Cic.Decl t) ->
1173 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1174 | Some (n, Cic.Def (bo,ty)) ->
1175 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1180 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1182 Some (n, Cic.Def (bo',ty'))
1186 ) substituted_metasenv
1188 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1191 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1193 type_of_aux' ?localization_tbl metasenv context term ugraph
1195 CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1197 let undebrujin uri typesno tys t =
1200 (fun (name,_,_,_) (i,t) ->
1201 (* here the explicit_named_substituion is assumed to be *)
1203 let t' = Cic.MutInd (uri,i,[]) in
1204 let t = CicSubstitution.subst t' t in
1206 ) tys (typesno - 1,t))
1208 let map_first_n n start f g l =
1209 let rec aux acc k l =
1212 | [] -> raise (Invalid_argument "map_first_n")
1213 | hd :: tl -> f hd k (aux acc (k+1) tl)
1219 (*CSC: this is a very rough approximation; to be finished *)
1220 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1221 let subst,metasenv,ugraph,tys =
1223 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1224 let subst,metasenv,ugraph,cl =
1226 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1227 let rec aux ctx k subst = function
1228 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1229 let subst,metasenv,ugraph,tl =
1231 (subst,metasenv,ugraph,[])
1232 (fun t n (subst,metasenv,ugraph,acc) ->
1233 let subst,metasenv,ugraph =
1235 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1237 subst,metasenv,ugraph,(t::acc))
1238 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1241 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1242 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1243 subst,metasenv,ugraph,t
1244 | Cic.Prod (name,s,t) ->
1245 let ctx = (Some (name,Cic.Decl s))::ctx in
1246 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1247 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1251 (lazy "not well formed constructor type"))
1253 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1254 subst,metasenv,ugraph,(name,ty) :: acc)
1255 cl (subst,metasenv,ugraph,[])
1257 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1258 tys ([],metasenv,ugraph,[])
1260 let substituted_tys =
1262 (fun (name,ind,arity,cl) ->
1264 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1266 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1269 metasenv,ugraph,substituted_tys
1271 let typecheck metasenv uri obj ~localization_tbl =
1272 let ugraph = CicUniv.empty_ugraph in
1274 Cic.Constant (name,Some bo,ty,args,attrs) ->
1275 let bo',boty,metasenv,ugraph =
1276 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1277 let ty',_,metasenv,ugraph =
1278 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1279 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1280 let bo' = CicMetaSubst.apply_subst subst bo' in
1281 let ty' = CicMetaSubst.apply_subst subst ty' in
1282 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1283 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1284 | Cic.Constant (name,None,ty,args,attrs) ->
1285 let ty',_,metasenv,ugraph =
1286 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1288 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1289 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1290 assert (metasenv' = metasenv);
1291 (* Here we do not check the metasenv for correctness *)
1292 let bo',boty,metasenv,ugraph =
1293 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1294 let ty',sort,metasenv,ugraph =
1295 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1299 (* instead of raising Uncertain, let's hope that the meta will become
1302 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1304 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1305 let bo' = CicMetaSubst.apply_subst subst bo' in
1306 let ty' = CicMetaSubst.apply_subst subst ty' in
1307 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1308 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1309 | Cic.Variable _ -> assert false (* not implemented *)
1310 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1311 (*CSC: this code is greately simplified and many many checks are missing *)
1312 (*CSC: e.g. the constructors are not required to build their own types, *)
1313 (*CSC: the arities are not required to have as type a sort, etc. *)
1314 let uri = match uri with Some uri -> uri | None -> assert false in
1315 let typesno = List.length tys in
1316 (* first phase: we fix only the types *)
1317 let metasenv,ugraph,tys =
1319 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1320 let ty',_,metasenv,ugraph =
1321 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1323 metasenv,ugraph,(name,b,ty',cl)::res
1324 ) tys (metasenv,ugraph,[]) in
1326 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1327 (* second phase: we fix only the constructors *)
1328 let metasenv,ugraph,tys =
1330 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1331 let metasenv,ugraph,cl' =
1333 (fun (name,ty) (metasenv,ugraph,res) ->
1335 CicTypeChecker.debrujin_constructor
1336 ~cb:(relocalize localization_tbl) uri typesno ty in
1337 let ty',_,metasenv,ugraph =
1338 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1339 let ty' = undebrujin uri typesno tys ty' in
1340 metasenv,ugraph,(name,ty')::res
1341 ) cl (metasenv,ugraph,[])
1343 metasenv,ugraph,(name,b,ty,cl')::res
1344 ) tys (metasenv,ugraph,[]) in
1345 (* third phase: we check the positivity condition *)
1346 let metasenv,ugraph,tys =
1347 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1349 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1352 let type_of_aux' metasenv context term =
1355 type_of_aux' metasenv context term in
1357 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1359 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1362 | RefineFailure msg as e ->
1363 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1365 | Uncertain msg as e ->
1366 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1370 let profiler2 = HExtlib.profile "CicRefine"
1372 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1373 profiler2.HExtlib.profile
1374 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1376 let typecheck ~localization_tbl metasenv uri obj =
1377 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj