text:
module Main

import Control.Isomorphism
import Regex.Type

infixl 7 :.:
infixl 6 :|:
infixl 6 :&:

%default total

mutual
  ||| The type of witnesses to a string matching `r+` for some regular
  ||| expression `r`, where `+` is the Kleene plus operator.
  data LPlus : List tok -> Regex tok -> Type where
    SP : (DecEq tok)
         => Matches {tok} s r
         -> LPlus {tok} s r
    CP : (DecEq tok)
         => (s1 ++ s2 = s)
         -> Matches {tok} s1 r
         -> LPlus {tok} s2 r
         -> LPlus {tok} s r

  ||| Returns a type of witnesses to the fact that a given regular expression
  ||| is matched by a given list of tokens.
  Matches : (DecEq tok) => List tok -> Regex tok -> Type
  Matches {tok} = Lang
    where
      Lang : List tok -> Regex tok -> Type
      Lang _  Ø         = Void
      Lang [] Ɛ         = ()
      Lang _  Ɛ         = Void
      Lang x  (Tok t)   = (x = [t])
      Lang x  (Comp r)  = Lang x r -> Void
      Lang [] (Star r)  = ()
      Lang x  (Star r)  = LPlus x r
      Lang x  (r :|: s) = Either (Lang x r) (Lang x s)
      Lang x  (r :&: s) = (Lang x r, Lang x s)
      Lang x  (r :.: s) = (p, q : List tok) -> (p ++ q = x, Lang p r, Lang q s)

||| A proof that the given regular expressions are equivalent.
Equiv : (DecEq tok) => Regex tok -> Regex tok -> Type
Equiv {tok} r s = (str : List tok) -> (Matches str r, Matches str s)

||| If the given regular expression contains the empty string, the result is Ɛ.
||| Otherwise, the result is Ø.
nullable : Regex tok -> Regex tok
nullable = \x => if go x then Ɛ else Ø
  where
    go : Regex t -> Bool
    go Ø         = False
    go Ɛ         = True
    go (Tok t)   = False
    go (Comp r)  = not (go r)
    go (Star r)  = True
    go (r :|: s) = go r || go s
    go (r :&: s) = go r && go s
    go (r :.: s) = go r && go s

||| A type-level witness to the claim that a given regular expression
||| is nullable
Nullable : (DecEq tok) => Regex tok -> Type
Nullable r = Matches [] r

absurdIso : {ty : Type}
            -> (DecEq ty)
            => (a : ty) -> (b : ty)
            -> (dec : Dec (a = b))
            -> (decAsBool dec = False)
            -> Iso Void (a = b)
absurdIso a b (Yes _)     Refl impossible
absurdIso a b (No contra) Refl = MkIso absurd contra
                                 (\x => absurd (contra x))
                                 (\x => absurd x)

||| FIXME: doc
nullableWorks : (DecEq tok, DecEq (Regex tok)) => (r : Regex tok)
                -> Iso (Nullable r) (nullable r = Ɛ)
nullableWorks Ø = absurdIso Ø Ɛ (decEq Ø Ɛ) ?fixme
--   where
--     fixme : (DecEq t) => (a : t) -> (b : t) -> {prf : (decEq a b = No contra)}
--             -> (a = b) -> Void
--     fixme = ?help
nullableWorks owise = ?fixme_nullableWorks_owise
-- nullableWorks Ø         = ?fixme71_1
-- nullableWorks Ɛ         = ?fixme71_2
-- nullableWorks (Tok x)   = ?fixme71_3
-- nullableWorks (Comp x)  = ?fixme71_4
-- nullableWorks (Star x)  = ?fixme71_5
-- nullableWorks (x :|: y) = ?fixme71_6
-- nullableWorks (x :&: y) = ?fixme71_7
-- nullableWorks (x :.: y) = ?fixme71_8

||| The Brzozowski derivative of a regular expression
deriv : (Eq tok) => tok -> Regex tok -> Regex tok
deriv a Ø         = Ø
deriv a Ɛ         = Ø
deriv a (Tok t)   = if t == a then Ɛ else Ø
deriv a (Comp r)  = Comp (deriv a r)
deriv a (Star r)  = deriv a r :.: Star r
deriv a (r :|: s) = deriv a r :|: deriv a s
deriv a (r :&: s) = deriv a r :&: deriv a s
deriv a (r :.: s) = let r' = deriv a r
                        s' = deriv a s
                    in (r' :.: s) :|: (nullable r :.: s')

||| The Brzozowski derivative with respect to strings
derivative : (Eq tok) => List tok -> Regex tok -> Regex tok
derivative []        r = r
derivative (a :: as) r = deriv a (derivative as r)

||| FIXME: doc
derivativeWorks : (DecEq tok, Eq tok)
                  => (str : List tok) -> (r : Regex tok)
                  -> Iso (Matches str r) (Matches [] (derivative str r))
derivativeWorks = ?fixme_derivativeWorks
-- derivativeWorks str Ø         = ?fixme72_1
-- derivativeWorks str Ɛ         = ?fixme72_2
-- derivativeWorks str (Tok x)   = ?fixme72_3
-- derivativeWorks str (Comp x)  = ?fixme72_4
-- derivativeWorks str (Star x)  = ?fixme72_5
-- derivativeWorks str (x :|: y) = ?fixme72_6
-- derivativeWorks str (x :&: y) = ?fixme72_7
-- derivativeWorks str (x :.: y) = ?fixme72_8

main : IO ()
main = print (decAsBool (regexDecEq Bool (Ø {tok=Bool}) (Ɛ {tok=Bool})))

max_stars_repo_name: taktoa/idris-regexp

max_issues_repo_name: taktoa/idris-regexp

max_forks_repo_name: taktoa/idris-regexp


text:
module LTE_Properties

-- properties of LTE

%access public export
%default total

LTE_Property1 : (a : Nat) -> (LTE a a)
LTE_Property1 Z = LTEZero
LTE_Property1 (S k) = LTESucc (LTE_Property1 k)

LTE_Property2 : (a, x, y : Nat) -> (LTE a x) -> (LTE x y) -> (LTE a y)
LTE_Property2 Z x y pf1 pf2 = LTEZero
LTE_Property2 (S k) (S l) (S m) (LTESucc pf1) (LTESucc pf2) =
    LTESucc (LTE_Property2 k l m pf1 pf2)

ext: idr


text:
module Control.Comonad.Store.Representable

import Control.Comonad
import public Control.Comonad.Store.Interface
import Data.Functor.Representable

%default total

public export
data Store : (f : Type -> Type) -> {rep : Representable f r} -> Type -> Type where
  MkStore : {0 rep : Representable f r} -> f a -> r -> Store {rep} f a

public export
(rep : Representable f r) => Functor (Store f {rep}) where
  map f (MkStore s i) = MkStore (map f s) i

public export
(rep : Representable f r) => Comonad (Store f {rep}) where
  extract (MkStore s i) = s `index` i
  duplicate (MkStore s i) = MkStore (tabulate (MkStore s)) i

public export
(rep : Representable f r) => ComonadStore r (Store {rep} f) where
  pos (MkStore _ i) = i
  peek i (MkStore s _) = s `index` i

public export
store : (rep : Representable f r) => (r -> a) -> r -> Store {rep} f a
store g i = MkStore (tabulate g) i

max_stars_repo_name: pnotequalnp/game-of-life

max_issues_repo_name: pnotequalnp/game-of-life

max_forks_repo_name: pnotequalnp/game-of-life


text:
data Prefix = User String | Server String

record Message where
  constructor Msg
  msg_prefix : Maybe Prefix
  msg_command : Either String Int
  msg_params : List String

-- utils

join : String -> List String -> String
join sep ls = pack $ intercalate (unpack sep) (map unpack ls)

instance Show Message where
  show (Msg pref cmd par) = pref' ++ cmd' ++ " " ++ join " " (map p par)
  where
    pref' = case pref of
      Nothing => ""
      Just (User s) => ":" ++ s ++ " "
      Just (Server s) => ":" ++ s ++ " "
    cmd' = case cmd of
      Left s => s
      Right n => show n
    p s = if length (words s) > 1 then ":" ++ s else s

-- simplified message constructors

msg : String -> List String -> Message
msg s l = Msg Nothing (Left s) l

msgl : String -> List String -> List Message
msgl s l = pure $ msg s l

cmsg : String -> String -> Message
cmsg c m = msg "PRIVMSG" [c, m]

cmsgl : String -> String -> List Message
cmsgl c m = pure $ cmsg c m

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

max_stars_repo_name: defanor/hydra-bot

max_issues_repo_name: defanor/hydra-bot

max_forks_repo_name: defanor/hydra-bot


text:
module TypeIndexedTypeChecker

-- Based on https://cs.brynmawr.edu/~rae/papers/2018/stitch/stitch.pdf

import Data.Fin
import Data.List
import Data.Vect
import Control.Catchable

data Ty : Type where
  TyInt : Ty
  TyFun : Ty -> Ty -> Ty

-- lemmas
notIntFun : TyInt = TyFun x y -> Void
notIntFun Refl impossible
notFunInt : (TyFun x y) = TyInt -> Void
notFunInt Refl impossible
xEqyNeq : (x = x') -> ((y = y') -> Void) -> TyFun x y = TyFun x' y' -> Void
xEqyNeq Refl contra Refl = contra Refl
xNeqyEq : (y = y') -> ((x = x') -> Void) -> TyFun x y = TyFun x' y' -> Void
xNeqyEq Refl contra Refl = contra Refl
xNeqyNEq : ((x = x') -> Void) -> ((y = y') -> Void) -> TyFun x y = TyFun x' y' -> Void
xNeqyNEq contra contra' Refl = contra Refl

implementation DecEq Ty where
  decEq TyInt TyInt = Yes Refl
  decEq TyInt (TyFun x y) = No notIntFun
  decEq (TyFun x y) TyInt = No notFunInt
  decEq (TyFun x y) (TyFun x' y') with (decEq x x')
    decEq (TyFun x'' y) (TyFun x'' y') | (Yes Refl) with (decEq y y')
      decEq (TyFun x'' y'') (TyFun x'' y'') | (Yes Refl) | (Yes Refl) = Yes Refl
      decEq (TyFun x'' y) (TyFun x'' y') | (Yes Refl) | (No contra) = No (\eq => xEqyNeq Refl contra eq)
    decEq (TyFun x y) (TyFun x' y') | (No contra) with (decEq y y')
      decEq (TyFun x y'') (TyFun x' y'') | (No contra) | (Yes Refl) = No (\eq => xNeqyEq Refl contra eq)
      decEq (TyFun x y) (TyFun x' y') | (No contra) | (No contra') = No (\eq => xNeqyNEq contra contra' eq)

data UExp : Nat -> Type where
  UVar : Fin n -> UExp n
  ULam : Ty -> UExp (S n) -> UExp n
  UApp : UExp n -> UExp n -> UExp n
  UPlus : UExp n -> UExp n -> UExp n
  UIntE : Int -> UExp n

data Expr : Vect n Ty -> Ty -> Type where
  Val : Int -> Expr ctx TyInt
  Plus : Expr ctx TyInt -> Expr ctx TyInt -> Expr ctx TyInt
  Var : Elem t ctx -> Expr ctx t
  Lam : Expr (a :: ctx) b -> Expr ctx (TyFun a b)
  App : Expr ctx (TyFun a b) -> Expr ctx a -> Expr ctx b

interpTy : Ty -> Type
interpTy TyInt = Int
interpTy (TyFun arg res) = interpTy arg -> interpTy res

interpCtx : Vect n Ty -> Type
interpCtx [] = ()
interpCtx (t :: ts) = (interpTy t, interpCtx ts)

lookup : Elem t ctx -> interpCtx ctx -> interpTy t
lookup Here (t, _) = t
lookup (There x) (_, ts) = lookup x ts

show : (t : Ty) -> interpTy t -> String
show TyInt v = show v
show (TyFun x y) v = "Fun"

eval : interpCtx ctx -> Expr ctx t -> interpTy t
eval ctx (Val x) = x
eval ctx (Var x) = lookup x ctx
eval ctx (Lam body) = \x => eval (x, ctx) body
eval ctx (App f x) = (eval ctx f) (eval ctx x)
eval ctx (Plus e1 e2) = (eval ctx e1) + (eval ctx e2)

check : (Catchable m String) => UExp Z -> ((t : Ty) -> Expr [] t -> m r) -> m r
check uexp k = go [] uexp k
  where
    go : (Catchable m String) => (ctx : Vect n Ty) -> UExp n -> ((t : Ty) -> Expr ctx t -> m r) -> m r
    go ctx (UVar n) k = checkVar n ctx $ \ty, elem => k ty (Var elem)
      where
        checkVar : (Catchable m String) => {n : Nat} -> Fin n -> (ctx : Vect n Ty) -> ((t : Ty) -> Elem t ctx -> m r) -> m r
        checkVar FZ (ty :: _) k = k ty Here
        checkVar (FS n') (_ :: ctx') k = checkVar n' ctx' $ \ty, elem => k ty (There elem)

    go ctx (ULam ty body) k = go (ty :: ctx) body $ \resTy, body' => k (TyFun ty resTy) (Lam body')
    go ctx (UApp e1 e2) k = go ctx e1 $ \funTy, e1' =>
                            go ctx e2 $ \argTy, e2' => checkApp funTy argTy e1' e2' k
      where
        checkApp : (Catchable m String) => (funTy : Ty) -> (argTy : Ty) -> Expr ctx funTy -> Expr ctx argTy -> ((t : Ty) -> Expr ctx t -> m r) -> m r
        checkApp (TyFun argTy' resTy) argTy e1' e2' k with (decEq argTy' argTy)
          checkApp (TyFun argTy resTy) argTy e1' e2' k | (Yes Refl) = k resTy (App e1' e2')
          checkApp (TyFun argTy' refTy) argTy e1' e2' k | (No contra) = throw "TypeError"
        checkApp _ _ e1' e2' k = throw "TypeError"
    go ctx (UPlus e1 e2) k = go ctx e1 $ \ty1, e1' =>
                             go ctx e2 $ \ty2, e2' => checkPlus ty1 ty2 e1' e2' k
      where
        checkPlus : (Catchable m String) => (ty1 : Ty) -> (ty2 : Ty) -> Expr ctx ty1 -> Expr ctx ty2 -> ((t : Ty) -> Expr ctx t -> m r) -> m r
        checkPlus TyInt TyInt e1' e2' k = k TyInt (Plus e1' e2')
        checkPlus _ _ e1' e2' k = throw "TypeError"
    go ctx (UIntE x) k = k TyInt (Val x)

example : UExp Z
example = UApp (ULam TyInt (UPlus (UVar FZ) (UIntE 1))) (UIntE 5)

test : Either String String
test = check example (\ty, expr => Right $ show ty $ eval () expr)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
import Erlang.Data.IORef

main : IO ()
main
    = do x <- newIORef 42
         let y = x
         writeIORef y 94
         val <- readIORef x
         printLn val
         val <- readIORef y
         printLn val
         modifyIORef x (* 2)
         val <- readIORef x
         printLn val
         val <- readIORef y
         printLn val


text:
import public Invincy.Core
import public Invincy.Parsing
import public Invincy.Printing
import public Invincy.Invertible
import public Invincy.Gen

max_stars_repo_name: defanor/invincy

max_issues_repo_name: defanor/invincy

max_forks_repo_name: defanor/invincy


text:
-- | Exercises on Ranges
module Koans.Ranges

rangeNums : Bool
rangeNums = [1,2,3,4,5,6,7,8,9,10,11,12,13] == [1..13]

stepUp : Bool
stepUp = [3,6,9,12,15,18] == [3,6..20]

stepDown : Bool
stepDown = [20,17,14,11,8,5,2] == [20,17..1]

stopMe : List Integer
stopMe = Stream.take 3 [1..]

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

max_stars_repo_name: simonewebdesign/idris-koans

max_issues_repo_name: simonewebdesign/idris-koans

max_forks_repo_name: simonewebdesign/idris-koans


text:
module Crypto.Hash

import Data.Bits
import Data.List
import Data.Nat
import Data.Vect
import public Crypto.Hash.Interfaces
import public Crypto.Hash.SHA2
import public Crypto.Hash.SHA1
import public Crypto.Hash.MD5

||| basically `Hash.initialize` but with explicit type argument
public export
init : (0 algo : Type) -> Hash algo => algo
init algo = initialize

||| hash a sequence of bytes and produce a digest
public export
hash : (0 algo : Type) -> Hash algo => (message : List Bits8) -> Vect (digest_nbyte {algo}) Bits8
hash algo xs = finalize $ update xs $ Hash.init algo

||| basically `MAC.initialize` but with explicit type argument
public export
init_mac : (0 algo : Type) -> MAC key algo => key -> algo
init_mac algo key = initialize_mac key

||| hash a sequence of bytes with key and produce a digest
public export
mac : (0 algo : Type) -> MAC key algo => key -> (message : List Bits8) -> Vect (digest_nbyte {algo}) Bits8
mac algo key xs = finalize $ update xs $ Hash.init_mac algo key


text:
module Main

import Data.Buffer
import Data.List.Quantifiers
import Control.Monad.Trans
import Control.Monad.Either
import Control.Monad.Maybe
import Node.HTTP.Server
import TyTTP.Adapter.Node.HTTP
import TyTTP.Adapter.Node.URI
import TyTTP.HTTP
import TyTTP.HTTP.Consumer
import TyTTP.HTTP.Producer
import TyTTP.HTTP.Routing
import TyTTP.URL
import TyTTP.URL.Path
import TyTTP.URL.Search

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

hQuery : Error e
  => Monad m
  => (src -> String)
  -> Step me (URL auth pth src) h1 s StringHeaders a ()
  -> m $ Step me (URL auth pth src) h1 Status StringHeaders a (Publisher IO e Buffer)
hQuery toString step = do
  let query = toString step.request.url.search
  text query step >>= status OK

hRouting : Error e
  => Step Method String StringHeaders Status StringHeaders (Publisher IO e Buffer) ()
  -> Promise e IO $ Step Method String StringHeaders Status StringHeaders (Publisher IO e Buffer) (Publisher IO e Buffer)
hRouting =
  let routingError = sendError NOT_FOUND "Resource could not be found"
      urlError = \err => sendError BAD_REQUEST "URL has invalid format"
      uriError = sendError BAD_REQUEST "URI decode has failed"
  in
    uri' uriError :> url' urlError :> routes' routingError
        [ get $ pattern "/query" :>> hQuery id
        , get $ pattern "/parsed" :> Simple.search :> hQuery show
        ]

main : IO ()
main = eitherT putStrLn pure $ do
  http <- HTTP.require
  ignore $ HTTP.listen' $ hRouting

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Flexidisc.Record.Read

import        Flexidisc.RecordContent
import public Flexidisc.Record.Type

%default total
%access export

||| Get value from a `Row`
||| (not the most convenient way to get a value
||| but it may be useful when you have a `Row`)
|||
||| Complexity is _O(n)_
atRow : RecordM m k header -> (loc : Row l ty header) -> m ty
atRow (Rec xs _) (R loc) = atRow xs loc

||| Get value from a `Label`
||| (not the most convenient way to get a value
||| but it may be useful when you have a `Label`)
|||
||| It's slightly less efficient than `atRow`,
||| as you need to go through the header to get the return type
|||
||| Complexity is _O(n)_
atLabel : RecordM m k header -> (loc : Label l header) -> m (atLabel header loc)
atLabel (Rec xs _) (L loc) = atLabel xs loc

||| Typesafe extraction of a value from a record
|||
||| Complexity is _O(n)_
get : (query : k) -> RecordM m k header ->
      {auto loc : Row query ty header} -> m ty
get query xs {loc} = atRow xs loc

||| Typesafe extraction of a value from a record,
||| `Nothing` if the Row doesn't exist.
|||
||| Complexity is _O(n)_
export
lookup : (Ord k, DecEq k) =>
         (query : k) -> (xs : RecordM m k header) ->
         {auto p : HereOrNot [(query, ty)] header} -> Maybe (m ty)
lookup _ xs {p = (HN p)} = (atRow xs . R) <$> (toRow p)

infixl 7 !!

||| (Almost) infix alias for `get`
|||
||| Almost: it requires an implicit paramet which may leads to weird behaviour
||| when used as an infix operator
(!!) : RecordM m k header -> (query : k) ->
      {auto loc : Row query ty header} -> m ty
(!!) rec field = get field rec

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Highlight.Formats

import Highlight.Regions
import Control.Monad.State

import Debug.Trace

||| A description of how to annotate a source file to output to a particular format.
public export
record Format where
  constructor MkFormat
  openTag   : HighlightType -> String
  closeTag  : HighlightType -> String
  escape    : Char -> String
  preamble  : String
  postamble : String

private total
openTagL : HighlightType -> String
openTagL (Name Function _ _)        = "\\IdrisFunction{"
openTagL (Name Constructor _ _)     = "\\IdrisData{"
openTagL (Name TypeConstructor _ _) = "\\IdrisType{"
openTagL (Bound _)                  = "\\IdrisBound{"
openTagL Keyword                    = "\\IdrisKeyword{"

private total
closeTagL : HighlightType -> String
closeTagL _ = "}"

private total
escapeL : Char -> String
escapeL '{'  = "\\{"
escapeL '}'  = "\\}"
escapeL '\\' = "\\textbackslash{}"
escapeL '~'  = "\\textasciitilde{}"
escapeL c    = singleton c

private total
preambleL : String
preambleL =
  """\documentclass{article}
\usepackage{fancyvrb}
\usepackage[usenames]{xcolor}
\newcommand{\IdrisData}[1]{\textcolor{red}{#1}}
\newcommand{\IdrisType}[1]{\textcolor{blue}{#1}}
\newcommand{\IdrisBound}[1]{\textcolor{magenta}{#1}}
\newcommand{\IdrisFunction}[1]{\textcolor{green}{#1}}
\newcommand{\IdrisKeyword}[1]{{\underline{#1}}}
\newcommand{\IdrisImplicit}[1]{{\itshape \IdrisBound{#1}}}

\begin{document}
% START CODE
\begin{Verbatim}[commandchars=\\\{\}]
"""

private total
postambleL : String
postambleL =
  """\end{Verbatim}
% END CODE
\end{document}
"""

||| LaTeX-style highlights
export total
LaTeX : Format
LaTeX = MkFormat openTagL closeTagL escapeL preambleL postambleL

private total
preambleH : String
preambleH =
  """<!doctype html>
"""

private total
postambleH : String
postambleH = "
"

private total
openTagH : HighlightType -> String
openTagH (Name Function d t)        = ""
openTagH (Name Constructor d t)     = ""
openTagH (Name TypeConstructor d t) = ""
openTagH (Bound i)                  = ""
openTagH Keyword                    = ""

private total
closeTagH : HighlightType -> String
closeTagH hl = ""

private total
escapeH : Char -> String
escapeH '&' = "&"
escapeH '<' = "<"
escapeH '>' = ">"
escapeH c = singleton c

||| HTML-style highlights
export total
HTML : Format
HTML = MkFormat openTagH closeTagH escapeH preambleH postambleH

------------------------------------
-- Applying formats to file contents
------------------------------------
private
record HLState where
  constructor MkHlState
  lineNo : Integer
  colNo : Integer
  highlights : List (Region HighlightType)
  openHighlights : List (Region HighlightType)
  output : List String

private
incCol : HLState -> HLState
incCol st = record {colNo = 1 + colNo st} st

private
incLine : HLState -> HLState
incLine st = record {lineNo = 1 + lineNo st} st

private
doOutput : String -> State HLState ()
doOutput str = do st <- get
                  put (record {output = str :: output st} st)

private
openAll : (line, col : Integer) -> Format -> State HLState ()
openAll line col fmt =
    do hls <- highlights <$> get
       let (toOpen, notYet) = List.span (\hl => startLine hl < line ||
                                                (startLine hl == line &&
                                                 startColumn hl <= col))
                                         hls
       traverse_ (doOutput . openTag fmt . metadata) toOpen
       st <- get
       put (record { highlights = notYet
                   , openHighlights = reverse toOpen ++ openHighlights st
                   } st)

||| Close all currently-open highlights
closeAll : (line, col : Integer) -> Format -> State HLState ()
closeAll line col fmt =
    do openHls <- openHighlights <$> get
       let (toClose, notYet) = span (\hl => endLine hl < line ||
                                          (endLine hl == line &&
                                           endColumn hl <= col))
                                    openHls
       traverse_ (doOutput . closeTag fmt . metadata) toClose
       st <- get
       put (record {openHighlights = notYet} st)

||| Apply highlighting to a source file for some output format
export
highlight : Format -> (fileContents : String) -> List (Region HighlightType) -> String
highlight fmt fileContents hls =
    preamble fmt ++
    concat (evalState (highlight' (split isNL fileContents) []) (MkHlState 0 0 (sort hls) [] [])) ++
    postamble fmt
  where highlight' : List String -> List Char -> State HLState (List String)
        highlight' [] [] =
            do traverse_ (doOutput . closeTag fmt . metadata) (openHighlights !get)
               pure (reverse (output !get))
        highlight' lines (c::cs) =
            do modify incCol
               line <- lineNo <$> get
               col <- colNo <$> get
               openAll line col fmt
               closeAll line col fmt
               doOutput $ escape fmt c
               highlight' lines cs
        highlight' (l::lines) [] =
            do modify incCol
               closeAll (lineNo !get) (colNo !get) fmt
               modify incLine
               modify (record {colNo = 0})
               doOutput "\n"
               highlight' lines (unpack l)


text:
module Compiler.Erlang.Codegen.AbstractFormat.Helpers

import Compiler.Erlang.IR.AbstractFormat

export
showBitType : TypeSpecifierList -> String
showBitType tsl =
  case tsl of
    ABInteger => "integer"
    ABFloat => "float"
    ABBinary => "binary"
    ABBitstring => "bitstring"
    ABUtf8 => "utf8"
    ABUtf16 => "utf16"
    ABUtf32 => "utf32"

export
showBitSignedness : BitSignedness -> String
showBitSignedness signedness =
  case signedness of
    ABUnsigned => "unsigned"
    ABSigned => "signed"

export
showBitEndianness : BitEndianness -> String
showBitEndianness endianness =
  case endianness of
    ABBig => "big"
    ABLittle => "little"
    ABNative => "native"

export
isAllowedToSpecifyBitUnit : BitSize -> Bool
isAllowedToSpecifyBitUnit ABSDefault = False
isAllowedToSpecifyBitUnit (ABSInteger _ _) = True
isAllowedToSpecifyBitUnit (ABSVar _ _) = True


text:
module RunElabNoEscape

import Language.Reflection

%language ElabReflection

escScr : Elab $ (0 _ : a) -> a
escScr = check $ ILam EmptyFC M0 ExplicitArg (Just `{x}) `(a) `(x)

esc : (0 _ : a) -> a
esc = %runElab escScr

escDecl : Name -> Elab Unit
escDecl name = declare [
                 IDef EmptyFC name [
                   PatClause EmptyFC
                     -- lhs
                     (IApp EmptyFC (IVar EmptyFC name) (IBindVar EmptyFC "x"))
                     -- rhs
                     `(x)
                 ]
               ]

0 esc' : (0 _ : a) -> a

%runElab escDecl `{esc'}

%runElab escDecl `{esc}

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Effekt.AvoidEta

import Effekt.CpsUnstaged
import Effekt.CpsStaged
import Effekt.IteratedUnstaged

mutual
  public export
  data CTX : List Type -> Type -> Type -> Type where
    Static :   (Exp a -> STM rs b)   -> CTX rs a b
    Dynamic :  Exp (a -> Stm rs b)   -> CTX rs a b

  public export
  STM : List Type -> Type -> Type
  STM [] a = Exp a
  STM (r :: rs) a = CTX rs a r -> STM rs r

mutual
  export
  reify : STM rs a -> Exp (Stm rs a)
  reify {rs = []} m = m
  reify {rs = (q :: qs)} m =
    (Lam $ \ k =>  reify (m (Dynamic k)))

  export
  reflect : Exp (Stm rs a) -> STM rs a
  reflect {rs = []} m = m
  reflect {rs = (q :: qs)} m =
    \k => reflect (App (m)  ((reifyContext k)))

  export
  reifyContext : CTX rs a r -> Exp (a -> Stm rs r)
  reifyContext (Static k) = (Lam $ \ a =>  reify (k a))
  reifyContext (Dynamic k) = k

export
resume : CTX rs a r -> (Exp a -> STM rs r)
resume (Static k) = k
resume (Dynamic k) = \a => reflect (App (k)  (a))

export
pure : Exp a -> STM rs a
pure{  rs= []}         a = a
pure{  rs= r :: rs}  a = \k => resume k a

push : CTX (r :: rs) a b -> CTX rs b r -> CTX rs a r
push f k = Static (\a => resume f a k)

bind : STM rs a -> CTX rs a b -> STM rs b
bind{  rs= []}         m f = resume f m
bind{  rs= r :: rs}  m f = \k => m (push f k)

export
shift0 : (CTX rs a r -> STM rs r) -> STM (r :: rs) a
shift0 = id

export
runIn0 : STM (r :: rs) a -> CTX rs a r -> STM rs r
runIn0 = id

export
reset0 : STM (a :: rs) a -> STM rs a
reset0 m = runIn0 m (Static pure)

export
lift : STM rs a -> STM (r :: rs) a
lift = bind

export
(>>=) : STM rs a -> (Exp a -> STM rs b) -> STM rs b
m >>= f = bind m (Static f)

add : STM rs Int -> STM rs Int -> STM rs Int
add mx my = do
  x <- mx
  y <- my
  pure ((Add x y))

display : Exp String -> STM (IO () :: rs) ()
display {rs} s = shift0 (\c => do
  a <- resume c Uni
  pure {rs} ((Seq ((Dis s)) a)))

export
displayTwice : STM [] (IO ())
displayTwice = reset0 {rs=[]} (
  (>>=) {rs=[IO ()]} (display {rs=[]} (Str "hello ")) (\u =>
  (>>=) {rs=[IO ()]} (display {rs=[]} (Str "world")) (\o =>
  pure {rs=[IO ()]} Ski)))

export
ifthenelse : Exp Bool -> STM rs a -> STM rs a -> STM rs a
ifthenelse {rs} Tru t _ = t
ifthenelse {rs} Fls _ e = e
ifthenelse {rs=[]} b t e = Ite b t e
ifthenelse {rs=q::qs} b t e = \k => ifthenelse b (t k) (e k)

export
letrec : ((Exp a -> STM rs b) -> Exp a -> STM rs b) -> Exp a -> STM rs b
letrec body a = reflect (App (Rec (\f => \x =>
  reify (body (\y => reflect (App (f)  (y))) x)))  (a))

-- Iteration happens to be recursion.
export
loop : (Exp a -> STM (r :: rs) a) -> Exp a -> STM rs r
loop m = letrec (\k => \a => m a (Static k))

export
break : Exp r -> STM (r :: rs) a
break r = shift0 (\_ => pure r)

max_stars_repo_name: b-studios/idris-effekt

max_issues_repo_name: b-studios/idris-effekt

max_forks_repo_name: b-studios/idris-effekt


text:
module Main

-- from http://docs.idris-lang.org/en/latest/tutorial/theorems.html?highlight=fiveIsFive#equality

-- = is defined in sourse code of idris
-- https://groups.google.com/forum/#!topic/idris-lang/-tmOaux6DFI

-- proudo-definition
-- data (=) : a -> b -> Type where
--   refl : x = x

fiveIsFive : 5 = 5
fiveIsFive = Refl

twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl

-- twoPlusTwo : 2 + 2 = 5 -- raise error
-- twoPlusTwo = Refl

--- (=) defined ourselves

using (a : Type, b : Type, x : a)
  data Equus : a -> b -> Type where
    --  will raise error `Main.eqRefl has a name which may be implicitly bound.`
    --  implicitly bound variable - implicit forall

    -- eqRefl : Equus x x

    EqRefl : Equus x x -- right definition

twoPlusTwo' : 2 + 2 `Equus` 4
twoPlusTwo' = EqRefl

heterogeneous : 2 + 2 ~=~ 4
heterogeneous = Refl

-- heterogeneous : 2 + 2 ~=~ 5 -- raise error
-- heterogeneous = Refl

max_stars_repo_name: srghma/hask-test

max_issues_repo_name: BjornMelgaard/hask-test

max_forks_repo_name: BjornMelgaard/hask-test


text:
-- --------------------------------------------------------------- [ BTree.idr ]
-- Module    : BTree.idr
-- Copyright : (c) 2017 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Implementation of a Binary Tree as a Red-Black Binary Search Tree.
|||
||| The underlying Red-Black Tree is a Key-Value Tree, this library
||| just wraps this up as a simple Binary tree for values i.e. keys.
module Data.RedBlack.BTree

import Data.RedBlack.Tree

%default total
%access export

-- ------------------------------------------------------------- [ Definitions ]

||| A Binary Search Tree.
|||
||| @ty The type of the elements in the tree.
data BTree : (ty : Type) -> Type
    where
      MkTree : {a : Type} -> RBTree n B a Unit -> BTree a

-- --------------------------------------------------------------------- [ API ]

||| Return an empty BTree.
empty : Ord a => BTree a
empty = MkTree empty

||| Insert an element into the Tree.
insert : (Ord a) => a -> BTree a -> BTree a
insert a (MkTree t) = case Tree.insert a () t of
  (_ ** t') => MkTree t'

||| Does the tree contain the given element?
contains : (Ord a) => a -> BTree a -> Bool
contains a (MkTree t) = isJust (Tree.lookup a t)

||| How many nodes are in the tree?
size : BTree a -> Nat
size (MkTree t) = Tree.size t

||| Construct an ordered list containing the elements of the tree.
toList : BTree a -> List a
toList (MkTree t) = map fst $ Tree.toList t

||| Construct a tree from a list of elements.
fromList : (Ord a) => List a -> BTree a
fromList xs = (foldl (\t,k => BTree.insert k t) empty xs)

-- --------------------------------------------------------------- [ Instances ]

Foldable BTree where
  foldr f i (MkTree t) = foldr (\x,_,p => f x p) i t

-- Eq a => Eq (BTree a) where
--   (==) (MkTree t) (MkTree t') = t == t'

Show a => Show (BTree a) where
  show s = "{ " ++ (unwords . intersperse "," . map show . BTree.toList $ s) ++ " }"

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


text:
module Hezarfen

import Hezarfen.Prover
import Hezarfen.Simplify
import Hezarfen.FunDefn
import Hezarfen.Hint
import Language.Reflection.Utils

%access public export

forget' : TT -> Elab Raw
forget' t = case forget t of
                 Nothing => fail [TextPart "Couldn't forget type"]
                 Just x => pure x

getCtx : Elab Context
getCtx = Ctx <$> xs <*> pure []
  where
    xs : Elab (List (TTName, Ty))
    xs = do env <- getEnv
            pure $ mapMaybe id $ map (\(n, b) =>
              MkPair n <$> forget (binderTy b)) env

getTy : TTName -> Elab (TTName, Ty)
getTy n = case !(lookupTyExact n) of
  (n, _, ty) => pure (n, !(forget' ty))

add : List TTName -> Elab Context
add xs = (flip Ctx) [] <$> traverse getTy xs

hezarfenExpr' : Context -> Elab ()
hezarfenExpr' c =
  do goal <- forget' (snd !getGoal)
     fill !(reduceLoop !(breakdown False $ Seq (c <+> !getCtx) goal))
     solve

hezarfenExpr : Elab ()
hezarfenExpr = hezarfenExpr' neutral

-- Generate declarations
hezarfenDecl : TTName -> Context -> Elab (FunDefn Raw)
hezarfenDecl n c = case !(lookupTy n) of
  [] => fail [TextPart "No type found for", NamePart n]
  [(_, _, tt)] =>
    do tt' <- normalise !getEnv tt
       -- normalization is necessary to change `Not p` into `p -> Void`, etc
       ty <- forget' tt'
       tm <- breakdown False (Seq (c <+> !getCtx) ty)
       proofTerm <- reduceLoop tm
       definitionize n proofTerm
  _ => fail [TextPart "Ambiguity: multiple types found for", NamePart n]

hezarfen' : TTName -> Context -> Elab ()
hezarfen' n c = defineFunction !(hezarfenDecl n c)

||| Generates a function definition for a previously undefined name.
||| Note that there should already be a type signature for that name.
||| Example usage:
||| ```
||| f : a -> a
||| derive f
||| ```
hezarfen : TTName -> Elab ()
hezarfen n = hezarfen' n neutral

||| Returns reflected proof term directly
hezarfenTT : (shouldReduce : Bool) -> TTName -> Elab TT
hezarfenTT b n =
  do (_, _, ty) <- lookupTyExact n
     pf <- breakdown False (Seq !getCtx !(forget' ty))
     pf' <- (if b then reduceLoop else pure) pf
     env <- getEnv
     fst <$> check env pf'

decl syntax "derive" {n} = %runElab (hezarfen `{n})
decl syntax "derive'" {n} = %runElab (hezarfen' `{n} !(add !getHints))

decl syntax "obtain" {n} "from" [xs] = %runElab (hezarfen' `{n} !(add xs))
decl syntax "obtain'" {n} "from" [xs] =
  %runElab (hezarfen' `{n} !(add (Prelude.List.(++) xs !getHints)))

max_stars_repo_name: joom/hezarfen

max_issues_repo_name: joom/hezarfen

max_forks_repo_name: joom/hezarfen


text:
||| N-ary congruence for reasoning
module Data.Telescope.Congruence

import Data.Telescope.Telescope
import Data.Telescope.Segment
import Data.Telescope.SimpleFun
import Data.Telescope.Fun

public export
congType : (delta : Segment n gamma)
  -> (env1 : Left.Environment gamma) -> (sy1 : SimpleFun env1 delta Type) -> (lhs : Fun env1 delta sy1)
  -> (env2 : Left.Environment gamma) -> (sy2 : SimpleFun env2 delta Type) -> (rhs : Fun env2 delta sy2)
  -> Type
congType []            env1 sy1 lhs  env2 sy2 rhs = lhs ~=~ rhs
congType (ty :: delta) env1 sy1 lhs  env2 sy2 rhs =
                         {x1 : ty env1} -> {x2 : ty env2}
                      -> x1 ~=~ x2
                      -> congType delta
                           (env1 ** x1) (sy1 x1) (lhs x1)
                           (env2 ** x2) (sy2 x2) (rhs x2)

public export
congSegment : {n : Nat} -> (0 delta : Segment n gamma)
  ->(0 env1 : Left.Environment gamma)-> (0 sy1 : SimpleFun env1 delta Type) -> (0 lhs : Fun env1 delta sy1)
  ->(0 env2 : Left.Environment gamma)-> (0 sy2 : SimpleFun env2 delta Type) -> (0 rhs : Fun env2 delta sy2)
  ->(0 _ : env1 ~=~ env2)      -> (0 _ : sy1 ~=~ sy2)                 -> (0 _ : lhs ~=~ rhs)
  -> congType delta env1 sy1 lhs
                    env2 sy2 rhs
congSegment {n = 0  } []            env sy context env sy context Refl Refl Refl = Refl
congSegment {n = S n} (ty :: delta) env sy context env sy context Refl Refl Refl = recursiveCall
  where
    recursiveCall : {x1 : ty env} -> {x2 : ty env} -> x1 ~=~ x2
                 -> congType delta (env ** x1) (sy x1) (context x1)
                                   (env ** x2) (sy x2) (context x2)
    recursiveCall {x1=x} {x2=x} Refl = congSegment delta
                                                   (env ** x) (sy x) (context x)
                                                   (env ** x) (sy x) (context x)
                                                   Refl       Refl   Refl

public export
cong : {n : Nat} -> {0 delta : Segment n []} -> {0 sy : SimpleFun () delta Type}
    -> (context : Fun () delta sy)
    -> congType delta () sy context
                      () sy context
cong {n} {delta} {sy} context = congSegment delta ()    sy   context
                                                  ()    sy   context
                                                  Refl  Refl Refl


text:
module Circuits.Common.Pretty

import System.File

import Data.String

import Toolkit.Data.List.Occurs.Does
import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Graph.EdgeBounded.HasExactDegree

import Text.Lexer
import Text.Parser

import Toolkit.Data.Whole
import Toolkit.Data.Location
import Toolkit.Text.Lexer.Run
import Toolkit.Text.Parser.Run

import Circuits.Common

export
Show Usage where
  show USED = "Used"
  show FREE = "Free"

export
Show DType where
  show LOGIC = "logic"
  show (BVECT n type) = show type <+> concat ["[", show n, "]"]

export
[circuitspf] Show a => Show (ParseFailure a) where
  show err
    = trim $ unlines [show (location err), (error err)]

export
[circuitspe] Show a => Show (ParseError a) where
  show (FError err)
    = trim $ unlines ["File Error: "
                     , show err]
  show (PError err)
    = trim $ unlines (forget (map (show @{circuitspf}) err))

  show (LError (MkLexFail l i))
    = trim $ unlines [show l, show i]

export
Show (Vertex String) where
  show (Node d k j i) = show k <+> " [label=\"" <+> show (j,i) <+> " " <+> d <+> "\"];"
  show (Leaf d x k j) = show k <+> " [label=\"" <+> withFlow x j <+> " " <+> d <+> "\"];"
    where withFlow : Flow -> Nat -> String
          withFlow f k = show f <+> "(" <+> show k <+>")"

export
showGraph : Graph String -> String
showGraph (MkGraph nodes edges)
    = unlines $ ["digraph G {"]
                ++
                  map show nodes
                ++
                  map (\(x,y) => unwords ["\t" <+> show x, "->", show y <+> ";"]) edges
                ++
                ["}"]

export
Show DegreeType where
  show I = "IN"
  show O = "OUT"

export
showErr : (Graph String, HasExactDegree.Error String)  -> String
showErr (g, MkError vertex kind (MkError vertexID k values))
 = unlines [showGraph g
           , "//because:"
           , "// Vertex " <+> show (ident vertex)
           , "//  has expected degree " <+> show k <+> " " <+> show (values.expected)
           , "//  but we found degree " <+> show k <+> " " <+> show (values.found)
           ]

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module Control.Monad.Ref

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

%default total
%access public export

%hide Language.Reflection.Ref
%hide Language.Reflection.Universe

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

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

infix 4 :=
(:=) : MonadRef u l m => l a -> (typeOf @{u} a) -> m ()
(:=) = assign

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

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

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

modify : MonadRef u l m => l a -> (typeOf @{u} a -> typeOf @{u} a) -> m ()
modify l f = do
  x <- deref l
  l := f x

{- Tests -----------------------------------------------------------------------

test0 : IO Int
test0 = do
  r <- newIORef 5
  writeIORef r 10
  x <- readIORef r
  pure x

test : MonadRef IORef IO => IO Int
test = do
  r <- ref (the Int 5)
  r := (the Int 10)
  x <- deref r
  pure x

-------------------------------------------------------------------------------}

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
> module SequentialDecisionProblems.TabBackwardsInduction2

> import Data.Vect
> import Control.Isomorphism
> -- import Debug.Trace

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.Utils

> import Nat.Operations
> import Nat.OperationsProperties
> import Nat.LTEProperties
> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Decidable.Properties
> import Sigma.Sigma
> import Sigma.Operations
> import Pairs.Operations
> import Vect.Operations
> import Vect.Properties
> import Decidable.Predicates
> import Fin.Operations

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

* Tabulation

If the state space is finite

> finiteState : (t : Nat) -> Finite (State t)

, we can compute the number of values of type |State t| and collect them
in a vector

> cardState : (t : Nat) -> Nat
> cardState t = card (finiteState t)

> vectState : (t : Nat) -> Vect (cardState t) (State t)
> vectState t = toVect (finiteState t)

If |Reachable| and |Viable n| are also decidable

> decidableReachable : {t' : Nat} -> (x' : State t') -> Dec (Reachable x')

< decidableViable : {t : Nat} -> (n : Nat) -> (x : State t) -> Dec (Viable n x)

then their conjunction

> ReachableAndViable : {t : Nat} -> (n : Nat) -> (x : State t) -> Type
> ReachableAndViable n x = (Reachable x , Viable n x)

is decidable

> decidableReachableAndViable : {t : Nat} -> (n : Nat) -> (x : State t) -> Dec (ReachableAndViable n x)
> decidableReachableAndViable n x = decPair (decidableReachable x) (decidableViable n x)

and we can collect all states which are reachable and viable in a vector:

> cardReachableAndViableState : (t : Nat) -> (n : Nat) -> Nat
> cardReachableAndViableState t n = outl (f t n) where
>   f : (t : Nat) -> (n : Nat) -> Sigma Nat (\ m => Vect m (Sigma (State t) (ReachableAndViable n)))
>   f t n = filterTagSigma (decidableReachableAndViable n) (vectState t)

> vectReachableAndViableState : (t : Nat) -> (n : Nat) ->
>                               Vect (cardReachableAndViableState t n) (Sigma (State t) (ReachableAndViable n))
> vectReachableAndViableState t n = outr (f t n) where
>   f : (t : Nat) -> (n : Nat) -> Sigma Nat (\ m => Vect m (Sigma (State t) (ReachableAndViable n)))
>   f t n = filterTagSigma (decidableReachableAndViable n) (vectState t)

--

If equality on values of type |State t| is decidable

> decidableEqState : (t : Nat) -> DecEq (State t)

we can store the result of looking up the index of a reachable and
viable state in |vectReachableAndViableState t n| into a table

> iat : {t, n : Nat} ->
>       Not (Z = cardReachableAndViableState t n) ->
>       Vect (cardState t) (Fin (cardReachableAndViableState t n))
> iat {t} {n} prf = toVect iatf where
>   iatf : (Fin (cardState t) -> Fin (cardReachableAndViableState t n))
>   iatf k with (lookup' (decidableEqState t)
>                        (from (iso (finiteState t)) k)
>                        (map outl (vectReachableAndViableState t n)))
>     | Nothing with (cardReachableAndViableState t n) proof contra
>         |   Z = void (prf Refl)
>         | S m = FZ {k = m}
>     | Just k' = k'

The table can then be used to replace lookups (like in |tabSval|, see
below) with |index| operations. The idea is that indexing can in
principle (Blodwin feature?) be done in constant time whereas lookups
(searcing) takes liner time.

--

In this case, we can implement a "tabulated" versions of |backwardsInduction|

< backwardsInduction : (t : Nat) -> (n : Nat) -> PolicySeq t n
< backwardsInduction t  Z     =  Nil
< backwardsInduction t (S n)  =  let ps = backwardsInduction (S t) n in
<                                optExt ps :: ps

The idea is to replace policies as functions from states to control with
policy tables. In analogy to policies as defined in the CoreTheory, the
type of a policy table that supports zero decision steps is just the
singleton type. A policy table that supports |S m| further decision
steps at decision step |t| is a vector with as many entries as there are
states in |State t| that are reachable and viable |S m| steps:

> |||
> PolicyTable : (t : Nat) -> (n : Nat) -> Type
> PolicyTable t  Z    = Unit
> PolicyTable t (S m) = Vect
>                       (cardReachableAndViableState t (S m))
>                       (Sigma (State t) (\x => (ReachableAndViable (S m) x, GoodCtrl t x m)))

Similarly, sequences of policy tables are either empty or made up of a
policy table consed with a tail sequence:

> |||
> data PolicyTableSeq : (t : Nat) -> (n : Nat) -> Type where
>   Nil   :  {t : Nat} ->
>            PolicyTableSeq t Z
>   (::)  :  {t, n : Nat} ->
>            PolicyTable t (S n) -> PolicyTableSeq (S t) n -> PolicyTableSeq t (S n)

With these notions in place, a tabulated version of backwards induction
will be a function of type

< (t : Nat) -> (n : Nat) -> PolicyTableSeq t n

In order to implement this function, some additional notions are needed. ...

> |||
> ValueTable : Nat -> Nat -> Type
> ValueTable t n = Vect (cardReachableAndViableState t n) Val

> |||
> zeroVec : (n : Nat) -> Vect n Val
> zeroVec Z     = Nil
> zeroVec (S n) = zero :: zeroVec n

> |||
> tabSval : {t,n : Nat} ->
>           (x  : State t) -> .(r  : Reachable x) -> .(v  : Viable (S n) x) ->
>           (gy  : GoodCtrl t x n) ->
>           (vt : Vect (cardReachableAndViableState (S t) n) Val) ->
>           PossibleNextState x (ctrl gy) -> Val
> tabSval {t} {n} x r v gy vt (MkSigma x' x'emx') =
>   let y    : Ctrl t x
>            = ctrl gy in
>   let mx'  : M (State (S t))
>            = nexts t x y in
>   let ar'  : All Reachable mx'
>            = reachableSpec1 x r y in
>   let av'  : All (Viable n) mx'
>            = allViable gy in
>   let r'   : Reachable x'
>            = allElemSpec0 x' mx' ar' x'emx' in
>   let v'   : Viable n x'
>            = allElemSpec0 x' mx' av' x'emx' in
>   let rvxs : Vect (cardReachableAndViableState (S t) n) (State (S t))
>            = map outl (vectReachableAndViableState (S t) n) in
>   let dRV  : ((x' : State (S t)) -> Dec (ReachableAndViable n x'))
>            = decidableReachableAndViable n in
>   let prf  : Elem x' (vectState (S t))
>            = toVectComplete (finiteState (S t)) x' in
>   let prf' : Elem x' rvxs
>            = filterTagSigmaLemma {P = ReachableAndViable n} dRV x' (vectState (S t)) prf (r',v') in
>   let k    : Fin (cardReachableAndViableState (S t) n)
>            -- = trace ("Lookup " ++ show n) (lookup x' rvxs prf') in
>            = lookup x' rvxs prf' in
>   reward t x y x' `plus` index k vt

> |||
> tabSval' : {t,n : Nat} ->
>            (x  : State t) -> .(r  : Reachable x) -> .(v  : Viable (S n) x) ->
>            (gy  : GoodCtrl t x n) ->
>            (vt : Vect (cardReachableAndViableState (S t) n) Val) ->
>            Vect (cardState (S t)) (Fin (cardReachableAndViableState (S t) n)) ->
>            PossibleNextState x (ctrl gy) -> Val
> tabSval' {t} {n} x r v gy vt iat (MkSigma x' x'emx') =
>   let y    : Ctrl t x
>            = ctrl gy in
>   let k    : Fin (cardReachableAndViableState (S t) n)
>            = index (to (iso (finiteState (S t))) x') iat in
>   reward t x y x' `plus` index k vt

> |||
> tabCval : {t, n : Nat} ->
>           (x  : State t) -> .(r  : Reachable x) -> .(v  : Viable (S n) x) ->
>           (vt : Vect (cardReachableAndViableState (S t) n) Val) ->
>           GoodCtrl t x n -> Val
> tabCval {t} x r v vt gy = let y    : Ctrl t x
>                                    = ctrl gy in
>                           let mx'  : M (State (S t))
>                                    = nexts t x y in
>                           meas (fmap (tabSval x r v gy vt) (tagElem mx'))

> {-
> tabCval' : {t, n : Nat} ->
>            (x  : State t) -> .(r  : Reachable x) -> .(v  : Viable (S n) x) ->
>            (vt : Vect (cardReachableAndViableState (S t) n) Val) ->
>            Vect (cardState (S t)) (Fin (cardReachableAndViableState (S t) n)) ->
>            GoodCtrl t x n -> Val
> tabCval' {t} x r v vt iat gy = let y    : Ctrl t x
>                                         = ctrl gy in
>                                let mx'  : M (State (S t))
>                                         = nexts t x y in
>                                let tmp  : Vect (cardState (S t)) (Fin (cardReachableAndViableState (S t) n))
>                                         = iat in
>                                meas (fmap (tabSval' x r v gy vt iat) (tagElem mx'))
> -}

> |||
> tabCvalargmaxMax : {t, n : Nat} ->
>                    (x  : State t) -> .(r : Reachable x) -> .(v : Viable (S n) x) ->
>                    (vt : Vect (cardReachableAndViableState (S t) n) Val) -> (GoodCtrl t x n, Val)

> |||
> tabCvalargmax : {t, n : Nat} ->
>                 (x  : State t) -> .(r : Reachable x) -> .(v : Viable (S n) x) ->
>                 (vt : Vect (cardReachableAndViableState (S t) n) Val) -> GoodCtrl t x n

> |||
> tabOptExt : {t, n : Nat} -> (vt : ValueTable (S t) n) -> PolicyTable t (S n)
> tabOptExt {t} {n} vt =
>   let ptf  : ((k : Fin (cardReachableAndViableState t (S n))) ->
>               (Sigma (State t) (\ x => (ReachableAndViable {t = t} (S n) x, GoodCtrl t x n))))
>            = \ k => let xrvk : Sigma (State t) (ReachableAndViable {t = t} (S n))
>                              = index k (vectReachableAndViableState t (S n)) in
>                     let x    : State t
>                              = outl xrvk in
>                     let rv   : ReachableAndViable {t = t} (S n) x
>                              = outr xrvk in
>                     let gy   : GoodCtrl t x n
>                              = tabCvalargmax {t = t} {n = n} x (fst rv) (snd rv) vt in
>                     MkSigma x (rv, gy) in
>   let pt   : PolicyTable t (S n)
>            = toVect ptf in
>   pt

> |||
> tabOptExt' : {t, n : Nat} ->
>              (vt : ValueTable (S t) n) ->
>              (PolicyTable t (S n), ValueTable t (S n))
> tabOptExt' {t} {n} vt =
>   let pt    : PolicyTable t (S n)
>             = tabOptExt vt in
>   -- let tmp   = iat {t = S t} {n = n} (believe_me 42) in
>   let vtf'  : ((k : Fin (cardReachableAndViableState t (S n))) -> Val)
>             = \ k => let ptk : Sigma (State t) (\ x => (ReachableAndViable {t = t} (S n) x, GoodCtrl t x n))
>                              = index k pt in
>                      let x   : State t
>                              = outl ptk in
>                      let rv  : ReachableAndViable {t = t} (S n) x
>                              = fst (outr ptk) in
>                      let gy  : GoodCtrl t x n
>                              = snd (outr ptk) in
>                      tabCval x (fst rv) (snd rv) vt gy in
>                      -- tabCval' x (fst rv) (snd rv) vt tmp in
>   let vt'   : ValueTable t (S n)
>             = toVect vtf' in
>   (pt, vt')

... finally

> |||
> tabBackwardsInduction' : (t : Nat) -> (n : Nat) -> (PolicyTableSeq t n, ValueTable t n)
> tabBackwardsInduction' t  Z     =  (Nil, zeroVec (cardReachableAndViableState t Z))
> tabBackwardsInduction' t (S n)  =  let (pts, vt) = tabBackwardsInduction' (S t) n in
>                                    let (pt, vt') = tabOptExt' vt in
>                                    (pt :: pts, vt')

> |||
> tabBackwardsInduction : (t : Nat) -> (n : Nat) -> PolicyTableSeq t n
> tabBackwardsInduction t  Z     =  Nil
> tabBackwardsInduction t (S n)  =  let (pts, vt) = tabBackwardsInduction' (S t) n in
>                                   let pt        = tabOptExt vt in
>                                   pt :: pts

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Data.Matrix.Structural

-- For structural lemmas involving matrix operations
import Control.Algebra
import Control.Algebra.VectorSpace -- definition of module
import Classes.Verified -- definition of verified algebras other than modules
import Data.Matrix
import Data.Matrix.Algebraic -- module instances; from Idris 0.9.20
import Data.Matrix.AlgebraicVerified

import Data.Vect.Structural

%default total

transposeIndexChariz : {xs : Matrix n m a} -> index k $ transpose xs = getCol k xs
transposeIndexChariz {xs=[]} {k} = indexReplicateChariz
transposeIndexChariz {xs=x::xs} {k} = trans zipWithEntryChariz $ vectConsCong _ _ _ transposeIndexChariz

transposeNHead: with Data.Vect ( head $ transpose xs = map head xs )
transposeNHead = trans (sym indexFZIsheadValued) $ trans transposeIndexChariz $ extensionalEqToMapEq (\xs => indexFZIsheadValued {xs=xs}) _

transposeIndicesChariz : {xs : Matrix n m a} -> (i : Fin n) -> (j : Fin m) -> indices j i $ transpose xs = indices i j xs
transposeIndicesChariz i j = trans (cong {f=index i} transposeIndexChariz) indexMapChariz

transposeIsInvolution : with Data.Vect ( transpose $ transpose xs = xs )
transposeIsInvolution {xs} = vecIndexwiseEq (\i => vecIndexwiseEq (\j => trans (transposeIndicesChariz j i) $ transposeIndicesChariz i j))

transposeNTail : with Data.Vect ( transpose $ tail $ transpose xs = map tail xs )
transposeNTail {xs} = vecIndexwiseEq $ \i => vecIndexwiseEq $ \j => trans (transposeIndicesChariz j i)
	$ trans (cong {f=(index i) . (index $ FS j)} $ sym $ headtails $ transpose xs)
	$ trans (transposeIndicesChariz i (FS j))
	$ trans (cong {f=index $ FS j} $ headtails $ index i xs)
	$ sym $ cong {f=index j} indexMapChariz

vecMatMultIsTransposeVecMult : Ring a => (v : Vect n a) -> (xs : Matrix n m a) -> v <\> xs = (transpose xs) </> v
vecMatMultIsTransposeVecMult v xs = Refl

matVecMultIsVecTransposeMult : Ring a => (v : Vect m a) -> (xs : Matrix n m a) -> xs </> v = v <\> (transpose xs)
matVecMultIsVecTransposeMult v xs = sym $ trans (vecMatMultIsTransposeVecMult v $ transpose xs) $ cong {f=(</> v)} $ transposeIsInvolution {xs=xs}

headVecMatMultChariz : Ring a => {xs : Matrix _ (S _) a} -> head $ v<\>xs = v <:> (getCol FZ xs)
headVecMatMultChariz {v} {xs} = trans (sym $ indexFZIsheadValued {xs=v<\>xs})
	$ trans (indexMapChariz {k=FZ} {f=(v<:>)} {xs=transpose xs})
	$ cong {f=(v<:>)} $ transposeIndexChariz {k=FZ} {xs=xs}

matMultIndicesChariz : Ring a => {l : Matrix _ _ a} -> {r : Matrix _ _ a} -> indices i j (l<>r) = (index i l)<:>(getCol j r)
matMultIndicesChariz {l} {r} {i} {j} = trans (cong {f=index j} $ indexMapChariz {f=(<\>r)}) $ trans (indexMapChariz {f=((index i l)<:>)}) $ cong {f=((Vect.index i l)<:>)} transposeIndexChariz

-- But basically from (map) being a verifiable functor.
leadingElemExtensionFirstColReplicate : (r : a) -> getCol FZ $ map (r::) xs = replicate _ r
leadingElemExtensionFirstColReplicate {xs=[]} r = Refl
leadingElemExtensionFirstColReplicate {xs=x::xs} r = vecHeadtailsEq Refl $ leadingElemExtensionFirstColReplicate r

-- But basically from (map) being a verifiable functor.
leadingElemExtensionColFSId : getCol (FS i) $ map (r::) xs = getCol i xs
leadingElemExtensionColFSId {xs} {r} {i} = trans (composeUnderMap xs (index $ FS i) (r::)) $ the (map ((index $ FS i) . (r::)) xs = map (index i) xs) $ extensionalEqToMapEq (\v => Refl) xs

leadingElemExtensionAsZipWithCons : map (r::) xs = Vect.zipWith Vect.(::) (replicate _ r) xs
leadingElemExtensionAsZipWithCons {xs=[]} = Refl
leadingElemExtensionAsZipWithCons {xs=x::xs} = vecHeadtailsEq Refl leadingElemExtensionAsZipWithCons

nullcolExtensionEq : Monoid a => {xs : Matrix n (S predm) a} -> (getCol FZ xs=Algebra.neutral) -> map ((Algebra.neutral)::) $ map Vect.tail xs = xs
nullcolExtensionEq {xs} prColNeut = trans leadingElemExtensionAsZipWithCons
	-- = zipWith (::) Algebra.neutral $ map tail xs
	$ trans (cong {f=zipWith (::) Algebra.neutral} $ sym $ transposeNTail)
	-- = zipWith (::) Algebra.neutral $ transpose $ tail $ transpose xs
	-- === transpose $ Algebra.neutral :: (tail $ transpose xs)
	$ trans (cong {f=transpose}
		$ trans (vecHeadtailsEq
			(trans (sym prColNeut)
				-- Algebra.neutral = getCol FZ xs
				$ trans (sym transposeIndexChariz)
				-- = index FZ $ transpose xs
				$ indexFZIsheadValued)
			Refl)
		-- Algebra.neutral :: (tail $ transpose xs) = head _ :: tail _
		$ sym $ headtails $ transpose xs)
	-- = transpose $ transpose xs
	transposeIsInvolution
	-- = xs

{-
Theorems about the module (Matrix n m a) over a ring (a):
* Compatibility between the Algebra.neutral of the ring (a) and of (Matrix n m a) as a module under (index).
-}

indexNeutralIsNeutral2D : Ring a => (k : Fin n) -> index k $ Algebra.neutral {a=Matrix n m a} = Algebra.neutral
indexNeutralIsNeutral2D FZ = Refl
indexNeutralIsNeutral2D (FS k) = indexNeutralIsNeutral2D k


text:
import InfList

total
getPrefix : (count : Nat) -> InfList ty -> List ty
getPrefix Z xs = []
getPrefix (S k) (value :: xs) = value :: getPrefix k xs

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Graphiti.Egor

%default total

interface PreEgor a where
    leq : a -> a -> Bool
    pEgRefl : { x : a } -> x `leq` x = True
    pEgTrans : { x, y, z : a } ->
        x `leq` y = True ->
            y `leq` z = True ->
                x `leq` z = True

interface SemEgor a where
    pls : a -> a -> a
    plsNeutral : a
    mlt : a -> a -> a
    mltNeutral : a

interface SemEgorGroup a where
    binop : a -> a -> a

interface AditiSemEgor a where
    plus : a -> a -> a

interface MultiSemEgor a where
    mult : a -> a -> a

interface SemEgorGroup a => MonoEgor a where
    neutral : a

interface AditiSemEgor a => MonoAditi a where
    pneutral : a

interface MultiSemEgor a => MonoMulti a where
    mneutral : a

max_stars_repo_name: umbrela-academy/idrusti

max_issues_repo_name: umbrela-academy/idrusti

max_forks_repo_name: umbrela-academy/idrusti


text:
{-
Couple of interesting cases where Idris code generation just shines
-}
module Part2.Sec4_2_2_gen
import Data.Vect

{-
2 case splits and Idris solution search works!
-}
zipV : Vect n a -> Vect n b -> Vect n (a,b)
zipV [] [] = []
-- note this would also work (Idris, you figure it out!)
-- zipV [] _ = []
zipV (x :: xs) (y :: ys) = (x, y) :: zipV xs ys

{-
Bonus case follows the rules above
-}
zipWithV : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWithV f [] [] = []
zipWithV f (x :: xs) (y :: ys) = f x y :: zipWithV f xs ys

{-
  This is again simple case split on the first variable and Idris finds solutions
-}
appendV : Vect n a -> Vect m a -> Vect (n + m) a
appendV [] ys = ys
appendV (x :: xs) ys = x :: appendV xs ys

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
import Control.JS.Async

%foreign "javascript:lambda:(act, time, w) => setTimeout(() => act(w), time)"
prim__setTimeout : PrimIO () -> Int -> PrimIO ()

wait : Int -> Async ()
wait time = prim__async $ \k => prim__setTimeout (k ()) time

main : IO ()
main = launch $ parallel
    [ wait 3000 *> putStrLn "world"
    , wait 1000 *> putStrLn "hello"
    ]


text:
module Test.API3
userAPI : Type


text:
module Main

import Cairo

public export
%foreign
  """
  code:
  func Main_cheapSqrt(x) -> (result):
      tempvar result
      %{
         import math
         ids.result = int(math.sqrt(ids.x))
      %}
      assert x = result * result
      return (result)
  end
  """
cheapSqrt : Felt -> Felt

%noinline
main : Cairo ()
main = output $ cheapSqrt 25

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module C

import Control.Monad.State
import B

-- there is an error in this code, since C doesn't import A, but B relies of A to describe
-- the type 'X'. Idris responds with the following appropriate error message, but takes a long time
-- to figure out what's wrong.
-- Error: While processing right hand side of foo. Undefined name A.AFoo.

foo : X ()
foo =
  do
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()
    pure ()


text:
module Idris.ModTree

import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Directory
import Core.Metadata
import Core.Options
import Core.Primitives
import Core.InitPrimitives
import Core.UnifyState

import Idris.Desugar
import Idris.Error
import Idris.Parser
import Idris.ProcessIdr
import Idris.REPLCommon
import Idris.Syntax
import Idris.Pretty

import Data.List
import Data.StringMap

import System.Directory
import System.File

import Utils.Either

%default covering

record ModTree where
  constructor MkModTree
  nspace : ModuleIdent
  sourceFile : Maybe String
  deps : List ModTree

Show ModTree where
  show t = show (sourceFile t) ++ " " ++ show (nspace t) ++ "<-" ++ show (deps t)

-- A module file to build, and its list of dependencies
-- From this we can work out if the source file needs rebuilding, assuming
-- things are build in dependency order. A source file needs rebuilding
-- if:
--  + Its corresponding ttc is older than the source file
--  + Any of the import ttcs are *newer* than the corresponding ttc
--    (If so: also any imported ttc's fingerprint is different from the one
--    stored in the source file's ttc)
public export
record BuildMod where
  constructor MkBuildMod
  buildFile : String
  buildNS : ModuleIdent
  imports : List ModuleIdent

export
Show BuildMod where
  show t = buildFile t ++ " [" ++ showSep ", " (map show (imports t)) ++ "]"

data AllMods : Type where

mkModTree : {auto c : Ref Ctxt Defs} ->
            {auto a : Ref AllMods (List (ModuleIdent, ModTree))} ->
            FC ->
            (done : List ModuleIdent) -> -- if 'mod' is here we have a cycle
            (mod : ModuleIdent) ->
            Core ModTree
mkModTree loc done mod
  = if mod `elem` done
       then throw (CyclicImports (done ++ [mod]))
       else
          -- Read imports from source file. If the source file isn't
          -- available, it's not our responsibility
          catch (do all <- get AllMods
                    -- If we've seen it before, reuse what we found
                    case lookup mod all of
                         Nothing =>
                           do file <- nsToSource loc mod
                              modInfo <- readHeader file
                              let imps = map path (imports modInfo)
                              ms <- traverse (mkModTree loc (mod :: done)) imps
                              let mt = MkModTree mod (Just file) ms
                              all <- get AllMods
                              put AllMods ((mod, mt) :: all)
                              pure mt
                         Just m => pure m)
                -- Couldn't find source, assume it's in a package directory
                (\err =>
                    case err of
                         CyclicImports _ => throw err
                         _ => pure (MkModTree mod Nothing []))

data DoneMod : Type where
data BuildOrder : Type where

-- Given a module tree, returns the modules in the reverse order they need to
-- be built, including their dependencies
mkBuildMods : {auto d : Ref DoneMod (StringMap ())} ->
              {auto o : Ref BuildOrder (List BuildMod)} ->
              ModTree -> Core ()
mkBuildMods mod
    = maybe (pure ())
         (\sf =>
            do done <- get DoneMod
               case lookup sf done of
                    Just _ => pure ()
                    Nothing =>
                       do -- build dependencies
                          traverse_ mkBuildMods (deps mod)
                          -- build it now
                          bo <- get BuildOrder
                          put BuildOrder
                                (MkBuildMod sf (nspace mod)
                                            (map nspace (deps mod)) :: bo)
                          done <- get DoneMod
                          put DoneMod (insert sf () done))
         (sourceFile mod)

-- Given a main file name, return the list of modules that need to be
-- built for that main file, in the order they need to be built
-- Return an empty list if it turns out it's in the 'done' list
getBuildMods : {auto c : Ref Ctxt Defs} ->
               {auto o : Ref ROpts REPLOpts} ->
               FC -> (done : List BuildMod) ->
               (mainFile : String) ->
               Core (List BuildMod)
getBuildMods loc done fname
    = do a <- newRef AllMods []
         d <- getDirs
         fname_ns <- pathToNS (working_dir d) (source_dir d) fname
         if fname_ns `elem` map buildNS done
            then pure []
            else
              do t <- mkModTree {a} loc [] fname_ns
                 dm <- newRef DoneMod empty
                 o <- newRef BuildOrder []
                 mkBuildMods {d=dm} {o} t
                 pure (reverse !(get BuildOrder))

fnameModified : String -> Core Integer
fnameModified fname
    = do Right f <- coreLift $ openFile fname Read
             | Left err => throw (FileErr fname err)
         Right t <- coreLift $ fileModifiedTime f
             | Left err => do coreLift $ closeFile f
                              throw (FileErr fname err)
         coreLift $ closeFile f
         pure (cast t)

buildMod : {auto c : Ref Ctxt Defs} ->
           {auto s : Ref Syn SyntaxInfo} ->
           {auto o : Ref ROpts REPLOpts} ->
           FC -> Nat -> Nat -> BuildMod ->
           Core (List Error)
-- Build from source if any of the dependencies, or the associated source
-- file, have a modification time which is newer than the module's ttc
-- file
buildMod loc num len mod
   = do clearCtxt; addPrimitives
        lazyActive True; setUnboundImplicits True
        let src = buildFile mod
        mttc <- getTTCFileName src "ttc"
        -- We'd expect any errors in nsToPath to have been caught by now
        -- since the imports have been built! But we still have to check.
        depFilesE <- traverse (nsToPath loc) (imports mod)
        let (ferrs, depFiles) = partitionEithers depFilesE
        ttcTime <- catch (do t <- fnameModified mttc
                             pure (Just t))
                         (\err => pure Nothing)
        srcTime <- fnameModified src
        depTimes <- traverse (\f => do t <- fnameModified f
                                       pure (f, t)) depFiles
        let needsBuilding =
               case ttcTime of
                    Nothing => True
                    Just t => any (\x => x > t) (srcTime :: map snd depTimes)
        u <- newRef UST initUState
        m <- newRef MD initMetadata
        put Syn initSyntax

        if needsBuilding
           then do let msg : Doc IdrisAnn = pretty num <+> slash <+> pretty len <+> colon
                               <++> pretty "Building" <++> pretty mod.buildNS <++> parens (pretty src)
                   [] <- process {u} {m} msg src
                      | errs => do emitWarnings
                                   traverse emitError errs
                                   pure (ferrs ++ errs)
                   emitWarnings
                   traverse_ emitError ferrs
                   pure ferrs
           else do emitWarnings
                   traverse_ emitError ferrs
                   pure ferrs

buildMods : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto o : Ref ROpts REPLOpts} ->
            FC -> Nat -> Nat -> List BuildMod ->
            Core (List Error)
buildMods fc num len [] = pure []
buildMods fc num len (m :: ms)
    = case !(buildMod fc num len m) of
           [] => buildMods fc (1 + num) len ms
           errs => pure errs

export
buildDeps : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            {auto o : Ref ROpts REPLOpts} ->
            (mainFile : String) ->
            Core (List Error)
buildDeps fname
    = do mods <- getBuildMods toplevelFC [] fname
         ok <- buildMods toplevelFC 1 (length mods) mods
         case ok of
              [] => do -- On success, reload the main ttc in a clean context
                       clearCtxt; addPrimitives
                       put MD initMetadata
                       mainttc <- getTTCFileName fname "ttc"
                       log "import" 10 $ "Reloading " ++ show mainttc ++ " from " ++ fname
                       readAsMain mainttc

                       -- Load the associated metadata for interactive editing
                       mainttm <- getTTCFileName fname "ttm"
                       log "import" 10 $ "Reloading " ++ show mainttm
                       readFromTTM mainttm
                       pure []
              errs => pure errs -- Error happened, give up

export
loadModules : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              {auto o : Ref ROpts REPLOpts} ->
              (namespaces : List ModuleIdent) ->
              Core ()
loadModules namespaces = do
  -- Load the the TTC files in a clean context
  clearCtxt; addPrimitives
  put MD initMetadata
  traverse (\ns => readModule True emptyFC True ns (miAsNamespace ns)) namespaces
  pure ()

export
getAllBuildMods : {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
                  {auto o : Ref ROpts REPLOpts} ->
                  (allFiles : List String) ->
                  Core (List BuildMod)
getAllBuildMods allFiles = do
  mods <- getMods toplevelFC [] allFiles
  pure $ dropLater mods
  where
    getMods : FC -> (done : List BuildMod) ->
              (allFiles : List String) ->
              Core (List BuildMod)
    getMods fc done [] = pure done
    getMods fc done (f :: fs)
        = do ms <- getBuildMods fc done f
             getMods fc (ms ++ done) fs
    dropLater : List BuildMod -> List BuildMod
    dropLater [] = []
    dropLater (b :: bs)
        = b :: dropLater (filter (\x => buildFile x /= buildFile b) bs)

export
filterUsedByMods : List ModuleIdent -> List BuildMod -> List BuildMod
filterUsedByMods [] mods = []
filterUsedByMods (x :: xs) mods =
   let (ancestors, restMods) = partition (\mod => x `elem` mod.imports) mods
   in ancestors ++ assert_total (filterUsedByMods (xs ++ map buildNS ancestors) restMods)

export
buildAll : {auto c : Ref Ctxt Defs} ->
           {auto s : Ref Syn SyntaxInfo} ->
           {auto o : Ref ROpts REPLOpts} ->
           List BuildMod ->
           Core (List Error)
buildAll mods = buildMods toplevelFC 1 (length mods) mods


text:
module Collections.BSTree.Map.Core

import Collections.Util.Bnd
import Control.Relation
import Decidable.Order.Strict

||| A verified binary search tree with erased proofs.
|||
||| The keys in the tree are constrained by min/max bounds, which make use of `Bnd` to extend the
||| tree key type with `Top` and `Bot` values. This allows for a natural way to leave bounds
||| unconstrained (by having a minimum of `Bot` or a maximum of `Top`).
|||
||| @ ord The ordering implementations used in the tree. Since these are w.r.t. a type `kTy`, the
|||       type of tree keys is defined implicitly by `ord`.
||| @ vTy The data type to carry in nodes in addition to the key type `kTy`.
||| @ mn  The minimum value constraint, proving that `rel mn (Mid x)` for all values `x` in the
|||       tree.
||| @ mx  The maximum value constraint, proving that `rel (Mid x) mx` for all values `x` in the
|||       tree.
public export
data BST : {0 rel : kTy -> kTy -> Type} ->
           (pre : StrictPreorder kTy rel) ->
           (tot : StrictOrdered kTy rel) ->
           (0 vTy : Type) ->
           (0 mn,mx : Bnd kTy) ->
           Type where
  ||| An empty tree node.
  |||
  ||| @ prf An ordering proof on the min and max constraints of this node. Since an in-order
  |||       traversal of a binary tree is an empty-node-empty-... alternation, storing ordering
  |||       information in the empty nodes is a natural way to store evidence that the nodes are in
  |||       order.
  Empty : {pre : StrictPreorder kTy rel} ->
          {tot : StrictOrdered kTy rel} ->
          (0 prf : BndLT rel mn mx) ->
          BST pre tot vTy mn mx
  ||| A node with a value and with left and right subtrees, each with appropriate bounds relative
  ||| to the key `k` of the node.
  |||
  ||| @ k The key value of the node
  ||| @ v The data value of the node
  ||| @ l The left subtree
  ||| @ r The right subtree
  Node  : {0 rel : kTy -> kTy -> Type} ->
          {pre : StrictPreorder kTy rel} ->
          {tot : StrictOrdered kTy rel} ->
          (k : kTy) ->
          (v : vTy) ->
          (l : BST pre tot vTy mn (Mid k)) ->
          (r : BST pre tot vTy (Mid k) mx) ->
          BST pre tot vTy mn mx
%name BST t,u,v

||| A verified binary search tree with erased proofs.
|||
||| This is an alias for the more generic `BST` (which accepts min/max bounds for its contents).
||| The bounds are necessary for verifying the structure of a tree, but the root node of any
||| `BST` will always be unconstrained. So generally, `BST` can be considered an implementation
||| detail.
|||
||| @ rel The strict total ordering used in the tree. Since a `StrictOrdered` impl is w.r.t. a type
|||       `kTy`, the type of tree values is defined implicitly by `ord`.
||| @ vTy The type for values stored in nodes of the tree.
public export
BSTree : {0 kTy : Type} ->
         (0 rel : kTy -> kTy -> Type) ->
         {auto pre : StrictPreorder kTy rel} ->
         {auto tot : StrictOrdered kTy rel} ->
         (0 vTy : Type) ->
         Type
BSTree rel {pre} {tot} vTy = BST pre tot vTy Bot Top
%name BSTree t,u,v

||| Proof that the minimum bound can be decreased arbitrarily.
public export
extendMin : {0 rel : kTy -> kTy -> Type} ->
            {pre : StrictPreorder kTy rel} ->
            {tot : StrictOrdered kTy rel} ->
            (0 prf : BndLT rel mn' mn) ->
            BST pre tot vTy mn mx ->
            BST pre tot vTy mn' mx
extendMin {pre} prf (Empty prf')   = Empty $ transitive {x=mn'} {y=mn} {z=mx} prf prf'
extendMin       prf (Node k v l r) = Node k v (extendMin prf l) r

||| Proof that the maximum bound can be increased arbitrarily.
public export
extendMax : {0 rel : kTy -> kTy -> Type} ->
            {pre : StrictPreorder kTy rel} ->
            {tot : StrictOrdered kTy rel} ->
            (0 prf : BndLT rel mx mx') ->
            BST pre tot vTy mn mx ->
            BST pre tot vTy mn mx'
extendMax {pre} prf (Empty prf')   = Empty $ transitive {x=mn} {y=mx} {z=mx'} prf' prf
extendMax       prf (Node k v l r) = Node k v l (extendMax prf r)

max_stars_repo_name: polendri/idris-collections

max_issues_repo_name: polendri/idris-collections

max_forks_repo_name: polendri/idris-collections


text:
module Lists

import Control.ST
import Control.ST.Exception
import DataTypes
import Util

%access public export

car : PrimitiveLispFunc
car [LispDottedList (x::_) _] = pure x
car [LispList []] = Left $ Default "Unexpected error in car"
car [LispList (x::_)] = pure x
car [badArg] = Left $ Default $ "car expected pair, found " ++ show badArg
car badArgList =
  Left $ NumArgs (MinMax 1 1) (cast $ length badArgList) badArgList

cdr : PrimitiveLispFunc
cdr [LispDottedList [_] a] = pure a
cdr [LispDottedList (_::xs) a] = pure $ LispDottedList xs a
cdr [LispList []] = Left $ Default "cdr on empty list" -- TODO: FIX ERROR MSG
cdr [LispList (_::[])] = pure $ LispList []
cdr [LispList (_::a)] = pure $ LispList a
cdr [badArg] = Left $ Default $ "cdr expected pair, found " ++ show badArg
cdr badArgList =
  Left $ NumArgs (MinMax 1 1) (cast $ length badArgList) badArgList

cons : PrimitiveLispFunc
cons [a, LispList b] = pure $ LispList (a :: b)
cons [a, LispDottedList b c] = pure $ LispDottedList (a :: b) c
cons [a, b] = pure $ LispDottedList [a] b
cons badArgList =
  Left $ NumArgs (MinMax 2 2) (cast $ length badArgList) badArgList

isPair : PrimitiveLispFunc
isPair [LispList []] = pure $ LispBool False
isPair [LispList _] = pure $ LispBool True
isPair [LispDottedList _ _] = pure $ LispBool True
isPair _ = pure $ LispBool False

empty : PrimitiveLispFunc
empty [LispList []] = pure $ LispBool True
empty [LispList _] = pure $ LispBool False
empty [args] = Left $ TypeMismatch "list" args
empty args = Left $ NumArgs (MinMax 1 1) (cast $ length args) args

accessors : List (String, PrimitiveLispFunc)
accessors =
  map (\a => ("c" ++ pack a ++ "r", makeAccessor a)) caaaars
  where
    caaaars : List (List Char)
    caaaars = (replicateM 2 ['a', 'd']) ++ (replicateM 3 ['a', 'd']) ++ (replicateM 4 ['a', 'd'])
    comp : PrimitiveLispFunc -> PrimitiveLispFunc -> PrimitiveLispFunc
    comp a b c = do
        d <- a c
        b [d]
    identity : PrimitiveLispFunc
    identity [n] = pure n
    identity a = pure $ LispList a
    makeAccessor : List Char -> PrimitiveLispFunc
    makeAccessor =
        foldr (\chr, acc =>
            if chr == 'a'
                then comp acc car
                else comp acc cdr)
            identity

list : PrimitiveLispFunc
list xs = pure $ LispList xs

isList : PrimitiveLispFunc
isList [LispList x] = pure $ LispBool True
isList _ = pure $ LispBool False

listLength : PrimitiveLispFunc
listLength [LispList xs] = pure $ LispInteger (cast $ length xs)
listLength [args] = Left $ TypeMismatch "list" args
listLength args = Left $ NumArgs (MinMax 1 1) (cast $ length args) args

listAppend : PrimitiveLispFunc
listAppend [LispList xs, LispList ys] = pure $ LispList (xs++ ys)
listAppend xs = helper [] xs
  where
    helper : List LispVal -> PrimitiveLispFunc
    helper acc [] = pure $ LispList acc
    helper acc [LispDottedList ls v] = pure $ LispDottedList (acc ++ ls) v
    helper [] [v] = pure $ v
    helper acc [v] = pure $ LispDottedList acc v
    helper acc ((LispList xs)::rest) = helper (acc ++ xs) rest
    helper _ (x::xs) = Left $ TypeMismatch "list" x
    helper _ _ = Left $ Default "Unknown error in append"

listReverse : PrimitiveLispFunc
listReverse [] = Left $ NumArgs (MinMax 1 1) 0 []
listReverse [LispList xs] = pure $ LispList (reverse xs)
listReverse [arg] = Left $ TypeMismatch "list" arg
listReverse args = Left $ NumArgs (MinMax 1 1) (cast $ length args) args

listMember : PrimitiveLispFunc
listMember [needle, LispList xs] = helper xs
    where
      helper : PrimitiveLispFunc
      helper [] = pure $ LispBool False
      helper (x::xs) =
        if x == needle
          then pure $ LispList (x::xs)
          else helper xs
listMember [_, arg] = Left $ TypeMismatch "list" arg
listMember args = Left $ NumArgs (MinMax 1 1) (cast $ length args) args

listPrimitives : List (String, PrimitiveLispFunc)
listPrimitives =
  [ ("pair?", isPair)
  , ("car", car)
  , ("cdr", cdr)
  , ("cons", cons)
  , ("empty?", empty)
  , ("null?", empty)
  , ("list", list)
  , ("list?", isList)
  , ("length", listLength)
  , ("append", listAppend)
  , ("reverse", listReverse)
  , ("member", listMember)
  ] ++
  accessors

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module Sub05Apply9x6

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(3x+2) --C[4,-4]--> 3x
c9x6To3x :
  (j:Nat) -> P (S (S (plus (plus j j) j))) 2 -> P j 2
c9x6To3x j prf =
  let prf2 = lvDown (S (S (plus (plus j j) j))) 2 prf in c9x6To3x' j prf2

export
apply9x6 : P (S (S (plus (plus j j) j))) 2
  -> (m : Nat ** (LTE (S m) (S (S (plus (plus j j) j))), P m 2))
apply9x6 {j} col = let col2 = c9x6To3x j col in (j ** (lte9x6 j, col2)) where
  lte9x6 : (j:Nat) -> LTE (S j) (S (S (plus (plus j j) j)))
  lte9x6 Z = (lteSuccRight . LTESucc) LTEZero
  lte9x6 (S j) = let lemma = lte9x6 j in
    rewrite (sym (plusSuccRightSucc j j)) in
    rewrite (sym (plusSuccRightSucc (plus j j) j)) in
      (lteSuccRight . lteSuccRight . LTESucc) lemma
-- ---------------------------


text:
import Data.Vect

createEmpties : Vect n (Vect 0 elem)
createEmpties = replicate _ []

-- This is just zipWith (::)
transposeHelper : (x : Vect n elem) ->
                  (xsTrans : Vect n (Vect len elem)) ->
                  Vect n (Vect (S len) elem)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys

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

-- Exercise 3.3.2
addMatrix : Num numType =>
            Vect rows (Vect cols numType) ->
            Vect rows (Vect cols numType) ->
            Vect rows (Vect cols numType)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (+) x y :: addMatrix xs ys

-- Exercise 3.3.3
-- check: multMatrix [[1,2], [3,4], [5,6]] [[7,8,9.10], [11,12,13,14]]
-- equals: [[29, 32,,,], [65,,,],,,]
multMatrix : Num numType =>
             Vect n (Vect m numType) ->
             Vect m (Vect p numType) ->
             Vect n (Vect p numType)
multMatrix xs ys = ?multMatrix_rhs1 xs (transposeMat ys)

max_stars_repo_name: defndaines/idris-bits

max_issues_repo_name: defndaines/idris-bits

max_forks_repo_name: defndaines/idris-bits


text:
{-
cd collatzProof_DivSeq/program2
chcp 65001
idris
-}
module ProofColDivSeqBase

%default total
-- %language ElabReflection
%access export

-- mod2
public export
data Parity : Nat -> Type where
  Even : Parity (n + n)
  Odd  : Parity (S (n + n))
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p
helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
helpOdd j p = rewrite plusSuccRightSucc j j in p
parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})
  parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})

-- mod3
public export
data Mod3 : Nat -> Type where
  ThreeZero : Mod3 (n + n + n)
  ThreeOne  : Mod3 (S (n + n + n))
  ThreeTwo  : Mod3 (S (S (n + n + n)))
helpThreeZero : (j:Nat) -> (plus (plus (S j) (S j)) (S j)) = S (S (S (plus (plus j j) j)))
helpThreeZero j = rewrite sym $ plusSuccRightSucc j j in
                  rewrite sym $ plusSuccRightSucc (plus j j) j in Refl
helpThreeOne : (j:Nat) -> S (plus (plus (S j) (S j)) (S j)) = S (S (S (S (plus (plus j j) j))))
helpThreeOne j = cong {f=S} $ helpThreeZero j
helpThreeTwo : (j:Nat) -> S (S (plus (plus (S j) (S j)) (S j))) = S (S (S (S (S (plus (plus j j) j)))))
helpThreeTwo j = cong {f=S} $ helpThreeOne j
mod3 : (n:Nat) -> Mod3 n
mod3 Z         = ThreeZero {n=Z}
mod3 (S Z)     = ThreeOne {n=Z}
mod3 (S (S Z)) = ThreeTwo {n=Z}
mod3 (S (S (S k))) with (mod3 k)
  mod3 (S (S (S (j + j + j))))         | ThreeZero =
    rewrite sym $ helpThreeZero j in ThreeZero {n=S j}
  mod3 (S (S (S (S (j + j + j)))))     | ThreeOne =
    rewrite sym $ helpThreeOne j in ThreeOne {n=S j}
  mod3 (S (S (S (S (S (j + j + j)))))) | ThreeTwo =
    rewrite sym $ helpThreeTwo j in ThreeTwo {n=S j}
-- ---------------------------------

-- divSeqの実装に必要な関数
    -- ----- from libs/contrib/Data/CoList.idr -----
public export
codata CoList : Type -> Type where
  Nil : CoList a
  (::) : a -> CoList a -> CoList a

implementation Functor CoList where
  map f []      = []
  map f (x::xs) = f x :: map f xs

implementation Show a => Show (CoList a) where
  show xs = "[" ++ show' "" 20 xs ++ "]" where
    show' : String -> (n : Nat) -> (xs : CoList a) -> String
    show' acc Z _             = acc ++ "..."
    show' acc (S n) []        = acc
    show' acc (S n) [x]       = acc ++ show x
    show' acc (S n) (x :: xs) = show' (acc ++ (show x) ++ ", ") n xs

unfoldr : (a -> Maybe (b, a)) -> a -> CoList b
unfoldr f x =
  case f x of
    Just (y, new_x) => y :: (unfoldr f new_x)
    _               => []
    -- ----- from libs/contrib/Data/CoList.idr -----

countEven : Nat -> Nat -> Nat -> (Nat, Nat)
countEven n Z      acc = (acc, n)
countEven n (S nn) acc =
  if (modNatNZ n 2 SIsNotZ) == 1
    then (acc, n)
    else countEven (divNatNZ n 2 SIsNotZ) nn (acc+1)

-- divSeqの実装
divSeq : Nat -> CoList Integer
divSeq n = divSeq' n n
  where
    divSeq' : Nat -> Nat -> CoList Integer
    divSeq' n     Z     = []
    divSeq' Z     (S k) = []
    divSeq' (S n) (S k) with (parity n)
      divSeq' (S (S (j + j))) (S k) | Odd  = divSeq' (S j) k
      divSeq' (S (j + j)    ) (S k) | Even =
        map toIntegerNat
          (unfoldr (\b => if b <= 1 then Nothing
                                    else Just (countEven (b*3+1) (b*3+1) 0) ) (S (j + j)))
definiDivSeq0 : divSeq Z = []
definiDivSeq0 = Refl
-- ---------------------------------

-- その他関数
limitedNStep : CoList Integer -> Nat -> Bool
limitedNStep []        _     = True
limitedNStep (_ :: _)  Z     = False
limitedNStep (_ :: xs) (S n) = limitedNStep xs n
definiLimited0 : limitedNStep [] Z = True
definiLimited0 = Refl
-- ---------------------------------


text:
module FreeQ

%default total
%access public export

||| Type representing a query type which encodes a query _request_ (presumably a
||| GADT), paired with a handler for it.
record HandledQry (q : Type -> Type)  (a : Type) where
  constructor HandleQry
  qry : q i
  handle : i -> a

||| HandledQry q is a strictly positive functor, regardless of the shape of q!
Functor (HandledQry q) where
  map f (HandleQry qry handle) = HandleQry qry (f . handle)

||| Since the standard Haskell-style Free monad is not strictly positive, and I
||| do not understand yet how to constrain a functor to be strictly positive;
||| nor do I understand Conor McBride's `General` free monad in
||| [Turing-Completeness Totally
||| Free](https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b814f6502630239f.pdf)
||| I define a FreeQ: a version of free that is monomorphic to the concept of a
||| handled query---that is, of a query GADT paired with a handler
||| function---but not monorphic to the specific query GADT. This definition is
||| then strictly positive. With the addition of a size to the type, the
||| consuming code is able to be total. Thus I am able to get one definition of
||| free for all my query DSLs, which is everywhere to date that I have
||| personally had a need for free monads, and yet maintain my dogmatism about
||| total programming. I don't doubt that sometime in the future I will have a
||| need for free monads with something that is not a query. But let the future
||| be the future. For now, it would be a tremendous step forward in my F# code
||| if I could use this approach!
data FreeQ : Nat -> (Type -> Type) -> Type -> Type where
  PureQ : a -> FreeQ Z f a
  BindHQ : HandledQry q (FreeQ n (HandledQry q) a)
         -> FreeQ (S n) (HandledQry q) a

Sized (FreeQ n f a) where
  size {n} _ = n

||| Thankfully due to the nature of functor, we are ablel to implement the
||| interface, since it does not change the size of our FreeQ.
Functor f => Functor (FreeQ n f) where
  map f (PureQ x) = PureQ (f x)
  map f (BindHQ slave) = BindHQ (map (map f) slave)

||| Recover applicative and monad instances by lifting... I mean half the point
||| of a free monad is to actually be able to use do notation etc. right?
record FreeQry (q : Type -> Type) a where
  constructor WrapFHQ
  unwrapFHQ : FreeQ qsize (HandledQry q) a

Sized (FreeQry q a) where
  size (WrapFHQ q) = size q

Functor (FreeQry q) where
  map f (WrapFHQ x) = WrapFHQ $ map f x

||| Applicative apply, except we can't implement the type class because the size
||| of our type changes between inputs and output.
apfq : Functor f => FreeQ n f (a -> b) -> FreeQ m f a -> FreeQ (n + m) f b
apfq {n=Z} (PureQ y) x = map y x
apfq (BindHQ y) x = BindHQ (map (flip apfq x) y)

Applicative (FreeQry q) where
  pure x = WrapFHQ (PureQ x)
  (WrapFHQ f) <*> (WrapFHQ x) = WrapFHQ $ apfq f x

||| Monad bind, except we can't implement the type class because the size of our
||| type changes between inputs and output.
bindfq : Functor f => (a -> FreeQ n f b) -> FreeQ m f a -> FreeQ (m + n) f b
bindfq {n} {m=Z} f (PureQ x) = f x
bindfq f (BindHQ x) = BindHQ (map (bindfq f) x)

||| Monad join, except we can't implement the type class because the size of our
||| type changes between inputs and output.
joinfq : Functor f => FreeQ n f (FreeQ m f a) -> FreeQ (n + m) f a
joinfq (PureQ x) = x
joinfq (BindHQ x) = BindHQ (map joinfq x)

join' : FreeQ n (HandledQry q) (FreeQry q a) -> FreeQry q a
join' {n=Z} (PureQ x) = x
join' {n=S m} (BindHQ x) =
  ?asdf $ map join' x
  --WrapFHQ (S m) $ BindHQ $ map (unwrapFHQ . join' m) x

Monad (FreeQry q) where
  join (WrapFHQ x) = join' x

||| Example specific query GADT
data FSQry : Type -> Type where
  LsFiles : String -> FSQry (List String)
  ReadText : String -> FSQry String
  DirExists : String -> FSQry Bool

||| Example accompanying commands, to in conjunction with the FSQry, form a sort
||| of little filesystem DSL.
data FSCmd
  = WriteLines String (List String)
  | CreateDir String
  | DeleteFile String
  | DeleteDir String

--B : Functor f => f (FreeQ f a) -> FreeQ f a
--B x = assert_total $ BindHQ x
--
--traverse : Functor f => (a -> FreeQ f b) -> List a -> FreeQ f (List b)
--traverse f [] = pure List.Nil
--traverse f (x::xs) = [| List.(::) (f x) (traverse f xs) |]
--
--liftQry : Qry a -> FreeQ Qry a
--liftQry x = B (map PureQx)
--
--lsFiles : String -> FreeQ Qry (List String)
--lsFiles = liftQry . LsFiles id
--
--readText : String -> FreeQ Qry String
--readText = liftQry . ReadText id
--
--lmap : (a -> b) -> List a -> List b
--lmap f [] = []
--lmap f (x :: xs) = f x :: lmap f xs
--
--consolidate : String -> String -> FreeQ Qry (List Cmd)
--consolidate frum tu = do
--  files <- lsFiles frum
--  texts <- traverse readText files
--  pure $ lmap DeleteFile files ++ [DeleteDir frum, CreateDir tu, WriteLines (tu ++ "/" ++ "consolidated.txt") texts]


text:
module Main

import System
import Effects
import Effect.Random
import Data.Vect

total
insert : Ord a => a -> Vect n a -> Vect (S n) a
insert x [] = [x]
insert x (y :: ys) = if (x < y) then x :: y :: ys else y :: insert x ys

vsort : Ord a => Vect n a -> Vect n a
vsort [] = []
vsort (x :: xs) = insert x (vsort xs)

mkSortVec : (n : Nat) -> Eff (Vect n Int) [RND]
mkSortVec Z = pure []
mkSortVec (S k) = pure (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))

main : IO ()
main = do
    arg <- getLine
    let vec = runPure $ (srand 123456789 *> mkSortVec (fromInteger (cast arg)))
    putStrLn "Made vector"
    printLn (vsort vec)

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module Project

%default total
%access public export

record GenModule where
  constructor GenMod
  fileName : String
  moduleName : String
  genExpr : List String

||| Example:
|||   templates
|||     Free.fs
|||   source
|||     Queries.fspp
|||   generate
|||     EnvQry.fs
|||       module MyNamespace.EnvQry
|||       gen EnvQry
|||       gen Free EnvQry
|||     FSQry.fs
|||       module MyNamespace.FSQry
|||       gen FSQry
|||       gen Free FSQry
record Project where
  constructor Proj
  templates, source : List String
  generate : List GenModule

Semigroup Project where
  p <+> q =
    let t = templates p <+> templates q
        s = source p <+> source q
        g = generate p <+> generate q
    in Proj t s g

Monoid Project where
  neutral = Proj [] [] []

ofTmpl : List String -> Project
ofTmpl t = Proj t [] []

ofSrc : List String -> Project
ofSrc s = Proj [] s []

ofGen : List GenModule -> Project
ofGen g = Proj [] [] g

Token : Type
Token = (Nat, String)

data Error
  = OddNSpaces Nat
  | UnrecognizedTopLevel String
  | UnexpectedIndentation Nat String

tokenizeOne : List Char -> Either Error (Maybe Token)
tokenizeOne = tokenize1 Z where
  tokenize1 : Nat -> List Char -> Either Error (Maybe Token)
  tokenize1 _ [] = Right Nothing
  tokenize1 _ (_ :: []) = Right Nothing
  tokenize1 k (' ' :: ' ' :: cs) = tokenize1 (S k) cs
  tokenize1 k (' ' :: _ :: _) = Left (OddNSpaces (k * 2 + 1))
  tokenize1 k cs@(_ :: _ :: _) = Right $ Just (k, pack cs)

tokenize : String -> Either (List (Nat, Error)) (List Token)
tokenize text =
  let ls = lines text
      lineNs = take (length ls) $ iterate S Z
      results = zip lineNs $ map (tokenizeOne . unpack) ls
  in foldr addResult (Right []) results where
    addResult : (Nat, Either Error (Maybe Token))
              -> Either (List (Nat, Error)) (List Token)
              -> Either (List (Nat, Error)) (List Token)
    addResult (k, Left e) (Left l) = Left ((k, e) :: l)
    addResult (_, _) x@(Left _) = x
    addResult (_, Right Nothing) x@(Right _) = x
    addResult (_, Right (Just tok)) (Right toks) = Right (tok :: toks)
    addResult (k, Left e) (Right _) = Left [(k, e)]

dropPlus1Smaller : (x : a) -> (xs : List a) -> (n : Nat)
                 -> Smaller (List.drop n xs) (x :: xs)
dropPlus1Smaller x [] Z = LTESucc LTEZero
dropPlus1Smaller x [] (S k) = LTESucc LTEZero
dropPlus1Smaller x (y :: xs) Z = lteRefl
dropPlus1Smaller x (y :: ys) (S k) =
  LTESucc $ lteSuccLeft $ dropPlus1Smaller x ys k

parseGenMods : List Token -> Either Error (List GenModule)
parseGenMods toks = ?blargh

step : (xs : List Token)
     -> ((ys : List Token) -> Smaller ys xs -> Project -> Either Error Project)
     -> Project -> Either Error Project
step [] _ p = Right p
step (x@(Z, "templates") :: xs) f p =
  let tmpls = map snd $ takeWhile ((== 1) . fst) xs
      p' = p <+> ofTmpl tmpls
      n = length tmpls
      rem = drop n xs in
  f rem (dropPlus1Smaller x xs n) p
step (x@(Z, "source") :: xs) f p =
  let srcs = map snd $ takeWhile ((== 1) . fst) xs
      p' = p <+> ofSrc srcs
      n = length srcs
      rem = drop n xs in
  f rem (dropPlus1Smaller x xs n) p
step (x@(Z, "generate") :: xs) f p =
  let raw = takeWhile ((> 0) . fst) xs in
  case parseGenMods raw of
    Left e => Left e
    Right genMods =>
      let p' = p <+> ofGen genMods
          n = length raw
          rem = drop n xs in
      f rem (dropPlus1Smaller x xs n) p
step ((Z,  x) :: _) _ _ = Left $ UnrecognizedTopLevel x
step ((S n,  x) :: _) _ _ = Left $ UnexpectedIndentation (S n) x

parseToks : List Token -> Either Error Project
parseToks toks =
  let addToProject = sizeRec step toks
  in addToProject neutral

parse : String -> Project
parse x = ?parse_rhs

max_stars_repo_name: Kazark/fspp

max_issues_repo_name: Kazark/fspp

max_forks_repo_name: Kazark/fspp


text:
twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible

valueNotSuc : (x : Nat) -> x = S x -> Void
valueNotSuc _ Refl impossible

loop : Void
loop = loop

partial
nohead : Void
nohead = getHead []
  where
    partial
    getHead : List Void -> Void
    getHead (x :: xs) = x


text:
-- --------------------------------------------------------------- [ Model.idr ]
-- Module    : Model.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Example of using PML to model a paper.
module GRL.Lang.Test.PML

import GRL.Lang.PML

-- ------------------------------------------------------------------- [ Paper ]

paper : PAPER
paper = MkPaper "My First Paper"

abst : ABSTRACT
abst = MkAbs

bib : BIB
bib = MkBib

intr : SECT
intr = MkSect "Introduction"

meth : SECT
meth = MkSect "Methodology"

res : SECT
res = MkSect "Results"

disc : SECT
disc = MkSect "Discussion"

-- ------------------------------------------------------------------- [ Tasks ]

wabs : WRITING
wabs = MkAuth "Abstract" SATISFIED

rabs : REVIEW
rabs = MkRev "Abstract" WEAKSATIS

wbib : WRITING
wbib = MkAuth "Bib" WEAKSATIS

rbib : REVIEW
rbib = MkRev "Bib" WEAKSATIS

wIntro : WRITING
wIntro = MkAuth "Intro" DENIED

rIntro : REVIEW
rIntro = MkRev "Intro" DENIED

wMeth : WRITING
wMeth = MkAuth "Meth" DENIED

rMeth : REVIEW
rMeth = MkRev "Meth" DENIED

wRes : WRITING
wRes = MkAuth "Res" DENIED

rRes : REVIEW
rRes = MkRev "Res" DENIED

wDis : WRITING
wDis = MkAuth "Dis" DENIED

rDis : REVIEW
rDis = MkRev "Dis" DENIED

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

paperPlan : GModel
paperPlan = emptyModel
 \= paper
 \= abst  \= wabs   \= rabs    \= bib   \= wbib   \= rbib
 \= intr  \= wIntro \= rIntro  \= meth  \= wMeth  \= rMeth
 \= res   \= wRes   \= rRes    \= disc  \= wDis   \= rDis

 \= (paper &= abst)  \= (wabs  ==> abst)  \= (rabs  ==> abst)
 \= (paper &= bib)   \= (wbib  ==> bib)   \= (rbib  ==> bib)
 \= (paper &= intr)  \= (wIntro ==> intr) \= (rIntro ==> intr)
 \= (paper &= meth)  \= (wMeth ==> meth)  \= (rMeth ==> meth)
 \= (paper &= res)   \= (wRes  ==> res)   \= (rRes  ==> res)
 \= (paper &= disc)  \= (wDis  ==> disc)  \= (rDis  ==> disc)

 -- -------------------------------------------------------------------- [ Test ]
export
runTest : IO ()
runTest = do
    putStrLn $ prettyModel paperPlan

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl