<commit_before>module Syntax.FreeVars.Popl14 where

-- Free variables of Calculus Popl14
--
-- Contents
-- FV: get the free variables of a term
-- closed?: test if a term is closed, producing a witness if yes.

open import Popl14.Syntax.Type
open import Popl14.Change.Term
open import Base.Syntax.Vars Type public

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

FV : ∀ {τ Γ} → Term Γ τ → Vars Γ
FV {Γ = Γ} (intlit n) = none
FV (add s t) = FV s ∪ FV t
FV (minus t) = FV t

FV {Γ = Γ} empty = none
FV (insert s t) = FV s ∪ FV t
FV (union s t) = FV s ∪ FV t
FV (negate t) = FV t

FV (flatmap s t) = FV s ∪ FV t
FV (sum t) = FV t

FV (var x) = singleton x
FV (abs t) = tail (FV t)
FV (app s t) = FV s ∪ FV t

closed? : ∀ {τ Γ} → (t : Term Γ τ) → (FV t ≡ none) ⊎ ⊤
closed? t = empty? (FV t)<commit_msg>Implement FV more parametrically.<commit_after>module Syntax.FreeVars.Popl14 where

-- Free variables of Calculus Popl14
--
-- Contents
-- FV: get the free variables of a term
-- closed?: test if a term is closed, producing a witness if yes.

open import Popl14.Syntax.Type
open import Popl14.Change.Term
open import Base.Syntax.Vars Type public

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

FV : ∀ {τ Γ} → Term Γ τ → Vars Γ
FV-terms : ∀ {Σ Γ} → Terms Γ Σ → Vars Γ

FV (const ι ts) = FV-terms ts
FV (var x) = singleton x
FV (abs t) = tail (FV t)
FV (app s t) = FV s ∪ FV t

FV-terms ∅ = none
FV-terms (t • ts) = FV t ∪ FV-terms ts

closed? : ∀ {τ Γ} → (t : Term Γ τ) → (FV t ≡ none) ⊎ ⊤
closed? t = empty? (FV t)
{'fraction_non_alphanumeric': 0.12024922118380062, 'fraction_numerical': 0.009968847352024923, 'mean_word_length': 3.0049875311720697, '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': '7527989', 'n_tokens_mistral': 715, 'n_tokens_neox': 652, 'n_words': 295}