Fixed AreaAnalysis semantics

parent 9627cb69
......@@ -58,7 +58,10 @@ X = 42
\AgdaTarget{areaσ[\_]}
\begin{code}
areaσ[_] : ∀ {G} → TyGate G Area → ℂσA {G} Area
areaσ[ g ] = record { GateA = g; PlugA = plugA; _⟫A_ = seqA {X} {X} {X}; _∥A_ = parA {X} {X} {X} {X} }
areaσ[ g ] = record { GateA = g
; PlugA = plugA
; _⟫A_ = seqA {X} {X} {X}
; _∥A_ = parA {X} {X} {X} {X} }
\end{code}
%</area-combinational-algebra>
......@@ -76,12 +79,13 @@ areaσ[ g ] = record { GateA = g; PlugA = plugA; _⟫A_ = seqA {X} {X} {X}; _∥
\AgdaTarget{area[\_]}
\begin{code}
area[_] : ∀ {G} → TyGate G Area → ℂA {G} Area Area
area[_] {G} g = record { GateA = GateA (areaσ[_] {G} g)
; PlugA = PlugA areaσ[ g ]
; _⟫A_ = _⟫A_ areaσ[ g ] {X} {X} {X}
; _∥A_ = _∥A_ areaσ[ g ] {X} {X} {X} {X}
area[_] {G} g = record { GateA = GateAσ
; PlugA = PlugAσ
; _⟫A_ = _⟫Aσ_ {X} {X} {X}
; _∥A_ = _∥Aσ_ {X} {X} {X} {X}
; DelayLoopA = delayLoop {X} {X} {X}
} where open ℂσA Area using (GateA; PlugA; _⟫A_; _∥A_)
} where open ℂσA {G} areaσ[ g ] using () renaming ( GateA to GateAσ; PlugA to PlugAσ
; _⟫A_ to _⟫Aσ_; _∥A_ to _∥Aσ_ )
\end{code}
%</area-sequential-algebra>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment