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;;
30 exception Impossible of int;;
31 exception NotRefinable of string;;
32 exception Uncertain of string;;
33 exception WrongUriToConstant of string;;
34 exception WrongUriToVariable of string;;
35 exception ListTooShort;;
36 exception WrongUriToMutualInductiveDefinitions of string;;
37 exception RelToHiddenHypothesis;;
38 exception WrongArgumentNumber;;
40 let debug_print = prerr_endline
42 let fo_unif_subst subst context metasenv t1 t2 =
44 CicUnification.fo_unif_subst subst context metasenv t1 t2
46 (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
47 | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
53 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
54 | (_,_) -> raise ListTooShort
57 let rec type_of_constant uri =
59 let module R = CicReduction in
60 let module U = UriManager in
61 match CicEnvironment.get_cooked_obj uri with
62 C.Constant (_,_,ty,_) -> ty
63 | C.CurrentProof (_,_,_,ty,_) -> ty
64 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
66 and type_of_variable uri =
68 let module R = CicReduction in
69 let module U = UriManager in
70 match CicEnvironment.get_cooked_obj uri with
71 C.Variable (_,_,ty,_) -> ty
72 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
74 and type_of_mutual_inductive_defs uri i =
76 let module R = CicReduction in
77 let module U = UriManager in
78 match CicEnvironment.get_cooked_obj uri with
79 C.InductiveDefinition (dl,_,_) ->
80 let (_,_,arity,_) = List.nth dl i in
82 | _ -> raise (WrongUriToMutualInductiveDefinitions (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
93 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
95 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
97 (* the check_branch function checks if a branch of a case is refinable.
98 It returns a pair (outype_instance,args), a subst and a metasenv.
99 outype_instance is the expected result of applying the case outtype
101 The problem is that outype is in general unknown, and we should
102 try to synthesize it from the above information, that is in general
103 a second order unification problem. *)
105 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
106 let module C = Cic in
107 let module R = CicMetaSubst in
108 let module Un = CicUnification in
109 match R.whd subst context expectedtype with
111 (n,context,actualtype, [term]), subst, metasenv
112 | C.Appl (C.MutInd (_,_,_)::tl) ->
113 let (_,arguments) = split tl left_args_no in
114 (n,context,actualtype, arguments@[term]), subst, metasenv
115 | C.Prod (name,so,de) ->
116 (* we expect that the actual type of the branch has the due
118 (match R.whd subst context actualtype with
119 C.Prod (name',so',de') ->
120 let subst, metasenv =
121 fo_unif_subst subst context metasenv so so' in
123 (match CicSubstitution.lift 1 term with
124 C.Appl l -> C.Appl (l@[C.Rel 1])
125 | t -> C.Appl [t ; C.Rel 1]) in
126 (* we should also check that the name variable is anonymous in
127 the actual type de' ?? *)
128 check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
129 | _ -> raise WrongArgumentNumber)
130 | _ -> raise (NotRefinable "Prod or MutInd expected")
132 and type_of_aux' metasenv context t =
133 let rec type_of_aux subst metasenv context =
134 let module C = Cic in
135 let module S = CicSubstitution in
136 let module U = UriManager in
137 let module Un = CicUnification in
141 match List.nth context (n - 1) with
142 Some (_,C.Decl t) -> S.lift n t,subst,metasenv
143 | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
144 | Some (_,C.Def (bo,None)) ->
145 type_of_aux subst metasenv context (S.lift n bo)
146 | None -> raise RelToHiddenHypothesis
148 _ -> raise (NotRefinable "Not a close term")
150 | C.Var (uri,exp_named_subst) ->
151 let subst',metasenv' =
152 check_exp_named_subst subst metasenv context exp_named_subst in
154 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
158 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
159 let subst',metasenv' =
160 check_metasenv_consistency n subst metasenv context canonical_context l
162 CicSubstitution.lift_meta l ty, subst', metasenv'
164 C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
166 | C.Implicit _ -> raise (Impossible 21)
168 let _,subst',metasenv' =
169 type_of_aux subst metasenv context ty in
170 let inferredty,subst'',metasenv'' =
171 type_of_aux subst' metasenv' context te
174 let subst''',metasenv''' =
175 fo_unif_subst subst'' context metasenv'' inferredty ty
177 ty,subst''',metasenv'''
179 _ -> raise (NotRefinable "Cast"))
180 | C.Prod (name,s,t) ->
181 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
182 let sort2,subst'',metasenv'' =
183 type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
185 sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
186 | C.Lambda (n,s,t) ->
187 let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
188 (match CicMetaSubst.whd subst' context sort1 with
192 raise (NotRefinable (sprintf
193 "Not well-typed lambda-abstraction: the source %s should be a type;
194 instead it is a term of type %s" (CicPp.ppterm s)
195 (CicPp.ppterm sort1)))
197 let type2,subst'',metasenv'' =
198 type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
200 C.Prod (n,s,type2),subst'',metasenv''
202 (* only to check if s is well-typed *)
203 let ty,subst',metasenv' = type_of_aux subst metasenv context s in
204 let inferredty,subst'',metasenv'' =
205 type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
207 (* One-step LetIn reduction. Even faster than the previous solution.
208 Moreover the inferred type is closer to the expected one. *)
209 CicSubstitution.subst s inferredty,subst',metasenv'
210 | C.Appl (he::tl) when List.length tl > 0 ->
211 let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
212 let tlbody_and_type,subst'',metasenv'' =
214 (fun x (res,subst,metasenv) ->
215 let ty,subst',metasenv' =
216 type_of_aux subst metasenv context x
218 (x, ty)::res,subst',metasenv'
219 ) tl ([],subst',metasenv')
221 eat_prods subst'' metasenv'' context hetype tlbody_and_type
222 | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
223 | C.Const (uri,exp_named_subst) ->
224 let subst',metasenv' =
225 check_exp_named_subst subst metasenv context exp_named_subst in
227 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
230 | C.MutInd (uri,i,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
235 (type_of_mutual_inductive_defs uri i)
238 | C.MutConstruct (uri,i,j,exp_named_subst) ->
239 let subst',metasenv' =
240 check_exp_named_subst subst metasenv context exp_named_subst in
242 CicSubstitution.subst_vars exp_named_subst
243 (type_of_mutual_inductive_constr uri i j)
246 | C.MutCase (uri, i, outtype, term, pl) ->
247 (* first, get the inductive type (and noparams) in the environment *)
248 let (_,b,arity,constructors), expl_params, no_left_params =
249 match CicEnvironment.get_cooked_obj ~trust:true uri with
250 C.InductiveDefinition (l,expl_params,parsno) ->
251 List.nth l i , expl_params, parsno
254 (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
255 let rec count_prod t =
256 match CicMetaSubst.whd subst context t with
257 C.Prod (_, _, t) -> 1 + (count_prod t)
259 let no_args = count_prod arity in
260 (* now, create a "generic" MutInd *)
261 let metasenv,left_args =
262 CicMkImplicit.n_fresh_metas metasenv context no_left_params in
263 let metasenv,right_args =
264 let no_right_params = no_args - no_left_params in
265 if no_right_params < 0 then assert false
266 else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
267 let metasenv,exp_named_subst =
268 CicMkImplicit.fresh_subst metasenv context expl_params in
271 C.MutInd (uri,i,exp_named_subst)
273 C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
275 (* check consistency with the actual type of term *)
276 let actual_type,subst,metasenv =
277 type_of_aux subst metasenv context term in
278 let _, subst, metasenv =
279 type_of_aux subst metasenv context expected_type
281 let actual_type = CicMetaSubst.whd subst context actual_type in
283 fo_unif_subst subst context metasenv expected_type actual_type
285 (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
286 let (_,outtypeinstances,subst,metasenv) =
288 (fun (j,outtypeinstances,subst,metasenv) p ->
290 if left_args = [] then
291 (C.MutConstruct (uri,i,j,exp_named_subst))
293 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
295 let actual_type,subst,metasenv =
296 type_of_aux subst metasenv context p in
297 let expected_type, subst, metasenv =
298 type_of_aux subst metasenv context constructor in
299 let outtypeinstance,subst,metasenv =
301 0 context metasenv subst
302 no_left_params actual_type constructor expected_type in
303 (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
304 (1,[],subst,metasenv) pl in
305 (* we are left to check that the outype matches his instances.
306 The easy case is when the outype is specified, that amount
307 to a trivial check. Otherwise, we should guess a type from
310 let _, subst, metasenv =
311 type_of_aux subst metasenv context
312 (C.Appl ((outtype :: right_args) @ [term]))
314 let (subst,metasenv) =
316 (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
320 CicSubstitution.lift constructor_args_no outtype
322 C.Appl (outtype'::args)
325 (* if appl is not well typed then the type_of below solves the
327 let (_, subst, metasenv) =
328 type_of_aux subst metasenv context appl
331 CicMetaSubst.whd subst context appl
333 fo_unif_subst subst context metasenv instance instance')
334 (subst,metasenv) outtypeinstances in
335 CicMetaSubst.whd subst
336 context (C.Appl(outtype::right_args@[term])),subst,metasenv
338 let subst,metasenv,types =
340 (fun (subst,metasenv,types) (n,_,ty,_) ->
341 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
342 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
343 ) (subst,metasenv,[]) fl
345 let len = List.length types in
346 let context' = types@context in
349 (fun (subst,metasenv) (name,x,ty,bo) ->
350 let ty_of_bo,subst,metasenv =
351 type_of_aux subst metasenv context' bo
353 fo_unif_subst subst context' metasenv
354 ty_of_bo (CicMetaSubst.lift subst len ty)
355 ) (subst,metasenv) fl in
356 let (_,_,ty,_) = List.nth fl i in
359 let subst,metasenv,types =
361 (fun (subst,metasenv,types) (n,ty,_) ->
362 let _,subst',metasenv' = type_of_aux subst metasenv context ty in
363 subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
364 ) (subst,metasenv,[]) fl
366 let len = List.length types in
367 let context' = types@context in
370 (fun (subst,metasenv) (name,ty,bo) ->
371 let ty_of_bo,subst,metasenv =
372 type_of_aux subst metasenv context' bo
374 fo_unif_subst subst context' metasenv
375 ty_of_bo (CicMetaSubst.lift subst len ty)
376 ) (subst,metasenv) fl in
378 let (_,ty,_) = List.nth fl i in
381 (* check_metasenv_consistency checks that the "canonical" context of a
382 metavariable is consitent - up to relocation via the relocation list l -
383 with the actual context *)
384 and check_metasenv_consistency
385 metano subst metasenv context canonical_context l
387 let module C = Cic in
388 let module R = CicReduction in
389 let module S = CicSubstitution in
390 let lifted_canonical_context =
394 | (Some (n,C.Decl t))::tl ->
395 (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
396 | (Some (n,C.Def (t,None)))::tl ->
397 (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
398 | None::tl -> None::(aux (i+1) tl)
399 | (Some (n,C.Def (t,Some ty)))::tl ->
401 C.Def ((S.lift_meta l (S.lift i t)),
402 Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
404 aux 1 canonical_context
408 (fun (subst,metasenv) t ct ->
412 | Some t,Some (_,C.Def (ct,_)) ->
414 fo_unif_subst subst context metasenv t ct
415 with e -> raise (NotRefinable (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 CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
416 | Some t,Some (_,C.Decl ct) ->
417 let inferredty,subst',metasenv' =
418 type_of_aux subst metasenv context t
422 subst' context metasenv' inferredty ct
423 with e -> raise (NotRefinable (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 CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
425 raise (NotRefinable (sprintf
426 "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"
427 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
428 (CicMetaSubst.ppcontext subst canonical_context)))
429 ) (subst,metasenv) l lifted_canonical_context
431 Invalid_argument _ ->
435 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
436 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
437 (CicMetaSubst.ppcontext subst canonical_context)))
439 and check_exp_named_subst metasubst metasenv context =
440 let rec check_exp_named_subst_aux metasubst metasenv substs =
442 [] -> metasubst,metasenv
443 | ((uri,t) as subst)::tl ->
445 CicSubstitution.subst_vars substs (type_of_variable uri) in
446 (match CicEnvironment.get_cooked_obj ~trust:false uri with
447 Cic.Variable (_,Some bo,_,_) ->
450 "A variable with a body can not be explicit substituted")
451 | Cic.Variable (_,None,_,_) -> ()
452 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
454 let typeoft,metasubst',metasenv' =
455 type_of_aux metasubst metasenv context t
458 let metasubst'',metasenv'' =
459 fo_unif_subst metasubst' context metasenv' typeoft typeofvar
461 check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
463 raise (NotRefinable "Wrong Explicit Named Substitution")
465 check_exp_named_subst_aux metasubst metasenv []
467 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
468 let module C = Cic in
469 let context_for_t2 = (Some (name,C.Decl s))::context in
470 let t1'' = CicMetaSubst.whd subst context t1 in
471 let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
472 match (t1'', t2'') with
473 (C.Sort s1, C.Sort s2)
474 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
475 C.Sort s2,subst,metasenv
476 | (C.Sort s1, C.Sort s2) ->
477 (*CSC manca la gestione degli universi!!! *)
478 C.Sort C.Type,subst,metasenv
479 | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
480 | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
481 (* TODO how can we force the meta to become a sort? If we don't we
482 * brake the invariant that refine produce only well typed terms *)
483 (* TODO if we check the non meta term and if it is a sort then we are
484 * likely to know the exact value of the result e.g. if the rhs is a
485 * Sort (Prop | Set | CProp) then the result is the rhs *)
487 CicMkImplicit.mk_implicit_sort metasenv in
488 let (subst, metasenv) =
489 fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
493 raise (NotRefinable (sprintf
494 "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
495 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
496 (CicPp.ppterm t2'')))
498 and eat_prods subst metasenv context hetype tlbody_and_type =
499 let rec mk_prod metasenv context =
502 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
504 CicMkImplicit.identity_relocation_list_for_metavariable context
506 metasenv,Cic.Meta (idx, irl)
508 let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
510 CicMkImplicit.identity_relocation_list_for_metavariable context
512 let meta = Cic.Meta (idx,irl) in
514 (* The name must be fresh for context. *)
515 (* Nevertheless, argty is well-typed only in context. *)
516 (* Thus I generate a name (name_hint) in context and *)
517 (* then I generate a name --- using the hint name_hint *)
518 (* --- that is fresh in (context'@context). *)
520 FreshNamesGenerator.mk_fresh_name
521 (CicMetaSubst.apply_subst_metasenv subst metasenv)
522 (CicMetaSubst.apply_subst_context subst context)
524 (CicMetaSubst.apply_subst subst argty)
526 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
527 FreshNamesGenerator.mk_fresh_name
528 [] context name_hint (Cic.Sort Cic.Prop)
530 let metasenv,target =
531 mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
533 metasenv,Cic.Prod (name,meta,target)
535 let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
536 let (subst, metasenv) =
537 CicUnification.fo_unif_subst subst context metasenv hetype hetype'
539 let rec eat_prods metasenv subst context hetype =
541 [] -> metasenv,subst,hetype
542 | (hete, hety)::tl ->
549 CicUnification.fo_unif_subst subst context metasenv s hety
551 eat_prods metasenv subst context
552 (CicMetaSubst.subst subst hete t) tl
557 (RefineFailure ("XXX " ^ Printexc.to_string e)))
562 let metasenv,subst,t =
563 eat_prods metasenv subst context hetype' tlbody_and_type
568 let rec aux context' args (resty,subst,metasenv) =
570 [] -> resty,subst,metasenv
576 | Some t -> Some (CicMetaSubst.lift subst 1 t)
578 let argty' = CicMetaSubst.lift subst (List.length args) argty in
580 (* The name must be fresh for (context'@context). *)
581 (* Nevertheless, argty is well-typed only in context. *)
582 (* Thus I generate a name (name_hint) in context and *)
583 (* then I generate a name --- using the hint name_hint *)
584 (* --- that is fresh in (context'@context). *)
586 FreshNamesGenerator.mk_fresh_name
587 (CicMetaSubst.apply_subst_metasenv subst metasenv)
588 (CicMetaSubst.apply_subst_context subst context)
590 (CicMetaSubst.apply_subst subst argty)
592 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
593 FreshNamesGenerator.mk_fresh_name
594 [] (context'@context) name_hint (Cic.Sort Cic.Prop)
596 let context'' = Some (name, Cic.Decl argty') :: context' in
597 let (metasenv, idx) =
598 CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
600 (Some (Cic.Rel 1))::args' @
601 (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
604 let newmeta = Cic.Meta (idx, irl) in
605 let prod = Cic.Prod (name, argty, newmeta) in
606 let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
607 let (subst, metasenv) =
608 fo_unif_subst subst context metasenv resty prod
610 aux context'' (Some arg :: args)
611 (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
613 aux [] [] (hetype,subst,metasenv) tlbody_and_type
617 let ty,subst',metasenv' =
618 type_of_aux [] metasenv context t
620 let substituted_t = CicMetaSubst.apply_subst subst' t in
621 let substituted_ty = CicMetaSubst.apply_subst subst' ty in
622 let substituted_metasenv =
623 CicMetaSubst.apply_subst_metasenv subst' metasenv'
626 FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
628 FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
629 let cleaned_metasenv =
631 (function (n,context,ty) ->
632 let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
637 | Some (n, Cic.Decl t) ->
639 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
640 | Some (n, Cic.Def (bo,ty)) ->
641 let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
646 Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
648 Some (n, Cic.Def (bo',ty'))
652 ) substituted_metasenv
654 (cleaned_t,cleaned_ty,cleaned_metasenv)
659 let type_of_aux' metasenv context term =
661 let (t,ty,m) = type_of_aux' metasenv context term in
663 ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
666 ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
670 | CicUnification.AssertFailure msg as e ->
671 debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
675 debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;