;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;;  ClassicJava: an implementation of the ClassicJava programming language
;;  utils.ss: general utilities used in the ClassicJava implementation.
;;  Copyright (C) 2005  Richard Cobbe
;;
;;  This library is free software; you can redistribute it and/or modify it
;;  under the terms of the GNU Lesser General Public License as published by
;;  the Free Software Foundation; either version 2.1 of the License, or (at
;;  your option) any later version.
;;
;;  This library is distributed in the hope that it will be useful, but WITHOUT
;;  ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
;;  FITNESS FOR A PARTICULAR PURPOSE.  See the GNU Lesser General Public
;;  License for more details.
;;
;;  You should have received a copy of the GNU Lesser General Public License
;;  along with this library; if not, write to the Free Software Foundation,
;;  Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(module utils mzscheme

  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 1 0))
           (lib "contract.ss"))

  (provide/contract [small-step             (-> (listof red?) any/c any)]
                    [big-step               (-> (listof red?) any/c any)]
                    [small-step-sequence    (-> (listof red?) any/c list?)])

  ;; small-step :: (Listof Reduction) Term -> (Union #f Term)
  ;; reduces term a single step; returns #f if no reduction possible.
  ;; signals error if multiple reductions possible.
  (define small-step
    (lambda (reductions term)
      (let ([results (reduce reductions term)])
        (cond
          [(null? results) #f]
          [(null? (cdr results)) (car results)]
          [else (error 'small-step
                       "reduction from ~a not unique: ~a" term results)]))))

  ;; big-step :: (Listof Reduction) Term -> Term
  ;; reduces term as many steps as possible and returns final result.
  ;; If at any point, multiple reductions are possible, signals an error.
  (define big-step
    (lambda (reductions term)
      (let loop ([term term])
        (cond
          [(small-step reductions term) => loop]
          [else term]))))

  ;; small-step-sequence :: (Listof Reduction) Term -> (Listof Term)
  ;; like big-step, but returns a list containing all intermediate results.
  (define small-step-sequence
    (lambda (reductions term)
      (let loop ([term term])
        (let ([next (small-step reductions term)])
          (if next
              (cons term (loop next))
              (list term))))))

  ;; mv-map :: (a -> b c) (Listof a) -> (Listof b) (Listof c)
  ;; map, but for functions that return 2 values.
  (define mv-map
    (lambda (f l)
      (if (null? l)
          (values null null)
          (let-values ([(bs cs) (mv-map f (cdr l))]
                       [(b c) (f (car l))])
            (values (cons b bs) (cons c cs))))))

  (provide mv-map))