text:
module Node.HTTP.Client

import public Node.HTTP

export
data ClientRequest : Type where [external]

export
data IncomingMessage : Type where [external]

namespace Request

  %foreign "node:lambda: req => req.end()"
  ffi_end : ClientRequest -> PrimIO ()

  export
  (.end) : HasIO io => ClientRequest -> io ()
  (.end) res = primIO $ ffi_end res

  %foreign "node:lambda: (ty, req, data) => req.write(data)"
  ffi_write : { 0 a : _ } -> ClientRequest -> a -> PrimIO ()

  export
  (.write) : HasIO io => ClientRequest -> a -> io ()
  (.write) res a = primIO $ ffi_write res a

namespace Response

  export
  %foreign "node:lambda: res => res.headers"
  (.headers) : IncomingMessage -> Headers

  export
  %foreign "node:lambda: res => res.statusCode"
  (.statusCode) : IncomingMessage -> String

  %foreign "node:lambda: (ty, res, data) => res.on('data', a => data(a)())"
  ffi_onData : IncomingMessage -> (a -> PrimIO ()) -> PrimIO ()

  export
  onData : HasIO io => IncomingMessage -> (a -> IO ()) -> io ()
  onData res cb = primIO $ ffi_onData res $ \a => toPrim $ cb a

  %foreign "node:lambda: (ty, res, error) => res.on('error', e => error(e)())"
  ffi_onError : IncomingMessage -> (e -> PrimIO ()) -> PrimIO ()

  export
  onError : HasIO io => IncomingMessage -> (a -> IO ()) -> io ()
  onError res cb = primIO $ ffi_onError res $ \e => toPrim $ cb e

  %foreign "node:lambda: (ty, res, end) => res.on('end', end)"
  ffi_onEnd : IncomingMessage -> PrimIO () -> PrimIO ()

  export
  onEnd : HasIO io => IncomingMessage -> (() -> IO ()) -> io ()
  onEnd res cb = primIO $ ffi_onEnd res $ toPrim $ cb ()

%foreign "node:lambda: (http, url, cb) => http.get(url, (res) => { cb(res)() })"
ffi_get : HTTP -> String -> (IncomingMessage -> PrimIO ()) -> PrimIO ClientRequest

export
(.get) : HasIO io => HTTP -> String -> (IncomingMessage -> IO ()) -> io ClientRequest
(.get) http url cb = primIO $ ffi_get http url $ \res => toPrim $ cb res

%foreign "node:lambda: (http, url, cb) => http.request(url, {method: 'POST'}, (res) => { cb(res)() })"
ffi_post : HTTP -> String -> (IncomingMessage -> PrimIO ()) -> PrimIO ClientRequest

export
(.post) : HasIO io => HTTP -> String -> (IncomingMessage -> IO ()) -> io ClientRequest
(.post) http url cb = primIO $ ffi_post http url $ \res => toPrim $ cb res

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Main

fac : Integer -> Integer
fac 0 = 1
fac n = n*fac(n-1)

binomial : Integer -> Integer -> Integer
binomial n k = divBigInt (fac n) ((fac k)*(fac (n-k)))

sumBinomials : Integer -> Integer
sumBinomials n = foldr (+) 0 (map (\k=>binomial n k) [0..n])

main : IO ()
main = do
	if sumBinomials 1000 - pow 2 1000 == 0
		then putStrLn "OK"
		else putStrLn "ERROR"

ext: idr

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
{- 1 -}

same_cons : {xs : List a} -> {ys : List a} ->
             xs = ys -> x :: xs = x :: ys
same_cons Refl = Refl

{- 2 -}

same_lists : {xs : List a} -> {ys : List a} ->
             x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

{- 3 -}

data ThreeEq : a -> b -> c -> Type where
     AllSame : ThreeEq x x x

{- 4 -}

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS x x x AllSame = AllSame

-- If you add a successor to three equal Nats, the results are all equal

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
-- -------------------------------------------------------------- [ Common.idr ]
-- Description : Common Parsing Functions
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Config.Parse.Common

import Effects
import Effect.File

import Lightyear
import Lightyear.Char
import Lightyear.Strings
import Lightyear.StringFile

import Config.Parse.Utils
import Config.Error

%access export

langSpace : Parser () -> Parser ()
langSpace p = p <|> spaces <?> "Space Lang"

keyvalue : String
         -> Parser String
         -> Parser (String, String)
keyvalue s value = do
    k <- word
    spaces
    token s
    v <- value
    spaces
    pure (k,v)
  <?> "KVPair"

readConfigFile : Parser a
              -> String
              -> Eff (Either ConfigError a) [FILE ()]
readConfigFile p f = parseFile FileNotFound ParseError p f

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

max_stars_repo_name: jfdm/idris-config

max_issues_repo_name: jfdm/idris-config

max_forks_repo_name: jfdm/idris-config


text:
module Postgres.Data.ResultStatus

||| See the `ExecStatusType` from libpq for more information.
||| constructors below are derived from libpq options by
||| dropping the "PGRES_" prefix
public export
data ResultStatus = EMPTY_QUERY
                  | COMMAND_OK
                  | TUPLES_OK
                  | COPY_OUT
                  | COPY_IN
                  | BAD_RESPONSE
                  | NONFATAL_ERROR
                  | FATAL_ERROR
                  | COPY_BOTH
                  | SINGLE_TUPLE
                  | OTHER Int

export
Show ResultStatus where
  show EMPTY_QUERY    = "EMPTY_QUERY"
  show COMMAND_OK     = "COMMAND_OK"
  show TUPLES_OK      = "TUPLES_OK"
  show COPY_OUT       = "COPY_OUT"
  show COPY_IN        = "COPY_IN"
  show BAD_RESPONSE   = "BAD_RESPONSE"
  show NONFATAL_ERROR = "NONFATAL_ERROR"
  show FATAL_ERROR    = "FATAL_ERROR"
  show COPY_BOTH      = "COPY_BOTH"
  show SINGLE_TUPLE   = "SINGLE_TUPLE"
  show (OTHER x)      = "OTHER " ++ (show x)

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
module Common.Util

import public Data.So
import public Data.Vect
import public Data.Rel
import public Decidable.Decidable
import public Common.Abbrev

%default total
%access public export

export
rewriteRelation : (rel : Binrel s) -> a = aa -> b = bb -> rel a b -> rel aa bb
rewriteRelation rel p q given = rewrite sym p in rewrite sym q in given

export
contraposition : (p -> q) -> Not q -> Not p
contraposition f contra p = contra (f p)

total export
butNotLeft : Either a b -> Not a -> b
butNotLeft (Left a) contra = absurd (contra a)
butNotLeft (Right b) _ = b

total
isItSo : (b : Bool) -> Dec (So b)
isItSo True = Yes Oh
isItSo False = No absurd

data EitherErased : Type -> Type -> Type where
  Left  : .a -> EitherErased a b
  Right : .b -> EitherErased a b

namespace Either3Erased
  data Either3Erased : Type -> Type -> Type -> Type where
    Left   : .a -> Either3Erased a b c
    Middle : .b -> Either3Erased a b c
    Right  : .c -> Either3Erased a b c

implementation Show (EitherErased a b) where
  show (Left _) = "Left"
  show (Right _) = "Right"

implementation Show (Either3Erased a b c) where
  show (Left _) = "Left"
  show (Middle _) = "Middle"
  show (Right _) = "Right"

decideBoth : (a -> b -> c) -> (c -> a) -> (c -> b) -> Dec a -> Dec b -> Dec c
decideBoth pair left right = dec
  where
    dec (Yes a) (Yes b) = Yes (pair a b)
    dec (No contra) _ = No (contra . left)
    dec _ (No contra) = No (contra . right)

||| Reduce code clutter: if you inline this where it is used, an
||| explicit type annotation would be needed.
decision : Decidable [s,s] rel => (a,b : s) -> Dec (rel a b)
decision {s} = decide {ts = [s,s]}

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
||| Properties of Ackermann functions
module Data.Nat.Ack

%default total

-- Primitive recursive functions are functions that can be calculated
-- by programs that don't use unbounded loops. Almost all common
-- mathematical functions are primitive recursive.

-- Uncomputable functions are functions that can't be calculated by
-- any programs at all. One example is the Busy Beaver function:
--   BB(k) = the maximum number of steps that can be executed by a
--           halting Turing machine with k states.
-- The values of the Busy Beaver function are unimaginably large for
-- any but the smallest inputs.

-- The Ackermann function is the most well-known example of a total
-- computable function that is not primitive recursive, i.e. a general
-- recursive function. It grows strictly faster than any primitive
-- recursive function, but also strictly slower than a function like
-- the Busy Beaver.

-- There are many variations of the Ackermann function. Here is one
-- common definition
-- (see https://sites.google.com/site/pointlesslargenumberstuff/home/2/ackermann)
-- that uses nested recursion:

ackRec : Nat -> Nat -> Nat
-- Base rule
ackRec Z m = S m
-- Prime rule
ackRec (S k) Z = ackRec k 1
-- Catastrophic rule
ackRec (S k) (S j) = ackRec k $ ackRec (S k) j

-- The so-called "base rule" and "prime rule" work together to ensure
-- termination. Happily, the Idris totality checker has no issues.

-- An unusual "repeating" defintion of the function is given in the
-- book The Little Typer:

ackRep : Nat -> Nat -> Nat
ackRep Z = (+) 1
ackRep (S k) = repeat (ackRep k)
  where
    repeat : (Nat -> Nat) -> Nat -> Nat
    repeat f Z = f 1
    repeat f (S k) = f (repeat f k)

-- These two definitions don't look like they define the same
-- function, but they do:

ackRepRec : (n, m : Nat) -> ackRep n m = ackRec n m
ackRepRec Z _ = Refl
ackRepRec (S k) Z = ackRepRec k 1
ackRepRec (S k) (S j) =
  rewrite sym $ ackRepRec (S k) j in
    ackRepRec k $ ackRep (S k) j


text:
module Brainfeck.Parse
-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:
import Control.ST
import Data.Vect as V

import Brainfeck.Type
import Brainfeck.Util

%default total

public export
data ParseError : Type where
  MkParseError  : Location -> String -> ParseError

data TempOp : Type where
  TOp  : Operation n -> Location -> TempOp
  TJZ  : Nat -> Location -> TempOp
  TJNZ : Nat -> Location -> TempOp

mkParseError : TempOp -> String -> ParseError
mkParseError (TOp  _ loc) err = MkParseError loc err
mkParseError (TJZ  _ loc) err = MkParseError loc err
mkParseError (TJNZ _ loc) err = MkParseError loc err

tokenToTOp : Token -> Location -> Nat -> TempOp
tokenToTOp TLeft loc _        = TOp OLeft {n=0} loc
tokenToTOp TRight loc _       = TOp ORight {n=0}loc
tokenToTOp TInc loc _         = TOp OInc {n=0} loc
tokenToTOp TDec loc _         = TOp ODec {n=0} loc
tokenToTOp TOut loc _         = TOp OOut {n=0} loc
tokenToTOp TIn loc _          = TOp OIn {n=0} loc
tokenToTOp TJumpForward loc i = TJZ i loc
tokenToTOp TJumpBack loc i    = TJNZ i loc

tempToOp : (numOps : Nat) -> TempOp -> Maybe (Operation numOps)
tempToOp _      (TOp OLeft  _) = Just OLeft
tempToOp _      (TOp ORight _) = Just ORight
tempToOp _      (TOp OInc   _) = Just OInc
tempToOp _      (TOp ODec   _) = Just ODec
tempToOp _      (TOp OOut   _) = Just OOut
tempToOp _      (TOp OIn    _) = Just OIn
tempToOp _      (TOp _      _) = Nothing
tempToOp numOps (TJZ  l _) = map OJumpZero  $ natToFin l numOps
tempToOp numOps (TJNZ l _) = map OJumpNZero $ natToFin l numOps

matchForwardJump : (jumpTo : Nat) -> TempOp -> TempOp
matchForwardJump n (TJZ _ loc) = TJZ n loc
matchForwardJump _ anything = anything

updateListElem : (a -> a) -> (idx : Nat) -> List a -> List a
updateListElem f n xs = go f (length xs `minus` S n) xs where
  go _ _ [] = []
  go f Z (x :: xs) = f x :: xs
  go f (S n) (x :: xs) = x :: go f n xs

goLoop : Tokens n -> (is : Var) -> (forwards : Var) -> (opNo : Var)
       -> ST id (Either ParseError (List TempOp))
            [ is ::: State (List TempOp),
              forwards ::: State (List (TempOp, Nat)),
              opNo ::: State Nat ]
goLoop [] is forwards _ = do
  fs <- read forwards
  case fs of
    Nil       => read is >>= \is => pure (Right $ reverse is)
    (f :: fs) => pure (Left $ mkParseError (fst f) "Unmatched forward jump")
goLoop ((loc, t) :: xs) is forwards iVar = do
  i <- read iVar
  update iVar (+1)
  let tOp = tokenToTOp t loc i
  case tOp of
    TJZ  _ l => do
      update forwards ((TJZ i l, i) ::)
      -- remember to update these when the matching bracket is found
      update is ((TJZ 0 l) ::)
      goLoop xs is forwards iVar
    TJNZ _ l => do
      fs <- read forwards
      case fs of
        Nil        => pure (Left $ MkParseError loc $ "Unmatched backward jump " ++ show i)
        ((_, prev) :: rem) => do
          write forwards rem
          update is ((TJNZ prev l) ::)
          update is (updateListElem (matchForwardJump i) prev)
          goLoop xs is forwards iVar
    _      => update is (tOp ::) >>= \_ => goLoop xs is forwards iVar

go : Tokens n -> ST id (Either ParseError (n : Nat ** Instructions n)) []
go ts = do
  is <- new Nil
  fs <- new Nil
  i  <- new Z

  instructionList <- call $ goLoop ts is fs i
  let instructionVect = map listToVect instructionList
  delete is
  delete fs
  delete i
  case instructionVect of
    (Left l) => pure $ Left l
    (Right (n ** vs)) =>
      let (m ** converted) = mapMaybe (tempToOp n) vs in
      case decEq n m of
        (Yes Refl   ) => pure . Right $ (n ** converted)
        (No  contra) =>
          pure . Left $ MkParseError (Loc 0 0) "Labels not bounded by number of operations."

export
parse : Tokens n -> Either ParseError (n : Nat ** Instructions n)
parse tokens = runPure (go tokens)

max_stars_repo_name: jhmcstanton/brainfeck

max_issues_repo_name: jhmcstanton/brainfeck

max_forks_repo_name: jhmcstanton/brainfeck


text:
module CoverBug

import Data.So

public export
data FastNat : Type where
  MkFastNat : (val : Integer) -> {auto 0 prf : So True} -> FastNat

prv1 : Integer -> (x : Integer ** So $ True)
prv1 x =
  case choose True of
    Left prf => (x ** Oh)
    Right noprf => absurd noprf

fromInteger : Integer -> FastNat
fromInteger v =
  let (v ** p) = prv1 $ v
  in MkFastNat v

doit : FastNat -> FastNat
doit 0 = 0


text:
x : Int
x = 1

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
-- By considering the terms in the Fibonacci sequence whose values do not exceed
-- four million, find the sum of the even-valued terms.

import Data.List
import Data.Stream

streamWhile : (a -> Bool) -> Stream a -> List a
streamWhile f (x::xs) =
  if   f x
  then x :: (streamWhile f xs)
  else []

even : Nat -> Bool
even Z     = True
even (S n) = not (even n)

fib : Stream Nat -- Why is this SOOOO slow?!
fib = 0 :: zipWith (+) fib (1::fib)

main : IO ()
main = print (sum (filter even (streamWhile (\x => x <= 4000000) fib)))

max_stars_repo_name: edu-di-wu/project-euler

max_issues_repo_name: edu-di-wu/project-euler

max_forks_repo_name: edu-di-wu/project-euler


text:
-- Port of https://hackage.haskell.org/package/parsec-3.1.13.0/docs/Text-Parsec-Expr.html
-- Original License	BSD-style: https://hackage.haskell.org/package/parsec-3.1.13.0/src/LICENSE

module Data.String.Parser.Expression

import Control.Monad.Identity
import Data.String.Parser

public export
data Assoc = AssocNone
           | AssocLeft
           | AssocRight

public export
data Operator a = Infix (Parser (a -> a -> a)) Assoc
                | Prefix (Parser (a -> a))
                | Postfix (Parser (a -> a))

public export
OperatorTable : Type -> Type
OperatorTable a = List (List (Operator a))

public export
BinaryOperator : Type -> Type
BinaryOperator a = List (Parser (a -> a -> a))

public export
UnaryOperator : Type -> Type
UnaryOperator a = List (Parser (a -> a))

public export
data Ops a = BinOp (BinaryOperator a) | UnOp (UnaryOperator a)

public export
ReturnType : Type -> Type
ReturnType a = (BinaryOperator a, BinaryOperator a, BinaryOperator a, UnaryOperator a, UnaryOperator a)

toParserBin : BinaryOperator a -> Parser (a -> a -> a)
toParserBin [] = fail "couldn't create binary parser"
toParserBin (x :: xs) = x <|> toParserBin xs

toParserUn : UnaryOperator a -> Parser (a -> a)
toParserUn [] = fail "couldn't create unary parser"
toParserUn (x :: xs) = x <|> toParserUn xs

ambiguous : (assoc : String) -> (op : Parser (a -> a -> a)) -> Parser a
ambiguous assoc op = do op
                        fail ("ambiguous use of a " ++ assoc ++ " associative operator")

mutual
  mkRassocP : (amLeft : Parser a) -> (amNon : Parser a) -> (rassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
  mkRassocP amLeft amNon rassocOp termP x =
   (do f <- rassocOp
       y <- do z <- termP ; mkRassocP1 amLeft amNon rassocOp termP z
       pure (f x y))
   <|> (amLeft)
   <|> (amNon)

  mkRassocP1 : (amLeft : Parser a) -> (amNon : Parser a) -> (rassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
  mkRassocP1 amLeft amNon rassocOp termP x = (mkRassocP amLeft amNon rassocOp termP x) <|> pure x

mutual
  mkLassocP : (amRight : Parser a) -> (amNon : Parser a) -> (lassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
  mkLassocP amRight amNon lassocOp termP x =
    (do f <- lassocOp
        y <- termP
        mkLassocP1 amRight amNon lassocOp termP (f x y))
    <|> amRight
    <|> amNon

  mkLassocP1 : (amRight : Parser a) -> (amNon : Parser a) -> (lassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
  mkLassocP1 amRight amNon lassocOp termP x = mkLassocP amRight amNon lassocOp termP x <|> pure x

mkNassocP : (amRight : Parser a) -> (amLeft : Parser a) -> (amNon : Parser a) -> (nassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
mkNassocP amRight amLeft amNon nassocOp termP x =
  do f <- nassocOp
     y <- termP
     amRight <|> amLeft <|> amNon
     pure (f x y)

public export
buildExpressionParser : (a : Type) -> OperatorTable a -> Parser a -> Parser a
buildExpressionParser a operators simpleExpr =
  foldl (makeParser a) simpleExpr operators
  where
    splitOp : (a : Type) -> Operator a -> ReturnType a -> ReturnType a
    splitOp x (Infix op AssocNone) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, op :: nassoc, prefixx, postfix)
    splitOp x (Infix op AssocLeft) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, op :: lassoc, nassoc, prefixx, postfix)
    splitOp x (Infix op AssocRight) (rassoc, lassoc, nassoc, prefixx, postfix) = (op :: rassoc, lassoc, nassoc, prefixx, postfix)
    splitOp x (Prefix op) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, nassoc, op :: prefixx, postfix)
    splitOp x (Postfix op) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, nassoc, prefixx, op :: postfix)

    makeParser : (a : Type) -> Parser a -> List (Operator a) -> Parser a
    makeParser a term ops =
      let (rassoc,lassoc,nassoc
               ,prefixx,postfix) = foldr (splitOp a) ([],[],[],[],[]) ops
          rassocOp = toParserBin rassoc
          lassocOp = toParserBin lassoc
          nassocOp = toParserBin nassoc
          prefixxOp = toParserUn prefixx
          postfixOp = toParserUn postfix

          amRight = ambiguous "right" rassocOp
          amLeft = ambiguous "left" lassocOp
          amNon = ambiguous "non" nassocOp

          prefixxP = prefixxOp <|> pure (\x => x)

          postfixP = postfixOp <|> pure (\x => x)

          termP = do pre <- prefixxP
                     x <- term
                     post <- postfixP
                     pure (post (pre x))

          rassocP = mkRassocP amLeft amNon rassocOp termP
          lassocP = mkLassocP amRight amNon lassocOp termP
          nassocP = mkNassocP amRight amLeft amNon nassocOp termP
          in
          do x <- termP
             rassocP x <|> lassocP x <|> nassocP x <|> pure x <?> "operator"


text:
module Data.DIMACS

import Data.List
import Data.Strings

import Text.Lexer
import Text.Parser

import Sat

%default total

public export
record CNFProblem where
  constructor MkCNFProblem
  numVars : Int
  numClauses : Int
  clauses : List Clause

export
Show CNFProblem where
  show prob = "CNF Problem (" ++ show prob.numVars ++ " vars, " ++ show prob.numClauses ++ " clauses):\n" ++
              show prob.clauses

data Token = Comment
           | Problem String
           | Zero
           | Lit String

Show Token where
  show Comment = "(comment)"
  show (Problem s) = "(problem: " ++ s ++ ")"
  show Zero = "0"
  show (Lit s) = s

comment : Lexer
comment = is 'c' <+> many (pred (/= '\n')) <+> is '\n' <+> many space

problem : Lexer
problem = is 'p' <+> is ' ' <+> many (pred (/= '\n')) <+> is '\n' <+> many space

zero : Lexer
zero = is '0' <+> many space

lit : Lexer
lit = opt (is '-') <+> some digit <+> some space

tokenMap : TokenMap Token
tokenMap = [
  (comment, \_ => Comment),
  (problem, Problem . trim),
  (zero, \_ => Zero),
  (lit, Lit . trim)
  ]

lexDimacs : String -> Either String (List Token)
lexDimacs s = let (toks, line, col, remainder) = lex tokenMap s in
                  if remainder == "" then Right $ map tok toks
                                     else Left $ "remaining: " ++ remainder

Parser : Type -> Type
Parser a = Grammar Token True a

isProblem : Token -> Maybe CNFProblem
isProblem (Problem s) = case words s of
                             ["p", "cnf", nVars, nClauses] =>
                               let numVars = cast nVars
                                   numClauses = cast nClauses in
                                     Just $ MkCNFProblem numVars numClauses []
                             _ => Nothing

isProblem _ = Nothing

literal : Token -> Maybe Sat.Lit
literal (Lit s) = let i = cast {to=Int} s in
                      if i > 0 then Just $ MkPos (MkVar (i-1))
                      else if i < 0 then Just $ MkNeg (MkVar ((-i) - 1))
                      else Nothing
literal _ = Nothing

isZero : Token -> Maybe ()
isZero Zero = Just ()
isZero _ = Nothing

isComment : Token -> Maybe ()
isComment Comment = Just ()
isComment _ = Nothing

parseClause : Parser (Maybe Clause)
parseClause = do
  lits <- many (terminal "literal" literal) <* terminal "zero" isZero
  many $ terminal "comment" isComment
  id $ case lits of
            [] => fatalError "empty clause can not be satisfied"
            (c::cs) => pure $ Just $ toClause (c::cs)

parseCNF : Parser CNFProblem
parseCNF = do
  many $ terminal "initial comment" isComment
  initState <- terminal "CNF problem header" isProblem
  parsedClauses <- some parseClause
  pure $ record { clauses = mapMaybe id parsedClauses } initState

showError : ParseError Token -> String
showError (Error e toks) = "parse error: " ++ e ++ "\nnext tokens: " ++ show toks

export
parseDIMACS : String -> Either String CNFProblem
parseDIMACS s = do
  toks <- lexDimacs s
  (parsed, toks) <- either (Left . showError) Right $ parse parseCNF toks
  Right parsed

export
showDIMACS : (Var, Bool) -> String
showDIMACS (MkVar d, True) = show (d+1)
showDIMACS (MkVar d, False) = show (-(d+1))


text:
module ProofColDivSeqLvDown

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

mutual
  lvDown''' : (n, lv:Nat) -> Any (Not . Limited) (allDivSeq n (S lv))
    -> Either (Any (Not . Limited) (allDivSeq n lv))
        (Either (Any (Not . Limited) (allDivSeqA n lv))
          (Either (Any (Not . Limited) (allDivSeqB n lv))
            (Either (Any (Not . Limited) (allDivSeqC n lv))
              (Either (Any (Not . Limited) (allDivSeqD n lv))
                (Either (Any (Not . Limited) (allDivSeqE n lv))
                  (Either (Any (Not . Limited) (allDivSeqF n lv))
                          (Any (Not . Limited) (allDivSeqG n lv)) ))))))
  lvDown''' n lv = rewrite defini n lv in
    \prf => anyFinal (allDivSeq n lv)
                     (allDivSeqA n lv)
                     (allDivSeqB n lv)
                     (allDivSeqC n lv)
                     (allDivSeqD n lv)
                     (allDivSeqE n lv)
                     (allDivSeqF n lv)
                     (allDivSeqG n lv) prf

  lvDown'' : (n,lv:Nat)
    -> Either (Any (Not . Limited) (allDivSeq n lv))
        (Either (Any (Not . Limited) (allDivSeqA n lv))
          (Either (Any (Not . Limited) (allDivSeqB n lv))
            (Either (Any (Not . Limited) (allDivSeqC n lv))
              (Either (Any (Not . Limited) (allDivSeqD n lv))
                (Either (Any (Not . Limited) (allDivSeqE n lv))
                  (Either (Any (Not . Limited) (allDivSeqF n lv))
                          (Any (Not . Limited) (allDivSeqG n lv)) ))))))
      -> Any (Not . Limited) (allDivSeq n lv)
  lvDown'' n Z (Left l)                                                  = l
  lvDown'' n Z (Right (Left l))                                          = defini0 n $ Right (Left (changeA0 n l))
  lvDown'' n Z (Right (Right (Left l)))                                  = defini0 n $ (Right (Right (Left (changeB0 n l))))
  lvDown'' n Z (Right (Right (Right (Left l))))                          = defini0 n $ (Right (Right (Right (Left (changeC0 n l)))))
  lvDown'' n Z (Right (Right (Right (Right (Left l)))))                  = defini0 n $ (Right (Right (Right (Right (Left (changeD0 n l))))))
  lvDown'' n Z (Right (Right (Right (Right (Right (Left l))))))          = defini0 n $ (Right (Right (Right (Right (Right (Left (changeE0 n l)))))))
  lvDown'' n Z (Right (Right (Right (Right (Right (Right (Left l)))))))  = defini0 n $ (Right (Right (Right (Right (Right (Right (Left (changeF0 n l))))))))
  lvDown'' n Z (Right (Right (Right (Right (Right (Right (Right r))))))) = defini0 n $ (Right (Right (Right (Right (Right (Right (Right (changeG0 n r))))))))
  lvDown'' n (S lv) (Left l)                                                  = l
  lvDown'' n (S lv) (Right (Left l))                                          = defini3 n lv $ Right (Left (lvDown' (divNatNZ ((n+7)*3) 4 SIsNotZ) (S lv) (changeA n lv l)))
  lvDown'' n (S lv) (Right (Right (Left l)))                                  = defini3 n lv $ (Right (Right (Left (lvDown' (n*6+3) (S lv) (changeB n lv l)))))
  lvDown'' n (S lv) (Right (Right (Right (Left l))))                          = defini3 n lv $ (Right (Right (Right (Left (lvDown' (n*3+6) (S lv) (changeC n lv l))))))
  lvDown'' n (S lv) (Right (Right (Right (Right (Left l)))))                  = defini3 n lv $ (Right (Right (Right (Right (Left (lvDown' (divNatNZ ((n+1)*3) 2 SIsNotZ) (S lv) (changeD n lv l)))))))
  lvDown'' n (S lv) (Right (Right (Right (Right (Right (Left l))))))          = defini3 n lv $ (Right (Right (Right (Right (Right (Left (lvDown' (n*12+9) (S lv) (changeE n lv l))))))))
  lvDown'' n (S lv) (Right (Right (Right (Right (Right (Right (Left l)))))))  = defini3 n lv $ (Right (Right (Right (Right (Right (Right (Left (lvDown' (divNatNZ ((n+3)*3) 8 SIsNotZ) (S lv) (changeF n lv l)))))))))
  lvDown'' n (S lv) (Right (Right (Right (Right (Right (Right (Right r))))))) = defini3 n lv $ (Right (Right (Right (Right (Right (Right (Right (lvDown' (divNatNZ (n `minus` 21) 64 SIsNotZ) (S lv) (changeG n lv r)))))))))

  -- レベルを下げる事ができる
  lvDown' : (n, lv:Nat) -> Any (Not . Limited) $ allDivSeq n lv
                        -> Any (Not . Limited) $ allDivSeq n (pred lv)
  lvDown' n Z      prf = prf
  lvDown' n (S lv) prf = lvDown'' n lv $ lvDown''' n lv prf
-- ---------------------------------


text:
module Matrix

-- Based on https://dl.acm.org/doi/10.1145/3406088.3409019

import Data.Nat.DivMod

data Shape : Type where
  Zero : Shape
  One : Shape
  Plus : Shape -> Shape -> Shape

data Matrix : (e : Type) -> (c : Shape) -> (r : Shape) -> Type where
  Elem : e -> Matrix e One One
  Join : Matrix e a r -> Matrix e b r -> Matrix e (Plus a b) r
  Fork : Matrix e c a -> Matrix e c b -> Matrix e c (Plus a b)

fromNat' : Nat -> Nat -> Shape
fromNat' k Z = Zero
fromNat' k (S Z) = One
fromNat' Z n = Zero
fromNat' (S k) n with (divMod n 1)
  fromNat' (S k) (remainder + (quotient * (S (S Z)))) | (MkDivMod quotient remainder remainderSmall) =
    let m = fromNat' k quotient in
    if remainder == Z then Plus m m else Plus One (Plus m m)

fromNat : Nat -> Shape
fromNat n = fromNat' 64 n

abideJF : Matrix e cols rows -> Matrix e cols rows
abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d))
abideJF (Elem e) = Elem e
abideJF (Join a b) = Join (abideJF a) (abideJF b)
abideJF (Fork a b) = Fork (abideJF a) (abideJF b)

zipWithM : (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM f (Elem a) (Elem b) = Elem (f a b)
zipWithM f (Join a b) (Join c d) = Join (zipWithM f a c) (zipWithM f b d)
zipWithM f (Fork a b) (Fork c d) = Fork (zipWithM f a c) (zipWithM f b d)
zipWithM f x@(Fork _ _) y@(Join _ _) = zipWithM f x (abideJF y)
zipWithM f x@(Join _ _) y@(Fork _ _) = zipWithM f (abideJF x) y

comp : Num e => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp (Elem a) (Elem b) = Elem (a * b)
comp (Join a b) (Fork c d) = zipWithM (+) (comp a c) (comp b d)
comp (Fork a b) c = Fork (comp a c) (comp b c)
comp c (Join a b) = Join (comp c a) (comp c b)

iden2x2 : Num e => Matrix e (fromNat 2) (fromNat 2)
iden2x2 = Fork (Join (Elem 1) (Elem 0))
               (Join (Elem 0) (Elem 1))

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module FinCmp

-- Decidable comparison of finite numbers less
-- than a given bound (i.e. "ordinals").

import public Data.Fin

%default total
%access public export

-------------------------------------------
-- Begin: DECIDABLE COMPARISONS OF ORDINALS

-- Data type for evidence that "i < j".
data FinLT : Fin n -> Fin n -> Type where
  LtZ : FinLT FZ (FS i)
  LtS : FinLT i j -> FinLT (FS i) (FS j)

-- Simplified symtax:
infixl 6 :<:
(:<:) : Fin n -> Fin n -> Type
(:<:) = FinLT

-- Data type for evidence of which of the
-- following holds between ordinals 'i' and 'j':
--
--    (a) i < j
--    (b) i = j
--    (c) i < j
--
data FinCMP : Fin n -> Fin n -> Type where
  CmpEq : (i = j) -> FinCMP i j
  CmpLt : i :<: j -> FinCMP i j
  CmpGt : j :<: i -> FinCMP i j

-- Function 'finNotLtZ' yields a proof of the following:
--
--    "There is no ordinal less than zero."
--     (In other words, given a proof that 'i' is
--     less than zero, the function 'finNotLtZ' yields
--     a member of the uninhabited type 'Void'.)
--
finNotLtZ : i :<: FZ -> Void
finNotLtZ _ impossible

-- Function 'finCmpDec' decides whether
--
--    (a) i < j, or
--    (b) i = j, or
--    (c) i > j  holds,
--
-- and yields evidence in the form of a value
-- of type 'FinCMP i j'.
finCmpDec : (i : Fin n) -> (j : Fin n) -> (FinCMP i j)
finCmpDec i j = case i of
  FZ => case j of
             FZ    => CmpEq Refl
             FS j' => CmpLt LtZ
  FS i' => case j of
                FZ    => CmpGt LtZ
                FS j' => case finCmpDec i' j' of
                              CmpEq eq => CmpEq (rewrite eq in Refl)
                              CmpLt lt => CmpLt (LtS lt)
                              CmpGt lt => CmpGt (LtS lt)

-- Function 'finLtPred' yields a proof of the following:
--
--    "Given (FS i) < (FS j)m then i < j".
--
finLtPred : (FS i) :<: (FS j) -> i :<: j
finLtPred lt = case lt of LtS lt' => lt'

-- End: DECIDABLE COMPARISONS OF ORDINALS
-----------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Core.Term

import Pruviloj
import Derive.Eq

import General

import Core.Variable

%language ElabReflection

%hide Language.Reflection.Elab.FunArg
%access private

--  oYYo _YYY_ 8o  0 oYYYo YY8YY 8YYYo 0   0  oYYo YY8YY _YYY_ 8YYYo
-- 0   " 0   0 8Yo 8 %___    0   8___P 0   0 0   "   0   0   0 8___P
-- 0   , 0   0 8 Yo8 `"""p   0   8""Yo 0   0 0   ,   0   0   0 8""Yo
--  YooY "ooo" 0   8 YoooY   0   0   0 "ooo"  YooY   0   "ooo" 0   0

public export
data Constructor = BareCon String | DottedCon String String | AbsoluteDottedCon String String

export
Interfaces.Eq Constructor where
	(BareCon x) == (BareCon x') = x == x'
	(DottedCon x y) == (DottedCon x' y') = x == x' && y == y'
	(AbsoluteDottedCon x y) == (AbsoluteDottedCon x' y') = x == x' && y == y'
	_ == _ = False

export
Show Constructor where
	show (BareCon con) = con
	show (DottedCon m con) = m ++ "." ++ con
	show (AbsoluteDottedCon m con) = m ++ "." ++ con

-- YY8YY 8YYYY 8YYYo 8_   _8 oYYYo
--   0   8___  8___P 8"o_o"8 %___
--   0   8"""  8""Yo 0  8  0 `"""p
--   0   8oooo 0   0 0     0 YoooY

mutual
	public export
	data Term : Type where
		-- Metavariable, or "hole"
		Meta : Int -> Term
		-- Bound variable
		Var : Variable -> Term
		-- Imported Variable
		DottedVar : String -> String -> Term
		AbsoluteDottedVar : String -> String -> Term
		-- Annotated term
		Ann : Term -> Term -> Term
		-- Universe
		Star : Term
		-- Function Type, “Pi”. Using HOAS for binding.
		Pi : Plict -> Term -> (Scope Term Term) -> Term
		-- Lambda abstraction
		Lam : Plict -> (Scope Term Term) -> Term
		-- Function Application
		App : Plict -> Term -> Term -> Term
		-- Data Construction
		Con : Constructor -> List (Plict >< Term) -> Term
		-- Case Analysis
		Case : List Term -> CaseMotive -> List Clause -> Term
		-- Record Types
		RecordType : Telescope -> Term
		-- Record Construction
		RecordCon : List (String, Term) -> Term
		-- Record Projection
		Project : Term -> String -> Term

	public export
	data CaseMotive
		= CaseMotiveNil Term
		| CaseMotiveCons Term (Scope Term CaseMotive)

	public export
	data Clause = NewClause (Scope Variable (List Pattern)) (Scope Term Term)

	public export
	data Pattern
		= VarPat Variable
		| ConPat Constructor (List (Plict >< Pattern))
		| AssertionPat Term
		| MakeMeta

	public export
	data Telescope
		= TelescopeNil
		| TelescopeCons Term (Scope Term Telescope)

-- 8YYYo 8YYYo 8YYYY YY8YY YY8YY 0   0      8YYYo 8YYYo Y8Y 8o  0 YY8YY
-- 8___P 8___P 8___    0     0   "o o" ____ 8___P 8___P  0  8Yo 8   0
-- 8"""  8""Yo 8"""    0     0     0   """" 8"""  8""Yo  0  8 Yo8   0
-- 0     0   0 8oooo   0     0     0        0     0   0 o8o 0   8   0

public export
data PatternParenLoc = ExplConPatArg | ImplConPatArg

derive Eq for PatternParenLoc

public export
ParenLoc Pattern where
	Loc = PatternParenLoc
	parenLoc (VarPat _)       = [ExplConPatArg,ImplConPatArg]
	parenLoc (ConPat _ _)     = [ImplConPatArg]
	parenLoc (AssertionPat _) = [ExplConPatArg,ImplConPatArg]
	parenLoc MakeMeta         = [ExplConPatArg,ImplConPatArg]

public export
data TermParenLoc
  = RootTerm
  | AnnLeft | AnnRight
  | FunArg | FunRet
  | LamBody | AppLeft | ExplAppRight | ImplAppRight
  | ExplConArg | ImplConArg | AssertionPatArg
  | RecDotArg
derive Eq for TermParenLoc

public export
ParenLoc Term where
	Loc = TermParenLoc
	parenLoc (Meta _) = [AnnLeft,FunArg,FunRet,LamBody,AppLeft,ExplAppRight,ImplAppRight,ExplConArg,ImplConArg,AssertionPatArg,RecDotArg]
	parenLoc (Var _) = [AnnLeft,FunArg,FunRet,LamBody,AppLeft,ExplAppRight,ImplAppRight,ExplConArg,ImplConArg,AssertionPatArg,RecDotArg]
	parenLoc (DottedVar _ _) = [AnnLeft,FunArg,FunRet,LamBody,AppLeft,ExplAppRight,ImplAppRight,ExplConArg,ImplConArg,AssertionPatArg,RecDotArg]
	parenLoc (AbsoluteDottedVar _ _) = [AnnLeft,FunArg,FunRet,LamBody,AppLeft,ExplAppRight,ImplAppRight,ExplConArg,ImplConArg,AssertionPatArg,RecDotArg]
	parenLoc (Ann _ _) = [FunArg,FunRet,LamBody,ImplAppRight,ImplConArg]
	parenLoc Star = [AnnLeft,FunArg,FunRet,LamBody,AppLeft,ExplAppRight,ImplAppRight,ExplConArg,ImplConArg,AssertionPatArg,RecDotArg]
	parenLoc (Pi _ _ _) = [FunArg,FunRet,LamBody,ImplAppRight,ImplConArg]
	parenLoc (Lam _ _) = [FunArg,FunRet,LamBody,ImplAppRight,ImplConArg]
	parenLoc (App _ _ _) = [FunArg,FunRet,AnnLeft,LamBody,AppLeft,ImplAppRight,ImplConArg]
	parenLoc (Con _ []) = [FunArg,FunRet,AnnLeft,LamBody,AppLeft,ExplAppRight,ImplAppRight,ExplConArg,ImplConArg,AssertionPatArg]
	parenLoc (Con _ _) = [FunArg,FunRet,AnnLeft,LamBody,ImplAppRight,ImplConArg]
	parenLoc (Case _ _ _) = [FunArg,FunRet,LamBody,ImplAppRight,ImplConArg]
	parenLoc (RecordType _) = [FunArg,FunRet,AnnLeft,LamBody,AppLeft,ExplAppRight,ImplAppRight,ExplConArg,ImplConArg,AssertionPatArg,RecDotArg]
	parenLoc (RecordCon _) = [FunArg,FunRet,AnnLeft,LamBody,AppLeft,ExplAppRight,ImplAppRight,ExplConArg,ImplConArg,AssertionPatArg,RecDotArg]
	parenLoc (Project _ _) = [AnnLeft,FunArg,FunRet,LamBody,AppLeft,ExplAppRight,ImplAppRight,ExplConArg,ImplConArg,AssertionPatArg,RecDotArg]

mutual
	export
	ParenRec Pattern where
		parenRec (VarPat x) = show x
		parenRec (ConPat c []) = show c
		parenRec (ConPat c ps) = show c ++ " " ++ unwords (map auxConPatArg ps)
		where
			auxConPatArg : (Plict,Pattern) -> String
			auxConPatArg (Expl,p) = parenthesize (Just ExplConPatArg) p
			auxConPatArg (Impl,p) = "{" ++ parenthesize (Just ImplConPatArg) p ++ "}"
		parenRec (AssertionPat m) = "." ++ parenthesize (Just AssertionPatArg) m
		parenRec MakeMeta = "?makemeta"

	export
	Show Pattern where
		show p = parenthesize Nothing p

	export
	ParenRec Term where
		parenRec (Meta i) = "?" ++ show i
		parenRec (Var x) = show x
		parenRec (DottedVar m x) = m ++ "." ++ x
		parenRec (AbsoluteDottedVar m x) = m ++ "." ++ x
		parenRec (Ann m ty) = parenthesize (Just AnnLeft) m ++ " : " ++ parenthesize (Just AnnRight) ty
		parenRec Star = "Type"
		parenRec (Pi plic a sc) = do
			let a0' = (unwords $ names sc) ++ " : " ++ parenthesize (Just FunArg) a
			let a' = case plic of
				Expl => "(" ++ a0' ++ ")"
				Impl => "{" ++ a0' ++ "}"
			a' ++ " -> " ++ parenthesize (Just FunRet) (descope (Var . Name) sc)
		parenRec (Lam plic sc) =
			let
				n0' = unwords (names sc)
				n' = case plic of
					Expl => n0'
					Impl => "{" ++ n0' ++ "}"
			in "\\" ++ n' ++ " => " ++ parenthesize (Just LamBody) (descope (Var . Name) sc)
		parenRec (App plic f a) =
			let
				a' = case plic of
					Expl => parenthesize (Just ExplAppRight) a
					Impl => "{" ++ parenthesize (Just ImplAppRight) a ++ "}"
			in parenthesize (Just AppLeft) f ++ " " ++ a'
		parenRec (Con c []) = show c
		parenRec (Con c as) = do
			let as' = [ case plic of
							Expl => parenthesize (Just ExplConArg) a
							Impl => "{" ++ parenthesize (Just ImplConArg) a ++ "}"
						| (plic, a) <- as ]
			hcat [
				(show c),
				" ",
				unwords as']
			-- Prelude.Strings.(++) (show c) $ Prelude.Strings.(++) " " (unwords as')
		parenRec (Case ms mot cs) = hcat [
				"case ",
				interlace " || " (map (parenthesize Nothing) ms),
				" motive ",
				show mot,
				" of ",
				interlace " | " (map auxClause cs),
				" end"
			]
			where
				auxClause : Clause -> String
				auxClause (NewClause psc sc) = hcat [
					interlace " || " (map show (descope Name psc)),
					" => ",
					parenthesize Nothing (descope (Var . Name) sc)
				]
		parenRec (RecordType tele)
			= case auxTelescope tele of
				[] => "Struct {}"
				fields => "Struct { " ++ interlace ", " fields ++ " }"
			where
				auxTelescope : Telescope -> List String
				auxTelescope TelescopeNil = []
				auxTelescope (TelescopeCons t sc) = do
					let f = unwords (names sc) ++ " : " ++ parenthesize Nothing t
					let fs = auxTelescope (descope (Var . Name) sc)
					f :: fs
		parenRec (RecordCon fields) = if (length fields == 0)
			then "new {}"
			else "new { " ++ interlace ", " [ x ++ " = " ++ parenthesize Nothing t | (x,t) <- fields ] ++ " }"
		parenRec (Project m x) = parenthesize (Just RecDotArg) m ++ "." ++ x

	export
	Show Term where
		show t = parenthesize Nothing t

	export
	Show CaseMotive where
		show (CaseMotiveNil ret) = show ret
		show (CaseMotiveCons arg sc)
			= "(" ++ unwords (names sc) ++ " : " ++ show arg ++ ") || "
				++ show (descope (Var . Name) sc)

-- 8888_ 8YYYY  oYYo 0     o8o  8YYYo  oYYo
-- 0   0 8___  0   " 0    8   8 8___P 0  __
-- 0   0 8"""  0   , 0    8YYY8 8""Yo 0  "8
-- 8oooY 8oooo  YooY 8ooo 0   0 0   0  YooY

public export
data DeclArg = NewDeclArg Plict String Term

export
Show DeclArg where
	show (NewDeclArg Expl x t) = "(" ++ x ++ " : " ++ show t ++ ")"
	show (NewDeclArg Impl x t) = "{" ++ x ++ " : " ++ show t ++ "}"

-- 8_   _8 8YYYY YY8YY  o8o  oYYYo
-- 8"o_o"8 8___    0   8   8 %___
-- 0  8  0 8"""    0   8YYY8 `"""p
-- 0     0 8oooo   0   0   0 YoooY

export
metas : Term -> List Int
metas x = nub (go x)
where
	go : Term -> List Int
	goPat : Pattern -> List Int
	goCaseMotive : CaseMotive -> List Int
	goClause : Clause -> List Int
	goTele : Telescope -> List Int

	go (Meta i) = [i]
	go (Var _) = []
	go (DottedVar _ _) = []
	go (AbsoluteDottedVar _ _) = []
	go (Ann m t) = go m ++ go t
	go Star = []
	go (Pi _ a sc) = go a ++ go (descope (Var . Name) sc)
	go (Lam _ sc) = go (descope (Var . Name) sc)
	go (App _ f x) = go f ++ metas x
	go (Con _ xs) = concat (map (go . snd) xs)
	go (Case as mot cs) = concat (map go as) ++ goCaseMotive mot ++ concat (map goClause cs)
	go (RecordType tele) = goTele tele
	go (RecordCon fields) = concat (map (go . snd) fields)
	go (Project m _) = go m

	goPat (VarPat _) = []
	goPat (ConPat _ ps) = concat (map (goPat . snd) ps)
	goPat (AssertionPat m) = go m
	goPat MakeMeta = []

	goCaseMotive (CaseMotiveNil t) = go t
	goCaseMotive (CaseMotiveCons a sc) = go a ++ goCaseMotive (descope (Var . Name) sc)

	goClause (NewClause psc sc) = concat (map goPat (descope Name psc)) ++ go (descope (Var . Name) sc)

	goTele TelescopeNil = []
	goTele (TelescopeCons m sc) = go m ++ goTele (descope (Var . Name) sc)

-- 0   0 YY8YY Y8Y 0    Y8Y YY8YY Y8Y 8YYYY oYYYo
-- 0   0   0    0  0     0    0    0  8___  %___
-- 0   0   0    0  0     0    0    0  8"""  `"""p
-- "ooo"   0   o8o 8ooo o8o   0   o8o 8oooo YoooY

export
caseMotiveLength : CaseMotive -> Int
caseMotiveLength (CaseMotiveNil _) = 0
caseMotiveLength (CaseMotiveCons _ sc) = 1 + caseMotiveLength (descope (Var . Name) sc)

export
patternVars : Pattern -> List Variable
patternVars (VarPat v) = [v]
patternVars (ConPat _ ps) = ps >>= (patternVars . snd)
patternVars (AssertionPat _) = []
patternVars MakeMeta = []

export
termToPattern : Term -> Pattern
termToPattern (Var x) = VarPat x
termToPattern (Con c xs) = ConPat c [ (plic, termToPattern x) | (plic,x) <- xs ]
termToPattern m = AssertionPat m

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
import Data.Primitives.Views
import System

quiz : Stream Int -> (score : Nat) -> IO ()
quiz (num1 :: num2 :: nums) score
   = do putStrLn ("Score so far: " ++ show score)
        putStr (show num1 ++ " * " ++ show num2 ++ "? ")
        answer <- getLine
        if cast answer == num1 * num2
           then do putStrLn "Correct!"
                   quiz nums (score + 1)
           else do putStrLn ("Wrong, the answer is " ++ show (num1 * num2))
                   quiz nums score

randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                   (seed' `shiftR` 2) :: randoms seed'

arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
  where
    bound : Int -> Int
    bound x with (divides x 12)
      bound ((12 * div) + rem) | (DivBy div rem prf) = rem + 1

main : IO ()
main = do seed <- time
          quiz (arithInputs (fromInteger seed)) 0


text:
module FreeRTOS.Task.Utils

import FreeRTOS.Task.Control

%default total
%include C "FreeRTOS.h"
%include C "task.h"

||| The handle of the currently running (calling) task.
getCurrentTaskTID : IO TID
getCurrentTaskTID = do
    ptr <- foreign FFI_C "xTaskGetCurrentTaskHandle" (IO Ptr)
    pure (MkTID ptr)

||| The task handle associated with the Idle task.
getIdleTaskHandle : IO TID
getIdleTaskHandle = do
    ptr <- foreign FFI_C "xTaskGetIdleTaskHandle" (IO Ptr)
    pure (MkTID ptr)

||| Looks up the name of a task from the task’s handle.
getName : TID -> IO String
getName (MkTID ptr) =
    foreign FFI_C "pcTaskGetName" (Ptr -> IO String) ptr

||| The number of tasks that the RTOS kernel is currently managing.
getNbrTasks : IO Int
getNbrTasks =
    foreign FFI_C "uxTaskGetNumberOfTasks" (IO Int)

max_stars_repo_name: mokshasoft/FreeRTOS-community-ports

max_issues_repo_name: mokshasoft/FreeRTOS-community-ports

max_forks_repo_name: mokshasoft/FreeRTOS-community-ports


text:
module Algebra

import public Algebra.ZeroOneOmega
import public Algebra.Semiring
import public Algebra.Preorder

%default total

public export
RigCount : Type
RigCount = ZeroOneOmega

max_stars_repo_name: archaeron/idris-ipkg

max_issues_repo_name: archaeron/idris-ipkg

max_forks_repo_name: archaeron/idris-ipkg


text:
module Main

import IdrisJvm.IO
import IdrisJvm.JvmImport
import Java.Lang
import Java.Util
import mmhelloworld.idrisjvmautoffisample.importer.JvmImporter

%access public export
%language ElabReflection

main : JVM_IO ()
main = do
  printLn !((integerClass <.!> "parseInt") "23")

  objectMapper <- (objectMapperClass <.!> "<init>()")
  jsonNode <- (objectMapperClass <.!> "readTree(java/lang/String)") objectMapper "{\"coord\": {\"lon\": -0.13, \"lat\": 51.51}}"
  latNode <- (jsonNodeClass <.!> "at(java/lang/String)") jsonNode "/coord/lat"
  lat <- (jsonNodeClass <.!> "asDouble()") latNode
  printLn lat

max_stars_repo_name: mmhelloworld/idris-jvm-auto-ffi-sample

max_issues_repo_name: mmhelloworld/idris-jvm-auto-ffi-sample

max_forks_repo_name: mmhelloworld/idris-jvm-auto-ffi-sample


text:
import System.File
import Data.String
import Data.List

-- read in a dictionary, shuffle and then resort

mylast : List a -> Maybe a
mylast [] = Nothing
mylast [x] = Just x
mylast (x::xs) = mylast xs

doSort : Nat -> IO ()
doSort Z     = putStrLn "Done"
doSort (S k) = do Right dict<-readFile "words"
                   | Left err => putStrLn $ show err
                  -- reverse and get last word
                  let xs  = reverse $ words dict
                  putStrLn $ show $ mylast xs
                  -- sort reversed list and get last word
                  putStrLn $ show $ mylast $ sort xs
                  doSort k

main : IO ()
main = do max <- getLine
          doSort (integerToNat (cast max))


text:
module Data.VectorSpace

import Data.Vect

infixr 9 *^
infixl 9 ^/
infixl 6 ^+^, ^-^
infix 7 `dot`

public export
interface VectorSpace v where
  ||| Vector with no magnitude (unit for addition).
  zeroVector : v

  ||| Multiplication by a scalar.
  (*^) : Double -> v -> v

  ||| Division by a scalar.
  (^/) : v -> Double -> v

  ||| Vector addition
  (^+^) : v -> v -> v

  ||| Vector subtraction
  (^-^) : v -> v -> v

  ||| Vector negation. Addition with a negated vector should
  ||| be same as subtraction.
  negateVector : v -> v
  negateVector v = zeroVector ^-^ v

  ||| Dot product (also known as scalar or inner product).
  ||| For two vectors, mathematically represented as a = a1,a2,...,an and b = b1,b2,...,bn,
  ||| the dot product is a . b = a1*b1 + a2*b2 + ... + an*bn.
  dot : v -> v -> Double

  ||| Vector's norm (also known as magnitude).
  ||| For a vector represented mathematically
  ||| as a = a1,a2,...,an, the norm is the square root of a1^2 + a2^2 + ... + an^2.
  norm : v -> Double
  norm v = sqrt $ dot v v

  ||| Return a vector with the same origin and orientation (angle),
  ||| but such that the norm is one (the unit for multiplication by a scalar).
  normalize : v -> v
  normalize v = let n = norm v in if n == 0 then v else v ^/ n

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export
VectorSpace Double where
  zeroVector = 0.0
  (^-^) = (-)
  (^+^) = (+)
  (^/)  = (/)
  (*^)  = (*)
  dot   = (*)

public export
{n : _} -> VectorSpace (Vect n Double) where
  zeroVector = replicate n 0.0
  (^-^)   = zipWith (-)
  (^+^)   = zipWith (+)
  v ^/ s  = map (/ s) v
  s *^ v  = map (* s) v
  dot a b = sum $ zipWith (*) a b


text:
||| Module containing the main typeclasses and recursion schemes on them.
module Data.Functor.Foldable.Mod

import Control.Monad.Identity
import Control.Monad.Free
import Control.Comonad
import Control.Comonad.Cofree

%access public export

||| This is an interface which does nothing interesting, but it functions as a
||| way of saying "f is a base functor with underlying type t"
interface Base t (f : Type -> Type) where

||| Interface for corecursive data types. Corecursive types correspond to
||| anamorphisms.
interface (Functor f, Base t f) => Corecursive (f : Type -> Type) (t : Type) where
  embed : f t -> t

||| Recursive types correspond to catamorphisms.
interface (Functor f, Base t f) => Recursive (f : Type -> Type) (t : Type) where
  project : t -> f t

||| Anamorphism, meant to build up a structure recursively.
ana : (Corecursive f t) => (a -> f a) -> a -> t
ana g = a'
  where a' x = embed . map a' . g $ x

||| Postpromorphism. Unfold a structure, applying a natural transformation along the way.
postpro : (Recursive f t, Corecursive f t) => (f t -> f t) -> (a -> f a) -> a -> t
postpro e g = a'
  where a' x = embed . map (ana (e . project) . a') . g $ x

||| Generalized Anamorphism
||| @ k A distributive law
||| @ g A (f . m)-coalgebra
gana : (Corecursive f t, Monad m) => (k : {b : _} -> m (f b) -> f (m b)) -> (g : a -> f (m a)) -> a -> t
gana k g = (gan k g) . pure . g
  where gan : (Corecursive f t, Monad m) => (k : {b : _} -> m (f b) -> f (m b)) -> (g : a -> f (m a)) -> m (f (m a)) -> t
        gan k g x = embed . map ((gan k g) . map g . join) . k $ x

||| Generalized catamorphism
||| @ k A distributive law
||| @ g A (f . w)-algebra
gcata : (Recursive f t, Comonad w) => (k : {b:_} -> f (w b) -> w (f b)) -> (g : f (w a) -> a) -> t -> a
gcata k g = g . extract . (gcat k g)
  where gcat : (Recursive f t, Comonad w) => (k : {b:_} -> f (w b) -> w (f b)) -> (g : f (w a) -> a) -> t -> w (f (w a))
        gcat k g x = k . map (duplicate . map g . (gcat k g)) . project $ x

||| Generalized hylomorphism
||| @ k A distributive law on f
||| @ l A distributive law on l
||| @ f' A (f . w)-algebra
||| @ g' A (f . m)-coalgebra
ghylo : (Functor f, Comonad w, Monad m) =>
        (k : {b:_} -> f (w b) -> w (f b)) ->
        (l : {c:_} -> m (f c) -> f (m c)) ->
        (f' : f (w b) -> b) ->
        (g' : a -> f (m a)) ->
        a -> b
ghylo k l f' g' = extract . (gh k l f' g') . pure where
  gh : (Functor f, Comonad w, Monad m) => (k : {d:_} -> f (w d) -> w (f d)) -> (l : {c:_} -> m (f c) -> f (m c)) -> (f' : f (w b) -> b) -> (g' : a -> f (m a)) -> m a -> w b
  gh k l f' g' x = map f' . k . map (duplicate . (gh k l f' g') . join) . l . map g' $ x

||| Distributive law for catamorphisms
distCata : Functor f => f (Identity a) -> Identity (f a)
distCata = Id . map runIdentity

||| Distributive law for anamorphisms.
distAna : Functor f => Identity (f a) -> f (Identity a)
distAna = map Id . runIdentity

||| Distributive law for futumorphisms.
distFutu : (Functor f) => Free f (f a) -> f (Free f a)
distFutu (Pure fa) = Pure <$> fa
distFutu (Bind as) = Bind <$> (distFutu <$> as)

||| Futumorphism
futu : (Corecursive f t) => (a -> f (Free f a)) -> a -> t
futu = gana distFutu

||| Distributive law for histomorphisms
distHisto : (Functor f) => f (Cofree f a) -> Cofree f (f a)
distHisto = unfold g where
  g as = (extract <$> as, unwrap <$> as)

||| Histomorphism
histo : (Recursive f t) => (f (Cofree f a) -> a) -> t -> a
histo = gcata distHisto

||| Chronomorphism
chrono : Functor f => (f (Cofree f b) -> b) -> (a -> f (Free f a)) -> a -> b
chrono = ghylo distHisto distFutu

||| Catamorphism. Folds a structure. (see [here](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.41.125&rep=rep1&type=pdf))
cata : (Recursive f t) => (f a -> a) -> t -> a
cata f = c
  where c x = f . map c . project $ x

||| Prepromorphism. Fold a structure while applying a natural transformation at each step.
prepro : (Recursive f t, Corecursive f t) => (f t -> f t) -> (f a -> a) -> t -> a
prepro e f = c
  where c x = f . map (c . (cata (embed . e))) . project $ x

||| Catamorphism interweaving two data types.
dicata : (Recursive f b, Recursive f a) => (f (b, a) -> b) -> (f (b, a) -> a) -> b -> a
dicata f g = snd . cata (\x => (f x, g x))

||| Mutumorphism
mutu : (Recursive f t) => (f (a, a) -> a) -> (f (a, a) -> a) -> t -> a
mutu f g x = g . map (\x => (mutu g f x, mutu f g x)) . project $ x

||| Zygomorphism (see [here](http://www.iis.sinica.edu.tw/~scm/pub/mds.pdf) for a neat example)
zygo : (Recursive f t) => (f b -> b) -> (f (b, a) -> a) -> t -> a
zygo f g = snd . cata (\x => (f $ map fst x, g x))

||| Paramorphism
para : (Recursive f t, Corecursive f t) => (f (t, a) -> a) -> t -> a
para f = snd . cata (\x => (embed $ map fst x, f x))

||| Hylomorphism; equivalent to a catamorphism and an anamorphism taken together.
hylo : Functor f => (f b -> b) -> (a -> f a) -> a -> b
hylo f g = h
  where h x = f . map h . g $ x


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.Web.DOM.NonElementParentNode

import API.Web.DOM.Document
import API.Web.DOM.DocumentType
import API.Web.DOM.Element
import API.Web.HTML.Document
import IdrisScript

%access public export
%default total

||| The original specification of NonElementParentNode can be found at
||| https://dom.spec.whatwg.org/#interface-nonelementparentnode
data NonElementParentNode : Type where
  FromDocument : API.Web.DOM.Document.Document _ -> NonElementParentNode

||| Returns the first element within a *node*'s descendatns whose ID is
||| *elm*.
|||
||| @ elm the ID of an element to fetch
getElementById : NonElementParentNode -> (elm : String) -> JS_IO $ Maybe Element
getElementById (FromDocument document) elm = case document of
    (FromHTMLDocument _ (New self)) => getElementById' self elm
    (New _ self)                    => getElementById' self elm
  where
    getElementById' : (ref : JSRef) -> (elm : String) -> JS_IO $ Maybe Element
    getElementById' ref x = join $ elementFromPointer <$>
      jscall "%0.getElementById(%1)" (JSRef -> String -> JS_IO JSRef) ref elm

max_stars_repo_name: blau-io/idris-web

max_issues_repo_name: pierrebeaucamp/idris-dom

max_forks_repo_name: pierrebeaucamp/idris-dom


text:
> module Fraction.LTEProperties

> import Syntax.PreorderReasoning

> import Fraction.Fraction
> import Fraction.BasicOperations
> import Fraction.Predicates
> import Fraction.BasicProperties
> import PNat.PNat
> import PNat.Operations
> import PNat.Properties
> import Nat.LTEProperties
> import Nat.LTProperties
> import Nat.OperationsProperties
> import Nat.Positive

> %default total
> %access export
> -- %access public export

> -- %freeze PNatOperations.toNat

|LTE| is a total preorder:

> ||| LTE is reflexive
> reflexiveLTE : (x : Fraction) -> x `LTE` x
> reflexiveLTE (n, d') = Nat.LTEProperties.reflexiveLTE (n * (toNat d'))

> ||| LTE is transitive
> transitiveLTE : (x, y, z : Fraction) -> x `LTE` y -> y `LTE` z -> x `LTE` z
> transitiveLTE (nx, dx') (ny, dy') (nz, dz') xLTEy yLTEz = s8 where
>   dx : Nat
>   dx = toNat dx'
>   dy : Nat
>   dy = toNat dy'
>   dz : Nat
>   dz = toNat dz'
>   s1    : LTE ((nx * dy) * dz) ((ny * dx) * dz)
>   s1    = monotoneNatMultLTE xLTEy (Nat.LTEProperties.reflexiveLTE dz)
>   s2    : LTE ((ny * dz) * dx) ((nz * dy) * dx)
>   s2    = monotoneNatMultLTE yLTEz (Nat.LTEProperties.reflexiveLTE dx)
>   s3    : LTE ((ny * dx) * dz) ((nz * dy) * dx)
>   s3    = replace {P = \ ZUZ => LTE ZUZ ((nz * dy) * dx)} (multSwapRight ny dz dx) s2
>   s4    : LTE ((nx * dy) * dz) ((nz * dy) * dx)
>   s4    = Nat.LTEProperties.transitiveLTE ((nx * dy) * dz)
>                                           ((ny * dx) * dz)
>                                           ((nz * dy) * dx)
>                                           s1 s3
>   s5    : LTE ((nx * dz) * dy) ((nz * dy) * dx)
>   s5    = replace {P = \ ZUZ => LTE ZUZ ((nz * dy) * dx)} (multSwapRight nx dy dz) s4
>   s6    : LTE ((nx * dz) * dy) ((nz * dx) * dy)
>   s6    = replace {P = \ ZUZ => LTE ((nx * dz) * dy) ZUZ} (multSwapRight nz dy dx) s5
>   s7    : LTE (nx * dz) (nz * dx)
>   s7    = elimRightMultLTE {a = nx * dz} {b = nz * dx} {c = dy} {d = dy}
>                            s6 Refl (gtZisnotZ (denLTLemma (ny, dy')))
>   s8 : (nx, dx') `LTE` (nz, dz')
>   s8 = s7

> ||| LTE is total
> totalLTE : (x, y : Fraction) -> Either (x `LTE` y) (y `LTE` x)
> totalLTE (n1, d1') (n2, d2') =
>   let d1 = toNat d1' in
>   let d2 = toNat d2' in
>   Nat.LTEProperties.totalLTE (n1 * d2) (n2 * d1)

Properties of |LTE| and |plus|:

> ||| LTE is monotone w.r.t. `plus`
> monotonePlusLTE : {a, b, c, d : Fraction} ->
>                   a `LTE` b -> c `LTE` d -> (a `plus` c) `LTE` (b `plus` d)
> monotonePlusLTE {a = (na, da')} {b = (nb, db')} {c = (nc, dc')} {d = (nd, dd')} aLTEb cLTEd = s16 where
>   da : Nat
>   da = toNat da'
>   db : Nat
>   db = toNat db'
>   dc : Nat
>   dc = toNat dc'
>   dd : Nat
>   dd = toNat dd'
>   s1 : LTE (na * db) (nb * da)
>   s1 = aLTEb
>   s2 : LTE (nc * dd) (nd * dc)
>   s2 = cLTEd
>   s3 : LTE ((na * db) * (dc * dd)) ((nb * da) * (dc * dd))
>   s3 = monotoneNatMultLTE s1 (Nat.LTEProperties.reflexiveLTE (dc * dd))
>   s4 : LTE ((nc * dd) * (da * db)) ((nd * dc) * (da * db))
>   s4 = monotoneNatMultLTE s2 (Nat.LTEProperties.reflexiveLTE (da * db))
>   s5 : LTE ((na * db) * (dc * dd) + (nc * dd) * (da * db))
>            ((nb * da) * (dc * dd) + (nd * dc) * (da * db))
>   s5 = monotoneNatPlusLTE s3 s4
>   s6 : LTE ((na * dc) * (db * dd) + (nc * dd) * (da * db))
>            ((nb * da) * (dc * dd) + (nd * dc) * (da * db))
>   s6 = replace {P = \ ZUZ => LTE (         ZUZ          + (nc * dd) * (da * db))
>                                  ((nb * da) * (dc * dd) + (nd * dc) * (da * db))}
>                (multSwap23 na db dc dd) s5
>   s7 : LTE ((na * dc) * (db * dd) + (nc * da) * (dd * db))
>            ((nb * da) * (dc * dd) + (nd * dc) * (da * db))
>   s7 = replace {P = \ ZUZ => LTE ((na * dc) * (db * dd) +          ZUZ         )
>                                  ((nb * da) * (dc * dd) + (nd * dc) * (da * db))}
>                (multSwap23 nc dd da db) s6
>   s8 : LTE ((na * dc) * (db * dd) + (nc * da) * (dd * db))
>            ((nb * dd) * (dc * da) + (nd * dc) * (da * db))
>   s8 = replace {P = \ ZUZ => LTE ((na * dc) * (db * dd) + (nc * da) * (dd * db))
>                                  (         ZUZ          + (nd * dc) * (da * db))}
>                (multSwap24 nb da dc dd) s7
>   s9 : LTE ((na * dc) * (db * dd) + (nc * da) * (dd * db))
>            ((nb * dd) * (dc * da) + (nd * db) * (da * dc))
>   s9 = replace {P = \ ZUZ => LTE ((na * dc) * (db * dd) + (nc * da) * (dd * db))
>                                  ((nb * dd) * (dc * da) +          ZUZ         )}
>                (multSwap24 nd dc da db) s8
>   s10 : LTE ((na * dc) * (db * dd) + (nc * da) * (db * dd))
>             ((nb * dd) * (dc * da) + (nd * db) * (da * dc))
>   s10 = replace {P = \ ZUZ => LTE ((na * dc) * (db * dd) + (nc * da) *    ZUZ   )
>                                   ((nb * dd) * (dc * da) + (nd * db) * (da * dc))}
>                 (multCommutative dd db) s9
>   s11 : LTE ((na * dc) * (db * dd) + (nc * da) * (db * dd))
>             ((nb * dd) * (da * dc) + (nd * db) * (da * dc))
>   s11 = replace {P = \ ZUZ => LTE ((na * dc) * (db * dd) + (nc * da) * (db * dd))
>                                   ((nb * dd) *    ZUZ    + (nd * db) * (da * dc))}
>                 (multCommutative dc da) s10
>   s12 : LTE ((na * dc + nc * da) * (db * dd))
>             ((nb * dd) * (da * dc) + (nd * db) * (da * dc))
>   s12 = replace {P = \ ZUZ => LTE ZUZ ((nb * dd) * (da * dc) + (nd * db) * (da * dc))}
>                 (sym (multDistributesOverPlusLeft (na * dc) (nc * da) (db * dd))) s11
>   s13 : LTE ((na * dc + nc * da) * (db * dd)) ((nb * dd + nd * db) * (da * dc))
>   s13 = replace {P = \ ZUZ => LTE (((na * dc) + (nc * da)) * (db * dd)) ZUZ}
>                 (sym (multDistributesOverPlusLeft (nb * dd) (nd * db) (da * dc))) s12
>   s14 : LTE ((na * dc + nc * da) * (toNat (db' * dd'))) ((nb * dd + nd * db) * (da * dc))
>   s14 = replace {P = \ ZUZ => LTE ((na * dc + nc * da) * ZUZ) ((nb * dd + nd * db) * (da * dc))}
>                 (sym toNatMultLemma) s13
>   s15 : LTE ((na * dc + nc * da) * (toNat (db' * dd'))) ((nb * dd + nd * db) * (toNat (da' * dc')))
>   s15 = replace {P = \ ZUZ => LTE ((na * dc + nc * da) * (toNat (db' * dd'))) ((nb * dd + nd * db) * ZUZ)}
>                 (sym toNatMultLemma) s14
>   s16 : ((na, da') `plus` (nc, dc')) `LTE` ((nb, db') `plus` (nd, dd'))
>   s16 = s15

Properties of |LTE| and |mult|:

> ||| LTE is monotone w.r.t. `(*)`
> monotoneMultLTE : {a, b, c, d : Fraction} ->
>                   a `LTE` b -> c `LTE` d -> (a `mult` c) `LTE` (b `mult` d)
> monotoneMultLTE {a = (na, da')} {b = (nb, db')} {c = (nc, dc')} {d = (nd, dd')} aLTEb cLTEd = s13 where
>   da : Nat
>   da = toNat da'
>   db : Nat
>   db = toNat db'
>   dc : Nat
>   dc = toNat dc'
>   dd : Nat
>   dd = toNat dd'
>   s01 : LTE (na * db) (nb * da)
>   s01 = aLTEb
>   s02 : LTE (nc * dd) (nd * dc)
>   s02 = cLTEd
>   s03 : LTE ((na * db) * (nc * dd)) ((nb * da) * (nc * dd))
>   s03 = monotoneNatMultLTE s01 (Nat.LTEProperties.reflexiveLTE (nc * dd))
>   s04 : LTE ((nc * dd) * (da * nb)) ((nd * dc) * (da * nb))
>   s04 = monotoneNatMultLTE s02 (Nat.LTEProperties.reflexiveLTE (da * nb))
>   s05 : LTE ((da * nb) * (nc * dd)) ((nd * dc) * (da * nb))
>   s05 = replace {P = \ ZUZ => LTE ZUZ ((nd * dc) * (da * nb))}
>                 (multCommutative (nc * dd) (da * nb)) s04
>   s06 : LTE ((nb * da) * (nc * dd)) ((nd * dc) * (da * nb))
>   s06 = replace {P = \ ZUZ => LTE (ZUZ * (nc * dd)) ((nd * dc) * (da * nb))}
>                 (multCommutative da nb) s05
>   s07 : LTE ((na * db) * (nc * dd)) ((nd * dc) * (da * nb))
>   s07 = Nat.LTEProperties.transitiveLTE ((na * db) * (nc * dd)) ((nb * da) * (nc * dd)) ((nd * dc) * (da * nb)) s03 s06
>   s08 : LTE ((na * nc) * (db * dd)) ((nd * dc) * (da * nb))
>   s08 = replace {P = \ ZUZ => LTE ZUZ ((nd * dc) * (da * nb))}
>                 (multSwap23 na db nc dd) s07
>   s09 : LTE ((na * nc) * (db * dd)) ((nd * nb) * (da * dc))
>   s09 = replace {P = \ ZUZ => LTE ((na * nc) * (db * dd)) ZUZ}
>                 (multSwap24 nd dc da nb) s08
>   s10 : LTE ((na * nc) * (db * dd)) ((nb * nd) * (da * dc))
>   s10 = replace {P = \ ZUZ => LTE ((na * nc) * (db * dd)) (ZUZ * (da * dc))}
>                 (multCommutative nd nb) s09
>   s11 : LTE ((na * nc) * (toNat (db' * dd'))) ((nb * nd) * (da * dc))
>   s11 = replace {P = \ ZUZ => LTE ((na * nc) * ZUZ) ((nb * nd) * (da * dc))}
>                 (sym toNatMultLemma) s10
>   s12 : LTE ((na * nc) * (toNat (db' * dd'))) ((nb * nd) * (toNat (da' * dc')))
>   s12 = replace {P = \ ZUZ => LTE ((na * nc) * (toNat (db' * dd'))) ((nb * nd) * ZUZ)}
>                 (sym toNatMultLemma) s11
>   s13 : ((na, da') `mult` (nc, dc')) `LTE` ((nb, db') `mult` (nd, dd'))
>   s13 = s12

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Data.AOC19.Day05

import Data.Fin
import Data.Vect
import Effects

total
slice : (i, n : Nat) -> Vect (i + (n + m)) a -> Vect n a
slice i n = take n . drop i

namespace IntCode
  data State : Type where
    Running : {n : Nat} -> (ptr : Fin n) -> (state : Vect n Int) -> State
    NotRunning : State

  data ParameterMode
    = PositionMode
    | ImmediateMode

  data OpCode
    = ADD
    | MUL
    | SET
    | PRN
    | END

  data Program : State -> Type where
    Halted : Program NotRunning
    MkP : (ptr : Fin n) -> (state : Vect n Int) -> Program (Running ptr state)

  data Instruction : Effect where
    Add : sig Instruction (Vect (S (S (S (S k)))) Int)
              (Program (Running ptr state))
              (\state' => Program (Running (shift 4 ptr) state'))

  Handler Instruction m where
    handle (MkP (ptr state {n=S (S (S (S j)))}) Add k =
      let dst = Vect.index (shift 3 ptr) state in
      ?rhs_1

-- program :: Parser (Vector Int)
-- program = fromList . map fromInteger <$> (natural `sepBy` comma)

-- runProgram :: Vector Int -> Vector Int
-- runProgram = go 0
--   where
--     go n state
--       | state ! n == 99 = state
--       | otherwise       = go (n + 4) $ step (toList (V.slice n 4 state))
--       where
--         step [1, x, y, dst] = modify (runOp (+) x y dst) state
--         step [2, x, y, dst] = modify (runOp (*) x y dst) state
--         step _              = state

--     runOp f x y dst v = write v dst =<< f <$> MV.read v x <*> MV.read v y

-- example1 :: Vector Int
-- example1 =
--     case parseString program mempty "1,9,10,3,2,3,11,0,99,30,40,50" of
--       Success prog   -> prog
--       Failure reason -> error (show reason)

max_stars_repo_name: yurrriq/advent-of-code


text:
module Syntax.PreorderReasoning.Generic

import Control.Relation
import Control.Order
infixl 0  ~~
infixl 0  <~
prefix 1  |~
infix  1  ...

public export
data Step : (leq : a -> a -> Type) -> a -> a -> Type where
  (...) : (y : a) -> x `leq` y -> Step leq x y

public export
data FastDerivation : (leq : a -> a -> Type) -> (x : a) -> (y : a) -> Type where
  (|~) : (x : a) -> FastDerivation leq x x
  (<~) : {x, y : a}
         -> FastDerivation leq x y -> {z : a} -> (step : Step leq y z)
         -> FastDerivation leq x z

public export
CalcWith : Preorder dom leq => {0 x : dom} -> {0 y : dom} -> FastDerivation leq x y -> x `leq` y
CalcWith (|~ x) = reflexive {rel = leq}
CalcWith ((<~) der (z ... step)) = transitive {rel = leq} (CalcWith der) step

public export
(~~) : {0 x : dom} -> {0 y : dom}
         -> FastDerivation leq x y -> {z : dom} -> (step : Step Equal y z)
         -> FastDerivation leq x z
(~~) der (z ... Refl) = der


text:
module SlideWise

import Data.Vect

public export data SlideWise2: Vect (S (S n)) e -> (Vect 2 e -> Type) -> Type where
  HeadMatches2: (searched: Vect (S (S m)) e) -> (match: Vect 2 e) -> (rest:Vect m e) -> prf match  -> SlideWise2 (match++rest) prf
  RestMatches2: (x:e) -> (rest: Vect (S (S n)) e) -> SlideWise2 rest prf -> SlideWise2 (x::rest) prf

export getMatchAndRest2: (xs: Vect (S (S n)) e) -> (prf: SlideWise2 xs prfT) -> (Vect 2 e, Vect n e)
getMatchAndRest2 (match ++ rest) (HeadMatches2 searched match rest x) = (match, rest)
getMatchAndRest2 (x :: rest) (RestMatches2 x rest prf) = let (match, rest') = getMatchAndRest2 rest prf in
                                                                 (match, x::rest')

export getRest2: (xs: Vect (S (S n)) e) -> (prf: SlideWise2 xs prfT) -> Vect n e
getRest2 (match ++ rest) (HeadMatches2 searched match rest x) = rest
getRest2 (x :: rest) (RestMatches2 x rest prf) = x::(getRest2 rest prf)

export getMatch2: (xs: Vect (S (S n)) e) -> (prf: SlideWise2 xs prfT) -> Vect 2 e
getMatch2 (match ++ rest) (HeadMatches2 searched match rest x) = match
getMatch2 (x :: rest) (RestMatches2 x rest prf) = getMatch2 rest prf

reachedEnd2 : (contra : prfT ([x1, x2]) -> Void) -> SlideWise2 [x1, x2] prfT -> Void
reachedEnd2 contra (HeadMatches2 sorted (x1:: x2 :: []) [] prf) = contra prf

notInHeadOrRest2 : (contra : SlideWise2 (x2 :: (x3 :: xs)) prfT -> Void) -> (head_contra : prfT [x1, x2] -> Void) -> SlideWise2 (x1 :: (x2 :: (x3 :: xs))) prfT -> Void
notInHeadOrRest2 contra head_contra (RestMatches2 x1 (x2 :: (x3 :: xs)) x) = contra x

export isSlideWise2: (xs: Vect (S (S n)) e) -> (prfFun: (y:Vect 2 e) -> Dec (prfT y)) -> Dec (SlideWise2 xs prfT)
isSlideWise2 {n = Z} (x1 :: x2:: []) prfFun = case prfFun [x1, x2] of
                                                (Yes prf) => Yes (HeadMatches2 [x1, x2] [x1, x2] [] prf)
                                                (No contra) => No (reachedEnd2 contra)
isSlideWise2 {n = (S k)} (x1 :: x2 :: x3 :: xs) prfFun = case prfFun [x1, x2] of
                                                              (Yes prf) => Yes (HeadMatches2 (x1 :: x2 :: x3 :: xs) [x1, x2] (x3::xs) prf)
                                                              (No head_contra) => (case isSlideWise2 (x2::x3::xs) prfFun of
                                                                                (Yes prf) => Yes (RestMatches2 x1 (x2::x3::xs) prf)
                                                                                (No contra) => No (notInHeadOrRest2 contra head_contra))

public export data SlideWise3: Vect (S (S (S n))) e -> (Vect 3 e -> Type) -> Type where
 HeadMatches3: (searched: Vect (S (S (S m))) e) -> (match: Vect 3 e) -> (rest:Vect m e) -> prf match  -> SlideWise3 (match++rest) prf
 RestMatches3: (x:e) -> (rest: Vect (S (S (S n))) e) -> SlideWise3 rest prf -> SlideWise3 (x::rest) prf

export getMatchAndRest3:(xs: Vect (S (S (S n))) e) -> (prf: SlideWise3 xs prfT) -> (Vect 3 e, Vect n e)
getMatchAndRest3 (match ++ rest) (HeadMatches3 searched match rest x) = (match, rest)
getMatchAndRest3 (x :: rest) (RestMatches3 x rest prf) = let (match, rest') = getMatchAndRest3 rest prf in
                                                                (match, x::rest')

export getRest3: (xs: Vect (S (S (S n))) e) -> (prf: SlideWise3 xs prfT) -> Vect n e
getRest3 (match ++ rest) (HeadMatches3 searched match rest x) = rest
getRest3 (x :: rest) (RestMatches3 x rest prf) = let rest' = getRest3 rest prf in
                                                                x::rest'

export getMatch3:(xs: Vect (S (S (S n))) e) -> (prf: SlideWise3 xs prfT) -> Vect 3 e
getMatch3 (match ++ rest) (HeadMatches3 searched match rest x) = match
getMatch3 (x :: rest) (RestMatches3 x rest prf) = let match = getMatch3 rest prf in
                                                            match

reachedEnd3 : (contra : prfT [x1, x2, x3] -> Void) -> SlideWise3 [x1, x2, x3] prfT -> Void
reachedEnd3 contra (HeadMatches3 sorted (x1:: x2 :: x3 :: []) [] prf) = contra prf

notInHeadOrRest3 : (contra : SlideWise3 (x2 :: (x3 :: (x4 :: xs))) prfT -> Void) -> (head_contra : prfT [x1, x2, x3] -> Void) -> SlideWise3 (x1 :: (x2 :: (x3 :: (x4 :: xs)))) prfT -> Void
notInHeadOrRest3 contra head_contra (RestMatches3 x1 (x2 :: (x3 :: (x4 :: xs))) x) = contra x

export isSlideWise3: (xs: Vect (S (S (S n))) e) -> (prfFun: (y:Vect 3 e) -> Dec (prfT y)) -> Dec (SlideWise3 xs prfT)
isSlideWise3 {n = Z} (x1::x2::x3::[]) prfFun = case prfFun [x1, x2, x3] of
                                                    (Yes prf) => Yes (HeadMatches3 [x1, x2, x3] [x1, x2, x3] [] prf)
                                                    (No contra) => No (reachedEnd3 contra)
isSlideWise3 {n = (S k)} (x1::x2::x3::x4::xs) prfFun = case prfFun [x1, x2, x3] of
                                          (Yes prf) => Yes (HeadMatches3 (x1::x2::x3::x4::xs) [x1, x2, x3] (x4::xs) prf)
                                          (No head_contra) => (case isSlideWise3 (x2::x3::x4::xs) prfFun of
                                                               (Yes prf) => Yes (RestMatches3 x1 (x2::x3::x4::xs) prf)
                                                               (No contra) => No (notInHeadOrRest3 contra head_contra))

public export data SlideWise4: Vect (S (S (S (S n)))) e -> (Vect 4 e -> Type) -> Type where
  HeadMatches4: (searched: Vect (S (S (S (S m)))) e) -> (match: Vect 4 e) -> (rest:Vect m e) -> prf match  -> SlideWise4 (match++rest) prf
  RestMatches4: (x:e) -> (rest: Vect (S (S (S (S n)))) e) -> SlideWise4 rest prf -> SlideWise4 (x::rest) prf

export getMatchAndRest4:(xs: Vect (S (S (S (S n)))) e) -> (prf: SlideWise4 xs prfT) -> (Vect 4 e, Vect n e)
getMatchAndRest4 (match ++ rest) (HeadMatches4 searched match rest x) = (match, rest)
getMatchAndRest4 (x :: rest) (RestMatches4 x rest prf) = let (match, rest') = getMatchAndRest4 rest prf in
                                                               (match, x::rest')

reachedEnd4 : (contra : prfT (x1::x2::x3::x4::[]) -> Void) -> SlideWise4 (x1::x2::x3::x4::[]) prfT -> Void
reachedEnd4 contra (HeadMatches4 sorted (x1::x2::x3::x4::[]) [] prf) = contra prf

notInHeadOrRest4 : (contra : SlideWise4 (x2 :: (x3 :: (x4 :: (x5 :: xs)))) prfT -> Void) -> (head_contra : prfT [x1, x2, x3, x4] -> Void) -> SlideWise4 (x1 :: (x2 :: (x3 :: (x4 :: (x5 :: xs))))) prfT -> Void
notInHeadOrRest4 contra head_contra (RestMatches4 x1 (x2 :: (x3 :: (x4 :: (x5 :: xs)))) x) = contra x

export isSlideWise4: (xs: Vect (S (S (S (S n)))) e) -> (prfFun: (y:Vect 4 e) -> Dec (prfT y)) -> Dec (SlideWise4 xs prfT)
isSlideWise4 {n = Z} (x1::x2::x3::x4::[]) prfFun = case prfFun [x1, x2, x3, x4] of
                                                   (Yes prf) => Yes (HeadMatches4 [x1, x2, x3, x4] [x1, x2, x3, x4] [] prf)
                                                   (No contra) => No (reachedEnd4 contra)
isSlideWise4 {n = (S k)} (x1::x2::x3::x4::x5::xs) prfFun = case prfFun [x1, x2, x3, x4] of
                                         (Yes prf) => Yes (HeadMatches4 (x1::x2::x3::x4::x5::xs) [x1, x2, x3, x4] (x5::xs) prf)
                                         (No head_contra) => (case isSlideWise4 (x2::x3::x4::x5::xs) prfFun of
                                                              (Yes prf) => Yes (RestMatches4 x1 (x2::x3::x4::x5::xs) prf)
                                                              (No contra) => No (notInHeadOrRest4 contra head_contra))


text:
module Lens.Util

import Data.List
import Data.Maybe
import Lens
import Lens.Uninhabited
import Map

%default total

public export
beq_prim : (v : PrimitiveValue) ->  v == v = True
beq_prim (Boolean b) = beq_bool b
beq_prim (Number n) = beq_nat n
beq_prim (Text t) = beq_str t

public export
beq_prim2 : (v1, v2 : PrimitiveValue) -> (v1 == v2 = True) -> v1 = v2
beq_prim2 (Boolean x) (Boolean y) prf = rewrite eq_bool x y prf in Refl
beq_prim2 (Boolean _) (Number _) Refl impossible
beq_prim2 (Boolean _) (Text _) Refl impossible
beq_prim2 (Number _) (Boolean _) Refl impossible
beq_prim2 (Number k) (Number j) prf = rewrite eq_nat k j prf in Refl
beq_prim2 (Number _) (Text _) Refl impossible
beq_prim2 (Text _) (Boolean _) Refl impossible
beq_prim2 (Text _) (Number _) Refl impossible
beq_prim2 (Text xs) (Text ys) prf = rewrite eq_str xs ys prf in Refl

public export
neq_prim : (v1, v2 : PrimitiveValue) -> (v1 == v2 = False) -> Not (v1 = v2)
neq_prim (Boolean x) (Boolean y) prf =
    neq_bool x y prf . justInjective . cong boolean
neq_prim (Boolean x) (Number k) prf = uninhabited
neq_prim (Boolean x) (Text xs) prf = uninhabited
neq_prim (Number k) (Boolean x) prf = uninhabited
neq_prim (Number k) (Number j) prf =
    neq_nat k j prf . justInjective . cong number
neq_prim (Number k) (Text xs) prf = uninhabited
neq_prim (Text xs) (Boolean x) prf = uninhabited
neq_prim (Text xs) (Number k) prf = uninhabited
neq_prim (Text xs) (Text ys) prf =
    neq_str xs ys prf . justInjective . cong text

beq_prim_kind : (k1, k2 : PrimitiveKind) -> (k1 == k2 = True) ->  k1 = k2
beq_prim_kind KBoolean KBoolean prf = Refl
beq_prim_kind KBoolean KNumber Refl impossible
beq_prim_kind KBoolean KText Refl impossible
beq_prim_kind KNumber KBoolean Refl impossible
beq_prim_kind KNumber KNumber prf = Refl
beq_prim_kind KNumber KText Refl impossible
beq_prim_kind KText KBoolean Refl impossible
beq_prim_kind KText KNumber Refl impossible
beq_prim_kind KText KText prf = Refl

public export
validate_properties_after_insert : (vm : Map Value) -> (sm : Map Schema) ->
    (k : Key) -> (v : Value) -> (s : Schema) -> validate s v = True ->
    validate_properties vm sm = True -> validate_properties (insert k v vm) (insert k s sm) = True

public export
validate_properties_after_remove : (vm : Map Value) -> (sm : Map Schema) -> (k : Key) ->
    validate_properties vm sm = True -> validate_properties (remove k vm) (remove k sm) = True

public export
invalid_property : (vm : Map Value) -> (sm : Map Schema) -> (k : Key) ->
    (v : Value) -> (s : Schema) -> get k vm = Just v -> get k sm = Just s -> validate s v = False ->
    validate_properties vm sm = False

public export
still_valid : (vm : Map Value) -> (sm : Map Schema) ->
    (k : Key) -> (kvm : Value) -> (ksm : Schema) ->
    get k vm = Just kvm -> get k sm = Just ksm ->
    validate_properties vm sm = True -> validate ksm kvm = True

public export
still_invalid : (vm : Map Value) -> (sm : Map Schema) ->
    (k : Key) ->  get k vm = Just kvm -> get k sm = Just ksm ->
    validate ksm kvm = False -> validate_properties vm sm = False

public export
flip_map_twice : (m : List (PrimitiveValue, PrimitiveValue)) -> flip_map (flip_map m) = m
flip_map_twice [] = Refl
flip_map_twice ((x, y) :: xs) = rewrite flip_map_twice xs in Refl

public export
flip_map_preserves_validity : (a, b : PrimitiveKind) -> (m : List (PrimitiveValue, PrimitiveValue)) ->
    validate_map a b m = True -> validate_map b a (flip_map m) = True
flip_map_preserves_validity a b [] prf = Refl
flip_map_preserves_validity a b ((x, y) :: xs) prf =
    let sprf = and_split (prim_kind_of x == a) (prim_kind_of y == b && Delay (validate_map a b xs)) prf
        sprf2 = and_split (prim_kind_of y == b) (validate_map a b xs) (snd sprf)
        ind = flip_map_preserves_validity a b xs (snd sprf2)
    in rewrite fst sprf2 in rewrite fst sprf in ind

validate_map_kind_a : (m : List (PrimitiveValue, PrimitiveValue)) -> (a, b : PrimitiveKind) -> (va : PrimitiveValue) ->
    (va, vb) :: _ = m -> validate_map a b m = True -> prim_kind_of va = a
validate_map_kind_a [] _ _ _ Refl _ impossible
validate_map_kind_a ((va, vb) :: m) KBoolean b (Number _) prf prf1 =
    let split = and_split (prim_kind_of va == KBoolean) (prim_kind_of vb == b && validate_map KBoolean b m) prf1
        xeq = cong prim_kind_of $ cong fst $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of va) KBoolean (fst split)
    in absurd $ trans xeq xeq2
validate_map_kind_a ((va, vb) :: m) KBoolean b (Text _) prf prf1 =
    let split = and_split (prim_kind_of va == KBoolean) (prim_kind_of vb == b && validate_map KBoolean b m) prf1
        xeq = cong prim_kind_of $ cong fst $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of va) KBoolean (fst split)
    in absurd $ trans xeq xeq2
validate_map_kind_a ((va, vb) :: m) KNumber b (Boolean _) prf prf1 =
    let split = and_split (prim_kind_of va == KNumber) (prim_kind_of vb == b && validate_map KNumber b m) prf1
        xeq = cong prim_kind_of $ cong fst $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of va) KNumber (fst split)
    in absurd $ trans xeq xeq2
validate_map_kind_a ((va, vb) :: m) KNumber b (Text _) prf prf1 =
    let split = and_split (prim_kind_of va == KNumber) (prim_kind_of vb == b && validate_map KNumber b m) prf1
        xeq = cong prim_kind_of $ cong fst $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of va) KNumber (fst split)
    in absurd $ trans xeq xeq2
validate_map_kind_a ((va, vb) :: m) KText b (Boolean _) prf prf1 =
    let split = and_split (prim_kind_of va == KText) (prim_kind_of vb == b && validate_map KText b m) prf1
        xeq = cong prim_kind_of $ cong fst $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of va) KText (fst split)
    in absurd $ trans xeq xeq2
validate_map_kind_a ((va, vb) :: m) KText b (Number _) prf prf1 =
    let split = and_split (prim_kind_of va == KText) (prim_kind_of vb == b && validate_map KText b m) prf1
        xeq = cong prim_kind_of $ cong fst $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of va) KText (fst split)
    in absurd $ trans xeq xeq2
validate_map_kind_a ((_, _) :: _) KBoolean _ (Boolean _) prf prf1 = Refl
validate_map_kind_a ((_, _) :: _) KNumber _ (Number _) prf prf1 = Refl
validate_map_kind_a ((_, _) :: _) KText _ (Text _) prf prf1 = Refl

validate_map_kind_b : (m : List (PrimitiveValue, PrimitiveValue)) -> (a, b : PrimitiveKind) -> (vb : PrimitiveValue) ->
    (va, vb) :: _ = m -> validate_map a b m = True -> prim_kind_of vb = b
validate_map_kind_b [] _ _ _ Refl _ impossible
validate_map_kind_b ((va, vb) :: m) a KBoolean (Number _) prf prf1 =
    let split = and_split (prim_kind_of va == a) (prim_kind_of vb == KBoolean && validate_map a KBoolean m) prf1
        split2 = and_split (prim_kind_of vb == KBoolean) (validate_map a KBoolean m) (snd split)
        xeq = cong prim_kind_of $ cong snd $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of vb) KBoolean (fst split2)
    in absurd $ trans xeq xeq2
validate_map_kind_b ((va, vb) :: m) a KBoolean (Text _) prf prf1 =
    let split = and_split (prim_kind_of va == a) (prim_kind_of vb == KBoolean && validate_map a KBoolean m) prf1
        split2 = and_split (prim_kind_of vb == KBoolean) (validate_map a KBoolean m) (snd split)
        xeq = cong prim_kind_of $ cong snd $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of vb) KBoolean (fst split2)
    in absurd $ trans xeq xeq2
validate_map_kind_b ((va, vb) :: m) a KNumber (Boolean _) prf prf1 =
    let split = and_split (prim_kind_of va == a) (prim_kind_of vb == KNumber && validate_map a KNumber m) prf1
        split2 = and_split (prim_kind_of vb == KNumber) (validate_map a KNumber m) (snd split)
        xeq = cong prim_kind_of $ cong snd $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of vb) KNumber (fst split2)
    in absurd $ trans xeq xeq2
validate_map_kind_b ((va, vb) :: m) a KNumber (Text _) prf prf1 =
    let split = and_split (prim_kind_of va == a) (prim_kind_of vb == KNumber && validate_map a KNumber m) prf1
        split2 = and_split (prim_kind_of vb == KNumber) (validate_map a KNumber m) (snd split)
        xeq = cong prim_kind_of $ cong snd $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of vb) KNumber (fst split2)
    in absurd $ trans xeq xeq2
validate_map_kind_b ((va, vb) :: m) a KText (Boolean _) prf prf1 =
    let split = and_split (prim_kind_of va == a) (prim_kind_of vb == KText && validate_map a KText m) prf1
        split2 = and_split (prim_kind_of vb == KText) (validate_map a KText m) (snd split)
        xeq = cong prim_kind_of $ cong snd $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of vb) KText (fst split2)
    in absurd $ trans xeq xeq2
validate_map_kind_b ((va, vb) :: m) a KText (Number _) prf prf1 =
    let split = and_split (prim_kind_of va == a) (prim_kind_of vb == KText && validate_map a KText m) prf1
        split2 = and_split (prim_kind_of vb == KText) (validate_map a KText m) (snd split)
        xeq = cong prim_kind_of $ cong snd $ fst $ consInjective prf
        xeq2 = beq_prim_kind (prim_kind_of vb) KText (fst split2)
    in absurd $ trans xeq xeq2
validate_map_kind_b ((va, vb) :: m) _ KBoolean (Boolean _) prf prf1 = Refl
validate_map_kind_b ((va, vb) :: m) _ KNumber (Number _) prf prf1 = Refl
validate_map_kind_b ((va, vb) :: m) _ KText (Text _) prf prf1 = Refl

validate_map_kind : (m : List (PrimitiveValue, PrimitiveValue)) -> (a, b : PrimitiveKind) ->
    (va, vb : PrimitiveValue) -> (va, vb) :: _ = m -> validate_map a b m = True ->
    (prim_kind_of va = a, prim_kind_of vb = b)
validate_map_kind m a b va vb prf prf1 =
    let pa = validate_map_kind_a m a b va prf prf1
        pb = validate_map_kind_b m a b vb prf prf1
    in (pa, pb)

map_still_valid : (m : List (PrimitiveValue, PrimitiveValue)) -> (a, b : PrimitiveKind) ->
    (x :: xs) = m -> validate_map a b m = True -> validate_map a b xs = True
map_still_valid [] _ _ Refl _ impossible
map_still_valid ((va, vb) :: m) a b prf prf1 with (prim_kind_of va == a, prim_kind_of vb == b) proof prf2
    map_still_valid ((va, vb) :: m) a b prf prf1 | (False, _) =
        let split = and_split (prim_kind_of va == a) (prim_kind_of vb == b && validate_map a b m) prf1
        in absurd $ trans (sym $ cong fst prf2) (fst split)
    map_still_valid ((va, vb) :: m) a b prf prf1 | (True, False) =
        let split = and_split (prim_kind_of va == a) (prim_kind_of vb == b && validate_map a b m) prf1
            split2 = and_split (prim_kind_of vb == b) (validate_map a b m) (snd split)
        in absurd $ trans (sym $ cong snd prf2) (fst split2)
    map_still_valid ((va, vb) :: m) a b prf prf1 | (True, True) =
        let split = and_split (prim_kind_of va == a) (prim_kind_of vb == b && validate_map a b m) prf1
            split2 = and_split (prim_kind_of vb == b) (validate_map a b m) (snd split)
        in rewrite snd $ consInjective prf in snd split2

public export
convert_prim_kind : (m : List (PrimitiveValue, PrimitiveValue)) ->
    (a, b : PrimitiveKind) -> (va, vb : PrimitiveValue) ->
    validate_map a b m = True -> prim_kind_of va = a ->
    convert_prim va m = Just vb -> prim_kind_of vb = b
convert_prim_kind [] _ _ _ _ _ _ Refl impossible
convert_prim_kind ((va', vb') :: m) a b va vb prf prf1 prf2 with (va == va') proof prf3
    convert_prim_kind ((va', vb') :: m) a b va vb prf prf1 prf2 | True =
        rewrite sym $ justInjective prf2 in
            snd $ validate_map_kind ((va', vb') :: m) a b va' vb' Refl prf
    convert_prim_kind ((va', vb') :: m) a b va vb prf prf1 prf2 | False =
        let sv = map_still_valid ((va', vb') :: m) a b Refl prf
            ind = convert_prim_kind m a b va vb sv prf1 prf2
        in ind

max_stars_repo_name: Actyx/cambria

max_issues_repo_name: Actyx/cambria

max_forks_repo_name: Actyx/cambria


text:
module Main

import Data.Vect

data Cat = Cas | Luna | Sherlock

f : (cat: Cat) -> String

getName : (cat: Cat) -> String
getName Cas = "Cas"
getName Luna = "Luna"
getName Sherlock = "Sherlock"

plusTwo : (n: Nat) -> Nat
plusTwo n = ?plusTwo_rhs

g : (n: Nat) -> (b: Bool) -> String
g n b = ?g_rhs

num : Nat
num = ?n_rhs

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


text:
module Text.WebIDL.Types.Attribute

import Data.List1
import Data.SOP
import Text.WebIDL.Types.Numbers
import Text.WebIDL.Types.StringLit
import Text.WebIDL.Types.Identifier
import Text.WebIDL.Types.Symbol

import Generics.Derive

%language ElabReflection

public export
isParenOrQuote : Char -> Bool
isParenOrQuote '(' = True
isParenOrQuote ')' = True
isParenOrQuote '[' = True
isParenOrQuote ']' = True
isParenOrQuote '{' = True
isParenOrQuote '}' = True
isParenOrQuote '"' = True
isParenOrQuote _   = False

public export
isCommaOrParenOrQuote : Char -> Bool
isCommaOrParenOrQuote ',' = True
isCommaOrParenOrQuote c   = isParenOrQuote c

public export
0 Other : Type
Other = NS I [IntLit,FloatLit,StringLit,Identifier,Keyword,Symbol]

||| ExtendedAttributeInner ::
public export
data EAInner : Type where
  |||   ( ExtendedAttributeInner ) ExtendedAttributeInner
  |||   [ ExtendedAttributeInner ] ExtendedAttributeInner
  |||   { ExtendedAttributeInner } ExtendedAttributeInner
  EAIParens : (inParens : EAInner) -> (eai : EAInner) -> EAInner

  |||   OtherOrComma ExtendedAttributeInner
  EAIOther  : (otherOrComma : Other) -> (eai : EAInner) -> EAInner

  |||   ε
  EAIEmpty  : EAInner

%runElab derive "EAInner" [Generic,Meta,Eq,Show]

namespace EAInner

  ||| Number of `Other`s.
  public export
  size : EAInner -> Nat
  size (EAIParens inParens eai)    = size inParens + size eai
  size (EAIOther otherOrComma eai) = 1 + size eai
  size EAIEmpty                    = 0

  ||| Number of `Other`s.
  public export
  leaves : EAInner -> Nat
  leaves (EAIParens inParens eai)    = leaves inParens + leaves eai
  leaves (EAIOther otherOrComma eai) = 1 + leaves eai
  leaves EAIEmpty                    = 1

  ||| Number of `Other`s.
  public export
  depth : EAInner -> Nat
  depth (EAIParens inParens eai)    = 1 + (depth inParens `max` depth eai)
  depth (EAIOther otherOrComma eai) = 1 + depth eai
  depth EAIEmpty                    = 0

||| ExtendedAttributeRest ::
|||   ExtendedAttribute
|||   ε
|||
||| ExtendedAttribute ::
public export
data ExtAttribute : Type where
  ||| ( ExtendedAttributeInner ) ExtendedAttributeRest
  ||| [ ExtendedAttributeInner ] ExtendedAttributeRest
  ||| { ExtendedAttributeInner } ExtendedAttributeRest
  EAParens : (inner : EAInner) -> (rest : Maybe ExtAttribute) -> ExtAttribute

  ||| Other ExtendedAttributeRest
  EAOther : (other : Other) -> (rest : Maybe ExtAttribute) -> ExtAttribute

%runElab derive "ExtAttribute" [Generic,Meta,Eq,Show]

namespace ExtAttribute

  ||| Number of `Other`s.
  public export
  size : ExtAttribute -> Nat
  size (EAParens inner rest) = size inner + maybe 0 size rest
  size (EAOther other rest)  = 1 + maybe 0 size rest

  ||| Number of leaves (unlike `size`, this includes empty leaves)
  public export
  leaves : ExtAttribute -> Nat
  leaves (EAParens inner rest) = leaves inner + maybe 1 leaves rest
  leaves (EAOther other rest)  = 1 + maybe 1 leaves rest

  ||| Number of `Other`s.
  public export
  depth : ExtAttribute -> Nat
  depth (EAParens inner rest) = 1 + (depth inner `max` maybe 0 depth rest)
  depth (EAOther other rest)  = 1 + maybe 0 depth rest

||| ExtendedAttributeList ::
|||   [ ExtendedAttribute ExtendedAttributes ]
|||   ε
|||
||| ExtendedAttributes ::
|||   , ExtendedAttribute ExtendedAttributes
|||   ε
public export
ExtAttributeList : Type
ExtAttributeList = List ExtAttribute

||| TypeWithExtendedAttributes ::
|||     ExtendedAttributeList Type
public export
Attributed : Type -> Type
Attributed a = (ExtAttributeList, a)

public export
interface HasAttributes a where
  attributes : a -> ExtAttributeList

public export
HasAttributes () where
  attributes = const Nil

public export
HasAttributes String where
  attributes = const Nil

public export
HasAttributes Identifier where
  attributes = const Nil

public export
HasAttributes Bool where
  attributes = const Nil

public export
HasAttributes FloatLit where
  attributes = const Nil

public export
HasAttributes IntLit where
  attributes = const Nil

public export
HasAttributes StringLit where
  attributes = const Nil

public export
(HasAttributes a, HasAttributes b) => HasAttributes (a,b) where
  attributes (x,y) = attributes x ++ attributes y

public export
HasAttributes ExtAttribute where
  attributes = pure

public export
HasAttributes a => HasAttributes (Maybe a) where
  attributes = maybe Nil attributes

public export
HasAttributes a => HasAttributes (List a) where
  attributes = concatMap attributes

public export
HasAttributes a => HasAttributes (List1 a) where
  attributes = attributes . forget

--------------------------------------------------------------------------------
--          Deriving HasAttributes
--------------------------------------------------------------------------------

public export
(all : NP HasAttributes ts) => HasAttributes (NP I ts) where
  attributes = hcconcatMap HasAttributes attributes

public export
(all : NP HasAttributes ts) => HasAttributes (NS I ts) where
  attributes = hcconcatMap HasAttributes attributes

public export
(all : POP HasAttributes ts) => HasAttributes (SOP I ts) where
  attributes = hcconcatMap HasAttributes attributes

public export
genAttributes :  Generic a code
              => POP HasAttributes code
              => a
              -> ExtAttributeList
genAttributes = attributes . from

namespace Derive

  public export %inline
  mkHasAttributes : (attrs : a -> ExtAttributeList) -> HasAttributes a
  mkHasAttributes = %runElab check (var $ singleCon "HasAttributes")

  ||| Derives an `Eq` implementation for the given data type
  ||| and visibility.
  export
  HasAttributesVis : Visibility -> DeriveUtil -> InterfaceImpl
  HasAttributesVis vis g = MkInterfaceImpl "HasAttributes" vis []
                             `(mkHasAttributes genAttributes)
                             (implementationType `(HasAttributes) g)

  ||| Alias for `EqVis Public`.
  export
  HasAttributes : DeriveUtil -> InterfaceImpl
  HasAttributes = HasAttributesVis Public

--------------------------------------------------------------------------------
--          Tests and Proofs
--------------------------------------------------------------------------------

isParenTrue : all Attribute.isParenOrQuote (unpack "(){}[]\"") = True
isParenTrue = Refl

isParenFalse : any Attribute.isParenOrQuote (unpack "=!?><:;,.-_") = False
isParenFalse = Refl

isCommaOrParenTrue : all Attribute.isCommaOrParenOrQuote (unpack ",(){}[]\"") = True
isCommaOrParenTrue = Refl

isCommaOrParenFalse : any Attribute.isCommaOrParenOrQuote (unpack "=!?><:;.-_") = False
isCommaOrParenFalse = Refl


text:
module ImplicitArgsError

import Data.Vect

{-
Expected behavior here - Idris throws an error

> implTy : Type -> Type
> implTy ty = Vect n ty -> Nat

"
When checking right hand side of implTy with expected type
        Type

When checking an application of type constructor Data.Vect.Vect:
        No such variable n
"
-}

-- This creates a problem down the line
implTy : Type -> Type
implTy ty = {n : Nat} -> Vect n ty -> Nat

-- This seems fine
fn : (ty : Type) -> (offender : implTy ty) -> Nat
fn ty offender = foo
	where
		barA : Vect 5 ()
		barB : implTy ty
		foo : Nat

{-
-- However, this one is a problem
fn2 : (ty : Type) -> (offender : implTy ty) -> Nat
fn2 ty offender = foo
	where
		barA : Type
		barB : implTy barA
		foo : Nat
-}

-- Similar problem here, with implTy2 and fn3
implTy2 : Vect n () -> Type
implTy2 v {n} = {m : Nat} -> Vect m (Vect n ()) -> Nat

{-
fn3 : (xs : Vect n ()) -> (offender : implTy2 xs) -> Nat
fn3 xs offender = foo
	where
		barA : Vect 5 ()
		barB : implTy2 barA
		foo : Nat
-}

{-
This seems okay, where there is no parameter to the type, because the problem occurs when (offender) interacts with another value of the type-valued function.
-}
implTy3 : Type
implTy3 = {n : Nat} -> Vect n () -> Nat

fn4 : (xs : Vect n ()) -> (offender : implTy3) -> Nat
fn4 xs offender = foo
	where
		bar : implTy3
		foo : Nat

{-
Namespace refinement doesn't help

---

fn5 : (xs : Vect n ()) -> (offender : ImplicitArgsError.implTy2 xs) -> Nat
fn5 xs offender = foo
	where
		barA : Vect 5 ()
		barB : ImplicitArgsError.implTy2 barA
		foo : Nat
-}

{-
Independence of the other arguments of the function type on the implicit argument does not resolve the situation.
-}
implTy4 : Vect n () -> Type
implTy4 v {n} = {m : Nat} -> Integer

{-
fn6 : (xs : Vect n ()) -> (offender : implTy4 xs) -> Integer
fn6 xs offender = foo
	where
		barA : Vect 5 ()
		barB : implTy4 barA
		foo : Integer
-}

-- It does not matter if there is no implicit argument to the type-valued function.
implTy5 : Either () () -> Type
implTy5 v = {m : Nat} -> Integer

{-
fn7 : (xs : Either () ()) -> (offender : implTy5 xs) -> Integer
fn7 xs offender = foo
	where
		barA : Either () ()
		barB : implTy5 barA
		foo : Integer
-}

{-
Finally, when the type-valued function is given explicit parameters in the inner value, you get a relevant error:

"Can't infer argument m1 to offender"

---

fn7 : (xs : Either () ()) -> (offender : implTy5 xs) -> Integer
fn7 xs offender = foo
	where
		bar : implTy5 $ Left ()
		foo : Integer

-----

... But not if the explicit parameter is specified indirectly.

---

fn8 : (xs : Either () ()) -> (offender : implTy5 xs) -> Integer
fn8 xs offender = foo
	where
		barA : Either () ()
		barA = Left ()
		barB : implTy5 barA
		foo : Integer

-}

{-

Relevant error:

"Can't infer argument m1 to offender"

---

fn9 : (offender : implTy5 $ Left ()) -> Integer
fn9 offender = foo
	where
		foo : Integer
-}

{-
Relevant error

	"Can't infer argument m1 to offender"

and no explicit arguments passed to the type-valued function.

---

fn10 : (xs : Either () ()) -> (offender : implTy5 xs) -> Integer
fn10 xs offender = foo
	where
		bar : ()
		foo : Integer
-}

{-
A distinct irrelevant error:

"
When checking right hand side of fn11 with expected type
        Integer

No such variable offender
"

---

fn11 : (xs : Either () ()) -> (offender : implTy5 xs) -> Integer
fn11 xs offender = offender {m=0}
-}

{-
When checking argument l to constructor Prelude.Either.Left:
        () is not a numeric type

---

fn12 : (offender : implTy5 $ Left 5) -> Integer
fn12 offender = offender {m=0}

---

fn13 : (offender : implTy5 $ Left 5) -> Integer
fn13 = (\offender => offender {m=0})

---

fn13 : (offender : implTy5 $ Left 5) -> Integer
fn13 = (\offender => offender 0)

---

fn14 : (offender : implTy5 $ Left 5) -> Integer
fn14 = ?fn14'
-}

{-
When checking right hand side of fn15 with expected type
        (xs : Either () ()) -> implTy5 xs -> Integer

No such variable friend

---

fn15 : (xs : Either () ()) -> (offender : implTy5 xs) -> Integer
fn15 = (\xs => \friend => friend 0)

---

fn16 : (xs : Either () ()) -> (offender : implTy5 xs) -> Integer
fn16 = (\xs => (\friend => friend {m=0}))
-}


text:
module Main

main : IO ()
main = pure ()


text:
module Puts

%default total

%foreign "C:puts,libc"
puts : String -> PrimIO ()

myPuts : HasIO io => String -> io ()
myPuts s = primIO $ puts s

main : IO ()
main = myPuts "Hello, world!\n"

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

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

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