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 (*CSC: must alfa-conversion be considered or not? *)
38 let xxx_type_of_aux' m c t =
40 Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph))
42 | CicTypeChecker.TypeCheckerFailure _ -> None (* because eta_expansion *)
45 type types = {synthesized : Cic.term ; expected : Cic.term option};;
47 (* does_not_occur n te *)
48 (* returns [true] if [Rel n] does not occur in [te] *)
49 let rec does_not_occur n =
52 C.Rel m when m = n -> false
54 (* FG/CSC: maybe we assume the meta is guarded so we do not recur on its *)
55 (* explicit subsitutions (copied from the kernel) ??? *)
58 | C.Implicit _ -> true
60 does_not_occur n te && does_not_occur n ty
61 | C.Prod (name,so,dest) ->
62 does_not_occur n so &&
63 does_not_occur (n + 1) dest
64 | C.Lambda (name,so,dest) ->
65 does_not_occur n so &&
66 does_not_occur (n + 1) dest
67 | C.LetIn (name,so,ty,dest) ->
68 does_not_occur n so &&
69 does_not_occur n ty &&
70 does_not_occur (n + 1) dest
72 List.fold_right (fun x i -> i && does_not_occur n x) l true
73 | C.Var (_,exp_named_subst)
74 | C.Const (_,exp_named_subst)
75 | C.MutInd (_,_,exp_named_subst)
76 | C.MutConstruct (_,_,_,exp_named_subst) ->
77 List.fold_right (fun (_,x) i -> i && does_not_occur n x)
79 | C.MutCase (_,_,out,te,pl) ->
80 does_not_occur n out && does_not_occur n te &&
81 List.fold_right (fun x i -> i && does_not_occur n x) pl true
83 let len = List.length fl in
84 let n_plus_len = n + len in
87 i && does_not_occur n ty &&
88 does_not_occur n_plus_len bo
91 let len = List.length fl in
92 let n_plus_len = n + len in
95 i && does_not_occur n ty &&
96 does_not_occur n_plus_len bo
100 (* FG: if ~clean:true, unreferenced letins are removed *)
101 (* (beta-reducttion can cause unreferenced letins) *)
102 let rec beta_reduce ?(clean=false)=
103 let module S = CicSubstitution in
104 let module C = Cic in
107 | C.Var (uri,exp_named_subst) ->
108 let exp_named_subst' =
109 List.map (function (i,t) -> i, beta_reduce ~clean t) exp_named_subst
111 C.Var (uri,exp_named_subst')
115 (function None -> None | Some t -> Some (beta_reduce ~clean t)) l
118 | C.Implicit _ -> assert false
120 C.Cast (beta_reduce ~clean te, beta_reduce ~clean ty)
122 C.Prod (n, beta_reduce ~clean s, beta_reduce ~clean t)
123 | C.Lambda (n,s,t) ->
124 C.Lambda (n, beta_reduce ~clean s, beta_reduce ~clean t)
125 | C.LetIn (n,s,ty,t) ->
126 let t' = beta_reduce ~clean t in
127 if clean && does_not_occur 1 t' then
128 (* since [Rel 1] does not occur in typ, substituting any term *)
129 (* in place of [Rel 1] is equivalent to delifting once *)
130 CicSubstitution.subst (C.Implicit None) t'
132 C.LetIn (n, beta_reduce ~clean s, beta_reduce ~clean ty, t')
133 | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
134 let he' = S.subst he t in
136 beta_reduce ~clean he'
139 C.Appl l -> beta_reduce ~clean (C.Appl (l@tl))
140 | _ -> beta_reduce ~clean (C.Appl (he'::tl)))
142 C.Appl (List.map (beta_reduce ~clean) l)
143 | C.Const (uri,exp_named_subst) ->
144 let exp_named_subst' =
145 List.map (function (i,t) -> i, beta_reduce ~clean 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, beta_reduce ~clean 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, beta_reduce ~clean 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,beta_reduce ~clean outt,beta_reduce ~clean t,
160 List.map (beta_reduce ~clean) pl)
164 (function (name,i,ty,bo) ->
165 name,i,beta_reduce ~clean ty,beta_reduce ~clean bo
172 (function (name,ty,bo) ->
173 name,beta_reduce ~clean ty,beta_reduce ~clean bo
182 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
183 | (_,_) -> raise ListTooShort
186 let type_of_constant uri =
187 let module C = Cic in
188 let module R = CicReduction in
189 let module U = UriManager in
191 match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
192 CicEnvironment.CheckedObj (cobj,_) -> cobj
193 | CicEnvironment.UncheckedObj (uobj,_) ->
194 raise (NotWellTyped "Reference to an unchecked constant")
197 C.Constant (_,_,ty,_,_) -> ty
198 | C.CurrentProof (_,_,_,ty,_,_) -> ty
199 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
202 let type_of_variable uri =
203 let module C = Cic in
204 let module R = CicReduction in
205 let module U = UriManager in
206 match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
207 CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
208 | CicEnvironment.UncheckedObj (C.Variable _,_) ->
209 raise (NotWellTyped "Reference to an unchecked variable")
210 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
213 let type_of_mutual_inductive_defs uri i =
214 let module C = Cic in
215 let module R = CicReduction in
216 let module U = UriManager in
218 match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
219 CicEnvironment.CheckedObj (cobj,_) -> cobj
220 | CicEnvironment.UncheckedObj (uobj,_) ->
221 raise (NotWellTyped "Reference to an unchecked inductive type")
224 C.InductiveDefinition (dl,_,_,_) ->
225 let (_,_,arity,_) = List.nth dl i in
227 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
230 let type_of_mutual_inductive_constr uri i j =
231 let module C = Cic in
232 let module R = CicReduction in
233 let module U = UriManager in
235 match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
236 CicEnvironment.CheckedObj (cobj,_) -> cobj
237 | CicEnvironment.UncheckedObj (uobj,_) ->
238 raise (NotWellTyped "Reference to an unchecked constructor")
241 C.InductiveDefinition (dl,_,_,_) ->
242 let (_,_,_,cl) = List.nth dl i in
243 let (_,ty) = List.nth cl (j-1) in
245 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
248 let pack_coercion = ref (fun _ _ _ -> assert false);;
250 let profiler_for_find = HExtlib.profile "CicHash ADD" ;;
252 let cic_CicHash_add a b c =
253 profiler_for_find.HExtlib.profile (Cic.CicHash.add a b) c
256 let profiler_for_find1 = HExtlib.profile "CicHash MEM" ;;
258 let cic_CicHash_mem a b =
259 profiler_for_find1.HExtlib.profile (Cic.CicHash.mem a) b
262 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
263 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
264 (* Coscoy's double type-inference algorithm *)
265 (* It computes the inner-types of every subterm of [t], *)
266 (* even when they are not needed to compute the types *)
267 (* of other terms. *)
268 let rec type_of_aux context t expectedty =
269 let module C = Cic in
270 let module R = CicReduction in
271 let module S = CicSubstitution in
272 let module U = UriManager in
274 match expectedty with
276 | Some t -> Some (!pack_coercion metasenv context t) in
281 match List.nth context (n - 1) with
282 Some (_,C.Decl t) -> S.lift n t
283 | Some (_,C.Def (_,ty)) -> S.lift n ty
284 | None -> raise RelToHiddenHypothesis
286 _ -> raise (NotWellTyped "Not a close term")
288 | C.Var (uri,exp_named_subst) ->
289 visit_exp_named_subst context uri exp_named_subst ;
290 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
292 (* Let's visit all the subterms that will not be visited later *)
293 let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
294 let lifted_canonical_context =
298 | (Some (n,C.Decl t))::tl ->
299 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
300 | (Some (n,C.Def (t,ty)))::tl ->
303 ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i t))))::
305 | None::tl -> None::(aux (i+1) tl)
307 aux 1 canonical_context
314 | Some t,Some (_,C.Def (ct,_)) ->
316 match xxx_type_of_aux' metasenv context ct with
318 | Some t -> Some (R.whd context t)
320 (* Maybe I am a bit too paranoid, because *)
321 (* if the term is well-typed than t and ct *)
322 (* are convertible. Nevertheless, I compute *)
323 (* the expected type. *)
324 ignore (type_of_aux context t expected_type)
325 | Some t,Some (_,C.Decl ct) ->
326 ignore (type_of_aux context t (Some ct))
327 | _,_ -> assert false (* the term is not well typed!!! *)
328 ) l lifted_canonical_context
330 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
331 (* Checks suppressed *)
332 CicSubstitution.subst_meta l ty
333 | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
334 C.Sort (C.Type (CicUniv.fresh()))
335 | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)
336 | C.Implicit _ -> raise (Impossible 21)
338 (* Let's visit all the subterms that will not be visited later *)
339 let _ = type_of_aux context te (Some (beta_reduce ty)) in
340 let _ = type_of_aux context ty None in
341 (* Checks suppressed *)
343 | C.Prod (name,s,t) ->
344 let sort1 = type_of_aux context s None
345 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
346 sort_of_prod context (name,s) (sort1,sort2)
347 | C.Lambda (n,s,t) ->
348 (* Let's visit all the subterms that will not be visited later *)
349 let _ = type_of_aux context s None in
350 let n, expected_target_type =
351 match expectedty with
353 | Some expectedty' ->
355 match R.whd context expectedty' with
356 | C.Prod (n',_,expected_target_type) ->
357 let xtt = beta_reduce expected_target_type in
358 if n <> C.Anonymous then n, xtt else n', xtt
364 type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
366 (* Checks suppressed *)
368 | C.LetIn (n,s,ty,t) ->
369 (*CSC: What are the right expected types for the source and *)
370 (*CSC: target of a LetIn? None used. *)
371 (* Let's visit all the subterms that will not be visited later *)
372 let _ = type_of_aux context ty None in
373 let _ = type_of_aux context s (Some ty) in
375 (* Checks suppressed *)
376 type_of_aux ((Some (n,(C.Def (s,ty))))::context) t None
377 in (* CicSubstitution.subst s t_typ *)
378 if does_not_occur 1 t_typ then
379 (* since [Rel 1] does not occur in typ, substituting any term *)
380 (* in place of [Rel 1] is equivalent to delifting once *)
381 CicSubstitution.subst (C.Implicit None) t_typ
383 C.LetIn (n,s,ty,t_typ)
384 | C.Appl (he::tl) when List.length tl > 0 ->
386 let expected_hetype =
387 (* Inefficient, the head is computed twice. But I know *)
388 (* of no other solution. *)
390 (R.whd context (xxx_type_of_aux' metasenv context he)))
392 let hetype = type_of_aux context he (Some expected_hetype) in
393 let tlbody_and_type =
397 | C.Prod (n,s,t),he::tl ->
398 (he, type_of_aux context he (Some (beta_reduce s)))::
399 (aux (R.whd context (S.subst he t), tl))
402 aux (expected_hetype, tl) *)
403 let hetype = R.whd context (type_of_aux context he None) in
404 let tlbody_and_type =
408 | C.Prod (n,s,t),he::tl ->
409 (he, type_of_aux context he (Some (beta_reduce s)))::
410 (aux (R.whd context (S.subst he t), tl))
415 eat_prods context hetype tlbody_and_type
416 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
417 | C.Const (uri,exp_named_subst) ->
418 visit_exp_named_subst context uri exp_named_subst ;
419 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
420 | C.MutInd (uri,i,exp_named_subst) ->
421 visit_exp_named_subst context uri exp_named_subst ;
422 CicSubstitution.subst_vars exp_named_subst
423 (type_of_mutual_inductive_defs uri i)
424 | C.MutConstruct (uri,i,j,exp_named_subst) ->
425 visit_exp_named_subst context uri exp_named_subst ;
426 CicSubstitution.subst_vars exp_named_subst
427 (type_of_mutual_inductive_constr uri i j)
428 | C.MutCase (uri,i,outtype,term,pl) ->
429 let outsort = type_of_aux context outtype None in
430 let (need_dummy, k) =
431 let rec guess_args context t =
432 match CicReduction.whd context t with
433 C.Sort _ -> (true, 0)
434 | C.Prod (name, s, t) ->
435 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
437 (* last prod before sort *)
438 match CicReduction.whd context s with
439 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
441 | C.Appl ((C.MutInd (uri',i',_)) :: _)
442 when U.eq uri' uri && i' = i -> (false, 1)
446 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
448 let (b, k) = guess_args context outsort in
449 if not b then (b, k - 1) else (b, k)
451 let (parameters, arguments,exp_named_subst) =
453 match xxx_type_of_aux' metasenv context term with
455 | Some t -> Some (beta_reduce t)
458 R.whd context (type_of_aux context term type_of_term)
460 (*CSC manca il caso dei CAST *)
461 C.MutInd (uri',i',exp_named_subst) ->
462 (* Checks suppressed *)
463 [],[],exp_named_subst
464 | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
466 split tl (List.length tl - k)
467 in params,args,exp_named_subst
469 raise (NotWellTyped "MutCase: the term is not an inductive one")
471 (* Checks suppressed *)
472 (* Let's visit all the subterms that will not be visited later *)
476 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
477 with Not_found -> assert false
480 C.InductiveDefinition (tl,_,parsno,_) ->
481 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
483 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
489 if parameters = [] then
490 (C.MutConstruct (uri,i,j,exp_named_subst))
492 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
495 match xxx_type_of_aux' metasenv context cons with
500 (type_of_branch context parsno need_dummy outtype
503 ignore (type_of_aux context p expectedtype);
505 ) 1 (List.combine pl cl)
507 if not need_dummy then
508 C.Appl ((outtype::arguments)@[term])
509 else if arguments = [] then
512 C.Appl (outtype::arguments)
514 (* Let's visit all the subterms that will not be visited later *)
519 let _ = type_of_aux context ty None in
520 (Some (C.Name n,(C.Decl ty)))
529 beta_reduce (CicSubstitution.lift (List.length fl) ty)
531 ignore (type_of_aux context' bo (Some expectedty))
534 (* Checks suppressed *)
535 let (_,_,ty,_) = List.nth fl i in
538 (* Let's visit all the subterms that will not be visited later *)
543 let _ = type_of_aux context ty None in
544 (Some (C.Name n,(C.Decl ty)))
553 beta_reduce (CicSubstitution.lift (List.length fl) ty)
555 ignore (type_of_aux context' bo (Some expectedty))
558 (* Checks suppressed *)
559 let (_,ty,_) = List.nth fl i in
562 (* FG: beta-reduction can cause unreferenced letins *)
563 let synthesized' = beta_reduce ~clean:true synthesized in
564 let synthesized' = !pack_coercion metasenv context synthesized' in
566 match expectedty with
568 (* No expected type *)
569 {synthesized = synthesized' ; expected = None}, synthesized
570 | Some ty when CicUtil.alpha_equivalence synthesized' ty ->
571 (* The expected type is synthactically equal to *)
572 (* the synthesized type. Let's forget it. *)
573 {synthesized = synthesized' ; expected = None}, synthesized
574 | Some expectedty' ->
575 {synthesized = synthesized' ; expected = Some expectedty'},
578 (* assert (not (cic_CicHash_mem subterms_to_types t));*)
579 cic_CicHash_add subterms_to_types t types ;
582 and visit_exp_named_subst context uri exp_named_subst =
586 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
587 with Not_found -> assert false
589 let params = CicUtil.params_of_obj obj in
594 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
595 with Not_found -> assert false
598 Cic.Variable (_,None,ty,_,_) -> uri,ty
599 | _ -> assert false (* the theorem is well-typed *)
602 let rec check uris_and_types subst =
603 match uris_and_types,subst with
605 | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
606 ignore (type_of_aux context t (Some ty)) ;
609 (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
612 | _,_ -> assert false (* the theorem is well-typed *)
614 check uris_and_types exp_named_subst
616 and sort_of_prod context (name,s) (t1, t2) =
617 let module C = Cic in
618 let t1' = CicReduction.whd context t1 in
619 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
620 match (t1', t2') with
621 | (C.Sort _, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> C.Sort s2
622 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->C.Sort(C.Type(CicUniv.fresh()))
623 | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1)
624 | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1)
625 | (C.Meta _, C.Sort _) -> t2'
626 | (C.Meta _, (C.Meta (_,_) as t))
627 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
632 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
634 and eat_prods context hetype =
635 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
639 | (hete, hety)::tl ->
640 (match (CicReduction.whd context hetype) with
642 (* Checks suppressed *)
643 eat_prods context (CicSubstitution.subst hete t) tl
644 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
647 and type_of_branch context argsno need_dummy outtype term constype =
648 let module C = Cic in
649 let module R = CicReduction in
650 match R.whd context constype with
655 C.Appl [outtype ; term]
656 | C.Appl (C.MutInd (_,_,_)::tl) ->
657 let (_,arguments) = split tl argsno
659 if need_dummy && arguments = [] then
662 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
663 | C.Prod (name,so,de) ->
665 match CicSubstitution.lift 1 term with
666 C.Appl l -> C.Appl (l@[C.Rel 1])
667 | t -> C.Appl [t ; C.Rel 1]
669 C.Prod (C.Anonymous,so,type_of_branch
670 ((Some (name,(C.Decl so)))::context) argsno need_dummy
671 (CicSubstitution.lift 1 outtype) term' de)
672 | _ -> raise (Impossible 20)
675 type_of_aux context t expectedty
678 let double_type_of metasenv context t expectedty =
679 let subterms_to_types = Cic.CicHash.create 503 in
680 ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;