Type application and abstractions are now exported correctly.

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

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index eeddc094996e2d06f9ff0051c92e2e152bcdaec8..94cd982fe3a1b4f02718eabf24fd6219936b7e74 100644 (file)
--- a/components/cic_exportation/cicExportation.ml
+++ b/components/cic_exportation/cicExportation.ml
@@ -62,7 +62,8 @@ let analyze_type context t =
 let ppid =
  let reserved =
   [ "to";
-    "mod"
+    "mod";
+    "val"
   ]
  in
   function n ->
@@ -163,8 +164,10 @@ let rec pp t context =
     | C.Implicit _ -> "?"
     | C.Prod (b,s,t) ->
        (match b with
-          C.Name n -> "(\\forall " ^ n ^ ":" ^ pp s context ^ "." ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")"
-        | C.Anonymous -> "(" ^ pp s context ^ "\\to " ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")"
+          C.Name n ->
+           let n = "'" ^ String.uncapitalize n in
+            "(" ^ pp s context ^ " -> " ^ pp t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
+        | C.Anonymous -> "(" ^ pp s context ^ " -> " ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")"
        )
     | C.Cast (v,t) -> pp v context
     | C.Lambda (b,s,t) ->
@@ -175,6 +178,10 @@ let rec pp t context =
     | C.LetIn (b,s,t) ->
        let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph in
        "(let " ^ ppname b ^ " = " ^ pp s context ^ " in " ^ pp t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")"
+    | C.Appl (C.MutInd _ as he::tl) ->
+       let hes = pp he context in
+       let stl = String.concat "," (clean_args_for_ty context tl) in
+        (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
     | C.Appl (C.MutConstruct _ as he::tl) ->
        let hes = pp he context in
        let stl = String.concat "," (clean_args context tl) in
@@ -337,6 +344,13 @@ and clean_args context =
        `Type -> None
      | `Proof -> None
      | `Term -> Some pp t context)
+and clean_args_for_ty context =
+ HExtlib.filter_map
+  (function t ->
+    match analyze_term context t with
+       `Type -> Some pp t context
+     | `Proof -> None
+     | `Term -> None)
 in
  pp
 ;;
@@ -345,6 +359,11 @@ let ppty current_module_name =
  let rec args context =
   function
      Cic.Prod (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
            `Sort Cic.Prop -> args ((Some (n,Cic.Decl s))::context) t
          | `Statement
@@ -369,7 +388,8 @@ let ppty current_module_name =
 (* 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 ppinductiveType current_module_name nparams (typename, inductive, arity, cons)
+=
  match analyze_type [] arity with
     `Sort Cic.Prop -> ""
   | `Statement
@@ -380,10 +400,10 @@ let ppinductiveType current_module_name (typename, inductive, arity, cons) =
     else (
      let abstr,scons =
       List.fold_right
-       (fun (id,ty) (abstr,i) ->
+       (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
           let abstr',sargs = ppty current_module_name [] ty in
           let sargs = String.concat " * " sargs in
-           abstr'@abstr,
+           abstr',
            String.capitalize id ^
             (if sargs = "" then "" else " of " ^ sargs) ^
             (if i = "" then "" else "\n | ") ^ i)
@@ -462,7 +482,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 ""
+       (fun x i -> ppinductiveType current_module_name nparams x ^ i) l ""
 ;;
 
 let ppobj current_module_name obj =