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 = prerr_endline
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 look_for_coercion src tgt =
52 if (src = (CicUtil.term_of_uri "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)")) &&
53 (tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con"))
56 prerr_endline "TROVATA coercion";
57 Some (CicUtil.term_of_uri "cic:/Coq/Reals/Raxioms/INR.con")
61 prerr_endline (sprintf "NON TROVATA la coercion %s %s" (CicPp.ppterm src)
69 let rec type_of_constant uri ugraph =
71 let module R = CicReduction in
72 let module U = UriManager in
76 CicEnvironment.get_cooked_obj uri
77 with Not_found -> assert false
80 let obj,u= CicEnvironment.get_obj ugraph uri in
82 C.Constant (_,_,ty,_,_) -> ty,u
83 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
86 (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
88 and type_of_variable uri ugraph =
90 let module R = CicReduction in
91 let module U = UriManager in
95 CicEnvironment.get_cooked_obj uri
96 with Not_found -> assert false
99 let obj,u = CicEnvironment.get_obj ugraph uri in
101 C.Variable (_,_,ty,_,_) -> ty,u
105 ("Unknown variable definition " ^ UriManager.string_of_uri uri))
107 and type_of_mutual_inductive_defs uri i ugraph =
108 let module C = Cic in
109 let module R = CicReduction in
110 let module U = UriManager in
114 CicEnvironment.get_cooked_obj uri
115 with Not_found -> assert false
118 let obj,u = CicEnvironment.get_obj ugraph uri in
120 C.InductiveDefinition (dl,_,_,_) ->
121 let (_,_,arity,_) = List.nth dl i in
126 ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
128 and type_of_mutual_inductive_constr uri i j ugraph =
129 let module C = Cic in
130 let module R = CicReduction in
131 let module U = UriManager in
135 CicEnvironment.get_cooked_obj uri
136 with Not_found -> assert false
139 let obj,u = CicEnvironment.get_obj ugraph uri in
141 C.InductiveDefinition (dl,_,_,_) ->
142 let (_,_,_,cl) = List.nth dl i in
143 let (_,ty) = List.nth cl (j-1) in
148 ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
151 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
153 (* the check_branch function checks if a branch of a case is refinable.
154 It returns a pair (outype_instance,args), a subst and a metasenv.
155 outype_instance is the expected result of applying the case outtype
157 The problem is that outype is in general unknown, and we should
158 try to synthesize it from the above information, that is in general
159 a second order unification problem. *)
161 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
162 let module C = Cic in
163 (* let module R = CicMetaSubst in *)
164 let module R = CicReduction in
165 match R.whd ~subst context expectedtype with
167 (n,context,actualtype, [term]), subst, metasenv, ugraph
168 | C.Appl (C.MutInd (_,_,_)::tl) ->
169 let (_,arguments) = split tl left_args_no in
170 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
171 | C.Prod (name,so,de) ->
172 (* we expect that the actual type of the branch has the due
174 (match R.whd ~subst context actualtype with
175 C.Prod (name',so',de') ->
176 let subst, metasenv, ugraph1 =
177 fo_unif_subst subst context metasenv so so' ugraph in
179 (match CicSubstitution.lift 1 term with
180 C.Appl l -> C.Appl (l@[C.Rel 1])
181 | t -> C.Appl [t ; C.Rel 1]) in
182 (* we should also check that the name variable is anonymous in
183 the actual type de' ?? *)
185 ((Some (name,(C.Decl so)))::context)
186 metasenv subst left_args_no de' term' de ugraph1
187 | _ -> raise (AssertFailure "Wrong number of arguments"))
188 | _ -> raise (AssertFailure "Prod or MutInd expected")
190 and type_of_aux' metasenv context t ugraph =
191 let rec type_of_aux subst metasenv context t ugraph =
192 let module C = Cic in
193 let module S = CicSubstitution in
194 let module U = UriManager in
199 match List.nth context (n - 1) with
200 Some (_,C.Decl ty) ->
201 t,S.lift n ty,subst,metasenv, ugraph
202 | Some (_,C.Def (_,Some ty)) ->
203 t,S.lift n ty,subst,metasenv, ugraph
204 | Some (_,C.Def (bo,None)) ->
205 type_of_aux subst metasenv context (S.lift n bo) ugraph
206 | None -> raise (RefineFailure "Rel to hidden hypothesis")
208 _ -> raise (RefineFailure "Not a close term")
210 | C.Var (uri,exp_named_subst) ->
211 let exp_named_subst',subst',metasenv',ugraph1 =
212 check_exp_named_subst
213 subst metasenv context exp_named_subst ugraph
215 let ty_uri,ugraph1 = type_of_variable uri ugraph in
217 CicSubstitution.subst_vars exp_named_subst' ty_uri
219 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
222 let (canonical_context, term,ty) =
223 CicUtil.lookup_subst n subst
225 let l',subst',metasenv',ugraph1 =
226 check_metasenv_consistency n subst metasenv context
227 canonical_context l ugraph
229 (* trust or check ??? *)
230 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
231 subst', metasenv', ugraph1
232 (* type_of_aux subst metasenv
233 context (CicSubstitution.subst_meta l term) *)
234 with CicUtil.Subst_not_found _ ->
235 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
236 let l',subst',metasenv', ugraph1 =
237 check_metasenv_consistency n subst metasenv context
238 canonical_context l ugraph
240 C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
241 subst', metasenv',ugraph1)
242 | C.Sort (C.Type tno) ->
243 let tno' = CicUniv.fresh() in
244 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
245 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
247 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
248 | C.Implicit _ -> raise (AssertFailure "21")
250 let ty',_,subst',metasenv',ugraph1 =
251 type_of_aux subst metasenv context ty ugraph
253 let te',inferredty,subst'',metasenv'',ugraph2 =
254 type_of_aux subst' metasenv' context te ugraph1
257 let subst''',metasenv''',ugraph3 =
258 fo_unif_subst subst'' context metasenv''
259 inferredty ty' ugraph2
261 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
263 _ -> raise (RefineFailure "Cast"))
264 | C.Prod (name,s,t) ->
265 let s',sort1,subst',metasenv',ugraph1 =
266 type_of_aux subst metasenv context s ugraph
268 let t',sort2,subst'',metasenv'',ugraph2 =
269 type_of_aux subst' metasenv'
270 ((Some (name,(C.Decl s')))::context) t ugraph1
272 let sop,subst''',metasenv''',ugraph3 =
273 sort_of_prod subst'' metasenv''
274 context (name,s') (sort1,sort2) ugraph2
276 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
277 | C.Lambda (n,s,t) ->
278 let s',sort1,subst',metasenv',ugraph1 =
279 type_of_aux subst metasenv context s ugraph
281 (match CicReduction.whd ~subst:subst' context sort1 with
285 raise (RefineFailure (sprintf
286 "Not well-typed lambda-abstraction: the source %s should be a type;
287 instead it is a term of type %s" (CicPp.ppterm s)
288 (CicPp.ppterm sort1)))
290 let t',type2,subst'',metasenv'',ugraph2 =
291 type_of_aux subst' metasenv'
292 ((Some (n,(C.Decl s')))::context) t ugraph1
294 C.Lambda (n,s',t'),C.Prod (n,s',type2),
295 subst'',metasenv'',ugraph2
297 (* only to check if s is well-typed *)
298 let s',ty,subst',metasenv',ugraph1 =
299 type_of_aux subst metasenv context s ugraph
301 let t',inferredty,subst'',metasenv'',ugraph2 =
302 type_of_aux subst' metasenv'
303 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
305 (* One-step LetIn reduction.
306 * Even faster than the previous solution.
307 * Moreover the inferred type is closer to the expected one.
309 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
310 subst',metasenv',ugraph2
311 | C.Appl (he::((_::_) as tl)) ->
312 let he',hetype,subst',metasenv',ugraph1 =
313 type_of_aux subst metasenv context he ugraph
315 let tlbody_and_type,subst'',metasenv'',ugraph2 =
317 (fun x (res,subst,metasenv,ugraph) ->
318 let x',ty,subst',metasenv',ugraph1 =
319 type_of_aux subst metasenv context x ugraph
321 (x', ty)::res,subst',metasenv',ugraph1
322 ) tl ([],subst',metasenv',ugraph1)
324 let tl',applty,subst''',metasenv''',ugraph3 =
325 eat_prods subst'' metasenv'' context
326 hetype tlbody_and_type ugraph2
328 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
329 | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
330 | C.Const (uri,exp_named_subst) ->
331 let exp_named_subst',subst',metasenv',ugraph1 =
332 check_exp_named_subst subst metasenv context
333 exp_named_subst ugraph in
334 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
336 CicSubstitution.subst_vars exp_named_subst' ty_uri
338 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
339 | C.MutInd (uri,i,exp_named_subst) ->
340 let exp_named_subst',subst',metasenv',ugraph1 =
341 check_exp_named_subst subst metasenv context
342 exp_named_subst ugraph
344 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
346 CicSubstitution.subst_vars exp_named_subst' ty_uri in
347 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
348 | C.MutConstruct (uri,i,j,exp_named_subst) ->
349 let exp_named_subst',subst',metasenv',ugraph1 =
350 check_exp_named_subst subst metasenv context
351 exp_named_subst ugraph
354 type_of_mutual_inductive_constr uri i j ugraph1
357 CicSubstitution.subst_vars exp_named_subst' ty_uri
359 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
361 | C.MutCase (uri, i, outtype, term, pl) ->
362 (* first, get the inductive type (and noparams)
363 * in the environment *)
364 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
365 let obj,u = CicEnvironment.get_obj ugraph uri in
367 C.InductiveDefinition (l,expl_params,parsno,_) ->
368 List.nth l i , expl_params, parsno, u
372 ("Unkown mutual inductive definition " ^
373 U.string_of_uri uri))
375 let rec count_prod t =
376 match CicReduction.whd ~subst context t with
377 C.Prod (_, _, t) -> 1 + (count_prod t)
380 let no_args = count_prod arity in
381 (* now, create a "generic" MutInd *)
382 let metasenv,left_args =
383 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
385 let metasenv,right_args =
386 let no_right_params = no_args - no_left_params in
387 if no_right_params < 0 then assert false
388 else CicMkImplicit.n_fresh_metas
389 metasenv subst context no_right_params
391 let metasenv,exp_named_subst =
392 CicMkImplicit.fresh_subst metasenv subst context expl_params in
395 C.MutInd (uri,i,exp_named_subst)
398 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
400 (* check consistency with the actual type of term *)
401 let term',actual_type,subst,metasenv,ugraph1 =
402 type_of_aux subst metasenv context term ugraph in
403 let expected_type',_, subst, metasenv,ugraph2 =
404 type_of_aux subst metasenv context expected_type ugraph1
406 let actual_type = CicReduction.whd ~subst context actual_type in
407 let subst,metasenv,ugraph3 =
408 fo_unif_subst subst context metasenv
409 expected_type' actual_type ugraph2
411 (* TODO: check if the sort elimination
412 * is allowed: [(I q1 ... qr)|B] *)
413 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
415 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
417 if left_args = [] then
418 (C.MutConstruct (uri,i,j,exp_named_subst))
421 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
423 let p',actual_type,subst,metasenv,ugraph1 =
424 type_of_aux subst metasenv context p ugraph
426 let constructor',expected_type, subst, metasenv,ugraph2 =
427 type_of_aux subst metasenv context constructor ugraph1
429 let outtypeinstance,subst,metasenv,ugraph3 =
430 check_branch 0 context metasenv subst no_left_params
431 actual_type constructor' expected_type ugraph2
434 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
435 ([],1,[],subst,metasenv,ugraph3) pl
438 (* we are left to check that the outype matches his instances.
439 The easy case is when the outype is specified, that amount
440 to a trivial check. Otherwise, we should guess a type from
446 (let candidate,ugraph5 =
447 match outtypeinstances with
448 | [] -> raise (Uncertain "Inference of annotation for empty inductive types not implemented")
449 | (constructor_args_no,_,instance,_)::tl ->
452 CicSubstitution.delift constructor_args_no
453 (CicMetaSubst.apply_subst subst instance)
456 fun (candidate_oty,ugraph)
457 (constructor_args_no,_,instance,_) ->
458 match candidate_oty with
459 | None -> None,ugraph
463 CicSubstitution.delift
465 (CicMetaSubst.apply_subst subst instance)
468 CicReduction.are_convertible context
472 candidate_oty,ugraph1
475 with Failure s -> None,ugraph
476 ) (Some instance',ugraph4) tl
481 | None -> raise (Uncertain "can't solve an higher order unification problem")
484 fo_unif_subst subst context metasenv
485 candidate outtype ugraph5
487 C.MutCase (uri, i, outtype, term', pl'),candidate,s,m,u)
488 | _ -> (* easy case *)
489 let _,_, subst, metasenv,ugraph5 =
490 type_of_aux subst metasenv context
491 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
493 let (subst,metasenv,ugraph6) =
495 (fun (subst,metasenv,ugraph)
496 (constructor_args_no,context,instance,args) ->
500 CicSubstitution.lift constructor_args_no outtype
502 C.Appl (outtype'::args)
504 CicReduction.whd ~subst context appl
506 fo_unif_subst subst context metasenv
507 instance instance' ugraph)
508 (subst,metasenv,ugraph5) outtypeinstances
510 C.MutCase (uri, i, outtype, term', pl'),
511 CicReduction.whd ~subst context
512 (C.Appl(outtype::right_args@[term])),
513 subst,metasenv,ugraph6)
515 let fl_ty',subst,metasenv,types,ugraph1 =
517 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
518 let ty',_,subst',metasenv',ugraph1 =
519 type_of_aux subst metasenv context ty ugraph
521 fl @ [ty'],subst',metasenv',
522 Some (C.Name n,(C.Decl ty')) :: types, ugraph
523 ) ([],subst,metasenv,[],ugraph) fl
525 let len = List.length types in
526 let context' = types@context in
527 let fl_bo',subst,metasenv,ugraph2 =
529 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
530 let bo',ty_of_bo,subst,metasenv,ugraph1 =
531 type_of_aux subst metasenv context' bo ugraph
533 let subst',metasenv',ugraph' =
534 fo_unif_subst subst context' metasenv
535 ty_of_bo (CicSubstitution.lift len ty) ugraph1
537 fl @ [bo'] , subst',metasenv',ugraph'
538 ) ([],subst,metasenv,ugraph1) fl
540 let (_,_,ty,_) = List.nth fl i in
541 (* now we have the new ty in fl_ty', the new bo in fl_bo',
542 * and we want the new fl with bo' and ty' injected in the right
545 let rec map3 f l1 l2 l3 =
548 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
551 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
554 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
556 let fl_ty',subst,metasenv,types,ugraph1 =
558 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
559 let ty',_,subst',metasenv',ugraph1 =
560 type_of_aux subst metasenv context ty ugraph
562 fl @ [ty'],subst',metasenv',
563 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
564 ) ([],subst,metasenv,[],ugraph) fl
566 let len = List.length types in
567 let context' = types@context in
568 let fl_bo',subst,metasenv,ugraph2 =
570 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
571 let bo',ty_of_bo,subst,metasenv,ugraph1 =
572 type_of_aux subst metasenv context' bo ugraph
574 let subst',metasenv',ugraph' =
575 fo_unif_subst subst context' metasenv
576 ty_of_bo (CicSubstitution.lift len ty) ugraph1
578 fl @ [bo'],subst',metasenv',ugraph'
579 ) ([],subst,metasenv,ugraph1) fl
581 let (_,ty,_) = List.nth fl i in
582 (* now we have the new ty in fl_ty', the new bo in fl_bo',
583 * and we want the new fl with bo' and ty' injected in the right
586 let rec map3 f l1 l2 l3 =
589 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
592 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
595 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
597 (* check_metasenv_consistency checks that the "canonical" context of a
598 metavariable is consitent - up to relocation via the relocation list l -
599 with the actual context *)
600 and check_metasenv_consistency
601 metano subst metasenv context canonical_context l ugraph
603 let module C = Cic in
604 let module R = CicReduction in
605 let module S = CicSubstitution in
606 let lifted_canonical_context =
610 | (Some (n,C.Decl t))::tl ->
611 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
612 | (Some (n,C.Def (t,None)))::tl ->
613 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
614 | None::tl -> None::(aux (i+1) tl)
615 | (Some (n,C.Def (t,Some ty)))::tl ->
617 C.Def ((S.subst_meta l (S.lift i t)),
618 Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
620 aux 1 canonical_context
624 (fun (l,subst,metasenv,ugraph) t ct ->
627 l @ [None],subst,metasenv,ugraph
628 | Some t,Some (_,C.Def (ct,_)) ->
629 let subst',metasenv',ugraph' =
631 fo_unif_subst subst context metasenv t ct ugraph
632 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)))))
634 l @ [Some t],subst',metasenv',ugraph'
635 | Some t,Some (_,C.Decl ct) ->
636 let t',inferredty,subst',metasenv',ugraph1 =
637 type_of_aux subst metasenv context t ugraph
639 let subst'',metasenv'',ugraph2 =
642 subst' context metasenv' inferredty ct ugraph1
643 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)))))
645 l @ [Some t'], subst'',metasenv'',ugraph2
647 raise (RefineFailure (sprintf
648 "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"
649 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
650 (CicMetaSubst.ppcontext subst canonical_context)))
651 ) ([],subst,metasenv,ugraph) l lifted_canonical_context
653 Invalid_argument _ ->
657 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
658 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
659 (CicMetaSubst.ppcontext subst canonical_context)))
661 and check_exp_named_subst metasubst metasenv context tl ugraph =
662 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
664 [] -> [],metasubst,metasenv,ugraph
665 | ((uri,t) as subst)::tl ->
666 let ty_uri,ugraph1 = type_of_variable uri ugraph in
668 CicSubstitution.subst_vars substs ty_uri in
669 (* CSC: why was this code here? it is wrong
670 (match CicEnvironment.get_cooked_obj ~trust:false uri with
671 Cic.Variable (_,Some bo,_,_) ->
674 "A variable with a body can not be explicit substituted")
675 | Cic.Variable (_,None,_,_) -> ()
679 ("Unkown variable definition " ^ UriManager.string_of_uri uri))
682 let t',typeoft,metasubst',metasenv',ugraph2 =
683 type_of_aux metasubst metasenv context t ugraph1
685 let metasubst'',metasenv'',ugraph3 =
688 metasubst' context metasenv' typeoft typeofvar ugraph2
691 ("Wrong Explicit Named Substitution: " ^
692 CicMetaSubst.ppterm metasubst' typeoft ^
693 " not unifiable with " ^
694 CicMetaSubst.ppterm metasubst' typeofvar))
696 (* FIXME: no mere tail recursive! *)
697 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
698 check_exp_named_subst_aux
699 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
701 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
703 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
706 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
707 let module C = Cic in
708 let context_for_t2 = (Some (name,C.Decl s))::context in
709 let t1'' = CicReduction.whd ~subst context t1 in
710 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
711 match (t1'', t2'') with
712 (C.Sort s1, C.Sort s2)
713 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
714 C.Sort s2,subst,metasenv,ugraph
715 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
716 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
717 let t' = CicUniv.fresh() in
718 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
719 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
720 C.Sort (C.Type t'),subst,metasenv,ugraph2
721 | (C.Sort _,C.Sort (C.Type t1)) ->
722 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
723 C.Sort (C.Type t1),subst,metasenv,ugraph
724 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
725 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
726 (* TODO how can we force the meta to become a sort? If we don't we
727 * brake the invariant that refine produce only well typed terms *)
728 (* TODO if we check the non meta term and if it is a sort then we are
729 * likely to know the exact value of the result e.g. if the rhs is a
730 * Sort (Prop | Set | CProp) then the result is the rhs *)
732 CicMkImplicit.mk_implicit_sort metasenv subst in
733 let (subst, metasenv,ugraph1) =
734 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
736 t2'',subst,metasenv,ugraph1
738 raise (RefineFailure (sprintf
739 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
740 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
741 (CicPp.ppterm t2'')))
743 and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
744 let rec mk_prod metasenv context =
747 let (metasenv, idx) =
748 CicMkImplicit.mk_implicit_type metasenv subst context
751 CicMkImplicit.identity_relocation_list_for_metavariable context
753 metasenv,Cic.Meta (idx, irl)
755 let (metasenv, idx) =
756 CicMkImplicit.mk_implicit_type metasenv subst context
759 CicMkImplicit.identity_relocation_list_for_metavariable context
761 let meta = Cic.Meta (idx,irl) in
763 (* The name must be fresh for context. *)
764 (* Nevertheless, argty is well-typed only in context. *)
765 (* Thus I generate a name (name_hint) in context and *)
766 (* then I generate a name --- using the hint name_hint *)
767 (* --- that is fresh in (context'@context). *)
769 (* Cic.Name "pippo" *)
770 FreshNamesGenerator.mk_fresh_name ~subst metasenv
771 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
772 (CicMetaSubst.apply_subst_context subst context)
774 ~typ:(CicMetaSubst.apply_subst subst argty)
776 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
777 FreshNamesGenerator.mk_fresh_name ~subst
778 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
780 let metasenv,target =
781 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
783 metasenv,Cic.Prod (name,meta,target)
785 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
786 let (subst, metasenv,ugraph1) =
788 fo_unif_subst subst context metasenv hetype hetype' ugraph
790 prerr_endline (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
791 (CicPp.ppterm hetype)
792 (CicPp.ppterm hetype')
793 (CicMetaSubst.ppmetasenv metasenv [])
794 (CicMetaSubst.ppsubst subst));
798 let rec eat_prods metasenv subst context hetype ugraph =
800 | [] -> [],metasenv,subst,hetype,ugraph
801 | (hete, hety)::tl ->
804 let arg,subst,metasenv,ugraph1 =
806 let subst,metasenv,ugraph1 =
807 fo_unif_subst subst context metasenv hety s ugraph
809 hete,subst,metasenv,ugraph1
811 (* we search a coercion from hety to s *)
812 let coer = look_for_coercion
813 (CicMetaSubst.apply_subst subst hety)
814 (CicMetaSubst.apply_subst subst s)
819 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
821 let coerced_args,metasenv',subst',t',ugraph2 =
822 eat_prods metasenv subst context
823 (* (CicMetaSubst.subst subst hete t) tl *)
824 (CicSubstitution.subst hete t) ugraph1 tl
826 arg::coerced_args,metasenv',subst',t',ugraph2
830 let coerced_args,metasenv,subst,t,ugraph2 =
831 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
833 coerced_args,t,subst,metasenv,ugraph2
836 (* eat prods ends here! *)
838 let t',ty,subst',metasenv',ugraph1 =
839 type_of_aux [] metasenv context t ugraph
841 let substituted_t = CicMetaSubst.apply_subst subst' t' in
842 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
843 (* Andrea: ho rimesso qui l'applicazione della subst al
844 metasenv dopo che ho droppato l'invariante che il metsaenv
845 e' sempre istanziato *)
846 let substituted_metasenv =
847 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
849 (* substituted_t,substituted_ty,substituted_metasenv *)
850 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
852 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
854 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
855 let cleaned_metasenv =
857 (function (n,context,ty) ->
858 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
863 | Some (n, Cic.Decl t) ->
865 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
866 | Some (n, Cic.Def (bo,ty)) ->
867 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
872 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
874 Some (n, Cic.Def (bo',ty'))
878 ) substituted_metasenv
880 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
884 let type_of_aux' metasenv context term =
887 type_of_aux' metasenv context term in
889 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
891 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
894 | RefineFailure msg as e ->
895 debug_print ("@@@ REFINE FAILED: " ^ msg);
897 | Uncertain msg as e ->
898 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);