New experimental commit: metavariables representation is changed again,

[helm.git] / helm / ocaml / cic_proof_checking / cicPp.ml

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 745a203a497e9c63de3241129bef2aa9c7a7ad28..07e306b0be83e167708dd4a05266205e166bbeb1 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -67,14 +67,18 @@ let rec pp t l =
        begin
         try
          (match get_nth l n with
-             C.Name s -> s
+             Some (C.Name s) -> s
            | _        -> raise CicPpInternalError
          )
         with
          NotEnoughElements -> string_of_int (List.length l - n)
        end
     | C.Var uri -> UriManager.name_of_uri uri
-    | C.Meta n -> "?" ^ (string_of_int n)
+    | C.Meta (n,l1) ->
+       "?" ^ (string_of_int n) ^ "[" ^ 
+        String.concat " ; "
+         (List.map (function None -> "_" | Some t -> pp t l) l1) ^
+        "]"
     | C.Sort s ->
        (match s with
            C.Prop -> "Prop"
@@ -84,14 +88,14 @@ let rec pp t l =
     | C.Implicit -> "?"
     | C.Prod (b,s,t) ->
        (match b with
-          C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t (b::l)
-        | C.Anonimous -> "(" ^ pp s l ^ "->" ^ pp t (b::l) ^ ")"
+          C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
+        | C.Anonimous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
        )
     | C.Cast (v,t) -> pp v l
     | C.Lambda (b,s,t) ->
-       "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t (b::l)
+       "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
     | C.LetIn (b,s,t) ->
-       "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t (b::l)
+       "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
     | C.Appl li ->
        "(" ^
        (List.fold_right
@@ -130,7 +134,9 @@ let rec pp t l =
           "\nend"
     | C.Fix (no, funs) ->
        let snames = List.map (fun (name,_,_,_) -> name) funs in
-        let names = List.rev (List.map (function name -> C.Name name) snames) in
+        let names =
+         List.rev (List.map (function name -> Some (C.Name name)) snames)
+        in
          "\nFix " ^ get_nth snames (no + 1) ^ " {" ^
          List.fold_right
           (fun (name,ind,ty,bo) i -> "\n" ^ name ^ " / " ^ string_of_int ind ^
@@ -140,7 +146,9 @@ let rec pp t l =
          "}\n"
     | C.CoFix (no,funs) ->
        let snames = List.map (fun (name,_,_) -> name) funs in
-        let names = List.rev (List.map (function name -> C.Name name) snames) in
+        let names =
+         List.rev (List.map (function name -> Some (C.Name name)) snames)
+        in
          "\nCoFix " ^ get_nth snames (no + 1) ^ " {" ^
          List.fold_right
           (fun (name,ty,bo) i -> "\n" ^ name ^ 
@@ -202,10 +210,29 @@ let ppobj obj =
       (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
    | C.CurrentProof (name, conjectures, value, ty) ->
       "Current Proof:\n" ^
-      List.fold_right
-       (fun (n, t) i -> "?" ^ (string_of_int n) ^ ": " ^ pp t [] ^ "\n" ^ i)
-       conjectures "" ^
-      "\n" ^ pp value [] ^ " : " ^ pp ty [] 
+      let separate s = if s = "" then "" else s ^ " ; " in
+       List.fold_right
+        (fun (n, context, t) i -> 
+          let conjectures',name_context =
+          List.fold_right 
+           (fun context_entry (i,name_context) ->
+             (match context_entry with
+                 Some (n,C.Decl at) ->
+                   (separate i) ^
+                    string_of_name n ^ ":" ^ pp at name_context ^ " ",
+                   (Some n)::name_context
+               | Some (n,C.Def at) ->
+                   (separate i) ^
+                    string_of_name n ^ ":= " ^ pp at name_context ^ " ",
+                   (Some n)::name_context
+                | None ->
+                   (separate i) ^ "_ :? _ ", None::name_context)
+             ) context ("",[])
+          in
+           conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
+            pp t name_context ^ "\n" ^ i
+        ) conjectures "" ^
+        "\n" ^ pp value [] ^ " : " ^ pp ty [] 
    | C.InductiveDefinition (l, params, nparams) ->
       "Parameters = " ^
       List.fold_right
@@ -216,6 +243,6 @@ let ppobj obj =
           ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
        ) params "" ^ "\n" ^
       "NParams = " ^ string_of_int nparams ^ "\n" ^
-      let names = List.rev (List.map (fun (n,_,_,_) -> C.Name n) l) in
+      let names = List.rev (List.map (fun (n,_,_,_) -> Some (C.Name n)) l) in
        List.fold_right (fun x i -> ppinductiveType x names ^ i) l ""
 ;;