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/.
28 exception Impossible of int;;
29 exception NotWellTyped of string;;
30 exception WrongUriToConstant of string;;
31 exception WrongUriToVariable of string;;
32 exception WrongUriToMutualInductiveDefinitions of string;;
33 exception ListTooShort;;
34 exception RelToHiddenHypothesis;;
36 let xxx_type_of_aux' m c t =
38 Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph))
40 | CicTypeChecker.TypeCheckerFailure _ -> None (* because eta_expansion *)
43 type types = {synthesized : Cic.term ; expected : Cic.term option};;
45 (* does_not_occur n te *)
46 (* returns [true] if [Rel n] does not occur in [te] *)
47 let rec does_not_occur n =
50 C.Rel m when m = n -> false
54 | C.Implicit _ -> true
56 does_not_occur n te && does_not_occur n ty
57 | C.Prod (name,so,dest) ->
58 does_not_occur n so &&
59 does_not_occur (n + 1) dest
60 | C.Lambda (name,so,dest) ->
61 does_not_occur n so &&
62 does_not_occur (n + 1) dest
63 | C.LetIn (name,so,dest) ->
64 does_not_occur n so &&
65 does_not_occur (n + 1) dest
67 List.fold_right (fun x i -> i && does_not_occur n x) l true
68 | C.Var (_,exp_named_subst)
69 | C.Const (_,exp_named_subst)
70 | C.MutInd (_,_,exp_named_subst)
71 | C.MutConstruct (_,_,_,exp_named_subst) ->
72 List.fold_right (fun (_,x) i -> i && does_not_occur n x)
74 | C.MutCase (_,_,out,te,pl) ->
75 does_not_occur n out && does_not_occur n te &&
76 List.fold_right (fun x i -> i && does_not_occur n x) pl true
78 let len = List.length fl in
79 let n_plus_len = n + len in
82 i && does_not_occur n ty &&
83 does_not_occur n_plus_len bo
86 let len = List.length fl in
87 let n_plus_len = n + len in
90 i && does_not_occur n ty &&
91 does_not_occur n_plus_len bo
96 let module S = CicSubstitution in
100 | C.Var (uri,exp_named_subst) ->
101 let exp_named_subst' =
102 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
104 C.Var (uri,exp_named_subst')
108 (function None -> None | Some t -> Some (beta_reduce t)) l
111 | C.Implicit _ -> assert false
113 C.Cast (beta_reduce te, beta_reduce ty)
115 C.Prod (n, beta_reduce s, beta_reduce t)
116 | C.Lambda (n,s,t) ->
117 C.Lambda (n, beta_reduce s, beta_reduce t)
119 C.LetIn (n, beta_reduce s, beta_reduce t)
120 | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
121 let he' = S.subst he t in
126 C.Appl l -> beta_reduce (C.Appl (l@tl))
127 | _ -> beta_reduce (C.Appl (he'::tl)))
129 C.Appl (List.map beta_reduce l)
130 | C.Const (uri,exp_named_subst) ->
131 let exp_named_subst' =
132 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
134 C.Const (uri,exp_named_subst')
135 | C.MutInd (uri,i,exp_named_subst) ->
136 let exp_named_subst' =
137 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
139 C.MutInd (uri,i,exp_named_subst')
140 | C.MutConstruct (uri,i,j,exp_named_subst) ->
141 let exp_named_subst' =
142 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
144 C.MutConstruct (uri,i,j,exp_named_subst')
145 | C.MutCase (sp,i,outt,t,pl) ->
146 C.MutCase (sp,i,beta_reduce outt,beta_reduce t,
147 List.map beta_reduce pl)
151 (function (name,i,ty,bo) ->
152 name,i,beta_reduce ty,beta_reduce bo
159 (function (name,ty,bo) ->
160 name,beta_reduce ty,beta_reduce bo
166 (* syntactic_equality up to the *)
167 (* distinction between fake dependent products *)
168 (* and non-dependent products, alfa-conversion *)
169 (*CSC: must alfa-conversion be considered or not? *)
170 let syntactic_equality t t' =
171 let module C = Cic in
172 let rec syntactic_equality t t' =
176 C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
177 UriManager.eq uri uri' &&
178 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
179 | C.Cast (te,ty), C.Cast (te',ty') ->
180 syntactic_equality te te' &&
181 syntactic_equality ty ty'
182 | C.Prod (_,s,t), C.Prod (_,s',t') ->
183 syntactic_equality s s' &&
184 syntactic_equality t t'
185 | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
186 syntactic_equality s s' &&
187 syntactic_equality t t'
188 | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
189 syntactic_equality s s' &&
190 syntactic_equality t t'
191 | C.Appl l, C.Appl l' ->
192 List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
193 | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
194 UriManager.eq uri uri' &&
195 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
196 | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
197 UriManager.eq uri uri' && i = i' &&
198 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
199 | C.MutConstruct (uri,i,j,exp_named_subst),
200 C.MutConstruct (uri',i',j',exp_named_subst') ->
201 UriManager.eq uri uri' && i = i' && j = j' &&
202 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
203 | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
204 UriManager.eq sp sp' && i = i' &&
205 syntactic_equality outt outt' &&
206 syntactic_equality t t' &&
208 (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
209 | C.Fix (i,fl), C.Fix (i',fl') ->
212 (fun b (_,i,ty,bo) (_,i',ty',bo') ->
214 syntactic_equality ty ty' &&
215 syntactic_equality bo bo') true fl fl'
216 | C.CoFix (i,fl), C.CoFix (i',fl') ->
219 (fun b (_,ty,bo) (_,ty',bo') ->
221 syntactic_equality ty ty' &&
222 syntactic_equality bo bo') true fl fl'
223 | _, _ -> false (* we already know that t != t' *)
224 and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
226 (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
227 exp_named_subst1 exp_named_subst2
230 syntactic_equality t t'
238 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
239 | (_,_) -> raise ListTooShort
242 let type_of_constant uri =
243 let module C = Cic in
244 let module R = CicReduction in
245 let module U = UriManager in
247 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
248 CicEnvironment.CheckedObj (cobj,_) -> cobj
249 | CicEnvironment.UncheckedObj uobj ->
250 raise (NotWellTyped "Reference to an unchecked constant")
253 C.Constant (_,_,ty,_,_) -> ty
254 | C.CurrentProof (_,_,_,ty,_,_) -> ty
255 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
258 let type_of_variable uri =
259 let module C = Cic in
260 let module R = CicReduction in
261 let module U = UriManager in
262 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
263 CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
264 | CicEnvironment.UncheckedObj (C.Variable _) ->
265 raise (NotWellTyped "Reference to an unchecked variable")
266 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
269 let type_of_mutual_inductive_defs uri i =
270 let module C = Cic in
271 let module R = CicReduction in
272 let module U = UriManager in
274 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
275 CicEnvironment.CheckedObj (cobj,_) -> cobj
276 | CicEnvironment.UncheckedObj uobj ->
277 raise (NotWellTyped "Reference to an unchecked inductive type")
280 C.InductiveDefinition (dl,_,_,_) ->
281 let (_,_,arity,_) = List.nth dl i in
283 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
286 let type_of_mutual_inductive_constr uri i j =
287 let module C = Cic in
288 let module R = CicReduction in
289 let module U = UriManager in
291 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
292 CicEnvironment.CheckedObj (cobj,_) -> cobj
293 | CicEnvironment.UncheckedObj uobj ->
294 raise (NotWellTyped "Reference to an unchecked constructor")
297 C.InductiveDefinition (dl,_,_,_) ->
298 let (_,_,_,cl) = List.nth dl i in
299 let (_,ty) = List.nth cl (j-1) in
301 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
304 let pack_coercion = ref (fun _ _ _ -> assert false);;
306 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
307 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
308 (* Coscoy's double type-inference algorithm *)
309 (* It computes the inner-types of every subterm of [t], *)
310 (* even when they are not needed to compute the types *)
311 (* of other terms. *)
312 let rec type_of_aux context t expectedty =
313 let module C = Cic in
314 let module R = CicReduction in
315 let module S = CicSubstitution in
316 let module U = UriManager in
318 match expectedty with
320 | Some t -> Some (!pack_coercion metasenv context t) in
325 match List.nth context (n - 1) with
326 Some (_,C.Decl t) -> S.lift n t
327 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
328 | Some (_,C.Def (bo,None)) ->
329 type_of_aux context (S.lift n bo) expectedty
330 | None -> raise RelToHiddenHypothesis
332 _ -> raise (NotWellTyped "Not a close term")
334 | C.Var (uri,exp_named_subst) ->
335 visit_exp_named_subst context uri exp_named_subst ;
336 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
338 (* Let's visit all the subterms that will not be visited later *)
339 let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
340 let lifted_canonical_context =
344 | (Some (n,C.Decl t))::tl ->
345 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
346 | (Some (n,C.Def (t,None)))::tl ->
347 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
349 | None::tl -> None::(aux (i+1) tl)
350 | (Some (_,C.Def (_,Some _)))::_ -> assert false
352 aux 1 canonical_context
359 | Some t,Some (_,C.Def (ct,_)) ->
361 match xxx_type_of_aux' metasenv context ct with
363 | Some t -> Some (R.whd context t)
365 (* Maybe I am a bit too paranoid, because *)
366 (* if the term is well-typed than t and ct *)
367 (* are convertible. Nevertheless, I compute *)
368 (* the expected type. *)
369 ignore (type_of_aux context t expected_type)
370 | Some t,Some (_,C.Decl ct) ->
371 ignore (type_of_aux context t (Some ct))
372 | _,_ -> assert false (* the term is not well typed!!! *)
373 ) l lifted_canonical_context
375 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
376 (* Checks suppressed *)
377 CicSubstitution.subst_meta l ty
378 | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
379 C.Sort (C.Type (CicUniv.fresh()))
380 | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)
381 | C.Implicit _ -> raise (Impossible 21)
383 (* Let's visit all the subterms that will not be visited later *)
384 let _ = type_of_aux context te (Some (beta_reduce ty)) in
385 let _ = type_of_aux context ty None in
386 (* Checks suppressed *)
388 | C.Prod (name,s,t) ->
389 let sort1 = type_of_aux context s None
390 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
391 sort_of_prod context (name,s) (sort1,sort2)
392 | C.Lambda (n,s,t) ->
393 (* Let's visit all the subterms that will not be visited later *)
394 let _ = type_of_aux context s None in
395 let expected_target_type =
396 match expectedty with
398 | Some expectedty' ->
400 match R.whd context expectedty' with
401 C.Prod (_,_,expected_target_type) ->
402 beta_reduce expected_target_type
408 type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
410 (* Checks suppressed *)
413 (*CSC: What are the right expected types for the source and *)
414 (*CSC: target of a LetIn? None used. *)
415 (* Let's visit all the subterms that will not be visited later *)
416 let ty = type_of_aux context s None in
418 (* Checks suppressed *)
419 type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None
420 in (* CicSubstitution.subst s t_typ *)
421 if does_not_occur 1 t_typ then
422 (* since [Rel 1] does not occur in typ, substituting any term *)
423 (* in place of [Rel 1] is equivalent to delifting once *)
424 CicSubstitution.subst (C.Implicit None) t_typ
427 | C.Appl (he::tl) when List.length tl > 0 ->
429 let expected_hetype =
430 (* Inefficient, the head is computed twice. But I know *)
431 (* of no other solution. *)
433 (R.whd context (xxx_type_of_aux' metasenv context he)))
435 let hetype = type_of_aux context he (Some expected_hetype) in
436 let tlbody_and_type =
440 | C.Prod (n,s,t),he::tl ->
441 (he, type_of_aux context he (Some (beta_reduce s)))::
442 (aux (R.whd context (S.subst he t), tl))
445 aux (expected_hetype, tl) *)
446 let hetype = R.whd context (type_of_aux context he None) in
447 let tlbody_and_type =
451 | C.Prod (n,s,t),he::tl ->
452 (he, type_of_aux context he (Some (beta_reduce s)))::
453 (aux (R.whd context (S.subst he t), tl))
458 eat_prods context hetype tlbody_and_type
459 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
460 | C.Const (uri,exp_named_subst) ->
461 visit_exp_named_subst context uri exp_named_subst ;
462 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
463 | C.MutInd (uri,i,exp_named_subst) ->
464 visit_exp_named_subst context uri exp_named_subst ;
465 CicSubstitution.subst_vars exp_named_subst
466 (type_of_mutual_inductive_defs uri i)
467 | C.MutConstruct (uri,i,j,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_constr uri i j)
471 | C.MutCase (uri,i,outtype,term,pl) ->
472 let outsort = type_of_aux context outtype None in
473 let (need_dummy, k) =
474 let rec guess_args context t =
475 match CicReduction.whd context t with
476 C.Sort _ -> (true, 0)
477 | C.Prod (name, s, t) ->
478 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
480 (* last prod before sort *)
481 match CicReduction.whd context s with
482 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
484 | C.Appl ((C.MutInd (uri',i',_)) :: _)
485 when U.eq uri' uri && i' = i -> (false, 1)
489 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
491 let (b, k) = guess_args context outsort in
492 if not b then (b, k - 1) else (b, k)
494 let (parameters, arguments,exp_named_subst) =
496 match xxx_type_of_aux' metasenv context term with
498 | Some t -> Some (beta_reduce t)
501 R.whd context (type_of_aux context term type_of_term)
503 (*CSC manca il caso dei CAST *)
504 C.MutInd (uri',i',exp_named_subst) ->
505 (* Checks suppressed *)
506 [],[],exp_named_subst
507 | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
509 split tl (List.length tl - k)
510 in params,args,exp_named_subst
512 raise (NotWellTyped "MutCase: the term is not an inductive one")
514 (* Checks suppressed *)
515 (* Let's visit all the subterms that will not be visited later *)
519 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
520 with Not_found -> assert false
523 C.InductiveDefinition (tl,_,parsno,_) ->
524 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
526 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
532 if parameters = [] then
533 (C.MutConstruct (uri,i,j,exp_named_subst))
535 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
538 match xxx_type_of_aux' metasenv context cons with
543 (type_of_branch context parsno need_dummy outtype
546 ignore (type_of_aux context p expectedtype);
548 ) 1 (List.combine pl cl)
550 if not need_dummy then
551 C.Appl ((outtype::arguments)@[term])
552 else if arguments = [] then
555 C.Appl (outtype::arguments)
557 (* Let's visit all the subterms that will not be visited later *)
562 let _ = type_of_aux context ty None in
563 (Some (C.Name n,(C.Decl ty)))
572 beta_reduce (CicSubstitution.lift (List.length fl) ty)
574 ignore (type_of_aux context' bo (Some expectedty))
577 (* Checks suppressed *)
578 let (_,_,ty,_) = List.nth fl i in
581 (* Let's visit all the subterms that will not be visited later *)
586 let _ = type_of_aux context ty None in
587 (Some (C.Name n,(C.Decl ty)))
596 beta_reduce (CicSubstitution.lift (List.length fl) ty)
598 ignore (type_of_aux context' bo (Some expectedty))
601 (* Checks suppressed *)
602 let (_,ty,_) = List.nth fl i in
605 let synthesized' = beta_reduce synthesized in
606 let synthesized' = !pack_coercion metasenv context synthesized' in
608 match expectedty with
610 (* No expected type *)
611 {synthesized = synthesized' ; expected = None}, synthesized
612 | Some ty when syntactic_equality synthesized' ty ->
613 (* The expected type is synthactically equal to *)
614 (* the synthesized type. Let's forget it. *)
615 {synthesized = synthesized' ; expected = None}, synthesized
616 | Some expectedty' ->
617 {synthesized = synthesized' ; expected = Some expectedty'},
620 assert (not (Cic.CicHash.mem subterms_to_types t));
621 Cic.CicHash.add subterms_to_types t types ;
624 and visit_exp_named_subst context uri exp_named_subst =
628 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
629 with Not_found -> assert false
631 let params = CicUtil.params_of_obj obj in
636 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
637 with Not_found -> assert false
640 Cic.Variable (_,None,ty,_,_) -> uri,ty
641 | _ -> assert false (* the theorem is well-typed *)
644 let rec check uris_and_types subst =
645 match uris_and_types,subst with
647 | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
648 ignore (type_of_aux context t (Some ty)) ;
651 (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
654 | _,_ -> assert false (* the theorem is well-typed *)
656 check uris_and_types exp_named_subst
658 and sort_of_prod context (name,s) (t1, t2) =
659 let module C = Cic in
660 let t1' = CicReduction.whd context t1 in
661 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
662 match (t1', t2') with
663 (C.Sort _, C.Sort s2)
664 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
665 (* different from Coq manual!!! *)
667 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
668 C.Sort (C.Type (CicUniv.fresh()))
669 | (C.Sort _,C.Sort (C.Type t1)) ->
670 (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
671 C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
672 | (C.Meta _, C.Sort _) -> t2'
673 | (C.Meta _, (C.Meta (_,_) as t))
674 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
679 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
681 and eat_prods context hetype =
682 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
686 | (hete, hety)::tl ->
687 (match (CicReduction.whd context hetype) with
689 (* Checks suppressed *)
690 eat_prods context (CicSubstitution.subst hete t) tl
691 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
694 and type_of_branch context argsno need_dummy outtype term constype =
695 let module C = Cic in
696 let module R = CicReduction in
697 match R.whd context constype with
702 C.Appl [outtype ; term]
703 | C.Appl (C.MutInd (_,_,_)::tl) ->
704 let (_,arguments) = split tl argsno
706 if need_dummy && arguments = [] then
709 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
710 | C.Prod (name,so,de) ->
712 match CicSubstitution.lift 1 term with
713 C.Appl l -> C.Appl (l@[C.Rel 1])
714 | t -> C.Appl [t ; C.Rel 1]
716 C.Prod (C.Anonymous,so,type_of_branch
717 ((Some (name,(C.Decl so)))::context) argsno need_dummy
718 (CicSubstitution.lift 1 outtype) term' de)
719 | _ -> raise (Impossible 20)
722 type_of_aux context t expectedty
725 let double_type_of metasenv context t expectedty =
726 let subterms_to_types = Cic.CicHash.create 503 in
727 ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;