<commit_before>------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- The syntax of terms with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Syntax.Term where

open import Nehemiah.Syntax.Type

open import Data.Integer

import Parametric.Syntax.Term Base as Term

data Const : Term.Structure where
  intlit-const : (n : ℤ) → Const ∅ int
  add-const : Const (int • int • ∅) int
  minus-const : Const (int • ∅) (int)

  empty-const : Const ∅ (bag)
  insert-const : Const (int • bag • ∅) (bag)
  union-const : Const (bag • bag • ∅) (bag)
  negate-const : Const (bag • ∅) (bag)

  flatmap-const : Const ((int ⇒ bag) • bag • ∅) (bag)
  sum-const : Const (bag • ∅) (int)


--open Term.Structure --works
open Term.Structure Const --fails, even with the rest disabled.
{-
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Substitute.hs:183
-}

{-
-- Shorthands of constants

pattern intlit n = const (intlit-const n) ∅
pattern add s t = const add-const (s • t • ∅)
pattern minus t = const minus-const (t • ∅)
pattern empty = const empty-const ∅
pattern insert s t = const insert-const (s • t • ∅)
pattern union s t = const union-const (s • t • ∅)
pattern negate t = const negate-const (t • ∅)
pattern flatmap s t = const flatmap-const (s • t • ∅)
pattern sum t = const sum-const (t • ∅)
-}<commit_msg>Success on Nehemiah.Syntax.Term<commit_after>------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- The syntax of terms with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Syntax.Term where

open import Nehemiah.Syntax.Type

open import Data.Integer

import Parametric.Syntax.Term Base as Term

data Const : Term.Structure where
  intlit-const : (n : ℤ) → Const ∅ int
  add-const : Const (int • int • ∅) int
  minus-const : Const (int • ∅) (int)

  empty-const : Const ∅ (bag)
  insert-const : Const (int • bag • ∅) (bag)
  union-const : Const (bag • bag • ∅) (bag)
  negate-const : Const (bag • ∅) (bag)

  flatmap-const : Const ((int ⇒ bag) • bag • ∅) (bag)
  sum-const : Const (bag • ∅) (int)


open Term.Structure Const public

-- Import Base.Data.DependentList again here, as part of the workaround for
-- agda/agda#1985; see Parametric.Syntax.Term for info.
--
-- XXX This import is needed to define the patterns in the right scope; if we
-- don't, • gets bound to a different occurrence, and we notice that during
-- typechecking, which happens at use site.
open import Base.Data.DependentList public

-- Shorthands of constants

pattern intlit n = const (intlit-const n) ∅
pattern add s t = const add-const (s • t • ∅)
pattern minus t = const minus-const (t • ∅)
pattern empty = const empty-const ∅
pattern insert s t = const insert-const (s • t • ∅)
pattern union s t = const union-const (s • t • ∅)
pattern negate t = const negate-const (t • ∅)
pattern flatmap s t = const flatmap-const (s • t • ∅)
pattern sum t = const sum-const (t • ∅)
{'fraction_non_alphanumeric': 0.20632385819227084, 'fraction_numerical': 0.002235707441711913, 'mean_word_length': 2.2659019812304484, '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': '2454522', 'n_tokens_mistral': 1085, 'n_tokens_neox': 988, 'n_words': 437}