...

[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 fafbd884845ee5465d555860647eed8002fa24e0..07e306b0be83e167708dd4a05266205e166bbeb1 100644 (file)
--- 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
@@ -124,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 ^
@@ -134,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 ^ 
@@ -144,6 +158,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 +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
@@ -206,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 ""
 ;;