More correct (but still bugged) implementation of type definition.

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index f35cd0e1e73d71996cb46770f5cae758795cc49e..e591a12784966aa815e8fc0723d326fd6b9527f9 100644 (file)
--- a/components/cic_exportation/cicExportation.ml
+++ b/components/cic_exportation/cicExportation.ml
@@ -427,6 +427,47 @@ let ppty current_module_uri =
   args
 ;;
 
+exception DoNotExtract;;
+
+let pp_abstracted_ty current_module_uri =
+ let rec args context =
+  function
+     Cic.Lambda (n,s,t) ->
+      let n =
+       match n with
+          Cic.Anonymous -> Cic.Anonymous
+        | Cic.Name n -> Cic.Name (String.uncapitalize n)
+      in
+       (match analyze_type context s with
+           `Statement
+         | `Type
+         | `Sort Cic.Prop ->
+             args ((Some (n,Cic.Decl s))::context) t
+         | `Sort _ ->
+             let n =
+              match n with
+                 Cic.Anonymous -> Cic.Anonymous
+               | Cic.Name name -> Cic.Name ("'" ^ name) in
+             let abstr,res =
+              args ((Some (n,Cic.Decl s))::context) t
+             in
+              (match n with
+                  Cic.Anonymous -> abstr
+                | Cic.Name name -> name::abstr),
+              res)
+   | ty ->
+     match analyze_type context ty with
+      `  Sort _
+      | `Statement -> raise DoNotExtract
+      | `Type ->
+          (* BUG HERE: this can be a real System F type *)
+          let head = pp ~in_type:true current_module_uri ty context in
+          [],head
+ in
+  args
+;;
+
+
 (* ppinductiveType (typename, inductive, arity, cons)                       *)
 (* pretty-prints a single inductive definition                              *)
 (* (typename, inductive, arity, cons)                                       *)
@@ -472,13 +513,15 @@ let ppobj current_module_uri obj =
             match analyze_type [] t1 with
                `Sort Cic.Prop -> ""
              | _ ->
-               let abstr,args = ppty current_module_uri 0 [] t1 in
-               let abstr =
-                let s = String.concat "," abstr in
-                if s = "" then "" else "(" ^ s ^ ") "
-               in
-                "type " ^ abstr ^ ppid name ^ " = " ^ String.concat "->" args ^
-                "\n")
+               (try
+                 let abstr,res = pp_abstracted_ty current_module_uri [] t1 in
+                 let abstr =
+                  let s = String.concat "," abstr in
+                  if s = "" then "" else "(" ^ s ^ ") "
+                 in
+                  "type " ^ abstr ^ ppid name ^ " = " ^ res ^ "\n"
+                with
+                 DoNotExtract -> ""))
    | C.Constant (name, None, ty, params, _) ->
       (match analyze_type [] ty with
           `Sort Cic.Prop