a mass commit
This commit is contained in:
parent
2d42a67707
commit
07640878c6
|
|
@ -7,45 +7,44 @@ number of cycles and if it doesn't give False. Else keep giving True.
|
|||
-}
|
||||
|
||||
import Clash.Prelude
|
||||
import Clash.Explicit.Testbench -- For simulation and testing
|
||||
import Clash.Explicit.Testbench
|
||||
|
||||
-- data NoNF = Unl Int NoNF
|
||||
-- λ> a = Unl 3 a
|
||||
|
||||
data State =
|
||||
Good
|
||||
| Bad
|
||||
| Tolerating Int
|
||||
deriving (Generic, NFDataX, Show) -- ADDED
|
||||
|
||||
monTf :: Int -> ((,) Int Int) -> State -> ((,) Int Int) -> (,) State Bool
|
||||
monTf limit bounds st ab =
|
||||
let {a = fst ab} in
|
||||
let {b = snd ab} in
|
||||
let {low = fst bounds} in
|
||||
let {high = snd bounds} in
|
||||
let {res = (+) a b} in
|
||||
let {outsideLimits = (||) ((<) res low) ((>) res high)} in
|
||||
case st of {
|
||||
Good ->
|
||||
case outsideLimits of {
|
||||
True -> (,) (Tolerating (succ 0)) True;
|
||||
False -> (,) Good True};
|
||||
Bad -> (,) Bad False;
|
||||
Tolerating failCount ->
|
||||
case outsideLimits of {
|
||||
True ->
|
||||
case (==) failCount limit of {
|
||||
True -> (,) Bad False;
|
||||
False -> (,) (Tolerating (succ failCount)) True};
|
||||
False -> (,) Good True}}
|
||||
|
||||
-- | Monitor state
|
||||
data State
|
||||
= Good -- ^ No intolerable violation
|
||||
| Bad -- ^ Violation beyond tolerance
|
||||
| Tolerating Word -- ^ Tolerating violation
|
||||
deriving (Generic, NFDataX)
|
||||
|
||||
monTf
|
||||
:: (Num a, Ord a)
|
||||
=> Word -- ^ Tolerance limit (inclusive)
|
||||
-> (a, a) -- ^ Lowest and highest allowed values
|
||||
-> State -- ^ Current state
|
||||
-> (a, a) -- ^ Input values
|
||||
-> (State, Bool) -- ^ Next state and output
|
||||
monTf limit (low, high) s (a, b) = case s of
|
||||
Good ->
|
||||
if outsideLimits res then
|
||||
(Tolerating 1, True)
|
||||
else
|
||||
(Good, True)
|
||||
Bad -> (Bad, False)
|
||||
Tolerating failCount ->
|
||||
if outsideLimits res then
|
||||
--if failCount > limit then -- Spec mismatch. Tolerance is inclusive
|
||||
if failCount == limit then
|
||||
(Bad, False)
|
||||
else
|
||||
(Tolerating (failCount+1), True)
|
||||
else
|
||||
(Good, True)
|
||||
where
|
||||
res = a + b
|
||||
outsideLimits val = val < low && val > high
|
||||
|
||||
mon
|
||||
:: SystemClockResetEnable
|
||||
=> Signal System (Signed 8, Signed 8)
|
||||
=> Signal System (Int, Int)
|
||||
-> Signal System Bool
|
||||
mon = mealy tf Good
|
||||
where
|
||||
|
|
@ -55,32 +54,133 @@ topEntity
|
|||
:: Clock System
|
||||
-> Reset System
|
||||
-> Enable System
|
||||
-> Signal System (Signed 8, Signed 8)
|
||||
-> Signal System (Int, Int)
|
||||
-> Signal System Bool
|
||||
topEntity = exposeClockResetEnable mon
|
||||
|
||||
|
||||
testBench :: Signal System Bool
|
||||
testBench = done
|
||||
where
|
||||
testInput = stimuliGenerator clk rst
|
||||
$(listToVecTH [(10, 15) :: (Signed 8, Signed 8),
|
||||
(25, 12),
|
||||
(23, 30),
|
||||
(1, 4)])
|
||||
expectedOutput = outputVerifier' clk rst
|
||||
$(listToVecTH [True,
|
||||
True,
|
||||
False,
|
||||
False])
|
||||
done = expectedOutput (topEntity clk rst (enableGen) testInput)
|
||||
clk = tbSystemClockGen (not <$> done)
|
||||
rst = systemResetGen
|
||||
|
||||
{-
|
||||
λ> import qualified Data.List
|
||||
λ> Data.List.take 5 $ sample testBench
|
||||
[False,False,False,False,False]
|
||||
-}
|
||||
|
||||
--Data.List.take 5 $ sample $ exposeClockResetEnable mon
|
||||
|
||||
|
||||
|
||||
-- -- | Monitor state
|
||||
-- data State
|
||||
-- = Good -- ^ No intolerable violation
|
||||
-- | Bad -- ^ Violation beyond tolerance
|
||||
-- | Tolerating Word -- ^ Tolerating violation
|
||||
-- deriving (Generic, NFDataX, Show)
|
||||
|
||||
-- monTf
|
||||
-- :: (Num a, Ord a)
|
||||
-- => Word -- ^ Tolerance limit (inclusive)
|
||||
-- -> (a, a) -- ^ Lowest and highest allowed sum
|
||||
-- -> State -- ^ Current state
|
||||
-- -> (a, a) -- ^ Input values
|
||||
-- -> (State, Bool) -- ^ Next state and output
|
||||
-- monTf limit (low, high) s (a, b) = case s of
|
||||
-- Good ->
|
||||
-- if outsideLimits res then
|
||||
-- (Tolerating 1, True)
|
||||
-- else
|
||||
-- (Good, True)
|
||||
-- Bad -> (Bad, False)
|
||||
-- Tolerating failCount ->
|
||||
-- if outsideLimits res then
|
||||
-- --if failCount > limit then -- Spec mismatch. Tolerance is inclusive
|
||||
-- if failCount == limit then
|
||||
-- (Bad, False)
|
||||
-- else
|
||||
-- (Tolerating (failCount+1), True)
|
||||
-- else
|
||||
-- (Good, True)
|
||||
-- where
|
||||
-- res = a + b
|
||||
-- outsideLimits val = val < low || val > high
|
||||
|
||||
-- mon
|
||||
-- :: SystemClockResetEnable
|
||||
-- => Signal System (Signed 8, Signed 8)
|
||||
-- -> Signal System Bool
|
||||
-- mon = mealy tf Good
|
||||
-- where
|
||||
-- tf = monTf 2 (10, 20)
|
||||
|
||||
-- topEntity
|
||||
-- :: Clock System
|
||||
-- -> Reset System
|
||||
-- -> Enable System
|
||||
-- -> Signal System (Signed 8, Signed 8)
|
||||
-- -> Signal System Bool
|
||||
-- topEntity = exposeClockResetEnable mon
|
||||
|
||||
|
||||
-- testBench :: Signal System Bool
|
||||
-- testBench = done
|
||||
-- where
|
||||
-- testInput = stimuliGenerator clk rst
|
||||
-- $(listToVecTH [(10, 15) :: (Signed 8, Signed 8),
|
||||
-- (25, 12),
|
||||
-- (23, 30),
|
||||
-- (1, 4)])
|
||||
-- expectedOutput = outputVerifier' clk rst
|
||||
-- $(listToVecTH [True,
|
||||
-- True,
|
||||
-- False,
|
||||
-- False])
|
||||
-- done = expectedOutput (topEntity clk rst (enableGen) testInput)
|
||||
-- clk = tbSystemClockGen (not <$> done)
|
||||
-- rst = systemResetGen
|
||||
|
||||
-- {-
|
||||
-- λ> monTf 2 (10,20) (Good) (10,15)
|
||||
-- (Tolerating 1,True)
|
||||
|
||||
-- λ> monTf 2 (10,20) (Tolerating 1) (25,12)
|
||||
-- (Tolerating 2,True)
|
||||
|
||||
-- λ> monTf 2 (10,20) (Tolerating 2) (23,30)
|
||||
-- (Bad,False)
|
||||
|
||||
|
||||
-- -----------------------
|
||||
|
||||
-- λ> monTf 2 (5,10) (Good) (0,1)
|
||||
-- (Tolerating 1,True)
|
||||
|
||||
-- λ> monTf 2 (5,10) (Tolerating 2) (0,1)
|
||||
-- (Bad,False)
|
||||
|
||||
-- λ> monTf 2 (5,10) (Tolerating 1) (0,1)
|
||||
-- (Tolerating 2,True)
|
||||
|
||||
-- λ> monTf 2 (5,10) (Bad) (0,1)
|
||||
-- (Bad,False)
|
||||
-- -}
|
||||
|
||||
-- {-
|
||||
-- λ> import qualified Data.List
|
||||
-- λ> Data.List.take 5 $ sample testBench
|
||||
-- [False,False,False,False,False]
|
||||
-- -}
|
||||
|
||||
-- --Data.List.take 5 $ sample $ exposeClockResetEnable mon
|
||||
|
||||
|
||||
|
||||
|
||||
-- -- [nix-shell:~/gits/playground/clash]$ clash --vhdl MonWithTolerance.hs
|
||||
-- -- GHC: Setting up GHC took: 0.697s
|
||||
-- -- GHC: Compiling and loading modules took: 3.549s
|
||||
-- -- Clash: Parsing and compiling primitives took 0.195s
|
||||
-- -- GHC+Clash: Loading modules cumulatively took 4.757s
|
||||
-- -- Clash: Compiling Main.testBench
|
||||
-- -- Clash: Compiling Main.topEntity
|
||||
-- -- Clash: Normalization took 0.090s
|
||||
-- -- Clash: Netlist generation took 0.000s
|
||||
-- -- Clash: Normalization took 0.117s
|
||||
-- -- Clash: Netlist generation took 0.002s
|
||||
-- -- Clash: Compiling Main.topEntity took 0.163s
|
||||
-- -- Clash: Compiling Main.testBench took 0.183s
|
||||
-- -- Clash: Total compilation took 4.943s
|
||||
|
||||
|
|
|
|||
|
|
@ -103,3 +103,4 @@ Extract Constant Init.Nat.modulo => "(\n m -> if m == 0 then n else mod n m)".
|
|||
Extract Inlined Constant snd => "snd".
|
||||
|
||||
Recursive Extraction monTf.
|
||||
Extraction "out.hs" monTf.
|
||||
|
|
|
|||
|
|
@ -90,3 +90,12 @@ Proof.
|
|||
intros lem dem.
|
||||
subst dem.
|
||||
intro dm.
|
||||
Abort.
|
||||
|
||||
Goal forall a b:Prop,
|
||||
~a \/ ~b -> ~(a /\ b).
|
||||
Proof.
|
||||
intros a b HaOrb Hab.
|
||||
destruct Hab as [Ha Hb].
|
||||
destruct HaOrb; apply H; assumption.
|
||||
Qed.
|
||||
|
|
|
|||
|
|
@ -13,11 +13,13 @@ Inductive member {A:Type} (elem:A): list A -> Type :=
|
|||
| HNext: forall (a:A) (l:list A),
|
||||
member elem l -> member elem (a::l).
|
||||
|
||||
(*
|
||||
Fixpoint hget {A:Type} {B:A->Type} {ts:list A}
|
||||
(l: hlist B ts) (elem: A): member elem ts -> B elem :=
|
||||
match l with
|
||||
|
|
||||
end.
|
||||
*)
|
||||
|
||||
|
||||
(* https://coq-community.org/coq-ext-lib/v0.10.3/ExtLib.Data.HList.html *)
|
||||
|
|
@ -114,3 +116,7 @@ Compute htl eg2.
|
|||
|
||||
Compute eg1 ++ eg2 ++ eg2.
|
||||
(* = « 3; 3; true; 3; true » *)
|
||||
|
||||
Require Import Extraction.
|
||||
Recursive Extraction hlist.
|
||||
|
||||
|
|
|
|||
|
|
@ -1,15 +0,0 @@
|
|||
-R _build/default/theories aruvi
|
||||
#_build/default/theories/Nfa.v
|
||||
#_build/default/theories/FinTyp.v
|
||||
|
||||
-I /media/julinusername/eins/gits/math-comp/mathcomp
|
||||
-R /media/julinusername/eins/gits/math-comp/mathcomp mathcomp
|
||||
|
||||
-arg -w -arg -projection-no-head-constant
|
||||
-arg -w -arg -redundant-canonical-projection
|
||||
-arg -w -arg -notation-overridden
|
||||
-arg -w -arg +duplicate-clear
|
||||
-arg -w -arg +non-primitive-record
|
||||
-arg -w -arg +undeclared-scope
|
||||
-arg -w -arg +deprecated-hint-rewrite-without-locality
|
||||
-arg -w -arg -elpi.add-const-for-axiom-or-sectionvar
|
||||
|
|
@ -140,6 +140,21 @@ Example eg7: 'rV_2 :=
|
|||
Check 1%:M: 'M_2.
|
||||
Check eg7.
|
||||
|
||||
Require Import Extraction.
|
||||
Extraction Language Haskell.
|
||||
Require Import ExtrHaskellBasic.
|
||||
Require Import ExtrHaskellZInteger.
|
||||
Require Import ExtrHaskellNatNum.
|
||||
|
||||
Extract Inductive Bool.reflect => "Bool" [ "True" "False" ].
|
||||
|
||||
|
||||
Example eg7' := Eval lazy in (\row_(i<2) (if i==0 then true else false)).
|
||||
(* Compute eg7. *)
|
||||
(* Compute eg7'. *)
|
||||
Recursive Extraction eg7'.
|
||||
|
||||
|
||||
Example eg8: 'cV_2 :=
|
||||
\col_(i<2) (if i!=0 then true else false).
|
||||
Check eg7 *m eg8.
|
||||
|
|
@ -233,16 +248,16 @@ Check 'M[bool]_(3, 4).
|
|||
|
||||
Local Open Scope ring_scope.
|
||||
|
||||
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.
|
||||
(* 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. *)
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -5,6 +5,20 @@ Import ListNotations.
|
|||
|
||||
Require Import ssreflect ssrbool.
|
||||
|
||||
(* Module Other. *)
|
||||
(* (1* Same as [PeanoNat.Nat.eqb_eq] *1) *)
|
||||
(* Theorem eqb_eq: forall (n1 n2: nat), *)
|
||||
(* Nat.eqb n1 n2 = true <-> n1 = n2. *)
|
||||
(* Proof. *)
|
||||
(* move => n1 n2. *)
|
||||
(* case (Nat.eqb n1 n2) eqn:H. *)
|
||||
(* - by rewrite PeanoNat.Nat.eqb_eq in H. *)
|
||||
(* - by rewrite PeanoNat.Nat.eqb_neq in H. *)
|
||||
(* Qed. *)
|
||||
(* End Other. *)
|
||||
|
||||
(* Import Other. *)
|
||||
|
||||
Theorem filter_not_empty_In : forall (n: nat) (l: list nat),
|
||||
(filter (fun x => Nat.eqb n x) l) <> [] ->
|
||||
In n l.
|
||||
|
|
@ -12,7 +26,7 @@ Proof.
|
|||
move => n l.
|
||||
elim: l => [|a l IH]; first by [].
|
||||
rewrite //=.
|
||||
destruct (Nat.eqb n a) eqn:H.
|
||||
case (Nat.eqb n a) eqn:H.
|
||||
- rewrite PeanoNat.Nat.eqb_eq in H => HH.
|
||||
by left.
|
||||
- rewrite PeanoNat.Nat.eqb_neq in H => HH.
|
||||
|
|
@ -37,7 +51,51 @@ Qed.
|
|||
Theorem reflect_iff: forall (P: Prop) (b: bool),
|
||||
reflect P b -> (P <-> b = true).
|
||||
Proof.
|
||||
move => P b.
|
||||
case b => H.
|
||||
- case H.
|
||||
+ rewrite HH.
|
||||
move => P b H.
|
||||
by split; case H.
|
||||
Qed.
|
||||
|
||||
Lemma eqbP : forall (n m: nat),
|
||||
reflect (n = m) (Nat.eqb n m).
|
||||
Proof.
|
||||
move => n m.
|
||||
case (Nat.eqb n m) eqn:H.
|
||||
- apply ReflectT.
|
||||
by rewrite PeanoNat.Nat.eqb_eq in H.
|
||||
- apply ReflectF.
|
||||
by rewrite PeanoNat.Nat.eqb_neq in H. (* ✓ *)
|
||||
Restart. (* Another way *)
|
||||
move => n m.
|
||||
apply iff_reflect.
|
||||
apply (iff_sym (PeanoNat.Nat.eqb_eq n m)).
|
||||
Qed.
|
||||
|
||||
Theorem filter_not_empty_In' : forall (n: nat) (l: list nat),
|
||||
filter (fun x => Nat.eqb n x) l <> [] ->
|
||||
In n l.
|
||||
Proof.
|
||||
move => n l.
|
||||
elim l => [|a l' IH]; first by [].
|
||||
move => H.
|
||||
case (eqbP a n) => Hr.
|
||||
- rewrite Hr.
|
||||
by apply in_eq. (* or just [left] *)
|
||||
- right.
|
||||
apply IH.
|
||||
Abort.
|
||||
|
||||
Require Import Arith.
|
||||
Fixpoint count (n: nat) (l: list nat): nat :=
|
||||
match l with
|
||||
| [] => 0
|
||||
| m :: l' => (if n =? m then 1 else 0) + count n l'
|
||||
end.
|
||||
|
||||
Theorem eqbP_practice : forall (n: nat) (l: list nat),
|
||||
count n l = 0 -> ~(In n l).
|
||||
Proof.
|
||||
move => n l.
|
||||
elim l => [| a l' IH]; first by move => _.
|
||||
case (eqbP n a) => H.
|
||||
- rewrite //=.
|
||||
|
||||
|
|
|
|||
|
|
@ -5,6 +5,19 @@
|
|||
From ExtLib Require Import HList.
|
||||
From ExtLib Require Import Member.
|
||||
|
||||
Require Import Program.
|
||||
|
||||
|
||||
Fail Program Fixpoint foo {A:Type} (A_beq: A -> A -> bool)
|
||||
(a:A): forall (l:list A), member a l := fun l =>
|
||||
match l with
|
||||
| nil => _
|
||||
| cons x xs =>
|
||||
if A_beq x a then MZ _ _
|
||||
else foo A_beq a xs
|
||||
end.
|
||||
|
||||
|
||||
(*
|
||||
s ∈ l1 -> s ∈ l1++l2
|
||||
*)
|
||||
|
|
@ -58,6 +71,35 @@ Example eg2 := «2; true»: hlist (fun x:Set=>x) [nat; bool].
|
|||
Example eg3 := «(0,3)» : hlist (fun x:Set=>(x*nat)%type) [nat].
|
||||
Example eg4 := «2; true; "h"; (2,3)»: hlist (fun x:Set=>x) [nat; bool; string; (nat*nat)%type].
|
||||
|
||||
Example eg5 := [0; 1].
|
||||
Print member.
|
||||
Check MN _ (MZ _ _): member 1 eg5.
|
||||
Fail Check [MZ _ _: member 0 eg5; MN _ (MZ _ _)].
|
||||
Example mm5 := «MZ _ _; MN _ (MZ _ _)»: hlist (fun t => t) [member 0 eg5; member 1 eg5].
|
||||
Check mm5.
|
||||
Example mm5' := «MZ _ _; MN _ (MZ _ _)»: hlist ((fun l => (fun x => member x l)) eg5) [0; 1].
|
||||
Example mm5'2 := «MZ _ _; MN _ (MZ _ _)»: hlist ((fun l x => member x l) eg5) [0; 1].
|
||||
Example mm5'3 := «MZ _ _; MN _ (MZ _ _)»: hlist ((fun l x => member x l) eg5) eg5.
|
||||
|
||||
|
||||
Section Foo.
|
||||
Context {A T:Type}.
|
||||
Variables (l:list A).
|
||||
Fail Variable f: forall (l:list A) (x:B), member x l.
|
||||
|
||||
Variable f': list T -> T -> Type.
|
||||
Variable f: forall (ts:list T) (x:T), member x ts.
|
||||
Variable ts: list T.
|
||||
Variable a: A.
|
||||
|
||||
Fixpoint foo (hls: hlist (f l) ts) (a: A)
|
||||
|
||||
foo (hl: hlist (f l) [member x l]): hlist (f l) [member x (l++[a])
|
||||
|
||||
End Foo.
|
||||
|
||||
|
||||
|
||||
|
||||
Check «» : hlist (fun x:Set=>x) [].
|
||||
(* « » : hlist (fun x : Set => x) [] *)
|
||||
|
|
@ -124,6 +166,9 @@ Compute hlist_gen (fun x=>x) [1].
|
|||
|
||||
|
||||
Infix "∈" := member (at level 50).
|
||||
|
||||
|
||||
|
||||
Compute memberappL (cons 2 nil) (MZ 3 (cons 3 nil)).
|
||||
Fail Compute memberappR (cons 2 nil) (MZ _ (cons 3 nil)).
|
||||
|
||||
|
|
|
|||
108
haskell/Hlist.hs
108
haskell/Hlist.hs
|
|
@ -3,56 +3,66 @@
|
|||
{-# LANGUAGE TypeOperators #-} -- Enabled by default apparently
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
|
||||
data Hlist :: [*] -> * where
|
||||
HNil :: Hlist '[]
|
||||
HCons :: t -> Hlist ts -> Hlist (t : ts)
|
||||
|
||||
data Member :: a -> [*] -> * where
|
||||
First :: Member x (x':l)
|
||||
Next :: Member x l -> Member x (x':l)
|
||||
|
||||
-- data Member x (l':ls) where
|
||||
-- First :: Member x (l:ls)
|
||||
-- Next :: Member x ls -> Member x (l:ls)
|
||||
|
||||
hd :: Hlist (t ': ts) -> t
|
||||
hd (HCons x _) = x
|
||||
|
||||
tl :: Hlist (t ': ts) -> Hlist ts
|
||||
tl (HCons _ xs) = xs
|
||||
|
||||
len :: Hlist ts -> Int
|
||||
len HNil = 0
|
||||
len (HCons _ xs) = 1 + (len xs)
|
||||
|
||||
type family (++) (l1 :: [*]) (l2 :: [*]) where
|
||||
'[] ++ y = y
|
||||
(x':xs) ++ y = x':(xs ++ y)
|
||||
|
||||
cat :: Hlist ts1 -> Hlist ts2 -> Hlist (ts1 ++ ts2)
|
||||
cat HNil y = y
|
||||
cat (HCons x xs) y = HCons x (cat xs y)
|
||||
|
||||
|
||||
data HList :: (* -> *) -> [*] -> * where
|
||||
HNil :: HList f '[]
|
||||
HCons :: f t -> HList f ts -> HList f (t':ts)
|
||||
|
||||
|
||||
-- Example hlists
|
||||
a = HCons 3 HNil
|
||||
b = HCons 3 (HCons True HNil)
|
||||
-- λ> a
|
||||
-- a :: Hlist '[Integer]
|
||||
-- λ> b
|
||||
-- b :: Hlist '[Integer, Bool]
|
||||
-- λ> tl a
|
||||
--
|
||||
-- tl a :: Hlist '[]
|
||||
-- λ> tl b
|
||||
-- tl b :: Hlist '[Bool]
|
||||
-- λ> hd a
|
||||
-- 3
|
||||
-- λ> hd (tl b)
|
||||
-- True
|
||||
-- λ> hd $ tl (tl b) -- Error
|
||||
--
|
||||
-- λ> cat b b
|
||||
-- cat b b :: Hlist '[Integer, Bool, Integer, Bool]
|
||||
-- a = HCons 3 HNil
|
||||
|
||||
|
||||
|
||||
|
||||
---------------------------------------------------------------------------
|
||||
|
||||
-- data Hlist :: [*] -> * where
|
||||
-- HNil :: Hlist '[]
|
||||
-- HCons :: t -> Hlist ts -> Hlist (t : ts)
|
||||
|
||||
-- data Member :: a -> [*] -> * where
|
||||
-- First :: Member x (y:l)
|
||||
-- Next :: Member x l -> Member x (y:l)
|
||||
|
||||
-- hd :: Hlist (t ': ts) -> t
|
||||
-- hd (HCons x _) = x
|
||||
|
||||
-- tl :: Hlist (t ': ts) -> Hlist ts
|
||||
-- tl (HCons _ xs) = xs
|
||||
|
||||
-- len :: Hlist ts -> Int
|
||||
-- len HNil = 0
|
||||
-- len (HCons _ xs) = 1 + (len xs)
|
||||
|
||||
-- type family (++) (l1 :: [*]) (l2 :: [*]) where
|
||||
-- '[] ++ y = y
|
||||
-- (x':xs) ++ y = x':(xs ++ y)
|
||||
|
||||
-- cat :: Hlist ts1 -> Hlist ts2 -> Hlist (ts1 ++ ts2)
|
||||
-- cat HNil y = y
|
||||
-- cat (HCons x xs) y = HCons x (cat xs y)
|
||||
|
||||
|
||||
|
||||
|
||||
-- -- Example hlists
|
||||
-- a = HCons 3 HNil
|
||||
-- b = HCons 3 (HCons True HNil)
|
||||
-- -- λ> a
|
||||
-- -- a :: Hlist '[Integer]
|
||||
-- -- λ> b
|
||||
-- -- b :: Hlist '[Integer, Bool]
|
||||
-- -- λ> tl a
|
||||
-- --
|
||||
-- -- tl a :: Hlist '[]
|
||||
-- -- λ> tl b
|
||||
-- -- tl b :: Hlist '[Bool]
|
||||
-- -- λ> hd a
|
||||
-- -- 3
|
||||
-- -- λ> hd (tl b)
|
||||
-- -- True
|
||||
-- -- λ> hd $ tl (tl b) -- Error
|
||||
-- --
|
||||
-- -- λ> cat b b
|
||||
-- -- cat b b :: Hlist '[Integer, Bool, Integer, Bool]
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ module AExpr where
|
|||
import qualified Parser as P
|
||||
|
||||
data E
|
||||
= Const Int
|
||||
= Cnst Int
|
||||
| Add E E
|
||||
| Sub E E
|
||||
| Mul E E
|
||||
|
|
@ -11,35 +11,39 @@ data E
|
|||
|
||||
eval :: E -> Int
|
||||
eval e = case e of
|
||||
Const n -> n
|
||||
Cnst n -> n
|
||||
Add e1 e2 -> (eval e1) + (eval e2)
|
||||
Sub e1 e2 -> (eval e1) - (eval e2)
|
||||
Mul e1 e2 -> (eval e1) * (eval e2)
|
||||
|
||||
|
||||
|
||||
parser :: P.Parser E
|
||||
parser = P.chainl cnst op
|
||||
parser = aconst
|
||||
where
|
||||
--cnst :: P.Parser E
|
||||
cnst = do {
|
||||
P.spaces
|
||||
; n <- P.nat
|
||||
; return $ (Const . read) n
|
||||
}
|
||||
--op :: P.Parser (E -> E -> E)
|
||||
op = do {
|
||||
P.spaces
|
||||
; sym <- P.choice $ map P.char "+-*"
|
||||
; return $
|
||||
case sym of
|
||||
'+' -> Add
|
||||
'-' -> Sub
|
||||
'*' -> Mul
|
||||
}
|
||||
aconst = (Cnst . read) <$> (P.spaces *> P.nat)
|
||||
|
||||
-- parser :: P.Parser E
|
||||
-- parser = P.chainl cnst op
|
||||
-- where
|
||||
-- --cnst :: P.Parser E
|
||||
-- cnst = do {
|
||||
-- P.spaces
|
||||
-- ; n <- P.nat
|
||||
-- ; return $ (Cnst . read) n
|
||||
-- }
|
||||
-- --op :: P.Parser (E -> E -> E)
|
||||
-- op = do {
|
||||
-- P.spaces
|
||||
-- ; sym <- P.choice $ map P.char "+-*"
|
||||
-- ; return $
|
||||
-- case sym of
|
||||
-- '*' -> Mul
|
||||
-- '+' -> Add
|
||||
-- '-' -> Sub
|
||||
-- }
|
||||
|
||||
|
||||
-- λ> P.parse AE.parser "2 * 3"
|
||||
-- Ok (Mul (Const 2) (Const 3)) ""
|
||||
-- Ok (Mul (Cnst 2) (Cnst 3)) ""
|
||||
-- λ> P.parse AE.parser "2 * 3 + 4"
|
||||
-- Ok (Add (Mul (Const 2) (Const 3)) (Const 4)) ""
|
||||
-- Ok (Add (Mul (Cnst 2) (Cnst 3)) (Cnst 4)) ""
|
||||
|
|
|
|||
|
|
@ -16,21 +16,24 @@ data E
|
|||
deriving Show
|
||||
|
||||
parser :: P.Parser E
|
||||
parser = bconst
|
||||
parser = andOp -- lesser precedence comes first
|
||||
<|> aOp
|
||||
<|> notOp
|
||||
<|> aOp
|
||||
<|> aOp
|
||||
<|> bconst
|
||||
where
|
||||
bconst = do {
|
||||
P.spaces
|
||||
; bval <- P.choice $ map P.string ["true", "false"]
|
||||
; return $ (Cnst . strToBool) bval
|
||||
}
|
||||
notOp = do {
|
||||
e <- notOpP
|
||||
P.spaces
|
||||
; e <- P.string "~" *> P.spaces *> parser
|
||||
; return $ Not e
|
||||
}
|
||||
aOp = do {
|
||||
x <- AE.parser
|
||||
P.spaces
|
||||
; x <- AE.parser
|
||||
; P.spaces
|
||||
; opcode <- P.choice $ map P.string ["==", "!=", "<=", ">"]
|
||||
; P.spaces
|
||||
|
|
@ -42,14 +45,15 @@ parser = bconst
|
|||
">" -> Gt x y
|
||||
}
|
||||
andOp = do {
|
||||
x <- parser
|
||||
P.spaces
|
||||
; x <- parser
|
||||
; P.spaces
|
||||
; opcode <- P.string "&&"
|
||||
; P.string "&&"
|
||||
; P.spaces
|
||||
; y <- parser
|
||||
; return $ And x y
|
||||
}
|
||||
notOpP = P.string "~" *> P.spaces *> parser
|
||||
-- notOpP = P.string "~" *> P.spaces *> parser
|
||||
strToBool s = if s == "true" then True else False
|
||||
|
||||
eval :: E -> Bool
|
||||
|
|
|
|||
|
|
@ -1,16 +1,21 @@
|
|||
module Expr where
|
||||
|
||||
import Control.Applicative -- for `Alternative' typeclass
|
||||
|
||||
import qualified AExpr as AE
|
||||
import qualified BExpr as BE
|
||||
import qualified Dict
|
||||
import qualified Parser as P
|
||||
|
||||
data Stmt
|
||||
= Skip
|
||||
= Skip -- for empty 'if' and 'while' body
|
||||
| Assign String AE.E
|
||||
| Seq Stmt Stmt
|
||||
| If BE.E Stmt Stmt
|
||||
| While BE.E Stmt
|
||||
|
||||
parser :: P.Parser Stmt
|
||||
|
||||
type Env = [(String, Int)]
|
||||
|
||||
eval :: Env -> Stmt -> Env
|
||||
|
|
|
|||
|
|
@ -1,68 +0,0 @@
|
|||
{-
|
||||
An experiment with Clash: Experiment 2
|
||||
|
||||
Okay, this failed as expected. Because it isn't as trivial as Experiment 1.
|
||||
`List.length' function is involved and its definition is recursive.
|
||||
-}
|
||||
|
||||
module Exp where
|
||||
|
||||
import Clash.Prelude
|
||||
import qualified Data.List as L
|
||||
|
||||
topFn :: [Int] -> Int -> ([Int], Int)
|
||||
topFn ls n = (n:ls, L.length ls)
|
||||
|
||||
topEntity
|
||||
:: Clock System
|
||||
-> Reset System
|
||||
-> Enable System
|
||||
-> Signal System Int
|
||||
-> Signal System Int
|
||||
topEntity = exposeClockResetEnable $ mealy topFn []
|
||||
|
||||
-- $ clash Exp.hs --verilog
|
||||
-- GHC: Setting up GHC took: 0.666s
|
||||
-- GHC: Compiling and loading modules took: 0.445s
|
||||
-- Clash: Parsing and compiling primitives took 0.266s
|
||||
-- GHC+Clash: Loading modules cumulatively took 1.502s
|
||||
-- Clash: Compiling Exp.topEntity
|
||||
-- Clash: Normalization took 0.031s
|
||||
--
|
||||
-- Exp.hs:19:1: error:
|
||||
--
|
||||
-- Clash.Netlist.BlackBox(319): No blackbox found for: GHC.List.$wlenAcc. Did you forget to include directories containing primitives? You can use '-i/my/prim/dir' to achieve this.
|
||||
--
|
||||
-- The source location of the error is not exact, only indicative, as it is acquired
|
||||
-- after optimizations. The actual location of the error can be in a function that is
|
||||
-- inlined. To prevent inlining of those functions, annotate them with a NOINLINE pragma.
|
||||
-- |
|
||||
-- 19 | topEntity = exposeClockResetEnable $ mealy topFn []
|
||||
-- | ^^^^^^^^^
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
-- {-
|
||||
-- An experiment with Clash: Experiment 1
|
||||
|
||||
-- I expected this not to synthesize. But it did.
|
||||
-- Probably because it was too simple.
|
||||
-- -}
|
||||
|
||||
-- module Exp where
|
||||
|
||||
-- import Clash.Prelude
|
||||
|
||||
-- topFn :: [Int] -> Int -> ([Int], Bool)
|
||||
-- topFn ls n = (ls, True)
|
||||
|
||||
-- topEntity
|
||||
-- :: Clock System
|
||||
-- -> Reset System
|
||||
-- -> Enable System
|
||||
-- -> Signal System Int
|
||||
-- -> Signal System Bool
|
||||
-- topEntity = exposeClockResetEnable $ mealy topFn []
|
||||
|
|
@ -9,13 +9,13 @@ import Clash.Prelude
|
|||
import Clash.Explicit.Testbench
|
||||
import qualified Data.List as L
|
||||
|
||||
type PC = Vec 4 Bit
|
||||
-- type PC = KnownNat n => Vec n Bit
|
||||
type Matrix a rows cols = Vec rows (Vec cols a)
|
||||
|
||||
isGood :: PC -> Bool
|
||||
isGood :: KnownNat n => Vec n Bit -> Bool
|
||||
isGood pc = (lsb pc) == high
|
||||
|
||||
isBad :: PC -> Bool
|
||||
isBad :: KnownNat n => Vec n Bit -> Bool
|
||||
isBad pc = reduceOr pc == low
|
||||
|
||||
conds :: Vec 4 (Char -> Bit)
|
||||
|
|
@ -23,7 +23,7 @@ conds
|
|||
= map (\c -> \x -> if c == x then high else low)
|
||||
('a' :> 'b' :> 'c' :> 'd' :> Nil)
|
||||
|
||||
condSat :: Char -> Vec 4 (Char -> Bit) -> Vec 4 Bit
|
||||
condSat :: KnownNat n => a -> Vec n (a -> Bit) -> Vec n Bit
|
||||
condSat c cnds = map (\f -> f c) cnds
|
||||
|
||||
-- | Transition matrix for a(b|c)
|
||||
|
|
@ -37,6 +37,17 @@ delta =
|
|||
{- F -} (bv2v 0b0000) :>
|
||||
Nil
|
||||
|
||||
-- | Transition matrix for (a|b)(c|d)
|
||||
delta2 :: Matrix Bit 5 5
|
||||
delta2 =
|
||||
-- abcdF
|
||||
{- a -} (bv2v 0b00110) :>
|
||||
{- b -} (bv2v 0b00110) :>
|
||||
{- c -} (bv2v 0b00001) :>
|
||||
{- d -} (bv2v 0b00001) :>
|
||||
{- F -} (bv2v 0b00000) :>
|
||||
Nil
|
||||
|
||||
dotProduct :: KnownNat n => Vec n Bit -> Vec n Bit -> Bit
|
||||
dotProduct a b =
|
||||
foldr (\b res -> xor b res) low
|
||||
|
|
@ -50,44 +61,60 @@ vecMatrixProd
|
|||
vecMatrixProd vec mat
|
||||
= map (\v -> dotProduct vec v) mat
|
||||
|
||||
-- matrixProd
|
||||
-- :: (KnownNat lrows, KnownNat comm, KnownNat rcols)
|
||||
-- => Matrix Bit lrows comm
|
||||
-- -> Matrix Bit comm rcols
|
||||
-- -> Matrix Bit lrows rcols
|
||||
-- matrixProd m1 m2 = map (\vec -> vecMatrixProd vec (transpose m2)) m1
|
||||
|
||||
topFn :: PC -> Char -> (PC, Maybe Bit)
|
||||
topFn pc c =
|
||||
let cndsats = condSat c conds in
|
||||
let pc' = bv2v $ (pack pc) .&. (pack cndsats) in
|
||||
genTopFn
|
||||
:: (KnownNat n, Eq a)
|
||||
=> Matrix Bit (n+1) (n+1) -- transition matrix
|
||||
-> Vec n (a -> Bit) -- symbol acceptance criteria
|
||||
-> Vec (n+1) Bit -- current state
|
||||
-> a -- input symbol
|
||||
-> (Vec (n+1) Bit, Maybe Bit) -- next state and result
|
||||
genTopFn delta cnds pc c =
|
||||
let cndsats = condSat c cnds in
|
||||
let pc' = liftA2 (.&.) pc (cndsats ++ (singleton low)) in
|
||||
--let pc' = bv2v $ (pack pc) .&. (pack cndsats) in
|
||||
let npc = vecMatrixProd pc' (transpose delta) in
|
||||
let res = if isGood npc then Just high
|
||||
else if isBad npc then Just low
|
||||
else Nothing in
|
||||
(npc, res)
|
||||
|
||||
topFn :: KnownNat n => Vec n Bit -> Char -> (Vec n Bit, Maybe Bit)
|
||||
topFn pc c = genTopFn delta conds pc c
|
||||
|
||||
|
||||
|
||||
-- topFn :: KnownNat n => Vec n Bit -> Char -> (Vec n Bit, Maybe Bit)
|
||||
-- topFn pc c =
|
||||
-- let cndsats = condSat c conds in
|
||||
-- let pc' = bv2v $ (pack pc) .&. (pack cndsats) in
|
||||
-- let npc = vecMatrixProd pc' (transpose delta) in
|
||||
-- let res = if isGood npc then Just high
|
||||
-- else if isBad npc then Just low
|
||||
-- else Nothing in
|
||||
-- (npc, res)
|
||||
|
||||
topEntity
|
||||
:: Clock System
|
||||
-> Reset System
|
||||
-> Enable System
|
||||
-> Signal System Char
|
||||
-> Signal System (Maybe Bit)
|
||||
topEntity = exposeClockResetEnable $ mealy topFn (bv2v 0b1000)
|
||||
-- topEntity
|
||||
-- :: Clock System
|
||||
-- -> Reset System
|
||||
-- -> Enable System
|
||||
-- -> Signal System Char
|
||||
-- -> Signal System (Maybe Bit)
|
||||
-- -- topEntity = exposeClockResetEnable $ mealy topFn (bv2v 0b11000)
|
||||
-- topEntity = exposeClockResetEnable $ mealy topFn (bv2v 0b1000)
|
||||
|
||||
|
||||
|
||||
testBench :: Signal System Bool
|
||||
testBench = done
|
||||
where
|
||||
--testInput = stimuliGenerator clk rst ('-' :> 'a' :> 'b' :> Nil)
|
||||
--expectedOutput = outputVerifier' clk rst (Nothing :> Nothing :> Just high :> Nil)
|
||||
testInput = stimuliGenerator clk rst ('a' :> 'b' :> Nil)
|
||||
expectedOutput = outputVerifier' clk rst (Nothing :> Just high :> Nil)
|
||||
done = expectedOutput (topEntity clk rst enableGen testInput)
|
||||
--done = expectedOutput (topEntity <$> testInput)
|
||||
clk = tbSystemClockGen (not <$> done)
|
||||
rst = systemResetGen
|
||||
-- testBench :: Signal System Bool
|
||||
-- testBench = done
|
||||
-- where
|
||||
-- --testInput = stimuliGenerator clk rst ('-' :> 'a' :> 'b' :> Nil)
|
||||
-- --expectedOutput = outputVerifier' clk rst (Nothing :> Nothing :> Just high :> Nil)
|
||||
-- testInput = stimuliGenerator clk rst ('a' :> 'b' :> Nil)
|
||||
-- expectedOutput = outputVerifier' clk rst (Nothing :> Just high :> Nil)
|
||||
-- done = expectedOutput (topEntity clk rst enableGen testInput)
|
||||
-- --done = expectedOutput (topEntity <$> testInput)
|
||||
-- clk = tbSystemClockGen (not <$> done)
|
||||
-- rst = systemResetGen
|
||||
|
||||
-- λ> L.take 5 $ sample testBench
|
||||
--
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ next
|
|||
=> a -- ^ Number whose square root is to be found
|
||||
-> a -- ^ Old approximation of square root
|
||||
-> a -- ^ New approximation of square root
|
||||
next n rt = (rt + (n/rt))/2
|
||||
next n rt = (rt + (n/rt))/3
|
||||
|
||||
-- | Starting from initial guess, keep finding better approximations
|
||||
rts
|
||||
|
|
@ -33,6 +33,7 @@ within eps l = case l of
|
|||
if a1-a0 < eps then a1
|
||||
else within eps (a1:l')
|
||||
|
||||
-- | Approximate square root of a number
|
||||
nrSqrt
|
||||
:: Float -- ^ Number whose square root is to be found
|
||||
-> Float -- ^ Initial guess of square root
|
||||
|
|
@ -50,6 +51,8 @@ nrSqrt n rt0 eps = within eps $ rts n rt0
|
|||
λ> nrSqrt 2 1.5 0.000001
|
||||
1.4166666666666665
|
||||
|
||||
-----
|
||||
|
||||
λ> sqrt 3
|
||||
1.7320508075688772
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue