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

Skyb0rg007

.DEFAULT: dict-test

dict-test: dict-test.uo
	mosmlc -toplevel $^ -o $@

key-sig.ui key-sig.uo: key-sig.sml
	mosmlc -toplevel -c $^

dict-sig.ui dict-sig.uo: dict-sig.sml

Skyb0rg007

signature DICT =
sig
  type key
  type 'a dict
  exception NotFound of key
  val empty : 'a dict
  val find : key * 'a dict ->'a
  val bind : key * 'a * 'a dict -> 'a dict
end

Skyb0rg007

--[=[

Relevant functions for creating lenses
Note that not all functions are always implemented

For Lens s t a b:

over : (a -> b) -> s -> t
    Map a function over the target of the lens
    Ex. over(each..each, function(x) return x+1 end, {{1,2},{3,4}})

Skyb0rg007

# Latest resolver with ghc-8.4.3
resolver: lts-12.14

# Local packages
packages:
- .

extra-deps:
- Cabal-2.2.0.1
- MemoTrie-0.6.9

Skyb0rg007

    ring_buffer: 0x404180
    Got value 1!
    ==================
    WARNING: ThreadSanitizer: data race (pid=19155)
      Read of size 4 at 0x000000404184 by thread T2:
        #0 ring_dequeue /home/ssoss/Desktop/Amber/Amber/util/tests/minimal-ring-race.c:84 (minimal-race+0x4013c5)
        #1 consumer /home/ssoss/Desktop/Amber/Amber/util/tests/minimal-ring-race.c:122 (minimal-race+0x4014c5)
        #2 <null> <null> (libSDL2-2.0.so.0+0x6875f)
    
      Previous write of size 4 at 0x000000404184 by thread T1: