text:
module Inigo.Async.Fetch

import Data.Buffer
import Extra.Buffer
import Inigo.Async.Base
import Inigo.Async.Promise
import Inigo.Async.Util

%foreign (promisifyPrim "(url)=>new Promise((resolve,reject)=>(url.startsWith('https')?require('https'):require('http')).get(url,(r)=>{let d='';r.on('data',(c)=>{d+=c;});r.on('end',()=>{resolve(d)});}).on('error',(e)=>{reject(e);}))")
fetch__prim : String -> promise String

%foreign (promisifyPrim "(url)=>new Promise((resolve,reject)=>(url.startsWith('https')?require('https'):require('http')).get(url,(r)=>{let cs=[];r.on('data',(c)=>{cs.push(Buffer.from(c))});r.on('end',()=>{resolve(Buffer.concat(cs))});}).on('error',(e)=>{reject(e);}))")
fetchBuf__prim : String -> promise Buffer

%foreign (promisifyPrim ("(url,method,data,headers)=>new Promise((resolve,reject)=>{"++ toObject ++";let u=new URL(url);let port=u.port!==''?u.port:u.protocol==='https:'?443:80;let opts={hostname:u.hostname,port,path:u.pathname,method,headers:toObject(headers)};let req=(u.protocol==='https:'?require('https'):require('http')).request(opts,(r)=>{let cs=[];r.on('data',(c)=>{cs.push(Buffer.from(c))});r.on('end',()=>{resolve(__prim_js2idris_array([Buffer.from(r.statusCode.toString(), 'utf-8'), Buffer.concat(cs)]))});}).on('error',(e)=>reject(e));req.on('error',(e)=>reject(e));req.write(data);req.end();})"))
request__prim : String -> String -> Buffer -> List (String, String) -> promise (List Buffer)

export
fetch : String -> Promise String
fetch url =
  promisify (fetch__prim url)

export
fetchBuf : String -> Promise Buffer
fetchBuf url =
  promisify (fetchBuf__prim url)

convertStatusCode : List Buffer -> Promise (Int, Buffer)
convertStatusCode lb =
  case lb of
    statusBuf :: buf :: [] =>
      do
        status <- liftIO $ readAll statusBuf
        pure (cast status, buf)
    _ =>
      reject "Invalid response"

export
requestBuf : String -> String -> Buffer -> List (String, String) -> Promise (Int, Buffer)
requestBuf url method body headers =
  do
    res <- promisify (request__prim url method body headers)
    convertStatusCode res

export
request : String -> String -> String -> List (String, String) -> Promise (Int, Buffer)
request url method body headers =
  do
    buf <- liftIO $ fromString body
    res <- promisify (request__prim url method buf headers)
    convertStatusCode res

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
-- this works
aNat : {default Z theNat : Nat} -> Nat
aNat = theNat

-- this does too, now (but did not work before)
record ANat where
  constructor MkANat
  {default Z theNat : Nat}

-- let's try out
ex : ANat
ex = MkANat

ext: idr


text:
module SkepticLang.ListUtils

%access public export

||| Looks up a value by key in a list of key-value pairs.
|||
||| @pairs  the list of key-value pairs
||| @key    the key to look up
lookup : Eq a => (pairs : List (a, b)) -> (key : a) -> Maybe b
lookup [] _ = Nothing
lookup ((a, b) :: pairs') key = if a == key then Just b else lookup pairs' key

||| Removes an entry from a list of key-value pairs, if an entry with that key exists.
|||
||| @pairs  the list of key-value pairs
||| @key    the key of the item to remove
remove : Eq a => (pairs : List (a, b)) -> (key : a) -> List (a, b)
remove [] _ = []
remove ((a, b) :: pairs') key = if a == key then remove pairs' key else (a, b) :: remove pairs' key

max_stars_repo_name: sr-lab/skeptic-lang

max_issues_repo_name: sr-lab/skeptic-lang

max_forks_repo_name: sr-lab/skeptic-lang


text:
module Data.HList

%default total

public export
data HList : List Type -> Type where
  Nil : HList []
  (::) : (a : x) -> HList xs -> HList (x :: xs)


text:
module Package.IkanAst
import Package.IpkgAst
%access public export

data IkanData : Type -> Type where
  AddDependencies : List String -> IkanData Unit
  AddSourcepaths : List String -> IkanData Unit

max_stars_repo_name: renpillay/ikan

max_issues_repo_name: renpillay/ikan

max_forks_repo_name: renpillay/ikan


text:
module Main

%language UniquenessTypes

data UList : Type -> UniqueType where
     Nil   : UList a
     (::)  : a -> UList a -> UList a

umap : (a -> b) -> UList a -> UList b
umap f [] = []
umap f (x :: xs) = f x :: umap f xs

free : {a : UniqueType} -> a -> String
free xs = ""

showU : Show a => Borrowed (UList a) -> String
showU [] = "END"
showU (x :: xs) = show x ++ "," ++ showU xs

mkUList : Nat -> UList Int
mkUList Z = []
mkUList (S k) = cast k :: mkUList k

showStuff : UList Int -> IO ()
showStuff xs = do
          putStrLn (showU xs)
          putStrLn (showU xs)
          let xs' = umap (*2) xs
          putStrLn (showU xs')
          putStrLn (showU xs')

main : IO ()
main = showStuff (mkUList 20)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Main

import Collie

import Interface
import Data.Version
import System.Directory.Extra
import Command

%hide Collie.(.handleWith)

exitError : HasIO io => String -> io a
exitError err = do
  putStrLn ""
  putStrLn err
  putStrLn ""
  exitFailure

exitSuccess : HasIO io => String -> io a
exitSuccess msg = do
  putStrLn ""
  putStrLn msg
  putStrLn ""
  exitSuccess

--
-- Entrypoint
--

-- Handling more complex commands (with arguemnts and modifiers) first
-- makes compile times shorter.
handleCommand' : Command.idv ~~> IO ()
handleCommand' =
  [ const $ do putStrLn "Expected a subcommand."
               exitError idv.usage
  , "install"   ::= [ (\args => let version = args.arguments
                                    -- Installing the LSP requires installing the API
                                    -- just as installing the API requires installing
                                    -- Idris.
                                in  if args.modifiers.project "--lsp"
                                       then installLSPCommand version
                                       else if args.modifiers.project "--api"
                                            then installAPICommand version
                                            else installCommand version True
                      )
                    ]
  , "uninstall" ::= [ (\args => let version = args.arguments
                                in  uninstallCommand version
                      )
                    ]
  , "select"    ::= [ (\args => let version = args.arguments
                                in  selectCommand version )
                    , "system" ::= [ const selectSystemCommand ]
                    ]
  , "--help"    ::= [ const . exitSuccess $ idv.usage ]
  , "list"      ::= [ const listVersionsCommand ]
  ]

main : IO ()
main = do
  Just _ <- inDir idvLocation $ idv.handleWith handleCommand'
    | Nothing => exitError "Could not access \{idvLocation}."
  pure ()

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
module FFI.GitHub

import Data.Promise
import Data.PullRequest
import Data.Review
import Data.String
import Data.String.Extra
import Data.User
import Data.Vect
import FFI
import Language.JSON
import Language.JSON.Accessors

import public Data.Fin

%default total

okit_ffi : (fnName : String) -> String
okit_ffi = node_ffi "okit"

data OctokitRef : Type

export
data Octokit = Kit (Ptr OctokitRef)

%foreign okit_ffi "octokit"
prim__octokit : (authToken : String) -> PrimIO (Ptr OctokitRef)

export
octokit : (authToken : String) -> IO Octokit
octokit authToken = Kit <$> (primIO $ prim__octokit authToken)

%foreign okit_ffi "get_repo_default_branch"
prim__getRepoDefaultBranch : Ptr OctokitRef
                          -> (org : String)
                          -> (repo : String)
                          -> (onSuccess : String -> PrimIO ())
                          -> (onFailure : String -> PrimIO ())
                          -> PrimIO ()

export
getRepoDefaultBranch : Octokit =>
                       (org : String)
                    -> (repo : String)
                    -> Promise String
getRepoDefaultBranch @{(Kit ptr)} org repo = promiseIO $ prim__getRepoDefaultBranch ptr org repo

%foreign okit_ffi "list_teams"
prim__listTeams : Ptr OctokitRef
               -> (org : String)
               -> (onSuccess : String -> PrimIO ())
               -> (onFailure : String -> PrimIO ())
               -> PrimIO ()

export
listTeams : Octokit => (org : String) -> Promise (List String)
listTeams @{(Kit ptr)} org =
  lines <$> (promiseIO $ prim__listTeams ptr org)

%foreign okit_ffi "list_prs"
prim__listPRsForBranch : Ptr OctokitRef
                      -> (owner : String)
                      -> (repo : String)
                      -> (branch : String)
                      -> (onSuccess : String -> PrimIO ())
                      -> (onFailure : String -> PrimIO ())
                      -> PrimIO ()

export
listPRsForBranch : Octokit =>
                   (owner : String)
                -> (repo : String)
                -> (branch : String)
                -> Promise (List PullRequest)
listPRsForBranch @{(Kit ptr)} owner repo branch =
  either . parsePullRequestsString =<< (promiseIO $ prim__listPRsForBranch ptr owner repo branch)

%foreign okit_ffi "create_pr"
prim__createPR : Ptr OctokitRef
              -> (owner : String)
              -> (repo : String)
              -> (head : String)
              -> (base : String)
              -> (title : String)
              -> (body : String)
              -> (onSuccess : String -> PrimIO ())
              -> (onFailure : String -> PrimIO ())
              -> PrimIO ()

export
createPR : Octokit =>
           (owner : String)
        -> (repo : String)
        -> (head : String)
        -> (base : String)
        -> (title : String)
        -> (description : String)
        -> Promise PullRequest
createPR @{(Kit ptr)} owner repo head base title description =
  either . parsePullRequestString =<< (promiseIO $ prim__createPR ptr owner repo head base title description)

%foreign okit_ffi "create_comment"
prim__createComment : Ptr OctokitRef
                   -> (owner : String)
                   -> (repo : String)
                   -> (issueOrPrNumber : Integer)
                   -> (message : String)
                   -> (onSuccess : String -> PrimIO ())
                   -> (onFailure : String -> PrimIO ())
                   -> PrimIO ()

export
createComment : Octokit =>
                (owner : String)
             -> (repo : String)
             -> (issueOrPrNumber : Integer)
             -> (message : String)
             -> Promise ()
createComment @{(Kit ptr)} owner repo issueOrPrNumber message =
  ignore . promiseIO $ prim__createComment ptr owner repo issueOrPrNumber message

pullRequestStateFilter : Maybe PRState -> String
pullRequestStateFilter Nothing = "all"
pullRequestStateFilter (Just s) = show s

%foreign okit_ffi "list_reviewers"
prim__listPullReviewers : Ptr OctokitRef
                       -> (owner : String)
                       -> (repo : String)
                       -> (stateFilter : String)
                       -> (pageLimit : Int16)
                       -> (onSuccess : String -> PrimIO ())
                       -> (onFailure : String -> PrimIO ())
                       -> PrimIO ()

||| List 1 page of pull reviewers (a list of usernames, one per user per review).
export
listPullReviewers : Octokit =>
                    (owner : String)
                 -> (repo : String)
                 -> (stateFilter : Maybe PRState)
                 -> (pageLimit : Fin 101)
                 -> Promise (List String)
listPullReviewers @{(Kit ptr)} owner repo stateFilter pageLimit =
  lines <$> (promiseIO $ prim__listPullReviewers ptr owner repo (pullRequestStateFilter stateFilter) (cast $ finToNat pageLimit))

%foreign okit_ffi "list_pull_requests"
prim__listPullRequests : Ptr OctokitRef
                      -> (owner : String)
                      -> (repo : String)
                      -> (stateFilter : String)
                      -> (pageLimit : Int16)
                      -> (page : Int16)
                      -> (onSuccess : String -> PrimIO ())
                      -> (onFailure : String -> PrimIO ())
                      -> PrimIO ()

export
listPullRequestsJsonStr : Octokit =>
                          (owner : String)
                       -> (repo : String)
                       -> (stateFilter : Maybe PRState)
                       -> (pageLimit : Fin 101)
                       -> {default 0 page : Nat}
                       -> Promise String
listPullRequestsJsonStr @{(Kit ptr)} owner repo stateFilter pageLimit {page} =
  let filter  = pullRequestStateFilter stateFilter
      pgLimit = cast $ finToNat pageLimit
      pg      = cast (S page)
  in  promiseIO $ prim__listPullRequests ptr owner repo filter pgLimit pg

||| List the most recent pull requests by creation date.
|||
||| @owner       The repository owner (a.k.a. org name).
||| @repo        The repository name.
||| @stateFilter Retrieve only open or only closed PRs. Pass Nothing to retrieve all PRs.
||| @pageLimit   The number of results per page (max 100).
||| @page        The zero-indexed page index to retieve. Defaults to 0.
export
listPullRequests : Octokit =>
                   (owner : String)
                -> (repo : String)
                -> (stateFilter : Maybe PRState)
                -> (pageLimit : Fin 101)
                -> {default 0 page : Nat}
                -> Promise (List PullRequest)
listPullRequests @{(Kit ptr)} owner repo stateFilter pageLimit {page} =
  either . parsePullRequestsString =<< listPullRequestsJsonStr owner repo stateFilter pageLimit {page}

-- reviewers and teamReviewers should be comma separated values encoded in a string.
%foreign okit_ffi "add_reviewers"
prim__addPullReviewers : Ptr OctokitRef
                      -> (owner : String)
                      -> (repo : String)
                      -> (pullNumber : Integer)
                      -> (reviewers : String)
                      -> (teamReviewers : String)
                      -> (onSuccess : String -> PrimIO ())
                      -> (onFailure : String -> PrimIO ())
                      -> PrimIO ()

||| Add reviewers to a Pull Request.
|||
||| onSuccess will receive a newline delimited list of
||| all reviewers of the modified PR.
export
addPullReviewers : Octokit =>
                   (owner : String)
                -> (repo : String)
                -> (pullNumber : Integer)
                -> (reviewers : List String)
                -> (teamReviewers : List String)
                -> Promise (List String)
addPullReviewers @{(Kit ptr)} owner repo pullNumber reviewers teamReviewers =
  lines <$> (promiseIO $ prim__addPullReviewers ptr owner repo pullNumber (join "," reviewers) (join "," teamReviewers))

%foreign okit_ffi "list_pr_reviews"
prim__listPullReviews : Ptr OctokitRef
                     -> (owner : String)
                     -> (repo : String)
                     -> (pullNumber : Integer)
                     -> (onSuccess : String -> PrimIO ())
                     -> (onFailure : String -> PrimIO ())
                     -> PrimIO ()

export
listPullReviewsJsonStr : Octokit =>
                         (owner : String)
                      -> (repo : String)
                      -> (pullNumber : Integer)
                      -> Promise String
listPullReviewsJsonStr @{(Kit ptr)} owner repo pullNumber =
  promiseIO $ prim__listPullReviews ptr owner repo pullNumber

export
listPullReviews : Octokit =>
                  (owner : String)
               -> (repo : String)
               -> (pullNumber : Integer)
               -> Promise (List Review)
listPullReviews owner repo pullNumber =
  either . parseReviewsString =<< listPullReviewsJsonStr owner repo pullNumber

%foreign okit_ffi "list_team_members"
prim__listTeamMembers : Ptr OctokitRef
                     -> (org : String)
                     -> (teamSlug : String)
                     -> (onSuccess : String -> PrimIO ())
                     -> (onFailure : String -> PrimIO ())
                     -> PrimIO ()

export
listTeamMembers : Octokit =>
                  (org : String)
               -> (teamSlug : String)
               -> Promise (List String)
listTeamMembers @{(Kit ptr)} org teamSlug =
  lines <$> (promiseIO $ prim__listTeamMembers ptr org teamSlug)

%foreign okit_ffi "list_org_members"
prim__listOrgMembers : Ptr OctokitRef
                    -> (org : String)
                    -> (onSuccess : String -> PrimIO ())
                    -> (onFailure : String -> PrimIO ())
                    -> PrimIO ()

export
listOrgMembers : Octokit => (org : String) -> Promise (List String)
listOrgMembers @{(Kit ptr)} org =
  lines <$> (promiseIO $ prim__listOrgMembers ptr org)

%foreign okit_ffi "get_user"
prim__getUser : Ptr OctokitRef
             -> (username : String)
             -> (onSuccess : String -> PrimIO ())
             -> (onFailure : String -> PrimIO ())
             -> PrimIO ()

export
getUser : Octokit => (username : String) -> Promise User
getUser @{(Kit ptr)} = either . parseUserString <=< promiseIO . prim__getUser ptr

%foreign okit_ffi "get_self"
prim__getSelf : Ptr OctokitRef
             -> (onSuccess : String -> PrimIO ())
             -> (onFailure : String -> PrimIO ())
             -> PrimIO ()

export
getSelf : Octokit => Promise User
getSelf @{(Kit ptr)} = either . parseUserString =<< promiseIO (prim__getSelf ptr)

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
module IndProp

import Logic

%access public export

%default total

data Reflect : (p : Type) -> Bool -> Type where
  ReflectT : p -> (b=True) -> Reflect p b
  ReflectF : (Not p) -> (b=False) -> Reflect p b

iff_reflect : (p ↔ (b=True)) -> Reflect p b
iff_reflect {b = False} (pb, _) = ReflectF (uninhabited . pb) Refl
iff_reflect {b = True} (_, bp) = ReflectT (bp Refl) Refl

reflect_iff : Reflect p b -> (p ↔ (b=True))
reflect_iff (ReflectT p b_true) = (\_ => b_true, \_ => p)
reflect_iff (ReflectF not_p b_false) =
  ( \p => void (not_p p)
  , \b_true => void . uninhabited $
      the (False = True) $ rewrite sym b_false in b_true)


text:
module Rnd

import Effects

%access public export

data Random : Effect where
     GetRandom : Random Int Int (\v => Int)

Handler Random m where
     handle seed GetRandom k
              = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremInt` (pow 2 32)) in
                    k seed' seed'

RND : EFFECT
RND = MkEff Int Random

rndInt : Int -> Int -> { [RND] } Eff Int
rndInt lower upper = do v <- call GetRandom
                        pure (abs (v `prim__sremInt` (upper - lower)) + lower)

max_stars_repo_name: idris-hackers/idris-demos

max_issues_repo_name: idris-hackers/idris-demos

max_forks_repo_name: idris-hackers/idris-demos


text:
module Main

import Average
import Palindrome

counts : String -> (Nat, Nat)
counts s = (length (words s), length s)

top_ten : Ord a => List a -> List a
top_ten xs = take 10 (reverse (sort xs))

over_length : Nat -> List String -> Nat
over_length n strs = length (filter (\w => length w > n) strs)

describe : String -> String
describe str = "The average word length is: "
  ++ show (average str) ++ ".\n"
  ++ "It " ++ (if palindrome 10 str then "is" else "is not") ++ " a palindrome.\n"

main : IO ()
main = repl "Enter a string:"
            describe

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Text.Readline

rlib : String -> String
rlib fn = "C:" ++ fn ++ ",libidrisreadline"

%foreign (rlib "getString")
export
getString : Ptr String -> String

%foreign (rlib "mkString")
export
mkString : String -> Ptr String

%foreign (rlib "nullString")
export
nullString : Ptr String

%foreign (rlib "isNullString")
prim__isNullString : Ptr String -> Int

export
isNullString : Ptr String -> Bool
isNullString str = not $ prim__isNullString str == 0

%foreign (rlib "readline")
prim__readline : String -> PrimIO (Ptr String)

export
readline : HasIO io => String -> io (Maybe String)
readline s
    = do mstr <- primIO $ prim__readline s
         pure $ if isNullString mstr
                   then Nothing
                   else Just (getString mstr)

%foreign (rlib "add_history")
prim__add_history : String -> PrimIO ()

export
addHistory : HasIO io => String -> io ()
addHistory s = primIO $ prim__add_history s

%foreign (rlib "idrisrl_setCompletion")
prim__setCompletion : (String -> Int -> PrimIO (Ptr String)) -> PrimIO ()

export
setCompletionFn : HasIO io => (String -> Int -> IO (Maybe String)) -> io ()
setCompletionFn fn
    = primIO $ prim__setCompletion $ \s, i => toPrim $
          do mstr <- fn s i
             case mstr of
                  Nothing => pure nullString
                  Just str => pure (mkString str)


text:
VendState : Type
VendState = (Nat, Nat)

data Input = COIN
           | VEND
           | CHANGE
           | REFILL Nat

strToInput : String -> Maybe Input
strToInput "insert" = Just COIN
strToInput "vend" = Just VEND
strToInput "change" = Just CHANGE
strToInput x = if all isDigit (unpack x)
                  then Just (REFILL (cast x))
                  else Nothing

data CoinResult = Inserted | Rejected

data MachineCmd : (res : Type) -> VendState -> (res -> VendState) -> Type where
     InsertCoin : MachineCmd CoinResult (pounds, chocs)
                               (\res => case res of
                                             Inserted => (S pounds, chocs)
                                             Rejected => (pounds, chocs))
     Vend       : MachineCmd () (S pounds, S chocs) (const (pounds, chocs))
     GetCoins   : MachineCmd () (pounds, chocs)     (const (Z, chocs))

     Display : String ->
                  MachineCmd () state               (const state)
     Refill : (bars : Nat) ->
                  MachineCmd () (Z, chocs)          (const (Z, bars + chocs))

     GetInput : MachineCmd (Maybe Input) state (const state)

     Pure : (res : ty) -> MachineCmd ty (state_fn res) state_fn
     (>>=) : MachineCmd a state1 state2_fn ->
             ((x : a) -> MachineCmd b (state2_fn x) state3_fn) ->
             MachineCmd b state1 state3_fn

data MachineIO : VendState -> Type where
     Do : MachineCmd a state1 state2_fn ->
          ((x : a) -> Inf (MachineIO (state2_fn x))) -> MachineIO state1

namespace MachineDo
     (>>=) : MachineCmd a state1 state2_fn ->
             ((x : a) -> Inf (MachineIO (state2_fn x))) -> MachineIO state1
     (>>=) = Do

mutual
  vend : MachineIO (pounds, chocs)
  vend {pounds = S p} {chocs = S c} = do Vend
                                         Display "Enjoy!"
                                         machineLoop
  vend {pounds = Z} = do Display "Insert a coin"
                         machineLoop
  vend {chocs = Z} = do Display "Out of stock"
                        machineLoop

  refill : (num : Nat) -> MachineIO (pounds, chocs)
  refill {pounds = Z} num = do Refill num
                               machineLoop
  refill _ = do Display "Can't refill: Coins in machine"
                machineLoop

  machineLoop : MachineIO (pounds, chocs)
  machineLoop =
       do Just x <- GetInput | Nothig => do Display "Invalid input"
                                            machineLoop
          case x of
              COIN => do res <- InsertCoin
                         case res of
                              Inserted => do Display "Coin inserted"
                                             machineLoop
                              Rejected => do Display "Coin rejected"
                                             machineLoop
              VEND => vend
              CHANGE => do GetCoins
                           Display "Change returned"
                           machineLoop
              REFILL num => refill num

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Node.Sync.FileSystem

import Node.Free.FileSystem

%lib Node "fs"
%access public export

writeFileSync : String -> String -> JS_IO ()
writeFileSync path contents =
  foreign FFI_JS "fs.writeFileSync(%0, %1)" (String -> String -> JS_IO ()) path contents

readFileSync : String -> JS_IO String
readFileSync path = foreign FFI_JS "fs.readFileSync(%0, 'utf8')" (String -> JS_IO String) path

interpret : FileSystemF a -> JS_IO a
interpret (WriteFile filePath contents next) = writeFileSync filePath contents *> pure next
interpret (ReadFile filePath nextFn) = do
  contents <- readFileSync filePath
  pure (nextFn contents)

max_stars_repo_name: Risto-Stevcev/idris-node-fs

max_issues_repo_name: Risto-Stevcev/idris-node-fs

max_forks_repo_name: Risto-Stevcev/idris-node-fs


text:
f1 : Nat
f1 = g1 where
  g1 : Nat
  g1 = 5

f2 : Nat
f2 = g2 where
  namespace X
    export
    g2 : Nat
    g2 = 5

--f3 : Integer -> Nat
--f3 x = g3 where
--  namespace Y
--    export
--    g3 : Nat
--    g3 = 4

f4 : Integer -> Nat
f4 x = g4 x where
  namespace Z
    export
    g4 : Nat
    g4 _ = 4

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Solutions.Dependent

%default total

--------------------------------------------------------------------------------
--          Length-Indexed Lists
--------------------------------------------------------------------------------

data Vect : (len : Nat) -> Type -> Type where
  Nil  : Vect 0 a
  (::) : a -> Vect n a -> Vect (S n) a

-- 1
head : Vect (S n) a -> a
head (x :: _) = x
head Nil impossible

-- 2
tail : Vect (S n) a -> Vect n a
tail (_ :: xs) = xs
tail Nil impossible

-- 3
zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d
zipWith3 f []        []        []        = []
zipWith3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: zipWith3 f xs ys zs

-- 4
-- Since we only have a `Semigroup` constraint, we can't conjure
-- a value of type `a` out of nothing in case of an empty list.
-- We therefore have to return a `Nothing` in case of an empty list.
foldSemi : Semigroup a => List a -> Maybe a
foldSemi []        = Nothing
foldSemi (x :: xs) = Just . maybe x (x <+>) $ foldSemi xs

-- 5
-- the `Nil` case is impossible here, so unlike in Exercise 4,
-- we don't need to wrap the result in a `Maybe`.
-- However, we need to pattern match on the tail of the Vect to
-- decide whether to invoke `foldSemiVect` recursively ore not
foldSemiVect : Semigroup a => Vect (S n) a -> a
foldSemiVect (x :: [])         = x
foldSemiVect (x :: t@(_ :: _)) = x <+> foldSemiVect t

-- 6
iterate : (n : Nat) -> (a -> a) -> a -> Vect n a
iterate 0     _ _ = Nil
iterate (S k) f v = v :: iterate k f (f v)

-- 7
generate : (n : Nat) -> (s -> (s,a)) -> s -> Vect n a
generate 0     _ _ = Nil
generate (S k) f v =
  let (v', va) = f v
   in va :: generate k f v'

-- 8
fromList : (as : List a) -> Vect (length as) a
fromList []        = []
fromList (x :: xs) = x :: fromList xs

-- 9
-- Lookup the type and implementation of functions `maybe` `const` and
-- try figuring out, what's going on here. An alternative implementation
-- would of course just pattern match on the argument.
maybeSize : Maybe a -> Nat
maybeSize = maybe 0 (const 1)

fromMaybe : (m : Maybe a) -> Vect (maybeSize m) a
fromMaybe Nothing  = []
fromMaybe (Just x) = [x]

--------------------------------------------------------------------------------
--          Fin: Safe Indexing into Vectors
--------------------------------------------------------------------------------

data Fin : (n : Nat) -> Type where
  FZ : {0 n : Nat} -> Fin (S n)
  FS : (k : Fin n) -> Fin (S n)

(++) : Vect m a -> Vect n a -> Vect (m + n) a
(++) []        ys = ys
(++) (x :: xs) ys = x :: (xs ++ ys)

replicate : (n : Nat) -> a -> Vect n a
replicate 0     _ = []
replicate (S k) x = x :: replicate k x

zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith _ []        []        = []
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys

-- 1
update : (a -> a) -> Fin n -> Vect n a -> Vect n a
update f FZ     (x :: xs) = f x :: xs
update f (FS k) (x :: xs) = x :: update f k xs

-- 2
insert : a -> Fin (S n) -> Vect n a -> Vect (S n) a
insert v FZ     xs         = v :: xs
insert v (FS k) (x :: xs)  = x :: insert v k xs
insert v (FS k) []  impossible

-- 3
-- The trick here is to pattern match on the tail of the
-- vector in the `FS k` case and realize that an empty
-- tail is impossible. Otherwise we won't be able to
-- convince the type checker, that the vector's tail is
-- non-empty in the recursive case.
delete : Fin (S n) -> Vect (S n) a -> Vect n a
delete FZ     (_ :: xs)          = xs
delete (FS k) (x :: xs@(_ :: _)) = x :: delete k xs
delete (FS k) (x :: []) impossible

-- 4
safeIndexList : (xs : List a) -> Fin (length xs) -> a
safeIndexList (x :: _)  FZ     = x
safeIndexList (x :: xs) (FS k) = safeIndexList xs k
safeIndexList Nil _ impossible

-- 5
finToNat : Fin n -> Nat
finToNat FZ     = Z
finToNat (FS k) = S $ finToNat k

take : (k : Fin (S n)) -> Vect n a -> Vect (finToNat k) a
take FZ     x         = []
take (FS k) (x :: xs) = x :: take k xs

-- 6
minus : (n : Nat) -> Fin (S n) -> Nat
minus n FZ         = n
minus (S j) (FS k) = minus j k
minus 0 (FS k) impossible

-- 7
drop : (k : Fin (S n)) -> Vect n a -> Vect (minus n k) a
drop FZ     xs        = xs
drop (FS k) (_ :: xs) = drop k xs

-- 8
splitAt :  (k : Fin (S n))
        -> Vect n a
        -> (Vect (finToNat k) a, Vect (minus n k) a)
splitAt k xs = (take k xs, drop k xs)

--------------------------------------------------------------------------------
--          Compile-Time Computations
--------------------------------------------------------------------------------

-- 1
flattenList : List (List a) -> List a
flattenList []          = []
flattenList (xs :: xss) = xs ++ flattenList xss

flattenVect : Vect m (Vect n a) -> Vect (m * n) a
flattenVect []          = []
flattenVect (xs :: xss) = xs ++ flattenVect xss

-- 2
take' : (m : Nat) -> Vect (m + n) a -> Vect m a
take' 0     _         = []
take' (S k) (x :: xs) = x :: take' k xs
take' (S k) Nil impossible

drop' : (m : Nat) -> Vect (m + n) a -> Vect n a
drop' 0     xs        = xs
drop' (S k) (x :: xs) = drop' k xs
drop' (S k) Nil impossible

splitAt' : (m : Nat) -> Vect (m + n) a -> (Vect m a, Vect n a)
splitAt' m xs = (take' m xs, drop' m xs)

-- 3
-- Since we must call `replicate` in the `Nil` case, `k`
-- must be a non-erased argument. I used an implicit argument here,
-- since this reflects the type of the mathematical function
-- more closely.
--
-- Empty matrices probably don't make too much sense,
-- so we could also request at the type-level that `k` and `m`
-- are non-zero, in which case both values could be derived
-- by pattern matching on the vectors.
transpose : {k : _} -> Vect m (Vect k a) -> Vect k (Vect m a)
transpose []          = replicate k []
transpose (xs :: xss) = zipWith (::) xs (transpose xss)


text:
module Java.Util

import IdrisJvm.IO
import Java.Lang
import Java.Util.Stream

%access public export

namespace Collection
  collectionClass : String
  collectionClass = "java/util/Collection"

  CollectionInterface : JVM_NativeTy
  CollectionInterface = Interface collectionClass

  Collection : Type
  Collection = JVM_Native CollectionInterface

  stream : Inherits Collection collection => collection -> JVM_IO JStream
  stream collection = invokeInstance "stream" (Collection -> JVM_IO JStream) (believe_me collection)

namespace Arrays

  ArraysClass : JVM_NativeTy
  ArraysClass = Class "java/util/Arrays"

  Arrays : Type
  Arrays = JVM_Native ArraysClass

  toString : Inherits ObjectArray that => that -> JVM_IO String
  toString arr = invokeStatic ArraysClass "toString" (ObjectArray -> JVM_IO String) (believe_me arr)

  toStringBooleanArray : JVM_Array Bool -> JVM_IO String
  toStringBooleanArray arr = invokeStatic ArraysClass "toString" (JVM_Array Bool -> JVM_IO String) arr

  toStringByteArray : JVM_Array Bits8 -> JVM_IO String
  toStringByteArray arr = invokeStatic ArraysClass "toString" (JVM_Array Bits8 -> JVM_IO String) arr

  toStringCharArray : JVM_Array Char -> JVM_IO String
  toStringCharArray arr = invokeStatic ArraysClass "toString" (JVM_Array Char -> JVM_IO String) arr

  toStringShortArray : JVM_Array Bits16 -> JVM_IO String
  toStringShortArray arr = invokeStatic ArraysClass "toString" (JVM_Array Bits16 -> JVM_IO String) arr

  toStringIntArray : JVM_Array Int -> JVM_IO String
  toStringIntArray arr = invokeStatic ArraysClass "toString" (JVM_Array Int -> JVM_IO String) arr

  toStringLongArray : JVM_Array Bits64 -> JVM_IO String
  toStringLongArray arr = invokeStatic ArraysClass "toString" (JVM_Array Bits64 -> JVM_IO String) arr

  toStringFloatArray : JVM_Array JFloat -> JVM_IO String
  toStringFloatArray arr = invokeStatic ArraysClass "toString" (JVM_Array JFloat -> JVM_IO String) arr

  toStringDoubleArray : JVM_Array Double -> JVM_IO String
  toStringDoubleArray arr = invokeStatic ArraysClass "toString" (JVM_Array Double -> JVM_IO String) arr

  deepToString : Inherits ObjectArray that => that -> JVM_IO String
  deepToString arr = invokeStatic ArraysClass "deepToString" (ObjectArray -> JVM_IO String) (believe_me arr)

namespace Iterator

  Iterator : Type
  Iterator = javaInterface "java/util/Iterator"

  hasNext : Inherits Iterator that => that -> JVM_IO Bool
  hasNext itr = invokeInstance "hasNext" (Iterator -> JVM_IO Bool) (believe_me itr)

  next : Inherits Iterator that => that -> JVM_IO Object
  next itr = invokeInstance "next" (Iterator -> JVM_IO Object) (believe_me itr)

  toList : Inherits Iterator itr => itr -> JVM_IO (List a)
  toList itr = do
    hasNext' <- hasNext itr
    if hasNext'
      then do
        item <- next itr
        rest <- toList itr
        pure (believe_me item :: rest)
      else pure []

namespace JList
  listClass: String
  listClass = "java/util/List"

  ListInterface : JVM_NativeTy
  ListInterface = Interface listClass

  JList : Type
  JList = JVM_Native ListInterface

  Inherits Collection JList where {}

  add : Inherits JList list => list -> a -> JVM_IO Bool
  add list item = invokeInstance "add" (JList -> Object -> JVM_IO Bool) (believe_me list) (believe_me item)

  size : Inherits JList list => list -> JVM_IO Nat
  size list = cast <$> invokeInstance "size" (JList -> JVM_IO Int) (believe_me list)

  iterator : Inherits JList list => list -> JVM_IO Iterator
  iterator list = invokeInstance "iterator" (JList -> JVM_IO Iterator) (believe_me list)

namespace ArrayList
  arrayListClass: String
  arrayListClass = "java/util/ArrayList"

  ArrayListClass : JVM_NativeTy
  ArrayListClass = Class arrayListClass

  ArrayList : Type
  ArrayList = JVM_Native ArrayListClass

  Inherits Collection ArrayList where {}
  Inherits JList ArrayList where {}

  new : JVM_IO ArrayList
  new = FFI.new (JVM_IO ArrayList)

  fromList : List a -> JVM_IO ArrayList
  fromList xs = do
      arrayList <- ArrayList.new
      fromList' arrayList xs
    where
      fromList' : ArrayList -> List a -> JVM_IO ArrayList
      fromList' arrayList [] = pure arrayList
      fromList' arrayList (x :: xs) = do
        JList.add arrayList x
        fromList' arrayList xs

namespace HashMap
  HashMap : Type
  HashMap = JVM_Native $ Class "java/util/HashMap"

  new : JVM_IO HashMap
  new = FFI.new (JVM_IO HashMap)

  get : Inherits Object key => HashMap -> key -> JVM_IO (Maybe Object)
  get this key = nullableToMaybe <$> invokeInstance "get" (HashMap -> Object -> JVM_IO Object) this (believe_me key)

  put : (Inherits Object key, Inherits Object value) => HashMap -> Maybe key -> Maybe value -> JVM_IO (Maybe Object)
  put this key value = nullableToMaybe <$> invokeInstance "put" (HashMap -> Object -> Object -> JVM_IO Object) this (maybeToNullable $ believe_me key) (maybeToNullable $ believe_me value)

namespace Objects

  ObjectsClass : JVM_NativeTy
  ObjectsClass = Class "java/util/Objects"

  toString : Inherits Object that => that -> JVM_IO String
  toString obj = invokeStatic ObjectsClass "toString" (Object -> JVM_IO String) (believe_me obj)

  isNull : Inherits Object that => that -> JVM_IO Bool
  isNull obj = invokeStatic ObjectsClass "isNull" (Object -> JVM_IO Bool) (believe_me obj)

namespace Scanner
    scannerClass : JVM_NativeTy
    scannerClass = Class "java/util/Scanner"

    Scanner : Type
    Scanner = JVM_Native scannerClass

    hasNext : Scanner -> JVM_IO Bool
    hasNext = invokeInstance "hasNext" (Scanner -> JVM_IO Bool)

    Inherits Closeable Scanner where {}


text:
module Main

import Data.Primitives.Views

quiz : Stream Int -> (score : Nat) -> IO ()
quiz (n1 :: n2 :: ns) score = do
  putStrLn $ "Score so far: " ++ show score
  putStrLn (show n1 ++ " * " ++ show n2 ++ "?")
  answer <- getLine
  case answer of
    "quit" => do putStrLn "Bye!"
                 pure ()
    _ => if cast answer == n1 * n2
           then do putStrLn "Correct!"
                   quiz ns (score + 1)
           else do putStrLn ("Wrong, the answer is " ++ show (n1 * n2))
                   quiz ns score

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

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

main : IO ()
main = quiz (arithInputs 52816) 0

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
-- --------------------------------------------------------------- [ Utils.idr ]
-- Module    : Utils.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Text.Markup.Edda.Process.Utils

import Data.AVL.Dict

%default total
%access export

lookupType : Dict String String -> Maybe String
lookupType = lookup "type"

lookupSrcLang : Dict String String -> Maybe String
lookupSrcLang = lookup "src_lang"

lookupSrcOpts : Dict String String -> Maybe String
lookupSrcOpts = lookup "src_opts"

nubAttribute : String -> Dict String String -> Dict String String
nubAttribute key as = fromList $ doNub key (toList as)
  where
    doNub : String -> List (String, String) -> List (String, String)
    doNub _   Nil     = Nil
    doNub key ((k,v)::xs) =
      case key == k of
        True => doNub key xs
        False => (k,v) :: doNub key xs

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Test.Generators

import Data.Nat
import Data.List
import Data.List.Elem
import Data.String
import Data.Vect
import public Hedgehog
import public Text.WebIDL.Types

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

-- list whose length scales linearily and shrinks towards 0
linList : Nat -> Gen a -> Gen (List a)
linList n = list (linear 0 n)

-- list whose length scales linearily and shrinks towards 1
linList1 : Nat -> Gen a -> Gen (List1 a)
linList1 n g = [| g ::: linList (pred n) g |]

-- string whose length scales linearily and shrinks towards 0
linString : Nat -> Gen Char -> Gen String
linString n = string (linear 0 n)

-- non-empty string whose length scales linearily and shrinks towards 1
linString1 : Nat -> Gen Char -> Gen String
linString1 n = string (linear 1 n)

maxInt : Integer
maxInt = 18446744073709551616

anyInt : Gen Integer
anyInt = integer $ exponentialFrom 0 (- maxInt) maxInt

posInt : Gen Integer
posInt = integer $ exponential 0 maxInt

nat : Gen Nat
nat = map fromInteger posInt

--------------------------------------------------------------------------------
--          Tokens
--------------------------------------------------------------------------------

export
identifier : Gen Identifier
identifier = map ident [| concIdent (maybe line) alpha rest |]
  where line : Gen Char
        line = element ['-','_']

        rest : Gen String
        rest = linString 15 (frequency [(20, alphaNum),(1,line)])

        concIdent : Maybe Char -> Char -> String -> String
        concIdent mc c r = maybe "" singleton mc ++ singleton c ++ r

        ident : String -> Identifier
        ident s = if isKeyword s then MkIdent "anIdentifier1_2_3" else MkIdent s

export
space : Gen String
space = linString1 5 (element [' ','\t','\n','\r'])

export
maybeSpace : Gen String
maybeSpace = frequency [(1, pure ""), (4, space)]

export
stringLit : Gen StringLit
stringLit = strLit <$> linList 15 unicode
  where escape : Char -> List Char
        escape '"'  = ['\\','"']
        escape '\\' = ['\\','\\']
        escape c    = [c]

        strLit : List Char -> StringLit
        strLit cs = MkStrLit $ fastPack $ '"' :: (cs >>= escape) ++ ['"']

export
intLit : Gen IntLit
intLit = choice [map int anyInt, map Hex nat, map Oct nat]
  where int : Integer -> IntLit
        int 0 = Oct 0
        int n = I n

export
floatLit : Gen FloatLit
floatLit = frequency [ (5, [| Exp sig nat (maybe nat) exp |])
                     , (5, [| NoExp sig nat nat |])
                     , (1, pure Infinity)
                     , (1, pure NegativeInfinity)
                     , (1, pure NaN)
                     ]

  where exp : Gen Integer
        exp = integer $ linearFrom 0 (-30) (30)

        sig : Gen Signum
        sig = element [Plus,Minus]

export
comment : Gen String
comment = choice [line, multiline]
  where noControl : Gen Char
        noControl = map (\c => if isControl c then ' ' else c) unicode

        noForward : Gen Char
        noForward = map (\c => if c == '/' then ' ' else c) unicode

        line : Gen String
        line = map ("//" ++) $ string (linear 0 20) noControl

        multiline : Gen String
        multiline = map (\s => "/*" ++ s ++ "*/")
                  $ string (linear 0 20) noForward

export
symbol : Gen Symbol
symbol = frequency [ (10, map Symb latinSymbol)
                   , (1, pure Ellipsis)
                   ]
  where latinSymbol : Gen Char
        latinSymbol = choice [ charc '!' '/'
                             , charc ':' '@'
                             , charc '[' '`'
                             , charc '{' '~'
                             , charc (chr 161) (chr 255)
                             ]

symbolUnless : Char -> (Char -> Bool) -> Gen Symbol
symbolUnless x f = map replace symbol
  where replace : Symbol -> Symbol
        replace (Symb c) = if f c then Symb x else Symb c
        replace p        = p

--------------------------------------------------------------------------------
--          Parser
--------------------------------------------------------------------------------

otherUnless : (Char -> Bool) -> Gen Other
otherUnless f = choice [ map (\v => inject v) identifier
                       , map (\v => inject v) intLit
                       , map (\v => inject v) stringLit
                       , map (\v => inject v) floatLit
                       , map (\v => inject v) (symbolUnless '@' f)
                       ]

export
otherOrComma : Gen Other
otherOrComma = otherUnless isParenOrQuote

export
other : Gen Other
other = otherUnless isCommaOrParenOrQuote

eaInner : Nat -> Gen EAInner
eaInner 0     = pure EAIEmpty
eaInner (S k) = frequency [ (4, eaInner 0)
                          , (1, [| EAIOther otherOrComma (eaInner k) |])
                          , (1, [| EAIParens (eaInner k) (eaInner k) |])
                          ]

export
extAttribute : Nat -> Gen ExtAttribute
extAttribute 0     = choice [ map (`EAParens` Nothing) (eaInner 0)
                            , map (`EAOther` Nothing) other ]

extAttribute (S k) = let rest = maybe $ extAttribute k
                      in choice [ extAttribute 0
                                , [| EAParens (eaInner k) rest |]
                                , [| EAOther other rest |]
                                ]

export
attributes : Gen ExtAttributeList
attributes = linList 2 $ extAttribute 3

export
attributed : Gen a -> Gen (Attributed a)
attributed ga = [| (,) attributes ga |]

--------------------------------------------------------------------------------
--          Types
--------------------------------------------------------------------------------

bufferRelated : Gen BufferRelatedType
bufferRelated = element [ ArrayBuffer
                        , DataView
                        , Int8Array
                        , Int16Array
                        , Int32Array
                        , Uint8Array
                        , Uint16Array
                        , Uint32Array
                        , Uint8ClampedArray
                        , Float32Array
                        , Float64Array
                        ]

stringType : Gen StringType
stringType = element [ByteString, DOMString, USVString]

export
primitive : Gen PrimitiveType
primitive = element [ Undefined
                    , Boolean
                    , Octet
                    , Byte
                    , BigInt
                    , Restricted Dbl
                    , Restricted Float
                    , Signed Short
                    , Signed Long
                    , Signed LongLong
                    , Unsigned Short
                    , Unsigned Long
                    , Unsigned LongLong
                    , Unrestricted Dbl
                    , Unrestricted Float
                    ]

nullable : Gen a -> Gen (Nullable a)
nullable g = choice [ map NotNull g, map MaybeNull g ]

mutual
  export
  idlType : Nat -> Gen IdlType
  idlType 0     = frequency [ (1, pure Any), (10, map D (distinguishable 0)) ]
  idlType (S k) = frequency [ (2, idlType 0)
                            , (1, Promise <$> idlType k)
                            , (2, map D (distinguishable k))
                            ]

  dist : Nat -> Gen Distinguishable
  dist 0     = choice [ (map P primitive)
                      , (map S stringType)
                      , (map I identifier)
                      , (map B bufferRelated)
                      , element [Object, Symbol]
                      ]

  dist (S k) = choice [ [| Sequence attributes (idlType k) |]
                      , [| FrozenArray attributes (idlType k) |]
                      , [| ObservableArray attributes (idlType k) |]
                      , [| Record stringType attributes (idlType k) |]
                      ]

  distinguishable : Nat -> Gen (Nullable Distinguishable)
  distinguishable n = nullable (dist n)

  union : Nat -> Gen UnionType
  union n = let um = unionMember n
             in [| UT um um (linList 2 um) |]

  unionMember : Nat -> Gen UnionMemberType
  unionMember 0     = [| MkUnionMember attributes (dist 0) |]
  unionMember (S k) = [| MkUnionMember attributes (dist k) |]

idlType' : Gen IdlType
idlType' = idlType 4

attributedType : Gen (Attributed IdlType)
attributedType = attributed idlType'

optionalType : Gen OptionalType
optionalType = maybe attributedType

--------------------------------------------------------------------------------
--          Arguments
--------------------------------------------------------------------------------

constValue : Gen ConstValue
constValue = choice [ map B bool, map I intLit, map F floatLit ]

defaultVal : Gen Default
defaultVal = choice [ map C constValue
                    , map S stringLit
                    , element [None, EmptyList, EmptySet, Null]
                    ]

argName : Gen ArgumentName
argName = choice [ map (MkArgName . value) identifier
                 , map MkArgName $ element [ "async"
                                           , "attribute"
                                           , "callback"
                                           , "const"
                                           , "constructor"
                                           , "deleter"
                                           , "dictionary"
                                           , "enum"
                                           , "getter"
                                           , "includes"
                                           , "inherit"
                                           , "interface"
                                           , "iterable"
                                           , "maplike"
                                           , "mixin"
                                           , "namespace"
                                           , "partial"
                                           , "readonly"
                                           , "required"
                                           , "setlike"
                                           , "setter"
                                           , "static"
                                           , "stringifier"
                                           , "typedef"
                                           , "unrestricted" ]
                 ]

arg : Gen Arg
arg = [| MkArg attributes idlType' argName |]

optArg : Gen OptArg
optArg = [| MkOptArg attributes attributes idlType' argName defaultVal |]

argumentList : Gen ArgumentList
argumentList =
  choice [ [| VarArg (linList 5 arg) arg |]
         , [| NoVarArg (linList 5 arg) (linList 5 optArg) |]
         ]

constType : Gen ConstType
constType = choice [map CP primitive, map CI identifier]

--------------------------------------------------------------------------------
--          Member
--------------------------------------------------------------------------------

memberSize : Nat
memberSize = 20

export
const : Gen Const
const = [| MkConst constType identifier constValue |]

special : Gen Special
special = element [Getter,Setter,Deleter]

opName : Gen OperationName
opName = frequency [ (1, pure (MkOpName "includes"))
                   , (10, map (MkOpName . value) identifier)
                   ]

op : Gen a -> Gen (Op a)
op g = [| MkOp g idlType' (maybe opName) (argumentList) |]

regularOperation : Gen RegularOperation
regularOperation = op $ pure ()

specialOperation : Gen SpecialOperation
specialOperation = op special

export
operation : Gen Operation
operation = choice [ map regToOp  regularOperation
                   , map specToOp specialOperation
                   ]

callbackInterfaceMember : Gen CallbackInterfaceMember
callbackInterfaceMember = choice [ map (\v => inject v) const
                                 , map (\v => inject v) regularOperation
                                 ]

callbackInterfaceMembers : Gen CallbackInterfaceMembers
callbackInterfaceMembers = linList memberSize (attributed callbackInterfaceMember)

inheritance : Gen Inheritance
inheritance = maybe identifier

dictMemberRest : Gen DictionaryMemberRest
dictMemberRest =
  choice [ [| Required attributes idlType' identifier |]
         , [| Optional idlType' identifier defaultVal |]
         ]

dictMembers : Gen DictionaryMembers
dictMembers = linList memberSize (attributed dictMemberRest)

attributeName : Gen AttributeName
attributeName =
  frequency [ (5, map (MkAttributeName . value) identifier)
            , (1, map MkAttributeName $ element ["async","required"])
            ]

readonly : Gen a -> Gen (Readonly a)
readonly = map MkRO

inherit : Gen a -> Gen (Inherit a)
inherit = map MkI

attribute : Gen Attribute
attribute = [| MkAttribute attributes idlType' attributeName |]

stringifier : Gen Stringifier
stringifier = choice [ map (\v => inject v) regularOperation
                     , map (\v => inject v) $ readonly attribute
                     , map (\v => inject v) $ attribute
                     , map (\v => inject v) (pure ())
                     ]

static : Gen StaticMember
static = choice [ map (\v => inject v) regularOperation
                , map (\v => inject v) $ readonly attribute
                , map (\v => inject v) $ attribute
                ]

maplike : Gen Maplike
maplike = [| MkMaplike attributedType attributedType |]

setlike : Gen Setlike
setlike = [| MkSetlike attributedType |]

namespaceMember : Gen NamespaceMember
namespaceMember = choice [ map (\v => inject v) regularOperation
                         , map (\v => inject v) $ readonly attribute
                         ]

namespaceMembers : Gen NamespaceMembers
namespaceMembers = linList memberSize (attributed namespaceMember)

constructor_ : Gen Constructor
constructor_ = map MkConstructor argumentList

partialInterfaceMember : Gen PartialInterfaceMember
partialInterfaceMember =
  choice [ map IConst const
         , map IOp operation
         , map IAttr attribute
         , map IAttrRO (readonly attribute)
         , map IAttrInh (inherit attribute)
         , map IMap maplike
         , map IMapRO (readonly maplike)
         , map ISet setlike
         , map ISetRO (readonly setlike)
         , map IStr stringifier
         , map IStatic static
         , [| IIterable attributedType optionalType |]
         , [| IAsync attributedType optionalType argumentList |]
         ]

mixinMember : Gen MixinMember
mixinMember = choice [ map MConst const
                     , map MOp regularOperation
                     , map MAttr attribute
                     , map MAttrRO (readonly attribute)
                     , map MStr stringifier
                     ]

mixinMembers : Gen MixinMembers
mixinMembers = linList memberSize (attributed mixinMember)

partialInterfaceMembers : Gen PartialInterfaceMembers
partialInterfaceMembers = linList memberSize (attributed partialInterfaceMember)

export
interfaceMember : Gen InterfaceMember
interfaceMember = frequency [ (1, map (\v => inject v) constructor_)
                            , (10, map (\v => inject v) partialInterfaceMember)
                            ]

interfaceMembers : Gen InterfaceMembers
interfaceMembers = linList memberSize (attributed interfaceMember)

--------------------------------------------------------------------------------
--          Definition
--------------------------------------------------------------------------------

export
definition : Gen Definition
definition = ns
  [ [| MkCallback attributes identifier idlType' argumentList |]
  , [| MkCallbackInterface attributes identifier callbackInterfaceMembers |]
  , [| MkDictionary attributes identifier inheritance dictMembers |]
  , [| MkEnum attributes identifier (linList1 5 stringLit) |]
  , [| MkIncludes attributes identifier identifier |]
  , [| MkInterface attributes identifier inheritance interfaceMembers |]
  , [| MkMixin  attributes identifier mixinMembers |]
  , [| MkNamespace attributes identifier namespaceMembers |]
  , [| MkTypedef attributes attributes idlType' identifier |]
  ]

export
part : Gen Part
part = ns
  [ [| MkPDictionary attributes identifier dictMembers |]
  , [| MkPInterface attributes identifier partialInterfaceMembers |]
  , [| MkPMixin attributes identifier mixinMembers |]
  , [| MkPNamespace attributes identifier namespaceMembers |]
  ]


text:
module Inigo.Async.Git

import Inigo.Async.Base
import Inigo.Async.Promise
import Inigo.Async.FS
import System.Path

||| Download a git repository optionally specifying the commit, then remove the .git folder
||| Returns `True` iff the file already exists.
export
git_downloadTo : (url : String) -> (commit : Maybe String) -> (dest : String) -> Promise Bool
git_downloadTo url commit dest = do
    case !(fs_exists dest) of
        False => do
            ignore $ system "git" ["clone", "-q", "--progress", "--recurse-submodules", url, dest] Nothing False False
            maybe
                (pure ())
                (\com => ignore $ system "git" ["checkout", "-q", com] (Just dest) False False)
                commit
            fs_rmdir True (dest </> ".git")
            pure False
        True => pure True


text:
module Minecraft.Base.PreClassic.Stone.ItemEntity

import public Minecraft.Base.PreClassic.Stone
import public Minecraft.Core.Entity.Pickup.Export
import public Minecraft.Data.Type.Vtbl

%default total

namespace Export
  public export %hint stoneItemEntity : Pickup Stone.ItemEntity
  public export %hint stoneVtbl       : Vtbl   Stone.ItemEntity

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Control.JS.Async

export
data Async : Type -> Type where
    Pure : a -> Async a
    LiftIO : PrimIO a -> Async a
    Asyn : ((a -> PrimIO ()) -> PrimIO ()) -> Async a
    Par : Async (a -> b) -> Async a -> Async b
    Bind : Async a -> (a -> Async b) -> Async b

export
Functor Async where
    map f (Pure x) = Pure $ f x
    map f (LiftIO g) = LiftIO $ \w => let MkIORes x w' = g w in MkIORes (f x) w'
    map f (Asyn g) = Asyn $ \k, w => g (\x, w' => k (f x) w') w
    map f (Par mf mx) = Par (map (f .) mf) mx
    map f (Bind mx g) = Bind mx $ \x => map f $ g x

export
Applicative Async where
    pure = Pure
    mf <*> mx = Bind mf $ \f => map f mx

export
[Parallel] Applicative Async where
    pure = Pure
    (<*>) = Par

export
Monad Async where
    (>>=) = Bind

export
HasIO Async where
    liftIO act = LiftIO (toPrim act)

export %inline
parallel : Traversable t => t (Async a) -> Async (t a)
parallel = sequence @{Parallel}

export %inline
parallelMap : Traversable t => (a -> Async b) -> t a -> Async (t b)
parallelMap = traverse @{%search} @{Parallel}

export %inline
prim__async : ((a -> PrimIO ()) -> PrimIO ()) -> Async a
prim__async = Asyn

export %inline
async : ((a -> IO ()) -> IO ()) -> Async a
async f = prim__async (\k, w => toPrim (f (\x => fromPrim (k x))) w)

data Promise : Type -> Type where [external]

%foreign "javascript:support:pure,async"
promise__pure : {0 a : _} -> a -> PrimIO (Promise a)

%foreign "javascript:support:liftIO,async"
promise__liftIO : {0 a : _} -> PrimIO a -> PrimIO (Promise a)

%foreign "javascript:support:async,async"
promise__async : {0 a : _} -> ((a -> PrimIO ()) -> PrimIO ()) -> PrimIO (Promise a)

%foreign "javascript:support:par_app,async"
promise__par_app : {0 a, b : _} -> Promise (a -> b) -> Promise a -> PrimIO (Promise b)

%foreign "javascript:support:bind,async"
promise__bind :{0 a, b : _} -> Promise a -> (a -> PrimIO (Promise b)) -> PrimIO (Promise b)

export
toPromise : Async a -> IO (Promise a)
toPromise (Pure x) = fromPrim $ promise__pure x
toPromise (LiftIO f) = fromPrim $ promise__liftIO f
toPromise (Asyn f) = fromPrim $ promise__async f
toPromise (Par x y) = fromPrim $ promise__par_app !(toPromise x) !(toPromise y)
toPromise (Bind x f) = fromPrim $ promise__bind !(toPromise x) (\x => toPrim $ toPromise (f x))

export
launch : Async a -> IO ()
launch = ignore . toPromise


text:
module Idris.IDEMode.REPL

import Compiler.Scheme.Chez
import Compiler.Scheme.Racket
import Compiler.Scheme.Gambit
import Compiler.Common

import Core.AutoSearch
import Core.CompileExpr
import Core.Context
import Core.Directory
import Core.InitPrimitives
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.TT
import Core.Unify

import Data.List
import Data.So
import Data.String

import Idris.Desugar
import Idris.Error
import Idris.ModTree
import Idris.Package
import Idris.Parser
import Idris.Pretty
import Idris.Resugar
import Idris.REPL
import Idris.Syntax
import Idris.Version
import Idris.Doc.String

import Idris.IDEMode.Commands
import Idris.IDEMode.Holes
import Idris.IDEMode.Parser
import Idris.IDEMode.SyntaxHighlight

import TTImp.Interactive.CaseSplit
import TTImp.Elab
import TTImp.TTImp
import TTImp.ProcessDecls

import Libraries.Utils.Hex
import Libraries.Utils.Path

import Data.List
import System
import System.FFI
import System.File

import Network.Socket
import Network.Socket.Data

%default covering

idrisSocketClass : String
idrisSocketClass = "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket"

||| TODO: use the version in `Network.FFI` in network after the next release.
%foreign
  "C:idrnet_fdopen, libidris2_support, idris_net.h"
  jvm idrisSocketClass "toFile"
prim__idrnet_fdopen : SocketDescriptor -> String -> PrimIO AnyPtr

export
socketToFile : Socket -> IO (Either String File)
socketToFile (MkSocket f _ _ _) = do
  file <- FHandle <$> primIO (prim__idrnet_fdopen f "r+")
  if !(fileError file)
    then pure (Left "Failed to fdopen socket file descriptor")
    else pure (Right file)

export
initIDESocketFile : String -> Int -> IO (Either String File)
initIDESocketFile h p = do
  osock <- socket AF_INET Stream 0
  case osock of
    Left fail => do
      putStrLn (show fail)
      putStrLn "Failed to open socket"
      exitWith (ExitFailure 1)
    Right sock => do
      res <- bind sock (Just (Hostname h)) p
      if res /= 0
        then pure (Left ("Failed to bind socket with error: " ++ show res))
        else
          do res <- listen sock
             if res /= 0
                then
                  pure (Left ("Failed to listen on socket with error: " ++ show res))
               else
                 do putStrLn (show p)
                    fflush stdout
                    res <- accept sock
                    case res of
                      Left err =>
                         pure (Left ("Failed to accept on socket with error: " ++ show err))
                      Right (s, _) =>
                         socketToFile s

getChar : File -> IO Char
getChar h = do
  if !(fEOF h)
     then do
       putStrLn "Alas the file is done, aborting"
       exitWith (ExitFailure 1)
     else do
       Right chr <- fGetChar h
           | Left err => do putStrLn "Failed to read a character"
                            exitWith (ExitFailure 1)
       pure chr

getFLine : File -> IO String
getFLine h
    = do Right str <- fGetLine h
               | Left err =>
                   do putStrLn "Failed to read a line"
                      exitWith (ExitFailure 1)
         pure str

getNChars : File -> Nat -> IO (List Char)
getNChars i Z = pure []
getNChars i (S k)
    = do x <- getChar i
         xs <- getNChars i k
         pure (x :: xs)

-- Read 6 characters. If they're a hex number, read that many characters.
-- Otherwise, just read to newline
getInput : File -> IO String
getInput f
    = do x <- getNChars f 6
         case fromHexChars (reverse x) of
              Nothing =>
                do rest <- getFLine f
                   pure (pack x ++ rest)
              Just num =>
                do inp <- getNChars f (integerToNat num)
                   pure (pack inp)

||| Do nothing and tell the user to wait for us to implmement this (or join the effort!)
todoCmd : {auto c : Ref Ctxt Defs} ->
          {auto o : Ref ROpts REPLOpts} ->
          String -> Core ()
todoCmd cmdName = iputStrLn $ reflow $ cmdName ++ ": command not yet implemented. Hopefully soon!"

data IDEResult
  = REPL REPLResult
  | NameList (List Name)
  | Term String   -- should be a PTerm + metadata, or SExp.
  | TTTerm String -- should be a TT Term + metadata, or perhaps SExp
  | NameLocList (List (Name, FC))

replWrap : Core REPLResult -> Core IDEResult
replWrap m = pure $ REPL !m

process : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto m : Ref MD Metadata} ->
          {auto o : Ref ROpts REPLOpts} ->
          IDECommand -> Core IDEResult
process (Interpret cmd)
    = replWrap $ interpret cmd
process (LoadFile fname_in _)
    = do let fname = case !(findIpkg (Just fname_in)) of
                          Nothing => fname_in
                          Just f' => f'
         replWrap $ Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname
process (NameAt name Nothing)
    = do defs <- get Ctxt
         glob <- lookupCtxtName (UN (mkUserName name)) (gamma defs)
         let dat = map (\(name, _, gdef) => (name, gdef.location)) glob
         pure (NameLocList dat)
process (NameAt n (Just _))
    = do todoCmd "name-at <name> <line> <column>"
         pure $ REPL $ Edited $ DisplayEdit emptyDoc
process (TypeOf n Nothing)
    = replWrap $ Idris.REPL.process (Check (PRef replFC (UN $ mkUserName n)))
process (TypeOf n (Just (l, c)))
    = replWrap $ Idris.REPL.process
               $ Editing (TypeAt (fromInteger l) (fromInteger c) (UN $ mkUserName n))
process (CaseSplit l c n)
    = replWrap $ Idris.REPL.process
    $ Editing $ CaseSplit False (fromInteger l) (fromInteger c)
    $ UN $ mkUserName n
process (AddClause l n)
    = replWrap $ Idris.REPL.process
    $ Editing $ AddClause False (fromInteger l)
    $ UN $ mkUserName n
process (AddMissing l n)
    = do todoCmd "add-missing"
         pure $ REPL $ Edited $ DisplayEdit emptyDoc
process (ExprSearch l n hs all)
    = replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l)
                     (UN $ Basic n) (map (UN . Basic) hs)))
process ExprSearchNext
    = replWrap $ Idris.REPL.process (Editing ExprSearchNext)
process (GenerateDef l n)
    = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN $ Basic n) 0))
process GenerateDefNext
    = replWrap $ Idris.REPL.process (Editing GenerateDefNext)
process (MakeLemma l n)
    = replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN $ mkUserName n)))
process (MakeCase l n)
    = replWrap $ Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN $ mkUserName n)))
process (MakeWith l n)
    = replWrap $ Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN $ mkUserName n)))
process (DocsFor n modeOpt)
    = replWrap $ Idris.REPL.process (Doc (PRef EmptyFC (UN $ mkUserName n)))
process (Apropos n)
    = do todoCmd "apropros"
         pure $ REPL $ Printed emptyDoc
process (Directive n)
    = do todoCmd "directive"
         pure $ REPL $ Printed emptyDoc
process (WhoCalls n)
    = do todoCmd "who-calls"
         pure $ NameList []
process (CallsWho n)
    = do todoCmd "calls-who"
         pure $ NameList []
process (BrowseNamespace ns)
    = replWrap $ Idris.REPL.process (Browse (mkNamespace ns))
process (NormaliseTerm tm)
    = do todoCmd "normalise-term"
         pure $ Term tm
process (ShowTermImplicits tm)
    = do todoCmd "show-term-implicits"
         pure $ Term tm
process (HideTermImplicits tm)
    = do todoCmd "hide-term-implicits"
         pure $ Term tm
process (ElaborateTerm tm)
    = do todoCmd "elaborate-term"
         pure $ TTTerm tm
process (PrintDefinition n)
    = do todoCmd "print-definition"
         pure $ REPL $ Printed (pretty n)
process (ReplCompletions n)
    = do todoCmd "repl-completions"
         pure $ NameList []
process (EnableSyntax b)
    = do setSynHighlightOn b
         pure $ REPL $ Printed (reflow "Syntax highlight option changed to" <++> pretty b)
process Version
    = replWrap $ Idris.REPL.process ShowVersion
process (Metavariables _)
    = replWrap $ Idris.REPL.process Metavars
process GetOptions
    = replWrap $ Idris.REPL.process GetOpts

processCatch : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto m : Ref MD Metadata} ->
               {auto o : Ref ROpts REPLOpts} ->
               IDECommand -> Core IDEResult
processCatch cmd
    = do c' <- branch
         u' <- get UST
         s' <- get Syn
         o' <- get ROpts
         catch (do res <- process cmd
                   commit
                   pure res)
               (\err => do put Ctxt c'
                           put UST u'
                           put Syn s'
                           put ROpts o'
                           msg <- perror err
                           pure $ REPL $ REPLError msg)

idePutStrLn : {auto c : Ref Ctxt Defs} -> File -> Integer -> String -> Core ()
idePutStrLn outf i msg
    = send outf (SExpList [SymbolAtom "write-string",
                toSExp msg, toSExp i])

returnFromIDE : {auto c : Ref Ctxt Defs} -> File -> Integer -> SExp -> Core ()
returnFromIDE outf i msg
    = do send outf (SExpList [SymbolAtom "return", msg, toSExp i])

printIDEResult : {auto c : Ref Ctxt Defs} -> File -> Integer -> SExp -> Core ()
printIDEResult outf i msg
  = returnFromIDE outf i
  $ SExpList [ SymbolAtom "ok"
             , toSExp msg
             ]

export
SExpable a => SExpable (Span a) where
  toSExp (MkSpan start width ann)
    = SExpList [ IntegerAtom (cast start)
               , IntegerAtom (cast width)
               , toSExp ann
               ]

printIDEResultWithHighlight :
  {auto c : Ref Ctxt Defs} ->
  File -> Integer -> (SExp, List (Span Properties)) ->
  Core ()
printIDEResultWithHighlight outf i (msg, spans) = do
--  log "ide-mode.highlight" 10 $ show spans
  returnFromIDE outf i
    $ SExpList [ SymbolAtom "ok"
               , msg
               , toSExp spans
               ]

printIDEError : Ref ROpts REPLOpts => {auto c : Ref Ctxt Defs} -> File -> Integer -> Doc IdrisAnn -> Core ()
printIDEError outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "error", toSExp !(renderWithoutColor msg) ])

SExpable REPLEval where
  toSExp EvalTC = SymbolAtom "typecheck"
  toSExp NormaliseAll = SymbolAtom "normalise"
  toSExp Execute = SymbolAtom "execute"

SExpable REPLOpt where
  toSExp (ShowImplicits impl) = SExpList [ SymbolAtom "show-implicits", toSExp impl ]
  toSExp (ShowNamespace ns) = SExpList [ SymbolAtom "show-namespace", toSExp ns ]
  toSExp (ShowTypes typs) = SExpList [ SymbolAtom "show-types", toSExp typs ]
  toSExp (EvalMode mod) = SExpList [ SymbolAtom "eval", toSExp mod ]
  toSExp (Editor editor) = SExpList [ SymbolAtom "editor", toSExp editor ]
  toSExp (CG str) = SExpList [ SymbolAtom "cg", toSExp str ]
  toSExp (Profile p) = SExpList [ SymbolAtom "profile", toSExp p ]

displayIDEResult : {auto c : Ref Ctxt Defs} ->
       {auto u : Ref UST UState} ->
       {auto s : Ref Syn SyntaxInfo} ->
       {auto m : Ref MD Metadata} ->
       {auto o : Ref ROpts REPLOpts} ->
       File -> Integer -> IDEResult -> Core ()
displayIDEResult outf i  (REPL $ REPLError err)
  = printIDEError outf i err
displayIDEResult outf i  (REPL RequestedHelp  )
  = printIDEResult outf i
  $ StringAtom $ displayHelp
displayIDEResult outf i  (REPL $ Evaluated x Nothing)
  = printIDEResultWithHighlight outf i
  $ mapFst StringAtom
   !(renderWithDecorations syntaxToProperties $ prettyTerm x)
displayIDEResult outf i  (REPL $ Evaluated x (Just y))
  = printIDEResultWithHighlight outf i
  $ mapFst StringAtom
   !(renderWithDecorations syntaxToProperties
     $ prettyTerm x <++> ":" <++> prettyTerm y)
displayIDEResult outf i  (REPL $ Printed xs)
  = printIDEResultWithHighlight outf i
  $ mapFst StringAtom
  $ !(renderWithDecorations annToProperties xs)
displayIDEResult outf i (REPL (PrintedDoc xs))
  = printIDEResultWithHighlight outf i
  $ mapFst StringAtom
  $ !(renderWithDecorations docToProperties xs)
displayIDEResult outf i  (REPL $ TermChecked x y)
  = printIDEResultWithHighlight outf i
  $ mapFst StringAtom
   !(renderWithDecorations syntaxToProperties
     $ prettyTerm x <++> ":" <++> prettyTerm y)
displayIDEResult outf i  (REPL $ FileLoaded x)
  = printIDEResult outf i $ SExpList []
displayIDEResult outf i  (REPL $ ErrorLoadingFile x err)
  = printIDEError outf i $ reflow "Error loading file" <++> pretty x <+> colon <++> pretty (show err)
displayIDEResult outf i  (REPL $ ErrorsBuildingFile x errs)
  = do errs' <- traverse perror errs
       printIDEError outf i $ reflow "Error(s) building file" <++> pretty x <+> colon <++> vsep errs'
displayIDEResult outf i  (REPL $ NoFileLoaded)
  = printIDEError outf i $ reflow "No file can be reloaded"
displayIDEResult outf i  (REPL $ CurrentDirectory dir)
  = printIDEResult outf i
  $ StringAtom $ "Current working directory is \"" ++ dir ++ "\""
displayIDEResult outf i  (REPL CompilationFailed)
  = printIDEError outf i $ reflow "Compilation failed"
displayIDEResult outf i  (REPL $ Compiled f)
  = printIDEResult outf i $ StringAtom
  $ "File " ++ f ++ " written"
displayIDEResult outf i  (REPL $ ProofFound x)
  = printIDEResult outf i
  $ StringAtom $ show x
displayIDEResult outf i  (REPL $ Missed cases)
  = printIDEResult outf i
  $ StringAtom $ showSep "\n"
  $ map handleMissing' cases
displayIDEResult outf i  (REPL $ CheckedTotal xs)
  = printIDEResult outf i
  $ StringAtom $ showSep "\n"
  $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs
displayIDEResult outf i  (REPL $ FoundHoles holes)
  = printIDEResultWithHighlight outf i =<< case holes of
      []  => pure (StringAtom "No holes", [])
      [x] => do let hole = pretty x.name <++> colon <++> prettyTerm x.type
                hlght <- renderWithDecorations syntaxToProperties
                           $ "1 hole" <+> colon <++> hole
                pure $ mapFst StringAtom hlght
      xs => do let holes = xs <&> \ x => pretty x.name <++> colon <++> prettyTerm x.type
               let header = pretty (length xs) <++> pretty "holes" <+> colon
               hlght <- renderWithDecorations syntaxToProperties
                           $ vcat (header :: map (indent 2) holes)
               pure $ mapFst StringAtom hlght
displayIDEResult outf i  (REPL $ LogLevelSet k)
  = printIDEResult outf i
  $ StringAtom $ "Set loglevel to " ++ show k
displayIDEResult outf i  (REPL $ OptionsSet opts)
  = printIDEResult outf i optionsSexp
  where
    optionsSexp : SExp
    optionsSexp = SExpList $ map toSExp opts
displayIDEResult outf i  (REPL $ VersionIs x)
  = printIDEResult outf i versionSExp
  where
  semverSexp : SExp
  semverSexp = case (semVer x) of
                  (maj, min, patch) => SExpList (map toSExp [maj, min, patch])
  tagSexp : SExp
  tagSexp = case versionTag x of
              Nothing => SExpList [ StringAtom "" ]
              Just t => SExpList [ StringAtom t ]
  versionSExp : SExp
  versionSExp = SExpList [ semverSexp, tagSexp ]

displayIDEResult outf i (REPL $ Edited (DisplayEdit xs))
  = printIDEResult outf i $ StringAtom $ show xs
displayIDEResult outf i (REPL $ Edited (EditError x))
  = printIDEError outf i x
displayIDEResult outf i (REPL $ Edited (MadeLemma lit name pty pappstr))
  = printIDEResult outf i
  $ SExpList [ SymbolAtom "metavariable-lemma"
             , SExpList [ SymbolAtom "replace-metavariable", StringAtom pappstr ]
             , SExpList [ SymbolAtom "definition-type", StringAtom $ relit lit $ show name ++ " : " ++ show pty ]
             ]
displayIDEResult outf i (REPL $ Edited (MadeWith lit wapp))
  = printIDEResult outf i
  $ StringAtom $ showSep "\n" (map (relit lit) wapp)
displayIDEResult outf i (REPL $ (Edited (MadeCase lit cstr)))
  = printIDEResult outf i
  $ StringAtom $ showSep "\n" (map (relit lit) cstr)
displayIDEResult outf i (NameList ns)
  = printIDEResult outf i $ SExpList $ map toSExp ns
displayIDEResult outf i (Term t)
  = printIDEResult outf i $ StringAtom t
displayIDEResult outf i (TTTerm t)
  = printIDEResult outf i $ StringAtom t
displayIDEResult outf i (REPL $ ConsoleWidthSet mn)
  = let width = case mn of
                    Just k  => show k
                    Nothing => "auto"
    in printIDEResult outf i $ StringAtom $ "Set consolewidth to " ++ width
displayIDEResult outf i (NameLocList dat)
  = printIDEResult outf i $ SExpList !(traverse (constructSExp . map toNonEmptyFC) dat)
  where
    -- In order to recover the full path to the module referenced by FC,
    -- which stores a module identifier as opposed to a full path,
    -- we need to check the project's source folder and all the library directories
    -- for the relevant source file.
    -- (!) Always returns the *absolute* path.
    sexpOriginDesc : OriginDesc -> Core String
    sexpOriginDesc (PhysicalIdrSrc modIdent) = do
      defs <- get Ctxt
      let wdir = defs.options.dirs.working_dir
      let pkg_dirs = filter (/= ".") defs.options.dirs.extra_dirs
      let exts = map show listOfExtensions
      Just fname <- catch
          (Just . (wdir </>) <$> nsToSource replFC modIdent) -- Try local source first
          -- if not found, try looking for the file amongst the loaded packages.
          (const $ firstAvailable $ do
            pkg_dir <- pkg_dirs
            let pkg_dir_abs = ifThenElse (isRelative pkg_dir) (wdir </> pkg_dir) pkg_dir
            ext <- exts
            pure (pkg_dir_abs </> ModuleIdent.toPath modIdent <.> ext))
        | _ => pure "(File-Not-Found)"
      pure fname
    sexpOriginDesc (PhysicalPkgSrc fname) = pure fname
    sexpOriginDesc (Virtual Interactive) = pure "(Interactive)"

    constructSExp : (Name, NonEmptyFC) -> Core SExp
    constructSExp (name, origin, (startLine, startCol), (endLine, endCol)) = pure $
        SExpList [ StringAtom !(render $ pretty name)
                 , StringAtom !(sexpOriginDesc origin)
                 , IntegerAtom $ cast $ startLine
                 , IntegerAtom $ cast $ startCol
                 , IntegerAtom $ cast $ endLine
                 , IntegerAtom $ cast $ endCol
                 ]
-- do not use a catchall so that we are warned about missing cases when adding a
-- new construtor to the enumeration.
displayIDEResult _ _ (REPL Done) = pure ()
displayIDEResult _ _ (REPL (Executed _)) = pure ()
displayIDEResult _ _ (REPL (ModuleLoaded _)) = pure ()
displayIDEResult _ _ (REPL (ErrorLoadingModule _ _)) = pure ()
displayIDEResult _ _ (REPL (ColorSet _)) = pure ()
displayIDEResult _ _ (REPL DefDeclared) = pure ()
displayIDEResult _ _ (REPL Exited) = pure ()

handleIDEResult : {auto c : Ref Ctxt Defs} ->
       {auto u : Ref UST UState} ->
       {auto s : Ref Syn SyntaxInfo} ->
       {auto m : Ref MD Metadata} ->
       {auto o : Ref ROpts REPLOpts} ->
       File -> Integer -> IDEResult -> Core ()
handleIDEResult outf i (REPL Exited) = idePutStrLn outf i "Bye for now!"
handleIDEResult outf i other = displayIDEResult outf i other

loop : {auto c : Ref Ctxt Defs} ->
       {auto u : Ref UST UState} ->
       {auto s : Ref Syn SyntaxInfo} ->
       {auto m : Ref MD Metadata} ->
       {auto o : Ref ROpts REPLOpts} ->
       Core ()
loop
    = do res <- getOutput
         case res of
              REPL _ => printError $ reflow "Running idemode but output isn't"
              IDEMode idx inf outf => do
                inp <- coreLift $ getInput inf
                end <- coreLift $ fEOF inf
                if end
                   then pure ()
                   else case parseSExp inp of
                      Left err =>
                        do printIDEError outf idx (reflow "Parse error:" <++> !(perror err))
                           loop
                      Right sexp =>
                        case getMsg sexp of
                          Just (cmd, i) =>
                            do updateOutput i
                               res <- processCatch cmd
                               handleIDEResult outf i res
                               loop
                          Nothing =>
                            do printIDEError outf idx (reflow "Unrecognised command:" <++> pretty (show sexp))
                               loop
  where
    updateOutput : Integer -> Core ()
    updateOutput idx
        = do IDEMode _ i o <- getOutput
                 | _ => pure ()
             setOutput (IDEMode idx i o)

export
replIDE : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto m : Ref MD Metadata} ->
          {auto o : Ref ROpts REPLOpts} ->
          Core ()
replIDE
    = do res <- getOutput
         case res of
              REPL _ => printError $ reflow "Running idemode but output isn't"
              IDEMode _ inf outf => do
                send outf (version 2 0)
                loop


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.TOML.Parser

import Language.TOML.ConcreteSyntax
import Language.TOML.Tokens

import Text.Parser
import Text.Token

import Data.List
import Data.List1

private
punct : Punctuation -> Grammar TOMLToken True ()
punct p = match $ TTPunct p

private
maybeNewlines : Grammar TOMLToken False ()
maybeNewlines = do
    _ <- many (punct NewLine)
    pure ()

private
newlines : Grammar TOMLToken False ()
newlines = (some (punct NewLine) >>= \_ => pure ()) <|> eof

private
allowNewlines : (p : Grammar TOMLToken True a) -> Grammar TOMLToken True a
allowNewlines p = maybeNewlines *> p <* maybeNewlines

private
unescape : List Char -> List Char
unescape ('"'::rest) = loop rest
    where
        loop : List Char -> List Char
        loop [] = []
        loop ('"'::_) = []
        loop ('\\'::'"'::rest) = '"' :: loop rest
        loop (x::rest) = x :: loop rest
unescape _ = []

private
string : Grammar TOMLToken True CValue
string = map (CVString . pack . unescape . unpack) $ match TTString

private
boolean : Grammar TOMLToken True CValue
boolean = map CVBoolean $ match TTBoolean

private
integer : Grammar TOMLToken True CValue
integer = map CVInteger $ match TTInt

private
float : Grammar TOMLToken True CValue
float = map CVFloat $ match TTFloat

private
bare : Grammar TOMLToken True String
bare = match TTBare

private
key : Grammar TOMLToken True CKey
key = do
        first <- keyAtom
        rest <- many (punct Dot *> keyAtom)
        case rest of
            [] => pure $ CKAtom first
            rest => pure $ CKDotted (first:::rest)
    where
        keyAtom : Grammar TOMLToken True CKeyAtom
        keyAtom = map CKBare bare
              <|> (map CKQuoted $ match TTString)

mutual
    private
    value : Grammar TOMLToken True CValue
    value = string
        <|> boolean
        <|> integer
        <|> float
        <|> array
        <|> inlineTable

    private
    array : Grammar TOMLToken True CValue
    array = do
        punct (Square Open)
        commit
        vals <- sepBy (allowNewlines $ punct Comma) (allowNewlines value)
        punct (Square Close)
        pure $ CVArray vals

    private
    inlineTable : Grammar TOMLToken True CValue
    inlineTable = do
        punct (Curly Open)
        commit
        vals <- sepBy (punct Comma) $ do
            k <- key
            punct Equal
            v <- value
            pure (k, v)

        punct (Curly Close)
        pure $ CVInlineTable vals

private
keyValue : Grammar TOMLToken True Item
keyValue = do
    k <- key
    punct Equal
    v <- value
    newlines
    pure $ IKeyValue k v

private
tableHeader : Grammar TOMLToken True Item
tableHeader = do
    punct (Square Open)
    k <- key
    commit
    punct (Square Close)
    newlines
    pure $ ITableHeader k

private
tableArrayHeader : Grammar TOMLToken True Item
tableArrayHeader = do
    punct (Square Open)
    punct (Square Open)
    commit
    k <- key
    punct (Square Close)
    punct (Square Close)
    newlines
    pure $ ITableArray k

private
item : Grammar TOMLToken True Item
item = keyValue
   <|> tableHeader
   <|> tableArrayHeader

private
items : Grammar TOMLToken False (List Item)
items = do
    maybeNewlines
    is <- many item
    maybeNewlines
    eof
    pure is

export
parseItems : List TOMLToken -> Either String (List Item)
parseItems toks = case parse items $ filter (not . ignored) toks of
    Right (its, []) => Right its
    Right _ => Left "unconsumed input"
    Left (Error msg _) => Left msg

max_stars_repo_name: tiatomee/toml-idr

max_issues_repo_name: tiatomee/toml-idr

max_forks_repo_name: tiatomee/toml-idr


text:
module PQ.CRUD

import Control.Monad.Either
import Data.List
import Data.List.Elem
import Data.SOP
import PQ.FFI
import PQ.Schema
import PQ.Types

%default total

public export
data Elems : List a -> List a -> Type where
  Single : Elem x vs -> Elems [x] vs
  (::)   : Elem x vs -> Elems xs vs -> Elems (x :: xs) vs

public export
Row : (f : Column -> Type) -> List Column -> Type
Row = NP

--------------------------------------------------------------------------------
--          Insert
--------------------------------------------------------------------------------

public export
0 PutRow : List Column -> Type
PutRow = Row PutTypeC

public export
0 GetTypes : List Column -> List Type
GetTypes = map GetTypeC

public export
0 GetRow : List Column -> Type
GetRow cs = NP I (GetTypes cs)

colVals : (cs : List Column) -> PutRow cs -> List String
colVals [] [] = []
colVals (MkField _ n pqTpe _ dflt _ toPQ _:: cs) (v :: vs) =
  encodePutType dflt (toPQ v) :: colVals cs vs

colStr : (cs : List Column) -> PutRow cs -> String
colStr cs row =
  let vals = fastConcat $ intersperse ", " (colVals cs row)
   in #"(\#{vals})"#

export
insertSQL : (t : Table) -> List (PutRow (columns t)) -> String
insertSQL (MkTable n cs) rows =
  let colNames = fastConcat $ intersperse ", " (map name cs)
      allVals  = fastConcat $ intersperse ", " (map (colStr cs) rows)
   in #"INSERT INTO \#{n} (\#{colNames}) VALUES \#{allVals};"#

export
getSQL :  (t        : Table)
       -> (cs       : List Column)
       -> {auto 0 _ : Elems cs (columns t)}
       -> (query    : Op)
       -> String
getSQL t cs query =
  let cols = fastConcat $ intersperse ", " $ map name cs
   in #"SELECT \#{cols} FROM \#{t.name} WHERE \#{opToSQL query};"#

export
count : (t : Table) -> (query : Op) -> String
count t query = #"SELECT count(*) FROM \#{t.name} WHERE \#{opToSQL query};"#

export
getJoinSQL :  (t1        : Table)
       ->     (t2       : Table)
       -> (cs       : List Column)
  --     -> {auto 0 _ : Elems cs ((columns t1)++(columns t2)) }
       -> (query    : Op)
       -> String
getJoinSQL t1 t2 cs query =
  let cols = fastConcat $ intersperse ", " $ [ (table_name x)++"."++(name x) | x <- cs ]
   in #"SELECT \#{cols} FROM \#{t1.name},\#{t2.name} WHERE \#{opToSQL query};"#

--------------------------------------------------------------------------------
--          IO
--------------------------------------------------------------------------------

export
insert :  HasIO io
       => MonadError SQLError io
       => Connection
       -> (t : Table)
       -> List (PutRow (columns t))
       -> io ()
insert c t rows = exec_ c (insertSQL t rows) COMMAND_OK

export
insert1 :  HasIO io
        => MonadError SQLError io
        => Connection
        -> (t : Table)
        -> PutRow (columns t)
        -> io ()
insert1 c t row = insert c t [row]

export
names : (cs : List Column) -> NP (K String) (GetTypes cs)
names []        = []
names (x :: xs) = x.name :: names xs

reader : (c : Column) -> String -> Maybe (GetTypeC c)
reader (MkField _ _ pqType _ _ fromPQ _ _) s =
  fromPQ (decodeDBType pqType s)
export
readers : (cs : List Column) -> NP (\t => String -> Maybe t) (GetTypes cs)
readers []        = []
readers (x :: xs) = reader x :: readers xs

export
get :  HasIO io
    => MonadError SQLError io
    => Connection
    -> (t        : Table)
    -> (cs       : List Column)
    -> {auto 0 _ : Elems cs (columns t)}
    -> (query : Op)
    -> io (List $ GetRow cs)
get c t cs query = do
  res <- exec c (getSQL t cs query) TUPLES_OK
  getRows (names cs) (readers cs) res

export
getJoin :  HasIO io
    => MonadError SQLError io
    => Connection
    -> (t1        : Table)
    -> (t2        : Table)
    -> (cs       : List Column)
--    -> {auto 0 _ : Elems cs ((columns t1)++(columns t2))}
    -> (query : Op)
    -> io (List $ GetRow cs)
getJoin c t1 t2 cs query = do
  res <- exec c (getJoinSQL t1 t2 cs query) TUPLES_OK
  getRows (names cs) (readers cs) res

export
countCmd :  HasIO io
         => MonadError SQLError io
         => Connection
         -> (t     : Table)
         -> (query : Op)
         -> io Bits32
countCmd c t query = do
  res   <- exec c (count t query) TUPLES_OK
  [[c]] <- getRows ["count"] [Just . cast {to = Bits32}] res
    | _ => pure 0
  pure c

export
delete :  HasIO io
       => MonadError SQLError io
       => Connection
       -> (t     : Table)
       -> (query : Op)
       -> io ()
delete c t query =
  let sql = #"DELETE FROM \#{t.name} WHERE \#{opToSQL query};"#
   in exec_ c sql COMMAND_OK

export
clearTable :  HasIO io
           => MonadError SQLError io
           => Connection
           -> (t     : Table)
           -> io ()
clearTable c t = delete c t True

--------------------------------------------------------------------------------
--          Example
--------------------------------------------------------------------------------

Id : Column
Id = primarySerial64 Int64 "id" (Just) ""

Name : Column
Name =  notNull String "name" Text (Just) id ""

Orders : Column
Orders = notNullDefault Int32 "orders" PQInteger 0 Just (id) ""

MyTable : Table
MyTable = MkTable "customer" [Id, Name, Orders]

newCustomer : PutRow (columns MyTable)
newCustomer = [(), "Gundi", Nothing]

getIdName : String
getIdName = getSQL MyTable [Name,Id] (Orders >= 3)


text:
module Relations

import congruence

%access public export

%default total

||| Composing two relations and then extend them to the smallest equivalence relation containing them

data AddRel : (ty : Type) -> (ty -> ty -> Type) -> (ty -> ty -> Type) -> (ty -> ty -> Type) where

    Inc_l : (ty : Type) -> (r1, r2 : (ty -> ty -> Type)) ->
            (a, b : ty) -> (r1 a b) -> (AddRel ty r1 r2 a b)

    Inc_r : (ty : Type) -> (r1, r2 : (ty -> ty -> Type)) ->
            (a, b : ty) -> (r2 a b) -> (AddRel ty r1 r2 a b)

    Inc_refl : (ty : Type) -> (r1, r2 : (ty -> ty -> Type)) ->
               (a : ty) -> (AddRel ty r1 r2 a a)

    Inc_sym : (ty : Type) -> (r1, r2 : (ty -> ty -> Type)) ->
              (a, b : ty) -> (AddRel ty r1 r2 a b) -> (AddRel ty r1 r2 b a)

    Inc_trans : (ty : Type) -> (r1, r2 : (ty -> ty -> Type)) ->
                (a, b, c : ty) -> (AddRel ty r1 r2 a b) -> (AddRel ty r1 r2 b c) ->
                (AddRel ty r1 r2 a c)

||| A proof that the composition operation is commutative

f : (ty : Type) -> (r1, r2 : (ty -> ty -> Type)) -> (a, b : ty) ->
    (AddRel ty r1 r2 a b) -> (AddRel ty r2 r1 a b)

f ty r1 r2 a b (Inc_l ty r1 r2 a b pf) = (Inc_r ty r2 r1 a b pf)
f ty r1 r2 a b (Inc_r ty r1 r2 a b pf) = (Inc_l ty r2 r1 a b pf)
f ty r1 r2 a a (Inc_refl ty r1 r2 a) = (Inc_refl ty r2 r1 a)
f ty r1 r2 b a (Inc_sym ty r1 r2 a b pf) = (Inc_sym ty r2 r1 a b (f ty r1 r2 a b pf))
f ty r1 r2 a c (Inc_trans ty r1 r2 a b c pfab pfbc) =
    (Inc_trans ty r2 r1 a b c (f ty r1 r2 a b pfab) (f ty r1 r2 b c pfbc))

||| Proof that f is the inverse of itself

rel_property_1 : (ty : Type) -> (r1, r2 : (ty -> ty -> Type)) ->
                 (a, b : ty) -> (pf : (AddRel ty r1 r2 a b)) ->
                 ( (f ty r2 r1 a b (f ty r1 r2 a b pf)) = pf)

rel_property_1 ty r1 r2 a b (Inc_l ty r1 r2 a b pf) = Refl
rel_property_1 ty r1 r2 a b (Inc_r ty r1 r2 a b pf) = Refl
rel_property_1 ty r1 r2 b b (Inc_refl ty r1 r2 b) = Refl
rel_property_1 ty r1 r2 a b (Inc_sym ty r1 r2 b a pf) = let
    pf1 = rel_property_1 ty r1 r2 b a pf
    pf2 = congruence (AddRel ty r1 r2 b a) (AddRel ty r1 r2 a b)
        (f ty r2 r1 b a (f ty r1 r2 b a pf)) pf
        (Inc_sym ty r1 r2 b a) pf1
    in
    pf2

rel_property_1 ty r1 r2 a c (Inc_trans ty r1 r2 a b c pfab pfbc) = let

    pf1 = rel_property_1 ty r1 r2 a b pfab
    pf2 = rel_property_1 ty r1 r2 b c pfbc

    pf3 = congruence (AddRel ty r1 r2 b c) (AddRel ty r1 r2 a c)
        (f ty r2 r1 b c (f ty r1 r2 b c pfbc)) pfbc (\k => Inc_trans ty r1 r2 a b c pfab k) pf2

    pf4 = congruence (AddRel ty r1 r2 a b) (AddRel ty r1 r2 a c)
        (f ty r2 r1 a b (f ty r1 r2 a b pfab)) pfab (\k => Inc_trans ty r1 r2 a b c k (f ty r2 r1 b c (f ty r1 r2 b c pfbc))) pf1

    in
    (trans pf4 pf3)


text:
module Prims

data MyList a = Nil | (:::) a (MyList a)

infixr 10 :::

-- *Prims> 1 ::: Nil
-- 1 ::: [] : MyList Integer
-- *Prims> 0 ::: 1 ::: Nil
-- 0 ::: 1 ::: [] : MyList Integer

-- Idris requires type declarations, using a single colon :
head' : MyList a -> Maybe a
head' Nil = Nothing
head' (x ::: xs) = Just x

-- *Prims> :let ls : MyList Nat; ls = 0 ::: 1 ::: Nil
-- *Prims> head' ls
-- Just 0 : Maybe Nat

-- data Nat    = Z   | S Nat        Natural numbers (zero and successor)
-- Z : Nat                          data constructors

plus' : Nat -> Nat -> Nat
plus' Z     y = y
plus' (S k) y = S (plus' k y)

x : Int
x = 123

foo : String
foo = "boo"

bar : Char
bar = 'X'

bool : Bool
bool = True


text:
We start with a trivial language comtaining numbers and booleans.

> import Math
> import Data.List

> data UntypedTerm : Type where
>   CTrue : UntypedTerm
>   CFalse : UntypedTerm
>   IfThenElse : UntypedTerm -> UntypedTerm -> UntypedTerm -> UntypedTerm
>   CZero : UntypedTerm
>   Succ : UntypedTerm -> UntypedTerm
>   Pred : UntypedTerm -> UntypedTerm
>   IsZero : UntypedTerm -> UntypedTerm

We can create a generator for such terms:

> data UntypedTermGenerator : Nat -> List UntypedTerm -> Type where
>   GenEmpty : UntypedTermGenerator Z []
>   GenSucc : UntypedTermGenerator k xs -> UntypedTermGenerator (S k) ([CTrue,CFalse,CZero]) -- ++ (map ))

This generator in fact covers the UntypedTerms. First, we need a notion of the
size of a term

> size : UntypedTerm -> Nat
> size CTrue = 1
> size CFalse = 1
> size CZero = 1
> size (Succ t) = S (size t)
> size (Pred t) = S (size t)
> size (IsZero t) = S (size t)
> size (IfThenElse i t e) = S (plus (plus (size i) (size t)) (size e))

Since the terms form a tree there is a notion of depth:

> depth : UntypedTerm -> Nat
> depth CTrue = 1
> depth CFalse = 1
> depth CZero = 1
> depth (Succ t) = S (depth t)
> depth (Pred t) = S (depth t)
> depth (IsZero t) = S (depth t)
> depth (IfThenElse i t e) = S (maximum (maximum (depth i) (depth t)) (depth e))--S (maximum (maximum( (depth i) (depth t))) (depth e))

Now we can prove covering. We prove the equivalent result that for any Nat n and any UntypedTerm t with depth LTE n, then there exists an UntypedTermGenerator n xs such that Elem t xs.

> generatorCovers : (t:UntypedTerm) -> (xs : List UntypedTerm ** ((UntypedTermGenerator (depth t) xs), (Elem t xs)))--((n:Nat ** (UntypedTermGenerator n xs)) ** (Elem t xs))
> generatorCovers CTrue = ([CTrue,CFalse,CZero] ** (GenSucc GenEmpty,Here))
> generatorCovers CFalse = ([CTrue,CFalse,CZero] ** (GenSucc GenEmpty,There (the (Elem CFalse [CFalse,CZero]) Here)))
> generatorCovers (IfThenElse x y z) = ?generatorCovers_rhs_1
> generatorCovers CZero = ([CTrue,CFalse,CZero] ** (GenSucc GenEmpty,There (There (the (Elem CZero [CZero]) Here))))
> generatorCovers (Succ x) = ?generatorCovers_rhs_5
> generatorCovers (Pred x) = ?generatorCovers_rhs_6
> generatorCovers (IsZero x) = ?generatorCovers_rhs_7

ext: lidr

max_stars_repo_name: nicklecompte/CSLearning

max_issues_repo_name: nicklecompte/CSLearning

max_forks_repo_name: nicklecompte/CSLearning


text:
module Sub06Apply36x9

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(12x+3) --E[2,-4]--> 3x
e36x9To3x :
  (l:Nat) -> P (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l)))))) 2 -> P l 2
e36x9To3x l prf =
  let prf2 = lvDown (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l)))))) 2 prf in e36x9To3x' l prf2

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


text:
module Control.Algebra.VectorSpace

import public Control.Algebra

infixl 5 <#>
infixr 2 <||>

||| A module over a ring is an additive abelian group of 'vectors' endowed with a
||| scale operation multiplying vectors by ring elements, and distributivity laws
||| relating the scale operation to both ring addition and module addition.
||| Must satisfy the following laws:
|||
||| + Compatibility of scalar multiplication with ring multiplication:
|||     forall a b v,  a <#> (b <#> v) = (a <.> b) <#> v
||| + Ring unity is the identity element of scalar multiplication:
|||     forall v,      unity <#> v = v
||| + Distributivity of `<#>` and `<+>`:
|||     forall a v w,  a <#> (v <+> w) == (a <#> v) <+> (a <#> w)
|||     forall a b v,  (a <+> b) <#> v == (a <#> v) <+> (b <#> v)
class (RingWithUnity a, AbelianGroup b) => Module a b where
  (<#>) : a -> b -> b

||| A vector space is a module over a ring that is also a field
class (Field a, Module a b) => VectorSpace a b where {}

||| An inner product space is a module – or vector space – over a ring, with a binary function
||| associating a ring value to each pair of vectors.
class Module a b => InnerProductSpace a b where
  (<||>) : b -> b -> a

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant