From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 10 Nov 2007 13:16:57 +0000 (+0000)
Subject: More correct (but still bugged) implementation of type definition.
X-Git-Tag: 0.4.95@7852~28
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=66a3a89245310e5f0430ffae01ef2e92bad2b691

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

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index f35cd0e1e..e591a1278 100644
--- 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