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 (*CSC: potrebbe creare applicazioni di applicazioni *)
37 (*CSC: ora non e' piu' head, ma completa!!! *)
38 let rec head_beta_reduce =
39 let module S = CicSubstitution in
47 (function None -> None | Some t -> Some (head_beta_reduce t)) l
50 | C.Implicit -> assert false
52 C.Cast (head_beta_reduce te, head_beta_reduce ty)
54 C.Prod (n, head_beta_reduce s, head_beta_reduce t)
56 C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
58 C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
59 | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
60 let he' = S.subst he t in
64 head_beta_reduce (C.Appl (he'::tl))
66 C.Appl (List.map head_beta_reduce l)
69 | C.MutConstruct _ as t -> t
70 | C.MutCase (sp,cno,i,outt,t,pl) ->
71 C.MutCase (sp,cno,i,head_beta_reduce outt,head_beta_reduce t,
72 List.map head_beta_reduce pl)
76 (function (name,i,ty,bo) ->
77 name,i,head_beta_reduce ty,head_beta_reduce bo
84 (function (name,ty,bo) ->
85 name,head_beta_reduce ty,head_beta_reduce bo
91 (* syntactic_equality up to cookingsno for uris *)
92 (* (which is often syntactically irrilevant), *)
93 (* distinction between fake dependent products *)
94 (* and non-dependent products, alfa-conversion *)
95 (*CSC: must alfa-conversion be considered or not? *)
96 let syntactic_equality t t' =
98 let rec syntactic_equality t t' =
106 | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
107 | C.Cast (te,ty), C.Cast (te',ty') ->
108 syntactic_equality te te' &&
109 syntactic_equality ty ty'
110 | C.Prod (_,s,t), C.Prod (_,s',t') ->
111 syntactic_equality s s' &&
112 syntactic_equality t t'
113 | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
114 syntactic_equality s s' &&
115 syntactic_equality t t'
116 | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
117 syntactic_equality s s' &&
118 syntactic_equality t t'
119 | C.Appl l, C.Appl l' ->
120 List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
121 | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
122 | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
123 UriManager.eq uri uri' && i = i'
124 | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
125 UriManager.eq uri uri' && i = i' && j = j'
126 | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
127 UriManager.eq sp sp' && i = i' &&
128 syntactic_equality outt outt' &&
129 syntactic_equality t t' &&
131 (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
132 | C.Fix (i,fl), C.Fix (i',fl') ->
135 (fun b (_,i,ty,bo) (_,i',ty',bo') ->
137 syntactic_equality ty ty' &&
138 syntactic_equality bo bo') true fl fl'
139 | C.CoFix (i,fl), C.CoFix (i',fl') ->
142 (fun b (_,ty,bo) (_,ty',bo') ->
144 syntactic_equality ty ty' &&
145 syntactic_equality bo bo') true fl fl'
149 syntactic_equality t t'
157 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
158 | (_,_) -> raise ListTooShort
161 let cooked_type_of_constant uri cookingsno =
162 let module C = Cic in
163 let module R = CicReduction in
164 let module U = UriManager in
166 match CicEnvironment.is_type_checked uri cookingsno with
167 CicEnvironment.CheckedObj cobj -> cobj
168 | CicEnvironment.UncheckedObj uobj ->
169 raise (NotWellTyped "Reference to an unchecked constant")
172 C.Definition (_,_,ty,_) -> ty
173 | C.Axiom (_,ty,_) -> ty
174 | C.CurrentProof (_,_,_,ty) -> ty
175 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
178 let type_of_variable uri =
179 let module C = Cic in
180 let module R = CicReduction in
181 let module U = UriManager in
182 (* 0 because a variable is never cooked => no partial cooking at one level *)
183 match CicEnvironment.is_type_checked uri 0 with
184 CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
185 | CicEnvironment.UncheckedObj (C.Variable _) ->
186 raise (NotWellTyped "Reference to an unchecked variable")
187 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
190 let cooked_type_of_mutual_inductive_defs uri cookingsno i =
191 let module C = Cic in
192 let module R = CicReduction in
193 let module U = UriManager in
195 match CicEnvironment.is_type_checked uri cookingsno with
196 CicEnvironment.CheckedObj cobj -> cobj
197 | CicEnvironment.UncheckedObj uobj ->
198 raise (NotWellTyped "Reference to an unchecked inductive type")
201 C.InductiveDefinition (dl,_,_) ->
202 let (_,_,arity,_) = List.nth dl i in
204 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
207 let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
208 let module C = Cic in
209 let module R = CicReduction in
210 let module U = UriManager in
212 match CicEnvironment.is_type_checked uri cookingsno with
213 CicEnvironment.CheckedObj cobj -> cobj
214 | CicEnvironment.UncheckedObj uobj ->
215 raise (NotWellTyped "Reference to an unchecked constructor")
218 C.InductiveDefinition (dl,_,_) ->
219 let (_,_,_,cl) = List.nth dl i in
220 let (_,ty,_) = List.nth cl (j-1) in
222 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
230 let hash = Hashtbl.hash
234 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
235 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
236 (* Coscoy's double type-inference algorithm *)
237 (* It computes the inner-types of every subterm of [t], *)
238 (* even when they are not needed to compute the types *)
239 (* of other terms. *)
240 let rec type_of_aux context t expectedty =
241 let module C = Cic in
242 let module R = CicReduction in
243 let module S = CicSubstitution in
244 let module U = UriManager in
249 match List.nth context (n - 1) with
250 Some (_,C.Decl t) -> S.lift n t
251 | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) expectedty
252 | None -> raise RelToHiddenHypothesis
254 _ -> raise (NotWellTyped "Not a close term")
256 | C.Var uri -> type_of_variable uri
258 (* Let's visit all the subterms that will not be visited later *)
259 let (_,canonical_context,_) =
260 List.find (function (m,_,_) -> n = m) metasenv
262 let lifted_canonical_context =
266 | (Some (n,C.Decl t))::tl ->
267 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
268 | (Some (n,C.Def t))::tl ->
269 (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
270 | None::tl -> None::(aux (i+1) tl)
272 aux 1 canonical_context
279 | Some t,Some (_,C.Def ct) ->
282 (CicTypeChecker.type_of_aux' metasenv context ct)
284 (* Maybe I am a bit too paranoid, because *)
285 (* if the term is well-typed than t and ct *)
286 (* are convertible. Nevertheless, I compute *)
287 (* the expected type. *)
288 ignore (type_of_aux context t (Some expected_type))
289 | Some t,Some (_,C.Decl ct) ->
290 ignore (type_of_aux context t (Some ct))
291 | _,_ -> assert false (* the term is not well typed!!! *)
292 ) l lifted_canonical_context
294 let (_,canonical_context,ty) =
295 List.find (function (m,_,_) -> n = m) metasenv
297 (* Checks suppressed *)
298 CicSubstitution.lift_meta l ty
299 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
300 | C.Implicit -> raise (Impossible 21)
302 (* Let's visit all the subterms that will not be visited later *)
303 let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
304 let _ = type_of_aux context ty None in
305 (* Checks suppressed *)
307 | C.Prod (name,s,t) ->
308 let sort1 = type_of_aux context s None
309 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
310 sort_of_prod context (name,s) (sort1,sort2)
311 | C.Lambda (n,s,t) ->
312 (* Let's visit all the subterms that will not be visited later *)
313 let _ = type_of_aux context s None in
314 let expected_target_type =
315 match expectedty with
317 | Some expectedty' ->
319 match R.whd context expectedty' with
320 C.Prod (_,_,expected_target_type) ->
321 head_beta_reduce expected_target_type
327 type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
329 (* Checks suppressed *)
332 (*CSC: What are the right expected types for the source and *)
333 (*CSC: target of a LetIn? None used. *)
334 (* Let's visit all the subterms that will not be visited later *)
335 let _ = type_of_aux context s None in
336 (* Checks suppressed *)
337 C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
338 | C.Appl (he::tl) when List.length tl > 0 ->
339 let expected_hetype =
340 (* Inefficient, the head is computed twice. But I know *)
341 (* of no other solution. *)
342 R.whd context (CicTypeChecker.type_of_aux' metasenv context he)
344 let hetype = type_of_aux context he (Some expected_hetype) in
345 let tlbody_and_type =
349 | C.Prod (n,s,t),he::tl ->
350 (he, type_of_aux context he (Some (head_beta_reduce s)))::
351 (aux (R.whd context (S.subst he t), tl))
354 aux (expected_hetype, tl)
356 eat_prods context hetype tlbody_and_type
357 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
358 | C.Const (uri,cookingsno) ->
359 cooked_type_of_constant uri cookingsno
360 | C.MutInd (uri,cookingsno,i) ->
361 cooked_type_of_mutual_inductive_defs uri cookingsno i
362 | C.MutConstruct (uri,cookingsno,i,j) ->
363 let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in
365 | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
366 let outsort = type_of_aux context outtype None in
367 let (need_dummy, k) =
368 let rec guess_args context t =
369 match CicReduction.whd context t with
370 C.Sort _ -> (true, 0)
371 | C.Prod (name, s, t) ->
372 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
374 (* last prod before sort *)
375 match CicReduction.whd context s with
376 (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
377 C.MutInd (uri',_,i') when U.eq uri' uri && i' = i ->
379 | C.Appl ((C.MutInd (uri',_,i')) :: _)
380 when U.eq uri' uri && i' = i -> (false, 1)
384 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
386 let (b, k) = guess_args context outsort in
387 if not b then (b, k - 1) else (b, k)
389 let (parameters, arguments) =
391 CicTypeChecker.type_of_aux' metasenv context term
394 R.whd context (type_of_aux context term
395 (Some (head_beta_reduce type_of_term)))
397 (*CSC manca il caso dei CAST *)
398 C.MutInd (uri',_,i') ->
399 (* Checks suppressed *)
401 | C.Appl (C.MutInd (uri',_,i') :: tl) ->
402 split tl (List.length tl - k)
404 raise (NotWellTyped "MutCase: the term is not an inductive one")
406 (* Checks suppressed *)
407 (* Let's visit all the subterms that will not be visited later *)
409 match CicEnvironment.get_cooked_obj uri cookingsno with
410 C.InductiveDefinition (tl,_,parsno) ->
411 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
413 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
417 (fun j (p,(_,c,_)) ->
419 if parameters = [] then
420 (C.MutConstruct (uri,cookingsno,i,j))
422 (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
425 type_of_branch context parsno need_dummy outtype cons
426 (CicTypeChecker.type_of_aux' metasenv context cons)
428 ignore (type_of_aux context p
429 (Some (head_beta_reduce expectedtype))) ;
431 ) 1 (List.combine pl cl)
433 if not need_dummy then
434 C.Appl ((outtype::arguments)@[term])
435 else if arguments = [] then
438 C.Appl (outtype::arguments)
440 (* Let's visit all the subterms that will not be visited later *)
445 let _ = type_of_aux context ty None in
446 (Some (C.Name n,(C.Decl ty)))
455 head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
457 ignore (type_of_aux context' bo (Some expectedty))
460 (* Checks suppressed *)
461 let (_,_,ty,_) = List.nth fl i in
464 (* Let's visit all the subterms that will not be visited later *)
469 let _ = type_of_aux context ty None in
470 (Some (C.Name n,(C.Decl ty)))
479 head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
481 ignore (type_of_aux context' bo (Some expectedty))
484 (* Checks suppressed *)
485 let (_,ty,_) = List.nth fl i in
488 let synthesized' = head_beta_reduce synthesized in
490 match expectedty with
492 (* No expected type *)
493 {synthesized = synthesized' ; expected = None}, synthesized
494 | Some ty when syntactic_equality synthesized' ty ->
495 (* The expected type is synthactically equal to *)
496 (* the synthesized type. Let's forget it. *)
497 {synthesized = synthesized' ; expected = None}, synthesized
498 | Some expectedty' ->
499 {synthesized = synthesized' ; expected = Some expectedty'},
502 CicHash.add subterms_to_types t types ;
505 and sort_of_prod context (name,s) (t1, t2) =
506 let module C = Cic in
507 let t1' = CicReduction.whd context t1 in
508 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
509 match (t1', t2') with
510 (C.Sort s1, C.Sort s2)
511 when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
513 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
517 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
519 and eat_prods context hetype =
520 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
524 | (hete, hety)::tl ->
525 (match (CicReduction.whd context hetype) with
527 (* Checks suppressed *)
528 eat_prods context (CicSubstitution.subst hete t) tl
529 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
532 and type_of_branch context argsno need_dummy outtype term constype =
533 let module C = Cic in
534 let module R = CicReduction in
535 match R.whd context constype with
540 C.Appl [outtype ; term]
541 | C.Appl (C.MutInd (_,_,_)::tl) ->
542 let (_,arguments) = split tl argsno
544 if need_dummy && arguments = [] then
547 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
548 | C.Prod (name,so,de) ->
550 match CicSubstitution.lift 1 term with
551 C.Appl l -> C.Appl (l@[C.Rel 1])
552 | t -> C.Appl [t ; C.Rel 1]
554 C.Prod (C.Anonimous,so,type_of_branch
555 ((Some (name,(C.Decl so)))::context) argsno need_dummy
556 (CicSubstitution.lift 1 outtype) term' de)
557 | _ -> raise (Impossible 20)
560 type_of_aux context t expectedty
563 let double_type_of metasenv context t expectedty =
564 let subterms_to_types = CicHash.create 503 in
565 ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;