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 fo_unif_subst subst context metasenv t1 t2 ugraph =
45 CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
47 (CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg))
48 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
54 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
55 | (_,_) -> raise (AssertFailure "split: list too short")
58 let rec type_of_constant uri ugraph =
60 let module R = CicReduction in
61 let module U = UriManager in
62 let _ = CicTypeChecker.typecheck uri in
65 CicEnvironment.get_cooked_obj ugraph uri
66 with Not_found -> assert false
69 C.Constant (_,_,ty,_,_) -> ty,u
70 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
73 (RefineFailure (Reason ("Unknown constant definition " ^ U.string_of_uri uri)))
75 and type_of_variable uri ugraph =
77 let module R = CicReduction in
78 let module U = UriManager in
79 let _ = CicTypeChecker.typecheck uri in
82 CicEnvironment.get_cooked_obj ugraph uri
83 with Not_found -> assert false
86 C.Variable (_,_,ty,_,_) -> ty,u
90 (Reason ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
92 and type_of_mutual_inductive_defs uri i ugraph =
94 let module R = CicReduction in
95 let module U = UriManager in
96 let _ = CicTypeChecker.typecheck uri in
99 CicEnvironment.get_cooked_obj ugraph uri
100 with Not_found -> assert false
103 C.InductiveDefinition (dl,_,_,_) ->
104 let (_,_,arity,_) = List.nth dl i in
109 (Reason ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
111 and type_of_mutual_inductive_constr uri i j ugraph =
112 let module C = Cic in
113 let module R = CicReduction in
114 let module U = UriManager in
115 let _ = CicTypeChecker.typecheck uri in
118 CicEnvironment.get_cooked_obj ugraph uri
119 with Not_found -> assert false
122 C.InductiveDefinition (dl,_,_,_) ->
123 let (_,_,_,cl) = List.nth dl i in
124 let (_,ty) = List.nth cl (j-1) in
129 (Reason ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
132 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
134 (* the check_branch function checks if a branch of a case is refinable.
135 It returns a pair (outype_instance,args), a subst and a metasenv.
136 outype_instance is the expected result of applying the case outtype
138 The problem is that outype is in general unknown, and we should
139 try to synthesize it from the above information, that is in general
140 a second order unification problem. *)
142 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
143 let module C = Cic in
144 (* let module R = CicMetaSubst in *)
145 let module R = CicReduction in
146 match R.whd ~subst context expectedtype with
148 (n,context,actualtype, [term]), subst, metasenv, ugraph
149 | C.Appl (C.MutInd (_,_,_)::tl) ->
150 let (_,arguments) = split tl left_args_no in
151 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
152 | C.Prod (name,so,de) ->
153 (* we expect that the actual type of the branch has the due
155 (match R.whd ~subst context actualtype with
156 C.Prod (name',so',de') ->
157 let subst, metasenv, ugraph1 =
158 fo_unif_subst subst context metasenv so so' ugraph in
160 (match CicSubstitution.lift 1 term with
161 C.Appl l -> C.Appl (l@[C.Rel 1])
162 | t -> C.Appl [t ; C.Rel 1]) in
163 (* we should also check that the name variable is anonymous in
164 the actual type de' ?? *)
166 ((Some (name,(C.Decl so)))::context)
167 metasenv subst left_args_no de' term' de ugraph1
168 | _ -> raise (AssertFailure "Wrong number of arguments"))
169 | _ -> raise (AssertFailure "Prod or MutInd expected")
171 and type_of_aux' metasenv context t ugraph =
172 let rec type_of_aux subst metasenv context t ugraph =
173 let module C = Cic in
174 let module S = CicSubstitution in
175 let module U = UriManager in
180 match List.nth context (n - 1) with
181 Some (_,C.Decl ty) ->
182 t,S.lift n ty,subst,metasenv, ugraph
183 | Some (_,C.Def (_,Some ty)) ->
184 t,S.lift n ty,subst,metasenv, ugraph
185 | Some (_,C.Def (bo,None)) ->
187 (* if it is in the context it must be already well-typed*)
188 CicTypeChecker.type_of_aux' ~subst metasenv context
191 t,ty,subst,metasenv,ugraph
192 | None -> raise (RefineFailure (Reason "Rel to hidden hypothesis"))
194 _ -> raise (RefineFailure (Reason "Not a close term"))
196 | C.Var (uri,exp_named_subst) ->
197 let exp_named_subst',subst',metasenv',ugraph1 =
198 check_exp_named_subst
199 subst metasenv context exp_named_subst ugraph
201 let ty_uri,ugraph1 = type_of_variable uri ugraph in
203 CicSubstitution.subst_vars exp_named_subst' ty_uri
205 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
208 let (canonical_context, term,ty) =
209 CicUtil.lookup_subst n subst
211 let l',subst',metasenv',ugraph1 =
212 check_metasenv_consistency n subst metasenv context
213 canonical_context l ugraph
215 (* trust or check ??? *)
216 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
217 subst', metasenv', ugraph1
218 (* type_of_aux subst metasenv
219 context (CicSubstitution.subst_meta l term) *)
220 with CicUtil.Subst_not_found _ ->
221 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
222 let l',subst',metasenv', ugraph1 =
223 check_metasenv_consistency n subst metasenv context
224 canonical_context l ugraph
226 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
227 subst', metasenv',ugraph1)
228 | C.Sort (C.Type tno) ->
229 let tno' = CicUniv.fresh() in
230 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
231 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
233 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
234 | C.Implicit _ -> raise (AssertFailure "21")
236 let ty',_,subst',metasenv',ugraph1 =
237 type_of_aux subst metasenv context ty ugraph
239 let te',inferredty,subst'',metasenv'',ugraph2 =
240 type_of_aux subst' metasenv' context te ugraph1
243 let subst''',metasenv''',ugraph3 =
244 fo_unif_subst subst'' context metasenv''
245 inferredty ty ugraph2
247 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
249 _ -> raise (RefineFailure (Reason "Cast")))
250 | C.Prod (name,s,t) ->
251 let s',sort1,subst',metasenv',ugraph1 =
252 type_of_aux subst metasenv context s ugraph
254 let t',sort2,subst'',metasenv'',ugraph2 =
255 type_of_aux subst' metasenv'
256 ((Some (name,(C.Decl s')))::context) t ugraph1
258 let sop,subst''',metasenv''',ugraph3 =
259 sort_of_prod subst'' metasenv''
260 context (name,s') (sort1,sort2) ugraph2
262 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
263 | C.Lambda (n,s,t) ->
264 let s',sort1,subst',metasenv',ugraph1 =
265 type_of_aux subst metasenv context s ugraph
267 (match CicReduction.whd ~subst:subst' context sort1 with
271 raise (RefineFailure (Reason (sprintf
272 "Not well-typed lambda-abstraction: the source %s should be a type;
273 instead it is a term of type %s" (CicPp.ppterm s)
274 (CicPp.ppterm sort1))))
276 let t',type2,subst'',metasenv'',ugraph2 =
277 type_of_aux subst' metasenv'
278 ((Some (n,(C.Decl s')))::context) t ugraph1
280 C.Lambda (n,s',t'),C.Prod (n,s',type2),
281 subst'',metasenv'',ugraph2
283 (* only to check if s is well-typed *)
284 let s',ty,subst',metasenv',ugraph1 =
285 type_of_aux subst metasenv context s ugraph
287 let t',inferredty,subst'',metasenv'',ugraph2 =
288 type_of_aux subst' metasenv'
289 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
291 (* One-step LetIn reduction.
292 * Even faster than the previous solution.
293 * Moreover the inferred type is closer to the expected one.
295 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
296 subst'',metasenv'',ugraph2
297 | C.Appl (he::((_::_) as tl)) ->
298 let he',hetype,subst',metasenv',ugraph1 =
299 type_of_aux subst metasenv context he ugraph
301 let tlbody_and_type,subst'',metasenv'',ugraph2 =
303 (fun x (res,subst,metasenv,ugraph) ->
304 let x',ty,subst',metasenv',ugraph1 =
305 type_of_aux subst metasenv context x ugraph
307 (x', ty)::res,subst',metasenv',ugraph1
308 ) tl ([],subst',metasenv',ugraph1)
310 let tl',applty,subst''',metasenv''',ugraph3 =
311 eat_prods subst'' metasenv'' context
312 hetype tlbody_and_type ugraph2
314 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
315 | C.Appl _ -> raise (RefineFailure (Reason "Appl: no arguments"))
316 | C.Const (uri,exp_named_subst) ->
317 let exp_named_subst',subst',metasenv',ugraph1 =
318 check_exp_named_subst subst metasenv context
319 exp_named_subst ugraph in
320 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
322 CicSubstitution.subst_vars exp_named_subst' ty_uri
324 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
325 | C.MutInd (uri,i,exp_named_subst) ->
326 let exp_named_subst',subst',metasenv',ugraph1 =
327 check_exp_named_subst subst metasenv context
328 exp_named_subst ugraph
330 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
332 CicSubstitution.subst_vars exp_named_subst' ty_uri in
333 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
334 | C.MutConstruct (uri,i,j,exp_named_subst) ->
335 let exp_named_subst',subst',metasenv',ugraph1 =
336 check_exp_named_subst subst metasenv context
337 exp_named_subst ugraph
340 type_of_mutual_inductive_constr uri i j ugraph1
343 CicSubstitution.subst_vars exp_named_subst' ty_uri
345 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
347 | C.MutCase (uri, i, outtype, term, pl) ->
348 (* first, get the inductive type (and noparams)
349 * in the environment *)
350 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
351 let _ = CicTypeChecker.typecheck uri in
352 let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
354 C.InductiveDefinition (l,expl_params,parsno,_) ->
355 List.nth l i , expl_params, parsno, u
359 (Reason ("Unkown mutual inductive definition " ^
360 U.string_of_uri uri)))
362 let rec count_prod t =
363 match CicReduction.whd ~subst context t with
364 C.Prod (_, _, t) -> 1 + (count_prod t)
367 let no_args = count_prod arity in
368 (* now, create a "generic" MutInd *)
369 let metasenv,left_args =
370 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
372 let metasenv,right_args =
373 let no_right_params = no_args - no_left_params in
374 if no_right_params < 0 then assert false
375 else CicMkImplicit.n_fresh_metas
376 metasenv subst context no_right_params
378 let metasenv,exp_named_subst =
379 CicMkImplicit.fresh_subst metasenv subst context expl_params in
382 C.MutInd (uri,i,exp_named_subst)
385 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
387 (* check consistency with the actual type of term *)
388 let term',actual_type,subst,metasenv,ugraph1 =
389 type_of_aux subst metasenv context term ugraph in
390 let expected_type',_, subst, metasenv,ugraph2 =
391 type_of_aux subst metasenv context expected_type ugraph1
393 let actual_type = CicReduction.whd ~subst context actual_type in
394 let subst,metasenv,ugraph3 =
395 fo_unif_subst subst context metasenv
396 expected_type' actual_type ugraph2
398 let rec instantiate_prod t =
402 match CicReduction.whd ~subst context t with
404 instantiate_prod (CicSubstitution.subst he t') tl
407 let arity_instantiated_with_left_args =
408 instantiate_prod arity left_args in
409 (* TODO: check if the sort elimination
410 * is allowed: [(I q1 ... qr)|B] *)
411 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
413 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
415 if left_args = [] then
416 (C.MutConstruct (uri,i,j,exp_named_subst))
419 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
421 let p',actual_type,subst,metasenv,ugraph1 =
422 type_of_aux subst metasenv context p ugraph
424 let constructor',expected_type, subst, metasenv,ugraph2 =
425 type_of_aux subst metasenv context constructor ugraph1
427 let outtypeinstance,subst,metasenv,ugraph3 =
428 check_branch 0 context metasenv subst no_left_params
429 actual_type constructor' expected_type ugraph2
432 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
433 ([],1,[],subst,metasenv,ugraph3) pl
436 (* we are left to check that the outype matches his instances.
437 The easy case is when the outype is specified, that amount
438 to a trivial check. Otherwise, we should guess a type from
444 (let candidate,ugraph5,metasenv,subst =
445 let exp_name_subst, metasenv =
447 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
449 let uris = CicUtil.params_of_obj o in
451 fun uri (acc,metasenv) ->
452 let metasenv',new_meta =
453 CicMkImplicit.mk_implicit metasenv subst context
456 CicMkImplicit.identity_relocation_list_for_metavariable
459 (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
463 match left_args,right_args with
464 [],[] -> Cic.MutInd(uri, i, exp_name_subst)
466 let rec mk_right_args =
469 | n -> (Cic.Rel n)::(mk_right_args (n - 1))
471 let right_args_no = List.length right_args in
472 let lifted_left_args =
473 List.map (CicSubstitution.lift right_args_no) left_args
475 Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
476 (lifted_left_args @ mk_right_args right_args_no))
479 FreshNamesGenerator.mk_fresh_name ~subst metasenv
480 context Cic.Anonymous ~typ:ty
482 match outtypeinstances with
484 let extended_context =
485 let rec add_right_args =
487 Cic.Prod (name,ty,t) ->
488 Some (name,Cic.Decl ty)::(add_right_args t)
491 (Some (fresh_name,Cic.Decl ty))::
493 (add_right_args arity_instantiated_with_left_args))@
496 let metasenv,new_meta =
497 CicMkImplicit.mk_implicit metasenv subst extended_context
500 CicMkImplicit.identity_relocation_list_for_metavariable
503 let rec add_lambdas b =
505 Cic.Prod (name,ty,t) ->
506 Cic.Lambda (name,ty,(add_lambdas b t))
507 | _ -> Cic.Lambda (fresh_name, ty, b)
510 add_lambdas (Cic.Meta (new_meta,irl))
511 arity_instantiated_with_left_args
513 (Some candidate),ugraph4,metasenv,subst
514 | (constructor_args_no,_,instance,_)::tl ->
516 let instance',subst,metasenv =
517 CicMetaSubst.delift_rels subst metasenv
518 constructor_args_no instance
520 let candidate,ugraph,metasenv,subst =
522 fun (candidate_oty,ugraph,metasenv,subst)
523 (constructor_args_no,_,instance,_) ->
524 match candidate_oty with
525 | None -> None,ugraph,metasenv,subst
528 let instance',subst,metasenv =
529 CicMetaSubst.delift_rels subst metasenv
530 constructor_args_no instance
532 let subst,metasenv,ugraph =
533 fo_unif_subst subst context metasenv
536 candidate_oty,ugraph,metasenv,subst
538 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
539 | CicUnification.UnificationFailure _
540 | CicUnification.Uncertain _ ->
541 None,ugraph,metasenv,subst
542 ) (Some instance',ugraph4,metasenv,subst) tl
545 | None -> None, ugraph,metasenv,subst
547 let rec add_lambdas n b =
549 Cic.Prod (name,ty,t) ->
550 Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
552 Cic.Lambda (fresh_name, ty,
553 CicSubstitution.lift (n + 1) t)
556 (add_lambdas 0 t arity_instantiated_with_left_args),
557 ugraph,metasenv,subst
558 with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
559 None,ugraph4,metasenv,subst
562 | None -> raise (Uncertain "can't solve an higher order unification problem")
564 let subst,metasenv,ugraph =
565 fo_unif_subst subst context metasenv
566 candidate outtype ugraph5
568 C.MutCase (uri, i, outtype, term', pl'),
569 CicReduction.head_beta_reduce
570 (CicMetaSubst.apply_subst subst
571 (Cic.Appl (outtype::right_args@[term']))),
572 subst,metasenv,ugraph)
573 | _ -> (* easy case *)
574 let _,_, subst, metasenv,ugraph5 =
575 type_of_aux subst metasenv context
576 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
578 let (subst,metasenv,ugraph6) =
580 (fun (subst,metasenv,ugraph)
581 (constructor_args_no,context,instance,args) ->
585 CicSubstitution.lift constructor_args_no outtype
587 C.Appl (outtype'::args)
589 CicReduction.whd ~subst context appl
591 fo_unif_subst subst context metasenv
592 instance instance' ugraph)
593 (subst,metasenv,ugraph5) outtypeinstances
595 C.MutCase (uri, i, outtype, term', pl'),
596 CicReduction.head_beta_reduce
597 (CicMetaSubst.apply_subst subst
598 (C.Appl(outtype::right_args@[term]))),
599 subst,metasenv,ugraph6)
601 let fl_ty',subst,metasenv,types,ugraph1 =
603 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
604 let ty',_,subst',metasenv',ugraph1 =
605 type_of_aux subst metasenv context ty ugraph
607 fl @ [ty'],subst',metasenv',
608 Some (C.Name n,(C.Decl ty')) :: types, ugraph
609 ) ([],subst,metasenv,[],ugraph) fl
611 let len = List.length types in
612 let context' = types@context in
613 let fl_bo',subst,metasenv,ugraph2 =
615 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
616 let bo',ty_of_bo,subst,metasenv,ugraph1 =
617 type_of_aux subst metasenv context' bo ugraph
619 let subst',metasenv',ugraph' =
620 fo_unif_subst subst context' metasenv
621 ty_of_bo (CicSubstitution.lift len ty) ugraph1
623 fl @ [bo'] , subst',metasenv',ugraph'
624 ) ([],subst,metasenv,ugraph1) fl
626 let (_,_,ty,_) = List.nth fl i in
627 (* now we have the new ty in fl_ty', the new bo in fl_bo',
628 * and we want the new fl with bo' and ty' injected in the right
631 let rec map3 f l1 l2 l3 =
634 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
637 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
640 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
642 let fl_ty',subst,metasenv,types,ugraph1 =
644 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
645 let ty',_,subst',metasenv',ugraph1 =
646 type_of_aux subst metasenv context ty ugraph
648 fl @ [ty'],subst',metasenv',
649 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
650 ) ([],subst,metasenv,[],ugraph) fl
652 let len = List.length types in
653 let context' = types@context in
654 let fl_bo',subst,metasenv,ugraph2 =
656 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
657 let bo',ty_of_bo,subst,metasenv,ugraph1 =
658 type_of_aux subst metasenv context' bo ugraph
660 let subst',metasenv',ugraph' =
661 fo_unif_subst subst context' metasenv
662 ty_of_bo (CicSubstitution.lift len ty) ugraph1
664 fl @ [bo'],subst',metasenv',ugraph'
665 ) ([],subst,metasenv,ugraph1) fl
667 let (_,ty,_) = List.nth fl i in
668 (* now we have the new ty in fl_ty', the new bo in fl_bo',
669 * and we want the new fl with bo' and ty' injected in the right
672 let rec map3 f l1 l2 l3 =
675 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
678 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
681 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
683 (* check_metasenv_consistency checks that the "canonical" context of a
684 metavariable is consitent - up to relocation via the relocation list l -
685 with the actual context *)
686 and check_metasenv_consistency
687 metano subst metasenv context canonical_context l ugraph
689 let module C = Cic in
690 let module R = CicReduction in
691 let module S = CicSubstitution in
692 let lifted_canonical_context =
696 | (Some (n,C.Decl t))::tl ->
697 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
698 | (Some (n,C.Def (t,None)))::tl ->
699 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
700 | None::tl -> None::(aux (i+1) tl)
701 | (Some (n,C.Def (t,Some ty)))::tl ->
703 C.Def ((S.subst_meta l (S.lift i t)),
704 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
706 aux 1 canonical_context
710 (fun (l,subst,metasenv,ugraph) t ct ->
713 l @ [None],subst,metasenv,ugraph
714 | Some t,Some (_,C.Def (ct,_)) ->
715 let subst',metasenv',ugraph' =
717 fo_unif_subst subst context metasenv t ct ugraph
718 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))))))
720 l @ [Some t],subst',metasenv',ugraph'
721 | Some t,Some (_,C.Decl ct) ->
722 let t',inferredty,subst',metasenv',ugraph1 =
723 type_of_aux subst metasenv context t ugraph
725 let subst'',metasenv'',ugraph2 =
728 subst' context metasenv' inferredty ct ugraph1
729 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))))))
731 l @ [Some t'], subst'',metasenv'',ugraph2
733 raise (RefineFailure (Reason (sprintf
734 "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"
735 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
736 (CicMetaSubst.ppcontext subst canonical_context))))
737 ) ([],subst,metasenv,ugraph) l lifted_canonical_context
739 Invalid_argument _ ->
743 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
744 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
745 (CicMetaSubst.ppcontext subst canonical_context))))
747 and check_exp_named_subst metasubst metasenv context tl ugraph =
748 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
750 [] -> [],metasubst,metasenv,ugraph
751 | ((uri,t) as subst)::tl ->
752 let ty_uri,ugraph1 = type_of_variable uri ugraph in
754 CicSubstitution.subst_vars substs ty_uri in
755 (* CSC: why was this code here? it is wrong
756 (match CicEnvironment.get_cooked_obj ~trust:false uri with
757 Cic.Variable (_,Some bo,_,_) ->
759 (RefineFailure (Reason
760 "A variable with a body can not be explicit substituted"))
761 | Cic.Variable (_,None,_,_) -> ()
764 (RefineFailure (Reason
765 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
768 let t',typeoft,metasubst',metasenv',ugraph2 =
769 type_of_aux metasubst metasenv context t ugraph1
771 let metasubst'',metasenv'',ugraph3 =
774 metasubst' context metasenv' typeoft typeofvar ugraph2
776 raise (RefineFailure (Reason
777 ("Wrong Explicit Named Substitution: " ^
778 CicMetaSubst.ppterm metasubst' typeoft ^
779 " not unifiable with " ^
780 CicMetaSubst.ppterm metasubst' typeofvar)))
782 (* FIXME: no mere tail recursive! *)
783 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
784 check_exp_named_subst_aux
785 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
787 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
789 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
792 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
793 let module C = Cic in
794 let context_for_t2 = (Some (name,C.Decl s))::context in
795 let t1'' = CicReduction.whd ~subst context t1 in
796 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
797 match (t1'', t2'') with
798 (C.Sort s1, C.Sort s2)
799 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
800 C.Sort s2,subst,metasenv,ugraph
801 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
802 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
803 let t' = CicUniv.fresh() in
804 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
805 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
806 C.Sort (C.Type t'),subst,metasenv,ugraph2
807 | (C.Sort _,C.Sort (C.Type t1)) ->
808 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
809 C.Sort (C.Type t1),subst,metasenv,ugraph
810 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
811 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
812 (* TODO how can we force the meta to become a sort? If we don't we
813 * brake the invariant that refine produce only well typed terms *)
814 (* TODO if we check the non meta term and if it is a sort then we are
815 * likely to know the exact value of the result e.g. if the rhs is a
816 * Sort (Prop | Set | CProp) then the result is the rhs *)
818 CicMkImplicit.mk_implicit_sort metasenv subst in
819 let (subst, metasenv,ugraph1) =
820 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
822 t2'',subst,metasenv,ugraph1
824 raise (RefineFailure (Reason (sprintf
825 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
826 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
827 (CicPp.ppterm t2''))))
829 and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
830 let rec mk_prod metasenv context =
833 let (metasenv, idx) =
834 CicMkImplicit.mk_implicit_type metasenv subst context
837 CicMkImplicit.identity_relocation_list_for_metavariable context
839 metasenv,Cic.Meta (idx, irl)
841 let (metasenv, idx) =
842 CicMkImplicit.mk_implicit_type metasenv subst context
845 CicMkImplicit.identity_relocation_list_for_metavariable context
847 let meta = Cic.Meta (idx,irl) in
849 (* The name must be fresh for context. *)
850 (* Nevertheless, argty is well-typed only in context. *)
851 (* Thus I generate a name (name_hint) in context and *)
852 (* then I generate a name --- using the hint name_hint *)
853 (* --- that is fresh in (context'@context). *)
855 (* Cic.Name "pippo" *)
856 FreshNamesGenerator.mk_fresh_name ~subst metasenv
857 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
858 (CicMetaSubst.apply_subst_context subst context)
860 ~typ:(CicMetaSubst.apply_subst subst argty)
862 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
863 FreshNamesGenerator.mk_fresh_name ~subst
864 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
866 let metasenv,target =
867 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
869 metasenv,Cic.Prod (name,meta,target)
871 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
872 let (subst, metasenv,ugraph1) =
874 fo_unif_subst subst context metasenv hetype hetype' ugraph
876 debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
877 (CicPp.ppterm hetype)
878 (CicPp.ppterm hetype')
879 (CicMetaSubst.ppmetasenv [] metasenv)
880 (CicMetaSubst.ppsubst subst));
884 let rec eat_prods metasenv subst context hetype ugraph =
886 | [] -> [],metasenv,subst,hetype,ugraph
887 | (hete, hety)::tl ->
890 let arg,subst,metasenv,ugraph1 =
892 let subst,metasenv,ugraph1 =
893 fo_unif_subst subst context metasenv hety s ugraph
895 hete,subst,metasenv,ugraph1
897 (* we search a coercion from hety to s *)
898 let coer = CoercGraph.look_for_coercion
899 (CicMetaSubst.apply_subst subst hety)
900 (CicMetaSubst.apply_subst subst s)
905 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
907 let coerced_args,metasenv',subst',t',ugraph2 =
908 eat_prods metasenv subst context
909 (* (CicMetaSubst.subst subst hete t) tl *)
910 (CicSubstitution.subst hete t) ugraph1 tl
912 arg::coerced_args,metasenv',subst',t',ugraph2
916 let coerced_args,metasenv,subst,t,ugraph2 =
917 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
919 coerced_args,t,subst,metasenv,ugraph2
922 (* eat prods ends here! *)
924 let t',ty,subst',metasenv',ugraph1 =
925 type_of_aux [] metasenv context t ugraph
927 let substituted_t = CicMetaSubst.apply_subst subst' t' in
928 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
929 (* Andrea: ho rimesso qui l'applicazione della subst al
930 metasenv dopo che ho droppato l'invariante che il metsaenv
931 e' sempre istanziato *)
932 let substituted_metasenv =
933 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
935 (* substituted_t,substituted_ty,substituted_metasenv *)
936 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
938 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
940 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
941 let cleaned_metasenv =
943 (function (n,context,ty) ->
944 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
949 | Some (n, Cic.Decl t) ->
951 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
952 | Some (n, Cic.Def (bo,ty)) ->
953 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
958 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
960 Some (n, Cic.Def (bo',ty'))
964 ) substituted_metasenv
966 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
969 let type_of_aux' metasenv context term ugraph =
971 type_of_aux' metasenv context term ugraph
973 CicUniv.UniverseInconsistency msg -> raise (RefineFailure (Reason msg))
975 (*CSC: this is a very very rough approximation; to be finished *)
976 let are_all_occurrences_positive uri =
978 (*CSC: here we should do a whd; but can we do that? *)
980 Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
981 | Cic.MutInd (uri',_,_) when uri = uri' -> ()
982 | Cic.Prod (_,_,t) -> aux t
983 | _ -> raise (RefineFailure (Reason "not well formed constructor type"))
987 let typecheck metasenv uri obj =
988 let ugraph = CicUniv.empty_ugraph in
990 Cic.Constant (name,Some bo,ty,args,attrs) ->
991 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
992 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
993 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
994 let bo' = CicMetaSubst.apply_subst subst bo' in
995 let ty' = CicMetaSubst.apply_subst subst ty' in
996 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
997 Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
998 | Cic.Constant (name,None,ty,args,attrs) ->
999 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1000 Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1001 | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1002 assert (metasenv' = metasenv);
1003 (* Here we do not check the metasenv for correctness *)
1004 let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
1005 let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1009 (* instead of raising Uncertain, let's hope that the meta will become
1012 | _ -> raise (RefineFailure (Reason "The term provided is not a type"))
1014 let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1015 let bo' = CicMetaSubst.apply_subst subst bo' in
1016 let ty' = CicMetaSubst.apply_subst subst ty' in
1017 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1018 Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1019 | Cic.Variable _ -> assert false (* not implemented *)
1020 | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1021 (*CSC: this code is greately simplified and many many checks are missing *)
1022 (*CSC: e.g. the constructors are not required to build their own types, *)
1023 (*CSC: the arities are not required to have as type a sort, etc. *)
1024 let uri = match uri with Some uri -> uri | None -> assert false in
1025 let typesno = List.length tys in
1026 (* first phase: we fix only the types *)
1027 let metasenv,ugraph,tys =
1029 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1030 let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1031 metasenv,ugraph,(name,b,ty',cl)::res
1032 ) tys (metasenv,ugraph,[]) in
1034 List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1035 (* second phase: we fix only the constructors *)
1036 let metasenv,ugraph,tys =
1038 (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1039 let metasenv,ugraph,cl' =
1041 (fun (name,ty) (metasenv,ugraph,res) ->
1042 let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1043 let ty',_,metasenv,ugraph =
1044 type_of_aux' metasenv con_context ty ugraph in
1048 (fun (name,_,_,_) (i,t) ->
1049 (* here the explicit_named_substituion is assumed to be *)
1051 let t' = Cic.MutInd (uri,i,[]) in
1052 let t = CicSubstitution.subst t' t in
1054 ) tys (typesno - 1,t)) in
1055 let ty' = undebrujin ty' in
1056 metasenv,ugraph,(name,ty')::res
1057 ) cl (metasenv,ugraph,[])
1059 metasenv,ugraph,(name,b,ty,cl')::res
1060 ) tys (metasenv,ugraph,[]) in
1061 (* third phase: we check the positivity condition *)
1064 List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
1066 Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1069 let type_of_aux' metasenv context term =
1072 type_of_aux' metasenv context term in
1074 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
1076 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
1079 | RefineFailure msg as e ->
1080 debug_print ("@@@ REFINE FAILED: " ^ msg);
1082 | Uncertain msg as e ->
1083 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);