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
43 | C.Var (uri,exp_named_subst) ->
44 let exp_named_subst' =
45 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
47 C.Var (uri,exp_named_subst)
51 (function None -> None | Some t -> Some (head_beta_reduce t)) l
54 | C.Implicit -> assert false
56 C.Cast (head_beta_reduce te, head_beta_reduce ty)
58 C.Prod (n, head_beta_reduce s, head_beta_reduce t)
60 C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
62 C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
63 | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
64 let he' = S.subst he t in
68 head_beta_reduce (C.Appl (he'::tl))
70 C.Appl (List.map head_beta_reduce l)
71 | C.Const (uri,exp_named_subst) ->
72 let exp_named_subst' =
73 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
75 C.Const (uri,exp_named_subst')
76 | C.MutInd (uri,i,exp_named_subst) ->
77 let exp_named_subst' =
78 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
80 C.MutInd (uri,i,exp_named_subst')
81 | C.MutConstruct (uri,i,j,exp_named_subst) ->
82 let exp_named_subst' =
83 List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
85 C.MutConstruct (uri,i,j,exp_named_subst')
86 | C.MutCase (sp,i,outt,t,pl) ->
87 C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t,
88 List.map head_beta_reduce pl)
92 (function (name,i,ty,bo) ->
93 name,i,head_beta_reduce ty,head_beta_reduce bo
100 (function (name,ty,bo) ->
101 name,head_beta_reduce ty,head_beta_reduce bo
107 (* syntactic_equality up to cookingsno for uris *)
108 (* (which is often syntactically irrilevant), *)
109 (* distinction between fake dependent products *)
110 (* and non-dependent products, alfa-conversion *)
111 (*CSC: must alfa-conversion be considered or not? *)
112 let syntactic_equality t t' =
113 let module C = Cic in
114 let rec syntactic_equality t t' =
118 C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
119 UriManager.eq uri uri' &&
120 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
121 | C.Cast (te,ty), C.Cast (te',ty') ->
122 syntactic_equality te te' &&
123 syntactic_equality ty ty'
124 | C.Prod (_,s,t), C.Prod (_,s',t') ->
125 syntactic_equality s s' &&
126 syntactic_equality t t'
127 | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
128 syntactic_equality s s' &&
129 syntactic_equality t t'
130 | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
131 syntactic_equality s s' &&
132 syntactic_equality t t'
133 | C.Appl l, C.Appl l' ->
134 List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
135 | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
136 UriManager.eq uri uri' &&
137 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
138 | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
139 UriManager.eq uri uri' && i = i' &&
140 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
141 | C.MutConstruct (uri,i,j,exp_named_subst),
142 C.MutConstruct (uri',i',j',exp_named_subst') ->
143 UriManager.eq uri uri' && i = i' && j = j' &&
144 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
145 | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
146 UriManager.eq sp sp' && i = i' &&
147 syntactic_equality outt outt' &&
148 syntactic_equality t t' &&
150 (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
151 | C.Fix (i,fl), C.Fix (i',fl') ->
154 (fun b (_,i,ty,bo) (_,i',ty',bo') ->
156 syntactic_equality ty ty' &&
157 syntactic_equality bo bo') true fl fl'
158 | C.CoFix (i,fl), C.CoFix (i',fl') ->
161 (fun b (_,ty,bo) (_,ty',bo') ->
163 syntactic_equality ty ty' &&
164 syntactic_equality bo bo') true fl fl'
165 | _, _ -> false (* we already know that t != t' *)
166 and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
168 (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
169 exp_named_subst1 exp_named_subst2
172 syntactic_equality t t'
180 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
181 | (_,_) -> raise ListTooShort
184 let type_of_constant uri =
185 let module C = Cic in
186 let module R = CicReduction in
187 let module U = UriManager in
189 match CicEnvironment.is_type_checked uri with
190 CicEnvironment.CheckedObj cobj -> cobj
191 | CicEnvironment.UncheckedObj uobj ->
192 raise (NotWellTyped "Reference to an unchecked constant")
195 C.Constant (_,_,ty,_) -> ty
196 | C.CurrentProof (_,_,_,ty,_) -> ty
197 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
200 let type_of_variable uri =
201 let module C = Cic in
202 let module R = CicReduction in
203 let module U = UriManager in
204 match CicEnvironment.is_type_checked uri with
205 CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
206 | CicEnvironment.UncheckedObj (C.Variable _) ->
207 raise (NotWellTyped "Reference to an unchecked variable")
208 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
211 let type_of_mutual_inductive_defs uri i =
212 let module C = Cic in
213 let module R = CicReduction in
214 let module U = UriManager in
216 match CicEnvironment.is_type_checked uri with
217 CicEnvironment.CheckedObj cobj -> cobj
218 | CicEnvironment.UncheckedObj uobj ->
219 raise (NotWellTyped "Reference to an unchecked inductive type")
222 C.InductiveDefinition (dl,_,_) ->
223 let (_,_,arity,_) = List.nth dl i in
225 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
228 let type_of_mutual_inductive_constr uri i j =
229 let module C = Cic in
230 let module R = CicReduction in
231 let module U = UriManager in
233 match CicEnvironment.is_type_checked uri with
234 CicEnvironment.CheckedObj cobj -> cobj
235 | CicEnvironment.UncheckedObj uobj ->
236 raise (NotWellTyped "Reference to an unchecked constructor")
239 C.InductiveDefinition (dl,_,_) ->
240 let (_,_,_,cl) = List.nth dl i in
241 let (_,ty) = List.nth cl (j-1) in
243 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
251 let hash = Hashtbl.hash
255 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
256 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
257 (* Coscoy's double type-inference algorithm *)
258 (* It computes the inner-types of every subterm of [t], *)
259 (* even when they are not needed to compute the types *)
260 (* of other terms. *)
261 let rec type_of_aux context t expectedty =
262 let module C = Cic in
263 let module R = CicReduction in
264 let module S = CicSubstitution in
265 let module U = UriManager in
270 match List.nth context (n - 1) with
271 Some (_,C.Decl t) -> S.lift n t
272 | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) expectedty
273 | None -> raise RelToHiddenHypothesis
275 _ -> raise (NotWellTyped "Not a close term")
277 | C.Var (uri,exp_named_subst) ->
278 visit_exp_named_subst context uri exp_named_subst ;
279 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
281 (* Let's visit all the subterms that will not be visited later *)
282 let (_,canonical_context,_) =
283 List.find (function (m,_,_) -> n = m) metasenv
285 let lifted_canonical_context =
289 | (Some (n,C.Decl t))::tl ->
290 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
291 | (Some (n,C.Def t))::tl ->
292 (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
293 | None::tl -> None::(aux (i+1) tl)
295 aux 1 canonical_context
302 | Some t,Some (_,C.Def ct) ->
305 (CicTypeChecker.type_of_aux' metasenv context ct)
307 (* Maybe I am a bit too paranoid, because *)
308 (* if the term is well-typed than t and ct *)
309 (* are convertible. Nevertheless, I compute *)
310 (* the expected type. *)
311 ignore (type_of_aux context t (Some expected_type))
312 | Some t,Some (_,C.Decl ct) ->
313 ignore (type_of_aux context t (Some ct))
314 | _,_ -> assert false (* the term is not well typed!!! *)
315 ) l lifted_canonical_context
317 let (_,canonical_context,ty) =
318 List.find (function (m,_,_) -> n = m) metasenv
320 (* Checks suppressed *)
321 CicSubstitution.lift_meta l ty
322 | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
323 | C.Implicit -> raise (Impossible 21)
325 (* Let's visit all the subterms that will not be visited later *)
326 let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
327 let _ = type_of_aux context ty None in
328 (* Checks suppressed *)
330 | C.Prod (name,s,t) ->
331 let sort1 = type_of_aux context s None
332 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
333 sort_of_prod context (name,s) (sort1,sort2)
334 | C.Lambda (n,s,t) ->
335 (* Let's visit all the subterms that will not be visited later *)
336 let _ = type_of_aux context s None in
337 let expected_target_type =
338 match expectedty with
340 | Some expectedty' ->
342 match R.whd context expectedty' with
343 C.Prod (_,_,expected_target_type) ->
344 head_beta_reduce expected_target_type
350 type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
352 (* Checks suppressed *)
355 (*CSC: What are the right expected types for the source and *)
356 (*CSC: target of a LetIn? None used. *)
357 (* Let's visit all the subterms that will not be visited later *)
358 let _ = type_of_aux context s None in
359 (* Checks suppressed *)
360 C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
361 | C.Appl (he::tl) when List.length tl > 0 ->
362 let expected_hetype =
363 (* Inefficient, the head is computed twice. But I know *)
364 (* of no other solution. *)
365 R.whd context (CicTypeChecker.type_of_aux' metasenv context he)
367 let hetype = type_of_aux context he (Some expected_hetype) in
368 let tlbody_and_type =
372 | C.Prod (n,s,t),he::tl ->
373 (he, type_of_aux context he (Some (head_beta_reduce s)))::
374 (aux (R.whd context (S.subst he t), tl))
377 aux (expected_hetype, tl)
379 eat_prods context hetype tlbody_and_type
380 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
381 | C.Const (uri,exp_named_subst) ->
382 visit_exp_named_subst context uri exp_named_subst ;
383 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
384 | C.MutInd (uri,i,exp_named_subst) ->
385 visit_exp_named_subst context uri exp_named_subst ;
386 CicSubstitution.subst_vars exp_named_subst
387 (type_of_mutual_inductive_defs uri i)
388 | C.MutConstruct (uri,i,j,exp_named_subst) ->
389 visit_exp_named_subst context uri exp_named_subst ;
390 CicSubstitution.subst_vars exp_named_subst
391 (type_of_mutual_inductive_constr uri i j)
392 | C.MutCase (uri,i,outtype,term,pl) ->
393 let outsort = type_of_aux context outtype None in
394 let (need_dummy, k) =
395 let rec guess_args context t =
396 match CicReduction.whd context t with
397 C.Sort _ -> (true, 0)
398 | C.Prod (name, s, t) ->
399 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
401 (* last prod before sort *)
402 match CicReduction.whd context s with
403 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
405 | C.Appl ((C.MutInd (uri',i',_)) :: _)
406 when U.eq uri' uri && i' = i -> (false, 1)
410 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
412 let (b, k) = guess_args context outsort in
413 if not b then (b, k - 1) else (b, k)
415 let (parameters, arguments,exp_named_subst) =
417 CicTypeChecker.type_of_aux' metasenv context term
420 R.whd context (type_of_aux context term
421 (Some (head_beta_reduce type_of_term)))
423 (*CSC manca il caso dei CAST *)
424 C.MutInd (uri',i',exp_named_subst) ->
425 (* Checks suppressed *)
426 [],[],exp_named_subst
427 | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
429 split tl (List.length tl - k)
430 in params,args,exp_named_subst
432 raise (NotWellTyped "MutCase: the term is not an inductive one")
434 (* Checks suppressed *)
435 (* Let's visit all the subterms that will not be visited later *)
437 match CicEnvironment.get_cooked_obj uri with
438 C.InductiveDefinition (tl,_,parsno) ->
439 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
441 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
447 if parameters = [] then
448 (C.MutConstruct (uri,i,j,exp_named_subst))
450 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
453 type_of_branch context parsno need_dummy outtype cons
454 (CicTypeChecker.type_of_aux' metasenv context cons)
456 ignore (type_of_aux context p
457 (Some (head_beta_reduce expectedtype))) ;
459 ) 1 (List.combine pl cl)
461 if not need_dummy then
462 C.Appl ((outtype::arguments)@[term])
463 else if arguments = [] then
466 C.Appl (outtype::arguments)
468 (* Let's visit all the subterms that will not be visited later *)
473 let _ = type_of_aux context ty None in
474 (Some (C.Name n,(C.Decl ty)))
483 head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
485 ignore (type_of_aux context' bo (Some expectedty))
488 (* Checks suppressed *)
489 let (_,_,ty,_) = List.nth fl i in
492 (* Let's visit all the subterms that will not be visited later *)
497 let _ = type_of_aux context ty None in
498 (Some (C.Name n,(C.Decl ty)))
507 head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
509 ignore (type_of_aux context' bo (Some expectedty))
512 (* Checks suppressed *)
513 let (_,ty,_) = List.nth fl i in
516 let synthesized' = head_beta_reduce synthesized in
518 match expectedty with
520 (* No expected type *)
521 {synthesized = synthesized' ; expected = None}, synthesized
522 | Some ty when syntactic_equality synthesized' ty ->
523 (* The expected type is synthactically equal to *)
524 (* the synthesized type. Let's forget it. *)
525 {synthesized = synthesized' ; expected = None}, synthesized
526 | Some expectedty' ->
527 {synthesized = synthesized' ; expected = Some expectedty'},
530 CicHash.add subterms_to_types t types ;
533 and visit_exp_named_subst context uri exp_named_subst =
535 match CicEnvironment.get_cooked_obj uri with
536 Cic.Constant (_,_,_,params)
537 | Cic.CurrentProof (_,_,_,_,params)
538 | Cic.Variable (_,_,_,params)
539 | Cic.InductiveDefinition (_,params,_) ->
542 match CicEnvironment.get_cooked_obj uri with
543 Cic.Variable (_,None,ty,_) -> uri,ty
544 | _ -> assert false (* the theorem is well-typed *)
547 let rec check uris_and_types subst =
548 match uris_and_types,subst with
550 | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
551 ignore (type_of_aux context t (Some ty)) ;
554 (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
557 | _,_ -> assert false (* the theorem is well-typed *)
559 check uris_and_types exp_named_subst
561 and sort_of_prod context (name,s) (t1, t2) =
562 let module C = Cic in
563 let t1' = CicReduction.whd context t1 in
564 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
565 match (t1', t2') with
566 (C.Sort s1, C.Sort s2)
567 when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
569 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
573 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
575 and eat_prods context hetype =
576 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
580 | (hete, hety)::tl ->
581 (match (CicReduction.whd context hetype) with
583 (* Checks suppressed *)
584 eat_prods context (CicSubstitution.subst hete t) tl
585 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
588 and type_of_branch context argsno need_dummy outtype term constype =
589 let module C = Cic in
590 let module R = CicReduction in
591 match R.whd context constype with
596 C.Appl [outtype ; term]
597 | C.Appl (C.MutInd (_,_,_)::tl) ->
598 let (_,arguments) = split tl argsno
600 if need_dummy && arguments = [] then
603 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
604 | C.Prod (name,so,de) ->
606 match CicSubstitution.lift 1 term with
607 C.Appl l -> C.Appl (l@[C.Rel 1])
608 | t -> C.Appl [t ; C.Rel 1]
610 C.Prod (C.Anonymous,so,type_of_branch
611 ((Some (name,(C.Decl so)))::context) argsno need_dummy
612 (CicSubstitution.lift 1 outtype) term' de)
613 | _ -> raise (Impossible 20)
616 type_of_aux context t expectedty
619 let double_type_of metasenv context t expectedty =
620 let subterms_to_types = CicHash.create 503 in
621 ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;