text:
-- Page 371

-- Exercise 1 to 4

import Data.Vect

data StackCmd : Type -> Nat -> Nat -> Type where
     Push : Integer -> StackCmd () height (S height)
     Pop : StackCmd Integer (S height) height
     Top : StackCmd Integer (S height) (S height)

     GetStr : StackCmd String height height
     PutStr : String -> StackCmd () height height

     Pure : ty -> StackCmd ty height height
     (>>=) : StackCmd a height1 height2 ->
             (a -> StackCmd b height2 height3) ->
             StackCmd b height1 height3

runStack : (stk : Vect inHeight Integer) ->
           StackCmd ty inHeight outHeight -> IO (ty, Vect outHeight Integer)
runStack stk (Push val) = pure ((), val :: stk)
runStack (val :: stk) Pop = pure (val, stk)
runStack (val :: stk) Top = pure (val, val :: stk)
runStack stk GetStr = do x <- getLine
                         pure (x, stk)
runStack stk (PutStr x) = do putStr x
                             pure ((), stk)
runStack stk (Pure x) = pure (x, stk)
runStack stk (x >>= f) = do (x', newStk) <- runStack stk x
                            runStack newStk (f x')

testAdd : StackCmd () 0 0
testAdd = do Push 10
             x <- GetStr
             Push (cast x)
             val1 <- Pop
             val2 <- Pop
             PutStr (show (val1 + val2) ++ "\n")

data StackIO : Nat -> Type where
     Do : StackCmd a height1 height2 ->
          (a -> Inf (StackIO height2)) -> StackIO height1

namespace StackDo
     (>>=) : StackCmd a height1 height2 ->
             (a -> Inf (StackIO height2)) -> StackIO height1
     (>>=) = Do

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

run : Fuel -> Vect height Integer -> StackIO height -> IO ()
run (More fuel) stk (Do c f)
     = do (res, newStk) <- runStack stk c
          run fuel newStk (f res)
run Dry stk p = pure ()

doAdd : StackCmd () (S (S height)) (S height)
doAdd = do val1 <- Pop
           val2 <- Pop
           Push (val1 + val2)

doSubtract : StackCmd () (S (S height)) (S height)
doSubtract = do val1 <- Pop
                val2 <- Pop
                Push (val1 - val2)

doMultiply : StackCmd () (S (S height)) (S height)
doMultiply = do val1 <- Pop
                val2 <- Pop
                Push (val1 * val2)

doNegate : StackCmd () (S height) (S height)
doNegate = do val1 <- Pop
              Push (-val1)

mutual
  tryAdd : StackIO height
  tryAdd {height = (S (S h))} = do doAdd
                                   result <- Top
                                   PutStr (show result ++ "\n")
                                   stackCalc
  tryAdd = do PutStr "Fewer than two items on the stack\n"
              stackCalc

  trySubtract : StackIO height
  trySubtract {height = (S (S h))} = do doSubtract
                                        result <- Top
                                        PutStr (show result ++ "\n")
                                        stackCalc
  trySubtract = do PutStr "Fewer than two items on the stack\n"
                   stackCalc

  tryMultiply : StackIO height
  tryMultiply {height = (S (S h))} = do doMultiply
                                        result <- Top
                                        PutStr (show result ++ "\n")
                                        stackCalc
  tryMultiply = do PutStr "Fewer than two items on the stack\n"
                   stackCalc

  tryNegate : StackIO height
  tryNegate {height = (S h)} = do doNegate
                                  result <- Top
                                  PutStr (show result ++ "\n")
                                  stackCalc
  tryNegate = do PutStr "Fewer than one item on the stack\n"
                 stackCalc

  tryDiscard : StackIO height
  tryDiscard {height = (S h)} = do result <- Top
                                   PutStr ("Discarded " ++ show result ++ "\n")
                                   stackCalc
  tryDiscard = do PutStr "Fewer than one item on the stack\n"
                  stackCalc

  tryDuplicate : StackIO height
  tryDuplicate {height = (S h)} = do val <- Top
                                     Push val
                                     PutStr ("Duplicated " ++ show val ++ "\n")
                                     stackCalc
  tryDuplicate = do PutStr "Fewer than one item on the stack\n"
                    stackCalc

  data StkInput = Number Integer
                | Add
                | Subtract
                | Multiply
                | Negate
                | Discard
                | Duplicate

  strToInput : String -> Maybe StkInput
  strToInput "" = Nothing
  strToInput "add" = Just Add
  strToInput "subtract" = Just Subtract
  strToInput "multiply" = Just Multiply
  strToInput "negate" = Just Negate
  strToInput "discard" = Just Discard
  strToInput "duplicate" = Just Duplicate
  strToInput x = if all isDigit (unpack x)
                    then Just (Number (cast x))
                    else Nothing

  stackCalc : StackIO height
  stackCalc = do PutStr "> "
                 input <- GetStr
                 case strToInput input of
                      Nothing => do PutStr "Invalid input\n"
                                    stackCalc
                      Just (Number x) => do Push x
                                            stackCalc
                      Just Add => tryAdd
                      Just Subtract => trySubtract
                      Just Multiply => tryMultiply
                      Just Negate => tryNegate
                      Just Discard => tryDiscard
                      Just Duplicate => tryDuplicate

main : IO ()
main = run forever [] stackCalc

-- Page 389

-- Exercise 1
namespace p389_ex1

  data Access = LoggedOut | LoggedIn
  data PwdCheck = Correct | Incorrect

  data ShellCmd : (ty : Type) -> Access -> (ty -> Access) -> Type where
      Password : String -> ShellCmd PwdCheck LoggedOut
          (\check => case check of
                     Correct => LoggedIn
                     Incorrect => LoggedOut)
      Logout : ShellCmd () LoggedIn (const LoggedOut)
      GetSecret : ShellCmd String LoggedIn (const LoggedIn)

      PutStr : String -> ShellCmd () state (const state)
      Pure : (res : ty) -> ShellCmd ty (stateFn res) stateFn
      (>>=) : ShellCmd a state1 state2Fn ->
              ((res : a) -> ShellCmd b (state2Fn res) state3Fn) ->
              ShellCmd b state1 state3Fn

  session : ShellCmd () LoggedOut (const LoggedOut)
  session = do Correct <- Password "wurzel"
               | Incorrect => PutStr "Wrong password"
               msg <- GetSecret
               PutStr ("Secret code: " ++ show msg ++ "\n")
               Logout

-- Exercise 2
-- See `Vending.idr`

max_stars_repo_name: JnxF/advanced-software-analysis

max_issues_repo_name: JnxF/advanced-software-analysis

max_forks_repo_name: JnxF/advanced-software-analysis


text:
module Mrk

import public Mrk.Document
import public Mrk.DSL
import public Mrk.NodeNames
import public Mrk.Attributes

ext: idr

max_stars_repo_name: camelpunch/mrk

max_issues_repo_name: camelpunch/mrk

max_forks_repo_name: camelpunch/mrk


text:
module Core.SchemeEval.ToScheme

import Core.TT
import Libraries.Utils.Scheme

export
Scheme Namespace where
  toScheme x = toScheme (unsafeUnfoldNamespace x)
  fromScheme x = Just $ unsafeFoldNamespace !(fromScheme x)

export
Scheme UserName where
  toScheme (Basic str) = toScheme str
  toScheme (Field str) = Vector 5 [toScheme str]
  toScheme Underscore = Vector 9 []

  fromScheme (Vector 5 [x]) = pure $ Field !(fromScheme x)
  fromScheme (Vector 9 []) = pure Underscore
  fromScheme (StringVal x) = pure (Basic x)
  fromScheme _ = Nothing

export
Scheme Name where
  toScheme (NS x y) = Vector 0 [toScheme x, toScheme y]
  toScheme (UN x) = toScheme x
  toScheme (MN x y) = Vector 2 [toScheme x, toScheme y]
  toScheme (PV x y) = Vector 3 [toScheme x, toScheme y]
  toScheme (DN x y) = Vector 4 [toScheme x, toScheme y]
  toScheme (Nested x y) = Vector 6 [toScheme x, toScheme y]
  toScheme (CaseBlock x y) = Vector 7 [toScheme x, toScheme y]
  toScheme (WithBlock x y) = Vector 8 [toScheme x, toScheme y]
  toScheme (Resolved x) = toScheme x -- we'll see this most often

  fromScheme (Vector 0 [x, y])
      = pure $ NS !(fromScheme x) !(fromScheme y)
  fromScheme (Vector 2 [x, y])
      = pure $ MN !(fromScheme x) !(fromScheme y)
  fromScheme (Vector 3 [x, y])
      = pure $ PV !(fromScheme x) !(fromScheme y)
  fromScheme (Vector 4 [x, y])
      = pure $ DN !(fromScheme x) !(fromScheme y)
  fromScheme (Vector 5 [x, y])
      = pure $ UN (Field !(fromScheme x))
  fromScheme (Vector 6 [x, y])
      = pure $ Nested !(fromScheme x) !(fromScheme y)
  fromScheme (Vector 7 [x, y])
      = pure $ CaseBlock !(fromScheme x) !(fromScheme y)
  fromScheme (Vector 8 [x, y])
      = pure $ WithBlock !(fromScheme x) !(fromScheme y)
  fromScheme (Vector 9 [])
      = pure $ UN Underscore
  fromScheme (IntegerVal x)
      = pure $ Resolved (cast x)
  fromScheme (StringVal x)
      = pure $ UN (Basic x)
  fromScheme _ = Nothing

export
Scheme ModuleIdent where
  toScheme ns = toScheme (miAsNamespace ns)
  fromScheme s = Just $ nsAsModuleIdent !(fromScheme s)

export
Scheme OriginDesc where
  toScheme (PhysicalIdrSrc ident) = Vector 0 [toScheme ident]
  toScheme (PhysicalPkgSrc fname) = Vector 1 [toScheme fname]
  toScheme (Virtual ident) = Null

  fromScheme (Vector 0 [i]) = Just (PhysicalIdrSrc !(fromScheme i))
  fromScheme (Vector 1 [i]) = Just (PhysicalPkgSrc !(fromScheme i))
  fromScheme (Vector _ _) = Nothing
  fromScheme _ = Just (Virtual Interactive)

export
Scheme FC where
  toScheme (MkFC d s e) = Vector 0 [toScheme d, toScheme s, toScheme e]
  toScheme (MkVirtualFC d s e) = Vector 1 [toScheme d, toScheme s, toScheme e]
  toScheme EmptyFC = Null

  fromScheme _ = Just EmptyFC

export
Scheme LazyReason where
  toScheme LInf = IntegerVal 0
  toScheme LLazy = IntegerVal 1
  toScheme LUnknown = IntegerVal 2

  fromScheme (IntegerVal 0) = Just LInf
  fromScheme (IntegerVal 1) = Just LLazy
  fromScheme _ = Just LUnknown

export
Scheme RigCount where
  toScheme x
      = if isErased x then IntegerVal 0
        else if isLinear x then IntegerVal 1
        else IntegerVal 2

  fromScheme (IntegerVal 0) = Just erased
  fromScheme (IntegerVal 1) = Just linear
  fromScheme _ = Just top

export
toSchemePi : PiInfo (SchemeObj Write) -> SchemeObj Write
toSchemePi Implicit = IntegerVal 0
toSchemePi Explicit = IntegerVal 1
toSchemePi AutoImplicit = IntegerVal 2
toSchemePi (DefImplicit s) = Box s


text:
module InfList

public export
data InfList : Type -> Type where
  (::) : (value: elem) -> Inf (InfList elem) -> InfList elem

%name InfList xs, ys, zs

public export
total countFrom : Integer -> InfList Integer
countFrom x = x :: countFrom (x + 1)

public export
total labelFrom : InfList k -> List a -> List (k, a)
labelFrom (key :: xs) []        = []
labelFrom (key :: xs) (y :: ys) = (key, y) :: labelFrom xs ys

public export
total labelWith : Stream labelType -> List a -> List (labelType, a)
labelWith xs [] = []
labelWith (lbl :: lbls) (x :: xs) = (lbl, x) :: labelWith lbls xs

public export
total label : List a -> List (Integer, a)
label = labelWith (iterate (+1) 0)

public export
total getPrefix : (count: Nat) -> InfList ty -> List ty
getPrefix Z     (value :: xs) = []
getPrefix (S k) (value :: xs) = value :: (getPrefix k xs)

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Graphexamples

import Graph
import Data.Vect

Am1 :(Vect 6 (Vect 6  Nat))
Am1 = [[0,1,1,0,0,0],[1,0,1,0,0,0],[1,1,0,0,0,0],[0,0,0,0,1,0],[0,0,0,1,0,1],[0,0,0,0,1,0]]
Am2:(Vect 6 (Vect 6  Nat))
Am2 = [[0,1,1,0,0,0],[1,0,1,1,0,0],[1,1,0,0,0,1],[0,1,0,0,1,0],[0,0,0,1,0,1],[0,0,1,0,1,0]]
Am3:(Vect 6 (Vect 6  Nat))
Am3=[[0,1,1,0,0,0],[1,0,1,1,0,0],[1,1,0,0,0,0],[0,1,0,0,1,0],[0,0,0,1,0,0],[0,0,0,0,0,0]]
Am4 : (Vect 8 (Vect 8  Nat))
Am4 = [[0,1,1,0,0,0,0,0],[1,0,1,0,1,0,0,1],[1,1,0,1,0,0,0,0],[0,0,1,0,1,0,1,0],[0,1,0,1,0,1,1,0],[0,0,0,0,1,0,1,0],[0,0,0,1,1,1,0,0],[0,1,0,0,0,0,0,0]]

ConnectedComponents_of_Am1 : List (List Nat )
ConnectedComponents_of_Am1 = (ConnectedComponents Am1)--[[6,5,4],[3,2,1]]

ConnectedComponents_of_Am3 : List (List Nat )
ConnectedComponents_of_Am3 = ConnectedComponents Am3

Path_Am4_2_7:Maybe  ( List Nat)
Path_Am4_2_7 = (FindPath Am4 2 7 )--Just ([2,1,3,4,7])

Path_Am1_2_5:Maybe  ( List Nat)
Path_Am1_2_5 = (FindPath Am1 2 5 )--Nothing

PathProof_Am4_2_7 :Maybe((List Nat),Path Am4 2 7 )
PathProof_Am4_2_7 = PathWithProof Am4 2 7--Returns Path between 2 and 7 and a proof that it is a path.

PathProof_Am1_2_5 :Maybe((List Nat),Path Am1 2 5 )
PathProof_Am1_2_5 = PathWithProof Am1 2 5


text:
module Test

%access public export

assertEq : Eq a => (given : a) -> (expected : a) -> IO Unit
assertEq g e = if g == e
               then putStrLn "Test Passed"
               else putStrLn "Test Failed"

spec : IO ()
spec = assertEq 1 1

max_stars_repo_name: jappeace/idris-age-of-conquerors

max_issues_repo_name: jappeace/idris-age-of-conquerors

max_forks_repo_name: jappeace/idris-age-of-conquerors


text:
||| Monad morphisms and interaction with monad transformer stacks.
module Data.MSF.Trans

import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer
import Data.MSF.Core
import Data.MSF.Util
import Data.MSF.Running
import Data.SOP

--------------------------------------------------------------------------------
--          General Morphisms
--------------------------------------------------------------------------------

||| The most general structure-preserving monad morphism.
||| This can be used to change the input and output type plus
||| the effect type of an MSF without affecting its internal
||| structure (wiring of stream functions).
|||
||| For examples of usage, have a look at the implementations of
||| functions like `unreader`, `reader`, `unstate`, and similar.
export
morphGS :  Monad m1
        => (forall c . (i1 -> m1(o1,c)) -> i2 -> m2(o2,c))
        -> MSF m1 i1 o1
        -> MSF m2 i2 o2
morphGS f sf = feedback sf (arrM run >>^ \(o2,sf2) => [sf2,o2])
  where run : NP I [MSF m1 i1 o1,i2] -> m2 (o2, MSF m1 i1 o1)
        run [sf1,vi2] = f (step sf1) vi2

||| Applies a monad morphism to change the context of an MSF.
|||
||| ```idris example
||| fromPure : Monad m => MSF Identity i o -> MSF m i o
||| fromPure = morph (pure . runIdentity)
||| ```
export
morph : Monad m1 => (forall c . m1 c -> m2 c) -> MSF m1 i1 o1 -> MSF m2 i1 o1
morph f = morphGS (f .)

--------------------------------------------------------------------------------
--          Identity
--------------------------------------------------------------------------------

||| Puts a pure MSF (over the `Identity` monad) in another
||| monadic context.
export
fromPure : Monad m => MSF Identity i o -> MSF m i o
fromPure = morph (pure . runIdentity)

--------------------------------------------------------------------------------
--          State
--------------------------------------------------------------------------------

||| Alias for `constM get`
export
get : MonadState s m => MSF m i s
get = constM get

||| Alias for `constM put`
export
put : MonadState s m => MSF m s ()
put = arrM put

||| Alias for `constM modify`
export
modify : MonadState s m => MSF m (s -> s) ()
modify = arrM modify

||| Converts an outer `StateT` wrapper to an MSF converting
||| an additional argument of the state type.
export
fromState : Monad m => MSF (StateT s m) i o -> MSF m (NP I [s,i]) (NP I [s,o])
fromState =
  morphGS (\f,[vs,vi] => (\(vs2,vo,vc) => ([vs2,vo],vc)) <$> runStateT vs (f vi))

||| Runs the given stateful MSF as a feedback loop with `ini` as the
||| initial input.
|||
||| This is a shorthand for `feedback ini . fromState`.
export
loopState : Monad m => (ini : s) -> MSF (StateT s m) i o -> MSF m i o
loopState ini = feedback ini . fromState

||| Like `fromState` but drops the uninteresting unit in- and output.
export
fromState_ : Monad m => MSF (StateT s m) () () -> MSF m s s
fromState_ = morphGS (\f,vs => (\(vs2,_,vc) => (vs2,vc)) <$> runStateT vs (f ()))

||| Converts a state transforming MSF to one with its monadic context
||| wrapped in `StateT s`.
export
toState : Monad m => MSF m (NP I [s,i]) (NP I [s,o]) -> MSF (StateT s m) i o
toState =
  morphGS (\f,vi => ST $ \vs => (\([vs2,vo],vc) => (vs2,vo,vc)) <$> f [vs,vi])

||| Like `toState` but for MSFs without additional in- or output
export
toState_ : Monad m => MSF m s s -> MSF (StateT s m) () ()
toState_ = morphGS (\f,_ => ST $ \vs => (\(vs2,vc) => (vs2,(),vc)) <$> f vs)

--------------------------------------------------------------------------------
--          Reader
--------------------------------------------------------------------------------

||| Alias for `constM ask`
export
ask : MonadReader e m => MSF m i e
ask = constM ask

||| Converts an outer `ReaderT` wrapper to an MSF taking an
||| an additional input.
export
fromReader : Monad m => MSF (ReaderT e m) i o -> MSF m (NP I [e,i]) o
fromReader = morphGS (\f,[ve,vi] => runReaderT ve (f vi))

||| Converts the given MSF to use `env` as its environment.
|||
||| This is an alias for `fan [ const env, id ] >>> fromReader sf`.
export
withEnv : Monad m => (env : e) -> (sf : MSF (ReaderT e m) i o) -> MSF m i o
withEnv env sf = fan [ const env, id ] >>> fromReader sf

||| Like `unReader` but drops the uninteresting unit input.
export
fromReader_ : Monad m => MSF (ReaderT e m) () o -> MSF m e o
fromReader_ = morphGS (\f,ve => runReaderT ve (f ()))

||| Converts an MSF taking an additional input
||| to one with its monadic context wrapped in `ReaderT e`.
export
toReader : Monad m => MSF m (NP I [e,i]) o -> MSF (ReaderT e m) i o
toReader = morphGS (\f,vi => MkReaderT $ \ve => f [ve,vi])

||| Like `toReader` but for MSFs without additional input
export
toReader_ : Monad m => MSF m e o -> MSF (ReaderT e m) () o
toReader_ = morphGS (\f,_ => MkReaderT f)

--------------------------------------------------------------------------------
--          Writer
--------------------------------------------------------------------------------

||| Alias for `arrM tell`
export
tell : MonadWriter w m => MSF m w ()
tell = arrM tell

||| Converts an outer `WriterT` wrapper to an MSF producing
||| an additional output.
export
fromWriter : Monoid w => Monad m => MSF (WriterT w m) i o -> MSF m i (NP I [w,o])
fromWriter =
  morphGS (\f,vi => (\((vo,vc),vw) => ([vw,vo],vc)) <$> runWriterT (f vi))

||| Like `fromWriter` but ignores the uninteresting output.
export
fromWriter_ : Monoid w => Monad m => MSF (WriterT w m) i () -> MSF m i w
fromWriter_ =
  morphGS (\f,vi => (\((_,vc),vw) => (vw,vc)) <$> runWriterT (f vi))

||| Converts an MSF producing an additional output
||| to one with its monadic context wrapped in `WriterT w`.
export
toWriter : Monoid w => Monad m => MSF m i (NP I [w,o]) -> MSF (WriterT w m) i o
toWriter =
  morphGS (\f,vi =>
    MkWriterT $ \vw => (\([vw2,vo],vc) => ((vo,vc),vw <+> vw2)) <$> f vi)

||| Like `toWriter` but produces unit as output.
export
toWriter_ : Monoid w => Monad m => MSF m i w -> MSF (WriterT w m) i ()
toWriter_ =
  morphGS (\f,vi =>
    MkWriterT $ \vw => (\(vw2,vc) => (((),vc),vw <+> vw2)) <$> f vi)


text:
module Main
import Data.List

myTriple : Double -> Double
myTriple x = 3 * x

myDoublePow : Double -> Double
myDoublePow x = (pow) x 2

main : IO ()
main = do printLn $ (myDoublePow . myTriple) 5


text:
data Wibble = Wobble

foo : a -> a -> Bool
foo x y = x == y

bar : Wibble -> Wibble -> Bool
bar x y = x == y


text:
||| Convenience module that re-exports everything.
module Data.Functor.Foldable

import public Data.Functor.Foldable.Mod
import public Data.Functor.Foldable.Exotic
import public Data.Functor.Foldable.Instances


text:
injToDec : {0 f : a -> b} -> ({0 x, y : a} -> f x = f y -> x = y) -> Dec (f x = f y) -> Dec (x = y)
injToDec inj $ Yes p = Yes $ inj p
injToDec _   $ No up = No $ up . cong f

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module DNSParser
import IdrisNet.Packet
import IdrisNet.PacketLang
import DNS
import Effects
import Effect.State

DNSReference : Type
DNSReference = Int

public
data DNSParseError = NonexistentRef Int -- Bad reference
                   | BadCode -- Error decoding something from an int to a datatype
                   | InternalError String -- Something else
                   | PayloadUnimplemented

instance Show DNSParseError where
  show (NonexistentRef i) = "Bad reference: " ++ show i
  show BadCode = "Bad code"
  show (InternalError s) = "Internal error: " ++ s
  show PayloadUnimplemented = "Payload unimplemented"

public
record DNSState : Type where
  MkDNSState : (blob : BufPtr) ->
               (labelCache : List (Position, List DomainFragment)) ->
               (pcktLen : Length) ->
               DNSState

public
data DNSParser : Effect where
  Initialise : BufPtr -> Length -> { () ==> DNSState } DNSParser ()
  Finalise : { DNSState ==> () } DNSParser ()
  ParseDNSPacket : (mkTy dns) -> { DNSState ==> () } DNSParser (Either DNSParseError DNSPacket)
  EncodeDNSPacket : DNSPacket -> { DNSState ==> () } DNSParser (mkTy dns)
  UpdateDNSState : DNSState -> { DNSState } DNSParser ()
  GetDNSState : { DNSState } DNSParser DNSState
  UnmarshalReference : DNSReference -> { DNSState } DNSParser (Maybe (List DomainFragment))

public
DNSPARSER : Type -> EFFECT
DNSPARSER t = MkEff t DNSParser

{-
parseDNSPacket : Applicative m =>
                 (mkTy dns) ->
                 { [DNSPARSER DNSState] }
                   Eff m (Either DNSParseError DNSPacket)
-}

packAndMap : Vect n (Bounded 8) -> String
packAndMap xs = pack $ map (chr . val) xs

unmarshalLabel : (mkTy dnsLabel) -> DomainFragment
unmarshalLabel (tagc ## len ## prf ## xs) = packAndMap xs

unmarshalReference' : BufPtr ->
                      Position ->
                      Length ->
                      IO (Maybe (List DomainFragment))
unmarshalReference' pckt pos p_len = with Monad do
  let res = unmarshal' (ActivePacketRes pckt pos p_len) dnsLabels
  case res of
    Just (lbls ## (Left nt), res_len) => do
      let res = map unmarshalLabel lbls
      return $ Just res
    Just (lbls ## (Right (_ ## ref)), res_len) => do
      let res = map unmarshalLabel lbls
      rest <- unmarshalReference' pckt ((val ref) * 8) p_len
      return $ [| (Just res) ++ rest |]
      --return $ Just (pack $ map (chr . val) xs) (doesn't work for some reason)
    Nothing => return Nothing

instance Handler DNSParser IO where
  handle st (UnmarshalReference ref) k = do
    putStrLn $ "Unmarshalling reference: " ++ (show ref)
    res <- unmarshalReference' (blob st) (ref * 8) (pcktLen st)
    k res st
  handle _ (Initialise ptr len) k = k () (MkDNSState ptr [] len)
  handle _ (Finalise) k = k () ()
  handle st (GetDNSState) k = k st st
  handle st (UpdateDNSState st') k = k () st'

private
getDNSState : { [DNSPARSER DNSState] } Eff DNSState
getDNSState = call GetDNSState

private
updateDNSState : DNSState -> { [DNSPARSER DNSState] } Eff ()
updateDNSState st = call $ UpdateDNSState st

private
unmarshalReference : DNSReference ->
                     { [DNSPARSER DNSState] } Eff (Maybe (List DomainFragment))
unmarshalReference ref = UnmarshalReference ref

parseDNSHeader : (mkTy dnsHeader) -> DNSHeader
parseDNSHeader (ident ## qr ## opcode ## aa ## tc ## rd ##
                ra ## z ## z_prf ## ans_auth ## nonauth_accept ## resp) =
  MkDNSHeader (val ident) qr opcode aa tc rd ra ans_auth nonauth_accept resp

decodeReference : DNSReference -> { [DNSPARSER DNSState] }
                  Eff (Either DNSParseError (List DomainFragment))
decodeReference ref = do
  st <- getDNSState
  case lookup ref (labelCache st) of
    Just frags => return $ Right frags
    Nothing => do
      unmarshal_res <- unmarshalReference ref
      return $ maybe (Left $ NonexistentRef ref)
                     (\frags => Right frags) unmarshal_res

decodeLabels : (mkTy dnsLabels) ->
               { [DNSPARSER DNSState] }
                 Eff (Either DNSParseError (List DomainFragment))
decodeLabels (lbls ## (Left null_term)) = return $ Right (map unmarshalLabel lbls)
decodeLabels (lbls ## (Right (_ ## ref))) = do
  let decoded_lbls = map unmarshalLabel lbls
  ref_lbls <- decodeReference (val ref)
  return $ either (\err => Left err)
                  (\r_lbls => Right $ decoded_lbls ++ r_lbls) ref_lbls

decodeDomain : (mkTy dnsDomain) ->
               { [DNSPARSER DNSState] }
                 Eff (Either DNSParseError (List DomainFragment))
decodeDomain (Left (_ ## ref)) = decodeReference (val ref)
decodeDomain (Right encoded_lbls) = decodeLabels encoded_lbls

parseDNSQuestion : (mkTy dnsQuestion) -> { [DNSPARSER DNSState] } Eff (Either DNSParseError DNSQuestion)
parseDNSQuestion (encoded_domain ## qt ## qc) = do
  decoded_domain <- decodeDomain encoded_domain
  case decoded_domain of
    Left err => return $ Left err
    Right decoded_domain' =>
      return $ Right (MkDNSQuestion decoded_domain' qt qc)

decodeIP : (mkTy dnsIP) -> SocketAddress
decodeIP (i1 ## i2 ## i3 ## i4) =
  IPv4Addr (val i1) (val i2) (val i3) (val i4)

decodeNone : (mkTy null) -> ()
decodeNone _ = ()

decodeDomainPayload : (mkTy dnsDomain) ->
                      { [DNSPARSER DNSState] }
                      Eff m (Either DNSParseError (DNSPayload DNSDomain))
decodeDomainPayload dom_pl = do
  domain <- decodeDomain dom_pl
  case domain of
    Left err => return $ Left err
    Right domain' => return $ Right (DNSDomainPayload domain')

getPayloadRel : (pl_ty : DNSPayloadType) ->
              (ty : DNSType) ->
              (cls : DNSClass) ->
              Either DNSParseError (DNSPayloadRel ty cls pl_ty)
getPayloadRel DNSIPv4 DNSTypeA DNSClassIN = Right DNSPayloadRelIP
getPayloadRel DNSIPv6 DNSTypeAAAA DNSClassIN = Right DNSPayloadRelIP6
getPayloadRel DNSDomain DNSTypeCNAME DNSClassIN = Right DNSPayloadRelCNAME
getPayloadRel DNSDomain DNSTypeNS DNSClassIN = Right DNSPayloadRelNS
getPayloadRel DNSSOA DNSTypeSOA DNSClassIN = Right DNSPayloadRelSOA
getPayloadRel _ _ _ = Left PayloadUnimplemented

payloadType : DNSType -> DNSClass -> Either DNSParseError DNSPayloadType
payloadType DNSTypeA DNSClassIN = Right DNSIPv4
payloadType DNSTypeAAAA DNSClassIN = Right DNSIPv6
payloadType DNSTypeNS DNSClassIN =  Right DNSDomain
payloadType DNSTypeCNAME DNSClassIN = Right DNSDomain
payloadType DNSTypeSOA DNSClassIN = Right DNSSOA
payloadType _ _ = Left PayloadUnimplemented

decodeSOAPayload : (mkTy dnsSOA) ->
                   { [DNSPARSER DNSState] }
                    Eff m (Either DNSParseError (DNSPayload DNSSOA))
decodeSOAPayload (mn ## rn ## ser ## ref ## ret ## exp ## min) = do
  mn' <- decodeDomain mn
  rn' <- decodeDomain rn
  case (mn', rn') of
    (Right mn'', Right rn'') =>
      return $ Right (DNSSOAPayload (MkSOA mn'' rn'' (val ser) (val ref)
                        (val ret)  (val exp)  (val min)))
    (Left err, _) => return $ Left err
    (_, Left err) => return $ Left err

total
decodePayload : (pl_rel : DNSPayloadRel ty cl pl_ty) ->
                (mkTy (dnsPayloadLang ty cl)) ->
                { [DNSPARSER DNSState] }
                Eff m (Either DNSParseError (DNSPayload pl_ty))
decodePayload DNSPayloadRelIP ip_pl = return $ Right (DNSIPv4Payload (decodeIP ip_pl))
decodePayload DNSPayloadRelCNAME dom_pl = decodeDomainPayload dom_pl
decodePayload DNSPayloadRelNS dom_pl = decodeDomainPayload dom_pl
decodePayload DNSPayloadRelSOA soa_pl = decodeSOAPayload soa_pl
decodePayload _ _ = return $ Left (PayloadUnimplemented)

-- TODO: Might be nice to prettify this... Pity we're wrapped in Eff so
-- we can't use the Either monad
parseDNSRecord : (mkTy dnsRR) ->
                 { [DNSPARSER DNSState] }
                 Eff m (Either DNSParseError DNSRecord)
parseDNSRecord (encoded_domain ## ty ## cls ## ttl ## len ## payload ## prf) = do
  let ttl' = val ttl
  domain <- (decodeDomain encoded_domain)
  case (payloadType ty cls) of
    Left err => return $ Left err
    Right pl_ty => do
      case (domain, getPayloadRel pl_ty ty cls) of
        (Left err, _) => return $ Left err
        (_, Left err) => return $ Left err
        (Right domain', Right pl_rel) => do
          decoded_pl <- decodePayload pl_rel payload
          case decoded_pl of
            Left err => return $ Left err
            Right decoded_pl' =>
              return $ Right (MkDNSRecord domain' ty cls (val ttl) pl_rel decoded_pl')

-- Ugly hack, since records aren't of the same type and therefore we can't
-- use sequence. Also proves to the TC that the lengths are as stated.
sequenceRecords :
               Vect n (Either DNSParseError DNSRecord) ->
               Vect m (Either DNSParseError DNSRecord) ->
               Vect l (Either DNSParseError DNSRecord) ->
               Either DNSParseError (Vect n DNSRecord, Vect m DNSRecord, Vect l DNSRecord)
sequenceRecords v1 v2 v3 = do
  v1' <- sequence v1
  v2' <- sequence v2
  v3' <- sequence v3
  return (v1', v2', v3')

parseDNSPacket : Applicative m =>
                 (mkTy dns) ->
                 { [DNSPARSER DNSState] }
                   Eff m (Either DNSParseError DNSPacket)
parseDNSPacket (hdr ## qdcount ## ancount ## nscount ##
                arcount ## qs ## as ## auths ## additionals) = with Eff do
  let hdr' = parseDNSHeader hdr
  let n_qdcount = intToNat $ val qdcount
  let n_ancount = intToNat $ val ancount
  let n_nscount = intToNat $ val nscount
  let n_arcount = intToNat $ val arcount
  qs' <- mapVE parseDNSQuestion qs
  -- sequence results in TC not terminating
  -- let qs_ = sequence qs'
  let qs'' = sequence qs'
  as' <- mapVE parseDNSRecord as
  auths' <- mapVE parseDNSRecord auths
  additionals' <- mapVE parseDNSRecord additionals
  let records = sequenceRecords as' auths' additionals'
  -- Now, see if everything was successful!
  case (qs'', records) of
    (Right qs''', Right (as'', auths'', additionals'')) => -- ?mv_rcase
      return $ Right (MkDNS hdr' _ _ _ _
                qs''' as'' auths'' additionals'')
    -- Record parsing may throw an error
    (Left err, _) => return $ Left err
    (_, Left err) => return $ Left err
    -- Nothing = bad code
    _ => return $ Left BadCode

--encodeDNSPacket : DNSPacket -> { [DNSPARSER DNSState] } Eff m (mkTy dns)
--encodeDNSPacket dnspckt = ?encodeDNSPacket_rhs

initialise : BufPtr -> Length -> { [DNSPARSER ()] ==> [DNSPARSER DNSState] } Eff ()
initialise ptr len = call $ Initialise ptr len

finalise : { [DNSPARSER DNSState] ==> [DNSPARSER ()] } Eff ()
finalise = call $ Finalise

public
parseDNS : BufPtr -> Length -> (mkTy dns) ->
           { [DNSPARSER ()] } Eff (Either DNSParseError DNSPacket)
parseDNS ptr len pckt = with Eff do
  initialise ptr len
  res <- parseDNSPacket pckt
  finalise
  return res

public
data DNSEncodeError = OutOfBoundsError Nat Nat
                    | ProofConstructionError String
                    | LengthMismatchError Nat Nat
                    | UnsupportedPayloadType
                    | InternalEncodeError String

instance Show DNSEncodeError where
  show (OutOfBoundsError n1 n2) = "Out of bounds: " ++ (show n1) ++ ", " ++ (show n2)
  show (ProofConstructionError s) = "Proof construction error: " ++ s
  show (LengthMismatchError n1 n2) = "Length mismatch: " ++ (show n1) ++ ", " ++ (show n2)
  show UnsupportedPayloadType = "Unsupported payload type"
  show (InternalEncodeError s) = "Internal error: " ++ s

-- Our old friend... Might be a better way of doing this
lemma_vect_len : {x : Nat} -> (y : Nat) -> Vect x a -> Either DNSEncodeError (Vect y a)
lemma_vect_len {x} y xs with (decEq x y)
  lemma_vect_len {x} x xs | (Yes refl) = Right xs
  lemma_vect_len {x} y _  | (No _) = Left $ LengthMismatchError x y

---encodeVectLen : (n : Nat) -> Bounded

lemma_vect : (y : Bounded m) -> (xs : Vect n a) -> Either DNSEncodeError (Vect (intToNat (val y)) a )
lemma_vect b xs = lemma_vect_len (intToNat (val b)) xs

isBounded : (bound : Nat) -> Nat -> Either DNSEncodeError (Bounded bound)
isBounded b n =
  case choose (i_n < (pow 2 b)) of
      Left yes => Right (BInt i_n yes)
      Right _ => Left $ OutOfBoundsError b n
  where i_n : Int
        i_n = natToInt n

zeroBit : Bounded 1
zeroBit = BInt 0 oh

oneBit : Bounded 1
oneBit = BInt 1 oh

charToBits8 : Char -> Bounded 8
charToBits8 c = BInt (ord c) (believe_me oh) -- Premise

encodeString : String -> (n ** (Vect n (Bounded 8)))
encodeString str =
  let unpacked_string = map charToBits8 (unpack str) in
  let vect_string = fromList unpacked_string in
  (_ ** vect_string)

mkTagCheck0 : (mkTy (tagCheck 0))
mkTagCheck0 = let zbit = zeroBit in
              (zbit ## zbit ## refl ## refl)

mkTagCheck1 : (mkTy (tagCheck 1))
mkTagCheck1 = let onebit = oneBit in
              (onebit ## onebit ## refl ## refl)

nullT : (mkTy nullterm)
nullT = (b0 ## oh)
  where b0 : Bounded 8
        b0 = BInt 0 oh

encodeDomainFragment : DomainFragment -> Either DNSEncodeError (mkTy dnsLabel)
encodeDomainFragment frag = with Monad do
  let (len ** vect_string) = encodeString frag
  encoded_len <- isBounded 6 len
  case choose ((val encoded_len) /= 0) of
    Left prf =>
      (lemma_vect encoded_len vect_string) >>= \encoded_string' =>
        Right (mkTagCheck0 ## encoded_len ## prf ## encoded_string')
    Right _ => Left $ ProofConstructionError "Length of encoded domain fragment may not be zero"

encodeDomain : List DomainFragment -> Either DNSEncodeError (mkTy dnsDomain)
encodeDomain xs = with Monad do
  xs <- sequence $ map encodeDomainFragment xs
  return (Right (xs ## (Left nullT)))

encodeQuestion : DNSQuestion -> Either DNSEncodeError (mkTy dnsQuestion)
encodeQuestion (MkDNSQuestion qnames ty cls) = with Monad do
  dom <- encodeDomain qnames
  return (dom ## ty ## cls)

encodeHeader : DNSHeader -> Either DNSEncodeError (mkTy dnsHeader)
encodeHeader (MkDNSHeader hdr_id query op auth trunc rd ra aa naa resp) = with Monad do
  b_id <- isBounded 16 (intToNat hdr_id)
  Right (b_id ## query ## op ## auth ## trunc ## rd ##
        ra ## False ## oh ## aa ## naa ## resp)

encodeIP : DNSPayload DNSIPv4 -> Either DNSEncodeError (mkTy dnsIP)
encodeIP (DNSIPv4Payload (IPv4Addr i1 i2 i3 i4)) = with Monad do
  i1' <- isBounded 8 (intToNat i1)
  i2' <- isBounded 8 (intToNat i2)
  i3' <- isBounded 8 (intToNat i3)
  i4' <- isBounded 8 (intToNat i4)
  return (i1' ## i2' ## i3' ## i4')
-- TODO: If we parameterised SocketAddress over its type, we wouldn't have to do this.
encodeIP _ = Left $ InternalEncodeError "Attempted to encode ipv6 address using ipv4 function"

encodeSOA : DNSSoA -> Either DNSEncodeError (mkTy dnsSOA)
encodeSOA soa = do
  mname <- encodeDomain (dnsSOAMName soa)
  rname <- encodeDomain (dnsSOARName soa)
  serial <- isBounded 32 (intToNat $ dnsSOASerial soa)
  refresh <- isBounded 32 (intToNat $ dnsSOASerial soa)
  retry <- isBounded 32 (intToNat $ dnsSOASerial soa)
  expire <- isBounded 32 (intToNat $ dnsSOASerial soa)
  minimum <- isBounded 32 (intToNat $ dnsSOASerial soa)
  return $ (mname ## rname ## serial ## refresh ## retry ## expire ## minimum)

encodePayload : (rel : DNSPayloadRel ty cls pl_ty) ->
                (payload : DNSPayload pl_ty) ->
                Either DNSEncodeError (mkTy (dnsPayloadLang ty cls))
--encodePayload {ty_code} {cls_code} rel ty_rel cls_rel = ?mv
encodePayload DNSPayloadRelIP payload = encodeIP payload
encodePayload DNSPayloadRelIP6 payload = Left UnsupportedPayloadType
encodePayload DNSPayloadRelCNAME (DNSDomainPayload payload) = encodeDomain payload
encodePayload DNSPayloadRelNS (DNSDomainPayload payload) = encodeDomain payload
encodePayload DNSPayloadRelSOA (DNSSOAPayload payload) = encodeSOA payload
encodePayload _ _ = Left UnsupportedPayloadType

{-
payloadLength : (rel : DNSPayloadRel ty cls pl_ty) ->
                (payload : (mkTy (dnsPayloadLang ty cls))) ->
                Either DNSEncodeError Int
payloadLength DNSPayloadRelIP pl = Right $ bitLength _ pl

payloadLength DNSPayloadRelIP6 pl = Left UnsupportedPayloadType
payloadLength DNSPayloadRelCNAME pl = encodeDomain payload
payloadLength DNSPayloadRelNS pl = encodeDomain payload
payloadLength _ _ = Left UnsupportedPayloadType
-}
%assert_total
encodeRR : DNSRecord -> Either DNSEncodeError (mkTy dnsRR)
encodeRR (MkDNSRecord name ty cls ttl rel pl) = with Monad do
  dom <- encodeDomain name
  b_ttl <- isBounded 32 (intToNat ttl)
  encoded_pl <- encodePayload rel pl
  let pl_len = (bitLength (dnsPayloadLang ty cls) encoded_pl) `div` 8
  b_len <- isBounded 16 (intToNat pl_len)
  case decEq (val b_len) (bitLength (dnsPayloadLang ty cls) encoded_pl `div` 8) of
    Yes p =>
      Right (dom ## ty ## cls ## b_ttl ## b_len ## encoded_pl ## p)
    No _ => Left $ ProofConstructionError "Length field not equal to payload length"

public
encodeDNS : DNSPacket -> Either DNSEncodeError (mkTy dns) -- Maybe (mkTy dns)
encodeDNS (MkDNS hdr qc ac nsc arc qs as auths ars) = with Monad do
    encoded_hdr <- encodeHeader hdr
    b_qc <- isBounded 16 qc
    b_ac <- isBounded 16 ac
    b_nsc <- isBounded 16 nsc
    b_arc <- isBounded 16 arc
    qs' <- sequence $ map encodeQuestion qs
    as' <- sequence $ map encodeRR as
    auths' <- sequence $ map encodeRR auths
    ars' <- sequence $ map encodeRR ars
    qs'' <- lemma_vect b_qc qs'
    as'' <- lemma_vect b_ac as'
    auths'' <- lemma_vect b_nsc auths'
    ars'' <- lemma_vect b_arc ars'
    return (encoded_hdr ## b_qc ## b_ac ## b_nsc ## b_arc ## qs'' ## as'' ## auths'' ## ars'')

-- Simple wrapper function to allow us to create a DNS request
public
mkDNSRequest : Int ->
               List DomainFragment ->
               DNSQType ->
               DNSQClass ->
               DNSPacket
mkDNSRequest req_id dom_frags qt qc = MkDNS hdr 1 0 0 0 [q] [] [] []
  where hdr = (MkDNSHeader req_id False QUERY False False
              True True False False DNSResponseNoError)
        q = (MkDNSQuestion dom_frags qt qc)
-- runInit [(MkDNSState ptr [] len)] (parseDNSPacket pckt)


text:
square_root_approx : (number : Double) -> (approx : Double) -> Stream Double
square_root_approx number approx =
  let next = (approx + (number / approx)) / 2
  in approx :: Delay (square_root_approx number next)

square_root_bound : (max : Nat) -> (number : Double) -> (bound : Double) ->
                    (approxs : Stream Double) -> Double
square_root_bound Z number bound (approx :: approxs) = approx
square_root_bound (S k) number bound (approx :: approxs)
  = if (within_bound number bound approx)
    then approx
    else square_root_bound k number bound approxs
  where
    within_bound : (number : Double) -> (bound : Double) -> (approx : Double) -> Bool
    within_bound number bound approx = abs((approx * approx) - number) < bound

square_root : (number : Double) -> Double
square_root number = square_root_bound 100 number 0.0000000001
                                       (square_root_approx number number)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Data.Time.LocalTime.TimeZone

import Text.Format.Decimal

import Generics.Derive

%default total
%language ElabReflection

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

public export
record TimeZone where
  constructor MkTimeZone
  ||| The minutes offset from UTC. positive means local time will be later in the day than UTC.
  minutes : Int

  ||| Is this timezone just persisting for the summer?
  summeronly : Bool
  name : String
%runElab derive "TimeZone" [Generic, Eq, Ord, DecEq]

public export
record TimeZoneFormat where
  constructor MkTimeZoneFormat
  width : Maybe Nat
  sep : Maybe Char
  pad : Maybe Char

export defaultTimeZoneFormat : TimeZoneFormat
defaultTimeZoneFormat = MkTimeZoneFormat Nothing Nothing Nothing

export timeZoneOffsetString' : TimeZoneFormat -> TimeZone -> String
timeZoneOffsetString' fmt tz = let
  h = tz.minutes `div` 60
  m = tz.minutes `mod` 60
  in case fmt.sep of
          Nothing => format' (record { width = fmt.width, pad = fmt.pad }) $ h * 100 + m
          Just c  => format' (record { width = map (\w => max 0 (w `minus` 3)) fmt.width,
                                       pad = fmt.pad }) h
                     ++ format' (record { width = Just 2, pad = Just '0' }) m

export timeZoneOffsetString : TimeZone -> String
timeZoneOffsetString x = timeZoneOffsetString' defaultTimeZoneFormat x

||| This only shows the time zone name, or offset if the name is empty.
public export
Show TimeZone where
  show x = if x.name == "" then timeZoneOffsetString x else x.name

||| Create a nameless non-summer timezone for this number of minutes.
export minutesToTimeZone : Int -> TimeZone
minutesToTimeZone m = MkTimeZone m False ""

||| Create a nameless non-summer timezone for this number of hours.
export hoursToTimeZone : Int -> TimeZone
hoursToTimeZone i = minutesToTimeZone (60 * i)

||| The UTC time zone.
export utc : TimeZone
utc = MkTimeZone 0 False "UTC"

{-

toCTime :: Int64 -> IO CTime
toCTime t = let
    tt = fromIntegral t
    t' = fromIntegral tt
    -- there's no instance Bounded CTime, so this is the easiest way to check for overflow
    in if t' == t
           then return $ CTime tt
           else fail "Data.Time.LocalTime.Internal.TimeZone.toCTime: Overflow"

-- | Get the local time-zone for a given time (varying as per summertime adjustments).
getTimeZoneSystem :: SystemTime -> IO TimeZone
getTimeZoneSystem t = do
    ctime <- toCTime $ systemSeconds t
    getTimeZoneCTime ctime

-- | Get the local time-zone for a given time (varying as per summertime adjustments).
getTimeZone :: UTCTime -> IO TimeZone
getTimeZone t = do
    ctime <- toCTime $ floor $ utcTimeToPOSIXSeconds t
    getTimeZoneCTime ctime
-}

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


text:
module CatenableDeque

import public Deque

%default total
%access private

public export
interface Deque d => CatenableDeque (d : Type -> Type) where
  (++) : d a -> d a -> d a


text:
module Compiler.Jvm.ShowUtil

import Core.CompileExpr
import Core.Context
import Core.Name
import Core.TT
import Data.Vect
import Data.List

quoted : String -> String
quoted str = "\"" ++ str ++ "\""

showObj : List (String, String) -> String
showObj props = "{" ++ concat (intersperse ", " $ go <$> props) ++ "}" where
    go : (String, String) -> String
    go (k, v) = "\"" ++ k ++ "\" : " ++ v

export
showType : String -> List (String, String) -> String
showType typeName properties = showObj (("__name", quoted typeName) :: properties)

indent : Nat -> String -> String
indent n s = concat (List.replicate (n * 4) " ") ++ s

showConstant : Constant -> String
showConstant (I value)   = "prim$I$" ++ show value
showConstant (BI value)  = "prim$BI$" ++ show value
showConstant (Ch value)  = "prim$Ch$" ++ show value
showConstant (Str value) = "prim$Str$" ++ show value
showConstant (I8 value)  = "prim$I8$" ++ show value
showConstant (I16 value) = "prim$I16$" ++ show value
showConstant (I32 value) = "prim$I32$" ++ show value
showConstant (I64 value) = "prim$I64$" ++ show value
showConstant (B8 value)  = "prim$B8$" ++ show value
showConstant (B16 value) = "prim$B16$" ++ show value
showConstant (B32 value) = "prim$B32$" ++ show value
showConstant (B64 value) = "prim$B64$" ++ show value
showConstant (Db value)  = "prim$Db$" ++ show value
showConstant value       = "prim$" ++ show value

mutual
    export
    showNamedCExp : Nat -> NamedCExp -> String
    showNamedCExp n (NmLocal fc x) = show x
    showNamedCExp n (NmRef fc x) = show x
    showNamedCExp n (NmLam fc x y) = "\\" ++ show x ++ " -> " ++ showNamedCExp n y
    showNamedCExp n (NmLet fc x y z) = "\n" ++ indent n ("let " ++ show x ++ " = \n") ++
        showNamedCExp (n + 1) y ++ "\n" ++ indent n "in\n" ++ indent n (showNamedCExp (n + 1) z)
    showNamedCExp n (NmApp fc (NmRef _ name) xs) = show name ++ "(" ++
        (showSep ", " $ showNamedCExp n <$> xs) ++ ")"
    showNamedCExp n (NmApp fc x xs) = showNamedCExp n x ++ "<$>(" ++
        (showSep ", " $ showNamedCExp n <$> xs) ++ ")"
    showNamedCExp n (NmCon fc x _ tag xs) = "new " ++ show x ++ "(" ++ show tag ++
        ", " ++ (showSep "," $ showNamedCExp n <$> xs) ++ ")"
    showNamedCExp n (NmOp fc op xs) = show op ++ "(" ++
        (showSep "," $ showNamedCExp n <$> toList xs) ++ ")"
    showNamedCExp n (NmExtPrim fc p xs) = "extprim$" ++ show p ++ "(" ++
        (showSep "," $ showNamedCExp n <$> xs) ++ ")"
    showNamedCExp n (NmForce _ _ x) = "force" ++ "(" ++ showNamedCExp n x ++ ")"
    showNamedCExp n (NmDelay _ _ x) = "delay" ++ "(" ++ showNamedCExp n x ++ ")"
    showNamedCExp n (NmConCase fc sc xs def) = "\n" ++
        indent n ("constructorswitch" ++ "(" ++ showNamedCExp n sc ++ ")\n") ++
            showSep "\n" (showNamedConAlt (n + 1) <$> xs) ++
                maybe "" (\defExp => "\n" ++ indent (n + 1) "default:\n" ++
                    indent (n + 1) (showNamedCExp (n + 1) defExp)) def
    showNamedCExp n (NmConstCase fc sc xs def) = "\n" ++
        indent n ("constantswitch" ++"(" ++ showNamedCExp n sc ++ ")\n") ++
            showSep "\n" (showNamedConstAlt (n + 1) <$> xs) ++
                maybe "" (\defExp => "\n" ++ indent (n + 1) "default:\n" ++
                    indent (n + 1) (showNamedCExp (n + 2) defExp)) def
    showNamedCExp n (NmPrimVal fc x) = showConstant x
    showNamedCExp n (NmErased fc) = "erased"
    showNamedCExp n (NmCrash fc x) = "crash " ++ show x

    export
    showNamedConAlt : Nat -> NamedConAlt -> String
    showNamedConAlt n (MkNConAlt x conInfo tag args exp) = indent n ("case " ++ show x ++ show conInfo ++
      "(" ++ show tag ++ "): \n") ++ indent (n + 1) ("bind " ++ show args ++ ";\n") ++
      (indent (n + 1) $ showNamedCExp (n + 1) exp)

    export
    showNamedConstAlt : Nat -> NamedConstAlt -> String
    showNamedConstAlt n (MkNConstAlt x exp) = indent n ("case " ++ showConstant x ++ ":\n") ++
        indent (n + 1) (showNamedCExp (n + 1) exp)


text:
module Compiler.CompileExpr

import Compiler.Opts.CSE
import Core.CaseTree
import public Core.CompileExpr
import Core.Context
import Core.Env
import Core.Name
import Core.Normalise
import Core.Options
import Core.TT
import Core.Value

import Data.List
import Data.Maybe
import Libraries.Data.NameMap
import Data.Vect

%default covering

data Args
    = NewTypeBy Nat Nat
    | EraseArgs Nat (List Nat)
    | Arity Nat

||| Extract the number of arguments from a term, or return that it's
||| a newtype by a given argument position
numArgs : Defs -> Term vars -> Core Args
numArgs defs (Ref _ (TyCon tag arity) n) = pure (Arity arity)
numArgs defs (Ref _ _ n)
    = do Just gdef <- lookupCtxtExact n (gamma defs)
              | Nothing => pure (Arity 0)
         case definition gdef of
           DCon _ arity Nothing => pure (EraseArgs arity (eraseArgs gdef))
           DCon _ arity (Just (_, pos)) => pure (NewTypeBy arity pos)
           PMDef _ args _ _ _ => pure (EraseArgs (length args) (eraseArgs gdef))
           ExternDef arity => pure (Arity arity)
           ForeignDef arity _ => pure (Arity arity)
           Builtin {arity} f => pure (Arity arity)
           _ => pure (Arity 0)
numArgs _ tm = pure (Arity 0)

mkSub : Nat -> (ns : List Name) -> List Nat -> (ns' ** SubVars ns' ns)
mkSub i _ [] = (_ ** SubRefl)
mkSub i [] ns = (_ ** SubRefl)
mkSub i (x :: xs) es
    = let (ns' ** p) = mkSub (S i) xs es in
          if i `elem` es
             then (ns' ** DropCons p)
             else (x :: ns' ** KeepCons p)

weakenVar : Var ns -> Var (a :: ns)
weakenVar (MkVar p) = (MkVar (Later p))

etaExpand : {vars : _} ->
            Int -> Nat -> CExp vars -> List (Var vars) -> CExp vars
etaExpand i Z exp args = mkApp exp (map (mkLocal (getFC exp)) (reverse args))
  where
    mkLocal : FC -> (Var vars) -> CExp vars
    mkLocal fc (MkVar p) = CLocal fc p

    mkApp : CExp vars -> List (CExp vars) -> CExp vars
    mkApp tm [] = tm
    mkApp (CApp fc f args) args' = CApp fc f (args ++ args')
    mkApp (CCon fc n ci t args) args' = CCon fc n ci t (args ++ args')
    mkApp (CExtPrim fc p args) args' = CExtPrim fc p (args ++ args')
    mkApp tm args = CApp (getFC tm) tm args
etaExpand i (S k) exp args
    = CLam (getFC exp) (MN "eta" i)
             (etaExpand (i + 1) k (weaken exp)
                  (MkVar First :: map weakenVar args))

export
expandToArity : {vars : _} ->
                Nat -> CExp vars -> List (CExp vars) -> CExp vars
-- No point in applying to anything
expandToArity _ (CErased fc) _ = CErased fc
-- Overapplied; apply everything as single arguments
expandToArity Z f args = applyAll f args
  where
    applyAll : CExp vars -> List (CExp vars) -> CExp vars
    applyAll fn [] = fn
    applyAll fn (a :: args) = applyAll (CApp (getFC fn) fn [a]) args
expandToArity (S k) f (a :: args) = expandToArity k (addArg f a) args
  where
    addArg : CExp vars -> CExp vars -> CExp vars
    addArg (CApp fc fn args) a = CApp fc fn (args ++ [a])
    addArg (CCon fc n ci tag args) a = CCon fc n ci tag (args ++ [a])
    addArg (CExtPrim fc p args) a = CExtPrim fc p (args ++ [a])
    addArg f a = CApp (getFC f) f [a]
-- Underapplied, saturate with lambdas
expandToArity num fn [] = etaExpand 0 num fn []

applyNewType : {vars : _} ->
               Nat -> Nat -> CExp vars -> List (CExp vars) -> CExp vars
applyNewType arity pos fn args
    = let fn' = expandToArity arity fn args in
          keepArg fn' -- fn' might be lambdas, after eta expansion
  where
    keep : Nat -> List (CExp vs) -> CExp vs
    keep i [] = CErased (getFC fn) -- can't happen if all is well!
    keep i (x :: xs)
        = if i == pos
             then x
             else keep (1 + i) xs

    keepArg : CExp vs -> CExp vs
    keepArg (CLam fc x sc) = CLam fc x (keepArg sc)
    keepArg (CCon fc _ _ _ args) = keep 0 args
    keepArg tm = CErased (getFC fn)

dropFrom : List Nat -> Nat -> List (CExp vs) -> List (CExp vs)
dropFrom epos i [] = []
dropFrom epos i (x :: xs)
    = if i `elem` epos
         then dropFrom epos (1 + i) xs
         else x :: dropFrom epos (1 + i) xs

dropPos : List Nat -> CExp vs -> CExp vs
dropPos epos (CLam fc x sc) = CLam fc x (dropPos epos sc)
dropPos epos (CApp fc tm@(CApp _ _ _) args')
    = CApp fc (dropPos epos tm) args'
dropPos epos (CApp fc f args) = CApp fc f (dropFrom epos 0 args)
dropPos epos (CCon fc c ci a args) = CCon fc c ci a (dropFrom epos 0 args)
dropPos epos tm = tm

eraseConArgs : {vars : _} ->
               Nat -> List Nat -> CExp vars -> List (CExp vars) -> CExp vars
eraseConArgs arity epos fn args
    = let fn' = expandToArity arity fn args in
          if not (isNil epos)
             then dropPos epos fn' -- fn' might be lambdas, after eta expansion
             else fn'

mkDropSubst : Nat -> List Nat ->
              (rest : List Name) ->
              (vars : List Name) ->
              (vars' ** SubVars (vars' ++ rest) (vars ++ rest))
mkDropSubst i es rest [] = ([] ** SubRefl)
mkDropSubst i es rest (x :: xs)
    = let (vs ** sub) = mkDropSubst (1 + i) es rest xs in
          if i `elem` es
             then (vs ** DropCons sub)
             else (x :: vs ** KeepCons sub)

-- Rewrite applications of Nat-like constructors and functions to more optimal
-- versions using Integer

-- None of these should be hard coded, but we'll do it this way until we
-- have a more general approach to optimising data types!
-- NOTE: Make sure that names mentioned here are listed in 'natHackNames' in
-- Common.idr, so that they get compiled, as they won't be spotted by the
-- usual calls to 'getRefs'.
data Magic : Type where
  MagicCCon : Name -> (arity : Nat) -> -- checks
              (FC -> forall vars. Vect arity (CExp vars) -> CExp vars) -> -- translation
              Magic
  MagicCRef : Name -> (arity : Nat) -> -- checks
              (FC -> FC -> forall vars. Vect arity (CExp vars) -> CExp vars) -> --translation
              Magic

magic : List Magic -> CExp vars -> CExp vars
magic ms (CLam fc x exp) = CLam fc x (magic ms exp)
magic ms e = go ms e where

  fire : Magic -> CExp vars -> Maybe (CExp vars)
  fire (MagicCCon n arity f) (CCon fc n' _ _ es)
    = do guard (n == n')
         map (f fc) (toVect arity es)
  fire (MagicCRef n arity f) (CApp fc (CRef fc' n') es)
    = do guard (n == n')
         map (f fc fc') (toVect arity es)
  fire _ _ = Nothing

  go : List Magic -> CExp vars -> CExp vars
  go [] e = e
  go (m :: ms) e = case fire m e of
    Nothing => go ms e
    Just e' => e'

%inline
magic__integerToNat : FC -> FC -> forall vars. Vect 1 (CExp vars) -> CExp vars
magic__integerToNat fc fc' [k]
  = CApp fc (CRef fc' (NS typesNS (UN $ Basic "prim__integerToNat"))) [k]

magic__natMinus : FC -> FC -> forall vars. Vect 2 (CExp vars) -> CExp vars
magic__natMinus fc fc' [m,n]
  = magic__integerToNat fc fc'
    [CApp fc (CRef fc' (UN $ Basic "prim__sub_Integer")) [m, n]]

-- We don't reuse natMinus here because we assume that unsuc will only be called
-- on S-headed numbers so we do not need the truncating integerToNat call!
magic__natUnsuc : FC -> FC -> forall vars. Vect 1 (CExp vars) -> CExp vars
magic__natUnsuc fc fc' [m]
  = CApp fc (CRef fc' (UN $ Basic "prim__sub_Integer")) [m, CPrimVal fc (BI 1)]

-- TODO: next release remove this and use %builtin pragma
natHack : List Magic
natHack =
    [ MagicCRef (NS typesNS (UN $ Basic "natToInteger")) 1 (\ _, _, [k] => k)
    , MagicCRef (NS typesNS (UN $ Basic "integerToNat")) 1 magic__integerToNat
    , MagicCRef (NS typesNS (UN $ Basic "plus")) 2
         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__add_Integer")) [m, n])
    , MagicCRef (NS typesNS (UN $ Basic "mult")) 2
         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__mul_Integer")) [m, n])
    , MagicCRef (NS typesNS (UN $ Basic "minus")) 2 magic__natMinus
    , MagicCRef (NS typesNS (UN $ Basic "equalNat")) 2
         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__eq_Integer")) [m, n])
    , MagicCRef (NS typesNS (UN $ Basic "compareNat")) 2
         (\ fc, fc', [m,n] => CApp fc (CRef fc' (NS eqOrdNS (UN $ Basic "compareInteger"))) [m, n])
    ]

-- get all transformation from %builtin pragmas
builtinMagic : Ref Ctxt Defs => Core (forall vars. CExp vars -> CExp vars)
builtinMagic = pure $ magic natHack

data NextSucc : Type where
newSuccName : {auto s : Ref NextSucc Int} -> Core Name
newSuccName = do
    x <- get NextSucc
    put NextSucc $ x + 1
    pure $ MN "succ" x

natBranch :  CConAlt vars -> Bool
natBranch (MkConAlt n ZERO _ _ _) = True
natBranch (MkConAlt n SUCC _ _ _) = True
natBranch _ = False

trySBranch : CExp vars -> CConAlt vars -> Maybe (CExp vars)
trySBranch n (MkConAlt nm SUCC _ [arg] sc)
    = Just (CLet (getFC n) arg True (magic__natUnsuc (getFC n) (getFC n) [n]) sc)
trySBranch _ _ = Nothing

tryZBranch : CConAlt vars -> Maybe (CExp vars)
tryZBranch (MkConAlt n ZERO _ [] sc) = Just sc
tryZBranch _ = Nothing

getSBranch : CExp vars -> List (CConAlt vars) -> Maybe (CExp vars)
getSBranch n [] = Nothing
getSBranch n (x :: xs) = trySBranch n x <+> getSBranch n xs

getZBranch : List (CConAlt vars) -> Maybe (CExp vars)
getZBranch [] = Nothing
getZBranch (x :: xs) = tryZBranch x <+> getZBranch xs

-- Rewrite case trees on Nat to be case trees on Integer
builtinNatTree : {auto s : Ref NextSucc Int} -> CExp vars -> Core (CExp vars)
builtinNatTree (CConCase fc sc@(CLocal _ _) alts def)
   = pure $ if any natBranch alts
               then let defb = fromMaybe (CCrash fc "Nat case not covered") def
                        salt = maybe defb id (getSBranch sc alts)
                        zalt = maybe defb id (getZBranch alts) in
                        CConstCase fc sc [MkConstAlt (BI 0) zalt] (Just salt)
               else CConCase fc sc alts def
builtinNatTree (CConCase fc sc alts def)
    = do x <- newSuccName
         pure $ CLet fc x True sc
                !(builtinNatTree $ CConCase fc (CLocal fc First) (map weaken alts) (map weaken def))
builtinNatTree t = pure t

enumTree : CExp vars -> CExp vars
enumTree (CConCase fc sc alts def)
   = let x = traverse toEnum alts
         Just alts' = x
              | Nothing => CConCase fc sc alts def in
         CConstCase fc sc alts' def
  where
    toEnum : CConAlt vars -> Maybe (CConstAlt vars)
    toEnum (MkConAlt nm ENUM (Just tag) [] sc)
        = pure $ MkConstAlt (I tag) sc
    toEnum _ = Nothing
enumTree t = t

-- See if the constructor is a special constructor type, e.g a nil or cons
-- shaped thing.
dconFlag : {auto c : Ref Ctxt Defs} ->
           Name -> Core ConInfo
dconFlag n
    = do defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs)
              | Nothing => throw (InternalError ("Can't find " ++ show n))
         pure (ciFlags (flags def))
  where
    ciFlags : List DefFlag -> ConInfo
    ciFlags [] = DATACON
    ciFlags (ConType ci :: xs) = ci
    ciFlags (x :: xs) = ciFlags xs

mutual
  toCExpTm : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto s : Ref NextSucc Int} ->
             (magic : forall vars. CExp vars -> CExp vars) ->
             Name -> Term vars ->
             Core (CExp vars)
  toCExpTm m n (Local fc _ _ prf)
      = pure $ CLocal fc prf
  toCExpTm m n (Ref fc (DataCon tag arity) fn)
      = do -- get full name for readability, and %builtin Natural
           cn <- getFullName fn
           fl <- dconFlag cn
           case fl of
                ENUM => pure $ CPrimVal fc (I tag)
                ZERO => pure $ CPrimVal fc (BI 0)
                SUCC => do x <- newSuccName
                           pure $ CLam fc x $ COp fc (Add IntegerType) [CPrimVal fc (BI 1), CLocal fc First]
                _ => pure $ CCon fc cn fl (Just tag) []
  toCExpTm m n (Ref fc (TyCon tag arity) fn)
      = pure $ CCon fc fn TYCON Nothing []
  toCExpTm m n (Ref fc _ fn)
      = do full <- getFullName fn
               -- ^ For readability of output code, and the Nat hack,
           pure $ CApp fc (CRef fc full) []
  toCExpTm m n (Meta fc mn i args)
      = pure $ CApp fc (CRef fc mn) !(traverse (toCExp m n) args)
  toCExpTm m n (Bind fc x (Lam _ _ _ _) sc)
      = pure $ CLam fc x !(toCExp m n sc)
  toCExpTm m n (Bind fc x (Let _ rig val _) sc)
      = do sc' <- toCExp m n sc
           pure $ branchZero (shrinkCExp (DropCons SubRefl) sc')
                          (CLet fc x True !(toCExp m n val) sc')
                          rig
  toCExpTm m n (Bind fc x (Pi _ c e ty) sc)
      = pure $ CCon fc (UN (Basic "->")) TYCON Nothing
                       [ !(toCExp m n ty)
                       , CLam fc x !(toCExp m n sc)]
  toCExpTm m n (Bind fc x b tm) = pure $ CErased fc
  -- We'd expect this to have been dealt with in toCExp, but for completeness...
  toCExpTm m n (App fc tm arg)
      = pure $ CApp fc !(toCExp m n tm) [!(toCExp m n arg)]
  -- This shouldn't be in terms any more, but here for completeness
  toCExpTm m n (As _ _ _ p) = toCExpTm m n p
  -- TODO: Either make sure 'Delayed' is always Rig0, or add to typecase
  toCExpTm m n (TDelayed fc _ _) = pure $ CErased fc
  toCExpTm m n (TDelay fc lr _ arg)
      = pure (CDelay fc lr !(toCExp m n arg))
  toCExpTm m n (TForce fc lr arg)
      = pure (CForce fc lr !(toCExp m n arg))
  toCExpTm m n (PrimVal fc c)
      = let t = constTag c in
            if t == 0
               then pure $ CPrimVal fc c
               else pure $ CCon fc (UN $ Basic $ show c) TYCON Nothing []
  toCExpTm m n (Erased fc _) = pure $ CErased fc
  toCExpTm m n (TType fc) = pure $ CCon fc (UN (Basic "Type")) TYCON Nothing []

  toCExp : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto s : Ref NextSucc Int} ->
           (magic : forall vars. CExp vars -> CExp vars) ->
           Name -> Term vars ->
           Core (CExp vars)
  toCExp m n tm
      = case getFnArgs tm of
             (f, args) =>
                do args' <- traverse (toCExp m n) args
                   defs <- get Ctxt
                   f' <- toCExpTm m n f
                   Arity a <- numArgs defs f
                      | NewTypeBy arity pos =>
                            do let res = applyNewType arity pos f' args'
                               pure $ m res
                      | EraseArgs arity epos =>
                            do let res = eraseConArgs arity epos f' args'
                               pure $ m res
                   let res = expandToArity a f' args'
                   pure $ m res

mutual
  conCases : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto s : Ref NextSucc Int} ->
             Name -> List (CaseAlt vars) ->
             Core (List (CConAlt vars))
  conCases n [] = pure []
  conCases {vars} n (ConCase x tag args sc :: ns)
      = do defs <- get Ctxt
           Just gdef <- lookupCtxtExact x (gamma defs)
                | Nothing => -- primitive type match
                     do xn <- getFullName x
                        pure $ MkConAlt xn TYCON Nothing args !(toCExpTree n sc)
                                  :: !(conCases n ns)
           case (definition gdef) of
                DCon _ arity (Just pos) => conCases n ns -- skip it
                _ => do xn <- getFullName x
                        let (args' ** sub)
                            = mkDropSubst 0 (eraseArgs gdef) vars args
                        sc' <- toCExpTree n sc
                        ns' <- conCases n ns
                        if dcon (definition gdef)
                           then pure $ MkConAlt xn !(dconFlag xn) (Just tag) args' (shrinkCExp sub sc') :: ns'
                           else pure $ MkConAlt xn !(dconFlag xn) Nothing args' (shrinkCExp sub sc') :: ns'
    where
      dcon : Def -> Bool
      dcon (DCon _ _ _) = True
      dcon _ = False
  conCases n (_ :: ns) = conCases n ns

  constCases : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto s : Ref NextSucc Int} ->
               Name -> List (CaseAlt vars) ->
               Core (List (CConstAlt vars))
  constCases n [] = pure []
  constCases n (ConstCase WorldVal sc :: ns)
      = constCases n ns
  constCases n (ConstCase x sc :: ns)
      = pure $ MkConstAlt x !(toCExpTree n sc) ::
                    !(constCases n ns)
  constCases n (_ :: ns) = constCases n ns

  -- If there's a case which matches on a 'newtype', return the RHS
  -- without matching.
  -- Take some care if the newtype involves a WorldVal - in that case we
  -- still need to let bind the scrutinee to ensure it's evaluated exactly
  -- once.
  getNewType : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto s : Ref NextSucc Int} ->
               FC -> CExp vars ->
               Name -> List (CaseAlt vars) ->
               Core (Maybe (CExp vars))
  getNewType fc scr n [] = pure Nothing
  getNewType fc scr n (DefaultCase sc :: ns)
      = pure $ Nothing
  getNewType {vars} fc scr n (ConCase x tag args sc :: ns)
      = do defs <- get Ctxt
           case !(lookupDefExact x (gamma defs)) of
                -- If the flag is False, we still take the
                -- default, but need to evaluate the scrutinee of the
                -- case anyway - if the data structure contains a %World,
                -- that we've erased, it means it has interacted with the
                -- outside world, so we need to evaluate to keep the
                -- side effect.
                Just (DCon _ arity (Just (noworld, pos))) =>
-- FIXME: We don't need the commented out bit *for now* because io_bind
-- isn't being inlined, but it does need to be a little bit cleverer to
-- get the best performance.
-- I'm (edwinb) keeping it visible here because I plan to put it back in
-- more or less this form once case inlining works better and the whole thing
-- works in a nice principled way.
--                      if noworld -- just substitute the scrutinee into
--                                 -- the RHS
--                         then
                             let env : SubstCEnv args vars
                                     = mkSubst 0 scr pos args in
                                 pure $ Just (substs env !(toCExpTree n sc))
--                         else -- let bind the scrutinee, and substitute the
--                              -- name into the RHS
--                              let env : SubstCEnv args (MN "eff" 0 :: vars)
--                                      = mkSubst 0 (CLocal fc First) pos args in
--                              do sc' <- toCExpTree n sc
--                                 let scope = insertNames {outer=args}
--                                                         {inner=vars}
--                                                         [MN "eff" 0] sc'
--                                 pure $ Just (CLet fc (MN "eff" 0) False scr
--                                                   (substs env scope))
                _ => pure Nothing -- there's a normal match to do
    where
      mkSubst : Nat -> CExp vs ->
                Nat -> (args : List Name) -> SubstCEnv args vs
      mkSubst _ _ _ [] = Nil
      mkSubst i scr pos (a :: as)
          = if i == pos
               then scr :: mkSubst (1 + i) scr pos as
               else CErased fc :: mkSubst (1 + i) scr pos as
  getNewType fc scr n (_ :: ns) = getNewType fc scr n ns

  getDef : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto s : Ref NextSucc Int} ->
           Name -> List (CaseAlt vars) ->
           Core (Maybe (CExp vars))
  getDef n [] = pure Nothing
  getDef n (DefaultCase sc :: ns)
      = pure $ Just !(toCExpTree n sc)
  getDef n (ConstCase WorldVal sc :: ns)
      = pure $ Just !(toCExpTree n sc)
  getDef n (_ :: ns) = getDef n ns

  toCExpTree : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto s : Ref NextSucc Int} ->
               Name -> CaseTree vars ->
               Core (CExp vars)
  toCExpTree n alts@(Case _ x scTy (DelayCase ty arg sc :: rest))
      = let fc = getLoc scTy in
            pure $
              CLet fc arg True (CForce fc LInf (CLocal (getLoc scTy) x)) $
              CLet fc ty True (CErased fc)
                   !(toCExpTree n sc)
  toCExpTree n alts
      = toCExpTree' n alts

  toCExpTree' : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto s : Ref NextSucc Int} ->
                Name -> CaseTree vars ->
                Core (CExp vars)
  toCExpTree' n (Case _ x scTy alts@(ConCase _ _ _ _ :: _))
      = let fc = getLoc scTy in
            do Nothing <- getNewType fc (CLocal fc x) n alts
                   | Just def => pure def
               defs <- get Ctxt
               cases <- conCases n alts
               def <- getDef n alts
               if isNil cases
                  then pure (fromMaybe (CErased fc) def)
                  else pure $ enumTree !(builtinNatTree $
                            CConCase fc (CLocal fc x) cases def)
  toCExpTree' n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
      = throw (InternalError "Unexpected DelayCase")
  toCExpTree' n (Case fc x scTy alts@(ConstCase _ _ :: _))
      = let fc = getLoc scTy in
            do cases <- constCases n alts
               def <- getDef n alts
               if isNil cases
                  then pure (fromMaybe (CErased fc) def)
                  else pure $ CConstCase fc (CLocal fc x) cases def
  toCExpTree' n (Case _ x scTy alts@(DefaultCase sc :: _))
      = toCExpTree n sc
  toCExpTree' n (Case _ x scTy [])
      = pure $ CCrash (getLoc scTy) $ "Missing case tree in " ++ show n
  toCExpTree' n (STerm _ tm) = toCExp !builtinMagic n tm
  toCExpTree' n (Unmatched msg)
      = pure $ CCrash emptyFC msg
  toCExpTree' n Impossible
      = pure $ CCrash emptyFC ("Impossible case encountered in " ++ show n)

-- Need this for ensuring that argument list matches up to operator arity for
-- builtins
data ArgList : Nat -> List Name -> Type where
     NoArgs : ArgList Z []
     ConsArg : (a : Name) -> ArgList k as -> ArgList (S k) (a :: as)

mkArgList : Int -> (n : Nat) -> (ns ** ArgList n ns)
mkArgList i Z = (_ ** NoArgs)
mkArgList i (S k)
    = let (_ ** rec) = mkArgList (i + 1) k in
          (_ ** ConsArg (MN "arg" i) rec)

data NArgs : Type where
     User : Name -> List (Closure []) -> NArgs
     Struct : String -> List (String, Closure []) -> NArgs
     NUnit : NArgs
     NPtr : NArgs
     NGCPtr : NArgs
     NBuffer : NArgs
     NForeignObj : NArgs
     NIORes : Closure [] -> NArgs

getPArgs : {auto c : Ref Ctxt Defs} ->
           Defs -> Closure [] -> Core (String, Closure [])
getPArgs defs cl
    = do NDCon fc _ _ _ args <- evalClosure defs cl
             | nf => throw (GenericMsg (getLoc nf) "Badly formed struct type")
         case reverse (map snd args) of
              (tydesc :: n :: _) =>
                  do NPrimVal _ (Str n') <- evalClosure defs n
                         | nf => throw (GenericMsg (getLoc nf) "Unknown field name")
                     pure (n', tydesc)
              _ => throw (GenericMsg fc "Badly formed struct type")

getFieldArgs : {auto c : Ref Ctxt Defs} ->
               Defs -> Closure [] -> Core (List (String, Closure []))
getFieldArgs defs cl
    = do NDCon fc _ _ _ args <- evalClosure defs cl
             | nf => throw (GenericMsg (getLoc nf) "Badly formed struct type")
         case map snd args of
              -- cons
              [_, t, rest] =>
                  do rest' <- getFieldArgs defs rest
                     (n, ty) <- getPArgs defs t
                     pure ((n, ty) :: rest')
              -- nil
              _ => pure []

getNArgs : {auto c : Ref Ctxt Defs} ->
           Defs -> Name -> List (Closure []) -> Core NArgs
getNArgs defs (NS _ (UN $ Basic "IORes")) [arg] = pure $ NIORes arg
getNArgs defs (NS _ (UN $ Basic "Ptr")) [arg] = pure NPtr
getNArgs defs (NS _ (UN $ Basic "AnyPtr")) [] = pure NPtr
getNArgs defs (NS _ (UN $ Basic "GCPtr")) [arg] = pure NGCPtr
getNArgs defs (NS _ (UN $ Basic "GCAnyPtr")) [] = pure NGCPtr
getNArgs defs (NS _ (UN $ Basic "Buffer")) [] = pure NBuffer
getNArgs defs (NS _ (UN $ Basic "ForeignObj")) [] = pure NForeignObj
getNArgs defs (NS _ (UN $ Basic "Unit")) [] = pure NUnit
getNArgs defs (NS _ (UN $ Basic "Struct")) [n, args]
    = do NPrimVal _ (Str n') <- evalClosure defs n
             | nf => throw (GenericMsg (getLoc nf) "Unknown name for struct")
         pure (Struct n' !(getFieldArgs defs args))
getNArgs defs n args = pure $ User n args

nfToCFType : {auto c : Ref Ctxt Defs} ->
             FC -> (inStruct : Bool) -> NF [] -> Core CFType
nfToCFType _ _ (NPrimVal _ IntType) = pure CFInt
nfToCFType _ _ (NPrimVal _ IntegerType) = pure CFInteger
nfToCFType _ _ (NPrimVal _ Bits8Type) = pure CFUnsigned8
nfToCFType _ _ (NPrimVal _ Bits16Type) = pure CFUnsigned16
nfToCFType _ _ (NPrimVal _ Bits32Type) = pure CFUnsigned32
nfToCFType _ _ (NPrimVal _ Bits64Type) = pure CFUnsigned64
nfToCFType _ _ (NPrimVal _ Int8Type) = pure CFInt8
nfToCFType _ _ (NPrimVal _ Int16Type) = pure CFInt16
nfToCFType _ _ (NPrimVal _ Int32Type) = pure CFInt32
nfToCFType _ _ (NPrimVal _ Int64Type) = pure CFInt64
nfToCFType _ False (NPrimVal _ StringType) = pure CFString
nfToCFType fc True (NPrimVal _ StringType)
    = throw (GenericMsg fc "String not allowed in a foreign struct")
nfToCFType _ _ (NPrimVal _ DoubleType) = pure CFDouble
nfToCFType _ _ (NPrimVal _ CharType) = pure CFChar
nfToCFType _ _ (NPrimVal _ WorldType) = pure CFWorld
nfToCFType _ False (NBind fc _ (Pi _ _ _ ty) sc)
    = do defs <- get Ctxt
         sty <- nfToCFType fc False !(evalClosure defs ty)
         sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
         tty <- nfToCFType fc False sc'
         pure (CFFun sty tty)
nfToCFType _ True (NBind fc _ _ _)
    = throw (GenericMsg fc "Function types not allowed in a foreign struct")
nfToCFType _ s (NTCon fc n_in _ _ args)
    = do defs <- get Ctxt
         n <- toFullNames n_in
         case !(getNArgs defs n $ map snd args) of
              User un uargs =>
                do nargs <- traverse (evalClosure defs) uargs
                   cargs <- traverse (nfToCFType fc s) nargs
                   pure (CFUser n cargs)
              Struct n fs =>
                do fs' <- traverse
                             (\ (n, ty) =>
                                    do tynf <- evalClosure defs ty
                                       tycf <- nfToCFType fc True tynf
                                       pure (n, tycf)) fs
                   pure (CFStruct n fs')
              NUnit => pure CFUnit
              NPtr => pure CFPtr
              NGCPtr => pure CFGCPtr
              NBuffer => pure CFBuffer
              NForeignObj => pure CFForeignObj
              NIORes uarg =>
                do narg <- evalClosure defs uarg
                   carg <- nfToCFType fc s narg
                   pure (CFIORes carg)
nfToCFType _ s (NType _)
    = pure (CFUser (UN (Basic "Type")) [])
nfToCFType _ s (NErased _ _)
    = pure (CFUser (UN (Basic "__")) [])
nfToCFType fc s t
    = do defs <- get Ctxt
         ty <- quote defs [] t
         throw (GenericMsg (getLoc t)
                       ("Can't marshal type for foreign call " ++
                                      show !(toFullNames ty)))

getCFTypes : {auto c : Ref Ctxt Defs} ->
             List CFType -> NF [] ->
             Core (List CFType, CFType)
getCFTypes args (NBind fc _ (Pi _ _ _ ty) sc)
    = do defs <- get Ctxt
         aty <- nfToCFType fc False !(evalClosure defs ty)
         sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
         getCFTypes (aty :: args) sc'
getCFTypes args t
    = pure (reverse args, !(nfToCFType (getLoc t) False t))

lamRHSenv : Int -> FC -> (ns : List Name) -> SubstCEnv ns []
lamRHSenv i fc [] = []
lamRHSenv i fc (n :: ns)
    = CRef fc (MN "x" i) :: lamRHSenv (i + 1) fc ns

mkBounds : (xs : _) -> Bounds xs
mkBounds [] = None
mkBounds (x :: xs) = Add x x (mkBounds xs)

getNewArgs : {done : _} ->
             SubstCEnv done args -> List Name
getNewArgs [] = []
getNewArgs (CRef _ n :: xs) = n :: getNewArgs xs
getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub

-- If a name is declared in one module and defined in another,
-- we have to assume arity 0 for incremental compilation because
-- we have no idea how it's defined, and when we made calls to the
-- function, they had arity 0.
lamRHS : (ns : List Name) -> CExp ns -> CExp []
lamRHS ns tm
    = let env = lamRHSenv 0 (getFC tm) ns
          tmExp = substs env (rewrite appendNilRightNeutral ns in tm)
          newArgs = reverse $ getNewArgs env
          bounds = mkBounds newArgs
          expLocs = mkLocals zero {vars = []} bounds tmExp in
          lamBind (getFC tm) _ expLocs
  where
    lamBind : FC -> (ns : List Name) -> CExp ns -> CExp []
    lamBind fc [] tm = tm
    lamBind fc (n :: ns) tm = lamBind fc ns (CLam fc n tm)

toCDef : {auto c : Ref Ctxt Defs} ->
         Name -> ClosedTerm -> List Nat -> Def ->
         Core CDef
toCDef n ty _ None
    = pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n))
toCDef n ty erased (PMDef pi args _ tree _)
    = do let (args' ** p) = mkSub 0 args erased
         s <- newRef NextSucc 0
         comptree <- toCExpTree n tree
         pure $ toLam (externalDecl pi) $ if isNil erased
            then MkFun args comptree
            else MkFun args' (shrinkCExp p comptree)
  where
    toLam : Bool -> CDef -> CDef
    toLam True (MkFun args rhs) = MkFun [] (lamRHS args rhs)
    toLam _ d = d
toCDef n ty _ (ExternDef arity)
    = let (ns ** args) = mkArgList 0 arity in
          pure $ MkFun _ (CExtPrim emptyFC !(getFullName n) (map toArgExp (getVars args)))
  where
    toArgExp : (Var ns) -> CExp ns
    toArgExp (MkVar p) = CLocal emptyFC p

    getVars : ArgList k ns -> List (Var ns)
    getVars NoArgs = []
    getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
toCDef n ty _ (ForeignDef arity cs)
    = do defs <- get Ctxt
         (atys, retty) <- getCFTypes [] !(nf defs [] ty)
         pure $ MkForeign cs atys retty
toCDef n ty _ (Builtin {arity} op)
    = let (ns ** args) = mkArgList 0 arity in
          pure $ MkFun _ (COp emptyFC op (map toArgExp (getVars args)))
  where
    toArgExp : (Var ns) -> CExp ns
    toArgExp (MkVar p) = CLocal emptyFC p

    getVars : ArgList k ns -> Vect k (Var ns)
    getVars NoArgs = []
    getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
toCDef n _ _ (DCon tag arity pos)
    = do let nt = snd <$> pos
         defs <- get Ctxt
         args <- numArgs {vars = []} defs (Ref EmptyFC (DataCon tag arity) n)
         let arity' = case args of
                 NewTypeBy ar _ => ar
                 EraseArgs ar erased => ar `minus` length erased
                 Arity ar => ar
         pure $ MkCon (Just tag) arity' nt
toCDef n _ _ (TCon tag arity _ _ _ _ _ _)
    = pure $ MkCon Nothing arity Nothing
-- We do want to be able to compile these, but also report an error at run time
-- (and, TODO: warn at compile time)
toCDef n ty _ (Hole _ _)
    = pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++
                                       show !(getFullName n))
toCDef n ty _ (Guess _ _ _)
    = pure $ MkError $ CCrash emptyFC ("Encountered constrained hole " ++
                                       show !(getFullName n))
toCDef n ty _ (BySearch _ _ _)
    = pure $ MkError $ CCrash emptyFC ("Encountered incomplete proof search " ++
                                       show !(getFullName n))
toCDef n ty _ def
    = pure $ MkError $ CCrash emptyFC ("Encountered uncompilable name " ++
                                       show (!(getFullName n), def))

export
compileExp : {auto c : Ref Ctxt Defs} ->
             ClosedTerm -> Core (CExp [])
compileExp tm
    = do m <- builtinMagic
         s <- newRef NextSucc 0
         exp <- toCExp m (UN $ Basic "main") tm
         pure exp

||| Given a name, look up an expression, and compile it to a CExp in the environment
export
compileDef : {auto c : Ref Ctxt Defs} -> Name -> Core ()
compileDef n
    = do defs <- get Ctxt
         Just gdef <- lookupCtxtExact n (gamma defs)
              | Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n))
         -- If we're incremental, and the name has no definition yet, it
         -- might end up defined in another module, so leave it, but warn
         if noDefYet (definition gdef) (incrementalCGs !getSession)
           -- This won't be accurate if we have names declared in one module
           -- and defined elsewhere. It's tricky to do the complete check that
           -- we do for whole program compilation, though, since that involves
           -- traversing everything from the main expression.
           -- For now, consider it an incentive not to have cycles :).
            then recordWarning (GenericWarn ("Compiling hole " ++ show n))
            else do ce <- toCDef n (type gdef) (eraseArgs gdef)
                           !(toFullNames (definition gdef))
                    setCompiled n ce
  where
    noDefYet : Def -> List CG -> Bool
    noDefYet None (_ :: _) = True
    noDefYet _ _ = False


text:
module AssRecRule

import Data.Fin
import Data.Vect

{-
 The recursion function for lists of type `a`. Define this by pattern matching
 recList : (x: Type) -> x -> (Nat -> List Nat -> x -> x) -> (List Nat -> x)
-}
recList : (a: Type) ->  (x: Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)
recList a x base step [] = base
recList a x base step (y :: xs) = step y xs (recList a x base step xs)

{-
Given a list of type `a` and a function `f: a -> b` get a list of type `b`
by applying `f` to each element.
Note: Define using `recList` and without pattern matching on lists.
-}
mapList : (a: Type) -> (b: Type) -> (f: a -> b) -> List a -> List b
mapList a b f la = recList a (List b) [] step la where
  step = \y: a => \xs: List a => \listb: List b => (f y) :: listb
{-
Given a list of type `a`, an initial value `init: a` and an operation `op: a -> a -> a`,
get an element of `a` by starting with init and repeatedly applying the elements of the
list,
e.g. fold Nat 1 (*) ([22] :: [3] :: [])  = 1 * 22 * 3
Note: Define using `recList` and without pattern matching on lists.
-}
foldList : (a: Type) ->  (init: a) -> (op : a -> a -> a) -> List a -> a
foldList a init op la = recList a a init step la where
  step = \y: a => \xs: List a=> \prev : a => (op y prev)

{-
The induction function on the `Fin` indexed type family. Define this by pattern matching.
-}
inducFin : (xs : (n: Nat) -> Fin n -> Type) ->
  (base : (m: Nat) -> xs (S m) FZ) ->
  (step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))) ->
  (q: Nat) -> (j: Fin q) -> xs q j
inducFin xs base step Z j = FinZElim j
inducFin xs base step (S p) FZ = base p
inducFin xs base step (S p) (FS k)  = step p k (inducFin xs base step p k)
{-
Given a type `a`, a natural number `q`, an element `j : Fin q` and a vector `v` of length q with entries of type `a`,
get the element in position `j` of `v`. Note that this is always well defined.

Note: Define using `inducList` and without pattern matching on the `Fin` family. You may pattern match on Vectors.
The definition should have only one case, and there should be no case splitting on `Fin`.
-}
fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)
fetchElem a q j vect =  inducFin xs base step q j vect where
  xs : (n: Nat) -> Fin n -> Type
  xs q j = Vect q a -> a
  base : (m: Nat) -> xs (S m) FZ
  base len = head
  step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))
  step p k prev = prevtail where
    prevtail : Vect (S p) a-> a
    prevtail (hd::tl) = prev tl
{-Q.E.D.-}


text:
module Dbcritic.Check.TimeZone

import Control.IOExcept
import Data.Vect
import Dbcritic.Check
import Dbcritic.Libpq

export
issueLocaltime : Issue
issueLocaltime =
    let
        identifier  = [ "localtime" ]
        description = "The client receives timestamps in the time zone of the server."
        problems    = [ "Changing the server time zone causes the client to receive different timestamps." ]
        solutions   = [ "Set the ‘TimeZone’ configuration parameter to a concrete time zone, such as UTC." ]
    in
        MkIssue identifier description problems solutions IsNonEmpty IsNonEmpty IsNonEmpty

export
checkTimeZone : Check
checkTimeZone = MkCheck name help inspect
    where
    name = "time_zone"
    help = "Check that the ‘TimeZone’ parameter is set to a sensible value."

    inspect : PgConnection -> IOExcept String (List Issue)
    inspect conn = do
        res <- pgExecute conn """
            SHOW "TimeZone"
        """
        case pgCell res 0 0 of
            Just "localtime" => pure [issueLocaltime]
            Just _           => pure []
            Nothing          => ioe_fail "checkTimeZone: Bad result"

max_stars_repo_name: channable/dbcritic

max_issues_repo_name: channable/dbcritic

max_forks_repo_name: channable/dbcritic


text:
module RecRule

import Data.Fin

% access public export

recNat : (x : Type) -> x -> (Nat -> x -> x) -> (Nat -> x)
recNat x base step Z = base
recNat x base step (S k) = step k (recNat x base step k)

fctl : Nat -> Nat
fctl = recNat Nat (S Z) step where
  step = \n: Nat => \y : Nat => (S n) * y

recListNat : (x: Type) -> x -> (Nat -> List Nat -> x -> x) -> (List Nat -> x)
recListNat x base step [] = base
recListNat x base step (y :: xs) = step y xs previous where
  previous = recListNat x base step xs

lsum : List Nat -> Nat
lsum = recListNat Nat base step where
  base = Z
  step = \h : Nat => \t : List Nat => \accum : Nat => h + accum

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

recFin : (x: Type) ->
  (Nat -> x) ->
  ((n: Nat) -> Fin n -> x -> x) ->
  ((n: Nat) -> Fin n -> x)
recFin x base _ (S k) FZ = base k
recFin x base step (S k) (FS y) = step k y previous where
  previous = recFin x base step k y


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 8

import Data.Vect

-- check that all functions are total
%default total

--
-- section 8.1
--

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

-- exactLength : (len : Nat) -> (input : Vector m a) -> Maybe (Vector len a)
-- exactLength {m} len input = case m == len of
--                                  False => Nothing
--                                  True => Just ?exactLength_rhs_2

data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
  Same : (num : Nat) -> EqNat num num

sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS j j (Same j) = Same (S j)

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just (Same 0)
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = checkEqNat k j >>= Just . (sameS _ _)

exactLength : (len : Nat) -> (input : Vector m a) -> Maybe (Vector len a)
exactLength {m} len input = case checkEqNat m len of
                                 Nothing => Nothing
                                 (Just (Same len)) => Just input

--
-- section 8.2
--

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse {n = S k} (x :: xs)
  = let result = myReverse xs ++ [x] in
        rewrite plusCommutative 1 k in result

reverse_proof : (x : elem) -> (xs : Vect len elem) ->
                Vect (len + 1) elem -> Vect (S len) elem
reverse_proof {len} x xs result = rewrite plusCommutative 1 len in result

myReverse' : Vect n elem -> Vect n elem
myReverse' [] = []
myReverse' (x :: xs) = reverse_proof x xs (myReverse' xs ++ [x])

append_nil : (ys : Vect m elem) ->
             Vect (plus m 0) elem
append_nil {m} ys = rewrite plusZeroRightNeutral m in ys

append_xs : Vect (S (m + len)) elem -> Vect (plus m (S len)) elem
append_xs {m} {len} xs = rewrite sym (plusSuccRightSucc m len) in xs

myAppend : Vect n elem -> Vect m elem -> Vect (m + n) elem
myAppend [] ys = append_nil ys
myAppend (x :: xs) ys = append_xs (x :: myAppend xs ys)

--
-- section 8.3
--

twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible

valueNotSucc : x = S x -> Void
valueNotSucc Refl impossible

zeroNotSucc : (0 = S k) -> Void
zeroNotSucc Refl impossible

succNotZero : (S k = 0) -> Void
succNotZero Refl impossible

noRec : (contra : (k = j) -> Void) -> (S k = S j) -> Void
noRec contra Refl = contra Refl

checkEqNat2 : (num1 : Nat) -> (num2 : Nat) -> Dec (num1 = num2)
checkEqNat2 Z Z = Yes Refl
checkEqNat2 Z (S k) = No zeroNotSucc
checkEqNat2 (S k) Z = No succNotZero
checkEqNat2 (S k) (S j) = case checkEqNat2 k j of
                               (Yes prf) => Yes (cong prf)
                               (No contra) => No (noRec contra)

exactLength2 : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength2 {m} len input = case decEq m len of
                                  (Yes Refl) => Just input
                                  (No contra) => Nothing

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module HandMadeVectorStuff

import Data.Fin

%default total

data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

%name Vect xs, ys, zs

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

zip : Vect m a -> Vect m b -> Vect m (a, b)
zip [] [] = []
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys

vectTake : (n : Fin m) -> Vect m a -> Vect (finToNat n) a
vectTake FZ xs = []
vectTake (FS x) (y :: xs) = y :: vectTake x xs

vectGet : (x : Fin n) -> Vect n a -> a
vectGet FZ (x :: xs) = x
vectGet (FS x) (y :: xs) = vectGet x xs

sumEntries : Num e => Integer -> Vect n e -> Vect n e -> Maybe e
sumEntries {n} i xs ys = map sumAtIndex (integerToFin i n)
  where sumAtIndex fin = vectGet fin xs + (vectGet fin ys)

-- tryIndex : Integer -> Vect n a -> Maybe a
-- tryIndex {n} x xs = map (\fin => ?index fin xs) (integerToFin x n)


text:
normalise : Task a -> State -> ( Task a, State )
-- Combinators
normalise (Seq (Pure v) cont) state =
    normalise (cont v) state
normalise (Seq left cont) state =
    let
    ( newLeft, newState ) = normalise left state
    in
    ( Seq newLeft cont, newState )
normalise (Par (Pure v1) (Pure v2)) state =
    ( Pure ( v1, v2 ), state )
normalise (Par left right) state =
    let
    ( newLeft, newState )    = normalise left state
    ( newRight, newerState ) = normalise right newState
    in
    normalise (Par newLeft newRight) newerState

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module Data.Monoid.Exponentiation

import Data.Nat.Views
import Syntax.PreorderReasoning

%default total

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

public export
linear : Monoid a => a -> Nat -> a
linear v Z = neutral
linear v (S k) = v <+> linear v k

public export
modularRec : Monoid a => a -> HalfRec n -> a
modularRec v HalfRecZ = neutral
modularRec v (HalfRecEven _ acc) = let e = modularRec v acc in e <+> e
modularRec v (HalfRecOdd _ acc) = let e = modularRec v acc in v <+> e <+> e

public export
modular : Monoid a => a -> Nat -> a
modular v n = modularRec v (halfRec n)

infixr 10 ^
public export
(^) : Num a => a -> Nat -> a
(^) = modular @{Multiplicative}

------------------------------------------------------------------------
-- Properties

-- Not using `MonoidV` because it's cursed
export
linearPlusHomo : (mon : Monoid a) =>
  -- good monoid
  (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) ->
  (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) ->
  -- result
  (v : a) -> {m, n : Nat} ->
  (linear v m <+> linear v n) === linear v (m + n)
linearPlusHomo opAssoc neutralL v = go m where

  go : (m : Nat) -> (linear v m <+> linear v n) === linear v (m + n)
  go Z = neutralL
  go (S m) = Calc $
    |~ (v <+> linear v m) <+> linear v n
    ~~ v <+> (linear v m <+> linear v n) ...( opAssoc )
    ~~ v <+> (linear v (m + n))          ...( cong (v <+>) (go m) )

export
modularRecCorrect : (mon : Monoid a) =>
    -- good monoid
  (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) ->
  (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) ->
  -- result
  (v : a) -> {n : Nat} -> (p : HalfRec n) ->
  modularRec v p === linear v n
modularRecCorrect opAssoc neutralL v acc = go acc where

  aux : {m, n : Nat} -> (linear v m <+> linear v n) === linear v (m + n)
  aux = linearPlusHomo opAssoc neutralL v

  go : {n : Nat} -> (p : HalfRec n) -> modularRec v p === linear v n
  go HalfRecZ = Refl
  go (HalfRecEven k acc) = rewrite go acc in aux
  go (HalfRecOdd k acc) = rewrite go acc in Calc $
    |~ (v <+> linear v k) <+> linear v k
    ~~ v <+> (linear v k <+> linear v k)  ...( opAssoc )
    ~~ v <+> (linear v (k + k))           ...( cong (v <+>) aux )

export
modularCorrect : (mon : Monoid a) =>
    -- good monoid
  (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) ->
  (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) ->
  -- result
  (v : a) -> {n : Nat} -> modular v n === linear v n
modularCorrect opAssoc neutralL v
  = modularRecCorrect opAssoc neutralL v (halfRec n)


text:
import Data.Vect
import Decidable.Equality

data Elem : a -> Vect k a -> Type where
     Here : Elem x (x :: xs)
     There : (later : Elem x xs) -> Elem x (y :: xs)

notInNil : Elem value [] -> Void
notInNil Here impossible
notInNil (There _) impossible

notInTail : (notThere : Elem value xs -> Void) ->
            (notHere : (value = x) -> Void) ->
            Elem value (x :: xs) -> Void
notInTail notThere notHere Here = notHere Refl
notInTail notThere notHere (There later) = notThere later

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = No notInNil
isElem value (x :: xs)
    = case decEq value x of
           Yes Refl => Yes Here
           No notHere => case isElem value xs of
                              Yes prf => Yes (There prf)
                              No notThere => No (notInTail notThere notHere)

-- similar example for checking if an element is in a Vect using Booleans
elem : Eq ty => (value : ty) -> (xs : Vect n ty) -> Bool
elem value [] = False
elem value (x :: xs) = case value == x of
                            False => Main.elem value xs
                            True => True


text:
> module Test.API3
> userAPI : Type
>
> map : (f : a -> b)
>     -> List a
>     -> List b
> map g as = ?g
>

ext: lidr


text:
module Main

import Vimscript.FFI
import Vimscript.Builtins

loop : Int -> VIM_IO ()
loop 0 = pure ()
loop n = do
  echo (show n)
  loop (n - 1)

main : VIM_IO ()
main = do
  echo "Hello, Vim!"
  loop 10

-- isolate the "call graph" with v/s:Idris_/d
-- then we have these:
-- function s:Idris_Main_46__123_loop_95_1_125_(loc0,loc1)
--    return s:Idris_Main_46_loop(l:loc2)
-- function s:Idris_Main_46__123_main_95_1_125_(loc0)
--    return s:Idris_Main_46_loop(l:loc1)

max_stars_repo_name: owickstrom/idris-vimscript

max_issues_repo_name: owickstrom/idris-vimscript

max_forks_repo_name: owickstrom/idris-vimscript


text:
import Data.Vect

total add_vec : Num t =>
          (x : Vect cols t) ->
          (y : Vect cols t) ->
          Vect cols t
add_vec [] [] = []
add_vec (x :: xs) (y :: ys) = (x + y) :: add_vec xs ys

total add : Num t =>
      Vect rows ( Vect cols t ) ->
      Vect rows ( Vect cols t ) ->
      Vect rows ( Vect cols t )
add [] [] = []
add (x :: xs) (y :: ys) = add_vec x y :: add xs ys

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

total transposeHelper : (x : Vect n elem) -> (xsTrans : Vect n (Vect k elem)) -> Vect n (Vect (S k) elem)
transposeHelper [] [] = []
transposeHelper (x :: ys) (y :: xs) = (x :: y) :: transposeHelper ys xs

total transpose' : Vect m (Vect n elem) -> Vect n (Vect m elem)
transpose' [] = createEmpties
transpose' (x :: xs) = let xsTrans = transpose' xs in
                          transposeHelper x xsTrans

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Data.Map.AssocList import Data.Map

%access public
%default total

AListMap : Type -> Type -> Type
AListMap k v = List (k,v)

instance Map AListMap where
  empty = Nil
  fromList = id
  toList = id
  listKeys = map fst
  listValues = map snd

  fromVect = List.toList
  toVect xs = (length xs ** Vect.fromList xs)
  vectKeys xs = let xs' = map fst xs in (length xs' ** Vect.fromList xs')
  vectValues xs = let xs' = map snd xs in (length xs' ** Vect.fromList xs')

  grub k xs = map snd $ filter (\x => fst x == k) xs
  lookup k xs = map snd $ find (\x => fst x == k) xs

  insert = (::)
  erase k = filter (\x => fst x /= k)
  eraseBy f = filter (not . f)

max_stars_repo_name: seagull-kamome/idris-toy

max_issues_repo_name: seagull-kamome/idris-toy

max_forks_repo_name: seagull-kamome/idris-toy


text:
module ExtEq

infix 9 =~=

-- Universal (of any order) extensional equality
public export
(=~=) : {ty : Type} -> ty -> ty -> Type
(=~=) {ty = s -> _} a b = (x : s) -> a x =~= b x
(=~=)               a b =            a   =   b

public export
interface Functor m => FunctorExt m where
  0 map_ext : {f, g : a -> b} -> f =~= g -> map {f=m} f =~= map g

export
FunctorExt List where
  map_ext fg [] = ?foo_1
  map_ext fg (x::xs) = let fgx = fg x
                           sub = map_ext fg xs in
                       ?foo_2