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 exception Impossible of int;;
27 exception NotWellTyped of string;;
28 exception WrongUriToConstant of string;;
29 exception WrongUriToVariable of string;;
30 exception WrongUriToMutualInductiveDefinitions of string;;
31 exception ListTooShort;;
32 exception RelToHiddenHypothesis;;
34 let syntactic_equality_add_time = ref 0.0;;
35 let type_of_aux'_add_time = ref 0.0;;
36 let number_new_type_of_aux'_double_work = ref 0;;
37 let number_new_type_of_aux' = ref 0;;
38 let number_new_type_of_aux'_prop = ref 0;;
40 let double_work = ref 0;;
42 let xxx_type_of_aux' m c t =
43 let t1 = Sys.time () in
44 let res = CicTypeChecker.type_of_aux' m c t in
45 let t2 = Sys.time () in
46 type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
50 type types = {synthesized : Cic.term ; expected : Cic.term option};;
52 (* does_not_occur n te *)
53 (* returns [true] if [Rel n] does not occur in [te] *)
54 let rec does_not_occur n =
57 C.Rel m when m = n -> false
63 does_not_occur n te && does_not_occur n ty
64 | C.Prod (name,so,dest) ->
65 does_not_occur n so &&
66 does_not_occur (n + 1) dest
67 | C.Lambda (name,so,dest) ->
68 does_not_occur n so &&
69 does_not_occur (n + 1) dest
70 | C.LetIn (name,so,dest) ->
71 does_not_occur n so &&
72 does_not_occur (n + 1) dest
74 List.fold_right (fun x i -> i && does_not_occur n x) l true
75 | C.Var (_,exp_named_subst)
76 | C.Const (_,exp_named_subst)
77 | C.MutInd (_,_,exp_named_subst)
78 | C.MutConstruct (_,_,_,exp_named_subst) ->
79 List.fold_right (fun (_,x) i -> i && does_not_occur n x)
81 | C.MutCase (_,_,out,te,pl) ->
82 does_not_occur n out && does_not_occur n te &&
83 List.fold_right (fun x i -> i && does_not_occur n x) pl true
85 let len = List.length fl in
86 let n_plus_len = n + len in
88 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
92 i && does_not_occur n ty &&
93 does_not_occur n_plus_len bo
96 let len = List.length fl in
97 let n_plus_len = n + len in
99 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
103 i && does_not_occur n ty &&
104 does_not_occur n_plus_len bo
108 (*CSC: potrebbe creare applicazioni di applicazioni *)
109 (*CSC: ora non e' piu' head, ma completa!!! *)
110 let rec head_beta_reduce =
111 let module S = CicSubstitution in
112 let module C = Cic in
115 | C.Var (uri,exp_named_subst) ->
116 let exp_named_subst' =
117 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
119 C.Var (uri,exp_named_subst)
123 (function None -> None | Some t -> Some (head_beta_reduce t)) l
126 | C.Implicit -> assert false
128 C.Cast (head_beta_reduce te, head_beta_reduce ty)
130 C.Prod (n, head_beta_reduce s, head_beta_reduce t)
131 | C.Lambda (n,s,t) ->
132 C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
134 C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
135 | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
136 let he' = S.subst he t in
140 head_beta_reduce (C.Appl (he'::tl))
142 C.Appl (List.map head_beta_reduce l)
143 | C.Const (uri,exp_named_subst) ->
144 let exp_named_subst' =
145 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
147 C.Const (uri,exp_named_subst')
148 | C.MutInd (uri,i,exp_named_subst) ->
149 let exp_named_subst' =
150 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
152 C.MutInd (uri,i,exp_named_subst')
153 | C.MutConstruct (uri,i,j,exp_named_subst) ->
154 let exp_named_subst' =
155 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
157 C.MutConstruct (uri,i,j,exp_named_subst')
158 | C.MutCase (sp,i,outt,t,pl) ->
159 C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t,
160 List.map head_beta_reduce pl)
164 (function (name,i,ty,bo) ->
165 name,i,head_beta_reduce ty,head_beta_reduce bo
172 (function (name,ty,bo) ->
173 name,head_beta_reduce ty,head_beta_reduce bo
179 (* syntactic_equality up to the *)
180 (* distinction between fake dependent products *)
181 (* and non-dependent products, alfa-conversion *)
182 (*CSC: must alfa-conversion be considered or not? *)
183 let syntactic_equality t t' =
184 let module C = Cic in
185 let rec syntactic_equality t t' =
189 C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
190 UriManager.eq uri uri' &&
191 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
192 | C.Cast (te,ty), C.Cast (te',ty') ->
193 syntactic_equality te te' &&
194 syntactic_equality ty ty'
195 | C.Prod (_,s,t), C.Prod (_,s',t') ->
196 syntactic_equality s s' &&
197 syntactic_equality t t'
198 | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
199 syntactic_equality s s' &&
200 syntactic_equality t t'
201 | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
202 syntactic_equality s s' &&
203 syntactic_equality t t'
204 | C.Appl l, C.Appl l' ->
205 List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
206 | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
207 UriManager.eq uri uri' &&
208 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
209 | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
210 UriManager.eq uri uri' && i = i' &&
211 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
212 | C.MutConstruct (uri,i,j,exp_named_subst),
213 C.MutConstruct (uri',i',j',exp_named_subst') ->
214 UriManager.eq uri uri' && i = i' && j = j' &&
215 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
216 | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
217 UriManager.eq sp sp' && i = i' &&
218 syntactic_equality outt outt' &&
219 syntactic_equality t t' &&
221 (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
222 | C.Fix (i,fl), C.Fix (i',fl') ->
225 (fun b (_,i,ty,bo) (_,i',ty',bo') ->
227 syntactic_equality ty ty' &&
228 syntactic_equality bo bo') true fl fl'
229 | C.CoFix (i,fl), C.CoFix (i',fl') ->
232 (fun b (_,ty,bo) (_,ty',bo') ->
234 syntactic_equality ty ty' &&
235 syntactic_equality bo bo') true fl fl'
236 | _, _ -> false (* we already know that t != t' *)
237 and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
239 (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
240 exp_named_subst1 exp_named_subst2
243 syntactic_equality t t'
248 let xxx_syntactic_equality t t' =
249 let t1 = Sys.time () in
250 let res = syntactic_equality t t' in
251 let t2 = Sys.time () in
252 syntactic_equality_add_time := !syntactic_equality_add_time +. t2 -. t1 ;
260 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
261 | (_,_) -> raise ListTooShort
264 let type_of_constant uri =
265 let module C = Cic in
266 let module R = CicReduction in
267 let module U = UriManager in
269 match CicEnvironment.is_type_checked uri with
270 CicEnvironment.CheckedObj cobj -> cobj
271 | CicEnvironment.UncheckedObj uobj ->
272 raise (NotWellTyped "Reference to an unchecked constant")
275 C.Constant (_,_,ty,_) -> ty
276 | C.CurrentProof (_,_,_,ty,_) -> ty
277 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
280 let type_of_variable uri =
281 let module C = Cic in
282 let module R = CicReduction in
283 let module U = UriManager in
284 match CicEnvironment.is_type_checked uri with
285 CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
286 | CicEnvironment.UncheckedObj (C.Variable _) ->
287 raise (NotWellTyped "Reference to an unchecked variable")
288 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
291 let type_of_mutual_inductive_defs uri i =
292 let module C = Cic in
293 let module R = CicReduction in
294 let module U = UriManager in
296 match CicEnvironment.is_type_checked uri with
297 CicEnvironment.CheckedObj cobj -> cobj
298 | CicEnvironment.UncheckedObj uobj ->
299 raise (NotWellTyped "Reference to an unchecked inductive type")
302 C.InductiveDefinition (dl,_,_) ->
303 let (_,_,arity,_) = List.nth dl i in
305 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
308 let type_of_mutual_inductive_constr uri i j =
309 let module C = Cic in
310 let module R = CicReduction in
311 let module U = UriManager in
313 match CicEnvironment.is_type_checked uri with
314 CicEnvironment.CheckedObj cobj -> cobj
315 | CicEnvironment.UncheckedObj uobj ->
316 raise (NotWellTyped "Reference to an unchecked constructor")
319 C.InductiveDefinition (dl,_,_) ->
320 let (_,_,_,cl) = List.nth dl i in
321 let (_,ty) = List.nth cl (j-1) in
323 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
331 let hash = Hashtbl.hash
335 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
336 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
337 (* Coscoy's double type-inference algorithm *)
338 (* It computes the inner-types of every subterm of [t], *)
339 (* even when they are not needed to compute the types *)
340 (* of other terms. *)
341 let rec type_of_aux context t expectedty =
342 let module C = Cic in
343 let module R = CicReduction in
344 let module S = CicSubstitution in
345 let module U = UriManager in
350 match List.nth context (n - 1) with
351 Some (_,C.Decl t) -> S.lift n t
352 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
353 | Some (_,C.Def (bo,None)) ->
354 type_of_aux context (S.lift n bo) expectedty
355 | None -> raise RelToHiddenHypothesis
357 _ -> raise (NotWellTyped "Not a close term")
359 | C.Var (uri,exp_named_subst) ->
360 visit_exp_named_subst context uri exp_named_subst ;
361 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
363 (* Let's visit all the subterms that will not be visited later *)
364 let (_,canonical_context,_) =
365 List.find (function (m,_,_) -> n = m) metasenv
367 let lifted_canonical_context =
371 | (Some (n,C.Decl t))::tl ->
372 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
373 | (Some (n,C.Def (t,None)))::tl ->
374 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::
376 | None::tl -> None::(aux (i+1) tl)
377 | (Some (_,C.Def (_,Some _)))::_ -> assert false
379 aux 1 canonical_context
386 | Some t,Some (_,C.Def (ct,_)) ->
389 (xxx_type_of_aux' metasenv context ct)
391 (* Maybe I am a bit too paranoid, because *)
392 (* if the term is well-typed than t and ct *)
393 (* are convertible. Nevertheless, I compute *)
394 (* the expected type. *)
395 ignore (type_of_aux context t (Some expected_type))
396 | Some t,Some (_,C.Decl ct) ->
397 ignore (type_of_aux context t (Some ct))
398 | _,_ -> assert false (* the term is not well typed!!! *)
399 ) l lifted_canonical_context
401 let (_,canonical_context,ty) =
402 List.find (function (m,_,_) -> n = m) metasenv
404 (* Checks suppressed *)
405 CicSubstitution.lift_meta l ty
406 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
407 | C.Implicit -> raise (Impossible 21)
409 (* Let's visit all the subterms that will not be visited later *)
410 let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
411 let _ = type_of_aux context ty None in
412 (* Checks suppressed *)
414 | C.Prod (name,s,t) ->
415 let sort1 = type_of_aux context s None
416 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
417 sort_of_prod context (name,s) (sort1,sort2)
418 | C.Lambda (n,s,t) ->
419 (* Let's visit all the subterms that will not be visited later *)
420 let _ = type_of_aux context s None in
421 let expected_target_type =
422 match expectedty with
424 | Some expectedty' ->
426 match R.whd context expectedty' with
427 C.Prod (_,_,expected_target_type) ->
428 head_beta_reduce expected_target_type
434 type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
436 (* Checks suppressed *)
439 (*CSC: What are the right expected types for the source and *)
440 (*CSC: target of a LetIn? None used. *)
441 (* Let's visit all the subterms that will not be visited later *)
442 let ty = type_of_aux context s None in
444 (* Checks suppressed *)
445 type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None
446 in (* CicSubstitution.subst s t_typ *)
447 if does_not_occur 1 t_typ then
448 (* since [Rel 1] does not occur in typ, substituting any term *)
449 (* in place of [Rel 1] is equivalent to delifting once *)
450 CicSubstitution.subst C.Implicit t_typ
453 | C.Appl (he::tl) when List.length tl > 0 ->
455 let expected_hetype =
456 (* Inefficient, the head is computed twice. But I know *)
457 (* of no other solution. *)
459 (R.whd context (xxx_type_of_aux' metasenv context he)))
461 let hetype = type_of_aux context he (Some expected_hetype) in
462 let tlbody_and_type =
466 | C.Prod (n,s,t),he::tl ->
467 (he, type_of_aux context he (Some (head_beta_reduce s)))::
468 (aux (R.whd context (S.subst he t), tl))
471 aux (expected_hetype, tl) *)
472 let hetype = R.whd context (type_of_aux context he None) in
473 let tlbody_and_type =
477 | C.Prod (n,s,t),he::tl ->
478 (he, type_of_aux context he (Some (head_beta_reduce s)))::
479 (aux (R.whd context (S.subst he t), tl))
484 eat_prods context hetype tlbody_and_type
485 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
486 | C.Const (uri,exp_named_subst) ->
487 visit_exp_named_subst context uri exp_named_subst ;
488 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
489 | C.MutInd (uri,i,exp_named_subst) ->
490 visit_exp_named_subst context uri exp_named_subst ;
491 CicSubstitution.subst_vars exp_named_subst
492 (type_of_mutual_inductive_defs uri i)
493 | C.MutConstruct (uri,i,j,exp_named_subst) ->
494 visit_exp_named_subst context uri exp_named_subst ;
495 CicSubstitution.subst_vars exp_named_subst
496 (type_of_mutual_inductive_constr uri i j)
497 | C.MutCase (uri,i,outtype,term,pl) ->
498 let outsort = type_of_aux context outtype None in
499 let (need_dummy, k) =
500 let rec guess_args context t =
501 match CicReduction.whd context t with
502 C.Sort _ -> (true, 0)
503 | C.Prod (name, s, t) ->
504 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
506 (* last prod before sort *)
507 match CicReduction.whd context s with
508 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
510 | C.Appl ((C.MutInd (uri',i',_)) :: _)
511 when U.eq uri' uri && i' = i -> (false, 1)
515 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
517 let (b, k) = guess_args context outsort in
518 if not b then (b, k - 1) else (b, k)
520 let (parameters, arguments,exp_named_subst) =
522 xxx_type_of_aux' metasenv context term
525 R.whd context (type_of_aux context term
526 (Some (head_beta_reduce type_of_term)))
528 (*CSC manca il caso dei CAST *)
529 C.MutInd (uri',i',exp_named_subst) ->
530 (* Checks suppressed *)
531 [],[],exp_named_subst
532 | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
534 split tl (List.length tl - k)
535 in params,args,exp_named_subst
537 raise (NotWellTyped "MutCase: the term is not an inductive one")
539 (* Checks suppressed *)
540 (* Let's visit all the subterms that will not be visited later *)
542 match CicEnvironment.get_cooked_obj uri with
543 C.InductiveDefinition (tl,_,parsno) ->
544 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
546 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
552 if parameters = [] then
553 (C.MutConstruct (uri,i,j,exp_named_subst))
555 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
558 type_of_branch context parsno need_dummy outtype cons
559 (xxx_type_of_aux' metasenv context cons)
561 ignore (type_of_aux context p
562 (Some (head_beta_reduce expectedtype))) ;
564 ) 1 (List.combine pl cl)
566 if not need_dummy then
567 C.Appl ((outtype::arguments)@[term])
568 else if arguments = [] then
571 C.Appl (outtype::arguments)
573 (* Let's visit all the subterms that will not be visited later *)
578 let _ = type_of_aux context ty None in
579 (Some (C.Name n,(C.Decl ty)))
588 head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
590 ignore (type_of_aux context' bo (Some expectedty))
593 (* Checks suppressed *)
594 let (_,_,ty,_) = List.nth fl i in
597 (* Let's visit all the subterms that will not be visited later *)
602 let _ = type_of_aux context ty None in
603 (Some (C.Name n,(C.Decl ty)))
612 head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
614 ignore (type_of_aux context' bo (Some expectedty))
617 (* Checks suppressed *)
618 let (_,ty,_) = List.nth fl i in
621 let synthesized' = head_beta_reduce synthesized in
623 match expectedty with
625 (* No expected type *)
626 {synthesized = synthesized' ; expected = None}, synthesized
627 | Some ty when xxx_syntactic_equality synthesized' ty ->
628 (* The expected type is synthactically equal to *)
629 (* the synthesized type. Let's forget it. *)
630 {synthesized = synthesized' ; expected = None}, synthesized
631 | Some expectedty' ->
632 {synthesized = synthesized' ; expected = Some expectedty'},
635 CicHash.add subterms_to_types t types ;
638 and visit_exp_named_subst context uri exp_named_subst =
640 match CicEnvironment.get_cooked_obj uri with
641 Cic.Constant (_,_,_,params)
642 | Cic.CurrentProof (_,_,_,_,params)
643 | Cic.Variable (_,_,_,params)
644 | Cic.InductiveDefinition (_,params,_) ->
647 match CicEnvironment.get_cooked_obj uri with
648 Cic.Variable (_,None,ty,_) -> uri,ty
649 | _ -> assert false (* the theorem is well-typed *)
652 let rec check uris_and_types subst =
653 match uris_and_types,subst with
655 | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
656 ignore (type_of_aux context t (Some ty)) ;
659 (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
662 | _,_ -> assert false (* the theorem is well-typed *)
664 check uris_and_types exp_named_subst
666 and sort_of_prod context (name,s) (t1, t2) =
667 let module C = Cic in
668 let t1' = CicReduction.whd context t1 in
669 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
670 match (t1', t2') with
671 (C.Sort s1, C.Sort s2)
672 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
674 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
678 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
680 and eat_prods context hetype =
681 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
685 | (hete, hety)::tl ->
686 (match (CicReduction.whd context hetype) with
688 (* Checks suppressed *)
689 eat_prods context (CicSubstitution.subst hete t) tl
690 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
693 and type_of_branch context argsno need_dummy outtype term constype =
694 let module C = Cic in
695 let module R = CicReduction in
696 match R.whd context constype with
701 C.Appl [outtype ; term]
702 | C.Appl (C.MutInd (_,_,_)::tl) ->
703 let (_,arguments) = split tl argsno
705 if need_dummy && arguments = [] then
708 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
709 | C.Prod (name,so,de) ->
711 match CicSubstitution.lift 1 term with
712 C.Appl l -> C.Appl (l@[C.Rel 1])
713 | t -> C.Appl [t ; C.Rel 1]
715 C.Prod (C.Anonymous,so,type_of_branch
716 ((Some (name,(C.Decl so)))::context) argsno need_dummy
717 (CicSubstitution.lift 1 outtype) term' de)
718 | _ -> raise (Impossible 20)
721 type_of_aux context t expectedty
724 let double_type_of metasenv context t expectedty =
725 let subterms_to_types = CicHash.create 503 in
726 ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;