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 = fun _ -> () ;;
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')
68 let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
71 | C.Implicit _ as t -> t
72 | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
73 | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
74 | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
75 | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t)
76 | C.Appl l -> C.Appl (List.map (aux k) l)
77 | C.Const (uri,exp_named_subst) ->
78 let exp_named_subst' =
79 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
81 C.Const (uri,exp_named_subst')
82 | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
83 if exp_named_subst != [] then
84 raise (TypeCheckerFailure
85 ("non-empty explicit named substitution is applied to "^
86 "a mutual inductive type which is being defined")) ;
87 C.Rel (k + number_of_types - tyno) ;
88 | C.MutInd (uri',tyno,exp_named_subst) ->
89 let exp_named_subst' =
90 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
92 C.MutInd (uri',tyno,exp_named_subst')
93 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
94 let exp_named_subst' =
95 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
97 C.MutConstruct (uri,tyno,consno,exp_named_subst')
98 | C.MutCase (sp,i,outty,t,pl) ->
99 C.MutCase (sp, i, aux k outty, aux k t,
102 let len = List.length fl in
105 (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
110 let len = List.length fl in
113 (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
116 C.CoFix (i, liftedfl)
121 exception CicEnvironmentError;;
123 let rec type_of_constant ~logger uri ugraph =
124 let module C = Cic in
125 let module R = CicReduction in
126 let module U = UriManager in
128 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
129 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
130 | CicEnvironment.UncheckedObj uobj ->
131 logger#log (`Start_type_checking uri) ;
132 (* let's typecheck the uncooked obj *)
134 (****************************************************************
135 TASSI: FIXME qui e' inutile ricordarselo,
136 tanto poi lo richiediamo alla cache che da quello su disco
137 *****************************************************************)
141 C.Constant (_,Some te,ty,_,_) ->
142 let _,ugraph = type_of ~logger ty ugraph in
143 let type_of_te,ugraph' = type_of ~logger te ugraph in
144 let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in
146 raise (TypeCheckerFailure (sprintf
147 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
148 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
152 | C.Constant (_,None,ty,_,_) ->
153 (* only to check that ty is well-typed *)
154 let _,ugraph' = type_of ~logger ty ugraph in
156 | C.CurrentProof (_,conjs,te,ty,_,_) ->
159 (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
161 type_of_aux' ~logger metasenv context ty ugraph
163 (metasenv @ [conj],ugraph')
166 let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
167 let type_of_te,ugraph3 =
168 type_of_aux' ~logger conjs [] te ugraph2
170 let b,ugraph4 = (R.are_convertible [] type_of_te ty ugraph3) in
172 raise (TypeCheckerFailure (sprintf
173 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
174 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
179 raise (TypeCheckerFailure
180 ("Unknown constant:" ^ U.string_of_uri uri)))
183 CicEnvironment.set_type_checking_info uri;
184 logger#log (`Type_checking_completed uri) ;
185 match CicEnvironment.is_type_checked ~trust:false ugraph uri with
186 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
187 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
188 with Invalid_argument s ->
189 (*debug_print (lazy s);*)
192 match cobj,ugraph with
193 (C.Constant (_,_,ty,_,_)),g -> ty,g
194 | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g
196 raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
198 and type_of_variable ~logger uri ugraph =
199 let module C = Cic in
200 let module R = CicReduction in
201 let module U = UriManager in
202 (* 0 because a variable is never cooked => no partial cooking at one level *)
203 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
204 CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
205 | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
206 logger#log (`Start_type_checking uri) ;
207 (* only to check that ty is well-typed *)
208 let _,ugraph1 = type_of ~logger ty ugraph in
213 let ty_bo,ugraph' = type_of ~logger bo ugraph1 in
214 let b,ugraph'' = (R.are_convertible [] ty_bo ty ugraph') in
216 raise (TypeCheckerFailure
217 ("Unknown variable:" ^ U.string_of_uri uri))
222 CicEnvironment.set_type_checking_info uri ;
223 logger#log (`Type_checking_completed uri) ;
224 match CicEnvironment.is_type_checked ~trust:false ugraph uri with
225 CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') ->
227 | CicEnvironment.CheckedObj _
228 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
229 with Invalid_argument s ->
230 (*debug_print (lazy s);*)
233 raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
235 and does_not_occur context n nn te =
236 let module C = Cic in
237 (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
238 (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
240 match CicReduction.whd context te with
241 C.Rel m when m > n && m <= nn -> false
243 | C.Meta _ (* CSC: Are we sure? No recursion?*)
245 | C.Implicit _ -> true
247 does_not_occur context n nn te && does_not_occur context n nn ty
248 | C.Prod (name,so,dest) ->
249 does_not_occur context n nn so &&
250 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
252 | C.Lambda (name,so,dest) ->
253 does_not_occur context n nn so &&
254 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
256 | C.LetIn (name,so,dest) ->
257 does_not_occur context n nn so &&
258 does_not_occur ((Some (name,(C.Def (so,None))))::context)
259 (n + 1) (nn + 1) dest
261 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
262 | C.Var (_,exp_named_subst)
263 | C.Const (_,exp_named_subst)
264 | C.MutInd (_,_,exp_named_subst)
265 | C.MutConstruct (_,_,_,exp_named_subst) ->
266 List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
268 | C.MutCase (_,_,out,te,pl) ->
269 does_not_occur context n nn out && does_not_occur context n nn te &&
270 List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
272 let len = List.length fl in
273 let n_plus_len = n + len in
274 let nn_plus_len = nn + len in
276 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
279 (fun (_,_,ty,bo) i ->
280 i && does_not_occur context n nn ty &&
281 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
284 let len = List.length fl in
285 let n_plus_len = n + len in
286 let nn_plus_len = nn + len in
288 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
292 i && does_not_occur context n nn ty &&
293 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
296 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
297 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
298 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
299 (*CSC strictly_positive *)
300 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
301 and weakly_positive context n nn uri te =
302 let module C = Cic in
303 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
305 C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
307 (*CSC mettere in cicSubstitution *)
308 let rec subst_inductive_type_with_dummy_mutind =
310 C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
312 | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
314 | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
315 | C.Prod (name,so,ta) ->
316 C.Prod (name, subst_inductive_type_with_dummy_mutind so,
317 subst_inductive_type_with_dummy_mutind ta)
318 | C.Lambda (name,so,ta) ->
319 C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
320 subst_inductive_type_with_dummy_mutind ta)
322 C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
323 | C.MutCase (uri,i,outtype,term,pl) ->
325 subst_inductive_type_with_dummy_mutind outtype,
326 subst_inductive_type_with_dummy_mutind term,
327 List.map subst_inductive_type_with_dummy_mutind pl)
329 C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
330 subst_inductive_type_with_dummy_mutind ty,
331 subst_inductive_type_with_dummy_mutind bo)) fl)
333 C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
334 subst_inductive_type_with_dummy_mutind ty,
335 subst_inductive_type_with_dummy_mutind bo)) fl)
336 | C.Const (uri,exp_named_subst) ->
337 let exp_named_subst' =
339 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
342 C.Const (uri,exp_named_subst')
343 | C.MutInd (uri,typeno,exp_named_subst) ->
344 let exp_named_subst' =
346 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
349 C.MutInd (uri,typeno,exp_named_subst')
350 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
351 let exp_named_subst' =
353 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
356 C.MutConstruct (uri,typeno,consno,exp_named_subst')
359 match CicReduction.whd context te with
360 C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
361 | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
362 | C.Prod (C.Anonymous,source,dest) ->
363 strictly_positive context n nn
364 (subst_inductive_type_with_dummy_mutind source) &&
365 weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
366 (n + 1) (nn + 1) uri dest
367 | C.Prod (name,source,dest) when
368 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
369 (* dummy abstraction, so we behave as in the anonimous case *)
370 strictly_positive context n nn
371 (subst_inductive_type_with_dummy_mutind source) &&
372 weakly_positive ((Some (name,(C.Decl source)))::context)
373 (n + 1) (nn + 1) uri dest
374 | C.Prod (name,source,dest) ->
375 does_not_occur context n nn
376 (subst_inductive_type_with_dummy_mutind source)&&
377 weakly_positive ((Some (name,(C.Decl source)))::context)
378 (n + 1) (nn + 1) uri dest
380 raise (TypeCheckerFailure "Malformed inductive constructor type")
382 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
383 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
384 and instantiate_parameters params c =
385 let module C = Cic in
386 match (c,params) with
388 | (C.Prod (_,_,ta), he::tl) ->
389 instantiate_parameters tl
390 (CicSubstitution.subst he ta)
391 | (C.Cast (te,_), _) -> instantiate_parameters params te
392 | (t,l) -> raise (AssertFailure "1")
394 and strictly_positive context n nn te =
395 let module C = Cic in
396 let module U = UriManager in
397 match CicReduction.whd context te with
400 (*CSC: bisogna controllare ty????*)
401 strictly_positive context n nn te
402 | C.Prod (name,so,ta) ->
403 does_not_occur context n nn so &&
404 strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
405 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
406 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
407 | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
408 let (ok,paramsno,ity,cl,name) =
409 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
411 C.InductiveDefinition (tl,_,paramsno,_) ->
412 let (name,_,ity,cl) = List.nth tl i in
413 (List.length tl = 1, paramsno, ity, cl, name)
415 raise (TypeCheckerFailure
416 ("Unknown inductive type:" ^ U.string_of_uri uri))
418 let (params,arguments) = split tl paramsno in
419 let lifted_params = List.map (CicSubstitution.lift 1) params in
423 instantiate_parameters lifted_params
424 (CicSubstitution.subst_vars exp_named_subst te)
429 (fun x i -> i && does_not_occur context n nn x)
431 (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
436 ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
439 | t -> does_not_occur context n nn t
441 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
442 and are_all_occurrences_positive context uri indparamsno i n nn te =
443 let module C = Cic in
444 match CicReduction.whd context te with
445 C.Appl ((C.Rel m)::tl) when m = i ->
446 (*CSC: riscrivere fermandosi a 0 *)
447 (* let's check if the inductive type is applied at least to *)
448 (* indparamsno parameters *)
454 match CicReduction.whd context x with
455 C.Rel m when m = n - (indparamsno - k) -> k - 1
457 raise (TypeCheckerFailure
458 ("Non-positive occurence in mutual inductive definition(s) " ^
459 UriManager.string_of_uri uri))
463 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
465 raise (TypeCheckerFailure
466 ("Non-positive occurence in mutual inductive definition(s) " ^
467 UriManager.string_of_uri uri))
468 | C.Rel m when m = i ->
469 if indparamsno = 0 then
472 raise (TypeCheckerFailure
473 ("Non-positive occurence in mutual inductive definition(s) " ^
474 UriManager.string_of_uri uri))
475 | C.Prod (C.Anonymous,source,dest) ->
476 strictly_positive context n nn source &&
477 are_all_occurrences_positive
478 ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
479 (i+1) (n + 1) (nn + 1) dest
480 | C.Prod (name,source,dest) when
481 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
482 (* dummy abstraction, so we behave as in the anonimous case *)
483 strictly_positive context n nn source &&
484 are_all_occurrences_positive
485 ((Some (name,(C.Decl source)))::context) uri indparamsno
486 (i+1) (n + 1) (nn + 1) dest
487 | C.Prod (name,source,dest) ->
488 does_not_occur context n nn source &&
489 are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
490 uri indparamsno (i+1) (n + 1) (nn + 1) dest
493 (TypeCheckerFailure ("Malformed inductive constructor type " ^
494 (UriManager.string_of_uri uri)))
496 (* Main function to checks the correctness of a mutual *)
497 (* inductive block definition. This is the function *)
498 (* exported to the proof-engine. *)
499 and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
500 let module U = UriManager in
501 (* let's check if the arity of the inductive types are well *)
503 let ugrap1 = List.fold_left
504 (fun ugraph (_,_,x,_) -> let _,ugraph' =
505 type_of ~logger x ugraph in ugraph')
508 (* let's check if the types of the inductive constructors *)
509 (* are well formed. *)
510 (* In order not to use type_of_aux we put the types of the *)
511 (* mutual inductive types at the head of the types of the *)
512 (* constructors using Prods *)
513 let len = List.length itl in
515 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
518 (fun (_,_,_,cl) (i,ugraph) ->
521 (fun ugraph (name,te) ->
522 let debrujinedte = debrujin_constructor uri len te in
525 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
528 let _,ugraph' = type_of ~logger augmented_term ugraph in
529 (* let's check also the positivity conditions *)
532 (are_all_occurrences_positive tys uri indparamsno i 0 len
536 (TypeCheckerFailure ("Non positive occurence in " ^
537 U.string_of_uri uri))
546 (* Main function to checks the correctness of a mutual *)
547 (* inductive block definition. *)
548 and check_mutual_inductive_defs uri obj ugraph =
550 Cic.InductiveDefinition (itl, params, indparamsno, _) ->
551 typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph
553 raise (TypeCheckerFailure (
554 "Unknown mutual inductive definition:" ^
555 UriManager.string_of_uri uri))
557 and type_of_mutual_inductive_defs ~logger uri i ugraph =
558 let module C = Cic in
559 let module R = CicReduction in
560 let module U = UriManager in
562 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
563 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
564 | CicEnvironment.UncheckedObj uobj ->
565 logger#log (`Start_type_checking uri) ;
567 check_mutual_inductive_defs ~logger uri uobj ugraph
569 (* TASSI: FIXME: check ugraph1 == ugraph ritornato da env *)
571 CicEnvironment.set_type_checking_info uri ;
572 logger#log (`Type_checking_completed uri) ;
573 (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
574 CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
575 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
578 Invalid_argument s ->
579 (*debug_print (lazy s);*)
583 C.InductiveDefinition (dl,_,_,_) ->
584 let (_,_,arity,_) = List.nth dl i in
587 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
588 U.string_of_uri uri))
590 and type_of_mutual_inductive_constr ~logger uri i j ugraph =
591 let module C = Cic in
592 let module R = CicReduction in
593 let module U = UriManager in
595 match CicEnvironment.is_type_checked ~trust:true ugraph uri with
596 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
597 | CicEnvironment.UncheckedObj uobj ->
598 logger#log (`Start_type_checking uri) ;
600 check_mutual_inductive_defs ~logger uri uobj ugraph
602 (* check ugraph1 validity ??? == ugraph' *)
604 CicEnvironment.set_type_checking_info uri ;
605 logger#log (`Type_checking_completed uri) ;
607 CicEnvironment.is_type_checked ~trust:false ugraph uri
609 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
610 | CicEnvironment.UncheckedObj _ ->
611 raise CicEnvironmentError)
613 Invalid_argument s ->
614 (*debug_print (lazy s);*)
618 C.InductiveDefinition (dl,_,_,_) ->
619 let (_,_,_,cl) = List.nth dl i in
620 let (_,ty) = List.nth cl (j-1) in
623 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
624 UriManager.string_of_uri uri))
626 and recursive_args context n nn te =
627 let module C = Cic in
628 match CicReduction.whd context te with
634 | C.Cast _ (*CSC ??? *) ->
635 raise (AssertFailure "3") (* due to type-checking *)
636 | C.Prod (name,so,de) ->
637 (not (does_not_occur context n nn so)) ::
638 (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
641 raise (AssertFailure "4") (* due to type-checking *)
643 | C.Const _ -> raise (AssertFailure "5")
648 | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *)
650 and get_new_safes ?(subst = []) context p c rl safes n nn x =
651 let module C = Cic in
652 let module U = UriManager in
653 let module R = CicReduction in
654 match (R.whd ~subst context c, R.whd ~subst context p, rl) with
655 (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
656 (* we are sure that the two sources are convertible because we *)
657 (* have just checked this. So let's go along ... *)
659 List.map (fun x -> x + 1) safes
662 if b then 1::safes' else safes'
664 get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
665 ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
666 | (C.Prod _, (C.MutConstruct _ as e), _)
667 | (C.Prod _, (C.Rel _ as e), _)
668 | (C.MutInd _, e, [])
669 | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
671 (* CSC: If the next exception is raised, it just means that *)
672 (* CSC: the proof-assistant allows to use very strange things *)
673 (* CSC: as a branch of a case whose type is a Prod. In *)
674 (* CSC: particular, this means that a new (C.Prod, x,_) case *)
675 (* CSC: must be considered in this match. (e.g. x = MutCase) *)
678 (Printf.sprintf "Get New Safes: c=%s ; p=%s"
679 (CicPp.ppterm c) (CicPp.ppterm p)))
681 and split_prods ?(subst = []) context n te =
682 let module C = Cic in
683 let module R = CicReduction in
684 match (n, R.whd context te) with
686 | (n, C.Prod (name,so,ta)) when n > 0 ->
687 split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
688 | (_, _) -> raise (AssertFailure "8")
690 and eat_lambdas ?(subst = []) context n te =
691 let module C = Cic in
692 let module R = CicReduction in
693 match (n, R.whd ~subst context te) with
694 (0, _) -> (te, 0, context)
695 | (n, C.Lambda (name,so,ta)) when n > 0 ->
696 let (te, k, context') =
697 eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
699 (te, k + 1, context')
701 raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
703 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
704 and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
705 (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
706 (*CSC: cfr guarded_by_destructors *)
707 let module C = Cic in
708 let module U = UriManager in
709 match CicReduction.whd context te with
710 C.Rel m when List.mem m safes -> true
717 (* | C.Cast (te,ty) ->
718 check_is_really_smaller_arg ~subst n nn kl x safes te &&
719 check_is_really_smaller_arg ~subst n nn kl x safes ty*)
720 (* | C.Prod (_,so,ta) ->
721 check_is_really_smaller_arg ~subst n nn kl x safes so &&
722 check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
723 (List.map (fun x -> x + 1) safes) ta*)
724 | C.Prod _ -> raise (AssertFailure "10")
725 | C.Lambda (name,so,ta) ->
726 check_is_really_smaller_arg ~subst context n nn kl x safes so &&
727 check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
728 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
729 | C.LetIn (name,so,ta) ->
730 check_is_really_smaller_arg ~subst context n nn kl x safes so &&
731 check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context)
732 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
734 (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
735 (*CSC: solo perche' non abbiamo trovato controesempi *)
736 check_is_really_smaller_arg ~subst context n nn kl x safes he
737 | C.Appl [] -> raise (AssertFailure "11")
739 | C.MutInd _ -> raise (AssertFailure "12")
740 | C.MutConstruct _ -> false
741 | C.MutCase (uri,i,outtype,term,pl) ->
743 C.Rel m when List.mem m safes || m = x ->
744 let (tys,len,isinductive,paramsno,cl) =
745 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
747 C.InductiveDefinition (tl,_,paramsno,_) ->
750 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
752 let (_,isinductive,_,cl) = List.nth tl i in
756 (id, snd (split_prods ~subst tys paramsno ty))) cl
758 (tys,List.length tl,isinductive,paramsno,cl')
760 raise (TypeCheckerFailure
761 ("Unknown mutual inductive definition:" ^
762 UriManager.string_of_uri uri))
764 if not isinductive then
767 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
774 Invalid_argument _ ->
775 raise (TypeCheckerFailure "not enough patterns")
780 let debrujinedte = debrujin_constructor uri len c in
781 recursive_args tys 0 len debrujinedte
783 let (e,safes',n',nn',x',context') =
784 get_new_safes ~subst context p c rl' safes n nn x
787 check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
789 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
790 let (tys,len,isinductive,paramsno,cl) =
791 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
793 C.InductiveDefinition (tl,_,paramsno,_) ->
794 let (_,isinductive,_,cl) = List.nth tl i in
796 List.map (fun (n,_,ty,_) ->
797 Some(Cic.Name n,(Cic.Decl ty))) tl
802 (id, snd (split_prods ~subst tys paramsno ty))) cl
804 (tys,List.length tl,isinductive,paramsno,cl')
806 raise (TypeCheckerFailure
807 ("Unknown mutual inductive definition:" ^
808 UriManager.string_of_uri uri))
810 if not isinductive then
813 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
820 Invalid_argument _ ->
821 raise (TypeCheckerFailure "not enough patterns")
823 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
824 (*CSC: sugli argomenti di una applicazione *)
828 let debrujinedte = debrujin_constructor uri len c in
829 recursive_args tys 0 len debrujinedte
831 let (e, safes',n',nn',x',context') =
832 get_new_safes context p c rl' safes n nn x
835 check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
840 i && check_is_really_smaller_arg ~subst context n nn kl x safes p
844 let len = List.length fl in
845 let n_plus_len = n + len
846 and nn_plus_len = nn + len
847 and x_plus_len = x + len
848 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
849 and safes' = List.map (fun x -> x + len) safes in
851 (fun (_,_,ty,bo) i ->
853 check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
857 let len = List.length fl in
858 let n_plus_len = n + len
859 and nn_plus_len = nn + len
860 and x_plus_len = x + len
861 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
862 and safes' = List.map (fun x -> x + len) safes in
866 check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
870 and guarded_by_destructors ?(subst = []) context n nn kl x safes =
871 let module C = Cic in
872 let module U = UriManager in
874 C.Rel m when m > n && m <= nn -> false
876 (match List.nth context (n-1) with
877 Some (_,C.Decl _) -> true
878 | Some (_,C.Def (bo,_)) ->
879 guarded_by_destructors context m nn kl x safes
880 (CicSubstitution.lift m bo)
881 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
885 | C.Implicit _ -> true
887 guarded_by_destructors context n nn kl x safes te &&
888 guarded_by_destructors context n nn kl x safes ty
889 | C.Prod (name,so,ta) ->
890 guarded_by_destructors context n nn kl x safes so &&
891 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
892 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
893 | C.Lambda (name,so,ta) ->
894 guarded_by_destructors context n nn kl x safes so &&
895 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
896 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
897 | C.LetIn (name,so,ta) ->
898 guarded_by_destructors context n nn kl x safes so &&
899 guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
900 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
901 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
902 let k = List.nth kl (m - n - 1) in
903 if not (List.length tl > k) then false
907 i && guarded_by_destructors context n nn kl x safes param
909 check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
912 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
914 | C.Var (_,exp_named_subst)
915 | C.Const (_,exp_named_subst)
916 | C.MutInd (_,_,exp_named_subst)
917 | C.MutConstruct (_,_,_,exp_named_subst) ->
919 (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
921 | C.MutCase (uri,i,outtype,term,pl) ->
922 (match CicReduction.whd context term with
923 C.Rel m when List.mem m safes || m = x ->
924 let (tys,len,isinductive,paramsno,cl) =
925 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
927 C.InductiveDefinition (tl,_,paramsno,_) ->
928 let len = List.length tl in
929 let (_,isinductive,_,cl) = List.nth tl i in
931 List.map (fun (n,_,ty,_) ->
932 Some(Cic.Name n,(Cic.Decl ty))) tl
937 let debrujinedty = debrujin_constructor uri len ty in
938 (id, snd (split_prods ~subst tys paramsno ty),
939 snd (split_prods ~subst tys paramsno debrujinedty)
942 (tys,len,isinductive,paramsno,cl')
944 raise (TypeCheckerFailure
945 ("Unknown mutual inductive definition:" ^
946 UriManager.string_of_uri uri))
948 if not isinductive then
949 guarded_by_destructors context n nn kl x safes outtype &&
950 guarded_by_destructors context n nn kl x safes term &&
951 (*CSC: manca ??? il controllo sul tipo di term? *)
954 i && guarded_by_destructors context n nn kl x safes p)
961 Invalid_argument _ ->
962 raise (TypeCheckerFailure "not enough patterns")
964 guarded_by_destructors context n nn kl x safes outtype &&
965 (*CSC: manca ??? il controllo sul tipo di term? *)
967 (fun (p,(_,c,brujinedc)) i ->
968 let rl' = recursive_args tys 0 len brujinedc in
969 let (e,safes',n',nn',x',context') =
970 get_new_safes context p c rl' safes n nn x
973 guarded_by_destructors context' n' nn' kl x' safes' e
975 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
976 let (tys,len,isinductive,paramsno,cl) =
977 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
979 C.InductiveDefinition (tl,_,paramsno,_) ->
980 let (_,isinductive,_,cl) = List.nth tl i in
983 (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
988 (id, snd (split_prods ~subst tys paramsno ty))) cl
990 (tys,List.length tl,isinductive,paramsno,cl')
992 raise (TypeCheckerFailure
993 ("Unknown mutual inductive definition:" ^
994 UriManager.string_of_uri uri))
996 if not isinductive then
997 guarded_by_destructors context n nn kl x safes outtype &&
998 guarded_by_destructors context n nn kl x safes term &&
999 (*CSC: manca ??? il controllo sul tipo di term? *)
1002 i && guarded_by_destructors context n nn kl x safes p)
1009 Invalid_argument _ ->
1010 raise (TypeCheckerFailure "not enough patterns")
1012 guarded_by_destructors context n nn kl x safes outtype &&
1013 (*CSC: manca ??? il controllo sul tipo di term? *)
1016 i && guarded_by_destructors context n nn kl x safes t)
1021 let debrujinedte = debrujin_constructor uri len c in
1022 recursive_args tys 0 len debrujinedte
1024 let (e, safes',n',nn',x',context') =
1025 get_new_safes context p c rl' safes n nn x
1028 guarded_by_destructors context' n' nn' kl x' safes' e
1031 guarded_by_destructors context n nn kl x safes outtype &&
1032 guarded_by_destructors context n nn kl x safes term &&
1033 (*CSC: manca ??? il controllo sul tipo di term? *)
1035 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
1039 let len = List.length fl in
1040 let n_plus_len = n + len
1041 and nn_plus_len = nn + len
1042 and x_plus_len = x + len
1043 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1044 and safes' = List.map (fun x -> x + len) safes in
1046 (fun (_,_,ty,bo) i ->
1047 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1048 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1049 x_plus_len safes' bo
1051 | C.CoFix (_, fl) ->
1052 let len = List.length fl in
1053 let n_plus_len = n + len
1054 and nn_plus_len = nn + len
1055 and x_plus_len = x + len
1056 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1057 and safes' = List.map (fun x -> x + len) safes in
1061 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1062 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1063 x_plus_len safes' bo
1066 (* the boolean h means already protected *)
1067 (* args is the list of arguments the type of the constructor that may be *)
1068 (* found in head position must be applied to. *)
1069 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
1070 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
1071 let module C = Cic in
1072 (*CSC: There is a lot of code replication between the cases X and *)
1073 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
1074 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
1075 match CicReduction.whd context te with
1076 C.Rel m when m > n && m <= nn -> h
1084 (* the term has just been type-checked *)
1085 raise (AssertFailure "17")
1086 | C.Lambda (name,so,de) ->
1087 does_not_occur context n nn so &&
1088 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
1089 (n + 1) (nn + 1) h de args coInductiveTypeURI
1090 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
1092 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
1093 | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
1097 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1098 with Not_found -> assert false
1101 C.InductiveDefinition (itl,_,_,_) ->
1102 let (_,_,_,cl) = List.nth itl i in
1103 let (_,cons) = List.nth cl (j - 1) in
1104 CicSubstitution.subst_vars exp_named_subst cons
1106 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1107 UriManager.string_of_uri uri))
1109 let rec analyse_branch context ty te =
1110 match CicReduction.whd context ty with
1111 C.Meta _ -> raise (AssertFailure "34")
1115 does_not_occur context n nn te
1118 raise (AssertFailure "24")(* due to type-checking *)
1119 | C.Prod (name,so,de) ->
1120 analyse_branch ((Some (name,(C.Decl so)))::context) de te
1123 raise (AssertFailure "25")(* due to type-checking *)
1124 | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1125 when uri == coInductiveTypeURI ->
1126 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1127 | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1128 guarded_by_constructors context n nn true te tl coInductiveTypeURI
1130 does_not_occur context n nn te
1131 | C.Const _ -> raise (AssertFailure "26")
1132 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1133 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1135 does_not_occur context n nn te
1136 | C.MutConstruct _ -> raise (AssertFailure "27")
1137 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1138 (*CSC: in head position. *)
1142 raise (AssertFailure "28")(* due to type-checking *)
1144 let rec analyse_instantiated_type context ty l =
1145 match CicReduction.whd context ty with
1151 | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1152 | C.Prod (name,so,de) ->
1157 analyse_branch context so he &&
1158 analyse_instantiated_type
1159 ((Some (name,(C.Decl so)))::context) de tl
1163 raise (AssertFailure "30")(* due to type-checking *)
1166 (fun i x -> i && does_not_occur context n nn x) true l
1167 | C.Const _ -> raise (AssertFailure "31")
1170 (fun i x -> i && does_not_occur context n nn x) true l
1171 | C.MutConstruct _ -> raise (AssertFailure "32")
1172 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1173 (*CSC: in head position. *)
1177 raise (AssertFailure "33")(* due to type-checking *)
1179 let rec instantiate_type args consty =
1182 | tlhe::tltl as l ->
1183 let consty' = CicReduction.whd context consty in
1189 let instantiated_de = CicSubstitution.subst he de in
1190 (*CSC: siamo sicuri che non sia troppo forte? *)
1191 does_not_occur context n nn tlhe &
1192 instantiate_type tl instantiated_de tltl
1194 (*CSC:We do not consider backbones with a MutCase, a *)
1195 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1196 raise (AssertFailure "23")
1198 | [] -> analyse_instantiated_type context consty' l
1199 (* These are all the other cases *)
1201 instantiate_type args consty tl
1202 | C.Appl ((C.CoFix (_,fl))::tl) ->
1203 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1204 let len = List.length fl in
1205 let n_plus_len = n + len
1206 and nn_plus_len = nn + len
1207 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1208 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1211 i && does_not_occur context n nn ty &&
1212 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1213 args coInductiveTypeURI
1215 | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1216 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1217 does_not_occur context n nn out &&
1218 does_not_occur context n nn te &&
1222 guarded_by_constructors context n nn h x args coInductiveTypeURI
1225 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1226 | C.Var (_,exp_named_subst)
1227 | C.Const (_,exp_named_subst) ->
1229 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1230 | C.MutInd _ -> assert false
1231 | C.MutConstruct (_,_,_,exp_named_subst) ->
1233 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1234 | C.MutCase (_,_,out,te,pl) ->
1235 does_not_occur context n nn out &&
1236 does_not_occur context n nn te &&
1240 guarded_by_constructors context n nn h x args coInductiveTypeURI
1243 let len = List.length fl in
1244 let n_plus_len = n + len
1245 and nn_plus_len = nn + len
1246 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1247 and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1249 (fun (_,_,ty,bo) i ->
1250 i && does_not_occur context n nn ty &&
1251 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1254 let len = List.length fl in
1255 let n_plus_len = n + len
1256 and nn_plus_len = nn + len
1257 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1258 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1261 i && does_not_occur context n nn ty &&
1262 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1263 args coInductiveTypeURI
1266 and check_allowed_sort_elimination ~logger context uri i need_dummy ind
1267 arity1 arity2 ugraph =
1268 let module C = Cic in
1269 let module U = UriManager in
1270 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1271 (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
1272 let b,ugraph1 = CicReduction.are_convertible context so1 so2 ugraph in
1274 check_allowed_sort_elimination ~logger context uri i need_dummy
1275 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1
1278 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
1279 | (C.Sort C.Prop, C.Sort C.Set)
1280 | (C.Sort C.Prop, C.Sort C.CProp)
1281 | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1282 (* TASSI: da verificare *)
1283 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1284 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1286 C.InductiveDefinition (itl,_,_,_) ->
1287 let (_,_,_,cl) = List.nth itl i in
1288 (* is a singleton definition or the empty proposition? *)
1289 (List.length cl = 1 || List.length cl = 0) , ugraph
1291 raise (TypeCheckerFailure
1292 ("Unknown mutual inductive definition:" ^
1293 UriManager.string_of_uri uri))
1295 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
1296 | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
1297 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
1298 | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph
1299 | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
1300 | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
1301 | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
1302 (* TASSI: da verificare *)
1304 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1306 C.InductiveDefinition (itl,_,paramsno,_) ->
1308 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1310 let (_,_,_,cl) = List.nth itl i in
1312 (fun (_,x) (i,ugraph) ->
1314 is_small ~logger tys paramsno x ugraph
1319 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1320 UriManager.string_of_uri uri))
1322 | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
1323 (* TASSI: da verificare *)
1324 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1325 let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1329 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1330 C.Sort C.Prop -> true,ugraph1
1331 | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
1332 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1334 C.InductiveDefinition (itl,_,_,_) ->
1335 let (_,_,_,cl) = List.nth itl i in
1336 (* is a singleton definition or the empty proposition? *)
1337 (List.length cl = 1 || List.length cl = 0),ugraph1
1339 raise (TypeCheckerFailure
1340 ("Unknown mutual inductive definition:" ^
1341 UriManager.string_of_uri uri)))
1342 | _ -> false,ugraph1)
1343 | ((C.Sort C.Set, C.Prod (name,so,ta))
1344 | (C.Sort C.CProp, C.Prod (name,so,ta)))
1345 when not need_dummy ->
1346 let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1350 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1352 | C.Sort C.Set -> true,ugraph1
1353 | C.Sort C.CProp -> true,ugraph1
1354 | C.Sort (C.Type _) ->
1355 (* TASSI: da verificare *)
1356 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1358 C.InductiveDefinition (itl,_,paramsno,_) ->
1359 let (_,_,_,cl) = List.nth itl i in
1362 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1365 (fun (_,x) (i,ugraph) ->
1367 is_small ~logger tys paramsno x ugraph
1370 ) cl (true,ugraph1))
1372 raise (TypeCheckerFailure
1373 ("Unknown mutual inductive definition:" ^
1374 UriManager.string_of_uri uri))
1376 | _ -> raise (AssertFailure "19")
1378 | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
1379 (* TASSI: da verificare *)
1380 CicReduction.are_convertible context so ind ugraph
1381 | (_,_) -> false,ugraph
1383 and type_of_branch context argsno need_dummy outtype term constype =
1384 let module C = Cic in
1385 let module R = CicReduction in
1386 match R.whd context constype with
1391 C.Appl [outtype ; term]
1392 | C.Appl (C.MutInd (_,_,_)::tl) ->
1393 let (_,arguments) = split tl argsno
1395 if need_dummy && arguments = [] then
1398 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1399 | C.Prod (name,so,de) ->
1401 match CicSubstitution.lift 1 term with
1402 C.Appl l -> C.Appl (l@[C.Rel 1])
1403 | t -> C.Appl [t ; C.Rel 1]
1405 C.Prod (C.Anonymous,so,type_of_branch
1406 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1407 (CicSubstitution.lift 1 outtype) term' de)
1408 | _ -> raise (AssertFailure "20")
1410 (* check_metasenv_consistency checks that the "canonical" context of a
1411 metavariable is consitent - up to relocation via the relocation list l -
1412 with the actual context *)
1415 and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
1416 canonical_context l ugraph
1418 let module C = Cic in
1419 let module R = CicReduction in
1420 let module S = CicSubstitution in
1421 let lifted_canonical_context =
1425 | (Some (n,C.Decl t))::tl ->
1426 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1427 | (Some (n,C.Def (t,None)))::tl ->
1428 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1429 | None::tl -> None::(aux (i+1) tl)
1430 | (Some (n,C.Def (t,Some ty)))::tl ->
1431 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
1433 aux 1 canonical_context
1439 | Some t,Some (_,C.Def (ct,_)) ->
1441 R.are_convertible ~subst ~metasenv context t ct ugraph
1446 (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))
1449 | Some t,Some (_,C.Decl ct) ->
1450 let type_t,ugraph1 =
1451 type_of_aux' ~logger ~subst metasenv context t ugraph
1454 R.are_convertible ~subst ~metasenv context type_t ct ugraph1
1457 raise (TypeCheckerFailure
1458 (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1459 (CicPp.ppterm ct) (CicPp.ppterm t)
1460 (CicPp.ppterm type_t)))
1464 raise (TypeCheckerFailure
1465 ("Not well typed metavariable local context: "^
1466 "an hypothesis, that is not hidden, is not instantiated"))
1467 ) ugraph l lifted_canonical_context
1471 type_of_aux' is just another name (with a different scope)
1475 and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
1476 let rec type_of_aux ~logger context t ugraph =
1477 let module C = Cic in
1478 let module R = CicReduction in
1479 let module S = CicSubstitution in
1480 let module U = UriManager in
1484 match List.nth context (n - 1) with
1485 Some (_,C.Decl t) -> S.lift n t,ugraph
1486 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
1487 | Some (_,C.Def (bo,None)) ->
1488 debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ;
1489 type_of_aux ~logger context (S.lift n bo) ugraph
1491 (TypeCheckerFailure "Reference to deleted hypothesis")
1494 raise (TypeCheckerFailure "unbound variable")
1496 | C.Var (uri,exp_named_subst) ->
1499 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1501 let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
1502 let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
1507 let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
1509 check_metasenv_consistency ~logger
1510 ~subst metasenv context canonical_context l ugraph
1512 (* assuming subst is well typed !!!!! *)
1513 ((CicSubstitution.subst_meta l ty), ugraph1)
1514 (* type_of_aux context (CicSubstitution.subst_meta l term) *)
1515 with CicUtil.Subst_not_found _ ->
1516 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1518 check_metasenv_consistency ~logger
1519 ~subst metasenv context canonical_context l ugraph
1521 ((CicSubstitution.subst_meta l ty),ugraph1))
1522 (* TASSI: CONSTRAINTS *)
1523 | C.Sort (C.Type t) ->
1524 let t' = CicUniv.fresh() in
1525 let ugraph1 = CicUniv.add_gt t' t ugraph in
1526 (C.Sort (C.Type t')),ugraph1
1527 (* TASSI: CONSTRAINTS *)
1528 | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
1529 | C.Implicit _ -> raise (AssertFailure "21")
1530 | C.Cast (te,ty) as t ->
1531 let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1532 let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
1534 R.are_convertible ~subst ~metasenv context ty_te ty ugraph2
1539 raise (TypeCheckerFailure
1540 (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1541 | C.Prod (name,s,t) ->
1542 let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1544 type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t ugraph1
1546 sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2
1547 | C.Lambda (n,s,t) ->
1548 let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1549 (match R.whd ~subst context sort1 with
1554 (TypeCheckerFailure (sprintf
1555 "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
1556 (CicPp.ppterm sort1)))
1559 type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
1561 (C.Prod (n,s,type2)),ugraph2
1562 | C.LetIn (n,s,t) ->
1563 (* only to check if s is well-typed *)
1564 let ty,ugraph1 = type_of_aux ~logger context s ugraph in
1565 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1566 LetIn is later reduced and maybe also re-checked.
1567 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1569 (* The type of the LetIn is reduced. Much faster than the previous
1570 solution. Moreover the inferred type is probably very different
1571 from the expected one.
1572 (CicReduction.whd context
1573 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1575 (* One-step LetIn reduction. Even faster than the previous solution.
1576 Moreover the inferred type is closer to the expected one. *)
1579 ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
1581 (CicSubstitution.subst s ty1),ugraph2
1582 | C.Appl (he::tl) when List.length tl > 0 ->
1583 let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
1584 let tlbody_and_type,ugraph2 =
1587 let ty,ugraph1 = type_of_aux ~logger context x ugraph in
1588 let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
1589 ((x,ty)::l,ugraph1))
1592 (* TASSI: questa c'era nel mio... ma non nel CVS... *)
1593 (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
1594 eat_prods ~subst context hetype tlbody_and_type ugraph2
1595 | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1596 | C.Const (uri,exp_named_subst) ->
1599 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1601 let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
1603 CicSubstitution.subst_vars exp_named_subst cty
1607 | C.MutInd (uri,i,exp_named_subst) ->
1610 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1612 (* TASSI: da me c'era anche questa, ma in CVS no *)
1613 let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
1614 (* fine parte dubbia *)
1616 CicSubstitution.subst_vars exp_named_subst mty
1620 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1622 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1624 (* TASSI: idem come sopra *)
1626 type_of_mutual_inductive_constr ~logger uri i j ugraph1
1629 CicSubstitution.subst_vars exp_named_subst mty
1632 | C.MutCase (uri,i,outtype,term,pl) ->
1633 let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
1634 let (need_dummy, k) =
1635 let rec guess_args context t =
1636 let outtype = CicReduction.whd ~subst context t in
1638 C.Sort _ -> (true, 0)
1639 | C.Prod (name, s, t) ->
1641 guess_args ((Some (name,(C.Decl s)))::context) t in
1643 (* last prod before sort *)
1644 match CicReduction.whd ~subst context s with
1645 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1646 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1648 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1649 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1650 when U.eq uri' uri && i' = i -> (false, 1)
1658 "Malformed case analasys' output type %s"
1659 (CicPp.ppterm outtype)))
1662 let (parameters, arguments, exp_named_subst),ugraph2 =
1663 let ty,ugraph2 = type_of_aux context term ugraph1 in
1664 match R.whd context ty with
1665 (*CSC manca il caso dei CAST *)
1666 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1667 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
1668 (*CSC: Hint: nella DTD servono per gli stylesheet. *)
1669 C.MutInd (uri',i',exp_named_subst) as typ ->
1670 if U.eq uri uri' && i = i' then
1671 ([],[],exp_named_subst),ugraph2
1676 ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1677 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1679 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1680 if U.eq uri uri' && i = i' then
1682 split tl (List.length tl - k)
1683 in (params,args,exp_named_subst),ugraph2
1688 ("Case analysys: analysed term type is %s, "^
1689 "but is expected to be (an application of) "^
1691 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1697 "analysed term %s is not an inductive one")
1698 (CicPp.ppterm term)))
1700 let (b, k) = guess_args context outsort in
1701 if not b then (b, k - 1) else (b, k) in
1702 let (parameters, arguments, exp_named_subst),ugraph2 =
1703 let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
1704 match R.whd ~subst context ty with
1705 C.MutInd (uri',i',exp_named_subst) as typ ->
1706 if U.eq uri uri' && i = i' then
1707 ([],[],exp_named_subst),ugraph2
1711 ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1712 (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1714 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1715 if U.eq uri uri' && i = i' then
1717 split tl (List.length tl - k)
1718 in (params,args,exp_named_subst),ugraph2
1722 ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1723 (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1728 "Case analysis: analysed term %s is not an inductive one"
1729 (CicPp.ppterm term)))
1732 let's control if the sort elimination is allowed:
1735 let sort_of_ind_type =
1736 if parameters = [] then
1737 C.MutInd (uri,i,exp_named_subst)
1739 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1741 let type_of_sort_of_ind_ty,ugraph3 =
1742 type_of_aux ~logger context sort_of_ind_type ugraph2 in
1744 check_allowed_sort_elimination ~logger context uri i need_dummy
1745 sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
1749 (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1750 (* let's check if the type of branches are right *)
1754 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1755 with Not_found -> assert false
1758 C.InductiveDefinition (_,_,parsno,_) -> parsno
1760 raise (TypeCheckerFailure
1761 ("Unknown mutual inductive definition:" ^
1762 UriManager.string_of_uri uri))
1764 let (_,branches_ok,ugraph5) =
1766 (fun (j,b,ugraph) p ->
1769 if parameters = [] then
1770 (C.MutConstruct (uri,i,j,exp_named_subst))
1773 (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1775 let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
1776 let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
1779 type_of_branch context parsno need_dummy outtype cons
1783 ~subst ~metasenv context ty_p ty_branch ugraph3
1787 ("#### " ^ CicPp.ppterm ty_p ^
1788 " <==> " ^ CicPp.ppterm ty_branch));
1792 ) (1,true,ugraph4) pl
1794 if not branches_ok then
1796 (TypeCheckerFailure "Case analysys: wrong branch type");
1798 if not need_dummy then outtype::arguments@[term]
1799 else outtype::arguments in
1801 if need_dummy && arguments = [] then outtype
1802 else CicReduction.head_beta_reduce (C.Appl arguments')
1806 let types_times_kl,ugraph1 =
1807 (* WAS: list rev list map *)
1809 (fun (l,ugraph) (n,k,ty,_) ->
1810 let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1811 ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
1814 let (types,kl) = List.split types_times_kl in
1815 let len = List.length types in
1818 (fun ugraph (name,x,ty,bo) ->
1820 type_of_aux ~logger (types@context) bo ugraph
1823 R.are_convertible ~subst ~metasenv (types@context)
1824 ty_bo (CicSubstitution.lift len ty) ugraph1 in
1827 let (m, eaten, context') =
1828 eat_lambdas ~subst (types @ context) (x + 1) bo
1831 let's control the guarded by
1832 destructors conditions D{f,k,x,M}
1834 if not (guarded_by_destructors context' eaten
1835 (len + eaten) kl 1 [] m) then
1838 ("Fix: not guarded by destructors"))
1843 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1845 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1846 let (_,_,ty,_) = List.nth fl i in
1851 (fun (l,ugraph) (n,ty,_) ->
1853 type_of_aux ~logger context ty ugraph in
1854 (Some (C.Name n,(C.Decl ty))::l,ugraph1)
1857 let len = List.length types in
1860 (fun ugraph (_,ty,bo) ->
1862 type_of_aux ~logger (types @ context) bo ugraph
1865 R.are_convertible ~subst ~metasenv (types @ context) ty_bo
1866 (CicSubstitution.lift len ty) ugraph1
1870 (* let's control that the returned type is coinductive *)
1871 match returns_a_coinductive context ty with
1875 ("CoFix: does not return a coinductive type"))
1878 let's control the guarded by constructors
1881 if not (guarded_by_constructors (types @ context)
1882 0 len false bo [] uri) then
1885 ("CoFix: not guarded by constructors"))
1891 (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1894 let (_,ty,_) = List.nth fl i in
1897 and check_exp_named_subst ~logger ?(subst = []) context ugraph =
1898 let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
1901 | ((uri,t) as item)::tl ->
1902 let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in
1904 CicSubstitution.subst_vars esubsts ty_uri in
1905 let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in
1907 CicReduction.are_convertible ~subst ~metasenv
1908 context typeoft typeofvar ugraph2
1911 check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3
1914 CicReduction.fdebug := 0 ;
1916 (CicReduction.are_convertible
1917 ~subst ~metasenv context typeoft typeofvar ugraph2) ;
1919 debug typeoft [typeofvar] ;
1920 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1923 check_exp_named_subst_aux ~logger [] ugraph
1925 and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph =
1926 let module C = Cic in
1927 let t1' = CicReduction.whd ~subst context t1 in
1928 let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1929 match (t1', t2') with
1930 (C.Sort s1, C.Sort s2)
1931 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1932 (* different from Coq manual!!! *)
1934 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1935 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1936 let t' = CicUniv.fresh() in
1937 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1938 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1939 C.Sort (C.Type t'),ugraph2
1940 | (C.Sort _,C.Sort (C.Type t1)) ->
1941 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1942 C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
1943 | (C.Meta _, C.Sort _) -> t2',ugraph
1944 | (C.Meta _, (C.Meta (_,_) as t))
1945 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1947 | (_,_) -> raise (TypeCheckerFailure (sprintf
1948 "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1949 (CicPp.ppterm t2')))
1951 and eat_prods ?(subst = []) context hetype l ugraph =
1952 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1956 | (hete, hety)::tl ->
1957 (match (CicReduction.whd ~subst context hetype) with
1960 CicReduction.are_convertible
1961 ~subst ~metasenv context hety s ugraph
1965 CicReduction.fdebug := -1 ;
1966 eat_prods ~subst context
1967 (CicSubstitution.subst hete t) tl ugraph1
1968 (*TASSI: not sure *)
1972 CicReduction.fdebug := 0 ;
1973 ignore (CicReduction.are_convertible
1974 ~subst ~metasenv context s hety ugraph) ;
1980 ("Appl: wrong parameter-type, expected %s, found %s")
1981 (CicPp.ppterm hetype) (CicPp.ppterm s)))
1984 raise (TypeCheckerFailure
1985 "Appl: this is not a function, it cannot be applied")
1988 and returns_a_coinductive context ty =
1989 let module C = Cic in
1990 match CicReduction.whd context ty with
1991 C.MutInd (uri,i,_) ->
1992 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1995 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1996 with Not_found -> assert false
1999 C.InductiveDefinition (itl,_,_,_) ->
2000 let (_,is_inductive,_,_) = List.nth itl i in
2001 if is_inductive then None else (Some uri)
2003 raise (TypeCheckerFailure
2004 ("Unknown mutual inductive definition:" ^
2005 UriManager.string_of_uri uri))
2007 | C.Appl ((C.MutInd (uri,i,_))::_) ->
2008 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
2010 C.InductiveDefinition (itl,_,_,_) ->
2011 let (_,is_inductive,_,_) = List.nth itl i in
2012 if is_inductive then None else (Some uri)
2014 raise (TypeCheckerFailure
2015 ("Unknown mutual inductive definition:" ^
2016 UriManager.string_of_uri uri))
2018 | C.Prod (n,so,de) ->
2019 returns_a_coinductive ((Some (n,C.Decl so))::context) de
2024 debug_print (lazy ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t)) ; flush stderr ;
2027 type_of_aux ~logger context t ugraph
2029 in debug_print (lazy "FINE TYPE_OF_AUX") ; flush stderr ; res
2032 (* is a small constructor? *)
2033 (*CSC: ottimizzare calcolando staticamente *)
2034 and is_small ~logger context paramsno c ugraph =
2035 let rec is_small_aux ~logger context c ugraph =
2036 let module C = Cic in
2037 match CicReduction.whd context c with
2039 (*CSC: [] is an empty metasenv. Is it correct? *)
2040 let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
2041 let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
2043 is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
2046 | _ -> true,ugraph (*CSC: we trust the type-checker *)
2048 let (context',dx) = split_prods context paramsno c in
2049 is_small_aux ~logger context' dx ugraph
2051 and type_of ~logger t ugraph =
2053 debug_print (lazy ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t)) ; flush stderr ;
2056 type_of_aux' ~logger [] [] t ugraph
2058 in debug_print (lazy "FINE TYPE_OF_AUX'") ; flush stderr ; res
2062 let typecheck_obj0 ~logger uri ugraph =
2063 let module C = Cic in
2065 C.Constant (_,Some te,ty,_,_) ->
2066 let _,ugraph = type_of ~logger ty ugraph in
2067 let ty_te,ugraph = type_of ~logger te ugraph in
2068 let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
2070 raise (TypeCheckerFailure
2071 ("the type of the body is not the one expected"))
2074 | C.Constant (_,None,ty,_,_) ->
2075 (* only to check that ty is well-typed *)
2076 let _,ugraph = type_of ~logger ty ugraph in
2078 | C.CurrentProof (_,conjs,te,ty,_,_) ->
2081 (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
2083 type_of_aux' ~logger metasenv context ty ugraph
2085 metasenv @ [conj],ugraph
2088 let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
2089 let type_of_te,ugraph =
2090 type_of_aux' ~logger conjs [] te ugraph
2092 let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
2094 raise (TypeCheckerFailure (sprintf
2095 "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
2096 (CicPp.ppterm type_of_te) (CicPp.ppterm ty)))
2099 | C.Variable (_,bo,ty,_,_) ->
2100 (* only to check that ty is well-typed *)
2101 let _,ugraph = type_of ~logger ty ugraph in
2105 let ty_bo,ugraph = type_of ~logger bo ugraph in
2106 let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
2108 raise (TypeCheckerFailure
2109 ("the body is not the one expected"))
2113 | (C.InductiveDefinition _ as obj) ->
2114 check_mutual_inductive_defs ~logger uri obj ugraph
2117 let module C = Cic in
2118 let module R = CicReduction in
2119 let module U = UriManager in
2120 let logger = new CicLogger.logger in
2121 (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
2122 match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
2123 CicEnvironment.CheckedObj (cobj,ugraph') ->
2124 (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*)
2126 | CicEnvironment.UncheckedObj uobj ->
2127 (* let's typecheck the uncooked object *)
2128 logger#log (`Start_type_checking uri) ;
2129 (* debug_print (lazy ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri)); *)
2130 let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
2132 CicEnvironment.set_type_checking_info uri;
2133 logger#log (`Type_checking_completed uri);
2134 match CicEnvironment.is_type_checked ~trust:false ugraph uri with
2135 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
2136 | _ -> raise CicEnvironmentError
2139 this is raised if set_type_checking_info is called on an object
2140 that has no associated universe file. If we are in univ_maker
2141 phase this is OK since univ_maker will properly commit the
2144 Invalid_argument s ->
2145 (*debug_print (lazy s);*)
2149 let typecheck_obj ~logger uri obj =
2150 let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
2151 let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
2152 CicEnvironment.add_type_checked_obj uri (obj,ugraph)
2154 (** wrappers which instantiate fresh loggers *)
2156 let type_of_aux' ?(subst = []) metasenv context t ugraph =
2157 let logger = new CicLogger.logger in
2158 type_of_aux' ~logger ~subst metasenv context t ugraph
2160 let typecheck_obj uri obj =
2161 let logger = new CicLogger.logger in
2162 typecheck_obj ~logger uri obj