From a634c95917dee0fca1d1cf77b6fb7491975128cc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 4 Sep 2012 07:55:26 +0000 Subject: [PATCH] 1. deriving (Show) no longer used because it fails on empty types 2. pretty-printing of types fixed: application arguments never had parentheses 3. Top replaced with GHC.Prim.Any --- matita/components/ng_kernel/nCicExtraction.ml | 22 +++++++++++-------- matita/matita/lib/preamble.hs | 2 -- 2 files changed, 13 insertions(+), 11 deletions(-) diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index ac6848b83..2bc21ec92 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -43,8 +43,8 @@ let rec size_of_kind = | KSkip k -> size_of_kind k ;; -let bracket size_of pp o = - if size_of o > 1 then +let bracket ?(prec=1) size_of pp o = + if size_of o > prec then "(" ^ pp o ^ ")" else pp o @@ -69,10 +69,10 @@ type typ = let rec size_of_type = function - | Var _ -> 1 - | Unit -> 1 - | Top -> 1 - | TConst _ -> 1 + | Var _ -> 0 + | Unit -> 0 + | Top -> 0 + | TConst _ -> 0 | Arrow _ -> 2 | TSkip t -> size_of_type t | Forall _ -> 2 @@ -954,7 +954,7 @@ let rec pretty_print_type status ctxt = function | Var n -> List.nth ctxt (n-1) | Unit -> "()" - | Top -> "Top" + | Top -> "GHC.Prim.Any" | TConst ref -> pp_ref status ref | Arrow (t1,t2) -> bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^ @@ -968,7 +968,11 @@ let rec pretty_print_type status ctxt = "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t else "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t - | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl) + | TAppl tl -> + String.concat " " + (List.map + (fun t -> bracket ~prec:0 size_of_type + (pretty_print_type status ctxt) t) tl) let pretty_print_term_context status ctx1 ctx2 = let name_context, rev_res = @@ -1082,7 +1086,7 @@ let rec pp_obj status (_,ref,obj_kind) = let namectx = namectx_of_ctx left in pp_ref status ref ^ " :: " ^ pretty_print_type status namectx tys - ) cl) ^ "\n deriving (Prelude.Show)" + ) cl) (*^ "\n deriving (Prelude.Show)"*) ) il) (* inductive and records missing *) diff --git a/matita/matita/lib/preamble.hs b/matita/matita/lib/preamble.hs index e196a2be3..abc288aa4 100644 --- a/matita/matita/lib/preamble.hs +++ b/matita/matita/lib/preamble.hs @@ -5,5 +5,3 @@ module Main where import Unsafe.Coerce import Prelude (error) import qualified Prelude - -data Top -- 2.39.2