Skyb0rg007

<#PSScriptInfo

.VERSION 1.0

.GUID dadcf7db-a1ab-4360-b66b-25d5e7a1666a

.AUTHOR skyler.soss@gmail.com

.COPYRIGHT Skye Soss 2024

Skyb0rg007

CREATE top3  3 CELLS ALLOT  top3 3 CELLS 0 FILL
0 VALUE file
12 CONSTANT max-line
CREATE line-buffer  max-line ALLOT

: init-file ( -- ) S" day1.txt" R/O OPEN-FILE THROW TO file ;

: free-file ( -- ) file CLOSE-FILE THROW  0 TO file ;

: step ( -- u f ) line-buffer max-line 2 - file READ-LINE THROW ;

Skyb0rg007

#!/usr/bin/env stack
-- stack script --resolver lts-19.30
{-# LANGUAGE GADTs, ViewPatterns, ScopedTypeVariables, InstanceSigs, MultiParamTypeClasses, DeriveFunctor, StandaloneDeriving, UnicodeSyntax, ImportQualifiedPost #-}

import Control.Applicative (liftA2)
import Control.Monad (join)
import Data.Proxy (Proxy (Proxy))

--

Skyb0rg007

local
   structure Cont = SMLofNJ.Cont
   structure IntervalTimer = SMLofNJ.IntervalTimer
   structure S = Signals
in
   (* `withTimeout t f` calls `f ()` and returns `SOME x` where `x` is the result of the function call.
    * If `f ()` takes longer than `t` to execute, `withTimeout` instead returns `NONE` *)
   fun withTimeout t f =
      let
         val result = ref NONE

Skyb0rg007

#!/usr/bin/env stack
-- stack script --resolver lts-18.18

module Main (main) where

import Control.Applicative    (liftA2)
import Control.Comonad        (extract)
import Control.Comonad.Cofree (Cofree ((:<)))
import Control.Monad          (forM_)
import Control.Monad.ST       (runST)

Skyb0rg007

From Coq Require Import Program.Basics.

Reserved Notation "¬ A" (at level 75, right associativity).

Notation "⊥" := Empty_set.
Notation "¬ A" := (A -> ⊥).

Axiom callcc : forall {A B : Type}, ((A -> B) -> A) -> A.

Definition LEM {P : Type} : P + ¬P :=

Skyb0rg007

Require Import Coq.Program.Basics.
Open Scope program_scope.

(* transportᵖ(p, -) : P(x) → P(y) *)
Definition transport {A : Type} {x y : A} (P : A -> Type) (p : x = y) : P x -> P y :=
  fun (px : P x) => eq_rect x P px y p.

(* (f ~ g) := Π(x:A) f(x) = g(x) *)
Definition homotopy {A : Type} {P : A -> Type} (f g : forall (x : A), P x) : Type :=
  forall (x : A), f x = g x.

Skyb0rg007

(import (scheme base)
        (only (scheme write) display)
        (only (srfi 18) make-thread thread-start! thread-join!))

;; Helpers
(define-syntax for
  (syntax-rules ()
    ((_ (i start end) body ...)
     (do ((i start (+ i 1)))

Skyb0rg007

{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE StandaloneDeriving    #-}

Skyb0rg007

sat :  'a producer * 'a producer -> 'a producer
(p1 <|> p2) ts == case p1 ts
                    of SOME x => SOME x
                     | NONE => p2 ts

sat : ('a -> bool) -> 'a producer -> 'a producer
sat predicate p ts = case p ts
                       of result as SOME (ERROR _, _) => result
                        | SOME x => if predicate x then SOME x else NONE