Universes introduction

[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 d3f7f0f60b181f7ccdcc02de45176079e92300dc..8172b47f7ac92ce9a9fdee3fada7775cc048c84d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -41,7 +41,7 @@ exception NotEnoughElements;;
 
 (* Utility functions *)
 
-let string_of_name =
+let ppname =
  function
     Cic.Name s     -> s
   | Cic.Anonymous  -> "_"
@@ -69,7 +69,7 @@ let rec pp t l =
          (match get_nth l n with
              Some (C.Name s) -> s
            | Some C.Anonymous -> "__" ^ string_of_int n
-           | _ -> raise CicPpInternalError
+           | None -> "_hidden_" ^ string_of_int n
          )
         with
          NotEnoughElements -> string_of_int (List.length l - n)
@@ -79,15 +79,16 @@ let rec pp t l =
     | C.Meta (n,l1) ->
        "?" ^ (string_of_int n) ^ "[" ^ 
         String.concat " ; "
-         (List.map (function None -> "_" | Some t -> pp t l) l1) ^
+         (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
         "]"
     | C.Sort s ->
        (match s with
-           C.Prop -> "Prop"
-         | C.Set  -> "Set"
-         | C.Type -> "Type"
+           C.Prop  -> "Prop"
+         | C.Set   -> "Set"
+         | C.Type _ -> "Type" (* TASSI: universe is not explicit *)
+        | C.CProp -> "CProp" 
        )
-    | C.Implicit -> "?"
+    | C.Implicit _ -> "?"
     | C.Prod (b,s,t) ->
        (match b with
           C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
@@ -95,9 +96,9 @@ let rec pp t l =
        )
     | C.Cast (v,t) -> pp v l
     | C.Lambda (b,s,t) ->
-       "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+       "[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
     | C.LetIn (b,s,t) ->
-       "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+       "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
     | C.Appl li ->
        "(" ^
        (List.fold_right
@@ -220,20 +221,21 @@ let ppobj obj =
        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) ->
+                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) ->
+                     ppname n ^ ":" ^ pp at name_context ^ " ",
+                      (Some n)::name_context
+                     | Some (n,C.Def (at,None)) ->
                    (separate i) ^
-                    string_of_name n ^ ":= " ^ pp at name_context ^ " ",
-                   (Some n)::name_context
+                     ppname n ^ ":= " ^ pp at name_context ^ " ",
+                      (Some n)::name_context
                 | None ->
-                   (separate i) ^ "_ :? _ ", None::name_context)
-             ) context ("",[])
+                   (separate i) ^ "_ :? _ ", None::name_context
+                | _ -> assert false)
+            ) context ("",[])
           in
            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
             pp t name_context ^ "\n" ^ i