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 exception Impossible of int;;
27 exception NotWellTyped of string;;
28 exception WrongUriToConstant of string;;
29 exception WrongUriToVariable of string;;
30 exception WrongUriToMutualInductiveDefinitions of string;;
31 exception ListTooShort;;
32 exception NotPositiveOccurrences of string;;
33 exception NotWellFormedTypeOfInductiveConstructor of string;;
34 exception WrongRequiredArgument of string;;
38 let rec debug_aux t i =
40 let module U = UriManager in
41 CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i
44 raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::context) ""))
45 (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
51 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
52 | (_,_) -> raise ListTooShort
55 exception CicEnvironmentError;;
57 let rec cooked_type_of_constant uri cookingsno =
59 let module R = CicReduction in
60 let module U = UriManager in
62 match CicEnvironment.is_type_checked uri cookingsno with
63 CicEnvironment.CheckedObj cobj -> cobj
64 | CicEnvironment.UncheckedObj uobj ->
65 Logger.log (`Start_type_checking uri) ;
66 (* let's typecheck the uncooked obj *)
68 C.Definition (_,te,ty,_) ->
70 if not (R.are_convertible [] (type_of te) ty) then
71 raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
73 (* only to check that ty is well-typed *)
74 let _ = type_of ty in ()
75 | C.CurrentProof (_,conjs,te,ty) ->
76 let _ = type_of_aux' conjs [] ty in
77 if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
79 raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
80 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
82 CicEnvironment.set_type_checking_info uri ;
83 Logger.log (`Type_checking_completed uri) ;
84 match CicEnvironment.is_type_checked uri cookingsno with
85 CicEnvironment.CheckedObj cobj -> cobj
86 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
89 C.Definition (_,_,ty,_) -> ty
90 | C.Axiom (_,ty,_) -> ty
91 | C.CurrentProof (_,_,_,ty) -> ty
92 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
94 and type_of_variable uri =
96 let module R = CicReduction in
97 let module U = UriManager in
98 (* 0 because a variable is never cooked => no partial cooking at one level *)
99 match CicEnvironment.is_type_checked uri 0 with
100 CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
101 | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty)) ->
102 Logger.log (`Start_type_checking uri) ;
103 (* only to check that ty is well-typed *)
104 let _ = type_of ty in
108 if not (R.are_convertible [] (type_of bo) ty) then
109 raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
111 CicEnvironment.set_type_checking_info uri ;
112 Logger.log (`Type_checking_completed uri) ;
114 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
116 and does_not_occur context n nn te =
117 let module C = Cic in
118 (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
119 (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
121 match CicReduction.whd context te with
122 C.Rel m when m > n && m <= nn -> false
129 does_not_occur context n nn te && does_not_occur context n nn ty
130 | C.Prod (_,so,dest) ->
131 does_not_occur context n nn so &&
132 does_not_occur ((C.Decl so)::context) (n + 1) (nn + 1) dest
133 | C.Lambda (_,so,dest) ->
134 does_not_occur context n nn so &&
135 does_not_occur ((C.Decl so)::context) (n + 1) (nn + 1) dest
136 | C.LetIn (_,so,dest) ->
137 does_not_occur context n nn so &&
138 does_not_occur ((C.Def so)::context) (n + 1) (nn + 1) dest
140 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
144 | C.MutConstruct _ -> true
145 | C.MutCase (_,_,_,out,te,pl) ->
146 does_not_occur context n nn out && does_not_occur context n nn te &&
147 List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
149 let len = List.length fl in
150 let n_plus_len = n + len in
151 let nn_plus_len = nn + len in
152 let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) fl in
154 (fun (_,_,ty,bo) i ->
155 i && does_not_occur context n nn ty &&
156 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
159 let len = List.length fl in
160 let n_plus_len = n + len in
161 let nn_plus_len = nn + len in
162 let tys = List.map (fun (_,ty,_) -> Cic.Decl ty) fl in
165 i && does_not_occur context n nn ty &&
166 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
169 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
170 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
171 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
172 (*CSC strictly_positive *)
173 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
174 and weakly_positive context n nn uri te =
175 let module C = Cic in
176 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
178 C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,0)
180 (*CSC mettere in cicSubstitution *)
181 let rec subst_inductive_type_with_dummy_mutind =
183 C.MutInd (uri',_,0) when UriManager.eq uri' uri ->
185 | C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri ->
187 | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
188 | C.Prod (name,so,ta) ->
189 C.Prod (name, subst_inductive_type_with_dummy_mutind so,
190 subst_inductive_type_with_dummy_mutind ta)
191 | C.Lambda (name,so,ta) ->
192 C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
193 subst_inductive_type_with_dummy_mutind ta)
195 C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
196 | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
197 C.MutCase (uri,cookingsno,i,
198 subst_inductive_type_with_dummy_mutind outtype,
199 subst_inductive_type_with_dummy_mutind term,
200 List.map subst_inductive_type_with_dummy_mutind pl)
202 C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
203 subst_inductive_type_with_dummy_mutind ty,
204 subst_inductive_type_with_dummy_mutind bo)) fl)
206 C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
207 subst_inductive_type_with_dummy_mutind ty,
208 subst_inductive_type_with_dummy_mutind bo)) fl)
211 match CicReduction.whd context te with
212 C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri -> true
213 | C.MutInd (uri',_,0) when UriManager.eq uri' uri -> true
214 | C.Prod (C.Anonimous,source,dest) ->
215 strictly_positive context n nn
216 (subst_inductive_type_with_dummy_mutind source) &&
217 weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest
218 | C.Prod (name,source,dest) when
219 does_not_occur ((C.Decl source)::context) 0 n dest ->
220 (* dummy abstraction, so we behave as in the anonimous case *)
221 strictly_positive context n nn
222 (subst_inductive_type_with_dummy_mutind source) &&
223 weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest
224 | C.Prod (_,source,dest) ->
225 does_not_occur context n nn
226 (subst_inductive_type_with_dummy_mutind source)&&
227 weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest
228 | _ -> raise (NotWellFormedTypeOfInductiveConstructor ("Guess where the error is ;-)"))
230 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
231 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
232 and instantiate_parameters params c =
233 let module C = Cic in
234 match (c,params) with
236 | (C.Prod (_,_,ta), he::tl) ->
237 instantiate_parameters tl
238 (CicSubstitution.subst he ta)
239 | (C.Cast (te,_), _) -> instantiate_parameters params te
240 | (t,l) -> raise (Impossible 1)
242 and strictly_positive context n nn te =
243 let module C = Cic in
244 let module U = UriManager in
245 match CicReduction.whd context te with
248 (*CSC: bisogna controllare ty????*)
249 strictly_positive context n nn te
250 | C.Prod (_,so,ta) ->
251 does_not_occur context n nn so &&
252 strictly_positive ((C.Decl so)::context) (n+1) (nn+1) ta
253 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
254 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
255 | C.Appl ((C.MutInd (uri,_,i))::tl) ->
256 let (ok,paramsno,ity,cl) =
257 match CicEnvironment.get_obj uri with
258 C.InductiveDefinition (tl,_,paramsno) ->
259 let (_,_,ity,cl) = List.nth tl i in
260 (List.length tl = 1, paramsno, ity, cl)
261 | _ -> raise(WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
263 let (params,arguments) = split tl paramsno in
264 let lifted_params = List.map (CicSubstitution.lift 1) params in
266 List.map (fun (_,te,_) -> instantiate_parameters lifted_params te) cl
270 (fun x i -> i && does_not_occur context n nn x)
272 (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
276 weakly_positive ((Cic.Decl ity)::context) (n+1) (nn+1) uri x
278 | t -> does_not_occur context n nn t
280 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
281 and are_all_occurrences_positive context uri indparamsno i n nn te =
282 let module C = Cic in
283 match CicReduction.whd context te with
284 C.Appl ((C.Rel m)::tl) when m = i ->
285 (*CSC: riscrivere fermandosi a 0 *)
286 (* let's check if the inductive type is applied at least to *)
287 (* indparamsno parameters *)
293 match CicReduction.whd context x with
294 C.Rel m when m = n - (indparamsno - k) -> k - 1
295 | _ -> raise (WrongRequiredArgument (UriManager.string_of_uri uri))
299 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
301 raise (WrongRequiredArgument (UriManager.string_of_uri uri))
302 | C.Rel m when m = i ->
303 if indparamsno = 0 then
306 raise (WrongRequiredArgument (UriManager.string_of_uri uri))
307 | C.Prod (C.Anonimous,source,dest) ->
308 strictly_positive context n nn source &&
309 are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno
310 (i+1) (n + 1) (nn + 1) dest
311 | C.Prod (name,source,dest) when
312 does_not_occur ((C.Decl source)::context) 0 n dest ->
313 (* dummy abstraction, so we behave as in the anonimous case *)
314 strictly_positive context n nn source &&
315 are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno
316 (i+1) (n + 1) (nn + 1) dest
317 | C.Prod (_,source,dest) ->
318 does_not_occur context n nn source &&
319 are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno
320 (i+1) (n + 1) (nn + 1) dest
321 | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri))
323 (*CSC: cambiare il nome, torna unit! *)
324 and cooked_mutual_inductive_defs uri =
325 let module U = UriManager in
327 Cic.InductiveDefinition (itl, _, indparamsno) ->
328 (* let's check if the arity of the inductive types are well *)
330 List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
332 (* let's check if the types of the inductive constructors *)
333 (* are well formed. *)
334 (* In order not to use type_of_aux we put the types of the *)
335 (* mutual inductive types at the head of the types of the *)
336 (* constructors using Prods *)
337 (*CSC: piccola??? inefficienza *)
338 let len = List.length itl in
339 (*CSC: siamo sicuri che non debba fare anche un List.rev? Il bug *)
340 (*CSC: si manifesterebbe solamene con tipi veramente mutualmente *)
341 (*CSC: induttivi... *)
342 let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in
350 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
353 let _ = type_of augmented_term in
354 (* let's check also the positivity conditions *)
357 (are_all_occurrences_positive tys uri indparamsno i 0 len te)
359 raise (NotPositiveOccurrences (U.string_of_uri uri))
362 Some _ -> raise (Impossible 2)
363 | None -> r := Some (recursive_args tys 0 len te)
370 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
372 and cooked_type_of_mutual_inductive_defs uri cookingsno i =
373 let module C = Cic in
374 let module R = CicReduction in
375 let module U = UriManager in
377 match CicEnvironment.is_type_checked uri cookingsno with
378 CicEnvironment.CheckedObj cobj -> cobj
379 | CicEnvironment.UncheckedObj uobj ->
380 Logger.log (`Start_type_checking uri) ;
381 cooked_mutual_inductive_defs uri uobj ;
382 CicEnvironment.set_type_checking_info uri ;
383 Logger.log (`Type_checking_completed uri) ;
384 (match CicEnvironment.is_type_checked uri cookingsno with
385 CicEnvironment.CheckedObj cobj -> cobj
386 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
390 C.InductiveDefinition (dl,_,_) ->
391 let (_,_,arity,_) = List.nth dl i in
393 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
395 and cooked_type_of_mutual_inductive_constr uri cookingsno i j =
396 let module C = Cic in
397 let module R = CicReduction in
398 let module U = UriManager in
400 match CicEnvironment.is_type_checked uri cookingsno with
401 CicEnvironment.CheckedObj cobj -> cobj
402 | CicEnvironment.UncheckedObj uobj ->
403 Logger.log (`Start_type_checking uri) ;
404 cooked_mutual_inductive_defs uri uobj ;
405 CicEnvironment.set_type_checking_info uri ;
406 Logger.log (`Type_checking_completed uri) ;
407 (match CicEnvironment.is_type_checked uri cookingsno with
408 CicEnvironment.CheckedObj cobj -> cobj
409 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
413 C.InductiveDefinition (dl,_,_) ->
414 let (_,_,_,cl) = List.nth dl i in
415 let (_,ty,_) = List.nth cl (j-1) in
417 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
419 and recursive_args context n nn te =
420 let module C = Cic in
421 match CicReduction.whd context te with
427 | C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *)
428 | C.Prod (_,so,de) ->
429 (not (does_not_occur context n nn so)) ::
430 (recursive_args ((C.Decl so)::context) (n+1) (nn + 1) de)
432 | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *)
435 | C.Abst _ -> raise (Impossible 5)
440 | C.CoFix _ -> raise (Impossible 6) (* due to type-checking *)
442 and get_new_safes context p c rl safes n nn x =
443 let module C = Cic in
444 let module U = UriManager in
445 let module R = CicReduction in
446 match (R.whd context c, R.whd context p, rl) with
447 (C.Prod (_,so,ta1), C.Lambda (_,_,ta2), b::tl) ->
448 (* we are sure that the two sources are convertible because we *)
449 (* have just checked this. So let's go along ... *)
451 List.map (fun x -> x + 1) safes
454 if b then 1::safes' else safes'
456 get_new_safes ((C.Decl so)::context) ta2 ta1 tl safes'' (n+1) (nn+1)
458 | (C.Prod _, (C.MutConstruct _ as e), _)
459 | (C.Prod _, (C.Rel _ as e), _)
460 | (C.MutInd _, e, [])
461 | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
463 (* CSC: If the next exception is raised, it just means that *)
464 (* CSC: the proof-assistant allows to use very strange things *)
465 (* CSC: as a branch of a case whose type is a Prod. In *)
466 (* CSC: particular, this means that a new (C.Prod, x,_) case *)
467 (* CSC: must be considered in this match. (e.g. x = MutCase) *)
470 and split_prods context n te =
471 let module C = Cic in
472 let module R = CicReduction in
473 match (n, R.whd context te) with
475 | (n, C.Prod (_,so,ta)) when n > 0 ->
476 split_prods ((C.Decl so)::context) (n - 1) ta
477 | (_, _) -> raise (Impossible 8)
479 and eat_lambdas context n te =
480 let module C = Cic in
481 let module R = CicReduction in
482 match (n, R.whd context te) with
483 (0, _) -> (te, 0, context)
484 | (n, C.Lambda (_,so,ta)) when n > 0 ->
485 let (te, k, context') = eat_lambdas ((C.Decl so)::context) (n - 1) ta in
486 (te, k + 1, context')
487 | (_, _) -> raise (Impossible 9)
489 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
490 and check_is_really_smaller_arg context n nn kl x safes te =
491 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
492 (*CSC: cfr guarded_by_destructors *)
493 let module C = Cic in
494 let module U = UriManager in
495 match CicReduction.whd context te with
496 C.Rel m when List.mem m safes -> true
503 (* | C.Cast (te,ty) ->
504 check_is_really_smaller_arg n nn kl x safes te &&
505 check_is_really_smaller_arg n nn kl x safes ty*)
506 (* | C.Prod (_,so,ta) ->
507 check_is_really_smaller_arg n nn kl x safes so &&
508 check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
509 (List.map (fun x -> x + 1) safes) ta*)
510 | C.Prod _ -> raise (Impossible 10)
511 | C.Lambda (_,so,ta) ->
512 check_is_really_smaller_arg context n nn kl x safes so &&
513 check_is_really_smaller_arg ((C.Decl so)::context) (n+1) (nn+1) kl (x+1)
514 (List.map (fun x -> x + 1) safes) ta
515 | C.LetIn (_,so,ta) ->
516 check_is_really_smaller_arg context n nn kl x safes so &&
517 check_is_really_smaller_arg ((C.Def so)::context) (n+1) (nn+1) kl (x+1)
518 (List.map (fun x -> x + 1) safes) ta
520 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
521 (*CSC: solo perche' non abbiamo trovato controesempi *)
522 check_is_really_smaller_arg context n nn kl x safes he
523 | C.Appl [] -> raise (Impossible 11)
526 | C.MutInd _ -> raise (Impossible 12)
527 | C.MutConstruct _ -> false
528 | C.MutCase (uri,_,i,outtype,term,pl) ->
530 C.Rel m when List.mem m safes || m = x ->
531 let (isinductive,paramsno,cl) =
532 match CicEnvironment.get_obj uri with
533 C.InductiveDefinition (tl,_,paramsno) ->
534 let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in
535 let (_,isinductive,_,cl) = List.nth tl i in
539 (id, snd (split_prods tys paramsno ty), r)) cl
541 (isinductive,paramsno,cl')
543 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
545 if not isinductive then
548 i && check_is_really_smaller_arg context n nn kl x safes p)
552 (fun (p,(_,c,rl)) i ->
556 let (_,rl'') = split rl' paramsno in
558 | None -> raise (Impossible 13)
560 let (e,safes',n',nn',x',context') =
561 get_new_safes context p c rl' safes n nn x
564 check_is_really_smaller_arg context' n' nn' kl x' safes' e
565 ) (List.combine pl cl) true
566 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
567 let (isinductive,paramsno,cl) =
568 match CicEnvironment.get_obj uri with
569 C.InductiveDefinition (tl,_,paramsno) ->
570 let (_,isinductive,_,cl) = List.nth tl i in
571 let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in
575 (id, snd (split_prods tys paramsno ty), r)) cl
577 (isinductive,paramsno,cl')
579 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
581 if not isinductive then
584 i && check_is_really_smaller_arg context n nn kl x safes p)
587 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
588 (*CSC: sugli argomenti di una applicazione *)
590 (fun (p,(_,c,rl)) i ->
594 let (_,rl'') = split rl' paramsno in
596 | None -> raise (Impossible 14)
598 let (e, safes',n',nn',x',context') =
599 get_new_safes context p c rl' safes n nn x
602 check_is_really_smaller_arg context' n' nn' kl x' safes' e
603 ) (List.combine pl cl) true
607 i && check_is_really_smaller_arg context n nn kl x safes p
611 let len = List.length fl in
612 let n_plus_len = n + len
613 and nn_plus_len = nn + len
614 and x_plus_len = x + len
615 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
616 and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl
617 and safes' = List.map (fun x -> x + len) safes in
619 (fun (_,_,ty,bo) i ->
621 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
625 let len = List.length fl in
626 let n_plus_len = n + len
627 and nn_plus_len = nn + len
628 and x_plus_len = x + len
629 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
630 and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl
631 and safes' = List.map (fun x -> x + len) safes in
635 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
639 and guarded_by_destructors context n nn kl x safes =
640 let module C = Cic in
641 let module U = UriManager in
643 C.Rel m when m > n && m <= nn -> false
645 (match List.nth context (n-1) with
647 | C.Def bo -> guarded_by_destructors context n nn kl x safes bo
654 guarded_by_destructors context n nn kl x safes te &&
655 guarded_by_destructors context n nn kl x safes ty
656 | C.Prod (_,so,ta) ->
657 guarded_by_destructors context n nn kl x safes so &&
658 guarded_by_destructors ((C.Decl so)::context) (n+1) (nn+1) kl (x+1)
659 (List.map (fun x -> x + 1) safes) ta
660 | C.Lambda (_,so,ta) ->
661 guarded_by_destructors context n nn kl x safes so &&
662 guarded_by_destructors ((C.Decl so)::context) (n+1) (nn+1) kl (x+1)
663 (List.map (fun x -> x + 1) safes) ta
664 | C.LetIn (_,so,ta) ->
665 guarded_by_destructors context n nn kl x safes so &&
666 guarded_by_destructors ((C.Def so)::context) (n+1) (nn+1) kl (x+1)
667 (List.map (fun x -> x + 1) safes) ta
668 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
669 let k = List.nth kl (m - n - 1) in
670 if not (List.length tl > k) then false
674 i && guarded_by_destructors context n nn kl x safes param
676 check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
679 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
684 | C.MutConstruct _ -> true
685 | C.MutCase (uri,_,i,outtype,term,pl) ->
687 C.Rel m when List.mem m safes || m = x ->
688 let (isinductive,paramsno,cl) =
689 match CicEnvironment.get_obj uri with
690 C.InductiveDefinition (tl,_,paramsno) ->
691 let (_,isinductive,_,cl) = List.nth tl i in
692 let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in
696 (id, snd (split_prods tys paramsno ty), r)) cl
698 (isinductive,paramsno,cl')
700 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
702 if not isinductive then
703 guarded_by_destructors context n nn kl x safes outtype &&
704 guarded_by_destructors context n nn kl x safes term &&
705 (*CSC: manca ??? il controllo sul tipo di term? *)
708 i && guarded_by_destructors context n nn kl x safes p)
711 guarded_by_destructors context n nn kl x safes outtype &&
712 (*CSC: manca ??? il controllo sul tipo di term? *)
714 (fun (p,(_,c,rl)) i ->
718 let (_,rl'') = split rl' paramsno in
720 | None -> raise (Impossible 15)
722 let (e,safes',n',nn',x',context') =
723 get_new_safes context p c rl' safes n nn x
726 guarded_by_destructors context' n' nn' kl x' safes' e
727 ) (List.combine pl cl) true
728 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
729 let (isinductive,paramsno,cl) =
730 match CicEnvironment.get_obj uri with
731 C.InductiveDefinition (tl,_,paramsno) ->
732 let (_,isinductive,_,cl) = List.nth tl i in
733 let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in
737 (id, snd (split_prods tys paramsno ty), r)) cl
739 (isinductive,paramsno,cl')
741 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
743 if not isinductive then
744 guarded_by_destructors context n nn kl x safes outtype &&
745 guarded_by_destructors context n nn kl x safes term &&
746 (*CSC: manca ??? il controllo sul tipo di term? *)
749 i && guarded_by_destructors context n nn kl x safes p)
752 guarded_by_destructors context n nn kl x safes outtype &&
753 (*CSC: manca ??? il controllo sul tipo di term? *)
756 i && guarded_by_destructors context n nn kl x safes t)
759 (fun (p,(_,c,rl)) i ->
763 let (_,rl'') = split rl' paramsno in
765 | None -> raise (Impossible 16)
767 let (e, safes',n',nn',x',context') =
768 get_new_safes context p c rl' safes n nn x
771 guarded_by_destructors context' n' nn' kl x' safes' e
772 ) (List.combine pl cl) true
774 guarded_by_destructors context n nn kl x safes outtype &&
775 guarded_by_destructors context n nn kl x safes term &&
776 (*CSC: manca ??? il controllo sul tipo di term? *)
778 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
782 let len = List.length fl in
783 let n_plus_len = n + len
784 and nn_plus_len = nn + len
785 and x_plus_len = x + len
786 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
787 and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl
788 and safes' = List.map (fun x -> x + len) safes in
790 (fun (_,_,ty,bo) i ->
791 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
792 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
796 let len = List.length fl in
797 let n_plus_len = n + len
798 and nn_plus_len = nn + len
799 and x_plus_len = x + len
800 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
801 and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl
802 and safes' = List.map (fun x -> x + len) safes in
806 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
807 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
811 (* the boolean h means already protected *)
812 (* args is the list of arguments the type of the constructor that may be *)
813 (* found in head position must be applied to. *)
814 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
815 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
816 let module C = Cic in
817 (*CSC: There is a lot of code replication between the cases X and *)
818 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
819 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
820 match CicReduction.whd context te with
821 C.Rel m when m > n && m <= nn -> h
830 raise (Impossible 17) (* the term has just been type-checked *)
831 | C.Lambda (_,so,de) ->
832 does_not_occur context n nn so &&
833 guarded_by_constructors ((C.Decl so)::context) (n + 1) (nn + 1) h de args
835 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
837 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
838 | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) ->
840 match CicEnvironment.get_cooked_obj uri cookingsno with
841 C.InductiveDefinition (itl,_,_) ->
842 let (_,_,_,cl) = List.nth itl i in
843 let (_,cons,_) = List.nth cl (j - 1) in cons
845 raise (WrongUriToMutualInductiveDefinitions
846 (UriManager.string_of_uri uri))
848 let rec analyse_branch context ty te =
849 match CicReduction.whd context ty with
850 C.Meta _ -> raise (Impossible 34)
854 does_not_occur context n nn te
856 | C.Cast _ -> raise (Impossible 24) (* due to type-checking *)
857 | C.Prod (_,so,de) ->
858 analyse_branch ((C.Decl so)::context) de te
860 | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *)
861 | C.Appl ((C.MutInd (uri,_,_))::tl) as ty
862 when uri == coInductiveTypeURI ->
863 guarded_by_constructors context n nn true te [] coInductiveTypeURI
864 | C.Appl ((C.MutInd (uri,_,_))::tl) as ty ->
865 guarded_by_constructors context n nn true te tl coInductiveTypeURI
867 does_not_occur context n nn te
869 | C.Abst _ -> raise (Impossible 26)
870 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
871 guarded_by_constructors context n nn true te [] coInductiveTypeURI
873 does_not_occur context n nn te
874 | C.MutConstruct _ -> raise (Impossible 27)
875 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
876 (*CSC: in head position. *)
879 | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *)
881 let rec analyse_instantiated_type context ty l =
882 match CicReduction.whd context ty with
888 | C.Cast _ -> raise (Impossible 29) (* due to type-checking *)
889 | C.Prod (_,so,de) ->
894 analyse_branch context so he &&
895 analyse_instantiated_type ((C.Decl so)::context) de tl
898 | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *)
901 (fun i x -> i && does_not_occur context n nn x) true l
903 | C.Abst _ -> raise (Impossible 31)
906 (fun i x -> i && does_not_occur context n nn x) true l
907 | C.MutConstruct _ -> raise (Impossible 32)
908 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
909 (*CSC: in head position. *)
912 | C.CoFix _ -> raise (Impossible 33) (* due to type-checking *)
914 let rec instantiate_type args consty =
918 let consty' = CicReduction.whd context consty in
924 let instantiated_de = CicSubstitution.subst he de in
925 (*CSC: siamo sicuri che non sia troppo forte? *)
926 does_not_occur context n nn tlhe &
927 instantiate_type tl instantiated_de tltl
929 (*CSC:We do not consider backbones with a MutCase, a *)
930 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
931 raise (Impossible 23)
933 | [] -> analyse_instantiated_type context consty' l
934 (* These are all the other cases *)
936 instantiate_type args consty tl
937 | C.Appl ((C.CoFix (_,fl))::tl) ->
938 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
939 let len = List.length fl in
940 let n_plus_len = n + len
941 and nn_plus_len = nn + len
942 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
943 and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl in
946 i && does_not_occur context n nn ty &&
947 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
948 args coInductiveTypeURI
950 | C.Appl ((C.MutCase (_,_,_,out,te,pl))::tl) ->
951 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
952 does_not_occur context n nn out &&
953 does_not_occur context n nn te &&
957 guarded_by_constructors context n nn h x args coInductiveTypeURI
960 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
963 | C.MutInd _ -> assert false
964 | C.MutConstruct _ -> true
965 | C.MutCase (_,_,_,out,te,pl) ->
966 does_not_occur context n nn out &&
967 does_not_occur context n nn te &&
971 guarded_by_constructors context n nn h x args coInductiveTypeURI
974 let len = List.length fl in
975 let n_plus_len = n + len
976 and nn_plus_len = nn + len
977 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
978 and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl in
980 (fun (_,_,ty,bo) i ->
981 i && does_not_occur context n nn ty &&
982 does_not_occur (tys@context) n_plus_len nn_plus_len bo
985 let len = List.length fl in
986 let n_plus_len = n + len
987 and nn_plus_len = nn + len
988 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
989 and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl in
992 i && does_not_occur context n nn ty &&
993 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
994 args coInductiveTypeURI
997 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
998 let module C = Cic in
999 let module U = UriManager in
1000 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1001 (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1002 when CicReduction.are_convertible context so1 so2 ->
1003 check_allowed_sort_elimination context uri i need_dummy
1004 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1005 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1006 | (C.Sort C.Prop, C.Sort C.Set) when need_dummy ->
1007 (match CicEnvironment.get_obj uri with
1008 C.InductiveDefinition (itl,_,_) ->
1009 let (_,_,_,cl) = List.nth itl i in
1010 (* is a singleton definition? *)
1013 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1015 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1016 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1017 | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
1018 (match CicEnvironment.get_obj uri with
1019 C.InductiveDefinition (itl,_,paramsno) ->
1020 let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in
1021 let (_,_,_,cl) = List.nth itl i in
1023 (fun (_,x,_) i -> i && is_small tys paramsno x) cl true
1025 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1027 | (C.Sort C.Type, C.Sort _) when need_dummy -> true
1028 | (C.Sort C.Prop, C.Prod (_,so,ta)) when not need_dummy ->
1029 let res = CicReduction.are_convertible context so ind
1032 (match CicReduction.whd ((C.Decl so)::context) ta with
1033 C.Sort C.Prop -> true
1035 (match CicEnvironment.get_obj uri with
1036 C.InductiveDefinition (itl,_,_) ->
1037 let (_,_,_,cl) = List.nth itl i in
1038 (* is a singleton definition? *)
1041 raise (WrongUriToMutualInductiveDefinitions
1042 (U.string_of_uri uri))
1046 | (C.Sort C.Set, C.Prod (_,so,ta)) when not need_dummy ->
1047 let res = CicReduction.are_convertible context so ind
1050 (match CicReduction.whd ((C.Decl so)::context) ta with
1052 | C.Sort C.Set -> true
1054 (match CicEnvironment.get_obj uri with
1055 C.InductiveDefinition (itl,_,paramsno) ->
1056 let (_,_,_,cl) = List.nth itl i in
1057 let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in
1059 (fun (_,x,_) i -> i && is_small tys paramsno x) cl true
1061 raise (WrongUriToMutualInductiveDefinitions
1062 (U.string_of_uri uri))
1064 | _ -> raise (Impossible 19)
1066 | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
1067 CicReduction.are_convertible context so ind
1070 and type_of_branch context argsno need_dummy outtype term constype =
1071 let module C = Cic in
1072 let module R = CicReduction in
1073 match R.whd context constype with
1078 C.Appl [outtype ; term]
1079 | C.Appl (C.MutInd (_,_,_)::tl) ->
1080 let (_,arguments) = split tl argsno
1082 if need_dummy && arguments = [] then
1085 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1086 | C.Prod (name,so,de) ->
1087 C.Prod (C.Anonimous,so,type_of_branch ((C.Decl so)::context) argsno
1088 need_dummy (CicSubstitution.lift 1 outtype)
1089 (C.Appl [CicSubstitution.lift 1 term ; C.Rel 1]) de)
1090 | _ -> raise (Impossible 20)
1093 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1094 and type_of_aux' metasenv context t =
1095 let rec type_of_aux context =
1096 let module C = Cic in
1097 let module R = CicReduction in
1098 let module S = CicSubstitution in
1099 let module U = UriManager in
1103 match List.nth context (n - 1) with
1104 C.Decl t -> S.lift n t
1105 | C.Def bo -> type_of_aux context (S.lift n bo)
1107 _ -> raise (NotWellTyped "Not a close term")
1111 let ty = type_of_variable uri in
1114 | C.Meta n -> List.assoc n metasenv
1115 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1116 | C.Implicit -> raise (Impossible 21)
1118 let _ = type_of_aux context ty in
1119 if R.are_convertible context (type_of_aux context te) ty then ty
1120 else raise (NotWellTyped "Cast")
1122 let sort1 = type_of_aux context s
1123 and sort2 = type_of_aux ((C.Decl s)::context) t in
1124 sort_of_prod (sort1,sort2)
1125 | C.Lambda (n,s,t) ->
1126 let sort1 = type_of_aux context s
1127 and type2 = type_of_aux ((C.Decl s)::context) t in
1128 let sort2 = type_of_aux ((C.Decl s)::context) type2 in
1129 (* only to check if the product is well-typed *)
1130 let _ = sort_of_prod (sort1,sort2) in
1132 | C.LetIn (n,s,t) ->
1133 let t' = CicSubstitution.subst s t in
1134 type_of_aux context t'
1135 | C.Appl (he::tl) when List.length tl > 0 ->
1136 let hetype = type_of_aux context he
1137 and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1138 eat_prods context hetype tlbody_and_type
1139 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
1140 | C.Const (uri,cookingsno) ->
1142 let cty = cooked_type_of_constant uri cookingsno in
1145 | C.Abst _ -> raise (Impossible 22)
1146 | C.MutInd (uri,cookingsno,i) ->
1148 let cty = cooked_type_of_mutual_inductive_defs uri cookingsno i in
1151 | C.MutConstruct (uri,cookingsno,i,j) ->
1152 let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j
1155 | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
1156 let outsort = type_of_aux context outtype in
1157 let (need_dummy, k) =
1158 let rec guess_args context t =
1159 match CicReduction.whd context t with
1160 C.Sort _ -> (true, 0)
1161 | C.Prod (_, s, t) ->
1162 let (b, n) = guess_args ((C.Decl s)::context) t in
1164 (* last prod before sort *)
1165 match CicReduction.whd context s with
1166 (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
1167 C.MutInd (uri',_,i') when U.eq uri' uri && i' = i -> (false, 1)
1168 | C.Appl ((C.MutInd (uri',_,i')) :: _)
1169 when U.eq uri' uri && i' = i -> (false, 1)
1173 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
1175 (*CSC whd non serve dopo type_of_aux ? *)
1176 let (b, k) = guess_args context outsort in
1177 if not b then (b, k - 1) else (b, k)
1179 let (parameters, arguments) =
1180 match R.whd context (type_of_aux context term) with
1181 (*CSC manca il caso dei CAST *)
1182 C.MutInd (uri',_,i') ->
1183 (*CSC vedi nota delirante sui cookingsno in cicReduction.ml*)
1184 if U.eq uri uri' && i = i' then ([],[])
1185 else raise (NotWellTyped ("MutCase: the term is of type " ^
1186 (U.string_of_uri uri') ^ "," ^ string_of_int i' ^
1187 " instead of type " ^ (U.string_of_uri uri') ^ "," ^
1189 | C.Appl (C.MutInd (uri',_,i') :: tl) ->
1190 if U.eq uri uri' && i = i' then split tl (List.length tl - k)
1191 else raise (NotWellTyped ("MutCase: the term is of type " ^
1192 (U.string_of_uri uri') ^ "," ^ string_of_int i' ^
1193 " instead of type " ^ (U.string_of_uri uri) ^ "," ^
1195 | _ -> raise (NotWellTyped "MutCase: the term is not an inductive one")
1197 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1198 let sort_of_ind_type =
1199 if parameters = [] then
1200 C.MutInd (uri,cookingsno,i)
1202 C.Appl ((C.MutInd (uri,cookingsno,i))::parameters)
1204 if not (check_allowed_sort_elimination context uri i need_dummy
1205 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1207 raise (NotWellTyped "MutCase: not allowed sort elimination") ;
1209 (* let's check if the type of branches are right *)
1211 match CicEnvironment.get_cooked_obj uri cookingsno with
1212 C.InductiveDefinition (tl,_,parsno) ->
1213 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
1215 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1217 let (_,branches_ok) =
1219 (fun (j,b) (p,(_,c,_)) ->
1221 if parameters = [] then
1222 (C.MutConstruct (uri,cookingsno,i,j))
1224 (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
1227 R.are_convertible context (type_of_aux context p)
1228 (type_of_branch context parsno need_dummy outtype cons
1229 (type_of_aux context cons))
1231 ) (1,true) (List.combine pl cl)
1233 if not branches_ok then
1234 raise (NotWellTyped "MutCase: wrong type of a branch") ;
1236 if not need_dummy then
1237 C.Appl ((outtype::arguments)@[term])
1238 else if arguments = [] then
1241 C.Appl (outtype::arguments)
1243 let types_times_kl =
1247 let _ = type_of_aux context ty in (C.Decl ty,k)) fl)
1249 let (types,kl) = List.split types_times_kl in
1250 let len = List.length types in
1252 (fun (name,x,ty,bo) ->
1254 (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1255 (CicSubstitution.lift len ty))
1258 let (m, eaten, context') =
1259 eat_lambdas (types @ context) (x + 1) bo
1261 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1264 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1266 raise (NotWellTyped "Fix: not guarded by destructors")
1269 raise (NotWellTyped "Fix: ill-typed bodies")
1272 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1273 let (_,_,ty,_) = List.nth fl i in
1279 (fun (_,ty,_) -> let _ = type_of_aux context ty in C.Decl ty) fl)
1281 let len = List.length types in
1285 (R.are_convertible (types @ context)
1286 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1289 (* let's control that the returned type is coinductive *)
1290 match returns_a_coinductive ty with
1292 raise(NotWellTyped "CoFix: does not return a coinductive type")
1294 (*let's control the guarded by constructors conditions C{f,M}*)
1297 (guarded_by_constructors (types @ context) 0 len false bo
1300 raise (NotWellTyped "CoFix: not guarded by constructors")
1303 raise (NotWellTyped "CoFix: ill-typed bodies")
1306 let (_,ty,_) = List.nth fl i in
1309 and sort_of_prod (t1, t2) =
1310 let module C = Cic in
1311 let t1' = CicReduction.whd context t1 in
1312 let t2' = CicReduction.whd context t2 in
1313 match (t1', t2') with
1314 (C.Sort s1, C.Sort s2)
1315 when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
1317 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1321 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
1323 and eat_prods context hetype =
1324 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1328 | (hete, hety)::tl ->
1329 (match (CicReduction.whd context hetype) with
1331 if CicReduction.are_convertible context s hety then
1332 (CicReduction.fdebug := -1 ;
1333 eat_prods context (CicSubstitution.subst hete t) tl
1337 CicReduction.fdebug := 0 ;
1338 ignore (CicReduction.are_convertible context s hety) ;
1341 raise (NotWellTyped "Appl: wrong parameter-type")
1343 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
1346 and returns_a_coinductive ty =
1347 let module C = Cic in
1348 match CicReduction.whd context ty with
1349 C.MutInd (uri,cookingsno,i) ->
1350 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1351 (match CicEnvironment.get_cooked_obj uri cookingsno with
1352 C.InductiveDefinition (itl,_,_) ->
1353 let (_,is_inductive,_,cl) = List.nth itl i in
1354 if is_inductive then None else (Some uri)
1356 raise (WrongUriToMutualInductiveDefinitions
1357 (UriManager.string_of_uri uri))
1359 | C.Appl ((C.MutInd (uri,_,i))::_) ->
1360 (match CicEnvironment.get_obj uri with
1361 C.InductiveDefinition (itl,_,_) ->
1362 let (_,is_inductive,_,_) = List.nth itl i in
1363 if is_inductive then None else (Some uri)
1365 raise (WrongUriToMutualInductiveDefinitions
1366 (UriManager.string_of_uri uri))
1368 | C.Prod (_,_,de) -> returns_a_coinductive de
1373 prerr_endline ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1376 type_of_aux context t
1378 in prerr_endline "FINE TYPE_OF_AUX" ; flush stderr ; res
1381 (* is a small constructor? *)
1382 (*CSC: ottimizzare calcolando staticamente *)
1383 and is_small context paramsno c =
1384 let rec is_small_aux context c =
1385 let module C = Cic in
1386 match CicReduction.whd context c with
1388 (*CSC: [] is an empty metasenv. Is it correct? *)
1389 let s = type_of_aux' [] context so in
1390 (s = C.Sort C.Prop || s = C.Sort C.Set) &&
1391 is_small_aux ((C.Decl so)::context) de
1392 | _ -> true (*CSC: we trust the type-checker *)
1394 let (context',dx) = split_prods context paramsno c in
1395 is_small_aux context' dx
1399 prerr_endline ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1402 type_of_aux' [] [] t
1404 in prerr_endline "FINE TYPE_OF_AUX'" ; flush stderr ; res
1409 let module C = Cic in
1410 let module R = CicReduction in
1411 let module U = UriManager in
1412 match CicEnvironment.is_type_checked uri 0 with
1413 CicEnvironment.CheckedObj _ -> ()
1414 | CicEnvironment.UncheckedObj uobj ->
1415 (* let's typecheck the uncooked object *)
1416 Logger.log (`Start_type_checking uri) ;
1418 C.Definition (_,te,ty,_) ->
1419 let _ = type_of ty in
1420 if not (R.are_convertible [] (type_of te ) ty) then
1421 raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
1422 | C.Axiom (_,ty,_) ->
1423 (* only to check that ty is well-typed *)
1424 let _ = type_of ty in ()
1425 | C.CurrentProof (_,conjs,te,ty) ->
1427 let _ = type_of_aux' conjs [] ty in
1428 debug (type_of_aux' conjs [] te) [] ;
1429 if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then
1430 raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
1431 | C.Variable (_,bo,ty) ->
1432 (* only to check that ty is well-typed *)
1433 let _ = type_of ty in
1437 if not (R.are_convertible [] (type_of bo) ty) then
1438 raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri)))
1440 | C.InductiveDefinition _ ->
1441 cooked_mutual_inductive_defs uri uobj
1443 CicEnvironment.set_type_checking_info uri ;
1444 Logger.log (`Type_checking_completed uri)