text:
||| Resources is framework for creating Resource Dependent EDSLs as described in the 2020 ECOOP paper:
||| *A Framework for Resource Dependent EDSLs in a Dependently Typed Language*.
|||
||| > Idris’ Effects library demonstrates how to embed resource dependent algebraic effect handlers into a
||| > dependently-typed host language, providing run-time and compile-time based reasoning on type-level resources.
||| > Building upon this work, Resources is a framework for realising Embedded Domain Specific Languages (EDSLs) with
||| > type-systems that contain domain specific substructural properties. Differing from Effects, Resources allows a
||| > language’s substructural properties to be encoded in a resource that is associated with language variables. Such
||| > an association allows for multiple effect instances to be reasoned about autonomically and without explicit
||| > type-level declaration. Type-level predicates are used as proof that the language’s substructural properties
||| > hold. Several exemplar EDSLs are presented that illustrates our framework’s operation and how dependent types
||| > provide correctness-by-construction guarantees that substructural properties of written programs hold.
|||
||| This module defines the Framework's core.
|||
module Resources

%default total
%access public export

namespace TypeLevel

  ||| Language variables are typed.
  |||
  ||| @Ty the type universe in which the variable exists.
  ||| @ty the variable's actual type.
  public export
  data Var : (Ty : Type) -> (ty : Ty) -> Type where
    MkVar : Var type value

  ||| Each variable has an associated abstract state.
  |||
  ||| @type the type universe in which the variable exists.
  ||| @calcStateType a function to compute the state's value from the provided type.
  ||| @value the variables type from which the abstract state's type is calculated.
  public export
  data StateItem : (type : Type)
                -> (calcStateType : type -> Type)
                -> (value : type)
                -> Type
    where
       MkStateItem : (value : type)
                  -> (label : Var type value)
                  -> (state : calcStateType value)
                  -> StateItem type calcStateType value

  ||| The context in which EDSL variables are bound and associated
  ||| with an abstract state.
  |||
  ||| The context is a simple cons-like data structure whose internal
  ||| values are are typed sith a common value.  We cannot utilise
  ||| Idris' `List` type as we need to collect at the type-level the
  ||| variable's type.  In future this should be replaced with `DList`
  ||| from idris-containers but that is future engineering.
  |||
  ||| @type the type universe in which the variable exists.
  ||| @calcStateType a function to compute the state's value from the provided type.
  public export
  data Context : (type : Type)
              -> (calcStateType : type -> Type)
              -> Type
    where
      Nil  : Context type calcStateType
      (::) : (item : StateItem type calcStateType value)
          -> (rest : Context type calcStateType)
          -> Context type calcStateType

  ||| A function to construct the type signature common to all
  ||| /Resource Dependent EDSLs/ as specified in the framework.
  |||
  ||| The signature describes a Hoare like monad that describes the
  ||| shift from an existing `pre` context to a new context based on
  ||| the expression's type.
  |||
  ||| @type the type universe in which the variable exists.
  ||| @calcStateType a function to compute the state's value from the provided type.
  public export
  Lang : (type : Type) -> (calcStateType : (val : type) -> Type) -> Type
  Lang type calcStateType =  (exprTy : Type)
                          -> (pre    : Context type calcStateType)
                          -> (postK  : exprTy -> Context type calcStateType)
                          -> Type

  ||| A simple algebraic data type to represent a /Resource Dependent EDSL/ instance.
  |||
  ||| @type the type universe in which the variable exists.
  ||| @calcStateType a function to compute the state's value from the provided type.
  public export
  data LANG : (type : Type) -> (calcStateType : type -> Type) -> Type where
      MkLang : (type : Type)
            -> (calcStateType : type -> Type)
            -> (lang : Lang type calcStateType)
            -> LANG type calcStateType

  ||| A type-level function calculate the next set of states based on a runtime value.
  |||
  ||| @value The runtime value used for calculation.
  ||| @postK The function that calculates the new state using `value`.
  public export
  updateState : (value : t)
             -> (postK : t -> Context type calcStateType)
             -> Context type calcStateType
  updateState value postK = postK value

  ||| A data structure that captures, generically, the sequencing of resource dependent EDSL language expressions.
  |||
  ||| @m the computation context in which this EDSL is defined.
  ||| @x the type associated with a language expression.
  ||| @calcStateType a function to compute the state's value from the provided type.
  ||| @spec The specific EDSL that is to be embedded.
  ||| @pre  The initial state that the expression knows about.
  ||| @post The final state the expression will be in that is dependent on the runtime value associated with the expression.
  public export
  data LangM : (m : Type -> Type)
            -> (x : Type)
            -> (spec : LANG type calcStateType)
            -> (pre  : Context type calcStateType)
            -> (post : x -> Context type calcStateType)
            -> Type
    where
      ||| Returns a value.
      Value : (value : a)
           -> {postK : a -> Context type calcStateType}
           -> LangM m a spec (postK value) postK

      ||| Provides sequencing of expressions and insertion of computed values into subsequent expressions.
      |||
      ||| @this The computation to run first.
      ||| @beInThis The next computation to run that uses the result of `this`.
      Let : (this : LangM m a spec old oldK)
         -> (beInThis : (val : a) -> LangM m b spec (oldK val) newK)
         -> LangM m b spec old newK

      ||| How to embedd an EDSL language expression into the framework.
      |||
      ||| @t The type of the expression.
      ||| @type the type universe in which the variable exists.
      ||| @calcStateType a function to compute the state's value from the provided type.
      ||| @pre  The initial state that the expression knows about.
      ||| @postK The final state the expression will be in that is dependent on the runtime value associated with the expression.
      ||| @eSig The function to compute the expressions type signature.
      ||| @expr The expression to embedd.
      Expr : {t,type : Type}
          -> {calcStateType : type -> Type}
          -> {pre   : Context type calcStateType}
          -> {postK : t -> Context type calcStateType}
          -> {eSig  : Lang type calcStateType}
          -> (expr : eSig t pre postK)
          -> LangM m t (MkLang type calcStateType eSig) pre (\v => updateState v postK)

  -- A high-level API to make embedding and use of the framework easier for users and designers.
  namespace API
    public export
    pure : (value : a) -> {postK : a -> Context type calcStateType} -> LangM m a spec (postK value) postK
    pure = Value

    public export
    (>>=) : LangM m a spec old oldK
       -> ((val : a) -> LangM m b spec (oldK val) postK)
       -> LangM m b spec old postK
    (>>=) = Let

    public export
    expr : {t,type : Type}
        -> {calcStateType : type -> Type}
        -> {pre   : Context type calcStateType}
        -> {postK : t -> Context type calcStateType}
        -> {eSig  : Lang type calcStateType}
        -> (expr : eSig t pre postK)
        -> LangM m t (MkLang type calcStateType eSig) pre (\v => updateState v postK)
    expr e = Expr e

namespace All
  ||| Ensure that a predicate applies to all items in the given context.
  |||
  ||| @p The predicate to apply to each item.
  ||| @c The context to apply the predicate to.
  public export
  data AllContext : (p : (value : type)
                      -> (item  : StateItem type calcStateType value)
                      -> Type)
                 -> (c : Context type calcStateType)
                 -> Type
    where
      Nil  : AllContext p Nil
      (::) : {p : (v : type) -> StateItem type calcStateType v -> Type}
          -> {value : type}
          -> {item  : StateItem type calcStateType value}
          -> {items : Context type calcStateType}
          -> (prf   : p value item)
          -> (rest  : AllContext p items)
          -> AllContext p (item :: items)

namespace Element

  ||| Existential quantification that there exists an item in the
  ||| context that the given predicate is satisifed.
  |||
  ||| @value The type of variable that the predicate is applied to.
  ||| @p The predicate to apply to each item.
  ||| @c The context to apply the predicate to.
  public export
  data InContext : (value : type)
                -> (p : StateItem type calcStateType value -> Type)
                -> (c : Context type calcStateType)
                -> Type
    where
      H : {p : StateItem type calcStateType value -> Type}
       -> (bewijs : p x)
       -> InContext value p (x :: rest)

      E : {p : StateItem type calcStateType value -> Type}
       -> (komt : InContext value p rest)
       -> InContext value p (not_x :: rest)

  Uninhabited (InContext value p Nil) where
    uninhabited (H _) impossible
    uninhabited (E _) impossible

  ||| Updates the element (at the provided index) in the provided context.
  |||
  ||| @context The context in which to apply the update.
  ||| @index The position of the item to be updated.
  ||| @f The update function to apply. The proof is included incase it contains
  |||    any interesting information for the update.
  public export
  update : (context : Context type calcStateType)
        -> (index   : InContext value predicate context)
        -> (f : (item   : StateItem type calcStateType value)
             -> (bewijs : predicate item)
             -> StateItem type calcStateType value)
        -> Context type calcStateType
  update (item :: rest)     (H bewijs) f = f item bewijs :: rest
  update (not_item :: rest) (E komt)   f = not_item :: update rest komt f

  ||| Remove the element (at the provided index) in the provided context.
  |||
  ||| @predicate The predicate that was applied to the item to be dropped.
  ||| @context The context in which the item is to be dropped.
  ||| @index The position of the item to drop.
  public export
  drop : {predicate : StateItem type calcStateType value -> Type}
      -> (context   : Context type calcStateType)
      -> (index     : InContext value predicate context)
      -> Context type calcStateType
  drop (item :: rest) (H bewijs) = rest
  drop (not_x :: rest) (E komt) = not_x :: drop rest komt

  ||| A helper function to replace the state in an element in our context.
  public export
  doUpdate : {predicate : StateItem type calcStateType value -> Type}
          -> (item     : StateItem type calcStateType value)
          -> (newState : calcStateType value)
          -> (bewijs   : predicate item)
          -> StateItem type calcStateType value
  doUpdate (MkStateItem value label state) newState bewijs = (MkStateItem value label newState)

  ||| An application of `update` to set the state for an item at the specified index.
  |||
  ||| @predicate The predicate that was applied to the item.
  ||| @context The context in which to apply the update.
  ||| @index The position of the item to be updated.
  ||| @item' The new state.
  public export
  setState : {predicate : StateItem type calcStateType value -> Type}
          -> (context   : Context type calcStateType)
          -> (index     : InContext value predicate context)
          -> (item'     : calcStateType value)
          -> Context type calcStateType
  setState context index item' = update context index (\i => doUpdate i item')

  ||| Proof that the given variable has the associated state.
  data HasVar : (lbl  : Var type value)
             -> (item : StateItem type calcStateType value)
             -> Type where
    DoesHaveVar : HasVar lbl (MkStateItem value lbl state)

-- -------------------------------------------------------------- [ Evaluation ]

namespace Env

  ||| Captures how EDSL variables are translated into concrete types.
  public export
  interface RealVar (type : Type) where
    CalcRealType : type -> Type

  ||| A container for holding concrete variable representations.
  public export
  data Tag : (type : Type) -> (value : type)
          -> Type
    where
      MkTag : RealVar type
           => (real : CalcRealType value)
           -> Tag type value

  ||| An evaluation environments to keep track of our language's real
  ||| variables and their abstract state, respective to the language's
  ||| typing context.
  public export
  data Env : (m : Type -> Type)
          -> (type    : Type)
          -> {calcStateType : type -> Type}
          -> (ctxt    : Context type calcStateType)
          -> Type
    where
      Nil  : Env m type Nil
      (::) : RealVar type
          => {item : StateItem type calcStateTy value}
          -> (tag  : Tag type value)
          -> (rest : Env m type items)
          -> Env m type (item::items)

  ||| Extracting a variable from the environment at the given index.
  |||
  ||| @env The environment being accessed.
  ||| @idx The position of the variable value to be extracted.
  public export
  lookup : RealVar type
        => (env : Env m type context)
        -> {p   : (item : StateItem type calcSTy value) -> Type}
        -> (idx : InContext value p context)
        -> Tag type value
  lookup (tag :: rest) (H bewijs) = tag
  lookup (tag :: rest) (E komt) = lookup rest komt

  ||| Update the type level state in the environment.
  |||
  ||| @env The environment being accessed.
  ||| @idx The position of the variable value to be updated
  ||| @up  The update function to be applied.
  public export
  update : RealVar type
        => (env  : Env m type ctxt)
        -> (idx  : InContext value p ctxt)
        -> (up   : (i : StateItem type calcSTy value)
                -> p i
                -> StateItem type calcSTy value)
        -> Env m type (update ctxt idx up)
  update (tag :: rest) (H bewijs) up = tag :: rest
  update (tag :: rest) (E komt) up = tag :: update rest komt up

  ||| Drop the state at the given index.
  |||
  ||| @env The environment being accessed.
  ||| @idx The position of the variable value to be dropped.
  public export
  drop : (env : Env m type ctxt)
      -> (idx : InContext value p ctxt)
      -> Env m type (drop ctxt idx)
  drop (tag :: rest) (H bewijs) = rest
  drop (tag :: rest) (E komt) = tag :: drop rest komt

namespace Building

  ||| The handler interface that describes how to evaluate languages in a presented computation context.
  |||
  ||| @type the type universe in which the variable exists.
  ||| @calcStateType a function to compute the state's value from the provided type.
  ||| @eSig The function to compute the expressions type signature.
  ||| @tyBRes The type associated with the accumulator if we are to build something.
  ||| @m The computation context in which to evaluate the language.
  public export
  interface RealVar type
         => Handler (type : Type)
                    (calcStateType : type -> Type)
                    (eSig   : Lang type calcStateType)
                    (tyBRes : Type)
                    (m      : Type -> Type) | type
    where
      ||| How to handle language expressions in the given computation context `m`.
      |||
      ||| @env the current evaluation context.
      ||| @expr the expression to be handled.
      ||| @acc an accumulator to be used if building something.
      ||| @cont a continuation to make things total.
      handle : (env  : Env m type pre)
            -> (expr : eSig tyExpr pre postK)
            -> (acc  : tyBRes)
            -> (cont : (value : tyExpr)
                    -> (env'  : Env m type (postK value))
                    -> (acc'  : tyBRes)
                    -> m tyRes)
            -> m tyRes

  ||| An internal helper function to evaluate an embedded language expression.
  |||
  ||| You will not need to call this at all.
  public export
  execBuild : RealVar type
           => Handler type calcStateType eSig tyBRes m
           => (env  : Env m type pre)
           -> (expr : eSig tyExpr pre postK)
           -> (acc  : tyBRes)
           -> (cont : (value : tyExpr)
                   -> (env'  : Env m type (updateState value postK))
                   -> (acc'  : tyBRes)
                   -> m tyRes)
           -> m tyRes
  execBuild env expr acc cont = handle env expr acc cont

  ||| An internal helper function to evaluate a `LangM` instance, and sequencing of expressions.
  |||
  ||| You will not need to call this at all.
  public export
  rawEval : RealVar type
         => Handler type calcStateType eSig tyBRes m
         => (env  : Env m type pre)
         -> (expr : LangM m tyExpr (MkLang type calcStateType eSig) pre postK)
         -> (acc  : tyBRes)
         -> (cont : (value : tyExpr)
                 -> (env'  : Env m type (postK value))
                 -> (acc'  : tyBRes)
                 -> m tyRes)
         -> m tyRes
  rawEval env (Value value {postK}) acc cont = cont value env acc
  rawEval env (Let this beIn) acc cont =
    rawEval env this acc (\this', env', acc' =>
                             rawEval env' (beIn this') acc' cont)
  rawEval env (Expr expr) acc cont = execBuild env expr acc cont

  ||| A helper data structure to container evaluation results.
  public export
  record Result (tyExpr : Type) (tyBRes : Type) where
    constructor MkResult
    computed : tyExpr
    built    : tyBRes

  ||| Evaluate the given closed program in the given applicative computation context `m`.
  |||
  ||| @init the initial value for our accumulator.
  ||| @expr the program to evaluate.
  public export
  run : Applicative m
     => RealVar type
     => Handler type calcStateType eSig tyBRes m
     => (init : tyBRes)
     -> (expr : LangM m tyExpr (MkLang type calcStateType eSig) Nil (const Nil))
     -> m (Result tyExpr tyBRes)
  run init expr = rawEval Nil expr init (\val, env', acc' => pure $ MkResult val acc')

  ||| Evaluate the given closed program in the identity computation context.
  |||
  ||| @init the initial value for our accumulator.
  ||| @expr the program to evaluate.
  public export
  runPure : RealVar type
        => Handler type calcStateType eSig tyBRes Basics.id
        => (init : tyBRes)
        -> (expr : LangM Basics.id tyExpr (MkLang type calcStateType eSig) Nil (const Nil))
        -> (Result tyExpr tyBRes)
  runPure init expr = rawEval Nil expr init (\val, env', acc' => MkResult val acc')

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

max_stars_repo_name: border-patrol/resources

max_issues_repo_name: border-patrol/resources

max_forks_repo_name: border-patrol/resources


text:
module ProofColDivSeqPostulate

import ProofColDivSeqBase

%default total
-- %language ElabReflection
%access export

%hide Language.Reflection.P

--            from ProofColDivSeqBase
-- ########################################
-- 無限降下法（の変形） Isabelleで証明した
postulate infiniteDescent :
  ((n:Nat) -> P (S n) 2 -> (m ** (LTE (S m) (S n), P m 2)))
    -> All Limited $ allDivSeq Z 2
      -> All Limited $ allDivSeq (n+n+n) 2

-- BaseLog0.txtより、保証される
postulate base0 : All Limited $ allDivSeq Z 2
-- ########################################

--            from ProofColDivSeqLvDown
-- ########################################
any2Sub : {pp : a -> Type} -> (x : a) -> (xs, ys : List a)
  -> Either (Any pp xs) (Any pp ys) -> Either (Any pp (x :: xs)) (Any pp ys)
any2Sub x []       ys (Left anL)  = absurd anL
any2Sub x (x2::xs) ys (Left anL)  = Left (There anL)
any2Sub x xs       ys (Right anR) = Right anR

-- これが肝
any2 : {pp : a -> Type} -> (xs, ys : List a)
  -> Any pp (xs ++ ys) -> Either (Any pp xs) (Any pp ys)
any2 []      ys an         = Right an
any2 (x::xs) ys (Here he)  = Left (Here he)
any2 (x::xs) ys (There th) =
  let foo = any2 xs ys th in any2Sub x xs ys foo

any3 : {pp : a -> Type} -> (xs1, xs2, xs3 : List a)
  -> Either (Any pp xs1) (Any pp (xs2++xs3))
    -> Either (Any pp xs1) (Either (Any pp xs2) (Any pp xs3))
any3 xs1 xs2 xs3 (Left prfL)  = Left prfL
any3 xs1 xs2 xs3 (Right prfR) = Right (any2 xs2 xs3 prfR)

any4 : {pp : a -> Type} -> (xs1, xs2, xs3, xs4 : List a)
  -> Either (Any pp xs1) (Either (Any pp xs2) (Any pp (xs3++xs4)))
    -> Either (Any pp xs1) (Either (Any pp xs2) (Either (Any pp xs3) (Any pp xs4)))
any4 xs1 xs2 xs3 xs4 (Left prfL)           = Left prfL
any4 xs1 xs2 xs3 xs4 (Right (Left prfRL))  = Right (Left prfRL)
any4 xs1 xs2 xs3 xs4 (Right (Right prfRR)) = Right (Right (any2 xs3 xs4 prfRR))

any5 : {pp : a -> Type} -> (xs1, xs2, xs3, xs4, xs5 : List a)
  -> Either (Any pp xs1) (Either (Any pp xs2) (Either (Any pp xs3) (Any pp (xs4++xs5))))
    -> Either (Any pp xs1) (Either (Any pp xs2) (Either (Any pp xs3) (Either (Any pp xs4) (Any pp xs5))))
any5 xs1 xs2 xs3 xs4 xs5 (Left prfL)                    = Left prfL
any5 xs1 xs2 xs3 xs4 xs5 (Right (Left prfRL))           = Right (Left prfRL)
any5 xs1 xs2 xs3 xs4 xs5 (Right (Right (Left prfRRL)))  = Right (Right (Left prfRRL))
any5 xs1 xs2 xs3 xs4 xs5 (Right (Right (Right prfRRR))) = Right (Right (Right (any2 xs4 xs5 prfRRR)))

any6 : {pp : a -> Type} -> (xs1, xs2, xs3, xs4, xs5, xs6 : List a)
  -> Either (Any pp xs1) (Either (Any pp xs2) (Either (Any pp xs3) (Either (Any pp xs4) (Any pp (xs5++xs6)))))
    -> Either (Any pp xs1) (Either (Any pp xs2) (Either (Any pp xs3) (Either (Any pp xs4) (Either (Any pp xs5) (Any pp xs6)))))
any6 xs1 xs2 xs3 xs4 xs5 xs6 (Left prfL)                             = Left prfL
any6 xs1 xs2 xs3 xs4 xs5 xs6 (Right (Left prfRL))                    = Right (Left prfRL)
any6 xs1 xs2 xs3 xs4 xs5 xs6 (Right (Right (Left prfRRL)))           = Right (Right (Left prfRRL))
any6 xs1 xs2 xs3 xs4 xs5 xs6 (Right (Right (Right (Left prfRRRL))))  = Right (Right (Right (Left prfRRRL)))
any6 xs1 xs2 xs3 xs4 xs5 xs6 (Right (Right (Right (Right prfRRRR)))) = Right (Right (Right (Right (any2 xs5 xs6 prfRRRR))))

any7 : {pp : a -> Type} -> (xs1, xs2, xs3, xs4, xs5, xs6, xs7 : List a)
  -> Either (Any pp xs1) (Either (Any pp xs2) (Either (Any pp xs3) (Either (Any pp xs4) (Either (Any pp xs5) (Any pp (xs6++xs7))))))
    -> Either (Any pp xs1) (Either (Any pp xs2) (Either (Any pp xs3) (Either (Any pp xs4) (Either (Any pp xs5) (Either (Any pp xs6) (Any pp xs7))))))
any7 xs1 xs2 xs3 xs4 xs5 xs6 xs7 (Left prfL)                                      = Left prfL
any7 xs1 xs2 xs3 xs4 xs5 xs6 xs7 (Right (Left prfRL))                             = Right (Left prfRL)
any7 xs1 xs2 xs3 xs4 xs5 xs6 xs7 (Right (Right (Left prfRRL)))                    = Right (Right (Left prfRRL))
any7 xs1 xs2 xs3 xs4 xs5 xs6 xs7 (Right (Right (Right (Left prfRRRL))))           = Right (Right (Right (Left prfRRRL)))
any7 xs1 xs2 xs3 xs4 xs5 xs6 xs7 (Right (Right (Right (Right (Left prfRRRRL)))))  = Right (Right (Right (Right (Left prfRRRRL))))
any7 xs1 xs2 xs3 xs4 xs5 xs6 xs7 (Right (Right (Right (Right (Right prfRRRRR))))) = Right (Right (Right (Right (Right (any2 xs6 xs7 prfRRRRR)))))

any8 : {pp : a -> Type} -> (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8 : List a)
  -> Either (Any pp xs1) (Either (Any pp xs2) (Either (Any pp xs3) (Either (Any pp xs4) (Either (Any pp xs5) (Either (Any pp xs6) (Any pp (xs7++xs8)))))))
    -> Either (Any pp xs1) (Either (Any pp xs2) (Either (Any pp xs3) (Either (Any pp xs4) (Either (Any pp xs5) (Either (Any pp xs6) (Either (Any pp xs7) (Any pp xs8)))))))
any8 xs1 xs2 xs3 xs4 xs5 xs6 xs7 xs8 (Left prfL)                                               = Left prfL
any8 xs1 xs2 xs3 xs4 xs5 xs6 xs7 xs8 (Right (Left prfRL))                                      = Right (Left prfRL)
any8 xs1 xs2 xs3 xs4 xs5 xs6 xs7 xs8 (Right (Right (Left prfRRL)))                             = Right (Right (Left prfRRL))
any8 xs1 xs2 xs3 xs4 xs5 xs6 xs7 xs8 (Right (Right (Right (Left prfRRRL))))                    = Right (Right (Right (Left prfRRRL)))
any8 xs1 xs2 xs3 xs4 xs5 xs6 xs7 xs8 (Right (Right (Right (Right (Left prfRRRRL)))))           = Right (Right (Right (Right (Left prfRRRRL))))
any8 xs1 xs2 xs3 xs4 xs5 xs6 xs7 xs8 (Right (Right (Right (Right (Right (Left prfRRRRRL))))))  = Right (Right (Right (Right (Right (Left prfRRRRRL)))))
any8 xs1 xs2 xs3 xs4 xs5 xs6 xs7 xs8 (Right (Right (Right (Right (Right (Right prfRRRRRR)))))) = Right (Right (Right (Right (Right (Right (any2 xs7 xs8 prfRRRRRR))))))

anyFinal : {pp : a -> Type} -> (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8 : List a)
  -> Any pp (xs1 ++ xs2 ++ xs3 ++ xs4 ++ xs5 ++ xs6 ++ xs7 ++ xs8)
    -> Either (Any pp xs1) (Either (Any pp xs2) (Either (Any pp xs3) (Either (Any pp xs4) (Either (Any pp xs5) (Either (Any pp xs6) (Either (Any pp xs7) (Any pp xs8)))))))
anyFinal xs1 xs2 xs3 xs4 xs5 xs6 xs7 xs8 prf =
  let prf2 = any2 xs1 (xs2 ++ xs3 ++ xs4 ++ xs5 ++ xs6 ++ xs7 ++ xs8) prf in
  let prf3 = any3 xs1 xs2 (xs3 ++ xs4 ++ xs5 ++ xs6 ++ xs7 ++ xs8) prf2 in
  let prf4 = any4 xs1 xs2 xs3 (xs4 ++ xs5 ++ xs6 ++ xs7 ++ xs8) prf3 in
  let prf5 = any5 xs1 xs2 xs3 xs4 (xs5 ++ xs6 ++ xs7 ++ xs8) prf4 in
  let prf6 = any6 xs1 xs2 xs3 xs4 xs5 (xs6 ++ xs7 ++ xs8) prf5 in
  let prf7 = any7 xs1 xs2 xs3 xs4 xs5 xs6 (xs7 ++ xs8) prf6 in
  let prf8 = any8 xs1 xs2 xs3 xs4 xs5 xs6 xs7 xs8 prf7 in prf8

-- 前方を削っているのは、（有限or無限を判定する）末尾に影響を与えないから
postulate dspCut : Any (Not . Limited) (map ([a,b] `dsp`) xs)
  -> Any (Not . Limited) xs
postulate dsp2Cut : Any (Not . Limited) (map ([a] `dsp2`) xs)
  -> Any (Not . Limited) xs

changeA' : (x, lv:Nat)
  -> Any (Not . Limited)
      (if (modNatNZ (x+7) 4 SIsNotZ) == 0
        then map ([6,-4] `dsp`) $ allDivSeq (divNatNZ ((x+7)*3) 4 SIsNotZ) (S lv)
        else [])
    -> Any (Not . Limited) (allDivSeq (divNatNZ ((x+7)*3) 4 SIsNotZ) (S lv))
changeA' x lv prf with ((modNatNZ (x+7) 4 SIsNotZ) == 0) proof p
  changeA' x lv prf | False = absurd prf
  changeA' x lv prf | True  = dspCut prf
changeA : (x, lv:Nat) -> Any (Not . Limited) (allDivSeqA x (S lv))
  -> Any (Not . Limited) (allDivSeq (divNatNZ ((x+7)*3) 4 SIsNotZ) (S lv))
changeA x lv prf = changeA' x lv $ replace (definiA x lv) prf

changeA0' : (x : Nat)
  -> Any (Not . Limited)
      (if (modNatNZ (x+7) 4 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+7) 4 SIsNotZ) 2 SIsNotZ) == 1
        then [[6,-4] `dsp` (Just (divSeq (divNatNZ ((x+7)*3) 4 SIsNotZ)))]
        else [])
    -> Any (Not . Limited) [Just (divSeq (divNatNZ ((x+7)*3) 4 SIsNotZ))]
changeA0' x prf with ((modNatNZ (x+7) 4 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+7) 4 SIsNotZ) 2 SIsNotZ) == 1) proof p
  changeA0' x prf | False = absurd prf
  changeA0' x prf | True  = dspCut prf
changeA0 : (x:Nat) -> Any (Not . Limited) (allDivSeqA x 0)
  -> Any (Not . Limited) [Just (divSeq (divNatNZ ((x+7)*3) 4 SIsNotZ))]
changeA0 x prf = changeA0' x $ replace (definiA0 x) prf

changeB : (x, lv:Nat) -> Any (Not . Limited) (allDivSeqB x (S lv))
  -> Any (Not . Limited) (allDivSeq (x*6+3) (S lv))
changeB x lv prf = dspCut $ replace (definiB x lv) prf

changeB0' : (x : Nat)
  -> Any (Not . Limited)
      (if (modNatNZ (x*6+3) 2 SIsNotZ) == 1
        then [[1,-2] `dsp` (Just (divSeq (x*6+3)))]
        else [])
    -> Any (Not . Limited) [Just (divSeq (x*6+3))]
changeB0' x prf with ((modNatNZ (x*6+3) 2 SIsNotZ) == 1) proof p
  changeB0' x prf | False = absurd prf
  changeB0' x prf | True  = dspCut prf
changeB0 : (x:Nat) -> Any (Not . Limited) (allDivSeqB x 0)
  -> Any (Not . Limited) [Just (divSeq (x*6+3))]
changeB0 x prf = changeB0' x $ replace (definiB0 x) prf

changeC : (x, lv:Nat) -> Any (Not . Limited) (allDivSeqC x (S lv))
  -> Any (Not . Limited) (allDivSeq (x*3+6) (S lv))
changeC x lv prf = dspCut $ replace (definiC x lv) prf

changeC0' : (x : Nat)
  -> Any (Not . Limited)
      (if (modNatNZ (x*3+6) 2 SIsNotZ) == 1
        then [[4,-4] `dsp` (Just (divSeq (x*3+6)))]
        else [])
    -> Any (Not . Limited) [Just (divSeq (x*3+6))]
changeC0' x prf with ((modNatNZ (x*3+6) 2 SIsNotZ) == 1) proof p
  changeC0' x prf | False = absurd prf
  changeC0' x prf | True  = dspCut prf
changeC0 : (x:Nat) -> Any (Not . Limited) (allDivSeqC x 0)
  -> Any (Not . Limited) [Just (divSeq (x*3+6))]
changeC0 x prf = changeC0' x $ replace (definiC0 x) prf

changeD' : (x, lv:Nat)
  -> Any (Not . Limited)
      (if (modNatNZ (x+1) 2 SIsNotZ) == 0
        then map ([3,-2] `dsp`) $ allDivSeq (divNatNZ ((x+1)*3) 2 SIsNotZ) (S lv)
        else [])
    -> Any (Not . Limited) (allDivSeq (divNatNZ ((x+1)*3) 2 SIsNotZ) (S lv))
changeD' x lv prf with ((modNatNZ (x+1) 2 SIsNotZ) == 0) proof p
  changeD' x lv prf | False = absurd prf
  changeD' x lv prf | True  = dspCut prf
changeD : (x, lv:Nat) -> Any (Not . Limited) (allDivSeqD x (S lv))
  -> Any (Not . Limited) (allDivSeq (divNatNZ ((x+1)*3) 2 SIsNotZ) (S lv))
changeD x lv prf = changeD' x lv $ replace (definiD x lv) prf

changeD0' : (x : Nat)
  -> Any (Not . Limited)
      (if (modNatNZ (x+1) 2 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+1) 2 SIsNotZ) 2 SIsNotZ) == 1
        then [[3,-2] `dsp` (Just (divSeq (divNatNZ ((x+1)*3) 2 SIsNotZ)))]
        else [])
    -> Any (Not . Limited) [Just (divSeq (divNatNZ ((x+1)*3) 2 SIsNotZ))]
changeD0' x prf with ((modNatNZ (x+1) 2 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+1) 2 SIsNotZ) 2 SIsNotZ) == 1) proof p
  changeD0' x prf | False = absurd prf
  changeD0' x prf | True  = dspCut prf
changeD0 : (x:Nat) -> Any (Not . Limited) (allDivSeqD x 0)
  -> Any (Not . Limited) [Just (divSeq (divNatNZ ((x+1)*3) 2 SIsNotZ))]
changeD0 x prf = changeD0' x $ replace (definiD0 x) prf

changeE : (x, lv:Nat) -> Any (Not . Limited) (allDivSeqE x (S lv))
  -> Any (Not . Limited) (allDivSeq (x*12+9) (S lv))
changeE x lv prf = dspCut $ replace (definiE x lv) prf

changeE0' : (x : Nat)
  -> Any (Not . Limited)
      (if (modNatNZ (x*12+9) 2 SIsNotZ) == 1
        then [[2,-4] `dsp` (Just (divSeq (x*12+9)))]
        else [])
    -> Any (Not . Limited) [Just (divSeq (x*12+9))]
changeE0' x prf with ((modNatNZ (x*12+9) 2 SIsNotZ) == 1) proof p
  changeE0' x prf | False = absurd prf
  changeE0' x prf | True  = dspCut prf
changeE0 : (x:Nat) -> Any (Not . Limited) (allDivSeqE x 0)
  -> Any (Not . Limited) [Just (divSeq (x*12+9))]
changeE0 x prf = changeE0' x $ replace (definiE0 x) prf

changeF' : (x, lv:Nat)
  -> Any (Not . Limited)
      (if (modNatNZ (x+3) 8 SIsNotZ) == 0
        then map ([5,-2] `dsp`) $ allDivSeq (divNatNZ ((x+3)*3) 8 SIsNotZ) (S lv)
        else [])
    -> Any (Not . Limited) (allDivSeq (divNatNZ ((x+3)*3) 8 SIsNotZ) (S lv))
changeF' x lv prf with ((modNatNZ (x+3) 8 SIsNotZ) == 0) proof p
  changeF' x lv prf | False = absurd prf
  changeF' x lv prf | True  = dspCut prf
changeF : (x, lv:Nat) -> Any (Not . Limited) (allDivSeqF x (S lv))
  -> Any (Not . Limited) (allDivSeq (divNatNZ ((x+3)*3) 8 SIsNotZ) (S lv))
changeF x lv prf = changeF' x lv $ replace (definiF x lv) prf

changeF0' : (x : Nat)
  -> Any (Not . Limited)
      (if (modNatNZ (x+3) 8 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+3) 8 SIsNotZ) 2 SIsNotZ) == 1
        then [[5,-2] `dsp` (Just (divSeq (divNatNZ ((x+3)*3) 8 SIsNotZ)))]
        else [])
    -> Any (Not . Limited) [Just (divSeq (divNatNZ ((x+3)*3) 8 SIsNotZ))]
changeF0' x prf with ((modNatNZ (x+3) 8 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+3) 8 SIsNotZ) 2 SIsNotZ) == 1) proof p
  changeF0' x prf | False = absurd prf
  changeF0' x prf | True  = dspCut prf
changeF0 : (x:Nat) -> Any (Not . Limited) (allDivSeqF x 0)
  -> Any (Not . Limited) [Just (divSeq (divNatNZ ((x+3)*3) 8 SIsNotZ))]
changeF0 x prf = changeF0' x $ replace (definiF0 x) prf

changeG' : (x, lv:Nat)
  -> Any (Not . Limited)
      (if (modNatNZ (x `minus` 21) 64 SIsNotZ) == 0 && x > 21
        then map ([6] `dsp2`) $ allDivSeq (divNatNZ (x `minus` 21) 64 SIsNotZ) (S lv)
        else [])
    -> Any (Not . Limited) (allDivSeq (divNatNZ (x `minus` 21) 64 SIsNotZ) (S lv))
changeG' x lv prf with ((modNatNZ (x `minus` 21) 64 SIsNotZ) == 0 && x > 21) proof p
  changeG' x lv prf | False = absurd prf
  changeG' x lv prf | True  = dsp2Cut prf
changeG : (x, lv:Nat) -> Any (Not . Limited) (allDivSeqG x (S lv))
  -> Any (Not . Limited) (allDivSeq (divNatNZ (x `minus` 21) 64 SIsNotZ) (S lv))
changeG x lv prf = changeG' x lv $ replace (definiG x lv) prf

changeG0' : (x : Nat)
  -> Any (Not . Limited)
      (if (modNatNZ (x `minus` 21) 64 SIsNotZ) == 0 && x > 21 && (modNatNZ (modNatNZ (x `minus` 21) 64 SIsNotZ) 2 SIsNotZ) == 1
        then [[6] `dsp2` (Just (divSeq (divNatNZ (x `minus` 21) 64 SIsNotZ)))]
        else [])
    -> Any (Not . Limited) [Just (divSeq (divNatNZ (x `minus` 21) 64 SIsNotZ))]
changeG0' x prf with ((modNatNZ (x `minus` 21) 64 SIsNotZ) == 0 && x > 21 && (modNatNZ (modNatNZ (x `minus` 21) 64 SIsNotZ) 2 SIsNotZ) == 1) proof p
  changeG0' x prf | False = absurd prf
  changeG0' x prf | True  = dsp2Cut prf
changeG0 : (x:Nat) -> Any (Not . Limited) (allDivSeqG x 0)
  -> Any (Not . Limited) [Just (divSeq (divNatNZ (x `minus` 21) 64 SIsNotZ))]
changeG0 x prf = changeG0' x $ replace (definiG0 x) prf

postulate defini3 : (x, lv:Nat)
  -> Either (Any (Not . Limited) $ allDivSeq x lv)
    (Either (Any (Not . Limited) $ allDivSeq (divNatNZ ((x+7)*3) 4 SIsNotZ) lv)
      (Either (Any (Not . Limited) $ allDivSeq (x*6+3) lv)
        (Either (Any (Not . Limited) $ allDivSeq (x*3+6) lv)
          (Either (Any (Not . Limited) $ allDivSeq (divNatNZ ((x+1)*3) 2 SIsNotZ) lv)
            (Either (Any (Not . Limited) $ allDivSeq (x*12+9) lv)
              (Either (Any (Not . Limited) $ allDivSeq (divNatNZ ((x+3)*3) 8 SIsNotZ) lv)
                      (Any (Not . Limited) $ allDivSeq (divNatNZ (x `minus` 21) 64 SIsNotZ) lv)))))))
    -> (Any (Not . Limited) $ allDivSeq x (S lv))
postulate defini0 : (x:Nat)
  -> Either (Any (Not . Limited) $ [Just (divSeq x)])
    (Either (Any (Not . Limited) $ [Just (divSeq (divNatNZ ((x+7)*3) 4 SIsNotZ))])
      (Either (Any (Not . Limited) $ [Just (divSeq (x*6+3))])
        (Either (Any (Not . Limited) $ [Just (divSeq (x*3+6))])
          (Either (Any (Not . Limited) $ [Just (divSeq (divNatNZ ((x+1)*3) 2 SIsNotZ))])
            (Either (Any (Not . Limited) $ [Just (divSeq (x*12+9))])
              (Either (Any (Not . Limited) $ [Just (divSeq (divNatNZ ((x+3)*3) 8 SIsNotZ))])
                      (Any (Not . Limited) $ [Just (divSeq (divNatNZ (x `minus` 21) 64 SIsNotZ))])))))))
    -> (Any (Not . Limited) $ allDivSeq x 0)

-- ProofColDivSeqLvDown.idrでlvDown'を証明したからOK
postulate lvDown : (n, lv:Nat) -> P n lv -> P n (pred lv)
-- ########################################

--            from sub0xxxxx
-- ########################################
-- 01 3(6x+1) --B[1,-2]--> 3x
postulate b18x3To3x' :
  (k:Nat) -> P (S (plus (plus (plus k k) (plus k k)) (plus k k))) 1 -> P k 2

-- 02 3(18x+4) --A[6,-4]->E[2,-4]--> 3(2x)
postulate ae54x12To6x' :
  (l:Nat) -> P (S (S (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                              (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                        (S (plus (plus (plus l l) l) (plus (plus l l) l)))))) 1
    -> P (plus l l) 3

-- 03 3(18x+10) --A[6,-4]->C[4,-4]--> 3(8x+3)
postulate ac54x30To24x9' :
  (l:Nat) -> P (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l))) (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                         (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))) 1
    -> P (S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))) 3

-- 04 3(18x+16) --A[6,-4]->B[1,-2]--> 3(4x+3)
postulate ab54x30To12x9' :
  (l:Nat) -> P (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                  (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                            (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))))) 1
    -> P (S (S (S (plus (plus l l) (plus l l))))) 3

-- 二重否定除去
postulate dne : ((a -> Void) -> Void) = a
-- 対偶
postulate contraposition2 :
  {A, B : Nat -> Type} -> (x : Nat) -> (Not $ B x -> Not $ A x) -> (A x -> B x)
-- 05 3(3x+2) --C[4,-4]--> 3x
postulate contraC9x6To3x' :
  (j:Nat) -> Not $ P j 2 -> Not $ P (S (S (plus (plus j j) j))) 1
{-
contraC9x6To3x' j =
  rewrite definiP j                           2 in
  rewrite definiP (S (S (plus (plus j j) j))) 1 in
  rewrite dne {a = All Limited (allDivSeq (plus (plus j j) j) 2)} in
  rewrite dne {a = All Limited (allDivSeq (S (S (plus (plus (plus (plus j j) j) (S (S (plus (plus j j) j)))) (S (S (plus (plus j j) j)))))) 1)} in ?rhs
-}
c9x6To3x' :
  (j:Nat) -> P (S (S (plus (plus j j) j))) 1 -> P j 2
c9x6To3x' j = contraposition2 j $ contraC9x6To3x' j

-- 06 3(12x+3) --E[2,-4]--> 3x
postulate e36x9To3x' :
  (l:Nat) -> P (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l)))))) 1 -> P l 2

-- 07 3(36x+9) --F[5,-2]->C[4,-4]--> 3(32x+7)
postulate fc108x27To96x21' :
  (o:Nat) -> P (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))) 1
    -> P (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                            (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))) 3

-- 08 3(36x+21) --F[5,-2]->B[1,-2]--> 3(16x+9)
postulate fb108x63To48x27' :
  (o:Nat) -> P (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                           (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                     (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                               (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))) 1
    -> P (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))))) 3

-- 09 3(36x+33) --F[5,-2]->E[2,-4]--> 3(8x+7)
postulate fe108x99To24x21' :
  (o:Nat) -> P (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                              (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                       (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))
                                  (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                 (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))))))) 1
    -> P (S (S (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))) 3

-- 10 3(36x+6) --F[5,-2]->E[2,-4]--> 3(8x+1)
postulate fe108x18To24x3' :
  (o:Nat) ->  P (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o))))))))) 1
    -> P (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))) 3

-- 11 3(36x+18) --F[5,-2]->C[4,-4]--> 3(32x+15)
postulate fc108x54To96x45' :
  (o:Nat) -> P (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                           (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                     (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                               (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))))) 1
    -> P (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                            (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))))))))))) 3

-- 12 3(36x+30) --F[5,-2]->B[1,-2]--> 3(16x+13)
postulate fb108x90To48x39' :
  (o:Nat) -> P (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                              (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))  (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                 (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))) 1
    -> P (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))))))))) 3

-- 13 3(36x+12) --F[5,-2]->B[1,-2]--> 3(16x+5)
postulate fb108x36To48x15' :
  (o:Nat) -> P (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                     (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                               (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))) 1
    -> P (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))) 3

-- 14 3(36x+24) --F[5,-2]->E[2,-4]--> 3(8x+5)
postulate fe108x72To24x15' :
  (o:Nat) ->  P (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                              (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                  (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))) 1
    -> P (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))) 3

-- 15 3(36x+36) --F[5,-2]->C[4,-4]--> 3(32x+31)
postulate fc108x108To96x93' :
  (o:Nat) -> P (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                 (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                           (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                             (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))
                                     (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                       (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))))))))) 1
    -> P (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                            (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o)
            (plus o o)))))))))))))))))))))))))))))))))))) 3
-- ########################################

--            from ProofColDivSeqMain
-- ########################################
all2Sub : {pp : a -> Type} -> (xs, ys : List a)
  -> All pp ((x::xs) ++ ys) -> (pp x, All pp (xs ++ ys))
all2Sub xs ys (Cons p ps) = (p, ps)

-- これが肝
all2 : {pp : a -> Type} -> (xs, ys : List a)
  -> All pp (xs ++ ys) -> All pp xs
all2 []      ys _   = NilA
all2 (x::xs) ys prf =
  let (prf2, prf3) = all2Sub xs ys prf
  in Cons prf2 (all2 xs ys prf3)
-- ########################################

ext: idr


text:
module Control.Eff.Reader

import Control.Eff.Internal

%default total

public export
data ReaderL : (lbl : k) -> (env : Type) -> (a : Type) -> Type where
  [search lbl]
  Ask : ReaderL lbl env env

public export
Reader : (env,a : Type) -> Type
Reader = ReaderL ()

export
askAt : (0 lbl : k) -> Has (ReaderL lbl env) fs => Eff fs env
askAt lbl = send $ Ask {lbl}

export %inline
ask : Has (Reader env) fs => Eff fs env
ask = askAt ()

export %inline
asksAt : (0 lbl : k) -> Has (ReaderL lbl env) fs => (env -> a) -> Eff fs a
asksAt lbl f = f <$> askAt lbl

export %inline
asks : Has (Reader env) fs => (env -> a) -> Eff fs a
asks f = f <$> ask

--------------------------------------------------------------------------------
--          Running Reader
--------------------------------------------------------------------------------

export
handleReader :  {0 m : Type -> Type}
             -> m env
             -> ReaderL lbl env a
             -> m a
handleReader x Ask = x

unReader : env -> ReaderL lbl env a -> a
unReader ve Ask = ve

export
runReaderAt : (0 lbl : k)
            -> Has (ReaderL lbl env) fs
            => env
            -> Eff fs t
            -> Eff (fs - ReaderL lbl env) t
runReaderAt _ ve = handleRelay pure $ \v,f => f (unReader ve v)

export %inline
runReader : Has (Reader env) fs => env -> Eff fs t -> Eff (fs - Reader env) t
runReader = runReaderAt ()


text:
||| Implementation of a Idris2 LSP Server.
|||
||| (C) The Idris Community, 2021
module Server.Main

import Core.Context
import Core.Core
import Core.InitPrimitives
import Core.Metadata
import Core.UnifyState
import Data.List1
import Data.Strings
import Idris.CommandLine
import Idris.REPL.Opts
import Idris.REPL.Common
import Idris.Package.Types
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import IdrisPaths
import Language.JSON
import Language.LSP.Message
import Libraries.Utils.Path
import Server.Configuration
import Server.Log
import Server.ProcessMessage
import Server.Response
import Server.Utils
import System
import System.Directory
import System.File

data Header = ContentLength Int | ContentType String | StartContent

Show Header where
  show (ContentLength l) = "Content-Length: " ++ show l
  show (ContentType s) = "Content-Type: " ++ s
  show StartContent = "stop"

headerPart : List Header -> String
headerPart [] = ""
headerPart (ContentLength l :: xs) = "Content-Length: " ++ show l ++ "\r\n" ++ headerPart xs
headerPart (ContentType s :: xs) = "Content-Type: " ++ s ++ "\r\n" ++ headerPart xs
headerPart (StartContent :: _) = "\r\n"

parseHeader : String -> Maybe Header
parseHeader "\r\n" = Just StartContent
parseHeader str =
  if "Content-Length:" `isPrefixOf` str
     then let (_ ::: xs) = split (== ':') str in
              ContentLength <$> parseInteger (fastAppend xs)
     else if "Content-Type:" `isPrefixOf` str
             then let (_ ::: xs) = split (== ':') str in
                      Just $ ContentType (fastAppend xs)
             else Nothing

parseHeaderPart : (h : File) -> Core (Either FileError (Maybe Int))
parseHeaderPart h = do
  Right line <- fGetHeader h
    | Left err => pure $ Left err
  case parseHeader line of
    Just (ContentLength l) => parseHeaderPart h *> pure (Right (Just l))
    Just (ContentType s) => parseHeaderPart h
    Just StartContent => pure $ Right Nothing
    Nothing => pure $ Right Nothing

runServer : Ref LSPConf LSPConfiguration
         => Ref Ctxt Defs
         => Ref UST UState
         => Ref Syn SyntaxInfo
         => Ref MD Metadata
         => Ref ROpts REPLOpts
         => Core ()
runServer = do
  inputHandle <- gets LSPConf inputHandle
  Right (Just l) <- parseHeaderPart inputHandle
    | _ => do logString Error "Error while parsing header part"
              sendUnknownResponseMessage parseError
              runServer
  Right msg <- coreLift $ fGetChars inputHandle l
    | Left err => do logShow Error (show err)
                     sendUnknownResponseMessage (internalError "Error while recovering the content part of a message")
                     runServer
  logString Debug msg
  let Just msg = parse msg
    | Nothing => do logString Error "Error while parsing content"
                    sendUnknownResponseMessage parseError
                    runServer
  let Just (Client ** type ** method ** msg) = the (Maybe (from ** type ** method : Method from type ** Message type method)) $ fromJSON msg
    | Just (Server ** type ** method ** msg) => do
        logString Warning "Received server message"
        sendUnknownResponseMessage (invalidRequest "Received a message meant to be sent by the server")
        runServer
    | Nothing => do logString Error "Error while parsing message"
                    sendUnknownResponseMessage parseError
                    runServer
  logString Info $ "Received message for method " ++ show (toJSON method)
  catch (processMessage method msg)
        (\err => do
          logString Error (show err)
          resetContext)
  runServer

main : IO ()
main = do
  coreRun (do l <- newRef LSPConf defaultConfig
              defs <- initDefs
              c <- newRef Ctxt defs
              s <- newRef Syn initSyntax
              addPrimitives
              setPrefix yprefix
              addPkgDir "prelude" anyBounds
              addPkgDir "base" anyBounds
              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
              o <- newRef ROpts (Opts.defaultOpts Nothing (REPL False) [])
              u <- newRef UST initUState
              m <- newRef MD initMetadata
              runServer)
    (\err => fPutStrLn stderr ("CRITICAL UNCAUGHT ERROR " ++ show err) *> exitWith (ExitFailure 1))
    (\res => pure ())


text:
||| Binary representation of natural numbers.
module BiNat

%access public export
%default total

data Bit = O | I

infixl 7 -:

data BiNat : Type where
  ||| Leading one bit
  J : BiNat

  ||| Append a bit to a BiNat.
  ||| `J -: O -: I -: I` corresponds to `1011`.
  (-:) : BiNat -> Bit -> BiNat

Uninhabited (J = n -: b) where
  uninhabited Refl impossible
Uninhabited (n -: b = J) where
  uninhabited Refl impossible
Uninhabited (m -: O = n -: I) where
  uninhabited Refl impossible
Uninhabited (m -: I = n -: O) where
  uninhabited Refl impossible

succ' : BiNat -> List Bit -> BiNat
succ' J        acc = foldl (-:) (J -: O) acc
succ' (n -: O) acc = foldl (-:) (n -: I) acc
succ' (n -: I) acc = succ' n (O :: acc)

||| The successor of a natural number.
succ : BiNat -> BiNat
succ n = succ' n []

pred' : BiNat -> List Bit -> BiNat
pred' J              acc = foldl (-:) J acc
pred' (n -: I)       acc = foldl (-:) (n -: O) acc
pred' (J -: O)       acc = foldl (-:) J acc
pred' (ns -: n -: O) acc = pred' (ns -: n) (I :: acc)

||| The predecessor of a natural number, but `pred J` is `J`.
pred : BiNat -> BiNat
pred n = pred' n []

nextCarry : Bit -> Bit -> Bit -> Bit
nextCarry I I I = I
nextCarry I I O = I
nextCarry I O I = I
nextCarry O I I = I
nextCarry _ _ _ = O

nextAcc : Bit -> Bit -> Bit -> Bit
nextAcc O O O = O
nextAcc O I I = O
nextAcc I O I = O
nextAcc I I O = O
nextAcc _ _ _ = I

plus' : BiNat -> BiNat -> Bit -> List Bit -> BiNat
plus' J         J         c acc = foldl (-:) (J -: c) acc
plus' J         ns        O acc = succ' ns acc
plus' J         (ns -: n) I acc = succ' ns (n :: acc)
plus' ms        J         O acc = succ' ms acc
plus' (ms -: m) J         I acc = succ' ms (m :: acc)
plus' (ms -: m) (ns -: n) c acc = plus' ms ns (nextCarry m n c) (nextAcc m n c :: acc)

||| Add two natural numbers.
plus : BiNat -> BiNat -> BiNat
plus m n = plus' m n O []

mult' : BiNat -> BiNat -> BiNat -> BiNat
mult' J         added acc = pred (plus added acc)
mult' (ms -: O) added acc = mult' ms (added -: O) acc
mult' (ms -: I) added acc = mult' ms (added -: O) (plus added acc)

||| Multiply natural numbers.
mult : BiNat -> BiNat -> BiNat
mult m n = mult' m n J

||| Convert an Integer to a BiNat, mapping non-positive numbers to J.
fromInteger : Integer -> BiNat
fromInteger i = if i <= 1 then J else fromInteger' i [] where
  fromInteger' : Integer -> List Bit -> BiNat
  fromInteger' 1 acc = foldl (-:) J acc
  fromInteger' i acc =
    fromInteger'
      (assert_smaller i (assert_total (div i 2)))
      ((if assert_total (mod i 2) == 0 then O else I) :: acc)

||| Convert a BiNat to an Integer.
toInteger : BiNat -> Integer
toInteger n = toInteger' n 1 0 where
  toInteger' : BiNat -> Integer -> Integer -> Integer
  toInteger' J         added acc = added + acc
  toInteger' (ns -: O) added acc = toInteger' ns (added * 2) acc
  toInteger' (ns -: I) added acc = toInteger' ns (added * 2) (acc + added)

tailToBiNat : List Bit -> BiNat
tailToBiNat []          = J
tailToBiNat (O :: tail) = tailToBiNat tail
tailToBiNat (I :: tail) = foldl (-:) J tail

minus' : BiNat -> BiNat -> List Bit -> BiNat
minus' J          J         tail = tailToBiNat tail
minus' J          ns        tail = J
minus' (J -: O)   J         tail = foldl (-:) J tail
minus' (ms -: O)  J         tail = foldl (-:) (pred ms -: I) tail
minus' (ms -: I)  J         tail = foldl (-:) (ms -: O) tail
minus' (ms -: O)  (ns -: O) tail = minus' ms ns (O :: tail)
minus' (J -: O)   (ns -: I) tail = J
minus' (ms -: O)  (ns -: I) tail = minus' (pred ms) ns (I :: tail)
minus' (ms -: I)  (ns -: O) tail = minus' ms ns (I :: tail)
minus' (ms -: I)  (ns -: I) tail = minus' ms ns (O :: tail)

||| Subtract natural numbers. If the second number is larger than or equal to the first, return J.
minus : BiNat -> BiNat -> BiNat
minus m n = minus' m n []

Eq BiNat where
  J         == J         = True
  (ns -: O) == (ms -: O) = ns == ms
  (ns -: I) == (ms -: I) = ns == ms
  _         == _         = False

||| Proofs that a BiNat is strictly less than another BiNat.
data LT : BiNat -> BiNat -> Type where
  JLT : (ns : BiNat) -> (n : Bit) -> LT J (ns -: n)
  LTLeading : (ms, ns : BiNat) -> ms = ns -> LT (ms -: O) (ns -: I)
  LTAppend : (ms, ns : BiNat) -> LT ms ns -> (m, n : Bit) -> LT (ms -: m) (ns -: n)

||| Strict greater than
GT : BiNat -> BiNat -> Type
GT m n = LT n m

Uninhabited (LT n J) where
  uninhabited JLT       impossible
  uninhabited LTLeading impossible
  uninhabited LTAppend  impossible

||| Less than or equal to
data LTE : BiNat -> BiNat -> Type where
  LTEEqual : (m, n : BiNat) -> m = n -> LTE m n
  LTELessThan : (m, n : BiNat) -> LT m n -> LTE m n

||| Greater than or equal to
GTE : BiNat -> BiNat -> Type
GTE m n = LTE n m

compare' : BiNat -> BiNat -> Ordering -> Ordering
compare' J         J         last = last
compare' J         (ns -: n) last = LT
compare' (ms -: m) J         last = GT
compare' (ms -: O) (ns -: O) last = compare' ms ns last
compare' (ms -: O) (ns -: I) last = compare' ms ns LT
compare' (ms -: I) (ns -: O) last = compare' ms ns GT
compare' (ms -: I) (ns -: I) last = compare' ms ns last

Ord BiNat where
  compare m n = compare' m n EQ

Num BiNat where
  (+) = plus
  (*) = mult
  fromInteger = BiNat.fromInteger

max_stars_repo_name: SekiT/BiNat

max_issues_repo_name: SekiT/BiNat

max_forks_repo_name: SekiT/BiNat


text:
module Main

main : IO ()
main = nullPtr null >>= printLn

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 math.Epsilon

import xquant.Core.Types

%default total

class Epsilon a where
  infinitessimal : a -> Bool

instance Epsilon Fl where
  infinitessimal x = abs x < 0.00000001

instance Epsilon Amp where
  infinitessimal x = realPart (abs x) < 0.00000001

instance Epsilon (Vect n Fl) where
  infinitessimal = all infinitessimal

instance Epsilon (Vect n Amp) where
  infinitessimal = all infinitessimal

instance Epsilon (Vect n (Vect m Fl)) where
  infinitessimal = all infinitessimal

instance Epsilon (Vect n (Vect m Amp)) where
  infinitessimal = all infinitessimal

sumSq : (Functor t, Foldable t, Neg a) => t a -> a
sumSq = sum . map ((\n => n*n) . abs)

data Real : Amp -> Type where
  IsReal : (z : Amp) -> {auto isinf : infinitessimal (imagPart z) = True} -> Real z

{-
*quantum> :r
Type checking ./math/Epsilon.idr
./math/Epsilon.idr:20:10:
Overlapping instance: Epsilon (Complex Double) already defined

approximates : Epsilon
-}

{-}
--instance (Neg a, Epsilon a) => Epsilon (Vect n a) where
--  infinitessimal = infinitessimal . sumSq

--data Infinitessimal : Type where
--  Infini : Epsilon a => (x : a) -> {auto isep : infinitessimal x = True} -> Infinitessimal x

-- data Unitary : (mat : Matrix n n (Complex Float)) -> Type where
--  IsUnitary : {prf : mat <> dagger )}
-}

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
||| An implementation of `Data.Heap` based on left-skewed binary trees.
|||
||| This implementation is a direct adaptation of Okasaki's `LeftistHeap`
||| found on pp.18-20 of his book without trying to lift anything at the
||| Type-level nor prove any properties. Its purpose is to be used as a
||| baseline for performance analysis and improvements in the "proven"
||| version found in `Data.Heap.LeftistHeap`.
module Data.Heap.RawBinaryHeap

import public Data.Heap

||| A implementation of a leftist binary tree which is not `Nat`-indexed
public export
data BinaryTree : (a : Type) -> Type where
  Empty : BinaryTree a
  Node : (elem : a) -> (rank : Int) -> (left : BinaryTree a) -> (right : BinaryTree a)
       -> BinaryTree a

rank : BinaryTree a -> Int
rank Empty = 0
rank (Node _ rk _ _) = rk

makeNode : (elem : a) -> BinaryTree a -> BinaryTree a -> BinaryTree a
makeNode elem left right =
  if rank left < rank right
  then Node elem (rank left + rank right) right left
  else Node elem (rank left + rank right) left right

mergeTree : (Ord a) => (left : BinaryTree a) -> (right : BinaryTree a) -> BinaryTree a
mergeTree Empty right = right
mergeTree left  Empty = left
mergeTree l@(Node elem rank left right) r@(Node elem' rank' left' right') =
  if (elem < elem')
  then  makeNode elem left (mergeTree right r)
  else  makeNode elem' left' (mergeTree l right')

findMin : BinaryTree a -> Maybe a
findMin Empty           = Nothing
findMin (Node elem _ _ _) = Just elem

popMin : (Ord a) => BinaryTree a -> (BinaryTree a, Maybe a)
popMin Empty  = (Empty, Nothing)
popMin (Node elem _ left right) = (mergeTree left right, Just elem)

insert : (Ord a) => a -> BinaryTree a -> BinaryTree a
insert x Empty = Node x 1 Empty Empty
insert x node  = mergeTree (Node x 1 Empty Empty) node

public export
data BinaryHeap : Type -> Type where

  ||| A Heap that keeps track of elements that's been inserted into
  ||| it.
  ||| For debugging and analysis purpose
  MkHeap : (tree : BinaryTree a) -> (inserts: Lazy (List a)) -> BinaryHeap a

traceInserts : BinaryHeap a -> List a
traceInserts (MkHeap tree inserts) = inserts

-- implementation of Heap
public export
Heap BinaryHeap where

  empty = MkHeap Empty []

  isEmpty (MkHeap Empty _) = True
  isEmpty _ = False

  push a (MkHeap tree ins) = MkHeap (insert a tree) (a :: ins)

  peek (MkHeap tree _ ) = findMin tree

  pop (MkHeap tree ins) = let (tree', a) = popMin tree
                         in (MkHeap tree' ins, a)

  merge (MkHeap tree ins) (MkHeap tree' ins') = MkHeap (mergeTree tree tree') (ins ++ ins')

  stats (MkHeap _ ins) = Just $ show ins

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Examples.Declassification.DatingSystem

import Pruviloj.Disjoint

import DepSec.Labeled
import DepSec.DIO
import DepSec.Declassification

import Examples.AuthorityLattice

%language ElabReflection

%default total

data Gender : Type where
 Unknown : Gender
 M : Gender
 F : Gender

implementation DecEq Gender where
  decEq Unknown Unknown = Yes Refl
  decEq Unknown M = No (%runElab disjoint)
  decEq Unknown F = No (%runElab disjoint)
  decEq M Unknown = No (%runElab disjoint)
  decEq M M = Yes Refl
  decEq M F = No (%runElab disjoint)
  decEq F Unknown = No (%runElab disjoint)
  decEq F M = No (%runElab disjoint)
  decEq F F = Yes Refl

record ProfileInfo (Owner : Principal) where
  constructor MkProfileInfo
  name      : Labeled Owner String
  gender    : Labeled Owner Gender
  birthdate : Labeled Owner String
  interests : Labeled Owner String
  city      : Labeled Owner String

DiscoveryResult : Principal -> Type
DiscoveryResult = ProfileInfo

Discoverer : Type
Discoverer = {bOwner : Principal}
          -> (b : ProfileInfo bOwner)
          -> DIO bOwner (Maybe (DiscoveryResult bOwner))

record Profile (Owner : Principal) where
  constructor MkProfile
  info       : ProfileInfo Owner
  discoverer : Discoverer

data GenProfile : (Principal : Type) -> Type where
  MkGenProfile : {t : Principal} -> Profile t -> GenProfile Principal

data Authority : a -> Type where
  ||| TCB
  MkAuthority : (t : a) -> Authority t

authorityHatch : { l, l' : Principal }
              -> (s ** (l = s, Authority s)) -> Labeled l a -> Labeled l' a
authorityHatch {l} = tokenHatch (\s => (l=s, Authority s))

--------------------------------------------------------------------------------
-- Convenience
--------------------------------------------------------------------------------
%hint
hint1 : {a : Principal} -> leq a a
hint1 {a} = reflexive a

implicit
genderToString : Gender -> String
genderToString M = "Male"
genderToString F = "Female"
genderToString Unknown = "Unknown"

implicit
profileToString : (p : DiscoveryResult viewer) -> DIO viewer String
profileToString (MkProfileInfo name gender birthdate likes location) =
   pure ("NAME: "      ++ !(unlabel name) ++ "\n" ++
         "BIRTHDATE: " ++ !(unlabel birthdate) ++ "\n" ++
         "LIKES: "     ++ !(unlabel likes) ++ "\n" ++
         "LOCATION: "  ++ !(unlabel location) ++ "\n")

implicit
toLabeled : Poset labelType => {l : labelType} -> String -> Labeled l String
toLabeled x = label x

implicit
toLabeledG : Poset labelType => {l : labelType} -> Gender -> Labeled l Gender
toLabeledG x = label x

--------------------------------------------------------------------------------
-- UTCB
--------------------------------------------------------------------------------
sampleDiscoverer : {A, B : Principal}
                -> Authority A
                -> (a : ProfileInfo A)
                -> (b : ProfileInfo B)
                -> DIO B (Maybe (DiscoveryResult B))
sampleDiscoverer {A} {B} auth a b =
  do bGender <- unlabel $ gender b
     aGender <- unlabel $ authorityHatch (A ** (Refl, auth)) (gender a)
     aName <- unlabel $ authorityHatch (A ** (Refl, auth)) (name a)
     case decEq bGender aGender of
       Yes prf => pure Nothing
       No contra =>
         let result : DiscoveryResult B = MkProfileInfo (label aName) (label Unknown) "" "" ""
         in pure $ Just result

--------------------------------------------------------------------------------
-- TCB
--------------------------------------------------------------------------------
profileBob : Profile Bob
profileBob =
  let profileInfo = MkProfileInfo "Bob" M "1994" "Nothing" "Aarhus"
  in MkProfile profileInfo (sampleDiscoverer (MkAuthority Bob) profileInfo)

profileAlice : Profile Alice
profileAlice =
  let profileInfo = MkProfileInfo "Alice" F "1993" "Hunting" "Aarhus"
  in MkProfile profileInfo (sampleDiscoverer (MkAuthority Alice) profileInfo)

profileChuck : Profile Chuck
profileChuck =
  let profileInfo = MkProfileInfo "Chuck" M "1992" "Swimming" "Ribe"
  in  MkProfile profileInfo (sampleDiscoverer (MkAuthority Chuck) profileInfo)

profileQueueAlice : List (GenProfile Principal)
profileQueueAlice = [MkGenProfile profileBob, MkGenProfile profileChuck]

printAlice : String -> DIO Alice ()
printAlice x = lift $ putStrLn x

runThroughQueueAlice : (acc : DIO Alice ()) -> List (GenProfile Principal) -> DIO Alice ()
runThroughQueueAlice acc [] = acc
runThroughQueueAlice acc ((MkGenProfile p) :: xs) =
  let thisProfilePrint : DIO Alice ()
    = do acc
         result <- (discoverer p) (info profileAlice)
         case result of
           Nothing => printAlice "Did not wanna be seen"
           Just result' => printAlice !result'
  in runThroughQueueAlice thisProfilePrint xs

main : IO ()
main =
  do putStrLn "########## Alice's queue is checked ##########\n"
     run $ runThroughQueueAlice (pure ()) profileQueueAlice
     putStrLn "########## Done checking ##########"
     pure ()

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
> module Main

> import Data.Fin
> import Data.Vect
> import Data.Matrix
> import Data.Matrix.Numeric

> import Fun.MathExpr
> import Double.Properties
> import Interfaces.Math

> %default total
> %access public export
> %auto_implicits off

* Preliminaries

This is a re-implementation of

  https://gist.github.com/mrkgnao/a45059869590d59f05100f4120595623

which, in turn, is an Idris implementation of

  https://blog.jle.im/entry/practical-dependent-types-in-haskell-1.html

* Layers

A layer of type |X| with |m| inputs and |n| outputs is a tuple
consisting of a function of type |X -> X|, a vector of |n| elements of
type |X| (the biases) and a |n| x |m| matrix of elements of type |X|
(the weights):

> Layer : (X : Type) -> (m : Nat) -> (n : Nat) -> Type
> Layer X m n = (MathExpr X, Vect n X, Matrix n m X)

* Sequential neural networks

A sequential neural network of type |X| with |m| inputs, |n| outputs and
a sequence of intermediate layers is a sequence of layers of type
|X|:

> infixr 5 :>:

> data Net : (X : Type) -> (m : Nat) -> List Nat -> (n : Nat) -> Type where
>   Id    : {X : Type} -> {m : Nat} ->
>           Net X m [] m
>   (:>:) : {X : Type} -> {m, m', n : Nat} -> {ms' : List Nat} ->
>           Layer X m m' -> Net X m' ms' n -> Net X m (m' :: ms') n

* Feed-forward

The idea is that, given a sequential neural network of type |X| with |m|
inputs and |n| outputs and a vector of |m| inputs of matching type, one
can compute a vector of |n| outputs. The computation is called
feed-forward.

> ff : {X : Type} -> {m, n : Nat} -> {ms : List Nat} ->
>      (Num X, Fractional X, Neg X, Math X) =>
>      Net X m ms n -> Vect m X -> Vect n X
> ff Id x         = id x
> ff ((s, b, w) :>: ls) x = ff ls (map (eval s) (b + (w </> x)))

* Error

Given a training pair |(x, y)|, the error is simply the difference
between |y| and the output of the network when fed with the input |x|:

> error : {X : Type} -> {n, m : Nat} -> {ms : List Nat} ->
>         (Num X, Fractional X, Neg X, Math X) =>
>         Net X m ms n -> Vect m X -> Vect n X -> Vect n X
> error net x y = y - (ff net x)

* Gradients

> nInputs : {X : Type} -> {m : Nat} -> {n : Nat} -> Layer X m n -> Nat
> nInputs {m} _ = m

> nOutputs : {X : Type} -> {m : Nat} -> {n : Nat} -> Layer X m n -> Nat
> nOutputs {n} _ = n

> nLayers : {X : Type} -> {m, n : Nat} -> {ms : List Nat} ->
>           Net X m ms n -> Nat
> nLayers Id         = Z
> nLayers (l :>: ls) = S (nLayers ls)

> dimOutputs : {X : Type} -> {m, n : Nat} -> {ms : List Nat} ->
>             Net X m ms n -> List Nat
> dimOutputs Id         = []
> dimOutputs (l :>: ls) = (nOutputs l) :: (dimOutputs ls)

> data ListVect : List Nat -> Type -> Type where
>   Nil  : {X : Type} ->
>          ListVect [] X
>   (::) : {m : Nat} -> {ms : List Nat} -> {X : Type} ->
>          Vect m X -> ListVect ms X -> ListVect (m :: ms) X

> gradZ : {X : Type} -> {m, m', n : Nat} -> {ms' : List Nat} ->
>         (Num X, Fractional X, Neg X, Math X) =>
>         (f   : Vect n X -> X) ->
>         (net : Net X m (m' :: ms') n) ->
>         ListVect (dimOutputs net) X

> {-

> -}

* Back propagation

> backPropagation : {X : Type} -> {m, m', n : Nat} -> {ms' : List Nat} ->
>                   (Num X, Fractional X, Neg X, Math X) =>
>                   (eta : X) ->
>                   (x   : Vect m X) ->
>                   (y   : Vect n X) ->
>                   Net X m (m' :: ms') n ->
>                   Net X m (m' :: ms')  n

> backPropagation {X} eta x y net = fst (go x y net)
>
>   where go : {m, m', n : Nat} -> {ms' : List Nat} ->
>              Vect m X ->
>              Vect n X ->
>              Net X m (m' :: ms') n -> (Net X m (m' :: ms') n, Vect m X)
>
>         go x y ((s, b, w) :>: Id) =
>           let z    = b + (w </> x)
>               x'   = map (eval s) z
>               dEdy = (map (eval (derivative s)) z) * (x' - y)
>               b'   = b - (eta <# dEdy)
>               w'   = w - (eta <#> (dEdy >< x))
>               dWs  = (transpose w) </> dEdy
>           in ((s, b', w') :>: Id, dWs)
>
>         go x y ((s, b, w) :>: l :>: ls) =
>           let z                  = b + (w </> x)
>               x'                 = map (eval s) z
>               (l' :>: ls', dWs') = go x' y (l :>: ls)
>               dEdy               = (map (eval (derivative s)) z) * dWs'
>               b'                 = b - (eta <# dEdy)
>               w'                 = w - (eta <#> (dEdy >< x))
>               dWs                = (transpose w) </> dEdy
>           in ((s, b', w') :>: l' :>: ls', dWs)

* Example

> s : MathExpr Double
> s = (Const 1) / (Const 1 + Exp . Neg)

> initial : Net Double 2 [2,2] 2
> initial = (s, [0.35, 0.35], [[0.15, 0.20], [0.25, 0.30]])
>           :>:
>           (s, [0.60, 0.60], [[0.40, 0.45], [0.50, 0.55]])
>           :>:
>           Id

> input : Vect 2 Double
> input = [0.05, 0.10]

> target : Vect 2 Double
> target = [0.01, 0.99]

> main : IO ()
> main = let step   = backPropagation 0.5 input target
>            errorF = \ net => error net input target
>            states = iterate step initial
>        in putStrLn . unlines $ map (show . errorF) (take 100 states)

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module FreeSelectiveDelivery

-- Based on https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf,
--          https://www.cs.ox.ac.uk/jeremy.gibbons/publications/delivery.pdf

interface Applicative f => Selective (f : Type -> Type) where
  select : f (Either a b) -> f (a -> b) -> f b

data Select : (Type -> Type) -> Type -> Type where
  Pure : a -> Select f a
  SelectC : Select f (Either a b) -> f (a -> b) -> Select f b

Functor f => Functor (Select f) where
  map f (Pure x) = Pure $ f x
  map f (SelectC fe ff) = SelectC (map (map f) fe) (map (f .) ff)

Functor f => Applicative (Select f) where
  pure x = Pure x

  (Pure f) <*> fa = map f fa
  (SelectC fe ff) <*> fa = SelectC (pure (\e, a => either (\x => Left (x, a)) (\f => Right (f a)) e) <*> fe <*> fa)
                                   (map uncurry ff)

Functor f => Selective (Select f) where
  select fe (Pure f) = map (either f id) fe
  select fe (SelectC fe' ff') = SelectC (select (map f fe) (map g fe')) (map uncurry ff')
    where
      f : {a, a', b : Type} -> Either a b -> Either a (Either (a', a) b)
      f e = map Right e
      g : {a, a', b : Type} -> Either a' (a -> b) -> a -> Either (a', a) b
      g e a = either (\a' => Left (a', a)) (\f => Right $ f a) e

runSelect : Selective g => ({x : Type} -> f x -> g x) -> Select f a -> g a
runSelect nat (Pure x) = pure x
runSelect nat (SelectC fe ff) = select (runSelect nat fe) (nat ff)

whenS : Selective f => f Bool -> f () -> f ()
whenS fb fu = select (selector fb) (effect fu)
  where
    selector : f Bool -> f (Either () ())
    selector fb = map (\x => if x then Left () else Right ()) fb
    effect : f () -> f (() -> ())
    effect fu = map const fu

Selective IO where
  select fb ff = fb >>= \e => case e of Left a => map (\f => f a) ff
                                        Right b => pure b

data Teletype : Type -> Type where
  GetLine : Teletype String
  PutStrLn : String -> Teletype ()

interface Serialize (f : Type -> Type) where
  serialize : f a -> (String, String)
interface Deserialize (f : Type -> Type) where
  deserialize : f a -> (String, String) -> Maybe (f a)

Serialize Teletype where
  serialize GetLine = ("GetLine", "")
  serialize (PutStrLn x) = ("PutStrLn", x)

Deserialize Teletype where
  deserialize GetLine ("GetLine", "") = Just $ GetLine
  deserialize (PutStrLn _) ("PutStrLn", s) = Just $ PutStrLn s
  deserialize _ _ = Nothing

data Action : (Type -> Type) -> Type -> Type where
  ActionC : f r -> (r -> a) -> Action f a

Functor (Action f) where
  map f (ActionC c k) = ActionC c (f . k)

Program : (Type -> Type) -> Type -> Type
Program f a = Select (Action f) a

serializeP : Serialize f => Program f a -> List (String, String)
serializeP (Pure _) = []
serializeP (SelectC fs (ActionC c _)) = serialize c :: serializeP fs

deserializeP : Deserialize f => Program f a -> List (String, String) -> Maybe (Program f a)
deserializeP (Pure x) [] = Just $ Pure x
deserializeP (SelectC ff (ActionC c k)) (s :: ss) with (deserialize c s)
  deserializeP (SelectC ff (ActionC c k)) (s :: ss) | Nothing = Nothing
  deserializeP (SelectC ff (ActionC c k)) (s :: ss) | (Just c') = deserializeP ff ss >>= (\ff' => pure $ SelectC ff' (ActionC c' k))
deserializeP _ _ = Nothing

effect : f r -> Program f r
effect c = SelectC (Pure (Left ())) (ActionC c const)

getLine : Program Teletype String
getLine = effect GetLine

putStrLn : String -> Program Teletype ()
putStrLn s = effect (PutStrLn s)

pingPongS : String -> Program Teletype ()
pingPongS s = whenS (map (== "ping") getLine) (putStrLn s)

toIO : Action Teletype a -> IO a
toIO (ActionC GetLine k) = getLine >>= (\x => pure $ k x)
toIO (ActionC (PutStrLn s) k) = putStrLn s >>= (\x => pure $ k x)

testIO : IO ()
testIO = runSelect toIO (pingPongS "pong")

testSerialize : List (String, String)
testSerialize = serializeP (pingPongS "ppong")

testDeserialize : IO ()
testDeserialize = case deserializeP (pingPongS "pong") testSerialize of
                      Nothing => pure ()
                      Just p => runSelect toIO p

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Optimisation.DeadCodeElimination

import Core.Context
import Data.List
import Data.SortedSet
import Data.SortedMap

import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import CairoCode.Traversal.Base
import CairoCode.Traversal.Defaults
import CairoCode.Traversal.Composition
import CairoCode.Traversal.ValueTracker
import Utils.Helpers
import Debug.Trace
import Utils.Lens

%hide Prelude.toList

-- Here starts the dead code detector
-- exported subset for reuse
export
registerTracker : (v:(InstVisit (SortedSet CairoReg))) -> Traversal (ScopedBindings (SortedSet CairoReg)) (ValBindType v (SortedSet CairoReg))
registerTracker = generalizeTrack initParam generalTrack implicitRegTracker
    where initParam : Maybe LinearImplicit -> CairoReg -> SortedSet CairoReg
          initParam _ reg = singleton reg
          implicitRegTracker : SortedMap LinearImplicit ((SortedSet CairoReg), CairoReg) -> Traversal (ScopedBindings (SortedSet CairoReg)) (SortedMap LinearImplicit (SortedSet CairoReg))
          implicitRegTracker impls = pure $ mapValueMap (\(val, reg) => insert reg val) impls
          generalTrack : (ret: List CairoReg) -> (params:List (SortedSet CairoReg)) -> Traversal (ScopedBindings (SortedSet CairoReg)) (List (SortedSet CairoReg))
          generalTrack rets args = do
            ctx <- getAllCaseBindings
            let requriedRegs = foldl union empty (ctx ++ args)
            pure $ map (\reg => insert reg requriedRegs) rets

-- the register collector
collectUsedRegisters : (Name, CairoDef) -> SortedSet CairoReg
collectUsedRegisters def = snd $ runVisitConcatCairoDef (traversal $ valueCollector idLens (dbgDef def) registerTracker returnCollector) def
    where dbgDef : (Name, CairoDef) -> CairoReg -> SortedSet CairoReg
          dbgDef (name, def) reg = trace "Register not bound in \{show name}: \{show reg}" (singleton reg)
          returnCollector : InstVisit  (SortedSet CairoReg) -> Traversal (ScopedBindings (SortedSet CairoReg)) (SortedSet CairoReg)
          returnCollector (VisitReturn res impls) = pure $ foldl union empty (res ++ (values impls))
          returnCollector _ = pure empty

-- Here starts the dead code marker

markUnusedRegisters : SortedSet CairoReg -> (Name, CairoDef) -> (Name, CairoDef)
markUnusedRegisters liveRegisters def = substituteDefRegisters marker def
    where marker : CairoReg -> Maybe CairoReg
          marker (Const c) = Nothing         -- We leave constant registers untouched
          marker (NamedParam n) = Nothing    -- We leave named registers untouched, they have a name for a reason
          marker reg = if contains reg liveRegisters
            then Nothing                -- We leave life registers untouched
            else (Just Eliminated)      -- The rest is eliminated

-- Here Starts the  dead code eliminator
isRegEliminated : CairoReg -> Bool
isRegEliminated Eliminated = True
isRegEliminated _ = False

isRegAssigEliminated : CairoReg -> Bool
isRegAssigEliminated (Const _) = True
isRegAssigEliminated rest = isRegEliminated rest

-- Here Starts the implicit preserver
substituteLinearImplicits : (Name, CairoDef) -> (Name, CairoDef)
substituteLinearImplicits def = substituteDefRegisters (\r => lookup r substitutions) def
    where discoverLinearImplicitSubstitutions : (rets:List CairoReg) -> SortedMap LinearImplicit (CairoReg, CairoReg) -> (params:List CairoReg) -> SortedMap CairoReg CairoReg
          discoverLinearImplicitSubstitutions res linImpls _ = if all isRegAssigEliminated res
            then fromList $ values linImpls
            else empty
          Semigroup CairoReg where (<+>) left _ = left
          substitutions : SortedMap CairoReg CairoReg
          substitutions = snd $ runVisitConcatCairoDef (pureTraversal $ generalize discoverLinearImplicitSubstitutions) def

-- Here All is put together as a compiler phase
eliminateAssignsDef : (Name, CairoDef) -> (Name, CairoDef)
eliminateAssignsDef def =  snd $ runVisitTransformCairoDef (fallbackTraversal (lift assigEliminatorSpecialCase) (ignoreControl $ instFallback $ lift $ generalize assigEliminatorGeneral), ()) def
    where assigEliminatorSpecialCase : InstVisit CairoReg -> Maybe (List (InstVisit CairoReg))
          assigEliminatorSpecialCase inst@(VisitReturn _ _) = Just [inst]
          assigEliminatorSpecialCase _ = Nothing
          assigEliminatorGeneral : (rets:List CairoReg) -> SortedMap LinearImplicit (CairoReg, CairoReg) -> (params:List CairoReg) -> Maybe (List (InstVisit CairoReg))
          assigEliminatorGeneral res _ _ = if all isRegAssigEliminated res then Just [] else Nothing

public export
eliminateDeadCode : (Name, CairoDef) -> (Name, CairoDef)
eliminateDeadCode def = orderUnassignedRegIndexes $ substituteLinearImplicits (eliminateAssignsDef (markUnusedRegisters lifeRegisters def))
    where lifeRegisters : SortedSet CairoReg
          lifeRegisters = collectUsedRegisters def

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Bar

main : IO ()
main = putStrLn "CouCou!"


text:
> module Unit.Properties

> import Data.Fin
> import Control.Isomorphism

> import Finite.Predicates
> import Sigma.Sigma
> import Pairs.Operations

> %default total

> %access public export

> ||| Mapping |Unit|s to |Fin|s
> toFin : Unit -> Fin (S Z)
> toFin MkUnit = FZ
> -- %freeze toFin

> ||| Mapping |Fin (S Z)|s to |Unit|s
> fromFin : Fin (S Z) -> Unit
> fromFin  FZ = MkUnit
> fromFin (FS k) = absurd k
> -- %freeze fromFin

> ||| |toFin| is the left-inverse of |fromFin|
> toFinFromFinLemma : (k : Fin (S Z)) -> toFin (fromFin k) = k
> toFinFromFinLemma FZ = Refl
> toFinFromFinLemma (FS k) = absurd k
> %freeze toFinFromFinLemma

> ||| |fromFin| is the left-inverse of |toFin|
> fromFinToFinLemma : (e : Unit) -> fromFin (toFin e) = e
> fromFinToFinLemma MkUnit = Refl
> %freeze fromFinToFinLemma

> ||| Unit is finite
> finiteUnit : Finite Unit
> finiteUnit = MkSigma (S Z) iso where
>   iso : Iso Unit (Fin (S Z))
>   iso = MkIso toFin fromFin toFinFromFinLemma fromFinToFinLemma

> ||| Unit is decidable
> decidableUnit : Dec Unit
> decidableUnit = Yes MkUnit

> {-

> ---}


text:
module Prelude.Interfaces

import Builtin
import Prelude.Basics
import Prelude.EqOrd
import Prelude.Num
import Prelude.Ops

%default total

-------------
-- ALGEBRA --
-------------

||| Sets equipped with a single binary operation that is associative.  Must
||| satisfy the following laws:
|||
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
public export
interface Semigroup ty where
  constructor MkSemigroup
  (<+>) : ty -> ty -> ty

||| Sets equipped with a single binary operation that is associative, along with
||| a neutral element for that binary operation.  Must satisfy the following
||| laws:
|||
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Neutral for `<+>`:
|||     forall a, a <+> neutral == a
|||     forall a, neutral <+> a == a
public export
interface Semigroup ty => Monoid ty where
  constructor MkMonoid
  neutral : ty

public export
Semigroup () where
  _ <+> _ = ()

public export
Monoid () where
  neutral = ()

public export
Semigroup a => Semigroup b => Semigroup (a, b) where
  (x, y) <+> (v, w) = (x <+> v, y <+> w)

public export
Monoid a => Monoid b => Monoid (a, b) where
  neutral = (neutral, neutral)

public export
Semigroup Ordering where
  LT <+> _ = LT
  GT <+> _ = GT
  EQ <+> o =  o

public export
Monoid Ordering where
  neutral = EQ

public export
Semigroup b => Semigroup (a -> b) where
  (f <+> g) x = f x <+> g x

public export
Monoid b => Monoid (a -> b) where
  neutral _ = neutral

---------------------------------------------------------
-- FUNCTOR, BIFUNCTOR, APPLICATIVE, ALTERNATIVE, MONAD --
---------------------------------------------------------

||| Functors allow a uniform action over a parameterised type.
||| @ f a parameterised type
public export
interface Functor f where
  constructor MkFunctor
  ||| Apply a function across everything of type 'a' in a parameterised type
  ||| @ f the parameterised type
  ||| @ func the function to apply
  map : (func : a -> b) -> f a -> f b

||| An infix alias for `map`, applying a function across everything of type 'a'
||| in a parameterised type.
||| @ f the parameterised type
||| @ func the function to apply
public export
(<$>) : Functor f => (func : a -> b) -> f a -> f b
(<$>) func x = map func x

||| Flipped version of `<$>`, an infix alias for `map`, applying a function across
||| everything of type 'a' in a parameterised type.
||| @ f the parameterised type
||| @ func the function to apply
public export
(<&>) : Functor f => f a -> (func : a -> b) -> f b
(<&>) x func = map func x

||| Run something for effects, replacing the return value with a given parameter.
public export
(<$) : Functor f => b -> f a -> f b
(<$) b = map (const b)

||| Flipped version of `<$`.
public export
($>) : Functor f => f a -> b -> f b
($>) fa b = map (const b) fa

||| Run something for effects, throwing away the return value.
%inline
public export
ignore : Functor f => f a -> f ()
ignore = map (const ())

namespace Functor
  ||| Composition of functors is a functor.
  public export
  [Compose] (Functor f, Functor g) => Functor (f . g) where
    map = map . map

||| Bifunctors
||| @f The action of the Bifunctor on pairs of objects
public export
interface Bifunctor f where
  constructor MkBifunctor
  ||| The action of the Bifunctor on pairs of morphisms
  |||
  ||| ````idris example
  ||| bimap (\x => x + 1) reverse (1, "hello") == (2, "olleh")
  ||| ````
  |||
  bimap : (a -> c) -> (b -> d) -> f a b -> f c d
  bimap f g = mapFst f . mapSnd g

  ||| The action of the Bifunctor on morphisms pertaining to the first object
  |||
  ||| ````idris example
  ||| mapFst (\x => x + 1) (1, "hello") == (2, "hello")
  ||| ````
  |||
  mapFst : (a -> c) -> f a b -> f c b
  mapFst f = bimap f id

  ||| The action of the Bifunctor on morphisms pertaining to the second object
  |||
  ||| ````idris example
  ||| mapSnd reverse (1, "hello") == (1, "olleh")
  ||| ````
  |||
  mapSnd : (b -> d) -> f a b -> f a d
  mapSnd = bimap id

public export
mapHom : Bifunctor f => (a -> b) -> f a a -> f b b
mapHom f = bimap f f

public export
interface Functor f => Applicative f where
  constructor MkApplicative
  pure : a -> f a
  (<*>) : f (a -> b) -> f a -> f b

public export
(<*) : Applicative f => f a -> f b -> f a
a <* b = map const a <*> b

public export
(*>) : Applicative f => f a -> f b -> f b
a *> b = map (const id) a <*> b

%allow_overloads pure
%allow_overloads (<*)
%allow_overloads (*>)

namespace Applicative
  ||| Composition of applicative functors is an applicative functor.
  public export
  [Compose] (Applicative f, Applicative g) => Applicative (f . g)
    using Functor.Compose where
      pure = pure . pure
      fun <*> x = [| fun <*> x |]

public export
interface Applicative f => Alternative f where
  constructor MkAlternative
  empty : f a
  (<|>) : f a -> Lazy (f a) -> f a

public export
interface Applicative m => Monad m where
  constructor MkMonad
  ||| Also called `bind`.
  (>>=) : m a -> (a -> m b) -> m b

  ||| Also called `flatten` or mu.
  join : m (m a) -> m a

  -- default implementations
  (>>=) x f = join (f <$> x)
  join x = x >>= id

%allow_overloads (>>=)

||| Right-to-left monadic bind, flipped version of `>>=`.
public export
(=<<) : Monad m => (a -> m b) -> m a -> m b
(=<<) = flip (>>=)

||| Sequencing of effectful composition
public export
(>>) : Monad m => m () -> Lazy (m b) -> m b
a >> b = a >>= \_ => b

||| Left-to-right Kleisli composition of monads.
public export
(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
(>=>) f g = \x => f x >>= g

||| Right-to-left Kleisli composition of monads, flipped version of `>=>`.
public export
(<=<) : Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
(<=<) = flip (>=>)

||| `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False`.
public export
guard : Alternative f => Bool -> f ()
guard x = if x then pure () else empty

||| Conditionally execute an applicative expression when the boolean is true.
public export
when : Applicative f => Bool -> Lazy (f ()) -> f ()
when True f = f
when False f = pure ()

||| Execute an applicative expression unless the boolean is true.
%inline public export
unless : Applicative f => Bool -> Lazy (f ()) -> f ()
unless = when . not

---------------------------
-- FOLDABLE, TRAVERSABLE --
---------------------------

||| The `Foldable` interface describes how you can iterate over the elements in
||| a parameterised type and combine the elements together, using a provided
||| function, into a single result.
||| @ t The type of the 'Foldable' parameterised type.
public export
interface Foldable t where
  constructor MkFoldable
  ||| Successively combine the elements in a parameterised type using the
  ||| provided function, starting with the element that is in the final position
  ||| i.e. the right-most position.
  ||| @ func  The function used to 'fold' an element into the accumulated result
  ||| @ init  The starting value the results are being combined into
  ||| @ input The parameterised type
  foldr : (func : elem -> acc -> acc) -> (init : acc) -> (input : t elem) -> acc

  ||| The same as `foldr` but begins the folding from the element at the initial
  ||| position in the data structure i.e. the left-most position.
  ||| @ func  The function used to 'fold' an element into the accumulated result
  ||| @ init  The starting value the results are being combined into
  ||| @ input The parameterised type
  foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc
  foldl f z t = foldr (flip (.) . flip f) id t z

  ||| Test whether the structure is empty.
  ||| @ acc The accumulator value which is specified to be lazy
  null : t elem -> Lazy Bool
  null = foldr {acc = Lazy Bool} (\ _,_ => False) True

  ||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
  ||| Consequently, the final value is wrapped in the same `Monad`.
  foldlM : Monad m => (funcM : acc -> elem -> m acc) -> (init : acc) -> (input : t elem) -> m acc
  foldlM fm a0 = foldl (\ma, b => ma >>= flip fm b) (pure a0)

  ||| Produce a list of the elements contained in the parametrised type.
  toList : t elem -> List elem
  toList = foldr (::) []

  ||| Maps each element to a value and combine them.
  ||| For performance reasons, this should wherever
  ||| be implemented with tail recursion.
  ||| @ f The function to apply to each element.
  foldMap : Monoid m => (f : a -> m) -> t a -> m
  foldMap f = foldr ((<+>) . f) neutral

||| Combine each element of a structure into a monoid.
public export
concat : (Foldable t, Monoid a) => t a -> a
concat = foldMap id

||| Combine into a monoid the collective results of applying a function to each
||| element of a structure.
public export
concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m
concatMap = foldMap

namespace Bool.Lazy
  namespace Semigroup
    public export
    [Any] Semigroup (Lazy Bool) where
      x <+> y = force x || y

    public export
    [All] Semigroup (Lazy Bool) where
      x <+> y = force x && y

  namespace Monoid
    public export
    [Any] Monoid (Lazy Bool) using Semigroup.Any where
      neutral = delay False

    public export
    [All] Monoid (Lazy Bool) using Semigroup.All where
      neutral = delay True

||| The conjunction of all elements of a structure containing lazy boolean
||| values.  `and` short-circuits from left to right, evaluating until either an
||| element is `False` or no elements remain.
public export
and : Foldable t => t (Lazy Bool) -> Bool
and = force . concat @{(%search, All)}

||| The disjunction of all elements of a structure containing lazy boolean
||| values.  `or` short-circuits from left to right, evaluating either until an
||| element is `True` or no elements remain.
public export
or : Foldable t => t (Lazy Bool) -> Bool
or = force . concat @{(%search, Any)}

namespace Bool
  namespace Semigroup
    public export
    [Any] Semigroup Bool where
      x <+> y = x || delay y

    public export
    [All] Semigroup Bool where
      x <+> y = x && delay y

  namespace Monoid
    public export
    [Any] Monoid Bool using Bool.Semigroup.Any where
      neutral = False

    public export
    [All] Monoid Bool using Bool.Semigroup.All where
      neutral = True

||| The disjunction of the collective results of applying a predicate to all
||| elements of a structure.  `any` short-circuits from left to right.
public export
any : Foldable t => (a -> Bool) -> t a -> Bool
any = foldMap @{%search} @{Any}

||| The disjunction of the collective results of applying a predicate to all
||| elements of a structure.  `all` short-circuits from left to right.
public export
all : Foldable t => (a -> Bool) -> t a -> Bool
all = foldMap @{%search} @{All}
  where
    monoid : Monoid Bool
    monoid = MkMonoid @{MkSemigroup (\x, y => x && y)} True

namespace Num
  namespace Semigroup
    public export
    [Additive] Num a => Semigroup a where
      (<+>) = (+)

    public export
    [Multiplicative] Num a => Semigroup a where
      (<+>) = (*)

  namespace Monoid
    public export
    [Additive] Num a => Monoid a using Semigroup.Additive where
      neutral = 0

    public export
    [Multiplicative] Num a => Monoid a using Semigroup.Multiplicative where
      neutral = 1

||| Add together all the elements of a structure.
public export
sum : (Foldable t, Num a) => t a -> a
sum = concat @{(%search, Additive)}

||| Add together all the elements of a structure.
||| Same as `sum` but tail recursive.
export
sum' : (Foldable t, Num a) => t a -> a
sum' = sum

||| Multiply together all elements of a structure.
public export
product : (Foldable t, Num a) => t a -> a
product = concat @{(%search, Multiplicative)}

||| Multiply together all elements of a structure.
||| Same as `product` but tail recursive.
export
product' : (Foldable t, Num a) => t a -> a
product' = product

||| Map each element of a structure to a computation, evaluate those
||| computations and discard the results.
public export
traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
traverse_ f = foldr ((*>) . f) (pure ())

||| Evaluate each computation in a structure and discard the results.
public export
sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
sequence_ = foldr (*>) (pure ())

||| Like `traverse_` but with the arguments flipped.
public export
for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
for_ = flip traverse_

namespace Lazy
  public export
  [SemigroupAlternative] Alternative f => Semigroup (Lazy (f a)) where
    x <+> y = force x <|> y

  public export
  [MonoidAlternative] Alternative f => Monoid (Lazy (f a)) using Lazy.SemigroupAlternative where
    neutral = delay empty

public export
[SemigroupAlternative] Alternative f => Semigroup (f a) where
  x <+> y = x <|> delay y

public export
[MonoidAlternative] Alternative f => Monoid (f a) using Interfaces.SemigroupAlternative where
  neutral = empty

||| Fold using Alternative.
|||
||| If you have a left-biased alternative operator `<|>`, then `choice` performs
||| left-biased choice from a list of alternatives, which means that it
||| evaluates to the left-most non-`empty` alternative.
|||
||| If the list is empty, or all values in it are `empty`, then it evaluates to
||| `empty`.
|||
||| Example:
|||
||| ```
||| -- given a parser expression like:
||| expr = literal <|> keyword <|> funcall
|||
||| -- choice lets you write this as:
||| expr = choice [literal, keyword, funcall]
||| ```
|||
||| Note: In Haskell, `choice` is called `asum`.
public export
choice : (Foldable t, Alternative f) => t (Lazy (f a)) -> f a
choice = force . concat @{(%search, Lazy.MonoidAlternative)}

||| A fused version of `choice` and `map`.
public export
choiceMap : (Foldable t, Alternative f) => (a -> f b) -> t a -> f b
choiceMap = foldMap @{%search} @{MonoidAlternative}

namespace Foldable
  ||| Composition of foldables is foldable.
  public export
  [Compose] (Foldable t, Foldable f) => Foldable (t . f) where
    foldr = foldr . flip . foldr
    foldl = foldl . foldl
    null tf = null tf || all (force . null) tf
    foldMap = foldMap . foldMap

||| `Bifoldable` identifies foldable structures with two different varieties
||| of elements (as opposed to `Foldable`, which has one variety of element).
||| Common examples are `Either` and `Pair`.
public export
interface Bifoldable p where
  constructor MkBifoldable
  bifoldr : (a -> acc -> acc) -> (b -> acc -> acc) -> acc -> p a b -> acc

  bifoldl : (acc -> a -> acc) -> (acc -> b -> acc) -> acc -> p a b -> acc
  bifoldl f g z t = bifoldr (flip (.) . flip f) (flip (.) . flip g) id t z

  binull : p a b -> Lazy Bool
  binull = bifoldr {acc = Lazy Bool} (\ _,_ => False) (\ _,_ => False) True

public export
interface (Functor t, Foldable t) => Traversable t where
  constructor MkTraversable
  ||| Map each element of a structure to a computation, evaluate those
  ||| computations and combine the results.
  traverse : Applicative f => (a -> f b) -> t a -> f (t b)

||| Evaluate each computation in a structure and collect the results.
public export
sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
sequence = traverse id

||| Like `traverse` but with the arguments flipped.
public export
for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
for = flip traverse

public export
interface (Bifunctor p, Bifoldable p) => Bitraversable p where
  constructor MkBitraversable
  ||| Map each element of a structure to a computation, evaluate those
  ||| computations and combine the results.
  bitraverse : Applicative f => (a -> f c) -> (b -> f d) -> p a b -> f (p c d)

||| Evaluate each computation in a structure and collect the results.
public export
bisequence : (Bitraversable p, Applicative f) => p (f a) (f b) -> f (p a b)
bisequence = bitraverse id id

||| Like `bitraverse` but with the arguments flipped.
public export
bifor :  (Bitraversable p, Applicative f)
      => p a b
      -> (a -> f c)
      -> (b -> f d)
      -> f (p c d)
bifor t f g = bitraverse f g t

namespace Traversable
  ||| Composition of traversables is traversable.
  public export
  [Compose] (Traversable t, Traversable f) => Traversable (t . f)
    using Foldable.Compose Functor.Compose where
      traverse = traverse . traverse

namespace Monad
  ||| Composition of a traversable monad and a monad is a monad.
  public export
  [Compose] (Monad m, Monad t, Traversable t) => Monad (m . t)
    using Applicative.Compose where
      a >>= f = a >>= map join . traverse f


text:
module Tools.FullList

%access public export

data FullList a = End a | Cons a (FullList a)

(++) : FullList a -> FullList a -> FullList a
(End x)     ++ tl' = Cons x tl'
(Cons x tl) ++ tl' = Cons x $ tl ++ tl'

Functor FullList where
  map f (End x)     = End $ f x
  map f (Cons x tl) = Cons (f x) $ map f tl

Foldable FullList where
  foldl func init (End x)     = func init x
  foldl func init (Cons x tl) = func (foldl func init tl) x
  foldr func init (End x)     = func x init
  foldr func init (Cons x tl) = func x $ foldr func init tl

Applicative FullList where
  pure x = End x
  (End f)     <*> lst = map f lst
  (Cons f tl) <*> lst = map f lst ++ (tl <*> lst)