<commit_before>module Syntax.Language.Atlas where

-- Base types of the calculus Atlas
-- to be used with Plotkin-style language description
--
-- Atlas supports maps with neutral elements. The change type to
-- `Map κ ι` is `Map κ Δι`, where Δι is the change type of the
-- ground type ι. Such a change to maps can support insertions
-- and deletions as well: Inserting `k -> v` means mapping `k` to
-- the change from the neutral element to `v`, and deleting
-- `k -> v` means mapping `k` to the change from `v` to the
-- neutral element.

data Atlas-type : Set where
  Bool : Atlas-type
  Map : (κ : Atlas-type) (ι : Atlas-type) → Atlas-type

open import Syntax.Type.Plotkin

data Atlas-const : Type Atlas-type → Set where
  true  : Atlas-const
    (base Bool)

  false : Atlas-const
    (base Bool)

  xor   : Atlas-const
    (base Bool ⇒ base Bool ⇒ base Bool)

  empty  : ∀ {κ ι : Atlas-type} → Atlas-const
    (base (Map κ ι))

  -- `update key val my-map` would
  -- - insert if `key` is not present in `my-map`
  -- - delete if `val` is the neutral element
  -- - make an update otherwise

  update : ∀ {κ ι : Atlas-type} → Atlas-const
    (base κ ⇒ base ι ⇒ base (Map κ ι) ⇒ base (Map κ ι))

  lookup : ∀ {κ ι : Atlas-type} → Atlas-const
    (base κ ⇒ base (Map κ ι) ⇒ base ι)

  -- Model of zip = Haskell Data.List.zipWith
  --
  -- zipWith :: (a → b → c) → [a] → [b] → [c]
  --
  -- Behavioral difference: all key-value pairs present
  -- in *either* (m₁ : Map κ a) *or* (m₂ : Map κ b) will
  -- be iterated over. Neutral element of type `a` or `b`
  -- will be supplied if the key is missing in the
  -- corresponding map.

  zip    : ∀ {κ a b c : Atlas-type} → Atlas-const
    ((base κ ⇒ base a ⇒ base b ⇒ base c) ⇒
     base (Map κ a) ⇒ base (Map κ b) ⇒ base (Map κ c))

  -- Model of fold = Haskell Data.Map.foldWithKey
  --
  -- foldWithKey :: (k → a → b → b) → b → Map k a → b

  fold   : ∀ {κ a b : Atlas-type} → Atlas-const
   ((base κ ⇒ base a ⇒ base b ⇒ base b) ⇒
    base b ⇒ base (Map κ a) ⇒ base b)

Atlas-Δbase : Atlas-type → Atlas-type
-- change to a boolean is a xor-rand
Atlas-Δbase Bool = Bool
-- change to a map is change to its values
Atlas-Δbase (Map key val) = (Map key (Atlas-Δbase val))

Atlas-Δtype : Type Atlas-type → Type Atlas-type
Atlas-Δtype = lift-Δtype₀ _ Atlas-Δbase

open import Syntax.Context

Atlas-context : Set
Atlas-context = Context {Type Atlas-type}

open import Syntax.Term.Plotkin

Atlas-term : Atlas-context → Type Atlas-type → Set
Atlas-term = Term {Atlas-type} {Atlas-const}

-- Shorthands of constants
--
-- There's probably a uniform way to lift constants
-- into term constructors.

true! : ∀ {Γ} →<commit_msg>Instantiate (Type Atlas-type) at module import.<commit_after>module Syntax.Language.Atlas where

-- Base types of the calculus Atlas
-- to be used with Plotkin-style language description
--
-- Atlas supports maps with neutral elements. The change type to
-- `Map κ ι` is `Map κ Δι`, where Δι is the change type of the
-- ground type ι. Such a change to maps can support insertions
-- and deletions as well: Inserting `k -> v` means mapping `k` to
-- the change from the neutral element to `v`, and deleting
-- `k -> v` means mapping `k` to the change from `v` to the
-- neutral element.

data Atlas-type : Set where
  Bool : Atlas-type
  Map : (κ : Atlas-type) (ι : Atlas-type) → Atlas-type

open import Syntax.Type.Plotkin Atlas-type

data Atlas-const : Type → Set where
  true  : Atlas-const
    (base Bool)

  false : Atlas-const
    (base Bool)

  xor   : Atlas-const
    (base Bool ⇒ base Bool ⇒ base Bool)

  empty  : ∀ {κ ι : Atlas-type} → Atlas-const
    (base (Map κ ι))

  -- `update key val my-map` would
  -- - insert if `key` is not present in `my-map`
  -- - delete if `val` is the neutral element
  -- - make an update otherwise

  update : ∀ {κ ι : Atlas-type} → Atlas-const
    (base κ ⇒ base ι ⇒ base (Map κ ι) ⇒ base (Map κ ι))

  lookup : ∀ {κ ι : Atlas-type} → Atlas-const
    (base κ ⇒ base (Map κ ι) ⇒ base ι)

  -- Model of zip = Haskell Data.List.zipWith
  --
  -- zipWith :: (a → b → c) → [a] → [b] → [c]
  --
  -- Behavioral difference: all key-value pairs present
  -- in *either* (m₁ : Map κ a) *or* (m₂ : Map κ b) will
  -- be iterated over. Neutral element of type `a` or `b`
  -- will be supplied if the key is missing in the
  -- corresponding map.

  zip    : ∀ {κ a b c : Atlas-type} → Atlas-const
    ((base κ ⇒ base a ⇒ base b ⇒ base c) ⇒
     base (Map κ a) ⇒ base (Map κ b) ⇒ base (Map κ c))

  -- Model of fold = Haskell Data.Map.foldWithKey
  --
  -- foldWithKey :: (k → a → b → b) → b → Map k a → b

  fold   : ∀ {κ a b : Atlas-type} → Atlas-const
   ((base κ ⇒ base a ⇒ base b ⇒ base b) ⇒
    base b ⇒ base (Map κ a) ⇒ base b)

Atlas-Δbase : Atlas-type → Atlas-type
-- change to a boolean is a xor-rand
Atlas-Δbase Bool = Bool
-- change to a map is change to its values
Atlas-Δbase (Map key val) = (Map key (Atlas-Δbase val))

Atlas-Δtype : Type → Type
Atlas-Δtype = lift-Δtype₀ Atlas-Δbase

open import Syntax.Context

Atlas-context : Set
Atlas-context = Context {Type}

open import Syntax.Term.Plotkin

Atlas-term : Atlas-context → Type → Set
Atlas-term = Term {Atlas-type} {Atlas-const}

-- Shorthands of constants
--
-- There's probably a uniform way to lift constants
-- into term constructors.

true! : ∀ {Γ} →
{'fraction_non_alphanumeric': 0.12682926829268293, 'fraction_numerical': 0.0, 'mean_word_length': 2.5421926910299004, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 7, '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': '1749828', 'n_tokens_mistral': 2062, 'n_tokens_neox': 1920, 'n_words': 852}