text:
module Cordial.Model.Interface.API

import Data.Vect
import Data.DList
import Data.Ranged

import Text.Markup.Edda

import Cordial.Model.Common
import Cordial.Model.Specification
import Cordial.Model.Projection

import Cordial.Model.Interface.Kinds
import Cordial.Model.Interface.Ports
import Cordial.Model.Interface.PortGroup

%default total
%access public export

(#) : Port annot labelTy endpoint endian type
   -> (Port annot labelTy endpoint endian type
    -> Port annot labelTy endpoint endian type')
   -> Port annot labelTy endpoint endian type'
(#) a f = f a

clock : (info : annot)
     -> (direction : Direction dty endpoint flow prf)
     -> (clockInfo : ClockInfo (Clock mce md mtc) direction)
     -> Port annot labelTy required endpoint endian
             (PortDesc  info' WIRE NoName (Clock mce md mtc) flow      One High opt      IP vorigin doc)
             (PPortDesc       WIRE NoName (Clock mce md mtc) direction One High required IP vorigin)
clock i d = Clock i Empty IP One NoName d High

reset : (info : annot)
     -> (direction : Direction dty endpoint flow prf)
     -> Port annot labelTy required endpoint endian
             (PortDesc  info' WIRE NoName Reset flow      One High opt      IP vorigin doc)
             (PPortDesc       WIRE NoName Reset direction One High required IP vorigin)
reset i d = Reset i Empty IP One NoName d High

interrupt : (info : annot)
         -> (direction : Direction dty endpoint flow prf)
         -> Port annot labelTy required endpoint endian
                 (PortDesc  info' WIRE NoName Interrupt flow      One High opt      IP vorigin doc )
                 (PPortDesc       WIRE NoName Interrupt direction One High required IP vorigin)
interrupt i d = Interrupt i Empty IP One NoName d High

control : (info : annot)
       -> (direction : Direction dty endpoint flow prf)
       -> Port annot labelTy required endpoint endian
               (PortDesc  info' WIRE NoName Control flow      One High opt      IP vorigin doc )
               (PPortDesc       WIRE NoName Control direction One High required IP vorigin)
control i d = Control i Empty IP One NoName d High

address : (info : annot)
       -> (w         : Whole)
       -> (direction : Direction dty endpoint flow prf)
       -> (dendian   : DataEndian endian)
       -> Port annot labelTy required endpoint endian
               (PortDesc  info' ARRAY NoName AddressWire flow      dwidth High opt      IP vorigin doc )
               (PPortDesc       ARRAY NoName AddressWire direction dwidth High required IP vorigin)
address i w d e {dwidth} = Address i Empty IP High NoName (fromWhole w dwidth) d e

bus : (info : annot)
   -> (w         : Whole)
   -> (direction : Direction dty endpoint flow prf)
   -> (dendian   : DataEndian endian)
   -> Port annot labelTy required endpoint endian
           (PortDesc  info' ARRAY NoName DataWire flow      dwidth High opt      IP vorigin doc )
           (PPortDesc       ARRAY NoName DataWire direction dwidth High required IP vorigin)
bus i w d e {dwidth} = Data i Empty IP High NoName (fromWhole w dwidth) d e

general : (info : annot)
       -> (width     : Whole)
       -> (direction : Direction dty endpoint flow prf)
       -> (dendian   : DataEndian endian)
       -> Port annot labelTy required endpoint endian
               (PortDesc  info' wty NoName General flow      dwidth High opt      IP vorigin doc )
               (PPortDesc wty NoName General direction dwidth High required IP vorigin)

general i w d e {dwidth} = General i Empty IP High NoName (fromWhole w dwidth) d e

info : (info      : annot)
    -> (width     : Whole)
    -> (direction : Direction dty endpoint flow prf)
    -> (dendian   : DataEndian endian)
    -> Port annot labelTy required endpoint endian
            (PortDesc  info' wty NoName Information flow      dwidth High opt      IP vorigin doc )
            (PPortDesc       wty NoName Information direction dwidth High required IP vorigin)
info i w d e {dwidth} = Information i Empty IP High NoName (fromWhole w dwidth) d e

namespace Modifier

  setSensitivity : (s : Sensitivity)
                -> Port annot labelTy req endpoint endian
                     (PortDesc  i' w l ty f dw s' opt origin vorigin doc )
                     (PPortDesc    w l ty d dw s' req origin vorigin)
                -> Port annot labelTy req endpoint endian
                   (PortDesc  i' w l ty f dw s opt origin vorigin doc )
                   (PPortDesc    w l ty d dw s req origin vorigin)
  setSensitivity s (General i doc origin s' l width d dendian)     = (General i doc origin s l width d dendian)
  setSensitivity s (Information i doc origin s' l width d dendian) = (Information i doc origin s l width d dendian)
  setSensitivity s (Clock i doc origin width l d s' clockInfo)     = (Clock i doc origin width l d s clockInfo)
  setSensitivity s (Address i doc origin s' l width d dendian)     = (Address i doc origin s l width d dendian)
  setSensitivity s (Data i doc origin s' l width d dendian)        = (Data i doc origin s l width d dendian)
  setSensitivity s (Reset i doc origin size l d s')                = (Reset i doc origin size l d s)
  setSensitivity s (Interrupt i doc origin size l d s')            = (Interrupt i doc origin size l d s)
  setSensitivity s (Control i doc origin size l d s')              = (Control i doc origin size l d s)

  isSystem : (src : String)
          -> Port annot labelTy req endpoint endian
               (PortDesc  i w l ty f dw s opt origin vorigin doc )
               (PPortDesc   w l ty d dw s req origin vorigin)
          -> Port annot labelTy req endpoint endian
               (PortDesc  i w l ty f dw s opt (SYSTEM src) vorigin doc )
               (PPortDesc   w l ty d dw s req (SYSTEM src) vorigin)

  isSystem src (Clock i doc o width label direction sensitivity clockInfo)    = (Clock i doc (SYSTEM src) width label direction sensitivity clockInfo)
  isSystem src (Address i doc o label direction sensitivity size dendian)     = (Address i doc (SYSTEM src) label direction sensitivity size dendian)
  isSystem src (Data i doc o label direction sensitivity size dendian)        = (Data i doc (SYSTEM src) label direction sensitivity size dendian)
  isSystem src (Reset i doc o size label direction sensitivity)               = (Reset i doc (SYSTEM src) size label direction sensitivity)
  isSystem src (Interrupt i doc o size label direction sensitivity)           = (Interrupt i doc (SYSTEM src) size label direction sensitivity)
  isSystem src (Control i doc o size label direction sensitivity)             = (Control i doc (SYSTEM src) size label direction sensitivity)
  isSystem src (General i doc o label direction sensitivity size dendian)     = (General i doc (SYSTEM src) label direction sensitivity size dendian)
  isSystem src (Information i doc o label direction sensitivity size dendian) = (Information i doc (SYSTEM src) label direction sensitivity size dendian)

  namespace PortGroup
    isSystem : (src : String)
             -> PortGroup annot labelTy endpoint endian ps pps
             -> PortGroup annot labelTy endpoint endian (map (\p => record {origin = (SYSTEM src)} p) ps) (setOrigin (SYSTEM src) pps)
    isSystem src xs with (xs)
      isSystem src xs | Empty           = Empty
      isSystem src xs | (Add port rest) = Add (isSystem src port) (isSystem src rest)
      isSystem src xs | (Skip rest)     = Skip (isSystem src rest)

  addDoc : (src : String)
        -> (p   : String -> Either String (Edda SNIPPET))
        -> Port annot labelTy req endpoint endian
                (PortDesc  i w label ty f dw s opt origin vorigin doc )
                (PPortDesc   w label ty d dw s req origin vorigin)
        -> Port annot labelTy req endpoint endian
                (PortDesc  i w label ty f dw s opt origin vorigin doc )
                (PPortDesc   w label ty d dw s req origin vorigin)
  addDoc src p (Clock i doc o width label direction sensitivity clockInfo)    = (Clock i (newDocString src p)  o width label direction sensitivity clockInfo)
  addDoc src p (Address i doc o label direction sensitivity size dendian)     = (Address i (newDocString src p)  o label direction sensitivity size dendian)
  addDoc src p (Data i doc o label direction sensitivity size dendian)        = (Data i (newDocString src p)  o label direction sensitivity size dendian)
  addDoc src p (Reset i doc o size label direction sensitivity)               = (Reset i (newDocString src p)  o size label direction sensitivity)
  addDoc src p (Interrupt i doc o size label direction sensitivity)           = (Interrupt i (newDocString src p)   o size label direction sensitivity)
  addDoc src p (Control i doc o size label direction sensitivity)             = (Control i (newDocString src p)   o size label direction sensitivity)
  addDoc src p (General i doc o label direction sensitivity size dendian)     = (General i (newDocString src p)  o label direction sensitivity size dendian)
  addDoc src p (Information i doc o label direction sensitivity size dendian) = (Information i (newDocString src p)  o label direction sensitivity size dendian)

  (:=) : (name : Name kind labelTy)
      -> Port annot labelTy req endpoint endian
              (PortDesc  i w l ty f dw s opt origin vorigin doc )
              (PPortDesc   w l ty d dw s req origin vorigin)
      -> Port annot labelTy req endpoint endian
              (PortDesc  i w name ty f dw s opt origin vorigin doc )
              (PPortDesc   w name ty d dw s req origin vorigin)
  (:=) label (General     i doc origin s l width d dendian)   = (General     i doc origin s label width d dendian)
  (:=) label (Information i doc origin s l width d dendian)   = (Information i doc origin s label width d dendian)
  (:=) label (Clock       i doc origin width l d s clockInfo) = (Clock       i doc origin width label d s clockInfo)
  (:=) label (Address     i doc origin s l width d dendian)   = (Address     i doc origin s label width d dendian)
  (:=) label (Data        i doc origin s l width d dendian)   = (Data        i doc origin s label width d dendian)
  (:=) label (Reset       i doc origin size l d s)            = (Reset       i doc origin size label d s)
  (:=) label (Interrupt   i doc origin size l d s)            = (Interrupt   i doc origin size label d s)
  (:=) label (Control     i doc origin size l d s)            = (Control     i doc origin size label d s)

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Main

import Command
import System
import State
import Data.Fin
import World
import Data.Vect
import Terminal
import Ui
import Input

%default total

data Result : Type where
  Won : Result
  Failed : Result

Eq Result where
  Won == Won = True
  Failed == Failed = True
  _ == _ = False

sleepOneSec : IO ()
sleepOneSec = usleep 1000000

resultOf : World.World -> Result
resultOf world = if (didWin world) then Won else Failed

partial
run : State -> IO Result
run (MkState world Nil) = pure $ resultOf world
run (MkState world (command::rest)) =
  let newWorld = updateWorld command world
      newState = (MkState newWorld rest)
   in do
      showState newState
      sleepOneSec
      if isOver newState
      then pure $ resultOf newWorld
      else run newState

partial
loop : State -> IO Result
loop state@(MkState world program) = do
  showState state
  Just c <- getInput | loop state
  case c of
    Quit => pure Failed
    RunProgram => run state
    AppendCommand command => loop $ MkState world (program ++ [command])
    DeleteCommand => let newProgram = maybe program id (init' program)
                      in loop $ MkState world newProgram

level1 : State
level1 =
  let turtle = MkTurtle FZ FZ North
      grid = [[Empty, Empty, Empty], [Empty, Empty, Empty], [Empty, Empty, Finish]]
      world = MkWorld turtle grid
   in (MkState world Nil)

level2 : State
level2 =
  let turtle = MkTurtle FZ FZ North
      grid = [[Empty, Empty, Empty, Empty, Empty], [Empty, Empty, Empty, Finish, Empty], [Empty, Empty, Empty, Empty, Finish]]
      world = MkWorld turtle grid
   in (MkState world Nil)

level3 : State
level3 =
  let turtle = MkTurtle FZ FZ North
      grid = [[Empty, Wall, Empty, Empty, Empty], [Empty, Wall, Empty, Finish, Empty], [Empty, Empty, Empty, Wall, Finish]]
      world = MkWorld turtle grid
   in (MkState world Nil)

levels : List State
levels = [level1, level2, level3]

partial
whileM : Monad m => (a -> Bool) -> m a -> m a
whileM pred action = do
  result <- action
  if (pred result)
  then whileM pred action
  else pure result

partial
untilSuccess : State -> IO Result
untilSuccess state = whileM ((==) Failed) (loop state)

partial
runLevels : List State -> IO (List Result)
runLevels = traverse untilSuccess

partial
main : IO ()
main = do
  setup
  runLevels levels
  tearDown

ext: idr

max_stars_repo_name: PeterHajdu/tulis

max_issues_repo_name: PeterHajdu/tulis

max_forks_repo_name: PeterHajdu/tulis


text:
import Album
import Eq
import Expr
import Fold
import Tree


text:
import Aoc
import Data.List
import Data.Strings
import Data.SortedMap as M
%default total

Bag : Type
Bag = String

Count : Type
Count = SortedMap Bag Nat

Rule : Type
Rule = (Bag, Count)

Rules : Type
Rules = SortedMap Bag Count

parseRule : String -> Maybe Rule
parseRule s =
  case words s of
    (a::b::"bags"::"contain"::rest) =>
      let
        go : List String -> List (Bag, Nat)
        go ("no"::_) = []
        go (n::c::d::_::rest) = (c++" "++d, maybe 0 id $ parsePositive n) :: go rest
        go _ = []
      in Just (a++" "++b, M.fromList (go rest))
    _ => Nothing

mergeCount : Count -> Count -> Count
mergeCount = M.mergeWith (+)

-- This function is partial, because the input might as well contain
-- a cycle of bags containing each other, which I don't want to worry
-- about handling.
partial
totalCount : Bag -> Rules -> Count
totalCount b r =
  case lookup b r of
    Nothing => M.empty
    Just c => foldl mergeCount c [map (*n) (totalCount b' r) | (b',n) <- M.toList c]

partial
main : IO ()
main = do
  rules <- M.fromList <$> parseLines parseRule
  let totals = M.fromList [(bag, totalCount bag rules) | bag <- M.keys rules]
  let shinyGold = "shiny gold"
  putStr "*   "
  printLn $ count ((>0) . sum . M.lookup shinyGold) totals
  putStr "**  "
  printLn $ map sum $ M.lookup shinyGold totals


text:
import Data.Vect

vlength : {n : Nat} -> Vect n a -> Nat
vlength [] = n
vlength (x :: xs) = n

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Web.Internal.XhrTypes

import JS

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace XMLHttpRequestResponseType

  public export
  data XMLHttpRequestResponseType = Empty
                                  | Arraybuffer
                                  | Blob
                                  | Document
                                  | Json
                                  | Text

  public export
  Show XMLHttpRequestResponseType where
    show Empty = ""
    show Arraybuffer = "arraybuffer"
    show Blob = "blob"
    show Document = "document"
    show Json = "json"
    show Text = "text"

  public export
  Eq XMLHttpRequestResponseType where
    (==) = (==) `on` show

  public export
  Ord XMLHttpRequestResponseType where
    compare = compare `on` show

  public export
  read : String -> Maybe XMLHttpRequestResponseType
  read "" = Just Empty
  read "arraybuffer" = Just Arraybuffer
  read "blob" = Just Blob
  read "document" = Just Document
  read "json" = Just Json
  read "text" = Just Text
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (XMLHttpRequestResponseType.read s)}
             -> XMLHttpRequestResponseType
  fromString s = fromJust $ read s

  export
  ToFFI XMLHttpRequestResponseType String where
    toFFI = show

  export
  FromFFI XMLHttpRequestResponseType String where
    fromFFI = read

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

export data FormData : Type where [external]

export
ToFFI FormData FormData where toFFI = id

export
FromFFI FormData FormData where fromFFI = Just

export
SafeCast FormData where
  safeCast = unsafeCastOnPrototypeName "FormData"

export data ProgressEvent : Type where [external]

export
ToFFI ProgressEvent ProgressEvent where toFFI = id

export
FromFFI ProgressEvent ProgressEvent where fromFFI = Just

export
SafeCast ProgressEvent where
  safeCast = unsafeCastOnPrototypeName "ProgressEvent"

export data XMLHttpRequest : Type where [external]

export
ToFFI XMLHttpRequest XMLHttpRequest where toFFI = id

export
FromFFI XMLHttpRequest XMLHttpRequest where fromFFI = Just

export
SafeCast XMLHttpRequest where
  safeCast = unsafeCastOnPrototypeName "XMLHttpRequest"

export data XMLHttpRequestEventTarget : Type where [external]

export
ToFFI XMLHttpRequestEventTarget XMLHttpRequestEventTarget where toFFI = id

export
FromFFI XMLHttpRequestEventTarget XMLHttpRequestEventTarget where fromFFI = Just

export
SafeCast XMLHttpRequestEventTarget where
  safeCast = unsafeCastOnPrototypeName "XMLHttpRequestEventTarget"

export data XMLHttpRequestUpload : Type where [external]

export
ToFFI XMLHttpRequestUpload XMLHttpRequestUpload where toFFI = id

export
FromFFI XMLHttpRequestUpload XMLHttpRequestUpload where fromFFI = Just

export
SafeCast XMLHttpRequestUpload where
  safeCast = unsafeCastOnPrototypeName "XMLHttpRequestUpload"

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

export data ProgressEventInit : Type where [external]

export
ToFFI ProgressEventInit ProgressEventInit where toFFI = id

export
FromFFI ProgressEventInit ProgressEventInit where fromFFI = Just


text:
foo : (x : Nat) -> case x of
                        Z => Nat -> Nat
                        S k => Nat


text:
import Data.Vect

createEmpties : Vect n (Vect 0 elem)
createEmpties {n = Z} = []
createEmpties {n = (S k)} = [] :: createEmpties

transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) = let xsTrans = transposeMat xs in
                            zipWith (::) x xsTrans

addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (+) x y :: addMatrix xs ys

multMatrixHelper : Num t => (xs : Vect n (Vect m t))
                         -> (ysTrans : Vect p (Vect m t))
                         -> Vect n (Vect p t)
multMatrixHelper [] ysTrans = []
multMatrixHelper (x :: xs) ysTrans = let topRow = multAll x ysTrans in
                                        topRow :: multMatrixHelper xs ysTrans
    where
        dotProd : Num t => Vect n t -> Vect n t -> t
        dotProd xs ys = sum (zipWith (*) xs ys)

        multAll : Num t => Vect n t -> Vect m (Vect n t) -> Vect m t
        multAll xs yss = map (dotProd xs) yss

multMatrix : Num t =>
             Vect n (Vect m t) -> Vect m (Vect p t) -> Vect n (Vect p t)
multMatrix xs ys = let ysTrans = transposeMat ys in
                multMatrixHelper xs ysTrans

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
module AutoSearchHide1

public export
interface A where
  Value : Nat

public export
[ZeroA] A where
  Value = 0

public export
%hint
HintZeroA : A
HintZeroA = ZeroA


text:
-- ----------------------------------------------------------------- [ INI.idr ]
-- Description : Read INI files.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Config.INI

import Effects
import Effect.File

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

import public Config.Error

import Config.Parse.Utils
import Config.Parse.Common

%access export

-- ------------------------------------------------------------------- [ Model ]

public export
data INIElem = INIFile (List INIElem)
             | INIEntry String String
             | INISection String (List INIElem)

public export
Show INIElem where
  show (INIFile is)   = show is
  show (INIEntry k v) = show k ++ " = " ++ show v ++ "\n"
  show (INISection t kvs) = "[" ++ t ++ "]\n" ++ show kvs

-- ------------------------------------------------------------------ [ Parser ]

private
iniComment : Parser ()
iniComment = comment ";" <|> comment "#"

private
iniSpace : Parser ()
iniSpace = langSpace iniComment <?> "INI Space"

private
kvpair : Parser INIElem
kvpair = do
    (k,v) <- keyvalue "=" (map pack $ manyTill (anyChar) (skip endOfLine <|> iniComment))
    pure $ INIEntry k v
  <?> "INI KVPair"

private
section : Parser INIElem
section = do
      name <- brackets word
      is <- some body
      pure $ INISection name is
    <?> "Section"
  where
    body : Parser INIElem
    body = iniSpace *> kvpair <?> "INI Section Body"

private
iniElem : Parser INIElem
iniElem = kvpair <|> section <?> "INI Elememnt"

parseINI : Parser INIElem
parseINI = do
    es <- some (iniSpace *> iniElem)
    pure $ INIFile es
  <?> "INI File"

-- -------------------------------------------------------------------- [ Read ]

readINIConfig : String -> Eff (Either ConfigError INIElem) [FILE ()]
readINIConfig = readConfigFile parseINI

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

max_stars_repo_name: jfdm/idris-config

max_issues_repo_name: jfdm/idris-config

max_forks_repo_name: jfdm/idris-config


text:
module FirSigned

import ClosedInt
import Synchronous

import Data.Vect
import Data.ZZ
import Data.Bits

%access export
%default total

-- The Vect implementation of Foldable breaks a proof here...
-- Let's redefine sum for now without using fold
%hide sum
sum :  Num a => Vect n a -> a
sum [] = 0
sum (x::xs) = x + sum xs

||| Combinatorial dot product over `ClosedInt`s
dotProd : (ws : Vect j ZZ)
        -> Vect j (ClosedInt n m)
        -> ClosedInt (sum $ map (multLo n m) ws)
                     (sum $ map (multHi n m) ws)
dotProd []        []        = zeros
dotProd (w :: ws) (x :: xs) = add (multConst x w) (dotProd ws xs)

||| Synchronous FIR over `ClosedInt`s
fir : (ws : Vect j ZZ)
   -> Stream (ClosedInt n m)
   -> Stream (ClosedInt (sum $ map (multLo n m) ws)
                        (sum $ map (multHi n m) ws))
fir {j} ws x = liftA (dotProd ws) (window j zeros x)

-- TODO Consider a wrapper for this with Signed

||| Example of simulating `fir`
main : IO ()
main = do let dut = fir [1,-1,2]
          let inp = map (saturate {n=0} {m=6}) $ counterFrom 0 {ty=ZZ}
          let out = take 5 $ simulate dut inp
          putStrLn $ show out

-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:


text:
module Koans.ListComprehensions

-- | What is the result of the List Comprehension.
listCompZero : Bool
listCompZero = ?fillme1 == [ x + x | x <- [1..5] ]

-- | Write a list comprehension that returns all the numbers divisible by four, doubled.
myFirstListComp : List Integer -> List Integer
myFirstListComp xs = ?fillme2

computeList : Bool
computeList = myFirstListComp [1..10] == [8,16]

-- | Return all the numbers between 20 and 100 that are divisible by 9.
divisibleByNine : List Integer
divisibleByNine = ?fillme3

-- | Using list comprehensions construct a function that turns a list of numbers into a list of strings.
-- Odd numbers should be bang, Even numbers boom.
boomBangs : List Integer -> List String
boomBangs xs = ?fillme4
               where
                 transform : Integer -> String
                 transform = ?fillme5

doBoomBangs : Bool
doBoomBangs = boomBangs [3,4,5,6,7] == ["bang", "boom", "bang", "boom", "bang"]

max_stars_repo_name: silky/idris-koans

max_issues_repo_name: silky/idris-koans

max_forks_repo_name: silky/idris-koans


text:
impure_op : Bits64 -> IO Bits64
impure_op foo = pure $ foo + 1

impure_int : IO Int
impure_int = pure 41

main : IO ()
main = impure_int >>= impure_op . prim__zextInt_B64 >>= printLn

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
-- Local Variables:
-- idris-packages: ("lightyear" "contrib")
-- End:

-- Quick and dirty bot

import Lightyear.Strings
import Network.Socket
import Prelude.Strings
import System
import Control.Monad.State
import Control.Monad.Trans

import MessyBot.Types
import MessyBot.IRCParsers
import MessyBot.NetworkUtils

Bot : Type -> Type
Bot = StateT BotState IO

action : String -> Bot String
action s = pure $ "\001ACTION " ++ s ++ "\001"

actionl : List String -> Bot (List String)
actionl s = traverse action s

-- Bot behaviour (i.e. commands) is defined below

||| A command (prefixed channel message) processor.
||| Returns a message to send back to that channel.
||| @u User nick
||| @m Message words
commandMessage : (u: String) -> (m: List String) -> Bot String
commandMessage u ["inc"] = do
  bs <- get
  put $ record { counter = counter bs + 1 } bs
  pure $ u ++ ": " ++ show (counter bs)
commandMessage _ ["slap", nick] = action $ "slaps " ++ nick
commandMessage _ _ = pure ""

||| IRC actions processor.
||| Returns a list of messages to react on an action.
||| @u User nick
||| @a Action words
actionMessages : (u: String) -> (a: List String) -> Bot (List String)
actionMessages u ["slaps", u2] = actionl ["slaps " ++ u]
actionMessages u ["hugs", u2] = actionl ["hugs " ++ u]
actionMessages _ _ = pure []

-- The rest is mostly bootstrap

||| Channel messages processor, returns a list of messages to send
||| @u User nick
||| @c Channel name
||| @m A received message
chanMessages : (u: String) -> (c: String) -> (m: String) -> Bot (List Message)
chanMessages u c m = case (strHead m) of
  ',' => do
    r <- commandMessage u (words $ strTail m)
    case r of
      "" => pure []
      msg => pure $ cmsgl c msg
  _ => case (isPrefixOf "\001ACTION " m && isSuffixOf "\001" m) of
    False => pure []
    True => case (init' $ drop 8 $ unpack m) of
      Nothing => pure []
      Just l => do
        msgs <- actionMessages u $ words $ pack l
        case msgs of
          [] => pure []
          l => pure $ map (cmsg c) msgs

||| Parsed IRC messages processor, returns a list of messages to send.
botMessages : Message -> Bot (List Message)
botMessages (Msg _ (Right 376) _) = do
  bs <- get
  pure $ map (msg "JOIN" . pure) $ channels bs
botMessages (Msg _ (Left "PING") p) = pure $ msgl "PONG" p
botMessages m@(Msg (Just (User u)) (Left "PRIVMSG") [c,msg]) = do
  bs <- get
  if c `elem` (channels bs)
  then chanMessages u c msg
  else return []
botMessages m = pure []

||| Raw IRC messages processor: simply parses them and passes to
||| botMessages. Returns a list of messages to send.
||| @s Raw message.
botLines : (s: String) -> Bot (List String)
botLines s = case (parse message s) of
  Left err => do
    lift $ putStrLn err
    return []
  Right msg => map (map show) (botMessages msg)

||| Main loop
||| @s A connected socket
botLoop : (s: Socket) -> Bot ()
botLoop s = do
  line <- lift $ recvTill s "\r\n"
  case line of
    Left err => lift $ putStrLn $ "Socket error on recv: " ++ show err
    Right str => do
      lift $ putStr $ "< " ++ str
      lines <- botLines str
      r <- lift $ traverse (sendLine s) lines
      -- might be worthwhile to check results here
      botLoop s

||| Entry point: processes args, connects, runs botLoop
main : IO ()
main = do
  args <- getArgs
  case args of
    (prog::host::port::n::u::ui::c) => do
      sock <- tcpConnect host (cast port)
      case sock of
        Nothing => putStrLn "Failed to connect"
        Just s => do
          lines <- pure (the (List String) [show $ msg "NICK" [n], show $ msg "USER" [u, "*", "*", ui]])
          traverse (sendLine s) lines
          runStateT (botLoop s) $ record { channels = c } defaultState
          return ()
    _ => putStrLn "Arguments: <server> <port> <nick> <user> <user info> [#channel1 #channel2...]"

max_stars_repo_name: defanor/hydra-bot

max_issues_repo_name: defanor/hydra-bot

max_forks_repo_name: defanor/hydra-bot


text:
module Main

import Palindrome

showPalindrome : String -> String
showPalindrome str = show (palindrome str) ++ "\n"

main : IO ()
main = repl "Enter a string: " showPalindrome

max_stars_repo_name: curtisalexander/tdd-idris

max_issues_repo_name: curtisalexander/tdd-idris

max_forks_repo_name: curtisalexander/tdd-idris


text:
-- @generated
module Server.Version

import Server.Generated
import Libraries.Data.Version

export
version : Version
version with (idrisLSPVersion)
 version | (s,"") = MkVersion s Nothing
 version | (s,t) = MkVersion s (Just t)


text:
import Data.List.Alternating

main : IO ()
main = do
    let xs = the (Odd Double String) [1, "Hello", 2, "world", 3]
    let ys = the (Odd Double String) [1, "Hello", 0, "world", 3]

    printLn xs

    printLn $ xs == xs
    printLn $ xs == ys

    printLn $ compare xs xs == EQ
    printLn $ compare xs ys == GT

    printLn $ bimap (+ 1) (++ "!") xs

    printLn $ bifoldr (mapFst . avg) (mapSnd . join) (0, "") xs
    printLn $ bifoldl (flip $ mapFst . avg) (flip $ mapSnd . (flip join)) (0, "") xs

    ignore $ bitraverse printLn printLn xs

    printLn $ map (++ "!") xs

    printLn $ the (Odd Double String) $ [1, "Hello"] ++ [2, "world", 3]
    printLn $ the (Odd Double String) $ [1, "Hello", 2] ++ ["world", 3]

    let us = the (Odd String Double) ["Hello", 0, "world", 1, "!"]
    let vs = the (Odd String Double) ["Lorem", 1, "ipsum"]

    printLn $ us <+> vs
    printLn $ us +> "!"
    printLn $ "Oh, " <+ us
    printLn $ the (Odd String Double) neutral

    printLn $ foldr avg 0 us
    printLn $ foldl avg 0 us

    printLn $ the (Odd String Double) $ pure 1
    printLn $ the (Odd String Double) $ ["Hello", (+1), "world", (+10), "!"] <*> ["Lorem", 1, "ipsum", 2, "."]

    printLn $ the (Odd String Double) empty
    printLn $ us <|> vs

    printLn $ Snd.do
        x <- the (Odd String Double) ["Hello", 1, "world", 2, "!"]
        [",", x + 1, " "]

    printLn $ Fst.do
        x <- the (Odd String Double) ["Hello", 1, "world", 2, "!"]
        ["Um,", 3, x]

    ignore $ traverse printLn us

    printLn $ odds xs
    printLn $ evens xs
    printLn $ the (List String) $ forget $ mapFst show xs
  where
    avg : Double -> Double -> Double
    avg x y = (x + y) / 2

    join : String -> String -> String
    join "" t = t
    join s "" = s
    join s t = s ++ " " ++ t


text:
module VirtualDOM

import VirtualDOM.DOM

%default total
%access private

export
data EventHandler : Type where
  On : (eventName : String) -> (handler : Ptr -> JS_IO ()) ->
       (opts : ListenerOptions) -> EventHandler

export
data Html : Type where
  HtmlElement : (tag : String) -> (events : List EventHandler) ->
                (attribs : List (String, String)) -> (children : List Html) ->
                Html
  HtmlText : String -> Html

updateAttribs : Node -> (old : List (String, String)) ->
              (new : List (String, String)) -> JS_IO ()
updateAttribs node old new =
  do
    traverse (removeAttribute node) (map fst old)
    traverse_ (uncurry $ setAttribute node) new

partial
addEventHandler : Node -> EventHandler -> JS_IO ()
addEventHandler element (On eventName handler opts) =
  addEventListener element eventName handler opts

mutual
  partial
  createDOMNodeList : List Html -> List (JS_IO Node)
  createDOMNodeList [] = []
  createDOMNodeList (node :: nodes) =
    createDOMNode node :: createDOMNodeList nodes

  partial
  createDOMNode : Html -> JS_IO Node
  createDOMNode (HtmlElement tag events attribs children) =
    do
      childNodes <- sequence $ createDOMNodeList children
      el <- createElement tag
      traverse (addEventHandler el) events
      updateAttribs el [] attribs
      traverse (appendChild el) childNodes
      pure el
  createDOMNode (HtmlText text) = createTextNode text

export
node : String -> List EventHandler -> List (String, String) -> List Html -> Html
node = HtmlElement

export
text : String -> Html
text = HtmlText

export
on : (eventName : String) -> (handler : Ptr -> JS_IO ()) ->
     (opts : ListenerOptions) -> EventHandler
on = On

indexed : (Integral n, Enum n) => List a -> List (n, a)
indexed = zipStreamList [0..]
  where
    zipStreamList : Stream n -> List a -> List (n, a)
    zipStreamList (x :: xs) [] = []
    zipStreamList (x :: xs) (y :: ys) = (x, y) :: zipStreamList xs ys

moveChildren : (count : Nat) -> (from : Node) -> (to : Node) -> JS_IO ()
moveChildren count from to =
  for_ [0..count] $ const $
    nthChild from 0 >>= removeChild from >>= appendChild to

-- This function is much longer than I prefer.
partial
renderList : (root : Node) -> (old : List (Int, Html)) -> (new : List Html) ->
             JS_IO ()
renderList root [] [] = pure ()
renderList root [] new@(_ :: _) =
  traverse createDOMNode new >>= traverse_ (appendChild root)
renderList root old@((n, _) :: _) [] =
  traverse_ (const $ nthChild root n >>= removeChild root) old
renderList root ((n, old) :: olds) (new :: news) =
  do
    case old of
      HtmlText oldText =>
        case new of
          HtmlText newText =>
            if oldText == newText
              then pure ()
              else replaceThisChild
          HtmlElement _ _ _ _ => replaceThisChild
      HtmlElement oldTag oldEvents oldAttribs oldChildren =>
        case new of
          HtmlText _ => replaceThisChild
          HtmlElement newTag newEvents newAttribs newChildren =>
            if oldTag == newTag
              then do
                {- We can't remove listeners by what we can get from an
                   EventHandler, so instead we just swap the element for
                   a new one and transfer its children. -}
                originalElement <- nthChild root n
                finalElement <- if isCons oldEvents
                  then do
                    replacementElement <- createElement newTag
                    updateAttribs replacementElement [] newAttribs
                    {- This is really inefficient. We are potentially
                       moving these children twice. This ought to
                       be integrated with the rest of the
                       differencing render. -}
                    for oldChildren $ const $
                      nthChild originalElement 0 >>=
                        removeChild originalElement >>=
                          appendChild replacementElement
                    traverse (addEventHandler replacementElement) newEvents
                    replaceChild root replacementElement originalElement
                    pure replacementElement
                  else do
                    updateAttribs originalElement oldAttribs newAttribs
                    traverse (addEventHandler originalElement) newEvents
                    pure originalElement
                renderList finalElement (indexed oldChildren) newChildren
              else replaceThisChild
    renderList root olds news
  where
    partial
    replaceThisChild : JS_IO ()
    replaceThisChild =
      do
        oldChild <- nthChild root n
        newChild <- createDOMNode new
        replaceChild root newChild oldChild
export
partial
render : (root : Node) -> (old : Maybe Html) -> (new : Maybe Html) -> JS_IO ()
render root old new =
  renderList root (indexed $ toList old) (toList new)
-- render root Nothing Nothing = pure ()
-- render root (Just oldHtml) Nothing =
--   do
--     nthChild root 0 >>= removeChild root
--     pure ()
-- render root Nothing (Just html) =
--   do
--     createDOMNode html >>= appendChild root
--     pure ()
-- render root (Just oldHtml) (Just newHtml) =
--   do
--     nthChild root 0 >>= removeChild root
--     createDOMNode newHtml >>= appendChild root
--     pure ()

max_stars_repo_name: concert/idris-vdom

max_issues_repo_name: concert/idris-vdom

max_forks_repo_name: concert/idris-vdom


text:
module B

import A


text:
module Ch05.Exercise_5_2_2

import Ch05.LambdaCalculus

%default total

||| Alternative version of the Church numeral successor
scc' : Term
scc' = Abs 0 (Abs 1 (Abs 2 (App (App (Var 0) (Var 1)) (App (Var 1) (Var 2)))))

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
%default total

interface C a (f : Bool -> Bool) | a where {}
implementation C Int Bool.not where {}

foo : C Int g => {auto pf : g True = False} -> Unit
foo = ()

main : IO ()
main = printLn $ foo -- {pf = Refl}


text:
-- --------------------------------------------------------------- [ Paths.idr ]
-- Module    : System.Posix.Paths
-- Copyright : (c) 2017 Josh Filstrup
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

module Paths

import Data.Vect

||| A type level distinguishment between files and directories.
public export
data Kind = Directory | File

||| A type level distinguishment between absolute paths and relative ones.
public export
data Anchoring = Relative | Absolute

||| An opaque path type in which paths are normalized at construction time.
|||
||| This means:
||| - '..' sequences are collapsed, i.e. foo/../bar  => bar/
|||     - Note that there is an exception here.
|||       Leading '..'s are disallowed, because we dont know how to expand them.
||| - '~'  sequences are disallowed, as they rely on the user environment.
||| - '/'  sequences are collapsed
export
data Path : (a : Anchoring) -> (f : Kind) -> Type where
  AbsoluteDirectory : String -> Path Absolute Directory
  AbsoluteFile      : String -> Path Absolute File
  RelativeDirectory : String -> Path Relative Directory
  RelativeFile      : String -> Path Relative File

-- ---------------------------------------------------------------------------
-- Implementation Details
-- ---------------------------------------------------------------------------
rmConsecutiveSlashes : String -> String
rmConsecutiveSlashes s = pack $ rmConsecutiveSlashesImpl (unpack s)
  where rmConsecutiveSlashesImpl : List Char -> List Char
        rmConsecutiveSlashesImpl [] = []
        rmConsecutiveSlashesImpl ('/' :: '/' :: cs) = rmConsecutiveSlashesImpl ('/' :: cs)
        rmConsecutiveSlashesImpl (c :: cs) = c :: rmConsecutiveSlashesImpl cs

rmDotSlashPrefix : String -> String
rmDotSlashPrefix s = pack $ rmDotSlashPrefixImpl (unpack s)
  where rmDotSlashPrefixImpl : List Char -> List Char
        rmDotSlashPrefixImpl [] = []
        rmDotSlashPrefixImpl ('.' :: '/' :: cs) = cs
        rmDotSlashPrefixImpl cs = cs

rmConsecutiveDots : String -> String
rmConsecutiveDots s = pack $ reverse $ rmConsecutiveDotsImpl $ reverse $ unpack s
  where clearNextSegment : List Char -> List Char
        clearNextSegment [] = []
        clearNextSegment (c :: cs) = if c == '/'
                                        then cs
                                        else clearNextSegment cs

        rmConsecutiveDotsImpl : List Char -> List Char
        rmConsecutiveDotsImpl [] = []
        rmConsecutiveDotsImpl ('/' :: '.' :: '.' :: '/' :: cs) = (
          rmConsecutiveDotsImpl ('/' :: clearNextSegment cs))
        rmConsecutiveDotsImpl (c :: cs) = c :: rmConsecutiveDotsImpl cs

containsTilde : String -> Bool
containsTilde s = containsTildeImpl $ unpack s
  where containsTildeImpl [] = False
        containsTildeImpl (c :: cs) = (c == '~') || containsTildeImpl cs

containsPrefixDotDot : String -> Bool
containsPrefixDotDot s = containsPrefixDotDotImpl $ unpack s
  where containsPrefixDotDotImpl : List Char -> Bool
        containsPrefixDotDotImpl [] = False
        containsPrefixDotDotImpl ('.' :: '.' :: cs) = True
        containsPrefixDotDotImpl (c :: cs) = False

containsAnyDotDot : String -> Bool
containsAnyDotDot s = containsAnyDotDotImpl $ unpack s
  where containsAnyDotDotImpl : List Char -> Bool
        containsAnyDotDotImpl [] = False
        containsAnyDotDotImpl ('.' :: '.' :: cs) = True
        containsAnyDotDotImpl (c :: cs) = containsAnyDotDotImpl cs

rmLeadingSlash : List Char -> String
rmLeadingSlash [] = ""
rmLeadingSlash ('/' :: cs) = pack cs
rmLeadingSlash cs = pack cs

addFrontSlash : List Char -> String
addFrontSlash [] = ""
addFrontSlash ('/' :: cs) = pack $ '/' :: cs
addFrontSlash cs = pack $ '/' :: cs

rmTrailingSlash : List Char -> String
rmTrailingSlash cs = reverse $ rmLeadingSlash $ reverse cs

||| Normalize a string such that it can be used to construct a path
||| via one of the mk* functions.
export
normalize : Anchoring -> String -> String
normalize Relative s = rmTrailingSlash $
                       unpack $
                       rmLeadingSlash $
                       unpack $
                       rmConsecutiveDots $
                       rmDotSlashPrefix $
                       rmConsecutiveSlashes s
normalize Absolute s = let s' = unpack $ rmDotSlashPrefix $ rmConsecutiveSlashes s in
                           if length s' == 1
                              then addFrontSlash s'
                              else rmTrailingSlash $ unpack $ addFrontSlash s'

parsePathImpl : List Char -> Anchoring -> Bool
parsePathImpl ('/' :: s) Relative = False
parsePathImpl s Relative          = True
parsePathImpl ('/' :: s) Absolute = True
parsePathImpl s Absolute          = False

parsePath : String -> Anchoring -> Maybe String
parsePath s Absolute = let empty = isNil (unpack s)
                           containsTilde' = containsTilde s
                           containsAnyDotDot' = containsAnyDotDot s
                           basicPreconditionsFailed = empty || containsTilde' || containsAnyDotDot' in
                       if basicPreconditionsFailed
                          then Nothing
                          else (if parsePathImpl (unpack s) Absolute
                                   then Just (normalize Absolute s)
                                   else Nothing)
parsePath s Relative = let empty = isNil (unpack s)
                           containsTilde' = containsTilde s
                           containsPrefixDotDot' = containsPrefixDotDot s
                           basicPreconditionsFailed = empty || containsTilde' || containsPrefixDotDot' in
                       if basicPreconditionsFailed
                          then Nothing
                          else (if parsePathImpl (unpack s) Relative
                                   then Just (normalize Relative s)
                                   else Nothing)

||| Attempt to construct a relative directory path from a string.
||| If the operation fails, it will return Nothing
export
mkRelativeDirectory : String -> Maybe (Path Relative Directory)
mkRelativeDirectory s = case parsePath s Relative of
                             Just s   => Just (RelativeDirectory s)
                             Nothing  => Nothing

||| Attempt to construct a relative file path from a string.
||| If the operation fails, it will return Nothing
export
mkRelativeFile : String -> Maybe (Path Relative File)
mkRelativeFile raw = case parsePath raw Relative of
                        Just raw  => Just (RelativeFile raw)
                        Nothing   => Nothing

||| Attempt to construct an absolute directory path from a string.
||| If the operation fails, it will return Nothing
export
mkAbsoluteDirectory : String -> Maybe (Path Absolute Directory)
mkAbsoluteDirectory raw = case parsePath raw Absolute of
                            Just raw => Just (AbsoluteDirectory raw)
                            Nothing  => Nothing

||| Attempt to construct an absolute file path from a string.
||| If the operation fails, it will return Nothing
export
mkAbsoluteFile : String -> Maybe (Path Absolute File)
mkAbsoluteFile raw = case parsePath raw Absolute of
                        Just raw => Just (AbsoluteFile raw)
                        Nothing  => Nothing

getFileExtensionImpl : String -> Maybe String
getFileExtensionImpl s = case split (\c => c == '.') s of
                            []        => Nothing
                            [c]       => Nothing
                            (c :: cs) => Just $ last (c :: cs)

||| Get the file extension from a path. If there
||| is no file extension, Nothing will be returned.
export
getFileExtension : Path _ File -> Maybe String
getFileExtension (AbsoluteFile raw) = getFileExtensionImpl raw
getFileExtension (RelativeFile raw) = getFileExtensionImpl raw

getDirectoryNameImpl : String -> Maybe String
getDirectoryNameImpl s = case (List.reverse (split (\c => c == '/') s)) of
                              []        => Nothing
                              ["", ""]  => Nothing
                              (c :: cs) => Just $ concat $ intersperse "/" $ List.reverse cs

||| Get the directory name from a file path.
export
getDirectoryName : Path _ File -> Maybe String
getDirectoryName (AbsoluteFile raw) = getDirectoryNameImpl raw
getDirectoryName (RelativeFile raw) = getDirectoryNameImpl raw

||| Join two paths together.
||| Its only valid to concatenate certain types of paths
|||
||| AbsoluteDirectory ++ Relative Directory/File
||| RelativeDirectory ++ Relative Directory/File
|||
||| Any other combination should be disallowed by the type sig.
export
concat : Path a Directory -> Path Relative k -> (Path a k)
concat (AbsoluteDirectory s1) (RelativeDirectory s2) = (AbsoluteDirectory (normalize Absolute (s1 ++ "/" ++ s2)))
concat (AbsoluteDirectory s1) (RelativeFile s2)      = (AbsoluteFile (normalize Absolute (s1 ++ "/" ++ s2)))
concat (RelativeDirectory s1) (RelativeDirectory s2) = (RelativeDirectory (normalize Relative (s1 ++ "/" ++ s2)))
concat (RelativeDirectory s1) (RelativeFile s2)      = (RelativeFile (normalize Relative (s1 ++ "/" ++ s2)))

||| String representation for Path.
export
str : Path a k -> String
str (AbsoluteFile raw)      = raw
str (AbsoluteDirectory raw) = raw
str (RelativeFile raw)      = raw
str (RelativeDirectory raw) = raw

||| Pretty for Path.
export
Show (Path a k) where
  show (AbsoluteDirectory raw) = "Absolute Directory: " ++ raw
  show (AbsoluteFile raw)      = "Absolute File: "      ++ raw
  show (RelativeDirectory raw) = "Relative Directory: " ++ raw
  show (RelativeFile raw)      = "Relative File: "      ++ raw

||| Equality for Path.
|||
||| Two paths are equal if they are of the same kind, same anchor,
||| and the underlying normalized representations are equal.
export
Eq (Path a k) where
  (==) (AbsoluteFile s1)      (AbsoluteFile s2)      = s1 == s2
  (==) (AbsoluteDirectory s1) (AbsoluteDirectory s2) = s1 == s2
  (==) (RelativeDirectory s1) (RelativeDirectory s2) = s1 == s2
  (==) (RelativeFile s1)      (RelativeFile s2)      = s1 == s2
  (==) _                      _                      = False

max_stars_repo_name: superfunc/dtp

max_issues_repo_name: superfunc/dtp

max_forks_repo_name: superfunc/dtp


text:
module IdrisScript.Arrays.Unpacked

import IdrisScript

%access public export

singleton : ToJS from to => from -> JS_IO (JSValue JSArray)
singleton {from} {to} val = do
  arr <- jscall "[%0]" (Ptr -> JS_IO Ptr) (unpack (toJS {from}{to} val))
  pure $ MkJSObject arr

push : ToJS from to => JSValue JSArray -> from -> JS_IO ()
push {from} {to} arr val =
      jscall "%0.push(%1)" (Ptr -> Ptr -> JS_IO ())
         (unpack arr) (unpack (toJS {from}{to} val))

insert : ToJS from to => Nat -> from -> JSValue JSArray -> JS_IO (JSValue JSArray)
insert {from} {to} idx val arr = do
  jscall "%0[%1] = %2" (Ptr -> Int -> Ptr -> JS_IO ())
         (unpack arr) (cast idx) (unpack (toJS {from}{to} val))
  pure arr

indexOf : ToJS from to => from -> JSValue JSArray -> JS_IO Int
indexOf {from} {to} val arr =
    jscall "%0.indexOf(%1)" (Ptr -> Ptr -> JS_IO Int)
           (unpack arr) (unpack (toJS {from}{to} val))

unshift : ToJS from to => JSValue JSArray -> from -> JS_IO Nat
unshift {from} {to} arr val = do
  res <- jscall "%0.unshift(%1)" (Ptr -> Ptr -> JS_IO Int)
                (unpack arr) (unpack (toJS {from}{to} val))
  pure $ cast {to=Nat} res

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module xquant.Spinor.Sigmas

import public Control.Algebra

infixr 5 <>
infixr 7 <&>

-------------------------------------------------------------------------------------------
--           Data for Sigma Operators  • Complex signs (Phases)
--                                     • Pauli operators
--                                     • Higher Sigma operators
--                                        (tensor products of Paulis with an overall phase)
-------------------------------------------------------------------------------------------

||| 4 primative complex phases, (+1), (+i), (-1), (-i),
||| bools represent minus sign and i presence respectively
data Phase : Type where
  Sign : (minus : Bool) -> (i : Bool) -> Phase

instance Show Phase where
  show (Sign False False) = "+1"
  show (Sign False True)  = "+i"
  show (Sign True False)  = "-1"
  show (Sign True True)   = "-i"

instance Eq Phase where
  (==) (Sign m1 i1) (Sign m2 i2) = (m1 == m2) && (i1 == i2)

-- Exclusive OR
xor : Bool -> Bool -> Bool
xor a b = if a then not b else b

instance Semigroup Phase where
  (<+>) (Sign as ai) (Sign bs bi) = Sign (xor (ai && bi) $ xor as bs) (xor ai bi)

instance Monoid Phase where
  neutral = Sign False False

instance Group Phase where
  inverse (Sign a b) = Sign (xor a b) b

star : Phase -> Phase
star (Sign a b) = Sign a (not b)

-- Phase Shorthands - Capital 'P' for phases
P1 : Phase
P1 = Sign False False
Pi : Phase
Pi = Sign False True
M1 : Phase
M1 = Sign True False
Mi : Phase
Mi = Sign True True

-- Pauli Data – Capital 'S' for basic sigma operators
data Pauli = SI | SX | SY | SZ

instance Show Pauli where
  show SI = "I"
  show SX = "x"
  show SY = "y"
  show SZ = "z" -- should be "σz" whene idris can print non-8-bit characters

instance Eq Pauli where
  SI == SI = True
  SX == SX = True
  SY == SY = True
  SZ == SZ = True
  _  == _  = False

-- Higher Sigma operator datatype, indexed by Nat
data Sigma : Nat -> Type where
  sPhase : Phase -> Sigma Z
  Sig    : Pauli -> Sigma k -> Sigma (S k)

instance Show (Sigma n) where
  show (sPhase phase) = show phase
  show s = (Prefix s) ++ "[" ++ (suffix s) ++ "]" where
    suffix : Sigma n -> String
    suffix (sPhase ph)         = ""
    suffix (Sig p (sPhase ph)) = (show p)
    suffix (Sig p s)           = (show p) ++ (suffix s)
    Prefix : Sigma n -> String
    Prefix (sPhase (Sign a b)) = (if a then "-" else "") ++ (if b then "i " else "")
    Prefix (Sig p s)           = Prefix s

-- 4 Standard Sigma 1s
sX : (Sigma 1)
sX = Sig SX $ sPhase P1

sY : Sigma 1
sY = Sig SY $ sPhase P1

sZ : Sigma 1
sZ = Sig SZ $ sPhase P1

sI : Sigma 1
sI = Sig SI $ sPhase P1

-------------------------------------------------------------------------------------------
--           Operations with Sigmas   • Helper functions: getPhase, topPauli, lastPauli, pack
--                                    • Scalar multiply
--                                    • (Single) Sigma multiply
--                                    • (Higher) Sigma multiply
-------------------------------------------------------------------------------------------

-- Extract the Phase, first Pauli or last Pauli from a Sigma
getPhase : Sigma n -> Phase
getPhase (sPhase p) = p
getPhase (Sig p s)  = getPhase s

topPauli : Sigma (S k) -> Pauli
topPauli (Sig p s) = p

lastPauli : Sigma (S k) -> Pauli
lastPauli (Sig pl (sPhase ph)) = pl
lastPauli (Sig pl (Sig pl2 s)) = lastPauli (Sig pl2 s)

-- Pack a Pauli into a Sigma
pack : Pauli -> Sigma 1
pack s = Sig s $ sPhase P1

-- Phase times a Sigma
xPhaseSig.(*) : Phase -> Sigma n -> Sigma n
xPhaseSig.(*) ph (sPhase ph2) = sPhase $ ph <+> ph2
xPhaseSig.(*) ph (Sig pl s)   = Sig pl $ ph * s

xSigPhase.(*) : Sigma n -> Phase -> Sigma n
xSigPhase.(*) s p = p * s

-- Single Sigma multiply
s1Mult : Sigma 1 -> Sigma 1 -> Sigma 1
s1Mult (Sig x1 $ sPhase p1) (Sig x2 $ sPhase p2) = case x1 of
                                                        SX => case x2 of
                                                                   SX => Sig SI (sPhase $ p1 <+> p2)
                                                                   SY => Sig SZ (sPhase $ p1 <+> p2 <+> Pi)
                                                                   SZ => Sig SY (sPhase $ p1 <+> p2 <+> Mi)
                                                                   SI => Sig SX (sPhase $ p1 <+> p2)
                                                        SY => case x2 of
                                                                   SY => Sig SI (sPhase $ p1 <+> p2)
                                                                   SZ => Sig SX (sPhase $ p1 <+> p2 <+> Pi)
                                                                   SX => Sig SZ (sPhase $ p1 <+> p2 <+> Mi)
                                                                   SI => Sig SY (sPhase $ p1 <+> p2)
                                                        SZ => case x2 of
                                                                   SZ => Sig SI (sPhase $ p1 <+> p2)
                                                                   SX => Sig SY (sPhase $ p1 <+> p2 <+> Pi)
                                                                   SY => Sig SX (sPhase $ p1 <+> p2 <+> Mi)
                                                                   SI => Sig SZ (sPhase $ p1 <+> p2)
                                                        SI => case x2 of
                                                                   SI => Sig SI (sPhase $ p1 <+> p2)
                                                                   SX => Sig SX (sPhase $ p1 <+> p2)
                                                                   SY => Sig SY (sPhase $ p1 <+> p2)
                                                                   SZ => Sig SZ (sPhase $ p1 <+> p2)

-- Higher Sigma mutiply
sMult : Sigma n -> Sigma n -> Sigma n
sMult (sPhase p1)  (sPhase p2)  = sPhase $ p1 <+> p2
sMult (Sig pl1 s1) (Sig pl2 s2) with (s1Mult (pack pl1) (pack pl2))
  sMult (Sig pl1 s1) (Sig pl2 s2) | r = Sig (topPauli r) ((getPhase r) * (sMult s1 s2))

-- Infix op for Sigma multiply
(<>) : Sigma n -> Sigma n -> Sigma n
(<>) = sMult

-- Tensor multiply Sigmas ('otimes', i.e. ⊗ )
ox : Sigma n -> Sigma m -> Sigma (n + m)
ox s            (sPhase p)   ?= {Sigma_OTimes_Lemma_1} p * s
ox (sPhase p)   s             = p * s
ox (Sig pl1 s1) (Sig pl2 s2) ?= {Sigma_OTimes_Lemma_2} ox (dropLast $ Sig pl1 s1)
                                                          (Sig (lastPauli $ Sig pl1 s1) (Sig pl2 s2)) where
  dropLast : {k : Nat} -> Sigma (S k) -> Sigma k
  dropLast (Sig pl (sPhase ph)) = (sPhase ph)
  dropLast (Sig pl (Sig pl2 s)) = Sig pl (dropLast (Sig pl2 s))

-- Infix tensor multiply Sigmas
(<&>) : Sigma n -> Sigma m -> Sigma (n + m)
(<&>) = ox

-- Tensor powers of a Sigma op
opower : Sigma n -> (m : Nat) -> Sigma (n * m)
opower s Z     ?=  {Sigma_Power_Lemma_1}  sPhase P1
opower s (S n) ?=  {Sigma_Power_Lemma_2}  s <&> (opower s n)

negId : (n : Nat) -> Sigma n
negId Z     = sPhase M1
negId (S n) = Sig SI $ negId n

---------- Proofs ----------

Sigma_OTimes_Lemma_1 = proof
  intro
  rewrite (plusZeroRightNeutral n)
  intros
  trivial

Sigma_OTimes_Lemma_2 = proof
  intros
  rewrite sym $ plusSuccRightSucc k (S k1)
  trivial

Sigma_Power_Lemma_1 = proof
  intros
  rewrite (sym $ multZeroRightZero n)
  trivial

Sigma_Power_Lemma_2 = proof
  intros
  rewrite (sym $ multRightSuccPlus n n1)
  trivial

max_stars_repo_name: BlackBrane/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module IdrisScript.Functions

import IdrisScript

%access public export

infixl 6 !!

Function : JS_IO (JSValue JSFunction)
Function = do
  fun <- jscall "Function" (JS_IO Ptr)
  pure $ MkJSFunction fun

||| Applys an array `args` as arguments to the function `fun`
apply : (fun : JSValue JSFunction)
     -> (args : JSValue JSArray)
     -> JS_IO (t ** JSValue t)
apply fun args = do
  res <- jscall "%0.apply(this, %1)" (Ptr -> Ptr -> JS_IO Ptr)
         (unpack fun) (unpack args)
  pack res

||| Sets the property `prop` to the value `val` for a function `fun`. Modifies
||| the original value.
setProperty : (prop : String)
           -> (val : JSValue a)
           -> (fun : JSValue JSFunction)
           -> JS_IO (JSValue JSFunction)
setProperty prop val fun = do
  jscall "%0[%1] = %2" (Ptr -> String -> Ptr -> JS_IO Ptr)
     (unpack fun) prop (unpack val)
  pure fun

||| Gets the property `prop` from a function `fun`.
getProperty : (prop : String)
           -> (fun : JSValue JSFunction)
           -> JS_IO (Maybe (t ** JSValue t))
getProperty prop fun = do
  elm <- jscall "%0[%1]" (Ptr -> String -> JS_IO Ptr) (unpack fun) prop
  case !(typeOf elm) of
       JSUndefined => pure Nothing
       _           => pure $ Just !(pack elm)

||| Gets the property `prop` from a function `fun`.
(!!) : (fun : JSValue JSFunction)
    -> (prop : String)
    -> JS_IO (Maybe (t : JSType ** JSValue t))
fun !! prop = getProperty prop fun

||| Checks if a function `fun` has the property `prop`.
hasOwnProperty : (prop : String)
              -> (fun : JSValue JSFunction)
              -> JS_IO Bool
hasOwnProperty prop fun = do
  res <- jscall "%0.hasOwnProperty(%1)" (Ptr -> String -> JS_IO Int)
                (unpack fun) prop
  pure $ res == 1

||| Returns the name of a function.
name : JSValue JSFunction -> JS_IO String
name fun = jscall "%0.name" (Ptr -> JS_IO String) (unpack fun)

||| Returns the constructor of a function.
constr : JSValue JSFunction -> JS_IO (JSValue JSFunction)
constr fun = do
  con <- jscall "%0.constructor" (Ptr -> JS_IO Ptr) (unpack fun)
  pure $ MkJSFunction con


text:
-- PrintLength.idr

-- Perform I/O operations with the (>>=) sequencing operator

printLength : IO ()
printLength = getLine >>= \input => let len = length input in
                                        putStrLn (show len)

printLonger : IO ()
printLonger = do
  s1 <- getLine
  s2 <- getLine
  let (len1, len2) = (length s1, length s2)
  let lenLonger = if len1 > len2 then len1 else len2
  putStrLn (show lenLonger)

printLonger2 : IO ()
printLonger2 = getLine >>= \s1 =>
               getLine >>= \s2 =>
               let (len1, len2) = (length s1, length s2)
                   lenLonger = if len1 > len2 then len1 else len2 in
                   putStrLn (show lenLonger)

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
-- Non-strictly-positive recursion
data La : Type where
  Lam : (La -> La) -> La

app : La -> La -> La
app (Lam f) x = f x

selfApp : La
selfApp = Lam \x => app x x

om : La
om = app selfApp selfApp


text:
module IdrisScript.Strings

import IdrisScript

%access public export

||| Upper case a string.
toUpperCase : String -> JS_IO String
toUpperCase str = jscall "%0.toUpperCase()" (String -> JS_IO String) str

||| Lower case a string.
toLowerCase : String -> JS_IO String
toLowerCase str = jscall "%0.toLowerCase()" (String -> JS_IO String) str

||| Trims a string.
trim : String -> JS_IO String
trim str = jscall "%0.trim()" (String -> JS_IO String) str

||| Trims a string from the left.
trimLeft : String -> JS_IO String
trimLeft str = jscall "%0.trimLeft()" (String -> JS_IO String) str

||| Trims a string from the right.
trimRight : String -> JS_IO String
trimRight str = jscall "%0.trimRight()" (String -> JS_IO String) str

||| Returns the position of the string `search` in the string `str`.
indexOf : (str : String) -> (search : String) -> JS_IO Int
indexOf str search =
  jscall "%0.indexOf(%1)" (String -> String -> JS_IO Int) str search

||| Returns a substring from postion `start` with the length `length` from
||| the string `str`.
substr : (str : String)
      -> (start : Int)
      -> (length : Int)
      -> JS_IO String
substr str start length =
  jscall "%0.substr(%1,%2)" (String -> Int -> Int -> JS_IO String)
          str start length

||| Returns a substring from position `from` to postion `to` in the
||| string `str`.
substring : (str : String)
         -> (from : Int)
         -> (to : Int)
         -> JS_IO String
substring str from to =
  jscall "%0.substring(%1,%2)" (String -> Int -> Int -> JS_IO String)
          str from to