[haskell] add few recent files
This commit is contained in:
parent
168df58125
commit
a836af8a44
|
|
@ -0,0 +1,48 @@
|
|||
-- To see how bit repr of (Bool,Maybe Bool) would be like
|
||||
|
||||
module BitsizeTest where
|
||||
|
||||
import Clash.Prelude
|
||||
import Clash.Explicit.Testbench
|
||||
|
||||
nxt :: (Bool, Maybe Bool) -> (Bool, Maybe Bool)
|
||||
nxt (a, b) = case (a, b) of
|
||||
(False, Nothing) -> (False, Just False)
|
||||
(False, Just False) -> (False, Just True)
|
||||
(False, Just True) -> (True, Nothing)
|
||||
(True, Nothing) -> (True, Just False)
|
||||
(True, Just False) -> (True, Just True)
|
||||
(True, Just True) -> (False, Nothing)
|
||||
|
||||
tf :: (Bool, Maybe Bool) -> Bool -> ((Bool, Maybe Bool), Bool)
|
||||
tf s inp = (nxt s, fst $ nxt s)
|
||||
|
||||
mon
|
||||
:: SystemClockResetEnable
|
||||
=> Signal System Bool
|
||||
-> Signal System Bool
|
||||
mon = mealy tf (False, Nothing)
|
||||
|
||||
topEntity
|
||||
:: Clock System
|
||||
-> Reset System
|
||||
-> Enable System
|
||||
-> Signal System Bool
|
||||
-> Signal System Bool
|
||||
topEntity = exposeClockResetEnable mon
|
||||
|
||||
|
||||
-- testBench :: Signal System Bool
|
||||
-- testBench = done
|
||||
-- where
|
||||
-- testInput = stimuliGenerator clk rst
|
||||
-- $(listToVecTH [_) :: Inp,
|
||||
-- _),
|
||||
-- _])
|
||||
-- expectedOutput = outputVerifier' clk rst
|
||||
-- $(listToVecTH [False,
|
||||
-- False,
|
||||
-- False])
|
||||
-- done = expectedOutput (topEntity clk rst (enableGen) testInput)
|
||||
-- clk = tbSystemClockGen (not < done)
|
||||
-- rst = systemResetGen
|
||||
55
coq/ohe.v
55
coq/ohe.v
|
|
@ -153,38 +153,6 @@ Proof.
|
|||
exact: (lmCountMark n true a).
|
||||
Qed.
|
||||
|
||||
(*
|
||||
The command has indeed failed with message:
|
||||
Illegal application:
|
||||
The term "@markCount" of type "forall n : nat, t n true -> nat"
|
||||
cannot be applied to the terms
|
||||
"n0" : "nat"
|
||||
"t" : "t n0 b"
|
||||
The 2nd term has type "t n0 b" which should be a subtype of
|
||||
"t n0 true".
|
||||
*)
|
||||
|
||||
Fail Check Mark (Pad (Mark (Pad Nil))).
|
||||
|
||||
Example eg1: t 0 false := Nil.
|
||||
Example eg2: t 2 true := Pad (Mark Nil).
|
||||
Example eg3: t 2 true := Mark (Pad Nil).
|
||||
Example eg4: t 3 true := Pad (Mark (Pad Nil)).
|
||||
Example eg5: t 4 true := Pad (Pad (Mark (Pad Nil))).
|
||||
|
||||
Compute eqb Nil Nil.
|
||||
Compute eqb (Mark Nil) Nil.
|
||||
Compute eqb (Pad (Mark Nil)) (Mark (Pad Nil)).
|
||||
Compute eqb (Pad (Mark Nil)) (Pad (Mark Nil)).
|
||||
|
||||
Compute markCount eg2.
|
||||
Compute markCount eg3.
|
||||
Compute markCount eg4.
|
||||
Compute markCount eg5.
|
||||
|
||||
Compute to_bv eg5.
|
||||
(* = [false; false; true; false] : Bvector 4 *)
|
||||
|
||||
Fixpoint genPad (z: nat): t z false :=
|
||||
match z with
|
||||
| O => Nil
|
||||
|
|
@ -228,6 +196,29 @@ refine (
|
|||
exact: padR _ _ (Pad (Mark a')) z'.
|
||||
Defined.
|
||||
|
||||
(**************************************)
|
||||
|
||||
Fail Check Mark (Pad (Mark (Pad Nil))).
|
||||
|
||||
Example eg1: t 0 false := Nil.
|
||||
Example eg2: t 2 true := Pad (Mark Nil).
|
||||
Example eg3: t 2 true := Mark (Pad Nil).
|
||||
Example eg4: t 3 true := Pad (Mark (Pad Nil)).
|
||||
Example eg5: t 4 true := Pad (Pad (Mark (Pad Nil))).
|
||||
|
||||
Compute eqb Nil Nil.
|
||||
Compute eqb (Mark Nil) Nil.
|
||||
Compute eqb (Pad (Mark Nil)) (Mark (Pad Nil)).
|
||||
Compute eqb (Pad (Mark Nil)) (Pad (Mark Nil)).
|
||||
|
||||
Compute markCount eg2.
|
||||
Compute markCount eg3.
|
||||
Compute markCount eg4.
|
||||
Compute markCount eg5.
|
||||
|
||||
Compute to_bv eg5.
|
||||
(* = [false; false; true; false] : Bvector 4 *)
|
||||
|
||||
Compute padL (Pad (Mark Nil)) 3.
|
||||
Compute padR (Pad (Mark Nil)) 3.
|
||||
Example eg8 := Eval compute in padR (Pad (Mark Nil)) 3.
|
||||
|
|
|
|||
|
|
@ -0,0 +1,65 @@
|
|||
-- https://hackage.haskell.org/package/bytestring-0.12.1.0/docs/Data-ByteString-Lazy.html#t:LazyByteString
|
||||
import qualified Data.ByteString.Lazy as BL
|
||||
|
||||
-- https://hackage.haskell.org/package/bytestring-0.12.1.0/docs/Data-ByteString-Builder.html
|
||||
import qualified Data.ByteString.Builder as B
|
||||
|
||||
import qualified Data.Foldable
|
||||
import qualified System.Process
|
||||
import qualified Text.Printf
|
||||
|
||||
type Hz = Float
|
||||
type Seconds = Float
|
||||
type Signal = [Float]
|
||||
|
||||
-- Byte strings with Little Endian 32 bit float
|
||||
|
||||
-- B.floatLE n :: B.Builder
|
||||
|
||||
outFile :: FilePath
|
||||
outFile = "out.bin"
|
||||
|
||||
-- volume :: Float
|
||||
-- volume = 0.2
|
||||
|
||||
-- Number of samples per second
|
||||
-- ie, number of float values per second
|
||||
sampleRate :: Hz
|
||||
sampleRate = 48000
|
||||
|
||||
-- step :: Float
|
||||
-- step = 0.01
|
||||
|
||||
|
||||
duration :: Float
|
||||
duration = 2.0
|
||||
|
||||
wave :: Float -> Hz -> Seconds -> Signal
|
||||
wave volume freq duration
|
||||
= map (* volume) -- adjust volume
|
||||
$ map sin -- generate wave
|
||||
$ map (* step) [0.0 .. sampleRate * duration]
|
||||
where
|
||||
step = (freq * 2 * pi) / sampleRate
|
||||
|
||||
sound :: Signal
|
||||
sound = concat $ map (++)
|
||||
[wave 0.2 440 duration
|
||||
wave 0.2 frq secs
|
||||
|
||||
toBS :: [Float] -> B.Builder
|
||||
toBS wav = Data.Foldable.fold $ map B.floatLE wav
|
||||
|
||||
|
||||
-- LazyByteString: Serializable-friendly form of ByteString
|
||||
-- https://hackage.haskell.org/package/bytestring-0.12.1.0/docs/Data-ByteString-Lazy.html#t:LazyByteString
|
||||
save :: FilePath -> IO ()
|
||||
save outfile = BL.writeFile outfile $ B.toLazyByteString $ toBS sound
|
||||
|
||||
play :: IO ()
|
||||
play = do
|
||||
save outFile
|
||||
_ <- System.Process.runCommand
|
||||
$ Text.Printf.printf "ffplay -showmode 1 -f f32le -ar %f %s" sampleRate outFile
|
||||
return ()
|
||||
|
||||
|
|
@ -0,0 +1,53 @@
|
|||
-- https://bentnib.org/docs/algebraic-typechecking-20150218.pdf
|
||||
|
||||
-- No values tracked. Just the types.
|
||||
-- de-Bruijn index
|
||||
data Typ
|
||||
= Nat
|
||||
| Boolean
|
||||
| Arrow Typ Typ
|
||||
deriving (Eq, Show)
|
||||
|
||||
data Term
|
||||
= Var Int
|
||||
| App Term Term
|
||||
| Abs Typ Term
|
||||
|
||||
-- Context here keeps track of the type of variables.
|
||||
-- Not their values.
|
||||
type Ctxt = [Typ]
|
||||
|
||||
typecheck :: Term -> Ctxt -> Maybe Typ
|
||||
typecheck tm ctxt = case tm of
|
||||
Var i -> Just $ ctxt !! i
|
||||
App tm1 tm2 ->
|
||||
case typecheck tm1 ctxt of
|
||||
Just (Arrow typ1 typ2) ->
|
||||
case typecheck tm2 ctxt of
|
||||
Nothing -> Nothing
|
||||
Just typ1' ->
|
||||
if typ1 == typ1' then Just typ2
|
||||
else Nothing
|
||||
_ -> Nothing
|
||||
Abs ty1 tm ->
|
||||
case typecheck tm (ty1:ctxt) of
|
||||
Just ty2 -> Just $ Arrow ty1 ty2
|
||||
_ -> Nothing
|
||||
|
||||
|
||||
eg1 = Abs Boolean (Var 0)
|
||||
|
||||
-- Open terms possible too
|
||||
eg2 = Abs Boolean (Var 2)
|
||||
|
||||
eg3 = App (Abs Boolean (Var 2)) (Var 0)
|
||||
|
||||
-- λ> typecheck eg1 [Boolean, Nat, Arrow Nat Boolean]
|
||||
-- Just (Arrow Boolean Boolean)
|
||||
-- λ> typecheck eg2 [Boolean, Nat, Arrow Nat Boolean]
|
||||
-- Just (Arrow Boolean Nat)
|
||||
-- λ> typecheck eg3 [Boolean, Nat, Arrow Nat Boolean]
|
||||
-- Just Nat
|
||||
|
||||
|
||||
type TypeChecker = Ctxt -> Maybe Typ
|
||||
Loading…
Reference in New Issue