Bug fixed: local type declarations are not allowed in ocaml.

[helm.git] / components / cic_exportation / cicExportation.ml

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index e591a12784966aa815e8fc0723d326fd6b9527f9..58e8170911ba0d05a3f470622a3b6b5ecfe59ba4 100644 (file)
--- a/components/cic_exportation/cicExportation.ml
+++ b/components/cic_exportation/cicExportation.ml
@@ -183,9 +183,23 @@ 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 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) ^ ")"
+       (match analyze_term context s with
+           `Type
+         | `Proof ->
+            let ty,_ =
+             CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph
+            in
+             pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context)
+         | `Term ->
+            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
@@ -331,11 +345,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
@@ -347,11 +362,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
@@ -410,6 +426,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