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 =
50 if (src = (CicUtil.term_of_uri "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)")) &&
51 (tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con"))
54 prerr_endline "TROVATA coercion";
55 Some (CicUtil.term_of_uri "cic:/Coq/Reals/Raxioms/INR.con")
59 prerr_endline (sprintf "NON TROVATA la coercion %s %s" (CicPp.ppterm src)
66 let rec type_of_constant uri ugraph =
68 let module R = CicReduction in
69 let module U = UriManager in
73 CicEnvironment.get_cooked_obj uri
74 with Not_found -> assert false
77 let obj,u= CicEnvironment.get_obj ugraph uri in
79 C.Constant (_,_,ty,_,_) -> ty,u
80 | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
83 (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
85 and type_of_variable uri ugraph =
87 let module R = CicReduction in
88 let module U = UriManager in
92 CicEnvironment.get_cooked_obj uri
93 with Not_found -> assert false
96 let obj,u = CicEnvironment.get_obj ugraph uri in
98 C.Variable (_,_,ty,_,_) -> ty,u
102 ("Unknown variable definition " ^ UriManager.string_of_uri uri))
104 and type_of_mutual_inductive_defs uri i ugraph =
105 let module C = Cic in
106 let module R = CicReduction in
107 let module U = UriManager in
111 CicEnvironment.get_cooked_obj uri
112 with Not_found -> assert false
115 let obj,u = CicEnvironment.get_obj ugraph uri in
117 C.InductiveDefinition (dl,_,_,_) ->
118 let (_,_,arity,_) = List.nth dl i in
123 ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
125 and type_of_mutual_inductive_constr uri i j ugraph =
126 let module C = Cic in
127 let module R = CicReduction in
128 let module U = UriManager in
132 CicEnvironment.get_cooked_obj uri
133 with Not_found -> assert false
136 let obj,u = CicEnvironment.get_obj ugraph uri in
138 C.InductiveDefinition (dl,_,_,_) ->
139 let (_,_,_,cl) = List.nth dl i in
140 let (_,ty) = List.nth cl (j-1) in
145 ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
148 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
150 (* the check_branch function checks if a branch of a case is refinable.
151 It returns a pair (outype_instance,args), a subst and a metasenv.
152 outype_instance is the expected result of applying the case outtype
154 The problem is that outype is in general unknown, and we should
155 try to synthesize it from the above information, that is in general
156 a second order unification problem. *)
158 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
159 let module C = Cic in
160 (* let module R = CicMetaSubst in *)
161 let module R = CicReduction in
162 match R.whd ~subst context expectedtype with
164 (n,context,actualtype, [term]), subst, metasenv, ugraph
165 | C.Appl (C.MutInd (_,_,_)::tl) ->
166 let (_,arguments) = split tl left_args_no in
167 (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
168 | C.Prod (name,so,de) ->
169 (* we expect that the actual type of the branch has the due
171 (match R.whd ~subst context actualtype with
172 C.Prod (name',so',de') ->
173 let subst, metasenv, ugraph1 =
174 fo_unif_subst subst context metasenv so so' ugraph in
176 (match CicSubstitution.lift 1 term with
177 C.Appl l -> C.Appl (l@[C.Rel 1])
178 | t -> C.Appl [t ; C.Rel 1]) in
179 (* we should also check that the name variable is anonymous in
180 the actual type de' ?? *)
182 ((Some (name,(C.Decl so)))::context)
183 metasenv subst left_args_no de' term' de ugraph1
184 | _ -> raise (AssertFailure "Wrong number of arguments"))
185 | _ -> raise (AssertFailure "Prod or MutInd expected")
187 and type_of_aux' metasenv context t ugraph =
188 let rec type_of_aux subst metasenv context t ugraph =
189 let module C = Cic in
190 let module S = CicSubstitution in
191 let module U = UriManager in
196 match List.nth context (n - 1) with
197 Some (_,C.Decl ty) ->
198 t,S.lift n ty,subst,metasenv, ugraph
199 | Some (_,C.Def (_,Some ty)) ->
200 t,S.lift n ty,subst,metasenv, ugraph
201 | Some (_,C.Def (bo,None)) ->
202 type_of_aux subst metasenv context (S.lift n bo) ugraph
203 | None -> raise (RefineFailure "Rel to hidden hypothesis")
205 _ -> raise (RefineFailure "Not a close term")
207 | C.Var (uri,exp_named_subst) ->
208 let exp_named_subst',subst',metasenv',ugraph1 =
209 check_exp_named_subst
210 subst metasenv context exp_named_subst ugraph
212 let ty_uri,ugraph1 = type_of_variable uri ugraph in
214 CicSubstitution.subst_vars exp_named_subst' ty_uri
216 C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
219 let (canonical_context, term,ty) =
220 CicUtil.lookup_subst n subst
222 let l',subst',metasenv',ugraph1 =
223 check_metasenv_consistency n subst metasenv context
224 canonical_context l ugraph
226 (* trust or check ??? *)
227 C.Meta (n,l'),CicSubstitution.lift_meta l' ty,
228 subst', metasenv', ugraph1
229 (* type_of_aux subst metasenv
230 context (CicSubstitution.lift_meta l term) *)
231 with CicUtil.Subst_not_found _ ->
232 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
233 let l',subst',metasenv', ugraph1 =
234 check_metasenv_consistency n subst metasenv context
235 canonical_context l ugraph
237 C.Meta (n,l'),CicSubstitution.lift_meta l' ty,
238 subst', metasenv',ugraph1)
239 | C.Sort (C.Type tno) ->
240 let tno' = CicUniv.fresh() in
241 let ugraph1 = CicUniv.add_gt tno' tno ugraph in
242 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
244 t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
245 | C.Implicit _ -> raise (AssertFailure "21")
247 let ty',_,subst',metasenv',ugraph1 =
248 type_of_aux subst metasenv context ty ugraph
250 let te',inferredty,subst'',metasenv'',ugraph2 =
251 type_of_aux subst' metasenv' context te ugraph1
254 let subst''',metasenv''',ugraph3 =
255 fo_unif_subst subst'' context metasenv''
256 inferredty ty' ugraph2
258 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
260 _ -> raise (RefineFailure "Cast"))
261 | C.Prod (name,s,t) ->
262 let s',sort1,subst',metasenv',ugraph1 =
263 type_of_aux subst metasenv context s ugraph
265 let t',sort2,subst'',metasenv'',ugraph2 =
266 type_of_aux subst' metasenv'
267 ((Some (name,(C.Decl s')))::context) t ugraph1
269 let sop,subst''',metasenv''',ugraph3 =
270 sort_of_prod subst'' metasenv''
271 context (name,s') (sort1,sort2) ugraph2
273 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
274 | C.Lambda (n,s,t) ->
275 let s',sort1,subst',metasenv',ugraph1 =
276 type_of_aux subst metasenv context s ugraph
278 (match CicReduction.whd ~subst:subst' context sort1 with
282 raise (RefineFailure (sprintf
283 "Not well-typed lambda-abstraction: the source %s should be a type;
284 instead it is a term of type %s" (CicPp.ppterm s)
285 (CicPp.ppterm sort1)))
287 let t',type2,subst'',metasenv'',ugraph2 =
288 type_of_aux subst' metasenv'
289 ((Some (n,(C.Decl s')))::context) t ugraph1
291 C.Lambda (n,s',t'),C.Prod (n,s',type2),
292 subst'',metasenv'',ugraph2
294 (* only to check if s is well-typed *)
295 let s',ty,subst',metasenv',ugraph1 =
296 type_of_aux subst metasenv context s ugraph
298 let t',inferredty,subst'',metasenv'',ugraph2 =
299 type_of_aux subst' metasenv'
300 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
302 (* One-step LetIn reduction.
303 * Even faster than the previous solution.
304 * Moreover the inferred type is closer to the expected one.
306 C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
307 subst',metasenv',ugraph2
308 | C.Appl (he::((_::_) as tl)) ->
309 let he',hetype,subst',metasenv',ugraph1 =
310 type_of_aux subst metasenv context he ugraph
312 let tlbody_and_type,subst'',metasenv'',ugraph2 =
314 (fun x (res,subst,metasenv,ugraph) ->
315 let x',ty,subst',metasenv',ugraph1 =
316 type_of_aux subst metasenv context x ugraph
318 (x', ty)::res,subst',metasenv',ugraph1
319 ) tl ([],subst',metasenv',ugraph1)
321 let tl',applty,subst''',metasenv''',ugraph3 =
322 eat_prods subst'' metasenv'' context
323 hetype tlbody_and_type ugraph2
325 C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
326 | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
327 | C.Const (uri,exp_named_subst) ->
328 let exp_named_subst',subst',metasenv',ugraph1 =
329 check_exp_named_subst subst metasenv context
330 exp_named_subst ugraph in
331 let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
333 CicSubstitution.subst_vars exp_named_subst' ty_uri
335 C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
336 | C.MutInd (uri,i,exp_named_subst) ->
337 let exp_named_subst',subst',metasenv',ugraph1 =
338 check_exp_named_subst subst metasenv context
339 exp_named_subst ugraph
341 let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
343 CicSubstitution.subst_vars exp_named_subst' ty_uri in
344 C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
345 | C.MutConstruct (uri,i,j,exp_named_subst) ->
346 let exp_named_subst',subst',metasenv',ugraph1 =
347 check_exp_named_subst subst metasenv context
348 exp_named_subst ugraph
351 type_of_mutual_inductive_constr uri i j ugraph1
354 CicSubstitution.subst_vars exp_named_subst' ty_uri
356 C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
358 | C.MutCase (uri, i, outtype, term, pl) ->
359 (* first, get the inductive type (and noparams)
360 * in the environment *)
361 let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
362 let obj,u = CicEnvironment.get_obj ugraph uri in
364 C.InductiveDefinition (l,expl_params,parsno,_) ->
365 List.nth l i , expl_params, parsno, u
369 ("Unkown mutual inductive definition " ^
370 U.string_of_uri uri))
372 let rec count_prod t =
373 match CicReduction.whd ~subst context t with
374 C.Prod (_, _, t) -> 1 + (count_prod t)
377 let no_args = count_prod arity in
378 (* now, create a "generic" MutInd *)
379 let metasenv,left_args =
380 CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
382 let metasenv,right_args =
383 let no_right_params = no_args - no_left_params in
384 if no_right_params < 0 then assert false
385 else CicMkImplicit.n_fresh_metas
386 metasenv subst context no_right_params
388 let metasenv,exp_named_subst =
389 CicMkImplicit.fresh_subst metasenv subst context expl_params in
392 C.MutInd (uri,i,exp_named_subst)
395 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
397 (* check consistency with the actual type of term *)
398 let term',actual_type,subst,metasenv,ugraph1 =
399 type_of_aux subst metasenv context term ugraph in
400 let expected_type',_, subst, metasenv,ugraph2 =
401 type_of_aux subst metasenv context expected_type ugraph1
403 let actual_type = CicReduction.whd ~subst context actual_type in
404 let subst,metasenv,ugraph3 =
405 fo_unif_subst subst context metasenv
406 expected_type' actual_type ugraph2
408 (* TODO: check if the sort elimination
409 * is allowed: [(I q1 ... qr)|B] *)
410 let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
412 (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
414 if left_args = [] then
415 (C.MutConstruct (uri,i,j,exp_named_subst))
418 (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
420 let p',actual_type,subst,metasenv,ugraph1 =
421 type_of_aux subst metasenv context p ugraph
423 let constructor',expected_type, subst, metasenv,ugraph2 =
424 type_of_aux subst metasenv context constructor ugraph1
426 let outtypeinstance,subst,metasenv,ugraph3 =
427 check_branch 0 context metasenv subst no_left_params
428 actual_type constructor' expected_type ugraph2
431 outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
432 ([],1,[],subst,metasenv,ugraph3) pl
435 (* we are left to check that the outype matches his instances.
436 The easy case is when the outype is specified, that amount
437 to a trivial check. Otherwise, we should guess a type from
443 (let candidate,ugraph5 =
444 match outtypeinstances with
445 | [] -> raise (Uncertain "Inference of annotation for empty inductive types not implemented")
446 | (constructor_args_no,_,instance,_)::tl ->
449 CicSubstitution.delift constructor_args_no
450 (CicMetaSubst.apply_subst subst instance)
453 fun (candidate_oty,ugraph)
454 (constructor_args_no,_,instance,_) ->
455 match candidate_oty with
456 | None -> None,ugraph
460 CicSubstitution.delift
462 (CicMetaSubst.apply_subst subst instance)
465 CicReduction.are_convertible context
469 candidate_oty,ugraph1
472 with Failure s -> None,ugraph
473 ) (Some instance',ugraph4) tl
478 | None -> raise (Uncertain "can't solve an higher order unification problem")
480 prerr_endline ("CANDIDATE=" ^ (CicPp.ppterm candidate));
482 fo_unif_subst subst context metasenv
483 candidate outtype ugraph5
485 C.MutCase (uri, i, outtype, term', pl'),candidate,s,m,u)
486 | _ -> (* easy case *)
487 let _,_, subst, metasenv,ugraph5 =
488 type_of_aux subst metasenv context
489 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
491 let (subst,metasenv,ugraph6) =
493 (fun (subst,metasenv,ugraph)
494 (constructor_args_no,context,instance,args) ->
498 CicSubstitution.lift constructor_args_no outtype
500 C.Appl (outtype'::args)
502 CicReduction.whd ~subst context appl
504 fo_unif_subst subst context metasenv
505 instance instance' ugraph)
506 (subst,metasenv,ugraph5) outtypeinstances
508 C.MutCase (uri, i, outtype, term', pl'),
509 CicReduction.whd ~subst context
510 (C.Appl(outtype::right_args@[term])),
511 subst,metasenv,ugraph6)
513 let fl_ty',subst,metasenv,types,ugraph1 =
515 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
516 let ty',_,subst',metasenv',ugraph1 =
517 type_of_aux subst metasenv context ty ugraph
519 fl @ [ty'],subst',metasenv',
520 Some (C.Name n,(C.Decl ty')) :: types, ugraph
521 ) ([],subst,metasenv,[],ugraph) fl
523 let len = List.length types in
524 let context' = types@context in
525 let fl_bo',subst,metasenv,ugraph2 =
527 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
528 let bo',ty_of_bo,subst,metasenv,ugraph1 =
529 type_of_aux subst metasenv context' bo ugraph
531 let subst',metasenv',ugraph' =
532 fo_unif_subst subst context' metasenv
533 ty_of_bo (CicSubstitution.lift len ty) ugraph1
535 fl @ [bo'] , subst',metasenv',ugraph'
536 ) ([],subst,metasenv,ugraph1) fl
538 let (_,_,ty,_) = List.nth fl i in
539 (* now we have the new ty in fl_ty', the new bo in fl_bo',
540 * and we want the new fl with bo' and ty' injected in the right
543 let rec map3 f l1 l2 l3 =
546 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
549 let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
552 C.Fix (i,fl''),ty,subst,metasenv,ugraph2
554 let fl_ty',subst,metasenv,types,ugraph1 =
556 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
557 let ty',_,subst',metasenv',ugraph1 =
558 type_of_aux subst metasenv context ty ugraph
560 fl @ [ty'],subst',metasenv',
561 Some (C.Name n,(C.Decl ty')) :: types, ugraph1
562 ) ([],subst,metasenv,[],ugraph) fl
564 let len = List.length types in
565 let context' = types@context in
566 let fl_bo',subst,metasenv,ugraph2 =
568 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
569 let bo',ty_of_bo,subst,metasenv,ugraph1 =
570 type_of_aux subst metasenv context' bo ugraph
572 let subst',metasenv',ugraph' =
573 fo_unif_subst subst context' metasenv
574 ty_of_bo (CicSubstitution.lift len ty) ugraph1
576 fl @ [bo'],subst',metasenv',ugraph'
577 ) ([],subst,metasenv,ugraph1) fl
579 let (_,ty,_) = List.nth fl i in
580 (* now we have the new ty in fl_ty', the new bo in fl_bo',
581 * and we want the new fl with bo' and ty' injected in the right
584 let rec map3 f l1 l2 l3 =
587 | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
590 let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
593 C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
595 (* check_metasenv_consistency checks that the "canonical" context of a
596 metavariable is consitent - up to relocation via the relocation list l -
597 with the actual context *)
598 and check_metasenv_consistency
599 metano subst metasenv context canonical_context l ugraph
601 let module C = Cic in
602 let module R = CicReduction in
603 let module S = CicSubstitution in
604 let lifted_canonical_context =
608 | (Some (n,C.Decl t))::tl ->
609 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
610 | (Some (n,C.Def (t,None)))::tl ->
611 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
612 | None::tl -> None::(aux (i+1) tl)
613 | (Some (n,C.Def (t,Some ty)))::tl ->
615 C.Def ((S.lift_meta l (S.lift i t)),
616 Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
618 aux 1 canonical_context
622 (fun (l,subst,metasenv,ugraph) t ct ->
625 l @ [None],subst,metasenv,ugraph
626 | Some t,Some (_,C.Def (ct,_)) ->
627 let subst',metasenv',ugraph' =
629 fo_unif_subst subst context metasenv t ct ugraph
630 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)))))
632 l @ [Some t],subst',metasenv',ugraph'
633 | Some t,Some (_,C.Decl ct) ->
634 let t',inferredty,subst',metasenv',ugraph1 =
635 type_of_aux subst metasenv context t ugraph
637 let subst'',metasenv'',ugraph2 =
640 subst' context metasenv' inferredty ct ugraph1
641 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)))))
643 l @ [Some t'], subst'',metasenv'',ugraph2
645 raise (RefineFailure (sprintf
646 "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"
647 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
648 (CicMetaSubst.ppcontext subst canonical_context)))
649 ) ([],subst,metasenv,ugraph) l lifted_canonical_context
651 Invalid_argument _ ->
655 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
656 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
657 (CicMetaSubst.ppcontext subst canonical_context)))
659 and check_exp_named_subst metasubst metasenv context tl ugraph =
660 let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
662 [] -> [],metasubst,metasenv,ugraph
663 | ((uri,t) as subst)::tl ->
664 let ty_uri,ugraph1 = type_of_variable uri ugraph in
666 CicSubstitution.subst_vars substs ty_uri in
667 (* CSC: why was this code here? it is wrong
668 (match CicEnvironment.get_cooked_obj ~trust:false uri with
669 Cic.Variable (_,Some bo,_,_) ->
672 "A variable with a body can not be explicit substituted")
673 | Cic.Variable (_,None,_,_) -> ()
677 ("Unkown variable definition " ^ UriManager.string_of_uri uri))
680 let t',typeoft,metasubst',metasenv',ugraph2 =
681 type_of_aux metasubst metasenv context t ugraph1
683 let metasubst'',metasenv'',ugraph3 =
686 metasubst' context metasenv' typeoft typeofvar ugraph2
689 ("Wrong Explicit Named Substitution: " ^
690 CicMetaSubst.ppterm metasubst' typeoft ^
691 " not unifiable with " ^
692 CicMetaSubst.ppterm metasubst' typeofvar))
694 (* FIXME: no mere tail recursive! *)
695 let exp_name_subst, metasubst''', metasenv''', ugraph4 =
696 check_exp_named_subst_aux
697 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
699 ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
701 check_exp_named_subst_aux metasubst metasenv [] tl ugraph
704 and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
705 let module C = Cic in
706 let context_for_t2 = (Some (name,C.Decl s))::context in
707 let t1'' = CicReduction.whd ~subst context t1 in
708 let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
709 match (t1'', t2'') with
710 (C.Sort s1, C.Sort s2)
711 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
712 C.Sort s2,subst,metasenv,ugraph
713 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
714 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
715 let t' = CicUniv.fresh() in
716 let ugraph1 = CicUniv.add_ge t' t1 ugraph in
717 let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
718 C.Sort (C.Type t'),subst,metasenv,ugraph2
719 | (C.Sort _,C.Sort (C.Type t1)) ->
720 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
721 C.Sort (C.Type t1),subst,metasenv,ugraph
722 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
723 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
724 (* TODO how can we force the meta to become a sort? If we don't we
725 * brake the invariant that refine produce only well typed terms *)
726 (* TODO if we check the non meta term and if it is a sort then we are
727 * likely to know the exact value of the result e.g. if the rhs is a
728 * Sort (Prop | Set | CProp) then the result is the rhs *)
730 CicMkImplicit.mk_implicit_sort metasenv subst in
731 let (subst, metasenv,ugraph1) =
732 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
734 t2'',subst,metasenv,ugraph1
736 raise (RefineFailure (sprintf
737 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
738 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
739 (CicPp.ppterm t2'')))
741 and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
742 let rec mk_prod metasenv context =
745 let (metasenv, idx) =
746 CicMkImplicit.mk_implicit_type metasenv subst context
749 CicMkImplicit.identity_relocation_list_for_metavariable context
751 metasenv,Cic.Meta (idx, irl)
753 let (metasenv, idx) =
754 CicMkImplicit.mk_implicit_type metasenv subst context
757 CicMkImplicit.identity_relocation_list_for_metavariable context
759 let meta = Cic.Meta (idx,irl) in
761 (* The name must be fresh for context. *)
762 (* Nevertheless, argty is well-typed only in context. *)
763 (* Thus I generate a name (name_hint) in context and *)
764 (* then I generate a name --- using the hint name_hint *)
765 (* --- that is fresh in (context'@context). *)
767 (* Cic.Name "pippo" *)
768 FreshNamesGenerator.mk_fresh_name ~subst metasenv
769 (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
770 (CicMetaSubst.apply_subst_context subst context)
772 ~typ:(CicMetaSubst.apply_subst subst argty)
774 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
775 FreshNamesGenerator.mk_fresh_name ~subst
776 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
778 let metasenv,target =
779 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
781 metasenv,Cic.Prod (name,meta,target)
783 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
784 let (subst, metasenv,ugraph1) =
786 fo_unif_subst subst context metasenv hetype hetype' ugraph
788 prerr_endline (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
789 (CicPp.ppterm hetype)
790 (CicPp.ppterm hetype')
791 (CicMetaSubst.ppmetasenv metasenv [])
792 (CicMetaSubst.ppsubst subst));
796 let rec eat_prods metasenv subst context hetype ugraph =
798 | [] -> [],metasenv,subst,hetype,ugraph
799 | (hete, hety)::tl ->
802 let arg,subst,metasenv,ugraph1 =
804 let subst,metasenv,ugraph1 =
805 fo_unif_subst subst context metasenv hety s ugraph
807 hete,subst,metasenv,ugraph1
809 (* we search a coercion from hety to s *)
810 let coer = look_for_coercion
811 (CicMetaSubst.apply_subst subst hety)
812 (CicMetaSubst.apply_subst subst s)
817 (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
819 let coerced_args,metasenv',subst',t',ugraph2 =
820 eat_prods metasenv subst context
821 (* (CicMetaSubst.subst subst hete t) tl *)
822 (CicSubstitution.subst hete t) ugraph1 tl
824 arg::coerced_args,metasenv',subst',t',ugraph2
828 let coerced_args,metasenv,subst,t,ugraph2 =
829 eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
831 coerced_args,t,subst,metasenv,ugraph2
834 (* eat prods ends here! *)
836 let t',ty,subst',metasenv',ugraph1 =
837 type_of_aux [] metasenv context t ugraph
839 let substituted_t = CicMetaSubst.apply_subst subst' t' in
840 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
841 (* Andrea: ho rimesso qui l'applicazione della subst al
842 metasenv dopo che ho droppato l'invariante che il metsaenv
843 e' sempre istanziato *)
844 let substituted_metasenv =
845 CicMetaSubst.apply_subst_metasenv subst' metasenv' in
847 (* substituted_t,substituted_ty,substituted_metasenv *)
848 (* ANDREA: spostare tutta questa robaccia da un altra parte *)
850 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
852 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
853 let cleaned_metasenv =
855 (function (n,context,ty) ->
856 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
861 | Some (n, Cic.Decl t) ->
863 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
864 | Some (n, Cic.Def (bo,ty)) ->
865 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
870 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
872 Some (n, Cic.Def (bo',ty'))
876 ) substituted_metasenv
878 (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
882 let type_of_aux' metasenv context term =
885 type_of_aux' metasenv context term in
887 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
889 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
892 | RefineFailure msg as e ->
893 debug_print ("@@@ REFINE FAILED: " ^ msg);
895 | Uncertain msg as e ->
896 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);