text:
module Text.WebIDL.Types.Token

import Text.WebIDL.Types.Identifier
import Text.WebIDL.Types.Numbers
import Text.WebIDL.Types.StringLit
import Text.WebIDL.Types.Symbol

import Generics.Derive

%default total

%language ElabReflection

||| Text tokens in the WebIDL grammar. The `Invalid` token
||| is not recognized by any parser and will lead to a
||| failure during parsing.
public export
data IdlToken : Type where
  ||| Any number of white space characters
  Space     : IdlToken

  ||| A string literal
  SLit      : StringLit  -> IdlToken

  ||| An integer literal (in decimal, hexadecimal, or
  ||| octal representation)
  ILit      : IntLit     -> IdlToken

  ||| A floating point literal
  FLit      : FloatLit   -> IdlToken

  ||| Any valid identifier that is not also a
  ||| keyword.
  Ident     : Identifier -> IdlToken

  ||| A WebIDL keyword
  Key       : Keyword    -> IdlToken

  ||| A single- or multiline comment
  Comment   : String     -> IdlToken

  ||| A single symbol character (or an ellipsis: ...)
  Other     : Symbol     -> IdlToken

  ||| An unrecognized - and therefore invalid - text
  ||| token.
  Invalid   : String     -> IdlToken

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


text:
-- | Some simple arithmetic exercises.
module Koans.Arithmetic

-- | There were 32 B/W Episodes of Ivor the Engine, and 72 episodes
-- were produced altogether. How many colour episodes were produced?
addition : Bool
addition = 40 + 32 == 72

-- | B/W Episodes of Ivor the Engine were ten minutes long. If you
-- were to watch all the episodes in one sitting how many minutes
-- would it take?
multiplication : Bool
multiplication = 320 == 10 * 32

-- | In what year did the Colourised version of Ivor the Engine first air?
subtraction : Bool
subtraction = 1977 + (-1974) == 3

-- | 26 B/W episodes of Ivor the Engine were discovered in a Pig shed
-- in 2010. There were two seasons. How many episodes per season were
-- there?
division : Bool
division = (26 `div` 13) == 2

-- | There were 32 B/W episodes of ten minutes each, and 40 colour
-- episodes of five minutes each. How many minutes of Ivor the Engine
-- exist?
parentheses : Int
parentheses = (32 * 10) + (40 * 5)

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

ext: idr

max_stars_repo_name: harrisi/on-being-better

max_issues_repo_name: harrisi/on-being-better

max_forks_repo_name: harrisi/on-being-better


text:
module AOC.Day

import AOC.Solution

import AOC.Day.One
import AOC.Day.Two
import AOC.Day.Three

%default total

export
days : List (inputType ** AOCSolution inputType)
days = [ day1
       , day2
       , day3
       ]


text:
module Hello

public export
hello : String -> String
hello = ("Hello " ++)


text:
module Instances

import BoundAst

%default total
%access public export

MapType : (Monotype, Monotype)
MapType =
  ( FuncType (Term "a") (Term "b")
  , FuncType
    (TypeFullyApplied TypeclassCtr (Term "a"))
    (TypeFullyApplied TypeclassCtr (Term "b"))
  )

mapImpl : String -> Method MapType
mapImpl = Method' _

FunctorTC : Typeclass Z [MapType]
FunctorTC = TyCl "Functor"

functorInstances : List (Instance FunctorTC)
functorInstances = map Inst
  [ (Appl1 (Regular 1 "Either"), [mapImpl "Either.rmap"])
  , (Appl1 (Regular 1 "Result"), [mapImpl "Result.mapError"])
  , (Regular Z "list", [mapImpl "List.map"])
  , (Regular Z "option", [mapImpl "Option.map"])
  , (Array, [mapImpl "Array.map"])
  , (Appl1 (Tuple Z), [mapImpl "Pair.map"])
  ]

BindType : (Monotype, Monotype)
BindType =
  ( FuncType (Term "a") (TypeFullyApplied TypeclassCtr (Term "b"))
  , FuncType
    (TypeFullyApplied TypeclassCtr (Term "a"))
    (TypeFullyApplied TypeclassCtr (Term "b"))
  )

ApplyType : (Monotype, Monotype)
ApplyType =
  ( TypeFullyApplied TypeclassCtr (FuncType (Term "a") (Term "b"))
  , FuncType
    (TypeFullyApplied TypeclassCtr (Term "a"))
    (TypeFullyApplied TypeclassCtr (Term "b"))
  )

--TraverseType : (Monotype, Monotype)
--TraverseType =
--  ( FuncType (Term "a") (TypeFullyApplied (TypeCtr "m") (Term "b"))
--  , FuncType
--    (TypeFullyApplied TypeclassCtr (Term "a"))
--    (TypeFullyApplied (TypeCtr "m") (NullaryTypeAppl TypeclassCtr (Term "b")))
--  )

BimapType : (Monotype, Monotype)
BimapType =
  ( FuncType (Term "a") (Term "b")
  , FuncType
    (FuncType (Term "c") (Term "d"))
    (FuncType
      (TypeFullyApplied (NAryTypeAppl TypeclassCtr (Term "a")) (Term "c"))
      (TypeFullyApplied (NAryTypeAppl TypeclassCtr (Term "b")) (Term "d"))
    )
  )

TrimapType : (Monotype, Monotype)
TrimapType =
  ( FuncType (Term "a") (Term "b")
  , FuncType
    (FuncType (Term "c") (Term "d"))
    (FuncType
        (FuncType (Term "e") (Term "f"))
        (FuncType
            (TypeFullyApplied (NAryTypeAppl (NAryTypeAppl TypeclassCtr (Term "a")) (Term "c")) (Term "e"))
            (TypeFullyApplied (NAryTypeAppl (NAryTypeAppl TypeclassCtr (Term "b")) (Term "d")) (Term "f"))
        )
    )
  )

max_stars_repo_name: Kazark/tyclgen

max_issues_repo_name: Kazark/tyclgen

max_forks_repo_name: Kazark/tyclgen


text:
main : IO ()
main = do
  putStrLn $ show (the Bits64 0xffffffffffffffff)
  putStrLn $ show (the Bits64 0x8000000000000000)


text:
||| References:
||| - https://github.com/MarcelineVQ/idris2-streaming
||| - https://hackage.haskell.org/package/streaming
module Extra.Streaming

import System.File
import Control.Monad.Trans
import Extra.Pair
import Extra.File
import Network.Socket

||| The `Stream` type
export
data Stream : (f : Type -> Type) -> (m : Type -> Type) -> (r : Type) -> Type where
  Step : f (Stream f m r) -> Stream f m r
  Effect : m (Stream f m r) -> Stream f m r
  Return : r -> Stream f m r

export
(Functor f, Functor m) => Functor (Stream f m) where
  map f (Step x) = Step (map (map f) x)
  map f (Effect x) = Effect (map (map f) x)
  map f (Return r) = Return (f r)

||| Wrap a new layer of a `Stream`
export
wrap : f (Stream f m r) -> Stream f m r
wrap = Step

||| Wrap a new effect layer of a `Stream`
export
effect : m (Stream f m r) -> Stream f m r
effect = Effect

||| Fold a stream
export
fold : (Functor f, Functor m) => (f a -> a) -> (m a -> a) -> (r -> a) -> Stream f m r -> a
fold step effect return stream =
  case stream of
    Step x => step $ map (fold step effect return) x
    Effect x => effect $ map (fold step effect return) x
    Return r => return r

||| `fold` but different argument positions
export
build : (Functor f, Functor m) => (r -> a) -> (m a -> a) -> (f a -> a) -> Stream f m r -> a
build return effect step = fold step effect return

||| Inspect a `Stream`
export
inspect : (Functor f, Monad m) => Stream f m r -> m (Either r (f (Stream f m r)))
inspect = fold (pure . (Right . map (Effect {f} {m} . map (either Return Step)))) join (pure . Left)

||| Unfold a `Stream`
export
unfold : (Functor f, Monad m) => (a -> m (Either r (f a))) -> a -> Stream f m r
unfold f a = Effect $ do
  Right a' <- f a
    | Left r => pure (Return r)
  pure (Step (unfold f <$> a'))

mutual
  export
  (Functor f, Functor m) => Applicative (Stream f m) where
    pure x = Return x
    x <*> y = do
      x' <- x
      y' <- y
      pure (x' y')

  export
  (Functor f, Functor m) => Monad (Stream f m) where
    stream >>= f =
      case stream of
        Step x => Step (map (>>= f) x)
        Effect x => Effect (map (>>= f) x)
        Return r => f r

export
MonadTrans (Stream f) where
  lift x = Effect (map Return x)

(HasIO m, Monad (Stream f m)) => HasIO (Stream f m) where
  liftIO x = lift (liftIO x)

||| Turns a `Stream` into
export
toList : Monad m => Stream (Of a) m r -> m (List a, r)
toList = fold (\(a :> b) => map (mapFst (a ::)) b) join (\x => pure (Nil, x))

||| `toList` but discards the result of a `Stream`
export
toList_ : Monad m => Stream (Of a) m r -> m (List a)
toList_ = fold (\(a :> b) => map (a ::) b) join (const (pure Nil))

||| Construct a `Stream` from a `List` with a result type
export
fromList : Monad m => r -> List a -> Stream (Of a) m r
fromList r Nil = Return r
fromList r (a :: as) = Step (a :> fromList r as)

||| `fromList` but the result type is `()`
export
fromList_ : Monad m => List a -> Stream (Of a) m ()
fromList_ = fromList ()

||| A `Stream` of `getLine`s
export
stdinLn : HasIO m => Stream (Of String) m r
stdinLn = unfold (\_ => getLine >>= \line => pure (Right (line :> ()))) ()

||| `putStrLn` a `Stream` of `String`s
export
stdoutLn : HasIO m => Stream (Of String) m r -> m r
stdoutLn = fold (\(a :> b) => putStrLn a *> b) join pure

||| Concatenate an element into a `Stream`
export
cons : Monad m => a -> Stream (Of a) m r -> Stream (Of a) m r
cons x stream = Step (x :> stream)

||| Construct a singleton `Stream`
export
yield : Monad m => a -> Stream (Of a) m ()
yield x = Step (x :> Return ())

||| Transform the functor layer of a `Stream`
export
mapf : (Functor f, Functor m) => (forall x. f x -> g x) -> Stream f m r -> Stream g m r
mapf f stream =
  case stream of
    Return r => Return r
    Effect x => Effect (map (mapf f) x)
    Step x => Step (f (map (mapf f) x))

||| Map through a `Stream`
export
maps : Functor m => (a -> b) -> Stream (Of a) m r -> Stream (Of b) m r
maps f = mapf (mapFst f)

--- interesting streams

||| Construct a `Stream` reading from a File
export
fromFile : HasIO m => File -> Stream (Of Bits8) m (Either FileError ())
fromFile file = do
  Right a <- liftIO $ fGetChar file
    | Left err => pure (Left err)
  eof <- liftIO $ fEOF file
  if eof then pure (Right ()) else yield (cast $ ord a) *> fromFile file

||| Write to a `File` from a `Stream`
export
toFile : HasIO m => File -> Stream (Of Bits8) m r -> m (Either FileError r)
toFile file = build (pure . Right) join $ \(a :> b) => do
  Right () <- fputc a file
    | Left err => pure (Left err)
  b


text:
module Rapid.Driver

import Data.List
import Data.String
import System
import System.File

import Compiler.Common
import Compiler.VMCode
import Core.Directory
import Core.CompileExpr
import Core.Name
import Data.Utils
import Libraries.Data.SortedMap
import Libraries.Utils.Path

import Rapid.Common
import Compiler.GenLLVMIR
import Compiler.LLVM.IR
import Compiler.PrepareCode

gcStubsBDW : String
gcStubsBDW =
  """
  @_LLVM_StackMaps = constant [1 x i8] [i8 0]\n@__LLVM_StackMaps = constant [1 x i8] [i8 0]
  declare ccc %ObjPtr @GC_malloc(i64)
  declare ccc %ObjPtr @GC_malloc_atomic(i64)
  define external i8* @get_stackmap() { call ccc void @idris_rts_crash(i64 76) noreturn \n unreachable }
  \n
  """

gcStubs : CompileOpts -> String
gcStubs (MkCompileOpts _ _ Statepoint targetOs _) =
  """
  define external ccc void @GC_init() { call ccc void @idris_rts_crash(i64 76) noreturn \n unreachable }
  define external ccc void @GC_disable() { call ccc void @idris_rts_crash(i64 76) noreturn \n unreachable }
  define external ccc i8* @GC_malloc() { call ccc void @idris_rts_crash(i64 76) noreturn \n unreachable }
  \n
  """ ++
  llvmStackmapsSymbolName ++ " = external global i8\n"
  ++ "define external i8* @get_stackmap() { ret i8* " ++ llvmStackmapsSymbolName ++ "}\n"
    where llvmStackmapsSymbolName : String
          llvmStackmapsSymbolName =
            if targetOs == "darwin"
               -- on Apple platforms, an underscore is added implicitly:
               then "@_LLVM_StackMaps"
               else "@__LLVM_StackMaps"
gcStubs (MkCompileOpts _ _ BDW _ _) = gcStubsBDW
gcStubs (MkCompileOpts _ _ Zero _ _) = gcStubsBDW

gcPreamble : CompileOpts -> String
gcPreamble opts =
  ("@rapid_gc_flavour = constant i32 " ++ (show $ encodeGCFlavourAsInt $ gcFlavour opts) ++ "\n")
    ++ gcStubs opts

export
writeIR : (functions : List (Name, VMDef)) ->
          (support : String) -> (outfile : String) -> (opts : CompileOpts) -> IO ()
writeIR functions support outfile opts = do
  let nameMap = getNameMap $ map snd functions
  let indexedFuncs = enumerate functions
  let fcount = length indexedFuncs
  ignore $ fPutStrLn stderr $ "functions to compile: " ++ show (length indexedFuncs)
  (Right outFile) <- openFile outfile WriteTruncate
  | Left err => putStrLn $ "error opening output file: " ++ show err
  ignore $ fPutStr outFile support
  ignore $ fPutStr outFile (gcPreamble opts)
  ignore $ fPutStr outFile (closureHelper opts)

  for_ indexedFuncs (\c => do
    -- This dummy IO forces the `getVMIR` calls to wait until it's "their turn",
    -- otherwise we get huge memory spikes.
    ignore $ fPutStr stderr ""
    let i = 1 + fst c
    when (i `mod` 100 == 0) $ ignore $ fPutStrLn stderr ("compile fun " ++ show i ++ "/" ++ (show fcount) ++ ": " ++ safeName (fst (snd c)))
    let funcIr = getVMIR opts nameMap c
    fPutStr outFile funcIr
    )
  closeFile outFile


text:
||| Copyright 2016 Google Inc.
|||
||| Licensed under the Apache License, Version 2.0 (the "License");
||| you may not use this file except in compliance with the License.
||| You may obtain a copy of the License at
|||
|||     http://www.apache.org/licenses/LICENSE-2.0
|||
||| Unless required by applicable law or agreed to in writing, software
||| distributed under the License is distributed on an "AS IS" BASIS,
||| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
||| See the License for the specific language governing permissions and
||| limitations under the License.

module Test.Utils

import Protobuf.Core

%access export

public export PhoneType : EnumDescriptor
PhoneType = MkEnumDescriptor "Person.PhoneNumber.PhoneType" [
  MkEnumValueDescriptor "MOBILE" 0,
  MkEnumValueDescriptor "HOME" 1,
  MkEnumValueDescriptor "WORK" 2
]

public export PhoneNumber : MessageDescriptor
PhoneNumber = MkMessageDescriptor "Person.PhoneNumber" [
  MkFieldDescriptor Required PBString "number" 0,
  MkFieldDescriptor Optional (PBEnum PhoneType) "type" 1
]

namespace PhoneNumber
  getNumber : InterpMessage PhoneNumber -> String
  getNumber (MkMessage [number, _]) = number

  getType : InterpMessage PhoneNumber -> Maybe (Fin 3)
  getType (MkMessage [_, type])  = type

public export Person : MessageDescriptor
Person = MkMessageDescriptor "Person" [
  MkFieldDescriptor Required PBString "name" 0,
  MkFieldDescriptor Required PBInt32 "id" 1,
  MkFieldDescriptor Optional PBString "email" 2,
  MkFieldDescriptor Repeated (PBMessage PhoneNumber) "phone" 3
]

namespace Person
  getName : (InterpMessage Person) -> String
  getName (MkMessage [name, _, _, _]) = name

  getId : (InterpMessage Person) -> Integer
  getId (MkMessage [_, id, _, _]) = id

  getEmail : (InterpMessage Person) -> Maybe String
  getEmail (MkMessage [_, _, email, _]) = email

  getPhoneNumbers : (InterpMessage Person) -> List (InterpMessage PhoneNumber)
  getPhoneNumbers (MkMessage [_, _, _, phone_number]) = phone_number

John : InterpMessage Person
John = MkMessage [
  "John Doe",
  1234,
  Just "jdoe@example.com",
  [
    MkMessage ["123-456-7890", Just 1],
    MkMessage ["987-654-3210", Nothing]
  ]
]

max_stars_repo_name: google/idris-protobuf

max_issues_repo_name: google/idris-protobuf

max_forks_repo_name: google/idris-protobuf


text:
module Sss

import Control.Monad.State

increase : Nat -> State Nat ()
increase k = do current <- get
                put (current + k)

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module System.Logger.Simple

import Control.App
-- import System.File

import Data.Fin
import Data.Time.Clock.System

import System.IO.Handle.Unix
import System.IO.Util.GetLine

%default total

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

public export
data Priority
  = DEBUG | INFO | NOTICE | WARNING | ERROR | CRITICAL | ALERT | EMERGENCY

public export
Show Priority where
  show DEBUG = "DEBUG"
  show INFO = "INFO"
  show NOTICE = "NOTICE"
  show WARNING = "WARNING"
  show ERROR = "ERROR"
  show CRITICAL = "CRITICAL"
  show ALERT = "ALERT"
  show EMERGENCY = "EMERGENCY"

public export
Cast Priority (Fin 8) where
  cast DEBUG = 0
  cast INFO = 1
  cast NOTICE = 2
  cast WARNING = 3
  cast ERROR = 4
  cast CRITICAL = 5
  cast ALERT = 6
  cast EMERGENCY = 7

public export
Cast (Fin 8) Priority where
  cast 0 = DEBUG
  cast 1 = INFO
  cast 2 = NOTICE
  cast 3 = WARNING
  cast 4 = ERROR
  cast 5 = CRITICAL
  cast 6 = ALERT
  cast 7 = EMERGENCY

public export
Eq Priority where
  x == y = (cast {to=Fin 8} x) == cast y

public export
Ord Priority where
  compare x y = compare (cast {to=Fin 8} x) (cast y)

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

public export
LogSource : Type
LogSource = String

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

public export
record LogRecord where
  constructor MkLogRecord
  priority : Priority
  src : LogSource
  msg : Lazy String

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

public export
LogFormatter : Type -> Type
LogFormatter a = a -> LogRecord -> IO String

export nullFormatter : LogFormatter a
nullFormatter _ lr = pure lr.msg

public export
data LogFormatElm
  = LFTxt String | LFMsg
  | LFPrio | LFLoggerName
  | LFUTCTime | LFLocalTime
  | LFThreadId | LFProcessId

public export
LogFormat : Type
LogFormat = List LogFormatElm

export simpleLogFormatter : LogFormat -> LogFormatter a
simpleLogFormatter format h lr = do
  ut <- getSystemTime
  lt <- getSystemLocalTime
  pure $ concat $
    map (\x => case x of
        LFTxt x => x
        LFMsg => lr.msg
        LFPrio => show lr.priority
        LFLoggerName => lr.src
        LFUTCTime => show ut     -- FIXME: format
        LFLocalTime => show lt   -- FIXME: format
        LFThreadId => "--"       -- FIXME:
        LFProcessId => "--"      -- FIXME:
        ) format

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

public export
record LogHandler where
  constructor MkLogHandler
  priority : Priority
  {prvtyp : Type}
  privdata : prvtyp
  emit : prvtyp -> LogRecord -> IO ()
  onclose : prvtyp -> IO ()

public export
interface HasRootLogHandler m where
  getRootLogHandler : m LogHandler

export emitLogRecord : HasIO io => LogHandler -> LogRecord -> io ()
emitLogRecord h lr = when (h.priority <= lr.priority) $ liftIO $ h.emit h.privdata lr

export log : (HasIO m, Monad m, HasRootLogHandler m) => Priority -> LogSource -> String -> m ()
log prio ls msg = do
  h <- getRootLogHandler
  liftIO $ emitLogRecord h $ MkLogRecord prio ls msg

export logClose : HasIO io => LogHandler -> io ()
logClose h = liftIO $ h.onclose h.privdata

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

fdLogHandler : {ps:List Permission} -> Handle ps -> {auto ok:elem Writable ps = True}
             -> (onclose:Handle ps -> IO ())
             -> LogHandler
fdLogHandler h onclose = MkLogHandler {
    priority = DEBUG,
    privdata = h,
    emit = emitter,
    onclose = onclose }
  where
    emitter : Handle ps -> LogRecord -> IO ()
    emitter h' x = let
      fmt = [ LFLocalTime, LFTxt " ", LFLoggerName, LFTxt " ", LFMsg ]
      in do
        _ <- liftIO (simpleLogFormatter fmt () x) >>= hPutStrLn h'
        pure ()

stdoutLogHandler : LogHandler
stdoutLogHandler = fdLogHandler stdout (const (pure ()))

{-

fileLogHandler : HasIO io => String -> io (Either FileError LogHandler)
fileLogHandler filename = do
  Right h <- openFile filename Append
    | Left e => pure $ Left e
  pure $ Right $ MkLogHandler
    DEBUG File h emitter closeFile
  where
    emitter : File -> LogRecord -> IO ()
    emitter f x = let
      fmt = [ LFLocalTime, LFTxt " ", LFLoggerName, LFTxt " ", LFMsg ]
      in simpleLogFormatter fmt () x >>= fPutStrLn f >> pure ()

-}

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

public export
0 Logging : List Type -> Type
Logging = Has [State LogHandler LogHandler, PrimIO]

Has [State LogHandler LogHandler] e => HasRootLogHandler (App e) where
  getRootLogHandler = get LogHandler

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

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


text:
module Bowling

 %default total

namespace cst

  pinsNumber : Nat
  pinsNumber = 10

  totalFrames : Nat
  totalFrames = 10

data FrameStatus = Incomplete Nat
                 | ExtraRoll1 Nat
                 | ExtraRoll2 Nat Nat

data Frame = Normal Nat Nat
           | Spare Nat
           | Strike
           | LastSpecial Nat Nat Nat

data Game : (toBeCompleted : Nat) -> Type where
  NewGame : Game 10
  CompletedFrame : (frame : Frame) -> (game : Game (S tbc)) -> Game tbc
  OngoingFrame : FrameStatus -> Game (S tbc) -> Game (S tbc)

isLastFrame : (completed : Nat) -> Dec (completed = 0)
isLastFrame completed = decEq completed 0

isSpare : (first : Nat) -> (second : Nat) -> Dec (first + second = cst.pinsNumber)
isSpare first second = decEq (first + second) pinsNumber

isStrike : (first : Nat) -> Dec (first = cst.pinsNumber)
isStrike first = decEq first pinsNumber

addFrame : (completed : List Frame) -> (newFrame : Frame) -> List Frame
addFrame completed newFrame = completed ++ [newFrame]

rolls : Game (S n) -> Nat -> Either (Game (S n)) (Game n)

rolls NewGame k with (isStrike k)
  | (Yes _) = Right (CompletedFrame Strike NewGame)
  | (No _) = Left (OngoingFrame (Incomplete k) NewGame)

rolls (CompletedFrame frame game) k {n} with (isStrike k)
  | (No _) = Left (OngoingFrame (Incomplete k) (CompletedFrame frame game))
  | (Yes _) with (isLastFrame n)
     | (Yes _) = Left (OngoingFrame (ExtraRoll1 k) (CompletedFrame frame game))
     | (No _) = Right (CompletedFrame Strike (CompletedFrame frame game))

rolls (OngoingFrame (Incomplete j) y) k {n} with (isSpare j k)
  | (Yes _) with (isLastFrame n)
    | (Yes _) = Left (OngoingFrame (ExtraRoll2 j k) (OngoingFrame (Incomplete j) y))
    | (No _) = Right (CompletedFrame (Spare j) (OngoingFrame (Incomplete j) y))
  | (No _) = Right (CompletedFrame (Normal j k) (OngoingFrame (Incomplete j) y))

rolls (OngoingFrame (ExtraRoll1 j) y) k = Left (OngoingFrame (ExtraRoll2 j k) (OngoingFrame (ExtraRoll1 j) y))

rolls (OngoingFrame (ExtraRoll2 j i) y) k = Right (CompletedFrame (LastSpecial j i k) (OngoingFrame (ExtraRoll2 j i) y))

listRolls : List Frame -> List Nat
listRolls [] = []
listRolls ((Normal k j) :: xs) = k::j::listRolls xs
listRolls ((Spare k) :: xs) = k :: minus 10 k :: listRolls xs
listRolls (Strike :: xs) = pinsNumber::listRolls xs
listRolls (LastSpecial k j i :: xs) = k::j::i::listRolls xs

bonus : (numberOfRolls : Nat) -> (xs : List Frame) -> Nat
bonus n = sum . take n . listRolls

scoreFrames : (xs : List Frame) -> Nat
scoreFrames [] = 0
scoreFrames ((Normal k j) :: xs) = k + j + scoreFrames xs
scoreFrames ((Spare _) :: xs)  = pinsNumber + bonus 1 xs + scoreFrames xs
scoreFrames (Strike :: xs)       = pinsNumber + bonus 2 xs + scoreFrames xs
scoreFrames (LastSpecial k j i :: xs) = k + j + i + scoreFrames xs

listFrames : Game n -> List Frame
listFrames NewGame = []
listFrames (CompletedFrame frame game) = listFrames game ++ [frame]
listFrames (OngoingFrame x game) = listFrames game

score : Game Z -> Nat
score = scoreFrames . listFrames

-- Test

replay : List Nat -> Maybe (n ** Game n)
replay = foldlM go (_ ** NewGame)
  where

    go : (n : Nat ** Game n) -> Nat -> Maybe (n' : Nat ** Game n')
    go (Z     ** game) k = Nothing
    go ((S n) ** game) k = either (\g => (Just (_ ** g))) (\g => (Just (_ ** g))) $ rolls game k

score' : Maybe (n ** Game n) -> Maybe Nat
score' Nothing = Nothing
score' (Just ((S _) ** _)) = Nothing
score' (Just (Z ** game)) = Just (score game)

--

allInTheGuttersScoresZero : score' (replay (replicate 20 0)) = Just 0
allInTheGuttersScoresZero = Refl

allOneDownsScores20 : score' (replay (replicate 20 1)) = Just 20
allOneDownsScores20 = Refl

strikeScoringIsOK : score' (replay (10::3::6::replicate 16 0)) = Just 28
strikeScoringIsOK = Refl

perfectScoreIs300 : score' (replay (replicate 12 10)) = Just 300
perfectScoreIs300 = Refl

lastFrameSpareScoresIsOk : score' (replay (replicate 18 0 ++ [5,5,3])) = Just 13
lastFrameSpareScoresIsOk = Refl

spareScoringIsOK :  (notStrike : Not (fstRoll = 10))
                 -> (spareProof : (fstRoll + sndRoll = 10))
                 -> (thirdNotStrike : Not (thirdRoll = 10))
                 -> score' (replay (fstRoll::sndRoll::thirdRoll::replicate 17 0)) = Just ((fstRoll + sndRoll + thirdRoll) + thirdRoll)
spareScoringIsOK notStrike spareProof thirdNotStrike {fstRoll} {sndRoll} {thirdRoll} with (isStrike fstRoll)
  | (Yes prf) = void (notStrike prf)
  | (No  _)   with (isSpare fstRoll sndRoll)
    | (No notASpare) = void (notASpare spareProof)
    | (Yes _) with (isStrike thirdRoll)
      | (Yes prf) = void (thirdNotStrike prf)
      | (No _) with (isSpare thirdRoll 0)
        | (Yes secondFrameIsASpare) =  void (thirdNotStrike (rewrite sym (plusZeroRightNeutral thirdRoll) in secondFrameIsASpare))
        | (No _) = rewrite spareProof in rewrite (plusZeroRightNeutral thirdRoll) in rewrite (plusZeroRightNeutral thirdRoll) in Refl

max_stars_repo_name: berewt/live-coding

max_issues_repo_name: berewt/live-coding

max_forks_repo_name: berewt/live-coding


text:
test : List Nat -> List Nat
test [] = []
test (n :: ns) = ?n :: ns

replicate : (n : Nat) -> a -> List a
replicate Z a = []
replicate (S n) a = a :: replicate n a

testReplicate : test (replicate (1+n) k) === replicate (2+n) k
testReplicate = ?goal


text:
import Arith
import ArithCmd
import ArithCmdDo
import ArithTotal
import Greet
import InfIO
import InfList
import Label
import RunIO
import Streams
import StreamFail


text:
module Prims

x : Int
x = 42

foo : String
foo = "Sausage machine"

bar : Char
bar = 'Z'

quux : Bool
quux = False

plus' : Nat -> Nat -> Nat
plus' Z y = y
plus' (S k) y = S (plus k y)

mult' : Nat -> Nat -> Nat
mult' Z y = Z
mult' (S k) y = plus y (mult k y)

reverse' : List a -> List a
reverse' xs =  revAcc [] xs where
    revAcc : List a -> List a -> List a
    revAcc acc [] = acc
    revAcc acc (x :: xs) = revAcc (x :: acc) xs

foo' : Int -> Int
foo' x = case isLT of
        YES => x*2
        NO => x*4
    where
        data MyLT = YES | NO

        isLT: MyLT
        isLT = if x<20 then YES else NO

-- 一般 where 从句中定义的函数和其它顶层函数一样，都需要类型声明
-- 函数 f 的类型声明可以在以下情况中省略
-- 1. f 出现在顶层定义的右边
-- 2. f 的类型完全可以通过其首次应用来确定

even' : Nat -> Bool
even' Z = True
even' (S k) = odd' k where
    odd' Z = False
    odd' (S k) = even' k

max_stars_repo_name: lonelyhentai/workspace

max_issues_repo_name: lonelyhentai/workspace

max_forks_repo_name: lonelyhentai/workspace


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Module      : XML.XPath.Parser
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
--
-- Turn an xpath dsl instance to edsl
-- --------------------------------------------------------------------- [ EOH ]
module XML.XPath.Parser

import public Text.Lexer
import public Text.Parser

import public Commons.Text.Lexer.Run
import public Commons.Text.Parser.Support
import public Commons.Text.Parser.Run

import XML.DOM

import XML.XPath.Types

%access private

keywords : List String
keywords = ["text", "comment", "cdata"]

symbols : String
symbols = "@()*/"

tokenMap : TokenMap Token
tokenMap =
  [ (space, WS)
  , (oneOf symbols, Symbol)
  ]
  ++
     Functor.map (\x => (exact x, ReservedNode)) keywords
  ++
  [ (alphaNums, UserNode)
  , (any, NotRecog)
  ]

keep : TokenData Token -> Bool
keep t = case tok t of
  WS _ => False
  _ => True

export
XPathLexer : Lexer Token
XPathLexer = MkLexer tokenMap keep EndInput

export
lexXPathStr : String -> Either LexError (List (TokenData Token))
lexXPathStr = lexString XPathLexer

export
lexXPathFile : String -> IO $ Either LexFail (List (TokenData Token))
lexXPathFile = lexFile XPathLexer

public export
Parser : (a : Type) -> Type
Parser = Rule Token

ParserE : (a : Type) -> Type
ParserE = RuleEmpty Token

eoi : RuleEmpty Token ()
eoi = eoi isEOI

  where
    isEOI : Token -> Bool
    isEOI EndInput = True
    isEOI _ = False

nodeIs : String -> Parser ()
nodeIs str =
  match ("Expected Symbol '" ++ str ++ "'")
        ()
        (ReservedNode str)

node : Parser String
node = terminalF "Expected node"
                   (\x => case tok x of
                            (UserNode s) => Just s
                            _          => Nothing)

symbol : String -> Parser ()
symbol str =
  match ("Expected Symbol '" ++ str ++ "'")
        ()
        (Symbol str)

parens : Parser ()
parens = symbol "(" *> symbol ")" *> pure ()

-- -------------------------------------------------------------------- [ Test ]

nodeTest : Parser $ (b ** ty ** XPath ty (TEST b))
nodeTest =
      nodeIs "text" *> parens *> pure (_ ** _ ** Text)
  <|> nodeIs "comment" *> parens *> pure (_ ** _ ** Comment)
  <|> nodeIs "cdata" *> parens *> pure (_ ** _ ** CData)
  <|> do symbol "@"
         w <- node
         pure (_ ** _ ** Attr w)

-- ------------------------------------------------------------------- [ Nodes ]

nodeStr : Parser (XPath ELEMENT NODE)
nodeStr =
  do n <- node
     pure (Elem n)

nodeAny : Parser (XPath ELEMENT NODE)
nodeAny = symbol "*" *> pure Any

nodeXPath : Parser (XPath ELEMENT NODE)
nodeXPath = nodeAny <|> nodeStr

-- ------------------------------------------------------------------- [ Roots ]

aRoot : Parser (XPath ELEMENT ROOT)
aRoot = do symbol "/"
           n <- nodeXPath
           pure (Root n)

dRoot : Parser $ XPath ELEMENT ROOT
dRoot = do symbol "/"
           symbol "/"
           n <- nodeXPath
           pure $ DRoot n

root : Parser $ XPath ELEMENT ROOT
root = aRoot <|> dRoot

-- ------------------------------------------------------------------- [ Paths ]

data ParseRes = P (XPath ty PATH)
              | N (XPath ty NODE)
              | T (XPath ty (TEST b))

mutual
  pathelem : Parser $ ParseRes
  pathelem = do {res <- nodeTest; pure $ T (snd (snd res))}
         <|> do {res <- decpath; pure $ P (snd res)}
         <|> do {res <- anypath; pure $ P (snd res)}
         <|> map N nodeXPath

  thing : XPath ELEMENT ROOT -> ParseRes -> (ty ** XPath ty PATH)
  thing r (P p) = (_ ** r </> p)
  thing r (N n) = (_ ** r </> n)
  thing r (T t) = (_ ** r </> t)

  thing' : XPath ELEMENT NODE -> ParseRes -> (ty ** XPath ty PATH)
  thing' r (P p) = (_ ** r </> p)
  thing' r (N n) = (_ ** r </> n)
  thing' r (T t) = (_ ** r </> t)

  abspath : Parser $ (ty ** XPath ty PATH)
  abspath = do r <- root
               symbol "/"
               pelem <- pathelem
               pure (thing r pelem)

  anypath : Parser $ (ty ** XPath ty PATH)
  anypath = do r <- nodeXPath
               symbol "/"
               pelem <- pathelem
               pure (thing' r pelem)

  decpath : Parser $ (ty ** XPath ty PATH)
  decpath = do r <- nodeXPath
               symbol "/"
               symbol "/"

               pelem <- pathelem
               pure (thing' r pelem)

path : Parser $ (ty ** XPath ty PATH)
path = decpath <|> anypath <|> abspath

export
query : Parser $ (ty ** XPath ty QUERY)
query = do {res <- nodeTest;  pure (_ ** Query (snd (snd res)))}
    <|> do {res <- path;      pure (_** Query (snd res))}
    <|> do {res <- root;      pure (_ ** Query res)}
    <|> do {res <- nodeXPath; pure (_ ** Query res)}
{-
export
parseQuery : Parser $ (ty ** XPath ty QUERY)
parseQuery = do (_ ** _ ** res) <- nodetest; pure $ (_ ** Query res)
         <|> do (_ ** res) <- path; pure $ (_ ** Query res)
         <|> do res <- root; pure (_ ** Query res)
         <|> do res <- node; pure (_ ** Query res)
         <?> "XPath Query"
  -}

export
parseXPathStr : (doc : String)
             -> (Either (Run.ParseError Token) (ty ** XPath ty QUERY))
parseXPathStr = parseString XPathLexer query

export
parseXMLPathFile : (fname : String)
               -> IO (Either (Run.ParseError Token) (ty ** XPath ty QUERY))
parseXMLPathFile = parseFile XPathLexer query

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

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
module Data.List1

%default total

infixr 7 :::

public export
record List1 a where
  constructor (:::)
  head : a
  tail : List a

------------------------------------------------------------------------
-- Conversion

||| Forget that a list is non-empty
public export
forget : (1 xs : List1 a) -> List a
forget (x ::: xs) = x :: xs

||| Check whether a list is non-empty
export
fromList : (1 xs : List a) -> Maybe (List1 a)
fromList [] = Nothing
fromList (x :: xs) = Just (x ::: xs)

------------------------------------------------------------------------
-- Basic functions

public export
singleton : (1 x : a) -> List1 a
singleton a = a ::: []

export
last : List1 a -> a
last (x ::: xs) = loop x xs where

  loop : a -> List a -> a
  loop x [] = x
  loop _ (x :: xs) = loop x xs

export
foldr1' : (a -> b -> b) -> (a -> b) -> List1 a -> b
foldr1' c n (x ::: xs) = loop x xs where

  loop : a -> List a -> b
  loop a [] = n a
  loop a (x :: xs) = c a (loop x xs)

export
foldr1 : (a -> a -> a) -> List1 a -> a
foldr1 c = foldr1' c id

export
foldl1 : (a -> b) -> (b -> a -> b) -> List1 a -> b
foldl1 n c (x ::: xs) = foldl c (n x) xs

------------------------------------------------------------------------
-- Append

export
appendl : (1 xs : List1 a) -> (1 ys : List a) -> List1 a
appendl (x ::: xs) ys = x ::: xs ++ ys

export
append : (1 xs, ys : List1 a) -> List1 a
append xs ys = appendl xs (forget ys)

export
lappend : (1 xs : List a) -> (1 ys : List1 a) -> List1 a
lappend [] ys = ys
lappend (x :: xs) ys = append (x ::: xs) ys

------------------------------------------------------------------------
-- Cons/Snoc

public export
cons : (1 x : a) -> (1 xs : List1 a) -> List1 a
cons x xs = x ::: forget xs

export
snoc : (1 xs : List1 a) -> (1 x : a) -> List1 a
snoc xs x = append xs (singleton x)

------------------------------------------------------------------------
-- Reverse

public export
reverseOnto : (1 acc : List1 a) -> (1 xs : List a) -> List1 a
reverseOnto acc [] = acc
reverseOnto acc (x :: xs) = reverseOnto (x ::: forget acc) xs

public export
reverse : (1 xs : List1 a) -> List1 a
reverse (x ::: xs) = reverseOnto (singleton x) xs

------------------------------------------------------------------------
-- Instances

export
Semigroup (List1 a) where
  (<+>) = append

export
Functor List1 where
  map f (x ::: xs) = f x ::: map f xs

export
Applicative List1 where
  pure x = singleton x
  f ::: fs <*> xs = appendl (map f xs) (fs <*> forget xs)

export
Monad List1 where
  (x ::: xs) >>= f = appendl (f x) (xs >>= forget . f)

export
Foldable List1 where
  foldr c n (x ::: xs) = c x (foldr c n xs)

export
Show a => Show (List1 a) where
  show = show . forget

export
Eq a => Eq (List1 a) where
  (x ::: xs) == (y ::: ys) = x == y && xs == ys

export
Ord a => Ord (List1 a) where
  compare xs ys = compare (forget xs) (forget ys)

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

export
consInjective : the (List1 a) (x ::: xs) === (y ::: ys) -> (x === y, xs === ys)
consInjective Refl = (Refl, Refl)


text:
||| Spec: https://webassembly.github.io/spec/core/valid/conventions.html
module WebAssembly.Validation.Conventions

import public WebAssembly.Validation.Conventions.Contexts

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module JsonTest

import Json

import Lightyear.Testing

%access export

test : String -> IO ()
test s = case parse jsonToplevelValue s of
  Left err => putStrLn $ "error: " ++ err
  Right v  => printLn v

jsonTests : IO ()
jsonTests = runTests
  [ parseTestCmpShow
      "JSON 1"
      jsonToplevelValue
      "[1,2,4,[5,6],null,{\"some\":[\"object\"]},false]"
      "[1, 2, 4, [5, 6], null, {\"some\": [\"object\"]}, false]"
  , parseTestCmpShow
      "JSON 2"
      jsonToplevelValue
      "{\n  \"hallo\":42,\"nichts\":null}"
      "{\"hallo\": 42, \"nichts\": null}"

  , parseTestCmpShow
      "JSON 3"
      jsonToplevelValue
      "{\"hello\": [{\"world\": false}, 3, \"string\", true, null]}"
      "{\"hello\": [{\"world\": false}, 3, \"string\", true, null]}"

  , parseTestCmpNot
      "JSON 4"
      jsonToplevelValue
      "{{\n  \"hallo\":42,\"nichts\":null}"
      """At 1:1:
	character '['
At 1:1:
	a different token
At 1:2:
	character '}'
At 1:2:
	a different token"""
  ]


text:
module Instances.TrustInteger

import Common.Util
import Common.Interfaces
import Specifications.DiscreteOrderedGroup
import Specifications.OrderedRing
import Instances.Notation

%default total
%access public export

data IntegerLeq : Integer -> Integer -> Type where
  CheckIntegerLeq : So (intToBool (prim__slteBigInt a b)) -> IntegerLeq a b

soIntegerLeq : IntegerLeq a b -> So (intToBool (prim__slteBigInt a b))
soIntegerLeq (CheckIntegerLeq so) = so

decideLeq : (a,b : Integer) -> Dec (IntegerLeq a b)
decideLeq a b = case isItSo (intToBool (prim__slteBigInt a b)) of
  Yes oh => Yes (CheckIntegerLeq oh)
  No contra => No (contra . soIntegerLeq)

implementation Ringops Integer where Ng = negate

implementation Decidable [Integer, Integer] IntegerLeq where
  decide = decideLeq

postulate integerDiscreteOrderedRing :
  specifyDiscreteOrderedRing {leq = IntegerLeq}

integerDiscreteOrderedGroup : specifyDiscreteOrderedGroup {leq = IntegerLeq}
integerDiscreteOrderedGroup = discreteOrderedGroup integerDiscreteOrderedRing

integerPartiallyOrderedGroup : specifyPartiallyOrderedGroup {leq = IntegerLeq}
integerPartiallyOrderedGroup = partiallyOrderedGroup integerDiscreteOrderedGroup

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Minecraft.Base.PreClassic.Dirt.Block.Export

import public Minecraft.Core.Entity
import public Minecraft.Base.PreClassic.Dirt.Block
import public Minecraft.Base.PreClassic.Dirt.Item
import public Minecraft.Base.PreClassic.Dirt.ItemEntity

%default total

public export
Eq Dirt.Block where
  x == y = True

public export
Serialize Dirt.Block where
  identifier = "Dirt.Block"
  serialize x = JObject [
    ("waterLogged", JBoolean x.base.waterLogged)
  ]

public export
Deserialize Dirt.Block where
  deserialize (JObject [
    ("waterLogged", JBoolean waterLogged)
  ]) = Just $ Dirt.MkBlock {base = (GenericData.MkBlock {waterLogged = waterLogged})}
  deserialize _ = Nothing

[dirtBlock']
Block Dirt.Block where
  id = Item.id {self = Dirt.Item}

[breakDirt']
Break Dirt.Block where
  breakBlk self = [new Dirt.ItemEntity Dirt.MkItemEntity]

[dirtVtbl']
Vtbl Dirt.Block where
  vtable (Block    Dirt.Block) = Just dirtBlock
  vtable (Break    Dirt.Block) = Just breakDirt
  vtable (Tangible Dirt.Block) = Just %search
  vtable _ = Nothing

dirtBlock = dirtBlock'
breakDirt = breakDirt'
dirtVtbl  = dirtVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module WordLength

allLengths : List String -> List Nat
allLengths [] = []
allLengths (x :: xs) = length x :: allLengths xs

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


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

import Effects
import Effect.System
import Effect.Default
import Effect.State
import Effect.Exception
import Effect.File
import Effect.StdIO
import Effect.Logging.Default
import Effect.Perf

import Lightyear
import Lightyear.Strings

import Config.Error
import Config.YAML

import Data.GraphViz.SimpleDot
import XML.DOM

import Sif.Types
import Sif.AbsSyntax
import Sif.Pattern
import Sif.DSL.State
import Sif.DSL.Parser.Problem
import Sif.DSL.Parser.Solution
import Sif.DSL.Parser
import Sif.DSL

import Sif.Effs
import Sif.Error
import Sif.Library

import Sif.Options
import Sif.Prelude

%default partial
%access export

||| Print results of evaluation
printResults : EvalResult -> Sif ()
printResults Bad        = Sif.raise ResultInvalid
printResults (Good is)  = do
    let is' = map (\(t,s) => unwords [showSValue s,"\t==>\t", t]) is
    putStrLn $ unlines is'
  where
    showSValue : Maybe SValue -> String
    showSValue Nothing  = "Nothing"
    showSValue (Just x) = show x

||| Syntax check a Problem or a solution pairing.
doSyntaxCheck : Maybe String -> Maybe String -> Sif ()

doSyntaxCheck (Just x) (Just y) = do
    readSifFile problem x
    readSifFile solution y
    pure ()

doSyntaxCheck (Just x) (Nothing) = do
    readSifFile problem x
    pure ()

doSyntaxCheck (Nothing) (Just y) = do
    readSifFile solution y
    pure ()

doSyntaxCheck (Nothing) (Nothing) = Sif.raise NoFileGiven

evalAndPrintPattern : (PATTERN impl d) -> Sif ()
evalAndPrintPattern p = do
  let tname = unwords ["Evaluating:", SifExpr.getTitle p]
  trace tname
  mkTimer tname
  startTimer tname
  let eRes = evalPattern p
  stopTimer tname
  printResults eRes

tryToBuildPatternE : SifBuilder impl
             -> Maybe String
             -> Maybe String
             -> Sif (d ** PATTERN impl d)
tryToBuildPatternE bob Nothing Nothing   = Sif.raise NoFileGiven
tryToBuildPatternE bob Nothing  _        = Sif.raise (FileMissing ("Solution File "))
tryToBuildPatternE bob _        Nothing  = Sif.raise (FileMissing ("Problem File "))
tryToBuildPatternE bob (Just p) (Just s) = do
  let tname = unwords ["Building for ", p, "&", s]
  mkTimer tname
  startTimer tname
  patt <- patternFromFile bob p s
  stopTimer tname
  pure patt

evalPatternFromFile : Maybe String -> Maybe String -> Sif ()
evalPatternFromFile p' s' = do
  bob <- getSifBackend
  (_ ** p) <- tryToBuildPatternE (builder bob) p' s'
  putStrLn $ unwords ["loaded", SifExpr.getTitle p]
  evalAndPrintPattern p

printPattern : PATTERN impl d -> Maybe SifOutFormat -> Sif ()
printPattern _ Nothing    = printLn NoFormatSpecified
printPattern p (Just fmt) = do
    let tname = unwords ["Converting", show $ SifExpr.getTitle p, "to", show fmt]
    mkTimer tname
    startTimer tname
    let res = showConvPattern fmt p
    stopTimer tname
    case res of
      Nothing  => printLn UnSuppFormat
      Just res => putStrLn res

convPatternFromFile : Maybe String
                   -> Maybe String
                   -> Maybe String
                   -> Maybe SifOutFormat
                   -> Sif ()
convPatternFromFile p s fname fmt = do
    bob <- getSifBackend
    (_ ** p) <- tryToBuildPatternE (builder bob) p s
    case fname of
      Nothing => printPattern p fmt
      Just _  => printLn FeatureNotImpl

-- ------------------------------------------------------- [ Library Functions ]

importPreludeIDX : String -> List (String, String) -> Sif ()
importPreludeIDX _      Nil         = pure ()
importPreludeIDX nspace ((p,s)::ps) = do
    trace $ unlines [ "Trying to build:"
                    , "\tProblem File: "  ++ show (pDir p)
                    , "\tSolution File: " ++ show (pDir s)]
    bob <- getSifBackend
    (_ ** patt) <- tryToBuildPatternE (builder bob) (pDir p) (pDir s)
    updateLibrary (\idx => addToLibrary patt idx)
    importPreludeIDX nspace ps
  where
    pDir : String -> Maybe String
    pDir f = Just $ with List concat [nspace,"/",f]

loadPrelude : Sif ()
loadPrelude = do
    mkTimer "prelude-loading"
    putLibrary emptyLib
    opts <- getOptions
    case (prelude opts) of
      Nothing   => pure ()
      Just pdir => do
        putStrLn $ unwords ["Importing Prelude:", pdir]
        case !(readYAMLConfig (pdir ++ "/index.yaml")) of
          Left err   => printLn err
          Right pIDX =>
            case filterPreludeIDX pIDX of
              Nil => printLn ImportError
              ps  => do
                  startTimer "prelude-loading"
                  importPreludeIDX pdir ps
                  stopTimer "prelude-loading"

listLibrary : Sif ()
listLibrary = do
    l <- getLibrary
    let idx = (getLibraryIndex l)
    putStrLn "Patterns"
    putStrLn (indexToString idx)

getPatternByIndexEff : Nat -> Sif (d ** (impl ** PATTERN impl d))
getPatternByIndexEff n =
  case getPatternByIndex n !getLibrary of
    Nothing => Sif.raise NoSuchPattern
    Just p' => pure p'

getAndEvalPattern : Nat -> Sif ()
getAndEvalPattern n = do
  (_ ** (_ ** p)) <- getPatternByIndexEff n
  evalAndPrintPattern p

getAndPrintPattern : Nat
                  -> Maybe SifOutFormat
                  -> Sif ()
getAndPrintPattern n fmt = do
  (_ ** (_ ** p)) <- getPatternByIndexEff n
  printPattern p fmt

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Elab3

import BC
import public Language.Reflection.Utils

%language ElabReflection

quicksort : List Nat -> List Nat
quicksort [] = []
quicksort (x::xs) =
  quicksort (filter (< x) xs) ++
  x :: quicksort (filter (>= x) xs)

--%runElab bc `{quicksort} `{{qs'}} `{{QSAcc}}
-- %runElab bc' `{quicksort} `{{qs'}} `{{qs2}}  `{{QSAcc}} `{{Elab3.qsProof}}

-- elab3.qsProof = ?todo

mkHole : String -> Raw -> Elab TTName
mkHole n ty =
  do s <- gensym n
     claim s ty
     pure s

auto : Elab ()
auto = do g <- goalType
          case g of
            `(() : Type) =>
              exact `(() : ())
            `((~A, ~B) : Type) =>
             do a <- mkHole "A" A
                b <- mkHole "B" B
                exact `(MkPair {A=~A} {B=~B}
                          ~(Var a) ~(Var b))
                focus a; auto
                focus b; auto

goal : ((), ((), ()))
goal = %runElab auto

partial
auto' : Elab ()
auto' = do compute
           attack
           try intros
           hs <- map fst <$> getEnv
           for_ hs $
             \ih => try (rewriteWith (Var ih))
           hypothesis <|> search' 100 []
           solve


text:
module Parser

import Data.List
import Data.Either

import Control.EffectAlgebra

import Control.Effect.Exception
import Control.Effect.Fail
import Control.Effect.State
import Control.Effect.NonDet

import Control.Monad.Identity
import Control.Monad.State
import Control.Monad.Either
import Control.Monad.List

import Control.Cont.Void

nextChar : (r : Inj (StateE (List Char)) sig)
        => (f : Inj (FailE String) sig)
        => (a : Algebra sig m)
        => m Char
nextChar = do
  c :: rest <- ask {r = List Char}
    | [] => fail "End of input"
  tell rest
  pure c

guardFail : (f : Inj (FailE e) sig)
         => (a : Algebra sig m)
         => Bool
         -> e
         -> m ()
guardFail True  e = pure ()
guardFail False e = fail e

parseChar : (e : Inj (FailE String) sig)
         => (r : Inj (StateE (List Char)) sig)
         => (a : Algebra sig m)
         => (Char -> Bool)
         -> String
         -> m Char
parseChar pred err = do
  c <- nextChar
  guardFail (pred c) err
  pure c

Parser : (sig : (Type -> Type) -> (Type -> Type)) -> (m : Type -> Type) -> Type -> Type
Parser sig m res = (e : Inj (EitherE String) sig)
                => (s : Inj (StateE (List Char)) sig)
                => (n : Inj ChoiceE sig)
                => (a : Algebra sig m)
                => m res

parseMany : m t -> Parser sig m (List t)
parseMany p = do
  Just x <- try {e = String} (map Just p) (\_ => pure Nothing)
    | _ => pure []
  map (x ::) (parseMany p)

||| Parses many A's.
testParser1 : Parser sig m (List Char)
testParser1 = parseMany (parseChar (== 'A') "Not A")

runParser1 : String -> List (Either String (List Char, List Char))
runParser1 str = runIdentity . runListT . runEitherT . runStateT (unpack str) $ testParser1
  {sig = StateE (List Char) :+: EitherE String :+: ChoiceE :+: VoidE}
  {s = L}
  {e = T L R}
  {n = T (T L R) R}
  {a = Algebra.State @{Algebra.Either @{Algebra.Concat}}}

parseAll : List (m t) -> Parser sig m (List t)
parseAll [] = pure []
parseAll (x :: xs) = map (::) x <*> parseAll xs

parseString : String -> Parser sig m (List Char)
parseString x =
  parseAll (map (\x => parseChar (x ==) "Expected \{show x}") (unpack x))

testParser2 : Parser sig m (List Char)
testParser2 = parseString "hello"

runParser2 : String -> ?
runParser2 str = runIdentity . runEitherT . runListT . runStateT (unpack str) $ testParser2
  {sig = StateE (List Char) :+: ChoiceE :+: EitherE String :+: VoidE}
  {s = L}
  {n = T L R}
  {e = T (T L R) R}
  {a = Algebra.State @{Algebra.Concat @{Algebra.Either}}}

testParser3 : Parser sig m (List Char)
testParser3 =
  oneOfM [parseString "hello", parseString "hi"]

runParser3 : String -> ?
runParser3 str = runIdentity . runListT . runEitherT . runStateT (unpack str) $ testParser3
  {sig = StateE (List Char) :+: EitherE String :+: ChoiceE :+: VoidE}
  {s = L}
  {e = T L R}
  {n = T (T L R) R}
  {a = Algebra.State @{Algebra.Either @{Algebra.Concat}}}

testParser4 : String -> Parser sig m (List Char)
testParser4 str = do
  oneOfM [parseString str, nextChar *> testParser4 str]

runParser4 : String -> String -> List Nat
runParser4 occ str =
             map ((\x => (length str `minus` length x) `minus` length occ) . fst)
           . rights
           . runIdentity
           . runListT
           . runEitherT
           . runStateT (unpack str) $ (testParser4 occ)
  {sig = StateE (List Char) :+: EitherE String :+: ChoiceE :+: VoidE}
  {s = L}
  {e = T L R}
  {n = T (T L R) R}
  {a = Algebra.State @{Algebra.Either @{Algebra.Concat}}}


text:
module Compiler.Erlang.Codegen.ErlExprToAbstractFormat

import Data.List
import Data.Nat
import Control.Monad.State

import public Compiler.Erlang.IR.ErlExpr
import public Compiler.Erlang.IR.AbstractFormat
import Compiler.Erlang.Codegen.ErlExprToAbstractFormat.Buffer
import Compiler.Erlang.Utils.String

%default total
%hide ErlExpr.Line

-- AND-GUARD

data AndGuard : Type where
  MkAndGuard : Maybe Guard -> AndGuard

fromGuard : Guard -> AndGuard
fromGuard guard = MkAndGuard (Just guard)

andGuardToGuardAlts : AndGuard -> List GuardAlt
andGuardToGuardAlts (MkAndGuard Nothing) = []
andGuardToGuardAlts (MkAndGuard (Just guard)) = [MkGuardAlt [guard]]

Semigroup AndGuard where
  MkAndGuard Nothing <+> y = y
  x <+> MkAndGuard Nothing = x
  MkAndGuard (Just x) <+> MkAndGuard (Just y) = MkAndGuard (Just (AGOp (getGuardLine x) "andalso" x y))

Monoid AndGuard where
  neutral = MkAndGuard Nothing

-- HELPER FUNCTIONS

varsToVarNames : (vars : List LocalVar) -> Vect (length vars) String
varsToVarNames [] = []
varsToVarNames (x :: xs) = show x :: varsToVarNames xs

toNonEmptyClauses : (clauses : List a) -> (def : a) -> Vect (S (length clauses)) a
toNonEmptyClauses [] def = [def]
toNonEmptyClauses (x :: xs) def = x :: toNonEmptyClauses xs def

record MatcherClause where
  constructor MkMatcherClause
  pattern : Pattern
  guard : AndGuard
  body : Expr
  preComputedValues : List (LocalVar, Expr)

wrapPreComputedValues : Line -> List (LocalVar, Expr) -> Expr -> Expr
wrapPreComputedValues l [] body = body
wrapPreComputedValues l preComputedValues@(_ :: _) body =
  let letBindings = map toLet preComputedValues
  in AEBlock {k=length letBindings} l (rewrite sym (plusCommutative (length letBindings) 1) in fromList letBindings ++ [body])
  where
    toLet : (LocalVar, Expr) -> Expr
    toLet (var, value) = AEMatch l (APVar l (show var)) value

genBinaryExpr : Line -> String -> Expr
genBinaryExpr l str =
  AEBitstring l [MkBitSegment l (AELiteral (ALCharlist l str)) ABSDefault (MkTSL Nothing Nothing (Just ABUtf8) Nothing)]

genBinaryPattern : Line -> String -> Pattern
genBinaryPattern l str =
  APBitstring l [MkBitSegment l (ABPCharlist l str) ABSDefault (MkTSL Nothing Nothing (Just ABUtf8) Nothing)]

-- CODE GENERATION

genIdrisConstant : Line -> (String -> a) -> (Literal -> a) -> IdrisConstant -> a
genIdrisConstant l fromStringValue fromLiteral constant =
  case constant of
    IInt x => fromLiteral (ALInteger l (cast x))
    IInteger x => fromLiteral (ALInteger l x)
    IB8 x => fromLiteral (ALInteger l (cast x))
    IB16 x => fromLiteral (ALInteger l (cast x))
    IB32 x => fromLiteral (ALInteger l (cast x))
    IB64 x => fromLiteral (ALInteger l x)
    IString x => fromStringValue x
    IChar x => fromLiteral (ALChar l x)
    IDouble x => fromLiteral (ALFloat l x)
    IWorldVal => fromLiteral (ALAtom l "world_val")
    IIntType => fromLiteral (ALAtom l "int_type")
    IIntegerType => fromLiteral (ALAtom l "integer_type")
    IBits8Type => fromLiteral (ALAtom l "bits8_type")
    IBits16Type => fromLiteral (ALAtom l "bits16_type")
    IBits32Type => fromLiteral (ALAtom l "bits32_type")
    IBits64Type => fromLiteral (ALAtom l "bits64_type")
    IStringType => fromLiteral (ALAtom l "string_type")
    ICharType => fromLiteral (ALAtom l "char_type")
    IDoubleType => fromLiteral (ALAtom l "double_type")
    IWorldType => fromLiteral (ALAtom l "world_type")

constExprToPattern : ErlExpr -> Maybe Pattern
constExprToPattern (ELocal l var) = pure $ APVar l (show var)
constExprToPattern (ERef l modName fnName) = Nothing
constExprToPattern (ELam l args body) = Nothing
constExprToPattern (ELet l newVar value body) = Nothing
constExprToPattern (ESequence l statements) = Nothing
constExprToPattern (EApp l expr args) = Nothing
constExprToPattern (EOp l op lhs rhs) = Nothing -- TODO: Could potentially work
constExprToPattern (ECon l name xs) = do
  exprs <- assert_total $ traverse constExprToPattern xs
  pure $ APTuple l (APLiteral (ALAtom l name) :: exprs)
constExprToPattern (EConstCase l sc xs def) = Nothing
constExprToPattern (EMatcherCase l sc xs def) = Nothing
constExprToPattern (EReceive l xs timeout def) = Nothing
constExprToPattern (ETryCatch l tryExpr okVar okExpr errorVar errorExpr) = Nothing
constExprToPattern (EBinaryConcat l bin1 bin2) = Nothing
constExprToPattern (EIdrisConstant l x) = pure $ genIdrisConstant l (genBinaryPattern l) APLiteral x
constExprToPattern (EAtom l x) = pure $ APLiteral (ALAtom l x)
constExprToPattern (EChar l x) = pure $ APLiteral (ALChar l x)
constExprToPattern (EFloat l x) = pure $ APLiteral (ALFloat l x)
constExprToPattern (EInteger l x) = pure $ APLiteral (ALInteger l x)
constExprToPattern (ECharlist l x) = pure $ APLiteral (ALCharlist l x)
constExprToPattern (EBinary l x) = pure $ genBinaryPattern l x
constExprToPattern (ENil l) = pure $ APNil l
constExprToPattern (ECons l x y) = pure $ APCons l !(constExprToPattern x) !(constExprToPattern y)
constExprToPattern (ETuple l xs) = do
  elems <- assert_total $ traverse constExprToPattern xs
  pure $ APTuple l elems
constExprToPattern (EMap l xs) = Nothing -- TODO: Could potentially work
constExprToPattern (EBufferNew l size) = Nothing
constExprToPattern (EBufferResize l bin newSize) = Nothing
constExprToPattern (EBufferFlatten l bin maxbytes) = Nothing
constExprToPattern (EBufferSetBits8 l bin loc value) = Nothing
constExprToPattern (EBufferGetBits8 l bin loc) = Nothing
constExprToPattern (EBufferSetBits16 l bin loc value) = Nothing
constExprToPattern (EBufferGetBits16 l bin loc) = Nothing
constExprToPattern (EBufferSetBits32 l bin loc value) = Nothing
constExprToPattern (EBufferGetBits32 l bin loc) = Nothing
constExprToPattern (EBufferSetBits64 l bin loc value) = Nothing
constExprToPattern (EBufferGetBits64 l bin loc) = Nothing
constExprToPattern (EBufferSetInt32 l bin loc value) = Nothing
constExprToPattern (EBufferGetInt32 l bin loc) = Nothing
constExprToPattern (EBufferSetInt64 l bin loc value) = Nothing
constExprToPattern (EBufferGetInt64 l bin loc) = Nothing
constExprToPattern (EBufferSetDouble l bin loc value) = Nothing
constExprToPattern (EBufferGetDouble l bin loc) = Nothing
constExprToPattern (EBufferSetString l bin loc value) = Nothing
constExprToPattern (EBufferGetString l bin loc len) = Nothing

mutual
  genErlExpr : ErlExpr -> State LocalVars Expr
  genErlExpr (ELocal l var) =
    pure $ AEVar l (show var)
  genErlExpr (ERef l modName fnName) =
    pure $ AERemoteRef l !(genErlExpr modName) !(genErlExpr fnName)
  genErlExpr (ELam l args body) = do
    let varNames = varsToVarNames args
    body' <- genErlExpr body
    pure $ AEFun l (length args) [MkFunClause l (map (APVar l) varNames) [] [body']]
  genErlExpr (ELet l newVar value body) = do
    let varName = show newVar
    value' <- genErlExpr value
    body' <- genErlExpr body
    pure $ AEBlock l
      [ AEMatch l (APVar l varName) value'
      , body'
      ]
  genErlExpr (ESequence l statements) = do
    statements' <- assert_total $ traverse genErlExpr statements
    pure $ AEBlock l statements'
  genErlExpr (EApp l expr args) = do
    expr' <- genErlExpr expr
    args' <- assert_total $ traverse genErlExpr args
    pure $ AEFunCall l expr' args'
  genErlExpr (EOp l opName x y) =
    pure $ AEOp l opName !(genErlExpr x) !(genErlExpr y)
  genErlExpr (ECon l name exprs) = do
    exprs' <- assert_total $ traverse genErlExpr exprs
    pure $ AETuple l (AELiteral (ALAtom l name) :: exprs')
  genErlExpr (EConstCase l sc clauses def) = do
    let defClause = MkCaseClause l (APUniversal l) [] [!(genErlExpr def)]
    generatedClauses <- assert_total $ traverse (genErlConstAlt l) clauses
    pure $ AECase l !(genErlExpr sc) (toNonEmptyClauses generatedClauses defClause)
  genErlExpr (EMatcherCase l sc matchers def) = do
    let defClause = MkCaseClause l (APUniversal l) [] [!(genErlExpr def)]
    generatedClauses <- assert_total (traverse (genErlMatcher l) matchers)
    let caseExpr = AECase l !(genErlExpr sc) (toNonEmptyClauses (map fst generatedClauses) defClause)
    pure $ wrapPreComputedValues l (concatMap snd generatedClauses) caseExpr
  -- EReceive generates the following code.
  --
  -- If matchers contain `MExact` or `MMapSubset`, the values will be pre-computed to allow
  -- the case expression to refer to existing bindings.
  --
  -- ```
  -- receive
  --   `matchers`
  -- after
  --   `timeout` ->
  --     `def`
  -- end
  -- ```
  genErlExpr (EReceive l matchers timeout def) = do
    let defClause = TimeoutAfter !(genErlExpr timeout) [!(genErlExpr def)]
    generatedClauses <- assert_total (traverse (genErlMatcher l) matchers)
    let receiveExpr = AEReceive l (map fst generatedClauses) defClause
    pure $ wrapPreComputedValues l (concatMap snd generatedClauses) receiveExpr
  -- ETryCatch generates the following code.
  --
  -- ```
  -- try `tryExpr` of
  --   `okVar` ->
  --     `okExpr`
  -- catch
  --   Class:Reason:Stacktrace ->
  --     `errorVar` = {Class, Reason, Stacktrace},
  --     `errorExpr`
  -- end
  -- ```
  genErlExpr (ETryCatch l tryExpr okVar okExpr errorVar errorExpr) = do
    exClassVar <- newLocalVar
    exReasonVar <- newLocalVar
    exStacktraceVar <- newLocalVar
    let exceptionValue = AETuple l [AEVar l (show exClassVar), AEVar l (show exReasonVar), AEVar l (show exStacktraceVar)]
    let tryCaseClause = MkCaseClause l (APVar l (show okVar)) [] [!(genErlExpr okExpr)]
    let tryCatchClause = MkCatchClause l (APVar l (show exClassVar)) (APVar l (show exReasonVar)) (APVar l (show exStacktraceVar)) []
          [ AEMatch l (APVar l (show errorVar)) exceptionValue
          , !(genErlExpr errorExpr)
          ]
    pure $ AETry l [!(genErlExpr tryExpr)] [tryCaseClause] [tryCatchClause] []
  genErlExpr (EBinaryConcat l bin1 bin2) =
    pure $ binaryConcat l !(genErlExpr bin1) !(genErlExpr bin2)
  genErlExpr (EIdrisConstant l x) =
    pure $ genIdrisConstant l (genBinaryExpr l) AELiteral x
  genErlExpr (EAtom l x) =
    pure $ AELiteral (ALAtom l x)
  genErlExpr (EChar l x) =
    pure $ AELiteral (ALChar l x)
  genErlExpr (EFloat l x) =
    pure $ AELiteral (ALFloat l x)
  genErlExpr (EInteger l x) =
    pure $ AELiteral (ALInteger l x)
  genErlExpr (ECharlist l x) =
    pure $ AELiteral (ALCharlist l x)
  genErlExpr (EBinary l x) =
    pure $ genBinaryExpr l x
  genErlExpr (ENil l) =
    pure $ AENil l
  genErlExpr (ECons l x y) =
    pure $ AECons l !(genErlExpr x) !(genErlExpr y)
  genErlExpr (ETuple l elems) = do
    elems' <- assert_total $ traverse genErlExpr elems
    pure $ AETuple l elems'
  genErlExpr (EMap l entries) = do
    entries' <- assert_total $ traverse (\(key, value) => pure $ MkAssoc l !(genErlExpr key) !(genErlExpr value)) entries
    pure $ AEMapNew l entries'
  genErlExpr (EBufferNew l size) =
    pure $ bufferNew l !(genErlExpr size)
  genErlExpr (EBufferResize l bin newSize) =
    pure $ bufferResize l !(genErlExpr bin) !(genErlExpr newSize)
  genErlExpr (EBufferFlatten l bin maxbytes) =
    pure $ bufferFlatten l !(genErlExpr bin) !(genErlExpr maxbytes)
  genErlExpr (EBufferSetBits8 l bin loc value) =
    pure $ bufferSetUnsignedInt 8 l !(genErlExpr bin) !(genErlExpr loc) !(genErlExpr value)
  genErlExpr (EBufferGetBits8 l bin loc) =
    pure $ bufferGetUnsignedInt 8 l !(genErlExpr bin) !(genErlExpr loc)
  genErlExpr (EBufferSetBits16 l bin loc value) =
    pure $ bufferSetUnsignedInt 16 l !(genErlExpr bin) !(genErlExpr loc) !(genErlExpr value)
  genErlExpr (EBufferGetBits16 l bin loc) =
    pure $ bufferGetUnsignedInt 16 l !(genErlExpr bin) !(genErlExpr loc)
  genErlExpr (EBufferSetBits32 l bin loc value) =
    pure $ bufferSetUnsignedInt 32 l !(genErlExpr bin) !(genErlExpr loc) !(genErlExpr value)
  genErlExpr (EBufferGetBits32 l bin loc) =
    pure $ bufferGetUnsignedInt 32 l !(genErlExpr bin) !(genErlExpr loc)
  genErlExpr (EBufferSetBits64 l bin loc value) =
    pure $ bufferSetUnsignedInt 64 l !(genErlExpr bin) !(genErlExpr loc) !(genErlExpr value)
  genErlExpr (EBufferGetBits64 l bin loc) =
    pure $ bufferGetUnsignedInt 64 l !(genErlExpr bin) !(genErlExpr loc)
  genErlExpr (EBufferSetInt32 l bin loc value) =
    pure $ bufferSetSignedInt 32 l !(genErlExpr bin) !(genErlExpr loc) !(genErlExpr value)
  genErlExpr (EBufferGetInt32 l bin loc) =
    pure $ bufferGetSignedInt 32 l !(genErlExpr bin) !(genErlExpr loc)
  genErlExpr (EBufferSetInt64 l bin loc value) =
    pure $ bufferSetSignedInt 64 l !(genErlExpr bin) !(genErlExpr loc) !(genErlExpr value)
  genErlExpr (EBufferGetInt64 l bin loc) =
    pure $ bufferGetSignedInt 64 l !(genErlExpr bin) !(genErlExpr loc)
  genErlExpr (EBufferSetDouble l bin loc value) =
    pure $ bufferSetDouble l !(genErlExpr bin) !(genErlExpr loc) !(genErlExpr value)
  genErlExpr (EBufferGetDouble l bin loc) =
    pure $ bufferGetDouble l !(genErlExpr bin) !(genErlExpr loc)
  genErlExpr (EBufferSetString l bin loc value) =
    pure $ bufferSetString l !(genErlExpr bin) !(genErlExpr loc) !(genErlExpr value)
  genErlExpr (EBufferGetString l bin loc len) =
    pure $ bufferGetString l !(genErlExpr bin) !(genErlExpr loc) !(genErlExpr len)

  genErlConstAlt : Line -> ErlConstAlt -> State LocalVars CaseClause
  genErlConstAlt l (MkConstAlt constant body) = do
    let pattern = genIdrisConstant l (genBinaryPattern l) APLiteral constant
    pure $ MkCaseClause l pattern [] [!(genErlExpr body)]

  genErlMatcher : Line -> ErlMatcher -> State LocalVars (CaseClause, List (LocalVar, Expr))
  genErlMatcher l matcher = do
    clause <- readErlMatcher l matcher
    pure (MkCaseClause l (pattern clause) (andGuardToGuardAlts (guard clause)) [body clause], preComputedValues clause)

  readErlMatcher : Line -> ErlMatcher -> State LocalVars MatcherClause
  readErlMatcher l (MExact expr) =
    case constExprToPattern expr of
      Just pattern => do
        let guard = neutral
        let body = !(genErlExpr expr)
        pure $ MkMatcherClause pattern guard body []
      Nothing => do
        localVar <- newLocalVar
        matchExactVar <- newLocalVar
        matchExactValue <- genErlExpr expr
        let pattern = APVar l (show localVar)
        let guard = fromGuard $ AGOp l "=:=" (AGVar l (show localVar)) (AGVar l (show matchExactVar))
        let body = AEVar l (show localVar)
        pure $ MkMatcherClause pattern guard body [(matchExactVar, matchExactValue)]
  readErlMatcher l MAny = do
    localVar <- newLocalVar
    let pattern = APVar l (show localVar)
    let guard = neutral
    let body = AEVar l (show localVar)
    pure $ MkMatcherClause pattern guard body []
  readErlMatcher l MCodepoint = do
    localVar <- newLocalVar
    let pattern = APVar l (show localVar)
    let guardVar = AGVar l (show localVar)
    let isIntegerGuard = fromGuard $ AGFunCall l "is_integer" [guardVar]
    let aboveMinValueGuard = fromGuard $ AGOp l ">=" guardVar (AGLiteral (ALInteger l 0))
    let belowMaxValueGuard = fromGuard $ AGOp l "=<" guardVar (AGLiteral (ALInteger l 1114111)) -- 0x10FFFF
    let guard = isIntegerGuard <+> aboveMinValueGuard <+> belowMaxValueGuard
    let body = AEVar l (show localVar)
    pure $ MkMatcherClause pattern guard body []
  readErlMatcher l MInteger = readSimpleGuardMatcherClause l "is_integer"
  readErlMatcher l MFloat = readSimpleGuardMatcherClause l "is_float"
  readErlMatcher l MAtom = readSimpleGuardMatcherClause l "is_atom"
  readErlMatcher l MBinary = readSimpleGuardMatcherClause l "is_binary"
  readErlMatcher l MMap = readSimpleGuardMatcherClause l "is_map"
  readErlMatcher l MPid = readSimpleGuardMatcherClause l "is_pid"
  readErlMatcher l MRef = readSimpleGuardMatcherClause l "is_reference"
  readErlMatcher l MPort = readSimpleGuardMatcherClause l "is_port"
  readErlMatcher l MAnyList = readSimpleGuardMatcherClause l "is_list"
  readErlMatcher l MNil = do
    let pattern = APNil l
    let guard = neutral
    let body = AENil l
    pure $ MkMatcherClause pattern guard body []
  readErlMatcher l (MCons x y hdVar tlVar fun) = do
    xClause <- readErlMatcher l x
    yClause <- readErlMatcher l y
    let varNames = varsToVarNames [hdVar, tlVar]
    let wrappedFun = AEFun l 2 [MkFunClause l (map (APVar l) varNames) [] [!(genErlExpr fun)]]
    let pattern = APCons l (pattern xClause) (pattern yClause)
    let guard = guard xClause <+> guard yClause
    let body = AEFunCall l wrappedFun [body xClause, body yClause]
    pure $ MkMatcherClause pattern guard body (preComputedValues xClause ++ preComputedValues yClause)
  readErlMatcher l (MList matchers fun) = do
    erlMatchers <- readErlMatchers l matchers
    let args = map fst erlMatchers
    let clauses = map snd erlMatchers
    let varNames = varsToVarNames args
    let wrappedFun = AEFun l (length args) [MkFunClause l (map (APVar l) varNames) [] [!(genErlExpr fun)]]
    let pattern = foldr (\clause, acc => APCons l (pattern clause) acc) (APNil l) clauses
    let guard = foldl (\acc, clause => guard clause <+> acc) (the AndGuard neutral) clauses
    let body = AEFunCall l wrappedFun (map body clauses)
    pure $ MkMatcherClause pattern guard body (concatMap preComputedValues clauses)
  readErlMatcher l (MTuple matchers fun) = do
    erlMatchers <- readErlMatchers l matchers
    let args = map fst erlMatchers
    let clauses = map snd erlMatchers
    let varNames = varsToVarNames args
    let wrappedFun = AEFun l (length args) [MkFunClause l (map (APVar l) varNames) [] [!(genErlExpr fun)]]
    let pattern = APTuple l (map pattern clauses)
    let guard = foldl (\acc, clause => guard clause <+> acc) (the AndGuard neutral) clauses
    let body = AEFunCall l wrappedFun (map body clauses)
    pure $ MkMatcherClause pattern guard body (concatMap preComputedValues clauses)
  readErlMatcher l (MTaggedTuple tag matchers fun) = do
    erlMatchers <- readErlMatchers l matchers
    let args = map fst erlMatchers
    let clauses = map snd erlMatchers
    let varNames = varsToVarNames args
    let wrappedFun = AEFun l (length args) [MkFunClause l (map (APVar l) varNames) [] [!(genErlExpr fun)]]
    let pattern = APTuple l (APLiteral (ALAtom l tag) :: map pattern clauses)
    let guard = foldl (\acc, clause => guard clause <+> acc) (the AndGuard neutral) clauses
    let body = AEFunCall l wrappedFun (map body clauses)
    pure $ MkMatcherClause pattern guard body (concatMap preComputedValues clauses)
  readErlMatcher l (MMapSubset matchers fun) = do
    erlMatchers <- readErlMapEntryMatchers l matchers
    let args = map fst erlMatchers
    let clauses = map snd erlMatchers
    let varNames = varsToVarNames args
    let wrappedFun = AEFun l (length args) [MkFunClause l (map (APVar l) varNames) [] [!(genErlExpr fun)]]
    let pattern = APMap l (map (\(keyVar, clause) => MkExact l (APVar l (show keyVar)) (pattern clause)) erlMatchers)
    let guard = foldl (\acc, (keyVar, clause) => guard clause <+> acc) (the AndGuard neutral) erlMatchers
    let body = AEFunCall l wrappedFun (map (\(keyVar, clause) => body clause) erlMatchers)
    pure $ MkMatcherClause pattern guard body (concatMap preComputedValues clauses)
  readErlMatcher l (MFun arity) = do
    localVar <- newLocalVar
    let pattern = APVar l (show localVar)
    let guard = fromGuard $ AGFunCall l "is_function" [AGVar l (show localVar), AGLiteral (ALInteger l (cast arity))]
    let body = AEVar l (show localVar)
    pure $ MkMatcherClause pattern guard body []
  readErlMatcher l (MTransform x xVar fun) = do
    xClause <- readErlMatcher l x
    let pattern = pattern xClause
    let guard = guard xClause
    let funClause = MkFunClause l [APVar l (show xVar)] [] [!(genErlExpr fun)]
    let body = AEFunCall l (AEFun l 1 [funClause]) [body xClause]
    pure $ MkMatcherClause pattern guard body (preComputedValues xClause)
  readErlMatcher l (MConst x body) = do
    xClause <- readErlMatcher l x
    let pattern = pattern xClause
    let guard = guard xClause
    let body = !(genErlExpr body)
    pure $ MkMatcherClause pattern guard body (preComputedValues xClause)

  readSimpleGuardMatcherClause : Line -> (fnName : String) -> State LocalVars MatcherClause
  readSimpleGuardMatcherClause l fnName = do
    localVar <- newLocalVar
    let pattern = APVar l (show localVar)
    let guard = fromGuard $ AGFunCall l fnName [AGVar l (show localVar)]
    let body = AEVar l (show localVar)
    pure $ MkMatcherClause pattern guard body []

  readErlMatchers : Line -> List (LocalVar, ErlMatcher) -> State LocalVars (List (LocalVar, MatcherClause))
  readErlMatchers l [] = pure []
  readErlMatchers l ((matcherVar, matcher) :: xs) = do
    xClause <- readErlMatcher l matcher
    xsClauses <- readErlMatchers l xs
    pure ((matcherVar, xClause) :: xsClauses)

  readErlMapEntryMatchers : Line -> List (LocalVar, ErlExpr, ErlMatcher) -> State LocalVars (List (LocalVar, MatcherClause))
  readErlMapEntryMatchers l [] = pure []
  readErlMapEntryMatchers l ((matcherVar, key, matcher) :: xs) = do
    keyVar <- newLocalVar
    keyValue <- genErlExpr key
    xClause <- readErlMatcher l matcher
    let xClause' = record { preComputedValues $= ((keyVar, keyValue) ::) } xClause
    xsClauses <- readErlMapEntryMatchers l xs
    pure ((matcherVar, xClause') :: xsClauses)

genCompileAttr : Line -> PrimTerm -> Decl
genCompileAttr l primTerm = ADAttribute l "compile" primTerm

genAttribute : ErlAttribute -> Decl
genAttribute (NoAutoImport l) = genCompileAttr l (PAtom "no_auto_import")
genAttribute (Inline l) = genCompileAttr l (PAtom "inline")
genAttribute (InlineSize l size) = genCompileAttr l (PTuple [PAtom "inline_size", PInteger (cast size)])

export
genErlModule : Line -> ErlModule -> List Decl
genErlModule exportsLine mod =
  -- NOTE: The order of declarations are important!
  genModuleName (name mod) :: map genAttribute (attributes mod) ++ [genExports (funDecls mod)] ++ map genFunDef (funDecls mod)
  where
    genModuleName : ErlModuleName -> Decl
    genModuleName (MkModuleName l name) = ADModule l name
    genExports : List ErlFunDecl -> Decl
    genExports funDecls =
      let exports = mapMaybe (\(MkFunDecl l visibility name args body) => if visibility == Public then Just (name, length args) else Nothing) funDecls
      in ADExport exportsLine exports
    genFunDef : ErlFunDecl -> Decl
    genFunDef (MkFunDecl l visibility name args body) =
      let varNames = varsToVarNames args
          expr = evalState (initLocalVars "E") (genErlExpr body)
      in ADFunDef l name (length args) [MkFunClause l (map (APVar l) varNames) [] [expr]]


text:
module Typing.Term

import public Syntax.Term
import public Loc

mutual

  public export
  record TyProgram where
    constructor MkProgram
    fileName  : String
    typedDefs : List TyDef
    dataDefs  : List DataDef
    recordDef : List RecordDef

  public export
  record TyDef where
    constructor TyDefine
    name : Name
    type : Ty
    value : TyExpr

  record TyPath where
    constructor MkTypedPath
    path : Path
    type : Ty

  public export
  data TyExpr
    = TELambda   Range Ty Name TyExpr
    | TECall     Range Ty TyExpr TyExpr
    | TEDo       Range Ty (List TyExpr)
    | TECase     Range Ty TyExpr (List (TyPat, TyExpr))
    | TEId       Path  Ty
    | TELit      Range Ty Literal

  public export
  data TyPat
    = TPaId      Name  Ty
    | TPaList    Range Ty (List TyPat)
    | TPaHdTl    Range Ty TyPat TyPat
    | TPaData    Range Ty TyPath (List TyPat)
    | TPaLit     Range Ty Literal

  public export
  data Ty
    = TyPoly     Range Path Ty
    | TySimple   Range String
    | TyArrow    Range Ty Ty
    | TyVar      Range String

  public export
  data Schema = MkSchema (List String) Ty

  Show TyPath where
    show (MkTypedPath p _) = show p

  public export
  Show Ty where
    show (TyPoly r path ty) = (show path) ++ " " ++ show ty
    show (TySimple r name) = name
    show (TyVar r name) = name
    show (TyArrow r a b) = show a ++ " -> " ++ show b

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
> import Decidable.Equality
>
> dnat : (x : Nat) -> (y : Nat) -> Maybe (x = y)
> dnat x y = ?dec

ext: lidr


text:
module Main

import Data.Vect

Matrix :  Nat -> Nat -> Type -> Type
Matrix n m a = Vect n (Vect m a)

empties : Vect m (Vect 0 a)
empties {m = Z} = []
empties {m = (S k)} = [] :: empties

transpose_helper : (row : Vect m a) -> (row_trans : Vect m (Vect k a)) -> Vect m (Vect (S k) a)
transpose_helper [] [] = []
transpose_helper (x :: xs) (y :: ys) = (x :: y) :: transpose_helper xs ys

transpose_vec: Matrix n m a -> Matrix m n a
transpose_vec [] = empties
transpose_vec (row :: rows) = let row_trans = transpose_vec rows in
  transpose_helper row row_trans

mult_vects : Num a => Vect m a -> Vect m a -> a
mult_vects [] [] = 0
mult_vects (x :: xs) (y :: ys) = x * y + mult_vects xs ys

mult_vect_mat : Num a => Vect m a -> Matrix n m a -> Vect n a
mult_vect_mat {n = Z} xs [] = replicate Z 0
mult_vect_mat {n = (S k)} xs (y :: ys) = (mult_vects xs y) :: mult_vect_mat xs ys

mult_mat : Num a => Matrix l m a -> Matrix m k a -> Matrix l k a
mult_mat [] [] = []
mult_mat [] (x :: xs) = []
mult_mat (x :: xs) as = let transposed = transpose_vec as in
                           (mult_vect_mat x transposed) :: mult_mat xs as

testMatrixA : Matrix 4 2 Nat
--testMatrixA = ( 1 :: 2 :: 3 :: Nil) :: ( 10 :: 20 :: 30 :: Nil) :: (7 :: 8 :: 9 :: Nil) :: (2 :: 4 :: 6 :: Nil) :: Nil
testMatrixA = ( 1 :: 2 :: 3 :: Nil) :: ( 10 :: 20 :: 30 :: Nil) :: (7 :: 8 :: 9 :: Nil) :: (2 :: 4 :: 6 :: Nil) :: Nil

testMatrixB : Matrix 3 4 Nat
testMatrixB = ( 1 :: 2 :: 3 :: 4 :: Nil) :: ( 10 :: 20 :: 30 :: 40 :: Nil) :: (22 :: 33 :: 44 :: 55 :: Nil) :: Nil

main : IO ()
main = putStrLn (show (mult_mat testMatrixA testMatrixB))

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Main

import Control.App
import Control.App.Console
import Decidable.Equality

import Test.Unit.Spec

import Data.Strings
import Data.String.Missing

partial main : IO ()
main = run $ consoleRunSpecSimple $ do
  describe "Data.String.Missing" $ do
    describe "strIndexV" $ do
      tests "basic" $ do
        let str0 = "0123456789"
        let len0 = length str0
        assertEqual '0' $ strIndexV{pr0=believe_me (Refl{x=True})} 0 str0
        assertEqual '1' $ strIndexV{pr0=believe_me (Refl{x=True})} 1 str0
        assertEqual '9' $ strIndexV{pr0=believe_me (Refl{x=True})} 9 str0

  describe "strSplit" $ do
    tests "basic" $ do
      let str0 = "0123456789"
      assertEqual ("012", "3456789") $ strSplit 3 str0
      assertEqual ("", "0123456789") $ strSplit 0 str0
      assertEqual ("0123456789", "") $ strSplit 10 str0
      assertEqual ("0123456789", "") $ strSplit 20 str0

  describe "strFindV" $ do
    tests "basic" $ do
      let str0 = "01234567890123456789"
      assertEqual (Just 0) $ map fst $ strFindrV (== '0') str0
      assertEqual (Just 2) $ map fst $ strFindrV (== '2') str0
      assertEqual (Just 9) $ map fst $ strFindrV (== '9') str0
      assertEqual Nothing $ map fst $ strFindrV (== 'A') str0

  describe "strFindrV" $ do
    tests "basic" $ do
      let str0 = "01234567890123456789"
      assertEqual (Just 10) $ map fst $ strFindrV (== '0') str0
      assertEqual (Just 12) $ map fst $ strFindrV (== '2') str0
      assertEqual (Just 19) $ map fst $ strFindrV (== '9') str0
      assertEqual Nothing $ map fst $ strFindrV (== 'A') str0

  describe "isPrefixOf" $ do
    tests "basic" $ do
      assertTrue $ isPrefixOf "123" "123456"
      assertTrue $ isPrefixOf "abcde" "abcde"
      assertFalse $ isPrefixOf "123" "12456"
      assertFalse $ isPrefixOf "abcde" ""