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 (*CSC: bisogna controllare anche il metasenv!!! *)
79 let _ = type_of_aux' conjs [] ty in
80 if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
82 raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
83 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
85 CicEnvironment.set_type_checking_info uri ;
86 Logger.log (`Type_checking_completed uri) ;
87 match CicEnvironment.is_type_checked uri cookingsno with
88 CicEnvironment.CheckedObj cobj -> cobj
89 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
92 C.Definition (_,_,ty,_) -> ty
93 | C.Axiom (_,ty,_) -> ty
94 | C.CurrentProof (_,_,_,ty) -> ty
95 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
97 and type_of_variable uri =
99 let module R = CicReduction in
100 let module U = UriManager in
101 (* 0 because a variable is never cooked => no partial cooking at one level *)
102 match CicEnvironment.is_type_checked uri 0 with
103 CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
104 | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty)) ->
105 Logger.log (`Start_type_checking uri) ;
106 (* only to check that ty is well-typed *)
107 let _ = type_of ty in
111 if not (R.are_convertible [] (type_of bo) ty) then
112 raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
114 CicEnvironment.set_type_checking_info uri ;
115 Logger.log (`Type_checking_completed uri) ;
117 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
119 and does_not_occur context n nn te =
120 let module C = Cic in
121 (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
122 (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
124 match CicReduction.whd context te with
125 C.Rel m when m > n && m <= nn -> false
132 does_not_occur context n nn te && does_not_occur context n nn ty
133 | C.Prod (name,so,dest) ->
134 does_not_occur context n nn so &&
135 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
136 | C.Lambda (name,so,dest) ->
137 does_not_occur context n nn so &&
138 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
139 | C.LetIn (name,so,dest) ->
140 does_not_occur context n nn so &&
141 does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest
143 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 *)
447 | C.Const _ -> raise (Impossible 5)
452 | C.CoFix _ -> raise (Impossible 6) (* due to type-checking *)
454 and get_new_safes context p c rl safes n nn x =
455 let module C = Cic in
456 let module U = UriManager in
457 let module R = CicReduction in
458 match (R.whd context c, R.whd context p, rl) with
459 (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
460 (* we are sure that the two sources are convertible because we *)
461 (* have just checked this. So let's go along ... *)
463 List.map (fun x -> x + 1) safes
466 if b then 1::safes' else safes'
468 get_new_safes ((Some (name,(C.Decl so)))::context)
469 ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
470 | (C.Prod _, (C.MutConstruct _ as e), _)
471 | (C.Prod _, (C.Rel _ as e), _)
472 | (C.MutInd _, e, [])
473 | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
475 (* CSC: If the next exception is raised, it just means that *)
476 (* CSC: the proof-assistant allows to use very strange things *)
477 (* CSC: as a branch of a case whose type is a Prod. In *)
478 (* CSC: particular, this means that a new (C.Prod, x,_) case *)
479 (* CSC: must be considered in this match. (e.g. x = MutCase) *)
482 and split_prods context n te =
483 let module C = Cic in
484 let module R = CicReduction in
485 match (n, R.whd context te) with
487 | (n, C.Prod (name,so,ta)) when n > 0 ->
488 split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta
489 | (_, _) -> raise (Impossible 8)
491 and eat_lambdas context n te =
492 let module C = Cic in
493 let module R = CicReduction in
494 match (n, R.whd context te) with
495 (0, _) -> (te, 0, context)
496 | (n, C.Lambda (name,so,ta)) when n > 0 ->
497 let (te, k, context') =
498 eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
500 (te, k + 1, context')
501 | (_, _) -> raise (Impossible 9)
503 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
504 and check_is_really_smaller_arg context n nn kl x safes te =
505 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
506 (*CSC: cfr guarded_by_destructors *)
507 let module C = Cic in
508 let module U = UriManager in
509 match CicReduction.whd context te with
510 C.Rel m when List.mem m safes -> true
517 (* | C.Cast (te,ty) ->
518 check_is_really_smaller_arg n nn kl x safes te &&
519 check_is_really_smaller_arg n nn kl x safes ty*)
520 (* | C.Prod (_,so,ta) ->
521 check_is_really_smaller_arg n nn kl x safes so &&
522 check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
523 (List.map (fun x -> x + 1) safes) ta*)
524 | C.Prod _ -> raise (Impossible 10)
525 | C.Lambda (name,so,ta) ->
526 check_is_really_smaller_arg context n nn kl x safes so &&
527 check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context)
528 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
529 | C.LetIn (name,so,ta) ->
530 check_is_really_smaller_arg context n nn kl x safes so &&
531 check_is_really_smaller_arg ((Some (name,(C.Def so)))::context)
532 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
534 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
535 (*CSC: solo perche' non abbiamo trovato controesempi *)
536 check_is_really_smaller_arg context n nn kl x safes he
537 | C.Appl [] -> raise (Impossible 11)
539 | C.MutInd _ -> raise (Impossible 12)
540 | C.MutConstruct _ -> false
541 | C.MutCase (uri,_,i,outtype,term,pl) ->
543 C.Rel m when List.mem m safes || m = x ->
544 let (isinductive,paramsno,cl) =
545 match CicEnvironment.get_obj uri with
546 C.InductiveDefinition (tl,_,paramsno) ->
548 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
550 let (_,isinductive,_,cl) = List.nth tl i in
554 (id, snd (split_prods tys paramsno ty), r)) cl
556 (isinductive,paramsno,cl')
558 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
560 if not isinductive then
563 i && check_is_really_smaller_arg context n nn kl x safes p)
567 (fun (p,(_,c,rl)) i ->
571 let (_,rl'') = split rl' paramsno in
573 | None -> raise (Impossible 13)
575 let (e,safes',n',nn',x',context') =
576 get_new_safes context p c rl' safes n nn x
579 check_is_really_smaller_arg context' n' nn' kl x' safes' e
580 ) (List.combine pl cl) true
581 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
582 let (isinductive,paramsno,cl) =
583 match CicEnvironment.get_obj uri with
584 C.InductiveDefinition (tl,_,paramsno) ->
585 let (_,isinductive,_,cl) = List.nth tl i in
587 List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
592 (id, snd (split_prods tys paramsno ty), r)) cl
594 (isinductive,paramsno,cl')
596 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
598 if not isinductive then
601 i && check_is_really_smaller_arg context n nn kl x safes p)
604 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
605 (*CSC: sugli argomenti di una applicazione *)
607 (fun (p,(_,c,rl)) i ->
611 let (_,rl'') = split rl' paramsno in
613 | None -> raise (Impossible 14)
615 let (e, safes',n',nn',x',context') =
616 get_new_safes context p c rl' safes n nn x
619 check_is_really_smaller_arg context' n' nn' kl x' safes' e
620 ) (List.combine pl cl) true
624 i && check_is_really_smaller_arg context n nn kl x safes p
628 let len = List.length fl in
629 let n_plus_len = n + len
630 and nn_plus_len = nn + len
631 and x_plus_len = x + len
632 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
633 and safes' = List.map (fun x -> x + len) safes in
635 (fun (_,_,ty,bo) i ->
637 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
641 let len = List.length fl in
642 let n_plus_len = n + len
643 and nn_plus_len = nn + len
644 and x_plus_len = x + len
645 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
646 and safes' = List.map (fun x -> x + len) safes in
650 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
654 and guarded_by_destructors context n nn kl x safes =
655 let module C = Cic in
656 let module U = UriManager in
658 C.Rel m when m > n && m <= nn -> false
660 (match List.nth context (n-1) with
661 Some (_,C.Decl _) -> true
662 | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo
663 | None -> raise RelToHiddenHypothesis
670 guarded_by_destructors context n nn kl x safes te &&
671 guarded_by_destructors context n nn kl x safes ty
672 | C.Prod (name,so,ta) ->
673 guarded_by_destructors context n nn kl x safes so &&
674 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
675 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
676 | C.Lambda (name,so,ta) ->
677 guarded_by_destructors context n nn kl x safes so &&
678 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
679 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
680 | C.LetIn (name,so,ta) ->
681 guarded_by_destructors context n nn kl x safes so &&
682 guarded_by_destructors ((Some (name,(C.Def so)))::context)
683 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
684 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
685 let k = List.nth kl (m - n - 1) in
686 if not (List.length tl > k) then false
690 i && guarded_by_destructors context n nn kl x safes param
692 check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
695 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
699 | C.MutConstruct _ -> true
700 | C.MutCase (uri,_,i,outtype,term,pl) ->
702 C.Rel m when List.mem m safes || m = x ->
703 let (isinductive,paramsno,cl) =
704 match CicEnvironment.get_obj uri with
705 C.InductiveDefinition (tl,_,paramsno) ->
706 let (_,isinductive,_,cl) = List.nth tl i in
708 List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
713 (id, snd (split_prods tys paramsno ty), r)) cl
715 (isinductive,paramsno,cl')
717 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
719 if not isinductive then
720 guarded_by_destructors context n nn kl x safes outtype &&
721 guarded_by_destructors context n nn kl x safes term &&
722 (*CSC: manca ??? il controllo sul tipo di term? *)
725 i && guarded_by_destructors context n nn kl x safes p)
728 guarded_by_destructors context n nn kl x safes outtype &&
729 (*CSC: manca ??? il controllo sul tipo di term? *)
731 (fun (p,(_,c,rl)) i ->
735 let (_,rl'') = split rl' paramsno in
737 | None -> raise (Impossible 15)
739 let (e,safes',n',nn',x',context') =
740 get_new_safes context p c rl' safes n nn x
743 guarded_by_destructors context' n' nn' kl x' safes' e
744 ) (List.combine pl cl) true
745 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
746 let (isinductive,paramsno,cl) =
747 match CicEnvironment.get_obj uri with
748 C.InductiveDefinition (tl,_,paramsno) ->
749 let (_,isinductive,_,cl) = List.nth tl i in
751 List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
756 (id, snd (split_prods tys paramsno ty), r)) cl
758 (isinductive,paramsno,cl')
760 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
762 if not isinductive then
763 guarded_by_destructors context n nn kl x safes outtype &&
764 guarded_by_destructors context n nn kl x safes term &&
765 (*CSC: manca ??? il controllo sul tipo di term? *)
768 i && guarded_by_destructors context n nn kl x safes p)
771 guarded_by_destructors context n nn kl x safes outtype &&
772 (*CSC: manca ??? il controllo sul tipo di term? *)
775 i && guarded_by_destructors context n nn kl x safes t)
778 (fun (p,(_,c,rl)) i ->
782 let (_,rl'') = split rl' paramsno in
784 | None -> raise (Impossible 16)
786 let (e, safes',n',nn',x',context') =
787 get_new_safes context p c rl' safes n nn x
790 guarded_by_destructors context' n' nn' kl x' safes' e
791 ) (List.combine pl cl) true
793 guarded_by_destructors context n nn kl x safes outtype &&
794 guarded_by_destructors context n nn kl x safes term &&
795 (*CSC: manca ??? il controllo sul tipo di term? *)
797 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
801 let len = List.length fl in
802 let n_plus_len = n + len
803 and nn_plus_len = nn + len
804 and x_plus_len = x + len
805 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
806 and safes' = List.map (fun x -> x + len) safes in
808 (fun (_,_,ty,bo) i ->
809 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
810 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
814 let len = List.length fl in
815 let n_plus_len = n + len
816 and nn_plus_len = nn + len
817 and x_plus_len = x + len
818 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
819 and safes' = List.map (fun x -> x + len) safes in
823 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
824 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
828 (* the boolean h means already protected *)
829 (* args is the list of arguments the type of the constructor that may be *)
830 (* found in head position must be applied to. *)
831 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
832 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
833 let module C = Cic in
834 (*CSC: There is a lot of code replication between the cases X and *)
835 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
836 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
837 match CicReduction.whd context te with
838 C.Rel m when m > n && m <= nn -> h
847 raise (Impossible 17) (* the term has just been type-checked *)
848 | C.Lambda (name,so,de) ->
849 does_not_occur context n nn so &&
850 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
851 (n + 1) (nn + 1) h de args coInductiveTypeURI
852 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
854 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
855 | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) ->
857 match CicEnvironment.get_cooked_obj uri cookingsno with
858 C.InductiveDefinition (itl,_,_) ->
859 let (_,_,_,cl) = List.nth itl i in
860 let (_,cons,_) = List.nth cl (j - 1) in cons
862 raise (WrongUriToMutualInductiveDefinitions
863 (UriManager.string_of_uri uri))
865 let rec analyse_branch context ty te =
866 match CicReduction.whd context ty with
867 C.Meta _ -> raise (Impossible 34)
871 does_not_occur context n nn te
873 | C.Cast _ -> raise (Impossible 24) (* due to type-checking *)
874 | C.Prod (name,so,de) ->
875 analyse_branch ((Some (name,(C.Decl so)))::context) de te
877 | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *)
878 | C.Appl ((C.MutInd (uri,_,_))::tl) as ty
879 when uri == coInductiveTypeURI ->
880 guarded_by_constructors context n nn true te [] coInductiveTypeURI
881 | C.Appl ((C.MutInd (uri,_,_))::tl) as ty ->
882 guarded_by_constructors context n nn true te tl coInductiveTypeURI
884 does_not_occur context n nn te
885 | C.Const _ -> raise (Impossible 26)
886 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
887 guarded_by_constructors context n nn true te [] coInductiveTypeURI
889 does_not_occur context n nn te
890 | C.MutConstruct _ -> raise (Impossible 27)
891 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
892 (*CSC: in head position. *)
895 | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *)
897 let rec analyse_instantiated_type context ty l =
898 match CicReduction.whd context ty with
904 | C.Cast _ -> raise (Impossible 29) (* due to type-checking *)
905 | C.Prod (name,so,de) ->
910 analyse_branch context so he &&
911 analyse_instantiated_type ((Some (name,(C.Decl so)))::context)
915 | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *)
918 (fun i x -> i && does_not_occur context n nn x) true l
919 | C.Const _ -> raise (Impossible 31)
922 (fun i x -> i && does_not_occur context n nn x) true l
923 | C.MutConstruct _ -> raise (Impossible 32)
924 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
925 (*CSC: in head position. *)
928 | C.CoFix _ -> raise (Impossible 33) (* due to type-checking *)
930 let rec instantiate_type args consty =
934 let consty' = CicReduction.whd context consty in
940 let instantiated_de = CicSubstitution.subst he de in
941 (*CSC: siamo sicuri che non sia troppo forte? *)
942 does_not_occur context n nn tlhe &
943 instantiate_type tl instantiated_de tltl
945 (*CSC:We do not consider backbones with a MutCase, a *)
946 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
947 raise (Impossible 23)
949 | [] -> analyse_instantiated_type context consty' l
950 (* These are all the other cases *)
952 instantiate_type args consty tl
953 | C.Appl ((C.CoFix (_,fl))::tl) ->
954 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
955 let len = List.length fl in
956 let n_plus_len = n + len
957 and nn_plus_len = nn + len
958 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
959 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
962 i && does_not_occur context n nn ty &&
963 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
964 args coInductiveTypeURI
966 | C.Appl ((C.MutCase (_,_,_,out,te,pl))::tl) ->
967 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
968 does_not_occur context n nn out &&
969 does_not_occur context n nn te &&
973 guarded_by_constructors context n nn h x args coInductiveTypeURI
976 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
978 | C.MutInd _ -> assert false
979 | C.MutConstruct _ -> true
980 | C.MutCase (_,_,_,out,te,pl) ->
981 does_not_occur context n nn out &&
982 does_not_occur context n nn te &&
986 guarded_by_constructors context n nn h x args coInductiveTypeURI
989 let len = List.length fl in
990 let n_plus_len = n + len
991 and nn_plus_len = nn + len
992 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
993 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
995 (fun (_,_,ty,bo) i ->
996 i && does_not_occur context n nn ty &&
997 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1000 let len = List.length fl in
1001 let n_plus_len = n + len
1002 and nn_plus_len = nn + len
1003 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1004 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1007 i && does_not_occur context n nn ty &&
1008 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1009 args coInductiveTypeURI
1012 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1013 let module C = Cic in
1014 let module U = UriManager in
1015 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1016 (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1017 when CicReduction.are_convertible context so1 so2 ->
1018 check_allowed_sort_elimination context uri i need_dummy
1019 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1020 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1021 | (C.Sort C.Prop, C.Sort C.Set) when need_dummy ->
1022 (match CicEnvironment.get_obj uri with
1023 C.InductiveDefinition (itl,_,_) ->
1024 let (_,_,_,cl) = List.nth itl i in
1025 (* is a singleton definition? *)
1028 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1030 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1031 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1032 | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
1033 (match CicEnvironment.get_obj uri with
1034 C.InductiveDefinition (itl,_,paramsno) ->
1036 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1038 let (_,_,_,cl) = List.nth itl i in
1040 (fun (_,x,_) i -> i && is_small tys paramsno x) cl true
1042 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1044 | (C.Sort C.Type, C.Sort _) when need_dummy -> true
1045 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1046 let res = CicReduction.are_convertible context so ind
1049 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1050 C.Sort C.Prop -> true
1052 (match CicEnvironment.get_obj uri with
1053 C.InductiveDefinition (itl,_,_) ->
1054 let (_,_,_,cl) = List.nth itl i in
1055 (* is a singleton definition? *)
1058 raise (WrongUriToMutualInductiveDefinitions
1059 (U.string_of_uri uri))
1063 | (C.Sort C.Set, C.Prod (name,so,ta)) when not need_dummy ->
1064 let res = CicReduction.are_convertible context so ind
1067 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1069 | C.Sort C.Set -> true
1071 (match CicEnvironment.get_obj uri with
1072 C.InductiveDefinition (itl,_,paramsno) ->
1073 let (_,_,_,cl) = List.nth itl i in
1076 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1079 (fun (_,x,_) i -> i && is_small tys paramsno x) cl true
1081 raise (WrongUriToMutualInductiveDefinitions
1082 (U.string_of_uri uri))
1084 | _ -> raise (Impossible 19)
1086 | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
1087 CicReduction.are_convertible context so ind
1090 and type_of_branch context argsno need_dummy outtype term constype =
1091 let module C = Cic in
1092 let module R = CicReduction in
1093 match R.whd context constype with
1098 C.Appl [outtype ; term]
1099 | C.Appl (C.MutInd (_,_,_)::tl) ->
1100 let (_,arguments) = split tl argsno
1102 if need_dummy && arguments = [] then
1105 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1106 | C.Prod (name,so,de) ->
1108 match CicSubstitution.lift 1 term with
1109 C.Appl l -> C.Appl (l@[C.Rel 1])
1110 | t -> C.Appl [t ; C.Rel 1]
1112 C.Prod (C.Anonimous,so,type_of_branch
1113 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1114 (CicSubstitution.lift 1 outtype) term' de)
1115 | _ -> raise (Impossible 20)
1117 (* check_metasenv_consistency checks that the "canonical" context of a
1118 metavariable is consitent - up to relocation via the relocation list l -
1119 with the actual context *)
1121 and check_metasenv_consistency metasenv context canonical_context l =
1122 let module C = Cic in
1123 let module R = CicReduction in
1124 let module S = CicSubstitution in
1125 let lifted_canonical_context =
1129 | (Some (n,C.Decl t))::tl ->
1130 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1131 | (Some (n,C.Def t))::tl ->
1132 (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1133 | None::tl -> None::(aux (i+1) tl)
1135 aux 1 canonical_context
1142 | Some t,Some (_,C.Def ct) ->
1143 R.are_convertible context t ct
1144 | Some t,Some (_,C.Decl ct) ->
1145 R.are_convertible context (type_of_aux' metasenv context t) ct
1148 if not res then raise MetasenvInconsistency
1149 ) l lifted_canonical_context
1151 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1152 and type_of_aux' metasenv context t =
1153 let rec type_of_aux context =
1154 let module C = Cic in
1155 let module R = CicReduction in
1156 let module S = CicSubstitution in
1157 let module U = UriManager in
1161 match List.nth context (n - 1) with
1162 Some (_,C.Decl t) -> S.lift n t
1163 | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
1164 | None -> raise RelToHiddenHypothesis
1166 _ -> raise (NotWellTyped "Not a close term")
1170 let ty = type_of_variable uri in
1174 let (_,canonical_context,ty) =
1175 List.find (function (m,_,_) -> n = m) metasenv
1177 check_metasenv_consistency metasenv context canonical_context l;
1178 CicSubstitution.lift_meta l ty
1179 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1180 | C.Implicit -> raise (Impossible 21)
1182 let _ = type_of_aux context ty in
1183 if R.are_convertible context (type_of_aux context te) ty then ty
1184 else raise (NotWellTyped "Cast")
1185 | C.Prod (name,s,t) ->
1186 let sort1 = type_of_aux context s
1187 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1188 sort_of_prod context (name,s) (sort1,sort2)
1189 | C.Lambda (n,s,t) ->
1190 let sort1 = type_of_aux context s
1191 and type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1192 let sort2 = type_of_aux ((Some (n,(C.Decl s)))::context) type2 in
1193 (* only to check if the product is well-typed *)
1194 let _ = sort_of_prod context (n,s) (sort1,sort2) in
1196 | C.LetIn (n,s,t) ->
1197 (* only to check if s is well-typed *)
1198 let _ = type_of_aux context s in
1199 C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)
1200 | C.Appl (he::tl) when List.length tl > 0 ->
1201 let hetype = type_of_aux context he
1202 and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1203 eat_prods context hetype tlbody_and_type
1204 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
1205 | C.Const (uri,cookingsno) ->
1207 let cty = cooked_type_of_constant uri cookingsno in
1210 | C.MutInd (uri,cookingsno,i) ->
1212 let cty = cooked_type_of_mutual_inductive_defs uri cookingsno i in
1215 | C.MutConstruct (uri,cookingsno,i,j) ->
1216 let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j
1219 | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
1220 let outsort = type_of_aux context outtype in
1221 let (need_dummy, k) =
1222 let rec guess_args context t =
1223 match CicReduction.whd context t with
1224 C.Sort _ -> (true, 0)
1225 | C.Prod (name, s, t) ->
1226 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1228 (* last prod before sort *)
1229 match CicReduction.whd context s with
1230 (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
1231 C.MutInd (uri',_,i') when U.eq uri' uri && i' = i -> (false, 1)
1232 | C.Appl ((C.MutInd (uri',_,i')) :: _)
1233 when U.eq uri' uri && i' = i -> (false, 1)
1237 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
1239 (*CSC whd non serve dopo type_of_aux ? *)
1240 let (b, k) = guess_args context outsort in
1241 if not b then (b, k - 1) else (b, k)
1243 let (parameters, arguments) =
1244 match R.whd context (type_of_aux context term) with
1245 (*CSC manca il caso dei CAST *)
1246 C.MutInd (uri',_,i') ->
1247 (*CSC vedi nota delirante sui cookingsno in cicReduction.ml*)
1248 if U.eq uri uri' && i = i' then ([],[])
1249 else raise (NotWellTyped ("MutCase: the term is of type " ^
1250 (U.string_of_uri uri') ^ "," ^ string_of_int i' ^
1251 " instead of type " ^ (U.string_of_uri uri') ^ "," ^
1253 | C.Appl (C.MutInd (uri',_,i') :: tl) ->
1254 if U.eq uri uri' && i = i' then split tl (List.length tl - k)
1255 else raise (NotWellTyped ("MutCase: the term is of type " ^
1256 (U.string_of_uri uri') ^ "," ^ string_of_int i' ^
1257 " instead of type " ^ (U.string_of_uri uri) ^ "," ^
1259 | _ -> raise (NotWellTyped "MutCase: the term is not an inductive one")
1261 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1262 let sort_of_ind_type =
1263 if parameters = [] then
1264 C.MutInd (uri,cookingsno,i)
1266 C.Appl ((C.MutInd (uri,cookingsno,i))::parameters)
1268 if not (check_allowed_sort_elimination context uri i need_dummy
1269 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1271 raise (NotWellTyped "MutCase: not allowed sort elimination") ;
1273 (* let's check if the type of branches are right *)
1275 match CicEnvironment.get_cooked_obj uri cookingsno with
1276 C.InductiveDefinition (tl,_,parsno) ->
1277 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
1279 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1281 let (_,branches_ok) =
1283 (fun (j,b) (p,(_,c,_)) ->
1285 if parameters = [] then
1286 (C.MutConstruct (uri,cookingsno,i,j))
1288 (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
1291 R.are_convertible context (type_of_aux context p)
1292 (type_of_branch context parsno need_dummy outtype cons
1293 (type_of_aux context cons))
1295 ) (1,true) (List.combine pl cl)
1297 if not branches_ok then
1298 raise (NotWellTyped "MutCase: wrong type of a branch") ;
1300 if not need_dummy then
1301 C.Appl ((outtype::arguments)@[term])
1302 else if arguments = [] then
1305 C.Appl (outtype::arguments)
1307 let types_times_kl =
1311 let _ = type_of_aux context ty in
1312 (Some (C.Name n,(C.Decl ty)),k)) fl)
1314 let (types,kl) = List.split types_times_kl in
1315 let len = List.length types in
1317 (fun (name,x,ty,bo) ->
1319 (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1320 (CicSubstitution.lift len ty))
1323 let (m, eaten, context') =
1324 eat_lambdas (types @ context) (x + 1) bo
1326 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1329 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1331 raise (NotWellTyped "Fix: not guarded by destructors")
1334 raise (NotWellTyped "Fix: ill-typed bodies")
1337 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1338 let (_,_,ty,_) = List.nth fl i in
1345 let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1347 let len = List.length types in
1351 (R.are_convertible (types @ context)
1352 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1355 (* let's control that the returned type is coinductive *)
1356 match returns_a_coinductive context ty with
1358 raise(NotWellTyped "CoFix: does not return a coinductive type")
1360 (*let's control the guarded by constructors conditions C{f,M}*)
1363 (guarded_by_constructors (types @ context) 0 len false bo
1366 raise (NotWellTyped "CoFix: not guarded by constructors")
1369 raise (NotWellTyped "CoFix: ill-typed bodies")
1372 let (_,ty,_) = List.nth fl i in
1375 and sort_of_prod context (name,s) (t1, t2) =
1376 let module C = Cic in
1377 let t1' = CicReduction.whd context t1 in
1378 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1379 match (t1', t2') with
1380 (C.Sort s1, C.Sort s2)
1381 when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
1383 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1387 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
1389 and eat_prods context hetype =
1390 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1394 | (hete, hety)::tl ->
1395 (match (CicReduction.whd context hetype) with
1397 if CicReduction.are_convertible context s hety then
1398 (CicReduction.fdebug := -1 ;
1399 eat_prods context (CicSubstitution.subst hete t) tl
1403 CicReduction.fdebug := 0 ;
1404 ignore (CicReduction.are_convertible context s hety) ;
1407 raise (NotWellTyped "Appl: wrong parameter-type")
1409 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
1412 and returns_a_coinductive context ty =
1413 let module C = Cic in
1414 match CicReduction.whd context ty with
1415 C.MutInd (uri,cookingsno,i) ->
1416 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1417 (match CicEnvironment.get_cooked_obj uri cookingsno with
1418 C.InductiveDefinition (itl,_,_) ->
1419 let (_,is_inductive,_,cl) = List.nth itl i in
1420 if is_inductive then None else (Some uri)
1422 raise (WrongUriToMutualInductiveDefinitions
1423 (UriManager.string_of_uri uri))
1425 | C.Appl ((C.MutInd (uri,_,i))::_) ->
1426 (match CicEnvironment.get_obj uri with
1427 C.InductiveDefinition (itl,_,_) ->
1428 let (_,is_inductive,_,_) = List.nth itl i in
1429 if is_inductive then None else (Some uri)
1431 raise (WrongUriToMutualInductiveDefinitions
1432 (UriManager.string_of_uri uri))
1434 | C.Prod (n,so,de) ->
1435 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1440 prerr_endline ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1443 type_of_aux context t
1445 in prerr_endline "FINE TYPE_OF_AUX" ; flush stderr ; res
1448 (* is a small constructor? *)
1449 (*CSC: ottimizzare calcolando staticamente *)
1450 and is_small context paramsno c =
1451 let rec is_small_aux context c =
1452 let module C = Cic in
1453 match CicReduction.whd context c with
1455 (*CSC: [] is an empty metasenv. Is it correct? *)
1456 let s = type_of_aux' [] context so in
1457 (s = C.Sort C.Prop || s = C.Sort C.Set) &&
1458 is_small_aux ((Some (n,(C.Decl so)))::context) de
1459 | _ -> true (*CSC: we trust the type-checker *)
1461 let (context',dx) = split_prods context paramsno c in
1462 is_small_aux context' dx
1466 prerr_endline ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1469 type_of_aux' [] [] t
1471 in prerr_endline "FINE TYPE_OF_AUX'" ; flush stderr ; res
1476 let module C = Cic in
1477 let module R = CicReduction in
1478 let module U = UriManager in
1479 match CicEnvironment.is_type_checked uri 0 with
1480 CicEnvironment.CheckedObj _ -> ()
1481 | CicEnvironment.UncheckedObj uobj ->
1482 (* let's typecheck the uncooked object *)
1483 Logger.log (`Start_type_checking uri) ;
1485 C.Definition (_,te,ty,_) ->
1486 let _ = type_of ty in
1487 if not (R.are_convertible [] (type_of te ) ty) then
1488 raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
1489 | C.Axiom (_,ty,_) ->
1490 (* only to check that ty is well-typed *)
1491 let _ = type_of ty in ()
1492 | C.CurrentProof (_,conjs,te,ty) ->
1493 (*CSC: bisogna controllare anche il metasenv!!! *)
1494 let _ = type_of_aux' conjs [] ty in
1495 debug (type_of_aux' conjs [] te) [] ;
1496 if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then
1497 raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
1498 | C.Variable (_,bo,ty) ->
1499 (* only to check that ty is well-typed *)
1500 let _ = type_of ty in
1504 if not (R.are_convertible [] (type_of bo) ty) then
1505 raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri)))
1507 | C.InductiveDefinition _ ->
1508 cooked_mutual_inductive_defs uri uobj
1510 CicEnvironment.set_type_checking_info uri ;
1511 Logger.log (`Type_checking_completed uri)