Skip to content

Instantly share code, notes, and snippets.

View kmicinski's full-sized avatar

Kristopher Micinski kmicinski

View GitHub Profile
#lang racket
;; CIS352 -- P3 Builtins help
;;
;; I wrote up these notes based on some student meetings.
;; This project is intentionally a bit vague about how to
;; handle the builtins. That is because I want you to have
;; some ability to have the experience of figuring out how
;; you might want to engineer your own solution, considering
;; the various trade-offs.
@kmicinski
kmicinski / buffer1.rkt
Created March 20, 2025 19:32
Exercise 3 help
#lang racket
;; Consider the folllowing λ-calculus expression, write
;; a reduction sequence where each β reduction in the
;; sequence uses CBV evaluation order
((λ (x) x)
((λ (y) y) (λ (z) z)))
((λ (x) x)
((λ (z) (z z)) (λ (y) (y y))))
@kmicinski
kmicinski / 03-20.rkt
Created March 20, 2025 17:34
CIS352 'S25 -- 3/20/25
#lang racket
;; CIS352 -- March 20, 2025
;; For the past few lectures, we've talked about the idea of "in-context" β:
;; the idea that we can "just do all the βs." So for example:
((λ (b) b)
(((λ (x) x) (λ (a) a))
((λ (y) y) (λ (z) z))))
#lang racket
;; CIS 352 -- Spring '25
;; March 18, 2025
;; This week in class:
;; [ ] λ-calculus refresher
;; [ ] λ-calculus β reduction motivation
;; [ ] Extending the λ-calculus with numbers
;; [ ] Building an interpreter with closures
#lang racket
;; CIS352 -- Feb 25, 2025
;; How do you calculate the transitive closure of a graph given using
;; the layout we've discussed?
;;
;;
;; Let's define a function `(step gr)`, which take a graph as
#lang racket
;; Algebraic Data II
;;
;; CIS352 2/6/25
;; Note: for this lecture I am transliterating some very nice
;; notes from https://abhiroop.github.io/Haskell-Red-Black-Tree/
;; (written by Abhiroop Sarkar)
#lang racket
;; 0 argument function which calls itself
;; (with zero arguments...)
(define (loop) (loop))
(if #t 42 (loop))
;; if cannot be a function, because if it were,
use std::collections::{HashMap, HashSet};
type Clause = Vec<i32>;
type Clauses = HashSet<Clause>;
type Trail = Vec<TrailEntry>;
type Assignment = HashMap<i32, bool>;
#[derive(Debug, Clone)]
enum TrailEntry {
Decision(i32),
fn run(clauses: &Clauses) {

let mut state = DpllState::Running(Vec::new(), Assignment::new(), clauses.clone()); loop {

match &state {
DpllState::Unsat => {
println!("UNSAT"); break;

} DpllState::Sat(trail) => {

println!("SAT {:?}", trail);
@kmicinski
kmicinski / dpll.rkt
Last active November 15, 2024 11:52
;; Traditional Abstract DPLL (no clause learning)
;; See this paper: https://homepage.cs.uiowa.edu/~tinelli/papers/NieOT-JACM-06.pdf
#lang racket
(define (clause? cl)
(match cl
[`(,(? integer? x) ...) #t]
[_ #f]))