More informative error message.

[helm.git] / components / cic_proof_checking / cicPp.ml

diff --git a/components/cic_proof_checking/cicPp.ml b/components/cic_proof_checking/cicPp.ml
index feca7c3cfe07951bfd32d42ff29e74f0391e976f..f3560cc3afe2733757f6fac1694a3c59328f7ec6 100644 (file)
--- a/components/cic_proof_checking/cicPp.ml
+++ b/components/cic_proof_checking/cicPp.ml
@@ -80,10 +80,8 @@ let rec pp t l =
        UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
     | C.Meta (n,l1) ->
        "?" ^ (string_of_int n) ^ "[" ^ 
-(*
         String.concat " ; "
          (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
-*)
         "]"
     | C.Sort s ->
        (match s with
@@ -97,14 +95,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 ((Some b)::l)
-        | C.Anonymous -> "(" ^ 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) ->
-       "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+       " let " ^ ppname b ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
     | C.Appl li ->
        "(" ^
        (List.fold_right
@@ -139,30 +137,60 @@ 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,_,_,_) ->
+            C.InductiveDefinition (dl,_,paramsno,_) ->
              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 toskip =
+                  function
+                     C.Prod (_,_,bo) when toskip > 0 ->
+                      count_prods (toskip - 1) bo
+                   | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
+                   | _ -> 0
+                 in
+                  id, count_prods paramsno 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 =
@@ -387,11 +415,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)
@@ -399,7 +427,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)