jfdm

module Tupled

import Data.Vect
import Data.Fin

%default total

namespace Types

  public export

jfdm

#!/bin/bash

# $1 first n words
# $2 the rebuttal.

echo "## WC"
grep -vE -e "^>" $2 | grep -vE -e "^#" | uniq | wc -w
echo ""
echo "## TeX Count"
grep -vE -e "^>" $2 | uniq | texcount -1 -

jfdm

About LightClick

LightClick is a linearly typed orchestration language for Systems-on-a-Chip Designs that supports lightweight dependent types in the form of domain-specific indexed-types.

Designs represent the specification of modules at the same level of design and we capture:

• various port attributes at the type level:
  • port direction (input/output/inout)
  • wire sensitivity (high/low, rising/falling, or insensitive)
  • signal usage intent (clocking, reset, interrupt, control, information, general)

jfdm

module Lambda

%default total

data Ty = TyFunc Ty Ty | TyNat

data Context = Empty | Extend Context Ty

data Contains : Context -> Ty -> Type where

jfdm

||| Dependent Types Suck!
|||
||| Sometimes dependent types push you towards mutually defined data
||| structures: I try to avoid them where I can. For me, this occurrs
||| when you need a helper data type where a container is not suitable
||| expressive at the type level to capture the inductive case. When
||| this happens you can index your helper data structure with the
||| signature of the top type. This helps remove the need for a mutual
||| definition, that is turn the call graph edge from being undirected
||| to directed.

jfdm

module LeftPad

import Data.List

data Padding : (s : List Char) -> (target : Nat) -> Type where
  Pad : (pad : Nat) -> Padding s (length s + pad)
  Nop : Padding (ys ++ x :: xs) (length ys)

padding : (s : List Char) -> (target : Nat) -> Padding s target
padding       []     t  = Pad t

jfdm

import Data.List
import Data.List.Quantifiers

data SubsetEq : (xs, ys : List a) -> Type where
  Empty : SubsetEq Nil xs

  Cons : (Elem x ys)
      -> SubsetEq xs ys
      -> SubsetEq (x::xs) ys

jfdm

data CanSkip = MustKeep | CanSkip
data ThinnedList : (a : Type)
                -> (contract : List (Pair a CanSkip))
                -> Type
  where
    Empty : ThinnedList a Nil
    Add  : (x : a) 
        -> (rest : ThinnedList a xs) -> ThinnedList a ((x,b      )::xs)
    Skip : (rest : ThinnedList a xs) -> ThinnedList a ((x,CanSkip)::xs)

jfdm

module Sorted

data LessThanOrEq : (x,y : type)
              -> Type
  where
    IsLessThan : Ord type => {x,y : type} -> (prf : compare x y = LT) -> LessThanOrEq x y
    IsEqual    : Ord type => {x,y : type} -> (prf : compare x y = EQ) -> LessThanOrEq x y

data IsSorted : (list : List type)
             -> Type

jfdm

class Tree():
    pass

class Node(Tree):
    def __init__(self,l,r,value):
        self.l = l
        self.r = r
        self.value = value

class Leaf(Tree):