ocaml 3.09 transition

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

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 614faf6df15f50d6af219ac90ccacf502afd04fb..718951c68a579756e4c4bd1d0994c835d28e2bac 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -68,9 +68,9 @@ context length: %d (avg = %.2f)
 
 
 
-exception MetaSubstFailure of string
-exception Uncertain of string
-exception AssertFailure of string
+exception MetaSubstFailure of string Lazy.t
+exception Uncertain of string Lazy.t
+exception AssertFailure of string Lazy.t
 exception DeliftingARelWouldCaptureAFreeVariable;;
 
 let debug_print = fun _ -> ()
@@ -191,8 +191,8 @@ let apply_subst_gen ~appl_fun subst term =
             List.map (function None -> None | Some t -> Some (um_aux t)) l
           in
            C.Meta (i,l'))
-    | C.Sort _ as t -> t
-    | C.Implicit _ -> assert false
+    | C.Sort _
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
@@ -288,9 +288,15 @@ let apply_subst_metasenv subst metasenv =
 
 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
-let ppterm_in_context subst term name_context =
+let ppterm_in_name_context subst term name_context =
  CicPp.pp (apply_subst subst term) name_context
 
+let ppterm_in_context subst term context =
+ let name_context =
+  List.map (function None -> None | Some (n,_) -> Some n) context
+ in
+  ppterm_in_name_context subst term name_context
+
 let ppcontext' ?(sep = "\n") subst context =
  let separate s = if s = "" then "" else s ^ sep in
   List.fold_right 
@@ -298,13 +304,13 @@ let ppcontext' ?(sep = "\n") subst context =
      match context_entry with
         Some (n,Cic.Decl t) ->
          sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
-          (ppterm_in_context subst t name_context), (Some n)::name_context
+          (ppterm_in_name_context subst t name_context), (Some n)::name_context
       | Some (n,Cic.Def (bo,ty)) ->
          sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
           (match ty with
               None -> "_"
-            | Some ty -> ppterm_in_context subst ty name_context)
-          (ppterm_in_context subst bo name_context), (Some n)::name_context
+            | Some ty -> ppterm_in_name_context subst ty name_context)
+          (ppterm_in_name_context subst bo name_context), (Some n)::name_context
        | None ->
           sprintf "%s_ :? _" (separate i), None::name_context
     ) context ("",[])
@@ -315,7 +321,7 @@ let ppsubst_unfolded subst =
       (fun (idx, (c, t,_)) ->
         let context,name_context = ppcontext' ~sep:"; " subst c in
          sprintf "%s |- ?%d:= %s" context idx
-          (ppterm_in_context subst t name_context))
+          (ppterm_in_name_context subst t name_context))
        subst)
 (* 
         Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
@@ -328,7 +334,7 @@ let ppsubst subst =
       (fun (idx, (c, t, _)) ->
         let context,name_context = ppcontext' ~sep:"; " [] c in
          sprintf "%s |- ?%d:= %s" context idx
-          (ppterm_in_context [] t name_context))
+          (ppterm_in_name_context [] t name_context))
        subst)
 ;;
 
@@ -340,7 +346,7 @@ let ppmetasenv ?(sep = "\n") subst metasenv =
       (fun (i, c, t) ->
         let context,name_context = ppcontext' ~sep:"; " subst c in
          sprintf "%s |- ?%d: %s" context i
-          (ppterm_in_context subst t name_context))
+          (ppterm_in_name_context subst t name_context))
       (List.filter
         (fun (i, _, _) -> not (List.mem_assoc i subst))
         metasenv))
@@ -536,10 +542,10 @@ let rec restrict subst to_be_restricted metasenv =
           (more @ more_to_be_restricted @ more_to_be_restricted',
           metasenv')
         with Occur ->
-          raise (MetaSubstFailure (sprintf
+          raise (MetaSubstFailure (lazy (sprintf
             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
-           n (names_of_context_indexes context to_be_restricted)))) 
-      metasenv ([], []) 
+           n (names_of_context_indexes context to_be_restricted)))))
+      metasenv ([], [])
   in
   let (more_to_be_restricted', subst) = (* restrict subst *)
     List.fold_right
@@ -567,10 +573,10 @@ let rec restrict subst to_be_restricted metasenv =
            @ more_to_be_restricted'@more_to_be_restricted'' in
           (more, subst')
         with Occur ->
-          let error_msg = sprintf
+          let error_msg = lazy (sprintf
             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
             n (names_of_context_indexes context to_be_restricted) n
-            (ppterm subst term)
+            (ppterm subst term))
          in 
           (* DEBUG
           debug_print (lazy error_msg);
@@ -623,10 +629,10 @@ let delift n subst context metasenv l t =
                 deliftaux k (S.lift m t)
              | Some (_,C.Decl t) ->
                 C.Rel ((position (m-k) l) + k)
-             | None -> raise (MetaSubstFailure "RelToHiddenHypothesis")
+             | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
            with
             Failure _ ->
-             raise (MetaSubstFailure "Unbound variable found in deliftaux")
+             raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
           )
      | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
@@ -640,9 +646,9 @@ let delift n subst context metasenv l t =
          with CicUtil.Subst_not_found _ ->
            (* see the top level invariant *)
            if (i = n) then 
-            raise (MetaSubstFailure (sprintf
+            raise (MetaSubstFailure (lazy (sprintf
               "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
-              i (ppterm subst t))) 
+              i (ppterm subst t))))
           else
             begin
            (* I do not consider the term associated to ?i in subst since *)
@@ -724,13 +730,13 @@ debug_print(lazy (sprintf
           (List.map
             (function Some t -> ppterm subst t | None -> "_") l
           )))); *)
-      raise (Uncertain (sprintf
+      raise (Uncertain (lazy (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)
         (String.concat "; "
           (List.map
             (function Some t -> ppterm subst t | None -> "_")
-            l))))
+            l)))))
    in
    let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
     res, metasenv, subst