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/.
26 (* TODO factorize functions to frequent errors (e.g. "Unknwon mutual inductive
31 exception AssertFailure of string;;
32 exception TypeCheckerFailure of string;;
36 let rec debug_aux t i =
38 let module U = UriManager in
39 CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
42 raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
45 let debug_print = prerr_endline ;;
50 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
52 raise (TypeCheckerFailure "Parameters number < left parameters number")
55 let debrujin_constructor uri number_of_types =
59 C.Rel n as t when n <= k -> t
61 raise (TypeCheckerFailure "unbound variable found in constructor type")
62 | C.Var (uri,exp_named_subst) ->
63 let exp_named_subst' =
64 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
66 C.Var (uri,exp_named_subst')
67 | C.Meta _ -> assert false
69 | C.Implicit _ as t -> t
70 | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
71 | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
72 | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
73 | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t)
74 | C.Appl l -> C.Appl (List.map (aux k) l)
75 | C.Const (uri,exp_named_subst) ->
76 let exp_named_subst' =
77 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
79 C.Const (uri,exp_named_subst')
80 | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
81 if exp_named_subst != [] then
82 raise (TypeCheckerFailure
83 ("non-empty explicit named substitution is applied to "^
84 "a mutual inductive type which is being defined")) ;
85 C.Rel (k + number_of_types - tyno) ;
86 | C.MutInd (uri',tyno,exp_named_subst) ->
87 let exp_named_subst' =
88 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
90 C.MutInd (uri',tyno,exp_named_subst')
91 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
92 let exp_named_subst' =
93 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
95 C.MutConstruct (uri,tyno,consno,exp_named_subst')
96 | C.MutCase (sp,i,outty,t,pl) ->
97 C.MutCase (sp, i, aux k outty, aux k t,
100 let len = List.length fl in
103 (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
108 let len = List.length fl in
111 (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
114 C.CoFix (i, liftedfl)
119 exception CicEnvironmentError;;
121 let rec type_of_constant ~logger uri ugraph =
122 let module C = Cic in
123 let module R = CicReduction in
124 let module U = UriManager in
126 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
127 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
128 | CicEnvironment.UncheckedObj uobj ->
129 logger#log (`Start_type_checking uri) ;
130 (* let's typecheck the uncooked obj *)
132 (****************************************************************
133 TASSI: FIXME qui e' inutile ricordarselo,
134 tanto poi lo richiediamo alla cache che da quello su disco
135 *****************************************************************)
139 C.Constant (_,Some te,ty,_,_) ->
140 let _,ugraph = type_of ~logger ty ugraph in
141 let type_of_te,ugraph' = type_of ~logger te ugraph in
142 let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in
144 raise (TypeCheckerFailure (sprintf
145 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
146 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
150 | C.Constant (_,None,ty,_,_) ->
151 (* only to check that ty is well-typed *)
152 let _,ugraph' = type_of ~logger ty ugraph in
154 | C.CurrentProof (_,conjs,te,ty,_,_) ->
157 (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
159 type_of_aux' ~logger metasenv context ty ugraph
161 (metasenv @ [conj],ugraph')
164 let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
165 let type_of_te,ugraph3 =
166 type_of_aux' ~logger conjs [] te ugraph2
168 let b,ugraph4 = (R.are_convertible [] type_of_te ty ugraph3) in
170 raise (TypeCheckerFailure (sprintf
171 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
172 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
177 raise (TypeCheckerFailure
178 ("Unknown constant:" ^ U.string_of_uri uri)))
181 CicEnvironment.set_type_checking_info uri;
182 logger#log (`Type_checking_completed uri) ;
183 match CicEnvironment.is_type_checked ~trust:false ugraph uri with
184 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
185 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
186 with Invalid_argument s ->
190 match cobj,ugraph with
191 (C.Constant (_,_,ty,_,_)),g -> ty,g
192 | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g
194 raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
196 and type_of_variable ~logger uri ugraph =
197 let module C = Cic in
198 let module R = CicReduction in
199 let module U = UriManager in
200 (* 0 because a variable is never cooked => no partial cooking at one level *)
201 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
202 CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
203 | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
204 logger#log (`Start_type_checking uri) ;
205 (* only to check that ty is well-typed *)
206 let _,ugraph1 = type_of ~logger ty ugraph in
211 let ty_bo,ugraph' = type_of ~logger bo ugraph1 in
212 let b,ugraph'' = (R.are_convertible [] ty_bo ty ugraph') in
214 raise (TypeCheckerFailure
215 ("Unknown variable:" ^ U.string_of_uri uri))
220 CicEnvironment.set_type_checking_info uri ;
221 logger#log (`Type_checking_completed uri) ;
222 match CicEnvironment.is_type_checked ~trust:false ugraph uri with
223 CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') ->
225 | CicEnvironment.CheckedObj _
226 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
227 with Invalid_argument s ->
231 raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
233 and does_not_occur context n nn te =
234 let module C = Cic in
235 (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
236 (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
238 match CicReduction.whd context te with
239 C.Rel m when m > n && m <= nn -> false
241 | C.Meta _ (* CSC: Are we sure? No recursion?*)
243 | C.Implicit _ -> true
245 does_not_occur context n nn te && does_not_occur context n nn ty
246 | C.Prod (name,so,dest) ->
247 does_not_occur context n nn so &&
248 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
250 | C.Lambda (name,so,dest) ->
251 does_not_occur context n nn so &&
252 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
254 | C.LetIn (name,so,dest) ->
255 does_not_occur context n nn so &&
256 does_not_occur ((Some (name,(C.Def (so,None))))::context)
257 (n + 1) (nn + 1) dest
259 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
260 | C.Var (_,exp_named_subst)
261 | C.Const (_,exp_named_subst)
262 | C.MutInd (_,_,exp_named_subst)
263 | C.MutConstruct (_,_,_,exp_named_subst) ->
264 List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
266 | C.MutCase (_,_,out,te,pl) ->
267 does_not_occur context n nn out && does_not_occur context n nn te &&
268 List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
270 let len = List.length fl in
271 let n_plus_len = n + len in
272 let nn_plus_len = nn + len in
274 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
277 (fun (_,_,ty,bo) i ->
278 i && does_not_occur context n nn ty &&
279 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
282 let len = List.length fl in
283 let n_plus_len = n + len in
284 let nn_plus_len = nn + len in
286 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
290 i && does_not_occur context n nn ty &&
291 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
294 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
295 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
296 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
297 (*CSC strictly_positive *)
298 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
299 and weakly_positive context n nn uri te =
300 let module C = Cic in
301 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
303 C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
305 (*CSC mettere in cicSubstitution *)
306 let rec subst_inductive_type_with_dummy_mutind =
308 C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
310 | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
312 | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
313 | C.Prod (name,so,ta) ->
314 C.Prod (name, subst_inductive_type_with_dummy_mutind so,
315 subst_inductive_type_with_dummy_mutind ta)
316 | C.Lambda (name,so,ta) ->
317 C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
318 subst_inductive_type_with_dummy_mutind ta)
320 C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
321 | C.MutCase (uri,i,outtype,term,pl) ->
323 subst_inductive_type_with_dummy_mutind outtype,
324 subst_inductive_type_with_dummy_mutind term,
325 List.map subst_inductive_type_with_dummy_mutind pl)
327 C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
328 subst_inductive_type_with_dummy_mutind ty,
329 subst_inductive_type_with_dummy_mutind bo)) fl)
331 C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
332 subst_inductive_type_with_dummy_mutind ty,
333 subst_inductive_type_with_dummy_mutind bo)) fl)
334 | C.Const (uri,exp_named_subst) ->
335 let exp_named_subst' =
337 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
340 C.Const (uri,exp_named_subst')
341 | C.MutInd (uri,typeno,exp_named_subst) ->
342 let exp_named_subst' =
344 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
347 C.MutInd (uri,typeno,exp_named_subst')
348 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
349 let exp_named_subst' =
351 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
354 C.MutConstruct (uri,typeno,consno,exp_named_subst')
357 match CicReduction.whd context te with
358 C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
359 | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
360 | C.Prod (C.Anonymous,source,dest) ->
361 strictly_positive context n nn
362 (subst_inductive_type_with_dummy_mutind source) &&
363 weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
364 (n + 1) (nn + 1) uri dest
365 | C.Prod (name,source,dest) when
366 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
367 (* dummy abstraction, so we behave as in the anonimous case *)
368 strictly_positive context n nn
369 (subst_inductive_type_with_dummy_mutind source) &&
370 weakly_positive ((Some (name,(C.Decl source)))::context)
371 (n + 1) (nn + 1) uri dest
372 | C.Prod (name,source,dest) ->
373 does_not_occur context n nn
374 (subst_inductive_type_with_dummy_mutind source)&&
375 weakly_positive ((Some (name,(C.Decl source)))::context)
376 (n + 1) (nn + 1) uri dest
378 raise (TypeCheckerFailure "Malformed inductive constructor type")
380 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
381 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
382 and instantiate_parameters params c =
383 let module C = Cic in
384 match (c,params) with
386 | (C.Prod (_,_,ta), he::tl) ->
387 instantiate_parameters tl
388 (CicSubstitution.subst he ta)
389 | (C.Cast (te,_), _) -> instantiate_parameters params te
390 | (t,l) -> raise (AssertFailure "1")
392 and strictly_positive context n nn te =
393 let module C = Cic in
394 let module U = UriManager in
395 match CicReduction.whd context te with
398 (*CSC: bisogna controllare ty????*)
399 strictly_positive context n nn te
400 | C.Prod (name,so,ta) ->
401 does_not_occur context n nn so &&
402 strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
403 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
404 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
405 | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
406 let (ok,paramsno,ity,cl,name) =
407 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
409 C.InductiveDefinition (tl,_,paramsno,_) ->
410 let (name,_,ity,cl) = List.nth tl i in
411 (List.length tl = 1, paramsno, ity, cl, name)
413 raise (TypeCheckerFailure
414 ("Unknown inductive type:" ^ U.string_of_uri uri))
416 let (params,arguments) = split tl paramsno in
417 let lifted_params = List.map (CicSubstitution.lift 1) params in
421 instantiate_parameters lifted_params
422 (CicSubstitution.subst_vars exp_named_subst te)
427 (fun x i -> i && does_not_occur context n nn x)
429 (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
434 ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
437 | t -> does_not_occur context n nn t
439 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
440 and are_all_occurrences_positive context uri indparamsno i n nn te =
441 let module C = Cic in
442 match CicReduction.whd context te with
443 C.Appl ((C.Rel m)::tl) when m = i ->
444 (*CSC: riscrivere fermandosi a 0 *)
445 (* let's check if the inductive type is applied at least to *)
446 (* indparamsno parameters *)
452 match CicReduction.whd context x with
453 C.Rel m when m = n - (indparamsno - k) -> k - 1
455 raise (TypeCheckerFailure
456 ("Non-positive occurence in mutual inductive definition(s) " ^
457 UriManager.string_of_uri uri))
461 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
463 raise (TypeCheckerFailure
464 ("Non-positive occurence in mutual inductive definition(s) " ^
465 UriManager.string_of_uri uri))
466 | C.Rel m when m = i ->
467 if indparamsno = 0 then
470 raise (TypeCheckerFailure
471 ("Non-positive occurence in mutual inductive definition(s) " ^
472 UriManager.string_of_uri uri))
473 | C.Prod (C.Anonymous,source,dest) ->
474 strictly_positive context n nn source &&
475 are_all_occurrences_positive
476 ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
477 (i+1) (n + 1) (nn + 1) dest
478 | C.Prod (name,source,dest) when
479 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
480 (* dummy abstraction, so we behave as in the anonimous case *)
481 strictly_positive context n nn source &&
482 are_all_occurrences_positive
483 ((Some (name,(C.Decl source)))::context) uri indparamsno
484 (i+1) (n + 1) (nn + 1) dest
485 | C.Prod (name,source,dest) ->
486 does_not_occur context n nn source &&
487 are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
488 uri indparamsno (i+1) (n + 1) (nn + 1) dest
491 (TypeCheckerFailure ("Malformed inductive constructor type " ^
492 (UriManager.string_of_uri uri)))
494 (* Main function to checks the correctness of a mutual *)
495 (* inductive block definition. This is the function *)
496 (* exported to the proof-engine. *)
497 and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
498 let module U = UriManager in
499 (* let's check if the arity of the inductive types are well *)
501 let ugrap1 = List.fold_left
502 (fun ugraph (_,_,x,_) -> let _,ugraph' =
503 type_of ~logger x ugraph in ugraph')
506 (* let's check if the types of the inductive constructors *)
507 (* are well formed. *)
508 (* In order not to use type_of_aux we put the types of the *)
509 (* mutual inductive types at the head of the types of the *)
510 (* constructors using Prods *)
511 let len = List.length itl in
513 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
516 (fun (_,_,_,cl) (i,ugraph) ->
519 (fun ugraph (name,te) ->
520 let debrujinedte = debrujin_constructor uri len te in
523 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
526 let _,ugraph' = type_of ~logger augmented_term ugraph in
527 (* let's check also the positivity conditions *)
530 (are_all_occurrences_positive tys uri indparamsno i 0 len
534 (TypeCheckerFailure ("Non positive occurence in " ^
535 U.string_of_uri uri))
544 (* Main function to checks the correctness of a mutual *)
545 (* inductive block definition. *)
546 and check_mutual_inductive_defs uri obj ugraph =
548 Cic.InductiveDefinition (itl, params, indparamsno, _) ->
549 typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph
551 raise (TypeCheckerFailure (
552 "Unknown mutual inductive definition:" ^
553 UriManager.string_of_uri uri))
555 and type_of_mutual_inductive_defs ~logger uri i ugraph =
556 let module C = Cic in
557 let module R = CicReduction in
558 let module U = UriManager in
560 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
561 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
562 | CicEnvironment.UncheckedObj uobj ->
563 logger#log (`Start_type_checking uri) ;
565 check_mutual_inductive_defs ~logger uri uobj ugraph
567 (* TASSI: FIXME: check ugraph1 == ugraph ritornato da env *)
569 CicEnvironment.set_type_checking_info uri ;
570 logger#log (`Type_checking_completed uri) ;
571 (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
572 CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
573 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
576 Invalid_argument s ->
581 C.InductiveDefinition (dl,_,_,_) ->
582 let (_,_,arity,_) = List.nth dl i in
585 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
586 U.string_of_uri uri))
588 and type_of_mutual_inductive_constr ~logger uri i j ugraph =
589 let module C = Cic in
590 let module R = CicReduction in
591 let module U = UriManager in
593 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
594 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
595 | CicEnvironment.UncheckedObj uobj ->
596 logger#log (`Start_type_checking uri) ;
598 check_mutual_inductive_defs ~logger uri uobj ugraph
600 (* check ugraph1 validity ??? == ugraph' *)
602 CicEnvironment.set_type_checking_info uri ;
603 logger#log (`Type_checking_completed uri) ;
605 CicEnvironment.is_type_checked ~trust:false ugraph uri
607 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
608 | CicEnvironment.UncheckedObj _ ->
609 raise CicEnvironmentError)
611 Invalid_argument s ->
616 C.InductiveDefinition (dl,_,_,_) ->
617 let (_,_,_,cl) = List.nth dl i in
618 let (_,ty) = List.nth cl (j-1) in
621 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
622 UriManager.string_of_uri uri))
624 and recursive_args context n nn te =
625 let module C = Cic in
626 match CicReduction.whd context te with
632 | C.Cast _ (*CSC ??? *) ->
633 raise (AssertFailure "3") (* due to type-checking *)
634 | C.Prod (name,so,de) ->
635 (not (does_not_occur context n nn so)) ::
636 (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
639 raise (AssertFailure "4") (* due to type-checking *)
641 | C.Const _ -> raise (AssertFailure "5")
646 | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *)
648 and get_new_safes ?(subst = []) context p c rl safes n nn x =
649 let module C = Cic in
650 let module U = UriManager in
651 let module R = CicReduction in
652 match (R.whd ~subst context c, R.whd ~subst context p, rl) with
653 (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
654 (* we are sure that the two sources are convertible because we *)
655 (* have just checked this. So let's go along ... *)
657 List.map (fun x -> x + 1) safes
660 if b then 1::safes' else safes'
662 get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
663 ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
664 | (C.Prod _, (C.MutConstruct _ as e), _)
665 | (C.Prod _, (C.Rel _ as e), _)
666 | (C.MutInd _, e, [])
667 | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
669 (* CSC: If the next exception is raised, it just means that *)
670 (* CSC: the proof-assistant allows to use very strange things *)
671 (* CSC: as a branch of a case whose type is a Prod. In *)
672 (* CSC: particular, this means that a new (C.Prod, x,_) case *)
673 (* CSC: must be considered in this match. (e.g. x = MutCase) *)
676 (Printf.sprintf "Get New Safes: c=%s ; p=%s"
677 (CicPp.ppterm c) (CicPp.ppterm p)))
679 and split_prods ?(subst = []) context n te =
680 let module C = Cic in
681 let module R = CicReduction in
682 match (n, R.whd context te) with
684 | (n, C.Prod (name,so,ta)) when n > 0 ->
685 split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
686 | (_, _) -> raise (AssertFailure "8")
688 and eat_lambdas ?(subst = []) context n te =
689 let module C = Cic in
690 let module R = CicReduction in
691 match (n, R.whd ~subst context te) with
692 (0, _) -> (te, 0, context)
693 | (n, C.Lambda (name,so,ta)) when n > 0 ->
694 let (te, k, context') =
695 eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
697 (te, k + 1, context')
699 raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
701 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
702 and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
703 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
704 (*CSC: cfr guarded_by_destructors *)
705 let module C = Cic in
706 let module U = UriManager in
707 match CicReduction.whd context te with
708 C.Rel m when List.mem m safes -> true
715 (* | C.Cast (te,ty) ->
716 check_is_really_smaller_arg ~subst n nn kl x safes te &&
717 check_is_really_smaller_arg ~subst n nn kl x safes ty*)
718 (* | C.Prod (_,so,ta) ->
719 check_is_really_smaller_arg ~subst n nn kl x safes so &&
720 check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
721 (List.map (fun x -> x + 1) safes) ta*)
722 | C.Prod _ -> raise (AssertFailure "10")
723 | C.Lambda (name,so,ta) ->
724 check_is_really_smaller_arg ~subst context n nn kl x safes so &&
725 check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
726 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
727 | C.LetIn (name,so,ta) ->
728 check_is_really_smaller_arg ~subst context n nn kl x safes so &&
729 check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context)
730 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
732 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
733 (*CSC: solo perche' non abbiamo trovato controesempi *)
734 check_is_really_smaller_arg ~subst context n nn kl x safes he
735 | C.Appl [] -> raise (AssertFailure "11")
737 | C.MutInd _ -> raise (AssertFailure "12")
738 | C.MutConstruct _ -> false
739 | C.MutCase (uri,i,outtype,term,pl) ->
741 C.Rel m when List.mem m safes || m = x ->
742 let (tys,len,isinductive,paramsno,cl) =
743 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
745 C.InductiveDefinition (tl,_,paramsno,_) ->
748 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
750 let (_,isinductive,_,cl) = List.nth tl i in
754 (id, snd (split_prods ~subst tys paramsno ty))) cl
756 (tys,List.length tl,isinductive,paramsno,cl')
758 raise (TypeCheckerFailure
759 ("Unknown mutual inductive definition:" ^
760 UriManager.string_of_uri uri))
762 if not isinductive then
765 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
771 let debrujinedte = debrujin_constructor uri len c in
772 recursive_args tys 0 len debrujinedte
774 let (e,safes',n',nn',x',context') =
775 get_new_safes ~subst context p c rl' safes n nn x
778 check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
779 ) (List.combine pl cl) true
780 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
781 let (tys,len,isinductive,paramsno,cl) =
782 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
784 C.InductiveDefinition (tl,_,paramsno,_) ->
785 let (_,isinductive,_,cl) = List.nth tl i in
787 List.map (fun (n,_,ty,_) ->
788 Some(Cic.Name n,(Cic.Decl ty))) tl
793 (id, snd (split_prods ~subst tys paramsno ty))) cl
795 (tys,List.length tl,isinductive,paramsno,cl')
797 raise (TypeCheckerFailure
798 ("Unknown mutual inductive definition:" ^
799 UriManager.string_of_uri uri))
801 if not isinductive then
804 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
807 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
808 (*CSC: sugli argomenti di una applicazione *)
812 let debrujinedte = debrujin_constructor uri len c in
813 recursive_args tys 0 len debrujinedte
815 let (e, safes',n',nn',x',context') =
816 get_new_safes context p c rl' safes n nn x
819 check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
820 ) (List.combine pl cl) true
824 i && check_is_really_smaller_arg ~subst context n nn kl x safes p
828 let len = List.length fl in
829 let n_plus_len = n + len
830 and nn_plus_len = nn + len
831 and x_plus_len = x + len
832 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
833 and safes' = List.map (fun x -> x + len) safes in
835 (fun (_,_,ty,bo) i ->
837 check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
841 let len = List.length fl in
842 let n_plus_len = n + len
843 and nn_plus_len = nn + len
844 and x_plus_len = x + len
845 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
846 and safes' = List.map (fun x -> x + len) safes in
850 check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
854 and guarded_by_destructors ?(subst = []) context n nn kl x safes =
855 let module C = Cic in
856 let module U = UriManager in
858 C.Rel m when m > n && m <= nn -> false
860 (match List.nth context (n-1) with
861 Some (_,C.Decl _) -> true
862 | Some (_,C.Def (bo,_)) ->
863 guarded_by_destructors context m nn kl x safes
864 (CicSubstitution.lift m bo)
865 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
869 | C.Implicit _ -> true
871 guarded_by_destructors context n nn kl x safes te &&
872 guarded_by_destructors context n nn kl x safes ty
873 | C.Prod (name,so,ta) ->
874 guarded_by_destructors context n nn kl x safes so &&
875 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
876 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
877 | C.Lambda (name,so,ta) ->
878 guarded_by_destructors context n nn kl x safes so &&
879 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
880 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
881 | C.LetIn (name,so,ta) ->
882 guarded_by_destructors context n nn kl x safes so &&
883 guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
884 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
885 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
886 let k = List.nth kl (m - n - 1) in
887 if not (List.length tl > k) then false
891 i && guarded_by_destructors context n nn kl x safes param
893 check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
896 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
898 | C.Var (_,exp_named_subst)
899 | C.Const (_,exp_named_subst)
900 | C.MutInd (_,_,exp_named_subst)
901 | C.MutConstruct (_,_,_,exp_named_subst) ->
903 (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
905 | C.MutCase (uri,i,outtype,term,pl) ->
907 C.Rel m when List.mem m safes || m = x ->
908 let (tys,len,isinductive,paramsno,cl) =
909 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
911 C.InductiveDefinition (tl,_,paramsno,_) ->
912 let len = List.length tl in
913 let (_,isinductive,_,cl) = List.nth tl i in
915 List.map (fun (n,_,ty,_) ->
916 Some(Cic.Name n,(Cic.Decl ty))) tl
921 let debrujinedty = debrujin_constructor uri len ty in
922 (id, snd (split_prods ~subst tys paramsno ty),
923 snd (split_prods ~subst tys paramsno debrujinedty)
926 (tys,len,isinductive,paramsno,cl')
928 raise (TypeCheckerFailure
929 ("Unknown mutual inductive definition:" ^
930 UriManager.string_of_uri uri))
932 if not isinductive then
933 guarded_by_destructors context n nn kl x safes outtype &&
934 guarded_by_destructors context n nn kl x safes term &&
935 (*CSC: manca ??? il controllo sul tipo di term? *)
938 i && guarded_by_destructors context n nn kl x safes p)
941 guarded_by_destructors context n nn kl x safes outtype &&
942 (*CSC: manca ??? il controllo sul tipo di term? *)
944 (fun (p,(_,c,brujinedc)) i ->
945 let rl' = recursive_args tys 0 len brujinedc in
946 let (e,safes',n',nn',x',context') =
947 get_new_safes context p c rl' safes n nn x
950 guarded_by_destructors context' n' nn' kl x' safes' e
951 ) (List.combine pl cl) true
952 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
953 let (tys,len,isinductive,paramsno,cl) =
954 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
956 C.InductiveDefinition (tl,_,paramsno,_) ->
957 let (_,isinductive,_,cl) = List.nth tl i in
960 (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
965 (id, snd (split_prods ~subst tys paramsno ty))) cl
967 (tys,List.length tl,isinductive,paramsno,cl')
969 raise (TypeCheckerFailure
970 ("Unknown mutual inductive definition:" ^
971 UriManager.string_of_uri uri))
973 if not isinductive then
974 guarded_by_destructors context n nn kl x safes outtype &&
975 guarded_by_destructors context n nn kl x safes term &&
976 (*CSC: manca ??? il controllo sul tipo di term? *)
979 i && guarded_by_destructors context n nn kl x safes p)
982 guarded_by_destructors context n nn kl x safes outtype &&
983 (*CSC: manca ??? il controllo sul tipo di term? *)
986 i && guarded_by_destructors context n nn kl x safes t)
991 let debrujinedte = debrujin_constructor uri len c in
992 recursive_args tys 0 len debrujinedte
994 let (e, safes',n',nn',x',context') =
995 get_new_safes context p c rl' safes n nn x
998 guarded_by_destructors context' n' nn' kl x' safes' e
999 ) (List.combine pl cl) true
1001 guarded_by_destructors context n nn kl x safes outtype &&
1002 guarded_by_destructors context n nn kl x safes term &&
1003 (*CSC: manca ??? il controllo sul tipo di term? *)
1005 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
1009 let len = List.length fl in
1010 let n_plus_len = n + len
1011 and nn_plus_len = nn + len
1012 and x_plus_len = x + len
1013 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1014 and safes' = List.map (fun x -> x + len) safes in
1016 (fun (_,_,ty,bo) i ->
1017 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1018 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1019 x_plus_len safes' bo
1021 | C.CoFix (_, fl) ->
1022 let len = List.length fl in
1023 let n_plus_len = n + len
1024 and nn_plus_len = nn + len
1025 and x_plus_len = x + len
1026 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1027 and safes' = List.map (fun x -> x + len) safes in
1031 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1032 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1033 x_plus_len safes' bo
1036 (* the boolean h means already protected *)
1037 (* args is the list of arguments the type of the constructor that may be *)
1038 (* found in head position must be applied to. *)
1039 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
1040 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
1041 let module C = Cic in
1042 (*CSC: There is a lot of code replication between the cases X and *)
1043 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
1044 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
1045 match CicReduction.whd context te with
1046 C.Rel m when m > n && m <= nn -> h
1054 (* the term has just been type-checked *)
1055 raise (AssertFailure "17")
1056 | C.Lambda (name,so,de) ->
1057 does_not_occur context n nn so &&
1058 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
1059 (n + 1) (nn + 1) h de args coInductiveTypeURI
1060 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
1062 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
1063 | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
1067 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1068 with Not_found -> assert false
1071 C.InductiveDefinition (itl,_,_,_) ->
1072 let (_,_,_,cl) = List.nth itl i in
1073 let (_,cons) = List.nth cl (j - 1) in
1074 CicSubstitution.subst_vars exp_named_subst cons
1076 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1077 UriManager.string_of_uri uri))
1079 let rec analyse_branch context ty te =
1080 match CicReduction.whd context ty with
1081 C.Meta _ -> raise (AssertFailure "34")
1085 does_not_occur context n nn te
1088 raise (AssertFailure "24")(* due to type-checking *)
1089 | C.Prod (name,so,de) ->
1090 analyse_branch ((Some (name,(C.Decl so)))::context) de te
1093 raise (AssertFailure "25")(* due to type-checking *)
1094 | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1095 when uri == coInductiveTypeURI ->
1096 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1097 | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1098 guarded_by_constructors context n nn true te tl coInductiveTypeURI
1100 does_not_occur context n nn te
1101 | C.Const _ -> raise (AssertFailure "26")
1102 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1103 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1105 does_not_occur context n nn te
1106 | C.MutConstruct _ -> raise (AssertFailure "27")
1107 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1108 (*CSC: in head position. *)
1112 raise (AssertFailure "28")(* due to type-checking *)
1114 let rec analyse_instantiated_type context ty l =
1115 match CicReduction.whd context ty with
1121 | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1122 | C.Prod (name,so,de) ->
1127 analyse_branch context so he &&
1128 analyse_instantiated_type
1129 ((Some (name,(C.Decl so)))::context) de tl
1133 raise (AssertFailure "30")(* due to type-checking *)
1136 (fun i x -> i && does_not_occur context n nn x) true l
1137 | C.Const _ -> raise (AssertFailure "31")
1140 (fun i x -> i && does_not_occur context n nn x) true l
1141 | C.MutConstruct _ -> raise (AssertFailure "32")
1142 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1143 (*CSC: in head position. *)
1147 raise (AssertFailure "33")(* due to type-checking *)
1149 let rec instantiate_type args consty =
1152 | tlhe::tltl as l ->
1153 let consty' = CicReduction.whd context consty in
1159 let instantiated_de = CicSubstitution.subst he de in
1160 (*CSC: siamo sicuri che non sia troppo forte? *)
1161 does_not_occur context n nn tlhe &
1162 instantiate_type tl instantiated_de tltl
1164 (*CSC:We do not consider backbones with a MutCase, a *)
1165 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1166 raise (AssertFailure "23")
1168 | [] -> analyse_instantiated_type context consty' l
1169 (* These are all the other cases *)
1171 instantiate_type args consty tl
1172 | C.Appl ((C.CoFix (_,fl))::tl) ->
1173 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1174 let len = List.length fl in
1175 let n_plus_len = n + len
1176 and nn_plus_len = nn + len
1177 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1178 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1181 i && does_not_occur context n nn ty &&
1182 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1183 args coInductiveTypeURI
1185 | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1186 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1187 does_not_occur context n nn out &&
1188 does_not_occur context n nn te &&
1192 guarded_by_constructors context n nn h x args coInductiveTypeURI
1195 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1196 | C.Var (_,exp_named_subst)
1197 | C.Const (_,exp_named_subst) ->
1199 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1200 | C.MutInd _ -> assert false
1201 | C.MutConstruct (_,_,_,exp_named_subst) ->
1203 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1204 | C.MutCase (_,_,out,te,pl) ->
1205 does_not_occur context n nn out &&
1206 does_not_occur context n nn te &&
1210 guarded_by_constructors context n nn h x args coInductiveTypeURI
1213 let len = List.length fl in
1214 let n_plus_len = n + len
1215 and nn_plus_len = nn + len
1216 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1217 and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1219 (fun (_,_,ty,bo) i ->
1220 i && does_not_occur context n nn ty &&
1221 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1224 let len = List.length fl in
1225 let n_plus_len = n + len
1226 and nn_plus_len = nn + len
1227 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1228 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1231 i && does_not_occur context n nn ty &&
1232 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1233 args coInductiveTypeURI
1236 and check_allowed_sort_elimination ~logger context uri i need_dummy ind
1237 arity1 arity2 ugraph =
1238 let module C = Cic in
1239 let module U = UriManager in
1240 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1241 (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
1242 let b,ugraph1 = CicReduction.are_convertible context so1 so2 ugraph in
1244 check_allowed_sort_elimination ~logger context uri i need_dummy
1245 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1
1248 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
1249 | (C.Sort C.Prop, C.Sort C.Set)
1250 | (C.Sort C.Prop, C.Sort C.CProp)
1251 | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1252 (* TASSI: da verificare *)
1253 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1254 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1256 C.InductiveDefinition (itl,_,_,_) ->
1257 let (_,_,_,cl) = List.nth itl i in
1258 (* is a singleton definition or the empty proposition? *)
1259 (List.length cl = 1 || List.length cl = 0) , ugraph
1261 raise (TypeCheckerFailure
1262 ("Unknown mutual inductive definition:" ^
1263 UriManager.string_of_uri uri))
1265 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
1266 | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
1267 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
1268 | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph
1269 | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
1270 | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
1271 | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
1272 (* TASSI: da verificare *)
1274 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1276 C.InductiveDefinition (itl,_,paramsno,_) ->
1278 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1280 let (_,_,_,cl) = List.nth itl i in
1282 (fun (_,x) (i,ugraph) ->
1284 is_small ~logger tys paramsno x ugraph
1289 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1290 UriManager.string_of_uri uri))
1292 | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
1293 (* TASSI: da verificare *)
1294 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1295 let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1299 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1300 C.Sort C.Prop -> true,ugraph1
1301 | (C.Sort C.Set | C.Sort C.CProp) ->
1302 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1304 C.InductiveDefinition (itl,_,_,_) ->
1305 let (_,_,_,cl) = List.nth itl i in
1306 (* is a singleton definition? *)
1307 List.length cl = 1,ugraph1
1309 raise (TypeCheckerFailure
1310 ("Unknown mutual inductive definition:" ^
1311 UriManager.string_of_uri uri))
1313 | _ -> false,ugraph1
1315 | ((C.Sort C.Set, C.Prod (name,so,ta))
1316 | (C.Sort C.CProp, C.Prod (name,so,ta)))
1317 when not need_dummy ->
1318 let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1322 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1324 | C.Sort C.Set -> true,ugraph1
1325 | C.Sort C.CProp -> true,ugraph1
1326 | C.Sort (C.Type _) ->
1327 (* TASSI: da verificare *)
1328 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1330 C.InductiveDefinition (itl,_,paramsno,_) ->
1331 let (_,_,_,cl) = List.nth itl i in
1334 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1337 (fun (_,x) (i,ugraph) ->
1339 is_small ~logger tys paramsno x ugraph
1342 ) cl (true,ugraph1))
1344 raise (TypeCheckerFailure
1345 ("Unknown mutual inductive definition:" ^
1346 UriManager.string_of_uri uri))
1348 | _ -> raise (AssertFailure "19")
1350 | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
1351 (* TASSI: da verificare *)
1352 CicReduction.are_convertible context so ind ugraph
1353 | (_,_) -> false,ugraph
1355 and type_of_branch context argsno need_dummy outtype term constype =
1356 let module C = Cic in
1357 let module R = CicReduction in
1358 match R.whd context constype with
1363 C.Appl [outtype ; term]
1364 | C.Appl (C.MutInd (_,_,_)::tl) ->
1365 let (_,arguments) = split tl argsno
1367 if need_dummy && arguments = [] then
1370 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1371 | C.Prod (name,so,de) ->
1373 match CicSubstitution.lift 1 term with
1374 C.Appl l -> C.Appl (l@[C.Rel 1])
1375 | t -> C.Appl [t ; C.Rel 1]
1377 C.Prod (C.Anonymous,so,type_of_branch
1378 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1379 (CicSubstitution.lift 1 outtype) term' de)
1380 | _ -> raise (AssertFailure "20")
1382 (* check_metasenv_consistency checks that the "canonical" context of a
1383 metavariable is consitent - up to relocation via the relocation list l -
1384 with the actual context *)
1387 and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
1388 canonical_context l ugraph
1390 let module C = Cic in
1391 let module R = CicReduction in
1392 let module S = CicSubstitution in
1393 let lifted_canonical_context =
1397 | (Some (n,C.Decl t))::tl ->
1398 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1399 | (Some (n,C.Def (t,None)))::tl ->
1400 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1401 | None::tl -> None::(aux (i+1) tl)
1402 | (Some (n,C.Def (t,Some ty)))::tl ->
1403 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
1405 aux 1 canonical_context
1411 | Some t,Some (_,C.Def (ct,_)) ->
1413 R.are_convertible ~subst ~metasenv context t ct ugraph
1418 (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))
1421 | Some t,Some (_,C.Decl ct) ->
1422 let type_t,ugraph1 =
1423 type_of_aux' ~logger ~subst metasenv context t ugraph
1426 R.are_convertible ~subst ~metasenv context type_t ct ugraph1
1429 raise (TypeCheckerFailure
1430 (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1431 (CicPp.ppterm ct) (CicPp.ppterm t)
1432 (CicPp.ppterm type_t)))
1436 raise (TypeCheckerFailure
1437 ("Not well typed metavariable local context: "^
1438 "an hypothesis, that is not hidden, is not instantiated"))
1439 ) ugraph l lifted_canonical_context
1443 type_of_aux' is just another name (with a different scope)
1447 and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
1448 let rec type_of_aux ~logger context t ugraph =
1449 let module C = Cic in
1450 let module R = CicReduction in
1451 let module S = CicSubstitution in
1452 let module U = UriManager in
1456 match List.nth context (n - 1) with
1457 Some (_,C.Decl t) -> S.lift n t,ugraph
1458 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
1459 | Some (_,C.Def (bo,None)) ->
1460 debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1461 type_of_aux ~logger context (S.lift n bo) ugraph
1463 (TypeCheckerFailure "Reference to deleted hypothesis")
1466 raise (TypeCheckerFailure "unbound variable")
1468 | C.Var (uri,exp_named_subst) ->
1471 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1473 let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
1474 let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
1479 let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
1481 check_metasenv_consistency ~logger
1482 ~subst metasenv context canonical_context l ugraph
1484 (* assuming subst is well typed !!!!! *)
1485 ((CicSubstitution.lift_meta l ty), ugraph1)
1486 (* type_of_aux context (CicSubstitution.lift_meta l term) *)
1487 with CicUtil.Subst_not_found _ ->
1488 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1490 check_metasenv_consistency ~logger
1491 ~subst metasenv context canonical_context l ugraph
1493 ((CicSubstitution.lift_meta l ty),ugraph1))
1494 (* TASSI: CONSTRAINTS *)
1495 | C.Sort (C.Type t) ->
1496 let t' = CicUniv.fresh() in
1497 let ugraph1 = CicUniv.add_gt t' t ugraph in
1498 (C.Sort (C.Type t')),ugraph1
1499 (* TASSI: CONSTRAINTS *)
1500 | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
1501 | C.Implicit _ -> raise (AssertFailure "21")
1502 | C.Cast (te,ty) as t ->
1503 let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1504 let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
1506 R.are_convertible ~subst ~metasenv context ty_te ty ugraph2
1511 raise (TypeCheckerFailure
1512 (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1513 | C.Prod (name,s,t) ->
1514 let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1516 type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t ugraph1
1518 sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2
1519 | C.Lambda (n,s,t) ->
1520 let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1521 (match R.whd ~subst context sort1 with
1526 (TypeCheckerFailure (sprintf
1527 "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
1528 (CicPp.ppterm sort1)))
1531 type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
1533 (C.Prod (n,s,type2)),ugraph2
1534 | C.LetIn (n,s,t) ->
1535 (* only to check if s is well-typed *)
1536 let ty,ugraph1 = type_of_aux ~logger context s ugraph in
1537 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1538 LetIn is later reduced and maybe also re-checked.
1539 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1541 (* The type of the LetIn is reduced. Much faster than the previous
1542 solution. Moreover the inferred type is probably very different
1543 from the expected one.
1544 (CicReduction.whd context
1545 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1547 (* One-step LetIn reduction. Even faster than the previous solution.
1548 Moreover the inferred type is closer to the expected one. *)
1551 ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
1553 (CicSubstitution.subst s ty1),ugraph2
1554 | C.Appl (he::tl) when List.length tl > 0 ->
1555 let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
1556 let tlbody_and_type,ugraph2 =
1559 let ty,ugraph1 = type_of_aux ~logger context x ugraph in
1560 let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
1561 ((x,ty)::l,ugraph1))
1564 (* TASSI: questa c'era nel mio... ma non nel CVS... *)
1565 (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
1566 eat_prods ~subst context hetype tlbody_and_type ugraph2
1567 | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1568 | C.Const (uri,exp_named_subst) ->
1571 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1573 let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
1575 CicSubstitution.subst_vars exp_named_subst cty
1579 | C.MutInd (uri,i,exp_named_subst) ->
1582 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1584 (* TASSI: da me c'era anche questa, ma in CVS no *)
1585 let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
1586 (* fine parte dubbia *)
1588 CicSubstitution.subst_vars exp_named_subst mty
1592 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1594 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1596 (* TASSI: idem come sopra *)
1598 type_of_mutual_inductive_constr ~logger uri i j ugraph1
1601 CicSubstitution.subst_vars exp_named_subst mty
1604 | C.MutCase (uri,i,outtype,term,pl) ->
1605 let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
1606 let (need_dummy, k) =
1607 let rec guess_args context t =
1608 let outtype = CicReduction.whd ~subst context t in
1610 C.Sort _ -> (true, 0)
1611 | C.Prod (name, s, t) ->
1613 guess_args ((Some (name,(C.Decl s)))::context) t in
1615 (* last prod before sort *)
1616 match CicReduction.whd ~subst context s with
1617 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1618 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1620 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1621 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1622 when U.eq uri' uri && i' = i -> (false, 1)
1630 "Malformed case analasys' output type %s"
1631 (CicPp.ppterm outtype)))
1634 let (parameters, arguments, exp_named_subst),ugraph2 =
1635 let ty,ugraph2 = type_of_aux context term ugraph1 in
1636 match R.whd context ty with
1637 (*CSC manca il caso dei CAST *)
1638 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1639 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
1640 (*CSC: Hint: nella DTD servono per gli stylesheet. *)
1641 C.MutInd (uri',i',exp_named_subst) as typ ->
1642 if U.eq uri uri' && i = i' then
1643 ([],[],exp_named_subst),ugraph2
1648 ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1649 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1651 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1652 if U.eq uri uri' && i = i' then
1654 split tl (List.length tl - k)
1655 in (params,args,exp_named_subst),ugraph2
1660 ("Case analysys: analysed term type is %s, "^
1661 "but is expected to be (an application of) "^
1663 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1669 "analysed term %s is not an inductive one")
1670 (CicPp.ppterm term)))
1672 let (b, k) = guess_args context outsort in
1673 if not b then (b, k - 1) else (b, k) in
1674 let (parameters, arguments, exp_named_subst),ugraph2 =
1675 let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
1676 match R.whd ~subst context ty with
1677 C.MutInd (uri',i',exp_named_subst) as typ ->
1678 if U.eq uri uri' && i = i' then
1679 ([],[],exp_named_subst),ugraph2
1683 ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1684 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1686 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1687 if U.eq uri uri' && i = i' then
1689 split tl (List.length tl - k)
1690 in (params,args,exp_named_subst),ugraph2
1694 "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1695 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1700 "Case analysis: analysed term %s is not an inductive one"
1701 (CicPp.ppterm term)))
1704 let's control if the sort elimination is allowed:
1707 let sort_of_ind_type =
1708 if parameters = [] then
1709 C.MutInd (uri,i,exp_named_subst)
1711 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1713 let type_of_sort_of_ind_ty,ugraph3 =
1714 type_of_aux ~logger context sort_of_ind_type ugraph2 in
1716 check_allowed_sort_elimination ~logger context uri i need_dummy
1717 sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
1721 (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1722 (* let's check if the type of branches are right *)
1726 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1727 with Not_found -> assert false
1730 C.InductiveDefinition (_,_,parsno,_) -> parsno
1732 raise (TypeCheckerFailure
1733 ("Unknown mutual inductive definition:" ^
1734 UriManager.string_of_uri uri))
1736 let (_,branches_ok,ugraph5) =
1738 (fun (j,b,ugraph) p ->
1741 if parameters = [] then
1742 (C.MutConstruct (uri,i,j,exp_named_subst))
1745 (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1747 let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
1748 let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
1751 type_of_branch context parsno need_dummy outtype cons
1755 ~subst ~metasenv context ty_p ty_branch ugraph3
1759 ("#### " ^ CicPp.ppterm ty_p ^
1760 " <==> " ^ CicPp.ppterm ty_branch);
1764 ) (1,true,ugraph4) pl
1766 if not branches_ok then
1768 (TypeCheckerFailure "Case analysys: wrong branch type");
1769 if not need_dummy then
1770 (C.Appl ((outtype::arguments)@[term])),ugraph5
1771 else if arguments = [] then
1774 (C.Appl (outtype::arguments)),ugraph5
1776 let types_times_kl,ugraph1 =
1777 (* WAS: list rev list map *)
1779 (fun (l,ugraph) (n,k,ty,_) ->
1780 let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1781 ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
1784 let (types,kl) = List.split types_times_kl in
1785 let len = List.length types in
1788 (fun ugraph (name,x,ty,bo) ->
1790 type_of_aux ~logger (types@context) bo ugraph
1793 R.are_convertible ~subst ~metasenv (types@context)
1794 ty_bo (CicSubstitution.lift len ty) ugraph1 in
1797 let (m, eaten, context') =
1798 eat_lambdas ~subst (types @ context) (x + 1) bo
1801 let's control the guarded by
1802 destructors conditions D{f,k,x,M}
1804 if not (guarded_by_destructors context' eaten
1805 (len + eaten) kl 1 [] m) then
1808 ("Fix: not guarded by destructors"))
1813 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1815 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1816 let (_,_,ty,_) = List.nth fl i in
1821 (fun (l,ugraph) (n,ty,_) ->
1823 type_of_aux ~logger context ty ugraph in
1824 (Some (C.Name n,(C.Decl ty))::l,ugraph1)
1827 let len = List.length types in
1830 (fun ugraph (_,ty,bo) ->
1832 type_of_aux ~logger (types @ context) bo ugraph
1835 R.are_convertible ~subst ~metasenv (types @ context) ty_bo
1836 (CicSubstitution.lift len ty) ugraph1
1840 (* let's control that the returned type is coinductive *)
1841 match returns_a_coinductive context ty with
1845 ("CoFix: does not return a coinductive type"))
1848 let's control the guarded by constructors
1851 if not (guarded_by_constructors (types @ context)
1852 0 len false bo [] uri) then
1855 ("CoFix: not guarded by constructors"))
1861 (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1864 let (_,ty,_) = List.nth fl i in
1867 and check_exp_named_subst ~logger ?(subst = []) context ugraph =
1868 let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
1871 | ((uri,t) as item)::tl ->
1872 let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in
1874 CicSubstitution.subst_vars esubsts ty_uri in
1875 let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in
1877 CicReduction.are_convertible ~subst ~metasenv
1878 context typeoft typeofvar ugraph2
1881 check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3
1884 CicReduction.fdebug := 0 ;
1886 (CicReduction.are_convertible
1887 ~subst ~metasenv context typeoft typeofvar ugraph2) ;
1889 debug typeoft [typeofvar] ;
1890 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1893 check_exp_named_subst_aux ~logger [] ugraph
1895 and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph =
1896 let module C = Cic in
1897 let t1' = CicReduction.whd ~subst context t1 in
1898 let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1899 match (t1', t2') with
1900 (C.Sort s1, C.Sort s2)
1901 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1902 (* different from Coq manual!!! *)
1904 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1905 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1906 let t' = CicUniv.fresh() in
1907 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1908 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1909 C.Sort (C.Type t'),ugraph2
1910 | (C.Sort _,C.Sort (C.Type t1)) ->
1911 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1912 C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
1913 | (C.Meta _, C.Sort _) -> t2',ugraph
1914 | (C.Meta _, (C.Meta (_,_) as t))
1915 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1917 | (_,_) -> raise (TypeCheckerFailure (sprintf
1918 "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1919 (CicPp.ppterm t2')))
1921 and eat_prods ?(subst = []) context hetype l ugraph =
1922 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1926 | (hete, hety)::tl ->
1927 (match (CicReduction.whd ~subst context hetype) with
1930 CicReduction.are_convertible
1931 ~subst ~metasenv context hety s ugraph
1935 CicReduction.fdebug := -1 ;
1936 eat_prods ~subst context
1937 (CicSubstitution.subst hete t) tl ugraph1
1938 (*TASSI: not sure *)
1942 CicReduction.fdebug := 0 ;
1943 ignore (CicReduction.are_convertible
1944 ~subst ~metasenv context s hety ugraph) ;
1950 ("Appl: wrong parameter-type, expected %s, found %s")
1951 (CicPp.ppterm hetype) (CicPp.ppterm s)))
1954 raise (TypeCheckerFailure
1955 "Appl: this is not a function, it cannot be applied")
1958 and returns_a_coinductive context ty =
1959 let module C = Cic in
1960 match CicReduction.whd context ty with
1961 C.MutInd (uri,i,_) ->
1962 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1965 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1966 with Not_found -> assert false
1969 C.InductiveDefinition (itl,_,_,_) ->
1970 let (_,is_inductive,_,_) = List.nth itl i in
1971 if is_inductive then None else (Some uri)
1973 raise (TypeCheckerFailure
1974 ("Unknown mutual inductive definition:" ^
1975 UriManager.string_of_uri uri))
1977 | C.Appl ((C.MutInd (uri,i,_))::_) ->
1978 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1980 C.InductiveDefinition (itl,_,_,_) ->
1981 let (_,is_inductive,_,_) = List.nth itl i in
1982 if is_inductive then None else (Some uri)
1984 raise (TypeCheckerFailure
1985 ("Unknown mutual inductive definition:" ^
1986 UriManager.string_of_uri uri))
1988 | C.Prod (n,so,de) ->
1989 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1994 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1997 type_of_aux ~logger context t ugraph
1999 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
2002 (* is a small constructor? *)
2003 (*CSC: ottimizzare calcolando staticamente *)
2004 and is_small ~logger context paramsno c ugraph =
2005 let rec is_small_aux ~logger context c ugraph =
2006 let module C = Cic in
2007 match CicReduction.whd context c with
2009 (*CSC: [] is an empty metasenv. Is it correct? *)
2010 let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
2011 let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
2013 is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
2016 | _ -> true,ugraph (*CSC: we trust the type-checker *)
2018 let (context',dx) = split_prods context paramsno c in
2019 is_small_aux ~logger context' dx ugraph
2021 and type_of ~logger t ugraph =
2023 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
2026 type_of_aux' ~logger [] [] t ugraph
2028 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
2032 let typecheck uri ugraph =
2033 let module C = Cic in
2034 let module R = CicReduction in
2035 let module U = UriManager in
2036 let logger = new CicLogger.logger in
2037 (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
2038 match CicEnvironment.is_type_checked ~trust:false ugraph uri with
2039 CicEnvironment.CheckedObj (cobj,ugraph') ->
2040 (* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
2042 | CicEnvironment.UncheckedObj uobj ->
2043 (* let's typecheck the uncooked object *)
2044 logger#log (`Start_type_checking uri) ;
2045 (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
2048 C.Constant (_,Some te,ty,_,_) ->
2049 let _,ugraph1 = type_of ~logger ty ugraph in
2050 let ty_te,ugraph2 = type_of ~logger te ugraph1 in
2051 let b,ugraph3 = (R.are_convertible [] ty_te ty ugraph2) in
2053 raise (TypeCheckerFailure
2054 ("Unknown constant:" ^ U.string_of_uri uri))
2057 | C.Constant (_,None,ty,_,_) ->
2058 (* only to check that ty is well-typed *)
2059 let _,ugraph1 = type_of ~logger ty ugraph in
2061 | C.CurrentProof (_,conjs,te,ty,_,_) ->
2064 (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
2066 type_of_aux' ~logger metasenv context ty ugraph
2068 metasenv @ [conj],ugraph1
2071 let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
2072 let type_of_te,ugraph3 =
2073 type_of_aux' ~logger conjs [] te ugraph2
2075 let b,ugraph4 = R.are_convertible [] type_of_te ty ugraph3 in
2077 raise (TypeCheckerFailure (sprintf
2078 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
2079 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
2083 | C.Variable (_,bo,ty,_,_) ->
2084 (* only to check that ty is well-typed *)
2085 let _,ugraph1 = type_of ~logger ty ugraph in
2089 let ty_bo,ugraph2 = type_of ~logger bo ugraph1 in
2090 let b,ugraph3 = R.are_convertible [] ty_bo ty ugraph2 in
2092 raise (TypeCheckerFailure
2093 ("Unknown variable:" ^ U.string_of_uri uri))
2097 | C.InductiveDefinition _ ->
2098 check_mutual_inductive_defs ~logger uri uobj ugraph
2101 CicEnvironment.set_type_checking_info uri;
2102 logger#log (`Type_checking_completed uri);
2103 match CicEnvironment.is_type_checked ~trust:false ugraph uri with
2104 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
2105 | _ -> raise CicEnvironmentError
2108 this is raised if set_type_checking_info is called on an object
2109 that has no associated universe file. If we are in univ_maker
2110 phase this is OK since univ_maker will properly commit the
2113 Invalid_argument s ->
2114 (*prerr_endline s;*)
2118 (** wrappers which instantiate fresh loggers *)
2120 let type_of_aux' ?(subst = []) metasenv context t =
2121 let logger = new CicLogger.logger in
2122 type_of_aux' ~logger ~subst metasenv context t
2124 let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) =
2125 let logger = new CicLogger.logger in
2126 typecheck_mutual_inductive_defs ~logger uri (itl, uris, indparamsno)