213 else down c r1 (SeqC r2 False # ctxts))" |
213 else down c r1 (SeqC r2 False # ctxts))" |
214 | "down c (CH d) ctxts = |
214 | "down c (CH d) ctxts = |
215 (if c = d then up c ONE ctxts else up c ZERO ctxts)" |
215 (if c = d then up c ONE ctxts else up c ZERO ctxts)" |
216 | "down c ONE ctxts = up c ZERO ctxts" |
216 | "down c ONE ctxts = up c ZERO ctxts" |
217 | "down c ZERO ctxts = up c ZERO ctxts" |
217 | "down c ZERO ctxts = up c ZERO ctxts" |
218 | "down c (ALT r1 r2) ctxts = down c r1 (AltCR r2 # ctxts)" |
218 | "down c (ALT r1 r2) ctxts = down c r1 (AltCH r2 # ctxts)" |
219 | "down c (STAR r1) ctxts = down c r1 (StarC r1 # ctxts)" |
219 | "down c (STAR r1) ctxts = down c r1 (StarC r1 # ctxts)" |
220 | "up c r [] = (r, [])" |
220 | "up c r [] = (r, [])" |
221 | "up c r (SeqC r2 False # ctxts) = up c (SEQ r r2) ctxts" |
221 | "up c r (SeqC r2 False # ctxts) = up c (SEQ r r2) ctxts" |
222 | "up c r (SeqC r2 True # ctxts) = down c r2 (AltCL (SEQ r r2) # ctxts)" |
222 | "up c r (SeqC r2 True # ctxts) = down c r2 (AltCL (SEQ r r2) # ctxts)" |
223 | "up c r (AltCL r1 # ctxts) = up c (ALT r1 r) ctxts" |
223 | "up c r (AltCL r1 # ctxts) = up c (ALT r1 r) ctxts" |
224 | "up c r (AltCR r2 # ctxts) = down c r2 (AltCL r # ctxts)" |
224 | "up c r (AltCH r2 # ctxts) = down c r2 (AltCL r # ctxts)" |
225 | "up c r (StarC r1 # ctxts) = up c (SEQ r (STAR r1)) ctxts" |
225 | "up c r (StarC r1 # ctxts) = up c (SEQ r (STAR r1)) ctxts" |
226 apply(pat_completeness) |
226 apply(pat_completeness) |
227 apply(auto) |
227 apply(auto) |
228 done |
228 done |
229 |
229 |