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 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 *)
359 | C.LetIn (n,s,ty,t) ->
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 _ = type_of_aux context ty None in
364 let _ = type_of_aux context s (Some ty) in
366 (* Checks suppressed *)
367 type_of_aux ((Some (n,(C.Def (s,ty))))::context) t None
368 in (* CicSubstitution.subst s t_typ *)
369 if does_not_occur 1 t_typ then
370 (* since [Rel 1] does not occur in typ, substituting any term *)
371 (* in place of [Rel 1] is equivalent to delifting once *)
372 CicSubstitution.subst (C.Implicit None) t_typ
374 C.LetIn (n,s,ty,t_typ)
375 | C.Appl (he::tl) when List.length tl > 0 ->
377 let expected_hetype =
378 (* Inefficient, the head is computed twice. But I know *)
379 (* of no other solution. *)
381 (R.whd context (xxx_type_of_aux' metasenv context he)))
383 let hetype = type_of_aux context he (Some expected_hetype) in
384 let tlbody_and_type =
388 | C.Prod (n,s,t),he::tl ->
389 (he, type_of_aux context he (Some (beta_reduce s)))::
390 (aux (R.whd context (S.subst he t), tl))
393 aux (expected_hetype, tl) *)
394 let hetype = R.whd context (type_of_aux context he None) in
395 let tlbody_and_type =
399 | C.Prod (n,s,t),he::tl ->
400 (he, type_of_aux context he (Some (beta_reduce s)))::
401 (aux (R.whd context (S.subst he t), tl))
406 eat_prods context hetype tlbody_and_type
407 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
408 | C.Const (uri,exp_named_subst) ->
409 visit_exp_named_subst context uri exp_named_subst ;
410 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
411 | C.MutInd (uri,i,exp_named_subst) ->
412 visit_exp_named_subst context uri exp_named_subst ;
413 CicSubstitution.subst_vars exp_named_subst
414 (type_of_mutual_inductive_defs uri i)
415 | C.MutConstruct (uri,i,j,exp_named_subst) ->
416 visit_exp_named_subst context uri exp_named_subst ;
417 CicSubstitution.subst_vars exp_named_subst
418 (type_of_mutual_inductive_constr uri i j)
419 | C.MutCase (uri,i,outtype,term,pl) ->
420 let outsort = type_of_aux context outtype None in
421 let (need_dummy, k) =
422 let rec guess_args context t =
423 match CicReduction.whd context t with
424 C.Sort _ -> (true, 0)
425 | C.Prod (name, s, t) ->
426 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
428 (* last prod before sort *)
429 match CicReduction.whd context s with
430 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
432 | C.Appl ((C.MutInd (uri',i',_)) :: _)
433 when U.eq uri' uri && i' = i -> (false, 1)
437 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
439 let (b, k) = guess_args context outsort in
440 if not b then (b, k - 1) else (b, k)
442 let (parameters, arguments,exp_named_subst) =
444 match xxx_type_of_aux' metasenv context term with
446 | Some t -> Some (beta_reduce t)
449 R.whd context (type_of_aux context term type_of_term)
451 (*CSC manca il caso dei CAST *)
452 C.MutInd (uri',i',exp_named_subst) ->
453 (* Checks suppressed *)
454 [],[],exp_named_subst
455 | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
457 split tl (List.length tl - k)
458 in params,args,exp_named_subst
460 raise (NotWellTyped "MutCase: the term is not an inductive one")
462 (* Checks suppressed *)
463 (* Let's visit all the subterms that will not be visited later *)
467 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
468 with Not_found -> assert false
471 C.InductiveDefinition (tl,_,parsno,_) ->
472 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
474 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
480 if parameters = [] then
481 (C.MutConstruct (uri,i,j,exp_named_subst))
483 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
486 match xxx_type_of_aux' metasenv context cons with
491 (type_of_branch context parsno need_dummy outtype
494 ignore (type_of_aux context p expectedtype);
496 ) 1 (List.combine pl cl)
498 if not need_dummy then
499 C.Appl ((outtype::arguments)@[term])
500 else if arguments = [] then
503 C.Appl (outtype::arguments)
505 (* Let's visit all the subterms that will not be visited later *)
510 let _ = type_of_aux context ty None in
511 (Some (C.Name n,(C.Decl ty)))
520 beta_reduce (CicSubstitution.lift (List.length fl) ty)
522 ignore (type_of_aux context' bo (Some expectedty))
525 (* Checks suppressed *)
526 let (_,_,ty,_) = List.nth fl i in
529 (* Let's visit all the subterms that will not be visited later *)
534 let _ = type_of_aux context ty None in
535 (Some (C.Name n,(C.Decl ty)))
544 beta_reduce (CicSubstitution.lift (List.length fl) ty)
546 ignore (type_of_aux context' bo (Some expectedty))
549 (* Checks suppressed *)
550 let (_,ty,_) = List.nth fl i in
553 let synthesized' = beta_reduce synthesized in
554 let synthesized' = !pack_coercion metasenv context synthesized' in
556 match expectedty with
558 (* No expected type *)
559 {synthesized = synthesized' ; expected = None}, synthesized
560 | Some ty when CicUtil.alpha_equivalence synthesized' ty ->
561 (* The expected type is synthactically equal to *)
562 (* the synthesized type. Let's forget it. *)
563 {synthesized = synthesized' ; expected = None}, synthesized
564 | Some expectedty' ->
565 {synthesized = synthesized' ; expected = Some expectedty'},
568 (* assert (not (cic_CicHash_mem subterms_to_types t));*)
569 cic_CicHash_add subterms_to_types t types ;
572 and visit_exp_named_subst context uri exp_named_subst =
576 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
577 with Not_found -> assert false
579 let params = CicUtil.params_of_obj obj in
584 CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
585 with Not_found -> assert false
588 Cic.Variable (_,None,ty,_,_) -> uri,ty
589 | _ -> assert false (* the theorem is well-typed *)
592 let rec check uris_and_types subst =
593 match uris_and_types,subst with
595 | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
596 ignore (type_of_aux context t (Some ty)) ;
599 (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
602 | _,_ -> assert false (* the theorem is well-typed *)
604 check uris_and_types exp_named_subst
606 and sort_of_prod context (name,s) (t1, t2) =
607 let module C = Cic in
608 let t1' = CicReduction.whd context t1 in
609 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
610 match (t1', t2') with
611 (C.Sort _, C.Sort s2)
612 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
613 (* different from Coq manual!!! *)
615 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
616 C.Sort (C.Type (CicUniv.fresh()))
617 | (C.Sort _,C.Sort (C.Type t1)) ->
618 (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
619 C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
620 | (C.Meta _, C.Sort _) -> t2'
621 | (C.Meta _, (C.Meta (_,_) as t))
622 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
627 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
629 and eat_prods context hetype =
630 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
634 | (hete, hety)::tl ->
635 (match (CicReduction.whd context hetype) with
637 (* Checks suppressed *)
638 eat_prods context (CicSubstitution.subst hete t) tl
639 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
642 and type_of_branch context argsno need_dummy outtype term constype =
643 let module C = Cic in
644 let module R = CicReduction in
645 match R.whd context constype with
650 C.Appl [outtype ; term]
651 | C.Appl (C.MutInd (_,_,_)::tl) ->
652 let (_,arguments) = split tl argsno
654 if need_dummy && arguments = [] then
657 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
658 | C.Prod (name,so,de) ->
660 match CicSubstitution.lift 1 term with
661 C.Appl l -> C.Appl (l@[C.Rel 1])
662 | t -> C.Appl [t ; C.Rel 1]
664 C.Prod (C.Anonymous,so,type_of_branch
665 ((Some (name,(C.Decl so)))::context) argsno need_dummy
666 (CicSubstitution.lift 1 outtype) term' de)
667 | _ -> raise (Impossible 20)
670 type_of_aux context t expectedty
673 let double_type_of metasenv context t expectedty =
674 let subterms_to_types = Cic.CicHash.create 503 in
675 ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;