1
2open HolKernel Parse boolLib bossLib term_tactic;
3open arithmeticTheory listTheory stringTheory;
4
5val _ = new_theory "source_values";
6
7(* Values in the source semantics are binary trees where the
8   leaves are natural numbers (num) *)
9Datatype:
10  v = Pair v v | Num num
11End
12
13(* Since strings are not in the representation, we have a function that
14   coverts strings into numbers. Note that parsing and pretty printing
15   is set up so that printing reproduces these strings when possible. *)
16Definition name_def:
17  name [] = 0 ���
18  name (c::cs) = ORD c * 256 ** (LENGTH cs) + name cs
19End
20
21Overload Name = �����n. Num (name n)���
22
23(* Lists are terminated with Num 0 *)
24Definition list_def[simp]:
25  list [] = Num 0 ���
26  list (x::xs) = Pair x (list xs)
27End
28
29(* various convenience functions below, most are automatic rewrites [simp] *)
30
31Definition less_def[simp]:
32  less (Num n) (Num m) <=> n < m
33End
34
35Definition plus_def[simp]:
36  plus (Num n) (Num m) = Num (n + m)
37End
38
39Definition minus_def[simp]:
40  minus (Num n) (Num m) = Num (n - m)
41End
42
43Definition div_def[simp]:
44  div (Num n) (Num m) = Num (n DIV m)
45End
46
47Definition head_def[simp]:
48  head (Pair x y) = x ���
49  head v = v
50End
51
52Definition tail_def[simp]:
53  tail (Pair x y) = y ���
54  tail v = v
55End
56
57Definition cons_def[simp]:
58  cons x y = Pair x y
59End
60
61Definition bool_def[simp]:
62  bool T = Num 1 ���
63  bool F = Num 0
64End
65
66Definition map_def[simp]:
67  map f xs = list (MAP f xs)
68End
69
70Overload "list" = ���map���;
71
72Definition pair_def[simp]:
73  pair f g (x,y) = Pair (f x) (g y)
74End
75
76Definition option_def[simp]:
77  option f NONE = list [] ���
78  option f (SOME x) = list [f x]
79End
80
81Definition char_def[simp]:
82  char c = Num (ORD c)
83End
84
85Definition isNum_def[simp]:
86  isNum (Num n) = T ��� isNum _ = F
87End
88
89Definition getNum_def[simp]:
90  getNum (Num n) = n ���
91  getNum _ = 0
92End
93
94Definition el1_def[simp]:
95  el1 v = head (tail v)
96End
97
98Definition el2_def[simp]:
99  el2 v = el1 (tail v)
100End
101
102Definition el3_def[simp]:
103  el3 v = el2 (tail v)
104End
105
106Overload isNil[inferior] = ���isNum���;
107Overload el0[inferior] = ���head���;
108
109Theorem isNum_bool[simp]:
110  isNum (bool b)
111Proof
112  Cases_on ���b��� \\ EVAL_TAC
113QED
114
115Theorem v_size_def[simp] = fetch "-" "v_size_def";
116
117Theorem all_macro_defs = LIST_CONJ [list_def, cons_def, bool_def,
118   map_def, pair_def, option_def];
119
120Definition is_upper_def:
121  (* checks whether string (represented as num) starts with uppercase letter *)
122  is_upper n =
123    if n < 256:num then
124      if n < 65 (* ord A = 65 *) then F else
125      if n < 91 (* ord Z = 90 *) then T else F
126    else is_upper (n DIV 256)
127End
128
129Definition otherwise_def[simp]:
130  otherwise x = x
131End
132
133val _ = export_theory();
134