text:
module Data.Time.Calendar.WeekDate

import Data.Vect
import Data.Fin

import Data.Time.Calendar.Types
import Data.Time.Calendar.Days
import Data.Time.Calendar.OrdinalDate

%default total

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

public export
data DayOfWeek = Sunday | Monday | Tuesday | Wednesday | Thursday | Friday | Saturday

export
dayOfWeeks : Vect 7 DayOfWeek
dayOfWeeks = [Sunday, Monday, Tuesday, Wednesday, Thursday, Friday, Saturday]

public export Cast (Fin 7) DayOfWeek where cast x = index x dayOfWeeks
public export
Num a => Cast DayOfWeek a where
  cast Sunday = 0
  cast Monday = 1
  cast Tuesday = 2
  cast Wednesday = 3
  cast Thursday = 4
  cast Friday = 5
  cast Saturday = 6

public export
Cast DayOfWeek (Fin 7) where
  cast Sunday = 0
  cast Monday = 1
  cast Tuesday = 2
  cast Wednesday = 3
  cast Thursday = 4
  cast Friday = 5
  cast Saturday = 6

public export
Eq DayOfWeek where
  Monday == Monday = True
  Tuesday == Tuesday = True
  Wednesday == Wednesday = True
  Thursday == Thursday = True
  Friday == Friday = True
  Saturday == Saturday = True
  Sunday == Sunday = True
  _ == _ = False

public export
Ord DayOfWeek where
  compare x y = compare (cast {to=Fin 7} x) (cast y)

public export
Show DayOfWeek where
  show Monday = "Monday"
  show Tuesday = "Tuesday"
  show Wednesday = "Wednesday"
  show Thursday = "Thursday"
  show Friday = "Friday"
  show Saturday = "Saturday"
  show Sunday = "Sunday"

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

export
dayOfWeek : Day -> DayOfWeek
dayOfWeek d = cast $ restrict 6 $ d.modifiedJulianDay + 3

||| @dayOfWeekDiff a b = a - b@ in range 0 to 6.
||| The number of days from b to the next a.
export
dayOfWeekDiff : DayOfWeek -> DayOfWeek -> Int
dayOfWeekDiff a b = (the Int (cast a) - cast b) `mod` 7

||| The first day-of-week on or after some day
firstDayOfWeekOnAfter : DayOfWeek -> Day -> Day
firstDayOfWeekOnAfter dw d = addDays (cast $ dayOfWeekDiff dw $ dayOfWeek d) d

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

public export data FirstWeekType
  = FirstWholeWeek   -- first week is the first whole week of the year
  | FirstMostWeek    -- first week is the first week with four days in the year

public export
Eq FirstWeekType where
  FirstWholeWeek == FirstWholeWeek = True
  FirstMostWeek == FirstMostWeek = True
  _ == _ = False

export firstDayOfWeekCalendar : FirstWeekType -> DayOfWeek -> Year -> Day
firstDayOfWeekCalendar wt dow year = let
  jan1st = fromOrdinalDate year 1
  in case wt of
          FirstWholeWeek => firstDayOfWeekOnAfter dow jan1st
          FirstMostWeek  => firstDayOfWeekOnAfter dow $ addDays (-3) jan1st

-- | Convert to the given kind of "week calendar".
-- Note that the year number matches the weeks, and so is not always the same as the Gregorian year number.
export
toWeekCalendar : FirstWeekType -- ^ how to reckon the first week of the year
              -> DayOfWeek     -- ^ the first day of each week
              -> Day
              -> (Year, WeekOfYear, DayOfWeek)
toWeekCalendar wt ws d = let
  dw      = dayOfWeek d
  (y0, _) = toOrdinalDate d
  j1p     = firstDayOfWeekCalendar wt ws $ y0 - 1
  j1      = firstDayOfWeekCalendar wt ws y0
  j1s     = firstDayOfWeekCalendar wt ws $ y0 + 1
  in if d < j1
        then (y0 - 1, (cast $ diffDays d j1p) `div` 7 + 1, dw)
        else if d < j1s then (y0, (cast $ diffDays d j1) `div` 7 + 1, dw)
        else (y0 + 1, (cast $ diffDays d j1s) `div` 7 + 1, dw)

                                                                                -- | Convert from the given kind of "week calendar".
-- Invalid week and day values will be clipped to the correct range.
export
fromWeekCalendar : FirstWeekType -- ^ how to reckon the first week of the year
                -> DayOfWeek -- ^ the first day of each week
                -> Year -> WeekOfYear -> DayOfWeek -> Day
fromWeekCalendar wt ws y wy dw = let
  d1 = firstDayOfWeekCalendar wt ws y
  wy' = max 1 $ min 53 wy
  d1s = firstDayOfWeekCalendar wt ws $ y + 1
  getday : WeekOfYear -> Day
  getday wy'' = addDays (cast $ ((wy'' - 1) * 7) + (dayOfWeekDiff dw ws)) d1
  day : Day
  day = getday wy'
  in if wy' == 53 && day >= d1s then getday 52 else day

||| Convert from the given kind of "week calendar".
||| Invalid week and day values will return Nothing.
export
fromWeekCalendarValid : FirstWeekType -- ^ how to reckon the first week of the year
                     -> DayOfWeek -- ^ the first day of each week
                     -> Year -> WeekOfYear -> DayOfWeek -> Maybe Day
fromWeekCalendarValid wt ws y wy dw = let
  d = fromWeekCalendar wt ws y wy dw
  in if toWeekCalendar wt ws d == (y,wy,dw) then Just d else Nothing

||| Convert to ISO 8601 Week Date format. First element of result is year, second week number (1-53), third day of week (1 for Monday to 7 for Sunday).
|||  Note that \"Week\" years are not quite the same as Gregorian years, as the first day of the year is always a Monday.
||| The first week of a year is the first week to contain at least four days in the corresponding Gregorian year.
export toWeekDate : Day -> (Year, WeekOfYear, Int)
toWeekDate d = let
  (y, wy, dw) = toWeekCalendar FirstMostWeek Monday d
  in (y, wy, cast dw)

||| Convert from ISO 8601 Week Date format. First argument is year, second week number (1-52 or 53), third day of week (1 for Monday to 7 for Sunday).
||| Invalid week and day values will be clipped to the correct range.
export fromWeekDate : Year -> WeekOfYear -> Int -> Day
fromWeekDate y wy dw =
   fromWeekCalendar FirstMostWeek Monday y wy (cast $ restrict 6 $ cast $ max 1 $ min 7 dw)

{-
||| Bidirectional abstract constructor for ISO 8601 Week Date format.
||| Invalid week values will be clipped to the correct range.
pattern YearWeekDay : Year -> WeekOfYear -> DayOfWeek -> Day
pattern YearWeekDay y wy dw <- (toWeekDate -> (y,wy,toEnum -> dw)) where
  YearWeekDay y wy dw = fromWeekDate y wy (fromEnum dw)
-}

||| Convert from ISO 8601 Week Date format. First argument is year, second week number (1-52 or 53), third day of week (1 for Monday to 7 for Sunday).
||| Invalid week and day values will return Nothing.
export fromWeekDateValid : Year -> WeekOfYear -> Int -> Maybe Day
fromWeekDateValid y wy dw =
  if dw < 1 || dw > 7
  then Nothing
  else fromWeekCalendarValid FirstMostWeek Monday y wy (cast $ restrict 6 $ cast dw)

{-
-- | Show in ISO 8601 Week Date format as yyyy-Www-d (e.g. \"2006-W46-3\").
showWeekDate : Day -> String
showWeekDate date = (show4 y) ++ "-W" ++ (show2 w) ++ "-" ++ (show d)
  where (y, w, d) = toWeekDate date
-}

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


text:
module Flexidisc.OrdList.Label

import Flexidisc.OrdList.Type

%default total
%access public export

||| Proof that a label is in an `OrdList`
data OrdLabel : (l : k) -> (xs : OrdList k o v) -> Type where
  ||| The label is in the first element of the list
  Here : OrdLabel l ((l,v)::xs)
  ||| The label is in the tail
  There : (later : OrdLabel l xs) -> OrdLabel l (x::xs)

%name OrdLabel lbl, loc, prf, e, elem

||| Given a proof that a label is in the list, get the corresponding value back
atLabel : (xs : OrdList k o v) -> (loc : OrdLabel l xs) -> v
atLabel ((_, v) :: _) Here = v
atLabel (_ :: xs) (There later) = atLabel xs later

Uninhabited (OrdLabel k []) where
  uninhabited Here      impossible
  uninhabited (There _) impossible

||| Decide whether a label is in a list or not
decLabel : DecEq k => (l : k) -> (xs : OrdList k o v) -> Dec (OrdLabel l xs)
decLabel l [] = No uninhabited
decLabel l ((kx, vx) :: xs) with (decEq l kx)
  | (Yes prf) = Yes (rewrite prf in Here)
  | (No contraHere) with (decLabel l xs)
    | (Yes prf) = Yes (There prf)
    | (No contraThere) = No (\p => case p of
                                        Here => contraHere Refl
                                        There later => contraThere later)

||| Given a proof that an element is in a vector, remove it
dropLabel : (xs : OrdList k o v) -> (loc : OrdLabel l xs) -> OrdList k o v
dropLabel (_ :: xs) Here          = xs
dropLabel (x :: xs) (There later) = x :: dropLabel xs later

||| Update a value in the list given it's location and a new value
changeValue : (xs : OrdList k o v) -> (loc : OrdLabel l xs) ->
             (new : v) -> OrdList k o v
changeValue ((x, old) :: xs) Here          new = (x, new) :: xs
changeValue (x :: xs)        (There later) new = x :: changeValue xs later new

ext: idr

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Symmetry.Abelian

import Specifications.TranslationInvariance

%default total
%access export

abelianTranslationInvariantLR : isAbelian op ->
  isTranslationInvariantL op rel ->
  isTranslationInvariantR op rel
abelianTranslationInvariantLR abel left x y a given =
  rewrite abel x a in
  rewrite abel y a in
  left x y a given

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Main

import IdrisScript
import IdrisScript.Arrays

main : JS_IO ()
main = do
  arr <- toJSArray {from=Int} {to=JSNumber} [1..100]
  forEach (\elm => log (getProof !(pack elm))) arr

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module Control.Optics.Review

import Control.Monad.Identity
import Data.Profunctor.Morphism
import public Control.Optics.Getter

export
(#) : AReview t b -> b -> t
(#) p = runIdentity . untag . p . MkTagged . Id

export
re : AReview t b -> Getter b t
re p = to (\x => p # x)


text:
module TransitivityOfDivisibility

data Divb : Nat -> Nat -> Type where
  DivbAx1 : a = k*b -> a `Divb` b

lemma1 : a `Divb` b*c -> a `Divb` c
lemma1 {a=a}{b=b}{c=c} (DivbAx1{k=k} aEqKBC) =
  let aEqKBC' = trans aEqKBC $ multAssociative k b c
  in DivbAx1 aEqKBC'

theorem : a `Divb` b -> b `Divb` c -> a `Divb` c
theorem aDivbB (DivbAx1{k=kb} bEqKbC) =
  let aDivbB' = replace bEqKbC aDivbB
  in lemma1 aDivbB'

max_stars_repo_name: GoPavel/idris-proof

max_issues_repo_name: GoPavel/idris-proof

max_forks_repo_name: GoPavel/idris-proof


text:
module Main

import IdrisScript
import IdrisScript.Date

main : JS_IO ()
main = do
  date <- now
  log date
  date `setFullYear` (MkYear 2016)
  log date


text:
data Natural : Type where
    S : Natural -> Natural
    Z : Natural

%builtin Natural Natural

plus : Natural -> Natural -> Natural
plus Z y = y
plus (S x) y = S (plus x y)

main : IO Natural
main = pure $ plus (S Z) (S $ S Z)


text:
module Vimscript.List

import Vimscript.FFI

%default total

export
data VimList a = MkList (Raw a)

%inline
unRaw : Raw a -> a
unRaw (MkRaw a) = a

%inline
public export
empty : VimList a
empty {a} =
  unsafePerformIO $ do
    MkRaw l <- foreign FFI_VIM VIM_ListEmpty (VIM_IO (Raw (VimList a)))
    pure l

%inline
unsafeIndex : Int -> VimList a -> a
unsafeIndex {a} i l =
  unsafePerformIO $ do
    MkRaw a <- foreign FFI_VIM VIM_ListIndex (Int -> Raw (VimList a) -> VIM_IO (Raw a)) i (MkRaw l)
    pure a

%inline
public export
length : VimList a -> Nat
length {a} l =
  unsafePerformIO $ do
    n <- foreign FFI_VIM (VIM_BuiltIn "len") (Raw (VimList a) -> VIM_IO Int) (MkRaw l)
    pure (fromInteger (cast n))

%inline
public export
concat : VimList a -> VimList a -> VimList a
concat {a} l1 l2 =
  unsafePerformIO $ do
    MkRaw l3 <-
      foreign
      FFI_VIM
      VIM_ListConcat
      (Raw (VimList a) -> Raw (VimList a) -> VIM_IO (Raw (VimList a)))
      (MkRaw l1)
      (MkRaw l2)
    pure l3

%inline
public export
cons : (x : a) -> VimList a -> VimList a
cons {a} x l1 =
  unsafePerformIO $ do
    MkRaw l2 <-
      foreign
      FFI_VIM
      VIM_ListCons
      (Raw a -> Raw (VimList a) -> VIM_IO (Raw (VimList a)))
      (MkRaw x)
      (MkRaw l1)
    pure l2

%inline
public export
head : VimList a -> Maybe a
head {a} l1 =
  case length l1 of
    Z => Nothing
    S _ => Just (unsafeIndex 0 l1)

%inline
public export
snoc : VimList a -> (x : a) -> VimList a
snoc {a} l1 x =
  unsafePerformIO $ do
    MkRaw l2 <-
      foreign
      FFI_VIM
      VIM_ListSnoc
      (Raw (VimList a) -> Raw a -> VIM_IO (Raw (VimList a)))
      (MkRaw l1)
      (MkRaw x)
    pure l2

%inline
public export
fromFoldable : (Foldable f) => f a -> VimList a
fromFoldable = foldl snoc empty

max_stars_repo_name: owickstrom/idris-vimscript

max_issues_repo_name: owickstrom/idris-vimscript

max_forks_repo_name: owickstrom/idris-vimscript


text:
module Shaped

import Data.Vect
import Data.So

%default total

mkRank : (len: Nat) -> (stride: Nat) -> Fin 3
mkRank len s = case len > s of
  True => the (Fin 3) 2
  False => if (len > 1) then the (Fin 3) 1 else the (Fin 3) 0

data Dim: (rows, stride, len: Nat) -> Type where
  MkDim: (rows, stride: Nat)
    -> {auto NZs : So (stride > 0)}
    -> {auto NZs : So (rows > 0)}
    -> Dim rows stride (rows * stride)

data Shape: (rank: Fin 3) -> Dim rows stride len -> Type where
  SomeScalar:
    Shape
      (mkRank 1 1)
      (MkDim 1 1)
  SomeVect:
    (stride: Nat)
    -> {auto NZs : So (stride > 0)}
    -> Shape
        (mkRank stride stride)
        (MkDim 1 stride)
  SomeMat:
    (rows, stride: Nat)
    -> {auto NZs : So (stride > 0)}
    -> {auto NZs : So (rows > 0)}
    -> Shape
        (mkRank (rows * stride) stride)
        (MkDim rows stride)

data Operation =
  Plus | Minus
  | Slash | Backslash
  | Equal

data Parallelism: Nat -> Nat -> Type where
  mkPar: (x: Nat) -> (y: Nat) -> Parallelism x y

record Phase where
  constructor MkPhase
  operation : Operation
  shape : Shape rank (MkDim (S rows) (S stride))
  par : Parallelism x y

-- shape (Reduce (SomeVect 4))
-- shape (Reduce (SomeMat 3 3))
-- shape (Sum (SomeVect 4) (shape (Reduce (SomeMat 3 3))))
-- shape (Sum SomeScalar (shape (Reduce (SomeVect 4))))
Reduce : Shape q (MkDim (S r) (S n)) -> Phase
Reduce {q=FZ} o = MkPhase Slash o (mkPar 0 0)
Reduce {q=FS(FZ)} {n} o = MkPhase Slash SomeScalar (mkPar (S n) 0)
Reduce {q=FS(FS(FZ))} {r} {n} o = MkPhase Slash (SomeVect (S n)) (mkPar ((S n)*(S r)) 0)

Scan : Shape p (MkDim (S r) (S n)) -> Phase
Scan {r} {n} o = MkPhase Backslash o (mkPar ((S n)*(S r)) 0)

-- scalarToVect (MkScalar 1) (MkVect [1,2,3,4])
-- [Plus, Minus, Slash]
-- shape (Sum SomeScalar SomeScalar)
-- shape (Sum (SomeVect 4) (SomeVect 4))
-- shape (Sum (SomeMat 3 3) (SomeMat 3 3))
Sum : Shape p (MkDim (S r) (S n)) -> Shape p (MkDim (S r) (S n)) -> Phase
Sum {r} {n} a o = MkPhase Plus o (mkPar 0 ((S n)*(S r)))

-- shape (NSum SomeScalar (SomeVect 4))
-- shape (NSum SomeScalar (SomeMat 3 3))
NSum : Shape 0 (MkDim (S r) (S n)) -> Shape p (MkDim (S j) (S m)) -> Phase
NSum {j} {m} a o = MkPhase Plus (SomeMat (S j) (S m)) (mkPar 0 ((S j)*(S m)))

max_stars_repo_name: jhvst/shaped-array

max_issues_repo_name: jhvst/shaped-array

max_forks_repo_name: jhvst/shaped-array


text:
module Web.Internal.StreamsPrim

import JS
import Web.Internal.Types

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

namespace ByteLengthQueuingStrategy

  export
  %foreign "browser:lambda:(a)=> new ByteLengthQueuingStrategy(a)"
  prim__new : QueuingStrategyInit -> PrimIO ByteLengthQueuingStrategy

  export
  %foreign "browser:lambda:x=>x.highWaterMark"
  prim__highWaterMark : ByteLengthQueuingStrategy -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.size"
  prim__size : ByteLengthQueuingStrategy -> PrimIO Function

namespace CountQueuingStrategy

  export
  %foreign "browser:lambda:(a)=> new CountQueuingStrategy(a)"
  prim__new : QueuingStrategyInit -> PrimIO CountQueuingStrategy

  export
  %foreign "browser:lambda:x=>x.highWaterMark"
  prim__highWaterMark : CountQueuingStrategy -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.size"
  prim__size : CountQueuingStrategy -> PrimIO Function

namespace ReadableByteStreamController

  export
  %foreign "browser:lambda:x=>x.byobRequest"
  prim__byobRequest :  ReadableByteStreamController
                    -> PrimIO (Nullable ReadableStreamBYOBRequest)

  export
  %foreign "browser:lambda:x=>x.desiredSize"
  prim__desiredSize : ReadableByteStreamController -> PrimIO (Nullable Double)

  export
  %foreign "browser:lambda:x=>x.close()"
  prim__close : ReadableByteStreamController -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.enqueue(a)"
  prim__enqueue :  ReadableByteStreamController
                -> Union10 Int8Array
                           Int16Array
                           Int32Array
                           UInt8Array
                           UInt8Array
                           UInt8Array
                           UInt8ClampedArray
                           Float32Array
                           Float64Array
                           DataView
                -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.error(a)"
  prim__error : ReadableByteStreamController -> UndefOr AnyPtr -> PrimIO ()

namespace ReadableStream

  export
  %foreign "browser:lambda:(a,b)=> new ReadableStream(a,b)"
  prim__new : UndefOr Object -> UndefOr QueuingStrategy -> PrimIO ReadableStream

  export
  %foreign "browser:lambda:x=>x.locked"
  prim__locked : ReadableStream -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,a)=>x.cancel(a)"
  prim__cancel : ReadableStream -> UndefOr AnyPtr -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:(x,a)=>x.getReader(a)"
  prim__getReader :  ReadableStream
                  -> UndefOr ReadableStreamGetReaderOptions
                  -> PrimIO (Union2 ReadableStreamDefaultReader
                                    ReadableStreamBYOBReader)

  export
  %foreign "browser:lambda:(x,a,b)=>x.pipeThrough(a,b)"
  prim__pipeThrough :  ReadableStream
                    -> ReadableWritablePair
                    -> UndefOr StreamPipeOptions
                    -> PrimIO ReadableStream

  export
  %foreign "browser:lambda:(x,a,b)=>x.pipeTo(a,b)"
  prim__pipeTo :  ReadableStream
               -> WritableStream
               -> UndefOr StreamPipeOptions
               -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:x=>x.tee()"
  prim__tee : ReadableStream -> PrimIO (Array ReadableStream)

namespace ReadableStreamBYOBReader

  export
  %foreign "browser:lambda:(a)=> new ReadableStreamBYOBReader(a)"
  prim__new : ReadableStream -> PrimIO ReadableStreamBYOBReader

  export
  %foreign "browser:lambda:(x,a)=>x.read(a)"
  prim__read :  ReadableStreamBYOBReader
             -> Union10 Int8Array
                        Int16Array
                        Int32Array
                        UInt8Array
                        UInt8Array
                        UInt8Array
                        UInt8ClampedArray
                        Float32Array
                        Float64Array
                        DataView
             -> PrimIO (Promise ReadableStreamBYOBReadResult)

  export
  %foreign "browser:lambda:x=>x.releaseLock()"
  prim__releaseLock : ReadableStreamBYOBReader -> PrimIO ()

namespace ReadableStreamBYOBRequest

  export
  %foreign "browser:lambda:x=>x.view"
  prim__view :  ReadableStreamBYOBRequest
             -> PrimIO (Nullable (Union10 Int8Array
                                          Int16Array
                                          Int32Array
                                          UInt8Array
                                          UInt8Array
                                          UInt8Array
                                          UInt8ClampedArray
                                          Float32Array
                                          Float64Array
                                          DataView))

  export
  %foreign "browser:lambda:(x,a)=>x.respond(a)"
  prim__respond : ReadableStreamBYOBRequest -> JSBits64 -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.respondWithNewView(a)"
  prim__respondWithNewView :  ReadableStreamBYOBRequest
                           -> Union10 Int8Array
                                      Int16Array
                                      Int32Array
                                      UInt8Array
                                      UInt8Array
                                      UInt8Array
                                      UInt8ClampedArray
                                      Float32Array
                                      Float64Array
                                      DataView
                           -> PrimIO ()

namespace ReadableStreamDefaultController

  export
  %foreign "browser:lambda:x=>x.desiredSize"
  prim__desiredSize :  ReadableStreamDefaultController
                    -> PrimIO (Nullable Double)

  export
  %foreign "browser:lambda:x=>x.close()"
  prim__close : ReadableStreamDefaultController -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.enqueue(a)"
  prim__enqueue : ReadableStreamDefaultController -> UndefOr AnyPtr -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.error(a)"
  prim__error : ReadableStreamDefaultController -> UndefOr AnyPtr -> PrimIO ()

namespace ReadableStreamDefaultReader

  export
  %foreign "browser:lambda:(a)=> new ReadableStreamDefaultReader(a)"
  prim__new : ReadableStream -> PrimIO ReadableStreamDefaultReader

  export
  %foreign "browser:lambda:x=>x.read()"
  prim__read :  ReadableStreamDefaultReader
             -> PrimIO (Promise ReadableStreamDefaultReadResult)

  export
  %foreign "browser:lambda:x=>x.releaseLock()"
  prim__releaseLock : ReadableStreamDefaultReader -> PrimIO ()

namespace TransformStream

  export
  %foreign "browser:lambda:(a,b,c)=> new TransformStream(a,b,c)"
  prim__new :  UndefOr Object
            -> UndefOr QueuingStrategy
            -> UndefOr QueuingStrategy
            -> PrimIO TransformStream

  export
  %foreign "browser:lambda:x=>x.readable"
  prim__readable : TransformStream -> PrimIO ReadableStream

  export
  %foreign "browser:lambda:x=>x.writable"
  prim__writable : TransformStream -> PrimIO WritableStream

namespace TransformStreamDefaultController

  export
  %foreign "browser:lambda:x=>x.desiredSize"
  prim__desiredSize :  TransformStreamDefaultController
                    -> PrimIO (Nullable Double)

  export
  %foreign "browser:lambda:(x,a)=>x.enqueue(a)"
  prim__enqueue :  TransformStreamDefaultController
                -> UndefOr AnyPtr
                -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.error(a)"
  prim__error : TransformStreamDefaultController -> UndefOr AnyPtr -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.terminate()"
  prim__terminate : TransformStreamDefaultController -> PrimIO ()

namespace WritableStream

  export
  %foreign "browser:lambda:(a,b)=> new WritableStream(a,b)"
  prim__new : UndefOr Object -> UndefOr QueuingStrategy -> PrimIO WritableStream

  export
  %foreign "browser:lambda:x=>x.locked"
  prim__locked : WritableStream -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,a)=>x.abort(a)"
  prim__abort : WritableStream -> UndefOr AnyPtr -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:x=>x.close()"
  prim__close : WritableStream -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:x=>x.getWriter()"
  prim__getWriter : WritableStream -> PrimIO WritableStreamDefaultWriter

namespace WritableStreamDefaultController

  export
  %foreign "browser:lambda:(x,a)=>x.error(a)"
  prim__error : WritableStreamDefaultController -> UndefOr AnyPtr -> PrimIO ()

namespace WritableStreamDefaultWriter

  export
  %foreign "browser:lambda:(a)=> new WritableStreamDefaultWriter(a)"
  prim__new : WritableStream -> PrimIO WritableStreamDefaultWriter

  export
  %foreign "browser:lambda:x=>x.closed"
  prim__closed : WritableStreamDefaultWriter -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:x=>x.desiredSize"
  prim__desiredSize : WritableStreamDefaultWriter -> PrimIO (Nullable Double)

  export
  %foreign "browser:lambda:x=>x.ready"
  prim__ready : WritableStreamDefaultWriter -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:(x,a)=>x.abort(a)"
  prim__abort :  WritableStreamDefaultWriter
              -> UndefOr AnyPtr
              -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:x=>x.close()"
  prim__close : WritableStreamDefaultWriter -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:x=>x.releaseLock()"
  prim__releaseLock : WritableStreamDefaultWriter -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.write(a)"
  prim__write :  WritableStreamDefaultWriter
              -> UndefOr AnyPtr
              -> PrimIO (Promise Undefined)

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

namespace GenericTransformStream

  export
  %foreign "browser:lambda:x=>x.readable"
  prim__readable : GenericTransformStream -> PrimIO ReadableStream

  export
  %foreign "browser:lambda:x=>x.writable"
  prim__writable : GenericTransformStream -> PrimIO WritableStream

namespace ReadableStreamGenericReader

  export
  %foreign "browser:lambda:x=>x.closed"
  prim__closed : ReadableStreamGenericReader -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:(x,a)=>x.cancel(a)"
  prim__cancel :  ReadableStreamGenericReader
               -> UndefOr AnyPtr
               -> PrimIO (Promise Undefined)

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

namespace QueuingStrategy

  export
  %foreign "browser:lambda:(a,b)=> {highWaterMark: a,size: b}"
  prim__new :  UndefOr Double
            -> UndefOr QueuingStrategySize
            -> PrimIO QueuingStrategy

  export
  %foreign "browser:lambda:x=>x.highWaterMark"
  prim__highWaterMark : QueuingStrategy -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.highWaterMark = v}"
  prim__setHighWaterMark : QueuingStrategy -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.size"
  prim__size : QueuingStrategy -> PrimIO (UndefOr QueuingStrategySize)

  export
  %foreign "browser:lambda:(x,v)=>{x.size = v}"
  prim__setSize : QueuingStrategy -> UndefOr QueuingStrategySize -> PrimIO ()

namespace QueuingStrategyInit

  export
  %foreign "browser:lambda:(a)=> {highWaterMark: a}"
  prim__new : Double -> PrimIO QueuingStrategyInit

  export
  %foreign "browser:lambda:x=>x.highWaterMark"
  prim__highWaterMark : QueuingStrategyInit -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.highWaterMark = v}"
  prim__setHighWaterMark : QueuingStrategyInit -> Double -> PrimIO ()

namespace ReadableStreamBYOBReadResult

  export
  %foreign "browser:lambda:(a,b)=> {value: a,done: b}"
  prim__new :  UndefOr (Union10 Int8Array
                                Int16Array
                                Int32Array
                                UInt8Array
                                UInt8Array
                                UInt8Array
                                UInt8ClampedArray
                                Float32Array
                                Float64Array
                                DataView)
            -> UndefOr Boolean
            -> PrimIO ReadableStreamBYOBReadResult

  export
  %foreign "browser:lambda:x=>x.done"
  prim__done : ReadableStreamBYOBReadResult -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.done = v}"
  prim__setDone : ReadableStreamBYOBReadResult -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.value"
  prim__value :  ReadableStreamBYOBReadResult
              -> PrimIO (UndefOr (Union10 Int8Array
                                          Int16Array
                                          Int32Array
                                          UInt8Array
                                          UInt8Array
                                          UInt8Array
                                          UInt8ClampedArray
                                          Float32Array
                                          Float64Array
                                          DataView))

  export
  %foreign "browser:lambda:(x,v)=>{x.value = v}"
  prim__setValue :  ReadableStreamBYOBReadResult
                 -> UndefOr (Union10 Int8Array
                                     Int16Array
                                     Int32Array
                                     UInt8Array
                                     UInt8Array
                                     UInt8Array
                                     UInt8ClampedArray
                                     Float32Array
                                     Float64Array
                                     DataView)
                 -> PrimIO ()

namespace ReadableStreamDefaultReadResult

  export
  %foreign "browser:lambda:(a,b)=> {value: a,done: b}"
  prim__new :  UndefOr AnyPtr
            -> UndefOr Boolean
            -> PrimIO ReadableStreamDefaultReadResult

  export
  %foreign "browser:lambda:x=>x.done"
  prim__done : ReadableStreamDefaultReadResult -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.done = v}"
  prim__setDone :  ReadableStreamDefaultReadResult
                -> UndefOr Boolean
                -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.value"
  prim__value : ReadableStreamDefaultReadResult -> PrimIO (UndefOr AnyPtr)

  export
  %foreign "browser:lambda:(x,v)=>{x.value = v}"
  prim__setValue :  ReadableStreamDefaultReadResult
                 -> UndefOr AnyPtr
                 -> PrimIO ()

namespace ReadableStreamGetReaderOptions

  export
  %foreign "browser:lambda:(a)=> {mode: a}"
  prim__new : UndefOr String -> PrimIO ReadableStreamGetReaderOptions

  export
  %foreign "browser:lambda:x=>x.mode"
  prim__mode : ReadableStreamGetReaderOptions -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.mode = v}"
  prim__setMode : ReadableStreamGetReaderOptions -> UndefOr String -> PrimIO ()

namespace ReadableStreamIteratorOptions

  export
  %foreign "browser:lambda:(a)=> {preventCancel: a}"
  prim__new : UndefOr Boolean -> PrimIO ReadableStreamIteratorOptions

  export
  %foreign "browser:lambda:x=>x.preventCancel"
  prim__preventCancel :  ReadableStreamIteratorOptions
                      -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.preventCancel = v}"
  prim__setPreventCancel :  ReadableStreamIteratorOptions
                         -> UndefOr Boolean
                         -> PrimIO ()

namespace ReadableWritablePair

  export
  %foreign "browser:lambda:(a,b)=> {readable: a,writable: b}"
  prim__new : ReadableStream -> WritableStream -> PrimIO ReadableWritablePair

  export
  %foreign "browser:lambda:x=>x.readable"
  prim__readable : ReadableWritablePair -> PrimIO ReadableStream

  export
  %foreign "browser:lambda:(x,v)=>{x.readable = v}"
  prim__setReadable : ReadableWritablePair -> ReadableStream -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.writable"
  prim__writable : ReadableWritablePair -> PrimIO WritableStream

  export
  %foreign "browser:lambda:(x,v)=>{x.writable = v}"
  prim__setWritable : ReadableWritablePair -> WritableStream -> PrimIO ()

namespace StreamPipeOptions

  export
  %foreign "browser:lambda:(a,b,c,d)=> {preventClose: a,preventAbort: b,preventCancel: c,signal: d}"
  prim__new :  UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr AbortSignal
            -> PrimIO StreamPipeOptions

  export
  %foreign "browser:lambda:x=>x.preventAbort"
  prim__preventAbort : StreamPipeOptions -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.preventAbort = v}"
  prim__setPreventAbort : StreamPipeOptions -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.preventCancel"
  prim__preventCancel : StreamPipeOptions -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.preventCancel = v}"
  prim__setPreventCancel : StreamPipeOptions -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.preventClose"
  prim__preventClose : StreamPipeOptions -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.preventClose = v}"
  prim__setPreventClose : StreamPipeOptions -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.signal"
  prim__signal : StreamPipeOptions -> PrimIO (UndefOr AbortSignal)

  export
  %foreign "browser:lambda:(x,v)=>{x.signal = v}"
  prim__setSignal : StreamPipeOptions -> UndefOr AbortSignal -> PrimIO ()

namespace Transformer

  export
  %foreign "browser:lambda:(a,b,c,d,e)=> {start: a,transform: b,flush: c,readableType: d,writableType: e}"
  prim__new :  UndefOr TransformerStartCallback
            -> UndefOr TransformerTransformCallback
            -> UndefOr TransformerFlushCallback
            -> UndefOr AnyPtr
            -> UndefOr AnyPtr
            -> PrimIO Transformer

  export
  %foreign "browser:lambda:x=>x.flush"
  prim__flush : Transformer -> PrimIO (UndefOr TransformerFlushCallback)

  export
  %foreign "browser:lambda:(x,v)=>{x.flush = v}"
  prim__setFlush : Transformer -> UndefOr TransformerFlushCallback -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.readableType"
  prim__readableType : Transformer -> PrimIO (UndefOr AnyPtr)

  export
  %foreign "browser:lambda:(x,v)=>{x.readableType = v}"
  prim__setReadableType : Transformer -> UndefOr AnyPtr -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.start"
  prim__start : Transformer -> PrimIO (UndefOr TransformerStartCallback)

  export
  %foreign "browser:lambda:(x,v)=>{x.start = v}"
  prim__setStart : Transformer -> UndefOr TransformerStartCallback -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.transform"
  prim__transform : Transformer -> PrimIO (UndefOr TransformerTransformCallback)

  export
  %foreign "browser:lambda:(x,v)=>{x.transform = v}"
  prim__setTransform :  Transformer
                     -> UndefOr TransformerTransformCallback
                     -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.writableType"
  prim__writableType : Transformer -> PrimIO (UndefOr AnyPtr)

  export
  %foreign "browser:lambda:(x,v)=>{x.writableType = v}"
  prim__setWritableType : Transformer -> UndefOr AnyPtr -> PrimIO ()

namespace UnderlyingSink

  export
  %foreign "browser:lambda:(a,b,c,d,e)=> {start: a,write: b,close: c,abort: d,type: e}"
  prim__new :  UndefOr UnderlyingSinkStartCallback
            -> UndefOr UnderlyingSinkWriteCallback
            -> UndefOr UnderlyingSinkCloseCallback
            -> UndefOr UnderlyingSinkAbortCallback
            -> UndefOr AnyPtr
            -> PrimIO UnderlyingSink

  export
  %foreign "browser:lambda:x=>x.abort"
  prim__abort : UnderlyingSink -> PrimIO (UndefOr UnderlyingSinkAbortCallback)

  export
  %foreign "browser:lambda:(x,v)=>{x.abort = v}"
  prim__setAbort :  UnderlyingSink
                 -> UndefOr UnderlyingSinkAbortCallback
                 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.close"
  prim__close : UnderlyingSink -> PrimIO (UndefOr UnderlyingSinkCloseCallback)

  export
  %foreign "browser:lambda:(x,v)=>{x.close = v}"
  prim__setClose :  UnderlyingSink
                 -> UndefOr UnderlyingSinkCloseCallback
                 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.start"
  prim__start : UnderlyingSink -> PrimIO (UndefOr UnderlyingSinkStartCallback)

  export
  %foreign "browser:lambda:(x,v)=>{x.start = v}"
  prim__setStart :  UnderlyingSink
                 -> UndefOr UnderlyingSinkStartCallback
                 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : UnderlyingSink -> PrimIO (UndefOr AnyPtr)

  export
  %foreign "browser:lambda:(x,v)=>{x.type = v}"
  prim__setType : UnderlyingSink -> UndefOr AnyPtr -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.write"
  prim__write : UnderlyingSink -> PrimIO (UndefOr UnderlyingSinkWriteCallback)

  export
  %foreign "browser:lambda:(x,v)=>{x.write = v}"
  prim__setWrite :  UnderlyingSink
                 -> UndefOr UnderlyingSinkWriteCallback
                 -> PrimIO ()

namespace UnderlyingSource

  export
  %foreign "browser:lambda:(a,b,c,d,e)=> {start: a,pull: b,cancel: c,type: d,autoAllocateChunkSize: e}"
  prim__new :  UndefOr UnderlyingSourceStartCallback
            -> UndefOr UnderlyingSourcePullCallback
            -> UndefOr UnderlyingSourceCancelCallback
            -> UndefOr String
            -> UndefOr JSBits64
            -> PrimIO UnderlyingSource

  export
  %foreign "browser:lambda:x=>x.autoAllocateChunkSize"
  prim__autoAllocateChunkSize : UnderlyingSource -> PrimIO (UndefOr JSBits64)

  export
  %foreign "browser:lambda:(x,v)=>{x.autoAllocateChunkSize = v}"
  prim__setAutoAllocateChunkSize :  UnderlyingSource
                                 -> UndefOr JSBits64
                                 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.cancel"
  prim__cancel :  UnderlyingSource
               -> PrimIO (UndefOr UnderlyingSourceCancelCallback)

  export
  %foreign "browser:lambda:(x,v)=>{x.cancel = v}"
  prim__setCancel :  UnderlyingSource
                  -> UndefOr UnderlyingSourceCancelCallback
                  -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.pull"
  prim__pull : UnderlyingSource -> PrimIO (UndefOr UnderlyingSourcePullCallback)

  export
  %foreign "browser:lambda:(x,v)=>{x.pull = v}"
  prim__setPull :  UnderlyingSource
                -> UndefOr UnderlyingSourcePullCallback
                -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.start"
  prim__start :  UnderlyingSource
              -> PrimIO (UndefOr UnderlyingSourceStartCallback)

  export
  %foreign "browser:lambda:(x,v)=>{x.start = v}"
  prim__setStart :  UnderlyingSource
                 -> UndefOr UnderlyingSourceStartCallback
                 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : UnderlyingSource -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.type = v}"
  prim__setType : UnderlyingSource -> UndefOr String -> PrimIO ()

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

namespace QueuingStrategySize

  export
  %foreign "browser:lambda:x=>(a)=>x(a)()"
  prim__toQueuingStrategySize :  ( UndefOr AnyPtr -> IO Double )
                              -> PrimIO QueuingStrategySize

namespace TransformerFlushCallback

  export
  %foreign "browser:lambda:x=>(a)=>x(a)()"
  prim__toTransformerFlushCallback :  (  TransformStreamDefaultController
                                      -> IO (Promise Undefined)
                                      )
                                   -> PrimIO TransformerFlushCallback

namespace TransformerStartCallback

  export
  %foreign "browser:lambda:x=>(a)=>x(a)()"
  prim__toTransformerStartCallback :  (  TransformStreamDefaultController
                                      -> IO AnyPtr
                                      )
                                   -> PrimIO TransformerStartCallback

namespace TransformerTransformCallback

  export
  %foreign "browser:lambda:x=>(a,b)=>x(a,b)()"
  prim__toTransformerTransformCallback :  (  AnyPtr
                                          -> TransformStreamDefaultController
                                          -> IO (Promise Undefined)
                                          )
                                       -> PrimIO TransformerTransformCallback

namespace UnderlyingSinkAbortCallback

  export
  %foreign "browser:lambda:x=>(a)=>x(a)()"
  prim__toUnderlyingSinkAbortCallback :  (  UndefOr AnyPtr
                                         -> IO (Promise Undefined)
                                         )
                                      -> PrimIO UnderlyingSinkAbortCallback

namespace UnderlyingSinkCloseCallback

  export
  %foreign "browser:lambda:x=>()=>x()()"
  prim__toUnderlyingSinkCloseCallback :  (() -> IO (Promise Undefined))
                                      -> PrimIO UnderlyingSinkCloseCallback

namespace UnderlyingSinkStartCallback

  export
  %foreign "browser:lambda:x=>(a)=>x(a)()"
  prim__toUnderlyingSinkStartCallback :  (  WritableStreamDefaultController
                                         -> IO AnyPtr
                                         )
                                      -> PrimIO UnderlyingSinkStartCallback

namespace UnderlyingSinkWriteCallback

  export
  %foreign "browser:lambda:x=>(a,b)=>x(a,b)()"
  prim__toUnderlyingSinkWriteCallback :  (  AnyPtr
                                         -> WritableStreamDefaultController
                                         -> IO (Promise Undefined)
                                         )
                                      -> PrimIO UnderlyingSinkWriteCallback

namespace UnderlyingSourceCancelCallback

  export
  %foreign "browser:lambda:x=>(a)=>x(a)()"
  prim__toUnderlyingSourceCancelCallback :  (  UndefOr AnyPtr
                                            -> IO (Promise Undefined)
                                            )
                                         -> PrimIO UnderlyingSourceCancelCallback

namespace UnderlyingSourcePullCallback

  export
  %foreign "browser:lambda:x=>(a)=>x(a)()"
  prim__toUnderlyingSourcePullCallback :  (  Union2 ReadableStreamDefaultController
                                                    ReadableByteStreamController
                                          -> IO (Promise Undefined)
                                          )
                                       -> PrimIO UnderlyingSourcePullCallback

namespace UnderlyingSourceStartCallback

  export
  %foreign "browser:lambda:x=>(a)=>x(a)()"
  prim__toUnderlyingSourceStartCallback :  (  Union2 ReadableStreamDefaultController
                                                     ReadableByteStreamController
                                           -> IO AnyPtr
                                           )
                                        -> PrimIO UnderlyingSourceStartCallback


text:
module Symbols

import DataTypes

%access public export

isSymbol : PrimitiveLispFunc
isSymbol [LispAtom _] = pure $ LispBool True
isSymbol _ = pure $ LispBool False

symbolToString : PrimitiveLispFunc
symbolToString [LispAtom s] = pure $ LispString s
symbolToString [arg] = Left $ TypeMismatch "list" arg
symbolToString args = Left $ NumArgs (MinMax 1 1) (cast $ length args) args

symbolPrimitives : List (String, PrimitiveLispFunc)
symbolPrimitives =
  [ ("symbol?", isSymbol)
  , ("symbol->string", symbolToString)
  ]

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module Syntax

||| Types
public export
data Ty : Type where
  ||| Integers
  TInt : Ty
  ||| Booleans
  TBool : Ty
  ||| Functions
  TArrow : Ty -> Ty -> Ty

export
implementation Eq Ty where
  TInt == TInt               = True
  TBool == TBool             = True
  (TArrow p1 r1) == (TArrow p2 r2) = p1 == p2 && r1 == r2
  _ == _                       = False

export
implementation Show Ty where
  show TInt  = "int"
  show TBool = "bool"
  show (TArrow pty rty) = "(" ++ (show pty) ++ " → " ++ (show rty) ++ ")"

public export
Name : Type
Name = String

public export
data Expr : Type where
  ||| Variables
  Var : Name -> Expr
  ||| Non-negative "integer" constant
  EInt : Integer -> Expr
  ||| Boolean constant
  EBool : Bool -> Expr
  ||| Product `e1 * e2`
  Times : Expr -> Expr -> Expr
  ||| Sum `e1 + e2`
  Plus : Expr -> Expr -> Expr
  ||| Difference `e1 - e2`
  Minus : Expr -> Expr -> Expr
  ||| Int comparison `e1 = e2`
  Equal : Expr -> Expr -> Expr
  ||| Int comparison `e1 < e2`
  Less : Expr -> Expr -> Expr
  ||| Conditional `if e1 then e2 else e3`
  If : Expr -> Expr -> Expr -> Expr
  ||| Function `fun f(x:s):t is e`
  Fun : Name -> Name -> Ty -> Ty -> Expr -> Expr
  ||| Application `e1 e2`
  Apply : Expr -> Expr -> Expr

export
implementation Show Expr where
  show (Var name) = "(Var " ++ name ++ ")"
  show (EInt n)   = show n
  show (EBool b)  = show b
  show (Times e1 e2) = "(" ++ show e1 ++ " * " ++ show e2 ++ ")"
  show (Plus e1 e2) = "(" ++ show e1 ++ " + " ++ show e2 ++ ")"
  show (Minus e1 e2) = "(" ++ show e1 ++ " - " ++ show e2 ++ ")"
  show (Equal e1 e2) = "(" ++ show e1 ++ " = " ++ show e2 ++ ")"
  show (Less e1 e2) = "(" ++ show e1 ++ " < " ++ show e2 ++ ")"
  show (If c te fe) = "if" ++ show c ++ " then " ++ show te ++ " else " ++ show fe
  show (Fun fnm pnm pty rty body) = "fun " ++ show fnm ++ " (" ++ pnm ++ " : " ++ show pty ++ ") : " ++ show (rty) ++ " is " ++ (show body)
  show (Apply e1 e2) = "(" ++ show e1 ++ " " ++ show e2 ++ ")"

public export
data TopLevelCmd : Type where
  ||| Expression
  TopExpr : Expr -> TopLevelCmd
  ||| Value definition `let x = e`
  TopDef : Name -> Expr -> TopLevelCmd

max_stars_repo_name: steshaw/idris-miniml

max_issues_repo_name: steshaw/idris-miniml

max_forks_repo_name: steshaw/idris-miniml


text:
module Language.Reflection.TT

import public Data.List

public export
FilePos : Type
FilePos = (Int, Int)

public export
data FC : Type where
     MkFC : String -> FilePos -> FilePos -> FC
     EmptyFC : FC

public export
emptyFC : FC
emptyFC = EmptyFC

public export
data NameType : Type where
     Bound   : NameType
     Func    : NameType
     DataCon : (tag : Int) -> (arity : Nat) -> NameType
     TyCon   : (tag : Int) -> (arity : Nat) -> NameType

public export
data Constant
    = I Int
    | BI Integer
    | B8 Int
    | B16 Int
    | B32 Int
    | B64 Integer
    | Str String
    | Ch Char
    | Db Double
    | WorldVal

    | IntType
    | IntegerType
    | Bits8Type
    | Bits16Type
    | Bits32Type
    | Bits64Type
    | StringType
    | CharType
    | DoubleType
    | WorldType

public export
data Namespace = MkNS (List String) -- namespace, stored in reverse order

export
showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs

export
Show Namespace where
  show (MkNS ns) = showSep "." (reverse ns)

public export
data Name = UN String -- user defined name
          | MN String Int -- machine generated name
          | NS Namespace Name -- name in a namespace
          | DN String Name -- a name and how to display it

export
Show Name where
  show (NS ns n) = show ns ++ "." ++ show n
  show (UN x) = x
  show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
  show (DN str y) = str

public export
data Count = M0 | M1 | MW

public export
data PiInfo t = ImplicitArg | ExplicitArg | AutoImplicit | DefImplicit t

public export
data IsVar : Name -> Nat -> List Name -> Type where
     First : IsVar n Z (n :: ns)
     Later : IsVar n i ns -> IsVar n (S i) (m :: ns)

public export
data LazyReason = LInf | LLazy | LUnknown

export
data TT : Type where [external]

{-
-- Type checked terms in the core TT
public export
data TT : List Name -> Type where
     Local : FC -> (idx : Nat) -> (0 prf : IsVar name idx vars) -> TT vars
     Ref : FC -> NameType -> Name -> TT vars
     Pi : FC -> Count -> PiInfo (TT vars) ->
          (x : Name) -> (argTy : TT vars) -> (retTy : TT (x :: vars)) ->
          TT vars
     Lam : FC -> Count -> PiInfo (TT vars) ->
           (x : Name) -> (argTy : TT vars) -> (scope : TT (x :: vars)) ->
           TT vars
     App : FC -> TT vars -> TT vars -> TT vars
     TDelayed : FC -> LazyReason -> TT vars -> TT vars
     TDelay : FC -> LazyReason -> (ty : TT vars) -> (arg : TT vars) -> TT vars
     TForce : FC -> LazyReason -> TT vars -> TT vars
     PrimVal : FC -> Constant -> TT vars
     Erased : FC -> TT vars
     TType : FC -> TT vars
     -}

public export
data TotalReq = Total | CoveringOnly | PartialOK

public export
data Visibility = Private | Export | Public


text:
-- Prototype of RealizedFunction as described in
-- https://blog.singularitynet.io/ai-dsl-toward-a-general-purpose-description-language-for-ai-agents-21459f691b9e
--
-- This is similar to SimpleDataRealizedFunction but the attributes
-- are wrapped in RealizedAttributes.

module RealizedFunction

import public RealizedAttributes

public export
data RealizedFunction : (t : Type) -> (attrs : RealizedAttributes) -> Type where
  MkRealizedFunction : (f : t) -> (attrs : RealizedAttributes)
                       -> RealizedFunction t attrs

-- Perform the composition between 2 realized functions.  The
-- resulting realized function is formed as follows:
--
-- 1. Composed lifted functions
-- 2. Use add_costs_min_quality for composing attributes
public export
compose : {a : Type} -> {b : Type} -> {c : Type} ->
          (RealizedFunction (b -> c) g_attrs) ->
          (RealizedFunction (a -> b) f_attrs) ->
          (RealizedFunction (a -> c) (add_costs_min_quality f_attrs g_attrs))
compose (MkRealizedFunction f f_attrs) (MkRealizedFunction g g_attrs) =
  MkRealizedFunction (f . g) (add_costs_min_quality f_attrs g_attrs)

-- Perform function application over realized functions.  Maybe we'd
-- want to used some funded data, as defined in FndType.
public export
apply : (RealizedFunction (a -> b) attrs) -> a -> b
apply (MkRealizedFunction f attrs) = f

max_stars_repo_name: sroberti/ai-dsl

max_issues_repo_name: sroberti/ai-dsl

max_forks_repo_name: sroberti/ai-dsl


text:
module Channel

import Data.List.Views
import System.Concurrency.Process
import public Network.Socket

%access public export

data Request msg = WriteLock
                 | Read
                 | ReleaseLock
                 | Pure msg

data ResultType msg = Fatal   String
                    | Warning String
                    | Correct msg

data Channel msg = MkChan (ProcID (Request msg))

data ChannelState = Unlocked | Locked

data ChannelCmd : (resultType : Type) -> (sharedResTyp : Type) -> (stateIn : ChannelState) ->
                  (stateOut : ChannelState) -> Type where
     ReadOnlyCmd : (chan : Channel typ) -> ChannelCmd (ResultType typ) typ Unlocked Unlocked
     ReadCmd : (chan : Channel typ) -> ChannelCmd (ResultType typ) typ Unlocked Locked
     WriteCmd : (chan : Channel typ) -> (newRes : typ) -> ChannelCmd Bool typ Locked Unlocked
     ReleaseLockCmd : (chan : Channel typ) -> ChannelCmd Bool typ Locked Unlocked

     PureCmd : (res : ty) -> ChannelCmd ty typ state state
     (>>=) : ChannelCmd a typ state1 state2 -> (a -> ChannelCmd b typ state2 state3) ->
             ChannelCmd b typ state1 state3

mutual
  write_inner : (req : Request msgType) -> (state : msgType) ->
                (procId : ProcID (Request msgType)) -> Process (Request msgType) ()
  write_inner req state procId =
    do send procId (Pure state)
       Just newReq <- recvFrom procId
        | Nothing => channelLoop state
       case newReq of
            (Pure newState) => channelLoop newState
            (ReleaseLock) => channelLoop state
            _ =>  channelLoop state

  channelLoop : (state : msgType) -> Process (Request msgType) ()
  channelLoop state = do (procId, req) <- recvWithSender
                         case req of
                               WriteLock => write_inner req state procId
                               ReleaseLock => channelLoop state
                               Read => do send procId (Pure state)
                                          channelLoop state

makeChan : (init : ty) -> IO (Channel (ty))
makeChan init = do procId <- run (create (channelLoop init))
                   pure (MkChan procId)

read_inner : Channel msg -> (req : Request msg) -> IO (ResultType msg)
read_inner (MkChan procId) req =
    do ok <- run (send procId req)
       Just newReq <- run (recvFrom procId)
        | Nothing => pure (Fatal "Channel thread died")
       case newReq of
            (Pure val) => pure (Correct val)
            _ => pure (Warning "Did not recieve correct formatted state from channel thread")

read : Channel msg -> IO (ResultType msg)
read chan = read_inner chan WriteLock

readOnly : Channel msg -> IO (ResultType msg)
readOnly chan = read_inner chan Read

write : Channel msg -> msg -> IO Bool
write (MkChan procId) msg = run (send procId (Pure msg))

run : ChannelCmd res typ inState outState -> IO res
run (ReadOnlyCmd chan) = readOnly chan
run (ReadCmd chan) = read chan
run (WriteCmd chan newRes) = write chan newRes
run (ReleaseLockCmd (MkChan procId)) = run (send procId ReleaseLock)
run (PureCmd res) = pure res
run (x >>= f) = do x' <- run x
                   run (f x')

max_stars_repo_name: AsmusAB/Idris-peer-to-peer-network

max_issues_repo_name: AsmusAB/Idris-peer-to-peer-network

max_forks_repo_name: AsmusAB/Idris-peer-to-peer-network


text:
module Idris.Codegen.ExtSTG.PrimOp

import Data.Vect
import Core.Core
import Core.Context
import Compiler.ANF
import Data.List
import Idris.Codegen.ExtSTG.STG
import Idris.Codegen.ExtSTG.Core
import Idris.Codegen.ExtSTG.String

||| PrimType when the constant is compiled insides the box.
export
constantToPrimRep : Constant -> Core (List PrimRep)
constantToPrimRep IntType     = pure [IntRep]
constantToPrimRep IntegerType = pure [IntRep] -- TODO: This is not the right representation for integer
constantToPrimRep Bits8Type   = pure [Word8Rep]
constantToPrimRep Bits16Type  = pure [Word16Rep]
constantToPrimRep Bits32Type  = pure [Word32Rep]
constantToPrimRep Bits64Type  = pure [Word64Rep]
constantToPrimRep DoubleType  = pure [DoubleRep]
-- constantToPrimRep StringType  = pure [AddrRep]
constantToPrimRep CharType    = pure [Word8Rep] -- TODO: Check if this is the right type for Chars?
constantToPrimRep WorldType   = pure []
constantToPrimRep other = coreFail $ InternalError $ "No PrimRep for " ++ show other

||| Creates a multilevel case statement block to unwrap/wrap the primitive values
||| around a two parameter STG primitive function call.
binPrimOp
  : {name : String} -> {primOpRep, retPrimOpRep: PrimRep}
  -> UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => FC -> Core.Name.Name
  -> Constant -> PrimOp name [primOpRep, primOpRep] retPrimOpRep -> Vect 2 AVar -> Constant
  -> Core (Expr Core.stgRepType)
binPrimOp fc n ty op as rt = do
  [arg1, arg2] <- traverseVect (mkBinderIdVar fc n Core.stgRepType) as
  ((AlgDataCon [rep]) ** dc) <- dataConIdForConstant ty
    | wrongRep => coreFail $ InternalError $ "DataConId has wrong RepType: " ++ show (fc, n, wrongRep)
  Refl <- checkSemiDecEq ("binPrimOp:" ++ show n ++ " " ++ PrimOp.name op) rep primOpRep
  n4 <- mkSBinderRepLocal (SingleValue primOpRep) fc n 4
  n5 <- mkSBinderRepLocal (SingleValue primOpRep) fc n 5
  let resultTypeName = Nothing
  pure $ StgCase
          (AlgAlt !(tyConIdForConstant ty))
          (StgApp arg1 [] Core.stgRepType)
          !(mkSBinderLocal fc n 3)
          [ MkAlt (AltDataCon (mkDataConIdSg dc)) n4
             (StgCase
                (AlgAlt !(tyConIdForConstant ty))
                (StgApp arg2 [] Core.stgRepType)
                !(mkSBinderLocal fc n 4)
                [ MkAlt (AltDataCon (mkDataConIdSg dc)) n5
                    (StgCase
                      (PrimAlt retPrimOpRep)
                      (StgOpApp op
                        [ StgVarArg !(mkBinderIdVar fc n (SingleValue primOpRep) (ALocal 4))
                        , StgVarArg !(mkBinderIdVar fc n (SingleValue primOpRep) (ALocal 5))
                        ])
                      !(mkSBinderRepLocal (SingleValue retPrimOpRep) fc n 6)
                      [ MkAlt AltDefault ()
                          (StgConApp
                            !(dataConIdRepForConstant retPrimOpRep rt)
                            (StgVarArg !(mkBinderIdVar fc n (SingleValue retPrimOpRep) (ALocal 6))))
                      ])
                ])
          ]

||| Creates a multilevel case statement block to unwrap/wrap the primitive values
||| around a two parameter STG primitive function call.
unaryPrimOp
  :  {name : String} -> {primOpRep, retPrimOpRep : PrimRep}
  -> UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => FC -> Core.Name.Name
  -> Constant -> PrimOp name [primOpRep] retPrimOpRep -> Vect 1 AVar -> Constant
  -> Core (Expr Core.stgRepType)
unaryPrimOp fc n ty op as rt = do
  [arg1] <- traverseVect (mkBinderIdVar fc n Core.stgRepType) as
  -- As we box everyting, and the result will be Lifted
  ((AlgDataCon [rep]) ** dc) <- dataConIdForConstant ty
    | wrongRep => coreFail $ InternalError $ "DataConId has wrong RepType: " ++ show (fc,n,wrongRep)
  Refl <- checkSemiDecEq ("unaryPrimOp:" ++ show n ++ " " ++ PrimOp.name op) primOpRep rep
  n4 <- mkSBinderRepLocal (SingleValue primOpRep) fc n 4
  pure $ StgCase
          (AlgAlt !(tyConIdForConstant ty))
          (StgApp arg1 [] Core.stgRepType)
          !(mkSBinderLocal fc n 3)
          [ MkAlt (AltDataCon (mkDataConIdSg dc)) n4
             (StgCase
                (PrimAlt retPrimOpRep)
                (StgOpApp op (StgVarArg !(mkBinderIdVar fc n (SingleValue primOpRep) (ALocal 4))))
                !(mkSBinderRepLocal (SingleValue retPrimOpRep) fc n 5)
                [ MkAlt AltDefault ()
                    (StgConApp
                      !(dataConIdRepForConstant retPrimOpRep rt)
                      (StgVarArg !(mkBinderIdVar fc n (SingleValue retPrimOpRep) (ALocal 5))))
                ])
          ]

-- TODO: Lookup the name of the already defined STG function. Mainly it is used to lookup
-- String helper functions.
definedFunction
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> String
  -> Core (BinderId Core.stgRepType)
definedFunction = mkBinderIdStr

export
compilePrimOp
  :  UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => FC -> Core.Name.Name -> PrimFn arity -> Vect arity AVar
  -> Core (Expr Core.stgRepType)
compilePrimOp {arity = 2} fc n (Add IntType)      as = binPrimOp fc n IntType    PlusInt     as IntType
compilePrimOp {arity = 2} fc n (Add IntegerType)  as = binPrimOp fc n IntType    PlusInt     as IntegerType
compilePrimOp {arity = 2} fc n (Add Bits8Type)    as = binPrimOp fc n Bits8Type  PlusWord8   as Bits8Type
compilePrimOp {arity = 2} fc n (Add Bits16Type)   as = binPrimOp fc n Bits16Type PlusWord16  as Bits16Type
compilePrimOp {arity = 2} fc n (Add Bits32Type)   as = binPrimOp fc n Bits32Type PlusWord    as Bits32Type
compilePrimOp {arity = 2} fc n (Add Bits64Type)   as = binPrimOp fc n Bits64Type PlusWord    as Bits64Type
compilePrimOp {arity = 2} fc n (Add DoubleType)   as = binPrimOp fc n DoubleType PlusDouble  as DoubleType
compilePrimOp {arity = 2} fc n (Add ty) _ = throw $ InternalError $ "No add for:" ++ show ty

compilePrimOp {arity = 2} fc n (Sub IntType)      as = binPrimOp fc n IntType     SubInt    as IntType
compilePrimOp {arity = 2} fc n (Sub IntegerType)  as = binPrimOp fc n IntegerType SubInt    as IntegerType
compilePrimOp {arity = 2} fc n (Sub Bits8Type)    as = binPrimOp fc n Bits8Type   SubWord8  as Bits8Type
compilePrimOp {arity = 2} fc n (Sub Bits16Type)   as = binPrimOp fc n Bits16Type  SubWord16 as Bits16Type
compilePrimOp {arity = 2} fc n (Sub Bits32Type)   as = binPrimOp fc n Bits32Type  SubWord   as Bits32Type
compilePrimOp {arity = 2} fc n (Sub Bits64Type)   as = binPrimOp fc n Bits64Type  SubWord   as Bits64Type
compilePrimOp {arity = 2} fc n (Sub DoubleType)   as = binPrimOp fc n DoubleType  SubDouble as DoubleType
compilePrimOp {arity = 2} fc n (Sub ty) _ = throw $ InternalError $ "No sub for:" ++ show ty

compilePrimOp {arity = 2} fc n (Mul IntType)      as = binPrimOp fc n IntType     TimesInt    as IntType
compilePrimOp {arity = 2} fc n (Mul IntegerType)  as = binPrimOp fc n IntegerType TimesInt    as IntegerType
compilePrimOp {arity = 2} fc n (Mul Bits8Type)    as = binPrimOp fc n Bits8Type   TimesWord8  as Bits8Type
compilePrimOp {arity = 2} fc n (Mul Bits16Type)   as = binPrimOp fc n Bits16Type  TimesWord16 as Bits16Type
compilePrimOp {arity = 2} fc n (Mul Bits32Type)   as = binPrimOp fc n Bits32Type  TimesWord   as Bits32Type
compilePrimOp {arity = 2} fc n (Mul Bits64Type)   as = binPrimOp fc n Bits64Type  TimesWord   as Bits64Type
compilePrimOp {arity = 2} fc n (Mul DoubleType)   as = binPrimOp fc n DoubleType  TimesDouble as DoubleType
compilePrimOp {arity = 2} fc n (Mul ty) _ = throw $ InternalError $ "No mul for:" ++ show ty

compilePrimOp {arity = 2} fc n (Div IntType)      as = binPrimOp fc n IntType     QuotInt     as IntType
compilePrimOp {arity = 2} fc n (Div IntegerType)  as = binPrimOp fc n IntegerType QuotInt     as IntegerType
compilePrimOp {arity = 2} fc n (Div Bits8Type)    as = binPrimOp fc n Bits8Type   QuotWord8   as Bits8Type
compilePrimOp {arity = 2} fc n (Div Bits16Type)   as = binPrimOp fc n Bits16Type  QuotWord16  as Bits16Type
compilePrimOp {arity = 2} fc n (Div Bits32Type)   as = binPrimOp fc n Bits32Type  QuotWord    as Bits32Type
compilePrimOp {arity = 2} fc n (Div Bits64Type)   as = binPrimOp fc n Bits64Type  QuotWord    as Bits64Type
compilePrimOp {arity = 2} fc n (Div DoubleType)   as = binPrimOp fc n DoubleType  QuotDouble  as DoubleType
compilePrimOp {arity = 2} fc n (Div ty) _ = throw $ InternalError $ "No div for:" ++ show ty

compilePrimOp {arity = 2} fc n (Mod IntType)      as = binPrimOp fc n IntType     RemInt    as IntType
compilePrimOp {arity = 2} fc n (Mod IntegerType)  as = binPrimOp fc n IntegerType RemInt    as IntegerType
compilePrimOp {arity = 2} fc n (Mod Bits8Type)    as = binPrimOp fc n Bits8Type   RemWord8  as Bits8Type
compilePrimOp {arity = 2} fc n (Mod Bits16Type)   as = binPrimOp fc n Bits16Type  RemWord16 as Bits16Type
compilePrimOp {arity = 2} fc n (Mod Bits32Type)   as = binPrimOp fc n Bits32Type  RemWord   as Bits32Type
compilePrimOp {arity = 2} fc n (Mod Bits64Type)   as = binPrimOp fc n Bits64Type  RemWord   as Bits64Type
compilePrimOp {arity = 2} fc n (Mod ty) _ = throw $ InternalError $ "No mod for:" ++ show ty

compilePrimOp {arity = 1} fc n (Neg IntType)      as = unaryPrimOp fc n IntType      NegateInt     as IntType
compilePrimOp {arity = 1} fc n (Neg IntegerType)  as = unaryPrimOp fc n IntegerType  NegateInt     as IntegerType
compilePrimOp {arity = 1} fc n (Neg DoubleType)   as = unaryPrimOp fc n DoubleType   NegateDouble  as DoubleType
compilePrimOp {arity = 1} fc n (Neg ty) _ = throw $ InternalError $ "No neg for:" ++ show ty

compilePrimOp {arity = 2} fc n (ShiftL IntType)     as = binPrimOp fc n IntType IShiftLInt as IntType
compilePrimOp {arity = 2} fc n (ShiftL IntegerType) as = binPrimOp fc n IntType IShiftLInt as IntegerType
compilePrimOp {arity = 2} fc n (ShiftL ty) _ = throw $ InternalError $ "No shiftl for:" ++ show ty

compilePrimOp {arity = 2} fc n (ShiftR IntType)     as = binPrimOp fc n IntType IShiftLRInt as IntType
compilePrimOp {arity = 2} fc n (ShiftR IntegerType) as = binPrimOp fc n IntType IShiftLRInt as IntegerType
compilePrimOp {arity = 2} fc n (ShiftR ty) _ = throw $ InternalError $ "No shiftr for:" ++ show ty

compilePrimOp {arity = 2} fc n (BAnd IntType)     as = binPrimOp fc n IntType     AndInt  as IntType
compilePrimOp {arity = 2} fc n (BAnd IntegerType) as = binPrimOp fc n IntegerType AndInt  as IntegerType
compilePrimOp {arity = 2} fc n (BAnd Bits8Type)   as = binPrimOp fc n Bits8Type   AndWord as Bits8Type
compilePrimOp {arity = 2} fc n (BAnd Bits16Type)  as = binPrimOp fc n Bits16Type  AndWord as Bits16Type
compilePrimOp {arity = 2} fc n (BAnd Bits32Type)  as = binPrimOp fc n Bits32Type  AndWord as Bits32Type
compilePrimOp {arity = 2} fc n (BAnd Bits64Type)  as = binPrimOp fc n Bits64Type  AndWord as Bits64Type
compilePrimOp {arity = 2} fc n (BAnd ty) _ = throw $ InternalError $ "No band for:" ++ show ty

compilePrimOp {arity = 2} fc n (BOr IntType)      as = binPrimOp fc n IntType     OrInt   as IntType
compilePrimOp {arity = 2} fc n (BOr IntegerType)  as = binPrimOp fc n IntegerType OrInt   as IntegerType
compilePrimOp {arity = 2} fc n (BOr Bits8Type)    as = binPrimOp fc n Bits8Type   OrWord  as Bits8Type
compilePrimOp {arity = 2} fc n (BOr Bits16Type)   as = binPrimOp fc n Bits16Type  OrWord  as Bits16Type
compilePrimOp {arity = 2} fc n (BOr Bits32Type)   as = binPrimOp fc n Bits32Type  OrWord  as Bits32Type
compilePrimOp {arity = 2} fc n (BOr Bits64Type)   as = binPrimOp fc n Bits64Type  OrWord  as Bits64Type
compilePrimOp {arity = 2} fc n (BOr ty) _ = throw $ InternalError $ "No bor for:" ++ show ty

compilePrimOp {arity = 2} fc n (BXOr IntType)     as = binPrimOp fc n IntType     XOrInt  as IntType
compilePrimOp {arity = 2} fc n (BXOr IntegerType) as = binPrimOp fc n IntegerType XOrInt  as IntegerType
compilePrimOp {arity = 2} fc n (BXOr Bits8Type)   as = binPrimOp fc n Bits8Type   XOrWord as Bits8Type
compilePrimOp {arity = 2} fc n (BXOr Bits16Type)  as = binPrimOp fc n Bits16Type  XOrWord as Bits16Type
compilePrimOp {arity = 2} fc n (BXOr Bits32Type)  as = binPrimOp fc n Bits32Type  XOrWord as Bits32Type
compilePrimOp {arity = 2} fc n (BXOr Bits64Type)  as = binPrimOp fc n Bits64Type  XOrWord as Bits64Type
compilePrimOp {arity = 2} fc n (BXOr ty) _ = throw $ InternalError $ "No bxor for:" ++ show ty

compilePrimOp {arity = 2} fc n (LT IntType)     as = binPrimOp fc n IntType     LTInt     as IntType
compilePrimOp {arity = 2} fc n (LT IntegerType) as = binPrimOp fc n IntegerType LTInt     as IntType
compilePrimOp {arity = 2} fc n (LT Bits8Type)   as = binPrimOp fc n Bits8Type   LTWord8   as IntType
compilePrimOp {arity = 2} fc n (LT Bits16Type)  as = binPrimOp fc n Bits16Type  LTWord16  as IntType
compilePrimOp {arity = 2} fc n (LT Bits32Type)  as = binPrimOp fc n Bits32Type  LTWord    as IntType
compilePrimOp {arity = 2} fc n (LT Bits64Type)  as = binPrimOp fc n Bits64Type  LTWord    as IntType
compilePrimOp {arity = 2} fc n (LT CharType)    as = binPrimOp fc n CharType    LTWord8   as IntType
compilePrimOp {arity = 2} fc n (LT DoubleType)  as = binPrimOp fc n DoubleType  LTDouble  as IntType
compilePrimOp {arity = 2} fc n (LT ty) _ = throw $ InternalError $ "No lt for:" ++ show ty

compilePrimOp {arity = 2} fc n (LTE IntType)      as = binPrimOp fc n IntType     LTEInt    as IntType
compilePrimOp {arity = 2} fc n (LTE IntegerType)  as = binPrimOp fc n IntType     LTEInt    as IntType
compilePrimOp {arity = 2} fc n (LTE Bits8Type)    as = binPrimOp fc n Bits8Type   LTEWord8  as IntType
compilePrimOp {arity = 2} fc n (LTE Bits16Type)   as = binPrimOp fc n Bits16Type  LTEWord16 as IntType
compilePrimOp {arity = 2} fc n (LTE Bits32Type)   as = binPrimOp fc n Bits32Type  LTEWord   as IntType
compilePrimOp {arity = 2} fc n (LTE Bits64Type)   as = binPrimOp fc n Bits64Type  LTEWord   as IntType
compilePrimOp {arity = 2} fc n (LTE CharType)     as = binPrimOp fc n CharType    LTEWord8  as IntType
compilePrimOp {arity = 2} fc n (LTE DoubleType)   as = binPrimOp fc n DoubleType  LTEDouble as IntType
compilePrimOp {arity = 2} fc n (LTE ty) _ = throw $ InternalError $ "No lte for:" ++ show ty

compilePrimOp {arity = 2} fc n (EQ IntType)     as = binPrimOp fc n IntType     EQInt     as IntType
compilePrimOp {arity = 2} fc n (EQ IntegerType) as = binPrimOp fc n IntType     EQInt     as IntType
compilePrimOp {arity = 2} fc n (EQ Bits8Type)   as = binPrimOp fc n Bits8Type   EQWord8   as IntType
compilePrimOp {arity = 2} fc n (EQ Bits16Type)  as = binPrimOp fc n Bits16Type  EQWord16  as IntType
compilePrimOp {arity = 2} fc n (EQ Bits32Type)  as = binPrimOp fc n Bits32Type  EQWord    as IntType
compilePrimOp {arity = 2} fc n (EQ Bits64Type)  as = binPrimOp fc n Bits64Type  EQWord    as IntType
compilePrimOp {arity = 2} fc n (EQ CharType)    as = binPrimOp fc n CharType    EQWord8   as IntType
compilePrimOp {arity = 2} fc n (EQ DoubleType)  as = binPrimOp fc n DoubleType  EQDouble  as IntType
compilePrimOp {arity = 2} fc n (EQ ty) _ = throw $ InternalError $ "No eq for:" ++ show ty

compilePrimOp {arity = 2} fc n (GTE IntType)      as = binPrimOp fc n IntType     GTEInt    as IntType
compilePrimOp {arity = 2} fc n (GTE IntegerType)  as = binPrimOp fc n IntType     GTEInt    as IntType
compilePrimOp {arity = 2} fc n (GTE Bits8Type)    as = binPrimOp fc n Bits8Type   GTEWord8  as IntType
compilePrimOp {arity = 2} fc n (GTE Bits16Type)   as = binPrimOp fc n Bits16Type  GTEWord16 as IntType
compilePrimOp {arity = 2} fc n (GTE Bits32Type)   as = binPrimOp fc n Bits32Type  GTEWord   as IntType
compilePrimOp {arity = 2} fc n (GTE Bits64Type)   as = binPrimOp fc n Bits64Type  GTEWord   as IntType
compilePrimOp {arity = 2} fc n (GTE CharType)     as = binPrimOp fc n CharType    GTEWord8  as IntType
compilePrimOp {arity = 2} fc n (GTE DoubleType)   as = binPrimOp fc n DoubleType  GTEDouble as IntType
compilePrimOp {arity = 2} fc n (GTE ty) _ = throw $ InternalError $ "No gte for:" ++ show ty

compilePrimOp {arity = 2} fc n (GT IntType)     as = binPrimOp fc n IntType     GTInt     as IntType
compilePrimOp {arity = 2} fc n (GT IntegerType) as = binPrimOp fc n IntType     GTInt     as IntType
compilePrimOp {arity = 2} fc n (GT Bits8Type)   as = binPrimOp fc n Bits8Type   GTWord8   as IntType
compilePrimOp {arity = 2} fc n (GT Bits16Type)  as = binPrimOp fc n Bits16Type  GTWord16  as IntType
compilePrimOp {arity = 2} fc n (GT Bits32Type)  as = binPrimOp fc n Bits32Type  GTWord    as IntType
compilePrimOp {arity = 2} fc n (GT Bits64Type)  as = binPrimOp fc n Bits64Type  GTWord    as IntType
compilePrimOp {arity = 2} fc n (GT CharType)    as = binPrimOp fc n CharType    GTWord8   as IntType
compilePrimOp {arity = 2} fc n (GT DoubleType)  as = binPrimOp fc n DoubleType  GTDouble  as IntType
compilePrimOp {arity = 2} fc n (GT ty) _ = throw $ InternalError $ "No gt for:" ++ show ty

{-
String literals must be toplevel STG definitions. That are represented as Addr in STG.
Idris string module that contains the STG definition of String Handling.

Idris:
String constants are instroduced with the Str constructor.
The runtime system of the backend should create runtme values from the String constants.
String operations should work on the runtime representation of the string values and return
new String value.

STG:
String constants are represented as LitString which will be represented as an Addr# inside a
top-level definition. When we create an STG-String value from the Idris.Str literal we need to
look-up the top-level STG definition for the String literal and extract the Addr# value
wrap it in a constructor that the STG.String Operation could handle.
I need an example for the top-level String constant in STG.
-}

compilePrimOp {arity=1} fc n StrLength as =
  pure (StgApp !(definedFunction "Idris.String.strLength")
               !(traverse (map (mkArgSg . StgVarArg) . mkBinderIdVar fc n Core.stgRepType) $ toList as)
               (SingleValue LiftedRep))

-- TODO: Appropiate Char handling.
compilePrimOp {arity=1} fc n StrHead as =
  pure (StgApp !(definedFunction "Idris.String.strHead")
               !(traverse (map (mkArgSg . StgVarArg) . mkBinderIdVar fc n Core.stgRepType) $ toList as)
               (SingleValue LiftedRep))

compilePrimOp {arity=1} fc n StrTail as =
  pure (StgApp !(definedFunction "Idris.String.strTail")
               !(traverse (map (mkArgSg . StgVarArg) . mkBinderIdVar fc n Core.stgRepType) $ toList as)
               (SingleValue LiftedRep))

compilePrimOp {arity=2} fc n StrIndex as =
  pure (StgApp !(definedFunction "Idris.String.strIndex")
               !(traverse (map (mkArgSg . StgVarArg) . mkBinderIdVar fc n Core.stgRepType) $ toList as)
               (SingleValue LiftedRep))

compilePrimOp {arity=2} fc n StrCons as =
  pure (StgApp !(definedFunction "Idris.String.strCons")
               !(traverse (map (mkArgSg . StgVarArg) . mkBinderIdVar fc n Core.stgRepType) $ toList as)
               (SingleValue LiftedRep))

compilePrimOp {arity=2} fc n StrAppend as =
  pure (StgApp !(definedFunction "Idris.String.strAppend")
               !(traverse (map (mkArgSg . StgVarArg) . mkBinderIdVar fc n Core.stgRepType) $ toList as)
               (SingleValue LiftedRep))

compilePrimOp {arity=1} fc n StrReverse as =
  pure (StgApp !(definedFunction "Idris.String.strReverse")
               !(traverse (map (mkArgSg . StgVarArg) . mkBinderIdVar fc n Core.stgRepType) $ toList as)
               (SingleValue LiftedRep))

compilePrimOp {arity=3} fc n StrSubstr as =
  pure (StgApp !(definedFunction "Idris.String.strSubstr")
               !(traverse (map (mkArgSg . StgVarArg) . mkBinderIdVar fc n Core.stgRepType) $ toList as)
               (SingleValue LiftedRep))

compilePrimOp {arity=1} fc n DoubleExp as = unaryPrimOp fc n DoubleType ExpDouble as DoubleType
compilePrimOp {arity=1} fc n DoubleLog as = unaryPrimOp fc n DoubleType LogDouble as DoubleType
compilePrimOp {arity=1} fc n DoubleSin as = unaryPrimOp fc n DoubleType SinDouble as DoubleType
compilePrimOp {arity=1} fc n DoubleCos as = unaryPrimOp fc n DoubleType CosDouble as DoubleType
compilePrimOp {arity=1} fc n DoubleTan as = unaryPrimOp fc n DoubleType TanDouble as DoubleType
compilePrimOp {arity=1} fc n DoubleASin as = unaryPrimOp fc n DoubleType ASinDouble as DoubleType
compilePrimOp {arity=1} fc n DoubleACos as = unaryPrimOp fc n DoubleType ACosDouble as DoubleType
compilePrimOp {arity=1} fc n DoubleATan as = unaryPrimOp fc n DoubleType ATanDouble as DoubleType
compilePrimOp {arity=1} fc n DoubleSqrt as = unaryPrimOp fc n DoubleType SqrtDouble as DoubleType

--     DoubleFloor : PrimFn 1
--     DoubleCeiling : PrimFn 1
--     Cast : Constant -> Constant -> PrimFn 1 -- What is the semantics for this? Check in the official backend.

--     BelieveMe : PrimFn 3
-- BeleiveMe should copy the data, but in referential transparance it is not needed.
compilePrimOp {arity=3} fc n BelieveMe [_,_,a] =
  pure (StgApp !(mkBinderIdVar fc n Core.stgRepType a) [] (SingleValue LiftedRep))

--     Crash : PrimFn 2 -- What are the parameters for this?
--     Use this FFI call to crash the haskell runtime.
--     https://github.com/grin-compiler/ghc-whole-program-compiler-project/blob/master/external-stg-interpreter/lib/Stg/Interpreter/FFI.hs#L178-L183
--     1b3f15ca69ea443031fa69a488c660a2c22182b8
compilePrimOp _ _ p as
  = pure
  $ StgApp (!(definedFunction STRING_FROM_ADDR))
           [ mkArgSg $ StgLitArg $ LitString $ "compilePrimOp " ++ show p ++ " " ++ show as
           ]
           (SingleValue LiftedRep)

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Main
import Effects
import Effect.StdIO
import IdrisNet.Socket
import IdrisNet.UDP.UDPServer

udpServerLoop : Nat ->
                { [UDPSERVER UDPBound, STDIO] ==>
                  [UDPSERVER (), STDIO] }
                Eff IO ()
udpServerLoop Z = udpClose
udpServerLoop (S k) = do
  case !(udpReadString 1024) of
    UDPSuccess (addr, str, _) => do
      putStr ("Received: " ++ str ++ "from " ++ (show (remote_addr addr)) ++ "\n")
      UDPSuccess _ <- udpWriteString (IPv4Addr 127 0 0 1) 9001 "pines test"
        | UDPFailure err => do putStr ("Error!" ++ (show err))
                               udpFinalise
        | UDPRecoverableError err => do putStr ("Error!" ++ (show err))
                                        udpClose
      udpServerLoop k
    UDPRecoverableError _ => udpServerLoop (S k)
    UDPFailure err => do
      putStr ("Error: " ++ (show err) ++ "\n")
      udpFinalise

udpBindAndLoop : Port ->
                 { [UDPSERVER (), STDIO] }
                 Eff IO ()
udpBindAndLoop p = do
  case !(udpBind Nothing p) of
    UDPSuccess _ => udpServerLoop 5
    UDPRecoverableError err => putStr ("Error binding: " ++ (show err) ++ "\n")
    UDPFailure err => putStr ("Error binding: " ++ (show err) ++ "\n")

main : IO ()
main = run (udpBindAndLoop 4099)


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.
--}
module XLA.Literal

import System.FFI
import XLA.XlaData
import XLA.FFI
import Types
import Util

libxla : String -> String
libxla fname = "C:" ++ fname ++ ",libxla"

public export
Literal : Type
Literal = Struct "Literal" []

export
interface XLAPrimitive dtype where
    primitiveType : PrimitiveType
    set : Literal -> Ptr Int -> dtype -> PrimIO ()
    get : Literal -> Ptr Int -> dtype

%foreign (libxla "Literal_new")
prim__allocLiteral : Ptr Int -> Int -> Int -> PrimIO Literal

%foreign (libxla "Literal_delete")
prim__Literal_delete : Literal -> PrimIO ()

export
delete : Literal -> IO ()
delete = primIO . prim__Literal_delete

populateLiteral : {rank : _} -> (shape : Shape {rank}) -> XLAPrimitive dtype =>
    Literal -> Array shape {dtype=dtype} -> IO ()
populateLiteral {rank} shape lit arr = impl {shapesSum=Refl} shape [] arr where
    impl : {a : _} -> (rem_shape : Shape {rank=r}) -> (acc_indices : Shape {rank=a})
        -> {shapesSum : a + r = rank} -> Array rem_shape {dtype=dtype} -> IO ()
    impl {a} [] acc_indices x = do
        idx_ptr <- mkIntArray acc_indices
        primIO $ set lit idx_ptr x
        free idx_ptr
    impl {shapesSum} {r=S r'} {a} (n :: rest) acc_indices xs =
        traverse_ setArrays (enumerate xs) where
            setArrays : (Nat, Array rest {dtype=dtype}) -> IO ()
            setArrays (idx, xs') =
                let shapesSum' = rewrite plusSuccRightSucc a r' in shapesSum
                 in impl {shapesSum=shapesSum'} rest (snoc acc_indices idx) xs'

export
mkLiteral : XLAPrimitive dtype => {rank : _} -> {shape : Shape {rank}}
    -> Array shape {dtype=dtype} -> IO Literal
mkLiteral xs = do
    shape_ptr <- mkIntArray shape
    literal <- primIO $ prim__allocLiteral shape_ptr (cast rank) (cast $ primitiveType {dtype=dtype})
    populateLiteral shape literal xs
    free shape_ptr
    pure literal

%foreign (libxla "Literal_Set_bool")
prim__literalSetBool : Literal -> Ptr Int -> Int -> PrimIO ()

%foreign (libxla "Literal_Get_bool")
literalGetBool : Literal -> Ptr Int -> Int

export
XLAPrimitive Bool where
  primitiveType = PRED
  set lit idxs x = prim__literalSetBool lit idxs (if x then 1 else 0)
  get lit idxs = case literalGetBool lit idxs of
    0 => False
    1 => True
    x => (assert_total idris_crash) (
           "Internal error: expected 0 or 1 from XLA C API for boolean conversion, got " ++ show x
         )

%foreign (libxla "Literal_Set_double")
prim__literalSetDouble : Literal -> Ptr Int -> Double -> PrimIO ()

%foreign (libxla "Literal_Get_double")
literalGetDouble : Literal -> Ptr Int -> Double

export
XLAPrimitive Double where
  primitiveType = F64
  set = prim__literalSetDouble
  get = literalGetDouble

%foreign (libxla "Literal_Set_int")
prim__literalSetInt : Literal -> Ptr Int -> Int -> PrimIO ()

%foreign (libxla "Literal_Get_int")
literalGetInt : Literal -> Ptr Int -> Int

export
XLAPrimitive Int where
  primitiveType = S32
  set = prim__literalSetInt
  get = literalGetInt

export
toArray : XLAPrimitive dtype => {shape : Shape} -> Literal -> Array shape {dtype=dtype}
toArray lit = impl {shapesSum=Refl} shape [] where
    impl : (remaining_shape : Vect r Nat)
        -> {a : _} -> {shapesSum : a + r = rank}
        -> (accumulated_indices : Vect a Nat)
        -> Array remaining_shape {dtype=dtype}
    impl [] acc = unsafePerformIO impl_io where
        impl_io : IO dtype
        impl_io = do
            idx_ptr <- mkIntArray acc
            let res = get lit idx_ptr
            free idx_ptr
            pure res
    impl (n :: rest) acc = map ((impl rest {shapesSum=Refl}) . (snoc acc)) (range n)

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
%foreign "C:mkThing, libmkalloc"
prim__mkThing : PrimIO AnyPtr
%foreign "C:getStr, libmkalloc"
prim__getStr : GCAnyPtr -> PrimIO String
%foreign "C:freeThing, libmkalloc"
prim__freeThing : AnyPtr -> PrimIO ()

mkThing : IO AnyPtr
mkThing = primIO prim__mkThing

getThingStr : GCAnyPtr -> IO String
getThingStr t = primIO (prim__getStr t)

freeThing : AnyPtr -> IO ()
freeThing t = primIO (prim__freeThing t)

doThings : IO ()
doThings
     = do xp <- mkThing
          yp <- mkThing

          x <- onCollectAny xp (\p => do putStrLn "Free X"
                                         freeThing p)
          y <- onCollectAny yp (\p => do putStrLn "Free Y"
                                         freeThing p)

          putStrLn !(getThingStr x)
          putStrLn !(getThingStr y)

main : IO ()
main = do doThings
          putStrLn "Done"


text:
module Idris.IDEMode.MakeClause

import Core.Name
import Parser.Lexer.Source
import Parser.Unlit

import Data.List
import Data.Nat
import Data.Strings

%default total

-- Implement make-with and make-case from the IDE mode

showRHSName : Name -> String
showRHSName n
    = let fn = show (dropNS n) in
          if any isOpChar (unpack fn)
             then "op"
             else fn

export
makeWith : Name -> String -> String
makeWith n srcline
    = let (markerM, src) = isLitLine srcline
          isrc : (Nat, String) =
             case span isSpace src of
                  (spc, rest) => (length spc, rest)
          indent = fst isrc
          src = snd isrc
          lhs = pack (readLHS 0 (unpack src)) in
          mkWithArg markerM indent lhs ++ "\n" ++
          mkWithPat markerM indent lhs ++ "\n"
  where
    readLHS : (brackets : Nat) -> List Char -> List Char
    readLHS Z ('=' :: rest) = []
    readLHS n ('(' :: rest) = '(' :: readLHS (S n) rest
    readLHS n ('{' :: rest) = '{' :: readLHS (S n) rest
    readLHS n (')' :: rest) = ')' :: readLHS (pred n) rest
    readLHS n ('}' :: rest) = '}' :: readLHS (pred n) rest
    readLHS n (x :: rest) = x :: readLHS n rest
    readLHS n [] = []

    pref : Maybe String -> Nat -> String
    pref mark ind = relit mark $ pack (replicate ind ' ')

    mkWithArg : Maybe String -> Nat -> String -> String
    mkWithArg mark indent lhs
        = pref mark indent ++ lhs ++ "with (_)"

    mkWithPat : Maybe String -> Nat -> String -> String
    mkWithPat mark indent lhs
        = pref mark (indent + 2) ++ lhs ++ "| with_pat = ?" ++
              showRHSName n ++ "_rhs"

export
makeCase : Bool -> Name -> String -> String
makeCase brack n srcline
    = let capp = ("case _ of", "case_val => ?" ++ show n) in
          newLines capp
  where
    addBrackets : Bool -> String -> String
    addBrackets False str = str
    addBrackets True str = "(" ++ str ++ ")"

    addCase : Nat -> (String, String) -> String
    addCase n (c, pat)
        = addBrackets brack $ c ++ "\n" ++
              pack (replicate (n + (if brack then 6 else 5)) ' ') ++ pat

    replaceStr : Nat -> String -> (String, String) -> String -> String
    replaceStr indent rep new "" = ""
    replaceStr indent rep new str
        = if isPrefixOf rep str
             then addCase indent new ++ pack (drop (length rep) (unpack str))
             else assert_total $ strCons (prim__strHead str)
                          (replaceStr (1 + indent) rep new
                                      (prim__strTail str))

    newLines : (String, String) -> String
    newLines capp = replaceStr 0 ("?" ++ show n) capp srcline


text:
> module Isomorphism.Operations

> import Data.Fin
> import Control.Isomorphism

> %default total

> %access public export

> to : {A, B : Type} -> Iso A B -> (A -> B)
> to (MkIso to from toFrom fromTo) = to

> from : {A, B : Type} -> Iso A B -> (B -> A)
> from (MkIso to from toFrom fromTo) = from

> toFrom : {A, B : Type} -> (iso : Iso A B) -> (b : B) -> Isomorphism.Operations.to iso (Isomorphism.Operations.from iso b) = b
> toFrom (MkIso to from toFrom fromTo) = toFrom

> fromTo : {A, B : Type} -> (iso : Iso A B) -> (a : A) -> Isomorphism.Operations.from iso (Isomorphism.Operations.to iso a) = a
> fromTo (MkIso to from toFrom fromTo) = fromTo

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Core.Name.Namespace

import Data.List
import Data.List1
import Data.String
import Decidable.Equality
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Utils.Path

%default total

-------------------------------------------------------------------------------------
-- TYPES
-------------------------------------------------------------------------------------

||| Nested namespaces are stored in reverse order.
||| i.e. `X.Y.Z.foo` will be represented as `NS [Z,Y,X] foo`
||| As a consequence we hide the representation behind an opaque type alias
||| and force users to manufacture and manipulate namespaces via the safe
||| functions we provide.
export
data Namespace : Type where
  MkNS : List String -> Namespace

||| A Module Identifier is, similarly to a namespace, stored inside out.
export
data ModuleIdent : Type where
  MkMI : List String -> ModuleIdent

||| Sometimes we need to convert a module identifier to the corresponding
||| namespace. It is still useful to have them as distinct types as it
||| clarifies the distinct roles of X.Y.Z as a module name vs. S.T.U as a
||| namespace in `import X.Y.Z as S.T.U`.
export
miAsNamespace : ModuleIdent -> Namespace
miAsNamespace (MkMI mi) = MkNS mi

||| Sometimes we need to convert a namespace to the corresponding
||| module identifier. It is still useful to have them as distinct types as
||| it clarifies the distinct roles of X.Y.Z as a module name vs. S.T.U as a
||| namespace in `import X.Y.Z as S.T.U`.
export
nsAsModuleIdent : Namespace -> ModuleIdent
nsAsModuleIdent (MkNS ns) = MkMI ns

-------------------------------------------------------------------------------------
-- SMART CONSTRUCTORS
-------------------------------------------------------------------------------------

export
mkNamespacedIdent : String -> (Maybe Namespace, String)
mkNamespacedIdent str
    = let nns = reverse (split (== '.') str)
          name = head nns
          ns = tail nns in
          case ns of
               [] => (Nothing, name)
               _ => (Just (MkNS ns), name)

export
mkNestedNamespace : Maybe Namespace -> String -> Namespace
mkNestedNamespace Nothing n = MkNS [n]
mkNestedNamespace (Just (MkNS ns)) n = MkNS (n :: ns)

export
mkNamespace : String -> Namespace
mkNamespace ""  = MkNS []
mkNamespace str = uncurry mkNestedNamespace (mkNamespacedIdent str)

export
mkModuleIdent : Maybe Namespace -> String -> ModuleIdent
mkModuleIdent Nothing n = MkMI [n]
mkModuleIdent (Just (MkNS ns)) n = MkMI (n :: ns)

-------------------------------------------------------------------------------------
-- MANIPULATING NAMESPACES
-------------------------------------------------------------------------------------

infixl 5 <.>
||| Extend an existing namespace with additional name parts to form a more local one.
||| e.g. `X.Y.Z <.> S.T.U` to get `X.Y.Z.S.T.U`.
export
(<.>) : (existing, local : Namespace) -> Namespace
(MkNS existing) <.> (MkNS local)
   -- The namespaces are stored in reverse order so the local should end up at
   -- the front of the existing one
   = MkNS (local ++ existing)

export
replace : (old : ModuleIdent) -> (new, ns : Namespace) -> Namespace
replace (MkMI old) (MkNS new) (MkNS ns) = MkNS (go ns) where

  go : List String -> List String
  go [] = []
  go (m :: ms)
        = if old == (m :: ms)
             then new
             else m :: go ms

||| Use at your own risks!
export
unsafeUnfoldNamespace : Namespace -> List String
unsafeUnfoldNamespace (MkNS ns) = ns

export
unsafeFoldNamespace : List String -> Namespace
unsafeFoldNamespace = MkNS

export
unsafeUnfoldModuleIdent : ModuleIdent -> List String
unsafeUnfoldModuleIdent (MkMI ns) = ns

export
unsafeFoldModuleIdent : List String -> ModuleIdent
unsafeFoldModuleIdent = MkMI

namespace ModuleIdent
  ||| A.B.C -> "A/B/C"
  export
  toPath : ModuleIdent -> String
  toPath = joinPath . reverse . unsafeUnfoldModuleIdent

-------------------------------------------------------------------------------------
-- HIERARCHICAL STRUCTURE
-------------------------------------------------------------------------------------

-- We don't use the prefix/suffix terminology as it is confusing: are we talking
-- about the namespaces or their representation? Instead our library is structured
-- around the parent/child relation induced by nested namespaces.

||| Nested namespaces naturally give rise to a hierarchical structure. In particular
||| from a given namespace we can compute all of the parent (aka englobing) ones.
||| For instance `allParents Data.List.Properties` should yield a set containing
||| both `Data.List` and `Data` (no guarantee is given on the order).
export
allParents : Namespace -> List Namespace
allParents (MkNS ns) = go ns where

  go : List String -> List Namespace
  go [] = []
  go (n :: ns) = MkNS (n :: ns) :: go ns

||| We can check whether a given namespace is a parent (aka englobing) namespace
||| of a candidate namespace.
||| We expect that `all (\ p => isParentOf p ns) (allParents ns)` holds true.
export
isParentOf : (given, candidate : Namespace) -> Bool
isParentOf (MkNS ms) (MkNS ns)
  -- This is not a typo: namespaces are stored in reverse order so a namespace is
  -- a prefix of another if its reversed list of identifiers is a suffix of that
  -- other's list of identifiers
  = isSuffixOf ms ns

||| When writing qualified names users often do not want to spell out the full
||| namespace, rightly considering that an unambiguous segment should be enough.
||| This function checks whether a candidate is an approximation of a given
||| namespace.
||| We expect `isApproximationOf List.Properties Data.List.Properties` to hold true
||| while `isApproximationOf Data.List Data.List.Properties` should not.
export
isApproximationOf : (given, candidate : Namespace) -> Bool
isApproximationOf (MkNS ms) (MkNS ns)
  -- This is not a typo: namespaces are stored in reverse order so a namespace matches
  -- the end of another if its representation as a list of identifiers is a prefix of
  -- the other's.
  = isPrefixOf ms ns

-------------------------------------------------------------------------------------
-- INSTANCES
-------------------------------------------------------------------------------------

export
Eq Namespace where
  (MkNS ms) == (MkNS ns) = ms == ns

export
Eq ModuleIdent where
  (MkMI ms) == (MkMI ns) = ms == ns

export
Ord Namespace where
    compare (MkNS ms) (MkNS ns) = compare ms ns

export
Ord ModuleIdent where
    compare (MkMI ms) (MkMI ns) = compare ms ns

mkNSInjective : MkNS ms === MkNS ns -> ms === ns
mkNSInjective Refl = Refl

export
DecEq Namespace where

  decEq (MkNS ms) (MkNS ns) with (decEq ms ns)
    decEq (MkNS ms) (MkNS ns) | No contra = No (contra . mkNSInjective)
    decEq (MkNS ms) (MkNS ns) | Yes eqmsns = Yes (cong MkNS eqmsns)

-- TODO: move somewhere more appropriate
export
showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs

export
showNSWithSep : String -> Namespace -> String
showNSWithSep sep (MkNS ns) = showSep sep (reverse ns)

export
Show Namespace where
  show = showNSWithSep "."

export
Show ModuleIdent where
  show = showNSWithSep "." . miAsNamespace

export
Pretty Namespace where
  pretty (MkNS ns) = concatWith (surround dot) (pretty <$> reverse ns)

export
Pretty ModuleIdent where
  pretty = pretty . miAsNamespace

-------------------------------------------------------------------------------------
-- CONSTANTS
-------------------------------------------------------------------------------------

||| This is used when evaluating things in the REPL
export
emptyNS : Namespace
emptyNS = mkNamespace ""

export
mainNS : Namespace
mainNS = mkNamespace "Main"

export
partialEvalNS : Namespace
partialEvalNS = mkNamespace "_PE"

export
builtinNS : Namespace
builtinNS = mkNamespace "Builtin"

export
preludeNS : Namespace
preludeNS = mkNamespace "Prelude"

export
numNS : Namespace
numNS = mkNamespace "Prelude.Num"

export
typesNS : Namespace
typesNS = mkNamespace "Prelude.Types"

export
basicsNS : Namespace
basicsNS = mkNamespace "Prelude.Basics"

export
eqOrdNS : Namespace
eqOrdNS = mkNamespace "Prelude.EqOrd"

export
primIONS : Namespace
primIONS = mkNamespace "PrimIO"

export
ioNS : Namespace
ioNS = mkNamespace "Prelude.IO"

export
reflectionNS : Namespace
reflectionNS = mkNamespace "Language.Reflection"

export
reflectionTTNS : Namespace
reflectionTTNS = mkNamespace "Language.Reflection.TT"

export
reflectionTTImpNS : Namespace
reflectionTTImpNS = mkNamespace "Language.Reflection.TTImp"

export
dpairNS : Namespace
dpairNS = mkNamespace "Builtin.DPair"

export
natNS : Namespace
natNS = mkNamespace "Data.Nat"


text:
module Stream

import public Stream.File
import public Stream.Internal
import public Stream.Util


text:
module Generics.Newtype.Neg

import Generics.Newtype.Num

import Generics.Derive
%language ElabReflection

--------------------------------------------------------------------------------
--          Neg
--------------------------------------------------------------------------------

public export %hint
NegToNumNP : NP (Neg . f) ks -> NP (Num . f) ks
NegToNumNP = mapNP (\_ => materialize Num)

public export %hint
NegToNumPOP : POP (Neg . f) kss -> POP (Num . f) kss
NegToNumPOP = mapPOP (\_ => materialize Num)

-- Derivation of Neg for n-ary products or newtypes
-- e.g. `(a,b,c)` or `data Foo a = MkFoo a`  or  `data Foo = Foo Int`

-- n-ary products, e.g. (a,b,c)   (data Foo x y = MkFoo x y)
public export
NP (Neg . f) ks => Neg (NP f ks) where
  (-) = hcliftA2 (Neg . f) (-)
  negate = hcliftA (Neg . f) negate

-- This type of deriving is for newtypes so we restrict oursellves to single constructor types.
public export
(all : NP (Neg . f) [k']) => Neg (NS f [k']) where
  (-) {all = _::_} (Z x) (Z y) = Z $ x - y
  negate {all = _::_} (Z x) = Z (negate x)

public export
POP (Neg . f) kss => Neg (POP f kss) where
  (-) = hcliftA2 (Neg . f) (-)
  negate = hcliftA (Neg . f) negate

public export
POP (Neg . f) [ks] => Neg (SOP_ k f [ks]) where
  MkSOP x - MkSOP y = MkSOP $ x - y
  negate (MkSOP n) = MkSOP $ negate n

export
genericNegate : Generic t [code] => POP Neg [code] => t -> t
genericNegate = to . negate . from

export
genericSubtract : Generic t [code] => POP Neg [code] => t -> t -> t
genericSubtract x y = to $ (-) (from x) (from y)

export
||| Derives a `Neg` implementation for the given data type
||| and visibility.
NegVis : Visibility -> DeriveUtil -> InterfaceImpl
NegVis vis g = MkInterfaceImpl "Neg" vis []
                       `(MkNeg genericNegate genericSubtract)
                       (implementationType `(Neg) g)

export
||| Alias for `EncodeVis Public`.
Neg : DeriveUtil -> InterfaceImpl
Neg = NegVis Public


text:
{- 4 -}

my_repl : (prompt : String) ->
          (fn : String -> String) -> IO ()
my_repl prompt fn
   = do putStr prompt
        x <- getLine
        putStr (fn x)
        my_repl prompt fn

my_replWith : (state : a) -> (prompt : String) ->
              (fn : a -> String -> Maybe (String, a)) -> IO ()
my_replWith acc prompt fn
   = do putStr prompt
        x <- getLine
        case fn acc x of
             Just (out, acc') => do putStr out
                                    my_replWith acc' prompt fn
             Nothing => pure ()

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Main

tstr : String
tstr = "abc123"

tlist : List Int
tlist = [1, 2, 3, 4, 5]

main : IO ()
main = do printLn (abs (-8))
          printLn (span isAlpha tstr)
          printLn (break isDigit tstr)
          printLn (span (\x => x < 3) tlist)
          printLn (break (\x => x > 2) tlist)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin