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')
634 | (_, _) -> raise (AssertFailure "9")
636 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
637 and check_is_really_smaller_arg context n nn kl x safes te =
638 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
639 (*CSC: cfr guarded_by_destructors *)
640 let module C = Cic in
641 let module U = UriManager in
642 match CicReduction.whd context te with
643 C.Rel m when List.mem m safes -> true
650 (* | C.Cast (te,ty) ->
651 check_is_really_smaller_arg n nn kl x safes te &&
652 check_is_really_smaller_arg n nn kl x safes ty*)
653 (* | C.Prod (_,so,ta) ->
654 check_is_really_smaller_arg n nn kl x safes so &&
655 check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
656 (List.map (fun x -> x + 1) safes) ta*)
657 | C.Prod _ -> raise (AssertFailure "10")
658 | C.Lambda (name,so,ta) ->
659 check_is_really_smaller_arg context n nn kl x safes so &&
660 check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context)
661 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
662 | C.LetIn (name,so,ta) ->
663 check_is_really_smaller_arg context n nn kl x safes so &&
664 check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::context)
665 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
667 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
668 (*CSC: solo perche' non abbiamo trovato controesempi *)
669 check_is_really_smaller_arg context n nn kl x safes he
670 | C.Appl [] -> raise (AssertFailure "11")
672 | C.MutInd _ -> raise (AssertFailure "12")
673 | C.MutConstruct _ -> false
674 | C.MutCase (uri,i,outtype,term,pl) ->
676 C.Rel m when List.mem m safes || m = x ->
677 let (tys,len,isinductive,paramsno,cl) =
678 match CicEnvironment.get_obj uri with
679 C.InductiveDefinition (tl,_,paramsno) ->
682 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
684 let (_,isinductive,_,cl) = List.nth tl i in
688 (id, snd (split_prods tys paramsno ty))) cl
690 (tys,List.length tl,isinductive,paramsno,cl')
692 raise (TypeCheckerFailure
693 ("Unknown mutual inductive definition:" ^
694 UriManager.string_of_uri uri))
696 if not isinductive then
699 i && check_is_really_smaller_arg context n nn kl x safes p)
705 let debrujinedte = debrujin_constructor uri len c in
706 recursive_args tys 0 len debrujinedte
708 let (e,safes',n',nn',x',context') =
709 get_new_safes context p c rl' safes n nn x
712 check_is_really_smaller_arg context' n' nn' kl x' safes' e
713 ) (List.combine pl cl) true
714 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
715 let (tys,len,isinductive,paramsno,cl) =
716 match CicEnvironment.get_obj uri with
717 C.InductiveDefinition (tl,_,paramsno) ->
718 let (_,isinductive,_,cl) = List.nth tl i in
720 List.map (fun (n,_,ty,_) ->
721 Some(Cic.Name n,(Cic.Decl ty))) tl
726 (id, snd (split_prods tys paramsno ty))) cl
728 (tys,List.length tl,isinductive,paramsno,cl')
730 raise (TypeCheckerFailure
731 ("Unknown mutual inductive definition:" ^
732 UriManager.string_of_uri uri))
734 if not isinductive then
737 i && check_is_really_smaller_arg context n nn kl x safes p)
740 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
741 (*CSC: sugli argomenti di una applicazione *)
745 let debrujinedte = debrujin_constructor uri len c in
746 recursive_args tys 0 len debrujinedte
748 let (e, safes',n',nn',x',context') =
749 get_new_safes context p c rl' safes n nn x
752 check_is_really_smaller_arg context' n' nn' kl x' safes' e
753 ) (List.combine pl cl) true
757 i && check_is_really_smaller_arg context n nn kl x safes p
761 let len = List.length fl in
762 let n_plus_len = n + len
763 and nn_plus_len = nn + len
764 and x_plus_len = x + len
765 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
766 and safes' = List.map (fun x -> x + len) safes in
768 (fun (_,_,ty,bo) i ->
770 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
774 let len = List.length fl in
775 let n_plus_len = n + len
776 and nn_plus_len = nn + len
777 and x_plus_len = x + len
778 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
779 and safes' = List.map (fun x -> x + len) safes in
783 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
787 and guarded_by_destructors context n nn kl x safes =
788 let module C = Cic in
789 let module U = UriManager in
791 C.Rel m when m > n && m <= nn -> false
793 (match List.nth context (n-1) with
794 Some (_,C.Decl _) -> true
795 | Some (_,C.Def (bo,_)) ->
796 guarded_by_destructors context n nn kl x safes bo
797 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
803 guarded_by_destructors context n nn kl x safes te &&
804 guarded_by_destructors context n nn kl x safes ty
805 | C.Prod (name,so,ta) ->
806 guarded_by_destructors context n nn kl x safes so &&
807 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
808 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
809 | C.Lambda (name,so,ta) ->
810 guarded_by_destructors context n nn kl x safes so &&
811 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
812 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
813 | C.LetIn (name,so,ta) ->
814 guarded_by_destructors context n nn kl x safes so &&
815 guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
816 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
817 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
818 let k = List.nth kl (m - n - 1) in
819 if not (List.length tl > k) then false
823 i && guarded_by_destructors context n nn kl x safes param
825 check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
828 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
830 | C.Var (_,exp_named_subst)
831 | C.Const (_,exp_named_subst)
832 | C.MutInd (_,_,exp_named_subst)
833 | C.MutConstruct (_,_,_,exp_named_subst) ->
835 (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
837 | C.MutCase (uri,i,outtype,term,pl) ->
839 C.Rel m when List.mem m safes || m = x ->
840 let (tys,len,isinductive,paramsno,cl) =
841 match CicEnvironment.get_obj uri with
842 C.InductiveDefinition (tl,_,paramsno) ->
843 let (_,isinductive,_,cl) = List.nth tl i in
845 List.map (fun (n,_,ty,_) ->
846 Some(Cic.Name n,(Cic.Decl ty))) tl
851 (id, snd (split_prods tys paramsno ty))) cl
853 (tys,List.length tl,isinductive,paramsno,cl')
855 raise (TypeCheckerFailure
856 ("Unknown mutual inductive definition:" ^
857 UriManager.string_of_uri uri))
859 if not isinductive then
860 guarded_by_destructors context n nn kl x safes outtype &&
861 guarded_by_destructors context n nn kl x safes term &&
862 (*CSC: manca ??? il controllo sul tipo di term? *)
865 i && guarded_by_destructors context n nn kl x safes p)
868 guarded_by_destructors context n nn kl x safes outtype &&
869 (*CSC: manca ??? il controllo sul tipo di term? *)
873 let debrujinedte = debrujin_constructor uri len c in
874 recursive_args tys 0 len debrujinedte
876 let (e,safes',n',nn',x',context') =
877 get_new_safes context p c rl' safes n nn x
880 guarded_by_destructors context' n' nn' kl x' safes' e
881 ) (List.combine pl cl) true
882 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
883 let (tys,len,isinductive,paramsno,cl) =
884 match CicEnvironment.get_obj uri with
885 C.InductiveDefinition (tl,_,paramsno) ->
886 let (_,isinductive,_,cl) = List.nth tl i in
889 (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
894 (id, snd (split_prods tys paramsno ty))) cl
896 (tys,List.length tl,isinductive,paramsno,cl')
898 raise (TypeCheckerFailure
899 ("Unknown mutual inductive definition:" ^
900 UriManager.string_of_uri uri))
902 if not isinductive then
903 guarded_by_destructors context n nn kl x safes outtype &&
904 guarded_by_destructors context n nn kl x safes term &&
905 (*CSC: manca ??? il controllo sul tipo di term? *)
908 i && guarded_by_destructors context n nn kl x safes p)
911 guarded_by_destructors context n nn kl x safes outtype &&
912 (*CSC: manca ??? il controllo sul tipo di term? *)
915 i && guarded_by_destructors context n nn kl x safes t)
920 let debrujinedte = debrujin_constructor uri len c in
921 recursive_args tys 0 len debrujinedte
923 let (e, safes',n',nn',x',context') =
924 get_new_safes context p c rl' safes n nn x
927 guarded_by_destructors context' n' nn' kl x' safes' e
928 ) (List.combine pl cl) true
930 guarded_by_destructors context n nn kl x safes outtype &&
931 guarded_by_destructors context n nn kl x safes term &&
932 (*CSC: manca ??? il controllo sul tipo di term? *)
934 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
938 let len = List.length fl in
939 let n_plus_len = n + len
940 and nn_plus_len = nn + len
941 and x_plus_len = x + len
942 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
943 and safes' = List.map (fun x -> x + len) safes in
945 (fun (_,_,ty,bo) i ->
946 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
947 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
951 let len = List.length fl in
952 let n_plus_len = n + len
953 and nn_plus_len = nn + len
954 and x_plus_len = x + len
955 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
956 and safes' = List.map (fun x -> x + len) safes in
960 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
961 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
965 (* the boolean h means already protected *)
966 (* args is the list of arguments the type of the constructor that may be *)
967 (* found in head position must be applied to. *)
968 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
969 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
970 let module C = Cic in
971 (*CSC: There is a lot of code replication between the cases X and *)
972 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
973 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
974 match CicReduction.whd context te with
975 C.Rel m when m > n && m <= nn -> h
983 (* the term has just been type-checked *)
984 raise (AssertFailure "17")
985 | C.Lambda (name,so,de) ->
986 does_not_occur context n nn so &&
987 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
988 (n + 1) (nn + 1) h de args coInductiveTypeURI
989 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
991 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
992 | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
994 match CicEnvironment.get_cooked_obj ~trust:false uri with
995 C.InductiveDefinition (itl,_,_) ->
996 let (_,_,_,cl) = List.nth itl i in
997 let (_,cons) = List.nth cl (j - 1) in
998 CicSubstitution.subst_vars exp_named_subst cons
1000 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1001 UriManager.string_of_uri uri))
1003 let rec analyse_branch context ty te =
1004 match CicReduction.whd context ty with
1005 C.Meta _ -> raise (AssertFailure "34")
1009 does_not_occur context n nn te
1012 raise (AssertFailure "24")(* due to type-checking *)
1013 | C.Prod (name,so,de) ->
1014 analyse_branch ((Some (name,(C.Decl so)))::context) de te
1017 raise (AssertFailure "25")(* due to type-checking *)
1018 | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1019 when uri == coInductiveTypeURI ->
1020 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1021 | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1022 guarded_by_constructors context n nn true te tl coInductiveTypeURI
1024 does_not_occur context n nn te
1025 | C.Const _ -> raise (AssertFailure "26")
1026 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1027 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1029 does_not_occur context n nn te
1030 | C.MutConstruct _ -> raise (AssertFailure "27")
1031 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1032 (*CSC: in head position. *)
1036 raise (AssertFailure "28")(* due to type-checking *)
1038 let rec analyse_instantiated_type context ty l =
1039 match CicReduction.whd context ty with
1045 | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1046 | C.Prod (name,so,de) ->
1051 analyse_branch context so he &&
1052 analyse_instantiated_type
1053 ((Some (name,(C.Decl so)))::context) de tl
1057 raise (AssertFailure "30")(* due to type-checking *)
1060 (fun i x -> i && does_not_occur context n nn x) true l
1061 | C.Const _ -> raise (AssertFailure "31")
1064 (fun i x -> i && does_not_occur context n nn x) true l
1065 | C.MutConstruct _ -> raise (AssertFailure "32")
1066 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1067 (*CSC: in head position. *)
1071 raise (AssertFailure "33")(* due to type-checking *)
1073 let rec instantiate_type args consty =
1076 | tlhe::tltl as l ->
1077 let consty' = CicReduction.whd context consty in
1083 let instantiated_de = CicSubstitution.subst he de in
1084 (*CSC: siamo sicuri che non sia troppo forte? *)
1085 does_not_occur context n nn tlhe &
1086 instantiate_type tl instantiated_de tltl
1088 (*CSC:We do not consider backbones with a MutCase, a *)
1089 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1090 raise (AssertFailure "23")
1092 | [] -> analyse_instantiated_type context consty' l
1093 (* These are all the other cases *)
1095 instantiate_type args consty tl
1096 | C.Appl ((C.CoFix (_,fl))::tl) ->
1097 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1098 let len = List.length fl in
1099 let n_plus_len = n + len
1100 and nn_plus_len = nn + len
1101 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1102 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1105 i && does_not_occur context n nn ty &&
1106 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1107 args coInductiveTypeURI
1109 | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1110 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1111 does_not_occur context n nn out &&
1112 does_not_occur context n nn te &&
1116 guarded_by_constructors context n nn h x args coInductiveTypeURI
1119 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1120 | C.Var (_,exp_named_subst)
1121 | C.Const (_,exp_named_subst) ->
1123 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1124 | C.MutInd _ -> assert false
1125 | C.MutConstruct (_,_,_,exp_named_subst) ->
1127 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1128 | C.MutCase (_,_,out,te,pl) ->
1129 does_not_occur context n nn out &&
1130 does_not_occur context n nn te &&
1134 guarded_by_constructors context n nn h x args coInductiveTypeURI
1137 let len = List.length fl in
1138 let n_plus_len = n + len
1139 and nn_plus_len = nn + len
1140 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1141 and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1143 (fun (_,_,ty,bo) i ->
1144 i && does_not_occur context n nn ty &&
1145 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1148 let len = List.length fl in
1149 let n_plus_len = n + len
1150 and nn_plus_len = nn + len
1151 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1152 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1155 i && does_not_occur context n nn ty &&
1156 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1157 args coInductiveTypeURI
1160 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1161 let module C = Cic in
1162 let module U = UriManager in
1163 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1164 (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1165 when CicReduction.are_convertible context so1 so2 ->
1166 check_allowed_sort_elimination context uri i need_dummy
1167 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1168 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1169 | (C.Sort C.Prop, C.Sort C.Set)
1170 | (C.Sort C.Prop, C.Sort C.CProp)
1171 | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
1172 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1173 (match CicEnvironment.get_obj uri with
1174 C.InductiveDefinition (itl,_,_) ->
1175 let (_,_,_,cl) = List.nth itl i in
1176 (* is a singleton definition or the empty proposition? *)
1177 List.length cl = 1 || List.length cl = 0
1179 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1180 UriManager.string_of_uri uri))
1182 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1183 | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true
1184 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1185 | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
1186 | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
1187 | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
1188 | ((C.Sort C.Set, C.Sort C.Type) | (C.Sort C.CProp, C.Sort C.Type))
1190 (match CicEnvironment.get_obj uri with
1191 C.InductiveDefinition (itl,_,paramsno) ->
1193 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1195 let (_,_,_,cl) = List.nth itl i in
1197 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1199 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1200 UriManager.string_of_uri uri))
1202 | (C.Sort C.Type, C.Sort _) when need_dummy -> true
1203 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1204 let res = CicReduction.are_convertible context so ind
1207 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1208 C.Sort C.Prop -> true
1209 | (C.Sort C.Set | C.Sort C.CProp) ->
1210 (match CicEnvironment.get_obj uri with
1211 C.InductiveDefinition (itl,_,_) ->
1212 let (_,_,_,cl) = List.nth itl i in
1213 (* is a singleton definition? *)
1216 raise (TypeCheckerFailure
1217 ("Unknown mutual inductive definition:" ^
1218 UriManager.string_of_uri uri))
1222 | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
1223 when not need_dummy ->
1224 let res = CicReduction.are_convertible context so ind
1227 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1229 | C.Sort C.Set -> true
1230 | C.Sort C.CProp -> true
1232 (match CicEnvironment.get_obj uri with
1233 C.InductiveDefinition (itl,_,paramsno) ->
1234 let (_,_,_,cl) = List.nth itl i in
1237 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1240 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1242 raise (TypeCheckerFailure
1243 ("Unknown mutual inductive definition:" ^
1244 UriManager.string_of_uri uri))
1246 | _ -> raise (AssertFailure "19")
1248 | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
1249 CicReduction.are_convertible context so ind
1252 and type_of_branch context argsno need_dummy outtype term constype =
1253 let module C = Cic in
1254 let module R = CicReduction in
1255 match R.whd context constype with
1260 C.Appl [outtype ; term]
1261 | C.Appl (C.MutInd (_,_,_)::tl) ->
1262 let (_,arguments) = split tl argsno
1264 if need_dummy && arguments = [] then
1267 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1268 | C.Prod (name,so,de) ->
1270 match CicSubstitution.lift 1 term with
1271 C.Appl l -> C.Appl (l@[C.Rel 1])
1272 | t -> C.Appl [t ; C.Rel 1]
1274 C.Prod (C.Anonymous,so,type_of_branch
1275 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1276 (CicSubstitution.lift 1 outtype) term' de)
1277 | _ -> raise (AssertFailure "20")
1279 (* check_metasenv_consistency checks that the "canonical" context of a
1280 metavariable is consitent - up to relocation via the relocation list l -
1281 with the actual context *)
1283 and check_metasenv_consistency metasenv context canonical_context l =
1284 let module C = Cic in
1285 let module R = CicReduction in
1286 let module S = CicSubstitution in
1287 let lifted_canonical_context =
1291 | (Some (n,C.Decl t))::tl ->
1292 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1293 | (Some (n,C.Def (t,None)))::tl ->
1294 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1295 | None::tl -> None::(aux (i+1) tl)
1296 | (Some (n,C.Def (_,Some _)))::_ -> assert false
1298 aux 1 canonical_context
1304 | Some t,Some (_,C.Def (ct,_)) ->
1305 if not (R.are_convertible context t ct) then
1306 raise (TypeCheckerFailure (sprintf
1307 "Not well typed metavariable local context: expected a term convertible with %s, found %s"
1308 (CicPp.ppterm ct) (CicPp.ppterm t)))
1309 | Some t,Some (_,C.Decl ct) ->
1310 let type_t = type_of_aux' metasenv context t in
1311 if not (R.are_convertible context type_t ct) then
1312 raise (TypeCheckerFailure (sprintf
1313 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1314 (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
1316 raise (TypeCheckerFailure
1317 "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
1318 ) l lifted_canonical_context
1320 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1321 and type_of_aux' metasenv context t =
1322 let rec type_of_aux context =
1323 let module C = Cic in
1324 let module R = CicReduction in
1325 let module S = CicSubstitution in
1326 let module U = UriManager in
1330 match List.nth context (n - 1) with
1331 Some (_,C.Decl t) -> S.lift n t
1332 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
1333 | Some (_,C.Def (bo,None)) ->
1334 debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1335 type_of_aux context (S.lift n bo)
1336 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
1339 raise (TypeCheckerFailure
1340 "unbound variable found in constructor type")
1342 | C.Var (uri,exp_named_subst) ->
1344 check_exp_named_subst context exp_named_subst ;
1346 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1351 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1352 check_metasenv_consistency metasenv context canonical_context l;
1353 CicSubstitution.lift_meta l ty
1354 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1355 | C.Implicit -> raise (AssertFailure "21")
1356 | C.Cast (te,ty) as t ->
1357 let _ = type_of_aux context ty in
1358 if R.are_convertible context (type_of_aux context te) ty then
1361 raise (TypeCheckerFailure
1362 (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1363 | C.Prod (name,s,t) ->
1364 let sort1 = type_of_aux context s
1365 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1366 sort_of_prod context (name,s) (sort1,sort2)
1367 | C.Lambda (n,s,t) ->
1368 let sort1 = type_of_aux context s
1369 and type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1370 let sort2 = type_of_aux ((Some (n,(C.Decl s)))::context) type2 in
1371 (* only to check if the product is well-typed *)
1372 let _ = sort_of_prod context (n,s) (sort1,sort2) in
1374 | C.LetIn (n,s,t) ->
1375 (* only to check if s is well-typed *)
1376 let ty = type_of_aux context s in
1377 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1378 LetIn is later reduced and maybe also re-checked.
1379 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1381 (* The type of the LetIn is reduced. Much faster than the previous
1382 solution. Moreover the inferred type is probably very different
1383 from the expected one.
1384 (CicReduction.whd context
1385 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1387 (* One-step LetIn reduction. Even faster than the previous solution.
1388 Moreover the inferred type is closer to the expected one. *)
1389 (CicSubstitution.subst s
1390 (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
1391 | C.Appl (he::tl) when List.length tl > 0 ->
1392 let hetype = type_of_aux context he
1393 and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1394 eat_prods context hetype tlbody_and_type
1395 | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1396 | C.Const (uri,exp_named_subst) ->
1398 check_exp_named_subst context exp_named_subst ;
1400 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1404 | C.MutInd (uri,i,exp_named_subst) ->
1406 check_exp_named_subst context exp_named_subst ;
1408 CicSubstitution.subst_vars exp_named_subst
1409 (type_of_mutual_inductive_defs uri i)
1413 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1414 check_exp_named_subst context exp_named_subst ;
1416 CicSubstitution.subst_vars exp_named_subst
1417 (type_of_mutual_inductive_constr uri i j)
1420 | C.MutCase (uri,i,outtype,term,pl) ->
1421 let outsort = type_of_aux context outtype in
1422 let (need_dummy, k) =
1423 let rec guess_args context t =
1424 let outtype = CicReduction.whd context t in
1426 C.Sort _ -> (true, 0)
1427 | C.Prod (name, s, t) ->
1428 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1430 (* last prod before sort *)
1431 match CicReduction.whd context s with
1432 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1433 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1435 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1436 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1437 when U.eq uri' uri && i' = i -> (false, 1)
1442 raise (TypeCheckerFailure (sprintf
1443 "Malformed case analasys' output type %s" (CicPp.ppterm outtype)))
1445 (*CSC whd non serve dopo type_of_aux ? *)
1446 let (b, k) = guess_args context outsort in
1447 if not b then (b, k - 1) else (b, k)
1449 let (parameters, arguments, exp_named_subst) =
1450 match R.whd context (type_of_aux context term) with
1451 (*CSC manca il caso dei CAST *)
1452 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1453 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
1454 (*CSC: Hint: nella DTD servono per gli stylesheet. *)
1455 C.MutInd (uri',i',exp_named_subst) as typ ->
1456 if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1457 else raise (TypeCheckerFailure (sprintf
1458 "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1459 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1460 | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1461 if U.eq uri uri' && i = i' then
1463 split tl (List.length tl - k)
1464 in params,args,exp_named_subst
1465 else raise (TypeCheckerFailure (sprintf
1466 "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1467 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1469 raise (TypeCheckerFailure (sprintf
1470 "Case analysis: analysed term %s is not an inductive one"
1471 (CicPp.ppterm term)))
1473 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1474 let sort_of_ind_type =
1475 if parameters = [] then
1476 C.MutInd (uri,i,exp_named_subst)
1478 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1480 if not (check_allowed_sort_elimination context uri i need_dummy
1481 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1484 (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1485 (* let's check if the type of branches are right *)
1487 match CicEnvironment.get_cooked_obj ~trust:false uri with
1488 C.InductiveDefinition (_,_,parsno) -> parsno
1490 raise (TypeCheckerFailure
1491 ("Unknown mutual inductive definition:" ^
1492 UriManager.string_of_uri uri))
1494 let (_,branches_ok) =
1498 if parameters = [] then
1499 (C.MutConstruct (uri,i,j,exp_named_subst))
1501 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1508 R.are_convertible context (type_of_aux context p)
1509 (type_of_branch context parsno need_dummy outtype cons
1510 (type_of_aux context cons))
1511 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
1515 if not branches_ok then
1517 (TypeCheckerFailure "Case analysys: wrong branch type");
1518 if not need_dummy then
1519 C.Appl ((outtype::arguments)@[term])
1520 else if arguments = [] then
1523 C.Appl (outtype::arguments)
1525 let types_times_kl =
1529 let _ = type_of_aux context ty in
1530 (Some (C.Name n,(C.Decl ty)),k)) fl)
1532 let (types,kl) = List.split types_times_kl in
1533 let len = List.length types in
1535 (fun (name,x,ty,bo) ->
1537 (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1538 (CicSubstitution.lift len ty))
1541 let (m, eaten, context') =
1542 eat_lambdas (types @ context) (x + 1) bo
1544 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1547 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1550 (TypeCheckerFailure ("Fix: not guarded by destructors"))
1553 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1556 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1557 let (_,_,ty,_) = List.nth fl i in
1564 let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1566 let len = List.length types in
1570 (R.are_convertible (types @ context)
1571 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1574 (* let's control that the returned type is coinductive *)
1575 match returns_a_coinductive context ty with
1579 ("CoFix: does not return a coinductive type"))
1581 (*let's control the guarded by constructors conditions C{f,M}*)
1584 (guarded_by_constructors (types @ context) 0 len false bo
1588 (TypeCheckerFailure ("CoFix: not guarded by constructors"))
1592 (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1595 let (_,ty,_) = List.nth fl i in
1598 and check_exp_named_subst context =
1599 let rec check_exp_named_subst_aux substs =
1602 | ((uri,t) as subst)::tl ->
1604 CicSubstitution.subst_vars substs (type_of_variable uri) in
1605 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1606 Cic.Variable (_,Some bo,_,_) ->
1609 ("A variable with a body can not be explicit substituted"))
1610 | Cic.Variable (_,None,_,_) -> ()
1612 raise (TypeCheckerFailure
1613 ("Unknown mutual inductive definition:" ^
1614 UriManager.string_of_uri uri))
1616 let typeoft = type_of_aux context t in
1617 if CicReduction.are_convertible context typeoft typeofvar then
1618 check_exp_named_subst_aux (substs@[subst]) tl
1621 CicReduction.fdebug := 0 ;
1622 ignore (CicReduction.are_convertible context typeoft typeofvar) ;
1624 debug typeoft [typeofvar] ;
1625 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1628 check_exp_named_subst_aux []
1630 and sort_of_prod context (name,s) (t1, t2) =
1631 let module C = Cic in
1632 let t1' = CicReduction.whd context t1 in
1633 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1634 match (t1', t2') with
1635 (C.Sort s1, C.Sort s2)
1636 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
1638 | (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)