1structure type_pp :> type_pp = 2struct 3 4open Feedback Type Portable HOLgrammars type_grammar 5 6datatype mygrav = Sfx 7 | Lfx of int * string 8 | Rfx of int * string 9 | Top 10 11datatype single_rule = IR of int * associativity * string 12 13val ERR = mk_HOL_ERR "type_pp" "pp_type"; 14 15val avoid_unicode = ref (Systeml.OS = "winNT") 16local 17 open Globals 18 fun ascii_delims () = 19 (List.app (fn r => r := "``") [type_pp_prefix, type_pp_suffix, 20 term_pp_prefix, term_pp_suffix]; 21 thm_pp_prefix := "|- "; 22 thm_pp_suffix := "") 23 fun unicode_delims () = 24 (List.app (fn r => r := UnicodeChars.ldquo) 25 [type_pp_prefix, term_pp_prefix]; 26 List.app (fn r => r := UnicodeChars.rdquo) 27 [type_pp_suffix, term_pp_suffix]; 28 thm_pp_prefix := UnicodeChars.turnstile ^ " "; 29 thm_pp_suffix := "") 30 fun avoidset i = if i = 0 then (unicode_delims(); avoid_unicode := false) 31 else (ascii_delims(); avoid_unicode := true) 32 fun avoidget () = if !avoid_unicode then 1 else 0 33in 34 35val _ = register_ftrace("PP.avoid_unicode", (avoidget, avoidset), 1) 36val _ = register_ftrace("Unicode", 37 (fn () => 1 - avoidget(), fn n => avoidset (1 - n)), 38 1) 39val _ = avoidset (avoidget()) 40end 41 42 43val pp_num_types = ref true 44val _ = register_btrace("pp_num_types", pp_num_types) 45 46val pp_annotations = ref (!Globals.interactive) 47val _ = register_btrace ("pp_annotations", pp_annotations) 48 49fun dest_numtype ty = let 50 open Arbnum 51 val _ = (* respect pp_num_types flag *) 52 !pp_num_types orelse raise mk_HOL_ERR "" "" "" 53 val _ = (* exception: don't print :one as one *) 54 let val {Thy,Tyop,Args} = dest_thy_type ty 55 in 56 if Thy = "one" andalso Tyop = "one" then raise mk_HOL_ERR "" "" "" 57 else () 58 end 59 fun recurse (base, acc) ty = let 60 val {Thy,Tyop,Args} = dest_thy_type ty 61 in 62 case (Thy,Tyop) of 63 ("one", "one") => acc + base 64 | ("fcp", "bit1") => recurse (two * base, acc + base) (hd Args) 65 | ("fcp", "bit0") => recurse (two * base, acc) (hd Args) 66 | _ => raise mk_HOL_ERR "" "" "" 67 end 68in 69 toString (recurse (one, zero) ty) 70end 71 72val greek4 = let 73 open UnicodeChars 74in 75 [alpha, beta, gamma, delta] 76end 77 78fun structure_to_string st = let 79 fun recurse paren st = 80 case st of 81 TYOP {Thy,Tyop,Args} => let 82 val opstr = Thy ^ "$" ^ Tyop 83 in 84 case Args of 85 [] => opstr 86 | [x] => recurse false x ^ " " ^ opstr 87 | [x,y] => if Thy = "min" andalso Tyop = "fun" then 88 (if paren then "(" else "") ^ 89 recurse true x ^ " -> " ^ 90 recurse false y ^ 91 (if paren then ")" else "") 92 else 93 "(" ^ recurse false x ^ ", " ^ recurse false y ^ ") " ^ 94 opstr 95 | _ => "(" ^ String.concatWith ", " (map (recurse false) Args) ^ 96 ") " ^ opstr 97 end 98 | PARAM i => if i < 4 then List.nth(greek4, i) 99 else "'" ^ str (Char.chr (Char.ord #"a" + i)) 100in 101 recurse false st 102end 103 104val pp_array_types = ref true 105val _ = register_btrace ("pp_array_types", pp_array_types) 106 107fun pp_type0 (G:grammar) (backend: PPBackEnd.t) = let 108 val {infixes,suffixes} = rules G 109 fun lookup_tyop s = let 110 fun recurse [] = NONE 111 | recurse (x::xs) = let 112 in 113 case x of 114 (p, INFIX (slist, a)) => let 115 val res = List.find (fn r => #opname r = s) slist 116 in 117 case res of 118 NONE => recurse xs 119 | SOME r => SOME(IR(p, a,#parse_string r)) 120 end 121 end 122 in 123 recurse infixes : single_rule option 124 end 125 fun pr_ty ty grav depth = let 126 open HOLPP smpp PPBackEnd 127 val {add_string, add_break, ublock, add_xstring,...} = backend 128 fun add_ann_string (s,ann) = add_xstring {s=s,ann=SOME ann,sz=NONE} 129 fun paren b p = if b then add_string "(" >> p >> add_string ")" else p 130 fun uniconvert s = 131 if not (!avoid_unicode) andalso get_tracefn "Greek tyvars" () = 1 132 andalso size s = 2 133 then 134 let 135 val i = Char.ord (String.sub(s, 1)) - Char.ord #"a" + 0x3B1 136 in 137 if 0x3B1 <= i andalso i <= 0x3C9 andalso i <> 0x3BB then UTF8.chr i 138 else s 139 end 140 else s 141 in 142 if depth = 0 then add_string "..." 143 else 144 if is_vartype ty then 145 add_ann_string (uniconvert (dest_vartype ty), TyV) 146 else let 147 val s = dest_numtype ty 148 in 149 add_string s 150 end handle HOL_ERR _ => 151 let 152 fun realtype ty = let val {Thy,Tyop,...} = dest_thy_type ty 153 in Thy ^ "$" ^ Tyop end 154 val {Tyop = abop, Args = abargs, Thy = thyopt} = 155 type_grammar.abb_dest_type G ty 156 val abop_s = 157 case thyopt of 158 NONE => abop 159 | SOME thy => KernelSig.name_toString {Thy = thy, Name = abop} 160 fun tooltip () = 161 let 162 val abbs = type_grammar.parse_map G 163 fun doabbrev st = 164 let 165 val numps = num_params st 166 in 167 if 0 < numps then let 168 val params = 169 if numps <= 4 then List.take(greek4, numps) 170 else let 171 fun tab i = str (Char.chr (Char.ord #"e" + i)) 172 in 173 greek4 @ List.tabulate(numps - 4, tab) 174 end 175 in 176 UnicodeChars.lambda ^ 177 String.concatWith " " params ^ ". " ^ 178 structure_to_string st 179 end 180 else structure_to_string st 181 end 182 in 183 case thyopt of 184 SOME thy => (* unprivileged abbrev *) 185 let 186 val knm = {Thy = thy, Name = abop} 187 in 188 case Binarymap.peek (abbs, knm) of 189 NONE => realtype ty (* probably shouldn't happen *) 190 | SOME st => doabbrev st 191 end 192 | NONE => 193 let 194 val privabbs = type_grammar.privileged_abbrevs G 195 in 196 case Binarymap.peek (privabbs, abop) of 197 NONE => realtype ty 198 | SOME thy => 199 let 200 val knm = {Thy = thy, Name = abop} 201 in 202 case Binarymap.peek (abbs, knm) of 203 NONE => raise Fail "Very confused tyabbrev" 204 | SOME st => doabbrev st 205 end 206 end 207 end 208 fun print_args grav0 args = let 209 val parens_needed = case args of [_] => false | _ => true 210 val grav = if parens_needed then Top else grav0 211 in 212 paren parens_needed ( 213 ublock INCONSISTENT 0 ( 214 pr_list (fn arg => pr_ty arg grav (depth - 1)) 215 (add_string "," >> add_break (1, 0)) args 216 ) 217 ) 218 end 219 val {Thy, Tyop = realTyop, Args = realArgs} = dest_thy_type ty 220 in 221 if abop = "cart" andalso length abargs = 2 andalso 222 Thy = "fcp" andalso realTyop = "cart" andalso !pp_array_types 223 then 224 pr_ty (hd realArgs) Sfx (depth - 1) >> 225 add_string "[" >> 226 pr_ty (hd (tl realArgs)) Top (depth - 1) >> 227 add_string "]" 228 else 229 case abargs of 230 [] => add_ann_string (abop_s, TyOp tooltip) 231 | [arg1, arg2] => 232 let 233 fun print_suffix_style () = 234 ublock INCONSISTENT 0 ( 235 (* knowing that there are two args, we know that they will 236 be printed with parentheses, so the gravity we pass in 237 here makes no difference. *) 238 print_args Top abargs >> 239 add_break(1,0) >> 240 add_ann_string (abop_s, TyOp tooltip) 241 ) 242 in 243 if isSome thyopt then print_suffix_style() 244 else 245 case lookup_tyop abop of 246 SOME (IR(prec, assoc, printthis)) => 247 let 248 val parens_needed = 249 case grav of 250 Sfx => true 251 | Lfx (n, s) => if s = printthis then 252 assoc <> LEFT 253 else (n >= prec) 254 | Rfx (n, s) => if s = printthis then 255 assoc <> RIGHT 256 else (n >= prec) 257 | _ => false 258 in 259 paren parens_needed ( 260 ublock INCONSISTENT 0 ( 261 pr_ty arg1 (Lfx (prec, printthis)) (depth - 1) >> 262 add_break(1,0) >> 263 add_ann_string (printthis, TySyn tooltip) >> 264 add_break(1,0) >> 265 pr_ty arg2 (Rfx (prec, printthis)) (depth -1) 266 ) 267 ) 268 end 269 | NONE => print_suffix_style() 270 end 271 | _ => 272 ublock INCONSISTENT 0 ( 273 print_args Sfx abargs >> 274 add_break(1,0) >> 275 add_ann_string (abop_s, TyOp tooltip) 276 ) 277 end 278 end 279in 280 pr_ty 281end 282 283fun pp_type G backend = let 284 val baseprinter = pp_type0 G backend 285in 286 (fn ty => baseprinter ty Top (!Globals.max_print_depth)) 287end 288 289fun pp_type_with_depth G backend = let 290 val baseprinter = pp_type0 G backend 291in 292 (fn depth => fn ty => baseprinter ty Top depth) 293end 294 295end; (* struct *) 296 297(* testing 298 299val G = parse_type.BaseHOLgrammar; 300fun p ty = 301 Portable.pp_to_string 75 302 (fn pp => fn ty => type_pp.pp_type G pp ty type_pp.Top 100) ty; 303 304new_type {Name = "fmap", Arity = 2}; 305 306val G' = [(0, parse_type.INFIX("->", "fun", parse_type.RIGHT)), 307 (1, parse_type.INFIX("=>", "fmap", parse_type.NONASSOC)), 308 (2, parse_type.INFIX("+", "sum", parse_type.LEFT)), 309 (3, parse_type.INFIX("#", "prod", parse_type.RIGHT)), 310 (100, parse_type.SUFFIX("list", true)), 311 (101, parse_type.SUFFIX("fun", false)), 312 (102, parse_type.SUFFIX("prod", false)), 313 (103, parse_type.SUFFIX("sum", false))]; 314fun p ty = 315 Portable.pp_to_string 75 316 (fn pp => fn ty => type_pp.pp_type G' pp ty type_pp.Top 100) ty; 317 318p (Type`:(bool,num)fmap`) 319 320*) 321