text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Module      : XML.Parser
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
--
-- A DOM-based XML parser.
-- --------------------------------------------------------------------- [ EOH ]
module XML.Parser

import public Text.Lexer
import public Text.Parser

import public Commons.Text.Lexer.Run
import public Commons.Text.Parser.Support
import public Commons.Text.Parser.Run

import XML.Lexer
import XML.DOM

%access private
%default total

-- --------------------------------------------------------------- [ Utilities ]

public export
Parser : (a : Type) -> Type
Parser = Rule Token

ParserE : (a : Type) -> Type
ParserE = RuleEmpty Token

eoi : RuleEmpty Token ()
eoi = eoi isEOI

  where
    isEOI : Token -> Bool
    isEOI EndInput = True
    isEOI _ = False

struct : String -> Parser ()
struct str =
  match ("Expected Symbol '" ++ str ++ "'")
        ()
        (Struct str)

isWord : String -> Parser ()
isWord str =
  match ("Expected Symbol '" ++ str ++ "'")
        ()
        (Word str)

isText : String -> Parser ()
isText str =
  match ("Expected Text '" ++ str ++ "'")
        ()
        (Text str)

isLit : String -> Parser ()
isLit str =
  match ("Expected Lit '" ++ str ++ "'")
        ()
        (StringLit ("\"" ++ str ++ "\""))

isSymbol : String -> Parser ()
isSymbol str =
  match ("Expected Symbol '" ++ str ++ "'")
        ()
        (Symbol str)

entity : Parser String
entity = terminalF "Expected entity"
                   (\x => case tok x of
                            (Entity s) => Just s
                            _          => Nothing)

symbol : Parser String
symbol = terminalF "Expected symbol"
                 (\x => case tok x of
                          (Symbol s) => Just s
                          _          => Nothing)

word : Parser String
word = terminalF "Expected word"
                 (\x => case tok x of
                          (Word s) => Just s
                          _        => Nothing)

textStr : Parser String
textStr = terminalF "Expected text"
                 (\x => case tok x of
                          (Text s) => Just s
                          _        => Nothing)

commentStr : Parser String
commentStr = terminalF "Expected comment"
                    (\x => case tok x of
                            (Comment s) => Just s
                            _           => Nothing)

cdataStr : Parser String
cdataStr = terminalF "Expected doc"
                  (\x => case tok x of
                           (CData s) =>
                             let s'  = substr 9 (length s) s in
                             let s'' = substr 3 (length s') (reverse s')
                             in Just (reverse s'')

                           _         => Nothing)

strLit : Parser String
strLit = terminalF "Expected string literal"
             (\x => case tok x of
                         StringLit s => Just (fst $ span (not . (==) '"') s)
                         _ => Nothing)

kvpair : Parser a -> Parser b -> Parser (a, b)
kvpair key value = do
    k <- key
    isSymbol "="
    v <- value
    pure (k,v)

kvpair' : String -> Parser b -> Parser b
kvpair' key value = do
    isWord key
    isSymbol "="
    v <- value
    pure v

angles : Parser a -> Parser a
angles = between (struct "<") (struct ">")

-- ------------------------------------------------------------------- [ Utils ]

qname : Parser $ Document QNAME
qname = do
    pre <- optional $ (word <* isSymbol ":")
    name <- word
    pure (mkQName name Nothing pre)

attr : Parser (Document QNAME, String)
attr = do
  res <- kvpair qname strLit
  pure (fst res, snd res)

elemStart : Parser (Document QNAME, Document QNAME, (List (Document QNAME, String)))
elemStart = do
  struct "<"
  qn <- qname
  ns <- optional $ kvpair' "xmlns" strLit
  as <- optional $ some attr
  pure (qn, setNameSpace ns qn, fromMaybe Nil as)

elemEnd : Document QNAME -> Parser ()
elemEnd n = angles (struct "/" *> isValid)
  where
    isValid : Parser ()
    isValid = do
       seen <- qname
       if (assert_total $ eqDoc n seen)
         then pure ()
         else fail "Malformed"

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

export
comment : Parser $ Document COMMENT
comment = map mkComment commentStr

export
cdata : Parser (Document CDATA)
cdata = map mkCData cdataStr

text : Parser (Document TEXT)
text = map (\xs => mkText (concat xs)) $ some text'
   where
     text' : Parser String
     text' =  entity
          <|> symbol
          <|> word
          <|> textStr

export
instruction : Parser $ Document INSTRUCTION
instruction = do
  struct "<"
  isSymbol "?"
  t <- word
  d <- some (kvpair word strLit) -- @TODO make proper URL parser
  isSymbol "?"
  struct ">"
  pure (mkInstruction t d)

export
empty : Parser (Document ELEMENT)
empty = do
  start <- elemStart
  struct "/"
  struct ">"
  pure (mkElement (fst $ snd start) (snd $ snd start) Nil)

private
buildNodeList : List (ty ** prf : ValidNode ty ** Document ty)
             -> (ts ** prfs ** NodeList ts prfs)
buildNodeList [] = ([] ** [] ** [])
buildNodeList ((ty ** prf ** node) :: xs) =
    let (ts ** prfs ** nodes) = buildNodeList xs
     in (ty :: ts ** prf :: prfs ** node :: nodes)

mutual

  export covering
  node : Parser $ (ty ** prf : ValidNode ty ** Document ty)
  node = map (\n => (COMMENT     ** ValidDoc   ** n)) comment
     <|> map (\n => (CDATA       ** ValidCData ** n)) cdata
     <|> map (\n => (INSTRUCTION ** ValidInstr ** n)) instruction
     <|> map (\n => (ELEMENT     ** ValidElem  ** n)) empty
     <|> map (\n => (ELEMENT     ** ValidElem  ** n)) element
     <|> map (\n => (TEXT        ** ValidText  ** n)) text

  covering
  element : Parser (Document ELEMENT)
  element = do
    start <- elemStart
    let qn = (fst $ snd start)
    let as = (snd $ snd start)
    struct ">"
    ns <- many node
    elemEnd (fst start)
    let nodes = buildNodeList ns
    pure (mkElement qn as (snd $ snd nodes))

%default covering

isStandalone : Parser Bool
isStandalone = (isLit "yes" <|> isLit "true") *> pure True

notStandalone : Parser Bool
notStandalone = (isLit "false" <|> isLit "no") *> pure False

export
xmlinfo : Parser (Document INFO)
xmlinfo = do
  struct "<"
  isSymbol "?"
  isWord "xml"
  vers  <- kvpair' "version" strLit
  enc   <- option "UTF-8" $ kvpair' ("encoding")   strLit
  alone <- option True    $ kvpair' ("standalone") (isStandalone <|> notStandalone)
  isSymbol "?"
  struct ">"
  pure (mkXMLInfo vers enc alone)

pubident : Parser (Document IDENT)
pubident = do
  isWord "PUBLIC"
  loc <- strLit
  loc' <- strLit
  pure (mkPublicID loc loc')

sysident : Parser (Document IDENT)
sysident = map mkSystemID (isWord "SYSTEM" *> strLit)

ident : Parser $ Document IDENT
ident = pubident <|> sysident

export
doctype : Parser (Document DOCTYPE)
doctype = do
  struct "<"
  isSymbol "!"
  isWord "DOCTYPE"
  v <- word
  id <- optional ident
  struct ">"
  pure (mkDocType v id)

xmlSnippet : Parser $ Document ELEMENT
xmlSnippet = (element <|> empty)

export
parseXMLSnippet : (str : String) -> Either (Run.ParseError Token) (Document ELEMENT)
parseXMLSnippet = parseString XMLLexer xmlSnippet

export
xmldoc : Parser $ Document DOCUMENT
xmldoc = do
    info  <- xmlinfo
    dtype <- optional doctype
    is    <- many instruction
    doc   <- optional comment
    root  <- element -- Add check if docttype exists for name of root element
    pure $ mkDocument info dtype is doc root

export
parseXMLDoc : (doc : String)
           -> (Either (Run.ParseError Token) (Document DOCUMENT))
parseXMLDoc = parseString XMLLexer xmldoc

export
parseXMLDocFile : (fname : String)
               -> IO (Either (Run.ParseError Token) (Document DOCUMENT))
parseXMLDocFile = parseFile XMLLexer xmldoc

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

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
module SumsAndProducts

import public Category
import public Isomorphism
import public Universality

%default total

TypeOperator : Category -> Type
TypeOperator cat = Object cat -> Object cat -> Object cat

IsUnitOf : {cat : Category} -> TypeOperator cat -> Object cat -> Type
IsUnitOf {cat} op u = (a : Object cat) ->
    (Isomorphic (op u a) a, Isomorphic (op a u) a)

TypeOperatorIsAssociative : {cat : Category} -> (op : TypeOperator cat) -> Type
TypeOperatorIsAssociative {cat} op = (a, b, c : Object cat) ->
    Isomorphic (op a (op b c)) (op (op a b) c)

IsMonoid : {cat : Category} -> TypeOperator cat -> Object cat -> Type
IsMonoid op u = (TypeOperatorIsAssociative op, IsUnitOf op u)

public export
ProjectionsFrom : {cat : Category} -> (source, target, target' : Object cat) ->
  Type
ProjectionsFrom {cat} source target target' =
  (Morphism cat source target, Morphism cat source target')

public export
InjectionsTo : {cat : Category} -> (target, source, source' : Object cat) ->
  Type
InjectionsTo {cat} target source source' =
  (Morphism cat source target, Morphism cat source' target)

public export
CandidateProduct : {cat : Category} -> (a, b : Object cat) -> Type
CandidateProduct {cat} a b = (c : Object cat ** ProjectionsFrom c a b)

public export
CandidateCoproduct : {cat : Category} -> (a, b : Object cat) -> Type
CandidateCoproduct {cat} a b = (c : Object cat ** InjectionsTo c a b)

public export
IsProduct : {cat : Category} -> (a, b : Object cat) ->
  CandidateProduct {cat} a b -> Type
IsProduct {cat} a b c =
  (c' : CandidateProduct a b) ->
    (m : Morphism cat (fst c') (fst c) **
     IsUniqueMorphismWithProperty
       (\m' =>
         ((fst (snd c)) .* m = (fst (snd c')),
          (snd (snd c)) .* m = (snd (snd c')))) m)

public export
IsCoproduct : {cat : Category} -> (a, b : Object cat) ->
  CandidateCoproduct {cat} a b -> Type
IsCoproduct {cat} a b c =
  (c' : CandidateCoproduct a b) ->
    (m : Morphism cat (fst c) (fst c') **
     IsUniqueMorphismWithProperty
       (\m' =>
         (m .* (fst (snd c)) = (fst (snd c')),
          m .* (snd (snd c)) = (snd (snd c')))) m)

public export
Product : {cat : Category} -> (a, b : Object cat) -> Type
Product a b = DPair (CandidateProduct a b) (IsProduct a b)

public export
candidateProduct : {cat : Category} -> {a, b : Object cat} ->
  Product {cat} a b -> CandidateProduct {cat} a b
candidateProduct {cat} prod = fst prod

public export
productObject : {cat : Category} -> {a, b : Object cat} ->
  Product {cat} a b -> Object cat
productObject {cat} prod = fst (candidateProduct prod)

public export
productProjections : {cat : Category} -> {a, b : Object cat} ->
  (prod : Product {cat} a b) ->
  ProjectionsFrom {cat} (productObject {cat} {a} {b} prod) a b
productProjections {cat} {a} {b} prod = snd (candidateProduct {a} {b} prod)

public export
productProperty : {cat : Category} -> {a, b : Object cat} ->
  (prod : Product {cat} a b) ->
  IsProduct {cat} a b (candidateProduct {cat} {a} {b} prod)
productProperty {cat} prod = snd prod

public export
Coproduct : {cat : Category} -> (a, b : Object cat) -> Type
Coproduct a b = DPair (CandidateCoproduct a b) (IsCoproduct a b)

public export
candidateCoproduct : {cat : Category} -> {a, b : Object cat} ->
  Coproduct {cat} a b -> CandidateCoproduct {cat} a b
candidateCoproduct {cat} prod = fst prod

public export
coproductObject : {cat : Category} -> {a, b : Object cat} ->
  Coproduct {cat} a b -> Object cat
coproductObject {cat} coprod = fst (candidateCoproduct coprod)

public export
coproductProperty : {cat : Category} -> {a, b : Object cat} ->
  (coprod : Coproduct {cat} a b) ->
  IsCoproduct {cat} a b (candidateCoproduct {cat} {a} {b} coprod)
coproductProperty {cat} coprod = snd coprod

public export
coproductInjections : {cat : Category} -> {a, b : Object cat} ->
  (coprod : Coproduct {cat} a b) ->
  InjectionsTo {cat} (coproductObject {cat} {a} {b} coprod) a b
coproductInjections {cat} {a} {b} coprod =
  snd (candidateCoproduct {a} {b} coprod)

public export
HasAllProducts : Category -> Type
HasAllProducts cat = (a, b : Object cat) -> Product a b

public export
HasAllCoproducts : Category -> Type
HasAllCoproducts cat = (a, b : Object cat) -> Coproduct a b

public export
morphismProduct : {c : Category} ->
  {a, b, b' : Object c} ->
  (prodb : Product {cat=c} b b') ->
  (m : Morphism c a b) -> (m' : Morphism c a b') ->
  Morphism c a (productObject {cat=c} {a=b} {b=b'} prodb)
morphismProduct prodb {a} {b} m m' = fst (productProperty prodb (a ** (m, m')))

public export
morphismCoproduct : {c : Category} ->
  {a, a', b : Object c} ->
  (coproda : Coproduct {cat=c} a a') ->
  (m : Morphism c a b) -> (m' : Morphism c a' b) ->
  Morphism c (coproductObject {cat=c} {a=a} {b=a'} coproda) b
morphismCoproduct coproda {a} {b} m m' =
  fst (coproductProperty coproda (b ** (m, m')))

parallelMorphismProduct : {c : Category} ->
  {a, a', b, b' : Object c} ->
  (proda : Product {cat=c} a a') ->
  (prodb : Product {cat=c} b b') ->
  (m : Morphism c a b) -> (m' : Morphism c a' b') ->
  Morphism c
    (productObject {cat=c} {a=a} {b=a'} proda)
    (productObject {cat=c} {a=b} {b=b'} prodb)
parallelMorphismProduct {c} proda prodb m m' =
  let
    projFromA = productProjections proda
    leftProj = m .* (fst projFromA)
    rightProj = m' .* (snd projFromA)
  in
  morphismProduct prodb leftProj rightProj

parallelMorphismCoproduct : {c : Category} ->
  {a, a', b, b' : Object c} ->
  (coproda : Coproduct {cat=c} a a') ->
  (coprodb : Coproduct {cat=c} b b') ->
  (m : Morphism c a b) -> (m' : Morphism c a' b') ->
  Morphism c
    (coproductObject {cat=c} {a=a} {b=a'} coproda)
    (coproductObject {cat=c} {a=b} {b=b'} coprodb)
parallelMorphismCoproduct {c} coproda coprodb m m' =
  let
    injToB = coproductInjections coprodb
    leftInj = (fst injToB) .* m
    rightInj = (snd injToB) .* m'
  in
  morphismCoproduct coproda leftInj rightInj

public export
record CartesianClosedCategory where
  CCC_cat : Category
  CCC_initial : Object CCC_cat
  CC_is_initial : IsInitial {cat=CCC_cat} CCC_initial
  CCC_terminal : Object CCC_cat
  CCC_is_terminal : IsTerminal {cat=CCC_cat} CCC_terminal
  CCC_has_all_products : HasAllProducts CCC_cat
  CCC_has_all_sums : HasAllCoproducts CCC_cat

public export
CCC_object : (ccc : CartesianClosedCategory) -> Type
CCC_object ccc = Object (CCC_cat ccc)

public export
CCC_morphism : {ccc : CartesianClosedCategory} ->
  CCC_object ccc -> CCC_object ccc -> Type
CCC_morphism {ccc} a b = Morphism (CCC_cat ccc) a b

public export
CCC_id : {ccc : CartesianClosedCategory} -> (a : CCC_object ccc) ->
  CCC_morphism {ccc} a a
CCC_id {ccc} a = Identity (CCC_cat ccc) a

public export
CCC_product : {ccc : CartesianClosedCategory} -> (a, b : CCC_object ccc) ->
  CCC_object ccc
CCC_product {ccc} a b = fst (fst (CCC_has_all_products ccc a b))

public export
CCC_sum : {ccc : CartesianClosedCategory} -> (a, b : CCC_object ccc) ->
  CCC_object ccc
CCC_sum {ccc} a b = fst (fst (CCC_has_all_sums ccc a b))

public export
CCC_morphism_product : {ccc : CartesianClosedCategory} ->
  {a, b, b' : CCC_object ccc} ->
  CCC_morphism {ccc} a b -> CCC_morphism {ccc} a b' ->
  CCC_morphism {ccc} a (CCC_product {ccc} b b')
CCC_morphism_product {ccc} {b} {b'} m m' =
  morphismProduct (CCC_has_all_products ccc b b') m m'

public export
CCC_morphism_sum : {ccc : CartesianClosedCategory} ->
  {a, a', b : CCC_object ccc} ->
  CCC_morphism {ccc} a b -> CCC_morphism {ccc} a' b ->
  CCC_morphism {ccc} (CCC_sum {ccc} a a') b
CCC_morphism_sum {ccc} {a} {a'} m m' =
  morphismCoproduct (CCC_has_all_sums ccc a a') m m'

public export
CCC_first : {ccc : CartesianClosedCategory} -> (a, b : CCC_object ccc) ->
  CCC_morphism {ccc} (CCC_product {ccc} a b) a
CCC_first a b = fst (productProjections (CCC_has_all_products ccc a b))

public export
CCC_second : {ccc : CartesianClosedCategory} -> (a, b : CCC_object ccc) ->
  CCC_morphism {ccc} (CCC_product {ccc} a b) b
CCC_second a b = snd (productProjections (CCC_has_all_products ccc a b))

public export
CCC_left : {ccc : CartesianClosedCategory} -> (a, b : CCC_object ccc) ->
  CCC_morphism {ccc} a (CCC_sum {ccc} a b)
CCC_left a b = fst (coproductInjections (CCC_has_all_sums ccc a b))

public export
CCC_right : {ccc : CartesianClosedCategory} -> (a, b : CCC_object ccc) ->
  CCC_morphism {ccc} b (CCC_sum {ccc} a b)
CCC_right a b = snd (coproductInjections (CCC_has_all_sums ccc a b))

public export
CCC_parallel_morphism_product : {ccc : CartesianClosedCategory} ->
  {a, a', b, b' : CCC_object ccc} ->
  CCC_morphism {ccc} a b -> CCC_morphism {ccc} a' b' ->
  CCC_morphism {ccc} (CCC_product {ccc} a a') (CCC_product {ccc} b b')
CCC_parallel_morphism_product {ccc} {a} {a'} {b} {b'} m m' =
  parallelMorphismProduct
    (CCC_has_all_products ccc a a') (CCC_has_all_products ccc b b') m m'

public export
CCC_parallel_morphism_sum : {ccc : CartesianClosedCategory} ->
  {a, a', b, b' : CCC_object ccc} ->
  CCC_morphism {ccc} a b -> CCC_morphism {ccc} a' b' ->
  CCC_morphism {ccc} (CCC_sum {ccc} a a') (CCC_sum {ccc} b b')
CCC_parallel_morphism_sum {ccc} {a} {a'} {b} {b'} m m' =
  parallelMorphismCoproduct
    (CCC_has_all_sums ccc a a') (CCC_has_all_sums ccc b b') m m'

ext: idr

max_stars_repo_name: rokopt/dao-fp-exercises

max_issues_repo_name: rokopt/dao-fp-exercises

max_forks_repo_name: rokopt/dao-fp-exercises


text:
> module EscardoOliva.SelectionFunction

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

> ||| Selection function
> J : Type -> Type -> Type
> J R X = (X -> R) -> X

* Selection functions for quantifiers

> |||
> partial
> argsup : {X : Type} -> (xs : List X) -> J Int X
> argsup (x :: Nil) p = x
> argsup (x :: x' :: xs) p = if p x < p x' then argsup (x' :: xs) p else argsup (x :: xs) p

> |||
> partial
> arginf : {X : Type} -> (xs : List X) -> J Int X
> arginf xs p = argsup xs (\ x => - p x)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
||| Copyright 2016 Google Inc.
|||
||| Licensed under the Apache License, Version 2.0 (the "License");
||| you may not use this file except in compliance with the License.
||| You may obtain a copy of the License at
|||
|||     http://www.apache.org/licenses/LICENSE-2.0
|||
||| Unless required by applicable law or agreed to in writing, software
||| distributed under the License is distributed on an "AS IS" BASIS,
||| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
||| See the License for the specific language governing permissions and
||| limitations under the License.
|||
||| A monad for printing with indents.  Used for TextFormat and for implementing
||| Show for MessageDescriptor and other descriptors.

module Protobuf.Printer

import public Control.Monad.State

-- This shouldn't need to be public, but it's hard to export just the
-- Monad implementation of Printer and nothing else.
||| A state monad that stores the string so far, and the current indent.
public export Printer : Type -> Type
Printer = State (Nat, String)

export print : String -> Printer ()
print s = do {
  (indent, buffer) <- get
  put (indent, buffer ++ s)
}

getIndent : Printer Nat
getIndent = do {
  (indent, buffer) <- get
  return indent
}

putIndent : Nat -> Printer ()
putIndent indent' = do {
  (indent, buffer) <- get
  put (indent', buffer)
}

||| Print the current indent.  Typically called at the start of a new line.
export printIndent : Printer ()
printIndent = getIndent >>= (print . makeIndent) where
  makeIndent : Nat -> String
  makeIndent Z     = ""
  makeIndent (S n) = "  " ++ (makeIndent n)

||| Prints the expression in braces
export braces : Printer () -> Printer ()
braces p = do {
  print "{\n"
  indent <- getIndent
  putIndent (indent + 1)
  p
  putIndent indent
  printIndent
  print "}"
}

export runPrinter : Printer () -> String
runPrinter p = snd $ execState p (Z, "")

max_stars_repo_name: google/idris-protobuf

max_issues_repo_name: google/idris-protobuf

max_forks_repo_name: google/idris-protobuf


text:
-- Import the Cairo prelude
import Cairo
import Data.List

-- Define a datatype
record Account where
  constructor MkAccount
  number: Felt
  balance: Felt

-- Read from private input (using inline Cairo)
%foreign
  """
  code:
  func Main_readFromInput(key) -> (result):
      tempvar result
      %{
          from starkware.cairo.common.math_utils import as_int
          val = program_input[ids.key]
          ids.result = as_int(val, PRIME) % PRIME
      %}
      return (result)
  end
  """
readFromInput : Felt -> Felt

-- Creates an account based on an index into the JSON array in `input.json`
createAccount : Felt -> Account
createAccount index = MkAccount number balance
  where number : Felt
        number = readFromInput index
        balance : Felt
        balance = readFromInput (index + 1)

-- List of available accounts (we assume there are 3 accounts)
privateAccounts : List Account
privateAccounts = map createAccount [0,2,4]

-- Define a function which gets a list of accounts and returns the sum of their balances
sumOfBalances : List Account -> Felt
sumOfBalances accounts = sum (map balance accounts)

-- Computes the hash of the account data (no need to pass the pedersen_ptr)
hashOfAccountData : List Account -> Felt
hashOfAccountData accounts = foldl pedersenHash 3 (foldMap (\a => [a.number, a.balance]) accounts)

-- The main entry point:
-- Computes and outputs the hash of the account data
-- together with the sum of the balances
main : Cairo ()
main = do
  output $ hashOfAccountData privateAccounts
  output $ sumOfBalances privateAccounts

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
interface Lalala where
  constructor cons
  x : Int -> Int


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
module XLA.XlaData

public export
data PrimitiveType = PRED | S32 | S64 | U32 | U64 | F32 | F64

export
Cast PrimitiveType Int where
    cast PRED = 1
    cast S32 = 4
    cast S64 = 5
    cast U32 = 8
    cast U64 = 9
    cast F32 = 11
    cast F64 = 12

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module HOAS

data Expr : Type -> Type where
  Val : a -> Expr a
  Op : (a -> b -> c) -> Expr a -> Expr b -> Expr c
  If : Expr Bool -> Expr a -> Expr a -> Expr a
  Lam : (Expr a -> Expr b) -> Expr (a -> b)
  App : Expr (a -> b) -> Expr a -> Expr b
  Fix : Expr ((a -> b) -> (a -> b)) -> Expr (a -> b)

eval : Expr a -> a
eval (Val x) = x
eval (Op f x y) = f (eval x) (eval y)
eval (If p x y) = if (eval p) then (eval x) else (eval y)
eval (Lam f) = \x => eval (f (Val x))
eval (App f x) = (eval f) (eval x)
eval (Fix f) = \x => loop f x
  where
    loop : Expr ((a -> b) -> (a -> b)) -> a -> b
    loop f a = (eval f) (loop f) a

example : Expr (Int -> Int)
example = Fix (Lam (\f => (Lam (\x =>
                    If (Op (==) x (Val 0))
                      (Val 1)
                      (Op (*) x (App f (Op (-) x (Val 1))))))))

test : Int
test = eval example 5

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
This is some documentation.

More documentation.

> module Main
>
> data Cat = Cas | Luna | Sherlock
>
> f : (cat: Cat) -> String
>
> getName : (cat: Cat) -> String
> getName Cas = "Cas"
> getName Luna = "Luna"

An intermission.

> plusTwo : (n: Nat) -> Nat
> plusTwo n = plus 2 n
>
> g : (n: Nat) -> (b: Bool) -> String
> g n b = ?g_rhs
>
> n : Nat
> n = ?n_rhs

Some closing thoughts.


text:
module RFC.Handshake

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

import System.Protocol

import RFC.Utils

data TCPMsg = Syn | SynAck | Ack

instance Default TCPMsg where
  default = Syn

data MsgTy = SYN | SYNACK | ACK

data TCPMsg' : MsgTy -> Type where
  Syn' : TCPMsg' SYN
  Ack' : TCPMsg' ACK
  Synack' :  TCPMsg' SYNACK

instance Default (TCPMsg' SYN) where
  default = Syn'

total
handshake' : Protocol ['Alice, 'Bob] ()
handshake' = do
  'Alice ==> 'Bob   | (TCPMsg, Nat)
  'Bob   ==> 'Alice | (TCPMsg, Nat, Nat)
  'Alice ==> 'Bob   | (TCPMsg, Nat)
  Done

total
handshake'' : Protocol ['Alice, 'Bob] ()
handshake'' = do
  (_, x) <- 'Alice ==> 'Bob | (TCPMsg' SYN, Nat)
  (_, y, _) <- 'Bob ==> 'Alice | (TCPMsg' SYNACK, Nat, (x' ** x' = S x))
  'Alice ==> 'Bob | (TCPMsg' ACK, (y' ** y' = S y))
  Done

total
handshake : Protocol ['Alice, 'Bob] ()
handshake = do
  (_, x) <- 'Alice ==> 'Bob | (TCPMsg, Nat)
  (_, y, _) <- 'Bob ==> 'Alice | (TCPMsg, Nat, (x' ** x' = S x))
  'Alice ==> 'Bob | (TCPMsg, (y' ** y' = S y))
  Done

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module RecursionSchemes

data Fix : (f : Type -> Type) -> Type where
  Fx : (f (Fix f)) -> Fix f

data ListF : Type -> Type -> Type where
  Nil : ListF a f
  Cons : a -> f -> ListF a f

Functor (ListF a) where
  map f [] = []
  map f (Cons x xs) = Cons x (f xs)

List' : Type -> Type
List' a = Fix (ListF a)

nil : List' a
nil = Fx Nil

(::) : a -> List' a -> List' a
(::) x xs = Fx (Cons x xs)

cata : Functor f => (f a -> a) -> Fix f -> a
cata alg (Fx f) = (alg . map (cata alg)) f

ana : Functor f => (a -> f a) -> a -> Fix f
ana f a = (Fx . map (ana f) . f) a

hylo : Functor f => (f b -> b) -> (a -> f a) -> a -> b
hylo f g a = (cata f . ana g) a

-- Catamorphism examples
count : List' a -> Int
count xs = cata countF xs
  where
    countF : ListF a Int -> Int
    countF [] = 0
    countF (Cons _ c) = 1 + c

sum : List' Int -> Int
sum xs = cata sumF xs
  where
    sumF : ListF Int Int -> Int
    sumF [] = 0
    sumF (Cons x c) = x + c

example : List' Int
example = 1 :: 2 :: 3 :: 4 :: 5 :: nil

testCount : Int
testCount = count example

testSum : Int
testSum = sum example

-- Anamorphism examples
repeat : Int -> List' Int
repeat n = ana countF n
  where
    countF : Int -> ListF Int Int
    countF n = if n <= 0 then Nil else Cons n (n - 1)

testRepeat : Int
testRepeat = sum (repeat 5)


text:
--    Copyright 2017, the blau.io contributors
--
--    Licensed under the Apache License, Version 2.0 (the "License");
--    you may not use this file except in compliance with the License.
--    You may obtain a copy of the License at
--
--        http://www.apache.org/licenses/LICENSE-2.0
--
--    Unless required by applicable law or agreed to in writing, software
--    distributed under the License is distributed on an "AS IS" BASIS,
--    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--    See the License for the specific language governing permissions and
--    limitations under the License.

module API.WebGL.Context

import API.WebGL.Buffer
import API.WebGL.Shader
import API.WebGL.Program
import IdrisScript
import IdrisScript.Arrays

%access public export
%default total

||| The WebGLRenderingContext represents the API allowing OpenGL ES 2.0 style
||| rendering into the canvas element.
|||
||| The original specification can be found at
||| https://www.khronos.org/registry/webgl/specs/latest/1.0/#WebGLRenderingContextBase
record WebGLRenderingContextBase where
  constructor New
  ||| A reference to the canvas element which created this context.
  canvas              : Ptr
  ||| The actual width of the drawing buffer. May be different from the width
  ||| attribute of the HTMLCanvasElement if the implementation is unable to
  ||| satisfy the requested widthor height.
  drawingBufferWidth  : Int
  ||| The actual height of the drawing buffer. May be different from the height
  ||| attribute of the HTMLCanvasElement if the implementation is unable to
  ||| satisfy the requested width or height.
  drawingBufferHeight : Int
  ||| A non standard field for easier JS integration
  self                : Ptr

-- ClearBufferMask
COLOR_BUFFER_BIT   : Int
COLOR_BUFFER_BIT   = 0x00004000

DEPTH_BUFFER_BIT   : Int
DEPTH_BUFFER_BIT   = 0x00000100

STENCIL_BUFFER_BIT : Int
STENCIL_BUFFER_BIT = 0x00000400

-- Begin Mode
TRIANGLES : Int
TRIANGLES = 0x0004

attachShader : WebGLRenderingContextBase -> (program : WebGLProgram) ->
               (shader : WebGLShader) -> JS_IO ()
attachShader ctx (New programRef) (New shaderRef) =
  jscall "%0.attachShader(%1, %2)" (JSRef -> JSRef -> JSRef -> JS_IO ())
  (self ctx) programRef shaderRef

bindBuffer : WebGLRenderingContextBase -> (target : Int) ->
             (buffer : WebGLBuffer) -> JS_IO ()
bindBuffer ctx target (New ref) = jscall "%0.bindBuffer(%1, %2)"
                                  (JSRef -> Int -> JSRef -> JS_IO ())
                                  (self ctx) target ref

-- TODO: proper types for all arguments
bufferData : WebGLRenderingContextBase -> (target : Int) ->
             (srcData : List Double) -> (usage : Int) -> JS_IO ()
bufferData ctx target srcData usage = jscall "%0.bufferData(%1, %2, %3)"
  (JSRef -> Int -> JSRef -> Int -> JS_IO ())
  (API.WebGL.Context.WebGLRenderingContextBase.self ctx)
  target (IdrisScript.unpack !(toJSArray {to=JSNumber} srcData)) usage

compileShader : WebGLRenderingContextBase -> (shader : WebGLShader) -> JS_IO ()
compileShader ctx (New ref) = jscall "%0.compileShader(%1)"
                              (JSRef -> JSRef -> JS_IO ()) (self ctx) ref

||| clears a buffer
-- TODO: Proper type for buffer
clear : WebGLRenderingContextBase -> (buffer : Int) -> JS_IO ()
clear ctx = jscall "%0.clear(%1)" (JSRef -> Int -> JS_IO ()) $ self ctx

||| clearColor sets the clear value of the color buffer.
-- TODO: Proper Type for red, green, blue, alpha
clearColor : WebGLRenderingContextBase -> (red : Double) -> (green : Double) ->
             (blue : Double) -> (alpha : Double) -> JS_IO ()
clearColor ctx = jscall "%0.clearColor(%1, %2, %3, %4)"
                 (JSRef -> Double -> Double -> Double -> Double -> JS_IO ()) $
                 self ctx

createBuffer : WebGLRenderingContextBase -> JS_IO WebGLBuffer
createBuffer ctx = map API.WebGL.Buffer.New bufferRef where
  bufferRef : JS_IO JSRef
  bufferRef = jscall "%0.createBuffer()" (JSRef -> JS_IO JSRef) $
              API.WebGL.Context.WebGLRenderingContextBase.self ctx

createProgram : WebGLRenderingContextBase -> JS_IO WebGLProgram
createProgram ctx = map API.WebGL.Program.New programRef where
  programRef : JS_IO JSRef
  programRef = jscall "%0.createProgram()" (JSRef -> JS_IO JSRef) $
               API.WebGL.Context.WebGLRenderingContextBase.self ctx

createShader : WebGLRenderingContextBase -> (type : Int) -> JS_IO WebGLShader
createShader ctx type = map API.WebGL.Shader.New shaderRef where
  shaderRef : JS_IO JSRef
  shaderRef = jscall "%0.createShader(%1)" (JSRef -> Int -> JS_IO JSRef)
              (API.WebGL.Context.WebGLRenderingContextBase.self ctx) type

drawArrays : WebGLRenderingContextBase -> (mode : Int) -> (first : Int) ->
             (count : Int) -> JS_IO ()
drawArrays ctx = jscall "%0.drawArrays(%1, %2, %3)"
                 (JSRef -> Int -> Int -> Int -> JS_IO ()) $ self ctx

enableVertexAttribArray : WebGLRenderingContextBase -> (index : Int) -> JS_IO ()
enableVertexAttribArray ctx = jscall "%0.enableVertexAttribArray(%1)"
                              (JSRef -> Int -> JS_IO ()) (self ctx)

getAttribLocation : WebGLRenderingContextBase -> (program : WebGLProgram) ->
                    (name : String) -> JS_IO $ Maybe Int
getAttribLocation ctx (New ref) name = case !(IdrisScript.pack !attribLocation) of
    (JSNumber ** n) => pure $ Just $ fromJS n
    _               => pure Nothing
  where
    attribLocation : JS_IO JSRef
    attribLocation = jscall "%0.getAttribLocation(%1, %2)"
                     (JSRef -> JSRef -> String -> JS_IO JSRef)
                     (self ctx) ref name

linkProgram : WebGLRenderingContextBase -> (program : WebGLProgram) -> JS_IO ()
linkProgram ctx (New ref) = jscall "%0.linkProgram(%1)"
                            (JSRef -> JSRef -> JS_IO ()) (self ctx) ref

useProgram : WebGLRenderingContextBase -> (program : WebGLProgram) -> JS_IO ()
useProgram ctx (New ref) = jscall "%0.useProgram(%1)"
                           (JSRef -> JSRef -> JS_IO ()) (self ctx) ref

shaderSource : WebGLRenderingContextBase -> (shader : WebGLShader) ->
               (source : String) -> JS_IO ()
shaderSource ctx (New ref) = jscall "%0.shaderSource(%1, %2)"
                             (JSRef -> JSRef -> String -> JS_IO ())
                             (self ctx) ref

vertexAttribPointer : WebGLRenderingContextBase -> (index : Int) ->
                      (size : Int) -> (type : Int) -> (normalized : Bool) ->
                      (stride : Int) -> (offset : Int) -> JS_IO ()
vertexAttribPointer ctx index size type normalized =
  jscall "%0.vertexAttribPointer(%1, %2, %3, %4, %5, %6)"
  (JSRef -> Int -> Int -> Int -> JSRef -> Int -> Int -> JS_IO ())
  (API.WebGL.Context.WebGLRenderingContextBase.self ctx) index size type
  (IdrisScript.unpack (toJS {to=JSBoolean} normalized))

WebGLRenderingContext : Type
WebGLRenderingContext = WebGLRenderingContextBase

||| webGlRenderingContextFromPointer is a helper function for easily creating
||| WebGLRenderingContexts from JavaScript references.
webGlRenderingContextFromPointer : JSRef -> JS_IO $ Maybe WebGLRenderingContext
webGlRenderingContextFromPointer ref = let
    canvas   = jscall "%0.canvas"              (JSRef -> JS_IO JSRef) ref
    dbWidth  = jscall "%0.drawingBufferWidth"  (JSRef -> JS_IO JSRef) ref
    dbHeight = jscall "%0.drawingBufferHeight" (JSRef -> JS_IO JSRef) ref
  in
    case !(IdrisScript.pack !dbWidth) of
      (JSNumber ** w) => case !(IdrisScript.pack !dbHeight) of
        (JSNumber ** h) => map Just $ New <$> canvas <*>
                                              pure (fromJS w) <*>
                                              pure (fromJS h) <*>
                                              pure ref
        _               => pure Nothing
      _               => pure Nothing

max_stars_repo_name: blau-io/idris-webgl

max_issues_repo_name: blau-io/idris-webgl

max_forks_repo_name: blau-io/idris-webgl


text:
import Data.Vect

||| Test if the type of local variables is correctly reported

-- Not meant to be called, just typechecked
partial
f : Nat -> Int -> Bool -> () -> z
f a b c d =

    -- Let with pattern match
    let (S a') = a

        -- Let without signature
        b' = b

        -- Let with signature
        c' : Bool
        c' = c

        -- In the type signature of the Let
        v1 : Vect a Nat
        v1 = ?vect1

    -- After the `in`
    -- It's good to include them all to test that they work regardless
    -- of how they were bound
    in ?result a' b' c' d' v1 v2
  where
    -- Where
    d' : ()
    d' = d

    -- In the type signature of the Where
    v2 : Vect x Nat
    v2 = ?vect2


text:
f : {default 1 0 x : Nat} -> Nat
f = 0

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Language.LSP.Message.Definition

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition
public export
record DefinitionClientCapabilities where
  constructor MkDefinitionClientCapabilities
  dynamicRegistration : Maybe Bool
  linkSupport         : Maybe Bool
%runElab deriveJSON defaultOpts `{{DefinitionClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition
public export
record DefinitionOptions where
  constructor MkDefinitionOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{{DefinitionOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition
public export
record DefinitionRegistrationOptions where
  constructor MkDefinitionRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
%runElab deriveJSON defaultOpts `{{DefinitionRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition
public export
record DefinitionParams where
  constructor MkDefinitionParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
  position           : Position
%runElab deriveJSON defaultOpts `{{DefinitionParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition
public export
record TypeDefinitionClientCapabilities where
  constructor MkTypeDefinitionClientCapabilities
  dynamicRegistration : Maybe Bool
  linkSupport         : Maybe Bool
%runElab deriveJSON defaultOpts `{{TypeDefinitionClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition
public export
record TypeDefinitionOptions where
  constructor MkTypeDefinitionOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{{TypeDefinitionOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition
public export
record TypeDefinitionRegistrationOptions where
  constructor MkTypeDefinitionRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
  id               : Maybe String
%runElab deriveJSON defaultOpts `{{TypeDefinitionRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition
public export
record TypeDefinitionParams where
  constructor MkTypeDefinitionParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
  position           : Position
%runElab deriveJSON defaultOpts `{{TypeDefinitionParams}}


text:
module Lambdapants.Command.Parser

import Lambdapants.Command
import Lambdapants.Term
import Lambdapants.Term.Parser
import Lambdapants.Term.Reduction
import Lightyear
import Lightyear.Char
import Lightyear.Strings

symbolArg : Parser String
symbolArg = symbol

termArg : Parser Term
termArg = (char '(' *> appl <* char ')') <|>| map Var symbol

natArg : Parser Nat
natArg = (cast . pack) <$> some (satisfy isDigit)

stratArg : Parser Strategy
stratArg = norm <|> appl where
  norm : Parser Strategy
  norm = string "normal" *> pure Normal
  appl : Parser Strategy
  appl = string "applicative" *> pure Applicative

data ArgT
  = Arg0 Command
  | Arg1 (a -> Command)           (Parser a)
  | Arg2 (a -> b -> Command)      (Parser a) (Parser b)
  | Arg3 (a -> b -> c -> Command) (Parser a) (Parser b) (Parser c)

arity : ArgT -> Nat
arity (Arg0 _      ) = 0
arity (Arg1 _ _    ) = 1
arity (Arg2 _ _ _  ) = 2
arity (Arg3 _ _ _ _) = 3

commands : List (String, (ArgT, String))
commands =
  [ ("q"       , (Arg0 Quit                      , ""))
  , ("quit"    , (Arg0 Quit                      , ""))
  , ("limit"   , (Arg1 Limit natArg              , "<number>"))
  , ("u"       , (Arg1 Unset symbolArg           , "<symbol>"))
  , ("unset"   , (Arg1 Unset symbolArg           , "<symbol>"))
  , ("s"       , (Arg2 Set symbolArg termArg     , "<symbol> <term>"))
  , ("set"     , (Arg2 Set symbolArg termArg     , "<symbol> <term>"))
  , ("w"       , (Arg1 Whatis termArg            , "<term>"))
  , ("whatis"  , (Arg1 Whatis termArg            , "<term>"))
  , ("r"       , (Arg1 Reduce termArg            , "<term>"))
  , ("reduce"  , (Arg1 Reduce termArg            , "<term>"))
  , ("eq"      , (Arg2 Eq termArg termArg        , "<term> <term>"))
  , ("aq"      , (Arg2 AlphaEq termArg termArg   , "<term> <term>"))
  , ("env"     , (Arg0 Env                       , ""))
  , ("eval"    , (Arg1 Eval (opt stratArg)       , "[normal | applicative]"))
  , ("?"       , (Arg0 Help                      , ""))
  , ("h"       , (Arg0 Help                      , ""))
  , ("help"    , (Arg0 Help                      , "")) ]

args : ArgT -> Parser Command
args (Arg0 constr) = do
  spaces
  eof
  pure constr
args (Arg1 constr arg1) = do
  a <- arg1
  spaces
  eof
  pure (constr a)
args (Arg2 constr arg1 arg2) = do
  a <- arg1
  some space
  b <- arg2
  spaces
  eof
  pure (constr a b)
args (Arg3 constr arg1 arg2 arg3) = do
  a <- arg1
  some space
  b <- arg2
  some space
  c <- arg3
  spaces
  eof
  pure (constr a b c)

parseArgs : String -> String -> Either String Command
parseArgs command argstr =
  maybe (Left err) (uncurry compile) (lookup command commands)
where
  compile : ArgT -> String -> Either String Command
  compile argt hint = do
    case parse (args argt) argstr of
         Left _  => Left (if 0 == arity argt
                         then command ++ " is like Chuck Norris. \
                           \It takes no arguments."
                         else "Usage is :" ++ command ++ " " ++ hint)
         right => right
  err : String
  err = "\ESC[0;91mUnrecognized command: " ++ command ++ "\ESC[0m"

export
parseCmd : String -> Either String Command
parseCmd str = do
  case words str of
       (w :: ws) =>
            let args = unwords ws in
                if "!" == w
                   then Right (Shell args)
                   else parseArgs w args
       otherwise => Left "error"

max_stars_repo_name: laserpants/redex-reflex

max_issues_repo_name: laserpants/lambdapants

max_forks_repo_name: laserpants/lambdapants


text:
module X
[


text:
||| Utilities functions for contitionally delaying values.
module Control.Delayed

||| Type-level function for a conditionally infinite type.
public export
inf : Bool -> Type -> Type
inf False t = t
inf True t = Inf t

||| Type-level function for a conditionally lazy type.
public export
lazy : Bool -> Type -> Type
lazy False t = t
lazy True t = Lazy t


text:
module Linear.Random

import Linear.V
import public System.Random

export
{n : _} -> Random a => Random (V n a) where
  randomIO = sequence $ pure $ randomIO
  randomRIO ([], []) = pure []
  randomRIO ((x :: xs), (y :: ys)) = pure $ !(randomRIO (x, y)) :: !(randomRIO (xs, ys))

||| random between 0 and 1
export
rand : HasIO m => Random a => {ns : _} -> m (T ns a)
rand {ns = []} = randomIO
rand {ns = n :: ns} = sequence $ pure $ rand

export
rand_v : HasIO m => Random a => {n : _} -> m (T [n] a)
rand_v = rand {ns = [_]}

export
rand_m : HasIO m => Random a => {n, p : _} -> m (T [n, p] a)
rand_m = rand {ns = [_, _]}

||| random between `low` and `high`
export
uniform : HasIO m => Random a => {ns : _} -> (low : a) -> (high : a) -> m (T ns a)
uniform {ns = []} low high = randomRIO (low, high)
uniform {ns = n :: ns} low high = sequence $ pure $ uniform low high


text:
parameters {n : Nat}
           (a : Int)
  0 func : Bool -> Type
  func True = List Bool
  func False = List Nat

  getType : (b : Bool) -> func b
  getType False = [0,1,2]
  getType True = [True, True, True]

  prf : (b : Bool) -> Int -> func b
  prf b i = let i1 = getType b in ?whut


text:
%builtin Natural Nat

natToInt : Nat -> Integer
natToInt Z = 0
natToInt (S k) = 1 + natToInt k

%builtin NaturalToInteger natToInt


text:
||| http://okmij.org/ftp/Computation/free-monad.html
module Freer

%default total
%access public export

||| Argh, has the same totality problems as free monad!
data FFree : (Type -> Type) -> Type -> Type where
  FPure   : a -> FFree g a
  FImpure : g x -> (x -> FFree g a) -> FFree g a

fmap : (a -> b) -> FFree g a -> FFree g b
fmap f (FPure x)     = FPure (f x)
fmap f (FImpure u q) = FImpure u (fmap f . q)

Functor (FFree g) where
  map f (FPure x)     = FPure (f x)
  map f (FImpure u q) = FImpure u (map f . q)

Applicative (FFree g) where
  pure = FPure
  (FPure f) <*> x = map f x
  (FImpure u q) <*> x = FImpure u ((<*> x) . q)

infixr 5 >=>

(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
f >=> g = (>>= g) . f

Monad (FFree g) where
  (FPure x) >>= f = f x
  (FImpure u f') >>= f = FImpure u (f' >=> f)


text:
module ProofColDivSeqPostulate

import ProofColDivSeqBase

%default total
-- %language ElabReflection
%access export

%hide Language.Reflection.P

--            from ProofColDivSeqBase
-- ########################################
public export
data Limited : CoList Integer -> Type where
  IsLimited00 : (step : Nat ** limitedNStep xs step = True) -> Limited xs
  IsLimited01 : (k : Nat)
    -> Limited $ divSeq (plus (plus k k) k)
      -> Limited $ divSeq (S (plus (plus (plus (plus (plus k k) (plus k k)) (plus k k))
                                         (S (plus (plus (plus k k) (plus k k))(plus k k))))
                                   (S (plus (plus (plus k k) (plus k k)) (plus k k)))))
  IsLimited02 : (l : Nat)
    -> Limited (divSeq (plus (plus (plus l l) (plus l l)) (plus l l)))
      -> Limited (divSeq (S (S (plus (plus (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                                       (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                                 (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                           (S (S (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                                             (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                                       (S (plus (plus (plus l l) l) (plus (plus l l) l)))))))
                                     (S (S (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                                       (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                                 (S (plus (plus (plus l l) l) (plus (plus l l) l))))))))))
  IsLimited03 : (l : Nat)
    -> Limited (divSeq (S (S (S (plus (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))
                                            (S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))))
                                      (S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))))))))
     -> Limited (divSeq (S (S (S (plus (plus (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l)))
                                                         (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                                                   (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                                             (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l)))
                                                                  (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                                                            (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))))
                                       (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l)))
                                                            (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                                                      (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))))))))
  IsLimited04 : (l : Nat)
    -> Limited (divSeq (S (S (S (plus (plus (plus (plus l l) (plus l l))
                                            (S (S (S (plus (plus l l) (plus l l))))))
                                      (S (S (S (plus (plus l l) (plus l l))))))))))
      -> Limited (divSeq (S (S (S (S (plus (plus (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                                             (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                                       (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                                 (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                                                         (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                                                   (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))))))
                                           (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                                                   (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                                             (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))))))))))))
  IsLimited05 : (j : Nat)
    -> Limited (divSeq (plus (plus j j) j))
      -> Limited (divSeq (S (S (plus (plus (plus (plus j j) j) (S (S (plus (plus j j) j))))
                                     (S (S (plus (plus j j) j)))))))
  IsLimited06 : (l : Nat)
    -> Limited (divSeq (plus (plus l l) l))
      -> Limited (divSeq (S (S (S (plus (plus (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l)))
                                              (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l)))))))
                                        (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l)))))))))))
  IsLimited07 : (o : Nat)
    -> Limited (divSeq (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus o o)
                                                                               (plus o o))
                                                                         (plus (plus o o) (plus o o)))
                                                                   (plus (plus (plus o o) (plus o o))
                                                                         (plus (plus o o) (plus o o))))
                                                             (plus (plus (plus (plus o o) (plus o o))
                                                                         (plus (plus o o) (plus o o)))
                                                                   (plus (plus (plus o o) (plus o o))
                                                                         (plus (plus o o) (plus o o)))))
                                                       (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o))))
                                                                                (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o)))))))))))))
                                                 (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o))))
                                                                            (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o)))))))))))))))))))))
      -> Limited (divSeq (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o)
                                                                          (plus (plus o o) o))))
                                                           (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o)
                                                                             (plus (plus o o) o))))))
                                                     (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                              (S (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))))))
                                               (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                             (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))
                                                                       (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))
                                                                 (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                          (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))
                                         (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o)
                                                                             (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))
                                                                 (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                          (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))
                                                           (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o)
                                                                             (plus (plus o o) o))))))))))))))))
  IsLimited08 : (o : Nat)
    -> Limited (divSeq (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) (plus o o))
                                                                         (plus (plus o o) (plus o o)))
                                                                   (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                             (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))))))))))))) (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o))))))))))))))))))))))))
      -> Limited (divSeq (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o)
                                                                          (S (plus (plus o o) o)))
                                                                    (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                              (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                                        (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                    (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                                  (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))
                                                                             (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))))))
                                            (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                             (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))
                                                                 (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                             (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))))))))))))
  IsLimited09 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                         (S (S (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))
                                                   (S (S (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                       (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                 (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))
                                                           (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                          (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))
                                                     (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))))))))
                                               (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))
                                                                       (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))))))))))))))))
  IsLimited10 : (o : Nat)
    -> Limited $ divSeq (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                       (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))
                                 (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))
      -> Limited $ divSeq (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                 (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                           (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                                     (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                               (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o))) (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                                                 (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                          (plus (plus (plus o o) o) (plus (plus o o) o))))))))))
                                         (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                 (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                                           (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                    (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))))
  IsLimited11 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                                                (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))
                                                                               (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o))))
                                                                                (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))))))))))))))))))))
                                                                         (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o))))
                                                                                (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o))))))))))))))))))))))))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                    (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                              (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                          (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                                        (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                    (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                                  (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                             (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))))))
                                            (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                             (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                                                 (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                             (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))))))
  IsLimited12 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                                               (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                                         (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o))))))))))))))))))
                                                                   (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))))))))))))))))))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                       (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                                                 (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))
                                                           (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                          (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))
                                                     (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))))
                                               (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))
                                                                       (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))))))))))
  IsLimited13 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                       (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                 (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                                      (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))
                                           (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                    (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                              (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                          (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                                        (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                                  (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                             (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))))
                                            (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                             (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                                                 (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                             (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))))))))
  IsLimited14 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                 (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))
                                           (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                       (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                                 (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                                           (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                                     (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))))
                                               (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                                                       (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))))))))))
  IsLimited15 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o))))
                                                                                (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))))
                               (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o)
                                                                         (plus o o))
                                                                   (plus (plus o o)
                                                                         (plus o o)))
                                                             (plus (plus (plus o o)
                                                                         (plus o o))
                                                                   (plus (plus o o)
                                                                         (plus o o))))
                                                       (plus (plus (plus (plus o o)
                                                                         (plus o o))
                                                                   (plus (plus o o)
                                                                         (plus o o)))
                                                             (plus (plus (plus o o)
                                                                         (plus o o))
                                                                   (plus (plus o o)
                                                                         (plus o o)))))))))))))))))))))))))))))))))))))
                           (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o)
                                                                   (plus o o))
                                                             (plus (plus o o)
                                                                   (plus o o)))
                                                       (plus (plus (plus o o)
                                                                   (plus o o))
                                                             (plus (plus o o)
                                                                   (plus o o))))
                                                 (plus (plus (plus (plus o o)
                                                                   (plus o o))
                                                             (plus (plus o o)
                                                                   (plus o o)))
                                                       (plus (plus (plus o o)
                                                                   (plus o o))
                                                             (plus (plus o o)
                                                                   (plus o o))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                          (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                    (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))
                                                              (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))
                                                        (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                                (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))))
                                                                                (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))))))))))))
                                                  (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                                (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))))
                                                                             (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))))))))))))))))))))))))))

P : Nat -> Type
P n = Limited $ divSeq (n+n+n)
definiP : (n : Nat) -> P n = Limited $ divSeq (n+n+n)
definiP n = Refl

-- 無限降下法（の変形） Isabelleで証明した
postulate infiniteDescent0 :
  ((n:Nat) -> (Not . P) (S n) -> (m ** (LTE (S m) (S n), (Not . P) m)))
    -> P Z
      -> P n
-- ########################################

--            from ProofColDivSeqMain
-- ########################################
-- ########################################

--            from sub0xxxxx
-- ########################################
-- ########################################


text:
{-
foo
bar
baz
qux
quux
-}

import CIL.FFI
import CIL.FFI.Array
import Data.Vect

ToCharArray : String -> CIL_IO CharArray
ToCharArray =
  invoke (CILInstance "ToCharArray")
         (String -> CIL_IO CharArray)

Split : String -> CharArray -> CIL_IO StringArray
Split =
  invoke (CILInstance "Split")
         (String -> CharArray -> CIL_IO StringArray)

putAll : StringArray -> CIL_IO ()
putAll ss = forEach_ ss putStrLn

main : CIL_IO ()
main = do
  Split "foo,bar baz" !(ToCharArray ", ") >>= putAll
  arrayOf CILTyStr ["qux", "quux"] >>= putAll

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

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module Data.Time.Calendar.Julian

import Data.Time.Calendar.Days
import public Data.Time.Calendar.Types

%default total

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

||| Is this year a leap year according to the proleptic Julian calendar?
isJulianLeapYear : Year -> Bool
isJulianLeapYear y = (y `mod` 4 == 0) && ((y `mod` 400 == 0) || (y `mod` 100 /= 0))

||| Convert to proleptic Julian year and day format.
toJulianYearAndDay : Day -> (Year, DayOfYear)
toJulianYearAndDay (ModifiedJulianDay mjd) =
  let a    = mjd + 678577
      quad = a `div` 1461
      d    = a `mod` 1461
      y    = min (d `div` 365) 3
    in (quad * 4 + y + 1, fromInteger $ d - (y * 365) + 1)

||| Convert from proleptic Julian year and day format.
||| Invalid day numbers will be clipped to the correct range (1 to 365 or 366).
fromJulianYearAndDay : Year -> DayOfYear -> Day
fromJulianYearAndDay year day =
  let y = year - 1
      yd = if isJulianLeapYear year then 366 else 365
      mjd = cast (if day < 1 then 1
            else if day > yd then yd
            else day) + (365 * y) + (y `div` 4) - 678578
    in ModifiedJulianDay mjd

||| Convert from proleptic Julian year and day format.
||| Invalid day numbers will return Nothing
fromJulianYearAndDayValid : Year -> DayOfYear -> Maybe Day
fromJulianYearAndDayValid year day =
  let y = year - 1
      yd = if isJulianLeapYear year then 366 else 365
    in if day < 1 then Nothing
       else if day > yd then Nothing
       else Just $ ModifiedJulianDay $ cast day + (365 * y) + (y `div` 4) - 678578

{-  -- FIXME:
||| Show in proleptic Julian year and day format (yyyy-ddd)
showJulianYearAndDay : Day -> String
showJulianYearAndDay date =
  let (y, d) = toJulianYearAndDay
   in (show4 y) ++ "-" ++ (show3 d)
-}

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


text:
module Effect.Socket

import Effects

import Network.Socket

-- A simple UDP library

||| The internal UDP effect structure
data UDPClient : Effect where
  MakeSocket : UDPClient (Either SocketError ()) () (\res => case res of
                                                               Left err => ()
                                                               Right s => Socket)
  Send : SocketAddress -> Int -> String ->
         UDPClient (Either SocketError ByteLength) Socket (const Socket)
  Close : UDPClient () Socket (const ())

instance Handler UDPClient IO where
  handle () MakeSocket k = do s <- socket AF_INET Datagram 0
                              case s of
                                Left err => k (Left err) ()
                                Right sock => do bind sock Nothing 0
                                                 k (Right ()) sock
  handle s (Send address port msg) k = do res <- (sendTo s address port msg)
                                          k res s
  handle s Close k = do close s
                        k () ()

||| A UDP socket effect.
||| @ resource either `()` or `Socket`, depending on whether the library is initialised
UDP : (resource : Type) -> EFFECT
UDP res = MkEff res UDPClient

||| Initialise a socket to send UDP packets
mksocket : { [UDP ()] ==>
             [UDP (case result of {Left _ => () ; Right _ => Socket})]
           } Eff (Either SocketError ())
mksocket = call MakeSocket

||| Send a message to a given address and port
send : SocketAddress -> Int -> String -> { [UDP Socket] } Eff (Either SocketError ByteLength)
send addr port buf = call (Send addr port buf)

||| Clean up the socket
close : { [UDP Socket] ==> [UDP ()] } Eff ()
close = call Close

max_stars_repo_name: GaloisInc/self-aware-pinball

max_issues_repo_name: GaloisInc/self-aware-pinball

max_forks_repo_name: GaloisInc/self-aware-pinball


text:
module Data.Tree

-- Implementation heavily inspired by Haskell's Data.Tree

%default total
%access public export

mutual
  record Tree a where
    constructor Node
    rootLabel : a
    subForest : Forest a

  Forest : Type -> Type
  Forest a = List (Tree a)

Eq a => Eq (Tree a) where
  (Node rootLabel1 subForest1) == (Node rootLabel2 subForest2) =
    rootLabel1 == rootLabel2 &&
     isSubForestsEqual subForest1 subForest2
      where
        isSubForestsEqual : Forest a -> Forest a -> Bool
        isSubForestsEqual [] [] = True
        isSubForestsEqual [] (y :: ys) = False
        isSubForestsEqual (x :: xs) [] = False
        isSubForestsEqual (x :: xs) (y :: ys) = x == y && isSubForestsEqual xs ys

Functor Tree where
  map func (Node rootLabel subForest) =
    Node (func rootLabel) (mapSubForest subForest)
      where
        mapSubForest : Forest a -> Forest b
        mapSubForest [] = []
        mapSubForest (x :: xs) = map func x :: mapSubForest xs

Show a => Show (Tree a) where
  show (Node rootLabel subForest) =
    "Node " ++ show rootLabel ++ " " ++ showSubForest subForest
      where
        showRestOfSubForest : Forest a -> String
        showRestOfSubForest [] = ""
        showRestOfSubForest (x :: xs) = ", " ++ show x ++ showRestOfSubForest xs

        showSubForest : Forest a -> String
        showSubForest [] = "[]"
        showSubForest (x :: xs) = "[" ++ show x ++ showRestOfSubForest xs ++ "]"

partial
draw : Tree String -> List String
draw (Node x ts0) = lines x ++ drawSubTrees ts0
  where
    shift : String -> String -> List String -> List String
    shift first other xs =
      zipWith (++) (first :: take (length xs `minus` 1) (repeat other)) xs

    drawSubTrees : Forest String -> List String
    drawSubTrees [] = []
    drawSubTrees [t] =
        "|" :: shift "`- " "   " (draw t)
    drawSubTrees (t :: ts) =
        "|" :: shift "+- " "|  " (draw t) ++ drawSubTrees ts

partial
drawTree : Tree String -> String
drawTree = unlines . draw

partial
drawForest : Forest String -> String
drawForest  = unlines . map drawTree

max_stars_repo_name: chrrasmussen/Idris-Deps

max_issues_repo_name: chrrasmussen/Idris-Deps

max_forks_repo_name: chrrasmussen/Idris-Deps