text:
module Effekt.CpsStaged

import Effekt.CpsUnstaged

public export
data Exp : Type -> Type where
  Lam : (Exp a -> Exp b) -> Exp (a -> b)
  App : Exp (a -> b) -> Exp a -> Exp b
  Var : String -> Exp a
  Tru : Exp Bool
  Fls : Exp Bool
  Uni : Exp ()
  Lit : Int -> Exp Int
  Add : Exp Int -> Exp Int -> Exp Int
  Sub : Exp Int -> Exp Int -> Exp Int
  Sma : Exp Int -> Exp Int -> Exp Bool
  Equ : Exp Int -> Exp Int -> Exp Bool
  Tri : Exp Int -> Exp Int -> Exp Int -> Exp (Int, Int, Int)
  Dis : Exp String -> Exp (IO ())
  Emp : Exp (List a)
  Con : Exp a -> Exp (List a) -> Exp (List a)
  Str : String -> Exp String
  Cat : Exp String -> Exp String -> Exp String
  Noh : Exp (Maybe a)
  Jus : Exp a -> Exp (Maybe a)
  Ski : Exp (IO ())
  Seq : Exp (IO ()) -> Exp (IO ()) -> Exp (IO ())
  Ite : Exp Bool -> Exp a -> Exp a -> Exp a
  Rec : (Exp (a -> b) -> Exp a -> Exp b) -> Exp (a -> b)

export
pretty : Int -> Exp a -> String
pretty s (Lam f) = "(\\x" ++ show s ++ " => " ++ pretty (s + 1) (f (Var ("x" ++ show s))) ++ ")"
pretty s (App f x) = "(" ++ pretty s f ++ " " ++ pretty s x ++ ")"
pretty s (Var x) = x
pretty s Tru = "True"
pretty s Fls = "False"
pretty s Uni = "()"
pretty s (Lit n) = show n
pretty s (Add l r) = "(" ++ pretty s l ++ " + " ++ pretty s r ++ ")"
pretty s (Sub l r) = "(" ++ pretty s l ++ " - " ++ pretty s r ++ ")"
pretty s (Sma l r) = "(" ++ pretty s l ++ " < " ++ pretty s r ++ ")"
pretty s (Equ l r) = "(" ++ pretty s l ++ " == " ++ pretty s r ++ ")"
pretty s (Tri i j k) = "(" ++ pretty s i ++ ", " ++ pretty s j ++ ", " ++ pretty s k ++ ")"
pretty s (Dis ijk) = "(putStrLn " ++ pretty s ijk ++ ")"
pretty s Emp = "[]"
pretty s (Con h t) = "(" ++ pretty s h ++ " :: " ++ pretty s t ++ ")"
pretty s (Str a) = "\"" ++ a ++ "\""
pretty s (Cat l r) = "(" ++ pretty s l ++ " ++ " ++ pretty s r ++ ")"
pretty s Noh = "Nothing"
pretty s (Jus a) = "(Just " ++ pretty s a ++ ")"
pretty s Ski = "(return ())"
pretty s (Seq l r) = "(" ++ pretty s l ++ " >> " ++ pretty s r ++ ")"
pretty s (Ite b t e) = "(if " ++ pretty s b ++ " then " ++ pretty s t ++ " else " ++ pretty s e ++ ")"
pretty s (Rec f) = "(let f" ++ show s ++ " x" ++ show (s + 1) ++ " = " ++ pretty (s + 2) (f (Var ("f" ++ show s)) (Var ("x" ++ show (s + 1)))) ++ " in f" ++ show s ++ ")"

CPS : Type -> Type -> Type
CPS r a = (Exp a -> Exp r) -> Exp r

shift0 : ((Exp a -> Exp r) -> Exp r) -> CPS r a
shift0 = id

runIn0 : CPS r a -> (Exp a -> Exp r) -> Exp r
runIn0 = id

reset0 : CPS a a -> Exp a
reset0 m = runIn0 m id

pure : Exp a -> CPS r a
pure a = \k => k a

push : (Exp a -> CPS r b) -> (Exp b -> Exp r) -> (Exp a -> Exp r)
push f k = \a => f a k

bind : CPS r a -> (Exp a -> CPS r b) -> CPS r b
bind m f = \k => m (push f k)

(>>=) : CPS r a -> (Exp a -> CPS r b) -> CPS r b
(>>=) = bind

reify : CPS r a -> Exp (Cps r a)
reify m    = (Lam $ \ k =>  m (\a => App k  a))

reflect : Exp (Cps r a) -> CPS r a
reflect m  = \k => App m  ((Lam $ \ a =>  k a))

app : CPS r (a -> Cps r b) -> CPS r a -> CPS r b
app mf ma = do
  f <- mf
  a <- ma
  reflect (App f  a)

lam : (Exp a -> CPS r b) -> CPS r (a -> Cps r b)
lam f = pure ((Lam $ \ a =>  reify (f a)))

export
example : Exp Int
example = Add (Lit 1) (reset0 (do
  x <- shift0 (\c => c (c (Lit 100)))
  pure (Add (Lit 10) x)))

resumeTwice : CPS Int (Int -> Cps Int Int)
resumeTwice = lam (\n => shift0 (\c => c (c n)))

example' : Exp Int
example' = Add (Lit 1) (reset0 (do
  x <- app resumeTwice (pure (Lit 100))
  pure ((Add (Lit 10) x))))

max_stars_repo_name: b-studios/idris-effekt

max_issues_repo_name: b-studios/idris-effekt

max_forks_repo_name: b-studios/idris-effekt


text:
||| Interface and utilities for marshalling Idris2 values from JSON
||| by using the functionality from JS.Object and Javascript's
||| internal JSON parser.
|||
||| For regular algebraic data types, implementations can automatically
||| be derived using elaborator reflection.
|||
||| Operators and functionality strongly influenced by Haskell's aeson
||| library
|||
||| Note: This should eventually be generalized for different
||| `Value` types and be moved to its own library.
module JS.JSON.FromJSON

import Data.List1
import Data.Vect
import Control.Monad.Trans
import JS.Array
import JS.Number
import JS.JSON.ToJSON
import JS.Object
import JS.Undefined
import JS.Util

import Generics.Derive

%language ElabReflection

--------------------------------------------------------------------------------
--          Types
--------------------------------------------------------------------------------

public export
data JSONPathElement = Key String | Index Bits32

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

public export
JSONPath : Type
JSONPath = List JSONPathElement

public export
JSONErr : Type
JSONErr = (JSONPath,String)

public export
Result : Type -> Type
Result = Either JSONErr

public export
Parser : Type -> Type
Parser a = Value -> Either JSONErr a

public export
orElse : Either a b -> Lazy (Either a b) -> Either a b
orElse r@(Right _) _ = r
orElse _           v = v

--------------------------------------------------------------------------------
--          Error Formatting
--------------------------------------------------------------------------------

||| Format a <http://goessner.net/articles/JsonPath/ JSONPath> as a 'String'
||| which represents the path relative to some root object.
export
formatRelativePath : JSONPath -> String
formatRelativePath path = format "" path
  where
    isIdentifierKey : List Char -> Bool
    isIdentifierKey []      = False
    isIdentifierKey (x::xs) = isAlpha x && all isAlphaNum xs

    escapeChar : Char -> String
    escapeChar '\'' = "\\'"
    escapeChar '\\' = "\\\\"
    escapeChar c    = singleton c

    escapeKey : List Char -> String
    escapeKey = fastConcat . map escapeChar

    formatKey : String -> String
    formatKey key =
      let chars = fastUnpack key
       in if isIdentifierKey chars then fastPack $ '.' :: chars
          else "['" ++ escapeKey chars ++ "']"

    format : String -> JSONPath -> String
    format pfx []                = pfx
    format pfx (Index idx :: parts) = format (pfx ++ "[" ++ show idx ++ "]") parts
    format pfx (Key key :: parts)   = format (pfx ++ formatKey key) parts

||| Format a <http://goessner.net/articles/JsonPath/ JSONPath> as a 'String',
||| representing the root object as @$@.
export
formatPath : JSONPath -> String
formatPath path = "$" ++ formatRelativePath path

||| Annotate an error message with a
||| <http://goessner.net/articles/JsonPath/ JSONPath> error location.
export
formatError : JSONPath -> String -> String
formatError path msg = "Error in " ++ formatPath path ++ ": " ++ msg

--------------------------------------------------------------------------------
--          Interface
--------------------------------------------------------------------------------

public export
interface FromJSON a  where
  fromJSON : Parser a

export
decode : FromJSON a => String -> Result a
decode s = mapFst ((Nil,) . dispErr) (parse s) >>= fromJSON

export
decodeEither : FromJSON a => String -> Either String a
decodeEither = mapFst (uncurry formatError) . decode

export
decodeMaybe : FromJSON a => String -> Maybe a
decodeMaybe = either (const Nothing) Just . decode

--------------------------------------------------------------------------------
--          Parsing Utilities
--------------------------------------------------------------------------------

typeOf : Value -> String
typeOf (Arr _)     = "Array"
typeOf (Boolean _) = "Boolean"
typeOf Null        = "Null"
typeOf (Num _)     = "Number"
typeOf (Obj _)     = "Object"
typeOf (Str _)     = "String"

export
fail : String -> Result a
fail s = Left (Nil,s)

typeMismatch : String -> Parser a
typeMismatch expected actual =
  fail $ #"expected \#{expected}, but encountered \#{typeOf actual}"#

unexpected : Parser a
unexpected actual = fail $ #"unexpected \#{typeOf actual}"#

export
modifyFailure : (String -> String) -> Result a -> Result a
modifyFailure f = mapFst (map f)

||| If the inner 'Parser' failed, prepend the given string to the failure
||| message.
export
prependFailure : String -> Result a -> Result a
prependFailure = modifyFailure . (++)

export
prependContext : String -> Result a -> Result a
prependContext name = prependFailure #"parsing \#{name} failed, "#

infixr 3 <?>, .:, .:?, .:!

export
(<?>) : Result a -> JSONPathElement -> Result a
r <?> elem = mapFst (\(path,s) => (elem :: path,s)) r

withValue :  (type : String)
          -> (Value -> Maybe v)
          -> (name : Lazy String)
          -> (v -> Result a)
          -> Parser a
withValue s get n f val = case get val of
                            Just v  => f v
                            Nothing => prependContext n $ typeMismatch s val

export
withObject : Lazy String -> (IObject -> Result a) -> Parser a
withObject = withValue "Object" getObject

export
withBool : Lazy String -> (Bool -> Result a) -> Parser a
withBool = withValue "Boolean" getBool

export
withString : Lazy String -> (String -> Result a) -> Parser a
withString = withValue "String" getStr

export
withNumber : Lazy String -> (Double -> Result a) -> Parser a
withNumber = withValue "Number" getNum

export
withInteger : Lazy String -> (Integer -> Result a) -> Parser a
withInteger s f =
  withNumber s $ \d =>
    let n = the Integer (cast d)
    in if d == fromInteger n
          then f n
          else fail #"not an integer: \#{show d}"#

export
withLargeInteger : Lazy String -> (Integer -> Result a) -> Parser a
withLargeInteger s f =
  withString s $ \str =>
    case parseInteger {a = Integer} str of
         Nothing => fail #"not an integer: \#{show str}"#
         Just n  => f n

export
boundedIntegral :  Num a
                => Lazy String
                -> (lower : Integer)
                -> (upper : Integer)
                -> Parser a
boundedIntegral s lo up =
  withInteger s $ \n =>
    if n >= lo && n <= up
       then pure $ fromInteger n
       else fail #"integer out of bounds: \#{show n}"#

export
boundedLargeIntegral :  Num a
                     => Lazy String
                     -> (lower : Integer)
                     -> (upper : Integer)
                     -> Parser a
boundedLargeIntegral s lo up =
  withLargeInteger s $ \n =>
    if n >= lo && n <= up
       then pure $ fromInteger n
       else fail #"integer out of bounds: \#{show n}"#

export
withArray : Lazy String -> (IArray Value -> Result a) -> Parser a
withArray = withValue "Array" getArray

export
withList : Lazy String -> (List Value -> Result a) -> Parser a
withList s f = withArray s (f . arrayToList)

||| See `.:`
export
explicitParseField : Parser a -> IObject -> String -> Result a
explicitParseField p obj key =
  case valueAt obj key of
       Nothing => fail #"key \#{show key} not found"#
       Just v  => p v <?> Key key

||| See `.:?`
export
explicitParseFieldMaybe : Parser a -> IObject -> String -> Result (Maybe a)
explicitParseFieldMaybe p obj key =
  case valueAt obj key of
       Nothing   => Right Nothing
       Just Null => Right Nothing
       Just v    => Just <$> p v <?> Key key

||| See `.:!`
export
explicitParseFieldMaybe' : Parser a -> IObject -> String -> Result (Maybe a)
explicitParseFieldMaybe' p obj key =
  case valueAt obj key of
       Nothing   => Right Nothing
       Just v    => Just <$> p v <?> Key key

||| Retrieve the value associated with the given key of an `IObject`.
||| The result is `empty` if the key is not present or the value cannot
||| be converted to the desired type.
|||
||| This accessor is appropriate if the key and value /must/ be present
||| in an object for it to be valid.  If the key and value are
||| optional, use `.:?` instead.
export
(.:) : FromJSON a => IObject -> String -> Result a
(.:) = explicitParseField fromJSON

||| Retrieve the value associated with the given key of an `IObject`. The
||| result is `Nothing` if the key is not present or if its value is `Null`,
||| or `empty` if the value cannot be converted to the desired type.
|||
||| This accessor is most useful if the key and value can be absent
||| from an object without affecting its validity.  If the key and
||| value are mandatory, use `.:` instead.
export
(.:?) : FromJSON a => IObject -> String -> Result (Maybe a)
(.:?) = explicitParseFieldMaybe fromJSON

||| Retrieve the value associated with the given key of an `IObject`
||| The result is `Nothing` if the key is not present or 'empty' if the
||| value cannot be converted to the desired type.
|||
||| This differs from `.:?` by attempting to parse `Null` the same as any
||| other JSON value, instead of interpreting it as `Nothing`.
export
(.:!) : FromJSON a => IObject -> String -> Result (Maybe a)
(.:!) = explicitParseFieldMaybe' fromJSON

||| Function variant of `.:`.
export
parseField : FromJSON a => IObject -> String -> Result a
parseField = (.:)

||| Function variant of `.:?`.
export
parseFieldMaybe : FromJSON a => IObject -> String -> Result (Maybe a)
parseFieldMaybe = (.:?)

||| Function variant of `.:!`.
export
parseFieldMaybe' : FromJSON a => IObject -> String -> Result (Maybe a)
parseFieldMaybe' = (.:!)

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

export
FromJSON Void where
  fromJSON v = fail "Cannot parse Void"

export
FromJSON () where
  fromJSON = withList "()" $
    \case Nil    => pure ()
          _ :: _ => fail "parsing () failed, expected empty list"

export
FromJSON Bool where
  fromJSON = withBool "Bool" pure

export
FromJSON Double where
  fromJSON = withNumber "Double" pure

export
FromJSON Bits8 where
  fromJSON = boundedIntegral "Bits8" 0 0xff

export
FromJSON Bits16 where
  fromJSON = boundedIntegral "Bits16" 0 0xffff

export
FromJSON Bits32 where
  fromJSON = boundedIntegral "Bits32" 0 0xffffffff

export
FromJSON Bits64 where
  fromJSON = boundedLargeIntegral "Bits64" 0 0xffffffffffffffff

export
FromJSON Int8 where
  fromJSON = boundedIntegral "Int8" (-0x80) 0x7f

export
FromJSON Int16 where
  fromJSON = boundedIntegral "Int16" (-0x8000) 0x7fff

export
FromJSON Int32 where
  fromJSON = boundedIntegral "Int32" (-0x80000000) 0x7fffffff

export
FromJSON Int64 where
  fromJSON = boundedIntegral "Int64" (-0x8000000000000000) 0x7fffffffffffffff

export
FromJSON Int where
  fromJSON = boundedLargeIntegral "Int" (-0x8000000000000000) 0x7fffffffffffffff

export
FromJSON Nat where
  fromJSON = withLargeInteger "Nat" $ \n =>
    if n >= 0 then pure $ fromInteger n
    else fail #"not a natural number: \#{show n}"#

export
FromJSON Integer where
  fromJSON = withLargeInteger "Integer" pure

export
FromJSON String where
  fromJSON = withString "String" pure

export
FromJSON Char where
  fromJSON = withString "Char" $
    \str => case strM str of
                 (StrCons c "") => pure c
                 _ => fail "expected a string of length 1"

export
FromJSON a => FromJSON (Maybe a) where
  fromJSON Null = pure Nothing
  fromJSON v    = Just <$> fromJSON v

export
FromJSON a => FromJSON (Optional a) where
  fromJSON = map maybeToOptional . fromJSON

export
FromJSON a => FromJSON (List a) where
  fromJSON = withList "List" $ traverse fromJSON

export
FromJSON a => FromJSON (IArray a) where
  fromJSON = withArray "IArray" $ traverse fromJSON

export
FromJSON a => FromJSON (List1 a) where
  fromJSON = withList "List1" $
    \case Nil    => fail #"expected non-empty list"#
          h :: t => traverse fromJSON (h ::: t)

export
{n : Nat} -> FromJSON a => FromJSON (Vect n a) where
  fromJSON = withList #"Vect \#{show n}"# $
    \vs => case toVect n vs of
                Just vect => traverse fromJSON vect
                Nothing   => fail #"expected list of length \#{show n}"#

export
(FromJSON a, FromJSON b) => FromJSON (Either a b) where
  fromJSON = withObject "Either" $ \o =>
               map Left (o .: "Left") `orElse` map Right (o .: "Right")

--------------------------------------------------------------------------------
--          SOP Implementations
--------------------------------------------------------------------------------

-- TODO: This should go as a utility to idris2-sop
size : NP f ks -> Nat
size []        = 0
size (_ :: vs) = size vs + 1

-- TODO: This should go (in sligthly modified form) as a utility to idris2-sop
values : Nat -> NP f ks -> List Value -> Result (NP (K Value) ks)
values n [] []              = pure []
values n [] (_ :: _)        = fail #"expected array of \#{show n} values"#
values n (_ :: _) []        = fail #"expected array of \#{show n} values"#
values n (_ :: t) (v :: vs) = (v ::) <$> values n t vs

np : (all : NP (FromJSON . f) ks) => List Value -> Result (NP f ks)
np vs = do npVS <- values (size all) all vs
           hctraverse (FromJSON . f) fromJSON npVS

export
NP (FromJSON . f) ks => FromJSON (NP f ks) where
  fromJSON = withList "NP" np

export
(FromJSON a, FromJSON b) => FromJSON (a,b) where
  fromJSON = map (\[x,y] => (x,y)) . fromJSON {a = NP I [a,b] }

-- TODO: This should go as a utility to idris2-sop
inj : NP g ks -> NP (Injection f ks) ks
inj []       = []
inj (_ :: t) = Z :: mapNP (S .) (inj t)

ns : (all : NP (FromJSON . f) ks) => Parser (NS f ks)
ns = withObject "NS" $ getFirst
                     $ hcliftA2 (FromJSON . f) parse (inj all) (indices all)
  where getFirst :  NP (K (IObject -> Result (NS f ks))) ts
                 -> IObject
                 -> Result (NS f ks)
        getFirst []        _ = fail #"Can't parse nullary sum"#
        getFirst (f :: []) o = f o
        getFirst (f :: fs) o = f o `orElse` getFirst fs o

        parse : FromJSON (f a) =>
                (f a -> NS f ks) -> Bits32 -> IObject -> Result (NS f ks)
        parse f ix o = map f (o .: show ix)

export
NP (FromJSON . f) ks => FromJSON (NS f ks) where
  fromJSON = ns

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

fromJSONC1 : NP (FromJSON . f) ks => ConInfo ks -> Parser (NP f ks)
fromJSONC1 info = maybe fromJSON decRecord (argNames info)
  where decRecord : NP (K String) ks -> Parser (NP f ks)
        decRecord names = withObject info.conName $ \o =>
                            hctraverse (FromJSON . f) (parseField o) names

fromJSONSOP1 : NP (FromJSON . f) ks => TypeInfo [ks] -> Parser (SOP f [ks])
fromJSONSOP1 (MkTypeInfo _ n (i :: [])) v =
  map (MkSOP . Z) (fromJSONC1 i v) <?> Key n
fromJSONSOP1 (MkTypeInfo _ _ (_ :: _ :: _)) impossible
fromJSONSOP1 (MkTypeInfo _ _ []) impossible

fromJSONC :  NP (FromJSON . f) ks
          => (typeName : String)
          -> ConInfo ks
          -> Parser (NP f ks)
fromJSONC tn i@(MkConInfo _ n _) =
  withObject tn $ \o => explicitParseField (fromJSONC1 i) o n

fromJSONSOP :  (all : POP_ k (FromJSON . f) kss)
            => TypeInfo kss -> Parser (SOP_ k f kss)
fromJSONSOP {all = MkPOP nps} (MkTypeInfo _ tn cons) =
  getFirst $ hcliftA2 (NP $ FromJSON . f) parse (injSOP nps) cons
  where getFirst :  NP_ (List k) (K (Parser (SOP_ k f kss))) tss -> Parser (SOP_ k f kss)
        getFirst []        _ = fail #"Can't parse nullary sum"#
        getFirst (f :: []) v = f v
        getFirst (f :: fs) v = f v `orElse` getFirst fs v

        -- TODO: This should go as a utility to idris2-sop
        injSOP : NP_ (List k) g tss -> NP_ (List k) (InjectionSOP f tss) tss
        injSOP np = hmap (MkSOP .) $ inj {ks = tss} np

        parse :  NP_ k (FromJSON . f) ts
              => (NP_ k f ts -> SOP_ k f kss)
              -> ConInfo_ k ts
              -> Parser (SOP_ k f kss)
        parse f c = map f . fromJSONC tn c

export
genFromJSON1 : Meta a [ks] => NP FromJSON ks => Parser a
genFromJSON1 = map to . fromJSONSOP1 (metaFor a)

export
genFromJSON : Meta a code => POP FromJSON code => Parser a
genFromJSON = map to . fromJSONSOP (metaFor a)

public export
mkFromJSON : (fromJSON : Parser a) -> FromJSON a
mkFromJSON = %runElab check (var $ singleCon "FromJSON")

namespace Derive

  ||| Derives a `FromJSON` implementation for the given data type
  export
  FromJSON : DeriveUtil -> InterfaceImpl
  FromJSON g = MkInterfaceImpl "FromJSON" Export []
                    `(mkFromJSON genFromJSON)
                    (implementationType `(FromJSON) g)

  ||| Derives a `FromJSON` implementation for the given single-constructor
  ||| data type
  export
  FromJSON1 : DeriveUtil -> InterfaceImpl
  FromJSON1 g = MkInterfaceImpl "FromJSON" Export []
                    `(mkFromJSON genFromJSON1)
                    (implementationType `(FromJSON) g)

ext: idr


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

import Effect.Default

import ArgParse

import Sif.Types

import Effect.Logging.Level

%access export
-- ----------------------------------------------------------------- [ Options ]

public export
data SifMode = Eval | Check | Conv | REPL | VERS | HELP

Show SifMode where
  show Eval  = "Eval"
  show Check = "Check"
  show Conv  = "Conv"
  show REPL  = "REPL"
  show VERS  = "VERSION"
  show HELP  = "HELP"

Eq SifMode where
  (==) Eval  Eval  = True
  (==) Check Check = True
  (==) Conv  Conv  = True
  (==) REPL  REPL  = True
  (==) VERS  VERS  = True
  (==) HELP  HELP  = True
  (==) _     _     = False

public export
record SifOpts where
  constructor MkSOpts
  pSpec      : Maybe String
  sSpec      : Maybe String
  mode       : Maybe SifMode
  out        : Maybe String
  to         : Maybe SifOutFormat
  prelude    : Maybe String
  banner     : Bool
  loglvl     : LogLevel n
  backend    : Maybe String
  perf       : Pair Bool Bool

defOpts : SifOpts
defOpts = MkSOpts
    Nothing Nothing (Just REPL) Nothing Nothing Nothing
    True OFF (Just "interp") (MkPair False False)

Default SifOpts where
  default = defOpts

strToLog : String -> (n ** LogLevel n)
strToLog s =
  case s of
    "1" => (_ ** TRACE)
    "2" => (_ ** DEBUG)
    "3" => (_ ** INFO)
    "4" => (_ ** WARN)
    "5" => (_ ** FATAL)
    "6" => (_ ** ERROR)
    "trace"   => (_ ** TRACE)
    "debug"   => (_ ** DEBUG)
    "info"    => (_ ** INFO)
    "warn"    => (_ ** WARN)
    "fatal"   => (_ ** FATAL)
    "error"   => (_ ** ERROR)
    "all"     => (_ ** ALL)
    otherwise => (_ ** OFF)

convOpts : Arg -> SifOpts -> Maybe SifOpts
convOpts (Files xs)     o = Nothing
convOpts (KeyValue k v) o =
  case k of
    "prelude"    => Just $ record {prelude = Just v}           o
    "problem"    => Just $ record {pSpec   = Just v}           o
    "solution"   => Just $ record {sSpec   = Just v}           o
    "out"        => Just $ record {out     = Just v}           o
    "to"         => Just $ record {to      = readOutFMT v}     o
    "log"        => Just $ record {loglvl  = snd $ strToLog v} o
    "backend"    => Just $ record {backend = Just v}           o
    otherwise    => Nothing
convOpts (Flag x) o =
  case x of
    "help"     => Just $ record {mode   = Just HELP}         o
    "version"  => Just $ record {mode   = Just VERS}         o
    "check"    => Just $ record {mode   = Just Check}        o
    "eval"     => Just $ record {mode   = Just Eval}         o
    "conv"     => Just $ record {mode   = Just Conv}         o
    "nobanner" => Just $ record {banner = False}             o
    "logtrace" => Just $ record {loglvl = TRACE}             o
    "logdebug" => Just $ record {loglvl = DEBUG}             o
    "loginfo"  => Just $ record {loglvl = INFO}              o
    "logwarn"  => Just $ record {loglvl = WARN}              o
    "logfatal" => Just $ record {loglvl = FATAL}             o
    "logerror" => Just $ record {loglvl = ERROR}             o
    "logall"   => Just $ record {loglvl = ALL}               o
    "perf"     => Just $ record {perf   = MkPair True True}  o
    "sperf"    => Just $ record {perf   = MkPair True False} o
    otherwise => Nothing

helpStr : String
helpStr = """Sif-Lang (C) Jan de Muijnck-Hughes 2015

Available Options:

Flag                 | Description
---------------------|----------------------------------------------------------
--prelude="<dir>"    | Load an externally defined prelude.
--problem="<fname>"  | A problem specification.
--solution="<fname"  | A solution specification.
--out="<fname>"      | File name to save things to.
--to="<fmt>"         | The output format.
--log="<num|word>"   | Set logging levels
                     | [1,     2,     3,    4,    5,     6]
                     | [trace, debug, info, warn, fatal, error]
--perf               | Collect and show performance metrics
--sperf              | Collect but *not* show performance metrics
--backend="<naam>"   | Change meta-model [interp|direct]
--help               | Display help
--version            | Display version
--check              | Check problem solution pairing.
--eval               | Evaluate problem solution pairing
--conv               | Convert problem solution pairing
--nobanner           | Don't display banner

--logtrace, --logdebug, --loginfo, --logwarn, --logfatal, --logerror
"""

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
||| Spec: http://webassembly.github.io/spec/core/syntax/types.html#value-types
module WebAssembly.Structure.Types.ValueTypes

import Decidable.Equality

-- Definition

public export
data ValType : Type where
  TI32 : ValType
  TI64 : ValType
  TF32 : ValType
  TF64 : ValType

-- Equality

total public export
lemma_ti32_not_ti64 : (TI32 = TI64) -> Void
lemma_ti32_not_ti64 Refl impossible

total public export
lemma_ti32_not_tf32 : (TI32 = TF32) -> Void
lemma_ti32_not_tf32 Refl impossible

total public export
lemma_ti32_not_tf64 : (TI32 = TF64) -> Void
lemma_ti32_not_tf64 Refl impossible

total public export
lemma_ti64_not_ti32 : (TI64 = TI32) -> Void
lemma_ti64_not_ti32 Refl impossible

total public export
lemma_ti64_not_tf32 : (TI64 = TF32) -> Void
lemma_ti64_not_tf32 Refl impossible

total public export
lemma_ti64_not_tf64 : (TI64 = TF64) -> Void
lemma_ti64_not_tf64 Refl impossible

total public export
lemma_tf32_not_ti32 : (TF32 = TI32) -> Void
lemma_tf32_not_ti32 Refl impossible

total public export
lemma_tf32_not_ti64 : (TF32 = TI64) -> Void
lemma_tf32_not_ti64 Refl impossible

total public export
lemma_tf32_not_tf64 : (TF32 = TF64) -> Void
lemma_tf32_not_tf64 Refl impossible

total public export
lemma_tf64_not_ti32 : (TF64 = TI32) -> Void
lemma_tf64_not_ti32 Refl impossible

total public export
lemma_tf64_not_ti64 : (TF64 = TI64) -> Void
lemma_tf64_not_ti64 Refl impossible

total public export
lemma_tf64_not_tf32 : (TF64 = TF32) -> Void
lemma_tf64_not_tf32 Refl impossible

-- Decidable Equality

public export
implementation DecEq ValType where
  decEq TI32 TI32 = Yes Refl
  decEq TI32 TI64 = No lemma_ti32_not_ti64
  decEq TI32 TF32 = No lemma_ti32_not_tf32
  decEq TI32 TF64 = No lemma_ti32_not_tf64
  decEq TI64 TI32 = No lemma_ti64_not_ti32
  decEq TI64 TI64 = Yes Refl
  decEq TI64 TF32 = No lemma_ti64_not_tf32
  decEq TI64 TF64 = No lemma_ti64_not_tf64
  decEq TF32 TI32 = No lemma_tf32_not_ti32
  decEq TF32 TI64 = No lemma_tf32_not_ti64
  decEq TF32 TF32 = Yes Refl
  decEq TF32 TF64 = No lemma_tf32_not_tf64
  decEq TF64 TI32 = No lemma_tf64_not_ti32
  decEq TF64 TI64 = No lemma_tf64_not_ti64
  decEq TF64 TF32 = No lemma_tf64_not_tf32
  decEq TF64 TF64 = Yes Refl

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module MonadicMemo

-- Monadic memoization, based on http://www.cs.utexas.edu/~wcook/Drafts/2006/MemoMixins.pdf

import Control.Monad.Identity
import Control.Monad.State
import Data.SortedMap

Gen : Type -> Type
Gen a = a -> a

gmFib : Monad m => Gen (Int -> m Int)
gmFib f 0 = pure 0
gmFib f 1 = pure 1
gmFib f n = do nm1 <- f (n - 1)
               nm2 <- f (n - 2)
               pure (nm1 + nm2)

fix : ((a -> b) -> (a -> b)) -> a -> b
fix f x = f (fix f) x

testIden : Int -> Int
testIden = runIdentity . (fix gmFib)

memo : MonadState (SortedMap a b) (StateT (SortedMap a b) m) => Gen (a -> StateT (SortedMap a b) m b)
memo f x = do map <- get
              apply map f x
  where
    apply : MonadState (SortedMap a b) (StateT (SortedMap a b) m) => SortedMap a b -> Gen (a -> StateT (SortedMap a b) m b)
    apply map f x with (lookup x map)
      apply map f x | Nothing = do y <- f x
                                   put (insert x y map)
                                   pure y
      apply map f x | (Just y) = pure y

testMemo : Int -> Int
testMemo x = fst . runIdentity $ runStateT (getState x) empty
  where
      getState : Int -> StateT (SortedMap Int Int) Identity Int
      getState x = fix (memo . gmFib) x

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Lambdapants.Term.Reduction

import Lambdapants.Term

%default total

public export
data Strategy = Normal | Applicative

export
Eq Strategy where
  Normal      == Normal      = True
  Applicative == Applicative = True
  _           == _           = False

export
Show Strategy where
  show Normal      = "Normal"
  show Applicative = "Applicative"

rename : String -> String -> Term -> Term
rename fr to = translate where
  translate (Var v)     = Var (if v == fr then to else v)
  translate (App e1 e2) = App (translate e1) (translate e2)
  translate (Lam x e)   = Lam (if x == fr then to else x) (translate e)

nextSuffix : List String -> Nat
nextSuffix xs = case last' (sort (map trailingDigits xs)) of
                     Nothing => 0
                     Just x => succ (cast x)
where
  trailingDigits : String -> String
  trailingDigits = reverse . pack . takeWhile isDigit . unpack . reverse

export
substitute : String -> Term -> Term -> Term
substitute var expr = translate . sanitized where
  vars : List String
  vars = freeVars expr
  suffix : String
  suffix = "_" ++ show (nextSuffix vars)
  sanitized : Term -> Term
  sanitized (Var v)     = Var v
  sanitized (App e1 e2) = App (sanitized e1) (sanitized e2)
  sanitized (Lam x e)   = if elem x vars
                             then let x' = x ++ suffix in
                                      Lam x' (rename x x' (sanitized e))
                             else Lam x (sanitized e)
  translate : Term -> Term
  translate (Var v)     = if var == v then expr else Var v
  translate (App e1 e2) = App (translate e1) (translate e2)
  translate (Lam x e)   = Lam x (if x == var then e else translate e)

export
normal : Term -> Bool
normal (App (Lam _ _) _) = False
normal (App e1 e2)       = normal e1 && normal e2
normal (Lam _ e)         = normal e
normal _                 = True

export
whnf : Term -> Bool
whnf (App e1 _) = case e1 of
                       Lam _ _   => False
                       otherwise => whnf e1
whnf _          = True

export
cbn : Term -> Term
cbn (Var x)            = Var x
cbn (Lam x e)          = Lam x e
cbn (App (Lam x e) e2) = substitute x e2 e
cbn (App e1 e2)        = App (cbn e1) e2

export
nor : Term -> Term
nor (Var x)            = Var x
nor (Lam x e)          = Lam x (nor e)
nor (App (Lam x e) e2) = substitute x e2 e
nor (App e1 e2)        = if normal e1 then App e1 (nor e2) else App (nor e1) e2

export
aor : Term -> Term
aor (Var x)   = Var x
aor (Lam x e) = Lam x (aor e)
aor (App e1 e2) with (normal e2)
  | False = App e1 (aor e2)
  | True  = case e1 of
                 Lam x e   => substitute x e2 e
                 otherwise => App (aor e1) e2

export
evaluate : Strategy -> Term -> Term
evaluate Normal      = nor
evaluate Applicative = aor

export
stream : Strategy -> Term -> Stream Term
stream strategy = iterate (evaluate strategy)

max_stars_repo_name: laserpants/redex-reflex

max_issues_repo_name: laserpants/lambdapants

max_forks_repo_name: laserpants/lambdapants


text:
module Ordinals

data Ord : Type where
  Zero : Ord
  Suc  : (x : Ord) -> Ord
  Lim  : (f : Nat -> Ord) -> Ord

(+) : Ord -> Ord -> Ord
(+) Zero m = m
(+) (Suc n) m = Suc $ n + m
(+) (Lim f) m = Lim (\x => f x + m)

(*) : Ord -> Ord -> Ord
(*) Zero m = Zero
(*) (Suc n) m = n + m
(*) (Lim f) m = Lim (\x => f x * m)

exp : Ord -> Ord -> Ord
exp Zero m = Suc Zero
exp (Suc n) m = n * m
exp (Lim f) m = Lim (\x => exp (f x) m)

omega : Ord
omega = Lim rec
  where
    rec : Nat -> Ord
    rec Z = Zero
    rec (S n) = Suc $ rec n

epsilonNought : Ord
epsilonNought = Lim rec
  where
    rec : Nat -> Ord
    rec Z = omega
    rec (S n) = exp omega (rec n)


text:
module JS.Nullable

import Data.List.Elem
import JS.Inheritance
import JS.Marshall
import JS.Util

export
data Nullable : Type -> Type where [external]

%foreign "javascript:lambda:()=>null"
prim__null : AnyPtr

export
null : Nullable a
null = believe_me prim__null

export
nonNull : a -> Nullable a
nonNull = believe_me

||| Tests, whether a value of questionable origin is null
export
isNull : a -> Bool
isNull = eqv prim__null

export
maybeToNullable : Maybe a -> Nullable a
maybeToNullable = maybe null nonNull

export
mayUp : (0 _ : JSType a) => Maybe a -> {auto 0 _ : Elem b (Types a)} -> Nullable b
mayUp x = maybe null (\v => nonNull $ up v) x

export
nullableToMaybe : Nullable a -> Maybe a
nullableToMaybe v = if isNull v then Nothing else Just (believe_me v)

export
ToFFI a b => ToFFI (Maybe a) (Nullable b) where
  toFFI = maybeToNullable . map toFFI

export
FromFFI a b => FromFFI (Maybe a) (Nullable b) where
  fromFFI v = case nullableToMaybe v of
                   Nothing => Just Nothing
                   Just x  => map Just $ fromFFI x

export
SafeCast a => SafeCast (Nullable a) where
  safeCast ptr = if isNull ptr
                    then Just null
                    else map nonNull $ safeCast ptr


text:
module Main
import Data.Bits

boolToInt : Bool -> Int
boolToInt True = 1
boolToInt False = 0

main : IO ()
main = do
  putStrLn . show $ (the Int8 100) + (the Int8 50)
  putStrLn . show $ (the Int8 100) - (the Int8 50)
  putStrLn . show $ (the Int8 100) * (the Int8 50)
  putStrLn . show $ (the Int8 100) `div` (the Int8 7)
  putStrLn . show $ (the Int8 100) `mod` (the Int8 7)
  putStrLn . show $ -(the Int8 50)

  putStrLn . show $ the Int8 100 .&. the Int8 50
  putStrLn . show $ the Int8 100 .|. the Int8 50
  putStrLn . show $ the Int8 100 `xor` the Int8 50

  putStrLn . show . boolToInt $ the Int8 100 < the Int8 50
  putStrLn . show . boolToInt $ the Int8 100 <= the Int8 50
  putStrLn . show . boolToInt $ the Int8 100 == the Int8 50
  putStrLn . show . boolToInt $ the Int8 100 >= the Int8 50
  putStrLn . show . boolToInt $ the Int8 100 > the Int8 50
  -- putStrLn . show  $ the Int8 50 `shiftL` 1
  -- putStrLn . show  $ the Int8 100 `shiftR` 1

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Main

interface SomeClass a where
  stuff : a -> String

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Gspider.Main

import Data.Vect
import Data.SortedMap

import Core
import File.FrequencyFileParsing
import File.SystemLoading
import Types.AttackFrame
import Types.RestrictedCharString

import Probability.Core

||| Looks up a password probability in a sorted map.
|||
||| @probs  the list of password probabilities
||| @pwd    the password to look up
lookupEff : (probs : SortedMap (RestrictedCharString s) Double) -> (pwd : RestrictedCharString s) -> Double
lookupEff probs pwd =
  case lookup pwd probs of
    Just prob => prob
    _ => 0

||| Unzips a list of password frequency records into two lists.
|||
||| @freqs  the list of password frequencies
splitFreqRecords : (freqs : List PasswordFrequency) -> (List String, List Int)
splitFreqRecords [] = ([], [])
splitFreqRecords (x :: xs) =
  let (ps, fs) = splitFreqRecords xs in
  ((pwd x) :: ps, (freq x) :: fs)

||| Converts a system and a list of password frequency records to a distribution.
|||
||| @s      the system to convert under
||| @freqs  the frequencies to use to build the distribution
toDist : (s : System) -> (freqs : List PasswordFrequency) -> Prob (RestrictedCharString s)
toDist s [] = flat []
toDist s freqs =
  let (ps, fs) = splitFreqRecords freqs in
  shape (convertToRestricted s ps) (map cast fs)

||| Loads a password probability distribution.
|||
||| @s      the system
||| @path   the path to the frequency file
loadDist : (s : System) -> (path : String) -> IO (Maybe (Distribution s))
loadDist s path = do
  txt <- readFile path
  case txt of
    (Right txt') =>
      let rows = parseRows ':' txt'
          dist = toDist s rows
          tuples = runProb dist
      in
      pure (Just (lookupEff (fromList tuples)))
    _ => pure Nothing

||| Loads an attack.
|||
||| @s      the system
||| @path   the path to the file
loadAtt : (s : System) -> (path : String) -> IO (Maybe (List (RestrictedCharString s)))
loadAtt s path = do
  txt <- readFile path
  case txt of
    (Right txt') => pure (Just (convertToRestricted s (lines txt')))
    _ => pure Nothing

||| Initialises a probabilistic attack frame.
|||
||| @att    the attack
||| @dist   the distribution
initFrame : (att : Vect n (RestrictedCharString s)) -> (dist : Distribution s) -> AttackFrame s n 0
initFrame [] dist = Empty dist
initFrame att@(_ :: _) dist = Initial att dist

||| Runs a probabilistic attack frame to completion, printing each probability.
|||
||| @paf    the probabilistic attack frame
runFrame : (paf : AttackFrame _ _ _) -> IO ()
runFrame (Empty _) = putStrLn "Frame is empty."
runFrame paf@(Initial _ _) = do
  next <- pure (advance paf)
  putStrLn ("Frame is initial.")
  case next of
    Ongoing _ _ _ q => putStrLn (cast q)
    Terminal _ _ q => putStrLn (cast q)
  runFrame next
runFrame paf@(Ongoing _ _ _ _) = do
  next <- pure (advance paf)
  case next of
    Ongoing _ _ _ q => putStrLn (cast q)
    Terminal _ _ q => putStrLn (cast q)
  runFrame next
runFrame (Terminal _ _ _) = putStrLn "Frame is terminal."

main : IO ()
main = do
  [_, arg_sys, arg_dist, arg_att] <- getArgs -- TODO: Bind alternatives!
  Just s <- loadSystem arg_sys | Nothing => putStrLn "Error: Could not load system."
  Just dist <- loadDist s arg_dist | Nothing => putStrLn "Error: Could not load distribution."
  Just att <- loadAtt s arg_att | Nothing => putStrLn "Error: Could not load attack."
  let frame = initFrame (fromList att) dist -- Initialise probabilistic attack frame.
  runFrame frame -- Run PAF to completion.

max_stars_repo_name: sr-lab/gspider

max_issues_repo_name: sr-lab/gspider

max_forks_repo_name: sr-lab/gspider


text:
module WebAssembly.Structure.Types

import public WebAssembly.Structure.Types.ValueTypes
import public WebAssembly.Structure.Types.ResultTypes
import public WebAssembly.Structure.Types.FunctionTypes
import public WebAssembly.Structure.Types.Limits
import public WebAssembly.Structure.Types.MemoryTypes
import public WebAssembly.Structure.Types.TableTypes
import public WebAssembly.Structure.Types.GlobalTypes
import public WebAssembly.Structure.Types.ExternalTypes


text:
module MiniForth

data IxList : {i  : Type} -> (rel : i -> i -> Type) -> i -> i -> Type where
  Nil : IxList rel i i
  (::) : rel i j -> IxList rel j k -> IxList rel i k

data Instr : Nat -> Nat -> Type where
  Lit : Int -> Instr n (S n)
  Dup : Instr (S n) (S (S n))
  Swap : Instr (S (S n)) (S (S n))
  Drop : Instr (S n) n
  Over : Instr (S (S n)) (S (S (S n)))
  Op : (Int -> Int -> Int) -> Instr (S (S n)) (S n)

data Val : Nat -> Nat -> Type where
  ValC : Int -> Val (S n) n

run : IxList Instr i j -> IxList Val i 0 -> IxList Val j 0
run [] st = st
run ((Lit x) :: xs) st = run xs (ValC x :: st)
run (Dup :: xs) ((ValC x) :: st) = run xs (ValC x :: ValC x :: st)
run (Swap :: _) ((ValC _) :: []) impossible
run (Swap :: xs) ((ValC x) :: ((ValC y) :: st)) = run xs (ValC y :: ValC x :: st)
run (Drop :: xs) ((ValC x) :: st) = run xs st
run (Over :: _) ((ValC _) :: []) impossible
run (Over :: xs) ((ValC x) :: (ValC y) :: st) = run xs ((ValC y) :: (ValC x) :: (ValC y) :: st)
run (Op _ :: _) ((ValC _) :: []) impossible
run (Op f :: xs) ((ValC x) :: ((ValC y) :: st)) = run xs (ValC (f x y) :: st)

square : IxList Instr (S n) (S n)
square = Dup :: Op (*) :: Nil

prg : IxList Instr 0 1
prg = Lit 5 :: square

test : run MiniForth.prg [] = [ValC 25]
test = Refl


text:
%flag C "-I/usr/local/Cellar/glfw3/3.1.1/include "
%flag C "-L/usr/local/Cellar/glfw3/3.1.1/lib -lglfw3 "

max_stars_repo_name: eckart/glfw-idris

max_issues_repo_name: eckart/glfw-idris

max_forks_repo_name: eckart/glfw-idris


text:
module Main

import Effects
import Effect.Process
import Effect.StdIO

myProcessOne : RunningProcess String IO [STDIO]
myProcessOne = do
  msg <- recvMessage
  putStr $ "Consumer process received message: " ++ msg ++ "\n"
  myProcessOne

myProcessTwo : ProcPID String -> Nat -> { [PROCESS (Running String)] } Eff IO ()
myProcessTwo _ Z = return ()
myProcessTwo pid (S k) = do
  sendMessage pid (show k)
  myProcessTwo pid k

setupProcesses : { [PROCESS (Running String), STDIO] } Eff IO ()
setupProcesses = do
  pid_one <- spawn String myProcessOne [()]
  myProcessTwo pid_one 10
  return ()

main : IO ()
main = do runInit [initProcess, ()] setupProcesses
          getLine
          return ()


text:
module Main -- where

main : IO ()
main = do
  let x = 69.0
  case x of
    69.0 => print $ 2.0
    _    => print $ 4.0

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Incrementer
import Service
import System
import Numeric

%default total

-- Run external service
public export
runIncrementer : Integer -> IO Integer
runIncrementer = do ?run

public export
incrementerContract : (a : Integer) -> Contract (runIncrementer a) Integer
incrementerContract a = MkContract (runIncrementer a)

public export
incrementerService : Integer -> Service Integer
incrementerService a = Promise (incrementerContract a)

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Test.Toml.LexerTest

import IdrTest.Test
import IdrTest.Expectation

import Toml.Lexer

lexerSpecs : List (String, Maybe (List TomlToken))
lexerSpecs =
  [
    (
      "# This is a TOML document.\n\ntitle = \"TOML Example\"\n[owner]\nname = \"Tom Preston-Werner\"",
      Just $
      [ Tok Comment "# This is a TOML document."
      , Tok Whitespace "\n\n"
      , Tok Keyword "title"
      , Tok Whitespace " "
      , Tok Equals "="
      , Tok Whitespace " "
      , Tok StringLit "\"TOML Example\""
      , Tok Whitespace "\n"
      , Tok LeftBracket "["
      , Tok Keyword "owner"
      , Tok RightBracket "]"
      , Tok Whitespace "\n"
      , Tok Keyword "name"
      , Tok Whitespace " "
      , Tok Equals "="
      , Tok Whitespace " "
      , Tok StringLit "\"Tom Preston-Werner\""
      ]
    ),
    (
      "[a]\nb=1\nc.d=2\n[e.f]\ng=3",
      Just $
      [ Tok LeftBracket "["
      , Tok Keyword "a"
      , Tok RightBracket "]"
      , Tok Whitespace "\n"
      , Tok Keyword "b"
      , Tok Equals "="
      , Tok Number "1"
      , Tok Whitespace "\n"
      , Tok Keyword "c"
      , Tok Dot "."
      , Tok Keyword "d"
      , Tok Equals "="
      , Tok Number "2"
      , Tok Whitespace "\n"
      , Tok LeftBracket "["
      , Tok Keyword "e"
      , Tok Dot "."
      , Tok Keyword "f"
      , Tok RightBracket "]"
      , Tok Whitespace "\n"
      , Tok Keyword "g"
      , Tok Equals "="
      , Tok Number "3"
      ]
    ),
    (
      "[\"a.b\"]\n\"c.b\"=1",
      Just $
      [ Tok LeftBracket "["
      , Tok StringLit "\"a.b\""
      , Tok RightBracket "]"
      , Tok Whitespace "\n"
      , Tok StringLit "\"c.b\""
      , Tok Equals "="
      , Tok Number "1"
      ]
    )
  ]

export
suite : Test
suite =
  let
    lexerTests =
      map (\(text, result) =>
        test text (\_ => assertEq (lexToml text) result)
      ) lexerSpecs
  in
    describe "Toml Lexer Tests"
      [ describe "Lexer Specs" lexerTests
      ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Main

import Erlang.System.File

main : IO ()
main = do
  Right tempFile <- openFile "temp.txt" WriteTruncate
    | Left _ => putStrLn "Failed to open"
  fPutStr tempFile "Hello world"
  closeFile tempFile
  Right contents <- readFile "temp.txt"
    | Left _ => putStrLn "Failed to read file"
  putStrLn contents


text:
module Graphics.DOT

import Data.List
import Data.List1

import public Graphics.DOT.AST
import Graphics.DOT.Lexer
import Graphics.DOT.Parser

-- TODO: REMOVE ONCE READY
import System.File
import Text.Lexer.Core
import Text.Parser.Core

lexTest : String -> IO ()
lexTest fp =
  do (Right contents) <- readFile fp
        | Left err => putStrLn $ "FILE ERROR: " ++ show err
     let (tokList, (line, col, rem)) = lex contents
     putStrLn $ "Reached " ++ (show line) ++ ":" ++ (show col)
     putStrLn $ "Remainder: " ++ rem
     putStrLn "----------------\n-- TOKEN LIST --\n----------------\n"
     putStrLn $ show tokList

parseTest : String -> IO ()
parseTest fp =
  do (Right contents) <- readFile fp
       | Left err => putStrLn $ "FILE ERROR: " ++ show err
     let (tokData, _) = lex contents
     let pRes = parse tokData
     putStrLn $
        the String $
            case pRes of
                 Left errs =>
                     "PARSER ERROR: " -- ++ (show errs) -- ++ "\n\t" ++ show ts
                 Right (ast, rem) =>
                     show ast ++ "\n\tREM: " ++ show rem
     Right (ast, rem) <- pure $ parse tokData
        | Left errs => do putStrLn $ "PARSER ERROR: " -- ++ (show errs)
                          -- putStrLn $ "\t" ++ show ts
     putStrLn $ "Remainder: " ++ show rem
--     putStrLn "----------------\n-- AST --\n----------------\n"
--     putStrLn $ show ast

||| The types of errors that can occur when processing a DOT/.gv file, combined
||| with the respective error message.
public export
data DOTError : Type where
   ||| An error occurred when trying to read the file.
   FError : (errMsg : String) -> DOTError
   ||| Something's wrong with the structure of the DOT in the file.
   ParseError : (errMsg : String) -> DOTError

||| Given a file name, open it and lex and parse the DOT in it.
|||
||| @ fname the file name to read
export
readDOTFile : (fname : String) -> IO (Either DOTError DOT)
readDOTFile fname =
   do (Right contents) <- readFile fname
         | Left err => pure $ Left $ FError (show err)
      let (tokData, _) = lex contents
      Right (ast, rem) <- pure $ parse tokData
         | Left _ => pure $ Left $ ParseError "Couldn't parse token data."
      if (not . isNil) rem
         then pure $ Left $ ParseError ("Couldn't parse entire token stream.\nRemainder: " ++ show rem)
         else pure $ Right ast


text:
module AssRecRule

import Data.Fin
import Data.Vect

--Question 1
recList : (a: Type) ->  (x: Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)
recList a x base step [] = base
recList a x base step (z :: xs) = step z xs previous where
  previous = recList a x base step xs

--Question 2
mapList : (a: Type) -> (b: Type) -> (f: a -> b) -> List a -> List b
mapList a b f xs = recList a (List b) base step xs where
  base = []
  step = \u: a => \r: List a => \d: List b => ((f u) :: d)

--Question 3 (this performs left folding, but the element init is evaluated at the end. I believe
--it is possible to perform the operation with 'init' at the beginning, but this would require the
-- the list to be reversed (which could be done with recList))
foldList : (a: Type) ->  (init: a) -> (op : a -> a -> a) -> List a -> a
foldList a init op xs = recList a a base step xs where
  base = init
  step = \u: a => \r: List a => \v: a => op u v

--Question 4
inducFin : (xs : (n: Nat) -> Fin n -> Type) ->
  (base : (m: Nat) -> xs (S m) FZ) ->
  (step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))) ->
  (q: Nat) -> (j: Fin q) -> xs q j
inducFin xs base step (S k) FZ = base k
inducFin xs base step (S k) (FS x) = step k x previous where
  previous = inducFin xs base step k x

--Question 5
fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)
fetchElem a q j vs = inducFin (mV a) base step q j vs where

  mV: (a: Type) -> (n: Nat) -> (q: Fin n) -> Type
  mV a n q = (Vect n a -> a)

  base: (m: Nat) -> (s: Vect (S m) a) -> a
  base m (x :: xs) = x

  step: (k: Nat) -> (q: Fin k) -> (f: Vect k a -> a) -> (Vect (S k) a) -> a
  step k q f (x :: xs) = f xs


text:
-- pass parameters in bulk to types and functions

module ParameterisedBlocks

import Data.Vect

parameters (x: Nat, y : Nat)
  addAll : Nat -> Nat
  addAll z = x + y + z

parameters (y : Nat, xs : Vect x a)
  data Vects : Type -> Type where
    MkVects : Vect y a -> Vects a

  append : Vects a -> Vect (x + y) a
  append (MkVects ys) = xs ++ ys

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module PQ.FFI.Bindings

import Control.Monad.Error.Interface
import Control.Monad.Reader.Interface
import PQ.FFI.Types

--------------------------------------------------------------------------------
--          Foreign Types
--------------------------------------------------------------------------------

public export
data PGConnection : Type where

public export
data PGResult : Type where

public export
Connection : Type
Connection = Ptr PGConnection

public export
Result : Type
Result = Ptr PGResult

--------------------------------------------------------------------------------
--          FFI
--------------------------------------------------------------------------------

pq : String -> String
pq s = #"C:\#{s},libpq"#

%foreign pq "PQconnectdb"
prim__connect : String -> PrimIO Connection

%foreign pq "PQstatus"
prim__status : Connection -> PrimIO Bits8

%foreign pq "PQerrorMessage"
prim__errorMessage : Connection -> PrimIO String

%foreign pq "PQfinish"
prim__finish : Connection -> PrimIO ()

%foreign pq "PQexec"
prim__exec : Connection -> String -> PrimIO Result

%foreign pq "PQntuples"
prim__ntuples : Result -> PrimIO Bits32

%foreign pq "PQnfields"
prim__nfields : Result -> PrimIO Bits32

%foreign pq "PQresultStatus"
prim__resultStatus : Result -> PrimIO Bits8

%foreign pq "PQresultErrorMessage"
prim__resultErrorMsg : Result -> PrimIO String

%foreign pq "PQclear"
prim__clear : Result -> PrimIO ()

%foreign pq "PQgetvalue"
prim__getValue : Result -> Bits32 -> Bits32 -> PrimIO String

--------------------------------------------------------------------------------
--          WithConnection and WithRes
--------------------------------------------------------------------------------

public export
record SQLEnv (env : Type) (io : Type -> Type) (a : Type) where
  constructor MkSQLEnv
  runSQL : env -> io (Either SQLError a)

bind : Monad io => SQLEnv env io a -> (a -> SQLEnv env io b) -> SQLEnv env io b
bind (MkSQLEnv g) f =
  MkSQLEnv $ \e => do
    Right a <- g e
      | Left err => pure (Left err)
    runSQL (f a) e

catch :  Monad io
      => SQLEnv env io a
      -> (SQLError -> SQLEnv env io a)
      -> SQLEnv env io a
catch (MkSQLEnv fun) f =
  MkSQLEnv $ \e => do
    Left err <- fun e
      | Right a => pure (Right a)
    runSQL (f err) e

public export %inline
Functor io => Functor (SQLEnv env io) where
  map f (MkSQLEnv run) = MkSQLEnv $ (map . map $ f) . run

public export %inline
Monad io => Applicative (SQLEnv env io) where
  pure a = MkSQLEnv $ \_ => pure (Right a)
  f <*> a = bind f $ \fun => map (apply fun) a

public export %inline
Monad io => Monad (SQLEnv env io) where
  (>>=) = bind

public export %inline
Monad io => MonadError SQLError (SQLEnv env io) where
  throwError err = MkSQLEnv $ \_ => pure (Left err)
  catchError = catch

public export %inline
Monad io => MonadReader env (SQLEnv env io) where
  ask = MkSQLEnv $ \e => pure (Right e)
  local f (MkSQLEnv fun) = MkSQLEnv (fun . f)

--------------------------------------------------------------------------------
--          Low level API
--------------------------------------------------------------------------------

public export
WithConnection : (Type -> Type) -> Type -> Type
WithConnection io a = Connection -> io a

public export
WithResult : (Type -> Type) -> Type -> Type
WithResult io a = Result -> io a

export
status : HasIO io => WithConnection io ConnStatusType
status c = fromBits8 <$> primIO (prim__status c)

export
connect :  HasIO io
        => MonadError SQLError io
        => String
        -> WithConnection io a
        -> io a
connect s f = do
  c <- primIO (prim__connect s)
  BAD <- status c
    | _ => do
      ea <- tryError (f c)
      primIO $ prim__finish c
      liftEither ea

  msg <- primIO (prim__errorMessage c)
  primIO $ prim__finish c
  throwError $ ConnectionError BAD msg

export
resultStatus : HasIO io => WithResult io ExecStatusType
resultStatus r = fromBits8 <$> primIO (prim__resultStatus r)

export
resultErrorMsg : HasIO io => WithResult io String
resultErrorMsg r = primIO (prim__resultErrorMsg r)

export
exec :  HasIO io
     => MonadError SQLError io
     => String
     -> ExecStatusType
     -> (Result -> io a)
     -> Connection
     -> io a
exec s est f c = do
  res <- primIO (prim__exec c s)
  st  <- resultStatus res
  if st == est
     then do
       ea <- tryError (f res)
       primIO $ prim__clear res
       liftEither ea
     else do
       msg <- resultErrorMsg res
       primIO $ prim__clear res
       throwError $ ExecError st msg

export
exec_ :  HasIO io
      => MonadError SQLError io
      => String
      -> ExecStatusType
      -> Connection
      -> io ()
exec_ s est = exec s est (\_ => pure ())

export
ntuples : HasIO io => Result -> io Bits32
ntuples r = primIO $ prim__ntuples r

export
nfields : HasIO io => Result -> io Bits32
nfields r = primIO $ prim__nfields r

export
getValue : HasIO io => Result -> Bits32 -> Bits32 -> io String
getValue r row col = primIO $ prim__getValue r row col

-- --------------------------------------------------------------------------------
-- --          SOP
-- --------------------------------------------------------------------------------
--
-- getVal :  HasIO io
--        => MonadError SQLError io
--        => Result
--        -> (row  : Bits32)
--        -> (name : String)
--        -> (col  : Bits32)
--        -> (read : String -> Maybe t)
--        -> io t
-- getVal res row name col read = do
--   s <- getValue res row col
--   case read s of
--     Just t => pure t
--     Nothing => throwError $ ReadError name row col s
--
-- getRow :  {0 ts : List Type}
--        -> HasIO io
--        => MonadError SQLError io
--        => NP (K String) ts
--        -> NP (K Bits32) ts
--        -> NP (\t => String -> Maybe t) ts
--        -> Result
--        -> (row : Bits32)
--        -> io (NP I ts)
-- getRow names columns readers res row =
--   sequenceNP $ hliftA3 (getVal res row) names columns readers
--
-- export
-- getRows :  {0 ts : List Type}
--         -> HasIO io
--         => MonadError SQLError io
--         => NP (K String) ts
--         -> NP (\t => String -> Maybe t) ts
--         -> Result
--         -> io (List $ NP I ts)
-- getRows names readers res =
--   let fieldCount = cast {to = Bits32} . length $ collapseNP names
--       indices    = the (NP (K Bits32) ts) $ iterateNP names (+1) 0
--    in do
--       nt <- ntuples res
--       if nt == 0
--          then pure []
--          else do
--            nf <- nfields res
--            if nf == fieldCount
--               then traverse (getRow names indices readers res) [0 .. nt - 1]
--               else throwError $ QueryError fieldCount nf


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 10

import Data.Vect
import Data.List.Views
import Data.Vect.Views
import Data.Nat.Views

-- check that all functions are total
%default total

--
-- section 10.1
--

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

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

-- more explicit using `with`
takeN' : (n : Nat) -> (xs : List a) -> TakeN xs
takeN' Z xs = Exact []
takeN' (S k) [] = Fewer
takeN' (S k) (x :: xs) with (takeN' k xs)
  takeN' (S k) (x :: xs) | Fewer = Fewer
  takeN' (S k) (x :: (n_xs ++ ys)) | (Exact n_xs) = Exact (x :: n_xs)

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

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

partial
halves : List a -> (List a, List a)
halves xs with (takeN (length xs `div` 2) xs)
  halves xs | Fewer = (xs, [])
  halves (n_xs ++ ys) | (Exact n_xs) = (n_xs, ys)

--
-- section 10.2
--

equalSuffix : Eq a => List a -> List a -> List a
equalSuffix input1 input2 with (snocList input1)
  equalSuffix [] input2 | Empty = []
  equalSuffix (xs ++ [x]) input2 | (Snoc xsrec) with (snocList input2)
    equalSuffix (xs ++ [x]) [] | (Snoc xsrec) | Empty = []
    equalSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec)
      = if x == y then (equalSuffix xs ys | xsrec | ysrec) ++ [x]
                  else []

mergeSortVect : Ord a => Vect n a -> Vect n a
mergeSortVect xs with (splitRec xs)
  mergeSortVect [] | SplitRecNil = []
  mergeSortVect [x] | SplitRecOne = [x]
  mergeSortVect (lefts ++ rights) | (SplitRecPair lrec rrec)
    = merge (mergeSortVect lefts | lrec)
            (mergeSortVect rights | rrec)

toBinary : Nat -> String
toBinary k with (halfRec k)
  toBinary Z | HalfRecZ = ""
  toBinary (n + n) | (HalfRecEven rec) = (toBinary n | rec) ++ "0"
  toBinary (S (n + n)) | (HalfRecOdd rec) = (toBinary n | rec) ++ "1"

-- needed due to lazy argument of HalfRec
-- use :exec toBinaryMain $ toBinary 42
toBinaryMain : Nat -> IO ()
toBinaryMain k = do putStrLn $ toBinary k

palindrome : Eq a => List a -> Bool
palindrome xs with (vList xs)
  palindrome [] | VNil = True
  palindrome [x] | VOne = True
  palindrome (x :: (ys ++ [y])) | (VCons rec)
    = (x == y) && palindrome ys | rec

--
-- section 10.3 (exercises)
-- see DataStore.idr and TestStore.idr
-- see Shape.idr and TestShape.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Compiler.Erlang.Codegen.AbstractFormatToErlangSource

import public Compiler.Erlang.IR.AbstractFormat
import Compiler.Erlang.Utils.CompositeString
import Compiler.Erlang.Utils.String
import Data.Fin
import Data.List

%default total

-- HELPER FUNCTIONS

sepBy : String -> List CompositeString -> CompositeString
sepBy sep xs =
  Nested $ intersperse (Str sep) xs

-- CODE GENERATION

genAtom : String -> String
genAtom x = "'" ++ escapeString (unpack x) "" ++  "'"

genCharlist : String -> String
genCharlist x = "\"" ++ escapeString (unpack x) "" ++ "\""

genLiteral : Literal -> String
genLiteral (ALAtom l x) = genAtom x
genLiteral (ALChar l x) = "$" ++ escapeChar x ""
genLiteral (ALFloat l x) = showDouble x
genLiteral (ALInteger l x) = show x
genLiteral (ALCharlist l x) = genCharlist x

genMapFieldAssoc : (a -> CompositeString) -> MapFieldAssoc a -> CompositeString
genMapFieldAssoc genValue (MkAssoc l key value) =
  Nested [genValue key, Str " => ", genValue value]

genMapFieldExact : (a -> CompositeString) -> MapFieldExact a -> CompositeString
genMapFieldExact genValue (MkExact l key value) =
  Nested [genValue key, Str " := ", genValue value]

genBitType : BitType -> String
genBitType type =
  case type of
    ABInteger => "integer"
    ABFloat => "float"
    ABBinary => "binary"
    ABBytes => "bytes"
    ABBitstring => "bitstring"
    ABBits => "bits"
    ABUtf8 => "utf8"
    ABUtf16 => "utf16"
    ABUtf32 => "utf32"

genBitSignedness : BitSignedness -> String
genBitSignedness signedness =
  case signedness of
    ABUnsigned => "unsigned"
    ABSigned => "signed"

genBitEndianness : BitEndianness -> String
genBitEndianness endianness =
  case endianness of
    ABBig => "big"
    ABLittle => "little"
    ABNative => "native"

genBitUnit : BitUnit -> String
genBitUnit (MkBitUnit size) =
  "unit:" ++ show (cast size + 1)

genBitSize : BitSize -> Maybe String
genBitSize ABSDefault = Nothing
genBitSize (ABSInteger l x) = Just $ show x
genBitSize (ABSVar l x) = Just x

genTypeSpecifierList : TypeSpecifierList -> List String
genTypeSpecifierList (MkTSL signedness endianness type unit) =
  toList (map genBitSignedness signedness) ++
    toList (map genBitEndianness endianness) ++
    toList (map genBitType type) ++
    toList (map genBitUnit unit)

genBitSegment : (a -> CompositeString) -> BitSegment a -> CompositeString
genBitSegment genValue (MkBitSegment l value size tsl) =
  let bitSizeStr = maybe "" (":" ++) (genBitSize size)
      tslStr = case genTypeSpecifierList tsl of
        [] => ""
        xs => "/" ++ showSep "-" xs
  in Nested [genValue value, Str bitSizeStr, Str tslStr]

genBitPattern : BitPattern -> CompositeString
genBitPattern (ABPInteger l x) = Str (show x)
genBitPattern (ABPFloat l x) = Str (showDouble x)
genBitPattern (ABPCharlist l x) = Str (genCharlist x)
genBitPattern (ABPUniversal l) = Str "_"
genBitPattern (ABPVar l x) = Str x

genPattern : Pattern -> CompositeString
genPattern (APLiteral x) = Str (genLiteral x)
genPattern (APBitstring l segments) =
  let segments' = sepBy ", " $ assert_total $ map (genBitSegment genBitPattern) segments
  in Nested [Str "<<", segments', Str ">>"]
genPattern (APCons l x y) = Nested [Str "[", genPattern x, Str " | ", genPattern y, Str "]"]
genPattern (APMap l entries) =
  let entries' = sepBy ", " $ assert_total $ map (genMapFieldExact genPattern) entries
  in Nested [Str "#{", entries', Str "}"]
genPattern (APNil l) = Str "[]"
genPattern (APTuple l patterns) =
  let patterns' = sepBy ", " $ assert_total $ map genPattern patterns
  in Nested [Str "{", patterns', Str "}"]
genPattern (APUniversal l) = Str "_"
genPattern (APVar l x) = Str x

genGuard : Guard -> CompositeString
genGuard (AGLiteral x) = Str (genLiteral x)
genGuard (AGCons l x y) = Nested [Str "[", genGuard x, Str " | ", genGuard y, Str "]"]
genGuard (AGFunCall l fnName args) =
  let args' = sepBy ", " $ assert_total $ map genGuard args
  in Nested [Str $ "(erlang:" ++ genAtom fnName ++ "(", args', Str "))"]
genGuard (AGNil l) = Str "[]"
genGuard (AGOp l opName x y) = Nested [Str "(", genGuard x, Str $ " " ++ opName ++ " ", genGuard y, Str ")"]
genGuard (AGTuple l guards) =
  let guards' = sepBy ", " $ assert_total $ map genGuard guards
  in Nested [Str "{", guards', Str "}"]
genGuard (AGVar l x) = Str x

genGuardAlt : GuardAlt -> CompositeString
genGuardAlt (MkGuardAlt guards) =
  sepBy "; " $ assert_total $ map genGuard (toList guards)

mutual
  genExpr : Expr -> CompositeString
  genExpr (AELiteral x) =
    Str (genLiteral x)
  genExpr (AEBitstring l segments) =
    let segments' = sepBy ", " $ assert_total $ map (genBitSegment genExpr) segments
    in Nested [Str "<<", segments', Str ">>"]
  genExpr (AEBlock l body) =
    let body' = sepBy ", " $ assert_total $ map genExpr (toList body)
    in Nested [Str "begin ", body', Str " end"]
  genExpr (AECase l sc clauses) =
    let sc' = genExpr sc
        clauses' = sepBy "; " $ assert_total $ map genCaseClause (toList clauses)
    in Nested [Str "case ", sc', Str " of ", clauses', Str " end"]
  genExpr (AECons l x y) =
    Nested [Str "[", genExpr x, Str " | ", genExpr y, Str "]"]
  genExpr (AEFun l arity clauses) =
    let clauses' = sepBy "; " $ assert_total $ map genFunClause (toList clauses)
    in Nested [Str "fun ", clauses', Str " end"]
  genExpr (AEFunCall l fn args) =
    let fn' = genExpr fn
        args' = sepBy ", " $ assert_total $ map genExpr args
    in Nested [Str "(", fn', Str "(", args', Str "))"]
  genExpr (AERemoteRef l modName fnName) =
    Nested [genExpr modName, Str ":", genExpr fnName]
  genExpr (AEMapNew l entries) =
    let entries' = sepBy ", " $ assert_total $ map (genMapFieldAssoc genExpr) entries
    in Nested [Str "#{", entries', Str "}"]
  genExpr (AEMatch l p x) =
    Nested [Str "(", genPattern p, Str " = ", genExpr x, Str ")"]
  genExpr (AENil l) =
    Str "[]"
  genExpr (AEOp l opName x y) =
    Nested [Str "(", genExpr x, Str $ " " ++ opName ++ " ", genExpr y, Str ")"]
  genExpr (AEReceive l clauses timeout) =
    let clauses' = sepBy "; " $ assert_total $ map genCaseClause clauses
        timeout' = case timeout of
          NoTimeout => Str ""
          TimeoutAfter ms afterBody =>
            let afterBody' = sepBy ", " $ assert_total $ map genExpr (toList afterBody)
            in Nested [Str $ " after ", genExpr ms, Str " -> ", afterBody']
    in Nested [Str "receive ", clauses', timeout', Str " end"]
  genExpr (AETuple l exprs) =
    let exprs' = sepBy ", " $ assert_total $ map genExpr exprs
    in Nested [Str "{", exprs', Str "}"]
  genExpr (AETry l sc caseClauses catchClauses afterBody) =
    let sc' = sepBy ", " $ assert_total $ map genExpr (toList sc)
        caseClauses' = case caseClauses of
          [] => Str ""
          xs => Nested [Str " of ", sepBy "; " $ assert_total $ map genCaseClause xs]
        catchClauses' = case catchClauses of
          [] => Str ""
          xs => Nested [Str " catch ", sepBy "; " $ assert_total $ map genCatchClause xs]
        afterBody' = case afterBody of
          [] => Str ""
          xs => Nested [Str " after ", sepBy ", " $ assert_total $ map genExpr xs]
    in Nested [Str "try ", sc', caseClauses', catchClauses', afterBody', Str " end"]
  genExpr (AEVar l x) =
    Str x

  genFunClause : FunClause arity -> CompositeString
  genFunClause (MkFunClause l patterns guardAlts body) =
    let patterns' = sepBy ", " $ assert_total $ map genPattern (toList patterns)
        guardAlts' = case guardAlts of
          [] => Str ""
          xs => Nested [Str " when ", sepBy ", " $ assert_total $ map genGuardAlt guardAlts]
        body' = sepBy ", " $ assert_total $ map genExpr (toList body)
    in Nested [Str "(", patterns', Str ")", guardAlts', Str " -> ", body']

  genCaseClause : CaseClause -> CompositeString
  genCaseClause (MkCaseClause l pattern guardAlts body) =
    let pattern' = genPattern pattern
        guardAlts' = case guardAlts of
          [] => Str ""
          xs => Nested [Str " when ", sepBy ", " $ assert_total $ map genGuardAlt guardAlts]
        body' = sepBy ", " $ assert_total $ map genExpr (toList body)
    in Nested [pattern', guardAlts', Str " -> ", body']

  genCatchClause : CatchClause -> CompositeString
  genCatchClause (MkCatchClause l classPat reasonPat stacktracePat guardAlts body) =
    let classPat' = genPattern classPat
        reasonPat' = genPattern reasonPat
        stacktracePat' = genPattern stacktracePat
        guardAlts' = case guardAlts of
          [] => Str ""
          xs => Nested [Str " when ", sepBy ", " $ assert_total $ map genGuardAlt guardAlts]
        body' = sepBy ", " $ assert_total $ map genExpr (toList body)
    in Nested [classPat', Str ":", reasonPat', Str ":", stacktracePat', guardAlts', Str " -> ", body']

genExportFun : (String, Nat) -> String
genExportFun (name, arity) = genAtom name ++ "/" ++ show (natToInteger arity)

-- Assumptions:
-- * Variables names in `Decl` are required to start with a capitalized letter.
-- * The attribute name of `ADAttribute` can't contain special characters that
--   would require apostrophe.
export
genDecl : Decl -> CompositeString
genDecl (ADExport l fs) =
  Str $ "-export([\n  " ++ showSep ",\n  " (map genExportFun fs) ++ "\n])."
genDecl (ADModule l name) =
  Str $ "-module(" ++ genAtom name ++ ")."
genDecl (ADFunDef l name arity clauses) =
  Nested [sepBy ";\n" $ map clauseToFunHead (toList clauses), Str "."]
  where
    clauseToFunHead : FunClause arity -> CompositeString
    clauseToFunHead clause = Nested [Str (genAtom name), genFunClause clause]
genDecl (ADAttribute l attr value) =
  Nested [Str $ "-" ++ attr ++ "(", primTermToCS value, Str ")."]


text:
module Parser

import Data.String
import Data.List

public export
Input : Type
Input = List Char

public export
data ParseResult a = Done (a, Input) | Error String

-- To make a parser we need to take a function to maps from input to
-- A parse result and feed it into the AParser constuctor
public export
data Parser : Type -> Type where
  AParser : (Input -> ParseResult a) -> Parser a

%name Parser parser, parser2

-- To actually apply a parser we need to call the parse function
export
parse : Parser a -> Input -> ParseResult a
parse (AParser p) input = p input

export
doParse : Parser a -> String -> ParseResult a
doParse parser str = parse parser (unpack str)

export
eitherParse : Parser a -> String -> Either String a
eitherParse parser input =
  case doParse parser input of
    Done (a, rest) => Right a
    Error str => Left str

-- This is a more general form of map, it takes a parser, applies it
-- and the maps over both the result and the remaining input
export
continue : Parser a -> ((a, Input) -> ParseResult b) -> Parser b
continue parser f = AParser $ \input =>
    case parse parser input of
      Error str => Error str
      Done a => f a

public export
Functor ParseResult where
  map _ (Error str) = Error str
  map f (Done (a, input)) = Done (f a, input)

public export
Functor Parser where
  -- map : (a -> b) -> Parser a -> Parser b
  map f parser = AParser $ map f . parse parser

public export
Applicative Parser where
  (<*>) parser1 parser2 =
    AParser $ \input =>
      case parse parser1 input of
        Error err => Error err
        Done (a, rest) => parse (map a parser2) rest

  pure a = AParser \input => Done (a, input)

public export
Monad Parser where
  -- (>>=) : Parser a -> (a -> Parser b) -> Parser b
  (>>=) parser f = continue parser (\(a, rest) => parse (f a) rest)

-- Defining Basic parsers

export
end : ParseResult a
end = Error "End of Input"

export
failure : Parser a
failure = AParser $ \input => Error "Always fails"

export
parseError : String -> Parser a
parseError err = AParser $ \input => Error err

export
pToken : Parser Char
pToken = AParser $ \input =>
  case input of
    [] => end
    (c :: cs) => Done (c, cs)

export
validate : (a -> Bool) -> Parser a -> Parser a
validate f parser = do
  result <- parser
  if f result
    then pure result
    else parseError "Invalid Parse"

export
pBool : (Char -> Bool) -> Parser Char
pBool f = validate f pToken

-- parse a specific word
export
pTag : String -> Parser String
pTag tag = AParser $ go (unpack tag) []
  where
    go : List Char -> List Char -> Input -> ParseResult String
    go [] acc input = Done (pack . reverse $ acc, input)
    go (c :: cs) acc [] = end
    go (c :: cs) acc (n :: rest) =
      if c == n then go cs (n :: acc) rest
      else Error "Did not match tag"

-- Apply a parser N times
-- This should return a Vect
-- There must be a better way to do this
export
pN : Parser a -> Nat -> Parser (List a)
pN parser n = go parser n []
  where
    go : Parser a -> Nat -> List a -> Parser (List a)
    go parser 0 xs = failure
    go parser (S k) acc = do
      parsed <- parser
      let newAcc = parsed :: acc
      case k of
        0 => pure $ reverse newAcc
        k => go parser k newAcc

export
pChar : Char -> Parser Char
pChar c = pBool (==c)

export
pDigit : Parser Char
pDigit = pBool isDigit

export
many : Parser a -> Parser (List a)
many parser = AParser $ map reverse . go []
  where
    go : List a -> Input -> ParseResult (List a)
    go acc input =
      case parse parser input of
        Done (parsed, rest) => go (parsed :: acc) rest
        Error str => Done (acc, input)

export
manyString : Parser Char -> Parser String
manyString parser = map pack (many parser)

export
or : Parser a -> Parser a -> Parser a
or parser1 parser2 = AParser $ \input =>
  case parse parser1 input of
    Done (result, rest) => Done (result, rest)
    Error _ => parse parser2 input

infixr 4 <^>
export
(<^>) : Parser a -> Parser a -> Parser a
(<^>) x y = or x y

export
while : (Char -> Bool) -> Parser String
while f = manyString (pBool f)

export
until : (Char -> Bool) -> Parser String
until f = while (not . f)

export
pWhiteSpace : Parser String
pWhiteSpace = while isSpace

export
-- Parse until it encounters whitespace
-- Doesn't consume the whitespace
pWord : Parser String
pWord = until isSpace

export
mapM : (a -> Maybe b) -> Parser a -> Parser b
mapM f parser = do
  parsed <- parser
  case f parsed of
    Nothing => parseError "Invalid mapM"
    Just a => pure a

export
pInteger : Parser Integer
pInteger = mapM parseInteger (while validChar)
  where validChar : Char -> Bool
        validChar '+' = True
        validChar '-' = True
        validChar c = isDigit c

export
pNat : Parser Nat
pNat = map stringToNatOrZ (while isDigit)

export
andThen : Parser a -> Parser b -> Parser (a,b)
andThen parser1 parser2 = do
  parsed1 <- parser1
  parsed2 <- parser2
  pure (parsed1, parsed2)

infixl 3 <&>
export
(<&>) : Parser a -> Parser b -> Parser (a,b)
(<&>) x y = andThen x y

export
thenDrop : Parser a -> Parser b -> Parser a
thenDrop parser1 parser2 = map fst (andThen parser1 parser2)

infixl 3 :>
export
(:>) : Parser a -> Parser b -> Parser a
(:>) x y = thenDrop x y

export
sepBy : Parser a -> Parser b -> Parser (List a)
sepBy parser1 parser2 = do
  most <- many (thenDrop parser1 parser2)
  AParser $ (\input =>
      case parse parser1 input of
        Done (result, rest) => Done (most ++ [result], rest)
        Error str => Done (most, input))

export
-- Matches the end of the file
theEnd : Parser ()
theEnd = AParser $ \input =>
  if input == [] then Done ((), [])
  else Error "Expected End of File"

export
-- Parses a word and consume whitespace
pWord' : Parser String
pWord' = pWord :> pWhiteSpace

export
ignore : Parser a -> Parser ()
ignore parser = map (\i => ()) parser

export
oneOf : List (Parser a) -> Parser a
oneOf parsers = foldl (<^>) (parseError "No opertion found") parsers

export
ignoreThen : Parser a -> Parser b -> Parser b
ignoreThen parser1 parser2 = map snd (parser1 <&> parser2)

-- Parses a line as text and consumes the newline
-- TODO make this work on windows style newlines
export
line : Parser String
line = (until (=='\n')) `thenDrop` (pChar '\n')

export
pLines : Parser a -> Parser (List a)
pLines parser = sepBy parser line

infixl 3 <:
export
(<:) : Parser a -> Parser b -> Parser b
(<:) x y = ignoreThen x y


text:
module Data.Prim.Int32

import public Control.WellFounded
import public Data.DPair
import public Data.Prim.Ord
import public Algebra.Solver.Ring
import Syntax.PreorderReasoning

%default total

unsafeRefl : a === b
unsafeRefl = believe_me (Refl {x = a})

--------------------------------------------------------------------------------
--          (<)
--------------------------------------------------------------------------------

||| Witness that `m < n === True`.
export
data (<) : (m,n : Int32) -> Type where
  LT : {0 m,n : Int32} -> (0 prf : (m < n) === True) -> m < n

||| Contructor for `(<)`.
|||
||| This can only be used in an erased context.
export %hint
0 mkLT : (0 prf : (m < n) === True) -> m < n
mkLT = LT

||| Extractor for `(<)`.
|||
||| This can only be used in an erased context.
export
0 runLT : m < n -> (m < n) === True
runLT (LT prf) = prf

||| We don't trust values of type `(<)` too much,
||| so we use this when creating magical results.
export
strictLT : (0 p : m < n) -> Lazy c -> c
strictLT (LT prf) x = x

--------------------------------------------------------------------------------
--          Aliases
--------------------------------------------------------------------------------

||| Flipped version of `(<)`.
public export
0 (>) : (m,n : Int32) -> Type
m > n = n < m

||| `m <= n` mean that either `m < n` or `m === n` holds.
public export
0 (<=) : (m,n : Int32) -> Type
m <= n = Either (m < n) (m === n)

||| Flipped version of `(<=)`.
public export
0 (>=) : (m,n : Int32) -> Type
m >= n = n <= m

||| `m /= n` mean that either `m < n` or `m > n` holds.
public export
0 (/=) : (m,n : Int32) -> Type
m /= n = Either (m < n) (m > n)

--------------------------------------------------------------------------------
--          Order
--------------------------------------------------------------------------------

0 ltNotEQ : m < n -> Not (m === n)
ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")

0 ltNotGT : m < n -> Not (n < m)
ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")

0 eqNotLT : m === n -> Not (m < n)
eqNotLT = flip ltNotEQ

export
comp : (m,n : Int32) -> Trichotomy (<) m n
comp m n = case prim__lt_Int32 m n of
  0 => case prim__eq_Int32 m n of
    0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
    x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)

export
Total Int32 (<) where
  trichotomy   = comp
  transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl

--------------------------------------------------------------------------------
--          Bounds and Well-Foundedness
--------------------------------------------------------------------------------

||| Lower bound of `Int32`
public export
MinInt32 : Int32
MinInt32 = -0x80000000

||| Upper bound of `Int32`
public export
MaxInt32 : Int32
MaxInt32 = 0x7fffffff

||| `m >= MinInt32` for all `m` of type `Int32`.
export
0 GTE_MinInt32 : (m : Int32) -> m >= MinInt32
GTE_MinInt32 m = case comp MinInt32 m of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total
            $ idris_crash "IMPOSSIBLE: Int32 smaller than \{show MinInt32}"

||| Not value of type `Int32` is less than zero.
export
0 Not_LT_MinInt32 : m < MinInt32 -> Void
Not_LT_MinInt32 = GTE_not_LT (GTE_MinInt32 m)

||| `m <= MaxInt32` for all `m` of type `Int32`.
export
0 LTE_MaxInt32 : (m : Int32) -> m <= MaxInt32
LTE_MaxInt32 m = case comp m MaxInt32 of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total
            $ idris_crash "IMPOSSIBLE: Int32 greater than \{show MaxInt32}"

||| Not value of type `Int32` is greater than `MaxInt32`.
export
0 Not_GT_MaxInt32 : m > MaxInt32 -> Void
Not_GT_MaxInt32 = LTE_not_GT (LTE_MaxInt32 m)

||| Every value of type `Int32` is accessible with relation
||| to `(<)`.
export
accessLT : (m : Int32) -> Accessible (<) m
accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)

||| `(<)` is well founded.
export %inline
WellFounded Int32 (<) where
  wellFounded = accessLT

||| Every value of type `Int32` is accessible with relation
||| to `(>)`.
export
accessGT : (m : Int32) -> Accessible (>) m
accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)

||| `(>)` is well founded.
export %inline
[GT] WellFounded Int32 (>) where
  wellFounded = accessGT

--------------------------------------------------------------------------------
--          Arithmetics
--------------------------------------------------------------------------------

||| Safe division.
export %inline
sdiv : (n,d : Int32) -> (0 prf : d /= 0) => Int32
sdiv n d = n `div` d

||| Safe modulo.
export %inline
smod : (n,d : Int32) -> (0 prf : d /= 0) => Int32
smod n d = n `mod` d


text:
module Arduino.Boards

import public Arduino.Util

%default total

-----------------------
-----------------------
---  General stuff  ---
-----------------------
-----------------------

-- How arduino pins are designated in board
public export
data Pin = D Nat
         | A Nat
         | DAC Nat

public export
data PinPurpose = Input | Output

public export
data Board = BoardLabel String (Maybe String)

--------------------------------
--------------------------------
---   Binary digital stuff   ---
--------------------------------
--------------------------------

public export
data DigitalPinValue = Low | High

public export
interface HasDigitalPins (0 board : Board) where
  CanBeDigital : Pin -> Type

  lowLevelNumberForDigitalPin : (p : Pin) -> {auto cbd : CanBeDigital p} -> Bits8
  -- TODO To think, maybe use `Fin 256` instead?

--------------------
--- Built-in LED ---
--------------------

public export
interface HasDigitalPins board => HasBuiltIn_LED (0 board : Board) where
  LED : Pin

  Builtin_LED_IsDigital : CanBeDigital {board} LED

--------------------------------
--- Interrupt-realated stuff ---
--------------------------------

namespace Interrupts

  public export
  data InterruptEvent = Low | High | Change | Rising | Falling

  public export
  interface HasDigitalPins board => HasInterruptPins (0 board : Board) where
    CanBeInterrupt : Pin -> Type
    interruptForPin : (p : Pin) -> {auto cbi : CanBeInterrupt p} -> Nat
    PinSupportsMode : (p : Pin) -> {auto cbi : CanBeInterrupt p} -> InterruptEvent -> Type

    InterruptPinsAreDigital : (p : Pin) -> CanBeInterrupt p -> CanBeDigital {board} p

----------------------------
----------------------------
---   Analog-ish stuff   ---
----------------------------
----------------------------

namespace Analogish

  public export
  data AnalogType = PWM -- pulse-width modulation
                  | DAC -- digital-to-analog convertion
                  | ADC -- analog-to-digital convertion

  public export
  interface HasAnalogPins (0 typ : AnalogType) (0 board : Board) where
    CanBeAnalog : Pin -> Type

    lowLevelNumberForAnalogPin : (p : Pin) -> {auto cba : CanBeAnalog p} -> Bits8
    -- TODO To think, maybe use `Fin 256` instead?

    -- resolution in bits of underlying hardware
    HardwareResolution : Nat

    CanBeSetAsResolution : Nat -> Type

    -- resultion that is set after start or reset
    StartupResolution : Nat

    StartupResolutionCanBeSet : CanBeSetAsResolution StartupResolution

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
module Contact

public export
record Contact where
  constructor CreateContact
  mobilePhone : Maybe String
  homePhone : Maybe String

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
||| The content of this module is based on the paper
||| Applications of Applicative Proof Search
||| by Liam O'Connor
|||
||| The main difference is that we use `Colist1` for the type of
||| generators rather than `Stream`. This allows us to avoid generating
||| many duplicates when dealing with finite types which are common in
||| programming (Bool) but even more so in dependently typed programming
||| (Vect 0, Fin (S n), etc.).

module Search.Generator

import Data.Colist
import Data.Colist1
import Data.Fin
import Data.List
import Data.Stream
import Data.Vect

------------------------------------------------------------------------
-- Interface

||| A generator for a given type is a non-empty colist of values of that
||| type.
public export
interface Generator a where
  generate : Colist1 a

------------------------------------------------------------------------
-- Implementations

-- Finite types

||| ALL of the natural numbers
public export
Generator Nat where
  generate = fromStream nats

||| ALL of the booleans
public export
Generator Bool where
  generate = True ::: [False]

||| ALL of the Fins
public export
{n : Nat} -> Generator (Fin (S n)) where
  generate = fromList1 (allFins n)

-- Polymorphic generators

||| We typically want to generate a generator for a unit-terminated right-nested
||| product so we have this special case that keeps the generator minimal.
public export
Generator a => Generator (a, ()) where
  generate = map (,()) generate

||| Put two generators together by exploring the plane they define.
||| This uses Cantor's zig zag traversal
public export
(Generator a, Generator b) => Generator (a, b) where
  generate = plane generate (\ _ => generate)

||| Put two generators together by exploring the plane they define.
||| This uses Cantor's zig zag traversal
public export
{0 b : a -> Type} -> (Generator a, (x : a) -> Generator (b x)) =>
  Generator (x : a ** b x) where
  generate = plane generate (\ x => generate)

||| Build entire vectors of values
public export
{n : Nat} -> Generator a => Generator (Vect n a) where
  generate = case n of
    Z => [] ::: []
    S n => map (uncurry (::)) generate

||| Generate arbitrary lists of values
||| Departing from the paper, to avoid having infinitely many copies of
||| the empty list, we handle the case `n = 0` separately.
public export
Generator a => Generator (List a) where
  generate = [] ::: forget (planeWith listy generate vectors) where
    listy : (n : Nat) -> Vect (S n) a -> List a
    listy _ = toList

    vectors : (n : Nat) -> Colist1 (Vect (S n) a)
    vectors n = generate


text:
module SpecExample

import Specdris.Spec

import System

%access export
%default total

add : Nat -> Nat -> Nat
add a b = a + b

addSpec : SpecTree
addSpec = describe "Add two Nats" $ do
            it "neutral element" $ do
              (1 `add` 0) === 1
            it "be associative" $ do
              ((1 `add` 2) `add` 3) === (1 `add` (2 `add` 3))
            it "be commutative" $ do
              (1 `add` 2) === (2 `add` 1)

multi : Nat -> Nat -> Nat
multi a b = a * b

multiSpec : SpecTree
multiSpec = describe "Multiply two Nats" $ do
              it "neutral element" $ do
                (2 `multi` 1) === 2
              it "be associative" $ do
                ((1 `multi` 2) `multi` 3) === (1 `multi` (2 `multi` 3))
              it "be commutative" $ do
                (1 `multi` 2) === (2 `multi` 1)

partial
specSuite : IO ()
specSuite = do seed <- System.time
               spec $ do addSpec
                         multiSpec
                         (shuffle multiSpec 999999)
                         (shuffle multiSpec seed)

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
module Data.Time.Calendar.Gregorian

import Data.Vect

--import Data.Time.Calendar.CalendarDiffDays
import Data.Time.Calendar.Days
import Data.Time.Calendar.MonthDay
import Data.Time.Calendar.OrdinalDate
import Data.Time.Calendar.Private

-- TODO: It would be nice to bound `day` based on `month`. But, I do know how to do it yet.
public export
record Gregorian where
  constructor MkGregorian
  year: Integer
  month: Int
  day: Int

export
Eq Gregorian where
  (MkGregorian y1 m1 d1) == (MkGregorian y2 m2 d2) = (y1 == y2) && (m1 == m2) && (d1 == d2)

-- | Convert to proleptic Gregorian calendar. First element of result is year, second month number (1-12), third day (1-31).
export
toGregorian : Day -> Gregorian
toGregorian date =
  let
    (year, yd) = toOrdinalDate date
    (month, day) = dayOfYearToMonthAndDay (isLeapYear year) yd
  in
     MkGregorian year month day

-- ||| Convert from proleptic Gregorian calendar. First argument is year, second month number (1-12), third day (1-31).
-- -- Invalid values will be clipped to the correct range, month first, then day.
-- export
-- fromGregorian: Integer -> Fin 12 -> Int -> Maybe Day
-- fromGregorian year month day = do
--   let isLeap = (isLeapYear year)
--   bd <- boundedDay' day month isLeap
--   let day_of_year = monthAndDayToDayOfYear isLeap month bd
--   let day = fromOrdinalDate year day_of_year
--   pure day

export
fromGregorian: Gregorian -> Day
fromGregorian gregorian =
  let
    MkGregorian year month day = gregorian
    isLeap = (isLeapYear year)
    --bd = boundedDay' day month isLeap
    day_of_year = monthAndDayToDayOfYear isLeap month day
    day = fromOrdinalDate year day_of_year
  in
     day

||| Show in ISO 8601 format (yyyy-mm-dd)
-- export
-- showGregorianFromDay: Day -> String
-- showGregorian date =
--   let
-- (MkGregorian y m d) = toGregorian date
--   in
--     (show4 y) ++ "-" ++ (show2 m) ++ "-" ++ (show2 d)

export
showGregorian: Gregorian -> String
showGregorian (MkGregorian y m d) =
    (show4 y) ++ "-" ++ (show2 m) ++ "-" ++ (show2 d)

||| The number of days in a given month according to the proleptic Gregorian calendar. First argument is year, second is month.
export
gregorianMonthLength: Integer -> Fin 12 -> Nat
gregorianMonthLength year month = index month $ monthLengths (isLeapYear year)

export
rolloverMonths: (Integer, Integer) -> (Integer, Int)
rolloverMonths (y, m) = (y + (div (m - 1) 12), integerToInt ((mod (m - 1) 12) + 1))

||| TODO: Fail on negative value
export
addGregorianMonths: Nat -> Day -> Gregorian
addGregorianMonths n day =
  let
    MkGregorian y m d = toGregorian day
    (y', m') = rolloverMonths (y, cast m + cast n)
  in
    MkGregorian  y' m' d

-- -- | Add months, with days past the last day of the month clipped to the last day.
-- -- For instance, 2005-01-30 + 1 month = 2005-02-28.
-- addGregorianMonthsClip :: Integer -> Day -> Day
-- addGregorianMonthsClip n day = fromGregorian y m d
--   where
--     (y, m, d) = addGregorianMonths n day

-- -- | Add months, with days past the last day of the month rolling over to the next month.
-- -- For instance, 2005-01-30 + 1 month = 2005-03-02.
-- addGregorianMonthsRollOver :: Integer -> Day -> Day
-- addGregorianMonthsRollOver n day = addDays (fromIntegral d - 1) (fromGregorian y m 1)
--   where
--     (y, m, d) = addGregorianMonths n day

-- -- | Add years, matching month and day, with Feb 29th clipped to Feb 28th if necessary.
-- -- For instance, 2004-02-29 + 2 years = 2006-02-28.
-- addGregorianYearsClip :: Integer -> Day -> Day
-- addGregorianYearsClip n = addGregorianMonthsClip (n * 12)

-- -- | Add years, matching month and day, with Feb 29th rolled over to Mar 1st if necessary.
-- -- For instance, 2004-02-29 + 2 years = 2006-03-01.
-- addGregorianYearsRollOver :: Integer -> Day -> Day
-- addGregorianYearsRollOver n = addGregorianMonthsRollOver (n * 12)

-- -- | Add months (clipped to last day), then add days
-- addGregorianDurationClip :: CalendarDiffDays -> Day -> Day
-- addGregorianDurationClip (CalendarDiffDays m d) day = addDays d $ addGregorianMonthsClip m day

-- -- | Add months (rolling over to next month), then add days
-- addGregorianDurationRollOver :: CalendarDiffDays -> Day -> Day
-- addGregorianDurationRollOver (CalendarDiffDays m d) day = addDays d $ addGregorianMonthsRollOver m day

-- -- | Calendrical difference, with as many whole months as possible
-- diffGregorianDurationClip :: Day -> Day -> CalendarDiffDays
-- diffGregorianDurationClip day2 day1 = let
--     (y1, m1, d1) = toGregorian day1
--     (y2, m2, d2) = toGregorian day2
--     ym1 = y1 * 12 + toInteger m1
--     ym2 = y2 * 12 + toInteger m2
--     ymdiff = ym2 - ym1
--     ymAllowed =
--         if day2 >= day1
--             then if d2 >= d1
--                      then ymdiff
--                      else ymdiff - 1
--             else if d2 <= d1
--                      then ymdiff
--                      else ymdiff + 1
--     dayAllowed = addGregorianDurationClip (CalendarDiffDays ymAllowed 0) day1
--     in CalendarDiffDays ymAllowed $ diffDays day2 dayAllowed

-- -- | Calendrical difference, with as many whole months as possible.
-- -- Same as 'diffGregorianDurationClip' for positive durations.
-- diffGregorianDurationRollOver :: Day -> Day -> CalendarDiffDays
-- diffGregorianDurationRollOver day2 day1 = let
--     (y1, m1, d1) = toGregorian day1
--     (y2, m2, d2) = toGregorian day2
--     ym1 = y1 * 12 + toInteger m1
--     ym2 = y2 * 12 + toInteger m2
--     ymdiff = ym2 - ym1
--     ymAllowed =
--         if day2 >= day1
--             then if d2 >= d1
--                      then ymdiff
--                      else ymdiff - 1
--             else if d2 <= d1
--                      then ymdiff
--                      else ymdiff + 1
--     dayAllowed = addGregorianDurationRollOver (CalendarDiffDays ymAllowed 0) day1
--     in CalendarDiffDays ymAllowed $ diffDays day2 dayAllowed

-- -- orphan instance
public export
Show Day where
  show = showGregorian . toGregorian

public export
Show Gregorian where
  show = showGregorian

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Baum

-- ein Baum ist entweder ein leeres Blatt
-- oder ein Ast mit einem Wert und zwei Unterbäumen
-- überlege wie der entsprechende Datentyp aussehen könnte

-- data Baum : ... where
--  Blatt : Baum a
--  Ast : ... -> Baum a

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

-- ähnlich `Elem` für den Vektor wollen wir eine Datenstruktur
-- die "beweist", dass ein Wert in einem Baum ist, indem der Weg
-- dorthin aufgezeigt wird
-- Wie kann das ausehen?

-- data PfadZu : (wert : a) -> (baum : Baum a) -> Type where
-- ??? lass Dich von Elem / IstDrin inspirieren

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

-- jetzt müssen wir noch entscheiden, ob wir einen Weg finden können

-- gibtEsPfad : DecEq a => (zu : a) -> (baum : Baum a) -> Dec (PfadZu zu baum)

----------------------------------------------------------------------
-- Wenn alles passt sollte `zu0 = Yes (IstLinks (IstRechts Hier))` sein!

-- beispiel : Baum Int
-- beispiel = Ast 2 (Ast 1 Blatt (Ast 0 Blatt Blatt)) (Ast 3 Blatt Blatt)

-- zu0 : Dec (PfadZu 0 Baum.beispiel)
-- zu0 = gibtEsPfad _ _


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

module Sif.PModel

import public GRL.Common
import public GRL.IR
import public GRL.Model
import public GRL.Builder
import public GRL.Pretty

%access export
%default total

-- ------------------------------------------------------------------- [ Types ]

public export
data FTy = FuncTy | UsabTy  | ReliTy | PerfTy | SuppTy

public export
data ATy = CodeTy | ControlTy | ActionTy

public export
data LTy = ActLink | AffLink

public export
data PMTy = Req FTy | Act ATy | Link LTy | Sub GStructTy

-- ------------------------------------------------------- [ Meta Typing Rules ]

public export
data ValidLink : LTy -> PMTy -> PMTy -> Type where
  RAct : ValidLink ty (Req x) (Req y)
  MAct : ValidLink ty (Act x) (Req y)
  AAct : ValidLink ty (Act y) (Act y)

public export
data ValidDecomp : PMTy -> PMTy -> Type where
  SubR : ValidDecomp (Req x) (Req y)
  SubM : ValidDecomp (Act x) (Act y)

public export
data ValidDecomps : PMTy -> List PMTy -> Type where
  Nil  : ValidDecomps x Nil
  (::) : (x : PMTy)
      -> (y : PMTy)
      -> {auto prf : ValidDecomp x y}
      -> ValidDecomps x ys
      -> ValidDecomps z (y::ys)

-- ------------------------------------------ [ Abstract Syntax & Typing Rules ]

public export
data PModel : PMTy -> GTy -> Type where
  MkReq    : (ty : FTy) -> String -> PModel (Req ty) ELEM
  MkAction : (ty : ATy) -> String -> Maybe SValue -> PModel (Act ty) ELEM
  MkLink   : (ty : LTy)
          -> CValue
          -> PModel x ELEM
          -> PModel y ELEM
          -> {auto prf : ValidLink ty x y}
          -> PModel (Link ty) INTENT
  MkSub    : (ty : GStructTy)
          -> PModel x ELEM
          -> DList PMTy (\y => PModel y ELEM) ys
          -> {auto prf : ValidDecomps x ys}
          -> PModel (Sub ty) STRUCT

-- ----------------------------------------------------- [ Typing Type-Aliases ]

public export
FUNCTIONAL : Type
FUNCTIONAL = PModel (Req FuncTy) ELEM

public export
USABILITY : Type
USABILITY = PModel (Req UsabTy) ELEM

public export
RELIABILITY : Type
RELIABILITY = PModel (Req ReliTy) ELEM

public export
PERFORMANCE : Type
PERFORMANCE = PModel (Req PerfTy) ELEM

public export
SUPPORTABILITY : Type
SUPPORTABILITY = PModel (Req SuppTy) ELEM

public export
CODEACTION : Type
CODEACTION = PModel (Act CodeTy) ELEM

public export
CONTROL : Type
CONTROL = PModel (Act ControlTy) ELEM

public export
ACTION : Type
ACTION = PModel (Act ActionTy) ELEM

-- ---------------------------------------------------- [ Element Constructors ]

mkFunctional : String -> FUNCTIONAL
mkFunctional = MkReq FuncTy

mkUsability : String -> USABILITY
mkUsability = MkReq UsabTy

mkReliability : String -> RELIABILITY
mkReliability = MkReq ReliTy

mkPerformance : String -> PERFORMANCE
mkPerformance = MkReq PerfTy

mkSupportability : String -> SUPPORTABILITY
mkSupportability = MkReq SuppTy

mkControl : String -> Maybe SValue -> CONTROL
mkControl = MkAction ControlTy

mkCode : String -> Maybe SValue -> CODEACTION
mkCode = MkAction CodeTy

mkAction : String -> Maybe SValue -> ACTION
mkAction = MkAction ActionTy

-- -------------------------------------------------------- [ Operator Aliases ]

syntax [a] "==>" [b] "|" [c] = MkLink ActLink c a b
syntax [a] "~~>" [b] "|" [c] = MkLink AffLink c a b
syntax [a] "&=" [bs] = MkSub ANDty a bs
syntax [a] "X=" [bs] = MkSub XORty a bs
syntax [a] "|=" [bs] = MkSub IORty a bs

-- ------------------------------------------------------------- [ Interpreter ]

GRL (\ty => PModel x ty) where
  mkElem (MkReq ty  t)        = Elem GOALty t Nothing
  mkElem (MkAction ty t sval) = Elem TASKty t sval

  mkIntent (MkLink AffLink c a b) = ILink AFFECTSty c (mkElem a) (mkElem b)
  mkIntent (MkLink ActLink c a b) = ILink IMPACTSty  c (mkElem a) (mkElem b)

  mkStruct (MkSub ty x ys) = SLink ty (mkElem x) (mapDList (mkElem) ys)

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module RunElab0

import Language.Reflection

%language ElabReflection

0 elabScript : Elab Unit
elabScript = pure ()

x : Unit
x = %runElab elabScript

%runElab elabScript

main : IO Unit
main = putStrLn $ show x

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module State

import Terminal
import Document
import Data.Vect

%default total

public export
data State : Type where
  MkState : Document -> State

export
showState : State -> IO ()
showState (MkState doc) = do
  clearScreen
  showDocument doc

export
initState : Document -> State
initState doc = MkState doc

export
saveDocument : State -> IO ()
saveDocument (MkState doc) = do
  saveDocument doc
  pure ()

max_stars_repo_name: PeterHajdu/peti

max_issues_repo_name: PeterHajdu/peti

max_forks_repo_name: PeterHajdu/peti