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 22b15f9eefc5b37e8f5cf22ed78a7e9eaae66c59..30069cdfec88d12f6549922d14d0c1a6561adf90 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -51,24 +51,24 @@ let rec force_does_not_occur subst to_be_restricted t =
     | C.Sort _ as t -> t
     | C.Implicit -> assert false
     | C.Meta (n, l) ->
-        (try
-          aux k (CicSubstitution.lift_meta l (List.assoc n subst))
-        with Not_found ->
-          let l' =
-            let i = ref 0 in
-            List.map
-              (function
-                | None -> None
-                | Some t ->
-                    incr i;
-                    try
-                      Some (aux k t)
-                    with Occur ->
-                      more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
-                      None)
-              l
-          in
-          C.Meta (n, l'))
+       (* we do not retrieve the term associated to ?n in subst since *)
+       (* in this way we can restrict if something goes wrong         *)
+       let l' =
+         let i = ref 0 in
+         List.map
+           (function t ->
+             incr i ;
+             match t with
+                None -> None
+              | Some t ->
+                 try
+                   Some (aux k t)
+                 with Occur ->
+                   more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
+                   None)
+           l
+       in
+        C.Meta (n, l')
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
     | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
     | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
@@ -476,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))