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 type types = {synthesized : Cic.term ; expected : Cic.term option};;
36 (* does_not_occur n te *)
37 (* returns [true] if [Rel n] does not occur in [te] *)
38 let rec does_not_occur n =
41 C.Rel m when m = n -> false
47 does_not_occur n te && does_not_occur n ty
48 | C.Prod (name,so,dest) ->
49 does_not_occur n so &&
50 does_not_occur (n + 1) dest
51 | C.Lambda (name,so,dest) ->
52 does_not_occur n so &&
53 does_not_occur (n + 1) dest
54 | C.LetIn (name,so,dest) ->
55 does_not_occur n so &&
56 does_not_occur (n + 1) dest
58 List.fold_right (fun x i -> i && does_not_occur n x) l true
59 | C.Var (_,exp_named_subst)
60 | C.Const (_,exp_named_subst)
61 | C.MutInd (_,_,exp_named_subst)
62 | C.MutConstruct (_,_,_,exp_named_subst) ->
63 List.fold_right (fun (_,x) i -> i && does_not_occur n x)
65 | C.MutCase (_,_,out,te,pl) ->
66 does_not_occur n out && does_not_occur n te &&
67 List.fold_right (fun x i -> i && does_not_occur n x) pl true
69 let len = List.length fl in
70 let n_plus_len = n + len in
72 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
76 i && does_not_occur n ty &&
77 does_not_occur n_plus_len bo
80 let len = List.length fl in
81 let n_plus_len = n + len in
83 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
87 i && does_not_occur n ty &&
88 does_not_occur n_plus_len bo
92 (*CSC: potrebbe creare applicazioni di applicazioni *)
93 (*CSC: ora non e' piu' head, ma completa!!! *)
94 let rec head_beta_reduce =
95 let module S = CicSubstitution in
99 | C.Var (uri,exp_named_subst) ->
100 let exp_named_subst' =
101 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
103 C.Var (uri,exp_named_subst)
107 (function None -> None | Some t -> Some (head_beta_reduce t)) l
110 | C.Implicit -> assert false
112 C.Cast (head_beta_reduce te, head_beta_reduce ty)
114 C.Prod (n, head_beta_reduce s, head_beta_reduce t)
115 | C.Lambda (n,s,t) ->
116 C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
118 C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
119 | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
120 let he' = S.subst he t in
124 head_beta_reduce (C.Appl (he'::tl))
126 C.Appl (List.map head_beta_reduce l)
127 | C.Const (uri,exp_named_subst) ->
128 let exp_named_subst' =
129 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
131 C.Const (uri,exp_named_subst')
132 | C.MutInd (uri,i,exp_named_subst) ->
133 let exp_named_subst' =
134 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
136 C.MutInd (uri,i,exp_named_subst')
137 | C.MutConstruct (uri,i,j,exp_named_subst) ->
138 let exp_named_subst' =
139 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
141 C.MutConstruct (uri,i,j,exp_named_subst')
142 | C.MutCase (sp,i,outt,t,pl) ->
143 C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t,
144 List.map head_beta_reduce pl)
148 (function (name,i,ty,bo) ->
149 name,i,head_beta_reduce ty,head_beta_reduce bo
156 (function (name,ty,bo) ->
157 name,head_beta_reduce ty,head_beta_reduce bo
163 (* syntactic_equality up to cookingsno for uris *)
164 (* (which is often syntactically irrilevant), *)
165 (* distinction between fake dependent products *)
166 (* and non-dependent products, alfa-conversion *)
167 (*CSC: must alfa-conversion be considered or not? *)
168 let syntactic_equality t t' =
169 let module C = Cic in
170 let rec syntactic_equality t t' =
174 C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
175 UriManager.eq uri uri' &&
176 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
177 | C.Cast (te,ty), C.Cast (te',ty') ->
178 syntactic_equality te te' &&
179 syntactic_equality ty ty'
180 | C.Prod (_,s,t), C.Prod (_,s',t') ->
181 syntactic_equality s s' &&
182 syntactic_equality t t'
183 | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
184 syntactic_equality s s' &&
185 syntactic_equality t t'
186 | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
187 syntactic_equality s s' &&
188 syntactic_equality t t'
189 | C.Appl l, C.Appl l' ->
190 List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
191 | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
192 UriManager.eq uri uri' &&
193 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
194 | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
195 UriManager.eq uri uri' && i = i' &&
196 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
197 | C.MutConstruct (uri,i,j,exp_named_subst),
198 C.MutConstruct (uri',i',j',exp_named_subst') ->
199 UriManager.eq uri uri' && i = i' && j = j' &&
200 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
201 | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
202 UriManager.eq sp sp' && i = i' &&
203 syntactic_equality outt outt' &&
204 syntactic_equality t t' &&
206 (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
207 | C.Fix (i,fl), C.Fix (i',fl') ->
210 (fun b (_,i,ty,bo) (_,i',ty',bo') ->
212 syntactic_equality ty ty' &&
213 syntactic_equality bo bo') true fl fl'
214 | C.CoFix (i,fl), C.CoFix (i',fl') ->
217 (fun b (_,ty,bo) (_,ty',bo') ->
219 syntactic_equality ty ty' &&
220 syntactic_equality bo bo') true fl fl'
221 | _, _ -> false (* we already know that t != t' *)
222 and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
224 (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
225 exp_named_subst1 exp_named_subst2
228 syntactic_equality t t'
236 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
237 | (_,_) -> raise ListTooShort
240 let type_of_constant uri =
241 let module C = Cic in
242 let module R = CicReduction in
243 let module U = UriManager in
245 match CicEnvironment.is_type_checked uri with
246 CicEnvironment.CheckedObj cobj -> cobj
247 | CicEnvironment.UncheckedObj uobj ->
248 raise (NotWellTyped "Reference to an unchecked constant")
251 C.Constant (_,_,ty,_) -> ty
252 | C.CurrentProof (_,_,_,ty,_) -> ty
253 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
256 let type_of_variable uri =
257 let module C = Cic in
258 let module R = CicReduction in
259 let module U = UriManager in
260 match CicEnvironment.is_type_checked uri with
261 CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
262 | CicEnvironment.UncheckedObj (C.Variable _) ->
263 raise (NotWellTyped "Reference to an unchecked variable")
264 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
267 let type_of_mutual_inductive_defs uri i =
268 let module C = Cic in
269 let module R = CicReduction in
270 let module U = UriManager in
272 match CicEnvironment.is_type_checked uri with
273 CicEnvironment.CheckedObj cobj -> cobj
274 | CicEnvironment.UncheckedObj uobj ->
275 raise (NotWellTyped "Reference to an unchecked inductive type")
278 C.InductiveDefinition (dl,_,_) ->
279 let (_,_,arity,_) = List.nth dl i in
281 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
284 let type_of_mutual_inductive_constr uri i j =
285 let module C = Cic in
286 let module R = CicReduction in
287 let module U = UriManager in
289 match CicEnvironment.is_type_checked uri with
290 CicEnvironment.CheckedObj cobj -> cobj
291 | CicEnvironment.UncheckedObj uobj ->
292 raise (NotWellTyped "Reference to an unchecked constructor")
295 C.InductiveDefinition (dl,_,_) ->
296 let (_,_,_,cl) = List.nth dl i in
297 let (_,ty) = List.nth cl (j-1) in
299 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
307 let hash = Hashtbl.hash
311 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
312 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
313 (* Coscoy's double type-inference algorithm *)
314 (* It computes the inner-types of every subterm of [t], *)
315 (* even when they are not needed to compute the types *)
316 (* of other terms. *)
317 let rec type_of_aux context t expectedty =
318 let module C = Cic in
319 let module R = CicReduction in
320 let module S = CicSubstitution in
321 let module U = UriManager in
326 match List.nth context (n - 1) with
327 Some (_,C.Decl t) -> S.lift n t
328 | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) expectedty
329 | None -> raise RelToHiddenHypothesis
331 _ -> raise (NotWellTyped "Not a close term")
333 | C.Var (uri,exp_named_subst) ->
334 visit_exp_named_subst context uri exp_named_subst ;
335 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
337 (* Let's visit all the subterms that will not be visited later *)
338 let (_,canonical_context,_) =
339 List.find (function (m,_,_) -> n = m) metasenv
341 let lifted_canonical_context =
345 | (Some (n,C.Decl t))::tl ->
346 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
347 | (Some (n,C.Def t))::tl ->
348 (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
349 | None::tl -> None::(aux (i+1) tl)
351 aux 1 canonical_context
358 | Some t,Some (_,C.Def ct) ->
361 (CicTypeChecker.type_of_aux' metasenv context ct)
363 (* Maybe I am a bit too paranoid, because *)
364 (* if the term is well-typed than t and ct *)
365 (* are convertible. Nevertheless, I compute *)
366 (* the expected type. *)
367 ignore (type_of_aux context t (Some expected_type))
368 | Some t,Some (_,C.Decl ct) ->
369 ignore (type_of_aux context t (Some ct))
370 | _,_ -> assert false (* the term is not well typed!!! *)
371 ) l lifted_canonical_context
373 let (_,canonical_context,ty) =
374 List.find (function (m,_,_) -> n = m) metasenv
376 (* Checks suppressed *)
377 CicSubstitution.lift_meta l ty
378 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
379 | C.Implicit -> raise (Impossible 21)
381 (* Let's visit all the subterms that will not be visited later *)
382 let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
383 let _ = type_of_aux context ty None in
384 (* Checks suppressed *)
386 | C.Prod (name,s,t) ->
387 let sort1 = type_of_aux context s None
388 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
389 sort_of_prod context (name,s) (sort1,sort2)
390 | C.Lambda (n,s,t) ->
391 (* Let's visit all the subterms that will not be visited later *)
392 let _ = type_of_aux context s None in
393 let expected_target_type =
394 match expectedty with
396 | Some expectedty' ->
398 match R.whd context expectedty' with
399 C.Prod (_,_,expected_target_type) ->
400 head_beta_reduce expected_target_type
406 type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
408 (* Checks suppressed *)
411 (*CSC: What are the right expected types for the source and *)
412 (*CSC: target of a LetIn? None used. *)
413 (* Let's visit all the subterms that will not be visited later *)
414 let _ = type_of_aux context s None in
416 (* Checks suppressed *)
417 type_of_aux ((Some (n,(C.Def s)))::context) t None
419 if does_not_occur 1 t_typ then
420 (* since [Rel 1] does not occur in typ, substituting any term *)
421 (* in place of [Rel 1] is equivalent to delifting once *)
422 CicSubstitution.subst C.Implicit t_typ
425 | C.Appl (he::tl) when List.length tl > 0 ->
426 let expected_hetype =
427 (* Inefficient, the head is computed twice. But I know *)
428 (* of no other solution. *)
430 (R.whd context (CicTypeChecker.type_of_aux' metasenv context he)))
432 let hetype = type_of_aux context he (Some expected_hetype) in
433 let tlbody_and_type =
437 | C.Prod (n,s,t),he::tl ->
438 (he, type_of_aux context he (Some (head_beta_reduce s)))::
439 (aux (R.whd context (S.subst he t), tl))
442 aux (expected_hetype, tl)
444 eat_prods context hetype tlbody_and_type
445 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
446 | C.Const (uri,exp_named_subst) ->
447 visit_exp_named_subst context uri exp_named_subst ;
448 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
449 | C.MutInd (uri,i,exp_named_subst) ->
450 visit_exp_named_subst context uri exp_named_subst ;
451 CicSubstitution.subst_vars exp_named_subst
452 (type_of_mutual_inductive_defs uri i)
453 | C.MutConstruct (uri,i,j,exp_named_subst) ->
454 visit_exp_named_subst context uri exp_named_subst ;
455 CicSubstitution.subst_vars exp_named_subst
456 (type_of_mutual_inductive_constr uri i j)
457 | C.MutCase (uri,i,outtype,term,pl) ->
458 let outsort = type_of_aux context outtype None in
459 let (need_dummy, k) =
460 let rec guess_args context t =
461 match CicReduction.whd context t with
462 C.Sort _ -> (true, 0)
463 | C.Prod (name, s, t) ->
464 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
466 (* last prod before sort *)
467 match CicReduction.whd context s with
468 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
470 | C.Appl ((C.MutInd (uri',i',_)) :: _)
471 when U.eq uri' uri && i' = i -> (false, 1)
475 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
477 let (b, k) = guess_args context outsort in
478 if not b then (b, k - 1) else (b, k)
480 let (parameters, arguments,exp_named_subst) =
482 CicTypeChecker.type_of_aux' metasenv context term
485 R.whd context (type_of_aux context term
486 (Some (head_beta_reduce type_of_term)))
488 (*CSC manca il caso dei CAST *)
489 C.MutInd (uri',i',exp_named_subst) ->
490 (* Checks suppressed *)
491 [],[],exp_named_subst
492 | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
494 split tl (List.length tl - k)
495 in params,args,exp_named_subst
497 raise (NotWellTyped "MutCase: the term is not an inductive one")
499 (* Checks suppressed *)
500 (* Let's visit all the subterms that will not be visited later *)
502 match CicEnvironment.get_cooked_obj uri with
503 C.InductiveDefinition (tl,_,parsno) ->
504 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
506 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
512 if parameters = [] then
513 (C.MutConstruct (uri,i,j,exp_named_subst))
515 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
518 type_of_branch context parsno need_dummy outtype cons
519 (CicTypeChecker.type_of_aux' metasenv context cons)
521 ignore (type_of_aux context p
522 (Some (head_beta_reduce expectedtype))) ;
524 ) 1 (List.combine pl cl)
526 if not need_dummy then
527 C.Appl ((outtype::arguments)@[term])
528 else if arguments = [] then
531 C.Appl (outtype::arguments)
533 (* Let's visit all the subterms that will not be visited later *)
538 let _ = type_of_aux context ty None in
539 (Some (C.Name n,(C.Decl ty)))
548 head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
550 ignore (type_of_aux context' bo (Some expectedty))
553 (* Checks suppressed *)
554 let (_,_,ty,_) = List.nth fl i in
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 head_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 synthesized' = head_beta_reduce synthesized in
583 match expectedty with
585 (* No expected type *)
586 {synthesized = synthesized' ; expected = None}, synthesized
587 | Some ty when syntactic_equality synthesized' ty ->
588 (* The expected type is synthactically equal to *)
589 (* the synthesized type. Let's forget it. *)
590 {synthesized = synthesized' ; expected = None}, synthesized
591 | Some expectedty' ->
592 {synthesized = synthesized' ; expected = Some expectedty'},
595 CicHash.add subterms_to_types t types ;
598 and visit_exp_named_subst context uri exp_named_subst =
600 match CicEnvironment.get_cooked_obj uri with
601 Cic.Constant (_,_,_,params)
602 | Cic.CurrentProof (_,_,_,_,params)
603 | Cic.Variable (_,_,_,params)
604 | Cic.InductiveDefinition (_,params,_) ->
607 match CicEnvironment.get_cooked_obj uri with
608 Cic.Variable (_,None,ty,_) -> uri,ty
609 | _ -> assert false (* the theorem is well-typed *)
612 let rec check uris_and_types subst =
613 match uris_and_types,subst with
615 | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
616 ignore (type_of_aux context t (Some ty)) ;
619 (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
622 | _,_ -> assert false (* the theorem is well-typed *)
624 check uris_and_types exp_named_subst
626 and sort_of_prod context (name,s) (t1, t2) =
627 let module C = Cic in
628 let t1' = CicReduction.whd context t1 in
629 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
630 match (t1', t2') with
631 (C.Sort s1, C.Sort s2)
632 when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
634 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
638 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
640 and eat_prods context hetype =
641 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
645 | (hete, hety)::tl ->
646 (match (CicReduction.whd context hetype) with
648 (* Checks suppressed *)
649 eat_prods context (CicSubstitution.subst hete t) tl
650 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
653 and type_of_branch context argsno need_dummy outtype term constype =
654 let module C = Cic in
655 let module R = CicReduction in
656 match R.whd context constype with
661 C.Appl [outtype ; term]
662 | C.Appl (C.MutInd (_,_,_)::tl) ->
663 let (_,arguments) = split tl argsno
665 if need_dummy && arguments = [] then
668 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
669 | C.Prod (name,so,de) ->
671 match CicSubstitution.lift 1 term with
672 C.Appl l -> C.Appl (l@[C.Rel 1])
673 | t -> C.Appl [t ; C.Rel 1]
675 C.Prod (C.Anonymous,so,type_of_branch
676 ((Some (name,(C.Decl so)))::context) argsno need_dummy
677 (CicSubstitution.lift 1 outtype) term' de)
678 | _ -> raise (Impossible 20)
681 type_of_aux context t expectedty
684 let double_type_of metasenv context t expectedty =
685 let subterms_to_types = CicHash.create 503 in
686 ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;