luau/prototyping/Examples/OpSem.agda

{-# OPTIONS --rewriting #-}

module Examples.OpSem where

open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
open import Luau.Syntax using (Block; var; val; nil; local_←_; _∙_; done; return; block_is_end)
open import Luau.Heap using (∅)

ex1 : ∅ ⊢ (local (var "x") ← val nil ∙ return (var "x") ∙ done) ⟶ᴮ (return (val nil) ∙ done) ⊣ ∅
ex1 = subst nil
Prototyping strict mode (#399) * First cut of strict mode Co-authored-by: Lily Brown <lily@lily.fyi> 2022-03-02 16:02:51 -06:00			`{-# OPTIONS --rewriting #-}`

Implement a prototype interpreter (#353) * First cut interpreter 2022-02-09 17:14:29 -06:00			`module Examples.OpSem where`

			`open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)`
Prototyping strict mode (#399) * First cut of strict mode Co-authored-by: Lily Brown <lily@lily.fyi> 2022-03-02 16:02:51 -06:00			`open import Luau.Syntax using (Block; var; val; nil; local_←_; _∙_; done; return; block_is_end)`
Prototype: added syntax for optional type annotations (#358) 2022-02-11 19:03:26 -06:00			`open import Luau.Heap using (∅)`
Implement a prototype interpreter (#353) * First cut interpreter 2022-02-09 17:14:29 -06:00
Prototyping strict mode (#399) * First cut of strict mode Co-authored-by: Lily Brown <lily@lily.fyi> 2022-03-02 16:02:51 -06:00			`ex1 : ∅ ⊢ (local (var "x") ← val nil ∙ return (var "x") ∙ done) ⟶ᴮ (return (val nil) ∙ done) ⊣ ∅`
			`ex1 = subst nil`