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 (* TODO factorize functions to frequent errors (e.g. "Unknwon mutual inductive
31 exception AssertFailure of string;;
32 exception TypeCheckerFailure of string;;
36 let rec debug_aux t i =
38 let module U = UriManager in
39 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
42 raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
45 let debug_print = prerr_endline ;;
50 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
52 raise (TypeCheckerFailure "Parameters number < left parameters number")
55 let debrujin_constructor uri number_of_types =
59 C.Rel n as t when n <= k -> t
61 raise (TypeCheckerFailure "unbound variable found in constructor type")
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
82 raise (TypeCheckerFailure
83 ("non-empty explicit named substitution is applied to "^
84 "a mutual inductive type which is being defined")) ;
85 C.Rel (k + number_of_types - tyno) ;
86 | C.MutInd (uri',tyno,exp_named_subst) ->
87 let exp_named_subst' =
88 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
90 C.MutInd (uri',tyno,exp_named_subst')
91 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
92 let exp_named_subst' =
93 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
95 C.MutConstruct (uri,tyno,consno,exp_named_subst')
96 | C.MutCase (sp,i,outty,t,pl) ->
97 C.MutCase (sp, i, aux k outty, aux k t,
100 let len = List.length fl in
103 (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
108 let len = List.length fl in
111 (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
114 C.CoFix (i, liftedfl)
119 exception CicEnvironmentError;;
121 let rec type_of_constant uri =
122 let module C = Cic in
123 let module R = CicReduction in
124 let module U = UriManager in
126 match CicEnvironment.is_type_checked ~trust:true uri with
127 CicEnvironment.CheckedObj cobj -> cobj
128 | CicEnvironment.UncheckedObj uobj ->
129 CicLogger.log (`Start_type_checking uri) ;
130 CicUniv.directly_to_env_begin ();
131 (* let's typecheck the uncooked obj *)
133 C.Constant (_,Some te,ty,_) ->
134 let _ = type_of ty in
135 let type_of_te = type_of te in
136 if not (R.are_convertible [] type_of_te ty) then
137 raise (TypeCheckerFailure (sprintf
138 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
139 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
141 | C.Constant (_,None,ty,_) ->
142 (* only to check that ty is well-typed *)
143 let _ = type_of ty in ()
144 | C.CurrentProof (_,conjs,te,ty,_) ->
147 (fun metasenv ((_,context,ty) as conj) ->
148 ignore (type_of_aux' metasenv context ty) ;
152 let _ = type_of_aux' conjs [] ty in
153 let type_of_te = type_of_aux' conjs [] te in
154 if not (R.are_convertible [] type_of_te ty) then
155 raise (TypeCheckerFailure (sprintf
156 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
157 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
160 raise (TypeCheckerFailure
161 ("Unknown constant:" ^ U.string_of_uri uri))
163 CicEnvironment.set_type_checking_info uri ;
164 CicUniv.directly_to_env_end ();
165 CicLogger.log (`Type_checking_completed uri) ;
166 match CicEnvironment.is_type_checked ~trust:false uri with
167 CicEnvironment.CheckedObj cobj -> cobj
168 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
171 C.Constant (_,_,ty,_) -> ty
172 | C.CurrentProof (_,_,_,ty,_) -> ty
174 raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
176 and type_of_variable uri =
177 let module C = Cic in
178 let module R = CicReduction in
179 let module U = UriManager in
180 (* 0 because a variable is never cooked => no partial cooking at one level *)
181 match CicEnvironment.is_type_checked ~trust:true uri with
182 CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
183 | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
184 CicLogger.log (`Start_type_checking uri) ;
185 CicUniv.directly_to_env_begin ();
186 (* only to check that ty is well-typed *)
187 let _ = type_of ty in
191 if not (R.are_convertible [] (type_of bo) ty) then
192 raise (TypeCheckerFailure
193 ("Unknown variable:" ^ U.string_of_uri uri))
195 CicEnvironment.set_type_checking_info uri ;
196 CicUniv.directly_to_env_end ();
197 CicLogger.log (`Type_checking_completed uri) ;
200 raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
202 and does_not_occur context n nn te =
203 let module C = Cic in
204 (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
205 (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
207 match CicReduction.whd context te with
208 C.Rel m when m > n && m <= nn -> false
210 | C.Meta _ (* CSC: Are we sure? No recursion?*)
212 | C.Implicit _ -> true
214 does_not_occur context n nn te && does_not_occur context n nn ty
215 | C.Prod (name,so,dest) ->
216 does_not_occur context n nn so &&
217 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
219 | C.Lambda (name,so,dest) ->
220 does_not_occur context n nn so &&
221 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
223 | C.LetIn (name,so,dest) ->
224 does_not_occur context n nn so &&
225 does_not_occur ((Some (name,(C.Def (so,None))))::context)
226 (n + 1) (nn + 1) dest
228 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
229 | C.Var (_,exp_named_subst)
230 | C.Const (_,exp_named_subst)
231 | C.MutInd (_,_,exp_named_subst)
232 | C.MutConstruct (_,_,_,exp_named_subst) ->
233 List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
235 | C.MutCase (_,_,out,te,pl) ->
236 does_not_occur context n nn out && does_not_occur context n nn te &&
237 List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
239 let len = List.length fl in
240 let n_plus_len = n + len in
241 let nn_plus_len = nn + len in
243 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
246 (fun (_,_,ty,bo) i ->
247 i && does_not_occur context n nn ty &&
248 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
251 let len = List.length fl in
252 let n_plus_len = n + len in
253 let nn_plus_len = nn + len in
255 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
259 i && does_not_occur context n nn ty &&
260 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
263 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
264 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
265 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
266 (*CSC strictly_positive *)
267 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
268 and weakly_positive context n nn uri te =
269 let module C = Cic in
270 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
272 C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
274 (*CSC mettere in cicSubstitution *)
275 let rec subst_inductive_type_with_dummy_mutind =
277 C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
279 | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
281 | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
282 | C.Prod (name,so,ta) ->
283 C.Prod (name, subst_inductive_type_with_dummy_mutind so,
284 subst_inductive_type_with_dummy_mutind ta)
285 | C.Lambda (name,so,ta) ->
286 C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
287 subst_inductive_type_with_dummy_mutind ta)
289 C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
290 | C.MutCase (uri,i,outtype,term,pl) ->
292 subst_inductive_type_with_dummy_mutind outtype,
293 subst_inductive_type_with_dummy_mutind term,
294 List.map subst_inductive_type_with_dummy_mutind pl)
296 C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
297 subst_inductive_type_with_dummy_mutind ty,
298 subst_inductive_type_with_dummy_mutind bo)) fl)
300 C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
301 subst_inductive_type_with_dummy_mutind ty,
302 subst_inductive_type_with_dummy_mutind bo)) fl)
303 | C.Const (uri,exp_named_subst) ->
304 let exp_named_subst' =
306 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
309 C.Const (uri,exp_named_subst')
310 | C.MutInd (uri,typeno,exp_named_subst) ->
311 let exp_named_subst' =
313 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
316 C.MutInd (uri,typeno,exp_named_subst')
317 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
318 let exp_named_subst' =
320 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
323 C.MutConstruct (uri,typeno,consno,exp_named_subst')
326 match CicReduction.whd context te with
327 C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
328 | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
329 | C.Prod (C.Anonymous,source,dest) ->
330 strictly_positive context n nn
331 (subst_inductive_type_with_dummy_mutind source) &&
332 weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
333 (n + 1) (nn + 1) uri dest
334 | C.Prod (name,source,dest) when
335 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
336 (* dummy abstraction, so we behave as in the anonimous case *)
337 strictly_positive context n nn
338 (subst_inductive_type_with_dummy_mutind source) &&
339 weakly_positive ((Some (name,(C.Decl source)))::context)
340 (n + 1) (nn + 1) uri dest
341 | C.Prod (name,source,dest) ->
342 does_not_occur context n nn
343 (subst_inductive_type_with_dummy_mutind source)&&
344 weakly_positive ((Some (name,(C.Decl source)))::context)
345 (n + 1) (nn + 1) uri dest
347 raise (TypeCheckerFailure "Malformed inductive constructor type")
349 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
350 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
351 and instantiate_parameters params c =
352 let module C = Cic in
353 match (c,params) with
355 | (C.Prod (_,_,ta), he::tl) ->
356 instantiate_parameters tl
357 (CicSubstitution.subst he ta)
358 | (C.Cast (te,_), _) -> instantiate_parameters params te
359 | (t,l) -> raise (AssertFailure "1")
361 and strictly_positive context n nn te =
362 let module C = Cic in
363 let module U = UriManager in
364 match CicReduction.whd context te with
367 (*CSC: bisogna controllare ty????*)
368 strictly_positive context n nn te
369 | C.Prod (name,so,ta) ->
370 does_not_occur context n nn so &&
371 strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
372 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
373 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
374 | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
375 let (ok,paramsno,ity,cl,name) =
376 match CicEnvironment.get_obj uri with
377 C.InductiveDefinition (tl,_,paramsno) ->
378 let (name,_,ity,cl) = List.nth tl i in
379 (List.length tl = 1, paramsno, ity, cl, name)
381 raise (TypeCheckerFailure
382 ("Unknown inductive type:" ^ U.string_of_uri uri))
384 let (params,arguments) = split tl paramsno in
385 let lifted_params = List.map (CicSubstitution.lift 1) params in
389 instantiate_parameters lifted_params
390 (CicSubstitution.subst_vars exp_named_subst te)
395 (fun x i -> i && does_not_occur context n nn x)
397 (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
402 ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
405 | t -> does_not_occur context n nn t
407 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
408 and are_all_occurrences_positive context uri indparamsno i n nn te =
409 let module C = Cic in
410 match CicReduction.whd context te with
411 C.Appl ((C.Rel m)::tl) when m = i ->
412 (*CSC: riscrivere fermandosi a 0 *)
413 (* let's check if the inductive type is applied at least to *)
414 (* indparamsno parameters *)
420 match CicReduction.whd context x with
421 C.Rel m when m = n - (indparamsno - k) -> k - 1
423 raise (TypeCheckerFailure
424 ("Non-positive occurence in mutual inductive definition(s) " ^
425 UriManager.string_of_uri uri))
429 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
431 raise (TypeCheckerFailure
432 ("Non-positive occurence in mutual inductive definition(s) " ^
433 UriManager.string_of_uri uri))
434 | C.Rel m when m = i ->
435 if indparamsno = 0 then
438 raise (TypeCheckerFailure
439 ("Non-positive occurence in mutual inductive definition(s) " ^
440 UriManager.string_of_uri uri))
441 | C.Prod (C.Anonymous,source,dest) ->
442 strictly_positive context n nn source &&
443 are_all_occurrences_positive
444 ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
445 (i+1) (n + 1) (nn + 1) dest
446 | C.Prod (name,source,dest) when
447 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
448 (* dummy abstraction, so we behave as in the anonimous case *)
449 strictly_positive context n nn source &&
450 are_all_occurrences_positive
451 ((Some (name,(C.Decl source)))::context) uri indparamsno
452 (i+1) (n + 1) (nn + 1) dest
453 | C.Prod (name,source,dest) ->
454 does_not_occur context n nn source &&
455 are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
456 uri indparamsno (i+1) (n + 1) (nn + 1) dest
459 (TypeCheckerFailure ("Malformed inductive constructor type " ^
460 (UriManager.string_of_uri uri)))
462 (* Main function to checks the correctness of a mutual *)
463 (* inductive block definition. This is the function *)
464 (* exported to the proof-engine. *)
465 and typecheck_mutual_inductive_defs uri (itl,_,indparamsno) =
466 let module U = UriManager in
467 (* let's check if the arity of the inductive types are well *)
469 List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
471 (* let's check if the types of the inductive constructors *)
472 (* are well formed. *)
473 (* In order not to use type_of_aux we put the types of the *)
474 (* mutual inductive types at the head of the types of the *)
475 (* constructors using Prods *)
476 let len = List.length itl in
478 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
484 let debrujinedte = debrujin_constructor uri len te in
487 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
490 let _ = type_of augmented_term in
491 (* let's check also the positivity conditions *)
494 (are_all_occurrences_positive tys uri indparamsno i 0 len
498 (TypeCheckerFailure ("Non positive occurence in " ^
499 U.string_of_uri uri))
506 (* Main function to checks the correctness of a mutual *)
507 (* inductive block definition. *)
508 and check_mutual_inductive_defs uri =
510 Cic.InductiveDefinition (itl, params, indparamsno) ->
511 typecheck_mutual_inductive_defs uri (itl,params,indparamsno)
513 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
514 UriManager.string_of_uri uri))
516 and type_of_mutual_inductive_defs uri i =
517 let module C = Cic in
518 let module R = CicReduction in
519 let module U = UriManager in
521 match CicEnvironment.is_type_checked ~trust:true uri with
522 CicEnvironment.CheckedObj cobj -> cobj
523 | CicEnvironment.UncheckedObj uobj ->
524 CicLogger.log (`Start_type_checking uri) ;
525 CicUniv.directly_to_env_begin ();
526 check_mutual_inductive_defs uri uobj ;
527 CicEnvironment.set_type_checking_info uri ;
528 CicUniv.directly_to_env_end ();
529 CicLogger.log (`Type_checking_completed uri) ;
530 (match CicEnvironment.is_type_checked ~trust:false uri with
531 CicEnvironment.CheckedObj cobj -> cobj
532 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
536 C.InductiveDefinition (dl,_,_) ->
537 let (_,_,arity,_) = List.nth dl i in
540 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
541 U.string_of_uri uri))
543 and type_of_mutual_inductive_constr uri i j =
544 let module C = Cic in
545 let module R = CicReduction in
546 let module U = UriManager in
548 match CicEnvironment.is_type_checked ~trust:true uri with
549 CicEnvironment.CheckedObj cobj -> cobj
550 | CicEnvironment.UncheckedObj uobj ->
551 CicLogger.log (`Start_type_checking uri) ;
552 (*CicUniv.directly_to_env_begin ();*)
553 check_mutual_inductive_defs uri uobj ;
554 CicEnvironment.set_type_checking_info uri ;
555 (*CicUniv.directly_to_env_end ();*)
556 CicLogger.log (`Type_checking_completed uri) ;
557 (match CicEnvironment.is_type_checked ~trust:false uri with
558 CicEnvironment.CheckedObj cobj -> cobj
559 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
563 C.InductiveDefinition (dl,_,_) ->
564 let (_,_,_,cl) = List.nth dl i in
565 let (_,ty) = List.nth cl (j-1) in
568 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
569 UriManager.string_of_uri uri))
571 and recursive_args context n nn te =
572 let module C = Cic in
573 match CicReduction.whd context te with
579 | C.Cast _ (*CSC ??? *) ->
580 raise (AssertFailure "3") (* due to type-checking *)
581 | C.Prod (name,so,de) ->
582 (not (does_not_occur context n nn so)) ::
583 (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
586 raise (AssertFailure "4") (* due to type-checking *)
588 | C.Const _ -> raise (AssertFailure "5")
593 | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *)
595 and get_new_safes context p c rl safes n nn x =
596 let module C = Cic in
597 let module U = UriManager in
598 let module R = CicReduction in
599 match (R.whd context c, R.whd context p, rl) with
600 (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
601 (* we are sure that the two sources are convertible because we *)
602 (* have just checked this. So let's go along ... *)
604 List.map (fun x -> x + 1) safes
607 if b then 1::safes' else safes'
609 get_new_safes ((Some (name,(C.Decl so)))::context)
610 ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
611 | (C.Prod _, (C.MutConstruct _ as e), _)
612 | (C.Prod _, (C.Rel _ as e), _)
613 | (C.MutInd _, e, [])
614 | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
616 (* CSC: If the next exception is raised, it just means that *)
617 (* CSC: the proof-assistant allows to use very strange things *)
618 (* CSC: as a branch of a case whose type is a Prod. In *)
619 (* CSC: particular, this means that a new (C.Prod, x,_) case *)
620 (* CSC: must be considered in this match. (e.g. x = MutCase) *)
623 (Printf.sprintf "Get New Safes: c=%s ; p=%s"
624 (CicPp.ppterm c) (CicPp.ppterm p)))
626 and split_prods context n te =
627 let module C = Cic in
628 let module R = CicReduction in
629 match (n, R.whd context te) with
631 | (n, C.Prod (name,so,ta)) when n > 0 ->
632 split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta
633 | (_, _) -> raise (AssertFailure "8")
635 and eat_lambdas context n te =
636 let module C = Cic in
637 let module R = CicReduction in
638 match (n, R.whd context te) with
639 (0, _) -> (te, 0, context)
640 | (n, C.Lambda (name,so,ta)) when n > 0 ->
641 let (te, k, context') =
642 eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
644 (te, k + 1, context')
646 raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
648 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
649 and check_is_really_smaller_arg context n nn kl x safes te =
650 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
651 (*CSC: cfr guarded_by_destructors *)
652 let module C = Cic in
653 let module U = UriManager in
654 match CicReduction.whd context te with
655 C.Rel m when List.mem m safes -> true
662 (* | C.Cast (te,ty) ->
663 check_is_really_smaller_arg n nn kl x safes te &&
664 check_is_really_smaller_arg n nn kl x safes ty*)
665 (* | C.Prod (_,so,ta) ->
666 check_is_really_smaller_arg n nn kl x safes so &&
667 check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
668 (List.map (fun x -> x + 1) safes) ta*)
669 | C.Prod _ -> raise (AssertFailure "10")
670 | C.Lambda (name,so,ta) ->
671 check_is_really_smaller_arg context n nn kl x safes so &&
672 check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context)
673 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
674 | C.LetIn (name,so,ta) ->
675 check_is_really_smaller_arg context n nn kl x safes so &&
676 check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::context)
677 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
679 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
680 (*CSC: solo perche' non abbiamo trovato controesempi *)
681 check_is_really_smaller_arg context n nn kl x safes he
682 | C.Appl [] -> raise (AssertFailure "11")
684 | C.MutInd _ -> raise (AssertFailure "12")
685 | C.MutConstruct _ -> false
686 | C.MutCase (uri,i,outtype,term,pl) ->
688 C.Rel m when List.mem m safes || m = x ->
689 let (tys,len,isinductive,paramsno,cl) =
690 match CicEnvironment.get_obj uri with
691 C.InductiveDefinition (tl,_,paramsno) ->
694 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
696 let (_,isinductive,_,cl) = List.nth tl i in
700 (id, snd (split_prods tys paramsno ty))) cl
702 (tys,List.length tl,isinductive,paramsno,cl')
704 raise (TypeCheckerFailure
705 ("Unknown mutual inductive definition:" ^
706 UriManager.string_of_uri uri))
708 if not isinductive then
711 i && check_is_really_smaller_arg context n nn kl x safes p)
717 let debrujinedte = debrujin_constructor uri len c in
718 recursive_args tys 0 len debrujinedte
720 let (e,safes',n',nn',x',context') =
721 get_new_safes context p c rl' safes n nn x
724 check_is_really_smaller_arg context' n' nn' kl x' safes' e
725 ) (List.combine pl cl) true
726 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
727 let (tys,len,isinductive,paramsno,cl) =
728 match CicEnvironment.get_obj uri with
729 C.InductiveDefinition (tl,_,paramsno) ->
730 let (_,isinductive,_,cl) = List.nth tl i in
732 List.map (fun (n,_,ty,_) ->
733 Some(Cic.Name n,(Cic.Decl ty))) tl
738 (id, snd (split_prods tys paramsno ty))) cl
740 (tys,List.length tl,isinductive,paramsno,cl')
742 raise (TypeCheckerFailure
743 ("Unknown mutual inductive definition:" ^
744 UriManager.string_of_uri uri))
746 if not isinductive then
749 i && check_is_really_smaller_arg context n nn kl x safes p)
752 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
753 (*CSC: sugli argomenti di una applicazione *)
757 let debrujinedte = debrujin_constructor uri len c in
758 recursive_args tys 0 len debrujinedte
760 let (e, safes',n',nn',x',context') =
761 get_new_safes context p c rl' safes n nn x
764 check_is_really_smaller_arg context' n' nn' kl x' safes' e
765 ) (List.combine pl cl) true
769 i && check_is_really_smaller_arg context n nn kl x safes p
773 let len = List.length fl in
774 let n_plus_len = n + len
775 and nn_plus_len = nn + len
776 and x_plus_len = x + len
777 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
778 and safes' = List.map (fun x -> x + len) safes in
780 (fun (_,_,ty,bo) i ->
782 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
786 let len = List.length fl in
787 let n_plus_len = n + len
788 and nn_plus_len = nn + len
789 and x_plus_len = x + len
790 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
791 and safes' = List.map (fun x -> x + len) safes in
795 check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
799 and guarded_by_destructors context n nn kl x safes =
800 let module C = Cic in
801 let module U = UriManager in
803 C.Rel m when m > n && m <= nn -> false
805 (match List.nth context (n-1) with
806 Some (_,C.Decl _) -> true
807 | Some (_,C.Def (bo,_)) ->
808 guarded_by_destructors context m nn kl x safes
809 (CicSubstitution.lift m bo)
810 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
814 | C.Implicit _ -> true
816 guarded_by_destructors context n nn kl x safes te &&
817 guarded_by_destructors context n nn kl x safes ty
818 | C.Prod (name,so,ta) ->
819 guarded_by_destructors context n nn kl x safes so &&
820 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
821 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
822 | C.Lambda (name,so,ta) ->
823 guarded_by_destructors context n nn kl x safes so &&
824 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
825 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
826 | C.LetIn (name,so,ta) ->
827 guarded_by_destructors context n nn kl x safes so &&
828 guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
829 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
830 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
831 let k = List.nth kl (m - n - 1) in
832 if not (List.length tl > k) then false
836 i && guarded_by_destructors context n nn kl x safes param
838 check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
841 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
843 | C.Var (_,exp_named_subst)
844 | C.Const (_,exp_named_subst)
845 | C.MutInd (_,_,exp_named_subst)
846 | C.MutConstruct (_,_,_,exp_named_subst) ->
848 (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
850 | C.MutCase (uri,i,outtype,term,pl) ->
852 C.Rel m when List.mem m safes || m = x ->
853 let (tys,len,isinductive,paramsno,cl) =
854 match CicEnvironment.get_obj uri with
855 C.InductiveDefinition (tl,_,paramsno) ->
856 let len = List.length tl in
857 let (_,isinductive,_,cl) = List.nth tl i in
859 List.map (fun (n,_,ty,_) ->
860 Some(Cic.Name n,(Cic.Decl ty))) tl
865 let debrujinedty = debrujin_constructor uri len ty in
866 (id, snd (split_prods tys paramsno ty),
867 snd (split_prods tys paramsno debrujinedty)
870 (tys,len,isinductive,paramsno,cl')
872 raise (TypeCheckerFailure
873 ("Unknown mutual inductive definition:" ^
874 UriManager.string_of_uri uri))
876 if not isinductive then
877 guarded_by_destructors context n nn kl x safes outtype &&
878 guarded_by_destructors context n nn kl x safes term &&
879 (*CSC: manca ??? il controllo sul tipo di term? *)
882 i && guarded_by_destructors context n nn kl x safes p)
885 guarded_by_destructors context n nn kl x safes outtype &&
886 (*CSC: manca ??? il controllo sul tipo di term? *)
888 (fun (p,(_,c,brujinedc)) i ->
889 let rl' = recursive_args tys 0 len brujinedc in
890 let (e,safes',n',nn',x',context') =
891 get_new_safes context p c rl' safes n nn x
894 guarded_by_destructors context' n' nn' kl x' safes' e
895 ) (List.combine pl cl) true
896 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
897 let (tys,len,isinductive,paramsno,cl) =
898 match CicEnvironment.get_obj uri with
899 C.InductiveDefinition (tl,_,paramsno) ->
900 let (_,isinductive,_,cl) = List.nth tl i in
903 (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
908 (id, snd (split_prods tys paramsno ty))) cl
910 (tys,List.length tl,isinductive,paramsno,cl')
912 raise (TypeCheckerFailure
913 ("Unknown mutual inductive definition:" ^
914 UriManager.string_of_uri uri))
916 if not isinductive then
917 guarded_by_destructors context n nn kl x safes outtype &&
918 guarded_by_destructors context n nn kl x safes term &&
919 (*CSC: manca ??? il controllo sul tipo di term? *)
922 i && guarded_by_destructors context n nn kl x safes p)
925 guarded_by_destructors context n nn kl x safes outtype &&
926 (*CSC: manca ??? il controllo sul tipo di term? *)
929 i && guarded_by_destructors context n nn kl x safes t)
934 let debrujinedte = debrujin_constructor uri len c in
935 recursive_args tys 0 len debrujinedte
937 let (e, safes',n',nn',x',context') =
938 get_new_safes context p c rl' safes n nn x
941 guarded_by_destructors context' n' nn' kl x' safes' e
942 ) (List.combine pl cl) true
944 guarded_by_destructors context n nn kl x safes outtype &&
945 guarded_by_destructors context n nn kl x safes term &&
946 (*CSC: manca ??? il controllo sul tipo di term? *)
948 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
952 let len = List.length fl in
953 let n_plus_len = n + len
954 and nn_plus_len = nn + len
955 and x_plus_len = x + len
956 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
957 and safes' = List.map (fun x -> x + len) safes in
959 (fun (_,_,ty,bo) i ->
960 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
961 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
965 let len = List.length fl in
966 let n_plus_len = n + len
967 and nn_plus_len = nn + len
968 and x_plus_len = x + len
969 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
970 and safes' = List.map (fun x -> x + len) safes in
974 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
975 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
979 (* the boolean h means already protected *)
980 (* args is the list of arguments the type of the constructor that may be *)
981 (* found in head position must be applied to. *)
982 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
983 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
984 let module C = Cic in
985 (*CSC: There is a lot of code replication between the cases X and *)
986 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
987 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
988 match CicReduction.whd context te with
989 C.Rel m when m > n && m <= nn -> h
997 (* the term has just been type-checked *)
998 raise (AssertFailure "17")
999 | C.Lambda (name,so,de) ->
1000 does_not_occur context n nn so &&
1001 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
1002 (n + 1) (nn + 1) h de args coInductiveTypeURI
1003 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
1005 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
1006 | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
1008 match CicEnvironment.get_cooked_obj ~trust:false uri with
1009 C.InductiveDefinition (itl,_,_) ->
1010 let (_,_,_,cl) = List.nth itl i in
1011 let (_,cons) = List.nth cl (j - 1) in
1012 CicSubstitution.subst_vars exp_named_subst cons
1014 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1015 UriManager.string_of_uri uri))
1017 let rec analyse_branch context ty te =
1018 match CicReduction.whd context ty with
1019 C.Meta _ -> raise (AssertFailure "34")
1023 does_not_occur context n nn te
1026 raise (AssertFailure "24")(* due to type-checking *)
1027 | C.Prod (name,so,de) ->
1028 analyse_branch ((Some (name,(C.Decl so)))::context) de te
1031 raise (AssertFailure "25")(* due to type-checking *)
1032 | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1033 when uri == coInductiveTypeURI ->
1034 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1035 | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1036 guarded_by_constructors context n nn true te tl coInductiveTypeURI
1038 does_not_occur context n nn te
1039 | C.Const _ -> raise (AssertFailure "26")
1040 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1041 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1043 does_not_occur context n nn te
1044 | C.MutConstruct _ -> raise (AssertFailure "27")
1045 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1046 (*CSC: in head position. *)
1050 raise (AssertFailure "28")(* due to type-checking *)
1052 let rec analyse_instantiated_type context ty l =
1053 match CicReduction.whd context ty with
1059 | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1060 | C.Prod (name,so,de) ->
1065 analyse_branch context so he &&
1066 analyse_instantiated_type
1067 ((Some (name,(C.Decl so)))::context) de tl
1071 raise (AssertFailure "30")(* due to type-checking *)
1074 (fun i x -> i && does_not_occur context n nn x) true l
1075 | C.Const _ -> raise (AssertFailure "31")
1078 (fun i x -> i && does_not_occur context n nn x) true l
1079 | C.MutConstruct _ -> raise (AssertFailure "32")
1080 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1081 (*CSC: in head position. *)
1085 raise (AssertFailure "33")(* due to type-checking *)
1087 let rec instantiate_type args consty =
1090 | tlhe::tltl as l ->
1091 let consty' = CicReduction.whd context consty in
1097 let instantiated_de = CicSubstitution.subst he de in
1098 (*CSC: siamo sicuri che non sia troppo forte? *)
1099 does_not_occur context n nn tlhe &
1100 instantiate_type tl instantiated_de tltl
1102 (*CSC:We do not consider backbones with a MutCase, a *)
1103 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1104 raise (AssertFailure "23")
1106 | [] -> analyse_instantiated_type context consty' l
1107 (* These are all the other cases *)
1109 instantiate_type args consty tl
1110 | C.Appl ((C.CoFix (_,fl))::tl) ->
1111 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1112 let len = List.length fl in
1113 let n_plus_len = n + len
1114 and nn_plus_len = nn + len
1115 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1116 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1119 i && does_not_occur context n nn ty &&
1120 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1121 args coInductiveTypeURI
1123 | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1124 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1125 does_not_occur context n nn out &&
1126 does_not_occur context n nn te &&
1130 guarded_by_constructors context n nn h x args coInductiveTypeURI
1133 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1134 | C.Var (_,exp_named_subst)
1135 | C.Const (_,exp_named_subst) ->
1137 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1138 | C.MutInd _ -> assert false
1139 | C.MutConstruct (_,_,_,exp_named_subst) ->
1141 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1142 | C.MutCase (_,_,out,te,pl) ->
1143 does_not_occur context n nn out &&
1144 does_not_occur context n nn te &&
1148 guarded_by_constructors context n nn h x args coInductiveTypeURI
1151 let len = List.length fl in
1152 let n_plus_len = n + len
1153 and nn_plus_len = nn + len
1154 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1155 and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1157 (fun (_,_,ty,bo) i ->
1158 i && does_not_occur context n nn ty &&
1159 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1162 let len = List.length fl in
1163 let n_plus_len = n + len
1164 and nn_plus_len = nn + len
1165 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1166 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1169 i && does_not_occur context n nn ty &&
1170 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1171 args coInductiveTypeURI
1174 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1175 let module C = Cic in
1176 let module U = UriManager in
1177 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1178 (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1179 when CicReduction.are_convertible context so1 so2 ->
1180 check_allowed_sort_elimination context uri i need_dummy
1181 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1182 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1183 | (C.Sort C.Prop, C.Sort C.Set)
1184 | (C.Sort C.Prop, C.Sort C.CProp)
1185 | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1186 (* TASSI: da verificare *)
1187 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1188 (match CicEnvironment.get_obj uri with
1189 C.InductiveDefinition (itl,_,_) ->
1190 let (_,_,_,cl) = List.nth itl i in
1191 (* is a singleton definition or the empty proposition? *)
1192 List.length cl = 1 || List.length cl = 0
1194 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1195 UriManager.string_of_uri uri))
1197 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1198 | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true
1199 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1200 | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
1201 | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
1202 | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
1203 | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
1204 (* TASSI: da verificare *)
1206 (match CicEnvironment.get_obj uri with
1207 C.InductiveDefinition (itl,_,paramsno) ->
1209 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1211 let (_,_,_,cl) = List.nth itl i in
1213 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1215 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1216 UriManager.string_of_uri uri))
1218 | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true
1219 (* TASSI: da verificare *)
1220 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1221 let res = CicReduction.are_convertible context so ind
1224 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1225 C.Sort C.Prop -> true
1226 | (C.Sort C.Set | C.Sort C.CProp) ->
1227 (match CicEnvironment.get_obj uri with
1228 C.InductiveDefinition (itl,_,_) ->
1229 let (_,_,_,cl) = List.nth itl i in
1230 (* is a singleton definition? *)
1233 raise (TypeCheckerFailure
1234 ("Unknown mutual inductive definition:" ^
1235 UriManager.string_of_uri uri))
1239 | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
1240 when not need_dummy ->
1241 let res = CicReduction.are_convertible context so ind
1244 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1246 | C.Sort C.Set -> true
1247 | C.Sort C.CProp -> true
1248 | C.Sort (C.Type _) ->
1249 (* TASSI: da verificare *)
1250 (match CicEnvironment.get_obj uri with
1251 C.InductiveDefinition (itl,_,paramsno) ->
1252 let (_,_,_,cl) = List.nth itl i in
1255 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1258 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1260 raise (TypeCheckerFailure
1261 ("Unknown mutual inductive definition:" ^
1262 UriManager.string_of_uri uri))
1264 | _ -> raise (AssertFailure "19")
1266 | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
1267 (* TASSI: da verificare *)
1268 CicReduction.are_convertible context so ind
1271 and type_of_branch context argsno need_dummy outtype term constype =
1272 let module C = Cic in
1273 let module R = CicReduction in
1274 match R.whd context constype with
1279 C.Appl [outtype ; term]
1280 | C.Appl (C.MutInd (_,_,_)::tl) ->
1281 let (_,arguments) = split tl argsno
1283 if need_dummy && arguments = [] then
1286 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1287 | C.Prod (name,so,de) ->
1289 match CicSubstitution.lift 1 term with
1290 C.Appl l -> C.Appl (l@[C.Rel 1])
1291 | t -> C.Appl [t ; C.Rel 1]
1293 C.Prod (C.Anonymous,so,type_of_branch
1294 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1295 (CicSubstitution.lift 1 outtype) term' de)
1296 | _ -> raise (AssertFailure "20")
1298 (* check_metasenv_consistency checks that the "canonical" context of a
1299 metavariable is consitent - up to relocation via the relocation list l -
1300 with the actual context *)
1302 and check_metasenv_consistency metasenv context canonical_context l =
1303 let module C = Cic in
1304 let module R = CicReduction in
1305 let module S = CicSubstitution in
1306 let lifted_canonical_context =
1310 | (Some (n,C.Decl t))::tl ->
1311 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1312 | (Some (n,C.Def (t,None)))::tl ->
1313 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1314 | None::tl -> None::(aux (i+1) tl)
1315 | (Some (n,C.Def (t,Some ty)))::tl ->
1316 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
1318 aux 1 canonical_context
1324 | Some t,Some (_,C.Def (ct,_)) ->
1325 if not (R.are_convertible context t ct) then
1326 raise (TypeCheckerFailure (sprintf
1327 "Not well typed metavariable local context: expected a term convertible with %s, found %s"
1328 (CicPp.ppterm ct) (CicPp.ppterm t)))
1329 | Some t,Some (_,C.Decl ct) ->
1330 let type_t = type_of_aux' metasenv context t in
1331 if not (R.are_convertible context type_t ct) then
1332 raise (TypeCheckerFailure (sprintf
1333 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1334 (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
1336 raise (TypeCheckerFailure
1337 "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
1338 ) l lifted_canonical_context
1340 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1341 and type_of_aux' metasenv context t =
1342 let rec type_of_aux context =
1343 let module C = Cic in
1344 let module R = CicReduction in
1345 let module S = CicSubstitution in
1346 let module U = UriManager in
1350 match List.nth context (n - 1) with
1351 Some (_,C.Decl t) -> S.lift n t
1352 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
1353 | Some (_,C.Def (bo,None)) ->
1354 debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1355 type_of_aux context (S.lift n bo)
1356 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
1359 raise (TypeCheckerFailure "unbound variable")
1361 | C.Var (uri,exp_named_subst) ->
1363 check_exp_named_subst context exp_named_subst ;
1365 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1370 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1371 check_metasenv_consistency metasenv context canonical_context l;
1372 CicSubstitution.lift_meta l ty
1373 (* TASSI: CONSTRAINTS *)
1374 | C.Sort (C.Type t) ->
1375 let t' = CicUniv.fresh() in
1376 if not (CicUniv.add_gt t' t ) then
1377 assert false (* t' is fresh! an error in CicUniv *)
1380 (* TASSI: CONSTRAINTS *)
1381 | C.Sort s -> C.Sort (C.Type (CicUniv.fresh ()))
1382 | C.Implicit _ -> raise (AssertFailure "21")
1383 | C.Cast (te,ty) as t ->
1384 let _ = type_of_aux context ty in
1385 if R.are_convertible context (type_of_aux context te) ty then
1388 raise (TypeCheckerFailure
1389 (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1390 | C.Prod (name,s,t) ->
1391 let sort1 = type_of_aux context s
1392 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1393 let res = sort_of_prod context (name,s) (sort1,sort2) in
1395 | C.Lambda (n,s,t) ->
1396 let sort1 = type_of_aux context s in
1397 (match R.whd context sort1 with
1402 (TypeCheckerFailure (sprintf
1403 "Not well-typed lambda-abstraction: the source %s should be a
1404 type; instead it is a term of type %s" (CicPp.ppterm s)
1405 (CicPp.ppterm sort1)))
1407 let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1409 | C.LetIn (n,s,t) ->
1410 (* only to check if s is well-typed *)
1411 let ty = type_of_aux context s in
1412 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1413 LetIn is later reduced and maybe also re-checked.
1414 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1416 (* The type of the LetIn is reduced. Much faster than the previous
1417 solution. Moreover the inferred type is probably very different
1418 from the expected one.
1419 (CicReduction.whd context
1420 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1422 (* One-step LetIn reduction. Even faster than the previous solution.
1423 Moreover the inferred type is closer to the expected one. *)
1424 (CicSubstitution.subst s
1425 (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
1426 | C.Appl (he::tl) when List.length tl > 0 ->
1427 let hetype = type_of_aux context he in
1428 let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1429 eat_prods context hetype tlbody_and_type
1430 | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1431 | C.Const (uri,exp_named_subst) ->
1433 check_exp_named_subst context exp_named_subst ;
1435 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1439 | C.MutInd (uri,i,exp_named_subst) ->
1441 check_exp_named_subst context exp_named_subst ;
1443 CicSubstitution.subst_vars exp_named_subst
1444 (type_of_mutual_inductive_defs uri i)
1448 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1449 check_exp_named_subst context exp_named_subst ;
1451 CicSubstitution.subst_vars exp_named_subst
1452 (type_of_mutual_inductive_constr uri i j)
1455 | C.MutCase (uri,i,outtype,term,pl) ->
1456 let outsort = type_of_aux context outtype in
1457 let (need_dummy, k) =
1458 let rec guess_args context t =
1459 let outtype = CicReduction.whd context t in
1461 C.Sort _ -> (true, 0)
1462 | C.Prod (name, s, t) ->
1463 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1465 (* last prod before sort *)
1466 match CicReduction.whd context s with
1467 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1468 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1470 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1471 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1472 when U.eq uri' uri && i' = i -> (false, 1)
1477 raise (TypeCheckerFailure (sprintf
1478 "Malformed case analasys' output type %s" (CicPp.ppterm outtype)))
1480 (*CSC whd non serve dopo type_of_aux ? *)
1481 let (b, k) = guess_args context outsort in
1482 if not b then (b, k - 1) else (b, k)
1484 let (parameters, arguments, exp_named_subst) =
1485 match R.whd context (type_of_aux context term) with
1486 (*CSC manca il caso dei CAST *)
1487 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1488 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
1489 (*CSC: Hint: nella DTD servono per gli stylesheet. *)
1490 C.MutInd (uri',i',exp_named_subst) as typ ->
1491 if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1492 else raise (TypeCheckerFailure (sprintf
1493 "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1494 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1495 | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1496 if U.eq uri uri' && i = i' then
1498 split tl (List.length tl - k)
1499 in params,args,exp_named_subst
1500 else raise (TypeCheckerFailure (sprintf
1501 "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1502 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1504 raise (TypeCheckerFailure (sprintf
1505 "Case analysis: analysed term %s is not an inductive one"
1506 (CicPp.ppterm term)))
1508 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1509 let sort_of_ind_type =
1510 if parameters = [] then
1511 C.MutInd (uri,i,exp_named_subst)
1513 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1515 if not (check_allowed_sort_elimination context uri i need_dummy
1516 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1519 (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1520 (* let's check if the type of branches are right *)
1522 match CicEnvironment.get_cooked_obj ~trust:false uri with
1523 C.InductiveDefinition (_,_,parsno) -> parsno
1525 raise (TypeCheckerFailure
1526 ("Unknown mutual inductive definition:" ^
1527 UriManager.string_of_uri uri))
1529 let (_,branches_ok) =
1533 if parameters = [] then
1534 (C.MutConstruct (uri,i,j,exp_named_subst))
1536 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1543 R.are_convertible context (type_of_aux context p)
1544 (type_of_branch context parsno need_dummy outtype cons
1545 (type_of_aux context cons))
1546 in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res
1550 if not branches_ok then
1552 (TypeCheckerFailure "Case analysys: wrong branch type");
1553 if not need_dummy then
1554 C.Appl ((outtype::arguments)@[term])
1555 else if arguments = [] then
1558 C.Appl (outtype::arguments)
1560 let types_times_kl =
1564 let _ = type_of_aux context ty in
1565 (Some (C.Name n,(C.Decl ty)),k)) fl)
1567 let (types,kl) = List.split types_times_kl in
1568 let len = List.length types in
1570 (fun (name,x,ty,bo) ->
1572 (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1573 (CicSubstitution.lift len ty))
1576 let (m, eaten, context') =
1577 eat_lambdas (types @ context) (x + 1) bo
1579 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1582 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1585 (TypeCheckerFailure ("Fix: not guarded by destructors"))
1588 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1591 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1592 let (_,_,ty,_) = List.nth fl i in
1599 let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1601 let len = List.length types in
1605 (R.are_convertible (types @ context)
1606 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1609 (* let's control that the returned type is coinductive *)
1610 match returns_a_coinductive context ty with
1614 ("CoFix: does not return a coinductive type"))
1616 (*let's control the guarded by constructors conditions C{f,M}*)
1619 (guarded_by_constructors (types @ context) 0 len false bo
1623 (TypeCheckerFailure ("CoFix: not guarded by constructors"))
1627 (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1630 let (_,ty,_) = List.nth fl i in
1633 and check_exp_named_subst context =
1634 let rec check_exp_named_subst_aux substs =
1637 | ((uri,t) as subst)::tl ->
1639 CicSubstitution.subst_vars substs (type_of_variable uri) in
1640 (* CSC: this test should not exist
1641 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1642 Cic.Variable (_,Some bo,_,_) ->
1645 ("A variable with a body can not be explicit substituted"))
1646 | Cic.Variable (_,None,_,_) -> ()
1648 raise (TypeCheckerFailure
1649 ("Unknown variable definition:" ^
1650 UriManager.string_of_uri uri))
1653 let typeoft = type_of_aux context t in
1654 if CicReduction.are_convertible context typeoft typeofvar then
1655 check_exp_named_subst_aux (substs@[subst]) tl
1658 CicReduction.fdebug := 0 ;
1659 ignore (CicReduction.are_convertible context typeoft typeofvar) ;
1661 debug typeoft [typeofvar] ;
1662 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1665 check_exp_named_subst_aux []
1667 and sort_of_prod context (name,s) (t1, t2) =
1668 let module C = Cic in
1669 let t1' = CicReduction.whd context t1 in
1670 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1671 match (t1', t2') with
1672 (C.Sort s1, C.Sort s2)
1673 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1674 (* different from Coq manual!!! *)
1676 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1677 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1678 let t' = CicUniv.fresh() in
1679 if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
1680 assert false ; (* not possible, error in CicUniv *)
1682 | (C.Sort _,C.Sort (C.Type t1)) ->
1683 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1684 C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
1685 | (C.Meta _, C.Sort _) -> t2'
1686 | (C.Meta _, (C.Meta (_,_) as t))
1687 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1689 | (_,_) -> raise (TypeCheckerFailure (sprintf
1690 "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1691 (CicPp.ppterm t2')))
1693 and eat_prods context hetype =
1694 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1698 | (hete, hety)::tl ->
1699 (match (CicReduction.whd context hetype) with
1701 if CicReduction.are_convertible context hety s then
1702 (CicReduction.fdebug := -1 ;
1703 eat_prods context (CicSubstitution.subst hete t) tl
1707 CicReduction.fdebug := 0 ;
1708 ignore (CicReduction.are_convertible context s hety) ;
1711 raise (TypeCheckerFailure (sprintf
1712 "Appl: wrong parameter-type, expected %s, found %s"
1713 (CicPp.ppterm hetype) (CicPp.ppterm s)))
1716 raise (TypeCheckerFailure
1717 "Appl: this is not a function, it cannot be applied")
1720 and returns_a_coinductive context ty =
1721 let module C = Cic in
1722 match CicReduction.whd context ty with
1723 C.MutInd (uri,i,_) ->
1724 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1725 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1726 C.InductiveDefinition (itl,_,_) ->
1727 let (_,is_inductive,_,_) = List.nth itl i in
1728 if is_inductive then None else (Some uri)
1730 raise (TypeCheckerFailure
1731 ("Unknown mutual inductive definition:" ^
1732 UriManager.string_of_uri uri))
1734 | C.Appl ((C.MutInd (uri,i,_))::_) ->
1735 (match CicEnvironment.get_obj uri with
1736 C.InductiveDefinition (itl,_,_) ->
1737 let (_,is_inductive,_,_) = List.nth itl i in
1738 if is_inductive then None else (Some uri)
1740 raise (TypeCheckerFailure
1741 ("Unknown mutual inductive definition:" ^
1742 UriManager.string_of_uri uri))
1744 | C.Prod (n,so,de) ->
1745 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1750 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1753 type_of_aux context t
1755 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
1758 (* is a small constructor? *)
1759 (*CSC: ottimizzare calcolando staticamente *)
1760 and is_small context paramsno c =
1761 let rec is_small_aux context c =
1762 let module C = Cic in
1763 match CicReduction.whd context c with
1765 (*CSC: [] is an empty metasenv. Is it correct? *)
1766 let s = type_of_aux' [] context so in
1767 (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
1768 is_small_aux ((Some (n,(C.Decl so)))::context) de
1769 | _ -> true (*CSC: we trust the type-checker *)
1771 let (context',dx) = split_prods context paramsno c in
1772 is_small_aux context' dx
1776 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1779 type_of_aux' [] [] t
1781 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
1785 (* tassi FIXME: not sure where is this called... no history here... *)
1787 let module C = Cic in
1788 let module R = CicReduction in
1789 let module U = UriManager in
1790 (*match CicEnvironment.is_type_checked ~trust:false uri with*)
1791 match CicEnvironment.is_type_checked ~trust:true uri with
1792 CicEnvironment.CheckedObj cobj -> cobj
1793 | CicEnvironment.UncheckedObj uobj ->
1794 (* let's typecheck the uncooked object *)
1795 CicLogger.log (`Start_type_checking uri) ;
1796 CicUniv.directly_to_env_begin ();
1798 C.Constant (_,Some te,ty,_) ->
1799 let _ = type_of ty in
1800 if not (R.are_convertible [] (type_of te ) ty) then
1801 raise (TypeCheckerFailure
1802 ("Unknown constant:" ^ U.string_of_uri uri))
1803 | C.Constant (_,None,ty,_) ->
1804 (* only to check that ty is well-typed *)
1805 let _ = type_of ty in ()
1806 | C.CurrentProof (_,conjs,te,ty,_) ->
1809 (fun metasenv ((_,context,ty) as conj) ->
1810 ignore (type_of_aux' metasenv context ty) ;
1814 let _ = type_of_aux' conjs [] ty in
1815 let type_of_te = type_of_aux' conjs [] te in
1816 if not (R.are_convertible [] type_of_te ty)
1818 raise (TypeCheckerFailure (sprintf
1819 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
1820 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
1822 | C.Variable (_,bo,ty,_) ->
1823 (* only to check that ty is well-typed *)
1824 let _ = type_of ty in
1828 if not (R.are_convertible [] (type_of bo) ty) then
1829 raise (TypeCheckerFailure
1830 ("Unknown variable:" ^ U.string_of_uri uri))
1832 | C.InductiveDefinition _ ->
1833 check_mutual_inductive_defs uri uobj
1835 CicEnvironment.set_type_checking_info uri ;
1836 CicUniv.directly_to_env_end ();
1837 CicLogger.log (`Type_checking_completed uri);