Define simple sequential-only programs

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-09 13:59:48 -08:00
parent ca99e18184
commit 75f981cb75

View File

@ -1,10 +1,93 @@
module Language where module Language where
open import Data.String using (String) open import Data.Nat using (; suc; pred)
open import Data.Nat using () 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 data Expr : Set where
_+_ : Expr Expr Expr _+_ : Expr Expr Expr
_-_ : Expr Expr Expr _-_ : Expr Expr Expr
`_ : String Expr `_ : String Expr
#_ : 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})
_≟_ = _≟ᶠ_