Mixfix синтаксис — когда положение аргументов функции или оператора задаётся специальными маркерами (Maude/Agda2 — подчеркиванием). Сами аргументы могут быть выражениями со своими правилами расположения аргументов и уровнями вложенности.
Примеры:
if_then_else_ — применять надо "if A then B else C"
_+_ — "1 + 2"
-_ — "- 10"
В сочетании с Юникодом получаются прикольные вещи. Да и без Юникода тоже ничего:
data [_] : A -> Set where
[] : [ A ]
_::_ : A -> [ A ] -> [ A ]
infixr 30 _||_
infix 20 _elem_
_elem_ : A -> [ A ] -> Bool
x elem [] = False
x elem (y :: ys) = x == y || x elem ys
-- BTW, elem__ отличается от _elem_
Так вот, в чём вопрос: что же можно описать с помощью mixfix синтаксиса?
В Maude можно даже списки описывать:
_,_ : A -> Q -> List
-- 1 , 2 , 3 будет списком.
-- кстати, упорядочение списка на Maude:
A , B => B , A if A < B -- это действительно так. ;)
Но Maude "слабо типизирован", это система переписывания термов, которая на этапе выполнения решает, принадлежит ли элемент множеству, или нет. То есть, он не ругнётся на "1 , 'a' , 3", а просто не сможет что-то выполнить.
А что можно описать в строго типизированном варианте?
Я попытался прикинуть, как и что надо задать, чтобы получить запись [[ 1 , 2 , 3 ]], чтобы писать списки практически удобным образом, но не смог понять, какой же тип должен быть у [_]].
Если переопределить "_,_ = _::_", то мы можем записывать списки так: "(1 , 2 , 3 , [])". Достаточно удобно, но не совсем привычно. Совсем привычно не получается.
Если у кого имеются (или появятся) мысли, милости прошу, очень интересно.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
T>Так вот, в чём вопрос: что же можно описать с помощью mixfix синтаксиса?
Ну вот тот же самый if then else например. case of, while do done, и прочие mixfix-конструкции.
T>Я попытался прикинуть, как и что надо задать, чтобы получить запись [[ 1 , 2 , 3 ]], чтобы писать списки практически удобным образом, но не смог понять, какой же тип должен быть у [_]].
T>Если переопределить "_,_ = _::_", то мы можем записывать списки так: "(1 , 2 , 3 , [])". Достаточно удобно, но не совсем привычно. Совсем привычно не получается.
T>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно.
Все таки [1,2,3] -- это синтаксический сахар, переводимый в 1:2:3:[]. Как и [1..10] в enumFromTo. В Agda так, скорее всего, не выйдет. Можно поизголяться через universe-ы, в простых случаях, для фиксированного набора типов элементов получится.
Что-то в таком роде (синтаксис не помню, в agda не проверял)
data ListU : a -> Set where
NatE : ListU Nat
BoolE : ListU Bool
ConsE : ListU a -> ListU a
list : ListU a -> Set
list NatE = Nat
list BoolE = Bool
list (ConsE a) = [a]
cons : hd -> {tl:ListU hd} -> (list tl) -> [hd]
cons hd {NatE} n = hd :: n :: []
cons hd {BoolE} b = hd :: b :: []
cons hd {ConsE} tl = hd :: tl
Но это дикое ограниченное убожество. Не полиморфное, непонятки со списком из одного элемента, и непонятки со списком списков (хотя, наверное, можно подкрутить).
Можно чуть менее ограниченно решить в духе template metaprogramming с explicit specialization (или overlapping/еще какие-нить instances)
instance Cons a a where ...
instance Cons a [a] where ...
придется еще крутить с унификацией, и опять будет лажа со списком из одного элемента.
В общем можно сделать оператор _::_ который получая список ведет себя так, а примитив сяк. Но сделать его полиморфным в Agda, скорее всего, не выйдет. И будут проблемы, что 1::2 -- список, а 1 -- непонятно что. Можно еще с [_]] поизголяться, чтобы [[a :: b]] = a :: b и [a]] = a :: []. Но надо ли это.
T>>Так вот, в чём вопрос: что же можно описать с помощью mixfix синтаксиса? V>Ну вот тот же самый if then else например. case of, while do done, и прочие mixfix-конструкции.
Получается многое, но не всё.
T>>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно. V>Все таки [1,2,3] -- это синтаксический сахар, переводимый в 1:2:3:[]. Как и [1..10] в enumFromTo. В Agda так, скорее всего, не выйдет. Можно поизголяться через universe-ы, в простых случаях, для фиксированного набора типов элементов получится.
Вот я и думал, а можно ли перевести синтаксический сахар в mixfix. Получается, что далеко не весь. Как минимум, без перегрузки не обойтись. Да и сравнение с образцом тоже будет страдать.
V>Но надо ли это.
"Мы отметём этот вопрос, как неорганизованный." (С) Выбегалло
У нас тут "фи-и-илосо-офия" программирования.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
T>>>Так вот, в чём вопрос: что же можно описать с помощью mixfix синтаксиса? V>>Ну вот тот же самый if then else например. case of, while do done, и прочие mixfix-конструкции.
T>Получается многое, но не всё.
Ну так mixfix -- это все-таки infix + еще чуть-чуть. Некоторые формы на нем легко записываются, некоторые не очень. Полноценные синтаксические преобразования -- это уже дальше. В agda, думаю, есть более приоритетные задачи. Хотя может кто и сделает какие-нить hygienic mixfix macros
T>>>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно. V>>Все таки [1,2,3] -- это синтаксический сахар, переводимый в 1:2:3:[]. Как и [1..10] в enumFromTo. В Agda так, скорее всего, не выйдет. Можно поизголяться через universe-ы, в простых случаях, для фиксированного набора типов элементов получится.
T>Вот я и думал, а можно ли перевести синтаксический сахар в mixfix. Получается, что далеко не весь. Как минимум, без перегрузки не обойтись. Да и сравнение с образцом тоже будет страдать.
Оно и в хаскеле страдает. case [1..5] of [1..5] -> True; _ -> False. тоже не пашет ))
А по поводу [1,2,3] есть еще мысль сделать ф-ии _] _,_ и [_ -- может что и выйдет. Правда появится проблема с пустыми списками, и pattern match тоже не запашет. Но все-таки это не тот инструмент.
Здравствуйте, thesz, Вы писали:
T>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно.
Надо просто вместо примитивного mixfix взять что-то поумнее. Например PEG.
Тогда можно будет описывать намного более широкий класс конструкций.
Ибо mixfix это подмножество регулярных грамматик, а PEG строго мощнее регулярных грамматик, почти полностью (*) покрывает контекстно свободные грамматики и захватывает часть контекстно зависимых.
* математически строгого описания взаимоотношений PEG и CFG насколько я знаю пока нет.
Короче если в Agda2 вместо (**) mixfix воткнуть PEG получится очень интересная штука. А если вспомнить про то что PEG может работать не только на основе текста но и принимать ЦУ от алгоритма вывода типов...
** можно и вместе ибо превратить mixfix в правило для PEG задача тривиальная
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
T>>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно. WH>Надо просто вместо примитивного mixfix взять что-то поумнее. Например PEG. WH>Тогда можно будет описывать намного более широкий класс конструкций. WH>Ибо mixfix это подмножество регулярных грамматик, а PEG строго мощнее регулярных грамматик, почти полностью (*) покрывает контекстно свободные грамматики и захватывает часть контекстно зависимых.
Ценно. Интересно.
Спасибо.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, WolfHound, Вы писали:
WH>Здравствуйте, thesz, Вы писали:
T>>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно. WH>Надо просто вместо примитивного mixfix взять что-то поумнее. Например PEG. WH>Тогда можно будет описывать намного более широкий класс конструкций. WH>Ибо mixfix это подмножество регулярных грамматик, а PEG строго мощнее регулярных грамматик, почти полностью (*) покрывает контекстно свободные грамматики и захватывает часть контекстно зависимых.
Посмотрел чуть-чуть на PEG. Какой-то он очень низкоуровневый. В нем как-нибуть можно задавать приоритеты операций? И можно ли его вообще по человечески расширять?
Фишка infix/mixfix в том, что для расширения синтаксиса достаточно определить ф-ю и, возможно, добавить одну строку (ассоциативность с приоритетом) в том же модуле. Т.е. синтаксис расширяется модульно. Если для расширения синтаксиса понадобится лезть в парсер языка, то это не есть куль (если только у нас не лисп).
Можно ли, при помощи PEG, добавлять в язык правила по отдельности?
Здравствуйте, vshabanov, Вы писали:
V>Посмотрел чуть-чуть на PEG. Какой-то он очень низкоуровневый. В нем как-нибуть можно задавать приоритеты операций? И можно ли его вообще по человечески расширять?
Можно.
Также как и в CFG
Но так как правила будет добавлять парсер то никакой ручной возни с этой структурой не будет.
V>Фишка infix/mixfix в том, что для расширения синтаксиса достаточно определить ф-ю и, возможно, добавить одну строку (ассоциативность с приоритетом) в том же модуле. Т.е. синтаксис расширяется модульно. Если для расширения синтаксиса понадобится лезть в парсер языка, то это не есть куль (если только у нас не лисп).
Ну для того чтобы добавить конструкцию которую добавляет mixfix в парсер придется лезть не больше чем в случае с mixfix.
А там где mixfix'а маловато будет придется написать кусочек грамматики.
Но так mixfix в этом случае вообще ни на что не способен.
Например тот же конструктор списка будет выглядеть как-то так:
data Nat : Set where
zero : Nat
suc : Nat -> Nat
data Vec (A : Set) : Nat -> Set where
[] : Vec A zero
_::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)
data List (A : Set) : Set where
[] : List A
_::_ : A -> List A -> List A
"[" list ("," list)* "]" : {A : Set}{n : Nat} -> (list : Vec A n) -> List A
... list = vecToList list
Если компилятор в правиле находит несколько упоминаний одного значения и/или значение внутри оператора повторения то он засовывает все что разобрал в Vec A n где A тип значения, а n количество разобранных значений.
V>Можно ли, при помощи PEG, добавлять в язык правила по отдельности?
В том то и прелесть данного формализма что можно.
Более того правила можно добавлять по ходу разбора текста.
Те разобрал правило и сразу после этого оно может быть использовано.
Все руке не доходят прикрутить это дело к немерлу
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
WH>В том то и прелесть данного формализма что можно. WH>Более того правила можно добавлять по ходу разбора текста. WH>Те разобрал правило и сразу после этого оно может быть использовано.
С комбинаторами это получится хорошо. Видимые проблемы: рапорт об ошибках разбора и рапорт об ошибках проверки типов.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
WH>>В том то и прелесть данного формализма что можно. WH>>Более того правила можно добавлять по ходу разбора текста. WH>>Те разобрал правило и сразу после этого оно может быть использовано. T>С комбинаторами это получится хорошо.
Вот тут я не понял как?
Ведь комбинаторный парсер это большое замыкание.
И я совершенно не понимаю как можно поменять потроха этого замыкания в процессе разбора теста этим замыканием.
T>Видимые проблемы: рапорт об ошибках разбора
Не хуже чем у любого рекурсивного парсера. А у них рапорты самые разборчивые.
Собственно PEG это и есть формальное описание рекурсивного парсера.
T>и рапорт об ошибках проверки типов.
Тут я вообще никаких проблем не вижу.
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
WH>>>В том то и прелесть данного формализма что можно. WH>>>Более того правила можно добавлять по ходу разбора текста. WH>>>Те разобрал правило и сразу после этого оно может быть использовано. T>>С комбинаторами это получится хорошо. WH>Вот тут я не понял как? WH>Ведь комбинаторный парсер это большое замыкание. WH>И я совершенно не понимаю как можно поменять потроха этого замыкания в процессе разбора теста этим замыканием.
pPEGDescr :: P (P Expr, P Pat)
pPEGDescr = ...
pFuncDef :: P Pat -> P Expr -> P FuncDef
pFuncDef pat expr = do
funcName <- pIdent
pats <- pMany pat
pEqual
expr <- pexpr
return $ FuncDef funcName pats expr
pModule :: P Module
pModule = do
pegs <- pMany parsePEGDescr
let anyPattern = foldr combinePatDef defaultPatterns (map fst pegs)
let anyExpression = foldr combineExpr defaultExpr (map snd pegs)
funcs <- pMany (pFuncDef anyPattern anyExpression)
return $ Module funcs
Плюс-минус, как-то так.
T>>Видимые проблемы: рапорт об ошибках разбора WH>Не хуже чем у любого рекурсивного парсера. А у них рапорты самые разборчивые. WH>Собственно PEG это и есть формальное описание рекурсивного парсера.
Да, тут будет умеренно просто. За исключением, возможно, если у нас получилось несколько вариантов разбора.
T>>и рапорт об ошибках проверки типов. WH>Тут я вообще никаких проблем не вижу.
Мы сделали разбор образца и выражения, и они преобразуются во внутренние форматы. Все проверки идут над внутренними представлениями, поэтому и рапорт будет в их терминах, не в терминах использованных нами конструкций.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
T>Плюс-минус, как-то так.
Понятно. Только спроектировано криво.
Правила нужно тащить внутри монады, а не передавать явно.
В твоем случае создается куча ненужного шума, куча лишней работы если появятся еще группы правил, defaultPatterns и defaultExpr непонятного происхождения, все правила должны быть описаны вначале модуля, другие модули которые экспортируют правила тоже можно подключать только в начале, что ты будешь делать с конструкциями типа let open SomeModule in тоже не очень понятно,...
T>Да, тут будет умеренно просто. За исключением, возможно, если у нас получилось несколько вариантов разбора.
Тут нам может помочь типизатор. PEG по построению не имеет неоднозначностей. По этому будет выбрано первое правило которое позволило разобрать текст. Но если в процессе вывода типов возникла ошибка то мы можем откатиться и попробовать следующие правило.
T>Мы сделали разбор образца и выражения, и они преобразуются во внутренние форматы. Все проверки идут над внутренними представлениями, поэтому и рапорт будет в их терминах, не в терминах использованных нами конструкций.
Рапорт будет вида: В строке XXX по смещению YYY ожидается BlahMinor, а получен BlahMajor.
Если да то ИМХО проблем с пониманием в подавляющем большинстве случаев не будет.
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
T>>Плюс-минус, как-то так. WH>Понятно. Только спроектировано криво. WH>Правила нужно тащить внутри монады, а не передавать явно. WH>В твоем случае создается куча ненужного шума, куча лишней работы если появятся еще группы правил, defaultPatterns и defaultExpr непонятного происхождения, все правила должны быть описаны вначале модуля, другие модули которые экспортируют правила тоже можно подключать только в начале, что ты будешь делать с конструкциями типа let open SomeModule in тоже не очень понятно,...
Запихивать вунтрь монады, или нет — вопрос второй.
Мне больше нравятся явно передаваемые параметры. Если уж они надоедают, тогда и вношу внутрь монады.
T>>Да, тут будет умеренно просто. За исключением, возможно, если у нас получилось несколько вариантов разбора. WH>Тут нам может помочь типизатор. PEG по построению не имеет неоднозначностей. По этому будет выбрано первое правило которое позволило разобрать текст. Но если в процессе вывода типов возникла ошибка то мы можем откатиться и попробовать следующие правило.
Это означает наличие некоторого труда по организации всего этого дела.
T>>Мы сделали разбор образца и выражения, и они преобразуются во внутренние форматы. Все проверки идут над внутренними представлениями, поэтому и рапорт будет в их терминах, не в терминах использованных нами конструкций. WH>Рапорт будет вида: В строке XXX по смещению YYY ожидается BlahMinor, а получен BlahMajor. WH>Если да то ИМХО проблем с пониманием в подавляющем большинстве случаев не будет.
Он будет сложней, чем ты это представил, это точно.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Думаю что можно сойтись на том что идея технически реализуема. Хоть и придется решить несколько непростых задач.
При этом получится система позволяющая описывать практически произвольный синтаксис.
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, thesz, Вы писали:
T>Да, тут будет умеренно просто. За исключением, возможно, если у нас получилось несколько вариантов разбора.
Нескольких вариантов не может быть по определению. PEG их не допускает.
А соощения об ошибках можно сделать такими же разборчивыми как при написании парсера в ручную методом рекурсивного спуска. Собственно один и вариантов создания парсера по PEG — это создание рекурсивного нисходящего парсера с откатами.
T>>>и рапорт об ошибках проверки типов. WH>>Тут я вообще никаких проблем не вижу.
T>Мы сделали разбор образца и выражения, и они преобразуются во внутренние форматы. Все проверки идут над внутренними представлениями, поэтому и рапорт будет в их терминах, не в терминах использованных нами конструкций.
Парсинг не имеет никакого отношения к семантичесому анализу. Как сделаешь так и будет. PEG позволяет вставлять тебе семантические предикаты. А то как ты их реализуешь — это твои проблемы.
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
T>>Мы сделали разбор образца и выражения, и они преобразуются во внутренние форматы. Все проверки идут над внутренними представлениями, поэтому и рапорт будет в их терминах, не в терминах использованных нами конструкций. VD>Парсинг не имеет никакого отношения к семантичесому анализу. Как сделаешь так и будет. PEG позволяет вставлять тебе семантические предикаты. А то как ты их реализуешь — это твои проблемы.
Мне надо выдать сообщение об ошибке в терминах исходной программы, а не некоторого абстрактного ядра, куда всё транслируется.
Если у меня был список [1,2,3], то негоже будет его преобразовывать в (123:[]))), что сказать, что в нём ошибка.
Это мелочь, но очень удобно.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
T>Мне надо выдать сообщение об ошибке в терминах исходной программы, а не некоторого абстрактного ядра, куда всё транслируется.
T>Если у меня был список [1,2,3], то негоже будет его преобразовывать в (123:[]))), что сказать, что в нём ошибка.
T>Это мелочь, но очень удобно.
PEG это просто рекурсивный парсинг. Так, что еще раз повторю, как реализуешь так и будет. Тут проблемы точно искать не надо.
Проблемы будут в первую очередь в производительности.
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
T>>Мне надо выдать сообщение об ошибке в терминах исходной программы, а не некоторого абстрактного ядра, куда всё транслируется. T>>Если у меня был список [1,2,3], то негоже будет его преобразовывать в (123:[]))), что сказать, что в нём ошибка. T>>Это мелочь, но очень удобно. VD>PEG это просто рекурсивный парсинг. Так, что еще раз повторю, как реализуешь так и будет. Тут проблемы точно искать не надо.
VD>Проблемы будут в первую очередь в производительности.
Ты меня не слушаешь.
Я не про разбор говорю, а про отображение обратно в исходный синтаксис для отчёта пользователю.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
T>Я не про разбор говорю, а про отображение обратно в исходный синтаксис для отчёта пользователю.
А не проще печатать исходную строку? — компиляторы обычно так и делают.