From 273b12e8f016fe1a716164d514af0b2683711fd2 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 3 Jul 2025 12:01:43 -0500 Subject: Add S-Expression parser and circuit typechecker --- Data/Circuit/Gate.agda | 137 ++++++++++++++++++++++++++++++++++++++++++++ Data/Circuit/Typecheck.agda | 78 +++++++++++++++++++++++++ Data/SExp.agda | 75 ++++++++++++++++++++++++ Data/SExp/Parser.agda | 73 +++++++++++++++++++++++ 4 files changed, 363 insertions(+) create mode 100644 Data/Circuit/Gate.agda create mode 100644 Data/Circuit/Typecheck.agda create mode 100644 Data/SExp.agda create mode 100644 Data/SExp/Parser.agda (limited to 'Data') 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 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 -- cgit v1.2.3