Big changes:

  1. every level now catches the *Failure excecptions of the lower level
     and converts it to its own *Failure. The same for *Uncertain.
  2. CicMetaSubst.delift now raises also Uncertain (that is converted
     to CicUnification.Uncertain and then to CicRefine.Uncertain).

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index a19bb2b25e405a83b6de8026c0c7b9b2f9795c9d..96b38e424970161afcbd301424eee55079f4adee 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -1,8 +1,33 @@
+(* Copyright (C) 2004, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
 
 open Printf
 
-exception AssertFailure of string
 exception MetaSubstFailure of string
+exception Uncertain of string
+exception AssertFailure of string
 
 let debug_print = prerr_endline
 
@@ -567,8 +592,9 @@ let delift n subst context metasenv l t =
       (* The reason is that our delift function is weaker than first  *)
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
-debug_print "!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
-      raise (MetaSubstFailure (sprintf
+debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
+print_endline "\nCicMetaSubst: UNCERTAIN" ;
+      raise (Uncertain (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)
         (String.concat "; "

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index 6034853da84dac5e612ec67946e90579aa43fcec..2ee78a7a443d4989973728c2f062b87041beafdf 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -23,8 +23,9 @@
  * http://helm.cs.unibo.it/
  *)
 
-exception AssertFailure of string
 exception MetaSubstFailure of string
+exception Uncertain of string
+exception AssertFailure of string
 
 (* The entry (i,t) in a substitution means that *)
 (* (META i) have been instantiated with t.      *)

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index fbbb10a6eefecebf6af669bf81e41be57330d8c1..8935d867c570628f4f80d70eac72e9c30ce564cd 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -37,20 +37,16 @@ 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*)
-;;
-
 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)
@@ -122,7 +118,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])
@@ -152,13 +148,11 @@ and type_of_aux' metasenv context t =
          _ -> raise (NotRefinable "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
@@ -178,7 +172,7 @@ 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
@@ -225,23 +219,19 @@ and type_of_aux' metasenv context t =
        eat_prods subst'' metasenv'' context hetype tlbody_and_type
    | C.Appl _ -> raise (NotRefinable "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' =
@@ -288,7 +278,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) =
@@ -338,7 +328,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 +348,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 +369,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
       
@@ -418,14 +408,14 @@ 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
+              fo_unif_subst subst context metasenv t ct
              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)))))
          | 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 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)))))
          | None, Some _  ->
@@ -455,8 +445,7 @@ and type_of_aux' 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 _ ->
@@ -486,8 +475,7 @@ and type_of_aux' metasenv context t =
          let (metasenv,idx) =
           CicMkImplicit.mk_implicit_sort metasenv in
          let (subst, metasenv) =
-          CicUnification.fo_unif_subst subst context_for_t2 metasenv
-           (C.Meta (idx,[])) t2''
+           fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
          in
           t2'',subst,metasenv
      | (_,_) ->
@@ -537,7 +525,7 @@ 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
@@ -602,10 +590,6 @@ let type_of_aux' metasenv context term =
      debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
      debug_print msg;
      raise e
- | CicUnification.UnificationFailure msg as e ->
-     debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
-     debug_print msg;
-     raise e
  | e ->
    debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
    raise e

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 3c8b077297fd5ad8da82700f4dd081fade124c19..bf035d74af217985f3a32f70126eed6afa133c4f 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -25,8 +25,9 @@
 
 open Printf
 
-exception AssertFailure of string;;
 exception UnificationFailure of string;;
+exception Uncertain of string;;
+exception AssertFailure of string;;
 
 let debug_print = prerr_endline
 
@@ -96,7 +97,11 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
           fo_unif_subst subst context metasenv lifted_oldt t
         with Not_found ->
          let t',metasenv',subst' =
+          try
            CicMetaSubst.delift n subst context metasenv l t
+          with
+             (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
+           | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
          in
           (n, t')::subst', metasenv'
        in

diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli
index 40b9f8ef78b2892d2d4f6ddc9bf39f30cff88846..9956b304378c40d7769378fafd5ffbf344de6855 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.mli
+++ b/helm/ocaml/cic_unification/cicUnification.mli
@@ -23,8 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception AssertFailure of string
-exception UnificationFailure of string
+exception UnificationFailure of string;;
+exception Uncertain of string;;
+exception AssertFailure of string;;
 
 (* fo_unif metasenv context t1 t2                *)
 (* unifies [t1] and [t2] in a context [context]. *)