text:
module Idris.Driver

import Compiler.Common

import Core.Context.Log
import Core.Core
import Core.Directory
import Core.InitPrimitives
import Core.Metadata
import Core.Unify

import Idris.CommandLine
import Idris.Env
import Idris.IDEMode.REPL
import Idris.ModTree
import Idris.Package
import Idris.ProcessIdr
import Idris.REPL
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import Idris.Pretty
import Idris.Error

import IdrisPaths

import Data.List
import Data.List1
import Data.So
import Data.String
import System
import System.Directory
import System.File
import Libraries.Utils.Path
import Libraries.Utils.Term

import Yaffle.Main

%default covering

findInput : List CLOpt -> Maybe String
findInput [] = Nothing
findInput (InputFile f :: fs) = Just f
findInput (_ :: fs) = findInput fs

-- Add extra data from the "IDRIS2_x" environment variables
updateEnv : {auto c : Ref Ctxt Defs} ->
            {auto o : Ref ROpts REPLOpts} ->
            Core ()
updateEnv
    = do defs <- get Ctxt
         bprefix <- coreLift $ idrisGetEnv "IDRIS2_PREFIX"
         case bprefix of
              Just p => setPrefix p
              Nothing => setPrefix yprefix
         bpath <- coreLift $ idrisGetEnv "IDRIS2_PATH"
         case bpath of
              Just path => do traverseList1_ addExtraDir (map trim (split (==pathSeparator) path))
              Nothing => pure ()
         bdata <- coreLift $ idrisGetEnv "IDRIS2_DATA"
         case bdata of
              Just path => do traverseList1_ addDataDir (map trim (split (==pathSeparator) path))
              Nothing => pure ()
         blibs <- coreLift $ idrisGetEnv "IDRIS2_LIBS"
         case blibs of
              Just path => do traverseList1_ addLibDir (map trim (split (==pathSeparator) path))
              Nothing => pure ()
         pdirs <- coreLift $ idrisGetEnv "IDRIS2_PACKAGE_PATH"
         case pdirs of
              Just path => do traverseList1_ addPackageDir (map trim (split (==pathSeparator) path))
              Nothing => pure ()
         cg <- coreLift $ idrisGetEnv "IDRIS2_CG"
         case cg of
              Just e => case getCG (options defs) e of
                             Just cg => setCG cg
                             Nothing => throw (InternalError ("Unknown code generator " ++ show e))
              Nothing => pure ()
         inccgs <- coreLift $ idrisGetEnv "IDRIS2_INC_CGS"
         case inccgs of
              Just cgs =>
                   traverse_ (setIncrementalCG False) $
                       map trim (toList (split (==',') cgs))
              Nothing => pure ()
         -- IDRIS2_PATH goes first so that it overrides this if there's
         -- any conflicts. In particular, that means that setting IDRIS2_PATH
         -- for the tests means they test the local version not the installed
         -- version
         defs <- get Ctxt
         -- These might fail while bootstrapping
         catch (addPkgDir "prelude" anyBounds) (const (pure ()))
         catch (addPkgDir "base" anyBounds) (const (pure ()))
         addDataDir (prefix_dir (dirs (options defs)) </>
                        ("idris2-" ++ showVersion False version) </> "support")
         addLibDir (prefix_dir (dirs (options defs)) </>
                        ("idris2-" ++ showVersion False version) </> "lib")
         Just cwd <- coreLift $ currentDir
              | Nothing => throw (InternalError "Can't get current directory")
         addLibDir cwd

updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
                 Core ()
updateREPLOpts
    = do opts <- get ROpts
         ed <- coreLift $ idrisGetEnv "EDITOR"
         case ed of
              Just e => put ROpts (record { editor = e } opts)
              Nothing => pure ()

showInfo : {auto c : Ref Ctxt Defs}
        -> {auto o : Ref ROpts REPLOpts}
        -> List CLOpt
        -> Core Bool
showInfo Nil = pure False
showInfo (_::rest) = showInfo rest

tryYaffle : List CLOpt -> Core Bool
tryYaffle [] = pure False
tryYaffle (Yaffle f :: _) = do yaffleMain f []
                               pure True
tryYaffle (c :: cs) = tryYaffle cs

ignoreMissingIpkg : List CLOpt -> Bool
ignoreMissingIpkg [] = False
ignoreMissingIpkg (IgnoreMissingIPKG :: _) = True
ignoreMissingIpkg (c :: cs) = ignoreMissingIpkg cs

tryTTM : List CLOpt -> Core Bool
tryTTM [] = pure False
tryTTM (Metadata f :: _) = do dumpTTM f
                              pure True
tryTTM (c :: cs) = tryTTM cs

banner : String
banner = "     ____    __     _         ___                                           \n" ++
         "    /  _/___/ /____(_)____   |__ \\                                          \n" ++
         "    / // __  / ___/ / ___/   __/ /     Version " ++ showVersion True version ++ "\n" ++
         "  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           \n" ++
         " /___/\\__,_/_/  /_/____/   /____/      Type :? for help                     \n" ++
         "\n" ++
         "Welcome to Idris 2.  Enjoy yourself!"

checkVerbose : List CLOpt -> Bool
checkVerbose [] = False
checkVerbose (Verbose :: _) = True
checkVerbose (_ :: xs) = checkVerbose xs

stMain : List (String, Codegen) -> List CLOpt -> Core ()
stMain cgs opts
    = do False <- tryYaffle opts
            | True => pure ()
         False <- tryTTM opts
            | True => pure ()
         defs <- initDefs
         let updated = foldl (\o, (s, _) => addCG (s, Other s) o) (options defs) cgs
         c <- newRef Ctxt (record { options = updated } defs)
         s <- newRef Syn initSyntax
         setCG {c} $ maybe Jvm (Other . fst) (head' cgs)
         addPrimitives

         setWorkingDir "."
         when (ignoreMissingIpkg opts) $
            setSession (record { ignoreMissingPkg = True } !getSession)

         let ide = ideMode opts
         let ideSocket = ideModeSocket opts
         let outmode = if ide then IDEMode 0 stdin stdout else REPL InfoLvl
         let fname = findInput opts
         o <- newRef ROpts (REPL.Opts.defaultOpts fname outmode cgs)
         updateEnv

         finish <- showInfo opts
         when (not finish) $ do
           -- If there's a --build or --install, just do that then quit
           done <- processPackageOpts opts

           when (not done) $ flip catch renderError $
              do True <- preOptions opts
                     | False => pure ()

                 when (checkVerbose opts) $ -- override Quiet if implicitly set
                     setOutput (REPL InfoLvl)
                 u <- newRef UST initUState
                 origin <- maybe
                   (pure $ Virtual Interactive) (\fname => do
                     modIdent <- ctxtPathToNS fname
                     pure (PhysicalIdrSrc modIdent)
                     ) fname
                 m <- newRef MD (initMetadata origin)
                 updateREPLOpts
                 session <- getSession
                 when (not $ nobanner session) $ do
                   iputStrLn $ pretty banner
                   when (isCons cgs) $ iputStrLn (reflow "With codegen for:" <++> hsep (pretty . fst <$> cgs))
                 fname <- if findipkg session
                             then findIpkg fname
                             else pure fname
                 setMainFile fname
                 result <- case fname of
                      Nothing => logTime "+ Loading prelude" $ do
                                   when (not $ noprelude session) $
                                     readPrelude True
                                   pure Done
                      Just f => logTime "+ Loading main file" $ do
                                  res <- loadMainFile f
                                  displayErrors res
                                  pure res

                 doRepl <- catch (postOptions result opts)
                                 (\err => emitError err *> pure False)
                 if doRepl then
                   if ide || ideSocket then
                     if not ideSocket
                      then do
                       setOutput (IDEMode 0 stdin stdout)
                       replIDE {c} {u} {m}
                     else do
                       let (host, port) = ideSocketModeAddress opts
                       f <- coreLift $ initIDESocketFile host port
                       case f of
                         Left err => do
                           coreLift $ putStrLn err
                           coreLift $ exitWith (ExitFailure 1)
                         Right file => do
                           setOutput (IDEMode 0 file file)
                           replIDE {c} {u} {m}
                   else do
                       repl {c} {u} {m}
                       showTimeRecord
                  else
                      -- exit with an error code if there was an error, otherwise
                      -- just exit
                    do ropts <- get ROpts
                       showTimeRecord
                       case errorLine ropts of
                         Nothing => pure ()
                         Just _ => coreLift $ exitWith (ExitFailure 1)

  where

  renderError : {auto c : Ref Ctxt Defs} ->
                {auto s : Ref Syn SyntaxInfo} ->
                {auto o : Ref ROpts REPLOpts} ->
                Error -> Core ()
  renderError err = do
    doc <- perror err
    msg <- render doc
    throw (UserError msg)

-- Run any options (such as --version or --help) which imply printing a
-- message then exiting. Returns wheter the program should continue

quitOpts : List CLOpt -> IO Bool
quitOpts [] = pure True
quitOpts (Version :: _)
    = do putStrLn versionMsg
         pure False
quitOpts (Help Nothing :: _)
    = do putStrLn usage
         pure False
quitOpts (Help (Just HelpLogging) :: _)
    = do putStrLn helpTopics
         pure False
quitOpts (Help (Just HelpPragma) :: _)
    = do putStrLn pragmaTopics
         pure False
quitOpts (_ :: opts) = quitOpts opts

export
mainWithCodegens : List (String, Codegen) -> IO ()
mainWithCodegens cgs = do
  Right opts <- getCmdOpts
    | Left err => do putStrLn err
                     putStrLn usage
  continue <- quitOpts opts
  when continue $ do
    setupTerm
    coreRun (stMain cgs opts)
      (\err : Error => do putStrLn ("Uncaught error: " ++ show err)
                          exitWith (ExitFailure 1))
      (\res => pure ())


text:
module Control.Monad.Reader

import Control.Monad.Identity
import Control.Monad.Trans

||| A computation which runs in a static context and produces an output
public export
interface Monad m => MonadReader stateType (m : Type -> Type) | m where
  ||| Get the context
  ask : m stateType

  ||| `local f c` runs the computation `c` in an environment modified by `f`.
  local : MonadReader stateType m => (stateType -> stateType) -> m a -> m a

||| The transformer on which the Reader monad is based
public export
record ReaderT (stateType : Type) (m : Type -> Type) (a : Type) where
  constructor MkReaderT
  runReaderT' : stateType -> m a

public export
implementation Functor f => Functor (ReaderT stateType f) where
  map f (MkReaderT g) = MkReaderT (\st => map f (g st))

public export
implementation Applicative f => Applicative (ReaderT stateType f) where
  pure x = MkReaderT (\st => pure x)

  (MkReaderT f) <*> (MkReaderT a) =
    MkReaderT (\st =>
      let f' = f st in
      let a' = a st in
      f' <*> a')

public export
implementation Monad m => Monad (ReaderT stateType m) where
  (MkReaderT f) >>= k =
    MkReaderT (\st => do v <- f st
                         let MkReaderT kv = k v
                         kv st)

public export
implementation MonadTrans (ReaderT stateType) where
  lift x = MkReaderT (\_ => x)

public export
implementation Monad m => MonadReader stateType (ReaderT stateType m) where
  ask = MkReaderT (\st => pure st)

  local f (MkReaderT action) = MkReaderT (action . f)

public export
implementation HasIO m => HasIO (ReaderT stateType m) where
  liftIO f = MkReaderT (\_ => liftIO f)

public export
implementation (Monad f, Alternative f) => Alternative (ReaderT stateType f) where
  empty = lift empty

  (MkReaderT f) <|> (MkReaderT g) = MkReaderT (\st => f st <|> g st)

||| Evaluate a function in the context held by this computation
public export
asks : MonadReader stateType m => (stateType -> a) -> m a
asks f = ask >>= pure . f

||| Unwrap and apply a ReaderT monad computation
public export
%inline
runReaderT : stateType -> ReaderT stateType m a -> m a
runReaderT s action = runReaderT' action s

||| The Reader monad. The ReaderT transformer applied to the Identity monad.
public export
Reader : (stateType : Type) -> (a : Type) -> Type
Reader s a = ReaderT s Identity a

||| Unwrap and apply a Reader monad computation
public export
runReader : stateType -> Reader stateType a -> a
runReader s = runIdentity . runReaderT s

ext: idr


text:
-- ------------------------------------------------------------ [ Strategy.idr ]
-- Module    : Strategy.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| Evaluation Strategies
module GRL.Eval.Strategy

import GRL.Common
import GRL.IR
import GRL.Builder
import GRL.Model

||| Strategies are just list of node evaluation pairings.
public export
Strategy : Type
Strategy = List (GoalNode, SValue)

export
buildStrategy : GRL expr => List (expr ELEM, SValue) -> Strategy
buildStrategy es = map (\(e,v) => ((convExpr . mkElem) e, v)) es

||| Deploy Strategy being careful not to override default values, returning a pairing of the modified model, and original.
export
deployStrategy : GModel -> Strategy -> (GModel, GModel)
deployStrategy oldG ss = (newG, oldG)
  where
    canUp : SValue -> GoalNode -> GoalNode
    canUp s n = record {getSValue = Just s} n

    doUp : (GoalNode, SValue) -> GModel -> GModel
    doUp (n,s) m = updateGoalNode (\x => getNodeTitle n == getNodeTitle x )
                                  (canUp s)
                                  m

    newG : GModel
    newG = foldr (doUp) oldG ss

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Data.Functor.Compose

public export
data Compose : (f : Type -> Type) -> (g : Type -> Type) -> Type -> Type where
  MkCompose : f (g x) -> Compose f g x

public export
getCompose : Compose f g a -> f (g a)
getCompose (MkCompose x) = x

public export
implementation (Functor f, Functor g) => Functor (Compose f g) where
  map f (MkCompose x) = MkCompose $ map (map f) x


text:
|||
|||
||| foldr is the unique solution to the equation:
|||
|||   h f e [] = e
|||   h f e (x :: xs) = x `h` (foldr f e xs)
|||
||| (This fact is called 'the universal property of foldr'.)
|||
||| Since the prelude defines foldr tail-recursively, this fact isn't immediate
||| and we need some lemmata to prove it.
module Data.Vect.Properties.Foldr

import Data.Vect
import Data.Vect.Elem
import Data.Fin
import Data.Nat
import Data.Nat.Order

import Syntax.PreorderReasoning
import Syntax.PreorderReasoning.Generic

import Control.Order

||| Sum implemented with foldr
public export
sumR : (Foldable f, Num a) => f a -> a
sumR = foldr (+) 0

%transform "sumR/sum" sumR = sum

||| A function H : forall n. Vect n A -> B preserving the structure of vectors over A
public export
record VectHomomorphismProperty {0 A, B : Type} (F : A -> B -> B) (E : B) (H : forall n . Vect n A -> B) where
  constructor ShowVectHomomorphismProperty
  nil  : H [] = E
  cons : {0 n : Nat} -> (x : A) -> (xs : Vect n A) -> H (x :: xs) = x `F` (H xs)

||| There is an extensionally unique function preserving the vector structure
export
nilConsInitiality :
     (f : a -> b -> b) -> (e : b)
  -> (h1, h2 : forall n . Vect n a -> b)
  -> (prf1 : VectHomomorphismProperty f e h1)
  -> (prf2 : VectHomomorphismProperty f e h2)
  -> (xs : Vect n a) -> h1 xs = h2 xs
nilConsInitiality f e h1 h2 prf1 prf2 [] = Calc $
  |~ h1 []
  ~~ e     ...(prf1.nil)
  ~~ h2 [] ...(sym prf2.nil)

nilConsInitiality f e h1 h2 prf1 prf2 (x :: xs) = Calc $
  |~ h1 (x :: xs)
  ~~ (x `f` (h1 xs)) ...(prf1.cons _ _)
  ~~ (x `f` (h2 xs)) ...(cong (x `f`) $ nilConsInitiality f e h1 h2 prf1 prf2 xs)
  ~~ h2 (x :: xs) ...(sym $ prf2.cons _ _)

||| extensionality is a congruence with respect to Data.Vect.foldrImpl
foldrImplExtensional :
  (f : a -> b -> b) -> (e : b)
  -> (go1, go2 : b -> b)
  -> ((y : b) -> go1 y = go2 y)
  -> (xs : Vect n a)
  -> foldrImpl f e go1 xs = foldrImpl f e go2 xs
foldrImplExtensional f e go1 go2 ext [] = ext e
foldrImplExtensional f e go1 go2 ext (x :: xs) =
  foldrImplExtensional f e _ _
  (\y => ext (f x y))
  xs

||| foldrImpl f e x : (b -> -) -> - is natural
foldrImplNaturality : (f : a -> b -> b) -> (e : b) -> (xs : Vect n a) -> (go1, go2 : b -> b)
  -> foldrImpl f e (go1 . go2) xs = go1 (foldrImpl f e go2 xs)
foldrImplNaturality f e    []     go1 go2 = Refl
foldrImplNaturality f e (x :: xs) go1 go2 = foldrImplNaturality f e xs go1 (go2 . (f x))

||| Our tail-recursive foldr preserves the vector structure
export
foldrVectHomomorphism : VectHomomorphismProperty f e (foldr f e)
foldrVectHomomorphism = ShowVectHomomorphismProperty
  { nil  = Refl
  , cons = \x, xs => Calc $
    |~ foldr f e (x :: xs)
    ~~ foldrImpl f e (id . (f x)) xs ...(Refl)
    ~~ foldrImpl f e ((f x) . id) xs ...(foldrImplExtensional f e _ _ (\y => Refl) xs)
    ~~ f x (foldrImpl f e id xs)     ...(foldrImplNaturality f e xs (f x) _)
    ~~ f x (foldr f e xs)            ...(Refl)
  }

||| foldr is the unique function preserving the vector structure
export
foldrUniqueness : (h : forall n . Vect n a -> b) -> VectHomomorphismProperty f e h -> (xs : Vect n a) -> h xs = foldr f e xs
foldrUniqueness {f} h prf xs = irrelevantEq $
  nilConsInitiality f e h (foldr f e) prf foldrVectHomomorphism xs

||| Each summand is `LTE` the sum
export
sumIsGTEtoParts : {x : Nat} -> (xs : Vect n Nat) -> (x `Elem` xs) -> sumR xs `GTE` x
sumIsGTEtoParts (x :: xs) Here
  = CalcWith $
  |~ x
  ~~ x + 0 ...(sym $ plusZeroRightNeutral _)
  <~ x + (sumR xs)   ...(plusLteMonotoneLeft x 0 _ LTEZero)
  ~~ sumR (x :: xs)  ...(sym $ (foldrVectHomomorphism {f = plus} {e = 0}).cons _ _)

sumIsGTEtoParts {x} (y :: xs) (There later)
  = CalcWith $
    |~ x
    <~ sumR xs       ...(sumIsGTEtoParts {x} xs later)
    ~~ 0 + sumR xs   ...(Refl)
    <~ y + (sumR xs) ...(plusLteMonotoneRight (sumR xs) 0 y LTEZero)
    ~~ sumR (y :: xs) ...(sym $ (foldrVectHomomorphism {f = plus} {e = 0}).cons _ _)

||| `sumR : Vect n Nat -> Nat` is monotone
export
sumMonotone : {n : Nat} -> (xs, ys : Vect n Nat)
  -> (prf : (i : Fin n) -> index i xs `LTE` index i ys)
  -> (sumR xs `LTE` sumR ys)
sumMonotone [] [] prf = LTEZero
sumMonotone (x :: xs) (y :: ys) prf =
  let prf' = sumMonotone xs ys (\i => prf (FS i))
  in CalcWith $
  |~ sumR (x :: xs)
  ~~ x + sumR xs    ...((foldrVectHomomorphism {f = plus} {e = 0}).cons x xs)
  <~ y + sumR ys    ...(plusLteMonotone  (prf 0) prf')
  ~~ sumR (y :: ys) ...(sym $ (foldrVectHomomorphism {f = plus} {e = 0}).cons y ys)


text:
import Door
import Stack
import StackIO
import Vending


text:
module Main

caseB8 : Bits8 -> String
caseB8 0 = "B8 - zero"
caseB8 42 = "B8 - answer"
caseB8 _ = "B8 - nonzero"

caseB16 : Bits16 -> String
caseB16 0 = "B16 - zero"
caseB16 42 = "B16 - answer"
caseB16 _ = "B16 - nonzero"

caseB32 : Bits32 -> String
caseB32 0 = "B32 - zero"
caseB32 42 = "B32 - answer"
caseB32 _ = "B32 - nonzero"

caseB64 : Bits64 -> String
caseB64 0 = "B64 - zero"
caseB64 42 = "B64 - answer"
caseB64 _ = "B64 - nonzero"

caseI8 : Bits8 -> String
caseI8 0 = "I8 - zero"
caseI8 42 = "I8 - answer"
caseI8 _ = "I8 - nonzero"

caseI16 : Bits16 -> String
caseI16 0 = "I16 - zero"
caseI16 42 = "I16 - answer"
caseI16 _ = "I16 - nonzero"

caseI32 : Bits32 -> String
caseI32 0 = "I32 - zero"
caseI32 42 = "I32 - answer"
caseI32 _ = "I32 - nonzero"

caseI64 : Bits64 -> String
caseI64 0 = "I64 - zero"
caseI64 42 = "I64 - answer"
caseI64 _ = "I64 - nonzero"

main : IO ()
main = do
  putStrLn $ caseB8 0
  putStrLn $ caseB8 (cast (the Bits64 0x1000002a))
  putStrLn $ caseB8 255

  putStrLn $ caseB16 0
  putStrLn $ caseB16 42
  putStrLn $ caseB16 255

  putStrLn $ caseB32 0
  putStrLn $ caseB32 42
  putStrLn $ caseB32 255

  putStrLn $ caseB64 0
  putStrLn $ caseB64 42
  putStrLn $ caseB64 255

  putStrLn $ caseI8 0
  putStrLn $ caseI8 (cast (the Bits64 0x1000002a))
  putStrLn $ caseI8 255

  putStrLn $ caseI16 0
  putStrLn $ caseI16 42
  putStrLn $ caseI16 255

  putStrLn $ caseI32 0
  putStrLn $ caseI32 42
  putStrLn $ caseI32 255

  putStrLn $ caseI64 0
  putStrLn $ caseI64 42
  putStrLn $ caseI64 255


text:
module Normalization

import MSubst
import PnP
import R
import Step
import Subst
import Term
import Typing

%default total

----------------------------------------------------------------
-- Begin: PREDICATE 'Halts' IS PRESERVED UNDER TERM CONSTRUCTION

mSubstHalts_Abs : (e : Term) -> (venv : VEnv ctx) ->
                  Halts (msubst (TAbs e) Z venv)
mSubstHalts_Abs e VNil = H (TAbs e) (TAbs e ** (VAbs, TStRefl _))
mSubstHalts_Abs e (VCons x _ _ venv) = mSubstHalts_Abs (subst x (S Z) e) venv

mSubstHalts_Zero : (venv : VEnv ctx) -> Halts (msubst TZero Z venv)
mSubstHalts_Zero VNil = haltsZero
mSubstHalts_Zero (VCons _ _ _ venv) = mSubstHalts_Zero venv

mSubstHalts_Succ : (e : Term) -> (venv : VEnv ctx) ->
                   Halts (msubst e Z venv) ->
                   Halts (msubst (TSucc e) Z venv)
mSubstHalts_Succ e venv (H _ (e1 ** (v1, tst))) =
  let tst'  = congSucc tst
      eq    = mSubstSuccComm e Z venv
      tst'' = replace {P = \q => TransStep q (TSucc e1)} eq tst'
  in H _ (TSucc e1 ** (VSucc v1, tst''))

mSubstHalts_Pred : (e : Term) -> Typing ctx e TyNat ->
                   (venv : VEnv ctx) ->
                   Halts (msubst e Z venv) ->
                   Halts (msubst (TPred e) Z venv)
mSubstHalts_Pred e ty venv (H _ (e1 ** (v1, tst))) =
  let ty'  = mSubstPreservesTy e {ctx1=[]} ty venv
      ty'' = transPreservation _ ty' tst
  in case canonicalNat e1 ty'' v1 of
          (Left Refl) => let tst' = congPred tst .+. StPredZero
                             eq   = mSubstPredComm e Z venv
                         in rewrite (sym eq) in H _ (TZero ** (VZero, tst'))
          (Right (_ ** (v1', Refl))) => let st   = StPredSucc v1'
                                            tst' = congPred tst .+. st
                                            eq   = mSubstPredComm e Z venv
                                        in rewrite (sym eq) in H _ (_ ** (v1', tst'))

-- End: PREDICATE 'Halts' IS PRESERVED UNDER TERM CONSTRUCTION
--------------------------------------------------------------

--------------------------------------------------------------------
-- Begin: LOGICAL PREDICATE 'R' IS PRESERVED UNDER TERM CONSTRUCTION

mSubstR_Var : (i : Nat) ->
              (ctx : Context) ->
              index' i ctx = Just t ->
              (venv : VEnv ctx) ->
              r t (msubst (TVar i) Z venv)
mSubstR_Var Z     []       Refl VNil impossible
mSubstR_Var (S _) []       Refl VNil impossible
mSubstR_Var Z     (s::ctx) Refl (VCons x _ rx venv) =
  let tyx = rTyping x rx
      eq  = mSubstPastCtx x [] tyx venv
  in rewrite eq in rx
mSubstR_Var (S i) (s::ctx) prf  (VCons x _ rx venv) =
  mSubstR_Var i ctx prf venv

mSubstR_App : (e1 : Term) -> (e2 : Term) ->
              (venv : VEnv ctx) ->
              r (s :->: t) (msubst e1 Z venv) ->
              r s (msubst e2 Z venv) ->
              r t (msubst (TApp e1 e2) Z venv)
mSubstR_App e1 e2 venv r1 r2 =
  let imp = rImplication r1
      r'  = imp (msubst e2 Z venv) r2
  in rewrite (sym $ mSubstAppComm e1 e2 Z venv) in r'

mSubstR_Ifz : (e1 : Term) -> Typing ctx e1 TyNat ->
              (e2 : Term) -> (e3 : Term) ->
              (venv : VEnv ctx) ->
              r TyNat (msubst e1 Z venv) ->
              r t (msubst e2 Z venv) ->
              r t (msubst e3 Z venv) ->
              r t (msubst (TIfz e1 e2 e3) Z venv)
mSubstR_Ifz e1 ty1 e2 e3 venv r1 r2 r3 =
  let (H _ (e11 ** (v11, tst))) = rHalts r1
      ty11 = mSubstPreservesTy e1 ty1 {ctx1=[]} venv
      ty12 = transPreservation _ ty11 tst
  in case canonicalNat e11 ty12 v11 of
     (Left Refl) => let tst' = congIfz tst
                                       {ez=(msubst e2 Z venv)}
                                       {es=(msubst e3 Z venv)}
                               .+. StIfzZero
                        ty = TyIfz ty11 (rTyping _ r2) (rTyping _ r3)
                        r' = transStepPreservesR_2 _ _ ty _ tst' r2
                    in rewrite (sym $ mSubstIfzComm e1 e2 e3 Z venv) in r'
     (Right (_ ** (v11', Refl))) => let tst' = congIfz tst
                                                       {ez=(msubst e2 Z venv)}
                                                       {es=(msubst e3 Z venv)}
                                               .+. StIfzSucc v11'
                                        ty = TyIfz ty11 (rTyping _ r2) (rTyping _ r3)
                                        r' = transStepPreservesR_2 _ _ ty _ tst' r3
                                    in rewrite (sym $ mSubstIfzComm e1 e2 e3 Z venv) in r'

mSubstR_Rec' : (e1 : Term) -> Value e1 -> Typing [] e1 TyNat -> r TyNat e1 ->
               (e2 : Term) -> (e3 : Term) ->
               (venv : VEnv ctx) ->
               r t (msubst e2 Z venv) ->
               r (TyNat:->:t:->:t) (msubst e3 Z venv) ->
               r t (TRec e1 (msubst e2 Z venv) (msubst e3 Z venv))
--
mSubstR_Rec' TZero VZero TyZero r1 e2 e3 venv r2 r3 =
 let st  = StRecZero {t0=(msubst e2 Z venv)} {t1=(msubst e3 Z venv)}
     ty  = TyRec TyZero (rTyping _ r2) (rTyping _ r3)
 in stepPreservesR_2 _ _ ty _ st r2
--
mSubstR_Rec' (TSucc e1) (VSucc v1) (TySucc ty1) r1 e2 e3 venv r2 r3 =
  let r1' = succRR r1
      ih  = mSubstR_Rec' e1 v1 ty1 r1' e2 e3 venv r2 r3
      rf  = rImplication $ (rImplication r3) _ r1'
      r'  = rf _ ih
      --
      st   = StRecSucc (VSucc v1) {t0=(msubst e2 Z venv)} {t1=(msubst e3 Z venv)}
      ty   = TyRec (TySucc ty1) (rTyping _ r2) (rTyping _ r3)
  in stepPreservesR_2 _ _ ty _ st r'
--
mSubstR_Rec' (TAbs e1)  VAbs _ r1 e2 e3 venv r2 r3 impossible

mSubstR_Rec : (e1 : Term) -> Typing ctx e1 TyNat ->
              (e2 : Term) -> (e3 : Term) ->
              (venv : VEnv ctx) ->
              r TyNat (msubst e1 Z venv)  ->
              r t (msubst e2 Z venv) ->
              r (TyNat:->:t:->:t) (msubst e3 Z venv) ->
              r t (msubst (TRec e1 e2 e3) Z venv)
mSubstR_Rec e1 ty1 e2 e3 venv r1 r2 r3 =
  let (H _ (e11 ** (v11, tst))) = rHalts r1
      tst' = congRec tst {e0=(msubst e2 Z venv)} {e1=(msubst e3 Z venv)}
      ty11 = mSubstPreservesTy e1 ty1 {ctx1=[]} venv
      ty   = TyRec ty11 (rTyping _ r2) (rTyping _ r3)
      ty12 = transPreservation _ ty11 tst
  in case canonicalNat e11 ty12 v11 of
     (Left Refl) => let r'   = mSubstR_Rec' TZero VZero ty12 rZero e2 e3 venv r2 r3
                        r''  = transStepPreservesR_2 _ _ ty _ tst' r'
                    in rewrite (sym $  mSubstRecComm e1 e2 e3 Z venv) in r''
     (Right (_ ** (_, Refl))) => let r1' = transStepPreservesR_1 _ _ _ tst r1
                                     r'  = mSubstR_Rec' _ v11 ty12 r1' e2 e3 venv r2 r3
                                     r'' = transStepPreservesR_2 _ _ ty _ tst' r'
                                 in rewrite (sym $  mSubstRecComm e1 e2 e3 Z venv) in r''

-- End: LOGICAL PREDICATE 'R' IS PRESERVED UNDER TERM CONSTRUCTION
------------------------------------------------------------------

--------------------------------------------------
-- Begin: PREDICATE 'R' HOLDS FOR ALL CLOSED TERMS

mutual
  mSubstR : (e : Term) -> (t : Ty) ->
            Typing ctx e t -> (venv : VEnv ctx) ->
            r t (msubst e Z venv)
  mSubstR e t ty venv =
    let h   = mSubstHalts e t ty venv
        ty' = mSubstPreservesTy e {ctx1=[]} ty venv
    in case t of
            TyNat => (ty', h)
            (TyFun t1 t2) => let rf = mSubstR_Fun e t1 t2 ty venv
                             in (ty', h, rf)

  mSubstHalts : (e : Term) -> (t : Ty) ->
                Typing ctx e t -> (venv : VEnv ctx) ->
                Halts (msubst e Z venv)
  --
  mSubstHalts (TVar i) t (TyVar prf) venv = rHalts $ mSubstR_Var _ _ prf venv
  --
  mSubstHalts (TAbs e) (s :->: y) (TyAbs s ty) venv = mSubstHalts_Abs e venv
  --
  mSubstHalts (TApp e1 e2) t (TyApp ty1 ty2) venv =
    let r1  = mSubstR e1 _ ty1 venv
        r2  = mSubstR e2 _ ty2 venv
    in rHalts $ mSubstR_App e1 e2 venv r1 r2
  --
  mSubstHalts (TRec e1 e2 e3) t (TyRec ty1 ty2 ty3) venv =
    let r1  = mSubstR e1 _ ty1 venv
        r2  = mSubstR e2 _ ty2 venv
        r3  = mSubstR e3 _ ty3 venv
    in rHalts $ mSubstR_Rec e1 ty1 e2 e3 venv r1 r2 r3
  --
  mSubstHalts TZero TyNat TyZero venv = mSubstHalts_Zero venv
  --
  mSubstHalts (TSucc e) TyNat (TySucc ty) venv =
    let h = rHalts $ mSubstR e _ ty venv
    in mSubstHalts_Succ e venv h
  --
  mSubstHalts (TPred e) TyNat (TyPred ty) venv =
    let h = rHalts $ mSubstR e _ ty venv
    in mSubstHalts_Pred e ty venv h
  --
  mSubstHalts (TIfz e1 e2 e3) t (TyIfz ty1 ty2 ty3) venv =
    let r1  = mSubstR e1 _ ty1 venv
        r2  = mSubstR e2 _ ty2 venv
        r3  = mSubstR e3 _ ty3 venv
    in rHalts $ mSubstR_Ifz e1 ty1 e2 e3 venv r1 r2 r3

  mSubstR_Fun : (e : Term) -> (s : Ty) -> (t : Ty) ->
                Typing ctx e (s:->:t) -> (venv : VEnv ctx) ->
                rFun s t (msubst e Z venv)
  --
  mSubstR_Fun (TVar i) s t (TyVar prf) venv y ry =
    let r'  = mSubstR_Var _ _ prf venv
        imp = rImplication r'
    in imp y ry
  --
  mSubstR_Fun (TAbs e) s t (TyAbs s ty) venv y ry {ctx} =
    let H _ (y1 ** (vy1, tsty)) = rHalts ry
        ry1  = transStepPreservesR_1 s _ _ tsty ry
        tst1 = congApp2 {e=(TAbs $ msubst e (S Z) venv)} {v=VAbs} tsty
        tst2 = tst1 .+. (StBeta vy1)
        eq1  = mSubstAbsComm e Z venv
        tst3 = replace {P = \q => TransStep (TApp q y)
                                            (subst y1 Z (msubst e (S Z) venv))}
                       eq1 tst2
        eq2  = mSubstSubstSwap' e Z venv {s=s} y1 vy1 ry1
        tst4 = replace {P = \q => TransStep (TApp (msubst (TAbs e) Z venv) y) q}
                       eq2 tst3
        r'   = mSubstR e t ty (VCons y1 vy1 ry1 venv)
        ty'  = mSubstPreservesTy {ctx1=[]} (TAbs e) (TyAbs s ty) venv
        ty'' = TyApp ty' (rTyping y ry)
    in transStepPreservesR_2 t _ ty'' _ tst4 r'
  --
  mSubstR_Fun (TApp e1 e2) s t (TyApp ty1 ty2) venv y ry =
    let r1  = mSubstR e1 _ ty1 venv
        r2  = mSubstR e2 _ ty2 venv
        r'  = mSubstR_App e1 e2 venv r1 r2
        imp = rImplication r'
    in imp y ry
  --
  mSubstR_Fun (TRec e1 e2 e3) s t (TyRec ty1 ty2 ty3) venv y ry =
    let r1  = mSubstR e1 _ ty1 venv
        r2  = mSubstR e2 _ ty2 venv
        r3  = mSubstR e3 _ ty3 venv
        r'  = mSubstR_Rec e1 ty1 e2 e3 venv r1 r2 r3
        imp = rImplication r'
    in imp y ry
  --
  mSubstR_Fun (TIfz e1 e2 e3) s t (TyIfz ty1 ty2 ty3) venv y ry =
    let r1  = mSubstR e1 _ ty1 venv
        r2  = mSubstR e2 _ ty2 venv
        r3  = mSubstR e3 _ ty3 venv
        r'  = mSubstR_Ifz e1 ty1 e2 e3 venv r1 r2 r3
        imp = rImplication r'
    in imp y ry

-- Finally, the fact that 'R' holds for all
-- closed terms implies that evaluation halts
-- for all closed terms; i.e. all closed terms
-- are normalizable:
halts : (e : Term) -> Typing [] e t -> Halts e
halts e ty = let r = mSubstR e _ ty VNil
             in rHalts r

-- End: PREDICATE 'R' HOLDS FOR ALL CLOSED TERMS
------------------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Solution

namespace Preloaded

  %access export
  %default total

  ltePlus : LTE m1 n1 -> LTE m2 n2 -> LTE (m1 + m2) (n1 + n2)
  ltePlus {n1=Z} LTEZero lte = lte
  ltePlus {n1=S k} LTEZero lte = lteSuccRight $ ltePlus {n1=k} LTEZero lte
  ltePlus (LTESucc lte1) lte2 = LTESucc $ ltePlus lte1 lte2

  lteMult : LTE m1 n1 -> LTE m2 n2 -> LTE (m1 * m2) (n1 * n2)
  lteMult LTEZero _ = LTEZero
  lteMult {m1=S k} (LTESucc _) LTEZero = rewrite multZeroRightZero k in LTEZero
  lteMult (LTESucc lte1) (LTESucc lte2) = LTESucc $ ltePlus lte2 $ lteMult lte1 $ LTESucc lte2

  lteCongMult : (k : Nat) -> LTE m n -> LTE (m * k) (n * k)
  lteCongMult k lte = lteMult lte lteRefl

  lteCongMultLeft : (k : Nat) -> LTE m n -> LTE (k * m) (k * n)
  lteCongMultLeft k lte = lteMult lteRefl lte

%access export
%default total

-- Task 1. Prove that the successor of a Nat cannot be ≤ zero.
notSuccLteZero : Not (S n `LTE` Z)
notSuccLteZero LTEZero impossible

-- Task 2. Prove that you can add any Nat to the right side of a ≤-property.

lteStepK : (k : Nat) -> m `LTE` n -> m `LTE` k + n
lteStepK _ = ltePlus LTEZero

-- Task 3. Prove that you can remove "addition on the left" from both sides of a ≤-property.

plusLteInjLeft : (a : Nat) -> a + b `LTE` a + c -> b `LTE` c
plusLteInjLeft Z     abc         = abc
plusLteInjLeft (S k) (LTESucc x) = plusLteInjLeft k x

-- Task 4. Prove that you can remove "multiplication on the left" from both sides of a <-property.

succGoesOut : (x, y, a : Nat) -> x + a * (S y) = a + (x + a * y)
succGoesOut x y a = rewrite multRightSuccPlus a y in
                    rewrite plusCommutative x $ a + (a*y) in
                    rewrite sym $ plusAssociative a (a*y) x in
                    rewrite plusCommutative (a*y) x in
                    Refl

multLtInjLeft : a * b `LT` a * c -> b `LT` c
multLtInjLeft {a=Z}   {b}     {c}     = \LTEZero impossible
multLtInjLeft {a=S a} {b=Z}   {c=Z}   = rewrite multZeroRightZero a in id
multLtInjLeft {a=S a} {b=Z}   {c=S c} = \_ => LTESucc LTEZero
multLtInjLeft {a=S a} {b=S b} {c=Z}   = rewrite multZeroRightZero a in \LTEZero impossible
multLtInjLeft {a=S a} {b=S b} {c=S c} = rewrite succGoesOut b b a in
                                        rewrite succGoesOut c c a in
                                        rewrite plusSuccRightSucc a $ b + a*b in
                                        \(LTESucc lt) => LTESucc . multLtInjLeft {a=S a} $ plusLteInjLeft a lt

-- Task 5. Prove this.

lteDelta : x `LTE` y -> (d ** x + d = y)
lteDelta {y} LTEZero = (y ** Refl)
lteDelta {x=S x} {y=S y} (LTESucc lte) = (_ ** cong {f=S} $ snd $ lteDelta lte)

lteCutLeft : c + a `LTE` b -> a `LTE` b
lteCutLeft {c=Z}   = id
lteCutLeft {c=S k} = lteCutLeft . lteSuccLeft

multLtCross'delta : (delta : Nat ** c + delta = a) -> a * b `LT` c * d -> b `LT` d
multLtCross'delta (delta ** prf) {b} {c} =
  rewrite sym prf in
  rewrite plusCommutative c delta in
  rewrite multDistributesOverPlusLeft delta c b in
  rewrite plusSuccRightSucc (delta * b) (c * b) in
  multLtInjLeft . lteCutLeft

multLtCross : a * b `LT` c * d -> c `LTE` a -> b `LT` d
multLtCross {a} {c} abcd ca = multLtCross'delta (lteDelta ca) abcd

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


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

data Command = Add String
             | Get Integer
             | Search String
             | Size
             | 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 "search" substr = Just (Search substr)
parseCommand "size" "" = Just Size
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

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

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

getBySubstr : (substr : String) -> (store : DataStore) -> Maybe (String, DataStore)
getBySubstr substr store@(MkData s is) = Just (printEntries is 0, store)
    where
        printEntries : Vect n String -> Integer -> String
        printEntries [] ind = ""
        printEntries (y :: ys) ind =
            case isInfixOf substr y of
                False => printEntries ys (ind + 1)
                True => show ind ++ " " ++ y ++ "\n" ++ printEntries ys (ind + 1)

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) => getBySubstr substr store
        Just Size => Just ("Store has " ++ show (size store) ++ " entries.\n", store)
        Just Quit => Nothing

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

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
module Commons.Text.Display

%access public export
%default total

||| Present a version `String` of `a` for display.
|||
||| By default `Display` displays `a`s `Show` instance.
|||
||| Unlike `Show` there is no link to `Read`, and should see this as
||| inbetween `Pretty` and `Show`, that is useful for adhoc `toString`
||| methods.
interface Display a where
  display : a -> String

Display String where
  display x = x

Display Int where
  display x = show x

Display Nat where
  display n = show (the Integer (cast n))

Display Bool where
  display True = "True"
  display False = "False"

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
interface A where
  x : Nat
  f : {auto pf : x = 0} -> ()


text:
-- Matrix.idr
--
-- Matrix arithmetics with dependent types

module Matrix

import Data.Vect

-- matrix addition
addCol : Num numType => (x : Vect cols numType) -> (y : Vect cols numType) ->
                        Vect cols numType
addCol [] [] = []
addCol (x :: xs) (y :: ys) = x + y :: addCol xs ys

addMatrix : Num numType =>
            Vect rows (Vect cols numType) ->
            Vect rows (Vect cols numType) ->
            Vect rows (Vect cols numType)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = addCol x y :: addMatrix xs ys

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

transposeHelper : (x : Vect n elem) -> (xsTrans : Vect n (Vect len elem)) ->
                  Vect n (Vect (S len) elem)
transposeHelper x xsTrans = zipWith (::) x xsTrans

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

-- matrix multiplication

calcStride : Num numType => (x : Vect m numType) -> (y : Vect m numType) -> numType
calcStride [] [] = 0
calcStride (x :: xs) (y :: ys) = x * y + calcStride xs ys

doLeftRow : Num numType => (x : Vect m numType) ->
                           (ys' : Vect p (Vect m numType)) ->
                           Vect p numType
doLeftRow x [] = []
doLeftRow x (y :: ys) = calcStride x y :: doLeftRow x ys

multMatrix' : Num numType => (xs : Vect n (Vect m numType)) ->
                             (ys' : Vect p (Vect m numType)) ->
                             Vect n (Vect p numType)
multMatrix' [] ys' = []
multMatrix' (x :: xs) ys' = doLeftRow x ys' :: multMatrix' xs ys'

multMatrix : Num numType =>
             Vect n (Vect m numType) ->
             Vect m (Vect p numType) ->
             Vect n (Vect p numType)
multMatrix xs ys = let ys' = transposeMat ys in
                       multMatrix' xs ys'

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module xquant.Core.Types

import public Data.Complex
import public Data.Matrix

%default total

Fl : Type
Fl = Float

Amp : Type
Amp = Complex Fl

---- Hilbert Space types ----

||| State vector type for n-dimensional complex Hilbert space
StateSpace : Nat -> Type -> Type
StateSpace n a = Vect n (Complex a)

||| Quantum observable type, n x n complex matrices
Op : Nat -> Type -> Type
Op n a = Matrix n n (Complex a)

||| Ket vector, a n x 1 matrix collumn
KetSpace : Nat -> Type -> Type
KetSpace n a = Matrix n 1 (Complex a)

||| Bra vector, a 1 x n matrix row
BraSpace : Nat -> Type -> Type
BraSpace n a = Matrix 1 n (Complex a)

||| Qubit state space type, 2^n dimensional Hilbert space
Qubit : Nat -> Type -> Type
Qubit n a = StateSpace (power 2 n) a

||| Qubit observable type
QubitOp : Nat -> Type -> Type
QubitOp n a = let m = power 2 n in Matrix m m (Complex a)

||| Qubit collumn vector type
QubitKet : Nat -> Type -> Type
QubitKet n a = let m = power 2 n in Matrix m 1 (Complex a)

||| Qubit row vector type
QubitBra : Nat -> Type -> Type
QubitBra n a = let m = power 2 n in Matrix 1 m (Complex a)

c0 : Num a => Complex a
c0 = 0 :+ 0

c1 : Num a => Complex a
c1 = 1 :+ 0

ci : Num a => Complex a
ci = 0 :+ 1

m1 : (Neg a, Num a) => Complex a
m1 = -1 :+ 0

mi : (Neg a, Num a) => Complex a
mi = 0 :+ -1

-- sqn : (Foldable t, Functor t) => t Amp -> Amp
-- sqn = sum' . map ((\x => conjugate x * x))

-- normalize : (Foldable t, Functor t) => t Amp -> t Amp
-- normalize xs = let n = sqn xs in map (map (\x => xn))
-- Can't resolve type class Functor f
-- normalize : Vect n

---- Relativistic types ----

Mink : Type
Mink = Vect 4 Amp

MinkR : Type
MinkR = Vect 4 Fl

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module Language.Elab.Deriving.Util

import Language.Reflection

import Data.Strings

import Util

%language ElabReflection

-- try making conditionals here, like

-- wrapShow : Show a => String -> String -> a -> String
-- which wraps with given parens if a constructor doesn't have arguments

-- e.g. Just x = "(Just x)"  Nothing = "Nothing"

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

-- No good, all the ways I can think of to do this complain about
-- ElabReflection not being enabled. I don't really want users to have to turn
-- that on to use my Elab-defined things.

-- to use fastAppend without importing it at use-site
private
stringConcat : List String -> String
stringConcat = fastAppend

-- private
-- moduleNameElab : Elab String
-- moduleNameElab = do
--   [((NS ns _),_)] <- getType `{{moduleName}}
--     | [] => fail "moduleName is not in scope"
--     | _ => fail "moduleName is not unique in scope"
--   pure (stringConcat . intersperse "." . reverse $ ns)

fef : (a -> b -> c) -> Stream a -> List b -> Stream (List c)
fef f (x :: xs) ys = map (f x) ys :: fef f xs ys

rar : Stream (List c) -> Stream c
rar ([] :: xss) = rar xss
rar ((x :: xs) :: xss) = x :: rar (xs :: xss)

-- There's probably a better way to do this, I'm a little weak on how strictness
-- works
||| Provides an endless sequence of alphabet-grouped variable names
||| [a0,b0..z0], [a1,b1..z1], ...
export
infAZVar : Stream (List String)
infAZVar = let c = [0,1..] {a=Int}
               d = ['a'..'z']
           in fef (\x,y => strCons y "" ++ show x) c d

||| Provides an endless sequence of variable names
||| a0,b0..z0,a1,b1..z1,...
export
infVars : Stream String
infVars = rar infAZVar


text:
foo : Nat -> Nat -> Bool
foo x y with (x == y)
  foo x y | True with (y == x)
    foo x y | True | False | 10 = x
    foo x y | True | True = x
  foo x y | False = y


text:
data ErlList : List Type -> Type where
  Nil : ErlList []
  (::) : x -> ErlList xs -> ErlList (x :: xs)

data ErlType : Type -> Type where
  ETInteger : ErlType Integer
  ETString : ErlType String

data ErlTypes : List Type -> Type where
  ETErlTypesNil : ErlTypes []
  ETErlTypesCons : (ErlType x, ErlTypes xs) => ErlTypes (x :: xs)

erlCall : ErlList xs -> {auto prf : ErlTypes xs} -> ()
erlCall args = ()

foo : ()
foo = erlCall [1,2,3, "foo", "bar", "baz", 4,5,6]


text:
-- ------------------------------------- [ Data.Functor.Foldable.Instances.idr ]
-- Module      : Data.Functor.Foldable.Internal.Instances
-- Description : Instances of 'Recursive' and 'Corecursive' for various
--               things.
-- --------------------------------------------------------------------- [ EOH ]
module Data.Functor.Foldable.Instances

import Control.Monad.Free
import Data.Functor.Foldable.Mod

%access public export

implementation Base Nat Maybe where

implementation Recursive Maybe Nat where
  project Z = Nothing
  project (S a) = Just a

implementation Corecursive Maybe Nat where
  embed Nothing = Z
  embed (Just a) = S a

||| Fix-point data type for exotic recursion schemes of various kinds
data Fix : (Type -> Type) -> Type where
  Fx : f (Fix f) -> Fix f

||| Nu fix-point functor for coinduction
codata Nu : (f : Type -> Type) -> Type -> Type where
  NuF : ((a -> f a) -> a) -> b -> Nu f b

||| Mu fix-point functor for induction
data Mu : (Type -> Type) -> Type where
  MuF : ({a : Type} -> (a -> f a) -> a) -> Mu f

implementation Functor (Nu f) where
  map g (NuF h a) = NuF h (g a)

implementation Base t (Nu f) where

implementation Base (Fix t) f where

implementation Base (Mu f) f where

||| Create a fix-point with a functor
fix : f (Fix f) -> Fix f
fix = Fx

||| Unfix a 'Fix f'
unfix : Fix f -> f (Fix f)
unfix (Fx x) = x

data ListF : Type -> Type -> Type where
  NilF : ListF _ _
  Cons : a -> b -> ListF a b

data StreamF : Type -> Type -> Type where
  Pipe : a -> b -> StreamF a b

implementation Functor (StreamF a) where
  map f (Pipe a b) = Pipe a (f b)

implementation Functor (ListF a) where
  map _ NilF       = NilF
  map f (Cons a b) = Cons a (f b)

implementation Base b (ListF a) where

implementation Base b (StreamF a) where

||| Lambek's lemma assures us this function always exists.
lambek : (Recursive f t, Corecursive f t) => (t -> f t)
lambek = cata (map embed)

||| The dual of Lambek's lemma.
colambek : (Recursive f t, Corecursive f t) => (f t -> t)
colambek = ana (map project)

implementation Recursive (StreamF a) (Stream a) where
  project (x::xs) = Pipe x xs

implementation Corecursive (StreamF a) (Stream a) where
  embed (Pipe x xs) = x::xs

implementation Recursive (ListF a) (List a) where
  project [] = NilF
  project (x::xs) = Cons x xs

implementation Corecursive (ListF a) (List a) where
  embed NilF = []
  embed (Cons x xs) = x::xs


text:
module ContriverText.Util

import Data.SortedMap

dic0 : Ord k => SortedMap k v
dic0 = fromList []

dic1 : Ord k => k -> v -> SortedMap k v
dic1 k0 v0 = fromList [(k0, v0)]

dic2 : Ord k => k -> v -> k -> v -> SortedMap k v
dic2 k0 v0 k1 v1 = fromList [(k0, v0), (k1, v1)]

dic3 : Ord k => k -> v -> k -> v -> k -> v -> SortedMap k v
dic3 k0 v0 k1 v1 k2 v2 = fromList [(k0, v0), (k1, v1), (k2, v2)]

dic4 : Ord k => k -> v -> k -> v -> k -> v -> k -> v -> SortedMap k v
dic4 k0 v0 k1 v1 k2 v2 k3 v3 =
  fromList [(k0, v0), (k1, v1), (k2, v2), (k3, v3)]

max_stars_repo_name: rocketnia/contrivertext

max_issues_repo_name: rocketnia/contrivertext

max_forks_repo_name: rocketnia/contrivertext


text:
-- Shamelessly stolen from Edwin Brady
module Main

pythag : Int -> List (Int, Int, Int)
pythag max = [
    (x, y, z)
    | z <- [1..max]
    , y <- [1..z]
    , x <- [1..y]
    , x * x + y * y == z * z
  ]

main : IO ()
main = do
  printLn $ pythag 100
  printLn $ sort ["foo", "bar", "baz"]

max_stars_repo_name: ziman/idris-scheme

max_issues_repo_name: ziman/idris-scheme

max_forks_repo_name: ziman/idris-scheme


text:
module UPIO

foo : List (IO ())
foo = [putStrLn "hey", putStrLn "you"]

namespace Main
  main : IO ()
  main = let stuff = map unsafePerformIO foo in putStrLn (show stuff)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Web.Internal.UrlTypes

import JS

%default total

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

export data URL : Type where [external]

export
ToFFI URL URL where toFFI = id

export
FromFFI URL URL where fromFFI = Just

export
SafeCast URL where
  safeCast = unsafeCastOnPrototypeName "URL"

export data URLSearchParams : Type where [external]

export
ToFFI URLSearchParams URLSearchParams where toFFI = id

export
FromFFI URLSearchParams URLSearchParams where fromFFI = Just

export
SafeCast URLSearchParams where
  safeCast = unsafeCastOnPrototypeName "URLSearchParams"


text:
||| General definitions
module General

import public Data.List
import public Data.SortedMap

import public Gen.Abs
import public Gen.Common
import public Gen.Env
import public Gen.Errors
import public Gen.Eval
import public Gen.Parens
import public Gen.Plict
import public Gen.Scope
import public Gen.TypeChecker

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
module LightClick.Types.Meta

import Data.Vect

import Toolkit.Data.Vect.Extra

%default total

public export
data MTy : Type where
  PORT : String -> MTy
  UNIT : MTy
  MODULE : {n : _} -> (Vect (S n) String) -> MTy
  CONN : MTy
  DATA : MTy
  GATE : MTy

export
Show MTy where
  show (PORT s)    = "(MTyPort " <+> s <+> ")"
  show UNIT        = "(MTyUnit)"
  show (MODULE ns) = "(MTyModule " <+> show ns <+> ")"
  show CONN        = "(MTyConnection)"
  show DATA        = "(MTyData)"
  show GATE        = "(MTyGate)"

export
show' : MTy -> String
show' (PORT s)    = "(MTyPort)"
show' UNIT        = "(MTyUnit)"
show' (MODULE ns) = "(MTyModule)"
show' CONN        = "(MTyConnection)"
show' DATA        = "(MTyData)"
show' GATE        = "(MTyGate)"

export
Eq MTy where
  (==) (PORT x)    (PORT y)    = x == y
  (==) UNIT        UNIT        = True
  (==) (MODULE xs) (MODULE ys) = vecEq xs ys
  (==) CONN        CONN        = True
  (==) DATA        DATA        = True
  (==) GATE        GATE        = True
  (==) _ _ = False

portLabelMismatch : (contra : (x = y) -> Void)
                 -> (PORT x = PORT y)
                 -> Void
portLabelMismatch contra Refl = contra Refl

vecsAreDiff : {xs : Vect (S n) String}
           -> {ys : Vect (S m) String}
           -> (contra : (xs = ys) -> Void)
           -> (MODULE xs = MODULE ys)
           -> Void
vecsAreDiff contra Refl = contra Refl

noPortUnit : (PORT s = UNIT) -> Void
noPortUnit Refl impossible

noPortModule : (PORT s = MODULE ns) -> Void
noPortModule Refl impossible

noPortConn : (PORT s = CONN) -> Void
noPortConn Refl impossible

noPortData : (PORT s = DATA) -> Void
noPortData Refl impossible

noPortGate : (PORT s = GATE) -> Void
noPortGate Refl impossible

noUnitConn : (UNIT = CONN) -> Void
noUnitConn Refl impossible

noUnitModule : (UNIT = MODULE xs) -> Void
noUnitModule Refl impossible

noUnitData : (UNIT = DATA) -> Void
noUnitData Refl impossible

noUnitGate : (UNIT = GATE) -> Void
noUnitGate Refl impossible

noModuleConn : (MODULE xs = CONN) -> Void
noModuleConn Refl impossible

noModuleData : (MODULE xs = DATA) -> Void
noModuleData Refl impossible

noModuleGate : (MODULE xs = GATE) -> Void
noModuleGate Refl impossible

noConnData : (CONN = DATA) -> Void
noConnData Refl impossible

noConnGate : (CONN = GATE) -> Void
noConnGate Refl impossible

noDataGate : (DATA = GATE) -> Void
noDataGate Refl impossible

export
DecEq MTy where
  decEq (PORT x) x2 with (x2)
    decEq (PORT x) x2 | (PORT y) with (decEq x y)
      decEq (PORT y) x2 | (PORT y) | (Yes Refl) = Yes Refl
      decEq (PORT x) x2 | (PORT y) | (No contra) = No (portLabelMismatch contra)
    decEq (PORT x) x2 | UNIT        = No (noPortUnit)
    decEq (PORT x) x2 | (MODULE xs) = No (noPortModule)
    decEq (PORT x) x2 | CONN        = No (noPortConn)
    decEq (PORT x) x2 | DATA        = No noPortData
    decEq (PORT x) x2 | GATE        = No noPortGate

  decEq UNIT x2 with (x2)
    decEq UNIT x2 | (PORT s)    = No (negEqSym noPortUnit)
    decEq UNIT x2 | UNIT        = Yes Refl
    decEq UNIT x2 | (MODULE xs) = No (noUnitModule)
    decEq UNIT x2 | CONN        = No (noUnitConn)
    decEq UNIT x2 | DATA        = No (noUnitData)
    decEq UNIT x2 | GATE        = No (noUnitGate)

  decEq (MODULE xs) x2 with (x2)
    decEq (MODULE xs) x2 | (PORT s)    = No (negEqSym noPortModule)
    decEq (MODULE xs) x2 | UNIT        = No (negEqSym noUnitModule)
    decEq (MODULE xs) x2 | (MODULE ys) with (decEq xs ys)
      decEq (MODULE ys) x2 | (MODULE ys) | (Yes Refl) = Yes Refl
      decEq (MODULE xs) x2 | (MODULE ys) | (No contra) = No (vecsAreDiff contra)

    decEq (MODULE xs) x2 | CONN        = No (noModuleConn)
    decEq (MODULE xs) x2 | DATA        = No (noModuleData)
    decEq (MODULE xs) x2 | GATE        = No (noModuleGate)

  decEq CONN x2 with (x2)
    decEq CONN x2 | (PORT s)    = No (negEqSym noPortConn)
    decEq CONN x2 | UNIT        = No (negEqSym noUnitConn)
    decEq CONN x2 | (MODULE ys) = No (negEqSym noModuleConn)
    decEq CONN x2 | CONN        = Yes Refl
    decEq CONN x2 | DATA        = No noConnData
    decEq CONN x2 | GATE        = No noConnGate

  decEq DATA x2 with (x2)
    decEq DATA x2 | (PORT s)    = No (negEqSym noPortData)
    decEq DATA x2 | UNIT        = No (negEqSym noUnitData)
    decEq DATA x2 | (MODULE ys) = No (negEqSym noModuleData)

    decEq DATA x2 | CONN        = No (negEqSym noConnData)
    decEq DATA x2 | DATA        = Yes Refl
    decEq DATA x2 | GATE        = No noDataGate

  decEq GATE x2 with (x2)
    decEq GATE x2 | (PORT s)    = No (negEqSym noPortGate)
    decEq GATE x2 | UNIT        = No (negEqSym noUnitGate)
    decEq GATE x2 | (MODULE ys) = No (negEqSym noModuleGate)

    decEq GATE x2 | CONN        = No (negEqSym noConnGate)
    decEq GATE x2 | DATA        = No (negEqSym noDataGate)
    decEq GATE x2 | GATE        = Yes Refl

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

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/values.html#syntax-byte
module WebAssembly.Structure.Values.Bytes

import Data.Fin

import Decidable.Equality

-- Definition

public export
Byte : Type
Byte = Bits8

-- Decidable Equality

public export
implementation DecEq Byte where
  decEq x y = case x == y of -- Blocks if x or y not concrete
    True => Yes primitiveEq
    False => No primitiveNotEq
  where primitiveEq : x = y
        primitiveEq = really_believe_me (Refl {x})
        primitiveNotEq : x = y -> Void
        primitiveNotEq prf = believe_me {b = Void} ()

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Control.Monad.Free

import Control.EffectAlgebra

||| Higher-order free monad.
||| Acts as a syntax generator of effectful programs.
public export
data Free : (sig : (Type -> Type) -> (Type -> Type))
         -> Type
         -> Type where
  Return : a -> Free sig a
  Op : sig (Free sig) a -> Free sig a

public export
Syntax sig => Functor (Free sig) where
  map f (Return x) = Return (f x)
  map f (Op op)    = Op (emap (map f) op)

public export
Syntax sig => Applicative (Free sig) where
  pure v = Return v

  Return v <*> prog = map v prog
  Op op    <*> prog = Op (emap (<*> prog) op)

public export
Syntax sig => Monad (Free sig) where
  Return v >>= prog = prog v
  Op op    >>= prog = Op (emap (>>= prog) op)

public export
return : a -> Free sig a
return = Return

public export
inject : Inj sub sup => sub (Free sup) a -> Free sup a
inject = Op . inj

public export
project : Prj sup sub => Free sup a -> Maybe (sub (Free sup) a)
project (Op s) = Just (prj s)
project _ = Nothing


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/instructions.html#numeric-instructions
module WebAssembly.Structure.Instructions.DecEq

import WebAssembly.Structure.Values
import WebAssembly.Structure.Types
import WebAssembly.Structure.Modules.Indices
import WebAssembly.Structure.Instructions.Definition
import WebAssembly.Structure.Instructions.Control
import WebAssembly.Structure.Instructions.Memory

import Decidable.Equality

mutual
  total
  maybeEquals  : (is : List Instr) -> (js : List Instr) -> Maybe (is = js)
  maybeEquals [] [] = Just Refl
  maybeEquals [] (x :: xs) = Nothing
  maybeEquals (x :: xs) [] = Nothing
  maybeEquals (x :: xs) (y :: ys) = case maybeEqual x y of
    Nothing   => Nothing
    Just Refl => case maybeEquals xs ys of
      Nothing   => Nothing
      Just Refl => Just Refl

  total
  maybeEqual : (i1 : Instr) -> (i2 : Instr)     -> Maybe (i1 = i2)
  maybeEqual Unreachable       Unreachable       = Just Refl
  maybeEqual Nop               Nop               = Just Refl
  maybeEqual     (Block x is) (Block y js) with (decEq x y)
    maybeEqual   (Block x is) (Block y js) | No contra = Nothing
    maybeEqual   (Block x is) (Block x js) | Yes Refl with (maybeEquals is js)
      maybeEqual (Block x is) (Block x js) | Yes Refl | Nothing   = Nothing
      maybeEqual (Block x is) (Block x is) | Yes Refl | Just Refl = Just Refl
  maybeEqual (Loop x is)          (Loop y js)    = case decEq x y of
    No contra => Nothing
    Yes Refl  => case maybeEquals is js of
      Nothing   => Nothing
      Just Refl => Just Refl
  maybeEqual (If x is1 js1)    (If y is2 js2)    = case decEq x y of
    No contra => Nothing
    Yes Refl  => case maybeEquals is1 is2 of
      Nothing   => Nothing
      Just Refl => case maybeEquals js1 js2 of
        Nothing   => Nothing
        Just Refl => Just Refl
  maybeEqual Else              Else              = Just Refl
  maybeEqual End               End               = Just Refl
  maybeEqual (Br x)            (Br y)            = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (BrIf x)          (BrIf y)          = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (BrTable xs x)    (BrTable ys y)    = case decEq xs ys of
    No contra => Nothing
    Yes Refl  => case decEq x y of
      No contra => Nothing
      Yes Refl  => Just Refl
  maybeEqual Return            Return            = Just Refl
  maybeEqual (Call x)          (Call y)          = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (CallIndirect x)  (CallIndirect y)  = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual Drop              Drop              = Just Refl
  maybeEqual Select            Select            = Just Refl
  maybeEqual (LocalGet x)      (LocalGet y)      = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (LocalSet x)      (LocalSet y)      = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (LocalTee x)      (LocalTee y)      = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (GlobalGet x)     (GlobalGet y)     = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (GlobalSet x)     (GlobalSet y)     = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I32Load x)       (I32Load y)       = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I64Load x)       (I64Load y)       = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (F32Load x)       (F32Load y)       = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (F64Load x)       (F64Load y)       = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I32Load8S x)     (I32Load8S y)     = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I32Load8U x)     (I32Load8U y)     = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I32Load16S x)    (I32Load16S y)    = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I32Load16U x)    (I32Load16U y)    = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I64Load8S x)     (I64Load8S y)     = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I64Load8U x)     (I64Load8U y)     = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I64Load16S x)    (I64Load16S y)    = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I64Load16U x)    (I64Load16U y)    = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I64Load32S x)    (I64Load32S y)    = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I64Load32U x)    (I64Load32U y)    = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I32Store x)      (I32Store y)      = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I64Store x)      (I64Store y)      = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (F32Store x)      (F32Store y)      = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (F64Store x)      (F64Store y)      = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I32Store8 x)     (I32Store8 y)     = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I32Store16 x)    (I32Store16 y)    = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I64Store8 x)     (I64Store8 y)     = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I64Store16 x)    (I64Store16 y)    = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (I64Store32 x)    (I64Store32 y)    = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual MemorySize        MemorySize        = Just Refl
  maybeEqual MemoryGrow        MemoryGrow        = Just Refl
  maybeEqual   (I32Const x)    (I32Const y) with (decEq x y)
    maybeEqual (I32Const x)    (I32Const y) | No contra = Nothing
    maybeEqual (I32Const x)    (I32Const x) | Yes Refl  = Just Refl
  maybeEqual (I64Const x)      (I64Const y)      = case decEq x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (F32Const x)      (F32Const y)      = case decEq @{F32DecEq} x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual (F64Const x)      (F64Const y)      = case decEq @{F64DecEq} x y of
    No contra => Nothing
    Yes Refl  => Just Refl
  maybeEqual I32Eqz            I32Eqz            = Just Refl
  maybeEqual I32Eq             I32Eq             = Just Refl
  maybeEqual I32Ne             I32Ne             = Just Refl
  maybeEqual I32LtS            I32LtS            = Just Refl
  maybeEqual I32LtU            I32LtU            = Just Refl
  maybeEqual I32GtS            I32GtS            = Just Refl
  maybeEqual I32GtU            I32GtU            = Just Refl
  maybeEqual I32LeS            I32LeS            = Just Refl
  maybeEqual I32LeU            I32LeU            = Just Refl
  maybeEqual I32GeS            I32GeS            = Just Refl
  maybeEqual I32GeU            I32GeU            = Just Refl
  maybeEqual I64Eqz            I64Eqz            = Just Refl
  maybeEqual I64Eq             I64Eq             = Just Refl
  maybeEqual I64Ne             I64Ne             = Just Refl
  maybeEqual I64LtS            I64LtS            = Just Refl
  maybeEqual I64LtU            I64LtU            = Just Refl
  maybeEqual I64GtS            I64GtS            = Just Refl
  maybeEqual I64GtU            I64GtU            = Just Refl
  maybeEqual I64LeS            I64LeS            = Just Refl
  maybeEqual I64LeU            I64LeU            = Just Refl
  maybeEqual I64GeS            I64GeS            = Just Refl
  maybeEqual I64GeU            I64GeU            = Just Refl
  maybeEqual F32Eq             F32Eq             = Just Refl
  maybeEqual F32Ne             F32Ne             = Just Refl
  maybeEqual F32Lt             F32Lt             = Just Refl
  maybeEqual F32Gt             F32Gt             = Just Refl
  maybeEqual F32Le             F32Le             = Just Refl
  maybeEqual F32Ge             F32Ge             = Just Refl
  maybeEqual F64Eq             F64Eq             = Just Refl
  maybeEqual F64Ne             F64Ne             = Just Refl
  maybeEqual F64Lt             F64Lt             = Just Refl
  maybeEqual F64Gt             F64Gt             = Just Refl
  maybeEqual F64Le             F64Le             = Just Refl
  maybeEqual F64Ge             F64Ge             = Just Refl
  maybeEqual I32Clz            I32Clz            = Just Refl
  maybeEqual I32Ctz            I32Ctz            = Just Refl
  maybeEqual I32Popcnt         I32Popcnt         = Just Refl
  maybeEqual I32Add            I32Add            = Just Refl
  maybeEqual I32Sub            I32Sub            = Just Refl
  maybeEqual I32Mul            I32Mul            = Just Refl
  maybeEqual I32DivS           I32DivS           = Just Refl
  maybeEqual I32DivU           I32DivU           = Just Refl
  maybeEqual I32RemS           I32RemS           = Just Refl
  maybeEqual I32RemU           I32RemU           = Just Refl
  maybeEqual I32And            I32And            = Just Refl
  maybeEqual I32Or             I32Or             = Just Refl
  maybeEqual I32Xor            I32Xor            = Just Refl
  maybeEqual I32Shl            I32Shl            = Just Refl
  maybeEqual I32ShrS           I32ShrS           = Just Refl
  maybeEqual I32ShrU           I32ShrU           = Just Refl
  maybeEqual I32Rotl           I32Rotl           = Just Refl
  maybeEqual I32Rotr           I32Rotr           = Just Refl
  maybeEqual I64Clz            I64Clz            = Just Refl
  maybeEqual I64Ctz            I64Ctz            = Just Refl
  maybeEqual I64Popcnt         I64Popcnt         = Just Refl
  maybeEqual I64Add            I64Add            = Just Refl
  maybeEqual I64Sub            I64Sub            = Just Refl
  maybeEqual I64Mul            I64Mul            = Just Refl
  maybeEqual I64DivS           I64DivS           = Just Refl
  maybeEqual I64DivU           I64DivU           = Just Refl
  maybeEqual I64RemS           I64RemS           = Just Refl
  maybeEqual I64RemU           I64RemU           = Just Refl
  maybeEqual I64And            I64And            = Just Refl
  maybeEqual I64Or             I64Or             = Just Refl
  maybeEqual I64Xor            I64Xor            = Just Refl
  maybeEqual I64Shl            I64Shl            = Just Refl
  maybeEqual I64ShrS           I64ShrS           = Just Refl
  maybeEqual I64ShrU           I64ShrU           = Just Refl
  maybeEqual I64Rotl           I64Rotl           = Just Refl
  maybeEqual I64Rotr           I64Rotr           = Just Refl
  maybeEqual F32Abs            F32Abs            = Just Refl
  maybeEqual F32Neg            F32Neg            = Just Refl
  maybeEqual F32Ceil           F32Ceil           = Just Refl
  maybeEqual F32Floor          F32Floor          = Just Refl
  maybeEqual F32Trunc          F32Trunc          = Just Refl
  maybeEqual F32Nearest        F32Nearest        = Just Refl
  maybeEqual F32Sqrt           F32Sqrt           = Just Refl
  maybeEqual F32Add            F32Add            = Just Refl
  maybeEqual F32Sub            F32Sub            = Just Refl
  maybeEqual F32Mul            F32Mul            = Just Refl
  maybeEqual F32Div            F32Div            = Just Refl
  maybeEqual F32Min            F32Min            = Just Refl
  maybeEqual F32Max            F32Max            = Just Refl
  maybeEqual F32Copysign       F32Copysign       = Just Refl
  maybeEqual F64Abs            F64Abs            = Just Refl
  maybeEqual F64Neg            F64Neg            = Just Refl
  maybeEqual F64Ceil           F64Ceil           = Just Refl
  maybeEqual F64Floor          F64Floor          = Just Refl
  maybeEqual F64Trunc          F64Trunc          = Just Refl
  maybeEqual F64Nearest        F64Nearest        = Just Refl
  maybeEqual F64Sqrt           F64Sqrt           = Just Refl
  maybeEqual F64Add            F64Add            = Just Refl
  maybeEqual F64Sub            F64Sub            = Just Refl
  maybeEqual F64Mul            F64Mul            = Just Refl
  maybeEqual F64Div            F64Div            = Just Refl
  maybeEqual F64Min            F64Min            = Just Refl
  maybeEqual F64Max            F64Max            = Just Refl
  maybeEqual F64Copysign       F64Copysign       = Just Refl
  maybeEqual I32WrapI64        I32WrapI64        = Just Refl
  maybeEqual I32TruncF32S      I32TruncF32S      = Just Refl
  maybeEqual I32TruncF32U      I32TruncF32U      = Just Refl
  maybeEqual I32TruncF64S      I32TruncF64S      = Just Refl
  maybeEqual I32TruncF64U      I32TruncF64U      = Just Refl
  maybeEqual I64ExtendI32S     I64ExtendI32S     = Just Refl
  maybeEqual I64ExtendI32U     I64ExtendI32U     = Just Refl
  maybeEqual I64TruncF32S      I64TruncF32S      = Just Refl
  maybeEqual I64TruncF32U      I64TruncF32U      = Just Refl
  maybeEqual I64TruncF64S      I64TruncF64S      = Just Refl
  maybeEqual I64TruncF64U      I64TruncF64U      = Just Refl
  maybeEqual F32ConvertI32S    F32ConvertI32S    = Just Refl
  maybeEqual F32ConvertI32U    F32ConvertI32U    = Just Refl
  maybeEqual F32ConvertI64S    F32ConvertI64S    = Just Refl
  maybeEqual F32ConvertI64U    F32ConvertI64U    = Just Refl
  maybeEqual F32DemoteF64      F32DemoteF64      = Just Refl
  maybeEqual F64ConvertI32S    F64ConvertI32S    = Just Refl
  maybeEqual F64ConvertI32U    F64ConvertI32U    = Just Refl
  maybeEqual F64ConvertI64S    F64ConvertI64S    = Just Refl
  maybeEqual F64ConvertI64U    F64ConvertI64U    = Just Refl
  maybeEqual F64PromoteF32     F64PromoteF32     = Just Refl
  maybeEqual I32ReinterpretF32 I32ReinterpretF32 = Just Refl
  maybeEqual I64ReinterpretF64 I64ReinterpretF64 = Just Refl
  maybeEqual F32ReinterpretI32 F32ReinterpretI32 = Just Refl
  maybeEqual F64ReinterpretI64 F64ReinterpretI64 = Just Refl
  maybeEqual I32Extend8S       I32Extend8S       = Just Refl
  maybeEqual I32Extend16S      I32Extend16S      = Just Refl
  maybeEqual I64Extend8S       I64Extend8S       = Just Refl
  maybeEqual I64Extend16S      I64Extend16S      = Just Refl
  maybeEqual I64Extend32S      I64Extend32S      = Just Refl
  maybeEqual I32TruncSatF32S   I32TruncSatF32S   = Just Refl
  maybeEqual I32TruncSatF32U   I32TruncSatF32U   = Just Refl
  maybeEqual I32TruncSatF64S   I32TruncSatF64S   = Just Refl
  maybeEqual I32TruncSatF64U   I32TruncSatF64U   = Just Refl
  maybeEqual I64TruncSatF32S   I64TruncSatF32S   = Just Refl
  maybeEqual I64TruncSatF32U   I64TruncSatF32U   = Just Refl
  maybeEqual I64TruncSatF64S   I64TruncSatF64S   = Just Refl
  maybeEqual I64TruncSatF64U   I64TruncSatF64U   = Just Refl
  maybeEqual _                 _                 = Nothing

mutual
  total
  maybeNotEquals : (xs : List Instr) -> (Nothing = maybeEquals xs xs) -> Void
  maybeNotEquals [] Refl impossible
  maybeNotEquals (x :: xs) prf with (maybeEqual x x) proof h1
    | Just Refl with (maybeEquals xs xs) proof h2
      | Just Refl = absurd prf
      | Nothing = maybeNotEquals xs h2
    | Nothing = maybeNotEqual x h1

  maybeNotEqual : (a : Instr) -> (Nothing = maybeEqual a a) -> Void
  maybeNotEqual Unreachable Refl impossible
  maybeNotEqual Nop Refl impossible
  maybeNotEqual (Block x xs) prf with (decEq x x)
    | Yes Refl  with (maybeEquals xs xs) proof p
      | Just Refl = absurd prf
      | Nothing   = maybeNotEquals xs p
    | No contra = contra Refl
  maybeNotEqual (Loop x xs) prf with (decEq x x)
    | Yes Refl  with (maybeEquals xs xs) proof p
      | Just Refl = absurd prf
      | Nothing   = maybeNotEquals xs p
    | No contra = contra Refl
  maybeNotEqual (If x xs ys) prf with (decEq x x)
    | Yes Refl  with (maybeEquals xs xs) proof p1
      | Just Refl with (maybeEquals ys ys) proof p2
        | Just Refl = absurd prf
        | Nothing = maybeNotEquals ys p2
      | Nothing   = maybeNotEquals xs p1
    | No contra = contra Refl
  maybeNotEqual Else Refl impossible
  maybeNotEqual End Refl impossible
  maybeNotEqual (Br k) prf with (decEq k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (BrIf k) prf with (decEq k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (BrTable xs x) prf with (decEq xs xs)
    | Yes Refl   with (decEq x x)
      | Yes Refl  = absurd prf
      | No contra = contra Refl
    | No  contra = contra Refl
  maybeNotEqual Return Refl impossible
  maybeNotEqual (Call k) prf with (decEq k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (CallIndirect k) prf with (decEq k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual Drop Refl impossible
  maybeNotEqual Select Refl impossible
  maybeNotEqual (LocalGet k) prf with (decEq k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (LocalSet k) prf with (decEq k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (LocalTee k) prf with (decEq k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (GlobalGet k) prf with (decEq k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (GlobalSet k) prf with (decEq k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I32Load x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Load x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (F32Load x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (F64Load x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I32Load8S x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I32Load8U x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I32Load16S x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I32Load16U x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Load8S x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Load8U x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Load16S x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Load16U x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Load32S x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Load32U x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I32Store x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Store x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (F32Store x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (F64Store x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I32Store8 x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I32Store16 x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Store8 x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Store16 x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Store32 x) prf with (decEq x x)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual MemorySize Refl impossible
  maybeNotEqual MemoryGrow Refl impossible
  maybeNotEqual (I32Const k) prf with (decEq k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (I64Const k) prf with (decEq k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (F32Const k) prf with (decEq @{F32DecEq} k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual (F64Const k) prf with (decEq @{F64DecEq} k k)
    | Yes Refl   = absurd prf
    | No  contra = contra Refl
  maybeNotEqual I32Eqz Refl impossible
  maybeNotEqual I32Eq Refl impossible
  maybeNotEqual I32Ne Refl impossible
  maybeNotEqual I32LtS Refl impossible
  maybeNotEqual I32LtU Refl impossible
  maybeNotEqual I32GtS Refl impossible
  maybeNotEqual I32GtU Refl impossible
  maybeNotEqual I32LeS Refl impossible
  maybeNotEqual I32LeU Refl impossible
  maybeNotEqual I32GeS Refl impossible
  maybeNotEqual I32GeU Refl impossible
  maybeNotEqual I64Eqz Refl impossible
  maybeNotEqual I64Eq Refl impossible
  maybeNotEqual I64Ne Refl impossible
  maybeNotEqual I64LtS Refl impossible
  maybeNotEqual I64LtU Refl impossible
  maybeNotEqual I64GtS Refl impossible
  maybeNotEqual I64GtU Refl impossible
  maybeNotEqual I64LeS Refl impossible
  maybeNotEqual I64LeU Refl impossible
  maybeNotEqual I64GeS Refl impossible
  maybeNotEqual I64GeU Refl impossible
  maybeNotEqual F32Eq Refl impossible
  maybeNotEqual F32Ne Refl impossible
  maybeNotEqual F32Lt Refl impossible
  maybeNotEqual F32Gt Refl impossible
  maybeNotEqual F32Le Refl impossible
  maybeNotEqual F32Ge Refl impossible
  maybeNotEqual F64Eq Refl impossible
  maybeNotEqual F64Ne Refl impossible
  maybeNotEqual F64Lt Refl impossible
  maybeNotEqual F64Gt Refl impossible
  maybeNotEqual F64Le Refl impossible
  maybeNotEqual F64Ge Refl impossible
  maybeNotEqual I32Clz Refl impossible
  maybeNotEqual I32Ctz Refl impossible
  maybeNotEqual I32Popcnt Refl impossible
  maybeNotEqual I32Add Refl impossible
  maybeNotEqual I32Sub Refl impossible
  maybeNotEqual I32Mul Refl impossible
  maybeNotEqual I32DivS Refl impossible
  maybeNotEqual I32DivU Refl impossible
  maybeNotEqual I32RemS Refl impossible
  maybeNotEqual I32RemU Refl impossible
  maybeNotEqual I32And Refl impossible
  maybeNotEqual I32Or Refl impossible
  maybeNotEqual I32Xor Refl impossible
  maybeNotEqual I32Shl Refl impossible
  maybeNotEqual I32ShrS Refl impossible
  maybeNotEqual I32ShrU Refl impossible
  maybeNotEqual I32Rotl Refl impossible
  maybeNotEqual I32Rotr Refl impossible
  maybeNotEqual I64Clz Refl impossible
  maybeNotEqual I64Ctz Refl impossible
  maybeNotEqual I64Popcnt Refl impossible
  maybeNotEqual I64Add Refl impossible
  maybeNotEqual I64Sub Refl impossible
  maybeNotEqual I64Mul Refl impossible
  maybeNotEqual I64DivS Refl impossible
  maybeNotEqual I64DivU Refl impossible
  maybeNotEqual I64RemS Refl impossible
  maybeNotEqual I64RemU Refl impossible
  maybeNotEqual I64And Refl impossible
  maybeNotEqual I64Or Refl impossible
  maybeNotEqual I64Xor Refl impossible
  maybeNotEqual I64Shl Refl impossible
  maybeNotEqual I64ShrS Refl impossible
  maybeNotEqual I64ShrU Refl impossible
  maybeNotEqual I64Rotl Refl impossible
  maybeNotEqual I64Rotr Refl impossible
  maybeNotEqual F32Abs Refl impossible
  maybeNotEqual F32Neg Refl impossible
  maybeNotEqual F32Ceil Refl impossible
  maybeNotEqual F32Floor Refl impossible
  maybeNotEqual F32Trunc Refl impossible
  maybeNotEqual F32Nearest Refl impossible
  maybeNotEqual F32Sqrt Refl impossible
  maybeNotEqual F32Add Refl impossible
  maybeNotEqual F32Sub Refl impossible
  maybeNotEqual F32Mul Refl impossible
  maybeNotEqual F32Div Refl impossible
  maybeNotEqual F32Min Refl impossible
  maybeNotEqual F32Max Refl impossible
  maybeNotEqual F32Copysign Refl impossible
  maybeNotEqual F64Abs Refl impossible
  maybeNotEqual F64Neg Refl impossible
  maybeNotEqual F64Ceil Refl impossible
  maybeNotEqual F64Floor Refl impossible
  maybeNotEqual F64Trunc Refl impossible
  maybeNotEqual F64Nearest Refl impossible
  maybeNotEqual F64Sqrt Refl impossible
  maybeNotEqual F64Add Refl impossible
  maybeNotEqual F64Sub Refl impossible
  maybeNotEqual F64Mul Refl impossible
  maybeNotEqual F64Div Refl impossible
  maybeNotEqual F64Min Refl impossible
  maybeNotEqual F64Max Refl impossible
  maybeNotEqual F64Copysign Refl impossible
  maybeNotEqual I32WrapI64 Refl impossible
  maybeNotEqual I32TruncF32S Refl impossible
  maybeNotEqual I32TruncF32U Refl impossible
  maybeNotEqual I32TruncF64S Refl impossible
  maybeNotEqual I32TruncF64U Refl impossible
  maybeNotEqual I64ExtendI32S Refl impossible
  maybeNotEqual I64ExtendI32U Refl impossible
  maybeNotEqual I64TruncF32S Refl impossible
  maybeNotEqual I64TruncF32U Refl impossible
  maybeNotEqual I64TruncF64S Refl impossible
  maybeNotEqual I64TruncF64U Refl impossible
  maybeNotEqual F32ConvertI32S Refl impossible
  maybeNotEqual F32ConvertI32U Refl impossible
  maybeNotEqual F32ConvertI64S Refl impossible
  maybeNotEqual F32ConvertI64U Refl impossible
  maybeNotEqual F32DemoteF64 Refl impossible
  maybeNotEqual F64ConvertI32S Refl impossible
  maybeNotEqual F64ConvertI32U Refl impossible
  maybeNotEqual F64ConvertI64S Refl impossible
  maybeNotEqual F64ConvertI64U Refl impossible
  maybeNotEqual F64PromoteF32 Refl impossible
  maybeNotEqual I32ReinterpretF32 Refl impossible
  maybeNotEqual I64ReinterpretF64 Refl impossible
  maybeNotEqual F32ReinterpretI32 Refl impossible
  maybeNotEqual F64ReinterpretI64 Refl impossible
  maybeNotEqual I32Extend8S Refl impossible
  maybeNotEqual I32Extend16S Refl impossible
  maybeNotEqual I64Extend8S Refl impossible
  maybeNotEqual I64Extend16S Refl impossible
  maybeNotEqual I64Extend32S Refl impossible
  maybeNotEqual I32TruncSatF32S Refl impossible
  maybeNotEqual I32TruncSatF32U Refl impossible
  maybeNotEqual I32TruncSatF64S Refl impossible
  maybeNotEqual I32TruncSatF64U Refl impossible
  maybeNotEqual I64TruncSatF32S Refl impossible
  maybeNotEqual I64TruncSatF32U Refl impossible
  maybeNotEqual I64TruncSatF64S Refl impossible
  maybeNotEqual I64TruncSatF64U Refl impossible

  total
  instr_not_equal : (Nothing = maybeEqual i1 i2) -> (i1 = i2) -> Void
  instr_not_equal maybe_nothing Refl = maybeNotEqual i1 maybe_nothing

  public export
  implementation DecEq Instr where
    decEq i1 i2 with (maybeEqual i1 i2) proof maybe_nothing
      decEq i1 i1 | Just Refl = Yes Refl
      decEq i1 i2 | Nothing = No (instr_not_equal maybe_nothing)


text:
{-
Code examples about

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

and

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
-}

module Part2.Sec9_1_elem
import Data.Vect

%default total
%access public export

{- This type of code derives automatically with term search !-}
twoTest : Elem 2 [1,2,3]
twoTest = There Here

{-
second condition derived via interactive development resulted in absurd and I just
commented it out, the function is still total, uncommented compiles too

Note:
absurd : Uninhabited t => t -> a
later is uninhabited
-}
removeElem : (value : a) -> (xs : Vect (S n) a) ->
                   (prf : Elem value xs) ->
                   Vect n a
removeElem value (value :: ys) Here = ys
-- removeElem {n = Z} value (y :: []) (There later) = absurd later
removeElem {n = (S k)} value (y :: ys) (There later) = y :: removeElem value ys later

removeElem_auto : (value : a) -> (xs : Vect (S n) a) ->
                  {auto prf : Elem value xs} -> Vect n a
removeElem_auto value xs {prf} = removeElem value xs prf

{-
repl:
*Part2/Sec9_1_elem> removeElem 2 [1,2,3,4,5] (There Here)
[1, 3, 4, 5] : Vect 4 Integer

*Part2/Sec9_1_elem> removeElem_auto 2 [1,2,3,4,5]
[1, 3, 4, 5] : Vect 4 Integer
-}

data Test : (Vect 1 String) -> Type where
   MkTest : Test (removeElem_auto "str" ["hello", "str"])

data Test1 : (Vect 1 String) -> Type where
   MkTest1 : Test1 (removeElem "str" ["hello", "str"] (There Here))

{-
Note: removeElem seems to be not resolved/reduced at compile time, same it true for Haskell
repl:
*Part2/Sec9_1_elem> :t MkTest
MkTest : Test (removeElem_auto "str" ["hello", "str"])

*Part2/Sec9_1_elem> :t MkTest1
MkTest1 : Test1 (removeElem "str" ["hello", "str"] (There Here))
-}

{-
However: this does not compile :) but it does in Haskell :(
data TestWrong : (Vect 1 String) -> Type where
   MkTestWrong : TestWrong (removeElem "str1" ["hello", "str"] (There Here))

Compiler error:
   |
57 |    MkTestWrong : TestWrong (removeElem "str1" ["hello", "str"] (There Here))
   |                                                                 ~~~~~~~~~~
When checking type of Part2.Sec9_1_elem.MkTestWrong:
When checking argument later to constructor Data.Vect.There:
        Type mismatch between
                Elem x (x :: xs) (Type of Here)
        and
                Elem "str1" ["str"] (Expected type)

        Specifically:
                Type mismatch between
                        "str1"
                and
                        "str"
-}

{-
 Type safe version of elem function
 elem : Eq ty => (value : ty) -> (xs : Vect n ty) -> Bool
 -}
notInNil : Elem value [] -> Void
notInNil Here impossible
notInNil (There _) impossible

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

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

{-
*Part2/Sec9_1_elem> isElem 1 [2,3,1]
Yes (There (There Here)) : Dec (Elem 1 [2, 3, 1])
-}

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module Postgres.Exec

import Postgres.Utility
import Postgres.Data.Conn
import Postgres.Result

%foreign libpq "PQexec"
prim__dbExec : Ptr PGconn -> (command: String) -> PrimIO (Ptr PGresult)

data ExecSource : Type where
  MkExecSource : Conn -> ExecSource

ResultProducer ExecSource String where
  exec (MkExecSource conn) = pgExec conn where
     pgExec : Conn -> (command: String) -> IO (Ptr PGresult)
     pgExec (MkConn conn) command = primIO $ prim__dbExec conn command

||| Execute the given command, apply the given function `f`,
||| and then free the memory for the result.
export
withExecResult : Conn -> (command : String) -> (f : Result -> IO b) -> IO b
withExecResult conn command = withResult (MkExecSource conn) command

export
ignore : Result -> IO ()
ignore _ = pure ()

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
module Test.HList

import Data.Vect
import Data.HList

%access public export
%default total

assertEq : Eq a => String -> (given : a) -> (expected : a) -> IO ()
assertEq desc g e = if g == e
    then putStr $ ""
    else putStrLn $ "Test Failed " ++ desc

sample3 : HList 3 [Nat, Bool, String]
sample3 = [S Z, True, "Yeah"]

sample3a : HList 3 [Bool, String, Integer]
sample3a = [True, "Yeah", 10]

sample4 : HList 4 [Bool, String, Integer, Nat]
sample4 = [False, "Text", 10, 4]

sample4a : HList 4 [Bool, String, Integer, Nat]
sample4a = [False, "Text", 11, 4]

testHLength :  IO ()
testHLength = do
  assertEq "Hlength" (hlength sample3) 3
  assertEq "Hlength" (hlength sample4) 4

testGet :  IO ()
testGet =
  do
    assertEq "TestGet" (S Z) (get 0 sample3)
    assertEq "TestGet" True (get 1 sample3)
    assertEq "TestGet" "Yeah" (get 2 sample3)

testSet : IO ()
testSet = do
  assertEq "TestSet" [Z, True, "Yeah"] $ set 0 sample3 Z
  assertEq "TestSet" [S Z, False, "Yeah"] $ set 1 sample3 False

testSetWith : IO ()
testSetWith = do
  assertEq "TestSetWith" [S (S Z), True, "Yeah"] $ setWith 0 sample3 (\x => (S x) )
  assertEq "TestSetWith" [S Z, False, "Yeah"] $ setWith 1 sample3 (\x => not x)

testHead : IO ()
testHead = assertEq "TestHead" (S Z) $ head sample3

testLast : IO ()
testLast = assertEq "TestLast" "Yeah" $ last sample3

testZip : IO ()
testZip =
  assertEq "TestZip" [(S Z, True), (True, "Yeah"), ("Yeah", 10)] $ zip sample3 sample3a

testTake : IO ()
testTake =
  assertEq "TestTake" [S Z, True] $ take 2 sample3

testDrop : IO ()
testDrop =
  assertEq "TestDrop" [True, "Yeah"] $ drop 1 sample3

testInit : IO ()
testInit = do
  assertEq "TestInit" [False, "Text", 10] $ init sample4
  assertEq "TestInit" [S Z, True] $ init sample3

testTail : IO ()
testTail = do
  assertEq "TestTail" [True, "Yeah"] $ tail sample3
  assertEq "TestTail" ["Text", 10, 4] $ tail sample4

testConcat : IO ()
testConcat = do
    assertEq "TestConcat" [S Z, True, "Yeah", False, "Text", 10, 4] $ sample3 ++ sample4
    assertEq "TestConcat" [False, "Text", 10, 4, S Z, True, "Yeah"] $ sample4 ++ sample3

testUpdate : IO ()
testUpdate = do
  assertEq "TestUpdate" ["YS", "Text", 10, 4] $ update 0 sample4 "YS"
  assertEq "TestUpdate" [False, "Text", "YS", 4] $ update 2 sample4 "YS"
  assertEq "TestUpdate" [False, "Text", 10, "YS"] $ update 3 sample4 "YS"

testInsertAt : IO ()
testInsertAt = do
  assertEq "TestInsertAt" [10, S Z, True, "Yeah"] $ insertAt 0 sample3 10
  assertEq "TestInsertAt" [S Z, 10, True, "Yeah"] $ insertAt 1 sample3 10
  assertEq "TestInsertAt" [S Z, True, 10, "Yeah"] $ insertAt 2 sample3 10

testDeleteAt : IO ()
testDeleteAt = do
  assertEq "DeleteAt" ["Text", 10, 4] $ deleteAt 0 sample4
  assertEq "DeleteAt" [False, 10, 4] $ deleteAt 1 sample4
  assertEq "DeleteAt" [False, "Text", 4] $ deleteAt 2 sample4
  assertEq "DeleteAt" [False, "Text", 10] $ deleteAt 3 sample4

testOrd : IO ()
testOrd = do
  assertEq "TestOrd" True $ sample4 < sample4a
  assertEq "TestOrd" False $ sample4 > sample4a

testHap : IO ()
testHap =
  let res = hap [1, "---", S Z] [f11, f12, \a => "nat" ++ (show a)]
  in assertEq "testHap" [S (S Z), 3, "nat1"] res
  where
    f11 : Integer -> Nat
    f11 a = S (cast a)
    f12 : String -> Integer
    f12 a = cast $ Prelude.Strings.length a

max_stars_repo_name: gdefacci/idris-hlist

max_issues_repo_name: gdefacci/idris-hlist

max_forks_repo_name: gdefacci/idris-hlist


text:
-- ----------------------------------------------------------------- [ XML.idr ]
-- Module    : XML.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Readability.Process.XML

import Prelude.Strings

import Effects
import Effect.State

import XML.DOM
import XML.XPath

import Readability.WordTypes
import Readability.Stats
import Readability.Metrics

import Readability.Process.Effs
import public Readability.Process.Common

||| Extract the sentences from a text node.
getSentences : Document a -> List String
getSentences (Text t) = Strings.split (isEOS) t
  where
    isEOS : Char -> Bool
    isEOS e = List.elem e ['.', ':', '!', '"', '\'']

processPara : List String -> Eff () ReadEffs
processPara Nil     = pure ()
processPara (s::ss) = do
  processSentence $ words s
  updateReadState (\x => record {sentances = (sentances x) + 1} x)
  processPara ss

processParas : List $ Document NODE -> Eff () ReadEffs
processParas Nil     = pure ()
processParas (Node p::ps) = do
   processPara (getSentences p)
   processParas ps

export
calcReadabilityE : Document DOCUMENT
                -> Eff (Maybe ReadResult) ReadEffs
calcReadabilityE doc =
  case query "//*/text()" doc of
      Left err => pure Nothing
      Right ps => do
        processParas ps
        res <- getReadState
        pure $ Just (calcScores res)

export
calcReadability : Document DOCUMENT -> Maybe ReadResult
calcReadability doc = runPure $ calcReadabilityE doc

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

max_stars_repo_name: jfdm/idris-read

max_issues_repo_name: jfdm/idris-read

max_forks_repo_name: jfdm/idris-read