text:
module Core.Primitives

import Core.Core
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

b8max : Int
b8max = 0x100

b16max : Int
b16max = 0x10000

b32max : Integer
b32max = 4294967296

b64max : Integer
b64max = 18446744073709551616 -- 0x10000000000000000

bitCastWrap : (i : Integer) -> (max : Integer) -> Integer
bitCastWrap i max
    = if i >= 0 -- oops, we don't have `rem` yet!
        then i `mod` max
        else max + i `mod` max

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 $ bitCastWrap (the Integer $ cast i) b32max)))
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 i))
castInteger [NPrimVal fc (I16 i)] = Just (NPrimVal fc (BI i))
castInteger [NPrimVal fc (I32 i)] = Just (NPrimVal fc (BI i))
castInteger [NPrimVal fc (I64 i)] = Just (NPrimVal fc (BI 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 (bitCastWrap (the Integer $ cast i) b32max)))
castInteger [NPrimVal fc (B64 i)] = Just (NPrimVal fc (BI 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 (fromInteger i)))
castInt [NPrimVal fc (I16 i)] = Just (NPrimVal fc (I (fromInteger i)))
castInt [NPrimVal fc (I32 i)] = Just (NPrimVal fc (I (fromInteger i)))
castInt [NPrimVal fc (I64 i)] = Just (NPrimVal fc (I (fromInteger i)))
castInt [NPrimVal fc (BI i)] = Just (NPrimVal fc (I (fromInteger i)))
castInt [NPrimVal fc (B8 i)] = Just (NPrimVal fc (I i))
castInt [NPrimVal fc (B16 i)] = Just (NPrimVal fc (I i))
castInt [NPrimVal fc (B32 i)] = Just (NPrimVal fc (I i))
castInt [NPrimVal fc (B64 i)] = Just (NPrimVal fc (I (fromInteger 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

bit8CastWrap : (i : Int) -> Int
bit8CastWrap i = cast $ bitCastWrap (cast i) (cast b8max)

bit16CastWrap : (i : Int) -> Int
bit16CastWrap i = cast $ bitCastWrap (cast i) (cast b16max)

bit32CastWrap : (i : Int) -> Int
bit32CastWrap i = cast $ bitCastWrap (cast i) b32max

bit64CastWrap : (i : Integer) -> Integer
bit64CastWrap i = bitCastWrap i b64max

int8max : Integer
int8max = 0x80

int16max : Integer
int16max = 0x8000

int32max : Integer
int32max = 0x80000000

int64max : Integer
int64max = 0x8000000000000000

intCastWrap : (i : Integer) -> (max : Integer) -> Integer
intCastWrap i max =
  let max2 = 2*max
      i2   = i `mod` max2
      i3   = if i2 < 0 then i2 + max2 else i2
   in if i3 >= max then i3 - max2 else i3

int8CastWrap : (i : Integer) -> Integer
int8CastWrap i = intCastWrap i int8max

int16CastWrap : (i : Integer) -> Integer
int16CastWrap i = intCastWrap i int16max

int32CastWrap : (i : Integer) -> Integer
int32CastWrap i = intCastWrap i int32max

int64CastWrap : (i : Integer) -> Integer
int64CastWrap i = intCastWrap i int64max

constantIntegerValue : Constant -> Maybe Integer
constantIntegerValue (I i)   = Just $ cast i
constantIntegerValue (I8 i)   = Just i
constantIntegerValue (I16 i)   = Just i
constantIntegerValue (I32 i)   = Just i
constantIntegerValue (I64 i)   = Just 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 i
constantIntegerValue _       = Nothing

castBits8 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits8 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = bitCastWrap value (cast b8max)
    pure (NPrimVal fc (B8 (cast wrapped)))
castBits8 _ = Nothing

castBits16 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits16 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = bitCastWrap value (cast b16max)
    pure (NPrimVal fc (B16 (cast wrapped)))
castBits16 _ = Nothing

castBits32 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits32 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = bitCastWrap value b32max
    pure (NPrimVal fc (B32 (cast wrapped)))
castBits32 _ = Nothing

castBits64 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits64 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = bitCastWrap value b64max
    pure (NPrimVal fc (B64 wrapped))
castBits64 _ = Nothing

castInt8 : Vect 1 (NF vars) -> Maybe (NF vars)
castInt8 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = int8CastWrap value
    pure (NPrimVal fc (I8 wrapped))
castInt8 _ = Nothing

castInt16 : Vect 1 (NF vars) -> Maybe (NF vars)
castInt16 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = int16CastWrap value
    pure (NPrimVal fc (I16 wrapped))
castInt16 _ = Nothing

castInt32 : Vect 1 (NF vars) -> Maybe (NF vars)
castInt32 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = int32CastWrap value
    pure (NPrimVal fc (I32 wrapped))
castInt32 _ = Nothing

castInt64 : Vect 1 (NF vars) -> Maybe (NF vars)
castInt64 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = int64CastWrap value
    pure (NPrimVal fc (I64 wrapped))
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 (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 _ = 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 (int8CastWrap $ x + y)
add (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ x + y)
add (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ x + y)
add (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ x + y)
add (B8 x) (B8 y) = pure $ B8 $ (x + y) `mod` b8max
add (B16 x) (B16 y) = pure $ B16 $ (x + y) `mod` b16max
add (B32 x) (B32 y) = pure $ B32 $ cast $ (cast (x + y)) `mod` b32max
add (B64 x) (B64 y) = pure $ B64 $ (x + y) `mod` b64max
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 (int8CastWrap $ x - y)
sub (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ x - y)
sub (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ x - y)
sub (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ x - y)
sub (B8 x) (B8 y) = pure $ B8 (bit8CastWrap $ x - y)
sub (B16 x) (B16 y) = pure $ B16 (bit16CastWrap $ x - y)
sub (B32 x) (B32 y) = pure $ B32 (bit32CastWrap $ x - y)
sub (B64 x) (B64 y) = pure $ B64 (bit64CastWrap $ 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) `mod` b8max
mul (B16 x) (B16 y) = pure $ B16 $ (x * y) `mod` b16max
mul (B32 x) (B32 y) = pure $ B32 $ cast $ (cast (x * y)) `mod` b32max
mul (B64 x) (B64 y) = pure $ B64 $ (x * y) `mod` b64max
mul (I x) (I y) = pure $ I (x * y)
mul (I8 x) (I8 y) = pure $ I8 (int8CastWrap $ x * y)
mul (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ x * y)
mul (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ x * y)
mul (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ 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 (int8CastWrap $ assert_total (x `div` y))
div (I16 x) (I16 0) = Nothing
div (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ assert_total (x `div` y))
div (I32 x) (I32 0) = Nothing
div (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ assert_total (x `div` y))
div (I64 x) (I64 0) = Nothing
div (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ assert_total (x `div` y))
div (B8 x) (B8 0) = Nothing
div (B8 x) (B8 y) = pure $ B8 (bit8CastWrap $ assert_total (x `div` y))
div (B16 x) (B16 0) = Nothing
div (B16 x) (B16 y) = pure $ B16 (bit16CastWrap $ assert_total (x `div` y))
div (B32 x) (B32 0) = Nothing
div (B32 x) (B32 y) = pure $ B32 (bit32CastWrap $ assert_total (x `div` y))
div (B64 x) (B64 0) = Nothing
div (B64 x) (B64 y) = pure $ B64 (bit64CastWrap $ 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 (int8CastWrap $ assert_total (x `mod` y))
mod (I16 x) (I16 0) = Nothing
mod (I16 x) (I16 y) = pure $ I16 (int16CastWrap $ assert_total (x `mod` y))
mod (I32 x) (I32 0) = Nothing
mod (I32 x) (I32 y) = pure $ I32 (int32CastWrap $ assert_total (x `mod` y))
mod (I64 x) (I64 0) = Nothing
mod (I64 x) (I64 y) = pure $ I64 (int64CastWrap $ assert_total (x `mod` y))
mod (B8 x) (B8 0) = Nothing
mod (B8 x) (B8 y) = pure $ B8 (bit8CastWrap $ assert_total (x `mod` y))
mod (B16 x) (B16 0) = Nothing
mod (B16 x) (B16 y) = pure $ B16 (bit16CastWrap $ assert_total (x `mod` y))
mod (B32 x) (B32 0) = Nothing
mod (B32 x) (B32 y) = pure $ B32 (bit32CastWrap $ assert_total (x `mod` y))
mod (B64 x) (B64 0) = Nothing
mod (B64 x) (B64 y) = pure $ B64 (bit64CastWrap $ assert_total (x `mod` y))
mod _ _ = Nothing

-- Make sure a signed integer stays within bounds after a
-- bitwise shift operation. If, after the shift, the highest bit
-- is set, treat the result as a negative number, computing its
-- twos complement, otherwise treat it as a positive number,
-- truncating all bits above the highest one.
signedShift : (i : Integer) -> (max : Integer) -> Integer
signedShift i max =
  if prim__and_Integer i max == 0
     then prim__and_Integer i (max - 1) -- treat as positive number: highest bit unset
     else prim__or_Integer i (-max)     -- treat as negative number: highest bit set

shiftl : Constant -> Constant -> Maybe Constant
shiftl (I x) (I y) = pure $ I (prim__shl_Int x y)
shiftl (I8 x) (I8 y) = pure $ I8 (signedShift (prim__shl_Integer x y) int8max)
shiftl (I16 x) (I16 y) = pure $ I16 (signedShift (prim__shl_Integer x y) int16max)
shiftl (I32 x) (I32 y) = pure $ I32 (signedShift (prim__shl_Integer x y) int32max)
shiftl (I64 x) (I64 y) = pure $ I64 (signedShift (prim__shl_Integer x y) int64max)
shiftl (BI x) (BI y) = pure $ BI (prim__shl_Integer x y)
shiftl (B8 x) (B8 y) = pure $ B8 $ (prim__shl_Int x y) `mod` b8max
shiftl (B16 x) (B16 y) = pure $ B16 $ (prim__shl_Int x y) `mod` b16max
shiftl (B32 x) (B32 y) = pure $ B32 $ cast $ (cast (prim__shl_Int x y)) `mod` b32max
shiftl (B64 x) (B64 y) = pure $ B64 $ (prim__shl_Integer x y) `mod` b64max
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 (signedShift (prim__shr_Integer x y) int8max)
shiftr (I16 x) (I16 y) = pure $ I16 (signedShift (prim__shr_Integer x y) int16max)
shiftr (I32 x) (I32 y) = pure $ I32 (signedShift (prim__shr_Integer x y) int32max)
shiftr (I64 x) (I64 y) = pure $ I64 (signedShift (prim__shr_Integer x y) int64max)
shiftr (B8 x) (B8 y) = pure $ B8 $ (prim__shr_Int x y)
shiftr (B16 x) (B16 y) = pure $ B16 $ (prim__shr_Int x y)
shiftr (B32 x) (B32 y) = pure $ B32 $ (prim__shr_Int x y)
shiftr (B64 x) (B64 y) = pure $ B64 $ (prim__shr_Integer 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_Integer x y)
band (I16 x) (I16 y) = pure $ I16 (prim__and_Integer x y)
band (I32 x) (I32 y) = pure $ I32 (prim__and_Integer x y)
band (I64 x) (I64 y) = pure $ I64 (prim__and_Integer x y)
band (BI x) (BI y) = pure $ BI (prim__and_Integer x y)
band (B8 x) (B8 y) = pure $ B8 (prim__and_Int x y)
band (B16 x) (B16 y) = pure $ B16 (prim__and_Int x y)
band (B32 x) (B32 y) = pure $ B32 (prim__and_Int x y)
band (B64 x) (B64 y) = pure $ B64 (prim__and_Integer 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_Integer x y)
bor (I16 x) (I16 y) = pure $ I16 (prim__or_Integer x y)
bor (I32 x) (I32 y) = pure $ I32 (prim__or_Integer x y)
bor (I64 x) (I64 y) = pure $ I64 (prim__or_Integer x y)
bor (BI x) (BI y) = pure $ BI (prim__or_Integer x y)
bor (B8 x) (B8 y) = pure $ B8 (prim__or_Int x y)
bor (B16 x) (B16 y) = pure $ B16 (prim__or_Int x y)
bor (B32 x) (B32 y) = pure $ B32 (prim__or_Int x y)
bor (B64 x) (B64 y) = pure $ B64 (prim__or_Integer 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_Int x y)
bxor (B16 x) (B16 y) = pure $ B16 (prim__xor_Int x y)
bxor (B32 x) (B32 y) = pure $ B32 (prim__xor_Int x y)
bxor (B64 x) (B64 y) = pure $ B64 (prim__xor_Integer x y)
bxor (I8 x) (I8 y) = pure $ I8 (prim__xor_Integer x y)
bxor (I16 x) (I16 y) = pure $ I16 (prim__xor_Integer x y)
bxor (I32 x) (I32 y) = pure $ I32 (prim__xor_Integer x y)
bxor (I64 x) (I64 y) = pure $ I64 (prim__xor_Integer 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 $ int8CastWrap (-x)
neg (I16 x) = pure . I16 $ int16CastWrap (-x)
neg (I32 x) = pure . I32 $ int32CastWrap (-x)
neg (I64 x) = pure . I64 $ int64CastWrap (-x)
neg (B8 x) = pure . B8 $ bit8CastWrap (-x)
neg (B16 x) = pure . B16 $ bit16CastWrap (-x)
neg (B32 x) = pure . B32 $ bit32CastWrap (-x)
neg (B64 x) = pure . B64 $ bit64CastWrap (-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] = Just (NType fc)
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) $
      pi "b" erased Explicit (TType emptyFC) $
      pi "x" top    Explicit (Local emptyFC Nothing _ (Later First)) $
      Local emptyFC Nothing _ (Later First)

crashTy : ClosedTerm
crashTy
    = pi "a" erased Explicit (TType emptyFC) $
      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 Sixel.Output

import System.FFI

import Sixel.Library
import Sixel.Symbols
import Sixel.Allocator

%default total

public export
PrimOutput : Type
PrimOutput = GCAnyPtr

public export
WriteFn : Type
WriteFn = (toWrite : AnyPtr) -> (size : Int) -> (priv : AnyPtr) -> PrimIO Int

MkOutputRes : Type
MkOutputRes = Struct "sixel_utils_output_t" [("output", AnyPtr), ("status", Int)]

export
data Output : (0 n : Nat) -> Type where
  PointOutput : PrimOutput -> Output Z
  RootOutput  : Output n -> Output (S n)

%foreign (sixelutils "sixel_utils_output_ptr_new")
sixel_utils_output_ptr_new : PrimIO (Ptr AnyPtr)

%foreign (sixelutils "sixel_utils_output_ptr_deref")
sixel_utils_output_ptr_deref : Ptr AnyPtr -> AnyPtr

%foreign (sixel "sixel_output_new")
sixel_output_new : Ptr AnyPtr -> WriteFn -> (priv : AnyPtr) -> PrimAllocator -> PrimIO Int

%foreign (sixel "sixel_output_ref")
sixel_output_ref : PrimOutput -> ()

%foreign (sixel "sixel_output_unref")
sixel_output_unref : PrimOutput -> ()

%foreign (sixel "sixel_output_destroy")
sixel_output_destroy : AnyPtr -> PrimIO ()

%foreign (sixel "sixel_output_get_8bit_availability")
sixel_output_get_8bit_availability : PrimOutput -> Int

%foreign (sixel "sixel_output_set_8bit_availability")
sixel_output_set_8bit_availability : PrimOutput -> Int -> ()

%foreign (sixel "sixel_output_set_gri_arg_limit")
sixel_output_set_gri_arg_limit : PrimOutput -> Int -> ()

%foreign (sixel "sixel_output_set_penetrate_multiplexer")
sixel_output_set_penetrate_multiplexer : PrimOutput -> Int -> ()

%foreign (sixel "sixel_output_set_skip_dcs_envelope")
sixel_output_set_skip_dcs_envelope : PrimOutput -> Int -> ()

%foreign (sixel "sixel_output_set_palette_type")
sixel_output_set_palette_type : PrimOutput -> Int -> ()

%foreign (sixel "sixel_output_set_encode_policy")
sixel_output_set_encode_policy : PrimOutput -> Int -> ()

export
MkOutput : {auto n : Nat} ->
  WriteFn ->
  {default prim__getNullAnyPtr priv : AnyPtr} ->
  {default (getNullAllocator n) alloc : Allocator n} ->
  IO (Either Status (Output Z))
MkOutput writefn {priv} {alloc} = do
  ppoutput <- fromPrim sixel_utils_output_ptr_new
  status   <- MkStatus <$> fromPrim (sixel_output_new ppoutput writefn priv (toPrim alloc))
  poutput  <- onCollectAny (sixel_utils_output_ptr_deref ppoutput) (\po => fromPrim $ sixel_output_destroy po)
  pure $ if succeeded status then Right (PointOutput poutput) else Left status

export
ref : Output n -> IO (Output (S n))
ref (RootOutput output)          = RootOutput <$> ref output
ref output@(PointOutput poutput) = let _ = sixel_output_ref poutput in pure $ RootOutput output

export
unref : Output (S n) -> IO (Output n)
unref (RootOutput output@(RootOutput _))        = RootOutput <$> unref output
unref (RootOutput output@(PointOutput poutput)) = let _ = sixel_output_unref poutput in pure output

export
refs : Output n -> Nat
refs (RootOutput output) = S (refs output)
refs (PointOutput _)     = Z

export
toPrim : Output n -> PrimOutput
toPrim (RootOutput output)   = toPrim output
toPrim (PointOutput poutput) = poutput

export %inline
get8BitAvailability : Output n -> IO Bool
get8BitAvailability output =
  pure $ intToBool $ sixel_output_get_8bit_availability $ toPrim output

export %inline
set8BitAvailability : Output n -> (setting : Bool) -> IO ()
set8BitAvailability output setting =
  pure $ sixel_output_set_8bit_availability (toPrim output) (ifThenElse setting 1 0)

export %inline
setGriArgLimit : Output n -> (setting : Bool) -> IO ()
setGriArgLimit output setting =
  pure $ sixel_output_set_gri_arg_limit (toPrim output) (ifThenElse setting 1 0)

export %inline
setPenetrateMultiplexer : Output n -> (setting : Bool) -> IO ()
setPenetrateMultiplexer output setting =
  pure $ sixel_output_set_penetrate_multiplexer (toPrim output) (ifThenElse setting 1 0)

export %inline
setSkipDcsEnvelope : Output n -> (setting : Bool) -> IO ()
setSkipDcsEnvelope output setting =
  pure $ sixel_output_set_skip_dcs_envelope (toPrim output) (ifThenElse setting 1 0)

export %inline
setPaletteType : Output n -> PaletteType -> IO ()
setPaletteType output type =
  pure $ sixel_output_set_palette_type (toPrim output) (binding type)

export %inline
setEncodePolicy : Output n -> EncodePolicy -> IO ()
setEncodePolicy output policy =
  pure $ sixel_output_set_encode_policy (toPrim output) (binding policy)

ext: idr

max_stars_repo_name: Kaiepi/id-sixel

max_issues_repo_name: Kaiepi/id-sixel

max_forks_repo_name: Kaiepi/id-sixel


text:
module Circuits.NetList.Parser

import Data.Nat
import Data.List1

import Circuits.Common.Lexer
import Circuits.Common.Parser

import Circuits.NetList.Types
import Circuits.NetList.AST
import Circuits.NetList.Lexer

import Circuits.NetList.Core

%default total

namespace Direction
  export
  direction : Rule Direction
  direction = gives "inout"  INOUT
          <|> gives "input"  INPUT
          <|> gives "output" OUTPUT

namespace Kinds

  export
  gateUnaryKind : Rule Unary.Kind
  gateUnaryKind
           =  gives "not" NOT

  export
  gateBinaryKind : Rule Binary.Kind
  gateBinaryKind
           =  gives "nand" ANDN
          <|> gives "and"  AND
          <|> gives "xor"  XOR
          <|> gives "xnor" XORN
          <|> gives "or"  IOR
          <|> gives "nor" IORN

namespace Terms

  portDecl : Rule (Location, Ref, Direction, DType)
  portDecl
    = do s <- Toolkit.location
         d <- direction
         t <- type
         r <- ref
         pure (s,r,d,t)

  portList : Rule (List1 (Location,Ref, Direction, DType))
  portList
    = do symbol "("
         ps <- sepBy1 (symbol ",") portDecl
         symbol ")"
         symbol ";"
         pure ps

  shim : Direction -> Rule AST -> Rule AST
  shim d port
    = do s <- Toolkit.location
         p <- port
         e <- Toolkit.location
         pure (Shim (newFC s e) d p)

  port : Direction -> Rule AST
  port d
      = (shim d idx) <|> (shim d ref')
    where

      ref' : Rule AST
      ref' = pure (Var !ref)

      value : Rule (Pair Nat Location)
      value
        = do symbol "["
             n <- nat
             symbol "]"
             e <- Toolkit.location
             pure (n,e)

      indices : Rule (List1 (Nat, Location))
      indices
        = some value

      build : Location
            -> AST
            -> List1 (Nat,Location)
            -> AST
      build s first (x:::xs)
        = foldl (\i, (n,e) => Index (newFC s e) n i) first (x::xs)

      idx : Rule AST
      idx
        = do s <- Toolkit.location
             r <- ref'
             is <- indices
             pure (build s r is)

  data Body = WDecl  FileContext DType Ref
            | GInst  FileContext Binary.Kind Ref AST AST AST
            | NInst  FileContext Unary.Kind Ref AST AST
            | MInst  FileContext Ref AST AST AST AST
            | AInst  FileContext AST AST
            | CInst  FileContext Ref AST AST AST
            | SInst  FileContext Ref AST AST AST

  assign : Rule Body
  assign
    = do s <- Toolkit.location
         keyword "assign"
         o <- port OUTPUT
         symbol "="
         i <- port INPUT
         symbol ";"
         e <- Toolkit.location
         pure (AInst (newFC s e) o i)

  gateNot : Rule Body
  gateNot
    = do s <- Toolkit.location
         k <- gateUnaryKind
         n <- ref
         symbol "("
         o <- port OUTPUT
         symbol ","
         i <- port INPUT
         symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (NInst (newFC s e) k n o i)

  gateBin : Rule Body
  gateBin
    = do s <- Toolkit.location
         k <- gateBinaryKind
         n <- ref
         symbol "("
         o <- port OUTPUT
         symbol ","
         a <- port INPUT
         symbol ","
         b <- port INPUT
         symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (GInst (newFC s e) k n o a b)

  gateMux : Rule Body
  gateMux
    = do s <- Toolkit.location
         keyword "mux"
         n <- ref
         symbol "("
         o <- port OUTPUT
         symbol ","
         c <- port INPUT
         symbol ","
         a <- port INPUT
         symbol ","
         b <- port INPUT
         symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (MInst (newFC s e) n o c a b)

  collect : Rule Body
  collect
    = do s <- Toolkit.location
         keyword "collect"
         n <- ref
         symbol "("
         o <- port OUTPUT
         symbol ","
         a <- port INPUT
         symbol ","
         b <- port INPUT
         symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (CInst (newFC s e) n o a b)

  split : Rule Body
  split
    = do s <- Toolkit.location
         keyword "split"
         n <- ref
         symbol "("
         o <- port OUTPUT
         symbol ","
         a <- port OUTPUT
         symbol ","
         b <- port INPUT
         symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (SInst (newFC s e) n o a b)

  wireDecl : Rule Body
  wireDecl
      = do s <- Toolkit.location
           keyword "wire"
           t <- type
           a <- ref
           symbol ";"
           e <- Toolkit.location
           pure (WDecl (newFC s e) t a)

  expr : Rule Body
  expr = assign <|> wireDecl <|> gateNot <|> gateBin <|> gateMux

  foldBody : Location
          -> List Body
          -> AST
  foldBody l bs
        = foldr doFold (Stop (newFC l l)) bs
    where
      doFold : Body -> AST -> AST

      doFold (WDecl x y z)
        = Wire x y z

      doFold (MInst v n w x y z)
        = GateDecl v n (Mux v w x y z)

      doFold (GInst x k n y z w)
        = GateDecl x n (GateB x k y z w)

      doFold (NInst x k n y z)
        = GateDecl x n (GateU x k y z)

      doFold (AInst fc o i)
        = Assign fc o i

      doFold (CInst fc n o a b)
        = GateDecl fc n (Collect fc o a b)

      doFold (SInst fc n o a b)
        = GateDecl fc n (Split fc o a b)

  foldPorts : Location
           -> List1 (Location,Ref, Direction, DType)
           -> AST
           -> AST
  foldPorts e (x:::xs) y
    = foldr (\(s,r,d,t), body => Port (newFC s e) d t r body) y (x::xs)

  export
  design : Rule AST
  design
    = do keyword "module"
         n <- ref
         ps <- portList
         b <- many expr
         e <- Toolkit.location
         keyword "endmodule"
         symbol ";"
         pure (foldPorts e ps (foldBody e b))

namespace NetList

  export
  fromFile : (fname : String)
                   -> NetList AST
  fromFile fname
    = do ast <- parseFile (Parse fname)
                NetList.Lexer
                design
                fname
         pure (setSource fname ast)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module GameServer.Protocol.Binary

import Data.List
import Network.Socket.Raw
import System

||| Returns an unsigned `Integer` value as a list of bytes
mkBytes : List Int -> Integer -> List Int
mkBytes acc 0 = acc
mkBytes acc n =
  let m = n `mod` 256
      q = n `div` 256
  in mkBytes (cast m :: acc) q

export
readBytes : (ptr: BufPtr) -> (offset:Integer) -> (len: Int) -> List Int -> IO (List Int)
readBytes _  _ 0 acc = pure acc
readBytes ptr offset n acc =
  do byte <- sock_peek ptr (cast offset + n-1)
     readBytes ptr offset (n-1) (byte :: acc)

export
putBytes : (ptr: BufPtr) -> (offset:Integer) -> (len:Int) -> List Int -> IO ()
putBytes ptr offset len bs = putBytes' len bs
  where
    putBytes' : (len:Int) -> List Int -> IO ()
    putBytes' 0 bs = pure ()
    putBytes' n (b::bs) = do
      sock_poke ptr (cast offset + len - n) b
      putBytes' (n-1) bs

mkInteger : (acc:Integer) -> (x:Int) -> Integer
mkInteger acc x = acc * 256 + cast x

padding : Integer -> Nat -> List Int
padding pad len = replicate (fromInteger $ pad - cast len) (the Int 0)

||| Writes an unsigned `Integer` value as a 64 bits in big endian form
||| into a buffer.
||| It assumes that 1/ the Integer is no larger than 2^63 -1 to fit
||| into 64 bits and 2/ the `ptr` points to a buffer with enough
||| room to fit 8 bytes
export
write64be : Integer -> (ptr: BufPtr) -> IO ()
write64be val ptr =
  do let bytes = mkBytes [] val
     let bytes8 = padding 8 (length bytes) ++ bytes
     putBytes ptr 0 8 bytes8

||| Read a 64 bits big endian value as an unsigned `Integer`
||| Assumes there are at least 8 bytes in the buffer pointed at by
||| `ptr`
export
read64be : (ptr: BufPtr) -> IO Integer
read64be ptr =
  do bytes <- readBytes ptr 0 8 []
     pure $ foldl mkInteger 0 bytes

export
write32be :  Integer -> (offset : Int) -> (ptr: BufPtr) -> IO ()
write32be val offset ptr =
  do let bytes = mkBytes [] val
     let bytes8 = padding 8 (length bytes) ++ bytes
     putBytes ptr (cast offset) 8 bytes8

||| Read a 32 bits big endian value as an unsigned `Integer`
||| Assumes there are at least 8 bytes in the buffer pointed at by
||| `ptr`
export
read32be : (ptr: BufPtr) -> (offset : Integer) -> IO Integer
read32be ptr offset =
  do bytes <- readBytes ptr offset 4 []
     pure $ foldl mkInteger 0 bytes

||| Read a length-encoded string from given buffers
||| Strings are assumed to be encoded as a 32 big endian length and
||| followed by utf8 encoded number of bytes
export
readString : (ptr : BufPtr) -> (offset : Integer) -> IO (String, Integer)
readString ptr offset =
  do len <- read32be ptr offset
     chars <- map chr <$> readBytes ptr (offset+4) (cast len) []
     pure $ (pack chars, offset+4+len)

export
writeString : (ptr : BufPtr) -> (offset : Integer) -> String -> IO Integer
writeString ptr offset str =
  do let chars = unpack str
     let len = length chars
     write32be (cast len) (cast offset) ptr
     putBytes ptr (offset + 4) (cast len) (map ord chars)
     pure $ offset + 4 + cast len

namespace Test

  export
  test_parseLength : IO Integer
  test_parseLength = do
    len_buf <- sock_alloc 8
    write64be 12345678901234567 len_buf
    read64be len_buf

  export
  test_parseLength2 : IO Integer
  test_parseLength2 = do
    len_buf <- sock_alloc 8
    write64be (-12345678901234567) len_buf
    read64be len_buf

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
||| Tests that no duplication occurs in recursive calls
||| as fixed in #1494
import Data.List

ints : List Int
ints = [1..100]

main : IO ()
main = printLn $ span (80 >=) ints


text:
module Specdris.TestUtil

import System

%access export

total
testAndPrint : (Show a, Eq a) => (info : String) -> a -> a -> (a -> a -> Bool) -> IO ()
testAndPrint info a b predicate
  = if predicate a b then
      pure ()
    else do
      putStrLn $ " - FAILED  " ++ info ++ ":\nactual   = " ++ show a ++ "\nexpected = " ++ show b
      exitFailure

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
module Editor

import Data.Fuel
import State
import InsertInput
import NormalInput
import EditorMode
import Document
import Cursor
import Data.Fin

%default total

normalModeChange : Maybe NormalInput -> EditorMode
normalModeChange (Just NormalInsert) = Insert
normalModeChange (Just NormalInsertNewLine) = Insert
normalModeChange (Just NormalInsertNewLineUp) = Insert
normalModeChange (Just NormalInsertRight) = Insert
normalModeChange (Just NormalInsertBeginningOfLine) = Insert
normalModeChange (Just NormalInsertEndOfLine) = Insert
normalModeChange (Just NormalChangeUntilNextWord) = Insert
normalModeChange (Just NormalChangeAWord) = Insert
normalModeChange (Just NormalQuit) = Quit
normalModeChange _ = Normal

insertModeChange : InsertInput -> EditorMode
insertModeChange (InsertChar _) = Insert
insertModeChange InsertNewLine = Insert
insertModeChange InsertNormal = Normal
insertModeChange InsertBackspace = Insert

data Command : (ty : Type) -> EditorMode -> (ty -> EditorMode) -> Type where
  GetNormalInput : Command (Maybe NormalInput) Normal (\input => normalModeChange input)
  GetInsertInput : Command InsertInput Insert (\input => insertModeChange input)
  ShowState : State -> Command () s (const s)
  Save : State -> Command () Normal (const Normal)
  Pure : a -> Command a s (const s)
  (>>=) : Command a state1 state2_fn ->
          ((res: a) -> Command b (state2_fn res) state3_fn) ->
          Command b state1 state3_fn

export
data RunCommand : EditorMode -> Type where
  Do : Command a state1 state2_fn ->
       ((res: a) -> Inf (RunCommand (state2_fn res))) ->
       RunCommand state1
  Stop : RunCommand Quit

namespace RunCommandDo
  (>>=) : Command a state1 state2_fn ->
          ((res: a) -> Inf (RunCommand (state2_fn res))) ->
          RunCommand state1
  (>>=) = Do

mutual
  export
  normalEditor : State -> RunCommand Normal
  normalEditor state = do
    ShowState state
    maybeInput <- GetNormalInput
    let (MkState doc) = state
    case maybeInput of
      Nothing => normalEditor state
      Just NormalInsert => insertEditor state
      Just NormalInsertNewLine => insertEditor $ MkState $ cursorDownNewLine doc
      Just NormalInsertNewLineUp => insertEditor $ MkState $ cursorUp $ newLine $ cursorBeginningOfLine $ doc --todo: this should be simpler
      Just NormalInsertRight => insertEditor $ MkState $ cursorRight doc
      Just NormalInsertBeginningOfLine => insertEditor $ MkState $ cursorBeginningOfLine doc
      Just NormalInsertEndOfLine => insertEditor $ MkState $ cursorRight $ cursorEndOfLine doc
      Just NormalUp => normalEditor $ MkState $ cursorUp doc
      Just NormalLeft => normalEditor $ MkState $ cursorLeft doc
      Just NormalRight => normalEditor $ MkState $ cursorRight doc
      Just NormalDown => normalEditor $ MkState $ cursorDownInBounds doc
      Just NormalDeleteAt => normalEditor $ MkState (deleteAt doc)
      Just NormalDeleteLine => normalEditor $ MkState (deleteLine doc)
      Just NormalDeleteUntilNextWord => normalEditor $ MkState (deleteUntilNextWord doc)
      Just NormalChangeUntilNextWord => insertEditor $ MkState (deleteUntilNextWord doc)
      Just NormalDeleteAWord => normalEditor $ MkState (deleteAWord doc)
      Just NormalChangeAWord => insertEditor $ MkState (deleteAWord doc)
      Just NormalTop => normalEditor $ MkState $ cursorTop doc
      Just NormalBottom => normalEditor $ MkState $ cursorBottom doc
      Just NormalBeginningOfLine => normalEditor $ MkState $ cursorBeginningOfLine doc
      Just NormalEndOfLine => normalEditor $ MkState $ cursorEndOfLine doc
      Just NormalEndOfWord => normalEditor $ MkState $ cursorEndOfWord doc
      Just NormalBeginningOfNextWord => normalEditor $ MkState $ cursorBeginningOfNextWord doc
      Just NormalBeginningOfWord => normalEditor $ MkState $ cursorBeginningOfWord doc
      Just NormalPageUp => normalEditor $ MkState $ cursorPageUp doc
      Just NormalPageDown => normalEditor $ MkState $ cursorPageDown doc
      Just NormalSave => do
        Save state
        normalEditor state
      Just NormalQuit => Stop

  export
  insertEditor : State -> RunCommand Insert
  insertEditor state = do
    ShowState state
    input <- GetInsertInput
    let (MkState doc) = state
    case input of
      (InsertChar c) => insertEditor $ MkState (insert doc c)
      InsertNewLine => insertEditor $ MkState (newLine doc)
      InsertNormal => normalEditor state
      InsertBackspace => insertEditor $ MkState (deleteBack doc)

private
runCommand : Command a s1 s2-> IO a
runCommand (Pure a) = pure a
runCommand GetNormalInput = getNormalInput
runCommand GetInsertInput = getInsertInput
runCommand (ShowState state) = showState state
runCommand (Save state) = saveDocument state
runCommand (cmdl >>= next) = do
  result <- runCommand cmdl
  runCommand (next result)

export
run : Fuel -> RunCommand s -> IO ()
run _ Stop = pure ()
run (More fuel) (Do cmd continuation) = do
  result <- runCommand cmd
  run fuel (continuation result)
run Dry _ = pure ()

max_stars_repo_name: PeterHajdu/peti

max_issues_repo_name: PeterHajdu/peti

max_forks_repo_name: PeterHajdu/peti


text:
module Core.Case.Util

import Core.Case.CaseTree
import Core.Context
import Core.Value

public export
record DataCon where
  constructor MkDataCon
  name  : Name
  tag   : Int
  arity : Nat

||| Given a normalised type, get all the possible constructors for that
||| type family, with their type, name, tag, and arity.
export
getCons : {auto c : Ref Ctxt Defs} ->
          {vars : _} ->
          Defs -> NF vars -> Core (List DataCon)
getCons defs (NTCon _ tn _ _ _)
    = case !(lookupDefExact tn (gamma defs)) of
           Just (TCon _ _ _ _ _ _ cons _) =>
                do cs' <- traverse addTy cons
                   pure (catMaybes cs')
           _ => throw (InternalError "Called `getCons` on something that is not a Type constructor")
  where
    addTy : Name -> Core (Maybe DataCon)
    addTy cn
        = do Just gdef <- lookupCtxtExact cn (gamma defs)
                  | _ => pure Nothing
             case (gdef.definition, gdef.type) of
                  (DCon t arity _, ty) =>
                        pure . Just $ MkDataCon cn t arity
                  _ => pure Nothing
getCons defs _ = pure []

emptyRHS : FC -> CaseTree vars -> CaseTree vars
emptyRHS fc (Case idx el sc alts) = Case idx el sc (map emptyRHSalt alts)
  where
    emptyRHSalt : CaseAlt vars -> CaseAlt vars
    emptyRHSalt (ConCase n t args sc) = ConCase n t args (emptyRHS fc sc)
    emptyRHSalt (DelayCase c arg sc) = DelayCase c arg (emptyRHS fc sc)
    emptyRHSalt (ConstCase c sc) = ConstCase c (emptyRHS fc sc)
    emptyRHSalt (DefaultCase sc) = DefaultCase (emptyRHS fc sc)
emptyRHS fc (STerm i s) = STerm i (Erased fc False)
emptyRHS fc sc = sc

export
mkAlt : {vars : _} ->
        FC -> CaseTree vars -> DataCon -> CaseAlt vars
mkAlt fc sc (MkDataCon cn t ar)
    = ConCase cn t (map (MN "m") (take ar [0..]))
              (weakenNs (map take) (emptyRHS fc sc))

export
tagIs : Int -> CaseAlt vars -> Bool
tagIs t (ConCase _ t' _ _) = t == t'
tagIs t (ConstCase _ _) = False
tagIs t (DelayCase _ _ _) = False
tagIs t (DefaultCase _) = True


text:
-- -------------------------------------------------------------- [ Reader.idr ]
-- Module      : XML.reader
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module XML.Serialise

import Commons.Data.Location

import XML.DOM
import XML.Lexer
import XML.Parser

%access private

public export
data XMLError : Type where
  ParseError     : Run.ParseError Token -> XMLError
  FileParseError : Run.ParseError Token -> String -> XMLError
  CannotReadFile : String -> FileError -> XMLError

public export
Show XMLError where
  show (ParseError err) =
    unlines [ unwords ["Error parsing was"]
            , case err of
               (FError e) => show e
               (PError e) => unlines [maybe "" show (location e), error e]
               (LError (MkLexFail l i)) => unlines [show l, show i]
            ]
  show (FileParseError err fn) =
    unlines [ unwords ["Error parsing file", show fn, "error was"]
            , case err of
               (FError e) => show e
               (PError e) => unlines [maybe "" show (location e), error e]
               (LError (MkLexFail l i)) => unlines [show l, show i]
            ]
  show (CannotReadFile fn err) =
    unlines [ unwords ["Cannot read file:", show fn, "error was"]
            , show err
            ]

namespace Doc
  export
  fromString : String -> Either XMLError (Document DOCUMENT)
  fromString str =
    case parseXMLDoc str of
      Left err  => Left $ ParseError err
      Right res => pure $ res

namespace Snippet
  export
  fromString : String -> Either XMLError (Document ELEMENT)
  fromString str = do
    case parseXMLSnippet str of
      Left err  => Left $ ParseError err
      Right res => pure $ res

interface XMLReader a where
  fromSnippet : XMLElem -> Either XMLError a
  fromXMLDoc  : XMLDoc  -> Either XMLError a

interface XMLWriter a where
  toXML   : a -> XMLElem

  toXMLDoc : a -> XMLDoc
  toXMLDoc o = mkSimpleDocument (toXML o)

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

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
module Main

import Data.SortedMap
import Data.SortedSet

data Node = MkNode String Int

Eq Node where
  (MkNode s1 i1) == (MkNode s2 i2) = s1 == s2 && i1 == i2

getName : Node -> String
getName (MkNode s _) = s

getWeight : Node -> Int
getWeight (MkNode _ i) = i

node0 : String -> Node
node0 s = MkNode s 0

data Graph = MkGraph (List (Node, List String))

mapGraph : (List (Node, List String) -> List (Node, List String)) -> Graph -> Graph
mapGraph f (MkGraph x) = MkGraph $ f x

inc : Node -> Node
inc (MkNode name i) = MkNode name $ i + 1

neighbors : Graph -> String -> Maybe (List String)
neighbors (MkGraph []) _ = Nothing
neighbors (MkGraph ((n, ss) :: ps)) s = if getName n == s then Just ss else neighbors (MkGraph ps) s

heaviest : (Maybe (Node, List String)) -> Graph -> Graph -> (Maybe (Node, List String), Graph, Graph)
heaviest n (MkGraph []) g = (n, MkGraph [], g)
heaviest mn (MkGraph ((n, ns) :: ps)) (MkGraph qs) =
  let w = getWeight n in
    if w > maybe (-1) (getWeight . fst) mn
      then heaviest (Just (n, ns)) (MkGraph ps) (MkGraph $ f mn)
      else heaviest mn (MkGraph ps) (MkGraph $ (n, ns) :: qs)
        where
          f Nothing = qs
          f (Just p) = p :: qs

first : (a -> b) -> (a, c) -> (b, c)
first f (x, y) = (f x, y)

incNeighbors : List String -> Graph -> Graph
incNeighbors _ (MkGraph []) = MkGraph []
incNeighbors ns (MkGraph (p :: ps)) =
  f $ if getName (fst p) `elem` ns
    then first inc
    else id
  where
    f : ((Node, List String) -> (Node, List String)) -> Graph
    f g = mapGraph (\x => g p :: x) $ incNeighbors ns $ MkGraph ps

-- Maximum cardinality search
mcs : Graph -> List (String, List String)
mcs g =
  let (qq, _, g') = heaviest Nothing g (MkGraph []) in
    case qq of
      Nothing => []
      Just (n, ns) => (getName n, ns) :: mcs (incNeighbors ns g')

Color : Type
Color = Int

lowest : List Color -> Color
lowest = f 0 . sort
  where
    f : Int -> List Color -> Color
    f n [] = n
    f n (c :: cs) = if n /= c then n else f (n + 1) cs

coloring' : List (String, List String) -> SortedMap String Color -> SortedMap String Color
coloring' [] m = m
coloring' ((name, ns) :: xs) m = coloring' xs $ insert name n m
  where
    f : List (Maybe a) -> List a
    f [] = []
    f (Nothing :: x) = f x
    f (Just a :: x) = a :: f x

    n : Color
    n = lowest $ f $ map (\n => lookup n m) ns

coloring : List (String, List String) -> SortedMap String Color
coloring xs = coloring' xs empty

namespace instruction
  data Inst = Mov String String | Add String String String

  Graph : Type
  Graph = SortedMap String (SortedSet String)

  update : Ord a => k -> SortedMap k (SortedSet a) -> (SortedSet a -> SortedSet a) -> SortedMap k (SortedSet a)
  update k m f = (\v => insert k v m) $ f $ fromMaybe empty $ lookup k m

  interfere : String -> instruction.Graph -> SortedSet String -> instruction.Graph
  interfere d g u = foldr (\x, acc => update x acc $ insert d) (update d g $ union u) u

  buildGraph : List Inst -> instruction.Graph
  buildGraph = snd . foldr (\i, acc => f i acc) (empty, empty)
    where
      f : Inst -> (SortedSet String, instruction.Graph) -> (SortedSet String, instruction.Graph)
      f (Mov d s)     (u, g) = (insert s $ delete d u             , interfere d g $ delete s $ delete d u)
      f (Add d s1 s2) (u, g) = (insert s2 $ insert s1 $ delete d u, interfere d g $ delete d u)

max_stars_repo_name: elpinal/regalloc

max_issues_repo_name: elpinal/regalloc

max_forks_repo_name: elpinal/regalloc


text:
> module SequentialDecisionProblems.TabBackwardsInduction

> import Data.Vect
> import Control.Isomorphism

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.Utils

> import Nat.Operations
> import Nat.OperationsProperties
> import Nat.LTEProperties
> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Decidable.Properties
> import Sigma.Sigma
> import Sigma.Operations
> import Pairs.Operations
> import Vect.Operations
> import Vect.Properties
> import Decidable.Predicates
> import Fin.Operations

> %default total
> %access public export
> %auto_implicits off

* Preliminaries

The major disadvantage of the generic backwards induction implementation
of the core theory

< bi : (t : Nat) -> (n : Nat) -> PolicySeq t n
< bi t  Z     =  Nil
< bi t (S n)  =  optExt ps :: ps where
<   ps : PolicySeq (S t) n
<   ps = bi (S t) n

is that its computational cost is exponential in the number of decidion
steps. Consider, for example, |bi 0 3|

< bi 0 3
<   = { def. |bi| }
< (optExt (bi 1 2)) :: (bi 1 2)
<   = { def. |bi| }
< (optExt ((optExt (bi 2 1)) :: (bi 2 1))) :: (optExt (bi 2 1)) :: (bi 2 1)
<   = { def. |bi| }
< (optExt ((optExt ((optExt (bi 3 0)) :: (bi 3 0))) :: (optExt (bi 3 0)) :: (bi 3 0))) ::
< (optExt ((optExt (bi 3 0)) :: (bi 3 0))) ::
< (optExt (bi 3 0)) ::
< (bi 3 0)
<   = { def. |bi| }
< (optExt ((optExt ((optExt Nil) :: Nil)) :: (optExt Nil) :: Nil)) ::
< (optExt ((optExt Nil) :: Nil)) ::
< (optExt Nil) ::
< Nil

resulting in

- 4 computations of |optExt Nil|
- 2 computations of |optExt ((optExt Nil) :: Nil)|
- 1 computation of |optExt ((optExt ((optExt Nil) :: Nil)) :: ((optExt Nil) :: Nil))|

or 7 calls to |optExt|. One more decision step implies 15 calls to
|optExt| suggesting that the number of calls to |optExt| for |n|
decision steps is |sum_{i = 0}^{n - 1} 2^j = (1 - 2^n) / (1 - 2)|.

* Towards a tail-recursive implementation

We can make the number of calls to |optExt| linear in |n| by rewriting
|bi| in tail-recursive form. The first step is to replace the recursive
call to |bi| with an iteration. Instead of pattern matching on the
number of steps, we delegate the computation of the policy sequence to
an auxiliary function |ibi| which implements backwards induction
iteratively:

> ||| Iterative backwards induction
> ibi : (t : Nat) -> (n : Nat) -> (c : Nat) -> LTE c n ->
>       PolicySeq (n - c + t) c -> PolicySeq t n
> ibi t n c prf ps with (n - c) proof itsEqual
>   |  Z    = replace {P = \ x => PolicySeq (Z + t) x} ceqn
>             ps where
>       ceqn : c = n
>       ceqn = minusLemma3 prf itsEqual
>   | (S m) = assert_total (ibi t n (S c) prf' ps') where
>       prf' : LTE (S c) n
>       prf' = minusLemma2 prf (sym itsEqual)
>       ps'  : PolicySeq (n - (S c) + t) (S c)
>       ps'  = replace {P = \ x => PolicySeq (x + t) (S c)} (minusLemma1 (sym itsEqual))
>              ((optExt ps) :: ps)

> ||| Tail-recursive backwardsinduction
> trbi : (t : Nat) -> (n : Nat) -> PolicySeq t n
> trbi t n = ibi t n Z LTEZero Nil

We can check that |trbi 0 3| and |bi 0 3| reduce to the same expression

< trbi 0 3
<   = { def. |trbi| }
< ibi 0 3 0 LTEZero Nil
<   = { def. |ibi| }
< ibi 0 3 1 (...) (optExt Nil) ::
<                 Nil
<   = {def. |ibi|}
< ibi 0 3 2 (...) (optExt ((optExt Nil) :: Nil)) ::
<                 (optExt Nil) ::
<                 Nil
<   = {def. |ibi|}
< ibi 0 3 3 (...) (optExt ((optExt ((optExt Nil) :: Nil)) :: (optExt Nil) :: Nil)) ::
<                 (optExt ((optExt Nil) :: Nil)) ::
<                 (optExt Nil) ::
<                 Nil
<   = {def. |ibi|}
< (optExt ((optExt ((optExt Nil) :: Nil)) :: (optExt Nil) :: Nil)) ::
< (optExt ((optExt Nil) :: Nil)) ::
< (optExt Nil) ::
< Nil

* Tabulation

If the state space is finite

> finiteState : (t : Nat) -> Finite (State t)

, we can compute the number of values of type |State t| and collect them
in a vector

> cardState : (t : Nat) -> Nat
> cardState t = card (finiteState t)

> vectState : (t : Nat) -> Vect (cardState t) (State t)
> vectState t = toVect (finiteState t)

If |Reachable| and |Viable n| are also decidable

> decidableReachable : {t' : Nat} -> (x' : State t') -> Dec (Reachable x')

< decidableViable : {t : Nat} -> (n : Nat) -> (x : State t) -> Dec (Viable n x)

then their conjunction

> ReachableAndViable : {t : Nat} -> (n : Nat) -> (x : State t) -> Type
> ReachableAndViable n x = (Reachable x , Viable n x)

is decidable

> decidableReachableAndViable : {t : Nat} -> (n : Nat) -> (x : State t) -> Dec (ReachableAndViable n x)
> decidableReachableAndViable n x = decPair (decidableReachable x) (decidableViable n x)

and we can collect all states which are reachable and viable in a vector:

> cardReachableAndViableState : (t : Nat) -> (n : Nat) -> Nat
> cardReachableAndViableState t n = outl (f t n) where
>   f : (t : Nat) -> (n : Nat) -> Sigma Nat (\ m => Vect m (Sigma (State t) (ReachableAndViable n)))
>   f t n = filterTagSigma (decidableReachableAndViable n) (vectState t)

> vectReachableAndViableState : (t : Nat) -> (n : Nat) ->
>                               Vect (cardReachableAndViableState t n) (Sigma (State t) (ReachableAndViable n))
> vectReachableAndViableState t n = outr (f t n) where
>   f : (t : Nat) -> (n : Nat) -> Sigma Nat (\ m => Vect m (Sigma (State t) (ReachableAndViable n)))
>   f t n = filterTagSigma (decidableReachableAndViable n) (vectState t)

In this case, we can implement a "tabulated" versions of |bi| which is
linear in the number of decidion steps. Remember that |optExt| takes a
policy sequence for |n| steps and computes a policy sequence for |n + 1|
steps:

< optExt : {t, n : Nat} ->
<          (ps : PolicySeq (S t) n) -> Policy t (S n)

The idea is to replace the |ps| argument of |optExt| with a "value
table" |vt : Vect (cardReachableAndViableState t n) Val| storing the
value, for every state in |vectReachableAndViableState (S t) n|, of
taking |n| decision steps with |ps| starting from that state:

> toptExt : {t, n : Nat} ->
>           (vt : Vect (cardReachableAndViableState (S t) n) Val) -> Policy t (S n)

We implement |toptExt| on the basis of the implementation of |optExt|
of the core theory. We start with a tabulated version of |sval|:

> tsval : {t,n : Nat} ->
>         (x  : State t) -> .(r  : Reachable x) -> .(v  : Viable (S n) x) ->
>         (gy  : GoodCtrl t x n) ->
>         (vt : Vect (cardReachableAndViableState (S t) n) Val) ->
>         PossibleNextState x (ctrl gy) -> Val
> {-
> tsval {t} {n} x r v gy vt (MkSigma x' x'emx') = reward t x y x' `plus` index k vt where
>   y   : Ctrl t x
>   y   = ctrl gy
>   mx' : M (State (S t))
>   mx' = nexts t x y
>   ar' : All Reachable mx'
>   ar' = reachableSpec1 x r y
>   av' : All (Viable n) mx'
>   av' = allViable gy
>   r' : Reachable x'
>   r' = allElemSpec0 x' mx' ar' x'emx'
>   v' : Viable n x'
>   v' = allElemSpec0 x' mx' av' x'emx'
>   rvxs : Vect (cardReachableAndViableState (S t) n) (State (S t))
>   rvxs = map outl (vectReachableAndViableState (S t) n)
>   k    : Fin (cardReachableAndViableState (S t) n)
>   k    = lookup x' rvxs prf' where
>     dRV : (x' : State (S t)) -> Dec (ReachableAndViable n x')
>     dRV = decidableReachableAndViable n
>     prf : Elem x' (vectState (S t))
>     prf = toVectComplete (finiteState (S t)) x'
>     prf' : Elem x' rvxs
>     prf' = filterTagSigmaLemma {P = ReachableAndViable n} dRV x' (vectState (S t)) prf (r',v')
> -}
> tsval {t} {n} x r v gy vt (MkSigma x' x'emx') =
>   let y    : Ctrl t x
>            = ctrl gy in
>   let mx'  : M (State (S t))
>            = nexts t x y in
>   let ar'  : All Reachable mx'
>            = reachableSpec1 x r y in
>   let av'  : All (Viable n) mx'
>            = allViable gy in
>   let r'   : Reachable x'
>            = allElemSpec0 x' mx' ar' x'emx' in
>   let v'   : Viable n x'
>            = allElemSpec0 x' mx' av' x'emx' in
>   let rvxs : Vect (cardReachableAndViableState (S t) n) (State (S t))
>            = map outl (vectReachableAndViableState (S t) n) in
>   let dRV  : ((x' : State (S t)) -> Dec (ReachableAndViable n x'))
>            = decidableReachableAndViable n in
>   let prf  : Elem x' (vectState (S t))
>            = toVectComplete (finiteState (S t)) x' in
>   let prf' : Elem x' rvxs
>            = filterTagSigmaLemma {P = ReachableAndViable n} dRV x' (vectState (S t)) prf (r',v') in
>   let k    : Fin (cardReachableAndViableState (S t) n)
>            = lookup x' rvxs prf' in
>   reward t x y x' `plus` index k vt

Next, we implement a tabulated version of |cval|:

> tcval : {t, n : Nat} ->
>         (x  : State t) -> .(r  : Reachable x) -> .(v  : Viable (S n) x) ->
>         (vt : Vect (cardReachableAndViableState (S t) n) Val) ->
>         GoodCtrl t x n -> Val
> {-
> tcval {t} x r v vt gy = meas (fmap (tsval x r v gy vt) (tagElem mx')) where
>   y    : Ctrl t x
>   y    = ctrl gy
>   mx'  :  M (State (S t))
>   mx'  =  nexts t x y
> -}
> tcval {t} x r v vt gy = let y    : Ctrl t x
>                                  = ctrl gy in
>                         let mx'  : M (State (S t))
>                                  = nexts t x y in
>                         meas (fmap (tsval x r v gy vt) (tagElem mx'))

And finally

> tcvalargmax : {t, n : Nat} ->
>               (x  : State t) -> .(r : Reachable x) -> .(v : Viable (S n) x) ->
>               (vt : Vect (cardReachableAndViableState (S t) n) Val) -> GoodCtrl t x n

> toptExt {t} {n} vt = p where
>   p : Policy t (S n)
>   p x r v = tcvalargmax x r v vt

* Tabulated tail-recursive backwards induction

With |toptExt| in place, it is easy to implement a tabulated version of
|trbi|:

> ||| A table of the result of calling |flip val| (roughly) on a policy sequence
> ValueTable : Nat -> Nat -> Type
> ValueTable t n = Vect (cardReachableAndViableState t n) Val

> |||
> PolicySeqAndTab : Nat -> Nat -> Type
> PolicySeqAndTab t n = (PolicySeq t n, ValueTable t n)

> |||
> zeroVec : (n : Nat) -> Vect n Val
> zeroVec Z     = Nil
> zeroVec (S n) = zero :: zeroVec n

> ||| Tabulated tail-recursive backwards induction iteration
> ttrbii : (t : Nat) -> (n : Nat) -> (c : Nat) -> (LTE c n) ->
>          PolicySeq (c + t) (n - c) ->
>          (vt : Vect (cardReachableAndViableState (c + t) (n - c)) Val) ->
>          PolicySeq t n
>
> ttrbii t n  Z     prf ps vt = replace {P = \ z => PolicySeq t z} (minusZeroRight n) ps
>
> {-
> ttrbii t n (S c') prf ps vt = ttrbii t n c' prf' ps' vt'' where
>   bic  : S (n - S c') = n - c'
>   bic  = minusLemma4 prf
>   prf' : LTE c' n
>   prf' = lteLemma1 c' n prf
>   p    : Policy (c' + t) (S (n - S c'))
>   p    = toptExt vt
>   ps'  : PolicySeq (c' + t) (n - c')
>   ps'  = replace {P = \ z => PolicySeq (c' + t) z} bic (p :: ps)
>   vt'  : Vect (cardReachableAndViableState (c' + t) (S (n - S c'))) Val
>   vt'  = toVect vt'f where
>     vt'f : Fin (cardReachableAndViableState (c' + t) (S (n - S c'))) -> Val
>     vt'f k = tcval x r v vt (p x r v) where
>       xrv : Sigma (State (c' + t)) (ReachableAndViable (S (n - S c')))
>       xrv = index k (vectReachableAndViableState (c' + t) (S (n - S c')))
>       x   : State (c' + t)
>       x   = outl xrv
>       r   : Reachable {t' = c' + t} x
>       r   = fst (outr xrv)
>       v   : Viable {t = c' + t} (S (n - S c')) x
>       v   = snd (outr xrv)
>   vt''  : Vect (cardReachableAndViableState (c' + t) (n - c')) Val
>   vt''  = replace {P = \z => Vect (cardReachableAndViableState (c' + t) z) Val} bic vt'
> -}
> ttrbii t n (S c') prf ps vt =
>   let bic  : (S (n - S c') = n - c')
>            = minusLemma4 prf in
>   let prf' : LTE c' n
>            = lteLemma1 c' n prf in
>   let p    : Policy (c' + t) (S (n - S c'))
>            = toptExt vt in
>   let ps'  : PolicySeq (c' + t) (n - c')
>            = replace {P = \ z => PolicySeq (c' + t) z} bic (p :: ps) in
>   let xrv  -- : ((k : Fin (cardReachableAndViableState (c' + t) (S (n - S c')))) -> Sigma (State (c' + t)) (ReachableAndViable (S (n - S c'))))
>            = \ k => index k (vectReachableAndViableState (c' + t) (S (n - S c'))) in
>   let x    : ((k : Fin (cardReachableAndViableState (c' + t) (S (n - S c')))) -> State (c' + t))
>            = \ k => outl (xrv k) in
>   let r    : ((k : Fin (cardReachableAndViableState (c' + t) (S (n - S c')))) -> Reachable {t' = c' + t} (x k))
>            = \ k => fst (outr (xrv k)) in
>   let v    : ((k : Fin (cardReachableAndViableState (c' + t) (S (n - S c')))) -> Viable {t = c' + t} (S (n - S c')) (x k))
>            = \ k => snd (outr (xrv k)) in
>   let vt'f : (Fin (cardReachableAndViableState (c' + t) (S (n - S c'))) -> Val)
>            = \ k => tcval (x k) (r k) (v k) vt (p (x k) (r k) (v k)) in
>   let vt'  : Vect (cardReachableAndViableState (c' + t) (S (n - S c'))) Val
>            = toVect vt'f in
>   let vt'' : Vect (cardReachableAndViableState (c' + t) (n - c')) Val
>            = replace {P = \z => Vect (cardReachableAndViableState (c' + t) z) Val} bic vt' in
>   ttrbii t n c' prf' ps' vt''

> ||| Tabulated tail-recursive backwards induction
> tabTailRecursiveBackwardsInduction : (t : Nat) -> (n : Nat) -> PolicySeq t n
> tabTailRecursiveBackwardsInduction t n = ttrbii t n n (reflexiveLTE n) zps (zeroVec _) where
>   zps : PolicySeq (n + t) (n - n)
>   zps = replace {P = \ z => PolicySeq (n + t) z} (minusZeroN n) Nil

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Scheme.Print

import Data.Vect
import Scheme.Core

%hide Data.Vect.(::)

%default total
%access public export

showSequence : Show a => List a -> String
showSequence = concat . intersperse " " . map show

showDotted : Show a => Maybe a -> String
showDotted Nothing  = ""
showDotted (Just x) = " . " ++ show x

Show SNum where
  show (SNExactInt n) = show n

Show SExp where
  -- Short special forms
  show (SECons (SESymbol "quote"           ) x) = "'"  ++ show x
  show (SECons (SESymbol "quasiquote"      ) x) = "`"  ++ show x
  show (SECons (SESymbol "unquote"         ) x) = ","  ++ show x
  show (SECons (SESymbol "unquote-splicing") x) = ",@" ++ show x
  show (SECons (SESymbol "lambda"          ) x) = "λ"  ++ show x

  -- Lists and dotted lists
  show (SECons x y) =
    assert_total $
    case listify $ SECons x y of
         (ss, md) => "(" ++ showSequence ss ++ showDotted md ++ ")"

  -- terminals
  show  SEUnit           = "()"
  show (SEVect    xs   ) = "#(" ++ assert_total (showSequence (toList xs)) ++ ")"
  show (SESymbol  t    ) = t
  show (SENum     sn   ) = show sn
  show (SEStr     s    ) = show s
  show (SEBool    False) = "#f"
  show (SEBool    True ) = "#t"
  show (SEChar    c    ) = "#\\" ++ case c of
                                         ' '  => "space"
                                         '\t' => "tab"
                                         '\n' => "newline"
                                         _    => pack [c]


text:
module Web.Raw.Xhr

import JS
import Web.Internal.XhrPrim
import Web.Internal.Types

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

namespace FormData

  export
  new : (form : Optional HTMLFormElement) -> JSIO FormData
  new a = primJS $ FormData.prim__new (toFFI a)

  export
  new' : JSIO FormData
  new' = primJS $ FormData.prim__new undef

  export
  append : (obj : FormData) -> (name : String) -> (value : String) -> JSIO ()
  append a b c = primJS $ FormData.prim__append a b c

  export
  append1 :  (0 _ : JSType t1)
          => {auto 0 _ : Elem Blob (Types t1)}
          -> (obj : FormData)
          -> (name : String)
          -> (blobValue : t1)
          -> (filename : Optional String)
          -> JSIO ()
  append1 a b c d = primJS $ FormData.prim__append1 a b (up c) (toFFI d)

  export
  append1' :  (0 _ : JSType t1)
           => {auto 0 _ : Elem Blob (Types t1)}
           -> (obj : FormData)
           -> (name : String)
           -> (blobValue : t1)
           -> JSIO ()
  append1' a b c = primJS $ FormData.prim__append1 a b (up c) undef

  export
  delete : (obj : FormData) -> (name : String) -> JSIO ()
  delete a b = primJS $ FormData.prim__delete a b

  export
  getAll :  (obj : FormData)
         -> (name : String)
         -> JSIO (Array (Union2 File String))
  getAll a b = primJS $ FormData.prim__getAll a b

  export
  get :  (obj : FormData)
      -> (name : String)
      -> JSIO (Maybe (NS I [ File , String ]))
  get a b = tryJS "FormData.get" $ FormData.prim__get a b

  export
  has : (obj : FormData) -> (name : String) -> JSIO Bool
  has a b = tryJS "FormData.has" $ FormData.prim__has a b

  export
  set : (obj : FormData) -> (name : String) -> (value : String) -> JSIO ()
  set a b c = primJS $ FormData.prim__set a b c

  export
  set1 :  (0 _ : JSType t1)
       => {auto 0 _ : Elem Blob (Types t1)}
       -> (obj : FormData)
       -> (name : String)
       -> (blobValue : t1)
       -> (filename : Optional String)
       -> JSIO ()
  set1 a b c d = primJS $ FormData.prim__set1 a b (up c) (toFFI d)

  export
  set1' :  (0 _ : JSType t1)
        => {auto 0 _ : Elem Blob (Types t1)}
        -> (obj : FormData)
        -> (name : String)
        -> (blobValue : t1)
        -> JSIO ()
  set1' a b c = primJS $ FormData.prim__set1 a b (up c) undef

namespace ProgressEvent

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem ProgressEventInit (Types t1)}
      -> (type : String)
      -> (eventInitDict : Optional t1)
      -> JSIO ProgressEvent
  new a b = primJS $ ProgressEvent.prim__new a (optUp b)

  export
  new' : (type : String) -> JSIO ProgressEvent
  new' a = primJS $ ProgressEvent.prim__new a undef

  export
  lengthComputable : (obj : ProgressEvent) -> JSIO Bool
  lengthComputable a = tryJS "ProgressEvent.lengthComputable"
                     $ ProgressEvent.prim__lengthComputable a

  export
  loaded : (obj : ProgressEvent) -> JSIO JSBits64
  loaded a = primJS $ ProgressEvent.prim__loaded a

  export
  total_ : (obj : ProgressEvent) -> JSIO JSBits64
  total_ a = primJS $ ProgressEvent.prim__total a

namespace XMLHttpRequest

  public export
  DONE : Bits16
  DONE = 4

  public export
  HEADERS_RECEIVED : Bits16
  HEADERS_RECEIVED = 2

  public export
  LOADING : Bits16
  LOADING = 3

  public export
  OPENED : Bits16
  OPENED = 1

  public export
  UNSENT : Bits16
  UNSENT = 0

  export
  new : JSIO XMLHttpRequest
  new = primJS $ XMLHttpRequest.prim__new

  export
  onreadystatechange :  XMLHttpRequest
                     -> Attribute False Maybe EventHandlerNonNull
  onreadystatechange v = fromNullablePrim "XMLHttpRequest.getonreadystatechange"
                                          prim__onreadystatechange
                                          prim__setOnreadystatechange
                                          v

  export
  readyState : (obj : XMLHttpRequest) -> JSIO Bits16
  readyState a = primJS $ XMLHttpRequest.prim__readyState a

  export
  response : (obj : XMLHttpRequest) -> JSIO Any
  response a = tryJS "XMLHttpRequest.response" $ XMLHttpRequest.prim__response a

  export
  responseText : (obj : XMLHttpRequest) -> JSIO String
  responseText a = primJS $ XMLHttpRequest.prim__responseText a

  export
  responseType : XMLHttpRequest -> Attribute True I XMLHttpRequestResponseType
  responseType v = fromPrim "XMLHttpRequest.getresponseType"
                            prim__responseType
                            prim__setResponseType
                            v

  export
  responseURL : (obj : XMLHttpRequest) -> JSIO String
  responseURL a = primJS $ XMLHttpRequest.prim__responseURL a

  export
  responseXML : (obj : XMLHttpRequest) -> JSIO (Maybe Document)
  responseXML a = tryJS "XMLHttpRequest.responseXML"
                $ XMLHttpRequest.prim__responseXML a

  export
  status : (obj : XMLHttpRequest) -> JSIO Bits16
  status a = primJS $ XMLHttpRequest.prim__status a

  export
  statusText : (obj : XMLHttpRequest) -> JSIO ByteString
  statusText a = primJS $ XMLHttpRequest.prim__statusText a

  export
  timeout : XMLHttpRequest -> Attribute True I Bits32
  timeout v = fromPrim "XMLHttpRequest.gettimeout"
                       prim__timeout
                       prim__setTimeout
                       v

  export
  upload : (obj : XMLHttpRequest) -> JSIO XMLHttpRequestUpload
  upload a = primJS $ XMLHttpRequest.prim__upload a

  export
  withCredentials : XMLHttpRequest -> Attribute True I Bool
  withCredentials v = fromPrim "XMLHttpRequest.getwithCredentials"
                               prim__withCredentials
                               prim__setWithCredentials
                               v

  export
  abort : (obj : XMLHttpRequest) -> JSIO ()
  abort a = primJS $ XMLHttpRequest.prim__abort a

  export
  getAllResponseHeaders : (obj : XMLHttpRequest) -> JSIO ByteString
  getAllResponseHeaders a = primJS
                          $ XMLHttpRequest.prim__getAllResponseHeaders a

  export
  getResponseHeader :  (obj : XMLHttpRequest)
                    -> (name : ByteString)
                    -> JSIO (Maybe ByteString)
  getResponseHeader a b = tryJS "XMLHttpRequest.getResponseHeader"
                        $ XMLHttpRequest.prim__getResponseHeader a b

  export
  open_ :  (obj : XMLHttpRequest)
        -> (method : ByteString)
        -> (url : String)
        -> JSIO ()
  open_ a b c = primJS $ XMLHttpRequest.prim__open a b c

  export
  open1 :  (obj : XMLHttpRequest)
        -> (method : ByteString)
        -> (url : String)
        -> (async : Bool)
        -> (username : Optional (Maybe String))
        -> (password : Optional (Maybe String))
        -> JSIO ()
  open1 a b c d e f = primJS
                    $ XMLHttpRequest.prim__open1 a
                                                 b
                                                 c
                                                 (toFFI d)
                                                 (toFFI e)
                                                 (toFFI f)

  export
  open1' :  (obj : XMLHttpRequest)
         -> (method : ByteString)
         -> (url : String)
         -> (async : Bool)
         -> JSIO ()
  open1' a b c d = primJS
                 $ XMLHttpRequest.prim__open1 a b c (toFFI d) undef undef

  export
  overrideMimeType : (obj : XMLHttpRequest) -> (mime : String) -> JSIO ()
  overrideMimeType a b = primJS $ XMLHttpRequest.prim__overrideMimeType a b

  export
  send :  (obj : XMLHttpRequest)
       -> (body : Optional (Maybe (NS I [ Document
                                        , Blob
                                        , Int8Array
                                        , Int16Array
                                        , Int32Array
                                        , UInt8Array
                                        , UInt8Array
                                        , UInt8Array
                                        , UInt8ClampedArray
                                        , Float32Array
                                        , Float64Array
                                        , DataView
                                        , ArrayBuffer
                                        , FormData
                                        , URLSearchParams
                                        , String
                                        ])))
       -> JSIO ()
  send a b = primJS $ XMLHttpRequest.prim__send a (toFFI b)

  export
  send' : (obj : XMLHttpRequest) -> JSIO ()
  send' a = primJS $ XMLHttpRequest.prim__send a undef

  export
  setRequestHeader :  (obj : XMLHttpRequest)
                   -> (name : ByteString)
                   -> (value : ByteString)
                   -> JSIO ()
  setRequestHeader a b c = primJS $ XMLHttpRequest.prim__setRequestHeader a b c

namespace XMLHttpRequestEventTarget

  export
  onabort :  (0 _ : JSType t)
          => {auto 0 _ : Elem XMLHttpRequestEventTarget (Types t)}
          -> t
          -> Attribute False Maybe EventHandlerNonNull
  onabort v = fromNullablePrim "XMLHttpRequestEventTarget.getonabort"
                               prim__onabort
                               prim__setOnabort
                               (v :> XMLHttpRequestEventTarget)

  export
  onerror :  (0 _ : JSType t)
          => {auto 0 _ : Elem XMLHttpRequestEventTarget (Types t)}
          -> t
          -> Attribute False Maybe EventHandlerNonNull
  onerror v = fromNullablePrim "XMLHttpRequestEventTarget.getonerror"
                               prim__onerror
                               prim__setOnerror
                               (v :> XMLHttpRequestEventTarget)

  export
  onload :  (0 _ : JSType t)
         => {auto 0 _ : Elem XMLHttpRequestEventTarget (Types t)}
         -> t
         -> Attribute False Maybe EventHandlerNonNull
  onload v = fromNullablePrim "XMLHttpRequestEventTarget.getonload"
                              prim__onload
                              prim__setOnload
                              (v :> XMLHttpRequestEventTarget)

  export
  onloadend :  (0 _ : JSType t)
            => {auto 0 _ : Elem XMLHttpRequestEventTarget (Types t)}
            -> t
            -> Attribute False Maybe EventHandlerNonNull
  onloadend v = fromNullablePrim "XMLHttpRequestEventTarget.getonloadend"
                                 prim__onloadend
                                 prim__setOnloadend
                                 (v :> XMLHttpRequestEventTarget)

  export
  onloadstart :  (0 _ : JSType t)
              => {auto 0 _ : Elem XMLHttpRequestEventTarget (Types t)}
              -> t
              -> Attribute False Maybe EventHandlerNonNull
  onloadstart v = fromNullablePrim "XMLHttpRequestEventTarget.getonloadstart"
                                   prim__onloadstart
                                   prim__setOnloadstart
                                   (v :> XMLHttpRequestEventTarget)

  export
  onprogress :  (0 _ : JSType t)
             => {auto 0 _ : Elem XMLHttpRequestEventTarget (Types t)}
             -> t
             -> Attribute False Maybe EventHandlerNonNull
  onprogress v = fromNullablePrim "XMLHttpRequestEventTarget.getonprogress"
                                  prim__onprogress
                                  prim__setOnprogress
                                  (v :> XMLHttpRequestEventTarget)

  export
  ontimeout :  (0 _ : JSType t)
            => {auto 0 _ : Elem XMLHttpRequestEventTarget (Types t)}
            -> t
            -> Attribute False Maybe EventHandlerNonNull
  ontimeout v = fromNullablePrim "XMLHttpRequestEventTarget.getontimeout"
                                 prim__ontimeout
                                 prim__setOntimeout
                                 (v :> XMLHttpRequestEventTarget)

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

namespace ProgressEventInit

  export
  new :  (lengthComputable : Optional Bool)
      -> (loaded : Optional JSBits64)
      -> (total_ : Optional JSBits64)
      -> JSIO ProgressEventInit
  new a b c = primJS $ ProgressEventInit.prim__new (toFFI a) (toFFI b) (toFFI c)

  export
  new' : JSIO ProgressEventInit
  new' = primJS $ ProgressEventInit.prim__new undef undef undef

  export
  lengthComputable :  (0 _ : JSType t)
                   => {auto 0 _ : Elem ProgressEventInit (Types t)}
                   -> t
                   -> Attribute True Optional Bool
  lengthComputable v = fromUndefOrPrim "ProgressEventInit.getlengthComputable"
                                       prim__lengthComputable
                                       prim__setLengthComputable
                                       False
                                       (v :> ProgressEventInit)

  export
  loaded :  (0 _ : JSType t)
         => {auto 0 _ : Elem ProgressEventInit (Types t)}
         -> t
         -> Attribute True Optional JSBits64
  loaded v = fromUndefOrPrim "ProgressEventInit.getloaded"
                             prim__loaded
                             prim__setLoaded
                             0
                             (v :> ProgressEventInit)

  export
  total_ :  (0 _ : JSType t)
         => {auto 0 _ : Elem ProgressEventInit (Types t)}
         -> t
         -> Attribute True Optional JSBits64
  total_ v = fromUndefOrPrim "ProgressEventInit.gettotal"
                             prim__total
                             prim__setTotal
                             0
                             (v :> ProgressEventInit)


text:
||| Spec: https://webassembly.github.io/spec/core/valid/types.html#memory-types
module WebAssembly.Validation.Types.MemoryTypes

import WebAssembly.Structure
import WebAssembly.Validation.Types.Limits

public export
MAX_LIMIT_MEMORY : Nat
MAX_LIMIT_MEMORY = power 2 4  -- set to (power 2 16) for original WebAssembly behvaiour WARNING: type-checking then takes like forever

-------------------------------------------------------------------------------
-- Validation Rules
-------------------------------------------------------------------------------

public export
data ValidMemoryType : MemType -> Type where
  |||
  |||   ⊢ limits : 2^16
  |||----------------------
  |||     ⊢ limits ok
  |||
  MkValidMemoryType : (limits: Limits) -> (limits_valid: ValidLimits limits MAX_LIMIT_MEMORY) -> ValidMemoryType limits

-------------------------------------------------------------------------------
-- Lemmas about memory-type validation
-------------------------------------------------------------------------------

total invalid_limit_mem : (contra : ValidLimits memType MAX_LIMIT_MEMORY -> Void) -> ValidMemoryType memType -> Void
invalid_limit_mem contra (MkValidMemoryType memType limits_valid) = contra limits_valid

-------------------------------------------------------------------------------
-- Decidability of validation
-------------------------------------------------------------------------------

total public export
isMemoryTypeValid : (memType : MemType) -> Dec (ValidMemoryType memType)
isMemoryTypeValid memType = case (isLimitsValid memType MAX_LIMIT_MEMORY) of
  No contra => No (invalid_limit_mem contra)
  Yes prof  => Yes (MkValidMemoryType memType prof)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Main

import Cairo

data Expr = Val Felt
          | Add Expr Expr

eval : Expr -> Felt
eval (Val f) = f
eval (Add l r) = eval l + eval r

%noinline
main : Cairo ()
main = output $ eval (Val 1 `Add` (Val 2 `Add` Val 3))

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
-- Define module to wrap constants starting with lower case to not
-- confuse them with implicitly bound argument.  See
-- https://docs.idris-lang.org/en/latest/faq/faq.html#why-can-t-i-use-a-function-with-no-arguments-in-a-type
module Main

import RealizedFunction

%default total

-- Realized incrementer
incrementer : Int -> Int
incrementer = (+1)
incrementer_attrs : RealizedAttributes
incrementer_attrs = MkRealizedAttributes (MkCosts 100 10 1) 1
rlz_incrementer : RealizedFunction (Int -> Int) Main.incrementer_attrs
rlz_incrementer = MkRealizedFunction incrementer incrementer_attrs

-- Realized twicer
twicer : Int -> Int
twicer = (*2)
twicer_attrs : RealizedAttributes
twicer_attrs = MkRealizedAttributes (MkCosts 200 20 2) 0.9
rlz_twicer : RealizedFunction (Int -> Int) Main.twicer_attrs
rlz_twicer = MkRealizedFunction twicer twicer_attrs

-- Realized halfer
halfer : Int -> Int
halfer = (flip div 2)
halfer_attrs : RealizedAttributes
halfer_attrs = MkRealizedAttributes (MkCosts 300 30 3) 0.8
rlz_halfer : RealizedFunction (Int -> Int) Main.halfer_attrs
rlz_halfer = MkRealizedFunction halfer halfer_attrs

-- Realized (twicer . incrementer).
rlz_compo1_attrs : RealizedAttributes
rlz_compo1_attrs = MkRealizedAttributes (MkCosts 300 30 3) 0.9
-- The following does not work because 301 ≠ 200+100
-- rlz_compo1_attrs = MkRealizedAttributes (MkCosts 301 30 3) 0.9
rlz_compo1 : RealizedFunction (Int -> Int) Main.rlz_compo1_attrs
rlz_compo1 = compose rlz_twicer rlz_incrementer

-- Realized (incrementer . twicer . halfer).
rlz_compo2_attrs : RealizedAttributes
rlz_compo2_attrs = MkRealizedAttributes (MkCosts 600 60 6) 0.8
-- The following does not work because 601 ≠ 300+200+100
-- rlz_compo2_attrs = MkRealizedAttributes (MkCosts 601 60 6) 0.8
rlz_compo2 : RealizedFunction (Int -> Int) Main.rlz_compo2_attrs
rlz_compo2 = (compose rlz_incrementer (compose rlz_twicer rlz_halfer))

-- Realized (halfer . incrementer . twicer).  If halfer can only take
-- an even integer, then such composition is not valid.
rlz_compo3_attrs : RealizedAttributes
rlz_compo3_attrs = MkRealizedAttributes (MkCosts 600 60 6) 0.8
rlz_compo3 : RealizedFunction (Int -> Int) Main.rlz_compo3_attrs
rlz_compo3 = (compose rlz_halfer (compose rlz_incrementer rlz_twicer))

-- Tests

-- Result should be (20+1)*2 = 42
lifted_compo1 : Int -> Int
lifted_compo1 = apply rlz_compo1
test1 : lifted_compo1 20 = 42
test1 = Refl

-- Result should be 1+2*(40/2) = 41
lifted_compo2 : Int -> Int
lifted_compo2 = apply rlz_compo2
test2 : lifted_compo2 40 = 41
test2 = Refl

-- Result should be (40*2+1)/2 = 40 [assuming no even integer
-- constraint on halfer's input].
lifted_compo3 : Int -> Int
lifted_compo3 = apply rlz_compo3
test2 : lifted_compo3 40 = 40
test2 = Refl

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Lambdapants.Environment

import Lambdapants.Term
import Lambdapants.Term.Nats
import Lambdapants.Term.Reduction

%default total

public export
Environment : Type
Environment = List (String, Term)

export
substEnv : Term -> Environment -> Term
substEnv = foldr (uncurry substitute)

export
encodeNats : Term -> Term
encodeNats = enc [] where
  enc : List String -> Term -> Term
  enc bound (Var name) =
    if not (elem name bound) && all isDigit (unpack name)
       then let num = cast name in
                if num > 800 -- Treat numbers larger than 800 as literals
                   then Var name
                   else encoded num
       else Var name
  enc bound (App t u) = App (enc bound t) (enc bound u)
  enc bound (Lam v t) = Lam v (enc (v :: bound) t)

export
closed : Term -> Environment -> Term
closed = substEnv . encodeNats

max_stars_repo_name: laserpants/redex-reflex

max_issues_repo_name: laserpants/lambdapants

max_forks_repo_name: laserpants/lambdapants


text:
-- Module      : Itea.Javascript.Types
-- Description :
-- Copyright   : (c) Simon Nielsen Knights 2018
-- License     : MIT
-- Maintainer  : simonank@mail.ru
-- Stability   : unstable
-- Portability : portable

module Itea.Javascript.Types
import Itea.Utils

%default total
%access public export

||| Opaque type for javascript references
data JSRef : Type -> Type where

||| Conversion from Idris values to Javascript values
interface Convertible a where
  convert : a -> Ptr
-- TODO Write implementations for more interesting structures

Convertible (JSRef a) where
  convert = believe_me

data JSType
  = JSNumber
  | JSString
  | JSBoolean
  | JSFunction
  | JSUndefined
  | JSObject String
  | JSNull

||| Return the constructor name
export
constructorName : JSRef a -> JS_IO String
constructorName = jscall "%0.constructor.name" (Ptr -> JS_IO String) . convert

||| Return the Javascript type of the given object
export
typeOf : JSRef a -> JS_IO JSType
typeOf p = case !(jscall check (Ptr -> JS_IO Int) (convert p)) of
                0 => pure JSNumber
                1 => pure JSString
                2 => pure JSBoolean
                3 => pure JSFunction
                4 => pure JSUndefined
                5 => pure $ JSObject !(constructorName p)
                _ => pure JSNull

  where

    check : String
    check ="""
(function (p) {
  if (typeof p == 'number') return 0;
  if (typeof p == 'string') return 1;
  if (typeof p == 'boolean') return 2;
  if (typeof p == 'function') return 3;
  if (typeof p == 'undefined') return 4;
  if (typeof p == 'object') return 5;
  return 6;})(%0)"""

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea


text:
-- ----------------------------------------------------------------- [ UML.idr ]
-- Module      : UML
-- Description : UML models in Idris
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML

import public UML.Class
import public UML.Sequence
import public UML.Deployment
import public UML.Component
import public UML.Code
import public UML.Types
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml