diff --git a/agda/add-assoc.agda b/agda/add-assoc.agda
new file mode 100644
index 0000000..36746b3
--- /dev/null
+++ b/agda/add-assoc.agda
@@ -0,0 +1,72 @@
+module add-assoc where
+
+open import Data.Nat using (ℕ;  zero; suc; _+_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+
+
+-- `+-assoc` is an identifier like `add-assoc`. Nothing special
++-assoc : Set
++-assoc = ∀ (a b c : ℕ) → a + (b + c) ≡ (a + b) + c  -- enunciation
+
+{- DOUBT:
+Why is this not type checking?
+
++-assoc = ∀ (a b c : ℕ) → a + (b + c) → (a + b) + c  -- enunciation
+
+ -}
+
+-- an object of this type is the proof
++-assoc-proof : ∀ (a b c : ℕ) → a + (b + c) ≡ (a + b) + c
++-assoc-proof zero b c = refl
++-assoc-proof (suc a) b c = cong suc (+-assoc-proof a b c)  -- generated from doing case-split on 'a'
+-- agda assigns a unique id to each hole
+-- C-c C-, (comma) to get info about hole under cursor
+-- For the above hole, it shows:
+-- 
+-- Goal: a + (b + c) ≡ a + b + c
+-- ————————————————————————————————————————————————————————————
+-- c : ℕ
+-- b : ℕ
+-- a : ℕ
+-- 
+-- `(a + b) + c` is shown as `a + b + c` as `+` is left associative.
+-- So both are same.
+
+{- Doing case split -}
+-- With cursor on the hole, press: C-c C-c
+-- It will ask name of variable to do case split on.
+-- We say 'a', here.
+-- Initial clause will be replaced by two new ones
+--
+-- > +-assoc-proof zero b c = {!!}       -- a replaced by zero
+-- > +-assoc-proof (suc a) b c = {!!}    -- a replaced by (suc a)
+--
+-- doing refl (by C-c C-r) finishes first case
+--
+-- Doing C-c C-, on remaining goal says:
+-- > 
+-- > Goal: suc (a + (b + c)) ≡ suc (a + b + c)
+-- > ————————————————————————————————————————————————————————————
+-- > c : ℕ
+-- > b : ℕ
+-- > a : ℕ
+-- >
+--
+-- The cong function handles cases where goal is like
+-- f(arg1) ≡ f(arg2)
+-- in which case we only have to show that arg1 ≡ arg2
+-- congruence of equality
+--
+-- we _write_ `cong suc` inside the remaining hole and do a `refl` with C-c C-r
+-- to get this goal:
+--
+-- > ?2 : a + (b + c) ≡ a + b + c
+--
+-- A recursive call to `+-assoc-proof` can finish this off.
+-- Write `+-assoc-proof a b c` into the last hole
+-- and solve it with C-c C-space
+--
+-- So the final proof is:
+--
+--   +-assoc-proof zero b c = refl
+--   +-assoc-proof (suc a) b c = cong suc (+-assoc-proof a b c)  -- generated from doing case-split on 'a'
diff --git a/agda/hello.agda b/agda/hello.agda
new file mode 100644
index 0000000..b5d3982
--- /dev/null
+++ b/agda/hello.agda
@@ -0,0 +1,101 @@
+
+-- False: a datatype without constructors
+data False : Set where
+
+-- True: a record type without fields => has
+-- only a single element, which is the empty
+-- record
+record True : Set where
+
+trivial : True
+
+-- same as 'trivial = _' as agda can
+-- figure out what the '_' stands for
+trivial = record{}
+
+
+
+
+open import Data.Bool
+isTrue : Bool -> Set
+isTrue true = True
+isTrue false = False
+
+{-
+data Nat : Set where
+  zero : Nat
+  suc : Nat → Nat
+  
+
+add : Nat → Nat → Nat
+add zero y = y
+add (suc x) y = suc (add x y)
+-}
+
+ -- _<_ : Nat → Nat → Bool
+ -- _ < zero = false
+
+open import Data.Nat
+open import Data.Bool
+-- infix 40 _<_
+_⇐_ : ℕ → ℕ → Bool
+_⇐_ zero zero = false
+_⇐_ zero _ = true
+_⇐_ (suc x) y = _⇐_ x y
+
+
+
+{-
+** Doubts
+*** true
+Anologous to Coq's
+
+Inductive True : Prop := I.
+Inductive False : Prop := .
+
+??
+
+But then again, those are propositions whereas the agda
+version deals with Set.
+Or is that how agda deals with propositions as well?
+Had heard that there was no separation unlike in the case of Coq,
+between the world of propositions and types
+
+*** Check?
+Equivalent of Check nat. of coq?
+-}
+
+{-
+open import Data.String
+
+s : String
+s = "hello"
+-}
+
+
+{-
+{-
+  Here is a comment above a module.
+-}
+module hello where --this is a comment! --fooo@.. jjwjw
+  open import Data.Bool
+  open import Data.String
+  not-comment : Bool -> Set
+{- but this is OK {-
+                    and indeed -}
+ they can be nested -}
+  s : String
+  s = "{- This is not a comment {- Notice the bad nesting -}"
+  not-comment b = {- another comment -} ? --more end-of-line
+-}
+-}
+
+{-
+data Bool : Set where
+  true : Bool
+  false : Bool
+  
+not : Bool -> Bool
+not true = false
+not false = true
+-}
diff --git a/agda/hott.agda b/agda/hott.agda
new file mode 100644
index 0000000..dc827a9
--- /dev/null
+++ b/agda/hott.agda
@@ -0,0 +1,134 @@
+Type = Set
+
+data Bool : Type where
+  true false : Bool
+
+not : Bool → Bool
+not true = false
+not false = true
+
+idBool : Bool → Bool
+idBool x = x
+
+idBool' : Bool → Bool
+idBool' = λ (x : Bool) → x
+
+id' : (X : Type) → X → X
+id' X x = x
+
+id : {X : Type} → X → X
+id x = x
+
+idBool'' : Bool → Bool
+idBool'' = id' _ -- asdf
+
+example : {P Q : Type} → P → (Q → P)
+example {P} {Q} p = f
+  where
+    f : Q → P
+    f _ = p
+
+
+example2 : {P Q : Type} → P → (Q → P)
+example2 {P} {Q} p = (λ q → p)
+
+
+ -- example : {P Q : Type} → P → (Q → P)
+ -- example {P} {Q} p = f
+ -- example : {P Q : Type} → P → (Q → P)
+ -- example {P} {Q} p = f
+ 
+-- open import binary-products
+-- 
+-- ex : {P Q : Type} → P x Q → Q x 
+
+data ℕ : Type where
+  zero : ℕ
+  succ : ℕ → ℕ
+
+three : ℕ
+three = succ (succ (succ zero))
+
+{-# BUILTIN NATURAL ℕ #-}
+-- a pragma
+three' : ℕ
+three' = 3 -- same as three
+
+-- Dependent types again
+D : Bool → Type
+D true = ℕ
+D false = Bool
+
+-- 'mix-fix' operator
+if_then_else : {X : Type} → Bool → X → X → X
+if true then x else y = x
+if false then x else y = y
+
+if[_]_then_else_ : (X : Bool → Type)
+                 → (b : Bool)
+                 → X true
+                 → X false
+                 → X b
+if[ X ] true then x else y = x                
+if[ X ] false then x else y = y                
+
+-- Π type
+unfamiliar : (b : Bool) → D b
+unfamiliar b = if[ D ] b then 3 else false
+
+-- A type indexed by a type
+data List (A : Type) : Type where
+  []   : List A
+  _::_ : A → List A → List A
+  
+ff : Type → Type
+ff = List
+-- okay, list is indeed Type → Type
+
+sample-list₀ : List ℕ
+sample-list₀ = 0 :: (1 :: (2 :: [])) -- brackets not really needed here, it's right associative
+
+infix 10 _::_
+
+-- brackets not really needed here, it's right associative
+-- sample-list1 : List ℕ
+-- sample-list1 = 0 :: 1 :: 2 :: []
+
+length : {X : Type} → List X → ℕ
+length [] = 0
+length (x :: xs) = succ (length xs)
+
+-- arbitrary recursive definitions not possible. Just like Coq.
+-- Recursions got to be structurally smaller.
+-- On a sub-term.
+
+
+ℕ-elim : {A : ℕ → Type}
+       → A 0                                -- base case
+       → ((k : ℕ) → A k → A (succ k))   -- induction step
+       → (n : ℕ) → A n
+ℕ-elim {A} a f = h
+  where
+    h : (n : ℕ) → A n
+    h zero = a
+    h (succ n) = f n IH
+      where
+        IH : A n
+        IH = h n  -- induction hypothesis
+
+ℕ-elim' : {A : ℕ → Type}
+       → A 0                                -- base case
+       → ((k : ℕ) → A k → A (succ k))   -- induction step
+       → (n : ℕ) → A n
+ℕ-elim' {A} a f zero = a
+ℕ-elim' {A} a f (succ n) = f n (ℕ-elim' a f n)
+
+
+-- Elimination principal for lists
+List-elim : {X : Type} (A : List X → Type)
+          → A []  -- base case
+          → ((x : X) (xs : List X) → A xs → A (x :: xs)) -- induction step
+          → (xs : List X) → A xs
+List-elim {X} A a f = h
+  where
+    h : (xs : List X) 
diff --git a/agda/vectors.agda b/agda/vectors.agda
new file mode 100644
index 0000000..47f2aa5
--- /dev/null
+++ b/agda/vectors.agda
@@ -0,0 +1,73 @@
+{-
+https://agda.readthedocs.io/en/latest/getting-started/a-taste-of-agda.html#programming-with-dependent-types-vectors
+
+Do:
+
+ - `C-c C-l`: saves, loads and type checks the file
+ -}
+ 
+-- file name has to be same as that of top-level module
+module vectors where
+-- This module can afterwards be imported like (in same directory)
+-- `open import vectors using (Vector; _::_)`
+
+-- Import type `ℕ` and its constructors `zero` and `suc` from `Data.Nat`
+open import Data.Nat using (ℕ; zero; suc)
+
+-- Define `Vector` type
+-- 'a typed list'
+-- the `A` argument means dependent typing. So `Vector` is actually a _family_ of types.
+-- the `ℕ` in the type is an 'index' (indexed type). Here, `Vector` has only one index.
+-- Here, the index represents the length of the vector.
+data Vector (A : Set) : ℕ → Set where
+  []   : Vector A zero
+  _::_ : ∀ {n : ℕ} (x : A) (xs : Vector A n) → Vector A (suc n)
+
+-- define precedence level of `_::_`
+infixr 5 _::_
+
+
+
+open import Data.Fin using (Fin; zero; suc)
+-- > Agda allows overloading of constructor names, and disambiguates
+-- > between them based on the expected type where they are used.'
+-- So, `Fin.zero` vs `Nat.zero` conflict is minimized.
+
+-- Function to get i-th element in a vector
+
+-- generalizable variables
+-- https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html#generalization-of-declared-variables
+variable
+  A : Set
+  n : ℕ
+
+--lookup (A : Set) (n : ℕ) : Vector A n → Fin n → ℕ
+--lookup : Vector A n → A
+--lookup (x :: xs) zero = x
+--lookup (x :: xs) (suc i) = lookup xs i
+
+lookup : Vector A n → Fin n → A
+lookup (x :: xs) zero = x
+lookup (x :: xs) (suc i) = lookup xs i
+
+
+
+{- More 
+https://agda.readthedocs.io/en/latest/language/mixfix-operators.html#mixfix-operators
+
+** Find type of an expression
+C-c C-d RET <expression>
+
+Eg:
+
+```
+1 :: []
+```
+(space around the `::` is needed as `1::[]` is an agda identifier)
+
+gives
+
+```
+Vector ℕ 1
+```
+ -}
diff --git a/c/arr-bounds-out.c b/c/arr-bounds-out.c
new file mode 100644
index 0000000..4c9523c
--- /dev/null
+++ b/c/arr-bounds-out.c
@@ -0,0 +1,24 @@
+#include<stdio.h>
+int main()
+{
+    int arr[2];
+    arr[0] = 0;
+    arr[2] = 2;                      //compcert gave no error!
+    printf("arr[0] = %d\n", arr[0]);
+    printf("arr[2] = %d\n", arr[2]); //compcert still gave no error!!
+    return 0;
+}
+
+/*
+Gave error like gcc when I tried using printf without header file:
+
+arr-bounds-out.c:6: warning: implicit declaration of function 'printf' is invalid in C99 [-Wimplicit-function-declaration]
+arr-bounds-out.c:6: warning: 'printf' is declared without a function prototype
+ */
+
+/*
+Out of bound array access gave no error! Instead printed the value:
+
+arr[0] = 0
+arr[2] = 2
+ */
diff --git a/c/hello.c b/c/hello.c
new file mode 100644
index 0000000..55c48fb
--- /dev/null
+++ b/c/hello.c
@@ -0,0 +1,6 @@
+#include<stdio.h>
+int main()
+{
+    printf("hello world!\n");
+    return 0;
+}
diff --git a/c/op-eval-order.c b/c/op-eval-order.c
new file mode 100644
index 0000000..bedcf7c
--- /dev/null
+++ b/c/op-eval-order.c
@@ -0,0 +1,25 @@
+#include<stdio.h>
+
+int a()
+{
+    printf("a ");
+    return 1;
+}
+
+int b()
+{
+    printf("b ");
+    return 2;
+}
+
+int c()
+{
+    printf("c ");
+    return 3;
+}
+
+int main()
+{
+    printf("rv: %d\n", a() + b() + c());
+    return 0;
+}
diff --git a/c/seq-point.c b/c/seq-point.c
new file mode 100644
index 0000000..ef3b6e5
--- /dev/null
+++ b/c/seq-point.c
@@ -0,0 +1,21 @@
+#include<stdio.h>
+int main()
+{
+    int a = 0;
+    a = a++ + ++a; 
+    //printf("%d\n", a); 
+    return a;
+
+/*
+a++ + ++a
+
+0++ + ++a 
+0   + ++1
+0   + 2
+2
+
+a++ + ++0
+1++ + 1
+3
+ */
+}
diff --git a/haskell/clash-unsorted/Adder.hs b/haskell/clash-unsorted/Adder.hs
new file mode 100644
index 0000000..3bdc0d7
--- /dev/null
+++ b/haskell/clash-unsorted/Adder.hs
@@ -0,0 +1,32 @@
+import Clash.Prelude
+import Clash.Explicit.Testbench
+
+foo
+  :: Applicative f
+  => (a -> b -> c)
+  -> f a
+  -> f b
+  -> f c
+foo fn x y = fn <$> x <*> y
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Signed 8)
+  -> Signal System (Signed 8)
+  -> Signal System (Signed 8)
+topEntity = exposeClockResetEnable $ foo (+)
+
+
+testBench :: Signal System Bool
+testBench = done
+ where
+  --testInput    = stimuliGenerator clk rst $(listToVecTH [2 :: Signed 8, 5, 7]) $(listToVecTH [3 :: Signed 8, 1, 5])
+  --expectOutput = outputVerifier' clk rst $(listToVecTH [5 :: Signed 8, 12])
+  testInput    = stimuliGenerator clk rst ((2 :: Signed 8) :> 5 :> 7 :> Nil) ((3 :: Signed 8) :> 1 :> 5 :> Nil)
+  expectOutput = outputVerifier' clk rst ((5 :: Signed 8) :> 12 :> Nil)
+  done         = expectOutput (topEntity clk rst en testInput)
+  en           = enableGen
+  clk          = tbSystemClockGen (not <$> done)
+  rst          = systemResetGen
diff --git a/haskell/clash-unsorted/FIR.hs b/haskell/clash-unsorted/FIR.hs
new file mode 100644
index 0000000..7311136
--- /dev/null
+++ b/haskell/clash-unsorted/FIR.hs
@@ -0,0 +1,39 @@
+module FIR where
+
+import Clash.Prelude
+
+
+-- Dot product?
+dotp :: SaturatingNum a
+     => Vec (n + 1) a
+     -> Vec (n + 1) a
+     -> a
+dotp as bs =
+  fold boundedAdd              -- Sum up the resultant list
+    (zipWith boundedMul as bs) -- Multiply corresponding values
+
+fir
+    :: (HiddenClockResetEnable dom
+      , Default a
+      , KnownNat n
+      , SaturatingNum a
+      , NFDataX a)
+    => Vec (n+1) a -> Signal dom a -> Signal dom a
+fir coeffs x_t = y_t
+ where
+  y_t = dotp coeffs <$> bundle xs
+  xs  = window x_t
+
+topEntity ::
+     Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Signed 16)
+  -> Signal System (Signed 16)
+topEntity = exposeClockResetEnable (fir (2:>3:>(-2):>8:>Nil))
+
+testBench :: Signal System Bool
+testBench = done
+ where
+  done = 
+  rst  = tbsystemClockGen
diff --git a/haskell/clash-unsorted/FullAdder.hs b/haskell/clash-unsorted/FullAdder.hs
new file mode 100644
index 0000000..338c836
--- /dev/null
+++ b/haskell/clash-unsorted/FullAdder.hs
@@ -0,0 +1,45 @@
+module FullAdder where
+
+-- import qualified Prelude.Bool as Bool
+import Clash.Prelude
+
+-- | A | B | S | C |
+-- |---+---+---+---|
+-- | 0 | 0 | 0 | 0 |
+-- | 0 | 1 | 1 | 0 |
+-- | 1 | 0 | 1 | 0 |
+-- | 1 | 1 | 0 | 1 |
+
+mac :: (Num a) => a -> (a, a) -> (a, a)
+mac acc (x, y) = (acc + x*y, acc)
+
+fulladder
+  :: Bool          -- ^ cin
+  -> (Bool, Bool)  -- ^ a and b
+  -> (Bool, Bool)  -- ^ cout and s
+fulladder False (False, False) = (False, False)
+fulladder True  (False, False) = (False, True)
+fulladder False (False, True)  = (False, True)
+fulladder True  (False, True)  = (True,  False)
+fulladder False (True,  False) = (False, True)
+fulladder True  (True,  False) = (True,  False)
+fulladder False (True,  True)  = (True,  False)
+fulladder True  (True,  True)  = (True,  True)
+
+fulladderS
+  :: (HiddenClockResetEnable dom)
+  => Signal dom (Bool, Bool)   -- ^ 
+  -> Signal dom Bool           -- ^ 
+fulladderS = mealy fulladder False
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Bool, Bool)
+  -> Signal System Bool
+topEntity = exposeClockResetEnable fulladderS
+
+-- clashi
+-- λ> :l FullAdder.hs
+-- λ> :vhdl
diff --git a/haskell/clash-unsorted/LastReg.hs b/haskell/clash-unsorted/LastReg.hs
new file mode 100644
index 0000000..1e4b08c
--- /dev/null
+++ b/haskell/clash-unsorted/LastReg.hs
@@ -0,0 +1,70 @@
+module LastReg where
+
+import Clash.Prelude
+
+lastval
+  :: Maybe b  -- ^ trigger (reset) value
+  -> Maybe a  -- ^ value saved in register
+  -> Maybe a  -- ^ output value of last
+lastval (Just _) reg = reg
+lastval Nothing  _   = Nothing
+
+lastregnextval
+  :: Maybe a  -- ^ v signal value
+  -> Maybe a  -- ^ value saved in register
+  -> Maybe a  -- ^ next value for register
+lastregnextval Nothing  Nothing    = Nothing
+lastregnextval Nothing  (Just reg) = Just reg
+lastregnextval (Just v) _          = Just v
+
+
+lastS
+  :: (HiddenClockResetEnable dom,
+      NFDataX a)
+  => Signal dom (Maybe a)    -- ^ v signal
+  -> Signal dom (Maybe b)    -- ^ r (reset) signal
+  -> Signal dom (Maybe a)    -- ^ output signal
+lastS v rst = lastval <$> rst <*> reg
+ where
+  reg = register Nothing (lastregnextval <$> v <*> reg)
+
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Maybe Int)
+  -> Signal System (Maybe Int)
+  -> Signal System (Maybe Int)
+topEntity = exposeClockResetEnable lastS
+
+
+-- import qualified Data.List as L
+-- *LastReg L> L.take 6 $ simulate @System (lastS (fromList [Just 1,  Just 2, Nothing, Just 3,  Just 4,  Nothing])) [Nothing, Just 1, Just 1,  Nothing,     Nothing, Just 1]
+-- [Nothing,Just 2,Just 2,Nothing,Nothing,Just 4]
+
+
+
+
+
+
+
+
+
+-- -- | Calculate output, next state
+-- -- output Nothing means no change in state
+-- last
+--   ::
+--   -> Maybe a -- ^ current state
+--   -> Maybe a -- ^ v
+--   -> Maybe b -- ^ r
+--   -> Maybe a -- ^ new state
+--   -> Maybe a -- ^ output
+-- last Nothing  Nothing  _        = (Nothing, Nothing)
+-- last Nothing  (Just x) _        = (Just x,  Nothing)
+-- last (Just s) Nothing  Nothing  = (Just s,  Nothing)
+-- last (Just s) Nothing  (Just _) = (Just s,  Just s)
+-- last (Just s) (Just x) Nothing  = (Just x,  Nothing)
+-- last (Just s) (Just x) (Just _) = (Just x,  Just s)
+
+
diff --git a/haskell/clash-unsorted/MAC.hs b/haskell/clash-unsorted/MAC.hs
new file mode 100644
index 0000000..feced46
--- /dev/null
+++ b/haskell/clash-unsorted/MAC.hs
@@ -0,0 +1,35 @@
+-- | Multiply and accumulate
+module MAC where
+
+-- https://haskell-haddock.readthedocs.io/en/latest/markup.html
+
+import Clash.Prelude
+
+-- | Multiply and accumulate
+mac' :: (Num a) =>
+     a       -- ^ accumulator
+  -> (a, a)  -- ^ next arguments
+  -> a       -- ^ new accumulator
+mac' acc (x, y) = acc + (x*y)
+
+mac :: (Num a) => a -> (a, a) -> (a, a)
+mac acc (x, y) = (acc + x*y, acc)
+
+macS :: (HiddenClockResetEnable dom, Num a, NFDataX a) =>
+     Signal dom (a, a)   -- ^ 
+  -> Signal dom a        -- ^ 
+macS = mealy mac 0
+
+-- s     = a
+-- i     = (a, a)
+-- s,o   = (a, a)
+-- ie,
+-- s,i,o = a,a,a
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Int, Int)
+  -> Signal System Int
+topEntity = exposeClockResetEnable macS
diff --git a/haskell/clash-unsorted/Merge.hs b/haskell/clash-unsorted/Merge.hs
new file mode 100644
index 0000000..c6b0749
--- /dev/null
+++ b/haskell/clash-unsorted/Merge.hs
@@ -0,0 +1,26 @@
+module Merge where
+
+import Clash.Prelude
+
+merge
+  :: Maybe a
+  -> Maybe a
+  -> Maybe a
+merge (Just x) _ = Just x
+merge Nothing y  = y
+
+mergef
+  :: Applicative f
+  => f (Maybe a)
+  -> f (Maybe a)
+  -> f (Maybe a)
+mergef x y = Merge.merge <$> x <*> y
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Maybe (Signed 8))
+  -> Signal System (Maybe (Signed 8))
+  -> Signal System (Maybe (Signed 8))
+topEntity = exposeClockResetEnable $ mergef
diff --git a/haskell/clash-unsorted/MulMatrixVec.hs b/haskell/clash-unsorted/MulMatrixVec.hs
new file mode 100644
index 0000000..715ab41
--- /dev/null
+++ b/haskell/clash-unsorted/MulMatrixVec.hs
@@ -0,0 +1,37 @@
+-- https://github.com/clash-lang/clash-compiler/blob/master/examples/MatrixVect.hs
+
+module MulVecMatrix where
+
+import Clash.Prelude
+import qualified Data.List as L
+
+row1 = 1 :> 2 :> 3 :> Nil
+row2 = 4 :> 5 :> 6 :> Nil
+row3 = 7 :> 8 :> 9 :> Nil
+
+matrix = row1 :> row2 :> row3 :> Nil
+-- [[1, 2, 3],
+--  [4, 5, 6],
+--  [7, 8, 9]]
+
+dotProduct v1 v2 = foldr (+) 0
+                     (zipWith (*) v1 v2)
+-- λ> dotProduct [1,2,3] [4,5,6]
+-- 32
+
+mulVecMatrix m v = map (dotProduct v) m
+
+topEntity :: Vec 3 (Signed 16) -> Vec 3 (Signed 16)
+topEntity = mulVecMatrix matrix
+{-# NOINLINE topEntity #-}
+
+
+import Clash.Explicit.Testbench
+testBench :: Signal System Bool
+testBench = done
+  where
+    testInput      = stimuliGenerator clk rst ((2 :> 3 :> 4 :> Nil) :> Nil)
+    expectedOutput = outputVerifier' clk rst ((20 :> 47 :> 74 :> Nil) :> Nil)
+    done           = expectedOutput (topEntity <$> testInput)
+    clk            = tbSystemClockGen (not <$> done)
+    rst            = systemResetGen
diff --git a/haskell/clash-unsorted/SevenSegment.hs b/haskell/clash-unsorted/SevenSegment.hs
new file mode 100644
index 0000000..22af4fe
--- /dev/null
+++ b/haskell/clash-unsorted/SevenSegment.hs
@@ -0,0 +1,43 @@
+module SevenSegment where
+
+import Clash.Prelude
+
+foo
+  :: KnownNat n
+  => BitVector n
+  -> Vec 7 Bool
+foo inp =
+  case (toInteger inp) of
+    0 -> (True  :> True :> True  :> True  :> True  :> True  :> True  :> Nil) -- 0
+    1 -> (False :> True :> True  :> False :> False :> False :> False :> Nil) -- 1
+    _ -> (True  :> True :> False :> False :> True  :> False :> True  :> Nil) -- Unknown
+
+bar
+  :: (KnownNat n,
+      Functor f)
+  => f (BitVector n)
+  -> f (Vec 7 Bool)
+bar inp = foo <$> inp
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (BitVector 7)
+  -> Signal System (Vec 7 Bool)
+topEntity = exposeClockResetEnable bar
+
+{-
+GHC: Setting up GHC took: 0.006s
+GHC: Compiling and loading modules took: 0.227s
+Clash: Parsing and compiling primitives took 0.205s
+GHC+Clash: Loading modules cumulatively took 0.553s
+Clash: Compiling SevenSegment.topEntity
+Clash: Normalization took 0.027s
+[WARNING] Dubious primitive instantiation for GHC.Integer.Type.eqInteger#: GHC.Integer.Type.eqInteger#: Integers are dynamically sized in simulation, but fixed-length after synthesis. Use carefully. (disable with -fclash-no-prim-warn)
+Clash: Netlist generation took 0.001s
+Clash: Compiling SevenSegment.topEntity took 0.031s
+Clash: Total compilation took 0.585s
+-}
+
+-- XXX: std.textio is imported in the vhdl generated. That's not synthesisable, right?
diff --git a/haskell/clash-unsorted/Streams.hs b/haskell/clash-unsorted/Streams.hs
new file mode 100644
index 0000000..70decb1
--- /dev/null
+++ b/haskell/clash-unsorted/Streams.hs
@@ -0,0 +1,78 @@
+module Streams where
+
+import Clash.Prelude
+
+type ClockType = Int
+
+-- data Stream a =
+--   Cons a (Stream a)
+-- 
+-- merge
+--   :: Stream (Maybe a)
+--   -> Stream (Maybe a)
+--   -> Stream (Maybe a)
+-- merge (Cons (Just x') xs) (Cons _  ys) = Cons (Just x') (merge xs ys)
+-- merge (Cons Nothing   xs) (Cons y' ys) = Cons y'        (merge xs ys)
+
+-- merge' :: (Maybe a, Maybe a) -> Maybe a
+-- merge' (Just x, _) = Just x
+-- merge' (_, y) = y
+
+
+merge
+  :: Maybe a             -- State: Unused
+  -> (Maybe a, Maybe a)  -- Input: values from 2 streams
+  -> (Maybe a, Maybe a)  -- Output, next state
+merge _ (Just x, _) = (Nothing, Just x)
+merge _ (_, y) = (Nothing, y)
+
+delay
+  :: Maybe ClockType              -- State: Remaining time
+  -> (Maybe ClockType, Maybe ())  -- Input: d,r values
+  -> (Maybe ClockType, Maybe ())  -- Output, next state
+-- XXX: Got to limit ClockType to greater than 0
+delay (Just 0) (Nothing, Nothing) = (Nothing, Just ())   -- fire. No new delay.
+delay (Just 0) (Just d, _) = (Just (d-1), Just ())       -- fire. New delay with/without reset signal
+delay _ (Nothing, Just ()) = (Nothing, Nothing)          -- reset when it wasn't about to fire
+delay _ (Just d, Just r) = (Just (d-1), Nothing)         -- set when it wasn't about to fire
+
+mergeS
+  :: (HiddenClockResetEnable dom,
+      Num a,
+      NFDataX a)
+  => Signal dom (Maybe a, Maybe a)
+  -> Signal dom (Maybe a)
+mergeS = mealy Streams.merge Nothing
+
+-- delayS
+--   :: (HiddenClockResetEnable dom,
+--       --Num a,
+--       NFDataX a)
+--   => Signal dom (Maybe a, Maybe ())
+--   -> Signal dom (Maybe ())
+-- -- XXX: There's a Clash.Prelude.delay: Could be something we can use
+-- delayS = mealy Streams.delay Nothing
+
+delayS
+  :: HiddenClockResetEnable dom
+  => Signal dom (Maybe ClockType, Maybe ())
+  -> Signal dom (Maybe ())
+delayS = mealy Streams.delay Nothing
+
+-- topEntity ::
+--      Clock System
+--   -> Reset System
+--   -> Enable System
+--   -> Signal System (Maybe Int, Maybe Int)
+--   -> Signal System (Maybe Int)
+-- topEntity = exposeClockResetEnable Streams.mergeS 
+
+topEntity ::
+     Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Maybe ClockType, Maybe ())
+  -> Signal System (Maybe ())
+topEntity = exposeClockResetEnable Streams.delayS
+
+-- XXX: How to pass functions as arguments to clash functions
diff --git a/haskell/clash-unsorted/TimeMealy.hs b/haskell/clash-unsorted/TimeMealy.hs
new file mode 100644
index 0000000..4775071
--- /dev/null
+++ b/haskell/clash-unsorted/TimeMealy.hs
@@ -0,0 +1,29 @@
+module TimeMealy where
+
+import Clash.Prelude
+
+-- | Transition function to be used for time TeSSLa operation
+timefn
+  :: Int            -- ^ state: current time
+  -> a              -- ^ input: irrelevant
+  -> (Int, Int)     -- ^ nextstate,output. output is current state itself
+timefn t _ = (t+1, t)
+
+timeS
+  :: HiddenClockResetEnable dom
+  => Signal dom a
+  -> Signal dom Int
+timeS = mealy timefn 0
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Maybe (Signed 8))
+  -> Signal System Int
+topEntity = exposeClockResetEnable timeS
+
+-- import qualified Data.List as L
+-- *TimeMealy L> L.take 4 $ simulate @System timeS [1::Int, 2, 3, 4]
+-- [0,1,2,3]
+
diff --git a/haskell/clash-unsorted/TimeReg.hs b/haskell/clash-unsorted/TimeReg.hs
new file mode 100644
index 0000000..705907e
--- /dev/null
+++ b/haskell/clash-unsorted/TimeReg.hs
@@ -0,0 +1,52 @@
+module TimeReg where
+
+import Clash.Prelude
+
+time
+  :: Maybe a    -- ^ signal value
+  -> Int        -- ^ time value present in register
+  -> Maybe Int  -- ^ output
+time Nothing _ = Nothing
+time _ t = Just t
+
+timeS
+  :: HiddenClockResetEnable dom
+  => Signal dom (Maybe a)
+  -> Signal dom (Maybe Int)
+timeS x = time <$> x <*> r
+ where
+  r = register 0 (r + 1)
+
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Maybe (Signed 8))
+  -> Signal System (Maybe Int)
+topEntity = exposeClockResetEnable timeS
+
+
+
+
+-- import qualified Data.List as L
+-- *TimeReg L> L.take 5 $ simulate @System timeS [Just 0, Just 1, Nothing, Just 3, Nothing]
+-- [Just 0,Just 1,Nothing,Just 3,Nothing]
+
+
+
+
+
+
+
+
+-- old output
+-- import qualified Data.List as L
+-- *TimeReg L> L.take 4 $ simulate @System timeS [Just 1::Maybe (Signed 8), Just 2, Nothing, Just 3, Just 4]
+-- *TimeReg L> L.take 4 $ simulate @System timeS [Just 1, Just 2, Nothing, Just 3, Just 4]
+-- [Just 0,Just 1,Nothing,Just 3]
+-- [Just 1, Just 2, Nothing, Just 3, Just 4]
+--         [Just 0,Just 1,Nothing,Just 3]
+
+
+
diff --git a/haskell/clash-unsorted/TimeSState.hs b/haskell/clash-unsorted/TimeSState.hs
new file mode 100644
index 0000000..6682cd6
--- /dev/null
+++ b/haskell/clash-unsorted/TimeSState.hs
@@ -0,0 +1,34 @@
+module TimeSState where
+
+import Clash.Prelude
+
+newtype SState a = SState a deriving Show
+
+instance Functor SState where
+  -- fmap :: (a -> b) -> SState a -> SState b
+  fmap f (SState x) = SState (f x)
+-- *TimeMealy L> (\x -> x + 1) <$> (SState 3)
+-- SState 4
+
+
+instance Applicative SState where
+  -- pure :: a -> SState a
+  pure x = SState x
+
+  -- (<*>) :: SState (a -> b) -> SState a -> SState b
+  (SState f) <*> (SState x) = SState (f x)
+-- *TimeMealy L> (+) <$> (SState 3) <*> (SState 2)
+-- SState 5
+
+
+instance Monad SState where
+  -- (>>=) :: SState a -> (a -> SState b) -> SState b
+  (SState x) >>= f = f x
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Maybe (Signed 8))
+  -> Signal System Int
+topEntity = exposeClockResetEnable timeS
diff --git a/haskell/clash-unsorted/mux.hs b/haskell/clash-unsorted/mux.hs
new file mode 100644
index 0000000..23dc2b5
--- /dev/null
+++ b/haskell/clash-unsorted/mux.hs
@@ -0,0 +1,20 @@
+import Clash.Prelude
+
+foo :: Bool -> a -> a -> a
+foo False x y = x
+foo True  x y = y
+
+topEntity
+  :: (Clock System,
+      Reset System,
+      Enable System)
+  -> Signal System Bool
+  -> Signal System Int
+  -> Signal System Int
+  -> Signal System Int
+topEntity sel a b = exposeClockResetEnable $ (mux foo) <$> a <*> b
+
+mux [True] [1] [2]
+mux (pure True :-) (1 :-)  (2 :-)
+
+mux (True) (1)  (2)
diff --git a/haskell/unsorted/coinductive-type.hs b/haskell/unsorted/coinductive-type.hs
new file mode 100644
index 0000000..04d0da2
--- /dev/null
+++ b/haskell/unsorted/coinductive-type.hs
@@ -0,0 +1,19 @@
+data Stream a =      
+   Cons a (Stream a) 
+   deriving Show
+
+-- | Return first n elements from a stream as a list
+streamTake
+  :: Int       -- ^ Number of elements to take
+  -> Stream a  -- ^ Input stream
+  -> [a]       -- ^ List of elements from input stream
+streamTake 0 xs = []
+streamTake n (Cons x xs) = x : streamTake (n-1) xs
+
+x = Cons 0 $ Cons 1 $ Cons 2 x
+
+{-
+ - *Main> streamTake 5 x
+ - [0,1,2,0,1]
+ - }
+
diff --git a/haskell/unsorted/mult-arg-datatype.hs b/haskell/unsorted/mult-arg-datatype.hs
new file mode 100644
index 0000000..f6f2fdc
--- /dev/null
+++ b/haskell/unsorted/mult-arg-datatype.hs
@@ -0,0 +1,13 @@
+data Foo d a = Nil d a
+             | Cons a (Foo d a)
+
+
+--data Vect n a = Cons a (Vect n a)
+
+--data Vect (n::Int) a = Cons a (Vect n a)
+--data Vect n a = Cons a (Vect n a)
+--              | Nil a
+
+--a = Nil 3
+
+--Is it possible to have a type which accepts two arguments? I was trying to have something like ` data Vect (n::Int) a = Cons a (Vect n a)`
diff --git a/haskell/unsorted/multi-arg-functor.hs b/haskell/unsorted/multi-arg-functor.hs
new file mode 100644
index 0000000..7737f5c
--- /dev/null
+++ b/haskell/unsorted/multi-arg-functor.hs
@@ -0,0 +1,13 @@
+-- https://stackoverflow.com/questions/58528701/how-can-i-instance-functor-for-a-type-with-two-parameters
+
+-- Tuple2
+data T2 a b = T2 a b deriving Show
+-- ghci> T2 2 3
+-- T2 2 3
+-- ghci> T2 2 True
+-- T2 2 True
+
+instance Functor m => Functor (T2 m) where
+  fmap f (T2 a) = T2 (\x -> fmap g (a x))
+   where
+    g, (r,s) = (f r, s)
diff --git a/haskell/unsorted/state-monad.hs b/haskell/unsorted/state-monad.hs
new file mode 100644
index 0000000..0b34511
--- /dev/null
+++ b/haskell/unsorted/state-monad.hs
@@ -0,0 +1,29 @@
+-- | https://en.wikibooks.org/wiki/Haskell/Understanding_monads/State#Turnstile_Example
+
+import Control.Monad
+-- import Control.Monad.State  -- For [state]
+
+newtype State s a = State {
+    -- a 'state processor'
+    runState :: s -> (a, s)
+    --          |     |  |
+    -- initial state  |  |
+    --    'output value' |
+    --          Final state
+}
+
+state :: (s -> (a, s)) -> State s a
+state = State
+
+instance Functor (State s) where
+  fmap = liftM
+
+instance Applicative (State s) where
+  pure = return
+  (<*>) = ap
+
+instance Monad (State s) where
+  return :: a -> State s a
+  return x = state (\s -> (x, s))
+
+  (>>=) :: State s a -> (a -> State s b) -> State s b
diff --git a/haskell/unsorted/tree.hs b/haskell/unsorted/tree.hs
new file mode 100644
index 0000000..44a2ddc
--- /dev/null
+++ b/haskell/unsorted/tree.hs
@@ -0,0 +1,24 @@
+data Tree a = Empty
+            | Node (Tree a) a (Tree a)
+            deriving Show
+
+
+-- | Assuming that 0 won't occur
+-- Find maximum value in a tree
+maxOfTree :: Tree Int -> Int
+maxOfTree Empty        = 0
+maxOfTree (Node l x r) = max x (max (maxOfTree l) (maxOfTree r))
+
+-- | Replace all elements in a tree with a value
+replaceElems :: Tree Int -> Int -> Tree Int
+replaceElems Empty        x = Empty
+replaceElems (Node l _ r) x = Node (replaceElems l x) x (replaceElems r x)
+
+-- | Replace all elements in a tree with its maximum value
+maxT :: Tree Int -> Tree Int
+maxT t = replaceElems t (maxOfTree t)
+
+
+sampleTree = Node (Node Empty 2 Empty) 3 (Node Empty 4 Empty)
+rv = maxT sampleTree
+-- Node (Node Empty 4 Empty) 4 (Node Empty 4 Empty)
diff --git a/haskell/unsorted/tree_sir.hs b/haskell/unsorted/tree_sir.hs
new file mode 100644
index 0000000..f06447c
--- /dev/null
+++ b/haskell/unsorted/tree_sir.hs
@@ -0,0 +1,30 @@
+data Tree a = Empty
+            | Node (Tree a) a (Tree a) deriving Show
+
+singleton :: a -> Tree a
+singleton x = Node Empty x Empty
+
+-- Return tree with all elements replaced by given value
+ofShape :: Tree a -> a -> Tree a
+ofShape Empty           _ = Empty
+ofShape (Node lt _ rt)  x = Node (ofShape lt x) x (ofShape rt x)
+
+-- Helper function does the following
+--
+-- Input :: a value x and a tree t
+--
+-- Output :: a tuple (t',m) where t' is a tree of the same shape as t but with
+--           x at each of the nodes, and m is the maximum of all elements in t
+--
+helper :: Int -> Tree Int -> (Tree Int, Int)
+helper _ Empty          = (Empty, 0)
+helper x (Node lt u rt) = (Node ls x rs, lmax `max` u `max` rmax)
+  where (ls,lmax) = helper x lt
+        (rs, rmax)= helper x rt
+
+onePass :: Tree Int -> Tree Int
+onePass t = tx
+     where (tx, mx) = helper mx t
+
+mytree :: Tree Int
+mytree = Node (singleton 8) 4 (Node (singleton 5) 2 (singleton 1))
diff --git a/haskell/unsorted/typeclass-as-param.hs b/haskell/unsorted/typeclass-as-param.hs
new file mode 100644
index 0000000..4778f44
--- /dev/null
+++ b/haskell/unsorted/typeclass-as-param.hs
@@ -0,0 +1,24 @@
+mergefn :: (Maybe a1) -> (Maybe a1) -> Maybe a1
+mergefn a b =
+  case a of {
+   Just _ -> a;
+   Nothing -> b}
+{-
+ - *Main> mergefn (Just 3) Nothing
+ - Just 3
+ - *Main> mergefn Nothing (Just 3)
+ - Just 3
+ -}
+
+merge :: (Functor a2) -> (Applicative a2) -> ((Maybe a1) -> (Maybe a1) ->
+         Maybe a1) -> a2 -> a2 -> a2
+merge ftor appl _ a b =
+  ap ftor appl (fmap ftor mergefn a) b
+
+{-
+mergefn :: (Maybe a1) -> (Maybe a1) -> Maybe a1
+mergefn a b =
+  case a of {
+   Just _ -> a;
+   Nothing -> b}
+-}
diff --git a/misc/acl2-hello.lisp b/misc/acl2-hello.lisp
new file mode 100644
index 0000000..9948139
--- /dev/null
+++ b/misc/acl2-hello.lisp
@@ -0,0 +1,6 @@
+(defun mem (e x)
+  (if (consp x)
+      (if (equal e (car list))
+          t
+          (mem e (cdr x))
+      nil)))
diff --git a/misc/bluespec/Makefile b/misc/bluespec/Makefile
new file mode 100644
index 0000000..33445b3
--- /dev/null
+++ b/misc/bluespec/Makefile
@@ -0,0 +1,14 @@
+FILENAME=Top.bs
+MODNAME=mkTop
+
+build: $(FILENAME)
+	bsc -sim -g $(MODNAME) $(FILENAME)
+link: $(MODNAME).ba
+	bsc -sim -e $(MODNAME) -o a.out
+sim: a.out
+	./a.out
+
+.PHONY: clean
+
+clean: 
+	rm -rf *.so *.out *.h *.o *.ba *.bo *.cxx *.h
diff --git a/misc/bluespec/Top.bs b/misc/bluespec/Top.bs
new file mode 100644
index 0000000..d9d19eb
--- /dev/null
+++ b/misc/bluespec/Top.bs
@@ -0,0 +1,25 @@
+{-
+https://raw.githubusercontent.com/BSVLang/Main/master/Tutorials/Bluespec_Classic_Training/Examples/Eg02_HelloWorld.pdf
+ -}
+package Top where
+
+-- module name is mkTop
+-- Empty is the interface part.
+-- mkTop module has no interface. ie, no methods.
+-- So it cannot interact with its environment.
+mkTop :: Module Empty
+
+-- mkTop's definition
+mkTop =
+  module
+    rules
+      -- a rule named `"rl_print_answer"`
+      -- Here, always executed because of the True, I guess.
+      "rl_print_answer": when True ==> do
+
+          -- `$display` prints messages (with a newline appended)
+          $display "Hello, World!"
+          $display "answer is: %0d (or, in hex: 0x%0h)\n"  42  42
+
+          -- halts whole simulation to terminate. So, this rule can fire only once
+          $finish