X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=d9c669ed570e318173056744488fa88b58ab4876;hb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;hp=d3f7f0f60b181f7ccdcc02de45176079e92300dc;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index d3f7f0f60..d9c669ed5 100644
--- 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,25 +79,27 @@ 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"
+         (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
+	 | 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)
         | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
        )
-    | C.Cast (v,t) -> pp v l
+    | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t 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
@@ -108,8 +110,8 @@ let rec pp t l =
        UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
     | C.MutInd (uri,n,exp_named_subst) ->
        (try
-         match CicEnvironment.get_obj uri with
-            C.InductiveDefinition (dl,_,_) ->
+         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+            C.InductiveDefinition (dl,_,_,_) ->
              let (name,_,_,_) = get_nth dl (n+1) in
               name ^ pp_exp_named_subst exp_named_subst l
           | _ -> raise CicPpInternalError
@@ -118,8 +120,8 @@ let rec pp t l =
        )
     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
        (try
-         match CicEnvironment.get_obj uri with
-            C.InductiveDefinition (dl,_,_) ->
+         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+            C.InductiveDefinition (dl,_,_,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
               let (id,_) = get_nth cons n2 in
                id ^ pp_exp_named_subst exp_named_subst l
@@ -131,8 +133,8 @@ let rec pp t l =
        )
     | C.MutCase (uri,n1,ty,te,patterns) ->
        let connames =
-        (match CicEnvironment.get_obj uri with
-            C.InductiveDefinition (dl,_,_) ->
+        (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+            C.InductiveDefinition (dl,_,_,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
               List.map (fun (id,_) -> id) cons
           | _ -> raise CicPpInternalError
@@ -192,27 +194,45 @@ let ppinductiveType (typename, inductive, arity, cons) =
    cons ""
 ;;
 
+let ppcontext ?(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
+      | 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
+       | None ->
+          Printf.sprintf "%s_ :? _" (separate i), None::name_context
+    ) context ("",[]))
+
 (* ppobj obj  returns a string with describing the cic object obj in a syntax *)
 (* similar to the one used by Coq                                             *)
 let ppobj obj =
  let module C = Cic in
  let module U = UriManager in
   match obj with
-    C.Constant (name, Some t1, t2, params) ->
+    C.Constant (name, Some t1, t2, params, _) ->
       "Definition of " ^ name ^
        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
        ")" ^ ":\n" ^ pp t1 [] ^ " : " ^ pp t2 []
-   | C.Constant (name, None, ty, params) ->
+   | C.Constant (name, None, ty, params, _) ->
       "Axiom " ^ name ^
        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
        "):\n" ^ pp ty []
-   | C.Variable (name, bo, ty, params) ->
+   | C.Variable (name, bo, ty, params, _) ->
       "Variable " ^ name ^
        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
        ")" ^ ":\n" ^
        pp ty [] ^ "\n" ^
        (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
-   | C.CurrentProof (name, conjectures, value, ty, params) ->
+   | C.CurrentProof (name, conjectures, value, ty, params, _) ->
       "Current Proof of " ^ name ^
        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
        ")" ^ ":\n" ^
@@ -220,28 +240,36 @@ 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
         ) conjectures "" ^
         "\n" ^ pp value [] ^ " : " ^ pp ty [] 
-   | C.InductiveDefinition (l, params, nparams) ->
+   | C.InductiveDefinition (l, params, nparams, _) ->
       "Parameters = " ^
        String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
        "NParams = " ^ string_of_int nparams ^ "\n" ^
         List.fold_right (fun x i -> ppinductiveType x ^ i) l ""
 ;;
+
+let ppsort = function
+  | Cic.Prop -> "Prop"
+  | Cic.Set -> "Set"
+  | Cic.Type _ -> "Type"
+  | Cic.CProp -> "CProp"
+