ppcontext (and thus also ppmetasenv) were buggy: the occurrences of a variable

[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 637c346b06972b7dcc747ff4298414c2824e2899..30069cdfec88d12f6549922d14d0c1a6561adf90 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -56,10 +56,11 @@ let rec force_does_not_occur subst to_be_restricted t =
        let l' =
          let i = ref 0 in
          List.map
-           (function
-             | None -> None
-             | Some t ->
-                 incr i;
+           (function t ->
+             incr i ;
+             match t with
+                None -> None
+              | Some t ->
                  try
                    Some (aux k t)
                  with Occur ->
@@ -475,25 +476,36 @@ let apply_subst_metasenv subst metasenv =
 
 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
-let ppcontext ?(sep = "\n") subst context =
-  String.concat sep
-    (List.rev_map (function
-      | Some (n, Cic.Decl t) ->
-          sprintf "%s : %s" (CicPp.ppname n) (ppterm subst t)
-      | Some (n, Cic.Def (t, ty)) ->
-          sprintf "%s : %s := %s"
-            (CicPp.ppname n)
-            (match ty with None -> "_" | Some ty -> ppterm subst ty)
-            (ppterm subst t)
-      | None -> "_")
-      context)
+let ppterm_in_context subst term name_context =
+ CicPp.pp (apply_subst subst term) name_context
+
+let ppcontext' ?(sep = "\n") subst context =
+ let separate s = if s = "" then "" else s ^ sep in
+  List.fold_right 
+   (fun context_entry (i,name_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
+      | 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
+       | None ->
+          sprintf "%s_ :? _" (separate i), None::name_context
+    ) context ("",[])
+
+let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
 
 let ppmetasenv ?(sep = "\n") metasenv subst =
   String.concat sep
     (List.map
       (fun (i, c, t) ->
-        sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i
-          (ppterm subst t))
+        let context,name_context = ppcontext' ~sep:"; " subst c in
+         sprintf "%s |- ?%d: %s" context i
+          (ppterm_in_context subst t name_context))
       (List.filter
         (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
         metasenv))