algebraic-dev

import Std.Internal.Async
import Std.Internal.UV
import Std.Net.Addr

open Std.Internal.IO.Async.TCP.Socket
open Std.Internal.IO.Async.TCP
open Std.Internal.IO.Async
open Std.Net

-- All of these function are used to create the Monads.

algebraic-dev

@[inline]
def emptyTask : Task (Except IO.Error Unit) :=
  Task.pure (Except.pure ())

@[inline]
def block (io : Task α) : IO α :=
  pure io.get

@[inline]
def nextTask {α} (t : Task α) (f : α → BaseIO Unit) : BaseIO Unit :=

algebraic-dev

import Std.Internal.Async
import Std.Internal.UV
import Std.Net.Addr

open Std.Internal.IO.Async.TCP.Socket
open Std.Internal.IO.Async.TCP
open Std.Internal.IO.Async
open Std.Net

-- The monad to make the code simpler to read.

algebraic-dev

use std::{iter::Peekable, str::Chars};

struct Parser<'a> {
    chars: Peekable<Chars<'a>>,
    input: &'a str,
    index: usize,
}

#[derive(Debug, Clone)]
pub enum Expr {

algebraic-dev

/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Runtime
import Lean.Compiler.NameMangling
import Lean.Compiler.ExportAttr
import Lean.Compiler.InitAttr

algebraic-dev

• YALE (1998): Paper / Impl
  • Type: Text
  • Language: ??
  • Description:
• AMINE / MPINE (2000) Paper / Impl
  • Type: Text
  • Language: ??
  • Description: "In this evaluator, each variable in the calculus is represented as a node that has the same name as the variable, and the substitution operation for a variable requires a search to find the node which corresponds to the variables. To prevent searching those nodes deeply, annotated terms, that have name lists of terms as annotations, are introduced; however, processing these annotations consume a considerable amount of time during execution. MPINE was also proposed as a concurrent." (Design and implementation of a low-level language for interaction nets - Shinya Sato) computation version of AMINE.
• in² (2002): Paper / Impl

algebraic-dev

// An address is just a pointer to some agent inside the interaction net.
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct Address(usize);

/// A slot is part of an agent that can connect to other ports.
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct Slot(usize);

impl Slot {
    /// The main port is always zero

algebraic-dev

use std::{collections::HashSet, fmt::Display, rc::Rc};

/// The AST. This thing describes
/// the syntatic tree of the program.
#[derive(Debug)]
pub enum Syntax {
    Lambda {
        param: String,
        body: Rc<Syntax>,
    },

algebraic-dev

Mudanças e ideias para o Kind2

Algumas mudanças bem importantes na linguagem vão ocorrer pelos próximos dias e que vão influenciar bastante o modo que programamos Kind2. Primeiro eu gostaria de introduzir as ideias que a linguagem tenta usar e, após isso, os problemas que pensei que não vão deixar a linguagem ir tanto para frente quanto eu queria.

Ideais

A unidade de modularização da linguagem seriam as funções já que tudo em Kind é primordialmente uma função ou um construtor (você pode considerar os 2 a mesma coisa já que um construtor é uma função que não reduz) e isso molda varios aspectos da linguagem como:

algebraic-dev

module Pipes 

import Control.Monad.Trans
import Data.IORef

-- It's just https://github.com/QuentinDuval/IdrisPipes with one small change.

||| PipeT is a composable data type to describe streams of data that 
||| can be generated and can flow upstream and downstream just like 
||| javascript generators