text:
module Clocks

%default total

-- An Idris implementation of 'A Clocked Denotational Semantics for
-- LUCID-SYNCHRONE in COQ' by S. Boulme & G. Hamon 2001

funPower : (f : (a -> a)) -> (repeats : Nat) -> (start : a) -> a
funPower f Z x = x
funPower f (S k) x = funPower f k (f x)

funPower_commutes : (f : (a -> a)) -> (n : Nat) -> (x : a) -> (f (funPower f n x)) = (funPower f (S n) x)
funPower_commutes f Z x = Refl
funPower_commutes f (S k) x = let ff = funPower_commutes f k (f x) in
                                  rewrite ff in Refl

-- nicked from bmckenna
-- dont think we can have DecEq for streams??
-- use equivalence instead
-- infixl 9 =~=
-- data Equiv : Stream a -> Stream a -> Type where
--   Cons :  (head_prf : a = b) -> Inf (Equiv as bs) -> Equiv (a :: as) (b :: bs)

-- stream_unfold : (DecEq a) => (s : Stream a) -> Equiv s (( head s ) :: ( tail s ))
-- stream_unfold (x :: xs) with (decEq x (head (x :: xs)))
--   stream_unfold (x :: xs) | (Yes prf) = ?stream_unfold_rhs_1_rhs_3
--   stream_unfold (x :: xs) | (No contra) = ?stream_unfold_rhs_1_rhs_4

data Clk = Tick | Tock

data SamplElt : (a : Type) -> Clk -> Type where
  CNone : SamplElt a Tock
  CAny  : a -> SamplElt a Tick
  CFail : SamplElt a Tick

bad_any_fail_prf : (clk : Clk) -> (CAny x = CFail) -> Void
bad_any_fail_prf _ Refl impossible

bad_fail_any_prf : (clk : Clk) -> (CFail = CAny x) -> Void
bad_fail_any_prf _ Refl impossible

bad_any_prf : (cont : (x = y) -> Void) -> (CAny x = CAny y) -> Void
bad_any_prf cont Refl = cont Refl

(DecEq a) => DecEq (SamplElt a clk) where
    decEq CNone CNone = Yes Refl
    decEq CFail CFail = Yes Refl
    decEq (CAny x) (CAny y) = case (decEq x y) of
                Yes prf => Yes (cong prf)
                No cont => No (bad_any_prf cont)
    decEq {clk=Tick} (CAny x) CFail = No (bad_any_fail_prf Tick)
    decEq {clk=Tick} CFail (CAny y) = No (bad_fail_any_prf Tick)

    decEq CNone CFail    impossible
    decEq CFail CNone    impossible
    decEq CNone (CAny y) impossible
    decEq (CAny x) CNone impossible

Clock : Type
Clock = Stream Clk

data SamplStr : (a : Type) -> (c : Clock) -> Type where
  (::) : (SamplElt a (head c)) -> Inf (SamplStr a (tail c)) -> SamplStr a c

-- infixl 9 =~~=
-- data (=~~=) : SamplStr a c -> SamplStr a c -> Type where
--   (:::) : a = b -> Inf (as =~~= bs) -> (SPCons a as =~~= SPCons b bs)

sp_hd : SamplStr a c -> SamplElt a (head c)
sp_hd (x :: _) = x

sp_tl : SamplStr a c -> SamplStr a (tail c)
sp_tl (_ :: xs) = xs

using (c1 : Clock, c2 : Clock)
  prf_samplElt : (a : Type ) -> (c1 : Clock) -> (c2 : Clock) ->
                 (head_prf : head c1 = head c2) ->
                 (SamplElt a (head c1) = SamplElt a (head c2))
  prf_samplElt a c1 c2 head_prf = rewrite head_prf in Refl

  head_coerce : (head_prf : head c1 = head c2) ->
                (x : SamplElt a (head c1)) -> SamplElt a (head c2)
  head_coerce {a} {c1} {c2} head_prf x = let prf = prf_samplElt a c1 c2 head_prf in
                                         rewrite sym $ prf in x

  clock_coerce : (prf : c1 = c2) -> SamplStr a c1 -> SamplStr a c2
  clock_coerce Refl x = x

  sp_eq_clock_coerce : (prf : (c1 = c2)) -> (s : SamplStr a c1) -> (s = (clock_coerce prf s))
  sp_eq_clock_coerce Refl s = Refl

-- DecEq (SamplElt a (head c)) => DecEq (SamplStr a c) where
--     decEq (x::xs) (y::ys) with (decEq x y)
--       decEq (x::xs) (y::ys) | Yes prf = ?DecEq_rhs_1_rhs_1
--       decEq (x::xs) (y::ys) | No cong = No ?DecEq_rhs_1_rhs_3

-- -- doesnt work becasue Bool is different but only one clk
-- -- notFails : a -> Vect 2 (SamplElt a clk)
-- -- notFails x = [CNone, CAny x]

-- -- is_not_fail : (e : SamplElt a clk) -> Bool
-- -- is_not_fail CNone = True
-- -- is_not_fail (CAny x) = True
-- -- is_not_fail CFail = False

-- -- data WellFormed : (s : SamplStr a c) -> Type where
-- --   IsNotFail : (prf : True = is_not_fail (sp_hd s)) -> WellFormed (sp_tl s) -> WellFormed s

data WellFormed : (s : SamplStr a c) -> Type where
  HeadIsAny : ((sp_hd s) = (CAny a)) -> WellFormed (sp_tl s) -> WellFormed s
  HeadIsNone : ((sp_hd s) = CNone) -> WellFormed (sp_tl s) -> WellFormed s

elt_const : a -> (clk_value : Clk) -> SamplElt a clk_value
elt_const x clk_value = case clk_value of
  Tick   => CAny x
  Tock => CNone

sp_const : a -> (clk : Clock) -> SamplStr a clk
sp_const x (c :: cs) = (elt_const x c) :: (sp_const x cs)

-- sp_const_wellformed : (x : a) -> (clk : Clock) -> WellFormed (sp_const a clk)
-- sp_const_wellformed x (Cons c cs) = let rest = (sp_const_wellformed x cs) in
--                                     case elt_const x c of
--                                     CAny x' => ?head_any_prf rest
--                                     CNone  =>  ?head_non_prf
--                                     CFail => ?head_fail_prf

elt_extend : (SamplElt (a -> b) clk_value) -> (SamplElt a clk_value) -> (SamplElt b clk_value)
elt_extend CNone    _        = CNone
elt_extend (CAny f) (CAny x) = CAny (f x)
elt_extend _        CFail    = CFail
elt_extend CFail    _        = CFail

sp_extend : (SamplStr (a -> b) clk) -> (SamplStr a clk) -> (SamplStr b clk)
sp_extend (f :: fs) (x :: xs) = (elt_extend f x) :: (sp_extend fs xs)

-- sp_extend_wellformed : (fs : SamplStr (a->b) clk) ->
--                        (s : SamplStr a clk) ->
--                        (WellFormed fs) ->
--                        (WellFormed s) ->
--                        (WellFormed (sp_extend fs s))
-- sp_extend_wellformed fs s wf_fs wf_xs = ?sp_extend_wellformed_rhs

-- sp_extend_const_prf : (f : a -> b) -> (x : a) -> (sp_extend (sp_const f clk) (sp_const x clk)) = sp_const (f x) clk
-- sp_extend_const_prf f x = ?sp_extend_const_prf_rhs

-- sp_extend_id_prf : (x : SamplStr a clk) -> (sp_extend (sp_const id clk) x) = x
-- sp_extend_id_prf x = ?sp_extend_id_prf_rhs

-- sp_extend_comp_prf : (f : a -> b) -> (g : b -> c) -> (x : SamplStr a clk) ->
--                      (sp_extend (sp_const g clk) (sp_extend (sp_const f clk) x)) = (sp_extend (sp_const (g . f) clk) x)
-- sp_extend_comp_prf f g (SPCons x xs) = ?sp_extend_comp_prf_rhs_1

flip_bool : Bool -> Bool
flip_bool False = True
flip_bool True = False

bool_to_clk : Bool -> Clk
bool_to_clk True = Tick
bool_to_clk False = Tock

clk_to_bool : Clk -> Bool
clk_to_bool Tick = True
clk_to_bool Tock = False

sp_not :(SamplStr Bool clk) -> (SamplStr Bool clk)
sp_not {clk} = sp_extend (sp_const flip_bool clk)

if_then_else : Bool -> a -> a -> a
if_then_else cond x y = if cond then x else y

sp_if : SamplStr Bool clk -> SamplStr a clk -> SamplStr a clk -> SamplStr a clk
sp_if {clk} lc x y = sp_extend (sp_extend (sp_extend (sp_const if_then_else clk) lc) x) y

elt_on : SamplElt Bool clk_value -> Clk
elt_on CNone = Tock
elt_on (CAny x) = bool_to_clk x
elt_on CFail = Tick

sp_on : SamplStr Bool clk -> Clock
sp_on (x :: xs) = (elt_on x) :: (sp_on xs)

head_sp_on_prf : (head (sp_on s)) = (elt_on (sp_hd s))
head_sp_on_prf = ?head_sp_on_prf_rhs1

elt_when : (o : SamplElt Bool clk_value) ->
           SamplElt a clk_value ->
           SamplElt a (elt_on o)
elt_when CNone        e = CNone
elt_when (CAny False) e = CNone
elt_when (CAny True)  e = e
elt_when CFail        e = CFail

sp_when : (lc : SamplStr Bool clk) -> SamplStr a clk -> SamplStr a (sp_on lc)
sp_when (c :: cs) (x :: xs) = (elt_when c x) :: (sp_when cs xs)

-- flip_bool_prf : (elt_on (elt_extend (elt_const flip_bool Tick) (CAny False))) = Tick

elt_merge : (o : SamplElt Bool clk_value) ->
            (SamplElt a (elt_on o)) ->
            (SamplElt a (elt_on (elt_extend (elt_const Clocks.flip_bool clk_value) o))) ->
            SamplElt a clk_value
elt_merge CNone        x y = CNone
elt_merge (CAny False) x y = y
elt_merge (CAny True)  x y = x -- elt_on (CAny True)
elt_merge CFail        x y = CFail

sp_merge : (lc : SamplStr Bool clk) ->
           SamplStr a (sp_on lc) ->
           SamplStr a (sp_on (sp_not lc)) ->
           SamplStr a clk
sp_merge (c :: cs) (x :: xs) (y :: ys) = (elt_merge c x y) :: (sp_merge cs xs ?ysthings)
             -- Type mismatch between
             --         SamplElt a
             --                  (head (sp_on (sp_extend (sp_const flip_bool clk)
             --                                          (c :: cs)))) (Type of y)
             -- and
             --         SamplElt a
             --                  (elt_on (elt_extend (elt_const flip_bool (head clk))
             --                                      c)) (Expected type)

--   (c :: cs) (x :: xs) (y :: ys) = (elt_merge c x y) :: (sp_merge cs xs ys)

-- sp_if_equiv_prf : (lc : SamplStr Bool clk) -> (x : SamplStr a clk) -> (y : SamplStr a clk) ->
--                   (WellFormed x) ->
--                   (WellFormed y) ->
--                   (sp_if lc x y) = (sp_merge lc (sp_when lc x) (sp_when (sp_not lc) y))

-- chooses xs until clock ticks, then chooses ys
sp_arrow : SamplStr a clk -> SamplStr a clk -> SamplStr a clk
sp_arrow {clk = (c :: cs)} (x :: xs) (y :: ys)
  = x :: (if (clk_to_bool c) then ys else (sp_arrow xs ys))

-- delay by one Clk element - if the clock ticks then initialised with init
-- else initialise with none and recurse with rest of x :: xs
sp_delay : (SamplStr a clk) -> (SamplElt a Tick) -> SamplStr a clk
sp_delay {clk = (Tick :: cs)} (x :: xs) init = init  :: (sp_delay xs x)
sp_delay {clk = (Tock :: cs)} (x :: xs) init = CNone :: (sp_delay xs init)

sp_pre : SamplStr a clk -> SamplStr a clk
sp_pre s = sp_delay s CFail

sp_fby : SamplStr a clk -> SamplStr a clk -> SamplStr a clk
sp_fby x y = sp_arrow x (sp_pre y)

-- arrow_equiv_prf : (x : SamplStr a clk) -> (y : SamplStr a clk) ->
--                   WellFormed x -> WellFormed y ->
--                   (sp_arrow x y) = (sp_if (sp_fby (sp_const True clk) (sp_const False clk)) x y)

max_stars_repo_name: wyn/incremental

max_issues_repo_name: wyn/incremental

max_forks_repo_name: wyn/incremental


text:
module Numbers

import DataTypes
import Control.ST
import Control.ST.Exception
import Data.Complex
import Ratio
import Util
import Data.Fuel

%access public export

numToInt : LispVal -> ThrowsError LispVal
numToInt a@(LispInteger _) = pure a
numToInt (LispRational a) =
  if denominator a == 1
    then pure $ LispInteger (numerator a)
    else Left $ Default "Could not convert rational to integer"
numToInt (LispFloat a) =
  if a == cast (round a) -- TODO
    then pure $ LispInteger (round a)
    else Left $ Default "Could not convert float to integer"
numToInt (LispComplex a) =
  let rp = realPart a
  in if imagPart a == 0 && rp == cast (round rp)
       then pure $ LispInteger (round rp)
       else Left $ Default "Could not convert complex to integer"
numToInt _ = Left $ Default "Could not convert non-number to integer"

numCast : PrimitiveLispFunc
numCast [a@(LispInteger _), b@(LispInteger _)] = pure $ LispList [a, b]
numCast [a@(LispRational _), b@(LispRational _)] = pure $ LispList [a, b]
numCast [a@(LispFloat _), b@(LispFloat _)] = pure $ LispList [a, b]
numCast [a@(LispComplex _), b@(LispComplex _)] = pure $ LispList [a, b]
-- Integer
numCast [(LispInteger a), b@(LispRational _)] =
  pure $ LispList [LispRational (a .% 1), b]
numCast [(LispInteger a), b@(LispFloat _)] = pure $ LispList [LispFloat (fromInteger a), b]
numCast [(LispInteger a), b@(LispComplex _)] = pure $ LispList [LispComplex (fromInteger a :+ 0), b]
-- Rational
numCast [a@(LispRational _), (LispInteger b)] =
  pure $ LispList [a, LispRational (b .% 1)]
numCast [(LispRational a), b@(LispFloat _)] =
  case rationalCast a of
    Just flt => pure $ LispList [LispFloat flt, b]
    Nothing => Left $ Default "Unexpected error in numCast"
numCast [(LispRational a), b@(LispComplex _)] =
  case rationalCast a of
    Just flt => pure $ LispList [LispComplex (flt :+ 0), b]
    Nothing => Left $ Default "Unexpected error in numCast"
-- Float
numCast [a@(LispFloat _), (LispRational b)] =
  case rationalCast b of
    Just flt => pure $ LispList [a, LispFloat flt]
    Nothing => Left $ Default "Unexpected error in numCast"
numCast [a@(LispFloat _), (LispInteger b)] = pure $ LispList [a, LispFloat (fromInteger b)]
numCast [(LispFloat a), b@(LispComplex _)] = pure $ LispList [LispComplex (a :+ 0), b]
-- Complex
numCast [a@(LispComplex _), (LispRational b)] =
  case rationalCast b of
    Just flt => pure $ LispList [a, LispComplex (flt :+ 0)]
    Nothing => Left $ Default "Unexpected error in numCast"
numCast [a@(LispComplex _), (LispFloat b)] = pure $ LispList [a, LispComplex (b :+ 0)]
numCast [a@(LispComplex _), (LispInteger b)] = pure $ LispList [a, LispComplex (fromInteger b :+ 0)]
numCast [a, b] =
  case a of
    LispInteger _ => dothrow b
    LispFloat _ => dothrow b
    LispRational _ => dothrow b
    LispComplex _ => dothrow b
    _ => dothrow a
  where
    dothrow : LispVal -> ThrowsError LispVal
    dothrow num = Left $ TypeMismatch "Integer" num
numCast _ = Left $ Default "Unexpected error in numCast"

variadicNumberOp : LispVal -> (LispVal -> ThrowsError LispVal) -> PrimitiveLispFunc
variadicNumberOp ident op xs = helper xs ident
    where
        helper : List LispVal -> LispVal -> ThrowsError LispVal
        helper [] acc = pure acc
        helper (x::xs) acc =
            do c <- numCast [acc, x]
               d <- op c
               helper xs d

rationalBinaryOpHelper : (Rational -> Rational -> Maybe Rational) -> Rational -> Rational -> String -> ThrowsError LispVal
rationalBinaryOpHelper op a b opStr =
  case op a b of
    Just rat => pure $ LispRational rat
    Nothing => Left $ Default $ "Unexpected error in " ++ opStr

numAdd : PrimitiveLispFunc
numAdd = variadicNumberOp (LispInteger 0) doAdd
    where
        doAdd : LispVal -> ThrowsError LispVal
        doAdd (LispList [LispInteger c, LispInteger d]) = pure $ LispInteger (c + d)
        doAdd (LispList [LispRational c, LispRational d]) =
          rationalBinaryOpHelper rationalAdd c d "+"
        doAdd (LispList [LispFloat c, LispFloat d]) = pure $ LispFloat (c + d)
        doAdd (LispList [LispComplex c, LispComplex d]) = pure $ LispComplex (c + d)
        doAdd _ = Left $ Default "Unexpected error in +"

doSub : LispVal -> ThrowsError LispVal
doSub (LispList [LispInteger c, LispInteger d]) = pure $ LispInteger (c - d)
doSub (LispList [LispRational c, LispRational d]) =
  rationalBinaryOpHelper rationalSub c d "-"
doSub (LispList [LispFloat c, LispFloat d]) = pure $ LispFloat (c - d)
doSub (LispList [LispComplex c, LispComplex d]) = pure $ LispComplex (c - d)
doSub _ = Left $ Default "Unexpected error in -"

numSub : PrimitiveLispFunc
numSub [] = Left $ NumArgs (Min 1) 0 []
numSub [x] = variadicNumberOp (LispInteger 0) doSub [x]
numSub (x::xs) = variadicNumberOp x doSub xs

numMul : PrimitiveLispFunc
numMul [] = pure $ LispInteger 1
numMul xs = variadicNumberOp (LispInteger 1) doMul xs
  where
    doMul : LispVal -> ThrowsError LispVal
    doMul (LispList [LispInteger c, LispInteger d]) = pure $ LispInteger (c * d)
    doMul (LispList [LispRational c, LispRational d]) =
      rationalBinaryOpHelper rationalMul c d "*"
    doMul (LispList [LispFloat c, LispFloat d]) = pure $ LispFloat (c * d)
    doMul (LispList [LispComplex c, LispComplex d]) = pure $ LispComplex (c * d)
    doMul _ = Left $ Default "Unexpected error in *"

numDiv : PrimitiveLispFunc
numDiv [] = Left $ NumArgs (Min 1) 0 []
numDiv (x::xs) = variadicNumberOp x doDiv xs -- TODO: Zero division error
  where
    doDiv : LispVal -> ThrowsError LispVal
    doDiv (LispList [LispFloat c, LispFloat d]) =
      if d == 0.0
        then Left $ Default "Zero division error"
        else pure $ LispFloat (c / d)
    doDiv (LispList [LispComplex c, LispComplex d]) =
      if d == 0
        then Left $ Default "Zero division error"
        else pure $ LispComplex (c / d)
    doDiv (LispList [LispInteger c, LispInteger d]) =
      case (c :% d) of
        Just rat => pure $ LispRational rat
        Nothing => Left $ Default "Zero division error"
    doDiv (LispList [LispRational c, LispRational d]) =
      rationalBinaryOpHelper rationalDiv c d "/"
    doDiv _ = Left $ Default "Unexpected error in /"

numMod : PrimitiveLispFunc
numMod [a, b] =
    do
        c <- numCast $ [a, b]
        doMod c
    where
    modHelper : Integer -> Integer -> Integer
    modHelper n d =
      let k = cast (floor ((cast n) / (cast d)))
      in n - k * d
    doMod : LispVal -> ThrowsError LispVal
    doMod (LispList [LispInteger c, LispInteger d]) = pure $ LispInteger (modHelper c d)
    doMod (LispList [c@(LispRational _), d@(LispRational _)]) = do
      LispInteger c' <- numToInt c
      LispInteger d' <- numToInt d
      pure $ LispRational ((modHelper c' d') .% 1)
    doMod (LispList [c@(LispFloat _), d@(LispFloat _)]) = do
      LispInteger c' <- numToInt c
      LispInteger d' <- numToInt d
      pure $ LispFloat (fromInteger (modHelper c' d'))
    doMod (LispList [c@(LispComplex _), d@(LispComplex _)]) = do
      LispInteger c' <- numToInt c
      LispInteger d' <- numToInt d
      pure $ LispComplex (fromInteger (modHelper c' d') :+ 0)
    doMod _ = Left $ Default "Unexpected error in modulo"
numMod a = Left $ NumArgs (MinMax 2 2) (cast $ length a) a

numRem : PrimitiveLispFunc
numRem [a, b] =
    do
        c <- numCast $ [a, b]
        doRem c
    where
    doRem : LispVal -> ThrowsError LispVal
    doRem (LispList [LispInteger c, LispInteger d]) = pure $ LispInteger (c `mod` d) -- TODO `rem`?
    doRem (LispList [c@(LispRational _), d@(LispRational _)]) = do
      LispInteger c' <- numToInt c
      LispInteger d' <- numToInt d
      pure $ LispRational ((c' `mod` d') .% 1)
    doRem (LispList [c@(LispFloat _), d@(LispFloat _)]) =
        do
            LispInteger c' <- numToInt c
            LispInteger d' <- numToInt d
            pure $ LispFloat (fromInteger (c' `mod` d')) -- TODO `rem`?
    doRem (LispList [c@(LispComplex _), d@(LispComplex _)]) =
        do
            LispInteger c' <- numToInt c
            LispInteger d' <- numToInt d
            pure $ LispComplex (fromInteger (c' `mod` d') :+ 0) -- TODO `rem`?
    doRem _ = Left $ Default "Unexpected error in remainder"
numRem a = Left $ NumArgs (MinMax 2 2) (cast $ length a) a

isInteger : PrimitiveLispFunc
isInteger [LispInteger _] = pure $ LispBool True
isInteger [_] = pure $ LispBool False
isInteger a = Left $ NumArgs (MinMax 1 1) (cast $ length a) a

isRational : PrimitiveLispFunc
isRational [LispRational _] = pure $ LispBool True
isRational a = isInteger a

isReal : PrimitiveLispFunc
isReal [LispFloat _] = pure $ LispBool True
isReal a = isRational a

isComplex : PrimitiveLispFunc
isComplex [LispComplex _] = pure $ LispBool True
isComplex a = isReal a

isNumber : PrimitiveLispFunc
isNumber = isComplex

numBoolBinop :
     String
  -> (LispVal -> LispVal -> ThrowsError LispVal)
  -> LispVal
  -> List LispVal
  -> ThrowsError LispVal
numBoolBinop name' op b (c::d) = do
  LispList [b', c'] <- numCast [b, c]
  result <- op b' c'
  case result of
    LispBool True => numBoolBinop name' op c' d
    LispBool False => pure $ LispBool False
    _ => Left $ Default $ "Unexpected error in " ++ name'
numBoolBinop _ _ _ _ = pure $ LispBool True

numBoolBinopEq : PrimitiveLispFunc
numBoolBinopEq [] = Left $ NumArgs (Min 1) 0 []
numBoolBinopEq (x::xs) = numBoolBinop "=" fn x xs
  where
    fn : LispVal -> LispVal -> ThrowsError LispVal
    fn (LispInteger c) (LispInteger d) = pure $ LispBool (c == d)
    fn (LispRational c) (LispRational d) = pure $ LispBool (c == d)
    fn (LispFloat c) (LispFloat d) = pure $ LispBool (c == d)
    fn (LispComplex c) (LispComplex d) = pure $ LispBool (c == d)
    fn _ _ = Left $ Default "Unexpected error in ="

numBoolBinopNeq : PrimitiveLispFunc
numBoolBinopNeq [] = Left $ NumArgs (Min 1) 0 []
numBoolBinopNeq (x::xs) = numBoolBinop "/=" fn x xs
  where
    fn : LispVal -> LispVal -> ThrowsError LispVal
    fn (LispInteger c) (LispInteger d) = pure $ LispBool (c /= d)
    fn (LispRational c) (LispRational d) = pure $ LispBool (c /= d)
    fn (LispFloat c) (LispFloat d) = pure $ LispBool (c /= d)
    fn (LispComplex c) (LispComplex d) = pure $ LispBool (c /= d)
    fn _ _ = Left $ Default "Unexpected error in /="

numBoolBinopLt : PrimitiveLispFunc
numBoolBinopLt [] = Left $ NumArgs (Min 1) 0 []
numBoolBinopLt (x::xs) = numBoolBinop "<" fn x xs
  where
    fn : LispVal -> LispVal -> ThrowsError LispVal
    fn (LispInteger c) (LispInteger d) = pure $ LispBool (c < d)
    fn (LispRational c) (LispRational d) = pure $ LispBool (c < d)
    fn (LispFloat c) (LispFloat d) = pure $ LispBool (c < d)
    fn (LispComplex _) (LispComplex _) =
      Left $ Default "< not defined for complex numbers"
    fn _ _ = Left $ Default "Unexpected error in <"

numBoolBinopLte : PrimitiveLispFunc
numBoolBinopLte [] = Left $ NumArgs (Min 1) 0 []
numBoolBinopLte (x::xs) = numBoolBinop "<=" fn x xs
  where
    fn : LispVal -> LispVal -> ThrowsError LispVal
    fn (LispInteger c) (LispInteger d) = pure $ LispBool (c <= d)
    fn (LispRational c) (LispRational d) = pure $ LispBool (c <= d)
    fn (LispFloat c) (LispFloat d) = pure $ LispBool (c <= d)
    fn (LispComplex _) (LispComplex _) =
      Left $ Default "<= not defined for complex numbers"
    fn _ _ = Left $ Default "Unexpected error in <="

numBoolBinopGt : PrimitiveLispFunc
numBoolBinopGt [] = Left $ NumArgs (Min 1) 0 []
numBoolBinopGt
 (x::xs) = numBoolBinop ">" fn x xs
  where
    fn : LispVal -> LispVal -> ThrowsError LispVal
    fn (LispInteger c) (LispInteger d) = pure $ LispBool (c > d)
    fn (LispRational c) (LispRational d) = pure $ LispBool (c > d)
    fn (LispFloat c) (LispFloat d) = pure $ LispBool (c > d)
    fn (LispComplex _) (LispComplex _) =
      Left $ Default "> not defined for complex numbers"
    fn _ _ = Left $ Default "Unexpected error in >"

numBoolBinopGte : PrimitiveLispFunc
numBoolBinopGte [] = Left $ NumArgs (Min 1) 0 []
numBoolBinopGte (x::xs) = numBoolBinop ">=" fn x xs
  where
    fn : LispVal -> LispVal -> ThrowsError LispVal
    fn (LispInteger c) (LispInteger d) = pure $ LispBool (c >= d)
    fn (LispRational c) (LispRational d) = pure $ LispBool (c >= d)
    fn (LispFloat c) (LispFloat d) = pure $ LispBool (c >= d)
    fn (LispComplex _) (LispComplex _) =
      Left $ Default ">= not defined for complex numbers"
    fn _ _ = Left $ Default "Unexpected error in >="

numQuotient : PrimitiveLispFunc
numQuotient args =
  if length args /= 2
    then Left $ NumArgs (MinMax 2 2) (cast $ length args) args
    else do
      nums <- numCast args
      case nums of
        LispList [LispInteger a, LispInteger b] => pure $ LispInteger (a `div` b) -- TODO: Should be `quot`
        _ => Left $ Default "Unexpected error in <=" -- TODO better errors

unaryTrig : (Double -> Double) -> (Double -> Double -> Complex Double) -> PrimitiveLispFunc
unaryTrig op complexOp args =
  if length args /= 1
    then Left $ NumArgs (MinMax 1 1) (cast $ length args) args
    else case args of
           [LispInteger a] => pure $ LispFloat (op $ fromInteger a)
           [LispRational a] =>
              case rationalCast a of
                Just flt => pure $ LispFloat (op flt)
                Nothing => Left $ Default "Unexpected error" -- TODO: Better error
           [LispFloat a] => pure $ LispFloat (op a)
           [LispComplex a] => pure $ LispComplex $ complexOp (realPart a) (imagPart a)
           _ => Left $ Default "Numerical input expected"

numSine : PrimitiveLispFunc
numSine = unaryTrig sin (\r, i => ((sin r) * (cosh i)) :+ ((cos r) * (sinh i)))

numCos : PrimitiveLispFunc
numCos =
  unaryTrig cos (\r, i => ((cos r) * (cosh i)) :+ (-1 * ((sin r) * (sinh i))))

numToString : PrimitiveLispFunc
numToString [n] =
  do num <- isNumber [n]
     case num of
        LispBool True => pure $ LispString $ show n
        LispBool False => Left $ TypeMismatch "number?" n
        _ => Left $ Default "Unexpected error"

numPrimitives : List (String, PrimitiveLispFunc)
numPrimitives =
    [ ("+", numAdd)
    , ("-", numSub)
    , ("*", numMul)
    , ("/", numDiv)
    , ("modulo", numMod)
    , ("number?", isNumber)
    , ("complex?", isComplex)
    , ("real?", isReal)
    , ("rational?", isRational)
    , ("integer?", isInteger)
    , ("=", numBoolBinopEq)
    , ("/=", numBoolBinopNeq)
    , (">", numBoolBinopGt)
    , ("<", numBoolBinopLt)
    , (">=", numBoolBinopGte)
    , ("<=", numBoolBinopLte)
    , ("quotient", numQuotient)
    , ("remainder", numRem)
    , ("sin", numSine)
    , ("cos", numCos)
    , ("number->string", numToString)
    ]

ext: idr

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module Network.HTTP.Header

import Generics.Derive
import Utils.Num
import Data.Nat
import Data.Either
import Control.Monad.Error.Either
import Control.Monad.Trans
import Network.HTTP.URL
import Network.HTTP.Cookie
import Utils.String

%language ElabReflection

public export
data Header
  = Host
  | ContentType
  | Accept
  | Cookie
  | SetCookie
  | ContentLength
  | Connection
  | TransferEncoding
  | ContentEncoding
  | Location
  | Unknown String

%runElab derive "Header" [Generic, Meta, Eq, DecEq, Ord, Show]

public export
data ConnectionAction : Type where
  KeepAlive : ConnectionAction
  Close : ConnectionAction

public export
data TransferEncodingScheme : Type where
  Chunked : TransferEncodingScheme
  Identity : TransferEncodingScheme

public export
data ContentEncodingScheme : Type where
  GZip : ContentEncodingScheme
  Deflate : ContentEncodingScheme

%runElab derive "ConnectionAction" [Generic, Meta, Eq, DecEq, Ord, Show]
%runElab derive "TransferEncodingScheme" [Generic, Meta, Eq, DecEq, Ord, Show]
%runElab derive "ContentEncodingScheme" [Generic, Meta, Eq, DecEq, Ord, Show]

public export
header_value_type : Header -> Type
header_value_type ContentLength = Integer
header_value_type Cookie = List (String, String)
header_value_type Host = Hostname
header_value_type Connection = ConnectionAction
header_value_type TransferEncoding = List1 TransferEncodingScheme
header_value_type ContentEncoding = List1 ContentEncodingScheme
header_value_type SetCookie = Cookie
header_value_type _ = String

export
header_key_name : Header -> String
header_key_name ContentType = "Content-Type"
header_key_name ContentLength = "Content-Length"
header_key_name TransferEncoding = "Transfer-Encoding"
header_key_name ContentEncoding = "Content-Encoding"
header_key_name SetCookie = "Set-Cookie"
header_key_name (Unknown x) = x
header_key_name x = show x

public export
key_name_to_header : String -> Header
key_name_to_header x =
  case toLower x of
    "host" => Host
    "content-type" => ContentType
    "accept" => Accept
    "cookie" => Cookie
    "content-length" => ContentLength
    "connection" => Connection
    "transfer-encoding" => TransferEncoding
    "content-encoding" => ContentEncoding
    "set-cookie" => SetCookie
    x => Unknown x

export
FromString Header where
  fromString = key_name_to_header

export
header_parse_value : (header : Header) -> (String -> Maybe (header_value_type header))
header_parse_value Host = getRight . parse_hostname
header_parse_value ContentType = Just
header_parse_value Accept = Just
header_parse_value Location = Just
header_parse_value ContentLength = stringToNat' 10
header_parse_value (Unknown x) = Just
header_parse_value Cookie = Just . map (splitBy '=' . ltrim) . forget . split (';' ==)
header_parse_value Connection = (\case "keep-alive" => Just KeepAlive; "close" => Just Close; _ => Nothing) . toLower . trim
header_parse_value SetCookie = deserialize_cookie
header_parse_value TransferEncoding = traverse parse_transfer_encoding . split (',' ==) where
  parse_transfer_encoding : String -> Maybe TransferEncodingScheme
  parse_transfer_encoding x =
    case toLower $ trim x of
      "chunked" => Just Chunked
      "identity" => Just Identity
      _ => Nothing
header_parse_value ContentEncoding = traverse parse_content_encoding . split (',' ==) where
  parse_content_encoding : String -> Maybe ContentEncodingScheme
  parse_content_encoding x =
    case toLower $ trim x of
      "gzip" => Just GZip
      "deflate" => Just Deflate
      _ => Nothing

export
header_write_value : (header : Header) -> (header_value_type header -> String)
header_write_value Host = hostname_string
header_write_value ContentType = id
header_write_value Accept = id
header_write_value Location = id
header_write_value Cookie = join "; " . map (\(a,b) => "\{a}=\{b}")
header_write_value ContentLength = show
header_write_value (Unknown x) = id
header_write_value Connection = \case KeepAlive => "keep-alive"; Close => "close"
header_write_value SetCookie = serialize_cookie
header_write_value TransferEncoding = join ", " . map (toLower . show)
header_write_value ContentEncoding = join ", " . map (toLower . show)

export
Show (DPair Header $ \h => header_value_type h) where
  show (header ** value) = (header_key_name header) <+> ": " <+> (header_write_value header value)

public export
Headers : Type
Headers = List (DPair Header $ \h => header_value_type h)

export
eq_ignore_case : String -> String -> Bool
eq_ignore_case a b = toUpper a == toUpper b

export
lookup_header : List (String, String) -> (header : Header) -> Maybe (header_value_type header)
lookup_header headers header = do
  raw_value <- lookupBy eq_ignore_case (header_key_name header) headers
  header_parse_value header raw_value

export
lookup_headers : List (String, String) -> (header : Header) -> List (header_value_type header)
lookup_headers headers header = mapMaybe go headers where
  go : (String, String) -> Maybe (header_value_type header)
  go (k, v) = do
    guard (eq_ignore_case k (header_key_name header))
    header_parse_value header v


text:
module Minecraft.Base.PreClassic.GrassBlock.Item.Export

import public Minecraft.Core.Entity.Pickup.Export
import public Minecraft.Base.PreClassic.GrassBlock.Block
import public Minecraft.Base.PreClassic.GrassBlock.Item
import public Minecraft.Base.PreClassic.GrassBlock.ItemEntity

%default total

[grassBlockItem']
Item GrassBlock.Item where
  id = "minecraft:grass_block"
  stackable = Just 64
  givenName = \x => x.base.givenName
  proj = \x => new GrassBlock.ItemEntity GrassBlock.MkItemEntity

[putGrassBlock']
Put GrassBlock.Item where
  putItem self = new GrassBlock.Block GrassBlock.MkBlock

[grassBlockVtbl']
Vtbl GrassBlock.Item where
  vtable (Item GrassBlock.Item) = Just grassBlockItem
  vtable (Put  GrassBlock.Item) = Just putGrassBlock
  vtable _ = Nothing

grassBlockItem = grassBlockItem'
putGrassBlock  = putGrassBlock'
grassBlockVtbl = grassBlockVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Main

import Data.String

import Data.Array

main : IO ()
main = do
    (cmd::args) <- getArgs
    arr <- fromList $ map unpack args
    printLn (length arr)
    main' arr
  where main' : IOArray (List Char) -> IO ()
        main' arr = do
          putStr "> "
          line <- getLine
          Just ix <- pure $ parsePositive {a = Int} line | pure ()
          True <- pure $ ix < length arr | pure ()
          printLn !(index ix arr)
          main' arr

max_stars_repo_name: idris-hackers/idris-array

max_issues_repo_name: idris-hackers/idris-array

max_forks_repo_name: idris-hackers/idris-array


text:
||| Hacky and rudimentary hint database for Idris using elaborator reflection.
||| You can now write tactics that does `getHints`
||| and try to prove the goal with the lemmas there.
module Hezarfen.Hint
import Language.Reflection.Utils
%language ElabReflection
%access public export

||| The hint to pass the machine generated names. Note that the word hint here
||| is used literally, not in the theorem prover sense.
mnString : String
mnString = "hint"

||| The number from which we can creating machine generated variables.
startNumber : Int
startNumber = 0

||| Create a metavariable name that will only be used in compile time.
hintName : Int -> TTName
hintName i = NS (SN (MetaN (UN mnString) (MN i mnString))) ["Hint", "Hezarfen"]

||| Learn the number of the last hint, if it exists at all.
learnLastHint : Elab (Maybe Int)
learnLastHint = up startNumber
  where up : Int -> Elab (Maybe Int)
        up i = (do lookupTyExact (hintName i) ; up (i + 1))
          <|> pure (if i == startNumber then Nothing else Just (i - 1))

||| Adds the given name to the hint database.
newHint : TTName -> Elab ()
newHint n = do
  let new = hintName (fromMaybe startNumber ((+ 1) <$> !learnLastHint))
  declareType (Declare new [] (Var `{TTName}))
  defineFunction (DefineFun new [MkFunClause (Var new) (quote n)])

reifyString : TT -> Elab String
reifyString (TConst (Str s)) = pure s
reifyString t = fail [ TextPart "Failed to reify", TermPart t
                     , TextPart "as a" , NamePart `{{String}}]

reifyInt : TT -> Elab Int
reifyInt (TConst (I i)) = pure i
reifyInt t = fail [ TextPart "Failed to reify", TermPart t
                  , TextPart "as an" , NamePart `{{Int}}]

reifyList : (TT -> Elab a) -> TT -> Elab (List a)
reifyList f `(Prelude.List.Nil {elem=~a}) = pure []
reifyList f `(Prelude.List.(::) {elem=~a} ~x ~xs) =
  (::) <$> f x <*> reifyList f xs
reifyList f t = fail [ TextPart "Failed to reify", TermPart t
                     , TextPart "as a" , NamePart `{List}]

reifyTTName : TT -> Elab TTName
reifyTTName `(UN ~x) = UN <$> reifyString x
reifyTTName `(NS ~n ~xs) = NS <$> reifyTTName n <*> reifyList reifyString xs
reifyTTName `(MN ~i ~s) = MN <$> reifyInt i <*> reifyString s
reifyTTName t = fail [ TextPart "Failed to reify", TermPart t
                     , TextPart "as a", NamePart `{TTName}]

reifyHint : Int -> Elab TTName
reifyHint i = do
    DefineFun _ [MkFunClause _ t] <- lookupFunDefnExact (hintName i)
    reifyTTName t

||| The `Elab` action to get the names of all the hints.
getHints : Elab (List TTName)
getHints = maybe (pure []) go !learnLastHint
  where go : Int -> Elab (List TTName)
        go i = if i < startNumber then pure []
                                  else (::) <$> reifyHint i <*> go (i - 1)

-- Defining Coq-style syntax for hints.
decl syntax "hint" {n} = %runElab (newHint `{n})

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module Main

h : Bool -> Nat
h False = r1 where
  r : Nat
  r = S Z
  r1 : Nat
  r1 = r
h True = r2 where
  r : Nat
  r = Z
  r2 : Nat
  r2 = r

main : IO ()
main = do printLn (h True); printLn (h False)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Adder

AdderType : (numargs : Nat) -> Type -> Type
AdderType Z numType = numType
AdderType (S k) numType = (next : numType) -> AdderType k numType

adder : Num num => (numargs : Nat) -> (acc : num) -> AdderType numargs num
adder Z acc = acc
adder (S k) acc = \i => adder k (i + acc)

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
module Language.Elab.Deriving

import Language.Reflection

import Language.Elab.Deriving.Eq
-- import Language.Elab.Deriving.Ord
import Language.Elab.Deriving.Show

%language ElabReflection

-- the handy regex for eliminating FC from tests: \(MkFC.+?\)\)\s
-- another form: \(MkFC \"\(interactive\)\" \([\s\S]*?\) \([\s\S]*?\)\)

-- In Newtype the method being used is to create the implementation record only,
-- as opposed to Show and Eq where we created the functions in the module scope
-- and then refereed to them in the record. The method of this module is likely
-- the better way to go to avoid namespace pollution. But worse for inspecting
-- the methods directly.

-- Eventually this module will house the generic 'derive' mechanism, allowing
-- for this sort of thing:
-- derive `{{Foo}} Export [Eq,Show,Ord]
-- customizable in this fashion
-- derive `{{Foo}} Export [Eq,Ord]
-- derive `{{Foo}} Private [Show]

-- don't forget to have newtype deriving too! There's no reason we should have
-- to write up instances ourselves when the type we wrap has an instance.

-- deriving via would be neat too, how do?

-- derive functor, and applicative and monad

derivable : Type -> (Visibility -> Name -> Elab ())
derivable (Eq a) = deriveEq
derivable (Show a) = deriveShow
derivable t = \_,_ => fail "Given a (currently) non-derivable interface."

-- sort instances by requirments, e.g. (1,Eq), (2,Ord) etc

-- export
-- deriving : Visibility -> Name -> Type -> Elab ()
-- deriving vis nam ty = do
  -- let fun = derivable ty

{-

This pattern comes up a lot

isNoSugar : UnelabMode -> Bool
isNoSugar (NoSugar _) = True
isNoSugar _ = False
isDefImp : PiInfo t -> Bool
isDefImp (DefImplicit _) = True
isDefImp _ = False

We should have a deriving or converstion for this sort of thing, where you
select the 'true' case and all others are false. e.g.

data Foo : Type where
  Bif : Foo
  Waf : Int -> Foo

deriveSelectors Foo
results in

isBif : Foo -> Bool
isBif Bif = True
isBif _ = False

isWaf : Foo -> Bool
isWaf (Waf _) = True
isWaf _ = False

-}


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

module Text.Markup.Edda.Reader.Common

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

import Effects
import Effect.File
import Effect.StdIO

import Data.AVL.Dict

import Text.Markup.Edda.Model.Common
import Text.Markup.Edda.Model.Raw
import Text.Markup.Edda.Model.Processed

import Text.Markup.Edda.Process

import Text.Markup.Edda.Reader.Utils

%access export

-- ------------------------------------------------------------------ [ Reader ]

readEddaFileE : Parser (EddaRaw DOC)
             -> String
             -> Eff (Either String (Edda DOC)) [FILE ()]
readEddaFileE p f = do
    c <- parseFile (\x,y => unwords [x,show y]) (\x,y => unwords [x,y]) p f
    case  c of
      Left err  => pure $ Left err
      Right res => pure $ Right (processDoc res)

readEddaFile : Parser (EddaRaw DOC)
            -> String
            -> IO (Either String (Edda DOC))
readEddaFile p f = do
    Right str <- readFile f | (Left err) => pure (Left (show err))
    case parse f p str of
      Left err  => pure (Left err)
      Right res => pure (Right $ processDoc res)

readEddaSentance : Parser (EddaRaw INLINE)
                -> String
                -> Either String (Edda SNIPPET)
readEddaSentance p s =
  case parse (some p) s of
    Left err  => Left err
    Right res => Right $ (processSnippet $ Snippet res IsInLine)

readEddaBody : Parser (EddaRaw BLOCK)
        -> String
        -> Either String (Edda SNIPPET)
readEddaBody p ps =
  case parse (some p) ps of
    Left err  => Left err
    Right res => Right $ processSnippet $ Snippet res IsBlock

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Data.Map

import Control.Monad.State

%access public
%default total

namespace immutable
  class Map (m : Type -> Type -> Type) where
    empty : m k v

    fromList : List (k,v) -> m k v
    toList : m k v -> List (k,v)
    listKeys : m k v -> List k
    listValues : m k v -> List v

    fromVect : Vect n (k,v) -> m k v
    toVect : m k v -> (n ** Vect n (k,v))
    vectKeys : m k v -> (n ** Vect n (k))
    vectValues : m k v -> (n ** Vect n (v))

    grub : Eq k => k -> m k v -> List v
    lookup : Eq k => k -> m k v -> Maybe v

    insert : (k, v) -> m k v -> m k v
    erase : Eq k => k -> m k v -> m k v
    eraseBy : ((k,v) -> Bool) -> m k v -> m k v

  infix 2 !!
  (!!) : (Eq k, Map m) => m k v -> k -> List v
  (!!) = flip grub

  infix 2 !
  (!) : (Eq k, Map m)  => m k v -> k -> Maybe v
  (!) = flip lookup

  insertBy : Map m => (v -> k) -> v -> m k v -> m k v
  insertBy f v x = insert (f v, v) x

namespace mutable
  class Map (m : (Type -> Type) -> Type -> Type -> Type) where
    empty : f (m f k v)

    fromList : List (k,v) -> f (m f k v)
    toList : m f k v -> f (List (k,v))
    listKeys : m f k v -> f (List k)
    listValues : m f k v -> f (List v)

    fromVect : Vect n (k,v) -> f (m f k v)
    toVect : m f k v -> f (n ** Vect n (k,v))
    vectKeys : m f k v -> f (n ** Vect n k)
    vectValues : m f k v -> f (n ** Vect n v)

    grub : k -> m f k v -> f (List v)
    lookup : k -> m f k v -> f (Maybe v)

    insert : (k, v) -> m f k v -> f ()
    erase : k -> m f k v -> f ()
    eraseBy : ((k,v) -> Bool) -> m f k v -> f ()
    wipe : m f k v -> f ()

  infix 2 !!
  (!!) : mutable.Map m => m f k v -> k -> f (List v)
  (!!) = flip grub

  infix 2 !
  (!) : mutable.Map m  => m f k v -> k -> f (Maybe v)
  (!) = flip lookup

  insertBy : (Monad f, mutable.Map m) => (v -> f k) -> v -> m f k v -> f ()
  insertBy f v x = do { k <- f v; insert (k, v) x }

max_stars_repo_name: seagull-kamome/idris-toy

max_issues_repo_name: seagull-kamome/idris-toy

max_forks_repo_name: seagull-kamome/idris-toy


text:
module Main

if' : (x : Bool) -> a -> b -> (if x then a else b)
if' True a b = a
if' False a b = b

theAnswer : Nat
theAnswer = 42

myFunc : (x : Bool) -> (if x then Nat else String)
myFunc input = if' input theAnswer "The Answer"

double : Nat -> Nat
double x = 2*x

main : IO ()
main = print (double $ myFunc True)
--This also works:
--main = print ("Hi" ++ myFunc False)
--Output: 84

--The following type errors:
--main = print ("Hi" ++ myFunc True)

{- This also type errors:
hasEven : List Nat -> Bool
hasEven [] = False
hasEven (x :: xs) = if mod x 2 == 0 then True else hasEven xs

main = print (double . myFunc $ hasEven [1,3,5,7,9,10])
-}


text:
module Main

import Data.Vect

----------------------------------------------------------------------
-- Hilffunktion

remove : (x : a) -> (xs : Vect (S n) a) -> { auto prf : Elem x xs } -> Vect n a
remove {prf = Here} x (x :: ys) = ys
remove {prf = (There Here)} x (y :: (x :: xs)) = y :: xs
remove {prf = (There (There later))} x (y :: (z :: xs)) = y :: remove x (z::xs)

----------------------------------------------------------------------
-- Spiel-Zustand

data GameState : (guessesRemaining : Nat) -> (letters : Nat) -> Type where
  MkGameState : (word : String)
                -> (missing : Vect letters Char)
                -> GameState guessesRemaining letters

data Finished : Type where
  Lost : (game : GameState 0 (S letters)) -> Finished
  Won : (game : GameState (S guesses) 0) -> Finished

----------------------------------------------------------------------
-- Spielereingabe prüfen

data ValidInput : List Char -> Type where
  Letter : (c : Char) -> ValidInput [c]

toFew : ValidInput [] -> Void
toFew (Letter _) impossible

toMuch : ValidInput (c::c'::cs) -> Void
toMuch (Letter _) impossible

isValidInput : (cs : List Char) -> Dec (ValidInput cs)
isValidInput [] = No toFew
isValidInput [c] = Yes (Letter c)
isValidInput (c::c'::cs) = No toMuch

isValidString : (s : String) -> Dec (ValidInput (unpack s))
isValidString s = isValidInput _

----------------------------------------------------------------------
-- Eingabe

readGuess : IO (c ** ValidInput c)
readGuess = do
  putStrLn "Buchstabe? "
  input <- getLine
  case isValidString (toUpper input) of
    Yes prf => pure (_ ** prf)
    No _ => do
      print "ungültige Eingabe"
      readGuess

----------------------------------------------------------------------
-- Verarbeitung

processGuess : (letter : Char) ->
               GameState (S guesses) (S letters) ->
               Either (GameState guesses (S letters))
                      (GameState (S guesses) letters)
processGuess letter (MkGameState word missing) =
  case isElem letter missing of
    Yes ind => Right (MkGameState word (remove letter missing))
    No _ => Left (MkGameState word missing)

----------------------------------------------------------------------
-- Spiel-Funktion

game : GameState (S guesses) (S letters) -> IO Finished
game {guesses} {letters} gameState = do
  (_ ** Letter letter) <- readGuess
  case processGuess letter gameState of
    Left nope => do
      putStrLn "falsch geraten"
      case guesses of
        Z => pure (Lost nope)
        S k => game nope
    Right yeah => do
      putStrLn "richtig geraten"
      case letters of
        Z => pure (Won yeah)
        S k => game yeah

----------------------------------------------------------------------
-- Main

main : IO ()
main = do
  ergebnis <- game {guesses=5}
	(MkGameState "DevOpenSpace" ['D','E','V','O','P','N','S','A','C'])
  case ergebnis of
    Lost (MkGameState word _) =>
      putStrLn ("Verloren - das Wort war " ++ word)
    Won _ =>
      putStrLn "Gewonnen!"


text:
module Mrk.DSL

import public Mrk.Attributes
import public Mrk.Document
import public Mrk.Elements

%default total
%access public export

data ValidAnchor : (href : Maybe URI) -> (attrs : List Attribute) -> Type where
  Hyperlink : IsJust href -> ValidAnchor href attrs
  Placeholder : (IsJust href -> Void) -> (attrs = []) -> ValidAnchor href attrs

namespace Attributeful
  html : (attrs : List Attribute) ->
         (children : Document Html) ->
         {auto attrsPrf : disallowedAttrs Html attrs = []} ->
         Document Root
  html attrs children =
    tell $ Generic Html attrs (fromDocument children)

  head : List Attribute ->
         (children : Document Head) ->
         {auto prf : numTitles (fromDocument children) = 1} ->
         {auto validMeta : ValidMetaPosition (fromDocument children)} ->
         Document Html
  head attrs children =
    tell $ Head attrs (fromDocument children)

  meta : (firstAttr : Attribute) ->
         (attrs : List Attribute) ->
         {auto validAttr : isValidMetaFirstAttr firstAttr = True} ->
         {auto prf : disallowedAttrs Meta attrs = []} ->
         {auto placement : Meta `HasParent` parent} ->
         Document parent
  meta firstAttr attrs =
    tell $ Meta firstAttr attrs

  title : (attrs : List Attribute) ->
          (text : String) ->
          {auto prf : disallowedAttrs Title attrs = []} ->
          Document Head
  title attrs text =
    tell $ Generic Title attrs (Text text)

  body : (attrs : List Attribute) ->
         (children : Document Body) ->
         {auto prf : disallowedAttrs Body attrs = []} ->
         Document Html
  body attrs children =
    tell $ Generic Body attrs (fromDocument children)

  div : (attrs : List Attribute) ->
        (children : Document Div) ->
        {auto prf : Div `HasParent` parent} ->
        {auto attrsPrf : disallowedAttrs Div attrs = []} ->
        Document parent
  div attrs children =
    tell $ Generic Div attrs (fromDocument children)

  p : (attrs : List Attribute) ->
      (children : Document P) ->
      {auto prf : P `HasParent` parent} ->
      {auto attrsPrf : disallowedAttrs P attrs = []} ->
      Document parent
  p attrs children =
    tell $ Generic P attrs (fromDocument children)

  link : (rel : LinkType) ->
         (href : URI) ->
         (optionalAttrs : List Attribute) ->
         {auto placement : Link `HasParent` parent} ->
         {auto attrsAllowed : disallowedAttrs Link optionalAttrs = []} ->
         Document parent
  link rel href optionalAttrs =
    tell $ Link rel href optionalAttrs

  h1 : (attrs : List Attribute) ->
       {auto placement : H 1 `HasParent` parent} ->
       {auto attrsAllowed : disallowedAttrs (H 1) attrs = []} ->
       (children : Document (H 1)) ->
       Document parent
  h1 attrs children =
    tell $ Generic (H 1) attrs (fromDocument children)

  h2 : (attrs : List Attribute) ->
       {auto placement : H 2 `HasParent` parent} ->
       {auto attrsAllowed : disallowedAttrs (H 2) attrs = []} ->
       (children : Document (H 2)) ->
       Document parent
  h2 attrs children =
    tell $ Generic (H 2) attrs (fromDocument children)

  h3 : (attrs : List Attribute) ->
       {auto placement : H 3 `HasParent` parent} ->
       {auto attrsAllowed : disallowedAttrs (H 3) attrs = []} ->
       (children : Document (H 3)) ->
       Document parent
  h3 attrs children =
    tell $ Generic (H 3) attrs (fromDocument children)

  h4 : (attrs : List Attribute) ->
       {auto placement : H 4 `HasParent` parent} ->
       {auto attrsAllowed : disallowedAttrs (H 4) attrs = []} ->
       (children : Document (H 4)) ->
       Document parent
  h4 attrs children =
    tell $ Generic (H 4) attrs (fromDocument children)

  h5 : (attrs : List Attribute) ->
       {auto placement : H 5 `HasParent` parent} ->
       {auto attrsAllowed : disallowedAttrs (H 5) attrs = []} ->
       (children : Document (H 5)) ->
       Document parent
  h5 attrs children =
    tell $ Generic (H 5) attrs (fromDocument children)

  h6 : (attrs : List Attribute) ->
       {auto placement : H 6 `HasParent` parent} ->
       {auto attrsAllowed : disallowedAttrs (H 6) attrs = []} ->
       (children : Document (H 6)) ->
       Document parent
  h6 attrs children =
    tell $ Generic (H 6) attrs (fromDocument children)

  img : (src : URI) ->
        (alt : String) ->
        (optionalAttrs : List Attribute) ->
        {auto placement : Img `HasParent` parent} ->
        {auto attrsAllowed : disallowedAttrs Img optionalAttrs = []} ->
        Document parent
  img src alt optionalAttrs =
    tell $ Img src alt optionalAttrs

  ul : (attrs : List Attribute) ->
       (children : Document Ul) ->
       {auto prf : Ul `HasParent` parent} ->
       {auto attrsPrf : disallowedAttrs Ul attrs = []} ->
       Document parent
  ul attrs children =
    tell $ Generic Ul attrs (fromDocument children)

  li : (attrs : List Attribute) ->
       (children : Document Li) ->
       {auto prf : Li `HasParent` parent} ->
       {auto attrsPrf : disallowedAttrs Li attrs = []} ->
       Document parent
  li attrs children =
    tell $ Generic Li attrs (fromDocument children)

  a : (href : Maybe URI) ->
      (attrs : List Attribute) ->
      (children : Document A) ->
      {auto validAnchor : ValidAnchor href attrs} ->
      {auto placement : A `HasParent` parent} ->
      {auto attrsPrf : disallowedAttrs A attrs = []} ->
      Document parent
  a Nothing _ children = tell $ AnchorPlaceholder (fromDocument children)
  a (Just uri) attrs children = tell $ AnchorHyperlink uri attrs (fromDocument children)

namespace Attributeless

  html : (children : Document Html) ->
         Document Root
  html children = html [] children

  head : (children : Document Head) ->
         {auto prf : numTitles (fromDocument children) = 1} ->
         {auto validMeta : ValidMetaPosition (fromDocument children)} ->
         Document Html
  head children = head [] children

  meta : (firstAttr : Attribute) ->
         {auto validAttr : isValidMetaFirstAttr firstAttr = True} ->
         {auto placement : Meta `HasParent` parent} ->
         Document parent
  meta firstAttr = meta firstAttr []

  title : (text : String) ->
          Document Head
  title text = title [] text

  body : (children : Document Body) ->
         Document Html
  body children = body [] children

  div : (children : Document Div) ->
        {auto prf : Div `HasParent` parent} ->
        Document parent
  div children = div [] children

  p : (children : Document P) ->
      {auto prf : P `HasParent` parent} ->
      Document parent
  p children = p [] children

  link : (rel : LinkType) ->
         (href : URI) ->
         {auto placement : Link `HasParent` parent} ->
         Document parent
  link rel href = link rel href []

  h1 : {auto placement : H 1 `HasParent` parent} ->
       (children : Document (H 1)) ->
       Document parent
  h1 children = h1 [] children

  h2 : {auto placement : H 2 `HasParent` parent} ->
       (children : Document (H 2)) ->
       Document parent
  h2 children = h2 [] children

  h3 : {auto placement : H 3 `HasParent` parent} ->
       (children : Document (H 3)) ->
       Document parent
  h3 children = h3 [] children

  h4 : {auto placement : H 4 `HasParent` parent} ->
       (children : Document (H 4)) ->
       Document parent
  h4 children = h4 [] children

  h5 : {auto placement : H 5 `HasParent` parent} ->
       (children : Document (H 5)) ->
       Document parent
  h5 children = h5 [] children

  h6 : {auto placement : H 6 `HasParent` parent} ->
       (children : Document (H 6)) ->
       Document parent
  h6 children = h6 [] children

  img : (src : URI) ->
        (alt : String) ->
        {auto placement : Img `HasParent` parent} ->
        Document parent
  img src alt = img src alt []

  ul : (children : Document Ul) ->
       {auto prf : Ul `HasParent` parent} ->
       Document parent
  ul children = ul [] children

  li : (children : Document Li) ->
       {auto prf : Li `HasParent` parent} ->
       Document parent
  li children = li [] children

  a : (href : Maybe URI) ->
      (children : Document A) ->
      {auto validAnchor : ValidAnchor href []} ->
      {auto placement : A `HasParent` parent} ->
      Document parent
  a Nothing children = a Nothing [] children
  a (Just uri) children = a (Just uri) [] children

  text : String ->
         Document parent
  text =
    tell . Text

namespace Texty
  li : (s : String) ->
       {auto prf : Li `HasParent` parent} ->
       Document parent
  li s = li [] $ text s

  p : (s : String) ->
      {auto prf : P `HasParent` parent} ->
      Document parent
  p s = p [] $ text s

  h1 : {auto placement : H 1 `HasParent` parent} ->
       (s : String) ->
       Document parent
  h1 s = h1 [] $ text s

  h2 : {auto placement : H 2 `HasParent` parent} ->
       (s : String) ->
       Document parent
  h2 s = h2 [] $ text s

  h3 : {auto placement : H 3 `HasParent` parent} ->
       (s : String) ->
       Document parent
  h3 s = h3 [] $ text s

  h4 : {auto placement : H 4 `HasParent` parent} ->
       (s : String) ->
       Document parent
  h4 s = h4 [] $ text s

  h5 : {auto placement : H 5 `HasParent` parent} ->
       (s : String) ->
       Document parent
  h5 s = h5 [] $ text s

  h6 : {auto placement : H 6 `HasParent` parent} ->
       (s : String) ->
       Document parent
  h6 s = h6 [] $ text s

  a : (href : Maybe URI) ->
      (s : String) ->
      {auto validAnchor : ValidAnchor href []} ->
      {auto placement : A `HasParent` parent} ->
      Document parent
  a Nothing s = a Nothing [] $ text s
  a (Just uri) s = a (Just uri) [] $ text s

namespace HighLevel
  stylesheet : (href : URI) ->
               {auto placement : Link `HasParent` parent} ->
               Document parent
  stylesheet href = link Stylesheet href [MimeType $ Text CSS]

max_stars_repo_name: camelpunch/mrk

max_issues_repo_name: camelpunch/mrk

max_forks_repo_name: camelpunch/mrk


text:
module GCD

data Divides : (d : Nat) -> (m : Nat) -> Type where
    FactorsWith : (d : Nat) -> (f : Nat) -> Divides d (d * f)

div_3_12 : Divides 3 12
div_3_12 = FactorsWith 3 4

total
testDivides : (d : Nat) -> (m : Nat) -> Bool
testDivides d Z = True
testDivides Z (S k) = False
testDivides (S d') (S k') = if (S d') > (S k') then False else testDivides (S d') (minus (S k') (S d'))

total
searchGCD_rec : Nat -> Nat -> Nat -> Nat
searchGCD_rec k j Z = Z--_1
searchGCD_rec k j (S d') = if testDivides (S d') k && testDivides (S d') j then (S d') else searchGCD_rec k j d'

total
searchGCD : Nat -> Nat -> Nat
searchGCD k j = searchGCD_rec k j k -- or j

-- total
-- euclid_rec : Nat -> Nat -> Nat -> Nat -> Nat
-- euclid_rec m n q r = if r >= n then euclid_rec m n (S q) (minus r n) else r

data IsPrime : (n : Nat) -> Type where
    NoDivisor : (d : Nat) -> (n : Nat) -> (Divides d (S n) -> Either (d = 1) (d = S n)) -> IsPrime (S n)

zeroNotPrime : Not (IsPrime Z)
zeroNotPrime (NoDivisor _ _ _) impossible

testPrime : (n : Nat) -> Dec (IsPrime n)
testPrime Z = No zeroNotPrime
testPrime (S n') = ?testPrime_rhs_2


text:
module Extra.C.Types

-- TODO: c int,uint is not guaranteed to be 32 bit

export
data Float : Type where [external]

public export
CUInt8 : Type
CUInt8 = Bits8

public export
CUInt16 : Type
CUInt16 = Bits16

public export
CUInt32 : Type
CUInt32 = Bits32

public export
CUInt64 : Type
CUInt64 = Bits64

||| `size_t in C`
public export
SizeT : Type
SizeT = Bits32

||| `ssize_t` in C
public export
SSizeT : Type
SSizeT = Int

public export
CInt32 : Type
CInt32 = Int

||| `int` in C
public export
CInt : Type
CInt = Int

||| `unsigned int` in C
public export
CUInt : Type
CUInt = CUInt32

public export
CChar : Type
CChar = Bits8

public export
CUChar : Type
CUChar = Bits8

public export
CString : Type
CString = Ptr CChar

public export
CDouble : Type
CDouble = Double

--- TODO: this is unholy
||| `SizeT` but uses `Int` for `Data.Int.Order` reasons
public export
SizeInt : Type
SizeInt = Int


text:
module Network.TLS.Wrapper

import Data.Nat
import Utils.Misc
import Data.Vect
import Data.List
import Network.TLS.Magic

public export
record Wrapper (mac_size : Nat) where
  constructor MkWrapper
  encrypted_data : List Bits8
  auth_tag : Vect mac_size Bits8

public export
to_application_data : Wrapper mac_size -> List Bits8
to_application_data x = x.encrypted_data <+> toList x.auth_tag

public export
from_application_data : {mac_size : _} -> (application_data : List Bits8) -> Maybe (Wrapper mac_size)
from_application_data xs =
  let xs' = fromList xs in
  case isLTE mac_size (length xs) of
    Yes prf =>
      let
        (encrypted_data, auth_tag) = splitAt (minus (length xs) mac_size) $ replace_vect (sym $ plusMinusLte _ _ prf) xs'
      in
        Just $ MkWrapper (toList encrypted_data) auth_tag
    No contra => Nothing

public export
record Wrapper2 (iv_size : Nat) (mac_size : Nat) where
  constructor MkWrapper2
  iv_data : Vect iv_size Bits8
  encrypted_data : List Bits8
  auth_tag : Vect mac_size Bits8

public export
to_application_data2 : Wrapper2 iv_size mac_size -> List Bits8
to_application_data2 x = toList x.iv_data <+> x.encrypted_data <+> toList x.auth_tag

public export
from_application_data2 : {iv_size : _} -> {mac_size : _} -> (application_data : List Bits8) -> Maybe (Wrapper2 iv_size mac_size)
from_application_data2 xs = do
  let (iv, ciphertext) = splitAt iv_size xs
  iv' <- exactLength iv_size $ fromList iv
  w <- from_application_data ciphertext
  pure $ MkWrapper2 iv' w.encrypted_data w.auth_tag

namespace WrappedRecord
  public export
  record WrappedRecord where
    constructor MkWrappedRecord
    record_type : RecordType
    wrapped_data : List Bits8

  public export
  to_application_data : WrappedRecord -> List Bits8
  to_application_data x = x.wrapped_data <+> [record_type_to_id x.record_type]


text:
module Core.Options

import Core.Core
import Core.Name
import public Core.Options.Log
import Core.TT
import Utils.Binary
import Utils.Path

import Data.List
import Data.List1
import Data.Maybe
import Data.Strings

import System.Info

%default total

public export
record Dirs where
  constructor MkDirs
  working_dir : String
  source_dir : Maybe String -- source directory, relative to working directory
  build_dir : String -- build directory, relative to working directory
  output_dir : Maybe String -- output directory, relative to working directory
  prefix_dir : String -- installation prefix, for finding data files (e.g. run time support)
  package_dirs : List String -- places to look for packages
  extra_dirs : List String -- places to look for import files
  lib_dirs : List String -- places to look for libraries (for code generation)
  data_dirs : List String -- places to look for data file

export
execBuildDir : Dirs -> String
execBuildDir d = build_dir d </> "exec"

export
outputDirWithDefault : Dirs -> String
outputDirWithDefault d = fromMaybe (build_dir d </> "exec") (output_dir d)

public export
toString : Dirs -> String
toString d@(MkDirs wdir sdir bdir odir dfix pdirs edirs ldirs ddirs) =
  unlines [ "+ Working Directory      :: " ++ show wdir
          , "+ Source Directory       :: " ++ show sdir
          , "+ Build Directory        :: " ++ show bdir
          , "+ Output Directory       :: " ++ show (outputDirWithDefault d)
          , "+ Installation Prefix    :: " ++ show dfix
          , "+ Package Directories    :: " ++ show pdirs
          , "+ Extra Directories      :: " ++ show edirs
          , "+ CG Library Directories :: " ++ show ldirs
          , "+ Data Directories       :: " ++ show ddirs]

public export
data CG = Chez
        | Racket
        | Gambit
        | Node
        | Javascript
        | Other String

export
Eq CG where
  Chez == Chez = True
  Racket == Racket = True
  Gambit == Gambit = True
  Node == Node = True
  Javascript == Javascript = True
  Other s == Other t = s == t
  _ == _ = False

export
Show CG where
  show Chez = "chez"
  show Racket = "racket"
  show Gambit = "gambit"
  show Node = "node"
  show Javascript = "javascript"
  show (Other s) = s

public export
record PairNames where
  constructor MkPairNs
  pairType : Name
  fstName : Name
  sndName : Name

public export
record RewriteNames where
  constructor MkRewriteNs
  equalType : Name
  rewriteName : Name

public export
record PrimNames where
  constructor MkPrimNs
  fromIntegerName : Maybe Name
  fromStringName : Maybe Name
  fromCharName : Maybe Name

public export
data LangExt
     = ElabReflection
     | Borrowing -- not yet implemented
     | PostfixProjections

export
Eq LangExt where
  ElabReflection == ElabReflection = True
  Borrowing == Borrowing = True
  PostfixProjections == PostfixProjections = True
  _ == _ = False

-- Other options relevant to the current session (so not to be saved in a TTC)
public export
record ElabDirectives where
  constructor MkElabDirectives
  lazyActive : Bool
  unboundImplicits : Bool
  totality : TotalReq
  ambigLimit : Nat
  autoImplicitLimit : Nat

public export
record Session where
  constructor MkSessionOpts
  noprelude : Bool
  nobanner : Bool
  findipkg : Bool
  codegen : CG
  directives : List String
  packages : List String
  changedModules : Maybe (List1 ModuleIdent)
  logLevel : LogLevels
  logTimings : Bool
  debugElabCheck : Bool -- do conversion check to verify results of elaborator
  dumpcases : Maybe String -- file to output compiled case trees
  dumplifted : Maybe String -- file to output lambda lifted definitions
  dumpanf : Maybe String -- file to output ANF definitions
  dumpvmcode : Maybe String -- file to output VM code definitions

public export
record PPrinter where
  constructor MkPPOpts
  showImplicits : Bool
  showFullEnv : Bool
  fullNamespace : Bool

public export
record Options where
  constructor MkOptions
  dirs : Dirs
  printing : PPrinter
  session : Session
  elabDirectives : ElabDirectives
  pairnames : Maybe PairNames
  rewritenames : Maybe RewriteNames
  primnames : PrimNames
  extensions : List LangExt
  additionalCGs : List (String, CG)

export
availableCGs : Options -> List (String, CG)
availableCGs o
    = [("chez", Chez),
       ("racket", Racket),
       ("node", Node),
       ("javascript", Javascript),
       ("gambit", Gambit)] ++ additionalCGs o

export
getCG : Options -> String -> Maybe CG
getCG o cg = lookup (toLower cg) (availableCGs o)

defaultDirs : Dirs
defaultDirs = MkDirs "." Nothing "build" Nothing
                     "/usr/local" [] ["."] [] []

defaultPPrint : PPrinter
defaultPPrint = MkPPOpts False True False

export
defaultSession : Session
defaultSession = MkSessionOpts False False False Chez [] [] Nothing defaultLogLevel
                               False False Nothing Nothing
                               Nothing Nothing

export
defaultElab : ElabDirectives
defaultElab = MkElabDirectives True True CoveringOnly 3 50

export
defaults : Options
defaults = MkOptions defaultDirs defaultPPrint defaultSession
                     defaultElab Nothing Nothing
                     (MkPrimNs Nothing Nothing Nothing) []
                     []

-- Reset the options which are set by source files
export
clearNames : Options -> Options
clearNames = record { pairnames = Nothing,
                      rewritenames = Nothing,
                      primnames = MkPrimNs Nothing Nothing Nothing,
                      extensions = []
                    }

export
setPair : (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->
          Options -> Options
setPair ty f s = record { pairnames = Just (MkPairNs ty f s) }

export
setRewrite : (eq : Name) -> (rwlemma : Name) -> Options -> Options
setRewrite eq rw = record { rewritenames = Just (MkRewriteNs eq rw) }

export
setFromInteger : Name -> Options -> Options
setFromInteger n = record { primnames->fromIntegerName = Just n }

export
setFromString : Name -> Options -> Options
setFromString n = record { primnames->fromStringName = Just n }

export
setFromChar : Name -> Options -> Options
setFromChar n = record { primnames->fromCharName = Just n }

export
setExtension : LangExt -> Options -> Options
setExtension e = record { extensions $= (e ::) }

export
isExtension : LangExt -> Options -> Bool
isExtension e opts = e `elem` extensions opts

export
addCG : (String, CG) -> Options -> Options
addCG cg = record { additionalCGs $= (cg::) }


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 11, section 3, questions 2 and 3

-- check that all functions are total
%default total

data LazyFuel = LDry | LMore (Lazy LazyFuel)

partial
forever : LazyFuel
forever = LMore forever

data Command : Type -> Type where
  PutStr : String -> Command ()
  GetLine : Command String
  Pure : ty -> Command ty
  Bind : Command a -> (a -> Command b) -> Command b
  ReadFile : String -> Command (Either FileError String)
  WriteFile : String -> String -> Command (Either FileError ())

namespace Command
  (>>=) : Command a -> (a -> Command b) -> Command b
  (>>=) = Bind

runCommand : Command a -> IO a
runCommand (PutStr x) = putStr x
runCommand GetLine = getLine
runCommand (Pure x) = pure x
runCommand (Bind x f) = do res <- runCommand x
                           runCommand (f res)
runCommand (ReadFile f) = readFile f
runCommand (WriteFile f x) = writeFile f x

data ConsoleIO : Type -> Type where
  Quit : a -> ConsoleIO a
  Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

namespace Console
  (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
  (>>=) = Do

run : LazyFuel -> ConsoleIO a -> IO (Maybe a)
run _ (Quit v) = pure $ Just v
run LDry (Do act gen) = pure Nothing
run (LMore fuel) (Do act gen) = do res <- runCommand act
                                   run fuel $ gen res

data ShellInput = Cat String
                | Copy String String
                | Exit
                | Error String

readInput : (prompt : String) -> Command ShellInput
readInput prompt
  = do PutStr prompt
       input <- GetLine
       parts <- Pure $ words input
       case parts of
         ["cat", filename] => Pure $ Cat filename
         ["copy", source, destination] => Pure $ Copy source destination
         ["exit"] => Pure $ Exit
         _ => Pure $ Error "Unknown command\n"

cat : String -> Command ()
cat filename = do res <- ReadFile filename
                  case res of
                    Right contents => PutStr contents
                    Left error => PutStr $ show error ++ "\n"

copy : String -> String -> Command ()
copy source destination =
  do res1 <- ReadFile source
     case res1 of
       Left error => PutStr $ show error ++ " (source) \n"
       Right contents => do res2 <- WriteFile destination contents
                            case res2 of
                              Left error => PutStr $ show error ++ " (destination)\n"
                              Right () => PutStr "File copied\n"

shell : ConsoleIO ()
shell = do cmd <- readInput "> "
           case cmd of
             Cat filename => do cat filename
                                shell
             Copy source destination => do copy source destination
                                           shell
             Exit => Quit ()
             Error error => do PutStr error
                               shell

-- :exec
-- > cat input.txt
-- (...) file
-- > copy input.txt output.txt
-- File copied
-- > cat output.txt
-- (...) file
partial
main : IO ()
main = do run forever shell
          pure ()

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module DataWAuto

data X : Int => Type -> Type where
  X0 : Int => X Int

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


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

import Data.List

import Test.Golden

%default total

netlistGood : IO TestPool
netlistGood
  = testsInDir "netlist/good"
               (const True)
               "NetList Good library"
               Nil
               Nothing

covering
main : IO ()
main
  = runner [ !netlistGood ]

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
||| State used during JS code generation and when
||| converting `NamedCExp` to imperative statements.
module Compiler.ES.State

import Core.Context
import Compiler.ES.Ast
import Libraries.Data.SortedMap

%default total

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

||| Convenient alias for `throw . InternalError`
export
error : String -> Core a
error = throw . InternalError

||| Convenient alias for `error . fastConcat`.
export
errorConcat : List String -> Core a
errorConcat = error . fastConcat

--------------------------------------------------------------------------------
--          CG Mode
--------------------------------------------------------------------------------

||| Specifies the readability of the generated code.
|||
||| In `Pretty` mode (the default), the codegen will
||| lift multiline lambdas from argument lists to the
||| surrounding scope and keep user generated names.
||| In addition, blocks of code are laid out with indentation
||| and linebreaks for better readability.
|||
||| In `Compact` mode, all local variables are replace with
||| short machine generated ones, and every toplevel
||| function is printed on a single line without
||| line-breaks or indentation.
|||
||| Finally, `Minimal` mode is like `Compact`, but toplevel
||| function names will be mangled and replaced with
||| machine generated indices.
public export
data CGMode = Pretty | Compact | Minimal

||| We only keep user defined local names and only so
||| in `Pretty` mode.
export
keepLocalName : Name -> CGMode -> Bool
keepLocalName (UN n) Pretty = True
keepLocalName _      _      = False

||| We mangle toplevel function names only in `Minimal` mode.
export
keepRefName : Name -> CGMode -> Bool
keepRefName _ Minimal = False
keepRefName _ _       = True

--------------------------------------------------------------------------------
--          State
--------------------------------------------------------------------------------

public export
data ESs : Type where

||| Settings and state used during JS code generation.
public export
record ESSt where
  constructor MkESSt
  ||| Whether to always use minimal names
  mode     : CGMode

  ||| Returns `True`, if the given expression can be used as an
  ||| argument in a function call. (If this returns `False`, the
  ||| given expression will be lifted to the surrounding scope
  ||| and bound to a new local variable).
  isArg    : Exp -> Bool

  ||| Returns `True`, if the given expression can be used directly
  ||| in a function application. (If this returns `False`, the
  ||| given expression will be lifted to the surrounding scope
  ||| and bound to a variable).
  isFun    : Exp -> Bool

  ||| Current local variable index
  loc      : Int

  ||| Current global variable index
  ref      : Int

  ||| Mapping from local names to minimal expressions
  locals   : SortedMap Name Minimal

  ||| Mapping from toplevel function names to variables
  refs     : SortedMap Name Var

  ||| Mappings from name to definitions to be added
  ||| to the preamble.
  preamble : SortedMap String String

  ||| Accepted codegen types in foreign function definitions.
  ||| For JS, this is either `["node","javascript"]` or
  ||| `["browser","javascript"]`.
  ccTypes  : List String

--------------------------------------------------------------------------------
--          Local Variables
--------------------------------------------------------------------------------

||| Map a local name to the given minimal expression
export
addLocal : { auto c : Ref ESs ESSt } -> Name -> Minimal -> Core ()
addLocal n v = update ESs $ record { locals $= insert n v }

||| Get and bump the local var index
export
nextLocal : { auto c : Ref ESs ESSt } -> Core Var
nextLocal = do
  st <- get ESs
  put ESs $ record { loc $= (+1) } st
  pure $ VLoc st.loc

||| Register a `Name` as a local variable. The name is kept
||| unchanged if `keepLocalName` returns `True` with the
||| current name and state, otherwise it is converted to
||| a new local variable.
export
registerLocal : {auto c : Ref ESs ESSt} -> (name : Name) -> Core Var
registerLocal n = do
  st <- get ESs
  if keepLocalName n st.mode
     then let v = VName n in addLocal n (MVar v) >> pure v
     else do v <- nextLocal
             addLocal n (MVar v)
             pure v

||| Look up a name and call `registerLocal` in case it has
||| not been added to the map of local names.
export
getOrRegisterLocal : {auto c : Ref ESs ESSt} -> Name -> Core Minimal
getOrRegisterLocal n = do
  Nothing <- lookup n . locals <$> get ESs
    | Just v => pure v
  MVar <$> registerLocal n

||| Maps the given list of names (from a pattern match
||| on a data constructor) to the corresponding
||| projections on the given scrutinee.
export
projections :  {auto c : Ref ESs ESSt}
            -> (scrutinee : Minimal)
            -> List Name
            -> Core ()
projections sc xs =
  let ps = zip [1..length xs] xs
   in traverse_ (\(i,n) => addLocal n $ MProjection i sc) ps

--------------------------------------------------------------------------------
--          Toplevel Names
--------------------------------------------------------------------------------

||| Map a toplevel function name to the given `Var`
export
addRef : { auto c : Ref ESs ESSt } -> Name -> Var -> Core ()
addRef n v = update ESs $ record { refs $= insert n v }

||| Get and bump the local ref index
export
nextRef : { auto c : Ref ESs ESSt } -> Core Var
nextRef = do
  st <- get ESs
  put ESs $ record { ref $= (+1) } st
  pure $ VRef st.ref

registerRef : {auto c : Ref ESs ESSt} -> (name : Name) -> Core Var
registerRef n = do
  st <- get ESs
  if keepRefName n st.mode
     then let v = VName n in addRef n v >> pure v
     else do v <- nextRef
             addRef n v
             pure v

||| Look up a name and call `registerRef` in case it has
||| not been added to the map of toplevel function names.
||| The name will be replace with an index if the current
||| `GCMode` is set to `Minimal`.
export
getOrRegisterRef : {auto c : Ref ESs ESSt} -> Name -> Core Var
getOrRegisterRef n = do
  Nothing <- lookup n . refs <$> get ESs
    | Just v => pure v
  registerRef n

--------------------------------------------------------------------------------
--          Preamble and Foreign Definitions
--------------------------------------------------------------------------------

||| Add a new set of definitions under the given name to
||| the preamble. Fails with an error if a different set
||| of definitions have already been added under the same name.
export
addToPreamble :  {auto c : Ref ESs ESSt}
              -> (name : String)
              -> (def : String) -> Core ()
addToPreamble name def = do
  s <- get ESs
  case lookup name (preamble s) of
    Nothing => put ESs $ record { preamble $= insert name def } s
    Just x =>
      unless (x == def) $ do
        errorConcat
              [ "two incompatible definitions for ", name
              , "<|",x ,"|> <|" , def, "|>"
              ]

--------------------------------------------------------------------------------
--          Initialize State
--------------------------------------------------------------------------------

||| Initial state of the code generator
export
init :  (mode  : CGMode)
     -> (isArg : Exp -> Bool)
     -> (isFun : Exp -> Bool)
     -> (types : List String)
     -> ESSt
init mode isArg isFun ccs =
  MkESSt mode isArg isFun 0 0 empty empty empty ccs

||| Reset the local state before defining a new toplevel
||| function.
export
reset : {auto c : Ref ESs ESSt} -> Core ()
reset = update ESs $ record { loc = 0, locals = empty }


text:
module Derive.Kit

import Data.Vect

import Language.Reflection.Elab
import Language.Reflection.Utils
import Pruviloj.Core

%default total

||| Run something for effects, throwing away the return value
ignore : Functor f => f a -> f ()
ignore x = map (const ()) x

||| Do nothing
skip : Applicative f => f ()
skip = pure ()

last : List a -> Elab a
last [] = fail [TextPart "Unexpected empty list"]
last [x] = pure x
last (_::x::xs) = last (x::xs)

getSigmaArgs : Raw -> Elab (Raw, Raw)
getSigmaArgs `(MkSigma {a=~_} {P=~_} ~rhsTy ~lhs) = pure (rhsTy, lhs)
getSigmaArgs arg = fail [TextPart "Not a sigma constructor"]

||| Ensure that all of a collection of holes was properly solved, to
||| sanity-check a use of `apply`
allSolved : List TTName -> Elab ()
allSolved ns = allSolved' ns !getHoles
  where allSolved' : List TTName -> List TTName -> Elab ()
        allSolved' [] hs = pure ()
        allSolved' (n::ns) hs =
          if elem n hs
            then debugMessage [TextPart "Not all holes were solved! Remaining: ",
                       TextPart $ show n,
                       TextPart $ show hs]
            else allSolved' ns hs

zipH : List a -> List b -> Elab (List (a, b))
zipH [] [] = pure []
zipH (x::xs) (y::ys) = ((x, y) ::) <$> zipH xs ys
zipH _ _ = fail [TextPart "length mismatch"]

assoc : Eq a => a -> List (a, b) -> Elab b
assoc x [] = fail [ TextPart "not found" ]
assoc x ((y, z)::ys) = if x == y then pure z else assoc x ys

doTimes : Applicative m => (n : Nat) -> m a -> m (Vect n a)
doTimes Z x = pure []
doTimes (S k) x = [| x :: (doTimes k x) |]

isRType : Raw -> Bool
isRType RType = True
isRType _ = False

unsafeNth : Nat -> List a -> Elab a
unsafeNth _     []        = fail [TextPart "Ran out of list elements"]
unsafeNth Z     (x :: _)  = pure x
unsafeNth (S k) (_ :: xs) = unsafeNth k xs

headVar : Raw -> Maybe TTName
headVar (RApp f _) = headVar f
headVar (Var n) = Just n
headVar x = Nothing

||| Generate holes suitable as arguments to a term of some type
argHoles : Raw -> Elab (List TTName)
argHoles (RBind n (Pi t _) body) = do n' <- nameFrom n
                                      claim n t
                                      unfocus n
                                      (n ::) <$> argHoles body
argHoles _ = pure []

enumerate : List a -> List (Nat, a)
enumerate xs = enumerate' xs 0
  where enumerate' : List a -> Nat -> List (Nat, a)
        enumerate' [] _ = []
        enumerate' (x::xs) n = (n, x) :: enumerate' xs (S n)

namespace Renamers
  ||| Cause a renamer to forget a renaming
  restrict : (TTName -> Maybe TTName) -> TTName -> (TTName -> Maybe TTName)
  restrict f n n' = if n == n' then Nothing else f n'

  ||| Extend a renamer with a new renaming
  extend : (TTName -> Maybe TTName) -> TTName -> TTName -> (TTName -> Maybe TTName)
  extend f n n' n'' = if n'' == n then Just n' else f n''

  rename : TTName -> TTName -> TTName -> Maybe TTName
  rename from to = extend (const Nothing) from to

||| Alpha-convert `Raw` terms
||| @ subst a partial name substitution function
partial
alphaRaw : (subst : TTName -> Maybe TTName) -> Raw -> Raw
alphaRaw subst (Var n) with (subst n)
  alphaRaw subst (Var n) | Nothing = Var n
  alphaRaw subst (Var n) | Just n' = Var n'
alphaRaw subst (RBind n b tm) =
  let subst' = restrict subst n
      b' = map (alphaRaw subst) b
  in RBind n b' (alphaRaw subst' tm)
alphaRaw subst (RApp tm tm') = RApp (alphaRaw subst tm) (alphaRaw subst tm')
alphaRaw subst RType = RType
alphaRaw subst (RUType x) = RUType x
alphaRaw subst (RConstant c) = RConstant c

||| Grab the binders from around a term, alpha-converting to make their names unique
partial
stealBindings : Raw -> (nsubst : TTName -> Maybe TTName) -> Elab (List (TTName, Binder Raw), Raw)
stealBindings (RBind n b tm) nsubst =
  do n' <- nameFrom n
     (bindings, result) <- stealBindings tm (extend nsubst n n')
     pure ((n', map (alphaRaw nsubst) b) :: bindings, result)
stealBindings tm nsubst = pure ([], alphaRaw nsubst tm)

||| Grab the binders from around a term, assuming that they have been previously uniquified
extractBinders : Raw -> (List (TTName, Binder Raw), Raw)
extractBinders (RBind n b tm) = let (bs, res) = extractBinders tm
                                in ((n, b) :: bs, res)
extractBinders tm = ([], tm)

||| Get the type annotation from a binder
getBinderTy : Binder t -> t
getBinderTy (Lam t) = t
getBinderTy (Pi t _) = t
getBinderTy (Let t _) = t
getBinderTy (Hole t) = t
getBinderTy (GHole t) = t
getBinderTy (Guess t _) = t
getBinderTy (PVar t) = t
getBinderTy (PVTy t) = t

mkDecl : TTName -> List (TTName, Erasure, Binder Raw) -> Raw -> TyDecl
mkDecl fn xs tm = Declare fn (map (\(n, e, b) => MkFunArg  n (getBinderTy b) Implicit e) xs) tm

mkPairTy : Raw -> Raw -> Raw
mkPairTy a b = `((~a, ~b) : Type)

rebind : List (TTName, Binder Raw) -> Raw -> Raw
rebind [] tm = tm
rebind ((n, b) :: nbs) tm = RBind n b $ rebind nbs tm

bindPats : List (TTName, Binder Raw) -> Raw -> Raw
bindPats [] res = res
bindPats ((n, b)::bs) res = RBind n (PVar (getBinderTy b)) $ bindPats bs res

bindPatTys : List (TTName, Binder Raw) -> Raw -> Raw
bindPatTys [] res = res
bindPatTys ((n, b)::bs) res = RBind n (PVTy (getBinderTy b)) $ bindPatTys bs res

updateFunArgTy : (Raw -> Raw) -> FunArg -> FunArg
updateFunArgTy f arg = record {type = f (record {type} arg)} arg

tyConArgName : TyConArg -> TTName
tyConArgName (TyConParameter a) = name a
tyConArgName (TyConIndex a) = name a

setTyConArgName : TyConArg -> TTName -> TyConArg
setTyConArgName (TyConParameter a) n = TyConParameter (record {name = n} a)
setTyConArgName (TyConIndex a) n = TyConIndex (record {name = n} a)

updateTyConArgTy : (Raw -> Raw) -> TyConArg -> TyConArg
updateTyConArgTy f (TyConParameter a) = TyConParameter (record {type = f (type a) } a)
updateTyConArgTy f (TyConIndex a) = TyConIndex (record {type = f (type a) } a)

namespace Tactics

  intro1 : Elab TTName
  intro1 = do g <- snd <$> getGoal
              case g of
                Bind n (Pi _ _) _ => do n' <- nameFrom n
                                        intro n'
                                        pure n'
                _ => fail [ TextPart "Can't intro1 because goal"
                          , TermPart g
                          , TextPart "isn't a function type."]

  intros : Elab (List TTName)
  intros = do g <- snd <$> getGoal
              go g
    where go : TT -> Elab (List TTName)
          go (Bind n (Pi _ _) body) = do n' <- nameFrom n
                                         intro n'
                                         (n' ::) <$> go body
          go _ = pure []

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:
module Data.SnocVect

import Data.Vect

%hide Prelude.Types.elem

%default total

||| A Backwards Vect
public export
data SnocVect : Nat -> Type -> Type where
  ||| Empty snoc-vect
  Lin : SnocVect 0 a

  ||| A non-empty snoc-vect, consisting of the rest of the snoc-vect and the final element.
  (:<) : (SnocVect n a) -> a -> SnocVect (S n) a

%name SnocVect sx, sy, sz

infixl 7 <><
infixr 6 <>>

||| 'fish': Action of lists on snoc-lists
public export
(<><) : SnocVect n a -> Vect m a -> SnocVect (n + m) a
sx <>< [] = rewrite plusZeroRightNeutral n in sx
sx <>< ((::) x xs {len}) =
  rewrite sym $ plusSuccRightSucc n len in
          sx :< x <>< xs

||| 'chips': Action of snoc-lists on lists
public export
(<>>) : SnocVect j a -> Vect k a -> Vect (j + k) a
Lin       <>> xs = xs
((:<) sx x {n}) <>> xs =
  rewrite plusSuccRightSucc n k in
          sx <>> x :: xs

export
Cast (SnocVect n a) (Vect n a) where
  cast sx = rewrite sym $ plusZeroRightNeutral n in
                    sx <>> []

export
Cast (Vect n a) (SnocVect n a) where
  cast xs = Lin <>< xs

||| Transform to a vect but keeping the contents in the spine order (term depth).
public export
asVect : SnocVect n type -> Vect n type
asVect = (reverse . cast)

public export
Eq a => Eq (SnocVect n a) where
  (==) Lin Lin = True
  (==) (sx :< x) (sy :< y) = x == y && sx == sy
  (==) _ _ = False

public export
Ord a => Ord (SnocVect n a) where
  compare Lin Lin = EQ
  compare (sx :< x) (sy :< y)
    = case compare sx sy of
        EQ => compare x y
        c  => c

||| True iff input is Lin
public export
isLin : SnocVect n a -> Bool
isLin Lin = True
isLin (sx :< x) = False

||| True iff input is (:<)
public export
isSnoc : SnocVect n a -> Bool
isSnoc Lin     = False
isSnoc (sx :< x) = True

public export
(++) : (sx : SnocVect j a) ->  (sy : SnocVect k a) -> SnocVect (j + k) a
(++) sx Lin = rewrite plusZeroRightNeutral j in sx
(++) sx ((:<) sy y {n}) =
  rewrite sym $ plusSuccRightSucc j n in
          (sx ++ sy) :< y

public export
length : SnocVect n a -> Nat
length Lin = Z
length (sx :< x) = S $ length sx

export
lengthCorrect : (sx : SnocVect n a) -> length sx = n
lengthCorrect [<]       = Refl
lengthCorrect (sx :< x) = cong S (lengthCorrect sx)

public export
replicate : (k : Nat) -> a -> SnocVect k a
replicate 0 x = [<]
replicate (S k) x = replicate k x :< x

||| The "head" of the snoc-vect
public export
deah : SnocVect (S n) a -> a
deah (sx :< x) = x

||| The "tail" of the snoc-vect
public export
liat : SnocVect (S n) a -> SnocVect n a
liat (sx :< x) = sx

export
Show a => Show (SnocVect n a) where
  show sx = concat ("[< " :: intersperse ", " (show' [] sx) ++ ["]"])
    where
      show' : Vect j String -> SnocVect k a -> Vect (j + k) String
      show' acc Lin       = rewrite plusZeroRightNeutral j in acc
      show' acc ((:<) xs x {n}) =
        rewrite sym $ plusSuccRightSucc j n in
                show' (show x :: acc) xs

public export
Functor (SnocVect n) where
  map f Lin = Lin
  map f (sx :< x) = (map f sx) :< (f x)

public export
Zippable (SnocVect k) where
  zipWith _ [<] [<] = [<]
  zipWith f (sx :< x) (sy :< y) = zipWith f sx sy :< f x y

  zipWith3 _ [<] [<] [<] = [<]
  zipWith3 f (sx :< x) (sy :< y) (sz :< z) = zipWith3 f sx sy sz :< f x y z

  unzipWith f [<] = ([<], [<])
  unzipWith f (sx :< x) = let (b, c) = f x
                              (sb, sc) = unzipWith f sx in
                              (sb :< b, sc :< c)

  unzipWith3 f [<] = ([<], [<], [<])
  unzipWith3 f (sx :< x) = let (b, c, d) = f x
                               (sb, sc, sd) = unzipWith3 f sx in
                               (sb :< b, sc :< c, sd :< d)

public export
Semigroup a => Semigroup (SnocVect n a) where
  (<+>) = zipWith (<+>)

public export
{k : Nat} -> Monoid a => Monoid (SnocVect k a) where
  neutral = replicate k neutral

public export
Foldable (SnocVect n) where
  foldr f z = foldr f z . (<>> [])

  foldl f z xs = h xs where
    h : SnocVect k elem -> acc
    h Lin = z
    h (xs :< x) = f (h xs) x

  null Lin      = True
  null (_ :< _) = False

  toList = toList . (<>> [])

  foldMap f = foldl (\xs, x => xs <+> f x) neutral

public export
{k : Nat} -> Applicative (SnocVect k) where
  pure = replicate _
  fs <*> sx = zipWith apply fs sx

||| Get diagonal elements
public export
diag : SnocVect len (SnocVect len elem) -> SnocVect len elem
diag [<]             = [<]
diag (ssx :< (sx :< x)) = diag (map liat ssx) :< x

||| This monad is different from the List monad, (>>=)
||| uses the diagonal.
public export
{k : Nat} -> Monad (SnocVect k) where
  sx >>= f = diag (map f sx)

public export
Traversable (SnocVect k) where
  traverse _ Lin = pure Lin
  traverse f (xs :< x) = [| traverse f xs :< f x |]

||| Check if something is a member of a snoc-vect using the default Boolean equality.
public export
elem : Eq a => a -> SnocVect k a -> Bool
elem x Lin = False
elem x (sx :< y) = x == y || elem x sx

||| Find the first element of the snoc-vect that satisfies the predicate.
public export
find : (a -> Bool) -> SnocVect k a -> Maybe a
find p Lin = Nothing
find p (xs :< x) = if p x then Just x else find p xs

||| Satisfiable if `k` is a valid index into `xs`.
|||
||| @ k  the potential index
||| @ xs the snoc-list into which k may be an index
public export
data InBounds : (k : Nat) -> (xs : SnocVect j a) -> Type where
    ||| Z is a valid index into any cons cell
    InFirst : InBounds Z (xs :< x)
    ||| Valid indices can be extended
    InLater : InBounds k xs -> InBounds (S k) (xs :< x)

||| Find the index and proof of InBounds of the first element (if exists) of a
||| snoc-list that satisfies the given test, else `Nothing`.
public export
findIndex : (a -> Bool) -> (sx : SnocVect k a) -> Maybe $ Fin (length sx)
findIndex _ Lin = Nothing
findIndex p (xs :< x) = if p x
  then Just FZ
  else FS <$> findIndex p xs

max_stars_repo_name: mattpolzin/idris-snocvect

max_issues_repo_name: mattpolzin/idris-snocvect

max_forks_repo_name: mattpolzin/idris-snocvect


text:
module System.File.Error

import System.Errno

import System.File.Support
import public System.File.Types

%default total

%foreign support "idris2_fileError"
         "node:lambda:x=>(x===1?1:0)"
prim__error : FilePtr -> PrimIO Int

%foreign support "idris2_fileErrno"
         "node:support:fileErrno,support_system_file"
prim__fileErrno : PrimIO Int

||| The types of errors that can occur during file operations.
public export
data FileError = ||| A generic error with an errno
                 GenericFileError Int
               | FileReadError
               | FileWriteError
               | FileNotFound
               | PermissionDenied
               | FileExists

||| Return the `FileError` corresponding to the errno that was set when the
||| function call before this one errored.
export
returnError : HasIO io => io (Either FileError a)
returnError
    = do err <- primIO prim__fileErrno
         pure $ Left $
           case err of
              0 => FileReadError
              1 => FileWriteError
              2 => FileNotFound
              3 => PermissionDenied
              4 => FileExists
              _ => GenericFileError (err-5)

export
Show FileError where
  show (GenericFileError errno) = strerror errno
  show FileReadError = "File Read Error"
  show FileWriteError = "File Write Error"
  show FileNotFound = "File Not Found"
  show PermissionDenied = "Permission Denied"
  show FileExists = "File Exists"

||| Check if the error indicator for the given file handle is set.
export
fileError : HasIO io => File -> io Bool
fileError (FHandle f)
    = do x <- primIO $ prim__error f
         pure (x /= 0)


text:
module Circuits.Idealised.Main

import System
import System.File

import Circuits.Idealised.Core
import Circuits.Idealised
import Circuits.Idealised.Pretty

idealised : (fname : String)
                  -> Idealised ()

idealised fname
  = do putStrLn "// LOG : Starting Idealised Linear"

       ast <- fromFile fname

       log "// LOG : Parsing Successful"

       term <- Design.check ast

       log "// LOG : Type Checking Complete"

       prf <- isSound term

       log "// LOG : Soundness Check Complete"

       putStrLn ((showGraph . fst . getGraph) prf)

       log "// LOG : BYE"

main : IO ()
main
  = do fname <- processArgs !getArgs
       run (idealised fname)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module Inigo.Package.PackageDhall

import Data.List
import Data.Maybe
import Extra.Either
import Extra.List
import Extra.String
import Fmt
import public Inigo.Package.ExtraDep
import Inigo.Package.Package
import Inigo.Package.ParseHelpers
import Inigo.Paths
import Inigo.PkgTree
import Inigo.Async.Promise
import SemVar
import System.Path
import Toml

import Idrall.API.V2
import Idrall.Parser
import Idrall.APIv1

import Language.Reflection
%language ElabReflection

record GitDep where
  constructor MkGitDep
  commit : String
  url : String
  subDirs : List String
%runElab (deriveFromDhall Record `{ GitDep })

Show GitDep where
  show (MkGitDep commit url subDirs) =
    "MkGitDep \{show commit} \{show url} \{show subDirs}"

gitDepDhallType : String
gitDepDhallType =
  "{ commit : Text, url : Text, subDirs : List Text }"

record DepPackage where
  constructor MkDepPackage
  ns : String
  name : String
  requirement : String
%runElab (deriveFromDhall Record `{ DepPackage })

Show DepPackage where
  show (MkDepPackage ns name requirement) =
    "{ ns = \{show ns}, name = \{show name}, requirement = \{show requirement} }"

public export
record PackageDhall where
  constructor MkPackageDhall
  depends : List String
  deps : List (DepPackage)
  description : Maybe String
  devDeps : List (DepPackage)
  executable : Maybe String
  license : Maybe String
  link : Maybe String
  main : Maybe String
  modules : List String
  ns : String
  package : String
  readme : Maybe String
  sourcedir : String
  version : String
  localDeps : List String
  gitDeps : List GitDep
%runElab (deriveFromDhall Record `{ PackageDhall })

depPackageDhallType : String
depPackageDhallType = "{ name : Text, ns : Text, requirement : Text }"

Show PackageDhall where
  show (MkPackageDhall {depends, deps, description, devDeps, executable, license, link, main, modules, ns, package, readme, sourcedir, version, localDeps, gitDeps}) =
    """
    { depends = \{show depends} : List Text
    , deps = \{show deps} : List \{ depPackageDhallType }
    , description = \{show description}
    , devDeps = \{show devDeps}
    , executable = \{show executable}
    , license = \{show license}
    , link = \{show link}
    , main = \{show main}
    , modules = \{show modules}
    , ns = \{show ns}
    , package = \{show package}
    , readme = \{show readme}
    , sourcedir = \{show sourcedir}
    , version = \{show version}
    , localDeps =
      \{show localDeps} : List String
    , gitDeps =
      \{show gitDeps} : List String
    }
    """

parsePackageDhall' : String -> IO $ Either String PackageDhall
parsePackageDhall' path = do
  Right package <- liftIOEither $ deriveFromDhallString {ty=PackageDhall} path
    | Left err => do
        pure $ Left $ show err
  pure $ Right package

inigoPackageFromDhall : PackageDhall -> Either String Package
inigoPackageFromDhall (MkPackageDhall {depends, deps, description, devDeps, executable, license, link, main, modules, ns, package, readme, sourcedir, version, localDeps, gitDeps}) =
  let packageVersion = !(versionFromDhall version)
      packageDeps = !(traverse depFromDhall deps)
      packageDevDeps = !(traverse depFromDhall devDeps)
      packageExtraDepsFromLocal = MkExtraDep SubDir () "." localDeps
      packageExtraDepsFromGit = map extraDepFromGit gitDeps
  in
  pure $ MkPackage
    { ns=ns
    , package=package
    , version=packageVersion
    , description=description
    , link=link
    , readme=readme
    , modules=modules
    , depends=depends
    , license=license
    , sourcedir=sourcedir
    , main=main
    , executable=executable
    , deps=packageDeps
    , devDeps=packageDevDeps
    , extraDeps=packageExtraDepsFromLocal :: packageExtraDepsFromGit
    }
  where
    requirementFromDhall : String -> Either String Requirement
    requirementFromDhall x =
      case parseRequirement x of
           Nothing => Left "Error parsing Requirement"
           (Just r) => pure r
    versionFromDhall : String -> Either String Version
    versionFromDhall x =
      case parseVersion x of
           Nothing => Left "Error parsing Version"
           (Just v) => pure v
    extraDepFromGit : GitDep -> ExtraDep
    extraDepFromGit (MkGitDep commit url subDirs) =
      MkExtraDep Git commit url subDirs
    depFromDhall : DepPackage -> Either String (List String, Requirement)
    depFromDhall (MkDepPackage ns name requirement) =
      pure ([ns, name], !(requirementFromDhall requirement))

export
parsePackageDhall : String -> Promise $ Either String Package
parsePackageDhall x = do
  Right package <- liftIO $ parsePackageDhall' x | Left err => pure $ Left err
  pure $ inigoPackageFromDhall package

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module IdrisJvm.Effects

import Effects
import Effect.System
import Effect.StdIO
import IdrisJvm.IO
import IdrisJvm.System
import Java.Util.Concurrent

%access export

Handler StdIO JVM_IO where
  handle () (PutStr s) k = do putStr' s; k () ()
  handle () GetStr     k = do x <- getLine'; k x ()
  handle () (PutCh c)  k = do putCh c; k () ()
  handle () GetCh      k = do x <- getCh; k x ()

implementation Handler System JVM_IO where
    handle () Args k = do x <- getArgs; k x ()
    handle () Time k = do x <- time; k x ()
    handle () (GetEnv s) k = do x <- getEnv s; k x ()
    handle () (CSystem s) k = do x <- system s; k x ()
    handle () (Usleep timeout _) k = do
      sleep microseconds $ prim__truncInt_B64 timeout
      k () ()


text:
module IntegerOrdering

-- Note that unlike (=) the types do not inherently need to be ambiguous
class OrdRel A where
	LT : A -> A -> Type

class (OrdRel s) => DecLT s where
	decLT : (x1 : s) -> (x2 : s) -> Dec ( LT x1 x2 )

LTZero : Integer -> Type
LTZero x = Not (x = abs x)

instance OrdRel Integer where
	LT a b = LTZero (a-b)

decLTBigInt : (a : Integer) -> (b : Integer) -> Dec ( LT a b )
decLTBigInt a b = case ( decEq (a-b) (abs (a-b)) ) of
		Yes prPos => No (\false => false prPos)
		No prNeg => Yes prNeg

instance DecLT Integer where
	decLT = decLTBigInt