text:
module Idris.IDEMode.CaseSplit

import Core.Context
import Core.Env
import Core.Metadata
import Core.TT
import Core.Value

import Parser.Lexer.Source
import Parser.Unlit

import TTImp.Interactive.CaseSplit
import TTImp.TTImp
import TTImp.Utils

import Idris.IDEMode.TokenLine
import Idris.REPLOpts
import Idris.Resugar
import Idris.Syntax

import Data.List
import Data.List.Extra
import Data.Strings
import System.File

%default covering

||| A series of updates is a mapping from `RawName` to `String`
||| `RawName` is currently just an alias for `String`
||| `String` is a rendered `List SourcePart`
Updates : Type
Updates = List (RawName, String)

||| Convert a RawImp update to a SourcePart one
toStrUpdate : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              (Name, RawImp) -> Core Updates
toStrUpdate (UN n, term)
    = do clause <- pterm term
         pure [(n, show (bracket clause))]
  where
    bracket : PTerm -> PTerm
    bracket tm@(PRef _ _) = tm
    bracket tm@(PList _ _) = tm
    bracket tm@(PPair _ _ _) = tm
    bracket tm@(PUnit _) = tm
    bracket tm@(PComprehension _ _ _) = tm
    bracket tm@(PPrimVal _ _) = tm
    bracket tm = PBracketed emptyFC tm
toStrUpdate _ = pure [] -- can't replace non user names

data UPD : Type where

doUpdates : {auto u : Ref UPD (List String)} ->
            Defs -> Updates -> List SourcePart ->
            Core (List SourcePart)
doUpdates defs ups [] = pure []
doUpdates defs ups (LBrace :: xs)
    = let (ws, nws) = spanSpace xs in map (LBrace :: ws ++) $
         case nws of
           Name n :: RBrace :: rest =>
                pure (Name n ::
                      Whitespace " " :: Equal :: Whitespace " " ::
                      !(doUpdates defs ups (Name n :: RBrace :: rest)))
           Name n :: Equal :: rest =>
                pure (Name n ::
                      Whitespace " " :: Equal :: Whitespace " " ::
                      !(doUpdates defs ups rest))
           _ => doUpdates defs ups xs
  where
    spanSpace : List SourcePart -> (List SourcePart, List SourcePart)
    spanSpace []                   = ([], [])
    spanSpace (RBrace           :: xs) = ([], RBrace :: xs)
    spanSpace (w@(Whitespace _) :: xs) = mapFst (w ::) (spanSpace xs)
    spanSpace (x                :: xs) = map    (x ::) (spanSpace xs)
doUpdates defs ups (Name n :: xs)
    = case lookup n ups of
           Nothing => pure (Name n :: !(doUpdates defs ups xs))
           Just up => pure (Other up :: !(doUpdates defs ups xs))
doUpdates defs ups (HoleName n :: xs)
    = do used <- get UPD
         n' <- uniqueName defs used n
         put UPD (n' :: used)
         pure $ HoleName n' :: !(doUpdates defs ups xs)
doUpdates defs ups (x :: xs)
    = pure $ x :: !(doUpdates defs ups xs)

-- State here is a list of new hole names we generated (so as not to reuse any).
-- Update the token list with the string replacements for each match, and return
-- the newly generated strings.
updateAll : {auto u : Ref UPD (List String)} ->
            Defs -> List SourcePart -> List Updates ->
            Core (List String)
updateAll defs l [] = pure []
updateAll defs l (rs :: rss)
    = do l' <- doUpdates defs rs l
         rss' <- updateAll defs l rss
         pure (concatMap toString l' :: rss')

-- Turn the replacements we got from 'getSplits' into a list of actual string
-- replacements
getReplaces : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto o : Ref ROpts REPLOpts} ->
              List (Name, RawImp) -> Core Updates
getReplaces updates
    = do strups <- traverse toStrUpdate updates
         pure (concat strups)

showImpossible : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 {auto o : Ref ROpts REPLOpts} ->
                 RawImp -> Core String
showImpossible lhs
    = do clause <- pterm lhs
         pure (show clause ++ " impossible")

-- Given a list of updates and a line and column, find the relevant line in
-- the source file and return the lines to replace it with
export
updateCase : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
             {auto o : Ref ROpts REPLOpts} ->
             List ClauseUpdate -> Int -> Int ->
             Core (List String)
updateCase splits line col
    = do opts <- get ROpts
         case mainfile opts of
              Nothing => throw (InternalError "No file loaded")
              Just f =>
                do Right file <- coreLift $ readFile f
                       | Left err => throw (FileErr f err)
                   let thisline = elemAt (lines file) (integerToNat (cast line))
                   case thisline of
                        Nothing => throw (InternalError "File too short!")
                        Just l =>
                            do let valid = mapMaybe getValid splits
                               let bad = mapMaybe getBad splits
                               if isNil valid
                                  then traverse showImpossible bad
                                  else do rs <- traverse getReplaces valid
                                          let stok = tokens l
                                          defs <- get Ctxt
                                          u <- newRef UPD (the (List String) [])
                                          updateAll defs stok rs
  where
    getValid : ClauseUpdate -> Maybe (List (Name, RawImp))
    getValid (Valid _ ups) = Just ups
    getValid _ = Nothing

    getBad : ClauseUpdate -> Maybe RawImp
    getBad (Impossible lhs) = Just lhs
    getBad _ = Nothing

fnName : Bool -> Name -> String
fnName lhs (UN n)
    = if isIdentNormal n then n
      else if lhs then "(" ++ n ++ ")"
      else "op"
fnName lhs (NS _ n) = fnName lhs n
fnName lhs (DN s _) = s
fnName lhs n = nameRoot n

export
getClause : {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto o : Ref ROpts REPLOpts} ->
            Int -> Name -> Core (Maybe String)
getClause l n
    = do defs <- get Ctxt
         Just (loc, nidx, envlen, ty) <- findTyDeclAt (\p, n => onLine (l-1) p)
             | Nothing => pure Nothing
         n <- getFullName nidx
         argns <- getEnvArgNames defs envlen !(nf defs [] ty)
         Just srcLine <- getSourceLine l
           | Nothing => pure Nothing
         let (mark, src) = isLitLine srcLine
         pure (Just (indent mark loc ++ fnName True n ++ concat (map (" " ++) argns) ++
                  " = ?" ++ fnName False n ++ "_rhs"))
  where
    indent : Maybe String -> FC -> String
    indent (Just mark) fc
        = relit (Just mark) $ pack (replicate (integerToNat (cast (max 0 (snd (startPos fc) - 1)))) ' ')
    indent Nothing fc = pack (replicate (integerToNat (cast (snd (startPos fc)))) ' ')


text:
module Main

triples : Int -> List (Int, Int, Int)
triples top = [(x,y,z) | z<-[1..top], y<-[1..z], x<-[1..y],
                         x * x + y * y == z * z ]

main : IO ()
main = do putStrLn "Max: "
          max <- getLine
          printLn (triples (cast max))

ext: idr


text:
module lib.Library2

import lib.Library3
import lib.Library5

export
salute2 : String
salute2 = "Hello, this is Library 2, friend of Library 3 who salutes:\n" ++
          "    " ++ salute3 ++ "\n" ++
          "    and another friend who also salutes:\n" ++
          "    " ++ salute5


text:
module Web.Internal.AnimationPrim

import JS
import Web.Internal.Types

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

namespace Animation

  export
  %foreign "browser:lambda:x=>x.currentTime"
  prim__currentTime : Animation -> PrimIO (Nullable Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.currentTime = v}"
  prim__setCurrentTime : Animation -> Nullable Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.effect"
  prim__effect : Animation -> PrimIO (Nullable AnimationEffect)

  export
  %foreign "browser:lambda:(x,v)=>{x.effect = v}"
  prim__setEffect : Animation -> Nullable AnimationEffect -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.finished"
  prim__finished : Animation -> PrimIO (Promise Animation)

  export
  %foreign "browser:lambda:x=>x.id"
  prim__id : Animation -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.id = v}"
  prim__setId : Animation -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.oncancel"
  prim__oncancel : Animation -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.oncancel = v}"
  prim__setOncancel : Animation -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onfinish"
  prim__onfinish : Animation -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onfinish = v}"
  prim__setOnfinish : Animation -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.pending"
  prim__pending : Animation -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.playState"
  prim__playState : Animation -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.playbackRate"
  prim__playbackRate : Animation -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.playbackRate = v}"
  prim__setPlaybackRate : Animation -> Double -> PrimIO ()

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

  export
  %foreign "browser:lambda:x=>x.startTime"
  prim__startTime : Animation -> PrimIO (Nullable Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.startTime = v}"
  prim__setStartTime : Animation -> Nullable Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.timeline"
  prim__timeline : Animation -> PrimIO (Nullable AnimationTimeline)

  export
  %foreign "browser:lambda:(x,v)=>{x.timeline = v}"
  prim__setTimeline : Animation -> Nullable AnimationTimeline -> PrimIO ()

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

  export
  %foreign "browser:lambda:x=>x.finish()"
  prim__finish : Animation -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.pause()"
  prim__pause : Animation -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.play()"
  prim__play : Animation -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.reverse()"
  prim__reverse : Animation -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.updatePlaybackRate(a)"
  prim__updatePlaybackRate : Animation -> Double -> PrimIO ()

namespace AnimationEffect

  export
  %foreign "browser:lambda:x=>x.getComputedTiming()"
  prim__getComputedTiming : AnimationEffect -> PrimIO ComputedEffectTiming

  export
  %foreign "browser:lambda:x=>x.getTiming()"
  prim__getTiming : AnimationEffect -> PrimIO EffectTiming

  export
  %foreign "browser:lambda:(x,a)=>x.updateTiming(a)"
  prim__updateTiming :  AnimationEffect
                     -> UndefOr OptionalEffectTiming
                     -> PrimIO ()

namespace AnimationPlaybackEvent

  export
  %foreign "browser:lambda:x=>x.currentTime"
  prim__currentTime : AnimationPlaybackEvent -> PrimIO (Nullable Double)

  export
  %foreign "browser:lambda:x=>x.timelineTime"
  prim__timelineTime : AnimationPlaybackEvent -> PrimIO (Nullable Double)

namespace AnimationTimeline

  export
  %foreign "browser:lambda:x=>x.currentTime"
  prim__currentTime : AnimationTimeline -> PrimIO (Nullable Double)

namespace KeyframeEffect

  export
  %foreign "browser:lambda:x=>x.composite"
  prim__composite : KeyframeEffect -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.composite = v}"
  prim__setComposite : KeyframeEffect -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.iterationComposite"
  prim__iterationComposite : KeyframeEffect -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.iterationComposite = v}"
  prim__setIterationComposite : KeyframeEffect -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.target"
  prim__target :  KeyframeEffect
               -> PrimIO (Nullable (Union2 Element CSSPseudoElement))

  export
  %foreign "browser:lambda:(x,v)=>{x.target = v}"
  prim__setTarget :  KeyframeEffect
                  -> Nullable (Union2 Element CSSPseudoElement)
                  -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.getKeyframes()"
  prim__getKeyframes : KeyframeEffect -> PrimIO (Array Object)

  export
  %foreign "browser:lambda:(x,a)=>x.setKeyframes(a)"
  prim__setKeyframes : KeyframeEffect -> Nullable Object -> PrimIO ()

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

namespace Animatable

  export
  %foreign "browser:lambda:(x,a,b)=>x.animate(a,b)"
  prim__animate :  Animatable
                -> Nullable Object
                -> UndefOr (Union2 Double KeyframeAnimationOptions)
                -> PrimIO Animation

  export
  %foreign "browser:lambda:x=>x.getAnimations()"
  prim__getAnimations : Animatable -> PrimIO (Array Animation)

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

namespace AnimationPlaybackEventInit

  export
  %foreign "browser:lambda:(a,b)=> {currentTime: a,timelineTime: b}"
  prim__new :  UndefOr (Nullable Double)
            -> UndefOr (Nullable Double)
            -> PrimIO AnimationPlaybackEventInit

  export
  %foreign "browser:lambda:x=>x.currentTime"
  prim__currentTime :  AnimationPlaybackEventInit
                    -> PrimIO (UndefOr (Nullable Double))

  export
  %foreign "browser:lambda:(x,v)=>{x.currentTime = v}"
  prim__setCurrentTime :  AnimationPlaybackEventInit
                       -> UndefOr (Nullable Double)
                       -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.timelineTime"
  prim__timelineTime :  AnimationPlaybackEventInit
                     -> PrimIO (UndefOr (Nullable Double))

  export
  %foreign "browser:lambda:(x,v)=>{x.timelineTime = v}"
  prim__setTimelineTime :  AnimationPlaybackEventInit
                        -> UndefOr (Nullable Double)
                        -> PrimIO ()

namespace BaseComputedKeyframe

  export
  %foreign "browser:lambda:(a,b,c,d)=> {offset: a,computedOffset: b,easing: c,composite: d}"
  prim__new :  UndefOr (Nullable Double)
            -> UndefOr Double
            -> UndefOr String
            -> UndefOr String
            -> PrimIO BaseComputedKeyframe

  export
  %foreign "browser:lambda:x=>x.composite"
  prim__composite : BaseComputedKeyframe -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.composite = v}"
  prim__setComposite : BaseComputedKeyframe -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.computedOffset"
  prim__computedOffset : BaseComputedKeyframe -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.computedOffset = v}"
  prim__setComputedOffset : BaseComputedKeyframe -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.easing"
  prim__easing : BaseComputedKeyframe -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.easing = v}"
  prim__setEasing : BaseComputedKeyframe -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.offset"
  prim__offset : BaseComputedKeyframe -> PrimIO (UndefOr (Nullable Double))

  export
  %foreign "browser:lambda:(x,v)=>{x.offset = v}"
  prim__setOffset :  BaseComputedKeyframe
                  -> UndefOr (Nullable Double)
                  -> PrimIO ()

namespace BaseKeyframe

  export
  %foreign "browser:lambda:(a,b,c)=> {offset: a,easing: b,composite: c}"
  prim__new :  UndefOr (Nullable Double)
            -> UndefOr String
            -> UndefOr String
            -> PrimIO BaseKeyframe

  export
  %foreign "browser:lambda:x=>x.composite"
  prim__composite : BaseKeyframe -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.composite = v}"
  prim__setComposite : BaseKeyframe -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.easing"
  prim__easing : BaseKeyframe -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.easing = v}"
  prim__setEasing : BaseKeyframe -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.offset"
  prim__offset : BaseKeyframe -> PrimIO (UndefOr (Nullable Double))

  export
  %foreign "browser:lambda:(x,v)=>{x.offset = v}"
  prim__setOffset : BaseKeyframe -> UndefOr (Nullable Double) -> PrimIO ()

namespace BasePropertyIndexedKeyframe

  export
  %foreign "browser:lambda:(a,b,c)=> {offset: a,easing: b,composite: c}"
  prim__new :  UndefOr (Nullable (Union2 Double (Array (Nullable Double))))
            -> UndefOr (Union2 String (Array String))
            -> UndefOr (Union2 String (Array String))
            -> PrimIO BasePropertyIndexedKeyframe

  export
  %foreign "browser:lambda:x=>x.composite"
  prim__composite :  BasePropertyIndexedKeyframe
                  -> PrimIO (UndefOr (Union2 String (Array String)))

  export
  %foreign "browser:lambda:(x,v)=>{x.composite = v}"
  prim__setComposite :  BasePropertyIndexedKeyframe
                     -> UndefOr (Union2 String (Array String))
                     -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.easing"
  prim__easing :  BasePropertyIndexedKeyframe
               -> PrimIO (UndefOr (Union2 String (Array String)))

  export
  %foreign "browser:lambda:(x,v)=>{x.easing = v}"
  prim__setEasing :  BasePropertyIndexedKeyframe
                  -> UndefOr (Union2 String (Array String))
                  -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.offset"
  prim__offset :  BasePropertyIndexedKeyframe
               -> PrimIO (UndefOr (Nullable (Union2 Double
                                                    (Array (Nullable Double)))))

  export
  %foreign "browser:lambda:(x,v)=>{x.offset = v}"
  prim__setOffset :  BasePropertyIndexedKeyframe
                  -> UndefOr (Nullable (Union2 Double
                                               (Array (Nullable Double))))
                  -> PrimIO ()

namespace ComputedEffectTiming

  export
  %foreign "browser:lambda:(a,b,c,d,e)=> {endTime: a,activeDuration: b,localTime: c,progress: d,currentIteration: e}"
  prim__new :  UndefOr Double
            -> UndefOr Double
            -> UndefOr (Nullable Double)
            -> UndefOr (Nullable Double)
            -> UndefOr (Nullable Double)
            -> PrimIO ComputedEffectTiming

  export
  %foreign "browser:lambda:x=>x.activeDuration"
  prim__activeDuration : ComputedEffectTiming -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.activeDuration = v}"
  prim__setActiveDuration : ComputedEffectTiming -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.currentIteration"
  prim__currentIteration :  ComputedEffectTiming
                         -> PrimIO (UndefOr (Nullable Double))

  export
  %foreign "browser:lambda:(x,v)=>{x.currentIteration = v}"
  prim__setCurrentIteration :  ComputedEffectTiming
                            -> UndefOr (Nullable Double)
                            -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.endTime"
  prim__endTime : ComputedEffectTiming -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.endTime = v}"
  prim__setEndTime : ComputedEffectTiming -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.localTime"
  prim__localTime : ComputedEffectTiming -> PrimIO (UndefOr (Nullable Double))

  export
  %foreign "browser:lambda:(x,v)=>{x.localTime = v}"
  prim__setLocalTime :  ComputedEffectTiming
                     -> UndefOr (Nullable Double)
                     -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.progress"
  prim__progress : ComputedEffectTiming -> PrimIO (UndefOr (Nullable Double))

  export
  %foreign "browser:lambda:(x,v)=>{x.progress = v}"
  prim__setProgress :  ComputedEffectTiming
                    -> UndefOr (Nullable Double)
                    -> PrimIO ()

namespace DocumentTimelineOptions

  export
  %foreign "browser:lambda:(a)=> {originTime: a}"
  prim__new : UndefOr Double -> PrimIO DocumentTimelineOptions

  export
  %foreign "browser:lambda:x=>x.originTime"
  prim__originTime : DocumentTimelineOptions -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.originTime = v}"
  prim__setOriginTime : DocumentTimelineOptions -> UndefOr Double -> PrimIO ()

namespace EffectTiming

  export
  %foreign "browser:lambda:(a,b,c,d,e,f,g,h)=> {delay: a,endDelay: b,fill: c,iterationStart: d,iterations: e,duration: f,direction: g,easing: h}"
  prim__new :  UndefOr Double
            -> UndefOr Double
            -> UndefOr String
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr (Union2 Double String)
            -> UndefOr String
            -> UndefOr String
            -> PrimIO EffectTiming

  export
  %foreign "browser:lambda:x=>x.delay"
  prim__delay : EffectTiming -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.delay = v}"
  prim__setDelay : EffectTiming -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.direction"
  prim__direction : EffectTiming -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.direction = v}"
  prim__setDirection : EffectTiming -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.duration"
  prim__duration : EffectTiming -> PrimIO (UndefOr (Union2 Double String))

  export
  %foreign "browser:lambda:(x,v)=>{x.duration = v}"
  prim__setDuration :  EffectTiming
                    -> UndefOr (Union2 Double String)
                    -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.easing"
  prim__easing : EffectTiming -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.easing = v}"
  prim__setEasing : EffectTiming -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.endDelay"
  prim__endDelay : EffectTiming -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.endDelay = v}"
  prim__setEndDelay : EffectTiming -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.fill"
  prim__fill : EffectTiming -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.fill = v}"
  prim__setFill : EffectTiming -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.iterationStart"
  prim__iterationStart : EffectTiming -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.iterationStart = v}"
  prim__setIterationStart : EffectTiming -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.iterations"
  prim__iterations : EffectTiming -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.iterations = v}"
  prim__setIterations : EffectTiming -> UndefOr Double -> PrimIO ()

namespace KeyframeAnimationOptions

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

  export
  %foreign "browser:lambda:x=>x.id"
  prim__id : KeyframeAnimationOptions -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.id = v}"
  prim__setId : KeyframeAnimationOptions -> UndefOr String -> PrimIO ()

namespace KeyframeEffectOptions

  export
  %foreign "browser:lambda:(a,b)=> {iterationComposite: a,composite: b}"
  prim__new : UndefOr String -> UndefOr String -> PrimIO KeyframeEffectOptions

  export
  %foreign "browser:lambda:x=>x.composite"
  prim__composite : KeyframeEffectOptions -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.composite = v}"
  prim__setComposite : KeyframeEffectOptions -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.iterationComposite"
  prim__iterationComposite : KeyframeEffectOptions -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.iterationComposite = v}"
  prim__setIterationComposite :  KeyframeEffectOptions
                              -> UndefOr String
                              -> PrimIO ()

namespace OptionalEffectTiming

  export
  %foreign "browser:lambda:(a,b,c,d,e,f,g,h)=> {delay: a,endDelay: b,fill: c,iterationStart: d,iterations: e,duration: f,direction: g,easing: h}"
  prim__new :  UndefOr Double
            -> UndefOr Double
            -> UndefOr String
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr (Union2 Double String)
            -> UndefOr String
            -> UndefOr String
            -> PrimIO OptionalEffectTiming

  export
  %foreign "browser:lambda:x=>x.delay"
  prim__delay : OptionalEffectTiming -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.delay = v}"
  prim__setDelay : OptionalEffectTiming -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.direction"
  prim__direction : OptionalEffectTiming -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.direction = v}"
  prim__setDirection : OptionalEffectTiming -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.duration"
  prim__duration :  OptionalEffectTiming
                 -> PrimIO (UndefOr (Union2 Double String))

  export
  %foreign "browser:lambda:(x,v)=>{x.duration = v}"
  prim__setDuration :  OptionalEffectTiming
                    -> UndefOr (Union2 Double String)
                    -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.easing"
  prim__easing : OptionalEffectTiming -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.easing = v}"
  prim__setEasing : OptionalEffectTiming -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.endDelay"
  prim__endDelay : OptionalEffectTiming -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.endDelay = v}"
  prim__setEndDelay : OptionalEffectTiming -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.fill"
  prim__fill : OptionalEffectTiming -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.fill = v}"
  prim__setFill : OptionalEffectTiming -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.iterationStart"
  prim__iterationStart : OptionalEffectTiming -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.iterationStart = v}"
  prim__setIterationStart : OptionalEffectTiming -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.iterations"
  prim__iterations : OptionalEffectTiming -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.iterations = v}"
  prim__setIterations : OptionalEffectTiming -> UndefOr Double -> PrimIO ()


text:
||| Utility types and functions for automatically deriving
||| interface instances. So far, this module does not provide
||| deriving functions for existing interfaces. See
||| Doc.Generic4 for examples, how this could be done
||| using the functionality provided here.
module Language.Reflection.Derive

import public Language.Reflection.Syntax
import public Language.Reflection.Types

%language ElabReflection

||| Utility type for deriving interface implementations
||| automatically. See implementations of `Eq'` and `Ord'`
||| in Doc.Generic4 as examples, how this can be done.
public export
record DeriveUtil where
  constructor MkDeriveUtil

  ||| The underlying type info containing the list and names
  ||| of data constructors plus their arguments as well as
  ||| the data type's name and type arguments.
  typeInfo           : ParamTypeInfo

  ||| Fully applied data type, i.e. `var "Either" .$ var "a" .$ var "b"`
  appliedType        : TTImp

  ||| The names of type parameters
  paramNames         : List Name

  ||| Types of constructor arguments where at least one
  ||| type parameter makes an appearance. These are the
  ||| `tpe` fields of `ExplicitArg` where `hasParam`
  ||| is set to true. See the documentation of `ExplicitArg`
  ||| when this is the case
  argTypesWithParams : List TTImp

||| Creates a deriving utility from information about
||| a (possibly) parameterized type.
export
genericUtil : ParamTypeInfo -> DeriveUtil
genericUtil ti = let pNames = map fst $ params ti
                     appTpe = appNames (name ti) pNames
                     twps   = concatMap hasParamTypes ti.cons
                  in MkDeriveUtil ti appTpe pNames twps

||| Generates the name of an interface's implementation function
export
implName : DeriveUtil -> String -> Name
implName g interfaceName =  UN $ "impl" ++ interfaceName
                                        ++ nameStr g.typeInfo.name

||| Syntax tree and additional info about the
||| implementation function of an interface.
|||
||| With 'implementation function', we mean the following:
||| When deriving an interface implementation, the elaborator
||| creates a function returning the corresponding record value.
||| Values of this record should provide both the full type
||| and implementation of this function as `TTImp` values.
|||
||| ```idris exampel
||| public export
||| implEqEither : {0 a : _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b)
||| implEqEither = ?impl
||| ```
public export
record InterfaceImpl where
  constructor MkInterfaceImpl
  ||| The interface's name, for instance "Eq" ord "Ord".
  ||| This is used to generate the name of the
  ||| implementation function.
  interfaceName : String

  ||| Visibility of the implementation function.
  visibility    : Visibility

  ||| Actual implementation of the implementation function.
  ||| This will be the right hand side of the sole pattern clause
  ||| in the function definition.
  |||
  ||| As an example, assume there is a `genEq` function used
  ||| as an implementation for `(==)` for data types with
  ||| some kind of `Generic` instance (see the tutorial on
  ||| Generics for more information about this). An implementation
  ||| for interface `Eq` could then look like this:
  |||
  ||| ```idirs example
  ||| impl = var (singleCon "Eq") .$ `(genEq) .$ `(\a,b => not (a == b))
  ||| ```
  impl          : TTImp

  ||| Full type of the implementation function, including
  ||| implicit arguments (type parameters), which have to be part
  ||| of the `TTImp`.
  |||
  ||| See also `implementationType`, a utility function to create this
  ||| kind of function types for type classes with a single parameter
  ||| of type `Type`.
  |||
  ||| Example:
  |||
  ||| ```idirs example
  ||| `({0 a: _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b))
  ||| ```
  type          : TTImp

private
implDecl : DeriveUtil -> (DeriveUtil -> InterfaceImpl) -> List Decl
implDecl g f = let (MkInterfaceImpl iname vis impl type) = f g
                   function = implName g iname

                in [ interfaceHint vis function type
                   , def function [var function .= impl] ]

private
deriveDecls : Name -> List (DeriveUtil -> InterfaceImpl) -> Elab (List Decl)
deriveDecls name fs = mkDecls <$> getParamInfo' name
  where mkDecls : ParamTypeInfo -> List Decl
        mkDecls pi = let g = genericUtil pi
                      in concatMap (implDecl g) fs

||| Given a name of a data type plus a list of interfaces, tries
||| to implement these interfaces automatically using
||| elaborator reflection.
|||
||| Again, see Doc.Generic4 for a tutorial and examples how
||| to use this.
export
derive : Name -> List (DeriveUtil -> InterfaceImpl) -> Elab ()
derive name fs = do decls <- deriveDecls name fs
                    declare decls

||| Given a `TTImp` representing an interface, generates
||| the type of the implementation function with all type
||| parameters applied and auto implicits specified.
|||
||| Example: Given the `DeriveUtil` info of `Either`, this
||| will generate the following type for input ``(Eq)`:
|||
||| ```idris example
||| {0 a : _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b)
||| ```
|||
||| Note: This function is only to be used with single-parameter
||| type classes, whose type parameters are of type `Type`.
export
implementationType : (iface : TTImp) -> DeriveUtil -> TTImp
implementationType iface (MkDeriveUtil _ appTp names argTypesWithParams) =
  let appIface = iface .$ appTp
      autoArgs = piAllAuto appIface $ map (iface .$) argTypesWithParams
   in piAllImplicit autoArgs names

--------------------------------------------------------------------------------
--          Interface Factories
--------------------------------------------------------------------------------

||| Creates an `Eq` value from the passed implementation functions
||| for (==) and (/=).
export
mkEq' : (eq : a -> a -> Bool) -> (neq : a -> a -> Bool) -> Eq a
mkEq' = %runElab check (var $ singleCon "Eq")

||| Like `mkEq'` but generates (/=) from the passed `eq` function.
export
mkEq : (eq : a -> a -> Bool) -> Eq a
mkEq eq = mkEq' eq (\a,b => not $ eq a b)

||| Creates an `Ord` value from the passed implementation functions
||| for `compare`, `(<)`, `(>)`, `(<=)`, `(>=)`, `min`, `max`.
export
mkOrd' :  (1 _ : Eq a)
      -> (compare : a -> a -> Ordering)
      -> (lt : a -> a -> Bool)
      -> (gt : a -> a -> Bool)
      -> (leq : a -> a -> Bool)
      -> (geq : a -> a -> Bool)
      -> (min : a -> a -> a)
      -> (max : a -> a -> a)
      -> Ord a
mkOrd' = %runElab check (var $ singleCon "Ord")

||| Creates an `Ord` value deriving all functions from the
||| passed `comp` function.
export
mkOrd : (1 prf : Eq a) => (comp : a -> a -> Ordering) -> Ord a
mkOrd comp = mkOrd' prf
                    comp
                    (\a,b => comp a b == LT)
                    (\a,b => comp a b == GT)
                    (\a,b => comp a b /= GT)
                    (\a,b => comp a b /= LT)
                    (\a,b => if comp a b == GT then a else b)
                    (\a,b => if comp a b == LT then a else b)

||| Creates a `Num` value from the passed functions.
export
mkNum :  (plus : a -> a -> a)
      -> (times : a -> a -> a)
      -> (fromInt : Integer -> a)
      -> Num a
mkNum = %runElab check (var $ singleCon "Num")

||| Creates a `Neg` value from the passed functions.
export
mkNeg' :  (1 num : Num a)
      -> (negate : a -> a)
      -> (minus  : a -> a -> a)
      -> Neg a
mkNeg' = %runElab check (var $ singleCon "Neg")

||| Creates a `Neg` value from the passed `minus` function.
export
mkNeg :  (num : Num a) => (minus  : a -> a -> a) -> Neg a
mkNeg minus = mkNeg' num (minus 0) minus

||| Creates an `Abs` value from the passed function
||| and `Num` instance.
export
mkAbs' :  (1 num : Num a) -> (abs : a -> a) -> Abs a
mkAbs' = %runElab check (var $ singleCon "Abs")

||| Creates an `Abs` value from the passed function,
||| using an implicitly passed `Num` instance.
export
mkAbs :  (1 num : Num a) => (abs : a -> a) -> Abs a
mkAbs abs = mkAbs' num abs

||| Creates a `Fractional` value from the passed functions
||| and `Num` instance.
export
mkFractional' :  (1 num : Num a)
              -> (div : a -> a -> a)
              -> (recip : a -> a)
              -> Fractional a
mkFractional' = %runElab check (var $ singleCon "Fractional")

||| Creates a `Fractional` value from the passed function.
export
mkFractional : (num : Num a) => (div : a -> a -> a) -> Fractional a
mkFractional div = mkFractional' num div (div 1)

mkIntegral' :  (1 num : Num a)
            -> (div : a -> a -> a)
            -> (mod : a -> a -> a)
            -> Integral a
mkIntegral' = %runElab check (var $ singleCon "Integral")

||| Creates an `Integral` value from the passed functions.
export
mkIntegral : (1 num : Num a)
           => (div : a -> a -> a)
           -> (mod : a -> a -> a)
           -> Integral a
mkIntegral div mod = mkIntegral' num div mod

||| Creates a `Show` value from the passed functions.
export
mkShow' : (show : a -> String) -> (showPrec : Prec -> a -> String) -> Show a
mkShow' = %runElab check (var $ singleCon "Show")

||| Creates a `Show` value from the passed `show` functions.
export
mkShow : (show : a -> String) -> Show a
mkShow show = mkShow' show (\_ => show)

||| Creates a `Show` value from the passed `showPrec` functions.
export
mkShowPrec : (showPrec : Prec -> a -> String) -> Show a
mkShowPrec showPrec = mkShow' (showPrec Open) showPrec

||| Creates an `Uninhabited` value from the passed function.
export
mkUninhabited : (uninhabited : a -> Void) -> Uninhabited a
mkUninhabited = %runElab check (var $ singleCon "Uninhabited")

||| Creates a `Semigroup` value from the passed function.
export
mkSemigroup : (mappend : a -> a -> a) -> Semigroup a
mkSemigroup = %runElab check (var $ singleCon "Semigroup")

||| Creates a `Monoid` value from the passed neutral value.
mkMonoid' : (1 semi : Semigroup a) -> (neutral : a) -> Monoid a
mkMonoid' = %runElab check (var $ singleCon "Monoid")

||| Creates a `Monoid` value from the passed neutral value.
export
mkMonoid : (1 semi : Semigroup a) => (neutral : a) -> Monoid a
mkMonoid = mkMonoid' semi


text:
module Main

import Data.Vect

%default total

data Store : Type where
  Create : (size : Nat) ->
           (elems : Vect size String) ->
           Store
{-
  Splitting up the Commands for Processing from the strings that represent them
  is what makes easier to isolate parsing and it's failure modes from the
  processing.
-}
data Command = Add String
             | Get Integer
             | Search String
             | Size
             | Quit

size : Store -> Nat
size (Create size' elems') = size'

items : (store : Store) -> Vect (size store) String
items (Create size' elems') = elems'

add : (store : Store) -> String -> Store
add (Create size elems) newElem = Create _ (elems ++ [newElem])

getByIndex : (store : Store) -> (pos : Integer) -> String
getByIndex store pos = case integerToFin pos (size store) of
                            Nothing => "Out of Range"
                            Just pos' => index pos' (items store)

getIndexByElement : (store : Store) -> (el : String) -> String
getIndexByElement store el = case elemIndex el (items store) of
                                 Just i => show (finToNat i)
                                 Nothing => "?"

search : (store : Store) -> (query : String) -> (n : Nat ** Vect n String)
search store query = filter (isInfixOf query) (items store)

formatMatches : (store : Store) -> (results : (n : Nat ** Vect n String)) -> String
formatMatches store (_ ** []) = "No matches\n"
formatMatches store (n ** rs) = foldr (++) "" (map resultToString rs)
  where
    resultToString : String -> String
    resultToString r = (getIndexByElement store r) ++ ": " ++ r ++ "\n"

run : Store -> Command -> Maybe (String, Store)
run store (Search query) = let results = search store query in
                               Just( (formatMatches store results), store )
run store (Add item) = Just ("ID: " ++ show (size store) ++ "\n", add store item)
run store (Get pos) = Just ("Result: " ++ show (getByIndex store pos) ++ "\n", store)
run store Size = Just (show (size store) ++ " item(s)\n", store)
run store Quit = Nothing

cleanInputs : String -> (String, String)
cleanInputs input = case (span (/= ' ') input) of
                         (cmd, args) => (toLower cmd, ltrim args)

parseCommand : (cmd : String) -> (args : String) -> Maybe Command
parseCommand "get" index = case all isDigit (unpack index) of
                                False => Nothing
                                True => Just (Get (cast index))
parseCommand "search" query = Just (Search query)
parseCommand "add" value = Just (Add value)
parseCommand "size" ""  = Just Size
parseCommand "quit" ""  = Just Quit
parseCommand _  _ = Nothing

parse : (input : String) -> Maybe Command
parse input = case cleanInputs input of
                   (cmd, args) => parseCommand cmd args

processInput : Store -> String -> Maybe (String, Store)
processInput store input
= case parse input of
       Just validCommand => run store validCommand
       Nothing => Just ("Invalid command\n", store)

partial main : IO ()
main = replWith (Create _ []) "Command > " processInput

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)
%name Tree tree, tree1

insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node left val right) = case compare x val of
                                      LT => Node (insert x left) val right
                                      EQ => orig
                                      GT => Node left val (insert x right)

{-data BSTree : Type -> Type where
     Empty : Ord elem => BSTree elem
     Node : Ord elem => (left : BSTree elem) -> (val : elem) ->
                        (right : BSTree elem) -> BSTree elem

insert : elem -> BSTree elem -> BSTree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node left val right) = case compare x val of
                                           LT => Node (insert x left) val right
                                           EQ => orig
                                           GT => Node left val (insert x right)
-}

listToTree : Ord a => List a -> Tree a
listToTree [] = Empty
listToTree (x :: xs) = insert x (listToTree xs)

treeToList : Tree a -> List a
treeToList Empty = []
treeToList (Node left x right) = treeToList left ++ [x] ++ treeToList right

data Expr : Type where
     Val : Int -> Expr
     Add : Expr -> Expr -> Expr
     Sub : Expr -> Expr -> Expr
     Mult : Expr -> Expr -> Expr

evaluate : Expr -> Int
evaluate (Val x) = x
evaluate (Add x y) = evaluate x + evaluate y
evaluate (Sub x y) = evaluate x - evaluate y
evaluate (Mult x y) = evaluate x * evaluate y

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing Nothing = Nothing
maxMaybe Nothing (Just x) = Just x
maxMaybe (Just x) Nothing = Just x
maxMaybe (Just x) (Just y) = Just (max x y)


text:
module Sprintf

%access export
%default total

public export
strToSty : (curr : String) -> (str : List Char) -> (t : Type ** t)
strToSty c []             = (_ ** c)
strToSty c ('%'::'%'::ks) = strToSty (c ++ "%") ks
strToSty c ('%'::'d'::ks) = (_ ** \n : Integer => snd $ strToSty (c ++ show n) ks)
strToSty c ('%'::'f'::ks) = (_ ** \x : Double  => snd $ strToSty (c ++ show x) ks)
strToSty c ('%'::'c'::ks) = (_ ** \k : Char    => snd $ strToSty (c ++ singleton k) ks)
strToSty c ('%':: ks)     = (_ ** \v : Void    => snd $ strToSty c ks)
strToSty c ( k :: ks)     = strToSty (c ++ singleton k) ks

sprintf : (str : String) -> fst (strToSty "" $ unpack str)
sprintf str = snd (strToSty "" $ unpack str)

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
-- Tests to check that casting between integer types works as expected
--
-- This tests in `idris2/basic043`, `chez/chez028` and `node/node022` are the
-- same and should all have the same output.

--
-- Widening should not have any effect
--

bits8WideningNoEffect : List String
bits8WideningNoEffect = [
    show $ cast {from = Bits8} {to = Bits16} 123,
    show $ cast {from = Bits8} {to = Bits32} 123,
    show $ cast {from = Bits8} {to = Bits64} 123,
    show $ cast {from = Bits8} {to = Int} 123,
    show $ cast {from = Bits8} {to = Integer} 123
]

bits16WideningNoEffect : List String
bits16WideningNoEffect = [
    show $ cast {from = Bits16} {to = Bits32} 1234,
    show $ cast {from = Bits16} {to = Bits64} 1234,
    show $ cast {from = Bits16} {to = Int} 1234,
    show $ cast {from = Bits16} {to = Integer} 1234
]

bits32WideningNoEffect : List String
bits32WideningNoEffect = [
    show $ cast {from = Bits32} {to = Bits64} 1234567,
    show $ cast {from = Bits32} {to = Int} 1234567,
    show $ cast {from = Bits32} {to = Integer} 1234567
]

--
-- Narrowing
--

b8max : Integer
b8max = 0x100

b16max : Integer
b16max = 0x10000

b32max : Integer
b32max = 0x100000000

b64max : Integer
b64max = 18446744073709551616 -- 0x10000000000000000

narrowFromInteger : List String
narrowFromInteger = [
    show $ cast {from = Integer} {to = Bits8} (b8max + 134),
    show $ cast {from = Integer} {to = Bits16} (b16max + 134),
    show $ cast {from = Integer} {to = Bits32} (b32max + 134),
    show $ cast {from = Integer} {to = Bits64} (b64max + 134)
]

narrowFromInt : List String
narrowFromInt = [
    show $ cast {from = Int} {to = Bits8} (cast (b8max + 134)),
    show $ cast {from = Int} {to = Bits16} (cast (b16max + 134)),
    show $ cast {from = Int} {to = Bits32} (cast (b32max + 134)),
    show $ cast {from = Int} {to = Bits64} (cast (b64max + 134))
]

narrowFromBits64 : List String
narrowFromBits64 = [
    show $ cast {from = Bits64} {to = Bits8} (cast (b8max + 134)),
    show $ cast {from = Bits64} {to = Bits16} (cast (b16max + 134)),
    show $ cast {from = Bits64} {to = Bits32} (cast (b32max + 134))
]

narrowFromBits32 : List String
narrowFromBits32 = [
    show $ cast {from = Bits32} {to = Bits8} (cast (b8max + 134)),
    show $ cast {from = Bits32} {to = Bits16} (cast (b16max + 134))
]

narrowFromBits16 : List String
narrowFromBits16 = [
    show $ cast {from = Bits16} {to = Bits8} (cast (b8max + 134))
]

--
-- Negative numbers
--

negativeNumberCast : List String
negativeNumberCast = [
    show $ cast {to = Bits8} (-19),
    show $ cast {to = Bits16} (-19),
    show $ cast {to = Bits32} (-19),
    show $ cast {to = Bits64} (-19)
]


text:
say : (=) "Hello World!" "Hello World!" -> IO ()
say _ = printLn "Hello World!"

main : IO ()
main = say $ Refl { x = "Hello World!" }

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Bautzen.Network

import Data.List

import Bautzen.SExp
import Bautzen.REPL.SExpParser

||| Returns a decimal string representation of `n` padded with 0s
||| The number must be representable with 6 digits or else it is
||| simply returned as a `String`
||| TODO: make it really total
export
padWith0 : Int -> String
padWith0 k =
  let num = show k
      len = prim__strLength num
  in if len < 6
       then  let padding = Prelude.pack $ replicate (fromInteger $ cast $ 6 - len) '0'
             in padding ++ num
       else num

||| Convert a `SExp` to "wire" format
export
toWire : SExp -> String
toWire sexp =
  let str = show sexp
      len = padWith0 (prim__strLength str)
  in  len ++ str

||| Convert a `String` to a SExp, if possible
export
fromWire : String -> Either String SExp
fromWire = parseSExp

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Extra.OpenSSL.FFI

public export
libcrypto : String -> String
libcrypto func = "C:" <+> func <+> ",libcrypto"


text:
> module NonNegDouble.open_issues.Main

> %default total
> %access public export

> data Positive : Nat -> Type where
>   MkPositive  : {n : Nat} -> Positive (S n)

> PNat : Type
> PNat = Subset Nat Positive

> Fraction : Type
> Fraction = (Nat, PNat)

> data Normal : Fraction -> Type

> NonNegRational : Type
> NonNegRational = Subset Fraction Normal

> plus : NonNegRational -> NonNegRational -> NonNegRational

> mult : NonNegRational -> NonNegRational -> NonNegRational

> fromNat : (n : Nat) -> NonNegRational

> implementation Num NonNegRational where
>   (+) = plus
>   (*) = mult
>   fromInteger = fromNat . fromIntegerNat

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Main

import Data.Vect

||| Verifies that `Fin.restrict` generates a valid `Fin`
||| by using it to index a `Vect`.
main : IO ()
main = do
    let xs = the (Vect 2 Char) ['a','b']
    printLn $ Vect.index (restrict 1 0) xs == 'a'
    printLn $ Vect.index (restrict 1 1) xs == 'b'

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
{--
AoC Utils Module
TODO: move to separate package
--}

module Util
import Data.Vect

public export
fromIntegerNat : Integer -> Nat
fromIntegerNat 0 = Z
fromIntegerNat n =
  if (n > 0) then
    S (fromIntegerNat (assert_smaller n (n - 1)))
  else
    Z

public export
consolidate:  List (Maybe a) -> Maybe (List a)
consolidate []  =  Just []
consolidate (Nothing :: mxs)  =  Nothing
consolidate ((Just x) :: mxs)  =
        case consolidate mxs  of
        		Nothing  =>  Nothing
        		Just xs  =>  Just (x :: xs)


text:
module Toolkit.Data.Location

import Toolkit.Data.Nat

%default total

public export
record Location where
  constructor MkLoc
  source : Maybe String
  line   : Nat
  col    : Nat

public export
record FileContext where
  constructor MkFC
  source : Maybe String
  start  : Location
  end    : Location

public export
record Ref where
  constructor MkRef
  span : FileContext
  get  : String

public export
FC : Type
FC = FileContext

export
newFC : Maybe String -> Location -> Location -> FileContext
newFC n s e = MkFC n (record {source = n} s) (record {source = n} e)

namespace FromCoords
  export
  newLoc : Maybe String -> (Nat, Nat) -> Location
  newLoc n (l,c) = MkLoc n l c

  export
  newFC : Maybe String -> (Nat, Nat) -> (Nat, Nat) -> FileContext
  newFC n s e = newFC n (newLoc n s) (newLoc n e)

  namespace Int
    export
    newLoc : Maybe String -> (Int, Int) -> Location
    newLoc n (l,c) = newLoc n (toNat l, toNat c)

    export
    newFC : Maybe String -> (Int , Int) -> (Int, Int) -> FileContext
    newFC n s e = newFC n (newLoc n s) (newLoc n e)

namespace Anon

  export
  newLoc : (Nat, Nat) -> Location
  newLoc (l,c) = MkLoc Nothing l c

  export
  newFC : Location -> Location -> FileContext
  newFC s e = newFC Nothing s e

export
emptyFC : FileContext
emptyFC = newFC Nothing (Z,Z) (Z,Z)

export
setSource : String -> FileContext -> FileContext
setSource str fc
  = record { source       = Just str
           , start.source = Just str
           , end.source   = Just str
           } fc

namespace Ref

  export
  setSource : String -> Ref -> Ref
  setSource new ref = record {span $= setSource new} ref

export
Show Location where
  show (MkLoc Nothing  l c) = with List concat [show l, ":", show c]
  show (MkLoc (Just n) l c) = with List concat [n, ":", show l, ":", show c]

export
Show FileContext where
  show (MkFC Nothing (MkLoc _ l scol) (MkLoc _ _ ecol)) = with List concat ["global:", show l, ":", show scol, "-", show ecol, ":"]
  show (MkFC (Just x) (MkLoc _ l scol) (MkLoc _ _ ecol)) = with List concat [x, ":", show l, ":", show scol, "-", show ecol, ":"]

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module AutoHotkey.FFI

%default total

mutual
  public export
  data AutoHotkeyFn t = MkAutoHotkeyFn t

  public export
  data AHK_FnTypes : Type -> Type where
    AHK_Fn : AHK_Types s -> AHK_FnTypes t -> AHK_FnTypes (s -> t)
    AHK_FnIO : AHK_Types t -> AHK_FnTypes (IO' l t)
    AHK_FnBase : AHK_Types t -> AHK_FnTypes t

  public export
  data AHK_Types : Type -> Type where
    AHK_Str    : AHK_Types String
    AHK_Int    : AHK_Types Int
    AHK_Float  : AHK_Types Double
    AHK_Unit   : AHK_Types ()
    AHK_Raw    : AHK_Types (Raw a)
    AHK_FnT    : AHK_FnTypes t -> AHK_Types (AutoHotkeyFn t)

  public export
  data AHK_Foreign
    = AHK_DotAccess String String
    | AHK_Command String

  %error_reverse
  public export
  FFI_AHK : FFI
  FFI_AHK = MkFFI AHK_Types AHK_Foreign String

  %error_reverse
  public export
  AHK_IO : Type -> Type
  AHK_IO = IO' FFI_AHK

  IO : Type -> Type
  IO a = IO' FFI_AHK a

max_stars_repo_name: joedf/idris-autohotkey

max_issues_repo_name: joedf/idris-autohotkey

max_forks_repo_name: joedf/idris-autohotkey


text:
plus2 : Nat -> Nat
plus2 = S . S

okplus2Injective : (x, y : Nat) -> Equal (plus2 x) (plus2 y) -> Equal x y
okplus2Injective Z Z Refl = Refl
okplus2Injective (S n) (S n) Refl = Refl
okplus2Injective Z (S _) _ impossible
okplus2Injective (S _) Z _ impossible

badplus2Injective : (x, y : Nat) -> Equal (plus2 x) (plus2 y) -> Equal x y
badplus2Injective Z Z Refl = Refl
badplus2Injective Z (S _) _ impossible
badplus2Injective (S _) Z _ impossible
badplus2Injective (S n) (S n) Refl = Refl


text:
||| This interface enables a clean additive and multiplicative
||| notation.  We add capitalized names because in this package,
||| implicit bounds are usually unwanted.
module Common.Interfaces

%default total
%access public export

||| This is a compromise.  We want the familiar notation (+ and *)
||| without introducing additional ambiguity.  That means extending
||| the existing numerical hierarchy.  But Num bundles additive with
||| multiplicative structure, whereas sometimes only one is relevant.
||| However the more interesting instances are rings anyway, so this
||| is not such a big deal.
interface Neg s => Ringops s where
  Ng : s -> s
  Zero : s
  One : s
  Ng = negate
  Zero = fromInteger 0
  One = fromInteger 1

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module regex

%default total

max_stars_repo_name: asmodehn/o

max_issues_repo_name: asmodehn/o

max_forks_repo_name: asmodehn/o


text:
--
-- A module about shapes
--

||| a Shape
data Shape =
  ||| Triangle with base and heigth
  Triangle Double Double |
  ||| Circle with radius
  Circle Double

||| computes the area of a shape
area : Shape -> Double
area (Triangle x y) = 0.5 * x * y
area (Circle x) = pi * x * x
                  -- pi is known by idris

{-
commented out code
-}


text:
module Language.LSP.CodeAction.MakeCase

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List
import Data.List1
import Data.String
import Idris.IDEMode.CaseSplit
import Idris.IDEMode.MakeClause
import Idris.REPL.Opts
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.Message
import Libraries.Data.List.Extra
import Libraries.Data.PosMap
import Server.Configuration
import Server.Response
import Server.Utils
import Server.Log
import System.File
import TTImp.Interactive.CaseSplit
import TTImp.TTImp

currentLineRange : Int -> String -> Range
currentLineRange i origLine =
  MkRange (MkPosition i 0)
          (MkPosition i (cast $ Prelude.String.length origLine))

export
handleMakeCase : Ref LSPConf LSPConfiguration
         => Ref MD Metadata
         => Ref Ctxt Defs
         => Ref UST UState
         => Ref Syn SyntaxInfo
         => Ref ROpts REPLOpts
         => CodeActionParams -> Core (Maybe CodeAction)
handleMakeCase params = do
  let True = params.range.start.line == params.range.end.line
    | _ => pure Nothing

  [] <- searchCache params.range MakeCase
    | action :: _ => do logString Debug "makeCase: found cached action"
                        pure (Just action)

  meta <- get MD
  let line = params.range.start.line
  let col = params.range.start.character
  let Just (loc, name) = findPointInTreeLoc (line, col) (nameLocMap meta)
    | Nothing =>
        do logString Debug $
             "makeCase: couldn't find name in tree for position (\{show line},\{show col})"
           pure Nothing

  defs <- get Ctxt
  let True = !(isHole defs name) -- should only work on holes
    | _ => do logString Debug $ "makeCase: \(show name) is not a hole"
              pure Nothing

  Just original <- getSourceLine (line + 1)
    | Nothing => do logString Debug $ "caseSplit: error while fetching the referenced line"
                    pure Nothing
  let name' = dropAllNS name
  let newText = makeCase False name' original -- TODO sort out brackets arg
  let rng = currentLineRange line original
  let edit = MkTextEdit rng newText

  let docURI = params.textDocument.uri
  let workspaceEdit = MkWorkspaceEdit
        { changes           = Just (singleton docURI [edit])
        , documentChanges   = Nothing
        , changeAnnotations = Nothing
        }
  let codeAction = MkCodeAction
        { title       = "Make case for hole ?\{show name'}"
        , kind        = Just RefactorRewrite
        , diagnostics = Just []
        , isPreferred = Just False -- not a quickfix
        , disabled    = Nothing
        , edit        = Just workspaceEdit
        , command     = Nothing
        , data_       = Nothing
        }
  modify LSPConf (record { cachedActions $= insert (cast loc, MakeCase, [codeAction]) })
  pure $ Just codeAction
  where
    isHole : Defs -> Name -> Core Bool
    isHole defs n
        = do Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => do pure False
             case definition def of
                  Hole _ _ => pure True
                  _ => pure False


text:
module SimpleCatenableDeque

import CatenableDeque

%default total
%access private

export
data SimpleCatDeque : (Type -> Type) -> Type -> Type where
  Shallow : d a -> SimpleCatDeque d a
  Deep : d a -> Lazy (SimpleCatDeque d (d a)) -> d a -> SimpleCatDeque d a

tooSmall : Deque d => d a -> Bool
tooSmall d = isEmpty d || isEmpty (tail d)

dappendL : Deque d => d a {- tooSmall -} -> d a -> d a
dappendL d1 d2 = if isEmpty d1 then d2 else cons (head d1) d2

dappendR : Deque d => d a -> d a {- tooSmall -} -> d a
dappendR d1 d2 = if isEmpty d2 then d1 else snoc d1 (head d2)

export
Deque d => Deque (SimpleCatDeque d) where
  empty = Shallow empty
  isEmpty (Shallow d) = isEmpty d
  isEmpty _           = False

  cons x (Shallow d)  = Shallow (cons x d)
  cons x (Deep f m r) = Deep (cons x f) m r

  head (Shallow d)  = head d
  head (Deep f m r) = head f

  tail (Shallow d)  = Shallow (tail d)
  tail (Deep f m r) = let f' = tail f in
    if not (tooSmall f') then Deep f' m r
    else if isEmpty m then Shallow (dappendL f' r)
    else Deep (dappendL f' (head m)) (tail m) r

  snoc (Shallow d) x  = Shallow (snoc d x)
  snoc (Deep f m r) x = Deep f m (snoc r x)

  last (Shallow d)  = last d
  last (Deep f m r) = last r

  init (Shallow d) = Shallow (init d)
  init (Deep f m r) = let r' = init r in
    if not (tooSmall r') then Deep f m r'
    else if isEmpty m then Shallow (dappendR f r')
    else Deep f (init m) (dappendR (last m) r')

export
Deque d => CatenableDeque (SimpleCatDeque d) where
  (Shallow d1) ++ (Shallow d2) =
    if tooSmall d1 then Shallow (dappendL d1 d2)
    else if tooSmall d2 then Shallow (dappendR d1 d2)
    else Deep d1 empty d2
  (Shallow d) ++ (Deep f m r) =
    if tooSmall d then Deep (dappendL d f) m r
    else Deep d (cons f m) r
  (Deep f m r) ++ (Shallow d) =
    if tooSmall d then Deep f m (dappendR r d)
    else Deep f (snoc m r) d
  (Deep f1 m1 r1) ++ (Deep f2 m2 r2) =
    let mf = assert_smaller (Deep f1 m1 r2) $ snoc m1 r1
        mr = assert_smaller (Deep f2 m2 r2) $ cons f2 m2
    in Deep f1 (mf ++ mr) r2


text:
module MacroDef

import Tokenizer

%default total
%access public export

record MacroDef where
  constructor Define
  name : String
  params : List String
  body : List String

data ParseOneState
  = NeedBegin
  | NeedEnd MacroHeader (List String)

ParseState : Type
ParseState = (ParseOneState, List MacroDef)

parseMacroDefs' : ParseState -> List String -> List MacroDef
parseMacroDefs' (NeedBegin, macros) [] = macros
parseMacroDefs' (NeedBegin, macros) (x :: xs) =
  case parseHeaderTok "define" x of
    Nothing => parseMacroDefs' (NeedBegin, macros) xs
    Just hd => parseMacroDefs' (NeedEnd hd [], macros) xs
parseMacroDefs' (NeedEnd _ _, macros) [] = macros
parseMacroDefs' (NeedEnd header body, macros) (x :: xs) =
  case parseFooter "def" x of
    False => parseMacroDefs' (NeedEnd header (x :: body), macros) xs
    True  => parseMacroDefs' (NeedBegin, Define (name header) (params header) body :: macros) xs

parseMacroDefs : List String -> List MacroDef
parseMacroDefs = parseMacroDefs' (NeedBegin, [])

max_stars_repo_name: Kazark/fspp

max_issues_repo_name: Kazark/fspp

max_forks_repo_name: Kazark/fspp


text:
import RealizedFunction

%default total

-- Realized incrementer
incrementer : Int -> Int
incrementer = (+1)
incrementer_attrs : RealizedAttributes
incrementer_attrs = RealizedAttributes (MkCosts 100 10 1) 1
rlz_incrementer : SimpleRealizedFunction (Int -> Int) incrementer_attrs
rlz_incrementer = MkSimpleRealizedFunction incrementer incrementer_attrs

-- Realized twicer
twicer : Int -> Int
twicer = (*2)
twicer_attrs = MkNonDTRealizedAttributes (MkCosts 200 20 2) 0.9
rlz_twicer : SimpleRealizedFunction (Int -> Int) twicer_attrs
rlz_twicer = MkSimpleRealizedFunction twicer twicer_attrs

-- Realized (twicer . incrementer).
rlz_composition_attrs = MkRealizedAttributes (MkCosts 300 30 3) 0.9
rlz_composition : RealizedFunction (Int -> Int) rlz_composition_attrs
rlz_composition = compose rlz_twicer rlz_incrementer

-- Simple test, result should be (3+1)*2 = 8
rslt : Int
rslt = apply rlz_composition 3

rsltTest : (rslt 3) = 8
rsltTest = Refl

max_stars_repo_name: sroberti/ai-dsl

max_issues_repo_name: sroberti/ai-dsl

max_forks_repo_name: sroberti/ai-dsl


text:
module Control.Effect.NonDet

import Control.EffectAlgebra

import Control.Monad.List

import Data.List1

||| Add non-determinism to a computation,
||| e.i. alternatives for program flow.
||| Choice between these alternatives is not directly specified and is
||| deferred to a particular handler.
public export
data ChoiceE : (Type -> Type) -> (Type -> Type) where
  Choose : List (m a) -> ChoiceE m a

namespace Algebra
  alg :   Algebra sig m
       => (f : Functor ctx)
       => ctx ()
       -> Handler ctx n (ListT m)
     -> (ChoiceE :+: sig) n a
     -> (ListT m) (ctx a)
  alg ctxx hdl (Inl (Choose list)) =
    go list
   where
    go : List (n a) -> ListT m (ctx a)
    go [] = pure []
    go (x :: xs) = (<+>) @{ListT} (hdl (x <$ ctxx)) (go xs)
  alg ctxx hdl (Inr other) =
    -- hdl : Handler ctx n (ListT m)
    -- hdl' : Handler (List m) (ListT m) m
    -- ? : Handler (List m . ctx) n m
    EffectAlgebra.alg {f = Functor.Compose @{(ListM, %search)}}
        {ctx = ListM m . ctx}
        {m} (ctxx :: pure [])
        ((~<~) @{%search} @{Functor.ListM} { ctx1 = ListM m
               , ctx2 = ctx
               , l = n
               , m = ListT m
               , n = m} f hdl) other
   where
    f : Handler (ListM m) (ListT m) m
    f = join @{Monad.ListT} . pure

  ||| Handle choice by accumulating all alternatives in a list transformer.
  %hint export
  Concat : (al : Algebra sig m) => Algebra (ChoiceE :+: sig) (ListT m)
  Concat = MkAlgebra @{Monad.ListT} Algebra.alg

||| Introduce non-deterministic branching to a computation.
public export
oneOf : Inj ChoiceE sig
     => Algebra sig m
     => List a
     -> m a
oneOf list =
  send (Choose (map pure list))

||| Introduce non-deterministic branching to a computation.
public export
oneOfM : Inj ChoiceE sig
     => Algebra sig m
     => List (m a)
     -> m a
oneOfM list =
  send (Choose list)


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

%name Vect xs, ys, zs

zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith f [] [] = []
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys


text:
-- --------------------------------------------------------------- [ DList.idr ]
-- Module    : DList.idr
-- Copyright : (c) 2015,2016,2017, 2020 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| A `list` construct to create lists of dependent types.
|||
||| One of the problems with using dependent types is that types
||| depend on values. This affects the ability to construct lists of
||| values that have a dependent type. The existing `List` type cannot
||| be used as it requires all elements to have the same type.
module Toolkit.Data.DList

import        Data.String
import public Data.List
import public Data.List.Elem

||| A list construct for dependent types.
|||
||| @aTy    The type of the value contained within the list element type.
||| @elemTy The type of the elements within the list
||| @as     The List used to contain the different values within the type.
public export
data DList : (aTy : Type)
          -> (elemTy : aTy -> Type)
          -> (as : List aTy)
          -> Type where
  ||| Create an empty List
  Nil  : DList aTy elemTy Nil
  ||| Cons
  |||
  ||| @elem The element to add
  ||| @rest The list for `elem` to be added to.
  (::) : {x : aTy}
      -> (elem : elemTy x)
      -> (rest : DList aTy elemTy xs)
      -> DList aTy elemTy (x::xs)

public export
mapToList : (forall x . e x -> b)
         -> DList a e xs
         -> List b
mapToList _ Nil = Nil
mapToList f (x::xs) = f x :: mapToList f xs

||| Function to show a `DList`.
|||
||| Due to limitations in idris wrt to class instances on dependent
||| types a generic show instance cannot be defined for
||| sigmalist. This will cause minor annoyances in its use.
|||
||| @showFunc A function to show the elements
||| @l       The list to be Shown.
public export
showDList : (showFunc : forall a . elemTy a -> String)
         -> (l : DList aTy elemTy as)
         -> String
showDList f xs = "[" ++ unwords (intersperse "," (mapToList f xs)) ++ "]"

namespace Alt
  public export
  index : (xs  : DList iTy eTy is)
       -> (idx : Elem i is)
       -> eTy i
  index (ex :: rest) Here = ex
  index (ex :: rest) (There later) = index rest later

  public export
  update : (vs  : DList iTy eTy is)
        -> (idx : Elem i is)
        -> (new : eTy i)
        -> DList iTy eTy is
  update (ex :: rest) Here new = new :: rest
  update (ex :: rest) (There later) new = ex :: update rest later new

  public export
  updateWith : DList iTy eTy is
            -> Elem i is
            -> (eTy i -> eTy i)
            -> DList iTy eTy is
  updateWith (ex :: rest) Here f = f ex :: rest
  updateWith (ex :: rest) (There later) f = ex :: updateWith rest later f

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

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Physics.Box2D.Definition

import Physics.Vector2D
import Physics.Box2D.Defaults

%default total

-- Maybe values usually indicate optional parameters

public export
data Body = MkBody Ptr
public export
data Fixture = MkFixture Ptr
public export
data Joint = MkJoint Ptr

public export
data BodyType = Static | Dynamic | Kinematic

export
Eq BodyType where
  Static == Static = True
  Dynamic == Dynamic = True
  Kinematic == Kinematic = True
  _ == _ = False

public export
record BodyDefinition where
  constructor MkBodyDefinition
  type : BodyType
  position : Vector2D
  angle : Maybe Double
  fixedRotation : Maybe Bool
  bullet : Maybe Bool
%name BodyDefinition bodyDef

export
Show BodyType where
  show Static = "static"
  show Dynamic = "dynamics"
  show Kinematic = "kinematic"

public export
data Shape = Circle Double
           | Box Vector2D
           | Polygon (List Vector2D)
           | Chain (List Vector2D)
%name Shape shape

export
Show Shape where
  show (Circle x) = "circle " ++ show x
  show (Box x) = "box " ++ show x
  show (Polygon xs) = "polygon " ++ show xs
  show (Chain xs) = "chain " ++ show xs

public export
record FixtureDefinition where
  constructor MkFixtureDefinition
  shape : Shape
  offset : Maybe Vector2D
  angle : Maybe Double
  density : Maybe Double
  friction : Maybe Double
  restitution : Maybe Double
  groupIndex : Maybe Int
  categoryBits : Maybe Int
  maskBits : Maybe Int
  name : Maybe String
%name FixtureDefinition fixtureDef

export
Show FixtureDefinition where
  show fd
    =  "{ shape: " ++ show (shape fd)
    ++ ", offset: " ++ show (offset fd)
    ++ ", angle: " ++ show (angle fd)
    ++ ", density: " ++ show (density fd)
    ++ ", friction: " ++ show (friction fd)
    ++ ", restitution: " ++ show (restitution fd)
    ++ ", group index: " ++ show (groupIndex fd)
    ++ ", category bits: " ++ show (categoryBits fd)
    ++ ", mask bits: " ++ show (maskBits fd)
    ++ ", name: " ++ show (name fd)
    ++ " }"

export
defaultFixture : Shape -> FixtureDefinition
defaultFixture shape
  = MkFixtureDefinition shape Nothing Nothing Nothing Nothing Nothing Nothing
                        Nothing Nothing Nothing

public export
record RevoluteJointDefinition where
  constructor MkRevoluteJointDefinition
  bodyA : Body
  localAnchorA : Vector2D
  bodyB : Body
  localAnchorB : Vector2D
  collideConnected : Maybe Bool


text:
module Minecraft.Base.PreClassic.Stone.ItemEntity.Export

import public Minecraft.Core.Entity.Export
import public Minecraft.Base.PreClassic.Stone.Item
import public Minecraft.Base.PreClassic.Stone.ItemEntity

%default total

[stoneItemEntity']
Pickup Stone.ItemEntity where
  collect self = new Stone.Item self.base.item

[stoneVtbl']
Vtbl Stone.ItemEntity where
  vtable (Pickup   Stone.ItemEntity) = Just stoneItemEntity
  vtable (Entity   Stone.ItemEntity) = Just %search
  vtable (Tangible Stone.ItemEntity) = Just %search
  vtable _ = Nothing

stoneItemEntity = stoneItemEntity'
stoneVtbl = stoneVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module JS.Inheritance

import Control.Monad.Either
import JS.Util
import Data.List.Elem
import Data.String
import Data.SOP

--------------------------------------------------------------------------------
--          Upcasting
--------------------------------------------------------------------------------

||| A `JSType` describes a type's inheritance chains and implemented
||| mixins. It is used to safely and conveniently cast a value to a
||| less specific type mentioned either in the list of
||| mixins or parent types by means of funciton `up` and operator `:>`.
public export
interface JSType a where

  ||| The inheritance chain of parent types of this data type
  ||| (starting at the direct supertype). At runtime, such an inheritance
  ||| chain can be inspected by recursively calling the Javascript
  ||| function `Object.getPrototypeOf`.
  parents : List Type

  ||| A Mixin is a concept from WebIDL: It is as programming interface
  ||| shared by several types. Unlike a WebIDL interface, a mixin does
  ||| not describe a type but just set of shared functions and
  ||| attributes. Mixins are not observable by means of inspecting
  ||| a value's prototype chain. It is therefore much harder
  ||| (and right now not supported in this library) to at runtime
  ||| check, whether a value implements a given mixin.
  mixins : List Type

||| Convenience alias for `parents`, which takes an explicit
||| erased type argument.
public export
0 Types : (0 a : Type) -> JSType a => List Type
Types a = a :: parents {a} ++ mixins {a}

||| Safe upcasting. This uses `believe_me` internally and is
||| therefore of course only safe, if the `JSType` implementation
||| is correct according to some specification and the backend
||| properly adhere to this specification.
public export %inline
up : (0 _ : JSType a) => a -> {auto 0 _ : Elem b (Types a)} -> b
up v = believe_me v

infixl 1 :>

||| Operator version of `up`.
public export %inline
(:>) : (0 _ : JSType a) => a -> (0 b : Type) -> {auto 0 _ : Elem b (Types a)} -> b
a :> _ = up a

--------------------------------------------------------------------------------
--          Downcasting
--------------------------------------------------------------------------------

%foreign #"""
         javascript:lambda:(s,v)=>{
         var o = v;
           while (o != null) {
             var p = Object.getPrototypeOf(o);
             var cn = p.constructor.name;
             if (cn === s) {
               return 1;
             } else if (cn === "Object") {
               return 0;
             }
             o = p;
           }
           return 0;
         }
         """#
prim__hasProtoName : String -> AnyPtr -> Double

||| This is an interface which should be implemented by external
||| types, the type of which can be inspected at runtime.
|||
||| This allows us to at runtime try and safely cast any value
||| to the type implementing this interface.
|||
||| Typically, there are two mechanisms for inspecting a value's
||| type at runtime: Function `typeof`, which is mainly useful
||| for primitives, and function `unsafeCastOnPrototypeName`, which
||| inspects a value's prototype chain
||| ([see also](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Inheritance_and_the_prototype_chain)).
|||
||| Note, that the intention of this interface is to use it
||| on *external* types and *primitives*, but not on types
||| defined in Idris2. If you need to marshal Idris2 values
||| from and to the FFI, use interfaces `ToJS` and `FromJS`.
public export
interface SafeCast a where
  safeCast : {0 x : Type} -> x -> Maybe a

public export %inline
castTo : (0 a : Type) -> SafeCast a => x -> Maybe a
castTo _ v = safeCast v

||| Tries to create an n-ary sum by trying all possible
||| casts. The first successful cast will determine the
||| result.
export
safeCastNS : (np : NP SafeCast ts) => x -> Maybe (NS I ts)
safeCastNS x = choiceMap runNS $ apInjsNP np
  where runNS : NS SafeCast ts -> Maybe (NS I ts)
        runNS = htraverse (\sc => safeCast x)

||| This is a utility function to implement instances of
||| `SafeCast`. Only use, if you know what you are doing.
export
unsafeCastOnPrototypeName : String -> a -> Maybe b
unsafeCastOnPrototypeName s a =
  if prim__hasProtoName s (believe_me a) == 1.0
     then Just (believe_me a)
     else Nothing

||| This is a utility function to implement instances of
||| `SafeCast`. Only use, if you know what you are doing.
export
unsafeCastOnTypeof : String -> a -> Maybe b
unsafeCastOnTypeof s a =
  if typeof a == s then Just (believe_me a) else Nothing

export
SafeCast Integer where
  safeCast = unsafeCastOnTypeof "bigint"

export
SafeCast Double where
  safeCast = unsafeCastOnTypeof "number"

export
SafeCast String where
  safeCast = unsafeCastOnTypeof "string"

-- As far as I understand, there are no "single characters"
-- in Javascript, only strings of length 1. Thats why we go via
-- String here
export
SafeCast Char where
  safeCast v = safeCast v >>= \s => case strM s of
                                         StrCons x "" => Just x
                                         _            => Nothing

export
bounded : Num a => (min : Integer) -> (max : Integer) -> x -> Maybe a
bounded min max ptr =
  safeCast ptr >>= \n => if n >= min && n <= max
                            then Just (fromInteger n)
                            else Nothing

export
SafeCast Bits8 where
  safeCast = bounded 0 0xff

export
SafeCast Bits16 where
  safeCast = bounded 0 0xffff

export
SafeCast Bits32 where
  safeCast = bounded 0 0xffffffff

export
SafeCast Bits64 where
  safeCast = bounded 0 0xffffffffffffffff

export
SafeCast Int8 where
  safeCast = bounded (-0x80) 0x7f

export
SafeCast Int16 where
  safeCast = bounded (-0x8000) 0x7fff

export
SafeCast Int32 where
  safeCast = bounded (-0x80000000) 0x7fffffff

export
SafeCast Int64 where
  safeCast = bounded (-0x8000000000000000) 0x7fffffffffffffff

export
SafeCast Int where
  safeCast = bounded (- 0x80000000) (0x7fffffff)

export
tryCast : SafeCast a => (fun : Lazy String) -> x -> JSIO a
tryCast fun val = case safeCast val of
                       Just a  => pure a
                       Nothing => throwError $ CastErr fun val

export
tryCast_ : (0 a : Type) -> SafeCast a => (fun : Lazy String) -> x -> JSIO a
tryCast_ _ = tryCast

export
castingTo : SafeCast a => (fun : String) -> JSIO x -> JSIO a
castingTo fun io = io >>= tryCast fun


text:
module Data.Time.Calendar.Month

import public Data.Time.Calendar.Types
import Data.Time.Calendar.Days
import Data.Time.Calendar.Gregorian
import Text.Format.Decimal

import Generics.Derive

%default total
%language ElabReflection

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

||| An absolute count of common calendar months.
||| Number is equal to @(year * 12) + (monthOfYear - 1)@.
export data Month = MkMonth Integer

public export Cast Month Integer where cast (MkMonth x) = x
public export Cast Integer Month where cast = MkMonth

%runElab derive "Month" [Generic, Meta, Eq, Ord]

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

export addMonths : Integer -> Month -> Month
addMonths n (MkMonth x) = MkMonth $ x + n

export diffMonths : Month -> Month -> Integer
diffMonths (MkMonth x) (MkMonth y) = x - y

export toYearMonth : Month -> (Year, MonthOfYear)
toYearMonth (MkMonth x) =
  let y = x `div` 12
      m = cast $ x `mod` 12
    in (y, m + 1)

export fromYearMonth : Year -> MonthOfYear -> Month
fromYearMonth y m =
 let m' = the Int $ if m < 1 then 1 else if m > 12 then 12 else m
  in MkMonth $ y * 12 + cast (m' - 1)

export fromYearMonthValid : Year -> MonthOfYear -> Maybe Month
fromYearMonthValid y m =
  if m < 1 || m > 12 then Nothing
  else Just $ MkMonth $ y * 12 + cast (m - 1)

export toMonthDay : Day -> (Month, DayOfMonth)
toMonthDay d = let
  (y, m, d) = toGregorian d
  in (MkMonth (y * 12 + cast (max 0 $ min 11 m)), d)

export fromMonth : Month -> DayOfMonth -> Day
fromMonth m dm = let
  (y, my) = toYearMonth m
  in fromGregorian y my dm

export fromMonthDayValid : Month -> DayOfMonth -> Maybe Day
fromMonthDayValid m dm = let
  (y, my) = toYearMonth m
  in fromGregorianValid y my dm

public export
Show Month where
  show m = let
    (y, my) = toYearMonth m
    in format' (record { width = Just 4, pad = Just '0' }) y
       ++ format' (record { width = Just 2, pad = Just '0' }) my

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


text:
-- run as: $ idris2 -p calc CalcClient.idr

module Main

import Data.Strings

import Calc.Add
import Calc.Sub
import Calc.Mul
import Calc.Div

readNum : HasIO io => io (Maybe Int)
readNum = do putStr "Enter a number: "
             ns <- getLine
             case all isDigit (unpack ns) of
                  False => pure Nothing
                  True => pure $ Just (cast ns)

main : HasIO io => io ()
main = do Just n <- readNum
            | Nothing => do putStrLn "First number is invalid"
          Just m <- readNum
            | Nothing => do putStrLn "Second number is invalid"
          let sum = add n m
          let diff = subtract n m
          let prod = multiply n m
          let quot = divide n m
          putStrLn $ "Sum = " ++ show sum ++ " , difference = " ++ show diff
                    ++ ", product = " ++ show prod ++ ", quotient = " ++ show quot

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

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

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


text:
> module Vect.Operations

> import Data.Vect
> import Data.Fin
> import Data.So

> import Decidable.Predicates
> import Rel.TotalPreorder
> import Rel.TotalPreorderOperations
> import Nat.LTProperties
> import Sigma.Sigma

> %default total
> %access public export
> %auto_implicits on

Lookup

> ||| Lookup the index of an element of a vector
> lookup : {A : Type} -> .(a : A) -> .(as : Vect n A) -> Elem a as -> Fin n
> lookup {n = Z}   a  Nil        Here         impossible
> lookup {n = Z}   a  Nil       (There p)     impossible
> lookup {n = S m} a (a :: as)   Here       = FZ
> lookup {n = S m} a (a' :: as) (There prf) = FS (lookup a as prf)

> ||| Lookup the index of an element of a vector
> -- lookup' : {n : Nat} -> {A : Type} -> (DecEq A) => (a : A) -> (as : Vect n A) -> Maybe (Fin n)
> lookup' : {n : Nat} -> {A : Type} -> (DecEq A) -> (a : A) -> (as : Vect n A) -> Maybe (Fin n)
> lookup' {n = Z}   _ _  Nil        = Nothing
> lookup' {n = S m} d a  (a' :: as) with (decEq a a')
>   | (Yes _) = Just FZ
>   | (No  _) with (lookup' d a as)
>     | Nothing  = Nothing
>     | (Just k) = Just (FS k)

Container monad operations

...

Filtering

> ||| Filters a vector on a decidable property
> filter : {A : Type} ->
>          {P : A -> Type} ->
>          Dec1 P ->
>          Vect n A ->
>          Sigma Nat (\ m => Vect m A)
> filter d1P Nil = MkSigma Z Nil
> filter d1P (a :: as) with (filter d1P as)
>   | (MkSigma n as') with (d1P a)
>     | (Yes _) = MkSigma (S n) (a :: as')
>     | (No  _) = MkSigma n as'

> ||| Filters a vector on a decidable property and pairs elements with proofs
> filterTagSigma : {A : Type} ->
>                  {P : A -> Type} ->
>                  Dec1 P ->
>                  Vect n A ->
>                  Sigma Nat (\ m => Vect m (Sigma A P))
> filterTagSigma d1P Nil = MkSigma _ Nil
> filterTagSigma d1P (a :: as) with (filterTagSigma d1P as)
>   | (MkSigma _ tail) with (d1P a)
>     | (Yes p) = MkSigma _ ((MkSigma a p) :: tail)
>     | (No  _) = MkSigma _ tail

> ||| Filters a vector on a decidable property and pairs elements with proofs
> filterTagExists : {A : Type} ->
>                   {P : A -> Type} ->
>                   Dec1 P ->
>                   Vect n A ->
>                   Sigma Nat (\ m => Vect m (Exists {a = A} P))
> filterTagExists d1P Nil = MkSigma _ Nil
> filterTagExists d1P (a :: as) with (filterTagExists d1P as)
>   | (MkSigma _ tail) with (d1P a)
>     | (Yes p) = MkSigma _ ((Evidence a p) :: tail)
>     | (No  _) = MkSigma _ tail

> ||| Filters a vector on a decidable property and pairs elements with proofs
> filterTagSubset : {A : Type} ->
>                   {P : A -> Type} ->
>                   Dec1 P ->
>                   Vect n A ->
>                   Sigma Nat (\ m => Vect m (Subset A P))
> filterTagSubset d1P Nil = MkSigma _ Nil
> filterTagSubset d1P (a :: as) with (filterTagSubset d1P as)
>   | (MkSigma _ tail) with (d1P a)
>     | (Yes p) = MkSigma _ ((Element a p) :: tail)
>     | (No  _) = MkSigma _ tail

Searching

> |||
> argmaxMax : {A : Type} -> {R : A -> A -> Type} ->
>             TotalPreorder R -> Vect n A -> .(LT Z n) -> (Fin n, A)
> argmaxMax {n = Z}       tp  Nil                p = absurd p
> argmaxMax {n = S Z}     tp (a :: Nil)          _ = (FZ, a)
> argmaxMax {n = S (S m)} tp (a' :: (a'' :: as)) _ with (argmaxMax tp (a'' :: as) (ltZS m))
>   | (k, max) with (totalPre tp a' max)
>     | (Left  _) = (FS k, max)
>     | (Right _) = (FZ, a')

> |||
> argmax : {A : Type} -> {R : A -> A -> Type} ->
>          TotalPreorder R -> Vect n A -> .(LT Z n) -> Fin n
> argmax tp as p = fst (argmaxMax tp as p)

> |||
> max : {A : Type} -> {R : A -> A -> Type} ->
>       TotalPreorder R -> Vect n A -> .(LT Z n) -> A
> max tp as p = snd (argmaxMax tp as p)

> {-

> |||
> argmaxMax : {A : Type} ->
>             TotalPreorder A -> Vect n A -> .(LT Z n) -> (Fin n, A)
> argmaxMax {n = Z}       tp  Nil                p = absurd p
> argmaxMax {n = S Z}     tp (a :: Nil)          _ = (FZ, a)
> argmaxMax {n = S (S m)} tp (a' :: (a'' :: as)) _ with (argmaxMax tp (a'' :: as) (ltZS m))
>   | (k, max) with (totalPre tp a' max)
>     | (Left  _) = (FS k, max)
>     | (Right _) = (FZ, a')

> |||
> argmax : {A : Type} ->
>          TotalPreorder A -> Vect n A -> .(LT Z n) -> Fin n
> argmax tp as p = fst (argmaxMax tp as p)

> |||
> max : {A : Type} ->
>       TotalPreorder A -> Vect n A -> .(LT Z n) -> A
> max tp as p = snd (argmaxMax tp as p)

> -}

Show

> implementation Show (Elem a as) where
>   show = show' where
>     show' : {n : Nat} -> {A : Type} -> {a : A} -> {as : Vect n A} -> Elem a as -> String
>     show'  Here     = "Here"
>     show' (There p) = "There" ++ show' p

Pointwise modify

> |||
> modifyVect : {n : Nat} -> {a : Type} ->
>              Vect n a -> Fin n -> a -> Vect n a
> modifyVect {n = Z}    Nil          k  _  = absurd k
> modifyVect {n = S m} (a :: as)  FZ    a' = a' :: as
> modifyVect {n = S m} (a :: as) (FS k) a' = a :: (modifyVect as k a')

Fold:

data Vect : Nat -> Type -> Type where
  Nil : Vect Z A
  Cons : A -> Vect n A -> Vect (S n) A

x0 : X 0
f  : A -> X n -> X (S n)

> foldVect : {X : Nat -> Type} ->
>            {A : Type} ->
>            X 0 ->
>            ((n : Nat) -> A -> X n -> X (S n)) ->
>            Vect n A ->
>            X n
> foldVect {n = Z} x0 f Nil = x0
> foldVect {n = S m} x0 f (a :: as) = f m a (foldVect x0 f as)

> {-

> |||
> argmaxMax : {A : Type} -> {TO : A -> A -> Type} -> Preordered A TO =>
>             Vect (S n) A -> (Fin (S n), A)
> argmaxMax     {n = Z}   (a :: Nil) = (FZ, a)
> argmaxMax {A} {n = S m} (a :: (a' :: as)) with (preorder a (snd (argmaxMax (a' :: as))))
>   | (Left  _) = (FS (fst ka), snd ka) where
>     ka : (Fin (S m), A)
>     ka = argmaxMax (a' :: as)
>   | (Right _) = (FZ, a)

> |||
> argmax : {A : Type} -> {TO : A -> A -> Type} -> Preordered A TO =>
>          Vect (S n) A -> Fin (S n)
> argmax = fst . argmaxMax

> |||
> max : {A : Type} -> {TO : A -> A -> Type} -> Preordered A TO =>
>       Vect (S n) A -> A
> max = snd . argmaxMax

> -}

> {-

> |||
> argmaxMax : {A, F : Type} -> {TO : F -> F -> Type} -> Ordered F TO =>
>             Vect (S n) (A,F) -> (A,F)
> argmaxMax {n = Z}   (af :: Nil) = af
> argmaxMax {n = S m} (af :: (af' :: afs)) with (order (snd af) (snd (argmaxMax (af' :: afs))))
>   | (Left  _) = argmaxMax (af' :: afs)
>   | (Right _) = af

> |||
> argmax : {A, F : Type} -> {TO : F -> F -> Type} -> Ordered F TO =>
>          Vect (S n) (A,F) -> A
> argmax = fst . argmaxMax

> |||
> max : {A, F : Type} -> {TO : F -> F -> Type} -> Ordered F TO =>
>       Vect (S n) (A,F) -> F
> max = snd . argmaxMax

> ---}

> ---}


text:
import Data.Nat

namespace MaybeList
  public export
  (>>=) : (Maybe . List) a -> (a -> (Maybe . List) b) -> (Maybe . List) b
  (>>=) = (>>=) @{Compose}

  public export
  pure : a -> (Maybe . List) a
  pure = Just . (:: Nil)

  public export
  guard : Bool -> (Maybe . List) ()
  guard False = Nothing
  guard True = pure ()

namespace ListMaybe
  public export
  (>>=) : (List . Maybe) a -> (a -> (List . Maybe) b) -> (List . Maybe) b
  (>>=) = (>>=) @{Compose}

  public export
  (>>) : (List . Maybe) () -> Lazy ((List . Maybe) b) -> (List . Maybe) b
  (>>) = (>>) @{Compose}

  public export
  pure : a -> (List . Maybe) a
  pure = (:: Nil) . Just

  public export
  guard : Bool -> (List . Maybe) ()
  guard False = []
  guard True = ListMaybe.pure ()

-- Deliberately introduce ambiguity
namespace ListMaybe2
  public export
  (>>=) : (List . Maybe) a -> (a -> (List . Maybe) b) -> (List . Maybe) b
  (>>=) = (>>=) @{Compose}

-- "Qualified do" should propagate the namespace to nested bangs.
-- "pure" and "guard" calls generated by comprehensions are
-- also subject to "qualified do".
partial
propagateNSToBangs : (List . Maybe) (Nat, Nat)
propagateNSToBangs = ListMaybe.do
  let x = ![x | x <- map Just [1..10], modNat x 2 == 0]
  let f = !(map Just $ Prelude.do [(+ x) | x <- [1..3]])
  xs <- [MaybeList.do
    Just [!(Just $ Prelude.do [(*x) | x <- [1..10], modNat x 2 == 1])
          !(Just [4, 5, 6])]]
  y <- map Just xs
  [Just (f (10 * x), y)]


text:
data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

Num ty => Num (Expr ty) where
    (+) = Add
    (*) = Mul
    fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
    negate x = 0 - x
    (-) = Sub

Abs ty => Abs (Expr ty) where
    abs = Abs

-- Exercise 7.3.1

Functor Expr where
    map func (Val x) = Val (func x)
    map func (Add x y) = Add (map func x) (map func y)
    map func (Sub x y) = Sub (map func x) (map func y)
    map func (Mul x y) = Mul (map func x) (map func y)
    map func (Div x y) = Div (map func x) (map func y)
    map func (Abs x) = Abs (map func x)

eval : (Abs num, Neg num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x) = abs (eval x)

Show num => Show (Expr num) where
     show (Val x) = show x
     show (Add x y) = show x ++ " + " ++ show y
     show (Sub x y) = show x ++ " - " ++ show y
     show (Mul x y) = show x ++ " * " ++ show y
     show (Div x y) = show x ++ " / " ++ show y
     show (Abs x) = "|" ++ show x ++ "|"

(Eq num, Num num, Abs num, Neg num, Integral num) => Eq (Expr num) where
     (==) x y = (eval x) == (eval y)

(Cast num toType, Abs num, Neg num, Integral num) => Cast (Expr num) toType where
     cast expr = cast (eval expr)


text:
module Main

import Kolgut.Swagger

%link C "Rust/target/debug/libkolgut_rust_backend.dylib"

serve : String -> IO ()
serve = foreign FFI_C "serve" (String -> IO ())

%language TypeProviders

%provide (Api : Type) with loadSwagger

x : Api
x = (Handle (\c => pure NoContent), Handle (\c => pure NoContent) )

runHandler : Handler m p s a -> String -> String -> a -> Maybe (IO (Response s))
runHandler (Handle f) method path x = if m == method  && path == p then (Just $ f x) else Nothing

getStatus : Response a -> String
getStatus {a} _ = show a

getMsg : Response a -> String
getMsg (Ok r) = r
getMsg NoContent = "Nothing here"
getMsg NotFound = "Not Found"
getMsg InternalServerError = "Server Error"

toStr : Response a -> (String, String)
toStr r = ("Status: " ++ getStatus r ++ "\n", getMsg r)

route : Api -> String -> String -> IO (String, String)
route (h1, h2) m p = let
           result1 = (toStr <$>) <$> runHandler h1 m p ()
           result2 = (toStr <$>) <$> runHandler h2 m p ()
           in maybe (pure $ toStr NotFound) id (result1 <+> result2)

getPets : () -> IO (Response 201)
getPets () = pure NoContent

getPets2 : () -> IO (Response 200)
getPets2 () = pure $ Ok "Sooty\nSmoky\n"

postPets : () -> IO (Response 201)
postPets () = pure NoContent

api : Api
api = (Handle getPets, Handle postPets) -- WILL COMPILE
--api = (Handle getPets2, Handle postPets) -- WILL NOT COMPILE

main : IO ()
main = serve "
Idris 💓 Rust
"

max_stars_repo_name: janschultecom/kolgut-api

max_issues_repo_name: janschultecom/kolgut-api

max_forks_repo_name: janschultecom/kolgut-api


text:
module Postgres.DB

import public Postgres.Data.ResultStatus
import public Postgres.Result
import public Postgres.Query

import Postgres.DB.Core
import Postgres.Data.Conn
import Postgres.Data.ConnectionStatus
import Postgres.Data.PostgresType
import Postgres.Data.PostgresValue
import Postgres.Exec
import Postgres.LoadTypes
import Postgres.Notification
import Language.JSON
import Data.HVect
import Data.Vect.Quantifiers

--
-- Safe connection
--

||| Open a connection to a Postgres database,
||| perform some actions with it, and then close
||| the connection.
|||
||| If the database connection is established successfully,
||| the `onOpen` function will be executed. If the
||| connection cannot be established, `onError` will be
||| executed.
|||
||| You do _not_ call `pgOpen` or `pgClose` directly
||| when using this function.
export
withConn : HasIO io => (pgUrl: String) -> (onOpen: Conn -> io b) -> (onError: ConnectionStatus -> io b) -> io b
withConn pgUrl onOpen onError
  = do conn <- pgOpen pgUrl
       out <- case (pgStatus conn) of
                OK => onOpen conn
                x => onError x
       pgClose conn
       pure out

--
-- Database abstraction
--

public export
data DBState = Open | Closed

public export
data OpenResult = OK | Failed String

public export
OpenResultState : OpenResult -> DBState
OpenResultState = \case OK          => Open
                        (Failed _)  => Closed

export
data Connection : Type where
  MkConnection : Conn -> TypeDictionary -> Connection

getConn : Connection -> Conn
getConn (MkConnection conn _) = conn

getTypes : Connection -> TypeDictionary
getTypes (MkConnection _ types) = types

export
data Database : (ty : Type) -> (s1 : DBState) -> (s2Fn : (ty -> DBState)) -> Type where
  DBOpen  : (url : String) -> Database OpenResult Closed OpenResultState
  DBClose : Database () Open (const Closed)

  Exec    : (fn : Connection -> IO a) -> Database a Open (const Open)

  DIO      : IO a -> Database a s1 (const s1)

  GetTypes : Database TypeDictionary Open (const Open)

  Pure    : (x : a) -> Database a (stateFn x) stateFn
  Bind    : (db : Database a s1 s2Fn) -> (f : (x : a) -> Database b (s2Fn x) s3Fn) -> Database b s1 s3Fn

%name Database db, db1, db2

export
(>>=) : (db : Database a s1 s2Fn) -> (f : (x : a) -> Database b (s2Fn x) s3Fn) -> Database b s1 s3Fn
(>>=) = Bind

export
(>>) : (db : Database a s1 (const s2)) -> Database b s2 s3Fn -> Database b s1 s3Fn
db >> db2 = db >>= (\_ => db2)

export
pure : (x : a) -> Database a (stateFn x) stateFn
pure = Pure

export
liftIO' : IO a -> Database a s1 (const s1)
liftIO' = DIO

data ConnectionState : DBState -> Type where
  CConnected : (conn : Connection) -> ConnectionState Open
  CDisconnected : ConnectionState Closed

openResult : HasIO io => Conn -> io OpenResult
openResult conn = case (pgStatus conn) of
                       OK => pure OK
                       x  => Failed <$> pgErrorMessage conn

runDatabase' : HasIO io => ConnectionState s1 -> Database a s1 s2Fn -> io $ (x : a ** ConnectionState (s2Fn x))
runDatabase' CDisconnected (DBOpen url) = do conn <- pgOpen url
                                             status <- openResult conn
                                             case status of
                                                  OK => do Right types <- pgLoadTypes conn
                                                             | Left err => pure (Failed err ** CDisconnected)
                                                           pure (OK ** CConnected (MkConnection conn types))
                                                  Failed err => pure (Failed err ** CDisconnected)
runDatabase' (CConnected conn) DBClose = do pgClose (getConn conn)
                                            pure $ (() ** CDisconnected)
runDatabase' (CConnected conn) (Exec fn) = liftIO $ do res <- fn conn
                                                       pure (res ** CConnected conn)
runDatabase' (CConnected conn) GetTypes = pure $ (getTypes conn ** CConnected conn)
runDatabase' cs (Pure y) = pure (y ** cs)
runDatabase' cs (Bind db f) = do (res ** cs') <- runDatabase' cs db
                                 runDatabase' cs' (f res)
runDatabase' cs (DIO io) = do v <- liftIO io
                              pure (v ** cs)

export
evalDatabase : HasIO io => Database a Closed (const Closed) -> io a
evalDatabase db = pure $ fst !(runDatabase' CDisconnected db)

export
initDatabase : Database () Closed (const Closed)
initDatabase = pure ()

export
openDatabase : (url : String) -> Database OpenResult Closed OpenResultState
openDatabase = DBOpen

export
closeDatabase : Database () Open (const Closed)
closeDatabase = DBClose

export
exec : (Connection -> IO a) -> Database a Open (const Open)
exec = Exec

||| You can execute arbitrary things against the lower-level
||| Conn, including closing the database connection prematurely.
export
unsafeExec : (Conn -> IO a) -> Database a Open (const Open)
unsafeExec f = Exec (\(MkConnection conn empty) => f conn)

||| Take a function that operates on a Conn
||| (currency of the underlying lower level
||| Postgres stuff) and turn it into a function
||| that operates on a Connection.
pgExec : (Conn -> IO a) -> Connection -> IO a
pgExec f = f . getConn

export
withDB : HasIO io => (url : String) -> Database a Open (const Open) -> io $ Either String a
withDB url dbOps = evalDatabase dbCommands
  where
    dbCommands : Database (Either String a) Closed (const Closed)
    dbCommands = do initDatabase
                    OK <- openDatabase url
                      | Failed err => pure $ Left err
                    out <- dbOps
                    closeDatabase
                    pure $ Right out

||| Dump the Postgres type dictionary for debugging purposes.
export
debugDumpTypes : Database () Open (const Open)
debugDumpTypes = do types <- GetTypes
                    liftIO' $ putStrLn $ show types
                    pure ()

--
-- Postgres Commands
--

||| Query the database interpreting all columns as strings.
export
stringQuery : (header : Bool) -> (query : String) -> Connection -> IO (Either String (StringResultset header))
stringQuery header query (MkConnection conn types) = pgStringResultsQuery header query conn

||| Query the database expecting a JSON result is returned.
export
jsonQuery : (query : String) -> Connection -> IO (Maybe JSON)
jsonQuery = pgExec . pgJSONResultQuery

||| Query the database expecting the given array of types in each
||| row of the result returned.
export
expectedQuery : {cols : Nat}
             -> (expected : Vect cols Type)
             -> (query : String)
             -> {auto castable : (All Castable expected)}
             -> Connection
             -> IO (Either String (rowCount ** Vect rowCount (HVect expected)))
expectedQuery expected query (MkConnection conn types) = pgResultQuery expected query conn

||| Perform the given command and instead of parsing the response
||| just report the result status. This is useful when you don't
||| care if/what the response looks like, just whether the command
||| worked
export
perform : (command : String) -> Connection -> IO ResultStatus
perform cmd = pgExec (\c => withExecResult c cmd (pure . pgResultStatus))

||| Start listening for notifications on the given channel.
export
listen : (channel : String) -> Connection -> IO ResultStatus
listen = pgExec . pgListen

||| Gets the next notification _of those sitting around locally_.
||| Returns `Nothing` if there are no notifications.
|||
||| See `libpq` documentation on `PQnotifies` for details on the
||| distinction between retrieving notifications from the server and
||| getting the next notification that has already been retrieved.
|||
||| NOTE: This function _does_ consume input to make sure no notification
|||  sent by the server but not processed by the client yet gets
|||  missed.
export
nextNotification : Connection -> IO (Maybe Notification)
nextNotification = pgExec pgNextNotification

||| Produce a potentially infinite stream of notifications.
||| Unlike `nextNotificaiton`, this will wait for the server
||| to deliver a notification.
|||
||| This _is_ an infinite sequence with a blocking wait for the
||| next notification so it is of somewhat limited utility
||| compared to checking for new notifications at a natural point
||| in your programs existing logic loop unless your entire loop
||| is dictated by notification arrival anyway.
export
partial
notificationStream : Connection -> Stream (IO Notification)
notificationStream = pgNotificationStream . getConn

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
module Replica.App

import public Control.App
import public Control.App.Console

import public Replica.App.FileSystem
import public Replica.App.Info
import public Replica.App.Log
import public Replica.App.Replica
import public Replica.App.Run
import public Replica.App.System

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica