X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicPp.ml;h=55d94899bc1b95ddae34462f38da2848775a4886;hb=7e30c63fcf9f9fe1780ba7aa4d95fd0d8658548b;hp=f3560cc3afe2733757f6fac1694a3c59328f7ec6;hpb=07e176d2d2355cea8c5b9990cbbc3c7d234bfe15;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index f3560cc3a..55d94899b 100644
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -62,6 +62,7 @@ let rec get_nth l n =
 (* pretty-prints a term t of cic in an environment l where l is a list of  *)
 (* identifier names used to resolve DeBrujin indexes. The head of l is the *)
 (* name associated to the greatest DeBrujin index in t                     *)
+let pp ?metasenv =
 let rec pp t l =
  let module C = Cic in
    match t with
@@ -79,10 +80,33 @@ let rec pp t l =
     | C.Var (uri,exp_named_subst) ->
        UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
     | C.Meta (n,l1) ->
-       "?" ^ (string_of_int n) ^ "[" ^ 
-        String.concat " ; "
-         (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
-        "]"
+       (match metasenv with
+           None ->
+            "?" ^ (string_of_int n) ^ "[" ^ 
+             String.concat " ; "
+              (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+             "]"
+         | Some metasenv ->
+            try
+             let _,context,_ = CicUtil.lookup_meta n metasenv in
+              "?" ^ (string_of_int n) ^ "[" ^ 
+               String.concat " ; "
+                (List.rev
+                  (List.map2
+                    (fun x y ->
+                      match x,y with
+                         _, None
+                       | None, _ -> "_"
+                       | Some _, Some t -> pp t l
+                    ) context l1)) ^
+               "]"
+            with
+             CicUtil.Meta_not_found _ ->
+              "???" ^ (string_of_int n) ^ "[" ^ 
+               String.concat " ; "
+                (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+               "]"
+       )
     | C.Sort s ->
        (match s with
            C.Prop  -> "Prop"
@@ -223,10 +247,12 @@ and pp_exp_named_subst exp_named_subst l =
      (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t l)
      exp_named_subst
    ) ^ "]"
+in
+ pp
 ;;
 
-let ppterm t =
- pp t []
+let ppterm ?metasenv t =
+ pp ?metasenv t []
 ;;
 
 (* ppinductiveType (typename, inductive, arity, cons)                       *)
@@ -241,20 +267,20 @@ let ppinductiveType (typename, inductive, arity, cons) =
    cons ""
 ;;
 
-let ppcontext ?(sep = "\n") context =
+let ppcontext ?metasenv ?(sep = "\n") context =
  let separate s = if s = "" then "" else s ^ sep in
  fst (List.fold_right 
    (fun context_entry (i,name_context) ->
      match context_entry with
         Some (n,Cic.Decl t) ->
          Printf.sprintf "%s%s : %s" (separate i) (ppname n)
-          (pp t name_context), (Some n)::name_context
+          (pp ?metasenv t name_context), (Some n)::name_context
       | Some (n,Cic.Def (bo,ty)) ->
          Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
           (match ty with
               None -> "_"
-            | Some ty -> pp ty name_context)
-          (pp bo name_context), (Some n)::name_context
+            | Some ty -> pp ?metasenv ty name_context)
+          (pp ?metasenv bo name_context), (Some n)::name_context
        | None ->
           Printf.sprintf "%s_ :? _" (separate i), None::name_context
     ) context ("",[]))
@@ -292,11 +318,13 @@ let ppobj obj =
 	            (match context_entry with
 	                Some (n,C.Decl at) ->
                    (separate i) ^
-                     ppname n ^ ":" ^ pp at name_context ^ " ",
+                     ppname n ^ ":" ^
+                      pp ~metasenv:conjectures at name_context ^ " ",
                       (Some n)::name_context
 	              | Some (n,C.Def (at,None)) ->
                    (separate i) ^
-                     ppname n ^ ":= " ^ pp at name_context ^ " ",
+                     ppname n ^ ":= " ^ pp ~metasenv:conjectures
+                      at name_context ^ " ",
                       (Some n)::name_context
                 | None ->
                    (separate i) ^ "_ :? _ ", None::name_context
@@ -304,9 +332,10 @@ let ppobj obj =
             ) context ("",[])
           in
            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
-            pp t name_context ^ "\n" ^ i
+            pp ~metasenv:conjectures t name_context ^ "\n" ^ i
         ) conjectures "" ^
-        "\n" ^ pp value [] ^ " : " ^ pp ty [] 
+        "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^
+          pp ~metasenv:conjectures ty [] 
    | C.InductiveDefinition (l, params, nparams, _) ->
       "Parameters = " ^
        String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^