Types as (Abstract) Intepreters for HDLs and Graphs...

REPL.txt

Idris 0.5.1-8bd5ca949

1/1: Building Temp (Temp.idr)
λΠ> fst (snd example)
G [3, 2, 1, 1, 2, 1, 3] [(2, 1), (3, 1)]
λΠ> example
MkDPair 3 (MkDPair (G [3, 2, 1, 1, 2, 1, 3] [(2, 1),
                                             (3,
                                             1)]) (Port LOGIC OUT (Port LOGIC IN (Port LOGIC IN (GDecl (Gate (Var (There (There Here))) (Var (There Here)) (Var Here)) Stop)))))
λΠ> :t example
Temp.example : DPair Nat (\c => DPair Graph (\g => Term 0 (G [] []) [] Unit () c g))
λΠ> :t (fst (snd example))
fst (snd example) : Graph
λΠ> snd (snd example)
Port LOGIC OUT (Port LOGIC IN (Port LOGIC IN (GDecl (Gate (Var (There (There Here))) (Var (There Here)) (Var Here)) Stop)))
λΠ> 

Temp.idr

module Temp

import Decidable.Equality
import Data.List.Elem

record Graph where
  constructor G
  vertices : List Nat
  edges    : List (Pair Nat Nat)


insertVertex : Nat -> Graph -> Graph
insertVertex n (G vs es)
  = G (n::vs) es

insertEdge : (Nat, Nat) -> Graph -> Graph
insertEdge (a,b) (G vs es)
  = G vs (MkPair a b :: es)

addEdge : (Nat, Nat) -> Graph -> Graph
addEdge (a,b) = { vertices $= (++) [b,a] , edges $= (::) (a,b)}

fromEdges : List (Nat, Nat) -> Graph
fromEdges = foldr addEdge (G Nil Nil)

merge : Graph -> Graph -> Graph
merge a
  = { vertices $= (++) (vertices a)
    , edges    $= (++) (edges a)}

namespace DataType
  public export
  data DataType = LOGIC | Vect Nat DataType

namespace Ty

  namespace Property
    public export
    data Direction = IN | OUT

  public export
  data Ty = Port DataType Direction
          | Chan DataType
          | Gate
          | Unit

namespace Context

  public export
  Interp : Ty -> Type
  Interp (Port d y) = Nat
  Interp (Chan s)   = (Nat, Nat)
  Interp Gate       = Graph
  Interp Unit       = Unit

  public export
  record Item where
    constructor I
    type   : Ty
    denote : Interp type

namespace Term

  public export
  data Term : (c_in   : Nat)
           -> (g_in   : Graph)
           -> (ctxt   : List Item)
           -> (type   : Ty)
           -> (denote : Interp type)
           -> (c_out  : Nat)
           -> (g_out  : Graph)
                     -> Type
    where
      Stop : Term c_in g_in ctxt Unit () c_in g_in

      Var : Elem (I ty de) ctxt
         -> Term c_in g_in ctxt ty de c_in g_in

      Port : (dtype  : DataType)
          -> (dir   : Direction)
          -> (scope : Term (S c_in)
                           (insertVertex (S c_in) g_in)
                           (I (Port dtype dir) (S c_in) :: ctxt)
                           Unit
                           ()
                           c_out
                           g_out)
                   -> Term c_in  g_in  ctxt Unit ()
                           c_out g_out

      Wire : (dtype : DataType)
          -> (scope : Term (S (S c_in))
                           (insertEdge (S (S c_in), S (S c_in)) (insertVertex (S (S c_in)) (insertVertex (S c_in) g_in)))
                           (I (Chan dtype) (S c_in, S (S c_in)) :: ctxt)
                           Unit
                           ()
                           c_out
                           g_out)
                   -> Term c_in  g_in  ctxt Unit ()
                           c_out g_out

      Gate : (outport : Term c_in  g_in ctxt (Port LOGIC OUT) vo
                             c_a   g_a)
          -> (inportA : Term c_a   g_a  ctxt (Port LOGIC IN)  va
                             c_b   g_b)
          -> (inportB : Term c_b   g_b  ctxt (Port LOGIC IN)  vb
                             c_out g_out)
                     -> Term c_in  g_in ctxt Gate (fromEdges [(va,vo), (vb,vo)])
                             c_out g_out

      GDecl : (gate : Term c_in  g_in  ctxt Gate g
                           c_mid g_mid)
           -> (scope : Term c_mid (merge g_mid g) (I Gate g :: ctxt) Unit ()
                            c_out g_out)
                   -> Term c_in g_in ctxt Unit ()
                           c_out g_out


example : (c : Nat **
           g : Graph ** Term Z (G Nil Nil) Nil Unit ()
                             c g)
example
  = (_ ** _ **
      Port LOGIC OUT
      $ Port LOGIC IN
      $ Port LOGIC IN
      $ GDecl (Gate (Var (There (There Here)))
                    (Var (There Here))
                    (Var Here))
      $ Stop)

-- [ EOF ]