text:
-- Module      : Itea.Javascript.Objects
-- Description :
-- Copyright   : (c) Simon Nielsen Knights 2018
-- License     : MIT
-- Maintainer  : simonank@mail.ru
-- Stability   : unstable
-- Portability : portable

module Itea.Javascript.Objects
import Itea.Javascript.Types
import Itea.Utils

import Data.List

%default total
%access public export

||| Interface for inheriting native Javascript object properties
||| of common objects
interface Inherit obj where
  property   : List String
  prototype : List String

||| Opaque type representing a javascript object
data Object : List String -> Type where

||| Extend a given object with a property if such
||| property is not present.
|||
||| @prop property to extend object with
||| @value object to set property to
||| @object object to extend
||| @ok proof of property not existing
extendProperty : Convertible a =>
         (prop   : String)
      -> (value  : a)
      -> (object : Object xs)
      -> { auto ok : Not (Elem prop xs) }
      -> Object (prop :: xs)
extendProperty prop value object = believe_me $
  foreign FFI_JS ("%0." ++ prop ++ " = %1")
                 (Ptr -> Ptr -> JS_IO ())
                 (believe_me object) (convert value)

||| Revoke an existing property from
||| an object
|||
||| @prop property to revoke
||| @object object to revoke property from
||| @ok proof of property existing
revokeProperty : (prop   : String)
              -> (object : Object xs)
              -> { auto ok : Elem prop xs }
              -> Object (filter (/=prop) xs)
revokeProperty prop object = believe_me $ object

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea


text:
module Coinduction

corecord Stream a where
  head : a
  tail : Stream a

total causal
zeros : Stream Nat
&head zeros = Z
&tail zeros = zeros

total causal
repeat : a -> Stream a
&head repeat n = n
&tail repeat n = repeat n

total causal
map : (a -> b) -> Stream a -> Stream b
&head map f s = f (head s)
&tail map f s = map f (tail s)

total causal
nats : Stream Nat
&head nats = Z
&tail nats = map S nats

total causal
zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c
&head zipWith f s t = f (head s) (head t)
&tail zipWith f s t = zipWith f (tail s) (tail t)

total causal
fib : Stream Nat
&head       fib = Z
&head &tail fib = S Z
&tail &tail fib = zipWith (+) fib (tail fib)

total causal
unfold : (s -> (a, s)) -> s -> Stream a
&head unfold step x = fst (step x)
&tail unfold step x = unfold step (snd (step x))

total causal
interleave : Stream a -> Stream a -> Stream a
&head interleave s t = head s
&tail interleave s t = interleave t (tail s)

total causal
toggle : Stream Nat
&head       toggle = Z
&head &tail toggle = S Z
&tail &tail toggle = toggle

total causal
paperfold : Stream Nat
&head paperfold = Z
&tail paperfold = interleave paperfold toggle

total causal
paperfold' : Stream Nat
paperfold' = interleave toggle paperfold'

total causal
cycle : Nat -> Stream Nat
cycle n = cycle' n n
  where
    total causal
    cycle' : Nat -> Nat -> Stream Nat
    &head cycle' Z     m = Z
    &head cycle' (S n) m = (S n)
    &tail cycle' Z     m = cycle' m m
    &tail cycle' (S n) m = cycle' n m

total causal
fac : Stream Nat
&head fac = (S Z)
&tail fac = (zipWith (*) (map S nats) fac)

total causal
mergef : (Nat -> Nat -> Stream Nat -> Stream Nat) ->
              Stream Nat -> Stream Nat -> Stream Nat
mergef f s t = f (head s) (head t) (mergef f (tail s) (tail t))

total causal
prepend : List a -> Stream a -> Stream
prepend []       s = s
prepend (x ::xs) s = x :: (prepend xs s)

corecord Tree : Type -> Type where
  value : Tree a -> a
  left  : Tree a -> Tree a
  right : Tree a -> Tree a

total causal
tmap : (a -> b) -> Tree a -> Tree b
&value tmap f t = f (value t)
&left  tmap f t = tmap f (left  t)
&right tmap f t = tmap f (right t)

total causal
tzip : (a -> b -> c) -> Tree a -> Tree b -> Tree c
&value tzip f t r = f (value t) (value r)
&left  tzip f t r = tzip f (left  t) (left  r)
&right tzip f t r = tzip f (right t) (right r)

total causal
trepeat : a -> Tree a
&value trepeat n = n
&left  trepeat n = trepeat n
&right trepeat n = trepeat n

total causal
carry : Tree Nat
&value carry = S Z
&left  carry = trepeat Z
&right carry = tmap S carry

total causal unfoldTree : (s -> (a, s, s)) -> s -> Tree a
&value unfoldTree step x = fst' (step x)
&left  unfoldTree step x = unfoldTree step (snd' (step x))
&right unfoldTree step x = unfoldTree step (trd' (step x))

total causal
calculateWilfully : Tree (Nat, Nat)
calculateWilfully = grow((S Z), (S Z))
  where
    total causal
    grow : (Nat, Nat) -> Tree(Nat, Nat)
    grow (n, d) = MkTree (n, d) (grow(n, n + d)) (grow(n + d, d))

corecord Partiality : Type -> Type where
  p : Partiality a -> Either a (Partiality a)
  constructor P

total causal
never : Partiality a
never = P (Right never)

total causal
bind : Partiality a -> (a -> Partiality b) -> Partiality b
bind (P (Left x)) f = f x
bind (P (Right x)) f = P (Right (bind x f))

corecord FunMachine : Type -> Type where
  skip : FunMachine a -> FunMachine a
  calc : FunMachine a -> (a, FunMachine a)
  fun  : FunMachine a -> (a -> a)

total causal
multmachine : Stream Nat -> FunMachine Nat
&skip multmachine s = multmachine (tail s)
&calc multmachine s =
     (fun (multmachine $ tail s) (head s) ,
      multmachine $ tail s)
&fun  multmachine s = (*) (head s)

data Response = OK | BadRequest

total
reject : a -> Response
reject _ = BadRequest

total causal
pingserver : FunMachine Response
&skip pingserver = pingserver
&calc pingserver = (OK, pingserver)
&fun  pingserver = reject

corecord Idler : Type -> Type where
  idle : Idler a -> Idler a
  stop : Idler a -> a

total causal
pingserver' : Idler Response
&idle pingserver' = pingserver'
&stop pingserver' = OK

ping' : Response
ping' = stop (idle (idle pingserver'))

total causal
imap : (a -> b) -> Idler a -> Idler b
&idle imap f i = imap f (idle i)
&stop imap f i = f (stop i)

total causal
counter : Nat -> Idler Nat
&idle counter n = imap S (counter n)
&stop counter n = n

ext: idr

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis


text:
module AssRecRule

import Data.Fin
import Data.Vect

{-
 The recursion function for lists of type `a`. Define this by pattern matching
-}
recList : (a: Type) ->  (x: Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)
recList a x base step [] = base
recList a x base step (y :: xs) = step y xs (recList a x base step xs)

{-
Given a list of type `a` and a function `f: a -> b` get a list of type `b`
by applying `f` to each element.
Note: Define using `recList` and without pattern matching on lists.
-}
mapList : (a: Type) -> (b: Type) -> (f: a -> b) -> List a -> List b
mapList a b f x = recList a (List b) [] step2 x where
  step2 : a -> List a -> List b -> List b
  step2 a1 y1 z1 = (f a1) :: z1

{-
Given a list of type `a`, an initial value `init: a` and an operation `op: a -> a -> a`,
get an element of `a` by starting with init and repeatedly applying the elements of the
list,
e.g. fold Nat 1 (*) ([22] :: [3] :: [])  = 1 * 22 * 3
Note: Define using `recList` and without pattern matching on lists.
-}
foldList : (a: Type) ->  (init: a) -> (op : a -> a -> a) -> List a -> a
foldList a init op y = recList a a init step3 y where
  step3 : a -> List a -> a -> a
  step3 a1 la1 a2 = op a2 a1

{-
The induction function on the `Fin` indexed type family. Define this by pattern matching.
-}
inducFin : (xs : (n: Nat) -> Fin n -> Type) -> (base : (m: Nat) -> xs (S m) FZ) -> (step : (p: Nat) -> (k: Fin p) -> (prev: xs p k) -> (xs (S p) (FS k))) -> (q: Nat) -> (j: Fin q) -> xs q j
inducFin xs base step (S q) FZ = base q
inducFin xs base step (S q) (FS x) = step q x (inducFin xs base step q x)

{-
Given a type `a`, a natural number `q`, an element `j : Fin q` and a vector `v` of length q with entries of type `a`,
get the element in position `j` of `v`. Note that this is always well defined.

Note: Define using `inducList` and without pattern matching on the `Fin` family. You may pattern match on Vectors.
The definition should have only one case, and there should be no case splitting on `Fin`.
-}
fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)
fetchElem a q j = inducFin xs base step q j where
  xs : (n: Nat) -> Fin n -> Type
  xs n m = (Vect n a -> a)
  base : (m: Nat) -> xs (S m) FZ
  base m = basef where
    basef : (Vect (S m) a) -> a
    basef (x :: y) = x
  step : (p: Nat) -> (k: Fin p) -> (prev: xs p k) -> (xs (S p) (FS k))
  step p k prev = stepf where
    stepf : (Vect (S p) a) -> a
    stepf (x :: y) = prev y


text:
{--
Copyright 2021 Joel Berkeley

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.
--}
||| This module contains definitions and utilities for probabilistic models.
module Model

import Distribution
import Tensor

||| A `ProbabilisticModel` is a mapping from a feature domain to a probability distribution over
||| a target domain.
|||
||| @features The shape of the feature domain.
||| @targets The shape of the target domain.
||| @marginal The type of mulitvariate marginal distribution over the target domain.
public export 0
ProbabilisticModel : Distribution targets marginal => (0 features : Shape) -> Type
ProbabilisticModel features = {n : _} -> Tensor (Vect.(::) (S n) features) Double -> marginal (S n)

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module Data.Music

import Data.Combinators
import Data.Int.Algebra

private
divMod : Nat -> Nat -> (Nat, Nat)
divMod n d = (n `div` d, n `mod` d)

%access public export

Octave : Type
Octave = Int

namespace Chromatic
  data PitchClass
    = C
    | Cis
    | D
    | Dis
    | E
    | F
    | Fis
    | G
    | Gis
    | A
    | Ais
    | B

  Enum PitchClass where
    pred C   = B
    pred Cis = C
    pred D   = Cis
    pred Dis = D
    pred E   = Dis
    pred F   = E
    pred Fis = F
    pred G   = Fis
    pred Gis = G
    pred A   = Gis
    pred Ais = A
    pred B   = Ais

    succ C   = Cis
    succ Cis = D
    succ D   = Dis
    succ Dis = E
    succ E   = F
    succ F   = Fis
    succ Fis = G
    succ G   = Gis
    succ Gis = A
    succ A   = Ais
    succ Ais = B
    succ B   = C

    toNat C   = 0
    toNat Cis = 1
    toNat D   = 2
    toNat Dis = 3
    toNat E   = 4
    toNat F   = 5
    toNat Fis = 6
    toNat G   = 7
    toNat Gis = 8
    toNat A   = 9
    toNat Ais = 10
    toNat B   = 11

    fromNat Z = C
    fromNat (S k) = succ (fromNat k)

  Cast PitchClass Int where
    cast = toIntNat . toNat

  Cast PitchClass (Zn n) where
    cast = MkZn . cast

  Eq PitchClass where
    (==) = (==) `on` toNat

  Ord PitchClass where
    compare = compare `on` toNat

  Show PitchClass where
    show C   = "C"
    show Cis = "Cis"
    show D   = "D"
    show Dis = "Dis"
    show E   = "E"
    show F   = "F"
    show Fis = "Fis"
    show G   = "G"
    show Gis = "Gis"
    show A   = "A"
    show Ais = "Ais"
    show B   = "B"

  Pitch : Type
  Pitch = Pair PitchClass Octave

  Enum Pitch where
    succ (B, oct)  = (C, oct + 1)
    succ (pc, oct) = (succ C, oct)

    pred (C, oct)  = (B, oct - 1)
    pred (pc, oct) = (pred pc, oct)

    toNat (pc, oct) = toNat pc + 12 * (toNat oct)

    fromNat k =
      let (pc, oct) = assert_total (divMod k 12) in
        (fromNat pc, toIntNat oct)

  Cast Pitch PitchClass where
    cast = fst

  Cast Pitch Int where
    cast (pc, oct) = toIntNat (toNat pc) + 12 * oct

  [PitchOrd] Ord Pitch where
    compare (pc1, oct1) (pc2, oct2) =
      case compare oct1 oct2 of
        EQ => compare pc1 pc2
        res => res

  [PitchShow] Show Pitch where
    show (pc, octave) = show pc ++ show octave

namespace Diatonic
  data PitchClass
    = C
    | D
    | E
    | F
    | G
    | A
    | B

  Enum Diatonic.PitchClass where
    pred C = B
    pred D = C
    pred E = D
    pred F = E
    pred G = F
    pred A = G
    pred B = A

    succ C = D
    succ D = E
    succ E = F
    succ F = G
    succ G = A
    succ A = B
    succ B = C

    toNat C = 0
    toNat D = 1
    toNat E = 2
    toNat F = 3
    toNat G = 4
    toNat A = 5
    toNat B = 6

    fromNat Z     = C
    fromNat (S k) = succ (fromNat k)

  Eq Diatonic.PitchClass where
    (==) = (==) `on` toNat

  Ord Diatonic.PitchClass where
    compare = compare `on` toNat

  Cast Diatonic.PitchClass Int where
    cast = toIntNat . toNat

  Cast Diatonic.PitchClass (Zn n) where
    cast = MkZn . cast

  Cast Diatonic.PitchClass Chromatic.PitchClass where
    cast C = C
    cast D = D
    cast E = E
    cast F = F
    cast G = G
    cast A = A
    cast B = B

  Show Diatonic.PitchClass where
    show = show . (cast {to = Chromatic.PitchClass})

  Pitch : Type
  Pitch = Pair Diatonic.PitchClass Octave

  Enum Diatonic.Pitch where
    succ (B, oct)  = (C, oct + 1)
    succ (pc, oct) = (succ C, oct)

    pred (C, oct)  = (B, oct - 1)
    pred (pc, oct) = (pred C, oct)

    toNat (pc, oct) = toNat pc + 7 * (toNat oct)

    fromNat k =
      let (pc, oct) = assert_total (divMod k 7) in
        (fromNat pc, toIntNat oct)

  Cast Diatonic.Pitch Diatonic.PitchClass where
    cast = fst

  Cast Diatonic.Pitch Chromatic.Pitch where
    cast (dpc, octave) = (cast dpc, octave)

  Cast Diatonic.Pitch Int where
    cast (pc, oct) = toIntNat (toNat pc) + 7 * oct

  [DiatonicPitchOrd] Ord Diatonic.Pitch where
    compare = compare@{PitchOrd} `on` cast

  [DiatonicPitchShow] Show Diatonic.Pitch where
    show = show . cast {to = Chromatic.Pitch}

max_stars_repo_name: yurrriq/gis

max_issues_repo_name: yurrriq/gis

max_forks_repo_name: yurrriq/gis


text:
import Erlang

%default partial

foo : Maybe a -> a
foo (Just x) = x

data Vect : ? -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

data Fin : Nat -> Type where
     FZ : Fin (S k)
     FS : Fin k -> Fin (S k)

lookup : Fin n -> Vect n a -> a
lookup FZ (x :: xs) = x
lookup (FS k) (x :: xs) = lookup k xs

lookup' : Fin n -> Vect n a -> a
lookup' (FS k) (x :: xs) = lookup' k xs

lookup'' : Fin n -> Vect n a -> a
lookup'' n xs = lookup' n xs

ex1 : IO ()
ex1 = do
  putStr "" -- TODO: Workaround to avoid pruning this function
  let x = foo Nothing
  printLn (the Int x)

ex2 : IO ()
ex2 = printLn $ lookup (FS FZ) [1,2,3,4]

ex3 : IO ()
ex3 = do
  putStr "" -- TODO: Workaround to avoid pruning this function
  printLn $ lookup' (FS FZ) [1,2,3,4]

ex4 : IO ()
ex4 = do
  putStr "" -- TODO: Workaround to avoid pruning this function
  printLn $ lookup'' (FS FZ) [1,2,3,4]

try : IO () -> IO ()
try action = do
  Right _ <- erlTryCatch action
    | Left (MkTuple3 _ reason _) =>
      let MkTuple2 _ msg = erlUnsafeCast (ErlTuple2 ErlTerm String) reason
      in putStrLn msg
  pure ()

main : IO ()
main = do
  -- try ex1 -- TODO: This example is not caught by `erlTryCatch`, thus exiting early.
  try ex2
  try ex3
  try ex4


text:
module DataStore

import Data.List
import Data.Strings
import Data.Vect
import System.REPL

%default total

infixr 5 .+.

data Schema = SChar
            | SString
            | SInt
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SChar = Char
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

parsePrefix : (schema : Schema) -> (inp : String) -> Maybe (SchemaType schema, String)
parsePrefix SChar inp = getSingleQuoted (unpack inp)
  where
    getSingleQuoted : List Char -> Maybe (Char, String)
    getSingleQuoted ('\'' :: xs) = case xs of
                                        (c :: '\'' :: rest) => Just (c, ltrim (pack rest))
                                        _ => Nothing
    getSingleQuoted _ = Nothing
parsePrefix SString inp = getQuoted (unpack inp)
  where
    getQuoted : List Char -> Maybe (String, String)
    getQuoted ('"' :: xs) = case span (/= '"') xs of
                                 (quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
                                 _ => Nothing
    getQuoted _ = Nothing
parsePrefix SInt inp = case span isDigit inp of
                            ("", rest) => Nothing
                            (num, rest) => Just (cast num, ltrim rest)
parsePrefix (schemal .+. schemar) inp =
  do (lval, inp') <- parsePrefix schemal inp
     (rval, inp'') <- parsePrefix schemar inp'
     Just ((lval, rval), inp'')

stringToSchema : (schema : Schema) -> (inp : String) -> Maybe (SchemaType schema)
stringToSchema schema inp =
  case parsePrefix schema inp of
       Just (res, "") => Just res
       Just _ => Nothing
       Nothing => Nothing

schemaToString : { schema : Schema } -> SchemaType schema -> String
schemaToString {schema = SChar} item = show item
schemaToString {schema = SString} item = show item
schemaToString {schema = SInt} item = show item
schemaToString {schema = (x .+. y)} (itemx, itemy) =
  schemaToString itemx ++ ", " ++ schemaToString itemy

record DataStore where
  constructor MkData
  schema : Schema
  size : Nat
  items : Vect size (SchemaType schema)

addToStore : (store : DataStore) -> (item : SchemaType (schema store)) -> DataStore
addToStore (MkData schema size items) newItem = MkData _ _ (addItem items)
  where
    addItem : Vect oldsize (SchemaType schema) -> Vect (S oldsize) (SchemaType schema)
    addItem [] = [newItem]
    addItem (item :: items) = item :: addItem items

getEntry : (store : DataStore) -> (idx : Integer) -> String
getEntry (MkData _ size items) idx = case integerToFin idx size of
                                      Nothing => "invalid index: " ++ show idx
                                      Just idx' => schemaToString (index idx' items)

getAllEntries : (store : DataStore) -> String
getAllEntries store = getAllEntriesHelper (size store) ""
  where
    getAllEntriesHelper : (idx : Nat) -> (results : String) -> String
    getAllEntriesHelper Z results = results
    getAllEntriesHelper (S idx') results = getAllEntriesHelper idx' results ++ "\n" ++ getEntry store (cast idx')

data Command : Schema -> Type where
  SetSchema : (newschema : Schema) -> Command schema
  Add : SchemaType schema -> Command schema
  Get : Maybe Integer -> Command schema
  Size : Command schema
  Quit : Command schema

parseSchema : List String -> Maybe Schema
parseSchema ("Char" :: xs) =
  case xs of
       [] => Just SChar
       _ => case parseSchema xs of
                 Nothing => Nothing
                 Just schema' => Just (SChar .+. schema')
parseSchema ("String" :: xs) =
  case xs of
       [] => Just SString
       _ => case parseSchema xs of
                 Nothing => Nothing
                 Just schema' => Just (SString .+. schema')
parseSchema ("Int" :: xs) =
  case xs of
       [] => Just SInt
       _ => case parseSchema xs of
                 Nothing => Nothing
                 Just schema' => Just (SInt .+. schema')
parseSchema _ = Nothing

parseCommand : (schema : Schema) -> (cmd : String) -> (args : String) -> Maybe (Command schema)
parseCommand schema "add" item = case stringToSchema schema item of
                                      Nothing => Nothing
                                      Just item' => Just (Add item')
parseCommand schema "get" idxStr =
  if idxStr == ""
     then Just (Get Nothing)
     else case all isDigit (unpack idxStr) of
             False => Nothing
             True => Just $ Get (Just (cast idxStr))
parseCommand schema "size" "" = Just Size
parseCommand schema "setschema" newschema =
  case parseSchema (words newschema) of
       Nothing => Nothing
       Just schema => Just (SetSchema schema)
parseCommand schema "quit" "" = Just Quit
parseCommand _ _ _ = Nothing

parse : (schema : Schema) -> (inp : String) -> Maybe (Command schema)
parse schema inp = let (cmd, args) = span (/= ' ') inp in
                       parseCommand schema cmd (ltrim args)

setSchema : (store : DataStore) -> (newschema : Schema) -> Maybe DataStore
setSchema store newschema = case size store of
                                 Z => Just (MkData newschema 0 [])
                                 _ => Nothing

processCommand : (store : DataStore) -> (cmd : Command (schema store)) -> Maybe (String, DataStore)
processCommand store (Add item) = Just ("ID" ++ show (size store) ++ "\n", addToStore store item)
processCommand store (Get idx) =
  case idx of
       Nothing => Just (getAllEntries store ++ "\n", store)
       Just idx' => Just (getEntry store idx' ++ "\n", store)
processCommand store Size = Just (show (size store) ++ "\n", store)
processCommand store (SetSchema schema) =
  case setSchema store schema of
       Nothing => Just ("Cannot update schema - store is possibly not empty\n", store)
       Just store' => Just ("updated schema\n", store')
processCommand store Quit = Nothing

processInput : (store : DataStore) -> (inp : String) -> Maybe (String, DataStore)
processInput store inp =
  case parse (schema store) inp of
       Nothing => Just ("invalid command\n", store)
       Just cmd => processCommand store cmd

partial
main : HasIO io => io ()
main = replWith (MkData (SString .+. SString .+. SInt) 0 []) "Command: " processInput

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

import Control.Algebra
import Classes.Verified
import Control.Algebra.VectorSpace -- definition of module

import Data.Matrix
import Data.Matrix.Algebraic -- module instances; from Idris 0.9.20
import Data.Matrix.AlgebraicVerified

import Data.Vect.Structural
import Data.Matrix.Structural

import Data.ZZ
import Control.Algebra.NumericInstances
import Control.Algebra.ZZVerifiedInstances
import Data.Matrix.ZZVerified

import Data.Matrix.ZZModuleSpan
import Data.Matrix.LinearCombinations

import Data.Matrix.RowEchelon
import Control.Algebra.ZZDivisors
import Data.Matrix.ZZGaussianEliminationLemmas

import Data.Fin.FinOrdering

import Control.Isomorphism

%default total

{-
Table of Contents:

* Main elimination algorithms
-}

{-
Main elimination algorithms
-}

parameters (
	gcdOfVectAlg :
		-- Will making argument "k" implicit work?
		(k : Nat)
		-> (x : Vect k ZZ)
		-> ( v : Vect k ZZ **
			( i : Fin k )
			-> (index i x) `quotientOverZZ` (v <:> x) )
	) {

{-
Structure of (elimFirstCol):

succImplWknStep_Qfunclemma => succImplWknStep_stepQfunc => succImplWknStep_unplumbed => succImplWknStep => foldedFully

(mkQfunc, foldedFully) => elimFirstCol (after some work)

---

Better to refine this to a type that depends on (m=S predm) so that the case (m=Z) may also be covered.

Shall start from the bottom of the matrix (last) and work up to row (FS FZ) using a traversal based on (weaken) and a binary map from index (Fin n) and oldvals to newvals.
-}

elimFirstCol :
	(xs : Matrix n (S predm) ZZ)
	-> (gexs : Matrix (S n) (S predm) ZZ **
		(downAndNotRightOfEntryImpliesZ gexs FZ FZ
		, gexs `bispanslz` xs))
elimFirstCol [] {predm}
	= ( row {n=S predm} $ neutral ** ( nosuch, ([] ** Refl), ([neutral] ** Refl) ) )
	where
		nosuch : (i : Fin _) -> (j : Fin _)
			-> LTRel Z (finToNat i)
			-> LTERel (finToNat j) Z
			-> indices i j (row {n=S predm} Prelude.Algebra.neutral) = Pos 0
		nosuch FZ FZ _ = either (const Refl) (const Refl)
		nosuch (FS k) FZ _ = absurd k
		nosuch _ (FS k) _ = void . ( either succNotLTEzero SIsNotZ )
elimFirstCol mat {n=S predn} {predm} =
	( index FZ endmat
		** (leftColZBelow, bispanslztrans endmatBispansMatandgcd bisWithGCD) )
	where
		{-
		Should just be nested (with) blocks over (vAndFn) & (endMatAndPropFn),
		but the typechecker is struggling.
		-}
		vAndFn : ( v : Vect (S predn) ZZ **
			( i : Fin (S predn) )
			-> (index i (getCol FZ mat))
				`quotientOverZZ` (v <:> (getCol FZ mat)) )
		vAndFn = gcdOfVectAlg (S predn) (getCol FZ mat)
		v : Vect (S predn) ZZ
		v = getWitness vAndFn
		fn : ( i : Fin (S predn) )
			-> (index i (getCol FZ mat))
				`quotientOverZZ` (v <:> (getCol FZ mat))
		fn = getProof vAndFn
		endMatAndPropFn : ( mats : Vect (S (S predn))
			$ Matrix (S (S predn)) (S predm) ZZ
			** (i : Fin (S (S predn)))
			-> succImplWknProp mat (v<\>mat) (S predn) i (index i mats) )
		endMatAndPropFn = foldedFully _ _ mat v $ mkQFunc _ _ v mat fn
		endmat : Vect (S (S predn)) $ Matrix (S (S predn)) (S predm) ZZ
		endmat = getWitness endMatAndPropFn
		endmatPropFn : (i : Fin (S (S predn)))
			-> succImplWknProp mat (v<\>mat) (S predn) i (index i endmat)
		endmatPropFn = getProof endMatAndPropFn
		bisWithGCD : (v<\>mat)::mat `bispanslz` mat
		bisWithGCD =
			(extendSpanningLZsByPreconcatTrivially {zs=[_]} spanslzrefl
			, mergeSpannedLZs spanslzRowTimesSelf spanslzrefl)
		{- In tuple match: headvecWasFixed = fst $ endmatPropFn FZ -}
		leftColZBelow : downAndNotRightOfEntryImpliesZ (index FZ endmat) FZ FZ
		leftColZBelow = fst . snd $ endmatPropFn FZ
		endmatBispansMatandgcd : (index FZ endmat) `bispanslz` ((v<\>mat)::mat)
		endmatBispansMatandgcd = snd . snd $ endmatPropFn FZ

}


text:
module Compiler.Opts.Identity

import Compiler.CompileExpr
import Core.Context
import Core.Context.Log
import Data.List
import Data.Vect

makeArgs : (args : List Name) -> List (Var (args ++ vars))
makeArgs args = makeArgs' args id
  where
    makeArgs' : (args : List Name) -> (Var (args ++ vars) -> a) -> List a
    makeArgs' [] f = []
    makeArgs' (x :: xs) f = f (MkVar First) :: makeArgs' xs (f . weaken)

parameters (fn1 : Name) (idIdx : Nat)
  mutual
    -- special case for matching on 'Nat'-shaped things
    isUnsucc : Var vars -> CExp vars -> Maybe (Constant, Var (x :: vars))
    isUnsucc (MkVar {i} _) (COp _ (Sub _) [CLocal {idx} _ _, CPrimVal _ c]) =
        if i == idx
            then Just (c, MkVar First)
            else Nothing
    isUnsucc _ _ = Nothing

    unsuccIdentity : Constant -> Var vars -> CExp vars -> Bool
    unsuccIdentity c1 var (COp _ (Add _) [exp, CPrimVal _ c2]) = c1 == c2 && cexpIdentity var Nothing Nothing exp
    unsuccIdentity _ _ _ = False

    -- does the CExp evaluate to the var, the constructor or the constant?
    cexpIdentity : Var vars -> Maybe (Name, List (Var vars)) -> Maybe Constant -> CExp vars -> Bool
    cexpIdentity (MkVar {i} _) _ _ (CLocal {idx} fc p) = idx == i
    cexpIdentity var _ _ (CRef _ _) = False
    cexpIdentity var _ _ (CLam _ _ _) = False
    cexpIdentity var con const (CLet _ _ _ val sc) = (case isUnsucc var val of
        Just (c, var') => unsuccIdentity c var' sc
        Nothing => False)
        || cexpIdentity
            (weaken var)
            (map (map (map weaken)) con)
            const
            sc
    cexpIdentity var con const (CApp _ (CRef _ fn2) as) = -- special case for self-recursive functions
        fn1 == fn2 &&
        case getAt idIdx as of
            Just exp => cexpIdentity var con const exp
            Nothing => False
    cexpIdentity _ _ _ (CApp _ _ _) = False
    cexpIdentity var (Just (con1, as1)) const (CCon _ con2 _ _ as2) =
        con1 == con2
        && eqArgs as1 as2
      where
        eqArgs : List (Var vars) -> List (CExp vars) -> Bool
        eqArgs [] [] = True
        eqArgs (v :: vs) (a :: as) = cexpIdentity v Nothing Nothing a && eqArgs vs as
        eqArgs _ _ = False
    cexpIdentity var Nothing const (CCon _ _ _ _ _) = False
    -- special case for integerToNat, see unsuccIdentity for a easier to read
    -- version that works when the let hasn't been inlined.
    -- integerToNat : (x : Integer) -> {auto 0 _ : (x >= 0) === True} -> Nat
    -- integerToNat x = case x of
    --                       0 => Z
    --                       _ => S $ integerToNat (x - 1)
    cexpIdentity var _ _ (COp _ (Add _) [a1, a2]) = case a2 of
        CPrimVal _ c1 => case a1 of
            CApp _ (CRef _ fn2) as =>
                fn1 == fn2
                && (case getAt idIdx as of
                    Just (COp _ (Sub _) [a3, (CPrimVal _ c2)]) =>
                        c1 == c2 && cexpIdentity var Nothing Nothing a3
                    _ => False)
            _ => False
        _ => False
    cexpIdentity var _ _ (COp _ _ _) = False
    cexpIdentity var _ _ (CExtPrim _ _ _) = False
    cexpIdentity var _ _ (CForce _ _ _) = False
    cexpIdentity var _ _ (CDelay _ _ _) = False
    cexpIdentity var con const (CConCase _ sc xs x) =
        cexpIdentity var Nothing Nothing sc
        && all altEq xs
        && maybeVarEq var con const x
      where

        altEq : CConAlt vars -> Bool
        altEq (MkConAlt y _ _ args exp) =
            cexpIdentity
                (weakenNs (mkSizeOf args) var)
                (Just (y, makeArgs args))
                const
                exp
    cexpIdentity var con const (CConstCase fc sc xs x) =
        cexpIdentity var Nothing Nothing sc
        && all altEq xs
        && maybeVarEq var con const x
    where
        altEq : CConstAlt vars -> Bool
        altEq (MkConstAlt c exp) = cexpIdentity var con (Just c) exp
    cexpIdentity _ _ (Just c1) (CPrimVal _ c2) = c1 == c2
    cexpIdentity _ _ Nothing (CPrimVal _ _) = False
    cexpIdentity _ _ _ (CErased _) = False
    cexpIdentity _ _ _ (CCrash _ _) = False

    -- fused `all (cexpIdentity var con const)`
    maybeVarEq : Var vars -> Maybe (Name, List (Var vars)) -> Maybe Constant -> Maybe (CExp vars) -> Bool
    maybeVarEq _ _ _ Nothing = True
    maybeVarEq var con const (Just exp) = cexpIdentity var con const exp

checkIdentity : (fullName : Name) -> List (Var vars) -> CExp vars -> Nat -> Maybe Nat
checkIdentity _ [] _ _ = Nothing
checkIdentity fn (v :: vs) exp idx = if cexpIdentity fn idx v Nothing Nothing exp
    then Just idx
    else checkIdentity fn vs exp (S idx)

calcIdentity : (fullName : Name) -> CDef -> Maybe Nat
calcIdentity fn (MkFun args exp) = checkIdentity fn (makeArgs {vars=[]} args) (rewrite appendNilRightNeutral args in exp) Z
calcIdentity _ _ = Nothing

getArg : FC -> Nat -> (args : List Name) -> Maybe (CExp args)
getArg _ _ [] = Nothing
getArg fc Z (a :: _) = Just $ CLocal fc First
getArg fc (S k) (_ :: as) = weaken <$> getArg fc k as

idCDef : Nat -> CDef -> Maybe CDef
idCDef idx (MkFun args exp) = MkFun args <$> getArg (getFC exp) idx args
idCDef _ def = Just def

export
rewriteIdentityFlag : Ref Ctxt Defs => Name -> Core ()
rewriteIdentityFlag fn = do
    defs <- get Ctxt
    Just (fnIdx, gdef) <- lookupCtxtExactI fn defs.gamma
        | Nothing => pure ()
    let Just flg@(Identity idx) = find isId gdef.flags
        | _ => pure ()
    log "compiler.identity" 5 $ "found identity flag for: "
                              ++ show !(getFullName fn) ++ ", " ++ show idx
                              ++ "\n\told def: " ++ show gdef.compexpr
    let Just cdef = the _ $ gdef.compexpr >>= idCDef idx
        | Nothing => pure ()
    log "compiler.identity" 5 $ "\tnew def: " ++ show cdef
    unsetFlag EmptyFC (Resolved fnIdx) flg -- other optimisations might mess with argument counts
    setFlag EmptyFC (Resolved fnIdx) Inline
    setCompiled (Resolved fnIdx) cdef
  where
    isId : DefFlag -> Bool
    isId (Identity _) = True
    isId _ = False

export
setIdentity : Ref Ctxt Defs => Name -> Core ()
setIdentity fn = do
    defs <- get Ctxt
    Just (fnIdx, gdef) <- lookupCtxtExactI fn defs.gamma
        | Nothing => pure ()
    let Just idx = the _ $ gdef.compexpr >>= calcIdentity fn
        | Nothing => pure ()
    setFlag EmptyFC (Resolved fnIdx) (Identity idx)
    rewriteIdentityFlag (Resolved fnIdx)


text:
module Compiler.Scheme.Chez

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

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

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

import Idris.Env

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

import Libraries.Data.NameMap
import Libraries.Data.Version
import Libraries.Utils.String

%default covering

export
findChez : IO String
findChez
    = do Nothing <- idrisGetEnv "CHEZ"
            | Just chez => pure chez
         path <- pathLookup ["chez", "chezscheme", "chez-scheme", "chezscheme9.5", "scheme"]
         pure $ fromMaybe "/usr/bin/env scheme" path

||| Returns the chez scheme version for given executable
|||
||| This uses `chez --version` which unfortunately writes the version
||| on `stderr` thus requiring suffixing the command which shell redirection
||| which does not seem very portable.
export
chezVersion : String -> IO (Maybe Version)
chezVersion chez = do
    Right fh <- popen cmd Read
        | Left err => pure Nothing
    Right output <- fGetLine fh
        | Left err => pure Nothing
    pclose fh
    pure $ parseVersion output
  where
  cmd : String
  cmd = chez ++ " --version 2>&1"

unsupportedCallingConvention : Maybe Version -> Bool
unsupportedCallingConvention Nothing = True
unsupportedCallingConvention (Just version) = version < MkVersion (9,5,0) Nothing

-- Given the chez compiler directives, return a list of pairs of:
--   - the library file name
--   - the full absolute path of the library file name, if it's in one
--     of the library paths managed by Idris
-- If it can't be found, we'll assume it's a system library and that chez
-- will thus be able to find it.
export
findLibs : {auto c : Ref Ctxt Defs} ->
           List String -> Core (List (String, String))
findLibs ds
    = do let libs = mapMaybe (isLib . trim) ds
         traverse locate (nub libs)
  where
    isLib : String -> Maybe String
    isLib d
        = if isPrefixOf "lib" d
             then Just (trim (substr 3 (length d) d))
             else Nothing

schHeader : String -> List String -> Bool -> String
schHeader chez libs whole
  = (if os /= "windows"
        then "#!" ++ chez ++ (if whole then " --program\n\n" else " --script\n\n")
        else "") ++
    "; " ++ (generatedString "Chez") ++ "\n" ++
    "(import (chezscheme))\n" ++
    "(case (machine-type)\n" ++
    "  [(i3fb ti3fb a6fb ta6fb) #f]\n" ++
    "  [(i3le ti3le a6le ta6le tarm64le) (load-shared-object \"libc.so.6\")]\n" ++
    "  [(i3osx ti3osx a6osx ta6osx tarm64osx) (load-shared-object \"libc.dylib\")]\n" ++
    "  [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")]\n" ++
    "  [else (load-shared-object \"libc.so\")])\n\n" ++
    showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeStringChez x ++ "\")") libs) ++ "\n\n" ++
    if whole
       then "(let ()\n"
       else "(source-directories (cons (getenv \"IDRIS2_INC_SRC\") (source-directories)))\n"

schFooter : Bool -> Bool -> String
schFooter prof whole
    = "(collect 4)\n(blodwen-run-finalisers)\n" ++
      (if prof
          then "(profile-dump-html)"
          else "") ++
      (if whole
          then ")\n" else "\n")

showChezChar : Char -> String -> String
showChezChar '\\' = ("\\\\" ++)
showChezChar c
   = if c < chr 32 || c > chr 126
        then (("\\x" ++ asHex (cast c) ++ ";") ++)
        else strCons c

showChezString : List Char -> String -> String
showChezString [] = id
showChezString ('"'::cs) = ("\\\"" ++) . showChezString cs
showChezString (c ::cs) = (showChezChar c) . showChezString cs

export
chezString : String -> String
chezString cs = strCons '"' (showChezString (unpack cs) "\"")

mutual
  handleRet : String -> String -> String
  handleRet "void" op = op ++ " " ++ mkWorld (schConstructor chezString (UN $ Basic "") (Just 0) [])
  handleRet _ op = mkWorld op

  getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp))
  getFArgs (NmCon fc _ _ (Just 0) _) = pure []
  getFArgs (NmCon fc _ _ (Just 1) [ty, val, rest]) = pure $ (ty, val) :: !(getFArgs rest)
  getFArgs arg = throw (GenericMsg (getFC arg) ("Badly formed c call argument list " ++ show arg))

  export
  chezExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String
  chezExtPrim i GetField [NmPrimVal _ (Str s), _, _, struct,
                          NmPrimVal _ (Str fld), _]
      = do structsc <- schExp chezExtPrim chezString 0 struct
           pure $ "(ftype-ref " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++ ")"
  chezExtPrim i GetField [_,_,_,_,_,_]
      = pure "(blodwen-error-quit \"bad getField\")"
  chezExtPrim i SetField [NmPrimVal _ (Str s), _, _, struct,
                          NmPrimVal _ (Str fld), _, val, world]
      = do structsc <- schExp chezExtPrim chezString 0 struct
           valsc <- schExp chezExtPrim chezString 0 val
           pure $ mkWorld $
              "(ftype-set! " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++
              " " ++ valsc ++ ")"
  chezExtPrim i SetField [_,_,_,_,_,_,_,_]
      = pure "(blodwen-error-quit \"bad setField\")"
  chezExtPrim i SysCodegen []
      = pure $ "\"chez\""
  chezExtPrim i OnCollect [_, p, c, world]
      = do p' <- schExp chezExtPrim chezString 0 p
           c' <- schExp chezExtPrim chezString 0 c
           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
  chezExtPrim i OnCollectAny [p, c, world]
      = do p' <- schExp chezExtPrim chezString 0 p
           c' <- schExp chezExtPrim chezString 0 c
           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
  chezExtPrim i MakeFuture [_, work]
      = do work' <- schExp chezExtPrim chezString 0 work
           pure $ "(blodwen-make-future " ++ work' ++ ")"
  chezExtPrim i prim args
      = schExtCommon chezExtPrim chezString i prim args

-- Reference label for keeping track of loaded external libraries
export
data Loaded : Type where

-- Label for noting which struct types are declared
export
data Structs : Type where

cftySpec : FC -> CFType -> Core String
cftySpec fc CFUnit = pure "void"
cftySpec fc CFInt = pure "int"
cftySpec fc CFInt8 = pure "integer-8"
cftySpec fc CFInt16 = pure "integer-16"
cftySpec fc CFInt32 = pure "integer-32"
cftySpec fc CFInt64 = pure "integer-64"
cftySpec fc CFUnsigned8 = pure "unsigned-8"
cftySpec fc CFUnsigned16 = pure "unsigned-16"
cftySpec fc CFUnsigned32 = pure "unsigned-32"
cftySpec fc CFUnsigned64 = pure "unsigned-64"
cftySpec fc CFString = pure "string"
cftySpec fc CFDouble = pure "double"
cftySpec fc CFChar = pure "char"
cftySpec fc CFPtr = pure "void*"
cftySpec fc CFGCPtr = pure "void*"
cftySpec fc CFBuffer = pure "u8*"
cftySpec fc (CFFun s t) = pure "void*"
cftySpec fc (CFIORes t) = cftySpec fc t
cftySpec fc (CFStruct n t) = pure $ "(* " ++ n ++ ")"
cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
                         " to foreign function"))

export
loadLib : {auto c : Ref Ctxt Defs} ->
          String -> String -> Core String
loadLib appdir clib
    = do (fname, fullname) <- locate clib
         copyLib (appdir </> fname, fullname)
         pure $ "(load-shared-object \""
                                    ++ escapeStringChez fname
                                    ++ "\")\n"

loadSO : {auto c : Ref Ctxt Defs} ->
         String -> String -> Core String
loadSO appdir "" = pure ""
loadSO appdir mod
    = do d <- getDirs
         let fs = map (\p => p </> mod)
                      ((build_dir d </> "ttc") :: extra_dirs d)
         Just fname <- firstAvailable fs
            | Nothing => throw (InternalError ("Missing .so:" ++ mod))
         -- Easier to put them all in the same directory, so we don't need
         -- to traverse a directory tree when installing the executable. So,
         -- separate with '-' rather than directory separators.
         let modfname = fastConcat (intersperse "-" (splitPath mod))
         copyLib (appdir </> modfname, fname)
         pure $ "(load \"" ++ escapeStringChez modfname ++ "\")\n"

cCall : {auto c : Ref Ctxt Defs}
     -> {auto l : Ref Loaded (List String)}
     -> FC
     -> (cfn : String)
     -> (clib : String)
     -> List (Name, CFType)
     -> CFType
     -> (collectSafe : Bool)
     -> Core (Maybe String, String)
cCall fc cfn clib args (CFIORes CFGCPtr) _
    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall fc cfn clib args CFGCPtr _
    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall fc cfn clib args (CFIORes CFBuffer) _
    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall fc cfn clib args CFBuffer _
    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall fc cfn clib args ret collectSafe
    = do loaded <- get Loaded
         lib <- if clib `elem` loaded
                   then pure Nothing
                   else do put Loaded (clib :: loaded)
                           pure (Just clib)
         argTypes <- traverse (cftySpec fc . snd) args
         retType <- cftySpec fc ret
         let callConv = if collectSafe then " __collect_safe" else ""
         let call = "((foreign-procedure" ++ callConv ++ " " ++ show cfn ++ " ("
                      ++ showSep " " argTypes ++ ") " ++ retType ++ ") "
                      ++ showSep " " !(traverse buildArg args) ++ ")"

         pure (lib, case ret of
                         CFIORes _ => handleRet retType call
                         _ => call)
  where
    mkNs : Int -> List CFType -> List (Maybe String)
    mkNs i [] = []
    mkNs i (CFWorld :: xs) = Nothing :: mkNs i xs
    mkNs i (x :: xs) = Just ("cb" ++ show i) :: mkNs (i + 1) xs

    applyLams : String -> List (Maybe String) -> String
    applyLams n [] = n
    applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as
    applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as

    getVal : String -> String
    getVal str = "(vector-ref " ++ str ++ "1)"

    mkFun : List CFType -> CFType -> String -> String
    mkFun args ret n
        = let argns = mkNs 0 args in
              "(lambda (" ++ showSep " " (mapMaybe id argns) ++ ") " ++
              (applyLams n argns ++ ")")

    notWorld : CFType -> Bool
    notWorld CFWorld = False
    notWorld _ = True

    callback : String -> List CFType -> CFType -> Core String
    callback n args (CFFun s t) = callback n (s :: args) t
    callback n args_rev retty
        = do let args = reverse args_rev
             argTypes <- traverse (cftySpec fc) (filter notWorld args)
             retType <- cftySpec fc retty
             pure $
                 "(let ([c-code (foreign-callable #f " ++
                       mkFun args retty n ++
                       " (" ++ showSep " " argTypes ++ ") " ++ retType ++ ")])" ++
                       " (lock-object c-code) (foreign-callable-entry-point c-code))"

    buildArg : (Name, CFType) -> Core String
    buildArg (n, CFFun s t) = callback (schName n) [s] t
    buildArg (n, CFGCPtr) = pure $ "(car " ++ schName n ++ ")"
    buildArg (n, _) = pure $ schName n

schemeCall : FC -> (sfn : String) ->
             List Name -> CFType -> Core String
schemeCall fc sfn argns ret
    = let call = "(" ++ sfn ++ " " ++ showSep " " (map schName argns) ++ ")" in
          case ret of
               CFIORes _ => pure $ mkWorld call
               _ => pure call

-- Use a calling convention to compile a foreign def.
-- Returns any preamble needed for loading libraries, and the body of the
-- function call.
useCC : {auto c : Ref Ctxt Defs} ->
        {auto l : Ref Loaded (List String)} ->
        FC -> List String -> List (Name, CFType) -> CFType ->
        Maybe Version -> Core (Maybe String, String)
useCC fc ccs args ret version
    = case parseCC ["scheme,chez", "scheme", "C__collect_safe", "C"] ccs of
           Just ("scheme,chez", [sfn]) =>
               do body <- schemeCall fc sfn (map fst args) ret
                  pure (Nothing, body)
           Just ("scheme", [sfn]) =>
               do body <- schemeCall fc sfn (map fst args) ret
                  pure (Nothing, body)
           Just ("C__collect_safe", (cfn :: clib :: _)) => do
             if unsupportedCallingConvention version
               then cCall fc cfn clib args ret False
               else cCall fc cfn clib args ret True
           Just ("C", (cfn :: clib :: _)) =>
             cCall fc cfn clib args ret False
           _ => throw (NoForeignCC fc ccs)

-- For every foreign arg type, return a name, and whether to pass it to the
-- foreign call (we don't pass '%World')
mkArgs : Int -> List CFType -> List (Name, Bool)
mkArgs i [] = []
mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs i cs
mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs

mkStruct : {auto s : Ref Structs (List String)} ->
           CFType -> Core String
mkStruct (CFStruct n flds)
    = do defs <- traverse mkStruct (map snd flds)
         strs <- get Structs
         if n `elem` strs
            then pure (concat defs)
            else do put Structs (n :: strs)
                    pure $ concat defs ++ "(define-ftype " ++ n ++ " (struct\n\t"
                           ++ showSep "\n\t" !(traverse showFld flds) ++ "))\n"
  where
    showFld : (String, CFType) -> Core String
    showFld (n, ty) = pure $ "[" ++ n ++ " " ++ !(cftySpec emptyFC ty) ++ "]"
mkStruct (CFIORes t) = mkStruct t
mkStruct (CFFun a b) = do ignore (mkStruct a); mkStruct b
mkStruct _ = pure ""

schFgnDef : {auto c : Ref Ctxt Defs} ->
            {auto l : Ref Loaded (List String)} ->
            {auto s : Ref Structs (List String)} ->
            FC -> Name -> NamedDef -> Maybe Version ->
            Core (Maybe String, String)
schFgnDef fc n (MkNmForeign cs args ret) version
    = do let argns = mkArgs 0 args
         let allargns = map fst argns
         let useargns = map fst (filter snd argns)
         argStrs <- traverse mkStruct args
         retStr <- mkStruct ret
         (load, body) <- useCC fc cs (zip useargns args) ret version
         defs <- get Ctxt
         pure (load,
                concat argStrs ++ retStr ++
                "(define " ++ schName !(full (gamma defs) n) ++
                " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++
                body ++ "))\n")
schFgnDef _ _ _ _ = pure (Nothing, "")

export
getFgnCall : {auto c : Ref Ctxt Defs} ->
             {auto l : Ref Loaded (List String)} ->
             {auto s : Ref Structs (List String)} ->
             Maybe Version -> (Name, FC, NamedDef) ->
             Core (Maybe String, String)
getFgnCall version (n, fc, d) = schFgnDef fc n d version

export
startChezPreamble : String
startChezPreamble = unlines
    [ "#!/bin/sh"
    , "# " ++ (generatedString "Chez")
    , ""
    , "set -e # exit on any error"
    , ""
    , "if [ \"$(uname)\" = Darwin ]; then"
    , "  DIR=$(zsh -c 'printf %s \"$0:A:h\"' \"$0\")"
    , "else"
    , "  DIR=$(dirname \"$(readlink -f -- \"$0\")\")"
    , "fi"
    , ""  -- so that the preamble ends with a newline
    ]

startChez : String -> String -> String
startChez appdir target = startChezPreamble ++ unlines
    [ "export LD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ ":$LD_LIBRARY_PATH\""
    , "export IDRIS2_INC_SRC=\"$DIR/" ++ appdir ++ "\""
    , "\"$DIR/" ++ target ++ "\" \"$@\""
    ]

startChezCmd : String -> String -> String -> String -> String
startChezCmd chez appdir target progType = unlines
    [ "@echo off"
    , "set APPDIR=%~dp0"
    , "set PATH=%APPDIR%" ++ appdir ++ ";%PATH%"
    , "set IDRIS2_INC_SRC=%APPDIR%" ++ appdir
    , "\"" ++ chez ++ "\" " ++ progType ++ " \"%APPDIR%" ++ target ++ "\" %*"
    ]

startChezWinSh : String -> String -> String -> String -> String
startChezWinSh chez appdir target progType = unlines
    [ "#!/bin/sh"
    , "# " ++ (generatedString "Chez")
    , ""
    , "set -e # exit on any error"
    , ""
    , "DIR=$(dirname \"$(readlink -f -- \"$0\" || cygpath -a -- \"$0\")\")"
    , "PATH=\"$DIR/" ++ appdir ++ ":$PATH\""
    , "export IDRIS2_INC_SRC=\"$DIR/" ++ appdir ++ "\""
    , "\"" ++ chez ++ "\" " ++ progType ++ " \"$DIR/" ++ target ++ "\" \"$@\""
    ]

||| Compile a TT expression to Chez Scheme
compileToSS : Ref Ctxt Defs ->
              Bool -> -- profiling
              String -> ClosedTerm -> (outfile : String) -> Core ()
compileToSS c prof appdir tm outfile
    = do ds <- getDirectives Chez
         libs <- findLibs ds
         traverse_ copyLib libs
         cdata <- getCompileData False Cases tm
         let ndefs = namedDefs cdata
         let ctm = forget (mainExpr cdata)

         defs <- get Ctxt
         l <- newRef {t = List String} Loaded ["libc", "libc 6"]
         s <- newRef {t = List String} Structs []
         chez <- coreLift findChez
         version <- coreLift $ chezVersion chez
         fgndefs <- traverse (getFgnCall version) ndefs
         loadlibs <- traverse (loadLib appdir) (mapMaybe fst fgndefs)

         compdefs <- traverse (getScheme chezExtPrim chezString) ndefs
         let code = fastAppend (map snd fgndefs ++ compdefs)
         main <- schExp chezExtPrim chezString 0 ctm
         support <- readDataFile "chez/support.ss"
         extraRuntime <- getExtraRuntime ds
         let scm = schHeader chez (map snd libs) True ++
                   support ++ extraRuntime ++ code ++
                   concat loadlibs ++
                   "(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))\n" ++
                   main ++ schFooter prof True
         Right () <- coreLift $ writeFile outfile scm
            | Left err => throw (FileErr outfile err)
         coreLift_ $ chmodRaw outfile 0o755
         pure ()

||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off.
compileToSO : {auto c : Ref Ctxt Defs} ->
              Bool -> -- profiling
              String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
compileToSO prof chez appDirRel outSsAbs
    = do let tmpFileAbs = appDirRel </> "compileChez"
         let build = "(parameterize ([optimize-level 3] "
                     ++ (if prof then "[compile-profile #t] "
                                else "") ++
                     "[compile-file-message #f]) (compile-program " ++
                    show outSsAbs ++ "))"
         Right () <- coreLift $ writeFile tmpFileAbs build
            | Left err => throw (FileErr tmpFileAbs err)
         coreLift_ $ chmodRaw tmpFileAbs 0o755
         coreLift_ $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"")
         pure ()

||| Compile a TT expression to Chez Scheme using incremental module builds
compileToSSInc : Ref Ctxt Defs ->
                 List String -> -- module so files
                 List String -> -- libraries to find and load
                 String -> ClosedTerm -> (outfile : String) -> Core ()
compileToSSInc c mods libs appdir tm outfile
    = do chez <- coreLift findChez
         tmcexp <- compileTerm tm
         let ctm = forget tmcexp

         loadlibs <- traverse (loadLib appdir) (nub libs)
         loadsos <- traverse (loadSO appdir) (nub mods)

         main <- schExp chezExtPrim chezString 0 ctm
         support <- readDataFile "chez/support.ss"

         let scm = schHeader chez [] False ++
                   support ++
                   concat loadlibs ++
                   concat loadsos ++
                   "(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))\n" ++
                   main ++ schFooter False False

         Right () <- coreLift $ writeFile outfile scm
            | Left err => throw (FileErr outfile err)
         coreLift_ $ chmodRaw outfile 0o755
         pure ()

makeSh : String -> String -> String -> Core ()
makeSh outShRel appdir outAbs
    = do Right () <- coreLift $ writeFile outShRel (startChez appdir outAbs)
            | Left err => throw (FileErr outShRel err)
         pure ()

||| Make Windows start scripts, one for bash environments and one batch file
makeShWindows : String -> String -> String -> String -> String -> Core ()
makeShWindows chez outShRel appdir outAbs progType
    = do let cmdFile = outShRel ++ ".cmd"
         Right () <- coreLift $ writeFile cmdFile (startChezCmd chez appdir outAbs progType)
            | Left err => throw (FileErr cmdFile err)
         Right () <- coreLift $ writeFile outShRel (startChezWinSh chez appdir outAbs progType)
            | Left err => throw (FileErr outShRel err)
         pure ()

compileExprWhole : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
                   ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExprWhole makeitso c tmpDir outputDir tm outfile
    = do let appDirRel = outfile ++ "_app" -- relative to build dir
         let appDirGen = outputDir </> appDirRel -- relative to here
         coreLift_ $ mkdirAll appDirGen
         Just cwd <- coreLift currentDir
              | Nothing => throw (InternalError "Can't get current directory")
         let outSsFile = appDirRel </> outfile <.> "ss"
         let outSoFile = appDirRel </> outfile <.> "so"
         let outSsAbs = cwd </> outputDir </> outSsFile
         let outSoAbs = cwd </> outputDir </> outSoFile
         chez <- coreLift $ findChez
         let prof = profile !getSession
         compileToSS c (makeitso && prof) appDirGen tm outSsAbs
         logTime "++ Make SO" $ when makeitso $
           compileToSO prof chez appDirGen outSsAbs
         let outShRel = outputDir </> outfile
         if isWindows
            then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile) "--program"
            else makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile)
         coreLift_ $ chmodRaw outShRel 0o755
         pure (Just outShRel)

compileExprInc : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
                 ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExprInc makeitso c tmpDir outputDir tm outfile
    = do defs <- get Ctxt
         let Just (mods, libs) = lookup Chez (allIncData defs)
             | Nothing =>
                 do coreLift $ putStrLn $ "Missing incremental compile data, reverting to whole program compilation"
                    compileExprWhole makeitso c tmpDir outputDir tm outfile
         let appDirRel = outfile ++ "_app" -- relative to build dir
         let appDirGen = outputDir </> appDirRel -- relative to here
         coreLift_ $ mkdirAll appDirGen
         Just cwd <- coreLift currentDir
              | Nothing => throw (InternalError "Can't get current directory")
         let outSsFile = appDirRel </> outfile <.> "ss"
         let outSoFile = appDirRel </> outfile <.> "so"
         let outSsAbs = cwd </> outputDir </> outSsFile
         let outSoAbs = cwd </> outputDir </> outSoFile
         chez <- coreLift $ findChez
         compileToSSInc c mods libs appDirGen tm outSsAbs
         let outShRel = outputDir </> outfile
         if isWindows
            then makeShWindows chez outShRel appDirRel outSsFile "--script"
            else makeSh outShRel appDirRel outSsFile
         coreLift_ $ chmodRaw outShRel 0o755
         pure (Just outShRel)

||| Chez Scheme implementation of the `compileExpr` interface.
compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
              ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr makeitso c tmpDir outputDir tm outfile
    = do s <- getSession
         if not (wholeProgram s) && (Chez `elem` incrementalCGs !getSession)
            then compileExprInc makeitso c tmpDir outputDir tm outfile
            else compileExprWhole makeitso c tmpDir outputDir tm outfile

||| Chez Scheme implementation of the `executeExpr` interface.
||| This implementation simply runs the usual compiler, saving it to a temp file, then interpreting it.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm
    = do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpchez"
            | Nothing => throw (InternalError "compileExpr returned Nothing")
         coreLift_ $ system sh
         pure ()

incCompile : Ref Ctxt Defs ->
             (sourceFile : String) -> Core (Maybe (String, List String))
incCompile c sourceFile
    = do
         ssFile <- getTTCFileName sourceFile "ss"
         soFile <- getTTCFileName sourceFile "so"
         soFilename <- getObjFileName sourceFile "so"
         cdata <- getIncCompileData False Cases

         d <- getDirs
         let outputDir = build_dir d </> "ttc"

         let ndefs = namedDefs cdata
         if isNil ndefs
            then pure (Just ("", []))
                      -- ^ no code to generate, but still recored that the
                      -- module has been compiled, with no output needed.
            else do
               l <- newRef {t = List String} Loaded ["libc", "libc 6"]
               s <- newRef {t = List String} Structs []
               chez <- coreLift findChez
               version <- coreLift $ chezVersion chez
               fgndefs <- traverse (getFgnCall version) ndefs
               compdefs <- traverse (getScheme chezExtPrim chezString) ndefs
               let code = fastAppend (map snd fgndefs ++ compdefs)
               Right () <- coreLift $ writeFile ssFile code
                  | Left err => throw (FileErr ssFile err)

               -- Compile to .so
               let tmpFileAbs = outputDir </> "compileChez"
               let build = "(parameterize ([optimize-level 3] " ++
                           "[compile-file-message #f]) (compile-file " ++
                          show ssFile ++ "))"
               Right () <- coreLift $ writeFile tmpFileAbs build
                  | Left err => throw (FileErr tmpFileAbs err)
               coreLift_ $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"")
               pure (Just (soFilename, mapMaybe fst fgndefs))

||| Codegen wrapper for Chez scheme implementation.
export
codegenChez : Codegen
codegenChez = MkCG (compileExpr True) executeExpr (Just incCompile) (Just "so")


text:
module GettingStarted

%default total

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

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

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


text:
module Twicer
import Service
import System
import Numeric

%default total

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

public export
twicerContract : (a : Integer) -> Contract (runTwicer a) Integer
twicerContract a = MkContract (runTwicer a)

public export
twicerService : Integer -> Service Integer
twicerService a = Promise (twicerContract a)

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Function

import IdrisJvm.IO
import Java.Lang

%access public export

namespace Function
  FunctionInterface : JVM_NativeTy
  FunctionInterface = Interface "java/util/function/Function"

  Function : Type
  Function = JVM_Native FunctionInterface

  %inline
  jlambda : fTy -> {auto jvmElemTy: JVM_FnTypes fTy} -> Function
  jlambda f = javalambda "apply" (Object -> Object) f

  apply : (Inherits Function function, Inherits Object arg) => function -> arg -> JVM_IO Object
  apply function arg = invokeInstance "apply" (Function -> Object -> JVM_IO Object) (believe_me function) (believe_me arg)

namespace BiFunction
  BiFunctionInterface : JVM_NativeTy
  BiFunctionInterface = Interface "java/util/function/BiFunction"

  BiFunction : Type
  BiFunction = JVM_Native BiFunctionInterface

  %inline
  jlambda : fTy -> {auto jvmElemTy: JVM_FnTypes fTy} -> BiFunction
  jlambda f = javalambda "apply" (Object -> Object -> Object) f

  apply : (Inherits BiFunction function, Inherits Object arg1, Inherits Object arg2) => function -> arg1 -> arg2 -> JVM_IO Object
  apply function arg1 arg2 = invokeInstance "apply" (BiFunction -> Object -> Object -> JVM_IO Object) (believe_me function) (believe_me arg1) (believe_me arg2)

namespace Predicate
  Predicate : Type
  Predicate = javaInterface "java/util/function/Predicate"

  %inline
  jlambda : fTy -> {auto jvmElemTy: JVM_FnTypes fTy} -> Predicate
  jlambda f = javalambda "test" (Object -> Bool) f

namespace Supplier
  Supplier : Type
  Supplier = javaInterface "java/util/function/Supplier"

  %inline
  jlambda : JVM_IO ty -> {auto jvmTy: JVM_Types ty} -> Supplier
  jlambda {ty} f = javalambda "get" (JVM_IO Object) g
    where
      g : () -> ty
      g x = believe_me $ unsafePerformIO f

namespace IntUnaryOperator
  IntUnaryOperatorInterface : JVM_NativeTy
  IntUnaryOperatorInterface = Interface "java/util/function/IntUnaryOperator"

  IntUnaryOperator : Type
  IntUnaryOperator = JVM_Native IntUnaryOperatorInterface

  %inline
  jlambda : (Int -> Int) -> IntUnaryOperator
  jlambda f = javalambda "applyAsInt" (Int -> Int) f


text:
module Average

export
average : String -> Double
average s = (cast (totalLength s)) / (cast (numWords s))
  where
    totalLength : String -> Nat
    totalLength s = sum (map length (words s))

    numWords : String -> Nat
    numWords x = length (words x)

max_stars_repo_name: neduard/type-driven-development

max_issues_repo_name: neduard/type-driven-development

max_forks_repo_name: neduard/type-driven-development


text:
module Monoid

%access public export

||| The proof that some element is identity in the type
total
IsIdentity : (mon : Type) -> ((*) : mon -> mon -> mon) -> (e : mon) -> Type
IsIdentity mon (*) e = (a : mon) -> ((a*e) = a, (e*a) = a)

||| Given a type and a binary operation the type of proofs that the operation is associative
total
Associative : (typ : Type) -> ((*): typ -> typ -> typ) -> Type
Associative typ (*) = (a : typ) -> (b : typ) -> (c : typ) -> ((a * b) * c) = (a * (b * c))

||| Given a type and a binary operation the type of proofs that the operation is commutative
total
Commutative : (typ : Type) -> ((*) : typ -> typ -> typ) -> Type
Commutative typ (*) = (a : typ) -> (b : typ) -> (a * b) = (b * a)

||| Given a type and a binary operation the type of proofs that identity exists
total
IdentityExists : (typ : Type) -> ((*) : typ -> typ -> typ) -> Type
IdentityExists typ (*) = (e : typ ** (IsIdentity typ (*) e))
--((a : typ) -> ((a*e) = a, (e*a) = a)))

total
IsMonoid : (mon : Type) -> ((*) : mon -> mon -> mon) -> Type
IsMonoid mon (*) = (Associative mon (*), IdentityExists mon (*))

||| Gives the identity of the monoid
total
Monoid_id : (mon : Type) -> ((*) : mon -> mon -> mon) -> (IsMonoid mon (*))
            -> (IdentityExists mon (*))
Monoid_id mon (*) (pfAss, pfId) = pfId


text:
-- ---------------------------------------------------------------- [ Time.idr ]
--
-- Implementation of the Time Protocol for programs
--
-- --------------------------------------------------------------------- [ EOH ]
module Time

import Effects

import Effect.Default
import Effect.StdIO
import Effect.Msg

import System
import System.Protocol

import RFC.Time

-- ---------------------------------------------------------- [ Server Process ]
||| Implementation of the Time Protocol from the Server's Perspective
covering
timeServer : (proc : PID)
                  -> Process (timeProtocol) 'Server ['Client := proc] [STDIO] ()
timeServer proc = do
    req <- recvFrom 'Client
    let t = systime
    let resp = if t /= 0
                 then Right t
                 else Left "No time"
    sendTo 'Client resp
    return ()

  where
    systime : Int
    systime = unsafePerformIO time

||| Implementation of the Time Protocol from the Clients Perspective.
covering
timeClient : (proc : PID)
                  -> Process (timeProtocol) 'Client ['Server := proc] [STDIO] ()
timeClient proc = do
    sendTo 'Server Nothing
    t <- recvFrom 'Server
    case t of
      Left err => do
        putStrLn $ "Time not returned: " ++ err
        return ()
      Right res => do
        putStrLn $ "The unix time is: " ++ show res
        return ()

-- ------------------------------------------------------ [ Sample Innvocation ]
||| Sample innvocation
covering
doTimeProcess : IO ()
doTimeProcess = runConc [()] doTime'
  where
    doTime' : Process (timeProtocol) 'Client [] [STDIO] ()
    doTime' = do
        server <- spawn timeServer [()]
        setChan 'Server server
        timeClient server
        dropChan 'Server

-- -------------------------------------------------------------------- [ Main ]
namespace Main
  main : IO ()
  main = doTimeProcess
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module Data.Hashable

import Data.Vect

||| A default salt used in the implementation of 'hash'.
export
defaultSalt : Bits64
defaultSalt = 14695981039346656037

infixl 10 `hashWithSalt`
infixl 10 `hash`

||| Interface for type that can be hashed.
||| Minimal implementation: 'hashWithSalt'
public export
interface Hashable a where
    ||| Hash a value with the given salt
    total
    hashWithSalt : Bits64 -> a -> Bits64
    ||| Hash a value with the default salt
    total
    hash : a -> Bits64
    hash = hashWithSalt defaultSalt

||| Combine 2 hashes.
export
combine : Bits64 -> Bits64 -> Bits64
combine h1 h2 = (h1 * 16777619) `prim__xor_Bits64` h2

||| Default implementation of 'hashWithSalt' for types which are smaller than Bits64 (eg Bits32, Int).
export
defaultHashWithSalt : (a -> Bits64) -> Bits64 -> a -> Bits64
defaultHashWithSalt hash salt x = salt `combine` hash x

export
Hashable Bits8 where
    hash = cast
    hashWithSalt = defaultHashWithSalt hash

export
Hashable Bits16 where
    hash = cast
    hashWithSalt = defaultHashWithSalt hash

export
Hashable Bits32 where
    hash = cast
    hashWithSalt = defaultHashWithSalt hash

export
Hashable Bits64 where
    hash = id
    hashWithSalt = defaultHashWithSalt hash

export
Hashable Int where
    hash = cast
    hashWithSalt = defaultHashWithSalt hash

export
Hashable Int8 where
    hash = cast
    hashWithSalt = defaultHashWithSalt hash

export
Hashable Int16 where
    hash = cast
    hashWithSalt = defaultHashWithSalt hash

export
Hashable Int32 where
    hash = cast
    hashWithSalt = defaultHashWithSalt hash

export
Hashable Int64 where
    hash = cast
    hashWithSalt = defaultHashWithSalt hash

export
Hashable Char where
    hash = cast . ord
    hashWithSalt = defaultHashWithSalt hash

export
Hashable Integer where
    hashWithSalt salt x = hashPositive (makeSalt salt x) (abs x)
      where
        makeSalt : Bits64 -> Integer -> Bits64
        makeSalt x y = if y >= 0
            then x
            else negate x

        bits64Max : Integer
        bits64Max = 1 `prim__shl_Integer` 64 - 1

        hashPositive : Bits64 -> Integer -> Bits64
        hashPositive salt x = if x > bits64Max
            then hashPositive
                (hashWithSalt salt
                    (cast {to=Bits64} (x `prim__and_Integer` bits64Max)))
                (assert_smaller x $ x `prim__shr_Integer` 64)
            else hashWithSalt salt (cast {to=Bits64} x)

export
Hashable Nat where
    hash x = hash (cast {to=Integer} x)
    hashWithSalt salt x = hashWithSalt salt (cast {to=Integer} x)

export
Hashable String where
    hashWithSalt salt str = finalise (foldl step (salt, 0) $ fastUnpack str)
      where
        step : (Bits64, Bits64) -> Char -> (Bits64, Bits64)
        step (s, l) x = (hashWithSalt s x, l + 1)
        finalise : (Bits64, Bits64) -> Bits64
        finalise (s, l) = hashWithSalt s l

export
Hashable Bool where
    hash False = 0
    hash True = 1

    hashWithSalt = defaultHashWithSalt hash

export
Hashable a => Hashable (Maybe a) where
    hashWithSalt salt Nothing = hashWithSalt salt 0
    hashWithSalt salt (Just x) = hashWithSalt salt 1 `hashWithSalt` x

export
Hashable a => Hashable (List a) where
    hashWithSalt salt [] = hashWithSalt salt 0
    hashWithSalt salt (x :: xs) =
        salt
            `hashWithSalt` 1
            `hashWithSalt` x
            `hashWithSalt` xs

export
Hashable a => Hashable (SnocList a) where
    hashWithSalt salt [<] = hashWithSalt salt 0
    hashWithSalt salt (sx :< x) =
        salt
            `hashWithSalt` 1
            `hashWithSalt` x
            `hashWithSalt` sx

export
Hashable a => Hashable (Vect len a) where
    hashWithSalt salt [] = hashWithSalt salt 0
    hashWithSalt salt (x :: xs) =
        salt
            `hashWithSalt` 1
            `hashWithSalt` x
            `hashWithSalt` xs


text:
import Data.Vect

{- Dependent types allow parts of a value's type to depend on that value. Another
 - common example of a dependent type is a dependent tuple or pair, where the
 - type of the second value depends on the first value.

 - A dependent pair is defined as follows:

     data DPair : (a : Type) -> (P : a -> Type) -> Type where
         MkDPair : {P : a -> Type} -> (x : a) -> P x -> DPair a P

 - Unpacking the types above gives a good intuition for dependent types.
 - `DPair` constructs the type of the dependent tuple from a Type for the first
 - value and a function from the first value giving the type of the second.
 - `MkDPair` takes the function constructing the type as an implicit argument,
 - and constructs the pair from the first value and the second value, where the
 - first value `x` has type `a` and the second value has type `P x` -}

vec : DPair Nat (\n => Vect n Int) -- Idris anon. function syntax is `\x => result`
vec = MkDPair 2 [3, 4]

{- Idris has syntactic sugar for dependent pairs, where `vec` above can
 - equivalently be written as follows. Here, a pair of type `(T1 ** T2)`
 - contains values of those types, and T2 can depend on the value of T1. -}

vec2 : (n : Nat ** Vect n Int) -- Vect n Int depends on the value n : Nat
vec2 = (2 ** [3, 4])           -- the first element is the length of the second

{- We can even leave out information in the type *and* in the values, which
 - the compiler can infer. -}

vec3 : (n ** Vect n Int)  -- n must be a Nat
vec3 = (_ ** [3, 4])      -- the first value must be the length of the second


text:
module Data.Profunctor.Strong

import Control.Category
import Data.Profunctor.Interface

infixr 3 ***, &&&

||| The `Strong` interface extends `Profunctor` with combinators for working with
||| product types.
|||
||| `first` and `second` lift values in a `Profunctor` to act on the first and
||| second components of a `Pair`, respectively.
|||
||| If we specialize the profunctor p to the function arrow, we get the following type
||| signatures, which may look a bit more familiar:
|||
||| ```
||| first :  (input -> output) -> (input, a) -> (output, a)
||| second : (input -> output) -> (a, input) -> (a, output)
||| ```
||| So, when the `profunctor` is `Function` application (represented by `Morphism`),
||| `first` essentially applies your function
||| to the first element of a `Tuple`, and `second` applies it to
||| the second element (same as `map` would do).
public export
interface Profunctor p => Strong p where
  first  : p a b -> p (a,c) (b,c)
  second : p a b -> p (c,a) (c,b)

||| Compose a value acting on a `Pair` from two values, each acting on one of
||| the components of the `Pair`.
|||
||| Specializing `(***)` to function application would look like this:
||| ```
||| (***) : (a -> b) -> (c -> d) -> (a, c) -> (b, d)
||| ```
||| We take two functions, `f` and `g`, and we transform
||| them into a single function which
||| takes a `Pair` and maps `f` over the first element
||| and `g` over the second.
public export
(***) : Category p => Strong p => p a b -> p c d -> p (a, c) (b, d)
l *** r = first l . second r

||| Compose a value which introduces a `Pair` from two values,
||| each introducing one side of the `Pair`.
|||
||| This combinator is useful when assembling values from smaller components,
||| because it provides a way to support two different types of output.
|||
||| Specializing `(&&&)` to function application would look like this:
||| ```
||| (&&&) : (a -> b) -> (a -> c) -> (a -> (b, c))
||| ```
||| We take two functions, `f` and `g`, with the same parameter
||| type and we transform them into a
||| single function which takes one parameter and
||| returns a `Pair` of the results of running
||| `f` and `g` on the parameter, respectively.
||| This allows us to run two parallel computations
||| on the same input and return both results in a `Pair`.
public export
(&&&) : Category p => Strong p => p a b -> p a c -> p a (b, c)
l &&& r = clmap dup (l *** r)

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

public export
Strong Morphism where
  first  (Mor f) = Mor $ mapFst f
  second (Mor f) = Mor $ mapSnd f

public export
Functor m => Strong (Kleislimorphism m) where
  first  (Kleisli f) = Kleisli $ \(a,c) => (,c) <$> f a
  second (Kleisli f) = Kleisli $ \(c,a) => (c,) <$> f a

public export
Strong (Forget r) where
  first  (MkForget f) = MkForget $ \(a,_) => f a
  second (MkForget f) = MkForget $ \(_,a) => f a


text:
module Data.Proxy

import Data.Stream

data Proxy a = MkProxy

%inline
public export
Functor Proxy where
  map f MkProxy = MkProxy

%inline
public export
Applicative Proxy where
  pure _  = MkProxy
  _ <*> _ = MkProxy

%inline
public export
Alternative Proxy where
  empty = MkProxy
  _ <|> _ = MkProxy

%inline
public export
Monad Proxy where
  _ >>= _ = MkProxy
  join _ = MkProxy

%inline
public export
Semigroup (Proxy a) where
  _ <+> _ = MkProxy

%inline
public export
Monoid (Proxy a) where
  neutral = MkProxy

%inline
public export
Eq (Proxy a) where
  _ == _ = True
  _ /= _ = False

%inline
public export
Ord (Proxy a) where
  compare _ _ = EQ

%inline
public export
Show (Proxy a) where
  show _ = "MkProxy"

public export
Range (Proxy a) where
  rangeFromTo _ _ = [MkProxy]
  rangeFromThenTo _ _ _ = [MkProxy]

  rangeFrom _ = repeat MkProxy
  rangeFromThen _ _ = repeat MkProxy


text:
import Data.List
import Data.List1
import Data.String

import System.File

cost : Nat -> Nat
cost 0 = 0
cost n@(S k) = n + cost k

fuel : List Nat -> Nat -> Nat
fuel [] y = 0
fuel (x :: xs) y = (cost (if x > y then minus x y else minus y x)) + fuel xs y

upTo : Nat -> List Nat
upTo 0 = 0 :: []
upTo (S k) = S k :: upTo k

run : String -> IO ()
run s = do let l = catMaybes $ parsePositive {a=Nat} <$> (forget $ split (== ',') s)
           Just u <- pure $ head' $ reverse $ (\(c ::: _) => c) <$> (group $ sort $ l)
             | Nothing => putStrLn "no upper bound"
           let fs = head' $ sort $ fuel l <$> (upTo u)
           putStrLn $ show fs

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


text:
module Salo.Language.AST

import Salo.Language.TT

public export
data Body : Type where
  Postulate : Body

public export
record Definition where
  constructor MkDef
  binding : Binding Z
  body : Body

public export
implementation Show Body where
  show Postulate = "Postulate"

public export
implementation Show Definition where
  show x = "Binding: " ++ show x.binding
        ++ " Body: "    ++ show x.body

max_stars_repo_name: semissioncontrol/semcos

max_issues_repo_name: semissioncontrol/semcos

max_forks_repo_name: semissioncontrol/semcos


text:
{-
(1, 1)
System.Collections.Generic.HashSet`1[System.Tuple`2[System.Int32,System.Int32]]
True
False
True
False
-}

import CIL.FFI

TupleTy : CILTy
TupleTy = corlibTy "System.Tuple"

IntTupleTy : CILTy
IntTupleTy = CILTyGen TupleTy [CILTyInt32, CILTyInt32]

IntTuple : Type
IntTuple = CIL IntTupleTy

IsA Object IntTuple where {}

CreateIntTuple : Int -> Int -> CIL_IO IntTuple
CreateIntTuple =
  invoke (CILCall (CILGenMethod CCCStatic TupleTy "Create" [CILTyInt32, CILTyInt32]
                                [CILTyGenMethodParam "0", CILTyGenMethodParam "1"]
                                (CILTyGen TupleTy [CILTyGenMethodParam "0", CILTyGenMethodParam "1"])))
         (Int -> Int -> CIL_IO IntTuple)

systemCollectionsTy : String -> CILTy
systemCollectionsTy = CILTyRef "System.Collections"

HashSetTy : CILTy
HashSetTy = systemCollectionsTy "System.Collections.Generic.HashSet"

IntTupleHashSet : Type
IntTupleHashSet = CIL (CILTyGen HashSetTy [IntTupleTy])

IsA Object IntTupleHashSet where {}

Add : IntTupleHashSet -> IntTuple -> CIL_IO Bool
Add =
  invoke (CILInstanceCustom "Add" [CILTyGenParam "0"] CILTyBool)
         (IntTupleHashSet -> IntTuple -> CIL_IO Bool)

Contains : IntTupleHashSet -> IntTuple -> CIL_IO Bool
Contains =
  invoke (CILInstanceCustom "Contains" [CILTyGenParam "0"] CILTyBool)
         (IntTupleHashSet -> IntTuple -> CIL_IO Bool)

AssemblyReferences : CIL_IO ()
AssemblyReferences =
  assemblyRef "System.Collections" "4.0.10.0" "B0 3F 5F 7F 11 D5 0A 3A"

main : CIL_IO ()
main = do
  AssemblyReferences
  CreateIntTuple 1 1 >>= ToString >>= putStrLn
  set <- new (CIL_IO IntTupleHashSet)
  ToString set >>= putStrLn
  CreateIntTuple 1 1 >>= Add set >>= printLn
  CreateIntTuple 1 1 >>= Add set >>= printLn
  CreateIntTuple 1 1 >>= Contains set >>= printLn
  CreateIntTuple 1 2 >>= Contains set >>= printLn

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

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
-- Idris2

import System
import System.Concurrency

-- Test `conditionSignal` works for 1 main and 1 child thread

main : IO ()
main =
  do cvMutex <- makeMutex
     cv <- makeCondition
     t <- fork $ do mutexAcquire cvMutex
                    conditionWait cv cvMutex
                    putStrLn "Hello mother"
                    mutexRelease cvMutex
     putStrLn "Hello child"
     sleep 1
     conditionSignal cv
     threadWait t


text:
module OCaml.IO

%default total
%access public export

--------- The OCaml FFI

data OCamlRaw : Type -> Type where
  MkOCamlRaw : (x:t) -> OCamlRaw t
%used MkOCamlRaw x

data Module : List (String, Type) -> Type

val : String -> Type -> (String, Type)
val s t = (s,t)

data Abstr1 : Type -> Type

mutual
  data OCaml_IntTypes  : Type -> Type where
       OCaml_IntChar   : OCaml_IntTypes Char
       OCaml_IntNative : OCaml_IntTypes Int
       OCaml_IntBits32 : OCaml_IntTypes Bits32
       OCaml_IntBits64 : OCaml_IntTypes Bits64

  data OCaml_FnTypes : Type -> Type where
       OCaml_Fn     : OCaml_Types s -> OCaml_FnTypes t -> OCaml_FnTypes (s -> t)
       OCaml_FnIO   : OCaml_Types s -> OCaml_Types t -> OCaml_FnTypes (s -> IO' l t)
       OCaml_FnBase : OCaml_Types s -> OCaml_Types t -> OCaml_FnTypes (s -> t)

  data OCamlTypeList : List (String, Type) -> Type where
       Done : OCamlTypeList []
       Next : OCaml_Types a -> OCamlTypeList tys -> OCamlTypeList ((l, a) :: tys)

  data OCaml_Types : Type -> Type where
       OCaml_Str   : OCaml_Types String
       OCaml_Float : OCaml_Types Double
       OCaml_Bool  : OCaml_Types Bool
       OCaml_Abstr1: OCaml_Types (Abstr1 a)
       OCaml_Ptr   : OCaml_Types Ptr
       OCaml_Unit  : OCaml_Types ()
       OCaml_Any   : OCaml_Types (OCamlRaw a)
       OCaml_FnT   : OCaml_FnTypes a -> OCaml_Types a
       OCaml_Pair  : OCaml_Types a -> OCaml_Types b -> OCaml_Types (a, b)
       OCaml_List  : OCaml_Types a -> OCaml_Types (List a)
       OCaml_Maybe : OCaml_Types a -> OCaml_Types (Maybe a)
       OCaml_IntT  : OCaml_IntTypes i -> OCaml_Types i
       OCaml_Mod   : OCamlTypeList tys -> OCaml_Types (Module tys)

%error_reverse
FFI_OCaml : FFI
FFI_OCaml = MkFFI OCaml_Types String String

%error_reverse
OCaml_IO : Type -> Type
OCaml_IO = IO' FFI_OCaml

mutual
  -- Translates an OCaml-conventions function to an Idris-conventions
  -- one by inserting an additional dummy 'world' argument.
  --%inline
  fromOCamlFn : OCaml_FnTypes a -> a -> a
  fromOCamlFn (OCaml_Fn s t)     f = \x => fromOCamlFn t (f (toOCaml s x))
  fromOCamlFn (OCaml_FnIO s t)   f = \x => pure (fromOCaml t (believe_me (f (toOCaml s x))))
  fromOCamlFn (OCaml_FnBase s t) f = \x => fromOCaml t (f (toOCaml s x))

  -- %inline
  fromOCaml : OCaml_Types a -> a -> a
  fromOCaml OCaml_Str        s = s
  fromOCaml OCaml_Float      f = f
  fromOCaml OCaml_Bool       b = b
  fromOCaml OCaml_Ptr        p = p
  fromOCaml OCaml_Abstr1     x = x
  fromOCaml OCaml_Unit       u = u
  fromOCaml OCaml_Any        a = a
  fromOCaml (OCaml_FnT t)    f = fromOCamlFn t f
  fromOCaml (OCaml_Pair s t) p = (fromOCaml s (fst p), fromOCaml t (snd p))
  fromOCaml (OCaml_List s)   l = map (fromOCaml s) l
  fromOCaml (OCaml_Maybe s)  m = map (fromOCaml s) m
  fromOCaml (OCaml_IntT _)   i = i
  fromOCaml (OCaml_Mod ts)   m = m

  --%inline
  toOCamlFn : OCaml_FnTypes a -> a -> a
  toOCamlFn (OCaml_Fn s t)     f = \x => toOCamlFn t (f (fromOCaml s x))
  toOCamlFn (OCaml_FnIO s t)   f = \x => believe_me (toOCaml t (unsafePerformIO (f (fromOCaml s x))))
  toOCamlFn (OCaml_FnBase s t) f = \x => toOCaml t (f (fromOCaml s x))

  -- %inline
  toOCaml : OCaml_Types a -> a -> a
  toOCaml OCaml_Str        s = s
  toOCaml OCaml_Float      f = f
  toOCaml OCaml_Bool       b = b
  toOCaml OCaml_Ptr        p = p
  toOCaml OCaml_Abstr1     x = x
  toOCaml OCaml_Unit       u = u
  toOCaml OCaml_Any        a = a
  toOCaml (OCaml_FnT t)    f = toOCamlFn t f
  toOCaml (OCaml_Pair s t) p = (toOCaml s (fst p), toOCaml t (snd p))
  toOCaml (OCaml_List s)   l = map (toOCaml s) l
  toOCaml (OCaml_Maybe s)  m = map (toOCaml s) m
  toOCaml (OCaml_IntT _)   i = i
  toOCaml (OCaml_Mod ts)   m = m

%inline
fromOCamlFTy : FTy FFI_OCaml xs ty -> ty -> ty
fromOCamlFTy (FRet t)   f = do x <- f; pure (fromOCaml t x)
fromOCamlFTy (FFun s t) f = \x => fromOCamlFTy t (f (toOCaml s x))

%inline
ocamlCall : (fname : String) -> (ty : Type) ->
          {auto fty : FTy FFI_OCaml [] ty} -> ty
ocamlCall fname ty {fty} = fromOCamlFTy fty (foreign FFI_OCaml fname ty)

printLn : Show a => a -> OCaml_IO ()
printLn = printLn'

putStrLn : String -> OCaml_IO ()
putStrLn = putStrLn'

print : Show a => a -> OCaml_IO ()
print = print'

putStr : String -> OCaml_IO ()
putStr = putStr'

getLine : OCaml_IO String
getLine = getLine'

-- Some specific functions from the Stdlib module

print_endline : String -> OCaml_IO ()
print_endline s =
  ocamlCall "Stdlib.print_endline" (String -> OCaml_IO ()) s

-- Modules

data StrItem : String -> Type -> Type where
  Let : (s : String) -> t -> StrItem s t

data Values : List (String, Type) -> Type where
  Nil  : Values []
  (::) : StrItem s t -> Values tys -> Values ((s, t) :: tys)

assocIdx : String -> Int -> List (String, Type) -> Maybe (Int, Type)
assocIdx k i [] = Nothing
assocIdx k i ((k',t)::tys) = if k == k' then Just (i,t) else assocIdx k (i+1) tys

infixl 1 #

%inline
(#) : Module tys -> (nm : String) ->
      {auto ok : assocIdx nm 0 tys = Just (i, a)} ->
      {auto p : OCaml_Types a} ->
      {auto q : OCamlTypeList tys} ->
      a
(#) {tys} {a} {i} m nm = unsafePerformIO $
 ocamlCall "Idrisobj.field" (Module tys -> Int -> OCaml_IO a) m i

%inline
struct : Values tys -> {auto p : OCamlTypeList tys} -> Module tys
struct {tys} vs {p} = unsafePerformIO (go vs p 0) where
  %inline
  go : Values tys2 -> OCamlTypeList tys2 -> Int -> OCaml_IO (Module tys)
  go {tys2 = []} Nil Done n =
   ocamlCall "Idrisobj.new_block" (Int -> Int -> OCaml_IO (Module tys)) 0 n
  go {tys2 = (_, ty) :: tys2} (Let _ v :: vs) (Next t q) n = do
     m <- go vs q (n + 1)
     ocamlCall "Idrisobj.set_field" (Module tys -> Int -> ty -> OCaml_IO ()) m n v
     pure m

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
-- -------------------------------------------------------------- [ Common.idr ]
-- Module      : Crypto.Common
-- Description : Common definitions for crypto.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Crypto.Common

data Visibility = Private | Public
data Setting = Symm | Sign | Asymm

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

max_stars_repo_name: silky/idris-crypto-types

max_issues_repo_name: silky/idris-crypto-types

max_forks_repo_name: silky/idris-crypto-types


text:
module TAP

import System
import Data.Vect

%default total
%access private

{-
  TAP v13 Test Output Producer and Runner

-}

comment : String -> IO ()
comment s = putStrLn ("# " ++ s)

stamp : IO () -> IO ()
stamp rest = do t <- time
                comment ("t " ++ (show t))
                rest

printResult : String -> Bool -> IO ()
printResult n True = putStrLn ("ok " ++ n)
printResult n False = putStrLn ("not ok " ++ n)

runTests : Nat -> Vect n (Lazy (IO Bool)) -> IO ()
runTests k [] = pure ()
runTests k (x :: xs) = x >>= printResult (show k) >>= \_ => runTests (S k) xs

export
plan : (desc : String) -> Vect n (Lazy (IO Bool)) -> IO ()
plan desc tests {n} = do putStrLn "TAP version 13"
                         comment desc
                         putStrLn ("1.." ++ show n)
                         runTests 1 tests
                         stamp $ comment "done"

max_stars_repo_name: ostera/idris-coda

max_issues_repo_name: ostera/idris-coda

max_forks_repo_name: ostera/idris-coda


text:
module Collections.BSTree.Map.Quantifiers

import Collections.BSTree.Map.Core
import Collections.Util.Bnd
import Decidable.Order.Strict

||| A proof that a tree is non-empty.
public export
data NonEmpty : BST pre tot vTy mn mx -> Type where
  IsNode : {pre : StrictPreorder kTy sto} ->
           {tot : StrictOrdered kTy sto} ->
           {l : BST pre tot vTy mn (Mid k)} ->
           {r : BST pre tot vTy (Mid k) mx} ->
           NonEmpty (Node k v l r)

max_stars_repo_name: polendri/idris-collections

max_issues_repo_name: polendri/idris-collections

max_forks_repo_name: polendri/idris-collections


text:
||| Pretty printing compatible with this [grin](https://github.com/grin-compiler/grin).
module GRIN.PrettyCompatB

import Data.SortedMap
import Data.String.Builder

import GRIN.AST
import GRIN.Name

%default total

export
ShowB Var where
    showB (MkVar i) = "v" <+> showB @{FromShow} i

export
ShowB TagType where
    showB Con = "C"
    showB UThunk = "FU"
    showB NUThunk = "FNU"
    showB (Partial missing) = "P" <+> showB @{FromShow} missing

escapeChar : Char -> String
escapeChar = \case
    '"' => "\\\""
    '\\' => "\\\\"
    '\a' => "\\a"
    '\b' => "\\b"
    '\f' => "\\f"
    '\n' => "\\n"
    '\r' => "\\r"
    '\t' => "\\t"
    '\v' => "\\v"
    c => cast c

escapeString : String -> Builder
escapeString = fromString . fastConcat . map escapeChar . unpack

escapeBuilder : Builder -> Builder
escapeBuilder = mapString $ fastConcat . map escapeChar . unpack

export
Show name => ShowB (Tag name) where
    showB (MkTag tagType tag) = "C\"" <+> showB tagType <+> escapeString (show tag) <+> "\""

export
ShowB Lit where
    showB (LInt i) = showB @{FromShow} i
    showB (LDouble x) = showB @{FromShow} x
    showB (LString s) = "#\"" <+> escapeString s <+> "\""
    showB (LChar c) = "#'" <+> fromString (escapeChar c) <+> "'"

ShowB IntPrec where
    showB (Signed n) = "T_Int" <+> showB @{FromShow} n
    showB (Unsigned n) = "T_Word" <+> showB @{FromShow} n

export
ShowB SType where
    showB (IntTy prec) = showB prec
    showB DoubleTy = "T_Float"
    showB CharTy = "T_Char"
    showB StringTy = "T_String"
    showB UnitTy = "T_Unit"
    showB (HeapPtr i) = "T_Location" <+> showB @{FromShow} i

export
Show name => ShowB (GType name) where
    showB (SimpleType ty) = showB ty
    showB (TyVar x) = "%" <+> showB @{FromShow} x
    showB Cons = "Constructor"

export
Show name => ShowB (FuncType name) where
    showB (MkFuncType args ret) =
        foldMap (\arg => showB arg <+> " -> ") args <+> showB ret

export
ShowB SVal where
    showB (SVar v) = showB v
    showB (SLit l) = showB l

export
Show name => ShowB (Val name) where
    showB (SimpleVal val) = showB val
    showB (ConstTagNode tag args) = parens $ function tag args
    showB (ConstTag tag) = showB tag
    showB (VarTagNode tag args) = parens $ function tag args
    showB VUnit = "()"

export
Show name => ShowB (CasePat name) where
    showB (NodePat tag args) = parens $ function tag args
    showB (TagPat tag) = showB tag
    showB (LitPat lit) = showB lit
    showB DefaultPat = "#default"

mutual
    showBSExp : Show name => (indent : Nat) -> SExp name -> Builder
    showBSExp i (Do exp) = "do\n"
        <+> indent (1 + i) (assert_total $ showBExp (1 + i) exp)
    showBSExp _ (App f args) = function @{FromShow} f args
    showBSExp _ (Pure val) = "pure " <+> showB val
    showBSExp _ (Store val) = "store " <+> showB val
    showBSExp _ (Fetch _ var) = "fetch " <+> showB var
    showBSExp _ (FetchI _ i var) =
        "fetch " <+> showB var <+> bracket (showB @{FromShow} i)
    showBSExp _ (Update var val) =
        "update " <+> showB var <+> " " <+> showB val

    showBExp : Show name => (indent : Nat) -> Exp name -> Builder
    showBExp i (SimpleExp exp) = showBSExp i exp
    showBExp i (Bind VUnit rhs rest) =
        showBSExp i rhs <+> "\n"
        <+> indent i (showBExp i rest)
    showBExp i (Bind val rhs rest) =
        showB val <+> " <- " <+> showBSExp i rhs <+> "\n"
        <+> indent i (showBExp i rest)
    showBExp i (Case val alts) =
        "case " <+> showB val <+> " of"
        <+> foldMap (\alt => "\n"
            <+> indent (1 + i) (assert_total $ showBAlt (i + 1) alt))
            alts

    showBAlt : Show name => (indent : Nat) -> Alt name -> Builder
    showBAlt i (MkAlt pat exp) =
        showB pat <+> " ->\n"
        <+> indent (i + 1) (showBExp (i + 1) exp)

export
Show name => ShowB (SExp name) where
    showB = showBSExp 0

export
Show name => ShowB (Exp name) where
    showB = showBExp 0

export
Show name => ShowB (Alt name) where
    showB = showBAlt 0

export
Show name => ShowB (Def name) where
    showB (MkDef fn args exp _) = function @{FromShow} fn args <+> " =\n" <+> indent 1 (showBExp 1 exp)

record Externs name where
    constructor MkExterns
    primopPure : List (Extern name)
    primopEffectful : List (Extern name)
    ffiPure : List (Extern name)
    ffiEffectful : List (Extern name)

initExterns : Externs name
initExterns = MkExterns [] [] [] []

collectExts : Foldable t => t (Extern name) -> Externs name
collectExts = foldl addExtern initExterns
  where
    addExtern : Externs name -> Extern name -> Externs name
    addExtern exts ext = case ext.prim of
        Primop => case ext.eff of
            NoEffect => record { primopPure $= (ext ::) } exts
            Effect => record { primopEffectful $= (ext ::) } exts
        FFI => case ext.eff of
            NoEffect => record { ffiPure $= (ext ::) } exts
            Effect => record { ffiEffectful $= (ext ::) } exts

whenCons : List a -> Lazy Builder -> Builder
whenCons [] _ = ""
whenCons xs s = s

Show name => ShowB (Extern name) where
    showB ext = indent 1 $ showB @{FromShow} ext.extName <+> " :: " <+> showB ext.type

export
Foldable t => Show name => ShowB (t (Extern name)) where
    showB exts0 =
        let exts = collectExts exts0
         in whenCons exts.primopPure ("primop pure"
            <+> nl1Sep exts.primopPure)
            <+> whenCons exts.primopEffectful ("primop effectful"
            <+> nl1Sep exts.primopEffectful)
            <+> whenCons exts.ffiPure ("ffi pure"
            <+> nl1Sep exts.ffiPure)
            <+> whenCons exts.ffiEffectful ("ffi effectful"
            <+> nl1Sep exts.ffiEffectful)

export
Show name => ShowB (Prog name) where
    showB (MkProg exts defs _) =
        showB exts
        <+> "\n"
        <+> nlSep (values defs)


text:
module Main

import System
import System.Concurrency

main : IO ()
main = do
    barrier <- makeBarrier 3
    threadIDs <- for [1,2,3] $ \n => fork $ do
        putStrLn "Hello"
        barrierWait barrier
        putStrLn "Goodbye"
    for threadIDs $ \threadID =>
        threadWait threadID
    sleep 1


text:
module Bools

import Control.ST
import Control.ST.Exception
import DataTypes
import Util
import Ratio
import Lists
import Numbers
import Strings
import Vector
import Data.Complex

%access public export

isBoolean : PrimitiveLispFunc
isBoolean [LispBool _] = pure $ LispBool True
isBoolean _ = pure $ LispBool False

or : PrimitiveLispFunc
or [] = pure $ LispBool False
or [x] = pure x
or (LispBool x::xs) =
    case x of
        True => pure $ LispBool True
        False => or xs
or (x::xs) = pure x

and : PrimitiveLispFunc
and [] = pure $ LispBool True
and [x] = pure x
and (LispBool x::xs) =
    case x of
        True => and xs
        False => pure $ LispBool False
and (x::xs) = and xs

not : PrimitiveLispFunc
not [LispBool False] = pure $ LispBool True
not [_] = pure $ LispBool False
not args = Left $ NumArgs (MinMax 1 1) (cast $ length args) args

boolPrimitives : List (String, PrimitiveLispFunc)
boolPrimitives =
  [ ("boolean?", isBoolean)
  , ("and", and)
  , ("or", or)
  , ("not", not)
  ]

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
-- module Main

data N = Zero | Suc N

addOne : N -> N
addOne Zero = Suc Zero
addOne (Suc n) = Suc (Suc n)

One : N
One = Suc Zero
Two : N
Two = (Suc (Suc Zero))
Three : N
Three = addOne Two
Four : N
Four = addOne Three
Five : N
Five = addOne Four

add : N -> N -> N
add Zero s = s
add (Suc a) b = add a (Suc b)

data Vec : (a : Type) -> N -> Type where
  Nil : Vec a Zero
  Cons : a -> Vec a n -> Vec a (Suc n)

empt : Vec N Zero
empt = Nil

test : Vec N Two
test = Cons One (Cons Two Nil)

test2 : Vec N Three
test2 = Cons Three (Cons Four (Cons Five Nil))

cc :  Vec g a -> Vec g b -> Vec g (add a b)
cc Nil rest = rest
cc (Cons a rest) b = cc rest (Cons a b)

t3 : Vec N (addOne (addOne (addOne (addOne One))))
t3 = cc test test2

max_stars_repo_name: karljakoblarsson/IdrisToAgda

max_issues_repo_name: karljakoblarsson/IdrisToAgda

max_forks_repo_name: karljakoblarsson/IdrisToAgda


text:
import Data.Vect

test : Vect 2 () -> IO ()
test b =
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  let i = index 1 b in
  pure ()

main : IO ()
main = do
  pure ()


text:
module Idris.Codegen.ExtSTG.Prelude

namespace FilePath
  export
  FilePath : Type
  FilePath = String

  export
  getFilePath : FilePath -> String
  getFilePath = id

  export
  mkFilePath : String -> FilePath
  mkFilePath = id

public export
interface SemiDecEq t where
  semiDecEq : (x : t) -> (y : t) -> Maybe (x = y)

export
SemiDecEq Nat where
  semiDecEq Z      Z      = Just Refl
  semiDecEq (S n1) (S n2) = do
    Refl <- semiDecEq n1 n2
    Just Refl
  semiDecEq _      _      = Nothing

export
SemiDecEq a => SemiDecEq (List a) where
  semiDecEq []        []        = Just Refl
  semiDecEq (x :: xs) (y :: ys) = do
    Refl <- semiDecEq x y
    Refl <- semiDecEq xs ys
    Just Refl
  semiDecEq _ _ = Nothing

public export
numberFrom : Nat -> List a -> List (Nat, a)
numberFrom n xs = go xs n [] where
  go : List a -> Nat -> List (Nat, a) -> List (Nat, a)
  go [] k ys = ys
  go (x :: xs) k ys = (k, x) :: go xs (S k) ys

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module A.C

import A.B