From dd1c4eeef3d38eb9e01d50d06de6892a048c05a5 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 13 Sep 2006 14:08:57 +0000
Subject: [PATCH] 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.

---
 components/cic_proof_checking/cicPp.ml | 64 ++++++++++++++++++--------
 1 file changed, 46 insertions(+), 18 deletions(-)

diff --git a/components/cic_proof_checking/cicPp.ml b/components/cic_proof_checking/cicPp.ml
index 06bb082b4..136e9ddae 100644
--- 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)
-- 
2.39.2