dannypsnl

{-# OPTIONS --postfix-projections #-}

module tuple where





------------------------------------------------------------------------------
--

dannypsnl

{-# language
  BlockArguments
, ImplicitParams
, LambdaCase
, OverloadedStrings
, PatternSynonyms
, Strict
, UnicodeSyntax
#-}
{-# options_ghc -Wincomplete-patterns -Wunused-imports #-}

dannypsnl

module C : sig
  type t 
  val empty : t 
  val one : char -> t 
  val union : t -> t -> t 
  val inter : t -> t -> t 
  val top : t 
  val mem : char -> t -> bool 
  val make : (char -> bool) -> t 
  val equal : t -> t -> bool

dannypsnl

{-# OPTIONS --cubical #-}
module natmod where
open import Cubical.Foundations.Prelude

data Ctx : Type
data _⊢_ : Ctx → Ctx → Type
data Ty : Ctx → Type
data Tm : Ctx → Type
-- This is halfway between EAT and GAT.
-- GAT is hard! Why is EAT so easy?

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

# source:http://reocities.com/SiliconValley/heights/7052/opcode.txt
From: mark@omnifest.uwm.edu (Mark Hopkins)
Newsgroups: alt.lang.asm
Subject: A Summary of the 80486 Opcodes and Instructions

(1) The 80x86 is an Octal Machine
   This is a follow-up and revision of an article posted in alt.lang.asm on
7-5-92 concerning the 80x86 instruction encoding.
 
   The only proper way to understand 80x86 coding is to realize that ALL 80x86

dannypsnl

#lang racket

(require cpsc411/compiler-lib)

(module+ a
  ;; Compiler style
  (define (expand e)
    (define (expand-expr e)
      (match e
        [`(and ,e1 ,e2)

dannypsnl

;; Exporting free identifier table operations that close over a global map
#lang racket/base

(require racket/list
         syntax/id-table)

(provide env-ref env-has-id? env-add!)

(define id-table (make-free-id-table))

dannypsnl

module PrettyParseError (
    prettyParseError,
    PrettyParseErrorOptions(PrettyParseErrorOptions),
    prettyParseErrorDefaults
) where

import Data.List (intercalate, nub)
import Text.Parsec
import Text.Parsec.Error
import Text.Parsec.Pos

dannypsnl

#lang racket
(require redex)

;; Run to explore all of the gradual typings of the example
(define (main)
  (traces -> (term example)))

(define-term example
  (λ (x : ?)
    (λ (y : ?)