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.empty_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,dest) ->
68 does_not_occur n so &&
69 does_not_occur (n + 1) dest
71 List.fold_right (fun x i -> i && does_not_occur n x) l true
72 | C.Var (_,exp_named_subst)
73 | C.Const (_,exp_named_subst)
74 | C.MutInd (_,_,exp_named_subst)
75 | C.MutConstruct (_,_,_,exp_named_subst) ->
76 List.fold_right (fun (_,x) i -> i && does_not_occur n x)
78 | C.MutCase (_,_,out,te,pl) ->
79 does_not_occur n out && does_not_occur n te &&
80 List.fold_right (fun x i -> i && does_not_occur n x) pl true
82 let len = List.length fl in
83 let n_plus_len = n + len in
86 i && does_not_occur n ty &&
87 does_not_occur n_plus_len bo
90 let len = List.length fl in
91 let n_plus_len = n + len in
94 i && does_not_occur n ty &&
95 does_not_occur n_plus_len bo
100 let module S = CicSubstitution in
101 let module C = Cic in
104 | C.Var (uri,exp_named_subst) ->
105 let exp_named_subst' =
106 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
108 C.Var (uri,exp_named_subst')
112 (function None -> None | Some t -> Some (beta_reduce t)) l
115 | C.Implicit _ -> assert false
117 C.Cast (beta_reduce te, beta_reduce ty)
119 C.Prod (n, beta_reduce s, beta_reduce t)
120 | C.Lambda (n,s,t) ->
121 C.Lambda (n, beta_reduce s, beta_reduce t)
123 C.LetIn (n, beta_reduce s, beta_reduce t)
124 | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
125 let he' = S.subst he t in
130 C.Appl l -> beta_reduce (C.Appl (l@tl))
131 | _ -> beta_reduce (C.Appl (he'::tl)))
133 C.Appl (List.map beta_reduce l)
134 | C.Const (uri,exp_named_subst) ->
135 let exp_named_subst' =
136 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
138 C.Const (uri,exp_named_subst')
139 | C.MutInd (uri,i,exp_named_subst) ->
140 let exp_named_subst' =
141 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
143 C.MutInd (uri,i,exp_named_subst')
144 | C.MutConstruct (uri,i,j,exp_named_subst) ->
145 let exp_named_subst' =
146 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
148 C.MutConstruct (uri,i,j,exp_named_subst')
149 | C.MutCase (sp,i,outt,t,pl) ->
150 C.MutCase (sp,i,beta_reduce outt,beta_reduce t,
151 List.map beta_reduce pl)
155 (function (name,i,ty,bo) ->
156 name,i,beta_reduce ty,beta_reduce bo
163 (function (name,ty,bo) ->
164 name,beta_reduce ty,beta_reduce bo
173 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
174 | (_,_) -> raise ListTooShort
177 let type_of_constant uri =
178 let module C = Cic in
179 let module R = CicReduction in
180 let module U = UriManager in
182 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
183 CicEnvironment.CheckedObj (cobj,_) -> cobj
184 | CicEnvironment.UncheckedObj uobj ->
185 raise (NotWellTyped "Reference to an unchecked constant")
188 C.Constant (_,_,ty,_,_) -> ty
189 | C.CurrentProof (_,_,_,ty,_,_) -> ty
190 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
193 let type_of_variable uri =
194 let module C = Cic in
195 let module R = CicReduction in
196 let module U = UriManager in
197 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
198 CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
199 | CicEnvironment.UncheckedObj (C.Variable _) ->
200 raise (NotWellTyped "Reference to an unchecked variable")
201 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
204 let type_of_mutual_inductive_defs uri i =
205 let module C = Cic in
206 let module R = CicReduction in
207 let module U = UriManager in
209 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
210 CicEnvironment.CheckedObj (cobj,_) -> cobj
211 | CicEnvironment.UncheckedObj uobj ->
212 raise (NotWellTyped "Reference to an unchecked inductive type")
215 C.InductiveDefinition (dl,_,_,_) ->
216 let (_,_,arity,_) = List.nth dl i in
218 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
221 let type_of_mutual_inductive_constr uri i j =
222 let module C = Cic in
223 let module R = CicReduction in
224 let module U = UriManager in
226 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
227 CicEnvironment.CheckedObj (cobj,_) -> cobj
228 | CicEnvironment.UncheckedObj uobj ->
229 raise (NotWellTyped "Reference to an unchecked constructor")
232 C.InductiveDefinition (dl,_,_,_) ->
233 let (_,_,_,cl) = List.nth dl i in
234 let (_,ty) = List.nth cl (j-1) in
236 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
239 let pack_coercion = ref (fun _ _ _ -> assert false);;
241 let profiler_for_find = HExtlib.profile "CicHash ADD" ;;
243 let cic_CicHash_add a b c =
244 profiler_for_find.HExtlib.profile (Cic.CicHash.add a b) c
247 let profiler_for_find1 = HExtlib.profile "CicHash MEM" ;;
249 let cic_CicHash_mem a b =
250 profiler_for_find1.HExtlib.profile (Cic.CicHash.mem a) b
253 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
254 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
255 (* Coscoy's double type-inference algorithm *)
256 (* It computes the inner-types of every subterm of [t], *)
257 (* even when they are not needed to compute the types *)
258 (* of other terms. *)
259 let rec type_of_aux context t expectedty =
260 let module C = Cic in
261 let module R = CicReduction in
262 let module S = CicSubstitution in
263 let module U = UriManager in
265 match expectedty with
267 | Some t -> Some (!pack_coercion metasenv context t) in
272 match List.nth context (n - 1) with
273 Some (_,C.Decl t) -> S.lift n t
274 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
275 | Some (_,C.Def (bo,None)) ->
276 type_of_aux context (S.lift n bo) expectedty
277 | None -> raise RelToHiddenHypothesis
279 _ -> raise (NotWellTyped "Not a close term")
281 | C.Var (uri,exp_named_subst) ->
282 visit_exp_named_subst context uri exp_named_subst ;
283 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
285 (* Let's visit all the subterms that will not be visited later *)
286 let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
287 let lifted_canonical_context =
291 | (Some (n,C.Decl t))::tl ->
292 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
293 | (Some (n,C.Def (t,None)))::tl ->
294 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
296 | None::tl -> None::(aux (i+1) tl)
297 | (Some (_,C.Def (_,Some _)))::_ -> assert false
299 aux 1 canonical_context
306 | Some t,Some (_,C.Def (ct,_)) ->
308 match xxx_type_of_aux' metasenv context ct with
310 | Some t -> Some (R.whd context t)
312 (* Maybe I am a bit too paranoid, because *)
313 (* if the term is well-typed than t and ct *)
314 (* are convertible. Nevertheless, I compute *)
315 (* the expected type. *)
316 ignore (type_of_aux context t expected_type)
317 | Some t,Some (_,C.Decl ct) ->
318 ignore (type_of_aux context t (Some ct))
319 | _,_ -> assert false (* the term is not well typed!!! *)
320 ) l lifted_canonical_context
322 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
323 (* Checks suppressed *)
324 CicSubstitution.subst_meta l ty
325 | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
326 C.Sort (C.Type (CicUniv.fresh()))
327 | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)
328 | C.Implicit _ -> raise (Impossible 21)
330 (* Let's visit all the subterms that will not be visited later *)
331 let _ = type_of_aux context te (Some (beta_reduce ty)) in
332 let _ = type_of_aux context ty None in
333 (* Checks suppressed *)
335 | C.Prod (name,s,t) ->
336 let sort1 = type_of_aux context s None
337 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
338 sort_of_prod context (name,s) (sort1,sort2)
339 | C.Lambda (n,s,t) ->
340 (* Let's visit all the subterms that will not be visited later *)
341 let _ = type_of_aux context s None in
342 let expected_target_type =
343 match expectedty with
345 | Some expectedty' ->
347 match R.whd context expectedty' with
348 C.Prod (_,_,expected_target_type) ->
349 beta_reduce expected_target_type
355 type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
357 (* Checks suppressed *)
360 (*CSC: What are the right expected types for the source and *)
361 (*CSC: target of a LetIn? None used. *)
362 (* Let's visit all the subterms that will not be visited later *)
363 let ty = type_of_aux context s None in
365 (* Checks suppressed *)
366 type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None
367 in (* CicSubstitution.subst s t_typ *)
368 if does_not_occur 1 t_typ then
369 (* since [Rel 1] does not occur in typ, substituting any term *)
370 (* in place of [Rel 1] is equivalent to delifting once *)
371 CicSubstitution.subst (C.Implicit None) t_typ
374 | C.Appl (he::tl) when List.length tl > 0 ->
376 let expected_hetype =
377 (* Inefficient, the head is computed twice. But I know *)
378 (* of no other solution. *)
380 (R.whd context (xxx_type_of_aux' metasenv context he)))
382 let hetype = type_of_aux context he (Some expected_hetype) in
383 let tlbody_and_type =
387 | C.Prod (n,s,t),he::tl ->
388 (he, type_of_aux context he (Some (beta_reduce s)))::
389 (aux (R.whd context (S.subst he t), tl))
392 aux (expected_hetype, tl) *)
393 let hetype = R.whd context (type_of_aux context he None) in
394 let tlbody_and_type =
398 | C.Prod (n,s,t),he::tl ->
399 (he, type_of_aux context he (Some (beta_reduce s)))::
400 (aux (R.whd context (S.subst he t), tl))
405 eat_prods context hetype tlbody_and_type
406 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
407 | C.Const (uri,exp_named_subst) ->
408 visit_exp_named_subst context uri exp_named_subst ;
409 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
410 | C.MutInd (uri,i,exp_named_subst) ->
411 visit_exp_named_subst context uri exp_named_subst ;
412 CicSubstitution.subst_vars exp_named_subst
413 (type_of_mutual_inductive_defs uri i)
414 | C.MutConstruct (uri,i,j,exp_named_subst) ->
415 visit_exp_named_subst context uri exp_named_subst ;
416 CicSubstitution.subst_vars exp_named_subst
417 (type_of_mutual_inductive_constr uri i j)
418 | C.MutCase (uri,i,outtype,term,pl) ->
419 let outsort = type_of_aux context outtype None in
420 let (need_dummy, k) =
421 let rec guess_args context t =
422 match CicReduction.whd context t with
423 C.Sort _ -> (true, 0)
424 | C.Prod (name, s, t) ->
425 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
427 (* last prod before sort *)
428 match CicReduction.whd context s with
429 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
431 | C.Appl ((C.MutInd (uri',i',_)) :: _)
432 when U.eq uri' uri && i' = i -> (false, 1)
436 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
438 let (b, k) = guess_args context outsort in
439 if not b then (b, k - 1) else (b, k)
441 let (parameters, arguments,exp_named_subst) =
443 match xxx_type_of_aux' metasenv context term with
445 | Some t -> Some (beta_reduce t)
448 R.whd context (type_of_aux context term type_of_term)
450 (*CSC manca il caso dei CAST *)
451 C.MutInd (uri',i',exp_named_subst) ->
452 (* Checks suppressed *)
453 [],[],exp_named_subst
454 | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
456 split tl (List.length tl - k)
457 in params,args,exp_named_subst
459 raise (NotWellTyped "MutCase: the term is not an inductive one")
461 (* Checks suppressed *)
462 (* Let's visit all the subterms that will not be visited later *)
466 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
467 with Not_found -> assert false
470 C.InductiveDefinition (tl,_,parsno,_) ->
471 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
473 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
479 if parameters = [] then
480 (C.MutConstruct (uri,i,j,exp_named_subst))
482 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
485 match xxx_type_of_aux' metasenv context cons with
490 (type_of_branch context parsno need_dummy outtype
493 ignore (type_of_aux context p expectedtype);
495 ) 1 (List.combine pl cl)
497 if not need_dummy then
498 C.Appl ((outtype::arguments)@[term])
499 else if arguments = [] then
502 C.Appl (outtype::arguments)
504 (* Let's visit all the subterms that will not be visited later *)
509 let _ = type_of_aux context ty None in
510 (Some (C.Name n,(C.Decl ty)))
519 beta_reduce (CicSubstitution.lift (List.length fl) ty)
521 ignore (type_of_aux context' bo (Some expectedty))
524 (* Checks suppressed *)
525 let (_,_,ty,_) = List.nth fl i in
528 (* Let's visit all the subterms that will not be visited later *)
533 let _ = type_of_aux context ty None in
534 (Some (C.Name n,(C.Decl ty)))
543 beta_reduce (CicSubstitution.lift (List.length fl) ty)
545 ignore (type_of_aux context' bo (Some expectedty))
548 (* Checks suppressed *)
549 let (_,ty,_) = List.nth fl i in
552 let synthesized' = beta_reduce synthesized in
553 let synthesized' = !pack_coercion metasenv context synthesized' in
555 match expectedty with
557 (* No expected type *)
558 {synthesized = synthesized' ; expected = None}, synthesized
559 | Some ty when CicUtil.alpha_equivalence synthesized' ty ->
560 (* The expected type is synthactically equal to *)
561 (* the synthesized type. Let's forget it. *)
562 {synthesized = synthesized' ; expected = None}, synthesized
563 | Some expectedty' ->
564 {synthesized = synthesized' ; expected = Some expectedty'},
567 (* assert (not (cic_CicHash_mem subterms_to_types t));*)
568 cic_CicHash_add subterms_to_types t types ;
571 and visit_exp_named_subst context uri exp_named_subst =
575 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
576 with Not_found -> assert false
578 let params = CicUtil.params_of_obj obj in
583 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
584 with Not_found -> assert false
587 Cic.Variable (_,None,ty,_,_) -> uri,ty
588 | _ -> assert false (* the theorem is well-typed *)
591 let rec check uris_and_types subst =
592 match uris_and_types,subst with
594 | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
595 ignore (type_of_aux context t (Some ty)) ;
598 (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
601 | _,_ -> assert false (* the theorem is well-typed *)
603 check uris_and_types exp_named_subst
605 and sort_of_prod context (name,s) (t1, t2) =
606 let module C = Cic in
607 let t1' = CicReduction.whd context t1 in
608 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
609 match (t1', t2') with
610 (C.Sort _, C.Sort s2)
611 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
612 (* different from Coq manual!!! *)
614 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
615 C.Sort (C.Type (CicUniv.fresh()))
616 | (C.Sort _,C.Sort (C.Type t1)) ->
617 (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
618 C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
619 | (C.Meta _, C.Sort _) -> t2'
620 | (C.Meta _, (C.Meta (_,_) as t))
621 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
626 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
628 and eat_prods context hetype =
629 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
633 | (hete, hety)::tl ->
634 (match (CicReduction.whd context hetype) with
636 (* Checks suppressed *)
637 eat_prods context (CicSubstitution.subst hete t) tl
638 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
641 and type_of_branch context argsno need_dummy outtype term constype =
642 let module C = Cic in
643 let module R = CicReduction in
644 match R.whd context constype with
649 C.Appl [outtype ; term]
650 | C.Appl (C.MutInd (_,_,_)::tl) ->
651 let (_,arguments) = split tl argsno
653 if need_dummy && arguments = [] then
656 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
657 | C.Prod (name,so,de) ->
659 match CicSubstitution.lift 1 term with
660 C.Appl l -> C.Appl (l@[C.Rel 1])
661 | t -> C.Appl [t ; C.Rel 1]
663 C.Prod (C.Anonymous,so,type_of_branch
664 ((Some (name,(C.Decl so)))::context) argsno need_dummy
665 (CicSubstitution.lift 1 outtype) term' de)
666 | _ -> raise (Impossible 20)
669 type_of_aux context t expectedty
672 let double_type_of metasenv context t expectedty =
673 let subterms_to_types = Cic.CicHash.create 503 in
674 ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;