bunch of files
This commit is contained in:
parent
c1fdd7e36f
commit
000a4f59fa
@ -12,3 +12,16 @@ Restart.
|
||||
rewrite size_eq0.
|
||||
by apply/eqP.
|
||||
Qed.
|
||||
|
||||
|
||||
(* [unfold_in]: Converting [\in] to function *)
|
||||
Goal forall A:Type,
|
||||
[::]
|
||||
\in (fun w0 : seq A => match w0 with
|
||||
| [::] => true
|
||||
| _ :: _ => false
|
||||
end).
|
||||
Proof.
|
||||
move => A.
|
||||
by rewrite unfold_in.
|
||||
Qed.
|
||||
|
@ -48,3 +48,13 @@ Proof.
|
||||
- rewrite finset.inE /=.
|
||||
by case (tt \in a) eqn:Hatt; rewrite Hatt !finset.inE.
|
||||
Qed.
|
||||
|
||||
(* Goal forall sp: {set unit}, *)
|
||||
(* (if tt \in sp then true else false) = x. *)
|
||||
|
||||
Lemma foo {A: finType} (sp: {set A}) (x: A):
|
||||
x \notin sp -> s = x |: sp -> false.
|
||||
Proof.
|
||||
Search (_ \notin _).
|
||||
Admitted.
|
||||
|
||||
|
100
coq/ohe.v
100
coq/ohe.v
@ -12,6 +12,7 @@ Set Bullet Behavior "Strict Subproofs".
|
||||
|
||||
(* Set Implicit Arguments. *)
|
||||
|
||||
Require Import Lia.
|
||||
Require Import Bvector.
|
||||
(* Require Import Arith. *)
|
||||
|
||||
@ -24,6 +25,66 @@ Inductive t: nat -> bool -> Type :=
|
||||
| Mark: forall {n: nat},
|
||||
t n false -> t (S n) true.
|
||||
|
||||
Fixpoint take {b: bool} {n tk: nat} (a: t n true) (pf: tk<n): t tk b.
|
||||
elim: tk pf => [pf|m' IH pf].
|
||||
- case: n pf a; first by []. (* Take nothing *)
|
||||
move => n pf a.
|
||||
exact: take b n.+1 0 a pf.
|
||||
Show Proof.
|
||||
-
|
||||
|
||||
- case: n pf a.
|
||||
+ by [].
|
||||
+ move => n' pf' a.
|
||||
|
||||
|
||||
Fixpoint take {b1 b2: bool} {n k: nat} (pf: k<n) (a: t (k+n) b1): t n b2.
|
||||
move: k pf a.
|
||||
move => k.
|
||||
case k eqn:Hk.
|
||||
Restart.
|
||||
elim: k pf a => [pf|k' IH pf a].
|
||||
- rewrite add0n => a.
|
||||
exact: take b1 b2 n 0 pf a.
|
||||
- move: n IH pf a => n IH pf.
|
||||
case.
|
||||
+
|
||||
|
||||
|
||||
- move: n IH pf a => n.
|
||||
case n eqn:Hn.
|
||||
+ move => IH pf; inversion pf.
|
||||
+ move => IH pf a.
|
||||
case a eqn:Ha.
|
||||
* by [].
|
||||
|
||||
|
||||
- refine (
|
||||
match a with
|
||||
| Nil => _
|
||||
| Pad n' b' a' => _
|
||||
| Mark n' a' => _
|
||||
end); first by [].
|
||||
+
|
||||
|
||||
|
||||
(* Fixpoint ltb {b1 b2: bool} {n: nat} (o1: t n b1) (o2: t n b2): bool. *)
|
||||
(* refine ( *)
|
||||
(* match o1, o2 with *)
|
||||
(* | Nil, Nil => true *)
|
||||
(* | Pad n1' b1' o1', Pad n2' b2' o2' => _ *)
|
||||
(* | Mark n1' o1', Mark n2' o2' => _ *)
|
||||
(* | _, _ => false *)
|
||||
(* end). *)
|
||||
|
||||
|
||||
(* Fixpoint ltb {b1 b2: bool} {n1 n2: nat} (o1: t n1 b1) (o2: t n2 b2): bool. *)
|
||||
(* case (Nat.eqb n1 n2) eqn:Hneq. *)
|
||||
(* - have Hn := iffLR (PeanoNat.Nat.eqb_eq n1 n2) Hneq. *)
|
||||
(* clear Hneq; rename Hn into Hneq. *)
|
||||
(* shelve. *)
|
||||
(* - exact: false. *)
|
||||
(* Defined. *)
|
||||
|
||||
Fixpoint eqb {b1 b2: bool} {n1 n2: nat} (o1: t n1 b1) (o2: t n2 b2): bool.
|
||||
case (Nat.eqb n1 n2) eqn:Hneq.
|
||||
@ -78,45 +139,6 @@ Fixpoint eqb' {b1 b2: bool} {n1 n2: nat} (o1: t n1 b1) (o2: t n2 b2): bool.
|
||||
- exact: false.
|
||||
Defined.
|
||||
|
||||
|
||||
|
||||
|
||||
(* move/PeanoNat.Nat.eqb_spec: Hneq => Hneq. *)
|
||||
(* refine ( *)
|
||||
(* match o1, o2 with *)
|
||||
(* | Nil, Nil => true *)
|
||||
(* | Pad n1' b1' o1', Pad n2' b2' o2' => _ *)
|
||||
(* | Mark n1' o1', Mark n2' o2' => _ *)
|
||||
(* | _, _ => false *)
|
||||
(* end). *)
|
||||
(* - move: n1' n2' o1' o2' => n1' n2'. *)
|
||||
(* case (Nat.eqb n1' n2') eqn:Hneq'. *)
|
||||
(* + Search Nat.eqb. *)
|
||||
(* (1* PeanoNat.Nat.eqb_eq *1) *)
|
||||
(* Check (EqNat.beq_nat_true_stt n1' n2'). *)
|
||||
(* Search Nat.eqb Nat.eqb. *)
|
||||
(* move: Hneq'. *)
|
||||
(* Check Nat.eqb_eq n1' n2'. *)
|
||||
(* Check (EqNat.beq_nat_true_stt n1' n2'). *)
|
||||
(* rewrite (EqNat.beq_nat_true_stt n1' n2') in Hneq'. *)
|
||||
(* move => o1' o2'. *)
|
||||
(* exact: eqb _ _ _ _ o1' o2'. *)
|
||||
(* Search (_ = _) Nat.eqb. *)
|
||||
(* Check PeanoNat.Nat.eqb_eq n1' n2'. *)
|
||||
(* rewrite (EqNat.beq_nat_true_stt n1' n2') in Hneq'. *)
|
||||
(* rewrite -(EqNat.beq_nat_true_stt n1' n2'). *)
|
||||
(* S *)
|
||||
(* + exact: (fun _ _ => false). *)
|
||||
(* - move: n1' n2' o1' o2' => n1' n2'. *)
|
||||
(* case (Nat.eqb n1' n2') eqn:Hneq'. *)
|
||||
(* + move/PeanoNat.Nat.eqb_spec: Hneq' => Hneq'. *)
|
||||
(* rewrite -Hneq'. *)
|
||||
(* move => o1' o2'. *)
|
||||
(* exact: eqb _ _ _ _ o1' o2'. *)
|
||||
(* + exact: (fun _ _ => false). *)
|
||||
(* - exact: false. *)
|
||||
(* Defined. *)
|
||||
|
||||
Fixpoint markCount_aux {n: nat} {b: bool} (a: t n b): nat :=
|
||||
match a with
|
||||
| Nil => 0
|
||||
|
23
easycrypt/hi.ec
Normal file
23
easycrypt/hi.ec
Normal file
@ -0,0 +1,23 @@
|
||||
(* https://alleystoughton.us/easycrypt-installation.html *)
|
||||
|
||||
(*
|
||||
load the "core" EasyCrypt theories, in
|
||||
particular giving us the relation < on the
|
||||
type int of integers
|
||||
*)
|
||||
require import AllCore.
|
||||
|
||||
|
||||
(*
|
||||
the smt tactic will only
|
||||
succeed if both Alt-Ergo and
|
||||
Z3 are able to solve the goal
|
||||
*)
|
||||
prover quorum=2 ["Alt-Ergo" "Z3"].
|
||||
|
||||
|
||||
lemma foo (x y : int) :
|
||||
x < y => x + 1 < y + 1.
|
||||
proof.
|
||||
smt().
|
||||
qed.
|
72
easycrypt/hi.eco
Normal file
72
easycrypt/hi.eco
Normal file
@ -0,0 +1,72 @@
|
||||
{
|
||||
"version": 3,
|
||||
"echash": "2023.09",
|
||||
"root": { "kind": "ec", "digest": "bdf2de2fc8d4967319450f975497b805" },
|
||||
"depends": {
|
||||
"AlgTactic": {
|
||||
"direct": false,
|
||||
"kind": "ec",
|
||||
"digest": "e6afb591d5b17db178ff233f2ced34fb"
|
||||
},
|
||||
"AllCore": {
|
||||
"direct": true,
|
||||
"kind": "ec",
|
||||
"digest": "b420321b00853b1dd4a3ea1e5d6793ca"
|
||||
},
|
||||
"Core": {
|
||||
"direct": false,
|
||||
"kind": "ec",
|
||||
"digest": "533a9184e00a09994f6770e8e93b6f34"
|
||||
},
|
||||
"CoreInt": {
|
||||
"direct": false,
|
||||
"kind": "ec",
|
||||
"digest": "301224e64ef6d0a3b1783dbb8ce7409e"
|
||||
},
|
||||
"CoreReal": {
|
||||
"direct": false,
|
||||
"kind": "ec",
|
||||
"digest": "71a66b712b2595af8e02fada3eaa0c67"
|
||||
},
|
||||
"Int": {
|
||||
"direct": false,
|
||||
"kind": "ec",
|
||||
"digest": "e1b1e343242e4e8ead996a359384b3da"
|
||||
},
|
||||
"Logic": {
|
||||
"direct": true,
|
||||
"kind": "ec",
|
||||
"digest": "02709af70bbfcc01ae52b66a2fa3283b"
|
||||
},
|
||||
"Monoid": {
|
||||
"direct": false,
|
||||
"kind": "eca",
|
||||
"digest": "e137ba3bc8dacd4374666a21fbb63724"
|
||||
},
|
||||
"Pervasive": {
|
||||
"direct": true,
|
||||
"kind": "ec",
|
||||
"digest": "0f385a91ae1a1269de2ba2b7fad360d0"
|
||||
},
|
||||
"Real": {
|
||||
"direct": false,
|
||||
"kind": "ec",
|
||||
"digest": "60e4174d5c39b108291a64e755d726fd"
|
||||
},
|
||||
"Ring": {
|
||||
"direct": false,
|
||||
"kind": "ec",
|
||||
"digest": "532076b711a9a848fbb7727cbfa8f9b7"
|
||||
},
|
||||
"Tactics": {
|
||||
"direct": true,
|
||||
"kind": "ec",
|
||||
"digest": "636a47e692aa516fc65775b561bbf08b"
|
||||
},
|
||||
"Xint": {
|
||||
"direct": false,
|
||||
"kind": "ec",
|
||||
"digest": "f8cdbe78777b5164dc57262d577911a4"
|
||||
}
|
||||
}
|
||||
}
|
25
haskell/IntToBin.hs
Normal file
25
haskell/IntToBin.hs
Normal file
@ -0,0 +1,25 @@
|
||||
intToLBool :: Int -> Int -> [Bool]
|
||||
intToLBool sz n =
|
||||
if sz < 1 then []
|
||||
else foo sz n
|
||||
where
|
||||
foo sz n =
|
||||
if n == 0 then repeatN False sz
|
||||
else bar sz n
|
||||
|
||||
-- bar :: Int -> Int -> [Bool]
|
||||
bar sz n =
|
||||
if n == 0 then repeatN False sz
|
||||
else if sz < 1 then []
|
||||
else
|
||||
(if mod n 2 == 0 then False else True) : bar (sz-1) (div n 2)
|
||||
|
||||
-- repeatN :: a -> Int -> [a]
|
||||
repeatN x n = take n $ repeat x
|
||||
|
||||
{-
|
||||
λ> intToLBool 1 1
|
||||
[True]
|
||||
λ> intToLBool 5 2
|
||||
[False,True,False,False,False]
|
||||
-}
|
53
haskell/ThompsonRe.hs
Normal file
53
haskell/ThompsonRe.hs
Normal file
@ -0,0 +1,53 @@
|
||||
data Re a
|
||||
= Nul
|
||||
| Eps
|
||||
| Char (a -> Bool)
|
||||
| Cat (Re a) (Re a)
|
||||
| Alt (Re a) (Re a)
|
||||
| Star (Re a)
|
||||
|
||||
data Instr a
|
||||
= Accept
|
||||
| Jump Int
|
||||
| Split Int
|
||||
| Chr (a -> Bool)
|
||||
|
||||
|
||||
-- drv :: Re a -> [a] -> (Re a, [a])
|
||||
-- drv r l = case r of
|
||||
-- Nul -> (Nul, [])
|
||||
-- Eps -> if null l then (Eps, []) else (Nul, [])
|
||||
-- Char f ->
|
||||
-- if (length l == 1 && f (head l)) then (Eps, [])
|
||||
-- else (Nul, [])
|
||||
-- Cat r1 r2 ->
|
||||
-- let r', l' = drv r1 l in
|
||||
-- case r1
|
||||
-- drv (Cat r'
|
||||
-- Alt r1 r2 -> (reDe r1 l) || (reDe r2 l)
|
||||
-- Star r -> (reDe Eps l) || (reDe (Cat r (Star r)) l)
|
||||
|
||||
drv ∅ l = False, l
|
||||
drv ε l = True, l
|
||||
drv c l =
|
||||
if null l then False, l
|
||||
else if head l == c then True, tail l
|
||||
else False, l
|
||||
drv r1;r2 l =
|
||||
let b l' = drv r1 l in
|
||||
if b then drv r2 l'
|
||||
else False, l'
|
||||
|
||||
|
||||
reDe :: Re a -> [a] -> Bool
|
||||
reDe r l = case r of
|
||||
Nul -> False
|
||||
Eps -> null l
|
||||
Char f -> length l == 1 && f (head l)
|
||||
Cat r1 r2 -> False
|
||||
Alt r1 r2 -> (reDe r1 l) || (reDe r2 l)
|
||||
Star r -> (reDe Eps l) || (reDe (Cat r (Star r)) l)
|
||||
where
|
||||
-- catHelper :: Re a -> [a] -> (Re a, [a])
|
||||
catHelper re lst =
|
||||
|
@ -111,3 +111,13 @@ tc1 = lam (Arrow Boolean Nat) (lam Boolean (app (var 1) (var 0)))
|
||||
-- tm2 = Lam (Arrow Boolean Nat) (Lam Boolean _)
|
||||
tc2 :: forall x. TypeChecker
|
||||
tc2 = \ctxt -> Nothing
|
||||
|
||||
|
||||
class TyChecker a where
|
||||
varC :: Int -> a
|
||||
appC :: a -> a -> a
|
||||
lamC :: Typ -> a -> a
|
||||
|
||||
failureC :: a
|
||||
hasTypeC :: Typ -> a -> a
|
||||
haveC :: Int -> Typ -> a -> a
|
||||
|
68
haskell/clash/experiments/Exp.hs
Normal file
68
haskell/clash/experiments/Exp.hs
Normal file
@ -0,0 +1,68 @@
|
||||
{-
|
||||
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 []
|
27
haskell/clash/experiments/Hlist.hs
Normal file
27
haskell/clash/experiments/Hlist.hs
Normal file
@ -0,0 +1,27 @@
|
||||
{-
|
||||
Question:
|
||||
Can clash synthesize hlist?
|
||||
|
||||
Answer:
|
||||
-}
|
||||
|
||||
module Hlist where
|
||||
|
||||
import Clash.Prelude
|
||||
import qualified Data.List as L
|
||||
|
||||
|
||||
-- No input.
|
||||
-- State is index to `l'.
|
||||
-- Output is l[state]
|
||||
topFn :: Int -> () -> (Int, Int)
|
||||
topFn idx _ = (mod (idx+1) 9, l L.!! idx)
|
||||
|
||||
topEntity
|
||||
:: Clock System
|
||||
-> Reset System
|
||||
-> Enable System
|
||||
-> Signal System ()
|
||||
-> Signal System Int
|
||||
topEntity = exposeClockResetEnable $ mealy topFn 0
|
||||
|
29
haskell/clash/experiments/ListSynth.hs
Normal file
29
haskell/clash/experiments/ListSynth.hs
Normal file
@ -0,0 +1,29 @@
|
||||
{-
|
||||
Question:
|
||||
Does the design synthesizable if the list is a constant list?
|
||||
|
||||
Answer:
|
||||
Yes, it does.
|
||||
-}
|
||||
|
||||
module ListSynth where
|
||||
|
||||
import Clash.Prelude
|
||||
import qualified Data.List as L
|
||||
|
||||
l = (*10) <$> [1..9]
|
||||
|
||||
-- No input.
|
||||
-- State is index to `l'.
|
||||
-- Output is l[state]
|
||||
topFn :: Int -> () -> (Int, Int)
|
||||
topFn idx _ = (mod (idx+1) 9, l L.!! idx)
|
||||
|
||||
topEntity
|
||||
:: Clock System
|
||||
-> Reset System
|
||||
-> Enable System
|
||||
-> Signal System ()
|
||||
-> Signal System Int
|
||||
topEntity = exposeClockResetEnable $ mealy topFn 0
|
||||
|
1386
haskell/clash/experiments/Matrix.hs
Normal file
1386
haskell/clash/experiments/Matrix.hs
Normal file
File diff suppressed because it is too large
Load Diff
@ -1,5 +1,174 @@
|
||||
-- {-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
-- import Control.Monad (void)
|
||||
import Text.Megaparsec
|
||||
import Text.Megaparsec.Expr
|
||||
import Text.Megaparsec.String -- input stream is of the type 'String'
|
||||
import qualified Text.Megaparsec.Lexer as L
|
||||
import Text.Megaparsec.Char
|
||||
import qualified Text.Megaparsec.Char.Lexer as L
|
||||
import Control.Monad.Combinators.Expr
|
||||
-- import Control.Applicative
|
||||
-- import Control.Monad
|
||||
import Data.Char
|
||||
import Data.Void
|
||||
import Data.Text
|
||||
-- import Data.Functor.Identity
|
||||
-- import Control.Applicative.Combinators
|
||||
|
||||
-- type Parser = Parsec Void Text
|
||||
-- type Parsec e s a = ParsecT e s Identity a
|
||||
-- type Parser = Parsec Void String
|
||||
type Parser = Parsec Void Text
|
||||
|
||||
sc :: Parser ()
|
||||
sc = L.space
|
||||
space1 -- (2)
|
||||
(L.skipLineComment "//") -- (3)
|
||||
(L.skipBlockComment "/*" "*/") -- (4)
|
||||
|
||||
lexeme :: Parser a -> Parser a
|
||||
lexeme = L.lexeme sc
|
||||
|
||||
symbol :: Text -> Parser Text
|
||||
symbol = L.symbol sc
|
||||
|
||||
binary :: Text -> ((Re a) -> (Re a) -> (Re a)) -> Operator Parser (Re a)
|
||||
binary name f = InfixL (f <$ symbol name)
|
||||
|
||||
prefix, postfix :: Text -> ((Re a) -> (Re a)) -> Operator Parser (Re a)
|
||||
prefix name f = Prefix (f <$ symbol name)
|
||||
postfix name f = Postfix (f <$ symbol name)
|
||||
|
||||
integer :: Parser Integer
|
||||
integer = L.decimal
|
||||
|
||||
data Re a
|
||||
= Atom a
|
||||
| CCls [a]
|
||||
| NCls [a]
|
||||
| Opt (Re a)
|
||||
| Rep (Re a) Integer Integer
|
||||
-- | Rep (Re a) Int Int
|
||||
| Dot a
|
||||
| Eps
|
||||
| Cat (Re a) (Re a)
|
||||
deriving Show
|
||||
|
||||
uchar :: Parser Char
|
||||
uchar = satisfy isUpper
|
||||
|
||||
uchars :: Parser [Char]
|
||||
uchars = many uchar
|
||||
|
||||
atom :: Parser (Re Char)
|
||||
atom = Atom <$> uchar
|
||||
|
||||
ccls :: Parser (Re Char)
|
||||
ccls = do
|
||||
_ <- char '['
|
||||
x <- uchars
|
||||
_ <- char ']'
|
||||
return $ CCls x
|
||||
|
||||
ncls :: Parser (Re Char)
|
||||
ncls = do
|
||||
_ <- char '['
|
||||
_ <- char '^'
|
||||
x <- uchars
|
||||
_ <- char ']'
|
||||
return $ NCls x
|
||||
|
||||
dot :: Parser (Re Char)
|
||||
dot = Dot <$> uchar
|
||||
|
||||
rep :: Parser (Re Char)
|
||||
rep = do
|
||||
r <- re
|
||||
_ <- char '{'
|
||||
low <- integer
|
||||
_ <- char ','
|
||||
high <- integer
|
||||
_ <- char '}'
|
||||
return $ Rep r low high
|
||||
|
||||
|
||||
opt :: Parser (Re Char)
|
||||
opt = do
|
||||
r <- re
|
||||
_ <- char '?'
|
||||
return $ Opt r
|
||||
|
||||
-- opt :: Parser (Re Char) -> Parser (Re Char -> Re Char)
|
||||
-- opt = do
|
||||
-- r <- re
|
||||
-- _ <- char '?'
|
||||
-- return $ Opt r
|
||||
|
||||
cat :: Parser (Re Char)
|
||||
cat = do
|
||||
x <- uchars
|
||||
return $ Prelude.foldr Cat Eps $ (Atom <$> x)
|
||||
|
||||
-- opt' :: Parser (Re Char)
|
||||
-- opt' = Opt <$> r <* (char '?')
|
||||
|
||||
|
||||
re :: Parser (Re Char)
|
||||
re = choice
|
||||
[ cat
|
||||
, ccls
|
||||
, opt
|
||||
, dot
|
||||
, ncls
|
||||
, rep
|
||||
]
|
||||
|
||||
-- optab :: [[Operator Parser (Re Char)]]
|
||||
-- optab =
|
||||
-- [
|
||||
-- [
|
||||
-- prefix "?" Opt
|
||||
-- ]
|
||||
-- -- ,
|
||||
-- -- [
|
||||
-- -- binary "" Cat
|
||||
-- -- ]
|
||||
-- ]
|
||||
|
||||
-- pre :: Parser (Re Char)
|
||||
-- pre = makeExprParser re optab
|
||||
|
||||
|
||||
|
||||
-- parseTest ccls :: String -> IO ()
|
||||
-- λ> parseTest ccls "[abcd]"
|
||||
-- 1:2:
|
||||
-- |
|
||||
-- 1 | [abcd]
|
||||
-- | ^
|
||||
-- unexpected 'a'
|
||||
-- expecting ']'
|
||||
-- λ> parseTest ccls "[ABCD]"
|
||||
-- CCls "ABCD"
|
||||
-- λ> parseTest ccls "[ABCD]adf"
|
||||
-- CCls "ABCD"
|
||||
|
||||
------------
|
||||
|
||||
-- λ> parseTest atom "h"
|
||||
-- 1:1:
|
||||
-- |
|
||||
-- 1 | h
|
||||
-- | ^
|
||||
-- unexpected 'h'
|
||||
-- λ> parseTest atom "H"
|
||||
-- Atom 'H'
|
||||
-- λ> parseTest atom "Hi"
|
||||
-- Atom 'H'
|
||||
|
||||
------------
|
||||
|
||||
-- a = parseTest (pre <* eof) "AB"
|
||||
-- b = parseTest (pre <* eof) "[AB]"
|
||||
|
||||
c = parseTest (re <* eof) "AB"
|
||||
d = parseTest (re <* eof) "AB[CDE]"
|
||||
|
90
haskell/megaparsec-eg/Re.hs
Normal file
90
haskell/megaparsec-eg/Re.hs
Normal file
@ -0,0 +1,90 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
import Text.Megaparsec
|
||||
import Text.Megaparsec.Char
|
||||
import qualified Text.Megaparsec.Char.Lexer as L
|
||||
import Control.Monad.Combinators.Expr
|
||||
-- import Control.Applicative
|
||||
-- import Control.Monad
|
||||
import Data.Char
|
||||
import Data.Void
|
||||
import Data.Text
|
||||
|
||||
type Parser = Parsec Void Text
|
||||
|
||||
data Term = Literal Char
|
||||
| Sequence [Term]
|
||||
| Repeat (Int, Maybe Int) Term
|
||||
| Choice [Term]
|
||||
deriving ( Show )
|
||||
|
||||
seq a b = Sequence $ (seqTerms a) ++ (seqTerms b)
|
||||
alt a b = Choice $ (choiceTerms a) ++ (choiceTerms b)
|
||||
seqTerms (Sequence ts) = ts
|
||||
seqTerms t = [t]
|
||||
|
||||
choiceTerms (Choice ts) = ts
|
||||
choiceTerms t = [t]
|
||||
|
||||
|
||||
-- ops = [ [ Postfix (Repeat (0, Nothing) <$ char '*')
|
||||
-- , Postfix (Repeat (1, Nothing) <$ char '+')
|
||||
-- , Postfix (Repeat (0, Just 1) <$ char '?')
|
||||
-- ]
|
||||
-- , [ InfixR (return sequence)
|
||||
-- ]
|
||||
-- , [ InfixR (alt <$ char '|')
|
||||
-- ]
|
||||
-- ]
|
||||
|
||||
-- term :: Parser Term
|
||||
-- term = makeExprParser ops atom where
|
||||
-- ops = [ [ Postfix (Repeat (0, Nothing) <$ char '*')
|
||||
-- , Postfix (Repeat (1, Nothing) <$ char '+')
|
||||
-- , Postfix (Repeat (0, Just 1) <$ char '?')
|
||||
-- ]
|
||||
-- , [ InfixR (return sequence)
|
||||
-- ]
|
||||
-- , [ InfixR (choice <$ char '|')
|
||||
-- ]
|
||||
-- ]
|
||||
|
||||
-- atom = msum [ Literal <$> lit
|
||||
-- , parens term
|
||||
-- ]
|
||||
|
||||
-- lit = noneOf "*+?|()"
|
||||
-- sequence a b = Sequence $ (seqTerms a) ++ (seqTerms b)
|
||||
-- choice a b = Choice $ (choiceTerms a) ++ (choiceTerms b)
|
||||
-- parens = between (char '(') (char ')')
|
||||
|
||||
-- seqTerms (Sequence ts) = ts
|
||||
-- seqTerms t = [t]
|
||||
|
||||
-- choiceTerms (Choice ts) = ts
|
||||
-- choiceTerms t = [t]
|
||||
|
||||
-- main = parseTest term "he(llo)*|wor+ld?"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
sc :: Parser ()
|
||||
sc = L.space
|
||||
space1 -- (2)
|
||||
(L.skipLineComment "//") -- (3)
|
||||
(L.skipBlockComment "/*" "*/") -- (4)
|
||||
|
||||
lexeme :: Parser a -> Parser a
|
||||
lexeme = L.lexeme sc
|
||||
|
||||
symbol :: Text -> Parser Text
|
||||
symbol = L.symbol sc
|
||||
|
||||
binary :: Text -> ((Term) -> (Term) -> (Term)) -> Operator Parser (Term)
|
||||
binary name f = InfixR (f <$ symbol name)
|
||||
|
||||
prefix, postfix :: Text -> ((Term) -> (Term)) -> Operator Parser (Term)
|
||||
prefix name f = Prefix (f <$ symbol name)
|
||||
postfix name f = Postfix (f <$ symbol name)
|
@ -7,6 +7,20 @@ Assumptions:
|
||||
|
||||
import argparse
|
||||
|
||||
HEADER_STR = """
|
||||
import qualified GHC.Base
|
||||
#if __GLASGOW_HASKELL__ >= 900
|
||||
import qualified GHC.Exts
|
||||
#endif
|
||||
|
||||
unsafeCoerce :: a -> b
|
||||
#if __GLASGOW_HASKELL__ >= 900
|
||||
unsafeCoerce = GHC.Exts.unsafeCoerce#
|
||||
#else
|
||||
unsafeCoerce = GHC.Base.unsafeCoerce#
|
||||
#endif
|
||||
"""
|
||||
|
||||
ADDENDUM_TMP = """
|
||||
tfun'
|
||||
:: SystemClockResetEnable
|
||||
@ -38,6 +52,7 @@ if __name__ == "__main__":
|
||||
for line in fin:
|
||||
if line == "import qualified Prelude\n":
|
||||
break
|
||||
print(HEADER_STR)
|
||||
print(f"module {args.module} where\n")
|
||||
print(f"import Clash.Prelude\n")
|
||||
if args.imports:
|
||||
|
@ -24,7 +24,7 @@ if __name__ == "__main__":
|
||||
|
||||
|
||||
"""
|
||||
$ python3 % "Char (fun _ => false)" bool
|
||||
$ python3 % "Char (fun _ => false)" Ascii.ascii
|
||||
|
||||
From aruvi Require Import re.
|
||||
From aruvi Require Import dfa.
|
||||
|
@ -22,7 +22,10 @@ rm -rf $COQFILE $HSFILE $CLASHFILE $TCLFILE
|
||||
|
||||
python3 hs-gen.py "$1" "Ascii.ascii" > "$COQFILE"
|
||||
coqc "$COQFILE" > "$HSFILE"
|
||||
cp "$HSFILE" "$CLASHFILE"
|
||||
|
||||
python3 extr-proc.py "$1" > "$CLASHFILE"
|
||||
# cp "$HSFILE" "$CLASHFILE"
|
||||
|
||||
clash -verilog "$CLASHFILE"
|
||||
python3 tcl-gen.py "$PROJNAME" "$BOARD" "$PROJPATH" "$VERILOGSRC" > "$TCLFILE"
|
||||
vivado -mode batch -source "$TCLFILE"
|
||||
|
Loading…
Reference in New Issue
Block a user