text:
module Test.Main

import Language.JSON
import JSON
import Hedgehog

import Generics.Derive

%language ElabReflection

--------------------------------------------------------------------------------
--          Fast Eq for Nat
--------------------------------------------------------------------------------

-- The default Eq for Nat runs in O(n), which leads to stack overflows
-- for large Nats
[FastNatEq] Eq Nat where
  (==) = (==) `on` natToInteger

-- The default Ord for Nat runs in O(n), which leads to stack overflows
-- for large Nats
[FastNatOrd] Ord Nat using FastNatEq where
  compare = compare `on` natToInteger

--------------------------------------------------------------------------------
--          Elab Deriving
--------------------------------------------------------------------------------

-- example newtype
record Newtype where
  constructor MkNewtype
  field : String

%runElab derive "Newtype" [Generic,Meta,Show,Eq,NewtypeToJSON,NewtypeFromJSON]

-- sum type with default encoding behavior: this will
-- be encoded as a mapping from constructor argument names
-- to values including a special field called "tag" with the
-- encoded constructor name.
data Sum : (a : Type) -> Type where
  Con1 : (name : String) -> (age : Bits32) -> (female : Bool) -> Sum a
  Con2 : (treasure : List a) -> (weight : Bits64) -> Sum a
  Con3 : (foo : Maybe a) -> (bar : Either Bool a) -> Sum a

%runElab derive "Sum" [Generic,Meta,Show,Eq,ToJSON,FromJSON]

-- this sum type will be encoded in the same manner as `Sum`
-- but without the additional "tag" field: This should
-- only be used if not two constructors have the same
-- type and field names.
data Sum2 : (a : Type) -> Type where
  Con21 : (name : String) -> (age : Bits32) -> (female : Bool) -> Sum2 a
  Con22 : (treasure : List a) -> (weight : Bits64) -> Sum2 a
  Con23 : (foo : Maybe a) -> (bar : Either Bool a) -> Sum2 a

%runElab derive "Sum2" [Generic,Meta,Show,Eq]

ToJSON a => ToJSON (Sum2 a) where
  toJSON = genToJSON UntaggedValue

FromJSON a => FromJSON (Sum2 a) where
  fromJSON = genFromJSON UntaggedValue

-- this sum type will be encoded as `Sum` but instead of adding
-- a "tag" for the constructor name, it will be wrapped up
-- as a single field object, the field being named as the
-- constructor used.
data Sum3 : (a : Type) -> Type where
  Con31 : (name : String) -> (age : Bits32) -> (female : Bool) -> Sum3 a
  Con32 : (treasure : List a) -> (weight : Bits64) -> Sum3 a
  Con33 : (foo : Maybe a) -> (bar : Either Bool a) -> Sum3 a

%runElab derive "Sum3" [Generic,Meta,Show,Eq]

ToJSON a => ToJSON (Sum3 a) where
  toJSON = genToJSON ObjectWithSingleField

FromJSON a => FromJSON (Sum3 a) where
  fromJSON = genFromJSON ObjectWithSingleField

-- this sum will be encoded as an array of two elements:
-- the first corresponding to the constructor name, the second
-- to the encoded value.
data Sum4 : (a : Type) -> Type where
  Con41 : (name : String) -> (age : Bits32) -> (female : Bool) -> Sum4 a
  Con42 : (treasure : List a) -> (weight : Bits64) -> Sum4 a
  Con43 : (foo : Maybe a) -> (bar : Either Bool a) -> Sum4 a

%runElab derive "Sum4" [Generic,Meta,Show,Eq]

ToJSON a => ToJSON (Sum4 a) where
  toJSON = genToJSON TwoElemArray

FromJSON a => FromJSON (Sum4 a) where
  fromJSON = genFromJSON TwoElemArray

-- this sum will be encoded as a tagged object with custom
-- names for the tag and content field
data Sum5 : (a : Type) -> Type where
  Con51 : (name : String) -> (age : Bits32) -> (female : Bool) -> Sum5 a
  Con52 : (treasure : List a) -> (weight : Bits64) -> Sum5 a
  Con53 : (foo : Maybe a) -> (bar : Either Bool a) -> Sum5 a

%runElab derive "Sum5" [Generic,Meta,Show,Eq]

ToJSON a => ToJSON (Sum5 a) where
  toJSON = genToJSON (TaggedObject "v" "c")

FromJSON a => FromJSON (Sum5 a) where
  fromJSON = genFromJSON (TaggedObject "v" "c")

-- since records have only one constructor, they can be encoded
-- without having to care about the different techniques to
-- distinguish between constructors
record ARecord where
  constructor MkRecord
  anInt   : Integer
  perhaps : Maybe (Sum Int)
  foo     : Either String Bool

%runElab derive "ARecord" [Generic,Meta,Show,Eq,RecordToJSON,RecordFromJSON]

-- enum types (all nullary constructors) can be encoded just
-- as a string representing the constructor's name
data Weekday = Monday
             | Tuesday
             | Wednesday
             | Thursday
             | Friday
             | Saturday
             | Sunday

%runElab derive "Weekday" [Generic,Meta,Show,Eq,EnumToJSON,EnumFromJSON]

--------------------------------------------------------------------------------
--          Generators
--------------------------------------------------------------------------------

bits8All : Gen Bits8
bits8All = bits8 $ linear 0 255

bits16All : Gen Bits16
bits16All = bits16 $ exponential 0 65535

bits32All : Gen Bits32
bits32All = bits32 $ exponential 0 4294967295

bits64All : Gen Bits64
bits64All = bits64 $ exponential 0 18446744073709551615

unicode16 : Gen Char
unicode16 = charc '\0' '\65535'

doubleE100 : Gen Double
doubleE100 = double $ exponentialFrom 0 (-1.0e100) 1.0e100

intAll : Gen Int
intAll = int $ exponential (-9223372036854775808) 9223372036854775807

integer128 : Gen Integer
integer128 = integer $ exponentialFrom 0 (-0x100000000000000000000000000000000) 0x100000000000000000000000000000000

nat128 : Gen Nat
nat128 = nat $ exponential @{FastNatOrd} 0 0x100000000000000000000000000000000

list20 : Gen a -> Gen (List a)
list20 = list (linear 0 20)

list1_20 : Gen a -> Gen (List1 a)
list1_20 = list1 (linear 1 20)

string20 : Gen Char -> Gen String
string20 = string $ linear 0 20

string20Ascii : Gen String
string20Ascii = string20 ascii

string20Unicode16 : Gen String
string20Unicode16 = string20 unicode16

vect13 : Gen a -> Gen (Vect 13 a)
vect13 = vect 13

newtype : Gen String
newtype = string20 unicode16

sumSop : Gen (SOP I [ [String,Bits32,Bool]
                    , [List Int, Bits64]
                    , [Maybe Int, Either Bool Int]
                    ])
sumSop = sop $ MkPOP [ [ string20 alphaNum, bits32All, bool ]
                       , [ list20 intAll, bits64All ]
                       , [ maybe intAll, either bool intAll ]
                       ]

sum : Gen (Sum Int)
sum = map to sumSop

rec : Gen ARecord
rec = map to $ sop $
      MkPOP [[integer128, maybe sum, either string20Unicode16 bool]]

weekday : Gen Weekday
weekday = element [Monday,Tuesday,Wednesday,Thursday,Friday,Saturday,Sunday]

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

roundTrip : Eq a => FromJSON a => ToJSON a => Show a => Gen a -> Property
roundTrip g = property $ do v <- forAll g
                            let enc = encode v
                            footnote enc
                            Right v === decode enc

prop_unit : Property
prop_unit = roundTrip $ pure ()

prop_bits8 : Property
prop_bits8 = roundTrip bits8All

prop_bits16 : Property
prop_bits16 = roundTrip bits16All

prop_bits32 : Property
prop_bits32 = roundTrip bits32All

prop_bits64 : Property
prop_bits64 = roundTrip bits64All

prop_bool : Property
prop_bool = roundTrip bool

prop_char : Property
prop_char = roundTrip unicode16

prop_double : Property
prop_double = roundTrip doubleE100

prop_either : Property
prop_either = roundTrip $ either bits8All ascii

prop_int : Property
prop_int = roundTrip intAll

prop_integer : Property
prop_integer = roundTrip integer128

prop_list : Property
prop_list = roundTrip $ list20 bits8All

prop_list1 : Property
prop_list1 = roundTrip $ list1_20 unicode16

prop_maybe : Property
prop_maybe = roundTrip $ maybe (either bool bits32All)

prop_nat : Property
prop_nat = roundTrip @{FastNatEq} nat128

prop_np : Property
prop_np = roundTrip $ np [ integer128, bool, unicode16, maybe string20Ascii ]

prop_ns : Property
prop_ns = roundTrip $ ns [ integer128, bool, unicode16, maybe string20Ascii ]

prop_pair : Property
prop_pair = roundTrip [| (,) (list1_20 bool) (maybe ascii) |]

prop_rec : Property
prop_rec = roundTrip rec

prop_newtype : Property
prop_newtype = roundTrip newtype

prop_string : Property
prop_string = roundTrip $ string20 unicode16

prop_sum : Property
prop_sum = roundTrip {a = Sum Int} (map to sumSop)

prop_sum2 : Property
prop_sum2 = roundTrip {a = Sum2 Int} (map to sumSop)

prop_sum3 : Property
prop_sum3 = roundTrip {a = Sum3 Int} (map to sumSop)

prop_sum4 : Property
prop_sum4 = roundTrip {a = Sum4 Int} (map to sumSop)

prop_sum5 : Property
prop_sum5 = roundTrip {a = Sum5 Int} (map to sumSop)

prop_vect : Property
prop_vect = roundTrip $ vect13 intAll

prop_weekday : Property
prop_weekday = roundTrip weekday

main : IO ()
main = test . pure $ MkGroup "JSON" [
            ("prop_bits8", prop_bits8)
          , ("prop_bits16", prop_bits16)
          , ("prop_bits32", prop_bits32)
          , ("prop_bits64", prop_bits64)
          , ("prop_bool", prop_bool)
          , ("prop_char", prop_char)
          , ("prop_double", prop_double)
          , ("prop_either", prop_either)
          , ("prop_int", prop_int)
          , ("prop_integer", prop_integer)
          , ("prop_list", prop_list)
          , ("prop_list1", prop_list1)
          , ("prop_maybe", prop_maybe)
          , ("prop_nat", prop_nat)
          , ("prop_newtype", prop_newtype)
          , ("prop_np", prop_np)
          , ("prop_ns", prop_ns)
          , ("prop_pair", prop_pair)
          , ("prop_rec", prop_rec)
          , ("prop_string", prop_string)
          , ("prop_sum", prop_sum)
          , ("prop_sum2", prop_sum2)
          , ("prop_sum3", prop_sum3)
          , ("prop_sum4", prop_sum4)
          , ("prop_sum5", prop_sum5)
          , ("prop_unit", prop_unit)
          , ("prop_vect", prop_vect)
          , ("prop_weekday", prop_weekday)
          ]


text:
module Data.Strong.Array

import public Data.IOArray.Prims
import Data.Nat

import Control.Monad.Identity
import Data.Zippable

import public Numeric.Floating

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

-- No good reason to hide the constructor just yet, safety can come later on
public export
data Array : Nat -> Type -> Type where
  MkArray : (size : Nat) -> (intSize : Int) -> (content : ArrayData a) -> Array size a

-- 0 so I don't have to remember where to erase it
0 lteReflexive : (j : Nat) -> LTE j j
lteReflexive j = reflexive {x=j}

export
size : Array s a -> Nat
size (MkArray s' intSize content) = s'

export
intSize : Array s a -> Int
intSize (MkArray s intSize' content) = intSize'

content : Array s a -> ArrayData a
content (MkArray s intSize c) = c

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

export
newArray : (s : Nat) -> (def : a) -> Array s a
newArray s x = unsafePerformIO $ do
    let intsize = cast s
    pure (MkArray s intsize !(primIO (prim__newArray intsize x)))

-- Consider relegating new array construction to ST, requiring a 'freeze' to say
-- we're done making it. This would make the mutable* methods below unneccesary
-- and we could remove them from public facing. I don't want to be that strict
-- until we have fusion though.
export
%inline
newArray' : {s:_} -> (def : a) -> Array s a
newArray' = newArray s

export
%inline
newUnintializedArray : (s : Nat) -> Array s a
newUnintializedArray s = newArray s (believe_me (the Int 0))

export
%inline
newUnintializedArray' : {s : Nat} -> Array s a
newUnintializedArray' = newUnintializedArray s

copyFrom : ArrayData elem ->
           ArrayData elem ->
           Int -> Int -> IO ()
copyFrom old new pos offset
    = if pos < 0
         then pure ()
         else do el <- primIO $ prim__arrayGet old pos
                 primIO $ prim__arraySet new (pos + offset) el
                 copyFrom old new (assert_smaller pos (pos - 1)) offset

export
||| You shouldn't need this yourself, other operations use this.
newArrayCopy : Array s a -> Array s a
newArrayCopy (MkArray s i contents) = unsafePerformIO $ do
    let new = newUnintializedArray s
    copyFrom contents (content new) (i - 1) 0
    pure new

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

export
||| This won't always be here
unsafeMutableWriteArray : HasIO io => Array s a -> (i : Nat) -> a -> io ()
unsafeMutableWriteArray arr i x = primIO (prim__arraySet (content arr) (cast i) x)

-- Consider an interface based on Int and So as an alternative.
export
%inline
||| This won't always be here
mutableWriteArray : HasIO io => Array s a -> (i : Nat) -> (0 prf : LTE i s) => a -> io ()
mutableWriteArray arr i x = unsafeMutableWriteArray arr i x

export
||| Don't use this unless you really just have one infrequent thing to change,
||| unsafeWriteArray copies the array every use.
unsafeWriteArray : Array s a -> (i : Nat) -> a -> Array s a
unsafeWriteArray arr i x = unsafePerformIO $ do
  let new = newArrayCopy arr
  unsafeMutableWriteArray new i x
  pure new

export
%inline
||| Don't use this unless you really just have one infrequent thing to change,
||| writeArray copies the array every use.
writeArray : Array s a -> (i : Nat) -> (0 prf : LTE i s) => a -> Array s a
writeArray arr i x = unsafeWriteArray arr i x

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

export
||| To match with unsafeMutableWriteArray in that it has io for
||| ordering ease-of-use.
unsafeMutableReadArray : HasIO io => Array s a -> (i : Nat) -> io a
unsafeMutableReadArray arr i = primIO (prim__arrayGet (content arr) (cast i))

export
unsafeReadArray : Array s a -> (i : Nat) -> a
unsafeReadArray arr i = unsafePerformIO $ unsafeMutableReadArray arr i

export
%inline
||| To match with unsafeMutableWriteArray in that it has io for
||| ordering ease-of-use, 'mutable' in name only.
mutableReadArray : HasIO io => Array s a -> (i : Nat) -> (0 prf : LTE i s) => io a
mutableReadArray arr i = unsafeMutableReadArray arr i

export
%inline
readArray : Array s a -> (i : Nat) -> (0 prf : LTE i s) => a
readArray arr i = unsafeReadArray arr i

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

export
||| Same caveat as writeArray
modifyArray : (a -> a) -> Array s a -> (i : Nat) -> LTE i s => Array s a
modifyArray f arr i = writeArray arr i (f (readArray arr i))

-- Keeping this around for now, Applicative version does the same job, but I'm
-- a little unsure about how I've written its `go`
export
imapArrayM' : Monad m => ((i : Nat) -> a -> m b) -> Array s a -> m (Array s b)
imapArrayM' f arr = case arr of
    MkArray s _ _ => do
      let new = newUnintializedArray {a=b} s
      let 0 prf = lteReflexive s
      go new s
  where
    go : Array s b -> (i : Nat) -> (0 prf : LTE i s) => m (Array s b)
    go new 0 = pure new
    go new (S k) = do
      let 0 newprf = lteSuccLeft prf
      let v = readArray arr k
      r <- f k v
      let () = unsafePerformIO $ mutableWriteArray new k r
      go new k

export
imapArrayM : Applicative f => ((i : Nat) -> a -> f b) -> Array s a -> f (Array s b)
imapArrayM g arr = case arr of
    MkArray s _ _ =>
      let new = newUnintializedArray {a=b} s
          0 prf = lteReflexive s
      in  go new s
  where
    go : Array s b -> (i : Nat) -> (0 prf : LTE i s) => f (Array s b)
    go new 0 = pure new
    go new (S k) =
      let 0 newprf = lteSuccLeft prf
          v = readArray arr k
          r = g k v
      in (\b => let () = unsafePerformIO $ mutableWriteArray new k b in id) <$> r <*> go new k

export
%inline
imapArray : ((i : Nat) -> a -> b) -> Array s a -> Array s b
imapArray f arr = runIdentity $ imapArrayM (Id .: f) arr

-- extra copy, but easy to write
export
%inline
inewArrayFillM : Monad m => (s : Nat) -> ((i : Nat) -> m a) -> m (Array s a)
inewArrayFillM s g = imapArrayM (\i,_ => g i) (newUnintializedArray {a} s)

export
%inline
inewArrayFill : (s : Nat) -> ((i : Nat) -> a) -> Array s a
inewArrayFill s g = runIdentity $ imapArrayM (\i,_ => Id (g i)) (newUnintializedArray {a} s)

-- this isn't really foldl, it's foldr but just reading the array in reverse, this should
-- be changed in the future so it's not surprising.
ifoldlArray : (b -> (i : Nat) -> a -> b) -> b -> Array s a -> b
ifoldlArray f acc arr = case arr of
    MkArray s _ _ => let 0 prf = lteReflexive s in go s
  where
    go : (i : Nat) -> (0 prf : LTE i s) => b
    go 0 = acc
    go (S k) =
      let 0 newprf = lteSuccLeft prf
      in f (go k) k (readArray arr k)

export
||| I expect this will dissapear from the api once fusion exists
ifoldl2Array : (b -> (i1,i2 : Nat) -> a -> a -> b) -> b -> Array s a -> Array s a -> b
ifoldl2Array f acc arr1 arr2 = case arr1 of
    MkArray s _ _ => let 0 prf = lteReflexive s in go s
  where
    go : (i : Nat) -> (0 prf : LTE i s) => b
    go 0 = acc
    go (S k) = let 0 p = lteSuccLeft prf in f (go k) k k (readArray arr1 k) (readArray arr2 k)

export
%inline
foldlArray : (b -> a -> b) -> b -> Array s a -> b
foldlArray f = ifoldlArray (\acc,_,x => f acc x)

export
%inline
||| I expect this will dissapear from the api once fusion exists
foldl2Array : (b -> a -> a -> b) -> b -> Array s a -> Array s a -> b
foldl2Array f = ifoldl2Array (\acc,_,_,x,y => f acc x y)

-- bleh, see ifoldlArray note above
-- exported via Foldable
%inline
foldrArray : (a -> b -> b) -> b -> Array s a -> b
foldrArray f = foldlArray (flip f)

export
%inline
mapArray : (a -> b) -> Array s a -> Array s b
mapArray f arr = imapArray (\_,x => f x) arr

export
zipWithArray : (a -> b -> c) -> Array s a -> Array s b -> Array s c
zipWithArray f arr1 arr2 = case arr1 of
    MkArray s _ _ =>
      let new = newUnintializedArray {a=c} s
          0 prf = lteReflexive s
      in  go new s
  where
    go : Array s c -> (i : Nat) -> (0 prf : LTE i s) => Array s c
    go new 0 = new
    go new (S k) =
      let 0 newprf = lteSuccLeft prf
          v1 = readArray arr1 k
          v2 = readArray arr2 k
          () = unsafePerformIO $ mutableWriteArray new k (f v1 v2)
      in  go new k

export
(++) : Array s1 a -> Array s2 a -> Array (s1 + s2) a
MkArray s1 is1 cnt1 ++ MkArray s2 is2 cnt2 with (newUnintializedArray {a} (s1 + s2))
  _ | new@(MkArray (s1 + s2) nis ncnt) = unsafePerformIO $ do
    copyFrom cnt1 ncnt (is1 - 1) 0
    copyFrom cnt2 ncnt (is2 - 1) is1
    pure new

export
Functor (Array s) where
  map = mapArray

-- do we really want this?
export
{s:_} -> Applicative (Array s) where
  pure a = newArray' a
  f <*> fa = zipWithArray (\f,x => f x) f fa

-- exported via Foldable
toList : Array s a -> List a
toList xs = foldlArray (\b,a => b . (a ::)) id xs []

-- TODO: toVect, to delistify while preserving size

export
fromList : (xs : List a) -> Array (length xs) a
fromList xs with (length xs)
  fromList xs | s =
      let new = newUnintializedArray {a} s
      in  go new xs 0
  where -- this used mutableWriteArray to prove
    go : Array s a -> (xs : List a) -> (i : Nat) -> Array s a
    go new (x :: xs) k =
      let () = unsafePerformIO $ unsafeMutableWriteArray new k x
      in  go new xs (S k)
    go new _ _ = new

export
fromList' : (xs : List a) -> (s : Nat ** Array s a)
fromList' xs =
    let s = length xs
        new = newUnintializedArray {a} s
    in  (s ** go new xs 0)
  where -- this used mutableWriteArray to prove
    go : Array s a -> (xs : List a) -> (i : Nat) -> Array s a
    go new (x :: xs) k =
      let () = unsafePerformIO $ unsafeMutableWriteArray new k x
      in  go new xs (S k)
    go new _ _ = new

-- TODO: fromVect, to listify while preserving size

export
Show a => Show (Array s a) where
  showPrec p x = showCon p "fromList" (showArg (Array.toList x))

export
sumArray : Num a => Array s a -> a
sumArray = foldlArray (+) 0

-- The quintessential example for where you'd want fusion, but we don't have it yet.
export
dotArray : Num a => Array s a -> Array s a -> a
dotArray a b = sumArray (zipWithArray (*) a b)

------------ Foldable ------------

export
Foldable (Array s) where
  foldr = foldrArray
  toList = Array.toList

------------ Traversable ------------

export
Traversable (Array s) where
  traverse f = imapArrayM (\_,x => f x)

------------ Semigroup / Monoid ------------

export
Semigroup a => Semigroup (Array s a) where
  a <+> b = zipWithArray (<+>) a b

export
{s:_} -> Monoid a => Monoid (Array s a) where
  neutral = newArray' neutral

------------ Cast ------------

export
Cast a b => Cast (Array s a) (Array s b) where
  cast = mapArray cast

------------ FromString ------------

||| :exec printLn $ the (s ** Array s Char) "abcde"
||| (5 ** fromList ['a', 'b', 'c', 'd', 'e'])
||| :exec printLn $ the (s ** Array s Bits8) "abcde"
||| (5 ** fromList [97, 98, 99, 100, 101])
||| :exec printLn $ snd $ the (s ** Array s Bits8) "abcde"
||| fromList [97, 98, 99, 100, 101]
export
Cast Char a => FromString (s ** Array s a) where
  fromString str = let (s ** arr) = fromList' (unpack str) in (s ** cast arr)

------------ Eq ------------

export
Eq a => Eq (Array s a) where
  x == y = foldl2Array (\b,x,y => x == y && b) True x y

------------ Ord ------------

export
Ord a => Ord (Array s a) where
  compare x y = foldl2Array (\b,x,y => compare x y <+> b) neutral x y

--------------------------------------------------
-- Forcing particular operations into these numerical interfaces makes
-- over-restrictive functions, e.g. fromInteger forces us to create a specific
-- array, requiring us to know what 's' is, but + and * don't need this
-- restriction since things like zipWith rediscovers what `s` was via pattern
-- matching. We thus provide the operations below without an accompanying
-- interface.
--------------------------------------------------
-- These interfaces are provided in Data.Strong.Array.Interfaces
--------------------------------------------------

------------ Num ------------

export
%inline
(+) : Num a => Array s a -> Array s a -> Array s a
x + y = zipWithArray (+) x y

export
%inline
(*) : Num a => Array s a -> Array s a -> Array s a
x * y = zipWithArray (*) x y

export
%inline
fromInteger : {s:_} -> Num a => Integer -> Array s a
fromInteger x = newArray' (fromInteger x)

------------ FromDouble ------------

export
%inline
fromDouble : {s : _} -> FromDouble a => Double -> Array s a
fromDouble x = newArray' (fromDouble x)

------------ Neg ------------

export
%inline
negate : Neg a => Array s a -> Array s a
negate = mapArray negate

export
%inline
(-) : Neg a => Array s a -> Array s a -> Array s a
x - y = zipWithArray (-) x y

------------ Abs ------------

export
%inline
abs : Abs a => Array s a -> Array s a
abs = mapArray abs

------------ Fractional ------------

export
%inline
(/) : Fractional a => Array s a -> Array s a -> Array s a
x / y = zipWithArray (/) x y
-- recip : Fractional a => Array s a -> Array s a

------------ Integral ------------

export
%inline
div : Integral a => Array s a -> Array s a -> Array s a
div x y = zipWithArray div x y

export
%inline
mod : Integral a => Array s a -> Array s a -> Array s a
mod x y = zipWithArray mod x y

------------ Floating ------------

export
%inline
exp : Floating a => Array s a -> Array s a
exp x = mapArray exp x

export
%inline
pi : {s:_} -> Floating a => Array s a
pi = newArray' pi

export
%inline
euler : {s:_} -> Floating a => Array s a
euler = newArray' euler

export
%inline
log : Floating a => Array s a -> Array s a
log x = mapArray log x

export
%inline
pow : Floating a => Array s a -> Array s a -> Array s a
pow x y = zipWithArray pow x y

export
%inline
sin : Floating a => Array s a -> Array s a
sin x = mapArray sin x

export
%inline
cos : Floating a => Array s a -> Array s a
cos x = mapArray cos x

export
%inline
tan : Floating a => Array s a -> Array s a
tan x = mapArray tan x

export
%inline
asin : Floating a => Array s a -> Array s a
asin x = mapArray asin x

export
%inline
acos : Floating a => Array s a -> Array s a
acos x = mapArray acos x

export
%inline
atan : Floating a => Array s a -> Array s a
atan x = mapArray atan x

export
%inline
sinh : Floating a => Array s a -> Array s a
sinh x = mapArray sinh x

export
%inline
cosh : Floating a => Array s a -> Array s a
cosh x = mapArray cosh x

export
%inline
tanh : Floating a => Array s a -> Array s a
tanh x = mapArray tanh x

export
%inline
sqrt : Floating a => Array s a -> Array s a
sqrt x = mapArray sqrt x

export
%inline
floor : Array s Double -> Array s Double
floor x = mapArray floor x

export
%inline
ceiling : Array s Double -> Array s Double
ceiling x = mapArray ceiling x

------------ Zippable ------------

export
%inline
zipWith : (a -> b -> c) -> Array s a -> Array s b -> Array s c
zipWith = zipWithArray

export
%inline
||| pretty wasteful array copying here, probably best to avod until we have fusion
zipWith3 : (a -> b -> c -> d) -> Array s a -> Array s b -> Array s c -> Array s d
zipWith3 f x y z = zipWithArray (\f',x' => f' x') (zipWithArray f x y) z

export
unzipWith : (f : a -> (b, c)) -> Array s a -> (Array s b, Array s c)
unzipWith f arr = case arr of
    MkArray s _ _ =>
      let new1 = newUnintializedArray s
          new2 = newUnintializedArray s
          () = ifoldlArray (\_,i,x' => unsafePerformIO $ do
                 let (x,y) = f x'
                 unsafeMutableWriteArray new1 i x
                 unsafeMutableWriteArray new2 i y) () arr
          in (new1,new2)

export
unzipWith3 : (func : a -> (b, c, d)) -> Array s a -> (Array s b, Array s c, Array s d)
unzipWith3 f arr = case arr of
    MkArray s _ _ =>
      let new1 = newUnintializedArray s
          new2 = newUnintializedArray s
          new3 = newUnintializedArray s
          () = ifoldlArray (\_,i,x' => unsafePerformIO $ do
                 let (x,y,z) = f x'
                 unsafeMutableWriteArray new1 i x
                 unsafeMutableWriteArray new2 i y
                 unsafeMutableWriteArray new3 i z) () arr
          in (new1,new2,new3)

export
Zippable (Array s) where
  zipWith = Array.zipWith
  zipWith3 = Array.zipWith3
  unzipWith = Array.unzipWith
  unzipWith3 = Array.unzipWith3

ext: idr

max_stars_repo_name: MarcelineVQ/sarray


text:
module C

import A

A.defA = ?newHole


text:
module Derive.TestDefs

data W : (a : Type) -> (a -> Type) -> Type where
  Sup : (x : a) -> (p x -> W a p) -> W a p

max_stars_repo_name: Garnasha/derive-all-the-instances

max_issues_repo_name: Garnasha/derive-all-the-instances

max_forks_repo_name: Garnasha/derive-all-the-instances


text:
record T where
  constructor mkT


text:
module Main

import Idris.Driver

import Pretty
import StringMap
import SortedSet

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Inline
import Compiler.Scheme.Common

import Core.Hash
import Core.Context
import Core.Directory
import Core.Name
import Core.Name.Namespace
import Core.Options
import Core.TT
import Libraries.Utils.Hex
import Libraries.Utils.Path

import Data.List
import Data.List1
import Data.Maybe
import Data.String
import Data.Vect
import Libraries.Data.NameMap

import System
import System.Directory
import System.File
import System.Info

%default covering

-- this will break if the same scheme foreign function is used to implement
-- an operation on, say, different numeric types, as pointed out by @karroffel
--
-- let's go with this for now, though
--
emulatedForeigns : StringMap String
emulatedForeigns = StringMap.fromList
  -- general
  [ ("scheme:string-concat", "Rts.Bytes.concat")
  , ("scheme:blodwen-args",  "Rts.System.get_args")
  , ("scheme:string-pack",   "Rts.String.pack")
  , ("scheme:string-unpack", "Rts.String.unpack")
  , ("scheme:blodwen-string-iterator-new",  "Rts.String.Iterator.new_")
  , ("scheme:blodwen-string-iterator-next", "Rts.String.Iterator.next")

  -- clock
  , ("scheme:blodwen-clock-time-gccpu", "Rts.System.clocktime_gc_cpu")
  , ("scheme:blodwen-clock-time-gcreal", "Rts.System.clocktime_gc_real")
  , ("scheme:blodwen-clock-time-monotonic", "Rts.System.clocktime_monotonic")
  , ("scheme:blodwen-clock-time-process", "Rts.System.clocktime_process")
  , ("scheme:blodwen-clock-time-thread", "Rts.System.clocktime_thread")
  , ("scheme:blodwen-clock-time-utc", "Rts.System.clocktime_utc")
  , ("scheme:blodwen-clock-second", "Rts.System.os_clock_second")
  , ("scheme:blodwen-clock-nanosecond", "Rts.System.os_clock_nanosecond")
  , ("scheme:blodwen-is-time?", "Rts.System.os_clock_valid")

  -- chez refuses to use foreign C functions for buffers
  -- probably as a reminder that the backend-specific versions will be faster
  , ("scheme:blodwen-new-buffer", "Rts.C.Lib_libidris2_support.idris2_newBuffer")
  , ("scheme:blodwen-buffer-size", "Rts.C.Lib_libidris2_support.idris2_getBufferSize")
  , ("scheme:blodwen-buffer-copydata", "Rts.C.Lib_libidris2_support.idris2_copyBuffer")
  , ("scheme:blodwen-buffer-getbyte", "Rts.C.Lib_libidris2_support.idris2_getBufferByte")
  , ("scheme:blodwen-buffer-getint", "Rts.C.Lib_libidris2_support.idris2_getBufferInt")
  , ("scheme:blodwen-buffer-getdouble", "Rts.C.Lib_libidris2_support.idris2_getBufferDouble")
  , ("scheme:blodwen-buffer-getstring", "Rts.C.Lib_libidris2_support.idris2_getBufferString")
  , ("scheme:blodwen-buffer-setbyte", "Rts.C.Lib_libidris2_support.idris2_setBufferByte")
  , ("scheme:blodwen-buffer-setint", "Rts.C.Lib_libidris2_support.idris2_setBufferInt")
  , ("scheme:blodwen-buffer-setdouble", "Rts.C.Lib_libidris2_support.idris2_setBufferDouble")
  , ("scheme:blodwen-buffer-setstring", "Rts.C.Lib_libidris2_support.idris2_setBufferString")
  ]

heXX : Int -> String
heXX x = hd (x `div` 16) ++ hd (x `mod` 16)
  where
    hd : Int -> String
    hd 10 = "A"
    hd 11 = "B"
    hd 12 = "C"
    hd 13 = "D"
    hd 14 = "E"
    hd 15 = "F"
    hd i = show i

showChar : Char -> String -> String
showChar '\\' = ("\\\\" ++)
showChar '"' = ("\\\"" ++)
showChar '\n' = ("\\n" ++)
showChar c
   = if c < chr 32
        then (("\\x" ++ heXX (cast c) ++ "") ++)
        else strCons c

showString : List Char -> String -> String
showString [] = id
showString (c::cs) = showChar c . showString cs

mlfString : String -> Doc
mlfString cs = text $ strCons '"' (showString (unpack cs) "\"")

sexp : List Doc -> Doc
sexp = parens . hsep

mlfGlobal : String -> Doc
mlfGlobal mlName = parens $
  text "global"
    <++> hsep
      [ text ("$" ++ n)
      | n <- toList $ split (== '.') mlName
      ]

mlfApply : Doc -> List Doc -> Doc
mlfApply f [] = f
mlfApply f args = parens $
  text "apply" <++> f
  $$ indentBlock args

mlfLibCall : String -> List Doc -> Doc
mlfLibCall fn args = mlfApply (mlfGlobal fn) args

mlfError : String -> Doc
mlfError msg = mlfLibCall "Stdlib.failwith" [mlfString msg]

mlfDebug : Show a => a -> Doc
mlfDebug = mlfError . show

sanitise : String -> String
sanitise = pack . concatMap sanitise' . unpack
  where
    san : Char -> Bool
    san c =
        ('A' <= c && c <= 'Z')
        || ('a' <= c && c <= 'z')
        || ('0' <= c && c <= '9')

    sanitise' : Char -> List Char
    sanitise' c =
      if san c
        then [c]
        else '_' :: unpack (show $ ord c) ++ ['_']

mlfName : Name -> Doc
mlfName (MN n i) = text (sanitise n) <+> show i
mlfName n = text . sanitise . schName $ n

-- ML identifiers can't start with capital letters
mlfGlobalName : Name -> Doc
mlfGlobalName n = text "idr_" <+> mlfName n

mlfLocalVar : Name -> Doc
mlfLocalVar n = text "$" <+> mlfName n

mlfGlobalVar : Name -> Doc
mlfGlobalVar n = text "$" <+> mlfGlobalName n

-- returns MLF module name
mlfNS : Name -> String
mlfNS (NS ns n) = "Mod_" ++ concat (intersperse "_" $ reverse $ unsafeUnfoldNamespace ns)
mlfNS n = "Misc"

record ModuleName where
  constructor MkMN
  string : String

Eq ModuleName where
  MkMN x == MkMN y = x == y

mlfGlobalNS : StringMap ModuleName -> ModuleName -> Name -> Doc
mlfGlobalNS nsMap curModuleName n =
  let mns = mlfNS n
    in case StringMap.lookup mns nsMap of
      Nothing => mlfError $ "mlfGlobalNS: impossible: could not find " ++ show mns
      Just targetModName =>
        if targetModName == curModuleName
          then mlfGlobalVar n  -- within-module reference
          else sexp [text "global", text ("$" ++ targetModName.string), mlfGlobalVar n]

mlfLet : Name -> Doc -> Doc -> Doc
mlfLet n val rhs = parens $
  text "let"
  $$ indentBlock
    [ sexp [mlfLocalVar n, val]
    , rhs
    ]

mlfLazy : Doc -> Doc
mlfLazy doc = sexp [text "lazy", doc]

mlfLam : List Name -> Doc -> Doc
mlfLam [] rhs = mlfLazy rhs
mlfLam args rhs =
  parens $
    text "lambda" <++> sexp (map mlfLocalVar args)
    $$ indent rhs

mlfForce : Doc -> Doc
mlfForce doc = sexp [text "force", doc]

mlfBlock : Maybe Int -> List Doc -> Doc
mlfBlock Nothing args = mlfError "no constructor tag (1)"
mlfBlock (Just tag) args = parens $
  text "block" <++> sexp [text "tag", show tag]
  $$ indentBlock args

mlfCmp : String -> String -> String -> List Doc -> Doc
mlfCmp conv cmp zero args = sexp [text cmp, mlfLibCall conv args, text zero]

mlfOp : PrimFn arr -> Vect arr Doc -> Doc
mlfOp (Add IntType) [x,y] = sexp [text "+.int", x,y]
mlfOp (Sub IntType) [x,y] = sexp [text "-.int", x,y]
mlfOp (Mul IntType) [x,y] = sexp [text "*.int", x,y]
mlfOp (Div IntType) [x,y] = sexp [text "/.int", x,y]
mlfOp (Mod IntType) [x,y] = sexp [text "%.int", x,y]
mlfOp (Neg IntType) [x]   = sexp [text "neg.int", x]
mlfOp (ShiftL IntType) [x,y] = sexp [text "<<.int", x, y]
mlfOp (ShiftR IntType) [x,y] = sexp [text ">>.int", x, y]
mlfOp (BAnd IntType)   [x,y] = sexp [text "&.int", x, y]
mlfOp (BOr IntType)    [x,y] = sexp [text "|.int", x, y]
mlfOp (BXOr IntType)   [x,y] = sexp [text "^.int", x, y]

mlfOp (LT IntType) [x,y] = sexp [text "<.int", x,y]
mlfOp (LTE IntType) [x,y] = sexp [text "<=.int", x,y]
mlfOp (EQ IntType) [x,y] = sexp [text "==.int", x,y]
mlfOp (GTE IntType) [x,y] = sexp [text ">=.int", x,y]
mlfOp (GT IntType) [x,y] = sexp [text ">.int", x,y]

mlfOp (LT CharType) [x,y] = sexp [text "<.int", x,y]
mlfOp (LTE CharType) [x,y] = sexp [text "<=.int", x,y]
mlfOp (EQ CharType) [x,y] = sexp [text "==.int", x,y]
mlfOp (GTE CharType) [x,y] = sexp [text ">=.int", x,y]
mlfOp (GT CharType) [x,y] = sexp [text ">.int", x,y]

mlfOp (Add IntegerType) [x,y] = sexp [text "+.ibig", x,y]
mlfOp (Sub IntegerType) [x,y] = sexp [text "-.ibig", x,y]
mlfOp (Mul IntegerType) [x,y] = sexp [text "*.ibig", x,y]
mlfOp (Div IntegerType) [x,y] = sexp [text "/.ibig", x,y]
mlfOp (Mod IntegerType) [x,y] = sexp [text "%.ibig", x,y]
mlfOp (Neg IntegerType) [x]   = sexp [text "neg.ibig", x]
mlfOp (ShiftL IntegerType) [x,y] = sexp [text "<<.ibig", x, y]
mlfOp (ShiftR IntegerType) [x,y] = sexp [text ">>.ibig", x, y]
mlfOp (BAnd IntegerType)   [x,y] = sexp [text "&.ibig", x, y]
mlfOp (BOr IntegerType)    [x,y] = sexp [text "|.ibig", x, y]
mlfOp (BXOr IntegerType)   [x,y] = sexp [text "^.ibig", x, y]

mlfOp (LT IntegerType) [x,y] = sexp [text "<.ibig", x,y]
mlfOp (LTE IntegerType) [x,y] = sexp [text "<=.ibig", x,y]
mlfOp (EQ IntegerType) [x,y] = sexp [text "==.ibig", x,y]
mlfOp (GTE IntegerType) [x,y] = sexp [text ">=.ibig", x,y]
mlfOp (GT IntegerType) [x,y] = sexp [text ">.ibig", x,y]

mlfOp (Add DoubleType) [x,y] = sexp [text "+.f64", x,y]
mlfOp (Sub DoubleType) [x,y] = sexp [text "-.f64", x,y]
mlfOp (Mul DoubleType) [x,y] = sexp [text "*.f64", x,y]
mlfOp (Div DoubleType) [x,y] = sexp [text "/.f64", x,y]
mlfOp (Mod DoubleType) [x,y] = sexp [text "%.f64", x,y]
mlfOp (Neg DoubleType) [x]   = sexp [text "neg.f64", x]

mlfOp (LT DoubleType) [x,y] = sexp [text "<.f64", x,y]
mlfOp (LTE DoubleType) [x,y] = sexp [text "<=.f64", x,y]
mlfOp (EQ DoubleType) [x,y] = sexp [text "==.f64", x,y]
mlfOp (GTE DoubleType) [x,y] = sexp [text ">=.f64", x,y]
mlfOp (GT DoubleType) [x,y] = sexp [text ">.f64", x,y]

mlfOp DoubleExp [x] = mlfLibCall "Float.exp" [x]
mlfOp DoubleLog [x] = mlfLibCall "Float.log" [x]  -- should this be Float.log10?
mlfOp DoubleSin [x] = mlfLibCall "Float.sin" [x]
mlfOp DoubleCos [x] = mlfLibCall "Float.cos" [x]
mlfOp DoubleTan [x] = mlfLibCall "Float.tan" [x]
mlfOp DoubleASin [x] = mlfLibCall "Float.asin" [x]
mlfOp DoubleACos [x] = mlfLibCall "Float.acos" [x]
mlfOp DoubleATan [x] = mlfLibCall "Float.atan" [x]
mlfOp DoubleSqrt [x] = mlfLibCall "Float.sqrt" [x]
mlfOp DoubleFloor [x] = mlfLibCall "Float.floor" [x]
mlfOp DoubleCeiling [x] = mlfLibCall "Float.ceil" [x]

mlfOp (Cast IntegerType DoubleType) [x] = sexp [text "convert.ibig.f64", x]
mlfOp (Cast DoubleType IntegerType) [x] = sexp [text "convert.f64.ibig", x]
mlfOp (Cast IntType DoubleType) [x] = sexp [text "convert.int.f64", x]
mlfOp (Cast DoubleType IntType) [x] = sexp [text "convert.f64.int", x]
mlfOp (Cast IntegerType IntType) [x] = sexp [text "convert.ibig.int", x]
mlfOp (Cast IntType IntegerType) [x] = sexp [text "convert.int.ibig", x]
mlfOp (Cast IntegerType CharType) [x] = sexp [text "convert.ibig.int", x]
mlfOp (Cast CharType IntegerType) [x] = sexp [text "convert.int.ibig", x]
mlfOp (Cast CharType IntType) [x] = x
mlfOp (Cast IntType CharType) [x] = x
mlfOp (Cast IntegerType StringType) [x] = mlfLibCall "Z.to_string" [x]
mlfOp (Cast IntType StringType) [x] = mlfLibCall "Stdlib.string_of_int" [x]
mlfOp (Cast StringType IntegerType) [x] = mlfLibCall "Z.of_string" [x]
mlfOp (Cast StringType IntType) [x] = mlfLibCall "Stdlib.int_of_string" [x]
mlfOp (Cast CharType StringType) [x] = mlfLibCall "Rts.String.of_char" [x]
mlfOp (Cast StringType CharType) [x] = mlfLibCall "Rts.String.head" [x]
mlfOp (Cast StringType DoubleType) [x] = mlfLibCall "Float.of_string" [x]
mlfOp (Cast DoubleType StringType) [x] = mlfLibCall "Float.to_string" [x]

mlfOp (Cast Int8Type IntType) [x] = x
mlfOp (Cast IntType Int8Type) [x] = x
mlfOp (Cast Int8Type IntegerType) [x] = sexp [text "convert.int.ibig", x]
mlfOp (Cast IntegerType Int8Type) [x] = sexp [text "convert.ibig.int", x]
mlfOp (Cast Int8Type StringType) [x] = mlfLibCall "Stdlib.string_of_int" [x]
mlfOp (Cast StringType Int8Type) [x] = mlfLibCall "Stdlib.int_of_string" [x]

mlfOp (Cast Int16Type IntType) [x] = x
mlfOp (Cast IntType Int16Type) [x] = x
mlfOp (Cast Int16Type IntegerType) [x] = sexp [text "convert.int.ibig", x]
mlfOp (Cast IntegerType Int16Type) [x] = sexp [text "convert.ibig.int", x]
mlfOp (Cast Int16Type StringType) [x] = mlfLibCall "Stdlib.string_of_int" [x]
mlfOp (Cast StringType Int16Type) [x] = mlfLibCall "Stdlib.int_of_string" [x]

mlfOp (Cast Int32Type IntType) [x] = sexp [text "convert.i32.int", x]
mlfOp (Cast IntType Int32Type) [x] = sexp [text "convert.int.i32", x]
mlfOp (Cast Int32Type IntegerType) [x] = sexp [text "convert.i32.ibig", x]
mlfOp (Cast IntegerType Int32Type) [x] = sexp [text "convert.ibig.i32", x]
mlfOp (Cast Int32Type StringType) [x] = mlfLibCall "Int32.to_string" [x]
mlfOp (Cast StringType Int32Type) [x] = mlfLibCall "Int32.of_string" [x]

mlfOp (Cast Int64Type IntType) [x] = sexp [text "convert.i64.int", x]
mlfOp (Cast IntType Int64Type) [x] = sexp [text "convert.int.i64", x]
mlfOp (Cast Int64Type IntegerType) [x] = sexp [text "convert.i64.ibig", x]
mlfOp (Cast IntegerType Int64Type) [x] = sexp [text "convert.ibig.i64", x]
mlfOp (Cast Int64Type StringType) [x] = mlfLibCall "Int64.to_string" [x]
mlfOp (Cast StringType Int64Type) [x] = mlfLibCall "Int64.of_string" [x]

mlfOp (Cast Bits8Type IntType) [x] = x
mlfOp (Cast IntType Bits8Type) [x] = x
mlfOp (Cast Bits8Type IntegerType) [x] = sexp [text "convert.int.ibig", x]
mlfOp (Cast IntegerType Bits8Type) [x] = sexp [text "convert.ibig.int", x]
mlfOp (Cast Bits8Type StringType) [x] = mlfLibCall "Stdlib.string_of_int" [x]
mlfOp (Cast StringType Bits8Type) [x] = mlfLibCall "Stdlib.int_of_string" [x]

mlfOp (Cast Bits16Type IntType) [x] = x
mlfOp (Cast IntType Bits16Type) [x] = x
mlfOp (Cast Bits16Type IntegerType) [x] = sexp [text "convert.int.ibig", x]
mlfOp (Cast IntegerType Bits16Type) [x] = sexp [text "convert.ibig.int", x]
mlfOp (Cast Bits16Type StringType) [x] = mlfLibCall "Stdlib.string_of_int" [x]
mlfOp (Cast StringType Bits16Type) [x] = mlfLibCall "Stdlib.int_of_string" [x]

-- mlfOp (Cast Bits32Type IntType) [x] = mlfLibCall "Int32.unsigned_to_int" [x]
mlfOp (Cast IntType Bits32Type) [x] = mlfLibCall "Int32.of_int" [x]
-- mlfOp (Cast Bits32Type IntegerType) [x] = sexp [text "convert.i32.ibig", x]
mlfOp (Cast IntegerType Bits32Type) [x] = sexp [text "convert.ibig.i32", x]
mlfOp (Cast Bits32Type IntegerType) [x] = sexp
  [ text "%.ibig"
  , sexp
    [ text "+.ibig"
    , sexp [text "convert.i32.ibig", x]
    , text "4294967296.ibig"
    ]
  , text "4294967296.ibig"
  ]
-- mlfOp (Cast Bits32Type StringType) [x] = mlfLibCall "Stdlib.string_of_int" [x]
-- mlfOp (Cast StringType Bits32Type) [x] = mlfLibCall "Stdlib.int_of_string" [x]

mlfOp (Cast IntType Bits64Type) [x] = mlfLibCall "Int64.of_int" [x]
mlfOp (Cast IntegerType Bits64Type) [x] = sexp [text "convert.ibig.i64", x]
mlfOp (Cast Bits64Type IntegerType) [x] = sexp
  [ text "%.ibig"
  , sexp
    [ text "+.ibig"
    , sexp [text "convert.i64.ibig", x]
    , text "18446744073709551616.ibig"
    ]
  , text "18446744073709551616.ibig"
  ]

mlfOp StrLength [x] = mlfLibCall "Rts.String.length" [x]
mlfOp StrHead [x] = mlfLibCall "Rts.String.head" [x]
mlfOp StrTail [x] = mlfLibCall "Rts.String.tail" [x]
mlfOp StrIndex [x, i] = mlfLibCall "Rts.String.get" [x, i]
mlfOp StrCons [x, xs] = mlfLibCall "Rts.String.cons" [x, xs]
mlfOp StrReverse [x] = mlfLibCall "Rts.String.reverse" [x]
mlfOp StrSubstr [off, len, s] = mlfLibCall "Rts.String.substring" [off, len, s]
mlfOp StrAppend [x,y] = mlfLibCall "Bytes.cat" [x, y]

mlfOp (LT StringType) [x,y] = mlfCmp "String.compare" "<.int" "0" [x,y]
mlfOp (LTE StringType) [x,y] = mlfCmp "String.compare" "<=.int" "0" [x,y]
mlfOp (EQ StringType) [x,y] = mlfCmp "String.compare" "==.int" "0" [x,y]
mlfOp (GTE StringType) [x,y] = mlfCmp "String.compare" ">=.int" "0" [x,y]
mlfOp (GT StringType) [x,y] = mlfCmp "String.compare" ">.int" "0" [x,y]

mlfOp Crash [_, msg] = mlfLibCall "Stdlib.failwith" [msg]
mlfOp BelieveMe [_, _, x] = x

mlfOp op args = mlfError $ "unimplemented primop: " ++ show op

private
un : String -> Name
un = UN . Basic

mlfExtPrim : Name -> Doc
mlfExtPrim (NS _ (UN (Basic "prim__newArray"))) =
  mlfLam [un "_ty", un "n", un "x", un "_world"] $
    sexp [text "makevec", mlfLocalVar (un "n"), mlfLocalVar (un "x")]
mlfExtPrim (NS _ (UN (Basic "prim__arrayGet"))) =
  mlfLam [un "_ty", un "arr", un "i", un "_world"] $
    sexp [text "load", mlfLocalVar (un "arr"), mlfLocalVar (un "i")]
mlfExtPrim (NS _ (UN (Basic "prim__arraySet"))) =
  mlfLam [un "_ty", un "arr", un "i", un "x", un "_world"] $
    sexp [text "store", mlfLocalVar (un "arr"), mlfLocalVar (un "i"), mlfLocalVar (un "x")]
mlfExtPrim (NS _ (UN (Basic "prim__newIORef"))) =
  mlfLam [un "_ty", un "x", un "_world"] $
    sexp [text "makevec", show 1, mlfLocalVar (un "x")]
mlfExtPrim (NS _ (UN (Basic "prim__readIORef"))) =
  mlfLam [un "_ty", un "ref", un "_world"] $
    sexp [text "load", mlfLocalVar (un "ref"), show 0]
mlfExtPrim (NS _ (UN (Basic "prim__writeIORef"))) =
  mlfLam [un "_ty", un "ref", un "x", un "_world"] $
    sexp [text "store", mlfLocalVar (un "ref"), show 0, mlfLocalVar (un "x")]
mlfExtPrim (NS _ (UN (Basic "prim__schemeCall"))) =
  mlfLam [un "_rTy", un "fn", un "_args", un "_world"] $
    mlfLibCall "Stdlib.failwith" [mlfLocalVar (un "fn")]
mlfExtPrim (NS _ (UN (Basic "prim__codegen"))) = mlfString "malfunction"
mlfExtPrim (NS _ (UN (Basic "prim__os"))) = mlfGlobal "Rts.System.os_name"
mlfExtPrim n = mlfError $ "unimplemented external primitive: " ++ show n

mlfConstant : Constant -> Doc
mlfConstant (I x) = show x
mlfConstant (BI x) = show x <+> text ".ibig"
mlfConstant (Str s) = mlfString s
mlfConstant (Ch x) = show (ord x)
mlfConstant (Db x) =
  case filter (== '.') (unpack $ Prelude.show x) of
    [] => Pretty.show x <+> text ".0"
    _  => Pretty.show x

mlfConstant (I8 x) = show x
mlfConstant (I16 x) = show x
mlfConstant (I32 x) = show x <+> text ".i32"
mlfConstant (I64 x) = show x <+> text ".i64"

mlfConstant (B8 x) = show x
mlfConstant (B16 x) = show x
mlfConstant (B32 x) = show x <+> text ".i32"
mlfConstant (B64 x) = show x <+> text ".i64"

mlfConstant WorldVal = show 0

mlfConstant IntType = show 0
mlfConstant IntegerType = show 1
mlfConstant StringType = show 2
mlfConstant CharType = show 3
mlfConstant DoubleType = show 4
mlfConstant WorldType = show 5
mlfConstant Bits8Type = show 6
mlfConstant Bits16Type = show 7
mlfConstant Bits32Type = show 8
mlfConstant Bits64Type = show 9
mlfConstant Int8Type = show 10
mlfConstant Int16Type = show 11
mlfConstant Int32Type = show 12
mlfConstant Int64Type = show 13

mlfConstPat : Constant -> Maybe Doc
-- malfunction cannot switch on these
mlfConstPat (BI x) = Nothing
mlfConstPat (Str s) = Nothing
mlfConstPat (Db x) = Nothing
mlfConstPat (I32 _) = Nothing
mlfConstPat (I64 _) = Nothing
mlfConstPat (B32 _) = Nothing
mlfConstPat (B64 _) = Nothing
mlfConstPat c = Just $ mlfConstant c

mlfConstEqCheck : Doc -> Constant -> Doc
-- these have special comparison ops
mlfConstEqCheck x (BI y) = sexp [text "==.ibig", x, mlfConstant (BI y)]
mlfConstEqCheck x (I32 y) = sexp [text "==.i32", x, mlfConstant (I32 y)]
mlfConstEqCheck x (I64 y) = sexp [text "==.i64", x, mlfConstant (I64 y)]
mlfConstEqCheck x (B32 y) = sexp [text "==.i32", x, mlfConstant (B32 y)]
mlfConstEqCheck x (B64 y) = sexp [text "==.i64", x, mlfConstant (B64 y)]
mlfConstEqCheck x (Db y) = sexp [text "==.f64", x, mlfConstant (Db y)]
mlfConstEqCheck x (Str y) = mlfLibCall "String.equal" [x, mlfConstant (Str y)]

-- everything else is represented as ints
mlfConstEqCheck x y = sexp [text "==.int", x, mlfConstant y]

mlfConDflt : Doc -> Doc
mlfConDflt rhs = sexp [sexp [text "tag", text "_"], text "_", rhs]

mlfSwitch : Doc -> List Doc -> Maybe Doc -> Doc
mlfSwitch scrut [] Nothing =
  mlfError $ "case with no RHS"
mlfSwitch scrut [] (Just dflt) = dflt
mlfSwitch scrut alts (Just dflt) = parens $
  text "switch" <++> scrut
  $$ indent (vcat alts $$ dflt)

mlfSwitch scrut alts Nothing = parens $
  text "switch" <++> scrut
  $$ indent (if debug then (vcat alts $$ catchall) else vcat alts)
 where
  debug : Bool
  debug = True

  catchall : Doc
  catchall =
    mlfConDflt $
      mlfLet (un "_") (mlfLibCall "Rts.Debug.inspect" [show 0, scrut])$
        mlfError "unmatched pattern! (block tree dump above)"

mlfConstDflt : Doc -> Doc
mlfConstDflt rhs = sexp [text "_", rhs]

mlfField : Name -> Int -> Doc
mlfField n i = sexp [text "field", show i, mlfLocalVar n]

number : Int -> List a -> List (Int, a)
number i [] = []
number i (x :: xs) = (i,x) :: number (i+1) xs

bindFieldProjs : Name -> List Name -> Doc -> Doc
bindFieldProjs scrutN [] rhs = rhs
bindFieldProjs scrutN ns rhs = parens $
  text "let"
  $$ indent (
    vcat [sexp [mlfLocalVar n, mlfField scrutN i] | (i, n) <- number 0 ns]
    $$ rhs
  )

ccLibFun : List String -> Maybe String
ccLibFun [] = Nothing
ccLibFun (cc :: ccs) =
  case StringMap.lookup cc emulatedForeigns of
    Just result => Just result
    Nothing =>
      if substr 0 3 cc == "ML:"
        then Just (substr 3 (length cc) cc)
        else if substr 0 2 cc == "C:"
            then case split (== ',') (substr 2 (length cc) cc) of
              fn ::: libn :: _ => Just ("Rts.C.Lib_" ++ rmSpaces libn ++ "." ++ fn)
              _ => ccLibFun ccs  -- something strange -> skip
            else ccLibFun ccs  -- search further
  where
    rmSpaces : String -> String
    rmSpaces = pack . filter (/= ' ') . unpack

{-
unApp : NamedCExp -> List NamedCExp -> (NamedCExp, List NamedCExp)
unApp (NmApp fc f args) args' = unApp f (args ++ args')
unApp f args = (f, args)
-}

-- namespaces mentioned within
mutual
  nsTm : NamedCExp -> SortedSet String
  nsTm (NmLocal fc n) = SortedSet.empty
  nsTm (NmRef fc n) = SortedSet.singleton $ mlfNS n
  nsTm (NmLam fc n rhs) = nsTm rhs
  nsTm (NmLet fc n val rhs) = nsTm val <+> nsTm rhs
  nsTm (NmApp fc f args) = nsTm f <+> concatMap nsTm args
  nsTm (NmCon fc cn ci tag args) = concatMap nsTm args
  nsTm (NmForce fc lr rhs) = nsTm rhs
  nsTm (NmDelay fc lr rhs) = nsTm rhs
  nsTm (NmErased fc) = SortedSet.empty
  nsTm (NmPrimVal ft x) = SortedSet.empty
  nsTm (NmOp fc op args) = concatMap nsTm args
  nsTm (NmExtPrim fc n args) = concatMap nsTm args
  nsTm (NmConCase fc scrut alts mbDflt) =
    nsTm scrut <+> concatMap nsConAlt alts <+> concatMap nsTm mbDflt
  nsTm (NmConstCase fc scrut alts mbDflt) =
    nsTm scrut <+> concatMap nsConstAlt alts <+> concatMap nsTm mbDflt
  nsTm (NmCrash fc msg) = SortedSet.empty

  nsConAlt : NamedConAlt -> SortedSet String
  nsConAlt (MkNConAlt n ci tag args rhs) = nsTm rhs

  nsConstAlt : NamedConstAlt -> SortedSet String
  nsConstAlt (MkNConstAlt c rhs) = nsTm rhs

nsDef : NamedDef -> SortedSet String
nsDef (MkNmFun argNs rhs) = nsTm rhs
nsDef (MkNmCon tag arity nt) = SortedSet.empty
nsDef (MkNmForeign ccs fargs rty) = SortedSet.empty
nsDef (MkNmError rhs) = nsTm rhs

parameters (ldefs : SortedSet Name, nsMapping : StringMap ModuleName, curModuleName : ModuleName)
  mutual
    bindScrut : NamedCExp -> (Name -> Doc) -> Doc
    bindScrut (NmLocal _ n) rhs = rhs n
    bindScrut scrut rhs =
      let scrutN = MN "scrut" 0
        in mlfLet scrutN (mlfTm scrut) (rhs scrutN)

    mlfEqChain : Name -> Maybe Doc -> List NamedConstAlt -> Doc
    mlfEqChain scrutN Nothing [] = mlfError "impossible eq chain"
    mlfEqChain scrutN (Just dflt) [] = dflt
    mlfEqChain scrutN mbDflt (MkNConstAlt c rhs :: alts) = parens $
      text "if" <++> mlfConstEqCheck (mlfLocalVar scrutN) c
      $$ indent (
        mlfTm rhs
        $$ mlfEqChain scrutN mbDflt alts
      )

    mlfConAlt : Name -> NamedConAlt -> Doc
    mlfConAlt scrutN (MkNConAlt cn ci Nothing args rhs) =
      mlfError $ "no tag for mlfConAlt: " ++ show cn
    mlfConAlt scrutN (MkNConAlt cn ci (Just tag) [] rhs) =
      -- nullary constructors compile to ints in ocaml
      sexp [show tag, mlfTm rhs]
    mlfConAlt scrutN (MkNConAlt cn ci (Just tag) args rhs) = parens $
      sexp [text "tag", show tag]
      $$ indent (bindFieldProjs scrutN args $ mlfTm rhs)

    mlfConstAlt : NamedConstAlt -> Maybe Doc
    mlfConstAlt (MkNConstAlt c rhs) =
      case mlfConstPat c of
        Just pat => Just $ parens (pat <++> mlfTm rhs)
        Nothing => Nothing

    mlfTm : NamedCExp -> Doc
    mlfTm (NmLocal fc n) = mlfLocalVar n
    mlfTm (NmRef fc n) =
        if contains n ldefs
          then mlfForce (mlfGlobalNS nsMapping curModuleName n)
          else mlfGlobalNS nsMapping curModuleName n
    mlfTm (NmLam fc n rhs) = mlfLam [n] (mlfTm rhs)
    mlfTm (NmLet fc n val rhs) = mlfLet n (mlfTm val) (mlfTm rhs)
    mlfTm (NmApp fc f args) =
      mlfApply (mlfTm f) (map mlfTm args)
      {- probably unnecessary
      let (f', args') = unApp f args
        in mlfApply (mlfTm f') (map mlfTm args')
      -}
    mlfTm (NmCon fc cn ci Nothing []) = mlfString (show cn)  -- type constructor
    mlfTm (NmCon fc cn ci (Just tag) []) = show tag
    mlfTm (NmCon fc cn ci mbTag args) = mlfBlock mbTag (map mlfTm args)
    mlfTm (NmCrash fc msg) = mlfError msg
    mlfTm (NmForce fc lr rhs) = mlfForce (mlfTm rhs)
    mlfTm (NmDelay fc lr rhs) = mlfLazy (mlfTm rhs)
    mlfTm (NmErased fc) = mlfString "erased"
    mlfTm (NmPrimVal ft x) = mlfConstant x
    mlfTm (NmOp fc op args) = mlfOp op (map mlfTm args)
    mlfTm (NmExtPrim fc n args) = mlfApply (mlfExtPrim n) (map mlfTm args)
    mlfTm (NmConCase fc scrut alts mbDflt) =
      bindScrut scrut $ \scrutN =>
        mlfSwitch
          (mlfLocalVar scrutN)
          (map (mlfConAlt scrutN) alts)
          (mlfConDflt . mlfTm <$> mbDflt)
    mlfTm (NmConstCase fc scrut alts mbDflt) =
      case the (Maybe (List Doc)) (traverse mlfConstAlt alts) of
        -- all patterns can be expressed efficiently
        Just alts' =>
          mlfSwitch (mlfTm scrut) alts' (mlfConstDflt . mlfTm <$> mbDflt)

        -- we need to use a chain of if-equals tests
        Nothing =>
          bindScrut scrut $ \scrutN =>
            mlfEqChain scrutN (mlfTm <$> mbDflt) alts

  mlfBody : NamedDef -> Doc
  mlfBody (MkNmFun args rhs) =
    mlfLam args (mlfTm rhs)

  mlfBody (MkNmCon mbTag arity mbNewtype) =
      mlfLam args (mlfBlock mbTag $ map mlfLocalVar args)
    where
      args : List Name
      args = [un $ "arg" ++ show i | i <- [0..cast {to = Int} arity-1]]

  mlfBody (MkNmForeign ccs args cty) =
    mlfLam (map fst lamArgs) $
      case ccLibFun ccs of
        Just fn => mlfLibCall fn (map mlfLocalVar mlArgs)
        Nothing =>
          mlfError $ "unimplemented foreign: " ++ show (MkNmForeign ccs args cty)
    where
      mkArgs : Int -> List CFType -> List (Name, Bool)
      mkArgs i [] = []
      mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs (i + 1) cs
      mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs

      -- arguments of the Malfunction lambda
      lamArgs : List (Name, Bool)
      lamArgs = mkArgs 0 args

      -- arguments of the foreign ML function
      mlArgs : List Name
      mlArgs = map fst $ case lamArgs of
        -- if we have only one argument, we have to keep it
        -- even if it's %World
        -- to avoid turning the function into a non-function
        [_] => lamArgs

        -- otherwise, attempt to remove %World
        _ => filter snd lamArgs

  mlfBody (MkNmError err) =
    mlfTm err

  mlfDef : (Name, FC, NamedDef) -> Doc
  mlfDef (n, fc, body) =
    parens (mlfGlobalVar n $$ indent (mlfBody body))
    $$ text ""

lazyDefs : List (Name, FC, NamedDef) -> SortedSet Name
lazyDefs [] = empty
lazyDefs ((n,_,MkNmFun [] rhs) :: defs) = insert n $ lazyDefs defs
lazyDefs ((n,_,MkNmCon tag Z nt) :: defs) = insert n $ lazyDefs defs
lazyDefs ((n,_,MkNmForeign ccs [] x) :: defs) = insert n $ lazyDefs defs
lazyDefs ((n,_,MkNmError x) :: defs) = insert n $ lazyDefs defs
lazyDefs (_ :: defs) = lazyDefs defs

mlfRec : List Doc -> Doc
mlfRec defs = parens $
  text "rec"
  $$ indentBlock defs

splitByNS : List (Name, FC, NamedDef) -> List (String, List (Name, FC, NamedDef))
splitByNS = StringMap.toList . foldl addOne StringMap.empty
  where
    addOne
      : StringMap (List (Name, FC, NamedDef))
      -> (Name, FC, NamedDef)
      -> StringMap (List (Name, FC, NamedDef))
    addOne nss def@(n, fc, nd) =
      StringMap.mergeWith
        (++)
        (StringMap.singleton (mlfNS n) [def])
        nss

-- https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm#The_algorithm_in_pseudocode
record TarjanVertex where
  constructor TV
  index : Int
  lowlink : Int
  inStack : Bool

record TarjanState where
  constructor TS
  vertices : StringMap TarjanVertex
  stack : List String
  nextIndex : Int
  components : List (List String)
  impossibleHappened : Bool

tarjan : StringMap (SortedSet String) -> List (List String)
tarjan deps = loop initialState (StringMap.keys deps)
  where
    initialState : TarjanState
    initialState =
      TS
        StringMap.empty
        []
        0
        []
        False

    strongConnect : TarjanState -> String -> TarjanState
    strongConnect ts v =
        let ts'' = case StringMap.lookup v deps of
              Nothing => ts'  -- no edges
              Just edgeSet => loop ts' (SortedSet.toList edgeSet)
          in case StringMap.lookup v ts''.vertices of
              Nothing => record { impossibleHappened = True } ts''
              Just vtv =>
                if vtv.index == vtv.lowlink
                  then createComponent ts'' v []
                  else ts''
      where
        createComponent : TarjanState -> String -> List String -> TarjanState
        createComponent ts v acc =
          case ts.stack of
            [] => record { impossibleHappened = True } ts
            w :: ws =>
              let ts' = record {
                      vertices $= StringMap.adjust w record{ inStack = False },
                      stack = ws
                    } ts
                in if w == v
                  then record { components $= ((v :: acc) ::) } ts'  -- that's it
                  else createComponent ts' v (w :: acc)

        loop : TarjanState -> List String -> TarjanState
        loop ts [] = ts
        loop ts (w :: ws) =
          loop (
            case StringMap.lookup w ts.vertices of
              Nothing => let ts' = strongConnect ts w in
                case StringMap.lookup w ts'.vertices of
                  Nothing => record { impossibleHappened = True } ts'
                  Just wtv => record { vertices $= StringMap.adjust v record{ lowlink $= min wtv.lowlink } } ts'

              Just wtv => case wtv.inStack of
                False => ts  -- nothing to do
                True => record { vertices $= StringMap.adjust v record{ lowlink $= min wtv.index } } ts
          ) ws

        ts' : TarjanState
        ts' = record {
            vertices  $= StringMap.insert v (TV ts.nextIndex ts.nextIndex True),
            stack     $= (v ::),
            nextIndex $= (1+)
          } ts

    loop : TarjanState -> List String -> List (List String)
    loop ts [] =
      if ts.impossibleHappened
        then []
        else ts.components
    loop ts (v :: vs) =
      case StringMap.lookup v ts.vertices of
        Just _ => loop ts vs  -- done, skip
        Nothing => loop (strongConnect ts v) vs

coreFor : List a -> (a -> Core b) -> Core (List b)
coreFor xs f = Core.traverse f xs

record ModuleInfo where
  constructor MkMI
  name : ModuleName
  outdated : Bool

generateModules : Ref Ctxt Defs -> ClosedTerm -> (outfile : String) -> Core (List ModuleInfo)
generateModules c tm bld = do
  cdata <- getCompileData False Cases tm
  let ndefs = namedDefs cdata
  let ctm = forget (mainExpr cdata)
  let ldefs = lazyDefs ndefs
  let defsByNS = StringMap.fromList $ splitByNS ndefs
  let defDepsRaw = [StringMap.singleton (mlfNS n) (SortedSet.delete (mlfNS n) (nsDef d)) | (n, fc, d) <- ndefs]
  let defDeps = foldl (StringMap.mergeWith SortedSet.union) StringMap.empty defDepsRaw
  let components = reverse $ tarjan defDeps  -- tarjan generates reverse toposort

  -- map each module name / namespace
  -- to the representative from its component
  let nsMapping =
        foldl
          (\nm, modNames => case modNames of
            [] => nm
            mn :: mns =>
              let mlMod = MkMN (foldl min mn mns)
                in foldl (\nm, modName => StringMap.insert modName mlMod nm)
                    nm
                    modNames
          )
          StringMap.empty
          components

  -- generate one module per strongly connected component
  -- start with Builtins, work up to modules with many dependencies
  outdatedModNames <- coreLift $ newIORef SortedSet.empty
  moduleNames <- coreFor components $ \modNames => case modNames of
    [] => throw $ InternalError "empty connected component"
    mn :: mns => do
      let mlModName = MkMN (foldl min mn mns)
      let defs = concatMap (\modName => fromMaybe [] $ StringMap.lookup modName defsByNS) modNames
      let defsMlf = map (mlfDef ldefs nsMapping mlModName) defs
      let code = render " " $ parens (
            text "module"
            $$ indent (
                 mlfRec defsMlf
              $$ text ""
              $$ parens (
                text "export"
                $$ indent (vcat [mlfGlobalVar n | (n, _, _) <- defs])
                )
              )
            )
            $$ text ""
            $$ text "; vim: ft=lisp"
            $$ text ""  -- end with a newline

      -- check if the files need updating
      let codeHashStr = show (hash code) ++ "\n"
      mbPrevHash <- coreLift (readFile (bld </> mlModName.string <.> "hash")) >>= \case
        Left err => pure $ Nothing
        Right h  => pure $ Just h

      isUpToDate <- do
        outdatedMNs <- coreLift $ readIORef outdatedModNames
        let allDeps = concat
              [ fromMaybe SortedSet.empty (StringMap.lookup n defDeps)
              | n <- with Prelude.(::) mn :: mns
              ]
        pure $
          -- hash matches
          (mbPrevHash == Just codeHashStr)
          -- no deps are outdated
          -- we check only direct deps because we're traversing in dep order, anyway
          && (null $ SortedSet.intersection allDeps outdatedMNs)

      if isUpToDate
        then pure (MkMI mlModName False)  -- up to date, nothing to do
        else do
          -- mark all namespaces in this module as outdated
          coreLift $ do
            omns <- readIORef outdatedModNames
            writeIORef outdatedModNames $
              omns <+> SortedSet.fromList (mn :: mns)

          -- write the MLF file
          let fname = bld </> mlModName.string <.> "mlf"
          Right () <- coreLift $ writeFile fname code
            | Left err => throw (FileErr fname err)

          -- update the hash file
          -- write into .hash.tmp, which will be renamed to .hash
          -- once the build succeeds
          let fname = bld </> mlModName.string <.> "hash.tmp"
          Right () <- coreLift $ writeFile fname codeHashStr
            | Left err => throw (FileErr fname err)

          -- write the MLI file
          let mliCode = render " " $
                vcat
                  [ text "val" <++> mlfGlobalName n <++> text ": 'a"
                  | (n, _, _) <- defs
                  ]
          let fname = bld </> mlModName.string <.> "mli"
          Right () <- coreLift $ writeFile fname mliCode
            | Left err => throw (FileErr fname err)

          pure (MkMI mlModName True)

  -- generate the main module
  mainMlf <- pure $ mlfTm ldefs nsMapping (MkMN "Main") ctm
  let code = render " " $ parens (
        text "module"
        $$ indent (
          parens (text "_" <++> mainMlf)
          $$ text ""
          $$ parens (text "export")
          )
        )
        $$ text ""
        $$ text "; vim: ft=lisp"
        $$ text ""  -- end with a newline
  Right () <- coreLift $ writeFile (bld </> "Main.mlf") code
    | Left err => throw (FileErr (bld </> "Main.mlf") err)

  -- write an empty hash file
  Right () <- coreLift $ writeFile (bld </> "Main.hash.tmp") ""
    | Left err => throw (FileErr (bld </> "Main.hash.tmp") err)

  -- write an empty Main.mli
  Right () <- coreLift $ writeFile (bld </> "Main.mli") ""
    | Left err => throw (FileErr (bld </> "Main.mli") err)

  pure $ moduleNames ++ [MkMI (MkMN "Main") True]

firstAvailable : List String -> String -> Core (Maybe String)
firstAvailable [] fname = pure Nothing
firstAvailable (dir :: dirs) fname = do
  let path = dir </> fname
  case !(coreLift $ openFile path Read) of
    Right f => do
      coreLift $ closeFile f
      pure (Just path)
    Left _ => firstAvailable dirs fname

copy : Dirs -> String -> String -> Core ()
copy dirs bld fn =
  firstAvailable dirs.data_dirs fn >>= \case
    Nothing => throw $ InternalError ("idris2-mlf/copy: could not find " ++ fn)
    Just path => do
      0 <- coreLift $ system $ unwords ["cp", path, bld]
        | e => throw (FileErr path (GenericFileError 0))
      pure ()

compileExpr : Ref Ctxt Defs
  -> (tmpDir : String) -> (outputDir : String)
  -> ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr c tmpDir outputDir tm outfile = do
  let bld = tmpDir </> "mlf-" ++ outfile
  Right () <- coreLift $ mkdirAll bld
    | Left err => throw (FileErr bld err)

  -- malfunction does not support libs in another directory
  -- let's just copy all of them
  dirs <- getDirs
  copy dirs bld ("mlf" </> "Rts.cmx")
  copy dirs bld ("mlf" </> "Rts.cmi")
  copy dirs bld ("mlf" </> "Rts.o")
  copy dirs bld ("mlf" </> "rts_c.o")

  modules <- generateModules c tm bld

  let cmd = unwords
        [ " (cd " ++ bld
        -- rebuild only the outdated MLF modules
        , unwords
          [    " && ocamlfind opt -I +threads -g -c " ++ mod.name.string ++ ".mli "
            ++ " && malfunction cmx " ++ mod.name.string ++ ".mlf"
            -- mark the module build as successful
            ++ " && mv " ++ mod.name.string ++ ".hash.tmp " ++ mod.name.string ++ ".hash"
          | mod <- modules
          , mod.outdated
          ]
        -- link it all together
        , "&& ocamlfind opt -thread -package zarith -linkpkg -nodynlink -g "
            ++ "rts_c.o "
            ++ !(findLibraryFile "libidris2_support.a") ++ " "
            ++ "Rts.cmx "
            ++ unwords [mod.name.string ++ ".cmx" | mod <- modules]
            ++ " -o ../" ++ outfile
        , ")"
        ]

  coreLift $ putStrLn cmd
  ok <- coreLift $ system cmd
  if ok == 0
    then pure (Just (outputDir </> outfile))
    else pure Nothing

executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm
    = do outn <- compileExpr c tmpDir tmpDir tm "_tmp_mlf"
         case outn of
              -- TODO: on windows, should add exe extension
              Just outn => map (const ()) $ coreLift $ system outn
              Nothing => pure ()

main : IO ()
main = mainWithCodegens
  [ ("mlf", MkCG compileExpr executeExpr Nothing Nothing)
  ]


text:
module System.FFI.Lua

import Data.List

%default total

export
data External : Type where [external]

%foreign "idris.support.world|support"
world : External

%foreign "function(_) end"
prim__compile : List External -> PrimIO ()

export
compile : HasIO io => List External -> io ()
compile externals = primIO (prim__compile externals)

export
data OpaqueDict : Type where [external]

-- TODO: How we properly manage nil?

public export
data Dict : List (String, Type) -> Type where
  MkDict : OpaqueDict -> Dict ts

public export
data List : List Type -> Type where
  MkList : (n : Nat) -> OpaqueDict -> n = length ts => List ts

%foreign "{}"
prim__empty : OpaqueDict

namespace Dict
  public export
  data FieldType : String -> Type -> List (String, Type) -> Type where
    First : FieldType n t ((n, t) :: ts)
    Later : FieldType n t ts -> FieldType n t (f :: ts)

  %foreign "_, d, n => d[n]"
  prim__getField : OpaqueDict -> (n : String) -> ty

  %foreign "_, d, n, v => function(_) d[n] = v end"
  prim__setField : OpaqueDict -> (n : String) -> ty -> PrimIO ()

  public export %inline
  getField : Dict ts -> (n : String) -> FieldType n ty ts => ty
  getField (MkDict dict) field = prim__getField dict field

  public export %inline
  setField : HasIO io => Dict ts -> (n : String) -> FieldType n ty ts => ty -> io ()
  setField (MkDict dict) field val = primIO $ prim__setField dict field val

  export
  empty : Dict []
  empty = MkDict prim__empty

  export
  addField : HasIO io => (n : String) -> (val : t) -> Dict ts -> io (Dict ((n, t) :: ts))
  addField n val (MkDict dict) = do
    primIO $ prim__setField dict n val
    pure (MkDict dict)

namespace List
  public export
  data FieldType : Nat -> Type -> List Type -> Type where
    First : FieldType 1 t (t :: ts)
    Later : FieldType n t ts -> FieldType (S n) t (t' :: ts)

  %foreign "_, d, n => d[n]"
  prim__getField : OpaqueDict -> (n : Nat) -> ty

  %foreign "_, d, n, v => function(_) d[n] = v end"
  prim__setField : OpaqueDict -> (n : Nat) -> ty -> PrimIO ()

  public export %inline
  getField : List ts -> (n : Nat) -> FieldType n ty ts => ty
  getField (MkList _ list) field = prim__getField list field

  public export %inline
  setField : HasIO io => List ts -> (n : Nat) -> FieldType n ty ts => ty -> io ()
  setField (MkList _ list) field val = primIO $ prim__setField list field val

  export
  empty : List []
  empty = MkList _ prim__empty

  lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
              length (xs ++ (y :: ys)) = S (length (xs ++ ys))
  lengthSuc [] _ _ = Refl
  lengthSuc (x :: xs) y ys = cong S (lengthSuc xs y ys)

  export
  addField : HasIO io => (val : t) -> List ts -> io (List (ts ++ [t]))
  addField val (MkList size list @{prf}) = do
    primIO $ prim__setField list (S size) val
    pure (MkList (S size) list @{rewrite prf in
                                 rewrite lengthSuc ts t [] in
                                 rewrite appendNilRightNeutral ts in Refl})

%foreign "v, _ => v == nil"
prim__isNil : OpaqueDict -> PrimIO Bool

isNil : HasIO io => OpaqueDict -> io Bool
isNil = primIO . prim__isNil


text:
module Eval

import Syntax

export
eval : Expression -> Integer
eval (Numeral i)    = i
eval (Plus   e1 e2) = (eval e1) + (eval e2)
eval (Minus  e1 e2) = (eval e1) - (eval e2)
eval (Times  e1 e2) = (eval e1) * (eval e2)
eval (Divide e1 e2) = (eval e1) `div` (eval e2) -- Note: a bit evil - will fail with RTS exception.
eval (Negate e)     = -(eval e)

max_stars_repo_name: steshaw/idris-calc

max_issues_repo_name: steshaw/idris-calc

max_forks_repo_name: steshaw/idris-calc


text:
import Data.Fin
import Data.List
import Data.Nat
import Data.SortedSet as S
import Data.String.Parser
import Data.Vect

import System.File

Node : Type
Node = (Nat, Nat)

-- A Non empty grid
Grid : Nat -> Type
Grid n = Vect (S n) (Vect (S n) Node)

gupdateAt : (Fin (S n), Fin (S n)) -> (Node -> Node) -> Grid n -> Grid n
gupdateAt (x, y) f = updateAt y (updateAt x f)

gindex : (Fin (S n), Fin (S n)) -> Grid n -> Node
gindex (x, y) = index x . index y

inf : Nat
inf = 1000000

parser : Parser (n ** Grid n)
parser = do row <- some digit <* char '\n'
            let n = length row
            Just v <- pure $ toVect n $ (,inf) . finToNat <$> row
              | Nothing => fail "not length"
            Yes ItIsSucc <- pure $ isItSucc n
              | No _ => fail "Row is zero"
            vs <- ntimes (pred n) (((map ((,inf) . finToNat)) <$> ntimes n digit) <* char '\n')
            pure $ MkDPair (pred n) (v :: vs)

decFin : Fin n -> Maybe (Fin n)
decFin FZ = Nothing
decFin (FS x) = Just $ weaken $ x
incFin : {n : Nat} -> Fin n -> Maybe (Fin n)
incFin f = strengthen $ shift 1 f

neighbours : {n : Nat} -> (Fin n, Fin n) -> List (Fin n, Fin n)
neighbours (x, y) = ((, y) <$> catMaybes [decFin x, incFin x]) ++
                    ((x, ) <$> catMaybes [decFin y, incFin y])

lowestRisk' : {n : Nat} -> List (Fin (S n), Fin (S n)) -> Grid n -> Grid n
lowestRisk' [] g = g
lowestRisk' ((x, y) :: queue) g = let (_, d) = gindex (x, y) g
                                      n = filter (\p => let (v, t) = gindex p g in v + d < t) $ neighbours (x, y)
                                      ng = foldl (\g' => \p => gupdateAt p (\(v, _) => (v, v + d)) g') g $ n
                                      nq = queue ++ n in
                                      lowestRisk' nq ng

lowestRisk : {n : Nat} -> Grid n -> Grid n
lowestRisk g = lowestRisk' ((0, 0) :: []) (gupdateAt (0, 0) (mapSnd (const 0)) g)

wrapAdd : Nat -> Nat -> Nat
wrapAdd 0 n = n
wrapAdd (S k) n = if n == 9
                     then wrapAdd k 1
                     else wrapAdd k (S n)

largerRow : Vect (S n) (Nat, Nat) -> Vect (5 * (S n)) (Nat, Nat)
largerRow v = v ++ (concat $ ((\a => mapFst (wrapAdd a) <$> v) <$> [1,2,3,4]))

largerColumn : Vect (S n) (Vect (5 * (S n)) (Nat, Nat)) -> Vect (5 * (S n)) (Vect (5 * (S n)) (Nat, Nat))
largerColumn v = v ++ (concat $ ((\a => (mapFst (wrapAdd a) <$>) <$> v) <$> [1,2,3,4]))

largerGrid : Grid n -> Grid (pred (5 * (S n)))
largerGrid g = let rowextended = largerRow <$> g in
                   largerColumn rowextended

run : String -> IO ()
run s = do Right (MkDPair n g, _) <- pure $ parse parser s
             | Left err => putStrLn $ show err
           let g = lowestRisk $ largerGrid g
           putStrLn $ show $ snd $ gindex (last, last) g

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s


text:
module Algebra.Solver.Semiring.Util

import Algebra.Semiring
import public Syntax.PreorderReasoning

%default total

export
0 p213 : Semiring a => {k,m,n : a} -> k + (m + n) === m + (k + n)
p213 = Calc $
  |~ k + (m + n)
  ~~ (k + m) + n   ... plusAssociative
  ~~ (m + k) + n   ... cong (+n) plusCommutative
  ~~ m + (k + n)   ..< plusAssociative

export
0 p1324 :  Semiring a
        => {k,l,m,n : a}
        -> (k + l) + (m + n) === (k + m) + (l + n)
p1324 = Calc $
  |~ (k + l) + (m + n)
  ~~ ((k + l) + m) + n ... plusAssociative
  ~~ (k + (l + m)) + n ..< cong (+n) plusAssociative
  ~~ (k + (m + l)) + n ... cong (\x => (k + x) + n) plusCommutative
  ~~ ((k + m) + l) + n ... cong (+n) plusAssociative
  ~~ (k + m) + (l + n) ..< plusAssociative

export
0 m1324 :  Semiring a
        => {k,l,m,n : a}
        -> (k * l) * (m * n) === (k * m) * (l * n)
m1324 = Calc $
  |~ (k * l) * (m * n)
  ~~ ((k * l) * m) * n ... multAssociative
  ~~ (k * (l * m)) * n ..< cong (*n) multAssociative
  ~~ (k * (m * l)) * n ... cong (\x => (k * x) * n) multCommutative
  ~~ ((k * m) * l) * n ... cong (*n) multAssociative
  ~~ (k * m) * (l * n) ..< multAssociative


text:
-- Idris2

import System
import System.Concurrency

-- Test `conditionWaitTimeout` times out m of n threads for 1 main and n child
-- threads

main : IO ()
main =
  let
    n = 5
    m = 3
  in
    do cvMutex <- makeMutex
       cv <- makeCondition

       -- spawn n-m inifinitely patient children
       waiting <- for [1..(n - m)] $ \_ => fork $
             do mutexAcquire cvMutex
                conditionWait cv cvMutex
                putStrLn "Woke up despite no timeout (SHOULDN'T HAPPEN)"
                mutexRelease cvMutex

       -- spawn m impatient children
       impatients <- for [1..m] $ \_ => fork $
             do mutexAcquire cvMutex
                conditionWaitTimeout cv cvMutex 1000000
                putStrLn "Where are you mother?"
                mutexRelease cvMutex

       sleep m
       putStrLn "Sorry I'm late children! Weren't there more of you?..."
       for impatients $ \t => threadWait t
       sleep 1


text:
module Test.Int

import Data.Prim.Int
import Data.SOP
import Hedgehog
import Test.RingLaws

allInt : Gen Int
allInt = int (linear (-0x8000000000000000) 0xffffffffffffffff)

prop_comp : Property
prop_comp = property $ do
  [m,n] <- forAll $ np [allInt, allInt]
  toOrdering (comp m n) === compare m n

export
props : Group
props = MkGroup "Int16" $
  [ ("prop_comp",   prop_comp)
  ] ++ ringProps allInt


text:
module Streams

labelWith : Stream labelType -> List a -> List (labelType, a)
labelWith lbs [] = []
labelWith (label :: ls) (x :: xs) = (label, x) :: labelWith ls xs

label : List a -> List (Integer, a)
label = labelWith (iterate (+1) 0)

max_stars_repo_path: Chapter 11/Streams.idr

max_issues_repo_path: Chapter 11/Streams.idr

max_forks_repo_path: Chapter 11/Streams.idr


text:
-- --------------------------------------------------------------- [ Error.idr ]
-- Module    : Error.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

module ArgParse.Error

import public ArgParse.Model

import ArgParse.Parser

%access public export

data ArgParseError : Type where
  InvalidOption : Arg -> ArgParseError
  ParseError : ParseError -> ArgParseError

implementation (Show Arg) => Show ArgParseError where
  show (InvalidOption o) = "Invalid Option " ++ show o
  show (ParseError err)  = "Parsing Error\n" ++ show err

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

max_stars_repo_name: jfdm/idris-argparse

max_issues_repo_name: jfdm/idris-argparse

max_forks_repo_name: jfdm/idris-argparse


text:
module TestBuffer

import Data.Buffer
import System.File

put : Show a => IO a -> IO ()
put = (>>= putStrLn . show)

main : IO ()
main = do
    Just buf <- newBuffer 31
        | Nothing => pure ()

    setByte buf 0 1
    setBits8 buf 1 2
    setInt buf 2 0x1122334455667788
    setDouble buf 10 (sqrt 2)

    let helloWorld = "Hello, world"

    Just helloWorldBuf <- newBuffer (stringByteLength helloWorld)
        | Nothing => pure ()

    setString helloWorldBuf 0 "Hello, world"
    copyData helloWorldBuf 0 12 buf 18

    put $ rawSize buf

    put $ getByte buf 0
    put $ getBits8 buf 1
    put $ getInt buf 2
    put $ getDouble buf 10
    put $ getString buf 18 12

    put $ bufferData buf

    Just readBuf <- newBuffer 8
        | Nothing => pure ()
    Right f <- openFile "testRead.buf" Read
        | Left err => put $ pure err
    Right () <- readBufferData f readBuf 0 8
        | Left err => put $ pure err
    put $ bufferData readBuf

    Just writeBuf <- newBuffer 8
        | Nothing => pure ()
    setInt writeBuf 0 0x7766554433221100
    Right f <- openFile "testWrite.buf" WriteTruncate
        | Left err => put $ pure err
    Right () <- writeBufferData f writeBuf 0 8
        | Left err => put $ pure err

    pure ()


text:
module TypGleichheit

import Data.Vect

congruent : { ty, ty' : Type } -> { a,b : ty } -> {f : ty -> ty' } -> (a = b) -> (f a = f b)
congruent Refl = Refl

gleicheZahl : (a : Nat) -> (b : Nat) -> Maybe (a = b)
gleicheZahl Z Z = Just Refl
gleicheZahl Z (S k) = Nothing
gleicheZahl (S k) Z = Nothing
gleicheZahl (S k) (S j) =
  case gleicheZahl k j of
    Just prf => Just (congruent prf)

plus1IstSucc : (n:Nat) -> S n = n+1
plus1IstSucc Z = Refl
plus1IstSucc (S k) = cong (plus1IstSucc k)

vecReverse : Vect n a -> Vect n a
vecReverse [] = []
vecReverse (x :: xs) =
  let ind = vecReverse xs
      v' = ind ++ [x]
  in isSame v'
  where
    isSame : Vect (k + 1) a -> Vect (S k) a
    isSame {k} v = rewrite (plus1IstSucc k) in v


text:
module MoreNatProofs

%access public export
%default total

||| If a /= b then b /= a
notEqReflexive : ((a = b) -> Void) -> (b = a) -> Void
notEqReflexive f Refl = f Refl

||| A decision procedure for `DecEq Nat`
||| @ m the first number
||| @ n the second number
isEq : (m : Nat) -> (n : Nat) -> Dec (m = n)
isEq m n = decEq m n

eQImpliesEq : {m, n : Nat} -> (m = n) -> (n = m)
eQImpliesEq {m = n} {n = n} Refl = Refl

eQAndNotEqImpossible : {n, k : Nat} -> (contra1 : (n = k) -> Void) -> (n = k) -> a
eQAndNotEqImpossible {n} {k} contra1 prf = void (contra1 prf)

||| Proofs that `m` is not equal to `n`
||| @ m the first number
||| @ n the second number
NotEq : (m, n : Nat) -> Type
NotEq m n = Not (m=n)

||| Not (m = n) implies m /= n
notEqImpliesNotEq : (contra : (m = n) -> Void) -> ((m = n) -> Void)
notEqImpliesNotEq contra Refl = contra Refl

||| (m = n) implies Not (m /= n)
eqImpliesNotNotEq : (prf : m = n) -> (((m = n) -> Void) -> Void)
eqImpliesNotNotEq Refl f = f Refl

||| A decision procedure for `NotEq`
isNotEq : (m : Nat) -> (n : Nat) -> Dec (NotEq m n)
isNotEq m n = case (isEq m n) of
                   (Yes prf) => No (eqImpliesNotNotEq prf)
                   (No contra) => Yes (notEqImpliesNotEq contra)

||| A successor is always greater than or equal zero
succGTEzero : GTE (S k) Z
succGTEzero = LTEZero

||| Zero cannot be greater than or equal to a successor
zeroNotGTESucc : LTE (S k) 0 -> Void
zeroNotGTESucc LTEZero impossible
zeroNotGTESucc (LTESucc _) impossible

||| A decision procedure for `GTE`
isGTE : (m : Nat) -> (n : Nat) -> Dec (GTE m n)
isGTE Z Z = Yes LTEZero
isGTE Z (S k) = No zeroNotGTESucc
isGTE (S k) Z = Yes succGTEzero
isGTE (S k) (S j) with (isGTE k j)
  isGTE (S k) (S j) | (Yes prf) = Yes (LTESucc prf)
  isGTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)

||| If n > m, then n + 1 > m + 1
GTSucc : (prf : LTE j k) -> LTE (S j) (S k)
GTSucc prf = LTESucc prf

||| Zero cannot be less than itself
zeroNotLTZero : LT 0 0 -> Void
zeroNotLTZero LTEZero impossible
zeroNotLTZero (LTESucc _) impossible

||| If 1 <= n + 1, then n + 1 > 0
succGTZero : LTE 1 (S k)
succGTZero = LTESucc LTEZero

||| A decision procedure for `GT`
isGT : (m : Nat) -> (n : Nat) -> Dec (GT m n)
isGT Z Z = No zeroNotLTZero
isGT Z (S k) = No zeroNotGTESucc
isGT (S k) Z = Yes succGTZero
isGT (S k) (S j) with (isGT k j)
  isGT (S k) (S j) | (Yes prf) = Yes (GTSucc prf)
  isGT (S k) (S j) | (No contra) = No (contra . fromLteSucc)

||| A decision procedure for `LT`
isLT : (m : Nat) -> (n : Nat) -> Dec (LT m n)
isLT Z Z = No zeroNotLTZero
isLT Z (S k) = Yes (LTESucc LTEZero)
isLT (S k) Z = No succNotLTEzero
isLT (S k) (S j) with (isLT k j)
  isLT (S k) (S j) | (Yes prf) = Yes (LTESucc prf)
  isLT (S k) (S j) | (No contra) = No (contra . fromLteSucc)

eqImpliesLTE : (n = k) -> LTE n k
eqImpliesLTE {n = Z} Refl = LTEZero
eqImpliesLTE {n = (S (S (S k)))} Refl = LTESucc (LTESucc (LTESucc (eqImpliesLTE Refl)))
eqImpliesLTE {n = (S k)} Refl = LTESucc (eqImpliesLTE Refl)

eqABImpliesEqBA : (prf : n = k) -> k = n
eqABImpliesEqBA Refl = Refl

notLTEandEqImpossible : (contra : LTE n k -> Void) -> (prf : n = k) -> LTE k n
notLTEandEqImpossible contra prf = eqImpliesLTE (eqABImpliesEqBA prf)

gTImpliesLTE : (prf : GT n k) -> LTE k n
gTImpliesLTE {n = (S left)} {k = (S right)} (LTESucc x) = LTESucc (gTImpliesLTE x)
gTImpliesLTE {n = Z} {k = Z} LTEZero impossible
gTImpliesLTE {n = Z} {k = Z} (LTESucc _) impossible
gTImpliesLTE {n = Z} {k = (S _)} LTEZero impossible
gTImpliesLTE {n = Z} {k = (S _)} (LTESucc _) impossible
gTImpliesLTE {n = (S j)} {k = Z} (LTESucc x) = LTEZero

notGTImpliesLTE : Not (GT a b) -> LTE a b
notGTImpliesLTE {a = Z} _ = LTEZero
notGTImpliesLTE {b = Z} {a = S k} notGt = absurd (notGt (LTESucc LTEZero))
notGTImpliesLTE {b = S k} {a = S j} notGt = LTESucc (notLTImpliesGTE (notGt . LTESucc))

notLTEFlips : (contra : LTE n k -> Void) -> LTE k n
notLTEFlips {n} {k} contra = case isEq n k of
                                  (Yes prf) => notLTEandEqImpossible contra prf
                                  (No contra1) => (case isGT n k of
                                                        (Yes prf) => gTImpliesLTE prf
                                                        (No contra2) => gTImpliesLTE (void (contra (notGTImpliesLTE contra2))))

lTESkk : (k : Nat) -> ((S k) `LTE` k) -> Void
lTESkk Z LTEZero impossible
lTESkk Z (LTESucc _) impossible
lTESkk (S k) (LTESucc x) = lTESkk k x

lTELeftNotSuccOfRight : (x : LTE (S k) k) -> Void
lTELeftNotSuccOfRight {k} x = lTESkk k x

||| k <= k
lTEkk : Nat.LTE k k
lTEkk {k = Z} = LTEZero
lTEkk {k = (S k)} = LTESucc lTEkk

max_stars_repo_name: zenntenn/Idris-NumericProofs

max_issues_repo_name: zenntenn/Idris-NumericProofs

max_forks_repo_name: zenntenn/Idris-NumericProofs


text:
%nomangle
continue : Int -> Int
continue x = x + 1

main : IO ()
main = pure ()


text:
-- ---------------------------------------------------------------- [ Effs.idr ]
-- Module    : Effs.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Effectful definitions
module GRL.Lang.Common.Effs

import System

import Effects
import Effect.System
import Effect.StdIO
import Effect.State
import Effect.Exception
import Effect.File

import Data.AVL.Dict

import Lightyear
import Lightyear.Char
import Lightyear.Strings
import Lightyear.StringFile

import GRL.Common
import GRL.Model
import GRL.IR
import GRL.Builder

import GRL.Lang.Common.Error

import GRL.Eval

%access export

-- ----------------------------------------------------------------- [ Context ]

public export
GEnv : Type -> Type
GEnv val = Dict String val

Default (GEnv a) where
  default = empty

-- ------------------------------------------------------- [ Effectful Context ]
public export
Lang : Type -> Type -> Type
Lang cTy rTy = Eff rTy
                   [ SYSTEM
                   , FILE_IO ()
                   , STDIO
                   , STATE (GEnv cTy)
                   , EXCEPTION GError]

||| Read in a language specification
readLangFile : Parser a
            -> String
            -> Lang ty a
readLangFile p f = do
    res <- parseFile (NoSuchFileError) (ParserError) p f
    case res of
      Left err  => raise err
      Right ast => pure ast

||| Add element to the context.
getElem : String -> Lang cTy cTy
getElem id = do
  env <- get
  case (lookup id env) of
    Nothing => raise $ NoSuchIdentError id
    Just e  => pure e

evaluateE : GModel
         -> Maybe Strategy
         -> Lang cTy EvalResult
evaluateE m strat = pure $ evaluate FORWARD strat m

processArgs : List String -> Lang cTy (String, Maybe String)
processArgs Nil           = raise NoFileError
processArgs [x]           = raise NoFileError
processArgs [x,y]         = pure (y, Nothing)
processArgs (x::y::z::xs) = pure (y, Just z)

-- ------------------------------------------------------------------ [ Pretty ]

showRes : (GoalNode -> String) -> EvalResult -> Lang cTy ()
showRes pfunc res =
    case toString res pfunc of
      Nothing  => raise BadModelError
      Just res => putStrLn res

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Test.Unit.Spec

import Control.App
import Control.App.Console
import Data.Maybe
import Data.Either
import Data.List      -- for replicate

%default total

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

public export
data TestFailure : Type where
  Unexpected : Show a => (expect : a) -> (actual : a) -> TestFailure
  UnexpectedMaybe : Show a => (actual : Maybe a) -> TestFailure
  UnexpectedEither : (Show a, Show b) => (actual : Either a b) -> TestFailure
Show TestFailure where
  show (Unexpected e a) = "Expected " ++ show e ++ ", But actual is " ++ show a
  show (UnexpectedMaybe x@(Just _)) = "Expected Nothing, But actual is " ++ show x
  show (UnexpectedMaybe x@Nothing) = "Expected Just _, But actual is " ++ show x
  show (UnexpectedEither x@(Left _)) = "Expected Right _, But actual is " ++ show x
  show (UnexpectedEither x@(Right _)) = "Expected Left _, But actual is " ++ show x

public export
interface UnitTest e where
  %inline assertEqual    : (Show t, Eq t) => t -> t -> App e ()
  %inline assertNotEqual : (Show t, Eq t) => t -> t -> App e ()
  %inline assertTrue     : Bool -> App e ()
  %inline assertFalse    : Bool -> App e ()
  %inline assertJust     : Show t => Maybe t -> App e ()
  %inline assertNothing  : Show t => Maybe t -> App e ()
  %inline assertRight    : (Show a, Show b) => Either a b -> App e ()
  %inline assertLeft     : (Show a, Show b) => Either a b -> App e ()

export %inline throwUnless    : Exception TestFailure e => Bool -> TestFailure -> App e ()
throwUnless b err = if b then pure () else throw err

public export
Has [Exception TestFailure] e => UnitTest e where
  assertEqual e a = throwUnless (e == a) $ Unexpected e a
  assertNotEqual e a = throwUnless (e /= a) $ Unexpected e a
  assertTrue a = throwUnless a $ Unexpected True False
  assertFalse a = throwUnless (not a) $ Unexpected False True
  assertJust a = throwUnless (isJust a) $ UnexpectedMaybe a
  assertNothing a = throwUnless (isNothing a) $ UnexpectedMaybe a
  assertRight a = throwUnless (isRight a) $ UnexpectedEither a
  assertLeft a = throwUnless (isLeft a) $ UnexpectedEither a

export runUnitTest : App (TestFailure::e) () -> App e (Maybe TestFailure)
runUnitTest tst = handle tst (pure . const Nothing) (pure . Just)

export runIOUnitTest : Has [PrimIO, Console] e => App (TestFailure::e) () -> App e (Maybe TestFailure)
runIOUnitTest tst = handle tst (pure . const Nothing) (pure . Just)

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

public export
interface Spec e where
  %inline describe : String -> App e () -> App e ()
  %inline tests  : String -> App (TestFailure::e) () -> App e ()
  %inline skip     : App e () -> App e ()

record TestStatus where
  constructor MkTestStatus
  numDescribes : Int
  numTests : Int
  numFailed : Int
  skipping : Bool
  nestlevel : Int

-- ---------------------------------------------------------------------------
-- Console runner

export
0 ConsoleTest : List Error -> Type
ConsoleTest = Has [Console, PrimIO, State TestStatus TestStatus]

public export partial
[markdown] ConsoleTest e => Spec e where
  describe sbj bdy = do
    sts <- get TestStatus
    putStrLn $ (pack $ replicate (fromInteger $ cast sts.nestlevel + 1) '#') ++ (if sts.skipping then " [SKIP] " else " ") ++ sbj
    put TestStatus $ { numDescribes $= (+ 1), nestlevel $= (+ 1) } sts
    bdy
    sts' <- get TestStatus
    put TestStatus $ { nestlevel $= (\x => x - 1) } sts'
  tests sbj bdy = do
    sts <- get TestStatus
    put TestStatus $ { numTests $= (+ 1) } sts
    putStrLn $ "    - " ++ (if sts.skipping then "[SKIP] " else "") ++ sbj
    if sts.skipping
       then pure ()
       else
         runIOUnitTest bdy >>= maybe (pure ()) (\e => do
           modify TestStatus (record { numFailed $= (+ 1) })
           putStrLn $ "TestFailed!!!  " ++ show e)
  skip tst = do
    sts <- get TestStatus
    modify TestStatus $ record { skipping = True }
    tst
    modify TestStatus $ record { skipping = sts.skipping }

export partial consoleRunSpec : Has [Console, PrimIO] e =>
                                 (Spec e => App e ())
                                 -> App e ()
consoleRunSpec tst = new (MkTestStatus 0 0 0 False 0) $ do
  putStrLn "------------------------------------------------"
  tst @{markdown}
  r <- get TestStatus
  putStrLn "------------------------------------------------"
  putStrLn "Done"
  putStrLn $ "  Total desc. : " ++ show r.numDescribes
  putStrLn $ "  Total tests. : " ++ show r.numTests
  putStrLn $ "  Total failure. : " ++ show r.numFailed

data TestAt : Type where

public export partial
[simple] Has [ConsoleTest, State TestAt (List String)] e => Spec e where
  describe sbj bdy = do
    sts <- get TestStatus
    putChar $ if sts.skipping then '*' else '#'
    put TestStatus $ { numDescribes $= (+ 1), nestlevel $= (+ 1) } sts
    modify TestAt (\xs => sbj :: xs)
    bdy
    sts' <- get TestStatus
    put TestStatus $ { nestlevel $= (\x => x - 1) } sts'
    modify TestAt (\(_::xs) => xs)
  tests sbj bdy = do
    sts <- get TestStatus
    put TestStatus $ { numTests $= (+ 1) } sts
    putChar $ if sts.skipping then '.' else '-'
    if sts.skipping
       then pure ()
       else
         runIOUnitTest bdy >>= maybe (pure ()) (\e => do
           testat <- get TestAt
           modify TestStatus (record { numFailed $= (+ 1) })
           putStrLn $ "! " ++ concat (intersperse " : " (testat ++ [show e])) )
  skip tst = do
    sts <- get TestStatus
    modify TestStatus $ record { skipping = True }
    tst
    modify TestStatus $ record { skipping = sts.skipping }

export partial consoleRunSpecSimple : Has [Console, PrimIO] e =>
                                      (Spec e => App e ())
                                      -> App e ()
consoleRunSpecSimple tst =
  new {tag=TestStatus} (MkTestStatus 0 0 0 False 0) $
    new {tag=TestAt} [] $ do
      tst @{simple}
      r <- get TestStatus
      putStrLn $ "Done. " ++ show r.numFailed ++ " / " ++ show r.numTests

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


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Lens
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Control.Lens.At

import Control.Lens.Setter
import Control.Lens.Types
import Control.Monad.Identity
import Data.Profunctor
import Data.List

%default total

public export
interface Ixed ( m : Type ) where
  IxInd : Type
  IxVal : Type
  ix : IxInd -> { f : Type -> Type } -> Applicative f => LensLike' f m IxVal

public export
implementation {a : Type} -> Ixed (List a) where
  IxInd = Nat
  IxVal = a
  ix k (Mor h) = Mor (\xs0 => go xs0 k)
    where
      go : List a -> Nat -> f (List a)
      go Nil _           = pure Nil
      go (a :: as) Z     = (:: as) <$> (h a)
      go (a :: as) (S n) = (a ::)  <$> (go as n)

public export
implementation {a : Type} -> Ixed (Maybe a) where
  IxInd = Unit
  IxVal = a
  ix _ (Mor f) = Mor (\g => case g of
                  (Just a) => Just <$> f a
                  Nothing  => pure Nothing
                  )

public export
interface At m where
  AtInd : Type
  AtVal : Type
  -- |
  -- >>> Map.fromList [(1,"world")] ^.at 1
  -- Just "world"
  --
  -- >>> at 1 ?~ "hello" $ Map.empty
  -- fromList [(1,"hello")]
  --
  -- /Note:/ 'Map'-like containers form a reasonable instance, but not 'Array'-like ones, where
  -- you cannot satisfy the 'Lens' laws.
  at : AtInd -> { f : Type -> Type } -> Applicative f => LensLike' f m (Maybe AtVal)

public export
sans : At m => AtInd { m } -> m -> m
sans k m = m |> at k .~ Nothing

public export
implementation {a : Type} -> At (Maybe a) where
  AtInd = Unit
  AtVal = a
  at () (Mor f) = (Mor f)

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


text:
module Libraries.Control.ANSI.SGR

import Data.List

%default total

public export
data Color
  = Black | Red | Green | Yellow | Blue | Magenta | Cyan | White
  | BrightBlack | BrightRed | BrightGreen | BrightYellow | BrightBlue | BrightMagenta | BrightCyan | BrightWhite

Cast Color String where
  cast Black = "0"
  cast Red = "1"
  cast Green = "2"
  cast Yellow = "3"
  cast Blue = "4"
  cast Magenta = "5"
  cast Cyan = "6"
  cast White = "7"
  cast BrightBlack = "8"
  cast BrightRed = "9"
  cast BrightGreen = "10"
  cast BrightYellow = "11"
  cast BrightBlue = "12"
  cast BrightMagenta = "13"
  cast BrightCyan = "14"
  cast BrightWhite = "15"

public export
data Style
  = Bold | Faint | NotBoldOrFaint | Italic
  | SingleUnderline | DoubleUnderline | NoUnderline
  | Striked | NotStriked

Cast Style String where
  cast Bold = "1"
  cast Faint = "2"
  cast NotBoldOrFaint = "22"
  cast Italic = "3"
  cast SingleUnderline = "4"
  cast DoubleUnderline = "21"
  cast NoUnderline = "24"
  cast Striked = "9"
  cast NotStriked = "29"

public export
data Blink = Slow | Rapid | NoBlink

Cast Blink String where
  cast Slow = "5"
  cast Rapid = "6"
  cast NoBlink = "25"

public export
data SGR
  = Reset
  | SetForeground Color
  | SetBackground Color
  | SetStyle Style
  | SetBlink Blink

||| Returns the ANSI escape code equivalent to the list of operations provided.
export
escapeSGR : List SGR -> String
escapeSGR xs = "\x1B[" ++ concat (intersperse ";" (toCode <$> xs)) ++ "m"
  where
    toCode : SGR -> String
    toCode Reset = "0"
    toCode (SetForeground c) = "38;5;" ++ cast c
    toCode (SetBackground c) = "48;5;" ++ cast c
    toCode (SetStyle s) = cast s
    toCode (SetBlink b) = cast b


text:
||| A collection of utlities shared accross the Razors.
|||
||| This consists of:
|||
|||  + some syntactic sugar to make functions detailing renaming,
|||    weakening, and substitution more like those seen in PLFA.
|||
|||  + Some data structures to make working with collections of
|||    dependent types easier.
module Razor.Common

import public Decidable.Equality

import public Data.List.Elem
import public Data.Vect
import public Data.Vect.Elem
import public Data.Fin
import public Data.DPair

%default total

-- A reverse cons operator.
infixr 6 +=

namespace List

  ||| Proof that the given list (`xs`) contains the given element
  ||| (`x`).
  |||
  |||
  public export
  Contains : List a -> a -> Type
  Contains xs x = Elem x xs

  ||| Append `x` to the head of `xs`.
  public export
  (+=) : List a -> a -> List a
  (+=) xs x = x :: xs

namespace Vect

  ||| Append `x` to the head of `xs`.
  public export
  (+=) : (xs : Vect n a) -> (x : a) -> Vect (S n) a
  (+=) xs x = x :: xs

namespace DList

  ||| A list construct for dependent types.
  |||
  ||| @a  The type of the value contained within the list element type.
  ||| @e  The type of the elements within the list
  ||| @vs The List used to contain the different values within the type.
  public export
  data DList : (a : Type)
            -> (e : a -> Type)
            -> (vs : List a)
            -> Type
    where
      Nil  : DList a e Nil
      (::) : forall v
           .  (head : (e v))
           -> (tail : DList a e vs)
                   -> DList a e (v::vs)

  ||| Append `x` to the head of `xs`.
  public export
  (+=) : forall v
       . (xs : DList a e vs)
      -> (x  : e v)
            -> DList a e (v::vs)
  (+=) xs x = x :: xs

  ||| A proof that some element (`x`) is found in the given list (`xs`).
  public export
  data Elem : (a : Type)
           -> (e : a -> Type)
           -> forall i, is
            . (x      : e i)
           -> (xs     : DList a e is)
           -> Type
      where
        ||| The element is at the head of the list.
        Here : Elem a e x (x :: xs)

        ||| The element is found in the tail of the list.
        There : (rest : Elem a e x        xs)
                     -> Elem a e x (x' :: xs)

namespace Index
  public export
  data AtIndex : (idx : Fin n)
              -> (xs  : Vect n type)
              -> (x   : type)
                     -> Type
    where
      Here : AtIndex FZ (x::xs) x

      There : (later : AtIndex     rest      xs  x)
                    -> AtIndex (FS rest) (y::xs) x

  namespace Check
    public export
    elemDiffers : (y = x -> Void)
                -> AtIndex FZ (y :: xs) x
                -> Void
    elemDiffers f Here
      = f Refl

    public export
    elemNotInRest : (AtIndex z xs x -> Void)
                 ->  AtIndex (FS z) (y :: xs) x
                 ->  Void
    elemNotInRest f (There later)
      = f later

    ||| Is the element at the given index?
    |||
    public export
    index : DecEq type
         => (idx : Fin n)
         -> (x   : type)
         -> (xs  : Vect n type)
                -> Dec (AtIndex idx xs x)

    index FZ _ [] impossible
    index (FS y) _ [] impossible

    index FZ x (y :: xs) with (decEq y x)
      index FZ x (x :: xs) | (Yes Refl)
        = Yes Here
      index FZ x (y :: xs) | (No contra)
        = No (elemDiffers contra)

    index (FS z) x (y :: xs) with (Check.index z x xs)
      index (FS z) x (y :: xs) | (Yes prf)
        = Yes (There prf)
      index (FS z) x (y :: xs) | (No contra)
        = No (elemNotInRest contra)

  namespace Find
    public export
    elemNotInRest : (DPair type (AtIndex     x        xs)  -> Void)
                 ->  DPair type (AtIndex (FS x) (y :: xs)) -> Void

    elemNotInRest f (MkDPair i (There later))
      = f (MkDPair i later)

    ||| What is the element at the given index?
    |||
    public export
    index : DecEq type
         => (idx : Fin n)
         -> (xs  : Vect n type)
                -> Dec (DPair type (AtIndex idx xs))
    index FZ (x :: xs)
      = Yes (MkDPair x Here)

    index (FS x) (y :: xs) with (Find.index x xs)
      index (FS x) (y :: xs) | (Yes (MkDPair i idx))
        = Yes (MkDPair i (There idx))
      index (FS x) (y :: xs) | (No contra) = No (elemNotInRest contra)

-- [ EOF ]

max_stars_repo_name: border-patrol/pearly-razors

max_issues_repo_name: border-patrol/pearly-razors

max_forks_repo_name: border-patrol/pearly-razors


text:
module Control.Eff

import public Control.Eff.Choose
import public Control.Eff.Except
import public Control.Eff.Internal
import public Control.Eff.Reader
import public Control.Eff.State
import public Control.Eff.Writer