open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_sexp";

open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory;
open combinTheory finite_mapTheory stringTheory;


infix \\
val op \\ = op THEN;
val RW = REWRITE_RULE;
val RW1 = ONCE_REWRITE_RULE;


(* type *)

val _ = Hol_datatype `SExp = Dot of SExp => SExp | Val of num | Sym of string`;
val SExp_11 = fetch "-" "SExp_11";
val SExp_distinct = fetch "-" "SExp_distinct";


(* definitions *)

val isDot_def = Define `
  (isDot (Dot x y) = T) /\ (isDot (Val n) = F) /\ (isDot (Sym s) = F)`;
val isVal_def = Define `
  (isVal (Dot x y) = F) /\ (isVal (Val n) = T) /\ (isVal (Sym s) = F)`;
val isSym_def = Define `
  (isSym (Dot x y) = F) /\ (isSym (Val n) = F) /\ (isSym (Sym s) = T)`;

val getVal_def = Define `
  (getVal (Dot x y) = 0) /\ (getVal (Val n) = n) /\ (getVal (Sym s) = 0)`;
val getSym_def = Define `
  (getSym (Dot x y) = "NIL") /\ (getSym (Val n) = "NIL") /\ (getSym (Sym s) = s)`;

val CAR_def = Define `
  (CAR (Dot x y) = x) /\
  (CAR (Val w) = Sym "NIL") /\
  (CAR (Sym s) = Sym "NIL")`;

val CDR_def = Define `
  (CDR (Dot x y) = y) /\
  (CDR (Val w) = Sym "NIL") /\
  (CDR (Sym s) = Sym "NIL")`;

val LISP_CONS_def  = Define `LISP_CONS x y = Dot x y`;

val LISP_ADD_def   = Define `LISP_ADD  x y = Val (getVal x + getVal y)`;
val LISP_SUB_def   = Define `LISP_SUB  x y = Val (getVal x - getVal y)`;
val LISP_MULT_def  = Define `LISP_MULT x y = Val (getVal x * getVal y)`;
val LISP_DIV_def   = Define `LISP_DIV  x y = Val (getVal x DIV getVal y)`;
val LISP_MOD_def   = Define `LISP_MOD  x y = Val (getVal x MOD getVal y)`;

val LISP_TEST_def  = Define `LISP_TEST x = if x then Sym "T" else Sym "NIL"`;

val LISP_EQUAL_def   = Define `LISP_EQUAL x y = LISP_TEST (x = y)`;
val LISP_LESS_def    = Define `LISP_LESS m n  = LISP_TEST (getVal m < getVal n)`;
val LISP_ATOMP_def   = Define `LISP_ATOMP x   = LISP_TEST (~(isDot x))`;
val LISP_CONSP_def   = Define `LISP_CONSP x   = LISP_TEST (isDot x)`;
val LISP_NUMBERP_def = Define `LISP_NUMBERP x = LISP_TEST (isVal x)`;
val LISP_SYMBOLP_def = Define `LISP_SYMBOLP x = LISP_TEST (isSym x)`;
val LISP_SYMBOL_LESS_def = Define `LISP_SYMBOL_LESS x y = LISP_TEST (getSym x < getSym y)`;

val TASK_CONT_def = Define `TASK_CONT = Sym "T"`;
val TASK_EVAL_def = Define `TASK_EVAL = Sym "NIL"`;
val TASK_FUNC_def = Define `TASK_FUNC = Sym "QUOTE"`;

val isQuote_def = Define `
  isQuote x = isDot x /\ (CAR x = Sym "QUOTE") /\
              isDot (CDR x) /\ (CDR (CDR x) = Sym "NIL")`;

val LSIZE_def = Define `
  (LSIZE (Dot x y) = SUC (LSIZE x + LSIZE y)) /\
  (LSIZE (Val w) = 0) /\
  (LSIZE (Sym s) = 0)`;

val LDEPTH_def = Define `
  (LDEPTH (Dot x y) = SUC (MAX (LDEPTH x) (LDEPTH y))) /\
  (LDEPTH (Val w) = 0) /\
  (LDEPTH (Sym s) = 0)`;

val SUM_LSIZE_def = Define `
  (SUM_LSIZE [] = 0) /\
  (SUM_LSIZE (x::xs) = LSIZE x + SUM_LSIZE xs)`;

val UPDATE_NTH_def = Define `
  (UPDATE_NTH 0 x [] = []) /\
  (UPDATE_NTH (SUC n) x [] = []) /\
  (UPDATE_NTH 0 x (y::ys) = x::ys) /\
  (UPDATE_NTH (SUC n) x (y::ys) = y::UPDATE_NTH n (x:'a) ys)`;

val _ = Hol_datatype `
  lisp_primitive_op =
    opCONS | opEQUAL | opLESS | opSYMBOL_LESS | opADD | opSUB |
    opCONSP | opNATP | opSYMBOLP | opCAR | opCDR`;

val isTrue_def = Define `isTrue s = ~(s = Sym "NIL")`;


(* theorems *)

val SExp_expand = store_thm("SExp_expand",
  ``!x. (?exp1 exp2. x = Dot exp1 exp2) \/ (?n. x = Val n) \/ (?s. x = Sym s)``,
  Cases \\ SRW_TAC [] []);

val isDot_thm = store_thm("isDot_thm",
  ``!z. isDot z = ?a b. z = Dot a b``,
  Cases \\ SIMP_TAC std_ss [SExp_11,SExp_distinct,isDot_def]);

val isVal_thm = store_thm("isVal_thm",
  ``!z. isVal z = ?a. z = Val a``,
  Cases \\ SIMP_TAC std_ss [SExp_11,SExp_distinct,isVal_def]);

val isSym_thm = store_thm("isSym_thm",
  ``!z. isSym z = ?a. z = Sym a``,
  Cases \\ SIMP_TAC std_ss [SExp_11,SExp_distinct,isSym_def]);

val isQuote_thm = store_thm("isQuote_thm",
  ``!x. isQuote x = ?y. x = Dot (Sym "QUOTE") (Dot y (Sym "NIL"))``,
  Cases \\ REWRITE_TAC [isQuote_def,isDot_def,CAR_def,CDR_def,SExp_11]
  \\ SIMP_TAC std_ss [SExp_distinct] \\ Cases_on `S0`
  \\ REWRITE_TAC [isQuote_def,isDot_def,CAR_def,CDR_def,SExp_11]
  \\ METIS_TAC [SExp_distinct]);


val _ = export_theory();