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