The smart way and the dumb way

flat-v-ho.rkt

#lang racket
(require redex/reduction-semantics)

(define-language pre-C
  (CON X
       nat?
       (or/c CON CON)
       (rec/c X CON)
       (cons/c CON CON)
       (CON -> CON))
  (X variable-not-otherwise-mentioned))

(define-metafunction pre-C
  flat? : CON -> #t or #f
  [(flat? nat?) #t]
  [(flat? (or/c CON_1 CON_2))
   ,(and (term (flat? CON_1))
         (term (flat? CON_2)))]
  [(flat? (rec/c X CON))
   (flat? (subst (subst nat? X CON) X CON))]
  [(flat? (cons/c CON_1 CON_2))
   ,(and (term (flat? CON_1))
         (term (flat? CON_2)))]
  [(flat? (CON_1 -> CON_2)) #f])

(define-metafunction pre-C
  subst : CON X CON -> CON
  [(subst CON X nat?) nat?] 
  [(subst CON X X) CON]
  [(subst CON X X_1) X_1]
  [(subst CON X (or/c CON_1 CON_2))
   (or/c (subst CON X CON_1)
         (subst CON X CON_2))]
  [(subst CON X (rec/c X CON_1)) (rec/c X CON_1)]
  [(subst CON X (rec/c X_1 CON_1)) (rec/c X_1 (subst CON X CON_1))]
  [(subst CON X (cons/c CON_1 CON_2))
   (cons/c (subst CON X CON_1)
           (subst CON X CON_2))]
  [(subst CON X (CON_1 -> CON_2))
   ((subst CON X CON_1) -> (subst CON X CON_2))])

(define-language C
  (CON X
       nat?
       (or/c CON CON)
       (rec/c X CON)
       (cons/c CON CON)
       (CON -> CON))
  (X variable)
  
  (FLAT (side-condition (name x CON)
                        (redex-match pre-C #t (term (flat? x)))))
  
  (FLAT-DUMB (side-condition (name x CON)
                             (no-arrow? (term x)))))

(define (no-arrow? x)
  (match x
    [(list-no-order '-> _ ...) #f]
    [(list y ...) (andmap no-arrow? y)]
    [_ #t]))
  
  

(define f? (redex-match C FLAT))
(define h? (negate f?))

(test-predicate h? '(rec/c X (nat? -> nat?)))
(test-predicate h? '(rec/c X (nat? -> X)))
(test-predicate h? '(rec/c X (X -> X)))
(test-predicate h? '(rec/c X (cons/c X (X -> X))))
(test-predicate f? '(rec/c X (or/c (cons/c X X) (cons/c X X))))
(test-predicate f? '(rec/c X (rec/c Y (or/c (cons/c X Y) (cons/c Y X)))))

(define fd? (redex-match C FLAT-DUMB))
(define hd? (negate fd?))

(test-predicate hd? '(rec/c X (nat? -> nat?)))
(test-predicate hd? '(rec/c X (nat? -> X)))
(test-predicate hd? '(rec/c X (X -> X)))
(test-predicate hd? '(rec/c X (cons/c X (X -> X))))
(test-predicate fd? '(rec/c X (or/c (cons/c X X) (cons/c X X))))
(test-predicate fd? '(rec/c X (rec/c Y (or/c (cons/c X Y) (cons/c Y X)))))