1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* TODO factorize functions to frequent errors (e.g. "Unknwon mutual inductive
31 exception AssertFailure of string;;
32 exception TypeCheckerFailure of string;;
36 let rec debug_aux t i =
38 let module U = UriManager in
39 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
42 raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
45 let debug_print = prerr_endline ;;
50 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
52 raise (TypeCheckerFailure "Parameters number < left parameters number")
55 let debrujin_constructor uri number_of_types =
59 C.Rel n as t when n <= k -> t
61 raise (TypeCheckerFailure "unbound variable found in constructor type")
62 | C.Var (uri,exp_named_subst) ->
63 let exp_named_subst' =
64 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
66 C.Var (uri,exp_named_subst')
67 | C.Meta _ -> assert false
69 | C.Implicit _ as t -> t
70 | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
71 | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
72 | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
73 | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t)
74 | C.Appl l -> C.Appl (List.map (aux k) l)
75 | C.Const (uri,exp_named_subst) ->
76 let exp_named_subst' =
77 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
79 C.Const (uri,exp_named_subst')
80 | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
81 if exp_named_subst != [] then
82 raise (TypeCheckerFailure
83 ("non-empty explicit named substitution is applied to "^
84 "a mutual inductive type which is being defined")) ;
85 C.Rel (k + number_of_types - tyno) ;
86 | C.MutInd (uri',tyno,exp_named_subst) ->
87 let exp_named_subst' =
88 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
90 C.MutInd (uri',tyno,exp_named_subst')
91 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
92 let exp_named_subst' =
93 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
95 C.MutConstruct (uri,tyno,consno,exp_named_subst')
96 | C.MutCase (sp,i,outty,t,pl) ->
97 C.MutCase (sp, i, aux k outty, aux k t,
100 let len = List.length fl in
103 (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
108 let len = List.length fl in
111 (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
114 C.CoFix (i, liftedfl)
119 exception CicEnvironmentError;;
121 let rec type_of_constant uri =
122 let module C = Cic in
123 let module R = CicReduction in
124 let module U = UriManager in
126 match CicEnvironment.is_type_checked ~trust:true uri with
127 CicEnvironment.CheckedObj cobj -> cobj
128 | CicEnvironment.UncheckedObj uobj ->
129 CicLogger.log (`Start_type_checking uri) ;
130 CicUniv.directly_to_env_begin ();
131 (* let's typecheck the uncooked obj *)
133 C.Constant (_,Some te,ty,_) ->
134 let _ = type_of ty in
135 let type_of_te = type_of te in
136 if not (R.are_convertible [] type_of_te ty) then
137 raise (TypeCheckerFailure (sprintf
138 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
139 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
141 | C.Constant (_,None,ty,_) ->
142 (* only to check that ty is well-typed *)
143 let _ = type_of ty in ()
144 | C.CurrentProof (_,conjs,te,ty,_) ->
147 (fun metasenv ((_,context,ty) as conj) ->
148 ignore (type_of_aux' metasenv context ty) ;
152 let _ = type_of_aux' conjs [] ty in
153 let type_of_te = type_of_aux' conjs [] te in
154 if not (R.are_convertible [] type_of_te ty) then
155 raise (TypeCheckerFailure (sprintf
156 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
157 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
160 raise (TypeCheckerFailure
161 ("Unknown constant:" ^ U.string_of_uri uri))
163 CicEnvironment.set_type_checking_info uri ;
164 CicUniv.directly_to_env_end ();
165 CicLogger.log (`Type_checking_completed uri) ;
166 match CicEnvironment.is_type_checked ~trust:false uri with
167 CicEnvironment.CheckedObj cobj -> cobj
168 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
171 C.Constant (_,_,ty,_) -> ty
172 | C.CurrentProof (_,_,_,ty,_) -> ty
174 raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
176 and type_of_variable uri =
177 let module C = Cic in
178 let module R = CicReduction in
179 let module U = UriManager in
180 (* 0 because a variable is never cooked => no partial cooking at one level *)
181 match CicEnvironment.is_type_checked ~trust:true uri with
182 CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
183 | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
184 CicLogger.log (`Start_type_checking uri) ;
185 CicUniv.directly_to_env_begin ();
186 (* only to check that ty is well-typed *)
187 let _ = type_of ty in
191 if not (R.are_convertible [] (type_of bo) ty) then
192 raise (TypeCheckerFailure
193 ("Unknown variable:" ^ U.string_of_uri uri))
195 CicEnvironment.set_type_checking_info uri ;
196 CicUniv.directly_to_env_end ();
197 CicLogger.log (`Type_checking_completed uri) ;
200 raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
202 and does_not_occur context n nn te =
203 let module C = Cic in
204 (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
205 (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
207 match CicReduction.whd context te with
208 C.Rel m when m > n && m <= nn -> false
210 | C.Meta _ (* CSC: Are we sure? No recursion?*)
212 | C.Implicit _ -> true
214 does_not_occur context n nn te && does_not_occur context n nn ty
215 | C.Prod (name,so,dest) ->
216 does_not_occur context n nn so &&
217 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
219 | C.Lambda (name,so,dest) ->
220 does_not_occur context n nn so &&
221 does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
223 | C.LetIn (name,so,dest) ->
224 does_not_occur context n nn so &&
225 does_not_occur ((Some (name,(C.Def (so,None))))::context)
226 (n + 1) (nn + 1) dest
228 List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
229 | C.Var (_,exp_named_subst)
230 | C.Const (_,exp_named_subst)
231 | C.MutInd (_,_,exp_named_subst)
232 | C.MutConstruct (_,_,_,exp_named_subst) ->
233 List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
235 | C.MutCase (_,_,out,te,pl) ->
236 does_not_occur context n nn out && does_not_occur context n nn te &&
237 List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
239 let len = List.length fl in
240 let n_plus_len = n + len in
241 let nn_plus_len = nn + len in
243 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
246 (fun (_,_,ty,bo) i ->
247 i && does_not_occur context n nn ty &&
248 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
251 let len = List.length fl in
252 let n_plus_len = n + len in
253 let nn_plus_len = nn + len in
255 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
259 i && does_not_occur context n nn ty &&
260 does_not_occur (tys @ context) n_plus_len nn_plus_len bo
263 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
264 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
265 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
266 (*CSC strictly_positive *)
267 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
268 and weakly_positive context n nn uri te =
269 let module C = Cic in
270 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
272 C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
274 (*CSC mettere in cicSubstitution *)
275 let rec subst_inductive_type_with_dummy_mutind =
277 C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
279 | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
281 | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
282 | C.Prod (name,so,ta) ->
283 C.Prod (name, subst_inductive_type_with_dummy_mutind so,
284 subst_inductive_type_with_dummy_mutind ta)
285 | C.Lambda (name,so,ta) ->
286 C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
287 subst_inductive_type_with_dummy_mutind ta)
289 C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
290 | C.MutCase (uri,i,outtype,term,pl) ->
292 subst_inductive_type_with_dummy_mutind outtype,
293 subst_inductive_type_with_dummy_mutind term,
294 List.map subst_inductive_type_with_dummy_mutind pl)
296 C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
297 subst_inductive_type_with_dummy_mutind ty,
298 subst_inductive_type_with_dummy_mutind bo)) fl)
300 C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
301 subst_inductive_type_with_dummy_mutind ty,
302 subst_inductive_type_with_dummy_mutind bo)) fl)
303 | C.Const (uri,exp_named_subst) ->
304 let exp_named_subst' =
306 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
309 C.Const (uri,exp_named_subst')
310 | C.MutInd (uri,typeno,exp_named_subst) ->
311 let exp_named_subst' =
313 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
316 C.MutInd (uri,typeno,exp_named_subst')
317 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
318 let exp_named_subst' =
320 (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
323 C.MutConstruct (uri,typeno,consno,exp_named_subst')
326 match CicReduction.whd context te with
327 C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
328 | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
329 | C.Prod (C.Anonymous,source,dest) ->
330 strictly_positive context n nn
331 (subst_inductive_type_with_dummy_mutind source) &&
332 weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
333 (n + 1) (nn + 1) uri dest
334 | C.Prod (name,source,dest) when
335 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
336 (* dummy abstraction, so we behave as in the anonimous case *)
337 strictly_positive context n nn
338 (subst_inductive_type_with_dummy_mutind source) &&
339 weakly_positive ((Some (name,(C.Decl source)))::context)
340 (n + 1) (nn + 1) uri dest
341 | C.Prod (name,source,dest) ->
342 does_not_occur context n nn
343 (subst_inductive_type_with_dummy_mutind source)&&
344 weakly_positive ((Some (name,(C.Decl source)))::context)
345 (n + 1) (nn + 1) uri dest
347 raise (TypeCheckerFailure "Malformed inductive constructor type")
349 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
350 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
351 and instantiate_parameters params c =
352 let module C = Cic in
353 match (c,params) with
355 | (C.Prod (_,_,ta), he::tl) ->
356 instantiate_parameters tl
357 (CicSubstitution.subst he ta)
358 | (C.Cast (te,_), _) -> instantiate_parameters params te
359 | (t,l) -> raise (AssertFailure "1")
361 and strictly_positive context n nn te =
362 let module C = Cic in
363 let module U = UriManager in
364 match CicReduction.whd context te with
367 (*CSC: bisogna controllare ty????*)
368 strictly_positive context n nn te
369 | C.Prod (name,so,ta) ->
370 does_not_occur context n nn so &&
371 strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
372 | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
373 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
374 | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
375 let (ok,paramsno,ity,cl,name) =
376 match CicEnvironment.get_obj uri with
377 C.InductiveDefinition (tl,_,paramsno) ->
378 let (name,_,ity,cl) = List.nth tl i in
379 (List.length tl = 1, paramsno, ity, cl, name)
381 raise (TypeCheckerFailure
382 ("Unknown inductive type:" ^ U.string_of_uri uri))
384 let (params,arguments) = split tl paramsno in
385 let lifted_params = List.map (CicSubstitution.lift 1) params in
389 instantiate_parameters lifted_params
390 (CicSubstitution.subst_vars exp_named_subst te)
395 (fun x i -> i && does_not_occur context n nn x)
397 (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
402 ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
405 | t -> does_not_occur context n nn t
407 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
408 and are_all_occurrences_positive context uri indparamsno i n nn te =
409 let module C = Cic in
410 match CicReduction.whd context te with
411 C.Appl ((C.Rel m)::tl) when m = i ->
412 (*CSC: riscrivere fermandosi a 0 *)
413 (* let's check if the inductive type is applied at least to *)
414 (* indparamsno parameters *)
420 match CicReduction.whd context x with
421 C.Rel m when m = n - (indparamsno - k) -> k - 1
423 raise (TypeCheckerFailure
424 ("Non-positive occurence in mutual inductive definition(s) " ^
425 UriManager.string_of_uri uri))
429 List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
431 raise (TypeCheckerFailure
432 ("Non-positive occurence in mutual inductive definition(s) " ^
433 UriManager.string_of_uri uri))
434 | C.Rel m when m = i ->
435 if indparamsno = 0 then
438 raise (TypeCheckerFailure
439 ("Non-positive occurence in mutual inductive definition(s) " ^
440 UriManager.string_of_uri uri))
441 | C.Prod (C.Anonymous,source,dest) ->
442 strictly_positive context n nn source &&
443 are_all_occurrences_positive
444 ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
445 (i+1) (n + 1) (nn + 1) dest
446 | C.Prod (name,source,dest) when
447 does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
448 (* dummy abstraction, so we behave as in the anonimous case *)
449 strictly_positive context n nn source &&
450 are_all_occurrences_positive
451 ((Some (name,(C.Decl source)))::context) uri indparamsno
452 (i+1) (n + 1) (nn + 1) dest
453 | C.Prod (name,source,dest) ->
454 does_not_occur context n nn source &&
455 are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
456 uri indparamsno (i+1) (n + 1) (nn + 1) dest
459 (TypeCheckerFailure ("Malformed inductive constructor type " ^
460 (UriManager.string_of_uri uri)))
462 (* Main function to checks the correctness of a mutual *)
463 (* inductive block definition. This is the function *)
464 (* exported to the proof-engine. *)
465 and typecheck_mutual_inductive_defs uri (itl,_,indparamsno) =
466 let module U = UriManager in
467 (* let's check if the arity of the inductive types are well *)
469 List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
471 (* let's check if the types of the inductive constructors *)
472 (* are well formed. *)
473 (* In order not to use type_of_aux we put the types of the *)
474 (* mutual inductive types at the head of the types of the *)
475 (* constructors using Prods *)
476 let len = List.length itl in
478 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
484 let debrujinedte = debrujin_constructor uri len te in
487 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
490 let _ = type_of augmented_term in
491 (* let's check also the positivity conditions *)
494 (are_all_occurrences_positive tys uri indparamsno i 0 len
498 (TypeCheckerFailure ("Non positive occurence in " ^
499 U.string_of_uri uri))
506 (* Main function to checks the correctness of a mutual *)
507 (* inductive block definition. *)
508 and check_mutual_inductive_defs uri =
510 Cic.InductiveDefinition (itl, params, indparamsno) ->
511 typecheck_mutual_inductive_defs uri (itl,params,indparamsno)
513 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
514 UriManager.string_of_uri uri))
516 and type_of_mutual_inductive_defs uri i =
517 let module C = Cic in
518 let module R = CicReduction in
519 let module U = UriManager in
521 match CicEnvironment.is_type_checked ~trust:true uri with
522 CicEnvironment.CheckedObj cobj -> cobj
523 | CicEnvironment.UncheckedObj uobj ->
524 CicLogger.log (`Start_type_checking uri) ;
525 CicUniv.directly_to_env_begin ();
526 check_mutual_inductive_defs uri uobj ;
527 CicEnvironment.set_type_checking_info uri ;
528 CicUniv.directly_to_env_end ();
529 CicLogger.log (`Type_checking_completed uri) ;
530 (match CicEnvironment.is_type_checked ~trust:false uri with
531 CicEnvironment.CheckedObj cobj -> cobj
532 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
536 C.InductiveDefinition (dl,_,_) ->
537 let (_,_,arity,_) = List.nth dl i in
540 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
541 U.string_of_uri uri))
543 and type_of_mutual_inductive_constr uri i j =
544 let module C = Cic in
545 let module R = CicReduction in
546 let module U = UriManager in
548 match CicEnvironment.is_type_checked ~trust:true uri with
549 CicEnvironment.CheckedObj cobj -> cobj
550 | CicEnvironment.UncheckedObj uobj ->
551 CicLogger.log (`Start_type_checking uri) ;
552 (*CicUniv.directly_to_env_begin ();*)
553 check_mutual_inductive_defs uri uobj ;
554 CicEnvironment.set_type_checking_info uri ;
555 (*CicUniv.directly_to_env_end ();*)
556 CicLogger.log (`Type_checking_completed uri) ;
557 (match CicEnvironment.is_type_checked ~trust:false uri with
558 CicEnvironment.CheckedObj cobj -> cobj
559 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
563 C.InductiveDefinition (dl,_,_) ->
564 let (_,_,_,cl) = List.nth dl i in
565 let (_,ty) = List.nth cl (j-1) in
568 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
569 UriManager.string_of_uri uri))
571 and recursive_args context n nn te =
572 let module C = Cic in
573 match CicReduction.whd context te with
579 | C.Cast _ (*CSC ??? *) ->
580 raise (AssertFailure "3") (* due to type-checking *)
581 | C.Prod (name,so,de) ->
582 (not (does_not_occur context n nn so)) ::
583 (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
586 raise (AssertFailure "4") (* due to type-checking *)
588 | C.Const _ -> raise (AssertFailure "5")
593 | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *)
595 and get_new_safes ?(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 context uri i need_dummy ind arity1 arity2 =
1175 let module C = Cic in
1176 let module U = UriManager in
1177 match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1178 (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1179 when CicReduction.are_convertible context so1 so2 ->
1180 check_allowed_sort_elimination context uri i need_dummy
1181 (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1182 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1183 | (C.Sort C.Prop, C.Sort C.Set)
1184 | (C.Sort C.Prop, C.Sort C.CProp)
1185 | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1186 (* TASSI: da verificare *)
1187 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1188 (match CicEnvironment.get_obj uri with
1189 C.InductiveDefinition (itl,_,_) ->
1190 let (_,_,_,cl) = List.nth itl i in
1191 (* is a singleton definition or the empty proposition? *)
1192 List.length cl = 1 || List.length cl = 0
1194 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1195 UriManager.string_of_uri uri))
1197 | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1198 | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true
1199 | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1200 | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
1201 | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
1202 | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
1203 | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
1204 (* TASSI: da verificare *)
1206 (match CicEnvironment.get_obj uri with
1207 C.InductiveDefinition (itl,_,paramsno) ->
1209 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1211 let (_,_,_,cl) = List.nth itl i in
1213 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1215 raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1216 UriManager.string_of_uri uri))
1218 | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true
1219 (* TASSI: da verificare *)
1220 | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1221 let res = CicReduction.are_convertible context so ind
1224 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1225 C.Sort C.Prop -> true
1226 | (C.Sort C.Set | C.Sort C.CProp) ->
1227 (match CicEnvironment.get_obj uri with
1228 C.InductiveDefinition (itl,_,_) ->
1229 let (_,_,_,cl) = List.nth itl i in
1230 (* is a singleton definition? *)
1233 raise (TypeCheckerFailure
1234 ("Unknown mutual inductive definition:" ^
1235 UriManager.string_of_uri uri))
1239 | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
1240 when not need_dummy ->
1241 let res = CicReduction.are_convertible context so ind
1244 (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1246 | C.Sort C.Set -> true
1247 | C.Sort C.CProp -> true
1248 | C.Sort (C.Type _) ->
1249 (* TASSI: da verificare *)
1250 (match CicEnvironment.get_obj uri with
1251 C.InductiveDefinition (itl,_,paramsno) ->
1252 let (_,_,_,cl) = List.nth itl i in
1255 (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1258 (fun (_,x) i -> i && is_small tys paramsno x) cl true
1260 raise (TypeCheckerFailure
1261 ("Unknown mutual inductive definition:" ^
1262 UriManager.string_of_uri uri))
1264 | _ -> raise (AssertFailure "19")
1266 | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
1267 (* TASSI: da verificare *)
1268 CicReduction.are_convertible context so ind
1271 and type_of_branch context argsno need_dummy outtype term constype =
1272 let module C = Cic in
1273 let module R = CicReduction in
1274 match R.whd context constype with
1279 C.Appl [outtype ; term]
1280 | C.Appl (C.MutInd (_,_,_)::tl) ->
1281 let (_,arguments) = split tl argsno
1283 if need_dummy && arguments = [] then
1286 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1287 | C.Prod (name,so,de) ->
1289 match CicSubstitution.lift 1 term with
1290 C.Appl l -> C.Appl (l@[C.Rel 1])
1291 | t -> C.Appl [t ; C.Rel 1]
1293 C.Prod (C.Anonymous,so,type_of_branch
1294 ((Some (name,(C.Decl so)))::context) argsno need_dummy
1295 (CicSubstitution.lift 1 outtype) term' de)
1296 | _ -> raise (AssertFailure "20")
1298 (* check_metasenv_consistency checks that the "canonical" context of a
1299 metavariable is consitent - up to relocation via the relocation list l -
1300 with the actual context *)
1302 and check_metasenv_consistency ?(subst=[]) metasenv context canonical_context l =
1303 let module C = Cic in
1304 let module R = CicReduction in
1305 let module S = CicSubstitution in
1306 let lifted_canonical_context =
1310 | (Some (n,C.Decl t))::tl ->
1311 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1312 | (Some (n,C.Def (t,None)))::tl ->
1313 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1314 | None::tl -> None::(aux (i+1) tl)
1315 | (Some (n,C.Def (t,Some ty)))::tl ->
1316 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
1318 aux 1 canonical_context
1324 | Some t,Some (_,C.Def (ct,_)) ->
1325 if not (R.are_convertible ~subst ~metasenv context t ct) then
1326 raise (TypeCheckerFailure (sprintf
1327 "Not well typed metavariable local context: expected a term convertible with %s, found %s"
1328 (CicPp.ppterm ct) (CicPp.ppterm t)))
1329 | Some t,Some (_,C.Decl ct) ->
1330 let type_t = type_of_aux' ~subst metasenv context t in
1331 if not (R.are_convertible ~subst ~metasenv context type_t ct) then
1338 let (cc, ecco) = CicUtil.lookup_subst n subst in
1339 prerr_endline (CicPp.ppterm ecco)
1340 with CicUtil.Subst_not_found _ ->
1341 prerr_endline "Non lo trovo"
1343 raise (TypeCheckerFailure (sprintf
1344 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1345 (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t))))
1347 raise (TypeCheckerFailure
1348 "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
1349 ) l lifted_canonical_context
1351 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1352 and type_of_aux' ?(subst = []) metasenv context t =
1353 let rec type_of_aux context =
1354 let module C = Cic in
1355 let module R = CicReduction in
1356 let module S = CicSubstitution in
1357 let module U = UriManager in
1361 match List.nth context (n - 1) with
1362 Some (_,C.Decl t) -> S.lift n t
1363 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
1364 | Some (_,C.Def (bo,None)) ->
1365 debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1366 type_of_aux context (S.lift n bo)
1367 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
1370 raise (TypeCheckerFailure "unbound variable")
1372 | C.Var (uri,exp_named_subst) ->
1374 check_exp_named_subst ~subst context exp_named_subst ;
1376 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1382 let (canonical_context, term) = CicUtil.lookup_subst n subst in
1383 check_metasenv_consistency
1384 ~subst metasenv context canonical_context l;
1385 type_of_aux context (CicSubstitution.lift_meta l term)
1386 with CicUtil.Subst_not_found _ ->
1387 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1388 check_metasenv_consistency
1389 ~subst metasenv context canonical_context l;
1390 CicSubstitution.lift_meta l ty)
1391 (* TASSI: CONSTRAINTS *)
1392 | C.Sort (C.Type t) ->
1393 let t' = CicUniv.fresh() in
1394 if not (CicUniv.add_gt t' t ) then
1395 assert false (* t' is fresh! an error in CicUniv *)
1398 (* TASSI: CONSTRAINTS *)
1399 | C.Sort s -> C.Sort (C.Type (CicUniv.fresh ()))
1400 | C.Implicit _ -> raise (AssertFailure "21")
1401 | C.Cast (te,ty) as t ->
1402 let _ = type_of_aux context ty in
1403 if R.are_convertible ~subst ~metasenv context (type_of_aux context te) ty then
1406 raise (TypeCheckerFailure
1407 (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1408 | C.Prod (name,s,t) ->
1409 let sort1 = type_of_aux context s
1410 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1411 let res = sort_of_prod ~subst context (name,s) (sort1,sort2) in
1413 | C.Lambda (n,s,t) ->
1414 let sort1 = type_of_aux context s in
1415 (match R.whd ~subst context sort1 with
1420 (TypeCheckerFailure (sprintf
1421 "Not well-typed lambda-abstraction: the source %s should be a
1422 type; instead it is a term of type %s" (CicPp.ppterm s)
1423 (CicPp.ppterm sort1)))
1425 let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1427 | C.LetIn (n,s,t) ->
1428 (* only to check if s is well-typed *)
1429 let ty = type_of_aux context s in
1430 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1431 LetIn is later reduced and maybe also re-checked.
1432 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1434 (* The type of the LetIn is reduced. Much faster than the previous
1435 solution. Moreover the inferred type is probably very different
1436 from the expected one.
1437 (CicReduction.whd context
1438 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1440 (* One-step LetIn reduction. Even faster than the previous solution.
1441 Moreover the inferred type is closer to the expected one. *)
1442 (CicSubstitution.subst s
1443 (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
1444 | C.Appl (he::tl) when List.length tl > 0 ->
1445 let hetype = type_of_aux context he in
1446 let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1447 eat_prods ~subst context hetype tlbody_and_type
1448 | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1449 | C.Const (uri,exp_named_subst) ->
1451 check_exp_named_subst ~subst context exp_named_subst ;
1453 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1457 | C.MutInd (uri,i,exp_named_subst) ->
1459 check_exp_named_subst ~subst context exp_named_subst ;
1461 CicSubstitution.subst_vars exp_named_subst
1462 (type_of_mutual_inductive_defs uri i)
1466 | C.MutConstruct (uri,i,j,exp_named_subst) ->
1467 check_exp_named_subst ~subst context exp_named_subst ;
1469 CicSubstitution.subst_vars exp_named_subst
1470 (type_of_mutual_inductive_constr uri i j)
1473 | C.MutCase (uri,i,outtype,term,pl) ->
1474 let outsort = type_of_aux context outtype in
1475 let (need_dummy, k) =
1476 let rec guess_args context t =
1477 let outtype = CicReduction.whd ~subst context t in
1479 C.Sort _ -> (true, 0)
1480 | C.Prod (name, s, t) ->
1482 guess_args ((Some (name,(C.Decl s)))::context) t in
1484 (* last prod before sort *)
1485 match CicReduction.whd ~subst context s with
1486 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1487 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1489 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1490 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1491 when U.eq uri' uri && i' = i -> (false, 1)
1499 "Malformed case analasys' output type %s"
1500 (CicPp.ppterm outtype)))
1502 let (b, k) = guess_args context outsort in
1503 if not b then (b, k - 1) else (b, k) in
1504 let (parameters, arguments, exp_named_subst) =
1505 match R.whd ~subst context (type_of_aux context term) with
1506 C.MutInd (uri',i',exp_named_subst) as typ ->
1507 if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1511 "Case analysys: analysed term type is %s,
1512 but is expected to be (an application of) %s#1/%d{_}"
1513 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1514 | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1515 if U.eq uri uri' && i = i' then
1517 split tl (List.length tl - k)
1518 in params,args,exp_named_subst
1522 "Case analysys: analysed term type is %s,
1523 but is expected to be (an application of) %s#1/%d{_}"
1524 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1529 "Case analysis: analysed term %s is not an inductive one"
1530 (CicPp.ppterm term)))
1532 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1533 let sort_of_ind_type =
1534 if parameters = [] then
1535 C.MutInd (uri,i,exp_named_subst)
1537 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) in
1539 (check_allowed_sort_elimination context uri i need_dummy
1540 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1543 (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1544 (* let's check if the type of branches are right *)
1546 match CicEnvironment.get_cooked_obj ~trust:false uri with
1547 C.InductiveDefinition (_,_,parsno) -> parsno
1549 raise (TypeCheckerFailure
1550 ("Unknown mutual inductive definition:" ^
1551 UriManager.string_of_uri uri))
1553 let (_,branches_ok) =
1557 if parameters = [] then
1558 (C.MutConstruct (uri,i,j,exp_named_subst))
1561 (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) in
1566 ~subst ~metasenv context (type_of_aux context p)
1567 (type_of_branch context parsno need_dummy outtype cons
1568 (type_of_aux context cons)) in
1570 debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res
1574 if not branches_ok then
1576 (TypeCheckerFailure "Case analysys: wrong branch type");
1577 if not need_dummy then
1578 C.Appl ((outtype::arguments)@[term])
1579 else if arguments = [] then
1582 C.Appl (outtype::arguments)
1584 let types_times_kl =
1588 let _ = type_of_aux context ty in
1589 (Some (C.Name n,(C.Decl ty)),k)) fl)
1591 let (types,kl) = List.split types_times_kl in
1592 let len = List.length types in
1594 (fun (name,x,ty,bo) ->
1597 ~subst ~metasenv (types@context) (type_of_aux (types@context) bo)
1598 (CicSubstitution.lift len ty))
1601 let (m, eaten, context') =
1602 eat_lambdas ~subst (types @ context) (x + 1) bo in
1603 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1605 not (guarded_by_destructors context'
1606 eaten (len + eaten) kl 1 [] m)
1609 (TypeCheckerFailure ("Fix: not guarded by destructors"))
1612 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1614 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1615 let (_,_,ty,_) = List.nth fl i in
1622 let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1624 let len = List.length types in
1629 ~subst ~metasenv (types @ context)
1630 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1633 (* let's control that the returned type is coinductive *)
1634 match returns_a_coinductive context ty with
1638 ("CoFix: does not return a coinductive type"))
1640 (*let's control the guarded by constructors conditions C{f,M}*)
1643 (guarded_by_constructors
1644 (types @ context) 0 len false bo [] uri)
1647 (TypeCheckerFailure ("CoFix: not guarded by constructors"))
1651 (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1653 let (_,ty,_) = List.nth fl i in
1656 and check_exp_named_subst ?(subst = []) context =
1657 let rec check_exp_named_subst_aux esubsts =
1660 | ((uri,t) as item)::tl ->
1662 CicSubstitution.subst_vars esubsts (type_of_variable uri) in
1663 let typeoft = type_of_aux context t in
1664 if CicReduction.are_convertible
1665 ~subst ~metasenv context typeoft typeofvar then
1666 check_exp_named_subst_aux (esubsts@[item]) tl
1669 CicReduction.fdebug := 0 ;
1670 ignore (CicReduction.are_convertible ~subst ~metasenv context typeoft typeofvar) ;
1672 debug typeoft [typeofvar] ;
1673 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1676 check_exp_named_subst_aux []
1678 and sort_of_prod ?(subst = []) context (name,s) (t1, t2) =
1679 let module C = Cic in
1680 let t1' = CicReduction.whd ~subst context t1 in
1681 let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1682 match (t1', t2') with
1683 (C.Sort s1, C.Sort s2)
1684 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1685 (* different from Coq manual!!! *)
1687 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1688 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1689 let t' = CicUniv.fresh() in
1690 if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
1691 assert false ; (* not possible, error in CicUniv *)
1693 | (C.Sort _,C.Sort (C.Type t1)) ->
1694 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1695 C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
1696 | (C.Meta _, C.Sort _) -> t2'
1697 | (C.Meta _, (C.Meta (_,_) as t))
1698 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1700 | (_,_) -> raise (TypeCheckerFailure (sprintf
1701 "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1702 (CicPp.ppterm t2')))
1704 and eat_prods ?(subst = []) context hetype =
1705 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1709 | (hete, hety)::tl ->
1710 (match (CicReduction.whd ~subst context hetype) with
1712 if CicReduction.are_convertible ~subst ~metasenv context hety s then
1713 (CicReduction.fdebug := -1 ;
1714 eat_prods ~subst context (CicSubstitution.subst hete t) tl
1718 CicReduction.fdebug := 0 ;
1719 ignore (CicReduction.are_convertible ~subst ~metasenv context s hety) ;
1722 raise (TypeCheckerFailure (sprintf
1723 "Appl: wrong parameter-type, expected %s, found %s"
1724 (CicPp.ppterm hetype) (CicPp.ppterm s)))
1727 raise (TypeCheckerFailure
1728 "Appl: this is not a function, it cannot be applied")
1731 and returns_a_coinductive context ty =
1732 let module C = Cic in
1733 match CicReduction.whd context ty with
1734 C.MutInd (uri,i,_) ->
1735 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1736 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1737 C.InductiveDefinition (itl,_,_) ->
1738 let (_,is_inductive,_,_) = List.nth itl i in
1739 if is_inductive then None else (Some uri)
1741 raise (TypeCheckerFailure
1742 ("Unknown mutual inductive definition:" ^
1743 UriManager.string_of_uri uri))
1745 | C.Appl ((C.MutInd (uri,i,_))::_) ->
1746 (match CicEnvironment.get_obj uri with
1747 C.InductiveDefinition (itl,_,_) ->
1748 let (_,is_inductive,_,_) = List.nth itl i in
1749 if is_inductive then None else (Some uri)
1751 raise (TypeCheckerFailure
1752 ("Unknown mutual inductive definition:" ^
1753 UriManager.string_of_uri uri))
1755 | C.Prod (n,so,de) ->
1756 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1761 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1764 type_of_aux context t
1766 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
1769 (* is a small constructor? *)
1770 (*CSC: ottimizzare calcolando staticamente *)
1771 and is_small context paramsno c =
1772 let rec is_small_aux context c =
1773 let module C = Cic in
1774 match CicReduction.whd context c with
1776 (*CSC: [] is an empty metasenv. Is it correct? *)
1777 let s = type_of_aux' [] context so in
1778 (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
1779 is_small_aux ((Some (n,(C.Decl so)))::context) de
1780 | _ -> true (*CSC: we trust the type-checker *)
1782 let (context',dx) = split_prods context paramsno c in
1783 is_small_aux context' dx
1787 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1790 type_of_aux' [] [] t
1792 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
1796 (* tassi FIXME: not sure where is this called... no history here... *)
1798 let module C = Cic in
1799 let module R = CicReduction in
1800 let module U = UriManager in
1801 (*match CicEnvironment.is_type_checked ~trust:false uri with*)
1802 match CicEnvironment.is_type_checked ~trust:true uri with
1803 CicEnvironment.CheckedObj cobj -> cobj
1804 | CicEnvironment.UncheckedObj uobj ->
1805 (* let's typecheck the uncooked object *)
1806 CicLogger.log (`Start_type_checking uri) ;
1807 CicUniv.directly_to_env_begin ();
1809 C.Constant (_,Some te,ty,_) ->
1810 let _ = type_of ty in
1811 if not (R.are_convertible [] (type_of te ) ty) then
1812 raise (TypeCheckerFailure
1813 ("Unknown constant:" ^ U.string_of_uri uri))
1814 | C.Constant (_,None,ty,_) ->
1815 (* only to check that ty is well-typed *)
1816 let _ = type_of ty in ()
1817 | C.CurrentProof (_,conjs,te,ty,_) ->
1820 (fun metasenv ((_,context,ty) as conj) ->
1821 ignore (type_of_aux' metasenv context ty) ;
1825 let _ = type_of_aux' conjs [] ty in
1826 let type_of_te = type_of_aux' conjs [] te in
1827 if not (R.are_convertible [] type_of_te ty)
1829 raise (TypeCheckerFailure (sprintf
1830 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
1831 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
1833 | C.Variable (_,bo,ty,_) ->
1834 (* only to check that ty is well-typed *)
1835 let _ = type_of ty in
1839 if not (R.are_convertible [] (type_of bo) ty) then
1840 raise (TypeCheckerFailure
1841 ("Unknown variable:" ^ U.string_of_uri uri))
1843 | C.InductiveDefinition _ ->
1844 check_mutual_inductive_defs uri uobj
1846 CicEnvironment.set_type_checking_info uri ;
1847 CicUniv.directly_to_env_end ();
1848 CicLogger.log (`Type_checking_completed uri);