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)) ->
177 type_of_aux subst metasenv context (S.lift n bo) ugraph
178 | None -> raise (RefineFailure "Rel to hidden hypothesis")
180 _ -> raise (RefineFailure "Not a close term")
182 | C.Var (uri,exp_named_subst) ->
183 let exp_named_subst',subst',metasenv',ugraph1 =
184 check_exp_named_subst
185 subst metasenv context exp_named_subst ugraph
187 let ty_uri,ugraph1 = type_of_variable uri ugraph in
189 CicSubstitution.subst_vars exp_named_subst' ty_uri
191 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
194 let (canonical_context, term,ty) =
195 CicUtil.lookup_subst n subst
197 let l',subst',metasenv',ugraph1 =
198 check_metasenv_consistency n subst metasenv context
199 canonical_context l ugraph
201 (* trust or check ??? *)
202 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
203 subst', metasenv', ugraph1
204 (* type_of_aux subst metasenv
205 context (CicSubstitution.subst_meta l term) *)
206 with CicUtil.Subst_not_found _ ->
207 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
208 let l',subst',metasenv', ugraph1 =
209 check_metasenv_consistency n subst metasenv context
210 canonical_context l ugraph
212 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
213 subst', metasenv',ugraph1)
214 | C.Sort (C.Type tno) ->
215 let tno' = CicUniv.fresh() in
216 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
217 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
219 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
220 | C.Implicit _ -> raise (AssertFailure "21")
222 let ty',_,subst',metasenv',ugraph1 =
223 type_of_aux subst metasenv context ty ugraph
225 let te',inferredty,subst'',metasenv'',ugraph2 =
226 type_of_aux subst' metasenv' context te ugraph1
229 let subst''',metasenv''',ugraph3 =
230 fo_unif_subst subst'' context metasenv''
231 inferredty ty ugraph2
233 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
235 _ -> raise (RefineFailure "Cast"))
236 | C.Prod (name,s,t) ->
237 let s',sort1,subst',metasenv',ugraph1 =
238 type_of_aux subst metasenv context s ugraph
240 let t',sort2,subst'',metasenv'',ugraph2 =
241 type_of_aux subst' metasenv'
242 ((Some (name,(C.Decl s')))::context) t ugraph1
244 let sop,subst''',metasenv''',ugraph3 =
245 sort_of_prod subst'' metasenv''
246 context (name,s') (sort1,sort2) ugraph2
248 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
249 | C.Lambda (n,s,t) ->
250 let s',sort1,subst',metasenv',ugraph1 =
251 type_of_aux subst metasenv context s ugraph
253 (match CicReduction.whd ~subst:subst' context sort1 with
257 raise (RefineFailure (sprintf
258 "Not well-typed lambda-abstraction: the source %s should be a type;
259 instead it is a term of type %s" (CicPp.ppterm s)
260 (CicPp.ppterm sort1)))
262 let t',type2,subst'',metasenv'',ugraph2 =
263 type_of_aux subst' metasenv'
264 ((Some (n,(C.Decl s')))::context) t ugraph1
266 C.Lambda (n,s',t'),C.Prod (n,s',type2),
267 subst'',metasenv'',ugraph2
269 (* only to check if s is well-typed *)
270 let s',ty,subst',metasenv',ugraph1 =
271 type_of_aux subst metasenv context s ugraph
273 let t',inferredty,subst'',metasenv'',ugraph2 =
274 type_of_aux subst' metasenv'
275 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
277 (* One-step LetIn reduction.
278 * Even faster than the previous solution.
279 * Moreover the inferred type is closer to the expected one.
281 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
282 subst'',metasenv'',ugraph2
283 | C.Appl (he::((_::_) as tl)) ->
284 let he',hetype,subst',metasenv',ugraph1 =
285 type_of_aux subst metasenv context he ugraph
287 let tlbody_and_type,subst'',metasenv'',ugraph2 =
289 (fun x (res,subst,metasenv,ugraph) ->
290 let x',ty,subst',metasenv',ugraph1 =
291 type_of_aux subst metasenv context x ugraph
293 (x', ty)::res,subst',metasenv',ugraph1
294 ) tl ([],subst',metasenv',ugraph1)
296 let tl',applty,subst''',metasenv''',ugraph3 =
297 eat_prods subst'' metasenv'' context
298 hetype tlbody_and_type ugraph2
300 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
301 | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
302 | C.Const (uri,exp_named_subst) ->
303 let exp_named_subst',subst',metasenv',ugraph1 =
304 check_exp_named_subst subst metasenv context
305 exp_named_subst ugraph in
306 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
308 CicSubstitution.subst_vars exp_named_subst' ty_uri
310 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
311 | C.MutInd (uri,i,exp_named_subst) ->
312 let exp_named_subst',subst',metasenv',ugraph1 =
313 check_exp_named_subst subst metasenv context
314 exp_named_subst ugraph
316 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
318 CicSubstitution.subst_vars exp_named_subst' ty_uri in
319 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
320 | C.MutConstruct (uri,i,j,exp_named_subst) ->
321 let exp_named_subst',subst',metasenv',ugraph1 =
322 check_exp_named_subst subst metasenv context
323 exp_named_subst ugraph
326 type_of_mutual_inductive_constr uri i j ugraph1
329 CicSubstitution.subst_vars exp_named_subst' ty_uri
331 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
333 | C.MutCase (uri, i, outtype, term, pl) ->
334 (* first, get the inductive type (and noparams)
335 * in the environment *)
336 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
337 let _ = CicTypeChecker.typecheck uri in
338 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
340 C.InductiveDefinition (l,expl_params,parsno,_) ->
341 List.nth l i , expl_params, parsno, u
345 ("Unkown mutual inductive definition " ^
346 U.string_of_uri uri))
348 let rec count_prod t =
349 match CicReduction.whd ~subst context t with
350 C.Prod (_, _, t) -> 1 + (count_prod t)
353 let no_args = count_prod arity in
354 (* now, create a "generic" MutInd *)
355 let metasenv,left_args =
356 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
358 let metasenv,right_args =
359 let no_right_params = no_args - no_left_params in
360 if no_right_params < 0 then assert false
361 else CicMkImplicit.n_fresh_metas
362 metasenv subst context no_right_params
364 let metasenv,exp_named_subst =
365 CicMkImplicit.fresh_subst metasenv subst context expl_params in
368 C.MutInd (uri,i,exp_named_subst)
371 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
373 (* check consistency with the actual type of term *)
374 let term',actual_type,subst,metasenv,ugraph1 =
375 type_of_aux subst metasenv context term ugraph in
376 let expected_type',_, subst, metasenv,ugraph2 =
377 type_of_aux subst metasenv context expected_type ugraph1
379 let actual_type = CicReduction.whd ~subst context actual_type in
380 let subst,metasenv,ugraph3 =
381 fo_unif_subst subst context metasenv
382 expected_type' actual_type ugraph2
384 let rec instantiate_prod t =
388 match CicReduction.whd ~subst context t with
390 instantiate_prod (CicSubstitution.subst he t') tl
393 let arity_instantiated_with_left_args =
394 instantiate_prod arity left_args in
395 (* TODO: check if the sort elimination
396 * is allowed: [(I q1 ... qr)|B] *)
397 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
399 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
401 if left_args = [] then
402 (C.MutConstruct (uri,i,j,exp_named_subst))
405 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
407 let p',actual_type,subst,metasenv,ugraph1 =
408 type_of_aux subst metasenv context p ugraph
410 let constructor',expected_type, subst, metasenv,ugraph2 =
411 type_of_aux subst metasenv context constructor ugraph1
413 let outtypeinstance,subst,metasenv,ugraph3 =
414 check_branch 0 context metasenv subst no_left_params
415 actual_type constructor' expected_type ugraph2
418 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
419 ([],1,[],subst,metasenv,ugraph3) pl
422 (* we are left to check that the outype matches his instances.
423 The easy case is when the outype is specified, that amount
424 to a trivial check. Otherwise, we should guess a type from
430 (let candidate,ugraph5,metasenv,subst =
431 let exp_name_subst, metasenv =
433 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
435 let uris = CicUtil.params_of_obj o in
437 fun uri (acc,metasenv) ->
438 let metasenv',new_meta =
439 CicMkImplicit.mk_implicit metasenv subst context
442 CicMkImplicit.identity_relocation_list_for_metavariable
445 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
449 match left_args,right_args with
450 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
452 let rec mk_right_args =
455 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
457 let right_args_no = List.length right_args in
458 let lifted_left_args =
459 List.map (CicSubstitution.lift right_args_no) left_args
461 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
462 (lifted_left_args @ mk_right_args right_args_no))
465 FreshNamesGenerator.mk_fresh_name ~subst metasenv
466 context Cic.Anonymous ~typ:ty
468 match outtypeinstances with
470 let extended_context =
471 let rec add_right_args =
473 Cic.Prod (name,ty,t) ->
474 Some (name,Cic.Decl ty)::(add_right_args t)
477 (Some (fresh_name,Cic.Decl ty))::
479 (add_right_args arity_instantiated_with_left_args))@
482 let metasenv,new_meta =
483 CicMkImplicit.mk_implicit metasenv subst extended_context
486 CicMkImplicit.identity_relocation_list_for_metavariable
489 let rec add_lambdas b =
491 Cic.Prod (name,ty,t) ->
492 Cic.Lambda (name,ty,(add_lambdas b t))
493 | _ -> Cic.Lambda (fresh_name, ty, b)
496 add_lambdas (Cic.Meta (new_meta,irl))
497 arity_instantiated_with_left_args
499 (Some candidate),ugraph4,metasenv,subst
500 | (constructor_args_no,_,instance,_)::tl ->
502 let instance',subst,metasenv =
503 CicMetaSubst.delift_rels subst metasenv
504 constructor_args_no instance
506 let candidate,ugraph,metasenv,subst =
508 fun (candidate_oty,ugraph,metasenv,subst)
509 (constructor_args_no,_,instance,_) ->
510 match candidate_oty with
511 | None -> None,ugraph,metasenv,subst
514 let instance',subst,metasenv =
515 CicMetaSubst.delift_rels subst metasenv
516 constructor_args_no instance
518 let subst,metasenv,ugraph =
519 fo_unif_subst subst context metasenv
522 candidate_oty,ugraph,metasenv,subst
524 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
525 | CicUnification.UnificationFailure _
526 | CicUnification.Uncertain _ ->
527 None,ugraph,metasenv,subst
528 ) (Some instance',ugraph4,metasenv,subst) tl
531 | None -> None, ugraph,metasenv,subst
533 let rec add_lambdas n b =
535 Cic.Prod (name,ty,t) ->
536 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
538 Cic.Lambda (fresh_name, ty,
539 CicSubstitution.lift (n + 1) t)
542 (add_lambdas 0 t arity_instantiated_with_left_args),
543 ugraph,metasenv,subst
544 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
545 None,ugraph4,metasenv,subst
548 | None -> raise (Uncertain "can't solve an higher order unification problem")
550 let subst,metasenv,ugraph =
551 fo_unif_subst subst context metasenv
552 candidate outtype ugraph5
554 C.MutCase (uri, i, outtype, term', pl'),
555 CicReduction.head_beta_reduce
556 (CicMetaSubst.apply_subst subst
557 (Cic.Appl (outtype::right_args@[term']))),
558 subst,metasenv,ugraph)
559 | _ -> (* easy case *)
560 let _,_, subst, metasenv,ugraph5 =
561 type_of_aux subst metasenv context
562 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
564 let (subst,metasenv,ugraph6) =
566 (fun (subst,metasenv,ugraph)
567 (constructor_args_no,context,instance,args) ->
571 CicSubstitution.lift constructor_args_no outtype
573 C.Appl (outtype'::args)
575 CicReduction.whd ~subst context appl
577 fo_unif_subst subst context metasenv
578 instance instance' ugraph)
579 (subst,metasenv,ugraph5) outtypeinstances
581 C.MutCase (uri, i, outtype, term', pl'),
582 CicReduction.head_beta_reduce
583 (CicMetaSubst.apply_subst subst
584 (C.Appl(outtype::right_args@[term]))),
585 subst,metasenv,ugraph6)
587 let fl_ty',subst,metasenv,types,ugraph1 =
589 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
590 let ty',_,subst',metasenv',ugraph1 =
591 type_of_aux subst metasenv context ty ugraph
593 fl @ [ty'],subst',metasenv',
594 Some (C.Name n,(C.Decl ty')) :: types, ugraph
595 ) ([],subst,metasenv,[],ugraph) fl
597 let len = List.length types in
598 let context' = types@context in
599 let fl_bo',subst,metasenv,ugraph2 =
601 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
602 let bo',ty_of_bo,subst,metasenv,ugraph1 =
603 type_of_aux subst metasenv context' bo ugraph
605 let subst',metasenv',ugraph' =
606 fo_unif_subst subst context' metasenv
607 ty_of_bo (CicSubstitution.lift len ty) ugraph1
609 fl @ [bo'] , subst',metasenv',ugraph'
610 ) ([],subst,metasenv,ugraph1) fl
612 let (_,_,ty,_) = List.nth fl i in
613 (* now we have the new ty in fl_ty', the new bo in fl_bo',
614 * and we want the new fl with bo' and ty' injected in the right
617 let rec map3 f l1 l2 l3 =
620 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
623 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
626 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
628 let fl_ty',subst,metasenv,types,ugraph1 =
630 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
631 let ty',_,subst',metasenv',ugraph1 =
632 type_of_aux subst metasenv context ty ugraph
634 fl @ [ty'],subst',metasenv',
635 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
636 ) ([],subst,metasenv,[],ugraph) fl
638 let len = List.length types in
639 let context' = types@context in
640 let fl_bo',subst,metasenv,ugraph2 =
642 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
643 let bo',ty_of_bo,subst,metasenv,ugraph1 =
644 type_of_aux subst metasenv context' bo ugraph
646 let subst',metasenv',ugraph' =
647 fo_unif_subst subst context' metasenv
648 ty_of_bo (CicSubstitution.lift len ty) ugraph1
650 fl @ [bo'],subst',metasenv',ugraph'
651 ) ([],subst,metasenv,ugraph1) fl
653 let (_,ty,_) = List.nth fl i in
654 (* now we have the new ty in fl_ty', the new bo in fl_bo',
655 * and we want the new fl with bo' and ty' injected in the right
658 let rec map3 f l1 l2 l3 =
661 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
664 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
667 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
669 (* check_metasenv_consistency checks that the "canonical" context of a
670 metavariable is consitent - up to relocation via the relocation list l -
671 with the actual context *)
672 and check_metasenv_consistency
673 metano subst metasenv context canonical_context l ugraph
675 let module C = Cic in
676 let module R = CicReduction in
677 let module S = CicSubstitution in
678 let lifted_canonical_context =
682 | (Some (n,C.Decl t))::tl ->
683 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
684 | (Some (n,C.Def (t,None)))::tl ->
685 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
686 | None::tl -> None::(aux (i+1) tl)
687 | (Some (n,C.Def (t,Some ty)))::tl ->
689 C.Def ((S.subst_meta l (S.lift i t)),
690 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
692 aux 1 canonical_context
696 (fun (l,subst,metasenv,ugraph) t ct ->
699 l @ [None],subst,metasenv,ugraph
700 | Some t,Some (_,C.Def (ct,_)) ->
701 let subst',metasenv',ugraph' =
703 fo_unif_subst subst context metasenv t ct ugraph
704 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)))))
706 l @ [Some t],subst',metasenv',ugraph'
707 | Some t,Some (_,C.Decl ct) ->
708 let t',inferredty,subst',metasenv',ugraph1 =
709 type_of_aux subst metasenv context t ugraph
711 let subst'',metasenv'',ugraph2 =
714 subst' context metasenv' inferredty ct ugraph1
715 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)))))
717 l @ [Some t'], subst'',metasenv'',ugraph2
719 raise (RefineFailure (sprintf
720 "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"
721 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
722 (CicMetaSubst.ppcontext subst canonical_context)))
723 ) ([],subst,metasenv,ugraph) l lifted_canonical_context
725 Invalid_argument _ ->
729 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
730 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
731 (CicMetaSubst.ppcontext subst canonical_context)))
733 and check_exp_named_subst metasubst metasenv context tl ugraph =
734 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
736 [] -> [],metasubst,metasenv,ugraph
737 | ((uri,t) as subst)::tl ->
738 let ty_uri,ugraph1 = type_of_variable uri ugraph in
740 CicSubstitution.subst_vars substs ty_uri in
741 (* CSC: why was this code here? it is wrong
742 (match CicEnvironment.get_cooked_obj ~trust:false uri with
743 Cic.Variable (_,Some bo,_,_) ->
746 "A variable with a body can not be explicit substituted")
747 | Cic.Variable (_,None,_,_) -> ()
751 ("Unkown variable definition " ^ UriManager.string_of_uri uri))
754 let t',typeoft,metasubst',metasenv',ugraph2 =
755 type_of_aux metasubst metasenv context t ugraph1
757 let metasubst'',metasenv'',ugraph3 =
760 metasubst' context metasenv' typeoft typeofvar ugraph2
763 ("Wrong Explicit Named Substitution: " ^
764 CicMetaSubst.ppterm metasubst' typeoft ^
765 " not unifiable with " ^
766 CicMetaSubst.ppterm metasubst' typeofvar))
768 (* FIXME: no mere tail recursive! *)
769 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
770 check_exp_named_subst_aux
771 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
773 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
775 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
778 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
779 let module C = Cic in
780 let context_for_t2 = (Some (name,C.Decl s))::context in
781 let t1'' = CicReduction.whd ~subst context t1 in
782 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
783 match (t1'', t2'') with
784 (C.Sort s1, C.Sort s2)
785 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
786 C.Sort s2,subst,metasenv,ugraph
787 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
788 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
789 let t' = CicUniv.fresh() in
790 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
791 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
792 C.Sort (C.Type t'),subst,metasenv,ugraph2
793 | (C.Sort _,C.Sort (C.Type t1)) ->
794 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
795 C.Sort (C.Type t1),subst,metasenv,ugraph
796 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
797 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
798 (* TODO how can we force the meta to become a sort? If we don't we
799 * brake the invariant that refine produce only well typed terms *)
800 (* TODO if we check the non meta term and if it is a sort then we are
801 * likely to know the exact value of the result e.g. if the rhs is a
802 * Sort (Prop | Set | CProp) then the result is the rhs *)
804 CicMkImplicit.mk_implicit_sort metasenv subst in
805 let (subst, metasenv,ugraph1) =
806 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
808 t2'',subst,metasenv,ugraph1
810 raise (RefineFailure (sprintf
811 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
812 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
813 (CicPp.ppterm t2'')))
815 and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
816 let rec mk_prod metasenv context =
819 let (metasenv, idx) =
820 CicMkImplicit.mk_implicit_type metasenv subst context
823 CicMkImplicit.identity_relocation_list_for_metavariable context
825 metasenv,Cic.Meta (idx, irl)
827 let (metasenv, idx) =
828 CicMkImplicit.mk_implicit_type metasenv subst context
831 CicMkImplicit.identity_relocation_list_for_metavariable context
833 let meta = Cic.Meta (idx,irl) in
835 (* The name must be fresh for context. *)
836 (* Nevertheless, argty is well-typed only in context. *)
837 (* Thus I generate a name (name_hint) in context and *)
838 (* then I generate a name --- using the hint name_hint *)
839 (* --- that is fresh in (context'@context). *)
841 (* Cic.Name "pippo" *)
842 FreshNamesGenerator.mk_fresh_name ~subst metasenv
843 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
844 (CicMetaSubst.apply_subst_context subst context)
846 ~typ:(CicMetaSubst.apply_subst subst argty)
848 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
849 FreshNamesGenerator.mk_fresh_name ~subst
850 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
852 let metasenv,target =
853 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
855 metasenv,Cic.Prod (name,meta,target)
857 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
858 let (subst, metasenv,ugraph1) =
860 fo_unif_subst subst context metasenv hetype hetype' ugraph
862 debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
863 (CicPp.ppterm hetype)
864 (CicPp.ppterm hetype')
865 (CicMetaSubst.ppmetasenv metasenv [])
866 (CicMetaSubst.ppsubst subst));
870 let rec eat_prods metasenv subst context hetype ugraph =
872 | [] -> [],metasenv,subst,hetype,ugraph
873 | (hete, hety)::tl ->
876 let arg,subst,metasenv,ugraph1 =
878 let subst,metasenv,ugraph1 =
879 fo_unif_subst subst context metasenv hety s ugraph
881 hete,subst,metasenv,ugraph1
883 (* we search a coercion from hety to s *)
884 let coer = CoercGraph.look_for_coercion
885 (CicMetaSubst.apply_subst subst hety)
886 (CicMetaSubst.apply_subst subst s)
891 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
893 let coerced_args,metasenv',subst',t',ugraph2 =
894 eat_prods metasenv subst context
895 (* (CicMetaSubst.subst subst hete t) tl *)
896 (CicSubstitution.subst hete t) ugraph1 tl
898 arg::coerced_args,metasenv',subst',t',ugraph2
902 let coerced_args,metasenv,subst,t,ugraph2 =
903 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
905 coerced_args,t,subst,metasenv,ugraph2
908 (* eat prods ends here! *)
910 let t',ty,subst',metasenv',ugraph1 =
911 type_of_aux [] metasenv context t ugraph
913 let substituted_t = CicMetaSubst.apply_subst subst' t' in
914 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
915 (* Andrea: ho rimesso qui l'applicazione della subst al
916 metasenv dopo che ho droppato l'invariante che il metsaenv
917 e' sempre istanziato *)
918 let substituted_metasenv =
919 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
921 (* substituted_t,substituted_ty,substituted_metasenv *)
922 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
924 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
926 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
927 let cleaned_metasenv =
929 (function (n,context,ty) ->
930 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
935 | Some (n, Cic.Decl t) ->
937 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
938 | Some (n, Cic.Def (bo,ty)) ->
939 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
944 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
946 Some (n, Cic.Def (bo',ty'))
950 ) substituted_metasenv
952 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
955 let type_of_aux' metasenv context term ugraph =
957 type_of_aux' metasenv context term ugraph
959 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
961 (*CSC: this is a very very rough approximation; to be finished *)
962 let are_all_occurrences_positive uri =
964 (*CSC: here we should do a whd; but can we do that? *)
966 Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
967 | Cic.MutInd (uri',_,_) when uri = uri' -> ()
968 | Cic.Prod (_,_,t) -> aux t
969 | _ -> raise (RefineFailure "not well formed constructor type")
973 let typecheck metasenv uri obj =
974 let ugraph = CicUniv.empty_ugraph in
976 Cic.Constant (name,Some bo,ty,args,attrs) ->
977 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
978 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
979 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
980 let bo' = CicMetaSubst.apply_subst subst bo' in
981 let ty' = CicMetaSubst.apply_subst subst ty' in
982 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
983 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
984 | Cic.Constant (name,None,ty,args,attrs) ->
985 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
986 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
987 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
988 assert (metasenv' = metasenv);
989 (* Here we do not check the metasenv for correctness *)
990 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
991 let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
995 (* instead of raising Uncertain, let's hope that the meta will become
998 | _ -> raise (RefineFailure "The term provided is not a type")
1000 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1001 let bo' = CicMetaSubst.apply_subst subst bo' in
1002 let ty' = CicMetaSubst.apply_subst subst ty' in
1003 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1004 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1005 | Cic.Variable _ -> assert false (* not implemented *)
1006 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1007 (*CSC: this code is greately simplified and many many checks are missing *)
1008 (*CSC: e.g. the constructors are not required to build their own types, *)
1009 (*CSC: the arities are not required to have as type a sort, etc. *)
1010 let uri = match uri with Some uri -> uri | None -> assert false in
1011 let typesno = List.length tys in
1012 (* first phase: we fix only the types *)
1013 let metasenv,ugraph,tys =
1015 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1016 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1017 metasenv,ugraph,(name,b,ty',cl)::res
1018 ) tys (metasenv,ugraph,[]) in
1020 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1021 (* second phase: we fix only the constructors *)
1022 let metasenv,ugraph,tys =
1024 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1025 let metasenv,ugraph,cl' =
1027 (fun (name,ty) (metasenv,ugraph,res) ->
1028 let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1029 let ty',_,metasenv,ugraph =
1030 type_of_aux' metasenv con_context ty ugraph in
1034 (fun (name,_,_,_) (i,t) ->
1035 (* here the explicit_named_substituion is assumed to be *)
1037 let t' = Cic.MutInd (uri,i,[]) in
1038 let t = CicSubstitution.subst t' t in
1040 ) tys (typesno - 1,t)) in
1041 let ty' = undebrujin ty' in
1042 metasenv,ugraph,(name,ty')::res
1043 ) cl (metasenv,ugraph,[])
1045 metasenv,ugraph,(name,b,ty,cl')::res
1046 ) tys (metasenv,ugraph,[]) in
1047 (* third phase: we check the positivity condition *)
1050 List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
1052 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1055 let type_of_aux' metasenv context term =
1058 type_of_aux' metasenv context term in
1060 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
1062 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
1065 | RefineFailure msg as e ->
1066 debug_print ("@@@ REFINE FAILED: " ^ msg);
1068 | Uncertain msg as e ->
1069 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);