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 let rec beta_reduce =
101 let module S = CicSubstitution in
102 let module C = Cic in
105 | C.Var (uri,exp_named_subst) ->
106 let exp_named_subst' =
107 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
109 C.Var (uri,exp_named_subst')
113 (function None -> None | Some t -> Some (beta_reduce t)) l
116 | C.Implicit _ -> assert false
118 C.Cast (beta_reduce te, beta_reduce ty)
120 C.Prod (n, beta_reduce s, beta_reduce t)
121 | C.Lambda (n,s,t) ->
122 C.Lambda (n, beta_reduce s, beta_reduce t)
123 | C.LetIn (n,s,ty,t) ->
124 C.LetIn (n, beta_reduce s, beta_reduce ty, beta_reduce t)
125 | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
126 let he' = S.subst he t in
131 C.Appl l -> beta_reduce (C.Appl (l@tl))
132 | _ -> beta_reduce (C.Appl (he'::tl)))
134 C.Appl (List.map beta_reduce l)
135 | C.Const (uri,exp_named_subst) ->
136 let exp_named_subst' =
137 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
139 C.Const (uri,exp_named_subst')
140 | C.MutInd (uri,i,exp_named_subst) ->
141 let exp_named_subst' =
142 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
144 C.MutInd (uri,i,exp_named_subst')
145 | C.MutConstruct (uri,i,j,exp_named_subst) ->
146 let exp_named_subst' =
147 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
149 C.MutConstruct (uri,i,j,exp_named_subst')
150 | C.MutCase (sp,i,outt,t,pl) ->
151 C.MutCase (sp,i,beta_reduce outt,beta_reduce t,
152 List.map beta_reduce pl)
156 (function (name,i,ty,bo) ->
157 name,i,beta_reduce ty,beta_reduce bo
164 (function (name,ty,bo) ->
165 name,beta_reduce ty,beta_reduce bo
174 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
175 | (_,_) -> raise ListTooShort
178 let type_of_constant uri =
179 let module C = Cic in
180 let module R = CicReduction in
181 let module U = UriManager in
183 match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
184 CicEnvironment.CheckedObj (cobj,_) -> cobj
185 | CicEnvironment.UncheckedObj (uobj,_) ->
186 raise (NotWellTyped "Reference to an unchecked constant")
189 C.Constant (_,_,ty,_,_) -> ty
190 | C.CurrentProof (_,_,_,ty,_,_) -> ty
191 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
194 let type_of_variable uri =
195 let module C = Cic in
196 let module R = CicReduction in
197 let module U = UriManager in
198 match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
199 CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
200 | CicEnvironment.UncheckedObj (C.Variable _,_) ->
201 raise (NotWellTyped "Reference to an unchecked variable")
202 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
205 let type_of_mutual_inductive_defs uri i =
206 let module C = Cic in
207 let module R = CicReduction in
208 let module U = UriManager in
210 match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
211 CicEnvironment.CheckedObj (cobj,_) -> cobj
212 | CicEnvironment.UncheckedObj (uobj,_) ->
213 raise (NotWellTyped "Reference to an unchecked inductive type")
216 C.InductiveDefinition (dl,_,_,_) ->
217 let (_,_,arity,_) = List.nth dl i in
219 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
222 let type_of_mutual_inductive_constr uri i j =
223 let module C = Cic in
224 let module R = CicReduction in
225 let module U = UriManager in
227 match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
228 CicEnvironment.CheckedObj (cobj,_) -> cobj
229 | CicEnvironment.UncheckedObj (uobj,_) ->
230 raise (NotWellTyped "Reference to an unchecked constructor")
233 C.InductiveDefinition (dl,_,_,_) ->
234 let (_,_,_,cl) = List.nth dl i in
235 let (_,ty) = List.nth cl (j-1) in
237 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
240 let pack_coercion = ref (fun _ _ _ -> assert false);;
242 let profiler_for_find = HExtlib.profile "CicHash ADD" ;;
244 let cic_CicHash_add a b c =
245 profiler_for_find.HExtlib.profile (Cic.CicHash.add a b) c
248 let profiler_for_find1 = HExtlib.profile "CicHash MEM" ;;
250 let cic_CicHash_mem a b =
251 profiler_for_find1.HExtlib.profile (Cic.CicHash.mem a) b
254 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
255 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
256 (* Coscoy's double type-inference algorithm *)
257 (* It computes the inner-types of every subterm of [t], *)
258 (* even when they are not needed to compute the types *)
259 (* of other terms. *)
260 let rec type_of_aux context t expectedty =
261 let module C = Cic in
262 let module R = CicReduction in
263 let module S = CicSubstitution in
264 let module U = UriManager in
266 match expectedty with
268 | Some t -> Some (!pack_coercion metasenv context t) in
273 match List.nth context (n - 1) with
274 Some (_,C.Decl t) -> S.lift n t
275 | Some (_,C.Def (_,ty)) -> S.lift n ty
276 | None -> raise RelToHiddenHypothesis
278 _ -> raise (NotWellTyped "Not a close term")
280 | C.Var (uri,exp_named_subst) ->
281 visit_exp_named_subst context uri exp_named_subst ;
282 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
284 (* Let's visit all the subterms that will not be visited later *)
285 let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
286 let lifted_canonical_context =
290 | (Some (n,C.Decl t))::tl ->
291 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
292 | (Some (n,C.Def (t,ty)))::tl ->
295 ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i t))))::
297 | None::tl -> None::(aux (i+1) tl)
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 n, expected_target_type =
343 match expectedty with
345 | Some expectedty' ->
347 match R.whd context expectedty' with
348 | C.Prod (n',_,expected_target_type) ->
349 let xtt = beta_reduce expected_target_type in
350 if n <> C.Anonymous then n, xtt else n', xtt
356 type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
358 (* Checks suppressed *)
360 | C.LetIn (n,s,ty,t) ->
361 (*CSC: What are the right expected types for the source and *)
362 (*CSC: target of a LetIn? None used. *)
363 (* Let's visit all the subterms that will not be visited later *)
364 let _ = type_of_aux context ty None in
365 let _ = type_of_aux context s (Some ty) in
367 (* Checks suppressed *)
368 type_of_aux ((Some (n,(C.Def (s,ty))))::context) t None
369 in (* CicSubstitution.subst s t_typ *)
370 if does_not_occur 1 t_typ then
371 (* since [Rel 1] does not occur in typ, substituting any term *)
372 (* in place of [Rel 1] is equivalent to delifting once *)
373 CicSubstitution.subst (C.Implicit None) t_typ
375 C.LetIn (n,s,ty,t_typ)
376 | C.Appl (he::tl) when List.length tl > 0 ->
378 let expected_hetype =
379 (* Inefficient, the head is computed twice. But I know *)
380 (* of no other solution. *)
382 (R.whd context (xxx_type_of_aux' metasenv context he)))
384 let hetype = type_of_aux context he (Some expected_hetype) in
385 let tlbody_and_type =
389 | C.Prod (n,s,t),he::tl ->
390 (he, type_of_aux context he (Some (beta_reduce s)))::
391 (aux (R.whd context (S.subst he t), tl))
394 aux (expected_hetype, tl) *)
395 let hetype = R.whd context (type_of_aux context he None) in
396 let tlbody_and_type =
400 | C.Prod (n,s,t),he::tl ->
401 (he, type_of_aux context he (Some (beta_reduce s)))::
402 (aux (R.whd context (S.subst he t), tl))
407 eat_prods context hetype tlbody_and_type
408 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
409 | C.Const (uri,exp_named_subst) ->
410 visit_exp_named_subst context uri exp_named_subst ;
411 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
412 | C.MutInd (uri,i,exp_named_subst) ->
413 visit_exp_named_subst context uri exp_named_subst ;
414 CicSubstitution.subst_vars exp_named_subst
415 (type_of_mutual_inductive_defs uri i)
416 | C.MutConstruct (uri,i,j,exp_named_subst) ->
417 visit_exp_named_subst context uri exp_named_subst ;
418 CicSubstitution.subst_vars exp_named_subst
419 (type_of_mutual_inductive_constr uri i j)
420 | C.MutCase (uri,i,outtype,term,pl) ->
421 let outsort = type_of_aux context outtype None in
422 let (need_dummy, k) =
423 let rec guess_args context t =
424 match CicReduction.whd context t with
425 C.Sort _ -> (true, 0)
426 | C.Prod (name, s, t) ->
427 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
429 (* last prod before sort *)
430 match CicReduction.whd context s with
431 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
433 | C.Appl ((C.MutInd (uri',i',_)) :: _)
434 when U.eq uri' uri && i' = i -> (false, 1)
438 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
440 let (b, k) = guess_args context outsort in
441 if not b then (b, k - 1) else (b, k)
443 let (parameters, arguments,exp_named_subst) =
445 match xxx_type_of_aux' metasenv context term with
447 | Some t -> Some (beta_reduce t)
450 R.whd context (type_of_aux context term type_of_term)
452 (*CSC manca il caso dei CAST *)
453 C.MutInd (uri',i',exp_named_subst) ->
454 (* Checks suppressed *)
455 [],[],exp_named_subst
456 | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
458 split tl (List.length tl - k)
459 in params,args,exp_named_subst
461 raise (NotWellTyped "MutCase: the term is not an inductive one")
463 (* Checks suppressed *)
464 (* Let's visit all the subterms that will not be visited later *)
468 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
469 with Not_found -> assert false
472 C.InductiveDefinition (tl,_,parsno,_) ->
473 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
475 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
481 if parameters = [] then
482 (C.MutConstruct (uri,i,j,exp_named_subst))
484 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
487 match xxx_type_of_aux' metasenv context cons with
492 (type_of_branch context parsno need_dummy outtype
495 ignore (type_of_aux context p expectedtype);
497 ) 1 (List.combine pl cl)
499 if not need_dummy then
500 C.Appl ((outtype::arguments)@[term])
501 else if arguments = [] then
504 C.Appl (outtype::arguments)
506 (* Let's visit all the subterms that will not be visited later *)
511 let _ = type_of_aux context ty None in
512 (Some (C.Name n,(C.Decl ty)))
521 beta_reduce (CicSubstitution.lift (List.length fl) ty)
523 ignore (type_of_aux context' bo (Some expectedty))
526 (* Checks suppressed *)
527 let (_,_,ty,_) = List.nth fl i in
530 (* Let's visit all the subterms that will not be visited later *)
535 let _ = type_of_aux context ty None in
536 (Some (C.Name n,(C.Decl ty)))
545 beta_reduce (CicSubstitution.lift (List.length fl) ty)
547 ignore (type_of_aux context' bo (Some expectedty))
550 (* Checks suppressed *)
551 let (_,ty,_) = List.nth fl i in
554 let synthesized' = beta_reduce synthesized in
555 let synthesized' = !pack_coercion metasenv context synthesized' in
557 match expectedty with
559 (* No expected type *)
560 {synthesized = synthesized' ; expected = None}, synthesized
561 | Some ty when CicUtil.alpha_equivalence synthesized' ty ->
562 (* The expected type is synthactically equal to *)
563 (* the synthesized type. Let's forget it. *)
564 {synthesized = synthesized' ; expected = None}, synthesized
565 | Some expectedty' ->
566 {synthesized = synthesized' ; expected = Some expectedty'},
569 (* assert (not (cic_CicHash_mem subterms_to_types t));*)
570 cic_CicHash_add subterms_to_types t types ;
573 and visit_exp_named_subst context uri exp_named_subst =
577 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
578 with Not_found -> assert false
580 let params = CicUtil.params_of_obj obj in
585 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
586 with Not_found -> assert false
589 Cic.Variable (_,None,ty,_,_) -> uri,ty
590 | _ -> assert false (* the theorem is well-typed *)
593 let rec check uris_and_types subst =
594 match uris_and_types,subst with
596 | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
597 ignore (type_of_aux context t (Some ty)) ;
600 (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
603 | _,_ -> assert false (* the theorem is well-typed *)
605 check uris_and_types exp_named_subst
607 and sort_of_prod context (name,s) (t1, t2) =
608 let module C = Cic in
609 let t1' = CicReduction.whd context t1 in
610 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
611 match (t1', t2') with
612 | (C.Sort _, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> C.Sort s2
613 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->C.Sort(C.Type(CicUniv.fresh()))
614 | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1)
615 | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1)
616 | (C.Meta _, C.Sort _) -> t2'
617 | (C.Meta _, (C.Meta (_,_) as t))
618 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
623 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
625 and eat_prods context hetype =
626 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
630 | (hete, hety)::tl ->
631 (match (CicReduction.whd context hetype) with
633 (* Checks suppressed *)
634 eat_prods context (CicSubstitution.subst hete t) tl
635 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
638 and type_of_branch context argsno need_dummy outtype term constype =
639 let module C = Cic in
640 let module R = CicReduction in
641 match R.whd context constype with
646 C.Appl [outtype ; term]
647 | C.Appl (C.MutInd (_,_,_)::tl) ->
648 let (_,arguments) = split tl argsno
650 if need_dummy && arguments = [] then
653 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
654 | C.Prod (name,so,de) ->
656 match CicSubstitution.lift 1 term with
657 C.Appl l -> C.Appl (l@[C.Rel 1])
658 | t -> C.Appl [t ; C.Rel 1]
660 C.Prod (C.Anonymous,so,type_of_branch
661 ((Some (name,(C.Decl so)))::context) argsno need_dummy
662 (CicSubstitution.lift 1 outtype) term' de)
663 | _ -> raise (Impossible 20)
666 type_of_aux context t expectedty
669 let double_type_of metasenv context t expectedty =
670 let subterms_to_types = Cic.CicHash.create 503 in
671 ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;