Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Start adding safety flags and removing naughty bits #13

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Start adding safety flags and removing naughty bits #13

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2f2e85d
Start adding safety flags and removing naughty bits
dsheets Nov 23, 2020
489d5b3
Complete the Eval interpretation as a coalgebra
dsheets Feb 17, 2021
6c22193
Refactor semantics
dsheets Feb 23, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/C.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# OPTIONS --safe --exact-split #-}

module C where

open import C.Lang public
4 changes: 3 additions & 1 deletion src/C/Lang.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# OPTIONS --safe --exact-split --without-K #-}

module C.Lang where

open import C.Lang.Lang public
open import C.Lang.Lang public
39 changes: 22 additions & 17 deletions src/C/Lang/Lang.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,29 +1,34 @@
{-# OPTIONS --safe --exact-split --without-K #-}

module C.Lang.Lang where

open import Data.Nat using (ℕ ; _≟_)
import Data.Nat as ℕ
open import Data.Product

open import Data.Integer as ℤ using (ℤ)
open import Relation.Binary using (Rel ; IsPartialOrder)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (Dec ; yes ; no)
open import Relation.Nullary.Decidable
open import Relation.Nullary.Product

data c_type : Set where
Int Bool : c_type -- TODO: Float type
Array : c_type → (n : ℕ) → c_type

≟-ctype : ∀ (x y : c_type) → Dec (x ≡ y)
≟-ctype Int Int = yes refl
≟-ctype Int Bool = no λ ()
≟-ctype Int (Array _ _) = no λ ()
≟-ctype Bool Int = no λ ()
≟-ctype Bool Bool = yes refl
≟-ctype Bool (Array _ -) = no λ ()
≟-ctype (Array _ _) Int = no λ ()
≟-ctype (Array _ _) Bool = no λ ()
≟-ctype (Array α n) (Array β m)
with n ≟ m | ≟-ctype α β
... | no ¬p | _ = no (λ { refl → ¬p refl })
... | yes refl | no ¬p = no (λ { refl → ¬p refl })
... | yes refl | yes refl = yes refl
Array : c_type → (n : ℕ.ℕ) → c_type

Array-inj : ∀ {m n x y} → Array m x ≡ Array n y → m ≡ n × x ≡ y
Array-inj refl = refl , refl

_≟_ : ∀ (x y : c_type) → Dec (x ≡ y)
Int ≟ Int = yes refl
Int ≟ Bool = no λ ()
Int ≟ Array _ _ = no λ ()
Bool ≟ Int = no λ ()
Bool ≟ Bool = yes refl
Bool ≟ Array _ _ = no λ ()
Array _ _ ≟ Int = no λ ()
Array _ _ ≟ Bool = no λ ()
Array x m ≟ Array y n = map′ (uncurry (cong₂ Array)) Array-inj (x ≟ y ×-dec m ℕ.≟ n)

record Lang : Set₁ where
field
Expand Down
2 changes: 2 additions & 0 deletions src/C/Semantics/SmallStep/Model.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
{-# OPTIONS --safe --exact-split --without-K --sized-types #-}

open import C.Lang

module C.Semantics.SmallStep.Model ⦃ _ : Lang ⦄ where
Expand Down
Loading