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