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