SHoltzen

#lang plait
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; an implementation of mark-and-sweep garbage collection for the CESK machine

(define-type SafeRefLang
  (letE [id : Symbol]
        [e1 : SafeRefLang]
        [e2 : SafeRefLang])
  (identE [id : Symbol])
  (addE [e1 : SafeRefLang] [e2 : SafeRefLang])

SHoltzen

#lang plait
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; an implementation of the CEK machine

(define-type SafeRefLang
  (letE [id : Symbol]
        [e1 : SafeRefLang]
        [e2 : SafeRefLang])
  (identE [id : Symbol])
  (addE [e1 : SafeRefLang] [e2 : SafeRefLang])

SHoltzen

#lang plait
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; an implementation of the CESK machine for a memory unsafe language with
;;; references

(define-type RefLang
  (letE [id : Symbol]
        [e1 : RefLang]
        [e2 : RefLang])
  (identE [id : Symbol])

SHoltzen

#lang plait
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; an implementation of the CEK machine for the untyped call-by-value lambda
;;; calculus

(define-type Lam
  (lamE [id : Symbol] [body : Lam])
  (appE [e1 : Lam] [e2 : Lam])
  (identE [id : Symbol])
  (valueE [v : Value]))

SHoltzen

#lang plait
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; an implementation of the CEK machine

(define-type Calc
  (addE [e1 : Calc] [e2 : Calc])
  (letE [id : Symbol]
        [e1 : Calc]
        [e2 : Calc])
  (identE [id : Symbol])

SHoltzen

#lang plait
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; an implementation of the CK machine

(define-type Calc
  (addE [e1 : Calc] [e2 : Calc])
  (numE [n : Number]))

(define-type Frame
  ;;; frame for (+ n e)

SHoltzen

import Lean
import Lean.Elab.Term
import Mathlib.Data.Finset.Basic
import Mathlib.Logic.ExistsUnique

-- class SmallCategory (ob : Type u) : Type (max u (v+1)) where
class SmallCategory (ob : Type) : Type 1 where
  hom : ob → ob → Type
  id : ∀ x, hom x x
  comp : ∀ {X Y Z}, hom X Y → hom Y Z → hom X Z

SHoltzen

#lang plait

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; starter code: do not modify
(define store-size 50)
(define empty-env (hash empty))

(define-type PairLang
  (letE [id : Symbol]
        [e1 : PairLang]

SHoltzen

#lang plait

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; starter code: do not modify
(define-type IfLang
  (boolE [b : Boolean])
  (ifE [g : IfLang] [thn : IfLang] [els : IfLang])
  (tryE [e : IfLang] [handle-id : Symbol] [handler : IfLang])
  (raiseE [id : Symbol]))

SHoltzen

#lang plait

(define-type ResExn
  (numE [n : Number])
  (addE [e1 : ResExn] [e2 : ResExn])
  (identE [id : Symbol])
  (appE [e1 : ResExn] [e2 : ResExn])
  (lamE [arg : Symbol] [body : ResExn])
  (tryE [body : ResExn] [handler : ResExn])
  (resumeE [n : Number])