1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_sexp";
2
3open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory;
4open combinTheory finite_mapTheory stringTheory;
5
6
7infix \\
8val op \\ = op THEN;
9val RW = REWRITE_RULE;
10val RW1 = ONCE_REWRITE_RULE;
11
12
13(* type *)
14
15val _ = Hol_datatype `SExp = Dot of SExp => SExp | Val of num | Sym of string`;
16val SExp_11 = fetch "-" "SExp_11";
17val SExp_distinct = fetch "-" "SExp_distinct";
18
19
20(* definitions *)
21
22val isDot_def = Define `
23  (isDot (Dot x y) = T) /\ (isDot (Val n) = F) /\ (isDot (Sym s) = F)`;
24val isVal_def = Define `
25  (isVal (Dot x y) = F) /\ (isVal (Val n) = T) /\ (isVal (Sym s) = F)`;
26val isSym_def = Define `
27  (isSym (Dot x y) = F) /\ (isSym (Val n) = F) /\ (isSym (Sym s) = T)`;
28
29val getVal_def = Define `
30  (getVal (Dot x y) = 0) /\ (getVal (Val n) = n) /\ (getVal (Sym s) = 0)`;
31val getSym_def = Define `
32  (getSym (Dot x y) = "NIL") /\ (getSym (Val n) = "NIL") /\ (getSym (Sym s) = s)`;
33
34val CAR_def = Define `
35  (CAR (Dot x y) = x) /\
36  (CAR (Val w) = Sym "NIL") /\
37  (CAR (Sym s) = Sym "NIL")`;
38
39val CDR_def = Define `
40  (CDR (Dot x y) = y) /\
41  (CDR (Val w) = Sym "NIL") /\
42  (CDR (Sym s) = Sym "NIL")`;
43
44val LISP_CONS_def  = Define `LISP_CONS x y = Dot x y`;
45
46val LISP_ADD_def   = Define `LISP_ADD  x y = Val (getVal x + getVal y)`;
47val LISP_SUB_def   = Define `LISP_SUB  x y = Val (getVal x - getVal y)`;
48val LISP_MULT_def  = Define `LISP_MULT x y = Val (getVal x * getVal y)`;
49val LISP_DIV_def   = Define `LISP_DIV  x y = Val (getVal x DIV getVal y)`;
50val LISP_MOD_def   = Define `LISP_MOD  x y = Val (getVal x MOD getVal y)`;
51
52val LISP_TEST_def  = Define `LISP_TEST x = if x then Sym "T" else Sym "NIL"`;
53
54val LISP_EQUAL_def   = Define `LISP_EQUAL x y = LISP_TEST (x = y)`;
55val LISP_LESS_def    = Define `LISP_LESS m n  = LISP_TEST (getVal m < getVal n)`;
56val LISP_ATOMP_def   = Define `LISP_ATOMP x   = LISP_TEST (~(isDot x))`;
57val LISP_CONSP_def   = Define `LISP_CONSP x   = LISP_TEST (isDot x)`;
58val LISP_NUMBERP_def = Define `LISP_NUMBERP x = LISP_TEST (isVal x)`;
59val LISP_SYMBOLP_def = Define `LISP_SYMBOLP x = LISP_TEST (isSym x)`;
60val LISP_SYMBOL_LESS_def = Define `LISP_SYMBOL_LESS x y = LISP_TEST (getSym x < getSym y)`;
61
62val TASK_CONT_def = Define `TASK_CONT = Sym "T"`;
63val TASK_EVAL_def = Define `TASK_EVAL = Sym "NIL"`;
64val TASK_FUNC_def = Define `TASK_FUNC = Sym "QUOTE"`;
65
66val isQuote_def = Define `
67  isQuote x = isDot x /\ (CAR x = Sym "QUOTE") /\
68              isDot (CDR x) /\ (CDR (CDR x) = Sym "NIL")`;
69
70val LSIZE_def = Define `
71  (LSIZE (Dot x y) = SUC (LSIZE x + LSIZE y)) /\
72  (LSIZE (Val w) = 0) /\
73  (LSIZE (Sym s) = 0)`;
74
75val LDEPTH_def = Define `
76  (LDEPTH (Dot x y) = SUC (MAX (LDEPTH x) (LDEPTH y))) /\
77  (LDEPTH (Val w) = 0) /\
78  (LDEPTH (Sym s) = 0)`;
79
80val SUM_LSIZE_def = Define `
81  (SUM_LSIZE [] = 0) /\
82  (SUM_LSIZE (x::xs) = LSIZE x + SUM_LSIZE xs)`;
83
84val UPDATE_NTH_def = Define `
85  (UPDATE_NTH 0 x [] = []) /\
86  (UPDATE_NTH (SUC n) x [] = []) /\
87  (UPDATE_NTH 0 x (y::ys) = x::ys) /\
88  (UPDATE_NTH (SUC n) x (y::ys) = y::UPDATE_NTH n (x:'a) ys)`;
89
90val _ = Hol_datatype `
91  lisp_primitive_op =
92    opCONS | opEQUAL | opLESS | opSYMBOL_LESS | opADD | opSUB |
93    opCONSP | opNATP | opSYMBOLP | opCAR | opCDR`;
94
95val isTrue_def = Define `isTrue s = ~(s = Sym "NIL")`;
96
97
98(* theorems *)
99
100val SExp_expand = store_thm("SExp_expand",
101  ``!x. (?exp1 exp2. x = Dot exp1 exp2) \/ (?n. x = Val n) \/ (?s. x = Sym s)``,
102  Cases \\ SRW_TAC [] []);
103
104val isDot_thm = store_thm("isDot_thm",
105  ``!z. isDot z = ?a b. z = Dot a b``,
106  Cases \\ SIMP_TAC std_ss [SExp_11,SExp_distinct,isDot_def]);
107
108val isVal_thm = store_thm("isVal_thm",
109  ``!z. isVal z = ?a. z = Val a``,
110  Cases \\ SIMP_TAC std_ss [SExp_11,SExp_distinct,isVal_def]);
111
112val isSym_thm = store_thm("isSym_thm",
113  ``!z. isSym z = ?a. z = Sym a``,
114  Cases \\ SIMP_TAC std_ss [SExp_11,SExp_distinct,isSym_def]);
115
116val isQuote_thm = store_thm("isQuote_thm",
117  ``!x. isQuote x = ?y. x = Dot (Sym "QUOTE") (Dot y (Sym "NIL"))``,
118  Cases \\ REWRITE_TAC [isQuote_def,isDot_def,CAR_def,CDR_def,SExp_11]
119  \\ SIMP_TAC std_ss [SExp_distinct] \\ Cases_on `S0`
120  \\ REWRITE_TAC [isQuote_def,isDot_def,CAR_def,CDR_def,SExp_11]
121  \\ METIS_TAC [SExp_distinct]);
122
123
124val _ = export_theory();
125