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/.
30 | UnificationFailure of CicUnification.failure_msg
35 | UnificationFailure msg -> CicUnification.explain_error msg
37 exception RefineFailure of failure_msg;;
38 exception Uncertain of string;;
39 exception AssertFailure of string;;
41 let debug_print = fun _ -> ()
43 let profiler = HExtlib.profile "CicRefine.fo_unif"
45 let fo_unif_subst subst context metasenv t1 t2 ugraph =
48 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
49 in profiler.HExtlib.profile foo ()
51 (CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg))
52 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
58 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
59 | (_,_) -> raise (AssertFailure "split: list too short")
62 let rec type_of_constant uri ugraph =
64 let module R = CicReduction in
65 let module U = UriManager in
66 let _ = CicTypeChecker.typecheck uri in
69 CicEnvironment.get_cooked_obj ugraph uri
70 with Not_found -> assert false
73 C.Constant (_,_,ty,_,_) -> ty,u
74 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
77 (RefineFailure (Reason ("Unknown constant definition " ^ U.string_of_uri uri)))
79 and type_of_variable uri ugraph =
81 let module R = CicReduction in
82 let module U = UriManager in
83 let _ = CicTypeChecker.typecheck uri in
86 CicEnvironment.get_cooked_obj ugraph uri
87 with Not_found -> assert false
90 C.Variable (_,_,ty,_,_) -> ty,u
94 (Reason ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
96 and type_of_mutual_inductive_defs uri i ugraph =
98 let module R = CicReduction in
99 let module U = UriManager in
100 let _ = CicTypeChecker.typecheck uri in
103 CicEnvironment.get_cooked_obj ugraph uri
104 with Not_found -> assert false
107 C.InductiveDefinition (dl,_,_,_) ->
108 let (_,_,arity,_) = List.nth dl i in
113 (Reason ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
115 and type_of_mutual_inductive_constr uri i j ugraph =
116 let module C = Cic in
117 let module R = CicReduction in
118 let module U = UriManager in
119 let _ = CicTypeChecker.typecheck uri in
122 CicEnvironment.get_cooked_obj ugraph uri
123 with Not_found -> assert false
126 C.InductiveDefinition (dl,_,_,_) ->
127 let (_,_,_,cl) = List.nth dl i in
128 let (_,ty) = List.nth cl (j-1) in
133 (Reason ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
136 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
138 (* the check_branch function checks if a branch of a case is refinable.
139 It returns a pair (outype_instance,args), a subst and a metasenv.
140 outype_instance is the expected result of applying the case outtype
142 The problem is that outype is in general unknown, and we should
143 try to synthesize it from the above information, that is in general
144 a second order unification problem. *)
146 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
147 let module C = Cic in
148 (* let module R = CicMetaSubst in *)
149 let module R = CicReduction in
150 match R.whd ~subst context expectedtype with
152 (n,context,actualtype, [term]), subst, metasenv, ugraph
153 | C.Appl (C.MutInd (_,_,_)::tl) ->
154 let (_,arguments) = split tl left_args_no in
155 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
156 | C.Prod (name,so,de) ->
157 (* we expect that the actual type of the branch has the due
159 (match R.whd ~subst context actualtype with
160 C.Prod (name',so',de') ->
161 let subst, metasenv, ugraph1 =
162 fo_unif_subst subst context metasenv so so' ugraph in
164 (match CicSubstitution.lift 1 term with
165 C.Appl l -> C.Appl (l@[C.Rel 1])
166 | t -> C.Appl [t ; C.Rel 1]) in
167 (* we should also check that the name variable is anonymous in
168 the actual type de' ?? *)
170 ((Some (name,(C.Decl so)))::context)
171 metasenv subst left_args_no de' term' de ugraph1
172 | _ -> raise (AssertFailure "Wrong number of arguments"))
173 | _ -> raise (AssertFailure "Prod or MutInd expected")
175 and type_of_aux' metasenv context t ugraph =
176 let rec type_of_aux subst metasenv context t ugraph =
177 let module C = Cic in
178 let module S = CicSubstitution in
179 let module U = UriManager in
184 match List.nth context (n - 1) with
185 Some (_,C.Decl ty) ->
186 t,S.lift n ty,subst,metasenv, ugraph
187 | Some (_,C.Def (_,Some ty)) ->
188 t,S.lift n ty,subst,metasenv, ugraph
189 | Some (_,C.Def (bo,None)) ->
191 (* if it is in the context it must be already well-typed*)
192 CicTypeChecker.type_of_aux' ~subst metasenv context
195 t,ty,subst,metasenv,ugraph
196 | None -> raise (RefineFailure (Reason "Rel to hidden hypothesis"))
198 _ -> raise (RefineFailure (Reason "Not a close term"))
200 | C.Var (uri,exp_named_subst) ->
201 let exp_named_subst',subst',metasenv',ugraph1 =
202 check_exp_named_subst
203 subst metasenv context exp_named_subst ugraph
205 let ty_uri,ugraph1 = type_of_variable uri ugraph in
207 CicSubstitution.subst_vars exp_named_subst' ty_uri
209 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
212 let (canonical_context, term,ty) =
213 CicUtil.lookup_subst n subst
215 let l',subst',metasenv',ugraph1 =
216 check_metasenv_consistency n subst metasenv context
217 canonical_context l ugraph
219 (* trust or check ??? *)
220 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
221 subst', metasenv', ugraph1
222 (* type_of_aux subst metasenv
223 context (CicSubstitution.subst_meta l term) *)
224 with CicUtil.Subst_not_found _ ->
225 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
226 let l',subst',metasenv', ugraph1 =
227 check_metasenv_consistency n subst metasenv context
228 canonical_context l ugraph
230 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
231 subst', metasenv',ugraph1)
232 | C.Sort (C.Type tno) ->
233 let tno' = CicUniv.fresh() in
234 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
235 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
237 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
238 | C.Implicit _ -> raise (AssertFailure "21")
240 let ty',_,subst',metasenv',ugraph1 =
241 type_of_aux subst metasenv context ty ugraph
243 let te',inferredty,subst'',metasenv'',ugraph2 =
244 type_of_aux subst' metasenv' context te ugraph1
247 let subst''',metasenv''',ugraph3 =
248 fo_unif_subst subst'' context metasenv''
249 inferredty ty ugraph2
251 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
253 _ -> raise (RefineFailure (Reason "Cast")))
254 | C.Prod (name,s,t) ->
255 let s',sort1,subst',metasenv',ugraph1 =
256 type_of_aux subst metasenv context s ugraph
258 let t',sort2,subst'',metasenv'',ugraph2 =
259 type_of_aux subst' metasenv'
260 ((Some (name,(C.Decl s')))::context) t ugraph1
262 let sop,subst''',metasenv''',ugraph3 =
263 sort_of_prod subst'' metasenv''
264 context (name,s') (sort1,sort2) ugraph2
266 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
267 | C.Lambda (n,s,t) ->
268 let s',sort1,subst',metasenv',ugraph1 =
269 type_of_aux subst metasenv context s ugraph
271 (match CicReduction.whd ~subst:subst' context sort1 with
275 raise (RefineFailure (Reason (sprintf
276 "Not well-typed lambda-abstraction: the source %s should be a type;
277 instead it is a term of type %s" (CicPp.ppterm s)
278 (CicPp.ppterm sort1))))
280 let t',type2,subst'',metasenv'',ugraph2 =
281 type_of_aux subst' metasenv'
282 ((Some (n,(C.Decl s')))::context) t ugraph1
284 C.Lambda (n,s',t'),C.Prod (n,s',type2),
285 subst'',metasenv'',ugraph2
287 (* only to check if s is well-typed *)
288 let s',ty,subst',metasenv',ugraph1 =
289 type_of_aux subst metasenv context s ugraph
291 let t',inferredty,subst'',metasenv'',ugraph2 =
292 type_of_aux subst' metasenv'
293 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
295 (* One-step LetIn reduction.
296 * Even faster than the previous solution.
297 * Moreover the inferred type is closer to the expected one.
299 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
300 subst'',metasenv'',ugraph2
301 | C.Appl (he::((_::_) as tl)) ->
302 let he',hetype,subst',metasenv',ugraph1 =
303 type_of_aux subst metasenv context he ugraph
305 let tlbody_and_type,subst'',metasenv'',ugraph2 =
307 (fun x (res,subst,metasenv,ugraph) ->
308 let x',ty,subst',metasenv',ugraph1 =
309 type_of_aux subst metasenv context x ugraph
311 (x', ty)::res,subst',metasenv',ugraph1
312 ) tl ([],subst',metasenv',ugraph1)
314 let tl',applty,subst''',metasenv''',ugraph3 =
315 eat_prods subst'' metasenv'' context
316 hetype tlbody_and_type ugraph2
318 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
319 | C.Appl _ -> raise (RefineFailure (Reason "Appl: no arguments"))
320 | C.Const (uri,exp_named_subst) ->
321 let exp_named_subst',subst',metasenv',ugraph1 =
322 check_exp_named_subst subst metasenv context
323 exp_named_subst ugraph in
324 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
326 CicSubstitution.subst_vars exp_named_subst' ty_uri
328 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
329 | C.MutInd (uri,i,exp_named_subst) ->
330 let exp_named_subst',subst',metasenv',ugraph1 =
331 check_exp_named_subst subst metasenv context
332 exp_named_subst ugraph
334 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
336 CicSubstitution.subst_vars exp_named_subst' ty_uri in
337 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
338 | C.MutConstruct (uri,i,j,exp_named_subst) ->
339 let exp_named_subst',subst',metasenv',ugraph1 =
340 check_exp_named_subst subst metasenv context
341 exp_named_subst ugraph
344 type_of_mutual_inductive_constr uri i j ugraph1
347 CicSubstitution.subst_vars exp_named_subst' ty_uri
349 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
351 | C.MutCase (uri, i, outtype, term, pl) ->
352 (* first, get the inductive type (and noparams)
353 * in the environment *)
354 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
355 let _ = CicTypeChecker.typecheck uri in
356 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
358 C.InductiveDefinition (l,expl_params,parsno,_) ->
359 List.nth l i , expl_params, parsno, u
363 (Reason ("Unkown mutual inductive definition " ^
364 U.string_of_uri uri)))
366 let rec count_prod t =
367 match CicReduction.whd ~subst context t with
368 C.Prod (_, _, t) -> 1 + (count_prod t)
371 let no_args = count_prod arity in
372 (* now, create a "generic" MutInd *)
373 let metasenv,left_args =
374 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
376 let metasenv,right_args =
377 let no_right_params = no_args - no_left_params in
378 if no_right_params < 0 then assert false
379 else CicMkImplicit.n_fresh_metas
380 metasenv subst context no_right_params
382 let metasenv,exp_named_subst =
383 CicMkImplicit.fresh_subst metasenv subst context expl_params in
386 C.MutInd (uri,i,exp_named_subst)
389 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
391 (* check consistency with the actual type of term *)
392 let term',actual_type,subst,metasenv,ugraph1 =
393 type_of_aux subst metasenv context term ugraph in
394 let expected_type',_, subst, metasenv,ugraph2 =
395 type_of_aux subst metasenv context expected_type ugraph1
397 let actual_type = CicReduction.whd ~subst context actual_type in
398 let subst,metasenv,ugraph3 =
399 fo_unif_subst subst context metasenv
400 expected_type' actual_type ugraph2
402 let rec instantiate_prod t =
406 match CicReduction.whd ~subst context t with
408 instantiate_prod (CicSubstitution.subst he t') tl
411 let arity_instantiated_with_left_args =
412 instantiate_prod arity left_args in
413 (* TODO: check if the sort elimination
414 * is allowed: [(I q1 ... qr)|B] *)
415 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
417 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
419 if left_args = [] then
420 (C.MutConstruct (uri,i,j,exp_named_subst))
423 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
425 let p',actual_type,subst,metasenv,ugraph1 =
426 type_of_aux subst metasenv context p ugraph
428 let constructor',expected_type, subst, metasenv,ugraph2 =
429 type_of_aux subst metasenv context constructor ugraph1
431 let outtypeinstance,subst,metasenv,ugraph3 =
432 check_branch 0 context metasenv subst no_left_params
433 actual_type constructor' expected_type ugraph2
436 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
437 ([],1,[],subst,metasenv,ugraph3) pl
440 (* we are left to check that the outype matches his instances.
441 The easy case is when the outype is specified, that amount
442 to a trivial check. Otherwise, we should guess a type from
448 (let candidate,ugraph5,metasenv,subst =
449 let exp_name_subst, metasenv =
451 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
453 let uris = CicUtil.params_of_obj o in
455 fun uri (acc,metasenv) ->
456 let metasenv',new_meta =
457 CicMkImplicit.mk_implicit metasenv subst context
460 CicMkImplicit.identity_relocation_list_for_metavariable
463 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
467 match left_args,right_args with
468 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
470 let rec mk_right_args =
473 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
475 let right_args_no = List.length right_args in
476 let lifted_left_args =
477 List.map (CicSubstitution.lift right_args_no) left_args
479 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
480 (lifted_left_args @ mk_right_args right_args_no))
483 FreshNamesGenerator.mk_fresh_name ~subst metasenv
484 context Cic.Anonymous ~typ:ty
486 match outtypeinstances with
488 let extended_context =
489 let rec add_right_args =
491 Cic.Prod (name,ty,t) ->
492 Some (name,Cic.Decl ty)::(add_right_args t)
495 (Some (fresh_name,Cic.Decl ty))::
497 (add_right_args arity_instantiated_with_left_args))@
500 let metasenv,new_meta =
501 CicMkImplicit.mk_implicit metasenv subst extended_context
504 CicMkImplicit.identity_relocation_list_for_metavariable
507 let rec add_lambdas b =
509 Cic.Prod (name,ty,t) ->
510 Cic.Lambda (name,ty,(add_lambdas b t))
511 | _ -> Cic.Lambda (fresh_name, ty, b)
514 add_lambdas (Cic.Meta (new_meta,irl))
515 arity_instantiated_with_left_args
517 (Some candidate),ugraph4,metasenv,subst
518 | (constructor_args_no,_,instance,_)::tl ->
520 let instance',subst,metasenv =
521 CicMetaSubst.delift_rels subst metasenv
522 constructor_args_no instance
524 let candidate,ugraph,metasenv,subst =
526 fun (candidate_oty,ugraph,metasenv,subst)
527 (constructor_args_no,_,instance,_) ->
528 match candidate_oty with
529 | None -> None,ugraph,metasenv,subst
532 let instance',subst,metasenv =
533 CicMetaSubst.delift_rels subst metasenv
534 constructor_args_no instance
536 let subst,metasenv,ugraph =
537 fo_unif_subst subst context metasenv
540 candidate_oty,ugraph,metasenv,subst
542 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
543 | CicUnification.UnificationFailure _
544 | CicUnification.Uncertain _ ->
545 None,ugraph,metasenv,subst
546 ) (Some instance',ugraph4,metasenv,subst) tl
549 | None -> None, ugraph,metasenv,subst
551 let rec add_lambdas n b =
553 Cic.Prod (name,ty,t) ->
554 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
556 Cic.Lambda (fresh_name, ty,
557 CicSubstitution.lift (n + 1) t)
560 (add_lambdas 0 t arity_instantiated_with_left_args),
561 ugraph,metasenv,subst
562 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
563 None,ugraph4,metasenv,subst
566 | None -> raise (Uncertain "can't solve an higher order unification problem")
568 let subst,metasenv,ugraph =
569 fo_unif_subst subst context metasenv
570 candidate outtype ugraph5
572 C.MutCase (uri, i, outtype, term', pl'),
573 CicReduction.head_beta_reduce
574 (CicMetaSubst.apply_subst subst
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.head_beta_reduce
601 (CicMetaSubst.apply_subst subst
602 (C.Appl(outtype::right_args@[term]))),
603 subst,metasenv,ugraph6)
605 let fl_ty',subst,metasenv,types,ugraph1 =
607 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
608 let ty',_,subst',metasenv',ugraph1 =
609 type_of_aux subst metasenv context ty ugraph
611 fl @ [ty'],subst',metasenv',
612 Some (C.Name n,(C.Decl ty')) :: types, ugraph
613 ) ([],subst,metasenv,[],ugraph) fl
615 let len = List.length types in
616 let context' = types@context in
617 let fl_bo',subst,metasenv,ugraph2 =
619 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
620 let bo',ty_of_bo,subst,metasenv,ugraph1 =
621 type_of_aux subst metasenv context' bo ugraph
623 let subst',metasenv',ugraph' =
624 fo_unif_subst subst context' metasenv
625 ty_of_bo (CicSubstitution.lift len ty) ugraph1
627 fl @ [bo'] , subst',metasenv',ugraph'
628 ) ([],subst,metasenv,ugraph1) fl
630 let (_,_,ty,_) = List.nth fl i in
631 (* now we have the new ty in fl_ty', the new bo in fl_bo',
632 * and we want the new fl with bo' and ty' injected in the right
635 let rec map3 f l1 l2 l3 =
638 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
641 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
644 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
646 let fl_ty',subst,metasenv,types,ugraph1 =
648 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
649 let ty',_,subst',metasenv',ugraph1 =
650 type_of_aux subst metasenv context ty ugraph
652 fl @ [ty'],subst',metasenv',
653 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
654 ) ([],subst,metasenv,[],ugraph) fl
656 let len = List.length types in
657 let context' = types@context in
658 let fl_bo',subst,metasenv,ugraph2 =
660 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
661 let bo',ty_of_bo,subst,metasenv,ugraph1 =
662 type_of_aux subst metasenv context' bo ugraph
664 let subst',metasenv',ugraph' =
665 fo_unif_subst subst context' metasenv
666 ty_of_bo (CicSubstitution.lift len ty) ugraph1
668 fl @ [bo'],subst',metasenv',ugraph'
669 ) ([],subst,metasenv,ugraph1) fl
671 let (_,ty,_) = List.nth fl i in
672 (* now we have the new ty in fl_ty', the new bo in fl_bo',
673 * and we want the new fl with bo' and ty' injected in the right
676 let rec map3 f l1 l2 l3 =
679 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
682 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
685 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
687 (* check_metasenv_consistency checks that the "canonical" context of a
688 metavariable is consitent - up to relocation via the relocation list l -
689 with the actual context *)
690 and check_metasenv_consistency
691 metano subst metasenv context canonical_context l ugraph
693 let module C = Cic in
694 let module R = CicReduction in
695 let module S = CicSubstitution in
696 let lifted_canonical_context =
700 | (Some (n,C.Decl t))::tl ->
701 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
702 | (Some (n,C.Def (t,None)))::tl ->
703 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
704 | None::tl -> None::(aux (i+1) tl)
705 | (Some (n,C.Def (t,Some ty)))::tl ->
707 C.Def ((S.subst_meta l (S.lift i t)),
708 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
710 aux 1 canonical_context
714 (fun (l,subst,metasenv,ugraph) t ct ->
717 l @ [None],subst,metasenv,ugraph
718 | Some t,Some (_,C.Def (ct,_)) ->
719 let subst',metasenv',ugraph' =
721 fo_unif_subst subst context metasenv t ct ugraph
722 with e -> raise (RefineFailure (Reason (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))))))
724 l @ [Some t],subst',metasenv',ugraph'
725 | Some t,Some (_,C.Decl ct) ->
726 let t',inferredty,subst',metasenv',ugraph1 =
727 type_of_aux subst metasenv context t ugraph
729 let subst'',metasenv'',ugraph2 =
732 subst' context metasenv' inferredty ct ugraph1
733 with e -> raise (RefineFailure (Reason (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))))))
735 l @ [Some t'], subst'',metasenv'',ugraph2
737 raise (RefineFailure (Reason (sprintf
738 "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"
739 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
740 (CicMetaSubst.ppcontext subst canonical_context))))
741 ) ([],subst,metasenv,ugraph) l lifted_canonical_context
743 Invalid_argument _ ->
747 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
748 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
749 (CicMetaSubst.ppcontext subst canonical_context))))
751 and check_exp_named_subst metasubst metasenv context tl ugraph =
752 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
754 [] -> [],metasubst,metasenv,ugraph
755 | ((uri,t) as subst)::tl ->
756 let ty_uri,ugraph1 = type_of_variable uri ugraph in
758 CicSubstitution.subst_vars substs ty_uri in
759 (* CSC: why was this code here? it is wrong
760 (match CicEnvironment.get_cooked_obj ~trust:false uri with
761 Cic.Variable (_,Some bo,_,_) ->
763 (RefineFailure (Reason
764 "A variable with a body can not be explicit substituted"))
765 | Cic.Variable (_,None,_,_) -> ()
768 (RefineFailure (Reason
769 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
772 let t',typeoft,metasubst',metasenv',ugraph2 =
773 type_of_aux metasubst metasenv context t ugraph1
775 let metasubst'',metasenv'',ugraph3 =
778 metasubst' context metasenv' typeoft typeofvar ugraph2
780 raise (RefineFailure (Reason
781 ("Wrong Explicit Named Substitution: " ^
782 CicMetaSubst.ppterm metasubst' typeoft ^
783 " not unifiable with " ^
784 CicMetaSubst.ppterm metasubst' typeofvar)))
786 (* FIXME: no mere tail recursive! *)
787 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
788 check_exp_named_subst_aux
789 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
791 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
793 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
796 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
797 let module C = Cic in
798 let context_for_t2 = (Some (name,C.Decl s))::context in
799 let t1'' = CicReduction.whd ~subst context t1 in
800 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
801 match (t1'', t2'') with
802 (C.Sort s1, C.Sort s2)
803 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
804 C.Sort s2,subst,metasenv,ugraph
805 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
806 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
807 let t' = CicUniv.fresh() in
808 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
809 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
810 C.Sort (C.Type t'),subst,metasenv,ugraph2
811 | (C.Sort _,C.Sort (C.Type t1)) ->
812 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
813 C.Sort (C.Type t1),subst,metasenv,ugraph
814 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
815 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
816 (* TODO how can we force the meta to become a sort? If we don't we
817 * brake the invariant that refine produce only well typed terms *)
818 (* TODO if we check the non meta term and if it is a sort then we are
819 * likely to know the exact value of the result e.g. if the rhs is a
820 * Sort (Prop | Set | CProp) then the result is the rhs *)
822 CicMkImplicit.mk_implicit_sort metasenv subst in
823 let (subst, metasenv,ugraph1) =
824 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
826 t2'',subst,metasenv,ugraph1
828 raise (RefineFailure (Reason (sprintf
829 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
830 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
831 (CicPp.ppterm t2''))))
833 and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
834 let rec mk_prod metasenv context =
837 let (metasenv, idx) =
838 CicMkImplicit.mk_implicit_type metasenv subst context
841 CicMkImplicit.identity_relocation_list_for_metavariable context
843 metasenv,Cic.Meta (idx, irl)
845 let (metasenv, idx) =
846 CicMkImplicit.mk_implicit_type metasenv subst context
849 CicMkImplicit.identity_relocation_list_for_metavariable context
851 let meta = Cic.Meta (idx,irl) in
853 (* The name must be fresh for context. *)
854 (* Nevertheless, argty is well-typed only in context. *)
855 (* Thus I generate a name (name_hint) in context and *)
856 (* then I generate a name --- using the hint name_hint *)
857 (* --- that is fresh in (context'@context). *)
859 (* Cic.Name "pippo" *)
860 FreshNamesGenerator.mk_fresh_name ~subst metasenv
861 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
862 (CicMetaSubst.apply_subst_context subst context)
864 ~typ:(CicMetaSubst.apply_subst subst argty)
866 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
867 FreshNamesGenerator.mk_fresh_name ~subst
868 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
870 let metasenv,target =
871 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
873 metasenv,Cic.Prod (name,meta,target)
875 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
876 let (subst, metasenv,ugraph1) =
878 fo_unif_subst subst context metasenv hetype hetype' ugraph
880 debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
881 (CicPp.ppterm hetype)
882 (CicPp.ppterm hetype')
883 (CicMetaSubst.ppmetasenv [] metasenv)
884 (CicMetaSubst.ppsubst subst)));
888 let rec eat_prods metasenv subst context hetype ugraph =
890 | [] -> [],metasenv,subst,hetype,ugraph
891 | (hete, hety)::tl ->
894 let arg,subst,metasenv,ugraph1 =
896 let subst,metasenv,ugraph1 =
897 fo_unif_subst subst context metasenv hety s ugraph
899 hete,subst,metasenv,ugraph1
901 (* we search a coercion from hety to s *)
902 let coer = CoercGraph.look_for_coercion
903 (CicMetaSubst.apply_subst subst hety)
904 (CicMetaSubst.apply_subst subst s)
909 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
911 let coerced_args,metasenv',subst',t',ugraph2 =
912 eat_prods metasenv subst context
913 (* (CicMetaSubst.subst subst hete t) tl *)
914 (CicSubstitution.subst hete t) ugraph1 tl
916 arg::coerced_args,metasenv',subst',t',ugraph2
920 let coerced_args,metasenv,subst,t,ugraph2 =
921 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
923 coerced_args,t,subst,metasenv,ugraph2
926 (* eat prods ends here! *)
928 let t',ty,subst',metasenv',ugraph1 =
929 type_of_aux [] metasenv context t ugraph
931 let substituted_t = CicMetaSubst.apply_subst subst' t' in
932 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
933 (* Andrea: ho rimesso qui l'applicazione della subst al
934 metasenv dopo che ho droppato l'invariante che il metsaenv
935 e' sempre istanziato *)
936 let substituted_metasenv =
937 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
939 (* substituted_t,substituted_ty,substituted_metasenv *)
940 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
942 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
944 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
945 let cleaned_metasenv =
947 (function (n,context,ty) ->
948 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
953 | Some (n, Cic.Decl t) ->
955 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
956 | Some (n, Cic.Def (bo,ty)) ->
957 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
962 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
964 Some (n, Cic.Def (bo',ty'))
968 ) substituted_metasenv
970 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
973 let type_of_aux' metasenv context term ugraph =
975 type_of_aux' metasenv context term ugraph
977 CicUniv.UniverseInconsistency msg -> raise (RefineFailure (Reason msg))
979 (*CSC: this is a very very rough approximation; to be finished *)
980 let are_all_occurrences_positive uri =
982 (*CSC: here we should do a whd; but can we do that? *)
984 Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
985 | Cic.MutInd (uri',_,_) when uri = uri' -> ()
986 | Cic.Prod (_,_,t) -> aux t
987 | _ -> raise (RefineFailure (Reason "not well formed constructor type"))
991 let typecheck metasenv uri obj =
992 let ugraph = CicUniv.empty_ugraph in
994 Cic.Constant (name,Some bo,ty,args,attrs) ->
995 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
996 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
997 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
998 let bo' = CicMetaSubst.apply_subst subst bo' in
999 let ty' = CicMetaSubst.apply_subst subst ty' in
1000 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1001 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1002 | Cic.Constant (name,None,ty,args,attrs) ->
1003 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1004 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1005 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1006 assert (metasenv' = metasenv);
1007 (* Here we do not check the metasenv for correctness *)
1008 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
1009 let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1013 (* instead of raising Uncertain, let's hope that the meta will become
1016 | _ -> raise (RefineFailure (Reason "The term provided is not a type"))
1018 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1019 let bo' = CicMetaSubst.apply_subst subst bo' in
1020 let ty' = CicMetaSubst.apply_subst subst ty' in
1021 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1022 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1023 | Cic.Variable _ -> assert false (* not implemented *)
1024 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1025 (*CSC: this code is greately simplified and many many checks are missing *)
1026 (*CSC: e.g. the constructors are not required to build their own types, *)
1027 (*CSC: the arities are not required to have as type a sort, etc. *)
1028 let uri = match uri with Some uri -> uri | None -> assert false in
1029 let typesno = List.length tys in
1030 (* first phase: we fix only the types *)
1031 let metasenv,ugraph,tys =
1033 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1034 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1035 metasenv,ugraph,(name,b,ty',cl)::res
1036 ) tys (metasenv,ugraph,[]) in
1038 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1039 (* second phase: we fix only the constructors *)
1040 let metasenv,ugraph,tys =
1042 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1043 let metasenv,ugraph,cl' =
1045 (fun (name,ty) (metasenv,ugraph,res) ->
1046 let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1047 let ty',_,metasenv,ugraph =
1048 type_of_aux' metasenv con_context ty ugraph in
1052 (fun (name,_,_,_) (i,t) ->
1053 (* here the explicit_named_substituion is assumed to be *)
1055 let t' = Cic.MutInd (uri,i,[]) in
1056 let t = CicSubstitution.subst t' t in
1058 ) tys (typesno - 1,t)) in
1059 let ty' = undebrujin ty' in
1060 metasenv,ugraph,(name,ty')::res
1061 ) cl (metasenv,ugraph,[])
1063 metasenv,ugraph,(name,b,ty,cl')::res
1064 ) tys (metasenv,ugraph,[]) in
1065 (* third phase: we check the positivity condition *)
1068 List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
1070 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1073 let type_of_aux' metasenv context term =
1076 type_of_aux' metasenv context term in
1078 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1080 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1083 | RefineFailure msg as e ->
1084 debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1086 | Uncertain msg as e ->
1087 debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1091 let profiler2 = HExtlib.profile "CicRefine"
1093 let type_of_aux' metasenv context term ugraph =
1094 profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph
1096 let typecheck metasenv uri obj =
1097 profiler2.HExtlib.profile (typecheck metasenv uri) obj