Empty types not in Prop and empty types elimination handled correctly.

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index 4b10fe7316514680e465d5d9d994c01bb1f01ba7..eeddc094996e2d06f9ff0051c92e2e152bcdaec8 100644 (file)
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -224,64 +224,74 @@ let rec pp t context =
                | [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))
+            if patterns = [] then "assert false"
+            else
+             (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
-               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")
+               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
+                     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
@@ -365,22 +375,25 @@ let ppinductiveType current_module_name (typename, inductive, arity, cons) =
   | `Statement
   | `Type -> assert false
   | `Sort _ ->
-    let abstr,scons =
-     List.fold_right
-      (fun (id,ty) (abstr,i) ->
-         let abstr',sargs = ppty current_module_name [] ty in
-         let sargs = String.concat " * " sargs in
-          abstr'@abstr,
-          String.capitalize id ^
-           (if sargs = "" then "" else " of " ^ sargs) ^
-           (if i = "" then "\n" else "\n | ") ^ i)
-      cons ([],"")
-     in
-      let abstr =
-       let s = String.concat "," abstr in
-       if s = "" then "" else "(" ^ s ^ ") "
+    if cons = [] then
+     "type " ^ String.uncapitalize typename ^ " = unit (* empty type *)\n"
+    else (
+     let abstr,scons =
+      List.fold_right
+       (fun (id,ty) (abstr,i) ->
+          let abstr',sargs = ppty current_module_name [] ty in
+          let sargs = String.concat " * " sargs in
+           abstr'@abstr,
+           String.capitalize id ^
+            (if sargs = "" then "" else " of " ^ sargs) ^
+            (if i = "" then "" else "\n | ") ^ i)
+       cons ([],"")
       in
-      "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n"
+       let abstr =
+        let s = String.concat "," abstr in
+        if s = "" then "" else "(" ^ s ^ ") "
+       in
+       "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n")
 ;;
 
 let ppobj current_module_name obj =
@@ -454,5 +467,5 @@ let ppobj current_module_name obj =
 
 let ppobj current_module_name obj =
  let res = ppobj current_module_name obj in
-  if res = "" then "" else res ^ ";;\n"
+  if res = "" then "" else res ^ ";;\n\n"
 ;;