From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 4 Nov 2007 18:27:05 +0000 (+0000)
Subject: 1. type definitions of propositions are no longer exported even if parametric
X-Git-Tag: make_still_working~5909
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=935c5379057ce2fe11fc660b55937ff1b153a670;p=helm.git

1. type definitions of propositions are no longer exported even if parametric
2. arguments of type definitions are now printed correctly according to
   OCaml awful syntax
---

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index 06fc38308..e5f1face1 100644
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -45,7 +45,8 @@ let analyze_type context t =
  let rec aux =
   function
      Cic.Sort s -> `Sort s
-   | Cic.Prod (_,_,t) -> aux t
+   | Cic.Prod (_,_,t)
+   | Cic.Lambda (_,_,t) -> aux t
    | _ -> `SomethingElse
  in
  match aux t with
@@ -322,47 +323,56 @@ in
  pp
 ;;
 
+let ppty current_module_name =
+ let rec args context =
+  function
+     Cic.Prod (n,s,t) ->
+       (match analyze_type context s with
+           `Sort Cic.Prop -> args ((Some (n,Cic.Decl s))::context) t
+         | `Statement
+         | `Sort _ ->
+             let n =
+              match n with
+                 Cic.Anonymous -> Cic.Anonymous
+               | Cic.Name name -> Cic.Name ("'" ^ name) in
+             let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
+              (match n with
+                  Cic.Anonymous -> abstr
+                | Cic.Name name -> name::abstr),
+              args
+         | `Type ->
+             let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
+              abstr,pp current_module_name s context::args)
+   | _ -> [],[]
+ in
+  args
+;;
+
 (* ppinductiveType (typename, inductive, arity, cons)                       *)
 (* pretty-prints a single inductive definition                              *)
 (* (typename, inductive, arity, cons)                                       *)
 let ppinductiveType current_module_name (typename, inductive, arity, cons) =
- let abstr,scons =
-  List.fold_right
-   (fun (id,ty) (abstr,i) ->
-     let rec args context =
-      function
-         Cic.Prod (n,s,t) ->
-           (match analyze_type context s with
-               `Sort Cic.Prop -> args ((Some (n,Cic.Decl s))::context) t
-             | `Statement
-             | `Sort _ ->
-                 let n =
-                  match n with
-                     Cic.Anonymous -> Cic.Anonymous
-                   | Cic.Name name -> Cic.Name ("'" ^ name) in
-                 let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
-                  (match n with
-                      Cic.Anonymous -> abstr
-                    | Cic.Name name -> name::abstr),
-                  args
-             | `Type ->
-                 let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
-                  abstr,pp current_module_name s context::args)
-       | _ -> [],[]
+ match analyze_type [] arity with
+    `Sort Cic.Prop -> ""
+  | `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',sargs = args [] 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 ^ ") "
-   in
-   "type " ^ abstr ^ typename ^ " =\n" ^ scons
+      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 =
@@ -374,8 +384,18 @@ let ppobj current_module_name obj =
       (match analyze_type [] t2 with
           `Sort Cic.Prop
         | `Statement -> ""
-        | `Type
-        | `Sort _ -> "let " ^ ppid name ^ " =\n" ^ pp t1 [] ^ "\n")
+        | `Type -> "let " ^ ppid name ^ " =\n" ^ pp t1 [] ^ "\n"
+        | `Sort _ ->
+            match analyze_type [] t1 with
+               `Sort Cic.Prop -> ""
+             | _ ->
+               let abstr,args = ppty current_module_name [] t1 in
+               let abstr =
+                let s = String.concat "," abstr in
+                if s = "" then "" else "(" ^ s ^ ") "
+               in
+                "type " ^ abstr ^ ppid name ^ " = " ^ String.concat "->" args ^
+                "\n")
    | C.Constant (name, None, ty, params, _) ->
       (match analyze_type [] ty with
           `Sort Cic.Prop
@@ -421,7 +441,7 @@ let ppobj current_module_name obj =
           pp ~metasenv:conjectures ty [] 
    | C.InductiveDefinition (l, params, nparams, _) ->
       List.fold_right
-       (fun x i -> ppinductiveType current_module_name x ^ i) l "\n"
+       (fun x i -> ppinductiveType current_module_name x ^ i) l ""
 ;;
 
 let ppobj current_module_name obj =