1structure type_grammar :> type_grammar = 2struct 3 4open HOLgrammars 5open Lib 6open type_grammar_dtype 7 8fun typstruct_uptodate ts = 9 case ts of 10 PARAM _ => true 11 | TYOP {Thy, Tyop, Args} => ( 12 case Type.op_arity {Thy = Thy, Tyop = Tyop} of 13 SOME a => length Args = a andalso List.all typstruct_uptodate Args 14 | _ => false 15 ) 16 17type kernelname = KernelSig.kernelname 18 19fun break_qident s = 20 case String.fields (equal #"$") s of 21 [ _ ] => (NONE, s) 22 | [thy, nm] => (SOME thy, nm) 23 | _ => raise GrammarError ("String \""^s^ 24 "\" is not a valid type identifier") 25 26 27datatype grammar = TYG of { 28 rules : (int * grammar_rule) list, 29 parse_str : (kernelname, type_structure) Binarymap.dict, 30 str_print : (int * kernelname) TypeNet.typenet, 31 bare_names : (string, string) Binarymap.dict, 32 tstamp : int 33} 34 35datatype ty_absyn = 36 VTY of string 37 | QTYOP of kernelname * ty_absyn list 38(* 39 40 Like term parsing, type parsing is handled in two phases: 41 42 1. Concrete syntax (involving infixes and the special syntax for 43 array-typeshere) is mapped to abstract syntax, the ty_absyn type 44 above. The infix rules are in the rules field. 45 46 Along the way, bare names in the concrete syntax are mapped to 47 "qualified" operators (the QTYOP constructor) using the 48 bare_names map of the grammar. 49 50 2. The parse_str field of the grammar is then used to turn QTYOPs 51 into genuine type operators. 52 53 Printing uses the str_print field to turn structures into syntactic 54 structure names. If these are privileged, they get to print in bare 55 form; otherwise they will be qualified. 56 57 As with term overloads, more specific structure matches are 58 preferred when turning underlying type operators into names, and 59 the timestamp is used to break ties. 60 61*) 62open FunctionalRecordUpdate 63fun tyg_mkUp z = makeUpdate5 z 64fun update_G z = let 65 fun from rules parse_str str_print bare_names tstamp = 66 {rules = rules, parse_str = parse_str, 67 str_print = str_print, bare_names = bare_names, tstamp = tstamp} 68 (* fields in reverse order *) 69 fun from' tstamp bare_names str_print parse_str rules = 70 {rules = rules, parse_str = parse_str, 71 str_print = str_print, bare_names = bare_names, tstamp = tstamp} 72 (* first order *) 73 fun to f {rules, parse_str, str_print, bare_names, tstamp} = 74 f rules parse_str str_print bare_names tstamp 75in 76 tyg_mkUp (from, from', to) 77end z 78 79fun fupdate_rules f (TYG g) = 80 TYG (update_G g (U #rules (f (#rules g))) $$) 81fun fupdate_str_print f (TYG g) = 82 TYG (update_G g (U #str_print (f (#str_print g))) $$) 83fun fupdate_parse_str f (TYG g) = 84 TYG (update_G g (U #parse_str (f (#parse_str g))) $$) 85fun fupdate_tstamp f (TYG g) = 86 TYG (update_G g (U #tstamp (f (#tstamp g))) $$) 87fun fupdate_bare_names f (TYG g) = 88 TYG (update_G g (U #bare_names (f (#bare_names g))) $$) 89 90fun default_typrinter (G:grammar) (ty:Type.hol_type) = 91 HOLPP.PrettyString "<a type>" 92 93val type_printer = ref default_typrinter 94val initialised_printer = ref false 95 96fun initialise_typrinter f = 97 if not (!initialised_printer) then 98 (type_printer := f; initialised_printer := true) 99 else 100 raise Feedback.HOL_ERR {origin_structure = "type_grammar", 101 origin_function = "initialised_printer", 102 message = "Printer function already initialised"} 103 104fun pp_type g ty = (!type_printer) g ty 105 106fun structure_to_type st = 107 case st of 108 TYOP {Thy,Tyop,Args} => 109 Type.mk_thy_type {Thy = Thy, Tyop = Tyop, 110 Args = map structure_to_type Args} 111 | PARAM n => Type.mk_vartype ("'"^str (chr (n + ord #"a"))) 112 113fun params0 acc (PARAM i) = HOLset.add(acc, i) 114 | params0 acc (TYOP{Args,...}) = foldl (fn (t,set) => params0 set t) acc Args 115val params = params0 (HOLset.empty Int.compare) 116 117val num_params = HOLset.numItems o params 118 119fun suffix_arity (abbrevs, privs) s = 120 case Binarymap.peek (privs, s) of 121 NONE => NONE 122 | SOME thy => 123 let 124 in 125 case Binarymap.peek(abbrevs, {Thy = thy, Name = s}) of 126 NONE => NONE (* shouldn't happen *) 127 | SOME st => if typstruct_uptodate st then SOME (s, num_params st) 128 else NONE 129 end 130 131fun merge r1 r2 = 132 case (r1, r2) of 133 (INFIX(rlist1, a1), INFIX(rlist2, a2)) => let 134 in 135 if a1 = a2 then INFIX(Lib.union rlist1 rlist2, a1) 136 else 137 raise GrammarError 138 "Attempt to merge two infix types with different associativities" 139 end 140 141fun insert_sorted (k, v) [] = [(k, v)] 142 | insert_sorted kv1 (wholething as (kv2::rest)) = let 143 val (k1, v1) = kv1 144 val (k2, v2) = kv2 145 in 146 if (k1 < k2) then kv1::wholething 147 else 148 if k1 = k2 then (k1, merge v1 v2) :: rest 149 else 150 kv2 :: insert_sorted kv1 rest 151 end 152 153fun new_binary_tyop g {precedence, infix_form = ix, opname, associativity = a} = 154 let 155 val rule = (precedence, INFIX([{parse_string = ix, opname = opname}], a)) 156 in 157 g |> fupdate_rules (insert_sorted rule) 158 end 159 160fun remove_binary_tyop g s = let 161 fun bad_irule {parse_string,...} = parse_string = s 162 fun edit_rule (prec, r) = 163 case r of 164 INFIX (irules, assoc) => let 165 val irules' = List.filter (not o bad_irule) irules 166 in 167 if null irules' then NONE 168 else SOME (prec, INFIX (irules', assoc)) 169 end 170in 171 g |> fupdate_rules (List.mapPartial edit_rule) 172end 173 174 175fun new_qtyop (kid as {Name = name, Thy = thy}) g = 176 let 177 open Type Theory 178 in 179 case Type.op_arity {Tyop = name, Thy = thy} of 180 NONE => raise GrammarError 181 (name ^ " is not the name of a type operator in theory "^ 182 thy) 183 | SOME i => 184 let 185 val TYG {tstamp,...} = g 186 val opstructure = TYOP {Thy = thy, Tyop = name, 187 Args = List.tabulate(i, PARAM)} 188 fun mk_vari i = mk_vartype ("'a" ^ Int.toString i) 189 val ty = 190 mk_thy_type {Tyop = name, Thy = thy, 191 Args = List.tabulate(i, mk_vari)} 192 in 193 g |> fupdate_str_print 194 (fn tynet => TypeNet.insert(tynet,ty,(tstamp,kid))) 195 |> fupdate_parse_str (fn m => Binarymap.insert(m, kid, opstructure)) 196 |> fupdate_tstamp (fn i => i + 1) 197 |> fupdate_bare_names (fn m => Binarymap.insert(m, name, thy)) 198 end 199 end 200 201fun hide_tyop s = 202 fupdate_bare_names 203 (fn m => #1 (Binarymap.remove(m,s)) handle Binarymap.NotFound => m) 204 205val empty_grammar = TYG { rules = [], 206 parse_str = Binarymap.mkDict KernelSig.name_compare, 207 bare_names = Binarymap.mkDict String.compare, 208 str_print = TypeNet.empty, 209 tstamp = 0 } 210 211fun keys m = Binarymap.foldr (fn (k,v,acc) => k :: acc) [] m 212 213fun rules (TYG gr) = {infixes = #rules gr, suffixes = keys (#bare_names gr)} 214fun parse_map (TYG gr) = #parse_str gr 215fun print_map (TYG gr) = #str_print gr 216fun privabbs (TYG gr) = #bare_names gr 217val privileged_abbrevs = privabbs 218fun tstamp (TYG gr) = #tstamp gr 219fun bump_tstamp g = (tstamp g, fupdate_tstamp (fn n => n + 1) g) 220 221fun check_structure st = let 222 fun param_numbers (PARAM i, pset) = HOLset.add(pset, i) 223 | param_numbers (TYOP{Args,...}, pset) = foldl param_numbers pset Args 224 val pset = param_numbers (st, HOLset.empty Int.compare) 225 val plist = HOLset.listItems pset 226 fun check_for_gaps expecting [] = () 227 | check_for_gaps expecting (h::t) = 228 if h <> expecting then 229 raise GrammarError 230 ("Expecting to find parameter #"^Int.toString expecting) 231 else 232 check_for_gaps (expecting + 1) t 233in 234 check_for_gaps 0 plist 235end 236 237fun remove_knm_abbreviation g knm = let 238 val (dict, st) = Binarymap.remove(parse_map g, knm) 239 fun doprint pmap0 = #1 (TypeNet.delete(pmap0, structure_to_type st)) 240 handle Binarymap.NotFound => pmap0 241 fun maybe_rmpriv d = 242 case Binarymap.peek (d, #Name knm) of 243 NONE => d 244 | SOME thy' => if thy' = #Thy knm then #1 (Binarymap.remove(d, #Name knm)) 245 else d 246in 247 g |> fupdate_parse_str (K dict) 248 |> fupdate_str_print doprint 249 |> fupdate_bare_names maybe_rmpriv 250end 251 252fun remove_abbreviation g s = 253 let 254 val (thyopt, nm) = break_qident s 255 fun parsemap nmcheck (knm,st,acc) = 256 if nmcheck knm then acc else Binarymap.insert(acc,knm,st) 257 fun printmap nmcheck (ty,i as (_, knm),acc) = 258 if nmcheck knm then acc else TypeNet.insert(acc,ty,i) 259 fun thyprivrm thy m = 260 case Binarymap.peek (m, nm) of 261 NONE => m 262 | SOME thy' => if thy' = thy then #1 (Binarymap.remove(m,nm)) 263 else m 264 val (check,privrm) = 265 case thyopt of 266 NONE => ((fn knm => #Name knm = nm), 267 (fn m => #1 (Binarymap.remove (m, nm)) 268 handle Binarymap.NotFound => m)) 269 | SOME thy => (equal {Name = nm, Thy = thy}, thyprivrm thy) 270 in 271 g |> fupdate_bare_names privrm 272 |> fupdate_str_print (TypeNet.fold (printmap check) TypeNet.empty) 273 |> fupdate_parse_str 274 (Binarymap.foldl (parsemap check) 275 (Binarymap.mkDict KernelSig.name_compare)) 276 end 277 278fun type_to_structure ty = 279 let 280 open Type 281 val params = Listsort.sort Type.compare (type_vars ty) 282 val (num_vars, pset) = 283 List.foldl (fn (ty,(i,pset)) => (i + 1, Binarymap.insert(pset,ty,i))) 284 (0, Binarymap.mkDict Type.compare) params 285 fun mk_structure pset ty = 286 if is_vartype ty then PARAM (Binarymap.find(pset, ty)) 287 else let 288 val {Thy,Tyop,Args} = dest_thy_type ty 289 in 290 TYOP {Thy = Thy, Tyop = Tyop, Args = map (mk_structure pset) Args} 291 end 292 in 293 mk_structure pset ty 294 end 295 296 297fun new_abbreviation {knm,print,ty} tyg = let 298 open Portable 299 val st = type_to_structure ty 300 val {Name = s, Thy = thy} = knm 301 val tyg = case Binarymap.peek(parse_map tyg, knm) of 302 NONE => tyg 303 | SOME st' => 304 if st = st' then tyg 305 else 306 let 307 val tyg' = remove_knm_abbreviation tyg knm 308 in 309 Feedback.HOL_WARNING 310 "type_grammar" 311 "new_abbreviation" 312 ("Replacing old mapping from " ^ s ^ " to "^ 313 PP.pp_to_string (!Globals.linewidth) 314 (pp_type tyg') 315 (structure_to_type st')); 316 tyg' 317 end 318 val _ = case st of PARAM _ => 319 raise GrammarError 320 "Abbreviation can't be to a type variable" 321 | _ => () 322 val (tstamp, tyg) = bump_tstamp tyg 323 val result = 324 tyg |> fupdate_parse_str (fn d => Binarymap.insert(d,knm,st)) 325 |> (print ? 326 fupdate_str_print 327 (fn pmap => TypeNet.insert(pmap, 328 structure_to_type st, 329 (tstamp, knm)))) 330 |> fupdate_bare_names(fn d => Binarymap.insert(d,s,thy)) 331in 332 result 333end 334 335 336fun rev_append [] acc = acc 337 | rev_append (x::xs) acc = rev_append xs (x::acc) 338 339fun merge_abbrevs G (d1, d2) = let 340 fun merge_dictinsert (k,v,newdict) = 341 case Binarymap.peek(newdict,k) of 342 NONE => Binarymap.insert(newdict,k,v) 343 | SOME v0 => 344 if v0 <> v then 345 (Feedback.HOL_WARNING "parse_type" "merge_grammars" 346 ("Conflicting entries for op/abbrev "^ 347 KernelSig.name_toString k ^ 348 "; arbitrarily keeping map to "^ 349 PP.pp_to_string (!Globals.linewidth) 350 (pp_type G) 351 (structure_to_type v0)); 352 newdict) 353 else 354 newdict 355in 356 Binarymap.foldr merge_dictinsert d1 d2 357end 358 359fun merge_pmaps (p1, p2) = 360 TypeNet.fold (fn (ty,v,acc) => TypeNet.insert(acc,ty,v)) p1 p2 361 362fun merge_privs (p1, p2) = 363 Binarymap.foldl (fn (nm,thy,acc) => Binarymap.insert(acc,nm,thy)) p1 p2 364 365fun merge_grammars (G1, G2) = let 366 (* both grammars are sorted, with no adjacent suffixes *) 367 val TYG { rules = grules1, parse_str = abbrevs1, 368 str_print = pmap1, tstamp = t1, bare_names = priv1 } = G1 369 val TYG { rules = grules2, parse_str = abbrevs2, 370 str_print = pmap2, tstamp = t2, bare_names = priv2 } = G2 371 fun merge_acc acc (gs as (g1, g2)) = 372 case gs of 373 ([], _) => rev_append acc g2 374 | (_, []) => rev_append acc g1 375 | ((g1rule as (g1k, g1v))::g1rest, (g2rule as (g2k, g2v))::g2rest) => let 376 in 377 case Int.compare (g1k, g2k) of 378 LESS => merge_acc (g1rule::acc) (g1rest, g2) 379 | GREATER => merge_acc (g2rule::acc) (g1, g2rest) 380 | EQUAL => merge_acc ((g1k, merge g1v g2v)::acc) (g1rest, g2rest) 381 end 382in 383 TYG { rules = merge_acc [] (grules1, grules2), 384 parse_str = merge_abbrevs G2 (abbrevs1, abbrevs2), 385 str_print = merge_pmaps (pmap1, pmap2), 386 bare_names = merge_privs (priv1, priv2), 387 tstamp = Int.max(t1,t2) + 1 } 388end 389 390fun can_print pmap kns ty = 391 let 392 val net_matches = TypeNet.match(pmap, ty) 393 fun check_match (pat, (tstamp, nm)) = 394 can (Type.match_type pat) ty andalso nm = kns 395 in 396 not (null (List.filter check_match net_matches)) 397 end 398 399fun prettyprint_grammar G = let 400 open Portable Lib HOLPP 401 val TYG grm = G 402 val {rules=g, parse_str=abbrevs, str_print=pmap, bare_names,... } = grm 403 fun print_suffix (s,arity) = let 404 fun print_ty_n_tuple n = 405 case n of 406 0 => [] 407 | 1 => [add_string "TY", add_break (1,0)] 408 | n => [add_string "(", 409 block INCONSISTENT 0 410 (tabulateWith (fn _ => add_string "TY") 411 [add_string ",", add_break(1,0)] 412 n), 413 add_string ")", add_break(1,0)] 414 in 415 block CONSISTENT 2 416 (print_ty_n_tuple arity @ [add_string s]) 417 end 418 419 fun print_abbrev lwidth (kid, kidstr0, st) = let 420 val kidstr = UTF8.padRight #" " (lwidth + 4) kidstr0 421 val ty = structure_to_type st 422 val printed = can_print pmap kid ty 423 val ty_string = PP.pp_to_string 100 424 (Feedback.trace ("print_tyabbrevs", 0) (pp_type G)) 425 ty 426 in 427 block INCONSISTENT 0 ( 428 add_string kidstr :: add_string "=" :: add_break(1,0) :: 429 add_string (UTF8.padRight #" " (35 - lwidth) ty_string) :: 430 (if not printed then 431 [add_break(1,lwidth + 6), add_string "[not printed]"] 432 else []) 433 ) 434 end 435 436 fun kid_string kid st = 437 let 438 val ispriv = case Binarymap.peek (bare_names, #Name kid) of 439 SOME thy => thy = #Thy kid 440 | NONE => false 441 val kns = if ispriv then #Name kid else KernelSig.name_toString kid 442 val paramstr = PP.pp_to_string 100 (pp_type G) o structure_to_type o PARAM 443 in 444 case num_params st of 445 0 => kns 446 | 1 => paramstr 0 ^ " " ^ kns 447 | n => "(" ^ String.concatWith ", " (List.tabulate(n, paramstr)) ^ 448 ") " ^ kns 449 end 450 451 val print_abbrevs = let 452 fun foldthis (k,st,acc as (mx,kstrs)) = 453 if typstruct_uptodate st then 454 let 455 val kstr = kid_string k st 456 in 457 (Int.max(mx,size kstr), (k,kstr,st)::kstrs) 458 end 459 else acc 460 val (lwidth, okabbrevs) = Binarymap.foldl foldthis (0, []) abbrevs 461 in 462 if length okabbrevs > 0 then [ 463 NL, add_string "Type abbreviations:", 464 add_break(2,2), 465 block CONSISTENT 0 ( 466 pr_list (print_abbrev lwidth) [NL] (List.rev okabbrevs) 467 ) 468 ] 469 else [] 470 end 471 472 fun print_infix {opname,parse_string} = 473 block INCONSISTENT 0 ( 474 [add_string "TY ",add_string parse_string,add_break(1,0),add_string "TY"]@ 475 (if opname <> parse_string then 476 [add_break(1,0), add_string ("["^opname^"]")] 477 else []) 478 ) 479 480 fun print_suffixes slist = let 481 val oksl = List.mapPartial (suffix_arity (abbrevs, bare_names)) slist 482 in 483 if null oksl then [] 484 else 485 [ 486 block INCONSISTENT 0 [ 487 add_string " TY ::= ", 488 block INCONSISTENT 16 ( 489 pr_list print_suffix [add_string " |", add_break(1,0)] oksl 490 ) 491 ] 492 ] 493 end 494 495 fun print_rule0 r = 496 case r of 497 INFIX(oplist, assoc) => let 498 val assocstring = 499 case assoc of 500 LEFT => "L-" 501 | RIGHT => "R-" 502 | NONASSOC => "non-" 503 in 504 [add_string "TY ::= ", 505 block INCONSISTENT 0 506 (pr_list print_infix [add_string " |", add_break(1,0)] oplist @ 507 [add_string (" ("^assocstring^"associative)")])] 508 end 509 fun print_rule (n, r) = let 510 val precstr = StringCvt.padRight #" " 7 ("("^Int.toString n^")") 511 in 512 block CONSISTENT 0 (add_string precstr :: print_rule0 r) 513 end 514in 515 block CONSISTENT 0 ( 516 block CONSISTENT 0 [ 517 add_string "Rules:", 518 add_break (1,2), 519 block CONSISTENT 0 ( 520 pr_list print_rule [NL] g @ [add_break(1,0)] @ 521 print_suffixes (keys bare_names) @ 522 [add_break(1,0), add_string " TY ::= TY[TY] (array type)"] 523 ) 524 ] :: print_abbrevs 525 ) 526end; 527 528val print_abbrevs = ref true 529val _ = Feedback.register_btrace ("print_tyabbrevs", print_abbrevs) 530 531fun tysize ty = 532 if Type.is_vartype ty then 1 533 else let 534 val {Args,...} = Type.dest_thy_type ty 535 in 536 1 + List.foldl (fn (ty,acc) => tysize ty + acc) 0 Args 537 end 538 539fun dest_type' ty = let 540 val {Thy, Tyop, Args} = Type.dest_thy_type ty 541in 542 {Thy = SOME Thy, Tyop = Tyop, Args = Args} 543end 544 545fun abb_dest_type0 (TYG{str_print = pmap, bare_names, ...}) ty = let 546 open HolKernel 547 val net_matches = TypeNet.match(pmap, ty) 548 fun mymatch pat ty = let 549 val (i, sames) = Type.raw_match_type pat ty ([], []) 550 in 551 i @ (map (fn ty => ty |-> ty) sames) 552 end 553 fun check_match (pat, (tstamp, nm)) = 554 SOME(mymatch pat ty, nm, tstamp) handle HOL_ERR _ => NONE 555 val checked_matches = List.mapPartial check_match net_matches 556 fun instcmp ({redex = r1, ...}, {redex = r2, ...}) = Type.compare(r1, r2) 557in 558 case checked_matches of 559 [] => dest_type' ty 560 | _ => let 561 fun instsize i = 562 List.foldl (fn ({redex,residue},acc) => tysize residue + acc) 0 i 563 fun match_info (i, _, tstamp) = (instsize i, tstamp) 564 val matchcmp = inv_img_cmp match_info 565 (pair_compare(Int.compare, 566 Lib.flip_order o Int.compare)) 567 val allinsts = Listsort.sort matchcmp checked_matches 568 val (inst,{Thy,Name},_) = hd allinsts 569 val inst' = Listsort.sort instcmp inst 570 val args = map #residue inst' 571 in 572 case Binarymap.peek (bare_names, Name) of 573 NONE => {Thy = SOME Thy, Tyop = Name, Args = args} 574 | SOME thy' => if Thy = thy' then {Thy = NONE, Tyop = Name, Args = args} 575 else {Thy = SOME Thy, Tyop = Name, Args = args} 576 end 577end 578 579fun abb_dest_type G ty = if !print_abbrevs then abb_dest_type0 G ty 580 else dest_type' ty 581 582fun disable_abbrev_printing s (g as TYG grm) = let 583 val (thyopt, nm) = break_qident s 584 fun rmprints namecheck g = 585 let 586 fun foldthis (ty, i as (_, knm), acc) = 587 if namecheck knm then acc else TypeNet.insert(acc,ty,i) 588 val pmap' = TypeNet.fold foldthis TypeNet.empty (print_map g) 589 in 590 fupdate_str_print (K pmap') g 591 end 592in 593 case thyopt of 594 NONE => rmprints (fn knm => #Name knm = nm) g 595 | SOME thy => rmprints (fn knm => knm = {Name = nm, Thy = thy}) g 596end 597 598(* ---------------------------------------------------------------------- 599 min grammar 600 601 Grammar that knows about types bool and ind, as well as the operator 602 fun, which also has an infix -> presentation 603 ---------------------------------------------------------------------- *) 604 605fun nparams s n = TYOP {Thy = "min", Tyop = s, 606 Args = List.tabulate(n, PARAM)} 607val funty = Type.-->(Type.alpha,Type.beta) 608val indty = Type.mk_thy_type {Thy = "min", Tyop = "ind", Args = []} 609 610fun insert_minop (s,arity,ty) g = 611 let 612 val kid = {Thy = "min", Name = s} 613 in 614 g |> fupdate_parse_str (fn m => Binarymap.insert(m,kid, nparams s arity)) 615 |> fupdate_str_print (fn n => TypeNet.insert(n,ty,(tstamp g, kid))) 616 |> fupdate_bare_names (fn m => Binarymap.insert(m,s,"min")) 617 |> fupdate_tstamp (fn i => i + 1) 618 end 619 620 621val fun_rule = (50,INFIX([{opname = "fun", parse_string = "->"}], RIGHT)) 622 623val min_grammar = 624 empty_grammar 625 |> fupdate_rules (K [fun_rule]) 626 |> insert_minop ("ind", 0, indty) 627 |> insert_minop ("bool", 0, Type.bool) 628 |> insert_minop ("fun", 2, funty) 629 630fun apply_delta d g = 631 case d of 632 NEW_TYPE kid => new_qtyop kid g 633 | NEW_INFIX {Name,ParseName,Assoc,Prec} => 634 new_binary_tyop g {precedence=Prec, infix_form = ParseName, 635 opname = Name, associativity = Assoc} 636 | TYABBREV (kid,ty,prp) => new_abbreviation {knm=kid,ty=ty,print=prp} g 637 | DISABLE_TYPRINT s => disable_abbrev_printing s g 638 | RM_KNM_TYABBREV kid => remove_knm_abbreviation g kid 639 | RM_TYABBREV s => remove_abbreviation g s 640 641 642fun apply_deltas ds g = 643 List.foldl (uncurry apply_delta) g ds 644 645fun delta_toString d = 646 case d of 647 NEW_TYPE kid => "NEW_TYPE" ^ KernelSig.name_toString kid 648 | NEW_INFIX {Name,ParseName,Assoc,Prec} => 649 "NEW_INFIX{Name=\"" ^ String.toString Name ^ "\",ParseName=\"" ^ 650 String.toString ParseName ^ "...}" 651 | _ => "" 652 653end 654