From 5c18d33d8e558068a9040c46ffc7bc17f34c29ef Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 23 Jan 2021 21:08:18 +0000
Subject: Define semantics of expressions.

---
 src/Cfe/Expression/Base.agda | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

(limited to 'src/Cfe/Expression')

diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index 3545f9a..2a71422 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -1,16 +1,32 @@
 {-# OPTIONS --without-K --safe #-}
 
+open import Relation.Binary
+
 module Cfe.Expression.Base
-  {ℓ} (A : Set ℓ)
+  {a ℓ} (setoid : Setoid a ℓ)
   where
 
+open Setoid setoid renaming (Carrier to A)
+
+open import Cfe.Language setoid renaming (_∙_ to _∙ₗ_)
+open import Data.Fin
 open import Data.Nat
+open import Data.Vec
 
-data Expression : ℕ → Set ℓ where
+data Expression : ℕ → Set a where
   ⊥ : {n : ℕ} → Expression n
   ε : {n : ℕ} → Expression n
   Char : {n : ℕ} → A → Expression n
   _∨_ : {n : ℕ} → Expression n → Expression n → Expression n
   _∙_ : {n : ℕ} → Expression n → Expression n → Expression n
-  Var : {m : ℕ} → (n : ℕ) → Expression (suc (m + n))
+  Var : {n : ℕ} → Fin n → Expression n
   μ : {n : ℕ} → Expression (suc n) → Expression n
+
+〚_〛 : {n : ℕ} → Expression n → Vec Language n → Language
+〚 ⊥ 〛 _ = ∅
+〚 ε 〛 _ = ｛ε｝
+〚 Char c 〛 _ = ｛ c ｝
+〚 e₁ ∨ e₂ 〛 γ = 〚 e₁ 〛 γ ∪ 〚 e₂ 〛 γ
+〚 e₁ ∙ e₂ 〛 γ = 〚 e₁ 〛 γ ∙ₗ 〚 e₂ 〛 γ
+〚 Var n 〛 γ = lookup γ n
+〚 μ e 〛 γ = fix (λ X → 〚 e 〛 (X ∷ γ))
-- 
cgit v1.2.3