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 RefineFailure of string;;
29 exception Uncertain of string;;
30 exception AssertFailure of string;;
32 let debug_print = fun _ -> ()
34 let fo_unif_subst subst context metasenv t1 t2 ugraph =
36 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
38 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
39 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
45 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
46 | (_,_) -> raise (AssertFailure "split: list too short")
49 let rec type_of_constant uri ugraph =
51 let module R = CicReduction in
52 let module U = UriManager in
53 let _ = CicTypeChecker.typecheck uri in
56 CicEnvironment.get_cooked_obj ugraph uri
57 with Not_found -> assert false
60 C.Constant (_,_,ty,_,_) -> ty,u
61 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
64 (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
66 and type_of_variable uri ugraph =
68 let module R = CicReduction in
69 let module U = UriManager in
70 let _ = CicTypeChecker.typecheck uri in
73 CicEnvironment.get_cooked_obj ugraph uri
74 with Not_found -> assert false
77 C.Variable (_,_,ty,_,_) -> ty,u
81 ("Unknown variable definition " ^ UriManager.string_of_uri uri))
83 and type_of_mutual_inductive_defs uri i ugraph =
85 let module R = CicReduction in
86 let module U = UriManager in
87 let _ = CicTypeChecker.typecheck uri in
90 CicEnvironment.get_cooked_obj ugraph uri
91 with Not_found -> assert false
94 C.InductiveDefinition (dl,_,_,_) ->
95 let (_,_,arity,_) = List.nth dl i in
100 ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
102 and type_of_mutual_inductive_constr uri i j ugraph =
103 let module C = Cic in
104 let module R = CicReduction in
105 let module U = UriManager in
106 let _ = CicTypeChecker.typecheck uri in
109 CicEnvironment.get_cooked_obj ugraph uri
110 with Not_found -> assert false
113 C.InductiveDefinition (dl,_,_,_) ->
114 let (_,_,_,cl) = List.nth dl i in
115 let (_,ty) = List.nth cl (j-1) in
120 ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
123 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
125 (* the check_branch function checks if a branch of a case is refinable.
126 It returns a pair (outype_instance,args), a subst and a metasenv.
127 outype_instance is the expected result of applying the case outtype
129 The problem is that outype is in general unknown, and we should
130 try to synthesize it from the above information, that is in general
131 a second order unification problem. *)
133 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
134 let module C = Cic in
135 (* let module R = CicMetaSubst in *)
136 let module R = CicReduction in
137 match R.whd ~subst context expectedtype with
139 (n,context,actualtype, [term]), subst, metasenv, ugraph
140 | C.Appl (C.MutInd (_,_,_)::tl) ->
141 let (_,arguments) = split tl left_args_no in
142 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
143 | C.Prod (name,so,de) ->
144 (* we expect that the actual type of the branch has the due
146 (match R.whd ~subst context actualtype with
147 C.Prod (name',so',de') ->
148 let subst, metasenv, ugraph1 =
149 fo_unif_subst subst context metasenv so so' ugraph in
151 (match CicSubstitution.lift 1 term with
152 C.Appl l -> C.Appl (l@[C.Rel 1])
153 | t -> C.Appl [t ; C.Rel 1]) in
154 (* we should also check that the name variable is anonymous in
155 the actual type de' ?? *)
157 ((Some (name,(C.Decl so)))::context)
158 metasenv subst left_args_no de' term' de ugraph1
159 | _ -> raise (AssertFailure "Wrong number of arguments"))
160 | _ -> raise (AssertFailure "Prod or MutInd expected")
162 and type_of_aux' metasenv context t ugraph =
163 let rec type_of_aux subst metasenv context t ugraph =
164 let module C = Cic in
165 let module S = CicSubstitution in
166 let module U = UriManager in
171 match List.nth context (n - 1) with
172 Some (_,C.Decl ty) ->
173 t,S.lift n ty,subst,metasenv, ugraph
174 | Some (_,C.Def (_,Some ty)) ->
175 t,S.lift n ty,subst,metasenv, ugraph
176 | Some (_,C.Def (bo,None)) ->
178 (* if it is in the context it must be already well-typed*)
179 CicTypeChecker.type_of_aux' ~subst metasenv context
182 t,ty,subst,metasenv,ugraph
183 | None -> raise (RefineFailure "Rel to hidden hypothesis")
185 _ -> raise (RefineFailure "Not a close term")
187 | C.Var (uri,exp_named_subst) ->
188 let exp_named_subst',subst',metasenv',ugraph1 =
189 check_exp_named_subst
190 subst metasenv context exp_named_subst ugraph
192 let ty_uri,ugraph1 = type_of_variable uri ugraph in
194 CicSubstitution.subst_vars exp_named_subst' ty_uri
196 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
199 let (canonical_context, term,ty) =
200 CicUtil.lookup_subst n subst
202 let l',subst',metasenv',ugraph1 =
203 check_metasenv_consistency n subst metasenv context
204 canonical_context l ugraph
206 (* trust or check ??? *)
207 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
208 subst', metasenv', ugraph1
209 (* type_of_aux subst metasenv
210 context (CicSubstitution.subst_meta l term) *)
211 with CicUtil.Subst_not_found _ ->
212 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
213 let l',subst',metasenv', ugraph1 =
214 check_metasenv_consistency n subst metasenv context
215 canonical_context l ugraph
217 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
218 subst', metasenv',ugraph1)
219 | C.Sort (C.Type tno) ->
220 let tno' = CicUniv.fresh() in
221 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
222 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
224 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
225 | C.Implicit _ -> raise (AssertFailure "21")
227 let ty',_,subst',metasenv',ugraph1 =
228 type_of_aux subst metasenv context ty ugraph
230 let te',inferredty,subst'',metasenv'',ugraph2 =
231 type_of_aux subst' metasenv' context te ugraph1
234 let subst''',metasenv''',ugraph3 =
235 fo_unif_subst subst'' context metasenv''
236 inferredty ty ugraph2
238 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
240 _ -> raise (RefineFailure "Cast"))
241 | C.Prod (name,s,t) ->
242 let s',sort1,subst',metasenv',ugraph1 =
243 type_of_aux subst metasenv context s ugraph
245 let t',sort2,subst'',metasenv'',ugraph2 =
246 type_of_aux subst' metasenv'
247 ((Some (name,(C.Decl s')))::context) t ugraph1
249 let sop,subst''',metasenv''',ugraph3 =
250 sort_of_prod subst'' metasenv''
251 context (name,s') (sort1,sort2) ugraph2
253 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
254 | C.Lambda (n,s,t) ->
255 let s',sort1,subst',metasenv',ugraph1 =
256 type_of_aux subst metasenv context s ugraph
258 (match CicReduction.whd ~subst:subst' context sort1 with
262 raise (RefineFailure (sprintf
263 "Not well-typed lambda-abstraction: the source %s should be a type;
264 instead it is a term of type %s" (CicPp.ppterm s)
265 (CicPp.ppterm sort1)))
267 let t',type2,subst'',metasenv'',ugraph2 =
268 type_of_aux subst' metasenv'
269 ((Some (n,(C.Decl s')))::context) t ugraph1
271 C.Lambda (n,s',t'),C.Prod (n,s',type2),
272 subst'',metasenv'',ugraph2
274 (* only to check if s is well-typed *)
275 let s',ty,subst',metasenv',ugraph1 =
276 type_of_aux subst metasenv context s ugraph
278 let t',inferredty,subst'',metasenv'',ugraph2 =
279 type_of_aux subst' metasenv'
280 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
282 (* One-step LetIn reduction.
283 * Even faster than the previous solution.
284 * Moreover the inferred type is closer to the expected one.
286 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
287 subst'',metasenv'',ugraph2
288 | C.Appl (he::((_::_) as tl)) ->
289 let he',hetype,subst',metasenv',ugraph1 =
290 type_of_aux subst metasenv context he ugraph
292 let tlbody_and_type,subst'',metasenv'',ugraph2 =
294 (fun x (res,subst,metasenv,ugraph) ->
295 let x',ty,subst',metasenv',ugraph1 =
296 type_of_aux subst metasenv context x ugraph
298 (x', ty)::res,subst',metasenv',ugraph1
299 ) tl ([],subst',metasenv',ugraph1)
301 let tl',applty,subst''',metasenv''',ugraph3 =
302 eat_prods subst'' metasenv'' context
303 hetype tlbody_and_type ugraph2
305 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
306 | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
307 | C.Const (uri,exp_named_subst) ->
308 let exp_named_subst',subst',metasenv',ugraph1 =
309 check_exp_named_subst subst metasenv context
310 exp_named_subst ugraph in
311 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
313 CicSubstitution.subst_vars exp_named_subst' ty_uri
315 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
316 | C.MutInd (uri,i,exp_named_subst) ->
317 let exp_named_subst',subst',metasenv',ugraph1 =
318 check_exp_named_subst subst metasenv context
319 exp_named_subst ugraph
321 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
323 CicSubstitution.subst_vars exp_named_subst' ty_uri in
324 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
325 | C.MutConstruct (uri,i,j,exp_named_subst) ->
326 let exp_named_subst',subst',metasenv',ugraph1 =
327 check_exp_named_subst subst metasenv context
328 exp_named_subst ugraph
331 type_of_mutual_inductive_constr uri i j ugraph1
334 CicSubstitution.subst_vars exp_named_subst' ty_uri
336 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
338 | C.MutCase (uri, i, outtype, term, pl) ->
339 (* first, get the inductive type (and noparams)
340 * in the environment *)
341 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
342 let _ = CicTypeChecker.typecheck uri in
343 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
345 C.InductiveDefinition (l,expl_params,parsno,_) ->
346 List.nth l i , expl_params, parsno, u
350 ("Unkown mutual inductive definition " ^
351 U.string_of_uri uri))
353 let rec count_prod t =
354 match CicReduction.whd ~subst context t with
355 C.Prod (_, _, t) -> 1 + (count_prod t)
358 let no_args = count_prod arity in
359 (* now, create a "generic" MutInd *)
360 let metasenv,left_args =
361 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
363 let metasenv,right_args =
364 let no_right_params = no_args - no_left_params in
365 if no_right_params < 0 then assert false
366 else CicMkImplicit.n_fresh_metas
367 metasenv subst context no_right_params
369 let metasenv,exp_named_subst =
370 CicMkImplicit.fresh_subst metasenv subst context expl_params in
373 C.MutInd (uri,i,exp_named_subst)
376 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
378 (* check consistency with the actual type of term *)
379 let term',actual_type,subst,metasenv,ugraph1 =
380 type_of_aux subst metasenv context term ugraph in
381 let expected_type',_, subst, metasenv,ugraph2 =
382 type_of_aux subst metasenv context expected_type ugraph1
384 let actual_type = CicReduction.whd ~subst context actual_type in
385 let subst,metasenv,ugraph3 =
386 fo_unif_subst subst context metasenv
387 expected_type' actual_type ugraph2
389 let rec instantiate_prod t =
393 match CicReduction.whd ~subst context t with
395 instantiate_prod (CicSubstitution.subst he t') tl
398 let arity_instantiated_with_left_args =
399 instantiate_prod arity left_args in
400 (* TODO: check if the sort elimination
401 * is allowed: [(I q1 ... qr)|B] *)
402 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
404 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
406 if left_args = [] then
407 (C.MutConstruct (uri,i,j,exp_named_subst))
410 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
412 let p',actual_type,subst,metasenv,ugraph1 =
413 type_of_aux subst metasenv context p ugraph
415 let constructor',expected_type, subst, metasenv,ugraph2 =
416 type_of_aux subst metasenv context constructor ugraph1
418 let outtypeinstance,subst,metasenv,ugraph3 =
419 check_branch 0 context metasenv subst no_left_params
420 actual_type constructor' expected_type ugraph2
423 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
424 ([],1,[],subst,metasenv,ugraph3) pl
427 (* we are left to check that the outype matches his instances.
428 The easy case is when the outype is specified, that amount
429 to a trivial check. Otherwise, we should guess a type from
435 (let candidate,ugraph5,metasenv,subst =
436 let exp_name_subst, metasenv =
438 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
440 let uris = CicUtil.params_of_obj o in
442 fun uri (acc,metasenv) ->
443 let metasenv',new_meta =
444 CicMkImplicit.mk_implicit metasenv subst context
447 CicMkImplicit.identity_relocation_list_for_metavariable
450 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
454 match left_args,right_args with
455 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
457 let rec mk_right_args =
460 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
462 let right_args_no = List.length right_args in
463 let lifted_left_args =
464 List.map (CicSubstitution.lift right_args_no) left_args
466 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
467 (lifted_left_args @ mk_right_args right_args_no))
470 FreshNamesGenerator.mk_fresh_name ~subst metasenv
471 context Cic.Anonymous ~typ:ty
473 match outtypeinstances with
475 let extended_context =
476 let rec add_right_args =
478 Cic.Prod (name,ty,t) ->
479 Some (name,Cic.Decl ty)::(add_right_args t)
482 (Some (fresh_name,Cic.Decl ty))::
484 (add_right_args arity_instantiated_with_left_args))@
487 let metasenv,new_meta =
488 CicMkImplicit.mk_implicit metasenv subst extended_context
491 CicMkImplicit.identity_relocation_list_for_metavariable
494 let rec add_lambdas b =
496 Cic.Prod (name,ty,t) ->
497 Cic.Lambda (name,ty,(add_lambdas b t))
498 | _ -> Cic.Lambda (fresh_name, ty, b)
501 add_lambdas (Cic.Meta (new_meta,irl))
502 arity_instantiated_with_left_args
504 (Some candidate),ugraph4,metasenv,subst
505 | (constructor_args_no,_,instance,_)::tl ->
507 let instance',subst,metasenv =
508 CicMetaSubst.delift_rels subst metasenv
509 constructor_args_no instance
511 let candidate,ugraph,metasenv,subst =
513 fun (candidate_oty,ugraph,metasenv,subst)
514 (constructor_args_no,_,instance,_) ->
515 match candidate_oty with
516 | None -> None,ugraph,metasenv,subst
519 let instance',subst,metasenv =
520 CicMetaSubst.delift_rels subst metasenv
521 constructor_args_no instance
523 let subst,metasenv,ugraph =
524 fo_unif_subst subst context metasenv
527 candidate_oty,ugraph,metasenv,subst
529 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
530 | CicUnification.UnificationFailure _
531 | CicUnification.Uncertain _ ->
532 None,ugraph,metasenv,subst
533 ) (Some instance',ugraph4,metasenv,subst) tl
536 | None -> None, ugraph,metasenv,subst
538 let rec add_lambdas n b =
540 Cic.Prod (name,ty,t) ->
541 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
543 Cic.Lambda (fresh_name, ty,
544 CicSubstitution.lift (n + 1) t)
547 (add_lambdas 0 t arity_instantiated_with_left_args),
548 ugraph,metasenv,subst
549 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
550 None,ugraph4,metasenv,subst
553 | None -> raise (Uncertain "can't solve an higher order unification problem")
555 let subst,metasenv,ugraph =
556 fo_unif_subst subst context metasenv
557 candidate outtype ugraph5
559 C.MutCase (uri, i, outtype, term', pl'),
560 CicReduction.head_beta_reduce
561 (CicMetaSubst.apply_subst subst
562 (Cic.Appl (outtype::right_args@[term']))),
563 subst,metasenv,ugraph)
564 | _ -> (* easy case *)
565 let _,_, subst, metasenv,ugraph5 =
566 type_of_aux subst metasenv context
567 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
569 let (subst,metasenv,ugraph6) =
571 (fun (subst,metasenv,ugraph)
572 (constructor_args_no,context,instance,args) ->
576 CicSubstitution.lift constructor_args_no outtype
578 C.Appl (outtype'::args)
580 CicReduction.whd ~subst context appl
582 fo_unif_subst subst context metasenv
583 instance instance' ugraph)
584 (subst,metasenv,ugraph5) outtypeinstances
586 C.MutCase (uri, i, outtype, term', pl'),
587 CicReduction.head_beta_reduce
588 (CicMetaSubst.apply_subst subst
589 (C.Appl(outtype::right_args@[term]))),
590 subst,metasenv,ugraph6)
592 let fl_ty',subst,metasenv,types,ugraph1 =
594 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
595 let ty',_,subst',metasenv',ugraph1 =
596 type_of_aux subst metasenv context ty ugraph
598 fl @ [ty'],subst',metasenv',
599 Some (C.Name n,(C.Decl ty')) :: types, ugraph
600 ) ([],subst,metasenv,[],ugraph) fl
602 let len = List.length types in
603 let context' = types@context in
604 let fl_bo',subst,metasenv,ugraph2 =
606 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
607 let bo',ty_of_bo,subst,metasenv,ugraph1 =
608 type_of_aux subst metasenv context' bo ugraph
610 let subst',metasenv',ugraph' =
611 fo_unif_subst subst context' metasenv
612 ty_of_bo (CicSubstitution.lift len ty) ugraph1
614 fl @ [bo'] , subst',metasenv',ugraph'
615 ) ([],subst,metasenv,ugraph1) fl
617 let (_,_,ty,_) = List.nth fl i in
618 (* now we have the new ty in fl_ty', the new bo in fl_bo',
619 * and we want the new fl with bo' and ty' injected in the right
622 let rec map3 f l1 l2 l3 =
625 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
628 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
631 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
633 let fl_ty',subst,metasenv,types,ugraph1 =
635 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
636 let ty',_,subst',metasenv',ugraph1 =
637 type_of_aux subst metasenv context ty ugraph
639 fl @ [ty'],subst',metasenv',
640 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
641 ) ([],subst,metasenv,[],ugraph) fl
643 let len = List.length types in
644 let context' = types@context in
645 let fl_bo',subst,metasenv,ugraph2 =
647 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
648 let bo',ty_of_bo,subst,metasenv,ugraph1 =
649 type_of_aux subst metasenv context' bo ugraph
651 let subst',metasenv',ugraph' =
652 fo_unif_subst subst context' metasenv
653 ty_of_bo (CicSubstitution.lift len ty) ugraph1
655 fl @ [bo'],subst',metasenv',ugraph'
656 ) ([],subst,metasenv,ugraph1) fl
658 let (_,ty,_) = List.nth fl i in
659 (* now we have the new ty in fl_ty', the new bo in fl_bo',
660 * and we want the new fl with bo' and ty' injected in the right
663 let rec map3 f l1 l2 l3 =
666 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
669 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
672 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
674 (* check_metasenv_consistency checks that the "canonical" context of a
675 metavariable is consitent - up to relocation via the relocation list l -
676 with the actual context *)
677 and check_metasenv_consistency
678 metano subst metasenv context canonical_context l ugraph
680 let module C = Cic in
681 let module R = CicReduction in
682 let module S = CicSubstitution in
683 let lifted_canonical_context =
687 | (Some (n,C.Decl t))::tl ->
688 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
689 | (Some (n,C.Def (t,None)))::tl ->
690 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
691 | None::tl -> None::(aux (i+1) tl)
692 | (Some (n,C.Def (t,Some ty)))::tl ->
694 C.Def ((S.subst_meta l (S.lift i t)),
695 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
697 aux 1 canonical_context
701 (fun (l,subst,metasenv,ugraph) t ct ->
704 l @ [None],subst,metasenv,ugraph
705 | Some t,Some (_,C.Def (ct,_)) ->
706 let subst',metasenv',ugraph' =
708 fo_unif_subst subst context metasenv t ct ugraph
709 with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
711 l @ [Some t],subst',metasenv',ugraph'
712 | Some t,Some (_,C.Decl ct) ->
713 let t',inferredty,subst',metasenv',ugraph1 =
714 type_of_aux subst metasenv context t ugraph
716 let subst'',metasenv'',ugraph2 =
719 subst' context metasenv' inferredty ct ugraph1
720 with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
722 l @ [Some t'], subst'',metasenv'',ugraph2
724 raise (RefineFailure (sprintf
725 "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"
726 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
727 (CicMetaSubst.ppcontext subst canonical_context)))
728 ) ([],subst,metasenv,ugraph) l lifted_canonical_context
730 Invalid_argument _ ->
734 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
735 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
736 (CicMetaSubst.ppcontext subst canonical_context)))
738 and check_exp_named_subst metasubst metasenv context tl ugraph =
739 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
741 [] -> [],metasubst,metasenv,ugraph
742 | ((uri,t) as subst)::tl ->
743 let ty_uri,ugraph1 = type_of_variable uri ugraph in
745 CicSubstitution.subst_vars substs ty_uri in
746 (* CSC: why was this code here? it is wrong
747 (match CicEnvironment.get_cooked_obj ~trust:false uri with
748 Cic.Variable (_,Some bo,_,_) ->
751 "A variable with a body can not be explicit substituted")
752 | Cic.Variable (_,None,_,_) -> ()
756 ("Unkown variable definition " ^ UriManager.string_of_uri uri))
759 let t',typeoft,metasubst',metasenv',ugraph2 =
760 type_of_aux metasubst metasenv context t ugraph1
762 let metasubst'',metasenv'',ugraph3 =
765 metasubst' context metasenv' typeoft typeofvar ugraph2
768 ("Wrong Explicit Named Substitution: " ^
769 CicMetaSubst.ppterm metasubst' typeoft ^
770 " not unifiable with " ^
771 CicMetaSubst.ppterm metasubst' typeofvar))
773 (* FIXME: no mere tail recursive! *)
774 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
775 check_exp_named_subst_aux
776 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
778 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
780 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
783 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
784 let module C = Cic in
785 let context_for_t2 = (Some (name,C.Decl s))::context in
786 let t1'' = CicReduction.whd ~subst context t1 in
787 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
788 match (t1'', t2'') with
789 (C.Sort s1, C.Sort s2)
790 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
791 C.Sort s2,subst,metasenv,ugraph
792 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
793 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
794 let t' = CicUniv.fresh() in
795 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
796 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
797 C.Sort (C.Type t'),subst,metasenv,ugraph2
798 | (C.Sort _,C.Sort (C.Type t1)) ->
799 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
800 C.Sort (C.Type t1),subst,metasenv,ugraph
801 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
802 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
803 (* TODO how can we force the meta to become a sort? If we don't we
804 * brake the invariant that refine produce only well typed terms *)
805 (* TODO if we check the non meta term and if it is a sort then we are
806 * likely to know the exact value of the result e.g. if the rhs is a
807 * Sort (Prop | Set | CProp) then the result is the rhs *)
809 CicMkImplicit.mk_implicit_sort metasenv subst in
810 let (subst, metasenv,ugraph1) =
811 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
813 t2'',subst,metasenv,ugraph1
815 raise (RefineFailure (sprintf
816 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
817 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
818 (CicPp.ppterm t2'')))
820 and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
821 let rec mk_prod metasenv context =
824 let (metasenv, idx) =
825 CicMkImplicit.mk_implicit_type metasenv subst context
828 CicMkImplicit.identity_relocation_list_for_metavariable context
830 metasenv,Cic.Meta (idx, irl)
832 let (metasenv, idx) =
833 CicMkImplicit.mk_implicit_type metasenv subst context
836 CicMkImplicit.identity_relocation_list_for_metavariable context
838 let meta = Cic.Meta (idx,irl) in
840 (* The name must be fresh for context. *)
841 (* Nevertheless, argty is well-typed only in context. *)
842 (* Thus I generate a name (name_hint) in context and *)
843 (* then I generate a name --- using the hint name_hint *)
844 (* --- that is fresh in (context'@context). *)
846 (* Cic.Name "pippo" *)
847 FreshNamesGenerator.mk_fresh_name ~subst metasenv
848 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
849 (CicMetaSubst.apply_subst_context subst context)
851 ~typ:(CicMetaSubst.apply_subst subst argty)
853 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
854 FreshNamesGenerator.mk_fresh_name ~subst
855 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
857 let metasenv,target =
858 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
860 metasenv,Cic.Prod (name,meta,target)
862 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
863 let (subst, metasenv,ugraph1) =
865 fo_unif_subst subst context metasenv hetype hetype' ugraph
867 debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
868 (CicPp.ppterm hetype)
869 (CicPp.ppterm hetype')
870 (CicMetaSubst.ppmetasenv metasenv [])
871 (CicMetaSubst.ppsubst subst));
875 let rec eat_prods metasenv subst context hetype ugraph =
877 | [] -> [],metasenv,subst,hetype,ugraph
878 | (hete, hety)::tl ->
881 let arg,subst,metasenv,ugraph1 =
883 let subst,metasenv,ugraph1 =
884 fo_unif_subst subst context metasenv hety s ugraph
886 hete,subst,metasenv,ugraph1
888 (* we search a coercion from hety to s *)
889 let coer = CoercGraph.look_for_coercion
890 (CicMetaSubst.apply_subst subst hety)
891 (CicMetaSubst.apply_subst subst s)
896 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
898 let coerced_args,metasenv',subst',t',ugraph2 =
899 eat_prods metasenv subst context
900 (* (CicMetaSubst.subst subst hete t) tl *)
901 (CicSubstitution.subst hete t) ugraph1 tl
903 arg::coerced_args,metasenv',subst',t',ugraph2
907 let coerced_args,metasenv,subst,t,ugraph2 =
908 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
910 coerced_args,t,subst,metasenv,ugraph2
913 (* eat prods ends here! *)
915 let t',ty,subst',metasenv',ugraph1 =
916 type_of_aux [] metasenv context t ugraph
918 let substituted_t = CicMetaSubst.apply_subst subst' t' in
919 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
920 (* Andrea: ho rimesso qui l'applicazione della subst al
921 metasenv dopo che ho droppato l'invariante che il metsaenv
922 e' sempre istanziato *)
923 let substituted_metasenv =
924 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
926 (* substituted_t,substituted_ty,substituted_metasenv *)
927 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
929 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
931 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
932 let cleaned_metasenv =
934 (function (n,context,ty) ->
935 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
940 | Some (n, Cic.Decl t) ->
942 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
943 | Some (n, Cic.Def (bo,ty)) ->
944 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
949 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
951 Some (n, Cic.Def (bo',ty'))
955 ) substituted_metasenv
957 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
960 let type_of_aux' metasenv context term ugraph =
962 type_of_aux' metasenv context term ugraph
964 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
966 (*CSC: this is a very very rough approximation; to be finished *)
967 let are_all_occurrences_positive uri =
969 (*CSC: here we should do a whd; but can we do that? *)
971 Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
972 | Cic.MutInd (uri',_,_) when uri = uri' -> ()
973 | Cic.Prod (_,_,t) -> aux t
974 | _ -> raise (RefineFailure "not well formed constructor type")
978 let typecheck metasenv uri obj =
979 let ugraph = CicUniv.empty_ugraph in
981 Cic.Constant (name,Some bo,ty,args,attrs) ->
982 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
983 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
984 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
985 let bo' = CicMetaSubst.apply_subst subst bo' in
986 let ty' = CicMetaSubst.apply_subst subst ty' in
987 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
988 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
989 | Cic.Constant (name,None,ty,args,attrs) ->
990 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
991 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
992 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
993 assert (metasenv' = metasenv);
994 (* Here we do not check the metasenv for correctness *)
995 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
996 let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1000 (* instead of raising Uncertain, let's hope that the meta will become
1003 | _ -> raise (RefineFailure "The term provided is not a type")
1005 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1006 let bo' = CicMetaSubst.apply_subst subst bo' in
1007 let ty' = CicMetaSubst.apply_subst subst ty' in
1008 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1009 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1010 | Cic.Variable _ -> assert false (* not implemented *)
1011 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1012 (*CSC: this code is greately simplified and many many checks are missing *)
1013 (*CSC: e.g. the constructors are not required to build their own types, *)
1014 (*CSC: the arities are not required to have as type a sort, etc. *)
1015 let uri = match uri with Some uri -> uri | None -> assert false in
1016 let typesno = List.length tys in
1017 (* first phase: we fix only the types *)
1018 let metasenv,ugraph,tys =
1020 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1021 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1022 metasenv,ugraph,(name,b,ty',cl)::res
1023 ) tys (metasenv,ugraph,[]) in
1025 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1026 (* second phase: we fix only the constructors *)
1027 let metasenv,ugraph,tys =
1029 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1030 let metasenv,ugraph,cl' =
1032 (fun (name,ty) (metasenv,ugraph,res) ->
1033 let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1034 let ty',_,metasenv,ugraph =
1035 type_of_aux' metasenv con_context ty ugraph in
1039 (fun (name,_,_,_) (i,t) ->
1040 (* here the explicit_named_substituion is assumed to be *)
1042 let t' = Cic.MutInd (uri,i,[]) in
1043 let t = CicSubstitution.subst t' t in
1045 ) tys (typesno - 1,t)) in
1046 let ty' = undebrujin ty' in
1047 metasenv,ugraph,(name,ty')::res
1048 ) cl (metasenv,ugraph,[])
1050 metasenv,ugraph,(name,b,ty,cl')::res
1051 ) tys (metasenv,ugraph,[]) in
1052 (* third phase: we check the positivity condition *)
1055 List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
1057 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1060 let type_of_aux' metasenv context term =
1063 type_of_aux' metasenv context term in
1065 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
1067 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
1070 | RefineFailure msg as e ->
1071 debug_print ("@@@ REFINE FAILED: " ^ msg);
1073 | Uncertain msg as e ->
1074 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);