1structure term_grammar :> term_grammar = 2struct 3 4open HOLgrammars GrammarSpecials Lib Feedback term_grammar_dtype 5 6val ERROR = mk_HOL_ERR "term_grammar" 7 8type term = Term.term 9 10type nthy_rec = {Name : string, Thy : string} 11 12fun RE_compare (TOK s1, TOK s2) = String.compare(s1,s2) 13 | RE_compare (TOK _, _) = LESS 14 | RE_compare (TM, TOK _) = GREATER 15 | RE_compare (TM, TM) = EQUAL 16 | RE_compare (TM, ListTM _) = LESS 17 | RE_compare (ListTM ls1, ListTM ls2) = 18 let 19 val {nilstr=n1,cons=c1,sep=s1} = ls1 20 val {nilstr=n2,cons=c2,sep=s2} = ls2 21 fun pcs cmp = pair_compare (String.compare, cmp) 22 in 23 pcs (pcs String.compare) ((n1,(c1,s1)), (n2,(c2,s2))) 24 end 25 | RE_compare (ListTM _, _) = GREATER 26 27fun first_rtok rel = 28 case rel of 29 [] => raise Fail "PrecAnalysis.first_rtok: no token" 30 | (TOK s :: _) => s 31 | _ :: rest => first_rtok rest 32 33fun first_tok ppel = 34 case ppel of 35 [] => raise Fail "PrecAnalysis.first_tok: no token" 36 | p::rest => 37 (case p of 38 PPBlock(pels, _) => first_tok (pels @ rest) 39 | RE (TOK s) => s 40 | ListForm lsp => first_tok (#separator lsp) 41 | _ => first_tok rest) 42 43 44fun rule_elements0 pplist acc = 45 case pplist of 46 [] => acc 47 | ((RE x) :: xs) => acc |> cons x |> rule_elements0 xs 48 | (PPBlock(pels, _) :: xs) => 49 acc |> rule_elements0 pels |> rule_elements0 xs 50 | ListForm{separator, nilstr, cons=c, ...} :: xs => 51 acc |> cons (ListTM{nilstr=nilstr,cons=c,sep=first_tok separator}) 52 |> rule_elements0 xs 53 | ( _ :: xs) => rule_elements0 xs acc 54fun rule_elements ppels = List.rev (rule_elements0 ppels []) 55 56 57 fun rels_ok [TOK _] = true 58 | rels_ok (TOK _ :: TM :: xs) = rels_ok xs 59 | rels_ok (TOK _ :: ListTM _ :: xs) = rels_ok xs 60 | rels_ok (TOK _ :: xs) = rels_ok xs 61 | rels_ok _ = false 62 63 fun pp_elements_ok pplist = let 64 fun check_em toplevel eibs_ok els = 65 case els of 66 [] => true 67 | (x::xs) => let 68 in 69 case x of 70 LastTM => false 71 | FirstTM => false 72 | EndInitialBlock _ => 73 toplevel andalso eibs_ok andalso check_em true true xs 74 | BeginFinalBlock _ => toplevel andalso check_em true false xs 75 | PPBlock(els, _) => 76 check_em false false els andalso check_em toplevel eibs_ok xs 77 | _ => check_em toplevel eibs_ok xs 78 end 79 in 80 rels_ok (rule_elements pplist) andalso check_em true true pplist 81 end 82 83 84 85 86fun reltoString (TOK s) = s 87 | reltoString TM = "TM" 88 | reltoString (ListTM _) = "ListTM" 89 90fun pptoks ppels = List.mapPartial (fn TOK s => SOME s | _ => NONE) 91 (rule_elements ppels) 92 93(* used so that ProvideUnicode can look at additions to grammars and see if 94 they involve Unicode *) 95fun grule_toks ({pp_elements, ...}:grule) = pptoks pp_elements 96 97(* ProvideUnicode wants to track term names of additions *) 98fun grule_name ({term_name, ...}:grule) = term_name 99 100 101type overload_info = Overload.overload_info 102 103type ('a,'b) printer_info = 104 (term * string * ('a,'b) term_pp_types.userprinter) FCNet.t * 105 string Binaryset.set 106type special_info = {type_intro : string, 107 lambda : string list, 108 endbinding : string, 109 restr_binders : (string option * string) list, 110 res_quanop : string} 111fun fupd_lambda f {type_intro,lambda,endbinding,restr_binders,res_quanop} = 112 {type_intro = type_intro, lambda = f lambda, endbinding = endbinding, 113 restr_binders = restr_binders, res_quanop = res_quanop} 114 115 116type prmP0 = Absyn.absyn -> Parse_supportENV.preterm_in_env 117 118datatype grammar = GCONS of 119 {rules : (int option * grammar_rule) list, 120 specials : special_info, 121 numeral_info : (char * string option) list, 122 strlit_map : string Symtab.table, 123 overload_info : overload_info, 124 user_printers : (type_grammar.grammar * grammar, grammar) printer_info, 125 absyn_postprocessors : (string * postprocessor) list, 126 preterm_processors : (string*int,ptmprocessor) Binarymap.dict, 127 next_timestamp : int 128 } 129and postprocessor = AbPP of grammar -> Absyn.absyn -> Absyn.absyn 130and ptmprocessor = PtmP of grammar -> prmP0 -> prmP0 131 132fun destAbPP (AbPP f) = f 133fun destPtmP (PtmP f) = f 134 135type absyn_postprocessor = grammar -> Absyn.absyn -> Absyn.absyn 136type AbPTME = Absyn.absyn -> Parse_supportENV.preterm_in_env 137type preterm_processor = grammar -> AbPTME -> AbPTME 138 139 140datatype ruleset = GRS of (int option * grammar_rule) list * special_info 141fun ruleset (GCONS {rules,specials,...}) = GRS (rules, specials) 142 143type userprinter = 144 (type_grammar.grammar * grammar, grammar) term_pp_types.userprinter 145 146fun specials (GCONS G) = #specials G 147fun numeral_info (GCONS G) = #numeral_info G 148fun overload_info (GCONS G) = #overload_info G 149fun known_constants (GCONS G) = Overload.known_constants (#overload_info G) 150fun grammar_rules (GCONS G) = map #2 (#rules G) 151fun rules (GCONS G) = (#rules G) 152fun absyn_postprocessors0 (GCONS g) = #absyn_postprocessors g 153fun absyn_postprocessors g = map (apsnd destAbPP) (absyn_postprocessors0 g) 154fun gnext_timestamp (GCONS g) = #next_timestamp g 155 156fun preterm_processor (GCONS g) k = 157 Option.map destPtmP (Binarymap.peek(#preterm_processors g, k)) 158 159 160(* fupdates *) 161open FunctionalRecordUpdate 162fun gcons_mkUp z = makeUpdate9 z 163fun update_G z = let 164 fun from rules specials numeral_info overload_info user_printers 165 absyn_postprocessors preterm_processors next_timestamp 166 strlit_map = 167 {rules = rules, specials = specials, numeral_info = numeral_info, 168 overload_info = overload_info, user_printers = user_printers, 169 absyn_postprocessors = absyn_postprocessors, strlit_map = strlit_map, 170 preterm_processors = preterm_processors, next_timestamp = next_timestamp} 171 (* fields in reverse order to above *) 172 fun from' strlit_map next_timestamp preterm_processors absyn_postprocessors 173 user_printers 174 overload_info numeral_info specials rules = 175 {rules = rules, specials = specials, numeral_info = numeral_info, 176 overload_info = overload_info, user_printers = user_printers, 177 absyn_postprocessors = absyn_postprocessors, strlit_map = strlit_map, 178 preterm_processors = preterm_processors, next_timestamp = next_timestamp } 179 (* first order *) 180 fun to f {rules, specials, numeral_info, 181 overload_info, user_printers, absyn_postprocessors, 182 preterm_processors, next_timestamp, strlit_map} = 183 f rules specials numeral_info overload_info user_printers 184 absyn_postprocessors preterm_processors next_timestamp strlit_map 185in 186 gcons_mkUp (from, from', to) 187end z 188 189fun fupdate_rules f (GCONS g) = 190 GCONS (update_G g (U #rules (f (#rules g))) $$) 191fun fupdate_specials f (GCONS g) = 192 GCONS (update_G g (U #specials (f (#specials g))) $$) 193fun fupdate_numinfo f (GCONS g) = 194 GCONS (update_G g (U #numeral_info (f (#numeral_info g))) $$) 195fun fupdate_strlit_map f (GCONS g) = 196 GCONS (update_G g (U #strlit_map (f (#strlit_map g))) $$) 197 198fun mfupdate_overload_info f (GCONS g) = let 199 val (new_oinfo,result) = f (#overload_info g) 200in 201 (GCONS (update_G g (U #overload_info new_oinfo) $$), result) 202end 203fun fupdate_overload_info f g = 204 #1 (mfupdate_overload_info (fn oi => (f oi, ())) g) 205 206val strip_overload_info = fupdate_overload_info (fn _ => Overload.null_oinfo) 207 208fun mfupdate_user_printers f (GCONS g) = let 209 val (new_uprinters, result) = f (#user_printers g) 210in 211 (GCONS (update_G g (U #user_printers new_uprinters) $$), result) 212end 213 214fun inc_timestamp (GCONS g) = 215 GCONS (update_G g (U #next_timestamp (#next_timestamp g + 1)) $$) 216 217fun grammar_name G tm = let 218 val oinfo = overload_info G 219in 220 if Term.is_const tm then 221 Overload.overloading_of_term oinfo tm 222 else if Term.is_var tm then let 223 val (vnm, _) = Term.dest_var tm 224 in 225 Option.map #fake (GrammarSpecials.dest_fakeconst_name vnm) 226 end 227 else NONE 228end 229 230 231(* invariant of user_printers is that there is only ever one value with a 232 given name in the mapping from terms to print functions *) 233fun fupdate_user_printers f g = 234 #1 (mfupdate_user_printers (fn ups => (f ups, ())) g) 235 236fun user_printers (GCONS g) = #1 (#user_printers g) 237 238fun remove_user_printer k (GCONS g) = let 239 val (net, keyset) = #user_printers g 240in 241 if Binaryset.member(keyset,k) then let 242 fun foldthis (t,nm,f) (olddata,newnet) = 243 if nm = k then (SOME (t,f), newnet) 244 else (olddata, FCNet.insert(t,(t,nm,f)) newnet) 245 val (data, newnet) = FCNet.itnet foldthis net (NONE, FCNet.empty) 246 val newkeys = Binaryset.delete(keyset, k) 247 in 248 (GCONS (update_G g (U #user_printers (newnet,newkeys)) $$), 249 data) 250 end 251 else (GCONS g, NONE) 252end 253 254fun add_user_printer (k,pat,v) g = let 255 val (g', _) = remove_user_printer k g 256 fun upd (net,keys) = 257 (FCNet.insert(pat, (pat,k,v)) net, Binaryset.add(keys, k)) 258in 259 fupdate_user_printers upd g' 260end 261 262fun update_alist (k,v) [] = [(k,v)] 263 | update_alist (k,v) ((kv as (k',_))::rest) = 264 if k = k' then (k,v) :: rest 265 else kv :: update_alist (k,v) rest 266 267fun new_absyn_postprocessor (k,f) (GCONS g) = let 268 val old = #absyn_postprocessors g 269in 270 GCONS (update_G g (U #absyn_postprocessors (update_alist (k,AbPP f) old)) $$) 271end 272 273fun remove_absyn_postprocessor k (GCONS g) = let 274 val old = #absyn_postprocessors g 275in 276 case total (pluck (equal k o #1)) old of 277 NONE => (GCONS g, NONE) 278 | SOME ((_,AbPP f), rest) => 279 (GCONS (update_G g (U #absyn_postprocessors rest) $$), SOME f) 280end 281 282fun new_preterm_processor k f (GCONS g) = let 283 val old = #preterm_processors g 284in 285 GCONS (update_G g 286 (U #preterm_processors (Binarymap.insert(old,k,PtmP f))) $$) 287end 288 289fun remove_preterm_processor k (G as GCONS g) = let 290 val old = #preterm_processors g 291in 292 case Lib.total Binarymap.remove (old,k) of 293 SOME(new, v) => (GCONS (update_G g (U #preterm_processors new) $$), 294 SOME (destPtmP v)) 295 | NONE => (G, NONE) 296end 297 298 299fun update_restr_binders rb 300 {lambda, endbinding, type_intro, restr_binders, res_quanop} = 301 {lambda = lambda, endbinding = endbinding, type_intro = type_intro, 302 restr_binders = rb, res_quanop = res_quanop} 303 304fun fupdate_restr_binders f 305 {lambda, endbinding, type_intro, restr_binders, res_quanop} = 306 {lambda = lambda, endbinding = endbinding, type_intro = type_intro, 307 restr_binders = f restr_binders, res_quanop = res_quanop} 308 309fun map_rrfn_rule f g r = 310 case r of 311 PREFIX (STD_prefix rlist) => PREFIX (STD_prefix (map f rlist)) 312 | PREFIX (BINDER bslist) => PREFIX (BINDER (map g bslist)) 313 314 | INFIX (STD_infix (rlist, a)) => INFIX (STD_infix (map f rlist, a)) 315 | INFIX RESQUAN_OP => r 316 | INFIX (FNAPP rlist) => INFIX (FNAPP (map f rlist)) 317 | INFIX VSCONS => r 318 319 | SUFFIX (STD_suffix rlist) => SUFFIX (STD_suffix (map f rlist)) 320 | SUFFIX TYPE_annotation => r 321 322 | CLOSEFIX rlist => CLOSEFIX (map f rlist) 323 324fun fupdate_rule_by_term t f g r = let 325 fun over_rr (rr:rule_record) = if #term_name rr = t then f rr else rr 326 fun over_br LAMBDA = LAMBDA 327 | over_br (b as BinderString {term_name,...}) = 328 if term_name = t then g b else b 329in 330 map_rrfn_rule over_rr over_br r 331end 332 333fun fupdate_rule_by_termtok {term_name, tok} f g r = let 334 fun over_rr (rr:rule_record) = 335 if #term_name rr = term_name andalso 336 List.exists (fn e => e = TOK tok) (rule_elements (#elements rr)) then 337 f rr 338 else 339 rr 340 fun over_br LAMBDA = LAMBDA 341 | over_br (b as BinderString {term_name = tnm, tok = tk, ...}) = 342 if term_name = tnm andalso tk = tok then g b else b 343in 344 map_rrfn_rule over_rr over_br r 345end 346 347fun fupdate_rule_by_termtoklist {term_name,toklist} f g r = let 348 fun toks rr = pptoks (#elements rr) 349 fun over_rr (rr:rule_record) = 350 if #term_name rr = term_name andalso toks rr = toklist then 351 f rr 352 else 353 rr 354 fun over_br LAMBDA = LAMBDA 355 | over_br (b as BinderString {term_name = tnm, tok, ...}) = 356 if term_name = tnm andalso [tok] = toklist then g b else b 357in 358 map_rrfn_rule over_rr over_br r 359end 360 361fun fupdate_rulelist f rules = map (fn (p,r) => (p, f r)) rules 362fun fupdate_prulelist f rules = map f rules 363 364fun update_b_tstamp _ LAMBDA = LAMBDA 365 | update_b_tstamp t (BinderString {tok,term_name,timestamp}) = 366 BinderString {tok = tok, term_name =term_name, timestamp = t} 367 368fun update_rr_tstamp t {term_name, elements, paren_style, 369 block_style, timestamp} = 370 {term_name = term_name, elements = elements, paren_style = paren_style, 371 block_style = block_style, timestamp = t} 372 373 374fun binder_to_string (G:grammar) b = 375 case b of 376 LAMBDA => hd (#lambda (specials G)) 377 | BinderString {term_name,...} => term_name 378 379(* the concrete tokens of the grammar corresponding to bind syntax. *) 380fun binders (G: grammar) = let 381 fun b2str (LAMBDA, acc) = #lambda (specials G) @ acc 382 | b2str (BinderString r, acc) = (#tok r)::acc 383 fun binders0 [] acc = acc 384 | binders0 ((_, x)::xs) acc = let 385 in 386 case x of 387 PREFIX (BINDER sl) => binders0 xs (List.foldl b2str acc sl) 388 | _ => binders0 xs acc 389 end 390in 391 binders0 (rules G) [] 392end 393 394fun resquan_op (G: grammar) = #res_quanop (specials G) 395 396fun update_assoc (item as (k,v)) alist = 397 case alist of 398 [] => [item] 399 | (first as (k1,v1))::rest => if k = k1 then item::rest 400 else first::update_assoc item rest 401 402fun associate_restriction G {binder = b, resbinder = s} = 403 fupdate_specials (fupdate_restr_binders (update_assoc (b, s))) G 404 405fun is_binder G = let val bs = binders G in fn s => Lib.mem s bs end 406 407 408(* gives the "wrong" lexicographic order, but is more likely to 409 resolve differences with one comparison because types/terms with 410 the same name are rare, but it's quite reasonable for many 411 types/terms to share the same theory *) 412fun nthy_compare ({Name = n1, Thy = thy1}, {Name = n2, Thy = thy2}) = 413 case String.compare(n1, n2) of 414 EQUAL => String.compare(thy1, thy2) 415 | x => x 416 417 418val stdhol : grammar = 419 GCONS 420 {rules = [(SOME 0, PREFIX (BINDER [LAMBDA])), 421 (SOME 4, INFIX RESQUAN_OP), 422 (SOME 5, INFIX VSCONS), 423 (SOME 460, 424 INFIX (STD_infix([{term_name = fnapp_special, 425 elements = [RE (TOK "$")], 426 timestamp = 0, 427 (* pp info irrelevant as will never print *) 428 block_style = 429 (AroundEachPhrase, (PP.CONSISTENT, 0)), 430 paren_style = OnlyIfNecessary}, 431 432 {term_name = recwith_special, 433 elements = [RE (TOK "with")], 434 timestamp = 0, 435 block_style = (AroundEachPhrase, 436 (PP.CONSISTENT, 0)), 437 paren_style = OnlyIfNecessary}, 438 {term_name = recupd_special, 439 elements = [RE (TOK ":=")], 440 timestamp = 0, 441 block_style = (AroundEachPhrase, 442 (PP.CONSISTENT, 0)), 443 paren_style = OnlyIfNecessary}, 444 {term_name = recfupd_special, 445 elements = [RE (TOK "updated_by")], 446 timestamp = 0, 447 block_style = (AroundEachPhrase, 448 (PP.CONSISTENT, 0)), 449 paren_style = OnlyIfNecessary}], RIGHT))), 450 (SOME 899, SUFFIX TYPE_annotation), 451 (SOME 2000, INFIX (FNAPP [])), 452 (SOME 2500, 453 INFIX (STD_infix ([{term_name = recsel_special, 454 elements = [RE (TOK ".")], 455 timestamp = 0, 456 block_style = (AroundEachPhrase, 457 (PP.CONSISTENT, 0)), 458 paren_style = OnlyIfNecessary}], LEFT))), 459 (NONE, 460 CLOSEFIX [{term_name = bracket_special, 461 elements = [RE (TOK "("), RE TM, RE (TOK ")")], 462 timestamp = 0, 463 (* these two elements here will not actually 464 ever be looked at by the printer *) 465 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 466 paren_style = Always}]), 467 (NONE, 468 CLOSEFIX [{term_name = recd_lform_name, 469 elements = [RE (TOK "<|"), 470 ListForm { 471 separator = [RE (TOK ";"), 472 BreakSpace(1,0)], 473 block_info = (PP.INCONSISTENT, 0), 474 cons = reccons_special, 475 nilstr = recnil_special 476 }, 477 RE (TOK "|>")], 478 timestamp = 0, 479 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 480 paren_style = OnlyIfNecessary}])], 481 specials = {lambda = ["\\"], type_intro = ":", endbinding = ".", 482 restr_binders = [], res_quanop = "::"}, 483 numeral_info = [], 484 strlit_map = Symtab.empty, 485 overload_info = Overload.null_oinfo, 486 user_printers = (FCNet.empty, Binaryset.empty String.compare), 487 absyn_postprocessors = [], 488 preterm_processors = 489 Binarymap.mkDict (pair_compare(String.compare, Int.compare)), 490 next_timestamp = 1 491 } 492 493fun first_tok [] = raise Fail "Shouldn't happen: term_grammar.first_tok" 494 | first_tok (RE (TOK s)::_) = s 495 | first_tok (_ :: t) = first_tok t 496 497local 498 open stmonad 499 infix >> 500 fun add x acc = (x::acc, ()) 501 fun specials_from_elm [] = ok 502 | specials_from_elm ((TOK x)::xs) = add x >> specials_from_elm xs 503 | specials_from_elm (TM::xs) = specials_from_elm xs 504 | specials_from_elm (ListTM {sep,...}::xs) = add sep >> specials_from_elm xs 505 val mmap = (fn f => fn args => mmap f args >> ok) 506 fun rule_specials G r = let 507 val rule_specials = rule_specials G 508 in 509 case r of 510 PREFIX(STD_prefix rules) => 511 mmap (specials_from_elm o rule_elements o #elements) rules 512 | PREFIX (BINDER b) => ok 513 | SUFFIX(STD_suffix rules) => 514 mmap (specials_from_elm o rule_elements o #elements) rules 515 | SUFFIX TYPE_annotation => add (#type_intro (specials G)) 516 | INFIX(STD_infix (rules, _)) => 517 mmap (specials_from_elm o rule_elements o #elements) rules 518 | INFIX RESQUAN_OP => ok 519 | INFIX (FNAPP rlst) => 520 mmap (specials_from_elm o rule_elements o #elements) rlst 521 | INFIX VSCONS => ok 522 | CLOSEFIX rules => 523 mmap (specials_from_elm o rule_elements o #elements) rules 524 end 525in 526 fun grammar_tokens G = let 527 fun gs (G:grammar) = mmap (rule_specials G o #2) (rules G) >> 528 mmap add (binders G) 529 val (all_specials, ()) = gs G [] 530 in 531 Lib.mk_set all_specials 532 end 533 fun rule_tokens G r = Lib.mk_set (#1 (rule_specials G r [])) 534end 535 536fun aug_compare (NONE, NONE) = EQUAL 537 | aug_compare (_, NONE) = LESS 538 | aug_compare (NONE, _) = GREATER 539 | aug_compare (SOME n, SOME m) = Int.compare(n,m) 540 541fun priv_a2string a = 542 case a of 543 LEFT => "LEFT" 544 | RIGHT => "RIGHT" 545 | NONASSOC => "NONASSOC" 546 547fun rr_eq (rr1: rule_record) (rr2 : rule_record) = 548 (* ignore timestamp field *) 549 #term_name rr1 = #term_name rr2 andalso 550 #elements rr1 = #elements rr2 andalso 551 #block_style rr1 = #block_style rr2 andalso 552 #paren_style rr1 = #paren_style rr2 553val rrunion = Lib.op_union rr_eq 554 555fun tokb_eq b1 b2 = 556 case (b1,b2) of 557 (LAMBDA, LAMBDA) => true 558 | (BinderString{tok=tk1, term_name = nm1,...}, 559 BinderString{tok=tk2, term_name = nm2,...}) => tk1 = tk2 andalso 560 nm1 = nm2 561 | _ => false 562val bunion = Lib.op_union tokb_eq 563 564fun merge_rules (r1, r2) = 565 case (r1, r2) of 566 (SUFFIX (STD_suffix sl1), SUFFIX (STD_suffix sl2)) => 567 SUFFIX (STD_suffix (rrunion sl1 sl2)) 568 | (SUFFIX TYPE_annotation, SUFFIX TYPE_annotation) => r1 569 | (PREFIX (STD_prefix pl1), PREFIX (STD_prefix pl2)) => 570 PREFIX (STD_prefix (rrunion pl1 pl2)) 571 | (PREFIX (BINDER b1), PREFIX (BINDER b2)) => 572 PREFIX (BINDER (bunion b1 b2)) 573 | (INFIX VSCONS, INFIX VSCONS) => INFIX VSCONS 574 | (INFIX(STD_infix (i1, a1)), INFIX(STD_infix(i2, a2))) => 575 if a1 <> a2 then 576 raise GrammarError 577 ("Attempt to have differently associated infixes ("^ 578 priv_a2string a1^" and "^priv_a2string a2^") at same level") 579 else 580 INFIX(STD_infix(rrunion i1 i2, a1)) 581 | (INFIX RESQUAN_OP, INFIX RESQUAN_OP) => INFIX(RESQUAN_OP) 582 | (INFIX (FNAPP rl1), INFIX (FNAPP rl2)) => INFIX (FNAPP (rrunion rl1 rl2)) 583 | (INFIX (STD_infix(i1, a1)), INFIX (FNAPP rl1)) => 584 if a1 <> LEFT then 585 raise GrammarError 586 ("Attempting to merge function application with non-left" ^ 587 " associated infix") 588 else INFIX (FNAPP (rrunion i1 rl1)) 589 | (INFIX (FNAPP _), INFIX (STD_infix _)) => merge_rules (r2, r1) 590 | (CLOSEFIX c1, CLOSEFIX c2) => CLOSEFIX (rrunion c1 c2) 591 | _ => raise GrammarError "Attempt to have different forms at same level" 592 593fun optmerge r NONE = SOME r 594 | optmerge r1 (SOME r2) = SOME (merge_rules (r1, r2)) 595 596(* the listrule and closefix rules don't have precedences and sit at the 597 end of the list. When merging grammars, we will have a list of possibly 598 intermingled closefix and listrule rules to look at, we want to produce 599 just one closefix and one listrule rule for the final grammar *) 600 601(* This allows for reducing more than just two closefix and listrules, but 602 when merging grammars with only one each, this shouldn't eventuate *) 603fun resolve_nullprecs closefix rules = 604 case rules of 605 [] => let 606 in 607 case closefix of 608 NONE => [] (* should never really happen *) 609 | SOME cf => [(NONE, cf)] 610 end 611 | (_, r as CLOSEFIX _)::xs => 612 resolve_nullprecs (optmerge r closefix) xs 613 | _ => raise Fail "resolve_nullprecs: can't happen" 614 615 616fun resolve_same_precs rules = 617 case rules of 618 [] => [] 619 | [x] => [x] 620 | ((p1 as SOME _, r1)::(rules1 as (p2, r2)::rules2)) => let 621 in 622 if p1 <> p2 then 623 (p1, r1)::(resolve_same_precs rules1) 624 else let 625 val merged_rule = merge_rules (r1, r2) 626 handle GrammarError s => 627 raise GrammarError (s ^ "(" ^Int.toString (valOf p1)^")") 628 in 629 (p1, merged_rule) :: resolve_same_precs rules2 630 end 631 end 632 | ((NONE, _)::_) => resolve_nullprecs NONE rules 633 634 635infix Gmerge 636(* only merges rules, keeps rest as in g1 *) 637fun ((g1:grammar) Gmerge (g2:(int option * grammar_rule) list)) = let 638 val g0_rules = 639 Listsort.sort (fn (e1,e2) => aug_compare(#1 e1, #1 e2)) 640 (rules g1 @ g2) 641 val g_rules = resolve_same_precs g0_rules 642in 643 fupdate_rules (fn _ => g_rules) g1 644end 645 646fun null_rule r = 647 case r of 648 SUFFIX (STD_suffix slist) => null slist 649 | PREFIX (STD_prefix slist) => null slist 650 | PREFIX (BINDER slist) => null slist 651 | INFIX (STD_infix(slist, _)) => null slist 652 | CLOSEFIX slist => null slist 653 | _ => false 654 655fun map_rules f G = let 656 fun recurse r = 657 case r of 658 [] => [] 659 | ((prec, rule)::rules) => let 660 val newrule = f rule 661 val rest = recurse rules 662 in 663 if null_rule newrule then rest else (prec, newrule)::rest 664 end 665in 666 fupdate_rules recurse G 667end 668 669 670fun remove_form s rule = let 671 fun rr_ok (r:rule_record) = #term_name r <> s 672 fun lr_ok (ls:listspec) = #cons ls <> s andalso #nilstr ls <> s 673 fun stringbinder LAMBDA = true 674 | stringbinder (BinderString r) = #term_name r <> s 675in 676 case rule of 677 SUFFIX (STD_suffix slist) => SUFFIX (STD_suffix (List.filter rr_ok slist)) 678 | INFIX (STD_infix(slist, assoc)) => 679 INFIX(STD_infix (List.filter rr_ok slist, assoc)) 680 | PREFIX (STD_prefix slist) => PREFIX (STD_prefix (List.filter rr_ok slist)) 681 | PREFIX (BINDER slist) => PREFIX (BINDER (List.filter stringbinder slist)) 682 | CLOSEFIX slist => CLOSEFIX (List.filter rr_ok slist) 683 | _ => rule 684end 685 686 687fun remove_tok P tok r = let 688 fun rel_matches rel = 689 case rel of 690 TOK t => t = tok 691 | ListTM{cons,nilstr,sep,...} => cons = tok orelse nilstr = tok orelse 692 sep = tok 693 | _ => false 694 fun rels_safe rels = not (List.exists rel_matches rels) 695 fun rr_safe ({term_name = s, elements,...}:rule_record) = 696 not (P s) orelse rels_safe (rule_elements elements) 697 fun binder_safe b = 698 case b of 699 BinderString {term_name = tnm, tok = tk, ...} => 700 tk <> tok orelse not (P tnm) 701 | LAMBDA => true 702in 703 case r of 704 SUFFIX (STD_suffix slist) => 705 SUFFIX (STD_suffix (List.filter rr_safe slist)) 706 | INFIX(STD_infix (slist, assoc)) => 707 INFIX (STD_infix (List.filter rr_safe slist, assoc)) 708 | PREFIX (STD_prefix slist) => 709 PREFIX (STD_prefix (List.filter rr_safe slist)) 710 | PREFIX (BINDER blist) => 711 PREFIX (BINDER (List.filter binder_safe blist)) 712 | CLOSEFIX slist => CLOSEFIX (List.filter rr_safe slist) 713 | _ => r 714end 715 716fun remove_toklist {term_name, toklist} r = let 717 fun relstoks rels = List.mapPartial (fn TOK s => SOME s | _ => NONE) rels 718 fun rr_safe ({term_name = s, elements, ...} : rule_record) = 719 s <> term_name orelse relstoks (rule_elements elements) <> toklist 720 fun binder_safe b = 721 case b of 722 BinderString { term_name = s, tok, ...} => [tok] <> toklist orelse 723 s <> term_name 724 | LAMBDA => true 725in 726 case r of 727 SUFFIX (STD_suffix slist) => SUFFIX (STD_suffix (List.filter rr_safe slist)) 728 | INFIX (STD_infix (slist, assoc)) => 729 INFIX (STD_infix (List.filter rr_safe slist, assoc)) 730 | PREFIX (STD_prefix slist) => PREFIX (STD_prefix (List.filter rr_safe slist)) 731 | PREFIX (BINDER blist) => PREFIX (BINDER (List.filter binder_safe blist)) 732 | CLOSEFIX slist => CLOSEFIX (List.filter rr_safe slist) 733 | _ => r 734end 735 736fun remove_standard_form G s = map_rules (remove_form s) G 737fun remove_form_with_tok G {tok,term_name} = 738 map_rules (remove_tok (fn s => s = term_name) tok) G 739fun remove_form_with_toklist r = map_rules (remove_toklist r) 740fun remove_rules_with_tok s = 741 map_rules (remove_tok (fn _ => true) s) 742 743 744fun fixityToString f = 745 case f of 746 Infix(a,i) => "Infix("^assocToString a^", "^Int.toString i^")" 747 | Closefix => "Closefix" 748 | Suffix p => "Suffix "^Int.toString p 749 | Prefix p => "Prefix "^Int.toString p 750 | Binder => "Binder" 751 752 753fun rrec2delta rf (rr : rule_record) = let 754 val {term_name,paren_style,block_style,elements,...} = rr 755in 756 (#timestamp rr, 757 GRULE {term_name = term_name, paren_style = paren_style, 758 block_style = block_style, pp_elements = elements, 759 fixity = rf}) 760end 761 762fun binder_grule {term_name,tok} = 763 {term_name = term_name, paren_style = OnlyIfNecessary, 764 block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)), 765 pp_elements = [RE (TOK tok)], fixity = Binder} 766 767fun extract_lspec rels = 768 case rels of 769 [] => NONE 770 | ListTM l :: _ => SOME l 771 | _ :: rest => extract_lspec rest 772 773fun rules_for G nm = let 774 fun search_rrlist rf acc rrl = let 775 fun check rrec a = 776 if #term_name rrec = nm then rrec2delta rf rrec :: a 777 else if term_name_is_lform (#term_name rrec) then 778 case extract_lspec (rule_elements (#elements rrec)) of 779 NONE => a 780 | SOME {cons,nilstr,...} => if nm = cons orelse nilstr = nm then 781 rrec2delta rf rrec :: a 782 else a 783 else a 784 fun recurse acc rrl = 785 case rrl of 786 [] => acc 787 | rr :: rest => recurse (check rr acc) rest 788 in 789 recurse acc rrl 790 end 791 fun search_blist acc blist = 792 case blist of 793 [] => acc 794 | LAMBDA :: rest => search_blist acc rest 795 | BinderString {tok,term_name,timestamp} :: rest => 796 if term_name = nm then 797 search_blist 798 ((timestamp, GRULE (binder_grule {term_name=term_name,tok=tok})) :: 799 acc) 800 rest 801 else 802 search_blist acc rest 803 fun search acc rs = 804 case rs of 805 [] => List.rev acc 806 | (fixopt, grule) :: rest => let 807 in 808 case grule of 809 PREFIX (BINDER blist) => search (search_blist acc blist) rest 810 | PREFIX (STD_prefix rrlist) => 811 search (search_rrlist (Prefix (valOf fixopt)) acc rrlist) 812 rest 813 | SUFFIX (STD_suffix rrlist) => 814 search (search_rrlist (Suffix (valOf fixopt)) acc rrlist) 815 rest 816 | INFIX (STD_infix (rrlist, assoc)) => 817 search (search_rrlist (Infix(assoc, valOf fixopt)) acc rrlist) 818 rest 819 | CLOSEFIX rrl => search (search_rrlist Closefix acc rrl) rest 820 | _ => search acc rest 821 end 822in 823 search [] (rules G) 824end 825 826fun add_rule {term_name = s : string, fixity = f, pp_elements, 827 paren_style, block_style} G0 = let 828 val _ = pp_elements_ok pp_elements orelse 829 raise GrammarError "token list no good" 830 val new_tstamp = gnext_timestamp G0 831 val rr = {term_name = s, elements = pp_elements, timestamp = new_tstamp, 832 paren_style = paren_style, block_style = block_style} 833 val new_rule = 834 case f of 835 Infix (a,p) => (SOME p, INFIX(STD_infix([rr], a))) 836 | Suffix p => (SOME p, SUFFIX (STD_suffix [rr])) 837 | Prefix p => (SOME p, PREFIX (STD_prefix [rr])) 838 | Closefix => (NONE, CLOSEFIX [rr]) 839 | Binder => 840 case pp_elements of 841 [RE (TOK b)] => (SOME std_binder_precedence, 842 PREFIX(BINDER[BinderString{tok=b,term_name=s, 843 timestamp=new_tstamp}])) 844 | _ => raise ERROR "add_rule" "Rules for binders must have one TOK only" 845 846in 847 inc_timestamp (G0 Gmerge [new_rule]) 848end 849 850fun add_grule G0 r = G0 Gmerge [r] 851 852fun add_binder {term_name,tok} G0 = let 853 val binfo = {term_name = term_name, tok = tok, 854 timestamp = gnext_timestamp G0 } 855in 856 inc_timestamp (G0 Gmerge [(SOME 0, PREFIX (BINDER [BinderString binfo]))]) 857end 858 859fun listform_to_rule (lform : listspec) = 860 let 861 val {separator, leftdelim, rightdelim, cons, nilstr, ...} = lform 862 val binfo = #block_info lform 863 fun ok_el e = 864 case e of 865 EndInitialBlock _ => false 866 | BeginFinalBlock _ => false 867 | RE TM => false 868 | LastTM => false 869 | FirstTM => false 870 | _ => true 871 fun check_els els = 872 case List.find (not o ok_el) els of 873 NONE => () 874 | SOME s => raise GrammarError "Invalid pp_element in listform" 875 fun is_tok (RE (TOK _)) = true 876 | is_tok _ = false 877 fun one_tok pps = 878 if length (List.filter is_tok pps) = 1 then () 879 else raise GrammarError "Must have exactly one TOK in listform elements" 880 val _ = app check_els [separator, leftdelim, rightdelim] 881 val _ = app one_tok [separator, leftdelim, rightdelim] 882 val els = 883 [PPBlock (leftdelim @ [ListForm { separator = separator, 884 block_info = binfo, 885 cons = cons, nilstr = nilstr}] @ 886 rightdelim, 887 binfo)] 888 in 889 {term_name = GrammarSpecials.mk_lform_name {cons=cons,nilstr=nilstr}, 890 pp_elements = els, fixity = Closefix, 891 block_style = (AroundEachPhrase, binfo), 892 paren_style = OnlyIfNecessary} 893 end 894 895fun add_listform G lrule = add_rule (listform_to_rule lrule) G 896 897fun rename_to_fixity_field 898 {rule_fixity,term_name,pp_elements,paren_style, block_style} = 899 {fixity=rule_fixity, term_name = term_name, pp_elements = pp_elements, 900 paren_style = paren_style, block_style = block_style} 901 902fun standard_mapped_spacing {term_name,tok,fixity} = let 903 val bstyle = (AroundSamePrec, (PP.INCONSISTENT, 0)) 904 val pstyle = OnlyIfNecessary 905 val ppels = 906 case fixity of 907 Infix _ => [HardSpace 1, RE (TOK tok), BreakSpace(1,0)] 908 | Prefix _ => [RE(TOK tok), HardSpace 1] 909 | Suffix _ => [HardSpace 1, RE(TOK tok)] 910 | Closefix => [RE(TOK tok)] 911 | Binder => [RE(TOK tok)] 912in 913 {term_name = term_name, fixity = fixity, pp_elements = ppels, 914 paren_style = pstyle, block_style = bstyle} 915end 916 917fun standard_spacing name fixity = 918 standard_mapped_spacing {term_name = name, tok = name, fixity = fixity} 919 920val std_binder_precedence = 0; 921 922fun set_mapped_fixity {term_name,tok,fixity} G = 923 let 924 val nmtok = {term_name=term_name, tok = tok} 925 val G = remove_form_with_tok G nmtok 926 in 927 case fixity of 928 Binder => if term_name <> tok then 929 raise ERROR "set_mapped_fixity" 930 "Can't map binders to different strings" 931 else 932 add_binder nmtok G 933 | rf => {fixity = rf, tok = tok, term_name = term_name} 934 |> standard_mapped_spacing 935 |> C add_rule G 936 end 937 938 939fun prefer_form_with_tok (r as {term_name,tok}) G0 = let 940 val newstamp = gnext_timestamp G0 941in 942 G0 |> fupdate_rules 943 (fupdate_rulelist 944 (fupdate_rule_by_termtok r 945 (update_rr_tstamp newstamp) 946 (update_b_tstamp newstamp))) 947 |> inc_timestamp 948end 949 950fun prefer_form_with_toklist (r as {term_name,toklist}) G = let 951 val t' = gnext_timestamp G 952in 953 G |> fupdate_rules (fupdate_rulelist 954 (fupdate_rule_by_termtoklist r 955 (update_rr_tstamp t') 956 (update_b_tstamp t'))) 957 |> inc_timestamp 958end 959 960 961fun set_associativity_at_level G (p, ass) = 962 fupdate_rules 963 (fupdate_prulelist 964 (fn (p', r) => 965 if isSome p' andalso p = valOf p' then 966 (p', (case r of 967 INFIX(STD_infix(els, _)) => INFIX (STD_infix(els, ass)) 968 | _ => r)) 969 else 970 (p', r))) G 971 972fun find_partial f [] = NONE 973 | find_partial f (x::xs) = let 974 in 975 case f x of 976 NONE => find_partial f xs 977 | y => y 978 end 979 980fun get_precedence (G:grammar) s = let 981 val rules = rules G 982 fun check_rule (p, r) = let 983 fun elmem s [] = false 984 | elmem s (({elements, ...}:rule_record)::xs) = 985 Lib.mem (TOK s) (rule_elements elements) orelse elmem s xs 986 in 987 case r of 988 INFIX(STD_infix (elms, assoc)) => 989 if elmem s elms then SOME(Infix(assoc, valOf p)) 990 else NONE 991 | PREFIX(STD_prefix elms) => 992 if elmem s elms then SOME (Prefix (valOf p)) 993 else NONE 994 | PREFIX (BINDER bs) => 995 find_partial 996 (fn BinderString r => if #tok r = s then SOME Binder else NONE 997 | LAMBDA => NONE) 998 bs 999 | SUFFIX (STD_suffix elms) => if elmem s elms then SOME (Suffix (valOf p)) 1000 else NONE 1001 | CLOSEFIX elms => if elmem s elms then SOME Closefix else NONE 1002 | _ => NONE 1003 end 1004in 1005 if Lib.mem s (#lambda (specials G)) then SOME Binder 1006 else 1007 find_partial check_rule rules 1008end 1009 1010fun update_assoc (k,v) alist = let 1011 val (_, newlist) = Lib.pluck (fn (k', _) => k' = k) alist 1012 in 1013 (k,v)::newlist 1014 end handle _ => (k,v)::alist 1015 1016 1017fun check c = 1018 if Char.isAlpha c then Char.toLower c 1019 else raise GrammarError "Numeric type suffixes must be letters" 1020 1021fun add_numeral_form G (c, stropt) = 1022 fupdate_numinfo (update_assoc (check c, stropt)) G 1023fun strlit_map (GCONS g) {tmnm} = Symtab.lookup (#strlit_map g) tmnm 1024fun add_strlit_injector {tmnm,ldelim} = 1025 fupdate_strlit_map (Symtab.update(tmnm,ldelim)) 1026fun remove_strlit_injector {tmnm} = 1027 fupdate_strlit_map (Symtab.delete_safe tmnm) 1028 1029structure userSyntaxFns = struct 1030 type 'a getter = string -> 'a 1031 type 'a setter = {name : string, code : 'a} -> unit 1032 type 'a t = 'a getter * 'a setter 1033 fun mk_table () = 1034 let 1035 val tab = ref (Binarymap.mkDict String.compare) 1036 in 1037 ((fn s => Binarymap.find(!tab, s)), 1038 (fn {name,code} => tab := Binarymap.insert(!tab, name, code))) 1039 end 1040 val (get_userPP, register_userPP) = mk_table() : userprinter t 1041 val (get_absynPostProcessor, register_absynPostProcessor) = 1042 mk_table() : absyn_postprocessor t 1043end 1044 1045fun add_delta ud G = 1046 case ud of 1047 GRULE r => add_rule r G 1048 | RMTMTOK r => remove_form_with_tok G r 1049 | RMTMNM s => remove_standard_form G s 1050 | RMTOK s => remove_rules_with_tok s G 1051 | OVERLOAD_ON p => fupdate_overload_info (Overload.add_overloading p) G 1052 | IOVERLOAD_ON p => 1053 fupdate_overload_info (Overload.add_inferior_overloading p) G 1054 | ASSOC_RESTR r => associate_restriction G r 1055 | RMOVMAP (s,kid) => 1056 fupdate_overload_info (Overload.remove_mapping s kid) G 1057 | GRMOVMAP (s,tm) => 1058 fupdate_overload_info (Overload.gen_remove_mapping s tm) G 1059 | MOVE_OVLPOSN {frontp,skid=(s,{Name,Thy})} => 1060 let 1061 val oact = if frontp then Overload.bring_to_front_overloading 1062 else Overload.send_to_back_overloading 1063 in 1064 fupdate_overload_info (oact {opname=s,realname=Name,realthy=Thy}) G 1065 end 1066 | ADD_NUMFORM cs => add_numeral_form G cs 1067 | CLR_OVL s => 1068 fupdate_overload_info (#1 o Overload.remove_overloaded_form s) G 1069 | ADD_UPRINTER {codename = s, pattern} => 1070 if s = "" then 1071 add_user_printer("", pattern, term_pp_types.dummyprinter) G 1072 else 1073 let 1074 val code = userSyntaxFns.get_userPP s 1075 handle Binarymap.NotFound => 1076 raise ERROR "add_delta" 1077 ("No code named "^s^ 1078 " registered for add user-printer") 1079 in 1080 add_user_printer (s,pattern,code) G 1081 end 1082 | ADD_ABSYN_POSTP {codename} => 1083 let 1084 val code = userSyntaxFns.get_absynPostProcessor codename 1085 handle Binarymap.NotFound => 1086 raise ERROR "add_delta" 1087 ("No code named "^codename^ 1088 " registered for add absyn-postprocessor") 1089 in 1090 new_absyn_postprocessor (codename, code) G 1091 end 1092 | ADD_STRLIT r => add_strlit_injector r G 1093 | RM_STRLIT r => remove_strlit_injector r G 1094 1095fun add_deltas uds G = List.foldl (uncurry add_delta) G uds 1096 1097fun give_num_priority G c = let 1098 val realc = check c 1099 fun update_fn alist = let 1100 val (oldval, rest) = Lib.pluck (fn (k,_) => k = realc) alist 1101 in 1102 oldval::rest 1103 end handle _ => raise GrammarError "No such numeral type in grammar" 1104in 1105 fupdate_numinfo update_fn G 1106end 1107 1108fun remove_numeral_form G c = 1109 fupdate_numinfo (List.filter (fn (k,v) => k <> (check c))) G 1110 1111fun merge_specials S1 S2 = let 1112 val {type_intro = typ1, lambda = lam1, endbinding = end1, 1113 restr_binders = res1, res_quanop = resq1} = S1 1114 val {type_intro = typ2, lambda = lam2, endbinding = end2, 1115 restr_binders = res2, res_quanop = resq2} = S2 1116in 1117 if typ1 = typ2 andalso lam1 = lam2 andalso end1 = end2 andalso resq1 = resq2 1118 then 1119 {type_intro = typ1, lambda = lam1, endbinding = end1, 1120 restr_binders = Lib.union res1 res2, res_quanop = resq1} 1121 else 1122 raise GrammarError "Specials in two grammars don't agree" 1123end 1124 1125fun merge_bmaps typestring keyprinter m1 m2 = let 1126 (* m1 takes precedence - arbitrarily *) 1127 fun foldfn (k,v,newmap) = 1128 (if isSome (Binarymap.peek(newmap, k)) then 1129 Feedback.HOL_WARNING "term_grammar" "merge_grammars" 1130 ("Merging "^typestring^" has produced a clash on key "^keyprinter k) 1131 else 1132 (); 1133 Binarymap.insert(newmap,k,v)) 1134in 1135 Binarymap.foldl foldfn m2 m1 1136end 1137 1138fun merge_user_printers (n1,ks1) (n2,_) = let 1139 fun foldthis (tm,k,f) (n,ks) = 1140 if Binaryset.member(ks,k) then (n,ks) 1141 else (FCNet.insert(tm,(tm,k,f)) n, Binaryset.add(ks, k)) 1142in 1143 FCNet.itnet foldthis n2 (n1,ks1) 1144end 1145 1146fun alist_merge al1 al2 = let 1147 (* could try to be smart here and preserve orderings in some circumstances *) 1148 fun foldthis ((k,v), acc) = 1149 case Lib.assoc1 k acc of 1150 NONE => (k,v) :: acc 1151 | SOME _ => acc 1152in 1153 List.rev (List.foldl foldthis (List.rev al1) al2) 1154end 1155 1156fun bmap_merge m1 m2 = 1157 Binarymap.foldl (fn (k,v,acc) => Binarymap.insert(acc,k,v)) m1 m2 1158 1159fun merge_grammars (G1 as GCONS g1, G2 as GCONS g2) :grammar = let 1160 val g0_rules = 1161 Listsort.sort (fn (e1,e2) => aug_compare(#1 e1, #1 e2)) 1162 (rules G1 @ rules G2) 1163 val newrules = resolve_same_precs g0_rules 1164 val newspecials = merge_specials (specials G1) (specials G2) 1165 val new_numinfo = Lib.union (numeral_info G1) (numeral_info G2) 1166 val new_oload_info = 1167 Overload.merge_oinfos (overload_info G1) (overload_info G2) 1168 val new_ups = let 1169 val GCONS g1 = G1 and GCONS g2 = G2 1170 in 1171 merge_user_printers (#user_printers g1) (#user_printers g2) 1172 end 1173in 1174 GCONS {rules = newrules, specials = newspecials, numeral_info = new_numinfo, 1175 overload_info = new_oload_info, user_printers = new_ups, 1176 absyn_postprocessors = alist_merge (absyn_postprocessors0 G1) 1177 (absyn_postprocessors0 G2), 1178 preterm_processors = 1179 bmap_merge (#preterm_processors g1) (#preterm_processors g2), 1180 next_timestamp = Int.max(#next_timestamp g1, #next_timestamp g2), 1181 strlit_map = Symtab.join (fn _ => fn (_,v2) => v2) 1182 (#strlit_map g1, #strlit_map g2) 1183 } 1184end 1185 1186(* ---------------------------------------------------------------------- 1187 * Prettyprinting grammars 1188 * ---------------------------------------------------------------------- *) 1189 1190datatype ruletype_info = add_prefix | add_suffix | add_both | add_nothing 1191 1192fun prettyprint_grammar_rules tmprint (GRS(rules,specials)) = let 1193 open Portable HOLPP smpp 1194 1195 fun pprint_rr m (rr:rule_record) = let 1196 val rels = rule_elements (#elements rr) 1197 val (pfx, sfx) = 1198 case m of 1199 add_prefix => ("", " TM") 1200 | add_suffix => ("TM ", "") 1201 | add_both => ("TM ", " TM") 1202 | add_nothing => ("", "") 1203 fun special_case s = 1204 if s = bracket_special then "just parentheses, no term produced" 1205 else if s = recsel_special then "record field selection" 1206 else if s = recupd_special then "record field update" 1207 else if s = recfupd_special then "functional record update" 1208 else if s = recwith_special then "record update" 1209 else 1210 case dest_fakeconst_name s of 1211 NONE => s 1212 | SOME {fake,original = NONE} => "%" ^ fake ^ "%" 1213 | SOME {fake,original = SOME{Thy,Name}} => 1214 Thy ^ "$" ^ Name ^ " - %" ^ fake ^ "%" 1215 1216 val tmid_suffix0 = "["^ special_case (#term_name rr)^"]" 1217 val tmid_suffix = 1218 case rels of 1219 [TOK s] => if s <> #term_name rr then tmid_suffix0 else "" 1220 | _ => tmid_suffix0 1221 in 1222 block PP.INCONSISTENT 0 ( 1223 add_string pfx >> 1224 pr_list (fn (TOK s) => add_string ("\""^s^"\"") 1225 | TM => add_string "TM" 1226 | ListTM {nilstr,cons,sep} => 1227 add_string ("LTM<" ^ 1228 String.concatWith "," [nilstr,cons,sep] ^ 1229 ">")) 1230 (add_string " ") rels >> 1231 add_string sfx >> add_break(2,4) >> 1232 add_string tmid_suffix 1233 ) 1234 end 1235 1236 1237 fun pprint_rrl (m:ruletype_info) (rrl : rule_record list) = 1238 block PP.INCONSISTENT 0 ( 1239 pr_list (pprint_rr m) (add_break(1,0) >> add_string "| ") rrl 1240 ) 1241 1242 fun print_binder b = let 1243 open Lib 1244 val bnames = 1245 case b of 1246 LAMBDA => map (fn s => (s,"")) (#lambda specials) 1247 | BinderString {term_name,tok,...} => [(tok, 1248 if tok = term_name then "" 1249 else " ["^term_name^"]")] 1250 val endb = quote (#endbinding specials) 1251 fun one_binder (s, tnminfo) = 1252 add_string (quote s ^ " <..binders..> " ^ endb ^ " TM" ^ tnminfo) 1253 in 1254 pr_list one_binder (add_break (1,0) >> add_string "| ") bnames 1255 end 1256 1257 1258 fun print_binderl bl = 1259 block PP.INCONSISTENT 0 ( 1260 pr_list print_binder (add_break (1,0) >> add_string "| ") bl 1261 ) 1262 1263 1264 fun pprint_grule (r: grammar_rule) = 1265 case r of 1266 PREFIX (STD_prefix rrl) => pprint_rrl add_prefix rrl 1267 | PREFIX (BINDER blist) => print_binderl blist 1268 | SUFFIX (STD_suffix rrl) => pprint_rrl add_suffix rrl 1269 | SUFFIX TYPE_annotation => let 1270 val type_intro = #type_intro specials 1271 in 1272 add_string ("TM \""^type_intro^"\" TY (type annotation)") 1273 end 1274 | INFIX (STD_infix (rrl, a)) => let 1275 val assocstring = 1276 case a of 1277 LEFT => "L-" 1278 | RIGHT => "R-" 1279 | NONASSOC => "non-" 1280 in 1281 block CONSISTENT 0 ( 1282 pprint_rrl add_both rrl >> 1283 add_break (3,4) >> 1284 add_string ("("^assocstring^"associative)") 1285 ) 1286 end 1287 | INFIX RESQUAN_OP => let 1288 val rsqstr = #res_quanop specials 1289 in 1290 add_string ("TM \""^rsqstr^ 1291 "\" TM (restricted quantification operator)") 1292 end 1293 | CLOSEFIX rrl => pprint_rrl add_nothing rrl 1294 | INFIX (FNAPP rrl) => let 1295 in 1296 block CONSISTENT 0 ( 1297 add_string "TM TM (function application)" >> 1298 (case rrl of [] => nothing 1299 | _ => (add_string " |" >> add_break(1,0) >> 1300 pprint_rrl add_both rrl)) >> 1301 add_break(3,0) >> 1302 add_string ("(L-associative)") 1303 ) 1304 end 1305 | INFIX VSCONS => add_string "TM TM (binder argument concatenation)" 1306 1307 fun print_whole_rule (intopt, rule) = let 1308 val precstr0 = 1309 case intopt of 1310 NONE => "" 1311 | SOME n => "("^Int.toString n^")" 1312 val precstr = StringCvt.padRight #" " 7 precstr0 1313 in 1314 block CONSISTENT 0 ( 1315 add_string precstr >> 1316 add_string "TM ::= " >> 1317 block CONSISTENT 13 (pprint_grule rule) 1318 ) 1319 end 1320 1321in 1322 pr_list print_whole_rule (add_break (1,0)) rules 1323end 1324 1325fun prettyprint_grammar tmprint (G :grammar) = let 1326 open Portable HOLPP smpp 1327 fun uninteresting_overload (k,r:Overload.overloaded_op_info) = 1328 length (#actual_ops r) = 1 andalso 1329 #Name (Term.dest_thy_const (hd (#actual_ops r))) = k 1330 handle HOL_ERR _ => false andalso 1331 length (Term.decls k) = 1 1332 fun print_overloading oinfo0 = 1333 if List.all uninteresting_overload oinfo0 then nothing 1334 else let 1335 open Lib infix ## 1336 fun nblanks n = CharVector.tabulate(n, fn _ => #" ") 1337 val oinfo1 = List.filter (not o uninteresting_overload) oinfo0 1338 val oinfo = Listsort.sort (String.compare o (#1 ## #1)) oinfo1 1339 val max = 1340 List.foldl (fn (oi,n) => Int.max(UTF8.size (#1 oi), n)) 1341 0 1342 oinfo 1343 fun pr_ov (overloaded_op0, 1344 (r as {actual_ops,...}:Overload.overloaded_op_info)) = 1345 let 1346 val overloaded_op = 1347 if overloaded_op0 = "" then " <won't print> " 1348 else overloaded_op0 1349 fun pr_name t = 1350 trace ("types", 1) (tmprint (strip_overload_info G)) t 1351 in 1352 block INCONSISTENT (max + 5) ( 1353 add_string (overloaded_op^ 1354 nblanks (max - UTF8.size overloaded_op)^ 1355 " -> ") >> 1356 pr_list pr_name (add_break (1,0)) actual_ops 1357 ) 1358 end 1359 in 1360 add_newline >> 1361 add_string "Overloading:" >> 1362 add_break(1,2) >> 1363 block CONSISTENT 0 (pr_list pr_ov add_newline oinfo) 1364 end 1365 fun print_user_printers printers = let 1366 fun pr (pat,nm,f) = 1367 (tmprint G pat >> add_string (" -> "^nm)) 1368 in 1369 if FCNet.size printers = 0 then nothing 1370 else 1371 add_newline >> 1372 add_string "User printing functions:" >> 1373 add_newline >> 1374 add_string " " >> 1375 block INCONSISTENT 2 ( 1376 pr_list pr add_newline (FCNet.itnet cons printers []) 1377 ) 1378 end 1379in 1380 block CONSISTENT 0 ( 1381 (* rules *) 1382 prettyprint_grammar_rules tmprint (ruleset G) >> add_newline >> 1383 (* known constants *) 1384 add_string "Known constants:" >> 1385 add_break(1,2) >> 1386 block INCONSISTENT 0 ( 1387 pr_list add_string (add_break(1,0)) 1388 (Listsort.sort String.compare (known_constants G)) 1389 ) >> 1390 (* overloading *) 1391 print_overloading (Overload.oinfo_ops (overload_info G)) >> 1392 print_user_printers (user_printers G) 1393 ) 1394end 1395 1396fun add_const (s,t) = 1397 fupdate_overload_info (Overload.add_overloading(s,t)) 1398val min_grammar = let 1399 open Term Portable PP 1400in 1401 stdhol |> add_const ("==>", prim_mk_const{Name = "==>", Thy = "min"}) 1402 |> add_const ("=", prim_mk_const{Name = "=", Thy = "min"}) 1403 |> add_const ("@", prim_mk_const{Name = "@", Thy = "min"}) 1404 |> add_binder {term_name="@", tok = "@"} 1405 1406 (* Using the standard rules for infixes for ==> and = seems 1407 to result in bad pretty-printing of goals. I think the 1408 following customised printing spec works better. The crucial 1409 difference is that the blocking style is CONSISTENT rather than 1410 INCONSISTENT. *) 1411 |> add_rule {term_name = "==>", 1412 block_style = (AroundSamePrec, (CONSISTENT, 0)), 1413 fixity = Infix(RIGHT, 200), 1414 pp_elements = [HardSpace 1, RE (TOK "==>"), 1415 BreakSpace(1,0)], 1416 paren_style = OnlyIfNecessary} 1417 |> add_rule {term_name = "=", 1418 block_style = (AroundSamePrec, (CONSISTENT, 0)), 1419 fixity = Infix(NONASSOC, 450), 1420 pp_elements = [HardSpace 1, RE (TOK "="), 1421 BreakSpace(1,0)], 1422 paren_style = OnlyIfNecessary} 1423 |> fupdate_specials (fupd_lambda (cons UnicodeChars.lambda)) 1424end 1425 1426 1427 1428fun debugprint G tm = 1429 let 1430 open HolKernel 1431 val pr = debugprint G 1432 val map = List.map 1433 in 1434 case dest_term tm of 1435 VAR (s,_) => s 1436 | CONST {Name,Thy,...} => 1437 Thy ^ "$" ^ Name ^ "<" ^ 1438 (case grammar_name G tm of NONE => "" | SOME s => s) ^ ">" 1439 | COMB _ => 1440 let 1441 val (f, args) = strip_comb tm 1442 in 1443 "(" ^ pr f ^ " " ^ String.concatWith " " (map pr args) ^ ")" 1444 end 1445 | LAMB _ => 1446 let 1447 val (vs, bod) = strip_abs tm 1448 in 1449 "(\\" ^ String.concatWith " " (map pr vs) ^ ". " ^ pr bod ^ ")" 1450 end 1451 end 1452 1453(** quick-and-dirty removal of all "non-trivial" overloadings **) 1454 1455(* add overloading of constant and its name *) 1456fun grm_self_ovl (tm : term, tmG : grammar) = 1457 let val (str, ty) = Term.dest_const tm ; 1458 in fupdate_overload_info (Overload.add_overloading (str, tm)) tmG end ; 1459 1460(* add in overloading of all constants with their names *) 1461fun self_ovl_all_consts (tmG : grammar) = 1462 List.foldr grm_self_ovl tmG (Term.all_consts ()) ; 1463 1464(* clear all overloading info in a term grammar *) 1465fun clear_all_overloads (tmG : grammar) = 1466 fupdate_overload_info (fn _ => Overload.null_oinfo) tmG ; 1467 1468fun clear_overloads (tmG : grammar) = 1469 self_ovl_all_consts (clear_all_overloads tmG) ; 1470 1471end; (* struct *) 1472