a) Detection of existential types now implemented

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

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index 9296b7bb05d260fd4429147b12c354104070a95c..75088e6fc11fe7ab36573d9b3d55338e7cf704ad 100644 (file)
--- a/components/cic_exportation/cicExportation.ml
+++ b/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
@@ -238,9 +243,10 @@ let rec pp ~in_type t context =
         "unit (* TOO POLYMORPHIC TYPE *)"
        else (
        let needs_obj_magic =
-        match ty with
+        (* BUG HERE: we should consider also the right parameters *)
+        match CicReduction.whd context ty with
            Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
-         | _ -> assert false
+         | _ -> false (* it can be a Rel, e.g. in *_rec *)
        in
        (match analyze_term context te with
            `Type -> assert false
@@ -293,6 +299,10 @@ let rec pp ~in_type t context =
                      let rec aux argsno context =
                       function
                          Cic.Lambda (name,ty,bo) when argsno > 0 ->
+                          let name =
+                           match name with
+                              Cic.Anonymous -> Cic.Anonymous
+                            | Cic.Name n -> Cic.Name (ppid n) in
                           let args,res =
                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
                             bo
@@ -404,6 +414,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
@@ -421,6 +434,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)                                       *)
@@ -466,13 +520,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