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 ->
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 ->
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 ->
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 ->
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)
773 let debrujinedte = debrujin_constructor uri len c in
774 recursive_args tys 0 len debrujinedte
776 let (e,safes',n',nn',x',context') =
777 get_new_safes ~subst context p c rl' safes n nn x
780 check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
781 ) (List.combine pl cl) true
782 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
783 let (tys,len,isinductive,paramsno,cl) =
784 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
786 C.InductiveDefinition (tl,_,paramsno,_) ->
787 let (_,isinductive,_,cl) = List.nth tl i in
789 List.map (fun (n,_,ty,_) ->
790 Some(Cic.Name n,(Cic.Decl ty))) tl
795 (id, snd (split_prods ~subst tys paramsno ty))) cl
797 (tys,List.length tl,isinductive,paramsno,cl')
799 raise (TypeCheckerFailure
800 ("Unknown mutual inductive definition:" ^
801 UriManager.string_of_uri uri))
803 if not isinductive then
806 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
809 (*CSC: supponiamo come prima che nessun controllo sia necessario*)
810 (*CSC: sugli argomenti di una applicazione *)
814 let debrujinedte = debrujin_constructor uri len c in
815 recursive_args tys 0 len debrujinedte
817 let (e, safes',n',nn',x',context') =
818 get_new_safes context p c rl' safes n nn x
821 check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
822 ) (List.combine pl cl) true
826 i && check_is_really_smaller_arg ~subst context n nn kl x safes p
830 let len = List.length fl in
831 let n_plus_len = n + len
832 and nn_plus_len = nn + len
833 and x_plus_len = x + len
834 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
835 and safes' = List.map (fun x -> x + len) safes in
837 (fun (_,_,ty,bo) i ->
839 check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
843 let len = List.length fl in
844 let n_plus_len = n + len
845 and nn_plus_len = nn + len
846 and x_plus_len = x + len
847 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
848 and safes' = List.map (fun x -> x + len) safes in
852 check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
856 and guarded_by_destructors ?(subst = []) context n nn kl x safes =
857 let module C = Cic in
858 let module U = UriManager in
860 C.Rel m when m > n && m <= nn -> false
862 (match List.nth context (n-1) with
863 Some (_,C.Decl _) -> true
864 | Some (_,C.Def (bo,_)) ->
865 guarded_by_destructors context m nn kl x safes
866 (CicSubstitution.lift m bo)
867 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
871 | C.Implicit _ -> true
873 guarded_by_destructors context n nn kl x safes te &&
874 guarded_by_destructors context n nn kl x safes ty
875 | C.Prod (name,so,ta) ->
876 guarded_by_destructors context n nn kl x safes so &&
877 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
878 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
879 | C.Lambda (name,so,ta) ->
880 guarded_by_destructors context n nn kl x safes so &&
881 guarded_by_destructors ((Some (name,(C.Decl so)))::context)
882 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
883 | C.LetIn (name,so,ta) ->
884 guarded_by_destructors context n nn kl x safes so &&
885 guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
886 (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
887 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
888 let k = List.nth kl (m - n - 1) in
889 if not (List.length tl > k) then false
893 i && guarded_by_destructors context n nn kl x safes param
895 check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
898 (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
900 | C.Var (_,exp_named_subst)
901 | C.Const (_,exp_named_subst)
902 | C.MutInd (_,_,exp_named_subst)
903 | C.MutConstruct (_,_,_,exp_named_subst) ->
905 (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
907 | C.MutCase (uri,i,outtype,term,pl) ->
908 (match CicReduction.whd context term with
909 C.Rel m when List.mem m safes || m = x ->
910 let (tys,len,isinductive,paramsno,cl) =
911 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
913 C.InductiveDefinition (tl,_,paramsno,_) ->
914 let len = List.length tl in
915 let (_,isinductive,_,cl) = List.nth tl i in
917 List.map (fun (n,_,ty,_) ->
918 Some(Cic.Name n,(Cic.Decl ty))) tl
923 let debrujinedty = debrujin_constructor uri len ty in
924 (id, snd (split_prods ~subst tys paramsno ty),
925 snd (split_prods ~subst tys paramsno debrujinedty)
928 (tys,len,isinductive,paramsno,cl')
930 raise (TypeCheckerFailure
931 ("Unknown mutual inductive definition:" ^
932 UriManager.string_of_uri uri))
934 if not isinductive then
935 guarded_by_destructors context n nn kl x safes outtype &&
936 guarded_by_destructors context n nn kl x safes term &&
937 (*CSC: manca ??? il controllo sul tipo di term? *)
940 i && guarded_by_destructors context n nn kl x safes p)
943 guarded_by_destructors context n nn kl x safes outtype &&
944 (*CSC: manca ??? il controllo sul tipo di term? *)
946 (fun (p,(_,c,brujinedc)) i ->
947 let rl' = recursive_args tys 0 len brujinedc in
948 let (e,safes',n',nn',x',context') =
949 get_new_safes context p c rl' safes n nn x
952 guarded_by_destructors context' n' nn' kl x' safes' e
953 ) (List.combine pl cl) true
954 | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
955 let (tys,len,isinductive,paramsno,cl) =
956 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
958 C.InductiveDefinition (tl,_,paramsno,_) ->
959 let (_,isinductive,_,cl) = List.nth tl i in
962 (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
967 (id, snd (split_prods ~subst tys paramsno ty))) cl
969 (tys,List.length tl,isinductive,paramsno,cl')
971 raise (TypeCheckerFailure
972 ("Unknown mutual inductive definition:" ^
973 UriManager.string_of_uri uri))
975 if not isinductive then
976 guarded_by_destructors context n nn kl x safes outtype &&
977 guarded_by_destructors context n nn kl x safes term &&
978 (*CSC: manca ??? il controllo sul tipo di term? *)
981 i && guarded_by_destructors context n nn kl x safes p)
984 guarded_by_destructors context n nn kl x safes outtype &&
985 (*CSC: manca ??? il controllo sul tipo di term? *)
988 i && guarded_by_destructors context n nn kl x safes t)
993 let debrujinedte = debrujin_constructor uri len c in
994 recursive_args tys 0 len debrujinedte
996 let (e, safes',n',nn',x',context') =
997 get_new_safes context p c rl' safes n nn x
1000 guarded_by_destructors context' n' nn' kl x' safes' e
1001 ) (List.combine pl cl) true
1003 guarded_by_destructors context n nn kl x safes outtype &&
1004 guarded_by_destructors context n nn kl x safes term &&
1005 (*CSC: manca ??? il controllo sul tipo di term? *)
1007 (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
1011 let len = List.length fl in
1012 let n_plus_len = n + len
1013 and nn_plus_len = nn + len
1014 and x_plus_len = x + len
1015 and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1016 and safes' = List.map (fun x -> x + len) safes in
1018 (fun (_,_,ty,bo) i ->
1019 i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1020 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1021 x_plus_len safes' bo
1023 | C.CoFix (_, fl) ->
1024 let len = List.length fl in
1025 let n_plus_len = n + len
1026 and nn_plus_len = nn + len
1027 and x_plus_len = x + len
1028 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1029 and safes' = List.map (fun x -> x + len) safes in
1033 guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1034 guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1035 x_plus_len safes' bo
1038 (* the boolean h means already protected *)
1039 (* args is the list of arguments the type of the constructor that may be *)
1040 (* found in head position must be applied to. *)
1041 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
1042 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
1043 let module C = Cic in
1044 (*CSC: There is a lot of code replication between the cases X and *)
1045 (*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
1046 (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
1047 match CicReduction.whd context te with
1048 C.Rel m when m > n && m <= nn -> h
1056 (* the term has just been type-checked *)
1057 raise (AssertFailure "17")
1058 | C.Lambda (name,so,de) ->
1059 does_not_occur context n nn so &&
1060 guarded_by_constructors ((Some (name,(C.Decl so)))::context)
1061 (n + 1) (nn + 1) h de args coInductiveTypeURI
1062 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
1064 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
1065 | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
1069 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1070 with Not_found -> assert false
1073 C.InductiveDefinition (itl,_,_,_) ->
1074 let (_,_,_,cl) = List.nth itl i in
1075 let (_,cons) = List.nth cl (j - 1) in
1076 CicSubstitution.subst_vars exp_named_subst cons
1078 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1079 UriManager.string_of_uri uri))
1081 let rec analyse_branch context ty te =
1082 match CicReduction.whd context ty with
1083 C.Meta _ -> raise (AssertFailure "34")
1087 does_not_occur context n nn te
1090 raise (AssertFailure "24")(* due to type-checking *)
1091 | C.Prod (name,so,de) ->
1092 analyse_branch ((Some (name,(C.Decl so)))::context) de te
1095 raise (AssertFailure "25")(* due to type-checking *)
1096 | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1097 when uri == coInductiveTypeURI ->
1098 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1099 | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1100 guarded_by_constructors context n nn true te tl coInductiveTypeURI
1102 does_not_occur context n nn te
1103 | C.Const _ -> raise (AssertFailure "26")
1104 | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1105 guarded_by_constructors context n nn true te [] coInductiveTypeURI
1107 does_not_occur context n nn te
1108 | C.MutConstruct _ -> raise (AssertFailure "27")
1109 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1110 (*CSC: in head position. *)
1114 raise (AssertFailure "28")(* due to type-checking *)
1116 let rec analyse_instantiated_type context ty l =
1117 match CicReduction.whd context ty with
1123 | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1124 | C.Prod (name,so,de) ->
1129 analyse_branch context so he &&
1130 analyse_instantiated_type
1131 ((Some (name,(C.Decl so)))::context) de tl
1135 raise (AssertFailure "30")(* due to type-checking *)
1138 (fun i x -> i && does_not_occur context n nn x) true l
1139 | C.Const _ -> raise (AssertFailure "31")
1142 (fun i x -> i && does_not_occur context n nn x) true l
1143 | C.MutConstruct _ -> raise (AssertFailure "32")
1144 (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1145 (*CSC: in head position. *)
1149 raise (AssertFailure "33")(* due to type-checking *)
1151 let rec instantiate_type args consty =
1154 | tlhe::tltl as l ->
1155 let consty' = CicReduction.whd context consty in
1161 let instantiated_de = CicSubstitution.subst he de in
1162 (*CSC: siamo sicuri che non sia troppo forte? *)
1163 does_not_occur context n nn tlhe &
1164 instantiate_type tl instantiated_de tltl
1166 (*CSC:We do not consider backbones with a MutCase, a *)
1167 (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1168 raise (AssertFailure "23")
1170 | [] -> analyse_instantiated_type context consty' l
1171 (* These are all the other cases *)
1173 instantiate_type args consty tl
1174 | C.Appl ((C.CoFix (_,fl))::tl) ->
1175 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1176 let len = List.length fl in
1177 let n_plus_len = n + len
1178 and nn_plus_len = nn + len
1179 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1180 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1183 i && does_not_occur context n nn ty &&
1184 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1185 args coInductiveTypeURI
1187 | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1188 List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1189 does_not_occur context n nn out &&
1190 does_not_occur context n nn te &&
1194 guarded_by_constructors context n nn h x args coInductiveTypeURI
1197 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1198 | C.Var (_,exp_named_subst)
1199 | C.Const (_,exp_named_subst) ->
1201 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1202 | C.MutInd _ -> assert false
1203 | C.MutConstruct (_,_,_,exp_named_subst) ->
1205 (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1206 | C.MutCase (_,_,out,te,pl) ->
1207 does_not_occur context n nn out &&
1208 does_not_occur context n nn te &&
1212 guarded_by_constructors context n nn h x args coInductiveTypeURI
1215 let len = List.length fl in
1216 let n_plus_len = n + len
1217 and nn_plus_len = nn + len
1218 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1219 and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1221 (fun (_,_,ty,bo) i ->
1222 i && does_not_occur context n nn ty &&
1223 does_not_occur (tys@context) n_plus_len nn_plus_len bo
1226 let len = List.length fl in
1227 let n_plus_len = n + len
1228 and nn_plus_len = nn + len
1229 (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1230 and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1233 i && does_not_occur context n nn ty &&
1234 guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1235 args coInductiveTypeURI
1238 and check_allowed_sort_elimination ~logger context uri i need_dummy ind
1239 arity1 arity2 ugraph =
1240 let module C = Cic in
1241 let module U = UriManager in
1242 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1243 (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
1244 let b,ugraph1 = CicReduction.are_convertible context so1 so2 ugraph in
1246 check_allowed_sort_elimination ~logger context uri i need_dummy
1247 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1
1250 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
1251 | (C.Sort C.Prop, C.Sort C.Set)
1252 | (C.Sort C.Prop, C.Sort C.CProp)
1253 | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1254 (* TASSI: da verificare *)
1255 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1256 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1258 C.InductiveDefinition (itl,_,_,_) ->
1259 let (_,_,_,cl) = List.nth itl i in
1260 (* is a singleton definition or the empty proposition? *)
1261 (List.length cl = 1 || List.length cl = 0) , ugraph
1263 raise (TypeCheckerFailure
1264 ("Unknown mutual inductive definition:" ^
1265 UriManager.string_of_uri uri))
1267 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
1268 | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
1269 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
1270 | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph
1271 | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
1272 | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
1273 | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
1274 (* TASSI: da verificare *)
1276 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1278 C.InductiveDefinition (itl,_,paramsno,_) ->
1280 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1282 let (_,_,_,cl) = List.nth itl i in
1284 (fun (_,x) (i,ugraph) ->
1286 is_small ~logger tys paramsno x ugraph
1291 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1292 UriManager.string_of_uri uri))
1294 | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
1295 (* TASSI: da verificare *)
1296 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1297 let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1301 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1302 C.Sort C.Prop -> true,ugraph1
1303 | (C.Sort C.Set | C.Sort C.CProp) ->
1304 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1306 C.InductiveDefinition (itl,_,_,_) ->
1307 let (_,_,_,cl) = List.nth itl i in
1308 (* is a singleton definition? *)
1309 List.length cl = 1,ugraph1
1311 raise (TypeCheckerFailure
1312 ("Unknown mutual inductive definition:" ^
1313 UriManager.string_of_uri uri))
1315 | _ -> false,ugraph1
1317 | ((C.Sort C.Set, C.Prod (name,so,ta))
1318 | (C.Sort C.CProp, C.Prod (name,so,ta)))
1319 when not need_dummy ->
1320 let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1324 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1326 | C.Sort C.Set -> true,ugraph1
1327 | C.Sort C.CProp -> true,ugraph1
1328 | C.Sort (C.Type _) ->
1329 (* TASSI: da verificare *)
1330 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1332 C.InductiveDefinition (itl,_,paramsno,_) ->
1333 let (_,_,_,cl) = List.nth itl i in
1336 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1339 (fun (_,x) (i,ugraph) ->
1341 is_small ~logger tys paramsno x ugraph
1344 ) cl (true,ugraph1))
1346 raise (TypeCheckerFailure
1347 ("Unknown mutual inductive definition:" ^
1348 UriManager.string_of_uri uri))
1350 | _ -> raise (AssertFailure "19")
1352 | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
1353 (* TASSI: da verificare *)
1354 CicReduction.are_convertible context so ind ugraph
1355 | (_,_) -> false,ugraph
1357 and type_of_branch context argsno need_dummy outtype term constype =
1358 let module C = Cic in
1359 let module R = CicReduction in
1360 match R.whd context constype with
1365 C.Appl [outtype ; term]
1366 | C.Appl (C.MutInd (_,_,_)::tl) ->
1367 let (_,arguments) = split tl argsno
1369 if need_dummy && arguments = [] then
1372 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1373 | C.Prod (name,so,de) ->
1375 match CicSubstitution.lift 1 term with
1376 C.Appl l -> C.Appl (l@[C.Rel 1])
1377 | t -> C.Appl [t ; C.Rel 1]
1379 C.Prod (C.Anonymous,so,type_of_branch
1380 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1381 (CicSubstitution.lift 1 outtype) term' de)
1382 | _ -> raise (AssertFailure "20")
1384 (* check_metasenv_consistency checks that the "canonical" context of a
1385 metavariable is consitent - up to relocation via the relocation list l -
1386 with the actual context *)
1389 and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
1390 canonical_context l ugraph
1392 let module C = Cic in
1393 let module R = CicReduction in
1394 let module S = CicSubstitution in
1395 let lifted_canonical_context =
1399 | (Some (n,C.Decl t))::tl ->
1400 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1401 | (Some (n,C.Def (t,None)))::tl ->
1402 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1403 | None::tl -> None::(aux (i+1) tl)
1404 | (Some (n,C.Def (t,Some ty)))::tl ->
1405 (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)
1407 aux 1 canonical_context
1413 | Some t,Some (_,C.Def (ct,_)) ->
1415 R.are_convertible ~subst ~metasenv context t ct ugraph
1420 (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))
1423 | Some t,Some (_,C.Decl ct) ->
1424 let type_t,ugraph1 =
1425 type_of_aux' ~logger ~subst metasenv context t ugraph
1428 R.are_convertible ~subst ~metasenv context type_t ct ugraph1
1431 raise (TypeCheckerFailure
1432 (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1433 (CicPp.ppterm ct) (CicPp.ppterm t)
1434 (CicPp.ppterm type_t)))
1438 raise (TypeCheckerFailure
1439 ("Not well typed metavariable local context: "^
1440 "an hypothesis, that is not hidden, is not instantiated"))
1441 ) ugraph l lifted_canonical_context
1445 type_of_aux' is just another name (with a different scope)
1449 and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
1450 let rec type_of_aux ~logger context t ugraph =
1451 let module C = Cic in
1452 let module R = CicReduction in
1453 let module S = CicSubstitution in
1454 let module U = UriManager in
1458 match List.nth context (n - 1) with
1459 Some (_,C.Decl t) -> S.lift n t,ugraph
1460 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
1461 | Some (_,C.Def (bo,None)) ->
1462 debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1463 type_of_aux ~logger context (S.lift n bo) ugraph
1465 (TypeCheckerFailure "Reference to deleted hypothesis")
1468 raise (TypeCheckerFailure "unbound variable")
1470 | C.Var (uri,exp_named_subst) ->
1473 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1475 let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
1476 let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
1481 let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
1483 check_metasenv_consistency ~logger
1484 ~subst metasenv context canonical_context l ugraph
1486 (* assuming subst is well typed !!!!! *)
1487 ((CicSubstitution.subst_meta l ty), ugraph1)
1488 (* type_of_aux context (CicSubstitution.subst_meta l term) *)
1489 with CicUtil.Subst_not_found _ ->
1490 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1492 check_metasenv_consistency ~logger
1493 ~subst metasenv context canonical_context l ugraph
1495 ((CicSubstitution.subst_meta l ty),ugraph1))
1496 (* TASSI: CONSTRAINTS *)
1497 | C.Sort (C.Type t) ->
1498 let t' = CicUniv.fresh() in
1499 let ugraph1 = CicUniv.add_gt t' t ugraph in
1500 (C.Sort (C.Type t')),ugraph1
1501 (* TASSI: CONSTRAINTS *)
1502 | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
1503 | C.Implicit _ -> raise (AssertFailure "21")
1504 | C.Cast (te,ty) as t ->
1505 let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1506 let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
1508 R.are_convertible ~subst ~metasenv context ty_te ty ugraph2
1513 raise (TypeCheckerFailure
1514 (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1515 | C.Prod (name,s,t) ->
1516 let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1518 type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t ugraph1
1520 sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2
1521 | C.Lambda (n,s,t) ->
1522 let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1523 (match R.whd ~subst context sort1 with
1528 (TypeCheckerFailure (sprintf
1529 "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
1530 (CicPp.ppterm sort1)))
1533 type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
1535 (C.Prod (n,s,type2)),ugraph2
1536 | C.LetIn (n,s,t) ->
1537 (* only to check if s is well-typed *)
1538 let ty,ugraph1 = type_of_aux ~logger context s ugraph in
1539 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1540 LetIn is later reduced and maybe also re-checked.
1541 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1543 (* The type of the LetIn is reduced. Much faster than the previous
1544 solution. Moreover the inferred type is probably very different
1545 from the expected one.
1546 (CicReduction.whd context
1547 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1549 (* One-step LetIn reduction. Even faster than the previous solution.
1550 Moreover the inferred type is closer to the expected one. *)
1553 ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
1555 (CicSubstitution.subst s ty1),ugraph2
1556 | C.Appl (he::tl) when List.length tl > 0 ->
1557 let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
1558 let tlbody_and_type,ugraph2 =
1561 let ty,ugraph1 = type_of_aux ~logger context x ugraph in
1562 let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
1563 ((x,ty)::l,ugraph1))
1566 (* TASSI: questa c'era nel mio... ma non nel CVS... *)
1567 (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
1568 eat_prods ~subst context hetype tlbody_and_type ugraph2
1569 | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1570 | C.Const (uri,exp_named_subst) ->
1573 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1575 let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
1577 CicSubstitution.subst_vars exp_named_subst cty
1581 | C.MutInd (uri,i,exp_named_subst) ->
1584 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1586 (* TASSI: da me c'era anche questa, ma in CVS no *)
1587 let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
1588 (* fine parte dubbia *)
1590 CicSubstitution.subst_vars exp_named_subst mty
1594 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1596 check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1598 (* TASSI: idem come sopra *)
1600 type_of_mutual_inductive_constr ~logger uri i j ugraph1
1603 CicSubstitution.subst_vars exp_named_subst mty
1606 | C.MutCase (uri,i,outtype,term,pl) ->
1607 let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
1608 let (need_dummy, k) =
1609 let rec guess_args context t =
1610 let outtype = CicReduction.whd ~subst context t in
1612 C.Sort _ -> (true, 0)
1613 | C.Prod (name, s, t) ->
1615 guess_args ((Some (name,(C.Decl s)))::context) t in
1617 (* last prod before sort *)
1618 match CicReduction.whd ~subst context s with
1619 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1620 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1622 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1623 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1624 when U.eq uri' uri && i' = i -> (false, 1)
1632 "Malformed case analasys' output type %s"
1633 (CicPp.ppterm outtype)))
1636 let (parameters, arguments, exp_named_subst),ugraph2 =
1637 let ty,ugraph2 = type_of_aux context term ugraph1 in
1638 match R.whd context ty with
1639 (*CSC manca il caso dei CAST *)
1640 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1641 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
1642 (*CSC: Hint: nella DTD servono per gli stylesheet. *)
1643 C.MutInd (uri',i',exp_named_subst) as typ ->
1644 if U.eq uri uri' && i = i' then
1645 ([],[],exp_named_subst),ugraph2
1650 ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1651 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1653 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1654 if U.eq uri uri' && i = i' then
1656 split tl (List.length tl - k)
1657 in (params,args,exp_named_subst),ugraph2
1662 ("Case analysys: analysed term type is %s, "^
1663 "but is expected to be (an application of) "^
1665 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1671 "analysed term %s is not an inductive one")
1672 (CicPp.ppterm term)))
1674 let (b, k) = guess_args context outsort in
1675 if not b then (b, k - 1) else (b, k) in
1676 let (parameters, arguments, exp_named_subst),ugraph2 =
1677 let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
1678 match R.whd ~subst context ty with
1679 C.MutInd (uri',i',exp_named_subst) as typ ->
1680 if U.eq uri uri' && i = i' then
1681 ([],[],exp_named_subst),ugraph2
1685 ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1686 (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1688 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1689 if U.eq uri uri' && i = i' then
1691 split tl (List.length tl - k)
1692 in (params,args,exp_named_subst),ugraph2
1696 ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1697 (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1702 "Case analysis: analysed term %s is not an inductive one"
1703 (CicPp.ppterm term)))
1706 let's control if the sort elimination is allowed:
1709 let sort_of_ind_type =
1710 if parameters = [] then
1711 C.MutInd (uri,i,exp_named_subst)
1713 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1715 let type_of_sort_of_ind_ty,ugraph3 =
1716 type_of_aux ~logger context sort_of_ind_type ugraph2 in
1718 check_allowed_sort_elimination ~logger context uri i need_dummy
1719 sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
1723 (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1724 (* let's check if the type of branches are right *)
1728 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1729 with Not_found -> assert false
1732 C.InductiveDefinition (_,_,parsno,_) -> parsno
1734 raise (TypeCheckerFailure
1735 ("Unknown mutual inductive definition:" ^
1736 UriManager.string_of_uri uri))
1738 let (_,branches_ok,ugraph5) =
1740 (fun (j,b,ugraph) p ->
1743 if parameters = [] then
1744 (C.MutConstruct (uri,i,j,exp_named_subst))
1747 (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1749 let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
1750 let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
1753 type_of_branch context parsno need_dummy outtype cons
1757 ~subst ~metasenv context ty_p ty_branch ugraph3
1761 ("#### " ^ CicPp.ppterm ty_p ^
1762 " <==> " ^ CicPp.ppterm ty_branch);
1766 ) (1,true,ugraph4) pl
1768 if not branches_ok then
1770 (TypeCheckerFailure "Case analysys: wrong branch type");
1772 if not need_dummy then outtype::arguments@[term]
1773 else outtype::arguments in
1775 if arguments = [] then outtype
1776 else CicReduction.head_beta_reduce (C.Appl arguments)
1780 let types_times_kl,ugraph1 =
1781 (* WAS: list rev list map *)
1783 (fun (l,ugraph) (n,k,ty,_) ->
1784 let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1785 ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
1788 let (types,kl) = List.split types_times_kl in
1789 let len = List.length types in
1792 (fun ugraph (name,x,ty,bo) ->
1794 type_of_aux ~logger (types@context) bo ugraph
1797 R.are_convertible ~subst ~metasenv (types@context)
1798 ty_bo (CicSubstitution.lift len ty) ugraph1 in
1801 let (m, eaten, context') =
1802 eat_lambdas ~subst (types @ context) (x + 1) bo
1805 let's control the guarded by
1806 destructors conditions D{f,k,x,M}
1808 if not (guarded_by_destructors context' eaten
1809 (len + eaten) kl 1 [] m) then
1812 ("Fix: not guarded by destructors"))
1817 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1819 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1820 let (_,_,ty,_) = List.nth fl i in
1825 (fun (l,ugraph) (n,ty,_) ->
1827 type_of_aux ~logger context ty ugraph in
1828 (Some (C.Name n,(C.Decl ty))::l,ugraph1)
1831 let len = List.length types in
1834 (fun ugraph (_,ty,bo) ->
1836 type_of_aux ~logger (types @ context) bo ugraph
1839 R.are_convertible ~subst ~metasenv (types @ context) ty_bo
1840 (CicSubstitution.lift len ty) ugraph1
1844 (* let's control that the returned type is coinductive *)
1845 match returns_a_coinductive context ty with
1849 ("CoFix: does not return a coinductive type"))
1852 let's control the guarded by constructors
1855 if not (guarded_by_constructors (types @ context)
1856 0 len false bo [] uri) then
1859 ("CoFix: not guarded by constructors"))
1865 (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1868 let (_,ty,_) = List.nth fl i in
1871 and check_exp_named_subst ~logger ?(subst = []) context ugraph =
1872 let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
1875 | ((uri,t) as item)::tl ->
1876 let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in
1878 CicSubstitution.subst_vars esubsts ty_uri in
1879 let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in
1881 CicReduction.are_convertible ~subst ~metasenv
1882 context typeoft typeofvar ugraph2
1885 check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3
1888 CicReduction.fdebug := 0 ;
1890 (CicReduction.are_convertible
1891 ~subst ~metasenv context typeoft typeofvar ugraph2) ;
1893 debug typeoft [typeofvar] ;
1894 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1897 check_exp_named_subst_aux ~logger [] ugraph
1899 and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph =
1900 let module C = Cic in
1901 let t1' = CicReduction.whd ~subst context t1 in
1902 let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1903 match (t1', t2') with
1904 (C.Sort s1, C.Sort s2)
1905 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1906 (* different from Coq manual!!! *)
1908 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1909 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1910 let t' = CicUniv.fresh() in
1911 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1912 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1913 C.Sort (C.Type t'),ugraph2
1914 | (C.Sort _,C.Sort (C.Type t1)) ->
1915 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1916 C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
1917 | (C.Meta _, C.Sort _) -> t2',ugraph
1918 | (C.Meta _, (C.Meta (_,_) as t))
1919 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1921 | (_,_) -> raise (TypeCheckerFailure (sprintf
1922 "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1923 (CicPp.ppterm t2')))
1925 and eat_prods ?(subst = []) context hetype l ugraph =
1926 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1930 | (hete, hety)::tl ->
1931 (match (CicReduction.whd ~subst context hetype) with
1934 CicReduction.are_convertible
1935 ~subst ~metasenv context hety s ugraph
1939 CicReduction.fdebug := -1 ;
1940 eat_prods ~subst context
1941 (CicSubstitution.subst hete t) tl ugraph1
1942 (*TASSI: not sure *)
1946 CicReduction.fdebug := 0 ;
1947 ignore (CicReduction.are_convertible
1948 ~subst ~metasenv context s hety ugraph) ;
1954 ("Appl: wrong parameter-type, expected %s, found %s")
1955 (CicPp.ppterm hetype) (CicPp.ppterm s)))
1958 raise (TypeCheckerFailure
1959 "Appl: this is not a function, it cannot be applied")
1962 and returns_a_coinductive context ty =
1963 let module C = Cic in
1964 match CicReduction.whd context ty with
1965 C.MutInd (uri,i,_) ->
1966 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1969 CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1970 with Not_found -> assert false
1973 C.InductiveDefinition (itl,_,_,_) ->
1974 let (_,is_inductive,_,_) = List.nth itl i in
1975 if is_inductive then None else (Some uri)
1977 raise (TypeCheckerFailure
1978 ("Unknown mutual inductive definition:" ^
1979 UriManager.string_of_uri uri))
1981 | C.Appl ((C.MutInd (uri,i,_))::_) ->
1982 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1984 C.InductiveDefinition (itl,_,_,_) ->
1985 let (_,is_inductive,_,_) = List.nth itl i in
1986 if is_inductive then None else (Some uri)
1988 raise (TypeCheckerFailure
1989 ("Unknown mutual inductive definition:" ^
1990 UriManager.string_of_uri uri))
1992 | C.Prod (n,so,de) ->
1993 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1998 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
2001 type_of_aux ~logger context t ugraph
2003 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
2006 (* is a small constructor? *)
2007 (*CSC: ottimizzare calcolando staticamente *)
2008 and is_small ~logger context paramsno c ugraph =
2009 let rec is_small_aux ~logger context c ugraph =
2010 let module C = Cic in
2011 match CicReduction.whd context c with
2013 (*CSC: [] is an empty metasenv. Is it correct? *)
2014 let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
2015 let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
2017 is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
2020 | _ -> true,ugraph (*CSC: we trust the type-checker *)
2022 let (context',dx) = split_prods context paramsno c in
2023 is_small_aux ~logger context' dx ugraph
2025 and type_of ~logger t ugraph =
2027 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
2030 type_of_aux' ~logger [] [] t ugraph
2032 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
2036 let typecheck_obj0 ~logger uri ugraph =
2037 let module C = Cic in
2039 C.Constant (_,Some te,ty,_,_) ->
2040 let _,ugraph = type_of ~logger ty ugraph in
2041 let ty_te,ugraph = type_of ~logger te ugraph in
2042 let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
2044 raise (TypeCheckerFailure
2045 ("the type of the body is not the one expected"))
2048 | C.Constant (_,None,ty,_,_) ->
2049 (* only to check that ty is well-typed *)
2050 let _,ugraph = type_of ~logger ty ugraph in
2052 | C.CurrentProof (_,conjs,te,ty,_,_) ->
2055 (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
2057 type_of_aux' ~logger metasenv context ty ugraph
2059 metasenv @ [conj],ugraph
2062 let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
2063 let type_of_te,ugraph =
2064 type_of_aux' ~logger conjs [] te ugraph
2066 let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
2068 raise (TypeCheckerFailure (sprintf
2069 "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
2070 (CicPp.ppterm type_of_te) (CicPp.ppterm ty)))
2073 | C.Variable (_,bo,ty,_,_) ->
2074 (* only to check that ty is well-typed *)
2075 let _,ugraph = type_of ~logger ty ugraph in
2079 let ty_bo,ugraph = type_of ~logger bo ugraph in
2080 let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
2082 raise (TypeCheckerFailure
2083 ("the body is not the one expected"))
2087 | (C.InductiveDefinition _ as obj) ->
2088 check_mutual_inductive_defs ~logger uri obj ugraph
2091 let module C = Cic in
2092 let module R = CicReduction in
2093 let module U = UriManager in
2094 let logger = new CicLogger.logger in
2095 (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
2096 match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
2097 CicEnvironment.CheckedObj (cobj,ugraph') ->
2098 (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
2100 | CicEnvironment.UncheckedObj uobj ->
2101 (* let's typecheck the uncooked object *)
2102 logger#log (`Start_type_checking uri) ;
2103 (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
2104 let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
2106 CicEnvironment.set_type_checking_info uri;
2107 logger#log (`Type_checking_completed uri);
2108 match CicEnvironment.is_type_checked ~trust:false ugraph uri with
2109 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
2110 | _ -> raise CicEnvironmentError
2113 this is raised if set_type_checking_info is called on an object
2114 that has no associated universe file. If we are in univ_maker
2115 phase this is OK since univ_maker will properly commit the
2118 Invalid_argument s ->
2123 let typecheck_obj ~logger uri obj =
2124 let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
2125 let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
2126 CicEnvironment.add_type_checked_obj uri (obj,ugraph)
2128 (** wrappers which instantiate fresh loggers *)
2130 let type_of_aux' ?(subst = []) metasenv context t ugraph =
2131 let logger = new CicLogger.logger in
2132 type_of_aux' ~logger ~subst metasenv context t ugraph
2134 let typecheck_obj uri obj =
2135 let logger = new CicLogger.logger in
2136 typecheck_obj ~logger uri obj