Дафни, я хочу проверить, могу ли я улучшить этот код - PullRequest
Новая
       66

Дафни, я хочу проверить, могу ли я улучшить этот код

0 голосов
/ 28 мая 2020 
datatype Tree<T> = Leaf | Node(Tree<T>, Tree<T>, T)//Declare Datatype Tree which can either be a leaf or a node; Node can agian be defined as 2 trees and 1 split point/node
datatype List<T> = Nil | Cons(T, List<T>)//Declare datatype List as either Nil or as Cons of Tree and a list

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

// Функция ниже принимает 2 списка xs и ys в качестве входных данных и возвращает список, который c представляет собой комбинацию из 2 входных списков 

function append<T>(xs:List<T>, ys:List<T>):List decreases  xs

{
  //Match input1 if it is Nil i.e. end of list/no list then return the right remaning element or if it is of format Cons(element1,remaining list) then return
  //Cons(element1,recursively call append with remaining list and one first element)
  //So whilst reaching last Nil element, we will get appended list of all the elements.
    match(xs) 
        case Nil => ys
        case Cons(element1, rem_list) =>  Cons(element1, append(rem_list, ys))
}

// Функция ниже принимает 1 список и 1 элемент в качестве входных и возвращает логическое значение True или False в зависимости от того, находится ли элемент в списке или нет 

function listContains<T>(xs:List<T>, element:T):bool
 decreases  xs
{
  //Match List1: If input parameter 1 is a list of format Cons(z,zs), and if z i.e. first element of list == input parameter 2 then return True
  //Else Continue recursively calling same function until the element condition is met or the list is exhausted. Then return True
    match(xs)
        case Cons(element1, rem_list) => element1==element || listContains(rem_list, element) 
        case Nil => false
}

// Функция ниже принимает 1 дерево и 1 элемент в качестве входных данных и возвращает логическое значение True или False в зависимости от того, находится ли элемент в дереве или нет 

function treeContains<T>(tree:Tree<T>, element:T):bool decreases  tree

{
  //Match Tree1: If input parameter 1 is a Leaf,return false implying the element is not present in the Tree
  // If it is a node then reduce node into 2 trees and keep checking each of the sub-trees contains the node
  //Continue recursively calling same function until Node is same as element or the Tree is exhausted. Then return True
    match(tree)
    case Leaf() => false
    case Node(tree1, tree2, CurrentNode) => treeContains(tree1, element) || treeContains(tree2, element)
}

// Функция ниже принимает 1 дерево в качестве входных данных и возвращает список, который получается путем добавления каждого узла как элемент списка 

function flatten<T>(tree:Tree<T>):List <T>
{
  //Match If the input is a LEaf return Nil or keep on returning and appending CurrentNode with the result of recursively callling faltten function.
  //Hence this will in turn result the complete list which constitutes each node as an element.
    match(tree)
    case Leaf() =>  Nil
    case Node(tree1, tree2, CurrentNode) => Cons(CurrentNode,append(flatten(tree1),flatten(tree2)))

}

ghost method sameElements<T>(tree:Tree<T>, element:T)
{
    match(tree)
    case Leaf() =>
    //If the Tree is a simple element the proof might not be needed
    //However if we have trees then we check the result of treecontains and listcontains function if that is true it prooves the thesis.
    case Node(tree11,tree2,CurrentNode) =>
    calc {
       treeContains(tree, element)
        == 
      listContains(flatten(tree),element);
    }
}
...