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 let debrujin_constructor uri number_of_types =
62 | C.Var (uri,exp_named_subst) ->
63 let exp_named_subst' =
64 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
66 C.Var (uri,exp_named_subst')
67 | C.Meta _ -> assert false
69 | C.Implicit as t -> t
70 | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
71 | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
72 | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
73 | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t)
74 | C.Appl l -> C.Appl (List.map (aux k) l)
75 | C.Const (uri,exp_named_subst) ->
76 let exp_named_subst' =
77 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
79 C.Const (uri,exp_named_subst')
80 | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
81 if exp_named_subst != [] then
84 ("Debrujin: a non-empty explicit named substitution is applied to " ^
85 "a mutual inductive type which is being defined")) ;
86 C.Rel (k + number_of_types - tyno) ;
87 | C.MutInd (uri',tyno,exp_named_subst) ->
88 let exp_named_subst' =
89 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
91 C.MutInd (uri',tyno,exp_named_subst')
92 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
93 let exp_named_subst' =
94 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
96 C.MutConstruct (uri,tyno,consno,exp_named_subst')
97 | C.MutCase (sp,i,outty,t,pl) ->
98 C.MutCase (sp, i, aux k outty, aux k t,
101 let len = List.length fl in
104 (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
109 let len = List.length fl in
112 (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
115 C.CoFix (i, liftedfl)
120 exception CicEnvironmentError;;
122 let rec type_of_constant uri =
123 let module C = Cic in
124 let module R = CicReduction in
125 let module U = UriManager in
127 match CicEnvironment.is_type_checked ~trust:true uri with
128 CicEnvironment.CheckedObj cobj -> cobj
129 | CicEnvironment.UncheckedObj uobj ->
130 Logger.log (`Start_type_checking uri) ;
131 (* let's typecheck the uncooked obj *)
133 C.Constant (_,Some te,ty,_) ->
134 let _ = type_of ty in
135 if not (R.are_convertible [] (type_of te) ty) then
136 raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
137 | C.Constant (_,None,ty,_) ->
138 (* only to check that ty is well-typed *)
139 let _ = type_of ty in ()
140 | C.CurrentProof (_,conjs,te,ty,_) ->
143 (fun metasenv ((_,context,ty) as conj) ->
144 ignore (type_of_aux' metasenv context ty) ;
148 let _ = type_of_aux' conjs [] ty in
149 if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
151 raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
152 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
154 CicEnvironment.set_type_checking_info uri ;
155 Logger.log (`Type_checking_completed uri) ;
156 match CicEnvironment.is_type_checked ~trust:false uri with
157 CicEnvironment.CheckedObj cobj -> cobj
158 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
161 C.Constant (_,_,ty,_) -> ty
162 | C.CurrentProof (_,_,_,ty,_) -> ty
163 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
165 and type_of_variable uri =
166 let module C = Cic in
167 let module R = CicReduction in
168 let module U = UriManager in
169 (* 0 because a variable is never cooked => no partial cooking at one level *)
170 match CicEnvironment.is_type_checked ~trust:true uri with
171 CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
172 | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
173 Logger.log (`Start_type_checking uri) ;
174 (* only to check that ty is well-typed *)
175 let _ = type_of ty in
179 if not (R.are_convertible [] (type_of bo) ty) then
180 raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
182 CicEnvironment.set_type_checking_info uri ;
183 Logger.log (`Type_checking_completed uri) ;
185 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
187 and does_not_occur context n nn te =
188 let module C = Cic in
189 (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
190 (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
192 match CicReduction.whd context te with
193 C.Rel m when m > n && m <= nn -> false
199 does_not_occur context n nn te && does_not_occur context n nn ty
200 | C.Prod (name,so,dest) ->
201 does_not_occur context n nn so &&
202 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
203 | C.Lambda (name,so,dest) ->
204 does_not_occur context n nn so &&
205 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
206 | C.LetIn (name,so,dest) ->
207 does_not_occur context n nn so &&
208 does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest
210 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
211 | C.Var (_,exp_named_subst)
212 | C.Const (_,exp_named_subst)
213 | C.MutInd (_,_,exp_named_subst)
214 | C.MutConstruct (_,_,_,exp_named_subst) ->
215 List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
217 | C.MutCase (_,_,out,te,pl) ->
218 does_not_occur context n nn out && does_not_occur context n nn te &&
219 List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
221 let len = List.length fl in
222 let n_plus_len = n + len in
223 let nn_plus_len = nn + len in
225 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
228 (fun (_,_,ty,bo) i ->
229 i && does_not_occur context n nn ty &&
230 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
233 let len = List.length fl in
234 let n_plus_len = n + len in
235 let nn_plus_len = nn + len in
237 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
241 i && does_not_occur context n nn ty &&
242 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
245 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
246 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
247 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
248 (*CSC strictly_positive *)
249 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
250 and weakly_positive context n nn uri te =
251 let module C = Cic in
252 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
254 C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,[])
256 (*CSC mettere in cicSubstitution *)
257 let rec subst_inductive_type_with_dummy_mutind =
259 C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
261 | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
263 | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
264 | C.Prod (name,so,ta) ->
265 C.Prod (name, subst_inductive_type_with_dummy_mutind so,
266 subst_inductive_type_with_dummy_mutind ta)
267 | C.Lambda (name,so,ta) ->
268 C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
269 subst_inductive_type_with_dummy_mutind ta)
271 C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
272 | C.MutCase (uri,i,outtype,term,pl) ->
274 subst_inductive_type_with_dummy_mutind outtype,
275 subst_inductive_type_with_dummy_mutind term,
276 List.map subst_inductive_type_with_dummy_mutind pl)
278 C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
279 subst_inductive_type_with_dummy_mutind ty,
280 subst_inductive_type_with_dummy_mutind bo)) fl)
282 C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
283 subst_inductive_type_with_dummy_mutind ty,
284 subst_inductive_type_with_dummy_mutind bo)) fl)
285 | C.Const (uri,exp_named_subst) ->
286 let exp_named_subst' =
288 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
291 C.Const (uri,exp_named_subst')
292 | C.MutInd (uri,typeno,exp_named_subst) ->
293 let exp_named_subst' =
295 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
298 C.MutInd (uri,typeno,exp_named_subst')
299 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
300 let exp_named_subst' =
302 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
305 C.MutConstruct (uri,typeno,consno,exp_named_subst')
308 match CicReduction.whd context te with
309 C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
310 | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
311 | C.Prod (C.Anonymous,source,dest) ->
312 strictly_positive context n nn
313 (subst_inductive_type_with_dummy_mutind source) &&
314 weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
315 (n + 1) (nn + 1) uri dest
316 | C.Prod (name,source,dest) when
317 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
318 (* dummy abstraction, so we behave as in the anonimous case *)
319 strictly_positive context n nn
320 (subst_inductive_type_with_dummy_mutind source) &&
321 weakly_positive ((Some (name,(C.Decl source)))::context)
322 (n + 1) (nn + 1) uri dest
323 | C.Prod (name,source,dest) ->
324 does_not_occur context n nn
325 (subst_inductive_type_with_dummy_mutind source)&&
326 weakly_positive ((Some (name,(C.Decl source)))::context)
327 (n + 1) (nn + 1) uri dest
328 | _ -> raise (NotWellFormedTypeOfInductiveConstructor ("Guess where the error is ;-)"))
330 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
331 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
332 and instantiate_parameters params c =
333 let module C = Cic in
334 match (c,params) with
336 | (C.Prod (_,_,ta), he::tl) ->
337 instantiate_parameters tl
338 (CicSubstitution.subst he ta)
339 | (C.Cast (te,_), _) -> instantiate_parameters params te
340 | (t,l) -> raise (Impossible 1)
342 and strictly_positive context n nn te =
343 let module C = Cic in
344 let module U = UriManager in
345 match CicReduction.whd context te with
348 (*CSC: bisogna controllare ty????*)
349 strictly_positive context n nn te
350 | C.Prod (name,so,ta) ->
351 does_not_occur context n nn so &&
352 strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
353 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
354 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
355 | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
356 let (ok,paramsno,ity,cl,name) =
357 match CicEnvironment.get_obj uri with
358 C.InductiveDefinition (tl,_,paramsno) ->
359 let (name,_,ity,cl) = List.nth tl i in
360 (List.length tl = 1, paramsno, ity, cl, name)
361 | _ -> raise(WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
363 let (params,arguments) = split tl paramsno in
364 let lifted_params = List.map (CicSubstitution.lift 1) params in
368 instantiate_parameters lifted_params
369 (CicSubstitution.subst_vars exp_named_subst te)
374 (fun x i -> i && does_not_occur context n nn x)
376 (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
381 ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri x
383 | t -> does_not_occur context n nn t
385 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
386 and are_all_occurrences_positive context uri indparamsno i n nn te =
387 let module C = Cic in
388 match CicReduction.whd context te with
389 C.Appl ((C.Rel m)::tl) when m = i ->
390 (*CSC: riscrivere fermandosi a 0 *)
391 (* let's check if the inductive type is applied at least to *)
392 (* indparamsno parameters *)
398 match CicReduction.whd context x with
399 C.Rel m when m = n - (indparamsno - k) -> k - 1
400 | _ -> raise (WrongRequiredArgument (UriManager.string_of_uri uri))
404 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
406 raise (WrongRequiredArgument (UriManager.string_of_uri uri))
407 | C.Rel m when m = i ->
408 if indparamsno = 0 then
411 raise (WrongRequiredArgument (UriManager.string_of_uri uri))
412 | C.Prod (C.Anonymous,source,dest) ->
413 strictly_positive context n nn source &&
414 are_all_occurrences_positive
415 ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
416 (i+1) (n + 1) (nn + 1) dest
417 | C.Prod (name,source,dest) when
418 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
419 (* dummy abstraction, so we behave as in the anonimous case *)
420 strictly_positive context n nn source &&
421 are_all_occurrences_positive
422 ((Some (name,(C.Decl source)))::context) uri indparamsno
423 (i+1) (n + 1) (nn + 1) dest
424 | C.Prod (name,source,dest) ->
425 does_not_occur context n nn source &&
426 are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
427 uri indparamsno (i+1) (n + 1) (nn + 1) dest
428 | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri))
430 (* Main function to checks the correctness of a mutual *)
431 (* inductive block definition. *)
432 and check_mutual_inductive_defs uri =
433 let module U = UriManager in
435 Cic.InductiveDefinition (itl, _, indparamsno) ->
436 (* let's check if the arity of the inductive types are well *)
438 List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
440 (* let's check if the types of the inductive constructors *)
441 (* are well formed. *)
442 (* In order not to use type_of_aux we put the types of the *)
443 (* mutual inductive types at the head of the types of the *)
444 (* constructors using Prods *)
445 let len = List.length itl in
447 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
453 let debrujinedte = debrujin_constructor uri len te in
456 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
459 let _ = type_of augmented_term in
460 (* let's check also the positivity conditions *)
463 (are_all_occurrences_positive tys uri indparamsno i 0 len
466 raise (NotPositiveOccurrences (U.string_of_uri uri))
473 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
475 and type_of_mutual_inductive_defs uri i =
476 let module C = Cic in
477 let module R = CicReduction in
478 let module U = UriManager in
480 match CicEnvironment.is_type_checked ~trust:true uri with
481 CicEnvironment.CheckedObj cobj -> cobj
482 | CicEnvironment.UncheckedObj uobj ->
483 Logger.log (`Start_type_checking uri) ;
484 check_mutual_inductive_defs uri uobj ;
485 CicEnvironment.set_type_checking_info uri ;
486 Logger.log (`Type_checking_completed uri) ;
487 (match CicEnvironment.is_type_checked ~trust:false uri with
488 CicEnvironment.CheckedObj cobj -> cobj
489 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
493 C.InductiveDefinition (dl,_,_) ->
494 let (_,_,arity,_) = List.nth dl i in
496 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
498 and type_of_mutual_inductive_constr uri i j =
499 let module C = Cic in
500 let module R = CicReduction in
501 let module U = UriManager in
503 match CicEnvironment.is_type_checked ~trust:true uri with
504 CicEnvironment.CheckedObj cobj -> cobj
505 | CicEnvironment.UncheckedObj uobj ->
506 Logger.log (`Start_type_checking uri) ;
507 check_mutual_inductive_defs uri uobj ;
508 CicEnvironment.set_type_checking_info uri ;
509 Logger.log (`Type_checking_completed uri) ;
510 (match CicEnvironment.is_type_checked ~trust:false uri with
511 CicEnvironment.CheckedObj cobj -> cobj
512 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
516 C.InductiveDefinition (dl,_,_) ->
517 let (_,_,_,cl) = List.nth dl i in
518 let (_,ty) = List.nth cl (j-1) in
520 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
522 and recursive_args context n nn te =
523 let module C = Cic in
524 match CicReduction.whd context te with
530 | C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *)
531 | C.Prod (name,so,de) ->
532 (not (does_not_occur context n nn so)) ::
533 (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
535 | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *)
537 | C.Const _ -> raise (Impossible 5)
542 | C.CoFix _ -> raise (Impossible 6) (* due to type-checking *)
544 and get_new_safes context p c rl safes n nn x =
545 let module C = Cic in
546 let module U = UriManager in
547 let module R = CicReduction in
548 match (R.whd context c, R.whd context p, rl) with
549 (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
550 (* we are sure that the two sources are convertible because we *)
551 (* have just checked this. So let's go along ... *)
553 List.map (fun x -> x + 1) safes
556 if b then 1::safes' else safes'
558 get_new_safes ((Some (name,(C.Decl so)))::context)
559 ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
560 | (C.Prod _, (C.MutConstruct _ as e), _)
561 | (C.Prod _, (C.Rel _ as e), _)
562 | (C.MutInd _, e, [])
563 | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
565 (* CSC: If the next exception is raised, it just means that *)
566 (* CSC: the proof-assistant allows to use very strange things *)
567 (* CSC: as a branch of a case whose type is a Prod. In *)
568 (* CSC: particular, this means that a new (C.Prod, x,_) case *)
569 (* CSC: must be considered in this match. (e.g. x = MutCase) *)
572 and split_prods context n te =
573 let module C = Cic in
574 let module R = CicReduction in
575 match (n, R.whd context te) with
577 | (n, C.Prod (name,so,ta)) when n > 0 ->
578 split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta
579 | (_, _) -> raise (Impossible 8)
581 and eat_lambdas context n te =
582 let module C = Cic in
583 let module R = CicReduction in
584 match (n, R.whd context te) with
585 (0, _) -> (te, 0, context)
586 | (n, C.Lambda (name,so,ta)) when n > 0 ->
587 let (te, k, context') =
588 eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
590 (te, k + 1, context')
591 | (_, _) -> raise (Impossible 9)
593 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
594 and check_is_really_smaller_arg context n nn kl x safes te =
595 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
596 (*CSC: cfr guarded_by_destructors *)
597 let module C = Cic in
598 let module U = UriManager in
599 match CicReduction.whd context te with
600 C.Rel m when List.mem m safes -> true
607 (* | C.Cast (te,ty) ->
608 check_is_really_smaller_arg n nn kl x safes te &&
609 check_is_really_smaller_arg n nn kl x safes ty*)
610 (* | C.Prod (_,so,ta) ->
611 check_is_really_smaller_arg n nn kl x safes so &&
612 check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
613 (List.map (fun x -> x + 1) safes) ta*)
614 | C.Prod _ -> raise (Impossible 10)
615 | C.Lambda (name,so,ta) ->
616 check_is_really_smaller_arg context n nn kl x safes so &&
617 check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context)
618 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
619 | C.LetIn (name,so,ta) ->
620 check_is_really_smaller_arg context n nn kl x safes so &&
621 check_is_really_smaller_arg ((Some (name,(C.Def so)))::context)
622 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
624 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
625 (*CSC: solo perche' non abbiamo trovato controesempi *)
626 check_is_really_smaller_arg context n nn kl x safes he
627 | C.Appl [] -> raise (Impossible 11)
629 | C.MutInd _ -> raise (Impossible 12)
630 | C.MutConstruct _ -> false
631 | C.MutCase (uri,i,outtype,term,pl) ->
633 C.Rel m when List.mem m safes || m = x ->
634 let (tys,len,isinductive,paramsno,cl) =
635 match CicEnvironment.get_obj uri with
636 C.InductiveDefinition (tl,_,paramsno) ->
638 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
640 let (_,isinductive,_,cl) = List.nth tl i in
644 (id, snd (split_prods tys paramsno ty))) cl
646 (tys,List.length tl,isinductive,paramsno,cl')
648 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
650 if not isinductive then
653 i && check_is_really_smaller_arg context n nn kl x safes p)
659 let debrujinedte = debrujin_constructor uri len c in
660 recursive_args tys 0 len debrujinedte
662 let (e,safes',n',nn',x',context') =
663 get_new_safes context p c rl' safes n nn x
666 check_is_really_smaller_arg context' n' nn' kl x' safes' e
667 ) (List.combine pl cl) true
668 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
669 let (tys,len,isinductive,paramsno,cl) =
670 match CicEnvironment.get_obj uri with
671 C.InductiveDefinition (tl,_,paramsno) ->
672 let (_,isinductive,_,cl) = List.nth tl i in
674 List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
679 (id, snd (split_prods tys paramsno ty))) cl
681 (tys,List.length tl,isinductive,paramsno,cl')
683 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
685 if not isinductive then
688 i && check_is_really_smaller_arg context n nn kl x safes p)
691 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
692 (*CSC: sugli argomenti di una applicazione *)
696 let debrujinedte = debrujin_constructor uri len c in
697 recursive_args tys 0 len debrujinedte
699 let (e, safes',n',nn',x',context') =
700 get_new_safes context p c rl' safes n nn x
703 check_is_really_smaller_arg context' n' nn' kl x' safes' e
704 ) (List.combine pl cl) true
708 i && check_is_really_smaller_arg context n nn kl x safes p
712 let len = List.length fl in
713 let n_plus_len = n + len
714 and nn_plus_len = nn + len
715 and x_plus_len = x + len
716 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
717 and safes' = List.map (fun x -> x + len) safes in
719 (fun (_,_,ty,bo) i ->
721 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
725 let len = List.length fl in
726 let n_plus_len = n + len
727 and nn_plus_len = nn + len
728 and x_plus_len = x + len
729 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
730 and safes' = List.map (fun x -> x + len) safes in
734 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
738 and guarded_by_destructors context n nn kl x safes =
739 let module C = Cic in
740 let module U = UriManager in
742 C.Rel m when m > n && m <= nn -> false
744 (match List.nth context (n-1) with
745 Some (_,C.Decl _) -> true
746 | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo
747 | None -> raise RelToHiddenHypothesis
753 guarded_by_destructors context n nn kl x safes te &&
754 guarded_by_destructors context n nn kl x safes ty
755 | C.Prod (name,so,ta) ->
756 guarded_by_destructors context n nn kl x safes so &&
757 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
758 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
759 | C.Lambda (name,so,ta) ->
760 guarded_by_destructors context n nn kl x safes so &&
761 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
762 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
763 | C.LetIn (name,so,ta) ->
764 guarded_by_destructors context n nn kl x safes so &&
765 guarded_by_destructors ((Some (name,(C.Def so)))::context)
766 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
767 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
768 let k = List.nth kl (m - n - 1) in
769 if not (List.length tl > k) then false
773 i && guarded_by_destructors context n nn kl x safes param
775 check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
778 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
780 | C.Var (_,exp_named_subst)
781 | C.Const (_,exp_named_subst)
782 | C.MutInd (_,_,exp_named_subst)
783 | C.MutConstruct (_,_,_,exp_named_subst) ->
785 (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
787 | C.MutCase (uri,i,outtype,term,pl) ->
789 C.Rel m when List.mem m safes || m = x ->
790 let (tys,len,isinductive,paramsno,cl) =
791 match CicEnvironment.get_obj uri with
792 C.InductiveDefinition (tl,_,paramsno) ->
793 let (_,isinductive,_,cl) = List.nth tl i in
795 List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
800 (id, snd (split_prods tys paramsno ty))) cl
802 (tys,List.length tl,isinductive,paramsno,cl')
804 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
806 if not isinductive then
807 guarded_by_destructors context n nn kl x safes outtype &&
808 guarded_by_destructors context n nn kl x safes term &&
809 (*CSC: manca ??? il controllo sul tipo di term? *)
812 i && guarded_by_destructors context n nn kl x safes p)
815 guarded_by_destructors context n nn kl x safes outtype &&
816 (*CSC: manca ??? il controllo sul tipo di term? *)
820 let debrujinedte = debrujin_constructor uri len c in
821 recursive_args tys 0 len debrujinedte
823 let (e,safes',n',nn',x',context') =
824 get_new_safes context p c rl' safes n nn x
827 guarded_by_destructors context' n' nn' kl x' safes' e
828 ) (List.combine pl cl) true
829 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
830 let (tys,len,isinductive,paramsno,cl) =
831 match CicEnvironment.get_obj uri with
832 C.InductiveDefinition (tl,_,paramsno) ->
833 let (_,isinductive,_,cl) = List.nth tl i in
835 List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
840 (id, snd (split_prods tys paramsno ty))) cl
842 (tys,List.length tl,isinductive,paramsno,cl')
844 raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
846 if not isinductive then
847 guarded_by_destructors context n nn kl x safes outtype &&
848 guarded_by_destructors context n nn kl x safes term &&
849 (*CSC: manca ??? il controllo sul tipo di term? *)
852 i && guarded_by_destructors context n nn kl x safes p)
855 guarded_by_destructors context n nn kl x safes outtype &&
856 (*CSC: manca ??? il controllo sul tipo di term? *)
859 i && guarded_by_destructors context n nn kl x safes t)
864 let debrujinedte = debrujin_constructor uri len c in
865 recursive_args tys 0 len debrujinedte
867 let (e, safes',n',nn',x',context') =
868 get_new_safes context p c rl' safes n nn x
871 guarded_by_destructors context' n' nn' kl x' safes' e
872 ) (List.combine pl cl) true
874 guarded_by_destructors context n nn kl x safes outtype &&
875 guarded_by_destructors context n nn kl x safes term &&
876 (*CSC: manca ??? il controllo sul tipo di term? *)
878 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
882 let len = List.length fl in
883 let n_plus_len = n + len
884 and nn_plus_len = nn + len
885 and x_plus_len = x + len
886 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
887 and safes' = List.map (fun x -> x + len) safes in
889 (fun (_,_,ty,bo) i ->
890 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
891 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
895 let len = List.length fl in
896 let n_plus_len = n + len
897 and nn_plus_len = nn + len
898 and x_plus_len = x + len
899 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
900 and safes' = List.map (fun x -> x + len) safes in
904 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
905 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
909 (* the boolean h means already protected *)
910 (* args is the list of arguments the type of the constructor that may be *)
911 (* found in head position must be applied to. *)
912 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
913 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
914 let module C = Cic in
915 (*CSC: There is a lot of code replication between the cases X and *)
916 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
917 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
918 match CicReduction.whd context te with
919 C.Rel m when m > n && m <= nn -> h
927 raise (Impossible 17) (* the term has just been type-checked *)
928 | C.Lambda (name,so,de) ->
929 does_not_occur context n nn so &&
930 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
931 (n + 1) (nn + 1) h de args coInductiveTypeURI
932 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
934 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
935 | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
937 match CicEnvironment.get_cooked_obj ~trust:false uri with
938 C.InductiveDefinition (itl,_,_) ->
939 let (_,_,_,cl) = List.nth itl i in
940 let (_,cons) = List.nth cl (j - 1) in
941 CicSubstitution.subst_vars exp_named_subst cons
943 raise (WrongUriToMutualInductiveDefinitions
944 (UriManager.string_of_uri uri))
946 let rec analyse_branch context ty te =
947 match CicReduction.whd context ty with
948 C.Meta _ -> raise (Impossible 34)
952 does_not_occur context n nn te
954 | C.Cast _ -> raise (Impossible 24) (* due to type-checking *)
955 | C.Prod (name,so,de) ->
956 analyse_branch ((Some (name,(C.Decl so)))::context) de te
958 | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *)
959 | C.Appl ((C.MutInd (uri,_,_))::_) as ty
960 when uri == coInductiveTypeURI ->
961 guarded_by_constructors context n nn true te [] coInductiveTypeURI
962 | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
963 guarded_by_constructors context n nn true te tl coInductiveTypeURI
965 does_not_occur context n nn te
966 | C.Const _ -> raise (Impossible 26)
967 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
968 guarded_by_constructors context n nn true te [] coInductiveTypeURI
970 does_not_occur context n nn te
971 | C.MutConstruct _ -> raise (Impossible 27)
972 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
973 (*CSC: in head position. *)
976 | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *)
978 let rec analyse_instantiated_type context ty l =
979 match CicReduction.whd context ty with
985 | C.Cast _ -> raise (Impossible 29) (* due to type-checking *)
986 | C.Prod (name,so,de) ->
991 analyse_branch context so he &&
992 analyse_instantiated_type ((Some (name,(C.Decl so)))::context)
996 | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *)
999 (fun i x -> i && does_not_occur context n nn x) true l
1000 | C.Const _ -> raise (Impossible 31)
1003 (fun i x -> i && does_not_occur context n nn x) true l
1004 | C.MutConstruct _ -> raise (Impossible 32)
1005 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1006 (*CSC: in head position. *)
1009 | C.CoFix _ -> raise (Impossible 33) (* due to type-checking *)
1011 let rec instantiate_type args consty =
1014 | tlhe::tltl as l ->
1015 let consty' = CicReduction.whd context consty in
1021 let instantiated_de = CicSubstitution.subst he de in
1022 (*CSC: siamo sicuri che non sia troppo forte? *)
1023 does_not_occur context n nn tlhe &
1024 instantiate_type tl instantiated_de tltl
1026 (*CSC:We do not consider backbones with a MutCase, a *)
1027 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1028 raise (Impossible 23)
1030 | [] -> analyse_instantiated_type context consty' l
1031 (* These are all the other cases *)
1033 instantiate_type args consty tl
1034 | C.Appl ((C.CoFix (_,fl))::tl) ->
1035 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1036 let len = List.length fl in
1037 let n_plus_len = n + len
1038 and nn_plus_len = nn + len
1039 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1040 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1043 i && does_not_occur context n nn ty &&
1044 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1045 args coInductiveTypeURI
1047 | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1048 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1049 does_not_occur context n nn out &&
1050 does_not_occur context n nn te &&
1054 guarded_by_constructors context n nn h x args coInductiveTypeURI
1057 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1058 | C.Var (_,exp_named_subst)
1059 | C.Const (_,exp_named_subst) ->
1061 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1062 | C.MutInd _ -> assert false
1063 | C.MutConstruct (_,_,_,exp_named_subst) ->
1065 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1066 | C.MutCase (_,_,out,te,pl) ->
1067 does_not_occur context n nn out &&
1068 does_not_occur context n nn te &&
1072 guarded_by_constructors context n nn h x args coInductiveTypeURI
1075 let len = List.length fl in
1076 let n_plus_len = n + len
1077 and nn_plus_len = nn + len
1078 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1079 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1081 (fun (_,_,ty,bo) i ->
1082 i && does_not_occur context n nn ty &&
1083 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1086 let len = List.length fl in
1087 let n_plus_len = n + len
1088 and nn_plus_len = nn + len
1089 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1090 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1093 i && does_not_occur context n nn ty &&
1094 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1095 args coInductiveTypeURI
1098 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1099 let module C = Cic in
1100 let module U = UriManager in
1101 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1102 (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1103 when CicReduction.are_convertible context so1 so2 ->
1104 check_allowed_sort_elimination context uri i need_dummy
1105 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1106 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1107 | (C.Sort C.Prop, C.Sort C.Set)
1108 | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
1109 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1110 (match CicEnvironment.get_obj uri with
1111 C.InductiveDefinition (itl,_,_) ->
1112 let (_,_,_,cl) = List.nth itl i in
1113 (* is a singleton definition or the empty proposition? *)
1114 List.length cl = 1 || List.length cl = 0
1116 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1118 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1119 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1120 | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
1121 (match CicEnvironment.get_obj uri with
1122 C.InductiveDefinition (itl,_,paramsno) ->
1124 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1126 let (_,_,_,cl) = List.nth itl i in
1128 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1130 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1132 | (C.Sort C.Type, C.Sort _) when need_dummy -> true
1133 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1134 let res = CicReduction.are_convertible context so ind
1137 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1138 C.Sort C.Prop -> true
1140 (match CicEnvironment.get_obj uri with
1141 C.InductiveDefinition (itl,_,_) ->
1142 let (_,_,_,cl) = List.nth itl i in
1143 (* is a singleton definition? *)
1146 raise (WrongUriToMutualInductiveDefinitions
1147 (U.string_of_uri uri))
1151 | (C.Sort C.Set, C.Prod (name,so,ta)) when not need_dummy ->
1152 let res = CicReduction.are_convertible context so ind
1155 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1157 | C.Sort C.Set -> true
1159 (match CicEnvironment.get_obj uri with
1160 C.InductiveDefinition (itl,_,paramsno) ->
1161 let (_,_,_,cl) = List.nth itl i in
1164 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1167 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1169 raise (WrongUriToMutualInductiveDefinitions
1170 (U.string_of_uri uri))
1172 | _ -> raise (Impossible 19)
1174 | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
1175 CicReduction.are_convertible context so ind
1178 and type_of_branch context argsno need_dummy outtype term constype =
1179 let module C = Cic in
1180 let module R = CicReduction in
1181 match R.whd context constype with
1186 C.Appl [outtype ; term]
1187 | C.Appl (C.MutInd (_,_,_)::tl) ->
1188 let (_,arguments) = split tl argsno
1190 if need_dummy && arguments = [] then
1193 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1194 | C.Prod (name,so,de) ->
1196 match CicSubstitution.lift 1 term with
1197 C.Appl l -> C.Appl (l@[C.Rel 1])
1198 | t -> C.Appl [t ; C.Rel 1]
1200 C.Prod (C.Anonymous,so,type_of_branch
1201 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1202 (CicSubstitution.lift 1 outtype) term' de)
1203 | _ -> raise (Impossible 20)
1205 (* check_metasenv_consistency checks that the "canonical" context of a
1206 metavariable is consitent - up to relocation via the relocation list l -
1207 with the actual context *)
1209 and check_metasenv_consistency metasenv context canonical_context l =
1210 let module C = Cic in
1211 let module R = CicReduction in
1212 let module S = CicSubstitution in
1213 let lifted_canonical_context =
1217 | (Some (n,C.Decl t))::tl ->
1218 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1219 | (Some (n,C.Def t))::tl ->
1220 (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1221 | None::tl -> None::(aux (i+1) tl)
1223 aux 1 canonical_context
1230 | Some t,Some (_,C.Def ct) ->
1231 R.are_convertible context t ct
1232 | Some t,Some (_,C.Decl ct) ->
1233 R.are_convertible context (type_of_aux' metasenv context t) ct
1236 if not res then raise MetasenvInconsistency
1237 ) l lifted_canonical_context
1239 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1240 and type_of_aux' metasenv context t =
1241 let rec type_of_aux context =
1242 let module C = Cic in
1243 let module R = CicReduction in
1244 let module S = CicSubstitution in
1245 let module U = UriManager in
1249 match List.nth context (n - 1) with
1250 Some (_,C.Decl t) -> S.lift n t
1251 | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
1252 | None -> raise RelToHiddenHypothesis
1254 _ -> raise (NotWellTyped "Not a close term")
1256 | C.Var (uri,exp_named_subst) ->
1258 check_exp_named_subst context exp_named_subst ;
1260 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1265 let (_,canonical_context,ty) =
1266 List.find (function (m,_,_) -> n = m) metasenv
1268 check_metasenv_consistency metasenv context canonical_context l;
1269 CicSubstitution.lift_meta l ty
1270 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1271 | C.Implicit -> raise (Impossible 21)
1273 let _ = type_of_aux context ty in
1274 if R.are_convertible context (type_of_aux context te) ty then ty
1275 else raise (NotWellTyped "Cast")
1276 | C.Prod (name,s,t) ->
1277 let sort1 = type_of_aux context s
1278 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1279 sort_of_prod context (name,s) (sort1,sort2)
1280 | C.Lambda (n,s,t) ->
1281 let sort1 = type_of_aux context s
1282 and type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1283 let sort2 = type_of_aux ((Some (n,(C.Decl s)))::context) type2 in
1284 (* only to check if the product is well-typed *)
1285 let _ = sort_of_prod context (n,s) (sort1,sort2) in
1287 | C.LetIn (n,s,t) ->
1288 (* only to check if s is well-typed *)
1289 let _ = type_of_aux context s in
1290 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1291 LetIn is later reduced and maybe also re-checked.
1292 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1294 (* The type of the LetIn is reduced. Much faster than the previous
1295 solution. Moreover the inferred type is probably very different
1296 from the expected one.
1297 (CicReduction.whd context
1298 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1300 (* One-step LetIn reduction. Even faster than the previous solution.
1301 Moreover the inferred type is closer to the expected one. *)
1302 (CicSubstitution.subst s
1303 (type_of_aux ((Some (n,(C.Def s)))::context) t))
1304 | C.Appl (he::tl) when List.length tl > 0 ->
1305 let hetype = type_of_aux context he
1306 and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1307 eat_prods context hetype tlbody_and_type
1308 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
1309 | C.Const (uri,exp_named_subst) ->
1311 check_exp_named_subst context exp_named_subst ;
1313 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1317 | C.MutInd (uri,i,exp_named_subst) ->
1319 check_exp_named_subst context exp_named_subst ;
1321 CicSubstitution.subst_vars exp_named_subst
1322 (type_of_mutual_inductive_defs uri i)
1326 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1327 check_exp_named_subst context exp_named_subst ;
1329 CicSubstitution.subst_vars exp_named_subst
1330 (type_of_mutual_inductive_constr uri i j)
1333 | C.MutCase (uri,i,outtype,term,pl) ->
1334 let outsort = type_of_aux context outtype in
1335 let (need_dummy, k) =
1336 let rec guess_args context t =
1337 match CicReduction.whd context t with
1338 C.Sort _ -> (true, 0)
1339 | C.Prod (name, s, t) ->
1340 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1342 (* last prod before sort *)
1343 match CicReduction.whd context s with
1344 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1345 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1347 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1348 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1349 when U.eq uri' uri && i' = i -> (false, 1)
1353 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
1355 (*CSC whd non serve dopo type_of_aux ? *)
1356 let (b, k) = guess_args context outsort in
1357 if not b then (b, k - 1) else (b, k)
1359 let (parameters, arguments, exp_named_subst) =
1360 match R.whd context (type_of_aux context term) with
1361 (*CSC manca il caso dei CAST *)
1362 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1363 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
1364 (*CSC: Hint: nella DTD servono per gli stylesheet. *)
1365 C.MutInd (uri',i',exp_named_subst) as typ ->
1366 if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1367 else raise (NotWellTyped ("MutCase: the term is of type " ^
1369 " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^
1370 string_of_int i ^ "{_}"))
1371 | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
1372 if U.eq uri uri' && i = i' then
1374 split tl (List.length tl - k)
1375 in params,args,exp_named_subst
1376 else raise (NotWellTyped ("MutCase: the term is of type " ^
1378 " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^
1379 string_of_int i ^ "{_}"))
1380 | _ -> raise (NotWellTyped "MutCase: the term is not an inductive one")
1382 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1383 let sort_of_ind_type =
1384 if parameters = [] then
1385 C.MutInd (uri,i,exp_named_subst)
1387 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1389 if not (check_allowed_sort_elimination context uri i need_dummy
1390 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1392 raise (NotWellTyped "MutCase: not allowed sort elimination") ;
1394 (* let's check if the type of branches are right *)
1396 match CicEnvironment.get_cooked_obj ~trust:false uri with
1397 C.InductiveDefinition (_,_,parsno) -> parsno
1399 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1401 let (_,branches_ok) =
1405 if parameters = [] then
1406 (C.MutConstruct (uri,i,j,exp_named_subst))
1408 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1415 R.are_convertible context (type_of_aux context p)
1416 (type_of_branch context parsno need_dummy outtype cons
1417 (type_of_aux context cons))
1418 in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res
1422 if not branches_ok then
1423 raise (NotWellTyped "MutCase: wrong type of a branch") ;
1425 if not need_dummy then
1426 C.Appl ((outtype::arguments)@[term])
1427 else if arguments = [] then
1430 C.Appl (outtype::arguments)
1432 let types_times_kl =
1436 let _ = type_of_aux context ty in
1437 (Some (C.Name n,(C.Decl ty)),k)) fl)
1439 let (types,kl) = List.split types_times_kl in
1440 let len = List.length types in
1442 (fun (name,x,ty,bo) ->
1444 (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1445 (CicSubstitution.lift len ty))
1448 let (m, eaten, context') =
1449 eat_lambdas (types @ context) (x + 1) bo
1451 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1454 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1456 raise (NotWellTyped "Fix: not guarded by destructors")
1459 raise (NotWellTyped "Fix: ill-typed bodies")
1462 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1463 let (_,_,ty,_) = List.nth fl i in
1470 let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1472 let len = List.length types in
1476 (R.are_convertible (types @ context)
1477 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1480 (* let's control that the returned type is coinductive *)
1481 match returns_a_coinductive context ty with
1483 raise(NotWellTyped "CoFix: does not return a coinductive type")
1485 (*let's control the guarded by constructors conditions C{f,M}*)
1488 (guarded_by_constructors (types @ context) 0 len false bo
1491 raise (NotWellTyped "CoFix: not guarded by constructors")
1494 raise (NotWellTyped "CoFix: ill-typed bodies")
1497 let (_,ty,_) = List.nth fl i in
1500 and check_exp_named_subst context =
1501 let rec check_exp_named_subst_aux substs =
1504 | ((uri,t) as subst)::tl ->
1506 CicSubstitution.subst_vars substs (type_of_variable uri) in
1507 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1508 Cic.Variable (_,Some bo,_,_) ->
1511 "A variable with a body can not be explicit substituted")
1512 | Cic.Variable (_,None,_,_) -> ()
1513 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
1515 let typeoft = type_of_aux context t in
1516 if CicReduction.are_convertible context typeoft typeofvar then
1517 check_exp_named_subst_aux (substs@[subst]) tl
1520 CicReduction.fdebug := 0 ;
1521 ignore (CicReduction.are_convertible context typeoft typeofvar) ;
1523 debug typeoft [typeofvar] ;
1524 raise (NotWellTyped "Wrong Explicit Named Substitution")
1527 check_exp_named_subst_aux []
1529 and sort_of_prod context (name,s) (t1, t2) =
1530 let module C = Cic in
1531 let t1' = CicReduction.whd context t1 in
1532 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1533 match (t1', t2') with
1534 (C.Sort s1, C.Sort s2)
1535 when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
1537 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1541 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
1543 and eat_prods context hetype =
1544 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1548 | (hete, hety)::tl ->
1549 (match (CicReduction.whd context hetype) with
1551 if CicReduction.are_convertible context s hety then
1552 (CicReduction.fdebug := -1 ;
1553 eat_prods context (CicSubstitution.subst hete t) tl
1557 CicReduction.fdebug := 0 ;
1558 ignore (CicReduction.are_convertible context s hety) ;
1561 raise (NotWellTyped "Appl: wrong parameter-type")
1563 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
1566 and returns_a_coinductive context ty =
1567 let module C = Cic in
1568 match CicReduction.whd context ty with
1569 C.MutInd (uri,i,_) ->
1570 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1571 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1572 C.InductiveDefinition (itl,_,_) ->
1573 let (_,is_inductive,_,_) = List.nth itl i in
1574 if is_inductive then None else (Some uri)
1576 raise (WrongUriToMutualInductiveDefinitions
1577 (UriManager.string_of_uri uri))
1579 | C.Appl ((C.MutInd (uri,i,_))::_) ->
1580 (match CicEnvironment.get_obj uri with
1581 C.InductiveDefinition (itl,_,_) ->
1582 let (_,is_inductive,_,_) = List.nth itl i in
1583 if is_inductive then None else (Some uri)
1585 raise (WrongUriToMutualInductiveDefinitions
1586 (UriManager.string_of_uri uri))
1588 | C.Prod (n,so,de) ->
1589 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1594 prerr_endline ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1597 type_of_aux context t
1599 in prerr_endline "FINE TYPE_OF_AUX" ; flush stderr ; res
1602 (* is a small constructor? *)
1603 (*CSC: ottimizzare calcolando staticamente *)
1604 and is_small context paramsno c =
1605 let rec is_small_aux context c =
1606 let module C = Cic in
1607 match CicReduction.whd context c with
1609 (*CSC: [] is an empty metasenv. Is it correct? *)
1610 let s = type_of_aux' [] context so in
1611 (s = C.Sort C.Prop || s = C.Sort C.Set) &&
1612 is_small_aux ((Some (n,(C.Decl so)))::context) de
1613 | _ -> true (*CSC: we trust the type-checker *)
1615 let (context',dx) = split_prods context paramsno c in
1616 is_small_aux context' dx
1620 prerr_endline ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1623 type_of_aux' [] [] t
1625 in prerr_endline "FINE TYPE_OF_AUX'" ; flush stderr ; res
1630 let module C = Cic in
1631 let module R = CicReduction in
1632 let module U = UriManager in
1633 match CicEnvironment.is_type_checked ~trust:false uri with
1634 CicEnvironment.CheckedObj _ -> ()
1635 | CicEnvironment.UncheckedObj uobj ->
1636 (* let's typecheck the uncooked object *)
1637 Logger.log (`Start_type_checking uri) ;
1639 C.Constant (_,Some te,ty,_) ->
1640 let _ = type_of ty in
1641 if not (R.are_convertible [] (type_of te ) ty) then
1642 raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
1643 | C.Constant (_,None,ty,_) ->
1644 (* only to check that ty is well-typed *)
1645 let _ = type_of ty in ()
1646 | C.CurrentProof (_,conjs,te,ty,_) ->
1647 (*CSC: bisogna controllare anche il metasenv!!! *)
1648 let _ = type_of_aux' conjs [] ty in
1649 debug (type_of_aux' conjs [] te) [] ;
1650 if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then
1651 raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
1652 | C.Variable (_,bo,ty,_) ->
1653 (* only to check that ty is well-typed *)
1654 let _ = type_of ty in
1658 if not (R.are_convertible [] (type_of bo) ty) then
1659 raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri)))
1661 | C.InductiveDefinition _ ->
1662 check_mutual_inductive_defs uri uobj
1664 CicEnvironment.set_type_checking_info uri ;
1665 Logger.log (`Type_checking_completed uri)