text:
module Data.Config

import Data.Either
import Data.List
import Data.String
import Data.Vect
import Language.JSON
import Language.JSON.Accessors

%default total

||| Unix Timestamp (seconds since epoch).
public export
Timestamp : Type
Timestamp = Bits32

public export
record Ephemeral where
  constructor MkEphem
  ||| The file path where the current configuration should be
  ||| persisted.
  filepath : String
  ||| True to use ANSI terminal colors.
  colors   : Bool

public export
record Config where
  constructor MkConfig
  ||| Timestamp when the config was last syncronized with GitHub.
  updatedAt   : Timestamp
  org         : String
  repo        : String
  ||| The main branch. New PRs are based off of this branch.
  mainBranch  : String
  ||| True to assign teams as well as individual users to PRs.
  assignTeams : Bool
  ||| True to comment on PRs after assigning users.
  commentOnAssign : Bool
  ||| Local cache of GitHub teams within the configured org.
  teamSlugs   : List String
  ||| Local cache of GitHub members within the configured org.
  orgMembers  : List String
  ||| Configuration properties that are not written to a file.
  ephemeral   : Ephemeral -- not written out to file

%name Config config

public export
settableProps : List String
settableProps = [
    "assignTeams"
  , "commentOnAssign"
  ]

export
(.filepath) : Config -> String
config.filepath = config.ephemeral.filepath

export
(.colors) : Config -> Bool
config.colors = config.ephemeral.colors

export
Show Config where
  show config = unlines [
      "      updatedAt: \{show config.updatedAt}"
    , "            org: \{show config.org}"
    , "           repo: \{show config.repo}"
    , "     mainBranch: \{show config.mainBranch}"
    , "    assignTeams: \{show config.assignTeams}"
    , "commentOnAssign: \{show config.commentOnAssign}"
    , "      teamSlugs: \{show config.teamSlugs}"
    , "     orgMembers: \{show config.orgMembers}"
    ]

export
json : Config -> JSON
json (MkConfig updatedAt org repo mainBranch assignTeams commentOnAssign teamSlugs orgMembers _) =
  JObject [
      ("mainBranch"     , JString mainBranch)
    , ("assignTeams"    , JBoolean assignTeams)
    , ("commentOnAssign", JBoolean commentOnAssign)
    , ("org"            , JString org)
    , ("orgMembers"     , JArray $ JString <$> sort orgMembers)
    , ("repo"           , JString repo)
    , ("teamSlugs"      , JArray $ JString <$> sort teamSlugs)
    , ("updatedAt"      , JNumber $ cast updatedAt)
    ]

export
parseConfig : (ephemeral : Ephemeral) -> (filecontents : String) -> Either String Config
parseConfig ephemeral = (maybeToEither "Failed to parse JSON" . JSON.parse) >=> parseConfigJson
  where
    parseConfigJson : JSON -> Either String Config
    parseConfigJson (JObject config) = do [   updatedAt
                                            , org
                                            , repo
                                            , mainBranch
                                            , assignTeams
                                            , commentOnAssign
                                            , teamSlugs
                                            , orgMembers
                                            ] <-
                                            lookupAll [
                                                "updatedAt"
                                              , "org"
                                              , "repo"
                                              , "mainBranch"
                                              , "assignTeams"
                                              , "commentOnAssign"
                                              , "teamSlugs"
                                              , "orgMembers"
                                              ] config
                                          ua <- cast <$> integer updatedAt
                                          o  <- string org
                                          r  <- string repo
                                          mb <- string mainBranch
                                          at <- bool assignTeams
                                          ca <- bool commentOnAssign
                                          ts <- array string teamSlugs
                                          om <- array string orgMembers
                                          pure $ MkConfig {
                                              updatedAt        = ua
                                            , org              = o
                                            , repo             = r
                                            , mainBranch       = mb
                                            , assignTeams      = at
                                            , teamSlugs        = ts
                                            , commentOnAssign  = ca
                                            , orgMembers       = om
                                            , ephemeral        = ephemeral
                                            }
    parseConfigJson (JArray _) = Left "Expected config JSON to be an Object, not an array."
    parseConfigJson _          = Left "Expected config JSON to be an Object."

export
filename : String
filename = "harmony.json"

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
module Text.CSS.Percentage

import Language.Reflection.Refined
import public Language.Reflection.Refined.Util
import Text.CSS.Render

%language ElabReflection
%default total

||| A floating point percentage value in the the
||| range [0,100].
public export
record Percentage where
  constructor MkPercentage
  value : Double
  0 prf : So (0 <= value && value <= 100)

%runElab refinedDouble "Percentage"

export
fromInteger :  (n : Integer)
            -> {auto 0 _ : IsJust (Percentage.refine (cast n))}
            -> Percentage
fromInteger n = fromJust $ Percentage.refine (cast n)

export
Render Percentage where
  render (MkPercentage v _) = show v ++ "%"

||| Convenience function for creating percentages with little
||| syntactic overhead.
|||
||| ```idris example
||| perc 12
||| ```
export %inline
perc :  Cast Percentage a
     => (v : Double)
     -> {auto 0 prf : So (0 <= v && v <= 100)}
     -> a
perc v = cast $ MkPercentage v prf

ext: idr


text:
module Main

%language UniquenessTypes

{-
 - IO monad
 -}
whatIsYourName : IO ()
whatIsYourName = do
  putStrLn "What is your name?"
  name <- getLine
  putStrLn ("Hello " ++ name)

{-
 - The World
 -}
data Wrld = TheWrld

printStr : String -> Wrld -> Wrld
printStr str world = ?printStr_rhs

readStr : Wrld -> (String, Wrld)
readStr world = ?readStr_rhs

whatIsYourPureName : Wrld -> Wrld
whatIsYourPureName w1 = w4
  where
    w2 : Wrld
    w2 = printStr "What is your name?" w1

    stringWorld : (String, Wrld)
    stringWorld = readStr w2

    w4 : Wrld
    w4 = printStr ("Hello " ++ (fst stringWorld)) (snd stringWorld)

{-
 - Branching the world
 -}
branch : Wrld -> (Wrld, Wrld)
branch w = (printStr "I love you!" w,
            printStr "I hate you!" w)

{-
 - Uniqueness types
 -}
data UWrld : Wrld -> UniqueType where
   MkUWrld : UWrld w

-- printStrU : String -> UWrld TheWrld -> UWrld TheWrld
-- printStrU str world = ?printStrU_rhs
--
-- readStrU : UWrld TheWrld -> (String, (UWrld TheWrld))
-- readStrU world = ?readStrU_rhs
--
-- branchU : UWrld TheWrld -> UWrld TheWrld
-- branchU x = ?branchU_rhs

{-
 - Hiding the world
 -}
WrldT : (a : Type) -> Type
WrldT x = Wrld -> (x, Wrld)

readStrT : WrldT String
readStrT = readStr

printStrT : String -> WrldT ()
printStrT s w = ((), printStr s w)

{-
 - Currying and uncurrying
 -}
f : Integer -> Integer -> Integer
f x y = x + y

g : Integer -> (Integer -> Integer)
g x = \y => x + y

uncurry' : (Integer -> Integer -> Integer) -> ((Integer, Integer) -> Integer)
uncurry' f = \(a,b) => f a b

{-
 - Composing transformers
 -}
infixl 1 >>>=
(>>>=) : WrldT a          -- Wrld -> (a, Wrld)
      -> (a -> WrldT b)   -- (a -> Wrld -> (b, Wrld))
      -> WrldT b          -- Wrld -> (b, Wrld)
wt >>>= f = uncurry f . wt

whatIsYourPureNameT : WrldT ()
whatIsYourPureNameT =
  printStrT "What is your name?" >>>= \_ =>
  readStrT                       >>>= \name =>
  printStrT ("Hello " ++ name)

{-
 - `do` notation
 -}
data WrldM : (a : Type) -> Type where
  MkWrldM : (asT : WrldT a) -> WrldM a

myWrldM : WrldM String
myWrldM = MkWrldM (\w => ("hello", w))

data ListOf : a -> Type where
  MkListOf : (list : List a) -> ListOf a

myStrLst : ListOf String
myStrLst = MkListOf ["hello"]

Functor WrldM where
  -- map : (func : a -> b) -> f a -> f b
  map f (MkWrldM asT) = MkWrldM $ (\(a, w) => (f a, w)) . asT

Applicative WrldM where
  -- pure : a -> f a
  pure x = MkWrldM (\w => (x, w))

  -- (<*>) : f (a -> b) -> f a -> f b
  (MkWrldM wtf) <*> (MkWrldM wt) = MkWrldM (wtf >>>= \f =>
                                            wt  >>>= \x =>
                                            \w    => (f x, w))
      -- MkWrldM ( \ w =>
      --   let (f,w1) = wtf w
      --       (a,w2) = wt w1
      --   in  (f a, w2)
      -- )

Monad WrldM where
  -- (>>=) : m a -> (a -> m b) -> m b
  -- wt >>= f = WorldM (asT wt >>>= asT . f)
  (MkWrldM wt) >>= f = MkWrldM ( \ w =>
      let (x,w1) = wt w
          MkWrldM foo = f x
          (y,b) = foo w1
      in  (y,b)
    )

printStrM : String -> WrldM ()
printStrM = MkWrldM . printStrT

readStrM : WrldM String
readStrM = MkWrldM readStrT

whatIsYourPureNameM : WrldM ()
whatIsYourPureNameM = do
  printStrM "What is your name?"
  name <- readStrM
  printStrM ("Hello " ++ name)

-- asT whatIsYourPureNameM World

{-
import System.IO.Unsafe

data World = World deriving Show

printStr :: String -> World -> World
printStr s !w = unsafePerformIO (putStrLn s >> return w)

readStr :: World -> (String, World)
readStr !w = unsafePerformIO (getLine >>= (\s -> return (s, w)))
-}


text:
module Language.SystemVerilog.Gates

%default total

public export
data TyGateComb = AND | IOR | XOR

export
toString : TyGateComb -> String
toString AND = "and"
toString IOR = "ior"
toString XOR = "xor"

export
Show TyGateComb where
  show = toString

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
-- Namespaces are currently allowed to be empty, as modules are, but also
-- require their contents to be indented to denote where they end.
-- Whereas a module's end is the end of the file.

-- Since there's no indentation on the latter definitions, this file should have
-- Test in scope under Main.X.Test, Test in scope under Main.Test, and nothing
-- in scope in Main.Y because namespace Y ends immediately.

namespace X
  private
  data Test = A | B

namespace Y
private
data Test = A | B


text:
showIfEq : (Eq a, Show a) => a -> a -> String
showIfEq x y = if x == y then show x else "Nope"

topeq : Eq a => a -> a -> Bool
topeq x y = x == y

data Foo = MkFoo | MkBar

-- Should only show the first interface search failure in the tuple
-- (Ideally it would keep going and find all the failures, but that is
-- hard to achieve and this way is better than displaying the whole
-- top level search when only part of it is relevant)

test : Int -> String
test x = showIfEq MkFoo MkBar

Eq Foo where
  MkFoo == MkFoo = True
  MkBar == MkBar = True
  _ == _ = False

test2 : String
test2 = showIfEq MkFoo MkBar


text:
module Main

import Data.Fin

%builtin Natural Nat
%builtin Natural Fin

%builtin NaturalToInteger Data.Fin.finToInteger

main : IO ()
main = putStrLn $ show $ finToInteger $ FS $ FZ {k=34}


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

import public WebAssembly.Structure.Instructions.Definition
import public WebAssembly.Structure.Instructions.DecEq
import public WebAssembly.Structure.Instructions.Control
import public WebAssembly.Structure.Instructions.Memory

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A command line argument parser
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Options.Applicative.Chunk

import public Text.PrettyPrint.Leijen

%default total
%access public export

data Chunk a = MkChunk (Maybe a)

unChunk : Chunk a -> Maybe a
unChunk (MkChunk a) = a

Functor Chunk where
  map f (MkChunk x) = MkChunk $ map f x

Applicative Chunk where
  pure = MkChunk . pure
  (MkChunk f) <*> (MkChunk x) = MkChunk (f <*> x)

Monad Chunk where
  (MkChunk m) >>= f = MkChunk $ m >>= unChunk . f

chunked : (a -> a -> a)
        -> Chunk a -> Chunk a -> Chunk a
chunked _ (MkChunk Nothing) y = y
chunked _ x (MkChunk Nothing) = x
chunked f (MkChunk (Just x)) (MkChunk (Just y)) = MkChunk (Just (f x y))

extractChunk : Monoid a => Chunk a -> a
extractChunk (MkChunk x) = fromMaybe neutral x

(<+>) : Chunk Doc -> Chunk Doc -> Chunk Doc
(<+>) = chunked (|++|)

isEmptyChunk : Chunk a -> Bool
isEmptyChunk (MkChunk Nothing)  = True
isEmptyChunk (MkChunk (Just _)) = False

tabulate' : Int -> List (Doc, Doc) -> Chunk Doc
tabulate' _ [] = MkChunk Nothing
tabulate' size table = pure $ vcat
  [ indent 2 (fillBreak size key |+| value)
  | (key, value) <- table ]

-- | Display pairs of strings in a table.
tabulate : List (Doc, Doc) -> Chunk Doc
tabulate = tabulate' 24

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


text:
||| Additional utilites for solving and deriving
||| (in)equalities in `Integer` arithmetics.
module Data.Prim.Integer.Extra

import public Data.Prim.Integer
import Syntax.PreorderReasoning

%default total

infixl 0  <>
prefix 1  |>
infix  1  ..., ..=, =.., =.=
infix  1  ~.., ..~, ~.~

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

||| Allows us to commute addition on both sides of an inequality.
export
0 pairPlusCommutative :  {w,x,y,z : Integer}
                      -> (w + x === x + w, y + z === z + y)
pairPlusCommutative = (plusCommutative, plusCommutative)

||| Allows us to commute multiplication on both sides of an inequality.
export
0 pairMultCommutative :  {w,x,y,z : Integer}
                      -> (w * x === x * w, y * z === z * y)
pairMultCommutative = (multCommutative, multCommutative)

--------------------------------------------------------------------------------
--          Syntax for deriving (in)equalities
--------------------------------------------------------------------------------

||| Type describing a relation between two integers.
|||
||| This is used to solve integer (in)equalities with
||| a syntax that is similar to the one used for preorder
||| reasoning.
public export
data Rel :  (rel : Integer -> Integer -> Type)
         -> (x,y : Integer)
         -> Type where
  (<)   : (x,y : Integer) -> Rel (<)   x y
  (<=)  : (x,y : Integer) -> Rel (<=)  x y
  (===) : (x,y : Integer) -> Rel (===) x y
  (>=)  : (x,y : Integer) -> Rel (>=)  x y
  (>)   : (x,y : Integer) -> Rel (>)   x y

public export
0 rel : Rel r x y -> (u,v : Integer) -> Rel r u v
rel (_ < _)   u v = u < v
rel (_ <= _)  u v = u <= v
rel (_ === _) u v = u === v
rel (_ >= _)  u v = u >= v
rel (_ > _)   u v = u > v

||| Reversed function application.
export
App : a -> (a -> b) -> b
App x f = f x

||| The identity function for relations.
export
0 (|>) : Rel r x y -> r x y -> r x y
(|>) _ v = v

||| Reversed function composition.
export
0 (<>) : (a -> b) -> (b -> c) -> a -> c
(<>) f g = g . f

||| Thought bubble similar to the one used in
||| `Syntax.PreorderReasoning`.
export
0 (...) : Rel r x y -> (Rel r x y -> a -> r x y) -> a -> r x y
(...) r f = f r

||| Replace the right hand side of an (in)equality.
export
0 (..=) : Rel r x z -> (y === z) -> r x y -> r x z
(..=) _ prf v = replace {p = r x} prf v

||| Replace the right hand side of an (in)equality.
export
0 (..~) : Rel r x z -> (z === y) -> r x y -> r x z
(..~) r prf = r ..= sym prf

||| Replace the left hand side of an (in)equality.
export
0 (=..) : Rel r x z -> (y === x) -> r y z -> r x z
(=..) _ prf v = replace {p = \a => r a z} prf v

||| Replace the left hand side of an (in)equality.
export
0 (~..) : Rel r x z -> (x === y) -> r y z -> r x z
(~..) r prf = r =.. sym prf

||| Replace both sides of an (in)equality.
export
0 (=.=) : Rel r w z -> (x === w, y === z) -> r x y -> r w z
(=.=) _ (p1,p2) v = replace {p = r w} p2
                  $ replace {p = \a => r a y} p1 v

||| Replace both sides of an (in)equality.
export
0 (~.~) : Rel r w z -> (w === x, z === y) -> r x y -> r w z
(~.~) r (p1,p2) = r =.= (sym p1, sym p2)

--------------------------------------------------------------------------------
--          Addition in Inequalities
--------------------------------------------------------------------------------

||| Adding a value on the left does not affect an inequality.
|||
||| ```idris example
||| |> x     < y
||| <> z + x < z + y ... plusLeft
||| ```
export
0 plusLeft :  {x,y,z : Integer}
           -> Rel r (z + x) (z + y)
           -> r x y
           -> r (z + x) (z + y)
plusLeft (_ < _)   v         = plusGT x y z v
plusLeft (_ <= _)  (Left v)  = Left $ plusGT x y z v
plusLeft (_ <= _)  (Right v) = Right $ cong (z +) v
plusLeft (_ === _) v         = cong (z +) v
plusLeft (_ >= _)  (Left v)  = Left $ plusGT y x z v
plusLeft (_ >= _)  (Right v) = Right $ cong (z +) v
plusLeft (_ > _)   v         = plusGT y x z v

||| Adding a value on the right does not affect an inequality.
|||
||| ```idris example
||| |> x     < y
||| <> x + z < y + z ... plusRight
||| ```
export
0 plusRight :  {x,y,z : Integer}
            -> Rel r (x + z) (y + z)
            -> r x y
            -> r (x + z) (y + z)
plusRight w =
  |> rel w x y
  <> rel w (z + x) (z + y) ... plusLeft
  <> rel w (x + z) (y + z) =.= pairPlusCommutative

||| The result of adding a positive value is greater than
||| the original.
export
0 plusPosRight :  {x,y : Integer} -> 0 < y -> x < x + y
plusPosRight =
  |> 0 < y
  <> x + 0 < x + y ... plusLeft
  <> x     < x + y =.. plusZeroRightNeutral

||| The result of adding a positive value is greater than
||| the original.
export
0 plusPosLeft :  {x,y : Integer} -> 0 < y -> x < y + x
plusPosLeft =
  |> 0 < y
  <> 0 + x < y + x ... plusRight
  <> x     < y + x =.. plusZeroLeftNeutral

||| The result of adding a positive value is not less than
||| the original.
export
0 plusNonNegRight :  {x,y : Integer} -> 0 <= y -> x <= x + y
plusNonNegRight (Left lt)  = Left (plusPosRight lt)
plusNonNegRight (Right eq) =
  Right $ rewrite sym eq in (sym $ plusZeroRightNeutral {n = x})

||| The result of adding a positive value is not less than
||| the original.
export
0 plusNonNegLeft :  {x,y : Integer} -> 0 <= y -> x <= y + x
plusNonNegLeft (Left lt)  = Left (plusPosLeft lt)
plusNonNegLeft (Right eq) =
  Right $ rewrite sym eq in (sym $ plusZeroLeftNeutral {n = x})

||| The result of adding a negative value is greater than
||| the original.
export
0 plusNegRight :  {x,y : Integer} -> y < 0 -> x + y < x
plusNegRight =
  |> y < 0
  <> x + y < x + 0 ... plusLeft
  <> x + y < x     ..= plusZeroRightNeutral

||| The result of adding a negative value is greater than
||| the original.
export
0 plusNegLeft :  {x,y : Integer} -> y < 0 -> y + x < x
plusNegLeft =
  |> y < 0
  <> y + x < 0 + x ... plusRight
  <> y + x < x     ..= plusZeroLeftNeutral

||| The result of adding a positive value is not less than
||| the original.
export
0 plusNonPosRight :  {x,y : Integer} -> y <= 0 -> x + y <= x
plusNonPosRight (Left lt)  = Left (plusNegRight lt)
plusNonPosRight (Right eq) =
  Right $ rewrite eq in (plusZeroRightNeutral {n = x})

||| The result of adding a positive value is not less than
||| the original.
export
0 plusNonPosLeft :  {x,y : Integer} -> y <= 0 -> y + x <= x
plusNonPosLeft (Left lt)  = Left (plusNegLeft lt)
plusNonPosLeft (Right eq) =
  Right $ rewrite eq in (plusZeroLeftNeutral {n = x})

||| Subtracting a value does not affect an inequality.
|||
||| ```idris example
||| |> x     < y
||| <> x - z < y - z ... minus
||| ```
export
0 minus :  {x,y,z : Integer}
        -> Rel r (x - z) (y - z)
        -> r x y
        -> r (x - z) (y - z)
minus r =
  |> rel r x y
  <> rel r (x + neg z) (y + neg z) ... plusRight
  <> rel r (x - z) (y - z)         ~.~ (minusIsPlusNeg, minusIsPlusNeg)

||| Subtracting a value from a larger one
||| yields a positive result.
export
0 minusLT :  {x,y : Integer} -> x < y -> 0 < y - x
minusLT =
  |> x     < y
  <> x - x < y - x ... minus
  <> 0     < y - x =.. minusSelfZero

||| Subtracting a value from a non-smaller one
||| yields a non-negative result.
export
0 minusLTE :  {x,y : Integer} -> x <= y -> 0 <= y - x
minusLTE (Left lt)  = Left (minusLT lt)
minusLTE (Right eq) = Right $ Calc $
  |~ 0
  ~~ x - x ..< minusSelfZero
  ~~ y - x ... cong (\v => v - x) eq

||| Subtracting a value from a smaller one
||| yields a negative result.
export
0 minusGT :  {x,y : Integer} -> x < y -> x - y < 0
minusGT =
  |> x     < y
  <> x - y < y - y ... minus
  <> x - y < 0     ..= minusSelfZero

||| Subtracting a value from a non-greater one
||| yields a non-positive result.
export
0 minusGTE :  {x,y : Integer} -> x <= y -> x - y <= 0
minusGTE (Left lt)  = Left (minusGT lt)
minusGTE (Right eq) = Right $ Calc $
  |~ x - y
  ~~ x - x ..< cong (\v => x - v) eq
  ~~ 0     ... minusSelfZero

||| We can solve (in)equalities, where the same value has
||| been added on both sides.
|||
||| ```idris example
||| |> x + z < y + z
||| <> x     < y     ... solvePlusRight
||| ```
export
0 solvePlusRight :  {x,y,z : Integer}
                 -> Rel r x y
                 -> r (x + z) (y + z)
                 -> r x y
solvePlusRight r =
  |> rel r (x + z) (y + z)
  <> rel r ((x + z) - z) ((y + z - z)) ... minus
  <> rel r x y                         =.= (
       solve [x,z] ((x .+. z) -. z) (var x)
     , solve [y,z] ((y .+. z) -. z) (var y)
     )

||| We can solve (in)equalities, where the same value has
||| been added on both sides.
|||
||| ```idris example
||| |> z + x < z + x
||| <> x     < y     ... solvePlusLeft
||| ```
export
0 solvePlusLeft :  {x,y,z : Integer}
                -> Rel r x y
                -> r (z + x) (z + y)
                -> r x y
solvePlusLeft r =
  |> rel r (z + x) (z + y)
  <> rel r (x + z) (y + z) =.= pairPlusCommutative
  <> rel r x y             ... solvePlusRight

||| We can solve (in)equalities, where the same value has
||| been subtracted from both sides.
|||
||| ```idris example
||| |> x - z < y - z
||| <> x     < y     ... solveMinus
||| ```
export
0 solveMinus :  {x,y,z : Integer}
             -> Rel r x y
             -> r (x - z) (y - z)
             -> r x y
solveMinus r =
  |> rel r (x - z) (y - z)
  <> rel r ((x - z) + z) ((y - z) + z) ... plusRight
  <> rel r x y                         =.= (
       solve [x,z] ((x .-. z) +. z) (var x)
     , solve [y,z] ((y .-. z) +. z) (var y)
     )

||| We can solve (in)equalities, with one side an addition
||| and the other equalling zero.
|||
||| ```idris example
||| |> 0     < x + y
||| <> neg y < x     ... solvePlusRightZero
||| ```
export
0 solvePlusRightZero :  {x,y : Integer}
                     -> Rel r (neg y) x
                     -> r 0 (x + y)
                     -> r (neg y) x
solvePlusRightZero r =
  |> rel r 0 (x + y)
  <> rel r (0 - y) ((x + y) - y) ... minus
  <> rel r (neg y) x             =.= (
       solve [y]   (0 -. y) (neg (var y))
     , solve [x,y] ((x .+. y) -. y) (var x)
     )

||| We can solve (in)equalities, with one side an addition
||| and the other equalling the added value.
|||
||| ```idris example
||| |> y  < x + y
||| <> 0  < x     ... solvePlusRightSelf
||| ```
export
0 solvePlusRightSelf :  {x,y : Integer}
                     -> Rel r 0 x
                     -> r y (x + y)
                     -> r 0 x
solvePlusRightSelf r =
  |> rel r y (x + y)
  <> rel r (0 + y) (x + y) ~.. plusZeroLeftNeutral
  <> rel r 0 x             ... solvePlusRight

||| We can solve (in)equalities, with one side an addition
||| and the other equalling zero.
|||
||| ```idris example
||| |> 0     < x + y
||| <> neg x < y     ... solvePlusLeftZero
||| ```
export
0 solvePlusLeftZero :  {x,y : Integer}
                     -> Rel r (neg x) y
                     -> r 0 (x + y)
                     -> r (neg x) y
solvePlusLeftZero r =
  |> rel r 0 (x + y)
  <> rel r 0 (y + x)  ..= plusCommutative
  <> rel r (neg x) y  ... solvePlusRightZero

||| We can solve (in)equalities, with one side an addition
||| and the other equalling the added value.
|||
||| ```idris example
||| |> x  < x + y
||| <> 0  < y     ... solvePlusLeftSelf
||| ```
export
0 solvePlusLeftSelf :  {x,y : Integer}
                    -> Rel r 0 y
                    -> r x (x + y)
                    -> r 0 y
solvePlusLeftSelf r =
  |> rel r x (x + y)
  <> rel r (x + 0) (x + y) ~.. plusZeroRightNeutral
  <> rel r 0 y             ... solvePlusLeft

||| We can solve (in)equalities, with one side a subtraction
||| and the other equalling zero.
|||
||| ```idris example
||| |> 0 < x - y
||| <> y < x     ... solveMinusZero
||| ```
export
0 solveMinusZero : {x,y : Integer} -> Rel r y x -> r 0 (x - y) -> r y x
solveMinusZero r =
  |> rel r 0 (x - y)
  <> rel r (0 + y) ((x - y) + y) ... plusRight
  <> rel r y x                   =.= (
       solve [y]   (0 +. y) (var y)
     , solve [x,y] ((x .-. y) +. y) (var x)
     )

export
0 plusOneLTE : {x,y : Integer} -> x < y -> x + 1 <= y
plusOneLTE lt = App (oneAfterZero (y - x) (minusLT lt)) $
  |> 1     <= y - x
  <> x + 1 <= x + (y - x) ... plusLeft
  <> x + 1 <= y           ..= solve [x,y] (x .+ (y .-. x)) (var y)

--------------------------------------------------------------------------------
--          Negation in Inequalities
--------------------------------------------------------------------------------

||| Negating both sides inverts an inequality.
|||
||| ```idris example
||| |> x     <= y
||| <> neg y <= neg x ... negate
||| ```
export
0 negate :  {x,y : Integer}
         -> Rel r (neg y) (neg x)
         -> r x y
         -> r (neg y) (neg x)
negate r =
  |> rel r x y
  <> rel r (x - (x + y)) (y - (x + y)) ... minus
  <> rel r (neg y) (neg x)             =.= (
       solve [x,y] (x .- (x .+. y)) (negate $ var y)
     , solve [x,y] (y .- (x .+. y)) (negate $ var x)
     )

||| Negating both sides inverts an inequality.
|||
||| ```idris example
||| |> neg x <= neg y
||| <> y     <= x     ... negateNeg
||| ```
export
0 negateNeg : {x,y : Integer} -> Rel r y x -> r (neg x) (neg y) -> r y x
negateNeg r =
  |> rel r (neg x) (neg y)
  <> rel r (neg $ neg y) (neg $ neg x) ... negate
  <> rel r y x                         =.= (negInvolutory, negInvolutory)

||| `negate` specialized to where one side equals zero.
|||
||| ```idris example
||| |> x < 0
||| <> 0 < neg x ... negateZero
||| ```
|||
||| ```idris example
||| |> x <= 0
||| <> 0 <= neg x ... negateZero
||| ```
export
0 negateZero : {x : Integer} -> Rel r (neg x) 0 -> r 0 x -> r (neg x) 0
negateZero r =
  |> rel r 0 x
  <> rel r (neg x) (neg 0) ... negate
  <> rel r (neg x) 0       ..= negZero

||| `negate` specialized to where one side equals zero and the other
||| a negated value.
|||
||| ```idris example
||| |> neg x < 0
||| <> 0     < x ... negateNegZero
||| ```
|||
||| ```idris example
||| |> neg x <= 0
||| <> 0     <= x ... negateNegZero
||| ```
export
0 negateNegZero : {x : Integer} -> Rel r x 0 -> r 0 (neg x) -> r x 0
negateNegZero r =
  |> rel r 0             (neg x)
  <> rel r (neg (neg x)) (neg 0) ... negate
  <> rel r x 0                   =.= (negInvolutory, negZero)

--------------------------------------------------------------------------------
--          Multiplication in Inequalities
--------------------------------------------------------------------------------

0 mplLemma :  {x,y,z : Integer}
           -> 0 < z
           -> x < y
           -> z * x < z * y
mplLemma p =
  |> x         < y
  <> x - x     < y - x               ... minus
  <> 0         < y - x               =.. minusSelfZero
  <> 0         < z * (y - x)         ... (\_ => multPosPosGT0 _ _ p)
  <> 0 + z * x < z * (y - x) + z * x ... plusRight
  <> z * x     < z * y               =.= (
       solve [x,z]   (0 + z .*. x) (z .*. x)
     , solve [x,y,z] (z .* (y .-. x) + z .*. x) (z .*. y)
     )

||| Multiplication with a positive number preserves an inequality.
|||
||| ```idris example
||| |> x     < y
||| <> z * x < z * y ... multPosLeft zgt0
||| ```
|||
||| ```idris example
||| |> x     <= y
||| <> z * x <= z * y ... multPosLeft zgt0
||| ```
export
0 multPosLeft :  {x,y,z : Integer}
              -> 0 < z
              -> Rel r (z * x) (z * y)
              -> r x y
              -> r (z * x) (z * y)
multPosLeft p (_ < _)   rxy       = mplLemma p rxy
multPosLeft p (_ <= _)  (Left w)  = Left $ mplLemma p w
multPosLeft p (_ <= _)  (Right w) = Right $ cong (z *) w
multPosLeft p (_ === _) rxy       = cong (z *) rxy
multPosLeft p (_ >= _)  (Left w)  = Left $ mplLemma p w
multPosLeft p (_ >= _)  (Right w) = Right $ cong (z *) w
multPosLeft p (_ > _)   rxy       = mplLemma p rxy

||| Multiplication with a positive number preserves an inequality.
|||
||| ```idris example
||| |> x     < y
||| <> x * z < y * z ... multPosRight zgt0
||| ```
|||
||| ```idris example
||| |> x     <= y
||| <> x * z <= y * z ... multPosRight zgt0
||| ```
export
0 multPosRight :  {x,y,z : Integer}
               -> 0 < z
               -> Rel r (x * z) (y * z)
               -> r x y
               -> r (x * z) (y * z)
multPosRight p r =
  |> rel r x y
  <> rel r (z * x) (z * y) ... multPosLeft p
  <> rel r (x * z) (y * z) =.= pairMultCommutative

||| Multiplication with a negative number reverses an inequality.
|||
||| ```idris example
||| |> x     < y
||| <> z * y < z * x ... multNegLeft zgt0
||| ```
|||
||| ```idris example
||| |> x     <= y
||| <> z * y <= z * x ... multNegLeft zgt0
||| ```
export
0 multNegLeft :  {x,y,z : Integer}
              -> z < 0
              -> Rel r (z * y) (z * x)
              -> r x y
              -> r (z * y) (z * x)
multNegLeft p r =
  let negp = negateZero (neg z > 0) p
   in |> rel r x y
      <> rel r (neg y) (neg x)                 ... negate
      <> rel r (neg z * neg y) (neg z * neg x) ... multPosLeft negp
      <> rel r (z * y) (z * x)                 =.= (
           solve [z,y] (neg (var z) * neg (var y)) (z .*. y)
         , solve [z,x] (neg (var z) * neg (var x)) (z .*. x)
         )

||| Multiplication with a negative number reverses an inequality.
|||
||| ```idris example
||| |> x     < y
||| <> y * z < x * z ... multNegRight zgt0
||| ```
|||
||| ```idris example
||| |> x     <= y
||| <> y * z <= x * z ... multNegRight zgt0
||| ```
export
0 multNegRight :  {x,y,z : Integer}
               -> z < 0
               -> Rel r (y * z) (x * z)
               -> r x y
               -> r (y * z) (x * z)
multNegRight p r =
  |> rel r x y
  <> rel r (z * y) (z * x) ... multNegLeft p
  <> rel r (y * z) (x * z) =.= pairMultCommutative

0 lemmaMult0 : {x,y,z : Integer} -> 0 === z -> x * z === y * z
lemmaMult0 prf = Calc $
  |~ x * z
  ~~ x * 0 ..< cong (x *) prf
  ~~ 0     ... multZeroRightAbsorbs
  ~~ y * 0 ..< multZeroRightAbsorbs
  ~~ y * z ... cong (y *) prf

||| Multiplication with a non-negative number weakens an inequality.
|||
||| ```idris example
||| |> x     <  y
||| <> x * z <= y * z ... multNonNegRight zgte0
||| ```
export
0 multNonNegRight :  {x,y,z : Integer}
                  -> 0 <= z
                  -> Rel (<=) (x * z) (y * z)
                  -> x < y
                  -> x * z <= y * z
multNonNegRight (Left p) r xy = Left $ multPosRight p (x * z < y * z) xy
multNonNegRight (Right p) r xy = Right $ lemmaMult0 p

||| Multiplication with a non-negative number weakens an inequality.
|||
||| ```idris example
||| |> x     <  y
||| <> z * x <= z * y ... multNonNegLeft zgte0
||| ```
export
0 multNonNegLeft :  {x,y,z : Integer}
                 -> 0 <= z
                 -> Rel (<=) (z * x) (z * y)
                 -> x < y
                 -> z * x <= z * y
multNonNegLeft p r =
  |> x < y
  <> x * z <= y * z ... multNonNegRight p
  <> z * x <= z * y =.= pairMultCommutative

||| Multiplication with a non-positive number weakens and
||| reverses an inequality.
|||
||| ```idris example
||| |> x     <  y
||| <> y * z <= x * z ... multNonPosRight zgte0
||| ```
export
0 multNonPosRight :  {x,y,z : Integer}
                  -> z <= 0
                  -> Rel (<=) (y * z) (x * z)
                  -> x < y
                  -> y * z <= x * z
multNonPosRight (Left p) r xy = Left $ multNegRight p (y * z < x * z) xy
multNonPosRight (Right p) r xy = Right $ lemmaMult0 (sym p)

||| Multiplication with a non-positive number weakens and
||| reverses an inequality.
|||
||| ```idris example
||| |> x     <  y
||| <> z * y <= z * x ... multNonPosLeft zlte0
||| ```
export
0 multNonPosLeft :  {x,y,z : Integer}
                 -> z <= 0
                 -> Rel (<=) (z * y) (z * x)
                 -> x < y
                 -> z * y <= z * x
multNonPosLeft p r =
  |> x < y
  <> y * z <= x * z ... multNonPosRight p
  <> z * y <= z * x =.= pairMultCommutative

0 smpLemma1 : {d,x,y : Integer} -> 0 < d -> d * x < d * y -> x < y
smpLemma1 dpos lt = case comp x y of
  LT p _ _ => p
  EQ _ p _ => void (EQ_not_LT (cong (d *) p) lt)
  GT _ _ p => void (GT_not_LT (multPosLeft dpos (d * x > d * y) p) lt)

0 smpLemma2 : {d,x,y : Integer} -> 0 < d -> d * x === d * y -> x === y
smpLemma2 dpos lt = case comp x y of
  LT p _ _ => void (LT_not_EQ (multPosLeft dpos (d * x < d * y) p) lt)
  EQ _ p _ => p
  GT _ _ p => void (GT_not_EQ (multPosLeft dpos (d * x > d * y) p) lt)

||| We can solve (in)equalities, where both sides have
||| been multiplied with the same positive value.
|||
||| ```idris example
||| |> z * x < z * y
||| <> x     < y     ... solveMultPosLeft zgt0
||| ```
export
0 solveMultPosLeft :  {d,x,y : Integer}
                   -> 0 < d
                   -> Rel r x y
                   -> r (d * x) (d * y)
                   -> r x y
solveMultPosLeft dpos (x < y)   lt         = smpLemma1 dpos lt
solveMultPosLeft dpos (x <= y)  (Left lt)  = Left $ smpLemma1 dpos lt
solveMultPosLeft dpos (x <= y)  (Right eq) = Right $ smpLemma2 dpos eq
solveMultPosLeft dpos (x === y) eq         = smpLemma2 dpos eq
solveMultPosLeft dpos (x >= y)  (Left lt)  = Left $ smpLemma1 dpos lt
solveMultPosLeft dpos (x >= y)  (Right eq) = Right $ smpLemma2 dpos eq
solveMultPosLeft dpos (x > y)   lt         = smpLemma1 dpos lt

||| We can solve (in)equalities, where both sides have
||| been multiplied with the same positive value.
|||
||| ```idris example
||| |> x * z < y * z
||| <> x     < y     ... solveMultPosRight zgt0
||| ```
export
0 solveMultPosRight :  {x,y,d : Integer}
                    -> 0 < d
                    -> Rel r x y
                    -> r (x * d) (y * d)
                    -> r x y
solveMultPosRight dpos r =
  |> rel r (x * d) (y * d)
  <> rel r (d * x) (d * y) =.= pairMultCommutative
  <> rel r x       y       ... solveMultPosLeft dpos

||| We can solve (in)equalities, where both sides have
||| been multiplied with the same negative value.
|||
||| ```idris example
||| |> z * x < z * y
||| <> y     < x     ... solveMultNegLeft zlt0
||| ```
export
0 solveMultNegLeft :  {d,x,y : Integer}
                   -> d < 0
                   -> Rel r y x
                   -> r (d * x) (d * y)
                   -> r y x
solveMultNegLeft dneg r =
  let negdPos = negateZero (neg d > 0) dneg
   in |> rel r (d * x) (d * y)
      <> rel r (neg (d * y)) (neg (d * x)) ... negate
      <> rel r (neg d * y) (neg d * x)     =.= (
           solve [d,y] (neg (d .*. y)) (neg (var d) *. y)
         , solve [d,x] (neg (d .*. x)) (neg (var d) *. x)
         )
      <> rel r y x ... solveMultPosLeft negdPos

||| We can solve (in)equalities, where both sides have
||| been multiplied with the same negative value.
|||
||| ```idris example
||| |> x * z < y * z
||| <> y     < y     ... solveMultNegLeft zlt0
||| ```
export
0 solveMultNegRight :  {x,y,d : Integer}
                    -> d < 0
                    -> Rel r y x
                    -> r (x * d) (y * d)
                    -> r y x
solveMultNegRight dneg r =
  |> rel r (x * d) (y * d)
  <> rel r (d * x) (d * y) =.= pairMultCommutative
  <> rel r y       x       ... solveMultNegLeft dneg

||| We can solve (in)equalities, with one side a multiplication
||| with a positive number and the other equalling zero.
|||
||| ```idris example
||| |> 0 < x * y
||| <> 0 < x     ... solveMultPosRightZero ygt0
||| ```
export
0 solveMultPosRightZero :  {x,y : Integer}
                        -> 0 < y
                        -> Rel r 0 x
                        -> r 0 (x * y)
                        -> r 0 x
solveMultPosRightZero pos r =
  |> rel r 0 (x * y)
  <> rel r (0 * y) (x * y) ~.. multZeroLeftAbsorbs
  <> rel r 0 x             ... solveMultPosRight pos

||| We can solve (in)equalities, with one side a multiplication
||| with a negative number and the other equalling zero.
|||
||| ```idris example
||| |> 0 < x * y
||| <> x < 0     ... solveMultNegRightZero ylt0
||| ```
export
0 solveMultNegRightZero :  {x,y : Integer}
                        -> y < 0
                        -> Rel r x 0
                        -> r 0 (x * y)
                        -> r x 0
solveMultNegRightZero neg r =
  |> rel r 0 (x * y)
  <> rel r (0 * y) (x * y) ~.. multZeroLeftAbsorbs
  <> rel r x 0             ... solveMultNegRight neg

||| We can solve (in)equalities, with one side a multiplication
||| with a positive number and the other equalling zero.
|||
||| ```idris example
||| |> 0 < x * y
||| <> 0 < y     ... solveMultPosLeftZero xgt0
||| ```
export
0 solveMultPosLeftZero :  {x,y : Integer}
                        -> 0 < x
                        -> Rel r 0 y
                        -> r 0 (x * y)
                        -> r 0 y
solveMultPosLeftZero pos r =
  |> rel r 0 (x * y)
  <> rel r (x * 0) (x * y) ~.. multZeroRightAbsorbs
  <> rel r 0 y             ... solveMultPosLeft pos

||| We can solve (in)equalities, with one side a multiplication
||| with a negative number and the other equalling zero.
|||
||| ```idris example
||| |> 0 < x * y
||| <> y < 0     ... solveMultNegLeftZero xlt0
||| ```
export
0 solveMultNegLeftZero :  {x,y : Integer}
                        -> x < 0
                        -> Rel r y 0
                        -> r 0 (x * y)
                        -> r y 0
solveMultNegLeftZero neg r =
  |> rel r 0 (x * y)
  <> rel r (x * 0) (x * y) ~.. multZeroRightAbsorbs
  <> rel r y 0             ... solveMultNegLeft neg

||| We can solve (in)equalities, with one side a multiplication
||| with a positive number and the other equalling the positive
||| number.
|||
||| ```idris example
||| |> y < x * y
||| <> 1 < x     ... solveMultPosRightSelf ygt0
||| ```
export
0 solveMultPosRightSelf :  {x,y : Integer}
                        -> 0 < y
                        -> Rel r 1 x
                        -> r y (x * y)
                        -> r 1 x
solveMultPosRightSelf pos r =
  |> rel r y (x * y)
  <> rel r (1 * y) (x * y) ~.. multOneLeftNeutral
  <> rel r 1 x             ... solveMultPosRight pos

||| We can solve (in)equalities, with one side a multiplication
||| with a positive number and the other equalling the positive
||| number.
|||
||| ```idris example
||| |> x < x * y
||| <> 1 < y     ... solveMultPosLeftSelf xgt0
||| ```
export
0 solveMultPosLeftSelf :  {x,y : Integer}
                       -> 0 < x
                       -> Rel r 1 y
                       -> r x (x * y)
                       -> r 1 y
solveMultPosLeftSelf pos r =
  |> rel r x (x * y)
  <> rel r (x * 1) (x * y) ~.. multOneRightNeutral
  <> rel r 1 y             ... solveMultPosLeft pos

||| We can solve (in)equalities, with one side a multiplication
||| with a negative number and the other equalling the negative
||| number.
|||
||| ```idris example
||| |> y < x * y
||| <> x < 1     ... solveMultNegRightSelf ylt0
||| ```
export
0 solveMultNegRightSelf :  {x,y : Integer}
                        -> y < 0
                        -> Rel r x 1
                        -> r y (x * y)
                        -> r x 1
solveMultNegRightSelf neg r =
  |> rel r y (x * y)
  <> rel r (1 * y) (x * y) ~.. multOneLeftNeutral
  <> rel r x 1             ... solveMultNegRight neg

||| We can solve (in)equalities, with one side a multiplication
||| with a negative number and the other equalling the negative
||| number.
|||
||| ```idris example
||| |> x < x * y
||| <> y < 1     ... solveMultNegLeftSelf xlt0
||| ```
export
0 solveMultNegLeftSelf :  {x,y : Integer}
                        -> x < 0
                        -> Rel r y 1
                        -> r x (x * y)
                        -> r y 1
solveMultNegLeftSelf neg r =
  |> rel r x (x * y)
  <> rel r (x * 1) (x * y) ~.. multOneRightNeutral
  <> rel r y 1             ... solveMultNegLeft neg

--------------------------------------------------------------------------------
--          Division
--------------------------------------------------------------------------------

export
0 multDivP1 : {n,d : Integer} -> (0 < d) -> d * (div n d + 1) > n
multDivP1 dpos = App (snd $ modLT n d dpos) $
  |> mod n d               < d
  <> d * div n d + mod n d < d * div n d + d ... plusLeft
  <> n < d * (div n d + 1)                   =.= (
       lawDivMod n d %search
     , solve [n,d,div n d] (d .*. div n d +. d)
                           (d .* (div n d .+ 1))
     )

export
0 multDiv : {n,d : Integer} -> (0 < d) -> d * div n d <= n
multDiv dpos = App (fst $ modLT n d dpos) $
  |> 0 <= mod n d
  <> d * div n d + 0 <= d * div n d + mod n d ... plusLeft
  <> d * div n d     <= n                     =.= (
       plusZeroRightNeutral
     , lawDivMod n d %search
     )

export
0 divNonNeg : {n,d : Integer} -> (0 <= n) -> (0 < d) -> 0 <= div n d
divNonNeg ngte0 dpos = App (trans_GT_GTE (multDivP1 dpos) ngte0) $
  |> 0     <  d * (div n d + 1)
  <> 0     <  div n d + 1       ... solveMultPosLeftZero dpos
  <> 1     <= div n d + 1       ... (\_ => oneAfterZero _)
  <> 0     <= div n d           ... solvePlusRightSelf

export
0 modLTE : {n,d : Integer} -> (0 <= n) -> (0 < d) -> mod n d <= n
modLTE ngte0 dpos = App (divNonNeg ngte0 dpos) $
  |> 0               <= div n d
  <> d * 0           <= d * div n d           ... multPosLeft dpos
  <> d * 0 + mod n d <= d * div n d + mod n d ... plusRight
  <> mod n d         <= n                     =.= (
       solve [d, mod n d] (d .* 0 +. mod n d) (var (mod n d))
     , lawDivMod n d %search
     )

export
0 modOneIsZero : {n : Integer} -> mod n 1 === 0
modOneIsZero = assert_total $ case comp (mod n 1) 0 of
  EQ _ p _ => p
  LT p _ _ => void (LT_not_GTE p $ fst $ modLT n 1 %search)
  GT _ _ p => void (LT_not_GTE (snd $ modLT n 1 %search) (oneAfterZero _ p))

export
0 divOneSame : {n : Integer} -> div n 1 === n
divOneSame = assert_total $ Calc $
  |~ div n 1
  ~~ 1 * div n 1           ..< multOneLeftNeutral
  ~~ 1 * div n 1 + 0       ..< plusZeroRightNeutral
  ~~ 1 * div n 1 + mod n 1 ..< cong (1 * div n 1 +) modOneIsZero
  ~~ n                     ... lawDivMod n 1 %search

export
0 divGreaterOneLT : {n,d : Integer} -> 0 < n -> 1 < d -> div n d < n
divGreaterOneLT npos dgt1 =
  let dpos = the (0 < d) $ trans %search dgt1
   in assert_total $ case comp 0 (div n d) of
       EQ _ p _ => replace {p = (< n)} p npos
       LT p _ _ => App dgt1 $
         |> 1 < d
         <> 1 * div n d < d * div n d ... multPosRight p
         <> div n d     < d * div n d =.. multOneLeftNeutral
         <> div n d     < n           ... (\_ => trans_GTE_GT $ multDiv dpos)
       GT _ _ p => void (LT_not_GTE p $ divNonNeg %search dpos)

export
0 divPos : {n,d : Integer} -> (d <= n) -> (0 < d) -> 0 < div n d
divPos dn dp = assert_total $ case comp 0 (div n d) of
  LT p _ _ => p
  EQ _ p _ =>
    let modIsN = Calc $
          |~ mod n d
          ~~ 0 + mod n d             ..< plusZeroLeftNeutral
          ~~ (d * 0) + mod n d       ..< cong (+ mod n d) multZeroRightAbsorbs
          ~~ (d * div n d) + mod n d ... cong (\x => (d * x) + mod n d) p
          ~~ n                       ... lawDivMod n d (Right dp)
     in void (LTE_not_GT dn $ rewrite sym modIsN in snd (modLT n d dp))
  GT _ _ p => void (GT_not_LTE p (divNonNeg (Left $ trans_LT_LTE dp dn) dp))


text:
import Data.Primitives.Views
import System

%default total

data InfIO : Type where
    Do : IO a -> (a -> Inf InfIO) -> InfIO

(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

loopPrint : String -> InfIO
loopPrint msg =
    do
        putStrLn msg
        loopPrint msg

data Fuel = Dry | More (Lazy Fuel)

run : Fuel -> InfIO -> IO ()
run (More fuel) (Do action cont) =
    do
        res <- action
        run fuel (cont res)
run Dry p = putStrLn "Out of fuel"


text:
--- ---------------------------------------------------------------- [ Core.idr ]
--- Module      : Lightyear.Core
--- Description : Central Definitions and Instances
---
--- This code is distributed under the BSD 2-clause license.
--- See the file LICENSE in the root directory for its full text.
--- --------------------------------------------------------------------- [ EOH ]
module Lightyear.Core

import Control.Monad.Trans
import Control.Monad.State

import Lightyear.Position

import Debug.Trace

-- %access public export

namespace Lightyear.State

  ||| State to keep track off during parsing.
  public export
  record State (str : Type) where
    constructor ST
    input     : str
    position  : Position
    tab_width : Nat

namespace Lightyear.Error

  ||| Error messages to return.
  public export
  record Error str where
    constructor Err
    position : Position
    msg : String

  export
  display : {0 str : Type} -> Error str -> String
  display (Err pos msg) = concat [display pos,":\n\t", msg]

public export
data Result : (str : Type) -> (a : Type) -> Type where
  Success : a -> Result str a
  Failure : List (Error str) -> Result str a

public export
Functor (Result str) where
  map f (Success x)  = Success (f x)
  map f (Failure es) = Failure es

public export
data Reply : (str : Type) -> (a : Type) -> Type where
  MkReply : State str -> Result str a -> Reply str a

public export
record ParserT (str : Type) (m : Type -> Type) a where
  constructor PT
  runParserT : (0 r : Type)
            -> (parseOK  : a -> State str -> m r)
            -> (emptyOK  : a -> State str -> m r)
            -> (parseErr : List (Error str) -> State str -> m r)
            -> (emptyErr : List (Error str) -> State str -> m r)
            -> State str
            -> m r

public export
execParserT : {0 str : Type}
           -> {0 a : Type}
           -> Monad m
           => (parser : ParserT str m a)
           -> (input  : State str)
           -> m (Reply str a)
execParserT (PT p) input =
    p (Reply str a) success success failure failure input
   where
     success : a -> State str -> m (Reply str a)
     success i x = pure $ MkReply x $ Success i

     failure : List (Error str) -> State str -> m (Reply str a)
     failure es x = pure $ MkReply x $ Failure es

public export
Monad m => Functor (ParserT str m) where
  map {a} {b} f (PT p) = PT $ \r, us, cs => p r (us . f) (cs . f)

public export
Monad m => Applicative (ParserT str m) where
  pure x = PT (\r, us, cs, ue, ce => us x)

  (<*>) (PT f) (PT g) =
      PT $ \r, us, cs, ue, ce
         => f r (\f' => g r (us . f') (cs . f') ue ce)
                (\f' => g r (cs . f') (cs . f') ce ce)
                ue ce

infixl 2 <*>|
||| A variant of <*>, lazy in its second argument, which must NOT be
||| pattern-matched right away because we want to keep it lazy in case
||| it's not used.
public export
(<*>|) : Monad m => ParserT str m (a -> b)
                 -> Lazy (ParserT str m a)
                 -> ParserT str m b
(<*>|) (PT f) x = PT $ \r, us, cs, ue, ce =>
    f r (\f' => let PT g = x in g r (us . f') (cs . f') ue ce)
        (\f' => let PT g = x in g r (cs . f') (cs . f') ce ce)
        ue ce

public export
Monad m => Monad (ParserT str m) where
  (>>=) (PT x) f =
      PT (\r, us, cs, ue, ce
            => x r (\x' => let PT y = f x' in y r us cs ue ce)
                   (\x' => let PT y = f x' in y r cs cs ce ce)
                   ue ce)

public export
MonadTrans (ParserT str) where
  lift x = PT (\r, us, cs, ue, ce, s => (x >>= flip us s))

public export
MonadState s m => MonadState s (ParserT str m) where
  get = lift get
  put = lift . put

||| Fail with some error message
public export
fail : String -> ParserT str m a
fail msg = PT $ \r, us, cs, ue, ce, (ST i p tw) => ue [Err p msg] (ST i p tw)

public export
Monad m => Alternative (ParserT str m) where
  empty = fail "non-empty alternative"

  (<|>) (PT left) (PT right) =
      PT $ \r, us, cs, ue, ce, st =>
          left r us cs (\err,st' => right r us cs (ue . (err ++))
                                                  (ce . (err ++)) st) ce st

public export
lightyearAlt' : Monad m
             => (left  : ParserT str m a)
             -> (right : Lazy (ParserT str m a))
             -> ParserT str m a
lightyearAlt' (PT left) right = PT leftright
  where
    leftright : (0 r : Type)
             -> (parseOK  : a -> State str -> m r)
             -> (emptyOK  : a -> State str -> m r)
             -> (parseErr : List (Error str) -> State str -> m r)
             -> (emptyErr : List (Error str) -> State str -> m r)
             -> State str
             -> m r
    leftright r us cs ue ce st =
        left r us cs (\err, st' => let PT right' = right
                                    in right' r us cs (ue . (err++))
                                                      (ce . (err++)) st)
                                                      ce st

infixl 3 <|>|

||| A variant of <|>, lazy in its second argument, which must NOT be
||| pattern-matched right away because we want to keep it lazy in case
||| it's not used.
public export
(<|>|) : Monad m => ParserT str m a
                 -> Lazy (ParserT str m a)
                 -> ParserT str m a
(<|>|) = lightyearAlt'

infixl 0 <?>
||| Associate an error with parse failure
public export
(<?>) : Monad m => ParserT str m a -> String -> ParserT str m a
(<?>) (PT f) msg = PT $ \r, us, cs, ue, ce, (ST i pos tw)
    => f r us cs (ue . ((Err pos msg)::))
                 (ce . ((Err pos msg)::)) (ST i pos tw)

||| Commit to a parse alternative and prevent backtracking
public export
commitTo : Monad m => ParserT str m a -> ParserT str m a
commitTo (PT f) = PT $ \r, us, cs, ue, ce => f r cs cs ce ce

-- There is no reason that we mark "str" as the determining type
-- other than to aid typeclass/interface resolution.
--
-- I feel that having this restriction (which is probably okay
-- given that the only streams so far are String and Text anyway)
-- is more acceptable than failing surprisingly
-- any time the unsuspecting user calls "satisfy" without {tok=Char}
-- in an odd context.
--
-- We make "str" the determining type because it's usually fixed
-- by the parser monad you're working in, which helps resolution.
public export
interface Stream tok str | str where
  uncons : str -> Maybe (tok, str)

  updatePos : Nat -> Position -> tok -> Pair Position Position

public export
initialState : Maybe String -> s -> Nat -> State s
initialState name s tw = ST s (defaultPos name) tw

||| Matches a single element that satisfies some condition, accepting
||| a transformation of successes.
public export
satisfyMaybe : (Monad m, Stream tok str)
            => (tok -> Maybe out)
            -> ParserT str m out
satisfyMaybe {tok=tok} {str=str} f =
   PT $ \r, us, cs, ue, ce, (ST i pos tw) =>
     case uncons {tok=tok} {str=str} i of
       Nothing        => ue [Err pos "a token, not EOF"] (ST i pos tw)
       Just (t, rest) => case f t of
         Nothing  => ue [Err pos "a different token"] (ST i pos tw)
         Just res => let (newPos, _) = updatePos {tok=tok} {str=str} tw pos t
                      in us res (ST rest newPos tw)

||| Matches a single element that satisfies some condition.
public export
satisfy : (Monad m, Stream tok str)
                   => (tok -> Bool)
                   -> ParserT str m tok
satisfy p = satisfyMaybe (\t => if p t then Just t else Nothing)

||| Succeeds if and only if the argument parser fails.
|||
||| In Parsec, this combinator is called `notFollowedBy`.
public export
requireFailure : ParserT str m tok -> ParserT str m ()
requireFailure (PT f) = PT requireFailureHelper where
    requireFailureHelper : (0 r : Type)
                        -> (() -> State str -> m r)
                        -> (() -> State str -> m r)
                        -> (List (Error str) -> State str -> m r)
                        -> (List (Error str) -> State str -> m r)
                        -> State str
                        -> m r
    requireFailureHelper r us cs ue ce ss@(ST i pos tw) =
        f r
            (\t, s => ue [Err pos "argument parser to fail"] s)
            (\t, s => ce [Err pos "argument parser to fail"] s)
            (\errs, _ => us () ss)
            (\errs, _ => cs () ss)
            ss

public export
getState : ParserT str m (State str)
getState = PT $ \r,us,cs,ue,ce,s => us s s

||| Return the current position of the parser in the input stream.
public export
getPosition : Monad m => ParserT str m Position
getPosition = position <$> getState

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

max_stars_repo_name: Mr-Andersen/lightyear

max_issues_repo_name: Mr-Andersen/lightyear

max_forks_repo_name: Mr-Andersen/lightyear


text:
||| Primitive operations for the Felt data type.
module Primitives.Felt

import Core.Context
import CairoCode.CairoCode
import Data.SortedSet
import Data.SortedMap
import Primitives.Common
import CommonDef
import CodeGen.CodeGenHelper

-- https://github.com/starkware-libs/cairo-lang/blob/cf8266fd5d1ff66962579ff7967ac5cdcf699f77/src/starkware/cairo/lang/cairo_constants.py
-- 2^251 + 17 * 2^192 + 1
public export
PRIME : Integer
PRIME = 3618502788666131213697322783095070105623107215331596699973092056135872020481

public export
HALF_PRIME : Integer
HALF_PRIME = PRIME `div` 2
-- 1809251394333065606848661391547535052811553607665798349986546028067936010240

-- Converts i to an integer in the range (-prime/2, prime/2) which is equivalent to val modulo prime.
-- https://github.com/starkware-libs/cairo-lang/blob/3d33c4e829a87bc3d88cf04ed6a489e788918b8b/src/starkware/cairo/lang/compiler/expression_simplifier.py#L147
export
integerToFelt : Integer -> Integer
integerToFelt i = (i + HALF_PRIME) `mod` PRIME - HALF_PRIME

-- Extended Euclidian Algorithm
-- extendedEu a PRIME computes (a^(-1),_)
extendedEu : Integer -> Integer -> (Integer, Integer)
extendedEu a 0 = (1, 0)
extendedEu a b =
  let q = a `div` b
      r = a `mod` b
      (s, t) = extendedEu b r
   in (t, s - q * t)

-- a / b
export
feltDiv : Integer -> Integer -> Integer
feltDiv a b = let (invB, _) = extendedEu b PRIME -- computes b^(-1)
                  res = (a * invB) `mod` PRIME
               in integerToFelt res

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

feltBinOp : (op: String) -> CairoReg -> List CairoReg -> LinearImplicitArgs -> PrimFnCode
feltBinOp op r [a,b] impls =
  if impls == empty
    then Raw "\{ compileRegDecl r } = \{ compileReg a } \{op} \{ compileReg b }\n"
    else assert_total $ idris_crash "no implicits expected for generateCodeBinOp: \{op}"
feltBinOp op _ _ _ = assert_total $ idris_crash "Bad arguments to feltBinOp: \{op}"

export
[add_felt] PrimFn where
    eval [_, ConstValue (F 0)] = Just $ ArgValue 0
    eval [ConstValue (F 0), _] = Just $ ArgValue 1
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ F $ integerToFelt (a+b)
    eval _ = Nothing

    generateCode = feltBinOp "+"

export
[sub_felt] PrimFn where
    eval [_, ConstValue (F 0)] = Just $ ArgValue 0
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ F $ integerToFelt (a-b)
    eval _ = Nothing

    generateCode = feltBinOp "-"

export
[mul_felt] PrimFn where
    eval [_, ConstValue (F 1)] = Just $ ArgValue 0
    eval [ConstValue (F 1), _] = Just $ ArgValue 1
    eval [_, ConstValue (F 0)] = Just $ NewValue $ ConstValue $ F 0
    eval [ConstValue (F 0), _] = Just $ NewValue $ ConstValue $ F 0
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ F $ integerToFelt (a*b)
    eval _ = Nothing

    generateCode = feltBinOp "*"

export
[div_felt] PrimFn where
    eval [_, ConstValue (F 0)] = Just $ Failure "Division by zero is not defined"
    eval [_, ConstValue (F 1)] = Just $ ArgValue 0
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ F (feltDiv a b)
    eval _ = Nothing

    generateCode = feltBinOp "/"

export
[neg_felt] PrimFn where
    eval [ConstValue (F a)] = Just $ NewValue $ ConstValue $ F $ integerToFelt (-a)
    eval _ = Nothing

    generateCode r [a] _ = Raw "\{ compileRegDecl r } = -\{ compileReg a }\n"
    generateCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode neg_felt"

--Todo: should we even allow this (should we have shifts in general)
export
[shl_felt] PrimFn where
    eval [_, ConstValue(F 0)] = Just $ ArgValue 0
    -- Todo: Just an incorrect quick hack add real felt impl in idris2
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ F $ integerToFelt (prim__shl_Integer (cast a) (cast b))
    eval _ = Nothing

    generateCode = generateMissingCodeError "shl_felt"

--Todo: should we even allow this (should we have shifts in general)
export
[shr_felt] PrimFn where
    eval [_, ConstValue(F 0)] = Just $ ArgValue 0
    -- Todo: Just an incorrect quick hack add real felt impl in idris2
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ F $ integerToFelt (prim__shr_Integer (cast a) (cast b))
    eval _ = Nothing

    generateCode = generateMissingCodeError "shr_felt"

-- Duplicate of UInt.and_uintX_code
and_felt_code : CairoReg -> CairoReg -> CairoReg -> CairoReg -> CairoReg -> String
and_felt_code r bitwise_ptr_in bitwise_ptr_out x y = """
    assert [\{compileReg bitwise_ptr_in}] = \{compileReg x}
    assert [\{compileReg bitwise_ptr_in}+1] = \{compileReg y}
    \{ compileRegDecl bitwise_ptr_out} = \{compileReg bitwise_ptr_in} + BitwiseBuiltin.SIZE
    \{ compileRegDecl r } = [\{compileReg bitwise_ptr_in}+2]

"""
export
[and_felt] PrimFn where
    -- Todo: Just an incorrect quick hack add real felt impl in idris2
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ F $ integerToFelt (prim__and_Integer (cast a) (cast b))
    eval _ = Nothing

    generateCode res [a,b] implicits =
        case lookup bitwise_builtin implicits of
            Just (bw_in, bw_out) => Raw $ and_felt_code res bw_in bw_out a b
            Nothing => assert_total $ idris_crash "bitwise_ptr not found"
    generateCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode and_felt"

-- Duplicate of UInt.or_uintX_code
or_felt_code : CairoReg -> CairoReg -> CairoReg -> CairoReg -> CairoReg -> String
or_felt_code r bitwise_ptr_in bitwise_ptr_out x y = """
    assert [\{compileReg bitwise_ptr_in}] = \{compileReg x}
    assert [\{compileReg bitwise_ptr_in}+1] = \{compileReg y}
    \{ compileRegDecl bitwise_ptr_out} = \{compileReg bitwise_ptr_in} + BitwiseBuiltin.SIZE
    \{ compileRegDecl r } = [\{compileReg bitwise_ptr_in}+4]

"""

export
[or_felt] PrimFn where
    -- Todo: Just an incorrect quick hack add real felt impl in idris2
    eval [ConstValue (F a),ConstValue (F b)] = Just $ NewValue $ ConstValue $ F $ integerToFelt (prim__or_Integer (cast a) (cast b))
    eval _ = Nothing

    generateCode res [a,b] implicits =
        case lookup bitwise_builtin implicits of
                Just (bw_in, bw_out) => Raw $ or_felt_code res bw_in bw_out a b
                Nothing => assert_total $ idris_crash "bitwise_ptr not found"
    generateCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode or_felt_code"

-- Duplicate of UInt.xor_uintX_code
xor_felt_code : CairoReg -> CairoReg -> CairoReg -> CairoReg -> CairoReg -> String
xor_felt_code r bitwise_ptr_in bitwise_ptr_out x y = """
    assert [\{compileReg bitwise_ptr_in}] = \{compileReg x}
    assert [\{compileReg bitwise_ptr_in}+1] = \{compileReg y}
    \{ compileRegDecl bitwise_ptr_out} = \{compileReg bitwise_ptr_in} + BitwiseBuiltin.SIZE
    \{ compileRegDecl r } = [\{compileReg bitwise_ptr_in}+3]

"""

export
[xor_felt] PrimFn where
    -- Todo: Just an incorrect quick hack add real felt impl in idris2
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ F $ integerToFelt (prim__xor_Integer (cast a) (cast b))
    eval _ = Nothing

    generateCode res [a,b] implicits =
        case lookup bitwise_builtin implicits of
                Just (bw_in, bw_out) => Raw $ xor_felt_code res bw_in bw_out a b
                Nothing => assert_total $ idris_crash "bitwise_ptr not found"
    generateCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode xor_felt"

---------------------------------------------------------------------------------------------------
-- Felt LT
---------------------------------------------------------------------------------------------------
lt_felt_name : Name
lt_felt_name = makeBuiltinName "is_lt_felt"

lt_felt_code : String
lt_felt_code = """
# Checks if the unsigned integer lift (as a number in the range [0, PRIME)) of a is lower than
# that of b.
# See split_felt() for more details.
# Returns 1 if true, 0 otherwise.
func \{cairoName lt_felt_name}(range_check_ptr,a, b) -> (res, range_check_ptr):
    %{ memory[ap] = 0 if (ids.a % PRIME) < (ids.b % PRIME) else 1 %}
    jmp not_lt if [ap] != 0; ap++
    assert_lt_felt{range_check_ptr=range_check_ptr}(a, b)
    return (1, range_check_ptr)

    not_lt:
    assert_le_felt{range_check_ptr=range_check_ptr}(b, a)
    return (0, range_check_ptr)
end

"""

export
[lt_felt] PrimFn where
    apStable = False

    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ toInt (a<b)
    eval _ = Nothing

    imports = fromList [
        MkImport "starkware.cairo.common.math_cmp" "assert_lt_felt",
        MkImport "starkware.cairo.common.math_cmp" "assert_le_felt"]
    implicits = singleton range_check_builtin
    dependencies = fromList [(lt_felt_name, ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty lt_felt_code) 2 1)]
    generateCode res args implicits = Instructions [CALL [res] implicits lt_felt_name args]

---------------------------------------------------------------------------------------------------
-- Felt LTE
---------------------------------------------------------------------------------------------------
lte_felt_name : Name
lte_felt_name = makeBuiltinName "is_lte_felt"

lte_felt_code : String
lte_felt_code = """
    # Checks if the unsigned integer lift (as a number in the range [0, PRIME)) of a is lower than
    # or equal to that of b.
    # See split_felt() for more details.
    # Returns 1 if true, 0 otherwise.
    func \{cairoName lte_felt_name}(range_check_ptr, a, b) -> (res, range_check_ptr):
        %{ memory[ap] = 0 if (ids.a % PRIME) <= (ids.b % PRIME) else 1 %}
        jmp not_le if [ap] != 0; ap++
        assert_le_felt{range_check_ptr=range_check_ptr}(a, b)
        return (1, range_check_ptr)

        not_le:
        assert_lt_felt{range_check_ptr=range_check_ptr}(b, a)
        return (0, range_check_ptr)
    end

"""

export
[lte_felt] PrimFn where
    apStable = False

    -- Todo: Just an incorrect quick hack add real felt impl in idris2
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ toInt (a<=b)
    eval _ = Nothing

    imports = fromList [
        MkImport "starkware.cairo.common.math_cmp" "assert_lt_felt",
        MkImport "starkware.cairo.common.math_cmp" "assert_le_felt"]
    implicits = singleton range_check_builtin
    dependencies = fromList [(lte_felt_name, ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty lte_felt_code) 2 1)]
    generateCode res args implicits = Instructions [CALL [res] implicits lte_felt_name args]

---------------------------------------------------------------------------------------------------
-- Felt EQ
---------------------------------------------------------------------------------------------------
export
[eq_felt] PrimFn where
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ toInt (a==b)
    eval _ = Nothing

    generateCode r a i = Raw $ compileEqOp "eq_felt" r a i

---------------------------------------------------------------------------------------------------
-- Felt GTE
-- Implementation uses flipped arguments to lte
---------------------------------------------------------------------------------------------------
export
[gte_felt] PrimFn where
    apStable = False

    -- Todo: Just an incorrect quick hack add real felt impl in idris2
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ toInt (a>=b)
    eval _ = Nothing

    imports = fromList [
        MkImport "starkware.cairo.common.math_cmp" "assert_lt_felt",
        MkImport "starkware.cairo.common.math_cmp" "assert_le_felt"]
    implicits = singleton range_check_builtin
    dependencies = fromList [(lte_felt_name, ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty lte_felt_code) 2 1)]
    generateCode res [a,b] implicits = Instructions [CALL [res] implicits lte_felt_name [b,a]] -- Flipped arguments
    generateCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode gte_felt"

---------------------------------------------------------------------------------------------------
-- Felt GT
-- Implementation uses flipped arguments to lt
---------------------------------------------------------------------------------------------------
export
[gt_felt] PrimFn where
    apStable = False

    -- Todo: Just an incorrect quick hack add real felt impl in idris2
    eval [ConstValue (F a), ConstValue (F b)] = Just $ NewValue $ ConstValue $ toInt (a>b)
    eval _ = Nothing

    imports = fromList [
        MkImport "starkware.cairo.common.math_cmp" "assert_lt_felt",
        MkImport "starkware.cairo.common.math_cmp" "assert_le_felt"]
    implicits = singleton range_check_builtin
    dependencies = fromList [(lt_felt_name, ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty lt_felt_code) 2 1)]
    generateCode res [a,b] implicits = Instructions [CALL [res] implicits lt_felt_name [b,a]] -- Flipped arguments
    generateCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode gt_felt"

-- Todo: How to treat Integers which are larger or smaller than Felt
export
[cast_to_felt] PrimFn where
    eval [ConstValue c] = map (\i => NewValue $ ConstValue $ F $ integerToFelt i) (constToInteger c)
    eval _ = Nothing

    generateCode r [a] _ = Raw "\{ compileRegDecl r } = \{ compileReg a } #Cast to felt\n"
    generateCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode cast_to_felt"

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module BinaryInt

||| A type for binary representation of integers
data Nat2   = Zbit              --  0
            | Ibit              --  1
            | Times2 Nat2       -- x0
            | Times2Plus1 Nat2  -- x1

||| Binary addition, case by case.
(+) : Nat2 -> Nat2 -> Nat2
(+) Zbit y = y                                                      --  0 +  y = y
(+) x Zbit = x                                                      --  x +  0 = x
(+) Ibit Ibit = Times2 Ibit                                         --  1 +  1 = 10
(+) Ibit (Times2 y) = Times2Plus1 y                                 --  1 + y0 = y1
(+) Ibit (Times2Plus1 y) = Times2 ((+) Ibit y)                      --  1 + y1 = (y+1)1
(+) (Times2 x) Ibit = Times2Plus1 x                                 -- x0 +  1 = x1
(+) (Times2 x) (Times2 y) = Times2 ((+) x y)                        -- x0 + y0 = (x+y)0
(+) (Times2 x) (Times2Plus1 y) = Times2Plus1 ((+) x y)              -- x0 + y1 = (x+y)1
(+) (Times2Plus1 x) Ibit = Times2 ((+) x Ibit)                      -- x1 +  1 = (x+1)0
(+) (Times2Plus1 x) (Times2 y) = Times2Plus1 ((+) x y)              -- x1 + y0 = (x+y)1
(+) (Times2Plus1 x) (Times2Plus1 y) = Times2 ((+) x ((+) y Ibit) )  -- x1 + y1 = (x+(y+1))0

||| ---------------------------------------------------------------------------
||| Prove associativity.
||| This is a simple proposition, i.e. a singleton type.
||| ---------------------------------------------------------------------------

assLaw : (x:Nat2) -> (y:Nat2) -> (z:Nat2) -> (+) x ( (+) y z ) = (+) ((+) x y ) z
assLaw x y Zbit = ?xyZbit

||| ---------------------------------------------------------------------------
||| Equality only supported by reflexive constructor `Same`
||| So `Same 5 : EqNat 5 5`  so `EqNat k k` is **always** inhabited.
||| However there is no constructor for `EqNat 4 5` for example, that type
||| exists but is **never** uninhabitted. I.e.
|||
||| *EqNat> the (EqNat 4 4) (Same _)  -- works, 4 replaces _
||| *EqNat> the (EqNat 4 5) (Same _)  -- fails, no solution to _
|||
||| ---------------------------------------------------------------------------
data EqNat : (i:Nat) -> (j:Nat) -> Type where
    Same : (k:Nat) -> EqNat k k

data EqNat2 : (i:Nat2) -> (j:Nat2) -> Type where
    Same2 : (k:Nat2) -> EqNat2 k k

||| ---------------------------------------------------------------------------
||| Function to lift equality inductively.
||| This isn't total but only used on equal inputs in the type checker.
||| ---------------------------------------------------------------------------
--liftEq : (i:Nat) -> (j:Nat) -> (i = j) -> (S i) = (S j)
--liftEq k k Refl = Refl

--liftEqTimes2 : (i:Nat2) -> (j:Nat2) -> (eq:EqNat2 i j) -> EqNat2 (Times2 i) (Times2 j)
--liftEqTimes2 k k (Same2 k) = Same2 (Times2 k)
--liftEqTimes2Plus1 : (i:Nat2) -> (j:Nat2) -> (eq:EqNat2 i j) -> EqNat2 (Times2Plus1 i) (Times2Plus1 j)
--liftEqTimes2Plus1 k k (Same2 k) = Same2 (Times2Plus1 k)

||| ---------------------------------------------------------------------------
||| Check equality and convert to Maybe EqNat
||| As usual define checkEqNat on the various constructors of Nat/Nat2
||| where the behavior is clear.  Makes an total function by induction.
|||
||| checkEqNat 4 5 = Nothing : Maybe EqNat 4 5
||| checkEqNat 4 4 = Just Same 4 : Maybe EqNat 4 4
|||
||| ---------------------------------------------------------------------------
checkEqNat : (i:Nat) -> (j:Nat) -> Maybe( i = j )
checkEqNat Z Z          = Just Refl
checkEqNat (S k) Z      = Nothing
checkEqNat Z (S k)      = Nothing
checkEqNat (S k) (S m)  = case checkEqNat k m of
                            Nothing => Nothing
                            Just prfEq  => Just (cong prfEq)

checkEqNat2 : (i:Nat2) -> (j:Nat2) -> Maybe( i = j )
checkEqNat2 Zbit            Zbit               = Just Refl
checkEqNat2 Ibit            Zbit               = Nothing
checkEqNat2 (Times2 k)      Zbit               = Nothing
checkEqNat2 (Times2Plus1 k) Zbit               = Nothing
checkEqNat2 Ibit            Ibit               = Just Refl
checkEqNat2 (Times2 k)      Ibit               = Nothing
checkEqNat2 (Times2Plus1 k) Ibit               = Nothing
checkEqNat2 (Times2 k)      (Times2 m)           = case checkEqNat2 k m of
                                                    Nothing => Nothing
                                                    Just eq => Just (cong eq)
checkEqNat2 (Times2Plus1 k) (Times2 m)           = Nothing
checkEqNat2 (Times2Plus1 k) (Times2Plus1 m)      = case checkEqNat2 k m of
                                                    Nothing => Nothing
                                                    Just eq => Just (cong eq)

||| ---------------------------------------------------------------------------
||| The Isomorphism binary natural numbers to unary natural numbers
||| ---------------------------------------------------------------------------

btou : Nat2 -> Nat
btou Zbit             = Z
btou Ibit             = S Z
btou (Times2 x)       = (btou x) + (btou x)
btou (Times2Plus1 x)  = S ((btou x) + (btou x))

utob : Nat -> Nat2
utob Z = Zbit
utob (S k) = (utob k) + Ibit

||| ---------------------------------------------------------------------------
||| The proof of Isomorphism
|||
||| Idris does eager evaluation so utob(btou Zbit) = utob Z
||| ---------------------------------------------------------------------------
leftIdBU : (x:Nat2) ->  utob (btou x) = x
leftIdBU Zbit = Refl

max_stars_repo_name: algeboy/BlackBoxType

max_issues_repo_name: algeboy/BlackBoxType

max_forks_repo_name: algeboy/BlackBoxType


text:
> module SequentialDecisionProblems.examples.Main

> import Decidable.Order

> import Data.List
> import Data.List.Quantifiers
> import Effects
> import Effect.Exception
> import Effect.StdIO

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.FullTheory
> import SequentialDecisionProblems.TabBackwardsInduction
> import SequentialDecisionProblems.Utils
> import SequentialDecisionProblems.NonDeterministicDefaults
> import SequentialDecisionProblems.CoreTheoryOptDefaults
> import SequentialDecisionProblems.FullTheoryOptDefaults
> import SequentialDecisionProblems.TabBackwardsInductionOptDefaults

> import SequentialDecisionProblems.examples.LeftAheadRight

> import List.Operations
> import List.Properties
> import BoundedNat.BoundedNat
> import BoundedNat.Operations
> import BoundedNat.Properties
> import Sigma.Sigma
> import Sigma.Operations
> import Nat.OperationsProperties
> import Nat.LTEProperties
> import Nat.LTProperties
> import Unit.Properties
> import Void.Properties
> import LocalEffect.Exception
> import LocalEffect.StdIO

> -- %default total
> %auto_implicits off

> -- %logging 5

Like "Example2.lidr", but now |step t x y| is empty in states
corresponding to |maxColumn|, no matter which |y| is selected! Thus,
such states are not viable for more than zero steps. Attemps at making
more than zero decision steps starting from |maxColumn| should be
detected and rejected.

* The decision process:

> maxColumn : Nat
> maxColumn = 10

> nColumns : Nat
> nColumns = S maxColumn

** States:

> SequentialDecisionProblems.CoreTheory.State t = LTB nColumns

** Controls:

> SequentialDecisionProblems.CoreTheory.Ctrl t x = LeftAheadRight

** Transition function:

> SequentialDecisionProblems.CoreTheory.nexts t (MkSigma Z prf) Left =
>   [MkSigma maxColumn (ltIdS maxColumn)]
> SequentialDecisionProblems.CoreTheory.nexts t (MkSigma (S n) prf) Left with (decLT (S n) maxColumn)
>   | (Yes p)     = [MkSigma n (ltLemma1 n nColumns prf)]
>   | (No contra) = []
> SequentialDecisionProblems.CoreTheory.nexts t (MkSigma n prf) Ahead with (decLT n maxColumn)
>   | (Yes p)     = [MkSigma n prf]
>   | (No contra) = []
> SequentialDecisionProblems.CoreTheory.nexts t (MkSigma n prf) Right with (decLT n maxColumn)
>   | (Yes p)     = [MkSigma (S n) (LTESucc p)]
>   | (No contra) = []

** |Val| and |LTE|:

> SequentialDecisionProblems.CoreTheory.Val =
>   Nat

> SequentialDecisionProblems.CoreTheory.plus =
>   Prelude.Nat.plus

> SequentialDecisionProblems.CoreTheory.zero =
>   Z

> SequentialDecisionProblems.CoreTheory.LTE =
>   Prelude.Nat.LTE

> SequentialDecisionProblems.FullTheory.reflexiveLTE =
>   Nat.LTEProperties.reflexiveLTE

> SequentialDecisionProblems.FullTheory.transitiveLTE =
>   Nat.LTEProperties.transitiveLTE

> SequentialDecisionProblems.FullTheory.monotonePlusLTE =
>   Nat.LTEProperties.monotoneNatPlusLTE

> SequentialDecisionProblems.CoreTheoryOptDefaults.totalPreorderLTE =
>   Nat.LTEProperties.totalPreorderLTE

** Reward function:

> SequentialDecisionProblems.CoreTheory.reward t x y (MkSigma c _) =
>   if c == Z
>   then (S Z)
>   else if (S c) == nColumns
>        then (S (S Z))
>        else Z

** Measure:

> SequentialDecisionProblems.CoreTheory.meas = sum
> SequentialDecisionProblems.FullTheory.measMon = sumMon

** |State| is finite:

> SequentialDecisionProblems.TabBackwardsInduction.finiteState t =
>   finiteLTB nColumns

** |Ctrl| is finite:

> SequentialDecisionProblems.Utils.finiteCtrl _ =
>   finiteLeftAheadRight

** Reachability:

> SequentialDecisionProblems.CoreTheory.Reachable x' = Unit
> SequentialDecisionProblems.CoreTheory.reachableSpec1 {t} x r y = all (nexts t x y) where
>   all : (xs : List (State (S t))) -> SequentialDecisionProblems.CoreTheory.All (Reachable {t' = S t}) xs
>   all Nil = Nil
>   all (x :: xs) = () :: (all xs)
> SequentialDecisionProblems.TabBackwardsInduction.decidableReachable x = decidableUnit

** Viability:

> nextsLemma0 : {t : Nat} ->
>               (x : State t) -> (outl x `LT` maxColumn) -> nexts t x Ahead = [x]
> nextsLemma0 {t} (MkSigma i prf) p with (decLT i maxColumn)
>   | (Yes _) = Refl
>   | (No contra) = void (contra p)

> nextsLemma1 : {t : Nat} ->
>               (x : State t) -> (outl x `LT` maxColumn) ->
>               SequentialDecisionProblems.CoreTheory.NotEmpty (nexts t x Ahead)
> nextsLemma1 {t} x prf with (decLT (outl x) maxColumn)
>   | (Yes p) = s3 where
>     s1 : SequentialDecisionProblems.CoreTheory.NotEmpty [x]
>     s1 = SequentialDecisionProblems.CoreTheory.elemNotEmptySpec0 x [x] Here
>     s2 : [x] = nexts t x Ahead
>     s2 = sym (nextsLemma0 x p)
>     s3 : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts t x Ahead)
>     s3 = replace s2 s1
>   | (No contra) = void (contra prf)

> SequentialDecisionProblems.CoreTheory.Viable  Z    _ = Unit
> SequentialDecisionProblems.CoreTheory.Viable (S n) x with (decLT (outl x) maxColumn)
>   | (Yes _) = Unit
>   | (No  _) = Void

> viableLemma0 : {t : Nat} -> {x : State t} -> Viable Z x = Unit
> viableLemma0 = Refl

> viableLemma1 : {t : Nat} -> {n : Nat} -> {x : State t} ->
>                (outl x) `Prelude.Nat.LT` maxColumn -> Viable (S n) x = Unit
> viableLemma1 {t} {n} {x} prf with (decLT (outl x) maxColumn)
>   | (Yes _) = Refl
>   | (No contra) = void (contra prf)

> viableLemma2 : {t : Nat} -> {n : Nat} -> {x : State t} ->
>                Not ((outl x) `Prelude.Nat.LT` maxColumn) -> Viable (S n) x = Void
> viableLemma2 {t} {n} {x} prf with (decLT (outl x) maxColumn)
>   | (Yes p) = void (prf p)
>   | (No _) = Refl

> viableLemma : {t : Nat} -> {n : Nat} ->
>               (x : State t) ->
>               SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} n) (nexts t x Ahead)
> viableLemma {t} {n = Z} (MkSigma i prf) with (decLT i maxColumn)
>   | (Yes p) = res where
>     res : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} Z) [MkSigma i prf]
>     res = v :: Nil where
>       v : Viable {t = S t} Z (MkSigma i prf)
>       v with (decLT i maxColumn)
>         | (Yes _) = MkUnit
>         | (No  contra) = void (contra p)
>   | (No  _) = Nil
> viableLemma {t} {n = S m} (MkSigma i prf) with (decLT i maxColumn)
>   | (Yes p) = res where
>     res : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} (S m)) [MkSigma i prf]
>     res = v :: Nil where
>       v : Viable {t = S t} (S m) (MkSigma i prf)
>       v with (decLT i maxColumn)
>         | (Yes _) = MkUnit
>         | (No  contra) = void (contra p)
>   | (No  _) = Nil

> SequentialDecisionProblems.CoreTheory.viableSpec1 {t} {n} x v with (decLT (outl x) maxColumn)
>   | (Yes prf) = MkSigma Ahead (ne, av) where
>     ne : NotEmpty (nexts t x Ahead)
>     ne = nextsLemma1 x prf
>     av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} n) (nexts t x Ahead)
>     av = viableLemma x
>   | (No _) = void v

> SequentialDecisionProblems.Utils.finiteViable  Z    _ = finiteUnit
> SequentialDecisionProblems.Utils.finiteViable (S m) x with (decLT (outl x) maxColumn)
>   | (Yes p) = finiteUnit
>   | (No  c) = finiteVoid

> SequentialDecisionProblems.Utils.decidableViable  Z    _ = decidableUnit
> SequentialDecisionProblems.Utils.decidableViable (S m) x with (decLT (outl x) maxColumn)
>   | (Yes _) = decidableUnit
>   | (No  _) = decidableVoid

* The computation:

> SequentialDecisionProblems.Utils.showState = show @{ShowLTB}
> SequentialDecisionProblems.Utils.showCtrl = show

> computation : { [STDIO] } Eff ()
> computation =
>   do putStr ("enter number of steps:\n")
>      nSteps <- getNat
>      putStr ("enter initial column:\n")
>      x0 <- getLTB nColumns
>      case (decidableViable {t = Z} nSteps x0) of
>        (Yes v0) => do putStrLn ("computing optimal policies ...")
>                       ps   <- pure (tabTailRecursiveBackwardsInduction Z nSteps)
>                       putStrLn ("computing optimal controls ...")
>                       mxys <- pure (possibleStateCtrlSeqs x0 () v0 ps)
>                       putStrLn (show mxys)
>                       putStrLn ("done!")
>        (No _)   => putStrLn ("initial column non viable for " ++ cast {from = Int} (cast nSteps) ++ " steps")

> main : IO ()
> main = run computation

> {-

> ---}

-- Local Variables:
-- idris-packages: ("effects")
-- End:

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
import Data.Nat

p1_equals_s : (1+) = S
p1_equals_s = Refl

funext : {p, q : a -> b} -> ((x : a) -> p x = q x) -> p = q
funext _ = believe_me (Z = Z)

onep_equals_s : (+1) = S
onep_equals_s = funext \x => plusCommutative x 1

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


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

import Sif.Effs

import Sif.Error

-- TODO Make more robust by returning Maybe and Either
%access export

namespace Sif
  writeFile : String -> String -> Sif ()
  writeFile fname content = do
      trace $ unwords ["Writing file:", show fname]
      res <- File.writeFile (\x => CannotWriteFile x) fname content
      case res of
          Left  err => Sif.raise err
          Right _   => trace $ unwords ["Finished writing file,", show fname]

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
data Expr = Val Int
          | Mult Expr Expr
          | Add Expr Expr
          | Sub Expr Expr
%name Expr expr1, expr2

evaluate : Expr -> Int
evaluate (Val x) = x
evaluate (Mult expr1 expr2) = evaluate expr1 * evaluate expr2
evaluate (Add expr1 expr2) = evaluate expr1 + evaluate expr2
evaluate (Sub expr1 expr2) = evaluate expr1 - evaluate expr2


text:
module Data.Functor

%access public
%default total

-- class Functor (f : Type -> Type) where
--  map : (a -> b) -> f a -> f b

instance Functor (\a => c -> a) where
  map f g = f . g

-- FIXME:
-- instance Functor (\a => (a, c)) where
--   map f (x,y) = (f x, y)

-- instance Functor (Either a) where
--   map _ (Left x) = Left x
--   map f (Right x) = Rignt $ f x

-- functor_law_1: map id == id
-- functor_law_2: map (f.g) == map f . map g

class CoFunctor (f : Type -> Type) where
  map' : f b -> f a -> (b -> a)

-- contravariant_law1: contramap id == id
-- contravariant_law2: contramap (g.f) = contramap f . contramap g
class Contravariant (f : Type -> Type) where
  contramap : (a -> b) -> f b -> f a

instance Contravariant (\b => b -> c) where
  contramap f g = g . f

class CoContravariant (f : Type -> Type) where
  contramap' : f a -> f b -> (b -> a)

class Bifunctor (f : Type -> Type -> Type) where
  bimap : (a -> b) -> (c -> d) -> f a c -> f b d

instance Bifunctor Either where
  bimap f _ (Left x) = Left $ f x
  bimap _ g (Right x) = Right $ g x

class CoBifunctor (f : Type -> Type -> Type) where
  bimap' : f b d -> f a c -> (d -> c) -> (b -> a)

class Profunctor (f : Type -> Type -> Type) where
  dimap : (a -> b) -> (c -> d) -> f b c -> f a d

instance Profunctor (\b => \c => b -> c) where
  dimap f g h = g . h . f

class CoProfunctor (f : Type -> Type -> Type) where
  dimap' : f a d -> f b c -> (d -> c) -> (b -> a)

max_stars_repo_name: seagull-kamome/idris-toy

max_issues_repo_name: seagull-kamome/idris-toy

max_forks_repo_name: seagull-kamome/idris-toy


text:
module Main

import GRIN.AST


text:
module Excercise_4_2

import Data.Vect

data PowerSource = Petrol | Pedal | Electricity

data Vehicle : PowerSource -> Type where
     Bicycle : Vehicle Pedal
     Car : (fuel : Nat) -> Vehicle Petrol
     Bus : (fuel : Nat) -> Vehicle Petrol
     Unicycle : Vehicle Pedal
     Motorcyle : (fuel : Nat) -> Vehicle Petrol
     Tram : Vehicle Electricity

wheels : Vehicle power -> Nat
wheels Bicycle = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4
wheels Unicycle = 1
wheels (Motorcyle fuel) = 2
wheels Tram = 60

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200
refuel Bicycle impossible
refuel Unicycle impossible
refuel (Motorcyle fuel) = Motorcyle 50
refuel Tram impossible

vectTake : (n : Nat) -> Vect (n + m) e -> Vect n e
vectTake Z xs = []
vectTake (S k) (x :: xs) = x :: vectTake k xs

sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys = case integerToFin pos n of
                                Nothing => Nothing
                                Just idx => Just ((index idx xs) + (index idx ys))


text:
-- --------------------------------------------------------------- [ Model.idr ]
-- Module      : UML.Component.Model
-- Description :
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Component.Model

import UML.Code.Model

%access public

data ElemTy = INTERFACE | COMPONENT | MODEL

data ComponentModel : ElemTy -> Type where
    ||| Constructs an interface
    Actual : (name : String) -> (fns : List Function) -> ComponentModel INTERFACE
    ||| Construct a provided interface.
    Provided : (name : String) -> (origin : String) -> ComponentModel INTERFACE
    ||| Construct a required interface.
    Required : (name : String) -> (origin : String) -> ComponentModel INTERFACE

    ||| A component in the diagram.
    |||
    ||| @name The components name.
    ||| @is A list of interfaces.
    ||| @cs A list of possible sub components.
    MkComponent : (name : String)
               -> (is : List $ ComponentModel INTERFACE)
               -> (cs : List $ ComponentModel COMPONENT)
               -> ComponentModel COMPONENT

    ||| A Component diagram is just a list of components.
    MkComponentModel : (ds : DTypes)
                     -> (cs : List $ ComponentModel COMPONENT)
                     -> ComponentModel MODEL

-- ------------------------------------------------------------------ [ Equals ]

instance Eq ElemTy where
  (==) INTERFACE INTERFACE = True
  (==) COMPONENT COMPONENT = True
  (==) MODEL     MODEL     = True
  (==) _         _         = False

mutual

  %assert_total
  eqCompModel : (ComponentModel x) -> (ComponentModel x) -> Bool
  eqCompModel (Provided xn xo)         (Provided yn yo)         = xn == yn && xo == yo
  eqCompModel (Required xn xo)         (Required yn yo)         = xn == yn && xo == yo
  eqCompModel (Actual xn xf)           (Actual yn yf)           = xn == yn && xf == yf
  eqCompModel (MkComponent x xis xcs)  (MkComponent y yis ycs)  =  x == y && xis == yis && xcs == ycs
  eqCompModel (MkComponentModel xd xc) (MkComponentModel yd yc) = xd == yd && xc == yc
  eqCompModel _                     _                           = False

  instance Eq (ComponentModel x) where
    (==) = eqCompModel

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

instance Show ElemTy where
  show INTERFACE = "INTERFACE"
  show COMPONENT = "COMPONENT"
  show MODEL     = "MODEL"

instance Show (ComponentModel x) where
  show (Actual n fs)            = unwords ["[Interface", show n, show fs, "]\n"]
  show (Provided n o)           = unwords ["[Provides Interface", show n, show o, "]\n"]
  show (Required n o)           = unwords ["[Requires Interface", show n, show o, "]\n"]
  show (MkComponent n is cs)    = unwords ["[Component", show n, "\n\t", show is, "\n\t", show cs,"]\n"]
  show (MkComponentModel ds cs) = unwords ["[CompModel", "\n", show ds, "\n", show cs, "\n]"]

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

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module CatR

%default total

{- A category is very much like a graph. It has vertices
   named objects and vertices named arrows. Each arrow goes
   from an object to an object (possibly the same!). -}
record Cat (obj: Type) (arr: obj -> obj -> Type) where
  constructor MkCat

  {- For each object, there is an arrow called `id` which
  goes from the object to itself. -}
  id: {o: obj} -> arr o o

  {- Given an arrow `f` from object `a` to `b` and an arrow
      `g` from `b` to `c`. We can compose these arrow. The
      result is an arrow from `a` to `c`. -}
  compose: {a, b, c: obj} -> arr a b -> arr b c -> arr a c

  -- Here comes some properties of `id` and `compose`

  {- For any arrow `f`, compose id f = f -}
  neutralLeft:  {a, b: obj} -> (f: arr a b) -> compose id f = f

  {- For any arrow `f`, compose f id = f  -}
  neutralRight: {a, b: obj} -> (f: arr a b) -> compose f id = f

  {- For any arrows `f`, `g` and `h`,
    composing f with g, and then the result with h
    gives exatctly the same result as
    composing f with the result of the composition of g and h

    Which means, like string concatenation than we can commpose
    the way we preserve the order of each element in the sequence.-}
  associativity: {a, b, c, d: obj} ->
                  (f: arr a b) -> (g: arr b c) -> (h: arr c d) ->
                  compose f (compose g h) = compose (compose f g) h

{- `LE n m` encode the property that `n ≤ m`
    i.e. `n` is less or equal to `m` -}
data LE : Nat -> Nat -> Type where
  LERefl : {o: Nat} -> LE o o
  LENext : {a, b: Nat} -> LE a b -> LE a (S b)

{- Taking naturals as objects and `LE` as arrows,
   this actually forms a category! -}
natPoset : Cat Nat LE
natPoset = ???


text:
labelFrom : Integer -> List a -> List (Integer, a)
labelFrom lbl [] = []
labelFrom lbl (val :: vals) = (lbl, val) :: labelFrom (lbl + 1) vals

label : List a -> List (Integer, a)
label = labelFrom 0


text:
public export
data DataFrame a  = ?hole


text:
module Crypto.AES.Common

import Utils.ConstantTable
import Data.Bits
import Data.DPair
import Data.Fin
import Data.List
import Data.Nat
import Data.Stream
import Data.Vect
import Utils.Misc
import Utils.Bytes

export
matmul : Num a => {p : _} -> (op : Vect m a -> Vect m b -> c) -> Vect n (Vect m a) -> Vect m (Vect p b) -> Vect n (Vect p c)
matmul op [] ys = []
matmul op (x :: xs) ys = map (op x) (transpose ys) :: matmul op xs ys

export
vecxor : Bits a => Vect n a -> Vect n a -> Vect n a
vecxor = zipWith xor

export
matxor : Bits a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
matxor x y = zipWith vecxor x y

export
sbox : ConstantTable 256 Bits8
sbox = from_vect
  [ 0x63, 0x7c, 0x77, 0x7b, 0xf2, 0x6b, 0x6f, 0xc5, 0x30, 0x01, 0x67, 0x2b, 0xfe, 0xd7, 0xab, 0x76
  , 0xca, 0x82, 0xc9, 0x7d, 0xfa, 0x59, 0x47, 0xf0, 0xad, 0xd4, 0xa2, 0xaf, 0x9c, 0xa4, 0x72, 0xc0
  , 0xb7, 0xfd, 0x93, 0x26, 0x36, 0x3f, 0xf7, 0xcc, 0x34, 0xa5, 0xe5, 0xf1, 0x71, 0xd8, 0x31, 0x15
  , 0x04, 0xc7, 0x23, 0xc3, 0x18, 0x96, 0x05, 0x9a, 0x07, 0x12, 0x80, 0xe2, 0xeb, 0x27, 0xb2, 0x75
  , 0x09, 0x83, 0x2c, 0x1a, 0x1b, 0x6e, 0x5a, 0xa0, 0x52, 0x3b, 0xd6, 0xb3, 0x29, 0xe3, 0x2f, 0x84
  , 0x53, 0xd1, 0x00, 0xed, 0x20, 0xfc, 0xb1, 0x5b, 0x6a, 0xcb, 0xbe, 0x39, 0x4a, 0x4c, 0x58, 0xcf
  , 0xd0, 0xef, 0xaa, 0xfb, 0x43, 0x4d, 0x33, 0x85, 0x45, 0xf9, 0x02, 0x7f, 0x50, 0x3c, 0x9f, 0xa8
  , 0x51, 0xa3, 0x40, 0x8f, 0x92, 0x9d, 0x38, 0xf5, 0xbc, 0xb6, 0xda, 0x21, 0x10, 0xff, 0xf3, 0xd2
  , 0xcd, 0x0c, 0x13, 0xec, 0x5f, 0x97, 0x44, 0x17, 0xc4, 0xa7, 0x7e, 0x3d, 0x64, 0x5d, 0x19, 0x73
  , 0x60, 0x81, 0x4f, 0xdc, 0x22, 0x2a, 0x90, 0x88, 0x46, 0xee, 0xb8, 0x14, 0xde, 0x5e, 0x0b, 0xdb
  , 0xe0, 0x32, 0x3a, 0x0a, 0x49, 0x06, 0x24, 0x5c, 0xc2, 0xd3, 0xac, 0x62, 0x91, 0x95, 0xe4, 0x79
  , 0xe7, 0xc8, 0x37, 0x6d, 0x8d, 0xd5, 0x4e, 0xa9, 0x6c, 0x56, 0xf4, 0xea, 0x65, 0x7a, 0xae, 0x08
  , 0xba, 0x78, 0x25, 0x2e, 0x1c, 0xa6, 0xb4, 0xc6, 0xe8, 0xdd, 0x74, 0x1f, 0x4b, 0xbd, 0x8b, 0x8a
  , 0x70, 0x3e, 0xb5, 0x66, 0x48, 0x03, 0xf6, 0x0e, 0x61, 0x35, 0x57, 0xb9, 0x86, 0xc1, 0x1d, 0x9e
  , 0xe1, 0xf8, 0x98, 0x11, 0x69, 0xd9, 0x8e, 0x94, 0x9b, 0x1e, 0x87, 0xe9, 0xce, 0x55, 0x28, 0xdf
  , 0x8c, 0xa1, 0x89, 0x0d, 0xbf, 0xe6, 0x42, 0x68, 0x41, 0x99, 0x2d, 0x0f, 0xb0, 0x54, 0xbb, 0x16
  ]

export
inv_sbox : ConstantTable 256 Bits8
inv_sbox = from_vect
  [ 0x52, 0x09, 0x6a, 0xd5, 0x30, 0x36, 0xa5, 0x38, 0xbf, 0x40, 0xa3, 0x9e, 0x81, 0xf3, 0xd7, 0xfb
  , 0x7c, 0xe3, 0x39, 0x82, 0x9b, 0x2f, 0xff, 0x87, 0x34, 0x8e, 0x43, 0x44, 0xc4, 0xde, 0xe9, 0xcb
  , 0x54, 0x7b, 0x94, 0x32, 0xa6, 0xc2, 0x23, 0x3d, 0xee, 0x4c, 0x95, 0x0b, 0x42, 0xfa, 0xc3, 0x4e
  , 0x08, 0x2e, 0xa1, 0x66, 0x28, 0xd9, 0x24, 0xb2, 0x76, 0x5b, 0xa2, 0x49, 0x6d, 0x8b, 0xd1, 0x25
  , 0x72, 0xf8, 0xf6, 0x64, 0x86, 0x68, 0x98, 0x16, 0xd4, 0xa4, 0x5c, 0xcc, 0x5d, 0x65, 0xb6, 0x92
  , 0x6c, 0x70, 0x48, 0x50, 0xfd, 0xed, 0xb9, 0xda, 0x5e, 0x15, 0x46, 0x57, 0xa7, 0x8d, 0x9d, 0x84
  , 0x90, 0xd8, 0xab, 0x00, 0x8c, 0xbc, 0xd3, 0x0a, 0xf7, 0xe4, 0x58, 0x05, 0xb8, 0xb3, 0x45, 0x06
  , 0xd0, 0x2c, 0x1e, 0x8f, 0xca, 0x3f, 0x0f, 0x02, 0xc1, 0xaf, 0xbd, 0x03, 0x01, 0x13, 0x8a, 0x6b
  , 0x3a, 0x91, 0x11, 0x41, 0x4f, 0x67, 0xdc, 0xea, 0x97, 0xf2, 0xcf, 0xce, 0xf0, 0xb4, 0xe6, 0x73
  , 0x96, 0xac, 0x74, 0x22, 0xe7, 0xad, 0x35, 0x85, 0xe2, 0xf9, 0x37, 0xe8, 0x1c, 0x75, 0xdf, 0x6e
  , 0x47, 0xf1, 0x1a, 0x71, 0x1d, 0x29, 0xc5, 0x89, 0x6f, 0xb7, 0x62, 0x0e, 0xaa, 0x18, 0xbe, 0x1b
  , 0xfc, 0x56, 0x3e, 0x4b, 0xc6, 0xd2, 0x79, 0x20, 0x9a, 0xdb, 0xc0, 0xfe, 0x78, 0xcd, 0x5a, 0xf4
  , 0x1f, 0xdd, 0xa8, 0x33, 0x88, 0x07, 0xc7, 0x31, 0xb1, 0x12, 0x10, 0x59, 0x27, 0x80, 0xec, 0x5f
  , 0x60, 0x51, 0x7f, 0xa9, 0x19, 0xb5, 0x4a, 0x0d, 0x2d, 0xe5, 0x7a, 0x9f, 0x93, 0xc9, 0x9c, 0xef
  , 0xa0, 0xe0, 0x3b, 0x4d, 0xae, 0x2a, 0xf5, 0xb0, 0xc8, 0xeb, 0xbb, 0x3c, 0x83, 0x53, 0x99, 0x61
  , 0x17, 0x2b, 0x04, 0x7e, 0xba, 0x77, 0xd6, 0x26, 0xe1, 0x69, 0x14, 0x63, 0x55, 0x21, 0x0c, 0x7d
  ]

export
sub_byte : Bits8 -> Bits8
sub_byte x = index_bits8 x sbox

export
inv_sub_byte : Bits8 -> Bits8
inv_sub_byte x = index_bits8 x inv_sbox

export
sub_word : Vect m Bits8 -> Vect m Bits8
sub_word = map sub_byte

export
inv_sub_word : Vect m Bits8 -> Vect m Bits8
inv_sub_word = map inv_sub_byte

export
sub_bytes : Vect n (Vect m Bits8) -> Vect n (Vect m Bits8)
sub_bytes = map sub_word

export
inv_sub_bytes : Vect n (Vect m Bits8) -> Vect n (Vect m Bits8)
inv_sub_bytes = map inv_sub_word

export
rot_word : {n : Nat} -> Nat -> Vect (S n) a -> Vect (S n) a
rot_word k = take (S n) . drop k . cycle

export
inv_rot_word : {n : Nat} -> Nat -> Vect (S n) a -> Vect (S n) a
inv_rot_word k = take (S n) . drop (n * k) . cycle

export
rcons : Stream Bits8
rcons = go 1
  where
  go : Bits8 -> Stream Bits8
  go x = x :: go ((if x < 0x80 then id else xor (0x1B)) $ 2 * x)

export
expand_key' : {n_k, n_b : _} -> {auto 0 ok : NonZero n_b} -> Fin n_k -> (rcs : Stream Bits8) -> (prev_block : Vect n_k (Vect n_b Bits8)) -> Stream (Vect n_b Bits8)
expand_key' {n_b = S n_b'} counter (rc :: rcs) (x :: xs) =
  let
    y = last (x :: xs)
  in
    case counter of
      FZ => let z = (vecxor (rc :: replicate _ 0) $ vecxor x $ sub_word $ rot_word 1 $ y) in z :: expand_key' Data.Fin.last rcs (snoc xs z)
      (FS counter') =>
        let
          z = vecxor x $ case isLT 6 n_k of
            Yes wit => if finToNat (FS counter') == 4 then sub_word y else y
            No contra => y
        in
          z :: expand_key' (weaken counter') (rc :: rcs) (snoc xs z)

export
expand_key : {n_k, n_b : _} -> {auto 0 ok : NonZero n_b} -> {auto 0 ok2 : NonZero n_k} -> Vect n_k (Vect n_b Bits8) -> Stream (Vect n_b Bits8)
expand_key {n_k = S n_k'} k = expand_key' FZ rcons k

public export
data Mode : Type where
  AES128 : Mode
  AES192 : Mode
  AES256 : Mode

public export
get_n_k : Mode -> Nat
get_n_k AES128 = 4
get_n_k AES192 = 6
get_n_k AES256 = 8

public export
n_k_never_Z : (mode : _) -> NonZero (get_n_k mode)
n_k_never_Z AES128 = SIsNonZero
n_k_never_Z AES192 = SIsNonZero
n_k_never_Z AES256 = SIsNonZero

public export
get_main_rounds : Mode -> Nat
get_main_rounds AES128 = 9
get_main_rounds AES192 = 11
get_main_rounds AES256 = 13


text:
data Baz : Int -> Type where
     AddThings : (x : Int) -> (y : Int) -> Baz (x + y)

addBaz : (x : Int) -> Baz x -> Int
addBaz (x + y) (AddThings x z) = x + y


text:
module TyTTP.HTTP.Producer

import Data.Buffer.Ext
import TyTTP
import TyTTP.HTTP

export
text :
  Applicative m
  => String
  -> Step me u h1 s StringHeaders a b
  -> m $ Step me u h1 s StringHeaders a (Publisher IO e Buffer)
text str step = do
  let stream : Publisher IO e Buffer = Stream.singleton $ fromString str
  pure $ { response.body := stream
         , response.headers :=
           [ ("Content-Type", "text/plain")
           , ("Content-Length", show $ length str)
           ]
         } step

export
status :
  Applicative m
  => Status
  -> Step me u h1 s h2 a b
  -> m $ Step me u h1 Status h2 a b
status s step = pure $ { response.status := s } step

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Z

import X
--import Y

g : Int
g = f 5


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/modules.html#memories
module WebAssembly.Structure.Modules.Memories

import WebAssembly.Structure.Types

import Decidable.Equality

-- Definition

public export
record Mem where
  constructor MkMem
  type : MemType

-- Equality

total public export
lemma_mem__type_injective : ((m1 = m2) -> Void) -> (MkMem m1 = MkMem m2) -> Void
lemma_mem__type_injective m1_not_m2 Refl = m1_not_m2 Refl

-- Decidable Equality

public export
implementation DecEq Mem where
  decEq (MkMem m1) (MkMem m2) = case decEq m1 m2 of
    No m1_not_m2 => No $ lemma_mem__type_injective m1_not_m2
    Yes Refl     => Yes Refl


text:
module Vec

import Data.Fin

%default total

%logging 1
%logging declare.def 2

Vec : Type -> Nat -> Type
Vec a n = Fin n -> a

Nil : Vec a Z
Nil = absurd

(::) : a -> Vec a n -> Vec a (S n)
(x :: xs) FZ = x
(x :: xs) (FS i) = xs i

test : Vec (List Nat) 2
test = [[], [0]]