1structure GrammarSpecials :> GrammarSpecials =
2struct
3
4  val fnapp_special = "_ fnapp"
5  val bracket_special = "_ bracket"
6  val let_special = " _ let"
7  val letcons_special = " _ letcons"
8  val letnil_special = " _ letnil"
9  val and_special = " _ and"
10  val fakeconst_special = " _ fakeconst"
11
12  fun mk_lform_name {nilstr,cons} = "ListForm<" ^ nilstr ^ "," ^ cons ^">"
13  val term_name_is_lform = String.isPrefix "ListForm<"
14
15  fun mk_fakeconst_name {original,fake} = let
16    open Coding
17  in
18    fakeconst_special ^
19    PairData.encode (StringData.encode,
20                     OptionData.encode KernelNameData.encode)
21                    (fake, original)
22  end
23
24  fun dest_fakeconst_name s = let
25    open Coding
26    val decoder =
27        PairData.decode (StringData.reader,
28                         OptionData.reader KernelNameData.reader)
29  in
30    case decoder (Lib.unprefix fakeconst_special s) of
31        SOME (fake, original) => SOME{fake = fake, original = original}
32      | _ => NONE
33  end handle Feedback.HOL_ERR _ => NONE
34
35  val decimal_fraction_special = "/decfrac/"
36
37  val recsel_special = " _ record select"
38  val recupd_special = " _ record update"
39  val recfupd_special = " _ record fupdate"
40  val recwith_special = " _ record with"
41  val reccons_special = " _ record cons"
42  val recnil_special = " _ record nil"
43  val bigrec_subdivider_string = "brss__"
44  val recd_lform_name =
45      mk_lform_name{cons = reccons_special, nilstr = recnil_special}
46
47
48  val vs_cons_special = " _ vs cons"
49  val resquan_special = " _ res quan special"
50
51  val nat_elim_term = "nat_elim__magic"
52  val fromNum_str = "_ inject_number"
53  val num_injection = "&"
54
55
56  val std_binder_precedence = 0
57
58
59  fun mk_case_special0 nm component =
60      mk_fakeconst_name {original = SOME {Thy = "case magic", Name = nm},
61                         fake = component}
62  val mk_default_case = mk_case_special0 "default"
63  fun mk_case_special nm = mk_case_special0 nm "case"
64  fun dest_case_special s =
65    case dest_fakeconst_name s of
66        SOME {original = SOME{Thy="case magic",Name},fake="case"} => SOME Name
67      | _ => NONE
68  val is_case_special = isSome o dest_case_special
69
70
71
72  val core_case_special = mk_default_case "case"
73  val case_split_special = mk_default_case "split"
74  val case_arrow_special = mk_default_case "arrow"
75
76  open HolKernel
77  val compilefn = ref (NONE : (term -> term) option)
78  val constructorsfn =
79      ref (NONE : ({Thy:string,Tyop:string} -> term list) option)
80
81  fun compile_pattern_match t =
82      case !compilefn of
83        NONE => raise HOL_ERR {origin_function = "compile_pattern_match",
84                               origin_structure = "GrammarSpecials",
85                               message = "Function not initialised"}
86      | SOME f => f t
87  fun type_constructors s =
88      case !constructorsfn of
89        NONE => raise HOL_ERR {origin_function = "type_constructors",
90                               origin_structure = "GrammarSpecials",
91                               message = "Function not initialised"}
92      | SOME f => f s
93
94  fun set_case_specials (cmp,cnst) = (compilefn := SOME cmp;
95                                      constructorsfn := SOME cnst)
96
97  fun case_initialised () = isSome (!compilefn)
98
99
100end
101