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;;
34 let profiler_clean_fill =
35 (CicUtil.profile "add_obj.typecheck_obj.clean_and_fill").CicUtil.profile
39 let rec debug_aux t i =
41 let module U = UriManager in
42 CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
45 raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
48 let debug_print = fun _ -> () ;;
53 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
55 raise (TypeCheckerFailure "Parameters number < left parameters number")
58 let debrujin_constructor uri number_of_types =
62 C.Rel n as t when n <= k -> t
64 raise (TypeCheckerFailure "unbound variable found in constructor type")
65 | C.Var (uri,exp_named_subst) ->
66 let exp_named_subst' =
67 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
69 C.Var (uri,exp_named_subst')
71 let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
74 | C.Implicit _ as t -> t
75 | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
76 | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
77 | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
78 | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t)
79 | C.Appl l -> C.Appl (List.map (aux k) l)
80 | C.Const (uri,exp_named_subst) ->
81 let exp_named_subst' =
82 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
84 C.Const (uri,exp_named_subst')
85 | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
86 if exp_named_subst != [] then
87 raise (TypeCheckerFailure
88 ("non-empty explicit named substitution is applied to "^
89 "a mutual inductive type which is being defined")) ;
90 C.Rel (k + number_of_types - tyno) ;
91 | C.MutInd (uri',tyno,exp_named_subst) ->
92 let exp_named_subst' =
93 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
95 C.MutInd (uri',tyno,exp_named_subst')
96 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
97 let exp_named_subst' =
98 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
100 C.MutConstruct (uri,tyno,consno,exp_named_subst')
101 | C.MutCase (sp,i,outty,t,pl) ->
102 C.MutCase (sp, i, aux k outty, aux k t,
105 let len = List.length fl in
108 (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
113 let len = List.length fl in
116 (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
119 C.CoFix (i, liftedfl)
124 exception CicEnvironmentError;;
126 let rec type_of_constant ~logger uri ugraph =
127 let module C = Cic in
128 let module R = CicReduction in
129 let module U = UriManager in
131 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
132 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
133 | CicEnvironment.UncheckedObj uobj ->
134 logger#log (`Start_type_checking uri) ;
135 (* let's typecheck the uncooked obj *)
137 (****************************************************************
138 TASSI: FIXME qui e' inutile ricordarselo,
139 tanto poi lo richiediamo alla cache che da quello su disco
140 *****************************************************************)
144 C.Constant (_,Some te,ty,_,_) ->
145 let _,ugraph = type_of ~logger ty ugraph in
146 let type_of_te,ugraph' = type_of ~logger te ugraph in
147 let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in
149 raise (TypeCheckerFailure (sprintf
150 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
151 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
155 | C.Constant (_,None,ty,_,_) ->
156 (* only to check that ty is well-typed *)
157 let _,ugraph' = type_of ~logger ty ugraph in
159 | C.CurrentProof (_,conjs,te,ty,_,_) ->
162 (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
164 type_of_aux' ~logger metasenv context ty ugraph
166 (metasenv @ [conj],ugraph')
169 let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
170 let type_of_te,ugraph3 =
171 type_of_aux' ~logger conjs [] te ugraph2
173 let b,ugraph4 = (R.are_convertible [] type_of_te ty ugraph3) in
175 raise (TypeCheckerFailure (sprintf
176 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
177 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
182 raise (TypeCheckerFailure
183 ("Unknown constant:" ^ U.string_of_uri uri)))
186 CicEnvironment.set_type_checking_info uri;
187 logger#log (`Type_checking_completed uri) ;
188 match CicEnvironment.is_type_checked ~trust:false ugraph uri with
189 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
190 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
191 with Invalid_argument s ->
192 (*debug_print (lazy s);*)
195 match cobj,ugraph with
196 (C.Constant (_,_,ty,_,_)),g -> ty,g
197 | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g
199 raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
201 and type_of_variable ~logger uri ugraph =
202 let module C = Cic in
203 let module R = CicReduction in
204 let module U = UriManager in
205 (* 0 because a variable is never cooked => no partial cooking at one level *)
206 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
207 CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
208 | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
209 logger#log (`Start_type_checking uri) ;
210 (* only to check that ty is well-typed *)
211 let _,ugraph1 = type_of ~logger ty ugraph in
216 let ty_bo,ugraph' = type_of ~logger bo ugraph1 in
217 let b,ugraph'' = (R.are_convertible [] ty_bo ty ugraph') in
219 raise (TypeCheckerFailure
220 ("Unknown variable:" ^ U.string_of_uri uri))
225 CicEnvironment.set_type_checking_info uri ;
226 logger#log (`Type_checking_completed uri) ;
227 match CicEnvironment.is_type_checked ~trust:false ugraph uri with
228 CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') ->
230 | CicEnvironment.CheckedObj _
231 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
232 with Invalid_argument s ->
233 (*debug_print (lazy s);*)
236 raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
238 and does_not_occur context n nn te =
239 let module C = Cic in
240 (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
241 (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
243 match CicReduction.whd context te with
244 C.Rel m when m > n && m <= nn -> false
246 | C.Meta _ (* CSC: Are we sure? No recursion?*)
248 | C.Implicit _ -> true
250 does_not_occur context n nn te && does_not_occur context n nn ty
251 | C.Prod (name,so,dest) ->
252 does_not_occur context n nn so &&
253 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
255 | C.Lambda (name,so,dest) ->
256 does_not_occur context n nn so &&
257 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
259 | C.LetIn (name,so,dest) ->
260 does_not_occur context n nn so &&
261 does_not_occur ((Some (name,(C.Def (so,None))))::context)
262 (n + 1) (nn + 1) dest
264 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
265 | C.Var (_,exp_named_subst)
266 | C.Const (_,exp_named_subst)
267 | C.MutInd (_,_,exp_named_subst)
268 | C.MutConstruct (_,_,_,exp_named_subst) ->
269 List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
271 | C.MutCase (_,_,out,te,pl) ->
272 does_not_occur context n nn out && does_not_occur context n nn te &&
273 List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
275 let len = List.length fl in
276 let n_plus_len = n + len in
277 let nn_plus_len = nn + len in
279 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
282 (fun (_,_,ty,bo) i ->
283 i && does_not_occur context n nn ty &&
284 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
287 let len = List.length fl in
288 let n_plus_len = n + len in
289 let nn_plus_len = nn + len in
291 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
295 i && does_not_occur context n nn ty &&
296 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
299 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
300 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
301 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
302 (*CSC strictly_positive *)
303 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
304 and weakly_positive context n nn uri te =
305 let module C = Cic in
306 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
308 C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
310 (*CSC mettere in cicSubstitution *)
311 let rec subst_inductive_type_with_dummy_mutind =
313 C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
315 | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
317 | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
318 | C.Prod (name,so,ta) ->
319 C.Prod (name, subst_inductive_type_with_dummy_mutind so,
320 subst_inductive_type_with_dummy_mutind ta)
321 | C.Lambda (name,so,ta) ->
322 C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
323 subst_inductive_type_with_dummy_mutind ta)
325 C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
326 | C.MutCase (uri,i,outtype,term,pl) ->
328 subst_inductive_type_with_dummy_mutind outtype,
329 subst_inductive_type_with_dummy_mutind term,
330 List.map subst_inductive_type_with_dummy_mutind pl)
332 C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
333 subst_inductive_type_with_dummy_mutind ty,
334 subst_inductive_type_with_dummy_mutind bo)) fl)
336 C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
337 subst_inductive_type_with_dummy_mutind ty,
338 subst_inductive_type_with_dummy_mutind bo)) fl)
339 | C.Const (uri,exp_named_subst) ->
340 let exp_named_subst' =
342 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
345 C.Const (uri,exp_named_subst')
346 | C.MutInd (uri,typeno,exp_named_subst) ->
347 let exp_named_subst' =
349 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
352 C.MutInd (uri,typeno,exp_named_subst')
353 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
354 let exp_named_subst' =
356 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
359 C.MutConstruct (uri,typeno,consno,exp_named_subst')
362 match CicReduction.whd context te with
363 C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
364 | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
365 | C.Prod (C.Anonymous,source,dest) ->
366 strictly_positive context n nn
367 (subst_inductive_type_with_dummy_mutind source) &&
368 weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
369 (n + 1) (nn + 1) uri dest
370 | C.Prod (name,source,dest) when
371 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
372 (* dummy abstraction, so we behave as in the anonimous case *)
373 strictly_positive 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
377 | C.Prod (name,source,dest) ->
378 does_not_occur context n nn
379 (subst_inductive_type_with_dummy_mutind source)&&
380 weakly_positive ((Some (name,(C.Decl source)))::context)
381 (n + 1) (nn + 1) uri dest
383 raise (TypeCheckerFailure "Malformed inductive constructor type")
385 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
386 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
387 and instantiate_parameters params c =
388 let module C = Cic in
389 match (c,params) with
391 | (C.Prod (_,_,ta), he::tl) ->
392 instantiate_parameters tl
393 (CicSubstitution.subst he ta)
394 | (C.Cast (te,_), _) -> instantiate_parameters params te
395 | (t,l) -> raise (AssertFailure "1")
397 and strictly_positive context n nn te =
398 let module C = Cic in
399 let module U = UriManager in
400 match CicReduction.whd context te with
403 (*CSC: bisogna controllare ty????*)
404 strictly_positive context n nn te
405 | C.Prod (name,so,ta) ->
406 does_not_occur context n nn so &&
407 strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
408 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
409 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
410 | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
411 let (ok,paramsno,ity,cl,name) =
412 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
414 C.InductiveDefinition (tl,_,paramsno,_) ->
415 let (name,_,ity,cl) = List.nth tl i in
416 (List.length tl = 1, paramsno, ity, cl, name)
418 raise (TypeCheckerFailure
419 ("Unknown inductive type:" ^ U.string_of_uri uri))
421 let (params,arguments) = split tl paramsno in
422 let lifted_params = List.map (CicSubstitution.lift 1) params in
426 instantiate_parameters lifted_params
427 (CicSubstitution.subst_vars exp_named_subst te)
432 (fun x i -> i && does_not_occur context n nn x)
434 (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
439 ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
442 | t -> does_not_occur context n nn t
444 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
445 and are_all_occurrences_positive context uri indparamsno i n nn te =
446 let module C = Cic in
447 match CicReduction.whd context te with
448 C.Appl ((C.Rel m)::tl) when m = i ->
449 (*CSC: riscrivere fermandosi a 0 *)
450 (* let's check if the inductive type is applied at least to *)
451 (* indparamsno parameters *)
457 match CicReduction.whd context x with
458 C.Rel m when m = n - (indparamsno - k) -> k - 1
460 raise (TypeCheckerFailure
461 ("Non-positive occurence in mutual inductive definition(s) " ^
462 UriManager.string_of_uri uri))
466 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
468 raise (TypeCheckerFailure
469 ("Non-positive occurence in mutual inductive definition(s) " ^
470 UriManager.string_of_uri uri))
471 | C.Rel m when m = i ->
472 if indparamsno = 0 then
475 raise (TypeCheckerFailure
476 ("Non-positive occurence in mutual inductive definition(s) " ^
477 UriManager.string_of_uri uri))
478 | C.Prod (C.Anonymous,source,dest) ->
479 strictly_positive context n nn source &&
480 are_all_occurrences_positive
481 ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
482 (i+1) (n + 1) (nn + 1) dest
483 | C.Prod (name,source,dest) when
484 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
485 (* dummy abstraction, so we behave as in the anonimous case *)
486 strictly_positive context n nn source &&
487 are_all_occurrences_positive
488 ((Some (name,(C.Decl source)))::context) uri indparamsno
489 (i+1) (n + 1) (nn + 1) dest
490 | C.Prod (name,source,dest) ->
491 does_not_occur context n nn source &&
492 are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
493 uri indparamsno (i+1) (n + 1) (nn + 1) dest
496 (TypeCheckerFailure ("Malformed inductive constructor type " ^
497 (UriManager.string_of_uri uri)))
499 (* Main function to checks the correctness of a mutual *)
500 (* inductive block definition. This is the function *)
501 (* exported to the proof-engine. *)
502 and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
503 let module U = UriManager in
504 (* let's check if the arity of the inductive types are well *)
506 let ugrap1 = List.fold_left
507 (fun ugraph (_,_,x,_) -> let _,ugraph' =
508 type_of ~logger x ugraph in ugraph')
511 (* let's check if the types of the inductive constructors *)
512 (* are well formed. *)
513 (* In order not to use type_of_aux we put the types of the *)
514 (* mutual inductive types at the head of the types of the *)
515 (* constructors using Prods *)
516 let len = List.length itl in
518 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
521 (fun (_,_,_,cl) (i,ugraph) ->
524 (fun ugraph (name,te) ->
525 let debrujinedte = debrujin_constructor uri len te in
528 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
531 let _,ugraph' = type_of ~logger augmented_term ugraph in
532 (* let's check also the positivity conditions *)
535 (are_all_occurrences_positive tys uri indparamsno i 0 len
539 (TypeCheckerFailure ("Non positive occurence in " ^
540 U.string_of_uri uri))
549 (* Main function to checks the correctness of a mutual *)
550 (* inductive block definition. *)
551 and check_mutual_inductive_defs uri obj ugraph =
553 Cic.InductiveDefinition (itl, params, indparamsno, _) ->
554 typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph
556 raise (TypeCheckerFailure (
557 "Unknown mutual inductive definition:" ^
558 UriManager.string_of_uri uri))
560 and type_of_mutual_inductive_defs ~logger uri i ugraph =
561 let module C = Cic in
562 let module R = CicReduction in
563 let module U = UriManager in
565 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
566 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
567 | CicEnvironment.UncheckedObj uobj ->
568 logger#log (`Start_type_checking uri) ;
570 check_mutual_inductive_defs ~logger uri uobj ugraph
572 (* TASSI: FIXME: check ugraph1 == ugraph ritornato da env *)
574 CicEnvironment.set_type_checking_info uri ;
575 logger#log (`Type_checking_completed uri) ;
576 (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
577 CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
578 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
581 Invalid_argument s ->
582 (*debug_print (lazy s);*)
586 C.InductiveDefinition (dl,_,_,_) ->
587 let (_,_,arity,_) = List.nth dl i in
590 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
591 U.string_of_uri uri))
593 and type_of_mutual_inductive_constr ~logger uri i j ugraph =
594 let module C = Cic in
595 let module R = CicReduction in
596 let module U = UriManager in
598 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
599 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
600 | CicEnvironment.UncheckedObj uobj ->
601 logger#log (`Start_type_checking uri) ;
603 check_mutual_inductive_defs ~logger uri uobj ugraph
605 (* check ugraph1 validity ??? == ugraph' *)
607 CicEnvironment.set_type_checking_info uri ;
608 logger#log (`Type_checking_completed uri) ;
610 CicEnvironment.is_type_checked ~trust:false ugraph uri
612 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
613 | CicEnvironment.UncheckedObj _ ->
614 raise CicEnvironmentError)
616 Invalid_argument s ->
617 (*debug_print (lazy s);*)
621 C.InductiveDefinition (dl,_,_,_) ->
622 let (_,_,_,cl) = List.nth dl i in
623 let (_,ty) = List.nth cl (j-1) in
626 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
627 UriManager.string_of_uri uri))
629 and recursive_args context n nn te =
630 let module C = Cic in
631 match CicReduction.whd context te with
637 | C.Cast _ (*CSC ??? *) ->
638 raise (AssertFailure "3") (* due to type-checking *)
639 | C.Prod (name,so,de) ->
640 (not (does_not_occur context n nn so)) ::
641 (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
644 raise (AssertFailure "4") (* due to type-checking *)
646 | C.Const _ -> raise (AssertFailure "5")
651 | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *)
653 and get_new_safes ?(subst = []) context p c rl safes n nn x =
654 let module C = Cic in
655 let module U = UriManager in
656 let module R = CicReduction in
657 match (R.whd ~subst context c, R.whd ~subst context p, rl) with
658 (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
659 (* we are sure that the two sources are convertible because we *)
660 (* have just checked this. So let's go along ... *)
662 List.map (fun x -> x + 1) safes
665 if b then 1::safes' else safes'
667 get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
668 ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
669 | (C.Prod _, (C.MutConstruct _ as e), _)
670 | (C.Prod _, (C.Rel _ as e), _)
671 | (C.MutInd _, e, [])
672 | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
674 (* CSC: If the next exception is raised, it just means that *)
675 (* CSC: the proof-assistant allows to use very strange things *)
676 (* CSC: as a branch of a case whose type is a Prod. In *)
677 (* CSC: particular, this means that a new (C.Prod, x,_) case *)
678 (* CSC: must be considered in this match. (e.g. x = MutCase) *)
681 (Printf.sprintf "Get New Safes: c=%s ; p=%s"
682 (CicPp.ppterm c) (CicPp.ppterm p)))
684 and split_prods ?(subst = []) context n te =
685 let module C = Cic in
686 let module R = CicReduction in
687 match (n, R.whd context te) with
689 | (n, C.Prod (name,so,ta)) when n > 0 ->
690 split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
691 | (_, _) -> raise (AssertFailure "8")
693 and eat_lambdas ?(subst = []) context n te =
694 let module C = Cic in
695 let module R = CicReduction in
696 match (n, R.whd ~subst context te) with
697 (0, _) -> (te, 0, context)
698 | (n, C.Lambda (name,so,ta)) when n > 0 ->
699 let (te, k, context') =
700 eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
702 (te, k + 1, context')
704 raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
706 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
707 and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
708 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
709 (*CSC: cfr guarded_by_destructors *)
710 let module C = Cic in
711 let module U = UriManager in
712 match CicReduction.whd context te with
713 C.Rel m when List.mem m safes -> true
720 (* | C.Cast (te,ty) ->
721 check_is_really_smaller_arg ~subst n nn kl x safes te &&
722 check_is_really_smaller_arg ~subst n nn kl x safes ty*)
723 (* | C.Prod (_,so,ta) ->
724 check_is_really_smaller_arg ~subst n nn kl x safes so &&
725 check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
726 (List.map (fun x -> x + 1) safes) ta*)
727 | C.Prod _ -> raise (AssertFailure "10")
728 | C.Lambda (name,so,ta) ->
729 check_is_really_smaller_arg ~subst context n nn kl x safes so &&
730 check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
731 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
732 | C.LetIn (name,so,ta) ->
733 check_is_really_smaller_arg ~subst context n nn kl x safes so &&
734 check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context)
735 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
737 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
738 (*CSC: solo perche' non abbiamo trovato controesempi *)
739 check_is_really_smaller_arg ~subst context n nn kl x safes he
740 | C.Appl [] -> raise (AssertFailure "11")
742 | C.MutInd _ -> raise (AssertFailure "12")
743 | C.MutConstruct _ -> false
744 | C.MutCase (uri,i,outtype,term,pl) ->
746 C.Rel m when List.mem m safes || m = x ->
747 let (tys,len,isinductive,paramsno,cl) =
748 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
750 C.InductiveDefinition (tl,_,paramsno,_) ->
753 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
755 let (_,isinductive,_,cl) = List.nth tl i in
759 (id, snd (split_prods ~subst tys paramsno ty))) cl
761 (tys,List.length tl,isinductive,paramsno,cl')
763 raise (TypeCheckerFailure
764 ("Unknown mutual inductive definition:" ^
765 UriManager.string_of_uri uri))
767 if not isinductive then
770 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
777 Invalid_argument _ ->
778 raise (TypeCheckerFailure "not enough patterns")
783 let debrujinedte = debrujin_constructor uri len c in
784 recursive_args tys 0 len debrujinedte
786 let (e,safes',n',nn',x',context') =
787 get_new_safes ~subst context p c rl' safes n nn x
790 check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
792 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
793 let (tys,len,isinductive,paramsno,cl) =
794 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
796 C.InductiveDefinition (tl,_,paramsno,_) ->
797 let (_,isinductive,_,cl) = List.nth tl i in
799 List.map (fun (n,_,ty,_) ->
800 Some(Cic.Name n,(Cic.Decl ty))) tl
805 (id, snd (split_prods ~subst tys paramsno ty))) cl
807 (tys,List.length tl,isinductive,paramsno,cl')
809 raise (TypeCheckerFailure
810 ("Unknown mutual inductive definition:" ^
811 UriManager.string_of_uri uri))
813 if not isinductive then
816 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
823 Invalid_argument _ ->
824 raise (TypeCheckerFailure "not enough patterns")
826 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
827 (*CSC: sugli argomenti di una applicazione *)
831 let debrujinedte = debrujin_constructor uri len c in
832 recursive_args tys 0 len debrujinedte
834 let (e, safes',n',nn',x',context') =
835 get_new_safes context p c rl' safes n nn x
838 check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
843 i && check_is_really_smaller_arg ~subst context n nn kl x safes p
847 let len = List.length fl in
848 let n_plus_len = n + len
849 and nn_plus_len = nn + len
850 and x_plus_len = x + len
851 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
852 and safes' = List.map (fun x -> x + len) safes in
854 (fun (_,_,ty,bo) i ->
856 check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
860 let len = List.length fl in
861 let n_plus_len = n + len
862 and nn_plus_len = nn + len
863 and x_plus_len = x + len
864 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
865 and safes' = List.map (fun x -> x + len) safes in
869 check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
873 and guarded_by_destructors ?(subst = []) context n nn kl x safes =
874 let module C = Cic in
875 let module U = UriManager in
877 C.Rel m when m > n && m <= nn -> false
879 (match List.nth context (n-1) with
880 Some (_,C.Decl _) -> true
881 | Some (_,C.Def (bo,_)) ->
882 guarded_by_destructors context m nn kl x safes
883 (CicSubstitution.lift m bo)
884 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
888 | C.Implicit _ -> true
890 guarded_by_destructors context n nn kl x safes te &&
891 guarded_by_destructors context n nn kl x safes ty
892 | C.Prod (name,so,ta) ->
893 guarded_by_destructors context n nn kl x safes so &&
894 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
895 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
896 | C.Lambda (name,so,ta) ->
897 guarded_by_destructors context n nn kl x safes so &&
898 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
899 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
900 | C.LetIn (name,so,ta) ->
901 guarded_by_destructors context n nn kl x safes so &&
902 guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
903 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
904 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
905 let k = List.nth kl (m - n - 1) in
906 if not (List.length tl > k) then false
910 i && guarded_by_destructors context n nn kl x safes param
912 check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
915 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
917 | C.Var (_,exp_named_subst)
918 | C.Const (_,exp_named_subst)
919 | C.MutInd (_,_,exp_named_subst)
920 | C.MutConstruct (_,_,_,exp_named_subst) ->
922 (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
924 | C.MutCase (uri,i,outtype,term,pl) ->
925 (match CicReduction.whd context term with
926 C.Rel m when List.mem m safes || m = x ->
927 let (tys,len,isinductive,paramsno,cl) =
928 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
930 C.InductiveDefinition (tl,_,paramsno,_) ->
931 let len = List.length tl in
932 let (_,isinductive,_,cl) = List.nth tl i in
934 List.map (fun (n,_,ty,_) ->
935 Some(Cic.Name n,(Cic.Decl ty))) tl
940 let debrujinedty = debrujin_constructor uri len ty in
941 (id, snd (split_prods ~subst tys paramsno ty),
942 snd (split_prods ~subst tys paramsno debrujinedty)
945 (tys,len,isinductive,paramsno,cl')
947 raise (TypeCheckerFailure
948 ("Unknown mutual inductive definition:" ^
949 UriManager.string_of_uri uri))
951 if not isinductive then
952 guarded_by_destructors context n nn kl x safes outtype &&
953 guarded_by_destructors context n nn kl x safes term &&
954 (*CSC: manca ??? il controllo sul tipo di term? *)
957 i && guarded_by_destructors context n nn kl x safes p)
964 Invalid_argument _ ->
965 raise (TypeCheckerFailure "not enough patterns")
967 guarded_by_destructors context n nn kl x safes outtype &&
968 (*CSC: manca ??? il controllo sul tipo di term? *)
970 (fun (p,(_,c,brujinedc)) i ->
971 let rl' = recursive_args tys 0 len brujinedc in
972 let (e,safes',n',nn',x',context') =
973 get_new_safes context p c rl' safes n nn x
976 guarded_by_destructors context' n' nn' kl x' safes' e
978 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
979 let (tys,len,isinductive,paramsno,cl) =
980 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
982 C.InductiveDefinition (tl,_,paramsno,_) ->
983 let (_,isinductive,_,cl) = List.nth tl i in
986 (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
991 (id, snd (split_prods ~subst tys paramsno ty))) cl
993 (tys,List.length tl,isinductive,paramsno,cl')
995 raise (TypeCheckerFailure
996 ("Unknown mutual inductive definition:" ^
997 UriManager.string_of_uri uri))
999 if not isinductive then
1000 guarded_by_destructors context n nn kl x safes outtype &&
1001 guarded_by_destructors context n nn kl x safes term &&
1002 (*CSC: manca ??? il controllo sul tipo di term? *)
1005 i && guarded_by_destructors context n nn kl x safes p)
1012 Invalid_argument _ ->
1013 raise (TypeCheckerFailure "not enough patterns")
1015 guarded_by_destructors context n nn kl x safes outtype &&
1016 (*CSC: manca ??? il controllo sul tipo di term? *)
1019 i && guarded_by_destructors context n nn kl x safes t)
1024 let debrujinedte = debrujin_constructor uri len c in
1025 recursive_args tys 0 len debrujinedte
1027 let (e, safes',n',nn',x',context') =
1028 get_new_safes context p c rl' safes n nn x
1031 guarded_by_destructors context' n' nn' kl x' safes' e
1034 guarded_by_destructors context n nn kl x safes outtype &&
1035 guarded_by_destructors context n nn kl x safes term &&
1036 (*CSC: manca ??? il controllo sul tipo di term? *)
1038 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
1042 let len = List.length fl in
1043 let n_plus_len = n + len
1044 and nn_plus_len = nn + len
1045 and x_plus_len = x + len
1046 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1047 and safes' = List.map (fun x -> x + len) safes in
1049 (fun (_,_,ty,bo) i ->
1050 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1051 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1052 x_plus_len safes' bo
1054 | C.CoFix (_, fl) ->
1055 let len = List.length fl in
1056 let n_plus_len = n + len
1057 and nn_plus_len = nn + len
1058 and x_plus_len = x + len
1059 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1060 and safes' = List.map (fun x -> x + len) safes in
1064 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1065 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1066 x_plus_len safes' bo
1069 (* the boolean h means already protected *)
1070 (* args is the list of arguments the type of the constructor that may be *)
1071 (* found in head position must be applied to. *)
1072 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
1073 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
1074 let module C = Cic in
1075 (*CSC: There is a lot of code replication between the cases X and *)
1076 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
1077 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
1078 match CicReduction.whd context te with
1079 C.Rel m when m > n && m <= nn -> h
1087 (* the term has just been type-checked *)
1088 raise (AssertFailure "17")
1089 | C.Lambda (name,so,de) ->
1090 does_not_occur context n nn so &&
1091 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
1092 (n + 1) (nn + 1) h de args coInductiveTypeURI
1093 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
1095 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
1096 | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
1100 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1101 with Not_found -> assert false
1104 C.InductiveDefinition (itl,_,_,_) ->
1105 let (_,_,_,cl) = List.nth itl i in
1106 let (_,cons) = List.nth cl (j - 1) in
1107 CicSubstitution.subst_vars exp_named_subst cons
1109 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1110 UriManager.string_of_uri uri))
1112 let rec analyse_branch context ty te =
1113 match CicReduction.whd context ty with
1114 C.Meta _ -> raise (AssertFailure "34")
1118 does_not_occur context n nn te
1121 raise (AssertFailure "24")(* due to type-checking *)
1122 | C.Prod (name,so,de) ->
1123 analyse_branch ((Some (name,(C.Decl so)))::context) de te
1126 raise (AssertFailure "25")(* due to type-checking *)
1127 | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1128 when uri == coInductiveTypeURI ->
1129 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1130 | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1131 guarded_by_constructors context n nn true te tl coInductiveTypeURI
1133 does_not_occur context n nn te
1134 | C.Const _ -> raise (AssertFailure "26")
1135 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1136 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1138 does_not_occur context n nn te
1139 | C.MutConstruct _ -> raise (AssertFailure "27")
1140 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1141 (*CSC: in head position. *)
1145 raise (AssertFailure "28")(* due to type-checking *)
1147 let rec analyse_instantiated_type context ty l =
1148 match CicReduction.whd context ty with
1154 | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1155 | C.Prod (name,so,de) ->
1160 analyse_branch context so he &&
1161 analyse_instantiated_type
1162 ((Some (name,(C.Decl so)))::context) de tl
1166 raise (AssertFailure "30")(* due to type-checking *)
1169 (fun i x -> i && does_not_occur context n nn x) true l
1170 | C.Const _ -> raise (AssertFailure "31")
1173 (fun i x -> i && does_not_occur context n nn x) true l
1174 | C.MutConstruct _ -> raise (AssertFailure "32")
1175 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1176 (*CSC: in head position. *)
1180 raise (AssertFailure "33")(* due to type-checking *)
1182 let rec instantiate_type args consty =
1185 | tlhe::tltl as l ->
1186 let consty' = CicReduction.whd context consty in
1192 let instantiated_de = CicSubstitution.subst he de in
1193 (*CSC: siamo sicuri che non sia troppo forte? *)
1194 does_not_occur context n nn tlhe &
1195 instantiate_type tl instantiated_de tltl
1197 (*CSC:We do not consider backbones with a MutCase, a *)
1198 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1199 raise (AssertFailure "23")
1201 | [] -> analyse_instantiated_type context consty' l
1202 (* These are all the other cases *)
1204 instantiate_type args consty tl
1205 | C.Appl ((C.CoFix (_,fl))::tl) ->
1206 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1207 let len = List.length fl in
1208 let n_plus_len = n + len
1209 and nn_plus_len = nn + len
1210 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1211 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1214 i && does_not_occur context n nn ty &&
1215 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1216 args coInductiveTypeURI
1218 | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1219 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1220 does_not_occur context n nn out &&
1221 does_not_occur context n nn te &&
1225 guarded_by_constructors context n nn h x args coInductiveTypeURI
1228 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1229 | C.Var (_,exp_named_subst)
1230 | C.Const (_,exp_named_subst) ->
1232 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1233 | C.MutInd _ -> assert false
1234 | C.MutConstruct (_,_,_,exp_named_subst) ->
1236 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1237 | C.MutCase (_,_,out,te,pl) ->
1238 does_not_occur context n nn out &&
1239 does_not_occur context n nn te &&
1243 guarded_by_constructors context n nn h x args coInductiveTypeURI
1246 let len = List.length fl in
1247 let n_plus_len = n + len
1248 and nn_plus_len = nn + len
1249 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1250 and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1252 (fun (_,_,ty,bo) i ->
1253 i && does_not_occur context n nn ty &&
1254 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1257 let len = List.length fl in
1258 let n_plus_len = n + len
1259 and nn_plus_len = nn + len
1260 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1261 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1264 i && does_not_occur context n nn ty &&
1265 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1266 args coInductiveTypeURI
1269 and check_allowed_sort_elimination ~logger context uri i need_dummy ind
1270 arity1 arity2 ugraph =
1271 let module C = Cic in
1272 let module U = UriManager in
1273 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1274 (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
1275 let b,ugraph1 = CicReduction.are_convertible context so1 so2 ugraph in
1277 check_allowed_sort_elimination ~logger context uri i need_dummy
1278 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1
1281 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
1282 | (C.Sort C.Prop, C.Sort C.Set)
1283 | (C.Sort C.Prop, C.Sort C.CProp)
1284 | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1285 (* TASSI: da verificare *)
1286 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1287 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1289 C.InductiveDefinition (itl,_,_,_) ->
1290 let (_,_,_,cl) = List.nth itl i in
1291 (* is a singleton definition or the empty proposition? *)
1292 (List.length cl = 1 || List.length cl = 0) , ugraph
1294 raise (TypeCheckerFailure
1295 ("Unknown mutual inductive definition:" ^
1296 UriManager.string_of_uri uri))
1298 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
1299 | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
1300 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
1301 | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph
1302 | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
1303 | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
1304 | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
1305 (* TASSI: da verificare *)
1307 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1309 C.InductiveDefinition (itl,_,paramsno,_) ->
1311 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1313 let (_,_,_,cl) = List.nth itl i in
1315 (fun (_,x) (i,ugraph) ->
1317 is_small ~logger tys paramsno x ugraph
1322 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1323 UriManager.string_of_uri uri))
1325 | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
1326 (* TASSI: da verificare *)
1327 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1328 let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1332 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1333 C.Sort C.Prop -> true,ugraph1
1334 | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
1335 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1337 C.InductiveDefinition (itl,_,_,_) ->
1338 let (_,_,_,cl) = List.nth itl i in
1339 (* is a singleton definition or the empty proposition? *)
1340 (List.length cl = 1 || List.length cl = 0),ugraph1
1342 raise (TypeCheckerFailure
1343 ("Unknown mutual inductive definition:" ^
1344 UriManager.string_of_uri uri)))
1345 | _ -> false,ugraph1)
1346 | ((C.Sort C.Set, C.Prod (name,so,ta))
1347 | (C.Sort C.CProp, C.Prod (name,so,ta)))
1348 when not need_dummy ->
1349 let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1353 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1355 | C.Sort C.Set -> true,ugraph1
1356 | C.Sort C.CProp -> true,ugraph1
1357 | C.Sort (C.Type _) ->
1358 (* TASSI: da verificare *)
1359 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1361 C.InductiveDefinition (itl,_,paramsno,_) ->
1362 let (_,_,_,cl) = List.nth itl i in
1365 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1368 (fun (_,x) (i,ugraph) ->
1370 is_small ~logger tys paramsno x ugraph
1373 ) cl (true,ugraph1))
1375 raise (TypeCheckerFailure
1376 ("Unknown mutual inductive definition:" ^
1377 UriManager.string_of_uri uri))
1379 | _ -> raise (AssertFailure "19")
1381 | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
1382 (* TASSI: da verificare *)
1383 CicReduction.are_convertible context so ind ugraph
1384 | (_,_) -> false,ugraph
1386 and type_of_branch context argsno need_dummy outtype term constype =
1387 let module C = Cic in
1388 let module R = CicReduction in
1389 match R.whd context constype with
1394 C.Appl [outtype ; term]
1395 | C.Appl (C.MutInd (_,_,_)::tl) ->
1396 let (_,arguments) = split tl argsno
1398 if need_dummy && arguments = [] then
1401 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1402 | C.Prod (name,so,de) ->
1404 match CicSubstitution.lift 1 term with
1405 C.Appl l -> C.Appl (l@[C.Rel 1])
1406 | t -> C.Appl [t ; C.Rel 1]
1408 C.Prod (C.Anonymous,so,type_of_branch
1409 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1410 (CicSubstitution.lift 1 outtype) term' de)
1411 | _ -> raise (AssertFailure "20")
1413 (* check_metasenv_consistency checks that the "canonical" context of a
1414 metavariable is consitent - up to relocation via the relocation list l -
1415 with the actual context *)
1418 and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
1419 canonical_context l ugraph
1421 let module C = Cic in
1422 let module R = CicReduction in
1423 let module S = CicSubstitution in
1424 let lifted_canonical_context =
1428 | (Some (n,C.Decl t))::tl ->
1429 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1430 | (Some (n,C.Def (t,None)))::tl ->
1431 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1432 | None::tl -> None::(aux (i+1) tl)
1433 | (Some (n,C.Def (t,Some ty)))::tl ->
1434 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
1436 aux 1 canonical_context
1442 | Some t,Some (_,C.Def (ct,_)) ->
1444 R.are_convertible ~subst ~metasenv context t ct ugraph
1449 (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))
1452 | Some t,Some (_,C.Decl ct) ->
1453 let type_t,ugraph1 =
1454 type_of_aux' ~logger ~subst metasenv context t ugraph
1457 R.are_convertible ~subst ~metasenv context type_t ct ugraph1
1460 raise (TypeCheckerFailure
1461 (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1462 (CicPp.ppterm ct) (CicPp.ppterm t)
1463 (CicPp.ppterm type_t)))
1467 raise (TypeCheckerFailure
1468 ("Not well typed metavariable local context: "^
1469 "an hypothesis, that is not hidden, is not instantiated"))
1470 ) ugraph l lifted_canonical_context
1474 type_of_aux' is just another name (with a different scope)
1478 and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
1479 let rec type_of_aux ~logger context t ugraph =
1480 let module C = Cic in
1481 let module R = CicReduction in
1482 let module S = CicSubstitution in
1483 let module U = UriManager in
1487 match List.nth context (n - 1) with
1488 Some (_,C.Decl t) -> S.lift n t,ugraph
1489 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
1490 | Some (_,C.Def (bo,None)) ->
1491 debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ;
1492 type_of_aux ~logger context (S.lift n bo) ugraph
1494 (TypeCheckerFailure "Reference to deleted hypothesis")
1497 raise (TypeCheckerFailure "unbound variable")
1499 | C.Var (uri,exp_named_subst) ->
1502 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1504 let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
1505 let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
1510 let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
1512 check_metasenv_consistency ~logger
1513 ~subst metasenv context canonical_context l ugraph
1515 (* assuming subst is well typed !!!!! *)
1516 ((CicSubstitution.subst_meta l ty), ugraph1)
1517 (* type_of_aux context (CicSubstitution.subst_meta l term) *)
1518 with CicUtil.Subst_not_found _ ->
1519 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1521 check_metasenv_consistency ~logger
1522 ~subst metasenv context canonical_context l ugraph
1524 ((CicSubstitution.subst_meta l ty),ugraph1))
1525 (* TASSI: CONSTRAINTS *)
1526 | C.Sort (C.Type t) ->
1527 let t' = CicUniv.fresh() in
1528 let ugraph1 = CicUniv.add_gt t' t ugraph in
1529 (C.Sort (C.Type t')),ugraph1
1530 (* TASSI: CONSTRAINTS *)
1531 | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
1532 | C.Implicit _ -> raise (AssertFailure "21")
1533 | C.Cast (te,ty) as t ->
1534 let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1535 let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
1537 R.are_convertible ~subst ~metasenv context ty_te ty ugraph2
1542 raise (TypeCheckerFailure
1543 (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1544 | C.Prod (name,s,t) ->
1545 let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1547 type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t ugraph1
1549 sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2
1550 | C.Lambda (n,s,t) ->
1551 let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1552 (match R.whd ~subst context sort1 with
1557 (TypeCheckerFailure (sprintf
1558 "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
1559 (CicPp.ppterm sort1)))
1562 type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
1564 (C.Prod (n,s,type2)),ugraph2
1565 | C.LetIn (n,s,t) ->
1566 (* only to check if s is well-typed *)
1567 let ty,ugraph1 = type_of_aux ~logger context s ugraph in
1568 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1569 LetIn is later reduced and maybe also re-checked.
1570 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1572 (* The type of the LetIn is reduced. Much faster than the previous
1573 solution. Moreover the inferred type is probably very different
1574 from the expected one.
1575 (CicReduction.whd context
1576 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1578 (* One-step LetIn reduction. Even faster than the previous solution.
1579 Moreover the inferred type is closer to the expected one. *)
1582 ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
1584 (CicSubstitution.subst s ty1),ugraph2
1585 | C.Appl (he::tl) when List.length tl > 0 ->
1586 let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
1587 let tlbody_and_type,ugraph2 =
1590 let ty,ugraph1 = type_of_aux ~logger context x ugraph in
1591 let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
1592 ((x,ty)::l,ugraph1))
1595 (* TASSI: questa c'era nel mio... ma non nel CVS... *)
1596 (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
1597 eat_prods ~subst context hetype tlbody_and_type ugraph2
1598 | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1599 | C.Const (uri,exp_named_subst) ->
1602 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1604 let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
1606 CicSubstitution.subst_vars exp_named_subst cty
1610 | C.MutInd (uri,i,exp_named_subst) ->
1613 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1615 (* TASSI: da me c'era anche questa, ma in CVS no *)
1616 let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
1617 (* fine parte dubbia *)
1619 CicSubstitution.subst_vars exp_named_subst mty
1623 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1625 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1627 (* TASSI: idem come sopra *)
1629 type_of_mutual_inductive_constr ~logger uri i j ugraph1
1632 CicSubstitution.subst_vars exp_named_subst mty
1635 | C.MutCase (uri,i,outtype,term,pl) ->
1636 let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
1637 let (need_dummy, k) =
1638 let rec guess_args context t =
1639 let outtype = CicReduction.whd ~subst context t in
1641 C.Sort _ -> (true, 0)
1642 | C.Prod (name, s, t) ->
1644 guess_args ((Some (name,(C.Decl s)))::context) t in
1646 (* last prod before sort *)
1647 match CicReduction.whd ~subst context s with
1648 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1649 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1651 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1652 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1653 when U.eq uri' uri && i' = i -> (false, 1)
1661 "Malformed case analasys' output type %s"
1662 (CicPp.ppterm outtype)))
1665 let (parameters, arguments, exp_named_subst),ugraph2 =
1666 let ty,ugraph2 = type_of_aux context term ugraph1 in
1667 match R.whd context ty with
1668 (*CSC manca il caso dei CAST *)
1669 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1670 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
1671 (*CSC: Hint: nella DTD servono per gli stylesheet. *)
1672 C.MutInd (uri',i',exp_named_subst) as typ ->
1673 if U.eq uri uri' && i = i' then
1674 ([],[],exp_named_subst),ugraph2
1679 ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1680 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1682 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1683 if U.eq uri uri' && i = i' then
1685 split tl (List.length tl - k)
1686 in (params,args,exp_named_subst),ugraph2
1691 ("Case analysys: analysed term type is %s, "^
1692 "but is expected to be (an application of) "^
1694 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1700 "analysed term %s is not an inductive one")
1701 (CicPp.ppterm term)))
1703 let (b, k) = guess_args context outsort in
1704 if not b then (b, k - 1) else (b, k) in
1705 let (parameters, arguments, exp_named_subst),ugraph2 =
1706 let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
1707 match R.whd ~subst context ty with
1708 C.MutInd (uri',i',exp_named_subst) as typ ->
1709 if U.eq uri uri' && i = i' then
1710 ([],[],exp_named_subst),ugraph2
1714 ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1715 (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1717 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1718 if U.eq uri uri' && i = i' then
1720 split tl (List.length tl - k)
1721 in (params,args,exp_named_subst),ugraph2
1725 ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1726 (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1731 "Case analysis: analysed term %s is not an inductive one"
1732 (CicPp.ppterm term)))
1735 let's control if the sort elimination is allowed:
1738 let sort_of_ind_type =
1739 if parameters = [] then
1740 C.MutInd (uri,i,exp_named_subst)
1742 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1744 let type_of_sort_of_ind_ty,ugraph3 =
1745 type_of_aux ~logger context sort_of_ind_type ugraph2 in
1747 check_allowed_sort_elimination ~logger context uri i need_dummy
1748 sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
1752 (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1753 (* let's check if the type of branches are right *)
1757 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1758 with Not_found -> assert false
1761 C.InductiveDefinition (_,_,parsno,_) -> parsno
1763 raise (TypeCheckerFailure
1764 ("Unknown mutual inductive definition:" ^
1765 UriManager.string_of_uri uri))
1767 let (_,branches_ok,ugraph5) =
1769 (fun (j,b,ugraph) p ->
1772 if parameters = [] then
1773 (C.MutConstruct (uri,i,j,exp_named_subst))
1776 (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1778 let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
1779 let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
1782 type_of_branch context parsno need_dummy outtype cons
1786 ~subst ~metasenv context ty_p ty_branch ugraph3
1790 ("#### " ^ CicPp.ppterm ty_p ^
1791 " <==> " ^ CicPp.ppterm ty_branch));
1795 ) (1,true,ugraph4) pl
1797 if not branches_ok then
1799 (TypeCheckerFailure "Case analysys: wrong branch type");
1801 if not need_dummy then outtype::arguments@[term]
1802 else outtype::arguments in
1804 if need_dummy && arguments = [] then outtype
1805 else CicReduction.head_beta_reduce (C.Appl arguments')
1809 let types_times_kl,ugraph1 =
1810 (* WAS: list rev list map *)
1812 (fun (l,ugraph) (n,k,ty,_) ->
1813 let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1814 ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
1817 let (types,kl) = List.split types_times_kl in
1818 let len = List.length types in
1821 (fun ugraph (name,x,ty,bo) ->
1823 type_of_aux ~logger (types@context) bo ugraph
1826 R.are_convertible ~subst ~metasenv (types@context)
1827 ty_bo (CicSubstitution.lift len ty) ugraph1 in
1830 let (m, eaten, context') =
1831 eat_lambdas ~subst (types @ context) (x + 1) bo
1834 let's control the guarded by
1835 destructors conditions D{f,k,x,M}
1837 if not (guarded_by_destructors context' eaten
1838 (len + eaten) kl 1 [] m) then
1841 ("Fix: not guarded by destructors"))
1846 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1848 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1849 let (_,_,ty,_) = List.nth fl i in
1854 (fun (l,ugraph) (n,ty,_) ->
1856 type_of_aux ~logger context ty ugraph in
1857 (Some (C.Name n,(C.Decl ty))::l,ugraph1)
1860 let len = List.length types in
1863 (fun ugraph (_,ty,bo) ->
1865 type_of_aux ~logger (types @ context) bo ugraph
1868 R.are_convertible ~subst ~metasenv (types @ context) ty_bo
1869 (CicSubstitution.lift len ty) ugraph1
1873 (* let's control that the returned type is coinductive *)
1874 match returns_a_coinductive context ty with
1878 ("CoFix: does not return a coinductive type"))
1881 let's control the guarded by constructors
1884 if not (guarded_by_constructors (types @ context)
1885 0 len false bo [] uri) then
1888 ("CoFix: not guarded by constructors"))
1894 (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1897 let (_,ty,_) = List.nth fl i in
1900 and check_exp_named_subst ~logger ?(subst = []) context ugraph =
1901 let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
1904 | ((uri,t) as item)::tl ->
1905 let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in
1907 CicSubstitution.subst_vars esubsts ty_uri in
1908 let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in
1910 CicReduction.are_convertible ~subst ~metasenv
1911 context typeoft typeofvar ugraph2
1914 check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3
1917 CicReduction.fdebug := 0 ;
1919 (CicReduction.are_convertible
1920 ~subst ~metasenv context typeoft typeofvar ugraph2) ;
1922 debug typeoft [typeofvar] ;
1923 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1926 check_exp_named_subst_aux ~logger [] ugraph
1928 and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph =
1929 let module C = Cic in
1930 let t1' = CicReduction.whd ~subst context t1 in
1931 let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1932 match (t1', t2') with
1933 (C.Sort s1, C.Sort s2)
1934 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1935 (* different from Coq manual!!! *)
1937 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1938 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1939 let t' = CicUniv.fresh() in
1940 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1941 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1942 C.Sort (C.Type t'),ugraph2
1943 | (C.Sort _,C.Sort (C.Type t1)) ->
1944 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1945 C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
1946 | (C.Meta _, C.Sort _) -> t2',ugraph
1947 | (C.Meta _, (C.Meta (_,_) as t))
1948 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1950 | (_,_) -> raise (TypeCheckerFailure (sprintf
1951 "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1952 (CicPp.ppterm t2')))
1954 and eat_prods ?(subst = []) context hetype l ugraph =
1955 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1959 | (hete, hety)::tl ->
1960 (match (CicReduction.whd ~subst context hetype) with
1963 CicReduction.are_convertible
1964 ~subst ~metasenv context hety s ugraph
1968 CicReduction.fdebug := -1 ;
1969 eat_prods ~subst context
1970 (CicSubstitution.subst hete t) tl ugraph1
1971 (*TASSI: not sure *)
1975 CicReduction.fdebug := 0 ;
1976 ignore (CicReduction.are_convertible
1977 ~subst ~metasenv context s hety ugraph) ;
1983 ("Appl: wrong parameter-type, expected %s, found %s")
1984 (CicPp.ppterm hetype) (CicPp.ppterm s)))
1987 raise (TypeCheckerFailure
1988 "Appl: this is not a function, it cannot be applied")
1991 and returns_a_coinductive context ty =
1992 let module C = Cic in
1993 match CicReduction.whd context ty with
1994 C.MutInd (uri,i,_) ->
1995 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1998 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1999 with Not_found -> assert false
2002 C.InductiveDefinition (itl,_,_,_) ->
2003 let (_,is_inductive,_,_) = List.nth itl i in
2004 if is_inductive then None else (Some uri)
2006 raise (TypeCheckerFailure
2007 ("Unknown mutual inductive definition:" ^
2008 UriManager.string_of_uri uri))
2010 | C.Appl ((C.MutInd (uri,i,_))::_) ->
2011 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
2013 C.InductiveDefinition (itl,_,_,_) ->
2014 let (_,is_inductive,_,_) = List.nth itl i in
2015 if is_inductive then None else (Some uri)
2017 raise (TypeCheckerFailure
2018 ("Unknown mutual inductive definition:" ^
2019 UriManager.string_of_uri uri))
2021 | C.Prod (n,so,de) ->
2022 returns_a_coinductive ((Some (n,C.Decl so))::context) de
2027 debug_print (lazy ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t)) ; flush stderr ;
2030 type_of_aux ~logger context t ugraph
2032 in debug_print (lazy "FINE TYPE_OF_AUX") ; flush stderr ; res
2035 (* is a small constructor? *)
2036 (*CSC: ottimizzare calcolando staticamente *)
2037 and is_small ~logger context paramsno c ugraph =
2038 let rec is_small_aux ~logger context c ugraph =
2039 let module C = Cic in
2040 match CicReduction.whd context c with
2042 (*CSC: [] is an empty metasenv. Is it correct? *)
2043 let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
2044 let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
2046 is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
2049 | _ -> true,ugraph (*CSC: we trust the type-checker *)
2051 let (context',dx) = split_prods context paramsno c in
2052 is_small_aux ~logger context' dx ugraph
2054 and type_of ~logger t ugraph =
2056 debug_print (lazy ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t)) ; flush stderr ;
2059 type_of_aux' ~logger [] [] t ugraph
2061 in debug_print (lazy "FINE TYPE_OF_AUX'") ; flush stderr ; res
2065 let typecheck_obj0 ~logger uri ugraph =
2066 let module C = Cic in
2068 C.Constant (_,Some te,ty,_,_) ->
2069 let _,ugraph = type_of ~logger ty ugraph in
2070 let ty_te,ugraph = type_of ~logger te ugraph in
2071 let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
2073 raise (TypeCheckerFailure
2074 ("the type of the body is not the one expected"))
2077 | C.Constant (_,None,ty,_,_) ->
2078 (* only to check that ty is well-typed *)
2079 let _,ugraph = type_of ~logger ty ugraph in
2081 | C.CurrentProof (_,conjs,te,ty,_,_) ->
2084 (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
2086 type_of_aux' ~logger metasenv context ty ugraph
2088 metasenv @ [conj],ugraph
2091 let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
2092 let type_of_te,ugraph =
2093 type_of_aux' ~logger conjs [] te ugraph
2095 let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
2097 raise (TypeCheckerFailure (sprintf
2098 "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
2099 (CicPp.ppterm type_of_te) (CicPp.ppterm ty)))
2102 | C.Variable (_,bo,ty,_,_) ->
2103 (* only to check that ty is well-typed *)
2104 let _,ugraph = type_of ~logger ty ugraph in
2108 let ty_bo,ugraph = type_of ~logger bo ugraph in
2109 let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
2111 raise (TypeCheckerFailure
2112 ("the body is not the one expected"))
2116 | (C.InductiveDefinition _ as obj) ->
2117 check_mutual_inductive_defs ~logger uri obj ugraph
2120 let module C = Cic in
2121 let module R = CicReduction in
2122 let module U = UriManager in
2123 let logger = new CicLogger.logger in
2124 (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
2125 match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
2126 CicEnvironment.CheckedObj (cobj,ugraph') ->
2127 (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*)
2129 | CicEnvironment.UncheckedObj uobj ->
2130 (* let's typecheck the uncooked object *)
2131 logger#log (`Start_type_checking uri) ;
2132 (* debug_print (lazy ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri)); *)
2133 let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
2135 CicEnvironment.set_type_checking_info uri;
2136 logger#log (`Type_checking_completed uri);
2137 match CicEnvironment.is_type_checked ~trust:false ugraph uri with
2138 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
2139 | _ -> raise CicEnvironmentError
2142 this is raised if set_type_checking_info is called on an object
2143 that has no associated universe file. If we are in univ_maker
2144 phase this is OK since univ_maker will properly commit the
2147 Invalid_argument s ->
2148 (*debug_print (lazy s);*)
2152 let clean_and_fill u o g =
2153 (profiler_clean_fill (CicUnivUtils.clean_and_fill u o)) g
2155 let typecheck_obj ~logger uri obj =
2156 let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
2157 let ugraph = clean_and_fill uri obj ugraph in
2158 CicEnvironment.add_type_checked_obj uri (obj,ugraph)
2160 (** wrappers which instantiate fresh loggers *)
2162 let type_of_aux' ?(subst = []) metasenv context t ugraph =
2163 let logger = new CicLogger.logger in
2164 type_of_aux' ~logger ~subst metasenv context t ugraph
2166 let typecheck_obj uri obj =
2167 let logger = new CicLogger.logger in
2168 typecheck_obj ~logger uri obj