cheery

module Regex2 where

open import Function
open import Data.Bool
open import Data.Maybe
open import Data.Product
open import Data.Sum
open import Data.List as List
open import Data.Empty
open import Data.Unit

cheery

module FinMap where

open import Agda.Builtin.Equality
open import Relation.Binary.PropositionalEquality using (refl; cong; trans; subst; sym)
open import Data.Nat as ℕ using (ℕ; _<_; _≤_; suc; s≤s; z≤n)
open import Data.Nat.Properties using (≤-refl; +-comm; +-identityˡ; +-identityʳ; +-suc; 1+n≢0)
open import Data.Fin hiding (compare; _<_; _≤_)
open import Data.List
open import Data.Product
open import Data.Sum

cheery

module parsergen4 where

-- for troubleshooting, not a complete parser generator/parsing engine.

open import Agda.Builtin.Equality
open import Relation.Nullary using (Dec)
open import Data.Nat
open import Data.Fin hiding (_<_)
open import Data.Fin.Properties using (suc-injective)
open import Data.Vec hiding (_>>=_)

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