agda-spa/Language.agda

module Language where

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})
    _≟_ = _≟ᶠ_