<commit_before>module Examples.Examples1 where


open import Syntactic.Types
open import Syntactic.Contexts Type
open import Syntactic.Terms.Total
open import Syntactic.Changes
open import Syntactic.Closures

open import Denotational.Notation
open import Denotational.Values
open import Denotational.Environments Type ⟦_⟧Type
open import Denotational.Evaluation.Total
open import Denotational.Equivalence
open import Denotational.ValidChanges

open import Changes
open import ChangeContexts
open import ChangeContextLifting
open import PropsDelta
open import SymbolicDerivation
open import Natural.Evaluation
open import Relation.Binary.PropositionalEquality

-- only some finger exercises to get used to the definitions
 
bool-identity : Term ∅ (bool ⇒ bool)
bool-identity = abs (var this)

term1 : Term ∅ bool
term1 = app bool-identity true

res : ⟦ bool ⟧
res = ⟦ term1 ⟧ ∅

-- test the denotational semantics

-- is this a good way to write unit tests in Agda?
test1 : res ≡ true
test1 = refl

-- test the natural semantics
open import Natural.Lookup
test2 : ∅ ⊢ term1 ↓ vtrue
test2 = app abs e-true (var this)
<commit_msg>tried to analyze a slightly larger example, but it is too big already<commit_after>module Examples.Examples1 where


open import Syntactic.Types
open import Syntactic.Contexts Type
open import Syntactic.Terms.Total
open import Syntactic.Changes
open import Syntactic.Closures

open import Denotational.Notation
open import Denotational.Values
open import Denotational.Environments Type ⟦_⟧Type
open import Denotational.Evaluation.Total
open import Denotational.Equivalence
open import Denotational.ValidChanges

open import Changes
open import ChangeContexts
open import ChangeContextLifting
open import PropsDelta
open import SymbolicDerivation
open import Natural.Evaluation
open import Relation.Binary.PropositionalEquality

-- only some finger exercises to get used to the definitions
 
bool-identity : Term ∅ (bool ⇒ bool)
bool-identity = abs (var this)

term1 : Term ∅ bool
term1 = app bool-identity true

res : ⟦ bool ⟧
res = ⟦ term1 ⟧ ∅

-- test the denotational semantics

-- is this a good way to write unit tests in Agda?
test1 : res ≡ true
test1 = refl

-- test the natural semantics
open import Natural.Lookup
test2 : ∅ ⊢ term1 ↓ vtrue
test2 = app abs e-true (var this)

term2 : Term (bool • bool • bool • ∅) bool
term2 = if (var this) (if (var (that this)) false true) (if (var (that (that this))) false true)

term3 : Term ∅ (bool ⇒ bool ⇒ bool ⇒ bool)
term3 = abs (abs (abs term2))

open import SymbolicDerivation
-- presumably there is some shorter way to do this?
-- I don't understand instance arguments sufficiently
term4 = derive-term {∅} {∅} {bool ⇒ bool ⇒ bool ⇒ bool} {{∅ }} term3

-- it turns out that term4 is already way too complicated to be analyzed by hand

{'fraction_non_alphanumeric': 0.06787491115849324, 'fraction_numerical': 0.00923951670220327, 'mean_word_length': 4.552268244575937, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2722672', 'n_tokens_mistral': 913, 'n_tokens_neox': 858, 'n_words': 374}