text:
module TTImp.Elab.Quote

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.Reflect
import Core.Unify
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.Reflect
import TTImp.TTImp

%default covering

-- Collecting names and terms to let bind for unquoting
data Unq : Type where

-- Collect the escaped subterms in a term we're about to quote, and let bind
-- them first
mutual
  getUnquote : {auto c : Ref Ctxt Defs} ->
               {auto q : Ref Unq (List (Name, FC, RawImp))} ->
               {auto u : Ref UST UState} ->
               RawImp ->
               Core RawImp
  getUnquote (IPi fc c p n arg ret)
      = pure $ IPi fc c p n !(getUnquote arg) !(getUnquote ret)
  getUnquote (ILam fc c p n arg sc)
      = pure $ ILam fc c p n !(getUnquote arg) !(getUnquote sc)
  getUnquote (ILet fc lhsFC c n ty val sc)
      = pure $ ILet fc lhsFC c n !(getUnquote ty) !(getUnquote val) !(getUnquote sc)
  getUnquote (ICase fc sc ty cs)
      = pure $ ICase fc !(getUnquote sc) !(getUnquote ty)
                        !(traverse getUnquoteClause cs)
  getUnquote (ILocal fc ds sc)
      = pure $ ILocal fc !(traverse getUnquoteDecl ds) !(getUnquote sc)
  getUnquote (IUpdate fc ds sc)
      = pure $ IUpdate fc !(traverse getUnquoteUpdate ds) !(getUnquote sc)
  getUnquote (IApp fc f a)
      = pure $ IApp fc !(getUnquote f) !(getUnquote a)
  getUnquote (IAutoApp fc f a)
      = pure $ IAutoApp fc !(getUnquote f) !(getUnquote a)
  getUnquote (INamedApp fc f n a)
      = pure $ INamedApp fc !(getUnquote f) n !(getUnquote a)
  getUnquote (IWithApp fc f a)
      = pure $ IWithApp fc !(getUnquote f) !(getUnquote a)
  getUnquote (IAlternative fc at as)
      = pure $ IAlternative fc at !(traverse getUnquote as)
  getUnquote (IRewrite fc f a)
      = pure $ IRewrite fc !(getUnquote f) !(getUnquote a)
  getUnquote (ICoerced fc t)
      = pure $ ICoerced fc !(getUnquote t)
  getUnquote (IBindHere fc m t)
      = pure $ IBindHere fc m !(getUnquote t)
  getUnquote (IAs fc nameFC u nm t)
      = pure $ IAs fc nameFC u nm !(getUnquote t)
  getUnquote (IMustUnify fc r t)
      = pure $ IMustUnify fc r !(getUnquote t)
  getUnquote (IDelayed fc r t)
      = pure $ IDelayed fc r !(getUnquote t)
  getUnquote (IDelay fc t)
      = pure $ IDelay fc !(getUnquote t)
  getUnquote (IForce fc t)
      = pure $ IForce fc !(getUnquote t)
  getUnquote (IQuote fc t)
      = pure $ IQuote fc !(getUnquote t)
  getUnquote (IUnquote fc tm)
      = do qv <- genVarName "q"
           unqs <- get Unq
           put Unq ((qv, fc, tm) :: unqs)
           pure (IUnquote fc (IVar fc qv)) -- turned into just qv when reflecting
  getUnquote tm = pure tm

  getUnquoteClause : {auto c : Ref Ctxt Defs} ->
                     {auto q : Ref Unq (List (Name, FC, RawImp))} ->
                     {auto u : Ref UST UState} ->
                     ImpClause ->
                     Core ImpClause
  getUnquoteClause (PatClause fc l r)
      = pure $ PatClause fc !(getUnquote l) !(getUnquote r)
  getUnquoteClause (WithClause fc l w prf flags cs)
      = pure $ WithClause
                 fc
                 !(getUnquote l)
                 !(getUnquote w)
                 prf
                 flags
                 !(traverse getUnquoteClause cs)
  getUnquoteClause (ImpossibleClause fc l)
      = pure $ ImpossibleClause fc !(getUnquote l)

  getUnquoteUpdate : {auto c : Ref Ctxt Defs} ->
                     {auto q : Ref Unq (List (Name, FC, RawImp))} ->
                     {auto u : Ref UST UState} ->
                     IFieldUpdate ->
                     Core IFieldUpdate
  getUnquoteUpdate (ISetField p t) = pure $ ISetField p !(getUnquote t)
  getUnquoteUpdate (ISetFieldApp p t) = pure $ ISetFieldApp p !(getUnquote t)

  getUnquoteTy : {auto c : Ref Ctxt Defs} ->
                 {auto q : Ref Unq (List (Name, FC, RawImp))} ->
                 {auto u : Ref UST UState} ->
                 ImpTy ->
                 Core ImpTy
  getUnquoteTy (MkImpTy fc nameFC n t) = pure $ MkImpTy fc nameFC n !(getUnquote t)

  getUnquoteField : {auto c : Ref Ctxt Defs} ->
                    {auto q : Ref Unq (List (Name, FC, RawImp))} ->
                    {auto u : Ref UST UState} ->
                    IField ->
                    Core IField
  getUnquoteField (MkIField fc c p n ty)
      = pure $ MkIField fc c p n !(getUnquote ty)

  getUnquoteRecord : {auto c : Ref Ctxt Defs} ->
                     {auto q : Ref Unq (List (Name, FC, RawImp))} ->
                     {auto u : Ref UST UState} ->
                     ImpRecord ->
                     Core ImpRecord
  getUnquoteRecord (MkImpRecord fc n ps cn fs)
      = pure $ MkImpRecord fc n !(traverse unqPair ps) cn
                           !(traverse getUnquoteField fs)
    where
      unqPair : (Name, RigCount, PiInfo RawImp, RawImp) ->
                Core (Name, RigCount, PiInfo RawImp, RawImp)
      unqPair (n, c, p, t) = pure (n, c, p, !(getUnquote t))

  getUnquoteData : {auto c : Ref Ctxt Defs} ->
                   {auto q : Ref Unq (List (Name, FC, RawImp))} ->
                   {auto u : Ref UST UState} ->
                   ImpData ->
                   Core ImpData
  getUnquoteData (MkImpData fc n tc opts cs)
      = pure $ MkImpData fc n !(getUnquote tc) opts
                         !(traverse getUnquoteTy cs)
  getUnquoteData (MkImpLater fc n tc)
      = pure $ MkImpLater fc n !(getUnquote tc)

  getUnquoteDecl : {auto c : Ref Ctxt Defs} ->
                   {auto q : Ref Unq (List (Name, FC, RawImp))} ->
                   {auto u : Ref UST UState} ->
                   ImpDecl ->
                   Core ImpDecl
  getUnquoteDecl (IClaim fc c v opts ty)
      = pure $ IClaim fc c v opts !(getUnquoteTy ty)
  getUnquoteDecl (IData fc v d)
      = pure $ IData fc v !(getUnquoteData d)
  getUnquoteDecl (IDef fc v d)
      = pure $ IDef fc v !(traverse getUnquoteClause d)
  getUnquoteDecl (IParameters fc ps ds)
      = pure $ IParameters fc
                           !(traverse unqTuple ps)
                           !(traverse getUnquoteDecl ds)
    where
      unqTuple : (Name, RigCount, PiInfo RawImp, RawImp) -> Core (Name, RigCount, PiInfo RawImp, RawImp)
      unqTuple (n, rig, i, t) = pure (n, rig, i, !(getUnquote t))
  getUnquoteDecl (IRecord fc ns v d)
      = pure $ IRecord fc ns v !(getUnquoteRecord d)
  getUnquoteDecl (INamespace fc ns ds)
      = pure $ INamespace fc ns !(traverse getUnquoteDecl ds)
  getUnquoteDecl (ITransform fc n l r)
      = pure $ ITransform fc n !(getUnquote l) !(getUnquote r)
  getUnquoteDecl d = pure d

bindUnqs : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto m : Ref MD Metadata} ->
           {auto u : Ref UST UState} ->
           {auto e : Ref EST (EState vars)} ->
           List (Name, FC, RawImp) ->
           RigCount -> ElabInfo -> NestedNames vars -> Env Term vars ->
           Term vars ->
           Core (Term vars)
bindUnqs [] _ _ _ _ tm = pure tm
bindUnqs ((qvar, fc, esctm) :: qs) rig elabinfo nest env tm
    = do defs <- get Ctxt
         Just (idx, gdef) <- lookupCtxtExactI (reflectionttimp "TTImp") (gamma defs)
              | _ => throw (UndefinedName fc (reflectionttimp "TTImp"))
         (escv, escty) <- check rig elabinfo nest env esctm
                                (Just (gnf env (Ref fc (TyCon 0 0)
                                           (Resolved idx))))
         sc <- bindUnqs qs rig elabinfo nest env tm
         pure (Bind fc qvar (Let fc (rigMult top rig) escv !(getTerm escty))
                    (refToLocal qvar qvar sc))

onLHS : ElabMode -> Bool
onLHS (InLHS _) = True
onLHS _ = False

export
checkQuote : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             {auto e : Ref EST (EState vars)} ->
             RigCount -> ElabInfo ->
             NestedNames vars -> Env Term vars ->
             FC -> RawImp -> Maybe (Glued vars) ->
             Core (Term vars, Glued vars)
checkQuote rig elabinfo nest env fc tm exp
    = do defs <- get Ctxt
         q <- newRef Unq []
         tm' <- getUnquote tm
         qtm <- reflect fc defs (onLHS (elabMode elabinfo)) env tm'
         unqs <- get Unq
         qty <- getCon fc defs (reflectionttimp "TTImp")
         qtm <- bindUnqs unqs rig elabinfo nest env qtm
         fullqtm <- normalise defs env qtm
         checkExp rig elabinfo env fc fullqtm (gnf env qty) exp

export
checkQuoteName : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
                 {auto e : Ref EST (EState vars)} ->
                 RigCount -> ElabInfo ->
                 NestedNames vars -> Env Term vars ->
                 FC -> Name -> Maybe (Glued vars) ->
                 Core (Term vars, Glued vars)
checkQuoteName rig elabinfo nest env fc n exp
    = do defs <- get Ctxt
         qnm <- reflect fc defs (onLHS (elabMode elabinfo)) env n
         qty <- getCon fc defs (reflectiontt "Name")
         checkExp rig elabinfo env fc qnm (gnf env qty) exp

export
checkQuoteDecl : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
                 {auto e : Ref EST (EState vars)} ->
                 RigCount -> ElabInfo ->
                 NestedNames vars -> Env Term vars ->
                 FC -> List ImpDecl -> Maybe (Glued vars) ->
                 Core (Term vars, Glued vars)
checkQuoteDecl rig elabinfo nest env fc ds exp
    = do defs <- get Ctxt
         q <- newRef Unq []
         ds' <- traverse getUnquoteDecl ds
         qds <- reflect fc defs (onLHS (elabMode elabinfo)) env ds'
         unqs <- get Unq
         qd <- getCon fc defs (reflectionttimp "Decl")
         qty <- appCon fc defs (basics "List") [qd]
         checkExp rig elabinfo env fc
                  !(bindUnqs unqs rig elabinfo nest env qds)
                  (gnf env qty) exp


text:
module Text.Show.Diff

import Data.Vect
import Generics.Derive
import public Text.Show.Pretty

%hide Language.Reflection.TT.Name

%language ElabReflection

%default total

--------------------------------------------------------------------------------
--          Diff Data Types
--------------------------------------------------------------------------------

public export
data ValueDiff = Con Name (List ValueDiff)
               | Rec Name (List (Name, ValueDiff))
               | Tuple ValueDiff ValueDiff (List ValueDiff)
               | Lst (List ValueDiff)
               | Same Value
               | Diff Value Value

%runElab derive "ValueDiff" [Generic,Meta]

export
Eq ValueDiff where (==) = assert_total genEq

export
Show ValueDiff where showPrec = assert_total genShowPrec

namespace ValueDiff
  export
  depth : ValueDiff -> Nat
  depth v = case v of
                 (Con x xs)     => S $ maxDepth xs
                 (Rec x xs)     => S $ maxDepthP xs
                 (Tuple x y xs) => S . max (depth x) $ max (depth y) (maxDepth xs)
                 (Lst xs)       => S $ maxDepth xs
                 (Same x)       => 0
                 (Diff x y)     => 0

    where maxDepth : List ValueDiff -> Nat
          maxDepth []       = 0
          maxDepth (h :: t) = max (depth h) (maxDepth t)

          maxDepthP : List (a,ValueDiff) -> Nat
          maxDepthP []           = 0
          maxDepthP ((_,h) :: t) = max (depth h) (maxDepthP t)

public export
data LineDiff = LineSame String
              | LineRemoved String
              | LineAdded String

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

public export
data DocDiff = DocSame Nat String
             | DocRemoved Nat String
             | DocAdded Nat String
             | DocOpen Nat String
             | DocItem Nat String (List DocDiff)
             | DocClose Nat String

%runElab derive "DocDiff" [Generic,Meta]

export
Eq DocDiff where (==) = assert_total genEq

export
Show DocDiff where showPrec = assert_total genShowPrec

namespace DocDiff
  export
  depth : DocDiff -> Nat
  depth v = case v of
                 DocItem _ _ ds => S $ maxDepth ds
                 _              => 1

    where maxDepth : List DocDiff -> Nat
          maxDepth []       = 0
          maxDepth (h :: t) = max (depth h) (maxDepth t)

--------------------------------------------------------------------------------
--          Diffing
--------------------------------------------------------------------------------

-- using the sledgehammer of totality here, since I couldn't satisfy
-- the totality checker otherwise.
valueDiffN : (depth : Nat) -> Value -> Value -> ValueDiff
valueDiffN 0 x y = if x == y then Same x else Diff x y
valueDiffN (S k) x y =
  case (x, y) of
       (Con nx xs, Con ny ys) =>
         if nx == ny  && length xs == length ys
            then Con nx (zipWith (valueDiffN k) xs ys)
            else Diff x y

       (Lst xs, Lst ys) =>
         if length xs == length ys
            then Lst (zipWith (valueDiffN k) xs ys)
            else Diff x y

       (Tuple v1 v2 vs, Tuple w1 w2 ws) =>
         if length vs == length ws
            then Tuple (valueDiffN k v1 w1)
                       (valueDiffN k v2 w2)
                       (zipWith (valueDiffN k) vs ws)
            else Diff x y

       (Rec nx nxs, Rec ny nys) =>
         let ns = map fst nxs
          in if nx == ny && ns == map fst nys
                then Rec nx . zip ns $ zipWith (valueDiffN k)
                                               (map snd nxs)
                                               (map snd nys)
                else Diff x y

       _ => if x == y then Same x else Diff x y

export
valueDiff : Value -> Value -> ValueDiff
valueDiff v w = valueDiffN (depth v `max` depth w) v w

take : (f : Value -> Value -> Value) -> ValueDiff -> Value
take f v = case v of
             Con x xs     => Con x $ ts xs
             Rec x xs     => Rec x $ tsP xs
             Tuple x y xs => Tuple (take f x) (take f y) (ts xs)
             Lst xs       => Lst $ ts xs
             Same x       => x
             Diff x y     => f x y

  where ts : List ValueDiff -> List Value
        ts []       = []
        ts (h :: t) = take f h :: ts t

        tsP : List (a,ValueDiff) -> List (a,Value)
        tsP []           = []
        tsP ((a,h) :: t) = (a,take f h) :: tsP t

export
takeLeft : ValueDiff -> Value
takeLeft = take $ \x,_ => x

export
takeRight : ValueDiff -> Value
takeRight = take $ \_,y => y

oneLiner : Value -> Bool
oneLiner x = case lines (valToStr x) of
               _ :: Nil   => True
               _          => False

removed : (indent: Nat) -> String -> List DocDiff
removed ind = map (DocRemoved ind) . lines

added : (indent: Nat) -> String -> List DocDiff
added ind = map (DocAdded ind) . lines

same : (indent: Nat) -> String -> List DocDiff
same ind = map (DocSame ind) . lines

sameN : (indent: Nat) -> Name -> List DocDiff
sameN ind = same ind . unName

remAdd : (indent : Nat) -> Value -> Value -> List DocDiff
remAdd ind x y = removed ind (valToStr x) ++ added ind (valToStr y)

oneLine : Nat -> ValueDiff -> Lazy (List DocDiff) -> List DocDiff
oneLine ind v dds =
  let x = takeLeft v
      y = takeRight v
   in if oneLiner x && oneLiner y then remAdd ind x y else dds

mkDocDiff : (depth : Nat) -> (indent : Nat) -> ValueDiff -> List DocDiff
mkDocDiff _ ind (Same x)   = same ind (valToStr x)
mkDocDiff _ ind (Diff x y) = remAdd ind x y
mkDocDiff 0 _   _          = []

mkDocDiff (S k) ind v@(Con n xs) =
  oneLine ind v $ sameN ind n ++
                  concatMap (mkDocDiff k (ind + 2)) xs

mkDocDiff (S k) ind v@(Rec n xs) =
  oneLine ind v $ sameN ind n ++
                  [DocOpen ind "{"] ++
                  map (\(nm, x) => DocItem (ind + 2) ", " (sameN 0 (nm <+> " =") ++ mkDocDiff k 2 x)) xs ++
                  [DocClose ind "}"]

mkDocDiff (S k) ind v@(Tuple x y xs) =
  oneLine ind v $ [DocOpen ind "("] ++
                  map (DocItem ind ", " . mkDocDiff k 0) (x::y::xs) ++
                  [DocClose ind ")"]

mkDocDiff (S k) ind v@(Lst xs) =
  oneLine ind v $ [DocOpen ind "["] ++
                  map (DocItem ind ", " . mkDocDiff k 0) xs ++
                  [DocClose ind "]"]

spaces : Nat -> String
spaces ind = fastPack $ replicate ind ' '

mkLineDiff : (d : Nat) -> (ind : Nat) -> String -> DocDiff -> List LineDiff
mkLineDiff 0     _    _    _    = []
mkLineDiff (S k) ind0 pre0 diff =
  case diff of
    DocSame i x    => [LineSame $ mkLinePrefix i ++ x]
    DocRemoved i x => [LineRemoved $ mkLinePrefix i ++ x]
    DocAdded i x   => [LineAdded $ mkLinePrefix i ++ x]
    DocOpen i x    => [LineSame $ mkLinePrefix i ++ x]
    DocClose i x   => [LineSame $ spaces (mkLineIndent i) ++ x]
    DocItem _ _ [] => []
    DocItem i p (x@(DocRemoved _ _) :: y@(DocAdded _ _) :: xs) =>
      mkLineDiff k (mkLineIndent i) p x ++
      mkLineDiff k (mkLineIndent i) p y ++
      concatMap (mkLineDiff k (mkLineIndent (i + length p)) "") xs

    DocItem i p (x :: xs) =>
      mkLineDiff k (mkLineIndent i) p x ++
      concatMap (mkLineDiff k (mkLineIndent (i + length p)) "") xs

  where mkLinePrefix : Nat -> String
        mkLinePrefix ind = spaces ind0 ++ pre0 ++ spaces ind

        mkLineIndent : Nat -> Nat
        mkLineIndent ind = ind0 + length pre0 + ind

collapseOpen : List DocDiff -> List DocDiff
collapseOpen (DocSame ind l :: DocOpen _ bra :: xs) =
  DocSame ind (l ++ " " ++ bra) :: collapseOpen xs
collapseOpen (DocItem ind pre xs :: ys) =
  DocItem ind pre (collapseOpen xs) :: collapseOpen ys
collapseOpen (x :: xs) = x :: collapseOpen xs
collapseOpen [] = []

dropLeadingSep : List DocDiff -> List DocDiff
dropLeadingSep (DocOpen oind bra :: DocItem ind pre xs :: ys) =
  DocOpen oind bra :: DocItem (ind + length pre) "" (dropLeadingSep xs) :: dropLeadingSep ys
dropLeadingSep (DocItem ind pre xs :: ys) =
  DocItem ind pre (dropLeadingSep xs) :: dropLeadingSep ys
dropLeadingSep (x :: xs) = x :: dropLeadingSep xs
dropLeadingSep [] = []

export
toLineDiff : ValueDiff -> List LineDiff
toLineDiff v =
  concatMap (\d => mkLineDiff (depth d) 0 "" d) .
  collapseOpen .
  dropLeadingSep $
  mkDocDiff (depth v) 0 v

export
lineDiff : Value -> Value -> List LineDiff
lineDiff x y = toLineDiff $ valueDiff x y

export
renderLineDiff : LineDiff -> String
renderLineDiff (LineSame x)    = "  " ++ x
renderLineDiff (LineRemoved x) = "- " ++ x
renderLineDiff (LineAdded x)   = "+ " ++ x

export
renderValueDiff : ValueDiff -> String
renderValueDiff = unlines . map renderLineDiff . toLineDiff

ext: idr


text:
import public Peer

main : IO ()
main = peerStart

max_stars_repo_name: AsmusAB/Idris-peer-to-peer-network

max_issues_repo_name: AsmusAB/Idris-peer-to-peer-network

max_forks_repo_name: AsmusAB/Idris-peer-to-peer-network


text:
module Main

import Data.Vect

data DataStore : Type where
     MkData : (size : Nat) -> (items : Vect size String) -> DataStore

size : DataStore -> Nat
size (MkData size' items') = size'

items : (store : DataStore) -> Vect (size store) String
items (MkData size' items') = items'

addToStore : DataStore -> String -> DataStore
addToStore (MkData size store) newitem = MkData _ (addToData store)
  where
    addToData : Vect oldsize String -> Vect (S oldsize) String
    addToData [] = [newitem]
    addToData (x :: xs) = x :: addToData xs

data Command = Add String
             | Get Integer
             | Quit

parseCommand : String -> String -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" val = case all isDigit (unpack val) of
                              False => Nothing
                              True => Just (Get (cast val))
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

parse : (input : String) -> Maybe Command
parse input = case span (/= ' ') input of
                   (cmd, args) => parseCommand cmd (ltrim args)

getEntry : (pos : Integer) -> (store : DataStore) ->
           Maybe (String, DataStore)
getEntry pos store
    = let store_items = items store in
          case integerToFin pos (size store) of
               Nothing => Just ("Out of range\n", store)
               Just id => Just (index id (items store) ++ "\n", store)

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
    = case parse input of
           Nothing => Just ("Invalid command\n", store)
           Just (Add item) =>
              Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
           Just (Get pos) => getEntry pos store
           Just Quit => Nothing

main : IO ()
main = replWith (MkData _ []) "Command: " processInput

max_stars_repo_name: Nikolaj-K/idris

max_issues_repo_name: Nikolaj-K/idris

max_forks_repo_name: Nikolaj-K/idris


text:
module TyTTP.Adapter.Node.Static

import Data.Buffer
import Data.Maybe
import Data.Mime.Apache
import Data.List
import Control.Monad.Either
import Node.Error
import Node.FS
import Node.FS.Stats
import Node.FS.Stream
import TyTTP.Adapter.Node.Error
import TyTTP.Adapter.Node.HTTP
import TyTTP.HTTP
import TyTTP.URL
import TyTTP.URL.Path

public export
Resource : Type
Resource = String

public export
data FileServingError : Type where
  StatError : Error e => e -> FileServingError
  NotAFile : Resource -> FileServingError

public export
StaticRequest : (e : Type) -> Type -> Type
StaticRequest e url = Context Method url StringHeaders Status StringHeaders (Publisher IO e Buffer) ()

public export
StaticResponse : (e : Type) -> Type -> Type
StaticResponse e url = Context Method url StringHeaders Status StringHeaders (Publisher IO e Buffer) (Publisher IO e Buffer)

record StaticSuccesResult (e : Type) where
  constructor MkStaticSuccessResult
  size : Int
  stream : Publisher IO e Buffer
  mime : Mime

export
hStatic : Error e
  => HasIO io
  => (folder : String)
  -> (returnError : FileServingError
    -> StaticRequest e (URL a Path s)
    -> io $ StaticResponse e (URL a Path s)
  )
  -> (ctx : StaticRequest e (URL a Path s))
  -> io $ StaticResponse e (URL a Path s)
hStatic folder returnError ctx = eitherT (flip returnError ctx) returnSuccess $ do
    let resource = ctx.request.url.path.rest
        file = "\{folder}\{resource}"

    fs <- FS.require
    Right stats <- stat_sync StatsInt file
      | Left e => throwError $ case code e of
         SystemError ENOENT => NotAFile resource
         _ => StatError e

    True <- pure $ stats.isFile
      | _ => throwError $ NotAFile resource

    False <- pure $ stats.isDirectory
      | _ => throwError $ NotAFile resource

    readStream <- createReadStream file

    pure $ MkStaticSuccessResult
            { size = Stats.size stats
            , stream = MkPublisher $ \s => do
                readStream.onData  s.onNext
                readStream.onEnd   s.onSucceded
                readStream.onError s.onFailed
            , mime = mimeOf file
            }

  where
    returnSuccess : Error e => StaticSuccesResult e -> io $ StaticResponse e (URL a Path s)
    returnSuccess result = do
      let hs = [ ("Content-Length", show $ result.size)
               , ("Content-Type", show $ result.mime)
               ]
      pure $ { response.status := OK
             , response.headers := hs
             , response.body := result.stream } ctx

    extensionOf' : (ext: List Char) -> (file: List Char) -> (dot: Bool) -> Maybe (List Char)
    extensionOf' ext ('.' :: xs) _ = extensionOf' xs xs True
    extensionOf' ext (x :: xs) dot = extensionOf' ext xs dot
    extensionOf' ext [] True = Just ext
    extensionOf' ext [] False = Nothing

    extensionOf : String -> Maybe String
    extensionOf file = let l = unpack file in
                           map pack $ extensionOf' l l False

    mimeOf : String -> Mime
    mimeOf file =
      fromMaybe TEXT_PLAIN $
        flip lookup extensions =<< extensionOf file

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module PQ.FFI.Types

import Generics.Derive

%default total
%language ElabReflection

--------------------------------------------------------------------------------
--          ConnStatusType
--------------------------------------------------------------------------------

||| `ConnStatusType` from `libpq-fe.h` but without the
||| `CONNECTION_` prefix.
public export
data ConnStatusType =
    OK
  | BAD
  | STARTED
  | MADE
  | AWAITING_RESPONSE
  | AUTH_OK
  | SETENV
  | SSL_STARTUP
  | NEEDED
  | CHECK_WRITABLE
  | CONSUME
  | GSS_STARTUP
  | CHECK_TARGET
  | CONN_STATUS_OTHER Bits8

%runElab derive "ConnStatusType" [Generic,Meta,Show,Eq,Ord]

namespace ConnStatusType
  public export
  fromBits8 : Bits8 -> ConnStatusType
  fromBits8  0 = OK
  fromBits8  1 = BAD
  fromBits8  2 = STARTED
  fromBits8  3 = MADE
  fromBits8  4 = AWAITING_RESPONSE
  fromBits8  5 = AUTH_OK
  fromBits8  6 = SETENV
  fromBits8  7 = SSL_STARTUP
  fromBits8  8 = NEEDED
  fromBits8  9 = CHECK_WRITABLE
  fromBits8 10 = CONSUME
  fromBits8 11 = GSS_STARTUP
  fromBits8 12 = CHECK_TARGET
  fromBits8  n = CONN_STATUS_OTHER n

--------------------------------------------------------------------------------
--          ExecStatusType
--------------------------------------------------------------------------------

public export
data ExecStatusType =
    EMPTY_QUERY
  | COMMAND_OK
  | TUPLES_OK
  | COPY_OUT
  | COPY_IN
  | BAD_RESPONSE
  | NONFATAL_ERROR
  | FATAL_ERROR
  | COPY_BOTH
  | SINGLE_TUPLE
  | EXEC_STATUS_OTHER Bits8

%runElab derive "ExecStatusType" [Generic,Meta,Show,Eq,Ord]

namespace ExecStatusType
  public export
  fromBits8 : Bits8 -> ExecStatusType
  fromBits8 0 = EMPTY_QUERY
  fromBits8 1 = COMMAND_OK
  fromBits8 2 = TUPLES_OK
  fromBits8 3 = COPY_OUT
  fromBits8 4 = COPY_IN
  fromBits8 5 = BAD_RESPONSE
  fromBits8 6 = NONFATAL_ERROR
  fromBits8 7 = FATAL_ERROR
  fromBits8 8 = COPY_BOTH
  fromBits8 9 = SINGLE_TUPLE
  fromBits8 n = EXEC_STATUS_OTHER n

--------------------------------------------------------------------------------
--          Errors
--------------------------------------------------------------------------------

public export
data SQLError : Type where
  ConnectionError : (type : ConnStatusType) -> (msg : String) -> SQLError

  ExecError       : (type : ExecStatusType) -> (msg : String) -> SQLError

  QueryError      :  (expectedNumerOfColumns : Bits32)
                  -> (numberOfColumns : Bits32)
                  -> SQLError

  ReadError       :  (name   : String)
                  -> (row    : Bits32)
                  -> (column : Bits32)
                  -> (value  : String)
                  -> SQLError

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


text:
module Example.Pil.Gen

import Data.List

import public Example.DecEq'
import public Example.Gen
import public Example.Pil

%default total

------------------
--- Generation ---
------------------

--- Expressions ---

export
constExprGen : Gen a -> Gen (Expression ctx a)
constExprGen = map C

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

export
varExprGen' : {a : Type} -> {ctx : Context} -> DecEq' Type => List (Expression ctx a)
varExprGen' = varExpressions {- this could be `oneOf $ map pure (fromList varExpressions)` if `Gen` could fail (contain zero) -} where
  varExpressions : List (Expression ctx a)
  varExpressions = map varExpr varsOfType where
    varExpr : (n : Name ** lk : Lookup n ctx ** reveal lk = a) -> Expression ctx a
    varExpr (n ** _ ** prf) = rewrite sym prf in V n

    varsOfType : List (n : Name ** lk : Lookup n ctx ** reveal lk = a)
    varsOfType = varsOfTypeOfCtx $ addLookups ctx
      where
        addLookups : (ctx : Context) -> List (n : Name ** ty : Type ** lk : Lookup n ctx ** reveal lk = ty)
        addLookups [] = []
        addLookups ((n, ty)::xs) = (n ** ty ** Here ty ** Refl) ::
                                   map (\(n ** ty ** lk ** lk_ty) => (n ** ty ** There lk ** lk_ty)) (addLookups xs)

        varsOfTypeOfCtx : List (n : Name ** ty : Type ** lk : Lookup n ctx ** reveal lk = ty) -> List (n : Name ** lk : Lookup n ctx ** reveal lk = a)
        varsOfTypeOfCtx [] = []
        varsOfTypeOfCtx ((n ** ty ** lk ** lk_ty)::xs) = maybeToList varX ++ varsOfTypeOfCtx xs where
          varX : Maybe (n : Name ** lk : Lookup n ctx ** reveal lk = a)
          varX = case decEq' ty a of
            (Yes ty_a) => Just (n ** lk ** trans lk_ty ty_a)
            No => Nothing

export
unaryExprGen : Gen (a -> a) -> Gen (Expression ctx a) -> Gen (Expression ctx a)
unaryExprGen gg sub = U <$> gg <*> sub

export
binaryExprGen : Gen (a -> a -> a) -> Gen (Expression ctx a) -> Gen (Expression ctx a)
binaryExprGen ggg sub = B <$> ggg <*> sub <*> sub

commonGens : {a : Type} -> {ctx : Context} -> Gen a -> DecEq' Type => (n ** Vect n $ Gen $ Expression ctx a)
commonGens g = ( _ ** [constExprGen g] ++ map pure (fromList varExprGen') )

export
exprGen : (szBound : Nat) -> {a : Type} -> Gen a -> Gen (a -> a) -> Gen (a -> a -> a) -> {ctx : Context} -> DecEq' Type => Gen (Expression ctx a)
exprGen Z g _ _ = oneOf $ snd $ commonGens g
exprGen (S n) g gg ggg = oneOf $ snd (commonGens g) ++
                               [ unaryExprGen gg (exprGen n g gg ggg)
                               , binaryExprGen ggg (exprGen n g gg ggg)
                               ]

--- Statements ---

lookupGen : (ctx : Context) -> NonEmpty ctx => Gen (n : Name ** Lookup n ctx)
lookupGen ctx = let (lks@(_::_) ** _) = mapLk ctx in
                oneOf $ map pure $ fromList lks
  where
    mapLk : (ctx : Context) -> NonEmpty ctx => (l : List (n : Name ** Lookup n ctx) ** NonEmpty l)
    mapLk [(n, ty)] = ( [(n ** Here ty)] ** IsNonEmpty )
    mapLk ((n, ty)::xs@(_::_)) = ( (n ** Here ty) :: map (\(n ** lk) => (n ** There lk)) (fst $ mapLk xs) ** IsNonEmpty )

mutual

  export
  covering
  noDeclStmtGen : (ctx : Context) ->
                  Gen Type =>
                  Gen Name =>
                  (genExpr : {a : Type} -> {ctx : Context} -> Gen (Expression ctx a)) =>
                  Gen (Statement ctx ctx)
  noDeclStmtGen ctx = oneOf
    [ pure nop
    , case ctx of
      []     => pure nop -- this is returned because `oneOf` requires `Vect`, thus all cases must have equal size.
      (_::_) => do (n ** _) <- lookupGen ctx
                   pure $ n #= !genExpr
    , do (inside_for ** init) <- stmtGen ctx
         (_ ** body) <- stmtGen inside_for
         pure $ for init !genExpr !(noDeclStmtGen inside_for) body
    , pure $ if__ !genExpr (snd !(stmtGen ctx)) (snd !(stmtGen ctx))
    , pure $ !(noDeclStmtGen ctx) *> !(noDeclStmtGen ctx)
    , pure $ block $ snd !(stmtGen ctx)
    , pure $ print !(genExpr {a=String})
    ]

  export
  covering
  stmtGen : (pre : Context) ->
            (genTy : Gen Type) =>
            (genName : Gen Name) =>
            ({a : Type} -> {ctx : Context} -> Gen (Expression ctx a)) =>
            Gen (post ** Statement pre post)
  stmtGen pre = oneOf
    [ do s <- noDeclStmtGen pre
         pure (pre ** s)
    , do ty <- genTy
         n <- genName
         pure ((n, ty)::pre ** ty. n)
    , do (mid ** l) <- stmtGen pre
         (post ** r) <- stmtGen mid
         pure (post ** l *> r)
    ]

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
module Data.List.Predicates.Unique

import Data.List

%access public export
%default total

||| Proof that a list `xs` is unique.
data Unique : (xs : List type) -> Type where

  ||| Empty lists are 'unique'
  Empty : Unique Nil

  ||| Only add an element to the list is it doesn't appear in the
  ||| remaining lists.
  Cons : (x : type)
      -> (prfU : Not (Elem x xs))
      -> (rest : Unique xs)
      -> Unique (x::xs)

-- ----------------------------------------------------------------- [ Helpers ]
duplicateElement : (prf : Elem x xs) -> Unique (x :: xs) -> Void
duplicateElement prf (Cons x f rest) = f prf

restNotUnique : (f : Unique xs -> Void) -> (contra : Elem x xs -> Void) -> Unique (x :: xs) -> Void
restNotUnique f contra (Cons x g rest) = f rest

||| Is the list `xs` unique?
unique : DecEq type
      => (xs : List type)
      -> Dec (Unique xs)
unique [] = Yes Empty
unique (x :: xs) with (isElem x xs)
  unique (x :: xs) | (Yes prf) = No (duplicateElement prf)
  unique (x :: xs) | (No contra) with (unique xs)
    unique (x :: xs) | (No contra) | (Yes prf) = Yes (Cons x contra prf)
    unique (x :: xs) | (No contra) | (No f) = No (restNotUnique f contra)

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
%foreign "javascript:lambda: (x) => console.log('ok')"
prim__ok : Double -> PrimIO ()

main : HasIO io => io ()
main = do
    primIO $ prim__ok 0
    primIO $ prim__ok 99
    primIO $ prim__ok 100
    primIO $ prim__ok (-1)
    primIO $ prim__ok 1234567890


text:
import Data.Vect

-- validConv : (Num t) => Vect (m + n) t -> Vect m t -> Vect (n + 1) t
-- validConv xs w = fromList [sum (window i (length w) xs) | i <- [0..length(xs)-length(w)]]

window : (i : Nat) -> (m : Nat) -> Vect (i + (m + n)) t -> Vect m t
window i m xs = take m (drop i xs)

-- xs : Vect 5 Int
-- xs = [1,2,3,4,5]

-- ys : List (Vect 3 Int)
-- ys = [window i 3 xs | i <- [1,3]]


text:
> module Functor.tests.Main

> import Control.Monad.Identity

> import Functor.Operations
> import Identity.Properties

> %default total
> %auto_implicits off

> b : Bool
> b = elem Z (Id Z)

> B : Type
> B = Elem (S Z) (Id Z)

> b' : Bool
> b' = decAsBool (decElem (S Z) (Id Z))

> main : IO ()
> main = do putStrLn ("b  = " ++ show b)
>           putStrLn ("b' = " ++ show b')

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
> module PNat.Properties

> import Syntax.PreorderReasoning

> import PNat.PNat
> import PNat.Operations
> import Nat.Positive
> import Unique.Predicates
> import Subset.Properties
> import Nat.LTProperties
> import Pairs.Operations

> %default total
> %access export

> ||| PNat is an implementation of DecEq
> implementation DecEq PNat where
>   decEq (Element m pm) (Element n pn) with (decEq m n)
>     | (Yes prf) = Yes (subsetEqLemma1 (Element m pm) (Element n pn) prf PositiveUnique)
>     | (No contra) = No (\ prf => contra (getWitnessPreservesEq prf))

> ||| PNat is an implementation of Show
> implementation Show PNat where
>   show = show . toNat

> |||
> predToNatLemma : (x : PNat) -> S (pred x) = toNat x
> predToNatLemma (Element _ (MkPositive {n})) = Refl

> |||
> toNatfromNatLemma : (m : Nat) -> (zLTm : Z `LT` m) -> toNat (fromNat m zLTm) = m
> {-
> toNatfromNatLemma  Z zLTz = absurd zLTz
> toNatfromNatLemma (S m) _ = Refl
> ---}
> --{-
> toNatfromNatLemma m zLTm = Refl
> ---}

> |||
> toNatLTLemma : (x : PNat) -> Z `LT` toNat x
> toNatLTLemma x = s2 where
>   s1 : Z `LT` (S (pred x))
>   s1 = ltZS (pred x)
>   s2 : Z `LT` (toNat x)
>   s2 = replace (predToNatLemma x) s1

> |||
> toNatEqLemma : {x, y : PNat} -> (toNat x) = (toNat y) -> x = y
> toNatEqLemma {x} {y} p = subsetEqLemma1 x y p PositiveUnique

> |||
> -- toNatMultLemma : {x, y : PNat} -> toNat (x * y) = (toNat x) * (toNat y)
> toNatMultLemma : {x, y : PNat} -> toNat (x * y) = (toNat x) * (toNat y)
> toNatMultLemma {x = (Element m pm)} {y = (Element n pn)} = Refl

> |||
> multOneRightNeutral : (x : PNat) -> x * (Element 1 MkPositive) = x
> multOneRightNeutral (Element m pm) =
>     ( (Element m pm) * (Element 1 MkPositive) )
>   ={ Refl }=
>     ( Element (m * 1) (multPreservesPositivity pm MkPositive) )
>   ={ toNatEqLemma (multOneRightNeutral m) }=
>     ( Element m pm )
>   QED

> |||
> multCommutative : (x : PNat) -> (y : PNat) -> x * y = y * x
> multCommutative (Element m pm) (Element n pn) =
>   let pmn = multPreservesPositivity pm pn in
>   let pnm = multPreservesPositivity pn pm in
>     ( Element (m * n) pmn )
>   ={ toNatEqLemma (multCommutative m n) }=
>     ( Element (n * m) pnm )
>   QED

> |||
> multAssociative : (x : PNat) -> (y : PNat) -> (z : PNat) ->
>                   x * (y * z) = (x * y) * z
> multAssociative (Element m pm) (Element n pn) (Element o po) =
>   let pno   = multPreservesPositivity pn po  in
>   let pmno  = multPreservesPositivity pm pno in
>   let pmn   = multPreservesPositivity pm pn  in
>   let pmno' = multPreservesPositivity pmn po in
>     ( (Element m pm) * ((Element n pn) * (Element o po)) )
>   ={ Refl }=
>     ( (Element m pm) * (Element (n * o) pno) )
>   ={ Refl }=
>     ( Element (m * (n * o)) pmno )
>   ={ toNatEqLemma (multAssociative m n o) }=
>     ( Element ((m * n) * o) pmno' )
>   ={ Refl }=
>     ( (Element (m * n) pmn) * (Element o po) )
>   ={ Refl }=
>     ( ((Element m pm) * (Element n pn)) * (Element o po) )
>   QED

> {-

> ---}


text:
module AutoHotkey.Builtins

import AutoHotkey.FFI

%access public export

||| Call an AutoHotkey command.
%inline
call_command : String -> (ty : Type) -> {auto fty : FTy FFI_AHK [] ty} -> ty
call_command name =
  foreign FFI_AHK (AHK_Command name)

%inline
msgBox : String -> AHK_IO ()
msgBox = call_command "MsgBox" (String -> AHK_IO ())

max_stars_repo_name: joedf/idris-autohotkey

max_issues_repo_name: joedf/idris-autohotkey

max_forks_repo_name: joedf/idris-autohotkey


text:
module Hoare

-- Based on http://eprints.nottingham.ac.uk/10779/1/Thesis.pdf

Pre : Type -> Type
Pre s = s -> Type

Post : Type -> Type -> Type
Post s a = s -> a -> s -> Type

HoareState : (s : Type) -> Pre s -> (a : Type) -> Post s a -> Type
HoareState s pre a post = (d : DPair s pre) -> DPair (a, s) (\(x, f) => post (fst d) x f)

return : {a : Type} -> (x : a) -> HoareState s (\_ => ()) a (\i, y, f => (i = f, x = y))
return x (st ** ()) = ((x, st) ** (Refl, Refl))

(>>=) : {p1 : Pre s} -> {q1 : Post s a} -> {p2 : a -> Pre s} -> {q2 : a -> Post s b} ->
        HoareState s p1 a q1 ->
        ((x : a) -> HoareState s (p2 x) b (q2 x)) ->
        HoareState s (\s1 => (p1 s1, ((x : a) -> (s2 : s) -> q1 s1 x s2 -> p2 x s2))) b
                     (\s1, x, s3 => DPair (a, s) (\(y,s2) => (q1 s1 y s2, q2 y s2 x s3)))
(>>=) c1 c2 (s1 ** (s1p1, f)) = let ((x, s2) ** p) = (c1 (s1 ** s1p1)) in
                                let ((y, s3) ** q) = c2 x (s2 ** (f x s2 p)) in
                                ((y, s3) ** ((x, s2) ** (p, q)))

get : HoareState s (\_ => ()) s (\i, x, f => (i = f, x = i))
get (st ** ()) = ((st, st) ** (Refl, Refl))

put : (st : s) -> HoareState s (\_ => ()) () (\i, x, f => f = st)
put st _ = (((), st) ** Refl)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Control.Monad.Indexed.State

import Control.Functor.Indexed
import Control.Applicative.Indexed
import Control.Monad.Indexed
import Control.Monad.Indexed.Do

||| Support for wrapping an IndexedMonad in another stateful
||| Monad.
||| The order of the parameters may seem odd compared to other
||| StateT types, but the ordering is such that an IndexedMonad
||| type can be elevated to a TransitionIndexedMonad type without
||| much refactoring.
public export
record IndexedStateT stateType x y (m : Type -> x -> y -> Type) a (i : x) (j : y) where
  constructor ST
  runStateT' : stateType -> m (stateType, a) i j

public export
%inline
runStateT : stateType -> IndexedStateT stateType x y m a i j -> m (stateType, a) i j
runStateT s act = runStateT' act s

public export
%inline
evalStateT : IndexedFunctor x y m => stateType -> IndexedStateT stateType x y m a i j -> m a i j
evalStateT s = map snd . runStateT s

public export
%inline
execStateT : IndexedFunctor x y m => stateType -> IndexedStateT stateType x y m a i j -> m stateType i j
execStateT s = map fst . runStateT s

public export
%inline
mapStateT : ({0 i : x} -> {0 j : y} -> m (s, a) i j -> n (s, b) i j) -> IndexedStateT s x y m a i j -> IndexedStateT s x y n b i j
mapStateT f m = ST $ f . runStateT' m

public export
lift : IndexedFunctor x y m => m a i j -> IndexedStateT stateType x y m a i j
lift z = ST $ \st => map (st,) z

implementation IndexedFunctor x y f => IndexedFunctor x y (IndexedStateT stateType x y f) where
  map f' (ST runStateT') = ST $ \st => map (mapSnd f') $ runStateT' st

public export
IndexedMonad z m => IndexedApplicative z (IndexedStateT stateType z z m) where
  pure x = ST $ \st => pure (st, x)

  (ST ff) `ap` (ST fx) = ST $ \st =>
                          ff st >>>= \(st', f) =>
                            fx st' >>>= \(st'', x) =>
                              pure (st'', f x)

public export
IndexedMonad z m => IndexedMonad z (IndexedStateT stateType z z m) where
  bind (ST f) g = ST $ \st =>
               f st >>>= \(st', x) =>
                 runStateT st' (g x)

public export
get : IndexedApplicative z m => IndexedStateT stateType z z m stateType i i
get = ST $ \st => pure (st, st)

public export
gets : IndexedApplicative z m => (stateType -> a) -> IndexedStateT stateType z z m a i i
gets f = ST $ \st => pure (st, f st)

public export
put : IndexedApplicative z m => stateType -> IndexedStateT stateType z z m () i i
put st = ST $ \_ => pure (st, ())

public export
modify : IndexedMonad z m => (stateType -> stateType) -> IndexedStateT stateType z z m () i i
modify f = do
  x <- get
  put (f x)

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
-- Find the difference between the sum of the squares of the first one hundred natural numbers and the square of the sum.

sumOfSquares : Int -> Int
sumOfSquares n = sum (map (\x => x*x) [1..n])

squareOfSums : Int -> Int
squareOfSums n = (\x => x*x) (sum [1..n])

main : IO ()
main = print ((squareOfSums 100) - (sumOfSquares 100))

max_stars_repo_name: edu-di-wu/project-euler

max_issues_repo_name: edu-di-wu/project-euler

max_forks_repo_name: edu-di-wu/project-euler


text:
||| Copyright 2016 Google Inc.
|||
||| Licensed under the Apache License, Version 2.0 (the "License");
||| you may not use this file except in compliance with the License.
||| You may obtain a copy of the License at
|||
|||     http://www.apache.org/licenses/LICENSE-2.0
|||
||| Unless required by applicable law or agreed to in writing, software
||| distributed under the License is distributed on an "AS IS" BASIS,
||| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
||| See the License for the specific language governing permissions and
||| limitations under the License.
|||
||| This module parses protocol descriptor files and parses them into protocol
||| buffer descriptors (TODO: create a file descriptor that contains multiple
||| messages).
|||
||| This module can be used together with Idris' type provider language
||| extension, to parse protocol message descriptions from files at compile
||| time and construct types based on them.

module Protobuf.Parser

import Data.String
import Control.Monad.State

import Lightyear
import Lightyear.Char
import Lightyear.Strings
import Lightyear.Combinators

import Protobuf.Core

record ParserState where
  constructor MkParserState
  scope : String
  messages : List MessageDescriptor
  enums : List EnumDescriptor

ProtoParser : Type -> Type
ProtoParser = ParserT String (State ParserState)

addMessage : MessageDescriptor -> ProtoParser ()
addMessage msg = do {
  (MkParserState scope messages enums) <- get
  put (MkParserState scope (messages ++ [msg]) enums)
}

addEnum : EnumDescriptor -> ProtoParser ()
addEnum enum = do {
  (MkParserState scope messages enums) <- get
  put (MkParserState scope messages (enums ++ [enum]))
}

||| Pushes a name to the scope and returns the original scope.
pushScope : String -> ProtoParser String
pushScope name = do {
  (MkParserState scope messages enums) <- get
  put (MkParserState (scope ++ name ++ ".") messages enums)
  return scope
}

getScope : ProtoParser String
getScope = do {
  (MkParserState scope messages enums) <- get
  return scope
}

setScope : String -> ProtoParser ()
setScope scope = do {
  (MkParserState _ messages enums) <- get
  put (MkParserState scope messages enums)
}

requiredSpace : ProtoParser ()
requiredSpace = space *> spaces *> return ()

label : ProtoParser Label
label = (char 'o' >! string "ptional" *> requiredSpace *> return Optional)
    <|> (string "req" >! string "uired" *> requiredSpace *> return Required)
    <|> (string "rep" >! string "eated" *> requiredSpace *> return Repeated)
    <?> "Label"

isIdentifierChar : Char -> Bool
isIdentifierChar c = (isAlpha c) || (isDigit c) || c == '_' || c == '.'

identifier : ProtoParser String
identifier = (map pack (some (satisfy isIdentifierChar))) <* spaces

nothingToErr : (errMsg : String) -> Maybe a -> ProtoParser a
nothingToErr errMsg = maybe (fail errMsg) return

nonNegative : ProtoParser Int
nonNegative = do {
  digits <- some (satisfy isDigit)
  nothingToErr "Could not parse digits" (parsePositive (pack digits))
}

listToVect : List a -> (k : Nat ** Vect k a)
listToVect Nil = (Z ** Nil)
listToVect (x::xs) = let (k ** xs') = listToVect xs in
  (S k ** (x :: xs'))

enumValueDescriptor : ProtoParser EnumValueDescriptor
enumValueDescriptor = do {
  name <- identifier
  token "="
  number <- nonNegative
  token ";"
  return (MkEnumValueDescriptor name number)
}

enumDescriptor : ProtoParser ()
enumDescriptor = (token "enum") *!> (do {
  name <- identifier
  values <- braces (many (enumValueDescriptor))
  (k ** values') <- return (listToVect values)
  scope <- getScope
  addEnum (MkEnumDescriptor (scope ++ name) values')
})

messageType : ProtoParser FieldValueDescriptor
messageType = do {
  msgName <- identifier
  state <- get
  case (find (\x => name x == msgName) (messages state)) of
    Nothing => fail $ "A message type (no message named " ++ msgName ++ ")"
    Just msg => return (PBMessage msg)
}

enumType : ProtoParser FieldValueDescriptor
enumType = do {
  enumName <- identifier
  state <- get
  case (find (\x => name x == enumName) (enums state)) of
    Nothing => fail $ "An enum type (no enum named " ++ enumName ++ ")"
    Just enum => return (PBEnum enum)
}

fieldValueDescriptor : ProtoParser FieldValueDescriptor
fieldValueDescriptor = (token "double" *!> return PBDouble)
                    <|> (token "float" *!> return PBFloat)
                    <|> (token "int32" *!> return PBInt32)
                    <|> (token "int64" *!> return PBInt64)
                    <|> (token "uint32" *!> return PBUInt32)
                    <|> (token "uint64" *!> return PBUInt64)
                    <|> (token "sint32" *!> return PBSInt32)
                    <|> (token "sint64" *!> return PBSInt64)
                    <|> (token "fixed32" *!> return PBFixed32)
                    <|> (token "fixed64" *!> return PBFixed64)
                    <|> (token "sfixed32" *!> return PBSFixed32)
                    <|> (token "sfixed64" *!> return PBSFixed64)
                    <|> (token "bool" *!> return PBBool)
                    <|> (token "string" *!> return PBString)
                    <|> (token "bytes" *!> return PBBytes)
                    <|> messageType
                    <|> enumType
                    <?> "The name of a message, enum or primitive type"

fieldDescriptor : ProtoParser FieldDescriptor
fieldDescriptor = do {
  l <- label
  ty <- fieldValueDescriptor
  name <- identifier
  token "="
  number <- nonNegative
  token ";"
  return (MkFieldDescriptor l ty name number)
}

messageDescriptor : ProtoParser ()
messageDescriptor = (token "message") *!> (do {
  name <- identifier
  scope <- pushScope name
  -- Parse fields and nested enum and message descriptors
  fields <- braces (many ((fieldDescriptor >>= return . Just)
                      <|> (messageDescriptor *> return Nothing)
                      <|> (enumDescriptor *> return Nothing)))
  setScope scope
  (k ** fields') <- return (listToVect (mapMaybe (\x => x) fields))
  addMessage (MkMessageDescriptor (scope ++ name) fields')
})

fileDescriptor : ProtoParser ()
fileDescriptor = (many (messageDescriptor <|> enumDescriptor)) *> eof

runParser : String -> Either String ParserState
runParser input = case output of
    Success _ x => Right x
    Failure es  => Left $ formatError input es
  where output : Result String ParserState
        output = evalState
          (execParserT (spaces *> fileDescriptor *> get) input)
          (MkParserState "" [] [])

export parseFile : String -> Either String (List MessageDescriptor, List EnumDescriptor)
parseFile input = case runParser input of
  Left err => Left err
  Right (MkParserState scope messages enums) => Right (messages, enums)

max_stars_repo_name: google/idris-protobuf

max_issues_repo_name: google/idris-protobuf

max_forks_repo_name: google/idris-protobuf


text:
module Chapter4

import TypesAndFunctions
import Naturality

%default total

Exercise_4_1_1_not : Bool -> Bool
Exercise_4_1_1_not b = if b then False else True

Exercise_4_1_1_id : Bool -> Bool
Exercise_4_1_1_id b = b

Exercise_4_1_1_const_true : Bool -> Bool
Exercise_4_1_1_const_true _ = True

Exercise_4_1_1_const_false : Bool -> Bool
Exercise_4_1_1_const_false _ = False

Exercise_4_4_1_Either_a_Void_To_a : {a : Type} -> Either a Void -> a
Exercise_4_4_1_Either_a_Void_To_a (Left x) = x
Exercise_4_4_1_Either_a_Void_To_a (Right y) = void y

Exercise_4_4_1_a_To_Either_a_Void : {a : Type} -> a -> Either a Void
Exercise_4_4_1_a_To_Either_a_Void x = Left x

Exericse_4_4_1_Either_a_Void_to_a_To_Either_a_Void_id : (a : Type) ->
    IsLeftInverse
        (Exercise_4_4_1_Either_a_Void_To_a {a})
        (Exercise_4_4_1_a_To_Either_a_Void {a})
Exericse_4_4_1_Either_a_Void_to_a_To_Either_a_Void_id a (Left _) = Refl
Exericse_4_4_1_Either_a_Void_to_a_To_Either_a_Void_id a (Right _) impossible

Exercise_4_4_1_a_To_Either_a_Void_to_a_id : (a : Type) ->
    IsRightInverse
        (Exercise_4_4_1_Either_a_Void_To_a {a})
        (Exercise_4_4_1_a_To_Either_a_Void {a})
Exercise_4_4_1_a_To_Either_a_Void_to_a_id a _ = Refl

Exercise_4_4_1_are_inverses : (a : Type) ->
    IsInverse
        (Exercise_4_4_1_Either_a_Void_To_a {a})
        (Exercise_4_4_1_a_To_Either_a_Void {a})
Exercise_4_4_1_are_inverses a =
    (Exericse_4_4_1_Either_a_Void_to_a_To_Either_a_Void_id a,
     Exercise_4_4_1_a_To_Either_a_Void_to_a_id a)

SumElimination : {a, b, x : Type} -> (f : a -> x) -> (g : b -> x) ->
    Either a b -> x
SumElimination f g (Left e) = f e
SumElimination f g (Right e) = g e

CommuteSumElimination : {a, b : Type} ->
  ObserverChange {cat=TypeCategory} (Either a b) (Either b a)
CommuteSumElimination _ h (Left e) = h (Right e)
CommuteSumElimination _ h (Right e) = h (Left e)

Exercise_4_4_2_CommuteSumEliminationIsOwnInverse : {a, b : Type} ->
    IsBijectionForEach (CommuteSumElimination {a} {b})
Exercise_4_4_2_CommuteSumEliminationIsOwnInverse x =
    (CommuteSumElimination {a=b} {b=a} x **
     (\h => functionalExtensionality (\e => case e of
        Left _ => Refl
        Right _ => Refl),
      \h => functionalExtensionality (\e => case e of
        Left _ => Refl
        Right _ => Refl)))

Exercise_4_4_2_CommuteSumEliminationIsNatural : {a, b : Type} ->
    ObserverChangeIsNatural {cat=TypeCategory} (CommuteSumElimination {a} {b})
Exercise_4_4_2_CommuteSumEliminationIsNatural {a} {b} x y g =
    functionalExtensionality
        (\h => functionalExtensionality
            (\e => case e of
                Left _ => Refl
                Right _ => Refl))

Exercise_4_4_3_CommuteSum : {a, b : Type} -> Either a b -> Either b a
Exercise_4_4_3_CommuteSum (Left e) = Right e
Exercise_4_4_3_CommuteSum (Right e) = Left e

Exercise_4_4_3_CommuteSumIsOwnLeftInverse : (a, b : Type) ->
    IsLeftInverse
        (Exercise_4_4_3_CommuteSum {a} {b})
        (Exercise_4_4_3_CommuteSum {a=b} {b=a})
Exercise_4_4_3_CommuteSumIsOwnLeftInverse a b (Left _) = Refl
Exercise_4_4_3_CommuteSumIsOwnLeftInverse a b (Right _) = Refl

Exercise_4_4_3_CommuteSumIsOwnRightInverse : (a, b : Type) ->
    IsRightInverse
        (Exercise_4_4_3_CommuteSum {a} {b})
        (Exercise_4_4_3_CommuteSum {a=b} {b=a})
Exercise_4_4_3_CommuteSumIsOwnRightInverse a b (Left _) = Refl
Exercise_4_4_3_CommuteSumIsOwnRightInverse a b (Right _) = Refl

Exercise_4_4_3_CommuteSumIsOwnInverse : (a, b : Type) ->
    IsInverse
        (Exercise_4_4_3_CommuteSum {a} {b})
        (Exercise_4_4_3_CommuteSum {a=b} {b=a})
Exercise_4_4_3_CommuteSumIsOwnInverse a b =
    (Exercise_4_4_3_CommuteSumIsOwnLeftInverse a b,
     Exercise_4_4_3_CommuteSumIsOwnRightInverse a b)

Exercise_4_4_4_Functoriality : {a, a', b, b' : Type} ->
    (f : a -> a') -> (g : b -> b') -> ((Either a b) -> (Either a' b'))
Exercise_4_4_4_Functoriality f g (Left e) = Left (f e)
Exercise_4_4_4_Functoriality f g (Right e) = Right (g e)

Exercise_4_4_4_Functoriality_Preserves_Composition :
    {a, a', a'', b, b', b'' : Type} ->
    (f : a -> a') -> (f' : a' -> a'') ->
    (g : b -> b') -> (g' : b' -> b'') ->
        Exercise_4_4_4_Functoriality (f' . f) (g' . g) =
        Exercise_4_4_4_Functoriality f' g' . Exercise_4_4_4_Functoriality f g
Exercise_4_4_4_Functoriality_Preserves_Composition f f' g g' =
    functionalExtensionality
        (\e => case e of
            Left _ => Refl
            Right _ => Refl)

Exercise_4_4_5_Functoriality_Preserves_Identity :
    (a, b : Type) ->
    Exercise_4_4_4_Functoriality (id {a}) (id {a=b}) = id {a=(Either a b)}
Exercise_4_4_5_Functoriality_Preserves_Identity a b =
    functionalExtensionality
        (\e => case e of
            Left _ => Refl
            Right _ => Refl)

max_stars_repo_name: rokopt/dao-fp-exercises

max_issues_repo_name: rokopt/dao-fp-exercises

max_forks_repo_name: rokopt/dao-fp-exercises


text:
module Test

import NanoParsec.Parser
import NanoParsec.Combinator

test : Show a => Parser a -> String -> IO ()
test p input = case parse p input of
    Just x => printLn x
    Nothing => putStrLn $ "FAIL: " ++ input

listOf : Parser a -> Parser (List a)
listOf p = do
    string "["
    xs <- p `sepBy` (string ",")
    string "]"
    return xs

testListOf1 : IO ()
testListOf1 = test (listOf natural) "[1,2,3,4,5,666]"

testListOf2 : IO ()
testListOf2 = test (listOf natural) "This is not a list, awesome!"

max_stars_repo_name: stallmanifold/idris-nanoparsec

max_issues_repo_name: lambdaxymox/idris-nanoparsec

max_forks_repo_name: lambdaxymox/idris-nanoparsec


text:
module Quantities.Power

--import Control.Algebra

infixr 10 ^

%default total
%access public export

-- 'Group', '<->' and 'AbelianGroup' are copied from Control.Algebra from 'contrib'.
-- I didn't just include Control.Algebra, because 'idris --install quantities.ipkg'
-- didn't know where to find Control.Algebra. Specifying 'contrib' in libs in
-- the IPKG file didn't help either.

-- XXX: change?
infixl 6 <->

||| Sets equipped with a single binary operation that is associative, along with
||| a neutral element for that binary operation and inverses for all elements.
||| Must satisfy the following laws:
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Neutral for `<+>`:
|||     forall a,     a <+> neutral   == a
|||     forall a,     neutral <+> a   == a
||| + Inverse for `<+>`:
|||     forall a,     a <+> inverse a == neutral
|||     forall a,     inverse a <+> a == neutral
interface Monoid a => Group a where
  inverse : a -> a

(<->) : Group a => a -> a -> a
(<->) left right = left <+> (inverse right)

interface Group a => AbelianGroup a where { }

public export
interface Power a where
  (^) : a -> Integer -> a

interface Power a => VerifiedPower a where
  iteratedPower : (x : a) -> (i : Integer) -> (j : Integer) ->
                  (x ^ i) ^ j = x ^ (i*j)

-- Inefficient. Use square and multiply!
grpPow : Group g => g -> g -> Nat -> g
grpPow _ y Z = y
grpPow x y (S k) = grpPow x (y <+> x) k

implementation Group g => Power g where
  (^) a i = case compare i 0 of
    LT => grpPow (inverse a) neutral (fromIntegerNat (-i))
    _  => grpPow a neutral (fromIntegerNat i)

implementation [floatmultpower] Power Double where
  a ^ 0 = fromInteger 1
  a ^ i = if a == 0 then 0 else case compare i 0 of
    LT => pow (1 / a) (fromIntegerNat (-i))
    _  => pow a (fromIntegerNat i)

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
||| Indexing Vectors.
|||
||| `Elem` proofs give existential quantification that a given element
||| *is* in the list, but not where in the list it is!  Here we give a
||| predicate that presents proof that a given index of a vector,
||| given by a `Fin` instance, will return a certain element.
|||
||| Two decidable decision procedures are presented:
|||
||| 1. Check that a given index points to the provided element in the
|||    presented vector.
|||
||| 2. Find the element at the given index in the presented vector.
module Data.Vect.AtIndex

import Data.Vect
import Decidable.Equality

%default total

public export
data AtIndex : (idx : Fin n)
            -> (xs  : Vect n type)
            -> (x   : type)
                   -> Type
  where
    Here : AtIndex FZ (x::xs) x

    There : (later : AtIndex     rest      xs  x)
                  -> AtIndex (FS rest) (y::xs) x

namespace Check
  public export
  elemDiffers : (y = x -> Void)
              -> AtIndex FZ (y :: xs) x
              -> Void
  elemDiffers f Here
    = f Refl

  public export
  elemNotInRest : (AtIndex z xs x -> Void)
               ->  AtIndex (FS z) (y :: xs) x
               ->  Void
  elemNotInRest f (There later)
    = f later

  ||| Is the element at the given index?
  |||
  public export
  index : DecEq type
       => (idx : Fin n)
       -> (x   : type)
       -> (xs  : Vect n type)
              -> Dec (AtIndex idx xs x)

  index FZ _ [] impossible
  index (FS y) _ [] impossible

  index FZ x (y :: xs) with (decEq y x)
    index FZ x (x :: xs) | (Yes Refl)
      = Yes Here
    index FZ x (y :: xs) | (No contra)
      = No (elemDiffers contra)

  index (FS z) x (y :: xs) with (Check.index z x xs)
    index (FS z) x (y :: xs) | (Yes prf)
      = Yes (There prf)
    index (FS z) x (y :: xs) | (No contra)
      = No (elemNotInRest contra)

namespace Find
  public export
  elemNotInRest : (DPair type (AtIndex     x        xs)  -> Void)
               ->  DPair type (AtIndex (FS x) (y :: xs)) -> Void

  elemNotInRest f (MkDPair i (There later))
    = f (MkDPair i later)

  ||| What is the element at the given index?
  |||
  public export
  index : DecEq type
       => (idx : Fin n)
       -> (xs  : Vect n type)
              -> Dec (DPair type (AtIndex idx xs))
  index FZ (x :: xs)
    = Yes (MkDPair x Here)

  index (FS x) (y :: xs) with (Find.index x xs)
    index (FS x) (y :: xs) | (Yes (MkDPair i idx))
      = Yes (MkDPair i (There idx))
    index (FS x) (y :: xs) | (No contra) = No (elemNotInRest contra)

-- [ EOF ]


text:
--    Copyright 2017, the blau.io contributors
--
--    Licensed under the Apache License, Version 2.0 (the "License");
--    you may not use this file except in compliance with the License.
--    You may obtain a copy of the License at
--
--        http://www.apache.org/licenses/LICENSE-2.0
--
--    Unless required by applicable law or agreed to in writing, software
--    distributed under the License is distributed on an "AS IS" BASIS,
--    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--    See the License for the specific language governing permissions and
--    limitations under the License.

module API.Web.DOM.Document

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

%access public export
%default total

||| A Document represents any web page loaded in the browser and servers as an
||| entry point into the web page's content. which is the DOM tree.
|||
||| The original interface specification can be found at
||| https://dom.spec.whatwg.org/#interface-document
data Document : DocumentType -> Type where
  FromHTMLDocument : (docType : DocumentType) ->
                     API.Web.HTML.Document.Document ->
                     API.Web.DOM.Document.Document docType

  ||| self is a non standard field which is used to facilitate integration with
  ||| Javascript.
  New : (docType : DocumentType) -> (self : Ptr) ->
        API.Web.DOM.Document.Document docType

||| documentFromPointer is a helper function for easily creating Documents from
||| JavaScript references.
|||
||| @ self a pointer to a document
documentFromPointer : (self : JSRef) ->
                      JS_IO $ Maybe $ API.Web.DOM.Document.Document docType
documentFromPointer self = case !maybeDocType of
    Nothing        => pure Nothing
    (Just docType) => case docType of

      -- A document is said to be an *XML document* if its type is "`xml`", and
      -- an *HTML document* otherwise.
      (New "xml" _ _ _) => pure $ Just $ New _ self
      (New _     _ _ _) => pure $ Just $ FromHTMLDocument _ $
                         API.Web.HTML.Document.New self

  where
    maybeDocType : JS_IO $ Maybe DocumentType
    maybeDocType = join $ map documentTypeFromPointer $
                   jscall "%0.docType" (JSRef -> JS_IO JSRef) self

max_stars_repo_name: blau-io/idris-web

max_issues_repo_name: pierrebeaucamp/idris-dom

max_forks_repo_name: pierrebeaucamp/idris-dom


text:
||| Reading and writing 'Defs' from/to a binary file. In order to be saved, a
||| name must have been flagged using 'toSave'. (Otherwise we'd save out
||| everything, not just the things in the current file).
module Core.Binary

import public Core.Binary.Prims
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Hash
import Core.Name.Namespace
import Core.Normalise
import Core.Options
import Core.TT
import Core.TTC
import Core.UnifyState

import Data.Buffer
import Data.List
import Data.String

import System.File

import Libraries.Data.IntMap
import Libraries.Data.NameMap

import public Libraries.Utils.Binary

%default covering

||| TTC files can only be compatible if the version number is the same
||| (Increment this when changing anything in the data format)
export
ttcVersion : Int
ttcVersion = 63

export
checkTTCVersion : String -> Int -> Int -> Core ()
checkTTCVersion file ver exp
  = when (ver /= exp) (throw $ TTCError $ Format file ver exp)

record TTCFile extra where
  constructor MkTTCFile
  version : Int
  totalReq : TotalReq
  sourceHash : Maybe String
  ifaceHash : Int
  importHashes : List (Namespace, Int)
  incData : List (CG, String, List String)
  context : List (Name, Binary)
  userHoles : List Name
  autoHints : List (Name, Bool)
  typeHints : List (Name, Name, Bool)
  imported : List (ModuleIdent, Bool, Namespace)
  nextVar : Int
  currentNS : Namespace
  nestedNS : List Namespace
  pairnames : Maybe PairNames
  rewritenames : Maybe RewriteNames
  primnames : PrimNames
  namedirectives : List (Name, List String)
  cgdirectives : List (CG, String)
  transforms : List (Name, Transform)
  extraData : extra

HasNames a => HasNames (List a) where
  full c ns = full_aux c [] ns
    where full_aux : Context -> List a -> List a -> Core (List a)
          full_aux c res [] = pure (reverse res)
          full_aux c res (n :: ns) = full_aux c (!(full c n):: res) ns

  resolved c ns = resolved_aux c [] ns
    where resolved_aux : Context -> List a -> List a -> Core (List a)
          resolved_aux c res [] = pure (reverse res)
          resolved_aux c res (n :: ns) = resolved_aux c (!(resolved c n) :: res) ns
HasNames (Int, FC, Name) where
  full c (i, fc, n) = pure (i, fc, !(full c n))
  resolved c (i, fc, n) = pure (i, fc, !(resolved c n))

HasNames (Name, Bool) where
  full c (n, b) = pure (!(full c n), b)
  resolved c (n, b) = pure (!(resolved c n), b)

HasNames (Name, List String) where
  full c (n, b) = pure (!(full c n), b)
  resolved c (n, b) = pure (!(resolved c n), b)

HasNames (Name, Transform) where
  full c (n, b) = pure (!(full c n), !(full c b))
  resolved c (n, b) = pure (!(resolved c n), !(resolved c b))

HasNames (Name, Name, Bool) where
  full c (n1, n2, b) = pure (!(full c n1), !(full c n2), b)
  resolved c (n1, n2, b) = pure (!(resolved c n1), !(resolved c n2), b)

HasNames e => HasNames (TTCFile e) where
  full gam (MkTTCFile version totalReq sourceHash ifaceHash iHashes incData
                      context userHoles
                      autoHints typeHints
                      imported nextVar currentNS nestedNS
                      pairnames rewritenames primnames
                      namedirectives cgdirectives trans
                      extra)
      = pure $ MkTTCFile version totalReq sourceHash ifaceHash iHashes incData
                         context userHoles
                         !(traverse (full gam) autoHints)
                         !(traverse (full gam) typeHints)
                         imported nextVar currentNS nestedNS
                         !(fullPair gam pairnames)
                         !(fullRW gam rewritenames)
                         !(fullPrim gam primnames)
                         !(full gam namedirectives)
                         cgdirectives
                         !(full gam trans)
                         !(full gam extra)
    where
      fullPair : Context -> Maybe PairNames -> Core (Maybe PairNames)
      fullPair gam Nothing = pure Nothing
      fullPair gam (Just (MkPairNs t f s))
          = pure $ Just $ MkPairNs !(full gam t) !(full gam f) !(full gam s)

      fullRW : Context -> Maybe RewriteNames -> Core (Maybe RewriteNames)
      fullRW gam Nothing = pure Nothing
      fullRW gam (Just (MkRewriteNs e r))
          = pure $ Just $ MkRewriteNs !(full gam e) !(full gam r)

      fullPrim : Context -> PrimNames -> Core PrimNames
      fullPrim gam (MkPrimNs mi ms mc md)
          = [| MkPrimNs (full gam mi) (full gam ms) (full gam mc) (full gam md) |]

  -- I don't think we ever actually want to call this, because after we read
  -- from the file we're going to add them to learn what the resolved names
  -- are supposed to be! But for completeness, let's do it right.
  resolved gam (MkTTCFile version totalReq sourceHash ifaceHash iHashes incData
                      context userHoles
                      autoHints typeHints
                      imported nextVar currentNS nestedNS
                      pairnames rewritenames primnames
                      namedirectives cgdirectives trans
                      extra)
      = pure $ MkTTCFile version totalReq sourceHash ifaceHash iHashes incData
                         context userHoles
                         !(traverse (resolved gam) autoHints)
                         !(traverse (resolved gam) typeHints)
                         imported nextVar currentNS nestedNS
                         !(resolvedPair gam pairnames)
                         !(resolvedRW gam rewritenames)
                         !(resolvedPrim gam primnames)
                         !(resolved gam namedirectives)
                         cgdirectives
                         !(resolved gam trans)
                         !(resolved gam extra)
    where
      resolvedPair : Context -> Maybe PairNames -> Core (Maybe PairNames)
      resolvedPair gam Nothing = pure Nothing
      resolvedPair gam (Just (MkPairNs t f s))
          = pure $ Just $ MkPairNs !(resolved gam t) !(resolved gam f) !(resolved gam s)

      resolvedRW : Context -> Maybe RewriteNames -> Core (Maybe RewriteNames)
      resolvedRW gam Nothing = pure Nothing
      resolvedRW gam (Just (MkRewriteNs e r))
          = pure $ Just $ MkRewriteNs !(resolved gam e) !(resolved gam r)

      resolvedPrim : Context -> PrimNames -> Core PrimNames
      resolvedPrim gam (MkPrimNs mi ms mc md)
          = pure $ MkPrimNs !(resolved gam mi)
                            !(resolved gam ms)
                            !(resolved gam mc)
                            !(resolved gam md)

-- NOTE: TTC files are only compatible if the version number is the same,
-- *and* the 'annot/extra' type are the same, or there are no holes/constraints
writeTTCFile : (HasNames extra, TTC extra) =>
               {auto c : Ref Ctxt Defs} ->
               Ref Bin Binary -> TTCFile extra -> Core ()
writeTTCFile b file_in
      = do file <- toFullNames file_in
           toBuf b "TT2"
           toBuf @{Wasteful} b (version file)
           toBuf b (totalReq file)
           toBuf b (sourceHash file)
           toBuf b (ifaceHash file)
           toBuf b (importHashes file)
           toBuf b (incData file)
           toBuf b (imported file)
           toBuf b (extraData file)
           toBuf b (context file)
           toBuf b (userHoles file)
           toBuf b (autoHints file)
           toBuf b (typeHints file)
           toBuf b (nextVar file)
           toBuf b (currentNS file)
           toBuf b (nestedNS file)
           toBuf b (pairnames file)
           toBuf b (rewritenames file)
           toBuf b (primnames file)
           toBuf b (namedirectives file)
           toBuf b (cgdirectives file)
           toBuf b (transforms file)

readTTCFile : TTC extra =>
              {auto c : Ref Ctxt Defs} ->
              Bool -> String -> Maybe (Namespace) ->
              Ref Bin Binary -> Core (TTCFile extra)
readTTCFile readall file as b
      = do hdr <- fromBuf b
           chunk <- get Bin
           when (hdr /= "TT2") $
             corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
           ver <- fromBuf @{Wasteful} b
           checkTTCVersion file ver ttcVersion
           totalReq <- fromBuf b
           sourceFileHash <- fromBuf b
           ifaceHash <- fromBuf b
           importHashes <- fromBuf b
           incData <- fromBuf b
           imp <- fromBuf b
           ex <- fromBuf b
           if not readall
              then pure (MkTTCFile ver totalReq
                                   sourceFileHash ifaceHash importHashes
                                   incData [] [] [] [] []
                                   0 (mkNamespace "") [] Nothing
                                   Nothing
                                   (MkPrimNs Nothing Nothing Nothing Nothing)
                                   [] [] [] ex)
              else do
                 defs <- fromBuf b
                 uholes <- fromBuf b
                 autohs <- fromBuf b
                 typehs <- fromBuf b
                 nextv <- fromBuf b
                 cns <- fromBuf b
                 nns <- fromBuf b
                 pns <- fromBuf b
                 rws <- fromBuf b
                 prims <- fromBuf b
                 nds <- fromBuf b
                 cgds <- fromBuf b
                 trans <- fromBuf b
                 pure (MkTTCFile ver totalReq
                                 sourceFileHash ifaceHash importHashes incData
                                 (map (replaceNS cns) defs) uholes
                                 autohs typehs imp nextv cns nns
                                 pns rws prims nds cgds trans ex)
  where
    -- We don't store full names in 'defs' - we remove the namespace if it's
    -- the same as the current namespace. So, this puts it back.
    replaceNS : Namespace -> (Name, a) -> (Name, a)
    replaceNS ns n@(NS _ _, d) = n
    replaceNS ns (n, d) = (NS ns n, d)

-- Pull out the list of GlobalDefs that we want to save
getSaveDefs : Namespace -> List Name -> List (Name, Binary) -> Defs ->
              Core (List (Name, Binary))
getSaveDefs modns [] acc _ = pure acc
getSaveDefs modns (n :: ns) acc defs
    = do Just gdef <- lookupCtxtExact n (gamma defs)
              | Nothing => getSaveDefs modns ns acc defs -- 'n' really should exist though!
         -- No need to save builtins
         case definition gdef of
              Builtin _ => getSaveDefs modns ns acc defs
              _ => do bin <- initBinaryS 16384
                      toBuf bin (trimNS modns !(full (gamma defs) gdef))
                      b <- get Bin
                      getSaveDefs modns ns ((trimName (fullname gdef), b) :: acc) defs
  where
    trimName : Name -> Name
    trimName n@(NS defns d) = if defns == modns then d else n
    trimName n = n

-- Write out the things in the context which have been defined in the
-- current source file
export
writeToTTC : (HasNames extra, TTC extra) =>
             {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             extra -> (sourceFileName : String) ->
             (ttcFileName : String) -> Core ()
writeToTTC extradata sourceFileName ttcFileName
    = do bin <- initBinary
         defs <- get Ctxt
         ust <- get UST
         gdefs <- getSaveDefs (currentNS defs) (keys (toSave defs)) [] defs
         sourceHash <- hashFileWith defs.options.hashFn sourceFileName
         totalReq <- getDefaultTotalityOption
         log "ttc.write" 5 $ unwords
           [ "Writing", ttcFileName
           , "with source hash", show sourceHash
           , "and interface hash", show (ifaceHash defs)
           ]
         writeTTCFile bin
                   (MkTTCFile ttcVersion totalReq
                              sourceHash
                              (ifaceHash defs) (importHashes defs)
                              (incData defs)
                              gdefs
                              (keys (userHoles defs))
                              (saveAutoHints defs)
                              (saveTypeHints defs)
                              (imported defs)
                              (nextName ust)
                              (currentNS defs)
                              (nestedNS defs)
                              (pairnames (options defs))
                              (rewritenames (options defs))
                              (primnames (options defs))
                              (NameMap.toList (namedirectives defs))
                              (cgdirectives defs)
                              (saveTransforms defs)
                              extradata)

         Right ok <- coreLift $ writeToFile ttcFileName !(get Bin)
               | Left err => throw (InternalError (ttcFileName ++ ": " ++ show err))
         pure ()

addGlobalDef : {auto c : Ref Ctxt Defs} ->
               (modns : ModuleIdent) -> Namespace ->
               (importAs : Maybe Namespace) ->
               (Name, Binary) -> Core ()
addGlobalDef modns filens asm (n, def)
    = do defs <- get Ctxt
         codedentry <- lookupContextEntry n (gamma defs)
         -- Don't update the coded entry because some names might not be
         -- resolved yet
         entry <- maybe (pure Nothing)
                        (\ p => do x <- decode (gamma defs) (fst p) False (snd p)
                                   pure (Just x))
                        codedentry
         unless (completeDef entry) $
           ignore $ addContextEntry filens n def

         whenJust asm $ \ as => addContextAlias (asName modns as n) n

  where
    -- If the definition already exists, don't overwrite it with an empty
    -- definition or hole. This might happen if a function is declared in one
    -- module and defined in another.
    completeDef : Maybe GlobalDef -> Bool
    completeDef Nothing = False
    completeDef (Just def)
        = case definition def of
               None => False
               Hole _ _ => False
               _ => True

addTypeHint : {auto c : Ref Ctxt Defs} ->
              FC -> (Name, Name, Bool) -> Core ()
addTypeHint fc (tyn, hintn, d)
   = do logC "ttc.read" 10 (pure (show !(getFullName hintn) ++ " for " ++
                            show !(getFullName tyn)))
        addHintFor fc tyn hintn d True

addAutoHint : {auto c : Ref Ctxt Defs} ->
              (Name, Bool) -> Core ()
addAutoHint (hintn_in, d)
    = do defs <- get Ctxt
         hintn <- toResolvedNames hintn_in

         put Ctxt (record { autoHints $= insert hintn d } defs)

export
updatePair : {auto c : Ref Ctxt Defs} ->
             Maybe PairNames -> Core ()
updatePair p
    = do defs <- get Ctxt
         put Ctxt (record { options->pairnames $= (p <+>) } defs)

export
updateRewrite : {auto c : Ref Ctxt Defs} ->
                Maybe RewriteNames -> Core ()
updateRewrite r
    = do defs <- get Ctxt
         put Ctxt (record { options->rewritenames $= (r <+>) } defs)

export
updatePrimNames : PrimNames -> PrimNames -> PrimNames
updatePrimNames p
    = record { fromIntegerName $= ((fromIntegerName p) <+>),
               fromStringName $= ((fromStringName p) <+>),
               fromCharName $= ((fromCharName p) <+>),
               fromDoubleName $= ((fromDoubleName p) <+>)
             }

export
updatePrims : {auto c : Ref Ctxt Defs} ->
              PrimNames -> Core ()
updatePrims p
    = do defs <- get Ctxt
         put Ctxt (record { options->primnames $= updatePrimNames p } defs)

export
updateNameDirectives : {auto c : Ref Ctxt Defs} ->
                       List (Name, List String) -> Core ()
updateNameDirectives [] = pure ()
updateNameDirectives ((t, ns) :: nds)
    = do defs <- get Ctxt
         put Ctxt (record { namedirectives $= insert t ns } defs)
         updateNameDirectives nds

export
updateCGDirectives : {auto c : Ref Ctxt Defs} ->
                     List (CG, String) -> Core ()
updateCGDirectives cgs
    = do defs <- get Ctxt
         let cgs' = nub (cgs ++ cgdirectives defs)
         put Ctxt (record { cgdirectives = cgs' } defs)

export
updateTransforms : {auto c : Ref Ctxt Defs} ->
                   List (Name, Transform) -> Core ()
updateTransforms [] = pure ()
updateTransforms ((n, t) :: ts)
    = do addT !(toResolvedNames n) !(toResolvedNames t)
         updateTransforms ts
  where
    addT : Name -> Transform -> Core ()
    addT n t
        = do defs <- get Ctxt
             case lookup n (transforms defs) of
                  Nothing =>
                     put Ctxt (record { transforms $= insert n [t] } defs)
                  Just ts =>
                     put Ctxt (record { transforms $= insert n (t :: ts) } defs)

getNSas : (String, (ModuleIdent, Bool, Namespace)) ->
          (ModuleIdent, Namespace)
getNSas (a, (b, c, d)) = (b, d)

-- Add definitions from a binary file to the current context
-- Returns the "extra" section of the file (user defined data), the interface
-- hash and the list of additional TTCs that need importing
-- (we need to return these, rather than do it here, because after loading
-- the data that's when we process the extra data...)
export
readFromTTC : TTC extra =>
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              Bool -> -- set nested namespaces (for records, to use at the REPL)
              FC ->
              Bool -> -- importing as public
              (fname : String) -> -- file containing the module
              (modNS : ModuleIdent) -> -- module namespace
              (importAs : Namespace) -> -- namespace to import as
              Core (Maybe (extra, Int,
                           List (ModuleIdent, Bool, Namespace)))
readFromTTC nestedns loc reexp fname modNS importAs
    = do defs <- get Ctxt
         -- If it's already in the context, with the same visibility flag,
         -- don't load it again (we do need to load it again if it's visible
         -- this time, because we need to reexport the dependencies.)
         let False = (modNS, reexp, importAs) `elem` map snd (allImported defs)
              | True => pure Nothing
         put Ctxt (record { allImported $= ((fname, (modNS, reexp, importAs)) :: ) } defs)

         Right buffer <- coreLift $ readFromFile fname
               | Left err => throw (InternalError (fname ++ ": " ++ show err))
         bin <- newRef Bin buffer -- for reading the file into
         let as = if importAs == miAsNamespace modNS
                     then Nothing
                     else Just importAs

         -- If it's already imported, but without reexporting, then all we're
         -- interested in is returning which other modules to load.
         -- Otherwise, add the data
         if alreadyDone modNS importAs (allImported defs)
            then do ttc <- readTTCFile False fname as bin
                    let ex = extraData ttc
                    pure (Just (ex, ifaceHash ttc, imported ttc))
            else do
               ttc <- readTTCFile True fname as bin
               let ex = extraData ttc
               traverse_ (addGlobalDef modNS (currentNS ttc) as) (context ttc)
               traverse_ (addUserHole True) (userHoles ttc)
               setNS (currentNS ttc)
               when nestedns $ setNestedNS (nestedNS ttc)
               -- Only do the next batch if the module hasn't been loaded
               -- in any form
               unless (modNS `elem` map (fst . getNSas) (allImported defs)) $
               -- Set up typeHints and autoHints based on the loaded data
                 do traverse_ (addTypeHint loc) (typeHints ttc)
                    traverse_ addAutoHint (autoHints ttc)
                    addImportedInc modNS (incData ttc)
                    defs <- get Ctxt
                    -- Set up pair/rewrite etc names
                    updatePair (pairnames ttc)
                    updateRewrite (rewritenames ttc)
                    updatePrims (primnames ttc)
                    updateNameDirectives (reverse (namedirectives ttc))
                    updateCGDirectives (cgdirectives ttc)
                    updateTransforms (transforms ttc)

               when (not reexp) clearSavedHints
               resetFirstEntry

               -- Finally, update the unification state with the holes from the
               -- ttc
               ust <- get UST
               put UST (record { nextName = nextVar ttc } ust)
               pure (Just (ex, ifaceHash ttc, imported ttc))
  where
    alreadyDone : ModuleIdent -> Namespace ->
                  List (String, (ModuleIdent, Bool, Namespace)) ->
                  Bool
    alreadyDone modns importAs [] = False
      -- If we've already imported 'modns' as 'importAs', or we're importing
      -- 'modns' as itself and it's already imported as anything, then no
      -- need to load again.
    alreadyDone modns importAs ((_, (m, _, a)) :: rest)
        = (modns == m && importAs == a)
          || (modns == m && miAsNamespace modns == importAs)
          || alreadyDone modns importAs rest

getImportHashes : String -> Ref Bin Binary ->
                  Core (List (Namespace, Int))
getImportHashes file b
    = do hdr <- fromBuf {a = String} b
         when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
         ver <- fromBuf @{Wasteful} b
         checkTTCVersion file ver ttcVersion
         totalReq <- fromBuf {a = TotalReq} b
         sourceFileHash <- fromBuf {a = Maybe String} b
         interfaceHash <- fromBuf {a = Int} b
         fromBuf b

export
getTotalReq : String -> Ref Bin Binary -> Core TotalReq
getTotalReq file b
    = do hdr <- fromBuf {a = String} b
         when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
         ver <- fromBuf @{Wasteful} b
         checkTTCVersion file ver ttcVersion
         fromBuf b

export
readTotalReq : (fileName : String) -> -- file containing the module
               Core (Maybe TotalReq)
readTotalReq fileName
    = do Right buffer <- coreLift $ readFromFile fileName
            | Left err => pure Nothing
         b <- newRef Bin buffer
         catch (Just <$> getTotalReq fileName b)
               (\err => pure Nothing)

export
getHashes : String -> Ref Bin Binary -> Core (Maybe String, Int)
getHashes file b
    = do hdr <- fromBuf {a = String} b
         when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
         ver <- fromBuf @{Wasteful} b
         checkTTCVersion file ver ttcVersion
         totReq <- fromBuf {a = TotalReq} b
         sourceFileHash <- fromBuf b
         interfaceHash <- fromBuf b
         pure (sourceFileHash, interfaceHash)

export
readHashes : (fileName : String) -> -- file containing the module
                Core (Maybe String, Int)
readHashes fileName
    = do Right buffer <- coreLift $ readFromFile fileName
            | Left err => pure (Nothing, 0)
         b <- newRef Bin buffer
         catch (getHashes fileName b)
               (\err => pure (Nothing, 0))

export
readImportHashes : (fname : String) -> -- file containing the module
                   Core (List (Namespace, Int))
readImportHashes fname
    = do Right buffer <- coreLift $ readFromFile fname
            | Left err => pure []
         b <- newRef Bin buffer
         catch (do res <- getImportHashes fname b
                   pure res)
               (\err => pure [])


text:
module ALaCarte

import Fix

%access public export

||| Position of a sub-type in a super-type composed of signatures `fs`.
data Sig : (fs : List (Type -> Type)) -> (a : Type) -> Type where
    ||| The sub-type `f` is located at the head of the list of composed types `fs`.
    Here  : f a -> Sig (f :: fs) a
    ||| The sub-type is located after the head of the list.
    There : Sig fs a -> Sig (f :: fs) a

||| A proof that some signature `f` is found in a list `fs`.
data Elem : (f : Type -> Type) -> (fs : List (Type -> Type)) -> Type where
    ||| A proof the signature `f` is at the head of the list of signatures `fs`.
    H : Elem f (f :: fs)
    ||| A proof the signature `f` is after the front of the list.
    T : Elem f ys -> Elem f (y :: ys)

||| Inject some sub-type `f a` into a super type, `Sig fs a`, containing syntax
||| for `f a`, i.e. `Elem f fs`.
inj : {auto prf : Elem f fs} -> f a -> Sig fs a
inj {prf=H}   x = Here x
inj {prf=T t} x = There (inj {prf=t} x)

||| Inject some type `f a` into a `Fix` tree containing syntax for `f a`.
inject : {auto prf : Elem f fs} -> f (Fix (Sig fs)) -> Fix (Sig fs)
inject = In . inj

||| Base case making `Sig` an instance of `Functor`.
Functor (Sig []) where
    map _ (Here _) impossible
    map _ (There _) impossible

||| Recursive case making `Sig` an instance of `Functor`.
(Functor f, Functor (Sig fs)) => Functor (Sig (f :: fs)) where
    map func (Here x) = Here (map func x)
    map func (There t) = There (map func t)

||| Algebra used to fold over a `Fix` tree, creating a value of type `a`.
interface Alg (f : Type -> Type) (a : Type) where
    alg : f a -> a

||| Base case making `Sig` an instance of `Alg`.
Alg (Sig []) a where
    alg (Here _) impossible
    alg (There _) impossible

||| Recusrive case making `Sig` an instance of `Alg`.
(Alg f a, Alg (Sig fs) a) => Alg (Sig (f :: fs)) a where
    alg (Here x) = alg x
    alg (There x) = alg x

||| Convenience method for folding over a `Fix` tree using the algebra defined
||| in interface instances.
eval : (Functor f, Alg f a) => Fix f -> a
eval = cata alg

max_stars_repo_name: BakerSmithA/alacarte-idris

max_issues_repo_name: BakerSmithA/alacarte-idris

max_forks_repo_name: BakerSmithA/alacarte-idris


text:
module Incrementer

import public RealizedFunction

%default total

-- Realized incrementer
public export
incrementer : Int -> Int
incrementer = (+1)

public export
incrementer_attrs : RealizedAttributes
incrementer_attrs = MkRealizedAttributes (MkCosts 100 10 1) 1

public export
rlz_incrementer : RealizedFunction (Int -> Int) Incrementer.incrementer_attrs
rlz_incrementer = MkRealizedFunction incrementer incrementer_attrs

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
-- --------------------------------------------------------------- [ PVect.idr ]
-- Module    : PVect.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A `list` construct to create lists of dependent types.
|||
||| One of the problems with using dependent types is that types
||| depend on values. This affects the ability to construct lists of
||| values that have a dependent type. The existing `List` type cannot
||| be used as it requires all elements to have the same type.
module Data.PVect

import Data.Vect
import Data.DVect

import Data.DList

import public Decidable.Equality.Indexed

%default total
%access export

using (aTy : Type, elemTy : (aTy -> Type), x : aTy)

  ||| A list construct for dependent types.
  |||
  ||| @aTy    The type of the value contained within the list element type.
  ||| @len    The length of the list.
  ||| @elemTy The type of the elements within the list
  ||| @as     The List used to contain the different values within the type.
  public export
  data PVect : (aTy : Type)
            -> (elemTy : aTy -> Type)
            -> (predTy : aTy -> Type)
            -> (len : Nat)
            -> (as : Vect len aTy)
            -> (ps : DVect aTy predTy len as)
            -> Type where
    ||| Create an empty List
    Nil  : PVect aTy elemTy prfTy Z Nil Nil
    ||| Cons
    |||
    ||| @ex The element to add
    ||| @rest The list for `elem` to be added to.
    Ext : (ex : elemTy x)
       -> (pf : prfTy x)
       -> (rest : PVect aTy elemTy prfTy n xs ps)
       -> PVect aTy elemTy prfTy (S n) (x::xs) (pf::ps)

(++) : PVect aTy eTy pTy x     xs         xps
    -> PVect aTy eTy pTy y     ys         yps
    -> PVect aTy eTy pTy (x+y) (xs ++ ys) (xps ++ yps)
(++) xs ys with (xs)
  (++) xs ys | [] = ys
  (++) xs ys | (Ext ex pf rest) = Ext ex pf ((++) rest ys)

-- -------------------------------------------------------------- [ Form Tests ]
isNil : PVect aTy elemTy prfTy n as ps -> Bool
isNil Nil     = True
isNil (Ext x pf xs) = False

isCons : PVect aTy elemTy prfTy n as ps -> Bool
isCons l = isNil l == False

-- ------------------------------------------------------------------ [ Length ]

length : PVect aTy elemTy prfTy n as ps -> Nat
length {n} _ = n

-- ---------------------------------------------------------------- [ Indexing ]

index : (idx : Fin l)
     -> (vs : PVect aTy elemTy prfTy l as ps)
     -> elemTy (index idx as)
index FZ (Ext ex px rest) = ex
index (FS x) (Ext ex px rest) = index x rest

head : (vs : PVect aTy elemTy prfTy (S n) (a::as) (p::ps))
    -> (elemTy a, prfTy a)
head (Ext x p rest) = (x,p)

tail : (vs : PVect aTy eTy pTy (S n) (a :: as) (p :: ps))
    -> (PVect aTy eTy pTy n as ps)
tail (Ext ex px rest) = rest

last : (vs : PVect aTy eTy pTy (S n) as ps)
    -> (eTy (last as), pTy (last as))
last (Ext ex px rest) with (rest)
  last (Ext ex px rest) | [] = (ex, px)
  last (Ext ex px rest) | (Ext ey py xs) = last (Ext ey py xs)

init : (vs : PVect aTy eTy pTy (S n) as ps)
    -> PVect aTy eTy pTy n (init as) (init ps)
init (Ext ex px []) = []
init (Ext ex px (Ext ey py zs)) = Ext ex px $ init (Ext ey py zs)

take : (n : Nat)
    -> (vs : PVect aTy eTy pTy (n+m) as ps)
    -> PVect aTy eTy pTy n (take n as) (take n ps)
take Z vs = []
take (S k) (Ext ex px rest) = Ext ex px $ take k rest

{-
takeWhile' : ({i : aTy} -> eTy i -> Bool)
          -> (vs : DVect aTy eTy l is)
          -> (l' : Nat ** bs : Vect l' aTy ** DVect aTy eTy l' bs)
takeWhile' f Nil = (_ ** _ ** Nil)
takeWhile' f (ex :: rest) =
  if f ex
  then (_ ** _ ** DVect.(::) ex (snd $ snd (takeWhile' f rest)))
  else (_ ** _ ** Nil)

drop : (n  : Nat)
    -> (vs : DVect aTy eTy (n + m) as)
    -> DVect aTy eTy m (drop n as)
drop Z vs = vs
drop (S k) (ex :: rest) = drop k rest

dropWhile' : ({i : aTy} -> eTy i -> Bool)
          -> (vs : DVect aTy eTy l is)
          -> (l' : Nat ** bs : Vect l' aTy ** DVect aTy eTy l' bs)
dropWhile' f Nil = (_ ** _ ** Nil)
dropWhile' f (ex :: rest) =
  if f ex
  then dropWhile' f rest
  else (_ ** _ ** DVect.(::) ex rest)

replicate : (n : Nat)
         -> (e : eTy i)
         -> DVect aTy eTy n (replicate n i)
replicate Z e = []
replicate (S k) e = e :: replicate k e

equals : ({i,j : aTy} -> e i -> e j -> Bool)
       -> DVect aTy e a as
       -> DVect aTy e b bs
       -> Bool
equals _ Nil Nil = True
equals f (x::xs) (y::ys) =
  if f x y
  then equals f xs ys
  else False
equals _ _ _ = False

compare : ({i,j : aTy} -> e i -> e j -> Bool)
        -> ({i,j : aTy} -> e i -> e j -> Ordering)
        -> DVect aTy e a as
        -> DVect aTy e b bs
        -> Ordering
compare _ _ Nil Nil = EQ
compare _ _ Nil _   = LT
compare _ _ _   Nil = GT
compare e c (a::as) (b::bs) =
  if (not (e a b))
  then c a b
  else compare e c as bs

concat : (xss : DVect (Vect n iTy) (DVect iTy e n) m iis)
      -> DVect iTy e (m * n) (concat iis)
concat [] = Nil
concat (ex :: rest) = ex ++ concat rest

foldr : ({i : iTy} -> e i -> p -> p)
     -> p
     -> DVect iTy e l as
     -> p
foldr _ acc Nil = acc
foldr f acc (x::xs) = f x (foldr f acc xs)

foldl : ({i : iTy} -> p -> e i -> p)
     -> p
     -> DVect iTy e l as
     -> p
foldl f init Nil = init
foldl f init (x::xs) = foldl f (f init x) xs

namespace Clean
  traverse : Applicative f
          => (funcTy : aTy -> bTy)
          -> (func : {a : aTy} -> elemTy a -> f $ elemTyB (funcTy a))
          -> (xs   : DVect aTy elemTy n as)
          -> f (DVect bTy elemTyB n (map funcTy as))
  traverse fTy func Nil     = pure Nil
  traverse fTy func (x::xs) = [| DVect.(::) (func x) (traverse fTy func xs) |]

namespace ToVect
 traverseToVect : Applicative f
        => (func : {a : aTy} -> elemTy a -> f b)
        -> (xs   : DVect aTy elemTy n as)
        -> f (Vect n b)
 traverseToVect func Nil     = pure Nil
 traverseToVect func (x::xs) = [| (::) (func x) (ToVect.traverseToVect func xs) |]

traverseToVDP : Applicative f
             => {bTy : Type}
             -> {elemTyB : bTy -> Type}
             -> (func : {a : aTy}
                     -> elemTy a
                     -> f (c ** elemTyB c))
             -> (xs : DVect aTy elemTy n as)
             -> f (Vect n (b ** elemTyB b))
traverseToVDP func [] = pure Nil
traverseToVDP func (e :: rest) = [| Vect.(::) (func e) $ traverseToVDP func rest|]

mapToVect : ({i : iTy} -> e i -> b)
         -> DVect iTy e l as
         -> Vect l b
mapToVect _ Nil = Nil
mapToVect f (x::xs) = f x :: mapToVect f xs

mapToList : ({i : iTy} -> e i -> b)
         -> DVect iTy e l as
         -> List b
mapToList f Nil = Nil
mapToList f (ex :: rest) = f ex :: mapToList f rest

toList' : Vect l type -> List type
toList' [] = []
toList' (x :: xs) = x :: toList' xs

mapToDList : DVect iTy e l as
          -> DList iTy e (toList' as)
mapToDList [] = []
mapToDList (ex :: rest) = ex :: mapToDList rest

mapMaybeToVect : ({i : iTy} -> e i -> Maybe b)
              -> DVect iTy e l as
              -> (l' ** Vect l' b)
mapMaybeToVect f Nil = (_ ** Nil)
mapMaybeToVect f (x::xs) =
  let rest = mapMaybeToVect f xs in
   case f x of
     Nothing => rest
     Just y  => (_ ** y :: (snd rest))

zipWith : (fT : iTy -> jTy -> kTy)
       -> (fV : {i : iTy} -> {j : jTy} -> e i -> f j -> g (fT i j))
       -> (xs : DVect iTy e l as)
       -> (ys : DVect jTy f l bs)
       -> DVect kTy g l (zipWith fT as bs)
zipWith fT fV [] [] = []
zipWith fT fV (ex :: restx) (ey :: resty) =
    fV ex ey :: zipWith fT fV restx resty

-- -------------------------------------------------------------------- [ Show ]

show : (showFunc : {a : aTy} -> elemTy a -> String)
    -> (vs : DVect aTy elemTy l as)
    -> String
show showFunc vs {l} = unwords strL
  where
     asVStr : Vect l String
     asVStr = mapToVect showFunc vs

     strL : List String
     strL = ["["] ++ intersperse ","  (toList asVStr) ++ ["]"]

-- -------------------------------------------------------------------- [ Elem ]

data VElem : (iTy : Type)
          -> (elemTy : iTy -> Type)
          -> (e : elemTy i)
          -> (es : DVect iTy elemTy l is)
          -> (prf : Elem i is)
          -> Type
  where
    Hier : (x=y) -> VElem iTy eTy x (y::xs) Here
    Er   : (komst : VElem iTy eTy x xs later)
        -> VElem iTy eTy x (not_x::xs) (There later)

Uninhabited (VElem iTy eTy a Nil prf) where
  uninhabited (Hier _) impossible
  uninhabited (Er _) impossible

vectIsEmpty : DecEq iTy => VElem iTy eTy e [] prf -> Void
vectIsEmpty (Hier _) impossible
vectIsEmpty (Er _) impossible

elemsNotEqual : DecEqIdx iTy eTy => (contra : (ex = ey) -> Void) -> VElem iTy eTy ex (ey :: rest) Here -> Void
elemsNotEqual contra (Hier Refl) = contra Refl

notInVect : DecEqIdx iTy eTy
        => (contra : VElem iTy eTy ex rest later -> Void)
        -> VElem iTy eTy ex (ey :: rest) (There later) -> Void
notInVect contra (Er komst) = contra komst

isElem' : {eTy : iTy -> Type}
       -> (DecEqIdx iTy eTy)
       => (e  : eTy i)
       -> (es : DVect iTy eTy l is)
       -> (prf : Elem i is)
       -> Dec (VElem iTy eTy e es prf)
isElem' ex (ey :: rest) Here with (decEq ex ey Refl)
  isElem' ey (ey :: rest) Here | (Yes Refl) = Yes (Hier Refl)
  isElem' ex (ey :: rest) Here | (No contra) = No (elemsNotEqual contra)

isElem' ex (ey :: rest) (There later) with (isElem' ex rest later)
  isElem' ex (ey :: rest) (There later) | (Yes komst) = Yes (Er komst)
  isElem' ex (ey :: rest) (There later) | (No contra) =
    No (notInVect contra)

isElem : {eTy : iTy -> Type}
      -> (DecEqIdx iTy eTy)
      => (e  : eTy i)
      -> (es : DVect iTy eTy l is)
      -> {auto prf : Elem i is}
      -> Dec (VElem iTy eTy e es prf)
isElem e es {prf} = isElem' e es prf

dropElem : (as : DVect iTy eTy (S l) is)
        -> (prf : VElem iTy eTy a as idx)
        -> DVect iTy eTy l (dropElem is idx)
dropElem (a :: x) (Hier _) = x
dropElem {l = (S k)} (not_x :: xs) (Er komst) =
  not_x :: dropElem xs komst
-}
-- --------------------------------------------------------------------- [ EOF ]