dannypsnl

{-# LANGUAGE LambdaCase #-}

module Tyck
  ( Term (..),
    Type (..),
    emptyContext,
    emptySolution,
    topInfer,
    infer,
    check,

dannypsnl

#lang racket

(define prime-list '(2 3 5 7 11 13 17 19 23 29 31 37 41 43 47 53 59))

(define (factor-list n)
  (define p-factor-list
    (for/list ([p prime-list]
               #:when (= (remainder n p) 0))
      p))
  (println p-factor-list)

dannypsnl

#lang racket
(require syntax/parse/define
         (for-syntax syntax/stx))

(begin-for-syntax
  (define-syntax-class type
    #:datum-literals (->)
    (pattern (~literal Type)
      #:attr occurs (λ (D) #f))
    (pattern x:id

dannypsnl

#lang racket/base
(require racket/future
         racket/async-channel
         racket/function
         racket/match)

(define process-map (make-hasheq))
(struct pid ())
(struct process (id fu ch))

dannypsnl

#lang typed/racket
#|
tree definitions
|#
(struct Tree ([v : String] [sub-tree : (Listof Tree)])
  #:property prop:custom-write
  (λ (v port mode) (if (empty? (Tree-sub-tree v))
                       (fprintf port "~a" (Tree-v v))
                       (fprintf port "~a ~a" (Tree-sub-tree v) (Tree-v v)))))

dannypsnl

#lang racket
(require syntax/parse/define
         (for-syntax syntax/stx
                     racket/string
                     racket/system)
         ffi/unsafe)

(begin-for-syntax
  (define-syntax-class c/ty
    #:datum-literals (double)

dannypsnl

#lang curly-fn racket
(require syntax/parse/define
         (for-syntax racket/syntax
                     syntax/stx))

(define-syntax-parser List
  [(_ ty) (with-disappeared-uses
              (record-disappeared-uses/recur #'ty)
            #''(List ty))])
(define-syntax-parser Integer

dannypsnl

#lang typed/racket

(define-type Prog (Listof Instruction))

(define-type Regsiter (U Symbol))
(define-type ImmediateValue (U Integer))

(struct Instruction () #:transparent)
(struct mov Instruction
  ([register : Regsiter]

dannypsnl

{-# LANGUAGE PatternSynonyms #-}

type Ix = Int
type Lvl = Int
type ULvl = Int

data Sort = Type ULvl | Prop
  deriving (Show, Eq)

data SortType = SType | SProp

dannypsnl

#lang racket

(define (%history ts xs)
  (λ args
    (cond ((null? args) `(%history ,ts ,xs))
          ((eq? (first args) 'x)
           (list-ref xs (second args)))
          ((eq? (first args) 't)
           (list-ref ts (second args)))
          ((eq? (first args) 'extend)