algebraic-dev

import Std.Data.HashMap

namespace LZ

/--
Encoder state for compression
-/
structure EncodeState where
  /--
  Dictionary mapping known sequences to their unique IDs for encoding

algebraic-dev

import Std.Internal.UV
import Lean
import Lean.Attributes

open Std.Internal.UV
open Lean Elab Term

-- Based on: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Introducing.20the.20nest/near/387447219

structure CallStack where

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>,
    },