noughtmare

open import Data.Fin as Fin using (Fin ; #_ ; _≟_)
open import Data.Fin.Properties using (suc-injective)
open import Level as Level using (Level)
open import Data.Unit using (⊤ ; tt)
open import Data.Empty
open import Data.Product as Product
open import Data.Product.Properties as Product using (,-injective ; ≡-dec)
open import Data.Sum
open import Relation.Binary.PropositionalEquality
open import Data.Nat using (ℕ ; _+_)

noughtmare

newtype SNat = SNat { unSNat :: forall x. (SNat -> x) -> x -> x }
newtype CNat = CNat { unCNat :: forall x. (x -> x) -> x -> x }
newtype Quad a b c d = Quad { unQuad :: forall x. (a -> b -> c -> d -> x) -> x }
newtype BNat = BNat { unBNat :: forall x. (BNat -> x) -> (BNat -> x) -> x -> x}

instance (Show a, Show b, Show c, Show d) => Show (Quad a b c d) where
  show q = unQuad q (\a b c d -> show (a,b,c,d))
instance Show CNat where
  show cn = show (unCNat cn (+ 1) 0)
instance Show SNat where

noughtmare

newtype SNat = SNat { unSNat :: forall x. (SNat -> x) -> x -> x }
newtype CNat = CNat { unCNat :: forall x. (x -> x) -> x -> x }
newtype Quad a b c d = Quad { unQuad :: forall x. (a -> b -> c -> d -> x) -> x }
newtype BNat = BNat { unBNat :: forall x. (BNat -> x) -> (BNat -> x) -> x -> x}

test =
  let
    ssuc = \x -> SNat (\s _ -> s x)
    s0 = SNat (\_ z -> z)
    s2 = ssuc (ssuc s0)

noughtmare

import qualified Language.Haskell.TH.Syntax as TH

data ULC = Var String | Lam String ULC | App ULC ULC deriving (Show, TH.Lift)

quote :: TH.Exp -> Maybe ULC
quote (TH.VarE v) = Just $ Var (TH.nameBase v)
quote (TH.UnboundVarE v) = Just $ Var (TH.nameBase v)
quote (TH.AppE x y) = App <$> quote x <*> quote y
quote (TH.LamE vs x) = foldr (\v xs -> Lam <$> (case v of TH.VarP v' -> Just (TH.nameBase v'); _ -> Nothing) <*> xs) (quote x) vs
quote _ = Nothing

noughtmare

{-# LANGUAGE PatternSynonyms, ViewPatterns #-}
{-# OPTIONS_GHC -Wall #-}
import Data.List
import Data.Ord

isPalindrome :: Eq a => [a] -> Bool
isPalindrome xs = xs == reverse xs

lps, lps' :: Eq a => [a] -> [a]
lps = maximumBy (comparing length) . filter isPalindrome . subsequences

noughtmare

{- cabal:
build-depends: base, recover-rtti, tasty-bench, tasty-bench-fit
-}
{-# LANGUAGE GHC2021, GADTs, DataKinds, LambdaCase, TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}

-- DATA-DEPENDENT PARSING WITH VARIABLES

import Prelude hiding (Monad (..))
import Data.Char (intToDigit)

noughtmare

{-# LANGUAGE GHC2021, GADTs, DataKinds #-}

import Control.Monad (ap, (>=>), replicateM_, guard)
import Control.Applicative
import Prelude hiding (or)
import Data.Kind
import Data.Char

asumMap :: Alternative f => (a -> f b) -> [a] -> f b
asumMap f x = asum (map f x)

noughtmare

{-# LANGUAGE GHC2021, GADTs, DataKinds #-}

import Control.Monad (ap, (>=>))
import Control.Applicative
import Prelude hiding (or)
import Data.Kind
import Data.Char

type Ctx :: Type
type Ctx = [Type]

noughtmare

{- cabal:
build-depends: base, liquidhaskell == 0.9.6.*
-}
{- project:
allow-newer: bytestring
-}
{-# LANGUAGE GHC2021 #-}
{-# OPTIONS_GHC -Wall -fplugin=LiquidHaskell #-}

-- Liquid Haskell checks termination for us, but you can disable it if you want.

noughtmare

{-# OPTIONS --guarded --rewriting --cubical -WnoUnsupportedIndexedMatch #-}

module 1-Parser where

open import 2-Guarded

open import Data.Product hiding (_<*>_)
open import Data.Char hiding (_≤_)
open import Data.Bool hiding (_≤_)
open import Function