Add S-Expression parser and circuit typecheckerhypergraph-conversion

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