1structure Parse :> Parse = 2struct 3 4open Feedback HolKernel HOLgrammars GrammarSpecials term_grammar type_grammar 5open term_grammar_dtype 6 7type pp_element = term_grammar.pp_element 8type PhraseBlockStyle = term_grammar.PhraseBlockStyle 9type ParenStyle = term_grammar.ParenStyle 10type block_info = term_grammar.block_info 11type associativity = HOLgrammars.associativity 12type 'a frag = 'a Portable.frag 13type 'a pprinter = 'a -> HOLPP.pretty 14 15val ERROR = mk_HOL_ERR "Parse"; 16val ERRORloc = mk_HOL_ERRloc "Parse"; 17val WARN = HOL_WARNING "Parse" 18 19val post_process_term = Preterm.post_process_term 20val quote = Lib.mlquote 21 22fun acc_strip_comb M rands = 23 let val (Rator,Rand) = dest_comb M 24 in acc_strip_comb Rator (Rand::rands) 25 end 26 handle HOL_ERR _ => (M,rands); 27 28fun strip_comb tm = acc_strip_comb tm []; 29 30val dest_forall = sdest_binder ("!","bool") (ERROR "dest_forall" ""); 31 32fun strip_forall fm = 33 let val (Bvar,Body) = dest_forall fm 34 val (bvs,core) = strip_forall Body 35 in (Bvar::bvs, core) 36 end handle HOL_ERR _ => ([],fm); 37 38fun lhs tm = #2(sdest_binop("=","min") (ERROR"lhs" "") tm); 39 40fun ftoString [] = "" 41 | ftoString (QUOTE s :: rest) = s ^ ftoString rest 42 | ftoString (ANTIQUOTE x :: rest) = "..." ^ ftoString rest 43 44fun lose_constrec_ty {Name,Thy,Ty} = {Name = Name, Thy = Thy} 45 46(*--------------------------------------------------------------------------- 47 Fixity stuff 48 ---------------------------------------------------------------------------*) 49 50val Infixl = fn i => Infix(LEFT, i) 51val Infixr = fn i => Infix(RIGHT, i) 52 53 54(*--------------------------------------------------------------------------- 55 pervasive type grammar 56 ---------------------------------------------------------------------------*) 57 58(* type grammar *) 59val the_type_grammar = ref type_grammar.min_grammar 60val type_grammar_changed = ref false 61fun type_grammar() = !the_type_grammar 62 63(*--------------------------------------------------------------------------- 64 pervasive term grammar 65 ---------------------------------------------------------------------------*) 66 67val the_term_grammar = ref term_grammar.min_grammar 68val term_grammar_changed = ref false 69fun term_grammar () = (!the_term_grammar) 70 71fun current_grammars() = (type_grammar(), term_grammar()); 72 73(* ---------------------------------------------------------------------- 74 Pervasive pretty-printing backend 75 ---------------------------------------------------------------------- *) 76 77fun interactive_ppbackend () = let 78 open PPBackEnd OS.Process 79in 80 (* assumes interactive *) 81 case getEnv "TERM" of 82 SOME s => if String.isPrefix "xterm" s then vt100_terminal 83 else raw_terminal 84 | _ => raw_terminal 85end 86 87val current_backend : PPBackEnd.t ref = 88 ref (if !Globals.interactive then interactive_ppbackend() 89 else PPBackEnd.raw_terminal) 90 91fun rawterm_pp f x = 92 Lib.with_flag(current_backend, PPBackEnd.raw_terminal) f x 93 94fun mlower m = 95 case smpp.lower m term_pp_utils.dflt_pinfo of 96 NONE => raise Fail "p/printer returned NONE!" 97 | SOME(p, _, _) => p 98 99fun ulower fm x = mlower (fm x) 100 101(*--------------------------------------------------------------------------- 102 local grammars 103 ---------------------------------------------------------------------------*) 104 105val the_lty_grm = ref type_grammar.empty_grammar 106val the_ltm_grm = ref term_grammar.stdhol 107fun current_lgrms() = (!the_lty_grm, !the_ltm_grm); 108 109 110fun fixity s = term_grammar.get_precedence (term_grammar()) s 111 112(*--------------------------------------------------------------------------- 113 Mysterious stuff 114 ---------------------------------------------------------------------------*) 115 116(* type parsing *) 117 118val ty_antiq = parse_type.ty_antiq; 119val dest_ty_antiq = parse_type.dest_ty_antiq; 120val is_ty_antiq = parse_type.is_ty_antiq; 121 122local 123 open parse_type Pretype 124in 125val type_parser1 = 126 ref (parse_type termantiq_constructors false (type_grammar())) 127val type_parser2 = 128 ref (parse_type typantiq_constructors false (type_grammar())) 129end 130 131(*--------------------------------------------------------------------------- 132 pretty printing types 133 ---------------------------------------------------------------------------*) 134 135val type_printer = ref (type_pp.pp_type (type_grammar())) 136 137val grammar_term_printer = 138 ref (term_pp.pp_term (term_grammar()) (type_grammar())) 139fun pp_grammar_term pps t = (!grammar_term_printer) (!current_backend) pps t 140 141val term_printer = ref pp_grammar_term 142 143fun get_term_printer () = ulower (!term_printer) 144 145fun set_term_printer new_pp_term = 146 let 147 open smpp 148 val old_pp_term = !term_printer 149 in 150 term_printer := lift new_pp_term; 151 ulower old_pp_term 152 end 153 154 155 156fun update_type_fns () = 157 if !type_grammar_changed then let 158 open Pretype parse_type 159 in 160 type_parser1 := parse_type termantiq_constructors false (type_grammar()); 161 type_parser2 := parse_type typantiq_constructors false (type_grammar()); 162 type_printer := type_pp.pp_type (type_grammar()); 163 type_grammar_changed := false 164 end 165 else () 166 167val dflt_pinfo = term_pp_utils.dflt_pinfo 168 169fun pp_type ty = 170 let 171 open smpp 172 val _ = update_type_fns() 173 val mptr = smpp.add_string ":" >> !type_printer (!current_backend) ty 174 in 175 lower mptr dflt_pinfo |> valOf |> #1 176 end 177 178val type_to_string = rawterm_pp (ppstring pp_type) 179val print_type = print o type_to_string 180 181fun type_pp_with_delimiters ppfn ty = 182 let 183 open Portable Globals smpp 184 in 185 mlower ( 186 add_string (!type_pp_prefix) >> 187 block CONSISTENT (UTF8.size (!type_pp_prefix)) (lift ppfn ty) >> 188 add_string (!type_pp_suffix) 189 ) 190 end 191 192fun print_from_grammars (tyG, tmG) = 193 (ulower (type_pp.pp_type tyG (!current_backend)), 194 ulower (term_pp.pp_term tmG tyG (!current_backend))) 195 196fun stdprint x = 197 HOLPP.prettyPrint (TextIO.print, !Globals.linewidth) x 198 199fun print_term_by_grammar Gs t = 200 let 201 val (_, termprinter) = print_from_grammars Gs 202 in 203 stdprint (termprinter t) ; 204 print "\n" 205end 206 207val min_grammars = (type_grammar.min_grammar, term_grammar.min_grammar) 208 209type grammarDB_info = type_grammar.grammar * term_grammar.grammar 210val grammarDB_value = 211 ref (Binarymap.mkDict String.compare :(string,grammarDB_info)Binarymap.dict) 212fun grammarDB s = Binarymap.peek (!grammarDB_value, s) 213fun grammarDB_fold f acc = Binarymap.foldl f acc (!grammarDB_value) 214fun grammarDB_insert (s, i) = 215 grammarDB_value := Binarymap.insert(!grammarDB_value, s, i) 216 217val _ = grammarDB_insert("min", min_grammars) 218 219fun minprint t = let 220 fun default t = let 221 val (_, baseprinter) = 222 with_flag (current_backend, PPBackEnd.raw_terminal) 223 print_from_grammars 224 min_grammars 225 val printer = 226 baseprinter 227 |> trace ("types", 1) |> trace ("Greek tyvars", 0) 228 |> with_flag (max_print_depth, ~1) 229 val t_str = 230 String.toString (PP.pp_to_string 1000000 printer t) 231 in 232 String.concat ["(#2 (parse_from_grammars min_grammars)", 233 "[QUOTE \"", t_str, "\"])"] 234 end 235in 236 if is_const t then let 237 val {Name,Thy,...} = dest_thy_const t 238 val t' = prim_mk_const {Name = Name, Thy = Thy} 239 in 240 if aconv t t' then 241 String.concat ["(Term.prim_mk_const { Name = ", 242 quote Name, ", Thy = ", 243 quote Thy, "})"] 244 else default t 245 end 246 else default t 247end 248 249(*--------------------------------------------------------------------------- 250 Parsing types 251 ---------------------------------------------------------------------------*) 252 253local open parse_type 254in 255fun parse_Type parser q = let 256 open base_tokens qbuf 257 val qb = new_buffer q 258in 259 case qbuf.current qb of 260 (BT_Ident s,locn) => 261 if String.sub(s, 0) <> #":" then 262 raise ERRORloc "parse_Type" locn "types must begin with a colon" 263 else let 264 val _ = if size s = 1 then advance qb 265 else let val locn' = locn.move_start 1 locn in 266 replace_current (BT_Ident (String.extract(s, 1, NONE)),locn') qb end 267 val pt = parser qb 268 in 269 case current qb of 270 (BT_EOI,_) => Pretype.toType pt 271 | (_,locn) => raise ERRORloc "parse_Type" locn 272 ("Couldn't make any sense of remaining input.") 273 end 274 | (_,locn) => raise ERRORloc "parse_Type" locn "types must begin with a colon" 275end 276end (* local *) 277 278fun Type q = let in 279 update_type_fns(); 280 parse_Type (!type_parser2) q 281 end 282 283fun == q x = Type q; 284 285 286(*--------------------------------------------------------------------------- 287 Parsing into abstract syntax 288 ---------------------------------------------------------------------------*) 289 290val the_absyn_parser: (term frag list -> Absyn.absyn) ref = 291 ref (TermParse.absyn (!the_term_grammar) (!the_type_grammar)) 292 293fun update_term_fns() = let 294 val _ = update_type_fns() 295in 296 if !term_grammar_changed then let 297 in 298 grammar_term_printer := term_pp.pp_term (term_grammar()) (type_grammar()); 299 the_absyn_parser := TermParse.absyn (!the_term_grammar) (!the_type_grammar); 300 term_grammar_changed := false 301 end 302 else () 303end 304 305fun Absyn q = let 306in 307 update_term_fns(); 308 !the_absyn_parser q 309end 310 311(* Pretty-print the grammar rules *) 312fun print_term_grammar() = let 313 fun tmprint g = snd (print_from_grammars (!the_type_grammar,g)) 314 fun ppg g = let 315 open smpp 316 in 317 block PP.CONSISTENT 0 ( 318 prettyprint_grammar_rules (lift o tmprint) (ruleset g) >> 319 add_newline 320 ) 321 end 322in 323 stdprint (ulower ppg (!the_term_grammar)) 324end 325 326 327(* Pretty-printing terms and types without certain overloads or abbreviations *) 328 329fun overload_info_for s = let 330 val (g,(ls1,ls2)) = term_grammar.mfupdate_overload_info 331 (Overload.remove_overloaded_form s) 332 (!the_term_grammar) 333 val (_,ppfn0) = print_from_grammars (!the_type_grammar,g) 334 val ppfn = ppfn0 |> Feedback.trace ("types", 1) 335 val ppaction = let 336 open smpp 337 in 338 block PP.CONSISTENT 0 339 (add_string (s ^ " parses to:") >> 340 add_break(1,2) >> 341 block PP.INCONSISTENT 0 (pr_list (lift ppfn) add_newline ls1) >> 342 add_newline >> 343 add_string (s ^ " might be printed from:") >> 344 add_break(1,2) >> 345 block PP.INCONSISTENT 0 (pr_list (lift ppfn) add_newline ls2) >> 346 add_newline) 347 end 348 fun act_topp pps a = ignore (a ((), pps)) 349in 350 stdprint (mlower ppaction) 351end 352 353fun pp_term_without_overloads_on ls t = let 354 fun remove s = #1 o term_grammar.mfupdate_overload_info 355 (Overload.remove_overloaded_form s) 356 val g = Lib.itlist remove ls (!the_term_grammar) 357in 358 #2 (print_from_grammars (!the_type_grammar,g)) t 359end 360fun pp_term_without_overloads ls t = let 361 fun remove (s,t) = term_grammar.fupdate_overload_info 362 (Overload.gen_remove_mapping s t) 363 val g = Lib.itlist remove ls (!the_term_grammar) 364in 365 #2 (print_from_grammars (!the_type_grammar,g)) t 366end 367fun pp_type_without_abbrevs ls ty = let 368 val g = Lib.itlist type_grammar.disable_abbrev_printing ls (!the_type_grammar) 369in 370 #1 (print_from_grammars (g,!the_term_grammar)) ty 371end 372 373(* ---------------------------------------------------------------------- 374 Top-level pretty-printing entry-points 375 ---------------------------------------------------------------------- *) 376 377fun pp_style_string (st, s) = 378 let open Portable PPBackEnd 379 val {add_string,ustyle,...} = (!current_backend) 380 val m = ustyle st (add_string s) 381 in 382 mlower m 383 end 384 385fun add_style_to_string st s = ppstring pp_style_string (st, s); 386fun print_with_style st s = stdprint (pp_style_string (st,s)) 387 388fun pp_term t = (update_term_fns(); mlower (!term_printer t)) 389 390val term_to_string = rawterm_pp (ppstring pp_term) 391fun print_term t = stdprint (rawterm_pp pp_term t) 392 393fun term_pp_with_delimiters ppfn tm = 394 let 395 open Portable Globals smpp 396 in 397 mlower ( 398 add_string (!term_pp_prefix) >> 399 block CONSISTENT (UTF8.size (!term_pp_prefix)) (lift ppfn tm) >> 400 add_string (!term_pp_suffix) 401 ) 402 end 403 404fun pp_thm th = 405 let 406 open Portable smpp 407 val prt = lift pp_term 408 fun repl ch alist = CharVector.tabulate (length alist, fn _ => ch) 409 fun pp_terms b L = 410 block INCONSISTENT 1 ( 411 add_string "[" >> 412 (if b then pr_list prt (add_string "," >> add_break(1,0)) L 413 else add_string (repl #"." L)) >> 414 add_string "]" 415 ) 416 val m = 417 block INCONSISTENT 0 ( 418 if !Globals.max_print_depth = 0 then add_string " ... " 419 else 420 let 421 open Globals 422 val (tg,asl,st,sa) = (tag th, hyp th, !show_tags, !show_assums) 423 in 424 (if not st andalso not sa andalso null asl then nothing 425 else 426 (if st then lift Tag.pp_tag tg else nothing) >> 427 add_break(1,0) >> pp_terms sa asl >> add_break(1,0)) >> 428 add_string (!Globals.thm_pp_prefix) >> 429 block CONSISTENT (UTF8.size (!Globals.thm_pp_prefix)) 430 (prt (concl th)) >> 431 add_string (!Globals.thm_pp_suffix) 432 end 433 ) 434 in 435 mlower m 436 end; 437 438val thm_to_string = rawterm_pp (ppstring pp_thm) 439val print_thm = print o thm_to_string 440 441(*--------------------------------------------------------------------------- 442 Parse into preterm type 443 ---------------------------------------------------------------------------*) 444 445fun absyn_to_preterm a = TermParse.absyn_to_preterm (term_grammar()) a 446 447fun Preterm q = 448 case (q |> Absyn |> absyn_to_preterm) Pretype.Env.empty of 449 errormonad.Error e => raise Preterm.mkExn e 450 | errormonad.Some (_, pt) => pt 451 452val absyn_to_term = 453 TermParse.absyn_to_term (SOME (term_to_string, type_to_string)) 454 455 456(*--------------------------------------------------------------------------- 457 Parse into term type. 458 ---------------------------------------------------------------------------*) 459 460fun Term q = absyn_to_term (term_grammar()) (Absyn q) 461 462fun typedTerm qtm ty = 463 let fun trail s = [QUOTE (s^"):"), ANTIQUOTE(ty_antiq ty), QUOTE""] 464 in 465 Term (case (Lib.front_last qtm) 466 of ([],QUOTE s) => trail ("("^s) 467 | (QUOTE s::rst, QUOTE s') => (QUOTE ("("^s)::rst) @ trail s' 468 | _ => raise ERROR"typedTerm" "badly formed quotation") 469 end; 470 471fun parse_from_grammars (tyG, tmG) = let 472 val ty_parser = parse_type.parse_type Pretype.typantiq_constructors false tyG 473 val tm_parser = absyn_to_term tmG o TermParse.absyn tmG tyG 474in 475 (parse_Type ty_parser, tm_parser) 476end 477 478(* ---------------------------------------------------------------------- 479 parsing in context 480 ---------------------------------------------------------------------- *) 481 482fun smashErrm m = 483 case m Pretype.Env.empty of 484 errormonad.Error e => raise Preterm.mkExn e 485 | errormonad.Some (_, result) => result 486val stdprinters = SOME(term_to_string,type_to_string) 487 488fun parse_in_context FVs q = 489 let 490 open errormonad 491 val m = 492 (q |> Absyn |> absyn_to_preterm) >- 493 TermParse.ctxt_preterm_to_term stdprinters NONE FVs 494 in 495 smashErrm m 496 end 497 498fun grammar_parse_in_context(tyg,tmg) ctxt q = 499 TermParse.ctxt_term stdprinters tmg tyg NONE ctxt q |> smashErrm 500 501fun grammar_typed_parses_in_context (tyg,tmg) ty ctxt q = 502 TermParse.ctxt_termS tmg tyg (SOME ty) ctxt q 503 504fun grammar_typed_parse_in_context gs ty ctxt q = 505 case seq.cases (grammar_typed_parses_in_context gs ty ctxt q) of 506 SOME(tm, _) => tm 507 | NONE => raise ERROR "grammar_typed_parse_in_context" "No consistent parse" 508 509fun typed_parse_in_context ty ctxt q = 510 let 511 fun mkA q = Absyn.TYPED(locn.Loc_None, Absyn q, Pretype.fromType ty) 512 in 513 case seq.cases (TermParse.prim_ctxt_termS mkA (term_grammar()) ctxt q) of 514 SOME (tm, _) => tm 515 | NONE => raise ERROR "typed_parse_in_context" "No consistent parse" 516 end 517 518(*--------------------------------------------------------------------------- 519 Making temporary and persistent changes to the grammars. 520 ---------------------------------------------------------------------------*) 521 522val grm_updates = ref [] : (string * string * term option) list ref; 523 524fun update_grms fname (x,y) = grm_updates := ((x,y,NONE) :: !grm_updates); 525fun full_update_grms (x,y,opt) = grm_updates := ((x,y,opt) :: !grm_updates) 526 527fun apply_udeltas uds = 528 let 529 in 530 term_grammar_changed := true; 531 the_term_grammar := 532 List.foldl (uncurry term_grammar.add_delta) (term_grammar()) uds 533 end 534 535fun temp_prefer_form_with_tok r = let open term_grammar in 536 the_term_grammar := prefer_form_with_tok r (term_grammar()); 537 term_grammar_changed := true 538 end 539 540fun prefer_form_with_tok (r as {term_name,tok}) = let in 541 temp_prefer_form_with_tok r; 542 update_grms "prefer_form_with_tok" 543 ("temp_prefer_form_with_tok", 544 String.concat ["{term_name = ", quote term_name, 545 ", tok = ", quote tok, "}"]) 546 end 547 548 549fun temp_set_grammars(tyG, tmG) = let 550in 551 the_term_grammar := tmG; 552 the_type_grammar := tyG; 553 term_grammar_changed := true; 554 type_grammar_changed := true 555end 556 557structure Unicode = 558struct 559 560 structure UChar = UnicodeChars 561 fun unicode_version r = 562 let 563 open ProvideUnicode 564 val uds = mk_unicode_version r (term_grammar()) 565 in 566 apply_udeltas uds; 567 List.app GrammarDeltas.record_tmdelta uds 568 end 569 570 fun temp_unicode_version r = 571 ProvideUnicode.mk_unicode_version r (term_grammar()) |> apply_udeltas 572 573end 574 575fun core_process_tyds f x k = 576 let 577 open type_grammar 578 val tyds = f x 579 in 580 the_type_grammar := 581 List.foldl (uncurry apply_delta) (!the_type_grammar) tyds; 582 type_grammar_changed := true; 583 term_grammar_changed := true; 584 k tyds 585 end 586 587fun mk_temp_tyd f x = core_process_tyds f x (fn uds => ()) 588fun mk_perm_tyd f x = 589 core_process_tyds f x (List.app GrammarDeltas.record_tydelta) 590 591fun add_qtype0 kid = [NEW_TYPE kid] 592 593val temp_add_qtype = mk_temp_tyd add_qtype0 594val add_qtype = mk_perm_tyd add_qtype0 595 596fun temp_add_type s = temp_add_qtype {Thy=current_theory(), Name = s} 597fun add_type s = add_qtype {Thy=current_theory(), Name = s} 598 599fun add_infix_type0 {Name,ParseName,Assoc,Prec} = 600 let 601 val pnm = case ParseName of NONE => Name | SOME s => s 602 in 603 [NEW_INFIX{Prec=Prec,ParseName=pnm,Name=Name,Assoc=Assoc}] 604 end 605 606val temp_add_infix_type = mk_temp_tyd add_infix_type0 607val add_infix_type = mk_perm_tyd add_infix_type0 608 609fun replace_exnfn fnm f x = 610 f x handle HOL_ERR {message = m, origin_structure = s, ...} => 611 raise HOL_ERR {message = m, origin_function = fnm, 612 origin_structure = s} 613 614fun thytype_abbrev0 r = [TYABBREV r] 615 616val temp_thytype_abbrev = mk_temp_tyd thytype_abbrev0 617val thytype_abbrev = mk_perm_tyd thytype_abbrev0 618 619fun temp_type_abbrev (s, ty) = 620 replace_exnfn "temp_type_abbrev" temp_thytype_abbrev 621 ({Thy = Theory.current_theory(), Name = s}, ty) 622 623fun type_abbrev (s, ty) = 624 replace_exnfn "type_abbrev" thytype_abbrev 625 ({Thy = Theory.current_theory(), Name = s}, ty) 626 627fun disable_tyabbrev_printing0 s = [DISABLE_TYPRINT s] 628val temp_disable_tyabbrev_printing = mk_temp_tyd disable_tyabbrev_printing0 629val disable_tyabbrev_printing = mk_perm_tyd disable_tyabbrev_printing0 630 631fun remove_type_abbrev0 s = [RM_TYABBREV s] 632val temp_remove_type_abbrev = mk_temp_tyd remove_type_abbrev0 633val remove_type_abbrev = mk_perm_tyd remove_type_abbrev0 634 635(* Not persistent? *) 636fun temp_set_associativity (i,a) = let in 637 the_term_grammar := set_associativity_at_level (term_grammar()) (i,a); 638 term_grammar_changed := true 639 end 640 641fun block_infoToString (Portable.CONSISTENT, n) = 642 "(Portable.CONSISTENT, "^Int.toString n^")" 643 | block_infoToString (Portable.INCONSISTENT, n) = 644 "(Portable.INCONSISTENT, "^Int.toString n^")" 645 646fun ParenStyleToString Always = "Always" 647 | ParenStyleToString OnlyIfNecessary = "OnlyIfNecessary" 648 | ParenStyleToString ParoundName = "ParoundName" 649 | ParenStyleToString ParoundPrec = "ParoundPrec" 650 | ParenStyleToString NotEvenIfRand = "NotEvenIfRand" 651 652fun BlockStyleToString AroundSameName = "AroundSameName" 653 | BlockStyleToString AroundSamePrec = "AroundSamePrec" 654 | BlockStyleToString AroundEachPhrase = "AroundEachPhrase" 655 | BlockStyleToString NoPhrasing = "NoPhrasing" 656 657 658(*---------------------------------------------------------------------------*) 659(* Apply a function to its argument. If it fails, revert the grammars *) 660(*---------------------------------------------------------------------------*) 661 662fun try_grammar_extension f x = 663 let val (tyG,tmG) = current_grammars() 664 val updates = !grm_updates 665 in 666 f x handle e 667 => (the_term_grammar := tmG; 668 the_type_grammar := tyG; 669 term_grammar_changed := true; 670 type_grammar_changed := true; 671 grm_updates := updates; raise e) 672 end; 673 674fun includes_unicode s = not (CharVector.all (fn c => Char.ord c < 128) s) 675val els_include_unicode = let 676in 677 List.exists (fn RE (TOK s) => includes_unicode s | _ => false) 678end 679 680val unicode_off_but_unicode_act_complaint = ref true 681val _ = register_btrace("Parse.unicode_trace_off_complaints", 682 unicode_off_but_unicode_act_complaint) 683 684fun make_add_rule gr = 685 let 686 in 687 the_term_grammar := term_grammar.add_delta (GRULE gr) (!the_term_grammar); 688 term_grammar_changed := true 689 end handle GrammarError s => raise ERROR "add_rule" ("Grammar error: "^s) 690 691fun core_udprocess f k x = 692 let 693 val uds = f x 694 fun apply_one ud = 695 case ud of 696 GRULE gr => make_add_rule gr 697 | _ => apply_udeltas [ud] 698 in 699 List.app apply_one uds ; 700 k uds 701 end 702 703fun mk_temp f = core_udprocess f (fn uds => ()) 704fun mk_perm f = core_udprocess f (List.app GrammarDeltas.record_tmdelta) 705 706fun remove_termtok0 r = [RMTMTOK r] 707val temp_remove_termtok = mk_temp remove_termtok0 708val remove_termtok = mk_perm remove_termtok0 709 710 711 712val temp_add_rule = mk_temp (fn x => [GRULE x]) 713val add_rule = mk_perm (fn x => [GRULE x]) 714 715fun temp_add_infix(s, prec, associativity) = 716 temp_add_rule (standard_spacing s (Infix(associativity, prec))) 717 718fun add_infix (s, prec, associativity) = 719 add_rule (standard_spacing s (Infix(associativity, prec))) 720 721fun make_overload_on add (s, t) = 722 (the_term_grammar := fupdate_overload_info (add (s, t)) (term_grammar()); 723 term_grammar_changed := true) 724 725val temp_overload_on = 726 make_overload_on Overload.add_overloading 727val temp_inferior_overload_on = 728 make_overload_on Overload.add_inferior_overloading 729 730fun overload_on p = 731 (make_overload_on Overload.add_overloading p ; 732 GrammarDeltas.record_tmdelta (OVERLOAD_ON p)) 733fun inferior_overload_on p = 734 (make_overload_on Overload.add_inferior_overloading p; 735 GrammarDeltas.record_tmdelta (IOVERLOAD_ON p)) 736 737fun add_listform0 x = [GRULE (listform_to_rule x)] 738val temp_add_listform = mk_temp add_listform0 739val add_listform = mk_perm add_listform0 740 741fun add_bare_numeral_form0 x = [ADD_NUMFORM x] 742val temp_add_bare_numeral_form = mk_temp add_bare_numeral_form0 743val add_bare_numeral_form = mk_perm add_bare_numeral_form0 744 745fun temp_give_num_priority c = let open term_grammar in 746 the_term_grammar := give_num_priority (term_grammar()) c; 747 term_grammar_changed := true 748 end 749 750fun give_num_priority c = let in 751 temp_give_num_priority c; 752 update_grms "give_num_priority" ("temp_give_num_priority", 753 String.concat ["#", Lib.quote(str c)]) 754 end 755 756fun temp_remove_numeral_form c = let in 757 the_term_grammar := term_grammar.remove_numeral_form (term_grammar()) c; 758 term_grammar_changed := true 759 end 760 761fun remove_numeral_form c = let in 762 temp_remove_numeral_form c; 763 update_grms "remove_numeral_form" ("temp_remove_numeral_form", 764 String.concat ["#", Lib.quote(str c)]) 765 end 766 767fun associate_restriction0 (bs, s) = 768 let val lambda = #lambda (specials (term_grammar())) 769 val b = if mem bs lambda then NONE else SOME bs 770 in 771 [ASSOC_RESTR{binder = b, resbinder = s}] 772 end 773 774val temp_associate_restriction = mk_temp associate_restriction0 775val associate_restriction = mk_perm associate_restriction0 776 777fun temp_remove_rules_for_term s = let open term_grammar in 778 the_term_grammar := remove_standard_form (term_grammar()) s; 779 term_grammar_changed := true 780 end 781 782fun remove_rules_for_term s = let in 783 temp_remove_rules_for_term s; 784 GrammarDeltas.record_tmdelta (RMTMNM s) 785 end 786 787fun set_mapped_fixity0 (r as {tok,...}) = 788 [RMTOK tok, r |> standard_mapped_spacing |> GRULE] 789fun set_fixity0 (s, f) = set_mapped_fixity0 {fixity = f, term_name = s, tok = s} 790 791 792val temp_set_mapped_fixity = mk_temp set_mapped_fixity0 793val temp_set_fixity = curry (mk_temp set_fixity0) 794val set_mapped_fixity = mk_perm set_mapped_fixity0 795val set_fixity = curry (mk_perm set_fixity0) 796 797(* ---------------------------------------------------------------------- 798 Post-processing : adding user transformations to the parse processs. 799 ---------------------------------------------------------------------- *) 800 801fun temp_add_absyn_postprocessor x = let 802 open term_grammar 803in 804 the_term_grammar := new_absyn_postprocessor x (!the_term_grammar) 805end 806 807val add_absyn_postprocessor = 808 mk_perm (fn s => [ADD_ABSYN_POSTP {codename = s}]) 809 810fun temp_remove_absyn_postprocessor s = 811 let 812 val (g, res) = term_grammar.remove_absyn_postprocessor s (!the_term_grammar) 813 in 814 the_term_grammar := g; 815 res 816 end 817 818fun temp_add_preterm_processor k f = 819 the_term_grammar := term_grammar.new_preterm_processor k f (!the_term_grammar) 820 821fun temp_remove_preterm_processor k = 822 let 823 val (g, res) = term_grammar.remove_preterm_processor k (!the_term_grammar) 824 in 825 the_term_grammar := g; 826 res 827 end 828 829(*------------------------------------------------------------------------- 830 Overloading 831 -------------------------------------------------------------------------*) 832 833fun overload_on_by_nametype0 (s, recd as {Name, Thy}) = let 834 val c = prim_mk_const recd handle HOL_ERR _ => 835 raise ERROR "temp_overload_on_by_nametype" 836 ("No such constant: "^Thy^"$"^Name) 837in 838 [OVERLOAD_ON (s,c)] 839end 840 841val temp_overload_on_by_nametype = curry (mk_temp overload_on_by_nametype0) 842val overload_on_by_nametype = curry (mk_perm overload_on_by_nametype0) 843 844val temp_send_to_back_overload = 845 curry (mk_temp (fn skid => [MOVE_OVLPOSN{frontp = false, skid = skid}])) 846val send_to_back_overload = 847 curry (mk_perm (fn skid => [MOVE_OVLPOSN{frontp = false, skid = skid}])) 848 849val temp_bring_to_front_overload = 850 curry (mk_temp (fn skid => [MOVE_OVLPOSN{frontp = true, skid = skid}])) 851val bring_to_front_overload = 852 curry (mk_perm (fn skid => [MOVE_OVLPOSN{frontp = true, skid = skid}])) 853 854fun clear_overloads_on0 s = 855 CLR_OVL s :: map (fn t => OVERLOAD_ON(s,t)) (Term.decls s) 856val temp_clear_overloads_on = mk_temp clear_overloads_on0 857val clear_overloads_on = mk_perm clear_overloads_on0 858 859fun remove_ovl_mapping0 (s, kid) = [RMOVMAP(s,kid)] 860val temp_remove_ovl_mapping = curry (mk_temp remove_ovl_mapping0) 861val remove_ovl_mapping = curry (mk_perm remove_ovl_mapping0) 862 863val temp_gen_remove_ovl_mapping = curry (mk_temp (fn p => [GRMOVMAP p])) 864val gen_remove_ovl_mapping = curry (mk_perm (fn p => [GRMOVMAP p])) 865 866fun primadd_rcdfld f ovopn (fldname, t) = let 867 val (d,r) = dom_rng (type_of t) 868 handle HOL_ERR _ => 869 raise ERROR f "field selection term must be of type t -> a" 870 val r = mk_var("rcd", d) 871 val recfldname = recsel_special^fldname 872in 873 ovopn(recfldname, mk_abs(r, mk_comb(t, r))) 874end 875 876val temp_add_record_field = 877 primadd_rcdfld "temp_add_record_field" temp_overload_on 878val add_record_field = primadd_rcdfld "add_record_field" overload_on 879 880fun buildfupdt f ovopn (fnm, t) = let 881 val (argtys, rty) = strip_fun (type_of t) 882 val err = ERROR f "fupdate term must be of type (a -> a) -> t -> t" 883 val f = mk_var("f", hd argtys) handle Empty => raise err 884 val x = mk_var("x", hd (tl argtys)) handle Empty => raise err 885 val recfldname = recfupd_special ^ fnm 886in 887 ovopn(recfldname, list_mk_abs([f,x], list_mk_comb(t, [f,x]))) 888end 889 890val temp_add_record_fupdate = 891 buildfupdt "temp_add_record_fupdate" temp_overload_on 892val add_record_fupdate = buildfupdt "add_record_fupdate" overload_on 893 894fun add_numeral_form0 (c, stropt) = let 895 val _ = 896 Lib.can Term.prim_mk_const{Name="NUMERAL", Thy="arithmetic"} 897 orelse 898 raise ERROR "add_numeral_form" 899 ("Numeral support not present; try load \"arithmeticTheory\"") 900 val num = Type.mk_thy_type {Tyop="num", Thy="num",Args = []} 901 val fromNum_type = num --> alpha 902 val const = 903 case stropt of 904 NONE => prim_mk_const {Name = nat_elim_term, Thy = "arithmetic"} 905 | SOME s => 906 case Term.decls s of 907 [] => raise ERROR "add_numeral_form" ("No constant with name "^s) 908 | h::_ => h 909in 910 ADD_NUMFORM (c, stropt) :: OVERLOAD_ON (fromNum_str, const) :: 911 (if isSome stropt then [OVERLOAD_ON (num_injection, const)] else []) 912end 913 914val temp_add_numeral_form = mk_temp add_numeral_form0 915val add_numeral_form = mk_perm add_numeral_form0 916 917(* to print a term using current grammars, 918 but with "non-trivial" overloads deleted *) 919fun print_without_macros tm = 920 let val (tyG, tmG) = current_grammars () ; 921 in print_term_by_grammar (tyG, term_grammar.clear_overloads tmG) tm end ; 922 923(*--------------------------------------------------------------------------- 924 Visibility of identifiers 925 ---------------------------------------------------------------------------*) 926 927fun hide s = let 928 val (newg, (tms1,tms2)) = 929 mfupdate_overload_info (Overload.remove_overloaded_form s) 930 (!the_term_grammar) 931 fun to_nthyrec t = let 932 val {Name,Thy,Ty} = dest_thy_const t 933 in 934 SOME {Name = Name, Thy = Thy} 935 end handle HOL_ERR _ => NONE 936 937in 938 the_term_grammar := newg; 939 term_grammar_changed := true; 940 (List.mapPartial to_nthyrec tms1, List.mapPartial to_nthyrec tms2) 941end; 942 943fun update_overload_maps s nthyrec_pair = let 944in 945 the_term_grammar := 946 fupdate_overload_info (Overload.raw_map_insert s nthyrec_pair) 947 (term_grammar()); 948 term_grammar_changed := true 949end handle Overload.OVERLOAD_ERR s => 950 raise ERROR "update_overload_maps" ("Overload: "^s) 951 952fun reveal s = 953 case Term.decls s of 954 [] => WARN "reveal" (s^" not a constant; reveal ignored") 955 | cs => let 956 in 957 app (fn c => temp_overload_on (s, c)) cs 958 end 959 960fun known_constants() = term_grammar.known_constants (term_grammar()) 961 962fun is_constname s = let 963 val oinfo = term_grammar.overload_info (term_grammar()) 964in 965 Overload.is_overloaded oinfo s 966end 967 968fun hidden s = 969 let val declared = Term.all_consts() 970 val names = map (fst o Term.dest_const) declared 971 in 972 Lib.mem s (Lib.subtract names (known_constants())) 973 end 974 975fun set_known_constants sl = let 976 val (ok_names, bad_names) = partition (not o null o Term.decls) sl 977 val _ = List.app (fn s => WARN "set_known_constants" 978 (s^" not a constant; ignored")) bad_names 979in 980 the_term_grammar := 981 fupdate_overload_info (K Overload.null_oinfo) (term_grammar()); 982 app reveal ok_names 983end 984 985fun add_const s = let 986 val c = prim_mk_const{Name = s, Thy = current_theory()} 987in 988 overload_on(s,c) 989end; 990 991 992(*---------------------------------------------------------------------- 993 User changes to the printer and parser 994 ----------------------------------------------------------------------*) 995 996fun constant_string_printer s : term_grammar.userprinter = 997 let 998 fun result (tyg, tmg) _ _ ppfns (pgr,lgr,rgr) depth tm = 999 let 1000 val {add_string,...} = ppfns 1001 in 1002 add_string s 1003 end 1004 in 1005 result 1006 end 1007 1008fun temp_add_user_printer (name, pattern, pfn) = let 1009in 1010 the_term_grammar := 1011 term_grammar.add_user_printer (name, pattern, pfn) 1012 (term_grammar()); 1013 term_grammar_changed := true 1014end 1015 1016fun temp_remove_user_printer name = let 1017 val (newg, printfnopt) = 1018 term_grammar.remove_user_printer name (term_grammar()) 1019in 1020 the_term_grammar := newg; 1021 term_grammar_changed := true; 1022 printfnopt 1023end 1024 1025 1026val add_user_printer = 1027 mk_perm (fn (s,t) => [ADD_UPRINTER {codename=s,pattern=t}]) 1028 1029fun remove_user_printer name = let 1030in 1031 update_grms "remove_user_printer" 1032 ("(ignore o temp_remove_user_printer)", mlquote name); 1033 temp_remove_user_printer name 1034end; 1035 1036 1037(*--------------------------------------------------------------------------- 1038 Updating the global and local grammars when a theory file is 1039 loaded. 1040 1041 The function "update_grms" updates both the local and global 1042 grammars by pointer swapping. Ugh! Relies on fact that no 1043 other state than that of the current global grammars changes 1044 in a call to f. 1045 1046 TODO: handle exceptions coming from application of "f" to "x" 1047 and print out informative messages. 1048 ---------------------------------------------------------------------------*) 1049 1050fun update_grms f x = let 1051 val _ = f x (* update global grammars *) 1052 handle HOL_ERR {origin_structure, origin_function, message} => 1053 (WARN "update_grms" 1054 ("Update to global grammar failed in "^origin_function^ 1055 " with message: "^message^"\nproceeding anyway.")) 1056 1057 val (tyG, tmG) = current_grammars() (* save global grm. values *) 1058 val (tyL0,tmL0) = current_lgrms() (* read local grm. values *) 1059 val _ = the_type_grammar := tyL0 (* mv locals into globals *) 1060 val _ = the_term_grammar := tmL0 1061 val _ = f x (* update global (really local) grms *) 1062 handle HOL_ERR {origin_structure, origin_function, message} => 1063 (WARN "update_grms" 1064 ("Update to local grammar failed in "^origin_function^ 1065 " with message: "^message^"\nproceeding anyway.")) 1066 val (tyL1, tmL1) = current_grammars() 1067 val _ = the_lty_grm := tyL1 (* mv updates into locals *) 1068 val _ = the_ltm_grm := tmL1 1069in 1070 the_type_grammar := tyG; (* restore global grm. values *) 1071 the_term_grammar := tmG 1072end 1073 1074fun gparents thyname = 1075 case GrammarAncestry.ancestry {thy = thyname} of 1076 [] => parents thyname 1077 | thys => thys 1078 1079fun gancestry thynm = 1080 let 1081 fun recurse acc seen worklist = 1082 case worklist of 1083 [] => acc 1084 | thynm :: rest => 1085 let 1086 val unseen_ps = 1087 List.filter (fn thy => not (HOLset.member(seen,thy))) 1088 (gparents thynm) 1089 in 1090 recurse (HOLset.add(acc,thynm)) 1091 (HOLset.addList(seen, unseen_ps)) 1092 (unseen_ps @ rest) 1093 end 1094 val empty_strset = HOLset.empty String.compare 1095 in 1096 recurse empty_strset empty_strset (gparents thynm) 1097 end 1098 1099fun merge_into (gname, (G, gset)) = 1100 let 1101 fun apply (tyuds, tmuds) (tyG, tmG) = 1102 (type_grammar.apply_deltas tyuds tyG, term_grammar.add_deltas tmuds tmG) 1103 datatype action = 1104 Visit of string 1105 | Apply of type_grammar.delta list * term_grammar.user_delta list 1106 fun recurse (G, gset) worklist = 1107 case worklist of 1108 [] => (G, gset) 1109 | Visit thy :: rest => 1110 let 1111 val parents0 = gparents thy 1112 val parents = 1113 List.filter (fn thy => not (HOLset.member(gset,thy))) parents0 1114 val uds = GrammarDeltas.thy_deltas {thyname = thy} 1115 in 1116 recurse (G, HOLset.add(gset, thy)) 1117 (map Visit parents @ (Apply uds :: rest)) 1118 end 1119 | Apply uds :: rest => recurse (apply uds G, gset) rest 1120 in 1121 recurse (G, gset) [Visit gname] 1122 end 1123 1124fun merge_grammars slist = 1125 case slist of 1126 [] => raise ERROR "merge_grammars" "Empty grammar list" 1127 | h::t => List.foldl merge_into (valOf (grammarDB h), gancestry h) t |> #1 1128 1129fun set_grammar_ancestry slist = 1130 let 1131 val (tyg,tmg) = merge_grammars slist 1132 in 1133 GrammarAncestry.set_ancestry slist; 1134 the_type_grammar := tyg; 1135 the_term_grammar := tmg; 1136 type_grammar_changed := true; 1137 term_grammar_changed := true 1138 end 1139 1140local fun sig_addn s = String.concat 1141 ["val ", s, "_grammars : type_grammar.grammar * term_grammar.grammar"] 1142 open Portable 1143in 1144fun setup_grammars (oldname, thyname) = let 1145in 1146 if not (null (!grm_updates)) andalso thyname <> oldname then 1147 HOL_WARNING "Parse" "setup_grammars" 1148 ("\"new_theory\" is throwing away grammar changes for "^ 1149 "theory "^oldname^":\n"^ 1150 String.concat (map (fn (s1, s2, _) => s1 ^ " - " ^ s2 ^ "\n") 1151 (!grm_updates))) 1152 else (); 1153 grm_updates := []; 1154 adjoin_to_theory 1155 {sig_ps = SOME (fn _ => PP.add_string (sig_addn thyname)), 1156 struct_ps = SOME (fn _ => 1157 let val B = PP.block CONSISTENT 1158 val IB = PP.block INCONSISTENT 1159 open PP 1160 fun pr_sml_list pfun L = 1161 B 0 [add_string "[", 1162 IB 1 (PP.pr_list pfun [add_string ",", add_break(0,0)] L), 1163 add_string "]"] 1164 fun pp_update(f,x,topt) = 1165 if isSome topt andalso not (Theory.uptodate_term (valOf topt)) 1166 then B 0 [] 1167 else 1168 B 5 [ 1169 add_string "val _ = update_grms", add_break(1,0), 1170 add_string f, add_break(1,0), 1171 B 0 [add_string x] 1172 ] 1173 in 1174 B 0 [ 1175 add_string "local open GrammarSpecials Parse", 1176 NL, 1177 add_string " fun UTOFF f = Feedback.trace(\"Parse.unicode_trace_\ 1178 \off_complaints\",0)f", 1179 NL, 1180 add_string "in", NL, 1181 add_string ("val " ^thyname ^ "_grammars = merge_grammars ["), 1182 IB 0 1183 (pr_list (add_string o quote) 1184 [add_string ",", add_break(1,0)] 1185 (gparents (current_theory()))), 1186 add_string "]", NL, 1187 add_string ("local"), 1188 NL, 1189 add_string ("val (tyUDs, tmUDs) = "^ 1190 "GrammarDeltas.thy_deltas{thyname="^ quote thyname^"}"), 1191 NL, 1192 add_string ("val addtmUDs = term_grammar.add_deltas tmUDs"), 1193 NL, 1194 add_string ("val addtyUDs = type_grammar.apply_deltas tyUDs"), 1195 NL, add_string ("in"), NL, 1196 1197 add_string ("val " ^ thyname ^ "_grammars = "), add_break(1,2), 1198 add_string ("Portable.## (addtyUDs,addtmUDs) " ^ 1199 thyname ^ "_grammars"), 1200 NL, 1201 1202 add_string (String.concat 1203 ["val _ = Parse.grammarDB_insert(",Lib.mlquote thyname,",", 1204 thyname, "_grammars)"]), 1205 NL, 1206 1207 add_string (String.concat 1208 ["val _ = Parse.temp_set_grammars ("^ 1209 "addtyUDs (Parse.type_grammar()), ", 1210 "addtmUDs (Parse.term_grammar()))"]), NL, 1211 add_string "end (* addUDs local *)", NL, 1212 1213 add_string "end", NL 1214 ] 1215 end)} 1216 end 1217end 1218 1219val _ = let 1220 val rawpp_thm = 1221 pp_thm 1222 |> Lib.with_flag (current_backend, PPBackEnd.raw_terminal) 1223 |> trace ("paranoid string literal printing", 1) 1224in 1225 Theory.pp_thm := rawpp_thm 1226end 1227 1228val _ = Theory.register_hook 1229 ("Parse.setup_grammars", 1230 (fn TheoryDelta.NewTheory{oldseg,newseg} => 1231 setup_grammars(oldseg, newseg) 1232 | _ => ())) 1233 1234 1235fun export_theorems_as_docfiles dirname thms = let 1236 val {arcs,isAbs,vol} = Path.fromString dirname 1237 fun check_arcs checked arcs = 1238 case arcs of 1239 [] => checked 1240 | x::xs => let 1241 val nextlevel = Path.concat (checked, x) 1242 in 1243 if FileSys.access(nextlevel, []) then 1244 if FileSys.isDir nextlevel then check_arcs nextlevel xs 1245 else raise Fail (nextlevel ^ " exists but is not a directory") 1246 else let 1247 in 1248 FileSys.mkDir nextlevel 1249 handle (OS.SysErr(s, erropt)) => let 1250 val part2 = case erropt of SOME err => OS.errorMsg err | NONE => "" 1251 in 1252 raise Fail ("Couldn't create directory "^nextlevel^": "^s^" - "^ 1253 part2) 1254 end; 1255 check_arcs nextlevel xs 1256 end 1257 end 1258 val dirname = check_arcs (Path.toString {arcs=[],isAbs=isAbs,vol=vol}) arcs 1259 fun write_thm (thname, thm) = let 1260 open Theory TextIO 1261 val outstream = openOut (Path.concat (dirname, thname^".doc")) 1262 in 1263 output(outstream, "\\THEOREM "^thname^" "^current_theory()^"\n"); 1264 output(outstream, thm_to_string thm); 1265 output(outstream, "\n\\ENDTHEOREM\n"); 1266 closeOut outstream 1267 end 1268in 1269 app write_thm thms 1270end handle IO.Io {function,name,...} => 1271 HOL_WARNING "Parse" "export_theorems_as_docfiles" 1272 ("Giving up on IO error: "^function^" : "^name) 1273 | Fail s => 1274 HOL_WARNING "Parse" "export_theorems_as_docfiles" 1275 ("Giving up after error: "^s) 1276 1277(*--------------------------------------------------------------------------- 1278 pp_element values that are brought across from term_grammar. 1279 Tremendous potential for confusion: TM and TOK are constructed 1280 values, but not constructors, here. Other things of this ilk 1281 are the constructors for the datatypes pp_element, 1282 PhraseBlockStyle, and ParenStyle. 1283 ---------------------------------------------------------------------------*) 1284 1285fun TM x = x; fun TOK x = x; (* remove constructor status *) 1286 1287val TM = term_grammar.RE term_grammar.TM 1288val TOK = term_grammar.RE o term_grammar.TOK 1289 1290(* ---------------------------------------------------------------------- 1291 hideous hack section 1292 ---------------------------------------------------------------------- *) 1293 1294 val _ = initialise_typrinter 1295 (fn G => ulower (type_pp.pp_type G PPBackEnd.raw_terminal)) 1296 val _ = let 1297 open TheoryDelta 1298 fun tempchk f nm = if Theory.is_temp_binding nm then () 1299 else ignore (f nm) 1300 fun hook ev = 1301 case ev of 1302 NewConstant{Thy,Name} => tempchk add_const Name 1303 | NewTypeOp{Thy,Name} => tempchk add_type Name 1304 | DelConstant{Thy,Name} => tempchk hide Name 1305 | _ => () 1306 in 1307 Theory.register_hook ("Parse.watch_constants", hook) 1308 end 1309 1310(* when new_theory is called, and if the new theory has the same name 1311 as the theory segment we were in anyway, then arrange that 1312 constants from this segment in the overload info section are removed. 1313 1314 This needs to be done because no such constant can exist any more *) 1315 1316 fun clear_thy_consts_from_oinfo thy oinfo = let 1317 val all_parse_consts = Overload.oinfo_ops oinfo 1318 fun bad_parse_guy (nm, {actual_ops, ...}) = let 1319 fun bad_guy t = let 1320 val {Name,Thy,...} = dest_thy_const t 1321 in 1322 if Thy = thy then SOME (nm, {Name = Name, Thy = Thy}) 1323 else NONE 1324 end 1325 in 1326 List.mapPartial bad_guy actual_ops 1327 end 1328 val parses_to_remove = List.concat (map bad_parse_guy all_parse_consts) 1329 val all_print_consts = Overload.print_map oinfo 1330 fun bad_print_guy (x as {Name,Thy}, nm) = 1331 if Thy = thy then SOME (nm, x) else NONE 1332 val prints_to_remove = List.mapPartial bad_print_guy all_print_consts 1333 fun foldthis ((nm, r), oi) = Overload.remove_mapping nm r oi 1334 in 1335 foldl foldthis (foldl foldthis oinfo parses_to_remove) prints_to_remove 1336 end 1337 1338 fun clear_thy_consts_from_grammar thy = let 1339 val new_grammar = 1340 term_grammar.fupdate_overload_info (clear_thy_consts_from_oinfo thy) 1341 (term_grammar()) 1342 in 1343 the_term_grammar := new_grammar; 1344 term_grammar_changed := true 1345 end 1346 1347 val _ = Theory.register_hook 1348 ("Parse.clear_consts_from_grammar", 1349 fn TheoryDelta.NewTheory{oldseg,newseg} => 1350 if oldseg = newseg then 1351 clear_thy_consts_from_grammar oldseg 1352 else () 1353 | _ => ()) 1354 1355end 1356