X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_exportation%2FcicExportation.ml;h=8af058f9692d3bb8590fac15264d8236893c859b;hb=4bc8832972166cc497cd8dc23faa6b63124c2d0b;hp=e671effca9a565645d8d7f8c41f780d8b13f5d38;hpb=db04e50168be1d78e9074543990c6c7d0b40298b;p=helm.git

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index e671effca..8af058f96 100644
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -45,8 +45,7 @@ let analyze_type context t =
  let rec aux =
   function
      Cic.Sort s -> `Sort s
-   | Cic.Prod (_,_,t)
-   | Cic.Lambda (_,_,t) -> aux t
+   | Cic.Prod (_,_,t) -> aux t
    | _ -> `SomethingElse
  in
  match aux t with
@@ -63,7 +62,9 @@ let ppid =
  let reserved =
   [ "to";
     "mod";
-    "val"
+    "val";
+    "in";
+    "function"
   ]
  in
   function n ->
@@ -182,9 +183,13 @@ let rec pp ~in_type t context =
             "(function " ^ ppname b ^ " -> " ^
              pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
     | C.LetIn (b,s,t) ->
-       let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph in
+       let ty,_ = CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph in
        "(let " ^ ppname b ^ " = " ^ pp ~in_type:false s context ^ " in " ^
         pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")"
+    | C.Appl (he::tl) when in_type ->
+       let hes = pp ~in_type he context in
+       let stl = String.concat "," (clean_args_for_ty context tl) in
+        (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
     | C.Appl (C.MutInd _ as he::tl) ->
        let hes = pp ~in_type he context in
        let stl = String.concat "," (clean_args_for_ty context tl) in
@@ -330,11 +335,12 @@ let rec pp ~in_type t context =
                    ) connames_and_argsno_and_patterns)) ^
                  ")\n")))
     | C.Fix (no, funs) ->
-       let names =
-        List.rev
-         (List.map
-           (function (name,_,ty,_) ->
-             Some (C.Name name,Cic.Decl ty)) funs)
+       let names,_ =
+        List.fold_left
+         (fun (types,len) (n,_,ty,_) ->
+            (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+             len+1)
+         ) ([],0) funs
        in
          "let rec " ^
          List.fold_right
@@ -346,11 +352,12 @@ let rec pp ~in_type t context =
              Some (Cic.Name n,_) -> n
            | _ -> assert false)
     | C.CoFix (no,funs) ->
-       let names =
-        List.rev
-         (List.map
-           (function (name,ty,_) ->
-             Some (C.Name name,Cic.Decl ty)) funs)
+       let names,_ =
+        List.fold_left
+         (fun (types,len) (n,ty,_) ->
+            (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+             len+1)
+         ) ([],0) funs
        in
          "\nCoFix " ^ " {" ^
          List.fold_right
@@ -409,6 +416,9 @@ let ppty current_module_uri =
              let abstr,args =
               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
                abstr,pp ~in_type:true current_module_uri s context::args
+         | `Sort _ when nparams <= 0 ->
+             let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in
+              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
          | `Sort _ ->
              let n =
               match n with
@@ -426,6 +436,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)                                       *)
@@ -471,13 +522,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