From 75f981cb7526640aa081bbd83e757615d6e29c38 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 9 Mar 2024 13:59:48 -0800
Subject: [PATCH] Define simple sequential-only programs

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language.agda | 87 +++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 85 insertions(+), 2 deletions(-)

diff --git a/Language.agda b/Language.agda
index 21e0784..97dcca7 100644
--- a/Language.agda
+++ b/Language.agda
@@ -1,10 +1,93 @@
 module Language where
 
-open import Data.String using (String)
-open import Data.Nat using (ℕ)
+open import Data.Nat using (ℕ; suc; pred)
+open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Data.Product using (Σ; _,_; proj₁; proj₂)
+open import Data.Vec using (Vec; foldr)
+open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
+open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁) renaming (_≟_ to _≟ᶠ_)
+open import Data.Fin.Properties using (suc-injective)
+open import Relation.Binary.PropositionalEquality using (cong; _≡_)
+open import Relation.Nullary using (¬_)
+open import Function using (_∘_)
+
+open import Lattice
+open import Utils using (Unique; Unique-map; empty; push)
 
 data Expr : Set where
     _+_ : Expr → Expr → Expr
     _-_ : Expr → Expr → Expr
     `_ : String → Expr
     #_ : ℕ → Expr
+
+data Stmt : Set where
+    _←_ : String → Expr → Stmt
+
+open import Lattice.MapSet String _≟ˢ_
+    renaming
+        ( MapSet to StringSet
+        ; insert to insertˢ
+        ; to-List to to-Listˢ
+        ; empty to emptyˢ
+        ; _⊔_ to _⊔ˢ_
+        )
+
+private
+    Expr-vars : Expr → StringSet
+    Expr-vars (l + r) = Expr-vars l ⊔ˢ Expr-vars r
+    Expr-vars (l - r) = Expr-vars l ⊔ˢ Expr-vars r
+    Expr-vars (` s) = insertˢ s emptyˢ
+    Expr-vars (# _) = emptyˢ
+
+    Stmt-vars : Stmt → StringSet
+    Stmt-vars (x ← e) = insertˢ x (Expr-vars e)
+
+    -- Creating a new number from a natural number can never create one
+    -- equal to one you get from weakening the bounds on another number.
+    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
+    z≢sf f ()
+
+    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (mapˡ suc fs)
+    z≢mapsfs [] = []
+    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
+
+    indices : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
+    indices 0 = ([] , empty)
+    indices (suc n') =
+        let
+            (inds' , unids') = indices n'
+        in
+            ( zero ∷ mapˡ suc inds'
+            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
+            )
+
+
+-- For now, just represent the program and CFG as one type, without branching.
+record Program : Set where
+    field
+        length : ℕ
+        stmts : Vec Stmt length
+
+    private
+        vars-Set : StringSet
+        vars-Set = foldr (λ n → StringSet)
+                         (λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ stmts
+
+    vars : List String
+    vars = to-Listˢ vars-Set
+
+    vars-Unique : Unique vars
+    vars-Unique = proj₂ vars-Set
+
+    State : Set
+    State = Fin length
+
+    states : List State
+    states = proj₁ (indices length)
+
+    states-Unique : Unique states
+    states-Unique = proj₂ (indices length)
+
+    _≟_ : IsDecidable (_≡_ {_} {State})
+    _≟_ = _≟ᶠ_