diff --git a/bash/pdfscript.sh b/bash/pdfscript.sh
new file mode 100644
index 0000000..12b4a23
--- /dev/null
+++ b/bash/pdfscript.sh
@@ -0,0 +1,103 @@
+# https://askubuntu.com/a/1360466
+
+# remove pages by range: 1-2,3,5,6-8
+#   what about 1-2,4,2-4
+#   what about 1,1
+# landscape/portrait option to pdfnup
+# outfile
+# tempfile name (default: ./.temp.pdf)
+# infile
+# inplace (in which case CROPPED,INFILE,OUTFILE would be same
+# margin (single val or ltrb)
+#   ie, 10
+#       10 15 10 15
+# number of pages (default 2x1)
+#
+# getopt input.pdf output.pdf [--landscape]
+
+#INFILE="in.pdf"
+#CROPPED="cropped.pdf"
+#OUTFILE="outnx1.pdf"
+#pdfcrop --margins 10 $INFILE $CROPPED
+#./pdfnup --nup 2x1 $CROPPED -o $OUTFILE --landscape
+
+DEBUG=
+
+# Handle optional arguments
+LANDSCAPE=
+PAGES=
+CROPPED=./cropped.pdf
+SELECTED=./selected.pdf
+LAYOUT="2x1"
+GETARGS=$(getopt -o 'r:o::' -l 'margins:,pages:,layout:,landscape::' -- $@) || exit
+eval "set -- $GETARGS"
+
+while true; do
+   case $1 in
+   (--margins)
+        MARGINS=$2
+        shift 2;;
+   (--layout)
+        LAYOUT=$2
+        shift 2;;
+   (--pages)
+        PAGES=$2
+        shift 2;;
+   (--landscape)
+        LANDSCAPE=1
+        shift 2;;
+   (--)
+      # opt args parsed
+      shift
+      break;;
+   *)
+      echo "Uh-oh.. Something went wrong.."
+      exit 1;
+   esac
+   #shift 2
+done;
+
+echo "REMARGS: $@"
+
+function echoyn {
+    if [ $1 ]; then
+        echo $1
+    else
+        echo "N"
+    fi
+}
+
+if [ $# -lt 2 ]; then
+    echo "Not enough positional args"
+    exit 1
+fi
+
+INFILE=$1
+OUTFILE=$2
+
+# select: in ->
+# crop:  ->
+# layout: -> out
+
+# Use only selected pages if needed if needed
+if [ $PAGES ]; then
+    gs -sDEVICE=pdfwrite -dNOPAUSE -dBATCH -sPageList=$PAGES -sOutputFile=$INFILE $SELECTED > /dev/null
+else
+    SELECTED=$INFILE
+fi
+
+# Crop if needed
+if [ $MARGINS ]; then
+    pdfcrop --margins $MARGINS $SELECTED $CROPPED
+else
+    CROPPED=$SELECTED
+fi
+
+if [ $LANDSCAPE ]; then
+    ./pdfnup --nup $LAYOUT $CROPPED -o $OUTFILE --landscape
+else
+    ./pdfnup --nup $LAYOUT $CROPPED -o $OUTFILE
+fi
+
+# Clean up
+rm -f $CROPPED $SELECTED
diff --git a/bsv/bMakefile b/bsv/bMakefile
new file mode 100644
index 0000000..50cc06e
--- /dev/null
+++ b/bsv/bMakefile
@@ -0,0 +1,46 @@
+# Tool for simulating verilog
+EXEFILE_VSIM ?= iverilog
+
+# Path to bsim
+EXEFILE_VSIM ?= bsim
+
+
+all: compile link sim
+
+compile:
+	@echo Compiling for Bluesim ...
+	bsc -u -sim $(BSCDIRS_BSIM)  $(BSCFLAGS)  -p $(BSCPATH_BSIM)  $(TOPFILE)
+	@echo Compilation for Bluesim finished
+
+link:
+	@echo Linking for Bluesim ...
+	bsc  -sim  -parallel-sim-link 8\
+		$(BSCDIRS_BSIM)  -p $(BSCPATH_BSIM) \
+		-e $(TOPMODULE) -o ./$(EXEFILE_BSIM) \
+		-keep-fires \
+		$(BSC_C_FLAGS)
+	@echo Linking for Bluesim finished
+
+sim:
+	@echo Simulation in Bluesim...
+	./$(EXEFILE_BSIM)
+	@echo Simulation in Bluesim finished
+
+vall: v_compile v_link v_sim
+
+v_compile: build_v verilog
+	@echo "Compiling for Verilog (Verilog generation) ..."
+	bsc -u -elab -verilog  $(BSCDIRS_V)  $(BSCFLAGS)  -p $(BSCPATH_V)  $(TOPFILE)
+	@echo Verilog generation finished
+
+v_link:
+	@echo Linking for Verilog simulation ...
+	bsc -verilog  -vsim $(VSIM)  $(BSCDIRS_V) \
+		-e $(TOPMODULE) -o ./$(EXEFILE_VSIM) \
+		-keep-fires
+	@echo Linking for Verilog simulation finished
+
+v_sim:
+	@echo Verilog simulation ...
+	./$(EXEFILE_VSIM)
+	@echo Verilog simulation finished
diff --git a/bsv/hack.bsv b/bsv/hack.bsv
new file mode 100644
index 0000000..2ebda84
--- /dev/null
+++ b/bsv/hack.bsv
@@ -0,0 +1,131 @@
+/*
+https://github.com/rsnikhil/RISCV_ISA_Formal_Spec_in_BSV/blob/master/RISCV_Spec/RISCV_Spec.bsv
+https://github.com/rsnikhil/RISCV_ISA_Formal_Spec_in_BSV/blob/master/RISCV_Spec/ISA_Decls.bsv
+ */
+
+package Instr;
+  import Ainstr :: *;
+  import Cinstr :: *;
+
+  /* typedef Bit#(16) Instr; */
+
+  typedef struct {
+    Bit#(1) ac;
+    union tagged {
+      Ainstr::T;
+      Cinstr::T;
+    }
+  } T deriving Bits;
+endpackage: Instr
+
+package Ainstr;
+  typedef struct {
+    Bit#(15) loc;
+  } T deriving Bits;
+
+  function Bit#(15) loc(T ai) = ai::loc; 
+endpackage: Ainstr
+
+package Cinstr;
+  typedef struct {
+    Bit#(1) zx;
+    Bit#(1) nx;
+    Bit#(1) zy;
+    Bit#(1) ny;
+    Bit#(1) f;
+    Bit#(1) no;
+  } Comp deriving Bits;
+
+  // Fields of C-instruction
+  typedef Bit#(1) A;     // `a' value
+  typedef Bit#(3) Dest;  // Destination register
+  typedef Bit#(3) Jump;  // Jump target
+
+  typedef struct {
+    Reserved#(2) dummy;  // unused bits
+    Instr::A a;
+    Instr::Comp comp;
+    Instr::Dest dest;
+    Instr::Jump jump;
+  } T deriving Bits;
+
+  function A a(T ci) = ci::a; 
+  function Comp comp(T ci) = ci::comp;
+  function Dest dest(T ci) = ci::dest;
+  function Jump jump(T ci) = ci::jump;
+
+  /* function A a(T i) = i[12]; */ 
+  /* function Comp comp(T i) = i[11:6]; */ 
+  /* function Dest dest(T i) = i[5:3]; */ 
+  /* function Jump jump(T i) = i[2:0]; */ 
+
+  // A -> Comp -> 
+  /* function Instr encode(A a, Comp c, Dest d, Jump j); */
+endpackage: cinstr
+
+package hack;
+  // ALU
+  function Tuple3#(Bit#(16), // out
+                   Bit#(1),  // zr: Set if out is zero
+                   Bit#(1))  // ng: Set if out is negative
+    alu(Bit#(16) x,
+        Bit#(16) y,
+        Bit#(1) zx,   // Zero x input
+        Bit#(1) nx,   // Negate x input
+        Bit#(1) zy,   // Zero y input
+        Bit#(1) ny,   // Negate y input
+        Bit#(1) f,    // x+y if set, else x&&y
+        Bit#(1) no);  // Negate out value
+    Bit#(16) out=0;
+    Bit#(1) zr=0;
+    Bit#(1) ng=0;
+
+    if(zx) x=0;
+    if(nx) x=!x;
+    if(zy) y=0;
+    if(ny) y=!y;
+
+    if(f) out=x+y;
+    else out=x&y;
+
+    if(no) out=!out;
+
+    if(out==0) zr=1;
+    else zr=0;
+
+    if(out<0) ng=1;
+    else ng=0;
+
+    return tuple3(out, zr, ng); 
+  endfunction
+
+import Instr :: *;
+
+function Tuple4#(Bit#(16), Bit#(1), Bit#(15), Bit#(15))
+   alufn(Bit#(16) inM, Bit#(16) instr, Bit#(1) reset);
+
+endfunction
+
+
+interface CPU_I;
+  method Action start(
+    Bit#(16) inM,
+    Instr::T instr,
+    Bit#(1) rst        // reset
+  );
+  method #(Bit#(16)) getOutM();
+  method #(Bit#(1)) getWriteM();
+  method #(Bit#(15)) getAddrM();
+  method #(Bit#(15)) getPC();
+endinterface: CPU_I
+
+module cpu(CPU_I);
+  Reg#(Bit#(16)) PC;
+  Reg#(Bit#(16)) D;
+  Reg#(Bit#(16)) M;
+
+  method Action start(Bit#(16) inM, Instr::T instr, Bit#(1) rst);
+  
+endmodule: cpu
+
+endpackage: hack
diff --git a/c/malloc-cast.c b/c/malloc-cast.c
new file mode 100644
index 0000000..554dc59
--- /dev/null
+++ b/c/malloc-cast.c
@@ -0,0 +1,21 @@
+#include<stdio.h>
+int main(void)
+{
+    char *ptr = (char *)malloc(sizeof(char) * 2);
+    ptr[0] = '0';
+    ptr[1] = '1';
+    printf("'%c'\n", ptr[0]);
+    printf("'%c'\n", ptr[1]);
+
+
+
+    /*
+    int *ptr = (int *)malloc(sizeof(ptr) * 2);
+    ptr[0] = 0;
+    ptr[1] = 1;
+    printf("%d\n", ptr[0]);
+    printf("%d\n", ptr[1]);
+    */
+    //free(ptr);
+    return 0;
+}
diff --git a/c/void-rv-assign.c b/c/void-rv-assign.c
new file mode 100644
index 0000000..6996646
--- /dev/null
+++ b/c/void-rv-assign.c
@@ -0,0 +1,15 @@
+#include<stdio.h>
+void foo() { }
+int main() {
+    void a = foo();
+    return 0;
+}
+
+/*
+void-rv-assign.c:4:10: error: variable or field ‘a’ declared void
+     void a = foo();
+          ^
+void-rv-assign.c:4:14: error: void value not ignored as it ought to be
+     void a = foo();
+              ^~~
+*/
diff --git a/clash/FIR.hs b/clash/FIR.hs
new file mode 100644
index 0000000..c93580e
--- /dev/null
+++ b/clash/FIR.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE CPP #-}
+
+module FIR where
+
+import Clash.Prelude
+
+dotp :: (SaturatingNum a, KnownNat n)
+     => Vec (n + 1) a
+     -> Vec (n + 1) a
+     -> a
+dotp as bs = fold boundedAdd (Clash.Prelude.zipWith boundedMul as bs)
+
+fir
+  :: ( HiddenClockResetEnable tag
+     , Default a
+     , KnownNat n
+     , SaturatingNum a
+     , NFDataX a )
+  => Vec (n + 1) a -> Signal tag a -> Signal tag 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))
diff --git a/clash/ListInput.hs b/clash/ListInput.hs
new file mode 100644
index 0000000..302b0cc
--- /dev/null
+++ b/clash/ListInput.hs
@@ -0,0 +1,30 @@
+module ListState where
+  
+import Clash.Prelude
+
+tf
+  :: (Ord a, Num a)
+  => ()
+  -> [a]
+  -> ((), Bool)
+tf s i =
+  if sum i > 10 then ((), True)
+  else ((), True)
+
+tfun
+  :: SystemClockResetEnable
+  => Signal System [Int]
+  -> Signal System Bool
+tfun = mealy tf ()
+          
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System [Int]
+  -> signal System Bool
+topEntity = exposeClockResetEnable tfun
+
+{-
+compiles but doesn't synthesize
+-}
diff --git a/clash/ListState.hs b/clash/ListState.hs
new file mode 100644
index 0000000..85b0758
--- /dev/null
+++ b/clash/ListState.hs
@@ -0,0 +1,31 @@
+module ListState where
+  
+import Clash.Prelude
+import qualified Data.List
+
+lst = [1,2,3]
+
+tf
+  :: Int
+  -> ()
+  -> (Int, Int)
+tf s i = (mod (s+1) 3, (Data.List.!!) lst s)
+
+tfun
+  :: SystemClockResetEnable
+  => Signal System ()
+  -> Signal System Int
+tfun = mealy tf 0
+             
+          
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System ()
+  -> Signal System Int
+topEntity = exposeClockResetEnable tfun
+
+{-
+compiles and synthesizes
+-}
diff --git a/clash/Mac.hs b/clash/Mac.hs
new file mode 100644
index 0000000..2eb2a05
--- /dev/null
+++ b/clash/Mac.hs
@@ -0,0 +1,28 @@
+module Mac where
+  
+import Clash.Prelude
+import Clash.Explicit.Testbench
+import qualified Data.List as L
+
+
+tf
+  :: Int
+  -> (Int, Int)
+  -> (Int, Int)
+tf s (a,b) = (s+a*b, s)
+
+tfun
+  :: SystemClockResetEnable
+  => Signal System (Int, Int)
+  -> Signal System Int
+tfun = mealy tf 0
+             
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Int, Int)
+  -> Signal System Int
+topEntity = exposeClockResetEnable tfun
+
+-- L.take 4 $ simulate @System tfun [(1,1),(2,2),(3,3),(4,4)]
diff --git a/clash/Nfa.hs.orig b/clash/Nfa.hs.orig
new file mode 100644
index 0000000..b036a81
--- /dev/null
+++ b/clash/Nfa.hs.orig
@@ -0,0 +1,58 @@
+import Clash.Prelude
+import qualified Prelude
+import qualified Data.List
+
+-------------------------------------------------------------
+
+lshift :: [a] -> [Either a b]
+lshift = Prelude.map Left
+
+rshift :: [b] -> [Either a b]
+rshift = Prelude.map Right
+
+-------------------------------------------------------------
+
+data Nfa a = Nfa {
+    start :: [a]
+  , final :: [a]
+  , tfun :: a -> Maybe Char -> a -> Bool
+}
+
+-------------------------------------------------------------
+
+eps :: Nfa ()
+eps = Nfa {
+    start = [()]
+  , final = [()]
+  , tfun = \ s c d -> case (c, s, d) of
+      (Nothing, (), ()) -> True
+      otherwise -> False
+    -- () to () possible but not by consuming `c'
+}
+
+char :: (Char -> Bool) -> Nfa Bool
+char f = Nfa {
+    start = [False]
+  , final = [True]
+  , tfun = \ s c d -> case (c, s, d) of
+      (Just c, False, True) -> f c
+      (Nothing, False, False) -> True
+      (Nothing, True, True) -> True
+      otherwise -> False
+}
+
+cat :: Nfa a -> Nfa b -> Nfa (Either a b)
+cat a1 a2 = Nfa {
+    start = lshift (start a1)
+  , final = rshift (final a2)
+  , tfun = \ s c d -> case (c, s, d) of
+      (Just c, Left s, Left d) -> (tfun a1) s c d
+      (Just c, Right s, Right d) -> (tfun a2) s c d
+      (Nothing, Left s, Right d) ->
+        if (final a1) s && (sta
+}
+
+-- if ∃st ∈ (start a1) and st ∈ (final a1) then
+--   (start a1) ++ 
+-- else
+--   start a1
diff --git a/clash/Overflow.hs b/clash/Overflow.hs
new file mode 100644
index 0000000..ee7608e
--- /dev/null
+++ b/clash/Overflow.hs
@@ -0,0 +1,22 @@
+module OverflowExp where
+
+import Clash.Prelude
+
+topFn :: () -> () -> ((), Word)
+--topFn _ _ = ((), 18446744073709551615)
+topFn _ _ = ((), 18446744073709551616)
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System ()
+  -> Signal System Word
+topEntity = exposeClockResetEnable $ mealy topFn ()
+
+{-
+      // Outputs
+    , output wire [63:0] result
+    );
+  assign result = 64'd18446744073709551615;
+-}
diff --git a/clash/VecInput.hs b/clash/VecInput.hs
new file mode 100644
index 0000000..4cbab4a
--- /dev/null
+++ b/clash/VecInput.hs
@@ -0,0 +1,26 @@
+module ListState where
+  
+import Clash.Prelude
+
+tf
+  :: (KnownNat n, Ord a, Num a)
+  => ()
+  -> Vec (n+1) a
+  -> ((), Bool)
+tf s i =
+  if sum i > 10 then ((), True)
+  else ((), True)
+
+tfun
+  :: SystemClockResetEnable
+  => Signal System (Vec 2 Int)
+  -> Signal System Bool
+tfun = mealy tf ()
+          
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System (Vec 2 Int)
+  -> Signal System Bool
+topEntity = exposeClockResetEnable tfun
diff --git a/clash/fsm.hs b/clash/fsm.hs
new file mode 100644
index 0000000..3207233
--- /dev/null
+++ b/clash/fsm.hs
@@ -0,0 +1,41 @@
+module FSM where
+
+import Clash.Prelude
+import qualified Prelude
+
+data Point a =
+    Pt (a -> Bool)
+  | Yes
+  | No
+
+getPtFn :: Point a -> (a -> Bool)
+getPtFn p = case p of
+    Pt f -> f
+    Yes -> \x -> True
+    No -> \x -> False
+-- getPtFn (Pt f) = f
+-- getPtFn Yes = \x -> True
+-- getPtFn No = \x -> False
+
+
+type State = [Point]
+
+-- [Pt 0, Pt 1, Pt 2]
+points = map Pt $ map (==) [0, 1, 2]
+
+-- ssyes =
+--   [[Pt 1, Pt 2, Yes],
+--    [Yes],
+--    [Pt 2, Yes]]
+ssyes =
+  [[points!!1, points!!2, Yes],
+   [Yes],
+   [points!!2, Yes]]
+
+sno = [No] >>= replicate 3
+
+one
+  :: Eq a
+  => Point
+  -> a
+  -> State
diff --git a/clash/list-to-vec.hs b/clash/list-to-vec.hs
new file mode 100644
index 0000000..964d524
--- /dev/null
+++ b/clash/list-to-vec.hs
@@ -0,0 +1,26 @@
+import Clash.Prelude
+import Clash.Sized.Vector
+import Clash.Explicit.Testbench
+
+sz = 3
+
+l :: [Int]
+l = [0, 1, 2, 3, 4, 5]
+
+v = unsafeFromList l :: Vec sz Int      
+
+
+{-
+list-to-vec.hs:10:5-20: error: …
+    • No instance for (KnownNat sz1)
+        arising from a use of ‘unsafeFromList’
+      Possible fix:
+        add (KnownNat sz1) to the context of
+          an expression type signature:
+            forall (sz1 :: Nat). Vec sz1 Int
+    • In the expression: unsafeFromList l :: Vec sz Int
+      In an equation for ‘v’: v = unsafeFromList l :: Vec sz Int
+   |
+Compilation failed.
+-}
+  
diff --git a/clash/strict-constr.hs b/clash/strict-constr.hs
new file mode 100644
index 0000000..4deef2c
--- /dev/null
+++ b/clash/strict-constr.hs
@@ -0,0 +1,86 @@
+import Clash.Prelude
+-- import Clash.Explicit.Testbench
+
+data SList a
+  = SNil
+  | SCons !a !(SList a)
+  deriving (NFDataX, Generic)
+
+isSNil :: SList a -> Bool
+isSNil sl = case sl of
+  SNil -> True
+  _ -> False
+
+tf :: SList Int -> Int -> (SList Int, Maybe Bool)
+tf s inp = case s of
+  SCons _ s' -> (s', Just False)
+  SNil -> (SNil, Just True)
+
+mon
+  :: SystemClockResetEnable
+  => Signal System Int
+  -> Signal System (Maybe Bool)
+mon = mealy tf SNil
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System Int
+  -> Signal System (Maybe Bool)
+topEntity = exposeClockResetEnable mon
+
+{-
+
+GHC: Setting up GHC took: 0.662s
+GHC: Compiling and loading modules took: 1.062s
+Clash: Parsing and compiling primitives took 0.176s
+GHC+Clash: Loading modules cumulatively took 2.192s
+Clash: Compiling Main.topEntity
+Clash.Normalize.Transformations.Inline(523): InlineNonRep: c$Main.mon_ds[19] already inlined 20 times in: Main.mon[8214565720323816306]
+. The type of the subject is:
+
+  GHC.Tuple.(,)[3746994889972252676]
+    (Main.SList[8214565720323816301]
+       GHC.Types.Int[3674937295934324766])
+    (GHC.Maybe.Maybe[3674937295934324792]
+       GHC.Types.Bool[3674937295934324744])
+
+Function Main.mon[8214565720323816306] will not reach a normal form and compilation 
+might fail.
+
+Run with '-fclash-inline-limit=N' to increase the inline limit to N.
+Clash.Normalize.Transformations.Inline(523): InlineNonRep: c$Main.mon_ds[19] already inlined 20 times in: Main.mon[8214565720323816306]
+. The type of the subject is:
+
+  GHC.Tuple.(,)[3746994889972252676]
+    (Main.SList[8214565720323816301]
+       GHC.Types.Int[3674937295934324766])
+    (GHC.Maybe.Maybe[3674937295934324792]
+       GHC.Types.Bool[3674937295934324744])
+
+Function Main.mon[8214565720323816306] will not reach a normal form and compilation 
+might fail.
+
+Run with '-fclash-inline-limit=N' to increase the inline limit to N.
+Clash.Normalize.Transformations.Inline(523): InlineNonRep: c$Main.mon_ds[19] already inlined 20 times in: Main.mon[8214565720323816306]
+. The type of the subject is:
+
+  GHC.Tuple.(,)[3746994889972252676]
+    (Main.SList[8214565720323816301]
+       GHC.Types.Int[3674937295934324766])
+    (GHC.Maybe.Maybe[3674937295934324792]
+       GHC.Types.Bool[3674937295934324744])
+
+Function Main.mon[8214565720323816306] will not reach a normal form and compilation 
+might fail.
+
+Run with '-fclash-inline-limit=N' to increase the inline limit to N.
+
+<no location info>: error:
+    Clash error call:
+    Clash.Core.Type(395): Report as bug: not a FunTy
+    CallStack (from HasCallStack):
+      error, called at src/Clash/Core/Type.hs:395:20 in clash-lib-1.6.3-4vM2gwSsWPHufxjlmfu4S:Clash.Core.Type
+
+-}
diff --git a/clash/strict-constrv2.hs b/clash/strict-constrv2.hs
new file mode 100644
index 0000000..13648f5
--- /dev/null
+++ b/clash/strict-constrv2.hs
@@ -0,0 +1,31 @@
+import Clash.Prelude
+-- import Clash.Explicit.Testbench
+
+data SList (n :: Nat) a
+  = SNil
+  | SCons !a !(SList a)
+  deriving (NFDataX, Generic)
+
+isSNil :: SList a -> Bool
+isSNil sl = case sl of
+  SNil -> True
+  _ -> False
+
+tf :: SList Int -> Int -> (SList Int, Maybe Bool)
+tf s inp = case s of
+  SCons _ s' -> (s', Just False)
+  SNil -> (SNil, Just True)
+
+mon
+  :: SystemClockResetEnable
+  => Signal System Int
+  -> Signal System (Maybe Bool)
+mon = mealy tf SNil
+
+topEntity
+  :: Clock System
+  -> Reset System
+  -> Enable System
+  -> Signal System Int
+  -> Signal System (Maybe Bool)
+topEntity = exposeClockResetEnable mon
diff --git a/coq/mathcomp/hello-ssreflect.v b/coq/mathcomp/hello-ssreflect.v
new file mode 100644
index 0000000..1377df7
--- /dev/null
+++ b/coq/mathcomp/hello-ssreflect.v
@@ -0,0 +1,23 @@
+From mathcomp Require Import all_ssreflect.
+
+Fixpoint twice (n: nat): nat :=
+  if n is n'.+1 then (twice n').+2 else 0.
+
+Lemma twiceDouble: forall n:nat,
+  twice (2 * n) = twice n + twice n.
+Proof.
+  elim=> [|n IHn].
+  - done.
+  - rewrite !addSn.
+    rewrite -/twice.
+    rewrite mulnS.
+    rewrite -IHn.
+Abort.
+
+Context (A B C: Prop).
+
+Lemma HilbertS: (A -> B -> C) -> (A -> B) -> A -> C.
+Proof.
+  move=> Habc Hab.
+  move: Habc.
+
diff --git a/coq/mathcomp/hello.v b/coq/mathcomp/hello.v
new file mode 100644
index 0000000..823b1f8
--- /dev/null
+++ b/coq/mathcomp/hello.v
@@ -0,0 +1,39 @@
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import fintype div tuple bigop prime finset fingroup.
+From mathcomp Require Import ssralg poly polydiv morphism action finalg zmodp.
+From mathcomp Require Import cyclic center pgroup abelian matrix mxpoly vector.
+From mathcomp Require Import falgebra fieldext separable galois.
+From mathcomp Require ssrnum ssrint algC cyclotomic.
+
+(* Identity of a group *)
+Check 1%g.
+Check 1%R.
+Check ringType.
+Check fieldType.
+(* Got +1,+2,+3,+4 and -1,-2 *)
+Compute 3.+4.
+(* = 7 : nat *)
+
+Print injective.
+(*
+injective = 
+fun (rT aT : Type) (f : aT -> rT) =>
+forall x1 x2 : aT, f x1 = f x2 -> x1 = x2
+     : forall rT aT : Type, (aT -> rT) -> Prop
+*)
+
+(* Check fieldExtType. *)
+Locate "0".
+Check 0%g.
+(* Check R. *)
+
+(* Factorial *)
+Compute 0`!.    (* = 1 : nat *)
+Compute 1`!.    (* = 1 : nat *)
+Compute 2`!.    (* = 2 : nat *)
+Compute 3`!.    (* = 6 : nat *)
+Compute 4`!.    (* = 24 : nat *)
+
+(* Summation. ie, Σ  *)
+Compute \sum_ (1 <= i < 5) i.       (* 1+2+3+4+5 *)
+Compute \sum_ (1 <= i < 3) (2*i).   (* 2*(1+2+3) *)
diff --git a/coq/mathcomp/hello2.v b/coq/mathcomp/hello2.v
new file mode 100644
index 0000000..34cabf3
--- /dev/null
+++ b/coq/mathcomp/hello2.v
@@ -0,0 +1,45 @@
+From mathcomp Require Import all_ssreflect all_algebra.
+
+Print negbK.
+Check negbK.      (* involutive negb *)
+Print involutive. (* f (f x) = x *)
+Print cancel.     (* f g such that f (g x) = x *)
+
+Locate "~~".      (* negb *)
+Locate "~".       (* Could be 'not' *)
+
+Goal forall b: bool,
+  ~~ (~~ b) = b.
+Proof.
+  intro b.
+  case: b.
+  by [].
+  by [].
+Show Proof.
+Restart.
+  intro b.
+  by case: b.
+  (* Or 'by [case: b].' *)
+Qed.
+
+Fixpoint multn (n m: nat): nat :=
+  if n is n'.+1 then m + multn n' m
+  else 0.
+Compute multn 3 4.
+(* = 12 : nat *)
+
+Goal forall n m: nat,
+  (n * m == 0) = (n == 0) || (m == 0).
+Proof.
+  intros n m.
+  case: n => [|n] //.
+  case: m => [|m]; last first => //. (* Good practice to get rid of easy goal first' *)
+  by rewrite muln0.
+Qed.
+
+Goal forall n p:nat,
+  prime p -> p %| (n`! + 1) -> n < p.
+Proof.
+  move => n p prime_p.
+  apply: contraLR.
+
diff --git a/coq/mathcomp/let-hello.v b/coq/mathcomp/let-hello.v
new file mode 100644
index 0000000..cc733f3
--- /dev/null
+++ b/coq/mathcomp/let-hello.v
@@ -0,0 +1,22 @@
+From mathcomp Require Import all_ssreflect all_algebra.
+
+(* Inductive point: Type := *)
+(* | Point (x y z: nat). *)
+
+(* Definition getX (p: point): nat := *)
+(*   let: Point x _ _ := p in x. *)
+(* Compute getX (Point 1 2 3). *)
+(* (1* = 1 : nat *1) *)
+
+Print matrix.
+
+Variant point: Type :=
+| Point (x y z: nat).
+
+Compute 3.+1.
+(* = 4 : nat *)
+
+Check point_rect.
+Check point_ind.
+Check point_rec.
+Check point_sind.
diff --git a/coq/mathcomp/reflect.v b/coq/mathcomp/reflect.v
new file mode 100644
index 0000000..2ee42d3
--- /dev/null
+++ b/coq/mathcomp/reflect.v
@@ -0,0 +1,146 @@
+(* From Chapter-5 of mathcomp book *)
+From mathcomp Require Import all_ssreflect.
+
+Lemma test_reflect (b: bool) (P: Prop):
+  reflect P b -> P \/ ~P.
+Proof.
+  case.
+    by move=> H; left.
+    by move=> H; right. (* ✓ *)
+Restart.
+  by case; [left | right].
+Qed.
+
+Lemma andP (b1 b2: bool): reflect (b1 /\ b2) (b1 && b2).
+Proof.
+  case: b1.
+    case b2.
+      by left.
+      right.
+      move=> [l r].
+      by [].
+    case b2.
+      right.
+      by move=> [l r].
+      right.
+      move=> [l _].
+      by [].  (* ✓ *)
+Restart.
+  case: b1; case b2.
+  by left.
+  by right; by move=>[l r].
+  by right; by move=>[l r].
+  by right; by move=>[l r].  (* ✓ *)
+Restart.
+  case: b1; case b2.
+  by left.
+  all: by right; by move=>[l r]. (* ✓ *)
+(* Restart. *)
+(*   by case: b1; case b2; *)
+(*     [left | right => //= [l r]]. *)
+Qed.
+
+Lemma orP (b1 b2: bool): reflect (b1 \/ b2) (b1 || b2).
+Proof.
+  case: b1; case b2.
+  by left; left.
+  by left; left.
+  by left; right.
+  right.
+  move=> [l | r].
+  by case b2.
+  by case b2. (* ✓ *)
+(* Restart. *)
+(*   case: b1; case b2; [ [left; [left | right]] | right]. *)
+(* Restart. *)
+(*   case: b1; case b2; *)
+(*     [left; by [move | left | right]]. *)
+Qed.
+
+Lemma implyP (b1 b2: bool): reflect (b1 -> b2) (b1 ==> b2).
+Proof.
+  case b1; case b2.
+  by left.
+  right.
+  Search (_ -> _).
+  apply/Bool.ReflectT.
+  apply/Bool.ReflectT.
+  apply/Bool.ReflectT.
+  apply/Bool.ReflectT.
+  apply/Bool.ReflectT.
+  apply/Bool.ReflectT.
+  apply/Bool.ReflectT.
+  apply/Bool.ReflectT.
+  apply/Bool.ReflectT.
+  apply/Bool.ReflectT.
+  move => H.
+  
+  rewrite /(_ isT).
+Abort.
+
+Lemma nat_inj_eq {A: Type} (f: A -> nat) (x y: A):
+  injective f -> reflect (x=y) (eqn (f x) (f y)).
+Proof.
+  move=> f_inj.
+  Check eqnP.
+  Check iffP.
+  Check iffP eqnP.
+  apply: (iffP eqnP).
+  apply: f_inj.
+  Search (_ = _ -> _ = _).
+  (* congruence. *)
+  apply: congr1. (* ✓ *)
+Restart.
+  move => f_inj; apply: (iffP eqnP); [apply: f_inj | apply: congr1].
+Qed.
+
+Lemma eqnP (n m: nat): reflect (n = m) (eqn n m).
+Proof.
+  apply: (iffP idP).
+Abort. (* TODO *)
+  
+Lemma example1 (n m k: nat):
+  k <= n ->
+  (n <= m) && (m <= k) ->
+  n = k.
+Proof.
+  move=> lekn.
+Undo.
+  move=> lekn /andP [lenm lemk].
+Undo.
+  move=> lekn /andP [/eqnP lenm lemk].
+Abort. (* TODO *)
+
+Lemma leq_total (n m: nat): (n <= m) || (n >= m).
+Proof.
+Abort.
+
+Locate "_ -> _ ".
+  
+Lemma example2 (a b: bool): a && b ==> (a == b).
+Proof.
+  case: andP => [ab | nab].
+  Search (reflect (_ = _) _).
+  apply/addbP.
+Abort.
+
+(* Euclidean division example *)
+Definition edivn_rec (d: nat): nat -> nat -> nat * nat :=
+  fix loop (m q: nat): nat * nat := 
+    if m-d is m'.+1 then loop m' q.+1
+    else (q, m).
+Definition edivn (m d: nat): nat*nat :=
+  if d>0 then edivn_rec d.-1 m 0 
+  else (0, m).
+
+(* Follows from definition but useful to have better control over level of
+* unfolding in later proof *)
+Lemma edivn_recE (d m q: nat):
+  edivn_rec d m q =
+    if m-d is m'.+1 then edivn_rec d m' q.+1
+    else (q, m).
+Proof. by case: m. Qed.
+
+Lemma edivnP (m d: nat) (ed := edivn m d):
+  ((d>0) ==> (ed.2 < d)) && (m == ed.1 * d + ed.2).
+Proof.
diff --git a/coq/mathcomp/sumj.v b/coq/mathcomp/sumj.v
new file mode 100644
index 0000000..6e0e693
--- /dev/null
+++ b/coq/mathcomp/sumj.v
@@ -0,0 +1,59 @@
+From mathcomp Require Import all_ssreflect.
+
+Fail Compute \sum_(0 < i < 12.*2 | odd i) i.
+(* Fail Compute \sum_i(0 < i < 12.*2 | odd i) i. *)
+
+From CoqEAL Require Import hrel param refinements trivial_seq.
+From CoqEAL Require Import binnat binint seqpoly binord seqmx.
+Check refines_rel.
+
+Check 3.-tuple.
+Search ".-tuple".
+Print nil_tuple.
+Check tval.
+
+Definition foo (n:nat): n.-tuple bool -> seq bool -> Type :=
+  fun btup bseq => tval btup = bseq.
+
+
+Lemma sum_odd_n (n: nat): \sum_(0 <= i < n.*2 | odd i) i = n^2.
+Proof.
+  rewrite unlock.
+  Fail rewrite bigop_unlock.
+Restart.
+  elim: n.
+  by rewrite unlock /=.
+  rewrite unlock /=.
+Restart.
+  elim: n => [ | n IH].
+    rewrite double0.
+      rewrite -mulnn muln0.
+      by rewrite big_geq.
+    Check big_ord_recr.
+    Search "big" nat.
+    rewrite -big_ord_recr.
+    rewrite (@big_cat_nat _ _ _ (n.*2)).
+    rewrite big_ord_recr.
+    
+
+  (* rewrite unlock. *)
+  Search bigop "_ind".
+  Search bigop "_rec".
+  (* elim/big_ind2. *)
+  (* Search reducebig. *)
+  (* rewrite -bigop_unlock. *)
+  (* move=> n. *)
+Abort.
+
+
+
+Lemma sum_odd_n (n: nat) : \sum_(0 <= i < n.*2 | odd i) i = n^2.
+Proof.
+  elim: n => [//=|n IH]; first by rewrite double0 -mulnn muln0 big_geq.
+  rewrite (@big_cat_nat _ _ _ n.*2) //=; last by rewrite -!addnn leq_add.
+  rewrite IH -!mulnn mulSnr mulnSr -addnA.
+  congr (_ + _).
+  rewrite big_ltn_cond ?ifF ?odd_double //.
+  rewrite big_ltn_cond /ifT ?oddS ?odd_double //=.
+  by rewrite big_geq ?addn0 -addnn addnS // -addnn addSn.
+Qed.
diff --git a/coq/matrix-as-list.v b/coq/matrix-as-list.v
new file mode 100644
index 0000000..62a1f7d
--- /dev/null
+++ b/coq/matrix-as-list.v
@@ -0,0 +1,64 @@
+Require Import List.
+Import ListNotations.
+
+Definition lstHd {A: Type} (ls: list A)
+  : length ls <> 0 -> A.
+Proof.
+  refine (
+    match ls with
+    | [] => fun pf => _
+    | x :: _ => fun _ => x
+    end).
+  contradiction.
+Defined.
+
+Module Vec.
+  Definition t (A: Type) (sz: nat): Type :=
+    {ls: list A | length ls = sz}.
+  
+  Context {A: Type} {sz: nat}.
+
+  Definition hd (v: t A (S sz)): A.
+    refine (
+      match v with
+      | exist _ l pf => _
+      end).
+    induction l.
+    - discriminate pf.
+    - exact a.
+  Show Proof.
+  Defined.
+
+  Definition tl (v: t A (S sz)): t A sz.
+    refine (let (l, _) := v in _).
+    induction l.
+    - discriminate e.
+    - simpl in e.
+      Search (S _ = S _).
+      rewrite (PeanoNat.Nat.succ_inj (length l) sz) in e.
+      + 
+      f_equal in e.
+      exact (exist _ l .
+Defined.
+
+  Fixpoint zip {A B: Type} {n:nat}
+    (av: Vec A n) (bv: Vec B n): Vec (A*B) n :=
+    match av with
+    | [] => []
+    | a::av' => 
+
+  Definition dotProduct {n:nat}
+    (v1 v2: Vec bool n): csr.A :=
+    let v12 := zip v1 v2 in
+    let ires := Vector.map (fun '(a, b) => csr.multn a b) v12 in
+    fold_right (fun elem res => csr.addtn elem res) ires csr.zero.
+End Vec.
+Definition 
+
+        
+
+  match av in Vec _ n
+    return Vec B n -> Vec (A*B) n with
+  | [] => fun _ => []
+  | a::av' => fun bv => (a, Vector.hd bv) :: zip av' (Vector.tl bv)
+  end bv.
diff --git a/coq/notations.v b/coq/notations.v
new file mode 100644
index 0000000..ad91779
--- /dev/null
+++ b/coq/notations.v
@@ -0,0 +1,11 @@
+Module FooMod.
+  #[local] Notation "⊥" := false.
+
+  Check ⊥.  (* ⊥ : bool *)
+
+End FooMod.
+Disable Notation "+" (all).
+
+Import FooMod.
+Compute ⊥.
+(* Syntax Error: Lexer: Undefined token *)
diff --git a/coq/red-black-tree.v b/coq/red-black-tree.v
new file mode 100644
index 0000000..8c36951
--- /dev/null
+++ b/coq/red-black-tree.v
@@ -0,0 +1,9 @@
+Inductive colour: Set := Red | Black.
+
+(* colour of root, black height *)
+Inductive tree {A:Type}: colour -> nat -> Type :=
+| Empty: tree Black 0
+| RNode: forall n:nat,
+    A -> tree Black n -> tree Black n -> tree Red n
+| BNode: forall (n:nat) (c1 c2:colour),
+    A -> tree c1 n -> tree c2 n -> tree Black n.
diff --git a/coq/reflect-even.v b/coq/reflect-even.v
new file mode 100644
index 0000000..1d89f00
--- /dev/null
+++ b/coq/reflect-even.v
@@ -0,0 +1,265 @@
+Inductive even: nat -> Prop :=
+| EvenO: even 0
+| EvenS: forall n:nat,
+    odd n -> even (S n)
+with odd: nat -> Prop :=
+| OddS: forall n:nat,
+    even n -> odd (S n).
+
+(*
+Print even_ind.
+Scheme even_ind' := Induction for even Sort Prop.
+Print even_ind'.
+*)
+
+Fixpoint evenb (n:nat): bool :=
+  match n with
+  | O => true
+  | S n' => oddb n'
+  end
+with oddb (n:nat): bool :=
+  match n with
+  | O => false
+  | S n' => evenb n'
+  end.
+
+Lemma foo: forall n:nat,
+  evenb n = true ->  oddb (S n) = true.
+Proof.
+  intros n H.
+  induction n.
+  - reflexivity.
+  - simpl.
+Abort.
+
+Definition evenBP (n: nat): (evenb n = true <-> even n) /\ (oddb n = true <-> odd n).
+Proof.
+  induction n.
+  - simpl.
+    split.
+    + split; intro H; constructor.
+    + split; intro H; inversion H.
+  - destruct IHn as [[H0 H1] [H2 H3]].
+    simpl.
+    split.
+    + split.
+      * intro H.
+        constructor.
+        exact (H2 H).
+      * intro H.
+        apply H3.
+
+Definition evenBP (n: nat): evenb n = true -> even n.
+Proof.
+  intros H.
+  induction n.
+  - constructor.
+  - apply EvenS.
+(*
+1 subgoal
+
+n : nat
+H : evenb (S n) = true
+IHn : evenb n = true -> even n
+
+========================= (1 / 1)
+
+odd n
+*)
+
+    destruct n.
+    + discriminate.
+    + simpl in H.
+      simpl.
+
+
+
+(***************************************)
+
+
+Inductive even: nat -> Prop :=
+| EvenO: even 0
+| EvenS: forall n:nat,
+    even n -> even (S (S n)).
+
+Example even256: even 256.
+Proof.
+  repeat constructor.
+Show Proof.
+Qed.
+
+Fixpoint evenb (n:nat): bool :=
+  match n with
+  | O => true
+  | S O => false
+  | S (S n') => evenb n'
+  end.
+
+Fixpoint evenBP (n: nat): evenb n = true -> even n.
+Proof.
+  intros H.
+  destruct n as [| [|n]].
+  - constructor.
+  - inversion H. 
+  - constructor.
+    simpl in H.
+    exact (evenBP n H).
+Qed.
+
+Example even256': even 256.
+Proof.
+  apply (evenBP 256).
+  simpl; reflexivity.
+Show Proof.
+Qed.
+
+(* ✓ *)
+
+
+(***************************************)
+
+Inductive even: nat -> Prop :=
+| EvenO: even 0
+| EvenS: forall n:nat,
+    even n -> even (S (S n))
+with odd: nat -> Prop :=
+| Odd1: odd 1
+| OddS: forall n:nat,
+    even (S n) -> odd n.
+
+Fixpoint evenb (n:nat): bool :=
+  match n with
+  | O => true
+  | S O => false
+  | S (S n') => evenb n'
+  end.
+
+Example even256: even 256.
+Proof.
+  repeat constructor.
+Show Proof.
+Qed.
+
+Lemma foo: forall n:nat,
+  evenb (S n) = negb (evenb n).
+Proof.
+  intros n.
+  induction n.
+  - simpl; reflexivity.
+  - rewrite IHn.
+    Require Import Bool.
+    rewrite negb_involutive.
+    simpl.
+    reflexivity.
+Qed.
+
+Theorem evenBP: forall n:nat,
+  evenb n = true -> even n.
+Proof.
+  intros n H.
+  induction n.
+  - constructor.
+  - 
+
+
+Require Import Bool.
+Print reflect.
+
+
+
+
+
+
+
+
+
+
+
+(*********************************************)
+
+
+Inductive even: nat -> Prop :=
+| EvenO: even 0
+| EvenSS: forall n:nat,
+    even n -> even (S (S n)).
+
+(*
+Inductive odd: nat -> Prop :=
+| Odd1: odd (S O)
+| OddSS: forall n:nat,
+    odd n -> odd (S (S n)).
+
+Lemma evenSodd: forall n:nat,
+  even n -> odd (S n).
+Proof.
+  intros n H.
+  induction n.
+  - constructor.
+  - apply OddSS.
+*)
+
+Lemma evenS: forall n:nat,
+  even n -> ~(even (S n)).
+Proof.
+  intros n H.
+  induction n.
+  - intro HH.
+
+Abort.
+
+Lemma even256: even 256.
+Proof.
+  repeat constructor.
+Show Proof.
+Qed.
+
+Fixpoint evenb (n:nat): bool :=
+  match n with
+  | O => true
+  | S O => false
+  | S (S n') => evenb n'
+  end.
+
+Require Import Arith.
+Print Nat.even.
+Print Nat.Even.
+Search (Nat.Even).
+Print Nat.even_spec.
+
+Axiom foo1: forall n:nat,
+  ~(even n) -> even (S n).
+Axiom foo1': forall n:nat,
+  (even n) -> ~(even (S n)).
+
+Axiom foo2: forall n:nat,
+  evenb n = true -> evenb (S n) = false.
+
+Theorem evenBP: forall n:nat,
+  evenb n = true -> even n.
+Proof.
+  intros n H.
+  induction n.
+  - constructor.
+  - 
+(*
+#+BEGIN_OUTPUT (Goal)
+1 subgoal
+
+n : nat
+H : evenb (S n) = true
+IHn : evenb n = true -> even n
+
+========================= (1 / 1)
+
+even (S n)
+#+END_OUTPUT (Goal) *)
+
+    destruct IHn.
+    pose proof (foo2 (S n) H).
+    inversion H.
+   
+apply foo1.
+intro HH.
+apply IHn.
+    
+o
diff --git a/coq/roman.v b/coq/roman.v
new file mode 100644
index 0000000..e1c23dd
--- /dev/null
+++ b/coq/roman.v
@@ -0,0 +1,103 @@
+(* ** Strictly decreasing [list nat] *)
+
+(*
+l MAX: non empty list
+
+l n
+| start: l n
+| cons: n >= m -> 
+| 
+
+repeat:
+| Repeat: forall n>1 ∧ n<4, tok -> repeat 
+
+repeat:
+| R1one: one -> repeat
+| R1oth: other -> repeat
+| R2: other -> repeat
+| R3: other -> repeat.
+
+ *)
+Inductive foo: nat -> nat -> Type :=
+| Foo: forall n m:nat, n > m -> foo n m.
+
+Inductive bar: nat -> Type :=
+| Bar: forall n:nat, bar n.
+
+Inductive decrList: nat -> Type :=
+| DEmpty: decrList 0
+| DCons: forall n m:nat,
+    foo n m -> bar m -> decrList n -> decrList m.
+
+Check DCons 0 0 (Foo _ _ _) (Bar _) DEmpty.
+Check DCons 3 0 (Foo _ _ _) (Bar _).
+
+
+(*
+pre     := I | X | C
+one     := D | L | V
+thrice  := M | pre
+all     := M | pre | once
+
+-----
+
+subpair := IV | IX
+           XL | XC
+           CD | CM
+one     := D | L | V
+
+No symbol occurs more than thrice consecutively: https://www.numere-romane.ro/rule2-repetition-of-basic-symbols-in-roman-numerals.php?lang=en
+
+MCX use instead of:
+'M, C, and X cannot be equalled or exceeded by smaller denominations.'
+ - X: VV
+ - M: C * 10 ✓
+ - C: X * 10 ✓
+
+num := all
+
+additive notation, subtractive notation
+ *)
+
+Inductive other: Set := V | L | D | M.
+Inductive subpre := I | X | C.
+Inductive tok: Set :=
+| Other: other -> tok
+| SubPre: subpre -> tok.
+
+Definition val (n:tok): nat :=
+  match n with
+  | Other x =>
+      match x with
+      | V => 5
+      | L => 50
+      | D => 500
+      | M => 1000
+      end
+  | SubPre x =>
+      match x with
+      | I => 1
+      | X => 10
+      | C => 100
+      end
+  end.
+
+
+Inductive rnumSub: Set :=
+| RSub: subpre -> tok -> rnumSub.
+
+Inductive rnum: Type :=
+| RNil: rnum
+| RCons: other -> rnum -> rnum
+| RSubCons: rnumSub -> rnum -> rnum.
+
+(*
+CDXCIX
+
+
+ *)
+Example eg1 := RSub I (SubPre X). (* IX *)
+Example eg2 := RSub X (SubPre C). (* XC *)
+Example eg3 := RSub C (Other D). (* XC *)
+
+
diff --git a/coq/utlc.v b/coq/utlc.v
new file mode 100644
index 0000000..db6182a
--- /dev/null
+++ b/coq/utlc.v
@@ -0,0 +1,15 @@
+Inductive term: Type :=
+| Var: nat -> term
+| Abs: term -> term
+| App: term -> term -> term.
+
+Notation "'λ' body" := (Abs body) (at level 60, right associativity).
+Notation "'❨' t1 t2 '❩'" := (App t1 t2) (at level 50).
+Notation "'`' varidx " := (Var varidx) (at level 40).
+
+Check λ`0.
+Check λ❨`0 `0❩.
+Check ❨λ❨`0 `0❩ λ❨`0 `0❩❩.
+
+Require Import List.
+Search In.
diff --git a/haskell/ccc.hs b/haskell/ccc.hs
new file mode 100644
index 0000000..e7f0f45
--- /dev/null
+++ b/haskell/ccc.hs
@@ -0,0 +1,52 @@
+-- https://github.com/compiling-to-categories/concat/blob/84900a2937cdfdfe7fcc773f18b4a4ddcf5251ee/classes/src/ConCat/Category.hs
+
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RecursiveDo #-}
+{-# LANGUAGE NoStarIsType #-}
+
+infixr 9 ∘
+infixr 3 △
+
+class Category k where
+  id :: k a a
+  (∘) :: k b c -> k a b -> k a c
+
+class Category k => Cartesian k where
+  (△) :: k a b -> k a c -> k a (b,c)
+  -- I wonder why ex{l,r} was chosen as the name
+  exl :: k (a,b) a
+  exr :: k (a,b) b
+
+instance Category (->) where
+  id = \x -> x
+  g ∘ f = \x -> g (f x)
+
+instance Cartesian (->) where
+  f △ g = \x -> (f x, g x)
+  exl = \(a, _) -> a
+  exr = \(_, b) -> b
diff --git a/haskell/cmd-args.hs b/haskell/cmd-args.hs
new file mode 100644
index 0000000..2b41e51
--- /dev/null
+++ b/haskell/cmd-args.hs
@@ -0,0 +1,21 @@
+import System.Environment
+
+main = do
+    args <- getArgs
+    progName <- getProgName
+    putStrLn "Prog name:"
+    putStrLn progName
+    putStrLn "Args:"
+    mapM putStrLn args  
+
+{-
+./a.out hello world
+
+-----
+
+Prog name:
+a.out
+Args:
+hello
+world
+-}
diff --git a/haskell/datatypes-a-la-carte.hs b/haskell/datatypes-a-la-carte.hs
new file mode 100644
index 0000000..9e12a1f
--- /dev/null
+++ b/haskell/datatypes-a-la-carte.hs
@@ -0,0 +1,28 @@
+data Expr f = In (f (Expr f))
+data Val e = ValC Int
+type IntExpr = Expr Val
+
+-- λ> In (ValC 3)
+-- In (ValC 3) :: Expr Val
+
+data Add e = AddC e e
+type AddExpr = Expr Add 
+
+-- In (_: Add (Expr Add))
+-- In $ AddC (_: Expr Add) (_: Expr Add)
+
+-- λ> In (AddC (In (ValC 2)) (In (ValC 3)))
+
+data (f :+: g) e
+  = Inl (f e)
+  | Inr (g e)
+
+type IntAddExpr = Expr (Val :+: Add)
+-- In (Inr _)
+-- In (Inr AddC (In (Inl (ValC 2)))
+--              (In (Inl (ValC 3))))
+
+
+a = In (Inr (AddC (In (Inl (ValC 2))) (In (Inl (ValC 3)))))
+b = In $ Inr $ AddC (In (Inl (ValC 2))) (In (Inl (ValC 3)))
+c = In $ Inr $ AddC (In $ Inl $ ValC 2) (In $ Inl $ ValC 3)
diff --git a/haskell/dfa.hs b/haskell/dfa.hs
new file mode 100644
index 0000000..bee88d3
--- /dev/null
+++ b/haskell/dfa.hs
@@ -0,0 +1,25 @@
+import Data.Set
+
+data DFA = DFA {
+   states :: Set String
+ , sigma  :: Set String
+ , tf     :: String -> String -> String
+ , strt  :: String
+ , final  :: Set String
+}
+
+instance Show DFA where
+  show x = show states ++
+           show sigma ++
+           "tf" ++ strt ++
+           show final
+
+tf1 "q0" "1" = "q1"
+tf1 "q1" "0" = "q0"
+
+a = fromList [1,1,2,3]
+dfa = DFA (fromList ["q0", "q1", "q2", "q3"])
+          (fromList ["0", "1"])
+          tf1
+          "q0"
+          (fromList ["q3"])
diff --git a/haskell/hello.hs b/haskell/hello.hs
new file mode 100644
index 0000000..5af5cab
--- /dev/null
+++ b/haskell/hello.hs
@@ -0,0 +1,4 @@
+main = do
+    putStrLn "Enter your name: "
+    name <- getLine
+    putStrLn ("Hi " ++ name ++ "! Good day.")
diff --git a/haskell/hlist0.hs b/haskell/hlist0.hs
new file mode 100644
index 0000000..e9d45eb
--- /dev/null
+++ b/haskell/hlist0.hs
@@ -0,0 +1,30 @@
+import Data.Dynamic
+-- import Data.Maybe
+
+type Result = [Row]
+type Row = HList
+type HList = [Dynamic]
+
+angus = [ toDyn 42, toDyn True]
+
+--hCount :: Typeable a => HList -> [a]
+
+-- Haskell record
+data Unpriced = Unpriced { key :: Integer
+                         , name :: String }
+
+angus = Unpriced { key = 42
+                 , name = "angus" }
+
+-- > key angus
+-- 42
+-- > name angus
+-- angus
+
+-- Update record
+notAngus = angus { key = 32 }
+-- > key angus
+-- 32
+-- > name angus
+-- angus
+
diff --git a/haskell/parser-monad.hs b/haskell/parser-monad.hs
new file mode 100644
index 0000000..b593508
--- /dev/null
+++ b/haskell/parser-monad.hs
@@ -0,0 +1,114 @@
+-- monadic parsing
+-- https://bitbucket.org/piyush-kurur/functional-programming/raw/a2b004847c92f88aa6ae3073f4d230b3a770cad8/notes/live.org
+-- Graham Hutton book (2e)
+
+import Control.Applicative
+import Data.Char
+
+-- | Result of parsing
+data Result a = OK a String  -- ^ Parsed data
+              | Error String -- ^ error message
+
+-- | Parser capable of parsing a value of type `a`
+newtype Parser a = Parser {runParser :: String -> Result a}
+
+instance Functor Result where
+  -- fmap :: (a -> b) -> Result a -> Result b
+  fmap f (OK a s) = OK (f a) s
+  fmap _ (Error msg) = Error msg
+  --fmap _ obj = obj
+
+instance Applicative Result where
+  -- pure :: a -> Result a
+  pure x = OK x ""
+
+  -- (<*>) :: Result (a -> b) -> Result a -> Result b
+  (OK fa2b rem) <*> a = fa2b <$> a
+  (Error msg) <*> _ = Error msg
+
+instance Functor Parser where
+  -- fmap :: (a -> b) -> Parser a -> Parser b
+  fmap f (Parser pa) = Parser pb
+   where
+    pb inp = f <$> pa inp
+
+instance Applicative Parser where
+  -- pure :: a -> Parser a
+  -- insert a value `x` of type `a` to the parsed part
+  pure x = Parser (\inp -> OK x inp)
+
+  -- (<*>) :: Parser (a -> b) -> Parser a -> Parser b
+  (Parser pa2b) <*> (Parser pa) = Parser pb
+   where
+    -- `pb inp` should be of type `Result b`
+    pb inp = case pa2b inp of
+              -- fa2b :: a -> b
+              -- rem :: String
+              -- 
+              -- attempt to parse rem as a, which is then
+              -- passed to fa2b to make it b
+              -- `pa rem` is of type `Result a`
+              -- `fa2b <$> pa rem` is of type `Result b`
+              OK fa2b rem -> fa2b <$> (pa rem)
+              Error msg -> Error msg
+
+instance Monad Parser where
+  -- Context sensitive parsing as ppk said
+  -- (>>=) :: Parser a -> (a -> Parser b) -> (Parser b)
+  (Parser pa) >>= fa2pb = Parser pb
+   where
+    -- fa2b :: a -> Parser b
+    pb inp = case pa inp of
+               -- `fa2pb a` is of type `Parser b`
+               -- `runParser $ fa2pb a` is of type `String -> Result b`
+               OK a rem -> (runParser $ fa2pb a) rem
+               Error msg -> Error msg
+
+instance Alternative Parser where
+  -- empty :: Parser a
+  empty = Parser (\inp -> Error "empty!")
+
+  -- (<|>) :: Parser a -> Parser a -> Parser a
+  -- Try parsing with first parser, if that fails
+  -- try parsing with the next parser.
+  (Parser px) <|> (Parser py) = Parser pz
+   where
+    pz inp = case px inp of
+               OK xval rem -> OK xval rem
+               Error _ ->
+                 case py inp of
+                   OK yval rem -> OK yval rem
+                   Error msg -> Error msg
+
+{-
+satisfy :: Char -> String -> Result a
+-- `x` is `Char`
+satisfy ch (x:rem) = if ch==x then OK x rem
+                     else Error "err"
+
+helloP = Parser
+-}
+
+
+
+
+
+
+  
+-- parse :: Parser a -> String -> [(a, String)]
+-- -- p :: String -> [(a, String)]
+-- parse (Parser p) inp = p inp
+-- 
+-- item :: Parser Char
+-- item = Parser (\inp -> case inp of
+--                          []     -> []
+--                          (x:xs) -> [(x, xs)])
+-- -- λ> parse item "hello"
+-- -- [('h',"ello")]
+-- 
+-- instance Functor Parser where
+--   -- fmap :: (a -> b) -> Parser a -> Parser b
+--   fmap f pp = Parser (\inp ->
+--                         case parse pp inp of
+--                           []       -> []
+--                           [(x,xs)] -> [(f x,xs)])
diff --git a/haskell/perms.hs b/haskell/perms.hs
new file mode 100644
index 0000000..11b925e
--- /dev/null
+++ b/haskell/perms.hs
@@ -0,0 +1,34 @@
+{- | Find factorial -}
+fact :: Int  -- ^ Integer whose factorial is to be found
+     -> Int  -- ^ Factorial value
+fact n
+  | n > 1  = n * fact (n - 1)
+  | n <= 1 = 1
+
+{- | No error handling
+
+
+Used div instead of / to get integer result instead of float.
+
+Example:
+
+    > p 9 4
+    3024
+-}
+p :: Int  -- ^ n
+  -> Int  -- ^ r
+  -> Int  -- ^ nPr
+p n r
+  | n > r && r >= 0 = (fact n) `div` fact (n - r)
+--  | n == (r + 1)  = 1
+--  | n > r         = n * (p (n-1) r)
+
+{- | No error handling
+
+Example:
+
+-}
+c :: Int  -- ^ n
+  -> Int  -- ^ r
+  -> Int  -- ^ nCr
+c n r = (p n r) `div` (fact r)
diff --git a/haskell/sierpinski.hs b/haskell/sierpinski.hs
new file mode 100644
index 0000000..a40d431
--- /dev/null
+++ b/haskell/sierpinski.hs
@@ -0,0 +1,76 @@
+-- | Find number to base b
+bin
+  :: Int    -- ^ number n
+  -> [Int]  -- ^ digits of n in binary as list. LSB first.
+bin n
+  | n==0 = [0]
+  | otherwise = helper n
+ where
+  helper n
+    | n==0 = []
+    | otherwise = rem:helper nxt
+   where
+    rem = mod n 2
+    nxt = quot n 2
+
+-- | Find value for aCb where a and b ∈ {0, 1}
+nCkBin
+  :: (Int, Int)  -- ^ a and b values as tuple
+  -> Int         -- ^ aCb value
+nCkBin (0, 1) = 0
+nCkBin _ = 1
+
+-- | Calculate nCr value
+nCr
+  :: Int   -- ^ n
+  -> Int   -- ^ r
+  -> Int   -- ^ nCr
+nCr a b = product $ map nCkBin $ zip apad bpad
+ where
+  abin = bin a
+  bbin = bin b
+  alen = length abin
+  blen = length bbin
+  maxlen = max alen blen
+  apad = abin ++ replicate (maxlen-alen) 0
+  bpad = bbin ++ replicate (maxlen-blen) 0
+
+-- | Find values for one level
+oneLine
+  :: Int    -- ^ current level
+  -> [Int]  -- ^ values of the level
+oneLine lvl = [nCr lvl r | r <- [0..lvl]]
+
+-- | Find values of all levels
+allLines
+  :: Int      -- ^ maximum level
+  -> [[Int]]  -- ^ values of levels. Values of each level is in a separate list
+allLines maxLvl = [oneLine i | i <- [0..maxLvl]]
+
+-- | Find values of a level and format it as a string
+fmtOneLine
+  :: Int     -- ^ maximum level
+  -> Int     -- ^ current level
+  -> String  -- ^ formatted string
+fmtOneLine maxLvl lvl = begg ++ bodyhead ++ bodytail
+ where
+  begg = replicate (maxLvl-lvl) ' '
+  digitstr = map show $ oneLine lvl
+  bodyhead = head digitstr
+  bodytail = foldl (++) "" $ map ((++) " ") $ tail digitstr
+
+
+-- | Find values of the entire Pascal triangle and format it as a string
+fmtAllLines
+  :: Int     -- ^ maximum level
+  -> String  -- ^ formatted, read-to-print, string
+fmtAllLines maxLvl = foldl (++) ""  $ map ((++) "\n") strLines
+ where
+  strLines = [fmtOneLine maxLvl lvl | lvl <- [0..maxLvl]]
+
+main = do
+  putStrLn "Enter max level:"
+  maxLevelStr <- getLine
+  let maxLevel = read maxLevelStr :: Int
+  let ll = allLines maxLevel
+  putStrLn $ fmtAllLines maxLevel
diff --git a/haskell/template-haskell/hi.hs b/haskell/template-haskell/hi.hs
new file mode 100644
index 0000000..81c5f35
--- /dev/null
+++ b/haskell/template-haskell/hi.hs
@@ -0,0 +1,16 @@
+-- {-# TemplateHaskell  #-}
+import Clash.Prelude
+import Clash.Sized.Vector
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax
+
+-- v1 = $(listToVecTH [0,1])
+
+  
+{-
+λ> :t $(listToVecTH [0,1])
+$(listToVecTH [0,1]) :: Num a => Vec 2 a
+
+λ> $(listToVecTH [0,1])
+0 :> 1 :> Nil
+-}
diff --git a/haskell/template-haskell/staging-restriction/TH.hs b/haskell/template-haskell/staging-restriction/TH.hs
new file mode 100644
index 0000000..c2ce9d8
--- /dev/null
+++ b/haskell/template-haskell/staging-restriction/TH.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module TH where
+
+import Language.Haskell.TH
+
+someSplice :: Q [Dec]
+someSplice = [d|y = 0|]
diff --git a/haskell/template-haskell/staging-restriction/THEg.hs b/haskell/template-haskell/staging-restriction/THEg.hs
new file mode 100644
index 0000000..4ecaca0
--- /dev/null
+++ b/haskell/template-haskell/staging-restriction/THEg.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+
+import Language.Haskell.TH
+
+import TH
+
+x :: Int
+x = 42
+
+$someSplice
+
+z :: String
+z = show x
+
+
+-- import Language.Haskell.TH
+-- import Language.Haskell.TH.Syntax
+
+-- someSplice :: Q [Dec]
+-- someSplice = [d| y = 0 |]  
+
+-- -- $(someSplice)
+
+-- {-
+--     GHC stage restriction:
+--       ‘someSplice’ is used in a top-level splice, quasi-quote, or annotation,
+--       and must be imported, not defined locally
+--   |
+-- 9 | $(someSplice)
+
+-- -}
+
+  
diff --git a/haskell/traffic-lights.hs b/haskell/traffic-lights.hs
new file mode 100644
index 0000000..7801dad
--- /dev/null
+++ b/haskell/traffic-lights.hs
@@ -0,0 +1,13 @@
+data Color = Red | Yellow | Green
+
+-- | Light state
+-- Format: CurrentNext
+data LState = RY | YG | G | YR
+
+controller :: LState -> () -> (LState, Color)
+controller RY _ = (YG, Yellow)
+controller YG _ = (G,  Green)
+controller G  _ = (YR, Yellow)
+controller YR _ = (RY, Red)
+
+  
diff --git a/lua/lua-date.lua b/lua/lua-date.lua
new file mode 100644
index 0000000..956d747
--- /dev/null
+++ b/lua/lua-date.lua
@@ -0,0 +1,19 @@
+require "io"
+--input = io.read()
+if package.loaded.io then
+  print("io module loaded.")
+else
+  print("io module not loaded.")
+end
+
+--[[
+s = "1950/01/26"
+print(s:match("^%d+"))
+_, i = s:find("^%d/")
+print(_, i)
+s = s:sub(i+1)
+print(s)
+--]]
+
+-- s = "01-Mar-2018"
+-- s:match("^%d%d",
diff --git a/lua/randlua.lua b/lua/randlua.lua
new file mode 100644
index 0000000..dff9ab9
--- /dev/null
+++ b/lua/randlua.lua
@@ -0,0 +1,11 @@
+seednum = io.read()
+math.randomseed(seednum)
+
+local counter = 0
+repeat 
+  local n = math.random(6)
+  print(n)
+  counter = counter + 1
+until n==6
+
+print(counter)
diff --git a/lua/table.lua b/lua/table.lua
new file mode 100644
index 0000000..853036e
--- /dev/null
+++ b/lua/table.lua
@@ -0,0 +1,5 @@
+a = {}
+for i=1,5 do
+  --io.write("Enter element number " .. i)
+  a[i] = io.read()
+end
diff --git a/ocaml/factorial.ml b/ocaml/factorial.ml
new file mode 100644
index 0000000..c69fffd
--- /dev/null
+++ b/ocaml/factorial.ml
@@ -0,0 +1,24 @@
+let rec fact n =
+  if n < 1 then 1
+  else n * (fact (n-1))
+
+let x = fact 5;;
+(*
+The double semicolon is needed above.
+
+This may be related:
+http://ocamlverse.net/content/faq_if_semicolon.html
+*)
+Printf.printf "%d" x
+(* 120 *)
+
+(*************************************************)
+
+(* https://github.com/wiredsister/example-ocaml/blob/master/examples/factorial.ml *)
+let rec fact2 = function
+  | 0          -> 1
+  | n when n>1 -> n * (fact2 (n-1))
+  | _          -> 0;;
+
+Printf.printf "%d" (fact 6)
+(* 720 *)
diff --git a/ocaml/lambda.ml b/ocaml/lambda.ml
new file mode 100644
index 0000000..0878e2d
--- /dev/null
+++ b/ocaml/lambda.ml
@@ -0,0 +1,57 @@
+(*
+https://www.cis.upenn.edu/~bcpierce/tapl/checkers/untyped/
+https://web.archive.org/web/20210423155718/https://www.cis.upenn.edu/~bcpierce/tapl/checkers/
+*)
+
+(* ** Compilation 
+
+ocamlc in.sml -o out.out
+*)
+
+type info = FI of string * int * int | UNKNOWN
+type binding = NameBind
+type context = (string * binding) list
+
+let rec isnamebound ctx x =
+  match ctx with
+      [] -> false
+    | (y,_)::rest ->
+        if y=x then true
+        else isnamebound rest x
+
+let rec pickfreshname ctx x =
+  if isnamebound ctx x then pickfreshname ctx (x^"'")
+  else ((x,NameBind)::ctx), x
+
+
+
+(* Bare bones definition of [term] 
+
+type term = Var of int           (* de-Bruijn index *)
+          | Abs of term
+          | App of term * term
+
+But we are using some annotations to make debugging easier.
+
+ - info: File position where term was found, so errors can point out where the error occurred.
+ - int: For [Var] nodes. Total length of the context in which the variable is occuring. For a consistency check.
+ - string: For [Abs] nodes. To replace de-Bruijn index with a variable name similar to what was used by user.
+*)
+
+type term = Var of info * int * int
+          | Abs of info * term * string
+          | App of info * term * term
+
+
+(* Recursive function to print terms *)
+let rec printTerm ctxt t = match t with
+    Abs(inf, trm, strng) ->
+      let (ctx', trm') = pickfreshname ctx x 
+        in
+      print_string "(lambda ";
+      (* ... *)
+  | App(inf, t1, t2) -> 
+	 	
+
+(* print_string "Hello world!" *)
+
diff --git a/prolog/bmatrix.pl b/prolog/bmatrix.pl
new file mode 100644
index 0000000..f5d98ff
--- /dev/null
+++ b/prolog/bmatrix.pl
@@ -0,0 +1,2 @@
+A = 3
+A = x
\ No newline at end of file
diff --git a/prolog/hello.pl b/prolog/hello.pl
new file mode 100644
index 0000000..67c4a65
--- /dev/null
+++ b/prolog/hello.pl
@@ -0,0 +1,61 @@
+/*
+$ swipl
+Welcome to SWI-Prolog (threaded, 64 bits, version 8.2.4)
+SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
+Please run ?- license. for legal details.
+
+For online help and background, visit https://www.swi-prolog.org
+For built-in help, use ?- help(Topic). or ?- apropos(Word).
+
+?- [user].
+|: nat(0).
+|: nat(s(N)) :- nat(N).
+|: ^D% user://1 compiled 0.01 sec, 2 clauses
+true.
+
+?- nat(0) -> true; abort.
+true.
+
+?- nat(s(s(s(0)))) -> true; abort.
+true.
+
+?- not(nat(s(s(z)))) -> true; abort.
+true.
+*/
+
+
+/*
+plus(X, 0, X).
+plus(0, X, X).
+plus(X, Y, Z) :- plus(s(X), y, s(Z)).
+*/
+
+/*
+member(X, [X|_]).
+member(X, [_|L]) :- member(X, L).
+
+
+?- member(1,[1,2,3]) -> true; abort.
+true.
+
+?- not(member(4,[1,2,3])) -> true; abort.
+true.
+*/
+
+
+/*
+range(ST,EN,N) :- N>=ST, N=<EN.
+
+
+?- not(range(1,2,0)) -> true; abort.
+true.
+
+?- range(1,2,1) -> true; abort.
+true.
+
+?- range(1,2,2) -> true; abort.
+true.
+
+?- not(range(1,2,3)) -> true; abort.
+true.
+*/
diff --git a/sml/defun.sml b/sml/defun.sml
new file mode 100644
index 0000000..33ecf88
--- /dev/null
+++ b/sml/defun.sml
@@ -0,0 +1,124 @@
+datatype re
+  = Chr of int
+  | Cat of re * re
+  | Alt of re * re
+  | Star of re
+  
+(* accept : re -> int list -> (int list -> bool) -> bool *)
+(* accept_star : re -> int list -> (int list -> bool) -> bool *)
+fun accept (Chr c) (x::xs) k
+    = (c=x) andalso (k xs)
+  | accept (Cat (r1,r2)) l k
+    (* = accept r1 l (fn xs => *)
+    (*     accept r2 xs (fn ys => k ys)) *)
+    = accept r1 l (fn xs => accept r2 xs k)
+  | accept (Alt (r1,r2)) l k
+    (* = (accept r1 l (fn xs => k xs)) orelse  *)
+    (*   (accept r2 l (fn xs => k xs)) *)
+    = (accept r1 l k) orelse (accept r2 l k)
+  | accept (Star r1) l k = accept_star r1 l k
+  | accept _ _ _ = false
+and accept_star r l k
+  = (k l) orelse (accept r l (fn xs => accept_star r xs k))
+         
+(* match : re -> int list -> bool *)
+fun match r l = accept r l (fn xs => xs=nil)
+
+datatype kont
+  (* (fn xs => xs=nil) *)
+  = KNil
+  (* (fn xs => accept r2 xs k) *)
+  | KAcc of re * kont
+  (* (fn xs => accept_star r xs k) *)
+  | KStar of re * int list * kont
+				 
+(* acceptDef: re -> int list -> kont -> bool *)
+fun acceptDef (Chr c) (x::xs) k
+    = (c=x) andalso (k xs)
+  | acceptDef (Cat (r1,r2)) l k
+    = acceptDef r l (KAcc (r2, k))
+  | acceptDef (Alt (r1,r2)) l k
+    = (acceptDef r1 l k) orelse (acceptDef r2 l k)
+  | acceptDef (Star r1) l k = accept_starDef r1 l k
+and apply KNil l = l=nil
+  | apply (KAcc (r,k)) l = acceptDef r l k
+  | apply (KStar (r,ll,k)) l = accept_starDef r ll k
+and accept_starDef r l k = acceptDef r l KNil
+		       
+(* (* datatype kont *) *)
+(* (*   = KNil           (* (fn xs => xs=nil) *) *) *)
+(* (*   | Kont of kont   (* (fn xs => k xs) *) *) *)
+(* (*   (* (fn xs => accept r2 xs (fn ys => k ys)) *) *) *)
+(* (*   | KNst of re * kont *) *)
+         
+(* val re0 = Cat (Chr 0, Cat (Chr 0, Cat (Chr 1, Chr 1))) *)
+(* val rv0t = accept re0 [0,0,1,1] (fn xs=>xs=nil) (* true : bool *) *)
+(* val rv0f = accept re0 [0,0,1] (fn xs=>xs=nil)   (* false : bool *) *)
+
+(* (* match re0 [0,0,1,1]; *) *)
+(* (* val it = true : bool *) *)
+(* (* - match re0 [0,0,1]; *) *)
+(* (* val it = false : bool *) *)
+
+
+
+
+(*****************************************************************)
+
+(* (* walk : int list -> (int list -> bool) -> bool *) *)
+(* fun walk (0::xs, k) *)
+(*     = walk (xs, fn (1::ys) => k ys *)
+(*                  | _       => false) *)
+(*   | walk (xs, k) =  k xs *)
+(*   (* Base case: xs == nil *) *)
+(*   (* Father... Is it over..? No king rules forever son.. *) *)
+          
+(* (* go : int list -> bool *) *)
+(* fun go xs = walk (xs, fn l => l = nil) *)
+(* (* go [1,2,3]; *) *)
+(* (* val it = false : bool *) *)
+(* (* - go [0,0,0,1,1,1]; *) *)
+(* (* val it = true : bool *) *)
+     
+(* (* *) *)
+(* (* Function as argument => [fn] usages. *) *)
+(* (* So there are two of them. *) *)
+(* (* *) *)
+
+(* datatype kont *)
+(*   = KId *)
+(*   | KWalk of kont *)
+
+(* (* apply: kont * int list -> bool *) *)
+(* fun apply (KId, xs)        = xs=nil *)
+(*   | apply (KWalk k, 1::xs) = apply (k, xs) *)
+(*   | apply (KWalk _, _)     = false *)
+				 
+(* (* walkDef : int list -> kont -> bool *) *)
+(* fun walkDef (0::xs) k = walkDef xs (KWalk k) *)
+(*   | walkDef xs k = apply (k, xs) *)
+
+(* fun goDef xs = walkDef xs KId *)
+(* (* - goDef [0,0,1,1]; *) *)
+(* (* val it = true : bool *) *)
+(* (* - goDef [0,0,1]; *) *)
+(* (* val it = false : bool *) *)
+
+(* (*********************** Peano arithmetic **************************************) *)
+
+(* (* apply: int * int list -> bool *) *)
+(* fun applyP (0, xs)        = xs=nil *)
+(*   | applyP (k, 1::xs) = applyP (k-1, xs) *)
+(*   | applyP _     = false *)
+				 
+(* (* walkDef : int list -> int -> bool *) *)
+(* fun walkDefP (0::xs) k = walkDefP xs (k+1) *)
+(*   | walkDefP xs k = applyP (k, xs) *)
+
+(* fun goDefP xs = walkDefP xs 0 *)
+(* (* - goDefP [1,1,0]; *) *)
+(* (* val it = false : bool *) *)
+(* (* - goDefP [0,0,1,1]; *) *)
+(* (* val it = true : bool *) *)
+(* (* - goDefP [0,0,0,1,1,1]; *) *)
+(* (* val it = true : bool *) *)
diff --git a/sml/inf.sml b/sml/inf.sml
new file mode 100644
index 0000000..50cb123
--- /dev/null
+++ b/sml/inf.sml
@@ -0,0 +1,42 @@
+(* Attempt to replicate a coq file *)
+datatype instr
+  = Const of bool
+  | Goto of int
+
+type prog = instr list
+
+fun eclosure_aux p idx visited =
+  let
+    val inds = List.tabulate (length p, fn x=>x)
+    val aug = ListPair.zip (inds, p)
+  in
+    case (List.nth (aug, idx)) of
+      (i, x) => 
+        (case x of
+          Const _ => [i]     
+        | Goto k =>
+	    if List.exists (fn x => x=k) visited then [i]
+            else i :: (eclosure_aux p k (i::visited)))
+  end
+fun eclosure p idx = eclosure_aux p idx []
+
+val p1 = [
+  Const true,     (* 0 *)
+  Const false,    (* 1 *)
+  Goto 4,         (* 2 *)
+  Const true,     (* 3 *)
+  Goto 1          (* 4 *)
+]
+
+val p2 = [
+  Const true,     (* 0 *)
+  Const false,    (* 1 *)
+  Goto 4,         (* 2 *)
+  Const true,     (* 3 *)
+  Goto 2          (* 4 *)
+]
+	     
+val v1 = eclosure p1 2
+(* [2,4,1] : int list *)
+
+val v2 = eclosure p2 2
diff --git a/sml/vec.sml b/sml/vec.sml
new file mode 100644
index 0000000..741d2bc
--- /dev/null
+++ b/sml/vec.sml
@@ -0,0 +1,199 @@
+structure Re : sig
+  (* Type of regular expressions. Int is used as type for now *)
+  datatype re
+    = Null
+    | Eps
+    | Chr of int
+    | Cat of re * re
+    | Alt of re * re
+    | Star of re
+  (* eqtype re *)
+
+  (* https://github.com/smlnj/smlnj/blob/4fd2ef86aa1341e9c43e118ab675738cd3e77135/system/Basis/Implementation/string.sig#L12 *)
+  val /\ : (re * re) -> re
+  val \/ : (re * re) -> re
+end = struct
+  datatype re
+    = Null
+    | Eps
+    | Chr of int
+    | Cat of re * re
+    | Alt of re * re
+    | Star of re
+  
+  (* Some 'notations' *)
+  fun op /\ (x, y) = Cat (x, y)
+  fun op \/ (x, y) = Alt (x, y)
+  infixr 8 /\
+  infixr 9 \/
+end
+
+structure Instr :
+sig
+  (* Type of instructions of VM *)
+  datatype instr
+    = Char of int
+    | Halt
+    | Fork of int
+    | Jump of int
+  val toString: instr -> string
+end = struct
+  datatype instr
+    = Char of int
+    | Halt
+    | Fork of int
+    | Jump of int
+
+  fun toString (Char c) = "Char " ^ (Int.toString c)  		
+    | toString Halt = "Halt"
+    | toString (Fork ind) = "Fork " ^ (Int.toString ind)
+    | toString (Jump ind) = "Jump " ^ (Int.toString ind)
+end
+	  
+structure Prog : sig
+  type prog = Instr.instr list
+  val compile: Re.re -> prog
+  val toString: prog -> string
+  val ecloseOne: int -> prog -> IntListSet.set
+end = struct
+  open Instr
+  open Re
+  type prog = instr list
+		    
+  fun compile_aux curr Null          = [Halt] 
+    | compile_aux curr Eps           = []
+    | compile_aux curr (Chr c)       = [Char c]
+    | compile_aux curr (Cat (r1,r2)) =
+        let
+          val p1 = compile_aux curr r1
+          val n1 = length p1
+        in
+	  p1 @ (compile_aux n1 r2)
+        end
+    | compile_aux curr (Alt (r1,r2)) =
+        let
+          val p1 = compile_aux (curr+1) r1
+          val n1 = length p1
+          val p2 = compile_aux (curr+1+n1+1) r2
+          val n2 = length p2
+          val offset1 = curr+n1+2 (* +2 for jump and next *)
+          val offset2 = curr+n1+2+n2
+        in
+          [Fork offset1] @ p1 @ [Jump offset2] @ p2
+        end
+    | compile_aux curr (Star r) =
+        let
+          val p = compile_aux (curr+1) r
+          val n = length p
+          val offset = curr+1+n+1
+        in
+          [Fork offset] @ p @ [Jump curr]
+        end
+  fun compile r = (compile_aux 0 r) @ [Halt]
+					  
+  fun toString p =
+    let
+      val inds = List.tabulate (length p, fn x=>Int.toString x)
+      val aug = ListPair.zip (inds, p)
+    in
+      foldl
+	(fn ((ind,i), acc) => acc ^ ind ^ "| " ^ (Instr.toString i) ^ "\n")
+	"" aug
+    end
+	
+
+  fun ecloseOne_aux acc ind prog =
+     if ind >= length prog then IntListSet.empty
+     else if IntListSet.member (acc, ind) then IntListSet.empty
+     else
+       case (List.nth (prog, ind)) of
+           Char _ => IntListSet.singleton ind
+         | Fork k =>
+             let val acc' = IntListSet.add (acc, ind) in
+               IntListSet.union (ecloseOne_aux acc' (ind+1) prog, ecloseOne_aux acc' k prog)
+             end
+         | Jump k =>
+             let val acc' = IntListSet.add (acc, ind) in
+               ecloseOne_aux acc' k prog
+             end
+         | Halt => IntListSet.singleton ind
+  (* ecloseOne: int -> prog -> {int} *)
+  (* Take epsilon-closure of one instruction. *)
+  fun ecloseOne ind prog = ecloseOne_aux IntListSet.empty ind prog
+end
+
+open Re
+open Instr
+open Prog
+	 
+fun getChars_aux ((ind, Char _)::p) = ind::(getChars_aux p)
+  | getChars_aux (_::p) = getChars_aux p
+  | getChars_aux [] = []
+(* getChars: prog -> [int] *)
+			 
+
+fun getChars' p =
+  let
+    val inds = List.tabulate (length p, fn x=>x)
+    val aug = ListPair.zip (inds, p)
+  in
+    getChars_aux aug
+  end
+
+(* Find location of all [Char] *)
+fun getChars p =
+  let
+    val chrs = getChars' p
+    val indsc = List.tabulate (length chrs, fn x=>x+1)
+  in
+    ListPair.zip (chrs, indsc)
+  end
+(* Find location of all [Halt] *)
+fun getHalts p =
+  let 
+    val temp = foldl (fn (x,(acc, ctr)) =>
+      case x of
+          Halt => (ctr::acc, ctr+1)
+        | _ => (acc, ctr+1)
+      ) ([],0) p
+  in
+    map (fn x => (x,0)) (#1 temp)
+  end
+    
+fun getTrTb p = (getHalts p) @ (getChars p)
+				   
+
+val eg1 = Cat (Chr 1, Chr 2)
+val eg2 = Star (Chr 1)
+val eg3 = Star (Star (Chr 1))
+val eg4 = Cat (Chr 0, Alt (Chr 1, Star (Chr 2)))
+val eg5 = Alt (Chr 0, Chr 1)
+
+val prog1 = compile eg1
+val prog2 = compile eg2
+val prog3 = compile eg3
+val prog4 = compile eg4
+(* 0| Char 0 *)
+(* 1| Fork 4 *)
+(* 2| Char 1 *)
+(* 3| Jump 7 *)
+(* 4| Fork 7 *)
+(* 5| Char 2 *)
+(* 6| Jump 4 *)
+(* 7| Halt *)
+
+val prog5 = compile eg5
+(* 0| Fork 3 *)
+(* 1| Char 0 *)
+(* 2| Jump 4 *)
+(* 3| Char 1 *)
+(* 4| Halt *)
+
+(* val chrs4 = getChars prog4 *)
+(* val halt4 = getHalts prog4 *)
+val trtb4 = getTrTb prog4
+(* val trtb4' = map (fn (a,b) => (b,a)) trtb4; *)
+val charIdxs = getChars' prog4
+val t1 = ecloseOne x prog4
+
+(* fun foo ind prog *)
diff --git a/vhdl/README.org b/vhdl/README.org
new file mode 100644
index 0000000..6739d0f
--- /dev/null
+++ b/vhdl/README.org
@@ -0,0 +1,24 @@
+#+TITLE: VHDL
+From 2021-2022..
+
+ - [[./2b-down-counter]]: 2b down counter
+ - [[./2b-timer]]: 2b timer
+ - [[./2b-up-counter]]: 2b up counter
+ - [[./2b-up-counter-gaisler]]: 2b down counter (Gaisler style)
+ - [[./cla-adder]]: 4b carry-lookahead adder
+ - [[./comparator]]: A comparator
+ - [[./half-adder]]: Half adder
+ - [[./ripple-ca]]: 4b ripple carry adder
+ - [[./mux]]: 2:1 MUX
+ - [[./record_inputs]]: using a record as input type
+
+#delay
+#delay2
+#enum
+#gcd
+#merge-dff
+#port_map-mod
+#vcd-record
+#weird-clock
+#rv
+#subtractor