<commit_before>#lang racket

(require "SL-syntax.rkt" "SL-semantics.rkt"
         "TL-syntax.rkt" "TL-semantics.rkt"
         "CMT.rkt"
         "common.rkt"
         redex)
(provide main same-result?)

(define (main . args)
  (define seed (add1 (random (sub1 (expt 2 31)))))
  (define unique-decomp-tests #f)
  (define CMT-range-all-tests #f)
  (define CMT-range-rules-tests #f)
  (define same-result-all-tests #f)
  (define same-result-rules-tests #f)
  
  (command-line
   #:argv args
   #:once-each
   ["--seed"
    n
    "Seed PRG with n"
    (set! seed (string->number n))]
   ["--unique-decomposition"
    n
    "Test unique decomposition of n expressions"
    (set! unique-decomp-tests (string->number n))]
   ["--CMT-range"
    n
    ("Test that CMT produces a TL expression for n expressions,"
     "chosen from SL's e non-terminal")
    (set! CMT-range-all-tests (string->number n))]
   ["--CMT-range-rules"
    n
    ("Test that CMT produces a TL expression for n expressions,"
     "chosen from the left-hand sides of -->SL")
    (set! CMT-range-rules-tests (string->number n))]
   ["--same-result"
    n
    ("Test that translation preserves meaning for n expression,"
     "chosen from SL's e non-terminal")
    (set! same-result-all-tests (string->number n))]
   ["--same-result-rules"
    n
    ("Test that translation preserves meaning for n expression,"
     "chosen from SL's e non-terminal")
    (set! same-result-rules-tests (string->number n))])
  
  (printf "Random seed: ~s\n" seed)
  
  (when unique-decomp-tests
    (test-unique-decomposition unique-decomp-tests))
  (when CMT-range-all-tests
    (test-CMT-range CMT-range-all-tests))
  (when CMT-range-rules-tests
    (test-CMT-range/rules CMT-range-rules-tests))
  (when same-result-all-tests
    (test-same-result same-result-all-tests))
  (when same-result-rules-tests
    (test-same-result/rules same-result-rules-tests)))

;; Unique decomposition
(define (test-unique-decomposition attempts)
  (redex-check SL e (uniquely-decomposes? (term e)) #:attempts attempts))

(define uniquely-decomposes?
  (let ([a? (redex-match SL a)]
        [decompositions (redex-match SL (in-hole T r))])
    (λ (e)
      (or (a? e)
          (match (decompositions e)
            [(list _) #t]
            [_ #f])))))

;; CMT produces TL expressions
(define (test-CMT-range attempts)
  (test-translation CMT-produces-TL?
                    #:attempts attempts))

(define (test-CMT-range/rules attempts)
  (test-translation CMT-produces-TL? 
                    #:attempts attempts 
                    #:source -->SL/no-side-conds))

(define CMT-produces-TL?
  (let ([TL-e? (redex-match TL e)])
    (λ (e) 
      (TL-e? (term (CMT ,e))))))

;; Translated programs have the same result
(define (test-same-result attempts)
  (test-translation same-result? 
                    #:attempts attempts))

(define (test-same-result/rules attempts)
  (test-translation same-result?
                    #:attempts attempts
                    #:source -->SL/no-side-conds))

(define (same-result? expr)
  (let/ec return
    (define SL-result
      (with-handlers ([normalization-timeout? return]
                      [eval-undefined? return])
        (parameterize ([max-normalization-steps 1000])
          (SL-eval (term (∅ / ,expr))))))
    (define TL-result
      (TL-eval (term (∅ / (translate ,expr)))))
    (or (equal? SL-result TL-result)
        (compares-incomparable-keys? expr))))

(define SL-eval
  (make-eval -->SL (redex-match SL v)))
(define TL-eval
  (make-eval -->TL (redex-match TL v)))

;; Utilities
(define-syntax-rule (test-translation predicate . kw-args)
  (redex-check SL-gen (Σ / e) 
               (predicate (term e))
               #:prepare close-program . kw-args))

(define-extended-language SL-gen SL
  (σ (ref (variable-except resume restore-marks c-w-i-c-m map-set kont/ms equal? last)))
  (K (side-condition string_1 (not (member (term string_1) '("square" "diamond")))))
  
  (K-tree (K K-tree ...)))

(define -->SL/no-side-conds
  ; Disables side-conditions on some rules.
  (extend-reduction-relation
   -->SL SL
   (--> (Σ / (in-hole E (match (K v ...) l ...))) any "2")
   (--> (Σ / (in-hole E (σ v ...))) any "4")<commit_msg>Reduces the memory used by the randomized tests<commit_after>#lang racket

(require "SL-syntax.rkt" "SL-semantics.rkt"
         "TL-syntax.rkt" "TL-semantics.rkt"
         "CMT.rkt"
         "common.rkt"
         redex)
(provide main same-result?)

(define (main . args)
  (define seed (add1 (random (sub1 (expt 2 31)))))
  (define unique-decomp-tests #f)
  (define CMT-range-all-tests #f)
  (define CMT-range-rules-tests #f)
  (define same-result-all-tests #f)
  (define same-result-rules-tests #f)
  
  (command-line
   #:argv args
   #:once-each
   ["--seed"
    n
    "Seed PRG with n"
    (set! seed (string->number n))]
   ["--unique-decomposition"
    n
    "Test unique decomposition of n expressions"
    (set! unique-decomp-tests (string->number n))]
   ["--CMT-range"
    n
    ("Test that CMT produces a TL expression for n expressions,"
     "chosen from SL's e non-terminal")
    (set! CMT-range-all-tests (string->number n))]
   ["--CMT-range-rules"
    n
    ("Test that CMT produces a TL expression for n expressions,"
     "chosen from the left-hand sides of -->SL")
    (set! CMT-range-rules-tests (string->number n))]
   ["--same-result"
    n
    ("Test that translation preserves meaning for n expression,"
     "chosen from SL's e non-terminal")
    (set! same-result-all-tests (string->number n))]
   ["--same-result-rules"
    n
    ("Test that translation preserves meaning for n expression,"
     "chosen from SL's e non-terminal")
    (set! same-result-rules-tests (string->number n))])
  
  (printf "Random seed: ~s\n" seed)
  
  (when unique-decomp-tests
    (test-unique-decomposition unique-decomp-tests))
  (when CMT-range-all-tests
    (test-CMT-range CMT-range-all-tests))
  (when CMT-range-rules-tests
    (test-CMT-range/rules CMT-range-rules-tests))
  (when same-result-all-tests
    (test-same-result same-result-all-tests))
  (when same-result-rules-tests
    (test-same-result/rules same-result-rules-tests)))

;; Unique decomposition
(define (test-unique-decomposition attempts)
  (redex-check SL e (uniquely-decomposes? (term e)) #:attempts attempts))

(define uniquely-decomposes?
  (let ([a? (redex-match SL a)]
        [decompositions (redex-match SL (in-hole T r))])
    (λ (e)
      (or (a? e)
          (match (decompositions e)
            [(list _) #t]
            [_ #f])))))

;; CMT produces TL expressions
(define (test-CMT-range attempts)
  (test-translation CMT-produces-TL?
                    #:attempts attempts))

(define (test-CMT-range/rules attempts)
  (test-translation CMT-produces-TL? 
                    #:attempts attempts 
                    #:source -->SL/no-side-conds))

(define CMT-produces-TL?
  (let ([TL-e? (redex-match TL e)])
    (λ (e) 
      (TL-e? (term (CMT ,e))))))

;; Translated programs have the same result
(define (test-same-result attempts)
  (test-translation same-result? 
                    #:attempts attempts))

(define (test-same-result/rules attempts)
  (test-translation same-result?
                    #:attempts attempts
                    #:source -->SL/no-side-conds))

(define (same-result? expr)
  (let/ec return
    (define SL-result
      (with-handlers ([normalization-timeout? return]
                      [eval-undefined? return])
        (parameterize ([max-normalization-steps 1000])
          (SL-eval (term (∅ / ,expr))))))
    (define TL-result
      (dynamic-wind
       (λ () (set-cache-size! 100))
       (λ () (TL-eval (term (∅ / (translate ,expr)))))
       (λ () (set-cache-size! 350))))
    (or (equal? SL-result TL-result)
        (compares-incomparable-keys? expr))))

(define SL-eval
  (make-eval -->SL (redex-match SL v)))
(define TL-eval
  (make-eval -->TL (redex-match TL v)))

;; Utilities
(define-syntax-rule (test-translation predicate . kw-args)
  (redex-check SL-gen (Σ / e) 
               (predicate (term e))
               #:prepare close-program . kw-args))

(define-extended-language SL-gen SL
  (σ (ref (variable-except resume restore-marks c-w-i-c-m map-set kont/ms equal? last)))
  (K (side-condition string_1 (not (member (term string_1) '("square" "diamond")))))
  
  (K-tree (K K-tree ...)))

(define -->SL/no-side-conds
  ; Disables side-conditions on some rules.
  (extend-reduction-relation
   -->SL SL
   (--> (Σ / (in-hole E (match (K v ...) l ...))) any "2")
   (--> (Σ / (in-hole E (σ v ...))) any "4")
{'fraction_non_alphanumeric': 0.1623353921454376, 'fraction_numerical': 0.0037291690945111295, 'mean_word_length': 2.5389690721649485, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 33, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2768600', 'n_tokens_mistral': 3066, 'n_tokens_neox': 2924, 'n_words': 766}