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
56 CicEnvironment.get_cooked_obj uri
57 with Not_found -> assert false
60 let obj,u= CicEnvironment.get_obj ugraph uri in
62 C.Constant (_,_,ty,_,_) -> ty,u
63 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
66 (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
68 and type_of_variable uri ugraph =
70 let module R = CicReduction in
71 let module U = UriManager in
75 CicEnvironment.get_cooked_obj uri
76 with Not_found -> assert false
79 let obj,u = CicEnvironment.get_obj ugraph uri in
81 C.Variable (_,_,ty,_,_) -> ty,u
85 ("Unknown variable definition " ^ UriManager.string_of_uri uri))
87 and type_of_mutual_inductive_defs uri i ugraph =
89 let module R = CicReduction in
90 let module U = UriManager in
94 CicEnvironment.get_cooked_obj uri
95 with Not_found -> assert false
98 let obj,u = CicEnvironment.get_obj ugraph uri in
100 C.InductiveDefinition (dl,_,_,_) ->
101 let (_,_,arity,_) = List.nth dl i in
106 ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
108 and type_of_mutual_inductive_constr uri i j ugraph =
109 let module C = Cic in
110 let module R = CicReduction in
111 let module U = UriManager in
115 CicEnvironment.get_cooked_obj uri
116 with Not_found -> assert false
119 let obj,u = CicEnvironment.get_obj ugraph uri in
121 C.InductiveDefinition (dl,_,_,_) ->
122 let (_,_,_,cl) = List.nth dl i in
123 let (_,ty) = List.nth cl (j-1) in
128 ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
131 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
133 (* the check_branch function checks if a branch of a case is refinable.
134 It returns a pair (outype_instance,args), a subst and a metasenv.
135 outype_instance is the expected result of applying the case outtype
137 The problem is that outype is in general unknown, and we should
138 try to synthesize it from the above information, that is in general
139 a second order unification problem. *)
141 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
142 let module C = Cic in
143 (* let module R = CicMetaSubst in *)
144 let module R = CicReduction in
145 match R.whd ~subst context expectedtype with
147 (n,context,actualtype, [term]), subst, metasenv, ugraph
148 | C.Appl (C.MutInd (_,_,_)::tl) ->
149 let (_,arguments) = split tl left_args_no in
150 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
151 | C.Prod (name,so,de) ->
152 (* we expect that the actual type of the branch has the due
154 (match R.whd ~subst context actualtype with
155 C.Prod (name',so',de') ->
156 let subst, metasenv, ugraph1 =
157 fo_unif_subst subst context metasenv so so' ugraph in
159 (match CicSubstitution.lift 1 term with
160 C.Appl l -> C.Appl (l@[C.Rel 1])
161 | t -> C.Appl [t ; C.Rel 1]) in
162 (* we should also check that the name variable is anonymous in
163 the actual type de' ?? *)
165 ((Some (name,(C.Decl so)))::context)
166 metasenv subst left_args_no de' term' de ugraph1
167 | _ -> raise (AssertFailure "Wrong number of arguments"))
168 | _ -> raise (AssertFailure "Prod or MutInd expected")
170 and type_of_aux' metasenv context t ugraph =
171 let rec type_of_aux subst metasenv context t ugraph =
172 let module C = Cic in
173 let module S = CicSubstitution in
174 let module U = UriManager in
179 match List.nth context (n - 1) with
180 Some (_,C.Decl ty) ->
181 t,S.lift n ty,subst,metasenv, ugraph
182 | Some (_,C.Def (_,Some ty)) ->
183 t,S.lift n ty,subst,metasenv, ugraph
184 | Some (_,C.Def (bo,None)) ->
185 type_of_aux subst metasenv context (S.lift n bo) ugraph
186 | None -> raise (RefineFailure "Rel to hidden hypothesis")
188 _ -> raise (RefineFailure "Not a close term")
190 | C.Var (uri,exp_named_subst) ->
191 let exp_named_subst',subst',metasenv',ugraph1 =
192 check_exp_named_subst
193 subst metasenv context exp_named_subst ugraph
195 let ty_uri,ugraph1 = type_of_variable uri ugraph in
197 CicSubstitution.subst_vars exp_named_subst' ty_uri
199 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
202 let (canonical_context, term,ty) =
203 CicUtil.lookup_subst n subst
205 let l',subst',metasenv',ugraph1 =
206 check_metasenv_consistency n subst metasenv context
207 canonical_context l ugraph
209 (* trust or check ??? *)
210 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
211 subst', metasenv', ugraph1
212 (* type_of_aux subst metasenv
213 context (CicSubstitution.subst_meta l term) *)
214 with CicUtil.Subst_not_found _ ->
215 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
216 let l',subst',metasenv', ugraph1 =
217 check_metasenv_consistency n subst metasenv context
218 canonical_context l ugraph
220 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
221 subst', metasenv',ugraph1)
222 | C.Sort (C.Type tno) ->
223 let tno' = CicUniv.fresh() in
224 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
225 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
227 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
228 | C.Implicit _ -> raise (AssertFailure "21")
230 let ty',_,subst',metasenv',ugraph1 =
231 type_of_aux subst metasenv context ty ugraph
233 let te',inferredty,subst'',metasenv'',ugraph2 =
234 type_of_aux subst' metasenv' context te ugraph1
237 let subst''',metasenv''',ugraph3 =
238 fo_unif_subst subst'' context metasenv''
239 inferredty ty ugraph2
241 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
243 _ -> raise (RefineFailure "Cast"))
244 | C.Prod (name,s,t) ->
245 let s',sort1,subst',metasenv',ugraph1 =
246 type_of_aux subst metasenv context s ugraph
248 let t',sort2,subst'',metasenv'',ugraph2 =
249 type_of_aux subst' metasenv'
250 ((Some (name,(C.Decl s')))::context) t ugraph1
252 let sop,subst''',metasenv''',ugraph3 =
253 sort_of_prod subst'' metasenv''
254 context (name,s') (sort1,sort2) ugraph2
256 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
257 | C.Lambda (n,s,t) ->
258 let s',sort1,subst',metasenv',ugraph1 =
259 type_of_aux subst metasenv context s ugraph
261 (match CicReduction.whd ~subst:subst' context sort1 with
265 raise (RefineFailure (sprintf
266 "Not well-typed lambda-abstraction: the source %s should be a type;
267 instead it is a term of type %s" (CicPp.ppterm s)
268 (CicPp.ppterm sort1)))
270 let t',type2,subst'',metasenv'',ugraph2 =
271 type_of_aux subst' metasenv'
272 ((Some (n,(C.Decl s')))::context) t ugraph1
274 C.Lambda (n,s',t'),C.Prod (n,s',type2),
275 subst'',metasenv'',ugraph2
277 (* only to check if s is well-typed *)
278 let s',ty,subst',metasenv',ugraph1 =
279 type_of_aux subst metasenv context s ugraph
281 let t',inferredty,subst'',metasenv'',ugraph2 =
282 type_of_aux subst' metasenv'
283 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
285 (* One-step LetIn reduction.
286 * Even faster than the previous solution.
287 * Moreover the inferred type is closer to the expected one.
289 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
290 subst',metasenv',ugraph2
291 | C.Appl (he::((_::_) as tl)) ->
292 let he',hetype,subst',metasenv',ugraph1 =
293 type_of_aux subst metasenv context he ugraph
295 let tlbody_and_type,subst'',metasenv'',ugraph2 =
297 (fun x (res,subst,metasenv,ugraph) ->
298 let x',ty,subst',metasenv',ugraph1 =
299 type_of_aux subst metasenv context x ugraph
301 (x', ty)::res,subst',metasenv',ugraph1
302 ) tl ([],subst',metasenv',ugraph1)
304 let tl',applty,subst''',metasenv''',ugraph3 =
305 eat_prods subst'' metasenv'' context
306 hetype tlbody_and_type ugraph2
308 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
309 | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
310 | C.Const (uri,exp_named_subst) ->
311 let exp_named_subst',subst',metasenv',ugraph1 =
312 check_exp_named_subst subst metasenv context
313 exp_named_subst ugraph in
314 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
316 CicSubstitution.subst_vars exp_named_subst' ty_uri
318 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
319 | C.MutInd (uri,i,exp_named_subst) ->
320 let exp_named_subst',subst',metasenv',ugraph1 =
321 check_exp_named_subst subst metasenv context
322 exp_named_subst ugraph
324 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
326 CicSubstitution.subst_vars exp_named_subst' ty_uri in
327 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
328 | C.MutConstruct (uri,i,j,exp_named_subst) ->
329 let exp_named_subst',subst',metasenv',ugraph1 =
330 check_exp_named_subst subst metasenv context
331 exp_named_subst ugraph
334 type_of_mutual_inductive_constr uri i j ugraph1
337 CicSubstitution.subst_vars exp_named_subst' ty_uri
339 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
341 | C.MutCase (uri, i, outtype, term, pl) ->
342 (* first, get the inductive type (and noparams)
343 * in the environment *)
344 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
345 let obj,u = CicEnvironment.get_obj ugraph uri in
347 C.InductiveDefinition (l,expl_params,parsno,_) ->
348 List.nth l i , expl_params, parsno, u
352 ("Unkown mutual inductive definition " ^
353 U.string_of_uri uri))
355 let rec count_prod t =
356 match CicReduction.whd ~subst context t with
357 C.Prod (_, _, t) -> 1 + (count_prod t)
360 let no_args = count_prod arity in
361 (* now, create a "generic" MutInd *)
362 let metasenv,left_args =
363 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
365 let metasenv,right_args =
366 let no_right_params = no_args - no_left_params in
367 if no_right_params < 0 then assert false
368 else CicMkImplicit.n_fresh_metas
369 metasenv subst context no_right_params
371 let metasenv,exp_named_subst =
372 CicMkImplicit.fresh_subst metasenv subst context expl_params in
375 C.MutInd (uri,i,exp_named_subst)
378 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
380 (* check consistency with the actual type of term *)
381 let term',actual_type,subst,metasenv,ugraph1 =
382 type_of_aux subst metasenv context term ugraph in
383 let expected_type',_, subst, metasenv,ugraph2 =
384 type_of_aux subst metasenv context expected_type ugraph1
386 let actual_type = CicReduction.whd ~subst context actual_type in
387 let subst,metasenv,ugraph3 =
388 fo_unif_subst subst context metasenv
389 expected_type' actual_type ugraph2
391 let rec instantiate_prod t =
395 match CicReduction.whd ~subst context t with
397 instantiate_prod (CicSubstitution.subst he t') tl
400 let arity_instantiated_with_left_args =
401 instantiate_prod arity left_args in
402 (* TODO: check if the sort elimination
403 * is allowed: [(I q1 ... qr)|B] *)
404 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
406 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
408 if left_args = [] then
409 (C.MutConstruct (uri,i,j,exp_named_subst))
412 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
414 let p',actual_type,subst,metasenv,ugraph1 =
415 type_of_aux subst metasenv context p ugraph
417 let constructor',expected_type, subst, metasenv,ugraph2 =
418 type_of_aux subst metasenv context constructor ugraph1
420 let outtypeinstance,subst,metasenv,ugraph3 =
421 check_branch 0 context metasenv subst no_left_params
422 actual_type constructor' expected_type ugraph2
425 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
426 ([],1,[],subst,metasenv,ugraph3) pl
429 (* we are left to check that the outype matches his instances.
430 The easy case is when the outype is specified, that amount
431 to a trivial check. Otherwise, we should guess a type from
437 (let candidate,ugraph5,metasenv,subst =
438 let exp_name_subst, metasenv =
440 CicEnvironment.get_obj CicUniv.empty_ugraph uri
442 let uris = CicUtil.params_of_obj o in
444 fun uri (acc,metasenv) ->
445 let metasenv',new_meta =
446 CicMkImplicit.mk_implicit metasenv subst context
449 CicMkImplicit.identity_relocation_list_for_metavariable
452 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
456 match left_args,right_args with
457 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
459 let rec mk_right_args =
462 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
464 let right_args_no = List.length right_args in
465 let lifted_left_args =
466 List.map (CicSubstitution.lift right_args_no) left_args
468 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
469 (lifted_left_args @ mk_right_args right_args_no))
472 FreshNamesGenerator.mk_fresh_name ~subst metasenv
473 context Cic.Anonymous ~typ:ty
475 match outtypeinstances with
477 let extended_context =
478 let rec add_right_args =
480 Cic.Prod (name,ty,t) ->
481 Some (name,Cic.Decl ty)::(add_right_args t)
484 (Some (fresh_name,Cic.Decl ty))::
486 (add_right_args arity_instantiated_with_left_args))@
489 let metasenv,new_meta =
490 CicMkImplicit.mk_implicit metasenv subst extended_context
493 CicMkImplicit.identity_relocation_list_for_metavariable
496 let rec add_lambdas b =
498 Cic.Prod (name,ty,t) ->
499 Cic.Lambda (name,ty,(add_lambdas b t))
500 | _ -> Cic.Lambda (fresh_name, ty, b)
503 add_lambdas (Cic.Meta (new_meta,irl))
504 arity_instantiated_with_left_args
506 (Some candidate),ugraph4,metasenv,subst
507 | (constructor_args_no,_,instance,_)::tl ->
510 CicSubstitution.delift constructor_args_no
511 (CicMetaSubst.apply_subst subst instance)
513 let candidate,ugraph,metasenv,subst =
515 fun (candidate_oty,ugraph,metasenv,subst)
516 (constructor_args_no,_,instance,_) ->
517 match candidate_oty with
518 | None -> None,ugraph,metasenv,subst
522 CicSubstitution.delift
524 (CicMetaSubst.apply_subst subst instance)
526 debug_print ("PRIMA subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst);
527 let subst,metasenv,ugraph =
528 fo_unif_subst subst context metasenv
531 debug_print ("DOPO subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst);
532 candidate_oty,ugraph,metasenv,subst
535 CicReduction.are_convertible context
539 candidate_oty,ugraph1,metasenv
545 | CicUnification.UnificationFailure _
546 | CicUnification.Uncertain _ ->
547 None,ugraph,metasenv,subst
548 ) (Some instance',ugraph4,metasenv,subst) tl
551 | None -> None, ugraph,metasenv,subst
553 let rec add_lambdas n b =
555 Cic.Prod (name,ty,t) ->
556 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
558 Cic.Lambda (fresh_name, ty,
559 CicSubstitution.lift (n + 1) t)
562 (add_lambdas 0 t arity_instantiated_with_left_args),
563 ugraph,metasenv,subst
565 None,ugraph4,metasenv,subst
568 | None -> raise (Uncertain "can't solve an higher order unification problem")
570 let subst,metasenv,ugraph =
571 fo_unif_subst subst context metasenv
572 candidate outtype ugraph5
574 C.MutCase (uri, i, outtype, term', pl'),
575 (Cic.Appl (outtype::right_args@[term'])),
576 subst,metasenv,ugraph)
577 | _ -> (* easy case *)
578 let _,_, subst, metasenv,ugraph5 =
579 type_of_aux subst metasenv context
580 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
582 let (subst,metasenv,ugraph6) =
584 (fun (subst,metasenv,ugraph)
585 (constructor_args_no,context,instance,args) ->
589 CicSubstitution.lift constructor_args_no outtype
591 C.Appl (outtype'::args)
593 CicReduction.whd ~subst context appl
595 fo_unif_subst subst context metasenv
596 instance instance' ugraph)
597 (subst,metasenv,ugraph5) outtypeinstances
599 C.MutCase (uri, i, outtype, term', pl'),
600 CicReduction.whd ~subst context
601 (C.Appl(outtype::right_args@[term])),
602 subst,metasenv,ugraph6)
604 let fl_ty',subst,metasenv,types,ugraph1 =
606 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
607 let ty',_,subst',metasenv',ugraph1 =
608 type_of_aux subst metasenv context ty ugraph
610 fl @ [ty'],subst',metasenv',
611 Some (C.Name n,(C.Decl ty')) :: types, ugraph
612 ) ([],subst,metasenv,[],ugraph) fl
614 let len = List.length types in
615 let context' = types@context in
616 let fl_bo',subst,metasenv,ugraph2 =
618 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
619 let bo',ty_of_bo,subst,metasenv,ugraph1 =
620 type_of_aux subst metasenv context' bo ugraph
622 let subst',metasenv',ugraph' =
623 fo_unif_subst subst context' metasenv
624 ty_of_bo (CicSubstitution.lift len ty) ugraph1
626 fl @ [bo'] , subst',metasenv',ugraph'
627 ) ([],subst,metasenv,ugraph1) fl
629 let (_,_,ty,_) = List.nth fl i in
630 (* now we have the new ty in fl_ty', the new bo in fl_bo',
631 * and we want the new fl with bo' and ty' injected in the right
634 let rec map3 f l1 l2 l3 =
637 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
640 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
643 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
645 let fl_ty',subst,metasenv,types,ugraph1 =
647 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
648 let ty',_,subst',metasenv',ugraph1 =
649 type_of_aux subst metasenv context ty ugraph
651 fl @ [ty'],subst',metasenv',
652 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
653 ) ([],subst,metasenv,[],ugraph) fl
655 let len = List.length types in
656 let context' = types@context in
657 let fl_bo',subst,metasenv,ugraph2 =
659 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
660 let bo',ty_of_bo,subst,metasenv,ugraph1 =
661 type_of_aux subst metasenv context' bo ugraph
663 let subst',metasenv',ugraph' =
664 fo_unif_subst subst context' metasenv
665 ty_of_bo (CicSubstitution.lift len ty) ugraph1
667 fl @ [bo'],subst',metasenv',ugraph'
668 ) ([],subst,metasenv,ugraph1) fl
670 let (_,ty,_) = List.nth fl i in
671 (* now we have the new ty in fl_ty', the new bo in fl_bo',
672 * and we want the new fl with bo' and ty' injected in the right
675 let rec map3 f l1 l2 l3 =
678 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
681 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
684 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
686 (* check_metasenv_consistency checks that the "canonical" context of a
687 metavariable is consitent - up to relocation via the relocation list l -
688 with the actual context *)
689 and check_metasenv_consistency
690 metano subst metasenv context canonical_context l ugraph
692 let module C = Cic in
693 let module R = CicReduction in
694 let module S = CicSubstitution in
695 let lifted_canonical_context =
699 | (Some (n,C.Decl t))::tl ->
700 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
701 | (Some (n,C.Def (t,None)))::tl ->
702 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
703 | None::tl -> None::(aux (i+1) tl)
704 | (Some (n,C.Def (t,Some ty)))::tl ->
706 C.Def ((S.subst_meta l (S.lift i t)),
707 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
709 aux 1 canonical_context
713 (fun (l,subst,metasenv,ugraph) t ct ->
716 l @ [None],subst,metasenv,ugraph
717 | Some t,Some (_,C.Def (ct,_)) ->
718 let subst',metasenv',ugraph' =
720 fo_unif_subst subst context metasenv t ct ugraph
721 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)))))
723 l @ [Some t],subst',metasenv',ugraph'
724 | Some t,Some (_,C.Decl ct) ->
725 let t',inferredty,subst',metasenv',ugraph1 =
726 type_of_aux subst metasenv context t ugraph
728 let subst'',metasenv'',ugraph2 =
731 subst' context metasenv' inferredty ct ugraph1
732 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)))))
734 l @ [Some t'], subst'',metasenv'',ugraph2
736 raise (RefineFailure (sprintf
737 "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"
738 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
739 (CicMetaSubst.ppcontext subst canonical_context)))
740 ) ([],subst,metasenv,ugraph) l lifted_canonical_context
742 Invalid_argument _ ->
746 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
747 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
748 (CicMetaSubst.ppcontext subst canonical_context)))
750 and check_exp_named_subst metasubst metasenv context tl ugraph =
751 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
753 [] -> [],metasubst,metasenv,ugraph
754 | ((uri,t) as subst)::tl ->
755 let ty_uri,ugraph1 = type_of_variable uri ugraph in
757 CicSubstitution.subst_vars substs ty_uri in
758 (* CSC: why was this code here? it is wrong
759 (match CicEnvironment.get_cooked_obj ~trust:false uri with
760 Cic.Variable (_,Some bo,_,_) ->
763 "A variable with a body can not be explicit substituted")
764 | Cic.Variable (_,None,_,_) -> ()
768 ("Unkown variable definition " ^ UriManager.string_of_uri uri))
771 let t',typeoft,metasubst',metasenv',ugraph2 =
772 type_of_aux metasubst metasenv context t ugraph1
774 let metasubst'',metasenv'',ugraph3 =
777 metasubst' context metasenv' typeoft typeofvar ugraph2
780 ("Wrong Explicit Named Substitution: " ^
781 CicMetaSubst.ppterm metasubst' typeoft ^
782 " not unifiable with " ^
783 CicMetaSubst.ppterm metasubst' typeofvar))
785 (* FIXME: no mere tail recursive! *)
786 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
787 check_exp_named_subst_aux
788 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
790 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
792 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
795 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
796 let module C = Cic in
797 let context_for_t2 = (Some (name,C.Decl s))::context in
798 let t1'' = CicReduction.whd ~subst context t1 in
799 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
800 match (t1'', t2'') with
801 (C.Sort s1, C.Sort s2)
802 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
803 C.Sort s2,subst,metasenv,ugraph
804 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
805 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
806 let t' = CicUniv.fresh() in
807 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
808 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
809 C.Sort (C.Type t'),subst,metasenv,ugraph2
810 | (C.Sort _,C.Sort (C.Type t1)) ->
811 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
812 C.Sort (C.Type t1),subst,metasenv,ugraph
813 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
814 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
815 (* TODO how can we force the meta to become a sort? If we don't we
816 * brake the invariant that refine produce only well typed terms *)
817 (* TODO if we check the non meta term and if it is a sort then we are
818 * likely to know the exact value of the result e.g. if the rhs is a
819 * Sort (Prop | Set | CProp) then the result is the rhs *)
821 CicMkImplicit.mk_implicit_sort metasenv subst in
822 let (subst, metasenv,ugraph1) =
823 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
825 t2'',subst,metasenv,ugraph1
827 raise (RefineFailure (sprintf
828 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
829 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
830 (CicPp.ppterm t2'')))
832 and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
833 let rec mk_prod metasenv context =
836 let (metasenv, idx) =
837 CicMkImplicit.mk_implicit_type metasenv subst context
840 CicMkImplicit.identity_relocation_list_for_metavariable context
842 metasenv,Cic.Meta (idx, irl)
844 let (metasenv, idx) =
845 CicMkImplicit.mk_implicit_type metasenv subst context
848 CicMkImplicit.identity_relocation_list_for_metavariable context
850 let meta = Cic.Meta (idx,irl) in
852 (* The name must be fresh for context. *)
853 (* Nevertheless, argty is well-typed only in context. *)
854 (* Thus I generate a name (name_hint) in context and *)
855 (* then I generate a name --- using the hint name_hint *)
856 (* --- that is fresh in (context'@context). *)
858 (* Cic.Name "pippo" *)
859 FreshNamesGenerator.mk_fresh_name ~subst metasenv
860 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
861 (CicMetaSubst.apply_subst_context subst context)
863 ~typ:(CicMetaSubst.apply_subst subst argty)
865 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
866 FreshNamesGenerator.mk_fresh_name ~subst
867 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
869 let metasenv,target =
870 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
872 metasenv,Cic.Prod (name,meta,target)
874 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
875 let (subst, metasenv,ugraph1) =
877 fo_unif_subst subst context metasenv hetype hetype' ugraph
879 debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
880 (CicPp.ppterm hetype)
881 (CicPp.ppterm hetype')
882 (CicMetaSubst.ppmetasenv metasenv [])
883 (CicMetaSubst.ppsubst subst));
887 let rec eat_prods metasenv subst context hetype ugraph =
889 | [] -> [],metasenv,subst,hetype,ugraph
890 | (hete, hety)::tl ->
893 let arg,subst,metasenv,ugraph1 =
895 let subst,metasenv,ugraph1 =
896 fo_unif_subst subst context metasenv hety s ugraph
898 hete,subst,metasenv,ugraph1
900 (* we search a coercion from hety to s *)
901 let coer = CoercGraph.look_for_coercion
902 (CicMetaSubst.apply_subst subst hety)
903 (CicMetaSubst.apply_subst subst s)
908 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
910 let coerced_args,metasenv',subst',t',ugraph2 =
911 eat_prods metasenv subst context
912 (* (CicMetaSubst.subst subst hete t) tl *)
913 (CicSubstitution.subst hete t) ugraph1 tl
915 arg::coerced_args,metasenv',subst',t',ugraph2
919 let coerced_args,metasenv,subst,t,ugraph2 =
920 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
922 coerced_args,t,subst,metasenv,ugraph2
925 (* eat prods ends here! *)
927 let t',ty,subst',metasenv',ugraph1 =
928 type_of_aux [] metasenv context t ugraph
930 let substituted_t = CicMetaSubst.apply_subst subst' t' in
931 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
932 (* Andrea: ho rimesso qui l'applicazione della subst al
933 metasenv dopo che ho droppato l'invariante che il metsaenv
934 e' sempre istanziato *)
935 let substituted_metasenv =
936 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
938 (* substituted_t,substituted_ty,substituted_metasenv *)
939 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
941 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
943 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
944 let cleaned_metasenv =
946 (function (n,context,ty) ->
947 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
952 | Some (n, Cic.Decl t) ->
954 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
955 | Some (n, Cic.Def (bo,ty)) ->
956 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
961 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
963 Some (n, Cic.Def (bo',ty'))
967 ) substituted_metasenv
969 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
972 let type_of_aux' metasenv context term ugraph =
974 type_of_aux' metasenv context term ugraph
976 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
980 let type_of_aux' metasenv context term =
983 type_of_aux' metasenv context term in
985 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
987 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
990 | RefineFailure msg as e ->
991 debug_print ("@@@ REFINE FAILED: " ^ msg);
993 | Uncertain msg as e ->
994 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);