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
1333 raise (TypeCheckerFailure (sprintf
1334 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1335 (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
1337 raise (TypeCheckerFailure
1338 "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
1339 ) l lifted_canonical_context
1341 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1342 and type_of_aux' ?(subst = []) metasenv context t =
1343 let rec type_of_aux context =
1344 let module C = Cic in
1345 let module R = CicReduction in
1346 let module S = CicSubstitution in
1347 let module U = UriManager in
1351 match List.nth context (n - 1) with
1352 Some (_,C.Decl t) -> S.lift n t
1353 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
1354 | Some (_,C.Def (bo,None)) ->
1355 debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1356 type_of_aux context (S.lift n bo)
1357 | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
1360 raise (TypeCheckerFailure "unbound variable")
1362 | C.Var (uri,exp_named_subst) ->
1364 check_exp_named_subst ~subst context exp_named_subst ;
1366 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1372 let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
1373 check_metasenv_consistency
1374 ~subst metasenv context canonical_context l;
1375 (* assuming subst is well typed !!!!! *)
1376 CicSubstitution.lift_meta l ty
1377 (* type_of_aux context (CicSubstitution.lift_meta l term) *)
1378 with CicUtil.Subst_not_found _ ->
1379 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1380 check_metasenv_consistency
1381 ~subst metasenv context canonical_context l;
1382 CicSubstitution.lift_meta l ty)
1383 (* TASSI: CONSTRAINTS *)
1384 | C.Sort (C.Type t) ->
1385 let t' = CicUniv.fresh() in
1386 if not (CicUniv.add_gt t' t ) then
1387 assert false (* t' is fresh! an error in CicUniv *)
1390 (* TASSI: CONSTRAINTS *)
1391 | C.Sort s -> C.Sort (C.Type (CicUniv.fresh ()))
1392 | C.Implicit _ -> raise (AssertFailure "21")
1393 | C.Cast (te,ty) as t ->
1394 let _ = type_of_aux context ty in
1395 if R.are_convertible ~subst ~metasenv context (type_of_aux context te) ty then
1398 raise (TypeCheckerFailure
1399 (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1400 | C.Prod (name,s,t) ->
1401 let sort1 = type_of_aux context s
1402 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1403 let res = sort_of_prod ~subst context (name,s) (sort1,sort2) in
1405 | C.Lambda (n,s,t) ->
1406 let sort1 = type_of_aux context s in
1407 (match R.whd ~subst context sort1 with
1412 (TypeCheckerFailure (sprintf
1413 "Not well-typed lambda-abstraction: the source %s should be a
1414 type; instead it is a term of type %s" (CicPp.ppterm s)
1415 (CicPp.ppterm sort1)))
1417 let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1419 | C.LetIn (n,s,t) ->
1420 (* only to check if s is well-typed *)
1421 let ty = type_of_aux context s in
1422 (* The type of a LetIn is a LetIn. Extremely slow since the computed
1423 LetIn is later reduced and maybe also re-checked.
1424 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1426 (* The type of the LetIn is reduced. Much faster than the previous
1427 solution. Moreover the inferred type is probably very different
1428 from the expected one.
1429 (CicReduction.whd context
1430 (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1432 (* One-step LetIn reduction. Even faster than the previous solution.
1433 Moreover the inferred type is closer to the expected one. *)
1434 (CicSubstitution.subst s
1435 (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
1436 | C.Appl (he::tl) when List.length tl > 0 ->
1437 let hetype = type_of_aux context he in
1438 let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1439 eat_prods ~subst context hetype tlbody_and_type
1440 | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1441 | C.Const (uri,exp_named_subst) ->
1443 check_exp_named_subst ~subst context exp_named_subst ;
1445 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1449 | C.MutInd (uri,i,exp_named_subst) ->
1451 check_exp_named_subst ~subst context exp_named_subst ;
1453 CicSubstitution.subst_vars exp_named_subst
1454 (type_of_mutual_inductive_defs uri i)
1458 | C.MutConstruct (uri,i,j,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_constr uri i j)
1465 | C.MutCase (uri,i,outtype,term,pl) ->
1466 let outsort = type_of_aux context outtype in
1467 let (need_dummy, k) =
1468 let rec guess_args context t =
1469 let outtype = CicReduction.whd ~subst context t in
1471 C.Sort _ -> (true, 0)
1472 | C.Prod (name, s, t) ->
1474 guess_args ((Some (name,(C.Decl s)))::context) t in
1476 (* last prod before sort *)
1477 match CicReduction.whd ~subst context s with
1478 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1479 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1481 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1482 | C.Appl ((C.MutInd (uri',i',_)) :: _)
1483 when U.eq uri' uri && i' = i -> (false, 1)
1491 "Malformed case analasys' output type %s"
1492 (CicPp.ppterm outtype)))
1494 let (b, k) = guess_args context outsort in
1495 if not b then (b, k - 1) else (b, k) in
1496 let (parameters, arguments, exp_named_subst) =
1497 match R.whd ~subst context (type_of_aux context term) with
1498 C.MutInd (uri',i',exp_named_subst) as typ ->
1499 if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1503 "Case analysys: analysed term type is %s,
1504 but is expected to be (an application of) %s#1/%d{_}"
1505 (CicPp.ppterm typ) (U.string_of_uri uri) i))
1506 | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1507 if U.eq uri uri' && i = i' then
1509 split tl (List.length tl - k)
1510 in params,args,exp_named_subst
1514 "Case analysys: analysed term type is %s,
1515 but is expected to be (an application of) %s#1/%d{_}"
1516 (CicPp.ppterm typ') (U.string_of_uri uri) i))
1521 "Case analysis: analysed term %s is not an inductive one"
1522 (CicPp.ppterm term)))
1524 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1525 let sort_of_ind_type =
1526 if parameters = [] then
1527 C.MutInd (uri,i,exp_named_subst)
1529 C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) in
1531 (check_allowed_sort_elimination context uri i need_dummy
1532 sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1535 (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1536 (* let's check if the type of branches are right *)
1538 match CicEnvironment.get_cooked_obj ~trust:false uri with
1539 C.InductiveDefinition (_,_,parsno) -> parsno
1541 raise (TypeCheckerFailure
1542 ("Unknown mutual inductive definition:" ^
1543 UriManager.string_of_uri uri))
1545 let (_,branches_ok) =
1549 if parameters = [] then
1550 (C.MutConstruct (uri,i,j,exp_named_subst))
1553 (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) in
1558 ~subst ~metasenv context (type_of_aux context p)
1559 (type_of_branch context parsno need_dummy outtype cons
1560 (type_of_aux context cons)) in
1562 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
1566 if not branches_ok then
1568 (TypeCheckerFailure "Case analysys: wrong branch type");
1569 if not need_dummy then
1570 C.Appl ((outtype::arguments)@[term])
1571 else if arguments = [] then
1574 C.Appl (outtype::arguments)
1576 let types_times_kl =
1580 let _ = type_of_aux context ty in
1581 (Some (C.Name n,(C.Decl ty)),k)) fl)
1583 let (types,kl) = List.split types_times_kl in
1584 let len = List.length types in
1586 (fun (name,x,ty,bo) ->
1589 ~subst ~metasenv (types@context) (type_of_aux (types@context) bo)
1590 (CicSubstitution.lift len ty))
1593 let (m, eaten, context') =
1594 eat_lambdas ~subst (types @ context) (x + 1) bo in
1595 (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1597 not (guarded_by_destructors context'
1598 eaten (len + eaten) kl 1 [] m)
1601 (TypeCheckerFailure ("Fix: not guarded by destructors"))
1604 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1606 (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1607 let (_,_,ty,_) = List.nth fl i in
1614 let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1616 let len = List.length types in
1621 ~subst ~metasenv (types @ context)
1622 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1625 (* let's control that the returned type is coinductive *)
1626 match returns_a_coinductive context ty with
1630 ("CoFix: does not return a coinductive type"))
1632 (*let's control the guarded by constructors conditions C{f,M}*)
1635 (guarded_by_constructors
1636 (types @ context) 0 len false bo [] uri)
1639 (TypeCheckerFailure ("CoFix: not guarded by constructors"))
1643 (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1645 let (_,ty,_) = List.nth fl i in
1648 and check_exp_named_subst ?(subst = []) context =
1649 let rec check_exp_named_subst_aux esubsts =
1652 | ((uri,t) as item)::tl ->
1654 CicSubstitution.subst_vars esubsts (type_of_variable uri) in
1655 let typeoft = type_of_aux context t in
1656 if CicReduction.are_convertible
1657 ~subst ~metasenv context typeoft typeofvar then
1658 check_exp_named_subst_aux (esubsts@[item]) tl
1661 CicReduction.fdebug := 0 ;
1662 ignore (CicReduction.are_convertible ~subst ~metasenv context typeoft typeofvar) ;
1664 debug typeoft [typeofvar] ;
1665 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1668 check_exp_named_subst_aux []
1670 and sort_of_prod ?(subst = []) context (name,s) (t1, t2) =
1671 let module C = Cic in
1672 let t1' = CicReduction.whd ~subst context t1 in
1673 let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1674 match (t1', t2') with
1675 (C.Sort s1, C.Sort s2)
1676 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1677 (* different from Coq manual!!! *)
1679 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1680 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1681 let t' = CicUniv.fresh() in
1682 if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
1683 assert false ; (* not possible, error in CicUniv *)
1685 | (C.Sort _,C.Sort (C.Type t1)) ->
1686 (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1687 C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
1688 | (C.Meta _, C.Sort _) -> t2'
1689 | (C.Meta _, (C.Meta (_,_) as t))
1690 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1692 | (_,_) -> raise (TypeCheckerFailure (sprintf
1693 "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1694 (CicPp.ppterm t2')))
1696 and eat_prods ?(subst = []) context hetype =
1697 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1701 | (hete, hety)::tl ->
1702 (match (CicReduction.whd ~subst context hetype) with
1704 if CicReduction.are_convertible ~subst ~metasenv context hety s then
1705 (CicReduction.fdebug := -1 ;
1706 eat_prods ~subst context (CicSubstitution.subst hete t) tl
1710 CicReduction.fdebug := 0 ;
1711 ignore (CicReduction.are_convertible ~subst ~metasenv context s hety) ;
1714 raise (TypeCheckerFailure (sprintf
1715 "Appl: wrong parameter-type, expected %s, found %s"
1716 (CicPp.ppterm hetype) (CicPp.ppterm s)))
1719 raise (TypeCheckerFailure
1720 "Appl: this is not a function, it cannot be applied")
1723 and returns_a_coinductive context ty =
1724 let module C = Cic in
1725 match CicReduction.whd context ty with
1726 C.MutInd (uri,i,_) ->
1727 (*CSC: definire una funzioncina per questo codice sempre replicato *)
1728 (match CicEnvironment.get_cooked_obj ~trust:false uri with
1729 C.InductiveDefinition (itl,_,_) ->
1730 let (_,is_inductive,_,_) = List.nth itl i in
1731 if is_inductive then None else (Some uri)
1733 raise (TypeCheckerFailure
1734 ("Unknown mutual inductive definition:" ^
1735 UriManager.string_of_uri uri))
1737 | C.Appl ((C.MutInd (uri,i,_))::_) ->
1738 (match CicEnvironment.get_obj uri with
1739 C.InductiveDefinition (itl,_,_) ->
1740 let (_,is_inductive,_,_) = List.nth itl i in
1741 if is_inductive then None else (Some uri)
1743 raise (TypeCheckerFailure
1744 ("Unknown mutual inductive definition:" ^
1745 UriManager.string_of_uri uri))
1747 | C.Prod (n,so,de) ->
1748 returns_a_coinductive ((Some (n,C.Decl so))::context) de
1753 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1756 type_of_aux context t
1758 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
1761 (* is a small constructor? *)
1762 (*CSC: ottimizzare calcolando staticamente *)
1763 and is_small context paramsno c =
1764 let rec is_small_aux context c =
1765 let module C = Cic in
1766 match CicReduction.whd context c with
1768 (*CSC: [] is an empty metasenv. Is it correct? *)
1769 let s = type_of_aux' [] context so in
1770 (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
1771 is_small_aux ((Some (n,(C.Decl so)))::context) de
1772 | _ -> true (*CSC: we trust the type-checker *)
1774 let (context',dx) = split_prods context paramsno c in
1775 is_small_aux context' dx
1779 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1782 type_of_aux' [] [] t
1784 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
1788 (* tassi FIXME: not sure where is this called... no history here... *)
1790 let module C = Cic in
1791 let module R = CicReduction in
1792 let module U = UriManager in
1793 (*match CicEnvironment.is_type_checked ~trust:false uri with*)
1794 match CicEnvironment.is_type_checked ~trust:true uri with
1795 CicEnvironment.CheckedObj cobj -> cobj
1796 | CicEnvironment.UncheckedObj uobj ->
1797 (* let's typecheck the uncooked object *)
1798 CicLogger.log (`Start_type_checking uri) ;
1799 CicUniv.directly_to_env_begin ();
1801 C.Constant (_,Some te,ty,_) ->
1802 let _ = type_of ty in
1803 if not (R.are_convertible [] (type_of te ) ty) then
1804 raise (TypeCheckerFailure
1805 ("Unknown constant:" ^ U.string_of_uri uri))
1806 | C.Constant (_,None,ty,_) ->
1807 (* only to check that ty is well-typed *)
1808 let _ = type_of ty in ()
1809 | C.CurrentProof (_,conjs,te,ty,_) ->
1812 (fun metasenv ((_,context,ty) as conj) ->
1813 ignore (type_of_aux' metasenv context ty) ;
1817 let _ = type_of_aux' conjs [] ty in
1818 let type_of_te = type_of_aux' conjs [] te in
1819 if not (R.are_convertible [] type_of_te ty)
1821 raise (TypeCheckerFailure (sprintf
1822 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
1823 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
1825 | C.Variable (_,bo,ty,_) ->
1826 (* only to check that ty is well-typed *)
1827 let _ = type_of ty in
1831 if not (R.are_convertible [] (type_of bo) ty) then
1832 raise (TypeCheckerFailure
1833 ("Unknown variable:" ^ U.string_of_uri uri))
1835 | C.InductiveDefinition _ ->
1836 check_mutual_inductive_defs uri uobj
1838 CicEnvironment.set_type_checking_info uri ;
1839 CicUniv.directly_to_env_end ();
1840 CicLogger.log (`Type_checking_completed uri);