Empty and singleton type elimination are now handled properly.

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index e5f1face1e9eb854049ba089b723f8d0a8705321..4b10fe7316514680e465d5d9d994c01bb1f01ba7 100644 (file)
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -216,64 +216,72 @@ let rec pp t context =
            string_of_int n2
        )
     | C.MutCase (uri,n1,ty,te,patterns) ->
-       let connames_and_argsno =
-        (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
-            C.InductiveDefinition (dl,_,paramsno,_) ->
-             let (_,_,_,cons) = get_nth dl (n1+1) in
-              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
-                  qualified_name_of_uri current_module_name ~capitalize:true
-                   (UriManager.uri_of_string
-                     (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
-                  count_prods paramsno ty
-               ) cons
-          | _ -> raise CicExportationInternalError
-        )
-       in
-        let connames_and_argsno_and_patterns =
-         let rec combine =
-            function
-               [],[] -> []
-             | [],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_and_argsno,patterns)
-        in
-         "\n(match " ^ pp te context ^ " with \n" ^
-          (String.concat "\n | "
-           (List.map
-            (fun (x,argsno,y) ->
-              let rec aux argsno context =
-               function
-                  Cic.Lambda (name,ty,bo) when argsno > 0 ->
-                   let args,res = aux (argsno - 1) (Some (name,Cic.Decl ty)::context) bo in
-                    (match name with C.Anonymous -> "_" | C.Name s -> s)::args,
-                    res
-                | t when argsno = 0 -> [],pp t context
-                | t -> ["{" ^ string_of_int argsno ^ " args missing}"],pp t context
+       (match analyze_term context te with
+           `Type -> assert false
+         | `Proof ->
+             (match patterns with
+                 [] -> "assert false"   (* empty type elimination *)
+               | [he] -> pp he context  (* singleton elimination *)
+               | _ -> assert false)
+         | `Term ->
+            let connames_and_argsno =
+             (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+                 C.InductiveDefinition (dl,_,paramsno,_) ->
+                  let (_,_,_,cons) = get_nth dl (n1+1) in
+                   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
+                       qualified_name_of_uri current_module_name ~capitalize:true
+                        (UriManager.uri_of_string
+                          (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
+                       count_prods paramsno ty
+                    ) cons
+               | _ -> raise CicExportationInternalError
+             )
+            in
+             let connames_and_argsno_and_patterns =
+              let rec combine =
+                 function
+                    [],[] -> []
+                  | [],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
-               let pattern,body =
-                match y with
-                   None -> x,""
-                 | Some y when argsno = 0 -> x,pp y context
-                 | Some y ->
-                    let args,body = aux argsno context y in
-                    let sargs = String.concat "," args in
-                     x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),body
-               in
-                pattern ^ " -> " ^ body
-            ) connames_and_argsno_and_patterns)) ^
-          ")\n"
+               combine (connames_and_argsno,patterns)
+             in
+              "\n(match " ^ pp te context ^ " with \n" ^
+               (String.concat "\n | "
+                (List.map
+                 (fun (x,argsno,y) ->
+                   let rec aux argsno context =
+                    function
+                       Cic.Lambda (name,ty,bo) when argsno > 0 ->
+                        let args,res = aux (argsno - 1) (Some (name,Cic.Decl ty)::context) bo in
+                         (match name with C.Anonymous -> "_" | C.Name s -> s)::args,
+                         res
+                     | t when argsno = 0 -> [],pp t context
+                     | t -> ["{" ^ string_of_int argsno ^ " args missing}"],pp t context
+                   in
+                    let pattern,body =
+                     match y with
+                        None -> x,""
+                      | Some y when argsno = 0 -> x,pp y context
+                      | Some y ->
+                         let args,body = aux argsno context y in
+                         let sargs = String.concat "," args in
+                          x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),body
+                    in
+                     pattern ^ " -> " ^ body
+                 ) connames_and_argsno_and_patterns)) ^
+               ")\n")
     | C.Fix (no, funs) ->
        let names =
         List.rev