philzook58

#A*x = 0
using LinearAlgebra
struct HRep{T}
   n :: Int64 #input size
   A :: AbstractArray{T}
end
struct VRep{T}
   n :: Int64 #input size
   A :: AbstractArray{T}
end

philzook58

module Numeric.ADLens.Interval where
import Numeric.Interval

-- interval combinators

type Lens a b = a -> (b, b -> a) 

class Lattice a where
   (/\) :: a -> a -> a
   (\/) :: a -> a -> a

philzook58

from z3 import *
def numbery_proofs(sort):
    
    x = Const("x", sort)
    y = Const("y", sort)
    z = Const("z", sort)
    print("Commutativity")
    prove(x + y == y + x) #Commutativity
    print("Associativity")
    prove(((x + y) + z) == ((x + (y + z)))) #associativity

philzook58

plus = GraphCat.block("+",   ["a","b"],   ["c"])
I = GraphCat.idd()
p1 = plus
p2 = p1 @ (p1 * p1)
p3 = p1 @ (p2 * p2)
p4 = p1 @ (p3 * p3)

d = p4.run()
d.format = "png"
d.render("adders")

philzook58

{-# LANGUAGE GADTs, NoImplicitPrelude, StandaloneDeriving, RankNTypes #-}

module NBE where

import Data.Monoid
import Control.Category
import Prelude hiding ((.), id, fst, snd)
import Control.Arrow ((&&&))
data FM a = Pure a | Mappend (FM a) (FM a) | Mempty deriving (Eq, Show)

philzook58

T = 10 # total number of time steps as a global parameter
class PetriCat():
    def compose(f,g):
        def res():
            a, b , fcon = f()
            b1, c, gcon = g()
            return a, c, fcon + gcon + [b == b1]
    def idd():
        def res()
           x = cvx.Variable((T-1,1), integer = True)

philzook58

from z3 import *

def compare_and_swap_z3(x,y):
    x1, y1 = FreshInt(), FreshInt()
    c = If(x <= y, And(x1 == x, y1 == y) , And(x1 == y, y1 == x) )
    return x1, y1, c
    
# predicates of interest
def sorted_list(x): # list is sorted
    return And([x <= y for x,y in zip(x , x[1:])])

philzook58

def controller(Cat,pend_step, pos, vel):
   acc = Cat.idd(3)
   for i in range(10):
      acc = acc @ pend_step
   init = Cat.const(pos) * Cat.const(vel) * Cat.idd(1) 
   return acc @ init

philzook58

def matrix_to_eqs(m):
   nrows, ncols = m.shape
   gens = [sy.Dummy() for i in range(ncols)]
   eqs = m @ sy.Matrix(gens)
   return eqs, gens
def eqs_to_matrix(eqns, gens):
    return sy.Matrix( [[ eq.coeff(g) for g in gens] for eq in eqns])

philzook58

from collections import Counter
class FinSet():
    def init(self, dom ,cod , f):
        '''  In order to specify a morphism, we need to give a python set that is the domain, a python set 
        that is the codomain, and a dictionary f that encodes a function between these two sets.
        We could by assumption just use f.keys() implicitly as the domain, however the codomain is not inferable from just f.
        In other categories that domain might not be either, so we chose to require both symmettrically.
        '''
        assert( dom == set(f.keys())) # f has value for everything in domain
        assert( all( [y in cod for y in f.value()] )) # f has only values in codomain