Как мне написать эту функцию на SML

Я пытаюсь написать функцию в Isabelle для некоторых задач в задании, и я хотел убедиться, что моя функция работает правильно, поэтому я подумал о тестировании ее в SML, но, похоже, не могу понять, как ее написать . Я никогда не использовал / не писал / не изучал функциональное программирование, поэтому у меня с этим возникают небольшие проблемы. Может ли кто-нибудь мне помочь или, может быть, если в Изабель есть что-то о тестировании работы функции, может ли он указать мне правильное направление?

Функции следующие, и в основном они удаляют первое вхождение элемента в списке и удаляют все вхождения из списка.

fun del1:: "'a ⇒ 'a list ⇒ 'a list" where
  "del1 a Nil = Nil" |
  "del1 a (x#xs) = (if x = a then xs else x#(del1 a xs))"


fun delall:: "'a ⇒ 'a list ⇒ 'a list" where
  "delall a Nil = Nil" |
  "delall a (x#xs) = (if x = a then (delall a xs) else x#(delall a xs))"

functional-programming sml isabelle
person Andreas Andreou    schedule 01.02.2014    source источник

Ответы (2)


arrow_upward
3
arrow_downward

Я не совсем уверен, понял ли я ваш вопрос. Во-первых, синтаксис Isabelle / HOL и SML не очень отличается. Если вы просто хотите получить варианты своей функции в SML, возможно, самый быстрый способ - использовать генератор кода Изабель.

export_code del1 delall in SML

что приводит к чему-то вроде

fun del1 A_ a [] = []
  | del1 A_ a (x :: xs) = (if HOL.eq A_ x a then xs else x :: del1 A_ a xs);

fun delall A_ a [] = []
  | delall A_ a (x :: xs) =
    (if HOL.eq A_ x a then delall A_ a xs else x :: delall A_ a xs);

Однако, поскольку он содержит некоторые специфические для Изабель вещи (например, конструкцию словаря для избавления от классов типов), возможно, вы предпочитаете рукописный код:

fun del1 a [] = []
  | del1 a (x::xs) = if x = a then xs else x :: (del1 a xs)

fun delall a [] = []
  | delall a (x::xs) = if x = a then delall a xs else x :: delall a xs

С другой стороны, если вы просто хотите опробовать свои функции на некоторых входах, вы можете сделать это внутри Isabelle, используя value. Например.,

value "del1 (2::nat) [1, 2 , 3]"
value "delall ''x'' [''x'', ''y'', ''z'', ''q'', ''x'']"
person chris    schedule 01.02.2014
comment
Ну, на самом деле все они были тем, что я искал, но особенно второе, чтобы я мог понять, что я делаю не так ... - person Andreas Andreou; 02.02.2014

arrow_upward
1
arrow_downward

К ответу Криса мало что можно добавить, только эта деталь: в Isabelle2013-2 на панели документации Isabelle / jEdit есть несколько примеров быстрого старта. Это включает src/HOL/ex/ML.thy, который показывает немного Isabelle / HOL как логического языка и SML как функционального языка, а также некоторые связи между ними.

person Makarius    schedule 02.02.2014