Big changes:

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

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