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/.
30 exception RefineFailure of string Lazy.t;;
31 exception Uncertain of string Lazy.t;;
32 exception AssertFailure of string Lazy.t;;
34 let insert_coercions = ref true
36 let debug_print = fun _ -> ()
38 let profiler = HExtlib.profile "CicRefine.fo_unif"
40 let fo_unif_subst subst context metasenv t1 t2 ugraph =
43 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
44 in profiler.HExtlib.profile foo ()
46 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
47 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
50 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
53 RefineFailure msg -> RefineFailure (f msg)
54 | Uncertain msg -> Uncertain (f msg)
55 | _ -> assert false in
58 Cic.CicHash.find localization_tbl t
60 prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
63 raise (HExtlib.Localized (loc,exn'))
65 let relocalize localization_tbl oldt newt =
67 let infos = Cic.CicHash.find localization_tbl oldt in
68 Cic.CicHash.remove localization_tbl oldt;
69 Cic.CicHash.add localization_tbl newt infos;
77 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
78 | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
81 let exp_impl metasenv subst context =
84 let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
85 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
86 metasenv', Cic.Meta (idx, irl)
88 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
89 metasenv', Cic.Meta (idx, [])
91 let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
92 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
93 metasenv', Cic.Meta (idx, irl)
98 let rec type_of_constant uri ugraph =
100 let module R = CicReduction in
101 let module U = UriManager in
102 let _ = CicTypeChecker.typecheck uri in
105 CicEnvironment.get_cooked_obj ugraph uri
106 with Not_found -> assert false
109 C.Constant (_,_,ty,_,_) -> ty,u
110 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
113 (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
115 and type_of_variable uri ugraph =
116 let module C = Cic in
117 let module R = CicReduction in
118 let module U = UriManager in
119 let _ = CicTypeChecker.typecheck uri in
122 CicEnvironment.get_cooked_obj ugraph uri
123 with Not_found -> assert false
126 C.Variable (_,_,ty,_,_) -> ty,u
130 (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
132 and type_of_mutual_inductive_defs uri i ugraph =
133 let module C = Cic in
134 let module R = CicReduction in
135 let module U = UriManager in
136 let _ = CicTypeChecker.typecheck uri in
139 CicEnvironment.get_cooked_obj ugraph uri
140 with Not_found -> assert false
143 C.InductiveDefinition (dl,_,_,_) ->
144 let (_,_,arity,_) = List.nth dl i in
149 (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
151 and type_of_mutual_inductive_constr uri i j ugraph =
152 let module C = Cic in
153 let module R = CicReduction in
154 let module U = UriManager in
155 let _ = CicTypeChecker.typecheck uri in
158 CicEnvironment.get_cooked_obj ugraph uri
159 with Not_found -> assert false
162 C.InductiveDefinition (dl,_,_,_) ->
163 let (_,_,_,cl) = List.nth dl i in
164 let (_,ty) = List.nth cl (j-1) in
170 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
173 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
175 (* the check_branch function checks if a branch of a case is refinable.
176 It returns a pair (outype_instance,args), a subst and a metasenv.
177 outype_instance is the expected result of applying the case outtype
179 The problem is that outype is in general unknown, and we should
180 try to synthesize it from the above information, that is in general
181 a second order unification problem. *)
183 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
184 let module C = Cic in
185 (* let module R = CicMetaSubst in *)
186 let module R = CicReduction in
187 match R.whd ~subst context expectedtype with
189 (n,context,actualtype, [term]), subst, metasenv, ugraph
190 | C.Appl (C.MutInd (_,_,_)::tl) ->
191 let (_,arguments) = split tl left_args_no in
192 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
193 | C.Prod (name,so,de) ->
194 (* we expect that the actual type of the branch has the due
196 (match R.whd ~subst context actualtype with
197 C.Prod (name',so',de') ->
198 let subst, metasenv, ugraph1 =
199 fo_unif_subst subst context metasenv so so' ugraph in
201 (match CicSubstitution.lift 1 term with
202 C.Appl l -> C.Appl (l@[C.Rel 1])
203 | t -> C.Appl [t ; C.Rel 1]) in
204 (* we should also check that the name variable is anonymous in
205 the actual type de' ?? *)
207 ((Some (name,(C.Decl so)))::context)
208 metasenv subst left_args_no de' term' de ugraph1
209 | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
210 | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
212 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
215 let rec type_of_aux subst metasenv context t ugraph =
216 let module C = Cic in
217 let module S = CicSubstitution in
218 let module U = UriManager in
219 let (t',_,_,_,_) as res =
224 match List.nth context (n - 1) with
225 Some (_,C.Decl ty) ->
226 t,S.lift n ty,subst,metasenv, ugraph
227 | Some (_,C.Def (_,Some ty)) ->
228 t,S.lift n ty,subst,metasenv, ugraph
229 | Some (_,C.Def (bo,None)) ->
231 (* if it is in the context it must be already well-typed*)
232 CicTypeChecker.type_of_aux' ~subst metasenv context
235 t,ty,subst,metasenv,ugraph
237 enrich localization_tbl t
238 (RefineFailure (lazy "Rel to hidden hypothesis"))
241 enrich localization_tbl t
242 (RefineFailure (lazy "Not a close term")))
243 | C.Var (uri,exp_named_subst) ->
244 let exp_named_subst',subst',metasenv',ugraph1 =
245 check_exp_named_subst
246 subst metasenv context exp_named_subst ugraph
248 let ty_uri,ugraph1 = type_of_variable uri ugraph in
250 CicSubstitution.subst_vars exp_named_subst' ty_uri
252 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
255 let (canonical_context, term,ty) =
256 CicUtil.lookup_subst n subst
258 let l',subst',metasenv',ugraph1 =
259 check_metasenv_consistency n subst metasenv context
260 canonical_context l ugraph
262 (* trust or check ??? *)
263 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
264 subst', metasenv', ugraph1
265 (* type_of_aux subst metasenv
266 context (CicSubstitution.subst_meta l term) *)
267 with CicUtil.Subst_not_found _ ->
268 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
269 let l',subst',metasenv', ugraph1 =
270 check_metasenv_consistency n subst metasenv context
271 canonical_context l ugraph
273 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
274 subst', metasenv',ugraph1)
275 | C.Sort (C.Type tno) ->
276 let tno' = CicUniv.fresh() in
277 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
278 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
280 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
281 | C.Implicit infos ->
282 let metasenv',t' = exp_impl metasenv subst context infos in
283 type_of_aux subst metasenv' context t' ugraph
285 let ty',_,subst',metasenv',ugraph1 =
286 type_of_aux subst metasenv context ty ugraph
288 let te',inferredty,subst'',metasenv'',ugraph2 =
289 type_of_aux subst' metasenv' context te ugraph1
292 let subst''',metasenv''',ugraph3 =
293 fo_unif_subst subst'' context metasenv''
294 inferredty ty' ugraph2
296 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
299 enrich localization_tbl te'
302 CicMetaSubst.ppterm_in_context subst'' te'
303 context ^ " has type " ^
304 CicMetaSubst.ppterm_in_context subst'' inferredty
305 context ^ " but is here used with type " ^
306 CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
308 | C.Prod (name,s,t) ->
309 let carr t subst context = CicMetaSubst.apply_subst subst t in
310 let coerce_to_sort in_source tgt_sort t type_to_coerce
311 subst context metasenv uragph
313 if not !insert_coercions then
314 t,type_to_coerce,subst,metasenv,ugraph
316 let coercion_src = carr type_to_coerce subst context in
317 match coercion_src with
319 t,type_to_coerce,subst,metasenv,ugraph
320 | Cic.Meta _ as meta ->
321 t, meta, subst, metasenv, ugraph
322 | Cic.Cast _ as cast ->
323 t, cast, subst, metasenv, ugraph
325 let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
326 let search = CoercGraph.look_for_coercion in
327 let boh = search coercion_src coercion_tgt in
329 | CoercGraph.NoCoercion
330 | CoercGraph.NotHandled _ ->
331 enrich localization_tbl t
334 CicMetaSubst.ppterm_in_context subst t context ^
335 " is not a type since it has type " ^
336 CicMetaSubst.ppterm_in_context
337 subst coercion_src context ^ " that is not a sort")))
338 | CoercGraph.NotMetaClosed ->
339 enrich localization_tbl t
342 CicMetaSubst.ppterm_in_context subst t context ^
343 " is not a type since it has type " ^
344 CicMetaSubst.ppterm_in_context
345 subst coercion_src context ^ " that is not a sort")))
346 | CoercGraph.SomeCoercion c ->
347 let newt, tty, subst, metasenv, ugraph =
348 avoid_double_coercion
349 subst metasenv ugraph
350 (Cic.Appl[c;t]) coercion_tgt
352 newt, tty, subst, metasenv, ugraph)
354 let s',sort1,subst',metasenv',ugraph1 =
355 type_of_aux subst metasenv context s ugraph
357 let s',sort1,subst', metasenv',ugraph1 =
358 coerce_to_sort true (Cic.Type(CicUniv.fresh()))
359 s' sort1 subst' context metasenv' ugraph1
361 let context_for_t = ((Some (name,(C.Decl s')))::context) in
362 let t',sort2,subst'',metasenv'',ugraph2 =
363 type_of_aux subst' metasenv'
364 context_for_t t ugraph1
366 let t',sort2,subst'',metasenv'',ugraph2 =
367 coerce_to_sort false (Cic.Type(CicUniv.fresh()))
368 t' sort2 subst'' context_for_t metasenv'' ugraph2
370 let sop,subst''',metasenv''',ugraph3 =
371 sort_of_prod subst'' metasenv''
372 context (name,s') (sort1,sort2) ugraph2
374 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
375 | C.Lambda (n,s,t) ->
377 let s',sort1,subst',metasenv',ugraph1 =
378 type_of_aux subst metasenv context s ugraph in
379 let s',sort1,subst',metasenv',ugraph1 =
380 if not !insert_coercions then
381 s',sort1, subst', metasenv', ugraph1
383 match CicReduction.whd ~subst:subst' context sort1 with
384 | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
386 let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
387 let search = CoercGraph.look_for_coercion in
388 let boh = search coercion_src coercion_tgt in
390 | CoercGraph.SomeCoercion c ->
391 let newt, tty, subst', metasenv', ugraph1 =
392 avoid_double_coercion
393 subst' metasenv' ugraph1
394 (Cic.Appl[c;s']) coercion_tgt
396 newt, tty, subst', metasenv', ugraph1
397 | CoercGraph.NoCoercion
398 | CoercGraph.NotHandled _ ->
399 enrich localization_tbl s'
402 CicMetaSubst.ppterm_in_context subst s' context ^
403 " is not a type since it has type " ^
404 CicMetaSubst.ppterm_in_context
405 subst coercion_src context ^ " that is not a sort")))
406 | CoercGraph.NotMetaClosed ->
407 enrich localization_tbl s'
410 CicMetaSubst.ppterm_in_context subst s' context ^
411 " is not a type since it has type " ^
412 CicMetaSubst.ppterm_in_context
413 subst coercion_src context ^ " that is not a sort")))
415 let context_for_t = ((Some (n,(C.Decl s')))::context) in
416 let t',type2,subst'',metasenv'',ugraph2 =
417 type_of_aux subst' metasenv' context_for_t t ugraph1
419 C.Lambda (n,s',t'),C.Prod (n,s',type2),
420 subst'',metasenv'',ugraph2
422 (* only to check if s is well-typed *)
423 let s',ty,subst',metasenv',ugraph1 =
424 type_of_aux subst metasenv context s ugraph
426 let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
428 let t',inferredty,subst'',metasenv'',ugraph2 =
429 type_of_aux subst' metasenv'
430 context_for_t t ugraph1
432 (* One-step LetIn reduction.
433 * Even faster than the previous solution.
434 * Moreover the inferred type is closer to the expected one.
436 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
437 subst'',metasenv'',ugraph2
438 | C.Appl (he::((_::_) as tl)) ->
439 let he',hetype,subst',metasenv',ugraph1 =
440 type_of_aux subst metasenv context he ugraph
442 let tlbody_and_type,subst'',metasenv'',ugraph2 =
444 (fun x (res,subst,metasenv,ugraph) ->
445 let x',ty,subst',metasenv',ugraph1 =
446 type_of_aux subst metasenv context x ugraph
448 (x', ty)::res,subst',metasenv',ugraph1
449 ) tl ([],subst',metasenv',ugraph1)
451 let tl',applty,subst''',metasenv''',ugraph3 =
452 eat_prods true subst'' metasenv'' context
453 hetype tlbody_and_type ugraph2
455 avoid_double_coercion
456 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
457 | C.Appl _ -> assert false
458 | C.Const (uri,exp_named_subst) ->
459 let exp_named_subst',subst',metasenv',ugraph1 =
460 check_exp_named_subst subst metasenv context
461 exp_named_subst ugraph in
462 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
464 CicSubstitution.subst_vars exp_named_subst' ty_uri
466 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
467 | C.MutInd (uri,i,exp_named_subst) ->
468 let exp_named_subst',subst',metasenv',ugraph1 =
469 check_exp_named_subst subst metasenv context
470 exp_named_subst ugraph
472 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
474 CicSubstitution.subst_vars exp_named_subst' ty_uri in
475 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
476 | C.MutConstruct (uri,i,j,exp_named_subst) ->
477 let exp_named_subst',subst',metasenv',ugraph1 =
478 check_exp_named_subst subst metasenv context
479 exp_named_subst ugraph
482 type_of_mutual_inductive_constr uri i j ugraph1
485 CicSubstitution.subst_vars exp_named_subst' ty_uri
487 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
489 | C.MutCase (uri, i, outtype, term, pl) ->
490 (* first, get the inductive type (and noparams)
491 * in the environment *)
492 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
493 let _ = CicTypeChecker.typecheck uri in
494 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
496 C.InductiveDefinition (l,expl_params,parsno,_) ->
497 List.nth l i , expl_params, parsno, u
499 enrich localization_tbl t
501 (lazy ("Unkown mutual inductive definition " ^
502 U.string_of_uri uri)))
504 let rec count_prod t =
505 match CicReduction.whd ~subst context t with
506 C.Prod (_, _, t) -> 1 + (count_prod t)
509 let no_args = count_prod arity in
510 (* now, create a "generic" MutInd *)
511 let metasenv,left_args =
512 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
514 let metasenv,right_args =
515 let no_right_params = no_args - no_left_params in
516 if no_right_params < 0 then assert false
517 else CicMkImplicit.n_fresh_metas
518 metasenv subst context no_right_params
520 let metasenv,exp_named_subst =
521 CicMkImplicit.fresh_subst metasenv subst context expl_params in
524 C.MutInd (uri,i,exp_named_subst)
527 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
529 (* check consistency with the actual type of term *)
530 let term',actual_type,subst,metasenv,ugraph1 =
531 type_of_aux subst metasenv context term ugraph in
532 let expected_type',_, subst, metasenv,ugraph2 =
533 type_of_aux subst metasenv context expected_type ugraph1
535 let actual_type = CicReduction.whd ~subst context actual_type in
536 let subst,metasenv,ugraph3 =
538 fo_unif_subst subst context metasenv
539 expected_type' actual_type ugraph2
542 enrich localization_tbl term' exn
545 CicMetaSubst.ppterm_in_context subst term'
546 context ^ " has type " ^
547 CicMetaSubst.ppterm_in_context subst actual_type
548 context ^ " but is here used with type " ^
549 CicMetaSubst.ppterm_in_context subst expected_type' context))
551 let rec instantiate_prod t =
555 match CicReduction.whd ~subst context t with
557 instantiate_prod (CicSubstitution.subst he t') tl
560 let arity_instantiated_with_left_args =
561 instantiate_prod arity left_args in
562 (* TODO: check if the sort elimination
563 * is allowed: [(I q1 ... qr)|B] *)
564 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
566 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
568 if left_args = [] then
569 (C.MutConstruct (uri,i,j,exp_named_subst))
572 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
574 let p',actual_type,subst,metasenv,ugraph1 =
575 type_of_aux subst metasenv context p ugraph
577 let constructor',expected_type, subst, metasenv,ugraph2 =
578 type_of_aux subst metasenv context constructor ugraph1
580 let outtypeinstance,subst,metasenv,ugraph3 =
581 check_branch 0 context metasenv subst no_left_params
582 actual_type constructor' expected_type ugraph2
585 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
586 ([],1,[],subst,metasenv,ugraph3) pl
589 (* we are left to check that the outype matches his instances.
590 The easy case is when the outype is specified, that amount
591 to a trivial check. Otherwise, we should guess a type from
595 let outtype,outtypety, subst, metasenv,ugraph4 =
596 type_of_aux subst metasenv context outtype ugraph4 in
599 (let candidate,ugraph5,metasenv,subst =
600 let exp_name_subst, metasenv =
602 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
604 let uris = CicUtil.params_of_obj o in
606 fun uri (acc,metasenv) ->
607 let metasenv',new_meta =
608 CicMkImplicit.mk_implicit metasenv subst context
611 CicMkImplicit.identity_relocation_list_for_metavariable
614 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
618 match left_args,right_args with
619 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
621 let rec mk_right_args =
624 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
626 let right_args_no = List.length right_args in
627 let lifted_left_args =
628 List.map (CicSubstitution.lift right_args_no) left_args
630 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
631 (lifted_left_args @ mk_right_args right_args_no))
634 FreshNamesGenerator.mk_fresh_name ~subst metasenv
635 context Cic.Anonymous ~typ:ty
637 match outtypeinstances with
639 let extended_context =
640 let rec add_right_args =
642 Cic.Prod (name,ty,t) ->
643 Some (name,Cic.Decl ty)::(add_right_args t)
646 (Some (fresh_name,Cic.Decl ty))::
648 (add_right_args arity_instantiated_with_left_args))@
651 let metasenv,new_meta =
652 CicMkImplicit.mk_implicit metasenv subst extended_context
655 CicMkImplicit.identity_relocation_list_for_metavariable
658 let rec add_lambdas b =
660 Cic.Prod (name,ty,t) ->
661 Cic.Lambda (name,ty,(add_lambdas b t))
662 | _ -> Cic.Lambda (fresh_name, ty, b)
665 add_lambdas (Cic.Meta (new_meta,irl))
666 arity_instantiated_with_left_args
668 (Some candidate),ugraph4,metasenv,subst
669 | (constructor_args_no,_,instance,_)::tl ->
671 let instance',subst,metasenv =
672 CicMetaSubst.delift_rels subst metasenv
673 constructor_args_no instance
675 let candidate,ugraph,metasenv,subst =
677 fun (candidate_oty,ugraph,metasenv,subst)
678 (constructor_args_no,_,instance,_) ->
679 match candidate_oty with
680 | None -> None,ugraph,metasenv,subst
683 let instance',subst,metasenv =
684 CicMetaSubst.delift_rels subst metasenv
685 constructor_args_no instance
687 let subst,metasenv,ugraph =
688 fo_unif_subst subst context metasenv
691 candidate_oty,ugraph,metasenv,subst
693 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
694 | CicUnification.UnificationFailure _
695 | CicUnification.Uncertain _ ->
696 None,ugraph,metasenv,subst
697 ) (Some instance',ugraph4,metasenv,subst) tl
700 | None -> None, ugraph,metasenv,subst
702 let rec add_lambdas n b =
704 Cic.Prod (name,ty,t) ->
705 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
707 Cic.Lambda (fresh_name, ty,
708 CicSubstitution.lift (n + 1) t)
711 (add_lambdas 0 t arity_instantiated_with_left_args),
712 ugraph,metasenv,subst
713 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
714 None,ugraph4,metasenv,subst
717 | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
719 let subst,metasenv,ugraph =
720 fo_unif_subst subst context metasenv
721 candidate outtype ugraph5
723 C.MutCase (uri, i, outtype, term', pl'),
724 CicReduction.head_beta_reduce
725 (CicMetaSubst.apply_subst subst
726 (Cic.Appl (outtype::right_args@[term']))),
727 subst,metasenv,ugraph)
728 | _ -> (* easy case *)
729 let tlbody_and_type,subst,metasenv,ugraph4 =
731 (fun x (res,subst,metasenv,ugraph) ->
732 let x',ty,subst',metasenv',ugraph1 =
733 type_of_aux subst metasenv context x ugraph
735 (x', ty)::res,subst',metasenv',ugraph1
736 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
738 let _,_,subst,metasenv,ugraph4 =
739 eat_prods false subst metasenv context
740 outtypety tlbody_and_type ugraph4
742 let _,_, subst, metasenv,ugraph5 =
743 type_of_aux subst metasenv context
744 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
746 let (subst,metasenv,ugraph6) =
748 (fun (subst,metasenv,ugraph)
749 (constructor_args_no,context,instance,args) ->
753 CicSubstitution.lift constructor_args_no outtype
755 C.Appl (outtype'::args)
757 CicReduction.whd ~subst context appl
759 fo_unif_subst subst context metasenv
760 instance instance' ugraph)
761 (subst,metasenv,ugraph5) outtypeinstances
763 C.MutCase (uri, i, outtype, term', pl'),
764 CicReduction.head_beta_reduce
765 (CicMetaSubst.apply_subst subst
766 (C.Appl(outtype::right_args@[term]))),
767 subst,metasenv,ugraph6)
769 let fl_ty',subst,metasenv,types,ugraph1 =
771 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
772 let ty',_,subst',metasenv',ugraph1 =
773 type_of_aux subst metasenv context ty ugraph
775 fl @ [ty'],subst',metasenv',
776 Some (C.Name n,(C.Decl ty')) :: types, ugraph
777 ) ([],subst,metasenv,[],ugraph) fl
779 let len = List.length types in
780 let context' = types@context in
781 let fl_bo',subst,metasenv,ugraph2 =
783 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
784 let bo',ty_of_bo,subst,metasenv,ugraph1 =
785 type_of_aux subst metasenv context' bo ugraph
787 let subst',metasenv',ugraph' =
788 fo_unif_subst subst context' metasenv
789 ty_of_bo (CicSubstitution.lift len ty) ugraph1
791 fl @ [bo'] , subst',metasenv',ugraph'
792 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
794 let ty = List.nth fl_ty' i in
795 (* now we have the new ty in fl_ty', the new bo in fl_bo',
796 * and we want the new fl with bo' and ty' injected in the right
799 let rec map3 f l1 l2 l3 =
802 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
805 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
808 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
810 let fl_ty',subst,metasenv,types,ugraph1 =
812 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
813 let ty',_,subst',metasenv',ugraph1 =
814 type_of_aux subst metasenv context ty ugraph
816 fl @ [ty'],subst',metasenv',
817 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
818 ) ([],subst,metasenv,[],ugraph) fl
820 let len = List.length types in
821 let context' = types@context in
822 let fl_bo',subst,metasenv,ugraph2 =
824 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
825 let bo',ty_of_bo,subst,metasenv,ugraph1 =
826 type_of_aux subst metasenv context' bo ugraph
828 let subst',metasenv',ugraph' =
829 fo_unif_subst subst context' metasenv
830 ty_of_bo (CicSubstitution.lift len ty) ugraph1
832 fl @ [bo'],subst',metasenv',ugraph'
833 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
835 let ty = List.nth fl_ty' i in
836 (* now we have the new ty in fl_ty', the new bo in fl_bo',
837 * and we want the new fl with bo' and ty' injected in the right
840 let rec map3 f l1 l2 l3 =
843 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
846 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
849 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
851 relocalize localization_tbl t t';
854 and avoid_double_coercion subst metasenv ugraph t ty =
856 | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when
857 CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
858 let source_carr = CoercGraph.source_of c2 in
859 let tgt_carr = CicMetaSubst.apply_subst subst ty in
860 (match CoercGraph.look_for_coercion source_carr tgt_carr
862 | CoercGraph.SomeCoercion c ->
863 Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph
864 | _ -> assert false) (* the composite coercion must exist *)
865 | _ -> t, ty, subst, metasenv, ugraph
867 (* check_metasenv_consistency checks that the "canonical" context of a
868 metavariable is consitent - up to relocation via the relocation list l -
869 with the actual context *)
870 and check_metasenv_consistency
871 metano subst metasenv context canonical_context l ugraph
873 let module C = Cic in
874 let module R = CicReduction in
875 let module S = CicSubstitution in
876 let lifted_canonical_context =
880 | (Some (n,C.Decl t))::tl ->
881 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
882 | (Some (n,C.Def (t,None)))::tl ->
883 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
884 | None::tl -> None::(aux (i+1) tl)
885 | (Some (n,C.Def (t,Some ty)))::tl ->
887 C.Def ((S.subst_meta l (S.lift i t)),
888 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
890 aux 1 canonical_context
894 (fun (l,subst,metasenv,ugraph) t ct ->
897 l @ [None],subst,metasenv,ugraph
898 | Some t,Some (_,C.Def (ct,_)) ->
899 let subst',metasenv',ugraph' =
901 fo_unif_subst subst context metasenv t ct ugraph
902 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))))))
904 l @ [Some t],subst',metasenv',ugraph'
905 | Some t,Some (_,C.Decl ct) ->
906 let t',inferredty,subst',metasenv',ugraph1 =
907 type_of_aux subst metasenv context t ugraph
909 let subst'',metasenv'',ugraph2 =
912 subst' context metasenv' inferredty ct ugraph1
913 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))))))
915 l @ [Some t'], subst'',metasenv'',ugraph2
917 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
919 Invalid_argument _ ->
923 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
924 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
925 (CicMetaSubst.ppcontext subst canonical_context))))
927 and check_exp_named_subst metasubst metasenv context tl ugraph =
928 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
930 [] -> [],metasubst,metasenv,ugraph
932 let ty_uri,ugraph1 = type_of_variable uri ugraph in
934 CicSubstitution.subst_vars substs ty_uri in
935 (* CSC: why was this code here? it is wrong
936 (match CicEnvironment.get_cooked_obj ~trust:false uri with
937 Cic.Variable (_,Some bo,_,_) ->
940 "A variable with a body can not be explicit substituted"))
941 | Cic.Variable (_,None,_,_) -> ()
945 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
948 let t',typeoft,metasubst',metasenv',ugraph2 =
949 type_of_aux metasubst metasenv context t ugraph1 in
950 let subst = uri,t' in
951 let metasubst'',metasenv'',ugraph3 =
954 metasubst' context metasenv' typeoft typeofvar ugraph2
956 raise (RefineFailure (lazy
957 ("Wrong Explicit Named Substitution: " ^
958 CicMetaSubst.ppterm metasubst' typeoft ^
959 " not unifiable with " ^
960 CicMetaSubst.ppterm metasubst' typeofvar)))
962 (* FIXME: no mere tail recursive! *)
963 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
964 check_exp_named_subst_aux
965 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
967 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
969 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
972 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
973 let module C = Cic in
974 let context_for_t2 = (Some (name,C.Decl s))::context in
975 let t1'' = CicReduction.whd ~subst context t1 in
976 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
977 match (t1'', t2'') with
978 (C.Sort s1, C.Sort s2)
979 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
980 (* different than Coq manual!!! *)
981 C.Sort s2,subst,metasenv,ugraph
982 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
983 let t' = CicUniv.fresh() in
984 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
985 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
986 C.Sort (C.Type t'),subst,metasenv,ugraph2
987 | (C.Sort _,C.Sort (C.Type t1)) ->
988 C.Sort (C.Type t1),subst,metasenv,ugraph
989 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
990 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
991 (* TODO how can we force the meta to become a sort? If we don't we
992 * brake the invariant that refine produce only well typed terms *)
993 (* TODO if we check the non meta term and if it is a sort then we
994 * are likely to know the exact value of the result e.g. if the rhs
995 * is a Sort (Prop | Set | CProp) then the result is the rhs *)
997 CicMkImplicit.mk_implicit_sort metasenv subst in
998 let (subst, metasenv,ugraph1) =
999 fo_unif_subst subst context_for_t2 metasenv
1000 (C.Meta (idx,[])) t2'' ugraph
1002 t2'',subst,metasenv,ugraph1
1008 ("Two sorts were expected, found %s " ^^
1009 "(that reduces to %s) and %s (that reduces to %s)")
1010 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1011 (CicPp.ppterm t2''))))
1014 allow_coercions subst metasenv context hetype tlbody_and_type ugraph
1016 let rec mk_prod metasenv context' =
1019 let (metasenv, idx) =
1020 CicMkImplicit.mk_implicit_type metasenv subst context'
1023 CicMkImplicit.identity_relocation_list_for_metavariable context'
1025 metasenv,Cic.Meta (idx, irl)
1027 let (metasenv, idx) =
1028 CicMkImplicit.mk_implicit_type metasenv subst context'
1031 CicMkImplicit.identity_relocation_list_for_metavariable context'
1033 let meta = Cic.Meta (idx,irl) in
1035 (* The name must be fresh for context. *)
1036 (* Nevertheless, argty is well-typed only in context. *)
1037 (* Thus I generate a name (name_hint) in context and *)
1038 (* then I generate a name --- using the hint name_hint *)
1039 (* --- that is fresh in context'. *)
1041 (* Cic.Name "pippo" *)
1042 FreshNamesGenerator.mk_fresh_name ~subst metasenv
1043 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
1044 (CicMetaSubst.apply_subst_context subst context)
1046 ~typ:(CicMetaSubst.apply_subst subst argty)
1048 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
1049 FreshNamesGenerator.mk_fresh_name ~subst
1050 [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
1052 let metasenv,target =
1053 mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
1055 metasenv,Cic.Prod (name,meta,target)
1057 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
1058 let (subst, metasenv,ugraph1) =
1060 fo_unif_subst subst context metasenv hetype hetype' ugraph
1062 debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
1063 (CicPp.ppterm hetype)
1064 (CicPp.ppterm hetype')
1065 (CicMetaSubst.ppmetasenv [] metasenv)
1066 (CicMetaSubst.ppsubst subst)));
1070 let rec eat_prods metasenv subst context hetype ugraph =
1072 | [] -> [],metasenv,subst,hetype,ugraph
1073 | (hete, hety)::tl ->
1076 let arg,subst,metasenv,ugraph1 =
1078 let subst,metasenv,ugraph1 =
1079 fo_unif_subst subst context metasenv hety s ugraph
1081 hete,subst,metasenv,ugraph1
1082 with exn when allow_coercions && !insert_coercions ->
1083 (* we search a coercion from hety to s *)
1084 let coer, tgt_carr =
1085 let carr t subst context =
1086 CicMetaSubst.apply_subst subst t
1088 let c_hety = carr hety subst context in
1089 let c_s = carr s subst context in
1090 CoercGraph.look_for_coercion c_hety c_s, c_s
1093 | CoercGraph.NoCoercion
1094 | CoercGraph.NotHandled _ ->
1095 enrich localization_tbl hete
1097 (lazy ("The term " ^
1098 CicMetaSubst.ppterm_in_context subst hete
1099 context ^ " has type " ^
1100 CicMetaSubst.ppterm_in_context subst hety
1101 context ^ " but is here used with type " ^
1102 CicMetaSubst.ppterm_in_context subst s context
1103 (* "\nReason: " ^ Lazy.force e*))))
1104 | CoercGraph.NotMetaClosed ->
1105 enrich localization_tbl hete
1107 (lazy ("The term " ^
1108 CicMetaSubst.ppterm_in_context subst hete
1109 context ^ " has type " ^
1110 CicMetaSubst.ppterm_in_context subst hety
1111 context ^ " but is here used with type " ^
1112 CicMetaSubst.ppterm_in_context subst s context
1113 (* "\nReason: " ^ Lazy.force e*))))
1114 | CoercGraph.SomeCoercion c ->
1115 let newt, _, subst, metasenv, ugraph =
1116 avoid_double_coercion
1117 subst metasenv ugraph
1118 (Cic.Appl[c;hete]) tgt_carr in
1120 let newty,newhety,subst,metasenv,ugraph =
1121 type_of_aux subst metasenv context newt ugraph in
1122 let subst,metasenv,ugraph1 =
1123 fo_unif_subst subst context metasenv
1126 newt, subst, metasenv, ugraph
1128 enrich localization_tbl hete
1130 (lazy ("The term " ^
1131 CicMetaSubst.ppterm_in_context subst hete
1132 context ^ " has type " ^
1133 CicMetaSubst.ppterm_in_context subst hety
1134 context ^ " but is here used with type " ^
1135 CicMetaSubst.ppterm_in_context subst s context
1136 (* "\nReason: " ^ Lazy.force e*)))) exn)
1138 enrich localization_tbl hete
1140 (lazy ("The term " ^
1141 CicMetaSubst.ppterm_in_context subst hete
1142 context ^ " has type " ^
1143 CicMetaSubst.ppterm_in_context subst hety
1144 context ^ " but is here used with type " ^
1145 CicMetaSubst.ppterm_in_context subst s context
1146 (* "\nReason: " ^ Lazy.force e*)))) exn
1148 let coerced_args,metasenv',subst',t',ugraph2 =
1149 eat_prods metasenv subst context
1150 (CicSubstitution.subst arg t) ugraph1 tl
1152 arg::coerced_args,metasenv',subst',t',ugraph2
1156 let coerced_args,metasenv,subst,t,ugraph2 =
1157 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1159 coerced_args,t,subst,metasenv,ugraph2
1162 (* eat prods ends here! *)
1164 let t',ty,subst',metasenv',ugraph1 =
1165 type_of_aux [] metasenv context t ugraph
1167 let substituted_t = CicMetaSubst.apply_subst subst' t' in
1168 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1169 (* Andrea: ho rimesso qui l'applicazione della subst al
1170 metasenv dopo che ho droppato l'invariante che il metsaenv
1171 e' sempre istanziato *)
1172 let substituted_metasenv =
1173 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1175 (* substituted_t,substituted_ty,substituted_metasenv *)
1176 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1178 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1180 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1181 let cleaned_metasenv =
1183 (function (n,context,ty) ->
1184 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1189 | Some (n, Cic.Decl t) ->
1191 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1192 | Some (n, Cic.Def (bo,ty)) ->
1193 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1198 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1200 Some (n, Cic.Def (bo',ty'))
1204 ) substituted_metasenv
1206 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1209 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1211 type_of_aux' ?localization_tbl metasenv context term ugraph
1213 CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1215 let undebrujin uri typesno tys t =
1218 (fun (name,_,_,_) (i,t) ->
1219 (* here the explicit_named_substituion is assumed to be *)
1221 let t' = Cic.MutInd (uri,i,[]) in
1222 let t = CicSubstitution.subst t' t in
1224 ) tys (typesno - 1,t))
1226 let map_first_n n start f g l =
1227 let rec aux acc k l =
1230 | [] -> raise (Invalid_argument "map_first_n")
1231 | hd :: tl -> f hd k (aux acc (k+1) tl)
1237 (*CSC: this is a very rough approximation; to be finished *)
1238 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1239 let subst,metasenv,ugraph,tys =
1241 (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1242 let subst,metasenv,ugraph,cl =
1244 (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1245 let rec aux ctx k subst = function
1246 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1247 let subst,metasenv,ugraph,tl =
1249 (subst,metasenv,ugraph,[])
1250 (fun t n (subst,metasenv,ugraph,acc) ->
1251 let subst,metasenv,ugraph =
1253 subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1255 subst,metasenv,ugraph,(t::acc))
1256 (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1259 subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1260 | Cic.MutInd(uri',_,_) as t when uri = uri'->
1261 subst,metasenv,ugraph,t
1262 | Cic.Prod (name,s,t) ->
1263 let ctx = (Some (name,Cic.Decl s))::ctx in
1264 let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1265 subst,metasenv,ugraph,Cic.Prod (name,s,t)
1269 (lazy "not well formed constructor type"))
1271 let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1272 subst,metasenv,ugraph,(name,ty) :: acc)
1273 cl (subst,metasenv,ugraph,[])
1275 subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1276 tys ([],metasenv,ugraph,[])
1278 let substituted_tys =
1280 (fun (name,ind,arity,cl) ->
1282 List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1284 name,ind,CicMetaSubst.apply_subst subst arity,cl)
1287 metasenv,ugraph,substituted_tys
1289 let typecheck metasenv uri obj ~localization_tbl =
1290 let ugraph = CicUniv.empty_ugraph in
1292 Cic.Constant (name,Some bo,ty,args,attrs) ->
1293 let bo',boty,metasenv,ugraph =
1294 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1295 let ty',_,metasenv,ugraph =
1296 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1297 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1298 let bo' = CicMetaSubst.apply_subst subst bo' in
1299 let ty' = CicMetaSubst.apply_subst subst ty' in
1300 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1301 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1302 | Cic.Constant (name,None,ty,args,attrs) ->
1303 let ty',_,metasenv,ugraph =
1304 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1306 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1307 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1308 assert (metasenv' = metasenv);
1309 (* Here we do not check the metasenv for correctness *)
1310 let bo',boty,metasenv,ugraph =
1311 type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1312 let ty',sort,metasenv,ugraph =
1313 type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1317 (* instead of raising Uncertain, let's hope that the meta will become
1320 | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1322 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1323 let bo' = CicMetaSubst.apply_subst subst bo' in
1324 let ty' = CicMetaSubst.apply_subst subst ty' in
1325 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1326 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1327 | Cic.Variable _ -> assert false (* not implemented *)
1328 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1329 (*CSC: this code is greately simplified and many many checks are missing *)
1330 (*CSC: e.g. the constructors are not required to build their own types, *)
1331 (*CSC: the arities are not required to have as type a sort, etc. *)
1332 let uri = match uri with Some uri -> uri | None -> assert false in
1333 let typesno = List.length tys in
1334 (* first phase: we fix only the types *)
1335 let metasenv,ugraph,tys =
1337 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1338 let ty',_,metasenv,ugraph =
1339 type_of_aux' ~localization_tbl metasenv [] ty ugraph
1341 metasenv,ugraph,(name,b,ty',cl)::res
1342 ) tys (metasenv,ugraph,[]) in
1344 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1345 (* second phase: we fix only the constructors *)
1346 let metasenv,ugraph,tys =
1348 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1349 let metasenv,ugraph,cl' =
1351 (fun (name,ty) (metasenv,ugraph,res) ->
1353 CicTypeChecker.debrujin_constructor
1354 ~cb:(relocalize localization_tbl) uri typesno ty in
1355 let ty',_,metasenv,ugraph =
1356 type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1357 let ty' = undebrujin uri typesno tys ty' in
1358 metasenv,ugraph,(name,ty')::res
1359 ) cl (metasenv,ugraph,[])
1361 metasenv,ugraph,(name,b,ty,cl')::res
1362 ) tys (metasenv,ugraph,[]) in
1363 (* third phase: we check the positivity condition *)
1364 let metasenv,ugraph,tys =
1365 are_all_occurrences_positive metasenv ugraph uri tys paramsno
1367 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1370 let type_of_aux' metasenv context term =
1373 type_of_aux' metasenv context term in
1375 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1377 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1380 | RefineFailure msg as e ->
1381 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1383 | Uncertain msg as e ->
1384 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1388 let profiler2 = HExtlib.profile "CicRefine"
1390 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1391 profiler2.HExtlib.profile
1392 (type_of_aux' ?localization_tbl metasenv context term) ugraph
1394 let typecheck ~localization_tbl metasenv uri obj =
1395 profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj