abailly

Keybase proof

I hereby claim:

• I am abailly on github.
• I am dr_c0d3 (https://keybase.io/dr_c0d3) on keybase.
• I have a public key ASD86WDkjx0YyL2R82hHkE2LJzHfpWcJDjCD7oYVnt33Xgo

To claim this, I am signing this object:

abailly

||| A proof of the validity of matching algorithm for
||| regular expressions
|||
||| From https://arxiv.org/abs/2003.06458
module re

import Decidable.Equality

%default total

abailly

module Substitution where

import Data.Maybe
import Data.List(findIndex)

newtype Message = Msg { unMsg :: [Int] }
  deriving (Eq, Show)

type SubstitutionTable = Int -> Int

abailly

module Subway where

import Control.Arrow((>>>))

import Data.List(sort)

data Subway = Sub [Subway]
  deriving (Show, Eq, Ord)

fromString' :: [Subway] -> String -> Subway

abailly

{-# LANGUAGE DeriveFunctor #-}
module Main where

import Data.List(group, sort)

data Tree a = E | N a (Tree a) (Tree a)
  deriving (Eq, Ord, Show, Functor)

insert :: (Ord a) => [a] -> Tree a
insert list = insert' list E

abailly

package org.jparsec.examples.dsl;

import org.jparsec.Parser;
import org.jparsec.Parsers;
import org.jparsec.Scanners;
import org.jparsec.Terminals;

import java.util.Arrays;

public class DSL {

abailly

||| A proof of the validity of matching algorithm for
||| regular expressions
|||
||| From https://arxiv.org/abs/2003.06458
module re

%default total

infix 7 .|
infix 6 ..

abailly

{-# LANGUAGE DeriveDataTypeable, DeriveGeneric, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, PolyKinds,
             ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-}
module Gorilla.Auth.Roles where

import           Control.Monad.Trans                        (liftIO)
import           Control.Monad.Trans.Except                 (runExceptT)
import           Data.Proxy                                 (Proxy (Proxy))
import           Data.Typeable                              (Typeable)
import           GHC.Generics                               (Generic)
import           Network.Wai                                (Request)

abailly

||| From Slack ADL: https://artisans-du-logiciel.slack.com/files/UA67NMTA6/FH0UVDUAX/tarif_parking.jpg
||| Goal is to "embed" the business rules for computing parking durations inside Idris,
||| computing a pricing expression as the type of a given duration

module Parking


import Data.List

mutual

abailly

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}

{-|