text:
module Text.CSS.Property

import Data.List
import Data.String
import Data.Vect
import Text.CSS.Color
import Text.CSS.Dir
import Text.CSS.Flexbox
import Text.CSS.Grid
import Text.CSS.Length
import Text.CSS.ListStyleType
import Text.CSS.Percentage
import Text.CSS.Render

%default total

namespace Direction
  public export
  data Direction = LTR | RTL

  export
  Render Direction where
    render LTR = "ltr"
    render RTL = "rtl"

namespace Display
  public export
  interface AreaTag a where
    showTag : a -> String

  public export
  data Display : Type where
    Flex  : Display
    Grid  : Display
    Area  :  {0 n,m : Nat}
          -> {0 a : Type}
          -> AreaTag a
          => (rows    : Vect (S m) GridValue)
          -> (columns : Vect (S n) GridValue)
          -> (area    : Vect (S m) (Vect (S n) a))
          -> Display

  export
  renderArea :  AreaTag a
             => Vect (S m) GridValue
             -> Vect (S n) GridValue
             -> Vect (S m) (Vect (S n) a)
             -> String
  renderArea rs cs as =
    let rsStr = "grid-template-rows: " ++ render (toList rs)
        csStr = "grid-template-columns: " ++ render (toList cs)
        aStr  = fastConcat . intersperse " " . map col $ toList as
     in "display: grid; \{rsStr}; \{csStr}; grid-template-areas: \{aStr}"
    where col : Vect (S n) a -> String
          col vs =
            let str = concat . intersperse " " . map showTag $ toList vs
             in #""\#{str}""#

namespace FlexBasis
  public export
  data FlexBasis : Type where
    FL       : Length -> FlexBasis
    FP       : Percentage -> FlexBasis

  export
  Render FlexBasis where
    render (FL x)   = render x
    render (FP x)   = render x

  export %inline
  Cast Length FlexBasis where
    cast = FL

  export %inline
  Cast Percentage FlexBasis where
    cast = FP

namespace FontSize
  public export
  data FontSize : Type where
    FL       : Length -> FontSize
    FP       : Percentage -> FontSize
    XXSmall  : FontSize
    XSmall   : FontSize
    Small    : FontSize
    Medium   : FontSize
    Large    : FontSize
    XLarge   : FontSize
    XXLarge  : FontSize
    XXXLarge : FontSize

  export
  Render FontSize where
    render (FL x)   = render x
    render (FP x)   = render x
    render XXSmall  = "xx-small"
    render XSmall   = "x-small"
    render Small    = "small"
    render Medium   = "medium"
    render Large    = "large"
    render XLarge   = "x-large"
    render XXLarge  = "xx-large"
    render XXXLarge = "xxx-large"

  export %inline
  Cast Length FontSize where
    cast = FL

  export %inline
  Cast Percentage FontSize where
    cast = FP

namespace BorderRadius
  public export
  data BorderRadius : Type where
    BL : Length -> BorderRadius
    BP : Percentage -> BorderRadius
    BS : String -> BorderRadius

  export
  Render BorderRadius where
    render (BL x) = render x
    render (BP x) = render x
    render (BS x) = x

  export %inline
  Cast Length BorderRadius where
    cast = BL

  export %inline
  Cast Percentage BorderRadius where
    cast = BP

  export %inline
  FromString BorderRadius where
    fromString = BS

namespace BorderStyle
  public export
  data BorderStyle : Type where
    None   : BorderStyle
    Hidden : BorderStyle
    Dotted : BorderStyle
    Dashed : BorderStyle
    Solid  : BorderStyle
    Dbl    : BorderStyle
    Groove : BorderStyle
    Ridge  : BorderStyle
    Inset  : BorderStyle
    Outset : BorderStyle

  export
  Render BorderStyle where
    render None   = "none"
    render Hidden = "hidden"
    render Dotted = "dotted"
    render Dashed = "dashed"
    render Solid  = "solid"
    render Dbl    = "double"
    render Groove = "groove"
    render Ridge  = "ridge"
    render Inset  = "inset"
    render Outset = "outset"

namespace BorderWidth
  public export
  data BorderWidth : Type where
    BL     : Length -> BorderWidth
    Thin   : BorderWidth
    Medium : BorderWidth
    Thick  : BorderWidth

  export
  Render BorderWidth where
    render (BL x) = render x
    render Thin   = "thin"
    render Medium = "medium"
    render Thick  = "thick"

  export %inline
  Cast Length BorderWidth where
    cast = BL

namespace TextAlign
  public export
  data TextAlign : Type where
    ||| The same as left if direction is left-to-right and right if direction is right-to-left.
    Start   : TextAlign
    ||| The same as right if direction is left-to-right and left if direction is right-to-left.
    End     : TextAlign
    ||| The inline contents are aligned to the left edge of the line box.
    Left    : TextAlign
    ||| The inline contents are aligned to the right edge of the line box.
    Right   : TextAlign
    ||| The inline contents are centered within the line box.
    Center  : TextAlign
    ||| The inline contents are justified. Text should be spaced to line up its left and right edges to the left and right edges of the line box, except for the last line.
    Justify : TextAlign

  export
  Render TextAlign where
    render Start   = "start"
    render End     = "end"
    render Left    = "left"
    render Right   = "right"
    render Center  = "center"
    render Justify = "justify"

namespace Width
  public export
  data Width : Type where
    WL       : Length -> Width
    WP       : Percentage -> Width

  export
  Render Width where
    render (WL x)   = render x
    render (WP x)   = render x

  export %inline
  Cast Length Width where
    cast = WL

  export %inline
  Cast Percentage Width where
    cast = WP

public export
data Property : Type -> Type where
  AlignItems          : Property FlexAlign
  AlignSelf           : Property FlexAlign
  BackgroundColor     : Property Color
  BackgroundSize      : Property Width
  BorderColor         : Property (Dir Color)
  BorderRadius        : Property BorderRadius
  BorderStyle         : Property (Dir BorderStyle)
  BorderWidth         : Property (Dir BorderWidth)
  Color               : Property Color
  ColumnGap           : Property Length
  Direction           : Property Direction
  Display             : Property Display
  Flex                : Property String
  FlexBasis           : Property FlexBasis
  FlexDirection       : Property FlexDirection
  FlexWrap            : Property String
  FontFamily          : Property String
  FontSize            : Property FontSize
  GridArea            : AreaTag a => Property a
  GridColumn          : Property GridPosition
  GridRow             : Property GridPosition
  GridTemplateColumns : Property (List GridValue)
  GridTemplateRows    : Property (List GridValue)
  Height              : Property Width
  JustifyContent      : Property FlexJustify
  JustifySelf         : Property FlexJustify
  ListStyleType       : Property ListStyleType
  Margin              : Property (Dir Length)
  MaxHeight           : Property Width
  MaxWidth            : Property Width
  MinHeight           : Property Width
  MinWidth            : Property Width
  Padding             : Property (Dir Length)
  RowGap              : Property Length
  TextAlign           : Property TextAlign
  Width               : Property Width

export
renderProp : Property t -> t -> String
renderProp AlignItems y          = "align-items: " ++ render y
renderProp AlignSelf y           = "align-self: " ++ render y
renderProp BackgroundColor y     = "background-color: " ++ render y
renderProp BackgroundSize y      = "background-size: " ++ render y
renderProp BorderColor y         = render2 "border" "color" render y
renderProp BorderRadius y        = "border-radius: " ++ render y
renderProp BorderStyle y         = render2 "border" "style" render y
renderProp BorderWidth y         = render2 "border" "width" render y
renderProp Color y               = "color: " ++ render y
renderProp ColumnGap y           = "column-gap: " ++ render y
renderProp Direction y           = "direction: " ++ render y
renderProp Display Grid          = "display: grid"
renderProp Display Flex          = "display: flex"
renderProp Display (Area r c a)  = renderArea r c a
renderProp Flex y                = "flex: " ++ y
renderProp FlexBasis y           = "flex-basis: " ++ render y
renderProp FlexDirection y       = "flex-direction: " ++ render y
renderProp FlexWrap y            = "flex-wrap: " ++ y
renderProp FontFamily y          = "font-family: " ++ y
renderProp FontSize y            = "font-size: " ++ render y
renderProp GridArea y            = "grid-area: " ++ showTag y
renderProp GridColumn y          = "grid-column: " ++ render y
renderProp GridRow y             = "grid-row: " ++ render y
renderProp GridTemplateColumns y = "grid-template-columns: " ++ render y
renderProp GridTemplateRows y    = "grid-template-rows: " ++ render y
renderProp Height y              = "height: " ++ render y
renderProp JustifyContent y      = "justify-content: " ++ render y
renderProp JustifySelf y         = "justify-self: " ++ render y
renderProp ListStyleType y       = "list-style-type: " ++ render y
renderProp Margin y              = render "margin" render y
renderProp MaxHeight y           = "max-height: " ++ render y
renderProp MaxWidth y            = "max-width: " ++ render y
renderProp MinHeight y           = "min-height: " ++ render y
renderProp MinWidth y            = "min-width: " ++ render y
renderProp Padding y             = render "padding" render y
renderProp RowGap y              = "row-gap: " ++ render y
renderProp TextAlign y           = "text-align: " ++ render y
renderProp Width y               = "width: " ++ render y


text:
module Files

import Data.Buffer
import Control.Monad.Either
import Control.Monad.Maybe
import Control.Monad.Trans
import Node.HTTP.Server
import Node.HTTP.Client
import Node
import System.Directory
import TyTTP.Adapter.Node.HTTP
import TyTTP.Adapter.Node.Static
import TyTTP.HTTP
import TyTTP.HTTP.Producer
import TyTTP.HTTP.Routing
import TyTTP.URL
import TyTTP.URL.Path

sendError :
  Error e
  => HasIO io
  => Status
  -> String
  -> Context me u h1 s StringHeaders a b
  -> io $ Context me u h1 Status StringHeaders a (Publisher IO e Buffer)
sendError st str ctx = do
  text str ctx >>= status st

routeDef : Error e
  => String
  -> StaticRequest e String
  -> Promise e IO $ StaticResponse e String
routeDef folder =
    let routingError = sendError NOT_FOUND "Resource could not be found"
        urlError = \err => sendError BAD_REQUEST "URL has invalid format"
    in
      parseUrl' urlError :>
        routes' routingError
          [ get $ path "/static/*" :> hStatic folder $ flip $ \ctx =>
              \case
                StatError e => sendError INTERNAL_SERVER_ERROR ("File error: " <+> message e) ctx
                NotAFile s => sendError NOT_FOUND ("Could not found file: " <+> s) ctx
          ]

main : IO ()
main = eitherT putStrLn pure $ do
  Just folder <- currentDir
    | _ => putStrLn "There is no current folder"

  http <- HTTP.require
  server <- HTTP.listen' $ routeDef "\{folder}/"

  defer $ ignore $ http.get "http://localhost:3000/static/run" $ \res => do
      putStrLn res.statusCode
      onData res putStrLn
      server.close

ext: idr

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Language.LSP.CodeAction.CaseSplit

import Core.Context
import Core.Core
import Core.Metadata
import Core.UnifyState
import Data.String
import Idris.IDEMode.CaseSplit
import Idris.REPL.Opts
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.CodeAction.Utils
import Language.LSP.Message
import Server.Configuration
import Server.Log
import Server.Utils
import TTImp.Interactive.CaseSplit

buildCodeAction : URI -> Name -> TextEdit -> CodeAction
buildCodeAction uri name edit =
  MkCodeAction
    { title       = "Case split on ?\{show name}"
    , kind        = Just RefactorRewrite
    , diagnostics = Nothing
    , isPreferred = Nothing
    , disabled    = Nothing
    , edit        = Just $ MkWorkspaceEdit
        { changes           = Just (singleton uri [edit])
        , documentChanges   = Nothing
        , changeAnnotations = Nothing
        }
    , command     = Nothing
    , data_       = Nothing
    }

export
caseSplitKind : CodeActionKind
caseSplitKind = Other "refactor.rewrite.CaseSplit"

isAllowed : CodeActionParams -> Bool
isAllowed params =
  maybe True (\filter => (caseSplitKind `elem` filter) || (RefactorRewrite `elem` filter)) params.context.only

export
caseSplit : Ref LSPConf LSPConfiguration
         => Ref MD Metadata
         => Ref Ctxt Defs
         => Ref UST UState
         => Ref Syn SyntaxInfo
         => Ref ROpts REPLOpts
         => CodeActionParams -> Core (Maybe CodeAction)
caseSplit params = do
  let True = isAllowed params
    | False => logI CaseSplit "Skipped" >> pure Nothing
  logI CaseSplit "Checking for \{show params.textDocument.uri} at \{show params.range}"

  withSingleLine CaseSplit params (pure Nothing) $ \line => do
    withSingleCache CaseSplit params CaseSplit $ do

      let col = params.range.start.character
      Just (loc, name) <- gets MD (findInTreeLoc (cast params.range.start) (cast params.range.end) . nameLocMap)
        | Nothing => logD CaseSplit "No name found at \{show line}:\{show col}}" >> pure Nothing

      logD CaseSplit "Found name \{show name}"
      let find = if col > 0 then within (line, col) else onLine line
      OK splits <- getSplits (anyAt find) name
        | SplitFail err => logD CaseSplit "Error while splitting: \{show err}" >> pure Nothing

      lines <- updateCase splits line col
      Just original <- getSourceLine (line + 1)
        | Nothing => do logE CaseSplit "Cannot fetch referenced line even if compiler command succeded"
                        pure Nothing

      let rng = MkRange (MkPosition line 0) (MkPosition line (cast (length original)))
      let edit = MkTextEdit rng (unlines lines)
      pure $ Just (cast loc, buildCodeAction params.textDocument.uri name edit)


text:
mapV : (a -> b) -> Vector xs a ->
                   Vector xs b
mapV f v {xs=[]}  = f v
mapV f v {xs = (y::ys)} = map (mapV f) v

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
module Select

-- Based on http://eptcs.web.cse.unsw.edu.au/paper.cgi?MSFP2014.3.pdf
--          https://downloads.haskell.org/~ghc/latest/docs/html/libraries/transformers-0.5.6.2/src/Control-Monad-Trans-Select.html#SelectT

import Data.Vect
import Control.Monad.Identity
import Control.Monad.Trans

data SelectT : (r : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
  Sel : ((a -> m r) -> m a) -> SelectT r m a

Select : Type -> Type -> Type
Select a r = SelectT r Identity a

Functor m => Functor (SelectT r m) where
  map f (Sel g) = Sel (\k => map f $ g (k . f))

Monad m => Applicative (SelectT r m) where
  pure a = Sel (\k => pure a)

  (Sel gf) <*> (Sel g) = Sel $ \k => do f <- gf (\f => h f k >>= k)
                                        h f k
    where
     h : (a -> b) -> (b -> m r) -> m b
     h f k = map f $ g (k . f)

Monad m => Monad (SelectT r m) where
  (Sel g) >>= f = Sel $ \k => do a <- g (\a => h a k >>= k)
                                 h a k
    where
      h : a -> (b -> m r) -> m b
      h a k = let (Sel g') = f a in g' k

MonadTrans (SelectT r) where
  lift m = Sel (\k => m)

boundedBinarySearch : Monad m => (n : Nat) -> SelectT Bool m (Vect n Bool)
boundedBinarySearch n = sequence $ replicate n $ Sel (\k => k True)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Control.Monad.Ref

import public Control.Monad.Identity
import public Control.Monad.Trans
import public Data.IORef

%default total
%access public export

-- Interface -------------------------------------------------------------------

interface Monad m => MonadRef (l : Type -> Type) (m : Type -> Type) | m where
  ref    : a -> m (l a)
  deref  : l a -> m a
  assign : l a -> a -> m ()

infix 4 :=
(:=) : MonadRef l m => l a -> a -> m ()
(:=) = assign

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

MonadRef IORef IO where
  ref    = newIORef
  deref  = readIORef
  assign = writeIORef

-- Helpers ---------------------------------------------------------------------

modify : MonadRef l m => l a -> (a -> a) -> m ()
modify l f = do
  x <- deref l
  l := f x

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module System.File.Buffer

import public System.File.Error
import System.File.Handle
import System.File.Meta
import System.File.Mode
import System.File.ReadWrite
import System.File.Support
import public System.File.Types

import Data.Buffer

%default total

%foreign support "idris2_readBufferData"
         "node:lambda:(f,b,l,m) => require('fs').readSync(f.fd,b,l,m)"
         "jvm:readFromFile(java/nio/channels/ReadableByteChannel io/github/mmhelloworld/idrisjvm/runtime/IdrisBuffer int int int),io/github/mmhelloworld/idrisjvm/runtime/IdrisBuffer"
prim__readBufferData : FilePtr -> Buffer -> (offset : Int) -> (maxbytes : Int) -> PrimIO Int

%foreign support "idris2_writeBufferData"
         "node:lambda:(f,b,l,m) => require('fs').writeSync(f.fd,b,l,m)"
         "jvm:writeToFile(java/nio/channels/WritableByteChannel io/github/mmhelloworld/idrisjvm/runtime/IdrisBuffer int int int),io/github/mmhelloworld/idrisjvm/runtime/IdrisBuffer"
prim__writeBufferData : FilePtr -> Buffer -> (offset : Int) -> (maxbytes : Int) -> PrimIO Int

export
readBufferData : HasIO io => File -> Buffer ->
                 (offset : Int) -> -- position in buffer to start adding
                 (maxbytes : Int) -> -- maximums size to read, which must not
                                     -- exceed buffer length
                 io (Either FileError ())
readBufferData (FHandle h) buf offset max
    = do read <- primIO (prim__readBufferData h buf offset max)
         if read >= 0
            then pure (Right ())
            else pure (Left FileReadError)

export
writeBufferData : HasIO io => File -> Buffer ->
                  (offset : Int) -> -- position in buffer to write from
                  (maxbytes : Int) -> -- maximums size to write, which must not
                                      -- exceed buffer length
                  io (Either FileError ())
writeBufferData (FHandle h) buf offset max
    = do written <- primIO (prim__writeBufferData h buf offset max)
         if written >= 0
            then pure (Right ())
            else pure (Left FileWriteError)

export
writeBufferToFile : HasIO io => String -> Buffer -> Int -> io (Either FileError ())
writeBufferToFile fn buf max
    = do Right f <- openFile fn WriteTruncate
             | Left err => pure (Left err)
         Right ok <- writeBufferData f buf 0 max
             | Left err => pure (Left err)
         closeFile f
         pure (Right ok)

export
createBufferFromFile : HasIO io => String -> io (Either FileError Buffer)
createBufferFromFile fn
    = do Right f <- openFile fn Read
             | Left err => pure (Left err)
         Right size <- fileSize f
             | Left err => pure (Left err)
         Just buf <- newBuffer size
             | Nothing => pure (Left FileReadError)
         Right ok <- readBufferData f buf 0 size
             | Left err => pure (Left err)
         closeFile f
         pure (Right buf)


text:
module Main

{-
To write these functions in vim:

\d to make a template definition
\c over a variable to do case analysis on that variable
\o to fill in a hole with the 'obvious' value

-}

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

%name Vect xs,ys,zs

append : Vect n a -> Vect m a -> Vect (n + m) a

{-
Try to write this using the interactive tools alone:

append [] ys = ys
append (x :: xs) ys = x :: append xs ys
-}

vZipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

{-
Try to write this using the interactive tools alone:

vZipWith f [] [] = []
vZipWith f (x :: xs) (y :: ys) = f x y :: vZipWith f xs ys
-}

max_stars_repo_name: idris-hackers/idris-demos

max_issues_repo_name: idris-hackers/idris-demos

max_forks_repo_name: idris-hackers/idris-demos


text:
module Proofs.GroupCancelationLemmas

import Specifications.Group
import Symmetry.Opposite

%default total
%access export

infixl 8 #

||| cancel two factors in a product of three
groupCancel1 : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b : s) ->
  (inv a # a) # b = b
groupCancel1 spec a b = o2 === o3 where
  o1 : inv a # a = e
  o1 = inverseL spec a
  o2 : (inv a # a) # b = e # b
  o2 = cong {f = (# b)} o1
  o3 : e # b = b
  o3 = neutralL (monoid spec) b

||| cancel two factors in a product of three
groupCancel1bis : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b : s) ->
  inv a # (a # b) = b
groupCancel1bis spec a b = assoc === groupCancel1 spec a b where
  assoc : inv a # (a # b) = (inv a # a) # b
  assoc = associative (monoid spec) _ _ _

||| cancel two factors in a product of three
groupCancel2 : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b : s) ->
  a # (inv b # b) = a
groupCancel2 spec a b = o2 === o3 where
  o1 : inv b # b = e
  o1 = inverseL spec b
  o2 : a # (inv b # b) = a # e
  o2 = cong o1
  o3 : a # e = a
  o3 = neutralR (monoid spec) a

||| cancel two factors in a product of three
groupCancel2bis : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b : s) ->
  (a # inv b) # b = a
groupCancel2bis spec a b = assoc @== groupCancel2 spec a b where
  assoc : a # (inv b # b) = (a # inv b) # b
  assoc = associative (monoid spec) _ _ _

||| cancel two factors in a product of three
groupCancel3 : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b : s) ->
  a # (b # inv b) = a
groupCancel3 spec a b = groupCancel1 (opposite spec) b a

||| cancel two factors in a product of three
groupCancel3bis : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b : s) ->
  (a # b) # inv b = a
groupCancel3bis spec a b = groupCancel1bis (opposite spec) b a

||| cancel two factors in a product of three
groupCancelAbelian : {(#) : Binop s} ->
  GroupSpec (#) e inv -> isAbelian (#) -> (a,b : s) ->
    a # (b # inv a) = b
groupCancelAbelian spec abel a b = abel a _ === o1 where
  o1 : (b # inv a) # a = b
  o1 = groupCancel2bis spec b a

||| Translations are injective.
groupTranslationInjectiveL : {(#) : Binop s} ->
  GroupSpec (#) e inv -> (a,x,y : s) -> a # x = a # y -> x = y
groupTranslationInjectiveL spec a x y given = o2 where
  o1 : inv a # (a # x) = inv a # (a # y)
  o1 = cong given
  o2 : x = y
  o2 = groupCancel1bis spec a x @== o1 === groupCancel1bis spec a y

||| ab = a implies b = e
groupCancelGivesNeutral : {(#) : Binop s} ->
  GroupSpec (#) e inv -> (a,b : s) ->
    a # b = a -> b = e
groupCancelGivesNeutral spec a b given = o2 === inverseL spec a where
  o1 : inv a # (a # b) = inv a # a
  o1 = cong given
  o2 : b = inv a # a
  o2 = groupCancel1bis spec a b @== o1

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Flutter.Widgets.Stateful

import Dart.FFI
import Flutter.FFI

%inline
public export
Stateful : Type
Stateful = Struct "_Stateful,
import 'package:flutter/material.dart' as material;

class _Stateful extends material.StatefulWidget {
  final $.Object initialState;
  final material.Widget Function(_StatefulWidgetState, material.BuildContext) onBuild;

  _Stateful({material.Key key, this.initialState, this.onBuild}) : super(key: key);

  @$.override
  _StatefulState createState() => _StatefulState(initialState, onBuild);
}

class _StatefulState extends material.State<_Stateful> {
  $.Object state;
  final $.Object Function(_StatefulWidgetState, material.BuildContext) onBuild;

  _StatefulState(this.state, this.onBuild);

  void modify($.Object Function($.Object) f) {
    setState(() {
      state = f(state);
    });
  }

  @$.override
  material.Widget build(material.BuildContext context) {
    return onBuild(_StatefulWidgetState(state, this), context);
  }
}

class _StatefulWidgetState {
  final $.dynamic value;
  final _StatefulState _state;
  _StatefulWidgetState(this.value, this._state);
  void modify($.Object Function($.Object) f) {
    _state.modify(f);
  }
}
" []

%inline
public export
StatefulWidgetState : Type -> Type
StatefulWidgetState ty = Struct "_StatefulWidgetState" [("value", ty)]

namespace StatefulWidgetState

  %inline
  public export
  get : StatefulWidgetState ty -> ty
  get widgetState = widgetState `getField` "value"

public export
IsAssignableFrom Widget Stateful where

namespace Stateful

  namespace New

    public export
    data Tag : (stateType : Type) -> Type where

    %inline
    public export
    key : {stateType : Type} -> Parameter (Tag stateType)
    key = mkParameter "key" Key

    %inline
    public export
    initialState : {stateType : Type} -> Parameter (Tag stateType)
    initialState = mkParameter "initialState" stateType

    %inline
    public export
    onBuild : {stateType : Type} -> Parameter (Tag stateType)
    onBuild = mkParameter "onBuild" (StatefulWidgetState stateType -> BuildContext -> IO Widget)

    %inline
    public export
    NamedParameters : {stateType : Type} -> Type
    NamedParameters = Parameters [
      Stateful.New.key {stateType = stateType},
      Stateful.New.initialState {stateType = stateType},
      Stateful.New.onBuild {stateType = stateType}
    ]

  %inline
  public export
  new : {stateType : Type} -> Stateful.New.NamedParameters {stateType = stateType} -> IO Stateful
  new ps = primIO (prim__dart_new Stateful [] ps)

  %foreign "Dart:.modify"
  prim__modify : StatefulWidgetState stateType -> (stateType -> stateType) -> PrimIO ()

  export
  modify : StatefulWidgetState stateType -> (stateType -> stateType) -> IO ()
  modify state f = primIO (prim__modify state f)


text:
module Main

import Foo

testConstValue1 : String
testConstValue1 = dep1

testConstValue2 : String
testConstValue2 = dep2

testFunctionPass : String -> String
testFunctionPass = dep3

testErasedFunction : List Int -> Foo.foo Int
testErasedFunction xs = xs

0 testInErasedContext : Type
testInErasedContext = foo Int


text:
module Data.Fun.Graph

||| A relation corresponding to the graph of `f`.
public export
record Graph {0 a : Type} {0 b : a -> Type}
             (f : (x : a) -> b x) (x : a) (y : b x) where
  constructor MkGraph
  equality : f x === y

||| An alternative for 'Syntax.WithProof' that allows to keep the
||| proof certificate in non-reduced form after nested matching.
||| Inspired by https://agda.github.io/agda-stdlib/README.Inspect.html
public export
remember : {0 a : Type} -> {0 b : a -> Type} ->
           (f : (x : a) -> b x) -> (x : a) -> Graph f x (f x)
remember _ _ = MkGraph Refl


text:
module Sub01Apply18x3

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(6x+1) --B[1,-2]--> 3x
b18x3To3x :
  (k:Nat) -> P (S (plus (plus (plus k k) (plus k k)) (plus k k))) 2 -> P k 2
b18x3To3x k prf =
  let prf2 = lvDown (S (plus (plus (plus k k) (plus k k)) (plus k k))) 2 prf in
    b18x3To3x' k prf2
export
apply18x3 : P (S (plus (plus (plus k k) (plus k k)) (plus k k))) 2
  -> (m : Nat **
      (LTE (S m) (S (plus (plus (plus k k) (plus k k)) (plus k k))), P m 2))
apply18x3 {k} col = let col2 = b18x3To3x k col in (k ** (lte18x3 k, col2)) where
  lte18x3 : (k:Nat) -> LTE (S k) (S (plus (plus (plus k k) (plus k k)) (plus k k)))
  lte18x3 Z = LTESucc LTEZero
  lte18x3 (S k) = rewrite (sym (plusSuccRightSucc k k)) in
    rewrite (sym (plusSuccRightSucc (plus k k) (S (plus k k)))) in
    rewrite (sym (plusSuccRightSucc (plus k k) (plus k k))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (S (plus k k)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (plus k k))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc) (lte18x3 k)
-- ---------------------------


text:
module LightClick.DSL.Parser

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

import public Text.Lexer
import public Text.Parser

import Toolkit.Data.List.View.PairWise

import public Toolkit.Data.Location
import public Toolkit.Text.Lexer.Run
import public Toolkit.Text.Parser.Support
import        Toolkit.Text.Parser.Location
import public Toolkit.Text.Parser.Run

import        Language.SystemVerilog.Gates

import        LightClick.Types.Direction
import        LightClick.Types.Sensitivity
import        LightClick.Types.WireType

import        LightClick.DSL.AST

import public LightClick.DSL.Lexer
import        LightClick.DSL.Parser.API

%default total

data TypeStyle = HASKELL | SYSV

var : Rule AST
var = do
  s <- Toolkit.location
  n <- name
  e <- Toolkit.location
  pure (Ref (newFC s e) n)

logic : Rule AST
logic = do
  st <- Toolkit.location
  keyword "logic"
  end <- Toolkit.location
  pure (DataLogic (newFC st end))

type__ : Rule AST
type__ = logic <|> var

array : Rule AST
array = do
  s <- Toolkit.location
  ty <- type__
  idx <- braces natLit
  e <- Toolkit.location
  pure (DataArray (newFC s e) ty idx)

mutual
  ascrip : Rule (String, AST)
  ascrip = do
    n <- name
    symbol ":"
    ty <- type_
    pure (n,ty)

  struct : Rule AST
  struct = do
    s <- Toolkit.location
    keyword "struct"
    kvs <- brackets $ commaSepBy1V ascrip
    e <- Toolkit.location
    pure (DataStruct (newFC s e) (snd kvs))

  union : Rule AST
  union = do
    s <- Toolkit.location
    keyword "union"
    kvs <- brackets $ commaSepBy1V ascrip
    e <- Toolkit.location
    pure (DataUnion (newFC s e) (snd kvs))

  type_ : Rule AST
  type_ = array <|> struct <|> union <|> type__

typeDef : Rule (FileContext, String, AST)
typeDef = do
  d <- optional doc
  s <- Toolkit.location
  n <- name
  symbol "="
  decl <- type_
  e <- Toolkit.location
  pure (newFC s e, n, decl)

direction : Rule Direction
direction = do {keyword "inout";  pure INOUT}
        <|> do {keyword "output"; pure OUT}
        <|> do {keyword "input"; pure IN}

sensitivity : Rule Sensitivity
sensitivity = do {keyword "high";  pure High}
          <|> do {keyword "low"; pure Low}
          <|> do {keyword "rising"; pure Rising}
          <|> do {keyword "falling"; pure Falling}
          <|> do {keyword "insensitive"; pure Insensitive}

wireType : Rule Wire
wireType = do {keyword "general";  pure General}
       <|> do {keyword "data"; pure Data}
       <|> do {keyword "address"; pure Address}
       <|> do {keyword "clock"; pure Clock}
       <|> do {keyword "reset"; pure Reset}
       <|> do {keyword "control"; pure Control}
       <|> do {keyword "interrupt"; pure Interrupt}
       <|> do {keyword "info"; pure Info}

portHaskellStyle : Rule AST
portHaskellStyle
  = do st <- Toolkit.location
       com <- optional doc
       label <- name
       symbol ":"
       t <- type_
       c <- option General wireType
       d <- direction
       s <- option Insensitive sensitivity
       e <- Toolkit.location
       pure (Port (newFC st e) label d s c t)

portSystemVerilogStyle : Rule AST
portSystemVerilogStyle
  = do st <- Toolkit.location
       com <- optional doc
       d <- direction
       s <- option Insensitive sensitivity
       c <- option General wireType
       t <- type_
       label <- name
       e <- Toolkit.location
       pure (Port (newFC st e) label d s c t)

port : TypeStyle -> Rule AST
port HASKELL = portHaskellStyle
port SYSV    = portSystemVerilogStyle

moduleDef : TypeStyle -> Rule (FileContext, String, AST)
moduleDef style
  = do ds <- optional doc
       d <- Toolkit.location
       n <- name
       symbol "="
       s <- Toolkit.location
       keyword "module"
       res <- brackets $ commaSepBy1V (port style)
       e <- Toolkit.location
       pure (newFC d e, n, ModuleDef (newFC s e) (snd res))

idx : Rule AST
idx = do
  s <- Toolkit.location
  m <- var
  n <- braces name
  e <- Toolkit.location
  pure (Index (newFC s e) m n)

ref : Rule AST
ref = idx

connect : Rule AST
connect
    = do s <- Toolkit.location
         l <- ref
         arrow
         r <- ref
         e <- Toolkit.location
         pure (newConn s e l r)
  where
    newConn : (s,e : Location)
           -> (l,r : AST)
           -> AST
    newConn s e = Connect (newFC s e)

fanout : Rule AST
fanout = do
  s <- Toolkit.location
  i  <- ref
  arrow
  fs <- brackets $ commaSepBy2V ref
  e <- Toolkit.location
  pure (FanOut (newFC s e) i (snd fs))

mux : Rule AST
mux = do
  s <- Toolkit.location
  fs <- brackets $ commaSepBy2V ref
  symbol "-"
  ctrl <- parens ref
  arrow
  o <- ref
  e <- Toolkit.location
  pure (Mux (newFC s e) (snd fs) ctrl o)

not : Rule AST
not = do s <- Toolkit.location
         i <- ref
         symbol "!"
         o <- ref
         e <- Toolkit.location
         pure (NOT (newFC s e) i o)

gateType : Rule TyGateComb
gateType = do {symbol "&"; pure AND}
       <|> do {symbol "|"; pure IOR}
       <|> do {symbol "+"; pure XOR}

gateArrow : Rule TyGateComb
gateArrow
  = do symbol "-"
       symbol "["
       g <- gateType
       symbol "]"
       arrow
       pure g

gate : Rule AST
gate = do s <- Toolkit.location
          fs <- brackets $ commaSepBy2V ref
          ty <- gateArrow
          o <- ref
          e <- Toolkit.location
          pure (GATE (newFC s e) ty (snd fs) o)

conns : Rule (List1 AST)
conns
    = some (conn <* symbol ";")
  where
    conn : Rule  AST
    conn = not <|> mux <|> fanout <|> gate <|> connect

types : Rule ( List1 (FileContext, String, AST))
types = do
  keyword "types"
  some (typeDef <* symbol ";")

export
design : Rule AST
design = do
   ds <- optional (many doc)
   keyword "model"
   keyword "lightclick"
   tyStyleDecl <- optional (do {keyword "verilog"; pure SYSV})
   let typeStyle = fromMaybe HASKELL tyStyleDecl
   ts <- optional types
   (keyword "modules")
   ms <- some (moduleDef typeStyle <* symbol ";")
   (keyword "connections")
   cs <- conns
   eoi
   let cs' = foldr Seq End (forget cs)
   let ms' = foldr buildBind cs' (forget ms)
   let res = foldr buildBind ms' $ maybe Nil forget ts
   pure res
  where
   buildBind : (FileContext, String, AST) -> AST -> AST
   buildBind (fc, n,e) body = (Bind fc n e body)

export
fromString : (str  : String)
                  -> Either (ParseError Token) AST
fromString
  = parseString LightClickLexer design

export
fromFile : (fname : String)
                 -> IO (Either (ParseError Token) AST)
fromFile fname
  = do Right ast <- parseFile LightClickLexer design fname
         | Left err => (pure (Left err))
       pure (Right (setFileName fname ast))

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Control.Monad.State

import public Control.Monad.Identity
import public Control.Monad.Trans

||| A computation which runs in a context and produces an output
public export
interface Monad m => MonadState stateType (m : Type -> Type) | m where
    ||| Get the context
    get : m stateType
    ||| Write a new context/output
    put : stateType -> m ()

||| The transformer on which the State monad is based
public export
record StateT (stateType : Type) (m : Type -> Type) (a : Type) where
  constructor ST
  runStateT : stateType -> m (a, stateType)

public export
implementation Functor f => Functor (StateT stateType f) where
    map f (ST g) = ST (\st => map (mapFst f) (g st)) where
       mapFst : (a -> x) -> (a, s) -> (x, s)
       mapFst fn (a, b) = (fn a, b)

public export
implementation Monad f => Applicative (StateT stateType f) where
    pure x = ST (\st => pure (x, st))

    (ST f) <*> (ST a)
        = ST (\st =>
                do (g, r) <- f st
                   (b, t) <- a r
                   pure (g b, t))

public export
implementation Monad m => Monad (StateT stateType m) where
    (ST f) >>= k
        = ST (\st =>
                do (v, st') <- f st
                   let ST kv = k v
                   kv st')

public export
implementation Monad m => MonadState stateType (StateT stateType m) where
    get   = ST (\x => pure (x, x))
    put x = ST (\y => pure ((), x))

public export
implementation MonadTrans (StateT stateType) where
    lift x
        = ST (\st =>
                do r <- x
                   pure (r, st))

public export
implementation (Monad f, Alternative f) => Alternative (StateT st f) where
    empty = lift empty
    (ST f) <|> (ST g) = ST (\st => f st <|> g st)

public export
implementation HasIO m => HasIO (StateT stateType m) where
  liftIO io = ST $ \s => liftIO $ io_bind io $ \a => pure (a, s)

||| Apply a function to modify the context of this computation
public export
modify : MonadState stateType m => (stateType -> stateType) -> m ()
modify f
    = do s <- get
         put (f s)

||| Evaluate a function in the context held by this computation
public export
gets : MonadState stateType m => (stateType -> a) -> m a
gets f
    = do s <- get
         pure (f s)

||| The State monad. See the MonadState interface
public export
State : (stateType : Type) -> (ty : Type) -> Type
State = \s, a => StateT s Identity a

||| Unwrap a State monad computation.
public export
runState : StateT stateType Identity a -> stateType -> (a, stateType)
runState act = runIdentity . runStateT act

||| Unwrap a State monad computation, but discard the final state.
public export
evalState : State stateType a -> stateType -> a
evalState m = fst . runState m

||| Unwrap a State monad computation, but discard the resulting value.
public export
execState : State stateType a -> stateType -> stateType
execState m = snd . runState m


text:
module Example.Gen

import Data.List
import public Data.Vect

import public Example.Random

%default total

-------------------------------
--- Definition of the `Gen` ---
-------------------------------

public export %inline
Seed : Type
Seed = StdGen

-- No "size" parameter in this definition unlike the quickcheck's `Gen`!
public export
record Gen a where
  constructor MkGen
  unGen : Seed -> a

export
Functor Gen where
  map f (MkGen gena) = MkGen $ f . gena

export
Applicative Gen where
  pure x = MkGen $ const x
  (MkGen f) <*> (MkGen x) = MkGen $ \r =>
    let (r1, r2) = bimap (snd . next) (snd . next) $ split r in
    f r1 $ x r2

export
Monad Gen where
  (MkGen l) >>= f = MkGen $ \r =>
    let (r1, r2) = bimap (snd . next) (snd . next) $ split r in
    unGen (f $ l r1) r2

---------------------------------
--- Particular general `Gen`s ---
---------------------------------

export
covering
suchThat : Gen a -> (a -> Bool) -> Gen a
suchThat (MkGen f) p = MkGen \r => findOrDie r where
  findOrDie : Seed -> a
  findOrDie r = let v = f r in
                if p v then v else findOrDie $ snd $ next r

export
chooseAny : Random a => Gen a
chooseAny = MkGen $ fst . random

export
choose : Random a => (a, a) -> Gen a
choose bounds = MkGen $ fst . randomR bounds

export
variant : Nat -> Gen a -> Gen a
variant v gen = MkGen (\r => unGen gen $ getV (S v) r)
  where
    getV : Nat -> Seed -> Seed
    getV Z     r = r
    getV (S n) r = getV n $ snd $ split r

export
promote : (a -> Gen b) -> Gen (a -> b)
promote f = MkGen (\r, x => unGen (f x) r)

export
oneOf : {n : Nat} -> Vect (S n) (Gen a) -> Gen a
oneOf v = index !chooseAny v

export
pairOf : Gen a -> Gen b -> Gen (a, b)
pairOf l r = (,) <$> l <*> r

export
listOf : Gen a -> Gen (List a)
listOf g = sequence $ replicate !chooseAny g

export
vectOf : Gen a -> {n : Nat} -> Gen (Vect n a)
vectOf g = sequence $ replicate n g

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
module LeftPad

import Data.Vect
import Data.Vect.Quantifiers

simpleLeftPad : Char -> Int -> String -> Int
simpleLeftPad = 2

testing : String -> Type
testing "Give me text" = String
testing _              = Int

-- `minus` is saturating subtraction, so this works like we want it to
eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k
eq_max  n     Z    = rewrite minusZeroRight n in
                     rewrite plusZeroRightNeutral n in Refl
eq_max  Z    (S _) = Refl
eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl

-- The type here says "the result is" padded to (maximum k n), and is padding plus the original
leftPad : (x : a) -> (n : Nat) -> (xs : Vect k a)
       -> (ys : Vect (maximum k n) a ** m : Nat ** ys = replicate m x ++ xs)
leftPad {k} x n xs = rewrite eq_max n k in (replicate (n `minus` k) x ++ xs ** n `minus` k ** Refl)

-- helperProof : (m : Fin n) -> Vect n a -> Vect (cast m) a
-- helperProof FZ v = []
-- helperProof (FS x) (y :: xs) = y :: helperProof x xs

-- minusItselfZero : (a : Nat) -> (b : Nat) -> LTE b a -> Vect (a - b + b) Char = Vect a Char
-- minusItselfZero a b p = ?minusItselfZero_rhs1

-- leftPad : (c : Char)
--         -> (s : List Char)
--         -> (n : Nat)
--         -> (case isLTE (length s) (S n) of
--                  No _ => (x : List Char ** (x = s))
--                  Yes _ => (v : Vect (S n) Char
--                               **
--                               (y : Vect ((S n) - (length s)) Char ** (y ++ (fromList s) = v))))
-- leftPad padChar s n with (isLTE (length s) (S n))
--   leftPad padChar s n | No _ = (s ** Refl)
--   leftPad padChar s n | Yes lteproof = let paddingVec = replicate ((S n) - (length s)) padChar
--                                            newVec = paddingVec ++ (fromList s)
--                                        in rewrite sym (minusItselfZero (S n) (length s) lteproof) in (newVec ** (paddingVec ** ?jotain))

max_stars_repo_name: neurogoo/idris-intro-presentation

max_issues_repo_name: neurogoo/idris-intro-presentation

max_forks_repo_name: neurogoo/idris-intro-presentation


text:
module Test.Tutorial

import Pipes
import Test.Pipes

--------------------------------------------------------------------------------
-- A simple echo program
--------------------------------------------------------------------------------

echo_setup : IO ()
echo_setup = disableBuffering

echo_bad : IO ()
echo_bad = do
  putStr "in> "
  l <- getLine                  -- Read the standard input
  when (l /= "quit") $ do       -- Stop upon encountering "quit"
    putStrLn ("out> " ++ l)     -- Echo the string in standard output
    echo_bad

echo_good : IO ()
echo_good = runEffect $
  stdinLn "in> "                -- Read the standard input
    .| takingWhile (/= "quit")  -- Stop upon encountering "quit"
    .| mapping ("out> " ++)     -- Add the prompt to the string
    .| stdoutLn                 -- Echo the string in standard output

-- Slight modification to the program:
-- * Do not repeat the same sentence twice
-- * See how it gets bad on the loop side

echo_once_bad : IO ()
echo_once_bad = loop (const True) where
  loop : (String -> Bool) -> IO ()
  loop isDifferent = do
    putStr "in> "
    l <- getLine                  -- Read the standard input
    when (l /= "quit") $ do       -- Stop upon encountering "quit"
      when (isDifferent l) $      -- Remove consecutive repeating calls
        putStrLn ("out> " ++ l)   -- Echo the string in standard output
      loop (/= l)                 -- Loop with last read string

echo_once_good : IO ()
echo_once_good = runEffect $
  stdinLn "in> "                -- Read the standard input
    .| takingWhile (/= "quit")  -- Stop upon encountering "quit"
    .| deduplicating            -- Remove consecutive repeating calls
    .| mapping ("out> " ++)     -- Add the prompt to the string
    .| stdoutLn                 -- Echo the string in standard output

--------------------------------------------------------------------------------
-- Just exploiting laziness
--------------------------------------------------------------------------------

sum_with_traces : IO ()
sum_with_traces = do
  r <- runPipe $ each [1..10] .| tracing printLn .| fold (+) 0
  printLn r

sum_with_limit : IO ()
sum_with_limit = do
  r <- runPipe $ each [1..10] .| tracing printLn .| takingWhile (< 5) .| tracing printLn .| fold (+) 0
  printLn r

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

export
run_tutotial : IO ()
run_tutotial = do
  -- echo_example
  sum_with_traces
  sum_with_limit

max_stars_repo_name: QuentinDuval/IdrisPipes

max_issues_repo_name: QuentinDuval/IdrisPipes

max_forks_repo_name: QuentinDuval/IdrisPipes


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

||| This module defines an 'interpreter' for constructing Goal Graphs
||| from GRL esque languages.
module GRL.Builder

import public Data.AVL.Graph
import public Data.DList
import public Data.List

import GRL.Model
import GRL.IR
import GRL.Common
import GRL.Property.Element
import GRL.Property.Intention
import GRL.Property.Structure
import GRL.Pretty

import Debug.Error
import Debug.Trace

%access export
%default total

-- ---------------------------------------------------- [ Allowed Constructors ]

||| Create an empty model
emptyModel : GModel
emptyModel = mkEmptyGraph

-- ------------------------------------------------------------- [ Interpreter ]

|||  Interpt the IR types to get Goal Graph Types.
public export
interpTy : GTy -> Type
interpTy ELEM   = GoalNode
interpTy INTENT = GoalEdge
interpTy STRUCT = GoalEdge

||| Convert expressions from the IR to Goal Graph objects.
convExpr : {ty : GTy} -> GExpr ty -> interpTy ty
convExpr (Elem eTy t s)            = GNode eTy t s Nothing
convExpr (ILink IMPACTSty cTy _ _) = Contribution cTy
convExpr (ILink AFFECTSty cTy _ _) = Correlation  cTy
convExpr (SLink _ _ _)             = Decomp

-- --------------------------------------------------------------- [ Insertion ]
private
data ValidInsert : {ty : GTy} -> GExpr ty -> GModel -> Type where
  IsValidInsert : ValidInsert decl model

||| Perform the insertion of elements into the model.
private
insertElem : (e : GExpr ELEM)
          -> (m : GModel)
--          -> ValidInsert e m
          -> GModel
insertElem decl model =
  if not $ checkElemBool decl model
    then error $ with List unwords
            ["Bad Element arises from trying to insert\n\n\t"
            , show decl
            , "\n\ninto\n\n\t"
            , prettyModel model]
    else addNode (convExpr decl) model

-- ------------------------------------------------------------------- [ Links ]

||| Do the actual insertion of an edge into the model.
private
insertLink : GExpr ELEM -> GExpr ELEM -> Maybe GoalEdge -> GModel -> GModel
insertLink (Elem _ x _) (Elem _ y _) i m =
  case getGoalByTitle x m of
    Nothing  => m
    Just xID =>
      case getGoalByTitle y m of
        Nothing  => m
        Just yID => addValueEdge (xID, yID, i) m

-- --------------------------------------------------------------- [ Intention ]

||| Perform the insertion of label into the model.
private
insertIntent : (i : GExpr INTENT)
            -> (m : GModel)
--            -> ValidInsert i m
            -> GModel
insertIntent decl@(ILink ty val x y) model =
  case not $ checkIntentBool decl model of
      True => error $ with List unwords
             ["Bad Intent arises from trying to insert\n\n\t"
             , show decl
             , "\n\ninto\n\n\t"
             , prettyModel model]
      False => insertLink y x (Just (convExpr decl)) model

-- --------------------------------------------------------------- [ Structure ]
||| Do structure insertion.
private
insertStruct : (s : GExpr STRUCT)
            -> (m : GModel)
--            -> ValidInsert s m
            -> GModel
insertStruct decl@(SLink ty x ys) model =
    case not $ checkStructBool decl model of
      True => error $ with List unwords
             ["Bad Structure arises from trying to insert\n\n\t"
             , show decl
             , "\n\ninto\n\n\t",
             prettyModel model]
      False => newModel
  where
    doInsert : GModel -> GExpr ELEM -> GModel
    doInsert m y = insertLink x y (Just $ (convExpr (SLink ty x ys))) m

    model' : GModel
    model' = foldl doInsert model ys

    newModel : GModel
    newModel = updateGoalNode (\n => getTitle x == getNodeTitle n)
                   (\n => record {getStructTy = Just ty} n)
                   model'

-- ----------------------------------------------------------- [ Do the Insert ]

||| Insert a single declarations into the model.
insert : GRL expr => expr ty
                  -> GModel
                  -> GModel
insert {ty=ELEM}   decl model = insertElem   (mkElem decl)   model
insert {ty=INTENT} decl model = insertIntent (mkIntent decl) model
insert {ty=STRUCT} decl model = insertStruct (mkStruct decl) model

||| Insert many declarations of the same type into the model.
insertMany : GRL expr => List (expr ty)
                      -> GModel
                      -> GModel
insertMany Nil model = model
insertMany ds model = foldl doInsert model ds
  where
    doInsert : GRL expr => GModel
                        -> expr ty
                        -> GModel
    doInsert m x = insert x m

insertGroup : GRL expr => List (expr ELEM)
                       -> List (expr STRUCT)
                       -> List (expr INTENT)
                       -> GModel
                       -> GModel
insertGroup es ss is model =
    insertMany is (insertMany ss (insertMany es model))

||| Insert many different declarations into the model.
insertMany' : GRL expr => DList GTy expr ts
                       -> GModel
                       -> GModel
insertMany' Nil model = model
insertMany' ds model = DList.foldl doInsert model ds
  where
    doInsert : GRL expr => GModel
                        -> expr ty
                        -> GModel
    doInsert m x = insert x m

infixl 4 \=

||| Short hand for inserting a single declaration.
(\=) : GRL expr => (m : GModel)
                -> (d : expr ty)
                -> GModel
(\=) model decl = insert decl model

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
 module Lecture.GCD

switchLTE : (n: Nat) -> (m: Nat) -> (contra : (LTE n m) -> Void) -> LTE m n
switchLTE Z m contra = void (contra (LTEZero))
switchLTE (S k) Z contra = LTEZero
switchLTE (S k) (S j) contra =
  LTESucc (switchLTE k j previousContra) where
    previousContra = \evidence : (LTE k j) => contra (LTESucc evidence)

EuclidIndAux_rhs_2 : (x : LTE left right) -> Nat
EuclidIndAux_rhs_2 x = ?EuclidIndAux_rhs_2_rhs

gcdAux: (n: Nat) -> (m: Nat) -> (LTE m n) -> Nat
gcdAux n Z LTEZero = n
gcdAux (S right) (S left) (LTESucc x) = EuclidIndAux_rhs_2 x

gcd : Nat -> Nat -> Nat
gcd k j = case isLTE j k of
               (Yes prf) => gcdAux k j prf
               (No contra) => gcdAux j k (switchLTE j k contra)


text:
module Control.Category

import Data.Morphisms

public export
interface Category (0 cat : obj -> obj -> Type) | cat where
  id  : cat a a
  (.) : cat b c -> cat a b -> cat a c

public export
Category Morphism where
  id                = Mor id
  -- disambiguation needed below, because unification can now get further
  -- here with Category.(.) and it's only interface resolution that fails!
  (Mor f) . (Mor g) = Mor $ Basics.(.) f g

public export
Monad m => Category (Kleislimorphism m) where
  id                        = Kleisli (pure . id)
  (Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f

infixr 1 >>>

public export
(>>>) : Category cat => cat a b -> cat b c -> cat a c
f >>> g = g . f


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

||| The example from Amyot
module GRL.Test.Amyot

import GRL.Lang.GLang
import GRL.Eval

import GRL.Test.Utils

%default total

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

-- Service Provider
highPerf : SOFT
highPerf = mkSoft "High Performance"

lowCost : SOFT
lowCost  = mkSoft "Low Cost"

minChange : SOFT
minChange = mkSoft "Minimum Changes to Infrastructure"

maxHardware : SOFT
maxHardware = mkSoft "Maximun Hardware Utilisation"

highThrough : SOFT
highThrough = mkSoft "High Throughput"

minMsgEx : SOFT
minMsgEx = mkSoft "Minimum Message Exchange"

minSwitch : SOFT
minSwitch = mkSoft "Minimum Switch Load"

-- System

detDataLoc : GOAL
detDataLoc = mkGoal "Determine Data Location"

dataSCP : TASK
dataSCP = mkTask "Data in Service Control Point"

dataNewSNode : TASK
dataNewSNode = mkTask "Data in New Service Node"

installSNode : TASK
installSNode = mkTask "Install Service Node"  -- chang

serviceCentralSwitch : TASK
serviceCentralSwitch = mkTask "Service in Central Switch"

detSLoc : GOAL
detSLoc = mkGoal "Determine Service Location"

serviceInSCP : TASK
serviceInSCP = mkTask "Service in Service Control Point"

-- ------------------------------------------------------------------- [ Model ]
amyotModel : GModel
amyotModel = emptyModel
   \= highPerf               --  0
   \= lowCost                --  1
   \= minChange              --  2
   \= maxHardware            --  3
   \= highThrough            --  4
   \= minMsgEx               --  5
   \= minSwitch              --  6
   \= detDataLoc             --  7
   \= dataSCP                --  8
   \= dataNewSNode           --  9
   \= installSNode           -- 10
   \= serviceCentralSwitch   -- 11
   \= detSLoc                -- 12
   \= serviceInSCP           -- 13
   \= (minChange    ==> lowCost   | HELPS                  )
   \= (maxHardware  ~~> minChange | HELPS                  )
   \= (dataNewSNode ~~> minChange | HURTS                  )
   \= (dataSCP      ~~> minChange | HELPS                  )
   \= (minMsgEx     ==> highThrough | SOMEPOS              )
   \= (minSwitch    ==> highThrough | HELPS                )
   \= (serviceInSCP ==> minMsgEx | SOMENEG                 )
   \= (serviceInSCP ~~> minSwitch | MAKES                  )
   \= (serviceCentralSwitch ==> minMsgEx  | MAKES          )
   \= (serviceCentralSwitch ~~> minSwitch | BREAK          )
   \= (detSLoc      |= [serviceCentralSwitch, serviceInSCP])
   \= (detDataLoc   |= [dataNewSNode, dataSCP]             )
   \= (dataNewSNode &= [installSNode]                      )
   \= (highPerf     &= [maxHardware, highThrough]          )

-- ---------------------------------------------------------------- [ Strategy ]

strategy1 : Strategy
strategy1 = buildStrategy [ (maxHardware, WEAKSATIS)
                          , (dataSCP, SATISFIED)
                          , (serviceCentralSwitch, SATISFIED)]

strategy1ExpectedResults : Strategy
strategy1ExpectedResults = buildStrategy
    [ (lowCost,              WEAKSATIS)
    , (minChange,            WEAKSATIS)
    , (detDataLoc,           SATISFIED)
    , (highPerf,             NONE)
    , (maxHardware,          WEAKSATIS)
    , (highThrough,          NONE)
    , (minMsgEx,             SATISFIED)
    , (minSwitch,            DENIED)
    , (dataSCP,              SATISFIED)
    , (dataNewSNode,         NONE)
    , (installSNode,         NONE)
    , (serviceCentralSwitch, SATISFIED)
    , (detSLoc,              SATISFIED)
    , (serviceInSCP,         NONE)]

-- ---------------------------------------------------------------- [ Strategy ]

strategy2 : Strategy
strategy2 = buildStrategy
    [ (maxHardware, WEAKSATIS)
    , (serviceCentralSwitch, SATISFIED)
    , (installSNode, SATISFIED)]

strategy2ExpectedResults : Strategy
strategy2ExpectedResults = buildStrategy
    [ (lowCost,              NONE)
    , (minChange,            NONE)
    , (detDataLoc,           SATISFIED)
    , (highPerf,             NONE)
    , (maxHardware,          WEAKSATIS)
    , (highThrough,          NONE)
    , (minMsgEx,             SATISFIED)
    , (minSwitch,            DENIED)
    , (dataSCP,              NONE)
    , (dataNewSNode,         SATISFIED)
    , (installSNode,         SATISFIED)
    , (serviceCentralSwitch, SATISFIED)
    , (detSLoc,              SATISFIED)
    , (serviceInSCP,         NONE)]

-- ---------------------------------------------------------------- [ Strategy ]

strategy4 : Strategy
strategy4 = buildStrategy
    [ (maxHardware, WEAKSATIS)
    , (dataSCP, SATISFIED)
    , (serviceInSCP, SATISFIED)]

strategy4ExpectedResults : Strategy
strategy4ExpectedResults = buildStrategy
    [ (lowCost,              WEAKSATIS)
    , (minChange,            WEAKSATIS)
    , (detDataLoc,           SATISFIED)
    , (highPerf,             NONE)
    , (maxHardware,          WEAKSATIS)
    , (highThrough,          NONE)
    , (minMsgEx,             WEAKDEN)
    , (minSwitch,            SATISFIED)
    , (dataSCP,              SATISFIED)
    , (dataNewSNode,         NONE)
    , (installSNode,         NONE)
    , (serviceCentralSwitch, NONE)
    , (detSLoc,              SATISFIED)
    , (serviceInSCP,         SATISFIED)]

-- -------------------------------------------------------------------- [ Test ]
export partial
runTest : IO ()
runTest = do
  putStrLn "--> Amyot 2010 gem"

  putStrLn "Strategy 1:"
  doTest amyotModel strategy1 strategy1ExpectedResults

  putStrLn "Strategy 2:"
  doTest amyotModel strategy2 strategy2ExpectedResults

  putStrLn "Strategy 3: Not Cannot be replicated"

  putStrLn "Strategy 4:"
  doTest amyotModel strategy4 strategy4ExpectedResults

  putStrLn "Strategy 5: Not Cannot be replicated"
  putStrLn "Strategy 6: Not Cannot be replicated"

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


text:
module Text.Markup.Edda.Process.BLock

import Data.AVL.Dict

import Text.Markup.Edda.Model.Common
import Text.Markup.Edda.Model.Raw
import Text.Markup.Edda.Model.Processed

import Text.Markup.Edda.Process.Inline
import Text.Markup.Edda.Process.Squash
import Text.Markup.Edda.Process.Shunt
import Text.Markup.Edda.Process.Utils

%default covering
%access private

-- ----------------------------------------------------------- [ Refine Blocks ]

mutual

  refineBlock : EddaRaw BLOCK -> Edda BLOCK
  refineBlock HRule = HRule

  refineBlock Empty = Empty

  refineBlock (Heading d l t as) = Section d l (process t) as Nil

  refineBlock (Figure l c as img) =
      Figure l (process c) as url
    where
       url = case process [img] of
               Nil => Text "Shouldn't happen"
               (res::_) => res

  refineBlock (DList kvs) = DList $ map (\(k, vs) => (process k, process vs)) kvs

  refineBlock (TextBlock ParaTy        l c as t) = Para (process t)
  refineBlock (TextBlock QuotationTy   l c as t) = Quotation   l (process t)
  refineBlock (TextBlock TheoremTy     l c as t) = Theorem     l (process c) (process t)
  refineBlock (TextBlock CorollaryTy   l c as t) = Corollary   l (process c) (process t)
  refineBlock (TextBlock LemmaTy       l c as t) = Lemma       l (process c) (process t)
  refineBlock (TextBlock PropositionTy l c as t) = Proposition l (process c) (process t)
  refineBlock (TextBlock ProofTy       l c as t) = Proof       l (process c) (process t)
  refineBlock (TextBlock DefinitionTy  l c as t) = Definition  l (process c) (process t)
  refineBlock (TextBlock ExerciseTy    l c as t) = Exercise    l (process c) (process t)
  refineBlock (TextBlock NoteTy        l c as t) = Note        l (process c) (process t)
  refineBlock (TextBlock ProblemTy     l c as t) = Problem     l (process c) (process t)
  refineBlock (TextBlock QuestionTy    l c as t) = Question    l (process c) (process t)
  refineBlock (TextBlock RemarkTy      l c as t) = Remark      l (process c) (process t)
  refineBlock (TextBlock SolutionTy    l c as t) = Solution    l (process c) (process t)
  refineBlock (TextBlock ExampleTy     l c as t) = Example     l (process c) (process t)

  refineBlock (VerbBlock CommentTy l c as s) = Comment s
  refineBlock (VerbBlock ListingTy l c as s) = Listing l (process c)
                                                         (lookupSrcLang as)
                                                         (lookupSrcOpts as)
                                                         ((nubAttribute "src_lang" $ nubAttribute "src_opts" as))
                                                         s
  refineBlock (VerbBlock LiteralTy  l c as s) = Literal l (process c) s
  refineBlock (VerbBlock EquationTy l c as s) = Equation l s

  refineBlock (ListBlock NumberTy bs) = OList $ map process bs
  refineBlock (ListBlock BulletTy bs) = BList $ map process bs

  refineBlocks : List (EddaRaw BLOCK) -> List (Edda BLOCK)
  refineBlocks = map refineBlock

export
process : List (EddaRaw BLOCK) -> List (Edda BLOCK)
process = shunt . squash2 . refineBlocks

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Part2.Sec6_2_1_adder

{-
Think of this type as type level function
second case maps AdderType to a function type
-}
AdderType : (numargs : Nat) -> Type
AdderType Z = Int
AdderType (S k) = (nextArg : Int) -> AdderType k

||| adder numargs acc nums...
||| adder 0 : Int -> Int
||| adder 1 : Int -> Int -> Int
||| adder 2 : Int -> Int -> Int -> Int
||| adder 2 : Int -> Int -> Int -> Int
adder : (numargs : Nat) -> (acc : Int) -> AdderType numargs
adder Z acc = acc
adder (S k) acc = \nextArg => adder k (nextArg + acc)

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
-- This is based on the David Christianen's port of QuickCheck to Idris 1

module Example.Random

import Data.Fin

%default total

--------------------------------
--- Interface for seed types ---
--------------------------------

public export
interface RandomGen g where
  next : g -> (Int, g)
  genRange : g -> (Int,Int)
  split : g -> (g, g)

--------------------------------
--- Example of the seed type ---
--------------------------------

export
data StdGen = MkStdGen Int Int

export
someStdGen : StdGen
someStdGen = MkStdGen 23462 254334222987

export
Show StdGen where
  show (MkStdGen i j) = "MkStdGen " ++ show i ++ " " ++ show j

-- Blatantly stolen from Haskell
export
RandomGen StdGen where
  next (MkStdGen s1 s2) =
    let k : Int = s1 `div` 53668 in
    let s1' : Int  = 40014 * (s1 - k * 53668) - k * 12211 in
    let s1'' : Int = if s1' < 0 then s1' + 2147483563 else s1' in
    let k' : Int = s2 `div` 52774 in
    let s2' : Int = 40692 * (s2 - k' * 52774) - k' * 3791 in
    let s2'' : Int = if s2' <= 0 then s2' + 2147483399 else s2' in
    let z : Int = s1'' - s2'' in
    let z' : Int = if z < 1 then z + 2147483562 else z in
    (z', MkStdGen s1'' s2'')

  genRange _ = (0, 2147483562)
  split (MkStdGen s1 s2) =
    let gen' : StdGen = snd (next (MkStdGen s1 s2)) in
    let t1 : Int = case gen' of { MkStdGen a b => a } in
    let t2 : Int = case gen' of { MkStdGen a b => b } in
    let new_s1 : Int = if s1 >= 2147483562 || s1 < 1
                         then 1
                         else s1 + 1 in
    let new_s2 : Int = if s2 <= 1 || s2 >= 2147483398
                         then 2147483398
                         else s2 - 1 in
    let left : StdGen = MkStdGen (new_s1 - 1) t2 in
    let right : StdGen = MkStdGen t1 (new_s2 + 1) in
    (left, right)

--------------------------------------------------------
--- Types for which values can be randomly generated ---
--------------------------------------------------------

public export
interface Random a where
  randomR : RandomGen g => (a, a) -> g -> (a, g)
  random : RandomGen g => g -> (a, g)

--- Random Int ---

export
Random Int where
  random gen = next gen
  randomR (lo, hi) gen = if lo > hi
                           then assert_total $ randomR (hi, lo) gen
                           else case (f n 1 gen) of
                             (v, gen') => ((lo + v `mod` k), gen')
    where
      k : Int
      k = hi - lo + 1
      -- ERROR: b here (2^31-87) represents a baked-in assumption about genRange:
      b : Int
      b = 2147483561

      iLogBase : Int -> Int
      iLogBase i = if i < b then 1 else 1 + iLogBase (assert_smaller i (i `div` b))

      n : Int
      n = iLogBase k

      -- Here we loop until we've generated enough randomness to cover the range:
      f : Int -> Int -> g -> (Int, g)
      f 0 acc g = (acc, g)
      f n' acc g =
        let (x,g') = next g in
        -- We shift over the random bits generated thusfar (* b) and add in the new ones.
        f (assert_smaller n' $ n' - 1) (x + acc * b) g'

--- Random Nat ---

intToNat : Int -> Nat
intToNat = fromInteger . cast

export
Random Nat where
  randomR (lo, hi) = mapFst intToNat . randomR (cast lo, cast hi)
  random = mapFst intToNat . random

--- Random Unit ---

export
Random Unit where
  randomR ((), ()) gen = ((), snd $ next gen)
  random gen = ((), snd $ next gen)

--- Random Fin ---

finToInt : Fin n -> Int
finToInt = fromInteger . cast

intToFin : (n : Nat) -> Int -> Fin (S n)
intToFin n = restrict n . cast

export
{n : Nat} -> Random (Fin (S n)) where
  randomR (lo, hi) gen = mapFst (intToFin n) $ randomR (finToInt lo, finToInt hi) gen
  random = mapFst (intToFin n) . random

--- Random Char ---

export
Random Char where
  randomR (lo, hi) = mapFst chr . randomR (ord lo, ord hi)
  random = mapFst chr . random

--- Random Bool ---

boolToInt : Bool -> Int
boolToInt True = 1
boolToInt False = 0

intToBoolUni : Int -> Bool
intToBoolUni x = x `mod` 2 == 0

export
Random Bool where
  randomR (lo, hi) = mapFst intToBoolUni . randomR (boolToInt lo, boolToInt hi)
  random = mapFst intToBoolUni . random


text:
> module PNat.PNat

> import Syntax.PreorderReasoning

> import Nat.Positive

> %default total
> %access public export

> ||| Positive natural numbers as sigma types
> PNat : Type
> PNat = Subset Nat Positive

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


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

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

%default total

[grassBlockItemEntity']
Pickup GrassBlock.ItemEntity where
  collect self = new GrassBlock.Item self.base.item

[grassBlockVtbl']
Vtbl GrassBlock.ItemEntity where
  vtable (Pickup GrassBlock.ItemEntity) = Just grassBlockItemEntity
  vtable (Entity GrassBlock.ItemEntity) = Just %search
  vtable _ = Nothing

grassBlockItemEntity = grassBlockItemEntity'
grassBlockVtbl = grassBlockVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module BioCore.Sequence

import Data.List
import Data.Strings

%default total

--Qual--

public export
data Qual = ||| Quality data associate with sequence data.
            UnQual Int

public export
Show Qual where
  show (UnQual x) = show x

public export
Eq Qual where
  (==) (UnQual x) (UnQual y) = True
  (==) _          _          = False

public export
Ord Qual where
  compare (UnQual x) (UnQual y) = compare x y

public export
Num Qual where
  fromInteger = UnQual . fromInteger

public export
extractUnQual : Qual -> Int
extractUnQual (UnQual unQual) = unQual

--------

--Offset--

public export
data Offset = ||| The offset in the sequence data.
              UnOff Int

public export
Show Offset where
  show (UnOff x) = show x

public export
Eq Offset where
  (==) (UnOff x) (UnOff y) = True
  (==) _          _        = False

public export
Ord Offset where
  compare (UnOff x) (UnOff y) = compare x y

public export
Num Offset where
  fromInteger = UnOff . fromInteger

public export
extractUnOff : Offset -> Int
extractUnOff (UnOff unOff) = unOff

----------

--SeqData--

public export
data SeqData = ||| Sequence data are List String of ASCII characters.
               UnSD String

public export
Show SeqData where
  show (UnSD x) = show x

public export
Eq SeqData where
  (==) (UnSD x) (UnSD y) = True
  (==) _          _      = False

public export
Ord SeqData where
  compare (UnSD x) (UnSD y) = compare x y

public export
extractUnSD : SeqData -> String
extractUnSD (UnSD unSD) = unSD

-----------

--SeqLabel--

public export
data SeqLabel = ||| Sequence labels are List String of ASCII characters.
                UnSL String

public export
Show SeqLabel where
  show (UnSL x) = show x

public export
Eq SeqLabel where
  (==) (UnSL x) (UnSL y) = True
  (==) _          _      = False

public export
Ord SeqLabel where
  compare (UnSL x) (UnSL y) = compare x y

public export
extractUnSL : SeqLabel -> String
extractUnSL (UnSL unSL) = unSL

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

--QualData--

public export
data QualData = ||| The quality data associated with the sequence data.
                UnQD String

public export
Show QualData where
  show (UnQD x) = show x

public export
Eq QualData where
  (==) (UnQD x) (UnQD y) = True
  (==) _          _      = False

public export
Ord QualData where
  compare (UnQD x) (UnQD y) = compare x y

public export
extractUnQD : QualData -> String
extractUnQD (UnQD unQD) = unQD

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

public export
toFastaSeqData : SeqLabel -> SeqData -> String
toFastaSeqData (UnSL seqlabel) (UnSD seqdata) = ">"      ++
                                                seqlabel ++
                                                "\n"     ++
                                                (wrapSeqData seqdata (unpack seqdata))
  where wrapSeqData : String -> List Char -> String
        wrapSeqData _ []       = ""
        wrapSeqData s (_::ss') = if isNil (unpack s)
                                   then ""
                                   else let (ln,rest) = splitAt 60 (unpack s)
                                          in (pack ln) ++
                                             "\n"      ++
                                             (wrapSeqData (pack rest) ss')

public export
toFastaQual : SeqLabel -> QualData -> String
toFastaQual (UnSL seqlabel) (UnQD qualdata) = ">"      ++
                                              seqlabel ++
                                              "\n"     ++
                                              (wrapqualdata qualdata (unpack qualdata))
  where wrapqualdata : String -> List Char -> String
        wrapqualdata _ []       = ""
        wrapqualdata s (_::ss') = if isNil (unpack s)
                                    then ""
                                    else let (ln,rest) = splitAt 20 (unpack s)
                                           in (pack ln) ++
                                              "\n"      ++
                                              (wrapqualdata (pack rest) ss')

max_stars_repo_name: Matthew-Mosior/biocore-idris

max_issues_repo_name: Matthew-Mosior/biocore-idris

max_forks_repo_name: Matthew-Mosior/biocore-idris


text:
||| An example EDSL to describe multiple file interactions, and a
||| handler for the IO computation context.
|||
module Example.Files

import public Resources

%access public export
%default total

namespace AbstractST
  ||| Files are open for reading or writing.
  public export
  data FMode = R | W

  ||| Abstract state.
  public export
  data FileState = Open FMode | Closed

  public export
  data FH = MkFH

  {- [ NOTE ]

  Type synonym to make writing the language easier.

  -}

  public export
  FHStateType : FH -> Type
  FHStateType _ = FileState

  public export
  FileHandle : Type
  FileHandle = Var FH MkFH

  public export
  FileStateItem : Type
  FileStateItem = StateItem FH FHStateType MkFH

{- [ NOTE ]

Predicates to reason about file handlers.

-}
namespace Predicates
  ||| Reason about a file handle's current abstract state.
  public export
  data IsOpenFor : (hdl  : Var FH MkFH)
                -> (mode : FMode)
                -> (item : FileStateItem)
                -> Type where
    FileIsOpenFor : (m : FMode) -> IsOpenFor hdl m (MkStateItem MkFH hdl (Open m))

  ||| Does the abstract state belong to the given handle.
  public export
  data IsHandle : (hdl : Var FH MkFH)
               -> (item : FileStateItem)
               -> Type where
    FileExists : (hdl : Var FH MkFH) -> IsHandle hdl (MkStateItem MkFH hdl st)

{- [ NOTE ]

Functions to update FileHandle abstract states.

-}
namespace Updates

  public export
  closeHandle : (item : FileStateItem)
             -> (prf  : IsOpenFor hdl m item)
             -> FileStateItem
  closeHandle (MkStateItem MkFH label _) prf = MkStateItem MkFH label Closed

namespace Definition

{- [ NOTE ]

Type level functions to perform state transitions and update the type-level context.

-}

  public export
  openTrans : Either FileError (Var FH MkFH)
           -> FMode
           -> Context FH FHStateType
           -> Context FH FHStateType
  openTrans (Left _)  _  old = old
  openTrans (Right x) fm old = MkStateItem MkFH x (Open fm) :: old

  public export
  readTrans : Either FileError String
           -> (old : Context FH FHStateType)
           -> InContext MkFH (IsOpenFor hdl R) old
           -> Context FH FHStateType
  readTrans (Right _) old _   = old
  readTrans (Left  _) old prf = update old prf (\i,p => closeHandle i p)

  public export
  writeTrans : Maybe FileError
           -> (old : Context FH FHStateType)
           -> (prf : InContext MkFH (IsOpenFor hdl W) old)
           -> Context FH FHStateType
  writeTrans Nothing  old _   = old
  writeTrans (Just _) old prf = update old prf (\i,p => closeHandle i p)

  ||| The language definition for working with multiple file handlers.
  public export
  data Files : Lang FH FHStateType where
      ||| Open the given file in the presented mode.
      Open : (fname : String)
          -> (fm : FMode)
          -> Files (Either FileError (Var FH MkFH))
                   old
                   (\res => openTrans res fm old)

      ||| Read a line from the open (for reading) file handle.
      Read : (hdl : Var FH MkFH)
          -> (prf : InContext MkFH (IsOpenFor hdl R) old)
          -> Files (Either FileError String) old (\res => readTrans res old prf)

      ||| Write the given String to the open (for writing) file handle.
      Write : (hdl : Var FH MkFH)
           -> (msg : String)
           -> (prf : InContext MkFH (IsOpenFor hdl W) old)
           -> Files (Maybe FileError) old (\res => writeTrans res old prf)

      ||| Close the open file handle
      Close : (hdl : Var FH MkFH)
           -> (prf : InContext MkFH (IsHandle hdl) old)
           -> Files () old (const $ drop old prf)

      ||| Print stuff.
      PrintLn : Show a => a -> Files () old (const old)

{- [ NOTE ]

A high-level API to embedd language expressions within `LangM`, and calculate language proofs.

-}
namespace API
  public export
  FILES : LANG FH FHStateType
  FILES = MkLang FH FHStateType Files

  ||| Open the given file in the presented mode.
  public export
  openFile : (fname : String)
          -> (fm : FMode)
          -> LangM m (Either FileError (Var FH MkFH)) FILES old (\res => openTrans res fm old)
  openFile fname fm = expr $ Open fname fm

  ||| Read a line from the open (for reading) file handle.
  public export
  readString : (hdl : Var FH MkFH)
            -> {auto prf : InContext MkFH (IsOpenFor hdl R) old}
            -> LangM m (Either FileError String) FILES old (\res => readTrans res old prf)
  readString hdl {prf} = expr (Read hdl prf)

  ||| Write the given String to the open (for writing) file handle.file handle.
  public export
  writeString : (hdl : Var FH MkFH)
             -> String
             -> {auto prf : InContext MkFH (IsOpenFor hdl W) old}
             -> LangM m (Maybe FileError) FILES old (\res => writeTrans res old prf)
  writeString hdl str {prf} = expr (Write hdl str prf)

  ||| Close the open file handle
  public export
  closeFile : (hdl : Var FH MkFH)
           -> {auto prf : InContext MkFH (IsHandle hdl) old}
           -> LangM m () FILES old (const $ drop old prf)
  closeFile hdl {prf} = expr (Close hdl prf)

  ||| Print showable things on a line.
  public export
  printLn : Show a
         => a
         -> LangM m () FILES old (const old)
  printLn a = expr (PrintLn a)

  ||| Type given to programs to ensure that they are closed.
  |||
  public export
  Files : (m : Type -> Type) -> Type -> Type
  Files m type = LangM m type FILES Nil (const Nil)

{- [ NOTE]

A handler for the `IO` context.

-}
namespace ContextIO

  ||| Files are Files
  public export
  RealVar FH where
    CalcRealType MkFH = File

  ||| How to handle files, in which we map high-level operations to unsafe ones from Idris' prelude.
  public export
  Handler FH FHStateType Files () IO where
    handle env (Open fname fm) acc cont = do
      let m = case fm of {R => Read; W => WriteTruncate}
      res <- openFile fname m
      case res of
        Left err => cont (Left  err)   env             acc
        Right fh => cont (Right MkVar) (MkTag fh::env) acc

    handle env (Read hdl prf) acc cont = do
      let MkTag fh = lookup env prf
      res <- fGetLine fh
      case res of
        Left err  => cont (Left  err) (update env prf (\i,p => closeHandle i p)) acc
        Right str => cont (Right str) env                                        acc

    handle env (Write hdl str prf) acc cont = do
      let MkTag fh = lookup env prf
      res <- fPutStrLn fh str
      case res of
        Left err  => cont (Just err) (update env prf (\i,p => closeHandle i p)) acc
        Right _   => cont Nothing    env                                        acc

    handle env (Close hdl prf) acc cont = do
      let MkTag fh = lookup env prf
      closeFile fh
      cont () (drop env prf) acc

    handle env (PrintLn a) acc cont = do
       printLn a
       cont () env acc

||| A sample program to copy a string from one file to another.
|||
copy : (a,b : String) -> Files m (Maybe FileError)
copy a b = do
  Right fh <- openFile a R | Left err => do {printLn err; pure (Just err)}
  Right str <- readString fh | Left err => do {printLn err; closeFile fh; pure (Just err)}
  closeFile fh
  Right fh1 <- openFile b W | Left err => do {printLn err; pure (Just err)}
  res <- writeString fh1 str
  case res of
    Nothing  => do {closeFile fh1; pure Nothing}
    Just err => do {printLn err; closeFile fh1; pure (Just err)}

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

max_stars_repo_name: border-patrol/resources

max_issues_repo_name: border-patrol/resources

max_forks_repo_name: border-patrol/resources


text:
module InvParComb

%default total

data IPC : (listtype : Type) -> (valtype : Type) -> Type where
  MkIPC : (parse : (List listtype -> Maybe (valtype, List listtype))) ->
          (compose : (valtype -> Maybe (List listtype))) ->
          IPC listtype valtype

ipc_parse : IPC a b -> List a -> Maybe (b, List a)
ipc_parse (MkIPC p c) = p

ipc_compose : IPC a b -> b -> Maybe (List a)
ipc_compose (MkIPC p c) = c

-- Functor, kind of
ipc_fmap : (fp : a -> b) -> (fc : b -> a) -> IPC c a -> IPC c b
ipc_fmap fp fc (MkIPC parse compose) = MkIPC pf cf
  where
    pf l = do
      (x, rest) <- parse l
      return (fp x, rest)
    cf x = compose $ fc x

-- Almost applicative
ipc_pure : (Eq a, Eq b) => a -> IPC a a
ipc_pure v = MkIPC pf cf
  where
    pf l = Just (v, l)
    cf x = if x == v then Just [v] else Nothing

ipc_empty : IPC a b
ipc_empty = MkIPC (\x => Nothing) (\x => Just $ List.Nil)

ipc_item : IPC a a
ipc_item = MkIPC pf cf
  where
    pf [] = Nothing
    pf (x :: xs) = Just (x, xs)
    cf x = Just [x]

ipc_fail : IPC a a
ipc_fail = MkIPC (const Nothing) (const Nothing)

-- Alternative
mplus : Maybe a -> Lazy (Maybe a) -> Maybe a
mplus Nothing m2 = m2
mplus j m2 = j

ipc_alt : IPC a b -> IPC a b -> IPC a b
ipc_alt (MkIPC p1 c1) (MkIPC p2 c2) = MkIPC pf cf
  where
    pf l = mplus (p1 l) (p2 l)
    cf x = mplus (c1 x) (c2 x)

-- Tuple
ipc_tup : IPC a b -> IPC a c -> IPC a (b, c)
ipc_tup (MkIPC p1 c1) (MkIPC p2 c2) = MkIPC pf cf
  where
   pf l = do
     (x, rest) <- p1 l
     (y, ret) <- p2 rest
     return ((x, y), ret)
   cf (x, y) = do
     l1 <- c1 x
     l2 <- c2 y
     return (l1 ++ l2)

-- Vector
ipc_nilv : IPC a (Vect 0 b)
ipc_nilv = MkIPC pf cf
  where
    pf l = Just $ ([], l)
    cf x = Just []

ipc_consv : IPC a b -> IPC a (Vect n b) -> IPC a (Vect (S n) b)
ipc_consv (MkIPC p1 c1) (MkIPC p2 c2) = MkIPC pf cf
  where
    pf l = do
      (x, rest) <- p1 l
      (xs, ret) <- p2 rest
      return (x :: xs, ret)
    cf (x :: xs) = do
      l1 <- c1 x
      l2 <- c2 xs
      return (l1 ++ l2)

ipc_rep : (n : Nat) -> IPC a b -> IPC a (Vect n b)
ipc_rep Z p = ipc_nilv
ipc_rep (S k) p = ipc_consv p (ipc_rep k p)

-- List
ipc_nil : (Eq a, Eq b) => IPC a (List b)
ipc_nil = MkIPC pf cf
  where
    pf l = Just ([], l)
    cf [] = Just []
    cf l = Nothing

ipc_cons : (Eq a, Eq b) => IPC a b -> Lazy (IPC a (List b)) -> IPC a (List b)
ipc_cons (MkIPC p1 c1) (MkIPC p2 c2) = MkIPC pf cf
  where
    pf l = do
      (x, rest) <- p1 l
      (xs, ret) <- p2 rest
      return (x :: xs, ret)
    cf [] = Nothing
    cf (x :: xs) = do
      l1 <- c1 x
      l2 <- c2 xs
      return (l1 ++ l2)

max_stars_repo_name: defanor/parcomb

max_issues_repo_name: defanor/parcomb

max_forks_repo_name: defanor/parcomb


text:
makeId : (a : Type) -> (a -> a)
makeId t = (\x : t => x)

pairwiseApply : (b : Type, c : Type) -> ((a : Type) -> a -> a) -> (b, c) -> (b, c)
pairwiseApply t1 t2 typeFun (b, c) = (typeFun t1 b, typeFun t2 c)

generalizedApply : (b : Type) -> (c : Type) -> (d : Type) -> (e : Type) -> ((a : Type) -> (a' : Type) -> a -> a') -> (b, c) -> (d, e)
generalizedApply tb tc td te tF (vB, vC) = (tF tb td vB, tF tc te vC)

ShowBox : Type
ShowBox = (b : Type) -> ((a : Type) -> ((Show a) => a -> b )) -> b

makeShowBox : (a : Type) -> (Show a) => a -> ShowBox
makeShowBox t a = \b => \f => f t a

applyShowBox : (b : Type) -> ((a : Type) -> ((Show a) => a -> b )) -> ShowBox -> b
applyShowBox b f box = box b f

fShow : (a : Type) -> ((Show a) => a -> String)
fShow t a = show a

implementation Show ShowBox where
    show box = box String fShow

a : ShowBox
a = makeShowBox Int 5

b : ShowBox
b = makeShowBox String "Hello, world!"

c : ShowBox
c = makeShowBox ShowBox (makeShowBox String "Box within a box!")

d : List ShowBox
d = [a, b, c]

e : ShowBox
e = makeShowBox (List ShowBox) d

main : IO ()
main = print e

doubleShow : (a : Type) -> (Show a) => a -> String
doubleShow t a = fShow t a ++ fShow t a


text:
module Control.Monad.Logic.Interface

infixl 1 >>-

||| inverse of `split`, i.e. `split xz >>= reflect = xz`
public export
reflect : Alternative m => Maybe (a, m a) -> m a
reflect Nothing = empty
reflect (Just (a, m)) = pure a <|> m

public export
interface (Monad m, Alternative m) => MonadLogic m where
  ||| basically `uncons`
  split : m a -> m (Maybe (a, m a))
  ||| fair disjunction, basically `(<|>)` but implemented in such a way to allow for infinite lists at the cost of sacrificing associativity
  interleave : m a -> Lazy (m a) -> m a
  ||| fair conjunction, basically `(>>=)` but implemented in such a way to allow for infinite lists at the cost of sacrificing distributivity, and do syntax
  (>>-) : m a -> (a -> m b) -> m b

  interleave xz yz = split xz >>= \case
    Nothing => yz
    Just (x, xs) => pure x <|> interleave yz xs

  xz >>- react = split xz >>= \case
    Nothing => empty
    Just (x, xs) => interleave (react x) (xs >>- react)


text:
module Stlc

import Expr
import Logic
import Maps

%access public export

%default total

data Ty : Type where
  TyBool : Ty
  TyArrow : Ty -> Ty -> Ty

Uninhabited (TyArrow ty _ = ty) where
  uninhabited Refl impossible

data Tm : Type where
  Var : Id -> Tm
  App : Tm -> Tm -> Tm
  Abs : Id -> Ty -> Tm -> Tm
  Tru : Tm
  Fls : Tm
  Test : Tm -> Tm -> Tm -> Tm

idB : Tm
idB = Abs X TyBool (Var X)

idBB : Tm
idBB = Abs X (TyArrow TyBool TyBool) (Var X)

idBBBB : Tm
idBBBB = Abs X (TyArrow (TyArrow TyBool TyBool) (TyArrow TyBool TyBool)) (Var X)

k : Tm
k = Abs X TyBool (Abs Y TyBool (Var X))

notB : Tm
notB = Abs X TyBool (Test (Var X) Fls Tru)

data Value : Tm -> Type where
  V_Abs : Value (Abs x ty t)
  V_Tru : Value Tru
  V_Fls : Value Fls

subst : (x : Id) -> (s : Tm) -> (t : Tm) -> Tm
subst x s (Var y) with (decEq x y)
  subst x s (Var y) | Yes _ = s
  subst x s (Var y) | No _ = Var y
subst x s (App t1 t2) = App (subst x s t1) (subst x s t2)
subst x s (Abs y ty t) with (decEq x y)
  subst x s (Abs y ty t) | Yes _ = Abs y ty t
  subst x s (Abs y ty t) | No _ = Abs y ty (subst x s t)
subst x s Tru = Tru
subst x s Fls = Fls
subst x s (Test t1 t2 t3) = Test (subst x s t1) (subst x s t2) (subst x s t3)

syntax "<" [x] ":=" [s] ">" [t] = subst x s t

data Substi : (s : Tm) -> (x : Id) -> Tm -> Tm -> Type where
  S_Var1 : Substi s x (Var x) s
  S_Var2 : Not (x = y) -> Substi s x (Var y) (Var y)
  S_App : Substi s x t1 t1' -> Substi s x t2 t2' ->
          Substi s x (App t1 t2) (App t1' t2')
  S_Abs1 : Substi s x (Abs x ty t) (Abs x ty t)
  S_Abs2 : Not (x = y) -> Substi s x t t' ->
           Substi s x (Abs y ty t) (Abs y ty t')
  S_Tru : Substi s x Tru Tru
  S_Fls : Substi s x Fls Fls
  S_Test : Substi s x t1 t1' -> Substi s x t2 t2' -> Substi s x t3 t3' ->
           Substi s x (Test t1 t2 t3) (Test t1' t2' t3')

substi_correct : (subst x s t = t') ↔ (Substi s x t t')
substi_correct = (forward, backward)
where forward : subst x s t = t' -> Substi s x t t'
      forward {x} {t = Var y} prf with (decEq x y)
        forward {x} {t = Var y} prf | Yes prf' = rewrite sym prf
                                                 in rewrite prf'
                                                 in S_Var1
        forward {x} {t = Var y} prf | No contra = rewrite sym prf
                                                  in S_Var2 contra
      forward {x} {s} {t = App t1 t2} prf with (subst x s t1) proof t1_prf
        forward {x} {s} {t = App t1 t2} prf | t1'
          with (subst x s t2) proof t2_prf
            forward {x} {s} {t = App t1 t2} prf | t1' | t2' =
              rewrite sym prf
              in S_App (forward (sym t1_prf)) (forward (sym t2_prf))
      forward {x} {s} {t = Abs y ty t} prf with (decEq x y)
        forward {x} {s} {t = Abs y ty t} prf | Yes prf' =
          rewrite sym prf
          in rewrite prf'
          in S_Abs1
        forward {x} {s} {t = Abs y ty t} prf | No contra
          with (subst x s t) proof t_prf
            forward {x} {s} {t = Abs y ty t} prf | No contra | t' =
              rewrite sym prf
              in S_Abs2 contra (forward (sym t_prf))
      forward {t = Tru} prf = rewrite sym prf in S_Tru
      forward {t = Fls} prf = rewrite sym prf in S_Fls
      forward {x} {s} {t = Test t1 t2 t3} prf with (subst x s t1) proof t1_prf
        forward {x} {s} {t = Test t1 t2 t3} prf | t1'
          with (subst x s t2) proof t2_prf
            forward {x} {s} {t = Test t1 t2 t3} prf | t1' | t2'
              with (subst x s t3) proof t3_prf
                forward {x} {s} {t = Test t1 t2 t3} prf | t1' | t2' | t3' =
                  rewrite sym prf
                  in S_Test (forward (sym t1_prf))
                            (forward (sym t2_prf))
                            (forward (sym t3_prf))
      backward : Substi s x t t' -> subst x s t = t'
      backward {x} S_Var1 with (decEq x x)
        backward {x} S_Var1 | Yes _ = Refl
        backward {x} S_Var1 | No contra = absurd (contra Refl)
      backward {x} {t=Var y} (S_Var2 contra) with (decEq x y)
        backward {x} {t=Var y} (S_Var2 contra) | Yes prf = absurd (contra prf)
        backward {x} {t=Var y} (S_Var2 contra) | No _ = Refl
      backward (S_App s1 s2) = rewrite backward s1
                               in rewrite backward s2
                               in Refl
      backward {x} S_Abs1 with (decEq x x)
        backward {x} S_Abs1 | Yes _ = Refl
        backward {x} S_Abs1 | No contra = absurd (contra Refl)
      backward {x} {t=Abs y _ _} (S_Abs2 contra s) with (decEq x y)
        backward {x} {t=Abs y _ _} (S_Abs2 contra s) | Yes prf =
          absurd (contra prf)
        backward {x} {t=Abs y _ _} (S_Abs2 contra s) | No _ =
          rewrite backward s in Refl
      backward S_Tru = Refl
      backward S_Fls = Refl
      backward (S_Test s1 s2 s3) = rewrite backward s1
                                   in rewrite backward s2
                                   in rewrite backward s3
                                   in Refl

data Step : Tm -> Tm -> Type where
  ST_AppAbs : Value v -> Step (App (Abs x ty t) v) (subst x v t)
  ST_App1 : Step t1 t1' -> Step (App t1 t2) (App t1' t2)
  ST_App2 : Value v1 -> Step t2 t2' -> Step (App v1 t2) (App v1 t2')
  ST_TestTru : Step (Test Tru t1 t2) t1
  ST_TestFls : Step (Test Fls t1 t2) t2
  ST_Test : Step t1 t1' -> Step (Test t1 t2 t3) (Test t1' t2 t3)

Uninhabited (Step Tru _) where
  uninhabited (ST_AppAbs _) impossible
  uninhabited (ST_App1 _) impossible
  uninhabited (ST_App2 _ _) impossible
  uninhabited ST_TestTru impossible
  uninhabited ST_TestFls impossible
  uninhabited (ST_Test _) impossible

Uninhabited (Step Fls _) where
  uninhabited (ST_AppAbs _) impossible
  uninhabited (ST_App1 _) impossible
  uninhabited (ST_App2 _ _) impossible
  uninhabited ST_TestTru impossible
  uninhabited ST_TestFls impossible
  uninhabited (ST_Test _) impossible

Uninhabited (Step (Abs _ _ _) _) where
  uninhabited (ST_AppAbs _) impossible
  uninhabited (ST_App1 _) impossible
  uninhabited (ST_App2 _ _) impossible
  uninhabited ST_TestTru impossible
  uninhabited ST_TestFls impossible
  uninhabited (ST_Test _) impossible

infix 4 -+>

(-+>) : Tm -> Tm -> Type
(-+>) = Step

MultiStep : Tm -> Tm -> Type
MultiStep = Multi Step

infix 4 -+>*

(-+>*) : Tm -> Tm -> Type
(-+>*) = MultiStep

step_example_1 : App Stlc.idBB Stlc.idB -+>* Stlc.idB
step_example_1 = MultiStep (ST_AppAbs V_Abs) MultiRefl

step_example_2 : App Stlc.idBB (App Stlc.idBB Stlc.idB) -+>* Stlc.idB
step_example_2 = MultiStep (ST_App2 V_Abs (ST_AppAbs V_Abs))
               $ MultiStep (ST_AppAbs V_Abs)
               $ MultiRefl

step_example_3 : App (App Stlc.idBB Stlc.notB) Tru -+>* Fls
step_example_3 = MultiStep (ST_App1 (ST_AppAbs V_Abs))
               $ MultiStep (ST_AppAbs V_Tru)
               $ MultiStep ST_TestTru
               $ MultiRefl

step_example_4 : App Stlc.idBB (App Stlc.notB Tru) -+>* Fls
step_example_4 = MultiStep (ST_App2 V_Abs (ST_AppAbs V_Tru))
               $ MultiStep (ST_App2 V_Abs ST_TestTru)
               $ MultiStep (ST_AppAbs V_Fls)
               $ MultiRefl

step_example_5 : App (App Stlc.idBBBB Stlc.idBB) Stlc.idB -+>* Stlc.idB
step_example_5 = MultiStep (ST_App1 (ST_AppAbs V_Abs))
               $ MultiStep (ST_AppAbs V_Abs)
               $ MultiRefl

Context : Type
Context = PartialMap Ty

data HasType : Context -> Tm -> Ty -> Type where
  T_Var : gamma x = Just ty -> HasType gamma (Var x) ty
  T_Abs : HasType (update x ty11 gamma) t12 ty12 ->
          HasType gamma (Abs x ty11 t12) (TyArrow ty11 ty12)
  T_App : HasType gamma t1 (TyArrow ty11 ty12) ->
          HasType gamma t2 ty11 ->
          HasType gamma (App t1 t2) ty12
  T_Tru : HasType gamma Tru TyBool
  T_Fls : HasType gamma Fls TyBool
  T_Test : HasType gamma t1 TyBool ->
           HasType gamma t2 ty ->
           HasType gamma t3 ty ->
           HasType gamma (Test t1 t2 t3) ty

typing_example_1 : HasType Maps.empty
                           (Abs x TyBool (Var x))
                           (TyArrow TyBool TyBool)
typing_example_1 {x} = T_Abs (T_Var (rewrite sym (beq_id_refl x) in Refl))

typing_example_2 : HasType Maps.empty
                           (Abs X TyBool
                                (Abs Y (TyArrow TyBool TyBool)
                                     (App (Var Y) (App (Var Y) (Var X)))))
                           (TyArrow TyBool
                                    (TyArrow (TyArrow TyBool TyBool)
                                             TyBool))
typing_example_2 =
  T_Abs (T_Abs (T_App (T_Var Refl) (T_App (T_Var Refl) (T_Var Refl))))

typing_example_3 : (  ty : Ty
                   ** HasType Maps.empty
                              (Abs X (TyArrow TyBool TyBool)
                                   (Abs Y (TyArrow TyBool TyBool)
                                        (Abs Z TyBool
                                             (App (Var Y)
                                                  (App (Var X) (Var Z))))))
                              ty )
typing_example_3 = ( TyArrow (TyArrow TyBool TyBool)
                             (TyArrow (TyArrow TyBool TyBool)
                                      (TyArrow TyBool TyBool))
                   ** T_Abs
                        (T_Abs (T_Abs (T_App (T_Var Refl)
                                             (T_App (T_Var Refl)
                                                    (T_Var Refl))))))

typing_nonexample_3 : Not (  ty1 : Ty ** ty2 : Ty
                          ** HasType Maps.empty
                                     (Abs X ty1 (App (Var X) (Var X)))
                                     ty2 )
typing_nonexample_3 (_ ** _ ** T_Abs (T_App (T_Var prf1) (T_Var prf2))) =
  absurd (justInjective (trans (sym prf1) prf2))


text:
module Extra.Proof

export
unsafeRefl : {0 a, b : t} -> a === b
unsafeRefl = believe_me (the (a === a) Refl)

-- TODO: I can't do rewrite on linear types? Am I missing something
||| A poor-man's linear version of rewrite/replace
public export
replace1 : forall x, y, p . (0 rule : x = y) -> (1 _ : p x) -> p y
replace1 prf = assert_linear (replace {p = p} prf)

||| Crash the program
export total
%foreign "scheme:lambda (x) (blodwen-error-quit x)"
crash : String -> a