string_encodingScript.sml
1Theory string_encoding
2Ancestors
3 string ASCIInumbers
4
5(* theory of encoding functions for encoding/decoding arbitrary string values
6 as "literals" in various forms.
7*)
8
9Datatype: delimiter = DQ | SQ | PIPE
10End
11
12Definition del_to_char_def[simp]:
13 del_to_char DQ = #"\"" /\
14 del_to_char SQ = #"'" /\
15 del_to_char PIPE = #"|"
16End
17
18Definition char_encode_def:
19 char_encode delopt c =
20 if ~ isPrint c then
21 if c = #"\n" then "\\n"
22 else if c = #"\t" then "\\t"
23 else if ORD c < 10 then
24 "\\00" ++ num_to_dec_string (ORD c)
25 else if ORD c < 100 then
26 "\\0" ++ num_to_dec_string (ORD c)
27 else "\\" ++ num_to_dec_string (ORD c)
28 else if c = #"\\" then "\\\\"
29 else case delopt of
30 NONE => [c]
31 | SOME d => if c = del_to_char d then
32 "\\" ++ [c]
33 else [c]
34End
35
36Definition char_decode_def:
37 char_decode delopt [] = NONE /\
38 char_decode delopt (c::s) =
39 if c = #"\\" then
40 case s of
41 [] => NONE
42 | c2 :: stl =>
43 if c2 = #"n" then SOME (#"\n", stl)
44 else if c2 = #"t" then SOME (#"\t", stl)
45 else if c2 = #"\\" then SOME (#"\\", stl)
46 else if isDigit c2 then
47 let d23 = TAKE 2 stl
48 in
49 if LENGTH d23 = 2 /\ EVERY isDigit d23 then
50 let n = num_from_dec_string (c2::d23)
51 in
52 if n < 256 then SOME (CHR n, DROP 2 stl)
53 else NONE
54 else NONE
55 else
56 case delopt of
57 NONE => NONE
58 | SOME d => if del_to_char d = c2 then SOME (c2, stl)
59 else NONE
60 else
61 if isPrint c then
62 case delopt of
63 NONE => SOME (c, s)
64 | SOME d => if del_to_char d = c then NONE
65 else SOME (c, s)
66 else NONE
67End
68
69Theorem char_decode_encode:
70 char_decode delopt (char_encode delopt c ++ s) =
71 SOME (c, s)
72Proof
73 rw[char_decode_def, char_encode_def, stringTheory.isDigit_def] >>~-
74 ([‘TAKE _ (toString (ORD c) ++ s)’],
75 assume_tac (LENGTH_num_to_dec_string |> Q.INST [‘n’ |-> ‘ORD c’]) >>
76 qmatch_goalsub_abbrev_tac ‘TAKE n (toString (ORD _) ++ _)’ >>
77 ‘n = LENGTH (toString (ORD c))’
78 by (simp[] >>
79 rw[DECIDE “x:num = x + y <=> y = 0”, logrootTheory.LOG_EQ_0] >>
80 simp[Abbr‘n’, DECIDE “n <= y ==> (x + n = y <=> x = y - n)”] >>
81 irule logrootTheory.LOG_UNIQUE >> simp[]) >>
82 pop_assum SUBST1_TAC >> qpat_x_assum ‘LENGTH (toString _) = _’ kall_tac >>
83 simp[rich_listTheory.TAKE_LENGTH_APPEND, toNum_toString,
84 EVERY_isDigit_num_to_dec_string]) >>~-
85 ([‘DROP _ (toString (ORD c) ++ s)’],
86 assume_tac (LENGTH_num_to_dec_string |> Q.INST [‘n’ |-> ‘ORD c’]) >>
87 qmatch_goalsub_abbrev_tac ‘DROP n (toString (ORD _) ++ _)’ >>
88 ‘n = LENGTH (toString (ORD c))’
89 by (simp[] >>
90 rw[DECIDE “x:num = x + y <=> y = 0”, logrootTheory.LOG_EQ_0] >>
91 simp[Abbr‘n’, DECIDE “n <= y ==> (x + n = y <=> x = y - n)”] >>
92 irule logrootTheory.LOG_UNIQUE >> simp[]) >>
93 pop_assum SUBST1_TAC >> qpat_x_assum ‘LENGTH (toString _) = _’ kall_tac >>
94 simp[rich_listTheory.DROP_LENGTH_APPEND]) >~
95 [‘list_CASE (toString (ORD c) ++ s)’]
96 >- (Cases_on ‘toString (ORD c)’ >> gs[num_to_dec_string_nil] >>
97 qspec_then ‘ORD c’ mp_tac EVERY_isDigit_num_to_dec_string >>
98 simp[] >> rw[] >> gs[isDigit_def] >>
99 ‘LENGTH t = 2’
100 by (assume_tac
101 (LENGTH_num_to_dec_string |> Q.INST [‘n’ |-> ‘ORD c’]) >>
102 gs[arithmeticTheory.ADD1] >>
103 irule logrootTheory.LOG_UNIQUE >>
104 qspec_then ‘c’ assume_tac ORD_BOUND >> simp[]) >>
105 ‘TAKE 2 (t ++ s) = t /\ DROP 2 (t ++ s) = s’
106 by metis_tac[rich_listTheory.TAKE_LENGTH_APPEND,
107 rich_listTheory.DROP_LENGTH_APPEND] >>
108 gs[] >> metis_tac[CHR_ORD, toNum_toString, ORD_BOUND]) >>
109 Cases_on ‘delopt’>> simp[char_decode_def] >> rw[] >>
110 simp[char_decode_def] >>
111 rename [‘del_to_char d’] >> Cases_on ‘d’ >> gs[] >>
112 simp[isDigit_def]
113QED
114
115Theorem char_decode_reduces:
116 char_decode delopt s = SOME (c,s') ==> LENGTH s' < LENGTH s
117Proof
118 Cases_on ‘s’ >> rw[char_decode_def] >> gvs[AllCaseEqs()]
119QED
120
121Definition strencode_def:
122 strencode delopt s = FLAT (MAP (char_encode delopt) s)
123End
124
125Definition strdecode_def:
126 strdecode delopt s =
127 case char_decode delopt s of
128 NONE => (case (s,delopt) of
129 ([], _) => SOME("", [])
130 | (_, NONE) => NONE
131 | (c::tl, SOME d) => if c = del_to_char d then SOME("", c::tl)
132 else NONE)
133 | SOME(c, rest) => OPTION_MAP (CONS c ## I) (strdecode delopt rest)
134Termination
135 WF_REL_TAC ‘measure (LENGTH o SND)’ >> metis_tac[char_decode_reduces]
136End
137
138Definition delopt_to_str_def[simp]:
139 delopt_to_str NONE = "" /\
140 delopt_to_str (SOME d) = [del_to_char d]
141End
142
143(* reverse not true because \n and \t can be encoded with numeric forms as well
144*)
145Theorem strdecode_strencode_tail_delimited:
146 strdecode delopt (strencode delopt s ++ delopt_to_str delopt) =
147 SOME (s, delopt_to_str delopt)
148Proof
149 simp[strencode_def] >> completeInduct_on ‘LENGTH s’ >> gs[PULL_FORALL] >>
150 qx_gen_tac ‘s’ >> rw[] >>
151 Cases_on ‘s’ >> simp[] >> rw[]
152 >- (Cases_on ‘delopt’ >>
153 simp[Once strdecode_def, char_decode_def] >>
154 rename [‘char_decode (SOME d)’] >> Cases_on ‘d’ >>
155 simp[char_decode_def]) >>
156 simp[Once strdecode_def] >>
157 REWRITE_TAC[char_decode_encode, GSYM listTheory.APPEND_ASSOC] >>
158 simp[pairTheory.EXISTS_PROD]
159QED
160
161Theorem strdecode_strencode:
162 strdecode delopt (strencode delopt s) = SOME (s, "")
163Proof
164 simp[strencode_def] >> completeInduct_on ‘LENGTH s’ >> gs[PULL_FORALL] >>
165 qx_gen_tac ‘s’ >> rw[] >>
166 Cases_on ‘s’ >> simp[] >> rw[]
167 >- (simp[Once strdecode_def, char_decode_def]) >>
168 simp[Once strdecode_def] >>
169 REWRITE_TAC[char_decode_encode, GSYM listTheory.APPEND_ASSOC] >>
170 simp[pairTheory.EXISTS_PROD]
171QED
172
173Theorem char_encode_isPrintable:
174 EVERY isPrint (char_encode delopt c)
175Proof
176 rw[char_encode_def, isPrint_def] >>~-
177 ([‘EVERY isPrint (toString _)’],
178 irule listTheory.MONO_EVERY >> qexists ‘isDigit’ >>
179 simp[EVERY_isDigit_num_to_dec_string] >>
180 simp[isDigit_def, isPrint_def]) >>
181 Cases_on ‘delopt’ >> rw[] >> gs[isPrint_def]
182QED
183
184Theorem strencode_isPrintable:
185 EVERY isPrint (strencode delopt s)
186Proof
187 simp[strencode_def, listTheory.EVERY_FLAT, listTheory.EVERY_MAP,
188 char_encode_isPrintable]
189QED
190
191
192