X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=fce4e7f48633a6ecc1070b19798f5ebf9d3437cb;hb=b1fb6b8e1767d775bc452303629e95941d142bea;hp=fafbd884845ee5465d555860647eed8002fa24e0;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index fafbd8848..fce4e7f48 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -37,6 +37,7 @@
 (******************************************************************************)
 
 exception CicPpInternalError;;
+exception NotEnoughElements;;
 
 (* Utility functions *)
 
@@ -46,13 +47,13 @@ let string_of_name =
   | Cic.Anonimous  -> "_"
 ;;
 
-(* get_nth l n   returns the nth element of the list l if it exists or raise *)
-(* a CicPpInternalError if l has less than n elements or n < 1               *)
+(* get_nth l n   returns the nth element of the list l if it exists or *)
+(* raises NotEnoughElements if l has less than n elements             *)
 let rec get_nth l n =
  match (n,l) with
     (1, he::_) -> he
   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
-  | (_,_) -> raise CicPpInternalError
+  | (_,_) -> raise NotEnoughElements
 ;;
 
 (* pp t l                                                                  *)
@@ -63,12 +64,21 @@ let rec pp t l =
  let module C = Cic in
    match t with
       C.Rel n ->
-       (match get_nth l n with
-           C.Name s -> s
-         | _        -> raise CicPpInternalError
-       )
+       begin
+        try
+         (match get_nth l n with
+             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"
@@ -78,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
@@ -93,22 +103,34 @@ let rec pp t l =
         li ""
        ) ^ ")"
     | C.Const (uri,_) -> UriManager.name_of_uri uri
-    | C.Abst uri -> UriManager.name_of_uri uri
     | C.MutInd (uri,_,n) ->
-       (match CicEnvironment.get_obj uri with
-           C.InductiveDefinition (dl,_,_) ->
-            let (name,_,_,_) = get_nth dl (n+1) in
-             name
-         | _ -> raise CicPpInternalError
-       )
+       begin
+        try
+         (match CicEnvironment.get_obj uri with
+             C.InductiveDefinition (dl,_,_) ->
+              let (name,_,_,_) = get_nth dl (n+1) in
+               name
+           | _ -> raise CicPpInternalError
+         )
+        with
+         NotEnoughElements ->
+          UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
+       end
     | C.MutConstruct (uri,_,n1,n2) ->
-       (match CicEnvironment.get_obj uri with
-           C.InductiveDefinition (dl,_,_) ->
-            let (_,_,_,cons) = get_nth dl (n1+1) in
-             let (id,_,_) = get_nth cons n2 in
-              id
-         | _ -> raise CicPpInternalError
-       )
+       begin
+        try
+         (match CicEnvironment.get_obj uri with
+             C.InductiveDefinition (dl,_,_) ->
+              let (_,_,_,cons) = get_nth dl (n1+1) in
+               let (id,_,_) = get_nth cons n2 in
+                id
+           | _ -> raise CicPpInternalError
+         )
+        with
+         NotEnoughElements ->
+          UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
+           string_of_int n2
+       end
     | C.MutCase (uri,_,n1,ty,te,patterns) ->
        let connames =
         (match CicEnvironment.get_obj uri with
@@ -124,7 +146,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 ^
@@ -134,7 +158,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 ^ 
@@ -144,6 +170,10 @@ let rec pp t l =
          "}\n"
 ;;
 
+let ppterm t =
+ pp t []
+;;
+
 (* ppinductiveType (typename, inductive, arity, cons) names                 *)
 (* pretty-prints a single inductive definition (typename, inductive, arity, *)
 (*  cons) where the cic terms in the inductive definition need to be        *)
@@ -192,10 +222,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
@@ -206,6 +255,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 ""
 ;;