thoughtpolice

module Test where
import Clash.Prelude

-- this just puts zeros in front of the bit vector
f :: KnownNat a => BitVector a -> BitVector (a + 1)
f bv = zeroExtend bv

-- this gets the length of a bit vector, as an SNat
g :: KnownNat a => BitVector a -> SNat a
g _ = SNat

thoughtpolice

{-# LANGUAGE GADTs          #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE TypeFamilies   #-}
module Assert
  ( assertProperty
  , initialAssume
  , getReset
  ) where

import           Clash.Prelude

thoughtpolice

{-# OPTIONS_GHC -Wall -Wno-orphans #-}

{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE DeriveLift         #-}
{-# LANGUAGE LambdaCase         #-}
{-# LANGUAGE PatternSynonyms    #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators      #-}
{-# LANGUAGE TemplateHaskell    #-}
{-# LANGUAGE ViewPatterns       #-}

thoughtpolice

{-# OPTIONS_GHC -Wall #-}

{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PartialTypeSignatures #-}
module RegAlloc1
  ( -- * Types
    Var

thoughtpolice

// Generated by BUCKLESCRIPT VERSION 1.7.5, PLEASE EDIT WITH CARE
'use strict';

var Request_promise = require("request-promise");
var Config          = require("../../config.json");

function main(ev) {
  var match = ev.data.data;
  if (match !== undefined) {
    if (match !== "") {

thoughtpolice

aseipp@ubuntu:~/t$ ghc -O2 Naperian.hs -fforce-recomp +RTS -s
[1 of 1] Compiling Naperian         ( Naperian.hs, Naperian.o )
   2,109,198,400 bytes allocated in the heap
     361,254,792 bytes copied during GC
      62,051,712 bytes maximum residency (10 sample(s))
       2,566,416 bytes maximum slop
             140 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0       238 colls,     0 par    0.631s   0.631s     0.0027s    0.0210s

thoughtpolice

Copyright 2017 Austin Seipp

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

thoughtpolice

diff --git a/Z3/Category.hs b/Z3/Category.hs
index 816d8ca..7147aba 100644
--- a/Z3/Category.hs
+++ b/Z3/Category.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -25,6 +26,16 @@ import Control.Arrow (Kleisli(..), arr)

thoughtpolice

{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}

module Test where

import Data.SBV.Plugin

{-# ANN test1 theorem { options = [Verbose] } #-}
test1 :: Integer -> Integer -> Bool
test1 x y = not(
    x < y &&

thoughtpolice

type Byte = Unsigned 8

data TxState
  = TxIdle
  | TxStart   (Unsigned 8)
  | TxSending (Unsigned 8)
  | TxDone
  deriving (Eq, Show, Ord, Generic, NFData)

isSending :: Signal TxState -> Signal Bool