From 127781aeff80e54f2c5d80ef6ffbe4ef27b24b38 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Nov 2007 10:10:33 +0000 Subject: [PATCH] Type application and abstractions are now exported correctly. --- components/cic_exportation/cicExportation.ml | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml index 769dc916c..94cd982fe 100644 --- a/components/cic_exportation/cicExportation.ml +++ b/components/cic_exportation/cicExportation.ml @@ -164,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) -> @@ -176,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 @@ -338,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 ;; -- 2.39.2