(module tl-test mzscheme
  (require "../reduction-semantics.ss"
           "test-util.ss")
  
  (reset-count)
  
  (define grammar
    (language (M (M M)
                 number)
              (E hole
                 (E M)
                 (number E))
              (X (number any)
                 (any number))
              (Q (Q ...)
                 variable)
              (UN (add1 UN)
                  zero)))
  
  (define-metafunction f
    grammar
    [(side-condition (number_1 number_2)
                     (< (term number_1)
                        (term number_2)))
     x]
    [(number 1) y]
    [(number_1 2) ,(+ (term number_1) 2)]
    [(4 4) q]
    [(4 4) r])
  
  (define-metafunction g
    grammar
    [X x])
  
  (test (term (f (1 17))) 'x)
  (test (term (f (11 1))) 'y)
  (test (term (f (11 2))) 13)
  
  ;; match two clauess => take first one
  (test (term (f (4 4))) 'q)
  
  ;; match one clause two ways => error
  (test (with-handlers ((exn? (λ (x) 'exn-raised))) (term (g (4 4))) 'no-exn)
        'exn-raised)
  
  ;; match no ways => error
  (test (with-handlers ((exn? (λ (x) 'exn-raised))) (term (f mis-match)) 'no-exn)
        'exn-raised)

  (define-metafunction h
    grammar
    [(M_1 M_2) ((h M_2) (h M_1))]
    [number_1 ,(+ (term number_1) 1)])
  
  (test (term (h ((1 2) 3)))
        (term (4 (3 2))))
  
  (define-metafunction h2
    grammar
    [(Q_1 ...) ((h2 Q_1) ...)]
    [variable z])
  
  (test (term (h2 ((x y) a b c)))
        (term ((z z) z z z)))
  
  ;; mutually recursive metafunctions
  (define-metafunction odd
    grammar
    [zero #f]
    [(add1 UN_1) (even UN_1)])
  
  (define-metafunction even
    grammar
    [zero #t]
    [(add1 UN_1) (odd UN_1)])
  
  (test (term (odd (add1 (add1 (add1 (add1 zero))))))
        (term #f))
    
  (let ()
    (define-metafunction pRe
      (language)
      [xxx 1])
    
    (define-metafunction Merge-Exns
      (language)
      [any_1 any_1])
    
    (test (term (pRe (Merge-Exns xxx)))
          1))
  
  (let ()
    (define-metafunction f
      (language)
      [(x) ,(term-let ([var-should-be-lookedup 'y]) (term (f var-should-be-lookedup)))]
      [y y]
      [var-should-be-lookedup var-should-be-lookedup]) ;; taking this case is bad!
    
    (test (term (f (x))) (term y)))
  
  (let ()
    (define-metafunction f
      (language)
      [(x) (x ,@(term-let ([var-should-be-lookedup 'y]) (term (f var-should-be-lookedup))) x)]
      [y (y)]
      [var-should-be-lookedup (var-should-be-lookedup)]) ;; taking this case is bad!
    
    (test (term (f (x))) (term (x y x))))
  
  (let ()
    (define-metafunction f
      (language)
      [(any_1 any_2)
       case1
       (side-condition (not (equal? (term any_1) (term any_2))))
       (side-condition (not (equal? (term any_1) 'x)))]
      [(any_1 any_2)
       case2
       (side-condition (not (equal? (term any_1) (term any_2))))]
      [(any_1 any_2)
       case3])
    (test (term (f (q r))) (term case1))
    (test (term (f (x y))) (term case2))
    (test (term (f (x x))) (term case3)))

  ;; test ..._1 patterns
  (let ()
    (define-metafunction zip (language)
      [((variable_id ..._1) (number_val ..._1))
       ((variable_id number_val) ...)])
    
    (test (term (zip ((a b) (1 2)))) (term ((a 1) (b 2)))))
  
  (test (pair? (test-match grammar M '(1 1))) #t)
  (test (pair? (test-match grammar M '(1 1 1))) #f)
  (test (pair? (test-match grammar
                           (side-condition (M_1 M_2) (equal? (term M_1) (term M_2)))
                           '(1 1)))
        #t)
  (test (pair? (test-match grammar
                           (side-condition (M_1 M_2) (equal? (term M_1) (term M_2))) 
                           '(1 2)))
        #f)
  
  (test (pair? ((test-match grammar M) '(1 1)))
        #t)

  (define base-grammar
    (language
     (q 1)
     (e (+ e e) number)
     (x (variable-except +))))
  
  (define extended-grammar
    (extend-language
     base-grammar 
     (e .... (* e e))
     (x (variable-except + *))
     (r 2)))
  
  (test (pair? (test-match extended-grammar e '(+ 1 1))) #t)
  (test (pair? (test-match extended-grammar e '(* 2 2))) #t)
  (test (pair? (test-match extended-grammar r '2)) #t)
  (test (pair? (test-match extended-grammar q '1)) #t)
  (test (pair? (test-match extended-grammar x '*)) #f)
  (test (pair? (test-match extended-grammar x '+)) #f)
  (test (pair? (test-match extended-grammar e '....)) #f)
  
  ;; make sure that `language' with a four period ellipses signals an error
  (test (regexp-match #rx"[.][.][.][.]" (with-handlers ([exn? exn-message]) (language (e ....))))
        '("...."))
  
  (test (apply-reduction-relation
         (reduction-relation 
          grammar
          (--> (in-hole E_1 (number_1 number_2))
               (in-hole E_1 ,(* (term number_1) (term number_2)))))
         '((2 3) (4 5)))
        (list '(6 (4 5))))
  
  (test (apply-reduction-relation
         (reduction-relation 
          grammar
          (~~> (number_1 number_2)
               ,(* (term number_1) (term number_2)))
          where
          [(~~> a b) (--> (in-hole E_1 a) (in-hole E_1 b))])
         '((2 3) (4 5)))
        (list '(6 (4 5))))
  
  (test (apply-reduction-relation
         (reduction-relation 
          grammar
          (==> (number_1 number_2)
               ,(* (term number_1) (term number_2)))
          where
          [(~~> a b) (--> (M_1 a) (M_1 b))]
          [(==> a b) (~~> (M_1 a) (M_1 b))])
         '((1 2) ((2 3) (4 5))))
        (list '((1 2) ((2 3) 20))))
  
  (test (apply-reduction-relation
         (reduction-relation 
          grammar
          (~~> (number_1 number_2)
               ,(* (term number_1) (term number_2)))
          (==> (number_1 number_2)
               ,(* (term number_1) (term number_2)))
          where
          [(~~> a b) (--> (M_1 a) (M_1 b))]
          [(==> a b) (--> (a M_1) (b M_1))])
         '((2 3) (4 5)))
        (list '(6 (4 5))
              '((2 3) 20)))
  
  (test (apply-reduction-relation
         (reduction-relation 
          grammar
          (--> (M_1 (number_1 number_2))
               (M_1 ,(* (term number_1) (term number_2))))
          (==> (number_1 number_2)
               ,(* (term number_1) (term number_2)))
          where
          [(==> a b) (--> (a M_1) (b M_1))])
         '((2 3) (4 5)))
        (list '((2 3) 20)
              '(6 (4 5))))
  
  (test (apply-reduction-relation/tag-with-names
         (reduction-relation 
          grammar
          (--> (number_1 number_2) 
               ,(* (term number_1) (term number_2))
               mul))
         '(4 5))
        (list (list "mul" 20)))
  
  (test (apply-reduction-relation/tag-with-names
         (reduction-relation 
          grammar
          (--> (number_1 number_2) 
               ,(* (term number_1) (term number_2))
               "mul"))
         '(4 5))
        (list (list "mul" 20)))
  
  (test (apply-reduction-relation/tag-with-names
         (reduction-relation 
          grammar
          (--> (number_1 number_2) 
               ,(* (term number_1) (term number_2))))
         '(4 5))
        (list (list #f 20)))
  
  (test (apply-reduction-relation/tag-with-names
         (reduction-relation 
          grammar
          (==> (number_1 number_2) 
               ,(* (term number_1) (term number_2))
               mult)
          where
          [(==> a b) (--> (M_1 a) (M_1 b))])
         '((2 3) (4 5)))
        (list (list "mult" '((2 3) 20))))

  (test (let ([x 0])
          (reduction-relation
           (begin (set! x (+ x 1))
                  (language))
           (--> 0 1)
           (--> 1 2)
           (==> 2 3)
           (==> 3 4)
           where
           [(==> a b) (--> a b)])
          x)
        1)
  
  (test (let ([lang (language)])
          (apply-reduction-relation
           (union-reduction-relations
            (reduction-relation lang
                                (--> x a)
                                (--> x b))
            (reduction-relation lang
                                (--> x c)
                                (--> x d)))
           'x))
        (list 'a 'b 'c 'd))
  
  (test (apply-reduction-relation
         (reduction-relation 
          (language)
          (--> (number_1 number_2) 
               number_2
               (side-condition (< (term number_1) (term number_2))))
          (--> (number_1 number_2) 
               number_1
               (side-condition (< (term number_2) (term number_1)))))
         '(1 2))
        (list 2))
  
  (parameterize ([current-namespace syn-err-test-namespace])
    (eval `(define grammar ,grammar)))
  
  (test-syn-err (reduction-relation 
                 grammar
                 (~~> (number_1 number_2)
                      ,(* (term number_1) (term number_2)))
                 where
                 [(~~> a b) (--> (M a) (M b))]
                 [(==> a b) (~~> (M a) (M b))])
                #rx"no rules")
  
  (test-syn-err (reduction-relation 
                 grammar
                 (~~> (number_1 number_2)
                      ,(* (term number_1) (term number_2))))
                #rx"no --> rules")
  
  (test-syn-err (reduction-relation 
                 grammar
                 (--> (number_1 number_2) 
                      ,(* (term number_1) (term number_2))
                      mult)
                 (--> (number_1 number_2) 
                      ,(* (term number_1) (term number_2))
                      mult))
                #rx"same name on multiple rules")
  
  (test-syn-err (reduction-relation 
                 grammar
                 (--> 1 2)
                 (==> 3 4))
                #rx"not defined.*==>")
  
  (test-syn-err  (reduction-relation 
                  (language)
                  (--> 1 2)
                  (==> 3 4)
                  where
                  [(==> a b) (~> a b)])
                 #rx"not defined.*~>")
  
  (test-syn-err (language (e name)) #rx"name")
  (test-syn-err (language (name x)) #rx"name")
  (test-syn-err (language (x_y x)) #rx"x_y")
  
  ;; expect union with duplicate names to fail
  (test (with-handlers ((exn? (λ (x) 'passed)))
          (union-reduction-relations
           (reduction-relation 
            grammar
            (--> (number_1 number_2) 
                 ,(* (term number_1) (term number_2))
                 mult))
           (reduction-relation 
            grammar
            (--> (number_1 number_2) 
                 ,(* (term number_1) (term number_2))
                 mult)))
          'failed)
        'passed)
  
  (test (with-handlers ((exn? (λ (x) 'passed)))
          (union-reduction-relations
           (union-reduction-relations
            (reduction-relation 
             grammar
             (--> (number_1 number_2) 
                  ,(* (term number_1) (term number_2))
                  mult))
            (reduction-relation 
             grammar
             (--> (number_1 number_2) 
                  ,(* (term number_1) (term number_2))
                  mult3)))
           
           (union-reduction-relations
            (reduction-relation 
             grammar
             (--> (number_1 number_2) 
                  ,(* (term number_1) (term number_2))
                  mult))
            (reduction-relation 
             grammar
             (--> (number_1 number_2) 
                  ,(* (term number_1) (term number_2))
                  mult2))))
          'passed)
        'passed)
  
  (test (apply-reduction-relation
         (compatible-closure 
          (reduction-relation 
           grammar
           (--> (number_1 number_2) 
                ,(* (term number_1) (term number_2))
                mult))
          grammar
          M)
         '((2 3) (4 5)))
        (list '((2 3) 20)
              '(6 (4 5))))
  
  (test (apply-reduction-relation
         (compatible-closure 
          (reduction-relation 
           grammar
           (--> (number_1 number_2) 
                ,(* (term number_1) (term number_2))
                mult))
          grammar
          M)
         '(4 2))
        (list '8))
  
  (test (apply-reduction-relation
         (context-closure 
          (context-closure 
           (reduction-relation grammar (--> 1 2))
           grammar
           (y hole))
          grammar
          (x hole))
         '(x (y 1)))
        (list '(x (y 2))))

  (test (apply-reduction-relation
         (reduction-relation 
          grammar
          (--> (variable_1 variable_2) 
               (variable_1 variable_2 x)
               mul
               (fresh x)))
         '(x x1))
        (list '(x x1 x2)))
  
  (test (apply-reduction-relation
         (reduction-relation 
          grammar
          (~~> number 
               x
               (fresh x))
          where 
          [(~~> a b) (--> (variable_1 variable_2 a) (variable_1 variable_2 b))])
         '(x x1 2))
        (list '(x x1 x2)))
  
  (test (apply-reduction-relation
         (reduction-relation 
          (language (x variable))
          (--> (x_1 ...)
               (x ...)
               (fresh ((x ...) (x_1 ...)))))
         '(x y x1))
        (list '(x2 x3 x4)))

  (test (apply-reduction-relation
         (reduction-relation
          (language)
          (--> (variable_1 ...)
               (x ... variable_1 ...)
               (fresh ((x ...) (variable_1 ...) (variable_1 ...)))))
         '(x y z))
        (list '(x1 y1 z1 x y z)))
  
  (test (apply-reduction-relation
         (reduction-relation
          (language)
          (--> variable_1
               (x variable_1)
               (fresh (x variable_1))))
         'q)
        (list '(q1 q)))
  
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;; examples from doc.txt
  ;;
  
  (define lc-lang
    (language (e (e e ...)
                 x
                 v)
              (c (v ... c e ...)
                 hole)
              (v (lambda (x ...) e))
              (x variable-not-otherwise-mentioned)))
  
  (test (let ([m (test-match lc-lang e (term (lambda (x) x)))])
          (and m (length m)))
        1)
  
  (test (test-match (extend-language lc-lang 
                                     (q a b c))
                    e
                    (term (lambda (a) a)))
        #f)
  
  (test (let ([m (test-match (extend-language lc-lang 
                                              (q a b c))
                             e
                             (term (lambda (z) z)))])
          (and m (length m)))
        1)
  
  (require (lib "list.ss"))
  ;; free-vars : e -> (listof x)
  (define-metafunction free-vars
    lc-lang
    [(e_1 e_2 ...) 
     ,(apply append (term ((free-vars e_1) (free-vars e_2) ...)))]
    [x_1 ,(list (term x_1))]
    [(lambda (x_1 ...) e_1)
     ,(foldr remq (term (free-vars e_1)) (term (x_1 ...)))])
  
  (test (term (free-vars (lambda (x) (x y))))
        (list 'y))

  (test (variable-not-in (term (x y z)) 'x)
        (term x1))
  
  (test (variable-not-in (term (y z)) 'x)
        (term x))
  (test (variable-not-in (term (x x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) 'x)
        (term x11))
  (test (variable-not-in (term (x x11)) 'x)
        (term x12))
  (test (variable-not-in (term (x x1 x2 x3)) 'x1)
        (term x4))
  
  (test (variables-not-in (term (x y z)) '(x))
        '(x1))
  (test (variables-not-in (term (x2 y z)) '(x x x))
        '(x x3 x4))
  
  (test ((term-match/single (language)
                            [(variable_x variable_y)
                             (cons (term variable_x)
                                   (term variable_y))])
         '(x y))
        '(x . y))
  
  (test ((term-match/single (language)
                            [(side-condition (variable_x variable_y)
                                             (eq? (term variable_x) 'x))
                             (cons (term variable_x)
                                   (term variable_y))])
         '(x y))
        '(x . y))
  (test ((term-match/single (language [x 1])
                            [(x x)
                             1])
         '(1 1))
        1)
  
  (test (let ([x 0])
          (cons ((term-match (language)
                             [(any ... number_1 any ...)
                              (begin (set! x (+ x 1))
                                     (term number_1))])
                 '(1 2 3))
                x))
        '((3 2 1) . 3))
  
  (test ((term-match (language)
                     [number_1
                      (term number_1)]
                     [number_1
                      (term number_1)])
         '1)
        '(1 1))
  
  (test (apply-reduction-relation
         (reduction-relation
          (language (sym variable))
          (--> (sym_one sym_!_one sym_!_one sym_!_one)
               (sym_one sym_!_one)))
         (term (a a b c)))
        (list (term (a sym_!_one))))

  
  (printf "tl-test.ss: all ~a tests passed.\n" tests))