text:
module Idris.Elab.Implementation

import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
import Core.TT
import Core.Unify

import Idris.Resugar
import Idris.Syntax

import TTImp.BindImplicits
import TTImp.Elab
import TTImp.Elab.Check
import TTImp.ProcessDecls
import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Unelab
import TTImp.Utils

import Control.Monad.State
import Libraries.Data.ANameMap
import Data.List
import Libraries.Data.NameMap

%default covering

replaceSep : String -> String
replaceSep = pack . map toForward . unpack
  where
    toForward : Char -> Char
    toForward '\\' = '/'
    toForward x = x

export
mkImplName : FC -> Name -> List RawImp -> Name
mkImplName fc n ps
    = DN (show n ++ " implementation at " ++ replaceSep (show fc))
         (UN $ Basic ("__Impl_" ++ show n ++ "_" ++
          showSep "_" (map show ps)))

bindConstraints : FC -> PiInfo RawImp ->
                  List (Maybe Name, RawImp) -> RawImp -> RawImp
bindConstraints fc p [] ty = ty
bindConstraints fc p ((n, ty) :: rest) sc
    = IPi fc top p n ty (bindConstraints fc p rest sc)

bindImpls : FC -> List (Name, RigCount, RawImp) -> RawImp -> RawImp
bindImpls fc [] ty = ty
bindImpls fc ((n, r, ty) :: rest) sc
    = IPi fc r Implicit (Just n) ty (bindImpls fc rest sc)

addDefaults : FC -> Name ->
              (params : List (Name, RawImp)) -> -- parameters have been specialised, use them!
              (allMethods : List Name) ->
              (defaults : List (Name, List ImpClause)) ->
              List ImpDecl ->
              (List ImpDecl, List Name) -- Updated body, list of missing methods
addDefaults fc impName params allms defs body
    = let missing = dropGot allms body in
          extendBody [] missing body
  where
    specialiseMeth : Name -> (Name, RawImp)
    specialiseMeth n = (n, INamedApp fc (IVar fc n) (UN $ Basic "__con") (IVar fc impName))
    -- Given the list of missing names, if any are among the default definitions,
    -- add them to the body
    extendBody : List Name -> List Name -> List ImpDecl ->
                 (List ImpDecl, List Name)
    extendBody ms [] body = (body, ms)
    extendBody ms (n :: ns) body
        = case lookup n defs of
               Nothing => extendBody (n :: ms) ns body
               Just cs =>
                    -- If any method names appear in the clauses, they should
                    -- be applied to the constraint name __con because they
                    -- are going to be referring to the present implementation.
                    -- That is, default method implementations could depend on
                    -- other methods.
                    -- (See test idris2/interface014 for an example!)

                    -- Similarly if any parameters appear in the clauses, they should
                    -- be substituted for the actual parameters because they are going
                    -- to be referring to unbound variables otherwise.
                    -- (See test idris2/interface018 for an example!)
                    let mupdates = params ++ map specialiseMeth allms
                        cs' = map (substNamesClause [] mupdates) cs in
                        extendBody ms ns
                             (IDef fc n (map (substLocClause fc) cs') :: body)

    -- Find which names are missing from the body
    dropGot : List Name -> List ImpDecl -> List Name
    dropGot ms [] = ms
    dropGot ms (IDef _ n _ :: ds)
        = dropGot (filter (/= n) ms) ds
    dropGot ms (_ :: ds) = dropGot ms ds

getMethImps : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              Env Term vars -> Term vars ->
              Core (List (Name, RigCount, RawImp))
getMethImps env (Bind fc x (Pi fc' c Implicit ty) sc)
    = do rty <- map (map rawName) $ unelabNoSugar env ty
         ts <- getMethImps (Pi fc' c Implicit ty :: env) sc
         pure ((x, c, rty) :: ts)
getMethImps env tm = pure []

export
elabImplementation : {vars : _} ->
                     {auto c : Ref Ctxt Defs} ->
                     {auto u : Ref UST UState} ->
                     {auto s : Ref Syn SyntaxInfo} ->
                     {auto m : Ref MD Metadata} ->
                     FC -> Visibility -> List FnOpt -> Pass ->
                     Env Term vars -> NestedNames vars ->
                     (implicits : List (Name, RigCount, RawImp)) ->
                     (constraints : List (Maybe Name, RawImp)) ->
                     Name ->
                     (ps : List RawImp) ->
                     (namedimpl : Bool) ->
                     (implName : Name) ->
                     (nusing : List Name) ->
                     Maybe (List ImpDecl) ->
                     Core ()
-- TODO: Refactor all these steps into separate functions
elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named impName_in nusing mbody
    = do -- let impName_in = maybe (mkImplName fc iname ps) id impln
         -- If we're in a nested block, update the name
         let impName_nest = case lookup impName_in (names nest) of
                                 Just (Just n', _) => n'
                                 _ => impName_in
         impName <- inCurrentNS impName_nest
         -- The interface name might be qualified, so check if it's an
         -- alias for something
         syn <- get Syn
         defs <- get Ctxt
         inames <- lookupCtxtName iname (gamma defs)
         let [cndata] = concatMap (\n => lookupName n (ifaces syn))
                                  (map fst inames)
             | [] => undefinedName vfc iname
             | ns => throw (AmbiguousName vfc (map fst ns))
         let cn : Name = fst cndata
         let cdata : IFaceInfo = snd cndata

         Just ity <- lookupTyExact cn (gamma defs)
              | Nothing => undefinedName vfc cn
         Just conty <- lookupTyExact (iconstructor cdata) (gamma defs)
              | Nothing => undefinedName vfc (iconstructor cdata)

         let impsp = nub (concatMap findIBinds ps ++
                          concatMap findIBinds (map snd cons))

         logTerm "elab.implementation" 3 ("Found interface " ++ show cn) ity
         log "elab.implementation" 3 $
                 "\n  with params: " ++ show (params cdata)
                 ++ "\n  specialised to: " ++ show ps
                 ++ "\n  and parents: " ++ show (parents cdata)
                 ++ "\n  using implicits: " ++ show impsp
                 ++ "\n  and methods: " ++ show (methods cdata) ++ "\n"
                 ++ "\nConstructor: " ++ show (iconstructor cdata) ++ "\n"
         logTerm "elab.implementation" 3 "Constructor type: " conty
         log "elab.implementation" 5 $ "Making implementation " ++ show impName

         -- 1. Build the type for the implementation
         -- Make the constraints auto implicit arguments, which can be explicitly
         -- given when using named implementations
         --    (cs : Constraints) -> Impl params
         -- Don't make it a hint if it's a named implementation
         let opts = if named
                       then [Inline]
                       else [Inline, Hint True]

         let initTy = bindImpls vfc is $ bindConstraints vfc AutoImplicit cons
                         (apply (IVar vfc iname) ps)
         let paramBinds = if !isUnboundImplicits
                          then findBindableNames True vars [] initTy
                          else []
         let impTy = doBind paramBinds initTy

         let impTyDecl = IClaim vfc top vis opts (MkImpTy EmptyFC EmptyFC impName impTy)

         log "elab.implementation" 5 $ "Implementation type: " ++ show impTy

         when (typePass pass) $ processDecl [] nest env impTyDecl

         -- If the body is empty, we're done for now (just declaring that
         -- the implementation exists and define it later)
         when (defPass pass) $
           whenJust mbody $ \body_in => do
               defs <- get Ctxt
               Just impTyc <- lookupTyExact impName (gamma defs)
                    | Nothing => throw (InternalError ("Can't happen, can't find type of " ++ show impName))
               methImps <- getMethImps [] impTyc
               log "elab.implementation" 3 $ "Bind implicits to each method: " ++ show methImps

               -- 1.5. Lookup default definitions and add them to the body
               let (body, missing)
                     = addDefaults vfc impName
                                      (zip (params cdata) ps)
                                      (map (dropNS . name) (methods cdata))
                                      (defaults cdata) body_in

               log "elab.implementation" 5 $ "Added defaults: body is " ++ show body
               log "elab.implementation" 5 $ "Missing methods: " ++ show missing
               when (not (isNil missing)) $
                 throw (GenericMsg ifc ("Missing methods in " ++ show iname ++ ": "
                                        ++ showSep ", " (map show missing)))

               -- Add the 'using' hints
               defs <- get Ctxt
               let hs = openHints defs -- snapshot open hint state
               log "elab.implementation" 10 $ "Open hints: " ++ (show (impName :: nusing))
               traverse_ (\n => do n' <- checkUnambig vfc n
                                   addOpenHint n') nusing

               -- 2. Elaborate top level function types for this interface
               defs <- get Ctxt
               fns <- topMethTypes [] impName methImps impsp
                                      (implParams cdata) (params cdata)
                                      (map name (methods cdata))
                                      (methods cdata)
               traverse_ (processDecl [] nest env) (map mkTopMethDecl fns)

               -- 3. Build the record for the implementation
               let mtops = map (Builtin.fst . snd) fns
               let con = iconstructor cdata
               let ilhs = impsApply (IVar EmptyFC impName)
                                    (map (\x => (x, IBindVar vfc (show x)))
                                              (map fst methImps))
               -- RHS is the constructor applied to a search for the necessary
               -- parent constraints, then the method implementations
               defs <- get Ctxt
               let fldTys = getFieldArgs !(normaliseHoles defs [] conty)
               log "elab.implementation" 5 $ "Field types " ++ show fldTys
               let irhs = apply (autoImpsApply (IVar vfc con) $ map (const (ISearch vfc 500)) (parents cdata))
                                  (map (mkMethField methImps fldTys) fns)
               let impFn = IDef vfc impName [PatClause vfc ilhs irhs]
               log "elab.implementation" 5 $ "Implementation record: " ++ show impFn

               -- If it's a named implementation, add it as a global hint while
               -- elaborating the record and bodies
               when named $ addOpenHint impName

               -- Make sure we don't use this name to solve parent constraints
               -- when elaborating the record, or we'll end up in a cycle!
               setFlag vfc impName BlockedHint

               -- Update nested names so we elaborate the body in the right
               -- environment
               names' <- traverse applyEnv (impName :: mtops)
               let nest' = record { names $= (names' ++) } nest

               traverse_ (processDecl [] nest' env) [impFn]
               unsetFlag vfc impName BlockedHint

               setFlag vfc impName TCInline
               -- it's the methods we're interested in, not the implementation
               setFlag vfc impName (SetTotal PartialOK)

               -- 4. (TODO: Order method bodies to be in declaration order, in
               --    case of dependencies)

               -- 5. Elaborate the method bodies
               let upds = map methNameUpdate fns
               body' <- traverse (updateBody upds) body

               log "elab.implementation" 10 $ "Implementation body: " ++ show body'
               traverse_ (processDecl [] nest' env) body'

               -- 6. Add transformation rules for top level methods
               traverse_ (addTransform impName upds) (methods cdata)

               -- inline flag has done its job, and outside the interface
               -- it can hurt, so unset it now
               unsetFlag vfc impName TCInline

               -- Reset the open hints (remove the named implementation)
               setOpenHints hs

    where
    vfc : FC
    vfc = virtualiseFC ifc

    applyEnv : Name ->
               Core (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars))
    applyEnv n
        = do n' <- resolveName n
             pure (Resolved n', (Nothing, reverse (allVars env),
                      \fn, nt => applyToFull vfc
                                     (Ref vfc nt (Resolved n')) env))

    -- For the method fields in the record, get the arguments we need to abstract
    -- over
    getFieldArgs : Term vs -> List (Name, List (Name, RigCount, PiInfo RawImp))
    getFieldArgs (Bind _ x (Pi _ _ _ ty) sc)
        = (x, getArgs ty) :: getFieldArgs sc
      where
        getArgs : Term vs' -> List (Name, RigCount, PiInfo RawImp)
        getArgs (Bind _ x (Pi _ c p _) sc)
            = (x, c, forgetDef p) :: getArgs sc
        getArgs _ = []
    getFieldArgs _ = []

    impsApply : RawImp -> List (Name, RawImp) -> RawImp
    impsApply fn [] = fn
    impsApply fn ((n, arg) :: ns)
        = impsApply (INamedApp vfc fn n arg) ns

    autoImpsApply : RawImp -> List RawImp -> RawImp
    autoImpsApply f [] = f
    autoImpsApply f (x :: xs) = autoImpsApply (IAutoApp (getFC f) f x) xs

    mkLam : List (Name, RigCount, PiInfo RawImp) -> RawImp -> RawImp
    mkLam [] tm = tm
    mkLam ((x, c, p) :: xs) tm
        = ILam EmptyFC c p (Just x) (Implicit vfc False) (mkLam xs tm)

    applyTo : RawImp -> List (Name, RigCount, PiInfo RawImp) -> RawImp
    applyTo tm [] = tm
    applyTo tm ((x, c, Explicit) :: xs)
        = applyTo (IApp EmptyFC tm (IVar EmptyFC x)) xs
    applyTo tm ((x, c, AutoImplicit) :: xs)
        = applyTo (INamedApp EmptyFC tm x (IVar EmptyFC x)) xs
    applyTo tm ((x, c, Implicit) :: xs)
        = applyTo (INamedApp EmptyFC tm x (IVar EmptyFC x)) xs
    applyTo tm ((x, c, DefImplicit _) :: xs)
        = applyTo (INamedApp EmptyFC tm x (IVar EmptyFC x)) xs

    -- When applying the method in the field for the record, eta expand
    -- the expected arguments based on the field type, so that implicits get
    -- inserted in the right place
    mkMethField : List (Name, RigCount, RawImp) ->
                  List (Name, List (Name, RigCount, PiInfo RawImp)) ->
                  (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> RawImp
    mkMethField methImps fldTys (topn, n, upds, c, treq, ty)
        = let argns = map applyUpdate (maybe [] id (lookup (dropNS topn) fldTys))
              imps = map fst methImps in
              -- Pass through implicit arguments to the function which are also
              -- implicit arguments to the declaration
              mkLam argns
                    (impsApply
                         (applyTo (IVar EmptyFC n) argns)
                         (map (\n => (n, IVar vfc (UN (Basic $ show n)))) imps))
      where
        applyUpdate : (Name, RigCount, PiInfo RawImp) ->
                      (Name, RigCount, PiInfo RawImp)
        applyUpdate (UN (Basic n), c, p)
            = maybe (UN (Basic n), c, p) (\n' => (UN (Basic n'), c, p)) (lookup n upds)
        applyUpdate t = t

    methName : Name -> Name
    methName (NS _ n) = methName n
    methName n
        = DN (show n)
             (UN $ Basic (show n ++ "_" ++ show iname ++ "_" ++
                     (if named then show impName_in else "") ++
                     showSep "_" (map show ps)))

    applyCon : Name -> Name -> Core (Name, RawImp)
    applyCon impl n
        = do mn <- inCurrentNS (methName n)
             pure (dropNS n, IVar vfc mn)

    bindImps : List (Name, RigCount, RawImp) -> RawImp -> RawImp
    bindImps [] ty = ty
    bindImps ((n, c, t) :: ts) ty
        = IPi vfc c Implicit (Just n) t (bindImps ts ty)

    -- Return method name, specialised method name, implicit name updates,
    -- and method type. Also return how the method name should be updated
    -- in later method types (specifically, putting implicits in)
    topMethType : List (Name, RawImp) ->
                  Name -> List (Name, RigCount, RawImp) ->
                  List String -> List Name -> List Name -> List Name ->
                  Method ->
                  Core ((Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp),
                           List (Name, RawImp))
    topMethType methupds impName methImps impsp imppnames pnames allmeths meth
        = do -- Get the specialised type by applying the method to the
             -- parameters
             n <- inCurrentNS (methName meth.name)

             -- Avoid any name clashes between parameters and method types by
             -- renaming IBindVars in the method types which appear in the
             -- parameters
             let upds' = !(traverse (applyCon impName) allmeths)
             let mty_in = substNames vars upds' meth.type
             let (upds, mty_in) = runState Prelude.Nil (renameIBinds impsp (findImplicits mty_in) mty_in)
             -- Finally update the method type so that implicits from the
             -- parameters are passed through to any earlier methods which
             -- appear in the type
             let mty_in = substNames vars methupds mty_in

             -- Substitute _ in for the implicit parameters, then
             -- substitute in the explicit parameters.
             let mty_iparams
                   = substBindVars vars
                                (map (\n => (n, Implicit vfc False)) imppnames)
                                mty_in
             let mty_params
                   = substNames vars (zip pnames ps) mty_iparams
             log "elab.implementation" 5 $ "Substitute implicits " ++ show imppnames ++
                     " parameters " ++ show (zip pnames ps) ++
                     " "  ++ show mty_in ++ " is " ++
                     show mty_params

             let mbase = bindImps methImps $
                         bindConstraints vfc AutoImplicit cons $
                         mty_params
             let ibound = findImplicits mbase

             mty <- bindTypeNamesUsed ifc ibound vars mbase

             log "elab.implementation" 3 $
                     "Method " ++ show meth.name ++ " ==> " ++
                     show n ++ " : " ++ show mty
             log "elab.implementation" 3 $ "    (initially " ++ show mty_in ++ ")"
             log "elab.implementation" 5 $ "Updates " ++ show methupds
             log "elab.implementation" 5 $ "From " ++ show mbase
             log "elab.implementation" 3 $ "Name updates " ++ show upds
             log "elab.implementation" 3 $ "Param names: " ++ show pnames
             log "elab.implementation" 10 $ "Used names " ++ show ibound
             let ibinds = map fst methImps
             let methupds' = if isNil ibinds then []
                             else [(n, impsApply (IVar vfc n)
                                     (map (\x => (x, IBindVar vfc (show x))) ibinds))]

             pure ((meth.name, n, upds, meth.count, meth.totalReq, mty), methupds')

    topMethTypes : List (Name, RawImp) ->
                   Name -> List (Name, RigCount, RawImp) ->
                   List String ->
                   List Name -> List Name -> List Name ->
                   List Method ->
                   Core (List (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp))
    topMethTypes upds impName methImps impsp imppnames pnames allmeths [] = pure []
    topMethTypes upds impName methImps impsp imppnames pnames allmeths (m :: ms)
        = do (m', newupds) <- topMethType upds impName methImps impsp imppnames pnames allmeths m
             ms' <- topMethTypes (newupds ++ upds) impName methImps impsp imppnames pnames allmeths ms
             pure (m' :: ms')

    mkTopMethDecl : (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> ImpDecl
    mkTopMethDecl (mn, n, upds, c, treq, mty)
        = let opts = maybe opts_in (\t => Totality t :: opts_in) treq in
              IClaim vfc c vis opts (MkImpTy EmptyFC EmptyFC n mty)

    -- Given the method type (result of topMethType) return the mapping from
    -- top level method name to current implementation's method name
    methNameUpdate : (Name, Name, t) -> (Name, Name)
    methNameUpdate (UN mn, fn, _) = (UN mn, fn)
    methNameUpdate (NS _ mn, fn, p) = methNameUpdate (mn, fn, p)
    methNameUpdate (mn, fn, p) = (UN (Basic $ nameRoot mn), fn) -- probably impossible

    findMethName : List (Name, Name) -> FC -> Name -> Core Name
    findMethName ns fc n
        = case lookup n ns of
               Nothing => throw (GenericMsg fc
                                (show n ++ " is not a method of " ++
                                 show iname))
               Just n' => pure n'

    updateApp : List (Name, Name) -> RawImp -> Core RawImp
    updateApp ns (IVar fc n)
        = do n' <- findMethName ns fc n
             pure (IVar fc n')
    updateApp ns (IApp fc f arg)
        = do f' <- updateApp ns f
             pure (IApp fc f' arg)
    updateApp ns (IAutoApp fc f arg)
        = do f' <- updateApp ns f
             pure (IAutoApp fc f' arg)
    updateApp ns (INamedApp fc f x arg)
        = do f' <- updateApp ns f
             pure (INamedApp fc f' x arg)
    updateApp ns tm
        = throw (GenericMsg (getFC tm) "Invalid method definition")

    updateClause : List (Name, Name) -> ImpClause ->
                   Core ImpClause
    updateClause ns (PatClause fc lhs rhs)
        = do lhs' <- updateApp ns lhs
             pure (PatClause fc lhs' rhs)
    updateClause ns (WithClause fc lhs wval prf flags cs)
        = do lhs' <- updateApp ns lhs
             cs' <- traverse (updateClause ns) cs
             pure (WithClause fc lhs' wval prf flags cs')
    updateClause ns (ImpossibleClause fc lhs)
        = do lhs' <- updateApp ns lhs
             pure (ImpossibleClause fc lhs')

    updateBody : List (Name, Name) -> ImpDecl -> Core ImpDecl
    updateBody ns (IDef fc n cs)
        = do cs' <- traverse (updateClause ns) cs
             n' <- findMethName ns fc n
             log "ide-mode.highlight" 1 $ show (n, n', fc)
             pure (IDef fc n' cs')
    updateBody ns e
        = throw (GenericMsg (getFC e)
                   "Implementation body can only contain definitions")

    addTransform : Name -> List (Name, Name) ->
                   Method ->
                   Core ()
    addTransform iname ns meth
        = do log "elab.implementation" 3 $
                     "Adding transform for " ++ show meth.name ++ " : " ++ show meth.type ++
                     "\n\tfor " ++ show iname ++ " in " ++ show ns
             let lhs = INamedApp vfc (IVar vfc meth.name)
                                     (UN $ Basic "__con")
                                     (IVar vfc iname)
             let Just mname = lookup (dropNS meth.name) ns
                 | Nothing => pure ()
             let rhs = IVar vfc mname
             log "elab.implementation" 5 $ show lhs ++ " ==> " ++ show rhs
             handleUnify
                 (processDecl [] nest env
                     (ITransform vfc (UN $ Basic (show meth.name ++ " " ++ show iname)) lhs rhs))
                 (\err =>
                     log "elab.implementation" 5 $ "Can't add transform " ++
                                show lhs ++ " ==> " ++ show rhs ++
                             "\n\t" ++ show err)


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 items) newItem = MkData _ (addToData items) where
  addToData : Vect old String -> Vect (S old) String
  addToData [] = [newItem]
  addToData (x :: xs) = x :: addToData xs

sumInputs : Integer -> String -> Maybe (String, Integer)
sumInputs tot inp =
  let val = cast inp in
    if val < 0
      then Nothing
      else let newVal = tot + val in
        Just ("Subtotal: " ++ show newVal ++ "\n", newVal)

data Command =
  Add String |
  Get Integer |
  Search String |
  Quit

parseCommand : (cmd : String) -> (args : 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 "search" substr = Just (Search substr)
parseCommand _ _ = Nothing

parse : 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 store_items ++ "\n", store)

searchData : (substr : String) -> (items : Vect size String) -> String -> Int -> String
searchData substr [] acc index = acc
searchData substr (x :: xs) acc index = case Strings.isInfixOf substr x of
  False => searchData substr xs acc (index + 1)
  True => "" ++ show index ++ ": " ++ x ++ "\n" ++ searchData substr xs acc (index + 1)

searchEntry : (substr : String) -> (store : DataStore) -> Maybe (String, DataStore)
searchEntry substr store@(MkData size items) = Just (searchData substr items "" 0, store)

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store inp = case parse inp 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 (Search substr) => searchEntry substr store
  Just Quit => Nothing

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

-- Exercise 1 is size above, not sure why it's in the exercises.
-- Exercise 2 - searchEntry above

ext: idr

max_stars_repo_name: rickyclarkson/idris-playground

max_issues_repo_name: rickyclarkson/idris-playground

max_forks_repo_name: rickyclarkson/idris-playground


text:
data Fin : Nat -> Type where
    FS : Fin k -> Fin (S k)
    FZ : Fin (S k)

%builtin Natural Fin


text:
module IdrisScript.Date.Days

import IdrisScript

%access public export

data Day = Monday
         | Tuesday
         | Wednesday
         | Thursday
         | Friday
         | Saturday
         | Sunday

implementation Eq Day where
  Monday    == Monday    = True
  Tuesday   == Tuesday   = True
  Wednesday == Wednesday = True
  Thursday  == Thursday  = True
  Friday    == Friday    = True
  Saturday  == Saturday  = True
  Sunday    == Sunday    = True
  _         == _         = False

implementation Cast Day Int where
  cast Monday    = 1
  cast Tuesday   = 2
  cast Wednesday = 3
  cast Thursday  = 4
  cast Friday    = 5
  cast Saturday  = 6
  cast Sunday    = 7

implementation Cast Day Integer where
  cast Monday    = 1
  cast Tuesday   = 2
  cast Wednesday = 3
  cast Thursday  = 4
  cast Friday    = 5
  cast Saturday  = 6
  cast Sunday    = 7

implementation Cast Day Nat where
  cast Monday    = 1
  cast Tuesday   = 2
  cast Wednesday = 3
  cast Thursday  = 4
  cast Friday    = 5
  cast Saturday  = 6
  cast Sunday    = 7

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module Http

import public Http.Uri
import public Http.Error
import public Http.RawResponse
import public Http.Request
import public Http.Response
import public Data.SortedMap
import public Data.Vect
import public Network.Socket

%access export

private
sendRequest : Request a -> IO (Either HttpError (RawResponse String))
sendRequest req = do
    Right sock <- socket AF_INET Stream 0 | Left err => pure (Left $ HttpSocketError err)
    0 <- connect sock (Hostname host) port | err => pure (Left $ HttpSocketError err)
    Right _ <- send sock (resolveRequest req) | Left err => pure (Left $ HttpSocketError err)
    Right (str, _) <- recv sock 65536 | Left err => pure (Left $ HttpSocketError err)
    pure (Right (MkRawResponse str))
  where
    host : String
    host = uriHost . uriAuth . uri $ req

    port : Int
    port = uriPort . uriAuth . uri $ req

httpRequest : Request a -> IO (Either HttpError (Response String))
httpRequest req = pure $ !(sendRequest req) >>= parseResponse

simpleHttp : Host -> Port -> (path : String) -> IO (Either HttpError (Response String))
simpleHttp host port path = do
  let headers = Data.SortedMap.fromList [("Host", host ++ ":" ++ show port)]
  repl <- sendRequest (MkRequest GET (MkURI "http" (MkURIAuth Nothing Nothing host port) path [] "") "" headers)
  pure (repl >>= parseResponse)

max_stars_repo_name: unthingable/idris-https

max_issues_repo_name: unthingable/idris-https

max_forks_repo_name: unthingable/idris-https


text:
data D = MkD
data E = MkE

data Proxy i = MkProxy

interface I i where
 (.idot) : i -> Int

I D where
 (.idot) _ = 0

interface J i where
 theInt  : Proxy i -> Int

 (.jdot) : i -> Int
 (.jdot) _ = theInt (the (Proxy i) MkProxy)

 val : i -> Int
 val v = 10 + v .jdot

J D where
  theInt _ = 0

J E where
  theInt _ = 0
  (.jdot) _ = 1
  val _ = 2


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

import Data.Vect

-- check that all functions are total
%default total

--
-- section 8.1
--

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

same_cons : {xs : List a} -> {ys : List a} ->
            xs = ys -> x :: xs = x :: ys
same_cons Refl = Refl

same_lists : {xs : List a} -> {ys : List a} ->
             x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

data ThreeEq : a -> b -> c -> Type where
  Same3 : ThreeEq n n n

-- for all three natural numbers,
-- if the three numbers are equal then their three successors are equal
allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS z z z Same3 = Same3

-- > allSameS 2 3 2 Same3
-- (input):1:1-20:When checking an application of function Main.allSameS:
--         Type mismatch between
--                 ThreeEq n n n (Type of Same3)
--         and
--                 ThreeEq 2 3 2 (Expected type)
--
--         Specifically:
--                 Type mismatch between
--                         0
--                 and
--                         1
-- > allSameS 2 2 2 Same3
-- Same3 : ThreeEq 3 3 3

--
-- section 8.2
--

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = rewrite sym (plusZeroRightNeutral m) in Refl
myPlusCommutes (S k) m = rewrite myPlusCommutes k m in
                         rewrite plusSuccRightSucc m k in Refl

reverseProof_nil : Vect n1 a -> Vect (plus n1 0) a
reverseProof_nil {n1} xs = rewrite plusZeroRightNeutral n1 in xs

reverseProof_xs : Vect (S (plus n1 len)) a -> Vect (plus n1 (S len)) a
reverseProof_xs {n1} {len} xs = rewrite sym (plusSuccRightSucc n1 len) in xs

myReverse : Vect n a -> Vect n a
myReverse xs = reverse [] xs
  where
    reverse : Vect n a -> Vect m a -> Vect (n+m) a
    reverse acc [] = reverseProof_nil acc
    reverse acc (x :: xs) = reverseProof_xs (reverse (x :: acc) xs)

--
-- section 8.3
--

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

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

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

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Ch03.Arith

import public Ch03.Relations

%default total
%access public export

----------------------------
-- Term syntax
----------------------------

namespace Terms
  data Term = True
            | False
            | IfThenElse Term Term Term
            | Zero
            | Succ Term
            | Pred Term
            | IsZero Term

namespace Values
  mutual
    Value : Type
    Value = Either BoolValue NumValue

    data BoolValue = True | False
    data NumValue = Zero | Succ NumValue

||| Converts a boolean value to its corresponding term
bv2t : BoolValue -> Term
bv2t True = True
bv2t False = False

||| Converts a numeric value to its corresponding term
nv2t : NumValue -> Term
nv2t Zero = Zero
nv2t (Succ x) = Succ (nv2t x)

||| Converts a value to its corresponding term
v2t : Value -> Term
v2t (Left bv) = bv2t bv
v2t (Right nv) = nv2t nv

namespace IsValue
  ||| Propositional type describing that a term "is" indeed a value
  data IsValue : Term -> Type where
    ConvertedFrom : (v : Value) -> IsValue (v2t v)

namespace IsNumValue
  ||| Propositional type describing that a term "is" indeed a numeric value
  data IsNumValue : Term -> Type where
    ConvertedFrom : (nv : NumValue) -> IsNumValue (v2t (Right nv))

namespace IsBoolValue
  ||| Propositional type describing that a term "is" indeed a boolean value
  data IsBoolValue : Term -> Type where
    ConvertedFrom : (bv : BoolValue) -> IsBoolValue (v2t (Left bv))

----------------------------
-- Evaluation rules
----------------------------

||| Propositional type describing that the first term one-step-evaluates to the second
|||
||| Explicitly, an inhabitant of `EvalsTo t1 t2` is a proof that `t1` evaluates to `t2` in one step.
data EvalsTo : Term -> Term -> Type where
  EIfTrue : EvalsTo (IfThenElse True t2 t3) t2
  EIfFalse : EvalsTo (IfThenElse False t2 t3) t3
  EIf : EvalsTo t1 t1' -> EvalsTo (IfThenElse t1 t2 t3) (IfThenElse t1' t2 t3)
  ESucc : EvalsTo t1 t2 -> EvalsTo (Succ t1) (Succ t2)
  EPredZero : EvalsTo (Pred Zero) Zero
  EPredSucc : {pf : IsNumValue nv1} -> EvalsTo (Pred (Succ nv1)) nv1
  EPred : EvalsTo t1 t2 -> EvalsTo (Pred t1) (Pred t2)
  EIsZeroZero : EvalsTo (IsZero Zero) True
  EIsZeroSucc : {pf : IsNumValue nv1} -> EvalsTo (IsZero (Succ nv1)) False
  EIsZero : EvalsTo t1 t2 -> EvalsTo (IsZero t1) (IsZero t2)

||| Propositional type describing that the first term evaluates to the second in a finite number of steps
|||
||| Explicitly, an inhabitant of `EvalToStar t1 t2` is a proof that there is a finite sequence
|||
|||     t1 = s_0, s_1, ..., s_n = t2
|||
||| of terms (where `0 <= n`), such that `s_i` one-step-evaluates to `s_{i+1}`.
EvalsToStar : Term -> Term -> Type
EvalsToStar = ReflSymmClos EvalsTo

----------------------------
-- Big Step Evaluation rules
----------------------------

||| Propositional type describing that the first term big-step evaluates to the second
data BigEvalsTo : Term -> Term -> Type where
  BValue : {pf : IsValue v} -> BigEvalsTo v v
  BIfTrue : {pf : IsValue v2} ->
            BigEvalsTo t1 True ->
            BigEvalsTo t2 v2 ->
            BigEvalsTo (IfThenElse t1 t2 t3) v2
  BIfFalse : {pf : IsValue v3} ->
             BigEvalsTo t1 False ->
             BigEvalsTo t3 v3 ->
             BigEvalsTo (IfThenElse t1 t2 t3) v3
  BSucc : {pf : IsNumValue nv1} ->
          BigEvalsTo t1 nv1 ->
          BigEvalsTo (Succ t1) (Succ nv1)
  BPredZero : BigEvalsTo t1 Zero ->
              BigEvalsTo (Pred t1) Zero
  BPredSucc : {pf : IsNumValue nv1} ->
              BigEvalsTo t1 (Succ nv1) ->
              BigEvalsTo (Pred t1) nv1
  BIsZeroZero : BigEvalsTo t1 Zero ->
                BigEvalsTo (IsZero t1) True
  BIsZeroSucc : {pf : IsNumValue nv1} ->
                BigEvalsTo t1 (Succ nv1) ->
                BigEvalsTo (IsZero t1) False

--------------------------------------------------------------------------------
-- Some properties of values and evaluation
--------------------------------------------------------------------------------

||| A numeric value is also a value
numValueIsValue : IsNumValue t -> IsValue t
numValueIsValue {t = (v2t (Right nv))} (ConvertedFrom nv) = IsValue.ConvertedFrom (Right nv)

||| The successor of a numeric value is a numeric value
succNumValueIsNumValue : IsNumValue t -> IsNumValue (Succ t)
succNumValueIsNumValue {t = (v2t (Right nv))} (ConvertedFrom nv) = ConvertedFrom (Succ nv)

||| A boolean value is also a value
boolValueIsValue : IsBoolValue t -> IsValue t
boolValueIsValue {t = (v2t (Left bv))} (ConvertedFrom bv) = IsValue.ConvertedFrom (Left bv)

numValueEither : IsNumValue t -> Either (t = Zero) (t' : Term ** (IsNumValue t', t = Succ t'))
numValueEither (ConvertedFrom nv) = case nv of
                                         Zero => Left Refl
                                         (Succ nv') => Right (nv2t nv' ** (ConvertedFrom nv', Refl))

boolValueEither : IsBoolValue t -> Either (t = True) (t = False)
boolValueEither (ConvertedFrom True) = Left Refl
boolValueEither (ConvertedFrom False) = Right Refl

zeroNotBool : IsBoolValue Zero -> Void
zeroNotBool (ConvertedFrom True) impossible
zeroNotBool (ConvertedFrom False) impossible

succNotTrue : {t : Term} -> (Succ t = True) -> Void
succNotTrue Refl impossible

succNotFalse : {t : Term} -> (Succ t = False) -> Void
succNotFalse Refl impossible

succNotBool : IsBoolValue (Succ t) -> Void
succNotBool {t} x = case boolValueEither x of
                         (Left l) => succNotTrue l
                         (Right r) => succNotFalse r

||| A value can't be both numeric and boolean at the same time.
numNotBool : IsNumValue t -> IsBoolValue t -> Void
numNotBool x y = case numValueEither x of
                      (Left Refl) => zeroNotBool y
                      (Right (_ ** (_, Refl))) => succNotBool y

||| Proof that values don't evaluate to anything in the `E`-calculus.
valuesDontEvaluate : {pf : IsValue v} -> EvalsTo v t -> Void
valuesDontEvaluate {pf = (ConvertedFrom (Left bv))} {v = (bv2t bv)} x = case bv of
                                                                             True => (case x of
                                                                                EIfTrue impossible
                                                                                EIfFalse impossible
                                                                                (EIf _) impossible
                                                                                (ESucc _) impossible
                                                                                EPredZero impossible
                                                                                EPredSucc impossible
                                                                                (EPred _) impossible
                                                                                EIsZeroZero impossible
                                                                                EIsZeroSucc impossible
                                                                                (EIsZero _) impossible)
                                                                             False => (case x of
                                                                                EIfTrue impossible
                                                                                EIfFalse impossible
                                                                                (EIf _) impossible
                                                                                (ESucc _) impossible
                                                                                EPredZero impossible
                                                                                EPredSucc impossible
                                                                                (EPred _) impossible
                                                                                EIsZeroZero impossible
                                                                                EIsZeroSucc impossible
                                                                                (EIsZero _) impossible)
valuesDontEvaluate {pf = (ConvertedFrom (Right nv))} {v = (nv2t nv)} x = case nv of
                                                                              Zero => (case x of
                                                                                EIfTrue impossible
                                                                                EIfFalse impossible
                                                                                (EIf _) impossible
                                                                                (ESucc _) impossible
                                                                                EPredZero impossible
                                                                                EPredSucc impossible
                                                                                (EPred _) impossible
                                                                                EIsZeroZero impossible
                                                                                EIsZeroSucc impossible
                                                                                (EIsZero _) impossible)
                                                                              (Succ nv) => (case x of
                                                                                (ESucc y) => valuesDontEvaluate {pf=ConvertedFrom (Right nv)} y)

||| Proof that the only derivation of a value term in the reflexive transitive of the `E`-evaluation rules
||| is the trivial derivation.
valuesAreNormal : {pf : IsValue v} -> (r : EvalsToStar v t) -> (r = (Refl {rel=EvalsTo} {x=v}))
valuesAreNormal (Refl {x}) = Refl
valuesAreNormal {pf} (Cons x y) with (valuesDontEvaluate {pf=pf} x)
  valuesAreNormal {pf} (Cons x y) | with_pat impossible

||| Proof that a value is either
|||
|||     1. `True`
|||     2. `False`
|||     3. `Zero`
|||     4. `Succ nv`, with `nv` a numeric value
valueIsEither : (v : Term) -> {pf : IsValue v} -> Either (v = True) (Either (v = False) (Either (v = Zero) (nv : Term ** ((v = Succ nv), IsNumValue nv))))
valueIsEither (bv2t x) {pf = (ConvertedFrom (Left x))} = case x of
                                                              True => Left Refl
                                                              False => Right (Left Refl)
valueIsEither (nv2t x) {pf = (ConvertedFrom (Right x))} = case x of
                                                               Zero => Right (Right (Left Refl))
                                                               (Succ y) => Right (Right (Right (nv2t y ** (Refl, ConvertedFrom y))))

||| Proof that a term of the form `Succ t` is only a value if `t` is a numeric value.
succIsValueIf : IsValue (Succ t) -> IsNumValue t
succIsValueIf (ConvertedFrom (Left Values.True)) impossible
succIsValueIf (ConvertedFrom (Left Values.False)) impossible
succIsValueIf (ConvertedFrom (Right Values.Zero)) impossible
succIsValueIf (ConvertedFrom (Right (Succ nv))) = ConvertedFrom nv

||| Proof that a term of the form `Pred t` is never a value.
predNotValue : IsValue (Pred t) -> Void
predNotValue (ConvertedFrom (Left Values.True)) impossible
predNotValue (ConvertedFrom (Left Values.False)) impossible
predNotValue (ConvertedFrom (Right Values.Zero)) impossible
predNotValue (ConvertedFrom (Right (Values.Succ nv))) impossible

||| Proof that a term of the form `IsZero t` is never a value.
isZeroNotValue : IsValue (IsZero t) -> Void
isZeroNotValue (ConvertedFrom (Left Values.True)) impossible
isZeroNotValue (ConvertedFrom (Left Values.False)) impossible
isZeroNotValue (ConvertedFrom (Right Values.Zero)) impossible
isZeroNotValue (ConvertedFrom (Right (Values.Succ nv))) impossible

||| Proof that a value only evaluates to itself under the reflexive transitive closure of
||| the `E`-evaluation rules.
valuesAreNormal' : {pf : IsValue v} ->
                   EvalsToStar v t ->
                   (t = v)
valuesAreNormal' {pf} x with (valuesAreNormal {pf=pf} x)
  valuesAreNormal' {pf} x | with_pat = case with_pat of
                                            Refl => Refl

||| Proof that a term of the form `IfThenElse x y z` is never a value.
ifThenElseNotNormal : (pf : IsValue (IfThenElse x y z)) -> Void
ifThenElseNotNormal {x} {y} {z} pf with (valueIsEither (IfThenElse x y z) {pf=pf})
  ifThenElseNotNormal {x} {y} {z} pf | (Left l) = case l of
                                                       Refl impossible
  ifThenElseNotNormal {x} {y} {z} pf | (Right (Left l)) = case l of
                                                               Refl impossible
  ifThenElseNotNormal {x} {y} {z} pf | (Right (Right (Left l))) = case l of
                                                                       Refl impossible
  ifThenElseNotNormal {x} {y} {z} pf | (Right (Right (Right (nv ** (pf1, pf2))))) = case pf1 of
                                                                                Refl impossible
----------------------------
-- Miscellanea
----------------------------

t1 : Term
t1 = IfThenElse False Zero (Succ Zero)

t2 : Term
t2 = IsZero (Pred (Succ Zero))

toString : Term -> String
toString True = "true"
toString False = "false"
toString (IfThenElse x y z) = "if " ++ toString x ++
                              " then " ++ toString y ++
                              " else " ++ toString z
toString Zero = "0"
toString (Succ x) = "succ (" ++ toString x ++ ")"
toString (Pred x) = "pred (" ++ toString x ++ ")"
toString (IsZero x) = "iszero (" ++ toString x ++ ")"

eval : Term -> Value
eval True = Left True
eval False = Left True
eval (IfThenElse x y z) = case eval x of
                               (Left r) => case r of
                                                True => eval y
                                                False => eval z
                               (Right l) => ?eval_rhs_1
eval Zero = Right Zero
eval (Succ x) = case eval x of
                     Left l => ?eval_rhs_4
                     Right r => Right (Succ r)
eval (Pred x) = case eval x of
                     Left l => ?eval_rhs_5
                     Right r => case r of
                                     Zero => Right Zero
                                     Succ x => Right x
eval (IsZero x) = case x of
                       Zero => Left True
                       Succ y => Left False
                       _ => ?eval_rhs2

||| The size of a term is the number of constructors it contains.
size : Term -> Nat
size True = 1
size False = 1
size (IfThenElse x y z) = (size x) + (size y) + (size z) + 1
size Zero = 1
size (Succ x) = S (size x)
size (Pred x) = S (size x)
size (IsZero x) = S (size x)

||| The depth of a term is depth of its derivation tree.
depth : Term -> Nat
depth True = 1
depth False = 1
depth (IfThenElse x y z) = (max (depth x) (max (depth y) (depth z))) + 1
depth Zero = 1
depth (Succ x) = S (depth x)
depth (Pred x) = S (depth x)
depth (IsZero x) = S (depth x)

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module Language.LSP.Message.Initialize

import Language.JSON
import Language.LSP.Message.ClientCapabilities
import Language.LSP.Message.Derive
import Language.LSP.Message.Progress
import Language.LSP.Message.ServerCapabilities
import Language.LSP.Message.Trace
import Language.LSP.Message.URI
import Language.LSP.Message.Utils
import Language.LSP.Message.Workspace
import Language.Reflection

%language ElabReflection
%default total

namespace InitializeParams
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
  public export
  record ClientInfo where
    name    : String
    version : Maybe String
  %runElab deriveJSON defaultOpts `{{ClientInfo}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record InitializeParams where
  constructor MkInitializeParams
  processId         : OneOf [Integer, Null]
  clientInfo        : Maybe ClientInfo
  locale            : Maybe String
  rootPath          : Maybe (OneOf [String, Null])
  rootUri           : OneOf [URI, Null]
  initializeOptions : Maybe JSON
  capabilities      : ClientCapabilities
  trace             : Maybe Trace
  workspaceFolders  : Maybe (OneOf [List WorkspaceFolder, Null])
  workDoneToken     : Maybe ProgressToken
%runElab deriveJSON defaultOpts `{{InitializeParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record InitializeResult where
  constructor MkInitializeResult
  capabilities : ServerCapabilities
  serverInfo   : Maybe ServerInfo
%runElab deriveJSON defaultOpts `{{InitializeResult}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record InitializeError where
  constructor MkInitializeError
  retry : Bool
%runElab deriveJSON defaultOpts `{{InitializeError}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialized
public export
record InitializedParams where
  constructor MkInitializedParams
%runElab deriveJSON defaultOpts `{{InitializedParams}}


text:
module TestArgs

import Data.List
import System

main : IO ()
main = getArgs >>= (putStrLn . show . drop 2)


text:
module Addition.Scaling

import Common.Util
import Common.Interfaces
import Specifications.Ring
import Proofs.SemigroupTheory
import Proofs.RingTheory
import Addition.Carry

%default total
%access export

scalingLemmaM : Ringops s => UnitalRingSpec {s} (+) Zero Ng (*) One ->
  (radix : s) ->
  scale Zero Ng radix M = radix * value M
scalingLemmaM spec radix = o2 @== o1 where
  o1 : Ng (radix * One) = radix * Ng One
  o1 = negatedMultiplication (ring spec) radix One
  o2 : Ng (radix * One) = Ng radix
  o2 = cong $ neutralR (multiplicativeMonoid spec) radix

scalingLemma : Ringops s => UnitalRingSpec {s} (+) Zero Ng (*) One ->
    (radix : s) -> (c : Carry) ->
    scale Zero Ng radix c = radix * value c
scalingLemma spec radix P = sym $ neutralR (multiplicativeMonoid spec) radix
scalingLemma spec radix O = sym $ zeroAbsorbsR (ring spec) radix
scalingLemma spec radix M = scalingLemmaM spec radix

rewriteInvariant : Ringops s => UnitalRingSpec {s} (+) Zero Ng (*) One ->
  (radix, i, o : s) ->
  (c : Carry) ->
  scale Zero Ng radix c + o = i ->
  o + radix * value c = i
rewriteInvariant spec radix i o c invariant = o2 @== invariant where
  o1 : scale Zero Ng radix c = radix * value c
  o1 = scalingLemma spec radix c
  o2 : scale Zero Ng radix c + o = o + radix * value c
  o2 = abelianCongruence (plusAbelian (ring spec)) o1

max_stars_repo_name: jeroennoels/verified-exact-real

max_issues_repo_name: jeroennoels/verified-exact-real

max_forks_repo_name: jeroennoels/verified-exact-real


text:
module Hedgehog.Internal.Report

import Data.List1
import Data.Nat
import Data.SortedMap
import Generics.Derive
import Hedgehog.Internal.Config
import Hedgehog.Internal.Property
import Hedgehog.Internal.Range
import Hedgehog.Internal.Seed
import Hedgehog.Internal.Util
import Text.Show.Diff
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.Terminal as Term
import Text.PrettyPrint.Prettyprinter.Render.String   as Str

%default total

%language ElabReflection

--------------------------------------------------------------------------------
--          Reporting
--------------------------------------------------------------------------------

public export
record FailedAnnotation where
  constructor MkFailedAnnotation
  failedValue : String

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

public export
record FailureReport where
  constructor MkFailureReport
  size        : Size
  seed        : Seed
  shrinks     : ShrinkCount
  coverage    : Maybe (Coverage CoverCount)
  annotations : List FailedAnnotation
  message     : String
  diff        : Maybe Diff
  footnotes   : List String

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

||| The status of a running property test.
public export
data Progress = Running | Shrinking FailureReport

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

||| The status of a completed property test.
|||
||| In the case of a failure it provides the seed used for the test, the
||| number of shrinks, and the execution log.
public export
data Result = Failed FailureReport | OK

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

public export
isFailure : Result -> Bool
isFailure (Failed _) = True
isFailure OK         = False

public export
isSuccess : Result -> Bool
isSuccess = not . isFailure

||| A report on a running or completed property test.
public export
record Report a where
  constructor MkReport
  tests    : TestCount
  coverage : Coverage CoverCount
  status   : a

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

export
Functor Report where
  map f = {status $= f}

export
Foldable Report where
  foldl f acc   = f acc . status
  foldr f acc r = f r.status acc
  null _        = False

export
Traversable Report where
  traverse f (MkReport t c a) = MkReport t c <$> f a

||| A summary of all the properties executed.
public export
record Summary where
  constructor MkSummary
  waiting : PropertyCount
  running : PropertyCount
  failed  : PropertyCount
  ok      : PropertyCount

%runElab derive "Summary" [Generic,Meta,Show,Eq,Semigroup,Monoid]

record ColumnWidth where
  constructor MkColumnWidth
  widthPercentage : Nat
  widthMinimum    : Nat
  widthName       : Nat
  widthNameFail   : Nat

Semigroup ColumnWidth where
  MkColumnWidth p0 m0 n0 f0 <+> MkColumnWidth p1 m1 n1 f1 =
    MkColumnWidth (max p0 p1) (max m0 m1) (max n0 n1) (max f0 f1)

Monoid ColumnWidth where
  neutral = MkColumnWidth 0 0 0 0

||| Construct a summary from a single result.
export
fromResult : Result -> Summary
fromResult (Failed _) = { failed := 1} neutral
fromResult OK         = { ok := 1} neutral

export
summaryCompleted : Summary -> PropertyCount
summaryCompleted (MkSummary _ _ x3 x4) = x3 + x4

export
summaryTotal : Summary -> PropertyCount
summaryTotal (MkSummary x1 x2 x3 x4) = x1 + x2 + x3 + x4

export
takeAnnotation : Lazy Log -> Maybe FailedAnnotation
takeAnnotation (Annotation x) = Just $ MkFailedAnnotation x
takeAnnotation (Footnote _  ) = Nothing
takeAnnotation (LogLabel _  ) = Nothing

export
takeFootnote : Lazy Log -> Maybe String
takeFootnote (Footnote x)   = Just x
takeFootnote (Annotation _) = Nothing
takeFootnote (LogLabel _)   = Nothing

export
mkFailure :  Size
          -> Seed
          -> ShrinkCount
          -> Maybe (Coverage CoverCount)
          -> String
          -> Maybe Diff
          -> List (Lazy Log)
          -> FailureReport
mkFailure size seed shrinks mcoverage message diff logs =
  let inputs    = mapMaybe takeAnnotation logs
      footnotes = mapMaybe takeFootnote logs
   in MkFailureReport size seed shrinks mcoverage inputs message diff footnotes

--------------------------------------------------------------------------------
--          Pretty Printing
--------------------------------------------------------------------------------

public export
data MarkupStyle = StyleDefault | StyleAnnotation | StyleFailure

export
Semigroup MarkupStyle where
  StyleFailure    <+> _               = StyleFailure
  _               <+> StyleFailure    = StyleFailure
  StyleAnnotation <+> _               = StyleAnnotation
  _               <+> StyleAnnotation = StyleAnnotation
  StyleDefault    <+> _               = StyleDefault

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

public export
data Markup =
    WaitingIcon
  | WaitingHeader
  | RunningIcon
  | RunningHeader
  | ShrinkingIcon
  | ShrinkingHeader
  | FailedIcon
  | FailedText
  | SuccessIcon
  | SuccessText
  | CoverageIcon
  | CoverageText
  | CoverageFill
  | StyledBorder MarkupStyle
  | AnnotationValue
  | DiffPrefix
  | DiffInfix
  | DiffSuffix
  | DiffSame
  | DiffRemoved
  | DiffAdded
  | ReproduceHeader
  | ReproduceGutter
  | ReproduceSource

ppShow : Show x => x -> Doc ann
ppShow = pretty . show

markup : Markup -> Doc Markup -> Doc Markup
markup = annotate

gutter : Markup -> Doc Markup -> Doc Markup
gutter m x = markup m ">" <++> x

icon : Markup -> Char -> Doc Markup -> Doc Markup
icon m i x = markup m (pretty i) <++> x

ppTestCount : TestCount -> Doc ann
ppTestCount (MkTagged 1) = "1 test"
ppTestCount (MkTagged n) = ppShow n <++> "tests"

ppShrinkCount : ShrinkCount -> Doc ann
ppShrinkCount (MkTagged 1) = "1 shrink"
ppShrinkCount (MkTagged n) = ppShow n <++> "shrinks"

ppRawPropertyCount : PropertyCount -> Doc ann
ppRawPropertyCount (MkTagged n) = ppShow n

ppLineDiff : LineDiff -> Doc Markup
ppLineDiff (LineSame x)    = markup DiffSame    $ "  " <+> pretty x
ppLineDiff (LineRemoved x) = markup DiffRemoved $ "- " <+> pretty x
ppLineDiff (LineAdded x)   = markup DiffAdded   $ "+ " <+> pretty x

ppDiff : Diff -> List (Doc Markup)
ppDiff (MkDiff pre removed inf added suffix diff) =
    ( markup DiffPrefix (pretty pre)      <+>
      markup DiffRemoved (pretty removed) <+>
      markup DiffInfix (pretty inf)       <+>
      markup DiffAdded (pretty added)     <+>
      markup DiffSuffix (pretty suffix)
    ) :: map ppLineDiff (toLineDiff diff)

ppLabelName : LabelName -> Doc ann
ppLabelName = pretty . unTag

renderCoverPercentage : CoverPercentage -> String
renderCoverPercentage (MkTagged p) =
  show (round {a = Double} (p * 10.0) / 10.0) <+> "%"

ppCoverPercentage : CoverPercentage -> Doc Markup
ppCoverPercentage = pretty . renderCoverPercentage

ppReproduce : Maybe PropertyName -> Size -> Seed -> Doc Markup
ppReproduce name size seed =
  vsep [
    markup ReproduceHeader "This failure can be reproduced by running:"
  , gutter ReproduceGutter . markup ReproduceSource $
        "recheck" <++>
        pretty (showPrec App size) <++>
        pretty (showPrec App seed) <++>
        maybe "<property>" (pretty . unTag) name
  ]

ppTextLines : String -> List (Doc Markup)
ppTextLines = map pretty . lines

ppFailedInput : Nat -> FailedAnnotation -> Doc Markup
ppFailedInput ix (MkFailedAnnotation val) =
  vsep [
    "forAll" <++> ppShow ix <++> "="
  , indent 2 . vsep . map (markup AnnotationValue . pretty) $ lines val
  ]

ppFailureReport :  Maybe PropertyName
                -> TestCount
                -> FailureReport
                -> List (Doc Markup)
ppFailureReport nm tests (MkFailureReport si se _ mcover inputs msg mdiff msgs0) =
  whenSome (neutral ::)         .
  whenSome (++ [neutral])       .
  punctuate line                .
  map (vsep . map (indent 2))   .
  filter (\xs => not $ null xs) $
  [punctuate line args, coverage, docs, bottom]

  where whenSome : Foldable t => (t a -> t a) -> t a -> t a
        whenSome f xs = if null xs then xs else f xs

        bottom : List (Doc Markup)
        bottom = maybe [ppReproduce nm si se] (const Nil) mcover

        docs : List (Doc Markup)
        docs = concatMap ppTextLines (msgs0 ++ if msg == "" then [] else [msg])
             <+> maybe [] ppDiff mdiff

        args : List (Doc Markup)
        args = zipWith ppFailedInput [0 .. length inputs] (reverse inputs)

        coverage : List (Doc Markup)
        coverage =
          case mcover of
            Nothing => []
            Just c  => do MkLabel _ _ count <- coverageFailures tests c
                          pure $
                            cat [ "Failed ("
                                , annotate CoverageText $
                                    ppCoverPercentage (coverPercentage tests count)
                                    <+> " coverage"
                                , ")"
                                ]

ppName : Maybe PropertyName -> Doc ann
ppName Nothing                = "<interactive>"
ppName (Just $ MkTagged name) = pretty name

labelWidth : TestCount -> Label CoverCount -> ColumnWidth
labelWidth tests x =
  let percentage = length .
                   renderCoverPercentage $
                   coverPercentage tests x.labelAnnotation

      minimum = if x.labelMinimum == 0
                   then the Nat 0
                   else length .
                        renderCoverPercentage $
                        x.labelMinimum

      name = length . unTag $ x.labelName

      nameFail = if labelCovered tests x then the Nat 0 else name

  in MkColumnWidth percentage minimum name nameFail

coverageWidth : TestCount -> Coverage CoverCount -> ColumnWidth
coverageWidth tests (MkCoverage labels) = concatMap (labelWidth tests) labels

ppLeftPad : Nat -> Doc ann -> Doc ann
ppLeftPad n doc =
  let ndoc = length (show doc)
      pad  = pretty . pack $ replicate (n `minus` ndoc) ' '
   in pad <+> doc

ppCoverBar : CoverPercentage -> CoverPercentage -> Doc Markup
ppCoverBar (MkTagged percentage) (MkTagged minimum) =
  let barWidth         = the Nat 20
      coverageRatio    = percentage / 100.0
      coverageWidth    = toNat . floor $ coverageRatio * cast barWidth
      minimumRatio     = minimum / 100.0
      minimumWidth     = toNat . floor $ minimumRatio * cast barWidth
      fillWidth        = pred $ barWidth `minus` coverageWidth
      fillErrorWidth   = pred $ minimumWidth `minus` coverageWidth
      fillSurplusWidth = fillWidth `minus` fillErrorWidth
      full             = '█'
      parts1           = '·' ::: ['▏','▎','▍','▌','▋','▊','▉']
      parts            = forget parts1

      ix               = toNat . floor $
                         ((coverageRatio * cast barWidth) - cast coverageWidth)
                         * cast (length parts)

      part             = case inBounds ix parts of
                              Yes ib => index ix parts
                              No  _  => head parts1

   in hcat [ pretty . pack $ replicate coverageWidth full
           , if coverageWidth < barWidth then
               if ix == 0 then
                 if fillErrorWidth > 0 then annotate FailedText $ pretty part
                 else annotate CoverageFill $ pretty part
               else pretty part
             else ""
           , annotate FailedText . pretty  . pack $
               replicate fillErrorWidth (head parts1)
           , annotate CoverageFill . pretty . pack $
               replicate fillSurplusWidth (head parts1)
           ]

ppLabel : TestCount -> ColumnWidth -> Label CoverCount -> Doc Markup
ppLabel tests w x@(MkLabel name minimum count) =
  let covered  = labelCovered tests x
      ltext    = if not covered then annotate CoverageText else id
      lborder  = annotate (StyledBorder StyleDefault)
      licon    = if not covered then annotate CoverageText "⚠ " else "  "
      lname    = fill (cast w.widthName) (ppLabelName name)
      wminimum = ppLeftPad w.widthMinimum $ ppCoverPercentage minimum
      lcover   = wcover ""

      lminimum =
        if w.widthMinimum == 0 then neutral
        else if not covered then " ✗ " <+> wminimum
        else if minimum == 0 then "   " <+> ppLeftPad w.widthMinimum ""
        else " ✓ " <+> wminimum

   in hcat [ licon
           , ltext lname
           , lborder " "
           , ltext lcover
           , lborder " "
           , ltext $ ppCoverBar (coverPercentage tests count) minimum
           , lborder ""
           , ltext lminimum
           ]

  where wcover : String -> Doc Markup
        wcover i = ppLeftPad (w.widthPercentage + length i) $
                   pretty i <+>
                   ppCoverPercentage (coverPercentage tests count)

ppCoverage : TestCount -> Coverage CoverCount -> List (Doc Markup)
ppCoverage tests x =
  map (ppLabel tests (coverageWidth tests x)) $
  values x.coverageLabels

ppWhenNonZero : Doc ann -> PropertyCount -> Maybe (Doc ann)
ppWhenNonZero _      0 = Nothing
ppWhenNonZero suffix n = Just $ ppRawPropertyCount n <++> suffix

export
ppProgress : Maybe PropertyName -> Report Progress -> Doc Markup
ppProgress name (MkReport tests coverage status) =
  case status of
     Running =>
       vsep $ [ icon RunningIcon '●' . annotate RunningHeader $
                ppName name <++>
                "passed" <++>
                ppTestCount tests <+> "(running)"
              ] ++ ppCoverage tests coverage

     Shrinking failure =>
       icon ShrinkingIcon '↯' . annotate ShrinkingHeader $
         ppName name <++> "failed after" <++> ppTestCount tests

annotateSummary : Summary -> Doc Markup -> Doc Markup
annotateSummary summary =
  if summary.failed > 0 then
    icon FailedIcon '✗' . annotate FailedText
  else if summary.waiting > 0 || summary.running > 0 then
    icon WaitingIcon '○' . annotate WaitingHeader
  else
    icon SuccessIcon '✓' . annotate SuccessText

ppResult : Maybe PropertyName -> Report Result -> Doc Markup
ppResult name (MkReport tests coverage result) =
  case result of
    Failed failure =>
      vsep $ [ icon FailedIcon '✗' . align . annotate FailedText $
               ppName name <++>
               "failed after" <++>
               ppTestCount tests <+>
               "."
             ] ++
             ppCoverage tests coverage ++
             ppFailureReport name tests failure

    OK => vsep $ [ icon SuccessIcon '✓' . annotate SuccessText $
                   ppName name <++>
                   "passed" <++>
                   ppTestCount tests <+>
                   "."
                 ] ++
                 ppCoverage tests coverage

export
ppSummary : Summary -> Doc Markup
ppSummary summary =
  let complete = summaryCompleted summary == summaryTotal summary
      suffix = if complete then the (Doc Markup) "." else " (running)"

   in annotateSummary summary .
      (<+> suffix) .
      hcat .
      addPrefix complete .
      punctuate ", " $
      catMaybes [
          ppWhenNonZero "failed" summary.failed
        , if complete then
            ppWhenNonZero "succeeded" summary.ok
          else
            Nothing
      ]

  where doPrefix : Bool -> Doc Markup -> Doc Markup
        doPrefix True _    = neutral
        doPrefix False end =
          ppRawPropertyCount (summaryCompleted summary) <+>
          "/" <+>
          ppRawPropertyCount (summaryTotal summary) <++>
          "complete" <+> end

        addPrefix : Bool -> List (Doc Markup) -> List (Doc Markup)
        addPrefix complete [] = [doPrefix complete neutral]
        addPrefix complete xs = doPrefix complete ": " :: xs

toAnsi : Markup -> AnsiStyle
toAnsi (StyledBorder StyleAnnotation) = []
toAnsi (StyledBorder StyleDefault)    = []
toAnsi (StyledBorder StyleFailure)    = []
toAnsi AnnotationValue                = color Magenta
toAnsi CoverageFill                   = color BrightBlack
toAnsi CoverageIcon                   = color Yellow
toAnsi CoverageText                   = color Yellow
toAnsi DiffAdded                      = color Green
toAnsi DiffInfix                      = []
toAnsi DiffPrefix                     = []
toAnsi DiffRemoved                    = color Red
toAnsi DiffSame                       = []
toAnsi DiffSuffix                     = []
toAnsi FailedIcon                     = color BrightRed
toAnsi FailedText                     = color BrightRed
toAnsi ReproduceGutter                = []
toAnsi ReproduceHeader                = []
toAnsi ReproduceSource                = []
toAnsi RunningHeader                  = []
toAnsi RunningIcon                    = []
toAnsi ShrinkingHeader                = color BrightRed
toAnsi ShrinkingIcon                  = color BrightRed
toAnsi SuccessIcon                    = color Green
toAnsi SuccessText                    = color Green
toAnsi WaitingHeader                  = []
toAnsi WaitingIcon                    = []

export
renderDoc : UseColor -> Doc Markup -> String
renderDoc usecol doc =
  let stream = layoutSmart defaultLayoutOptions
             $ indent 2 doc

   in case usecol of
           DisableColor => Str.renderString stream
           EnableColor  => Term.renderString $ reAnnotateS toAnsi stream

export
renderProgress : UseColor -> Maybe PropertyName -> Report Progress -> String
renderProgress color name = renderDoc color . ppProgress name

export
renderResult : UseColor -> Maybe PropertyName -> Report Result -> String
renderResult color name = renderDoc color . ppResult name

export
renderSummary : UseColor -> Summary -> String
renderSummary color = renderDoc color . ppSummary

--------------------------------------------------------------------------------
--          Test Report
--------------------------------------------------------------------------------

export
report :  (aborted : Bool)
       -> TestCount
       -> Size
       -> Seed
       -> Coverage CoverCount
       -> Maybe Confidence
       -> Report Result
report aborted tests size seed cover conf =
  let failureReport = \msg =>
        MkReport tests cover . Failed $
          mkFailure size seed 0 (Just cover) msg Nothing []

      coverageReached = successVerified tests cover conf

      labelsCovered = coverageSuccess tests cover

      successReport = MkReport tests cover OK

      confidenceReport =
        if coverageReached && labelsCovered
           then successReport
           else failureReport $
                  "Test coverage cannot be reached after " <+>
                  show tests <+>
                  " tests"

  in if aborted then confidenceReport
     else if labelsCovered then successReport
     else failureReport $
          "Labels not sufficently covered after " <+>
          show tests <+>
          " tests"


text:
module Verified.Applicative

import Verified.Functor

%default total

class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
  applicativeMap : (x : f a) -> (g : a -> b) ->
                   map g x = pure g <*> x
  applicativeIdentity : (x : f a) -> pure id <*> x = x
  applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->
                           ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)
  applicativeHomomorphism : (x : a) -> (g : a -> b) ->
                            (<*>) {f} (pure g) (pure x) = pure {f} (g x)
  applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
                           g <*> pure x = pure (\g' : a -> b => g' x) <*> g

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
module FFI.Git

import Data.String
import Data.Promise
import FFI

%default total

git_ffi : (fnName : String) -> String
git_ffi = node_ffi "git"

data GitRef : Type

export
data Git = G (Ptr GitRef)

%foreign git_ffi "git"
prim__git : PrimIO (Ptr GitRef)

export
git : HasIO io => io Git
git = G <$> (primIO $ prim__git)

%foreign git_ffi "current_branch"
prim__currentBranch : Ptr GitRef
                   -> (onSuccess : String -> PrimIO ())
                   -> (onFailure : String -> PrimIO ())
                   -> PrimIO ()

export
currentBranch : Git => Promise String
currentBranch @{(G ptr)} = promiseIO $ prim__currentBranch ptr

%foreign git_ffi "push_new_branch"
prim__pushNewBranch : Ptr GitRef
                   -> (remoteName : String)
                   -> (branch : String)
                   -> (onSuccess : String -> PrimIO ())
                   -> (onFailure : String -> PrimIO ())
                   -> PrimIO ()

export
pushNewBranch : Git => (remoteName : String) -> (branch : String) -> Promise ()
pushNewBranch @{(G ptr)} remoteName branch =
  ignore . promiseIO $ prim__pushNewBranch ptr remoteName branch

%foreign git_ffi "remote_uri"
prim__remoteURI : Ptr GitRef
               -> (remoteName : String)
               -> (onSuccess : String -> PrimIO ())
               -> (onFailure : String -> PrimIO ())
               -> PrimIO ()

||| Get the Git remote URI for the remote with the given name.
||| For example,
|||   "git@github.com:org/reponame.git"
|||   "https://github.com/org/reponame.git"
export
remoteURI : Git => (remoteName : String) -> Promise String
remoteURI @{(G ptr)} remoteName = promiseIO $ prim__remoteURI ptr remoteName

%foreign git_ffi "remote_tracking_branch"
prim__remoteTrackingBranch : Ptr GitRef
                          -> (onSuccess : String -> PrimIO ())
                          -> (onFailure : String -> PrimIO ())
                          -> PrimIO ()

export
remoteTrackingBranch : Git => Promise (Maybe String)
remoteTrackingBranch @{(G ptr)} =
  do str <- promiseIO $ prim__remoteTrackingBranch ptr
     pure $
       case strM str of
            StrNil         => Nothing
            (StrCons x xs) => Just str

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
module Idris2Rust.CompileCfg

import Control.Monad.Maybe
import Control.Monad.Trans
import Control.Monad.Error.Either

import Data.String
import Data.Either
import Data.Maybe
import Data.List

import Libraries.Data.Version
import Libraries.Utils.Path

import System
import System.File

||| Find path to rust compiler
public export
findRust : IO (Maybe String)
findRust = do
  provided <- getEnv "RUSTC"
  finded <- pathLookup ["rustc"]
  pure $ provided <|> finded

-- TODO: Refactor in more beauty way (with monad Transformers AFAIK)
||| Returns the rust compiler version for given executable
public export
rustVersion : IO (Maybe Version)
rustVersion = do
  Just cmd <- findRust
    | Nothing => pure Nothing
  Just process_descriptor <- map getRight $ popen (cmd ++ " --version") Read
    | Nothing => pure Nothing
  Just output <- map getRight $ fGetLine process_descriptor
    | Nothing => pure Nothing
  pure . choiceMap parseVersion $ words output

||| Compilation profile
public export
data Profile = Debug | Release

-- TODO: Add CompileCommand record
export
showCompileCommand : Profile -> (path : String)-> String
showCompileCommand Debug path = ?getCompileCommand_rhs1
showCompileCommand Release path = ?getCompileCommand_rhs2


text:
module Main

main : IO ()
main = putStrLn "Yo, Idris"

max_stars_repo_name: takemyoxygen/playground

max_issues_repo_name: takemyoxygen/playground

max_forks_repo_name: takemyoxygen/playground


text:
module Postgres.Result

import public Data.Vect

import Postgres.Utility
import Postgres.Data.ResultStatus
import Postgres.Data.PostgresType
import Data.Fin

||| Internal phantom type used to mark pointers to the
||| `libpq` struct of the same name.
export
data PGresult : Type

%foreign libpq "PQclear"
prim__dbClearResult : Ptr PGresult -> PrimIO ()

||| The result of executing a command. See `Postgres.Exec`
||| for more.
export
data Result : Type where
  MkResult : Ptr PGresult -> Result

||| All of the various forms of execution supported by libpq
||| provide types that conform to the `ResultProducer` interface.
public export
interface ResultProducer source input where
  exec : source -> input -> IO (Ptr PGresult)

||| Execute the given result producer, do the given thing with the
||| result, and then free the memory used for the result.
export
withResult : ResultProducer source a => source -> a -> (Result -> IO b) -> IO b
withResult src cmd f = do resPtr <- exec src cmd
                          out <- f $ MkResult resPtr
                          primIO $ prim__dbClearResult resPtr
                          pure out

--
-- Result Status
--

resultStatus : Int -> ResultStatus
resultStatus i =
  case i of
       0 => EMPTY_QUERY
       1 => COMMAND_OK
       2 => TUPLES_OK
       3 => COPY_OUT
       4 => COPY_IN
       5 => BAD_RESPONSE
       6 => NONFATAL_ERROR
       7 => FATAL_ERROR
       8 => COPY_BOTH
       9 => SINGLE_TUPLE
       x => OTHER x

%foreign libpq "PQresultStatus"
prim__dbResultStatus : Ptr PGresult -> Int

export
pgResultStatus : Result -> ResultStatus
pgResultStatus (MkResult res) = resultStatus $ prim__dbResultStatus res

export
pgResultSuccess : Result -> Bool
pgResultSuccess res with (pgResultStatus res)
  pgResultSuccess _ | EMPTY_QUERY = True
  pgResultSuccess _ | COMMAND_OK = True
  pgResultSuccess _ | TUPLES_OK = True
  pgResultSuccess _ | COPY_OUT = True
  pgResultSuccess _ | COPY_IN = True
  pgResultSuccess _ | COPY_BOTH = True
  pgResultSuccess _ | SINGLE_TUPLE = True
  pgResultSuccess _ | x = False

%foreign libpq "PQresultErrorMessage"
prim__dbResultErrorMessage : Ptr PGresult -> String

||| Get the Postgres error message for the given result or
||| Nothing if the result was a success.
export
pgResultErrorMessage : Result -> Maybe String
pgResultErrorMessage result@(MkResult res) = case pgResultSuccess result of
                                                  False => Just $ prim__dbResultErrorMessage res
                                                  True  => Nothing

--
-- Tuple Result
--

%foreign libpq "PQntuples"
prim__dbResultRowCount : Ptr PGresult -> Int

%foreign libpq "PQnfields"
prim__dbResultColCount : Ptr PGresult -> Int

||| Assumes the result is of type TUPLES_OK. Used
||| internally to define TupleResult or else it
||| would require TupleResult itself.
resultRowCount : Result -> Nat
resultRowCount (MkResult res) = integerToNat $ cast $ prim__dbResultRowCount res

||| Assumes the result is of type TUPLES_OK. Used
||| internally to define TupleResult or else it
||| would require TupleResult itself.
resultColCount : Result -> Nat
resultColCount (MkResult res) = integerToNat $ cast $ prim__dbResultColCount res

export
data TupleResult : (rows: Nat) -> (cols: Nat) -> Type where
  MkTupleResult : (res : Result) -> TupleResult (resultRowCount res) (resultColCount res)

export
tupleResult : (res: Result) -> Maybe (TupleResult (resultRowCount res) (resultColCount res))
tupleResult res = case (pgResultStatus res) of
                       TUPLES_OK => pure $ MkTupleResult res
                       _ => Nothing

--
-- Result Value
--

%foreign libpq "PQfname"
prim__dbResultColName : Ptr PGresult -> (col : Int) -> String

%foreign libpq "PQgetisnull"
prim__dbResultValueIsNull : Ptr PGresult -> (row : Int) -> (col : Int) -> Int

%foreign libpq "PQfformat"
prim__dbResultColFormatCode : Ptr PGresult -> (col : Int) -> Int

||| Get the type of the column. The resulting Int is a Postgres OID.
||| Built-in data types are defined in the file src/include/catalog/pg_type.h
%foreign libpq "PQftype"
prim__dbResultColType : Ptr PGresult -> (col : Int) -> Int

||| Get the name of the given column for this tuple result.
resultColName : TupleResult r c -> (col : Fin c) -> String
resultColName (MkTupleResult (MkResult res)) col = prim__dbResultColName res (cast $ finToInteger col)

||| Get whether the value at the given row and column is null or not.
resultValueIsNull : TupleResult r c -> (row : Fin r) -> (col : Fin c) -> Bool
resultValueIsNull (MkTupleResult (MkResult res)) row col =
  intToBool $ prim__dbResultValueIsNull res (cast $ finToInteger row) (cast $ finToInteger col)

||| Get the result column type. Note that this is currently limited
||| by the few known types that are looked up and stored in the
||| TypeDictionary.
resultColType : {auto types : TypeDictionary} -> TupleResult r c -> (col : Fin c) -> PType
resultColType (MkTupleResult (MkResult res)) col =
  let oid = prim__dbResultColType res (cast $ finToInteger col) in
      lookup (MkOid oid) types

intToFormatCode : Int -> FormatCode
intToFormatCode 0 = Text
intToFormatCode 1 = Binary
intToFormatCode _ = Text -- technically, other codes are reserved for future definition.

resultColFormatCode : TupleResult r c -> (col : Fin c) -> FormatCode
resultColFormatCode (MkTupleResult (MkResult res)) col =
  intToFormatCode $ prim__dbResultColFormatCode res (cast $ finToInteger col)

||| Get the size of the resultset as (row, col).
export
pgResultSize : {r: Nat} -> {c: Nat} -> TupleResult r c -> (Nat, Nat)
pgResultSize res = (r, c)

%foreign libpq "PQgetvalue"
prim__dbResultValue : Ptr PGresult -> (row: Int) -> (col: Int) -> String

||| Get the result value at the given row and column as a String regardless
||| of what the underlying Postgres type is.
|||
||| Null postgres values are treated as empty strings.
|||
||| Use `pgResultNullableStringValue` to handle nulls as Nothing.
export
pgResultStringValue : (res: TupleResult rows cols) -> (row: Fin rows) -> (col: Fin cols) -> String
pgResultStringValue (MkTupleResult (MkResult res)) row col =
  let r = cast $ the Nat (cast row)
      c = cast $ the Nat (cast col) in
    prim__dbResultValue res r c

||| Get the result value at the given row and column as a (Maybe String) regardless
||| of what the underlying Postgres type is.
|||
||| Null postgres values are Nothing, whereas all other values are String (this does not
||| fail to parse Strings by returning Nothing -- anything non-null is guaranteed to return
||| a `Just` value).
|||
||| Use `pgResultStringValue` to handle nulls as empty Strings.
export
pgResultNullableStringValue : (res: TupleResult rows cols) -> (row: Fin rows) -> (col: Fin cols) -> Maybe String
pgResultNullableStringValue (MkTupleResult (MkResult res)) row col =
  let r = cast $ the Nat (cast row)
      c = cast $ the Nat (cast col) in
    case intToBool $ prim__dbResultValueIsNull res r c of
         True  => Nothing
         False => Just $ prim__dbResultValue res r c

||| The combination of name and type information for a single Postgres result column.
public export
record ColHeader where
  constructor MkHeader
  name : String
  type : PType

export
Show ColHeader where
  show (MkHeader name type) = name ++ " " ++ (show type)

--
-- Resultset
--

resultRow : {cols: Nat} -> (res : TupleResult rows cols) -> (row: Fin rows) -> (Vect cols (Lazy String))
resultRow res row = valueAt <$> (range {len=cols}) where
  valueAt : Fin cols -> Lazy String
  valueAt col = pgResultStringValue res row col

nullableResultRow : {cols: Nat} -> (res : TupleResult rows cols) -> (row: Fin rows) -> (Vect cols (Lazy (Maybe String)))
nullableResultRow res row = valueAt <$> (range {len=cols}) where
  valueAt : Fin cols -> Lazy (Maybe String)
  valueAt col = pgResultNullableStringValue res row col

||| Get the resultset (all rows and columns) with all values as Strings
||| regardless of the underlying Postgres value type.
|||
||| Null is treated as the empty String.
|||
||| To get (Maybe String) where null is Nothing, use `pgNullableStringResultset`
export
pgStringResultset : {rows: Nat}
                 -> {cols: Nat}
                 -> (res : TupleResult rows cols)
                 -> (Vect rows (Vect cols (Lazy String)))
pgStringResultset res = valueAt <$> (range {len=rows}) where
  valueAt : Fin rows -> Vect cols (Lazy String)
  valueAt = resultRow res

public export
StringResultset : (header : Bool) -> Type
StringResultset False = (rows ** cols ** Vect rows (Vect cols (Maybe String)))
StringResultset True = (rows ** cols ** (Vect cols ColHeader, Vect rows (Vect cols (Maybe String))))

||| Get the resultset (all rows and columns) with all values as (Maybe Strings)
||| regardless of the underlying Postgres value type.
|||
||| Null is treated as Nothing -- No matter what type the Postgres column is, a non-null
||| value will be a `Just` value with a String in it; Nothing only means null, not
||| ever that the value failed to parse as a String.
|||
||| To get String where null is the empty String, use `pgStringResultset`
export
pgNullableStringResultset : {rows: Nat}
                         -> {cols: Nat}
                         -> (res : TupleResult rows cols)
                         -> (Vect rows (Vect cols (Lazy (Maybe String))))
pgNullableStringResultset res = valueAt <$> (range {len=rows}) where
  valueAt : Fin rows -> Vect cols (Lazy (Maybe String))
  valueAt = nullableResultRow res

export
pgResultsetColNames : {cols : Nat} -> (res : TupleResult rows cols) -> Vect cols String
pgResultsetColNames res = resultColName res <$> (range {len=cols})

||| Get all the column types for the given result. Note that
||| this is currently limited by the few known types that
||| are looked up and stored in the TypeDictionary.
export
pgResultsetColTypes : {auto types : TypeDictionary} -> {cols : Nat} -> (res : TupleResult rows cols) -> Vect cols PType
pgResultsetColTypes res = resultColType res <$> (range {len=cols})

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
module GameServer.Protocol.State where

data

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Vect
-- File referenced from Chapter4.idr

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

%name Vect xs, ys, zs

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

zip : Vect n a -> Vect n b -> Vect n (a,b)
zip [] [] = []
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys  -- <3<3<3<3 autocompleted

-- Fin n means a number that has an upper bound of n.
-- i.e. proof that the element < n
-- FZ : Fin n, for all n 0 < S n
-- FS (FZ) : proof that 1 < S (S n)
--   therefore FS : Fin n -> Fin (S n)
data Fin : Nat -> Type where
  FZ : Fin (S n)
  FS : Fin n -> Fin (S n)

index : Fin n -> Vect n a -> a
index FZ (x :: xs) = x
index (FS k) (x :: xs) = index k xs

natToFin : Nat -> (n : Nat) ->  Maybe (Fin n)
natToFin k Z = Nothing  -- Nothing is < 0
natToFin Z (S j) = Just FZ  -- Z < S n
natToFin (S k) (S j) = map FS (natToFin k j)  -- Functor example

integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
integerToFin x Z = Nothing
integerToFin x (S k) = if x == 0 then Just FZ
                                 else map FS (integerToFin (x-1) k)  -- <3 Functors
-- Note to self: functor has map function and it's type is (a->b) -> f a -> f b
-- there is bit of missmatch between haskell: in hl map is of type (a->b) -> [a] -> [b]
-- fmap is the more general case.
-- If we look at https://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.Base.html#line-966
-- we see fmap for [] is defined as map (so map is the primitive operation).

-- In the book we now go to TryIndex.idr where we import Data.Vect.
-- Given that we've already implemented integerToFin here, I'll just
-- continue in this file.
tryIndex : Integer -> Vect n a -> Maybe a
-- we want to go from x to Maybe Fin n to Maybe a
tryIndex {n} x xs = (map index (integerToFin x n)) <*> (Just xs)  -- Woot!
-- applicative takes a f (a->b) -> f a -> f b

tryIndex' : Integer -> Vect n a -> Maybe a
tryIndex' {n} x xs = map (flip index xs) (integerToFin x n) -- Woot2!

-- Return to Chapter4.idr

max_stars_repo_name: neduard/type-driven-development

max_issues_repo_name: neduard/type-driven-development

max_forks_repo_name: neduard/type-driven-development


text:
import DataStore

testStore : DataStore (SString .+. SString .+. SInt)
testStore = addToStore ("Mercury", "Mariner 10", 1974) $
            addToStore ("Venus", "Venera", 1961) $
            addToStore ("Uranus", "Voyager 2", 1986) $
            addToStore ("Pluto", "New Horizons", 2015) $
            empty

listItems : DataStore schema -> List (SchemaType schema)
listItems input with (storeView input)
  listItems DataStore.empty | SNil = []
  listItems (addToStore entry store) | (SAdd entry store rec)
         = entry :: listItems store | rec

filterKeys : (test : SchemaType val_schema -> Bool) ->
             DataStore (SString .+. val_schema) -> List String
filterKeys test input with (storeView input)
  filterKeys test DataStore.empty | SNil = []
  filterKeys test (addToStore (key, value) store) | (SAdd (key, value) store rec)
       = if test value
            then key :: filterKeys test store | rec
            else filterKeys test store | rec


text:
module Network.Curl.Prim.Mime

-------------------------------------------------
-- Mime
-------------------------------------------------
-- curl_mime_addpart
-- curl_mime_data
-- curl_mime_data_cb
-- curl_mime_encoder
-- curl_mime_filedata
-- curl_mime_filename
-- curl_mime_free
-- curl_mime_headers
-- curl_mime_init
-- curl_mime_name
-- curl_mime_subparts
-- curl_mime_type
-------------------------------------------------

%foreign "fizz:bop,pop"
fizz : Int -> Int

-- Because multiple flavors of Scheme are supported as Idris backends scheme foreign specifiers can be written to target particular flavors.
-- The following example shows a foreign declaration that allocates memory in a way specific to the choice of backend. There is no general scheme specifier present that matches every flavor, e.g `scheme:foo`, so the example will only match the specific backends listed.
--
-- .. code-block:: idris
--
--     %foreign "scheme,chez:foreign-alloc"
--              "scheme,racket:malloc"
--              "C:malloc,libc"
--     allocMem : (bytes : Int) -> PrimIO AnyPtr
--
-- .. note:: If your backend is not specified here but defines a C FFI it will be able to make use of the `C:malloc,libc` specifier.


text:
module Gen.Errors

import public Control.Catchable
import public Control.Monad.Identity
import public Control.Monad.Trans
import public Control.Monad.Reader
import public Control.Monad.State

CatchType : Type -> (Type -> Type) -> Type -> Type
CatchType t m a = m a -> (t -> m a) -> m a

liftCatchReader : CatchType e m a -> CatchType e (ReaderT r m) a
liftCatchReader f m h = RD $ \r => f (runReaderT m r) (\e => runReaderT (h e) r)

liftCatchState : CatchType e m (a,s) -> CatchType e (StateT s m) a
liftCatchState f m h = ST $ \ s => runStateT m s `f` \ e => runStateT (h e) s

export
(Monad m, Catchable m e) => Catchable (ReaderT r m) e where
	throw = lift . throw
	catch = liftCatchReader catch

export
(Monad m, Catchable m e) => Catchable (StateT s m) e where
	throw = lift . throw
	catch = liftCatchState catch

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
||| An abstract Shape data type (from Listing 10.11).
module Shape

%access  export
-- %default total

||| A shape is a triangle, rectangle or circle.
data Shape = Triangle  Double Double
           | Rectangle Double Double
           | Circle    Double

--------------------------------------------------------------- [ Constructors ]
-- Export functions for building shapes, rather than their constructors.

triangle : (base, height : Double) -> Shape
triangle = Triangle

rectangle : (width, height : Double) -> Shape
rectangle = Rectangle

circle : (radius : Double) -> Shape
circle = Circle

---------------------------------------------------------- [ Exercise 10.3.4.2 ]

public export
data ShapeView  : (shape : Shape) -> Type where
     STriangle  : ShapeView (triangle base height)
     SRectangle : ShapeView (rectangle width height)
     SCircle    : ShapeView (circle radius)

shapeView : (shape : Shape) -> ShapeView shape
shapeView (Triangle  _ _) = STriangle
shapeView (Rectangle _ _) = SRectangle
shapeView (Circle    _)   = SCircle

area : (shape : Shape) -> Double
area shape with (shapeView shape)
  area (triangle  base  height) | STriangle  = 0.5 * base * height
  area (rectangle width height) | SRectangle = width * height
  area (circle    radius)       | SCircle    = pi * pow radius 2

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Test.Main

import Control.ANSI.SGR
import Test.Mini
import Test.Parser
import Test.PP
import System

main : IO ()
main = do
  res <- testAll [ lexTest, parseTest, ppTest ]
  if res
     then putStrLn (foreground Green "\n\nAll tests passed") >>
          exitSuccess

     else putStrLn (foreground Red "\n\nSome tests failed") >>
          exitFailure


text:
module Heap

%default total
%access private

public export
interface Heap (h : Type -> Type) where
  empty : Ord a => h a
  isEmpty : Ord a => h a -> Bool

  insert : Ord a => a -> h a -> h a
  merge : Ord a => h a -> h a -> h a

  findMin : Ord a => h a -> a
  deleteMin : Ord a => h a -> h a


text:
import Data.Vect
import Data.Vect.Views

total
merge_sort : Ord a => Vect n a -> Vect n a
merge_sort xs with (splitRec xs)
  merge_sort [] | SplitRecNil = []
  merge_sort [x] | SplitRecOne = [x]
  merge_sort (lefts ++ rights) | (SplitRecPair lrec rrec)
    = merge (merge_sort lefts | lrec) (merge_sort  rights | rrec)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Calc.Add

%default total

export
add : Int -> Int -> Int
add x y = x + y

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

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

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


text:
module Addition.Absorb

import Data.Vect
import Common.Util
import Common.Interfaces
import Specifications.DiscreteOrderedGroup
import Specifications.OrderedRing
import Proofs.GroupTheory
import Addition.Carry
import Addition.Scaling
import Addition.AbsorptionLemmas
import Addition.Adhoc

%default total
%access export

||| This is a proof friendly semantics function.  Consider a tail
||| recursive variation for run time use.
public export
phi : Ringops s => (radix : s) -> (lsdf : Vect n s) -> (msc : Carry) -> s
phi radix (x :: xs) c = x + radix * phi radix xs c
phi radix [] c = value c

||| The result of absorbing carry digits:
|||
|||           in1    in2    in3
|||           ou1    ou2    pen + unk
|||    msc    abs    abs    unk
|||
||| unk = the least significant carry is still unknown
||| pen = ouput of reduction before absorbing the unknown carry
||| msc = most significant carry
||| abs = carry already absorbed in the corresponding output
data Absorption :
  (k : Nat) ->
  (constraints : s -> Vect k s -> Type) ->
  (semantics : Vect (S k) s -> Carry -> s) ->
  (inputs : Vect (S k) s) -> Type
  where MkAbsorption :
    (msc : Carry) ->
    (pending : s) ->
    (outputs : Vect k s) ->
    (constraints pending outputs) ->
    (semantics inputs O = semantics (pending :: outputs) msc) ->
    Absorption k constraints semantics inputs

outputs : Absorption {s} k _ _ _ -> (Carry, Vect (S k) s)
outputs (MkAbsorption c p o _ _) = (c, reverse (p :: o))

absorptionBase : Ringops s =>
  DiscreteOrderedRingSpec {s} (+) Zero Ng (*) leq One ->
  (radix : s) ->
  (red : Reduction (+) Zero Ng leq One u radix) ->
  Absorption Z (Ranges leq Ng u (u + Ng One)) (phi radix) [input red]
absorptionBase spec radix (MkReduction i c o invariant outRange) =
  MkAbsorption c o [] (MkRanges outRange []) o3
  where
    o1 : o + radix * value c = i
    o1 = rewriteInvariant (unitalRing spec) radix i o c invariant
    o2 : i = i + radix * value O
    o2 = adhocIdentity2 (ring (unitalRing spec)) i radix
    o3 : phi radix [i] O = phi radix [o] c
    o3 = sym (o1 === o2)

arithLemma : Ringops s => UnitalRingSpec {s} (+) Zero Ng (*) One ->
  (msc : Carry) ->
  (pending : s) ->
  (outputs : Vect k s) ->
  (inputs : Vect (S k) s) ->
  (red : Reduction {s} (+) Zero Ng _ One u radix) ->
  (ih : phi radix inputs O = phi radix (pending :: outputs) msc) ->
  phi radix (input red :: inputs) O =
  phi radix (output red :: (value (carry red) + pending) :: outputs) msc
arithLemma {s} {radix} spec msc pending outputs inputs
        (MkReduction i c o invariant _) inductionHypothesis =
  let
    adhoc = adhocIdentity1 (ring spec) pending o radix (value c) o2
    shift = radix * phi radix inputs O
    shifted = cong {f = (+ shift)} o1
  in shifted @== adhoc
  where
    o1 : o + radix * value c = i
    o1 = rewriteInvariant spec radix i o c invariant
    o2 : phi radix inputs O = pending + radix * phi radix outputs msc
    o2 = inductionHypothesis

absorptionStep : Ringops s =>
  DiscreteOrderedRingSpec {s} (+) Zero Ng (*) leq One ->
  (radix : s) ->
  (red : Reduction (+) Zero Ng leq One u radix) ->
  Absorption k (Ranges leq Ng u (u + Ng One)) (phi radix) inputs ->
  Absorption (S k) (Ranges leq Ng u (u + Ng One))
    (phi radix) (input red :: inputs)
absorptionStep spec radix red@(MkReduction _ _ _ _ reducedRange)
       (MkAbsorption {inputs} msc pending outputs ranges invariant) =
  let absorb = value (carry red) + pending
  in MkAbsorption msc (output red) (absorb :: outputs)
      (rangeLemma (discreteOrderedGroup spec) ranges reducedRange (carry red))
      (arithLemma (unitalRing spec) msc pending outputs inputs red invariant)


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

import Decidable.Equality

import Toolkit.Decidable.Informative

%default total

||| An item in our context, paramterised by the type collected.
|||
||| @kind the type of the datatype describing types
||| @type the instance of the type being recorded.
public export
data Item : (type : kind)
                 -> Type
  where
    I : (name : String)
     -> (type : kind)
             -> Item type

||| A generic container to capture properties over items in the
||| context.
public export
data Holds : (kind : Type)
          -> (pred : (type : kind) -> Type)
          -> (key  : String)
          -> {type : kind}
          -> (item : Item type)
                  -> Type
  where
    H : {pred : (type : kind) -> Type}
     -> {i    : kind}
     -> (prfK : key = str)
     -> (prf  : pred i)
             -> Holds kind pred key (I str i)

namespace Holds
  public export
  data Error type = NotSatisfied type
                  | WrongName String String
export
holds : {pred : (type : kind) -> Type}
     -> (func : (type : kind) -> DecInfo err (pred type))
     -> (key  : String)
     -> {type : kind}
     -> (item : Item type)
             -> DecInfo (Holds.Error err)
                        (Holds kind pred key item)
holds func key (I name type) with (decEq key name)
  holds func key (I key type) | (Yes Refl) with (func type)
    holds func key (I key type) | (Yes Refl) | (Yes prfWhy)
      = Yes (H Refl prfWhy)

    holds func key (I key type) | (Yes Refl) | (No msg contra)
      = No (NotSatisfied msg)
           (\(H Refl prf) => contra prf)

  holds func key (I name type) | (No contra)
    = No (WrongName key name)
         (\(H Refl prf) => contra Refl)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits