Добавление переменных / типов в среду ввода

Question

У меня есть среда, которая содержит набор токенов, с которыми я уже сталкивался; когда я смотрю на новый токен, я хочу добавить этот токен в текущую среду. По сути, я хочу выразить операцию объединения-объединения в среде, в которой я выполняю анализ.

что-то вроде Γ' = {Γ, x}

и если я хочу удалить переменную "х" (удалить х из среды)

Γ '= Γ - x, если x ∈ Γ .

Как правильно написать эти два формализма? Благодарю.

Answer 1

По сути, вы хотите реализовать свою среду как некоторую структуру данных, которая поддерживает вставку, удаление и поиск, и передает эту структуру данных вашему анализатору. Я полагаю, что в вашем парсере вы посмотрите на текущий токен, выполните соответствующее обновление среды, затем рекурсивно вызовите парсер на следующем токене, а затем перейдете в обновленную среду.

Какая конкретная структура данных использовать, зависит от вас, дерево двоичного поиска или его варианты подойдут, или вы можете просто использовать встроенный тип списка Haskell, если вам не нужна производительность.

РЕДАКТИРОВАТЬ: Чтобы записать этот процесс формально, вы можете позаимствовать из правил типа и как они написаны, вот ссылка. Например, мы можем обозначить, что программа успешно проанализирована Γ ⊢ program:OK (Я не уверен, если вы хотите иметь дело с реальными типами здесь). Затем, чтобы добавить токен в среду, вы можете написать

    Γ,id ⊢ program:OK
-------------------------
  Γ ⊢ add id, program:OK

Чтобы удалить токен, вы можете написать

        Γ ⊢ program:OK
------------------------------
  Γ,id ⊢ remove id, program:OK