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