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 m nn kl x safes
801 (CicSubstitution.lift m bo)
802 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
806 | C.Implicit _ -> true
808 guarded_by_destructors context n nn kl x safes te &&
809 guarded_by_destructors context n nn kl x safes ty
810 | C.Prod (name,so,ta) ->
811 guarded_by_destructors context n nn kl x safes so &&
812 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
813 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
814 | C.Lambda (name,so,ta) ->
815 guarded_by_destructors context n nn kl x safes so &&
816 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
817 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
818 | C.LetIn (name,so,ta) ->
819 guarded_by_destructors context n nn kl x safes so &&
820 guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
821 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
822 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
823 let k = List.nth kl (m - n - 1) in
824 if not (List.length tl > k) then false
828 i && guarded_by_destructors context n nn kl x safes param
830 check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
833 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
835 | C.Var (_,exp_named_subst)
836 | C.Const (_,exp_named_subst)
837 | C.MutInd (_,_,exp_named_subst)
838 | C.MutConstruct (_,_,_,exp_named_subst) ->
840 (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
842 | C.MutCase (uri,i,outtype,term,pl) ->
844 C.Rel m when List.mem m safes || m = x ->
845 let (tys,len,isinductive,paramsno,cl) =
846 match CicEnvironment.get_obj uri with
847 C.InductiveDefinition (tl,_,paramsno) ->
848 let len = List.length tl in
849 let (_,isinductive,_,cl) = List.nth tl i in
851 List.map (fun (n,_,ty,_) ->
852 Some(Cic.Name n,(Cic.Decl ty))) tl
857 let debrujinedty = debrujin_constructor uri len ty in
858 (id, snd (split_prods tys paramsno ty),
859 snd (split_prods tys paramsno debrujinedty)
862 (tys,len,isinductive,paramsno,cl')
864 raise (TypeCheckerFailure
865 ("Unknown mutual inductive definition:" ^
866 UriManager.string_of_uri uri))
868 if not isinductive then
869 guarded_by_destructors context n nn kl x safes outtype &&
870 guarded_by_destructors context n nn kl x safes term &&
871 (*CSC: manca ??? il controllo sul tipo di term? *)
874 i && guarded_by_destructors context n nn kl x safes p)
877 guarded_by_destructors context n nn kl x safes outtype &&
878 (*CSC: manca ??? il controllo sul tipo di term? *)
880 (fun (p,(_,c,brujinedc)) i ->
881 let rl' = recursive_args tys 0 len brujinedc in
882 let (e,safes',n',nn',x',context') =
883 get_new_safes context p c rl' safes n nn x
886 guarded_by_destructors context' n' nn' kl x' safes' e
887 ) (List.combine pl cl) true
888 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
889 let (tys,len,isinductive,paramsno,cl) =
890 match CicEnvironment.get_obj uri with
891 C.InductiveDefinition (tl,_,paramsno) ->
892 let (_,isinductive,_,cl) = List.nth tl i in
895 (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
900 (id, snd (split_prods tys paramsno ty))) cl
902 (tys,List.length tl,isinductive,paramsno,cl')
904 raise (TypeCheckerFailure
905 ("Unknown mutual inductive definition:" ^
906 UriManager.string_of_uri uri))
908 if not isinductive then
909 guarded_by_destructors context n nn kl x safes outtype &&
910 guarded_by_destructors context n nn kl x safes term &&
911 (*CSC: manca ??? il controllo sul tipo di term? *)
914 i && guarded_by_destructors context n nn kl x safes p)
917 guarded_by_destructors context n nn kl x safes outtype &&
918 (*CSC: manca ??? il controllo sul tipo di term? *)
921 i && guarded_by_destructors context n nn kl x safes t)
926 let debrujinedte = debrujin_constructor uri len c in
927 recursive_args tys 0 len debrujinedte
929 let (e, safes',n',nn',x',context') =
930 get_new_safes context p c rl' safes n nn x
933 guarded_by_destructors context' n' nn' kl x' safes' e
934 ) (List.combine pl cl) true
936 guarded_by_destructors context n nn kl x safes outtype &&
937 guarded_by_destructors context n nn kl x safes term &&
938 (*CSC: manca ??? il controllo sul tipo di term? *)
940 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
944 let len = List.length fl in
945 let n_plus_len = n + len
946 and nn_plus_len = nn + len
947 and x_plus_len = x + len
948 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
949 and safes' = List.map (fun x -> x + len) safes in
951 (fun (_,_,ty,bo) i ->
952 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
953 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
957 let len = List.length fl in
958 let n_plus_len = n + len
959 and nn_plus_len = nn + len
960 and x_plus_len = x + len
961 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
962 and safes' = List.map (fun x -> x + len) safes in
966 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
967 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
971 (* the boolean h means already protected *)
972 (* args is the list of arguments the type of the constructor that may be *)
973 (* found in head position must be applied to. *)
974 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
975 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
976 let module C = Cic in
977 (*CSC: There is a lot of code replication between the cases X and *)
978 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
979 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
980 match CicReduction.whd context te with
981 C.Rel m when m > n && m <= nn -> h
989 (* the term has just been type-checked *)
990 raise (AssertFailure "17")
991 | C.Lambda (name,so,de) ->
992 does_not_occur context n nn so &&
993 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
994 (n + 1) (nn + 1) h de args coInductiveTypeURI
995 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
997 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
998 | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
1000 match CicEnvironment.get_cooked_obj ~trust:false uri with
1001 C.InductiveDefinition (itl,_,_) ->
1002 let (_,_,_,cl) = List.nth itl i in
1003 let (_,cons) = List.nth cl (j - 1) in
1004 CicSubstitution.subst_vars exp_named_subst cons
1006 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1007 UriManager.string_of_uri uri))
1009 let rec analyse_branch context ty te =
1010 match CicReduction.whd context ty with
1011 C.Meta _ -> raise (AssertFailure "34")
1015 does_not_occur context n nn te
1018 raise (AssertFailure "24")(* due to type-checking *)
1019 | C.Prod (name,so,de) ->
1020 analyse_branch ((Some (name,(C.Decl so)))::context) de te
1023 raise (AssertFailure "25")(* due to type-checking *)
1024 | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1025 when uri == coInductiveTypeURI ->
1026 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1027 | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1028 guarded_by_constructors context n nn true te tl coInductiveTypeURI
1030 does_not_occur context n nn te
1031 | C.Const _ -> raise (AssertFailure "26")
1032 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1033 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1035 does_not_occur context n nn te
1036 | C.MutConstruct _ -> raise (AssertFailure "27")
1037 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1038 (*CSC: in head position. *)
1042 raise (AssertFailure "28")(* due to type-checking *)
1044 let rec analyse_instantiated_type context ty l =
1045 match CicReduction.whd context ty with
1051 | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1052 | C.Prod (name,so,de) ->
1057 analyse_branch context so he &&
1058 analyse_instantiated_type
1059 ((Some (name,(C.Decl so)))::context) de tl
1063 raise (AssertFailure "30")(* due to type-checking *)
1066 (fun i x -> i && does_not_occur context n nn x) true l
1067 | C.Const _ -> raise (AssertFailure "31")
1070 (fun i x -> i && does_not_occur context n nn x) true l
1071 | C.MutConstruct _ -> raise (AssertFailure "32")
1072 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1073 (*CSC: in head position. *)
1077 raise (AssertFailure "33")(* due to type-checking *)
1079 let rec instantiate_type args consty =
1082 | tlhe::tltl as l ->
1083 let consty' = CicReduction.whd context consty in
1089 let instantiated_de = CicSubstitution.subst he de in
1090 (*CSC: siamo sicuri che non sia troppo forte? *)
1091 does_not_occur context n nn tlhe &
1092 instantiate_type tl instantiated_de tltl
1094 (*CSC:We do not consider backbones with a MutCase, a *)
1095 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1096 raise (AssertFailure "23")
1098 | [] -> analyse_instantiated_type context consty' l
1099 (* These are all the other cases *)
1101 instantiate_type args consty tl
1102 | C.Appl ((C.CoFix (_,fl))::tl) ->
1103 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1104 let len = List.length fl in
1105 let n_plus_len = n + len
1106 and nn_plus_len = nn + len
1107 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1108 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1111 i && does_not_occur context n nn ty &&
1112 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1113 args coInductiveTypeURI
1115 | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1116 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1117 does_not_occur context n nn out &&
1118 does_not_occur context n nn te &&
1122 guarded_by_constructors context n nn h x args coInductiveTypeURI
1125 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1126 | C.Var (_,exp_named_subst)
1127 | C.Const (_,exp_named_subst) ->
1129 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1130 | C.MutInd _ -> assert false
1131 | C.MutConstruct (_,_,_,exp_named_subst) ->
1133 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1134 | C.MutCase (_,_,out,te,pl) ->
1135 does_not_occur context n nn out &&
1136 does_not_occur context n nn te &&
1140 guarded_by_constructors context n nn h x args coInductiveTypeURI
1143 let len = List.length fl in
1144 let n_plus_len = n + len
1145 and nn_plus_len = nn + len
1146 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1147 and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1149 (fun (_,_,ty,bo) i ->
1150 i && does_not_occur context n nn ty &&
1151 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1154 let len = List.length fl in
1155 let n_plus_len = n + len
1156 and nn_plus_len = nn + len
1157 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1158 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1161 i && does_not_occur context n nn ty &&
1162 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1163 args coInductiveTypeURI
1166 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1167 let module C = Cic in
1168 let module U = UriManager in
1169 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1170 (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1171 when CicReduction.are_convertible context so1 so2 ->
1172 check_allowed_sort_elimination context uri i need_dummy
1173 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1174 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1175 | (C.Sort C.Prop, C.Sort C.Set)
1176 | (C.Sort C.Prop, C.Sort C.CProp)
1177 | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
1178 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1179 (match CicEnvironment.get_obj uri with
1180 C.InductiveDefinition (itl,_,_) ->
1181 let (_,_,_,cl) = List.nth itl i in
1182 (* is a singleton definition or the empty proposition? *)
1183 List.length cl = 1 || List.length cl = 0
1185 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1186 UriManager.string_of_uri uri))
1188 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1189 | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true
1190 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1191 | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
1192 | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
1193 | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
1194 | ((C.Sort C.Set, C.Sort C.Type) | (C.Sort C.CProp, C.Sort C.Type))
1196 (match CicEnvironment.get_obj uri with
1197 C.InductiveDefinition (itl,_,paramsno) ->
1199 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1201 let (_,_,_,cl) = List.nth itl i in
1203 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1205 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1206 UriManager.string_of_uri uri))
1208 | (C.Sort C.Type, C.Sort _) when need_dummy -> true
1209 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1210 let res = CicReduction.are_convertible context so ind
1213 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1214 C.Sort C.Prop -> true
1215 | (C.Sort C.Set | C.Sort C.CProp) ->
1216 (match CicEnvironment.get_obj uri with
1217 C.InductiveDefinition (itl,_,_) ->
1218 let (_,_,_,cl) = List.nth itl i in
1219 (* is a singleton definition? *)
1222 raise (TypeCheckerFailure
1223 ("Unknown mutual inductive definition:" ^
1224 UriManager.string_of_uri uri))
1228 | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
1229 when not need_dummy ->
1230 let res = CicReduction.are_convertible context so ind
1233 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1235 | C.Sort C.Set -> true
1236 | C.Sort C.CProp -> true
1238 (match CicEnvironment.get_obj uri with
1239 C.InductiveDefinition (itl,_,paramsno) ->
1240 let (_,_,_,cl) = List.nth itl i in
1243 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1246 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1248 raise (TypeCheckerFailure
1249 ("Unknown mutual inductive definition:" ^
1250 UriManager.string_of_uri uri))
1252 | _ -> raise (AssertFailure "19")
1254 | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
1255 CicReduction.are_convertible context so ind
1258 and type_of_branch context argsno need_dummy outtype term constype =
1259 let module C = Cic in
1260 let module R = CicReduction in
1261 match R.whd context constype with
1266 C.Appl [outtype ; term]
1267 | C.Appl (C.MutInd (_,_,_)::tl) ->
1268 let (_,arguments) = split tl argsno
1270 if need_dummy && arguments = [] then
1273 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1274 | C.Prod (name,so,de) ->
1276 match CicSubstitution.lift 1 term with
1277 C.Appl l -> C.Appl (l@[C.Rel 1])
1278 | t -> C.Appl [t ; C.Rel 1]
1280 C.Prod (C.Anonymous,so,type_of_branch
1281 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1282 (CicSubstitution.lift 1 outtype) term' de)
1283 | _ -> raise (AssertFailure "20")
1285 (* check_metasenv_consistency checks that the "canonical" context of a
1286 metavariable is consitent - up to relocation via the relocation list l -
1287 with the actual context *)
1289 and check_metasenv_consistency metasenv context canonical_context l =
1290 let module C = Cic in
1291 let module R = CicReduction in
1292 let module S = CicSubstitution in
1293 let lifted_canonical_context =
1297 | (Some (n,C.Decl t))::tl ->
1298 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1299 | (Some (n,C.Def (t,None)))::tl ->
1300 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1301 | None::tl -> None::(aux (i+1) tl)
1302 | (Some (n,C.Def (t,Some ty)))::tl ->
1303 (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)
1305 aux 1 canonical_context
1311 | Some t,Some (_,C.Def (ct,_)) ->
1312 if not (R.are_convertible context t ct) then
1313 raise (TypeCheckerFailure (sprintf
1314 "Not well typed metavariable local context: expected a term convertible with %s, found %s"
1315 (CicPp.ppterm ct) (CicPp.ppterm t)))
1316 | Some t,Some (_,C.Decl ct) ->
1317 let type_t = type_of_aux' metasenv context t in
1318 if not (R.are_convertible context type_t ct) then
1319 raise (TypeCheckerFailure (sprintf
1320 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1321 (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
1323 raise (TypeCheckerFailure
1324 "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
1325 ) l lifted_canonical_context
1327 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1328 and type_of_aux' metasenv context t =
1329 let rec type_of_aux context =
1330 let module C = Cic in
1331 let module R = CicReduction in
1332 let module S = CicSubstitution in
1333 let module U = UriManager in
1337 match List.nth context (n - 1) with
1338 Some (_,C.Decl t) -> S.lift n t
1339 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
1340 | Some (_,C.Def (bo,None)) ->
1341 debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1342 type_of_aux context (S.lift n bo)
1343 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
1346 raise (TypeCheckerFailure "unbound variable")
1348 | C.Var (uri,exp_named_subst) ->
1350 check_exp_named_subst context exp_named_subst ;
1352 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1357 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1358 check_metasenv_consistency metasenv context canonical_context l;
1359 CicSubstitution.lift_meta l ty
1360 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1361 | C.Implicit _ -> raise (AssertFailure "21")
1362 | C.Cast (te,ty) as t ->
1363 let _ = type_of_aux context ty in
1364 if R.are_convertible context (type_of_aux context te) ty then
1367 raise (TypeCheckerFailure
1368 (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1369 | C.Prod (name,s,t) ->
1370 let sort1 = type_of_aux context s
1371 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1372 sort_of_prod context (name,s) (sort1,sort2)
1373 | C.Lambda (n,s,t) ->
1374 let sort1 = type_of_aux context s in
1375 (match R.whd context sort1 with
1380 (TypeCheckerFailure (sprintf
1381 "Not well-typed lambda-abstraction: the source %s should be a
1382 type; instead it is a term of type %s" (CicPp.ppterm s)
1383 (CicPp.ppterm sort1)))
1385 let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1387 | C.LetIn (n,s,t) ->
1388 (* only to check if s is well-typed *)
1389 let ty = type_of_aux context s in
1390 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1391 LetIn is later reduced and maybe also re-checked.
1392 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1394 (* The type of the LetIn is reduced. Much faster than the previous
1395 solution. Moreover the inferred type is probably very different
1396 from the expected one.
1397 (CicReduction.whd context
1398 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1400 (* One-step LetIn reduction. Even faster than the previous solution.
1401 Moreover the inferred type is closer to the expected one. *)
1402 (CicSubstitution.subst s
1403 (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
1404 | C.Appl (he::tl) when List.length tl > 0 ->
1405 let hetype = type_of_aux context he
1406 and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1407 eat_prods context hetype tlbody_and_type
1408 | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1409 | C.Const (uri,exp_named_subst) ->
1411 check_exp_named_subst context exp_named_subst ;
1413 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1417 | C.MutInd (uri,i,exp_named_subst) ->
1419 check_exp_named_subst context exp_named_subst ;
1421 CicSubstitution.subst_vars exp_named_subst
1422 (type_of_mutual_inductive_defs uri i)
1426 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1427 check_exp_named_subst context exp_named_subst ;
1429 CicSubstitution.subst_vars exp_named_subst
1430 (type_of_mutual_inductive_constr uri i j)
1433 | C.MutCase (uri,i,outtype,term,pl) ->
1434 let outsort = type_of_aux context outtype in
1435 let (need_dummy, k) =
1436 let rec guess_args context t =
1437 let outtype = CicReduction.whd context t in
1439 C.Sort _ -> (true, 0)
1440 | C.Prod (name, s, t) ->
1441 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1443 (* last prod before sort *)
1444 match CicReduction.whd context s with
1445 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1446 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1448 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1449 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1450 when U.eq uri' uri && i' = i -> (false, 1)
1455 raise (TypeCheckerFailure (sprintf
1456 "Malformed case analasys' output type %s" (CicPp.ppterm outtype)))
1458 (*CSC whd non serve dopo type_of_aux ? *)
1459 let (b, k) = guess_args context outsort in
1460 if not b then (b, k - 1) else (b, k)
1462 let (parameters, arguments, exp_named_subst) =
1463 match R.whd context (type_of_aux context term) with
1464 (*CSC manca il caso dei CAST *)
1465 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1466 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
1467 (*CSC: Hint: nella DTD servono per gli stylesheet. *)
1468 C.MutInd (uri',i',exp_named_subst) as typ ->
1469 if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1470 else raise (TypeCheckerFailure (sprintf
1471 "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1472 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1473 | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1474 if U.eq uri uri' && i = i' then
1476 split tl (List.length tl - k)
1477 in params,args,exp_named_subst
1478 else raise (TypeCheckerFailure (sprintf
1479 "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1480 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1482 raise (TypeCheckerFailure (sprintf
1483 "Case analysis: analysed term %s is not an inductive one"
1484 (CicPp.ppterm term)))
1486 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1487 let sort_of_ind_type =
1488 if parameters = [] then
1489 C.MutInd (uri,i,exp_named_subst)
1491 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1493 if not (check_allowed_sort_elimination context uri i need_dummy
1494 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1497 (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1498 (* let's check if the type of branches are right *)
1500 match CicEnvironment.get_cooked_obj ~trust:false uri with
1501 C.InductiveDefinition (_,_,parsno) -> parsno
1503 raise (TypeCheckerFailure
1504 ("Unknown mutual inductive definition:" ^
1505 UriManager.string_of_uri uri))
1507 let (_,branches_ok) =
1511 if parameters = [] then
1512 (C.MutConstruct (uri,i,j,exp_named_subst))
1514 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1521 R.are_convertible context (type_of_aux context p)
1522 (type_of_branch context parsno need_dummy outtype cons
1523 (type_of_aux context cons))
1524 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
1528 if not branches_ok then
1530 (TypeCheckerFailure "Case analysys: wrong branch type");
1531 if not need_dummy then
1532 C.Appl ((outtype::arguments)@[term])
1533 else if arguments = [] then
1536 C.Appl (outtype::arguments)
1538 let types_times_kl =
1542 let _ = type_of_aux context ty in
1543 (Some (C.Name n,(C.Decl ty)),k)) fl)
1545 let (types,kl) = List.split types_times_kl in
1546 let len = List.length types in
1548 (fun (name,x,ty,bo) ->
1550 (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1551 (CicSubstitution.lift len ty))
1554 let (m, eaten, context') =
1555 eat_lambdas (types @ context) (x + 1) bo
1557 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1560 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1563 (TypeCheckerFailure ("Fix: not guarded by destructors"))
1566 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1569 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1570 let (_,_,ty,_) = List.nth fl i in
1577 let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1579 let len = List.length types in
1583 (R.are_convertible (types @ context)
1584 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1587 (* let's control that the returned type is coinductive *)
1588 match returns_a_coinductive context ty with
1592 ("CoFix: does not return a coinductive type"))
1594 (*let's control the guarded by constructors conditions C{f,M}*)
1597 (guarded_by_constructors (types @ context) 0 len false bo
1601 (TypeCheckerFailure ("CoFix: not guarded by constructors"))
1605 (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1608 let (_,ty,_) = List.nth fl i in
1611 and check_exp_named_subst context =
1612 let rec check_exp_named_subst_aux substs =
1615 | ((uri,t) as subst)::tl ->
1617 CicSubstitution.subst_vars substs (type_of_variable uri) in
1618 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1619 Cic.Variable (_,Some bo,_,_) ->
1622 ("A variable with a body can not be explicit substituted"))
1623 | Cic.Variable (_,None,_,_) -> ()
1625 raise (TypeCheckerFailure
1626 ("Unknown variable definition:" ^
1627 UriManager.string_of_uri uri))
1629 let typeoft = type_of_aux context t in
1630 if CicReduction.are_convertible context typeoft typeofvar then
1631 check_exp_named_subst_aux (substs@[subst]) tl
1634 CicReduction.fdebug := 0 ;
1635 ignore (CicReduction.are_convertible context typeoft typeofvar) ;
1637 debug typeoft [typeofvar] ;
1638 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1641 check_exp_named_subst_aux []
1643 and sort_of_prod context (name,s) (t1, t2) =
1644 let module C = Cic in
1645 let t1' = CicReduction.whd context t1 in
1646 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1647 match (t1', t2') with
1648 (C.Sort s1, C.Sort s2)
1649 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
1651 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1652 | (C.Meta _, C.Sort _) -> t2'
1653 | (C.Meta _, (C.Meta (_,_) as t))
1654 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1656 | (_,_) -> raise (TypeCheckerFailure (sprintf
1657 "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1658 (CicPp.ppterm t2')))
1660 and eat_prods context hetype =
1661 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1665 | (hete, hety)::tl ->
1666 (match (CicReduction.whd context hetype) with
1668 if CicReduction.are_convertible context hety s then
1669 (CicReduction.fdebug := -1 ;
1670 eat_prods context (CicSubstitution.subst hete t) tl
1674 CicReduction.fdebug := 0 ;
1675 ignore (CicReduction.are_convertible context s hety) ;
1678 raise (TypeCheckerFailure (sprintf
1679 "Appl: wrong parameter-type, expected %s, found %s"
1680 (CicPp.ppterm hetype) (CicPp.ppterm s)))
1683 raise (TypeCheckerFailure
1684 "Appl: this is not a function, it cannot be applied")
1687 and returns_a_coinductive context ty =
1688 let module C = Cic in
1689 match CicReduction.whd context ty with
1690 C.MutInd (uri,i,_) ->
1691 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1692 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1693 C.InductiveDefinition (itl,_,_) ->
1694 let (_,is_inductive,_,_) = List.nth itl i in
1695 if is_inductive then None else (Some uri)
1697 raise (TypeCheckerFailure
1698 ("Unknown mutual inductive definition:" ^
1699 UriManager.string_of_uri uri))
1701 | C.Appl ((C.MutInd (uri,i,_))::_) ->
1702 (match CicEnvironment.get_obj uri with
1703 C.InductiveDefinition (itl,_,_) ->
1704 let (_,is_inductive,_,_) = List.nth itl i in
1705 if is_inductive then None else (Some uri)
1707 raise (TypeCheckerFailure
1708 ("Unknown mutual inductive definition:" ^
1709 UriManager.string_of_uri uri))
1711 | C.Prod (n,so,de) ->
1712 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1717 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1720 type_of_aux context t
1722 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
1725 (* is a small constructor? *)
1726 (*CSC: ottimizzare calcolando staticamente *)
1727 and is_small context paramsno c =
1728 let rec is_small_aux context c =
1729 let module C = Cic in
1730 match CicReduction.whd context c with
1732 (*CSC: [] is an empty metasenv. Is it correct? *)
1733 let s = type_of_aux' [] context so in
1734 (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
1735 is_small_aux ((Some (n,(C.Decl so)))::context) de
1736 | _ -> true (*CSC: we trust the type-checker *)
1738 let (context',dx) = split_prods context paramsno c in
1739 is_small_aux context' dx
1743 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1746 type_of_aux' [] [] t
1748 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
1753 let module C = Cic in
1754 let module R = CicReduction in
1755 let module U = UriManager in
1756 match CicEnvironment.is_type_checked ~trust:false uri with
1757 CicEnvironment.CheckedObj _ -> ()
1758 | CicEnvironment.UncheckedObj uobj ->
1759 (* let's typecheck the uncooked object *)
1760 CicLogger.log (`Start_type_checking uri) ;
1762 C.Constant (_,Some te,ty,_) ->
1763 let _ = type_of ty in
1764 if not (R.are_convertible [] (type_of te ) ty) then
1765 raise (TypeCheckerFailure
1766 ("Unknown constant:" ^ U.string_of_uri uri))
1767 | C.Constant (_,None,ty,_) ->
1768 (* only to check that ty is well-typed *)
1769 let _ = type_of ty in ()
1770 | C.CurrentProof (_,conjs,te,ty,_) ->
1773 (fun metasenv ((_,context,ty) as conj) ->
1774 ignore (type_of_aux' metasenv context ty) ;
1778 let _ = type_of_aux' conjs [] ty in
1779 let type_of_te = type_of_aux' conjs [] te in
1780 if not (R.are_convertible [] type_of_te ty)
1782 raise (TypeCheckerFailure (sprintf
1783 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
1784 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
1786 | C.Variable (_,bo,ty,_) ->
1787 (* only to check that ty is well-typed *)
1788 let _ = type_of ty in
1792 if not (R.are_convertible [] (type_of bo) ty) then
1793 raise (TypeCheckerFailure
1794 ("Unknown variable:" ^ U.string_of_uri uri))
1796 | C.InductiveDefinition _ ->
1797 check_mutual_inductive_defs uri uobj
1799 CicEnvironment.set_type_checking_info uri ;
1800 CicLogger.log (`Type_checking_completed uri)