1open HolKernel Parse boolLib bossLib; 2 3local open stringLib in end 4 5open grammarLib 6open monadsyntax lcsymtacs pegTheory 7 8val _ = new_theory "simpleSexp"; 9 10val _ = temp_add_monadsyntax() 11 12val _ = overload_on ("monad_bind", ``OPTION_BIND``) 13val _ = overload_on ("monad_unitbind", ``OPTION_IGNORE_BIND``) 14val _ = temp_overload_on ("return", ``SOME``) 15val _ = temp_overload_on ("SOME", ``SOME``) 16 17val _ = computeLib.add_persistent_funs ["option.OPTION_BIND_def", 18 "option.OPTION_IGNORE_BIND_def", 19 "option.OPTION_GUARD_def", 20 "option.OPTION_CHOICE_def"] 21 22val _ = overload_on ("assert", ``option$OPTION_GUARD : bool -> unit option``) 23val _ = overload_on ("++", ``option$OPTION_CHOICE``) 24 25 26val _ = Datatype` 27 sexp = SX_CONS sexp sexp 28 | SX_SYM string 29 | SX_NUM num 30 | SX_STR string 31`; 32 33val _ = add_numeral_form(#"s", SOME "SX_NUM") 34val _ = overload_on ("nil", ``SX_SYM "nil"``) 35val _ = add_rule { block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)), 36 fixity = Closefix, 37 paren_style = OnlyIfNecessary, 38 pp_elements = [Parse.TOK "���", TM, HardSpace 1, 39 Parse.TOK "���", BreakSpace(1, 0), TM, 40 Parse.TOK "���"], 41 term_name = "SX_CONS" } 42val _ = add_listform { block_info = (PP.INCONSISTENT, 0), 43 cons = "SX_CONS", leftdelim = [Parse.TOK "���"], 44 nilstr = "nil", rightdelim = [Parse.TOK "���"], 45 separator = [Parse.TOK ";", BreakSpace(1,0)]} 46 47val _ = overload_on ("���", ``��s. ��� SX_SYM "quote" ; s ���``) 48 49val valid_first_symchar_def = Define` 50 valid_first_symchar c ��� isGraph c ��� c ��� {#"'"; #"("; #")"; #"."; #"\""} ��� ��isDigit c`; 51 52val valid_symchar_def = Define` 53 valid_symchar c ��� isGraph c ��� c ��� {#"'"; #"("; #")"}`; 54 55val valid_symbol_def = Define` 56 (valid_symbol "" ��� F) ��� 57 (valid_symbol (c::cs) ��� valid_first_symchar c ��� EVERY valid_symchar cs)`; 58 59val valid_sexp_def = Define` 60 (valid_sexp (SX_SYM s) ��� valid_symbol s) ��� 61 (valid_sexp (SX_CONS s1 s2) ��� valid_sexp s1 ��� valid_sexp s2) ��� 62 (valid_sexp (SX_STR s) ��� EVERY isPrint s) ��� 63 (valid_sexp s ��� T)`; 64val _ = export_rewrites["valid_first_symchar_def","valid_symchar_def","valid_symbol_def","valid_sexp_def"]; 65 66val arb_sexp_def = Define`arb_sexp = SX_NUM 0`; 67 68val destSXNUM_def = Define` 69 destSXNUM (SX_NUM n) = n ��� 70 destSXNUM _ = 0 71`; 72 73val destSXSYM_def = Define` 74 destSXSYM (SX_SYM s) = s ��� 75 destSXSYM _ = "" 76`; 77 78val destSXCONS_def = Define` 79 destSXCONS (SX_CONS a d) = (a,d) ��� 80 destSXCONS _ = (arb_sexp, arb_sexp) 81`; 82 83val strip_sxcons_def = Define` 84 strip_sxcons s = 85 case s of 86 SX_CONS h t => OPTION_MAP (CONS h) (strip_sxcons t) 87 | SX_SYM s => if s = "nil" then SOME [] 88 else NONE 89 | _ => NONE 90`; 91 92val sxMEM_def = Define` 93 sxMEM e s ��� ���l. strip_sxcons s = SOME l ��� MEM e l 94`; 95 96val sexp_size_def = definition"sexp_size_def"; 97 98val sxMEM_sizelt = store_thm( 99 "sxMEM_sizelt", 100 ``���s1 s2. sxMEM s1 s2 ��� sexp_size s1 < sexp_size s2``, 101 dsimp[sxMEM_def] >> Induct_on `s2` >> 102 dsimp[Once strip_sxcons_def, sexp_size_def] >> rpt strip_tac >> 103 res_tac >> simp[]); 104 105val dstrip_sexp_def = Define` 106 (dstrip_sexp (SX_CONS sym args) = 107 case sym of 108 SX_SYM s => OPTION_MAP (��t. (s, t)) (strip_sxcons args) 109 | _ => NONE) ��� 110 (dstrip_sexp _ = NONE) 111`; 112 113val tokmap = List.foldl (fn ((s,t), acc) => Binarymap.insert(acc, s, t)) 114 (Binarymap.mkDict String.compare) 115 [("(", ``#"("``), (")", ``#")"``), ("'", ``#"'"``), 116 ("\"", ``#"\""``), ("\\", ``#"\\"``), (".", ``#"."``)] 117 118fun toklookup s = 119 Binarymap.find(tokmap, s) 120 handle Binarymap.NotFound => raise Fail ("No tok def for "^s) 121 122val ginfo = { tokmap = toklookup, 123 tokty = ``:char``, nt_tyname = "sexpNT", start = "sexp", 124 gname = "sexpG", mkntname = (fn s => "sxnt_" ^ s) } 125 126 127val sexpG_def = mk_grammar_def ginfo ` 128 sexp ::= WSsexp grabWS ; 129 WSsexp ::= grabWS sexp0 ; 130 grabWS ::= WS grabWS | ; 131 WS ::= ^(``{ c | isSpace c }``) ; 132 sexp0 ::= sexpsym | sexpnum | sexpstr | "(" sexpseq grabWS ")" 133 | "(" sexp "." sexp ")" | "'" WSsexp ; 134 135 sexpseq ::= WSsexp sexpseq | ; 136 137 sexpnum ::= sexpnum digit | digit ; 138 digit ::= ^(``{ c | isDigit c}``); 139 140 sexpstr ::= "\"" strcontents "\"" ; 141 strcontents ::= | strchar strcontents ; 142 strchar ::= normstrchar | escapedstrchar ; 143 normstrchar ::= ^(``{ c | isPrint c ��� c ��� #"\\" ��� c ��� #"\"" }``) ; 144 escapedstrchar ::= "\\" escapablechar ; 145 escapablechar ::= "\\" | "\"" ; 146 147 sexpsym ::= first_symchar symchars ; 148 first_symchar ::= ^(``{ c | valid_first_symchar c }``) 149 ; 150 symchars ::= symchar symchars | ; 151 symchar ::= ^(``{ c | valid_symchar c }``); 152`; 153 154val _ = type_abbrev("NT", ``:sexpNT inf``) 155val _ = overload_on("mkNT", ``INL : sexpNT -> NT``) 156val _ = overload_on ("TK", ``TOK : char -> (char,sexpNT)symbol``) 157 158 159val ptree_digit_def = Define` 160 (ptree_digit (Lf _) = NONE) ��� 161 (ptree_digit (Nd (ntm,_) args) = 162 if ntm ��� mkNT sxnt_digit then NONE 163 else 164 case args of 165 [Lf tksym] => 166 do 167 c <- destTOK tksym ; 168 return (ORD c - ORD #"0") 169 od 170 | _ => NONE) 171`; 172 173val ptree_sexpnum_def = Define` 174 (ptree_sexpnum (Lf _) = NONE) ��� 175 (ptree_sexpnum (Nd (ntm,_) args) = 176 if ntm ��� mkNT sxnt_sexpnum then NONE 177 else 178 case args of 179 [d] => ptree_digit d 180 | [sn; d] => 181 do 182 dn <- ptree_digit d ; 183 snn <- ptree_sexpnum sn ; 184 return (10 * snn + dn) 185 od 186 | _ => NONE) 187`; 188 189 190val ptree_WS_def = Define` 191 (ptree_WS (Lf _) = NONE) ��� 192 (ptree_WS (Nd (ntm,_) args) = 193 if ntm ��� mkNT sxnt_WS then NONE 194 else 195 case args of 196 [c] => return () 197 | _ => NONE)`; 198 199val ptree_grabWS_def = Define` 200 (ptree_grabWS (Lf _) = NONE) ��� 201 (ptree_grabWS (Nd (ntm,_) args) = 202 if ntm ��� mkNT sxnt_grabWS then NONE 203 else 204 case args of 205 [w; g] => 206 do 207 ptree_WS w; 208 ptree_grabWS g; 209 return () 210 od 211 | _ => NONE)`; 212 213val ptree_normstrchar_def = Define` 214 (ptree_normstrchar (Lf _) = NONE) ��� 215 (ptree_normstrchar (Nd (ntm,_) args) = 216 if ntm ��� mkNT sxnt_normstrchar then NONE 217 else 218 case args of 219 [Lf(TK c,_)] => return c 220 | _ => NONE)`; 221 222val ptree_escapablechar_def = Define` 223 (ptree_escapablechar (Lf _) = NONE) ��� 224 (ptree_escapablechar (Nd (ntm,_) args) = 225 if ntm ��� mkNT sxnt_escapablechar then NONE 226 else 227 case args of 228 [Lf(TK c,_)] => return c 229 | _ => NONE)`; 230 231val ptree_escapedstrchar_def = Define` 232 (ptree_escapedstrchar (Lf _) = NONE) ��� 233 (ptree_escapedstrchar (Nd (ntm,_) args) = 234 if ntm ��� mkNT sxnt_escapedstrchar then NONE 235 else 236 case args of 237 [Lf(TK#"\\",_) ; c] => ptree_escapablechar c 238 | _ => NONE)`; 239 240val ptree_strchar_def = Define` 241 (ptree_strchar (Lf _) = NONE) ��� 242 (ptree_strchar (Nd (ntm,_) args) = 243 if ntm ��� mkNT sxnt_strchar then NONE 244 else 245 case args of 246 [c] => ptree_normstrchar c ++ ptree_escapedstrchar c 247 | _ => NONE)`; 248 249val ptree_strcontents_def = Define` 250 (ptree_strcontents (Lf _) = NONE) ��� 251 (ptree_strcontents (Nd (ntm,_) args) = 252 if ntm ��� mkNT sxnt_strcontents then NONE 253 else 254 case args of 255 [] => return "" 256 | [sc; ss] => 257 do 258 c <- ptree_strchar sc; 259 s <- ptree_strcontents ss; 260 return (c::s) 261 od 262 | _ => NONE)`; 263 264val ptree_sexpstr_def = Define` 265 (ptree_sexpstr (Lf _) = NONE) ��� 266 (ptree_sexpstr (Nd (ntm,_) args) = 267 if ntm ��� mkNT sxnt_sexpstr then NONE 268 else 269 case args of 270 [Lf(TK#"\"",_) ; s; Lf(TK#"\"",_)] => ptree_strcontents s 271 | _ => NONE)`; 272 273val ptree_first_symchar_def = Define` 274 (ptree_first_symchar (Lf _) = NONE) ��� 275 (ptree_first_symchar (Nd (ntm,_) args) = 276 if ntm ��� mkNT sxnt_first_symchar then NONE 277 else 278 case args of 279 [Lf(TK c,_)] => return c 280 | _ => NONE)`; 281 282val ptree_symchar_def = Define` 283 (ptree_symchar (Lf _) = NONE) ��� 284 (ptree_symchar (Nd (ntm,_) args) = 285 if ntm ��� mkNT sxnt_symchar then NONE 286 else 287 case args of 288 [Lf(TK c,_)] => return c 289 | _ => NONE)`; 290 291val ptree_symchars_def = Define` 292 (ptree_symchars (Lf _) = NONE) ��� 293 (ptree_symchars (Nd (ntm,_) args) = 294 if ntm ��� mkNT sxnt_symchars then NONE 295 else 296 case args of 297 [f;s] => 298 do 299 c <- ptree_symchar f; 300 cs <- ptree_symchars s; 301 return (c::cs) 302 od 303 | _ => NONE)`; 304 305val ptree_sexpsym_def = Define` 306 (ptree_sexpsym (Lf _) = NONE) ��� 307 (ptree_sexpsym (Nd (ntm,_) args) = 308 if ntm ��� mkNT sxnt_sexpsym then NONE 309 else 310 case args of 311 [f;s] => 312 do 313 c <- ptree_first_symchar f; 314 cs <- ptree_symchars s; 315 return (c::cs) 316 od 317 | _ => NONE)`; 318 319val ptree_sexp_def = Define` 320 (ptree_sexp (Lf _) = NONE) ��� 321 (ptree_sexp (Nd (ntm,_) args) = 322 if ntm ��� mkNT sxnt_sexp then NONE 323 else 324 case args of 325 [w; g] => do ptree_grabWS g; ptree_WSsexp w od 326 | _ => NONE) ��� 327 (ptree_WSsexp (Lf _) = NONE) ��� 328 (ptree_WSsexp (Nd (ntm,_) args) = 329 if ntm ��� mkNT sxnt_WSsexp then NONE 330 else 331 case args of 332 [g; s] => do ptree_grabWS g; ptree_sexp0 s od 333 | _ => NONE) ��� 334 (ptree_sexp0 (Lf _) = NONE) ��� 335 (ptree_sexp0 (Nd (ntm,_) args) = 336 if ntm ��� mkNT sxnt_sexp0 then NONE 337 else 338 case args of 339 [s] => 340 do x <- ptree_sexpsym s; return (SX_SYM x) od ++ 341 do x <- ptree_sexpnum s; return (SX_NUM x) od ++ 342 do x <- ptree_sexpstr s; return (SX_STR x) od 343 | [Lf (TK#"'",_) ;w] => ptree_WSsexp w 344 | [Lf (TK#"(",_) ; s; g; Lf (TK#")",_) ] => 345 do 346 ptree_grabWS g; 347 ptree_sexpseq s 348 od 349 | [Lf (TK#"(",_); sa; Lf (TK#".",_) ; sd; Lf (TK#")",_) ] => 350 do 351 a <- ptree_sexp sa; 352 d <- ptree_sexp sd; 353 return (SX_CONS a d) 354 od 355 | _ => NONE) ��� 356 (ptree_sexpseq (Lf _) = NONE) ��� 357 (ptree_sexpseq (Nd (ntm,_) args) = 358 if ntm ��� mkNT sxnt_sexpseq then NONE 359 else 360 case args of 361 [] => return nil 362 | [w; s] => 363 do 364 x <- ptree_WSsexp w; 365 r <- ptree_sexpseq s; 366 return (SX_CONS x r) 367 od 368 | _ => NONE)`; 369 370 371val _ = export_theory() 372