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