1open HolKernel Parse boolLib simpLib bossLib 2open testutils 3 4local 5 open pegLib simpleSexpPEGTheory pegexecTheory 6 val ds = derive_compset_distincts ``:sexpNT`` 7 val {lookups,...} = derive_lookup_ths {pegth = sexpPEG_def, ntty = ``:sexpNT``, 8 simp = SIMP_CONV (srw_ss())} 9 val _ = computeLib.add_funs (ds::lookups) 10 val _ = let 11 open computeLib 12 in 13 set_skip the_compset ``evalcase_CASE`` (SOME 1); 14 set_skip the_compset ``option_CASE`` (SOME 1); 15 set_skip the_compset ``COND`` (SOME 1) 16 end 17in 18fun test0 nt s = let 19 val str_t = stringSyntax.fromMLstring s 20 val th = EVAL ``peg_exec sexpPEG (pnt ^nt) (MAP (��c. (c, unknown_loc)) (^str_t)) 21 [] done failed`` 22in 23 rhs (concl th) 24end 25end (* local *) 26 27fun test (s, exp) = let 28 val exp_t = ``Result (SOME ([], ^exp)) : (char, sexpNT, sexp) evalcase`` 29in 30 tprint (s ^ " --> " ^ term_to_string exp_t); 31 require_msg (check_result (aconv exp_t)) 32 term_to_string (test0 ``sxnt_sexp``) 33 s 34end 35val _ = temp_overload_on ("Ok", ``��t. (Result (SOME ([], t)))``) 36 37val _ = print "\n" before app test [ 38 ("123", ``123s``), 39 ("(123)", ``���123���``), 40 (" (123 10) ", ``���123; 10���``), 41 (" (123 10 (1 2 3)) ", ``��� 123; 10; ���1; 2; 3��� ���``), 42 (" ( (123 10 )) ", ``��� ��� 123; 10 ��� ���``), 43 ("'(1 2)", ``��� ���1; 2���``), 44 ("(1(2(3)))", ``���1; ��� 2; ��� 3 ��� ��� ���``), 45 ("'1", ``��� 1``), 46 ("foo", ``SX_SYM "foo"``), 47 ("(foo)", ``���SX_SYM "foo"���``), 48 ("()", ``nil``), 49 ("(foo )", ``���SX_SYM "foo"���``), 50 ("foo2", ``SX_SYM "foo2"``), 51 ("(foo bar 3 4)", ``��� SX_SYM "foo"; SX_SYM "bar"; 3; 4 ���``), 52 ("(1 2 3 . 4)", ``SX_CONS 1 (SX_CONS 2 (SX_CONS 3 4))``), 53 ("(1 . (2 . (3 . 4)))", ``SX_CONS 1 (SX_CONS 2 (SX_CONS 3 4))``), 54 ("(3 . 4)", ``SX_CONS 3 4``), 55 ("\"foo bar\"", ``SX_STR "foo bar"``), 56 ("( \" foo \" \"bar\" )", ``��� SX_STR " foo "; SX_STR "bar" ���``), 57 ("\"foo\\\"\"", ``SX_STR "foo\""``), 58 ("\"foo\\\\\"", ``SX_STR "foo\\"``), 59 ("(1sym)", ``���1; SX_SYM "sym"���``), 60 ("symq\"9", ``SX_SYM "symq\"9"``), 61 ("symd.9", ``SX_SYM "symd.9"``) 62] 63 64val _ = app tpp ["���2; 3���", "��� ���", "���SX_SYM \"foo\"���", "��� ���3 ��� 4���; ���3; 4��� ���"] 65