MarisaKirisame

class LVal: # logical value. store fact we know about a logical variable
    pass

class Unknown(LVal): # we dont know it's value
    pass

class Known(LVal): # we know it's value
    def __init__(self, x):
        self.x = x

MarisaKirisame

import math

def sin(x):
    if isinstance(x, Dual):
        return Dual(sin(x.x), cos(x.x) * x.dx)
    return math.sin(x)

def cos(x):
    if isinstance(x, Dual):
        return Dual(cos(x.x), -1 * sin(x.x) * x.dx)

MarisaKirisame

#!/bin/bash

set -e
set -x

mkdir $1
cd $1

gclient root

MarisaKirisame

module StringMap = Map.Make (String);;

open StringMap;;

type op =
  | Add 
  | Sub
  | Mult
  | Div;;

MarisaKirisame

Require Export List FunctionalExtensionality.
Set Implicit Arguments.

Ltac get_goal := match goal with |- ?x => x end.

Ltac get_match H F := match H with context [match ?n with _ => _ end] => F n end.

Ltac get_matches F := 
  match goal with
  | [ |- ?X ] => get_match X F

MarisaKirisame

import Data.List

data Op = Add | Mult | Sub

select :: [x] -> [(x, [x])]
select [] = []
select (a : b) = (a, b) : (do
  (c, d) <- select b
  return $ (c, a : d))

MarisaKirisame

type expr =
| Var of string
| Int of int
| Add of (expr * expr)
| Mult of (expr * expr)
| Let of (string * expr * expr)
| IfZero of (expr * expr * expr)
| Pair of (expr * expr)
| Zro of expr
| Fst of expr

MarisaKirisame

type gen = | Init | Gen of bool | Running of bool * bool * gen

let flip () = true
let one_in_three() = true

let rec generate g = 
  match g with
  | Init -> generate (Running (true, true, Init))
  | Gen b -> 
      if one_in_three() then 

MarisaKirisame

type expr = Var of int | Abs of int * expr | App of expr * expr 
          | Lit of int | Add of expr * expr;;

let cnt = ref 100;;
let fresh () = let ret = !cnt in cnt := 1; ret;;

let rec cps e k = 
  match e with
  | Var x -> App (k, (Var x))
  | Abs (v, x) ->