cheery

module Main where

import Prelude

import Effect (Effect)
import Data.Foldable (fold)
import TryPureScript (h1, h2, p, text, list, indent, link, render, code)
import Unsafe.Coerce (unsafeCoerce)
import Prim.RowList
import Prim.Row

cheery

{-# LANGUAGE TypeFamilies, DataKinds, GADTs #-}
module TypeFam where

data JsValue = VArray [JsValue] | VNum Double | VString String deriving (Show)

data JsTypeMap
    = AsDouble
    | AsList JsTypeMap
    | AsString
    deriving (Show)

cheery

module ICat2

%default total

data Ft       -- functors
  = Var Nat
  | Terminal
  | Prod Ft Ft
  | Exp Ft Ft

cheery

{-# LANGUAGE FlexibleInstances #-}
module LC where

import Control.Monad.Cont
import Control.Monad (guard)
import Control.Concurrent
import Data.Bifunctor (bimap)

-- Interface to retrieve a boolean and then produce a boolean.
interface1 :: FT

cheery

module Linc where

import Data.STRef
import Control.Monad.ST
import Control.Monad ((>=>))

data Structure = Structure
    { term       :: Tm Int Int
    , link_count :: Int
    , opt_count  :: Int

cheery

module INet where

import Data.STRef
import Control.Monad.ST

-- This kind of implementation of optimal reduction 
-- accumulates control nodes (Croissants and brackets)
--
-- I'd guess the reason for that is that it's lacking essential structure.
-- Adding a "box" around the exponential solves the problem, but also removes the optimality.

cheery

module GS2 where

import Data.STRef
import Control.Monad.ST
import qualified Data.Map as Map
import Data.Map (Map)

-- Terms to normalise
type Arity = (Int, Int, Int)
data Tm

cheery

-- Haven't tested this, may contain trivial bugs.
module GS2 where

import Control.Concurrent
import Control.Concurrent.MVar
-- import qualified Data.Map as Map
-- import Data.Map (Map)

data Ty
    = Initial

cheery

-- Haven't tested this, may contain trivial bugs.
module GS2 where

import Control.Concurrent
import Control.Concurrent.MVar
-- import qualified Data.Map as Map
-- import Data.Map (Map)

data Ty
    = Initial

cheery

/* There may be mistakes here.
   This program implements "optimal reduction" in CHR,
   it runs in CHR.js playground.
   
   The N in front of each structure is a label.
   Rest of the numbers are edges between combinators.
   fresh(N) tracks fresh numbers to produce new edges.
 */

eq(X,Y), eq(Y,Z) <=> eq(X,Z)