diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/Circuit/Gate.agda | 137 | ||||
| -rw-r--r-- | Data/Circuit/Typecheck.agda | 78 | ||||
| -rw-r--r-- | Data/SExp.agda | 75 | ||||
| -rw-r--r-- | Data/SExp/Parser.agda | 73 |
4 files changed, 363 insertions, 0 deletions
diff --git a/Data/Circuit/Gate.agda b/Data/Circuit/Gate.agda new file mode 100644 index 0000000..915ee8b --- /dev/null +++ b/Data/Circuit/Gate.agda @@ -0,0 +1,137 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Gate where + +open import Level using (0ℓ) +open import Data.Castable using (Castable) +open import Data.Hypergraph.Base using (HypergraphLabel; module Edge; module HypergraphList) +open import Data.String using (String) +open import Data.Nat.Base using (ℕ; _≤_) +open import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; isEquivalence; cong) +import Relation.Binary.PropositionalEquality as ≡ + +import Data.Nat as Nat +import Data.Fin as Fin + +data Gate : ℕ → Set where + ZERO : Gate 1 + ONE : Gate 1 + ID : Gate 2 + NOT : Gate 2 + AND : Gate 3 + OR : Gate 3 + XOR : Gate 3 + NAND : Gate 3 + NOR : Gate 3 + XNOR : Gate 3 + +cast-gate : {e e′ : ℕ} → .(e ≡ e′) → Gate e → Gate e′ +cast-gate {1} {1} eq g = g +cast-gate {2} {2} eq g = g +cast-gate {3} {3} eq g = g + +cast-gate-trans + : {m n o : ℕ} + → .(eq₁ : m ≡ n) + .(eq₂ : n ≡ o) + (g : Gate m) + → cast-gate eq₂ (cast-gate eq₁ g) ≡ cast-gate (trans eq₁ eq₂) g +cast-gate-trans {1} {1} {1} eq₁ eq₂ g = refl +cast-gate-trans {2} {2} {2} eq₁ eq₂ g = refl +cast-gate-trans {3} {3} {3} eq₁ eq₂ g = refl + +cast-gate-is-id : {m : ℕ} .(eq : m ≡ m) (g : Gate m) → cast-gate eq g ≡ g +cast-gate-is-id {1} eq g = refl +cast-gate-is-id {2} eq g = refl +cast-gate-is-id {3} eq g = refl + +subst-is-cast-gate : {m n : ℕ} (eq : m ≡ n) (g : Gate m) → subst Gate eq g ≡ cast-gate eq g +subst-is-cast-gate refl g = sym (cast-gate-is-id refl g) + +GateCastable : Castable +GateCastable = record + { B = Gate + ; isCastable = record + { cast = cast-gate + ; cast-trans = cast-gate-trans + ; cast-is-id = cast-gate-is-id + ; subst-is-cast = subst-is-cast-gate + } + } + +showGate : (n : ℕ) → Gate n → String +showGate _ ZERO = "ZERO" +showGate _ ONE = "ONE" +showGate _ ID = "ID" +showGate _ NOT = "NOT" +showGate _ AND = "AND" +showGate _ OR = "OR" +showGate _ XOR = "XOR" +showGate _ NAND = "NAND" +showGate _ NOR = "NOR" +showGate _ XNOR = "XNOR" + +toℕ : (n : ℕ) → Gate n → ℕ +toℕ 1 ZERO = 0 +toℕ 1 ONE = 1 +toℕ 2 ID = 0 +toℕ 2 NOT = 1 +toℕ 3 AND = 0 +toℕ 3 OR = 1 +toℕ 3 XOR = 2 +toℕ 3 NAND = 3 +toℕ 3 NOR = 4 +toℕ 3 XNOR = 5 + +toℕ-injective : {n : ℕ} {x y : Gate n} → toℕ n x ≡ toℕ n y → x ≡ y +toℕ-injective {1} {ZERO} {ZERO} refl = refl +toℕ-injective {1} {ONE} {ONE} refl = refl +toℕ-injective {2} {ID} {ID} refl = refl +toℕ-injective {2} {NOT} {NOT} refl = refl +toℕ-injective {3} {AND} {AND} refl = refl +toℕ-injective {3} {OR} {OR} refl = refl +toℕ-injective {3} {XOR} {XOR} refl = refl +toℕ-injective {3} {NAND} {NAND} refl = refl +toℕ-injective {3} {NOR} {NOR} refl = refl +toℕ-injective {3} {XNOR} {XNOR} refl = refl + +open import Relation.Binary using (Rel; Decidable; DecidableEquality) +import Relation.Nullary.Decidable as Dec + +_[_≤_] : (n : ℕ) → Rel (Gate n) 0ℓ +_[_≤_] n x y = toℕ n x ≤ toℕ n y + +_≟_ : {n : ℕ} → DecidableEquality (Gate n) +_≟_ {n} x y = Dec.map′ toℕ-injective (cong (toℕ n)) (toℕ n x Nat.≟ toℕ n y) + +_≤?_ : {n : ℕ} → Decidable (n [_≤_]) +_≤?_ {n} x y = toℕ n x Nat.≤? toℕ n y + +GateLabel : HypergraphLabel +GateLabel = record + { Label = Gate + ; showLabel = showGate + ; isCastable = record + { cast = cast-gate + ; cast-trans = cast-gate-trans + ; cast-is-id = cast-gate-is-id + ; subst-is-cast = subst-is-cast-gate + } + ; _[_≤_] = λ n x y → toℕ n x ≤ toℕ n y + ; isDecTotalOrder = λ n → record + { isTotalOrder = record + { isPartialOrder = record + { isPreorder = record + { isEquivalence = isEquivalence + ; reflexive = λ { refl → ≤-refl } + ; trans = ≤-trans + } + ; antisym = λ i≤j j≤i → toℕ-injective (≤-antisym i≤j j≤i) + } + ; total = λ { x y → ≤-total (toℕ n x) (toℕ n y) } + } + ; _≟_ = _≟_ + ; _≤?_ = _≤?_ + } + } diff --git a/Data/Circuit/Typecheck.agda b/Data/Circuit/Typecheck.agda new file mode 100644 index 0000000..bb7e23c --- /dev/null +++ b/Data/Circuit/Typecheck.agda @@ -0,0 +1,78 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Typecheck where + +open import Data.SExp using (SExp) +open import Data.Hypergraph.Base using (HypergraphLabel; module Edge; module HypergraphList) +open import Data.Circuit.Gate using (GateLabel; Gate) +open Edge GateLabel using (Edge) +open HypergraphList GateLabel using (Hypergraph) + +open import Data.List using (List; length) renaming (map to mapL) +open import Data.List.Effectful using () renaming (module TraversableA to ListTraversable) +open import Data.Maybe using (Maybe) renaming (map to mapM) +open import Data.Nat using (ℕ; _<?_; _≟_) +open import Data.String using (String) +open import Data.Product using (_×_; _,_; Σ) +open import Data.Vec using (Vec; []; _∷_; fromList) renaming (map to mapV) +open import Data.Vec.Effectful using () renaming (module TraversableA to VecTraversable) +open import Data.Maybe.Effectful using (applicative) +open import Data.Fin using (Fin; #_; fromℕ<) +open import Level using (0ℓ) + +import Relation.Binary.PropositionalEquality as ≡ + +open List +open SExp +open Gate +open Maybe + +gate : {n a : ℕ} (g : Gate a) → Vec (Fin n) a → Edge n +gate g p = record { label = g; ports = p } + +typeCheckGateLabel : SExp → Maybe (Σ ℕ Gate) +typeCheckGateLabel (Atom "one") = just (1 , ONE) +typeCheckGateLabel (Atom "zero") = just (1 , ZERO) +typeCheckGateLabel (Atom "not") = just (2 , NOT) +typeCheckGateLabel (Atom "id") = just (2 , ID) +typeCheckGateLabel (Atom "and") = just (3 , AND) +typeCheckGateLabel (Atom "or") = just (3 , OR) +typeCheckGateLabel (Atom "xor") = just (3 , XOR) +typeCheckGateLabel (Atom "nand") = just (3 , NAND) +typeCheckGateLabel (Atom "nor") = just (3 , NOR) +typeCheckGateLabel (Atom "xnor") = just (3 , XNOR) +typeCheckGateLabel _ = nothing + +open import Relation.Nullary.Decidable using (Dec; yes; no) +open Dec +open VecTraversable {0ℓ} applicative using () renaming (sequenceA to vecSequenceA) +open ListTraversable {0ℓ} applicative using () renaming (sequenceA to listSequenceA) + +typeCheckPort : (v : ℕ) → SExp → Maybe (Fin v) +typeCheckPort v (Nat n) with n <? v +... | yes n<v = just (fromℕ< n<v) +... | no _ = nothing +typeCheckPort _ _ = nothing + +typeCheckPorts : (v n : ℕ) → List SExp → Maybe (Vec (Fin v) n) +typeCheckPorts v n xs with length xs ≟ n +... | yes ≡.refl = vecSequenceA (mapV (typeCheckPort v) (fromList xs)) +... | no _ = nothing + +typeCheckGate : (v : ℕ) → SExp → Maybe (Edge v) +typeCheckGate v (SExps (labelString ∷ ports)) with typeCheckGateLabel labelString +... | just (n , label) = mapM (gate label) (typeCheckPorts v n ports) +... | nothing = nothing +typeCheckGate v _ = nothing + +typeCheckHeader : SExp → Maybe ℕ +typeCheckHeader (SExps (Atom "hypergraph" ∷ Nat n ∷ [])) = just n +typeCheckHeader _ = nothing + +typeCheckHypergraph : SExp → Maybe (Σ ℕ Hypergraph) +typeCheckHypergraph (SExps (x ∷ xs)) with typeCheckHeader x +... | nothing = nothing +... | just n with listSequenceA (mapL (typeCheckGate n) xs) +... | just e = just (n , record { edges = e }) +... | nothing = nothing +typeCheckHypergraph _ = nothing diff --git a/Data/SExp.agda b/Data/SExp.agda new file mode 100644 index 0000000..adf4325 --- /dev/null +++ b/Data/SExp.agda @@ -0,0 +1,75 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.SExp where + +open import Data.List using (List) +open import Data.Nat.Base using (ℕ) +open import Data.Nat.Show using () renaming (show to showNat) +open import Data.String.Base as String using (String; parens; intersperse; _<+>_) + +open List + +module ListBased where + + data SExp : Set where + Atom : String → SExp + Nat : ℕ → SExp + SExps : List SExp → SExp + + mutual + showSExp : SExp → String + showSExp (Atom s) = s + showSExp (Nat n) = showNat n + showSExp (SExps xs) = parens (intersperse " " (showList xs)) + + -- expanded out map for termination checker + showList : List SExp → List String + showList [] = [] + showList (x ∷ xs) = showSExp x ∷ showList xs + +module PairBased where + + data SExp : Set where + Atom : String → SExp + Nat : ℕ → SExp + Nil : SExp + Pair : SExp → SExp → SExp + + mutual + showSExp : SExp → String + showSExp (Atom s) = s + showSExp (Nat n) = showNat n + showSExp Nil = "()" + showSExp (Pair l r) = parens (showPair l r) + + showPair : SExp → SExp → String + showPair x (Atom s) = showSExp x <+> "." <+> s + showPair x (Nat n) = showSExp x <+> "." <+> showNat n + showPair x Nil = showSExp x + showPair x (Pair l r) = showSExp x <+> showPair l r + +open ListBased public +open PairBased + +mutual + sexpL→sexpP : ListBased.SExp → PairBased.SExp + sexpL→sexpP (Atom s) = Atom s + sexpL→sexpP (Nat n) = Nat n + sexpL→sexpP (SExps xs) = [sexpL]→sexpP xs + + [sexpL]→sexpP : List (ListBased.SExp) → PairBased.SExp + [sexpL]→sexpP [] = Nil + [sexpL]→sexpP (x ∷ xs) = Pair (sexpL→sexpP x) ([sexpL]→sexpP xs) + +mutual + sexpP→sexpL : PairBased.SExp → ListBased.SExp + sexpP→sexpL (Atom s) = Atom s + sexpP→sexpL (Nat n) = Nat n + sexpP→sexpL Nil = SExps [] + sexpP→sexpL (Pair x y) = SExps (sexpP→sexpL x ∷ sexpP→[sexpL] y) + + sexpP→[sexpL] : PairBased.SExp → List (ListBased.SExp) + sexpP→[sexpL] (Atom _) = [] + sexpP→[sexpL] (Nat _) = [] + sexpP→[sexpL] Nil = [] + sexpP→[sexpL] (Pair x y) = sexpP→sexpL x ∷ sexpP→[sexpL] y diff --git a/Data/SExp/Parser.agda b/Data/SExp/Parser.agda new file mode 100644 index 0000000..ec1b6a5 --- /dev/null +++ b/Data/SExp/Parser.agda @@ -0,0 +1,73 @@ +{-# OPTIONS --without-K --guardedness --safe #-} + +open import Text.Parser.Types.Core using (Parameters) + +module Data.SExp.Parser {l} {P : Parameters l} where + +import Data.String.Base as String +open import Data.List as List using (List) + +open import Data.Char.Base using (Char) +open import Data.List.Sized.Interface using (Sized) +open import Data.List.NonEmpty as List⁺ using (List⁺) renaming (map to map⁺) +open import Data.Subset using (Subset; into) +open import Effect.Monad using (RawMonadPlus) +open import Function.Base using (_∘_; _$_) +open import Induction.Nat.Strong using (fix; map; □_) +open import Relation.Binary.PropositionalEquality.Decidable using (DecidableEquality) +open import Relation.Unary using (IUniversal; _⇒_) +open import Level.Bounded using (theSet; [_]) +open import Text.Parser.Types P using (Parser) +open import Text.Parser.Combinators {P = P} using (_<$>_; list⁺; _<|>_; _<$_; _<&_; _<&?_; box) +open import Text.Parser.Combinators.Char {P = P} using (alpha; parens; withSpaces; spaces; char) +open import Text.Parser.Combinators.Numbers {P = P} using (decimalℕ) + +open import Data.SExp using (SExp) +open SExp + +open Parameters P using (M; Tok; Toks) + +module _ + {{𝕄 : RawMonadPlus M}} + {{𝕊 : Sized Tok Toks}} + {{𝔻 : DecidableEquality (theSet Tok)}} + {{ℂ : Subset Char (theSet Tok)}} + {{ℂ⁻ : Subset (theSet Tok) Char}} + where + + -- An atom is just a non-empty list of alphabetical characters. + -- We use `<$>` to turn that back into a string and apply the `Atom` constructor. + atom : ∀[ Parser [ SExp ] ] + atom = Atom ∘ String.fromList⁺ ∘ map⁺ (into ℂ⁻) <$> list⁺ alpha + + -- Natural number parser + nat : ∀[ Parser [ SExp ] ] + nat = Nat <$> decimalℕ + + -- Empty list parser + nil : ∀[ Parser [ SExp ] ] + nil = SExps List.[] <$ char '(' <&? box spaces <& box (char ')') + + -- Parser for a list of S-Expressions + list : ∀[ Parser [ SExp ] ⇒ Parser [ List SExp ] ] + list sexp = List⁺.toList <$> list⁺ (withSpaces sexp) + + -- Compound S-Expression parser + compound : ∀[ □ Parser [ SExp ] ⇒ Parser [ SExp ] ] + compound rec = nil <|> SExps <$> parens (map list rec) + + -- S-Expression parser + sexp : ∀[ □ Parser [ SExp ] ⇒ Parser [ SExp ] ] + sexp rec = atom <|> nat <|> compound rec + + -- Build the parser as a fixpoint since SExp is an inductive type + sexp-top : ∀[ Parser [ SExp ] ] + sexp-top = fix (Parser [ SExp ]) sexp + + -- Top-level parser for list of S-Expressions + LIST : ∀[ Parser [ SExp ] ] + LIST = SExps <$> list sexp-top + + -- Top-level S-Expression parser + SEXP : ∀[ Parser [ SExp ] ] + SEXP = withSpaces sexp-top |