text:
module TTImp.Reflect

import Core.Context
import Core.Normalise
import public Core.Reflect
import Core.Unify
import Core.TT

import TTImp.TTImp

import Data.List

%default covering

-- TODO: Remaining cases!
export
Reify annot => Reify (RawImp annot) where
  reify defs (NDCon (NS ["Reflect"] (UN "Var")) _ _ [fc, n])
      = do fc' <- reify defs (evalClosure defs fc)
           n' <- reify defs (evalClosure defs n)
           pure (IVar fc' n')
  reify defs (NDCon (NS ["Reflect"] (UN "App")) _ _ [fc, f, a])
      = do fc' <- reify defs (evalClosure defs fc)
           f' <- reify defs (evalClosure defs f)
           a' <- reify defs (evalClosure defs a)
           pure (IApp fc' f' a')
  reify defs _ = Nothing

-- TODO: Remaining cases!
export
Reflect annot => Reflect (RawImp annot) where
  reflect defs env (IVar fc nm)
      = do fc' <- reflect defs env fc
           nm' <- reflect defs env nm
           appCon defs (NS ["Reflect"] (UN "Var")) [fc', nm']
  reflect defs env (IApp fc f a)
      = do fc' <- reflect defs env fc
           f' <- reflect defs env f
           a' <- reflect defs env a
           appCon defs (NS ["Reflect"] (UN "App")) [fc', f', a']
  reflect defs env (IUnquote fc (IVar _ nm))
      = do (count, el) <- defined nm env
           pure (Local Nothing el)
  reflect defs env _ = Nothing

export
Reify FnOpt where
  reify defs (NDCon (NS ["Reflect"] (UN "Inline")) _ _ [])
      = pure Inline
  reify defs (NDCon (NS ["Reflect"] (UN "Hint")) _ _ [t])
      = do t' <- reify defs (evalClosure defs t)
           pure (Hint t')
  reify defs (NDCon (NS ["Reflect"] (UN "GlobalHint")) _ _ [t])
      = do t' <- reify defs (evalClosure defs t)
           pure (GlobalHint t')
  reify defs (NDCon (NS ["Reflect"] (UN "ExternFn")) _ _ [])
      = pure ExternFn
  reify defs (NDCon (NS ["Reflect"] (UN "Invertible")) _ _ [])
      = pure Invertible
  reify defs (NDCon (NS ["Reflect"] (UN "Total")) _ _ [])
      = pure Total
  reify defs (NDCon (NS ["Reflect"] (UN "Covering")) _ _ [])
      = pure Covering
  reify defs (NDCon (NS ["Reflect"] (UN "PartialOK")) _ _ [])
      = pure PartialOK
  reify defs _ = Nothing

export
Reflect FnOpt where
  reflect defs env Inline = getCon defs (NS ["Reflect"] (UN "Inline"))
  reflect defs env (Hint t)
      = do t' <- reflect defs env t
           appCon defs (NS ["Reflect"] (UN "Hint")) [t']
  reflect defs env (GlobalHint t)
      = do t' <- reflect defs env t
           appCon defs (NS ["Reflect"] (UN "GlobalHint")) [t']
  reflect defs env ExternFn = getCon defs (NS ["Reflect"] (UN "ExternFn"))
  reflect defs env Invertible = getCon defs (NS ["Reflect"] (UN "Invertible"))
  reflect defs env Total = getCon defs (NS ["Reflect"] (UN "Total"))
  reflect defs env Covering = getCon defs (NS ["Reflect"] (UN "Covering"))
  reflect defs env PartialOK = getCon defs (NS ["Reflect"] (UN "PartialOK"))

export
Reify annot => Reify (ImpTy annot) where
  reify defs (NDCon (NS ["Reflect"] (UN "MkTy")) _ _ [fc, n, ty])
      = do fc' <- reify defs (evalClosure defs fc)
           n' <- reify defs (evalClosure defs n)
           ty' <- reify defs (evalClosure defs ty)
           pure (MkImpTy fc' n' ty')
  reify defs _ = Nothing

export
Reflect annot => Reflect (ImpTy annot) where
  reflect defs env (MkImpTy fc n ty)
      = do fc' <- reflect defs env fc
           n' <- reflect defs env n
           ty' <- reflect defs env ty
           appCon defs (NS ["Reflect"] (UN "MkTy")) [fc', n', ty']

export
Reify annot => Reify (ImpClause annot) where
  reify defs (NDCon (NS ["Reflect"] (UN "PatClause")) _ _ [fc, lhs, rhs])
      = do fc' <- reify defs (evalClosure defs fc)
           lhs' <- reify defs (evalClosure defs lhs)
           rhs' <- reify defs (evalClosure defs rhs)
           pure (PatClause fc' lhs' rhs')
  reify defs (NDCon (NS ["Reflect"] (UN "WithClause")) _ _ [fc, lhs, wval, cs])
      = do fc' <- reify defs (evalClosure defs fc)
           lhs' <- reify defs (evalClosure defs lhs)
           wval' <- reify defs (evalClosure defs wval)
           cs' <- reify defs (evalClosure defs cs)
           pure (WithClause fc' lhs' wval' cs')
  reify defs (NDCon (NS ["Reflect"] (UN "Impossible")) _ _ [fc, lhs])
      = do fc' <- reify defs (evalClosure defs fc)
           lhs' <- reify defs (evalClosure defs lhs)
           pure (ImpossibleClause fc' lhs')
  reify defs _ = Nothing

export
Reflect annot => Reflect (ImpClause annot) where
  reflect defs env (PatClause fc lhs rhs)
      = do fc' <- reflect defs env fc
           lhs' <- reflect defs env lhs
           rhs' <- reflect defs env rhs
           appCon defs (NS ["Reflect"] (UN "PatClause")) [fc', lhs', rhs']
  reflect defs env (WithClause fc lhs wval cs)
      = do fc' <- reflect defs env fc
           lhs' <- reflect defs env lhs
           wval' <- reflect defs env wval
           cs' <- reflect defs env cs
           appCon defs (NS ["Reflect"] (UN "WithClause")) [fc', lhs', wval', cs']
  reflect defs env (ImpossibleClause fc lhs)
      = do fc' <- reflect defs env fc
           lhs' <- reflect defs env lhs
           appCon defs (NS ["Reflect"] (UN "Impossible")) [fc', lhs']

export
Reify DataOpt where
  reify defs (NDCon (NS ["Reflect"] (UN "SearchBy")) _ _ [xs])
      = do xs' <- reify defs (evalClosure defs xs)
           pure (SearchBy xs')
  reify defs (NDCon (NS ["Reflect"] (UN "NoHints")) _ _ [])
      = pure NoHints
  reify defs _ = Nothing

export
Reflect DataOpt where
  reflect defs env (SearchBy xs)
      = do xs' <- reflect defs env xs
           appCon defs (NS ["Reflect"] (UN "SearchBy")) [xs']
  reflect defs env NoHints = getCon defs (NS ["Reflect"] (UN "Hint"))

export
Reify annot => Reify (ImpData annot) where
  reify defs (NDCon (NS ["Reflect"] (UN "MkData")) _ _ [fc, tyn, ty, opts, cons])
      = do fc' <- reify defs (evalClosure defs fc)
           tyn' <- reify defs (evalClosure defs tyn)
           ty' <- reify defs (evalClosure defs ty)
           opts' <- reify defs (evalClosure defs opts)
           cons' <- reify defs (evalClosure defs cons)
           pure (MkImpData fc' tyn' ty' opts' cons')
  reify defs (NDCon (NS ["Reflect"] (UN "MkLater")) _ _ [fc, tyn, ty])
      = do fc' <- reify defs (evalClosure defs fc)
           tyn' <- reify defs (evalClosure defs tyn)
           ty' <- reify defs (evalClosure defs ty)
           pure (MkImpLater fc' tyn' ty')
  reify defs _ = Nothing

export
Reflect annot => Reflect (ImpData annot) where
  reflect defs env (MkImpData fc n tycon opts cons)
      = do fc' <- reflect defs env fc
           n' <- reflect defs env n
           tycon' <- reflect defs env tycon
           opts' <- reflect defs env opts
           cons' <- reflect defs env cons
           appCon defs (NS ["Reflect"] (UN "MkData")) [fc', n', tycon', opts', cons']
  reflect defs env (MkImpLater fc n tycon)
      = do fc' <- reflect defs env fc
           n' <- reflect defs env n
           tycon' <- reflect defs env tycon
           appCon defs (NS ["Reflect"] (UN "MkLater")) [fc', n', tycon']

export
Reify annot => Reify (ImpDecl annot) where
  reify defs (NDCon (NS ["Reflect"] (UN "Claim")) _ _ [fc, vis, opts, ty])
      = do fc' <- reify defs (evalClosure defs fc)
           vis' <- reify defs (evalClosure defs vis)
           opts' <- reify defs (evalClosure defs opts)
           ty' <- reify defs (evalClosure defs ty)
           pure (IClaim fc' RigW vis' opts' ty')
  reify defs (NDCon (NS ["Reflect"] (UN "Def")) _ _ [fc, n, cs])
      = do fc' <- reify defs (evalClosure defs fc)
           n' <- reify defs (evalClosure defs n)
           cs' <- reify defs (evalClosure defs cs)
           pure (IDef fc' n' cs')
  reify defs (NDCon (NS ["Reflect"] (UN "Data")) _ _ [fc, vis, ddecl])
      = do fc' <- reify defs (evalClosure defs fc)
           vis' <- reify defs (evalClosure defs vis)
           ddecl' <- reify defs (evalClosure defs ddecl)
           pure (IData fc' vis' ddecl')
  reify defs _ = Nothing

export
Reflect annot => Reflect (ImpDecl annot) where
  reflect defs env (IClaim fc _ vis opts ty)
      = do fc' <- reflect defs env fc
           vis' <- reflect defs env vis
           opts' <- reflect defs env opts
           ty' <- reflect defs env ty
           appCon defs (NS ["Reflect"] (UN "Claim")) [fc', vis', opts', ty']
  reflect defs env (IDef fc n cs)
      = do fc' <- reflect defs env fc
           n' <- reflect defs env n
           cs' <- reflect defs env cs
           appCon defs (NS ["Reflect"] (UN "Def")) [fc', n', cs']
  reflect defs env (IData fc vis ddecl)
      = do fc' <- reflect defs env fc
           vis' <- reflect defs env vis
           ddecl' <- reflect defs env ddecl
           appCon defs (NS ["Reflect"] (UN "Data")) [fc', vis', ddecl']
  reflect defs env _ = Nothing

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module JSON.Option

import Generics.Derive

%language ElabReflection

||| Specifies how to encode constructors of a sum datatype.
public export
data SumEncoding : Type where
  ||| Constructor names won't be encoded. Instead only the contents of the
  ||| constructor will be encoded as if the type had a single constructor. JSON
  ||| encodings have to be disjoint for decoding to work properly.
  |||
  ||| When decoding, constructors are tried in the order of definition. If some
  ||| encodings overlap, the first one defined will succeed.
  |||
  ||| Note: Nullary constructors are encoded as strings (using
  ||| constructorTagModifier).  Having a nullary constructor
  ||| alongside a single field constructor that encodes to a
  ||| string leads to ambiguity.
  |||
  ||| Note: Only the last error is kept when decoding, so in the case of
  ||| malformed JSON, only an error for the last constructor will be reported.
  UntaggedValue         : SumEncoding

  ||| A constructor will be encoded to an object with a single field named
  ||| after the constructor tag (modified by the constructorTagModifier) which
  ||| maps to the encoded contents of the constructor.
  ObjectWithSingleField : SumEncoding

  ||| A constructor will be encoded to a 2-element array where the first
  ||| element is the tag of the constructor (modified by the constructorTagModifier)
  ||| and the second element the encoded contents of the constructor.
  TwoElemArray          : SumEncoding

  ||| A constructor will be encoded to an object with a field `tagFieldName`
  ||| which specifies the constructor tag (modified by the
  ||| constructorTagModifier). If the constructor is a record the
  ||| encoded record fields will be unpacked into this object. So
  ||| make sure that your record doesn't have a field with the
  ||| same label as the tagFieldName.  Otherwise the tag gets
  ||| overwritten by the encoded value of that field! If the constructor
  ||| is not a record the encoded constructor contents will be
  ||| stored under the contentsFieldName field.
  TaggedObject          :  (tagFieldName : String)
                        -> (contentsFieldName : String)
                        -> SumEncoding

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

||| Corresponds to `TaggedObject "tag" "contents"`
public export
defaultTaggedObject : SumEncoding
defaultTaggedObject = TaggedObject "tag" "contents"

public export
adjustConnames : (String -> String) -> TypeInfo' k kss -> TypeInfo' k kss
adjustConnames f = { constructors $= mapNP adjCon }
  where adjCon : ConInfo_ k ks -> ConInfo_ k ks
        adjCon (MkConInfo ns n fs) = MkConInfo ns (f n) fs

public export
adjustInfo :  (adjFields : String -> String)
           -> (adjCons : String -> String)
           -> TypeInfo' k kss
           -> TypeInfo' k kss
adjustInfo af ac = { constructors $= mapNP adjCon }
  where adjArg : ArgName -> ArgName
        adjArg (NamedArg ix n) = NamedArg ix $ af n
        adjArg arg = arg

        adjCon : ConInfo_ k ks -> ConInfo_ k ks
        adjCon (MkConInfo ns n fs) = MkConInfo ns (ac n) (mapNP adjArg fs)

public export
adjustFieldNames : (String -> String) -> TypeInfo' k kss -> TypeInfo' k kss
adjustFieldNames f = adjustInfo f id

public export
nullaryInjections :  NP_ (List k) (ConInfo_ k) kss
                  -> (0 et : EnumType kss)
                  -> NP_ (List k) (K (NS_ (List k) (NP f) kss)) kss
nullaryInjections []                       _  = []
nullaryInjections (MkConInfo _ _ [] :: vs) es =
  Z [] :: mapNP (\ns => S ns) (nullaryInjections vs (enumTail es))

ext: idr


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

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


text:
||| GCD and LCM. This is partial algorhytm with assert_total notation.
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Integral.Gcd

%default total

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

export gcd : (Eq a, Num a, Abs a, Integral a) => a -> a -> a
gcd x y = go (abs x) (abs y)
  where go : a -> a -> a
        go x' y' = if y' == 0 then x' else assert_total $ go y' (x' `mod` y')

export lcm : (Eq a, Num a, Abs a, Integral a) => a -> a -> a
lcm x y = if x == 0 then 0
          else if y == 0 then 0
          else abs $ (x `div` (gcd x y)) * y

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


text:
module Main

import Data.Vect
import Data.Nat.Exponentiation

-- https://bmwant.github.io/idris-is-awesome.github.io/docs/basic.html

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

average : Double -> Double -> Double

x : Int
x = 2

max_stars_repo_name: DejanMilicic/IdrisPlayground

max_issues_repo_name: DejanMilicic/IdrisPlayground

max_forks_repo_name: DejanMilicic/IdrisPlayground


text:
module Main

import System.FFI

%default total

libsmall : String -> String
libsmall fn = "C:" ++ fn ++ ",libsmall"

Point : Type
Point = Struct "point" [("x", Int), ("y", Int)]

%foreign (libsmall "mk_point")
mkPoint : Int -> Int -> Point

%foreign (libsmall "free_point")
prim_freePoint : Point -> PrimIO ()

freePoint : HasIO io => Point -> io ()
freePoint p = primIO $ prim_freePoint p

showPoint : Point -> String
showPoint p =
  let x : Int = getField p "x"
      y : Int = getField p "y" in
      show (x, y)

main : IO ()
main = do let p = mkPoint 100 200
          putStrLn (showPoint p)
          setField p "x" (the Int 42)
          setField p "y" (the Int (-42))
          putStrLn (showPoint p)
          freePoint p

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

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

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


text:
module TestStrings

import Data.String
import Data.String.Iterator

iteratorTail : String -> String
iteratorTail str = withString str $ \it => unconsTail str (uncons str it)
  where
    unconsTail : (str : String) -> (1 _ : UnconsResult str) -> String
    unconsTail str EOF = ""
    unconsTail str (Character _ tailIt) = withIteratorString str tailIt id

isUnderscore : Char -> Bool
isUnderscore '_' = True
isUnderscore _ = False

isHelloWorld : String -> Bool
isHelloWorld "Hello, world" = True
isHelloWorld _ = False

main : IO ()
main = do
    let helloWorld = "Hello, " ++ "world"

    putStrLn helloWorld
    putStrLn $ show $ length helloWorld
    putStrLn $ show $ String.length ""

    putStrLn $ reverse helloWorld
    putStrLn $ reverse ""
    putStrLn $ substr 1 2 helloWorld
    putStrLn $ substr 10 10 helloWorld
    putStrLn $ substr 1 2 ""
    putStrLn $ show $ assert_total $ strIndex helloWorld 1

    putStrLn $ strCons 'a' "bc"
    putStrLn $ strCons 'a' ""
    putStrLn $ show $ strUncons "abc"
    putStrLn $ show $ strUncons ""

    putStrLn $ fastPack ['p', 'a', 'c', 'k']
    putStrLn $ fastPack []
    putStrLn $ show $ fastUnpack "unpack"
    putStrLn $ show $ fastUnpack ""
    putStrLn $ fastConcat ["con", "cat", "en", "ate"]
    putStrLn $ fastConcat []

    let chars = the (List Char) ['a', 'A', '~', '0', ' ', '\n', '\x9f']
    putStrLn $ show $ map isUpper chars
    putStrLn $ show $ map isLower chars
    putStrLn $ show $ map isDigit chars
    putStrLn $ show $ map isSpace chars
    putStrLn $ show $ map isNL chars
    putStrLn $ show $ map isControl chars

    putStrLn $ show $ map {f = List} chr [97, 65, 126, 48, 32, 10, 159]
    putStrLn $ show $ map ord chars

    putStrLn $ show $ Data.String.Iterator.unpack "iterator unpack"
    putStrLn $ show $ iteratorTail "iterator tail"

    -- Test Char pattern matching
    putStrLn $ show $ isUnderscore '_'
    putStrLn $ show $ isUnderscore ' '

    -- Test String pattern matching
    putStrLn $ show $ isHelloWorld helloWorld
    putStrLn $ show $ isHelloWorld "Hello, Idris"


text:
module Main

import Erlang.System

main : IO ()
main = do
  args <- getArgs
  printLn args


text:
module Postgres.DB.Core

import Postgres.Utility
import Postgres.Data.Conn
import Postgres.Data.ConnectionStatus

--
-- Open Connection
--
%foreign (Utility.libpq "PQconnectdb")
prim__dbOpen : String -> PrimIO (Ptr PGconn)

||| Open a connection to a Postgres database.
||| This connection must be closed using `pgClose`.
|||
||| You can check the status of the connection
||| (including failure to connect) with the
||| `pgStatus` function.
export
pgOpen : HasIO io => (pgUrl: String) -> io Conn
pgOpen url = (map MkConn (primIO $ prim__dbOpen url))

--
-- Close Connection
--
%foreign libpq "PQfinish"
prim__dbClose : Ptr PGconn -> PrimIO ()

||| Close a connection to a Postgres database.
export
pgClose : HasIO io => Conn -> io ()
pgClose (MkConn conn) = primIO $ prim__dbClose conn

--
-- Get Connection Status
--
%foreign libpq "PQstatus"
prim__dbStatus : Ptr PGconn -> Int

connectionStatus: Int -> ConnectionStatus
connectionStatus i
    = case i of
        0 => OK
        1 => BAD
        2 => STARTED
        3 => MADE
        4 => AWAITING_RESPONSE
        5 => AUTH_OK
        6 => SETENV
        7 => SSL_STARTUP
        8 => NEEDED
        _ => OTHER i

||| Get the status of a Postgres database connection.
export
pgStatus : Conn -> ConnectionStatus
pgStatus (MkConn conn) = connectionStatus $ prim__dbStatus conn

%foreign helper "connErrorMessage"
prim__dbErrorMessage : Ptr PGconn -> PrimIO String

||| Get an error message from Postgres when something goes wrong.
export
pgErrorMessage : HasIO io => Conn -> io String
pgErrorMessage (MkConn conn) = primIO $ prim__dbErrorMessage conn

--
-- Consume Input from Server
--

%foreign libpq "PQconsumeInput"
prim__dbConsumeInput : Ptr PGconn -> PrimIO Int

||| Consume any input the server has delivered
||| since the last time we ran a command that
||| otherwise consumed server input.
|||
||| It can be useful to explicitly call upon
||| `libpq` to consume input when doing something
||| like listening for notifications that does
||| not otherwise require making any calls to
||| execute anything on the server.
|||
||| Returns True if successfuly and False
||| otherwise.
export pgConsumeInput : Conn -> IO Bool
pgConsumeInput (MkConn conn) = (map intToBool (primIO $ prim__dbConsumeInput conn))

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
module General

import Basic
import Unit
import Void
import Sigma
import Coproduct
import Path
import PreorderReasoning

infix 0 <=>

||| Logical equivalence
public export
(<=>) : Type -> Type -> Type
a <=> b = Pair (a -> b) (b -> a)

infix 0 /=

public export
(/=) : a -> a -> Type
x /= y = Neg (x == y)

public export
negSym : {x, y : _} -> x /= y -> y /= x
negSym p u = p (sym u)


text:
module Main

import Package3.Lib

export
main : IO ()
main = putStrLn testFunc3

max_stars_repo_name: idream-build/idream

max_issues_repo_name: idream-build/idream

max_forks_repo_name: idream-build/idream


text:
module Extra.List

import Data.List
import Data.Maybe

export
dropPrefix : Eq a => List a -> List a -> List a
dropPrefix pre x =
  if isPrefixOf pre x
    then drop (length pre) x
    else x

export
collapse : Monad t => List (t a) -> t (List a)
collapse =
  foldl f (pure [])
    where
      fi : t a -> List a -> t (List a)
      fi el acc =
        map (\e => e :: acc) el

      f : t (List a) -> t a -> t (List a)
      f acc el =
        acc >>= fi el

export
range : Nat -> List Nat
range n =
  reverse (drop 1 (iterate next n))
    where
      next : Nat -> Maybe Nat
      next (S k) = Just k
      next Z = Nothing

export
zipWithIndex : List a -> List (a, Nat)
zipWithIndex l =
  zip l (range (length l))

export
repeat : a -> Nat -> List a
repeat _ Z = []
repeat x (S n) = x :: repeat x n

export
findAll : Eq a => List a -> List a -> List Nat
findAll l k =
  reverse (findAllHelper l k 0 [])
  where
    findAllHelper : List a -> List a -> Nat -> List Nat -> List Nat
    findAllHelper l k index acc =
      case l of
        [] =>
          acc
        _ =>
          let
            nextAcc =
              if isPrefixOf k l then
                (index :: acc)
              else
                acc
          in
            findAllHelper (drop 1 l) k (index + 1) nextAcc

export
replace : Eq a => List a -> List a -> List a -> List a
replace l k v =
  let
    matches = findAll l k
    repl = reverse v
    skipLen = case length k of
      Z =>
        0 -- This is really impossible but we haven't refined our types to say so
      (S Z) =>
        0
      (S k) =>
        k
  in
    reverse $ fst $ foldl (\(acc, skip), (c, i) =>
      case skip of
        Just (S k) =>
          (acc, Just k)
        _ =>
          if any (== i) matches then
            -- We need to insert a replacement and then skip N els
            (repl ++ acc, Just skipLen)
          else
            (c :: acc, Nothing)
    ) ([], (the (Maybe Nat) Nothing)) (zipWithIndex l)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Main
import Data.Strings

myCondition : Nat -> String
myCondition x = case x of
                    Z => "Zero"
                    _ => "Non-Zero"

main : IO ()
main = do  putStr "Enter a positive number: "
           str <- getLine
           let num = stringToNatOrZ str
           printLn $ myCondition num
--           case num of
--               Z => do printLn $ "0"
--               Z => do printLn $ "Your number is interesting but you should think bigger."
--               (<= 6) => printLn "You can get that on a roll of dice."
--               (> 10) => printLn "You have to have multiple rolls of dice to get that."
           printLn $ "Bye for now."


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 12

import Control.Monad.State
import Tree

-- check that all functions are total
%default total

--
-- section 12.1
--

update : (stateType -> stateType) -> State stateType ()
update f = get >>= put . f
-- or:
-- update f = do s <- get
--               put $ f s

increase : Nat -> State Nat ()
increase x = update (+x)

countEmpty : Tree a -> State Nat ()
countEmpty Empty = increase 1
countEmpty (Node left val right)
  = do countEmpty left
       countEmpty right

incrementFst : State (Nat, Nat) ()
incrementFst = update (\(x,y) => (x + 1, y))

incrementSnd : State (Nat, Nat) ()
incrementSnd = update (\(x,y) => (x, y + 1))

countEmptyNode : Tree a -> State (Nat, Nat) ()
countEmptyNode Empty = incrementFst
countEmptyNode (Node left val right)
  = do countEmptyNode left
       countEmptyNode right
       incrementSnd

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty) "Fred"
                      (Node Empty "Sheila" Empty)) "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

--
-- section 12.3
-- see Quiz.idr (with added things to update difficulty)
-- see SocialNews.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module FibGCD

import Data.Nat

import Decidable.Equality

fib : Nat -> Nat
fib 0 = 0
fib 1 = 1
fib (S $ S n) = fib (S n) + fib n

%hint
fib_isSucc : (n : Nat) -> IsSucc n => IsSucc (fib n)

fib_gcd : {n, m : Nat} -> case fib_isSucc (S n) of ItIsSucc => gcd {ok=LeftIsNotZero} (fib $ S n) (fib $ S m) = fib (gcd (S n) (S m))

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module System.Concurrency.Raw

-- At the moment this is pretty fundamentally tied to the Scheme RTS
-- Given that different back ends will have entirely different threading
-- models, it might be unavoidable, but we might want to think about possible
-- primitives that back ends should support.

%foreign "scheme:blodwen-thisthread"
prim__threadID : PrimIO ThreadID
%foreign "scheme:blodwen-set-thread-data"
prim__setThreadData : {a : Type} -> a -> PrimIO ()
%foreign "scheme:blodwen-get-thread-data"
prim__getThreadData : (a : Type) -> PrimIO a

-- Mutexes and condition variables.

export
threadID : IO ThreadID
threadID = primIO prim__threadID

export
setThreadData : {a : Type} -> a -> IO ()
setThreadData val = primIO (prim__setThreadData val)

export
getThreadData : (a : Type) -> IO a
getThreadData a = primIO (prim__getThreadData a)

export
data Mutex : Type where [external]

%foreign "scheme:blodwen-mutex"
prim__makeMutex : PrimIO Mutex
%foreign "scheme:blodwen-lock"
prim__mutexAcquire : Mutex -> PrimIO ()
%foreign "scheme:blodwen-unlock"
prim__mutexRelease : Mutex -> PrimIO ()

export
makeMutex : IO Mutex
makeMutex = primIO prim__makeMutex

export
mutexAcquire : Mutex -> IO ()
mutexAcquire m = primIO (prim__mutexAcquire m)

export
mutexRelease : Mutex -> IO ()
mutexRelease m = primIO (prim__mutexRelease m)

export
data Condition : Type where [external]

%foreign "scheme:blodwen-condition"
prim__makeCondition : PrimIO Condition
%foreign "scheme:blodwen-condition-wait"
prim__conditionWait : Condition -> Mutex -> PrimIO ()
%foreign "scheme:blodwen-condition-wait-timeout"
prim__conditionWaitTimeout : Condition -> Mutex -> Int -> PrimIO ()
%foreign "scheme:blodwen-condition-signal"
prim__conditionSignal : Condition -> PrimIO ()
%foreign "scheme:blodwen-condition-broadcast"
prim__conditionBroadcast : Condition -> PrimIO ()

export
makeCondition : IO Condition
makeCondition = primIO prim__makeCondition

export
conditionWait : Condition -> Mutex -> IO ()
conditionWait c m = primIO (prim__conditionWait c m)

||| Timeout is in microseconds
export
conditionWaitTimeout : Condition -> Mutex -> Int -> IO ()
conditionWaitTimeout c m t = primIO (prim__conditionWaitTimeout c m t)

export
conditionSignal : Condition -> IO ()
conditionSignal c = primIO (prim__conditionSignal c)

export
conditionBroadcast : Condition -> IO ()
conditionBroadcast c = primIO (prim__conditionBroadcast c)


text:
module Test.RingLaws

import public Algebra.Ring
import Data.SOP
import Hedgehog

prop_plusCommutative : Show a => Eq a => Ring a => Gen a -> Property
prop_plusCommutative g = property $ do
  [m,n] <- forAll $ np [g,g]
  m + n === n + m

prop_plusAssociative : Show a => Eq a => Ring a => Gen a -> Property
prop_plusAssociative g = property $ do
  [k,m,n] <- forAll $ np [g,g,g]
  k + (m + n) === k + (n + m)

prop_plusZeroLeftNeutral : Show a => Eq a => Ring a => Gen a -> Property
prop_plusZeroLeftNeutral g = property $ do
  n <- forAll g
  0 + n === n

prop_plusNegateLeftZero : Show a => Eq a => Ring a => Gen a -> Property
prop_plusNegateLeftZero g = property $ do
  n <- forAll g
  negate n + n === 0

prop_multCommutative : Show a => Eq a => Ring a => Gen a -> Property
prop_multCommutative g = property $ do
  [m,n] <- forAll $ np [g,g]
  m * n === n * m

prop_multAssociative : Show a => Eq a => Ring a => Gen a -> Property
prop_multAssociative g = property $ do
  [k,m,n] <- forAll $ np [g,g,g]
  k * (m * n) === k * (n * m)

prop_multOneLeftNeutral : Show a => Eq a => Ring a => Gen a -> Property
prop_multOneLeftNeutral g = property $ do
  n <- forAll g
  1 * n === n

prop_distributive : Show a => Eq a => Ring a => Gen a -> Property
prop_distributive g = property $ do
  [k,m,n] <- forAll $ np [g,g,g]
  k * (m + n) === (k * m) + (k * n)

prop_minusIsPlusNegate : Show a => Eq a => Ring a => Gen a -> Property
prop_minusIsPlusNegate g = property $ do
  [m,n] <- forAll $ np [g,g]
  m - n === m + negate n

export
ringProps :  Show a
          => Eq a
          => Ring a
          => Gen a
          -> List (PropertyName,Property)
ringProps g =
  [ ("prop_plusCommutative",     prop_plusCommutative g)
  , ("prop_plusAssociative",     prop_plusAssociative g)
  , ("prop_plusZeroLeftNeutral", prop_plusZeroLeftNeutral g)
  , ("prop_plusNegateLeftZero",  prop_plusNegateLeftZero g)
  , ("prop_multCommutative",     prop_multCommutative g)
  , ("prop_multAssociative",     prop_multAssociative g)
  , ("prop_multOneLeftNeutral",  prop_multOneLeftNeutral g)
  , ("prop_distributive",        prop_distributive g)
  , ("prop_minusIsPlusNegate",   prop_minusIsPlusNegate g)
  ]


text:
-- -------------------------------------------------------------- [ StringFile ]
-- Module      : Lightyear.StringFile
-- Description : String-related effectful file parsers.
--
-- This code is distributed under the BSD 2-clause license.
-- See the file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]

module Lightyear.StringFile

import public Effects
import public Effect.File

import Lightyear
import Lightyear.Strings

%access export
-- ---------------------------------------------------- [ A String File Parser ]

||| Parse a file using the specified parser.
|||
||| @rErr  A custom error for reporting FileIO errors.
||| @pErr  A custom error for reporting Parsing errors.
||| @p     The parser to use on the specified file.
||| @fname The name of the file to parser.
parseFile : (rErr  : String -> FileError -> e)
         -> (pErr  : String -> String -> e)
         -> (p     : Parser a)
         -> (fname : String)
         -> Eff (Either e a) [FILE ()]
parseFile rErr pErr p fn = do
    Result src <- readFile fn
                  | FError err => pure (Left (rErr fn err))
    case parse p src of
      Left err  => pure $ Left (pErr fn err)
      Right res => pure $ Right res

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


text:
%default total

test : (String, ()) -> ()
test ("a", ()) = ()

test' : (Int, ()) -> ()
test' (1, ()) = ()

test'' : Type -> Type
test'' (List a) = a


text:
-- ----------------------------------------------------------- [ Component.idr ]
-- Module    : Component.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Definition of an IP Core.
|||
||| We call IP Cores components because...
module Cordial.Model.Component

import Data.DList

import Text.Markup.Edda

import public Cordial.Model.Common
import        Cordial.Model.Specification
import public Cordial.Model.Projection
import public Cordial.Model.Interface

%default total
%access public export

data TrustKind = Trusted | UnTrusted

||| Representation of an IP Core as a list of interfaces.
|||
||| @trusted Do we trust the underlying IP Core.
||| @kinds   Collect the Kinds of interface the IP Core has.
||| @interfaceTys Collect the top level abstract description that each interface models.
data Component : (annot : Type)
              -> (trusted       : TrustKind)
              -> (kinds         : InterfaceKinds ks)
              -> (interfaceTys  : InterfaceTys annot tts)
              -> Type
  where
    MkComponent : (info : annot)
               -> (name : VLNV)
               -> (doc : DocString)
               -> (t : TrustKind)
               -> (interfaces : Interfaces annot kinds itys)
               -> Component annot t kinds itys

||| Add an interface to an IP Core.
|||
||| We make explicit the interface kind, type, and structure.
addInterface : (c    : Component annot t ks types)
            -> (kind : InterfaceKind b e)
            -> (type : InterfaceTy annot labelTy)
            -> (i    : Interface annot labelTy e kind endian type (projectByKind kind type))
            -> Component annot t (kind::ks) (type::types)
addInterface (MkComponent info name doc t is) kind type i = MkComponent info name doc t (i :: is)

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module UnderscoredIntegerLiterals

-- grouping decimal numbers by thousands
amount : Integer
amount = 10_000_000_000

equalAmounts : Bool
equalAmounts = amount == 10000000000

-- grouping hexadecimal addresses by words
addr : Int
addr = 0xCAFE_F00D

equalAddrs : Bool
equalAddrs = addr == 0xCAFEF00D

-- grouping bits into nibbles in a binary literal
equalFlags : Bool
equalFlags = 0b0011_1111_0100_1110 == 0b0011111101001110

-- grouping octals
equalOctals : Bool
equalOctals = 0o455_777 == 0o455777


text:
{- Ctrl-Alt-A: Add definition
   Ctrl-Alt-C: Case split
   Ctrl-Alt-D: Documentation
   Ctrl-Alt-L: Lift hole: Lifts a hole to the top level as a new function definition
   Ctrl-Alt-M: Match: Replaces a hole with a case expression that matches on an intermediate result
   Ctrl-Alt-R: Reloads and typechecks the current buffer
   Ctrl-Alt-S: Search
   Ctrl-Alt-T: Type-check: Displays the type under cursor -}
module Main

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

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

data Expr' : Type -> Type where
  Val' : num -> Expr' num
  Add' : Num num => Expr' num -> Expr' num -> Expr' num
  Mul' : Num num => Expr' num -> Expr' num -> Expr' num
  Sub' : Neg neg => Expr' neg -> Expr' neg -> Expr' neg
  Div' : Integral int => Expr' int -> Expr' int -> Expr' int
  Abs' : Abs abs => Expr' abs -> Expr' abs

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

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

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

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

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

(Eq ty, Integral ty, Neg ty, Abs ty) => Eq (Expr ty) where
  e1 == e2 = eval e1 == eval e2

(Integral ty, Neg ty, Abs ty) => Cast (Expr ty) ty where
  cast e = eval e

totalLen : List String -> Nat
totalLen xs = foldr (\str, len => length str + len) 0 xs

main : IO ()
main = do
  putStrLn "Expr"
  printLn $ eval $ the (Expr Integer) (Add (Val 6) (Mul (Val 3) (Val 12)))
  printLn $ eval $ the (Expr Integer) (6 + 3 * 12)
  printLn $ the (Expr Integer) (6 + 3 * 12)
  printLn $ eval' $ the (Expr' Integer) (Add' (Val' 6) (Mul' (Val' 3) (Val' 12)))
  printLn $ map (*2) [1,2,3,4]
  printLn $ foldr (+) 0 [1,2,3,4]
  printLn $ foldr (*) 1 [1,2,3,4]
  printLn $ totalLen ["One", "Two", "Three"]

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
-- Module      : Itea.Program
-- Description :
-- Copyright   : (c) Simon Nielsen Knights 2018
-- License     : MIT
-- Maintainer  : simonank@mail.ru
-- Stability   : unstable
-- Portability : portable

module Itea.Program
import Itea.Html
import Itea.Dom.Primitives

%default total
%access public export

||| Commands
data Cmd : Type -> Type where

||| Subscriptions
data Sub : Type -> Type where

||| Data representation of the program which carries all information
||| to run the applicationg indefinetly
|||
||| @model the used supplied model (state) for the program
||| @msg the message type representing user actions
record Program model msg where
  constructor MkProgram
  ||| Initial state
  init          : (model, Cmd msg)
  ||| Update function used to advance state by one step
  update        : msg -> model -> (model, Cmd msg)
  ||| Subscription to services which fire events upon completion
  subscriptions : model -> Sub msg
  ||| View constructing the DOM tree
  view          : model -> Html msg

runProgram : Program model msg -> JS_IO ()
runProgram (MkProgram init update subscriptions view) = loop init

  where

    -- The main event loop handles fetching events from the event
    -- queue, values from subscriptions. This provides the interface
    -- where we focus on events over time rather than having to deal
    -- explicitly with the looping details ourselves.
    loop : (model, Cmd msg) -> JS_IO ()
    loop =
      do ?k
         -- setTimeout (loop ?p) 50
         -- pure ()

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea


text:
module Control.Monad.Maybe

-------------------------------------------------
-- The monad transformer `MaybeT m a` equips a monad with the ability to
-- return no value at all.

-- Sequenced actions of `MaybeT m a` produce a value `a` only if all of the
-- actions in the sequence returned a value.

-- This is isomorphic to `EitherT ()` and therefore less powerful than `EitherT e a`
-- ability to not return a result.
-------------------------------------------------

import Control.Monad.Trans
import Data.Maybe

%default total

public export
data MaybeT : (m : Type -> Type) -> (a : Type) -> Type where
  MkMaybeT : m (Maybe a) -> MaybeT m a

public export
%inline
runMaybeT : MaybeT m a -> m (Maybe a)
runMaybeT (MkMaybeT x) = x

public export
%inline
isNothingT : Functor m => MaybeT m a -> m Bool
isNothingT = map isNothing . runMaybeT

public export
%inline
isJustT : Functor m => MaybeT m a -> m Bool
isJustT = map isJust . runMaybeT

public export
%inline
maybeT : Monad m => m b -> (a -> m b) -> MaybeT m a -> m b
maybeT v g x = runMaybeT x >>= maybe v g

public export
%inline
fromMaybeT : Monad m => m a -> MaybeT m a -> m a
fromMaybeT v x = runMaybeT x >>= maybe v pure

public export
%inline
toMaybeT : Functor m => Bool -> m a -> MaybeT m a
toMaybeT b m = MkMaybeT $ map (\a => toMaybe b a) m

||| map the underlying computation
||| The basic 'unwrap, apply, rewrap' of this transformer.
public export
%inline
mapMaybeT : (m (Maybe a) -> n (Maybe a')) -> MaybeT m a -> MaybeT n a'
mapMaybeT f = MkMaybeT . f . runMaybeT

||| Analogous to Just, aka pure for MaybeT
public export
%inline
just : Applicative m => a -> MaybeT m a
just = MkMaybeT . pure . Just

||| Analogous to Nothing, aka empty for MaybeT
public export
%inline
nothing : Applicative m => MaybeT m a
nothing = MkMaybeT $ pure Nothing

-------------------------------------------------
-- Interface Implementations
-------------------------------------------------

public export
Eq (m (Maybe a)) => Eq (MaybeT m a) where
 (==) = (==) `on` runMaybeT

public export
Ord (m (Maybe a)) => Ord (MaybeT m a) where
 compare = compare `on` runMaybeT

public export
Show (m (Maybe a)) => Show (MaybeT m a) where
  showPrec d (MkMaybeT x) = showCon d "MkMaybeT" $ showArg x

||| Corresponds to the Semigroup instance of Maybe
|||
||| Note: This could also be implemented with only an Applicative
||| prerequisite: `MkMaybeT x <+> MkMaybeT y = MkMaybeT $ [| x <+> y |]`
||| However, the monadic version is more efficient for long-running effects,
||| only evaluating the second argument if the first returns `Nothing`.
public export
Monad m => Semigroup (MaybeT m a) where
  MkMaybeT x <+> MkMaybeT y = MkMaybeT $ do
    r@(Just _) <- x | Nothing => y
    pure r

public export
Monad m => Monoid (MaybeT m a) where
  neutral = nothing

public export
Functor m => Functor (MaybeT m) where
  map f m = MkMaybeT $ map f <$> runMaybeT m

public export
Foldable m => Foldable (MaybeT m) where
  foldr f acc (MkMaybeT e)
    = foldr (\x,xs => maybe xs (`f` xs) x) acc e

  null (MkMaybeT e) = null e

public export
Traversable m => Traversable (MaybeT m) where
  traverse f (MkMaybeT x)
    = MkMaybeT <$> traverse (maybe (pure Nothing) (map Just . f)) x

public export
Applicative m => Applicative (MaybeT m) where
  pure = just
  MkMaybeT f <*> MkMaybeT x = MkMaybeT [| f <*> x |]

public export
Monad m => Monad (MaybeT m) where
  MkMaybeT x >>= k = MkMaybeT $ x >>= maybe (pure Nothing) (runMaybeT . k)

||| See note about Monad prerequisite on Semigroup instance.
public export
Monad m => Alternative (MaybeT m) where
  empty = nothing
  MkMaybeT x <|> my = MkMaybeT $ x >>= \case
    r@(Just _) => pure r
    Nothing    => runMaybeT my

public export
MonadTrans MaybeT where
  lift = MkMaybeT . map Just

public export
HasIO m => HasIO (MaybeT m) where
  liftIO act = MkMaybeT $ liftIO (io_bind act (pure . Just))


text:
module Vimscript.FFI

%default total

mutual
  public export
  data VimFn t = MkVimFn t

  public export
  data VIM_FnTypes : Type -> Type where
    VIM_Fn : VIM_Types s -> VIM_FnTypes t -> VIM_FnTypes (s -> t)
    VIM_FnIO : VIM_Types t -> VIM_FnTypes (IO' l t)
    VIM_FnBase : VIM_Types t -> VIM_FnTypes t

  public export
  data VIM_Types : Type -> Type where
    VIM_Str    : VIM_Types String
    VIM_Int    : VIM_Types Int
    VIM_Float  : VIM_Types Double
    VIM_Unit   : VIM_Types ()
    VIM_Raw    : VIM_Types (Raw a)
    VIM_FnT    : VIM_FnTypes t -> VIM_Types (VimFn t)

public export
data VIM_Scope
  = VIM_Local
  | VIM_Global

public export
data VIM_MutableRef
  = VIM_Option
  | VIM_ScopedOption VIM_Scope
  | VIM_Register

public export
VIM_GlobalOption : VIM_MutableRef
VIM_GlobalOption = VIM_ScopedOption VIM_Global

public export
VIM_LocalOption : VIM_MutableRef
VIM_LocalOption = VIM_ScopedOption VIM_Local

public export
data VIM_Foreign
  = VIM_Echo
  | VIM_ListEmpty
  | VIM_ListIndex
  | VIM_ListCons
  | VIM_ListSnoc
  | VIM_ListConcat
  | VIM_ListSetAt
  | VIM_BuiltIn String
  | VIM_Get VIM_MutableRef String
  | VIM_Set VIM_MutableRef String
  | VIM_Toggle VIM_MutableRef String

%error_reverse
public export
FFI_VIM : FFI
FFI_VIM = MkFFI VIM_Types VIM_Foreign String

%error_reverse
public export
VIM_IO : Type -> Type
VIM_IO = IO' FFI_VIM

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

max_stars_repo_name: owickstrom/idris-vimscript

max_issues_repo_name: owickstrom/idris-vimscript

max_forks_repo_name: owickstrom/idris-vimscript


text:
||| Spec: http://webassembly.github.io/spec/core/syntax/types.html#memory-types
module WebAssembly.Structure.Types.MemoryTypes

import WebAssembly.Structure.Types.Limits

-- Definition

public export
MemType : Type
MemType = Limits

-- Equality
-- See Limits

-- Decidable Equality
-- See Limits

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Derive.Common

import public Language.Reflection

-- nat casting is slow
export
intLength : List a -> Int
intLength = foldl (\xs,_ => 1 + xs) 0

export
eFC : FC
eFC = EmptyFC

export
toIVar : Name -> TTImp
toIVar = IVar eFC

export
toIBindVar : String -> TTImp
toIBindVar = IBindVar eFC

export
guard : Bool -> String -> Elab ()
guard p s = if p then pure () else fail s

export
nameStr : Name -> String
nameStr (UN x) = x
nameStr (MN x y) = x
nameStr (NS xs x) = nameStr x
nameStr (DN x y) = x
nameStr (RF n) = n

export
mapName : (String -> String) -> Name -> Name
mapName f (UN x) = UN (f x)
mapName f (MN x y) = MN (f x) y
mapName f (NS x y) = NS x (mapName f y)
mapName f (DN x y) = DN (f x) y
mapName f (RF n) = RF (f n)

export
lookupType : Name -> Elab (Name, TTImp)
lookupType n = do
  [res@(qname,ttimp)] <- getType n
    | _ => fail $ show n ++ " is not unique in scope."
  pure res

export
constructors : Name -> Elab (List (Name, TTImp))
constructors x = do
  cons <- getCons x
  for cons lookupType

export
conNames : Name -> Elab (List Name)
conNames x = map fst <$> constructors x

export
argCount : TTImp -> Nat
argCount (IPi _ _ _ _ _ retty) = S (argCount retty)
argCount retty = Z

export
getTTImpFC : TTImp -> FC
getTTImpFC (IVar fc _) = fc
getTTImpFC (IPi fc _ _ _ _ _) = fc
getTTImpFC (ILam fc _ _ _ _ _) = fc
getTTImpFC (ILet fc _ _ _ _ _ _) = fc
getTTImpFC (ICase fc _ _ _) = fc
getTTImpFC (ILocal fc _ _) = fc
getTTImpFC (IUpdate fc _ _) = fc
getTTImpFC (IApp fc _ _) = fc
getTTImpFC (INamedApp fc _ _ _) = fc
getTTImpFC (IAutoApp fc _ _) = fc
getTTImpFC (IWithApp fc _ _) = fc
getTTImpFC (ISearch fc _) = fc
getTTImpFC (IAlternative fc _ _) = fc
getTTImpFC (IRewrite fc _ _) = fc
getTTImpFC (IBindHere fc _ _) = fc
getTTImpFC (IBindVar fc _) = fc
getTTImpFC (IAs fc _ _ _ _) = fc
getTTImpFC (IMustUnify fc _ _) = fc
getTTImpFC (IDelayed fc _ _) = fc
getTTImpFC (IDelay fc _) = fc
getTTImpFC (IForce fc _) = fc
getTTImpFC (IQuote fc _) = fc
getTTImpFC (IQuoteName fc _) = fc
getTTImpFC (IQuoteDecl fc _) = fc
getTTImpFC (IUnquote fc _) = fc
getTTImpFC (IPrimVal fc _) = fc
getTTImpFC (IType fc) = fc
getTTImpFC (IHole fc _) = fc
getTTImpFC (Implicit fc _) = fc
getTTImpFC (IWithUnambigNames fc _ _) = fc


text:
||| A key-value tree data structure.
|||
||| This structure doesn't encode the invariants of the tree and is
||| *simply* a container. This structure ideally shouldn't be exposed
||| to the user at all. This structure should be used to build other
||| data structures.  See the modules alongside this for appropriate
||| interfaces for using the tree.
|||
||| @keyTy The type associated with the key.
data Tree : (keyTy : Type)
         -> Type
  where
    ||| An empty Tree node.
    Empty : Tree k

    ||| A Key Value node in the Tree.
    |||
    ||| @key   The key.
    ||| @left  The left child of the Node
    ||| @right THe right child of the Node.
    Node : (key   : k)
        -> (left  : Tree k)
        -> (right : Tree k)
        -> Tree k

%name Tree t, tree

 -- ------------------------------------------------------------- [ Definitions ]
data Balance : Nat -> Nat -> Type where
  LHeavy   : Balance (S n) n
  RHeavy   : Balance n     (S n)
  Balanced : Balance n     n

%name Balance b, bal

||| Indirection ensures that it reduces to at least S n' without
||| needing to case split on balance.
|||
||| Should make proofs easier.
height : Balance n m -> Nat
height b = S (height' b)
  where
    height' : Balance n m -> Nat
    height' (LHeavy {n}) = S n
    height' (RHeavy {n}) = S n
    height' {n} (Balanced {n}) = n

||| Encoding of the AVL tree height invariants.
|||
||| @height The height of a Tree.
||| @tree   The tree whose height we are capturing.
data AVLInvariant : (height : Nat)
                 -> (tree   : Tree k)
                 -> Type
  where
    ||| A tree of height zero.
    AVLEmpty : AVLInvariant 0 Empty
    ||| A Balanced tree.
    |||
    ||| @left  The invariant of the left child.
    ||| @right The invariant of the right child.
    ||| @b     The encoding of the nodes' balance.
    AVLNode : (left  : AVLInvariant n l)
           -> (right :  AVLInvariant m r)
           -> (b : Balance n m)
           -> AVLInvariant (height b) (Node k l r)

%name AVLInvariant inv

||| An AVL Tree.
|||
||| Modelled using subset to separate the invariants from the tree
||| implementation itself.
|||
||| @height  The height of the Tree.
||| @keyTy   The type associated with the keys.
AVLTree : (height  : Nat)
       -> (keyTy   : Type)
       -> Type
AVLTree n k = Subset (Tree k) (AVLInvariant n)

-- --------------------------------------------------------------- [ Rotations ]
data InsertRes : Nat -> (k : Type) -> Type where
  Same : AVLTree n k     -> InsertRes n k
  Grew : AVLTree (S n) k -> InsertRes n k

%name InsertRes res, r

||| Process the result of an insertion of a new Key-Value pair into
||| the Tree, returning the new tree and proof of the new tree's
||| height.
|||
||| `InsertRes` is obtained from the result of running `Tree.insert`.
runInsertRes : InsertRes n k -> (n : Nat ** AVLTree n k)
runInsertRes (Same t) = (_ ** t)
runInsertRes (Grew t) = (_ ** t)

||| Perform a Left rotation.
rotLeft : k
       -> AVLTree n k
       -> AVLTree (S (S n)) k
       -> InsertRes (S (S n)) k
-- Impossible because Empty has depth 0 and we know the depth is at least 2 from the type
rotLeft key l (Element Empty AVLEmpty) impossible

rotLeft key (Element l invl) (Element (Node key' rl rr) (AVLNode invrl invrr Balanced)) =
    Grew $ Element (Node key' (Node key l rl) rr)
                        (AVLNode (AVLNode invl invrl RHeavy) invrr LHeavy)

rotLeft key (Element l invl) (Element (Node key' (Node key'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr LHeavy) invrr LHeavy)) =
    Same $ Element (Node key'' (Node key l rll) (Node key' rlr rr)) -- Needs Checking
                   (AVLNode (AVLNode invl invrll Balanced) (AVLNode invrlr invrr RHeavy) Balanced)

rotLeft key (Element l invl) (Element (Node key' (Node key'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr RHeavy) invrr LHeavy)) =
    Same $ Element (Node key'' (Node key l rll) (Node key' rlr rr))
                   (AVLNode (AVLNode invl invrll LHeavy) (AVLNode invrlr invrr Balanced) Balanced)

rotLeft key (Element l invl) (Element (Node key' (Node key'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr Balanced) invrr LHeavy)) =
    Same $ Element (Node key'' (Node key l rll) (Node key' rlr rr))
                   (AVLNode (AVLNode invl invrll Balanced) (AVLNode invrlr invrr Balanced) Balanced) -- Needs Checking

rotLeft key (Element l invl) (Element (Node key' rl rr) (AVLNode invrl invrr RHeavy)) =
    Same $ Element (Node key' (Node key l rl) rr)
                   (AVLNode (AVLNode invl invrl Balanced) invrr Balanced)

||| Perform a Right rotation.
rotRight : k
        -> AVLTree (S (S n)) k
        -> AVLTree n k
        -> InsertRes (S (S n)) k
rotRight key (Element Empty AVLEmpty) r impossible

rotRight key'' (Element (Node key ll (Node key' lrl lrr))
             (AVLNode invll (AVLNode invlrl invlrr RHeavy) RHeavy)) (Element r invr) =
  Same $ Element (Node key' (Node key ll lrl) (Node key'' lrr r))
                 (AVLNode (AVLNode invll invlrl LHeavy) (AVLNode invlrr invr Balanced) Balanced)
rotRight key'' (Element (Node key ll (Node key' lrl lrr))
             (AVLNode invll (AVLNode invlrl invlrr LHeavy) RHeavy)) (Element r invr) =
  Same $ Element (Node key' (Node key ll lrl) (Node key'' lrr r))
                 (AVLNode (AVLNode invll invlrl Balanced) (AVLNode invlrr invr RHeavy) Balanced)
rotRight key (Element (Node key' ll lr) (AVLNode invll invlr Balanced)) (Element r invr) =
  Grew $ Element (Node key' ll (Node key lr r))
                 (AVLNode invll (AVLNode invlr invr LHeavy) RHeavy)

rotRight key (Element (Node key' ll lr) (AVLNode invll invlr LHeavy)) (Element r invr) =
  Same $ Element (Node key' ll (Node key lr r))
                 (AVLNode invll (AVLNode invlr invr Balanced) Balanced)

rotRight key (Element (Node key' ll (Node key'' lrl lrr))
             (AVLNode invll (AVLNode invlrl invlrr Balanced) RHeavy)) (Element r invr) =
  Same $ Element (Node key'' (Node key' ll lrl) (Node key lrr r))
                 (AVLNode (AVLNode invll invlrl Balanced) (AVLNode invlrr invr Balanced) Balanced)

 --------------------------------------------------------------- [ Insertion ]

||| Perform an insertion into the tree returning the new tree wrapped
||| in a description describing the height change.
doInsert : (Ord k)
         => k
         -> AVLTree n k
         -> InsertRes n k
doInsert newKey (Element Empty AVLEmpty) = Grew (Element (Node newKey Empty Empty)
                                                       (AVLNode AVLEmpty AVLEmpty Balanced))
doInsert newKey (Element (Node key l r) (AVLNode invl invr b)) with (compare newKey key)
  doInsert newKey (Element (Node key l r) (AVLNode invl invr b)) | EQ = Same (Element (Node newKey l r) (AVLNode invl invr b))

  doInsert newKey (Element (Node key l r) (AVLNode invl invr b)) | LT with (assert_total $ doInsert newKey (Element l invl))
    -- Totality checker not clever enough to see that this is smaller
    doInsert newKey (Element (Node key l r) (AVLNode invl invr b))        | LT | (Same (Element l' invl'))
                                                                               = Same $ Element (Node key l' r) (AVLNode invl' invr b)
    doInsert newKey (Element (Node key l r) (AVLNode invl invr LHeavy))   | LT | (Grew (Element l' invl'))
                                                                               = rotRight key (Element l' invl') (Element r invr)
    doInsert newKey (Element (Node key l r) (AVLNode invl invr Balanced)) | LT | (Grew (Element l' invl'))
                                                                               = Grew $ Element (Node key l' r) (AVLNode invl' invr LHeavy)
    doInsert newKey (Element (Node key l r) (AVLNode invl invr RHeavy))   | LT | (Grew (Element l' invl'))
                                                                               = Same $ Element (Node key l' r) (AVLNode invl' invr Balanced)

  doInsert newKey (Element (Node key l r) (AVLNode invl invr b)) | GT with (assert_total $ doInsert newKey (Element r invr))
  -- Totality checker not clever enough to see that this is smaller
    doInsert newKey (Element (Node key l r) (AVLNode invl invr b))        | GT | (Same (Element r' invr'))
                                                                               = Same $ Element (Node key l r') (AVLNode invl invr' b)
    doInsert newKey (Element (Node key l r) (AVLNode invl invr LHeavy))   | GT | (Grew (Element r' invr'))
                                                                               = Same $ Element (Node key l r') (AVLNode invl invr' Balanced)
    doInsert newKey (Element (Node key l r) (AVLNode invl invr Balanced)) | GT | (Grew (Element r' invr'))
                                                                               = Grew $ Element (Node key l r') (AVLNode invl invr' RHeavy)
    doInsert newKey (Element (Node key l r) (AVLNode invl invr RHeavy))   | GT | (Grew (Element r' invr'))
                                                                               = rotLeft key (Element l invl) (Element r' invr')

||| Insert a key value pair into the tree, returning a the new tree
||| and possibly its new height.
insert : Ord k => k -> AVLTree n k -> (n : Nat ** AVLTree n k)
insert k t = runInsertRes (doInsert k t)

||| AVL instance implementation
|||
||| @ty The type of the elements in the tree.
data AVLImpl : (ty : Type) -> Type
    where
      MkTree : {a : Type } -> AVLTree n a -> AVLImpl a

||| Insert an element into the Tree.
insertImpl : (Ord a) => a -> AVLImpl a -> AVLImpl a
insertImpl a (MkTree t) = MkTree (snd $ insert a t)

max_stars_repo_name: LucasTornai/pgc-ufabc

max_issues_repo_name: LucasTornai/pgc-ufabc

max_forks_repo_name: LucasTornai/pgc-ufabc


text:
module Test.Main

import Test.Char
import Test.Bits8
import Test.Bits16
import Test.Bits32
import Test.Bits64
import Test.Int8
import Test.Int16
import Test.Int32
import Test.Int64
import Test.Int
import Test.Integer
import Test.String
import Hedgehog

main : IO ()
main = test
  [ Char.props
  , Bits8.props
  , Bits16.props
  , Bits32.props
  , Bits64.props
  , Int8.props
  , Int16.props
  , Int32.props
  , Int64.props
  , Int.props
  , Integer.props
  , String.props
  ]


text:
-- ------------------------------------------------------- [ StateMachines.idr ]
-- Module      : Exercises.StateMachines
-- Description : Solutions to the Chapter 13 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.StateMachines

import public Chapter.StateMachines

%access export

-- -------------------------------------------------------- [ 13.1.5 Exercises ]

public export
data GuessCmd : Type -> Nat -> Nat -> Type where
     Try : Integer -> GuessCmd Ordering (S n) n

     Pure : ty -> GuessCmd ty state state
     (>>=) : GuessCmd a state1 state2 ->
             (a -> GuessCmd b state2 state3) ->
             GuessCmd b state1 state3

export
threeGuesses : GuessCmd () 3 0
threeGuesses = do Try 10
                  Try 20
                  Try 15
                  Pure ()

-- NOTE: noGuesses should not type check.
-- noGuesses : GuessCmd () 0 0
-- noGuesses = do Try 10
--                Pure ()

namespace Matter

  public export
  data Matter = Solid | Liquid | Gas

  public export
  data MatterCmd : (ty : Type) ->
                   (beforeState, afterState : Matter) ->
                   Type where
       Melt : MatterCmd () Solid Liquid
       Boil : MatterCmd () Liquid Gas
       Condense : MatterCmd () Gas Liquid
       Freeze : MatterCmd () Liquid Solid

       Pure : ty -> MatterCmd ty state state
       (>>=) : MatterCmd a state1 state2 ->
               (a -> MatterCmd b state2 state3) ->
               MatterCmd b state1 state3

export
iceSteam : MatterCmd () Solid Gas
iceSteam = do Melt
              Boil

export
steamIce : MatterCmd () Gas Solid
steamIce = do Condense
              Freeze

-- NOTE: overMelt should not type check.
-- overMelt : MatterCmd () Solid Gas
-- overMelt = do Melt
--               Melt

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Data.Fin.FinOrdering
-- Classes (OrdRel, DecLT) are redundant with IntegerOrdering.idr

import Data.Fin
import Data.ZZ

%default total

{-
Definitions
-}

-- Note that unlike (=) the types do not inherently need to be ambiguous
class OrdRel A where
	LTRel : A -> A -> Type

LTERel : OrdRel s => s -> s -> Type
LTERel a b = Either (LTRel a b) (a=b)

class (OrdRel s) => DecLT s where
	decLT : (x1 : s) -> (x2 : s) -> Dec ( LTRel x1 x2 )

class (OrdRel s) => DecLTE s where
	decLTE : (x1 : s) -> (x2 : s) -> Dec ( LTERel x1 x2 )

implDeclte : (DecLT s, DecEq s) => (a, b: s) -> Dec ( LTERel a b )
implDeclte a b with (decEq a b)
	| Yes x = Yes (Right x)
	| No x with (decLT a b)
		| Yes y = Yes (Left {b=(a=b)} y)
		| No y = No (either y x)

{-
Won't let us work with this at all.
---
instance (DecLT s, DecEq s) => DecLTE s where
	-- decLTE = implDeclte
	decLTE = ?declte_from_ltNeq

=====

Compiles but doesn't resolve any of the falsely split instances
---
instance (OrdRel s, DecLT s, DecEq s) => DecLTE s where
	decLTE ?= implDeclte {s=s} @{the (DecLT s) %instance} @{the (DecEq s) %instance}

=====

Other things we tried
---

instance (OrdRel s, DecLT s, DecEq s) => DecLTE s where
	decLTE ?= implDeclte {s=s} @{the (OrdRel s) %instance} @{the (DecLT s) %instance} @{the (DecEq s) %instance}

instance (OrdRel s, DecLT s, DecEq s) => DecLTE s where
	decLTE = ?declte_from_ltNeq
-}

instance OrdRel Nat where
	LTRel = LT

instance DecLT Nat where
	decLT a b = isLTE (S a) b

||| Normalizes the notion of decidable LTE provided by Prelude.Nat.isLTE.
decLTENat : (n, m : Nat) -> Dec ( LTERel n m )
decLTENat a b with (decEq a b)
	| Yes pr = Yes (Right pr)
	| No prneq with (decLT a b)
		| Yes pr = Yes (Left pr)
		| No pr = No ( either pr prneq )

instance DecLTE Nat where
	decLTE = decLTENat

{-
-- Just use `finToNat`.
instance DecLT (Fin n) where
	decLT {n} = decLTFin n
-}

{-
Equivalence between LTERel and LTE
-}

lteToLTERel : {a, b : Nat} -> LTE a b -> LTERel a b
lteToLTERel LTEZero {b=Z} = Right Refl
lteToLTERel LTEZero {b=S predb} = Left $ LTESucc $ LTEZero {right=predb}
lteToLTERel (LTESucc ltepr) {a=S preda} {b=S predb} = either
	(Left . LTESucc)
	(Right . (cong {f=S}))
	$ lteToLTERel ltepr

lteRelToLTE : LTERel a b -> LTE a b
lteRelToLTE (Left lt) = fromLteSucc . lteSuccRight $ lt
lteRelToLTE (Right pr) = rewrite pr in lteRefl

{-
Productions
-}

zLtSuccIsTrue : (k : Nat) -> LTRel Z (S k)
zLtSuccIsTrue _ = LTESucc LTEZero

natGtAnyImpliesGtZ : (m, n : Nat) -> LTRel m n -> LTRel Z n
natGtAnyImpliesGtZ m Z = absurd
natGtAnyImpliesGtZ m (S n) = const $ zLtSuccIsTrue n


text:
module Main

-- base
import Data.List
import Data.Strings
import System.File

-- contrib
import Data.SortedMap
import Text.Lexer
import Text.Lexer.Core
import Text.Parser
import Text.Parser.Core
import Text.Token

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

namespace Rules

  data Terminal = A
                | B

  Eq Terminal where
    A == A = True
    B == B = True
    _ == _ = False

  Show Terminal where
    show A = "A"
    show B = "B"

  data Ruleset : Type where
    Match : Terminal -> Ruleset
    References : (references : List Nat ** NonEmpty references) -> Ruleset
    Option : Ruleset -> Ruleset -> Ruleset

  Show Ruleset where
    show (Match terminal) = "Match " ++ show terminal
    show (References (ns**_)) = "References " ++ show ns
    show (Option x y) = "Option " ++ show x ++ " " ++ show y

  record Rule where
    constructor MkRule
    number : Nat
    ruleset : Ruleset

  [EqNumber] Eq Rule where
    (MkRule number _) == (MkRule number' _) = number == number'

  [OrdNumber] Ord Rule using EqNumber where
    compare (MkRule number _) (MkRule number' _) = compare number number'

  Show Rule where
    show (MkRule number ruleset) = "Rule " ++ show number ++ " " ++ show ruleset

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

namespace RulesParsing

  data RulesKind = RKNumber
                 | RKCharA
                 | RKCharB
                 | RKColon
                 | RKSpace
                 | RKPipe
                 | RKQuotationMarks

  Eq RulesKind where
    RKNumber == RKNumber = True
    RKCharA == RKCharA = True
    RKCharB == RKCharB = True
    RKColon == RKColon = True
    RKSpace == RKSpace = True
    RKPipe == RKPipe = True
    RKQuotationMarks == RKQuotationMarks = True
    _ == _ = False

  TokenKind RulesKind where
    TokType RKNumber = Nat
    TokType _ = ()
    tokValue RKNumber x = integerToNat $ cast x
    tokValue RKCharA _ = ()
    tokValue RKCharB _ = ()
    tokValue RKColon _ = ()
    tokValue RKSpace _ = ()
    tokValue RKPipe _ = ()
    tokValue RKQuotationMarks _ = ()

  tokenMap : TokenMap $ Token RulesKind
  tokenMap = toTokenMap
    [ (digits, RKNumber)
    , (is 'a', RKCharA)
    , (is 'b', RKCharB)
    , (is ':', RKColon)
    , (spaces, RKSpace)
    , (is '|', RKPipe)
    , (is '"', RKQuotationMarks)
    ]

  grammarRuleset : Grammar (Token RulesKind) True Ruleset
  grammarRuleset = grammarOption <|> grammarReferences <|> grammarMatch where
    grammarMatch : Grammar (Token RulesKind) True Ruleset
    grammarMatch = do
      match RKQuotationMarks
      terminal <- (match RKCharA *> pure A) <|> (match RKCharB *> pure B)
      match RKQuotationMarks
      pure $ Match terminal
    grammarReferences : Grammar (Token RulesKind) True Ruleset
    grammarReferences = References <$> sepBy1' (match RKSpace) (match RKNumber)
    grammarOption : Grammar (Token RulesKind) True Ruleset
    grammarOption = do
      left <- (grammarMatch <|> grammarReferences)
      match RKSpace
      match RKPipe
      match RKSpace
      right <- (grammarMatch <|> grammarReferences)
      pure $ Option left right

  grammarRule : Grammar (Token RulesKind) True Rule
  grammarRule = do
    number <- match RKNumber
    match RKColon
    match RKSpace
    ruleset <- grammarRuleset
    eof
    pure $ MkRule number ruleset

  export
  readRule : String -> Maybe Rule
  readRule str = do
    let (tokens, debugLexed) = lex tokenMap str
        parsed = parse grammarRule $ tok <$> tokens
    case parsed of
         Left _ => Nothing
         Right (rule, _) => Just rule

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

namespace ParserCombination

  ruleMap : List Rule -> SortedMap Nat Ruleset
  ruleMap rules = fromList $ extract <$> rules where
    extract : Rule -> (Nat, Ruleset)
    extract (MkRule number ruleset) = (number, ruleset)

  public export
  TestGrammar : Type
  TestGrammar = Grammar Terminal True ()

  TestGrammarMap : Type
  TestGrammarMap = SortedMap Nat TestGrammar

  lookupTestGrammar : TestGrammarMap -> Nat -> Maybe TestGrammar
  lookupTestGrammar = flip lookup

  mapOnDPair : (f : a -> b) -> (xs : List a ** NonEmpty xs) -> (ys : List b ** NonEmpty ys)
  mapOnDPair f ([x] ** IsNonEmpty) = ([f x] ** IsNonEmpty)
  mapOnDPair f ((x :: x' :: xs) ** IsNonEmpty) with (mapOnDPair f ((x' :: xs) ** IsNonEmpty))
    mapOnDPair f ((x :: x' :: xs) ** IsNonEmpty) | ((y :: ys) ** IsNonEmpty) = ((f x :: y :: ys) ** IsNonEmpty)

  lookupTestGrammars' : TestGrammarMap -> (references : List Nat ** NonEmpty references) ->
                                          (grammars : List (Maybe TestGrammar) ** NonEmpty grammars)
  lookupTestGrammars' map refs = mapOnDPair (lookupTestGrammar map) refs

  takeMaybeOutProof : (xs : List (Maybe a) ** NonEmpty xs) -> Maybe (ys : List a ** NonEmpty ys)
  takeMaybeOutProof ([ Nothing ] ** IsNonEmpty) = Nothing
  takeMaybeOutProof ([ Just x ] ** IsNonEmpty) = Just ([ x ] ** IsNonEmpty)
  takeMaybeOutProof ((Nothing :: x' :: xs) ** IsNonEmpty) = Nothing
  takeMaybeOutProof ((Just x :: x' :: xs) ** IsNonEmpty) with (takeMaybeOutProof ((x' :: xs) ** IsNonEmpty))
    takeMaybeOutProof ((Just x :: x' :: xs) ** IsNonEmpty) | Nothing = Nothing
    takeMaybeOutProof ((Just x :: x' :: xs) ** IsNonEmpty) | (Just dpair) = Just $ f x (g dpair) where
      f : a -> List a -> (bs : List a ** NonEmpty bs)
      f q qs = ((q :: qs) ** IsNonEmpty)
      g : (x : List a ** NonEmpty x) -> List a
      g (x ** y) = x

  lookupTestGrammars : TestGrammarMap -> (references : List Nat ** NonEmpty references) ->
                                         Maybe (grammars : List TestGrammar ** NonEmpty grammars)
  lookupTestGrammars map refs = takeMaybeOutProof $ lookupTestGrammars' map refs

  combineTestGrammars : TestGrammar -> TestGrammar -> TestGrammar
  combineTestGrammars x y = x *> y

  grammar : (ruleset : Ruleset) -> (grammars : TestGrammarMap) -> Maybe TestGrammar
  grammar (Match char) grammars =
    Just $ terminal "Failed to parse Terminal" test where
      test : Terminal -> Maybe ()
      test x = if x == char
                  then Just ()
                  else Nothing
  grammar (References references) grammars = do
    let testGrammarsStuff = lookupTestGrammars grammars references
    case testGrammarsStuff of
         Nothing => Nothing
         Just (testGrammars ** nonEmptyTestGrammarProof) =>
           Just $ foldl1 combineTestGrammars testGrammars
  grammar (Option leftRuleset rightRuleset) grammars =
    [| grammar leftRuleset grammars <|> grammar rightRuleset grammars |]

  grammarMap' : (rules : List Rule) -> TestGrammarMap -> TestGrammarMap
  grammarMap' [] acc = acc
  grammarMap' (rule@(MkRule number ruleset) :: rules) acc with (grammar ruleset acc)
    grammarMap' (rule@(MkRule number ruleset) :: rules) acc | Nothing = grammarMap' (rules ++ [rule]) acc
    grammarMap' (rule@(MkRule number ruleset) :: rules) acc | Just g = grammarMap' rules $ insert number g acc

  grammarMap : (rules : List Rule) -> TestGrammarMap
  grammarMap rules = grammarMap' rules empty

  export
  grammar0 : (rules : List Rule) -> Maybe TestGrammar
  grammar0 rules = lookup 0 $ grammarMap rules

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

  newGrammar8 : TestGrammarMap -> Maybe TestGrammar
  newGrammar8 gmap = do
    grammar42 <- lookupTestGrammar gmap 42
    let g : TestGrammar
        g = do
          grammar42
          optional g
          pure ()
    Just $ g

  newGrammar11 : TestGrammarMap -> Maybe TestGrammar
  newGrammar11 gmap = do
    grammar42 <- lookupTestGrammar gmap 42
    grammar31 <- lookupTestGrammar gmap 31
    let g : TestGrammar
        g = do
          grammar42
          optional g
          grammar31
          pure ()
    Just g

  contains8Or11 : List Nat -> Bool
  contains8Or11 [] = False
  contains8Or11 (8 :: _) = True
  contains8Or11 (11 :: _) = True
  contains8Or11 (_ :: ns) = contains8Or11 ns

  fromDepPair : (xs : List a ** NonEmpty xs) -> List a
  fromDepPair (xs ** _) = xs

  contains8Or11' : Ruleset -> Bool
  contains8Or11' (References refs) = contains8Or11 $ fromDepPair refs
  contains8Or11' _ = False

  grammar' : (ruleset : Rule) -> (grammars : TestGrammarMap) -> Maybe TestGrammar
  grammar' (MkRule 8 _) grammars = newGrammar8 grammars
  grammar' (MkRule 11 _) grammars = newGrammar11 grammars
  grammar' (MkRule _ (Match char)) grammars =
    Just $ terminal "Failed to parse Terminal" test where
      test : Terminal -> Maybe ()
      test x = if x == char
                  then Just ()
                  else Nothing
  grammar' (MkRule _ (References references)) grammars = do
    let testGrammarsStuff = lookupTestGrammars grammars references
    case testGrammarsStuff of
         Nothing => Nothing
         Just (testGrammars ** nonEmptyTestGrammarProof) =>
           Just $ foldl1 combineTestGrammars testGrammars
  grammar' (MkRule _ (Option leftRuleset rightRuleset)) grammars =
    if contains8Or11' leftRuleset
       then [| grammar' (MkRule 0 rightRuleset) grammars <|> grammar' (MkRule 0 leftRuleset) grammars |]
       else [| grammar' (MkRule 0 leftRuleset) grammars <|> grammar' (MkRule 0 rightRuleset) grammars |]

  grammar'Map' : (rules : List Rule) -> TestGrammarMap -> TestGrammarMap
  grammar'Map' [] acc = acc
  grammar'Map' (rule@(MkRule number ruleset) :: rules) acc with (grammar' rule acc)
    grammar'Map' (rule@(MkRule number ruleset) :: rules) acc | Nothing = grammar'Map' (rules ++ [rule]) acc
    grammar'Map' (rule@(MkRule number ruleset) :: rules) acc | Just g = grammar'Map' rules $ insert number g acc

  grammar'Map : (rules : List Rule) -> TestGrammarMap
  grammar'Map rules = grammar'Map' rules empty

  export
  grammar0' : (rules : List Rule) -> Maybe TestGrammar
  grammar0' rules = lookup 0 $ grammar'Map rules

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

namespace MessagesParsing

  toTerminal : Char -> Maybe Terminal
  toTerminal 'a' = Just A
  toTerminal 'b' = Just B
  toTerminal _ = Nothing

  export
  toTerminals : String -> Maybe $ List Terminal
  toTerminals message = traverse toTerminal $ unpack message

  export
  testMessage : TestGrammar -> List Terminal -> Bool
  testMessage grammar word =
    case parse (grammar <* eof) word of
         Left _ => False
         Right _ => True

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

main : IO ()
main = do
  rulesData <- readFile "./rules"
  messagesData <- readFile "./messages"
  case (lines <$> rulesData, lines <$> messagesData) of
       (Right rulesData, Right messagesData) => do
         let mbRules = sort @{OrdNumber} <$> sequence (readRule <$> rulesData)
             mbMessages = traverse toTerminals messagesData
         case (mbRules, mbMessages) of
              (Just rules, Just messages) => do
                --case grammar0 rules of
                --     Nothing => putStrLn "Can't construct grammar0"
                --     Just grammar => do
                --       let tests = testMessage grammar <$> messages
                --           countParsed = length $ filter id tests
                --       print countParsed
                case grammar0' rules of
                     Nothing => putStrLn "Can't construct grammar0'"
                     Just grammar => do
                       let tests = testMessage grammar <$> messages
                           countParsed = length $ filter id tests
                       print countParsed
              _ => pure ()
         pure ()
       _ => pure ()
  pure ()


text:
module Subst

-- This module constructs an expressively typed substitution
-- function 'subst' for substituting variables in the simply-typed
-- lambda calculus.
--
-- The key point is that the expressive type signature of the
-- function 'subst' can be read as the following theorem:
--
--    "Given a variable with de Bruijn index 'idx'.
--     Given further the terms
--       ts : Term sctx s, and
--       tt : Term ctx  t.
--     Then 'subst ts idx tt' has type 't' in context '(remove idx ctx)++sctx'."
--
-- Note that 'subst ts idx tt' is typically written as "tt[ts/(TVar idx)]".
--
-- Note that the theorem that is expressed by the type signature
-- of 'subst' is usually referred to as
--
--    *** the substitution lemma ***
--
-- and casually summarized as
--
--    *** substitution preserves type ***.
--

import Term

%default total

------------------------------------------------------------
-- Begin: SHIFTING, I.E. ADDING UNUSED VARIABLES TO CONTEXTS

-- When adding variables in 'ctx' in the middle of
-- a context 'ctx1++ctx2', de Bruijn indices must
-- be adjusted accordingly:
shift : (ctx : Context) -> HasType (ctx1++ctx2) t ->
        HasType (ctx1++(ctx++ctx2)) t
shift {ctx1 = []}         []       x        = x
shift {ctx1 = []}         (_::ctx) x        = Next $ shift {ctx1=[]} ctx x
shift {ctx1 = (_::ctx1')} ctx      First    = First
shift {ctx1 = (_::ctx1')} ctx      (Next x) = Next $ shift {ctx1=ctx1'} ctx x

shift' : (ctx : Context) -> HasType (ctx1++ctx2) t ->
         HasType ((ctx1++ctx)++ctx2) t
shift' {ctx1} {ctx2} ctx ht = let assoc = appendAssociative ctx1 ctx ctx2
                                  sh    = shift {ctx1=ctx1} {ctx2=ctx2} ctx ht
                              in rewrite (sym assoc) in sh

-- Adjust terms for the (unused) variables in 'ctx':
shiftTerm : (ctx : Context) -> Term (ctx1++ctx2) t ->
            Term (ctx1++(ctx++ctx2)) t
--
shiftTerm ctx (TVar ht) = let sht = shift ctx ht
                          in TVar sht
--
shiftTerm {ctx1} {ctx2} {t = t1:->:t2} ctx (TAbs e) =
  let e' = shiftTerm {ctx1=(t1::ctx1)} {ctx2=ctx2} ctx e
  in TAbs e'
--
shiftTerm {ctx1} {ctx2} ctx (TApp e1 e2) =
  let e1' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e1
      e2' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e2
  in TApp e1' e2'
--
shiftTerm {ctx1} {ctx2} ctx (TFix e) =
  let e' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e
  in TFix e'
--
shiftTerm ctx TZero = TZero
--
shiftTerm {ctx1} {ctx2} ctx (TSucc e) =
  let e' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e
  in TSucc e'
--
shiftTerm {ctx1} {ctx2} ctx (TPred e) =
  let e' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e
  in TPred e'
--
shiftTerm {ctx1} {ctx2} ctx (TIfz e1 e2 e3) =
  let e1' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e1
      e2' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e2
      e3' = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx e3
  in TIfz e1' e2' e3'

shiftTerm' : (ctx : Context) -> Term (ctx1++ctx2) t -> Term ((ctx1++ctx)++ctx2) t
shiftTerm' {ctx1} {ctx2} ctx ht = let assoc = appendAssociative ctx1 ctx ctx2
                                      sh    = shiftTerm {ctx1=ctx1} {ctx2=ctx2} ctx ht
                                  in rewrite (sym assoc) in sh

-- Shifting a de Bruijn index 'x' with the empty
-- context '[]' preserves the de Bruijn index 'x':
shiftNil : {ctx1 : Context} -> {ctx2 : Context} ->
           {t : Ty} -> {x : HasType (ctx1++ctx2) t} ->
           shift [] x = x
shiftNil {ctx1 = []}      {ctx2 = ctx2} {x = x}        = Refl
shiftNil {ctx1 = _::ctx'} {ctx2 = ctx2} {x = First}    = Refl
shiftNil {ctx1 = _::ctx'} {ctx2 = ctx2} {x = (Next x)} =
  let eq = shiftNil {ctx1=ctx'} {ctx2=ctx2} {x=x}
  in cong {f = \z => Next z} eq

-- Shifting a term 'e' with the empty
-- context '[]' preserves the term 'e':
shiftTermNil : {ctx1 : Context} -> {ctx2 : Context} ->
               {t : Ty} -> {e : Term (ctx1++ctx2) t} ->
               shiftTerm [] e = e
--
shiftTermNil {ctx1 = ctx1} {ctx2 = ctx2} {t=t} {e = (TVar ht)} =
  cong {f = \z => TVar z} $ shiftNil {ctx1=ctx1} {ctx2=ctx2} {t=t} {x=ht}
--
shiftTermNil {ctx1 = ctx1} {ctx2 = ctx2} {t=t1:->:t2} {e = (TAbs e')} =
  let eq = shiftTermNil {ctx1=(t1::ctx1)} {ctx2=ctx2} {t=t2} {e=e'}
  in cong {f = \z => TAbs z} eq
--
shiftTermNil {ctx1 = ctx1} {ctx2 = ctx2} {e = (TApp e1 e2)} =
  let eq1 = shiftTermNil {ctx1=ctx1} {ctx2=ctx2} {e=e1}
      eq2 = shiftTermNil {ctx1=ctx1} {ctx2=ctx2} {e=e2}
      c   = cong {f = \z => TApp z e2} eq1
      c'  = cong {f = \z => TApp (shiftTerm [] e1) z} eq2
  in trans c' c
--
shiftTermNil {ctx1 = ctx1} {ctx2 = ctx2} {e = (TFix e')} =
  let eq = shiftTermNil {ctx1=ctx1} {ctx2=ctx2} {e=e'}
  in cong {f = \z => TFix z} eq
--
shiftTermNil {ctx1 = ctx1} {ctx2 = ctx2} {e = TZero} = Refl
--
shiftTermNil {ctx1 = ctx1} {ctx2 = ctx2} {e = (TSucc e')} =
  let eq = shiftTermNil {ctx1=ctx1} {ctx2=ctx2} {e=e'}
  in cong {f = \z => TSucc z} eq
--
shiftTermNil {ctx1 = ctx1} {ctx2 = ctx2} {e = (TPred e')} =
  let eq = shiftTermNil {ctx1=ctx1} {ctx2=ctx2} {e=e'}
  in cong {f = \z => TPred z} eq
--
shiftTermNil {ctx1 = ctx1} {ctx2 = ctx2} {e = (TIfz e1 e2 e3)} =
  let eq1 = shiftTermNil {ctx1=ctx1} {ctx2=ctx2} {e=e1}
      eq2 = shiftTermNil {ctx1=ctx1} {ctx2=ctx2} {e=e2}
      eq3 = shiftTermNil {ctx1=ctx1} {ctx2=ctx2} {e=e3}
      c   = cong {f = \z => TIfz z e2 e3} eq1
      c'  = cong {f = \z => TIfz (shiftTerm [] e1) z e3} eq2
      c'' = cong {f = \z => TIfz (shiftTerm [] e1) (shiftTerm [] e2) z} eq3
  in trans (trans c'' c') c

-- End: SHIFTING, I.E. ADDING UNUSED VARIABLES TO CONTEXTS
----------------------------------------------------------

-----------------------------------------------------------------------------
-- Begin: SUBSTITUTION PRESERVES TYPING OF EXPRESSIONS IN THE LAMBDA CALCULUS

subst_var : Term sctx s ->            -- Term of type 's' is subtituted in.
            (idx : HasType ctx s) ->  -- Index of the variable in 'ctx' that is subsituted for.
                                      -- (and hence must have type 's').
            HasType ctx t ->          -- Substitution takes place inside the variable
                                      -- with this index.
            Term ((remove ctx idx)++sctx) t
--
subst_var {sctx} {s=s} {ctx=s::ctx'} {t=s} ts First First =
  shiftTerm' {ctx1=[]} {ctx2=sctx} ctx' ts
--
subst_var {sctx} {s=s} {ctx=s::ctx'} {t=t} ts First (Next htv) =
  let anr1 = sym $ appendNilRightNeutral ctx'
      htv1 = replace {P = \z => HasType z t} anr1 htv
      htv2 = shift {ctx1=ctx'} {ctx2=[]} sctx htv1
      anr2 = appendNilRightNeutral sctx
      htv3 = replace {P = \z => HasType (ctx'++z) t} anr2 htv2
   in TVar htv3
--
subst_var {sctx} {s=s} {ctx=u::ctx'} {t=u} ts (Next _) First = TVar First
--
subst_var {sctx} {s=s} {ctx=u::ctx'} {t=t} ts (Next x) (Next y) =
  let t' = subst_var ts x y
  in shiftTerm {ctx1=[]} {ctx2=(remove ctx' x)++sctx} [u] t'

export subst : Term sctx s ->            -- Term of type 's' is substituted in.
               (idx : HasType ctx s) ->  -- Index of the variable in 'ctx' that is substituted for
                                         -- (and hence must have type 's').
               Term ctx t  ->            -- Substitution takes place inside this
                                         -- term of type 't'
               Term ((remove ctx idx)++sctx) t
--
subst ts ht (TVar htv) = subst_var ts ht htv
--
subst {ctx} {t = t1:->:t2} ts ht (TAbs e) =
  TAbs $ subst {ctx=t1::ctx} ts (Next ht) e
--
subst ts ht (TApp e1 e2)    = TApp (subst ts ht e1) (subst ts ht e2)
subst ts ht (TFix e)        = TFix (subst ts ht e)
subst ts ht TZero           = TZero
subst ts ht (TSucc e)       = TSucc (subst ts ht e)
subst ts ht (TPred e)       = TPred (subst ts ht e)
subst ts ht (TIfz e1 e2 e3) = TIfz (subst ts ht e1)
                                   (subst ts ht e2)
                                   (subst ts ht e3)

-- Substituting a term 'e' into a single variable 'TVar First'
-- gives back the same term 'e' but in a shifted context:
substInVar' : (e : Term sctx t) ->
             subst {ctx=(t::ctx')} {s=t} {t=t} e First (TVar First) = shiftTerm {ctx1=[]} {ctx2=sctx} ctx' e
substInVar' e = Refl

-- Specialization of the previous result to a minimal
-- context '[t]' gives back exactly term 'e':
substInVar : (e : Term sctx t) ->
             subst {ctx=[t]} {s=t} {t=t} e First (TVar First) = e
substInVar {sctx} e = shiftTermNil {ctx1=[]} {ctx2=sctx} {e=e}

-- End: SUBSTITUTION PRESERVES TYPING OF EXPRESSIONS IN THE LAMBDA CALCULUS
---------------------------------------------------------------------------

--------------------------------
-- Begin: DIVERGING TERM 'omega'

-- Define 'omega' to be the diverging term that
-- is the fix-point of the identity function:
public export omega : Term [] TyNat
omega = TFix (TAbs $ TVar First)

-- To show (later) that 'omega' diverges, one needs the result that
-- substituting 'omega' into a single variable 'TVar FZ' reproduces
-- the term 'omega' itself:
export substOmega : subst {ctx=[TyNat]} {s=TyNat} {t=TyNat} Subst.omega First (TVar First) = Subst.omega
-- Note that while 'substOmega' is a special case of the more general
-- result 'substInVar' (see above), the general result is in fact not
-- needed. This is because the Idris type checker can evaluate
-- 'shiftTerm _ omega' (resulting from 'subst'), but it cannot
-- evaluate 'shiftTerm _ e' for a variable 'e' because 'shiftTerm'
-- is defined by recursion on the structure of 'e'.
substOmega = Refl

-- End: DIVERGING TERM 'omega'
------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Utils

import Data.Vect

cycle : (xs : Vect (S n) a) -> Stream a
cycle (x :: xs) = x :: cycle' xs
  where cycle' : Vect n a -> Stream a
        cycle' []        = x :: cycle' xs
        cycle' (y :: ys) = y :: cycle' ys

take' : (n : Nat) -> (xs : Stream a) -> Vect n a
take' Z _ = []
take' (S n) (x :: xs) = x :: (take' n xs)

export
shift : Nat -> Vect n a -> Vect n a
shift Z xs = xs
shift (S k) [] = []
shift {n = S m} (S k) (x :: xs) = take' (S m) $ drop (S k) $ cycle (x :: xs)

export
max' : Ord a => Vect (S n) a -> a
max' (x :: xs) = foldl max x xs

export
min' : Ord a => Vect (S n) a -> a
min' (x :: xs) = foldl min x xs

export
allPairs : Vect (S n) a -> Vect (S n) (Vect n (a, a))
allPairs {n} xs = g xs n where
  f : Vect (S n) a -> Vect n (a, a)
  f (x :: xs) = map (MkPair x) xs

  g : Vect (S n) a -> (m : Nat) -> Vect (S m) (Vect n (a, a))
  g xs Z = [f xs]
  g xs (S k) = (f $ shift (S k) xs) :: g xs k


text:
module Data.Time.LocalTime.Internal.TimeOfDay

import Data.Time.Clock.Internal.Fixed
import Data.Time.Clock.Internal.DiffTime

public export
record TimeOfDay where
  constructor MkTimeOfDay
  todHour: Integer
  todMin: Integer
  todSec: Pico

export
Show TimeOfDay where
  show (MkTimeOfDay h m s) = show h ++ ":" ++ show m ++ ":" ++ show s

posixDayLength: Integer
posixDayLength = 86400

export
nonLeapTimeOfDay : Integer -> TimeOfDay
nonLeapTimeOfDay picoSeconds =
  let
    s = mod picoSeconds 60
    s' = div picoSeconds 60
    h = div s' 60
    m' = mod s' 60
  in
    MkTimeOfDay h m' (MkFixed s)

export
timeToTimeOfDay: DiffTime -> TimeOfDay
timeToTimeOfDay x =
  let
    picoSeconds = (diffTimeToPicoseconds x)
  in
    if picoSeconds >= posixDayLength then (MkTimeOfDay 23 59 (MkFixed (60 + (picoSeconds - posixDayLength))))
    else nonLeapTimeOfDay picoSeconds

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Brainfeck.ST
import Control.ST
import Data.Fin
import Data.Fuel
import Data.Vect as V
import System

import Brainfeck.Lex
import Brainfeck.Parse
import Brainfeck.Type
import Brainfeck.VM as VM

%default total

export
interface CharIO (m : Type -> Type) where
  getChar : STrans m Char res (const res)
  putChar : Char -> STrans m () res (const res)
  info    : String -> STrans m () res (const res)

export
VMST : Nat -> Nat -> Nat -> Type
VMST l r i = State (VMState l r i)

readChar : CharIO io => (vm : Var) -> ST io () [vm ::: VMST l r i]
readChar vm = do c <- getChar
                 update vm (inputChar c)

outputChar : CharIO io => (vm : Var) -> ST io () [vm ::: VMST l r i]
outputChar vmVar = do
 vm <- read vmVar
 let cell = outputChar vm
 putChar cell

updateVM : (VMState l r i -> VMState l r i)
         -> (vm : Var)
         -> ST id () [vm ::: VMST l r i]
updateVM f vmVar = update vmVar f

increment : (vm : Var) -> ST id () [vm ::: VMST l r i]
increment = updateVM VM.increment

decrement : (vm : Var) -> ST id () [vm ::: VMST l r i]
decrement = updateVM VM.decrement

jumpBack : (vm : Var) -> ST id () [vm ::: VMST l r (S i)]
jumpBack = updateVM VM.jumpBack

jumpForward : (vm : Var) -> ST id () [vm ::: VMST l r (S i)]
jumpForward = updateVM VM.jumpForward

data StepResult : Type where
  StepInfo   : String -> (l : Nat) -> (r : Nat) -> (i : Nat) -> StepResult
  StepSuccess : (l : Nat) -> (r : Nat) -> (i : Nat) -> StepResult

ResultST : Type
ResultST = State StepResult

data AlwaysSucceeds : Type where
  STrivial : (l : Nat) -> (r : Nat) -> AlwaysSucceeds

AlwaysST : Type
AlwaysST = State StepResult

shiftLeft : CharIO io
          => (vm : Var)
          -> ST io StepResult [vm ::: VMST l r i :->
                                 (\res => case res of
                                            (StepInfo e l r i)   => VMST l r i
                                            (StepSuccess l' r' i) => VMST l' r' i)]
shiftLeft {l = Z} {r} {i} _ = do
  let msg = "Cell index is 0. Unable to leftshift."
  info msg
  pure $ StepInfo msg Z r i
shiftLeft {l = (S k)} {r} {i} vm = update vm (VM.shiftLeft) >>= \_ => pure (StepSuccess k (S r) i)

shiftRight : {l : Nat} -> {r : Nat} -> {auto p : IsSucc (l + r)}
           -> (vm : Var)
           -> ST id AlwaysSucceeds [ vm ::: VMST l r i :->
                                      (\res => case res of
                                                 (STrivial l' r') => VMST l' r' i) ]
shiftRight {l = (S k)} {r = Z} vmVar =
  update vmVar (VM.shiftRight . grow) >>= \_ => pure (STrivial (S (S k)) k)
  where
    growProof : (vm : VMState llen (0 + (rlen + 0)) i) -> VMState llen rlen i
    growProof {rlen} vm = rewrite plusCommutative 0 rlen in vm
    grow : VMState (S k) 0 i -> VMState (S k) (S k) i
    grow vm = growProof (growVM vm)
shiftRight {l} {r = (S k)} vm = update vm VM.shiftRight >>= \_ => pure (STrivial (S l) k)

stepSuccess : {l : Nat} -> {r : Nat} -> {i : Nat} -> StepResult
stepSuccess {l} {r} {i} = StepSuccess l r i

step : CharIO io => {auto p : IsSucc (l + r) }
     -> (vm : Var)
     -> ST io StepResult [ vm ::: VMST l r (S i) :->
                                (\res => case res of
                                           (StepInfo e l  r  i) => VMST l  r  i
                                           (StepSuccess l' r' i) => VMST l' r' i) ]
step {l} {r} {i} vmVar = do
  vm <- read vmVar
  case instruction vm of
    OLeft        => do vm' <- shiftLeft vmVar
                       case vm' of
                         (StepInfo e l  r  i) => pure $ StepInfo e l r i
                         (StepSuccess l' r' i) => pure $ StepSuccess l' r' i
    ORight       => shiftRight vmVar >>= \(STrivial l' r') => pure (StepSuccess l' r' (S i))
    OInc         => increment vmVar >>= \_ => pure stepSuccess
    ODec         => decrement vmVar >>= \_ => pure stepSuccess
    OOut         => outputChar vmVar >>= \_ => pure stepSuccess
    OIn          => readChar vmVar >>= \_ => pure stepSuccess
    OJumpZero _  => jumpForward vmVar >>= \_ => pure stepSuccess
    OJumpNZero _ => jumpBack vmVar >>= \_ => pure stepSuccess

runLoop : CharIO io => {auto p : IsSucc (l + r) }
                    -> Fuel -> (vm : Var)
                    -> ST io () [ remove vm (VMST l r (S i)) ]
runLoop Dry vmVar      = delete vmVar
runLoop (More f) vmVar = do
  res <- step vmVar
  case res of
    (StepInfo _ _ _ (S k)) => info "Aborting" >>= \_ => delete vmVar
    (StepInfo _ _ _  Z   ) => info "Ended up in an undefined state (missing all instructions)" >>= \_ => delete vmVar
    (StepSuccess _ _  Z   ) => do info "Ended up in an undefined state (missing all instructions) after successful step"
                                  delete vmVar
    (StepSuccess tapeL tapeR (S k)) => do
      case isItSucc (tapeL + tapeR) of
         No _    => info "Somehow the tape was deleted. Aborting." >>= \_ => delete vmVar
         Yes prf => do
           vm <- read vmVar
           let pc' = FS (pc vm)
           case strengthen pc' of
             (Left l) => delete vmVar -- end of program
             (Right r) => do
               update vmVar (record { pc = r })
               runLoop f vmVar

printTokens : CharIO io => Bool -> Tokens n -> ST io () []
printTokens False _ = pure ()
printTokens True xs = do
  info "Lexed Tokens: "
  let strs = foldr (++) "" . V.intersperse ", " $ map (tokenToS . snd) xs
  info strs
  info ""
  pure ()

printParse : CharIO io => Bool -> Instructions n -> ST io () []
printParse False _ = pure ()
printParse True xs = do
  info "Parsed Operations: "
  let strs = foldr (++) "" . V.intersperse ", " $ map operationToS xs
  info strs
  info ""
  pure ()

export
runProgram : CharIO io => (printLex : Bool) -> (printParse : Bool)
          -> Fuel -> (progText : String) -> ST io () []
runProgram plex pparse fuel progText =
  case lex progText of
    (Z ** _ ) => info "Nothing to do. Bye"
    (S n ** ts) => do
      printTokens plex ts
      case parse ts of
        Left (MkParseError loc s) =>
          info $ "Error at " ++ locToS loc ++ " " ++ s
        Right (Z ** _)     => info "Empty parse"
        Right (S n ** ops) => do
          printParse pparse ops
          let vm = initVM ops
          case isItSucc InitialVMSize of
            (No _)    => info "This was compiled with an invalid InitialVMSize! See ya."
            (Yes prf) => do v <- new vm
                            runLoop {p = prf} {l = 0} {r = InitialVMSize} fuel v

max_stars_repo_name: jhmcstanton/brainfeck

max_issues_repo_name: jhmcstanton/brainfeck

max_forks_repo_name: jhmcstanton/brainfeck


text:
module Part1

import Data.String

mode : (Nat, Nat) -> Char
mode (a, b) = if a > b then '0' else '1'

indexedCounter : Nat -> List (List Char) -> (Nat, Nat)
indexedCounter n llc = foldl foldOp (0, 0) llc where
    foldOp : (Nat, Nat) -> List Char -> (Nat, Nat)
    foldOp (x, y) l = if (index' n l) == Just '0' then (x + 1, y) else (x, y + 1)

countModes : List (List Char) -> List (Nat, Nat)
countModes llc = map doer (natRange 12) where
    doer : Nat -> (Nat, Nat)
    doer n = indexedCounter n llc

export
solve : List String -> List (Char)
solve a = map mode (countModes (map unpack a))


text:
mult_0_r : (n : Nat) -> n * 0 = 0
mult_0_r Z = Refl
mult_0_r (S k) =
    let indHypothesis = mult_0_r k in
        rewrite indHypothesis in Refl

plus_0_r : (n : Nat) -> n + 0 = n
plus_0_r Z = Refl
plus_0_r (S k) = rewrite plus_0_r k in Refl

plus_n_Sm : (n, m : Nat) -> S (n + m) = n + (S m)
plus_n_Sm Z m = Refl
plus_n_Sm (S k) j = rewrite plus_n_Sm k j in Refl

total
plus_comm : (n, m : Nat) -> n + m = m + n
plus_comm Z Z = Refl
plus_comm Z (S k) = rewrite plus_comm Z k in Refl
plus_comm (S k) m = rewrite plus_comm k m in rewrite plus_n_Sm m k in Refl

total
plus_assoc : (n, m, p : Nat) -> n + (m + p) = (n + m) + p
plus_assoc Z m p = Refl
plus_assoc (S k) m n = rewrite plus_assoc k m n in Refl

double : (n : Nat) -> Nat
double Z = Z
double (S k) = S (S (double k))

total
double_plus : (n : Nat) -> double n = n + n
double_plus Z = Refl
double_plus (S k) = rewrite double_plus k in rewrite plus_n_Sm k k in Refl

evenb : (n : Nat) -> Bool
evenb Z = True
evenb (S Z) = False
evenb (S (S k)) = evenb k

total
not_involutive : (b : Bool) -> not (not b) = b
not_involutive True = Refl
not_involutive False = Refl

total
evenb_S : (n : Nat) -> evenb (S n) = not (evenb n)
evenb_S Z = Refl
evenb_S (S k) = rewrite evenb_S k in rewrite not_involutive (evenb k) in Refl

total
plus_rearrange : (n, m, p, q : Nat) -> (n + m) + (p + q) = (m + n) + (p + q)
plus_rearrange n m p q = rewrite plus_comm n m in Refl

total
plus_swap : (n, m, p : Nat) -> n + (m + p) = m + (n + p)
plus_swap n m p =
    rewrite plus_assoc n m p in
        rewrite plus_comm n m in
            rewrite plus_assoc m n p in Refl

mult_n_Sk : (n, k : Nat) -> n * (S k) = n + (n * k)
mult_n_Sk Z k = Refl
mult_n_Sk (S j) k =
    rewrite mult_n_Sk j k in
        rewrite plus_swap k j (mult j k) in
            Refl

total
mult_comm : (m, n : Nat) -> m * n = n * m
mult_comm Z n = rewrite mult_0_r n in Refl
mult_comm (S k) n = rewrite mult_n_Sk n k in rewrite mult_comm k n in Refl

total
le_refl : (n : Nat) -> lte n n = True
le_refl Z = Refl
le_refl (S k) = rewrite le_refl k in Refl

zero_nbeq_S : (n : Nat) -> 0 == (S n) = False
zero_nbeq_S n = Refl

andb_false_r : (b : Bool) -> b && False = False
andb_false_r False = Refl
andb_false_r True = Refl

plus_ble_compat_l : (n, m, p : Nat) -> lte n m = True -> lte (p + n) (p + m) = True
plus_ble_compat_l n m Z prf = prf
plus_ble_compat_l n m (S k) prf = rewrite plus_ble_compat_l n m k prf in Refl

S_nbeq_0 : (n : Nat) -> (S n) == 0 = False
S_nbeq_0 n = Refl

mult_1_l : (n : Nat) -> 1 * n = n
mult_1_l n = rewrite plus_0_r n in Refl

all3_spec : (b, c : Bool) -> (b && c) || ((not b) || (not c)) = True
all3_spec False c = Refl
all3_spec True False = Refl
all3_spec True True = Refl

total
mult_plus_distr_r : (n, m, p : Nat) -> (n + m) * p = (n * p) + (m * p)
mult_plus_distr_r Z m p = Refl
mult_plus_distr_r (S k) m p =
    rewrite mult_plus_distr_r k m p in
        rewrite plus_assoc p (k * p) (m * p) in
            Refl

total
mult_assoc : (n, m, p : Nat) -> n * (m * p) = (n * m) * p
mult_assoc Z m p = Refl
mult_assoc (S k) m p =
    rewrite mult_assoc k m p in
        rewrite mult_plus_distr_r m (mult k m) p in
            Refl

total
beq_nat_refl : (n : Nat) -> True = n == n
beq_nat_refl Z = Refl
beq_nat_refl (S k) = rewrite beq_nat_refl k in Refl

total
plus_swap' : (n, m, p : Nat) -> n + (m + p) = m + (n + p)
plus_swap' n m p =
    rewrite plus_assoc n m p in
        rewrite plus_assoc m n p in
            rewrite plus_comm n m in
                Refl

data Bin : Type where
    Z : Bin
    Odd : Bin -> Bin
    Even : Bin -> Bin

incr : Bin -> Bin
incr Z = Odd Z
incr b@(Odd x) = Even b
incr b@(Even x) = Odd b

binToNat : Bin -> Nat
binToNat Z = Z
binToNat (Odd x) = 1 + binToNat x
binToNat (Even x) = 1 + binToNat x

bin_to_nat_pres_incr : (b : Bin) -> S (binToNat b) = binToNat $ incr b
bin_to_nat_pres_incr Z = Refl
bin_to_nat_pres_incr (Odd x) = Refl
bin_to_nat_pres_incr (Even x) = Refl

natToBin : Nat -> Bin
natToBin Z = Z
natToBin (S (S k)) = Even (natToBin k)
natToBin (S k) = Odd (natToBin k)

nat_conv_full_cycle : (n : Nat) -> binToNat $ natToBin n = n
nat_conv_full_cycle Z = Refl
nat_conv_full_cycle (S k) = ?nat_conv_full_cycle_rhs_2


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

||| This module details correctness properties for element insertion.
|||
||| Correctness/Soundness Properties ::
|||
||| 1. All elements added to the model must be unique.
|||
||| Note ::
|||
||| + This property should probably be replaced within the model using a Set.
|||
module GRL.Property.Element

import public Decidable.Equality

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

import GRL.Model
import GRL.IR
import GRL.Common

%access export
-- ------------------------------------------------------- [ Element Insertion ]

||| Check to see if the element is unique.
|||
isElemUnique : (node : GExpr ELEM) -> (model : GModel) -> Bool
isElemUnique (Elem ty t s) m = not $ hasGoal t m

||| Check to see if the element is unique.
|||
%hint
checkElemBool : (node : GExpr ELEM) -> (model : GModel) -> Bool
checkElemBool n m = isElemUnique n m

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl