text:
import Data.Vect

my_length : List a -> Nat
my_length [] = 0
my_length (x :: xs) = 1 + my_length xs

my_reverse : List a -> List a
my_reverse [] = []
my_reverse (x :: xs) = reverse xs ++ [x]

my_map : (a -> b) -> List a -> List b
my_map f [] = []
my_map f (x :: xs) = f x :: map f xs

my_vect_map : (a -> b) -> Vect k a -> Vect k b
my_vect_map f [] = []
my_vect_map f (x :: xs) = f x :: map f xs

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

transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) = let xsTrans = transposeMat xs in
                         zipWith (\x, y => x :: y) x xsTrans

addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (\x, y => x + y) x y :: addMatrix xs ys

multMatrix : Num a => Vect n (Vect m a) ->
                      Vect m (Vect p a) ->
                      Vect n (Vect p a)
multMatrix xs ys = multHelper xs (transposeMat ys)
  where
        dot : Num a => Vect k a -> Vect k a -> a
        dot xs ys = sum $ map (\ (s1, s2) => s1 * s2) (zip xs ys)

        multHelper : Num a => Vect n (Vect m a) ->
                              Vect p (Vect m a) ->
                              Vect n (Vect p a)
        multHelper [] _ = []
        multHelper (x :: xs) ys = map (dot x) ys :: multHelper xs ys


text:
module Commons.Text.Parser.Support

import Text.Lexer
import Text.Parser

%default total
%access public export

Rule : Type -> Type -> Type
Rule tok ty = Grammar (TokenData tok) True ty

RuleEmpty : Type -> Type -> Type
RuleEmpty tok ty = Grammar (TokenData tok) False ty

export
eoi : (isEOI : a -> Bool) -> RuleEmpty a ()
eoi isEOI = do
    nextIs (isEOI . tok)
    pure ()

export
terminalF : String
         -> (TokenData tok -> Maybe a)
         -> Rule tok a
terminalF x f = terminal f <|> fail x

export
help : Rule tok ty
    -> String
    -> Rule tok ty
help p msg = p <|> fail msg

infixl 0 <?>

export
(<?>) : Rule tok ty
     -> String
     -> Rule tok ty
(<?>) p msg = help p msg

export
match : Eq tok
      => String
      -> a
      -> tok
      -> Rule tok a
match msg v exp =
  terminalF msg
            (\x => if (TokenData.tok x) == exp then Just v else Nothing)

ext: idr

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Ex3

import Data.Vect

%default total

myLength : List a -> Nat
myLength [] = 0
myLength (_ :: xs) = 1 + myLength xs

myReverse : List a -> List a
myReverse [] = []
myReverse (x :: xs) = myReverse xs ++ [x]

myMap : (a -> b) -> List a -> List b
myMap _ [] = []
myMap f (x :: xs) = f x :: myMap f xs

myVectMap : (a -> b) -> Vect n a -> Vect n b
myVectMap _ [] = []
myVectMap f (x :: xs) = f x :: myVectMap f xs

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

addMatrix : Num elem => Vect m (Vect n elem) -> Vect m (Vect n elem) -> Vect m (Vect n elem)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (+) x y :: addMatrix xs ys

subMatrix : (Neg elem, Num elem) => Vect m (Vect n elem) -> Vect m (Vect n elem) -> Vect m (Vect n elem)
subMatrix [] [] = []
subMatrix (x :: xs) (y :: ys) = zipWith (-) x y :: subMatrix xs ys

multMatrix : Num elem => { m, n, o : _ } -> Vect m (Vect n elem) -> Vect n (Vect o elem) -> Vect m (Vect o elem)
multMatrix xs ys = let ysTrans = transposeMatrix ys in
                       aux xs ysTrans

  where
    dotProduct : { n : _ } -> Vect n elem -> Vect n elem -> elem
    dotProduct [] [] = 0
    dotProduct (x :: xs) (y :: ys) = x * y + dotProduct xs ys

    aux :  {m, n, o : _} -> Vect m (Vect n elem) -> Vect o (Vect n elem) -> Vect m (Vect o elem)
    aux [] _ = []
    aux (x :: xs) ys = map (\y => dotProduct x y) ys :: aux xs ys

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Store

import Control.App
import Control.App.Console

data Access = LoggedOut | LoggedIn
data Store : Access -> Type where
     MkStore : (secret : String) -> Store a

interface StoreI e where
  connect : App1 e (Store LoggedOut)
  login : (1 d : Store LoggedOut) -> (password : String) ->
          App1 e (Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut)))
  logout : (1 d : Store LoggedIn) -> App1 e (Store LoggedOut)
  readSecret : (1 d : Store LoggedIn) ->
               App1 e (Res String (const (Store LoggedIn)))
  disconnect : (1 d : Store LoggedOut) -> App {l} e ()

Has [Console] e => StoreI e where
  connect
      = do app $ putStrLn "Connect"
           pure1 (MkStore "xyzzy")

  login (MkStore str) pwd
      = if pwd == "Mornington Crescent"
           then pure1 (True # MkStore str)
           else pure1 (False # MkStore str)
  logout (MkStore str) = pure1 (MkStore str)
  readSecret (MkStore str) = pure1 (str # MkStore str)

  disconnect (MkStore _)
      = putStrLn "Door destroyed"

storeProg : Has [Console, StoreI] e =>
            App e ()
storeProg
    = app1 $ do
         s <- connect
         app $ putStr "Password: "
         pwd <- app $ getStr
         True # s <- login s pwd
              | False # s => do app $ putStrLn "Login failed"
                                app $ disconnect s
         app $ putStrLn "Logged in"
         secret # s <- readSecret s
         app $ putStrLn ("Secret: " ++ secret)
         s <- logout s
         app $ putStrLn "Logged out"
         app $ disconnect s

main : IO ()
main = run storeProg


text:
module Replica.Option.Filter

import Data.List
import Data.String

import Replica.Core
import Replica.Option.Types
import Replica.Other.Decorated

%default total

public export
record Filter' (f : Type -> Type) where
  constructor MkFilter
  only : f (List String)
  exclude : f (List String)
  onlyTags : f (List String)
  excludeTags : f (List String)
  lastFailures : f Bool

public export
Filter : Type
Filter = Done Filter'

export
TyMap Filter' where
  tyMap func x = MkFilter
    (func x.only)
    (func x.exclude)
    (func x.onlyTags)
    (func x.excludeTags)
    (func x.lastFailures)

export
TyTraversable Filter' where
  tyTraverse func x = [| MkFilter
    (func x.only)
    (func x.exclude)
    (func x.onlyTags)
    (func x.excludeTags)
    (func x.lastFailures)
    |]

export
Show Filter where
  show x = unwords
    [ "MkFilter"
    , show x.only
    , show x.exclude
    , show x.onlyTags
    , show x.excludeTags
    , show x.lastFailures
    ]

onlyPart : Part (Builder Filter') (List String)
onlyPart = inj $ MkOption
      (singleton $ MkMod (singleton "only") ['n']
          (Right $ MkValue "testX,testY" $ Just . go)
          "a comma separated list of the tests to run")
      [] compose
      where
        go : String -> List String
        go = forget . split (== ',')
        compose : List String -> Builder Filter' -> Either String (Builder Filter')
        compose xs x = case either (const []) (intersect xs) x.exclude of
          [] => Right $ record {only $= Right . (++ xs) . either (const []) id} x
          xs => Left "Some tests were both included and excluded: \{show xs}"

excludePart : Part (Builder Filter') (List String)
excludePart = inj $ MkOption
      (singleton $ MkMod (singleton "exclude") ['N']
          (Right $ MkValue "testX,testY" $ Just . go)
          "a comma separated list of the tests to exclude")
      [] compose
      where
        go : String -> List String
        go = forget . split (== ',')
        compose : List String -> Builder Filter' -> Either String (Builder Filter')
        compose xs x = case either (const []) (intersect xs) x.only of
          [] => Right $ record {exclude $= Right . (++ xs) . either (const []) id} x
          xs => Left "Some tests were both included and excluded: \{show xs}"

onlyTagsPart : Part (Builder Filter') (List String)
onlyTagsPart = inj $ MkOption
      (singleton $ MkMod ("tags" ::: ["only-tags"]) ['t']
          (Right $ MkValue "TAGS" $ Just . go)
          "a comma separated list of the tags to run")
      [] compose
      where
        go : String -> List String
        go = forget . split (== ',')
        compose : List String -> Builder Filter' -> Either String (Builder Filter')
        compose xs x = case either (const []) (intersect xs) x.excludeTags of
          [] => Right $ record {onlyTags $= Right . (++ xs) . either (const []) id} x
          xs => Left "Some tags were both included and excluded: \{show xs}"

excludeTagsPart : Part (Builder Filter') (List String)
excludeTagsPart = inj $ MkOption
      (singleton $ MkMod (singleton "exclude-tags") ['T']
          (Right $ MkValue "TAGS" $ Just . go)
          "a comma separated list of the tags to exclude")
      []
      compose
      where
        go : String -> List String
        go = forget . split (== ',')
        compose : List String -> Builder Filter' -> Either String (Builder Filter')
        compose xs x = case either (const []) (intersect xs) x.onlyTags of
          [] => Right $ record {excludeTags $= Right . (++ xs) . either (const []) id} x
          xs => Left "Some tags were both included and excluded: \{show xs}"

lastFailuresPart : Part (Builder Filter') Bool
lastFailuresPart = inj $ MkOption
      (singleton $ MkMod (singleton "last-fails") ['l']
          (Left True)
          "if a previous run fails, rerun only the tests that failed")
      False
      go
      where
        go : Bool -> Builder Filter' -> Either String (Builder Filter')
        go = ifSame lastFailures
                    (\x => record {lastFailures = Right x})
                    (const $ const "Contradictory values for last failures mode")

export
optParseFilter : OptParse (Builder Filter') (Done Filter')
optParseFilter = [|MkFilter
  (liftAp onlyPart) (liftAp excludePart)
  (liftAp onlyTagsPart) (liftAp excludeTagsPart)
  (liftAp lastFailuresPart) |]

export
defaultFilter : Default Filter'
defaultFilter = MkFilter (defaultPart onlyPart) (defaultPart excludePart)
  (defaultPart onlyTagsPart) (defaultPart excludeTagsPart)
  (defaultPart lastFailuresPart)

export
keepTest : Filter -> Test -> Bool
keepTest x y = (null x.only        || (y.name `elem` x.only))
            && (null x.exclude     || not (y.name `elem` x.exclude))
            && (null x.onlyTags    || not (null $ y.tags `intersect` x.onlyTags))
            && (null x.excludeTags || null (y.tags `intersect` x.excludeTags))

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
||| Environments.
|||
||| Module    : Environment.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
module Toolkit.DeBruijn.Environment

import Decidable.Equality

import Data.DPair

import Toolkit.Decidable.Informative

import Toolkit.Data.List.AtIndex
import Toolkit.Data.DList
import Toolkit.Data.DList.AtIndex

import Toolkit.DeBruijn.Context.Item
import Toolkit.DeBruijn.Context
import Toolkit.DeBruijn.Renaming

%default total

||| Sometimes it is bettern to think that we have this thing called an
||| environment and not a `DList`.
|||
||| @t    The Type for Types in our environment.
||| @obj  How we interpret the types in our DSL. Either this is a
|||       dependent type or a function that computes a type.
||| @ctxt The typing context.
public export
Env : (t : Type) -> (obj : t -> Type) -> (ctxt : List t) -> Type
Env = DList

||| Add an object to our execution environment.
||| @env The typing environment.
export
extend : {t : ty}
      -> (env : Env ty e ctxt)
      -> (obj : e t)
      -> Env ty e (t::ctxt)
extend env obj = obj :: env

namespace Elem
  ||| Read an object from our typing environment.
  |||
  ||| @idx Which object.
  ||| @env The execution environment.
  export
  read : (idx : Elem t ctxt)
      -> (env : Env ty e ctxt)
      -> e t
  read Here      (obj::store) = obj
  read (There x) (obj::store) = read x store

  ||| Add an object to our execution environment.
  |||
  ||| @idx Where the object is.
  ||| @obj The new object.
  ||| @env The environment to which the object is added.
  export
  update : (idx : Elem t ctxt)
        -> (obj : e t)
        -> (env : Env ty e ctxt)
        -> Env ty e ctxt
  update Here      obj (_    :: store) = obj  :: store
  update (There x) obj (obj' :: store) = obj' :: update x obj store

namespace IsVar
  ||| Read an object from our typing environment.
  |||
  ||| @idx Which object.
  ||| @env The execution environment.
  export
  read : (idx : IsVar ctxt t)
      -> (env : Env ty e ctxt)
      -> e t
  read (V 0 Here) (elem :: rest)
    = elem
  read (V (S idx) (There later)) (elem :: rest)
    = read (V idx later) rest

  ||| Add an object to our execution environment.
  |||
  ||| @idx Where the object is.
  ||| @obj The new object.
  ||| @env The environment to which the object is added.
  export
  update : (idx : IsVar ctxt t)
        -> (obj : e t)
        -> (env : Env ty e ctxt)
        -> Env ty e ctxt
  update (V 0 Here) obj (elem :: rest)
    = obj :: rest
  update (V (S k) (There later)) obj (elem :: rest)
    = elem :: update (V k later) obj rest

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module Stuff

import Data.Vect

StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True = Int

data Thing = T1 | T2 | T3

t2nott1 : T2 = T1 -> Void
t2nott1 Refl impossible

t3nott1 : T3 = T1 -> Void
t3nott1 Refl impossible

isThing1 : (t : Thing) -> Dec (t = T1)
isThing1 T1 = Yes Refl
isThing1 T2 = No t2nott1
isThing1 T3 = No t3nott1

is_not_thing1 : (t : Thing) -> Type
is_not_thing1 t with (isThing1 t)
  | Yes _ = Void
  | No  _ = Type

data Atest : (ts : Vect (S n) Thing) -> Type where
  Make : (is_not_thing1 (head ts)) -> (Atest (tail ts)) -> Atest ts

make_atest : (ts : Vect (S n) Thing) -> Atest ts
make_atest ts with (isThing1 (head ts))
  | (Yes prf) = absurd prf
  | (No cont) = Make x xs

print_things : (Atest vs) -> String
print_things (Make x xs) = "did it: "

max_stars_repo_name: wyn/incremental

max_issues_repo_name: wyn/incremental

max_forks_repo_name: wyn/incremental


text:
data Vect : Nat -> Type -> Type where
     Nil  : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

%name Vect xs, ys, zs

{- 1 -}

headUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
           (contra : (x = y) -> Void) -> (x :: xs) = (y :: ys) -> Void
headUnequal contra Refl = contra Refl

tailUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
          (contra : (xs = ys) -> Void) -> (x :: xs) = (y :: ys) -> Void
tailUnequal contra Refl = contra Refl

{- 2 -}

DecEq a => DecEq (Vect n a) where
    decEq [] [] = Yes Refl
    decEq (x :: xs) (y :: ys) = case decEq x y of
                                     No contra => No (headUnequal contra)
                                     Yes Refl => case decEq xs ys of
                                                      Yes Refl => Yes Refl
                                                      No contra => No (tailUnequal contra)


text:
{-
  An embeded DSL for prolog-style logic programming, based on the
  pure-prolog parser and interpreter originally written in Haskell

  Original author: Ken Friis Larsen      <kflarsen@diku.dk>
  Translated into Idris by Nathan Bedell <nbedell@tulane.edu>
-}

import Interp
import Ast
import Data.List

%default partial

public export
p : Term
p = Comp "p" []

public export
q : Term
q = Comp "q" []

public export
x : Term
x = Comp "x" []

public export
z : Term
z = Comp "z" []

public export
r : Term -> Term
r x = Comp "r" [x]

public export
n : Term -> Term
n x = Comp "n" [x]

public export
X : Term
X = Var "X"

public export
s : Term -> Term
s x = Comp "s" [x]

public export
f : Term -> Term -> Term
f x y = Comp "f" [x, y]

public export
%hint
program : Program
program = unDSL
  [ p
    , q :- [p]
    , (n z)
    , (n (s X)) :- [n X]
    , (f z z)
    , (f z (s z))
    , (f X X)
  ]

public export
result : List Solution
result = nub $ bfs $ makeReportTree program [f z X]

-- Note: I should make this more type-safe.
public export
getSolutions : List Solution -> List Term
getSolutions xs = concat $ map getSolution xs
  where getSolution : Solution -> List Term
        getSolution (MkSolution x) = map snd x

public export
f_val : Term -> List Term
f_val x = getSolutions $ nub $ bfs $ makeReportTree program [f x X]

public export
nat : Term -> Bool
nat t = query /= []
  where query : List Solution
        query = ?- n t

-- This is a version of f_val that runs on our embedded prolog
-- system, but only allows values of type Nat.
public export
f_val' : (x : Term) -> {auto p : True = nat x} -> List Term
f_val' x = getSolutions $ ?- f x X

-- An example. The following (should) compile.
-- However, the compiler doesn't like when I try to assert this total. It does strange things.
-- val : List Term
-- val = f_val' z

-- The following does not compile.
-- val' : List Term
-- val' = f_val' (s z)


text:
module Linear.Epsilon

public export
interface Num a => Epsilon a where
  ||| Determine if a quantity is near zero.
  nearZero : a -> Bool

public export
implementation Epsilon Double where
  nearZero a = abs a <= (10 `pow` -12)

max_stars_repo_name: yurrriq/idris-linear

max_issues_repo_name: yurrriq/idris-linear

max_forks_repo_name: yurrriq/idris-linear


text:
module Core.Primitives

import Core.Core
import Core.Context
import Core.TT
import Core.Value
import Utils.String

import Data.Vect

%default covering

public export
record Prim where
  constructor MkPrim
  {arity : Nat}
  fn : PrimFn arity
  type : ClosedTerm
  totality : Totality

binOp : (Constant -> Constant -> Maybe Constant) ->
        {vars : _} -> Vect 2 (NF vars) -> Maybe (NF vars)
binOp fn [NPrimVal fc x, NPrimVal _ y]
    = map (NPrimVal fc) (fn x y)
binOp _ _ = Nothing

unaryOp : (Constant -> Maybe Constant) ->
          {vars : _} -> Vect 1 (NF vars) -> Maybe (NF vars)
unaryOp fn [NPrimVal fc x]
    = map (NPrimVal fc) (fn x)
unaryOp _ _ = Nothing

castString : Vect 1 (NF vars) -> Maybe (NF vars)
castString [NPrimVal fc (I i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (BI i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (B8 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (B16 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (B32 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (B64 i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (Ch i)] = Just (NPrimVal fc (Str (stripQuotes (show i))))
castString [NPrimVal fc (Db i)] = Just (NPrimVal fc (Str (show i)))
castString _ = Nothing

castInteger : Vect 1 (NF vars) -> Maybe (NF vars)
castInteger [NPrimVal fc (I i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (B8 i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (B16 i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (B32 i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (B64 i)] = Just (NPrimVal fc (BI i))
castInteger [NPrimVal fc (Ch i)] = Just (NPrimVal fc (BI (cast (cast {to=Int} i))))
castInteger [NPrimVal fc (Db i)] = Just (NPrimVal fc (BI (cast i)))
castInteger [NPrimVal fc (Str i)] = Just (NPrimVal fc (BI (cast i)))
castInteger _ = Nothing

castInt : Vect 1 (NF vars) -> Maybe (NF vars)
castInt [NPrimVal fc (BI i)] = Just (NPrimVal fc (I (fromInteger i)))
castInt [NPrimVal fc (B8 i)] = Just (NPrimVal fc (I i))
castInt [NPrimVal fc (B16 i)] = Just (NPrimVal fc (I i))
castInt [NPrimVal fc (B32 i)] = Just (NPrimVal fc (I i))
castInt [NPrimVal fc (B64 i)] = Just (NPrimVal fc (I (fromInteger i)))
castInt [NPrimVal fc (Db i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (Ch i)] = Just (NPrimVal fc (I (cast i)))
castInt [NPrimVal fc (Str i)] = Just (NPrimVal fc (I (cast i)))
castInt _ = Nothing

b8max : Int
b8max = 0x100

b16max : Int
b16max = 0x10000

b32max : Int
b32max = 0x100000000

b64max : Integer
b64max = 18446744073709551616 -- 0x10000000000000000

bitCastWrap : (i : Integer) -> (max : Integer) -> Integer
bitCastWrap i max
    = if i >= 0 -- oops, we don't have `rem` yet!
        then i `mod` max
        else max + i `mod` max

constantIntegerValue : Constant -> Maybe Integer
constantIntegerValue (I i)   = Just $ cast i
constantIntegerValue (BI i)  = Just i
constantIntegerValue (B8 i)  = Just $ cast i
constantIntegerValue (B16 i) = Just $ cast i
constantIntegerValue (B32 i) = Just $ cast i
constantIntegerValue (B64 i) = Just i
constantIntegerValue _       = Nothing

castBits8 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits8 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = bitCastWrap value (cast b8max)
    pure (NPrimVal fc (B8 (cast wrapped)))
castBits8 _ = Nothing

castBits16 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits16 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = bitCastWrap value (cast b16max)
    pure (NPrimVal fc (B16 (cast wrapped)))
castBits16 _ = Nothing

castBits32 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits32 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = bitCastWrap value (cast b32max)
    pure (NPrimVal fc (B32 (cast wrapped)))
castBits32 _ = Nothing

castBits64 : Vect 1 (NF vars) -> Maybe (NF vars)
castBits64 [NPrimVal fc constant] = do
    value <- constantIntegerValue constant
    let wrapped = bitCastWrap value b64max
    pure (NPrimVal fc (B64 wrapped))
castBits64 _ = Nothing

castDouble : Vect 1 (NF vars) -> Maybe (NF vars)
castDouble [NPrimVal fc (I i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (BI i)] = Just (NPrimVal fc (Db (cast i)))
castDouble [NPrimVal fc (Str i)] = Just (NPrimVal fc (Db (cast i)))
castDouble _ = Nothing

castChar : Vect 1 (NF vars) -> Maybe (NF vars)
castChar [NPrimVal fc (I i)] = Just (NPrimVal fc (Ch (cast i)))
castChar _ = Nothing

strLength : Vect 1 (NF vars) -> Maybe (NF vars)
strLength [NPrimVal fc (Str s)] = Just (NPrimVal fc (I (cast (length s))))
strLength _ = Nothing

strHead : Vect 1 (NF vars) -> Maybe (NF vars)
strHead [NPrimVal fc (Str "")] = Nothing
strHead [NPrimVal fc (Str str)]
    = Just (NPrimVal fc (Ch (assert_total (prim__strHead str))))
strHead _ = Nothing

strTail : Vect 1 (NF vars) -> Maybe (NF vars)
strTail [NPrimVal fc (Str "")] = Nothing
strTail [NPrimVal fc (Str str)]
    = Just (NPrimVal fc (Str (assert_total (prim__strTail str))))
strTail _ = Nothing

strIndex : Vect 2 (NF vars) -> Maybe (NF vars)
strIndex [NPrimVal fc (Str str), NPrimVal _ (I i)]
    = if i >= 0 && integerToNat (cast i) < length str
         then Just (NPrimVal fc (Ch (assert_total (prim__strIndex str i))))
         else Nothing
strIndex _ = Nothing

strCons : Vect 2 (NF vars) -> Maybe (NF vars)
strCons [NPrimVal fc (Ch x), NPrimVal _ (Str y)]
    = Just (NPrimVal fc (Str (strCons x y)))
strCons _ = Nothing

strAppend : Vect 2 (NF vars) -> Maybe (NF vars)
strAppend [NPrimVal fc (Str x), NPrimVal _ (Str y)]
    = Just (NPrimVal fc (Str (x ++ y)))
strAppend _ = Nothing

strReverse : Vect 1 (NF vars) -> Maybe (NF vars)
strReverse [NPrimVal fc (Str x)]
    = Just (NPrimVal fc (Str (reverse x)))
strReverse _ = Nothing

strSubstr : Vect 3 (NF vars) -> Maybe (NF vars)
strSubstr [NPrimVal fc (I start), NPrimVal _ (I len), NPrimVal _ (Str str)]
    = Just (NPrimVal fc (Str (prim__strSubstr start len str)))
strSubstr _ = Nothing

add : Constant -> Constant -> Maybe Constant
add (BI x) (BI y) = pure $ BI (x + y)
add (I x) (I y) = pure $ I (x + y)
add (B8 x) (B8 y) = pure $ B8 $ (x + y) `mod` b8max
add (B16 x) (B16 y) = pure $ B16 $ (x + y) `mod` b16max
add (B32 x) (B32 y) = pure $ B32 $ (x + y) `mod` b32max
add (B64 x) (B64 y) = pure $ B64 $ (x + y) `mod` b64max
add (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x + cast y))
add (Db x) (Db y) = pure $ Db (x + y)
add _ _ = Nothing

sub : Constant -> Constant -> Maybe Constant
sub (BI x) (BI y) = pure $ BI (x - y)
sub (I x) (I y) = pure $ I (x - y)
sub (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x - cast y))
sub (Db x) (Db y) = pure $ Db (x - y)
sub _ _ = Nothing

mul : Constant -> Constant -> Maybe Constant
mul (BI x) (BI y) = pure $ BI (x * y)
mul (B8 x) (B8 y) = pure $ B8 $ (x * y) `mod` b8max
mul (B16 x) (B16 y) = pure $ B16 $ (x * y) `mod` b16max
mul (B32 x) (B32 y) = pure $ B32 $ (x * y) `mod` b32max
mul (B64 x) (B64 y) = pure $ B64 $ (x * y) `mod` b64max
mul (I x) (I y) = pure $ I (x * y)
mul (Db x) (Db y) = pure $ Db (x * y)
mul _ _ = Nothing

div : Constant -> Constant -> Maybe Constant
div (BI x) (BI 0) = Nothing
div (BI x) (BI y) = pure $ BI (assert_total (x `div` y))
div (I x) (I 0) = Nothing
div (I x) (I y) = pure $ I (assert_total (x `div` y))
div (Db x) (Db y) = pure $ Db (x / y)
div _ _ = Nothing

mod : Constant -> Constant -> Maybe Constant
mod (BI x) (BI 0) = Nothing
mod (BI x) (BI y) = pure $ BI (assert_total (x `mod` y))
mod (I x) (I 0) = Nothing
mod (I x) (I y) = pure $ I (assert_total (x `mod` y))
mod _ _ = Nothing

shiftl : Constant -> Constant -> Maybe Constant
shiftl (I x) (I y) = pure $ I (shiftL x y)
shiftl (BI x) (BI y) = pure $ BI (prim__shl_Integer x y)
shiftl (B8 x) (B8 y) = pure $ B8 $ (prim__shl_Int x y) `mod` b8max
shiftl (B16 x) (B16 y) = pure $ B16 $ (prim__shl_Int x y) `mod` b16max
shiftl (B32 x) (B32 y) = pure $ B32 $ (prim__shl_Int x y) `mod` b32max
shiftl (B64 x) (B64 y) = pure $ B64 $ (prim__shl_Integer x y) `mod` b64max
shiftl _ _ = Nothing

shiftr : Constant -> Constant -> Maybe Constant
shiftr (I x) (I y) = pure $ I (shiftR x y)
shiftr (BI x) (BI y) = pure $ BI (prim__shr_Integer x y)
shiftr (B8 x) (B8 y) = pure $ B8 $ (prim__shr_Int x y)
shiftr (B16 x) (B16 y) = pure $ B16 $ (prim__shr_Int x y)
shiftr (B32 x) (B32 y) = pure $ B32 $ (prim__shr_Int x y)
shiftr (B64 x) (B64 y) = pure $ B64 $ (prim__shr_Integer x y)
shiftr _ _ = Nothing

band : Constant -> Constant -> Maybe Constant
band (I x) (I y) = pure $ I (prim__and_Int x y)
band (BI x) (BI y) = pure $ BI (prim__and_Integer x y)
band (B8 x) (B8 y) = pure $ B8 (prim__and_Int x y)
band (B16 x) (B16 y) = pure $ B16 (prim__and_Int x y)
band (B32 x) (B32 y) = pure $ B32 (prim__and_Int x y)
band (B64 x) (B64 y) = pure $ B64 (prim__and_Integer x y)
band _ _ = Nothing

bor : Constant -> Constant -> Maybe Constant
bor (I x) (I y) = pure $ I (prim__or_Int x y)
bor (BI x) (BI y) = pure $ BI (prim__or_Integer x y)
bor (B8 x) (B8 y) = pure $ B8 (prim__or_Int x y)
bor (B16 x) (B16 y) = pure $ B16 (prim__or_Int x y)
bor (B32 x) (B32 y) = pure $ B32 (prim__or_Int x y)
bor (B64 x) (B64 y) = pure $ B64 (prim__or_Integer x y)
bor _ _ = Nothing

bxor : Constant -> Constant -> Maybe Constant
bxor (I x) (I y) = pure $ I (prim__xor_Int x y)
bxor (B8 x) (B8 y) = pure $ B8 (prim__xor_Int x y)
bxor (B16 x) (B16 y) = pure $ B16 (prim__xor_Int x y)
bxor (B32 x) (B32 y) = pure $ B32 (prim__xor_Int x y)
bxor _ _ = Nothing

neg : Constant -> Maybe Constant
neg (BI x) = pure $ BI (-x)
neg (I x) = pure $ I (-x)
neg (Db x) = pure $ Db (-x)
neg _ = Nothing

toInt : Bool -> Constant
toInt True = I 1
toInt False = I 0

lt : Constant -> Constant -> Maybe Constant
lt (I x) (I y) = pure $ toInt (x < y)
lt (BI x) (BI y) = pure $ toInt (x < y)
lt (B8 x) (B8 y) = pure $ toInt (x < y)
lt (B16 x) (B16 y) = pure $ toInt (x < y)
lt (B32 x) (B32 y) = pure $ toInt (x < y)
lt (B64 x) (B64 y) = pure $ toInt (x < y)
lt (Str x) (Str y) = pure $ toInt (x < y)
lt (Ch x) (Ch y) = pure $ toInt (x < y)
lt (Db x) (Db y) = pure $ toInt (x < y)
lt _ _ = Nothing

lte : Constant -> Constant -> Maybe Constant
lte (I x) (I y) = pure $ toInt (x <= y)
lte (BI x) (BI y) = pure $ toInt (x <= y)
lte (B8 x) (B8 y) = pure $ toInt (x <= y)
lte (B16 x) (B16 y) = pure $ toInt (x <= y)
lte (B32 x) (B32 y) = pure $ toInt (x <= y)
lte (B64 x) (B64 y) = pure $ toInt (x <= y)
lte (Str x) (Str y) = pure $ toInt (x <= y)
lte (Ch x) (Ch y) = pure $ toInt (x <= y)
lte (Db x) (Db y) = pure $ toInt (x <= y)
lte _ _ = Nothing

eq : Constant -> Constant -> Maybe Constant
eq (I x) (I y) = pure $ toInt (x == y)
eq (BI x) (BI y) = pure $ toInt (x == y)
eq (B8 x) (B8 y) = pure $ toInt (x == y)
eq (B16 x) (B16 y) = pure $ toInt (x == y)
eq (B32 x) (B32 y) = pure $ toInt (x == y)
eq (B64 x) (B64 y) = pure $ toInt (x == y)
eq (Str x) (Str y) = pure $ toInt (x == y)
eq (Ch x) (Ch y) = pure $ toInt (x == y)
eq (Db x) (Db y) = pure $ toInt (x == y)
eq _ _ = Nothing

gte : Constant -> Constant -> Maybe Constant
gte (I x) (I y) = pure $ toInt (x >= y)
gte (BI x) (BI y) = pure $ toInt (x >= y)
gte (B8 x) (B8 y) = pure $ toInt (x >= y)
gte (B16 x) (B16 y) = pure $ toInt (x >= y)
gte (B32 x) (B32 y) = pure $ toInt (x >= y)
gte (B64 x) (B64 y) = pure $ toInt (x >= y)
gte (Str x) (Str y) = pure $ toInt (x >= y)
gte (Ch x) (Ch y) = pure $ toInt (x >= y)
gte (Db x) (Db y) = pure $ toInt (x >= y)
gte _ _ = Nothing

gt : Constant -> Constant -> Maybe Constant
gt (I x) (I y) = pure $ toInt (x > y)
gt (BI x) (BI y) = pure $ toInt (x > y)
gt (B8 x) (B8 y) = pure $ toInt (x > y)
gt (B16 x) (B16 y) = pure $ toInt (x > y)
gt (B32 x) (B32 y) = pure $ toInt (x > y)
gt (B64 x) (B64 y) = pure $ toInt (x > y)
gt (Str x) (Str y) = pure $ toInt (x > y)
gt (Ch x) (Ch y) = pure $ toInt (x > y)
gt (Db x) (Db y) = pure $ toInt (x > y)
gt _ _ = Nothing

doubleOp : (Double -> Double) -> Vect 1 (NF vars) -> Maybe (NF vars)
doubleOp f [NPrimVal fc (Db x)] = Just (NPrimVal fc (Db (f x)))
doubleOp f _ = Nothing

doubleExp : Vect 1 (NF vars) -> Maybe (NF vars)
doubleExp = doubleOp exp

doubleLog : Vect 1 (NF vars) -> Maybe (NF vars)
doubleLog = doubleOp log

doubleSin : Vect 1 (NF vars) -> Maybe (NF vars)
doubleSin = doubleOp sin

doubleCos : Vect 1 (NF vars) -> Maybe (NF vars)
doubleCos = doubleOp cos

doubleTan : Vect 1 (NF vars) -> Maybe (NF vars)
doubleTan = doubleOp tan

doubleASin : Vect 1 (NF vars) -> Maybe (NF vars)
doubleASin = doubleOp asin

doubleACos : Vect 1 (NF vars) -> Maybe (NF vars)
doubleACos = doubleOp acos

doubleATan : Vect 1 (NF vars) -> Maybe (NF vars)
doubleATan = doubleOp atan

doubleSqrt : Vect 1 (NF vars) -> Maybe (NF vars)
doubleSqrt = doubleOp sqrt

doubleFloor : Vect 1 (NF vars) -> Maybe (NF vars)
doubleFloor = doubleOp floor

doubleCeiling : Vect 1 (NF vars) -> Maybe (NF vars)
doubleCeiling = doubleOp ceiling

-- Only reduce for concrete values
believeMe : Vect 3 (NF vars) -> Maybe (NF vars)
believeMe [_, _, val@(NDCon _ _ _ _ _)] = Just val
believeMe [_, _, val@(NTCon _ _ _ _ _)] = Just val
believeMe [_, _, val@(NPrimVal _ _)] = Just val
believeMe [_, _, NType fc] = Just (NType fc)
believeMe [_, _, val] = Nothing

constTy : Constant -> Constant -> Constant -> ClosedTerm
constTy a b c
    = let arr = linFnType emptyFC in
    PrimVal emptyFC a `arr` (PrimVal emptyFC b `arr` PrimVal emptyFC c)

constTy3 : Constant -> Constant -> Constant -> Constant -> ClosedTerm
constTy3 a b c d
    = let arr = linFnType emptyFC in
    PrimVal emptyFC a `arr`
         (PrimVal emptyFC b `arr`
             (PrimVal emptyFC c `arr` PrimVal emptyFC d))

predTy : Constant -> Constant -> ClosedTerm
predTy a b = let arr = linFnType emptyFC in
             PrimVal emptyFC a `arr` PrimVal emptyFC b

arithTy : Constant -> ClosedTerm
arithTy t = constTy t t t

cmpTy : Constant -> ClosedTerm
cmpTy t = constTy t t IntType

doubleTy : ClosedTerm
doubleTy = predTy DoubleType DoubleType

believeMeTy : ClosedTerm
believeMeTy
    = Bind emptyFC (UN "a") (Pi emptyFC erased Explicit (TType emptyFC)) $
      Bind emptyFC (UN "b") (Pi emptyFC erased Explicit (TType emptyFC)) $
      Bind emptyFC (UN "x") (Pi emptyFC top Explicit (Local emptyFC Nothing _ (Later First))) $
      Local emptyFC Nothing _ (Later First)

crashTy : ClosedTerm
crashTy
    = Bind emptyFC (UN "a") (Pi emptyFC erased Explicit (TType emptyFC)) $
      Bind emptyFC (UN "msg") (Pi emptyFC top Explicit (PrimVal emptyFC StringType)) $
      Local emptyFC Nothing _ (Later First)

castTo : Constant -> Vect 1 (NF vars) -> Maybe (NF vars)
castTo IntType = castInt
castTo IntegerType = castInteger
castTo Bits8Type = castBits8
castTo Bits16Type = castBits16
castTo Bits32Type = castBits32
castTo Bits64Type = castBits64
castTo StringType = castString
castTo CharType = castChar
castTo DoubleType = castDouble
castTo _ = const Nothing

export
getOp : PrimFn arity ->
        {vars : List Name} -> Vect arity (NF vars) -> Maybe (NF vars)
getOp (Add ty) = binOp add
getOp (Sub ty) = binOp sub
getOp (Mul ty) = binOp mul
getOp (Div ty) = binOp div
getOp (Mod ty) = binOp mod
getOp (Neg ty) = unaryOp neg
getOp (ShiftL ty) = binOp shiftl
getOp (ShiftR ty) = binOp shiftr

getOp (BAnd ty) = binOp band
getOp (BOr ty) = binOp bor
getOp (BXOr ty) = binOp bxor

getOp (LT ty) = binOp lt
getOp (LTE ty) = binOp lte
getOp (EQ ty) = binOp eq
getOp (GTE ty) = binOp gte
getOp (GT ty) = binOp gt

getOp StrLength = strLength
getOp StrHead = strHead
getOp StrTail = strTail
getOp StrIndex = strIndex
getOp StrCons = strCons
getOp StrAppend = strAppend
getOp StrReverse = strReverse
getOp StrSubstr = strSubstr

getOp DoubleExp = doubleExp
getOp DoubleLog = doubleLog
getOp DoubleSin = doubleSin
getOp DoubleCos = doubleCos
getOp DoubleTan = doubleTan
getOp DoubleASin = doubleASin
getOp DoubleACos = doubleACos
getOp DoubleATan = doubleATan
getOp DoubleSqrt = doubleSqrt
getOp DoubleFloor = doubleFloor
getOp DoubleCeiling = doubleCeiling

getOp (Cast _ y) = castTo y
getOp BelieveMe = believeMe

getOp _ = const Nothing

prim : String -> Name
prim str = UN $ "prim__" ++ str

export
opName : PrimFn arity -> Name
opName (Add ty) = prim $ "add_" ++ show ty
opName (Sub ty) = prim $ "sub_" ++ show ty
opName (Mul ty) = prim $ "mul_" ++ show ty
opName (Div ty) = prim $ "div_" ++ show ty
opName (Mod ty) = prim $ "mod_" ++ show ty
opName (Neg ty) = prim $ "negate_" ++ show ty
opName (ShiftL ty) = prim $ "shl_" ++ show ty
opName (ShiftR ty) = prim $ "shr_" ++ show ty
opName (BAnd ty) = prim $ "and_" ++ show ty
opName (BOr ty) = prim $ "or_" ++ show ty
opName (BXOr ty) = prim $ "xor_" ++ show ty
opName (LT ty) = prim $ "lt_" ++ show ty
opName (LTE ty) = prim $ "lte_" ++ show ty
opName (EQ ty) = prim $ "eq_" ++ show ty
opName (GTE ty) = prim $ "gte_" ++ show ty
opName (GT ty) = prim $ "gt_" ++ show ty
opName StrLength = prim "strLength"
opName StrHead = prim "strHead"
opName StrTail = prim "strTail"
opName StrIndex = prim "strIndex"
opName StrCons = prim "strCons"
opName StrAppend = prim "strAppend"
opName StrReverse = prim "strReverse"
opName StrSubstr = prim "strSubstr"
opName DoubleExp = prim "doubleExp"
opName DoubleLog = prim "doubleLog"
opName DoubleSin = prim "doubleSin"
opName DoubleCos = prim "doubleCos"
opName DoubleTan = prim "doubleTan"
opName DoubleASin = prim "doubleASin"
opName DoubleACos = prim "doubleACos"
opName DoubleATan = prim "doubleATan"
opName DoubleSqrt = prim "doubleSqrt"
opName DoubleFloor = prim "doubleFloor"
opName DoubleCeiling = prim "doubleCeiling"
opName (Cast x y) = prim $ "cast_" ++ show x ++ show y
opName BelieveMe = prim $ "believe_me"
opName Crash = prim $ "crash"

export
allPrimitives : List Prim
allPrimitives =
    map (\t => MkPrim (Add t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
    map (\t => MkPrim (Sub t) (arithTy t) isTotal) [IntType, IntegerType, CharType, DoubleType] ++
    map (\t => MkPrim (Mul t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, DoubleType] ++
    map (\t => MkPrim (Div t) (arithTy t) notCovering) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, DoubleType] ++
    map (\t => MkPrim (Mod t) (arithTy t) notCovering) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
    map (\t => MkPrim (Neg t) (predTy t t) isTotal) [IntType, IntegerType, DoubleType] ++
    map (\t => MkPrim (ShiftL t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
    map (\t => MkPrim (ShiftR t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++

    map (\t => MkPrim (BAnd t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
    map (\t => MkPrim (BOr t) (arithTy t) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
    map (\t => MkPrim (BXOr t) (arithTy t) isTotal) [IntType, Bits8Type, Bits16Type, Bits32Type] ++

    map (\t => MkPrim (LT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
    map (\t => MkPrim (LTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
    map (\t => MkPrim (EQ t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
    map (\t => MkPrim (GTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++
    map (\t => MkPrim (GT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType, Bits8Type, Bits16Type, Bits32Type, Bits64Type] ++

    [MkPrim StrLength (predTy StringType IntType) isTotal,
     MkPrim StrHead (predTy StringType CharType) notCovering,
     MkPrim StrTail (predTy StringType StringType) notCovering,
     MkPrim StrIndex (constTy StringType IntType CharType) notCovering,
     MkPrim StrCons (constTy CharType StringType StringType) isTotal,
     MkPrim StrAppend (arithTy StringType) isTotal,
     MkPrim StrReverse (predTy StringType StringType) isTotal,
     MkPrim StrSubstr (constTy3 IntType IntType StringType StringType) isTotal,
     MkPrim BelieveMe believeMeTy isTotal,
     MkPrim Crash crashTy notCovering] ++

    [MkPrim DoubleExp doubleTy isTotal,
     MkPrim DoubleLog doubleTy isTotal,
     MkPrim DoubleSin doubleTy isTotal,
     MkPrim DoubleCos doubleTy isTotal,
     MkPrim DoubleTan doubleTy isTotal,
     MkPrim DoubleASin doubleTy isTotal,
     MkPrim DoubleACos doubleTy isTotal,
     MkPrim DoubleATan doubleTy isTotal,
     MkPrim DoubleSqrt doubleTy isTotal,
     MkPrim DoubleFloor doubleTy isTotal,
     MkPrim DoubleCeiling doubleTy isTotal] ++

    map (\t => MkPrim (Cast t StringType) (predTy t StringType) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
    map (\t => MkPrim (Cast t IntegerType) (predTy t IntegerType) isTotal) [StringType, IntType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
    map (\t => MkPrim (Cast t IntType) (predTy t IntType) isTotal) [StringType, IntegerType, Bits8Type, Bits16Type, Bits32Type, Bits64Type, CharType, DoubleType] ++
    map (\t => MkPrim (Cast t DoubleType) (predTy t DoubleType) isTotal) [StringType, IntType, IntegerType] ++
    map (\t => MkPrim (Cast t CharType) (predTy t CharType) isTotal) [StringType, IntType] ++

    map (\t => MkPrim (Cast t Bits8Type) (predTy t Bits8Type) isTotal) [IntType, IntegerType, Bits16Type, Bits32Type, Bits64Type] ++
    map (\t => MkPrim (Cast t Bits16Type) (predTy t Bits16Type) isTotal) [IntType, IntegerType, Bits8Type, Bits32Type, Bits64Type] ++
    map (\t => MkPrim (Cast t Bits32Type) (predTy t Bits32Type) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits64Type] ++
    map (\t => MkPrim (Cast t Bits64Type) (predTy t Bits64Type) isTotal) [IntType, IntegerType, Bits8Type, Bits16Type, Bits32Type]


text:
> test : String
> test = "LIDR"

ext: lidr


text:
import Data.IOArray

main : IO ()
main
    = do x <- newArray {io = IO, elem = String} 20
         ignore $ writeArray {io = IO} x 10 "Hello"
         ignore $ writeArray {io = IO} x 11 "World"
         printLn !(toList x)

         y <- fromList (map Just [1,2,3,4,5])
         printLn !(toList y)


text:
module Queue

%default total
%access private

public export
interface Queue (q: Type -> Type) where
  empty : q a
  isEmpty : q a -> Bool

  snoc : q a -> a -> q a
  head : q a -> a
  tail : q a -> q a


text:
module Utils.Queue

import Data.Seq.Unsized
import Data.IORef
import Data.List
import System.Concurrency

data QueueEvent a = Msg a | Chan (Channel a)

export
data Queue a = Q Mutex (IORef (Seq (QueueEvent a)))

export
mk_queue : HasIO io => io (Queue a)
mk_queue = liftIO $ pure $ Q !makeMutex !(newIORef empty)

||| receive a message, if empty, block until there is one
export
recv : HasIO io => Queue a -> io a
recv (Q mutex ref) = liftIO $ do
  mutexAcquire mutex
  queue <- readIORef ref
  case viewl queue of
    Just (Msg message, rest) => do
      writeIORef ref rest
      mutexRelease mutex
      pure message
    _ => do
      chan <- makeChannel
      writeIORef ref (snoc queue (Chan chan))
      mutexRelease mutex
      channelGet chan

||| receive a message, if empty, returns nothing
export
recv' : HasIO io => Queue a -> io (Maybe a)
recv' (Q mutex ref) = liftIO $ do
  mutexAcquire mutex
  queue <- readIORef ref
  case viewl queue of
    Just (Msg message, rest) => do
      writeIORef ref rest
      mutexRelease mutex
      pure $ Just message
    _ => do
      mutexRelease mutex
      pure Nothing

||| receive all the messages waiting to be processed
export
recv_all : HasIO io => Queue a -> io (List a)
recv_all (Q mutex ref) = liftIO $ do
  mutexAcquire mutex
  queue <- readIORef ref
  let (msgs, others) = spanBy (\case Msg msg => Just msg; _ => Nothing) (toList queue)
  writeIORef ref (fromList others)
  mutexRelease mutex
  pure msgs

||| send a message to one of the receiver
export
signal : HasIO io => Queue a -> a -> io ()
signal (Q mutex ref) msg = liftIO $ do
  mutexAcquire mutex
  queue <- readIORef ref
  case viewl queue of
    Just (Chan chan, rest) => do
      writeIORef ref rest
      mutexRelease mutex
      channelPut chan msg
    _ => do
      writeIORef ref (snoc queue (Msg msg))
      mutexRelease mutex

||| send a message to all the receivers
export
broadcast : HasIO io => Queue a -> a -> io ()
broadcast (Q mutex ref) msg = liftIO $ do
  mutexAcquire mutex
  queue <- readIORef ref
  writeIORef ref empty
  mutexRelease mutex
  let channels = mapMaybe (\case Chan chan => Just chan; _ => Nothing) (toList queue)
  traverse_ (flip channelPut msg) channels


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

s150 : PrintString m => CanSleep m => (offset : Time) => m String
s150 = do
  printTime offset "s150 proc, first"
  for 5 $ do
    printTime offset "s150 proc, before 1000"
    sleepFor 1.seconds
    printTime offset "s150 proc, before 2000"
    sleepFor 2.seconds
  "long" <$ printTime offset "s150 proc, last"

s55 : PrintString m => CanSleep m => (offset : Time) => m String
s55 = do
  printTime offset "                         s55 proc, first"
  for 5 $ do
    printTime offset "                         s55 proc, before 350"
    sleepFor 350.millis
    printTime offset "                         s55 proc, before 750"
    sleepFor 750.millis
  "short" <$ printTime offset "                         s55 proc, last"

n35 : PrintString m => CanSleep m => (offset : Time) => m Nat
n35 = do
  printTime offset "                                               n35 proc, first"
  for 5 $ do
    printTime offset "                                               n35 proc, before 700"
    sleepFor 700.millis
  35 <$ printTime offset "                                               n35 proc, last"

n77 : PrintString m => CanSleep m => (offset : Time) => m Nat
n77 = do
  printTime offset "                                                                      n77 proc, first"
  for 5 $ do
    printTime offset "                                                                      n77 proc, before 1350"
    sleepFor 1350.millis
  sleepFor 950.millis
  77 <$ printTime offset "                                                                      n77 proc, last"

prn : PrintString m => CanSleep m => (offset : Time) => Nat -> m String
prn n = do
  printTime offset "--- printing sleep, 1.45 sec ---"
  sleepFor 1.seconds
  printTime offset "\{show n}##"
  sleepFor 450.millis
  pure $ "#\{show n}#"

prs : PrintString m => CanSleep m => (offset : Time) => String -> m Nat
prs s = do
  printTime offset "--- printing sleep, 1.45 sec ---"
  sleepFor 1.seconds
  printTime offset "\{show s}$$"
  sleepFor 450.millis
  pure $ length s

export
program : PrintString m => CanSleep m => Alternative m => m Unit
program = do
  printString "\n------\n"

  do
    offset <- currentTime
    printTime offset "start"

    res <- ((n77 <|> n35) >>= prn) <|> (s150 <|> s55)
    printTime offset "top: \{res}"

    printTime offset "end"

  printString "\n------\n"

  do
    offset <- currentTime
    printTime offset "start"

    res <- ((s150 <|> s55) >>= prs) <|> (n77 <|> (n35 *> n35))
    printTime offset "top: \{show res}"

    printTime offset "end"

  printString "\n------"


text:
module Data.Linear.Array

import Data.IOArray

-- Linear arrays. General idea: mutable arrays are constructed linearly,
-- using newArray. Once everything is set up, they can be converted to
-- read only arrays with constant time, pure, access, using toIArray.

-- Immutable arrays which can be read in constant time, but not updated
public export
interface Array arr where
  read : (1 _ : arr t) -> Int -> Maybe t
  size : (1 _ : arr t) -> Int

-- Mutable arrays which can be used linearly
public export
interface Array arr => MArray arr where
  newArray : (size : Int) -> (1 _ : (1 _ : arr t) -> a) -> a
  -- Array is unchanged if the index is out of bounds
  write : (1 _ : arr t) -> Int -> t -> arr t

  mread : (1 _ : arr t) -> Int -> LPair (Maybe t) (arr t)
  msize : (1 _ : arr t) -> LPair Int (arr t)

export
data IArray : Type -> Type where
     MkIArray : IOArray t -> IArray t

export
data LinArray : Type -> Type where
     MkLinArray : IOArray t -> LinArray t

-- Convert a mutable array to an immutable array
export
toIArray : (1 _ : LinArray t) -> (IArray t -> a) -> a
toIArray (MkLinArray arr) k = k (MkIArray arr)

export
Array LinArray where
  read (MkLinArray a) i = unsafePerformIO (readArray a i)
  size (MkLinArray a) = max a

export
MArray LinArray where
  newArray size k = k (MkLinArray (unsafePerformIO (newArray size)))

  write (MkLinArray a) i el
      = unsafePerformIO (do writeArray a i el
                            pure (MkLinArray a))
  msize (MkLinArray a) = max a # MkLinArray a
  mread (MkLinArray a) i
      = unsafePerformIO (readArray a i) # MkLinArray a

export
Array IArray where
  read (MkIArray a) i = unsafePerformIO (readArray a i)
  size (MkIArray a) = max a

export
copyArray : MArray arr => (newsize : Int) -> (1 _ : arr t) -> (arr t, arr t)
copyArray newsize a
    = let size # a = msize a in
          newArray newsize $
            (\a' => copyContent (min (newsize - 1) (size - 1)) a a')
  where
    copyContent : Int -> (1 _ : arr t) -> (1 _ : arr t) -> (arr t, arr t)
    copyContent pos a a'
        = if pos < 0
             then (a, a')
             else let val # a = mread a pos
                      1 a' = case val of
                                  Nothing => a'
                                  Just v => write a' pos v in
                      copyContent (pos - 1) a a'


text:
module Addition.Reduce

import Data.Vect
import Common.Util
import Common.Interfaces
import Specifications.OrderedRing
import Addition.Carry
import Addition.Absorb
import Addition.AbsorptionLemmas
import public Addition.Digit

%default total
%access export

||| Recursively reduce the input digits and absorb the carries.
total
reduce : (Ringops s, Decidable [s,s] leq) =>
  DiscreteOrderedRingSpec (+) Zero Ng (*) leq One ->
  (u : s) ->
  (bound : leq One (u + Ng One)) ->
  (digits : Vect (S k) (Digit leq Ng (u + u))) ->
  Absorption k (Ranges leq Ng u (u + Ng One)) (phi (One + u))
      (map Digit.val digits)
-- Base case. Explicitly pass dictionaries to improve compilation time.
reduce @{ops} spec u bound [MkDigit input inRange] =
  absorptionBase @{ops} spec {u} (One + u)
      (computeCarry @{ops}
        (discreteOrderedGroup spec) u bound input inRange)
-- Recursive case.
reduce @{ops} spec u bound (MkDigit input inRange :: digits@(_::_)) =
  absorptionStep @{ops} spec {u} (One + u)
    (computeCarry @{ops}
       (discreteOrderedGroup spec) u bound input inRange)
    (reduce @{ops} spec u bound digits)

max_stars_repo_name: jeroennoels/verified-exact-real

max_issues_repo_name: jeroennoels/verified-exact-real

max_forks_repo_name: jeroennoels/verified-exact-real


text:
import Data.Fin

data Graph : Nat -> Type where
  Empty : Graph Z
  Node : Bool -> Graph (S Z)
  Combine : (Fin (S n) -> Fin (S m) -> Bool) -> Graph (S n) -> Graph (S m) -> Graph (S n + S m)

combine : {n:Nat} -> {m:Nat} -> (Fin n -> Fin m -> Bool) -> Graph n -> Graph m -> Graph (n+m)
combine {n=n} _ a Empty = rewrite plusZeroRightNeutral n in a
combine {m=m} _ Empty b = b
combine {n=S n} {m=S m} f a b = Combine f a b

f : Bool -> Fin n -> Fin m -> Bool
f a _ _ = a

overlay : Graph n -> Graph m -> Graph (n+m)
overlay a b = combine (f False) a b

connect : Graph n -> Graph m -> Graph (n+m)
connect a b = combine (f True) a b

unconnected : (n : Nat) -> Graph n
unconnected Z = Empty
unconnected (S n) = overlay (Node False) (unconnected n)

clique : (n : Nat) -> Graph n
clique Z = Empty
clique (S n) = connect (Node True) (clique n)


text:
-- Classical logic, PHOAS approach, initial encoding

module Pi.C

%default total

-- Types

data Indiv : Type where
  TODO : Indiv

Ty : Type

Pred : Type
Pred = Indiv -> Ty

infixl 2 :&&
infixl 1 :||
infixr 0 :=>
data Ty : Type where
  UNIT   :             Ty
  (:=>)  : Ty -> Ty -> Ty
  (:&&)  : Ty -> Ty -> Ty
  (:||)  : Ty -> Ty -> Ty
  FALSE  :             Ty
  FORALL : Pred     -> Ty
  EXISTS : Pred     -> Ty

infixr 0 :<=>
(:<=>) : Ty -> Ty -> Ty
(:<=>) a b = (a :=> b) :&& (b :=> a)

NOT : Ty -> Ty
NOT a = a :=> FALSE

TRUE : Ty
TRUE = FALSE :=> FALSE

-- Context and truth judgement

data El : Type where
  mkTrue  : Ty    -> El
  mkIndiv : Indiv -> El

Cx : Type
Cx = El -> Type

isTrue : Ty -> Cx -> Type
isTrue a tc = tc (mkTrue a)

isIndiv : Indiv -> Cx -> Type
isIndiv x tc = tc (mkIndiv x)

-- Terms

infixl 2 :$$
infixl 1 :$

data Tm : Cx -> Ty -> Type where
  var    : isTrue a tc                           -> Tm tc a
  lam'   : (isTrue a tc -> Tm tc b)              -> Tm tc (a :=> b)
  (:$)   : Tm tc (a :=> b)  -> Tm tc a           -> Tm tc b
  pair   : Tm tc a          -> Tm tc b           -> Tm tc (a :&& b)
  fst    : Tm tc (a :&& b)                       -> Tm tc a
  snd    : Tm tc (a :&& b)                       -> Tm tc b
  left   : Tm tc a                               -> Tm tc (a :|| b)
  right  : Tm tc b                               -> Tm tc (a :|| b)
  case'  : Tm tc (a :|| b)  -> (isTrue a tc -> Tm tc c) -> (isTrue b tc -> Tm tc c) -> Tm tc c
  pi'    : ({x : Indiv} -> isIndiv x tc -> Tm tc (p x)) -> Tm tc (FORALL p)
  (:$$)  : Tm tc (FORALL p) -> isIndiv x tc      -> Tm tc (p x)
  sig    : isIndiv x tc     -> Tm tc (p x)       -> Tm tc (EXISTS p)
  split' : Tm tc (EXISTS p) -> (isTrue (p x) tc -> Tm tc a) -> Tm tc a
  abort' : (isTrue (NOT a) tc -> Tm tc FALSE)    -> Tm tc a

lam'' : (Tm tc a -> Tm tc b) -> Tm tc (a :=> b)
lam'' f = lam' $ \x => f (var x)

case'' : Tm tc (a :|| b) -> (Tm tc a -> Tm tc c) -> (Tm tc b -> Tm tc c) -> Tm tc c
case'' xy f g = case' xy (\x => f (var x)) (\y => g (var y))

split'' : Tm tc (EXISTS p) -> (Tm tc (p x) -> Tm tc a) -> Tm tc a
split'' x f = split' x $ \y => f (var y)

abort'' : (Tm tc (NOT a) -> Tm tc FALSE) -> Tm tc a
abort'' f = abort' $ \na => f (var na)

syntax "lam"   {a}  ":=>" [b]           = lam'' (\a => b)
syntax "["     [a]  ","   [b] "]"       = pair a b
syntax "case"  [ab] "of"  {a} ":=>" [c1] or {b} ":=>" [c2] = case'' ab (\a => c1) (\b => c2)
syntax "pi"    {x}  ":=>" [y]           = pi' (\x => y)
syntax "["     [x]  ",,"  [y] "]"       = sig x y
syntax "split" [x]  as    {y} ":=>" [z] = split'' x (\y => z)
syntax "abort" {a}  ":=>" [b]           = abort'' (\a => b)

Thm : Ty -> Type
Thm a = {tc : Cx} -> Tm tc a

-- Example theorems

t214 : Thm (NOT (FORALL (\x => NOT (p x))) :=> EXISTS p)
t214 =
  lam f :=>
    abort g :=>
      f :$ (pi x :=>
            lam p :=> g :$ [ x ,, p ])

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
import Data.Vect

fourInts : Vect 4 Int
fourInts = [0,1,2,3]

||| The sum of both 4D vectors is an 8D vector
eightInts : Vect 8 Int
eightInts = fourInts ++ fourInts

total allLengths : Vect len String -> Vect len Nat
allLengths [] = []
allLengths (word :: words) = length word :: allLengths words

badLengthWithList : List String -> List Nat
badLengthWithList xs = []

badLengthWithVect : Vect n String -> Vect n Nat
badLengthWithVect xs = ?replace_with_empty_list_for_type_checking_error

anotherLengths : Vect length String -> Vect length Nat
anotherLengths [] = ?anotherLengths_rhs_1
anotherLengths (x :: xs) = ?anotherLengths_rhs_2

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
data PowerSource = Petrol | Pedal | Electric

-- 4.2.4 Exercises
-- Extend the Vehicle data type so that it supports unicycles and motorcycles, and wheels and refuel
data Vehicle : PowerSource -> Type where
     Bicycle : Vehicle Pedal
     Unicycle : Vehicle Pedal
     Car : (fuel : Nat) -> Vehicle Petrol
     Bus : (fuel : Nat) -> Vehicle Petrol
     Motorcycle : (fuel : Nat) -> Vehicle Petrol
     Tram : (charge : Nat) -> Vehicle Electric
     ElectricCar : (charge : Nat) -> Vehicle Electric

wheels : Vehicle power -> Nat
wheels Bicycle = 2
wheels Unicycle = 1
wheels (Car fuel) = 4
wheels (Bus fuel) = 4
wheels (Tram charge) = 40
wheels (ElectricCar charge) = 4

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 120

data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
%name Vect xs, ys, zs


text:
module Data.AVL.Core.Quantifiers

import public Data.Tree
import public Data.AVL.Core
import public Data.AVL.Core.API

%default total
%access export

namespace AVL
  namespace Keys

    public export
    data HasKey : (key : typeKey)
               -> (tree : AVLTree h typeKey typeValue)
               -> Type
      where
        IsKey : (prf : IsKeyIn key (Subset.getWitness avl))
             -> HasKey key avl

    keyNotInAVlTree : (contra : IsKeyIn key tree -> Void)
                   -> HasKey key (Element tree prf)
                   -> Void
    keyNotInAVlTree contra (IsKey x) = contra x

    isKey : DecEq typeKey
         => (key : typeKey)
         -> (tree : AVLTree h typeKey typeValue)
         -> Dec (HasKey key tree)
    isKey key (Element tree prf) with (isKey key tree)
      isKey key (Element tree prf) | (Yes x) = Yes (IsKey x)
      isKey key (Element tree prf) | (No contra) = No (keyNotInAVlTree contra)

    public export
    data All : (predicate : typeKey -> Type)
            -> (tree : AVLTree h typeKey typeValue)
            -> Type
      where
        MkProof : (prf : Tree.Keys.All p (Subset.getWitness avl))
               -> All p avl

  namespace Values

    public export
    data HasValue : (value : typeValue)
                 -> (tree : AVLTree h typeKey typeValue)
                 -> Type
      where
        IsValue : (prf : IsValueIn value (Subset.getWitness avl))
               -> HasValue value avl

    valueNotInAVLTree : (contra : IsValueIn value tree -> Void)
                     -> HasValue value (Element tree prf)
                     -> Void
    valueNotInAVLTree contra (IsValue prf) = contra prf

    isValue : DecEq typeValue
           => (value : typeValue)
           -> (tree : AVLTree h typeKey typeValue)
           -> Dec (HasValue value tree)
    isValue value (Element tree prf) with (isValue value tree)
      isValue value (Element tree prf) | (Yes x) = Yes (IsValue x)
      isValue value (Element tree prf) | (No contra) = No (valueNotInAVLTree contra)

    public export
    data All : (predicate : typeValue -> Type)
            -> (tree : AVLTree h typeKey typeValue)
            -> Type
      where
        MkProof : (prf : Tree.Values.All p (Subset.getWitness avl))
               -> AVL.Values.All p avl

  namespace KVPairs

    public export
    data All : (predicate : typeKey -> typeValue -> Type)
            -> (tree : AVLTree k typeKey typeValue)
            -> Type
      where
        MkProof : (prf : Tree.KVPairs.All p (Subset.getWitness avl))
                -> All p avl


text:
import System
import Data.Vect

{- Toy program that outputs the n first digits of Pi.

   Inspired from http://www.haskell.org/haskellwiki/Shootout/Pidigits.
   The original ns and str lazy lists have been replaced by strict functions.

   Memory usage seems to be excessive. One of the branches of str is tail recursive, and
   the other one only needs to cons an extra Integer.

   For reference, the Haskell version runs in 0m0.230s when printing to /dev/null.
   It almost runs in constant space.
-}

data F = MkF Integer Integer Integer

-- Prints the list of digits by groups of 10
loop : Nat -> Nat -> List Integer -> IO ()
loop n k' Nil = putStrLn $ (pack $ Vect.replicate n ' ') ++ "\t:" ++ show k'
loop Z k' xs = do
    putStrLn ("\t:" ++ show k')
    loop 10 k' xs
loop (S k) k' (x::xs) = do
    putStr (show x)
    loop k (S k') xs

fn : Integer -> F
fn k = MkF k (4*k+2) (2*k+1)

flr : Integer -> F -> Integer
flr x (MkF q r t) = (q*x + r) `div` t

comp : F -> F -> F
comp (MkF q r t) (MkF u v x) = MkF (q*u) (q*v + r*x) (t*x)

-- Returns the list of digits of pi. Memory hungry.
str : F -> Integer -> Nat -> List Integer
str _ _ Z = Nil
str z k (S n) =
    if y == flr 4 z
        then y :: str (comp (MkF 10 (-10*y) 1) z    ) k     n
        else      str (comp z                 (fn k)) (k+1) (S n)
    where y = flr 3 z

main : IO ()
main = do
    arg <- getLine
    let n = fromInteger (cast arg)
    let l = str (MkF 1 0 1) 1 n
    loop 10 0 l
    pure ()

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
> module SequentialDecisionProblems.applications.Main

> import Data.Fin
> import Data.List
> import Data.List.Quantifiers
> import Data.So
> import Control.Isomorphism
> import Effects
> import Effect.Exception
> import Effect.StdIO

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.FullTheory
> import SequentialDecisionProblems.Utils
> import SequentialDecisionProblems.FastStochasticDefaults
> import SequentialDecisionProblems.CoreTheoryOptDefaults
> import SequentialDecisionProblems.FullTheoryOptDefaults

> import SequentialDecisionProblems.examples.LeftAheadRight

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.BasicProperties
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.MonadicProperties
> import FastSimpleProb.MeasuresPostulates
> import FastSimpleProb.Measures
> import FastSimpleProb.MeasuresProperties
> import Sigma.Sigma
> import Sigma.Operations
> import Sigma.Properties
> import Nat.LTProperties
> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import NonNegDouble.Predicates
> import NonNegDouble.LTEProperties
> import NonNegDouble.Measures
> import NonNegDouble.MeasureProperties
> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Unique.Predicates
> import Decidable.Predicates
> import LocalEffect.Exception
> import LocalEffect.StdIO
> import Fin.Operations
> import Fraction.Fraction
> import Fraction.Normal
> import Nat.Positive
> import List.Operations
> import Unit.Properties

> -- %default total
> %auto_implicits off

> -- %logging 5

* Introduction

We specify Newcomb's problem as exemplified in [1]:

  "In Newcomb's problem, an agent may choose to take an opaque box or to
  take both the opaque box and a transparent one. The transparent box
  contains 1000 dollars that the agent plainly sees. The opaque box
  contains either nothing or one million dollars, depending on a
  prediction already made. The prediction was about the decision maker's
  choice. If the prediction was that the decision maker will take both
  boxes, then the opaque box is empty. On the other hand, if the
  prediction was that the agent will take just the opaque box, then the
  opaque box contains a million dollars. The prediction is reliable. The
  agent knows all these features of his decision problem."

as a stochastic sequential decision problem. Thus, even though we are
only interested in a single decision step, we have to define states,
controls and the transition and reward functions for an arbitrary number
of steps. We start with controls.

* Controls

At the first decision step, the agent can pick up either the opaque box
or both boxes:

> data Choice = TakeOpaqueBox | TakeBothBoxes

> SequentialDecisionProblems.CoreTheory.Ctrl  Z    _ = Choice

In all subsequent decision steps, the agent has no relevant alternatives

> SequentialDecisionProblems.CoreTheory.Ctrl (S n) _ = Unit

For reasons that will become clear in section "Completing the problem
specification" below, it is useful to show that |Choice| is finite. This
means that there is a one-to-one correspondence between |Choice| and
|Fin 2|:

> to : Choice -> Fin 2
> to TakeOpaqueBox =    FZ
> to TakeBothBoxes = FS FZ

> from : Fin 2 -> Choice
> from             FZ   = TakeOpaqueBox
> from         (FS FZ)  = TakeBothBoxes
> from     (FS (FS  k)) = absurd k

> toFrom : (k : Fin 2) -> to (from k) = k
> toFrom             FZ   = Refl
> toFrom         (FS FZ)  = Refl
> toFrom     (FS (FS  k)) = absurd k

> fromTo : (a : Choice) -> from (to a) = a
> fromTo TakeOpaqueBox  = Refl
> fromTo TakeBothBoxes = Refl

> finiteChoice : Finite Choice
> finiteChoice = MkSigma 2 (MkIso to from toFrom fromTo)

It will also be useful to know that |Choice| is non empty:

> cardNotZChoice : CardNotZ finiteChoice
> cardNotZChoice = cardNotZLemma finiteChoice TakeOpaqueBox

* States

The states that the agent can observe are similarly trivial. At the
first decision step, the agent can see 1000 dollars in the transparent
box but not the content of the opaque box. After the decision has been
made, he can see the content of the opaque box which can be empty of
contain one million dollars:

> data OpaqueBoxContent = Zero | OneMillion

> SequentialDecisionProblems.CoreTheory.State  Z    = Unit
> SequentialDecisionProblems.CoreTheory.State (S n) = OpaqueBoxContent

The agent knows that his choices are predicted reliably. This means
that, if he picks up the opaque box only, there is a high probability
that it contains one million dollars. Similarly, if he chooses both
boxes, the opaque box will likely be empty. Let |p1| be the probability
that the prediction is right and |p2| the probability that it is wrong
with |p1 >> p2|:

> p   :  Double
> p   =  99

> p1  :  NonNegDouble
> p1  =  mkNonNegDouble (p   / (p + 1.0))
> p2  :  NonNegDouble
> p2  =  mkNonNegDouble (1.0 / (p + 1.0))

* Transition function

Selecting the opaque box at decision step zero yields one million
dollars in the opaque box with probability |p1| and zero dollars with
probability |p2| (with |p1 >> p2|):

> SequentialDecisionProblems.CoreTheory.nexts Z () TakeOpaqueBox =
>   MkSimpleProb [(OneMillion, p1), (Zero, p2)] (MkLT Oh)

Conversely, selecting both boxes yields one million dollars in the
opaque box with probability |p2| and zero dollars with probability |p1|:

> SequentialDecisionProblems.CoreTheory.nexts Z () TakeBothBoxes =
>   MkSimpleProb [(OneMillion, p2), (Zero, p1)] (MkLT Oh)

At all subsequent decision steps, nothing interesting happens. There are
no options to decide upon and the transition function simply returns the
current state:

> SequentialDecisionProblems.CoreTheory.nexts (S n) s _ = FastSimpleProb.MonadicOperations.ret s

* |Val| and |LTE|:

> SequentialDecisionProblems.CoreTheory.Val =
>   NonNegDouble.NonNegDouble

> SequentialDecisionProblems.CoreTheory.plus =
>   NonNegDouble.Operations.plus

> SequentialDecisionProblems.CoreTheory.zero =
>   fromInteger @{NumNonNegDouble} 0

> SequentialDecisionProblems.CoreTheory.LTE =
>   NonNegDouble.Predicates.LTE

> SequentialDecisionProblems.FullTheory.reflexiveLTE =
>   NonNegDouble.LTEProperties.reflexiveLTE

> SequentialDecisionProblems.FullTheory.transitiveLTE =
>   NonNegDouble.LTEProperties.transitiveLTE

> SequentialDecisionProblems.FullTheory.monotonePlusLTE =
>   NonNegDouble.LTEProperties.monotonePlusLTE

> SequentialDecisionProblems.CoreTheoryOptDefaults.totalPreorderLTE =
>   NonNegDouble.LTEProperties.totalPreorderLTE

* Reward function

We can now define the reward function for Newcomb's problem. We measure
rewards in units of millions of dollars

> oneMillion : NonNegDouble
> oneMillion = mkNonNegDouble 1.0

> oneThousand : NonNegDouble
> oneThousand = mkNonNegDouble 0.001

>
> using implementation NumNonNegDouble
>
>   SequentialDecisionProblems.CoreTheory.reward Z () TakeOpaqueBox OneMillion = oneMillion
>   SequentialDecisionProblems.CoreTheory.reward Z () TakeOpaqueBox Zero       =       zero
>   SequentialDecisionProblems.CoreTheory.reward Z () TakeBothBoxes OneMillion = oneMillion + oneThousand
>   SequentialDecisionProblems.CoreTheory.reward Z () TakeBothBoxes Zero       =       zero + oneThousand

For all subsequent steps, rewards are simply zero:

>   SequentialDecisionProblems.CoreTheory.reward (S n) _ _ _       = zero

* Completing the problem specification

To be able to apply the verified, generic backwards induction algorithm
of |CoreTheory| to compute optimal policies for Newcomb's problem, we
have to explain how the decision maker accounts for uncertainties on
rewards induced by uncertainties in the transition function. We first
assume that the decision maker measures uncertain rewards by their
average or, in other words, expected value:

> SequentialDecisionProblems.CoreTheory.meas = worst -- expectedValue
> SequentialDecisionProblems.FullTheory.measMon = monotoneWorst -- monotoneExpectedValue

Further on, we have to implement the notions of viability and
reachability. We start by positing that all states are viable for any
number of steps:

> -- Viable : (n : Nat) -> State t -> Type
> SequentialDecisionProblems.CoreTheory.Viable n x = Unit

From this definition, it trivially follows that all elements of an
arbitrary list of states are viable for an arbitrary number of steps:

> viableLemma : {t, n : Nat} -> (xs : List (State t)) -> All (Viable n) xs
> viableLemma  Nil      = Nil
> viableLemma (x :: xs) = () :: (viableLemma xs)

This fact and the (less trivial) result that simple probability
distributions are never empty, see |nonEmptyLemma| in
|MonadicProperties| in |SimpleProb|, allows us to show that the above
definition of |Viable| fulfills |viableSpec1|:

> -- viableSpec1 : (x : State t) -> Viable (S n) x -> GoodCtrl t x
> SequentialDecisionProblems.CoreTheory.viableSpec1 {t = Z} {n} () v =
>   MkSigma TakeOpaqueBox (ne, av) where
>     ne : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts Z () TakeOpaqueBox)
>     ne = nonEmptyLemma (nexts Z () TakeOpaqueBox)
>     av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S Z} n) (nexts Z () TakeOpaqueBox)
>     av = viableLemma {t = S Z} (support (nexts Z () TakeOpaqueBox))
> SequentialDecisionProblems.CoreTheory.viableSpec1 {t = S m} {n} x v =
>   MkSigma () (ne, av) where
>     ne : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts (S m) x ())
>     ne = nonEmptyLemma (nexts (S m) x ())
>     av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S (S m)} n) (nexts (S m) x ())
>     av = viableLemma {t = S (S m)} (support (nexts (S m) x ()))

> SequentialDecisionProblems.Utils.finiteViable n x = finiteUnit

> SequentialDecisionProblems.Utils.decidableViable n x = decidableUnit

For reachability, we proceed in a similar way. We say that all states
are reachable

> -- Reachable : State t' -> Type
> SequentialDecisionProblems.CoreTheory.Reachable x' = Unit

which immediately implies |reachableSpec1|:

> -- reachableSpec1 : (x : State t) -> Reachable {t' = t} x -> (y : Ctrl t x) -> All (Reachable {t' = S t}) (nexts t x y)
> SequentialDecisionProblems.CoreTheory.reachableSpec1 {t} x r y = all (nexts t x y) where
>   all : (sp : SimpleProb  (State (S t))) -> SequentialDecisionProblems.CoreTheory.All (Reachable {t' = S t}) sp
>   all sp = all' (support sp) where
>     all' : (xs : List (State (S t))) -> Data.List.Quantifiers.All (Reachable {t' = S t}) xs
>     all' Nil = Nil
>     all' (x :: xs) = () :: (all' xs)

Finally, we have to show that controls are finite

> -- finiteCtrl : {t : Nat} -> (x : State t) -> Finite (Ctrl t x)
> SequentialDecisionProblems.Utils.finiteCtrl {t = Z}   _ = finiteChoice
> SequentialDecisionProblems.Utils.finiteCtrl {t = S m} _ = finiteUnit

* Optimal policies, optimal decisions, ...

With Necomb's problem fully specified as a SDP, we can apply the results
of our |CoreTheory| and of the |FullTheory| to compute verified optimal
policies, possible state-control sequences, etc.

The interesting question is whether the decision maker will pick up only
the opaque box or both boxes at the first decision step. All following
decisions should be immaterial. Still, we want to assess that we get
consistent results no matter how many decision steps we do. To this end,
we need to be able to show the outcome of the decision process. This
means implemeting functions to print states and controls:

> -- showState : {t : Nat} -> State t -> String
> SequentialDecisionProblems.Utils.showState {t = Z}  ()          = ""
> SequentialDecisionProblems.Utils.showState {t = S n} Zero       = "0"
> SequentialDecisionProblems.Utils.showState {t = S n} OneMillion = "1"

> -- showControl : {t : Nat} -> {x : State t} -> Ctrl t x -> String
> SequentialDecisionProblems.Utils.showCtrl {t = Z}   {x = ()} TakeOpaqueBox = "Take opaque box"
> SequentialDecisionProblems.Utils.showCtrl {t = Z}   {x = ()} TakeBothBoxes = "Take both boxes"
> SequentialDecisionProblems.Utils.showCtrl {t = S n} {x}      ()            = ""

>
> using implementation ShowNonNegDouble
>
>   computation : { [STDIO] } Eff ()
>   computation =
>     do putStr ("enter number of steps:\n")
>        nSteps <- getNat
>        case (decidableViable {t = Z} nSteps ()) of
>          (Yes v) => do putStrLn ("computing optimal policies ...")
>                        ps   <- pure (backwardsInduction Z nSteps)
>                        putStrLn ("computing optimal controls ...")
>                        mxys <- pure (possibleStateCtrlSeqs () () v ps)
>                        putStrLn "possible state-control sequences:"
>                        putStr "  "
>                        putStrLn (show mxys)
>                        mvs <- pure (possibleRewards' mxys)
>                        putStrLn "possible rewards:"
>                        putStr "  "
>                        putStrLn (show mvs)
>                        -- mxyvs <- pure (possibleStateCtrlSeqsRewards' mxys)
>                        -- putStrLn "possible state-control sequences and rewards:"
>                        -- putStr "  "
>                        -- putStrLn (show mxyvs)
>                        -- putStrLn "measure of possible rewards: "
>                        -- putStr "  "
>                        -- putStrLn (show (meas mvs))
>                        -- argmaxmax <- pure (argmaxMax {A = StateCtrlSeq Z nSteps} {B = Val} totalPreorderLTE (support mxyvs) (nonEmptyLemma mxyvs))
>                        -- putStrLn "best possible state-control sequence: "
>                        -- putStr "  "
>                        -- putStrLn (show (fst argmaxmax))
>                        -- putStrLn "best possible reward: "
>                        -- putStr "  "
>                        -- putStrLn (show (snd argmaxmax))
>                        -- -- argminmin <- pure (argminMin totalPreorderLTE (support mxyvs) (nonEmptyLemma mxyvs))
>                        -- -- putStrLn "worst possible state-control sequence: "
>                        -- -- putStr "  "
>                        -- -- putStrLn (show (fst argminmin))
>                        -- -- putStrLn "worst possible reward: "
>                        -- -- putStr "  "
>                        -- -- putStrLn (show (snd argminmin))
>                        putStrLn ("done!")
>          (No _)  => putStrLn ("initial state non viable for " ++ cast {from = Int} (cast nSteps) ++ " steps")

> main : IO ()
> main = run computation

> ---}

[1] Stanford Encyclopedia of Phylosophy, Causal Decision Theory, 2010

-- Local Variables:
-- idris-packages: ("effects")
-- End:

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
-- ---------------------------------------------------------- [ Bottleneck.idr ]
-- Module    : Bottleneck.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Strange bottleneck in printing.
module Bottleneck

import System
import Data.Sigma.DList
import Data.AVL.Dict

-- ---------------------------------------------------- [ Test Data Structures ]
data FTy = A | B | C | D

instance Show FTy where
  show _ = "ABCD"

data Foobar : FTy -> Type where
  Foo : Foobar A
  Bar : Foobar B
  Boo : Foobar C
  Far : Foobar D

instance Show (Foobar ty) where
  show (Foo) = "Foo"
  show (Bar) = "Bar"
  show (Boo) = "Boo"
  show (Far) = "Far"

data FWrap : Type where
  MkWrap : Foobar ty -> FWrap

instance Show FWrap where
  show (MkWrap p) = show p

-- -------------------------------------------------------------------- [ Data ]

repeat : Nat -> (Foobar ty) -> List (Foobar ty)
repeat Z     x = [x]
repeat (S n) x = x :: repeat n x

as : List (Foobar A)
as = repeat 1000 Foo

bs : List (Foobar B)
bs = repeat 1000 Bar

cs : List (Foobar C)
cs = repeat 1000 Boo

ds : (xs ** DList FTy Foobar xs)
ds = (_ ** getProof (fromList as) ++ (getProof (fromList bs)) ++ (getProof (fromList cs)))

-- ------------------------------------------------------- [ Report Generation ]

mkReport : String -> Integer -> Maybe Integer -> Integer -> String
mkReport str a Nothing z =
  unwords [ show a
          , "\t", show z
          , "\t", show (z -a)
          , "\t", "#", str]

mkReport str a (Just s) z =
  unwords [ show a
          , "\t", show s
          , "\t", show z
          , "\t", show (z - a)
          , "\t", show (s - a)
          , "\t", show (z - s)
          , "\t", "#", str]

-- ------------------------------------------------------ [ Testing Framewortk ]
harness : String -> IO (Maybe Integer) -> IO String
harness str test = do
  putStrLn str
  a <- time
  s <- test
  z <- time
  let res = mkReport str a s z
  pure res

-- ---------------------------------------------------------- [ Things to Test ]

namespace DListDict
  addMany : DList FTy Foobar xs -> Dict Nat FWrap -> Dict Nat FWrap
  addMany ds dict = snd $ DList.foldl (\(c,res),d => (S c, insert c (MkWrap d) res)) (Z,dict) ds

namespace DListDictInt
  addMany : DList FTy Foobar xs -> Dict Integer FWrap -> Dict Integer FWrap
  addMany ds dict = snd $ DList.foldl (\(c,res),d => (c+1, insert c (MkWrap d) res)) (0,dict) ds

namespace DListAssocList
  addMany : DList FTy Foobar xs -> List (Nat, FWrap) -> List (Nat, FWrap)
  addMany ds alist = snd $ DList.foldl (\(c,res),d => (S c, (c, (MkWrap d))::res)) (Z,alist) ds

namespace DListAssocListInt
  addMany : DList FTy Foobar xs -> List (Integer, FWrap) -> List (Integer, FWrap)
  addMany ds alist = snd $ DList.foldl (\(c,res),d => (c+1, (c, (MkWrap d))::res)) (0,alist) ds

namespace ListDict
  addMany : List (Foobar ty) -> Dict Nat (Foobar ty) -> Dict Nat (Foobar ty)
  addMany ds dict = snd $ foldr (\d,(c,res)=> (S c, insert c d res)) (Z,dict) ds

namespace ListDictInt
  addMany : List (Foobar ty) -> Dict Integer (Foobar ty) -> Dict Integer (Foobar ty)
  addMany ds dict = snd $ foldr (\d,(c,res)=> (c+1, insert c d res)) (0,dict) ds

namespace ListAssocList
  addMany : List (Foobar ty) -> List (Nat, (Foobar ty)) -> List (Nat, (Foobar ty))
  addMany ds dict = snd $ foldr (\d,(c,res)=> (S c, (c, d)::res)) (Z,dict) ds

namespace ListAssocListInt
  addMany : List (Foobar ty) -> List (Integer, (Foobar ty)) -> List (Integer, (Foobar ty))
  addMany ds dict = snd $ foldr (\d,(c,res)=> (c+1, (c, d)::res)) (0,dict) ds

-- --------------------------------------------------------------- [ The Tests ]

buildAndPrint : IO String
buildAndPrint = do
      r1 <- harness "Dependent List and Dict with Nat" $ do
               let d = DListDict.addMany (Sigma.getProof ds) empty
               s <- time
               printLn d
               pure (Just s)
      r2 <- harness "Dependent List and Dict with Integer" $ do
               let d = DListDictInt.addMany (Sigma.getProof ds) empty
               s <- time
               printLn d
               pure (Just s)
      r3 <- harness "Dependent List and Assoc List with Nat" $ do
               let d = DListAssocList.addMany (Sigma.getProof ds) Nil
               s <- time
               printLn d
               pure (Just s)
      r4 <- harness "Dependent List and Assoc List with Integer" $ do
               let d = DListAssocListInt.addMany (Sigma.getProof ds) Nil
               s <- time
               printLn d
               pure (Just s)
      r5 <- harness "List and Dict with Nat" $ do
               let d = ListDict.addMany (as ++ as ++ as) empty
               s <- time
               printLn d
               pure (Just s)
      r6 <- harness "List and Dict with Int" $ do
               let d = ListDictInt.addMany (as ++ as ++ as) empty
               s <- time
               printLn d
               pure (Just s)
      r7 <- harness "List and AssocList with Nat" $ do
               let d = ListAssocList.addMany (as ++ as ++ as) Nil
               s <- time
               printLn d
               pure (Just s)
      r8 <- harness "List and AssocList with Int" $ do
               let d = ListAssocListInt.addMany (as ++ as ++ as) Nil
               s <- time
               printLn d
               pure (Just s)
      pure $unlines [r1,r2,r3,r4,r5,r6,r7,r8]

justBuild : IO String
justBuild = do
      r1 <- harness "Dependent List and Dict with Nat" $ do
               let d = DListDict.addMany (Sigma.getProof ds) empty
               pure Nothing
      r2 <- harness "Dependent List and Dict with Integer" $ do
               let d = DListDictInt.addMany (Sigma.getProof ds) empty
               s <- time
               pure Nothing
      r3 <- harness "Dependent List and Assoc List with Nat" $ do
               let d = DListAssocList.addMany (Sigma.getProof ds) Nil
               s <- time
               pure Nothing
      r4 <- harness "Dependent List and Assoc List with Integer" $ do
               let d = DListAssocListInt.addMany (Sigma.getProof ds) Nil
               s <- time
               pure Nothing
      r5 <- harness "List and Dict with Nat" $ do
               let d = ListDict.addMany (as ++ as ++ as) empty
               s <- time
               pure Nothing
      r6 <- harness "List and Dict with Int" $ do
               let d = ListDictInt.addMany (as ++ as ++ as) empty
               s <- time
               pure Nothing
      r7 <- harness "List and AssocList with Nat" $ do
               let d = ListAssocList.addMany (as ++ as ++ as) Nil
               s <- time
               pure Nothing
      r8 <- harness "List and AssocList with Int" $ do
               let d = ListAssocListInt.addMany (as ++ as ++ as) Nil
               s <- time
               pure Nothing
      pure $ unlines [r1,r2,r3,r4,r5,r6,r7,r8]

-- --------------------------------------------------------------- [ Execution ]
namespace Main
    main : IO ()
    main = do
      putStrLn "-- ------------------------------------------------------------------------ [  ]"
      report <- buildAndPrint
      putStrLn "Building and Printing"
      putStrLn "Start\tSplit\tStop\tTotal\tBuild\tPrint"
      putStrLn report
      putStrLn "--  ------------------------------------------------------------------------ [  ]"
      report <- justBuild
      putStrLn "Just Building"
      putStrLn $ "Start\tStop\tTotal"
      putStrLn report

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module Idris.SetOptions

import Compiler.Common

import Core.Context
import Core.Directory
import Core.Metadata
import Core.Options
import Core.Unify
import Libraries.Utils.Path
import Libraries.Data.List.Extra

import Idris.CommandLine
import Idris.Package.Types
import Idris.Pretty
import Idris.ProcessIdr
import Idris.REPL
import Idris.Syntax
import Idris.Version

import IdrisPaths

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

import Libraries.Data.List1 as Lib

import System
import System.Directory

%default covering

%hide Libraries.Data.String.Extra.unlines

||| Dissected information about a package directory
record PkgDir where
  constructor MkPkgDir
  ||| Directory name. Example "contrib-0.3.0"
  dirName : String
  ||| Package name. Example "contrib"
  pkgName : String
  ||| Package version. Example `Just $ MkPkgVersion (0 ::: [3,0])`
  version : Maybe PkgVersion

-- dissects a directory name, trying to extract
-- the corresponding package name and -version
pkgDir : String -> PkgDir
pkgDir str =
   -- Split the dir name into parts concatenated by "-"
   -- treating the last part as the version number
   -- and the initial parts as the package name.
   -- For reasons of backwards compatibility, we also
   -- accept hyphenated directory names without a part
   -- corresponding to a version number.
   case Lib.unsnoc $ split (== '-') str of
     (Nil, last) => MkPkgDir str last Nothing
     (init,last) =>
       case toVersion last of
         Just v  => MkPkgDir str (concat $ intersperse "-" init) (Just v)
         Nothing => MkPkgDir str str Nothing
  where
    toVersion : String -> Maybe PkgVersion
    toVersion = map MkPkgVersion
              . traverse parsePositive
              . split (== '.')

dirEntries : String -> IO (List String)
dirEntries dname =
    do Right d <- openDir dname
         | Left err => pure []
       getFiles d []
  where
    getFiles : Directory -> List String -> IO (List String)
    getFiles d acc
        = do Right str <- dirEntry d
               | Left err => pure (reverse acc)
             getFiles d (str :: acc)

getPackageDirs : String -> IO (List PkgDir)
getPackageDirs dname = map pkgDir <$> dirEntries dname

-- Get a list of all the candidate directories that match a package spec
-- in a given path. Return an empty list on file error (e.g. path not existing)
export
candidateDirs : String -> String -> PkgVersionBounds ->
                IO (List (String, Maybe PkgVersion))
candidateDirs dname pkg bounds =
  mapMaybe checkBounds <$> getPackageDirs dname

  where checkBounds : PkgDir -> Maybe (String,Maybe PkgVersion)
        checkBounds (MkPkgDir dirName pkgName ver) =
          do guard (pkgName == pkg && inBounds ver bounds)
             pure ((dname </> dirName), ver)

globalPackageDir : {auto c : Ref Ctxt Defs} -> Core String
globalPackageDir
    = do defs <- get Ctxt
         pure $ prefix_dir (dirs (options defs)) </>
                  "idris2-" ++ showVersion False version

localPackageDir : {auto c : Ref Ctxt Defs} -> Core String
localPackageDir
    = do defs <- get Ctxt
         Just srcdir <- coreLift currentDir
             | Nothing => throw (InternalError "Can't get current directory")
         let depends = depends_dir (dirs (options defs))
         pure $ srcdir </> depends

export
addPkgDir : {auto c : Ref Ctxt Defs} ->
            String -> PkgVersionBounds -> Core ()
addPkgDir p bounds
    = do defs <- get Ctxt
         globaldir <- globalPackageDir
         localdir <- localPackageDir

         -- Get candidate directories from the global install location,
         -- and the local package directory
         locFiles <- coreLift $ candidateDirs localdir p bounds
         globFiles <- coreLift $ candidateDirs globaldir p bounds
         -- Look in all the package paths too
         let pkgdirs = (options defs).dirs.package_dirs
         pkgFiles <- coreLift $ traverse (\d => candidateDirs d p bounds) pkgdirs

         -- If there's anything locally, use that and ignore the global ones
         let allFiles = if isNil locFiles
                           then globFiles ++ concat pkgFiles
                           else locFiles
         -- Sort in reverse order of version number
         let sorted = sortBy (\x, y => compare (snd y) (snd x)) allFiles

         -- From what remains, pick the one with the highest version number.
         -- If there's none, report it
         -- (TODO: Can't do this quite yet due to idris2 build system...)
         case sorted of
              [] => if defs.options.session.ignoreMissingPkg
                       then pure ()
                       else throw (CantFindPackage (p ++ " (" ++ show bounds ++ ")"))
              ((p, _) :: ps) => addExtraDir p

visiblePackages : String -> IO (List PkgDir)
visiblePackages dir = filter viable <$> getPackageDirs dir
  where notHidden : PkgDir -> Bool
        notHidden = not . isPrefixOf "." . pkgName

        notDenylisted : PkgDir -> Bool
        notDenylisted = not . flip elem ["include", "lib", "support", "refc"] . pkgName

        viable : PkgDir -> Bool
        viable p = notHidden p && notDenylisted p

findPackages : {auto c : Ref Ctxt Defs} -> Core (List PkgDir)
findPackages
    = do -- global packages
         defs <- get Ctxt
         globalPkgs <- coreLift $ visiblePackages !globalPackageDir
         -- additional packages in directories specified
         let pkgDirs = (options defs).dirs.package_dirs
         additionalPkgs <- coreLift $ traverse (\d => visiblePackages d) pkgDirs
         -- local packages
         localPkgs <- coreLift $ visiblePackages !localPackageDir
         pure $ globalPkgs ++ (join additionalPkgs) ++ localPkgs

listPackages : {auto c : Ref Ctxt Defs} ->
               {auto o : Ref ROpts REPLOpts} ->
               Core ()
listPackages
    = do pkgs <- sortBy (compare `on` pkgName) <$> findPackages
         traverse_ (iputStrLn . pkgDesc) pkgs
  where
    pkgDesc : PkgDir -> Doc IdrisAnn
    pkgDesc (MkPkgDir _ pkgName version) = pretty pkgName <++> parens (pretty version)

dirOption : {auto c : Ref Ctxt Defs} ->
            {auto o : Ref ROpts REPLOpts} ->
            Dirs -> DirCommand -> Core ()
dirOption dirs LibDir
    = coreLift $ putStrLn
         (prefix_dir dirs </> "idris2-" ++ showVersion False version)
dirOption dirs BlodwenPaths
    = iputStrLn $ pretty (toString dirs)
dirOption dirs Prefix
    = coreLift $ putStrLn yprefix

--------------------------------------------------------------------------------
--          Bash Autocompletions
--------------------------------------------------------------------------------

findIpkg : {auto c : Ref Ctxt Defs} -> Core (List String)
findIpkg =
  do Just srcdir <- coreLift currentDir
       | Nothing => throw (InternalError "Can't get current directory")
     fs <- coreLift $ dirEntries srcdir
     pure $ filter (".ipkg" `isSuffixOf`) fs

-- keep only those Strings, of which `x` is a prefix
prefixOnly : String -> List String -> List String
prefixOnly x = sortedNub . filter (\s => x /= s && isPrefixOf x s)

-- filter a list of Strings by the given prefix, but only if
-- the prefix is not "--", bash complete's constant for empty input.
prefixOnlyIfNonEmpty : String -> List String -> List String
prefixOnlyIfNonEmpty "--" = id
prefixOnlyIfNonEmpty s    = prefixOnly s

-- list of registered codegens
codegens : {auto c : Ref Ctxt Defs} -> Core (List String)
codegens = map fst . availableCGs . options <$> get Ctxt

logLevels : List String
logLevels = map fst knownTopics >>= prefixes . forget . split (== '.')
  where prefixes : List String -> List String
        prefixes [] = []
        prefixes (x :: xs) = x :: map (x ++ "." ++) (prefixes xs)

-- given a pair of strings, the first representing the word
-- actually being edited, the second representing the word
-- before the one being edited, return a list of possible
-- completions. If the list of completions is empty, bash
-- will perform directory completion.
opts : {auto c : Ref Ctxt Defs} -> String -> String -> Core (List String)
opts "--" "idris2"  = pure optionFlags

-- codegens
opts x "--cg"      = prefixOnlyIfNonEmpty x <$> codegens
opts x "--codegen" = prefixOnlyIfNonEmpty x <$> codegens

-- packages
opts x "-p"        = prefixOnlyIfNonEmpty x . (map pkgName) <$> findPackages
opts x "--package" = prefixOnlyIfNonEmpty x . (map pkgName) <$> findPackages

-- logging
opts x "--log"     = pure $ prefixOnlyIfNonEmpty x logLevels

-- with directories
opts "--" "-o"           = pure []
opts "--" "--output"     = pure []
opts "--" "--source-dir" = pure []
opts "--" "--build-dir"  = pure []
opts "--" "--output-dir" = pure []

-- with package files
opts x "--build"     = prefixOnlyIfNonEmpty x <$> findIpkg
opts x "--install"   = prefixOnlyIfNonEmpty x <$> findIpkg
opts x "--mkdoc"     = prefixOnlyIfNonEmpty x <$> findIpkg
opts x "--typecheck" = prefixOnlyIfNonEmpty x <$> findIpkg
opts x "--clean"     = prefixOnlyIfNonEmpty x <$> findIpkg
opts x "--repl"      = prefixOnlyIfNonEmpty x <$> findIpkg

-- options
opts x _ = pure $ if (x `elem` optionFlags)
                     -- `x` is already a known option => perform
                     -- directory completion
                     then Nil
                     else prefixOnly x optionFlags

-- bash autocompletion script using the given function name
completionScript : (fun : String) -> String
completionScript fun =
  let fun' = "_" ++ fun
   in unlines [ fun' ++ "()"
              , "{"
              , "  ED=$([ -z $2 ] && echo \"--\" || echo $2)"
              , "  COMPREPLY=($(idris2 --bash-completion $ED $3))"
              , "}"
              , ""
              , "complete -F " ++ fun' ++ " -o default idris2"
              ]

--------------------------------------------------------------------------------
--          Processing Options
--------------------------------------------------------------------------------

export
setIncrementalCG : {auto c : Ref Ctxt Defs} ->
                   {auto o : Ref ROpts REPLOpts} ->
                   Bool -> String -> Core ()
setIncrementalCG failOnError cgn
    = do defs <- get Ctxt
         case getCG (options defs) cgn of
           Just cg =>
               do Just cgd <- getCG cg
                       | Nothing => pure ()
                  let Just _ = incCompileFile cgd
                       | Nothing =>
                            if failOnError
                               then do coreLift $ putStrLn $ cgn ++ " does not support incremental builds"
                                       coreLift $ exitWith (ExitFailure 1)
                               else pure ()
                  setSession (record { incrementalCGs $= (cg :: )} !getSession)
           Nothing =>
              if failOnError
                 then do coreLift $ putStrLn "No such code generator"
                         coreLift $ putStrLn $ "Code generators available: " ++
                                         showSep ", " (map fst (availableCGs (options defs)))
                         coreLift $ exitWith (ExitFailure 1)
                 else pure ()

-- Options to be processed before type checking. Return whether to continue.
export
preOptions : {auto c : Ref Ctxt Defs} ->
             {auto o : Ref ROpts REPLOpts} ->
             List CLOpt -> Core Bool
preOptions [] = pure True
preOptions (NoBanner :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
-- These things are processed later, but imply nobanner too
preOptions (OutputFile _ :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (ExecFn _ :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (IdeMode :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (IdeModeSocket _ :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (CheckOnly :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (Profile :: opts)
    = do setSession (record { profile = True } !getSession)
         preOptions opts
preOptions (Quiet :: opts)
    = do setOutput (REPL VerbosityLvl.ErrorLvl)
         preOptions opts
preOptions (NoPrelude :: opts)
    = do setSession (record { noprelude = True } !getSession)
         preOptions opts
preOptions (SetCG e :: opts)
    = do defs <- get Ctxt
         case getCG (options defs) e of
            Just cg => do setCG cg
                          preOptions opts
            Nothing =>
              do coreLift $ putStrLn "No such code generator"
                 coreLift $ putStrLn $ "Code generators available: " ++
                                 showSep ", " (map fst (availableCGs (options defs)))
                 coreLift $ exitWith (ExitFailure 1)
preOptions (Directive d :: opts)
    = do setSession (record { directives $= (d::) } !getSession)
         preOptions opts
preOptions (PkgPath p :: opts)
    = do addPkgDir p anyBounds
         preOptions opts
preOptions (SourceDir d :: opts)
    = do setSourceDir (Just d)
         preOptions opts
preOptions (BuildDir d :: opts)
    = do setBuildDir d
         preOptions opts
preOptions (OutputDir d :: opts)
    = do setOutputDir (Just d)
         preOptions opts
preOptions (Directory d :: opts)
    = do defs <- get Ctxt
         dirOption (dirs (options defs)) d
         pure False
preOptions (ListPackages :: opts)
    = do listPackages
         pure False
preOptions (Timing :: opts)
    = do setLogTimings True
         preOptions opts
preOptions (DebugElabCheck :: opts)
    = do setDebugElabCheck True
         preOptions opts
preOptions (AltErrorCount c :: opts)
    = do setSession (record { logErrorCount = c } !getSession)
         preOptions opts
preOptions (RunREPL _ :: opts)
    = do setOutput (REPL VerbosityLvl.ErrorLvl)
         setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (FindIPKG :: opts)
    = do setSession (record { findipkg = True } !getSession)
         preOptions opts
preOptions (IgnoreMissingIPKG :: opts)
    = do setSession (record { ignoreMissingPkg = True } !getSession)
         preOptions opts
preOptions (DumpCases f :: opts)
    = do setSession (record { dumpcases = Just f } !getSession)
         preOptions opts
preOptions (DumpLifted f :: opts)
    = do setSession (record { dumplifted = Just f } !getSession)
         preOptions opts
preOptions (DumpANF f :: opts)
    = do setSession (record { dumpanf = Just f } !getSession)
         preOptions opts
preOptions (DumpVMCode f :: opts)
    = do setSession (record { dumpvmcode = Just f } !getSession)
         preOptions opts
preOptions (Logging n :: opts)
    = do setSession (record { logEnabled = True,
                              logLevel $= insertLogLevel n } !getSession)
         preOptions opts
preOptions (ConsoleWidth n :: opts)
    = do setConsoleWidth n
         preOptions opts
preOptions (Color b :: opts)
    = do setColor b
         preOptions opts
preOptions (WarningsAsErrors :: opts)
    = do updateSession (record { warningsAsErrors = True })
         preOptions opts
preOptions (IgnoreShadowingWarnings :: opts)
    = do updateSession (record { showShadowingWarning = False })
         preOptions opts
preOptions (HashesInsteadOfModTime :: opts)
    = do throw (InternalError "-Xcheck-hashes disabled (see issue #1935)")
         updateSession (record { checkHashesInsteadOfModTime = True })
         preOptions opts
preOptions (CaseTreeHeuristics :: opts)
    = do updateSession (record { caseTreeHeuristics = True })
         preOptions opts
preOptions (IncrementalCG e :: opts)
    = do defs <- get Ctxt
         setIncrementalCG True e
         preOptions opts
preOptions (WholeProgram :: opts)
    = do updateSession (record { wholeProgram = True })
         preOptions opts
preOptions (BashCompletion a b :: _)
    = do os <- opts a b
         coreLift $ putStr $ unlines os
         pure False
preOptions (BashCompletionScript fun :: _)
    = do coreLift $ putStrLn $ completionScript fun
         pure False
preOptions (Total :: opts)
    = do updateSession (record { totalReq = Total })
         preOptions opts
preOptions (_ :: opts) = preOptions opts

-- Options to be processed after type checking. Returns whether execution
-- should continue (i.e., whether to start a REPL)
export
postOptions : {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} ->
              REPLResult -> List CLOpt -> Core Bool
postOptions _ [] = pure True
postOptions res@(ErrorLoadingFile _ _) (OutputFile _ :: rest)
    = do ignore $ postOptions res rest
         pure False
postOptions res (OutputFile outfile :: rest)
    = do ignore $ compileExp (PRef EmptyFC (UN $ Basic "main")) outfile
         ignore $ postOptions res rest
         pure False
postOptions res (ExecFn str :: rest)
    = do ignore $ execExp (PRef EmptyFC (UN $ Basic str))
         ignore $ postOptions res rest
         pure False
postOptions res (CheckOnly :: rest)
    = do ignore $ postOptions res rest
         pure False
postOptions res (RunREPL str :: rest)
    = do replCmd str
         pure False
postOptions res (_ :: rest) = postOptions res rest

export
ideMode : List CLOpt -> Bool
ideMode [] = False
ideMode (IdeMode :: _) = True
ideMode (_ :: xs) = ideMode xs

export
ideModeSocket : List CLOpt -> Bool
ideModeSocket [] = False
ideModeSocket (IdeModeSocket _ :: _) = True
ideModeSocket (_ :: xs) = ideModeSocket xs


text:
module effects

import Data.Vect

import Effects
import Effect.StdIO

vadd : Vect n Int -> Vect n Int -> Vect n Int
vadd [] [] = []
vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys

hello : Eff () [STDIO]
hello = putStrLn "hello, world!"

main : IO ()
main = run hello