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 =
36 CicUnification.fo_unif_subst subst context metasenv t1 t2
38 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
39 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
45 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
46 | (_,_) -> raise (AssertFailure "split: list too short")
49 let rec type_of_constant uri =
51 let module R = CicReduction in
52 let module U = UriManager in
53 match CicEnvironment.get_cooked_obj uri with
54 C.Constant (_,_,ty,_) -> ty
55 | C.CurrentProof (_,_,_,ty,_) -> ty
58 (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
60 and type_of_variable uri =
62 let module R = CicReduction in
63 let module U = UriManager in
64 match CicEnvironment.get_cooked_obj uri with
65 C.Variable (_,_,ty,_) -> ty
69 ("Unknown variable definition " ^ UriManager.string_of_uri uri))
71 and type_of_mutual_inductive_defs uri i =
73 let module R = CicReduction in
74 let module U = UriManager in
75 match CicEnvironment.get_cooked_obj uri with
76 C.InductiveDefinition (dl,_,_) ->
77 let (_,_,arity,_) = List.nth dl i in
82 ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
84 and type_of_mutual_inductive_constr uri i j =
86 let module R = CicReduction in
87 let module U = UriManager in
88 match CicEnvironment.get_cooked_obj uri with
89 C.InductiveDefinition (dl,_,_) ->
90 let (_,_,_,cl) = List.nth dl i in
91 let (_,ty) = List.nth cl (j-1) in
96 ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
98 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
100 (* the check_branch function checks if a branch of a case is refinable.
101 It returns a pair (outype_instance,args), a subst and a metasenv.
102 outype_instance is the expected result of applying the case outtype
104 The problem is that outype is in general unknown, and we should
105 try to synthesize it from the above information, that is in general
106 a second order unification problem. *)
108 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
109 let module C = Cic in
110 let module R = CicMetaSubst in
111 match R.whd subst context expectedtype with
113 (n,context,actualtype, [term]), subst, metasenv
114 | C.Appl (C.MutInd (_,_,_)::tl) ->
115 let (_,arguments) = split tl left_args_no in
116 (n,context,actualtype, arguments@[term]), subst, metasenv
117 | C.Prod (name,so,de) ->
118 (* we expect that the actual type of the branch has the due
120 (match R.whd subst context actualtype with
121 C.Prod (name',so',de') ->
122 let subst, metasenv =
123 fo_unif_subst subst context metasenv so so' in
125 (match CicSubstitution.lift 1 term with
126 C.Appl l -> C.Appl (l@[C.Rel 1])
127 | t -> C.Appl [t ; C.Rel 1]) in
128 (* we should also check that the name variable is anonymous in
129 the actual type de' ?? *)
130 check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
131 | _ -> raise (AssertFailure "Wrong number of arguments"))
132 | _ -> raise (AssertFailure "Prod or MutInd expected")
134 and type_of_aux' metasenv context t =
135 let rec type_of_aux subst metasenv context =
136 let module C = Cic in
137 let module S = CicSubstitution in
138 let module U = UriManager in
142 match List.nth context (n - 1) with
143 Some (_,C.Decl t) -> S.lift n t,subst,metasenv
144 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
145 | Some (_,C.Def (bo,None)) ->
146 type_of_aux subst metasenv context (S.lift n bo)
147 | None -> raise (RefineFailure "Rel to hidden hypothesis")
149 _ -> raise (RefineFailure "Not a close term")
151 | C.Var (uri,exp_named_subst) ->
152 let subst',metasenv' =
153 check_exp_named_subst subst metasenv context exp_named_subst in
155 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
159 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
160 let subst',metasenv' =
161 check_metasenv_consistency n subst metasenv context canonical_context l
163 CicSubstitution.lift_meta l ty, subst', metasenv'
164 (* TASSI: CONSTRAINT *)
165 | C.Sort (C.Type t) ->
166 let t' = CicUniv.fresh() in
167 if not (CicUniv.add_gt t' t ) then
168 assert false (* t' is fresh! an error in CicUniv *)
170 C.Sort (C.Type t'),subst,metasenv
171 (* TASSI: CONSTRAINT *)
172 | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv
173 | C.Implicit _ -> raise (AssertFailure "21")
175 let _,subst',metasenv' =
176 type_of_aux subst metasenv context ty in
177 let inferredty,subst'',metasenv'' =
178 type_of_aux subst' metasenv' context te
181 let subst''',metasenv''' =
182 fo_unif_subst subst'' context metasenv'' inferredty ty
184 ty,subst''',metasenv'''
186 _ -> raise (RefineFailure "Cast"))
187 | C.Prod (name,s,t) ->
188 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
189 let sort2,subst'',metasenv'' =
190 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
192 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
193 | C.Lambda (n,s,t) ->
194 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
195 (match CicMetaSubst.whd subst' context sort1 with
199 raise (RefineFailure (sprintf
200 "Not well-typed lambda-abstraction: the source %s should be a type;
201 instead it is a term of type %s" (CicPp.ppterm s)
202 (CicPp.ppterm sort1)))
204 let type2,subst'',metasenv'' =
205 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
207 C.Prod (n,s,type2),subst'',metasenv''
209 (* only to check if s is well-typed *)
210 let ty,subst',metasenv' = type_of_aux subst metasenv context s in
211 let inferredty,subst'',metasenv'' =
212 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
214 (* One-step LetIn reduction. Even faster than the previous solution.
215 Moreover the inferred type is closer to the expected one. *)
216 CicSubstitution.subst s inferredty,subst',metasenv'
217 | C.Appl (he::tl) when List.length tl > 0 ->
218 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
219 let tlbody_and_type,subst'',metasenv'' =
221 (fun x (res,subst,metasenv) ->
222 let ty,subst',metasenv' =
223 type_of_aux subst metasenv context x
225 (x, ty)::res,subst',metasenv'
226 ) tl ([],subst',metasenv')
228 eat_prods subst'' metasenv'' context hetype tlbody_and_type
229 | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
230 | C.Const (uri,exp_named_subst) ->
231 let subst',metasenv' =
232 check_exp_named_subst subst metasenv context exp_named_subst in
234 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
237 | C.MutInd (uri,i,exp_named_subst) ->
238 let subst',metasenv' =
239 check_exp_named_subst subst metasenv context exp_named_subst in
241 CicSubstitution.subst_vars exp_named_subst
242 (type_of_mutual_inductive_defs uri i)
245 | C.MutConstruct (uri,i,j,exp_named_subst) ->
246 let subst',metasenv' =
247 check_exp_named_subst subst metasenv context exp_named_subst in
249 CicSubstitution.subst_vars exp_named_subst
250 (type_of_mutual_inductive_constr uri i j)
253 | C.MutCase (uri, i, outtype, term, pl) ->
254 (* first, get the inductive type (and noparams) in the environment *)
255 let (_,b,arity,constructors), expl_params, no_left_params =
256 match CicEnvironment.get_cooked_obj ~trust:true uri with
257 C.InductiveDefinition (l,expl_params,parsno) ->
258 List.nth l i , expl_params, parsno
262 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
263 let rec count_prod t =
264 match CicMetaSubst.whd subst context t with
265 C.Prod (_, _, t) -> 1 + (count_prod t)
267 let no_args = count_prod arity in
268 (* now, create a "generic" MutInd *)
269 let metasenv,left_args =
270 CicMkImplicit.n_fresh_metas metasenv context no_left_params in
271 let metasenv,right_args =
272 let no_right_params = no_args - no_left_params in
273 if no_right_params < 0 then assert false
274 else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
275 let metasenv,exp_named_subst =
276 CicMkImplicit.fresh_subst metasenv context expl_params in
279 C.MutInd (uri,i,exp_named_subst)
281 C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
283 (* check consistency with the actual type of term *)
284 let actual_type,subst,metasenv =
285 type_of_aux subst metasenv context term in
286 let _, subst, metasenv =
287 type_of_aux subst metasenv context expected_type
289 let actual_type = CicMetaSubst.whd subst context actual_type in
291 fo_unif_subst subst context metasenv expected_type actual_type
293 (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
294 let (_,outtypeinstances,subst,metasenv) =
296 (fun (j,outtypeinstances,subst,metasenv) p ->
298 if left_args = [] then
299 (C.MutConstruct (uri,i,j,exp_named_subst))
301 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
303 let actual_type,subst,metasenv =
304 type_of_aux subst metasenv context p in
305 let expected_type, subst, metasenv =
306 type_of_aux subst metasenv context constructor in
307 let outtypeinstance,subst,metasenv =
309 0 context metasenv subst
310 no_left_params actual_type constructor expected_type in
311 (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
312 (1,[],subst,metasenv) pl in
313 (* we are left to check that the outype matches his instances.
314 The easy case is when the outype is specified, that amount
315 to a trivial check. Otherwise, we should guess a type from
319 let _, subst, metasenv =
320 type_of_aux subst metasenv context
321 (C.Appl ((outtype :: right_args) @ [term]))
323 let (subst,metasenv) =
325 (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
329 CicSubstitution.lift constructor_args_no outtype
331 C.Appl (outtype'::args)
334 (* if appl is not well typed then the type_of below solves the
336 let (_, subst, metasenv) =
337 type_of_aux subst metasenv context appl
340 CicMetaSubst.whd subst context appl
342 fo_unif_subst subst context metasenv instance instance')
343 (subst,metasenv) outtypeinstances in
344 CicMetaSubst.whd subst
345 context (C.Appl(outtype::right_args@[term])),subst,metasenv
347 let subst,metasenv,types =
349 (fun (subst,metasenv,types) (n,_,ty,_) ->
350 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
351 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
352 ) (subst,metasenv,[]) fl
354 let len = List.length types in
355 let context' = types@context in
358 (fun (subst,metasenv) (name,x,ty,bo) ->
359 let ty_of_bo,subst,metasenv =
360 type_of_aux subst metasenv context' bo
362 fo_unif_subst subst context' metasenv
363 ty_of_bo (CicMetaSubst.lift subst len ty)
364 ) (subst,metasenv) fl in
365 let (_,_,ty,_) = List.nth fl i in
368 let subst,metasenv,types =
370 (fun (subst,metasenv,types) (n,ty,_) ->
371 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
372 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
373 ) (subst,metasenv,[]) fl
375 let len = List.length types in
376 let context' = types@context in
379 (fun (subst,metasenv) (name,ty,bo) ->
380 let ty_of_bo,subst,metasenv =
381 type_of_aux subst metasenv context' bo
383 fo_unif_subst subst context' metasenv
384 ty_of_bo (CicMetaSubst.lift subst len ty)
385 ) (subst,metasenv) fl in
387 let (_,ty,_) = List.nth fl i in
390 (* check_metasenv_consistency checks that the "canonical" context of a
391 metavariable is consitent - up to relocation via the relocation list l -
392 with the actual context *)
393 and check_metasenv_consistency
394 metano subst metasenv context canonical_context l
396 let module C = Cic in
397 let module R = CicReduction in
398 let module S = CicSubstitution in
399 let lifted_canonical_context =
403 | (Some (n,C.Decl t))::tl ->
404 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
405 | (Some (n,C.Def (t,None)))::tl ->
406 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
407 | None::tl -> None::(aux (i+1) tl)
408 | (Some (n,C.Def (t,Some ty)))::tl ->
410 C.Def ((S.lift_meta l (S.lift i t)),
411 Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
413 aux 1 canonical_context
417 (fun (subst,metasenv) t ct ->
421 | Some t,Some (_,C.Def (ct,_)) ->
423 fo_unif_subst subst context metasenv t ct
424 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)))))
425 | Some t,Some (_,C.Decl ct) ->
426 let inferredty,subst',metasenv' =
427 type_of_aux subst metasenv context t
431 subst' context metasenv' inferredty ct
432 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)))))
434 raise (RefineFailure (sprintf
435 "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"
436 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
437 (CicMetaSubst.ppcontext subst canonical_context)))
438 ) (subst,metasenv) l lifted_canonical_context
440 Invalid_argument _ ->
444 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
445 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
446 (CicMetaSubst.ppcontext subst canonical_context)))
448 and check_exp_named_subst metasubst metasenv context =
449 let rec check_exp_named_subst_aux metasubst metasenv substs =
451 [] -> metasubst,metasenv
452 | ((uri,t) as subst)::tl ->
454 CicSubstitution.subst_vars substs (type_of_variable uri) in
455 (match CicEnvironment.get_cooked_obj ~trust:false uri with
456 Cic.Variable (_,Some bo,_,_) ->
459 "A variable with a body can not be explicit substituted")
460 | Cic.Variable (_,None,_,_) -> ()
464 ("Unkown variable definition " ^ UriManager.string_of_uri uri))
466 let typeoft,metasubst',metasenv' =
467 type_of_aux metasubst metasenv context t
470 let metasubst'',metasenv'' =
471 fo_unif_subst metasubst' context metasenv' typeoft typeofvar
473 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
475 raise (RefineFailure "Wrong Explicit Named Substitution")
477 check_exp_named_subst_aux metasubst metasenv []
479 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
480 let module C = Cic in
481 let context_for_t2 = (Some (name,C.Decl s))::context in
482 let t1'' = CicMetaSubst.whd subst context t1 in
483 let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
484 match (t1'', t2'') with
485 (C.Sort s1, C.Sort s2)
486 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
487 C.Sort s2,subst,metasenv
488 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
489 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
490 let t' = CicUniv.fresh() in
491 if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
492 assert false ; (* not possible, error in CicUniv *)
493 C.Sort (C.Type t'),subst,metasenv
494 | (C.Sort _,C.Sort (C.Type t1)) ->
495 (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
496 C.Sort (C.Type t1),subst,metasenv
497 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
498 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
499 (* TODO how can we force the meta to become a sort? If we don't we
500 * brake the invariant that refine produce only well typed terms *)
501 (* TODO if we check the non meta term and if it is a sort then we are
502 * likely to know the exact value of the result e.g. if the rhs is a
503 * Sort (Prop | Set | CProp) then the result is the rhs *)
505 CicMkImplicit.mk_implicit_sort metasenv in
506 let (subst, metasenv) =
507 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
511 raise (RefineFailure (sprintf
512 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
513 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
514 (CicPp.ppterm t2'')))
516 and eat_prods subst metasenv context hetype tlbody_and_type =
517 let rec mk_prod metasenv context =
520 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
522 CicMkImplicit.identity_relocation_list_for_metavariable context
524 metasenv,Cic.Meta (idx, irl)
526 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
528 CicMkImplicit.identity_relocation_list_for_metavariable context
530 let meta = Cic.Meta (idx,irl) in
532 (* The name must be fresh for context. *)
533 (* Nevertheless, argty is well-typed only in context. *)
534 (* Thus I generate a name (name_hint) in context and *)
535 (* then I generate a name --- using the hint name_hint *)
536 (* --- that is fresh in (context'@context). *)
538 FreshNamesGenerator.mk_fresh_name
539 (CicMetaSubst.apply_subst_metasenv subst metasenv)
540 (CicMetaSubst.apply_subst_context subst context)
542 (CicMetaSubst.apply_subst subst argty)
544 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
545 FreshNamesGenerator.mk_fresh_name
546 [] context name_hint (Cic.Sort Cic.Prop)
548 let metasenv,target =
549 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
551 metasenv,Cic.Prod (name,meta,target)
553 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
554 let (subst, metasenv) =
555 fo_unif_subst subst context metasenv hetype hetype'
557 let rec eat_prods metasenv subst context hetype =
559 [] -> metasenv,subst,hetype
560 | (hete, hety)::tl ->
564 fo_unif_subst subst context metasenv hety s
566 eat_prods metasenv subst context
567 (CicMetaSubst.subst subst hete t) tl
571 let metasenv,subst,t =
572 eat_prods metasenv subst context hetype' tlbody_and_type
576 let rec aux context' args (resty,subst,metasenv) =
578 [] -> resty,subst,metasenv
584 | Some t -> Some (CicMetaSubst.lift subst 1 t)
586 let argty' = CicMetaSubst.lift subst (List.length args) argty in
588 (* The name must be fresh for (context'@context). *)
589 (* Nevertheless, argty is well-typed only in context. *)
590 (* Thus I generate a name (name_hint) in context and *)
591 (* then I generate a name --- using the hint name_hint *)
592 (* --- that is fresh in (context'@context). *)
594 FreshNamesGenerator.mk_fresh_name
595 (CicMetaSubst.apply_subst_metasenv subst metasenv)
596 (CicMetaSubst.apply_subst_context subst context)
598 (CicMetaSubst.apply_subst subst argty)
600 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
601 FreshNamesGenerator.mk_fresh_name
602 [] (context'@context) name_hint (Cic.Sort Cic.Prop)
604 let context'' = Some (name, Cic.Decl argty') :: context' in
605 let (metasenv, idx) =
606 CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
608 (Some (Cic.Rel 1))::args' @
609 (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
612 let newmeta = Cic.Meta (idx, irl) in
613 let prod = Cic.Prod (name, argty, newmeta) in
614 let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
615 let (subst, metasenv) =
616 fo_unif_subst subst context metasenv resty prod
618 aux context'' (Some arg :: args)
619 (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
621 aux [] [] (hetype,subst,metasenv) tlbody_and_type
624 let ty,subst',metasenv' =
625 type_of_aux [] metasenv context t
627 let substituted_t = CicMetaSubst.apply_subst subst' t in
628 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
629 let substituted_metasenv =
630 CicMetaSubst.apply_subst_metasenv subst' metasenv'
633 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
635 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
636 let cleaned_metasenv =
638 (function (n,context,ty) ->
639 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
644 | Some (n, Cic.Decl t) ->
646 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
647 | Some (n, Cic.Def (bo,ty)) ->
648 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
653 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
655 Some (n, Cic.Def (bo',ty'))
659 ) substituted_metasenv
661 (cleaned_t,cleaned_ty,cleaned_metasenv)
666 let type_of_aux' metasenv context term =
668 let (t,ty,m) = type_of_aux' metasenv context term in
670 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
673 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
677 | RefineFailure msg as e ->
678 debug_print ("@@@ REFINE FAILED: " ^ msg);
680 | Uncertain msg as e ->
681 debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);