text:
import Aoc
import Data.List
import Data.Nat
import Data.Strings
import Data.SortedSet as S
%default total
-- TODO: this broke when I upgraded from 0.2.1 to 0.2.1-0a685f8d2... merry christmas

data Instruction
  = Nop Integer
  | Acc Integer
  | Jmp Integer

Program : Type
Program = List Instruction

parseInstruction : String -> Maybe Instruction
parseInstruction s =
  case words s of
    -- thankfully parseInteger has no problem with "+3"
    ["nop", n] => Nop <$> parseInteger n
    ["acc", n] => Acc <$> parseInteger n
    ["jmp", n] => Jmp <$> parseInteger n
    _ => Nothing

data Outcome = InfiniteLoop Integer | Terminated Integer
Show Outcome where
  show (InfiniteLoop acc) = "acc = " ++ show acc ++ " before infinite loop"
  show (Terminated acc) = "terminated with acc = " ++ show acc

-- This one's partial because... you know... (gestures)
partial
runFrom : (pc : Nat) -> (acc : Integer) -> (visited : SortedSet Nat) -> Program -> Outcome
runFrom pc acc visited program =
  if S.contains pc visited then InfiniteLoop acc else
    let visited' = S.insert pc visited in
    case maybeIndex pc program of
      Just (Nop _) => runFrom (pc+1) acc visited' program
      Just (Acc n) => runFrom (pc+1) (acc+n) visited' program
      Just (Jmp n) => runFrom (pc+integerToNat n) acc visited' program
      Nothing      => Terminated acc

partial
run : Program -> Outcome
run program = runFrom 0 0 S.empty program

||| Given an "edit" function that maybe applies to one element of the list,
||| try to apply it at every position in the list.
||| e.g.  halve n = if mod n 2 == 0 then Just (div n 2) else Nothing
|||       tryEach halve [10..13] = [[5,11,12,13], [10,11,6,13]]
tryEach : (a -> Maybe a) -> List a -> List (List a)
tryEach f xs = go f xs [] where
  go : (a -> Maybe a) -> List a -> List a -> List (List a)
  go f [] _ = []
  go f (x::xs) pre =
    case f x of
      Just y  => reverseOnto (y::xs) pre :: go f xs (x::pre)
      Nothing =>                            go f xs (x::pre)

||| Change nops into jmps and vice versa.
edit : Instruction -> Maybe Instruction
edit (Nop n) = Just $ Jmp n
edit (Jmp n) = Just $ Nop n
edit _ = Nothing

||| Extract Just a terminated accumulator from an outcome, else Nothing.
justTerminated : Outcome -> Maybe Integer
justTerminated (Terminated acc) = Just acc
justTerminated _ = Nothing

partial
main : IO ()
main = do
  program <- parseLines parseInstruction
  printLn $ length program
  putStr "*   "
  printLn $ run program
  putStr "**  "
  printLn $ mapMaybe (justTerminated . run) (tryEach edit program)


text:
module Parsing

import public Text.Lexer

%default total

public export
data Token = Ident String
           | Literal Integer
           | StrLit String
           | CharLit String
           | DoubleLit Double
           | Symbol String
           | Keyword String
           | Unrecognised String
           | Comment String
           | EndInput

comment : Lexer
comment = exact "--" <+> many (isNot '\n')

rawTokens : TokenMap Token
rawTokens = [(comment, Comment)]

doParse : String-> Either String $ List (TokenData Token)
doParse str =case lex rawTokens str of
  (a, (_,_,""))=> Right a
  (_,(_,_,e)) => Left $ "error!   " ++ e

main : IO ()
main = do
  pure ()

ext: idr

max_stars_repo_name: idris-industry/paradise

max_issues_repo_name: idris-industry/paradise

max_forks_repo_name: idris-industry/paradise


text:
import Data.Fin
import Data.Vect

tail : (Fin (S n) -> a) -> (Fin n -> a)
tail f = f . FS

toVectFun : {n : Nat} -> (Fin n -> a) -> Vect n a
toVectFun {n =   Z} _ = Nil
toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))

N : Nat
N = 500

xs : Vect (S N) Nat
xs = toVectFun {n = S N} finToNat

main : IO ()
main = putStrLn $
  "xs(" ++ show N ++ ") = " ++ show (index (fromInteger (natToInteger N)) xs)


text:
module Commons.Text.Parser.Run

import Commons.Data.Location

import Text.Parser

import Text.Lexer
import Commons.Text.Lexer.Run

%default total
%access export

public export
record ParseFailure a where
  constructor MkParseFail
  error : String
  location : Maybe Location
  rest : List a

public export
data ParseError a = PError (ParseFailure a)
                  | LError LexError
                  | FError FileError

export
convError : Core.ParseError (TokenData a)
         -> Maybe String
         -> Run.ParseError a
convError (Error msg Nil) _ = PError (MkParseFail msg Nothing Nil)
convError (Error msg (r::rs)) mn = PError $
    MkParseFail msg (Just $ MkLoc mn (toNat (TokenData.line r))
                                     (toNat (TokenData.col r)))
                    (map tok (r::rs))

export
parseString : Lexer a
           -> Grammar (TokenData a) e ty
           -> (str : String)
           -> (Either (Run.ParseError a) ty)
parseString lexer rule str =
  case lexString lexer str of
    Left err   => Left (LError err)
    Right toks =>
      case parse rule toks of
        Left err      => Left (convError err Nothing)
        Right (val,_) => Right val

export
parseFile : Lexer a
         -> Grammar (TokenData a) e ty
         -> (fname : String)
         -> IO $ Either (Run.ParseError a) ty
parseFile lexer grammar fname =
  case !(lexFile lexer fname) of
    Left (LError err) => pure (Left (LError err))
    Left (LIOErr err) => pure (Left (FError err))
    Right toks =>
      case parse grammar toks of
        Left err      => pure (Left (convError err (Just fname)))
        Right (val,_) => pure (Right val)

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Parser

import Data.Fuel

%default total

public export
data Parser : Type -> Type -> Type where
   Continuation : (i -> Parser i o) -> Parser i o
   Finished : Maybe o -> Parser i o

export
runParser : Monad m => Fuel -> m i -> (Parser i o) -> m (Maybe o)
runParser Dry _ _ = pure Nothing
runParser _ _ (Finished result) = pure result
runParser (More rest) input (Continuation parser) = do
  c <- input
  runParser rest input (parser c)

max_stars_repo_name: PeterHajdu/peti

max_issues_repo_name: PeterHajdu/peti

max_forks_repo_name: PeterHajdu/peti


text:
module Control.Algebra.ZZDivisors

import Control.Algebra
import Classes.Verified
import Control.Algebra.VectorSpace -- definition of module

import Data.Matrix
import Data.Matrix.Algebraic -- module instances; from Idris 0.9.20
import Data.Matrix.AlgebraicVerified

import Data.Vect.Structural
import Data.Matrix.Structural

import Data.ZZ
import Control.Algebra.NumericInstances
import Control.Algebra.ZZVerifiedInstances
import Data.Matrix.ZZVerified

import Data.Matrix.ZZModuleSpan
import Data.Matrix.LinearCombinations

%default total

{-
Trivial lemmas and plumbing
-}

bileibniz : (f : a -> b -> c) -> (x1=x2) -> (y1=y2) -> f x1 y1 = f x2 y2
bileibniz f {x1} {x2} {y1} {y2} xeq yeq = rewrite (cong {f=f} xeq) in cong {f=f x2} yeq

{-
A divisibility relation
-}

-- Should be modified to account for (gcd x 0 = 0).
quotientOverZZ : ZZ -> ZZ -> Type
quotientOverZZ x y = ( d : ZZ ** d<.>y=x )

quotientOverZZrefl : x `quotientOverZZ` x
quotientOverZZrefl {x} = ( unity ** ringWithUnityIsUnityR x )

quotientOverZZtrans : x `quotientOverZZ` y -> y `quotientOverZZ` z -> x `quotientOverZZ` z
quotientOverZZtrans (dx ** prx) (dy ** pry) {x} {y} {z} = ( dx<.>dy ** trans (sym $ ringOpIsAssociative dx dy z) $ trans (cong pry) prx )

quotientOverZZreflFromEq : (a=b) -> a `quotientOverZZ` b
quotientOverZZreflFromEq {a} {b} eq with (quotientOverZZrefl {x=b})
	| (d ** pr) = (d ** trans pr $ sym eq)

{-
Interactions between integer divisibility and linear combinations
-}

||| Examples:
|||
||| > divisorByDistrib (Pos 4) ((Pos 8)::(Pos 0)::[]) (\x => case x of { FZ => (Pos 2 ** Refl); (FS FZ) => (Pos 0 ** Refl) })
|||
||| (Pos 2 ** ?divisorByDistrib_pr) : (d : ZZ ** multZ d (Pos 4) = Pos 8)
|||
||| > divisorByDistrib (Pos 4) ((Pos 8)::(Pos 4)::[]) (\x => case x of { FZ => (Pos 2 ** Refl); (FS FZ) => (Pos 1 ** Refl) })
|||
||| (Pos 3 ** ?divisorByDistrib_pr) : (d : ZZ ** multZ d (Pos 4) = Pos 12)
|||
||| > divisorByDistrib (Pos 4) ((Pos 8)::(Pos 1)::[]) (\x => case x of { FZ => (Pos 2 ** Refl); (FS FZ) => (Pos 0 ** Refl) })
|||
||| ... Type mismatch between 0 and 1
divisorByDistrib : (z : ZZ)
	-> (x : Vect n ZZ)
	-> ( (k : _) -> index k x `quotientOverZZ` z )
	-> (LinearCombinations.monoidsum x) `quotientOverZZ` z
divisorByDistrib z [] fn = (0 ** ringNeutralIsMultZeroL z)
{-
-- Doesn't like the (fn . FS) passed to divisorByDistrib in the recursive step.
divisorByDistrib z (xx::xxs) fn with ( divisorByDistrib z xxs (fn . FS) )
	| (dxxs ** prxxs) with (fn FZ)
		| (dxx ** prxx) = (dxx<+>dxxs ** ?divisorByDistrib_pr)
	-- divisorByDistrib_pr {z} {xx} {xxs} {fn} {dxx} {dxxs} =
	-- 	(dxx<+>dxxs)<.>z	={ ringOpIsDistributiveR dxx dxxs z }=
	-- 	(dxx<.>z)<+>(dxxs<.>z)	={ cong {f=((dxx<.>z)<+>)} prxxs }=
	-- 	(dxx<.>z)<+>sum xxs	={ cong {f=(<+>_)} prxx }=
	-- 	xx<+>sum xxs	={ rewrite sym $ monoidrec1D {v=xx} {vs=xxs} }=
	-- 	sum (x::xxs)	QED
-}
divisorByDistrib z (xx::xxs) {n=S predn} fn = ( dxx<+>dxxs ** divisorByDistrib' )
	where
		dxx : ZZ
		dxx = getWitness $ fn FZ
		prxx : dxx<.>z = xx
		prxx = getProof $ fn FZ
		dxxs : ZZ
		-- Passing (fn . FS) as an arg during proof reqs implicit arg (n).
		{-
		In REPL: "No such variable __pi_arg7"
		Otherwise:
		"Type mismatch between
			(k1 : Fin (S k)) ->
			quotientOverZZ (index k1 (xx :: xxs)) z (Type of fn)
		and
			Fin (S k) ->
			(\k1 =>
				quotientOverZZ (index k1 xxs) z) (__pi_arg7) (Expected type)

		Specifically:
			Type mismatch between
				index v1 (xx :: xxs)
			and
				index (__pi_arg7) xxs
		"

		> dxxs = getWitness $ divisorByDistrib z xxs (fn . FS)
		-}
		dxxs = getWitness $ divisorByDistrib z xxs (\i => fn (FS i))
		prxxs : dxxs<.>z = LinearCombinations.monoidsum xxs
		-- prxxs = getProof $ divisorByDistrib z xxs (fn . FS)
		prxxs = getProof $ divisorByDistrib z xxs (\i => fn (FS i))
		{-
		If you only write the following (note the missing (<.>_) from (_<.>_ = _))

		> divisorByDistrib' : (dxx<+>dxxs) = LinearCombinations.monoidsum (xx::xxs)

		then you get a type mismatch error that looks like

		"type mismatch between _ and _, specifically between

			foldrImpl (flip plusZ) (Pos 0) (plusZ xx) xxs

		and

			foldrImpl (flip plusZ) (Pos 0) (plusZ xx) xxs
		"

		which is not at all what's wrong, and is an unhelpful error message.
		-}
		divisorByDistrib' : (dxx<+>dxxs)<.>z = LinearCombinations.monoidsum (xx::xxs)
		divisorByDistrib' = trans (ringOpIsDistributiveR dxx dxxs z) $ trans (bileibniz (<+>) prxx prxxs) $ sym $ monoidrec1D {v=xx} {vs=xxs}

{-
We need to modify this formula to make the right-hand-argument of (quotientOverZZ) constant. It should perhaps be saying the (quotientOverZZ)'s right-hand-arg lies in the transpose of xs in a constant position.
-}
zipWithHeadsQuotientRelation : {zs : Vect (S predn) ZZ} -> {xs : Matrix (S predn) (S predm) ZZ} -> (k : _ ) -> ( index k $ map head $ zipWith (<#>) zs xs ) `quotientOverZZ` (head $ index k xs)
zipWithHeadsQuotientRelation {zs=z::zs} {xs=(xx::xxs)::xs} FZ = (z ** Refl)
zipWithHeadsQuotientRelation {zs=z::zs} {xs=(xx::xxs)::xs} {predn=Z} (FS prelk) = FinZElim prelk
zipWithHeadsQuotientRelation {zs=z::zs} {xs=x::xs} {predn=S prededn} (FS prelk) = zipWithHeadsQuotientRelation {zs=zs} {xs=xs} {predn=prededn} prelk

-- Should be applied to (fn) as given by the gcd equality.
zipWithHeadsQuotientRelation2 : {zs : Vect (S predn) ZZ} -> {xs : Matrix (S predn) (S predm) ZZ} -> ( fn : ( i : Fin _ ) -> (head $ Vect.index i xs) `quotientOverZZ` (head $ Vect.head xs) ) -> (k : _ ) -> ( Vect.index k $ map head $ Vect.zipWith (<#>) zs xs ) `quotientOverZZ` (head $ Vect.head xs)
zipWithHeadsQuotientRelation2 {zs} {xs} fn k = quotientOverZZtrans (zipWithHeadsQuotientRelation {zs=zs} {xs=xs} k) (fn k)

linearComboQuotientRelation : (x : Vect (S predm) ZZ) -> (xs : Matrix predn (S predm) ZZ) -> (z : Vect (S predn) ZZ)
	-> ( fn : ( i : Fin _ ) -> (head $ Vect.index i (x::xs)) `quotientOverZZ` (head x) )
	-> ( LinearCombinations.monoidsum $
			map head $
			zipWith (<#>) z (x::xs) )
		`quotientOverZZ` (head x)
linearComboQuotientRelation x xs z fn = divisorByDistrib _ _ (zipWithHeadsQuotientRelation2 {zs=z} {xs=x::xs} fn)

-- Motivation: succImplWknStep_Qfunclemma
linearComboQuotientRelation_corrollary : (x : Vect (S predm) ZZ) -> (xs : Matrix predn (S predm) ZZ) -> (z : Vect (S predn) ZZ)
	-> ( fn : ( i : Fin _ ) -> (head $ Vect.index i (x::xs)) `quotientOverZZ` (head x) )
	-> ( head $
			LinearCombinations.monoidsum $
			zipWith (<#>) z (x::xs) )
		`quotientOverZZ` (head x)
linearComboQuotientRelation_corrollary x xs z fn = quotientOverZZtrans (quotientOverZZreflFromEq $ headOfSumIsSumOfHeads _) $ linearComboQuotientRelation x xs z fn


text:
module Main
import Data.List
main : IO ()
main = putStrLn "Hello world"

lst1 :  List String
lst1 = ["as", "the"]

lst2 : List String
lst2 = ["as", "them", "the", "here"]

--lst3 : List String
--lst3 = lst1 \\ lst2

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Main

rep : (n : Nat) -> a -> List a
rep Z x = []
rep (S k) x = x :: rep k x

data RLE : List Char -> Type where
     REnd  : RLE []
     RChar : (n : Nat) -> (c : Char) -> (rs : RLE xs) ->
             RLE (rep n c ++ xs)

------------

rle : (xs : List Char) -> RLE xs
rle [] = REnd
rle (x :: xs) with (rle xs)
  rle (x :: []) | REnd = RChar 1 x REnd
  rle (x :: (rep n c ++ ys)) | (RChar n c rs) with (decEq x c)
    rle (x :: (rep n x ++ ys)) | (RChar n x rs) | (Yes refl)
             = RChar (S n) x rs
    rle (x :: (rep n c ++ ys)) | (RChar n c rs) | (No f)
             = RChar 1 x (RChar n c rs)

compress : List Char -> String
compress xs with (rle xs)
  compress [] | REnd = ""
  compress (rep n c ++ ys) | (RChar n c rs)
         = show n ++ strCons c (compress ys)

compressString : String -> String
compressString xs = compress (unpack xs)

main : IO ()
main = putStrLn (compressString "foooobaaaarbaaaz")

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module Language.Elab.Deriving.Ord

-- Public: Things here we actually use in deriving Eq need to be re-exported to
-- be available at the deriving use-site. A little odd but that's how it is.
-- Otherwise you get extremely vague "Can't reify as X" errors and chances are
-- you don't have an FC to track it down.

import public Language.Elab.Syntax
import public Language.Elab.Types

import public Util
import public Language.Elab.Deriving.Util

import public Language.Reflection

import Language.Elab.Deriving.Eq

%language ElabReflection

addAutoImps : List String -> Name -> TTImp -> TTImp
addAutoImps xs na retty
  = foldr (\arg,tt => `(~(iVar na) ~(iBindVar arg) => ~(tt))) retty xs

addOrdAutoImps : List String -> TTImp -> TTImp
addOrdAutoImps xs retty
  = foldr (\arg,tt => `(Ord ~(iBindVar arg) => ~(tt))) retty xs

-- I want better names here, including better index names
-- e.g we have this now
{-
Language.Elab.Deriving.Eq.eqImplFoo6'Fun : Eq arg6281 => Eq arg6282
  => Eq arg6283 => Foo6' arg6281 arg6282 arg6283 arg6284
    -> Foo6' arg6281 arg6282 arg6283 arg6284 -> Bool
-}

||| e.g. compare : Foo a b -> Foo a b -> Ordering
compareClaim : (opname : Name) -> TypeInfo -> Visibility -> Elab Decl
compareClaim op tyinfo vis = do
  let conargs = pullExplicits tyinfo
      varnames = map (show . name) conargs
      params = map (extractNameStr . name) $ filter (not . isIndex) conargs
      tysig = `(~(tyinfo.type) -> ~(tyinfo.type) -> Ordering)
  logMsg "compareClaim" 1 $ ("auto params: ") ++ show params
  -- NB: I can't think of a reason not to Inline here
  pure $ iClaim MW vis [Inline] (mkTy op (addOrdAutoImps params tysig))

compareClause : (opname : Name)
             -> (Int, Constructor)
             -> (Int, Constructor) -> Elab Clause
compareClause op (i1,con1) (i2,con2) = do
    let vars1 = filter (isExplicitPi . piInfo) con1.args
    let vars2 = filter (isExplicitPi . piInfo) con2.args
    let pats1 = makePatNames vars1 infVars "_1"
    let pats2 = makePatNames vars2 infVars "_2"
    let lhs = iVar op `iApp` (makePat con1.name pats1) `iApp` (makePat con2.name pats2)
    let rhs = case compare i1 i2 of
                LT => `(LT)
                GT => `(GT)
                EQ => makeRhs (zip (catMaybes pats1) (catMaybes pats2))
    pure $ patClause lhs rhs
  where
    -- Make our pat names, we use Just to flag the vars we want to use, we don't
    -- compare indices since they're vacuously EQ for the Ord interface.
    -- It doesn't seem to matter if an index is M1 or not.
    makePatNames : List ArgInfo
               -> Stream String -> String -> List (Maybe Name)
    makePatNames [] vs s = []
    makePatNames (a :: as) (v :: vs) s
      = let xs = makePatNames as vs s
            basicname = UN v
        in if isUse0 a.count || a.isIndex
             then Nothing :: xs
             else Just (mapName (++ s) basicname) :: xs

    -- The lhs of our function, fields we don't want to use are replaced with _
    makePat : (con : Name) -> (vars : List (Maybe Name)) -> TTImp
    makePat con vars = foldl
      (\tt,v => `(~(tt) ~(maybe implicit' bindNameVar v))) (iVar con) vars

    -- A little wordy here, it's set up this way instead of a fold to avoid an
    -- extra True when building up our && chain. There's no reason to make the
    -- user repeat work every time they use their derived implementation.
    makeRhs : List (Name,Name) -> TTImp
    makeRhs [] = `(EQ)
    makeRhs [(x,y)] = `( compare ~(iVar x) ~(iVar y) )
    makeRhs ((x,y) :: xs) = `( compare ~(iVar x) ~(iVar y) <+> ~(makeRhs xs) )

-- Assign a number to the position of a constructor. We use this to check simple
-- ordering. When equal we go on to check constituents.
compareClauses : (opname : Name) -> TypeInfo -> Elab (List Clause)
compareClauses op tyinfo = do
    let ncons = zipSL [0..] tyinfo.cons
        clauses = [| compareClause (pure op) ncons ncons |]
    logMsg "compareClauses" 1 ""
    sequence clauses
    -- pure [] --clauses

||| The record that idris would make for you when you write an implementation.
ordObject : (decname : Name) -> (funname : Name) -> TypeInfo
          -> Visibility -> Elab (Decl, Decl)
ordObject decname eqfun tyinfo vis = do
  (qname,_) <- lookupName `{{Ord}}
  [NS _ (DN _ ordcon)] <- getCons qname
    | _ => fail "ordObject: error during Ord constructor lookup"
  (qname',tyimp) <- lookupName ordcon
  let conargs' = pullExplicits tyinfo
  logMsg "sada" 1 $ show (length conargs')
  logTerm "lll" 1 "" tyimp
  let conargs = pullExplicits tyinfo
      varnames = map (show . name) conargs
      varnames' = map (show . name) (filter (not . isIndex) conargs)
      ty = appTyCon (map (show . name) conargs)  tyinfo.name
      retty = `( Ord ~(appTyCon (map (show . name) conargs)  tyinfo.name))
      tysig = `( Eq ~ty => ~(addOrdAutoImps varnames' retty))
  logTerm "ty" 1 "asd" ty
  let
      claim = iClaim MW vis [Hint True] (mkTy decname tysig)
      compare = iVar eqfun
      lt = `(\x,y => compare x y == LT)
      gt = `(\x,y => compare x y == GT)
      lte = `(\x,y => compare x y /= GT)
      gte = `(\x,y => compare x y /= LT)
      max = `(\x,y => case compare x y of LT => y; _ => x)
      min = `(\x,y => case compare x y of LT => x; _ => y)
      -- neqfun = `(\x,y => not (x == y))
      -- neqfun = `(\x,y => not (x == y))
      -- neqfun = `(\x,y => not (x == y))
      rhs = `( ~(iVar ordcon) %search ~compare ~lt ~gt ~lte ~gte ~max ~min)
      body = iDef decname [(patClause (iVar decname) rhs)]
  logDecls "ordObject" 1 "claim" [claim]
  logDecls "ordObject" 1 "body" [body]

  pure $ (claim,body)

--
-- (%pi Rig0 Implicit (Just ty)
--   %type
--   (%pi Rig1 Explicit (Just {arg:368})
--     (Prelude.EqOrd.Eq ty)
--     (%pi RigW Explicit (Just compare)
--       (%pi RigW Explicit (Just {arg:369})
--         ty
--         (%pi RigW Explicit (Just {arg:370})
--           ty Prelude.EqOrd.Ordering))
--       (%pi RigW Explicit (Just <)
--         (%pi RigW Explicit (Just {arg:371})
--           ty
--           (%pi RigW Explicit (Just {arg:372})
--             ty
--             Prelude.Basics.Bool))
--         (%pi RigW Explicit (Just >)
--           (%pi RigW Explicit (Just {arg:373})
--             ty
--             (%pi RigW Explicit (Just {arg:374})
--               ty
--               Prelude.Basics.Bool))
--           (%pi RigW Explicit (Just <=)
--             (%pi RigW Explicit (Just {arg:375})
--               ty
--               (%pi RigW Explicit (Just {arg:376})
--                 ty
--                 Prelude.Basics.Bool))
--             (%pi RigW Explicit (Just >=)
--               (%pi RigW Explicit (Just {arg:377})
--                 ty
--                 (%pi RigW Explicit (Just {arg:378})
--                   ty
--                   Prelude.Basics.Bool))
--               (%pi RigW Explicit (Just max)
--                 (%pi RigW Explicit (Just {arg:379})
--                   ty
--                   (%pi RigW Explicit (Just {arg:380})
--                     ty
--                     ty))
--                 (%pi RigW Explicit (Just min)
--                   (%pi RigW Explicit (Just {arg:381})
--                     ty
--                     (%pi RigW Explicit (Just {arg:382})
--                       ty
--                       ty))
--                   (Prelude.EqOrd.Ord ty))))))))))

export
||| Usage: %runElab deriveEq Export `{{Foo}}
||| Currently, this adds eqImplFoo and eqImpltFooFun to the module namespace.
||| This is likely to change in the future to only have eqImplFoo being added
||| to the namespace.
deriveOrd : Visibility -> Name -> Elab ()
deriveOrd vis dataname = do
    (qname,_) <- lookupName dataname -- get the qualified name of our type
    -- create human readable names for our instance components
    let decn = mapName (\d => "ordImpl" ++ d) dataname
        funn = mapName (\d => "ordImpl" ++ d ++ "Fun") dataname
    -- Build general info about the type we're deriving (e.g. Foo) that we want
    -- to keep around.
    tyinfo <- makeTypeInfo qname

    -- The components of our eq-ing function
    funclaim <- compareClaim funn tyinfo Private -- NB private
    funclauses <- compareClauses funn tyinfo

    -- Our function's complete definition
    let fundecl = iDef funn funclauses

    -- The actual eqImplFoo : Eq Foo record.
    (objclaim,objclause) <- ordObject decn funn tyinfo vis

    -- Declare our things into the namespace
    -- Both claims first, otherwise we won't find our own Eq in fundecl
    declare [funclaim, objclaim]
    declare [fundecl, objclause]

export
data Foo1 : Type -> Type where
  Bor1 : Foo1 a

export
data Foo2 : Type -> Type where
  Bor2 : a -> Foo2 a

data Foo4 : Type -> Type -> Type where
  Bor4 : b -> Foo4 a b

data Foo5 : Type -> Type -> Type -> Type where
  Bor5 : a -> b -> c -> Foo5 a b c

-- NB c is never used, so Eq shouldn't be required for it
data Foo7 : Type -> Type -> Type -> Type where
  Zor7 : a -> Foo7 a b c
  Gor7 : b -> Foo7 a b c
  Nor7A : a -> b -> Foo7 a b c
  Nor7B : a -> b -> c -> Foo7 a b c
  Bor7 : Foo7 a b c

-- NB a is never used, so Eq shouldn't be required for it
data Foo7' : Type -> Type -> Type -> Type where
  Zor7' : c -> Foo7' a b c
  Gor7' : b -> Foo7' a b c
  Nor7' : b -> c -> Foo7' a b c
  Bor7' : Foo7' a b c

  -- we'll use our own nat for index experimentation
export
data MyNat : Type where
  MZ : MyNat
  MS : MyNat -> MyNat

data Foo6 : Type -> Type -> Type -> Nat -> Type where
  Zor6 : a -> b -> Foo6 a b c Z
  Gor6 : b -> Foo6 a b c (S k)
  Nor6A : a -> b -> c -> Foo6 a b c n
  Nor6B : a -> (0 _ : b) -> c -> Foo6 a b c n -- NB: 0 Use arg
  Bor6A : Foo6 a b c n
  Bor6B : Foo6 a b c n -> Foo6 a b c n
  Wah6 : a -> (n : Nat) -> Foo6 a b c n

export
data Foo6' : Type -> Type -> Type -> MyNat -> Type where
  Zor6'  : a -> b -> Foo6' a b c MZ
  Gor6A'  : b -> Foo6' a b c (MS k)
  Gor6B'  : (k : MyNat) -> b -> Foo6' a b c (MS k)
  Nor6A' : a -> b -> c -> Foo6' a b c n
  Nor6B' : a -> (0 _ : b) -> c -> Foo6' a b c n
  Bor6'  : Foo6' a b c n
  Wah6'  : a -> (n : MyNat) -> Foo6' a b c n
  Kah6'  : a -> (n : MyNat) -> (0 _ : c) -> Foo6' a b c n
  Pah6'  : a -> (n : MyNat) -> MyNat -> (0 _ : c) -> Foo6' a b c n
  -- Rah6'  : a -> (n : MyNat) -> Foo6' a b c n -> MyNat -> (0 _ : c) -> Foo6' a b c n -> Foo6' a b c n
  -- Gah6'  : {1 _ : a} -> (n : MyNat) -> MyNat -> (0 _ : c) -> Foo6' a b c n
  -- ^ another case to consider, what if I'm implicit but M1?
  -- Seems like an error would be appropriate there rather than showing
  -- implicits. Though showing implicits could be a flag in instance generation
  -- I guess.

-- eqImplFoo6'Fun (Wah6' 'c' MZ) (Wah6' 'c' MZ)
-- eqImplFoo6'Fun (Nor6A' {n=MZ} 'c' 'd' 'e')

-- eqImplFoo6Fun (Wah6 {b=Int} {c=String} 'c' (S Z)) (Wah6 'c' (S Z))

-- reference impl
-- NB We need to use n twice, Eq is not dependent, two values of `a` compared
-- against each other must have the same indices. Which follows since if they
-- don't they're obviously not equal.
-- if a con has no explicit, non-M0, non-index, vars then it's empty, and thus
-- vauously true to compare to itself. only explicit, non-M0, non-index vars need
-- to be compared. M0 values can't be used and index vars can't vary in an Eq
-- definition
eqFoo6 : (Eq a, Eq b, Eq c) => Foo6 a b c n -> Foo6 a b c n -> Bool
eqFoo6 (Zor6 x1 y1) (Zor6 x2 y2) = x1 == x2 && y1 == y2
eqFoo6 (Gor6 x1) (Gor6 x2) = x1 == x2
eqFoo6 (Nor6A x1 y1 z1) (Nor6A x2 y2 z2) = x1 == x2 && y1 == y2 && z1 == z2
eqFoo6 (Nor6B x1 _ z1) (Nor6B x2 _ z2) = x1 == x2 && z1 == z2
eqFoo6 Bor6A Bor6A = True
eqFoo6 (Bor6B x1) (Bor6B x2) = eqFoo6 x1 x2
-- we prefer to write this as x1 == x2, and we do so by declaring our Eq object
-- early, otherwise there's no instance for Foo6 to use == from
eqFoo6 (Wah6 x1 _) (Wah6 x2 _) = x1 == x2 -- indices do not differ
eqFoo6 _ _ = False
-- eqFoo6 {b=Int} {c=String} (Wah6 'c' (S Z)) (Wah6 'c' (S Z))

data FooN : MyNat -> Type -> Type where
  BorZ : b -> FooN MZ b
  BorS : b -> FooN (MS MZ) b
  BorNA : (k : MyNat) -> b -> FooN n b
  BorNB : (n : MyNat) -> b -> FooN n b

-- TODO Tim: Broken
-- %runElab deriveEq Export `{{MyNat}}
-- %runElab deriveOrd Export `{{MyNat}}
-- %runElab deriveEq Export  `{{Foo2}}
-- %runElab deriveOrd Export `{{Foo2}} -- works but doesn't warn if no Eq instance is this because the constraint is the more involved Eq (Foo2 a) instead of Eq MyNat?
-- %runElab deriveEq Private `{{Foo4}}
-- %runElab deriveOrd Private `{{Foo4}}
-- %runElab deriveEq Private `{{Foo5}}
-- %runElab deriveOrd Private `{{Foo5}}
-- %runElab deriveEq Private `{{Foo7}}
-- %runElab deriveOrd Private `{{Foo7}}
-- %runElab deriveEq Private `{{Foo7'}}
-- %runElab deriveOrd Private `{{Foo7'}}
-- %runElab deriveOrd Private `{{FooN}} -- trouble with indices still
-- %runElab deriveOrd Private `{{Foo6}}
-- %runElab deriveOrd Export  `{{Foo6'}}


text:
module CLaSH.Prelude

import CLaSH.Default
import CLaSH.Signal
import CLaSH.Prelude.Vect
import Data.HVect

%access public

window : (Default a) => Signal a -> Vect (S (S n)) (Signal a)
window {a} x = (x::prev)
  where
    prev : Default a => Vect (S n) (Signal a)
    next : Default a => Vect (S n) (Signal a)
    prev = unpack (register (pure def) (pack next))
    next = x +>> prev

max_stars_repo_name: christiaanb/clash-prelude-idris

max_issues_repo_name: christiaanb/clash-prelude-idris

max_forks_repo_name: christiaanb/clash-prelude-idris


text:
module Sub12LTE108t39

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total

-- 6(18t+6)+3 --DB[3,-1,-2]--> 6(2t)+3
export
lte108t39 : (l : Nat) -> LTE (S (plus l l)) (S (S (S ((S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l)))))))
lte108t39 Z     = (lteSuccRight . LTESucc) LTEZero
lte108t39 (S l) =
  let lemma = lte108t39 l in
  rewrite (sym (plusSuccRightSucc l l)) in
  rewrite (sym (plusSuccRightSucc (plus l l) l)) in

  rewrite (sym (plusSuccRightSucc (plus (plus l l) l) (S (S (plus (plus l l) l))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus l l) l)    (S (plus (plus l l) l)))) in
  rewrite (sym (plusSuccRightSucc (plus (plus l l) l)       (plus (plus l l) l))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l)) (S (S (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l)))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l))    (S (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l))       (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l)))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l))          (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l))             (S (S (plus (plus (plus l l) l) (plus (plus l l) l)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l))                (S (plus (plus (plus l l) l) (plus (plus l l) l))))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l)) (S (plus (plus (plus l l) l) (plus (plus l l) l)))) (S (S (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l)))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l)) (S (plus (plus (plus l l) l) (plus (plus l l) l))))    (S (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l)) (S (plus (plus (plus l l) l) (plus (plus l l) l))))       (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l)))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l)) (S (plus (plus (plus l l) l) (plus (plus l l) l))))          (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l)) (S (plus (plus (plus l l) l) (plus (plus l l) l))))             (S (S (plus (plus (plus l l) l) (plus (plus l l) l)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l)) (S (plus (plus (plus l l) l) (plus (plus l l) l))))                (S (plus (plus (plus l l) l) (plus (plus l l) l))))) in
    (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc) lemma


text:
--    Copyright 2017, the blau.io contributors
--
--    Licensed under the Apache License, Version 2.0 (the "License");
--    you may not use this file except in compliance with the License.
--    You may obtain a copy of the License at
--
--        http://www.apache.org/licenses/LICENSE-2.0
--
--    Unless required by applicable law or agreed to in writing, software
--    distributed under the License is distributed on an "AS IS" BASIS,
--    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--    See the License for the specific language governing permissions and
--    limitations under the License.

module API.WebGL.Shader

import IdrisScript

%access public export
%default total

record WebGLShader where
  constructor New
  self : JSRef

FRAGMENT_SHADER : Int
FRAGMENT_SHADER = 0x8B30

VERTEX_SHADER : Int
VERTEX_SHADER = 0x8B31

max_stars_repo_name: blau-io/idris-webgl

max_issues_repo_name: blau-io/idris-webgl

max_forks_repo_name: blau-io/idris-webgl


text:
module Commons.System

import System

import Control.IOExcept
import Control.ST

import Data.So

public export
interface SystemIO (m : Type -> Type) where
  getArgs : STrans m (List String) xs (const xs)
  time    : STrans m Integer       xs (const xs)
  usleep  : (i : Int)
         -> {auto prf : So (i >= 0)}
         -> STrans m () xs (const xs)

export
SystemIO IO where
  getArgs = lift getArgs
  time    = lift time
  usleep i {prf} = lift $ usleep i {prf=prf}

-- --------------------------------------------------------------------- [ EOF ]


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/modules.html#indices
module WebAssembly.Structure.Modules.Indices

import WebAssembly.Structure.Values

-- Definition

public export
TypeIdx : Type
TypeIdx = U32

public export
FuncIdx : Type
FuncIdx = U32

public export
TableIdx : Type
TableIdx = U32

public export
MemIdx : Type
MemIdx = U32

public export
GlobalIdx : Type
GlobalIdx = U32

public export
LocalIdx : Type
LocalIdx = U32

public export
LabelIdx : Type
LabelIdx = U32

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
||| Derive Eq and DecEq
|||
||| You'll get cryptic errors if you try to use it without importing
||| `Language.Reflection` and `Extra.Prelude`.
module Extra.Language.Derive

import Extra.Prelude
import Language.Reflection
import Decidable.Equality

%language ElabReflection

argTys : (ty : TTImp) -> List TTImp
argTys (IPi _ _ ExplicitArg _ argTy retTy) = argTy :: argTys retTy
argTys (IPi _ _ _ _ _ retTy) = argTys retTy
argTys _ = []

countArgs : (ty : TTImp) -> Nat
countArgs = length . argTys

fullyBind : FC -> TTImp -> String -> Int -> (ty : TTImp) -> TTImp
fullyBind pos f argName i (IPi _ _ ExplicitArg _ _ retTy)
  = fullyBind pos (IApp pos f (IBindVar pos (argName ++ show i))) argName (i+1) retTy
fullyBind pos f argName i (IPi _ _ _ _ _ retTy)
  = fullyBind pos f argName i retTy
fullyBind pos f argName i _ = f

fullyApply : FC -> TTImp -> String -> Int -> (ty : TTImp) -> TTImp
fullyApply pos f argName i (IPi _ _ ExplicitArg _ _ retTy)
  = fullyApply pos (IApp pos f (IVar pos $ UN $ argName ++ show i)) argName (i+1) retTy
fullyApply pos f argName i (IPi _ _ _ _ _ retTy)
  = fullyApply pos f argName i retTy
fullyApply pos f argName i _ = f

lookupConstr : Name -> Elab (Name, TTImp)
lookupConstr constr = do
  [(n, ty)] <- getType constr
    | [] => fail $ "constr " ++ show constr ++ " does not exist? hmmm"
    | _ => fail $ "ambiguous name for constr " ++ show constr
  pure (n, ty)

lookupType : Name -> Elab (Name, TTImp)
lookupType typeName = do
  [(n, ty)] <- getType typeName
    | [] => fail $ "name " ++ show typeName ++ " not in scope"
    | _ => fail $ "ambiguous name " ++ show typeName
  pure (n, ty)

||| Derive `Eq` for a type.
|||
||| Use:
||| mutual
|||   myEq : Eq a => MyType a -> MyType a -> Bool
|||   %runElab deriveEq `{{ myEq }} `{{ MyType }}
|||
|||   Eq a => Eq (MyType a) where
|||     (==) = myEq
export
deriveEq : Name -> Name -> Elab ()
deriveEq funcName typeName = do
  let pos = MkFC ("deriveEq for " ++ show typeName) (0,0) (0,0)
  (n, _) <- lookupType typeName
  constrs <- getCons n
  let and : TTImp -> TTImp -> TTImp
      and x y = `(~(x) && ~(y))
      compareEq : String -> String -> TTImp
      compareEq x y = `((~(IVar pos $ UN x)) == (~(IVar pos $ UN y)))
      makeClause : Name -> Elab Clause
      makeClause constr = do
        (_, ty) <- lookupConstr constr
        let nArgs = countArgs ty
        let xs = map (\i => "x_" ++ show i) $ take nArgs [1..]
        let ys = map (\i => "y_" ++ show i) $ take nArgs [1..]
        let px = foldl (IApp pos) (IVar pos constr) $ map (IBindVar pos) xs
        let py = foldl (IApp pos) (IVar pos constr) $ map (IBindVar pos) ys
        pure $ PatClause pos `(MkPair ~(px) ~(py))
             $ foldl and `(True) $ zipWith compareEq xs ys
      finalClause : Clause
      finalClause = PatClause pos `(_) `(False)
  clauses <- traverse makeClause constrs
  let allClauses = clauses ++ [finalClause]
      caseExpr = ICase pos `(MkPair x y) (Implicit pos True) allClauses
      result = `(\x, y => ~(caseExpr))
      clauses = [PatClause pos (IVar pos funcName) result]
  declare [IDef pos funcName clauses]

-- Wow! what an opportunity to derive equality
eqNamespace : Namespace -> Namespace -> Bool
%runElab deriveEq `{{ eqNamespace }} `{{ Namespace }}

export
Eq Namespace where
  (==) = eqNamespace

mutual
  eqName : Name -> Name -> Bool
  %runElab deriveEq `{{ eqName }} `{{ Name }}

  export
  Eq Name where
    (==) = eqName

||| Derive `DecEq` for a type.
|||
||| Use:
||| mutual
|||   myDecEq : DecEq a => (x : MyType a) -> (y : MyType a) -> Dec (x = y)
|||   %runElab deriveDecEq `{{ myDecEq }} `{{ MyType }}
|||
|||   DecEq a => DecEq (MyType a) where
|||     decEq = myDecEq
export
deriveDecEq : Name -> Name -> Elab ()
deriveDecEq funcName typeName = do
  let pos = MkFC ("deriveDecEq for " ++ show typeName) (0,0) (0,0)
      thisFunc = IVar pos funcName
  (n, _) <- lookupType typeName
  constrs <- getCons n
  let makeClause : Int -> (Int -> TTImp) -> TTImp -> List TTImp -> TTImp -> Clause
      makeClause i mkIndTy lhsSoFar withBinds ty = case ty of
        IPi _ _ ExplicitArg _ argTy retTy =>
          let nArgs = 1 + countArgs retTy
              px = fullyBind pos lhsSoFar "x__" i ty
              py = fullyBind pos lhsSoFar "y__" i ty
              thisX = IVar pos $ UN $ "x__" ++ show i
              thisY = IVar pos $ UN $ "y__" ++ show i
              decEqXY = `(decEq ~(thisX) ~(thisY))
              lhs = foldl (IApp pos) `(~(thisFunc) ~(px) ~(py)) withBinds
          in WithClause pos lhs decEqXY [
            -- No clause
            PatClause pos `(~(lhs) (No ~(IBindVar pos "bad")))
              $ ILocal pos `[ ind : ~(mkIndTy i)
                              ind Refl = Refl ]
                           `(No (bad . ind)),
            -- Yes clause
            makeClause (i+1)
                       mkIndTy
                       (IApp pos lhsSoFar thisX)
                       (withBinds ++ [`(Yes Refl)])
                       retTy
            ]
        IPi _ _ _ _ _ retTy =>
          makeClause i mkIndTy lhsSoFar withBinds retTy -- Ignore implicit arguments
        _ => let startingLhs = `(~(thisFunc) ~(lhsSoFar) ~(lhsSoFar))
                 lhs = foldl (IApp pos) startingLhs withBinds
             in PatClause pos lhs `(Yes Refl)
      -- bindImplicits "x" Constr (typeof Constr) thing = forall xi. thing
      bindImplicits : String -> Name -> TTImp -> TTImp -> TTImp
      bindImplicits varName constr ty thing =
        let args = the (List (Int, _)) $ zip [1..] $ argTys ty in
        let implicitPi : (String,TTImp) -> TTImp -> TTImp
            implicitPi (n,arg) ty = IPi pos M0 ImplicitArg (Just $ UN n) arg ty
        in foldr implicitPi thing $ map (\(i,t) => (varName ++ show i, t)) args
      makeSameClause : Name -> Elab Clause
      makeSameClause constr = do
        (name, ty) <- lookupConstr constr
        let boundA = fullyApply pos (IVar pos name) "a__" 1 ty
            boundB = fullyApply pos (IVar pos name) "b__" 1 ty
        let makeIndTy : Int -> TTImp
            makeIndTy i = let a = IVar pos $ UN $ "a__" ++ show i
                              b = IVar pos $ UN $ "b__" ++ show i
                          in bindImplicits "a__" name ty
                            $ bindImplicits "b__" name ty
                            $ `(~(boundA) === ~(boundB) -> ~(a) === ~(b))
        pure $ makeClause 1 makeIndTy (IVar pos name) [] ty
      makeDiffClause : Name -> Name -> Elab Clause
      makeDiffClause c1 c2 = do
        (n1, ty1) <- lookupConstr c1
        (n2, ty2) <- lookupConstr c2
        let thing1 = fullyApply pos (IVar pos n1) "a__" 1 ty1
            thing2 = fullyApply pos (IVar pos n2) "b__" 1 ty2
            badTy = bindImplicits "a__" n1 ty1
                  $ bindImplicits "b__" n2 ty2
                  $ `(~(thing1) = ~(thing2) -> Void)
        let pat1 : TTImp
            pat1 = foldl (\t, _ => IApp pos t (Implicit pos True)) (IVar pos n1) $ argTys ty1
            pat2 : TTImp
            pat2 = foldl (\t, _ => IApp pos t (Implicit pos True)) (IVar pos n2) $ argTys ty2
            lhs : TTImp
            lhs = `(~(thisFunc) ~(pat1) ~(pat2))
            bad : List Decl
            bad = [IClaim pos MW Private [] $ MkTy pos (UN "bad") badTy]
                ++ `[ bad Refl impossible ]
        pure $ PatClause pos lhs
             $ ILocal pos bad `(No bad)
  clauses <- sequence $ do
    a <- constrs
    b <- constrs
    pure $ if a == b then makeSameClause a
                     else makeDiffClause a b
  declare [IDef pos funcName clauses]


text:
module MSubst

-- Multiple substitution in order to
-- turn a term that is well-typed in
-- a context into a closed term (i.e.
-- into a term that is well-typed in
-- the empty context).

import R
import Subst
import SubstLemmas
import Term
import Typing

%default total
%access export

-------------------------------------------------------------
-- Begin: VALUE ENVIRONMENT THAT IS COMPATIBLE WITH A CONTEXT

public export
data VEnv : Context -> Type where
  VNil  : VEnv []
  VCons : (e : Term) -> Value e -> r s e ->
          VEnv ctx ->
          VEnv (s::ctx)

-- End: VALUE ENVIRONMENT THAT IS COMPATIBLE WITH A CONTEXT
-----------------------------------------------------------

-------------------------------
-- Begin: MULTIPLE SUBSTITUTION

public export
msubst : Term -> (i : Nat) -> VEnv ctx -> Term
msubst e _ VNil = e
msubst e i (VCons x _ _ venv) =
  let e' = subst x i e
  in msubst e' i venv

-- End: MULTIPLE SUBSTITUTION
-----------------------------

-------------------
-- Begin: WEAKENING

-- Weakening means extending a typing context
-- of a term 'e' on the right. This leaves the
-- de Bruijn indices that are referenced in 'e'
-- unchanged.
-- Weakening can be implemented with the 'shiftTerm'
-- operation by using a cutoff that is exactly the
-- length of the typing context.
-- Weakening is useful in the subsequent reasoning
-- about the 'msubst' operation.

weaken : (e : Term) ->
         Typing ctx e t ->
         Context ->
         Term
weaken e {ctx} _ ctx' = shiftTerm (length ctx) (length ctx') e

-- Weakening does not actually change a term:
weakenIdentity : (e : Term) ->
                 (ty : Typing ctx e t) ->
                 (ctx' : Context) ->
                 weaken e ty ctx' = e
weakenIdentity e {ctx} ty ctx' =
  let eq1 = shiftTermPastCtx e ctx ty Z (length ctx')
      eq2 = plusZeroRightNeutral (length ctx)
      eq3 = cong {f = \q => shiftTerm q (length ctx') e} (sym eq2)
  in trans eq3 eq1

-- Weakening preserves typing, albeit in
-- an extended context:
weakenPreservesTy : (e : Term) ->
                    (ty : Typing ctx e t) ->
                    (ctx' : Context) ->
                    Typing (ctx++ctx') (weaken e ty ctx') t
weakenPreservesTy e {ctx} {t} ty ctx' =
  let eq1 = appendNilRightNeutral ctx
      ty1 = replace {P = \q => Typing q e t} (sym eq1) ty
      ty2 = shiftTermTy e {ctx1=ctx} {ctx2=[]} ty1 ctx'
      e'  = shiftTerm (length ctx) (length ctx') e
      eq2 = appendNilRightNeutral ctx'
  in replace {P = \q => Typing (ctx++q) e' t} eq2 ty2

-- End: WEAKENING
-----------------

--------------------------------------------
-- Begin: LEMMAS ABOUT MULTIPLE SUBSTITUTION

-- Multiple substitution preserves typing:
mSubstPreservesTy : (e : Term) ->
                    Typing (ctx1++ctx2) e t ->
                    (venv : VEnv ctx2) ->
                    Typing ctx1 (msubst e (length ctx1) venv) t
mSubstPreservesTy e ty {t} VNil {ctx1} =
  let eq = appendNilRightNeutral ctx1
  in replace {P = \q => Typing q e t} eq ty
mSubstPreservesTy e ty {t} (VCons x _ rx venv) {ctx1} {ctx2 = s::ctx2} =
  let tyx  = rTyping x rx
      x'   = weaken x tyx ctx2
      tyx1 = weakenPreservesTy x tyx ctx2
      ty'  = substPreservesTy {ctx1=ctx1} e ty x' tyx1
      eq1  = weakenIdentity x tyx ctx2
      ty'' = replace {P = \q => Typing (ctx1++ctx2) (subst q (length ctx1) e) t} eq1 ty'
  in mSubstPreservesTy (subst x (length ctx1) e) ty'' venv

-- Multiple substitution acts as the identity
-- on an expression 'e' if 'e' is typed in the
-- context 'ctx' but multiple substitution only
-- takes place at an index 'i' that is equal to
-- or greater than 'length ctx':
mSubstPastCtx : (e : Term) ->
                (ctx : Context) ->
                (Typing ctx e t) ->
                (venv : VEnv ctx') ->
                msubst e (length ctx) venv = e
mSubstPastCtx e ctx ty VNil = Refl
mSubstPastCtx e ctx ty (VCons x _ rx venv) {t} {ctx' = s::ctx'} =
  let e'  = weaken e ty [s]
      ty1 = weakenPreservesTy e ty [s]
      tyx = rTyping x rx
      ty2 = substPreservesTy {ctx1=ctx} {ctx2=[]} e' ty1 x tyx
      eq1 = appendNilRightNeutral ctx
      ty3 = replace {P = \q => Typing q (subst x (length ctx) e') t} eq1 ty2
      eq2 = weakenIdentity e ty [s]
      ty4 = replace {P = \q => Typing ctx (subst x (length ctx) q) t} eq2 ty3
      ih  = mSubstPastCtx (subst x (length ctx) e) ctx ty4 venv
      eq3 = substPastCtx e ctx ty {n=0}
      eq4 = cong {f = \q => subst x q e} $ plusZeroRightNeutral (length ctx)
      eq5 = trans (sym eq4) eq3
  in trans ih eq5

-- Multiple subsitution commutes with (ordinary) substitution:
mSubstSubstSwap : (e : Term) ->
                  (i : Nat) -> (venv : VEnv ctx) ->
                  (y : Term) -> Typing [] y s ->
                  subst y i (msubst e (S i) venv) = msubst (subst y i e) i venv
mSubstSubstSwap e i VNil y tyy = Refl
mSubstSubstSwap e i (VCons x _ _ venv) y tyy =
  let eq1 = substSwap e i y x tyy
      eq2 = cong {f = \q => msubst q i venv} eq1
      ih  = mSubstSubstSwap (subst x (S i) e) i venv y tyy
  in trans ih (sym eq2)

-- Following multiple substitution with an ordinary
-- substitution amounts to multiple substitution in
-- an extended environment:
mSubstSubstSwap' : (e : Term) ->
                   (i : Nat) -> (venv : VEnv ctx) ->
                   (y : Term) -> (vy : Value y) -> (ry : r s y) ->
                   subst y i (msubst e (S i) venv) = msubst e i (VCons y vy ry venv)
mSubstSubstSwap' e i venv y vy ry = mSubstSubstSwap e i venv y (rTyping y ry)

-- End: LEMMAS ABOUT MULTIPLE SUBSTITUTION
------------------------------------------

---------------------------------------------------------------
-- Begin: MULTIPLE SUBSTITUTION COMMUTES WITH TERM CONSTRUCTORS

mSubstAbsComm : (e : Term) ->
                (i : Nat) -> (venv : VEnv ctx) ->
                TAbs (msubst e (S i) venv) = msubst (TAbs e) i venv
mSubstAbsComm e _ VNil = Refl
mSubstAbsComm e i (VCons x _ _ venv) = mSubstAbsComm (subst x (S i) e) i venv

mSubstAppComm : (e1 : Term) -> (e2 : Term) ->
                (i : Nat) -> (venv : VEnv ctx) ->
                TApp (msubst e1 i venv) (msubst e2 i venv) = msubst (TApp e1 e2) i venv
mSubstAppComm e1 e2 i VNil = Refl
mSubstAppComm e1 e2 i (VCons x _ _ venv) =
  mSubstAppComm (subst x i e1) (subst x i e2) i venv

mSubstRecComm : (e1 : Term) -> (e2 : Term) -> (e3 : Term) ->
                (i : Nat) -> (venv : VEnv ctx) ->
                TRec (msubst e1 i venv) (msubst e2 i venv) (msubst e3 i venv) =
                  msubst (TRec e1 e2 e3) i venv
mSubstRecComm e1 e2 e3 i VNil = Refl
mSubstRecComm e1 e2 e3 i (VCons x _ _ venv) =
  mSubstRecComm (subst x i e1) (subst x i e2) (subst x i e3) i venv

mSubstSuccComm : (e : Term) ->
                 (i : Nat) -> (venv : VEnv ctx) ->
                 TSucc (msubst e i venv) = msubst (TSucc e) i venv
mSubstSuccComm e i VNil = Refl
mSubstSuccComm e i (VCons x _ _ venv) =
  mSubstSuccComm (subst x i e) i venv

mSubstPredComm : (e : Term) ->
                 (i : Nat) -> (venv : VEnv ctx) ->
                 TPred (msubst e i venv) = msubst (TPred e) i venv
mSubstPredComm e i VNil = Refl
mSubstPredComm e i (VCons x _ _ venv) =
  mSubstPredComm (subst x i e) i venv

mSubstIfzComm : (e1 : Term) -> (e2 : Term) -> (e3 : Term) ->
                (i : Nat) -> (venv : VEnv ctx) ->
                TIfz (msubst e1 i venv) (msubst e2 i venv) (msubst e3 i venv) =
                  msubst (TIfz e1 e2 e3) i venv
mSubstIfzComm e1 e2 e3 i VNil = Refl
mSubstIfzComm e1 e2 e3 i (VCons x _ _ venv) =
  mSubstIfzComm (subst x i e1) (subst x i e2) (subst x i e3) i venv

-- End: MULTIPLE SUBSTITUTION COMMUTES WITH TERM CONSTRUCTORS
-------------------------------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Data.Stream

import Data.List

||| The first element of an infinite stream
public export
head : Stream a -> a
head (x::xs) = x

||| Drop the first n elements from the stream
||| @ n how many elements to drop
public export
drop : (n : Nat) -> Stream a -> Stream a
drop Z     xs = xs
drop (S k) (x::xs) = drop k xs

||| An infinite stream of repetitions of the same thing
public export
repeat : a -> Stream a
repeat x = x :: repeat x

||| Generate an infinite stream by repeatedly applying a function
||| @ f the function to iterate
||| @ x the initial value that will be the head of the stream
public export
iterate : (f : a -> a) -> (x : a) -> Stream a
iterate f x = x :: iterate f (f x)

||| Get the nth element of a stream
public export
index : Nat -> Stream a -> a
index Z     (x::xs) = x
index (S k) (x::xs) = index k xs

||| Combine two streams element-wise using a function.
|||
||| @ f the function to combine elements with
||| @ xs the first stream of elements
||| @ ys the second stream of elements
export
zipWith : (f : a -> b -> c) -> (xs : Stream a) -> (ys : Stream b) -> Stream c
zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

||| Combine three streams by applying a function element-wise along them
export
zipWith3 : (a -> b -> c -> d) -> Stream a -> Stream b -> Stream c -> Stream d
zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs

||| Create a stream of pairs from two streams
export
zip : Stream a -> Stream b -> Stream (a, b)
zip = zipWith (\x,y => (x,y))

||| Combine three streams into a stream of tuples elementwise
export
zip3 : Stream a -> Stream b -> Stream c -> Stream (a, b, c)
zip3 = zipWith3 (\x,y,z => (x,y,z))

||| Create a pair of streams from a stream of pairs
export
unzip : Stream (a, b) -> (Stream a, Stream b)
unzip xs = (map fst xs, map snd xs)

||| Split a stream of three-element tuples into three streams
export
unzip3 : Stream (a, b, c) -> (Stream a, Stream b, Stream c)
unzip3 xs = (map (\(x,_,_) => x) xs, map (\(_,x,_) => x) xs, map (\(_,_,x) => x) xs)

||| Return the diagonal elements of a stream of streams
export
diag : Stream (Stream a) -> Stream a
diag ((x::xs)::xss) = x :: diag (map tail xss)

||| Produce a Stream of left folds of prefixes of the given Stream
||| @ f the combining function
||| @ acc the initial value
||| @ xs the Stream to process
export
scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Stream b) -> Stream a
scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs

||| Produce a Stream repeating a sequence
||| @ xs the sequence to repeat
||| @ ok proof that the list is non-empty
export
cycle : (xs : List a) -> {auto ok : NonEmpty xs} -> Stream a
cycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs
  where cycle' : List a -> Stream a
        cycle' []        = x :: cycle' xs
        cycle' (y :: ys) = y :: cycle' ys

public export
partial
takeUntil : (n -> Bool) -> Stream n -> List n
takeUntil p (x :: xs)
    = if p x
         then [x]
         else x :: takeUntil p xs

public export
partial
takeBefore : (n -> Bool) -> Stream n -> List n
takeBefore p (x :: xs)
    = if p x
         then []
         else x :: takeBefore p xs

export
Applicative Stream where
  pure = repeat
  (<*>) = zipWith apply

export
Monad Stream where
  s >>= f = diag (map f s)

--------------------------------------------------------------------------------
-- Properties
--------------------------------------------------------------------------------

lengthTake : (1 n : Nat) -> (xs : Stream a) -> length (take n xs) = n
lengthTake Z _ = Refl
lengthTake (S n) (x :: xs) = cong S (lengthTake n xs)


text:
foo : String
foo = """\{"hello"}
"""


text:
module Poker

import Control.ST
import Control.ST.Random
import Data.Fin
-- import Data.Fin.Extra
import Data.Vect
import Data.Vect.Views

import Poker.Deck

%default total

Hand : Type
Hand = Vect 7 Card

sort : Ord t => Vect n t -> Vect n t
sort xs with (splitRec xs)
  sort [] | SplitRecNil = []
  sort [x] | SplitRecOne = [x]
  sort (ys ++ zs) | (SplitRecPair lrec rrec) =
    merge (sort ys | lrec) (sort zs | rrec)

data SuitCount : Suit -> Vect n Card -> Nat -> Type where
  SuitEmpty : (h : Vect Z Card) -> SuitCount s h Z
  SuitMatch : (rec : SuitCount s h n) -> SuitCount s ((MkCard s r) :: h) (S n)
  SuitMiss : (rec : SuitCount s h n) ->
             (contra: Not (s = s')) ->
             SuitCount s ((MkCard s' r) :: h) (S n)

suitCount : (s : Suit) -> (h : Vect m Card) -> (n ** SuitCount s h n)
suitCount s [] = (0 ** SuitEmpty [])
suitCount s ((MkCard s' r) :: xs) =
  let (_ ** rec) = suitCount s xs
  in case decEq s s' of
    Yes Refl => (_ ** SuitMatch rec)
    No contra => (_ ** SuitMiss rec contra)

data Run : (b : Nat) -> (xs : Vect m Nat) -> (n : Nat) -> Type where
  EmptyRun : (xs : Vect m Nat) -> Run b xs Z
  Step : Elem (n + b) xs -> (rec : Run b xs n) -> Run b xs (S n)

data RankCount : Rank -> Vect n Card -> Nat -> Type where
  RankEmpty : (h : Vect Z Card) -> RankCount s h Z
  RankMatch : (rec : RankCount r h n) -> RankCount r ((MkCard s r) :: h) (S n)
  RankMiss : (rec : RankCount r h n) ->
             (contra: Not (r = r')) ->
             RankCount r ((MkCard s r') :: h) (S n)

rankCount : (r : Rank) -> (h : Vect m Card) -> (n ** RankCount r h n)
rankCount r [] = (0 ** RankEmpty [])
rankCount r ((MkCard s r') :: xs) =
  let (_ ** rec) = rankCount r xs
  in case decEq r r' of
    Yes Refl => (_ ** RankMatch rec)
    No contra => (_ ** RankMiss rec contra)

data Ranks : Vect 5 Rank -> Type where
  MkRanks : (rs : Vect 5 Rank) -> Ranks rs

data StraightRun : Hand -> Type where
  HighStraight : Run b (map (finToNat . Poker.Deck.Card.rank) h) 5 ->
                 StraightRun h
  LowStright : Elem Poker.Deck.ace (map Poker.Deck.Card.rank h) ->
               Run 0 (map (finToNat . Poker.Deck.Card.rank) h) 4 ->
               StraightRun h

data FlushRun : Hand -> Type where
  MkFlush : SuitCount s h n -> LTE 5 n -> FlushRun h

data Score : Hand -> Type where
  HighCard : Ranks (take 5 . reverse . Poker.sort $ map (Poker.Deck.Card.rank) h) ->
             Score h
  Pair : RankCount r h 2 -> Score h
  TwoPair : RankCount r h 2 -> RankCount s h 2 -> Not (r = s) -> Score h
  Trip : RankCount r h 3 -> Score h
  Straight : StraightRun h -> Score h
  Flush : FlushRun h -> Score h
  FullHouse : RankCount r h 3 -> RankCount s h 2 -> Score h
  FullHouse' : RankCount r h 3 -> RankCount s h 3 -> Not (r = s) -> Score h
  Quad : RankCount r h 4 -> Score h
  StraightFlush : StraightRun h -> FlushRun h -> Score h

isFlushHelp : (h : Hand) -> (s : Suit) -> Maybe (FlushRun h)
isFlushHelp h s with (suitCount s h)
  isFlushHelp h s | (n ** ss) with (isLTE 5 n)
    isFlushHelp h s | (n ** ss) | (Yes lte) = Just (MkFlush ss lte)
    isFlushHelp h s | (n ** ss) | (No contra) = Nothing

isFlush : (h : Hand) -> Maybe (FlushRun h)
isFlush h = foldr (<+>) Nothing (map (isFlushHelp h) suits)

checkRun : (b : Nat) -> (xs : Vect m Nat) -> (n : Nat) -> Maybe (Run b xs n)
checkRun b xs Z = Just (EmptyRun xs)
checkRun b xs (S n) =
  case isElem (n + b) xs of
    (Yes prf) => Step prf <$> checkRun b xs n
    (No contra) => Nothing

isStraightHelp : (h : Hand) -> (b : Nat) -> Maybe (StraightRun h)
isStraightHelp h b =
  HighStraight <$> checkRun b (map (finToNat . rank) h) 5

isLowStraight : (h : Hand) -> Maybe (StraightRun h)
isLowStraight h with (isElem ace (map rank h))
  isLowStraight h | (Yes prf) =
    (LowStright prf <$> checkRun 0 (map (finToNat . rank) h) 4)
  isLowStraight h | (No contra) = Nothing

isStraight : (h : Hand) -> Maybe (StraightRun h)
isStraight h =
  foldr (<+>) Nothing (map (isStraightHelp h . finToNat) ranks) <+>
  isLowStraight h

countRanks : (h : Hand) -> Vect 13 (r ** n ** RankCount r h n)
countRanks h = map (\r => (r ** rankCount r h)) (reverse ranks)

findReps : (c : Nat) ->
           Vect o (r ** n ** RankCount r h n) ->
           List (r' ** RankCount r' h c)
findReps c [] = []
findReps c (x :: xs) with (x)
  findReps c (x :: xs) | (r'' ** n' ** rc) =
    case decEq c n' of
      (Yes Refl) => (r'' ** rc) :: findReps c xs
      (No contra) => findReps c xs

findQuad : Vect o (r ** n ** RankCount r h n) ->
           Maybe (Score h)
findQuad rs with (findReps 4 rs)
  findQuad rs | [] = Nothing
  findQuad rs | ((r' ** rc) :: _) = Just (Quad rc)

findTrip : Vect o (r ** n ** RankCount r h n) ->
           Maybe (Score h)
findTrip rs with (findReps 3 rs)
  findTrip rs | [] = Nothing
  findTrip rs | ((r' ** rc) :: _) = Just (Trip rc)

findPairs : Vect o (r ** n ** RankCount r h n) ->
            Maybe (Score h)
findPairs rs with (findReps 2 rs)
  findPairs rs | ((r1 ** rc1) :: (r2 ** rc2) :: xs) =
    case decEq r1 r2 of
      (Yes prf) =>
        -- this should never happen, but handle it
        assert_total $ findPairs rs | ((r1 ** rc1) :: xs)
      (No contra) => Just (TwoPair rc1 rc2 contra)
  findPairs rs | ((r' ** rc) :: []) = Just (Pair rc)
  findPairs rs | [] = Nothing

findFH : Vect o (r ** n ** RankCount r h n) ->
         Maybe (Score h)
findFH rs with (findReps 3 rs)
  findFH rs | [] = Nothing
  findFH rs | (x :: []) with (findReps 2 rs)
    findFH rs | (x :: []) | [] = Nothing
    findFH rs | ((r1 ** rc1) :: []) | ((r2 ** rc2) :: _) = Just (FullHouse rc1 rc2)
  findFH rs | ((r1 ** rc1) :: (r2 ** rc2) :: ys) with (decEq r1 r2)
    findFH rs | ((r1 ** rc1) :: (r2 ** rc2) :: ys) | (Yes prf) =
      -- this should never happen, but handle it
      assert_total $ findFH rs | ((r1 ** rc1) :: ys)
    findFH rs | ((r1 ** rc1) :: (r2 ** rc2) :: _) | (No contra) with (findReps 2 rs)
      findFH rs | ((r1 ** rc1) :: (r2 ** rc2) :: _) | (No contra) | [] =
        Just (FullHouse' rc1 rc2 contra)
      findFH rs | ((r1 ** rc1) :: (r2 ** rc2) :: _) | (No contra) | ((r3 ** rc3) :: _) =
        if (r2 > r3)
        then Just (FullHouse' rc1 rc2 contra)
        else Just (FullHouse rc1 rc3)

score : (h : Hand) -> Score h
score h =
  let f = isFlush h
      s = isStraight h
      rs = countRanks h
      m = (StraightFlush <$> s <*> f) <+>
          (findQuad rs) <+>
          (findFH rs) <+>
          (Flush <$> f) <+>
          (Straight <$> s) <+>
          (findTrip rs) <+>
          (findPairs rs)
      hc = HighCard $ MkRanks (take 5 . reverse . sort $ map rank h)
  in maybe hc id m

-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:

max_stars_repo_name: farrellm/idris-poker

max_issues_repo_name: farrellm/idris-poker

max_forks_repo_name: farrellm/idris-poker


text:
module Data.String.Missing

import Data.Strings
import Data.String.Extra
import Decidable.Equality

import Data.ArrayLike

%default total

-- ---------------------------------------------------------------------------

%foreign "scheme,chez:string-length"
prim__strlength : (sbj:String) -> Int

%foreign "scheme,chez:string-ref"
prim__strAt : (sbj:String) -> (idx:Int) -> Char

%foreign "scheme,chez:substring"
prim__substring : (sbj:String) -> (start:Int) -> (end:Int) -> String

-- ---------------------------------------------------------------------------
--

export
strIndexV : (i:Nat) -> (s:String)
         -> {auto 0 pr0:i < length s = True}
         -> Char
strIndexV i s = prim__strAt s (cast i)

-- ---------------------------------------------------------------------------

export strSplit : (i:Nat) -> (s:String) -> (String, String)
strSplit Z s = ("", s)
strSplit i s = let
    n = length s
    in if n <= i then (s, "")
                 else (substr 0 i s, substr i (n `minus` 1) s)

{-
export strSplitV : (i:Nat) -> (s:String)
                -> {auto 0 pr0:i <= length s}
                -> ((s0:String ** i = length s0), String)
-}

-- ---------------------------------------------------------------------------

export
strFindV : (Char -> Bool) -> (s:String)
        -> Maybe (i:Nat ** i < length s = True )
strFindV f s = go 0 (length s) Refl where
  go : (i, n:Nat) -> (0 pr1:n = length s)
    -> Maybe (i:Nat ** (i < length s = True))
  go i n pr1 with (decEq (i < n) True)
    go i n pr1 | No _ = Nothing
    go i n pr1 | Yes pr2 = let
      pr3 = rewrite sym pr1 in pr2
       in if f (strIndexV{pr0=pr3} i s)
             then Just (i ** pr3 )
             else assert_total $ go (i `plus` 1) n pr1

export
strFindrV : (Char -> Bool) -> (s:String)
        -> Maybe (i:Nat ** (i < length s = True))
strFindrV f s = go (length s) (believe_me (Refl{x=True})) where
  go : (i:Nat) -> (pr1:i <= length s = True)
    -> Maybe (i:Nat ** (i < length s = True))
  go Z _ = Nothing
  go (S i) pr1 = let
    pr3 = believe_me pr1
    pr4 = believe_me pr1
    in if f (strIndexV{pr0=pr3} i s)
         then let pr3 = believe_me pr1 in Just (i ** pr3)
         else go i pr4

-- ---------------------------------------------------------------------------
covering
export isPrefixOf : (pre:String) -> (s:String) -> Bool
isPrefixOf pre s = let
  n = length pre
  m = length s
  in if n <= m
        then let s' = substr 0 n s in s' == pre
        else False

export stripPrefix : (pre:String) -> (s:String) -> String

export isSuffixOf : (suf:String) -> (s:String) -> Bool
export stripSuffix : (suf:String) -> (s:String) -> String

-- ---------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
{- using 'z' in file name to recover alphabetical sort -}
module Part2.Sez10_1_views

%default total

{- ListLast view examples -}
data ListLast : List a -> Type where
   Empty : ListLast []
   NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])

total
listLast : (xs : List a) -> ListLast xs
listLast [] = Empty
listLast (x :: xs) = case listLast xs of
      Empty => NonEmpty [] x
      NonEmpty ys y => NonEmpty (x :: ys) y

describeHelper : (input : List Int) -> ListLast input -> String
describeHelper [] Empty = "Empty"
describeHelper (xs ++ [x]) (NonEmpty xs x)
        = "Non-empty, initial portion = " ++ show xs

describeListEnd : List Int -> String
describeListEnd xs = describeHelper xs (listLast xs)

{- cool with syntax adds additional arguments to function implementation -}
describeListEnd' : List Int -> String
describeListEnd' input with (listLast input)
  describeListEnd' [] | Empty = "Empty"
  describeListEnd' (xs ++ [x]) | (NonEmpty xs x)
          = "Non-empty, initial portion = " ++ show xs

|||slow reverse - ListLast view is rebuilt in each recursive step
covering
myReverse : List a -> List a
myReverse input with (listLast input)
    myReverse [] | Empty = []
    myReverse (xs ++ [x]) | (NonEmpty xs x) = x :: myReverse xs

{-
idris repl:
*Part2/Sez10_1_views> myReverse [5,2,7,1]
[1, 7, 2, 5] : List Integer
-}

{- SplitList, merge sort example -}
data SplitList : List a -> Type where
     SplitNil : SplitList []
     SplitOne : SplitList [x]
     SplitPair : (lefts : List a) -> (rights : List a) ->
                 SplitList (lefts ++ rights)

total
splitList : (input : List a) -> SplitList input
splitList input = splitListHelp input input
where
  {- the first list acts as a counter only,
     each step removes 2 elements from the counter and adds new elements to `lefts`
     when counter is excausted all elements are added to `rights` -}
  splitListHelp : List a -> (input : List a) -> SplitList input
  splitListHelp _ [] = SplitNil
  splitListHelp _ [x] = SplitOne
  splitListHelp (_ :: _ :: counter) (item :: items)
       = case splitListHelp counter items of
              SplitNil => SplitOne  --cool how Idris figures this out!
              SplitOne {x} => SplitPair [item] [x]
              SplitPair lefts rights => SplitPair (item :: lefts) rights
  splitListHelp _ items = SplitPair [] items

covering
mergeSort : Ord a => List a -> List a
mergeSort input with (splitList input)
   mergeSort [] | SplitNil = []
   mergeSort [x] | SplitOne = [x]
   mergeSort (lefts ++ rights) | (SplitPair lefts rights)
                 -- merge : Ord a => List a -> List a -> List a
                 = merge (mergeSort lefts) (mergeSort rights)

{-
idris repl:
*Part2/Sez10_1_views> mergeSort [5,2,7,1]
[1, 2, 5, 7] : List Integer
-}

-- excercises
data TakeN : List a -> Type where
      Fewer : TakeN xs
      Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)

takeN : (n : Nat) -> (xs : List a) -> TakeN xs
takeN Z xs = Exact []  --kinda amazing how much Idris infers here!
takeN (S k) [] = Fewer
takeN (S k) (x :: xs) = case takeN k xs of
       Fewer => Fewer
       Exact rxs => Exact (x :: rxs)

covering
groupByN : (n : Nat) -> (xs : List a) -> List (List a)
groupByN n xs with (takeN n xs)
  groupByN n xs | Fewer = [xs]
  groupByN n (n_xs ++ rest) | (Exact n_xs) = n_xs :: groupByN n rest

{-
idris repl:
*Part2/Sez10_1_views> groupByN 3 [1..10]
[[1, 2, 3], [4, 5, 6], [7, 8, 9], [10]] : List (List Integer)
-}

-- excercise 2
-- use of div forces `partial` here
partial
halves : List a -> (List a, List a)
halves list with (takeN ((length list) `div` 2) list)
   halves list | Fewer = (list, [])
   halves (half1 ++ half2) | (Exact half1) = (half1, half2)

{-
*Part2/Sez10_1_views> halves [1..10]
([1, 2, 3, 4, 5], [6, 7, 8, 9, 10]) : (List Integer, List Integer)
*Part2/Sez10_1_views> halves [1]
([], [1]) : (List Integer, List Integer)
*Part2/Sez10_1_views> the (List Integer, List Integer) (halves [])
([], []) : (List Integer, List Integer)
-}

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module Minecraft.Core.Item

import Minecraft.Core
import public Minecraft.Data.Type.As

%default total

public export
interface Item (self : Type) where
  id : String
  stackable : Maybe Nat
  givenName : self -> Maybe String
  proj : self -> Inf (As Pickup)

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Classical
-- Based on http://www.cs.nott.ac.uk/~psztxa/g53cfr/l06.html/l06.html

-- tertium non datur
TND : Type
TND = (P : Type) -> Either P (P -> Void)
-- reductio ad absurdum
RAA : Type
RAA = (P : Type) -> ((P -> Void) -> Void) -> P
-- Pierce's law
Pierce : Type
Pierce = (P, Q : Type) -> ((P -> Q) -> P) -> P

-- ex falso quod libet
efq : (P : Type) -> Void -> P

tndToRaa : TND -> RAA
tndToRaa tnd P = f (tnd P)
  where
    f : Either P (P -> Void) -> ((P -> Void) -> Void) -> P
    f (Left p) k = p
    f (Right notp) k = efq P (k notp)

raaToTnd : RAA -> TND
raaToTnd raa P = raa (Either P (P -> Void)) (\k => k (Right (\p => k (Left p))))

pierceToRaa : Pierce -> RAA
pierceToRaa pierce P k = pierce (((P -> Void) -> P) -> P) P (\_ => pierce P Void) (\x => efq P (k x))

raaToPierce : RAA -> Pierce
raaToPierce raa P _Q = raa (((P -> _Q) -> P) -> P) (\k => k (\p => p (\q => raa _Q (\_ => k (\_ => q)))))

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
||| The `Node` generator.
module Compiler.ES.Node

import Idris.Env

import Compiler.ES.Codegen

import Compiler.Common
import Compiler.CompileExpr

import Core.Context
import Core.Options
import Core.TT
import Libraries.Utils.Path

import System
import System.File

import Data.Maybe

%default covering

findNode : IO String
findNode = do
   Nothing <- idrisGetEnv "NODE"
      | Just node => pure node
   path <- pathLookup ["node"]
   pure $ fromMaybe "/usr/bin/env node" path

||| Compile a TT expression to Node
compileToNode : Ref Ctxt Defs -> ClosedTerm -> Core String
compileToNode c tm = compileToES c Node tm ["node", "javascript"]

||| Node implementation of the `compileExpr` interface.
compileExpr :  Ref Ctxt Defs
            -> (tmpDir : String)
            -> (outputDir : String)
            -> ClosedTerm
            -> (outfile : String)
            -> Core (Maybe String)
compileExpr c tmpDir outputDir tm outfile =
  do es <- compileToNode c tm
     let out = outputDir </> outfile
     Core.writeFile out es
     pure (Just out)

||| Node implementation of the `executeExpr` interface.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm =
  do let outn = tmpDir </> "_tmp_node" ++ ".js"
     js <- compileToNode c tm
     Core.writeFile outn js
     node <- coreLift findNode
     quoted_node <- pure $ "\"" ++ node ++ "\"" -- Windows often have a space in the path.
     coreLift_ $ system (quoted_node ++ " " ++ outn)
     pure ()

||| Codegen wrapper for Node implementation.
export
codegenNode : Codegen
codegenNode = MkCG compileExpr executeExpr Nothing Nothing


text:
module Data.Function

%access public export
%default total

Inverse : (f : a -> b) -> (g : b -> a) -> Type
Inverse f g = (g . f) = Prelude.Basics.id

Involution : (f : a -> a) -> Type
Involution f = (f . f) = Prelude.Basics.id

Injective : (f : a -> b) -> Type
Injective f {a} {b} = {x : a} -> {y : a} -> (f x = f y) -> (x = y)

Surjective : (g : a -> b) -> Type
Surjective g = Exists (\f => Inverse f g)

Bijective : (f : a -> b) -> Type
Bijective f = (Injective f, Surjective f)

applyId : (f = Prelude.Basics.id) -> (f x = f y) -> (x = y)
applyId p = rewrite p in id

hasInverseIsInjective : Inverse f g -> Injective f
hasInverseIsInjective p1 p2 {g} = applyId p1 (cong p2 {f=g})

inverseIsSurjective : Inverse f g -> Surjective g
inverseIsSurjective p {f} = Evidence f p

involutionIsBijective : Involution f -> Bijective f
involutionIsBijective inv = (hasInverseIsInjective inv, inverseIsSurjective inv)

inverseOfComposition : Inverse f invF -> Inverse g invG -> Inverse (f . g) (invG . invF)
inverseOfComposition pf pg {g} {invF} {invG} =
    let p = cong (cong pf {f=(. g)}) {f=(invG .)}
        in rewrite sym pg
            in p

uniqueInverse : Surjective f -> Inverse f g -> Inverse f h -> g = h
uniqueInverse (Evidence inv p) invG invH {f} {g} {h} = trans gInv hInv
  where
    gInv : g = inv
    gInv = trans (sym (cong p {f=(g .)})) (cong invG {f=(. inv)})
    hInv : inv = h
    hInv = trans (sym (cong invH {f=(. inv)})) (cong p {f=(h .)})

inverseSymmetry : Surjective f -> Inverse f g -> Inverse g f
inverseSymmetry (Evidence val p) invF {f} {g} = solution
  where
    step1 : g . f . val = g
    step1 = cong p {f=(g .)}
    step2 : g . f . val = val
    step2 = cong invF {f=(. val)}
    step3 : g = val
    step3 = trans (sym step1) step2
    solution : Inverse g f
    solution = rewrite step3 in p


text:
||| Borrowed From Idris2 and improved with Test.Unit
module Netlist

import Data.List

import Test.Golden

%default covering

main : IO ()
main
  = runner [ !tests ]

  where
    tests : IO TestPool
    tests
      = testsInDir "netlist"
                   (const True)
                   "NetList Tests"
                   []
                   Nothing
-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module Brainfeck.Instructions

import Data.Vect as V

import Brainfeck.Type

-- TODO: Implement this at some point

%default total

-- TODO: Possibly mae index : Fin n, so its always bounded by the length of instrutions.
-- How to encode that in the constructor?
data Instructions : (index : Nat) -> Vect n Token -> Type where
  Ins : (prev : Vect index Token) -> (remaining : Vect rLen Token) -> Instructions (V.length prev) (reverse prev ++ remaining)

%name Instructions instructions

instructions : (is : Vect n Token) -> Instructions 0 is
instructions is = Ins [] is

current : {auto p: LT pc (V.length is) } -> Instructions pc is -> Token
-- current (Ins prev (cur :: is)) = cur

step : {auto p : LT pc (V.length is)} -> Instructions pc is -> Instructions (S pc) is
-- step (Ins prev (cur :: rem)) = ?stepPrf $ Ins (cur :: prev) rem

jump : (next : Nat) -> Instructions pc is -> Instructions next is

max_stars_repo_name: jhmcstanton/brainfeck

max_issues_repo_name: jhmcstanton/brainfeck

max_forks_repo_name: jhmcstanton/brainfeck


text:
import BasicTypes
import Descriptor
%access public export
mutual
    record Version where
      constructor MkVersion
      major : Maybe Int32
      minor : Maybe Int32
      patch : Maybe Int32
      suffix : Maybe String

    record CodeGeneratorRequest where
      constructor MkCodeGeneratorRequest
      fileToGenerate : List String
      parameter : Maybe String
      proto_file : List FileDescriptorProto
      compiler_version : Maybe Version

    namespace CodeGeneratorResponse
      record File_ where
        constructor MkFile_
        name : Maybe String
        insertionPoint : Maybe String
        content : Maybe String

    record CodeGeneratorResponse where
      constructor MkCodeGeneratorResponse
      error : Maybe String
      file : List File_

max_stars_repo_name: zenhack/idris-protobufs

max_issues_repo_name: zenhack/idris-protobufs

max_forks_repo_name: zenhack/idris-protobufs


text:
module ArgsWrongOrder

import IdrisPrelude

%hide Prelude.Nat.Nat

myFun : (a : Type) -> a -> Nat -> Nat
myFun _ x y = y

myApp : Nat
myApp = myFun _ Zero (IdrisPrelude.Nil Nat)

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

-- Exercise 1

Eq Shape where
    (==) (Triangle base height) (Triangle base' height')
         = base == base' && height == height'
    (==) (Rectangle length height) (Rectangle length' height')
         = length == length' && height == height'
    (==) (Circle radius) (Circle radius') = radius == radius'
    (==) _ _ = False

-- Exercise 2

Ord Shape where
    compare x y = compare (area x) (area y)

testShapes : List Shape
testShapes = [Circle 3, Triangle 3 9, Rectangle 2 6, Circle 4,
              Rectangle 2 7]


text:
--import public Renderer
import public TagList
import public Attributes
import public VNode

max_stars_repo_name: Stinners/alder

max_issues_repo_name: Stinners/alder

max_forks_repo_name: Stinners/alder


text:
module Python.Lib.Threading

import Python
import Python.Prim
import Python.Exceptions

import Python.Lib.Queue

%default total
%access public export

Thread : Signature
Thread f = case f of
  "start" => [] ~~> ()
  "join"  => [] ~~> ()
  _ => Object f

Threading : Signature
Threading f = case f of
  -- the first arg must always be Nothing, according to Python spec
  "Thread" => [Maybe Void, [] ~> ()] ~~> Obj Thread
  _ => Module f

import_ : PIO $ Obj Threading
import_ = importModule "threading"

||| Fork a side thread. The thread will send its result
||| through the queue that is returned by this function.
forkPIO : PIO a -> PIO (Obj $ Queue a)
forkPIO {a = a} work = do
    queue <- Queue.import_ /: "Queue" $: [Erase a, Just 1]
    thread <- Threading.import_ /: "Thread" $: [Nothing, marshalPIO $ worker queue]
    thread /. "start" $. []

    pure queue
  where
    worker : (Obj $ Queue a) -> PIO ()
    worker queue = do
      result <- work
      queue /. "put" $. [result]

||| Wait for the result of a side thread.
wait : Obj (Queue a) -> PIO a
wait q = q /. "get" $. [1]

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module NanoParsec.MonadPlus

export
interface (Monad m) => MonadPlus (m : Type -> Type) where
    mzero : m a
    mplus : m a -> m a -> m a

max_stars_repo_name: stallmanifold/idris-nanoparsec

max_issues_repo_name: lambdaxymox/idris-nanoparsec

max_forks_repo_name: lambdaxymox/idris-nanoparsec


text:
module Ethambda.Common

import Eth.Prelude

infixr 3 <.
infixr 3 <.>

export
(<.>) : String -> String -> String
v <.> w =
  if isNullStr v
  then v
  else v ++ " " ++ " " ++ w

export
ShowS : Type
ShowS = String -> String

export
(<.) : String -> ShowS -> ShowS
s <. c = (s <.>) . c

max_stars_repo_name: fredefox/ethambda-idr

max_issues_repo_name: fredefox/ethambda-idr

max_forks_repo_name: fredefox/ethambda-idr


text:
module Keypad

import Data.Vect

%default total

export
record Keypad where
  constructor MkKeypad
  -- 16 key hexadecimal keypad
  K : Vect 16 Bool

export
Show Keypad where
  show k = show (K k)

export
isKeyPressed : (keypad : Keypad) -> (n : Fin 16) -> Bool
isKeyPressed keypad n = Vect.index n (K keypad)

export
setKeyPress : (keypad : Keypad) -> (n : Fin 16) -> Keypad
setKeyPress keypad n =
  let newK = Vect.replaceAt n True (K keypad) in
  record { K = newK } keypad

export
clearKeyPress : (keypad : Keypad) -> (n : Fin 16) -> Keypad
clearKeyPress keypad n =
  let newK = Vect.replaceAt n False (K keypad) in
  record { K = newK } keypad


text:
module Main

import IdrisJvm.IO
import IdrisJvm.JvmImport
import Java.Lang
import Java.Util

%access public export

%language TypeProviders
%language ElabReflection

comparatorClass : String
comparatorClass = "java/util/Comparator"

pointClass : String
pointClass = "java/awt/Point"

collectionsClass : String
collectionsClass = "java/util/Collections"

stringBuilderClass : String
stringBuilderClass = "java/lang/StringBuilder"

objectsClass : String
objectsClass = "java/util/Objects"

jdkimport [
    (systemClass, ["getProperty", "setProperty"]),
    (stringClass, ["substring", "CASE_INSENSITIVE_ORDER", "valueOf"]),
    (integerClass, ["parseInt"]),
    (comparatorClass, ["compare"]),
    (arrayListClass, ["<init>", "add"]),
    (listClass, ["get"]),
    (collectionsClass, ["max"]),
    (stringBuilderClass, ["<init>", "toString"]),
    (objectsClass, ["toString"]),
    (pointClass, ["<init>", "x"])
  ]

NumberFormatExceptionClass : JVM_NativeTy
NumberFormatExceptionClass = Class "java/lang/NumberFormatException"

NullPointerExceptionClass : JVM_NativeTy
NullPointerExceptionClass = Class "java/lang/NullPointerException"

IllegalArgumentExceptionClass : JVM_NativeTy
IllegalArgumentExceptionClass = Class "java/lang/IllegalArgumentException"

SecurityExceptionClass : JVM_NativeTy
SecurityExceptionClass = Class "java/lang/SecurityException"

objectToString : Inherits Object obj => obj -> JVM_IO String
objectToString obj = (objectsClass <.!> "toString") $ believe_me obj

main : JVM_IO ()
main = do

  -- Safe static methods. Since the return type is primitive and it cannot be null, the return type needs to be only
  -- exception safe so the type is `JVM_IO (Either Throwable Int)`.
  exceptionOrInt <- (integerClass <.> "parseInt") "not a number"
  printLn $ either (const 0) id exceptionOrInt

  -- Unsafe Static method. Type: JVM_IO Int
  printLn !((integerClass <.!> "parseInt") "23")

  -- overload resolution
  printLn !((stringClass <.!> "valueOf(double)") 2.5)
  printLn !((stringClass <.!> "valueOf(char)") 'B')

  -- exception handling
  propValue <- try ((systemClass <.> "getProperty(?java/lang/String)") Nothing) [
    ([jcatch IllegalArgumentExceptionClass, jcatch NullPointerExceptionClass], \t =>
        do
          printLn "property name is null or empty"
          pure Nothing
    ),
    ([catchNonFatal], \t =>
      do
        printLn $ "unable to get property value: " ++ show t
        pure Nothing
    )
  ]
  printLn propValue

  -- Safe instance methods. Here as the return type `String` is not primitive, it can be null so the return type has to
  -- be both exception safe and null safe so the type is `JVM_IO (Either Throwable (Maybe String))`
  noSecondCharException <- (stringClass <.> "substring(int)") "" 1
  putStrLn !(either objectToString (pure . show) noSecondCharException)

  s <- (stringClass <.> "substring(int)") "Foobar" 1
  putStrLn !(either jthrow (pure . show) s) -- rethrowing

  -- Unsafe instance method
  printLn $ !((stringClass <.!> "substring(int)") "Foobar" 1)

  -- Safe constructor. As constructors cannot return null, it needs to be only exception safe so the return type is
  -- `JVM_IO (Either Throwable ArrayList)`
  -- It also demonstrates constructor overloading resolution
  invalidList <- (arrayListClass <.> "<init>(int)") (-1)
  putStrLn !(either objectToString objectToString invalidList)

  -- Unsafe constructor
  list <- arrayListClass <.!> "<init>()"
  exceptionOrMaybeFirstItem <- (listClass <.> "get") list 0
  putStrLn !(either objectToString (maybe (pure "") objectToString) exceptionOrMaybeFirstItem)

  arrayList <- arrayListClass <.!> "<init>()"
  (arrayListClass <.!> "add(java/lang/Object)") arrayList "hello"
  (arrayListClass <.!> "add(java/lang/Object)") arrayList "world"
  -- Passing ArrayList for a Collection. It works because of the "inherits" declaration above.
  max <- (collectionsClass <.!> "max(java/util/Collection)") arrayList
  printLn !(objectToString max)

  -- static field getter
  caseInsensitiveComparator <- stringClass <.#!> "CASE_INSENSITIVE_ORDER"
  printLn !((comparatorClass <.!> "compare") caseInsensitiveComparator "Bar" "august")

  point <- (pointClass <.!> "<init>(int,int)") 2 3

  -- instance field getter
  printLn !((pointClass <.#> "x") point)

  -- instance field setter
  (pointClass <.=> "x") point 34
  printLn !((pointClass <.#> "x") point)


text:
module Main

import System
import System.File
import Language.JSON

import Ipkg.Types
import Ipkg.Parser

dependsObj : Depends -> JSON
dependsObj (D name (PVB lb li ub ui)) = JObject $ [("name", JString name)] ++
  (case lb of Nothing => []
              Just v => [ ("lowerBound", JString $ show v)
                        , ("lowerInclusive", JBoolean li) ]) ++
  (case ub of Nothing => []
              Just v => [ ("upperBound", JString $ show v)
                        , ("upperInclusive", JBoolean ui) ])

pkgToJSON : Package -> JSON
pkgToJSON (P name version misc depends modules) = JObject $
  [ ("name", JString name)
  , ("depends", JArray (map dependsObj depends))
  , ("version", maybe JNull (JString . show) version)
  , ("modules", JArray (map JString modules))
  ] ++ rest
  where rest : List (String, JSON)
        rest = mapSnd JString <$> misc

main : IO ()
main = do
  (_ :: fn :: []) <- getArgs
    | _ => putStrLn "Bad command line"
  Right s <- readFile fn
    | Left err => putStrLn $ show err
  let Right pkg = parsePkg s
     | Left err => putStrLn err
  printLn $ pkgToJSON pkg

max_stars_repo_name: claymager/ipkg-to-json

max_issues_repo_name: claymager/ipkg-to-json

max_forks_repo_name: claymager/ipkg-to-json


text:
module Crypto

import Control.Monad.State
import Crypto.RSA
import Crypto.Random
import Crypto.Random.C
import Crypto.AES.Common
import Crypto.AES.Small
import Crypto.AES.Big
import Crypto.Hash
import Crypto.Hash.HMAC
import Data.Vect
import Data.List1
import Utils.Bytes
import Utils.Misc

test_chacha : HasIO m => m ()
test_chacha = do
  drg <- new_chacha12_drg
  let a = evalState drg (random_bytes 1024)
  putStrLn $ show a

test_rsa : HasIO m => m Integer
test_rsa = do
  (pk, sk) <- generate_key_pair 1024
  let m = 42069
  let c = rsa_encrypt pk m
  rsa_decrypt_blinded sk c

test_aes_128_key : Vect 16 Bits8
test_aes_128_key =
  [ 0x2b, 0x7e, 0x15, 0x16, 0x28, 0xae, 0xd2, 0xa6, 0xab, 0xf7, 0x15, 0x88, 0x09, 0xcf, 0x4f, 0x3c ]

test_aes_192_key : Vect 24 Bits8
test_aes_192_key =
  [ 0x8e, 0x73, 0xb0, 0xf7, 0xda, 0x0e, 0x64, 0x52, 0xc8, 0x10, 0xf3, 0x2b, 0x80, 0x90, 0x79, 0xe5
  , 0x62, 0xf8, 0xea, 0xd2, 0x52, 0x2c, 0x6b, 0x7b ]

test_aes_256_key : Vect 32 Bits8
test_aes_256_key =
  [ 0x60, 0x3d, 0xeb, 0x10, 0x15, 0xca, 0x71, 0xbe, 0x2b, 0x73, 0xae, 0xf0, 0x85, 0x7d, 0x77, 0x81
  , 0x1f, 0x35, 0x2c, 0x07, 0x3b, 0x61, 0x08, 0xd7, 0x2d, 0x98, 0x10, 0xa3, 0x09, 0x14, 0xdf, 0xf4 ]

test_aes_plaintext : Vect 16 Bits8
test_aes_plaintext =
  [ 0x6b, 0xc1, 0xbe, 0xe2, 0x2e, 0x40, 0x9f, 0x96, 0xe9, 0x3d, 0x7e, 0x11, 0x73, 0x93, 0x17, 0x2a ]

test_aes_128_ciphertext : Vect 16 Bits8
test_aes_128_ciphertext =
  Small.encrypt_block AES128 test_aes_128_key test_aes_plaintext

test_aes_192_ciphertext : Vect 16 Bits8
test_aes_192_ciphertext =
  Small.encrypt_block AES192 test_aes_192_key test_aes_plaintext

test_aes_256_ciphertext : Vect 16 Bits8
test_aes_256_ciphertext =
  Small.encrypt_block AES256 test_aes_256_key test_aes_plaintext

test_aes_big_128_ciphertext : Vect 16 Bits8
test_aes_big_128_ciphertext =
  Big.encrypt_block AES128 test_aes_128_key test_aes_plaintext

test_aes_big_192_ciphertext : Vect 16 Bits8
test_aes_big_192_ciphertext =
  Big.encrypt_block AES192 test_aes_192_key test_aes_plaintext

test_aes_big_256_ciphertext : Vect 16 Bits8
test_aes_big_256_ciphertext =
  Big.encrypt_block AES256 test_aes_256_key test_aes_plaintext

||| test case where padding first bit would be set
test_rsa_pss : Maybe ()
test_rsa_pss =
  emsa_pss_verify {algo=Sha256}
    (mgf1 {algo=Sha256})
    32
    [ 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20
    , 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20
    , 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x20, 0x54, 0x4c
    , 0x53, 0x20, 0x31, 0x2e, 0x33, 0x2c, 0x20, 0x73, 0x65, 0x72, 0x76, 0x65, 0x72, 0x20, 0x43, 0x65, 0x72, 0x74, 0x69, 0x66, 0x69, 0x63
    , 0x61, 0x74, 0x65, 0x56, 0x65, 0x72, 0x69, 0x66, 0x79, 0x00, 0x8b, 0xea, 0x0f, 0x13, 0xa1, 0xa0, 0xa2, 0x30, 0xfc, 0x94, 0xe4, 0x21
    , 0xf1, 0x21, 0x3a, 0x4e, 0x00, 0xed, 0x45, 0x39, 0xe6, 0x49, 0x04, 0xfe, 0x98, 0x55, 0x0c, 0x97, 0xa0, 0xa3, 0xaf, 0x34, 0x64, 0xcf
    , 0xa0, 0x35, 0x36, 0xcf, 0x60, 0x0a, 0x2f, 0x1e, 0x04, 0xe7, 0x0d, 0xe6, 0x04, 0x6d ]
    (0x18 ::: [ 0xf9, 0x15, 0x8c, 0x76, 0x0d, 0x2d, 0x7f, 0x57, 0x36, 0x01, 0x8e, 0x89, 0x33, 0x92, 0xdc, 0x04, 0xb2, 0x02, 0x46, 0x30, 0x8b
    , 0x06, 0xc8, 0x65, 0x94, 0x71, 0xac, 0x3c, 0x6f, 0xe2, 0x71, 0x2b, 0x11, 0xe6, 0x4c, 0x7d, 0x11, 0x1f, 0x5a, 0x82, 0x20, 0x3c, 0x7c
    , 0x29, 0x83, 0x43, 0x1a, 0xcf, 0xd8, 0xc4, 0x4c, 0xad, 0xfc, 0x78, 0xf0, 0xef, 0x16, 0x1b, 0x24, 0xbf, 0xa5, 0x16, 0x8a, 0x47, 0xe7
    , 0x1d, 0x60, 0xd2, 0x6b, 0x08, 0xfa, 0x37, 0xdc, 0x76, 0x42, 0x88, 0x7c, 0xa5, 0x91, 0x97, 0x69, 0xa7, 0xd5, 0x50, 0x66, 0x09, 0xb6
    , 0x8a, 0x12, 0x76, 0x6e, 0xd1, 0xa6, 0xb0, 0x9e, 0x6d, 0xe6, 0xf2, 0x8a, 0x79, 0x4c, 0x68, 0x29, 0x52, 0xdb, 0x53, 0x36, 0x9b, 0x49
    , 0xed, 0x21, 0xf2, 0x48, 0x1d, 0x0e, 0x9f, 0x92, 0x23, 0x96, 0x0b, 0xc4, 0x47, 0x94, 0xb5, 0xec, 0x13, 0x40, 0x75, 0xde, 0x14, 0x9c
    , 0xa6, 0xa7, 0x2c, 0x9f, 0xbf, 0xe3, 0x94, 0xde, 0xeb, 0x49, 0xdc, 0x6a, 0xdc, 0x30, 0xa3, 0x0c, 0xf5, 0x2e, 0xe6, 0x14, 0x3f, 0xe2
    , 0x98, 0x27, 0x14, 0x8d, 0x21, 0x92, 0x20, 0xaa, 0xfb, 0x4e, 0x08, 0xa5, 0xd4, 0x7c, 0x8a, 0xf2, 0xed, 0x75, 0xa7, 0x6c, 0x01, 0xa4
    , 0x18, 0x4c, 0x58, 0x12, 0x10, 0xff, 0x2d, 0xc5, 0x0f, 0x8d, 0xe5, 0xab, 0x56, 0xa9, 0x81, 0x7c, 0x87, 0x4d, 0x19, 0xa4, 0x37, 0x96
    , 0x5d, 0x82, 0x84, 0xaa, 0x44, 0xc0, 0x7f, 0x4f, 0x39, 0xf4, 0x5d, 0x0d, 0xeb, 0xda, 0x3e, 0x2c, 0xd3, 0xaf, 0xe9, 0xf5, 0x24, 0x1e
    , 0x38, 0xb7, 0x35, 0x09, 0xda, 0x62, 0xc1, 0x3b, 0x89, 0x5c, 0xa9, 0xcc, 0x76, 0xe6, 0xed, 0x7f, 0xc6, 0xe0, 0x3a, 0x73, 0x94, 0x33
    , 0xca, 0x60, 0xf0, 0x15, 0xc7, 0x79, 0x62, 0x69, 0x68, 0x4d, 0xfd, 0x49, 0x98, 0xbc ])
    2047