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 type type_checker_exn =
28 | NotWellTyped of string
29 | WrongUriToConstant of string
30 | WrongUriToVariable of string
31 | WrongUriToMutualInductiveDefinitions of string
33 | NotPositiveOccurrences of string
34 | NotWellFormedTypeOfInductiveConstructor of string
35 | WrongRequiredArgument of string
36 | RelToHiddenHypothesis
37 | MetasenvInconsistency;;
39 (* This is the only exception that will be raised *)
40 exception TypeCheckerFailure of type_checker_exn;;
44 let rec debug_aux t i =
46 let module U = UriManager in
47 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
52 (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::context) "")))
53 (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
59 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
60 | (_,_) -> raise (TypeCheckerFailure ListTooShort)
63 let debrujin_constructor uri number_of_types =
67 C.Rel n as t when n <= k -> t
69 raise (TypeCheckerFailure (NotWellTyped ("Debrujin: open term found")))
70 | C.Var (uri,exp_named_subst) ->
71 let exp_named_subst' =
72 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
74 C.Var (uri,exp_named_subst')
75 | C.Meta _ -> assert false
77 | C.Implicit as t -> t
78 | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
79 | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
80 | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
81 | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t)
82 | C.Appl l -> C.Appl (List.map (aux k) l)
83 | C.Const (uri,exp_named_subst) ->
84 let exp_named_subst' =
85 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
87 C.Const (uri,exp_named_subst')
88 | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
89 if exp_named_subst != [] then
93 ("Debrujin: a non-empty explicit named substitution is applied to "^
94 "a mutual inductive type which is being defined"))) ;
95 C.Rel (k + number_of_types - tyno) ;
96 | C.MutInd (uri',tyno,exp_named_subst) ->
97 let exp_named_subst' =
98 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
100 C.MutInd (uri',tyno,exp_named_subst')
101 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
102 let exp_named_subst' =
103 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
105 C.MutConstruct (uri,tyno,consno,exp_named_subst')
106 | C.MutCase (sp,i,outty,t,pl) ->
107 C.MutCase (sp, i, aux k outty, aux k t,
110 let len = List.length fl in
113 (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
118 let len = List.length fl in
121 (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
124 C.CoFix (i, liftedfl)
129 exception CicEnvironmentError;;
131 let rec type_of_constant uri =
132 let module C = Cic in
133 let module R = CicReduction in
134 let module U = UriManager in
136 match CicEnvironment.is_type_checked ~trust:true uri with
137 CicEnvironment.CheckedObj cobj -> cobj
138 | CicEnvironment.UncheckedObj uobj ->
139 Logger.log (`Start_type_checking uri) ;
140 (* let's typecheck the uncooked obj *)
142 C.Constant (_,Some te,ty,_) ->
143 let _ = type_of ty in
144 if not (R.are_convertible [] (type_of te) ty) then
147 (NotWellTyped ("Constant " ^ (U.string_of_uri uri))))
148 | C.Constant (_,None,ty,_) ->
149 (* only to check that ty is well-typed *)
150 let _ = type_of ty in ()
151 | C.CurrentProof (_,conjs,te,ty,_) ->
154 (fun metasenv ((_,context,ty) as conj) ->
155 ignore (type_of_aux' metasenv context ty) ;
159 let _ = type_of_aux' conjs [] ty in
160 if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
164 (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))))
166 raise (TypeCheckerFailure (WrongUriToConstant (U.string_of_uri uri)))
168 CicEnvironment.set_type_checking_info uri ;
169 Logger.log (`Type_checking_completed uri) ;
170 match CicEnvironment.is_type_checked ~trust:false uri with
171 CicEnvironment.CheckedObj cobj -> cobj
172 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
175 C.Constant (_,_,ty,_) -> ty
176 | C.CurrentProof (_,_,_,ty,_) -> ty
177 | _ -> raise (TypeCheckerFailure (WrongUriToConstant (U.string_of_uri uri)))
179 and type_of_variable uri =
180 let module C = Cic in
181 let module R = CicReduction in
182 let module U = UriManager in
183 (* 0 because a variable is never cooked => no partial cooking at one level *)
184 match CicEnvironment.is_type_checked ~trust:true uri with
185 CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
186 | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
187 Logger.log (`Start_type_checking uri) ;
188 (* only to check that ty is well-typed *)
189 let _ = type_of ty in
193 if not (R.are_convertible [] (type_of bo) ty) then
196 (NotWellTyped ("Variable " ^ (U.string_of_uri uri))))
198 CicEnvironment.set_type_checking_info uri ;
199 Logger.log (`Type_checking_completed uri) ;
203 (TypeCheckerFailure (WrongUriToVariable (UriManager.string_of_uri uri)))
205 and does_not_occur context n nn te =
206 let module C = Cic in
207 (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
208 (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
210 match CicReduction.whd context te with
211 C.Rel m when m > n && m <= nn -> false
217 does_not_occur context n nn te && does_not_occur context n nn ty
218 | C.Prod (name,so,dest) ->
219 does_not_occur context n nn so &&
220 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
221 | C.Lambda (name,so,dest) ->
222 does_not_occur context n nn so &&
223 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
224 | C.LetIn (name,so,dest) ->
225 does_not_occur context n nn so &&
226 does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest
228 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
229 | C.Var (_,exp_named_subst)
230 | C.Const (_,exp_named_subst)
231 | C.MutInd (_,_,exp_named_subst)
232 | C.MutConstruct (_,_,_,exp_named_subst) ->
233 List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
235 | C.MutCase (_,_,out,te,pl) ->
236 does_not_occur context n nn out && does_not_occur context n nn te &&
237 List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
239 let len = List.length fl in
240 let n_plus_len = n + len in
241 let nn_plus_len = nn + len in
243 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
246 (fun (_,_,ty,bo) i ->
247 i && does_not_occur context n nn ty &&
248 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
251 let len = List.length fl in
252 let n_plus_len = n + len in
253 let nn_plus_len = nn + len in
255 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
259 i && does_not_occur context n nn ty &&
260 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
263 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
264 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
265 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
266 (*CSC strictly_positive *)
267 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
268 and weakly_positive context n nn uri te =
269 let module C = Cic in
270 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
272 C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,[])
274 (*CSC mettere in cicSubstitution *)
275 let rec subst_inductive_type_with_dummy_mutind =
277 C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
279 | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
281 | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
282 | C.Prod (name,so,ta) ->
283 C.Prod (name, subst_inductive_type_with_dummy_mutind so,
284 subst_inductive_type_with_dummy_mutind ta)
285 | C.Lambda (name,so,ta) ->
286 C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
287 subst_inductive_type_with_dummy_mutind ta)
289 C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
290 | C.MutCase (uri,i,outtype,term,pl) ->
292 subst_inductive_type_with_dummy_mutind outtype,
293 subst_inductive_type_with_dummy_mutind term,
294 List.map subst_inductive_type_with_dummy_mutind pl)
296 C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
297 subst_inductive_type_with_dummy_mutind ty,
298 subst_inductive_type_with_dummy_mutind bo)) fl)
300 C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
301 subst_inductive_type_with_dummy_mutind ty,
302 subst_inductive_type_with_dummy_mutind bo)) fl)
303 | C.Const (uri,exp_named_subst) ->
304 let exp_named_subst' =
306 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
309 C.Const (uri,exp_named_subst')
310 | C.MutInd (uri,typeno,exp_named_subst) ->
311 let exp_named_subst' =
313 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
316 C.MutInd (uri,typeno,exp_named_subst')
317 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
318 let exp_named_subst' =
320 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
323 C.MutConstruct (uri,typeno,consno,exp_named_subst')
326 match CicReduction.whd context te with
327 C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
328 | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
329 | C.Prod (C.Anonymous,source,dest) ->
330 strictly_positive context n nn
331 (subst_inductive_type_with_dummy_mutind source) &&
332 weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
333 (n + 1) (nn + 1) uri dest
334 | C.Prod (name,source,dest) when
335 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
336 (* dummy abstraction, so we behave as in the anonimous case *)
337 strictly_positive context n nn
338 (subst_inductive_type_with_dummy_mutind source) &&
339 weakly_positive ((Some (name,(C.Decl source)))::context)
340 (n + 1) (nn + 1) uri dest
341 | C.Prod (name,source,dest) ->
342 does_not_occur context n nn
343 (subst_inductive_type_with_dummy_mutind source)&&
344 weakly_positive ((Some (name,(C.Decl source)))::context)
345 (n + 1) (nn + 1) uri dest
349 (NotWellFormedTypeOfInductiveConstructor
350 ("Guess where the error is ;-)")))
352 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
353 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
354 and instantiate_parameters params c =
355 let module C = Cic in
356 match (c,params) with
358 | (C.Prod (_,_,ta), he::tl) ->
359 instantiate_parameters tl
360 (CicSubstitution.subst he ta)
361 | (C.Cast (te,_), _) -> instantiate_parameters params te
362 | (t,l) -> raise (TypeCheckerFailure (Impossible 1))
364 and strictly_positive context n nn te =
365 let module C = Cic in
366 let module U = UriManager in
367 match CicReduction.whd context te with
370 (*CSC: bisogna controllare ty????*)
371 strictly_positive context n nn te
372 | C.Prod (name,so,ta) ->
373 does_not_occur context n nn so &&
374 strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
375 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
376 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
377 | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
378 let (ok,paramsno,ity,cl,name) =
379 match CicEnvironment.get_obj uri with
380 C.InductiveDefinition (tl,_,paramsno) ->
381 let (name,_,ity,cl) = List.nth tl i in
382 (List.length tl = 1, paramsno, ity, cl, name)
386 (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)))
388 let (params,arguments) = split tl paramsno in
389 let lifted_params = List.map (CicSubstitution.lift 1) params in
393 instantiate_parameters lifted_params
394 (CicSubstitution.subst_vars exp_named_subst te)
399 (fun x i -> i && does_not_occur context n nn x)
401 (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
406 ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri x
408 | t -> does_not_occur context n nn t
410 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
411 and are_all_occurrences_positive context uri indparamsno i n nn te =
412 let module C = Cic in
413 match CicReduction.whd context te with
414 C.Appl ((C.Rel m)::tl) when m = i ->
415 (*CSC: riscrivere fermandosi a 0 *)
416 (* let's check if the inductive type is applied at least to *)
417 (* indparamsno parameters *)
423 match CicReduction.whd context x with
424 C.Rel m when m = n - (indparamsno - k) -> k - 1
428 (WrongRequiredArgument (UriManager.string_of_uri uri)))
432 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
436 (WrongRequiredArgument (UriManager.string_of_uri uri)))
437 | C.Rel m when m = i ->
438 if indparamsno = 0 then
443 (WrongRequiredArgument (UriManager.string_of_uri uri)))
444 | C.Prod (C.Anonymous,source,dest) ->
445 strictly_positive context n nn source &&
446 are_all_occurrences_positive
447 ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
448 (i+1) (n + 1) (nn + 1) dest
449 | C.Prod (name,source,dest) when
450 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
451 (* dummy abstraction, so we behave as in the anonimous case *)
452 strictly_positive context n nn source &&
453 are_all_occurrences_positive
454 ((Some (name,(C.Decl source)))::context) uri indparamsno
455 (i+1) (n + 1) (nn + 1) dest
456 | C.Prod (name,source,dest) ->
457 does_not_occur context n nn source &&
458 are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
459 uri indparamsno (i+1) (n + 1) (nn + 1) dest
463 (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri)))
465 (* Main function to checks the correctness of a mutual *)
466 (* inductive block definition. This is the function *)
467 (* exported to the proof-engine. *)
468 and typecheck_mutual_inductive_defs uri (itl,_,indparamsno) =
469 let module U = UriManager in
470 (* let's check if the arity of the inductive types are well *)
472 List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
474 (* let's check if the types of the inductive constructors *)
475 (* are well formed. *)
476 (* In order not to use type_of_aux we put the types of the *)
477 (* mutual inductive types at the head of the types of the *)
478 (* constructors using Prods *)
479 let len = List.length itl in
481 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
487 let debrujinedte = debrujin_constructor uri len te in
490 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
493 let _ = type_of augmented_term in
494 (* let's check also the positivity conditions *)
497 (are_all_occurrences_positive tys uri indparamsno i 0 len
502 (NotPositiveOccurrences (U.string_of_uri uri)))
509 (* Main function to checks the correctness of a mutual *)
510 (* inductive block definition. *)
511 and check_mutual_inductive_defs uri =
513 Cic.InductiveDefinition (itl, params, indparamsno) ->
514 typecheck_mutual_inductive_defs uri (itl,params,indparamsno)
518 (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri)))
520 and type_of_mutual_inductive_defs uri i =
521 let module C = Cic in
522 let module R = CicReduction in
523 let module U = UriManager in
525 match CicEnvironment.is_type_checked ~trust:true uri with
526 CicEnvironment.CheckedObj cobj -> cobj
527 | CicEnvironment.UncheckedObj uobj ->
528 Logger.log (`Start_type_checking uri) ;
529 check_mutual_inductive_defs uri uobj ;
530 CicEnvironment.set_type_checking_info uri ;
531 Logger.log (`Type_checking_completed uri) ;
532 (match CicEnvironment.is_type_checked ~trust:false uri with
533 CicEnvironment.CheckedObj cobj -> cobj
534 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
538 C.InductiveDefinition (dl,_,_) ->
539 let (_,_,arity,_) = List.nth dl i in
544 (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)))
546 and type_of_mutual_inductive_constr uri i j =
547 let module C = Cic in
548 let module R = CicReduction in
549 let module U = UriManager in
551 match CicEnvironment.is_type_checked ~trust:true uri with
552 CicEnvironment.CheckedObj cobj -> cobj
553 | CicEnvironment.UncheckedObj uobj ->
554 Logger.log (`Start_type_checking uri) ;
555 check_mutual_inductive_defs uri uobj ;
556 CicEnvironment.set_type_checking_info uri ;
557 Logger.log (`Type_checking_completed uri) ;
558 (match CicEnvironment.is_type_checked ~trust:false uri with
559 CicEnvironment.CheckedObj cobj -> cobj
560 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
564 C.InductiveDefinition (dl,_,_) ->
565 let (_,_,_,cl) = List.nth dl i in
566 let (_,ty) = List.nth cl (j-1) in
571 (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)))
573 and recursive_args context n nn te =
574 let module C = Cic in
575 match CicReduction.whd context te with
581 | C.Cast _ (*CSC ??? *) ->
582 raise (TypeCheckerFailure (Impossible 3)) (* due to type-checking *)
583 | C.Prod (name,so,de) ->
584 (not (does_not_occur context n nn so)) ::
585 (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
588 raise (TypeCheckerFailure (Impossible 4)) (* due to type-checking *)
590 | C.Const _ -> raise (TypeCheckerFailure (Impossible 5))
596 raise (TypeCheckerFailure (Impossible 6)) (* due to type-checking *)
598 and get_new_safes context p c rl safes n nn x =
599 let module C = Cic in
600 let module U = UriManager in
601 let module R = CicReduction in
602 match (R.whd context c, R.whd context p, rl) with
603 (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
604 (* we are sure that the two sources are convertible because we *)
605 (* have just checked this. So let's go along ... *)
607 List.map (fun x -> x + 1) safes
610 if b then 1::safes' else safes'
612 get_new_safes ((Some (name,(C.Decl so)))::context)
613 ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
614 | (C.Prod _, (C.MutConstruct _ as e), _)
615 | (C.Prod _, (C.Rel _ as e), _)
616 | (C.MutInd _, e, [])
617 | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
619 (* CSC: If the next exception is raised, it just means that *)
620 (* CSC: the proof-assistant allows to use very strange things *)
621 (* CSC: as a branch of a case whose type is a Prod. In *)
622 (* CSC: particular, this means that a new (C.Prod, x,_) case *)
623 (* CSC: must be considered in this match. (e.g. x = MutCase) *)
624 raise (TypeCheckerFailure (Impossible 7))
626 and split_prods context n te =
627 let module C = Cic in
628 let module R = CicReduction in
629 match (n, R.whd context te) with
631 | (n, C.Prod (name,so,ta)) when n > 0 ->
632 split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta
633 | (_, _) -> raise (TypeCheckerFailure (Impossible 8))
635 and eat_lambdas context n te =
636 let module C = Cic in
637 let module R = CicReduction in
638 match (n, R.whd context te) with
639 (0, _) -> (te, 0, context)
640 | (n, C.Lambda (name,so,ta)) when n > 0 ->
641 let (te, k, context') =
642 eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
644 (te, k + 1, context')
645 | (_, _) -> raise (TypeCheckerFailure (Impossible 9))
647 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
648 and check_is_really_smaller_arg context n nn kl x safes te =
649 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
650 (*CSC: cfr guarded_by_destructors *)
651 let module C = Cic in
652 let module U = UriManager in
653 match CicReduction.whd context te with
654 C.Rel m when List.mem m safes -> true
661 (* | C.Cast (te,ty) ->
662 check_is_really_smaller_arg n nn kl x safes te &&
663 check_is_really_smaller_arg n nn kl x safes ty*)
664 (* | C.Prod (_,so,ta) ->
665 check_is_really_smaller_arg n nn kl x safes so &&
666 check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
667 (List.map (fun x -> x + 1) safes) ta*)
668 | C.Prod _ -> raise (TypeCheckerFailure (Impossible 10))
669 | C.Lambda (name,so,ta) ->
670 check_is_really_smaller_arg context n nn kl x safes so &&
671 check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context)
672 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
673 | C.LetIn (name,so,ta) ->
674 check_is_really_smaller_arg context n nn kl x safes so &&
675 check_is_really_smaller_arg ((Some (name,(C.Def so)))::context)
676 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
678 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
679 (*CSC: solo perche' non abbiamo trovato controesempi *)
680 check_is_really_smaller_arg context n nn kl x safes he
681 | C.Appl [] -> raise (TypeCheckerFailure (Impossible 11))
683 | C.MutInd _ -> raise (TypeCheckerFailure (Impossible 12))
684 | C.MutConstruct _ -> false
685 | C.MutCase (uri,i,outtype,term,pl) ->
687 C.Rel m when List.mem m safes || m = x ->
688 let (tys,len,isinductive,paramsno,cl) =
689 match CicEnvironment.get_obj uri with
690 C.InductiveDefinition (tl,_,paramsno) ->
692 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
694 let (_,isinductive,_,cl) = List.nth tl i in
698 (id, snd (split_prods tys paramsno ty))) cl
700 (tys,List.length tl,isinductive,paramsno,cl')
704 (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)))
706 if not isinductive then
709 i && check_is_really_smaller_arg context n nn kl x safes p)
715 let debrujinedte = debrujin_constructor uri len c in
716 recursive_args tys 0 len debrujinedte
718 let (e,safes',n',nn',x',context') =
719 get_new_safes context p c rl' safes n nn x
722 check_is_really_smaller_arg context' n' nn' kl x' safes' e
723 ) (List.combine pl cl) true
724 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
725 let (tys,len,isinductive,paramsno,cl) =
726 match CicEnvironment.get_obj uri with
727 C.InductiveDefinition (tl,_,paramsno) ->
728 let (_,isinductive,_,cl) = List.nth tl i in
730 List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
735 (id, snd (split_prods tys paramsno ty))) cl
737 (tys,List.length tl,isinductive,paramsno,cl')
741 (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)))
743 if not isinductive then
746 i && check_is_really_smaller_arg context n nn kl x safes p)
749 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
750 (*CSC: sugli argomenti di una applicazione *)
754 let debrujinedte = debrujin_constructor uri len c in
755 recursive_args tys 0 len debrujinedte
757 let (e, safes',n',nn',x',context') =
758 get_new_safes context p c rl' safes n nn x
761 check_is_really_smaller_arg context' n' nn' kl x' safes' e
762 ) (List.combine pl cl) true
766 i && check_is_really_smaller_arg context n nn kl x safes p
770 let len = List.length fl in
771 let n_plus_len = n + len
772 and nn_plus_len = nn + len
773 and x_plus_len = x + len
774 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
775 and safes' = List.map (fun x -> x + len) safes in
777 (fun (_,_,ty,bo) i ->
779 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
783 let len = List.length fl in
784 let n_plus_len = n + len
785 and nn_plus_len = nn + len
786 and x_plus_len = x + len
787 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
788 and safes' = List.map (fun x -> x + len) safes in
792 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
796 and guarded_by_destructors context n nn kl x safes =
797 let module C = Cic in
798 let module U = UriManager in
800 C.Rel m when m > n && m <= nn -> false
802 (match List.nth context (n-1) with
803 Some (_,C.Decl _) -> true
804 | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo
805 | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
811 guarded_by_destructors context n nn kl x safes te &&
812 guarded_by_destructors context n nn kl x safes ty
813 | C.Prod (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.Lambda (name,so,ta) ->
818 guarded_by_destructors context n nn kl x safes so &&
819 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
820 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
821 | C.LetIn (name,so,ta) ->
822 guarded_by_destructors context n nn kl x safes so &&
823 guarded_by_destructors ((Some (name,(C.Def so)))::context)
824 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
825 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
826 let k = List.nth kl (m - n - 1) in
827 if not (List.length tl > k) then false
831 i && guarded_by_destructors context n nn kl x safes param
833 check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
836 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
838 | C.Var (_,exp_named_subst)
839 | C.Const (_,exp_named_subst)
840 | C.MutInd (_,_,exp_named_subst)
841 | C.MutConstruct (_,_,_,exp_named_subst) ->
843 (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
845 | C.MutCase (uri,i,outtype,term,pl) ->
847 C.Rel m when List.mem m safes || m = x ->
848 let (tys,len,isinductive,paramsno,cl) =
849 match CicEnvironment.get_obj uri with
850 C.InductiveDefinition (tl,_,paramsno) ->
851 let (_,isinductive,_,cl) = List.nth tl i in
853 List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
858 (id, snd (split_prods tys paramsno ty))) cl
860 (tys,List.length tl,isinductive,paramsno,cl')
864 (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)))
866 if not isinductive then
867 guarded_by_destructors context n nn kl x safes outtype &&
868 guarded_by_destructors context n nn kl x safes term &&
869 (*CSC: manca ??? il controllo sul tipo di term? *)
872 i && guarded_by_destructors context n nn kl x safes p)
875 guarded_by_destructors context n nn kl x safes outtype &&
876 (*CSC: manca ??? il controllo sul tipo di term? *)
880 let debrujinedte = debrujin_constructor uri len c in
881 recursive_args tys 0 len debrujinedte
883 let (e,safes',n',nn',x',context') =
884 get_new_safes context p c rl' safes n nn x
887 guarded_by_destructors context' n' nn' kl x' safes' e
888 ) (List.combine pl cl) true
889 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
890 let (tys,len,isinductive,paramsno,cl) =
891 match CicEnvironment.get_obj uri with
892 C.InductiveDefinition (tl,_,paramsno) ->
893 let (_,isinductive,_,cl) = List.nth tl i in
895 List.map (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')
906 (WrongUriToMutualInductiveDefinitions(U.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 (TypeCheckerFailure (Impossible 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
1008 (WrongUriToMutualInductiveDefinitions
1009 (UriManager.string_of_uri uri)))
1011 let rec analyse_branch context ty te =
1012 match CicReduction.whd context ty with
1013 C.Meta _ -> raise (TypeCheckerFailure (Impossible 34))
1017 does_not_occur context n nn te
1020 raise (TypeCheckerFailure (Impossible 24))(* due to type-checking *)
1021 | C.Prod (name,so,de) ->
1022 analyse_branch ((Some (name,(C.Decl so)))::context) de te
1025 raise (TypeCheckerFailure (Impossible 25))(* due to type-checking *)
1026 | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1027 when uri == coInductiveTypeURI ->
1028 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1029 | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1030 guarded_by_constructors context n nn true te tl coInductiveTypeURI
1032 does_not_occur context n nn te
1033 | C.Const _ -> raise (TypeCheckerFailure (Impossible 26))
1034 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1035 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1037 does_not_occur context n nn te
1038 | C.MutConstruct _ -> raise (TypeCheckerFailure (Impossible 27))
1039 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1040 (*CSC: in head position. *)
1044 raise (TypeCheckerFailure (Impossible 28))(* due to type-checking *)
1046 let rec analyse_instantiated_type context ty l =
1047 match CicReduction.whd context ty with
1054 raise (TypeCheckerFailure (Impossible 29))(* due to type-checking *)
1055 | C.Prod (name,so,de) ->
1060 analyse_branch context so he &&
1061 analyse_instantiated_type ((Some (name,(C.Decl so)))::context)
1066 raise (TypeCheckerFailure (Impossible 30))(* due to type-checking *)
1069 (fun i x -> i && does_not_occur context n nn x) true l
1070 | C.Const _ -> raise (TypeCheckerFailure (Impossible 31))
1073 (fun i x -> i && does_not_occur context n nn x) true l
1074 | C.MutConstruct _ -> raise (TypeCheckerFailure (Impossible 32))
1075 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1076 (*CSC: in head position. *)
1080 raise (TypeCheckerFailure (Impossible 33))(* due to type-checking *)
1082 let rec instantiate_type args consty =
1085 | tlhe::tltl as l ->
1086 let consty' = CicReduction.whd context consty in
1092 let instantiated_de = CicSubstitution.subst he de in
1093 (*CSC: siamo sicuri che non sia troppo forte? *)
1094 does_not_occur context n nn tlhe &
1095 instantiate_type tl instantiated_de tltl
1097 (*CSC:We do not consider backbones with a MutCase, a *)
1098 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1099 raise (TypeCheckerFailure (Impossible 23))
1101 | [] -> analyse_instantiated_type context consty' l
1102 (* These are all the other cases *)
1104 instantiate_type args consty tl
1105 | C.Appl ((C.CoFix (_,fl))::tl) ->
1106 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1107 let len = List.length fl in
1108 let n_plus_len = n + len
1109 and nn_plus_len = nn + len
1110 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1111 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1114 i && does_not_occur context n nn ty &&
1115 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1116 args coInductiveTypeURI
1118 | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1119 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1120 does_not_occur context n nn out &&
1121 does_not_occur context n nn te &&
1125 guarded_by_constructors context n nn h x args coInductiveTypeURI
1128 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1129 | C.Var (_,exp_named_subst)
1130 | C.Const (_,exp_named_subst) ->
1132 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1133 | C.MutInd _ -> assert false
1134 | C.MutConstruct (_,_,_,exp_named_subst) ->
1136 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1137 | C.MutCase (_,_,out,te,pl) ->
1138 does_not_occur context n nn out &&
1139 does_not_occur context n nn te &&
1143 guarded_by_constructors context n nn h x args coInductiveTypeURI
1146 let len = List.length fl in
1147 let n_plus_len = n + len
1148 and nn_plus_len = nn + len
1149 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1150 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1152 (fun (_,_,ty,bo) i ->
1153 i && does_not_occur context n nn ty &&
1154 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1157 let len = List.length fl in
1158 let n_plus_len = n + len
1159 and nn_plus_len = nn + len
1160 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1161 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1164 i && does_not_occur context n nn ty &&
1165 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1166 args coInductiveTypeURI
1169 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1170 let module C = Cic in
1171 let module U = UriManager in
1172 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1173 (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1174 when CicReduction.are_convertible context so1 so2 ->
1175 check_allowed_sort_elimination context uri i need_dummy
1176 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1177 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1178 | (C.Sort C.Prop, C.Sort C.Set)
1179 | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
1180 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1181 (match CicEnvironment.get_obj uri with
1182 C.InductiveDefinition (itl,_,_) ->
1183 let (_,_,_,cl) = List.nth itl i in
1184 (* is a singleton definition or the empty proposition? *)
1185 List.length cl = 1 || List.length cl = 0
1189 (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)))
1191 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1192 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1193 | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
1194 (match CicEnvironment.get_obj uri with
1195 C.InductiveDefinition (itl,_,paramsno) ->
1197 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1199 let (_,_,_,cl) = List.nth itl i in
1201 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1205 (WrongUriToMutualInductiveDefinitions (U.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
1215 (match CicEnvironment.get_obj uri with
1216 C.InductiveDefinition (itl,_,_) ->
1217 let (_,_,_,cl) = List.nth itl i in
1218 (* is a singleton definition? *)
1223 (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)))
1227 | (C.Sort C.Set, C.Prod (name,so,ta)) when not need_dummy ->
1228 let res = CicReduction.are_convertible context so ind
1231 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1233 | C.Sort C.Set -> true
1235 (match CicEnvironment.get_obj uri with
1236 C.InductiveDefinition (itl,_,paramsno) ->
1237 let (_,_,_,cl) = List.nth itl i in
1240 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1243 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1247 (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)))
1249 | _ -> raise (TypeCheckerFailure (Impossible 19))
1251 | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
1252 CicReduction.are_convertible context so ind
1255 and type_of_branch context argsno need_dummy outtype term constype =
1256 let module C = Cic in
1257 let module R = CicReduction in
1258 match R.whd context constype with
1263 C.Appl [outtype ; term]
1264 | C.Appl (C.MutInd (_,_,_)::tl) ->
1265 let (_,arguments) = split tl argsno
1267 if need_dummy && arguments = [] then
1270 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1271 | C.Prod (name,so,de) ->
1273 match CicSubstitution.lift 1 term with
1274 C.Appl l -> C.Appl (l@[C.Rel 1])
1275 | t -> C.Appl [t ; C.Rel 1]
1277 C.Prod (C.Anonymous,so,type_of_branch
1278 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1279 (CicSubstitution.lift 1 outtype) term' de)
1280 | _ -> raise (TypeCheckerFailure (Impossible 20))
1282 (* check_metasenv_consistency checks that the "canonical" context of a
1283 metavariable is consitent - up to relocation via the relocation list l -
1284 with the actual context *)
1286 and check_metasenv_consistency metasenv context canonical_context l =
1287 let module C = Cic in
1288 let module R = CicReduction in
1289 let module S = CicSubstitution in
1290 let lifted_canonical_context =
1294 | (Some (n,C.Decl t))::tl ->
1295 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1296 | (Some (n,C.Def t))::tl ->
1297 (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1298 | None::tl -> None::(aux (i+1) tl)
1300 aux 1 canonical_context
1307 | Some t,Some (_,C.Def ct) ->
1308 R.are_convertible context t ct
1309 | Some t,Some (_,C.Decl ct) ->
1310 R.are_convertible context (type_of_aux' metasenv context t) ct
1313 if not res then raise (TypeCheckerFailure MetasenvInconsistency)
1314 ) l lifted_canonical_context
1316 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1317 and type_of_aux' metasenv context t =
1318 let rec type_of_aux context =
1319 let module C = Cic in
1320 let module R = CicReduction in
1321 let module S = CicSubstitution in
1322 let module U = UriManager in
1326 match List.nth context (n - 1) with
1327 Some (_,C.Decl t) -> S.lift n t
1328 | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
1329 | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
1331 _ -> raise (TypeCheckerFailure (NotWellTyped "Not a close term"))
1333 | C.Var (uri,exp_named_subst) ->
1335 check_exp_named_subst context exp_named_subst ;
1337 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1342 let (_,canonical_context,ty) =
1343 List.find (function (m,_,_) -> n = m) metasenv
1345 check_metasenv_consistency metasenv context canonical_context l;
1346 CicSubstitution.lift_meta l ty
1347 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1348 | C.Implicit -> raise (TypeCheckerFailure (Impossible 21))
1350 let _ = type_of_aux context ty in
1351 if R.are_convertible context (type_of_aux context te) ty then ty
1352 else raise (TypeCheckerFailure (NotWellTyped "Cast"))
1353 | C.Prod (name,s,t) ->
1354 let sort1 = type_of_aux context s
1355 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1356 sort_of_prod context (name,s) (sort1,sort2)
1357 | C.Lambda (n,s,t) ->
1358 let sort1 = type_of_aux context s
1359 and type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1360 let sort2 = type_of_aux ((Some (n,(C.Decl s)))::context) type2 in
1361 (* only to check if the product is well-typed *)
1362 let _ = sort_of_prod context (n,s) (sort1,sort2) in
1364 | C.LetIn (n,s,t) ->
1365 (* only to check if s is well-typed *)
1366 let _ = type_of_aux context s in
1367 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1368 LetIn is later reduced and maybe also re-checked.
1369 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1371 (* The type of the LetIn is reduced. Much faster than the previous
1372 solution. Moreover the inferred type is probably very different
1373 from the expected one.
1374 (CicReduction.whd context
1375 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1377 (* One-step LetIn reduction. Even faster than the previous solution.
1378 Moreover the inferred type is closer to the expected one. *)
1379 (CicSubstitution.subst s
1380 (type_of_aux ((Some (n,(C.Def s)))::context) t))
1381 | C.Appl (he::tl) when List.length tl > 0 ->
1382 let hetype = type_of_aux context he
1383 and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1384 eat_prods context hetype tlbody_and_type
1385 | C.Appl _ -> raise (TypeCheckerFailure (NotWellTyped "Appl: no arguments"))
1386 | C.Const (uri,exp_named_subst) ->
1388 check_exp_named_subst context exp_named_subst ;
1390 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1394 | C.MutInd (uri,i,exp_named_subst) ->
1396 check_exp_named_subst context exp_named_subst ;
1398 CicSubstitution.subst_vars exp_named_subst
1399 (type_of_mutual_inductive_defs uri i)
1403 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1404 check_exp_named_subst context exp_named_subst ;
1406 CicSubstitution.subst_vars exp_named_subst
1407 (type_of_mutual_inductive_constr uri i j)
1410 | C.MutCase (uri,i,outtype,term,pl) ->
1411 let outsort = type_of_aux context outtype in
1412 let (need_dummy, k) =
1413 let rec guess_args context t =
1414 match CicReduction.whd context t with
1415 C.Sort _ -> (true, 0)
1416 | C.Prod (name, s, t) ->
1417 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1419 (* last prod before sort *)
1420 match CicReduction.whd context s with
1421 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1422 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1424 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1425 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1426 when U.eq uri' uri && i' = i -> (false, 1)
1432 (TypeCheckerFailure (NotWellTyped "MutCase: outtype ill-formed"))
1434 (*CSC whd non serve dopo type_of_aux ? *)
1435 let (b, k) = guess_args context outsort in
1436 if not b then (b, k - 1) else (b, k)
1438 let (parameters, arguments, exp_named_subst) =
1439 match R.whd context (type_of_aux context term) with
1440 (*CSC manca il caso dei CAST *)
1441 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1442 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
1443 (*CSC: Hint: nella DTD servono per gli stylesheet. *)
1444 C.MutInd (uri',i',exp_named_subst) as typ ->
1445 if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1446 else raise (TypeCheckerFailure
1447 (NotWellTyped ("MutCase: the term is of type " ^
1449 " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^
1450 string_of_int i ^ "{_}")))
1451 | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
1452 if U.eq uri uri' && i = i' then
1454 split tl (List.length tl - k)
1455 in params,args,exp_named_subst
1456 else raise (TypeCheckerFailure (NotWellTyped
1457 ("MutCase: the term is of type " ^
1459 " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^
1460 string_of_int i ^ "{_}")))
1461 | _ -> raise (TypeCheckerFailure
1462 (NotWellTyped "MutCase: the term is not an inductive one"))
1464 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1465 let sort_of_ind_type =
1466 if parameters = [] then
1467 C.MutInd (uri,i,exp_named_subst)
1469 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1471 if not (check_allowed_sort_elimination context uri i need_dummy
1472 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1476 (NotWellTyped "MutCase: not allowed sort elimination")) ;
1478 (* let's check if the type of branches are right *)
1480 match CicEnvironment.get_cooked_obj ~trust:false uri with
1481 C.InductiveDefinition (_,_,parsno) -> parsno
1485 (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)))
1487 let (_,branches_ok) =
1491 if parameters = [] then
1492 (C.MutConstruct (uri,i,j,exp_named_subst))
1494 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1501 R.are_convertible context (type_of_aux context p)
1502 (type_of_branch context parsno need_dummy outtype cons
1503 (type_of_aux context cons))
1504 in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res
1508 if not branches_ok then
1511 (NotWellTyped "MutCase: wrong type of a branch")) ;
1513 if not need_dummy then
1514 C.Appl ((outtype::arguments)@[term])
1515 else if arguments = [] then
1518 C.Appl (outtype::arguments)
1520 let types_times_kl =
1524 let _ = type_of_aux context ty in
1525 (Some (C.Name n,(C.Decl ty)),k)) fl)
1527 let (types,kl) = List.split types_times_kl in
1528 let len = List.length types in
1530 (fun (name,x,ty,bo) ->
1532 (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1533 (CicSubstitution.lift len ty))
1536 let (m, eaten, context') =
1537 eat_lambdas (types @ context) (x + 1) bo
1539 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1542 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1546 (NotWellTyped "Fix: not guarded by destructors"))
1549 raise (TypeCheckerFailure (NotWellTyped "Fix: ill-typed bodies"))
1552 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1553 let (_,_,ty,_) = List.nth fl i in
1560 let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1562 let len = List.length types in
1566 (R.are_convertible (types @ context)
1567 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1570 (* let's control that the returned type is coinductive *)
1571 match returns_a_coinductive context ty with
1575 (NotWellTyped "CoFix: does not return a coinductive type"))
1577 (*let's control the guarded by constructors conditions C{f,M}*)
1580 (guarded_by_constructors (types @ context) 0 len false bo
1585 (NotWellTyped "CoFix: not guarded by constructors"))
1590 (NotWellTyped "CoFix: ill-typed bodies"))
1593 let (_,ty,_) = List.nth fl i in
1596 and check_exp_named_subst context =
1597 let rec check_exp_named_subst_aux substs =
1600 | ((uri,t) as subst)::tl ->
1602 CicSubstitution.subst_vars substs (type_of_variable uri) in
1603 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1604 Cic.Variable (_,Some bo,_,_) ->
1608 "A variable with a body can not be explicit substituted"))
1609 | Cic.Variable (_,None,_,_) -> ()
1613 (WrongUriToVariable (UriManager.string_of_uri uri)))
1615 let typeoft = type_of_aux context t in
1616 if CicReduction.are_convertible context typeoft typeofvar then
1617 check_exp_named_subst_aux (substs@[subst]) tl
1620 CicReduction.fdebug := 0 ;
1621 ignore (CicReduction.are_convertible context typeoft typeofvar) ;
1623 debug typeoft [typeofvar] ;
1626 (NotWellTyped "Wrong Explicit Named Substitution"))
1629 check_exp_named_subst_aux []
1631 and sort_of_prod context (name,s) (t1, t2) =
1632 let module C = Cic in
1633 let t1' = CicReduction.whd context t1 in
1634 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1635 match (t1', t2') with
1636 (C.Sort s1, C.Sort s2)
1637 when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
1639 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1644 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= "^ CicPp.ppterm t2')))
1646 and eat_prods context hetype =
1647 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1651 | (hete, hety)::tl ->
1652 (match (CicReduction.whd context hetype) with
1654 if CicReduction.are_convertible context s hety then
1655 (CicReduction.fdebug := -1 ;
1656 eat_prods context (CicSubstitution.subst hete t) tl
1660 CicReduction.fdebug := 0 ;
1661 ignore (CicReduction.are_convertible context s hety) ;
1665 (TypeCheckerFailure (NotWellTyped "Appl: wrong parameter-type"))
1667 | _ -> raise (TypeCheckerFailure (NotWellTyped "Appl: wrong Prod-type"))
1670 and returns_a_coinductive context ty =
1671 let module C = Cic in
1672 match CicReduction.whd context ty with
1673 C.MutInd (uri,i,_) ->
1674 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1675 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1676 C.InductiveDefinition (itl,_,_) ->
1677 let (_,is_inductive,_,_) = List.nth itl i in
1678 if is_inductive then None else (Some uri)
1681 (TypeCheckerFailure (WrongUriToMutualInductiveDefinitions
1682 (UriManager.string_of_uri uri)))
1684 | C.Appl ((C.MutInd (uri,i,_))::_) ->
1685 (match CicEnvironment.get_obj uri with
1686 C.InductiveDefinition (itl,_,_) ->
1687 let (_,is_inductive,_,_) = List.nth itl i in
1688 if is_inductive then None else (Some uri)
1692 (WrongUriToMutualInductiveDefinitions
1693 (UriManager.string_of_uri uri)))
1695 | C.Prod (n,so,de) ->
1696 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1701 prerr_endline ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1704 type_of_aux context t
1706 in prerr_endline "FINE TYPE_OF_AUX" ; flush stderr ; res
1709 (* is a small constructor? *)
1710 (*CSC: ottimizzare calcolando staticamente *)
1711 and is_small context paramsno c =
1712 let rec is_small_aux context c =
1713 let module C = Cic in
1714 match CicReduction.whd context c with
1716 (*CSC: [] is an empty metasenv. Is it correct? *)
1717 let s = type_of_aux' [] context so in
1718 (s = C.Sort C.Prop || s = C.Sort C.Set) &&
1719 is_small_aux ((Some (n,(C.Decl so)))::context) de
1720 | _ -> true (*CSC: we trust the type-checker *)
1722 let (context',dx) = split_prods context paramsno c in
1723 is_small_aux context' dx
1727 prerr_endline ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1730 type_of_aux' [] [] t
1732 in prerr_endline "FINE TYPE_OF_AUX'" ; flush stderr ; res
1737 let module C = Cic in
1738 let module R = CicReduction in
1739 let module U = UriManager in
1740 match CicEnvironment.is_type_checked ~trust:false uri with
1741 CicEnvironment.CheckedObj _ -> ()
1742 | CicEnvironment.UncheckedObj uobj ->
1743 (* let's typecheck the uncooked object *)
1744 Logger.log (`Start_type_checking uri) ;
1746 C.Constant (_,Some te,ty,_) ->
1747 let _ = type_of ty in
1748 if not (R.are_convertible [] (type_of te ) ty) then
1751 (NotWellTyped ("Constant " ^ (U.string_of_uri uri))))
1752 | C.Constant (_,None,ty,_) ->
1753 (* only to check that ty is well-typed *)
1754 let _ = type_of ty in ()
1755 | C.CurrentProof (_,conjs,te,ty,_) ->
1758 (fun metasenv ((_,context,ty) as conj) ->
1759 ignore (type_of_aux' metasenv context ty) ;
1763 let _ = type_of_aux' conjs [] ty in
1764 if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
1768 (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))))
1769 | C.Variable (_,bo,ty,_) ->
1770 (* only to check that ty is well-typed *)
1771 let _ = type_of ty in
1775 if not (R.are_convertible [] (type_of bo) ty) then
1778 (NotWellTyped ("Variable" ^ (U.string_of_uri uri))))
1780 | C.InductiveDefinition _ ->
1781 check_mutual_inductive_defs uri uobj
1783 CicEnvironment.set_type_checking_info uri ;
1784 Logger.log (`Type_checking_completed uri)