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;;
35 exception RelToHiddenHypothesis;;
36 exception MetasenvInconsistency;;
40 let rec debug_aux t i =
42 let module U = UriManager in
43 CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i
46 raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::context) ""))
47 (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
53 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
54 | (_,_) -> raise ListTooShort
57 exception CicEnvironmentError;;
59 let rec cooked_type_of_constant uri cookingsno =
61 let module R = CicReduction in
62 let module U = UriManager in
64 match CicEnvironment.is_type_checked uri cookingsno with
65 CicEnvironment.CheckedObj cobj -> cobj
66 | CicEnvironment.UncheckedObj uobj ->
67 Logger.log (`Start_type_checking uri) ;
68 (* let's typecheck the uncooked obj *)
70 C.Definition (_,te,ty,_) ->
72 if not (R.are_convertible [] (type_of te) ty) then
73 raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
75 (* only to check that ty is well-typed *)
76 let _ = type_of ty in ()
77 | C.CurrentProof (_,conjs,te,ty) ->
78 let _ = type_of_aux' conjs [] ty in
79 if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
81 raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
82 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
84 CicEnvironment.set_type_checking_info uri ;
85 Logger.log (`Type_checking_completed uri) ;
86 match CicEnvironment.is_type_checked uri cookingsno with
87 CicEnvironment.CheckedObj cobj -> cobj
88 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
91 C.Definition (_,_,ty,_) -> ty
92 | C.Axiom (_,ty,_) -> ty
93 | C.CurrentProof (_,_,_,ty) -> ty
94 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
96 and type_of_variable uri =
98 let module R = CicReduction in
99 let module U = UriManager in
100 (* 0 because a variable is never cooked => no partial cooking at one level *)
101 match CicEnvironment.is_type_checked uri 0 with
102 CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
103 | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty)) ->
104 Logger.log (`Start_type_checking uri) ;
105 (* only to check that ty is well-typed *)
106 let _ = type_of ty in
110 if not (R.are_convertible [] (type_of bo) ty) then
111 raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
113 CicEnvironment.set_type_checking_info uri ;
114 Logger.log (`Type_checking_completed uri) ;
116 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
118 and does_not_occur context n nn te =
119 let module C = Cic in
120 (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
121 (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
123 match CicReduction.whd context te with
124 C.Rel m when m > n && m <= nn -> false
131 does_not_occur context n nn te && does_not_occur context n nn ty
132 | C.Prod (name,so,dest) ->
133 does_not_occur context n nn so &&
134 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
135 | C.Lambda (name,so,dest) ->
136 does_not_occur context n nn so &&
137 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
138 | C.LetIn (name,so,dest) ->
139 does_not_occur context n nn so &&
140 does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest
142 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
146 | C.MutConstruct _ -> true
147 | C.MutCase (_,_,_,out,te,pl) ->
148 does_not_occur context n nn out && does_not_occur context n nn te &&
149 List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
151 let len = List.length fl in
152 let n_plus_len = n + len in
153 let nn_plus_len = nn + len in
155 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
158 (fun (_,_,ty,bo) i ->
159 i && does_not_occur context n nn ty &&
160 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
163 let len = List.length fl in
164 let n_plus_len = n + len in
165 let nn_plus_len = nn + len in
167 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
171 i && does_not_occur context n nn ty &&
172 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
175 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
176 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
177 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
178 (*CSC strictly_positive *)
179 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
180 and weakly_positive context n nn uri te =
181 let module C = Cic in
182 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
184 C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,0)
186 (*CSC mettere in cicSubstitution *)
187 let rec subst_inductive_type_with_dummy_mutind =
189 C.MutInd (uri',_,0) when UriManager.eq uri' uri ->
191 | C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri ->
193 | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
194 | C.Prod (name,so,ta) ->
195 C.Prod (name, subst_inductive_type_with_dummy_mutind so,
196 subst_inductive_type_with_dummy_mutind ta)
197 | C.Lambda (name,so,ta) ->
198 C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
199 subst_inductive_type_with_dummy_mutind ta)
201 C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
202 | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
203 C.MutCase (uri,cookingsno,i,
204 subst_inductive_type_with_dummy_mutind outtype,
205 subst_inductive_type_with_dummy_mutind term,
206 List.map subst_inductive_type_with_dummy_mutind pl)
208 C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
209 subst_inductive_type_with_dummy_mutind ty,
210 subst_inductive_type_with_dummy_mutind bo)) fl)
212 C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
213 subst_inductive_type_with_dummy_mutind ty,
214 subst_inductive_type_with_dummy_mutind bo)) fl)
217 match CicReduction.whd context te with
218 C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri -> true
219 | C.MutInd (uri',_,0) when UriManager.eq uri' uri -> true
220 | C.Prod (C.Anonimous,source,dest) ->
221 strictly_positive context n nn
222 (subst_inductive_type_with_dummy_mutind source) &&
223 weakly_positive ((Some (C.Anonimous,(C.Decl source)))::context)
224 (n + 1) (nn + 1) uri dest
225 | C.Prod (name,source,dest) when
226 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
227 (* dummy abstraction, so we behave as in the anonimous case *)
228 strictly_positive context n nn
229 (subst_inductive_type_with_dummy_mutind source) &&
230 weakly_positive ((Some (name,(C.Decl source)))::context)
231 (n + 1) (nn + 1) uri dest
232 | C.Prod (name,source,dest) ->
233 does_not_occur context n nn
234 (subst_inductive_type_with_dummy_mutind source)&&
235 weakly_positive ((Some (name,(C.Decl source)))::context)
236 (n + 1) (nn + 1) uri dest
237 | _ -> raise (NotWellFormedTypeOfInductiveConstructor ("Guess where the error is ;-)"))
239 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
240 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
241 and instantiate_parameters params c =
242 let module C = Cic in
243 match (c,params) with
245 | (C.Prod (_,_,ta), he::tl) ->
246 instantiate_parameters tl
247 (CicSubstitution.subst he ta)
248 | (C.Cast (te,_), _) -> instantiate_parameters params te
249 | (t,l) -> raise (Impossible 1)
251 and strictly_positive context n nn te =
252 let module C = Cic in
253 let module U = UriManager in
254 match CicReduction.whd context te with
257 (*CSC: bisogna controllare ty????*)
258 strictly_positive context n nn te
259 | C.Prod (name,so,ta) ->
260 does_not_occur context n nn so &&
261 strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
262 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
263 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
264 | C.Appl ((C.MutInd (uri,_,i))::tl) ->
265 let (ok,paramsno,ity,cl,name) =
266 match CicEnvironment.get_obj uri with
267 C.InductiveDefinition (tl,_,paramsno) ->
268 let (name,_,ity,cl) = List.nth tl i in
269 (List.length tl = 1, paramsno, ity, cl, name)
270 | _ -> raise(WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
272 let (params,arguments) = split tl paramsno in
273 let lifted_params = List.map (CicSubstitution.lift 1) params in
275 List.map (fun (_,te,_) -> instantiate_parameters lifted_params te) cl
279 (fun x i -> i && does_not_occur context n nn x)
281 (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
286 ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri x
288 | t -> does_not_occur context n nn t
290 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
291 and are_all_occurrences_positive context uri indparamsno i n nn te =
292 let module C = Cic in
293 match CicReduction.whd context te with
294 C.Appl ((C.Rel m)::tl) when m = i ->
295 (*CSC: riscrivere fermandosi a 0 *)
296 (* let's check if the inductive type is applied at least to *)
297 (* indparamsno parameters *)
303 match CicReduction.whd context x with
304 C.Rel m when m = n - (indparamsno - k) -> k - 1
305 | _ -> raise (WrongRequiredArgument (UriManager.string_of_uri uri))
309 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
311 raise (WrongRequiredArgument (UriManager.string_of_uri uri))
312 | C.Rel m when m = i ->
313 if indparamsno = 0 then
316 raise (WrongRequiredArgument (UriManager.string_of_uri uri))
317 | C.Prod (C.Anonimous,source,dest) ->
318 strictly_positive context n nn source &&
319 are_all_occurrences_positive
320 ((Some (C.Anonimous,(C.Decl source)))::context) uri indparamsno
321 (i+1) (n + 1) (nn + 1) dest
322 | C.Prod (name,source,dest) when
323 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
324 (* dummy abstraction, so we behave as in the anonimous case *)
325 strictly_positive context n nn source &&
326 are_all_occurrences_positive
327 ((Some (name,(C.Decl source)))::context) uri indparamsno
328 (i+1) (n + 1) (nn + 1) dest
329 | C.Prod (name,source,dest) ->
330 does_not_occur context n nn source &&
331 are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
332 uri indparamsno (i+1) (n + 1) (nn + 1) dest
333 | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri))
335 (*CSC: cambiare il nome, torna unit! *)
336 and cooked_mutual_inductive_defs uri =
337 let module U = UriManager in
339 Cic.InductiveDefinition (itl, _, indparamsno) ->
340 (* let's check if the arity of the inductive types are well *)
342 List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
344 (* let's check if the types of the inductive constructors *)
345 (* are well formed. *)
346 (* In order not to use type_of_aux we put the types of the *)
347 (* mutual inductive types at the head of the types of the *)
348 (* constructors using Prods *)
349 (*CSC: piccola??? inefficienza *)
350 let len = List.length itl in
351 (*CSC: siamo sicuri che non debba fare anche un List.rev? Il bug *)
352 (*CSC: si manifesterebbe solamene con tipi veramente mutualmente *)
353 (*CSC: induttivi... *)
355 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
363 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
366 let _ = type_of augmented_term in
367 (* let's check also the positivity conditions *)
370 (are_all_occurrences_positive tys uri indparamsno i 0 len te)
372 raise (NotPositiveOccurrences (U.string_of_uri uri))
375 Some _ -> raise (Impossible 2)
376 | None -> r := Some (recursive_args tys 0 len te)
383 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
385 and cooked_type_of_mutual_inductive_defs uri cookingsno i =
386 let module C = Cic in
387 let module R = CicReduction in
388 let module U = UriManager in
390 match CicEnvironment.is_type_checked uri cookingsno with
391 CicEnvironment.CheckedObj cobj -> cobj
392 | CicEnvironment.UncheckedObj uobj ->
393 Logger.log (`Start_type_checking uri) ;
394 cooked_mutual_inductive_defs uri uobj ;
395 CicEnvironment.set_type_checking_info uri ;
396 Logger.log (`Type_checking_completed uri) ;
397 (match CicEnvironment.is_type_checked uri cookingsno with
398 CicEnvironment.CheckedObj cobj -> cobj
399 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
403 C.InductiveDefinition (dl,_,_) ->
404 let (_,_,arity,_) = List.nth dl i in
406 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
408 and cooked_type_of_mutual_inductive_constr uri cookingsno i j =
409 let module C = Cic in
410 let module R = CicReduction in
411 let module U = UriManager in
413 match CicEnvironment.is_type_checked uri cookingsno with
414 CicEnvironment.CheckedObj cobj -> cobj
415 | CicEnvironment.UncheckedObj uobj ->
416 Logger.log (`Start_type_checking uri) ;
417 cooked_mutual_inductive_defs uri uobj ;
418 CicEnvironment.set_type_checking_info uri ;
419 Logger.log (`Type_checking_completed uri) ;
420 (match CicEnvironment.is_type_checked uri cookingsno with
421 CicEnvironment.CheckedObj cobj -> cobj
422 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
426 C.InductiveDefinition (dl,_,_) ->
427 let (_,_,_,cl) = List.nth dl i in
428 let (_,ty,_) = List.nth cl (j-1) in
430 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
432 and recursive_args context n nn te =
433 let module C = Cic in
434 match CicReduction.whd context te with
440 | C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *)
441 | C.Prod (name,so,de) ->
442 (not (does_not_occur context n nn so)) ::
443 (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
445 | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *)
448 | C.Abst _ -> raise (Impossible 5)
453 | C.CoFix _ -> raise (Impossible 6) (* due to type-checking *)
455 and get_new_safes context p c rl safes n nn x =
456 let module C = Cic in
457 let module U = UriManager in
458 let module R = CicReduction in
459 match (R.whd context c, R.whd context p, rl) with
460 (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
461 (* we are sure that the two sources are convertible because we *)
462 (* have just checked this. So let's go along ... *)
464 List.map (fun x -> x + 1) safes
467 if b then 1::safes' else safes'
469 get_new_safes ((Some (name,(C.Decl so)))::context)
470 ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
471 | (C.Prod _, (C.MutConstruct _ as e), _)
472 | (C.Prod _, (C.Rel _ as e), _)
473 | (C.MutInd _, e, [])
474 | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
476 (* CSC: If the next exception is raised, it just means that *)
477 (* CSC: the proof-assistant allows to use very strange things *)
478 (* CSC: as a branch of a case whose type is a Prod. In *)
479 (* CSC: particular, this means that a new (C.Prod, x,_) case *)
480 (* CSC: must be considered in this match. (e.g. x = MutCase) *)
483 and split_prods context n te =
484 let module C = Cic in
485 let module R = CicReduction in
486 match (n, R.whd context te) with
488 | (n, C.Prod (name,so,ta)) when n > 0 ->
489 split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta
490 | (_, _) -> raise (Impossible 8)
492 and eat_lambdas context n te =
493 let module C = Cic in
494 let module R = CicReduction in
495 match (n, R.whd context te) with
496 (0, _) -> (te, 0, context)
497 | (n, C.Lambda (name,so,ta)) when n > 0 ->
498 let (te, k, context') =
499 eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
501 (te, k + 1, context')
502 | (_, _) -> raise (Impossible 9)
504 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
505 and check_is_really_smaller_arg context n nn kl x safes te =
506 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
507 (*CSC: cfr guarded_by_destructors *)
508 let module C = Cic in
509 let module U = UriManager in
510 match CicReduction.whd context te with
511 C.Rel m when List.mem m safes -> true
518 (* | C.Cast (te,ty) ->
519 check_is_really_smaller_arg n nn kl x safes te &&
520 check_is_really_smaller_arg n nn kl x safes ty*)
521 (* | C.Prod (_,so,ta) ->
522 check_is_really_smaller_arg n nn kl x safes so &&
523 check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
524 (List.map (fun x -> x + 1) safes) ta*)
525 | C.Prod _ -> raise (Impossible 10)
526 | C.Lambda (name,so,ta) ->
527 check_is_really_smaller_arg context n nn kl x safes so &&
528 check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context)
529 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
530 | C.LetIn (name,so,ta) ->
531 check_is_really_smaller_arg context n nn kl x safes so &&
532 check_is_really_smaller_arg ((Some (name,(C.Def so)))::context)
533 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
535 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
536 (*CSC: solo perche' non abbiamo trovato controesempi *)
537 check_is_really_smaller_arg context n nn kl x safes he
538 | C.Appl [] -> raise (Impossible 11)
541 | C.MutInd _ -> raise (Impossible 12)
542 | C.MutConstruct _ -> false
543 | C.MutCase (uri,_,i,outtype,term,pl) ->
545 C.Rel m when List.mem m safes || m = x ->
546 let (isinductive,paramsno,cl) =
547 match CicEnvironment.get_obj uri with
548 C.InductiveDefinition (tl,_,paramsno) ->
550 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
552 let (_,isinductive,_,cl) = List.nth tl i in
556 (id, snd (split_prods tys paramsno ty), r)) cl
558 (isinductive,paramsno,cl')
560 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
562 if not isinductive then
565 i && check_is_really_smaller_arg context n nn kl x safes p)
569 (fun (p,(_,c,rl)) i ->
573 let (_,rl'') = split rl' paramsno in
575 | None -> raise (Impossible 13)
577 let (e,safes',n',nn',x',context') =
578 get_new_safes context p c rl' safes n nn x
581 check_is_really_smaller_arg context' n' nn' kl x' safes' e
582 ) (List.combine pl cl) true
583 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
584 let (isinductive,paramsno,cl) =
585 match CicEnvironment.get_obj uri with
586 C.InductiveDefinition (tl,_,paramsno) ->
587 let (_,isinductive,_,cl) = List.nth tl i in
589 List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
594 (id, snd (split_prods tys paramsno ty), r)) cl
596 (isinductive,paramsno,cl')
598 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
600 if not isinductive then
603 i && check_is_really_smaller_arg context n nn kl x safes p)
606 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
607 (*CSC: sugli argomenti di una applicazione *)
609 (fun (p,(_,c,rl)) i ->
613 let (_,rl'') = split rl' paramsno in
615 | None -> raise (Impossible 14)
617 let (e, safes',n',nn',x',context') =
618 get_new_safes context p c rl' safes n nn x
621 check_is_really_smaller_arg context' n' nn' kl x' safes' e
622 ) (List.combine pl cl) true
626 i && check_is_really_smaller_arg context n nn kl x safes p
630 let len = List.length fl in
631 let n_plus_len = n + len
632 and nn_plus_len = nn + len
633 and x_plus_len = x + len
634 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
635 and safes' = List.map (fun x -> x + len) safes in
637 (fun (_,_,ty,bo) i ->
639 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
643 let len = List.length fl in
644 let n_plus_len = n + len
645 and nn_plus_len = nn + len
646 and x_plus_len = x + len
647 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
648 and safes' = List.map (fun x -> x + len) safes in
652 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
656 and guarded_by_destructors context n nn kl x safes =
657 let module C = Cic in
658 let module U = UriManager in
660 C.Rel m when m > n && m <= nn -> false
662 (match List.nth context (n-1) with
663 Some (_,C.Decl _) -> true
664 | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo
665 | None -> raise RelToHiddenHypothesis
672 guarded_by_destructors context n nn kl x safes te &&
673 guarded_by_destructors context n nn kl x safes ty
674 | C.Prod (name,so,ta) ->
675 guarded_by_destructors context n nn kl x safes so &&
676 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
677 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
678 | C.Lambda (name,so,ta) ->
679 guarded_by_destructors context n nn kl x safes so &&
680 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
681 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
682 | C.LetIn (name,so,ta) ->
683 guarded_by_destructors context n nn kl x safes so &&
684 guarded_by_destructors ((Some (name,(C.Def so)))::context)
685 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
686 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
687 let k = List.nth kl (m - n - 1) in
688 if not (List.length tl > k) then false
692 i && guarded_by_destructors context n nn kl x safes param
694 check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
697 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
702 | C.MutConstruct _ -> true
703 | C.MutCase (uri,_,i,outtype,term,pl) ->
705 C.Rel m when List.mem m safes || m = x ->
706 let (isinductive,paramsno,cl) =
707 match CicEnvironment.get_obj uri with
708 C.InductiveDefinition (tl,_,paramsno) ->
709 let (_,isinductive,_,cl) = List.nth tl i in
711 List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
716 (id, snd (split_prods tys paramsno ty), r)) cl
718 (isinductive,paramsno,cl')
720 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
722 if not isinductive then
723 guarded_by_destructors context n nn kl x safes outtype &&
724 guarded_by_destructors context n nn kl x safes term &&
725 (*CSC: manca ??? il controllo sul tipo di term? *)
728 i && guarded_by_destructors context n nn kl x safes p)
731 guarded_by_destructors context n nn kl x safes outtype &&
732 (*CSC: manca ??? il controllo sul tipo di term? *)
734 (fun (p,(_,c,rl)) i ->
738 let (_,rl'') = split rl' paramsno in
740 | None -> raise (Impossible 15)
742 let (e,safes',n',nn',x',context') =
743 get_new_safes context p c rl' safes n nn x
746 guarded_by_destructors context' n' nn' kl x' safes' e
747 ) (List.combine pl cl) true
748 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
749 let (isinductive,paramsno,cl) =
750 match CicEnvironment.get_obj uri with
751 C.InductiveDefinition (tl,_,paramsno) ->
752 let (_,isinductive,_,cl) = List.nth tl i in
754 List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
759 (id, snd (split_prods tys paramsno ty), r)) cl
761 (isinductive,paramsno,cl')
763 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
765 if not isinductive then
766 guarded_by_destructors context n nn kl x safes outtype &&
767 guarded_by_destructors context n nn kl x safes term &&
768 (*CSC: manca ??? il controllo sul tipo di term? *)
771 i && guarded_by_destructors context n nn kl x safes p)
774 guarded_by_destructors context n nn kl x safes outtype &&
775 (*CSC: manca ??? il controllo sul tipo di term? *)
778 i && guarded_by_destructors context n nn kl x safes t)
781 (fun (p,(_,c,rl)) i ->
785 let (_,rl'') = split rl' paramsno in
787 | None -> raise (Impossible 16)
789 let (e, safes',n',nn',x',context') =
790 get_new_safes context p c rl' safes n nn x
793 guarded_by_destructors context' n' nn' kl x' safes' e
794 ) (List.combine pl cl) true
796 guarded_by_destructors context n nn kl x safes outtype &&
797 guarded_by_destructors context n nn kl x safes term &&
798 (*CSC: manca ??? il controllo sul tipo di term? *)
800 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
804 let len = List.length fl in
805 let n_plus_len = n + len
806 and nn_plus_len = nn + len
807 and x_plus_len = x + len
808 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
809 and safes' = List.map (fun x -> x + len) safes in
811 (fun (_,_,ty,bo) i ->
812 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
813 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
817 let len = List.length fl in
818 let n_plus_len = n + len
819 and nn_plus_len = nn + len
820 and x_plus_len = x + len
821 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
822 and safes' = List.map (fun x -> x + len) safes in
826 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
827 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
831 (* the boolean h means already protected *)
832 (* args is the list of arguments the type of the constructor that may be *)
833 (* found in head position must be applied to. *)
834 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
835 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
836 let module C = Cic in
837 (*CSC: There is a lot of code replication between the cases X and *)
838 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
839 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
840 match CicReduction.whd context te with
841 C.Rel m when m > n && m <= nn -> h
850 raise (Impossible 17) (* the term has just been type-checked *)
851 | C.Lambda (name,so,de) ->
852 does_not_occur context n nn so &&
853 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
854 (n + 1) (nn + 1) h de args coInductiveTypeURI
855 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
857 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
858 | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) ->
860 match CicEnvironment.get_cooked_obj uri cookingsno with
861 C.InductiveDefinition (itl,_,_) ->
862 let (_,_,_,cl) = List.nth itl i in
863 let (_,cons,_) = List.nth cl (j - 1) in cons
865 raise (WrongUriToMutualInductiveDefinitions
866 (UriManager.string_of_uri uri))
868 let rec analyse_branch context ty te =
869 match CicReduction.whd context ty with
870 C.Meta _ -> raise (Impossible 34)
874 does_not_occur context n nn te
876 | C.Cast _ -> raise (Impossible 24) (* due to type-checking *)
877 | C.Prod (name,so,de) ->
878 analyse_branch ((Some (name,(C.Decl so)))::context) de te
880 | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *)
881 | C.Appl ((C.MutInd (uri,_,_))::tl) as ty
882 when uri == coInductiveTypeURI ->
883 guarded_by_constructors context n nn true te [] coInductiveTypeURI
884 | C.Appl ((C.MutInd (uri,_,_))::tl) as ty ->
885 guarded_by_constructors context n nn true te tl coInductiveTypeURI
887 does_not_occur context n nn te
889 | C.Abst _ -> raise (Impossible 26)
890 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
891 guarded_by_constructors context n nn true te [] coInductiveTypeURI
893 does_not_occur context n nn te
894 | C.MutConstruct _ -> raise (Impossible 27)
895 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
896 (*CSC: in head position. *)
899 | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *)
901 let rec analyse_instantiated_type context ty l =
902 match CicReduction.whd context ty with
908 | C.Cast _ -> raise (Impossible 29) (* due to type-checking *)
909 | C.Prod (name,so,de) ->
914 analyse_branch context so he &&
915 analyse_instantiated_type ((Some (name,(C.Decl so)))::context)
919 | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *)
922 (fun i x -> i && does_not_occur context n nn x) true l
924 | C.Abst _ -> raise (Impossible 31)
927 (fun i x -> i && does_not_occur context n nn x) true l
928 | C.MutConstruct _ -> raise (Impossible 32)
929 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
930 (*CSC: in head position. *)
933 | C.CoFix _ -> raise (Impossible 33) (* due to type-checking *)
935 let rec instantiate_type args consty =
939 let consty' = CicReduction.whd context consty in
945 let instantiated_de = CicSubstitution.subst he de in
946 (*CSC: siamo sicuri che non sia troppo forte? *)
947 does_not_occur context n nn tlhe &
948 instantiate_type tl instantiated_de tltl
950 (*CSC:We do not consider backbones with a MutCase, a *)
951 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
952 raise (Impossible 23)
954 | [] -> analyse_instantiated_type context consty' l
955 (* These are all the other cases *)
957 instantiate_type args consty tl
958 | C.Appl ((C.CoFix (_,fl))::tl) ->
959 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
960 let len = List.length fl in
961 let n_plus_len = n + len
962 and nn_plus_len = nn + len
963 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
964 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
967 i && does_not_occur context n nn ty &&
968 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
969 args coInductiveTypeURI
971 | C.Appl ((C.MutCase (_,_,_,out,te,pl))::tl) ->
972 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
973 does_not_occur context n nn out &&
974 does_not_occur context n nn te &&
978 guarded_by_constructors context n nn h x args coInductiveTypeURI
981 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
984 | C.MutInd _ -> assert false
985 | C.MutConstruct _ -> true
986 | C.MutCase (_,_,_,out,te,pl) ->
987 does_not_occur context n nn out &&
988 does_not_occur context n nn te &&
992 guarded_by_constructors context n nn h x args coInductiveTypeURI
995 let len = List.length fl in
996 let n_plus_len = n + len
997 and nn_plus_len = nn + len
998 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
999 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1001 (fun (_,_,ty,bo) i ->
1002 i && does_not_occur context n nn ty &&
1003 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1006 let len = List.length fl in
1007 let n_plus_len = n + len
1008 and nn_plus_len = nn + len
1009 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1010 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1013 i && does_not_occur context n nn ty &&
1014 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1015 args coInductiveTypeURI
1018 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1019 let module C = Cic in
1020 let module U = UriManager in
1021 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1022 (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1023 when CicReduction.are_convertible context so1 so2 ->
1024 check_allowed_sort_elimination context uri i need_dummy
1025 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1026 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1027 | (C.Sort C.Prop, C.Sort C.Set) when need_dummy ->
1028 (match CicEnvironment.get_obj uri with
1029 C.InductiveDefinition (itl,_,_) ->
1030 let (_,_,_,cl) = List.nth itl i in
1031 (* is a singleton definition? *)
1034 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1036 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1037 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1038 | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
1039 (match CicEnvironment.get_obj uri with
1040 C.InductiveDefinition (itl,_,paramsno) ->
1042 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1044 let (_,_,_,cl) = List.nth itl i in
1046 (fun (_,x,_) i -> i && is_small tys paramsno x) cl true
1048 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1050 | (C.Sort C.Type, C.Sort _) when need_dummy -> true
1051 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1052 let res = CicReduction.are_convertible context so ind
1055 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1056 C.Sort C.Prop -> true
1058 (match CicEnvironment.get_obj uri with
1059 C.InductiveDefinition (itl,_,_) ->
1060 let (_,_,_,cl) = List.nth itl i in
1061 (* is a singleton definition? *)
1064 raise (WrongUriToMutualInductiveDefinitions
1065 (U.string_of_uri uri))
1069 | (C.Sort C.Set, C.Prod (name,so,ta)) when not need_dummy ->
1070 let res = CicReduction.are_convertible context so ind
1073 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1075 | C.Sort C.Set -> true
1077 (match CicEnvironment.get_obj uri with
1078 C.InductiveDefinition (itl,_,paramsno) ->
1079 let (_,_,_,cl) = List.nth itl i in
1082 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1085 (fun (_,x,_) i -> i && is_small tys paramsno x) cl true
1087 raise (WrongUriToMutualInductiveDefinitions
1088 (U.string_of_uri uri))
1090 | _ -> raise (Impossible 19)
1092 | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
1093 CicReduction.are_convertible context so ind
1096 and type_of_branch context argsno need_dummy outtype term constype =
1097 let module C = Cic in
1098 let module R = CicReduction in
1099 match R.whd context constype with
1104 C.Appl [outtype ; term]
1105 | C.Appl (C.MutInd (_,_,_)::tl) ->
1106 let (_,arguments) = split tl argsno
1108 if need_dummy && arguments = [] then
1111 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1112 | C.Prod (name,so,de) ->
1113 C.Prod (C.Anonimous,so,type_of_branch
1114 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1115 (CicSubstitution.lift 1 outtype)
1116 (C.Appl [CicSubstitution.lift 1 term ; C.Rel 1]) de)
1117 | _ -> raise (Impossible 20)
1119 (* check_metasenv_consistency checks that the "canonical" context of a
1120 metavariable is consitent - up to relocation via the relocation list l -
1121 with the actual context *)
1123 and check_metasenv_consistency metasenv context canonical_context l =
1124 let module C = Cic in
1125 let module R = CicReduction in
1126 let module S = CicSubstitution in
1127 let lifted_canonical_context =
1131 | (Some (n,C.Decl t))::tl ->
1132 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1133 | (Some (n,C.Def t))::tl ->
1134 (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1135 | None::tl -> None::(aux (i+1) tl)
1137 aux 1 canonical_context
1144 | Some t,Some (_,C.Def ct) ->
1145 R.are_convertible context t ct
1146 | Some t,Some (_,C.Decl ct) ->
1147 R.are_convertible context (type_of_aux' metasenv context t) ct
1150 if not res then raise MetasenvInconsistency
1151 ) l lifted_canonical_context
1153 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1154 and type_of_aux' metasenv context t =
1155 let rec type_of_aux context =
1156 let module C = Cic in
1157 let module R = CicReduction in
1158 let module S = CicSubstitution in
1159 let module U = UriManager in
1163 match List.nth context (n - 1) with
1164 Some (_,C.Decl t) -> S.lift n t
1165 | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
1166 | None -> raise RelToHiddenHypothesis
1168 _ -> raise (NotWellTyped "Not a close term")
1172 let ty = type_of_variable uri in
1176 let (_,canonical_context,ty) =
1177 List.find (function (m,_,_) -> n = m) metasenv
1179 check_metasenv_consistency metasenv context canonical_context l;
1180 CicSubstitution.lift_meta l ty
1181 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1182 | C.Implicit -> raise (Impossible 21)
1184 let _ = type_of_aux context ty in
1185 if R.are_convertible context (type_of_aux context te) ty then ty
1186 else raise (NotWellTyped "Cast")
1187 | C.Prod (name,s,t) ->
1188 let sort1 = type_of_aux context s
1189 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1190 sort_of_prod context (name,s) (sort1,sort2)
1191 | C.Lambda (n,s,t) ->
1192 let sort1 = type_of_aux context s
1193 and type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1194 let sort2 = type_of_aux ((Some (n,(C.Decl s)))::context) type2 in
1195 (* only to check if the product is well-typed *)
1196 let _ = sort_of_prod context (n,s) (sort1,sort2) in
1198 | C.LetIn (n,s,t) ->
1199 (* only to check if s is well-typed *)
1200 let _ = type_of_aux context s in
1201 C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)
1202 | C.Appl (he::tl) when List.length tl > 0 ->
1203 let hetype = type_of_aux context he
1204 and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1205 eat_prods context hetype tlbody_and_type
1206 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
1207 | C.Const (uri,cookingsno) ->
1209 let cty = cooked_type_of_constant uri cookingsno in
1212 | C.Abst _ -> raise (Impossible 22)
1213 | C.MutInd (uri,cookingsno,i) ->
1215 let cty = cooked_type_of_mutual_inductive_defs uri cookingsno i in
1218 | C.MutConstruct (uri,cookingsno,i,j) ->
1219 let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j
1222 | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
1223 let outsort = type_of_aux context outtype in
1224 let (need_dummy, k) =
1225 let rec guess_args context t =
1226 match CicReduction.whd context t with
1227 C.Sort _ -> (true, 0)
1228 | C.Prod (name, s, t) ->
1229 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1231 (* last prod before sort *)
1232 match CicReduction.whd context s with
1233 (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
1234 C.MutInd (uri',_,i') when U.eq uri' uri && i' = i -> (false, 1)
1235 | C.Appl ((C.MutInd (uri',_,i')) :: _)
1236 when U.eq uri' uri && i' = i -> (false, 1)
1240 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
1242 (*CSC whd non serve dopo type_of_aux ? *)
1243 let (b, k) = guess_args context outsort in
1244 if not b then (b, k - 1) else (b, k)
1246 let (parameters, arguments) =
1247 match R.whd context (type_of_aux context term) with
1248 (*CSC manca il caso dei CAST *)
1249 C.MutInd (uri',_,i') ->
1250 (*CSC vedi nota delirante sui cookingsno in cicReduction.ml*)
1251 if U.eq uri uri' && i = i' then ([],[])
1252 else raise (NotWellTyped ("MutCase: the term is of type " ^
1253 (U.string_of_uri uri') ^ "," ^ string_of_int i' ^
1254 " instead of type " ^ (U.string_of_uri uri') ^ "," ^
1256 | C.Appl (C.MutInd (uri',_,i') :: tl) ->
1257 if U.eq uri uri' && i = i' then split tl (List.length tl - k)
1258 else raise (NotWellTyped ("MutCase: the term is of type " ^
1259 (U.string_of_uri uri') ^ "," ^ string_of_int i' ^
1260 " instead of type " ^ (U.string_of_uri uri) ^ "," ^
1262 | _ -> raise (NotWellTyped "MutCase: the term is not an inductive one")
1264 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1265 let sort_of_ind_type =
1266 if parameters = [] then
1267 C.MutInd (uri,cookingsno,i)
1269 C.Appl ((C.MutInd (uri,cookingsno,i))::parameters)
1271 if not (check_allowed_sort_elimination context uri i need_dummy
1272 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1274 raise (NotWellTyped "MutCase: not allowed sort elimination") ;
1276 (* let's check if the type of branches are right *)
1278 match CicEnvironment.get_cooked_obj uri cookingsno with
1279 C.InductiveDefinition (tl,_,parsno) ->
1280 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
1282 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1284 let (_,branches_ok) =
1286 (fun (j,b) (p,(_,c,_)) ->
1288 if parameters = [] then
1289 (C.MutConstruct (uri,cookingsno,i,j))
1291 (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
1294 R.are_convertible context (type_of_aux context p)
1295 (type_of_branch context parsno need_dummy outtype cons
1296 (type_of_aux context cons))
1298 ) (1,true) (List.combine pl cl)
1300 if not branches_ok then
1301 raise (NotWellTyped "MutCase: wrong type of a branch") ;
1303 if not need_dummy then
1304 C.Appl ((outtype::arguments)@[term])
1305 else if arguments = [] then
1308 C.Appl (outtype::arguments)
1310 let types_times_kl =
1314 let _ = type_of_aux context ty in
1315 (Some (C.Name n,(C.Decl ty)),k)) fl)
1317 let (types,kl) = List.split types_times_kl in
1318 let len = List.length types in
1320 (fun (name,x,ty,bo) ->
1322 (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1323 (CicSubstitution.lift len ty))
1326 let (m, eaten, context') =
1327 eat_lambdas (types @ context) (x + 1) bo
1329 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1332 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1334 raise (NotWellTyped "Fix: not guarded by destructors")
1337 raise (NotWellTyped "Fix: ill-typed bodies")
1340 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1341 let (_,_,ty,_) = List.nth fl i in
1348 let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1350 let len = List.length types in
1354 (R.are_convertible (types @ context)
1355 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1358 (* let's control that the returned type is coinductive *)
1359 match returns_a_coinductive context ty with
1361 raise(NotWellTyped "CoFix: does not return a coinductive type")
1363 (*let's control the guarded by constructors conditions C{f,M}*)
1366 (guarded_by_constructors (types @ context) 0 len false bo
1369 raise (NotWellTyped "CoFix: not guarded by constructors")
1372 raise (NotWellTyped "CoFix: ill-typed bodies")
1375 let (_,ty,_) = List.nth fl i in
1378 and sort_of_prod context (name,s) (t1, t2) =
1379 let module C = Cic in
1380 let t1' = CicReduction.whd context t1 in
1381 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1382 match (t1', t2') with
1383 (C.Sort s1, C.Sort s2)
1384 when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
1386 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1390 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
1392 and eat_prods context hetype =
1393 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1397 | (hete, hety)::tl ->
1398 (match (CicReduction.whd context hetype) with
1400 if CicReduction.are_convertible context s hety then
1401 (CicReduction.fdebug := -1 ;
1402 eat_prods context (CicSubstitution.subst hete t) tl
1406 CicReduction.fdebug := 0 ;
1407 ignore (CicReduction.are_convertible context s hety) ;
1410 raise (NotWellTyped "Appl: wrong parameter-type")
1412 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
1415 and returns_a_coinductive context ty =
1416 let module C = Cic in
1417 match CicReduction.whd context ty with
1418 C.MutInd (uri,cookingsno,i) ->
1419 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1420 (match CicEnvironment.get_cooked_obj uri cookingsno with
1421 C.InductiveDefinition (itl,_,_) ->
1422 let (_,is_inductive,_,cl) = List.nth itl i in
1423 if is_inductive then None else (Some uri)
1425 raise (WrongUriToMutualInductiveDefinitions
1426 (UriManager.string_of_uri uri))
1428 | C.Appl ((C.MutInd (uri,_,i))::_) ->
1429 (match CicEnvironment.get_obj uri with
1430 C.InductiveDefinition (itl,_,_) ->
1431 let (_,is_inductive,_,_) = List.nth itl i in
1432 if is_inductive then None else (Some uri)
1434 raise (WrongUriToMutualInductiveDefinitions
1435 (UriManager.string_of_uri uri))
1437 | C.Prod (n,so,de) ->
1438 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1443 prerr_endline ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1446 type_of_aux context t
1448 in prerr_endline "FINE TYPE_OF_AUX" ; flush stderr ; res
1451 (* is a small constructor? *)
1452 (*CSC: ottimizzare calcolando staticamente *)
1453 and is_small context paramsno c =
1454 let rec is_small_aux context c =
1455 let module C = Cic in
1456 match CicReduction.whd context c with
1458 (*CSC: [] is an empty metasenv. Is it correct? *)
1459 let s = type_of_aux' [] context so in
1460 (s = C.Sort C.Prop || s = C.Sort C.Set) &&
1461 is_small_aux ((Some (n,(C.Decl so)))::context) de
1462 | _ -> true (*CSC: we trust the type-checker *)
1464 let (context',dx) = split_prods context paramsno c in
1465 is_small_aux context' dx
1469 prerr_endline ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1472 type_of_aux' [] [] t
1474 in prerr_endline "FINE TYPE_OF_AUX'" ; flush stderr ; res
1479 let module C = Cic in
1480 let module R = CicReduction in
1481 let module U = UriManager in
1482 match CicEnvironment.is_type_checked uri 0 with
1483 CicEnvironment.CheckedObj _ -> ()
1484 | CicEnvironment.UncheckedObj uobj ->
1485 (* let's typecheck the uncooked object *)
1486 Logger.log (`Start_type_checking uri) ;
1488 C.Definition (_,te,ty,_) ->
1489 let _ = type_of ty in
1490 if not (R.are_convertible [] (type_of te ) ty) then
1491 raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
1492 | C.Axiom (_,ty,_) ->
1493 (* only to check that ty is well-typed *)
1494 let _ = type_of ty in ()
1495 | C.CurrentProof (_,conjs,te,ty) ->
1497 let _ = type_of_aux' conjs [] ty in
1498 debug (type_of_aux' conjs [] te) [] ;
1499 if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then
1500 raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
1501 | C.Variable (_,bo,ty) ->
1502 (* only to check that ty is well-typed *)
1503 let _ = type_of ty in
1507 if not (R.are_convertible [] (type_of bo) ty) then
1508 raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri)))
1510 | C.InductiveDefinition _ ->
1511 cooked_mutual_inductive_defs uri uobj
1513 CicEnvironment.set_type_checking_info uri ;
1514 Logger.log (`Type_checking_completed uri)