1structure GrammarDeltas :> GrammarDeltas = 2struct 3 4open HolKernel type_grammar_dtype term_grammar_dtype term_grammar 5open HOLgrammars LoadableThyData 6 7val ERROR = mk_HOL_ERR "GrammarDeltas" 8type tmg_delta = term_grammar.user_delta 9type tyg_delta = type_grammar.delta 10datatype gdelta = TYD of tyg_delta | TMD of tmg_delta 11fun fopt >> g = Option.map g o fopt 12 13open ThyDataSexp 14fun assoc_decode t = 15 case t of 16 String "LEFT" => SOME LEFT 17 | String "RIGHT" => SOME RIGHT 18 | String "NONASSOC" => SOME NONASSOC 19 | _ => NONE 20fun assoc_encode LEFT = String "LEFT" 21 | assoc_encode RIGHT = String "RIGHT" 22 | assoc_encode NONASSOC = String "NONASSOC" 23 24val tydelta_decode = 25 let 26 open ThyDataSexp 27 infix || 28 fun new_infix (nm,pnm,assoc,prec) = 29 NEW_INFIX {Name = nm, ParseName = pnm, Assoc = assoc, Prec = prec} 30 fun tyabbrev (kid, ty, p) = TYABBREV (kid, ty, p) 31 in 32 (tag_decode "new-type" kname_decode >> NEW_TYPE) || 33 (tag_decode "new-tyinfix" 34 (pair4_decode (string_decode,string_decode,assoc_decode, 35 int_decode)) >> new_infix) || 36 (tag_decode "type-abbrev" 37 (pair3_decode (kname_decode, type_decode, bool_decode)) >> 38 tyabbrev) || 39 (tag_decode "disable-typrint" string_decode >> DISABLE_TYPRINT) || 40 (tag_decode "remove-knm-tyabbrev" kname_decode >> RM_KNM_TYABBREV)|| 41 (tag_decode "remove-tyabbrev" string_decode >> RM_TYABBREV) 42 end 43 44fun tydelta_encode tyd = 45 let 46 open ThyDataSexp 47 in 48 case tyd of 49 NEW_TYPE kid => tag_encode "new-type" KName kid 50 | NEW_INFIX{Name,ParseName,Assoc,Prec} => 51 tag_encode "new-tyinfix" 52 (pair4_encode (String,String,assoc_encode,Int)) 53 (Name,ParseName,Assoc,Prec) 54 | TYABBREV (kid, ty, prp) => 55 tag_encode "type-abbrev" (pair3_encode(KName,Type,Bool)) (kid,ty,prp) 56 | DISABLE_TYPRINT s => 57 tag_encode "disable-typrint" String s 58 | RM_KNM_TYABBREV kid => tag_encode "remove-knm-tyabbrev" KName kid 59 | RM_TYABBREV s => tag_encode "remove-tyabbrev" String s 60 end 61 62fun check_tydelta (d: type_grammar.delta) = 63 case d of 64 NEW_TYPE knm => Type.uptodate_kname knm 65 | TYABBREV (_, ty, _) => Type.uptodate_type ty 66 | _ => true 67 68(* ---------------------------------------------------------------------- 69 encoding and decoding grammars to and from s-expresions 70 ---------------------------------------------------------------------- *) 71open ThyDataSexp term_grammar_dtype 72infix || 73fun brks_encode PP.CONSISTENT = String "C" 74 | brks_encode PP.INCONSISTENT = String "I" 75fun brks_decode (String "C") = SOME PP.CONSISTENT 76 | brks_decode (String "I") = SOME PP.INCONSISTENT 77 | brks_decode _ = NONE 78 79val binfo_encode = pair_encode (brks_encode, Int) 80val binfo_decode = pair_decode (brks_decode, int_decode) 81 82fun style_encode AroundEachPhrase = String "each-phrase" 83 | style_encode AroundSamePrec = String "same-prec" 84 | style_encode AroundSameName = String "same-name" 85 | style_encode NoPhrasing = String "no-phrasing" 86fun style_decode (String "each-phrase") = SOME AroundEachPhrase 87 | style_decode (String "same-prec") = SOME AroundSamePrec 88 | style_decode (String "same-name") = SOME AroundSameName 89 | style_decode (String "no-phrasing") = SOME NoPhrasing 90 | style_decode _ = NONE 91 92val block_style_encode = pair_encode (style_encode, binfo_encode) 93val block_style_decode = pair_decode (style_decode, binfo_decode) 94 95fun rule_element_encode rel = 96 case rel of 97 TOK s => tag_encode "TOK" String s 98 | TM => Sym "TM" 99 | ListTM{nilstr,cons,sep} => 100 tag_encode "ListTM" (pair3_encode(String,String,String)) 101 (nilstr,cons,sep) 102val rule_element_decode = 103 (tag_decode "TOK" string_decode >> TOK) || 104 (require_tag "TM" >> (fn _ => TM)) || 105 (tag_decode "ListTM" 106 (pair3_decode(string_decode,string_decode,string_decode)) >> 107 (fn (n,c,s) => ListTM {nilstr=n,cons=c,sep=s})) 108 109fun paren_style_encode Always = String "A" 110 | paren_style_encode OnlyIfNecessary = String "O" 111 | paren_style_encode ParoundPrec = String "C" 112 | paren_style_encode ParoundName = String "N" 113 | paren_style_encode NotEvenIfRand = String "R" 114fun paren_style_decode t = 115 case t of 116 String "A" => SOME Always 117 | String "O" => SOME OnlyIfNecessary 118 | String "C" => SOME ParoundPrec 119 | String "N" => SOME ParoundName 120 | String "R" => SOME NotEvenIfRand 121 | _ => NONE 122 123fun ppel_encode ppel = 124 case ppel of 125 PPBlock (ppels, binfo) => 126 tag_encode "P" (pair_encode (mk_list ppel_encode, binfo_encode)) 127 (ppels, binfo) 128 | EndInitialBlock binfo => tag_encode "E" binfo_encode binfo 129 | BeginFinalBlock binfo => tag_encode "B" binfo_encode binfo 130 | HardSpace i => tag_encode "H" Int i 131 | BreakSpace (x,y) => tag_encode "S" (pair_encode(Int,Int)) (x,y) 132 | RE rel => tag_encode "R" rule_element_encode rel 133 | ListForm lspec => tag_encode "ListForm" lspec_encode lspec 134 | LastTM => Sym "L" 135 | FirstTM => Sym "F" 136and lspec_encode {separator, block_info, cons, nilstr} = 137 pair4_encode (mk_list ppel_encode, String, String, binfo_encode) 138 (separator, cons, nilstr, block_info) 139 140 141fun ppel_decode s = 142 ((tag_decode "P" (pair_decode (list_decode ppel_decode, binfo_decode)) >> 143 PPBlock) || 144 (tag_decode "E" binfo_decode >> EndInitialBlock) || 145 (tag_decode "B" binfo_decode >> BeginFinalBlock) || 146 (tag_decode "H" int_decode >> HardSpace) || 147 (tag_decode "S" (pair_decode(int_decode,int_decode)) >> BreakSpace) || 148 (tag_decode "R" rule_element_decode >> RE) || 149 (tag_decode "ListForm" lspec_decode >> ListForm) || 150 (require_tag "L" >> (fn _ => LastTM)) || 151 (require_tag "F" >> (fn _ => FirstTM))) s 152and lspec_decode s = let 153 fun f (separator,cons,nilstr,binfo) = 154 {separator = separator, nilstr = nilstr, block_info = binfo, cons = cons} 155in 156 (pair4_decode 157 (list_decode ppel_decode,string_decode,string_decode,binfo_decode) >> f) s 158end 159 160fun rrule_encode {term_name,elements,timestamp,block_style,paren_style} = 161 pair_encode(String, 162 pair4_encode(mk_list ppel_encode, Int, 163 block_style_encode, paren_style_encode)) 164 (term_name, (elements, timestamp, block_style, paren_style)) 165val rrule_decode = let 166 fun f (term_name, (elements, timestamp, block_style, paren_style)) = 167 {term_name = term_name, timestamp = timestamp, 168 block_style = block_style, paren_style = paren_style, 169 elements = elements} 170in 171 pair_decode(string_decode, 172 pair4_decode(list_decode ppel_decode, int_decode, 173 block_style_decode, paren_style_decode)) >> f 174end; 175 176fun binder_encode b = 177 case b of 178 LAMBDA => Sym "L" 179 | BinderString{tok,term_name,timestamp} => 180 tag_encode "B" (pair3_encode (String,String,Int)) 181 (tok,term_name,timestamp) 182val binder_decode = let 183 fun f (tok,term_name,timestamp) = 184 BinderString {tok = tok, term_name = term_name, 185 timestamp = timestamp} 186in 187 (require_tag "L" >> (fn _ => LAMBDA)) || 188 (tag_decode "B" (pair3_decode(string_decode, string_decode, int_decode)) >> f) 189end 190 191fun pfxrule_encode prule = 192 case prule of 193 STD_prefix rrl => tag_encode "S" (mk_list rrule_encode) rrl 194 | BINDER bl => tag_encode "B" (mk_list binder_encode) bl 195val pfxrule_decode = 196 (tag_decode "S" (list_decode rrule_decode) >> STD_prefix) || 197 (tag_decode "B" (list_decode binder_decode) >> BINDER) 198 199fun sfxrule_encode srule = 200 case srule of 201 STD_suffix rrl => tag_encode "S" (mk_list rrule_encode) rrl 202 | TYPE_annotation => Sym "T" 203val sfxrule_reader = 204 (tag_decode "S" (list_decode rrule_decode) >> STD_suffix) || 205 (require_tag "T" >> (fn _ => TYPE_annotation)) 206 207fun ifxrule_encode irule = 208 case irule of 209 STD_infix (rrl,a) => 210 tag_encode "S" (pair_encode (mk_list rrule_encode, assoc_encode)) 211 (rrl, a) 212 | RESQUAN_OP => Sym "R" 213 | VSCONS => Sym "V" 214 | FNAPP rrl => tag_encode "F" (mk_list rrule_encode) rrl 215val ifxrule_reader = 216 (tag_decode "S" (pair_decode(list_decode rrule_decode, assoc_decode)) >> 217 STD_infix) || 218 (require_tag "R" >> K RESQUAN_OP) || 219 (require_tag "V" >> K VSCONS) || 220 (tag_decode "F" (list_decode rrule_decode) >> FNAPP); 221 222fun fixity_encode f = 223 case f of 224 Infix(a,p) => tag_encode "I" (pair_encode(assoc_encode,Int)) (a,p) 225 | Suffix p => tag_encode "S" Int p 226 | Prefix p => tag_encode "P" Int p 227 | Closefix => Sym "C" 228 | Binder => Sym "B" 229val fixity_decode = 230 (tag_decode "I" (pair_decode(assoc_decode, int_decode)) >> Infix) || 231 (tag_decode "S" int_decode >> Suffix) || 232 (tag_decode "P" int_decode >> Prefix) || 233 (require_tag "C" >> K Closefix) || 234 (require_tag "B" >> K Binder) 235 236fun grule_encode (gr : grule) = 237 let 238 val {term_name, pp_elements, paren_style, block_style, fixity} = gr 239 in 240 pair_encode (String, 241 pair4_encode(paren_style_encode, 242 block_style_encode, 243 fixity_encode, 244 mk_list ppel_encode)) 245 (term_name, (paren_style, block_style, fixity, pp_elements)) 246 end 247val grule_decode : grule dec = let 248 fun grule (tn,(ps,bs,f,ppels)) = 249 {term_name = tn, paren_style = ps, block_style = bs, 250 fixity = f, pp_elements = ppels} 251in 252 pair_decode(string_decode, 253 pair4_decode(paren_style_decode, block_style_decode, 254 fixity_decode, list_decode ppel_decode)) >> grule 255end 256 257val skid_encode = pair_encode (String, KName) 258val skid_decode = pair_decode (string_decode, kname_decode) 259 260fun user_delta_encode ud = 261 case ud of 262 ADD_ABSYN_POSTP {codename} => tag_encode "AAPP" String codename 263 | ADD_NUMFORM (c,s) => 264 tag_encode "AN" (pair_encode(Char,option_encode String)) (c,s) 265 | ADD_STRLIT {tmnm,ldelim} => 266 tag_encode "AS" (pair_encode(String,String)) (tmnm,ldelim) 267 | ADD_UPRINTER{codename=s,pattern=tm} => 268 tag_encode "AUP" (pair_encode(String,Term)) (s,tm) 269 | ASSOC_RESTR {binder,resbinder} => 270 tag_encode "AR" (pair_encode (option_encode String, String)) 271 (binder,resbinder) 272 | CLR_OVL s => tag_encode "COV" String s 273 | GRMOVMAP(s,tm) => 274 tag_encode "RMG" (pair_encode(String,Term)) (s,tm) 275 | GRULE gr => tag_encode "G" grule_encode gr 276 | IOVERLOAD_ON (s,t) => tag_encode "OI" (pair_encode(String,Term)) (s,t) 277 | MOVE_OVLPOSN {frontp,skid} => 278 tag_encode "MOP" (pair_encode(Bool,skid_encode)) (frontp,skid) 279 | OVERLOAD_ON (s,t) => tag_encode "OO" (pair_encode(String,Term)) (s,t) 280 | RMOVMAP skid => tag_encode "RMO" skid_encode skid 281 | RMTMNM s => tag_encode "RN" String s 282 | RMTMTOK {term_name,tok} => 283 tag_encode "RK" (pair_encode(String,String)) (term_name,tok) 284 | RMTOK s => tag_encode "RMT" String s 285 | RM_STRLIT {tmnm} => tag_encode "RMS" String tmnm; 286 287 288val user_delta_decode = 289 (tag_decode "AAPP" string_decode >> (fn s => ADD_ABSYN_POSTP{codename = s}))|| 290 (tag_decode "AN" (pair_decode(char_decode, option_decode string_decode)) >> 291 ADD_NUMFORM) || 292 (tag_decode "AS" (pair_decode(string_decode,string_decode)) >> 293 (fn (tmnm,ldelim) => ADD_STRLIT{tmnm=tmnm,ldelim=ldelim})) || 294 (tag_decode "AUP" (pair_decode(string_decode,term_decode)) >> 295 (fn (s,p) => ADD_UPRINTER {codename = s, pattern = p})) || 296 (tag_decode "AR" (pair_decode(option_decode string_decode, string_decode)) >> 297 (fn (b,rb) => ASSOC_RESTR {binder = b, resbinder = rb})) || 298 (tag_decode "COV" string_decode >> CLR_OVL) || 299 (tag_decode "RMG" (pair_decode (string_decode,term_decode)) >> GRMOVMAP) || 300 (tag_decode "G" grule_decode >> GRULE) || 301 (tag_decode "OI" (pair_decode(string_decode,term_decode)) >> IOVERLOAD_ON) || 302 (tag_decode "MOP" (pair_decode(bool_decode, skid_decode)) >> 303 (fn (frontp,skid) => MOVE_OVLPOSN {frontp=frontp,skid=skid})) || 304 (tag_decode "OO" (pair_decode(string_decode,term_decode)) >> OVERLOAD_ON) || 305 (tag_decode "RMO" skid_decode >> RMOVMAP) || 306 (tag_decode "RN" string_decode >> RMTMNM) || 307 (tag_decode "RK" (pair_decode(string_decode,string_decode)) >> 308 (fn (nm,tok) => RMTMTOK {term_name = nm, tok = tok})) || 309 (tag_decode "RMT" string_decode >> RMTOK) || 310 (tag_decode "RMS" string_decode >> (fn s => RM_STRLIT{tmnm=s})); 311 312fun grammar_rule_encode grule = 313 case grule of 314 PREFIX pr => tag_encode "P" pfxrule_encode pr 315 | SUFFIX sr => tag_encode "S" sfxrule_encode sr 316 | INFIX ir => tag_encode "I" ifxrule_encode ir 317 | CLOSEFIX rrl => tag_encode "C" (mk_list rrule_encode) rrl 318 319val grammar_rule_decode = 320 (tag_decode "P" pfxrule_decode >> PREFIX) || 321 (tag_decode "S" sfxrule_reader >> SUFFIX) || 322 (tag_decode "I" ifxrule_reader >> INFIX) || 323 (tag_decode "C" (list_decode rrule_decode) >> CLOSEFIX); 324 325fun gdelta_encode (TMD udelta) = user_delta_encode udelta 326 | gdelta_encode (TYD tydelta) = tydelta_encode tydelta 327val gdelta_decode = (user_delta_decode >> TMD) || (tydelta_decode >> TYD); 328 329fun check_delta (d: user_delta) = 330 case d of 331 MOVE_OVLPOSN {skid = (_, kid), ...} => can prim_mk_const kid 332 | RMOVMAP (_, kid) => can prim_mk_const kid 333 | OVERLOAD_ON(_, t) => Term.uptodate_term t 334 | IOVERLOAD_ON(_, t) => Term.uptodate_term t 335 | GRMOVMAP(_, t) => Term.uptodate_term t 336 | ADD_UPRINTER{pattern,...} => Term.uptodate_term pattern 337 | _ => true 338 339fun nopp s _ = HOLPP.add_string ("<" ^ s ^ ">") 340 341fun check_gdelta (TMD tmd) = check_delta tmd 342 | check_gdelta (TYD tyd) = check_tydelta tyd 343 344fun other_tds (t, thyevent) = 345 case list_decode gdelta_decode t of 346 NONE => raise Fail ("GrammarDelta: encoding failure: t = \n " ^ 347 HOLPP.pp_to_string 70 348 (pp_sexp (nopp"ty") (nopp"tm") (nopp"thm")) 349 t) 350 | SOME gds => 351 let 352 val (goodgds, badgds) = Lib.partition check_gdelta gds 353 in 354 if null badgds then NONE 355 else 356 SOME (mk_list gdelta_encode goodgds) 357 end 358 359val {export, segment_data, set} = ThyDataSexp.new { 360 thydataty = "grammardelta", 361 merge = append_merge, 362 load = fn _ => (), 363 other_tds = other_tds 364 } 365 366fun thy_deltas {thyname} = 367 case segment_data {thyname = thyname} of 368 NONE => [] 369 | SOME gds => 370 case list_decode gdelta_decode gds of 371 NONE => raise Fail "GrammarDelta: encoding failure 2" 372 | SOME gds => gds 373 374 375 376fun userdelta_toString ud = 377 case ud of 378 OVERLOAD_ON (s, _) => "overload_on(" ^ Lib.mlquote s ^ ")" 379 | CLR_OVL s => "clear_overloads_on(" ^ Lib.mlquote s ^ ")" 380 | _ => "" 381 382fun record_tmdelta d = export (mk_list gdelta_encode [TMD d]) 383 384fun record_tydelta d = export (mk_list gdelta_encode [TYD d]) 385 386fun clear_deltas() = set (mk_list gdelta_encode []) 387 388end 389