<commit_before>module Denotational.ValidChanges where

open import Data.Product
open import Data.Unit
open import Relation.Binary.PropositionalEquality

open import Syntactic.Types

open import Denotational.Notation
open import Denotational.Values
open import Denotational.Equivalence

open import Changes

-- DEFINITION of valid changes via a logical relation

{-
What I wanted to write:

data ValidΔ : {T : Type} → (v : ⟦ T ⟧) → (dv : ⟦ Δ-Type T ⟧) → Set where
  base : (v : ⟦ bool ⟧) → (dv : ⟦ Δ-Type bool ⟧) → ValidΔ v dv
  fun : ∀ {S T} → (f : ⟦ S ⇒ T ⟧) → (df : ⟦ Δ-Type (S ⇒ T) ⟧) →
    (∀ (s : ⟦ S ⟧) ds (valid : ValidΔ s ds) → (ValidΔ (f s) (df s ds)) × ((apply df f) (apply ds s) ≡ apply (df s ds) (f s))) → 
    ValidΔ f df
-}
-- What I had to write:
-- Note: now I could go back to using a datatype, since the datatype is now strictly positive.
Valid-Δ : {τ : Type} → ⟦ τ ⟧ → ⟦ Δ-Type τ ⟧ → Set
Valid-Δ {bool} v dv = ⊤
Valid-Δ {S ⇒ T} f df =
  ∀ (s : ⟦ S ⟧) ds {- (valid-w : Valid-Δ s ds) -} →
    Valid-Δ (f s) (df s ds) ×
    (apply df f) (apply ds s) ≡ apply (df s ds) (f s)

diff-is-valid : ∀ {τ} (v′ v : ⟦ τ ⟧) → Valid-Δ {τ} v (diff v′ v)
diff-is-valid {bool} v′ v = tt<commit_msg>agda: Update alternative definition of Valid-Δ<commit_after>module Denotational.ValidChanges where

open import Data.Product
open import Data.Unit
open import Relation.Binary.PropositionalEquality

open import Syntactic.Types

open import Denotational.Notation
open import Denotational.Values
open import Denotational.Equivalence

open import Changes

-- DEFINITION of valid changes via a logical relation

{-
What I wanted to write:

data Valid-Δ : {T : Type} → (v : ⟦ T ⟧) → (dv : ⟦ Δ-Type T ⟧) → Set where
  base : (v : ⟦ bool ⟧) → (dv : ⟦ Δ-Type bool ⟧) → ValidΔ v dv
  fun : ∀ {S T} → (f : ⟦ S ⇒ T ⟧) → (df : ⟦ Δ-Type (S ⇒ T) ⟧) →
    (∀ (s : ⟦ S ⟧) ds → (ValidΔ (f s) (df s ds)) × ((apply df f) (apply ds s) ≡ apply (df s ds) (f s))) → 
    ValidΔ f df
-}

-- What I had to write:
-- Note: now I could go back to using a datatype, since the datatype is now strictly positive.
Valid-Δ : {τ : Type} → ⟦ τ ⟧ → ⟦ Δ-Type τ ⟧ → Set
Valid-Δ {bool} v dv = ⊤
Valid-Δ {S ⇒ T} f df =
  ∀ (s : ⟦ S ⟧) ds {- (valid-w : Valid-Δ s ds) -} →
    Valid-Δ (f s) (df s ds) ×
    (apply df f) (apply ds s) ≡ apply (df s ds) (f s)

diff-is-valid : ∀ {τ} (v′ v : ⟦ τ ⟧) → Valid-Δ {τ} v (diff v′ v)
diff-is-valid {bool} v′ v = tt
{'fraction_non_alphanumeric': 0.1585720215857202, 'fraction_numerical': 0.0, 'mean_word_length': 2.7538940809968846, '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': '6693719', 'n_tokens_mistral': 1106, 'n_tokens_neox': 1031, 'n_words': 452}