text:
module Core.Primitives

import Core.Context
import Core.TT
import Core.Value
import Libraries.Utils.String

import Data.Vect

%default covering

public export
record Prim where
  constructor MkPrim
  {arity : Nat}
  fn : PrimFn arity
  type : ClosedTerm
  totality : Totality

binOp : (Constant -> Constant -> Maybe Constant) ->
        {vars : _} -> Vect 2 (NF vars) -> Maybe (NF vars)
binOp fn [NPrimVal fc x, NPrimVal _ y]
    = map (NPrimVal fc) (fn x y)
binOp _ _ = Nothing

unaryOp : (Constant -> Maybe Constant) ->
          {vars : _} -> Vect 1 (NF vars) -> Maybe (NF vars)
unaryOp fn [NPrimVal fc x]
    = map (NPrimVal fc) (fn x)
unaryOp _ _ = Nothing

castString : Vect 1 (NF vars) -> Maybe (NF vars)
castString [NPrimVal fc (I i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (I8 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (I16 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (I32 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (I64 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (BI i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (B8 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (B16 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (B32 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (B64 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (Ch i)] = Just (NPrimVal fc (Str (stripQuotes (show i))))
castString [NPrimVal fc (Db i)] = Just (NPrimVal fc (Str (show i)))
castString _ = Nothing

castInteger : Vect 1 (NF vars) -> Maybe (NF vars)
castInteger [NPrimVal fc (I i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (I8 i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (I16 i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (I32 i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (I64 i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (B8 i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (B16 i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (B32 i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (B64 i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (Ch i)] = Just (NPrimVal fc (BI (cast (cast {to=Int} i))))
castInteger [NPrimVal fc (Db i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (Str i)] = Just (NPrimVal fc (BI (cast i)))
castInteger _ = Nothing

castInt : Vect 1 (NF vars) -> Maybe (NF vars)
castInt [NPrimVal fc (I8 i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (I16 i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (I32 i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (I64 i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (BI i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (B8 i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (B16 i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (B32 i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (B64 i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (Db i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (Ch i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (Str i)] = Just (NPrimVal fc (I (cast i)))
castInt _ = Nothing

constantIntegerValue : Constant -> Maybe Integer
constantIntegerValue (I i)   = Just $ cast i
constantIntegerValue (I8 i)   = Just $ cast i
constantIntegerValue (I16 i)   = Just $ cast i
constantIntegerValue (I32 i)   = Just $ cast i
constantIntegerValue (I64 i)   = Just $ cast i
constantIntegerValue (BI i)  = Just i
constantIntegerValue (B8 i)  = Just $ cast i
constantIntegerValue (B16 i) = Just $ cast i
constantIntegerValue (B32 i) = Just $ cast i
constantIntegerValue (B64 i) = Just $ cast i
constantIntegerValue _       = Nothing

castBits8 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits8 [NPrimVal fc constant] =
    NPrimVal fc . B8 . cast <$> constantIntegerValue constant
castBits8 _ = Nothing

castBits16 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits16 [NPrimVal fc constant] =
    NPrimVal fc . B16 . cast <$> constantIntegerValue constant
castBits16 _ = Nothing

castBits32 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits32 [NPrimVal fc constant] =
    NPrimVal fc . B32 . cast <$> constantIntegerValue constant
castBits32 _ = Nothing

castBits64 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits64 [NPrimVal fc constant] =
    NPrimVal fc . B64 . cast <$> constantIntegerValue constant
castBits64 _ = Nothing

castInt8 : Vect 1 (NF vars) -> Maybe (NF vars)
castInt8 [NPrimVal fc constant] =
    NPrimVal fc . I8 . cast <$> constantIntegerValue constant
castInt8 _ = Nothing

castInt16 : Vect 1 (NF vars) -> Maybe (NF vars)
castInt16 [NPrimVal fc constant] =
    NPrimVal fc . I16 . cast <$> constantIntegerValue constant
castInt16 _ = Nothing

castInt32 : Vect 1 (NF vars) -> Maybe (NF vars)
castInt32 [NPrimVal fc constant] =
    NPrimVal fc . I32 . cast <$> constantIntegerValue constant
castInt32 _ = Nothing

castInt64 : Vect 1 (NF vars) -> Maybe (NF vars)
castInt64 [NPrimVal fc constant] =
    NPrimVal fc . I64 . cast <$> constantIntegerValue constant
castInt64 _ = Nothing

castDouble : Vect 1 (NF vars) -> Maybe (NF vars)
castDouble [NPrimVal fc (I i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (I8 i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (I16 i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (I32 i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (I64 i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (B8 i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (B16 i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (B32 i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (B64 i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (BI i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (Str i)] = Just (NPrimVal fc (Db (cast i)))
castDouble _ = Nothing

castChar : Vect 1 (NF vars) -> Maybe (NF vars)
castChar [NPrimVal fc (I i)] = Just (NPrimVal fc (Ch (cast i)))
castChar [NPrimVal fc (I8 i)] = Just (NPrimVal fc (Ch (cast i)))
castChar [NPrimVal fc (I16 i)] = Just (NPrimVal fc (Ch (cast i)))
castChar [NPrimVal fc (I32 i)] = Just (NPrimVal fc (Ch (cast i)))
castChar [NPrimVal fc (I64 i)] = Just (NPrimVal fc (Ch (cast i)))
castChar [NPrimVal fc (B8 i)] = Just (NPrimVal fc (Ch (cast i)))
castChar [NPrimVal fc (B16 i)] = Just (NPrimVal fc (Ch (cast i)))
castChar [NPrimVal fc (B32 i)] = Just (NPrimVal fc (Ch (cast i)))
castChar [NPrimVal fc (B64 i)] = Just (NPrimVal fc (Ch (cast i)))
castChar [NPrimVal fc (BI i)] = Just (NPrimVal fc (Ch (cast i)))
castChar _ = Nothing

strLength : Vect 1 (NF vars) -> Maybe (NF vars)
strLength [NPrimVal fc (Str s)] = Just (NPrimVal fc (I (cast (length s))))
strLength _ = Nothing

strHead : Vect 1 (NF vars) -> Maybe (NF vars)
strHead [NPrimVal fc (Str "")] = Nothing
strHead [NPrimVal fc (Str str)]
    = Just (NPrimVal fc (Ch (assert_total (prim__strHead str))))
strHead _ = Nothing

strTail : Vect 1 (NF vars) -> Maybe (NF vars)
strTail [NPrimVal fc (Str "")] = Nothing
strTail [NPrimVal fc (Str str)]
    = Just (NPrimVal fc (Str (assert_total (prim__strTail str))))
strTail _ = Nothing

strIndex : Vect 2 (NF vars) -> Maybe (NF vars)
strIndex [NPrimVal fc (Str str), NPrimVal _ (I i)]
    = if i >= 0 && integerToNat (cast i) < length str
         then Just (NPrimVal fc (Ch (assert_total (prim__strIndex str i))))
         else Nothing
strIndex _ = Nothing

strCons : Vect 2 (NF vars) -> Maybe (NF vars)
strCons [NPrimVal fc (Ch x), NPrimVal _ (Str y)]
    = Just (NPrimVal fc (Str (strCons x y)))
strCons _ = Nothing

strAppend : Vect 2 (NF vars) -> Maybe (NF vars)
strAppend [NPrimVal fc (Str x), NPrimVal _ (Str y)]
    = Just (NPrimVal fc (Str (x ++ y)))
strAppend _ = Nothing

strReverse : Vect 1 (NF vars) -> Maybe (NF vars)
strReverse [NPrimVal fc (Str x)]
    = Just (NPrimVal fc (Str (reverse x)))
strReverse _ = Nothing

strSubstr : Vect 3 (NF vars) -> Maybe (NF vars)
strSubstr [NPrimVal fc (I start), NPrimVal _ (I len), NPrimVal _ (Str str)]
    = Just (NPrimVal fc (Str (prim__strSubstr start len str)))
strSubstr _ = Nothing

add : Constant -> Constant -> Maybe Constant
add (BI x) (BI y) = pure $ BI (x + y)
add (I x) (I y) = pure $ I (x + y)
add (I8 x) (I8 y) = pure $ I8 (x + y)
add (I16 x) (I16 y) = pure $ I16 (x + y)
add (I32 x) (I32 y) = pure $ I32 (x + y)
add (I64 x) (I64 y) = pure $ I64 (x + y)
add (B8 x) (B8 y) = pure $ B8 (x + y)
add (B16 x) (B16 y) = pure $ B16 (x + y)
add (B32 x) (B32 y) = pure $ B32 (x + y)
add (B64 x) (B64 y) = pure $ B64 (x + y)
add (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x + cast y))
add (Db x) (Db y) = pure $ Db (x + y)
add _ _ = Nothing

sub : Constant -> Constant -> Maybe Constant
sub (BI x) (BI y) = pure $ BI (x - y)
sub (I x) (I y) = pure $ I (x - y)
sub (I8 x) (I8 y) = pure $ I8 (x - y)
sub (I16 x) (I16 y) = pure $ I16 (x - y)
sub (I32 x) (I32 y) = pure $ I32 (x - y)
sub (I64 x) (I64 y) = pure $ I64 (x - y)
sub (B8 x) (B8 y) = pure $ B8 (x - y)
sub (B16 x) (B16 y) = pure $ B16 (x - y)
sub (B32 x) (B32 y) = pure $ B32 (x - y)
sub (B64 x) (B64 y) = pure $ B64 (x - y)
sub (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x - cast y))
sub (Db x) (Db y) = pure $ Db (x - y)
sub _ _ = Nothing

mul : Constant -> Constant -> Maybe Constant
mul (BI x) (BI y) = pure $ BI (x * y)
mul (B8 x) (B8 y) = pure $ B8 (x * y)
mul (B16 x) (B16 y) = pure $ B16 (x * y)
mul (B32 x) (B32 y) = pure $ B32 (x * y)
mul (B64 x) (B64 y) = pure $ B64 (x * y)
mul (I x) (I y) = pure $ I (x * y)
mul (I8 x) (I8 y) = pure $ I8 (x * y)
mul (I16 x) (I16 y) = pure $ I16 (x * y)
mul (I32 x) (I32 y) = pure $ I32 (x * y)
mul (I64 x) (I64 y) = pure $ I64 (x * y)
mul (Db x) (Db y) = pure $ Db (x * y)
mul _ _ = Nothing

div : Constant -> Constant -> Maybe Constant
div (BI x) (BI 0) = Nothing
div (BI x) (BI y) = pure $ BI (assert_total (x `div` y))
div (I x) (I 0) = Nothing
div (I x) (I y) = pure $ I (assert_total (x `div` y))
div (I8 x) (I8 0) = Nothing
div (I8 x) (I8 y) = pure $ I8 (assert_total (x `div` y))
div (I16 x) (I16 0) = Nothing
div (I16 x) (I16 y) = pure $ I16 (assert_total (x `div` y))
div (I32 x) (I32 0) = Nothing
div (I32 x) (I32 y) = pure $ I32 (assert_total (x `div` y))
div (I64 x) (I64 0) = Nothing
div (I64 x) (I64 y) = pure $ I64 (assert_total (x `div` y))
div (B8 x) (B8 0) = Nothing
div (B8 x) (B8 y) = pure $ B8 (assert_total (x `div` y))
div (B16 x) (B16 0) = Nothing
div (B16 x) (B16 y) = pure $ B16 (assert_total (x `div` y))
div (B32 x) (B32 0) = Nothing
div (B32 x) (B32 y) = pure $ B32 (assert_total (x `div` y))
div (B64 x) (B64 0) = Nothing
div (B64 x) (B64 y) = pure $ B64 (assert_total (x `div` y))
div (Db x) (Db y) = pure $ Db (x / y)
div _ _ = Nothing

mod : Constant -> Constant -> Maybe Constant
mod (BI x) (BI 0) = Nothing
mod (BI x) (BI y) = pure $ BI (assert_total (x `mod` y))
mod (I x) (I 0) = Nothing
mod (I x) (I y) = pure $ I (assert_total (x `mod` y))
mod (I8 x) (I8 0) = Nothing
mod (I8 x) (I8 y) = pure $ I8 (assert_total (x `mod` y))
mod (I16 x) (I16 0) = Nothing
mod (I16 x) (I16 y) = pure $ I16 (assert_total (x `mod` y))
mod (I32 x) (I32 0) = Nothing
mod (I32 x) (I32 y) = pure $ I32 (assert_total (x `mod` y))
mod (I64 x) (I64 0) = Nothing
mod (I64 x) (I64 y) = pure $ I64 (assert_total (x `mod` y))
mod (B8 x) (B8 0) = Nothing
mod (B8 x) (B8 y) = pure $ B8 (assert_total (x `mod` y))
mod (B16 x) (B16 0) = Nothing
mod (B16 x) (B16 y) = pure $ B16 (assert_total (x `mod` y))
mod (B32 x) (B32 0) = Nothing
mod (B32 x) (B32 y) = pure $ B32 (assert_total (x `mod` y))
mod (B64 x) (B64 0) = Nothing
mod (B64 x) (B64 y) = pure $ B64 (assert_total (x `mod` y))
mod _ _ = Nothing

shiftl : Constant -> Constant -> Maybe Constant
shiftl (I x) (I y) = pure $ I (prim__shl_Int x y)
shiftl (I8 x) (I8 y) = pure $ I8 (prim__shl_Int8 x y)
shiftl (I16 x) (I16 y) = pure $ I16 (prim__shl_Int16 x y)
shiftl (I32 x) (I32 y) = pure $ I32 (prim__shl_Int32 x y)
shiftl (I64 x) (I64 y) = pure $ I64 (prim__shl_Int64 x y)
shiftl (BI x) (BI y) = pure $ BI (prim__shl_Integer x y)
shiftl (B8 x) (B8 y) = pure $ B8 (prim__shl_Bits8 x y)
shiftl (B16 x) (B16 y) = pure $ B16 (prim__shl_Bits16 x y)
shiftl (B32 x) (B32 y) = pure $ B32 (prim__shl_Bits32 x y)
shiftl (B64 x) (B64 y) = pure $ B64 (prim__shl_Bits64 x y)
shiftl _ _ = Nothing

shiftr : Constant -> Constant -> Maybe Constant
shiftr (I x) (I y) = pure $ I (prim__shr_Int x y)
shiftr (I8 x) (I8 y) = pure $ I8 (prim__shr_Int8 x y)
shiftr (I16 x) (I16 y) = pure $ I16 (prim__shr_Int16 x y)
shiftr (I32 x) (I32 y) = pure $ I32 (prim__shr_Int32 x y)
shiftr (I64 x) (I64 y) = pure $ I64 (prim__shr_Int64 x y)
shiftr (B8 x) (B8 y) = pure $ B8 $ (prim__shr_Bits8 x y)
shiftr (B16 x) (B16 y) = pure $ B16 (prim__shr_Bits16 x y)
shiftr (B32 x) (B32 y) = pure $ B32 (prim__shr_Bits32 x y)
shiftr (B64 x) (B64 y) = pure $ B64 (prim__shr_Bits64 x y)
shiftr _ _ = Nothing

band : Constant -> Constant -> Maybe Constant
band (I x) (I y) = pure $ I (prim__and_Int x y)
band (I8 x) (I8 y) = pure $ I8 (prim__and_Int8 x y)
band (I16 x) (I16 y) = pure $ I16 (prim__and_Int16 x y)
band (I32 x) (I32 y) = pure $ I32 (prim__and_Int32 x y)
band (I64 x) (I64 y) = pure $ I64 (prim__and_Int64 x y)
band (BI x) (BI y) = pure $ BI (prim__and_Integer x y)
band (B8 x) (B8 y) = pure $ B8 (prim__and_Bits8 x y)
band (B16 x) (B16 y) = pure $ B16 (prim__and_Bits16 x y)
band (B32 x) (B32 y) = pure $ B32 (prim__and_Bits32 x y)
band (B64 x) (B64 y) = pure $ B64 (prim__and_Bits64 x y)
band _ _ = Nothing

bor : Constant -> Constant -> Maybe Constant
bor (I x) (I y) = pure $ I (prim__or_Int x y)
bor (I8 x) (I8 y) = pure $ I8 (prim__or_Int8 x y)
bor (I16 x) (I16 y) = pure $ I16 (prim__or_Int16 x y)
bor (I32 x) (I32 y) = pure $ I32 (prim__or_Int32 x y)
bor (I64 x) (I64 y) = pure $ I64 (prim__or_Int64 x y)
bor (BI x) (BI y) = pure $ BI (prim__or_Integer x y)
bor (B8 x) (B8 y) = pure $ B8 (prim__or_Bits8 x y)
bor (B16 x) (B16 y) = pure $ B16 (prim__or_Bits16 x y)
bor (B32 x) (B32 y) = pure $ B32 (prim__or_Bits32 x y)
bor (B64 x) (B64 y) = pure $ B64 (prim__or_Bits64 x y)
bor _ _ = Nothing

bxor : Constant -> Constant -> Maybe Constant
bxor (I x) (I y) = pure $ I (prim__xor_Int x y)
bxor (B8 x) (B8 y) = pure $ B8 (prim__xor_Bits8 x y)
bxor (B16 x) (B16 y) = pure $ B16 (prim__xor_Bits16 x y)
bxor (B32 x) (B32 y) = pure $ B32 (prim__xor_Bits32 x y)
bxor (B64 x) (B64 y) = pure $ B64 (prim__xor_Bits64 x y)
bxor (I8 x) (I8 y) = pure $ I8 (prim__xor_Int8 x y)
bxor (I16 x) (I16 y) = pure $ I16 (prim__xor_Int16 x y)
bxor (I32 x) (I32 y) = pure $ I32 (prim__xor_Int32 x y)
bxor (I64 x) (I64 y) = pure $ I64 (prim__xor_Int64 x y)
bxor (BI x) (BI y) = pure $ BI (prim__xor_Integer x y)
bxor _ _ = Nothing

neg : Constant -> Maybe Constant
neg (BI x) = pure $ BI (-x)
neg (I x) = pure $ I (-x)
neg (I8 x) = pure $ I8 (-x)
neg (I16 x) = pure $ I16 (-x)
neg (I32 x) = pure $ I32 (-x)
neg (I64 x) = pure $ I64 (-x)
neg (B8 x) = pure $ B8 (-x)
neg (B16 x) = pure $ B16 (-x)
neg (B32 x) = pure $ B32 (-x)
neg (B64 x) = pure $ B64 (-x)
neg (Db x) = pure $ Db (-x)
neg _ = Nothing

toInt : Bool -> Constant
toInt True = I 1
toInt False = I 0

lt : Constant -> Constant -> Maybe Constant
lt (I x) (I y) = pure $ toInt (x < y)
lt (I8 x) (I8 y) = pure $ toInt (x < y)
lt (I16 x) (I16 y) = pure $ toInt (x < y)
lt (I32 x) (I32 y) = pure $ toInt (x < y)
lt (I64 x) (I64 y) = pure $ toInt (x < y)
lt (BI x) (BI y) = pure $ toInt (x < y)
lt (B8 x) (B8 y) = pure $ toInt (x < y)
lt (B16 x) (B16 y) = pure $ toInt (x < y)
lt (B32 x) (B32 y) = pure $ toInt (x < y)
lt (B64 x) (B64 y) = pure $ toInt (x < y)
lt (Str x) (Str y) = pure $ toInt (x < y)
lt (Ch x) (Ch y) = pure $ toInt (x < y)
lt (Db x) (Db y) = pure $ toInt (x < y)
lt _ _ = Nothing

lte : Constant -> Constant -> Maybe Constant
lte (I x) (I y) = pure $ toInt (x <= y)
lte (I8 x) (I8 y) = pure $ toInt (x <= y)
lte (I16 x) (I16 y) = pure $ toInt (x <= y)
lte (I32 x) (I32 y) = pure $ toInt (x <= y)
lte (I64 x) (I64 y) = pure $ toInt (x <= y)
lte (BI x) (BI y) = pure $ toInt (x <= y)
lte (B8 x) (B8 y) = pure $ toInt (x <= y)
lte (B16 x) (B16 y) = pure $ toInt (x <= y)
lte (B32 x) (B32 y) = pure $ toInt (x <= y)
lte (B64 x) (B64 y) = pure $ toInt (x <= y)
lte (Str x) (Str y) = pure $ toInt (x <= y)
lte (Ch x) (Ch y) = pure $ toInt (x <= y)
lte (Db x) (Db y) = pure $ toInt (x <= y)
lte _ _ = Nothing

eq : Constant -> Constant -> Maybe Constant
eq (I x) (I y) = pure $ toInt (x == y)
eq (I8 x) (I8 y) = pure $ toInt (x == y)
eq (I16 x) (I16 y) = pure $ toInt (x == y)
eq (I32 x) (I32 y) = pure $ toInt (x == y)
eq (I64 x) (I64 y) = pure $ toInt (x == y)
eq (BI x) (BI y) = pure $ toInt (x == y)
eq (B8 x) (B8 y) = pure $ toInt (x == y)
eq (B16 x) (B16 y) = pure $ toInt (x == y)
eq (B32 x) (B32 y) = pure $ toInt (x == y)
eq (B64 x) (B64 y) = pure $ toInt (x == y)
eq (Str x) (Str y) = pure $ toInt (x == y)
eq (Ch x) (Ch y) = pure $ toInt (x == y)
eq (Db x) (Db y) = pure $ toInt (x == y)
eq _ _ = Nothing

gte : Constant -> Constant -> Maybe Constant
gte (I x) (I y) = pure $ toInt (x >= y)
gte (I8 x) (I8 y) = pure $ toInt (x >= y)
gte (I16 x) (I16 y) = pure $ toInt (x >= y)
gte (I32 x) (I32 y) = pure $ toInt (x >= y)
gte (I64 x) (I64 y) = pure $ toInt (x >= y)
gte (BI x) (BI y) = pure $ toInt (x >= y)
gte (B8 x) (B8 y) = pure $ toInt (x >= y)
gte (B16 x) (B16 y) = pure $ toInt (x >= y)
gte (B32 x) (B32 y) = pure $ toInt (x >= y)
gte (B64 x) (B64 y) = pure $ toInt (x >= y)
gte (Str x) (Str y) = pure $ toInt (x >= y)
gte (Ch x) (Ch y) = pure $ toInt (x >= y)
gte (Db x) (Db y) = pure $ toInt (x >= y)
gte _ _ = Nothing

gt : Constant -> Constant -> Maybe Constant
gt (I x) (I y) = pure $ toInt (x > y)
gt (I8 x) (I8 y) = pure $ toInt (x > y)
gt (I16 x) (I16 y) = pure $ toInt (x > y)
gt (I32 x) (I32 y) = pure $ toInt (x > y)
gt (I64 x) (I64 y) = pure $ toInt (x > y)
gt (BI x) (BI y) = pure $ toInt (x > y)
gt (B8 x) (B8 y) = pure $ toInt (x > y)
gt (B16 x) (B16 y) = pure $ toInt (x > y)
gt (B32 x) (B32 y) = pure $ toInt (x > y)
gt (B64 x) (B64 y) = pure $ toInt (x > y)
gt (Str x) (Str y) = pure $ toInt (x > y)
gt (Ch x) (Ch y) = pure $ toInt (x > y)
gt (Db x) (Db y) = pure $ toInt (x > y)
gt _ _ = Nothing

doubleOp : (Double -> Double) -> Vect 1 (NF vars) -> Maybe (NF vars)
doubleOp f [NPrimVal fc (Db x)] = Just (NPrimVal fc (Db (f x)))
doubleOp f _ = Nothing

doubleExp : Vect 1 (NF vars) -> Maybe (NF vars)
doubleExp = doubleOp exp

doubleLog : Vect 1 (NF vars) -> Maybe (NF vars)
doubleLog = doubleOp log

doublePow : {vars : _ } -> Vect 2 (NF vars) -> Maybe (NF vars)
doublePow = binOp pow'
    where pow' : Constant -> Constant -> Maybe Constant
          pow' (Db x) (Db y) = pure $ Db (pow x y)
          pow' _ _ = Nothing

doubleSin : Vect 1 (NF vars) -> Maybe (NF vars)
doubleSin = doubleOp sin

doubleCos : Vect 1 (NF vars) -> Maybe (NF vars)
doubleCos = doubleOp cos

doubleTan : Vect 1 (NF vars) -> Maybe (NF vars)
doubleTan = doubleOp tan

doubleASin : Vect 1 (NF vars) -> Maybe (NF vars)
doubleASin = doubleOp asin

doubleACos : Vect 1 (NF vars) -> Maybe (NF vars)
doubleACos = doubleOp acos

doubleATan : Vect 1 (NF vars) -> Maybe (NF vars)
doubleATan = doubleOp atan

doubleSqrt : Vect 1 (NF vars) -> Maybe (NF vars)
doubleSqrt = doubleOp sqrt

doubleFloor : Vect 1 (NF vars) -> Maybe (NF vars)
doubleFloor = doubleOp floor

doubleCeiling : Vect 1 (NF vars) -> Maybe (NF vars)
doubleCeiling = doubleOp ceiling

-- Only reduce for concrete values
believeMe : Vect 3 (NF vars) -> Maybe (NF vars)
believeMe [_, _, val@(NDCon _ _ _ _ _)] = Just val
believeMe [_, _, val@(NTCon _ _ _ _ _)] = Just val
believeMe [_, _, val@(NPrimVal _ _)] = Just val
believeMe [_, _, NType fc u] = Just (NType fc u)
believeMe [_, _, val] = Nothing

constTy : Constant -> Constant -> Constant -> ClosedTerm
constTy a b c
    = let arr = fnType emptyFC in
    PrimVal emptyFC a `arr` (PrimVal emptyFC b `arr` PrimVal emptyFC c)

constTy3 : Constant -> Constant -> Constant -> Constant -> ClosedTerm
constTy3 a b c d
    = let arr = fnType emptyFC in
    PrimVal emptyFC a `arr`
         (PrimVal emptyFC b `arr`
             (PrimVal emptyFC c `arr` PrimVal emptyFC d))

predTy : Constant -> Constant -> ClosedTerm
predTy a b = let arr = fnType emptyFC in
             PrimVal emptyFC a `arr` PrimVal emptyFC b

arithTy : Constant -> ClosedTerm
arithTy t = constTy t t t

cmpTy : Constant -> ClosedTerm
cmpTy t = constTy t t IntType

doubleTy : ClosedTerm
doubleTy = predTy DoubleType DoubleType

pi : (x : String) -> RigCount -> PiInfo (Term xs) -> Term xs ->
     Term (UN (Basic x) :: xs) -> Term xs
pi x rig plic ty sc = Bind emptyFC (UN (Basic x)) (Pi emptyFC rig plic ty) sc

believeMeTy : ClosedTerm
believeMeTy
    = pi "a" erased Explicit (TType emptyFC (MN "top" 0)) $
      pi "b" erased Explicit (TType emptyFC (MN "top" 0)) $
      pi "x" linear Explicit (Local emptyFC Nothing _ (Later First)) $
      Local emptyFC Nothing _ (Later First)

crashTy : ClosedTerm
crashTy
    = pi "a" erased Explicit (TType emptyFC (MN "top" 0)) $
      pi "msg" top Explicit (PrimVal emptyFC StringType) $
      Local emptyFC Nothing _ (Later First)

castTo : Constant -> Vect 1 (NF vars) -> Maybe (NF vars)
castTo IntType = castInt
castTo Int8Type = castInt8
castTo Int16Type = castInt16
castTo Int32Type = castInt32
castTo Int64Type = castInt64
castTo IntegerType = castInteger
castTo Bits8Type = castBits8
castTo Bits16Type = castBits16
castTo Bits32Type = castBits32
castTo Bits64Type = castBits64
castTo StringType = castString
castTo CharType = castChar
castTo DoubleType = castDouble
castTo _ = const Nothing

export
getOp : {0 arity : Nat} -> PrimFn arity ->
        {vars : List Name} -> Vect arity (NF vars) -> Maybe (NF vars)
getOp (Add ty) = binOp add
getOp (Sub ty) = binOp sub
getOp (Mul ty) = binOp mul
getOp (Div ty) = binOp div
getOp (Mod ty) = binOp mod
getOp (Neg ty) = unaryOp neg
getOp (ShiftL ty) = binOp shiftl
getOp (ShiftR ty) = binOp shiftr

getOp (BAnd ty) = binOp band
getOp (BOr ty) = binOp bor
getOp (BXOr ty) = binOp bxor

getOp (LT ty) = binOp lt
getOp (LTE ty) = binOp lte
getOp (EQ ty) = binOp eq
getOp (GTE ty) = binOp gte
getOp (GT ty) = binOp gt

getOp StrLength = strLength
getOp StrHead = strHead
getOp StrTail = strTail
getOp StrIndex = strIndex
getOp StrCons = strCons
getOp StrAppend = strAppend
getOp StrReverse = strReverse
getOp StrSubstr = strSubstr

getOp DoubleExp = doubleExp
getOp DoubleLog = doubleLog
getOp DoublePow = doublePow
getOp DoubleSin = doubleSin
getOp DoubleCos = doubleCos
getOp DoubleTan = doubleTan
getOp DoubleASin = doubleASin
getOp DoubleACos = doubleACos
getOp DoubleATan = doubleATan
getOp DoubleSqrt = doubleSqrt
getOp DoubleFloor = doubleFloor
getOp DoubleCeiling = doubleCeiling

getOp (Cast _ y) = castTo y
getOp BelieveMe = believeMe

getOp _ = const Nothing

prim : String -> Name
prim str = UN $ Basic $ "prim__" ++ str

export
opName : {0 arity : Nat} -> PrimFn arity -> Name
opName (Add ty) = prim $ "add_" ++ show ty
opName (Sub ty) = prim $ "sub_" ++ show ty
opName (Mul ty) = prim $ "mul_" ++ show ty
opName (Div ty) = prim $ "div_" ++ show ty
opName (Mod ty) = prim $ "mod_" ++ show ty
opName (Neg ty) = prim $ "negate_" ++ show ty
opName (ShiftL ty) = prim $ "shl_" ++ show ty
opName (ShiftR ty) = prim $ "shr_" ++ show ty
opName (BAnd ty) = prim $ "and_" ++ show ty
opName (BOr ty) = prim $ "or_" ++ show ty
opName (BXOr ty) = prim $ "xor_" ++ show ty
opName (LT ty) = prim $ "lt_" ++ show ty
opName (LTE ty) = prim $ "lte_" ++ show ty
opName (EQ ty) = prim $ "eq_" ++ show ty
opName (GTE ty) = prim $ "gte_" ++ show ty
opName (GT ty) = prim $ "gt_" ++ show ty
opName StrLength = prim "strLength"
opName StrHead = prim "strHead"
opName StrTail = prim "strTail"
opName StrIndex = prim "strIndex"
opName StrCons = prim "strCons"
opName StrAppend = prim "strAppend"
opName StrReverse = prim "strReverse"
opName StrSubstr = prim "strSubstr"
opName DoubleExp = prim "doubleExp"
opName DoubleLog = prim "doubleLog"
opName DoublePow = prim "doublePow"
opName DoubleSin = prim "doubleSin"
opName DoubleCos = prim "doubleCos"
opName DoubleTan = prim "doubleTan"
opName DoubleASin = prim "doubleASin"
opName DoubleACos = prim "doubleACos"
opName DoubleATan = prim "doubleATan"
opName DoubleSqrt = prim "doubleSqrt"
opName DoubleFloor = prim "doubleFloor"
opName DoubleCeiling = prim "doubleCeiling"
opName (Cast x y) = prim $ "cast_" ++ show x ++ show y
opName BelieveMe = prim $ "believe_me"
opName Crash = prim $ "crash"

integralTypes : List Constant
integralTypes = [ IntType
                , Int8Type
                , Int16Type
                , Int32Type
                , Int64Type
                , IntegerType
                , Bits8Type
                , Bits16Type
                , Bits32Type
                , Bits64Type
                ]

numTypes : List Constant
numTypes = integralTypes ++ [DoubleType]

primTypes : List Constant
primTypes = numTypes ++ [StringType, CharType]

export
allPrimitives : List Prim
allPrimitives =
    map (\t => MkPrim (Add t) (arithTy t) isTotal)     numTypes ++
    map (\t => MkPrim (Sub t) (arithTy t) isTotal)     numTypes ++
    map (\t => MkPrim (Mul t) (arithTy t) isTotal)     numTypes ++
    map (\t => MkPrim (Neg t) (predTy t t) isTotal)    numTypes ++
    map (\t => MkPrim (Div t) (arithTy t) notCovering) numTypes ++
    map (\t => MkPrim (Mod t) (arithTy t) notCovering) integralTypes ++

    map (\t => MkPrim (ShiftL t) (arithTy t) isTotal)  integralTypes ++
    map (\t => MkPrim (ShiftR t) (arithTy t) isTotal)  integralTypes ++
    map (\t => MkPrim (BAnd t) (arithTy t) isTotal)    integralTypes ++
    map (\t => MkPrim (BOr t) (arithTy t) isTotal)     integralTypes ++
    map (\t => MkPrim (BXOr t) (arithTy t) isTotal)    integralTypes ++

    map (\t => MkPrim (LT t) (cmpTy t) isTotal)  primTypes ++
    map (\t => MkPrim (LTE t) (cmpTy t) isTotal) primTypes ++
    map (\t => MkPrim (EQ t) (cmpTy t) isTotal)  primTypes ++
    map (\t => MkPrim (GTE t) (cmpTy t) isTotal) primTypes ++
    map (\t => MkPrim (GT t) (cmpTy t) isTotal)  primTypes ++

    [MkPrim StrLength (predTy StringType IntType) isTotal,
     MkPrim StrHead (predTy StringType CharType) notCovering,
     MkPrim StrTail (predTy StringType StringType) notCovering,
     MkPrim StrIndex (constTy StringType IntType CharType) notCovering,
     MkPrim StrCons (constTy CharType StringType StringType) isTotal,
     MkPrim StrAppend (arithTy StringType) isTotal,
     MkPrim StrReverse (predTy StringType StringType) isTotal,
     MkPrim StrSubstr (constTy3 IntType IntType StringType StringType) isTotal,
     MkPrim BelieveMe believeMeTy isTotal,
     MkPrim Crash crashTy notCovering] ++

    [MkPrim DoubleExp doubleTy isTotal,
     MkPrim DoubleLog doubleTy isTotal,
     MkPrim DoublePow (arithTy DoubleType) isTotal,
     MkPrim DoubleSin doubleTy isTotal,
     MkPrim DoubleCos doubleTy isTotal,
     MkPrim DoubleTan doubleTy isTotal,
     MkPrim DoubleASin doubleTy isTotal,
     MkPrim DoubleACos doubleTy isTotal,
     MkPrim DoubleATan doubleTy isTotal,
     MkPrim DoubleSqrt doubleTy isTotal,
     MkPrim DoubleFloor doubleTy isTotal,
     MkPrim DoubleCeiling doubleTy isTotal] ++

    -- support all combinations of primitive casts with the following
    -- exceptions: String -> Char, Double -> Char, Char -> Double
    [ MkPrim (Cast t1 t2) (predTy t1 t2) isTotal
    | t1 <- primTypes
    , t2 <- primTypes
    , t1 /= t2                         &&
      (t1,t2) /= (StringType,CharType) &&
      (t1,t2) /= (DoubleType,CharType) &&
      (t1,t2) /= (CharType,DoubleType)
    ]


text:
module JS.Any

import JS.Inheritance
import JS.Marshall

public export
record Any where
  constructor MkAny
  value : tpe

export
ToFFI Any AnyPtr where
  toFFI (MkAny v) = believe_me v

export
FromFFI Any AnyPtr where
  fromFFI = Just . MkAny

export
SafeCast Any where
  safeCast = Just . MkAny

ext: idr


text:
module Markdown.Lexer

import Data.List1

import Text.Lexer
import Text.Token
import Text.Bounded

import Markdown.String
import public Markdown.Tokens

%default total

private
markdownTokenMap : TokenMap MarkdownToken
markdownTokenMap = toTokenMap $
  [ (codeFence, MdCodeBlock)
  , (pre, MdPre)
  , (headingSym, HeadingSym)
  , (italicsSym, ItalicsSym)
  , (boldSym, BoldSym)
  , (imageSym, ImageSym)
  , (link, MdLink)
  , (htmlCloseTag, HtmlCloseTag)
  , (htmlOpenTag, HtmlOpenTag)
  , (newLine, NewLine)
  , (text, MdText)
  ]

||| Combine consecutive `MdText` nodes into one
combineText : List (WithBounds MarkdownToken) -> List (WithBounds MarkdownToken)
combineText [] = []
combineText (el :: rest) =
  let
    init = (List1.singleton el, el)
  in
    forget $ reverse $ fst $ (foldl accumulate init rest)
  where
    accumulate : (List1 $ WithBounds MarkdownToken, WithBounds MarkdownToken) -> WithBounds MarkdownToken -> (List1 $ WithBounds MarkdownToken, WithBounds MarkdownToken)
    accumulate (acc0 ::: acc1, last) el =
      case (last, el) of
        ( (MkBounded (Tok MdText a) isIrr (MkBounds startLine startCol _ _)),
          (MkBounded (Tok MdText b) _     (MkBounds _ _ endLine endCol)))
          => let
               combined = (MkBounded (Tok MdText (a ++ b)) isIrr (MkBounds startLine startCol endLine endCol))
             in (combined ::: acc1, combined)
        _ =>
          (el ::: acc0 :: acc1, el)

public export
lexMarkdown : String -> Maybe (List $ WithBounds MarkdownToken)
lexMarkdown str
  = case lex markdownTokenMap str of
         (tokens, _, _, "") => Just $ combineText $ tokens
         _ => Nothing

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import Drahko

main : Promise ()
main = msgBox "Hello world!"

max_stars_repo_name: NickSeagull/idris-autohotkey

max_issues_repo_name: NickSeagull/idris-autohotkey

max_forks_repo_name: drahko/drahko


text:
module Text.Html.Node

import Data.List.TR
import Data.String
import Text.Html.Attribute
import Text.Html.Event
import Web.Dom

%hide Web.Internal.DomTypes.Node

%default total

public export
data Node : (event : Type) -> Type where
  El   :  {0 ev, el : Type}
       -> {tag : String}
       -> (tpe : ElementType tag el)
       -> List (Attribute ev)
       -> List (Node ev)
       -> Node ev

  Raw  : String -> Node ev

  Text : String -> Node ev

public export %inline
FromString (Node ev) where
  fromString = Text

public export %inline
a : List (Attribute ev) -> List (Node ev) -> Node ev
a = El A

public export %inline
address : List (Attribute ev) -> List (Node ev) -> Node ev
address = El Address

public export %inline
area : List (Attribute ev) -> List (Node ev) -> Node ev
area = El Area

public export %inline
article : List (Attribute ev) -> List (Node ev) -> Node ev
article = El Article

public export %inline
audio : List (Attribute ev) -> List (Node ev) -> Node ev
audio = El Audio

public export %inline
base : List (Attribute ev) -> List (Node ev) -> Node ev
base = El Base

public export %inline
blockquote : List (Attribute ev) -> List (Node ev) -> Node ev
blockquote = El Blockquote

public export %inline
body : List (Attribute ev) -> List (Node ev) -> Node ev
body = El Body

public export %inline
br : List (Attribute ev) -> List (Node ev) -> Node ev
br = El Br

public export %inline
button : List (Attribute ev) -> List (Node ev) -> Node ev
button = El Button

public export %inline
canvas : List (Attribute ev) -> List (Node ev) -> Node ev
canvas = El Canvas

public export %inline
caption : List (Attribute ev) -> List (Node ev) -> Node ev
caption = El Caption

public export %inline
col : List (Attribute ev) -> List (Node ev) -> Node ev
col = El Col

public export %inline
colgroup : List (Attribute ev) -> List (Node ev) -> Node ev
colgroup = El Colgroup

public export %inline
data_ : List (Attribute ev) -> List (Node ev) -> Node ev
data_ = El Data

public export %inline
datalist : List (Attribute ev) -> List (Node ev) -> Node ev
datalist = El Datalist

public export %inline
del : List (Attribute ev) -> List (Node ev) -> Node ev
del = El Del

public export %inline
details : List (Attribute ev) -> List (Node ev) -> Node ev
details = El Details

public export %inline
dialog : List (Attribute ev) -> List (Node ev) -> Node ev
dialog = El Dialog

public export %inline
div : List (Attribute ev) -> List (Node ev) -> Node ev
div = El Div

public export %inline
dl : List (Attribute ev) -> List (Node ev) -> Node ev
dl = El Dl

public export %inline
embed : List (Attribute ev) -> List (Node ev) -> Node ev
embed = El Embed

public export %inline
fieldset : List (Attribute ev) -> List (Node ev) -> Node ev
fieldset = El FieldSet

public export %inline
footer : List (Attribute ev) -> List (Node ev) -> Node ev
footer = El Footer

public export %inline
form : List (Attribute ev) -> List (Node ev) -> Node ev
form = El Form

public export %inline
h1 : List (Attribute ev) -> List (Node ev) -> Node ev
h1 = El H1

public export %inline
h2 : List (Attribute ev) -> List (Node ev) -> Node ev
h2 = El H2

public export %inline
h3 : List (Attribute ev) -> List (Node ev) -> Node ev
h3 = El H3

public export %inline
h4 : List (Attribute ev) -> List (Node ev) -> Node ev
h4 = El H4

public export %inline
h5 : List (Attribute ev) -> List (Node ev) -> Node ev
h5 = El H5

public export %inline
h6 : List (Attribute ev) -> List (Node ev) -> Node ev
h6 = El H6

public export %inline
header : List (Attribute ev) -> List (Node ev) -> Node ev
header = El Header

public export %inline
hr : List (Attribute ev) -> List (Node ev) -> Node ev
hr = El HR

public export %inline
html : List (Attribute ev) -> List (Node ev) -> Node ev
html = El Html

public export %inline
iframe : List (Attribute ev) -> List (Node ev) -> Node ev
iframe = El IFrame

public export %inline
img : List (Attribute ev) -> List (Node ev) -> Node ev
img = El Img

public export %inline
input : List (Attribute ev) -> List (Node ev) -> Node ev
input = El Input

public export %inline
ins : List (Attribute ev) -> List (Node ev) -> Node ev
ins = El Ins

public export %inline
label : List (Attribute ev) -> List (Node ev) -> Node ev
label = El Label

public export %inline
legend : List (Attribute ev) -> List (Node ev) -> Node ev
legend = El Legend

public export %inline
li : List (Attribute ev) -> List (Node ev) -> Node ev
li = El Li

public export %inline
link : List (Attribute ev) -> List (Node ev) -> Node ev
link = El Link

public export %inline
map : List (Attribute ev) -> List (Node ev) -> Node ev
map = El Map

public export %inline
menu : List (Attribute ev) -> List (Node ev) -> Node ev
menu = El Menu

public export %inline
meta : List (Attribute ev) -> List (Node ev) -> Node ev
meta = El Meta

public export %inline
meter : List (Attribute ev) -> List (Node ev) -> Node ev
meter = El Meter

public export %inline
object : List (Attribute ev) -> List (Node ev) -> Node ev
object = El Object

public export %inline
ol : List (Attribute ev) -> List (Node ev) -> Node ev
ol = El Ol

public export %inline
optgroup : List (Attribute ev) -> List (Node ev) -> Node ev
optgroup = El OptGroup

public export %inline
option : List (Attribute ev) -> List (Node ev) -> Node ev
option = El Option

public export %inline
output : List (Attribute ev) -> List (Node ev) -> Node ev
output = El Output

public export %inline
p : List (Attribute ev) -> List (Node ev) -> Node ev
p = El P

public export %inline
param : List (Attribute ev) -> List (Node ev) -> Node ev
param = El Param

public export %inline
picture : List (Attribute ev) -> List (Node ev) -> Node ev
picture = El Picture

public export %inline
pre : List (Attribute ev) -> List (Node ev) -> Node ev
pre = El Pre

public export %inline
progress : List (Attribute ev) -> List (Node ev) -> Node ev
progress = El Progress

public export %inline
q : List (Attribute ev) -> List (Node ev) -> Node ev
q = El Q

public export %inline
script : List (Attribute ev) -> List (Node ev) -> Node ev
script = El Script

public export %inline
section : List (Attribute ev) -> List (Node ev) -> Node ev
section = El Section

public export %inline
select : List (Attribute ev) -> List (Node ev) -> Node ev
select = El Select

public export %inline
slot : List (Attribute ev) -> List (Node ev) -> Node ev
slot = El Slot

public export %inline
source : List (Attribute ev) -> List (Node ev) -> Node ev
source = El Source

public export %inline
span : List (Attribute ev) -> List (Node ev) -> Node ev
span = El Span

public export %inline
style : List (Attribute ev) -> List (Node ev) -> Node ev
style = El Style

public export %inline
table : List (Attribute ev) -> List (Node ev) -> Node ev
table = El Table

public export %inline
tbody : List (Attribute ev) -> List (Node ev) -> Node ev
tbody = El Tbody

public export %inline
td : List (Attribute ev) -> List (Node ev) -> Node ev
td = El Td

public export %inline
template : List (Attribute ev) -> List (Node ev) -> Node ev
template = El Template

public export %inline
textarea : List (Attribute ev) -> List (Node ev) -> Node ev
textarea = El TextArea

public export %inline
tfoot : List (Attribute ev) -> List (Node ev) -> Node ev
tfoot = El Tfoot

public export %inline
th : List (Attribute ev) -> List (Node ev) -> Node ev
th = El Th

public export %inline
thead : List (Attribute ev) -> List (Node ev) -> Node ev
thead = El Thead

public export %inline
time : List (Attribute ev) -> List (Node ev) -> Node ev
time = El Time

public export %inline
title : List (Attribute ev) -> List (Node ev) -> Node ev
title = El Title

public export %inline
tr : List (Attribute ev) -> List (Node ev) -> Node ev
tr = El Tr

public export %inline
track : List (Attribute ev) -> List (Node ev) -> Node ev
track = El Track

public export %inline
ul : List (Attribute ev) -> List (Node ev) -> Node ev
ul = El Ul

public export %inline
video : List (Attribute ev) -> List (Node ev) -> Node ev
video = El Video

--------------------------------------------------------------------------------
--          Rendering Html
--------------------------------------------------------------------------------

export
escape : String -> String
escape = fastConcat . mapTR esc . unpack
  where esc : Char -> String
        esc '<'          = "<"
        esc '>'          = ">"
        esc '&'          = "&"
        esc '"'          = """
        esc '\''         = "&#x27"
        esc '\n'         = "\n"
        esc '\r'         = "\r"
        esc '\t'         = "\t"
        esc c            = if c < ' ' then "" else singleton c

attrs : List (Attribute ev) -> String
attrs as = let s = displayAttributes as in if null s then "" else " " ++ s

export
render : Node ev -> String
render n = case n of
  Raw x             => x
  Text x            => escape x
  El {tag} _ as ns  => #"<\#{tag}\#{attrs as}>\#{go Nil ns}</\#{tag}>"#

  where go : List String -> List (Node ev) -> String
        go ss (n :: ns) = go (render n :: ss) ns
        go ss []        = fastConcat $ reverse ss

export
renderMany : List (Node ev) -> String
renderMany = fastConcat . mapTR render


text:
module Network.ST.IOUtils

import Control.ST
import Network.ST.TcpSockets
import Data.Nat.NatTheorems
import Data.Bool.BoolTheorems

export
writeSocketFully : {m : Type -> Type} ->
                   {auto tcpSocketInstance : TcpSockets m} ->
                   (out : String) ->
                   (sock : Var) ->
                   ST m Bool [sock ::: (Sock tcpSocketInstance Connected :-> (\v => if v then Sock tcpSocketInstance Connected else Sock tcpSocketInstance Failed))]
writeSocketFully "" _ = pure True
writeSocketFully {tcpSocketInstance} out sock = with ST do
  case !(writeSocket tcpSocketInstance out sock) of
    Nothing => pure False
    Just out' => writeSocketFully out' sock

export
record IOBuffer (sock : Var) where
  constructor MkIOBuffer
  ioBufferContents : String

public export
record BufferedSocket where
  constructor MkBufferedSocket
  ioSocket, ioBuffer : Var

initIOBuffer : {m : Type -> Type}
               -> {auto tcpSocketInstance : TcpSockets m}
               -> (sock : Var)
               -> ST m Var [add (State $ IOBuffer sock)
                           , sock ::: Sock tcpSocketInstance st]
initIOBuffer sock = new (MkIOBuffer "")

export total
initBufferedSocket : {m : Type -> Type}
                     -> {auto tcpSocketInstance : TcpSockets m}
                     -> (sock : Var)
                     -> ST m (bufSock : BufferedSocket ** (sock = ioSocket bufSock)) [
                          Add (\bs => [(ioBuffer $ fst $ bs) ::: (State (IOBuffer sock))])
                          , sock ::: Sock tcpSocketInstance st
                        ]
initBufferedSocket sock = with ST do
  ioBuf <- initIOBuffer sock
  pure $ ((MkBufferedSocket sock ioBuf) ** Refl)

export total
deleteIOBuffer : {m : Type -> Type}
               -> (sock : Var)
               -> (sockBuffer : Var)
               -> ST m () [remove sockBuffer (State $ IOBuffer sock)]
deleteIOBuffer _ sockBuffer = ST.delete sockBuffer

export total
closeBufferedSocket : {m : Type -> Type}
                    -> {auto tcpSocketInstance : TcpSockets m}
                    -> (sock : BufferedSocket)
                    -> ST m () [ remove (ioBuffer sock) (State $ IOBuffer (ioSocket sock))
                               , remove (ioSocket sock) (Sock tcpSocketInstance st)]
closeBufferedSocket {tcpSocketInstance} sock = do
  call $ deleteIOBuffer (ioSocket sock) (ioBuffer sock)
  call $ close tcpSocketInstance (ioSocket sock)

export total
putIOBuffer : {m : Type -> Type}
            -> (sock : BufferedSocket)
            -> String
            -> ST m () [(ioBuffer sock) ::: State (IOBuffer (ioSocket sock))]
putIOBuffer sock newData =
  update (ioBuffer sock) (\buf : IOBuffer (ioSocket sock) => record {
    ioBufferContents = newData ++ (ioBufferContents buf)
  } buf)

export total
takeIOBuffer : {m : Type -> Type}
            -> (sock : BufferedSocket)
            -> ST m String [(ioBuffer sock) ::: State (IOBuffer (ioSocket sock))]
takeIOBuffer sock = do
  MkIOBuffer contents <- read (ioBuffer sock)
  write (ioBuffer sock) $ MkIOBuffer ""
  pure contents

public export total
%error_reduce -- always evaluate this before showing errors
maybeBufferedSocketFails : {auto tcpSocketInstance : TcpSockets m} -> {ty : Type} -> (sock : BufferedSocket) -> List (Action (Maybe ty))
maybeBufferedSocketFails {tcpSocketInstance} {ty} sock = [
    (ioBuffer sock) ::: State (IOBuffer (ioSocket sock))
  , (ioSocket sock) ::: (Sock tcpSocketInstance Connected :-> wrappedMaybeCaseOnly (Sock tcpSocketInstance) Failed Connected)
  ]

export total
readFromBufferedSocket : {m : Type -> Type}
                       -> {auto tcpSocketInstance : TcpSockets m}
                       -> (sock : BufferedSocket)
                       -> ST m (Maybe String) (maybeBufferedSocketFails sock)
readFromBufferedSocket {m} {tcpSocketInstance} sock = with ST do
    result <- ST.call (takeIOBuffer sock)
    if result == "" then
      call (readSocket {m} tcpSocketInstance (ioSocket sock))
    else
      pure (Just result)

-- TODO - We probably want an upper limit on the line length if we are going to use this for HTTP, as otherwise it could have
--        unbounded memory usage.
export
readLineFromSocket : {m : Type -> Type}
                     -> {auto tcpSocketInstance : TcpSockets m}
                     -> (sock : BufferedSocket)
                     -> ST m (Maybe String) (maybeBufferedSocketFails sock)
readLineFromSocket {m} {tcpSocketInstance} sock = go ""
  where
    go : String -> ST m (Maybe String) [
          (ioBuffer sock) ::: State (IOBuffer (ioSocket sock)),
          (ioSocket sock) ::: Sock tcpSocketInstance Connected :-> wrappedMaybeCaseOnly (Sock tcpSocketInstance) Failed Connected]
    go pfx = with ST do
      Just readData <- readFromBufferedSocket {m} {tcpSocketInstance} sock
        | Nothing => pure Nothing
      let (beforeNewline, afterAndIncludingNewline) = break (=='\n') readData
      ifWithProofs (afterAndIncludingNewline == "")
        (\_ =>
          go (pfx ++ beforeNewline)
        )
        (\proofNotEmpty => do
          call (putIOBuffer {m} sock (strTail' afterAndIncludingNewline proofNotEmpty))
          pure $ Just $ pfx ++ beforeNewline
        )

export
readFullyFromSocket : {m : Type -> Type}
                      -> {auto tcpSocketInstance : TcpSockets m}
                      -> (readLength : Nat)
                      -> (sock : BufferedSocket)
                      -> ST m (Maybe String) (maybeBufferedSocketFails sock)
readFullyFromSocket {m} {tcpSocketInstance} l sock = go l ""
  where
    go : (remaining : Nat) -> String -> ST m (Maybe String) (maybeBufferedSocketFails sock)
    go Z s = pure $ Just s
    go remaining pfx = with ST do
      Just readData <- readFromBufferedSocket {m} {tcpSocketInstance} sock
        | Nothing => pure Nothing
      let dataLen : Nat = length readData
      ifWithProofs (dataLen `ltNat` remaining)
        (\proofLt =>
          let
            prfComparison : LTE dataLen remaining = natALTBImpliesALTEB dataLen remaining (natALtBIsTrueImpliesLTAB dataLen remaining (ltNatIsLt proofLt))
          in
            go (remaining - dataLen) (pfx ++ readData)
        )
        (\proofNotLt => with ST do
          let prfComparison : LTE remaining dataLen =
            natALtBIsFalseImpliesGTEAB dataLen remaining (ltNatIsLt (NotAEqNotBImpliesAEqB (dataLen `ltNat` remaining) False proofNotLt))
          call $ putIOBuffer {m} sock (substr remaining (dataLen - remaining) readData)
          pure $ Just $ pfx ++ substr 0 remaining readData
        )


text:
module Hedgehog.Internal.Runner

import Data.Colist
import Data.Cotree
import Data.IORef
import Data.List
import Hedgehog.Internal.Config
import Hedgehog.Internal.Gen
import Hedgehog.Internal.Options
import Hedgehog.Internal.Property
import Hedgehog.Internal.Range
import Hedgehog.Internal.Report
import Hedgehog.Internal.Seed
import Hedgehog.Internal.Terminal
import System

%default total

public export
TestRes : Type
TestRes = (Either Failure (), Journal)

--------------------------------------------------------------------------------
--          Shrinking
--------------------------------------------------------------------------------

-- Shrinking
shrink : Monad m => Nat -> Coforest a -> b -> (Nat -> a -> m (Maybe b)) -> m b
shrink _     []        b _ = pure b
shrink 0 _             b _ = pure b
shrink (S k) (t :: ts) b f = do Just b2 <- f (S k) t.value
                                  | Nothing => shrink k ts b f
                                shrink k t.forest b2 f

takeSmallest :
     Monad m
  => Size
  -> Seed
  -> ShrinkLimit
  -> (Progress -> m ())
  -> Cotree TestRes
  -> m Result
takeSmallest si se (MkTagged slimit) updateUI t =
  do res <- run 0 t.value
     if isFailure res
        then shrink slimit t.forest res runMaybe
        else pure res

  where
    -- calc number of shrinks from the remaining
    -- allowed numer and the shrink limit
    calcShrinks : Nat -> ShrinkCount
    calcShrinks rem = MkTagged $ (slimit `minus` rem) + 1

    run : ShrinkCount -> TestRes -> m Result
    run shrinks t =
      case t of
        (Left $ MkFailure err diff, MkJournal logs) =>
           let fail = mkFailure si se shrinks Nothing err diff (reverse logs)
            in updateUI (Shrinking fail) $> Failed fail

        (Right x, _) => pure OK

    runMaybe : Nat -> TestRes -> m (Maybe Result)
    runMaybe shrinksLeft testRes =
      do res <- run (calcShrinks shrinksLeft) testRes
         if isFailure res then pure (Just res) else pure Nothing

--------------------------------------------------------------------------------
--          Test Runners
--------------------------------------------------------------------------------

-- main test runner
checkReport :
     Monad m
  => PropertyConfig
  -> Size
  -> Seed
  -> PropertyT ()
  -> (Report Progress -> m ())
  -> m (Report Result)
checkReport cfg si0 se0 test updateUI =
  let (conf, MkTagged numTests) = unCriteria cfg.terminationCriteria
   in loop numTests 0 si0 se0 neutral conf

  where
    loop :  Nat
         -> TestCount
         -> Size
         -> Seed
         -> Coverage CoverCount
         -> Maybe Confidence
         -> m (Report Result)
    loop n tests si se cover conf = do
      updateUI (MkReport tests cover Running)
      case n of
        0   =>
          -- required number of tests run
          pure $ report False tests si se cover conf
        S k =>
          if abortEarly cfg.terminationCriteria tests cover conf
             then
               -- at this point we know that enough
               -- tests have been run due to early termination
               pure $ report True tests si se cover conf
             else
              -- run another test
              let (s0,s1) = split se
                  tr      = runGen si s0 $ runTestT test
                  nextSize = if si < maxSize then (si + 1) else 0
               in case tr.value of
                    -- the test failed, so we abort and shrink
                    (Left x, _)  =>
                      let upd = updateUI . MkReport (tests+1) cover
                       in map (MkReport (tests+1) cover) $
                            takeSmallest si se cfg.shrinkLimit upd tr

                    -- the test succeeded, so we accumulate results
                    -- and loop once more
                    (Right x, journal) =>
                      let cover1 = journalCoverage journal <+> cover
                       in loop k (tests + 1) nextSize s1 cover1 conf

checkTerm :  HasIO io
          => Terminal
          -> UseColor
          -> Maybe PropertyName
          -> Size
          -> Seed
          -> Property
          -> io (Report Result)
checkTerm term color name si se prop =
  do result <- checkReport {m = io} prop.config si se prop.test $ \prog =>
               if multOf100 prog.tests
                  then let ppprog = renderProgress color name prog
                        in case prog.status of
                               Running     => putTmp term ppprog
                               Shrinking _ => putTmp term ppprog
                  else pure ()

     putOut term (renderResult color name result)
     pure result

checkWith :  HasIO io
          => Terminal
          -> UseColor
          -> Maybe PropertyName
          -> Property
          -> io (Report Result)
checkWith term color name prop =
  initSMGen >>= \se => checkTerm term color name 0 se prop

||| Check a property.
export
checkNamed : HasIO io => PropertyName -> Property -> io Bool
checkNamed name prop = do
  color <- detectColor
  term  <- console
  rep   <- checkWith term color (Just name) prop
  pure $ rep.status == OK

||| Check a property.
export
check : HasIO io => Property -> io Bool
check prop = do
  color <- detectColor
  term  <- console
  rep   <- checkWith term color Nothing prop
  pure $ rep.status == OK

||| Check a property using a specific size and seed.
export
recheck : HasIO io => Size -> Seed -> Property -> io ()
recheck si se prop = do
  color <- detectColor
  term  <- console
  _     <- checkTerm term color Nothing si se (withTests 1 prop)
  pure ()

checkGroupWith :  Terminal
               -> UseColor
               -> List (PropertyName, Property)
               -> IO Summary
checkGroupWith term color = run neutral
  where run : Summary -> List (PropertyName, Property) -> IO Summary
        run s [] = pure s
        run s ((pn,p) :: ps) = do rep  <- checkWith term color (Just pn) p
                                  run (s <+> fromResult rep.status) ps

export
checkGroup : HasIO io => Group -> io Bool
checkGroup (MkGroup group props) =
  do term    <- console
     putOut term $ "━━━ " ++ unTag group ++ " ━━━"
     color   <- detectColor
     summary <- liftIO $ checkGroupWith term color props
     putOut term (renderSummary color summary)
     pure $ summary.failed == 0

||| Simple test runner.
|||
||| Use this in a `main` function in order to test a list of
||| property groups. The runner will take into account several
||| command line arguments in order to adjust the number of
||| tests to be run for each property, the maximal number of
||| shrinks and the confidence value to use.
|||
||| ```idris example
||| main : IO ()
||| main = test myGroups
||| ```
|||
||| The resulting executable can then be run as follows:
|||
||| ```sh
||| build/exec/runTests -n 1000
||| ```
|||
||| It will fail with an exit code of 1 if at least one property
||| fails.
export
test : HasIO io => List Group -> io ()
test gs = do
  args    <- getArgs
  Right c <- pure $ applyArgs args
    | Left errs => do
        putStrLn "Errors when parsing command line args:"
        traverse_ putStrLn errs
        exitFailure
  if c.printHelp
     then putStrLn info >> exitSuccess
     else
       let gs2 = map (applyConfig c) gs
        in do
             res <- foldlM (\b,g => map (b &&) (checkGroup g)) True gs2
             if res
                then exitSuccess
                else putStrLn "\n\nSome tests failed" >> exitFailure


text:
module Matrix

import Data.Vect

addMatrix : Num num => Vect rows (Vect cols num) -> Vect rows (Vect cols num) -> Vect rows (Vect cols num)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (+) x y :: addMatrix xs ys

-- We have to bring the implicit {n} into scope before case splitting on it
create_empties : Vect n (Vect 0 elem)
create_empties {n = Z} = []
create_empties {n = (S k)} = [] :: create_empties

transpose_helper : (x : Vect n elem) -> (xs_transpose : Vect n (Vect k elem)) -> Vect n (Vect (S k) elem)
transpose_helper = zipWith (::)
-- transpose_helper [] [] = []
-- transpose_helper (x :: xs) (y :: ys) = (x :: y) :: transpose_helper xs ys

transposeMatrix : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMatrix [] = create_empties
transposeMatrix (x :: xs) = let xs_transpose = transposeMatrix xs in
                                transpose_helper x xs_transpose

total multiplyOneRow : Num num => Vect m num -> Vect p (Vect m num) -> Vect p num
multiplyOneRow xs [] = []
multiplyOneRow xs (x :: ys) = (foldl (+) 0 (zipWith (*) xs x)) :: multiplyOneRow xs ys

total multiplyTransposedMatrices : Num num => Vect n (Vect m num) -> Vect p (Vect m num) -> Vect n (Vect p num)
multiplyTransposedMatrices [] ys = []
multiplyTransposedMatrices (x :: xs) ys = multiplyOneRow x ys :: multiplyTransposedMatrices xs ys

total multMatrix : Num num => Vect n (Vect m num) -> Vect m (Vect p num) -> Vect n (Vect p num)
multMatrix xs ys = multiplyTransposedMatrices xs (transposeMatrix ys)

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
module Utils
import Prelude.List as L
import Data.Vect as V

%access export

public export
Matrix : Nat -> Nat -> Type -> Type
Matrix n m a = Vect n $ Vect m a

toList : Matrix m n elem -> List $ List elem
toList = L.toList . map L.toList

group : (Eq a) => List a -> List $ List a
group [] = []
group (x :: xs) =
	let (ys, zs) = L.span (== x) xs in (x :: ys) :: (group $ assert_smaller (x :: xs) zs) -- Bad

splitAt' : (n : Nat) -> Vect (1 + n + m) elem -> (Vect n elem, elem, Vect m elem)
splitAt' Z (x :: xs) = ([], x, xs)
splitAt' (S k) (x :: xs) with (splitAt' k xs)
	| (l, m, r) = (x :: l, m, r)

natToFin' : (n : Nat) -> (m : Nat) -> Maybe (Fin m, LT n m) -- Is there a better way to do this?
natToFin' Z (S x) = Just (FZ, LTESucc $ LTEZero)
natToFin' (S k1) (S k2) with (natToFin' k1 k2)
	| Just (x, p) = Just (FS x, LTESucc p)
	| Nothing = Nothing
natToFin' _ _ = Nothing

plusMinusNeutral : {n : Nat} -> {m : Nat} -> (p : GTE m n) -> (n + (minus m n)) = m
plusMinusNeutral {n = Z} {m = m} _ = minusZeroRight m
plusMinusNeutral {n = (S _)} {m = Z} LTEZero impossible
plusMinusNeutral {n = (S _)} {m = Z} (LTESucc _) impossible
plusMinusNeutral {n = (S k1)} {m = (S k2)} p =
	eqSucc (k1 + (minus k2 k1)) k2 (plusMinusNeutral {n = k1} {m = k2} $ fromLteSucc p)

succMinus : {n : Nat} -> {m : Nat} -> (p : GTE n m) -> (1 + minus n m) = (minus (1 + n) m)
succMinus {n = Z} {m = Z} _ = Refl
succMinus {n = Z} {m = (S _)} LTEZero impossible
succMinus {n = Z} {m = (S _)} (LTESucc _) impossible
succMinus {n = (S k)} {m = Z} p = Refl
succMinus {n = (S k1)} {m = S (k2)} p = succMinus {n = k1} {m = k2} (fromLteSucc p)

private
lemma : {n : Nat} -> {x : Maybe $ elem} -> {xs : Vect n $ Maybe $ elem} -> LTE (fst $ catMaybes $ x :: xs) (S $ fst $ catMaybes $ xs)
lemma {n = Z} {x = Nothing} {xs = []} = LTEZero
lemma {n = Z} {x = (Just x)} {xs = []} = LTESucc LTEZero
lemma {n = (S len)} {x = Nothing} = lteSuccRight $ lteRefl
lemma {n = (S len)} {x = Just x} = ?l -- No idea how to prove this in Idris! The proof involves a case expression.

catMaybesLTE : {n : Nat} -> {xs : Vect n (Maybe elem)} -> LTE (fst $ catMaybes xs) n
catMaybesLTE {n = Z} {xs = []} = LTEZero
catMaybesLTE {n = (S len)} {xs = (x :: xs)} =
	lteTransitive lemma $ LTESucc $ catMaybesLTE {n = len} {xs = xs}


text:
arg1 : Int -> String
arg1 a1 = "arg1: " ++ show a1

arg2 : Int -> Int -> String
arg2 a1 a2 = "arg2: " ++ show a1 ++ ", " ++ show a2

arg3 : Int -> Int -> Int -> String
arg3 a1 a2 a3 = "arg3: " ++ show a1 ++ ", " ++ show a2 ++ ", " ++ show a3

arg4 : Int -> Int -> Int -> Int -> String
arg4 a1 a2 a3 a4 = "arg4: " ++ show a1 ++ ", " ++ show a2 ++ ", " ++ show a3 ++ ", " ++ show a4

arg5 : Int -> Int -> Int -> Int -> Int -> String
arg5 a1 a2 a3 a4 a5 = "arg5: " ++ show a1 ++ ", " ++ show a2 ++ ", " ++ show a3 ++ ", " ++ show a4 ++ ", " ++ show a5

main : IO ()
main = do
  traverse_ putStrLn (map arg1 [13, 17])
  traverse_ putStrLn (map (arg2 5) [13, 17])
  traverse_ putStrLn (map (arg3 5 19) [13, 17])
  traverse_ putStrLn (map (arg4 5 19 23) [13, 17])
  traverse_ putStrLn (map (arg5 5 19 23 41) [13, 17])

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Data.Compress.Utils.Misc

import Data.Fin
import Data.Vect
import Data.List
import Data.Bits
import Data.List1
import Data.SnocList

export
take_last : Nat -> SnocList a -> Maybe (List a)
take_last = loop Lin where
  loop : SnocList a -> Nat -> SnocList a -> Maybe (List a)
  loop acc Z _ = Just (asList acc)
  loop acc (S n) (init :< last) = loop (acc :< last) n init
  loop acc _ Lin = Nothing

export
stream_concat : Stream (List a) -> Stream a
stream_concat ([] :: ys) = stream_concat ys
stream_concat ((x :: xs) :: ys) = x :: stream_concat (xs :: ys)

export
index_may : Nat -> List a -> Maybe a
index_may Z (x :: xs) = Just x
index_may (S n) (x :: xs) = index_may n xs
index_may _ [] = Nothing

export
count : Ord a => List a -> List (a, Nat)
count = map (\xs => (head xs, length xs)) . group . sort


text:
module Scheme_Expressions

import Scheme_Parsers

||| The type of curried function on double
Curried_fn : (n : Nat) -> Type
Curried_fn Z = Double
Curried_fn (S n) = Double -> (Curried_fn n)

||| Type of expressions
data Statement : Type where
    Expression : Double -> Statement
    Definition : (var : Char) -> (value : Double) -> Statement
    Function : (n : Nat) -> (Curried_fn n) -> Statement


text:
module Web.Internal.ServiceworkerTypes

import JS

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace ServiceWorkerState

  public export
  data ServiceWorkerState = Parsed
                          | Installing
                          | Installed
                          | Activating
                          | Activated
                          | Redundant

  public export
  Show ServiceWorkerState where
    show Parsed = "parsed"
    show Installing = "installing"
    show Installed = "installed"
    show Activating = "activating"
    show Activated = "activated"
    show Redundant = "redundant"

  public export
  Eq ServiceWorkerState where
    (==) = (==) `on` show

  public export
  Ord ServiceWorkerState where
    compare = compare `on` show

  public export
  read : String -> Maybe ServiceWorkerState
  read "parsed" = Just Parsed
  read "installing" = Just Installing
  read "installed" = Just Installed
  read "activating" = Just Activating
  read "activated" = Just Activated
  read "redundant" = Just Redundant
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (ServiceWorkerState.read s)}
             -> ServiceWorkerState
  fromString s = fromJust $ read s

  export
  ToFFI ServiceWorkerState String where
    toFFI = show

  export
  FromFFI ServiceWorkerState String where
    fromFFI = read

namespace ServiceWorkerUpdateViaCache

  public export
  data ServiceWorkerUpdateViaCache = Imports | All | None

  public export
  Show ServiceWorkerUpdateViaCache where
    show Imports = "imports"
    show All = "all"
    show None = "none"

  public export
  Eq ServiceWorkerUpdateViaCache where
    (==) = (==) `on` show

  public export
  Ord ServiceWorkerUpdateViaCache where
    compare = compare `on` show

  public export
  read : String -> Maybe ServiceWorkerUpdateViaCache
  read "imports" = Just Imports
  read "all" = Just All
  read "none" = Just None
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (ServiceWorkerUpdateViaCache.read s)}
             -> ServiceWorkerUpdateViaCache
  fromString s = fromJust $ read s

  export
  ToFFI ServiceWorkerUpdateViaCache String where
    toFFI = show

  export
  FromFFI ServiceWorkerUpdateViaCache String where
    fromFFI = read

namespace FrameType

  public export
  data FrameType = Auxiliary | TopLevel | Nested | None

  public export
  Show FrameType where
    show Auxiliary = "auxiliary"
    show TopLevel = "top-level"
    show Nested = "nested"
    show None = "none"

  public export
  Eq FrameType where
    (==) = (==) `on` show

  public export
  Ord FrameType where
    compare = compare `on` show

  public export
  read : String -> Maybe FrameType
  read "auxiliary" = Just Auxiliary
  read "top-level" = Just TopLevel
  read "nested" = Just Nested
  read "none" = Just None
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (FrameType.read s)}
             -> FrameType
  fromString s = fromJust $ read s

  export
  ToFFI FrameType String where
    toFFI = show

  export
  FromFFI FrameType String where
    fromFFI = read

namespace ClientType

  public export
  data ClientType = Window | Worker | Sharedworker | All

  public export
  Show ClientType where
    show Window = "window"
    show Worker = "worker"
    show Sharedworker = "sharedworker"
    show All = "all"

  public export
  Eq ClientType where
    (==) = (==) `on` show

  public export
  Ord ClientType where
    compare = compare `on` show

  public export
  read : String -> Maybe ClientType
  read "window" = Just Window
  read "worker" = Just Worker
  read "sharedworker" = Just Sharedworker
  read "all" = Just All
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (ClientType.read s)}
             -> ClientType
  fromString s = fromJust $ read s

  export
  ToFFI ClientType String where
    toFFI = show

  export
  FromFFI ClientType String where
    fromFFI = read

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

export data Cache : Type where [external]

export
ToFFI Cache Cache where toFFI = id

export
FromFFI Cache Cache where fromFFI = Just

export
SafeCast Cache where
  safeCast = unsafeCastOnPrototypeName "Cache"

export data CacheStorage : Type where [external]

export
ToFFI CacheStorage CacheStorage where toFFI = id

export
FromFFI CacheStorage CacheStorage where fromFFI = Just

export
SafeCast CacheStorage where
  safeCast = unsafeCastOnPrototypeName "CacheStorage"

export data Client : Type where [external]

export
ToFFI Client Client where toFFI = id

export
FromFFI Client Client where fromFFI = Just

export
SafeCast Client where
  safeCast = unsafeCastOnPrototypeName "Client"

export data Clients : Type where [external]

export
ToFFI Clients Clients where toFFI = id

export
FromFFI Clients Clients where fromFFI = Just

export
SafeCast Clients where
  safeCast = unsafeCastOnPrototypeName "Clients"

export data ExtendableEvent : Type where [external]

export
ToFFI ExtendableEvent ExtendableEvent where toFFI = id

export
FromFFI ExtendableEvent ExtendableEvent where fromFFI = Just

export
SafeCast ExtendableEvent where
  safeCast = unsafeCastOnPrototypeName "ExtendableEvent"

export data ExtendableMessageEvent : Type where [external]

export
ToFFI ExtendableMessageEvent ExtendableMessageEvent where toFFI = id

export
FromFFI ExtendableMessageEvent ExtendableMessageEvent where fromFFI = Just

export
SafeCast ExtendableMessageEvent where
  safeCast = unsafeCastOnPrototypeName "ExtendableMessageEvent"

export data FetchEvent : Type where [external]

export
ToFFI FetchEvent FetchEvent where toFFI = id

export
FromFFI FetchEvent FetchEvent where fromFFI = Just

export
SafeCast FetchEvent where
  safeCast = unsafeCastOnPrototypeName "FetchEvent"

export data NavigationPreloadManager : Type where [external]

export
ToFFI NavigationPreloadManager NavigationPreloadManager where toFFI = id

export
FromFFI NavigationPreloadManager NavigationPreloadManager where fromFFI = Just

export
SafeCast NavigationPreloadManager where
  safeCast = unsafeCastOnPrototypeName "NavigationPreloadManager"

export data ServiceWorker : Type where [external]

export
ToFFI ServiceWorker ServiceWorker where toFFI = id

export
FromFFI ServiceWorker ServiceWorker where fromFFI = Just

export
SafeCast ServiceWorker where
  safeCast = unsafeCastOnPrototypeName "ServiceWorker"

export data ServiceWorkerContainer : Type where [external]

export
ToFFI ServiceWorkerContainer ServiceWorkerContainer where toFFI = id

export
FromFFI ServiceWorkerContainer ServiceWorkerContainer where fromFFI = Just

export
SafeCast ServiceWorkerContainer where
  safeCast = unsafeCastOnPrototypeName "ServiceWorkerContainer"

export data ServiceWorkerGlobalScope : Type where [external]

export
ToFFI ServiceWorkerGlobalScope ServiceWorkerGlobalScope where toFFI = id

export
FromFFI ServiceWorkerGlobalScope ServiceWorkerGlobalScope where fromFFI = Just

export
SafeCast ServiceWorkerGlobalScope where
  safeCast = unsafeCastOnPrototypeName "ServiceWorkerGlobalScope"

export data ServiceWorkerRegistration : Type where [external]

export
ToFFI ServiceWorkerRegistration ServiceWorkerRegistration where toFFI = id

export
FromFFI ServiceWorkerRegistration ServiceWorkerRegistration where fromFFI = Just

export
SafeCast ServiceWorkerRegistration where
  safeCast = unsafeCastOnPrototypeName "ServiceWorkerRegistration"

export data WindowClient : Type where [external]

export
ToFFI WindowClient WindowClient where toFFI = id

export
FromFFI WindowClient WindowClient where fromFFI = Just

export
SafeCast WindowClient where
  safeCast = unsafeCastOnPrototypeName "WindowClient"

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

export data CacheQueryOptions : Type where [external]

export
ToFFI CacheQueryOptions CacheQueryOptions where toFFI = id

export
FromFFI CacheQueryOptions CacheQueryOptions where fromFFI = Just

export data ClientQueryOptions : Type where [external]

export
ToFFI ClientQueryOptions ClientQueryOptions where toFFI = id

export
FromFFI ClientQueryOptions ClientQueryOptions where fromFFI = Just

export data ExtendableEventInit : Type where [external]

export
ToFFI ExtendableEventInit ExtendableEventInit where toFFI = id

export
FromFFI ExtendableEventInit ExtendableEventInit where fromFFI = Just

export data ExtendableMessageEventInit : Type where [external]

export
ToFFI ExtendableMessageEventInit ExtendableMessageEventInit where toFFI = id

export
FromFFI ExtendableMessageEventInit ExtendableMessageEventInit where fromFFI = Just

export data FetchEventInit : Type where [external]

export
ToFFI FetchEventInit FetchEventInit where toFFI = id

export
FromFFI FetchEventInit FetchEventInit where fromFFI = Just

export data MultiCacheQueryOptions : Type where [external]

export
ToFFI MultiCacheQueryOptions MultiCacheQueryOptions where toFFI = id

export
FromFFI MultiCacheQueryOptions MultiCacheQueryOptions where fromFFI = Just

export data NavigationPreloadState : Type where [external]

export
ToFFI NavigationPreloadState NavigationPreloadState where toFFI = id

export
FromFFI NavigationPreloadState NavigationPreloadState where fromFFI = Just

export data RegistrationOptions : Type where [external]

export
ToFFI RegistrationOptions RegistrationOptions where toFFI = id

export
FromFFI RegistrationOptions RegistrationOptions where fromFFI = Just


text:
module Main

test : List Nat -> List Nat

test_main : List Nat
test_main = test [4, 3, "cat"]


text:
import Decidable.Equality

0 foo : (i, j : Nat) -> Bool
foo i j = case decEq i j of
            Yes pf => True
            No  pf => False


text:
module HoTT

import Builtin
import Basic
import Unit
import Void
import Coproduct
import Sigma
import Nat
import Path
import PreorderReasoning
import General
import Dec

%default total

-- Little nuances and inconveniences experienced while writing this:
-- 1)Not overloadable syntax: = (,) ()
--  and, in general, no custom syntax extensions.
-- 2)Why prefix (-) is parsed as `negate` ?
-- 3)Lexicographically ordered fixities over Natural Numbers ?
--   It solves the problem:
--   For any two fixities x, z such that x < z
--     there is a fixity y such that x < y < z
--     (and x, y, z are Natural Numbers, which is convenient).
-- 4)No option to unhide global names.
-- 5)System of numeric literal overloading is flawed:
--    Overloading of numeric literals works by providing a function of type `Integer -> a`.
--    But to carry this out for naturals
--     we have to map all negative integers to zero in this case, to provide a sensible transformation.

-- The project doesn't depend on the Prelude and other libraries
-- to be bare-bones and more comprehensible

-- Some operators and names are chosen to be different
-- from the standard ones to closely follow those found in
-- the HoTT book or in this course: https://arxiv.org/pdf/1911.00580.pdf

-- While sometimes differing naming is introduced as a matter of preference.

||| A type together with a point, called its basepoint.
PointedType : Type
PointedType = Sigma Type id

||| A pointed type of paths from a point to itself, a.k.a loops,
||| with the basepoint set to reflexivity.
||| We don't carry the reflexivity proof in its elements, as it is static.
LoopSpace : (ty : Type) -> (a : ty) -> Type
LoopSpace ty a = Id ty a a

||| Another name for loop space.
Omega1 : (ty : Type) -> (a : ty) -> Type
Omega1 = LoopSpace

-- LoopSpace forms a higher group

||| 2-fold iterated loop space.
Omega2 : (ty : Type) -> (a : ty) -> Type
Omega2 ty a = Omega1 (Id ty a a) (Refl a)

||| Right neutral element of the identity composition.
ConcatRightNeutral : (p : Id ty a b)
                   -> p == (p . Refl b)
ConcatRightNeutral (Refl b) = Refl (Refl b)

||| Left neutral element of the identity composition.
ConcatLeftNeutral : (p : Id ty a b)
                 -> p == (Refl a . p)
ConcatLeftNeutral (Refl b) = Refl (Refl b)

||| Composition of a identity with
||| its inverse on the left is reflexivity.
ConcatLeftIdentity : (p : Id ty a b)
                   -> (sym p . p) == Refl b
ConcatLeftIdentity (Refl b) = Refl (Refl b)

||| Composition of a identity with
||| its inverse on the right is reflexivity.
ConcatRightIdentity : (p : Id ty a b)
                   -> (p . sym p) == Refl a
ConcatRightIdentity (Refl a) = Refl (Refl a)

||| Identity inverse is idempotent.
SymIdempotent : (p : Id ty a b)
             -> (p == sym (sym p))
SymIdempotent (Refl b) = Refl (Refl b)

||| Associativity of identity composition.
ConcatAssoc : (p : Id ty a b)
           -> (q : Id ty b c)
           -> (r : Id ty c d)
           -> (p . (q . r)) == ((p . q) . r)
ConcatAssoc (Refl b) (Refl b) (Refl b) = Refl (Refl b)

||| The right whiskering operation.
RightWhisker : (a, b, c : ty)
            -> (p, q : Id ty a b)
            -> (alpha : Id (Id ty a b) p q)
            -> (r : Id ty b c)
            -> Id (Id ty a c) (p . r) (q . r)
RightWhisker a b b p q alpha (Refl b) =
  sym (ConcatRightNeutral p) . alpha . ConcatRightNeutral q

||| The left whiskering operation.
LeftWhisker : (a, b, c : ty)
           -> (q : Id ty a b)
           -> (r, s : Id ty b c)
           -> (beta : Id (Id ty b c) r s)
           -> Id (Id ty a c) (q . r) (q . s)
LeftWhisker b b c (Refl b) r s beta =
  sym (ConcatLeftNeutral r) . beta . ConcatLeftNeutral s

||| Horizontal composition of 2-paths.
HorizontalComposition : (a, b, c : ty)
                    -> (p, q : Id ty a b)
                    -> (r, s : Id ty b c)
                    -> (alpha : Id (Id ty a b) p q)
                    -> (beta : Id (Id ty b c) r s)
                    -> Id (Id ty a c) (p . r) (q . s)
HorizontalComposition a b c p q r s alpha beta =
  RightWhisker a b c p q alpha r . LeftWhisker a b c q r s beta

||| Another definition of horizontal composition of 2-paths.
HorizontalComposition' : (a, b, c : ty)
                     -> (p, q : Id ty a b)
                     -> (r, s : Id ty b c)
                     -> (alpha : Id (Id ty a b) p q)
                     -> (beta : Id (Id ty b c) r s)
                     -> Id (Id ty a c) (p . r) (q . s)
HorizontalComposition' a b c p q r s alpha beta =
  LeftWhisker a b c p r s beta . RightWhisker a b c p q alpha s

||| Above definitions agree.
HorizontalCompositionsAgree :
     (a, b, c : ty)
  -> (p, q : Id ty a b)
  -> (r, s : Id ty b c)
  -> (alpha : Id (Id ty a b) p q)
  -> (beta : Id (Id ty b c) r s)
  -> HorizontalComposition a b c p q r s alpha beta
  == HorizontalComposition' a b c p q r s alpha beta
HorizontalCompositionsAgree b b b
  (Refl b) (Refl b) (Refl b)
  (Refl b) (Refl (Refl b)) (Refl (Refl b)) =
    Refl (Refl (Refl b))

||| (.) composition of loop spaces agrees with both compositions defined above.
Omega2HorizontalCompose :
     (alpha, beta : Omega2 ty a)
  -> (alpha . beta)
  == HorizontalComposition a a a (Refl a) (Refl a) (Refl a) (Refl a)
       alpha beta
Omega2HorizontalCompose (Refl (Refl a)) (Refl (Refl a)) =
  Refl (Refl (Refl a))

-- Eckmann-Hilton
||| Composition of 2-loops is commutative.
Omega2ConcatCommut : (alpha, beta : Omega2 ty a)
                  -> (alpha . beta) == (beta . alpha)
Omega2ConcatCommut (Refl (Refl a)) (Refl (Refl a)) =
  Refl (Refl (Refl a))

infix 0 ~~

||| Pointwise equality of functions.
||| A homotopy from f to g.
public export
(~~) : {p : a -> Type} -> (f, g : (x : a) -> p x) -> Type
f ~~ g = (x : a) -> f x == g x

||| Any function is homotopic to itself.
HomotopyRefl :
     {p : a -> Type}
  -> (f : (x : a) -> p x)
  -> f ~~ f
HomotopyRefl hom x = Refl (hom x)

||| The homotopy relation is symmetric.
HomotopySym :
     {p : a -> Type}
  -> {f, g : (x : a) -> p x}
  -> f ~~ g
  -> g ~~ f
HomotopySym hom x = sym (hom x)

||| The homotopy relation is transitive.
||| This is also called horizontal composition.
HomotopyTransitive :
     {p : a -> Type}
  -> {f, g, h : (x : a) -> p x}
  -> f ~~ g
  -> g ~~ h
  -> f ~~ h
HomotopyTransitive alpha beta x =
  alpha x . beta x

||| A different name for transitivity of homotopies.
HomotopyHorCompose :
     {p : a -> Type}
  -> {f, g, h : (x : a) -> p x}
  -> f ~~ g
  -> g ~~ h
  -> f ~~ h
HomotopyHorCompose = HomotopyTransitive

||| Vertical composition of homotopies.
HomotopyVertCompose :
     {f, g : a -> b}
  -> {f', g' : b -> c}
  -> (f ~~ g)
  -> (f' ~~ g')
  -> (f . f') ~~ (g . g')
HomotopyVertCompose alpha beta x with (alpha x)
  HomotopyVertCompose alpha beta x | ax with (f x)
   HomotopyVertCompose alpha beta x | ax | fx with (g x)
    HomotopyVertCompose alpha beta x | Refl _ | fx | fx = beta fx

||| Non-dependent version
HomotopyNaturalTransformation :
     {f, g : a -> b}
  -> (hom : f ~~ g)
  -> (p : x == y)
  -> (hom x . ap g p) == (ap f p . hom y)
HomotopyNaturalTransformation hom (Refl x) =
  sym (ConcatRightNeutral (hom x)) . Refl (hom x) . ConcatLeftNeutral (hom x)

||| Type of quasi-inverses of the given function.
QInv :
     {a, b : _}
  -> (f : a -> b)
  -> Type
QInv f = Sigma (b -> a) \g => Pair (g . f ~~ id) (f . g ~~ id)

||| Type of equivalences of the given function.
IsEquiv :
     {a, b : _}
  -> (f : a -> b)
  -> Type
IsEquiv f = Pair (Sigma (b -> a) \g => g . f ~~ id)
                 (Sigma (b -> a) \g => f . g ~~ id)

||| Being a quasi-inverse implies being an equivalence.
QInvIsEquiv :
     {f : a -> b}
  -> QInv f -> IsEquiv f
QInvIsEquiv (g # hom # hom') = (g # hom) # (g # hom')

||| Being an equivalence implies being a quasi-inverse.
EquivIsQInv :
     {a, b : _}
  -> {f : a -> b}
  -> IsEquiv f -> QInv f
EquivIsQInv ((g # alpha) # (h # beta)) =
  g # alpha # let
    alpha' = HomotopyVertCompose alpha (HomotopyRefl h)
    beta' = HomotopyVertCompose (HomotopyRefl g) beta
    gamma = HomotopyHorCompose (HomotopySym alpha') beta'
    gamma' = HomotopyVertCompose (HomotopyRefl f) gamma in
    HomotopyHorCompose (HomotopySym gamma') beta

infix 0 ~=

||| An equivalence from `a` to `b`.
(~=) : (a : Type) -> (b : Type) -> Type
a ~= b = Sigma (a -> b) IsEquiv

||| The equivalence is a reflexive relation.
EquivalenceReflexive :
     (a : Type)
  -> a ~= a
EquivalenceReflexive a =
  id # (id # \x => Refl x) # (id # \x => Refl x)

||| The equivalence is a symmetric relation.
EquivalenceSymmetric :
     {a, b : Type}
  -> a ~= b
  -> b ~= a
EquivalenceSymmetric (f # eq) =
  let (g # a # b) = EquivIsQInv {f} eq in g # QInvIsEquiv (f # b # a)
                 --              ^--- TODO Unifier should've actually solved that. Report ?

||| The equivalence is a transitive relation.
EquivalenceTransitive :
     {a, b, c : Type}
  -> a ~= b
  -> b ~= c
  -> a ~= c
EquivalenceTransitive (f # eqf) (g # eqg) =
  let (f' # a # b) = EquivIsQInv eqf
      (g' # c # d) = EquivIsQInv {f = g} eqg
                 --               ^--- TODO same problem
      alpha = HomotopyVertCompose (HomotopyRefl g') a
      alpha' = HomotopyVertCompose alpha (HomotopyRefl g)
      alpha'' = HomotopyHorCompose alpha' c
      beta = HomotopyVertCompose (HomotopyRefl f) d
      beta' = HomotopyVertCompose beta (HomotopyRefl f')
      beta'' = HomotopyHorCompose beta' b in
      f . g # QInvIsEquiv (g' . f' # alpha'' # beta'')

||| Product identity elimination rule.
PairEqElim :
     {x, y : Pair a b}
  -> (p : x == y)
  -> Pair (pr1 x == pr1 y) (pr2 x == pr2 y)
PairEqElim p = ap pr1 p # ap pr2 p

||| Product identity introduction rule.
PairEqIntro :
     {x, y : Pair a b}
  -> Pair (pr1 x == pr1 y) (pr2 x == pr2 y)
  -> x == y
PairEqIntro {x = e1 # e2, y = e1 # e2} (Refl _ # Refl _) =
  Refl (e1 # e2)

||| Product identity introduction rule is a quasi-inverse of
||| its elimination rule.
PairEqQInv : {a, b, x, y : _} -> QInv (PairEqElim {a, b, x, y})
PairEqQInv = PairEqIntro # fst # snd
 where
  fst : {a, b, x, y : _}
     -> (PairEqIntro {a, b, x, y} . PairEqElim {a, b, x, y})
     ~~ id {a = Pair (pr1 x == pr1 y) (pr2 x == pr2 y)}
  fst {x = e1 # e2, y = e1 # e2} (Refl _ # Refl _) = Refl (Refl e1 # Refl e2)

  snd : {a, b, x, y : _}
     -> (PairEqElim {a, b, x, y} . PairEqIntro {a, b, x, y})
     ~~ id {a = x == y}
  snd {x = e1 # e2, y = e1 # e2} (Refl _) = Refl (Refl (e1 # e2))

||| Product identity introduction & elimination rules
||| form an equivalence.
PairEqIsEquiv : {a, b, x, y : _} -> IsEquiv (PairEqElim {a, b, x, y})
PairEqIsEquiv = QInvIsEquiv PairEqQInv

||| Propositional uniqueness principle for products.
PairUniqueness :
     (x : Pair a b)
  -> x == (pr1 {p = const b} x # pr2 {p = const b} x)
  -- TODO pretty strange why I had to manually specify the `p`.
PairUniqueness x =
  PairEqIntro {x} {y = pr1 x # pr2 x} (Refl (pr1 x) # Refl (pr2 x))

namespace Family
  ||| Pointwise product of type families.
  public export
  Cross :
       (a, b : ty -> Type)
    -> ty
    -> Type
  Cross a b x = Pair (a x) (b x)

||| Functoriality (?) of `transport` under cartesian products.
TransportPair :
     {x, y : ty}
  -> {a, b : ty -> Type}
  -> (p : Id ty x y)
  -> (c : Pair (a x) (b x))
  -> transport (Cross a b) p c == (transport a p (pr1 c) # transport b p (pr2 c))
TransportPair (Refl x) c = PairUniqueness c

namespace Function
  ||| Pointwise product of functions.
  public export
  Cross :
       (f : a -> a')
    -> (g : b -> b')
    -> Pair a b -> Pair a' b'
  Cross f g x = f (pr1 x) # g (pr2 x)

||| Functoriality of `ap` under cartesian products.
ApPair :
     (f : a -> a')
  -> (g : b -> b')
  -> (x, y : Pair a b)
  -> (p : pr1 x == pr1 y)
  -> (q : pr2 x == pr2 y)
  -> ap (Cross f g) (PairEqIntro {x, y} (p # q))
               --                 ^--^---TODO strange unification problems again
  == PairEqIntro (ap f p # ap g q)
ApPair f g (a # b) (a # b) (Refl _) (Refl _) =
  Refl (Refl (f a # g b))

||| Sigma type identity elimination rule.
SigmaEqElim :
     {p : a -> Type}
  -> {w, w' : Sigma a p}
  -> (w == w')
  -> Sigma (pr1 w == pr1 w')
           (\path => transport p path (pr2 w) == pr2 w')
SigmaEqElim (Refl w) = Refl (pr1 w) # Refl (pr2 w)

||| Sigma type identity introduction rule.
SigmaEqIntro :
     {p : a -> Type}
  -> {w, w' : Sigma a p}
  -> Sigma (pr1 w == pr1 w')
           (\path => transport p path (pr2 w) == pr2 w')
  -> (w == w')
SigmaEqIntro {w = a # b, w' = a' # b'} sigma =
  SigmaInduction (\_ => Id (Sigma _ p) (a # b) (a' # b'))
    (\(Refl a) => \(Refl b) => Refl (a # b)) sigma

||| Sigma type identity introduction rule is a quasi-inverse of
||| its elimination rule.
SigmaEqQInv :
     {p : a -> Type}
  -> {w, w' : Sigma a p}
  -> QInv (SigmaEqElim {p, w, w'})
SigmaEqQInv {w = a # b, w' = a' # b'} =
  SigmaEqIntro # (\(Refl _ # Refl _) => Refl (Refl a # Refl b))
               # (\(Refl (a # b)) => Refl (Refl (a # b)))

||| Sigma type identity introduction & elimination rules
||| form an equivalence.
SigmaEqIsEquiv :
     {p : a -> Type}
  -> {w, w' : Sigma a p}
  -> IsEquiv (SigmaEqElim {p, w, w'})
SigmaEqIsEquiv =
  QInvIsEquiv {f = SigmaEqElim {p, w, w'}}
              (SigmaEqQInv {p, w, w'})

||| Propositional uniqueness principle for sigma types.
SigmaUniqueness :
     {p : a -> Type}
  -> (z : Sigma a p)
  -> z == (pr1 z # pr2 z)
SigmaUniqueness z =
  SigmaEqIntro {w = z, w' = pr1 z # pr2 z} (Refl (pr1 z) # Refl (pr2 z))

||| Unit identity elimination rule.
UnitEqElim :
     {x, y : Unit}
  -> (x == y)
  -> Unit
UnitEqElim _ = MkUnit

||| Unit identity introduction rule.
UnitEqIntro :
     {x, y : Unit}
  -> Unit
  -> (x == y)
UnitEqIntro {x = MkUnit, y = MkUnit} _ = Refl MkUnit

||| Unit identity introduction rule is a quasi-inverse of
||| its elimination rule.
UnitEqQInv : {x, y : Unit} -> QInv (UnitEqElim {x, y})
UnitEqQInv = UnitEqIntro
           # (\MkUnit => Refl MkUnit)
           # (\(Refl MkUnit) => Refl (Refl MkUnit))

||| Unit identity introduction & elimination rules
||| form an equivalence.
UnitEqIsEquiv : {x, y : Unit} -> IsEquiv (UnitEqElim {x, y})
UnitEqIsEquiv = QInvIsEquiv {f = UnitEqElim} (UnitEqQInv {x, y})

||| Propositional uniqueness principle for Unit.
UnitUniqueness : (z : Unit) -> z == MkUnit
UnitUniqueness z = UnitEqIntro {x = z, y = MkUnit} MkUnit

||| Any two inhabitants of an equivalence of some function
||| are identified.
EquivUniqueness :
    (f : a -> b)
 -> (e1, e2 : IsEquiv f)
 -> e1 == e2
-- e : g . f ~~ id
-- q : h . f ~~ id

-- e' : f . g' ~~ id
-- q' : f . h' ~~ id

-- ? :
EquivUniqueness f ((g # e) # (g' # e')) ((h # q) # (h' # q')) =
  PairEqIntro (?a # ?b)
  -- TODO

||| Pi identity elimination rule.
HApply :
     {p : a -> Type}
  -> {f, g : (x : a) -> p x}
  -> (f == g)
  -> f ~~ g
HApply (Refl f) = HomotopyRefl f

||| Function extensionality is introduced
||| as an axiom of the Type Theory.
||| Nonetheless, it has a computational meaning (?).
FunEqIsEquiv :
     {p : a -> Type}
  -> {f, g : (x : a) -> p x}
  -> IsEquiv (HApply {p, f, g})
FunEqIsEquiv = ((\x => axiom (Refl f)) # (\x => axiom (Refl (HomotopyRefl f))))
             # ((\x => axiom (Refl f)) # (\x => axiom (Refl (Refl f))))

||| Pi identity introduction rule.
||| Also known as "function extensionality".
FunExt :
     {p : a -> Type}
  -> {f, g : (x : a) -> p x}
  -> f ~~ g
  -> (f == g)
FunExt = pr1 $ EquivIsQInv {f = HApply} (FunEqIsEquiv {p, f, g})

||| Pi identity computation rule.
||| Follows from the postulated equivalence.
FunEqCompute :
     {p : a -> Type}
  -> {x : _}
  -> {f, g : (x : a) -> p x}
  -> (h : f ~~ g)
  -> HApply (FunExt h) x == h x
FunEqCompute h =
  let (p1 # _) = pr2 $ EquivIsQInv {f = HApply} (FunEqIsEquiv {p, f, g})
  in ap ($ x) (p1 h)

||| Propositional uniqueness principle for Pi types.
FunUniqueness :
     {p : a -> Type}
  -> {f, g : (x : a) -> p x}
  -> f == (\x => f x)
FunUniqueness = FunExt {f, g = \x => f x} (HomotopyRefl f)

||| Propositional uniqueness principle for Pi identities.
FunEqUniqueness :
     {p : a -> Type}
  -> {f, g : (x : a) -> p x}
  -> (u : f == g)
  -> u == FunExt (\x => HApply u x)
FunEqUniqueness u =
  let (_ # p2) = pr2 $ EquivIsQInv {f = HApply} (FunEqIsEquiv {p, f, g})
  in sym (p2 u)


text:
module Main

fact : Nat -> Nat
fact 0 = 1
fact (S k) = (S k) * (fact k)

main : IO ()
main = putStrLn $ show $ fact 1000


text:
module Main

rec : Int -> Int -> Int
rec 0 y = y
rec 1 y = y
rec x y =
   rec (y-1) (x-2)

f : (Int -> Int -> Int) -> Int -> Int -> Int
f op x y = op x y

main : IO ()
main = do
	fn <- pure rec
	print (f fn 10 5)


text:
module Python.Functions

import Python.Objects
import Python.Fields
import Python.Telescope
import Python.IO

%default total
%access public export

Function : (t : Telescope a) -> Signature
Function {a = a} t f = case f of
  "__call__" => Call {a = a} t
  _ => Object f

infix 5 ~>
||| Infix alias for functions with fixed arguments.
(~>) : List Type -> Type -> Type
(~>) args ret = Obj . Function $ simple args ret

infix 5 ~~>
(~~>) : List Type -> Type -> Field
(~~>) args ret = Attr $ args ~> ret

fun : (t : Telescope a) -> Field
fun t = Attr . Obj $ Function t

||| Strip the given tuple `xs` to the list of runtime-relevant values.
strip : (t : Telescope a) -> (args : a) -> List Dyn
strip (Return _)              ()        = []
strip (Bind (Pi      _  ) tf) (x ** xs) = toDyn x :: strip (tf x) xs
strip (Bind (Forall  _  ) tf) (x ** xs) = strip (tf x) xs
strip (Bind (Default _ d) tf) (x ** xs) = toDyn x :: strip (tf $ fromMaybe d x) xs

infixl 4 $.
||| Duck-typed function call.
($.) :
  {t : Telescope a}
  -> (f : Obj sig)
  -> {auto pf : sig "__call__" = Call t}
  -> (args : a)
  -> PIO $ retTy t args
($.) {t = t} (MkObj f) args =
  unRaw <$>
    foreign FFI_Py "_idris_call"
      (Ptr -> List Dyn -> PIO (Raw $ Telescope.retTy t args))
      f
      (strip t args)

infixl 4 $:
||| Duck-typed function call, useful for chaining.
($:) :
  {t : Telescope a}
  -> (f : PIO (Obj sig))
  -> {auto pf : sig "__call__" = Call t}
  -> (args : a)
  -> PIO $ retTy t args
($:) meth args = meth >>= \m => m $. args

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Main

import Graphics.SDL2.SDL

import Control.Algebra
import Data.Matrix

import Graphics.Util.Transforms
import Graphics.Util.ObjLoader
import Graphics.Util.Mesh
import Graphics.Rendering.Gl
import Graphics.Rendering.Config

%include C "GL/glew.h"
%flag C "-Wno-pointer-sign"

||| contains the display / viewport dimension
record Display where
  constructor MkDisplay
  width : Int
  height : Int

||| returns the aspect ratio of a disply
aspectRatio : Display -> Double
aspectRatio (MkDisplay width height) = (cast width) / (cast height)

||| camera parameterers
||| the values in this data type will be used to calculate the view and perspective
||| projection matrices
record Camera where
  constructor MkCamera
  ||| the 3D position of the camera
  position : Vec3
  ||| field of view of the camera
  fov : Angle
  ||| near plane limit of the camera frustum
  nearPlane : Double
  ||| far plane limit of the camera frustum
  farPlane : Double
  ||| the direction of the camera as a vector
  direction : Vec3

record ShaderLocations where
  constructor Locs
  viewMatrixLocation : Int

record State where
  constructor MkState
  renderer: SDLRenderer
  window: SDLWindow
  display : Display
  camera  : Camera
  locations: ShaderLocations
  entities : List (Entity String)

updateCameraPosition : State -> (Vec3 -> Vec3) -> State
updateCameraPosition state f = record { camera->position = f (record {camera->position} state) } state

update: Event -> State -> State
update (KeyDown (KeyAny 'w'))  state = updateCameraPosition state (\p => p <-> [0,    0,    0.05])
update (KeyDown (KeyAny 's'))  state = updateCameraPosition state (\p => p <+> [0,    0,    0.05])
update (KeyDown (KeyAny 'a'))  state = updateCameraPosition state (\p => p <-> [0.05, 0,    0])
update (KeyDown (KeyAny 'd'))  state = updateCameraPosition state (\p => p <+> [0.05, 0,    0])
update (KeyDown KeyUpArrow)    state = updateCameraPosition state (\p => p <+> [0,    0.05, 0])
update (KeyDown KeyDownArrow)  state = updateCameraPosition state (\p => p <-> [0,    0.05, 0])
update (KeyDown _)             state = state
update (KeyUp x)               state = state
update (MouseMotion x y dx dy) state = state
update (MouseButtonDown x y z) state = state
update (MouseButtonUp x y z)   state = state
update (MouseWheel x)          state = state
update (Resize x y)            state = state
update AppQuit                 state = state
update WindowEvent             state = state

setViewMatrix : State -> Entity String -> String -> IO ()
setViewMatrix state (SimpleEntity _ _ entityPosition rotation location _) s = do
  let pos = entityPosition <-> (record { camera->position } state)
  let transform = (translate pos) <> (rotate rotation) <> (scaleAll 1)
  glUniformMatrix4fv location 1 0 (toList $ toGl transform)

draw : State -> IO ()
draw state = do
                glClearColor 0.2 0.2 0.2 1
                glClear GL_COLOR_BUFFER_BIT
                glClear GL_DEPTH_BUFFER_BIT

                let locView = record {locations->viewMatrixLocation} state
                let cameraDirection = record {camera->direction} state
                glUniformMatrix4fv locView 1 0 (toList $ toGl $ standardViewMatrix cameraDirection)

                traverse (\entity => render entity (setViewMatrix state entity)) (entities state)

                glSwapWindow $ window state

camera : Camera
camera = MkCamera [0.0, 0.0, 0.0] (Degree 45) 0.1 100.0 [0.0, 0.0, -1.0]

display : Display
display = MkDisplay 800 600

main : IO ()
main = do
          initSDL
          glSetAttribute SDL_GL_CONTEXT_PROFILE_MASK (toSDLInt SDL_GL_CONTEXT_PROFILE_CORE)
          glSetAttribute SDL_GL_CONTEXT_MAJOR_VERSION 4
          glSetAttribute SDL_GL_CONTEXT_MINOR_VERSION 1
          glSetAttribute SDL_GL_ACCELERATED_VISUAL 1
          glSetAttribute SDL_GL_DOUBLEBUFFER  1
          glSetAttribute SDL_GL_DEPTH_SIZE 16

          (win,renderer) <- startSDL "Hello Idris" 800 600
          ctx <- createGLContext win
          glMakeCurrent win ctx

          glSetSwapInterval 1

          glewInit
          info <- glGetInfo
          putStrLn info
          glEnable GL_DEPTH_TEST
          glDepthFunc GL_LESS

          texture <- loadTexture "stone.png" 0
          plane <- loadObj "stone.obj"
          planeModel <- createModel plane [texture]

          shader <- createShaders [(GL_VERTEX_SHADER, "shader.vert"), (GL_FRAGMENT_SHADER, "shader.frag")]
          traverse printShaderLog  (shaders shader)
          glUseProgram $ program shader

          locView <- glGetUniformLocation (program shader) "viewMatrix"
          glUniformMatrix4fv locView 1 0 (toList $ toGl $ viewMatrix [0,0,-1] [0,0,0] [0,1,0])

          locProj <- glGetUniformLocation (program shader) "projectionMatrix"
          let projM = perspectiveProjection (fov camera) (aspectRatio display) ((nearPlane camera), (farPlane camera))
          glUniformMatrix4fv locProj 1 0 (toList $ toGl projM)

          loc <- glGetUniformLocation (program shader) "transformMatrix"

          let entity = SimpleEntity planeModel shader [0,-0.5,-3] [(Degree 0),(Degree 0),(Degree 0)] loc "Test"

          let initialState = MkState renderer win display camera (Locs locView) [entity]
          eventLoop initialState
          deleteModel planeModel
          deleteShaders shader
          deleteTextures [texture]
          --deleteGLContext ctx
          endSDL win renderer
          pure ()
       where
         eventLoop : State -> IO ()
         eventLoop state = do
                         e <- pollEvent
                         case e of
                           Just AppQuit => return ()
                           Just event   => do
                             draw state
                             --handle r event
                             --putStrLn $ "event" ++ (show event)
                             eventLoop $ update event state
                           _            => eventLoop state

max_stars_repo_name: spearman/gl-idris

max_issues_repo_name: spearman/gl-idris

max_forks_repo_name: spearman/gl-idris


text:
module TakeN

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

total
takeN : (n : Nat) -> (xs : List a) -> TakeN xs
takeN Z xs = Exact []
takeN (S k) [] = Fewer
-- takeN (S k) (x :: xs) = case takeN k xs of
--   Fewer => Fewer
--   Exact n_xs => Exact (x :: n_xs)
takeN (S k) (x :: xs) with (takeN k xs)
  takeN (S k) (x :: xs) | Fewer = Fewer
  takeN (S k) (x :: _) | Exact n_xs = Exact (x :: n_xs)

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

halves : List a -> (List a, List a)
halves xs with (takeN ((length xs) `div` 2) xs)
  halves _ | Fewer = ([], []) -- impossible?
  halves (lft ++ rgt) | Exact _ = (lft, rgt)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module LongestNonRepeatingSubstring

Set : Type -> Type
Set = List

contains : Eq a => a -> Set a -> Bool
contains x [] = False
contains x (y :: ys) = (x == y) || contains x ys

add : a -> Set a -> Set a
add x xs = x :: xs

emptySet : {0 a : Type} -> Set a
emptySet = []

longestHelp : {0 a : Type} -> Eq a => Set a -> Int -> Int -> List a -> Int
longestHelp seen count soFar [] = max soFar count
longestHelp seen count soFar (x :: xs) =
  if contains x seen then longestHelp (emptySet {a}) 0 (max soFar count) (x :: xs) else
  longestHelp (add x seen) (count + 1) soFar xs

longest : Eq a => List a -> Int
longest = longestHelp (emptySet {a}) 0 0

test1 : longest (unpack "abcabcbb") = 3
test1 = Refl
test2 : longest (unpack "bbbbb") = 1
test2 = Refl
test3 : longest (unpack "pwwkew") = 3
test3 = Refl
test4 : longest (unpack "") = 0
test4 = Refl


text:
module Fold

import Data.Strings

%default total

totalLen : List String -> Nat
totalLen = foldr (\str, acc => length str + acc) 0

{-
  interface Foldable (t : Type -> Type) where
    foldr : (a -> b -> b) -> b -> t a -> b
    foldl : (b -> a -> b) -> b -> t a -> b

  Foldable List where
    foldr func acc [] = acc
    foldr func acc (x :: xs) = func x (foldr func acc xs)

    foldl func acc [] = acc
    foldl func acc (x :: xs) = foldl func (func acc x) xs

-}

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris