(module language-composer-tools mzscheme
  
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2))
           (planet "gui.ss" ("robby" "redex.plt" 2))
           (lib "match.ss"))
  
  (provide define-pre-grammar
           grammar-union
           define-type-judgements
           type-system-union
           empty-set
           lookup
           extend
           get-evaluators)
  
  ;; ============================================================
  ;; PLUMBING
  ;; Utilities for stitching together different language slices
  ;; into a single language
  
  ;; (define-pre-grammar id (id rhs ...) ...) -> void                    SYNTAX
  ;; Binds id to a syntax object representing a "pre-language," i.e. a set of
  ;; nonterminals that can be fused with others to form a complete language.
  ;; This makes id a valid argument to language-union, below
  (define-syntax (define-pre-grammar stx)
    (syntax-case stx ()
      [(_ name (nt rhs ...) ...)
       (identifier? #'name)
       (syntax/loc stx 
         (define-syntax name (list (syntax (nt (... rhs) ...)) ...)))]))
  
  ;; (language-union pre-grammar-identifier ...) -> language              SYNTAX
  ;; unites an arbitrary number of pre-languages to form a single overall language
  (define-syntax (grammar-union stx)
    (syntax-case stx ()
      [(_ prelang ...)
       (let ([syntaxes (map syntax-local-value (syntax-e #'(prelang ...)))]
             [nonterms-to-clauses (make-hash-table 'equal)])
         (for-each
          (λ (clause)
            (syntax-case clause (replace)
              [((replace id) rhs ...)
               (hash-table-put! nonterms-to-clauses (syntax-e #'id) (syntax-e #'((... rhs) ...)))]
              [(id rhs ...)
               (identifier? #'id)
               (hash-table-put! nonterms-to-clauses (syntax-e #'id)
                                (append 
                                 (syntax-e #'((... rhs) ...)) 
                                 (hash-table-get nonterms-to-clauses (syntax-e #'id) (λ () '()))))]))
          (apply append syntaxes))
         (with-syntax ([((id rhs ...) ...) (hash-table-map 
                                            nonterms-to-clauses
                                            (λ (name rhses)
                                              (datum->syntax-object 
                                               stx
                                               `(,name ,@rhses))))])
             (syntax/loc stx (language (id rhs ...) ...))))]))
  
  (define-syntax define-type-judgements
    (syntax-rules ()
      [(define-type-judgements judgement-set-name (judgement-name Γ  judgement ...) ...)
       (define judgement-set-name
         (list
          (lambda (judgement-name ...)
            (lambda (t Γ)
              (match t
                judgement ...
                [_ #f]))) ...))]))
  
  ;; pivot ::= m, n > 0 => (list[n] (list[m] X)) -> (list[m] (list[n] X))
  (define (pivot ls) (apply map list ls))
  
  (define all-same?
    (case-lambda
      [() #t]
      [(a) #t]
      [as (apply = as)]))
  
  ;; JS[n]            ::= (list[n] PRE-JUDGEMENT[n])
  ;; PRE-JUDGEMENT[n] ::= JUDGEMENT_1 ... JUDGEMENT_n -> JUDGEMENT
  ;; JUDGEMENT        ::= expr env -> type option
  (define (type-system-union . jss)
    (unless (apply all-same? (map length jss))
      (error 'type-system-union "all judgement-sets must have the same number of judgements"))
    (let* ([groups (pivot jss)])
      (letrec ([judgerses (map (λ (group) 
                            (map (λ (pre-j) 
                                   (λ (t gamma) ((apply pre-j judgement-fns) t gamma)))
                                 group)) groups)]
               [judgement-fns
                (map 
                 (λ (judgers) (λ (t gamma)
                                (let loop ((judgers judgers))
                                  (cond
                                    [(null? judgers) #f]
                                    [((car judgers) t gamma) => (λ (x) x)]
                                    [else (loop (cdr judgers))]))))
                 judgerses)])
        (apply values judgement-fns))))
  
  ;; ----------------------------------------
  ;; environment management
  
  (define empty-set '())
  (define (lookup x Γ)
    (let ((ans (assq x Γ)))
      (unless ans
        (error 'lookup "Variable not in environment: ~a" x))
      (cadr ans)))
  (define (extend Γ x v)
    (cons (list x v) Γ))  
  
  
  (define (get-evaluators grammar typeof reductions error-message?)
    
    (define (run p)
      (let* ([initial-type (typeof p empty-set)]
             [initial-term (if initial-type p "Type error")])
        (traces/pred grammar 
                     reductions
                     (list initial-term)
                     (λ (x) 
                       (or (equal? (typeof x empty-set) initial-type)
                           (error-message? x))))))
  
    (define (evaluate p)
      (if (typeof p empty-set)
          (normalize p)
          "Type error"))
    
    (define normalize (λ (p) (normalize* p void)))
    (define normalize/tell (λ (p) (normalize* p (λ (x) (write x) (newline)))))
    (define (normalize* p observer)
      (let loop ((p p))
        (observer p)
        (let ((nexts (reduce reductions p)))
          (cond
            [(null? nexts) p]
            [(null? (cdr nexts))
             (loop (car nexts))]
            [else
             (error 'normalize "Term ~s reduces multiple ways" p)]))))
    
    (values run evaluate normalize normalize/tell)))