Решение о том, может ли неправильная программа иметь правильное продолжение - PullRequest
3 голосов
/ 16 марта 2011

(Следующий вопрос касается языка OCaml и содержит примеры на OCaml, но вопрос очень общий, и, вероятно, правильный ответ для любого другого компьютерного языка также решит мою проблему. Итак, просто примите этот вопрос на вашем любимом языке. )

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

Я предполагаю, что где-то есть компилятор языка и что я могу применить его и получить ответ, говорящий либо «Компилируется», либо «Не компилируется - ошибка в строке X, символ Y» (как и во всяком случае, с большинством языков). Таким образом, я хотел бы иметь функцию, которая принимает программу и возвращает:

  • Исправить - если строка содержит правильную программу;
  • Ошибочно - если строка содержит неверную программу, которая, независимо от того, как вы ее объедините, никогда не станет правильной;
  • Неполный - если строка содержит неверную программу, которая не является ошибочной.

Например, программа OCaml let x = f неверна, поскольку f не была определена ко времени ее использования. И это не может быть продолжено, потому что все, что вы пишете после f, всегда будет идентификатором, который не был определен ранее. Программа let x = также неверна; но если мы расширим let x = 5, тогда у нас будет совершенно корректная программа. Итак, моя функция должна возвращать Erroneous в первом случае и Incomplete во втором.

Все может стать сложнее, если у нас есть программа

let ans = 5
let x = a

потому что моя функция должна видеть, что если я продолжу программу с ns, тогда программа станет правильной.

Мой вопрос : как вы думаете, возможно ли написать такую ​​функцию / алгоритм? Если так, какова общая идея? Если нет, попробуйте убедить меня, что это не так.

(Я буду рад любым выводам или частичным ответам, например, тем, что подразумевает «Неполный». Например, я считаю, что если языковой компилятор говорит об ошибке в строке 3, а программа имеет 100 строк, то есть невозможно продолжение программы.)

1 Ответ

6 голосов
/ 16 марта 2011

В вашем первом примере, let x = f, что если я добавлю un y -> y?

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

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

Свойства, облегчающие на этапе лексирования / синтаксического анализа, состоят в том, что лексер управляется парсером по требованию - он читает только настолько, насколько необходимо для парсера, чтобы определить поток токенов - и парсер «строгий» или сбои на раннем этапе вместо запроса дополнительной информации на сайте сбоев.

Последним основным этапом правильности программы являются разрешение идентификатора (к чему относится это имя переменной?) И система типов - существуют и другие критерии, такие как проверка арности конструкторов и имен типов, но они ' не очень интересно WRT. у тебя проблема. Как правило, они не написаны в стиле, ориентированном на спрос, или в более общем случае не пытаются рассуждать о частичной информации. Должна быть возможность изменить их таким образом, но это, вероятно, потребует больших усилий.

Хорошее направление - "инкрементные парсеры". Многие люди осознали необходимость инкрементальности программных инструментов, связанных с редактором (где программы пишутся постепенно). Они решают более общую проблему обновления абстрактной информации после конкретного изменения исходного кода; не только изменение «добавлено в конце», но и более общий вид изменений. Их инструменты тоже могут решить вашу проблему.

Редактировать : Ах, я наконец-то нашел то, что искал. Вы должны взглянуть на дифференцирующие парсеры Олега .

...