1structure Symbolic :> Symbolic =
2struct
3
4val symb_map = [("Type",         "-->", "arrow"),
5                ("Lib",          "|->", "maplet"),
6                ("Lib",          "##",  "hash2"),
7                ("bossLib",      "&&",  "amper2"),
8                ("BasicProvers", "&&",  "amper2"),
9                ("simpLib",      "++",  "plus2"),
10                ("Parse",        "--",  "minus2"),
11                ("Parse",        "==",  "equal2")];
12
13fun unsymb "Type.-->"        = "Type.arrow"
14  | unsymb "Lib.|->"         = "Lib.maplet"
15  | unsymb "Lib.\\#\\#"      = "Lib.hash2"
16  | unsymb "Lib.|>"          = "Lib.pipegt"
17  | unsymb "Lib.##"          = "Lib.hash2"
18  | unsymb "bossLib.&&"      = "bossLib.amper2"
19  | unsymb "BasicProvers.&&" = "BasicProvers.amper2"
20  | unsymb "simpLib.++"      = "simpLib.plus2"
21  | unsymb "bossLib.++"      = "bossLib.plus2"
22  | unsymb "Parse.--"        = "Parse.minus2"
23  | unsymb "Parse.=="        = "Parse.equal2"
24  | unsymb other             = other;
25
26fun tosymb "Type.arrow"          = "Type.-->"
27  | tosymb "Lib.maplet"          = "Lib.|->"
28  | tosymb "Lib.pipegt"          = "Lib.|>"
29  | tosymb "Lib.hash2"           = "Lib.##"
30  | tosymb "bossLib.amper2"      = "bossLib.&&"
31  | tosymb "BasicProvers.amper2" = "BasicProvers.&&"
32  | tosymb "simpLib.plus2"       = "simpLib.++"
33  | tosymb "Parse.minus2"        = "Parse.--"
34  | tosymb "Parse.equal2"        = "Parse.=="
35  | tosymb other                 = other;
36
37end
38