Dias da semana

A declaração a seguir diz para o Kind que estamos declarando um novo conjunto de dados - um Tipo.

type Dia { // Dia é um Tipo
  segunda  // Segunda é um Dia
  terca    // Terça   é um Dia
  quarta   // Quarta  é um Dia
  quinta   // Quinta  é um Dia
  sexta    // Sexta   é um Dia
  sabado   // Sábado  é um Dia
  domingo  // Domingo é um Dia
  }

O tipo se chama Dia, e seus membros são Segunda, Terça, Quarta, etc. A definição <nome> : <tipo> pode ser lida como: "nome é um tipo". Acima temos tanto um exemplo de criar um tipo novo Dia : Type, quanto a de declarar um elemento de um tipo existente Quarta : Dia.

Agora que temos definido o que é um Dia, podemos escrever funções que operam usando esse tipo. Digite o seguinte:

ProximoDiaUtil (d: Dia) : Dia

Isso declara que temos uma função chamado ProximoDiaUtil, que recebe um argumento chamado d, do tipo Dia, e retorna um Dia. Continue a definição da função da seguinte forma:

ProximoDiaUtil Dia.segunda  = ?
ProximoDiaUtil Dia.terca    = ?
ProximoDiaUtil Dia.quarta   = ?
ProximoDiaUtil Dia.quinta   = ?
ProximoDiaUtil Dia.sexta    = ?
ProximoDiaUtil Dia.sabado   = ?
ProximoDiaUtil Dia.domingo  = ?

O que estamos fazendo aqui é o que chamamos de pattern matching. Estamos declarando como a função deve rodar para cada possibilidade da entrada d. Nem sempre será necessário fazer isso, como será mostrado em exemplos mais a frente.

Por fim, complete as funções escrevendo o que cada uma deve retornar, e use espaços para estilizar como preferir:

ProximoDiaUtil Dia.segunda = Dia.terca
ProximoDiaUtil Dia.terca   = Dia.quarta
ProximoDiaUtil Dia.quarta  = Dia.quinta
ProximoDiaUtil Dia.quinta  = Dia.sexta
ProximoDiaUtil Dia.sexta   = Dia.segunda
ProximoDiaUtil Dia.sabado  = Dia.segunda
ProximoDiaUtil Dia.domingo = Dia.segunda

Com a função finalizada, nós podemos checar o funcionamento dela com alguns exemplos. O jeito principal de fazer isso em Kind é criar uma função Main no seu arquivo, e rodando ele com o comando kind2 run <file>.

Por exemplo, se você escrever a seguinte Main e rodar o arquivo

Main {
  // Dois dias úteis depois do sábado
  ProximoDiaUtil (ProximoDiaUtil Sabado)
}

Deve ser retornado pra você algo como:

(Dia.terca)

Outro jeito de testar seu código, é dizer o que esperamos que o código retorne, por meio de uma prova:

// O terceiro dia útil depois de uma segunda é uma quinta
TesteDiaUtil : Equal Dia (ProximoDiaUtil (ProximoDiaUtil (ProximoDiaUtil Dia.segunda))) Dia.quinta
TesteDiaUtil = Equal.refl

Os detalhes de como provas funcionam serão explicados mais a frente. No momento, o que precisa ser entendido disso é:

  • Tem-se a constatação de que (ProximoDiaUtil (ProximoDiaUtil (ProximoDiaUtil Dia.segunda))) é igual a Dia.quinta
  • Essa constatação foi nomeada TesteDiaUtil
  • TesteDiaUtil = Equal.refl diz que constatação pode ser provada usando apenas simplificação nos dois lados

Para testar que essa prova (e qualquer outra prova adiante) está correta, você precisa checar o arquivo, usando o comando kind2 check <file>, que deve te retornar algo como:

All terms check.