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 type_of_aux'_add_time = ref 0.0;;
35 let number_new_type_of_aux'_double_work = ref 0;;
36 let number_new_type_of_aux' = ref 0;;
37 let number_new_type_of_aux'_prop = ref 0;;
39 let double_work = ref 0;;
41 let xxx_type_of_aux' m c t =
42 let t1 = Sys.time () in
43 let res = CicTypeChecker.type_of_aux' m c t in
44 let t2 = Sys.time () in
45 type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
49 type types = {synthesized : Cic.term ; expected : Cic.term option};;
51 (* does_not_occur n te *)
52 (* returns [true] if [Rel n] does not occur in [te] *)
53 let rec does_not_occur n =
56 C.Rel m when m = n -> false
62 does_not_occur n te && does_not_occur n ty
63 | C.Prod (name,so,dest) ->
64 does_not_occur n so &&
65 does_not_occur (n + 1) dest
66 | C.Lambda (name,so,dest) ->
67 does_not_occur n so &&
68 does_not_occur (n + 1) dest
69 | C.LetIn (name,so,dest) ->
70 does_not_occur n so &&
71 does_not_occur (n + 1) dest
73 List.fold_right (fun x i -> i && does_not_occur n x) l true
74 | C.Var (_,exp_named_subst)
75 | C.Const (_,exp_named_subst)
76 | C.MutInd (_,_,exp_named_subst)
77 | C.MutConstruct (_,_,_,exp_named_subst) ->
78 List.fold_right (fun (_,x) i -> i && does_not_occur n x)
80 | C.MutCase (_,_,out,te,pl) ->
81 does_not_occur n out && does_not_occur n te &&
82 List.fold_right (fun x i -> i && does_not_occur n x) pl true
84 let len = List.length fl in
85 let n_plus_len = n + len in
87 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
91 i && does_not_occur n ty &&
92 does_not_occur n_plus_len bo
95 let len = List.length fl in
96 let n_plus_len = n + len in
98 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
102 i && does_not_occur n ty &&
103 does_not_occur n_plus_len bo
107 (*CSC: potrebbe creare applicazioni di applicazioni *)
108 (*CSC: ora non e' piu' head, ma completa!!! *)
109 let rec head_beta_reduce =
110 let module S = CicSubstitution in
111 let module C = Cic in
114 | C.Var (uri,exp_named_subst) ->
115 let exp_named_subst' =
116 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
118 C.Var (uri,exp_named_subst)
122 (function None -> None | Some t -> Some (head_beta_reduce t)) l
125 | C.Implicit -> assert false
127 C.Cast (head_beta_reduce te, head_beta_reduce ty)
129 C.Prod (n, head_beta_reduce s, head_beta_reduce t)
130 | C.Lambda (n,s,t) ->
131 C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
133 C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
134 | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
135 let he' = S.subst he t in
139 head_beta_reduce (C.Appl (he'::tl))
141 C.Appl (List.map head_beta_reduce l)
142 | C.Const (uri,exp_named_subst) ->
143 let exp_named_subst' =
144 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
146 C.Const (uri,exp_named_subst')
147 | C.MutInd (uri,i,exp_named_subst) ->
148 let exp_named_subst' =
149 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
151 C.MutInd (uri,i,exp_named_subst')
152 | C.MutConstruct (uri,i,j,exp_named_subst) ->
153 let exp_named_subst' =
154 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
156 C.MutConstruct (uri,i,j,exp_named_subst')
157 | C.MutCase (sp,i,outt,t,pl) ->
158 C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t,
159 List.map head_beta_reduce pl)
163 (function (name,i,ty,bo) ->
164 name,i,head_beta_reduce ty,head_beta_reduce bo
171 (function (name,ty,bo) ->
172 name,head_beta_reduce ty,head_beta_reduce bo
178 (* syntactic_equality up to the *)
179 (* distinction between fake dependent products *)
180 (* and non-dependent products, alfa-conversion *)
181 (*CSC: must alfa-conversion be considered or not? *)
182 let syntactic_equality t t' =
183 let module C = Cic in
184 let rec syntactic_equality t t' =
188 C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
189 UriManager.eq uri uri' &&
190 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
191 | C.Cast (te,ty), C.Cast (te',ty') ->
192 syntactic_equality te te' &&
193 syntactic_equality ty ty'
194 | C.Prod (_,s,t), C.Prod (_,s',t') ->
195 syntactic_equality s s' &&
196 syntactic_equality t t'
197 | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
198 syntactic_equality s s' &&
199 syntactic_equality t t'
200 | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
201 syntactic_equality s s' &&
202 syntactic_equality t t'
203 | C.Appl l, C.Appl l' ->
204 List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
205 | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
206 UriManager.eq uri uri' &&
207 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
208 | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
209 UriManager.eq uri uri' && i = i' &&
210 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
211 | C.MutConstruct (uri,i,j,exp_named_subst),
212 C.MutConstruct (uri',i',j',exp_named_subst') ->
213 UriManager.eq uri uri' && i = i' && j = j' &&
214 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
215 | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
216 UriManager.eq sp sp' && i = i' &&
217 syntactic_equality outt outt' &&
218 syntactic_equality t t' &&
220 (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
221 | C.Fix (i,fl), C.Fix (i',fl') ->
224 (fun b (_,i,ty,bo) (_,i',ty',bo') ->
226 syntactic_equality ty ty' &&
227 syntactic_equality bo bo') true fl fl'
228 | C.CoFix (i,fl), C.CoFix (i',fl') ->
231 (fun b (_,ty,bo) (_,ty',bo') ->
233 syntactic_equality ty ty' &&
234 syntactic_equality bo bo') true fl fl'
235 | _, _ -> false (* we already know that t != t' *)
236 and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
238 (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
239 exp_named_subst1 exp_named_subst2
242 syntactic_equality t t'
250 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
251 | (_,_) -> raise ListTooShort
254 let type_of_constant uri =
255 let module C = Cic in
256 let module R = CicReduction in
257 let module U = UriManager in
259 match CicEnvironment.is_type_checked uri with
260 CicEnvironment.CheckedObj cobj -> cobj
261 | CicEnvironment.UncheckedObj uobj ->
262 raise (NotWellTyped "Reference to an unchecked constant")
265 C.Constant (_,_,ty,_) -> ty
266 | C.CurrentProof (_,_,_,ty,_) -> ty
267 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
270 let type_of_variable uri =
271 let module C = Cic in
272 let module R = CicReduction in
273 let module U = UriManager in
274 match CicEnvironment.is_type_checked uri with
275 CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
276 | CicEnvironment.UncheckedObj (C.Variable _) ->
277 raise (NotWellTyped "Reference to an unchecked variable")
278 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
281 let type_of_mutual_inductive_defs uri i =
282 let module C = Cic in
283 let module R = CicReduction in
284 let module U = UriManager in
286 match CicEnvironment.is_type_checked uri with
287 CicEnvironment.CheckedObj cobj -> cobj
288 | CicEnvironment.UncheckedObj uobj ->
289 raise (NotWellTyped "Reference to an unchecked inductive type")
292 C.InductiveDefinition (dl,_,_) ->
293 let (_,_,arity,_) = List.nth dl i in
295 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
298 let type_of_mutual_inductive_constr uri i j =
299 let module C = Cic in
300 let module R = CicReduction in
301 let module U = UriManager in
303 match CicEnvironment.is_type_checked uri with
304 CicEnvironment.CheckedObj cobj -> cobj
305 | CicEnvironment.UncheckedObj uobj ->
306 raise (NotWellTyped "Reference to an unchecked constructor")
309 C.InductiveDefinition (dl,_,_) ->
310 let (_,_,_,cl) = List.nth dl i in
311 let (_,ty) = List.nth cl (j-1) in
313 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
321 let hash = Hashtbl.hash
325 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
326 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
327 (* Coscoy's double type-inference algorithm *)
328 (* It computes the inner-types of every subterm of [t], *)
329 (* even when they are not needed to compute the types *)
330 (* of other terms. *)
331 let rec type_of_aux context t expectedty =
332 let module C = Cic in
333 let module R = CicReduction in
334 let module S = CicSubstitution in
335 let module U = UriManager in
340 match List.nth context (n - 1) with
341 Some (_,C.Decl t) -> S.lift n t
342 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
343 | Some (_,C.Def (bo,None)) ->
344 type_of_aux context (S.lift n bo) expectedty
345 | None -> raise RelToHiddenHypothesis
347 _ -> raise (NotWellTyped "Not a close term")
349 | C.Var (uri,exp_named_subst) ->
350 visit_exp_named_subst context uri exp_named_subst ;
351 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
353 (* Let's visit all the subterms that will not be visited later *)
354 let (_,canonical_context,_) =
355 List.find (function (m,_,_) -> n = m) metasenv
357 let lifted_canonical_context =
361 | (Some (n,C.Decl t))::tl ->
362 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
363 | (Some (n,C.Def (t,None)))::tl ->
364 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::
366 | None::tl -> None::(aux (i+1) tl)
367 | (Some (_,C.Def (_,Some _)))::_ -> assert false
369 aux 1 canonical_context
376 | Some t,Some (_,C.Def (ct,_)) ->
379 (xxx_type_of_aux' metasenv context ct)
381 (* Maybe I am a bit too paranoid, because *)
382 (* if the term is well-typed than t and ct *)
383 (* are convertible. Nevertheless, I compute *)
384 (* the expected type. *)
385 ignore (type_of_aux context t (Some expected_type))
386 | Some t,Some (_,C.Decl ct) ->
387 ignore (type_of_aux context t (Some ct))
388 | _,_ -> assert false (* the term is not well typed!!! *)
389 ) l lifted_canonical_context
391 let (_,canonical_context,ty) =
392 List.find (function (m,_,_) -> n = m) metasenv
394 (* Checks suppressed *)
395 CicSubstitution.lift_meta l ty
396 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
397 | C.Implicit -> raise (Impossible 21)
399 (* Let's visit all the subterms that will not be visited later *)
400 let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
401 let _ = type_of_aux context ty None in
402 (* Checks suppressed *)
404 | C.Prod (name,s,t) ->
405 let sort1 = type_of_aux context s None
406 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
407 sort_of_prod context (name,s) (sort1,sort2)
408 | C.Lambda (n,s,t) ->
409 (* Let's visit all the subterms that will not be visited later *)
410 let _ = type_of_aux context s None in
411 let expected_target_type =
412 match expectedty with
414 | Some expectedty' ->
416 match R.whd context expectedty' with
417 C.Prod (_,_,expected_target_type) ->
418 head_beta_reduce expected_target_type
424 type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
426 (* Checks suppressed *)
429 (*CSC: What are the right expected types for the source and *)
430 (*CSC: target of a LetIn? None used. *)
431 (* Let's visit all the subterms that will not be visited later *)
432 let ty = type_of_aux context s None in
434 (* Checks suppressed *)
435 type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None
437 if does_not_occur 1 t_typ then
438 (* since [Rel 1] does not occur in typ, substituting any term *)
439 (* in place of [Rel 1] is equivalent to delifting once *)
440 CicSubstitution.subst C.Implicit t_typ
443 | C.Appl (he::tl) when List.length tl > 0 ->
444 let expected_hetype =
445 (* Inefficient, the head is computed twice. But I know *)
446 (* of no other solution. *)
448 (R.whd context (xxx_type_of_aux' metasenv context he)))
450 let hetype = type_of_aux context he (Some expected_hetype) in
451 let tlbody_and_type =
455 | C.Prod (n,s,t),he::tl ->
456 (he, type_of_aux context he (Some (head_beta_reduce s)))::
457 (aux (R.whd context (S.subst he t), tl))
460 aux (expected_hetype, tl)
462 eat_prods context hetype tlbody_and_type
463 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
464 | C.Const (uri,exp_named_subst) ->
465 visit_exp_named_subst context uri exp_named_subst ;
466 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
467 | C.MutInd (uri,i,exp_named_subst) ->
468 visit_exp_named_subst context uri exp_named_subst ;
469 CicSubstitution.subst_vars exp_named_subst
470 (type_of_mutual_inductive_defs uri i)
471 | C.MutConstruct (uri,i,j,exp_named_subst) ->
472 visit_exp_named_subst context uri exp_named_subst ;
473 CicSubstitution.subst_vars exp_named_subst
474 (type_of_mutual_inductive_constr uri i j)
475 | C.MutCase (uri,i,outtype,term,pl) ->
476 let outsort = type_of_aux context outtype None in
477 let (need_dummy, k) =
478 let rec guess_args context t =
479 match CicReduction.whd context t with
480 C.Sort _ -> (true, 0)
481 | C.Prod (name, s, t) ->
482 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
484 (* last prod before sort *)
485 match CicReduction.whd context s with
486 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
488 | C.Appl ((C.MutInd (uri',i',_)) :: _)
489 when U.eq uri' uri && i' = i -> (false, 1)
493 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
495 let (b, k) = guess_args context outsort in
496 if not b then (b, k - 1) else (b, k)
498 let (parameters, arguments,exp_named_subst) =
500 xxx_type_of_aux' metasenv context term
503 R.whd context (type_of_aux context term
504 (Some (head_beta_reduce type_of_term)))
506 (*CSC manca il caso dei CAST *)
507 C.MutInd (uri',i',exp_named_subst) ->
508 (* Checks suppressed *)
509 [],[],exp_named_subst
510 | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
512 split tl (List.length tl - k)
513 in params,args,exp_named_subst
515 raise (NotWellTyped "MutCase: the term is not an inductive one")
517 (* Checks suppressed *)
518 (* Let's visit all the subterms that will not be visited later *)
520 match CicEnvironment.get_cooked_obj uri with
521 C.InductiveDefinition (tl,_,parsno) ->
522 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
524 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
530 if parameters = [] then
531 (C.MutConstruct (uri,i,j,exp_named_subst))
533 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
536 type_of_branch context parsno need_dummy outtype cons
537 (xxx_type_of_aux' metasenv context cons)
539 ignore (type_of_aux context p
540 (Some (head_beta_reduce expectedtype))) ;
542 ) 1 (List.combine pl cl)
544 if not need_dummy then
545 C.Appl ((outtype::arguments)@[term])
546 else if arguments = [] then
549 C.Appl (outtype::arguments)
551 (* Let's visit all the subterms that will not be visited later *)
556 let _ = type_of_aux context ty None in
557 (Some (C.Name n,(C.Decl ty)))
566 head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
568 ignore (type_of_aux context' bo (Some expectedty))
571 (* Checks suppressed *)
572 let (_,_,ty,_) = List.nth fl i in
575 (* Let's visit all the subterms that will not be visited later *)
580 let _ = type_of_aux context ty None in
581 (Some (C.Name n,(C.Decl ty)))
590 head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
592 ignore (type_of_aux context' bo (Some expectedty))
595 (* Checks suppressed *)
596 let (_,ty,_) = List.nth fl i in
599 let synthesized' = head_beta_reduce synthesized in
601 match expectedty with
603 (* No expected type *)
604 {synthesized = synthesized' ; expected = None}, synthesized
605 | Some ty when syntactic_equality synthesized' ty ->
606 (* The expected type is synthactically equal to *)
607 (* the synthesized type. Let's forget it. *)
608 {synthesized = synthesized' ; expected = None}, synthesized
609 | Some expectedty' ->
610 {synthesized = synthesized' ; expected = Some expectedty'},
613 CicHash.add subterms_to_types t types ;
616 and visit_exp_named_subst context uri exp_named_subst =
618 match CicEnvironment.get_cooked_obj uri with
619 Cic.Constant (_,_,_,params)
620 | Cic.CurrentProof (_,_,_,_,params)
621 | Cic.Variable (_,_,_,params)
622 | Cic.InductiveDefinition (_,params,_) ->
625 match CicEnvironment.get_cooked_obj uri with
626 Cic.Variable (_,None,ty,_) -> uri,ty
627 | _ -> assert false (* the theorem is well-typed *)
630 let rec check uris_and_types subst =
631 match uris_and_types,subst with
633 | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
634 ignore (type_of_aux context t (Some ty)) ;
637 (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
640 | _,_ -> assert false (* the theorem is well-typed *)
642 check uris_and_types exp_named_subst
644 and sort_of_prod context (name,s) (t1, t2) =
645 let module C = Cic in
646 let t1' = CicReduction.whd context t1 in
647 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
648 match (t1', t2') with
649 (C.Sort s1, C.Sort s2)
650 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
652 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
656 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
658 and eat_prods context hetype =
659 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
663 | (hete, hety)::tl ->
664 (match (CicReduction.whd context hetype) with
666 (* Checks suppressed *)
667 eat_prods context (CicSubstitution.subst hete t) tl
668 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
671 and type_of_branch context argsno need_dummy outtype term constype =
672 let module C = Cic in
673 let module R = CicReduction in
674 match R.whd context constype with
679 C.Appl [outtype ; term]
680 | C.Appl (C.MutInd (_,_,_)::tl) ->
681 let (_,arguments) = split tl argsno
683 if need_dummy && arguments = [] then
686 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
687 | C.Prod (name,so,de) ->
689 match CicSubstitution.lift 1 term with
690 C.Appl l -> C.Appl (l@[C.Rel 1])
691 | t -> C.Appl [t ; C.Rel 1]
693 C.Prod (C.Anonymous,so,type_of_branch
694 ((Some (name,(C.Decl so)))::context) argsno need_dummy
695 (CicSubstitution.lift 1 outtype) term' de)
696 | _ -> raise (Impossible 20)
699 type_of_aux context t expectedty
702 let double_type_of metasenv context t expectedty =
703 let subterms_to_types = CicHash.create 503 in
704 ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;