agda-spa/Language.agda
Danila Fedorin f21ebdcf46 Start working on the evaluation operation.
Proving monotonicity is the main hurdle here.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-10 18:13:01 -07:00

212 lines
9.1 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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; lookup; _∷_)
open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any as RelAny using ()
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; _≡_; refl)
open import Relation.Nullary using (¬_)
open import Function using (_∘_)
open import Lattice
open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs)
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ˢ
; singleton to singletonˢ
; _⊔_ to _⊔ˢ_
; `_ to `ˢ_
; _∈_ to _∈ˢ_
; ⊔-preserves-∈k₁ to ⊔ˢ-preserves-∈k₁
; ⊔-preserves-∈k₂ to ⊔ˢ-preserves-∈k₂
)
data _∈ᵉ_ : String Expr Set where
in⁺₁ : {e₁ e₂ : Expr} {k : String} k ∈ᵉ e₁ k ∈ᵉ (e₁ + e₂)
in⁺₂ : {e₁ e₂ : Expr} {k : String} k ∈ᵉ e₂ k ∈ᵉ (e₁ + e₂)
in⁻₁ : {e₁ e₂ : Expr} {k : String} k ∈ᵉ e₁ k ∈ᵉ (e₁ - e₂)
in⁻₂ : {e₁ e₂ : Expr} {k : String} k ∈ᵉ e₂ k ∈ᵉ (e₁ - e₂)
here : {k : String} k ∈ᵉ (` k)
data _∈ᵗ_ : String Stmt Set where
in←₁ : {k : String} {e : Expr} k ∈ᵗ (k e)
in←₂ : {k k' : String} {e : Expr} k ∈ᵉ e k ∈ᵗ (k' e)
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) = singletonˢ s
Expr-vars (# _) = emptyˢ
∈-Expr-vars⇒∈ : {k : String} (e : Expr) k ∈ˢ (Expr-vars e) k ∈ᵉ e
∈-Expr-vars⇒∈ {k} (e₁ + e₂) k∈vs
with Expr-Provenance k (( (Expr-vars e₁)) ( (Expr-vars e₂))) k∈vs
... | in (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
... | in _ (single k,tt∈vs₂) = (in⁺₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂)))
... | bothᵘ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
∈-Expr-vars⇒∈ {k} (e₁ - e₂) k∈vs
with Expr-Provenance k (( (Expr-vars e₁)) ( (Expr-vars e₂))) k∈vs
... | in (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
... | in _ (single k,tt∈vs₂) = (in⁻₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂)))
... | bothᵘ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
∈-Expr-vars⇒∈ {k} (` k) (RelAny.here refl) = here
∈⇒∈-Expr-vars : {k : String} {e : Expr} k ∈ᵉ e k ∈ˢ (Expr-vars e)
∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₁ k∈e₁) =
⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
{m₂ = Expr-vars e₂}
(∈⇒∈-Expr-vars k∈e₁)
∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₂ k∈e₂) =
⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
{m₂ = Expr-vars e₂}
(∈⇒∈-Expr-vars k∈e₂)
∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₁ k∈e₁) =
⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
{m₂ = Expr-vars e₂}
(∈⇒∈-Expr-vars k∈e₁)
∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₂ k∈e₂) =
⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
{m₂ = Expr-vars e₂}
(∈⇒∈-Expr-vars k∈e₂)
∈⇒∈-Expr-vars here = RelAny.here refl
Stmt-vars : Stmt StringSet
Stmt-vars (x e) = (singletonˢ x) ⊔ˢ (Expr-vars e)
∈-Stmt-vars⇒∈ : {k : String} (s : Stmt) k ∈ˢ (Stmt-vars s) k ∈ᵗ s
∈-Stmt-vars⇒∈ {k} (k' e) k∈vs
with Expr-Provenance k (( (singletonˢ k')) ( (Expr-vars e))) k∈vs
... | in (single (RelAny.here refl)) _ = in←₁
... | in _ (single k,tt∈vs') = in←₂ (∈-Expr-vars⇒∈ e (forget k,tt∈vs'))
... | bothᵘ (single (RelAny.here refl)) _ = in←₁
∈⇒∈-Stmt-vars : {k : String} {s : Stmt} k ∈ᵗ s k ∈ˢ (Stmt-vars s)
∈⇒∈-Stmt-vars {k} {k e} in←₁ =
⊔ˢ-preserves-∈k₁ {m₁ = singletonˢ k}
{m₂ = Expr-vars e}
(RelAny.here refl)
∈⇒∈-Stmt-vars {k} {k' e} (in←₂ k∈e) =
⊔ˢ-preserves-∈k₂ {m₁ = singletonˢ k'}
{m₂ = Expr-vars e}
(∈⇒∈-Expr-vars k∈e)
Stmts-vars : {n : } Vec Stmt n StringSet
Stmts-vars = foldr (λ n StringSet)
(λ {k} stmt acc (Stmt-vars stmt) ⊔ˢ acc) emptyˢ
∈-Stmts-vars⇒∈ : {n : } {k : String} (ss : Vec Stmt n)
k ∈ˢ (Stmts-vars ss) Σ (Fin n) (λ f k ∈ᵗ lookup ss f)
∈-Stmts-vars⇒∈ {suc n'} {k} (s ss') k∈vss
with Expr-Provenance k (( (Stmt-vars s)) ( (Stmts-vars ss'))) k∈vss
... | in (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs))
... | in _ (single k,tt∈vss') =
let
(f' , k∈s') = ∈-Stmts-vars⇒∈ ss' (forget k,tt∈vss')
in
(suc f' , k∈s')
... | bothᵘ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs))
∈⇒∈-Stmts-vars : {n : } {k : String} {ss : Vec Stmt n} {f : Fin n}
k ∈ᵗ lookup ss f k ∈ˢ (Stmts-vars ss)
∈⇒∈-Stmts-vars {suc n} {k} {s ss'} {zero} k∈s =
⊔ˢ-preserves-∈k₁ {m₁ = Stmt-vars s}
{m₂ = Stmts-vars ss'}
(∈⇒∈-Stmt-vars k∈s)
∈⇒∈-Stmts-vars {suc n} {k} {s ss'} {suc f'} k∈ss' =
⊔ˢ-preserves-∈k₂ {m₁ = Stmt-vars s}
{m₂ = Stmts-vars ss'}
(∈⇒∈-Stmts-vars {n} {k} {ss'} {f'} k∈ss')
-- 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')
)
indices-complete : (n : ) (f : Fin n) f ∈ˡ (proj₁ (indices n))
indices-complete (suc n') zero = RelAny.here refl
indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f'))
-- 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 = Stmts-vars 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-complete : (s : State) s ∈ˡ states
states-complete = indices-complete length
states-Unique : Unique states
states-Unique = proj₂ (indices length)
code : State Stmt
code = lookup stmts
vars-complete : {k : String} (s : State) k ∈ᵗ (code s) k ∈ˡ vars
vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s}
_≟_ : IsDecidable (_≡_ {_} {State})
_≟_ = _≟ᶠ_
-- Computations for incoming and outgoing edged will have to change too
-- when we support branching etc.
incoming : State List State
incoming
with length
... | 0 = (λ ())
... | suc n' = (λ
{ zero []
; (suc f') (inject₁ f') []
})