Idiomatic explode

explode.rkt

#lang racket
(require redex)
(current-cache-all? #t)
   
;; String -> (Listof 1String)
(define (explode s)
  (car (apply-reduction-relation* split+join s)))

;; String -> Void
(define (show-explode s)
  (traces split+join s))

(define-language STRINGS
  (e ::= string)
  (f ::= (side-condition string_1 (not (equal? (term string_1) ""))))
  (g ::= (side-condition string_1 (= 1 (string-length (term string_1)))))
  (n ::= natural)
  (s ::= (e n)))

(define split+join
  (reduction-relation
   STRINGS
   (--> e ((e 0)))
   (--> (s_1 ... (e n) s_2 ...)
        (s_1 ... (f_i ,(term n)) (f_j ,(+ (term n) (term n_i))) s_2 ...)
        (judgment-holds (substrings e f_i f_j n_i)))
   (--> (e_0 ... (e_1 n_1) ... (g 0) (e_2 n_2) ...)
        (e_0 ... g (e_1 n_1d) ... (e_2 n_2d) ...)
        (where (n_1d ...) (decr (n_1 ...)))
        (where (n_2d ...) (decr (n_2 ...))))
   (--> (e_0 ... s_1 s_2 ...)
        (e_0 ... s_1 s_2 ...))
   (--> (e_0 ... s_1 ... s_2 s_3 s_4 ...)
        (e_0 ... s_1 ... s_3 s_2 s_4 ...))))

(define-judgment-form STRINGS 
  #:mode (substrings I O O O)
  [(substrings e e_1 e_2 n)
   (range ,(string-length (term e)) n)
   (where e_1 ,(substring (term e) 0 (term n)))
   (where e_2 ,(substring (term e) (term n)))])

(define-judgment-form STRINGS  
  #:mode (range I O)
  [(range n 0)]
  [(range n n)]
  [(range n n_2) (range ,(sub1 (term n)) n_2)])

(define-metafunction STRINGS
  decr : (n ...) -> (n ...)
  [(decr ()) ()]
  [(decr (n_1 n_2 ...))
   (,(sub1 (term n_1)) n_3 ...)
   (where (n_3 ...) (decr (n_2 ...)))])