kmicinski

#lang racket

;; CIS700, Fall 2023 -- Kris Micinski
;; 
;; Demo of SMT (SMTLIB) to perform bounded-model checking for an example
;; program.
;; 
;;  // input x, a bit vector of length N
;;  i = 0;
;;  r = 0;

kmicinski

;; CIS352 -- Fall 2023
;; Closure-Creating Interpreters
#lang racket

(define (expr? e)
  (match e
    [(? symbol? x) #t] ;; variables
    [(? number? n) #t]
    ;; single-variable let binding
    [`(let ([,(? symbol? x) ,(? expr? e-let-binding)]) ,(? expr? e-body)) #t]

kmicinski

#lang racket

;; CIS352 Office hours code -- 9/27/2023
;; matching and type predicates

;; Direct-style length
(define (length lst)
  (if (empty? lst)
      0
      (add1 (length (rest lst)))))

kmicinski

#lang racket

;; CIS352 -- Fall 2023
;; Lambdas

;; first order function -- no functions as arguments
;; O(n^2) the way it's written -- an easier implementation
;; is not easy functionally, need a different representation 
(define (reverse lst)
  (if (empty? lst)

kmicinski

#lang racket

;; Recursion over lists
(cons 1 (cons 2 (cons 3 (cons 4 '()))))

;; more laboriously as ...
(let ([last-link (cons 4 '())])
  (let ([second-to-last-link (cons 3 last-link)])
    (let ([third-to-last-link (cons 2 second-to-last-link)])
      (cons 1 third-to-last-link))))

kmicinski

-- see cek.slog
def var := String

-- terms
inductive term : Type where
  | Ref : var → term
  | Lam : var → term → term
  | App : term → term → term
open term

kmicinski

#lang racket

;; CIS352 -- Spring 2023, 4/4 and 4/6/2023
;; Beginning to the Church encoding project

;; output
(define (lambda-calculus? e)
  (match e
    [(? symbol? x) #t]
    [`(lambda (,(? symbol? x)) ,(? lambda-calculus? e-body)) #t]

kmicinski

#lang racket

;; CIS352 -- Spring 2023, 4/4/2023
;; Beginning to the Church encoding project

;; output
(define (lambda-calculus? e)
  (match e
    [(? symbol? x) #t]
    [`(lambda (,(? symbol? x)) ,(? lambda-calculus? e-body)) #t]

kmicinski

;; CIS352 -- 2/28/23
#lang racket

(define x
  (hash "A" (set "B" "C")
        "B" (set "C" "A")
        "C" (set "B")))

(define (count-edges graph)
  (foldl

kmicinski

#lang racket

;; Interpreters, Feb 23

(define (arith-expr? e)
  (match e
    [(? number? n) #t]
    [`(,(? number? n0) + ,(? number? n1)) #t]
    [`(,(? number? n0) - ,(? number? n1)) #t]
    [`(,(? number? n0) * ,(? number? n1)) #t]