typed-refs.rkt

#lang plait

; State-passing language

; Language has: let bindings, variables, numbers, box and set!
(define-type AtomicExp
  (varE (id : Symbol))
  (boolE (b : Boolean))
  (numE (n : Number))
  (addE (l : AtomicExp) (r : AtomicExp))
  (andE (l : AtomicExp) (r : AtomicExp)))

(define-type Exp
  (let1E (id : Symbol) (assignment : Exp) (body : Exp))
  (atom (a : AtomicExp))
  (unboxE (e : AtomicExp))
  (boxE (e : AtomicExp))
  (setE (b : AtomicExp) (v : AtomicExp)))

(define-type-alias Heap (Number * (Hashof Number Value)))
(define-type-alias Store (Hashof Symbol Value))
(define mt-env (hash '()))

(define-type Value
  [numV (n : Number)]
  [boolV (b : Boolean)]
  [locV (l : Number)])

(define (lookup-store (s : Symbol) (n : Store))
  (type-case (Optionof Value) (hash-ref n s)
             [(none) (error s "not bound")]
             [(some v) v]))

(test (lookup-store 's (hash (list (pair 's (numV 10))))) (numV 10))
(test (lookup-store 's (hash (list (pair 's (locV 10))))) (locV 10))
(test/exn (lookup-store 'n (hash (list (pair 's (numV 10))))) "not bound")

; it is important to note that extend-store will overwrite if there are
; overlapping symbols.
(extend-store : (Store Symbol Value -> Store))
(define (extend-store old-store new-name value)
  (hash-set old-store new-name value))

(test (extend-store mt-env 's (numV 10)) (hash (list (pair 's (numV 10)))))
(test (extend-store (hash (list (pair 's (numV 20)))) 's (numV 10)) 
      (hash (list (pair 's (numV 10)))))

(define mt-heap (pair 0 (hash '())))

(define (lookup-heap (l : Number) (h : Heap))
  (type-case (Optionof Value) (hash-ref (snd h) l)
             [(none) (error 'runtime "invalid location")]
             [(some v) v]))

(test (lookup-heap 0 (pair 1 (hash (list (pair 0 (numV 10)))))) (numV 10))
(test (lookup-heap 0 (pair 1 (hash (list (pair 0 (locV 10)))))) (locV 10))
(test/exn (lookup-heap 23 (pair 1 (hash (list (pair 0 (locV 10))))))
  "invalid location")

(extend-heap : (Heap Value -> (Number * Heap)))
(define (extend-heap h value)
  (letrec [(cur-loc (fst h))
        (cur-heap (snd h))
        (new-heap (hash-set cur-heap cur-loc value))]
    (pair cur-loc (pair (+ 1 cur-loc) new-heap))))

(test (extend-heap (pair 1 (hash (list (pair 0 (numV 10))))) (locV 20))
  (pair 1 (pair 2 (hash (list (pair 0 (numV 10)) (pair 1 (locV 20)))))))

(set-heap : (Heap Number Value -> Heap))
(define (set-heap h loc value)
  (pair (fst h) (hash-set (snd h) loc value)))

(test (set-heap (pair 1 (hash (list (pair 0 (numV 10)))))  5 (locV 20))
  (pair 1 (hash (list (pair 0 (numV 10)) (pair 5 (locV 20))))))

(interp-atomic : (AtomicExp Store Heap -> Value))
(define (interp-atomic e store heap)
  (type-case AtomicExp e
             [(numE n) (numV n)]
             [(varE id) (lookup-store id store)]
             [(boolE b) (boolV b)]
             [(addE l r) (numV (+ (numV-n (interp-atomic l store heap))
                                  (numV-n (interp-atomic r store heap))))]
             [(andE l r) (boolV (and (boolV-b (interp-atomic l store heap))
                                     (boolV-b (interp-atomic r store heap))))]
             ))

; the store will store local variables (e.g. ones in let-binds)
; the heap will store boxed variables
(interp : (Exp Store Heap -> (Value * Heap)))
(define (interp e store heap)
  (type-case Exp e
             [(atom a) (pair (interp-atomic a store heap) heap)]
             [(let1E id assignment body)
              (letrec [(eval-assgn (interp assignment store heap))
                       (assgn-value (fst eval-assgn))
                       (assgn-heap (snd eval-assgn))
                       (new-store (extend-store store id assgn-value))]
                (interp body new-store assgn-heap))]
             [(boxE e)
              (letrec [(eval-e (interp-atomic e store heap))
                       (heap-insertion (extend-heap heap eval-e))]
                (pair (locV (fst heap-insertion)) (snd heap-insertion)))]
             [(unboxE body)
              (letrec [(eval-body (interp-atomic body store heap))]
                (type-case Value eval-body
                           [(locV l) (pair (lookup-heap l heap) heap)]
                           [else (error 'runtime "tried to unbox non-location")]))]
             [(setE body arg)
              (letrec [(eval-body (interp-atomic body store heap))
                       (eval-arg (interp-atomic arg store heap))]
                (type-case Value eval-body
                           [(locV l) (pair (numV 0) (set-heap heap l eval-arg))]
                           [else (error 'runtime "tried to set non-location")]))]))

; let x = box 0 in unbox x
(test (interp (let1E 'x (boxE (numE 0)) (unboxE (varE 'x))) mt-env mt-heap)
      (values (numV 0) (values 1 (hash (list (pair 0 (numV 0)))))))

; let x = box 0 in let y = set! x 10 in unbox x
(test
 (interp (let1E 'x (boxE (numE 0))
 (let1E 'y (setE (varE 'x) (numE 10))
        (unboxE (varE 'x)))) mt-env mt-heap)
  (values (numV 10) (values 1 (hash (list (pair 0 (numV 10)))))) )

; let x = box 0 in let y = box 1 in unbox x
(test (interp
  (let1E 'x (boxE (numE 0))
  (let1E 'y (boxE (numE 1))
  (unboxE (varE 'x)))) mt-env mt-heap)
  (values (numV 0) (values 2 (hash (list (pair 0 (numV 0)) (pair 1 (numV 1)))))))

; let x = box 0 in let y = box 1 in let z = set! y 10 in unbox x
(test (interp
  (let1E 'x (boxE (numE 0))
  (let1E 'y (boxE (numE 1))
  (let1E 'z (setE (varE 'y) (numE 10))
  (unboxE (varE 'x))))) mt-env mt-heap)
  (values (numV 0) (values 2 (hash (list (pair 0 (numV 0)) (pair 1 (numV 10)))))))

; let x = box 0 in let x = box 10 in unbox x
(test (interp
  (let1E 'x (boxE (numE 0))
  (let1E 'x (boxE (numE 10))
  (unboxE (varE 'x)))) mt-env mt-heap)
  (values (numV 10) (values 2 (hash (list (pair 0 (numV 0)) (pair 1 (numV 10)))))))

(define-type Type
  [TNum]
  [TBool]
  [TRef (t : Type)])

(define-type-alias TypeEnv (Hashof Symbol Type))
(define (extend-tenv old new-name type)
  (hash-set old new-name type))

(define (lookup-tenv (env : TypeEnv) (x : Symbol))
  (type-case (Optionof Type) (hash-ref env x)
             [(none) (error 'runtime "invalid location")]
             [(some v) v]))

(define (atomic-type-of env e)
  (type-case AtomicExp e
             [(varE s) (lookup-tenv env s)]
             [(boolE v) (TBool)]
             [(numE n) (TNum)]
             [(andE l r)
              (if (and (TBool? (atomic-type-of env l))
                       (TBool? (atomic-type-of env r)))
                  (TBool)
                  (error 'type "Invalid types for and"))]
             [(addE l r)
              (if (and (TNum? (atomic-type-of env l))
                       (TNum? (atomic-type-of env r)))
                  (TNum)
                  (error 'type "Invalid types for add"))]))


(type-of : (TypeEnv Exp -> Type))
(define (type-of env e)
  (type-case Exp e
             [(let1E id assgn body)
              (type-of (extend-tenv env id (type-of env assgn)) body)]
             [(atom a) (atomic-type-of env a)]
             [(unboxE e)
              (type-case Type (atomic-type-of env e)
                         [(TRef t) t]
                         [else (error 'type "Attempting to dereference non-location")])]
             [(boxE e) (TRef (atomic-type-of env e))]
             [(setE l v)
              (type-case Type (atomic-type-of env l)
                         [(TRef t) (if (equal? (atomic-type-of env v) t)
                                       (TNum)
                                       (error 'type "Attempting to change type of ref"))]
                         [else (error 'type "Attempting to set non-location")])]))