1. Some warnings about unused warning fixed (hopefully well)

2. We now try to print the MutCase in the new syntax.
   This fails silently when the type of the constructor is not a spine of Prods
   ended by something not convertible to another Prod. It also fails providing
   reasonable information when one pattern has not enough Lambdas.

diff --git a/components/cic_proof_checking/cicPp.ml b/components/cic_proof_checking/cicPp.ml
index 06bb082b4110b531209d55321e4aa9e4f4763b15..136e9ddaee9150c9eb0acd8d16d7dec0c3986476 100644 (file)
--- a/components/cic_proof_checking/cicPp.ml
+++ b/components/cic_proof_checking/cicPp.ml
@@ -95,14 +95,14 @@ let rec pp t l =
     | C.Implicit _ -> "?"
     | C.Prod (b,s,t) ->
        (match b with
-          C.Name n -> "(\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
+          C.Name n -> "(\\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
         | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")"
        )
     | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
     | C.Lambda (b,s,t) ->
        "(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
     | C.LetIn (b,s,t) ->
-       " let " ^ ppname b ^ " \def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
+       " let " ^ ppname b ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
     | C.Appl li ->
        "(" ^
        (List.fold_right
@@ -137,30 +137,58 @@ let rec pp t l =
            string_of_int n2
        )
     | C.MutCase (uri,n1,ty,te,patterns) ->
-       let connames =
+       let connames_and_argsno =
         (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
+              List.map
+               (fun id,ty ->
+                 (* this is just an approximation since we do not have
+                    reduction yet! *)
+                 let rec count_prods =
+                  function
+                     C.Prod (_,_,bo) -> 1 + count_prods bo
+                   | _ -> 0
+                 in
+                  id, count_prods ty
+               ) cons
           | _ -> raise CicPpInternalError
         )
        in
-        let connames_and_patterns =
+        let connames_and_argsno_and_patterns =
          let rec combine =
             function
                [],[] -> []
-             | [],l -> List.map (fun x -> "???",Some x) l
-             | l,[] -> List.map (fun x -> x,None) l
-             | x::tlx,y::tly -> (x,Some y)::(combine (tlx,tly))
+             | [],l -> List.map (fun x -> "???",0,Some x) l
+             | l,[] -> List.map (fun (x,no) -> x,no,None) l
+             | (x,no)::tlx,y::tly -> (x,no,Some y)::(combine (tlx,tly))
          in
-          combine (connames,patterns)
+          combine (connames_and_argsno,patterns)
         in
-        "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^
-          List.fold_right
-           (fun (x,y) i -> "\n " ^ x ^ " => " ^
-             (match y with None -> "" | Some y -> pp y l) ^ i)
-           connames_and_patterns "" ^
-          "\nend"
+         "\nmatch " ^ pp te l ^ " return " ^ pp ty l ^ " with \n [ " ^
+          (String.concat "\n | "
+           (List.map
+            (fun (x,argsno,y) ->
+              let rec aux argsno l =
+               function
+                  Cic.Lambda (name,ty,bo) when argsno > 0 ->
+                   let args,res = aux (argsno - 1) (Some name::l) bo in
+                    ("(" ^ (match name with C.Anonymous -> "_" | C.Name s -> s)^
+                     ":" ^ pp ty l ^ ")")::args, res
+                | t when argsno = 0 -> [],pp t l
+                | t -> ["{" ^ string_of_int argsno ^ " args missing}"],pp t l
+              in
+               let pattern,body =
+                match y with
+                   None -> x,""
+                 | Some y when argsno = 0 -> x,pp y l
+                 | Some y ->
+                    let args,body = aux argsno l y in
+                     "(" ^ x ^ " " ^ String.concat " " args ^ ")",body
+               in
+                pattern ^ " => " ^ body
+            ) connames_and_argsno_and_patterns)) ^
+          "\n]"
     | C.Fix (no, funs) ->
        let snames = List.map (fun (name,_,_,_) -> name) funs in
         let names =
@@ -385,11 +413,11 @@ let rec check_rec ctx string_name =
          | _ -> assert false) in
        remove_prefix name string_name  
     | Cic.MutCase (_,_,_,te,pl) ->
-       let strig_name = remove_prefix "match" string_name in
+       let string_name = remove_prefix "match" string_name in
        let string_name = check_rec ctx string_name te in
         List.fold_right (fun t s -> check_rec ctx s t) pl string_name
     | Cic.Fix (_,fl) ->
-        let strig_name = remove_prefix "fix" string_name in
+        let string_name = remove_prefix "fix" string_name in
         let names = List.map (fun (name,_,_,_) -> name) fl in
         let onames =
           List.rev (List.map (function name -> Cic.Name name) names)
@@ -397,7 +425,7 @@ let rec check_rec ctx string_name =
         List.fold_right 
          (fun (_,_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
     | Cic.CoFix (_,fl) ->
-       let strig_name = remove_prefix "cofix" string_name in
+       let string_name = remove_prefix "cofix" string_name in
         let names = List.map (fun (name,_,_) -> name) fl in
         let onames =
           List.rev (List.map (function name -> Cic.Name name) names)