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 let _,ty,subst,metasenv,ugraph =
178 type_of_aux subst metasenv context (S.lift n bo) ugraph
180 t,ty,subst,metasenv,ugraph
181 | None -> raise (RefineFailure "Rel to hidden hypothesis")
183 _ -> raise (RefineFailure "Not a close term")
185 | C.Var (uri,exp_named_subst) ->
186 let exp_named_subst',subst',metasenv',ugraph1 =
187 check_exp_named_subst
188 subst metasenv context exp_named_subst ugraph
190 let ty_uri,ugraph1 = type_of_variable uri ugraph in
192 CicSubstitution.subst_vars exp_named_subst' ty_uri
194 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
197 let (canonical_context, term,ty) =
198 CicUtil.lookup_subst n subst
200 let l',subst',metasenv',ugraph1 =
201 check_metasenv_consistency n subst metasenv context
202 canonical_context l ugraph
204 (* trust or check ??? *)
205 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
206 subst', metasenv', ugraph1
207 (* type_of_aux subst metasenv
208 context (CicSubstitution.subst_meta l term) *)
209 with CicUtil.Subst_not_found _ ->
210 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
211 let l',subst',metasenv', ugraph1 =
212 check_metasenv_consistency n subst metasenv context
213 canonical_context l ugraph
215 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
216 subst', metasenv',ugraph1)
217 | C.Sort (C.Type tno) ->
218 let tno' = CicUniv.fresh() in
219 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
220 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
222 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
223 | C.Implicit _ -> raise (AssertFailure "21")
225 let ty',_,subst',metasenv',ugraph1 =
226 type_of_aux subst metasenv context ty ugraph
228 let te',inferredty,subst'',metasenv'',ugraph2 =
229 type_of_aux subst' metasenv' context te ugraph1
232 let subst''',metasenv''',ugraph3 =
233 fo_unif_subst subst'' context metasenv''
234 inferredty ty ugraph2
236 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
238 _ -> raise (RefineFailure "Cast"))
239 | C.Prod (name,s,t) ->
240 let s',sort1,subst',metasenv',ugraph1 =
241 type_of_aux subst metasenv context s ugraph
243 let t',sort2,subst'',metasenv'',ugraph2 =
244 type_of_aux subst' metasenv'
245 ((Some (name,(C.Decl s')))::context) t ugraph1
247 let sop,subst''',metasenv''',ugraph3 =
248 sort_of_prod subst'' metasenv''
249 context (name,s') (sort1,sort2) ugraph2
251 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
252 | C.Lambda (n,s,t) ->
253 let s',sort1,subst',metasenv',ugraph1 =
254 type_of_aux subst metasenv context s ugraph
256 (match CicReduction.whd ~subst:subst' context sort1 with
260 raise (RefineFailure (sprintf
261 "Not well-typed lambda-abstraction: the source %s should be a type;
262 instead it is a term of type %s" (CicPp.ppterm s)
263 (CicPp.ppterm sort1)))
265 let t',type2,subst'',metasenv'',ugraph2 =
266 type_of_aux subst' metasenv'
267 ((Some (n,(C.Decl s')))::context) t ugraph1
269 C.Lambda (n,s',t'),C.Prod (n,s',type2),
270 subst'',metasenv'',ugraph2
272 (* only to check if s is well-typed *)
273 let s',ty,subst',metasenv',ugraph1 =
274 type_of_aux subst metasenv context s ugraph
276 let t',inferredty,subst'',metasenv'',ugraph2 =
277 type_of_aux subst' metasenv'
278 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
280 (* One-step LetIn reduction.
281 * Even faster than the previous solution.
282 * Moreover the inferred type is closer to the expected one.
284 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
285 subst'',metasenv'',ugraph2
286 | C.Appl (he::((_::_) as tl)) ->
287 let he',hetype,subst',metasenv',ugraph1 =
288 type_of_aux subst metasenv context he ugraph
290 let tlbody_and_type,subst'',metasenv'',ugraph2 =
292 (fun x (res,subst,metasenv,ugraph) ->
293 let x',ty,subst',metasenv',ugraph1 =
294 type_of_aux subst metasenv context x ugraph
296 (x', ty)::res,subst',metasenv',ugraph1
297 ) tl ([],subst',metasenv',ugraph1)
299 let tl',applty,subst''',metasenv''',ugraph3 =
300 eat_prods subst'' metasenv'' context
301 hetype tlbody_and_type ugraph2
303 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
304 | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
305 | C.Const (uri,exp_named_subst) ->
306 let exp_named_subst',subst',metasenv',ugraph1 =
307 check_exp_named_subst subst metasenv context
308 exp_named_subst ugraph in
309 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
311 CicSubstitution.subst_vars exp_named_subst' ty_uri
313 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
314 | C.MutInd (uri,i,exp_named_subst) ->
315 let exp_named_subst',subst',metasenv',ugraph1 =
316 check_exp_named_subst subst metasenv context
317 exp_named_subst ugraph
319 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
321 CicSubstitution.subst_vars exp_named_subst' ty_uri in
322 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
323 | C.MutConstruct (uri,i,j,exp_named_subst) ->
324 let exp_named_subst',subst',metasenv',ugraph1 =
325 check_exp_named_subst subst metasenv context
326 exp_named_subst ugraph
329 type_of_mutual_inductive_constr uri i j ugraph1
332 CicSubstitution.subst_vars exp_named_subst' ty_uri
334 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
336 | C.MutCase (uri, i, outtype, term, pl) ->
337 (* first, get the inductive type (and noparams)
338 * in the environment *)
339 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
340 let _ = CicTypeChecker.typecheck uri in
341 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
343 C.InductiveDefinition (l,expl_params,parsno,_) ->
344 List.nth l i , expl_params, parsno, u
348 ("Unkown mutual inductive definition " ^
349 U.string_of_uri uri))
351 let rec count_prod t =
352 match CicReduction.whd ~subst context t with
353 C.Prod (_, _, t) -> 1 + (count_prod t)
356 let no_args = count_prod arity in
357 (* now, create a "generic" MutInd *)
358 let metasenv,left_args =
359 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
361 let metasenv,right_args =
362 let no_right_params = no_args - no_left_params in
363 if no_right_params < 0 then assert false
364 else CicMkImplicit.n_fresh_metas
365 metasenv subst context no_right_params
367 let metasenv,exp_named_subst =
368 CicMkImplicit.fresh_subst metasenv subst context expl_params in
371 C.MutInd (uri,i,exp_named_subst)
374 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
376 (* check consistency with the actual type of term *)
377 let term',actual_type,subst,metasenv,ugraph1 =
378 type_of_aux subst metasenv context term ugraph in
379 let expected_type',_, subst, metasenv,ugraph2 =
380 type_of_aux subst metasenv context expected_type ugraph1
382 let actual_type = CicReduction.whd ~subst context actual_type in
383 let subst,metasenv,ugraph3 =
384 fo_unif_subst subst context metasenv
385 expected_type' actual_type ugraph2
387 let rec instantiate_prod t =
391 match CicReduction.whd ~subst context t with
393 instantiate_prod (CicSubstitution.subst he t') tl
396 let arity_instantiated_with_left_args =
397 instantiate_prod arity left_args in
398 (* TODO: check if the sort elimination
399 * is allowed: [(I q1 ... qr)|B] *)
400 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
402 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
404 if left_args = [] then
405 (C.MutConstruct (uri,i,j,exp_named_subst))
408 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
410 let p',actual_type,subst,metasenv,ugraph1 =
411 type_of_aux subst metasenv context p ugraph
413 let constructor',expected_type, subst, metasenv,ugraph2 =
414 type_of_aux subst metasenv context constructor ugraph1
416 let outtypeinstance,subst,metasenv,ugraph3 =
417 check_branch 0 context metasenv subst no_left_params
418 actual_type constructor' expected_type ugraph2
421 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
422 ([],1,[],subst,metasenv,ugraph3) pl
425 (* we are left to check that the outype matches his instances.
426 The easy case is when the outype is specified, that amount
427 to a trivial check. Otherwise, we should guess a type from
433 (let candidate,ugraph5,metasenv,subst =
434 let exp_name_subst, metasenv =
436 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
438 let uris = CicUtil.params_of_obj o in
440 fun uri (acc,metasenv) ->
441 let metasenv',new_meta =
442 CicMkImplicit.mk_implicit metasenv subst context
445 CicMkImplicit.identity_relocation_list_for_metavariable
448 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
452 match left_args,right_args with
453 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
455 let rec mk_right_args =
458 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
460 let right_args_no = List.length right_args in
461 let lifted_left_args =
462 List.map (CicSubstitution.lift right_args_no) left_args
464 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
465 (lifted_left_args @ mk_right_args right_args_no))
468 FreshNamesGenerator.mk_fresh_name ~subst metasenv
469 context Cic.Anonymous ~typ:ty
471 match outtypeinstances with
473 let extended_context =
474 let rec add_right_args =
476 Cic.Prod (name,ty,t) ->
477 Some (name,Cic.Decl ty)::(add_right_args t)
480 (Some (fresh_name,Cic.Decl ty))::
482 (add_right_args arity_instantiated_with_left_args))@
485 let metasenv,new_meta =
486 CicMkImplicit.mk_implicit metasenv subst extended_context
489 CicMkImplicit.identity_relocation_list_for_metavariable
492 let rec add_lambdas b =
494 Cic.Prod (name,ty,t) ->
495 Cic.Lambda (name,ty,(add_lambdas b t))
496 | _ -> Cic.Lambda (fresh_name, ty, b)
499 add_lambdas (Cic.Meta (new_meta,irl))
500 arity_instantiated_with_left_args
502 (Some candidate),ugraph4,metasenv,subst
503 | (constructor_args_no,_,instance,_)::tl ->
505 let instance',subst,metasenv =
506 CicMetaSubst.delift_rels subst metasenv
507 constructor_args_no instance
509 let candidate,ugraph,metasenv,subst =
511 fun (candidate_oty,ugraph,metasenv,subst)
512 (constructor_args_no,_,instance,_) ->
513 match candidate_oty with
514 | None -> None,ugraph,metasenv,subst
517 let instance',subst,metasenv =
518 CicMetaSubst.delift_rels subst metasenv
519 constructor_args_no instance
521 let subst,metasenv,ugraph =
522 fo_unif_subst subst context metasenv
525 candidate_oty,ugraph,metasenv,subst
527 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
528 | CicUnification.UnificationFailure _
529 | CicUnification.Uncertain _ ->
530 None,ugraph,metasenv,subst
531 ) (Some instance',ugraph4,metasenv,subst) tl
534 | None -> None, ugraph,metasenv,subst
536 let rec add_lambdas n b =
538 Cic.Prod (name,ty,t) ->
539 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
541 Cic.Lambda (fresh_name, ty,
542 CicSubstitution.lift (n + 1) t)
545 (add_lambdas 0 t arity_instantiated_with_left_args),
546 ugraph,metasenv,subst
547 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
548 None,ugraph4,metasenv,subst
551 | None -> raise (Uncertain "can't solve an higher order unification problem")
553 let subst,metasenv,ugraph =
554 fo_unif_subst subst context metasenv
555 candidate outtype ugraph5
557 C.MutCase (uri, i, outtype, term', pl'),
558 CicReduction.head_beta_reduce
559 (CicMetaSubst.apply_subst subst
560 (Cic.Appl (outtype::right_args@[term']))),
561 subst,metasenv,ugraph)
562 | _ -> (* easy case *)
563 let _,_, subst, metasenv,ugraph5 =
564 type_of_aux subst metasenv context
565 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
567 let (subst,metasenv,ugraph6) =
569 (fun (subst,metasenv,ugraph)
570 (constructor_args_no,context,instance,args) ->
574 CicSubstitution.lift constructor_args_no outtype
576 C.Appl (outtype'::args)
578 CicReduction.whd ~subst context appl
580 fo_unif_subst subst context metasenv
581 instance instance' ugraph)
582 (subst,metasenv,ugraph5) outtypeinstances
584 C.MutCase (uri, i, outtype, term', pl'),
585 CicReduction.head_beta_reduce
586 (CicMetaSubst.apply_subst subst
587 (C.Appl(outtype::right_args@[term]))),
588 subst,metasenv,ugraph6)
590 let fl_ty',subst,metasenv,types,ugraph1 =
592 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
593 let ty',_,subst',metasenv',ugraph1 =
594 type_of_aux subst metasenv context ty ugraph
596 fl @ [ty'],subst',metasenv',
597 Some (C.Name n,(C.Decl ty')) :: types, ugraph
598 ) ([],subst,metasenv,[],ugraph) fl
600 let len = List.length types in
601 let context' = types@context in
602 let fl_bo',subst,metasenv,ugraph2 =
604 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
605 let bo',ty_of_bo,subst,metasenv,ugraph1 =
606 type_of_aux subst metasenv context' bo ugraph
608 let subst',metasenv',ugraph' =
609 fo_unif_subst subst context' metasenv
610 ty_of_bo (CicSubstitution.lift len ty) ugraph1
612 fl @ [bo'] , subst',metasenv',ugraph'
613 ) ([],subst,metasenv,ugraph1) fl
615 let (_,_,ty,_) = List.nth fl i in
616 (* now we have the new ty in fl_ty', the new bo in fl_bo',
617 * and we want the new fl with bo' and ty' injected in the right
620 let rec map3 f l1 l2 l3 =
623 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
626 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
629 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
631 let fl_ty',subst,metasenv,types,ugraph1 =
633 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
634 let ty',_,subst',metasenv',ugraph1 =
635 type_of_aux subst metasenv context ty ugraph
637 fl @ [ty'],subst',metasenv',
638 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
639 ) ([],subst,metasenv,[],ugraph) fl
641 let len = List.length types in
642 let context' = types@context in
643 let fl_bo',subst,metasenv,ugraph2 =
645 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
646 let bo',ty_of_bo,subst,metasenv,ugraph1 =
647 type_of_aux subst metasenv context' bo ugraph
649 let subst',metasenv',ugraph' =
650 fo_unif_subst subst context' metasenv
651 ty_of_bo (CicSubstitution.lift len ty) ugraph1
653 fl @ [bo'],subst',metasenv',ugraph'
654 ) ([],subst,metasenv,ugraph1) fl
656 let (_,ty,_) = List.nth fl i in
657 (* now we have the new ty in fl_ty', the new bo in fl_bo',
658 * and we want the new fl with bo' and ty' injected in the right
661 let rec map3 f l1 l2 l3 =
664 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
667 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
670 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
672 (* check_metasenv_consistency checks that the "canonical" context of a
673 metavariable is consitent - up to relocation via the relocation list l -
674 with the actual context *)
675 and check_metasenv_consistency
676 metano subst metasenv context canonical_context l ugraph
678 let module C = Cic in
679 let module R = CicReduction in
680 let module S = CicSubstitution in
681 let lifted_canonical_context =
685 | (Some (n,C.Decl t))::tl ->
686 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
687 | (Some (n,C.Def (t,None)))::tl ->
688 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
689 | None::tl -> None::(aux (i+1) tl)
690 | (Some (n,C.Def (t,Some ty)))::tl ->
692 C.Def ((S.subst_meta l (S.lift i t)),
693 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
695 aux 1 canonical_context
699 (fun (l,subst,metasenv,ugraph) t ct ->
702 l @ [None],subst,metasenv,ugraph
703 | Some t,Some (_,C.Def (ct,_)) ->
704 let subst',metasenv',ugraph' =
706 fo_unif_subst subst context metasenv t ct ugraph
707 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)))))
709 l @ [Some t],subst',metasenv',ugraph'
710 | Some t,Some (_,C.Decl ct) ->
711 let t',inferredty,subst',metasenv',ugraph1 =
712 type_of_aux subst metasenv context t ugraph
714 let subst'',metasenv'',ugraph2 =
717 subst' context metasenv' inferredty ct ugraph1
718 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)))))
720 l @ [Some t'], subst'',metasenv'',ugraph2
722 raise (RefineFailure (sprintf
723 "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"
724 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
725 (CicMetaSubst.ppcontext subst canonical_context)))
726 ) ([],subst,metasenv,ugraph) l lifted_canonical_context
728 Invalid_argument _ ->
732 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
733 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
734 (CicMetaSubst.ppcontext subst canonical_context)))
736 and check_exp_named_subst metasubst metasenv context tl ugraph =
737 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
739 [] -> [],metasubst,metasenv,ugraph
740 | ((uri,t) as subst)::tl ->
741 let ty_uri,ugraph1 = type_of_variable uri ugraph in
743 CicSubstitution.subst_vars substs ty_uri in
744 (* CSC: why was this code here? it is wrong
745 (match CicEnvironment.get_cooked_obj ~trust:false uri with
746 Cic.Variable (_,Some bo,_,_) ->
749 "A variable with a body can not be explicit substituted")
750 | Cic.Variable (_,None,_,_) -> ()
754 ("Unkown variable definition " ^ UriManager.string_of_uri uri))
757 let t',typeoft,metasubst',metasenv',ugraph2 =
758 type_of_aux metasubst metasenv context t ugraph1
760 let metasubst'',metasenv'',ugraph3 =
763 metasubst' context metasenv' typeoft typeofvar ugraph2
766 ("Wrong Explicit Named Substitution: " ^
767 CicMetaSubst.ppterm metasubst' typeoft ^
768 " not unifiable with " ^
769 CicMetaSubst.ppterm metasubst' typeofvar))
771 (* FIXME: no mere tail recursive! *)
772 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
773 check_exp_named_subst_aux
774 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
776 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
778 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
781 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
782 let module C = Cic in
783 let context_for_t2 = (Some (name,C.Decl s))::context in
784 let t1'' = CicReduction.whd ~subst context t1 in
785 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
786 match (t1'', t2'') with
787 (C.Sort s1, C.Sort s2)
788 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
789 C.Sort s2,subst,metasenv,ugraph
790 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
791 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
792 let t' = CicUniv.fresh() in
793 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
794 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
795 C.Sort (C.Type t'),subst,metasenv,ugraph2
796 | (C.Sort _,C.Sort (C.Type t1)) ->
797 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
798 C.Sort (C.Type t1),subst,metasenv,ugraph
799 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
800 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
801 (* TODO how can we force the meta to become a sort? If we don't we
802 * brake the invariant that refine produce only well typed terms *)
803 (* TODO if we check the non meta term and if it is a sort then we are
804 * likely to know the exact value of the result e.g. if the rhs is a
805 * Sort (Prop | Set | CProp) then the result is the rhs *)
807 CicMkImplicit.mk_implicit_sort metasenv subst in
808 let (subst, metasenv,ugraph1) =
809 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
811 t2'',subst,metasenv,ugraph1
813 raise (RefineFailure (sprintf
814 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
815 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
816 (CicPp.ppterm t2'')))
818 and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
819 let rec mk_prod metasenv context =
822 let (metasenv, idx) =
823 CicMkImplicit.mk_implicit_type metasenv subst context
826 CicMkImplicit.identity_relocation_list_for_metavariable context
828 metasenv,Cic.Meta (idx, irl)
830 let (metasenv, idx) =
831 CicMkImplicit.mk_implicit_type metasenv subst context
834 CicMkImplicit.identity_relocation_list_for_metavariable context
836 let meta = Cic.Meta (idx,irl) in
838 (* The name must be fresh for context. *)
839 (* Nevertheless, argty is well-typed only in context. *)
840 (* Thus I generate a name (name_hint) in context and *)
841 (* then I generate a name --- using the hint name_hint *)
842 (* --- that is fresh in (context'@context). *)
844 (* Cic.Name "pippo" *)
845 FreshNamesGenerator.mk_fresh_name ~subst metasenv
846 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
847 (CicMetaSubst.apply_subst_context subst context)
849 ~typ:(CicMetaSubst.apply_subst subst argty)
851 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
852 FreshNamesGenerator.mk_fresh_name ~subst
853 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
855 let metasenv,target =
856 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
858 metasenv,Cic.Prod (name,meta,target)
860 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
861 let (subst, metasenv,ugraph1) =
863 fo_unif_subst subst context metasenv hetype hetype' ugraph
865 debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
866 (CicPp.ppterm hetype)
867 (CicPp.ppterm hetype')
868 (CicMetaSubst.ppmetasenv metasenv [])
869 (CicMetaSubst.ppsubst subst));
873 let rec eat_prods metasenv subst context hetype ugraph =
875 | [] -> [],metasenv,subst,hetype,ugraph
876 | (hete, hety)::tl ->
879 let arg,subst,metasenv,ugraph1 =
881 let subst,metasenv,ugraph1 =
882 fo_unif_subst subst context metasenv hety s ugraph
884 hete,subst,metasenv,ugraph1
886 (* we search a coercion from hety to s *)
887 let coer = CoercGraph.look_for_coercion
888 (CicMetaSubst.apply_subst subst hety)
889 (CicMetaSubst.apply_subst subst s)
894 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
896 let coerced_args,metasenv',subst',t',ugraph2 =
897 eat_prods metasenv subst context
898 (* (CicMetaSubst.subst subst hete t) tl *)
899 (CicSubstitution.subst hete t) ugraph1 tl
901 arg::coerced_args,metasenv',subst',t',ugraph2
905 let coerced_args,metasenv,subst,t,ugraph2 =
906 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
908 coerced_args,t,subst,metasenv,ugraph2
911 (* eat prods ends here! *)
913 let t',ty,subst',metasenv',ugraph1 =
914 type_of_aux [] metasenv context t ugraph
916 let substituted_t = CicMetaSubst.apply_subst subst' t' in
917 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
918 (* Andrea: ho rimesso qui l'applicazione della subst al
919 metasenv dopo che ho droppato l'invariante che il metsaenv
920 e' sempre istanziato *)
921 let substituted_metasenv =
922 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
924 (* substituted_t,substituted_ty,substituted_metasenv *)
925 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
927 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
929 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
930 let cleaned_metasenv =
932 (function (n,context,ty) ->
933 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
938 | Some (n, Cic.Decl t) ->
940 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
941 | Some (n, Cic.Def (bo,ty)) ->
942 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
947 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
949 Some (n, Cic.Def (bo',ty'))
953 ) substituted_metasenv
955 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
958 let type_of_aux' metasenv context term ugraph =
960 type_of_aux' metasenv context term ugraph
962 CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
964 (*CSC: this is a very very rough approximation; to be finished *)
965 let are_all_occurrences_positive uri =
967 (*CSC: here we should do a whd; but can we do that? *)
969 Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
970 | Cic.MutInd (uri',_,_) when uri = uri' -> ()
971 | Cic.Prod (_,_,t) -> aux t
972 | _ -> raise (RefineFailure "not well formed constructor type")
976 let typecheck metasenv uri obj =
977 let ugraph = CicUniv.empty_ugraph in
979 Cic.Constant (name,Some bo,ty,args,attrs) ->
980 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
981 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
982 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
983 let bo' = CicMetaSubst.apply_subst subst bo' in
984 let ty' = CicMetaSubst.apply_subst subst ty' in
985 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
986 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
987 | Cic.Constant (name,None,ty,args,attrs) ->
988 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
989 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
990 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
991 assert (metasenv' = metasenv);
992 (* Here we do not check the metasenv for correctness *)
993 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
994 let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
998 (* instead of raising Uncertain, let's hope that the meta will become
1001 | _ -> raise (RefineFailure "The term provided is not a type")
1003 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1004 let bo' = CicMetaSubst.apply_subst subst bo' in
1005 let ty' = CicMetaSubst.apply_subst subst ty' in
1006 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1007 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1008 | Cic.Variable _ -> assert false (* not implemented *)
1009 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1010 (*CSC: this code is greately simplified and many many checks are missing *)
1011 (*CSC: e.g. the constructors are not required to build their own types, *)
1012 (*CSC: the arities are not required to have as type a sort, etc. *)
1013 let uri = match uri with Some uri -> uri | None -> assert false in
1014 let typesno = List.length tys in
1015 (* first phase: we fix only the types *)
1016 let metasenv,ugraph,tys =
1018 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1019 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1020 metasenv,ugraph,(name,b,ty',cl)::res
1021 ) tys (metasenv,ugraph,[]) in
1023 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1024 (* second phase: we fix only the constructors *)
1025 let metasenv,ugraph,tys =
1027 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1028 let metasenv,ugraph,cl' =
1030 (fun (name,ty) (metasenv,ugraph,res) ->
1031 let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1032 let ty',_,metasenv,ugraph =
1033 type_of_aux' metasenv con_context ty ugraph in
1037 (fun (name,_,_,_) (i,t) ->
1038 (* here the explicit_named_substituion is assumed to be *)
1040 let t' = Cic.MutInd (uri,i,[]) in
1041 let t = CicSubstitution.subst t' t in
1043 ) tys (typesno - 1,t)) in
1044 let ty' = undebrujin ty' in
1045 metasenv,ugraph,(name,ty')::res
1046 ) cl (metasenv,ugraph,[])
1048 metasenv,ugraph,(name,b,ty,cl')::res
1049 ) tys (metasenv,ugraph,[]) in
1050 (* third phase: we check the positivity condition *)
1053 List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
1055 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1058 let type_of_aux' metasenv context term =
1061 type_of_aux' metasenv context term in
1063 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
1065 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
1068 | RefineFailure msg as e ->
1069 debug_print ("@@@ REFINE FAILED: " ^ msg);
1071 | Uncertain msg as e ->
1072 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);