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
206 | C.Meta _ (* CSC: Are we sure? No recursion?*)
208 | C.Implicit _ -> true
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 (HelmLibraryObjects.Datatypes.nat_URI,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) *)
615 (Printf.sprintf "Get New Safes: c=%s ; p=%s"
616 (CicPp.ppterm c) (CicPp.ppterm p)))
618 and split_prods context n te =
619 let module C = Cic in
620 let module R = CicReduction in
621 match (n, R.whd context te) with
623 | (n, C.Prod (name,so,ta)) when n > 0 ->
624 split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta
625 | (_, _) -> raise (AssertFailure "8")
627 and eat_lambdas context n te =
628 let module C = Cic in
629 let module R = CicReduction in
630 match (n, R.whd context te) with
631 (0, _) -> (te, 0, context)
632 | (n, C.Lambda (name,so,ta)) when n > 0 ->
633 let (te, k, context') =
634 eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
636 (te, k + 1, context')
638 raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
640 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
641 and check_is_really_smaller_arg context n nn kl x safes te =
642 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
643 (*CSC: cfr guarded_by_destructors *)
644 let module C = Cic in
645 let module U = UriManager in
646 match CicReduction.whd context te with
647 C.Rel m when List.mem m safes -> true
654 (* | C.Cast (te,ty) ->
655 check_is_really_smaller_arg n nn kl x safes te &&
656 check_is_really_smaller_arg n nn kl x safes ty*)
657 (* | C.Prod (_,so,ta) ->
658 check_is_really_smaller_arg n nn kl x safes so &&
659 check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
660 (List.map (fun x -> x + 1) safes) ta*)
661 | C.Prod _ -> raise (AssertFailure "10")
662 | C.Lambda (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.Decl so)))::context)
665 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
666 | C.LetIn (name,so,ta) ->
667 check_is_really_smaller_arg context n nn kl x safes so &&
668 check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::context)
669 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
671 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
672 (*CSC: solo perche' non abbiamo trovato controesempi *)
673 check_is_really_smaller_arg context n nn kl x safes he
674 | C.Appl [] -> raise (AssertFailure "11")
676 | C.MutInd _ -> raise (AssertFailure "12")
677 | C.MutConstruct _ -> false
678 | C.MutCase (uri,i,outtype,term,pl) ->
680 C.Rel m when List.mem m safes || m = x ->
681 let (tys,len,isinductive,paramsno,cl) =
682 match CicEnvironment.get_obj uri with
683 C.InductiveDefinition (tl,_,paramsno) ->
686 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
688 let (_,isinductive,_,cl) = List.nth tl i in
692 (id, snd (split_prods tys paramsno ty))) cl
694 (tys,List.length tl,isinductive,paramsno,cl')
696 raise (TypeCheckerFailure
697 ("Unknown mutual inductive definition:" ^
698 UriManager.string_of_uri uri))
700 if not isinductive then
703 i && check_is_really_smaller_arg context n nn kl x safes p)
709 let debrujinedte = debrujin_constructor uri len c in
710 recursive_args tys 0 len debrujinedte
712 let (e,safes',n',nn',x',context') =
713 get_new_safes context p c rl' safes n nn x
716 check_is_really_smaller_arg context' n' nn' kl x' safes' e
717 ) (List.combine pl cl) true
718 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
719 let (tys,len,isinductive,paramsno,cl) =
720 match CicEnvironment.get_obj uri with
721 C.InductiveDefinition (tl,_,paramsno) ->
722 let (_,isinductive,_,cl) = List.nth tl i in
724 List.map (fun (n,_,ty,_) ->
725 Some(Cic.Name n,(Cic.Decl ty))) tl
730 (id, snd (split_prods tys paramsno ty))) cl
732 (tys,List.length tl,isinductive,paramsno,cl')
734 raise (TypeCheckerFailure
735 ("Unknown mutual inductive definition:" ^
736 UriManager.string_of_uri uri))
738 if not isinductive then
741 i && check_is_really_smaller_arg context n nn kl x safes p)
744 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
745 (*CSC: sugli argomenti di una applicazione *)
749 let debrujinedte = debrujin_constructor uri len c in
750 recursive_args tys 0 len debrujinedte
752 let (e, safes',n',nn',x',context') =
753 get_new_safes context p c rl' safes n nn x
756 check_is_really_smaller_arg context' n' nn' kl x' safes' e
757 ) (List.combine pl cl) true
761 i && check_is_really_smaller_arg context n nn kl x safes p
765 let len = List.length fl in
766 let n_plus_len = n + len
767 and nn_plus_len = nn + len
768 and x_plus_len = x + len
769 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
770 and safes' = List.map (fun x -> x + len) safes in
772 (fun (_,_,ty,bo) i ->
774 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
778 let len = List.length fl in
779 let n_plus_len = n + len
780 and nn_plus_len = nn + len
781 and x_plus_len = x + len
782 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
783 and safes' = List.map (fun x -> x + len) safes in
787 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
791 and guarded_by_destructors context n nn kl x safes =
792 let module C = Cic in
793 let module U = UriManager in
795 C.Rel m when m > n && m <= nn -> false
797 (match List.nth context (n-1) with
798 Some (_,C.Decl _) -> true
799 | Some (_,C.Def (bo,_)) ->
800 guarded_by_destructors context n nn kl x safes bo
801 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
805 | C.Implicit _ -> true
807 guarded_by_destructors context n nn kl x safes te &&
808 guarded_by_destructors context n nn kl x safes ty
809 | C.Prod (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.Lambda (name,so,ta) ->
814 guarded_by_destructors context n nn kl x safes so &&
815 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
816 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
817 | C.LetIn (name,so,ta) ->
818 guarded_by_destructors context n nn kl x safes so &&
819 guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
820 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
821 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
822 let k = List.nth kl (m - n - 1) in
823 if not (List.length tl > k) then false
827 i && guarded_by_destructors context n nn kl x safes param
829 check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
832 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
834 | C.Var (_,exp_named_subst)
835 | C.Const (_,exp_named_subst)
836 | C.MutInd (_,_,exp_named_subst)
837 | C.MutConstruct (_,_,_,exp_named_subst) ->
839 (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
841 | C.MutCase (uri,i,outtype,term,pl) ->
843 C.Rel m when List.mem m safes || m = x ->
844 let (tys,len,isinductive,paramsno,cl) =
845 match CicEnvironment.get_obj uri with
846 C.InductiveDefinition (tl,_,paramsno) ->
847 let len = List.length tl in
848 let (_,isinductive,_,cl) = List.nth tl i in
850 List.map (fun (n,_,ty,_) ->
851 Some(Cic.Name n,(Cic.Decl ty))) tl
856 let debrujinedty = debrujin_constructor uri len ty in
857 (id, snd (split_prods tys paramsno ty),
858 snd (split_prods tys paramsno debrujinedty)
861 (tys,len,isinductive,paramsno,cl')
863 raise (TypeCheckerFailure
864 ("Unknown mutual inductive definition:" ^
865 UriManager.string_of_uri uri))
867 if not isinductive then
868 guarded_by_destructors context n nn kl x safes outtype &&
869 guarded_by_destructors context n nn kl x safes term &&
870 (*CSC: manca ??? il controllo sul tipo di term? *)
873 i && guarded_by_destructors context n nn kl x safes p)
876 guarded_by_destructors context n nn kl x safes outtype &&
877 (*CSC: manca ??? il controllo sul tipo di term? *)
879 (fun (p,(_,c,brujinedc)) i ->
880 let rl' = recursive_args tys 0 len brujinedc in
881 let (e,safes',n',nn',x',context') =
882 get_new_safes context p c rl' safes n nn x
885 guarded_by_destructors context' n' nn' kl x' safes' e
886 ) (List.combine pl cl) true
887 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
888 let (tys,len,isinductive,paramsno,cl) =
889 match CicEnvironment.get_obj uri with
890 C.InductiveDefinition (tl,_,paramsno) ->
891 let (_,isinductive,_,cl) = List.nth tl i in
894 (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
899 (id, snd (split_prods tys paramsno ty))) cl
901 (tys,List.length tl,isinductive,paramsno,cl')
903 raise (TypeCheckerFailure
904 ("Unknown mutual inductive definition:" ^
905 UriManager.string_of_uri uri))
907 if not isinductive then
908 guarded_by_destructors context n nn kl x safes outtype &&
909 guarded_by_destructors context n nn kl x safes term &&
910 (*CSC: manca ??? il controllo sul tipo di term? *)
913 i && guarded_by_destructors context n nn kl x safes p)
916 guarded_by_destructors context n nn kl x safes outtype &&
917 (*CSC: manca ??? il controllo sul tipo di term? *)
920 i && guarded_by_destructors context n nn kl x safes t)
925 let debrujinedte = debrujin_constructor uri len c in
926 recursive_args tys 0 len debrujinedte
928 let (e, safes',n',nn',x',context') =
929 get_new_safes context p c rl' safes n nn x
932 guarded_by_destructors context' n' nn' kl x' safes' e
933 ) (List.combine pl cl) true
935 guarded_by_destructors context n nn kl x safes outtype &&
936 guarded_by_destructors context n nn kl x safes term &&
937 (*CSC: manca ??? il controllo sul tipo di term? *)
939 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
943 let len = List.length fl in
944 let n_plus_len = n + len
945 and nn_plus_len = nn + len
946 and x_plus_len = x + len
947 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
948 and safes' = List.map (fun x -> x + len) safes in
950 (fun (_,_,ty,bo) i ->
951 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
952 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
956 let len = List.length fl in
957 let n_plus_len = n + len
958 and nn_plus_len = nn + len
959 and x_plus_len = x + len
960 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
961 and safes' = List.map (fun x -> x + len) safes in
965 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
966 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
970 (* the boolean h means already protected *)
971 (* args is the list of arguments the type of the constructor that may be *)
972 (* found in head position must be applied to. *)
973 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
974 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
975 let module C = Cic in
976 (*CSC: There is a lot of code replication between the cases X and *)
977 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
978 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
979 match CicReduction.whd context te with
980 C.Rel m when m > n && m <= nn -> h
988 (* the term has just been type-checked *)
989 raise (AssertFailure "17")
990 | C.Lambda (name,so,de) ->
991 does_not_occur context n nn so &&
992 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
993 (n + 1) (nn + 1) h de args coInductiveTypeURI
994 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
996 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
997 | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
999 match CicEnvironment.get_cooked_obj ~trust:false uri with
1000 C.InductiveDefinition (itl,_,_) ->
1001 let (_,_,_,cl) = List.nth itl i in
1002 let (_,cons) = List.nth cl (j - 1) in
1003 CicSubstitution.subst_vars exp_named_subst cons
1005 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1006 UriManager.string_of_uri uri))
1008 let rec analyse_branch context ty te =
1009 match CicReduction.whd context ty with
1010 C.Meta _ -> raise (AssertFailure "34")
1014 does_not_occur context n nn te
1017 raise (AssertFailure "24")(* due to type-checking *)
1018 | C.Prod (name,so,de) ->
1019 analyse_branch ((Some (name,(C.Decl so)))::context) de te
1022 raise (AssertFailure "25")(* due to type-checking *)
1023 | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1024 when uri == coInductiveTypeURI ->
1025 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1026 | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1027 guarded_by_constructors context n nn true te tl coInductiveTypeURI
1029 does_not_occur context n nn te
1030 | C.Const _ -> raise (AssertFailure "26")
1031 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1032 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1034 does_not_occur context n nn te
1035 | C.MutConstruct _ -> raise (AssertFailure "27")
1036 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1037 (*CSC: in head position. *)
1041 raise (AssertFailure "28")(* due to type-checking *)
1043 let rec analyse_instantiated_type context ty l =
1044 match CicReduction.whd context ty with
1050 | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1051 | C.Prod (name,so,de) ->
1056 analyse_branch context so he &&
1057 analyse_instantiated_type
1058 ((Some (name,(C.Decl so)))::context) de tl
1062 raise (AssertFailure "30")(* due to type-checking *)
1065 (fun i x -> i && does_not_occur context n nn x) true l
1066 | C.Const _ -> raise (AssertFailure "31")
1069 (fun i x -> i && does_not_occur context n nn x) true l
1070 | C.MutConstruct _ -> raise (AssertFailure "32")
1071 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1072 (*CSC: in head position. *)
1076 raise (AssertFailure "33")(* due to type-checking *)
1078 let rec instantiate_type args consty =
1081 | tlhe::tltl as l ->
1082 let consty' = CicReduction.whd context consty in
1088 let instantiated_de = CicSubstitution.subst he de in
1089 (*CSC: siamo sicuri che non sia troppo forte? *)
1090 does_not_occur context n nn tlhe &
1091 instantiate_type tl instantiated_de tltl
1093 (*CSC:We do not consider backbones with a MutCase, a *)
1094 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1095 raise (AssertFailure "23")
1097 | [] -> analyse_instantiated_type context consty' l
1098 (* These are all the other cases *)
1100 instantiate_type args consty tl
1101 | C.Appl ((C.CoFix (_,fl))::tl) ->
1102 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1103 let len = List.length fl in
1104 let n_plus_len = n + len
1105 and nn_plus_len = nn + len
1106 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1107 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1110 i && does_not_occur context n nn ty &&
1111 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1112 args coInductiveTypeURI
1114 | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1115 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1116 does_not_occur context n nn out &&
1117 does_not_occur context n nn te &&
1121 guarded_by_constructors context n nn h x args coInductiveTypeURI
1124 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1125 | C.Var (_,exp_named_subst)
1126 | C.Const (_,exp_named_subst) ->
1128 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1129 | C.MutInd _ -> assert false
1130 | C.MutConstruct (_,_,_,exp_named_subst) ->
1132 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1133 | C.MutCase (_,_,out,te,pl) ->
1134 does_not_occur context n nn out &&
1135 does_not_occur context n nn te &&
1139 guarded_by_constructors context n nn h x args coInductiveTypeURI
1142 let len = List.length fl in
1143 let n_plus_len = n + len
1144 and nn_plus_len = nn + len
1145 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1146 and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1148 (fun (_,_,ty,bo) i ->
1149 i && does_not_occur context n nn ty &&
1150 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1153 let len = List.length fl in
1154 let n_plus_len = n + len
1155 and nn_plus_len = nn + len
1156 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1157 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1160 i && does_not_occur context n nn ty &&
1161 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1162 args coInductiveTypeURI
1165 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1166 let module C = Cic in
1167 let module U = UriManager in
1168 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1169 (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1170 when CicReduction.are_convertible context so1 so2 ->
1171 check_allowed_sort_elimination context uri i need_dummy
1172 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1173 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1174 | (C.Sort C.Prop, C.Sort C.Set)
1175 | (C.Sort C.Prop, C.Sort C.CProp)
1176 | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
1177 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1178 (match CicEnvironment.get_obj uri with
1179 C.InductiveDefinition (itl,_,_) ->
1180 let (_,_,_,cl) = List.nth itl i in
1181 (* is a singleton definition or the empty proposition? *)
1182 List.length cl = 1 || List.length cl = 0
1184 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1185 UriManager.string_of_uri uri))
1187 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1188 | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true
1189 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1190 | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
1191 | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
1192 | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
1193 | ((C.Sort C.Set, C.Sort C.Type) | (C.Sort C.CProp, C.Sort C.Type))
1195 (match CicEnvironment.get_obj uri with
1196 C.InductiveDefinition (itl,_,paramsno) ->
1198 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1200 let (_,_,_,cl) = List.nth itl i in
1202 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1204 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1205 UriManager.string_of_uri uri))
1207 | (C.Sort C.Type, C.Sort _) when need_dummy -> true
1208 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1209 let res = CicReduction.are_convertible context so ind
1212 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1213 C.Sort C.Prop -> true
1214 | (C.Sort C.Set | C.Sort C.CProp) ->
1215 (match CicEnvironment.get_obj uri with
1216 C.InductiveDefinition (itl,_,_) ->
1217 let (_,_,_,cl) = List.nth itl i in
1218 (* is a singleton definition? *)
1221 raise (TypeCheckerFailure
1222 ("Unknown mutual inductive definition:" ^
1223 UriManager.string_of_uri uri))
1227 | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
1228 when not need_dummy ->
1229 let res = CicReduction.are_convertible context so ind
1232 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1234 | C.Sort C.Set -> true
1235 | C.Sort C.CProp -> true
1237 (match CicEnvironment.get_obj uri with
1238 C.InductiveDefinition (itl,_,paramsno) ->
1239 let (_,_,_,cl) = List.nth itl i in
1242 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1245 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1247 raise (TypeCheckerFailure
1248 ("Unknown mutual inductive definition:" ^
1249 UriManager.string_of_uri uri))
1251 | _ -> raise (AssertFailure "19")
1253 | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
1254 CicReduction.are_convertible context so ind
1257 and type_of_branch context argsno need_dummy outtype term constype =
1258 let module C = Cic in
1259 let module R = CicReduction in
1260 match R.whd context constype with
1265 C.Appl [outtype ; term]
1266 | C.Appl (C.MutInd (_,_,_)::tl) ->
1267 let (_,arguments) = split tl argsno
1269 if need_dummy && arguments = [] then
1272 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1273 | C.Prod (name,so,de) ->
1275 match CicSubstitution.lift 1 term with
1276 C.Appl l -> C.Appl (l@[C.Rel 1])
1277 | t -> C.Appl [t ; C.Rel 1]
1279 C.Prod (C.Anonymous,so,type_of_branch
1280 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1281 (CicSubstitution.lift 1 outtype) term' de)
1282 | _ -> raise (AssertFailure "20")
1284 (* check_metasenv_consistency checks that the "canonical" context of a
1285 metavariable is consitent - up to relocation via the relocation list l -
1286 with the actual context *)
1288 and check_metasenv_consistency metasenv context canonical_context l =
1289 let module C = Cic in
1290 let module R = CicReduction in
1291 let module S = CicSubstitution in
1292 let lifted_canonical_context =
1296 | (Some (n,C.Decl t))::tl ->
1297 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1298 | (Some (n,C.Def (t,None)))::tl ->
1299 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1300 | None::tl -> None::(aux (i+1) tl)
1301 | (Some (n,C.Def (t,Some ty)))::tl ->
1302 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
1304 aux 1 canonical_context
1310 | Some t,Some (_,C.Def (ct,_)) ->
1311 if not (R.are_convertible context t ct) then
1312 raise (TypeCheckerFailure (sprintf
1313 "Not well typed metavariable local context: expected a term convertible with %s, found %s"
1314 (CicPp.ppterm ct) (CicPp.ppterm t)))
1315 | Some t,Some (_,C.Decl ct) ->
1316 let type_t = type_of_aux' metasenv context t in
1317 if not (R.are_convertible context type_t ct) then
1318 raise (TypeCheckerFailure (sprintf
1319 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1320 (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
1322 raise (TypeCheckerFailure
1323 "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
1324 ) l lifted_canonical_context
1326 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1327 and type_of_aux' metasenv context t =
1328 let rec type_of_aux context =
1329 let module C = Cic in
1330 let module R = CicReduction in
1331 let module S = CicSubstitution in
1332 let module U = UriManager in
1336 match List.nth context (n - 1) with
1337 Some (_,C.Decl t) -> S.lift n t
1338 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
1339 | Some (_,C.Def (bo,None)) ->
1340 debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1341 type_of_aux context (S.lift n bo)
1342 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
1345 raise (TypeCheckerFailure "unbound variable")
1347 | C.Var (uri,exp_named_subst) ->
1349 check_exp_named_subst context exp_named_subst ;
1351 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1356 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1357 check_metasenv_consistency metasenv context canonical_context l;
1358 CicSubstitution.lift_meta l ty
1359 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1360 | C.Implicit _ -> raise (AssertFailure "21")
1361 | C.Cast (te,ty) as t ->
1362 let _ = type_of_aux context ty in
1363 if R.are_convertible context (type_of_aux context te) ty then
1366 raise (TypeCheckerFailure
1367 (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1368 | C.Prod (name,s,t) ->
1369 let sort1 = type_of_aux context s
1370 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1371 sort_of_prod context (name,s) (sort1,sort2)
1372 | C.Lambda (n,s,t) ->
1373 let sort1 = type_of_aux context s in
1374 (match R.whd context sort1 with
1379 (TypeCheckerFailure (sprintf
1380 "Not well-typed lambda-abstraction: the source %s should be a
1381 type; instead it is a term of type %s" (CicPp.ppterm s)
1382 (CicPp.ppterm sort1)))
1384 let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1386 | C.LetIn (n,s,t) ->
1387 (* only to check if s is well-typed *)
1388 let ty = type_of_aux context s in
1389 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1390 LetIn is later reduced and maybe also re-checked.
1391 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1393 (* The type of the LetIn is reduced. Much faster than the previous
1394 solution. Moreover the inferred type is probably very different
1395 from the expected one.
1396 (CicReduction.whd context
1397 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1399 (* One-step LetIn reduction. Even faster than the previous solution.
1400 Moreover the inferred type is closer to the expected one. *)
1401 (CicSubstitution.subst s
1402 (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
1403 | C.Appl (he::tl) when List.length tl > 0 ->
1404 let hetype = type_of_aux context he
1405 and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1406 eat_prods context hetype tlbody_and_type
1407 | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1408 | C.Const (uri,exp_named_subst) ->
1410 check_exp_named_subst context exp_named_subst ;
1412 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1416 | C.MutInd (uri,i,exp_named_subst) ->
1418 check_exp_named_subst context exp_named_subst ;
1420 CicSubstitution.subst_vars exp_named_subst
1421 (type_of_mutual_inductive_defs uri i)
1425 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1426 check_exp_named_subst context exp_named_subst ;
1428 CicSubstitution.subst_vars exp_named_subst
1429 (type_of_mutual_inductive_constr uri i j)
1432 | C.MutCase (uri,i,outtype,term,pl) ->
1433 let outsort = type_of_aux context outtype in
1434 let (need_dummy, k) =
1435 let rec guess_args context t =
1436 let outtype = CicReduction.whd context t in
1438 C.Sort _ -> (true, 0)
1439 | C.Prod (name, s, t) ->
1440 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1442 (* last prod before sort *)
1443 match CicReduction.whd context s with
1444 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1445 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1447 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1448 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1449 when U.eq uri' uri && i' = i -> (false, 1)
1454 raise (TypeCheckerFailure (sprintf
1455 "Malformed case analasys' output type %s" (CicPp.ppterm outtype)))
1457 (*CSC whd non serve dopo type_of_aux ? *)
1458 let (b, k) = guess_args context outsort in
1459 if not b then (b, k - 1) else (b, k)
1461 let (parameters, arguments, exp_named_subst) =
1462 match R.whd context (type_of_aux context term) with
1463 (*CSC manca il caso dei CAST *)
1464 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1465 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
1466 (*CSC: Hint: nella DTD servono per gli stylesheet. *)
1467 C.MutInd (uri',i',exp_named_subst) as typ ->
1468 if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1469 else raise (TypeCheckerFailure (sprintf
1470 "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1471 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1472 | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1473 if U.eq uri uri' && i = i' then
1475 split tl (List.length tl - k)
1476 in params,args,exp_named_subst
1477 else raise (TypeCheckerFailure (sprintf
1478 "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1479 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1481 raise (TypeCheckerFailure (sprintf
1482 "Case analysis: analysed term %s is not an inductive one"
1483 (CicPp.ppterm term)))
1485 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1486 let sort_of_ind_type =
1487 if parameters = [] then
1488 C.MutInd (uri,i,exp_named_subst)
1490 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1492 if not (check_allowed_sort_elimination context uri i need_dummy
1493 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1496 (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1497 (* let's check if the type of branches are right *)
1499 match CicEnvironment.get_cooked_obj ~trust:false uri with
1500 C.InductiveDefinition (_,_,parsno) -> parsno
1502 raise (TypeCheckerFailure
1503 ("Unknown mutual inductive definition:" ^
1504 UriManager.string_of_uri uri))
1506 let (_,branches_ok) =
1510 if parameters = [] then
1511 (C.MutConstruct (uri,i,j,exp_named_subst))
1513 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1520 R.are_convertible context (type_of_aux context p)
1521 (type_of_branch context parsno need_dummy outtype cons
1522 (type_of_aux context cons))
1523 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
1527 if not branches_ok then
1529 (TypeCheckerFailure "Case analysys: wrong branch type");
1530 if not need_dummy then
1531 C.Appl ((outtype::arguments)@[term])
1532 else if arguments = [] then
1535 C.Appl (outtype::arguments)
1537 let types_times_kl =
1541 let _ = type_of_aux context ty in
1542 (Some (C.Name n,(C.Decl ty)),k)) fl)
1544 let (types,kl) = List.split types_times_kl in
1545 let len = List.length types in
1547 (fun (name,x,ty,bo) ->
1549 (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1550 (CicSubstitution.lift len ty))
1553 let (m, eaten, context') =
1554 eat_lambdas (types @ context) (x + 1) bo
1556 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1559 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1562 (TypeCheckerFailure ("Fix: not guarded by destructors"))
1565 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1568 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1569 let (_,_,ty,_) = List.nth fl i in
1576 let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1578 let len = List.length types in
1582 (R.are_convertible (types @ context)
1583 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1586 (* let's control that the returned type is coinductive *)
1587 match returns_a_coinductive context ty with
1591 ("CoFix: does not return a coinductive type"))
1593 (*let's control the guarded by constructors conditions C{f,M}*)
1596 (guarded_by_constructors (types @ context) 0 len false bo
1600 (TypeCheckerFailure ("CoFix: not guarded by constructors"))
1604 (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1607 let (_,ty,_) = List.nth fl i in
1610 and check_exp_named_subst context =
1611 let rec check_exp_named_subst_aux substs =
1614 | ((uri,t) as subst)::tl ->
1616 CicSubstitution.subst_vars substs (type_of_variable uri) in
1617 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1618 Cic.Variable (_,Some bo,_,_) ->
1621 ("A variable with a body can not be explicit substituted"))
1622 | Cic.Variable (_,None,_,_) -> ()
1624 raise (TypeCheckerFailure
1625 ("Unknown mutual inductive definition:" ^
1626 UriManager.string_of_uri uri))
1628 let typeoft = type_of_aux context t in
1629 if CicReduction.are_convertible context typeoft typeofvar then
1630 check_exp_named_subst_aux (substs@[subst]) tl
1633 CicReduction.fdebug := 0 ;
1634 ignore (CicReduction.are_convertible context typeoft typeofvar) ;
1636 debug typeoft [typeofvar] ;
1637 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1640 check_exp_named_subst_aux []
1642 and sort_of_prod context (name,s) (t1, t2) =
1643 let module C = Cic in
1644 let t1' = CicReduction.whd context t1 in
1645 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1646 match (t1', t2') with
1647 (C.Sort s1, C.Sort s2)
1648 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
1650 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1651 | (C.Meta _, C.Sort _) -> t2'
1652 | (C.Meta _, (C.Meta (_,_) as t))
1653 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1655 | (_,_) -> raise (TypeCheckerFailure (sprintf
1656 "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1657 (CicPp.ppterm t2')))
1659 and eat_prods context hetype =
1660 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1664 | (hete, hety)::tl ->
1665 (match (CicReduction.whd context hetype) with
1667 if CicReduction.are_convertible context s hety then
1668 (CicReduction.fdebug := -1 ;
1669 eat_prods context (CicSubstitution.subst hete t) tl
1673 CicReduction.fdebug := 0 ;
1674 ignore (CicReduction.are_convertible context s hety) ;
1677 raise (TypeCheckerFailure (sprintf
1678 "Appl: wrong parameter-type, expected %s, found %s"
1679 (CicPp.ppterm hetype) (CicPp.ppterm s)))
1682 raise (TypeCheckerFailure
1683 "Appl: this is not a function, it cannot be applied")
1686 and returns_a_coinductive context ty =
1687 let module C = Cic in
1688 match CicReduction.whd context ty with
1689 C.MutInd (uri,i,_) ->
1690 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1691 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1692 C.InductiveDefinition (itl,_,_) ->
1693 let (_,is_inductive,_,_) = List.nth itl i in
1694 if is_inductive then None else (Some uri)
1696 raise (TypeCheckerFailure
1697 ("Unknown mutual inductive definition:" ^
1698 UriManager.string_of_uri uri))
1700 | C.Appl ((C.MutInd (uri,i,_))::_) ->
1701 (match CicEnvironment.get_obj uri with
1702 C.InductiveDefinition (itl,_,_) ->
1703 let (_,is_inductive,_,_) = List.nth itl i in
1704 if is_inductive then None else (Some uri)
1706 raise (TypeCheckerFailure
1707 ("Unknown mutual inductive definition:" ^
1708 UriManager.string_of_uri uri))
1710 | C.Prod (n,so,de) ->
1711 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1716 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1719 type_of_aux context t
1721 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
1724 (* is a small constructor? *)
1725 (*CSC: ottimizzare calcolando staticamente *)
1726 and is_small context paramsno c =
1727 let rec is_small_aux context c =
1728 let module C = Cic in
1729 match CicReduction.whd context c with
1731 (*CSC: [] is an empty metasenv. Is it correct? *)
1732 let s = type_of_aux' [] context so in
1733 (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
1734 is_small_aux ((Some (n,(C.Decl so)))::context) de
1735 | _ -> true (*CSC: we trust the type-checker *)
1737 let (context',dx) = split_prods context paramsno c in
1738 is_small_aux context' dx
1742 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1745 type_of_aux' [] [] t
1747 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
1752 let module C = Cic in
1753 let module R = CicReduction in
1754 let module U = UriManager in
1755 match CicEnvironment.is_type_checked ~trust:false uri with
1756 CicEnvironment.CheckedObj _ -> ()
1757 | CicEnvironment.UncheckedObj uobj ->
1758 (* let's typecheck the uncooked object *)
1759 CicLogger.log (`Start_type_checking uri) ;
1761 C.Constant (_,Some te,ty,_) ->
1762 let _ = type_of ty in
1763 if not (R.are_convertible [] (type_of te ) ty) then
1764 raise (TypeCheckerFailure
1765 ("Unknown constant:" ^ U.string_of_uri uri))
1766 | C.Constant (_,None,ty,_) ->
1767 (* only to check that ty is well-typed *)
1768 let _ = type_of ty in ()
1769 | C.CurrentProof (_,conjs,te,ty,_) ->
1772 (fun metasenv ((_,context,ty) as conj) ->
1773 ignore (type_of_aux' metasenv context ty) ;
1777 let _ = type_of_aux' conjs [] ty in
1778 let type_of_te = type_of_aux' conjs [] te in
1779 if not (R.are_convertible [] type_of_te ty)
1781 raise (TypeCheckerFailure (sprintf
1782 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
1783 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
1785 | C.Variable (_,bo,ty,_) ->
1786 (* only to check that ty is well-typed *)
1787 let _ = type_of ty in
1791 if not (R.are_convertible [] (type_of bo) ty) then
1792 raise (TypeCheckerFailure
1793 ("Unknown variable:" ^ U.string_of_uri uri))
1795 | C.InductiveDefinition _ ->
1796 check_mutual_inductive_defs uri uobj
1798 CicEnvironment.set_type_checking_info uri ;
1799 CicLogger.log (`Type_checking_completed uri)