X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=b3525d3182bcec3737d02c2883cd7402d1acf730;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=b64d8f4bb8b2236793b5be72d911e038e946b227;hpb=f42507bf45ea6b50adbae7ba8117905cc9631101;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index b64d8f4bb..b3525d318 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -26,36 +26,24 @@
 open Printf
 
 exception RefineFailure of string;;
-
-exception Impossible of int;;
-exception NotRefinable of string;;
 exception Uncertain of string;;
-exception WrongUriToConstant of string;;
-exception WrongUriToVariable of string;;
-exception ListTooShort;;
-exception WrongUriToMutualInductiveDefinitions of string;;
-exception RelToHiddenHypothesis;;
-exception WrongArgumentNumber;;
-
-let fdebug = ref 0;;
-let debug t context =
- let rec debug_aux t i =
-  let module C = Cic in
-  let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
- in
-  if !fdebug = 0 then
-   raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
-   (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
-;;
+exception AssertFailure of string;;
 
 let debug_print = prerr_endline
 
+let fo_unif_subst subst context metasenv t1 t2 =
+ try
+  CicUnification.fo_unif_subst subst context metasenv t1 t2
+ with
+    (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
+  | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
+;;
+
 let rec split l n =
  match (l,n) with
     (l,0) -> ([], l)
   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
-  | (_,_) -> raise ListTooShort
+  | (_,_) -> raise (AssertFailure "split: list too short")
 ;;
 
 let rec type_of_constant uri =
@@ -65,7 +53,9 @@ let rec type_of_constant uri =
   match CicEnvironment.get_cooked_obj uri with
      C.Constant (_,_,ty,_) -> ty
    | C.CurrentProof (_,_,_,ty,_) -> ty
-   | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
+   | _ ->
+     raise
+      (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
 
 and type_of_variable uri =
  let module C = Cic in
@@ -73,7 +63,10 @@ and type_of_variable uri =
  let module U = UriManager in
   match CicEnvironment.get_cooked_obj uri with
      C.Variable (_,_,ty,_) -> ty
-   |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+   |  _ ->
+      raise
+       (RefineFailure
+         ("Unknown variable definition " ^ UriManager.string_of_uri uri))
 
 and type_of_mutual_inductive_defs uri i =
  let module C = Cic in
@@ -83,7 +76,10 @@ and type_of_mutual_inductive_defs uri i =
      C.InductiveDefinition (dl,_,_) ->
       let (_,_,arity,_) = List.nth dl i in
        arity
-   | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+   | _ ->
+     raise
+      (RefineFailure
+        ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
 
 and type_of_mutual_inductive_constr uri i j =
  let module C = Cic in
@@ -94,7 +90,10 @@ and type_of_mutual_inductive_constr uri i j =
        let (_,_,_,cl) = List.nth dl i in
         let (_,ty) = List.nth cl (j-1) in
          ty
-   | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+   | _ ->
+     raise
+      (RefineFailure
+        ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
 
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 
@@ -109,7 +108,6 @@ and type_of_mutual_inductive_constr uri i j =
 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
   let module C = Cic in
   let module R = CicMetaSubst in
-  let module Un = CicUnification in 
   match R.whd subst context expectedtype with
      C.MutInd (_,_,_) ->
        (n,context,actualtype, [term]), subst, metasenv
@@ -122,7 +120,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
       (match R.whd subst context actualtype with
            C.Prod (name',so',de') ->
              let subst, metasenv = 
-                Un.fo_unif_subst subst context metasenv so so' in
+               fo_unif_subst subst context metasenv so so' in
              let term' =
                (match CicSubstitution.lift 1 term with
                    C.Appl l -> C.Appl (l@[C.Rel 1])
@@ -130,15 +128,14 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
              (* we should also check that the name variable is anonymous in
              the actual type de' ?? *)
              check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de 
-	 | _ -> raise WrongArgumentNumber)
-  | _ -> raise (NotRefinable "Prod or MutInd expected")
+        | _ -> raise (AssertFailure "Wrong number of arguments"))
+   | _ -> raise (AssertFailure "Prod or MutInd expected")
 
 and type_of_aux' metasenv context t =
  let rec type_of_aux subst metasenv context =
   let module C = Cic in
   let module S = CicSubstitution in
   let module U = UriManager in
-  let module Un = CicUnification in
    function
       C.Rel n ->
        (try
@@ -147,18 +144,16 @@ and type_of_aux' metasenv context t =
           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
           | Some (_,C.Def (bo,None)) ->
              type_of_aux subst metasenv context (S.lift n bo)
-	  | None -> raise RelToHiddenHypothesis
+          | None -> raise (RefineFailure "Rel to hidden hypothesis")
         with
-         _ -> raise (NotRefinable "Not a close term")
+         _ -> raise (RefineFailure "Not a close term")
        )
     | C.Var (uri,exp_named_subst) ->
-      incr fdebug ;
       let subst',metasenv' =
        check_exp_named_subst subst metasenv context exp_named_subst in
       let ty =
        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
       in
-       decr fdebug ;
        ty,subst',metasenv'
     | C.Meta (n,l) -> 
        let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
@@ -166,10 +161,16 @@ and type_of_aux' metasenv context t =
          check_metasenv_consistency n subst metasenv context canonical_context l
         in
         CicSubstitution.lift_meta l ty, subst', metasenv'
-    | C.Sort s ->
-       C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
-        subst,metasenv
-    | C.Implicit -> raise (Impossible 21)
+     (* TASSI: CONSTRAINT *)
+    | C.Sort (C.Type t) ->
+        let t' = CicUniv.fresh() in
+        if not (CicUniv.add_gt t' t ) then
+	  assert false (* t' is fresh! an error in CicUniv *)
+	else
+          C.Sort (C.Type t'),subst,metasenv
+     (* TASSI: CONSTRAINT *)
+    | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv
+    | C.Implicit _ -> raise (AssertFailure "21")
     | C.Cast (te,ty) ->
        let _,subst',metasenv' =
         type_of_aux subst metasenv context ty in
@@ -178,11 +179,11 @@ and type_of_aux' metasenv context t =
        in
         (try
           let subst''',metasenv''' =
-           Un.fo_unif_subst subst'' context metasenv'' inferredty ty
+           fo_unif_subst subst'' context metasenv'' inferredty ty
           in
            ty,subst''',metasenv'''
          with
-          _ -> raise (NotRefinable "Cast"))
+          _ -> raise (RefineFailure "Cast"))
     | C.Prod (name,s,t) ->
        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
        let sort2,subst'',metasenv'' =
@@ -191,17 +192,19 @@ and type_of_aux' metasenv context t =
         sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
    | C.Lambda (n,s,t) ->
        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
+       (match CicMetaSubst.whd subst' context sort1 with
+           C.Meta _
+         | C.Sort _ -> ()
+         | _ ->
+           raise (RefineFailure (sprintf
+            "Not well-typed lambda-abstraction: the source %s should be a type;
+             instead it is a term of type %s" (CicPp.ppterm s)
+            (CicPp.ppterm sort1)))
+       ) ;
        let type2,subst'',metasenv'' =
         type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
        in
-        let sort2,subst''',metasenv''' =
-         type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
-        in
-         (* only to check if the product is well-typed *)
-         let _,subst'''',metasenv'''' =
-          sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
-         in
-          C.Prod (n,s,type2),subst'''',metasenv''''
+          C.Prod (n,s,type2),subst'',metasenv''
    | C.LetIn (n,s,t) ->
       (* only to check if s is well-typed *)
       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
@@ -223,25 +226,21 @@ and type_of_aux' metasenv context t =
         ) tl ([],subst',metasenv')
       in
        eat_prods subst'' metasenv'' context hetype tlbody_and_type
-   | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
+   | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
    | C.Const (uri,exp_named_subst) ->
-      incr fdebug ;
       let subst',metasenv' =
        check_exp_named_subst subst metasenv context exp_named_subst in
       let cty =
        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
       in
-       decr fdebug ;
        cty,subst',metasenv'
    | C.MutInd (uri,i,exp_named_subst) ->
-      incr fdebug ;
       let subst',metasenv' =
        check_exp_named_subst subst metasenv context exp_named_subst in
       let cty =
        CicSubstitution.subst_vars exp_named_subst
         (type_of_mutual_inductive_defs uri i)
       in
-       decr fdebug ;
        cty,subst',metasenv'
    | C.MutConstruct (uri,i,j,exp_named_subst) ->
       let subst',metasenv' =
@@ -259,7 +258,8 @@ and type_of_aux' metasenv context t =
               List.nth l i , expl_params, parsno
           | _ ->
             raise
-             (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
+             (RefineFailure
+              ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
        let rec count_prod t =
          match CicMetaSubst.whd subst context t with
              C.Prod (_, _, t) -> 1 + (count_prod t)
@@ -288,7 +288,7 @@ and type_of_aux' metasenv context t =
        in
        let actual_type = CicMetaSubst.whd subst context actual_type in
        let subst,metasenv =
-         Un.fo_unif_subst subst context metasenv expected_type actual_type
+         fo_unif_subst subst context metasenv expected_type actual_type
        in
        (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
        let (_,outtypeinstances,subst,metasenv) =
@@ -314,6 +314,7 @@ and type_of_aux' metasenv context t =
            The easy case is when the outype is specified, that amount
            to a trivial check. Otherwise, we should guess a type from
            its instances *)
+
         (* easy case *)
         let _, subst, metasenv =
           type_of_aux subst metasenv context
@@ -338,7 +339,7 @@ and type_of_aux' metasenv context t =
 *)
                 CicMetaSubst.whd subst context appl
               in
-               Un.fo_unif_subst subst context metasenv instance instance')
+               fo_unif_subst subst context metasenv instance instance')
              (subst,metasenv) outtypeinstances in
         CicMetaSubst.whd subst
           context (C.Appl(outtype::right_args@[term])),subst,metasenv
@@ -358,7 +359,7 @@ and type_of_aux' metasenv context t =
            let ty_of_bo,subst,metasenv =
             type_of_aux subst metasenv context' bo
            in
-            Un.fo_unif_subst subst context' metasenv
+            fo_unif_subst subst context' metasenv
               ty_of_bo (CicMetaSubst.lift subst len ty)
          ) (subst,metasenv) fl in
         let (_,_,ty,_) = List.nth fl i in
@@ -379,7 +380,7 @@ and type_of_aux' metasenv context t =
            let ty_of_bo,subst,metasenv =
             type_of_aux subst metasenv context' bo
            in
-            Un.fo_unif_subst subst context' metasenv
+            fo_unif_subst subst context' metasenv
               ty_of_bo (CicMetaSubst.lift subst len ty)
          ) (subst,metasenv) fl in
       
@@ -411,6 +412,7 @@ and type_of_aux' metasenv context t =
      in
       aux 1 canonical_context
     in
+    try
      List.fold_left2 
       (fun (subst,metasenv) t ct -> 
         match (t,ct) with
@@ -418,22 +420,30 @@ and type_of_aux' metasenv context t =
              subst,metasenv
          | Some t,Some (_,C.Def (ct,_)) ->
             (try
-              CicUnification.fo_unif_subst subst context metasenv t ct
-             with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct))))
+              fo_unif_subst subst context metasenv t ct
+             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)))))
          | Some t,Some (_,C.Decl ct) ->
             let inferredty,subst',metasenv' =
              type_of_aux subst metasenv context t
             in
              (try
-               CicUnification.fo_unif_subst
+               fo_unif_subst
                 subst' context metasenv' inferredty ct
-             with _ -> 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" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct))))
+             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)))))
          | None, Some _  ->
-             raise (NotRefinable (sprintf
+             raise (RefineFailure (sprintf
               "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"
               (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
               (CicMetaSubst.ppcontext subst canonical_context)))
       ) (subst,metasenv) l lifted_canonical_context 
+    with
+     Invalid_argument _ ->
+      raise
+       (RefineFailure
+         (sprintf
+           "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
+             (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
+             (CicMetaSubst.ppcontext subst canonical_context)))
 
  and check_exp_named_subst metasubst metasenv context =
   let rec check_exp_named_subst_aux metasubst metasenv substs =
@@ -445,36 +455,45 @@ and type_of_aux' metasenv context t =
        (match CicEnvironment.get_cooked_obj ~trust:false uri with
            Cic.Variable (_,Some bo,_,_) ->
             raise
-             (NotRefinable
+             (RefineFailure
                "A variable with a body can not be explicit substituted")
          | Cic.Variable (_,None,_,_) -> ()
-         | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+         | _ ->
+           raise
+            (RefineFailure
+             ("Unkown variable definition " ^ UriManager.string_of_uri uri))
        ) ;
        let typeoft,metasubst',metasenv' =
         type_of_aux metasubst metasenv context t
        in
         try
          let metasubst'',metasenv'' =
-          CicUnification.fo_unif_subst
-           metasubst' context metasenv' typeoft typeofvar
+          fo_unif_subst metasubst' context metasenv' typeoft typeofvar
          in
           check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
         with _ ->
-         raise (NotRefinable "Wrong Explicit Named Substitution")
+         raise (RefineFailure "Wrong Explicit Named Substitution")
   in
    check_exp_named_subst_aux metasubst metasenv []
 
  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
   let module C = Cic in
+    let context_for_t2 = (Some (name,C.Decl s))::context in
     let t1'' = CicMetaSubst.whd subst context t1 in
-    let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2 in
+    let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
     match (t1'', t2'') with
        (C.Sort s1, C.Sort s2)
          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
           C.Sort s2,subst,metasenv
-     | (C.Sort s1, C.Sort s2) ->
-         (*CSC manca la gestione degli universi!!! *)
-         C.Sort C.Type,subst,metasenv
+     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
+       (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
+       let t' = CicUniv.fresh() in
+       if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
+         assert false ; (* not possible, error in CicUniv *)
+       C.Sort (C.Type t'),subst,metasenv
+     | (C.Sort _,C.Sort (C.Type t1)) -> 
+       (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
+	C.Sort (C.Type t1),subst,metasenv
      | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
      | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
          (* TODO how can we force the meta to become a sort? If we don't we
@@ -483,19 +502,77 @@ and type_of_aux' metasenv context t =
           * likely to know the exact value of the result e.g. if the rhs is a
           * Sort (Prop | Set | CProp) then the result is the rhs *)
          let (metasenv,idx) =
-          CicMkImplicit.mk_implicit metasenv [] in
+          CicMkImplicit.mk_implicit_sort metasenv in
          let (subst, metasenv) =
-          CicUnification.fo_unif_subst subst context metasenv
-           (C.Meta (idx,[])) t2''
+           fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
          in
           t2'',subst,metasenv
      | (_,_) ->
-         raise (NotRefinable (sprintf
-          "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
+         raise (RefineFailure (sprintf
+          "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
           (CicPp.ppterm t2'')))
 
  and eat_prods subst metasenv context hetype tlbody_and_type =
+ let rec mk_prod metasenv context =
+  function
+     [] ->
+       let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
+       let irl =
+        CicMkImplicit.identity_relocation_list_for_metavariable context
+       in
+        metasenv,Cic.Meta (idx, irl)
+   | (_,argty)::tl ->
+      let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
+      let irl =
+       CicMkImplicit.identity_relocation_list_for_metavariable context
+      in
+       let meta = Cic.Meta (idx,irl) in
+       let name =
+        (* The name must be fresh for context.                 *)
+        (* Nevertheless, argty is well-typed only in context.  *)
+        (* Thus I generate a name (name_hint) in context and   *)
+        (* then I generate a name --- using the hint name_hint *)
+        (* --- that is fresh in (context'@context).            *)
+        let name_hint =
+         FreshNamesGenerator.mk_fresh_name
+          (CicMetaSubst.apply_subst_metasenv subst metasenv)
+          (CicMetaSubst.apply_subst_context subst context)
+          Cic.Anonymous
+          (CicMetaSubst.apply_subst subst argty)
+        in
+         (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+         FreshNamesGenerator.mk_fresh_name
+          [] context name_hint (Cic.Sort Cic.Prop)
+       in
+       let metasenv,target =
+        mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+       in
+        metasenv,Cic.Prod (name,meta,target)
+ in
+  let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
+  let (subst, metasenv) =
+   fo_unif_subst subst context metasenv hetype hetype'
+  in
+   let rec eat_prods metasenv subst context hetype =
+      function
+         [] -> metasenv,subst,hetype
+       | (hete, hety)::tl ->
+        (match hetype with
+            Cic.Prod (n,s,t) ->
+              let subst,metasenv =
+               fo_unif_subst subst context metasenv hety s
+              in
+               eat_prods metasenv subst context
+                (CicMetaSubst.subst subst hete t) tl
+          | _ -> assert false
+        )
+   in
+    let metasenv,subst,t =
+     eat_prods metasenv subst context hetype' tlbody_and_type
+    in
+     t,subst,metasenv
+(*
   let rec aux context' args (resty,subst,metasenv) =
    function
       [] -> resty,subst,metasenv
@@ -526,7 +603,7 @@ and type_of_aux' metasenv context t =
        in
        let context'' = Some (name, Cic.Decl argty') :: context' in
        let (metasenv, idx) =
-        CicMkImplicit.mk_implicit metasenv (context'' @ context) in
+        CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
        let irl =
          (Some (Cic.Rel 1))::args' @
           (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
@@ -536,13 +613,13 @@ and type_of_aux' metasenv context t =
        let prod = Cic.Prod (name, argty, newmeta) in
        let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
        let (subst, metasenv) =
-         CicUnification.fo_unif_subst subst context metasenv resty prod
+         fo_unif_subst subst context metasenv resty prod
        in
         aux context'' (Some arg :: args)
          (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
   in
    aux [] [] (hetype,subst,metasenv) tlbody_and_type
-
+*)
  in
   let ty,subst',metasenv' =
    type_of_aux [] metasenv context t
@@ -597,16 +674,10 @@ let type_of_aux' metasenv context term =
 *)
    (t,ty,m)
  with
- | CicUnification.AssertFailure msg as e ->
-     debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
-     debug_print msg;
+ | RefineFailure msg as e ->
+     debug_print ("@@@ REFINE FAILED: " ^ msg);
      raise e
- | CicUnification.UnificationFailure msg as e ->
-     debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
-     debug_print msg;
+ | Uncertain msg as e ->
+     debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
      raise e
- | e ->
-   debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
-   raise e
 ;;
-