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 uri =
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 uri with
127 CicEnvironment.CheckedObj cobj -> cobj
128 | CicEnvironment.UncheckedObj uobj ->
129 CicLogger.log (`Start_type_checking uri) ;
130 (* let's typecheck the uncooked obj *)
132 C.Constant (_,Some te,ty,_) ->
133 let _ = type_of ty in
134 let type_of_te = type_of te in
135 if not (R.are_convertible [] type_of_te ty) then
136 raise (TypeCheckerFailure (sprintf
137 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
138 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
140 | C.Constant (_,None,ty,_) ->
141 (* only to check that ty is well-typed *)
142 let _ = type_of ty in ()
143 | C.CurrentProof (_,conjs,te,ty,_) ->
146 (fun metasenv ((_,context,ty) as conj) ->
147 ignore (type_of_aux' metasenv context ty) ;
151 let _ = type_of_aux' conjs [] ty in
152 let type_of_te = type_of_aux' conjs [] te in
153 if not (R.are_convertible [] type_of_te ty) then
154 raise (TypeCheckerFailure (sprintf
155 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
156 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
159 raise (TypeCheckerFailure
160 ("Unknown constant:" ^ U.string_of_uri uri))
162 CicEnvironment.set_type_checking_info uri ;
163 CicLogger.log (`Type_checking_completed uri) ;
164 match CicEnvironment.is_type_checked ~trust:false uri with
165 CicEnvironment.CheckedObj cobj -> cobj
166 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
169 C.Constant (_,_,ty,_) -> ty
170 | C.CurrentProof (_,_,_,ty,_) -> ty
172 raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
174 and type_of_variable uri =
175 let module C = Cic in
176 let module R = CicReduction in
177 let module U = UriManager in
178 (* 0 because a variable is never cooked => no partial cooking at one level *)
179 match CicEnvironment.is_type_checked ~trust:true uri with
180 CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
181 | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
182 CicLogger.log (`Start_type_checking uri) ;
183 (* only to check that ty is well-typed *)
184 let _ = type_of ty in
188 if not (R.are_convertible [] (type_of bo) ty) then
189 raise (TypeCheckerFailure
190 ("Unknown variable:" ^ U.string_of_uri uri))
192 CicEnvironment.set_type_checking_info uri ;
193 CicLogger.log (`Type_checking_completed uri) ;
196 raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
198 and does_not_occur context n nn te =
199 let module C = Cic in
200 (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
201 (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
203 match CicReduction.whd context te with
204 C.Rel m when m > n && m <= nn -> false
210 does_not_occur context n nn te && does_not_occur context n nn ty
211 | C.Prod (name,so,dest) ->
212 does_not_occur context n nn so &&
213 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
215 | C.Lambda (name,so,dest) ->
216 does_not_occur context n nn so &&
217 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
219 | C.LetIn (name,so,dest) ->
220 does_not_occur context n nn so &&
221 does_not_occur ((Some (name,(C.Def (so,None))))::context)
222 (n + 1) (nn + 1) dest
224 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
225 | C.Var (_,exp_named_subst)
226 | C.Const (_,exp_named_subst)
227 | C.MutInd (_,_,exp_named_subst)
228 | C.MutConstruct (_,_,_,exp_named_subst) ->
229 List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
231 | C.MutCase (_,_,out,te,pl) ->
232 does_not_occur context n nn out && does_not_occur context n nn te &&
233 List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
235 let len = List.length fl in
236 let n_plus_len = n + len in
237 let nn_plus_len = nn + len in
239 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
242 (fun (_,_,ty,bo) i ->
243 i && does_not_occur context n nn ty &&
244 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
247 let len = List.length fl in
248 let n_plus_len = n + len in
249 let nn_plus_len = nn + len in
251 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
255 i && does_not_occur context n nn ty &&
256 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
259 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
260 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
261 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
262 (*CSC strictly_positive *)
263 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
264 and weakly_positive context n nn uri te =
265 let module C = Cic in
266 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
268 C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,[])
270 (*CSC mettere in cicSubstitution *)
271 let rec subst_inductive_type_with_dummy_mutind =
273 C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
275 | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
277 | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
278 | C.Prod (name,so,ta) ->
279 C.Prod (name, subst_inductive_type_with_dummy_mutind so,
280 subst_inductive_type_with_dummy_mutind ta)
281 | C.Lambda (name,so,ta) ->
282 C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
283 subst_inductive_type_with_dummy_mutind ta)
285 C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
286 | C.MutCase (uri,i,outtype,term,pl) ->
288 subst_inductive_type_with_dummy_mutind outtype,
289 subst_inductive_type_with_dummy_mutind term,
290 List.map subst_inductive_type_with_dummy_mutind pl)
292 C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
293 subst_inductive_type_with_dummy_mutind ty,
294 subst_inductive_type_with_dummy_mutind bo)) fl)
296 C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
297 subst_inductive_type_with_dummy_mutind ty,
298 subst_inductive_type_with_dummy_mutind bo)) fl)
299 | C.Const (uri,exp_named_subst) ->
300 let exp_named_subst' =
302 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
305 C.Const (uri,exp_named_subst')
306 | C.MutInd (uri,typeno,exp_named_subst) ->
307 let exp_named_subst' =
309 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
312 C.MutInd (uri,typeno,exp_named_subst')
313 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
314 let exp_named_subst' =
316 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
319 C.MutConstruct (uri,typeno,consno,exp_named_subst')
322 match CicReduction.whd context te with
323 C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
324 | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
325 | C.Prod (C.Anonymous,source,dest) ->
326 strictly_positive context n nn
327 (subst_inductive_type_with_dummy_mutind source) &&
328 weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
329 (n + 1) (nn + 1) uri dest
330 | C.Prod (name,source,dest) when
331 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
332 (* dummy abstraction, so we behave as in the anonimous case *)
333 strictly_positive context n nn
334 (subst_inductive_type_with_dummy_mutind source) &&
335 weakly_positive ((Some (name,(C.Decl source)))::context)
336 (n + 1) (nn + 1) uri dest
337 | C.Prod (name,source,dest) ->
338 does_not_occur context n nn
339 (subst_inductive_type_with_dummy_mutind source)&&
340 weakly_positive ((Some (name,(C.Decl source)))::context)
341 (n + 1) (nn + 1) uri dest
343 raise (TypeCheckerFailure "Malformed inductive constructor type")
345 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
346 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
347 and instantiate_parameters params c =
348 let module C = Cic in
349 match (c,params) with
351 | (C.Prod (_,_,ta), he::tl) ->
352 instantiate_parameters tl
353 (CicSubstitution.subst he ta)
354 | (C.Cast (te,_), _) -> instantiate_parameters params te
355 | (t,l) -> raise (AssertFailure "1")
357 and strictly_positive context n nn te =
358 let module C = Cic in
359 let module U = UriManager in
360 match CicReduction.whd context te with
363 (*CSC: bisogna controllare ty????*)
364 strictly_positive context n nn te
365 | C.Prod (name,so,ta) ->
366 does_not_occur context n nn so &&
367 strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
368 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
369 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
370 | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
371 let (ok,paramsno,ity,cl,name) =
372 match CicEnvironment.get_obj uri with
373 C.InductiveDefinition (tl,_,paramsno) ->
374 let (name,_,ity,cl) = List.nth tl i in
375 (List.length tl = 1, paramsno, ity, cl, name)
377 raise (TypeCheckerFailure
378 ("Unknown inductive type:" ^ U.string_of_uri uri))
380 let (params,arguments) = split tl paramsno in
381 let lifted_params = List.map (CicSubstitution.lift 1) params in
385 instantiate_parameters lifted_params
386 (CicSubstitution.subst_vars exp_named_subst te)
391 (fun x i -> i && does_not_occur context n nn x)
393 (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
398 ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
401 | t -> does_not_occur context n nn t
403 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
404 and are_all_occurrences_positive context uri indparamsno i n nn te =
405 let module C = Cic in
406 match CicReduction.whd context te with
407 C.Appl ((C.Rel m)::tl) when m = i ->
408 (*CSC: riscrivere fermandosi a 0 *)
409 (* let's check if the inductive type is applied at least to *)
410 (* indparamsno parameters *)
416 match CicReduction.whd context x with
417 C.Rel m when m = n - (indparamsno - k) -> k - 1
419 raise (TypeCheckerFailure
420 ("Non-positive occurence in mutual inductive definition(s) " ^
421 UriManager.string_of_uri uri))
425 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
427 raise (TypeCheckerFailure
428 ("Non-positive occurence in mutual inductive definition(s) " ^
429 UriManager.string_of_uri uri))
430 | C.Rel m when m = i ->
431 if indparamsno = 0 then
434 raise (TypeCheckerFailure
435 ("Non-positive occurence in mutual inductive definition(s) " ^
436 UriManager.string_of_uri uri))
437 | C.Prod (C.Anonymous,source,dest) ->
438 strictly_positive context n nn source &&
439 are_all_occurrences_positive
440 ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
441 (i+1) (n + 1) (nn + 1) dest
442 | C.Prod (name,source,dest) when
443 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
444 (* dummy abstraction, so we behave as in the anonimous case *)
445 strictly_positive context n nn source &&
446 are_all_occurrences_positive
447 ((Some (name,(C.Decl source)))::context) uri indparamsno
448 (i+1) (n + 1) (nn + 1) dest
449 | C.Prod (name,source,dest) ->
450 does_not_occur context n nn source &&
451 are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
452 uri indparamsno (i+1) (n + 1) (nn + 1) dest
455 (TypeCheckerFailure ("Malformed inductive constructor type " ^
456 (UriManager.string_of_uri uri)))
458 (* Main function to checks the correctness of a mutual *)
459 (* inductive block definition. This is the function *)
460 (* exported to the proof-engine. *)
461 and typecheck_mutual_inductive_defs uri (itl,_,indparamsno) =
462 let module U = UriManager in
463 (* let's check if the arity of the inductive types are well *)
465 List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
467 (* let's check if the types of the inductive constructors *)
468 (* are well formed. *)
469 (* In order not to use type_of_aux we put the types of the *)
470 (* mutual inductive types at the head of the types of the *)
471 (* constructors using Prods *)
472 let len = List.length itl in
474 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
480 let debrujinedte = debrujin_constructor uri len te in
483 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
486 let _ = type_of augmented_term in
487 (* let's check also the positivity conditions *)
490 (are_all_occurrences_positive tys uri indparamsno i 0 len
494 (TypeCheckerFailure ("Non positive occurence in " ^
495 U.string_of_uri uri))
502 (* Main function to checks the correctness of a mutual *)
503 (* inductive block definition. *)
504 and check_mutual_inductive_defs uri =
506 Cic.InductiveDefinition (itl, params, indparamsno) ->
507 typecheck_mutual_inductive_defs uri (itl,params,indparamsno)
509 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
510 UriManager.string_of_uri uri))
512 and type_of_mutual_inductive_defs uri i =
513 let module C = Cic in
514 let module R = CicReduction in
515 let module U = UriManager in
517 match CicEnvironment.is_type_checked ~trust:true uri with
518 CicEnvironment.CheckedObj cobj -> cobj
519 | CicEnvironment.UncheckedObj uobj ->
520 CicLogger.log (`Start_type_checking uri) ;
521 check_mutual_inductive_defs uri uobj ;
522 CicEnvironment.set_type_checking_info uri ;
523 CicLogger.log (`Type_checking_completed uri) ;
524 (match CicEnvironment.is_type_checked ~trust:false uri with
525 CicEnvironment.CheckedObj cobj -> cobj
526 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
530 C.InductiveDefinition (dl,_,_) ->
531 let (_,_,arity,_) = List.nth dl i in
534 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
535 U.string_of_uri uri))
537 and type_of_mutual_inductive_constr uri i j =
538 let module C = Cic in
539 let module R = CicReduction in
540 let module U = UriManager in
542 match CicEnvironment.is_type_checked ~trust:true uri with
543 CicEnvironment.CheckedObj cobj -> cobj
544 | CicEnvironment.UncheckedObj uobj ->
545 CicLogger.log (`Start_type_checking uri) ;
546 check_mutual_inductive_defs uri uobj ;
547 CicEnvironment.set_type_checking_info uri ;
548 CicLogger.log (`Type_checking_completed uri) ;
549 (match CicEnvironment.is_type_checked ~trust:false uri with
550 CicEnvironment.CheckedObj cobj -> cobj
551 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
555 C.InductiveDefinition (dl,_,_) ->
556 let (_,_,_,cl) = List.nth dl i in
557 let (_,ty) = List.nth cl (j-1) in
560 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
561 UriManager.string_of_uri uri))
563 and recursive_args context n nn te =
564 let module C = Cic in
565 match CicReduction.whd context te with
571 | C.Cast _ (*CSC ??? *) ->
572 raise (AssertFailure "3") (* due to type-checking *)
573 | C.Prod (name,so,de) ->
574 (not (does_not_occur context n nn so)) ::
575 (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
578 raise (AssertFailure "4") (* due to type-checking *)
580 | C.Const _ -> raise (AssertFailure "5")
585 | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *)
587 and get_new_safes context p c rl safes n nn x =
588 let module C = Cic in
589 let module U = UriManager in
590 let module R = CicReduction in
591 match (R.whd context c, R.whd context p, rl) with
592 (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
593 (* we are sure that the two sources are convertible because we *)
594 (* have just checked this. So let's go along ... *)
596 List.map (fun x -> x + 1) safes
599 if b then 1::safes' else safes'
601 get_new_safes ((Some (name,(C.Decl so)))::context)
602 ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
603 | (C.Prod _, (C.MutConstruct _ as e), _)
604 | (C.Prod _, (C.Rel _ as e), _)
605 | (C.MutInd _, e, [])
606 | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
608 (* CSC: If the next exception is raised, it just means that *)
609 (* CSC: the proof-assistant allows to use very strange things *)
610 (* CSC: as a branch of a case whose type is a Prod. In *)
611 (* CSC: particular, this means that a new (C.Prod, x,_) case *)
612 (* CSC: must be considered in this match. (e.g. x = MutCase) *)
613 raise (AssertFailure "7")
615 and split_prods context n te =
616 let module C = Cic in
617 let module R = CicReduction in
618 match (n, R.whd context te) with
620 | (n, C.Prod (name,so,ta)) when n > 0 ->
621 split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta
622 | (_, _) -> raise (AssertFailure "8")
624 and eat_lambdas context n te =
625 let module C = Cic in
626 let module R = CicReduction in
627 match (n, R.whd context te) with
628 (0, _) -> (te, 0, context)
629 | (n, C.Lambda (name,so,ta)) when n > 0 ->
630 let (te, k, context') =
631 eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
633 (te, k + 1, context')
635 raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
637 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
638 and check_is_really_smaller_arg context n nn kl x safes te =
639 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
640 (*CSC: cfr guarded_by_destructors *)
641 let module C = Cic in
642 let module U = UriManager in
643 match CicReduction.whd context te with
644 C.Rel m when List.mem m safes -> true
651 (* | C.Cast (te,ty) ->
652 check_is_really_smaller_arg n nn kl x safes te &&
653 check_is_really_smaller_arg n nn kl x safes ty*)
654 (* | C.Prod (_,so,ta) ->
655 check_is_really_smaller_arg n nn kl x safes so &&
656 check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
657 (List.map (fun x -> x + 1) safes) ta*)
658 | C.Prod _ -> raise (AssertFailure "10")
659 | C.Lambda (name,so,ta) ->
660 check_is_really_smaller_arg context n nn kl x safes so &&
661 check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context)
662 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
663 | C.LetIn (name,so,ta) ->
664 check_is_really_smaller_arg context n nn kl x safes so &&
665 check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::context)
666 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
668 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
669 (*CSC: solo perche' non abbiamo trovato controesempi *)
670 check_is_really_smaller_arg context n nn kl x safes he
671 | C.Appl [] -> raise (AssertFailure "11")
673 | C.MutInd _ -> raise (AssertFailure "12")
674 | C.MutConstruct _ -> false
675 | C.MutCase (uri,i,outtype,term,pl) ->
677 C.Rel m when List.mem m safes || m = x ->
678 let (tys,len,isinductive,paramsno,cl) =
679 match CicEnvironment.get_obj uri with
680 C.InductiveDefinition (tl,_,paramsno) ->
683 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
685 let (_,isinductive,_,cl) = List.nth tl i in
689 (id, snd (split_prods tys paramsno ty))) cl
691 (tys,List.length tl,isinductive,paramsno,cl')
693 raise (TypeCheckerFailure
694 ("Unknown mutual inductive definition:" ^
695 UriManager.string_of_uri uri))
697 if not isinductive then
700 i && check_is_really_smaller_arg context n nn kl x safes p)
706 let debrujinedte = debrujin_constructor uri len c in
707 recursive_args tys 0 len debrujinedte
709 let (e,safes',n',nn',x',context') =
710 get_new_safes context p c rl' safes n nn x
713 check_is_really_smaller_arg context' n' nn' kl x' safes' e
714 ) (List.combine pl cl) true
715 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
716 let (tys,len,isinductive,paramsno,cl) =
717 match CicEnvironment.get_obj uri with
718 C.InductiveDefinition (tl,_,paramsno) ->
719 let (_,isinductive,_,cl) = List.nth tl i in
721 List.map (fun (n,_,ty,_) ->
722 Some(Cic.Name n,(Cic.Decl ty))) tl
727 (id, snd (split_prods tys paramsno ty))) cl
729 (tys,List.length tl,isinductive,paramsno,cl')
731 raise (TypeCheckerFailure
732 ("Unknown mutual inductive definition:" ^
733 UriManager.string_of_uri uri))
735 if not isinductive then
738 i && check_is_really_smaller_arg context n nn kl x safes p)
741 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
742 (*CSC: sugli argomenti di una applicazione *)
746 let debrujinedte = debrujin_constructor uri len c in
747 recursive_args tys 0 len debrujinedte
749 let (e, safes',n',nn',x',context') =
750 get_new_safes context p c rl' safes n nn x
753 check_is_really_smaller_arg context' n' nn' kl x' safes' e
754 ) (List.combine pl cl) true
758 i && check_is_really_smaller_arg context n nn kl x safes p
762 let len = List.length fl in
763 let n_plus_len = n + len
764 and nn_plus_len = nn + len
765 and x_plus_len = x + len
766 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
767 and safes' = List.map (fun x -> x + len) safes in
769 (fun (_,_,ty,bo) i ->
771 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
775 let len = List.length fl in
776 let n_plus_len = n + len
777 and nn_plus_len = nn + len
778 and x_plus_len = x + len
779 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
780 and safes' = List.map (fun x -> x + len) safes in
784 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
788 and guarded_by_destructors context n nn kl x safes =
789 let module C = Cic in
790 let module U = UriManager in
792 C.Rel m when m > n && m <= nn -> false
794 (match List.nth context (n-1) with
795 Some (_,C.Decl _) -> true
796 | Some (_,C.Def (bo,_)) ->
797 guarded_by_destructors context n nn kl x safes bo
798 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
804 guarded_by_destructors context n nn kl x safes te &&
805 guarded_by_destructors context n nn kl x safes ty
806 | C.Prod (name,so,ta) ->
807 guarded_by_destructors context n nn kl x safes so &&
808 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
809 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
810 | C.Lambda (name,so,ta) ->
811 guarded_by_destructors context n nn kl x safes so &&
812 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
813 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
814 | C.LetIn (name,so,ta) ->
815 guarded_by_destructors context n nn kl x safes so &&
816 guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
817 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
818 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
819 let k = List.nth kl (m - n - 1) in
820 if not (List.length tl > k) then false
824 i && guarded_by_destructors context n nn kl x safes param
826 check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
829 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
831 | C.Var (_,exp_named_subst)
832 | C.Const (_,exp_named_subst)
833 | C.MutInd (_,_,exp_named_subst)
834 | C.MutConstruct (_,_,_,exp_named_subst) ->
836 (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
838 | C.MutCase (uri,i,outtype,term,pl) ->
840 C.Rel m when List.mem m safes || m = x ->
841 let (tys,len,isinductive,paramsno,cl) =
842 match CicEnvironment.get_obj uri with
843 C.InductiveDefinition (tl,_,paramsno) ->
844 let (_,isinductive,_,cl) = List.nth tl i in
846 List.map (fun (n,_,ty,_) ->
847 Some(Cic.Name n,(Cic.Decl ty))) tl
852 (id, snd (split_prods tys paramsno ty))) cl
854 (tys,List.length tl,isinductive,paramsno,cl')
856 raise (TypeCheckerFailure
857 ("Unknown mutual inductive definition:" ^
858 UriManager.string_of_uri uri))
860 if not isinductive then
861 guarded_by_destructors context n nn kl x safes outtype &&
862 guarded_by_destructors context n nn kl x safes term &&
863 (*CSC: manca ??? il controllo sul tipo di term? *)
866 i && guarded_by_destructors context n nn kl x safes p)
869 guarded_by_destructors context n nn kl x safes outtype &&
870 (*CSC: manca ??? il controllo sul tipo di term? *)
874 let debrujinedte = debrujin_constructor uri len c in
875 recursive_args tys 0 len debrujinedte
877 let (e,safes',n',nn',x',context') =
878 get_new_safes context p c rl' safes n nn x
881 guarded_by_destructors context' n' nn' kl x' safes' e
882 ) (List.combine pl cl) true
883 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
884 let (tys,len,isinductive,paramsno,cl) =
885 match CicEnvironment.get_obj uri with
886 C.InductiveDefinition (tl,_,paramsno) ->
887 let (_,isinductive,_,cl) = List.nth tl i in
890 (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
895 (id, snd (split_prods tys paramsno ty))) cl
897 (tys,List.length tl,isinductive,paramsno,cl')
899 raise (TypeCheckerFailure
900 ("Unknown mutual inductive definition:" ^
901 UriManager.string_of_uri uri))
903 if not isinductive then
904 guarded_by_destructors context n nn kl x safes outtype &&
905 guarded_by_destructors context n nn kl x safes term &&
906 (*CSC: manca ??? il controllo sul tipo di term? *)
909 i && guarded_by_destructors context n nn kl x safes p)
912 guarded_by_destructors context n nn kl x safes outtype &&
913 (*CSC: manca ??? il controllo sul tipo di term? *)
916 i && guarded_by_destructors context n nn kl x safes t)
921 let debrujinedte = debrujin_constructor uri len c in
922 recursive_args tys 0 len debrujinedte
924 let (e, safes',n',nn',x',context') =
925 get_new_safes context p c rl' safes n nn x
928 guarded_by_destructors context' n' nn' kl x' safes' e
929 ) (List.combine pl cl) true
931 guarded_by_destructors context n nn kl x safes outtype &&
932 guarded_by_destructors context n nn kl x safes term &&
933 (*CSC: manca ??? il controllo sul tipo di term? *)
935 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
939 let len = List.length fl in
940 let n_plus_len = n + len
941 and nn_plus_len = nn + len
942 and x_plus_len = x + len
943 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
944 and safes' = List.map (fun x -> x + len) safes in
946 (fun (_,_,ty,bo) i ->
947 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
948 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
952 let len = List.length fl in
953 let n_plus_len = n + len
954 and nn_plus_len = nn + len
955 and x_plus_len = x + len
956 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
957 and safes' = List.map (fun x -> x + len) safes in
961 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
962 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
966 (* the boolean h means already protected *)
967 (* args is the list of arguments the type of the constructor that may be *)
968 (* found in head position must be applied to. *)
969 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
970 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
971 let module C = Cic in
972 (*CSC: There is a lot of code replication between the cases X and *)
973 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
974 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
975 match CicReduction.whd context te with
976 C.Rel m when m > n && m <= nn -> h
984 (* the term has just been type-checked *)
985 raise (AssertFailure "17")
986 | C.Lambda (name,so,de) ->
987 does_not_occur context n nn so &&
988 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
989 (n + 1) (nn + 1) h de args coInductiveTypeURI
990 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
992 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
993 | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
995 match CicEnvironment.get_cooked_obj ~trust:false uri with
996 C.InductiveDefinition (itl,_,_) ->
997 let (_,_,_,cl) = List.nth itl i in
998 let (_,cons) = List.nth cl (j - 1) in
999 CicSubstitution.subst_vars exp_named_subst cons
1001 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1002 UriManager.string_of_uri uri))
1004 let rec analyse_branch context ty te =
1005 match CicReduction.whd context ty with
1006 C.Meta _ -> raise (AssertFailure "34")
1010 does_not_occur context n nn te
1013 raise (AssertFailure "24")(* due to type-checking *)
1014 | C.Prod (name,so,de) ->
1015 analyse_branch ((Some (name,(C.Decl so)))::context) de te
1018 raise (AssertFailure "25")(* due to type-checking *)
1019 | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1020 when uri == coInductiveTypeURI ->
1021 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1022 | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1023 guarded_by_constructors context n nn true te tl coInductiveTypeURI
1025 does_not_occur context n nn te
1026 | C.Const _ -> raise (AssertFailure "26")
1027 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1028 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1030 does_not_occur context n nn te
1031 | C.MutConstruct _ -> raise (AssertFailure "27")
1032 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1033 (*CSC: in head position. *)
1037 raise (AssertFailure "28")(* due to type-checking *)
1039 let rec analyse_instantiated_type context ty l =
1040 match CicReduction.whd context ty with
1046 | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1047 | C.Prod (name,so,de) ->
1052 analyse_branch context so he &&
1053 analyse_instantiated_type
1054 ((Some (name,(C.Decl so)))::context) de tl
1058 raise (AssertFailure "30")(* due to type-checking *)
1061 (fun i x -> i && does_not_occur context n nn x) true l
1062 | C.Const _ -> raise (AssertFailure "31")
1065 (fun i x -> i && does_not_occur context n nn x) true l
1066 | C.MutConstruct _ -> raise (AssertFailure "32")
1067 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1068 (*CSC: in head position. *)
1072 raise (AssertFailure "33")(* due to type-checking *)
1074 let rec instantiate_type args consty =
1077 | tlhe::tltl as l ->
1078 let consty' = CicReduction.whd context consty in
1084 let instantiated_de = CicSubstitution.subst he de in
1085 (*CSC: siamo sicuri che non sia troppo forte? *)
1086 does_not_occur context n nn tlhe &
1087 instantiate_type tl instantiated_de tltl
1089 (*CSC:We do not consider backbones with a MutCase, a *)
1090 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1091 raise (AssertFailure "23")
1093 | [] -> analyse_instantiated_type context consty' l
1094 (* These are all the other cases *)
1096 instantiate_type args consty tl
1097 | C.Appl ((C.CoFix (_,fl))::tl) ->
1098 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1099 let len = List.length fl in
1100 let n_plus_len = n + len
1101 and nn_plus_len = nn + len
1102 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1103 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1106 i && does_not_occur context n nn ty &&
1107 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1108 args coInductiveTypeURI
1110 | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1111 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1112 does_not_occur context n nn out &&
1113 does_not_occur context n nn te &&
1117 guarded_by_constructors context n nn h x args coInductiveTypeURI
1120 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1121 | C.Var (_,exp_named_subst)
1122 | C.Const (_,exp_named_subst) ->
1124 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1125 | C.MutInd _ -> assert false
1126 | C.MutConstruct (_,_,_,exp_named_subst) ->
1128 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1129 | C.MutCase (_,_,out,te,pl) ->
1130 does_not_occur context n nn out &&
1131 does_not_occur context n nn te &&
1135 guarded_by_constructors context n nn h x args coInductiveTypeURI
1138 let len = List.length fl in
1139 let n_plus_len = n + len
1140 and nn_plus_len = nn + len
1141 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1142 and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1144 (fun (_,_,ty,bo) i ->
1145 i && does_not_occur context n nn ty &&
1146 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1149 let len = List.length fl in
1150 let n_plus_len = n + len
1151 and nn_plus_len = nn + len
1152 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1153 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1156 i && does_not_occur context n nn ty &&
1157 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1158 args coInductiveTypeURI
1161 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1162 let module C = Cic in
1163 let module U = UriManager in
1164 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1165 (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1166 when CicReduction.are_convertible context so1 so2 ->
1167 check_allowed_sort_elimination context uri i need_dummy
1168 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1169 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1170 | (C.Sort C.Prop, C.Sort C.Set)
1171 | (C.Sort C.Prop, C.Sort C.CProp)
1172 | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
1173 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1174 (match CicEnvironment.get_obj uri with
1175 C.InductiveDefinition (itl,_,_) ->
1176 let (_,_,_,cl) = List.nth itl i in
1177 (* is a singleton definition or the empty proposition? *)
1178 List.length cl = 1 || List.length cl = 0
1180 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1181 UriManager.string_of_uri uri))
1183 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1184 | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true
1185 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1186 | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
1187 | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
1188 | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
1189 | ((C.Sort C.Set, C.Sort C.Type) | (C.Sort C.CProp, C.Sort C.Type))
1191 (match CicEnvironment.get_obj uri with
1192 C.InductiveDefinition (itl,_,paramsno) ->
1194 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1196 let (_,_,_,cl) = List.nth itl i in
1198 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1200 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1201 UriManager.string_of_uri uri))
1203 | (C.Sort C.Type, C.Sort _) when need_dummy -> true
1204 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1205 let res = CicReduction.are_convertible context so ind
1208 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1209 C.Sort C.Prop -> true
1210 | (C.Sort C.Set | C.Sort C.CProp) ->
1211 (match CicEnvironment.get_obj uri with
1212 C.InductiveDefinition (itl,_,_) ->
1213 let (_,_,_,cl) = List.nth itl i in
1214 (* is a singleton definition? *)
1217 raise (TypeCheckerFailure
1218 ("Unknown mutual inductive definition:" ^
1219 UriManager.string_of_uri uri))
1223 | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
1224 when not need_dummy ->
1225 let res = CicReduction.are_convertible context so ind
1228 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1230 | C.Sort C.Set -> true
1231 | C.Sort C.CProp -> true
1233 (match CicEnvironment.get_obj uri with
1234 C.InductiveDefinition (itl,_,paramsno) ->
1235 let (_,_,_,cl) = List.nth itl i in
1238 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1241 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1243 raise (TypeCheckerFailure
1244 ("Unknown mutual inductive definition:" ^
1245 UriManager.string_of_uri uri))
1247 | _ -> raise (AssertFailure "19")
1249 | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
1250 CicReduction.are_convertible context so ind
1253 and type_of_branch context argsno need_dummy outtype term constype =
1254 let module C = Cic in
1255 let module R = CicReduction in
1256 match R.whd context constype with
1261 C.Appl [outtype ; term]
1262 | C.Appl (C.MutInd (_,_,_)::tl) ->
1263 let (_,arguments) = split tl argsno
1265 if need_dummy && arguments = [] then
1268 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1269 | C.Prod (name,so,de) ->
1271 match CicSubstitution.lift 1 term with
1272 C.Appl l -> C.Appl (l@[C.Rel 1])
1273 | t -> C.Appl [t ; C.Rel 1]
1275 C.Prod (C.Anonymous,so,type_of_branch
1276 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1277 (CicSubstitution.lift 1 outtype) term' de)
1278 | _ -> raise (AssertFailure "20")
1280 (* check_metasenv_consistency checks that the "canonical" context of a
1281 metavariable is consitent - up to relocation via the relocation list l -
1282 with the actual context *)
1284 and check_metasenv_consistency metasenv context canonical_context l =
1285 let module C = Cic in
1286 let module R = CicReduction in
1287 let module S = CicSubstitution in
1288 let lifted_canonical_context =
1292 | (Some (n,C.Decl t))::tl ->
1293 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1294 | (Some (n,C.Def (t,None)))::tl ->
1295 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1296 | None::tl -> None::(aux (i+1) tl)
1297 | (Some (n,C.Def (_,Some _)))::_ -> assert false
1299 aux 1 canonical_context
1305 | Some t,Some (_,C.Def (ct,_)) ->
1306 if not (R.are_convertible context t ct) then
1307 raise (TypeCheckerFailure (sprintf
1308 "Not well typed metavariable local context: expected a term convertible with %s, found %s"
1309 (CicPp.ppterm ct) (CicPp.ppterm t)))
1310 | Some t,Some (_,C.Decl ct) ->
1311 let type_t = type_of_aux' metasenv context t in
1312 if not (R.are_convertible context type_t ct) then
1313 raise (TypeCheckerFailure (sprintf
1314 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1315 (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
1317 raise (TypeCheckerFailure
1318 "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
1319 ) l lifted_canonical_context
1321 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1322 and type_of_aux' metasenv context t =
1323 let rec type_of_aux context =
1324 let module C = Cic in
1325 let module R = CicReduction in
1326 let module S = CicSubstitution in
1327 let module U = UriManager in
1331 match List.nth context (n - 1) with
1332 Some (_,C.Decl t) -> S.lift n t
1333 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
1334 | Some (_,C.Def (bo,None)) ->
1335 debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1336 type_of_aux context (S.lift n bo)
1337 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
1340 raise (TypeCheckerFailure
1341 "unbound variable found in constructor type")
1343 | C.Var (uri,exp_named_subst) ->
1345 check_exp_named_subst context exp_named_subst ;
1347 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1352 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1353 check_metasenv_consistency metasenv context canonical_context l;
1354 CicSubstitution.lift_meta l ty
1355 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1356 | C.Implicit -> raise (AssertFailure "21")
1357 | C.Cast (te,ty) as t ->
1358 let _ = type_of_aux context ty in
1359 if R.are_convertible context (type_of_aux context te) ty then
1362 raise (TypeCheckerFailure
1363 (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1364 | C.Prod (name,s,t) ->
1365 let sort1 = type_of_aux context s
1366 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1367 sort_of_prod context (name,s) (sort1,sort2)
1368 | C.Lambda (n,s,t) ->
1369 let sort1 = type_of_aux context s
1370 and type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1371 let sort2 = type_of_aux ((Some (n,(C.Decl s)))::context) type2 in
1372 (* only to check if the product is well-typed *)
1373 let _ = sort_of_prod context (n,s) (sort1,sort2) in
1375 | C.LetIn (n,s,t) ->
1376 (* only to check if s is well-typed *)
1377 let ty = type_of_aux context s in
1378 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1379 LetIn is later reduced and maybe also re-checked.
1380 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1382 (* The type of the LetIn is reduced. Much faster than the previous
1383 solution. Moreover the inferred type is probably very different
1384 from the expected one.
1385 (CicReduction.whd context
1386 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1388 (* One-step LetIn reduction. Even faster than the previous solution.
1389 Moreover the inferred type is closer to the expected one. *)
1390 (CicSubstitution.subst s
1391 (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
1392 | C.Appl (he::tl) when List.length tl > 0 ->
1393 let hetype = type_of_aux context he
1394 and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1395 eat_prods context hetype tlbody_and_type
1396 | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1397 | C.Const (uri,exp_named_subst) ->
1399 check_exp_named_subst context exp_named_subst ;
1401 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1405 | C.MutInd (uri,i,exp_named_subst) ->
1407 check_exp_named_subst context exp_named_subst ;
1409 CicSubstitution.subst_vars exp_named_subst
1410 (type_of_mutual_inductive_defs uri i)
1414 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1415 check_exp_named_subst context exp_named_subst ;
1417 CicSubstitution.subst_vars exp_named_subst
1418 (type_of_mutual_inductive_constr uri i j)
1421 | C.MutCase (uri,i,outtype,term,pl) ->
1422 let outsort = type_of_aux context outtype in
1423 let (need_dummy, k) =
1424 let rec guess_args context t =
1425 let outtype = CicReduction.whd context t in
1427 C.Sort _ -> (true, 0)
1428 | C.Prod (name, s, t) ->
1429 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1431 (* last prod before sort *)
1432 match CicReduction.whd context s with
1433 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1434 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1436 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1437 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1438 when U.eq uri' uri && i' = i -> (false, 1)
1443 raise (TypeCheckerFailure (sprintf
1444 "Malformed case analasys' output type %s" (CicPp.ppterm outtype)))
1446 (*CSC whd non serve dopo type_of_aux ? *)
1447 let (b, k) = guess_args context outsort in
1448 if not b then (b, k - 1) else (b, k)
1450 let (parameters, arguments, exp_named_subst) =
1451 match R.whd context (type_of_aux context term) with
1452 (*CSC manca il caso dei CAST *)
1453 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1454 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
1455 (*CSC: Hint: nella DTD servono per gli stylesheet. *)
1456 C.MutInd (uri',i',exp_named_subst) as typ ->
1457 if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1458 else raise (TypeCheckerFailure (sprintf
1459 "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1460 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1461 | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1462 if U.eq uri uri' && i = i' then
1464 split tl (List.length tl - k)
1465 in params,args,exp_named_subst
1466 else raise (TypeCheckerFailure (sprintf
1467 "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1468 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1470 raise (TypeCheckerFailure (sprintf
1471 "Case analysis: analysed term %s is not an inductive one"
1472 (CicPp.ppterm term)))
1474 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1475 let sort_of_ind_type =
1476 if parameters = [] then
1477 C.MutInd (uri,i,exp_named_subst)
1479 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1481 if not (check_allowed_sort_elimination context uri i need_dummy
1482 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1485 (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1486 (* let's check if the type of branches are right *)
1488 match CicEnvironment.get_cooked_obj ~trust:false uri with
1489 C.InductiveDefinition (_,_,parsno) -> parsno
1491 raise (TypeCheckerFailure
1492 ("Unknown mutual inductive definition:" ^
1493 UriManager.string_of_uri uri))
1495 let (_,branches_ok) =
1499 if parameters = [] then
1500 (C.MutConstruct (uri,i,j,exp_named_subst))
1502 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1509 R.are_convertible context (type_of_aux context p)
1510 (type_of_branch context parsno need_dummy outtype cons
1511 (type_of_aux context cons))
1512 in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res
1516 if not branches_ok then
1518 (TypeCheckerFailure "Case analysys: wrong branch type");
1519 if not need_dummy then
1520 C.Appl ((outtype::arguments)@[term])
1521 else if arguments = [] then
1524 C.Appl (outtype::arguments)
1526 let types_times_kl =
1530 let _ = type_of_aux context ty in
1531 (Some (C.Name n,(C.Decl ty)),k)) fl)
1533 let (types,kl) = List.split types_times_kl in
1534 let len = List.length types in
1536 (fun (name,x,ty,bo) ->
1538 (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1539 (CicSubstitution.lift len ty))
1542 let (m, eaten, context') =
1543 eat_lambdas (types @ context) (x + 1) bo
1545 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1548 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1551 (TypeCheckerFailure ("Fix: not guarded by destructors"))
1554 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1557 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1558 let (_,_,ty,_) = List.nth fl i in
1565 let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1567 let len = List.length types in
1571 (R.are_convertible (types @ context)
1572 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1575 (* let's control that the returned type is coinductive *)
1576 match returns_a_coinductive context ty with
1580 ("CoFix: does not return a coinductive type"))
1582 (*let's control the guarded by constructors conditions C{f,M}*)
1585 (guarded_by_constructors (types @ context) 0 len false bo
1589 (TypeCheckerFailure ("CoFix: not guarded by constructors"))
1593 (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1596 let (_,ty,_) = List.nth fl i in
1599 and check_exp_named_subst context =
1600 let rec check_exp_named_subst_aux substs =
1603 | ((uri,t) as subst)::tl ->
1605 CicSubstitution.subst_vars substs (type_of_variable uri) in
1606 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1607 Cic.Variable (_,Some bo,_,_) ->
1610 ("A variable with a body can not be explicit substituted"))
1611 | Cic.Variable (_,None,_,_) -> ()
1613 raise (TypeCheckerFailure
1614 ("Unknown mutual inductive definition:" ^
1615 UriManager.string_of_uri uri))
1617 let typeoft = type_of_aux context t in
1618 if CicReduction.are_convertible context typeoft typeofvar then
1619 check_exp_named_subst_aux (substs@[subst]) tl
1622 CicReduction.fdebug := 0 ;
1623 ignore (CicReduction.are_convertible context typeoft typeofvar) ;
1625 debug typeoft [typeofvar] ;
1626 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1629 check_exp_named_subst_aux []
1631 and sort_of_prod context (name,s) (t1, t2) =
1632 let module C = Cic in
1633 let t1' = CicReduction.whd context t1 in
1634 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1635 match (t1', t2') with
1636 (C.Sort s1, C.Sort s2)
1637 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
1639 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1640 | (_,_) -> raise (TypeCheckerFailure (sprintf
1641 "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1642 (CicPp.ppterm t2')))
1644 and eat_prods context hetype =
1645 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1649 | (hete, hety)::tl ->
1650 (match (CicReduction.whd context hetype) with
1652 if CicReduction.are_convertible context s hety then
1653 (CicReduction.fdebug := -1 ;
1654 eat_prods context (CicSubstitution.subst hete t) tl
1658 CicReduction.fdebug := 0 ;
1659 ignore (CicReduction.are_convertible context s hety) ;
1662 raise (TypeCheckerFailure (sprintf
1663 "Appl: wrong parameter-type, expected %s, found %s"
1664 (CicPp.ppterm hetype) (CicPp.ppterm s)))
1667 raise (TypeCheckerFailure
1668 "Appl: this is not a function, it cannot be applied")
1671 and returns_a_coinductive context ty =
1672 let module C = Cic in
1673 match CicReduction.whd context ty with
1674 C.MutInd (uri,i,_) ->
1675 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1676 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1677 C.InductiveDefinition (itl,_,_) ->
1678 let (_,is_inductive,_,_) = List.nth itl i in
1679 if is_inductive then None else (Some uri)
1681 raise (TypeCheckerFailure
1682 ("Unknown mutual inductive definition:" ^
1683 UriManager.string_of_uri uri))
1685 | C.Appl ((C.MutInd (uri,i,_))::_) ->
1686 (match CicEnvironment.get_obj uri with
1687 C.InductiveDefinition (itl,_,_) ->
1688 let (_,is_inductive,_,_) = List.nth itl i in
1689 if is_inductive then None else (Some uri)
1691 raise (TypeCheckerFailure
1692 ("Unknown mutual inductive definition:" ^
1693 UriManager.string_of_uri uri))
1695 | C.Prod (n,so,de) ->
1696 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1701 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1704 type_of_aux context t
1706 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
1709 (* is a small constructor? *)
1710 (*CSC: ottimizzare calcolando staticamente *)
1711 and is_small context paramsno c =
1712 let rec is_small_aux context c =
1713 let module C = Cic in
1714 match CicReduction.whd context c with
1716 (*CSC: [] is an empty metasenv. Is it correct? *)
1717 let s = type_of_aux' [] context so in
1718 (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
1719 is_small_aux ((Some (n,(C.Decl so)))::context) de
1720 | _ -> true (*CSC: we trust the type-checker *)
1722 let (context',dx) = split_prods context paramsno c in
1723 is_small_aux context' dx
1727 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1730 type_of_aux' [] [] t
1732 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
1737 let module C = Cic in
1738 let module R = CicReduction in
1739 let module U = UriManager in
1740 match CicEnvironment.is_type_checked ~trust:false uri with
1741 CicEnvironment.CheckedObj _ -> ()
1742 | CicEnvironment.UncheckedObj uobj ->
1743 (* let's typecheck the uncooked object *)
1744 CicLogger.log (`Start_type_checking uri) ;
1746 C.Constant (_,Some te,ty,_) ->
1747 let _ = type_of ty in
1748 if not (R.are_convertible [] (type_of te ) ty) then
1749 raise (TypeCheckerFailure
1750 ("Unknown constant:" ^ U.string_of_uri uri))
1751 | C.Constant (_,None,ty,_) ->
1752 (* only to check that ty is well-typed *)
1753 let _ = type_of ty in ()
1754 | C.CurrentProof (_,conjs,te,ty,_) ->
1757 (fun metasenv ((_,context,ty) as conj) ->
1758 ignore (type_of_aux' metasenv context ty) ;
1762 let _ = type_of_aux' conjs [] ty in
1763 let type_of_te = type_of_aux' conjs [] te in
1764 if not (R.are_convertible [] type_of_te ty)
1766 raise (TypeCheckerFailure (sprintf
1767 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
1768 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
1770 | C.Variable (_,bo,ty,_) ->
1771 (* only to check that ty is well-typed *)
1772 let _ = type_of ty in
1776 if not (R.are_convertible [] (type_of bo) ty) then
1777 raise (TypeCheckerFailure
1778 ("Unknown variable:" ^ U.string_of_uri uri))
1780 | C.InductiveDefinition _ ->
1781 check_mutual_inductive_defs uri uobj
1783 CicEnvironment.set_type_checking_info uri ;
1784 CicLogger.log (`Type_checking_completed uri)