diff --git a/c/README.org b/c/README.org index e55b3a2..283afcc 100644 --- a/c/README.org +++ b/c/README.org @@ -4,4 +4,5 @@ - [[./pi-val-leibnitz.c][pi-val-leibnitz.c]]: Approximating value of pi using Ramanjuan's method - [[./pi-val-ramanjuan.c][pi-val-ramanjuan.c]]: Approximating value of pi using Leibnitz's method - [[./grammar-comment-like.c][grammar-comment-like.c]]: A C-grammar 'pitfall' + - [[./void-rv-assign.c]]: What happens when we try to use value returned by a function returning ~void~ diff --git a/coq/MAC.v b/coq/MAC.v new file mode 100644 index 0000000..6a918e0 --- /dev/null +++ b/coq/MAC.v @@ -0,0 +1,26 @@ +Require Extraction. +Extraction Language Haskell. +Require Import ExtrHaskellBasic. +Require Import ExtrHaskellString. + +Require Import ExtrHaskellNatInt. +Require Import ExtrHaskellZInt. + +(* +Require Import ExtrHaskellNatInteger. +Require Import ExtrHaskellZInteger. +Require Import ExtrHaskellNatNum. +Require Import ExtrHaskellZNum. + *) + +Set Extraction File Comment "Made from Coq". +Extract Inlined Constant fst => "Prelude.fst". +Extract Inlined Constant snd => "Prelude.snd". +Extraction Blacklist Main. + + +Definition mac' (acc: nat) (xy: nat*nat): nat := acc + ((fst xy)*(snd xy)). + +Definition topFn (acc: nat) (xy: nat*nat) : nat * nat := (mac' acc xy, acc). + +Recursive Extraction topFn. diff --git a/coq/b2-ssft22.v b/coq/b2-ssft22.v new file mode 100644 index 0000000..cd05d43 --- /dev/null +++ b/coq/b2-ssft22.v @@ -0,0 +1,60 @@ +(* Boolean formula *) +Inductive boolf: Type := +| Atom: bool -> boolf +| Neg: boolf -> boolf +| And: boolf -> boolf -> boolf +| Or: boolf -> boolf -> boolf +| Impl: boolf -> boolf -> boolf. +Notation "⊤" := (Atom true) (at level 10). +Notation "⊥" := (Atom false) (at level 10). +Notation "'¬' b" := (Neg b) (at level 10). +Infix "∧" := And (at level 15). +Infix "∨" := Or (at level 20). +Infix "→" := Impl (at level 25). + +Example f1 := ((⊤ ∨ ⊥) ∧ ⊥) → (¬ ⊥). + +Inductive kont {V:Type}: Type := +| Letk: kont -> kont -> kont. +Arguments kont: clear implicits. + +Inductive kont {V:Type}: Type := +| KAtom: bool -> kont +| KNeg: kont -> kont +| KAnd: (V -> kont) -> (V -> kont) -> kont +| KOr: (V -> kont) -> (V -> kont) -> kont +| KImpl: (V -> kont) -> (V -> kont) -> kont. +Arguments kont: clear implicits. + +Fixpoint compile {V:Type} (f:boolf): kont V := + match f with + | Atom b => KAtom b + | Neg f => KNeg (compile f) + | And f1 f2 => KAnd (fun k => compile f1) (fun k => compile f2) + | Or f1 f2 => KOr (fun k => compile f1) (fun k => compile f2) + | Impl f1 f2 => KImpl (fun k => compile f1) (fun k => compile f2) + end. + +Check compile (V:=unit) f1. +Compute compile (V:=unit) f1. +(* https://en.wikipedia.org/wiki/Tseytin_transformation *) + +Inductive cnf: Type := +| CTru | CFls: cnf +| CNeg: cnf -> cnf +| CCons: cnf -> cnf -> cnf. + +Fixpoint cnfy (f:boolf): cnf := + match f with + | Tru => CTru + | Fls => CFls + | Neg b => CNeg (cnfy b) + | And Fls _ => CFls + | And _ Fls => CFls + | And Tru f2 => cnfy f2 + | And f1 Tru => cnfy f1 + | And f1 f2 => + | Or f1 f2 => + | Impl f1 f2 => CCons (CNeg (cnfy f1)) (cnfy f2) + end. + diff --git a/coq/bits.v b/coq/bits.v new file mode 100644 index 0000000..da13473 --- /dev/null +++ b/coq/bits.v @@ -0,0 +1,90 @@ +Require Import Vector String Ascii. +Import VectorNotations. + +(* +Fixpoint bv (n:nat): Type := + match n with + | O => unit + | S n' => (bv n') * bool + end. +Check (false, false, false, false, tt). +Compute bv 2. +Compute (tt, true, true) : bv 2. + +Definition charToNibble (c:Ascii.ascii): bv 4 := + (match c with + | "0" => (tt, false, false, false, false) + | "1" => (tt, true, false, false, false) + | "2" => (tt, false, true, false, false) + | "3" => (tt, true, true, false, false) + | "4" => (tt, false, false, true, false) + | "5" => (tt, true, false, true, false) + | "6" => (tt, false, true, true, false) + | "7" => (tt, true, true, true, false) + | "8" => (tt, false, false, false, true) + | "9" => (tt, true, false, false, true) + | "a" | "A" => (tt, false, true, false, true) + | "b" | "B" => (tt, true, true, false, true) + | "c" | "C" => (tt, false, false, true, true) + | "d" | "D" => (tt, true, false, true, true) + | "e" | "E" => (tt, false, true, true, true) + | "f" | "F" => (tt, true, true, true, true) + | _ => (tt, false, false, false, false) + end)%char. + +Fixpoint fromHex (s:string): bv ((String.length s)*4) := + match s with + | String x xs => (fromHex xs) (charToNibble x) + | EmptyString => tt + end. +Compute fromHex "ae". +*) + + + +(*****************************************************) + +Definition bv (n:nat):= Vector.t bool n. + +Print string. +Check "c"%char. + +Definition charToNibble (c:Ascii.ascii): bv 4 := + (match c with + | "0" => [false; false; false; false] + | "1" => [true; false; false; false] + | "2" => [false; true; false; false] + | "3" => [true; true; false; false] + | "4" => [false; false; true; false] + | "5" => [true; false; true; false] + | "6" => [false; true; true; false] + | "7" => [true; true; true; false] + | "8" => [false; false; false; true] + | "9" => [true; false; false; true] + | "a" | "A" => [false; true; false; true] + | "b" | "B" => [true; true; false; true] + | "c" | "C" => [false; false; true; true] + | "d" | "D" => [true; false; true; true] + | "e" | "E" => [false; true; true; true] + | "f" | "F" => [true; true; true; true] + | _ => [false; false; false; false] + end)%char. + +Fixpoint fromHex (s:string): bv ((String.length s)*4) := + match s with + | String x xs => Vector.append (charToNibble x) (fromHex xs) + | EmptyString => Vector.nil bool + end. +Compute fromHex "ae". + +Fixpoint bvToNat {n:nat} (bv: bv n) (pw: nat): nat := + match bv with + | Vector.nil _ => 0 + | Vector.cons _ x _ xs => + match x with + | true => (Nat.pow 2 pw) + (bvToNat xs) (S pw) + | _ => bvToNat xs (S pw) + end + end. +Compute fromHex "0ea". +Compute bvToNat (fromHex "0ea") 0. diff --git a/coq/brzozowski.v b/coq/brzozowski.v new file mode 100644 index 0000000..75f54cf --- /dev/null +++ b/coq/brzozowski.v @@ -0,0 +1,69 @@ +Require Import List. +Import ListNotations. + +(* Syntax of re *) +Inductive re {A:Type}: Type := +| ε | Null: re +| Char: A -> re +| Cat: re -> re -> re +| Alt: re -> re -> re +| Star: re -> re. +Arguments re: clear implicits. + +Module ReNotations. + Notation "∅" := Null. + Notation "'↑' a" := (Char a) (at level 10). + Notation "r '∗'" := (Star r) (at level 20). + Infix ";" := Cat (at level 60, right associativity). + Infix "│" := Alt (at level 65, right associativity). +End ReNotations. + +(* Small-step operational semantics for re *) +Inductive reDe {A:Type}: list A -> re A -> Prop := +| εDe: reDe [] ε +| CharDe: forall (a:A), reDe [a] (Char a) +| CatDe: forall (r1 r2:re A) (l1 l2: list A), + reDe l1 r1 -> reDe l2 r2 -> reDe (l1++l2) (Cat r1 r2) +| AltDeL: forall (r1 r2:re A) (l: list A), + reDe l r1 -> reDe l (Alt r1 r2) +| AltDeR: forall (r1 r2:re A) (l: list A), + reDe l r2 -> reDe l (Alt r1 r2) +| StarDeMore: forall (r:re A) (l1 l2:list A), + reDe l1 r -> reDe l2 (Star r) -> reDe (l1++l2) (Star r) +| StarDeDone: forall r:re A, reDe [] r. +Notation "w '⊨' r" := (reDe w r) (at level 50, only parsing). + + +Section Deriv. + Context {A:Type}. + Variable A_eqb: A -> A -> bool. + + (* Brzozowski derivative *) + Fixpoint δ (a:A) (r: re A): re A := + match r with + | ε | Null => Null + | Char c => + if A_eqb c a then ε + else Null + | Cat r1 r2 => Cat (δ a r1) r2 + | Alt r1 r2 => Alt (δ a r1) (δ a r2) + | Star r' => δ a r' (* ε case won't be possible in derivative *) + end. +End Deriv. + +Theorem foo (A:Type) (A_eqb: A -> A -> bool) (r:re A) (a:A) (w:list A): + (a::w) ⊨ r -> w ⊨ (δ A_eqb a r). +Proof. + induction r; simpl. + - intro H; inversion H. + - intro H; inversion H. + + - intro H. + pv_opt. + repeat in_inv. + induction w. + + constructor. + + induction w. +Abort. + + diff --git a/coq/bsv-mimicry.v b/coq/bsv-mimicry.v new file mode 100644 index 0000000..5e0cd8a --- /dev/null +++ b/coq/bsv-mimicry.v @@ -0,0 +1,26 @@ +(* +https://coq.inria.fr/library/Coq.Vectors.VectorDef.html +https://coq.inria.fr/library/Coq.Bool.Bvector.html +https://github.com/sifive/Kami/blob/ffb77238f27b603dbd42d2622ba911740bf5eadf/Extraction.v + + + +https://news.ycombinator.com/item?id=12183095 + +A scala extractor plugin: https://bitbucket.org/yoshihiro503/coq2scala/src/1657d65c747bb9747a4ec32b3da36464631bcd18/coq-8.3pl2/plugins/extraction/scala.ml +A rust extractor plugin: https://github.com/pirapira/coq2rust/blob/rust/plugins/extraction/rust.ml +*) +Require Import Vector. +Require Import Bvector. +Import VectorNotations. +Import BvectorNotations. + +Definition halfadder (a b: Bvector 1): Bvector 2 := + (a ^& b) ++ (a ^⊕ b). + + +Require Extraction. +Extraction Language Haskell. +Extract + + diff --git a/coq/cpdt/red-black-tree.v b/coq/cpdt/red-black-tree.v new file mode 100644 index 0000000..02a02ab --- /dev/null +++ b/coq/cpdt/red-black-tree.v @@ -0,0 +1,82 @@ +(* +Cormen - Chapter 13: + +Red-black trees are Binary trees such that: + 1) Each node is either red or black + 2) Root is black + 3) All leaves are black + 4) All children of a red node are black + 5) For each node, number of black nodes in every possible simple path to + leaves is the same. + *) + +Inductive colour: Set := Red | Black. + +(* [rbtree c d] denotes a tree of black depth [d] + whose root node is coloured [c] + + Black depth is the number of black nodes (not including current node) + in a path to one of the leaf nodes. + + Root needn't be red in this implementation. *) +Inductive rbtree: colour -> nat -> Type := +| Leaf: rbtree Black 0 + +(* Red node can't be a leaf and both children of a red node must be black *) +| RedNode: forall {n:nat}, + rbtree Black n -> rbtree Black n -> rbtree Red n + +| BlackNode: forall {n:nat} {c1 c2:colour}, +(* If both children have black depth [n], regardless of their colour, then + this node, which is black, would have black depth [n+1]. + And [n] has to be same for both branches, by definition of rb tree. *) + rbtree c1 n -> rbtree c2 n -> rbtree Black (S n). + + +Fixpoint depth {c:colour} {n:nat} + (f: nat -> nat -> nat) (* a 'combining' function *) + (t: rbtree c n): nat := + match t with + | Leaf => 0 + | RedNode t1 t2 => S (f (depth f t1) (depth f t2)) + | BlackNode t1 t2 => S (f (depth f t1) (depth f t2)) + end. + +Example eg1 := Leaf. +Example rLeaf := RedNode Leaf Leaf. (* red leaf *) +Example bLeaf := BlackNode Leaf Leaf. (* black leaf *) +Check bLeaf. +(* bLeaf : rbtree Black 1 *) +Check rLeaf. +(* bLeaf : rbtree Red 0 *) +Check BlackNode bLeaf bLeaf. +(* BlackNode bLeaf bLeaf : rbtree Black 2 *) + +(* Left tree has d=2, right tree has d=1 *) +Fail Check BlackNode bLeaf rLeaf. +(* + B + R + B + + +B + + + B + B + B + *) + +Require Import Arith. +Check Nat.min_dec. +Print Nat.Private_Dec.min_dec. + +(* +Lemma min_dec (n m:nat): {min n m = n} + {min n m = m}. +Proof. + induction n. + - simpl; now left. + - induction m. + + right; now simpl. + *) diff --git a/coq/folds.v b/coq/folds.v new file mode 100644 index 0000000..e4b6d1f --- /dev/null +++ b/coq/folds.v @@ -0,0 +1,170 @@ +Require Import List. +Import ListNotations. +(* Print fold_left. *) +(* Print fold_right. *) + +Definition compose {A B C: Type} + (g: B -> C) (f: A -> B): A -> C := fun a => + g (f a). +Infix "∘" := compose (at level 45, right associativity). + +Section Folds. + Context {A B: Type}. + Variable (f: A -> B -> B). + + Fixpoint foldr (acc: B) (l: list A): B := + match l with + | [] => acc + | x::xs => f x (foldr acc xs) + end. +End Folds. + +Section Folds. + Context {A B: Type}. + Variable (f: A -> B -> B). + Variable (g: list A -> B). + Variable (acc: B). + + Theorem univFold: + g [] = acc /\ + (forall (x:A) (xs:list A), + g (x::xs) = f x (g xs)) + <-> forall (l:list A), + g l = foldr f acc l. + Proof. + split. + - intros [HNil HCons] l. + induction l. + + simpl; trivial. + + simpl. + rewrite <- IHl. + rewrite (HCons a l). + reflexivity. + - intros H. + split. + + apply H. + + intros x xs. + rewrite (H (x::xs)). + simpl. + rewrite (H xs). + reflexivity. + Qed. + + (* Theorem univFold: *) + (* g [] = acc *) + (* -> (forall (x:A) (xs:list A), *) + (* g (x::xs) = f x (g xs)) *) + (* -> forall (l:list A), *) + (* g l = foldr f acc l. *) + (* Proof. *) + (* intros HNil HCons l. *) + (* induction l. *) + (* - simpl; trivial. *) + (* - simpl. *) + (* rewrite <- IHl. *) + (* rewrite (HCons a l). *) + (* reflexivity. *) + (* Qed. *) +End Folds. + +Section Folds. + Context {A B: Type}. + Variable (f g: A -> B -> B). + Variable (h: B -> B). + Variable (acc acc': B). + + Theorem fusionFold: + h acc' = acc + -> (forall (a:A) (b:B), + h (g a b) = f a (h b)) + -> forall l:list A, + (h ∘ (foldr g acc')) l = (foldr f acc) l. + Proof. + intros HNil HCons l. + unfold compose. + induction l. + - simpl; apply HNil. + - simpl. + rewrite HCons. + rewrite IHl. + reflexivity. + Qed. + + (* Theorem fusionFold': *) + (* h acc' = acc *) + (* /\ (forall (a:A) (b:B), *) + (* h (g a b) = f a (h b)) *) + (* <-> forall l:list A, *) + (* (h ∘ (foldr g acc')) l = (foldr f acc) l. *) + (* Proof. *) + (* unfold compose. *) + (* split. *) + (* - intros [HNil HCons] l. *) + (* induction l. *) + (* + simpl; apply HNil. *) + (* + simpl. *) + (* rewrite HCons. *) + (* rewrite IHl. *) + (* reflexivity. *) + (* - intros H. *) + (* split. *) + (* + assert (foldr g acc' [] = acc') as H1; try reflexivity. *) + (* rewrite <- H1. *) + (* assert ((h (foldr g acc' [])) = (h ∘ foldr g acc') []) as H2; try reflexivity. *) + (* rewrite H2. *) + (* assert (((foldr f acc) []) = (h ∘ foldr g acc') []) as H3; try reflexivity. *) + (* * simpl. *) + (* unfold compose. *) + (* rewrite (H []). *) + (* simpl; reflexivity. *) + (* * unfold compose. *) + (* rewrite (H []). *) + (* simpl; reflexivity. *) + (* + intros a b. *) + (* Qed. *) +End Folds. + +Section UnivEg. + Fixpoint sumlist (l: list nat): nat := + match l with + | x::l' => x + sumlist l' + | [] => 0 + end. + Compute sumlist [1;2;3;4;5]. + (* = 15 : nat *) + Compute ((Nat.add 1) ∘ sumlist) [1;2;3;4;5]. + (* = 16 : nat *) + + + Lemma sumlistLemma: forall (x:nat) (xs:list nat), + S (x + sumlist xs) = x + S (sumlist xs). + Proof. + intros x xs. + induction x. + - simpl; trivial. + - simpl. + rewrite IHx. + reflexivity. + Qed. + + Example sumfold: forall l:list nat, + ((Nat.add 1) ∘ sumlist) l = foldr Nat.add 1 l. + Proof. + intros l. + apply univFold. + - unfold compose. + simpl; reflexivity. + - intros x xs. + unfold compose. + simpl. + (* [ring] could also be used at this stage *) + (* Require Import Arith. *) + (* ring. *) + apply sumlistLemma. + Qed. (* No induction was needed! *) +End UnivEg. + +Section FusionEg. +End FusionEg. + +Compute foldr Nat.add 0 [1;2;3;4;5]. (* = 15 : nat *) diff --git a/coq/fstr.v b/coq/fstr.v new file mode 100644 index 0000000..dd530e7 --- /dev/null +++ b/coq/fstr.v @@ -0,0 +1,45 @@ +Require Import String. + +(* https://docs.python.org/3/library/string.html#formatspec *) + +(* bcdeEfFgGnosxX% *) +Inductive type: Set := | TypHex | TypInt | TypStr | TypFloat. + +Inductive align: Set := AlignLeft | AlignRight | AlignJust | AlignCenter. +Inductive sign: Set := SignPos | SignNeg | SignSpc. + +Definition digit := nat. +Definition width := digit. +Definition precision := digit. + +Inductive prec := +| Prec: width -> option type -> prec. + +Notation "'․' width '_d'" := (Prec width (Some TypInt)) + (at level 9, width constr). +Notation "'․' width" := (Prec width None) (at level 10). + + +Print Grammar constr. +Compute ․2. +Compute ․2 _d. + + +Inductive spec: Set := +| Spec: option width -> precision -> type -> spec. + +(* .2f *) +Check Spec None 2 TypFloat. + +Notation "F '.' precision typ " := (Spec None precision typ) (at level 50). +Check F.2 + + +(* +Inductive digit: Set := | D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9. + +Inductive align: Type := option Ascii.ascii -> + +Inductive spec: Type := +| Spec: align -> + *) diff --git a/coq/misc/lia-stuff.v b/coq/misc/lia-stuff.v new file mode 100644 index 0000000..73035d4 --- /dev/null +++ b/coq/misc/lia-stuff.v @@ -0,0 +1,16 @@ +Require Import ssreflect Lia. + +Locate "_ <= _". +Search not lt le. + +Goal forall (a b: nat), + ~(a < b) -> b <= a. +Proof. + lia. +Show Proof. (* Quite big and incomprehensible. + Price to be paid for automation *) +Restart. + move => a b H. + by rewrite -PeanoNat.Nat.nlt_ge. +Show Proof. (* Simpler. More readable *) +Qed. diff --git a/coq/misc/mathcomp-stuff.v b/coq/misc/mathcomp-stuff.v new file mode 100644 index 0000000..6263fd2 --- /dev/null +++ b/coq/misc/mathcomp-stuff.v @@ -0,0 +1,67 @@ +From mathcomp Require Import all_ssreflect. +Require Import Arith. + +(*=================================================================*) + +Goal forall n m:nat, + n.+1 < m.+1 -> n < m. + (* I guess it's because mathcomp uses `addn` and coq stdlib uses `Nat.add`? *) +Proof. + move => n m /ltP //=. + (* Check (ltn_add2r 1) n m. *) +Qed. + + +Goal forall n m:nat, + n < m -> n.+1 < m.+1. +Proof. + move => n m /ltP //=. +Qed. + +Goal forall (n m: nat), + (forall a b:nat, a < b) -> n.+1 < m.+1. +Proof. + move => n m H. + have HH := H n m. + move: HH. + by move /ltP. +Qed. + + +(*=================================================================*) + +Locate "_ False. +Proof. +(* + move: H1 /Nat.ltb_spec0. + +Error: +dependents switch `/' in move tactic +*) +Restart. + move => a b H1. + move: H1. + move /Nat.ltb_spec0 /ltP => H. (* ✓ *) +Restart. + move => a b /Nat.ltb_spec0 /ltP. +Abort. (* ✓ *) + +(*=================================================================*) + +Lemma le_ge_symm: forall n m:nat, + n >= m <-> m <= n. +Proof. + split. + - elim: n => [|n]; first by []. + move => IHn. + by case. + - elim: n => [|n]; first by []. + move => IHn. + by case. +Qed. diff --git a/coq/misc/ssreflect-stuff.v b/coq/misc/ssreflect-stuff.v new file mode 100644 index 0000000..ee850e7 --- /dev/null +++ b/coq/misc/ssreflect-stuff.v @@ -0,0 +1,38 @@ +Require Import ssreflect. +Require Import Arith. + +Goal forall a b:nat, + a - b < 0 -> a < b. +Proof. + elim => [|a']. + - case => [|b']; first by []. + rewrite //= => H. + by have HH := PeanoNat.Nat.lt_irrefl 0. + - move => IH. + case => [|b']; first by []. + rewrite //= => H. + have HH := IH b' H. + exact: iffLR (PeanoNat.Nat.succ_lt_mono a' b') HH. +Qed. + + +Goal forall n:nat, + S n - 1 = n. +Proof. + move => n. + by rewrite PeanoNat.Nat.sub_succ_r. + (* by rewrite (PeanoNat.Nat.sub_succ_r (S n) 0). *) +Qed. + + +Goal forall n:nat, + S (S n) < 2 -> False. +Proof. + elim. + - exact: PeanoNat.Nat.lt_irrefl 2. + - move => n IH H. + apply: IH. + have HH := PeanoNat.Nat.lt_succ_l (S (S n)) 2. + exact: HH H. +Qed. + diff --git a/elisp/one.el b/elisp/one.el new file mode 100644 index 0000000..a7f35bb --- /dev/null +++ b/elisp/one.el @@ -0,0 +1,5 @@ +(defun foomar () + (interactive) + ;(message (region-beginning) (region-end)) + (message (evil-visual-beginning) (evil-visual-end)) +) diff --git a/fstar/hello.fst b/fstar/hello.fst new file mode 100644 index 0000000..4fb12d3 --- /dev/null +++ b/fstar/hello.fst @@ -0,0 +1,7 @@ +module Hello + +// let nat = x:int{x >= 0} + +let rec factorial n = + if n = 0 then 1 + else n * factorial (n-1) diff --git a/haskell/LucasPascal.hs b/haskell/LucasPascal.hs new file mode 100644 index 0000000..c35135b --- /dev/null +++ b/haskell/LucasPascal.hs @@ -0,0 +1,134 @@ +module Main where + +{- + - Level indexing starts from zero. + - Levels on top are of smaller index. + +Level 0 | 1 +Level 1 | 1 1 +Level 2 | 1 0 1 +Level 3 | 1 1 1 1 +Level 4 | 1 0 0 0 1 + -} + +-- | Find number to base b +nBaseB + :: Int -- ^ base + -> Int -- ^ number n + -> [Int] -- ^ digits of n to the base n. LSB first. +nBaseB n b + | n < b = [n] + | otherwise = rem:nBaseB nxt b + where + rem = mod n b + nxt = quot n b +{- +*Main> nBaseB 15 2 +[1,1,1,1] + +*Main> nBaseB 16 2 +[0,0,0,0,1] + +*Main> nBaseB 16 3 +[1,2,1] +-} + +-- | 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 = nBaseB a 2 + bbin = nBaseB b 2 + 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 + +{- +Enter max level: +32 + + 1 + 1 1 + 1 0 1 + 1 1 1 1 + 1 0 0 0 1 + 1 1 0 0 1 1 + 1 0 1 0 1 0 1 + 1 1 1 1 1 1 1 1 + 1 0 0 0 0 0 0 0 1 + 1 1 0 0 0 0 0 0 1 1 + 1 0 1 0 0 0 0 0 1 0 1 + 1 1 1 1 0 0 0 0 1 1 1 1 + 1 0 0 0 1 0 0 0 1 0 0 0 1 + 1 1 0 0 1 1 0 0 1 1 0 0 1 1 + 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 + 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 + 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 + 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 + 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 + 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 + 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 + 1 1 0 0 1 1 0 0 0 0 0 0 0 0 0 0 1 1 0 0 1 1 + 1 0 1 0 1 0 1 0 0 0 0 0 0 0 0 0 1 0 1 0 1 0 1 + 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 + 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 1 + 1 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0 1 1 + 1 0 1 0 0 0 0 0 1 0 1 0 0 0 0 0 1 0 1 0 0 0 0 0 1 0 1 + 1 1 1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1 + 1 0 0 0 1 0 0 0 1 0 0 0 1 0 0 0 1 0 0 0 1 0 0 0 1 0 0 0 1 + 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 + 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 + 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 +-} diff --git a/haskell/NumBase.hs b/haskell/NumBase.hs new file mode 100644 index 0000000..ff12294 --- /dev/null +++ b/haskell/NumBase.hs @@ -0,0 +1,32 @@ +-- | Find number to base b +base + :: Int -- ^ base + -> Int -- ^ number n + -> [Int] -- ^ digits of n to the base n. LSB first. +base b 0 = [0] +base b n + | n < b = [n] + | otherwise = rem:base b nxt + where + rem = mod n b + nxt = quot n b + +-- | Reverse a list +revList + :: [a] -- ^ Input list + -> [a] -- ^ output list +revList l = helper [] l + where + helper l [] = l + helper l (x:xs) = x:(helper l xs) + +listToStr + :: Show a + => [a] -- ^ Input list + -> String -- ^ Equivalent string +listToStr l = foldl (++) "" $ map show l + +{- +*Main> listToStr $ revList $ base 2 18 +"01001" +-} diff --git a/haskell/PostfixEval.hs b/haskell/PostfixEval.hs new file mode 100644 index 0000000..815f05a --- /dev/null +++ b/haskell/PostfixEval.hs @@ -0,0 +1,70 @@ +-- | Demo of state monad + +import Data.Char +import GHC.Float +import Control.Monad.State + + +-- | Process next input character +chrToOp + :: (Num a, Fractional a) + => Char -- ^ Character denoting an operation + -> (a -> a -> a) -- ^ Function corresponding to the operation + +chrToOp ch = + case ch of + '+' -> (+) + '-' -> (-) + '*' -> (*) + '/' -> (/) + + +-- | Process next input character +process_inp + :: Char -- ^ Next input character + -> [Float] -- ^ Current state of stack + -> [Float] -- ^ New state of stack + +process_inp ch st + | isDigit ch = [int2Float $ digitToInt ch] ++ st + | elem ch "+-*/" = [(chrToOp ch) (st!!1) (st!!0)] ++ (tail (tail st)) + | otherwise = st + + +postfixeval + :: String -- ^ Input string + -> State [Float] Float + +postfixeval [] = do + st <- get + return $ head st + +postfixeval (x:xs) = do + st <- get + let newst = process_inp x st + put newst + postfixeval xs + +-- main = print $ fst $ runState (postfixeval "32+") [] +main = do + putStrLn "Enter the postfix expression:" + inp <- getLine + print $ fst $ runState (postfixeval inp) [] + + +{- +λ> fst $ runState (postfixeval "32+2*6-2/") [] +2.0 + +λ> fst $ runState (postfixeval "32+") [] +-} + +{- +Enter the postfix expression: +32+ +5.0 + +Enter the postfix expression: +32+2*6-2/ +2.0 +-} diff --git a/haskell/calc.hs b/haskell/calc.hs new file mode 100644 index 0000000..1b6f57e --- /dev/null +++ b/haskell/calc.hs @@ -0,0 +1,24 @@ +data Result a + = Ok a String + | Err + deriving (Eq, Show) + +{- +https://hub.darcs.net/ppk/calculator/browse/src/Parser.hs +-} +data Op = Plus | Mult + +data Ast + = Val Int + | Expr Op Ast Ast + +opDe :: Op -> (Int -> Int -> Int) +opDe Plus = (+) +opDe Mult = (*) + +astDe :: Ast -> Int +astDe (Val n) = n +astDe (Expr op e1 e2) = (opDe op) (astDe e1) (astDe e2) + +eg1 = Expr Plus (Val 2) (Expr Mult (Val 3) (Val 2)) +a = astDe eg1 diff --git a/haskell/clash/FullAdder.hs b/haskell/clash/FullAdder.hs new file mode 100644 index 0000000..338c836 --- /dev/null +++ b/haskell/clash/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/MAC.hs b/haskell/clash/MAC.hs new file mode 100644 index 0000000..4159382 --- /dev/null +++ b/haskell/clash/MAC.hs @@ -0,0 +1,36 @@ +-- | 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) + +topFn :: (Num a) => a -> (a, a) -> (a, a) +topFn 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 $ mealy topFn 0 +--topEntity = exposeClockResetEnable macS diff --git a/haskell/clash/mux.hs b/haskell/clash/mux.hs new file mode 100644 index 0000000..f443a61 --- /dev/null +++ b/haskell/clash/mux.hs @@ -0,0 +1,25 @@ +module MUX where -- MUX2 + +import Clash.Prelude + +mux2 :: () -> (a, a, Bool) -> ((), a) +mux2 _ (x, y, sel) = + case sel of + False -> ((), x) + _ -> ((), y) + +-- *MAC> mux2 () (3, 2, False) +-- ((),3) +-- *MAC> mux2 () (3, 2, True) +-- ((),2) + +mux2S :: (HiddenClockResetEnable dom, Num a, NFDataX a) => Signal dom (a, a, Bool) -> Signal dom a +mux2S = mealy mux2 () + +topEntity + :: Clock System + -> Reset System + -> Enable System + -> Signal System (Int, Int, Bool) + -> Signal System Int +topEntity = exposeClockResetEnable mux2S diff --git a/haskell/clash/rand.hs b/haskell/clash/rand.hs new file mode 100644 index 0000000..8cc4fff --- /dev/null +++ b/haskell/clash/rand.hs @@ -0,0 +1,38 @@ +import Clash.Prelude + +type Matrix a rows cols = Vec rows (Vec cols a) + +getNthCol + :: (KnownNat rows, KnownNat cols) + => Matrix a rows cols -- matrix + -> Int -- n + -> Vec rows a -- nth column of matrix +getNthCol mat n = map (\rw -> rw !! n) mat + +transpRow + :: KnownNat n + => Vec n a + -> Matrix a n 1 +transpRow Nil = Nil +transpRow v = ((head v) :> Nil) :> (transpRow $ tail v) +--transpRow (x :> xs) = (x :> Nil) :> (transpRow xs) + + +dotProduct + :: (KnownNat n, Num a) + => Vec n a + -> Vec n a + -> a +dotProduct p q + = foldr (\x acc -> acc+x) 0 + $ map (\x -> (fst x)*(snd x)) + $ zipWith (,) p q + +-- matProd p q + +eg1 + = (0 :> 1 :> 2 :> Nil) :> + (3 :> 4 :> 5 :> Nil) :> + Nil +-- λ> getNthCol eg1 0 +-- 0 :> 3 :> Nil diff --git a/latex/tikz/example2.tex b/latex/tikz/example2.tex new file mode 100644 index 0000000..8a1d631 --- /dev/null +++ b/latex/tikz/example2.tex @@ -0,0 +1,51 @@ + +\documentclass{article} +\usepackage{tikz} +\usetikzlibrary{arrows,positioning} +\usetikzlibrary{arrows.meta,chains,shapes.geometric} +\usetikzlibrary{decorations.pathreplacing} + + +\begin{document} + +\begin{figure}%[h] + \centering + \begin{tikzpicture}[ + proc/.style = {rectangle, minimum width=5mm, minimum height=5mm, text centered, draw=black} + ] + \node (input)[align=center] {Input\\ symbol}; + \node (tf) [proc,align=center,right of=input,xshift=20mm] {Transition\\ function}; + \node (output)[right of=tf,xshift=15mm,yshift=2.5mm] {Judgement}; + + \draw[->] (input) -- (tf); + \draw[->] (tf.15) -- (output); + \end{tikzpicture} + +% \begin{tikzpicture}[ +% node distance = 4mm and 8mm, +% arrow/.style = {-Straight Barb}, +% block/.style = {draw, minimum height=12mm, text width=31mm, align=center} +% ] +% \node (judgement) [block] {Judgement}; +% \node (state) [block, below=of judgement] {FA state}; +% \node[above] at (judgement.north) {Combinatory}; +% \node[below] at (state.south) {Sequential}; +% %([yshift=-10pt]state.west) +% +% \node[left] at ([xshift=-2mm, yshift=1.5mm]judgement.190) {$r$}; +% \node[left] at ([xshift=8mm, yshift=-2mm]state.east) {$r_{in}$}; +% %\draw[arrow] (state.170) -- ++(-4mm,0) |- (judgement.190); +% +% \coordinate[left=of judgement.170, label=left:$D$] (Input symbol); +% \coordinate[left=of state.190, label=left:$clk$] (clk); +% \coordinate[right=of judgement.10, label=right:$Q$] (Q); +% \draw[arrow] (D) -- (D -| judgement.west); +% \draw[arrow] (clk) -- (clk -| state.west); +% \draw[arrow] (Q -| judgement.east) -- (Q); +% \draw[arrow] (state.170) -- ++(-4mm,0) |- (judgement.190); +% \draw[arrow] (judgement.350) -- ++(4mm,0) |- (state.east); +% \end{tikzpicture} +\end{figure} + + +\end{document}