text:
module Fahr

%foreign "C:printFahr,libfahr"
printFahr : PrimIO ()

%foreign "C:printCelsius,libfahr"
printCelsius : PrimIO ()

main : IO ()
main = do primIO printFahr
          putStrLn ""
          primIO printCelsius

ext: idr


text:
module Protocol
import Data.List

%access public export
%default total

-- A Choice is a type representing a discrete set of choices.
data Choice : List a -> Type
where Choose : (x : a) ->
               {xs : List a} ->
               {auto p : Elem x xs} ->
               Choice xs

-- Read a list of pairs from a file.
readSteps : String -> IO (Either FileError (List (String, String)))
readSteps filename =
  do result <- readFile filename
     pure $ map (pair . words) result
  where pair : List String -> List (String, String)
        pair (x1::x2::xs) = (x1, x2)::(pair xs)
        pair _ = []

-- Deconstruct a step into its states.
single : (xs : List (String, String)) -> (Choice xs) -> (String, String)
single _ (Choose x) = x

-- Use the allowed steps to define a finite state machine type.
data Path : (step : Type) -> (convert : (step -> (String, String))) -> Type -> (String, String) -> Type
where
  Begin : Path step convert () (state, state)
  Then  : (s : step) -> Path step convert () (convert s)
  (>>=) : Path step convert a (s1, s2) ->
          (a -> Path step convert b (s2, s3)) ->
          Path step convert b (s1, s3)

-- A type provider providing a list of steps.
Protocol : String -> IO (Provider ((String, String) -> Type))
Protocol filename =
  do result <- readSteps filename
     pure $
       case result of
         Left error => Error $ "Unable to read steps file: " ++ filename
         Right steps => Provide $ Path (Choice steps) (single steps) ()

max_stars_repo_name: ctford/elba

max_issues_repo_name: ctford/elba

max_forks_repo_name: ctford/elba


text:
import Effects
import Effect.Exception
import Effect.StdIO
import Effect.Random
import Effect.System
import Data.Vect

%default total

--------------------------------------------------------------------------------
-- Operations on individual rows
--------------------------------------------------------------------------------

||| Fills in an array
fillIn : LTE n m -> a -> Vect n a -> Vect m a
fillIn LTEZero c []            = replicate _ c
fillIn (LTESucc w) c (x :: xs) = x :: (fillIn w c xs)

||| Filters out the Nothings from a vector of maybes.
|||
||| Takes a vector of length n with elements of type Maybe a
||| and returns the dependent pair (m ** (Vect m a, LTE m n)) where
||| m is the new length, Vect m a is the filtered list, and LTE m n
||| is a prove that m <= n, that is, that the new list has length
||| less than or equal to the original list.
filterMaybes : Vect n (Maybe a) -> (m ** (Vect m a, LTE m n))
filterMaybes []              = (Z ** ([], LTEZero))
filterMaybes (Just x :: xs)  = let (_ ** (ys, w)) = filterMaybes xs in
  (_ ** ((x :: ys), LTESucc w))
filterMaybes (Nothing :: xs) = let (_ ** (ys, w)) = filterMaybes xs in
  (_ ** (ys, lteSuccRight w))

||| The collapsing of pairs operation of the 2048 game.
|||
||| Takes a vector of elements of type a, and performs the "collapsing"
||| operation of the 2048 game.  This takes adjacent pairs, and if they
||| are equal, combines them into a single element with double the value.
||| Returns a vector of length m and proof that m <= n.
collapsePairs : (Num a, Eq a) => Vect n a -> (m ** (Vect m a, LTE m n))
collapsePairs (x::x'::xs) =
  if x == x' then
    let (_ ** (ys, w)) = collapsePairs xs in (_ ** ((2 * x) :: ys, lteSuccRight (LTESucc w)))
  else
    let (_ ** (ys, w)) = collapsePairs (x' :: xs) in (_ ** (x :: ys, LTESucc w))
collapsePairs (x::[])     = (_ ** ([x], LTESucc LTEZero))
collapsePairs []          = (_ ** ([], LTEZero))

||| The basic row operation of the 2048 game.
|||
||| Combines the operations of filterMaybes and collapsePairs,
||| and combines their proofs, and transitivity of <=, to
||| prove that the result of applying both operations is
||| a shorter vector than the original.  This proof is used
||| to apply the fillIn function.
basicRowOperation : (Eq a, Num a) => Vect n (Maybe a) -> Vect n (Maybe a)
basicRowOperation xs = let (m ** (ys, w)) = filterMaybes xs in let
  (l ** (zs, wPrime)) = collapsePairs ys in
  (fillIn (lteTransitive wPrime w) Nothing (map Just zs))

--------------------------------------------------------------------------------
-- Operations on the game board
--------------------------------------------------------------------------------

||| Takes the transpose of a rectangular array
transposeArray : Vect n (Vect m a) -> Vect m (Vect n a)
transposeArray []      = replicate _ []
transposeArray (x::xs) = zipWith (::) x (transposeArray xs)

||| Flattens a rectangular array
flattenArray : Vect n (Vect m a) -> Vect (n * m) a
flattenArray Nil     = Nil
flattenArray (x::xs) = x ++ (flattenArray xs)

||| Splits an array
split' : Vect (plus n m) a -> (Vect n a, Vect m a)
split' {n=Z} xs                = ([], xs)
split' {n=(S k)}{m=l} (x::xs) = let (ys, zs) = split' {n=k}{m=l} xs in
  (x::ys, zs)

||| Unflattens an array
unFlattenArray : Vect (n * m) a -> Vect n (Vect m a)
unFlattenArray {n=Z} Nil         = Nil
unFlattenArray {n=(S k)}{m=l} xs = let (ys, zs) = split' {n=l}{m=k*l} xs in
  (ys :: (unFlattenArray zs))

||| Find the indices of all elements of a vector that satisfy some test
findIndicesFin : (a -> Bool) -> Vect n a -> List (Fin n)
findIndicesFin f [] = []
findIndicesFin f (x::xs) = let tail = (map FS (findIndicesFin f xs)) in
  if f x then (FZ :: tail) else tail

--------------------------------------------------------------------------------
-- Display functions
--------------------------------------------------------------------------------

showValue : Show a => Maybe a -> String
showValue Nothing  = "...."
showValue (Just x) = pack (List.take 4 (unpack ((show x) ++ "....")))

showRow : Show a => Vect n (Maybe a) -> String
showRow []      = ""
showRow (x::xs) = (showValue x) ++ " " ++ (showRow xs)

showBoard : Show a => Vect m (Vect n (Maybe a)) -> String
showBoard []      = ""
showBoard (x::xs) = (showRow x) ++ "\n" ++ (showBoard xs)

--------------------------------------------------------------------------------
-- High level game logic
--------------------------------------------------------------------------------

Board : Type
Board = Vect 4 (Vect 4 (Maybe Int))

data Direction = Left | Right | Up | Down

partial
move : (Eq a, Num a) => Direction -> Vect m (Vect n (Maybe a)) -> Vect m (Vect n (Maybe a))
move Left  xs = map basicRowOperation xs
move Right xs = map (reverse . basicRowOperation . reverse) xs
move Up    xs = (transposeArray . (move Left) . transposeArray) xs
move Down  xs = (transposeArray . (move Right) . transposeArray) xs

-- myIndex : List (Fin 16) -> Maybe Nat
-- myIndex lst =
addRandomPiece : Board -> {[RND, EXCEPTION String]} Eff Board
addRandomPiece arr =
  case integerToFin 3 16 of
    Nothing => raise "Game Over"
    Just idx => pure (unFlattenArray (replaceAt idx (Just 2) flattened))
  where
    flattened : Vect 16 (Maybe Int)
    flattened = flattenArray arr
    indices : List (Fin 16)
    indices = findIndicesFin isNothing flattened

data UserAction = Quit | Invalid | Move Direction

getAction : Char -> UserAction
getAction 'a' = Move Left
getAction 'd' = Move Right
getAction 'w' = Move Up
getAction 's' = Move Down
getAction 'x' = Quit
getAction _   = Invalid

partial
mainLoop : Board -> {[RND, STDIO, EXCEPTION String]} Eff (Board)
mainLoop b = do putStrLn (showBoard b)
                c <- getChar
                performAction (getAction c)
    where
      partial
      performAction : UserAction -> {[RND, STDIO, EXCEPTION String]} Eff (Board)
      performAction Quit       = raise "You have quit"
      performAction Invalid    = mainLoop b
      performAction (Move dir) = let b' = move dir b in
        if b == b' then
          mainLoop b'
        else
          do
            b'' <- addRandomPiece b'
            mainLoop b''

partial
startGame : { [RND, STDIO, SYSTEM, EXCEPTION String] } Eff ()
startGame = do
  srand !time
  initialBoard <- addRandomPiece (replicate _ (replicate _ Nothing))
  mainLoop initialBoard
  pure ()

partial
main : IO ()
main = run startGame


text:
import Language.Reflection

%language ElabReflection

logPrims : Elab a
logPrims
    = do ns <- getType `{ (++) }
         traverse_ (\ (n, ty) =>
                        do logMsg "" 0 ("Name: " ++ show n)
                           logTerm "" 0 "Type" ty) ns
         fail "Not really trying"

logDataCons : Elab a
logDataCons
    = do [(n, _)] <- getType `{ Nat }
             | _ => fail "Ambiguous name"
         logMsg "" 0 ("Resolved name: " ++ show n)
         logMsg "" 0 ("Constructors: " ++ show !(getCons n))
         fail "Still not trying"

logBad : Elab a
logBad
    = do [(n, _)] <- getType `{ DoesntExist }
             | [] => fail "Undefined name"
             | _ => fail "Ambiguous name"
         logMsg "" 0 ("Resolved name: " ++ show n)
         logMsg "" 0 ("Constructors: " ++ show !(getCons n))
         fail "Still not trying"

-- because the exact sequence number in a gensym depends on
-- the library and compiler internals we need to censor it so the
-- output won't be overly dependent on the exact versions used.
censorDigits : String -> String
censorDigits str = pack $ map (\c => if isDigit c then 'X' else c) (unpack str)

tryGenSym : Elab a
tryGenSym
   = do n <- genSym "plus"
        ns <- inCurrentNS n
        fail $ "failed after generating " ++ censorDigits (show ns)

dummy1 : a
dummy1 = %runElab logPrims

dummy2 : a
dummy2 = %runElab logDataCons

dummy3 : a
dummy3 = %runElab logBad

dummy4 : a
dummy4 = %runElab tryGenSym


text:
||| Division theorem for (type-level) natural number division
module Data.Nat.Division

import Syntax.WithProof
import Syntax.PreorderReasoning
import Syntax.PreorderReasoning.Generic
import Data.Nat
import Data.Nat.Equational
import Data.Nat.Order
import Data.Nat.Order.Strict
import Data.Nat.Order.Properties
import Decidable.Order.Strict

import Data.Nat.Properties

%default total

-- Division theorem --------------------

-- This is disgusting, but will do for now
||| Show that, if we have enough fuel, we have enough fuel for the
||| recursive call in `div'` and `mod'`.
fuelLemma : (numer, predDenom, fuel : Nat)
          -> (enough : numer `LTE` (S fuel))
          -> (recurse : Data.Nat.lte numer predDenom = False)
          -> (numer `minus` (S predDenom)) `LTE` fuel
fuelLemma numer predDenom fuel enough recurse =
  let denom  : Nat
      denom = S predDenom
      numer' : Nat
      numer' = numer `minus` denom
      -- a bunch of inequational reasoning to show we have enough fuel
      -- on the recursive call
      denom_lte_numer : denom `LTE` numer
      denom_lte_numer = Properties.notlteIsLT numer predDenom recurse
      numer'_lt_numer : numer' `LT` numer
      numer'_lt_numer = (minusPosLT denom numer
                          (LTESucc LTEZero)
                          denom_lte_numer)
      succenough : S numer' `LTE` S fuel
      succenough = transitive {rel = LTE} numer'_lt_numer enough
  in fromLteSucc succenough

-- equivalence between the duplicate definitions in Data.Nar  ---

-- Internally, we use the two component definitions of divmod'
div'' : (fuel, numer, denom : Nat) -> Nat
div'' fuel numer denom = fst (divmod' fuel numer denom)

mod'' : (fuel, numer, denom : Nat) -> Nat
mod'' fuel numer denom = snd (divmod' fuel numer denom)

divmod'_eq_div'_mod' : (fuel, numer, denom : Nat)
            -> (divmod' fuel numer denom) = (div' fuel numer denom, mod' fuel numer denom)
divmod'_eq_div'_mod'   0       numer denom = Refl
divmod'_eq_div'_mod'  (S fuel) numer denom with (Data.Nat.lte numer denom)
 divmod'_eq_div'_mod' (S fuel) numer denom | True  = Refl
 divmod'_eq_div'_mod' (S fuel) numer denom | False =
   rewrite divmod'_eq_div'_mod' fuel (numer `minus` (S denom)) denom in
   Refl

div''_eq_div' : (fuel, numer, denom : Nat)
            -> div'' fuel numer denom = div' fuel numer denom
div''_eq_div' fuel numer denom = cong fst $
                                       divmod'_eq_div'_mod' fuel numer denom

mod''_eq_mod' : (fuel, numer, denom : Nat)
            -> mod'' fuel numer denom = mod' fuel numer denom
mod''_eq_mod' fuel numer denom = cong snd $
                                       divmod'_eq_div'_mod' fuel numer denom

export
divmodNatNZeqDivMod : (numer, denom : Nat) -> (0 prf1, prf2, prf3 : NonZero denom)
            -> (divmodNatNZ numer denom prf1) = (divNatNZ numer denom prf2, modNatNZ numer denom prf3)
divmodNatNZeqDivMod numer (S denom) prf1 prf2 prf3 = divmod'_eq_div'_mod' numer numer denom

export
fstDivmodNatNZeqDiv : (numer, denom : Nat) -> (0 prf1, prf2 : NonZero denom)
            -> (fst $ divmodNatNZ numer denom prf1) = divNatNZ numer denom prf2
fstDivmodNatNZeqDiv numer denom prf1 prf2 =
  rewrite divmodNatNZeqDivMod numer denom prf1 prf2 prf2 in
  Refl

export
sndDivmodNatNZeqMod : (numer, denom : Nat) -> (0 prf1, prf2 : NonZero denom)
            -> (snd $ divmodNatNZ numer denom prf1) = modNatNZ numer denom prf2
sndDivmodNatNZeqMod numer denom prf1 prf2 =
  rewrite divmodNatNZeqDivMod numer denom prf1 prf2 prf2 in
  Refl

-----------------------------------------------------------------------------
bound_mod'' : (fuel, numer, predDenom : Nat) -> (numer `LTE` fuel)
           -> (mod'' fuel numer predDenom) `LTE` predDenom
bound_mod'' 0        0     predDenom LTEZero = LTEZero
bound_mod'' (S fuel) numer predDenom enough  = case @@(Data.Nat.lte numer predDenom) of
  (True  ** numer_lte_predn)  => rewrite numer_lte_predn in
                                 Properties.lteIsLTE _ _ numer_lte_predn
  (False ** numer_gte_n    )  => rewrite numer_gte_n in
                                 bound_mod'' fuel (numer `minus` (S predDenom)) predDenom
                                                  (fuelLemma numer predDenom fuel enough numer_gte_n)

export
boundModNatNZ : (numer, denom : Nat) -> (0 denom_nz : NonZero denom)
              -> (modNatNZ numer denom denom_nz) `LT` denom
boundModNatNZ numer (S predDenom) denom_nz =
  LTESucc $
    rewrite sym $ mod''_eq_mod' numer numer predDenom in
      bound_mod'' numer numer predDenom $ reflexive {rel = LTE}
divisionTheorem' : (numer, predDenom : Nat)
                -> (fuel : Nat) -> (enough : numer `LTE` fuel)
                -> numer = (mod'' fuel numer predDenom) + (div'' fuel numer predDenom) * (S predDenom)

divisionTheorem'  0     predDenom  0       LTEZero = Refl
divisionTheorem'  numer predDenom (S fuel) enough with (@@(Data.Nat.lte numer predDenom))
 divisionTheorem' numer predDenom (S fuel) enough | (True ** prf)
   = rewrite prf in
     rewrite plusZeroRightNeutral numer in Refl
 divisionTheorem' numer predDenom (S fuel) enough | (False ** prf)
   = rewrite prf in
     let denom  : Nat
         denom = S predDenom
         numer' : Nat
         numer' = numer `minus` denom
         denom_lte_numer : denom `LTE` numer
         denom_lte_numer = Properties.notlteIsLT numer predDenom prf
         enough' : numer' `LTE` fuel
         enough' = fuelLemma numer predDenom fuel enough prf

         inductionHypothesis : (numer'
                             = (mod'' fuel numer' predDenom) +  (div'' fuel numer' predDenom) * denom)
         inductionHypothesis = divisionTheorem' numer' predDenom fuel enough'
     in sym $ Calc $
     |~ (mod'' fuel numer' predDenom) + (denom + (div'' fuel numer' predDenom) * denom)
     ~~ (mod'' fuel numer' predDenom) + ((div'' fuel numer' predDenom) * denom + denom)
               ...(cong ((mod'' fuel numer' predDenom) +) $ plusCommutative
                                                            denom
                                                            ((div'' fuel numer' predDenom) * denom))
     ~~((mod'' fuel numer' predDenom) +  (div'' fuel numer' predDenom) * denom) + denom
               ...(plusAssociative
                     (mod'' fuel numer' predDenom)
                     ((div'' fuel numer' predDenom) * denom)
                     denom)
     ~~ numer' + denom ...(cong (+ denom) $ sym inductionHypothesis)
     ~~ numer ...(plusMinusLte denom numer denom_lte_numer)

export
DivisionTheoremDivMod : (numer, denom : Nat)  -> (0 prf : NonZero denom)
               -> numer = snd ( divmodNatNZ numer denom prf)
                       + (fst $ divmodNatNZ numer denom prf)*denom
DivisionTheoremDivMod numer (S predDenom) prf
  = divisionTheorem' numer predDenom numer $ reflexive {rel = LTE}

export
DivisionTheorem : (numer, denom : Nat) -> (0 prf1, prf2 : NonZero denom)
               -> numer = (modNatNZ numer denom prf1) + (divNatNZ numer denom prf2)*denom
DivisionTheorem numer denom prf1 prf2
  = rewrite sym $ fstDivmodNatNZeqDiv numer denom prf1 prf2 in
    rewrite sym $ sndDivmodNatNZeqMod numer denom prf1 prf1 in
    DivisionTheoremDivMod numer denom prf1

divmodZeroZero : (denom, fuel : Nat)
           -> divmod' fuel 0 denom = (0,0)
divmodZeroZero denom  0       = Refl
divmodZeroZero denom (S fuel) = Refl

modZeroZero : (denom, fuel : Nat)
           -> mod'' fuel 0 denom = 0
modZeroZero denom fuel = rewrite divmodZeroZero denom fuel in Refl

divZeroZero : (denom, fuel : Nat)
           -> div'' fuel 0 denom = 0
divZeroZero denom fuel = rewrite divmodZeroZero denom fuel in Refl

divmodFuelLemma : (numer, denom, fuel1, fuel2 : Nat)
            -> (enough1 : fuel1 `GTE` numer)
            -> (enough2 : fuel2 `GTE` numer)
            -> divmod' fuel1 numer denom = divmod' fuel2 numer denom
divmodFuelLemma  0 denom 0 fuel2 LTEZero enough2 = rewrite divmodZeroZero denom fuel2 in
                                                Refl
divmodFuelLemma  0 denom (S fuel1) 0 enough1 LTEZero = Refl
divmodFuelLemma  numer denom (S fuel1) (S fuel2) enough1 enough2 with (@@(Data.Nat.lte numer denom))
 divmodFuelLemma numer denom (S fuel1) (S fuel2) enough1 enough2 | (True  ** prf)  =
   rewrite prf in Refl
 divmodFuelLemma numer denom (S fuel1) (S fuel2) enough1 enough2 | (False ** prf) =
   rewrite prf in
   rewrite divmodFuelLemma (numer `minus` (S denom)) denom fuel1 fuel2
             (fuelLemma numer denom fuel1 enough1 prf)
             (fuelLemma numer denom fuel2 enough2 prf) in
   Refl

multiplicationLemma : (q, predn, r : Nat) -> q * (S predn) + r `LTE` 0 -> (q = 0, r = 0)
multiplicationLemma q predn r bound =
  let r_eq_z : (r = 0)
      r_eq_z = zeroPlusRightZero (q * (S predn)) r (sym $ lteZeroIsZero bound)
      qn_eq_z : (q * (S predn) = 0)
      qn_eq_z = zeroPlusLeftZero (q * (S predn)) r (sym $ lteZeroIsZero bound)
      q_eq_z : q = 0
      q_eq_z = case zeroMultEitherZero q (S predn) qn_eq_z of
        Left  q_eq_0 => q_eq_0
        Right spred_eq_z impossible
  in (q_eq_z, r_eq_z)

multiplesModuloZero : (fuel, predn, k : Nat)
       -> (enough : fuel `GTE` k * (S predn) )
       -> mod' fuel (k * (S predn)) predn = 0
multiplesModuloZero 0        predn k enough =
  let (k_eq_z, _) = multiplicationLemma k predn 0 $
                    rewrite plusZeroRightNeutral (k * (S predn)) in
                    enough
  in rewrite k_eq_z in
  Refl
multiplesModuloZero  (S fuel) predn 0 enough = Refl
multiplesModuloZero  (S fuel) predn (S k) enough =
  let n : Nat
      n = S predn
      n_lte_skn : n `LTE` (1 + k)*n
      n_lte_skn = CalcWith {leq = LTE} $
        |~ n
        ~~ n  + 0     ...(sym $ plusZeroRightNeutral n)
        ~~ (1 + 0)*n ...(Refl)
        <~ (1 + k)*n   ...(multLteMonotoneLeft (1+0) (1+k) n $
                           plusLteMonotoneLeft 1 0 k LTEZero)
  in case @@(Data.Nat.lte ((1 + k)*n) predn) of
    (True  ** skn_lte_predn) => absurd $ irreflexive {rel = Data.Nat.LT}
                                       $ CalcWith {leq = LTE} $
      |~ 1 + predn
      ~~ n         ...(Refl)
      ~~ n + 0     ...(sym $ plusZeroRightNeutral n)
      ~~ (1 + 0)*n ...(Refl)
      <~ (1 + k)*n ...(multLteMonotoneLeft (1+0) (1+k) n $
                       LTESucc LTEZero)
      <~ predn     ...(Properties.lteIsLTE _ _ skn_lte_predn)
    (False ** prf) =>
      rewrite prf in
      let skn_minus_n_eq_kn : ((1 + k)*n `minus` n = k*n)
          skn_minus_n_eq_kn = Calc $
            |~ ((1+k)*n `minus` n)
            ~~ ((1+k)*n `minus` (n + 0)) ...(cong ((1+k)*n `minus`) $ sym $ plusZeroRightNeutral n)
            ~~ (n + k*n `minus` (n + 0)) ...(Refl)
            ~~ (k*n `minus` 0)           ...(plusMinusLeftCancel n (k*n) 0)
            ~~ k*n                       ...(minusZeroRight (k*n))
      in rewrite skn_minus_n_eq_kn in
      multiplesModuloZero fuel predn k $
      (rewrite sym $ skn_minus_n_eq_kn in
       fuelLemma ((1 + k)*n) predn fuel enough prf)

-- We also want to show uniqueness of this decomposition
-- This is, of course, quite horrible, but I want this theorem in the stdlib
addMultipleMod': (fuel1, fuel2, predn, a, b : Nat) -> (enough1 : fuel1 `GTE` b * (S predn) + a)
                                           -> (enough2 : fuel2 `GTE` a)
       -> mod'' fuel1 (b * (S predn) + a) predn = mod'' fuel2 a predn
addMultipleMod' 0         fuel2 predn a b enough1 enough2
  = let (b_eq_z, a_eq_z) = multiplicationLemma b predn a enough1
    in rewrite a_eq_z in
       rewrite b_eq_z in
       rewrite modZeroZero predn fuel2 in
       Refl
addMultipleMod' fuel1@(S _) fuel2 predn a 0 enough1 enough2 =
  rewrite divmodFuelLemma a predn fuel1 fuel2 enough1 enough2 in
  Refl
addMultipleMod' (S fuel1) fuel2 predn a (S k) enough1 enough2 =
  let n : Nat
      n = S predn
      lhsarg_geq_predn : ((1 + k)*n + a) `GT` predn
      lhsarg_geq_predn = CalcWith {leq = LTE} $
        |~ n
        ~~ (1+0)*n     ...(sym $ plusZeroRightNeutral n)
        <~ (1+k)*n     ...(multLteMonotoneLeft 1 (1+k) n $
                           LTESucc LTEZero)
        <~ (1+k)*n + a ...(lteAddRight $ (1+k)*n)
      prf1 : lte ((1 + k)*n + a) predn = False
      prf1 = GTIsnotlte ((1 + k)*n + a) predn lhsarg_geq_predn
      argsimplify : (((1 + k) *n + a ) `minus` n = k*n + a)
      argsimplify = Calc $
        |~ (((1+k)*n + a) `minus` n)
        ~~ (((n + k*n) + a) `minus` n)       ...(Refl)
        ~~ ((n + (k*n + a)) `minus` (n + 0)) ...(cong2 minus
                                                   (sym $ plusAssociative n (k*n) a)
                                                   (sym $ plusZeroRightNeutral n))
        ~~ ((k*n + a) `minus` 0)             ...(plusMinusLeftCancel n (k*n + a) 0)
        ~~ k*n + a                           ...(minusZeroRight (k*n + a))
  in rewrite prf1 in
     rewrite argsimplify in
     addMultipleMod' fuel1 fuel2 predn a k
       (rewrite sym argsimplify in
        fuelLemma ((1+k)*n + a) predn fuel1 enough1 prf1)
       enough2

addMultipleMod : (a, b, n : Nat) -> (0 n_neq_z1, n_neq_z2 : NonZero n)
              -> snd (divmodNatNZ (a*n + b) n n_neq_z1) = snd (divmodNatNZ b n n_neq_z2)
addMultipleMod a b n@(S predn) n_neq_z1  n_neq_z2 =
  addMultipleMod' (a*n + b) b predn b a (reflexive {rel = LTE}) (reflexive {rel = LTE})

modBelowDenom : (r, n : Nat) -> (0 n_neq_z : NonZero n)
             -> (r `LT` n)
             -> snd (divmodNatNZ r n n_neq_z)  = r
modBelowDenom 0 (S predn) n_neq_0 (LTESucc r_lte_predn) = Refl
modBelowDenom r@(S _) (S predn) n_neq_0 (LTESucc r_lte_predn) =
  rewrite LteIslte r predn r_lte_predn in
  Refl

modInjective : (r1, r2, n : Nat) -> (0 n_neq_z1, n_neq_z2 : NonZero n)
             -> (r1 `LT` n)
             -> (r2 `LT` n)
             -> snd (divmodNatNZ r1 n n_neq_z1)  = snd (divmodNatNZ r2 n n_neq_z2)
             -> r1 = r2
modInjective r1 r2 n n_neq_z1 n_neq_z2 r1_lt_n r2_lt_n ri_mod_eq = Calc $
  |~ r1
  ~~ snd (divmodNatNZ r1 n n_neq_z1) ...(sym $ modBelowDenom r1 n n_neq_z1 r1_lt_n)
  ~~ snd (divmodNatNZ r2 n n_neq_z2) ...(ri_mod_eq)
  ~~ r2                              ...(      modBelowDenom r2 n n_neq_z2 r2_lt_n)

step1 : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom)
     -> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
     -> snd (divmodNatNZ numer denom denom_nz) = r
step1 x n n_nz q r r_lt_n x_eq_qnpr = Calc $
  |~ snd(divmodNatNZ x         n n_nz)
  ~~ snd(divmodNatNZ (q*n + r) n n_nz) ...(cong (\u => snd $ divmodNatNZ u n n_nz) $ x_eq_qnpr)
  ~~ snd(divmodNatNZ r         n n_nz) ...(addMultipleMod q r n n_nz n_nz)
  ~~ r                                 ...(modBelowDenom r n n_nz r_lt_n)

step2 : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom)
     -> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
     -> fst (divmodNatNZ numer denom denom_nz) = q
step2 x n n_nz q r r_lt_n x_eq_qnr =
  let mod_eq_r : (snd (divmodNatNZ x n n_nz) = r)
      mod_eq_r = step1 x n n_nz q r r_lt_n x_eq_qnr

      two_decompositions : (fst $ divmodNatNZ x n n_nz) * n + r = q * n + r
      two_decompositions = Calc $
        |~ (fst $ divmodNatNZ x n n_nz) * n + r
        ~~ (fst $ divmodNatNZ x n n_nz) * n + (snd $ divmodNatNZ x n n_nz)
                                                       ...(cong (\ u =>
                                                                (fst $ divmodNatNZ x n n_nz)* n + u)
                                                                $ sym mod_eq_r)
        ~~ snd(divmodNatNZ x n n_nz) + fst (divmodNatNZ x n n_nz) * n
                                                       ...(plusCommutative _ _)
        ~~ x                                           ...(sym $ DivisionTheoremDivMod x n n_nz)
        ~~ q*n + r                                     ...(x_eq_qnr)

  in multRightCancel  (fst $ divmodNatNZ x n n_nz) q n n_nz
   $ plusRightCancel ((fst $ divmodNatNZ x n n_nz)* n) (q*n) r
   $ two_decompositions

export
DivisionTheoremUniquenessDivMod : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom)
     -> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
     -> divmodNatNZ numer denom denom_nz = (q, r)
DivisionTheoremUniquenessDivMod numer denom denom_nz q r x prf =
  rewrite sym $ step1 numer denom denom_nz q r x prf in
  rewrite sym $ step2 numer denom denom_nz q r x prf in
  pair_eta _  -- Should idris be able to see this automatically? Maybe only with homogeneous equality?
  where
    -- Should this go elsewhere?
    ||| extensionality law for simple pairs
    pair_eta : (x : (a,b)) -> x = (fst x, snd x)
    pair_eta (x,y) = Refl

export
DivisionTheoremUniqueness : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom)
     -> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
     -> (divNatNZ numer denom denom_nz = q, modNatNZ numer denom denom_nz = r)
DivisionTheoremUniqueness numer denom denom_nz q r x prf =
  rewrite sym $ fstDivmodNatNZeqDiv numer denom denom_nz denom_nz in
  rewrite sym $ sndDivmodNatNZeqMod numer denom denom_nz denom_nz in
  rewrite DivisionTheoremUniquenessDivMod numer denom denom_nz q r x prf in
  (Refl, Refl)


text:
module Flexidisc.Tutorial

import Flexidisc

person0 : Record String ["Firstname" ::: String]
person0 = ["Firstname" := "John"]

||| From here, we can access row by name.
|||
||| Fields arepublic  verified at compile time: if we try to access a field that is
||| not defined for our record, we obtain a compilation error, not a runtime
||| error.
|||
||| One of the key contribution in Flexidisc is that you can't declare the
||| smae field twice (no, it's not that easy)
||| If we add another field 'Firstname', even with a different type,
||| we'll obtain a compilation error.
person0Name : String
person0Name = get "Firstname" person0

||| or with the infix notation:
person0Name' : String
person0Name' = person0 !! "Firstname"

||| you can even lookup for fields that my or may not be there
person0Age : Maybe Nat
person0Age = Read.lookup "Age" person0

||| We can of course extend records:
person1 : Record String ["Age" ::: Nat, "Lastname" ::: String, "Firstname" ::: String]
person1 = ("Lastname" := "Doe") :: ("Age" := the Nat 42) :: person0

||| We can also project a record on a smaller one
person3 : Record String ["Firstname" ::: String, "Lastname" ::: String]
person3 = project person1

||| You can merge records
idJohn : Record String [("ID", Nat), ("Firstname", String), ("Lastname", String), ("Age", Nat)]
idJohn = ["ID" := the Nat 1, "Firstname" := "John"]
      ++ ["Lastname" := "Doe", "Age" := the Nat 42]

||| If you want to give explicitly the order of the new elements you want
||| you can use `keep`
person4 : Record String ["Firstname" ::: String, "Lastname" ::: String]
person4 = keep ["Firstname", "Lastname"] person1

||| If you want to give explicitly the order of the new elements you want
||| you can use `keep`
person4' : Record String ["Age" ::: Nat]
person4' = discard ["Firstname", "Lastname"] person1

||| You can alternatively decide to drop a field by its name:
person5 :  Record String ["Firstname" ::: String, "Lastname" ::: String]
person5 = drop "Age" person1

{-
||| You can also patch a record with another record:
person6 :  Record String ["Firstname" ::: String, "Lastname" ::: String, "Age" ::: Nat]
person6 = patch person2 (namedRec ["Lastname" := "Biri", "Firstname" := "Nicolas"])
-}

||| Field can be updated quite easily too
olderPerson : Record String ["Firstname" ::: String, "Lastname" ::: String, "Age" ::: Nat]
olderPerson = update "Age" (+1) person1

||| What if we want a generic `birthday` function for record with an age?
||| The result type is a bit complex here.
||| Actually we just explain that we update the `"Age"` field, replacing it
||| its content by a Nat.
birthday : Record String xs -> {auto hasAge: Row "Age" Nat xs} ->
           Record String (changeType xs hasAge Nat)
birthday rec = update "Age" (+1) rec

||| And we can check that it works on different types:
olderPeople : ( Record String ["Age" ::: Nat]
              , Record String ["Firstname" ::: String, "Lastname" ::: String, "Age" ::: Nat]
              )
olderPeople = (birthday person4', birthday person1)

||| You can also ensure that several fields are there
fullname : Record String xs ->
           {auto requiredFields : Sub [ "Lastname"  ::: String
                                      , "Firstname" ::: String ] xs} ->
           String
fullname xs = (xs !! "Firstname") ++ " " ++ (xs !! "Lastname")

||| Or ensure that some row doesn't exist to create them
addFullname : Record String xs ->
              {auto requiredFields : Sub [ "Firstname" ::: String
                                         , "Lastname"  ::: String ] xs} ->
              {auto newFields : Disjoint [ "Fullname"  ::: String ] xs} ->
              Record String (merge ["Fullname" :::  String] xs)
addFullname r = ["Fullname" := fullname r] ++ r

||| We can also decide to merge records if there is no overlap
twoPartsPerson : Record String [ "ID" ::: Nat
                        , "Firstname" ::: String
                        , "Lastname" ::: String
                        , "Age" ::: Nat
                        ]
twoPartsPerson = ["ID" := the Nat 1, "Firstname" := "John"] ++ ["Lastname" := "Doe", "Age" := the Nat 42]

eqExample : Bool
eqExample = person1 == olderPerson

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Main

import Cairo
import Data.Bits

-- The following functions are required to avoid that the constantfolder
-- evaluates the expressions at compile time.
-- Maybe we should disable the constantfolder and write the tests more direct.

%foreign
  """
  code:
  func Main_f_200() -> (r):
      return (200)
  end
  """
f_200 : Felt

%foreign
  """
  code:
  func Main_f_100() -> (r):
      return (100)
  end
  """
f_100 : Felt

u_200 : Bits8
u_200 = cast {to=Bits8} f_200

u_100 : Bits8
u_100 = cast {to=Bits8} f_100

out : Cast a Felt => a -> Cairo ()
out = output . cast

%noinline
main : Cairo ()
main = do
  out $ u_200 + u_100
  out $ u_200 - u_100
  out $ u_200 * u_100
  -- BUG, this returns 0!!!
  -- Patternmachting on felt famously does not work.
  -- Best would be to make it work - otherwise throw an error at compile time or at least crash at runtime.
  -- out $ case b of 0 => 0 ; x => (cast {to=Bits8} a) `div` (cast {to=Bits8} x)
  out $ assert_total $ u_200 `div` 7
  out $ assert_total $ u_200 `mod` 7
  out $ - u_100
  out $ u_200 .&. u_100
  out $ u_200 .|. u_100
  out $ u_200 `xor` u_100
  out $ u_200 < u_100
  out $ u_200 <= u_100
  out $ u_200 == u_100
  out $ u_200 >= u_100
  out $ u_200 > u_100
  -- out $ u_100 `shiftL` 1 -- Index is of type Nat. Not implemented yet
  -- out $ u_100 `shiftR` 1

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
-- Module      : Itea.Html.Attributes
-- Description :
-- Copyright   : (c) Simon Nielsen Knights 2018
-- License     : MIT
-- Maintainer  : simonank@mail.ru
-- Stability   : unstable
-- Portability : portable

module Itea.Html.Attributes

%default total
%access public export

||| Element attirbutes
Attribute : Type
Attribute = Pair String String

||| Image dimension
data Dimension : Type where
  ||| Size in pixels
  Pixel   : Int -> Dimension
  ||| Size in percent
  Percent : Int -> Dimension

Show Dimension where
  show (Pixel x) = show x ++ "px"
  show (Percent x) = show x ++ "%"

cssClass : List String -> Attribute
cssClass = MkPair "class" . unwords

namespace Simple

  cssClass : String -> Attribute
  cssClass = cssClass . (::[])

href : String -> Attribute
href = MkPair "href"

id : String -> Attribute
id = MkPair "id"

title : String -> Attribute
title = MkPair "title"

rel : String -> Attribute
rel = MkPair "rel"

width : Dimension -> Attribute
width = MkPair "width" . show

height : Dimension -> Attribute
height = MkPair "height" . show

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea


text:
module Diff

import VNode
import Render
import Attributes

%foreign "browser:lambda: node => node.remove()"
prim__remove : NodeRef -> PrimIO ()

%foreign "browser:lambda: node => node.attributes.forEach(attr => node.removeAttribute(attr))"
prim__removeAttrs : NodeRef -> PrimIO ()

reRender : (root: NodeRef) -> (old : DOM L) -> (new : DOM V) -> IO (DOM L)
reRender root (LiveDOM _ _ oldRef) new = do
  _ <- primIO $ prim__remove oldRef
  render root new

-- Currently this does nothing
updateMeta : (new : DOM V) -> (old : DOM L) -> IO (DOM L)
updateMeta new old = pure old

resetAttrs : (old : DOM L) -> List Attribute -> IO (DOM L)
resetAttrs old@(LiveDOM _ _ ref) attrs = do
  _ <- primIO $ prim__removeAttrs ref
  _ <- setAttributes ref attrs
  pure old

-- Checks if we need to update the attributes
updateAttributes : (new : DOM V) -> (old : DOM L) -> IO (DOM L)
updateAttributes new@(VDOM _ newNode) old@(LiveDOM _ oldNode ref) =
  case (newNode, oldNode) of
   (Tag _ oldAttr _, Tag _ newAttr _) =>
     if oldAttr /= newAttr
        then resetAttrs old newAttr
        else pure old
   (Void _ oldAttr, Void _ newAttr) =>
     if oldAttr /= newAttr
        then resetAttrs old newAttr
        else pure old
   (Text oldText, Text newText) => pure old
   (_, _) => pure old

mutual
  diffChildren : (root : NodeRef) -> (old : List (DOM L)) -> (new : List (DOM V)) -> IO (List (DOM L))
  diffChildren root (old :: olds) (new :: news) = do
    this <-  diff root new old
    rest <- diffChildren root olds news
    pure (this :: rest)
  diffChildren root ((LiveDOM _ _ ref) :: olds) [] = do
    _ <- primIO $ prim__remove ref
    rest <- diffChildren root olds []
    pure rest
  diffChildren root [] (new :: news) = do
    this <- render root new
    rest <- diffChildren root [] news
    pure (this :: rest)
  diffChildren root [] [] = pure []

  -- Checks if we need to re-render the whole Node
  reRenderAll : (root : NodeRef) ->  (new : DOM V) -> (old : DOM L) -> IO (DOM L)
  reRenderAll root new@(VDOM _ newNode) old@(LiveDOM oldMeta oldNode oldRef) =
    case (oldNode, newNode) of
     ((Tag oldName oldAttr oldChildren), (Tag newName newAttr newChildren)) =>
        if oldName /= newName
           then reRender root old new
           else do
             newChildren <- diffChildren oldRef oldChildren newChildren
             let newTag = Tag oldName oldAttr newChildren
             pure (LiveDOM oldMeta newTag oldRef)
     ((Void oldName oldAttr), (Void newName newAttr)) =>
        if oldName /= newName
           then reRender root old new
           else pure old
     ((Text oldText), (Text newText)) =>
        if oldText /= newText
           then reRender root old new
           else pure old
     (_, _) => reRender root old new

  export
  diff : (root : NodeRef) -> (new : DOM V) -> (old : DOM L) -> IO (DOM L)
  diff root new old = updateMeta new old >>= reRenderAll root new >>= updateAttributes new

max_stars_repo_name: Stinners/alder

max_issues_repo_name: Stinners/alder

max_forks_repo_name: Stinners/alder


text:
{-
Copyright 2019, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module Main

import StwfFFI.Utils

main : IO ()
main = do
    consoleUtilsInit
    consoleUtilsSetType 0
    consoleUtilsPrintf "Setup UART logging\n"

max_stars_repo_name: mokshasoft/bare-metal-idris-apps

max_issues_repo_name: mokshasoft/bare-metal-idris-apps

max_forks_repo_name: mokshasoft/bare-metal-idris-apps


text:
import System

main : IO ()
main = printLn !getArgs


text:
module Data.LengthMatch

%default total

public export
data LengthMatch : List a -> List b -> Type where
     NilMatch : LengthMatch [] []
     ConsMatch : LengthMatch xs ys -> LengthMatch (x :: xs) (y :: ys)

export
checkLengthMatch : (xs : List a) -> (ys : List b) -> Maybe (LengthMatch xs ys)
checkLengthMatch [] [] = Just NilMatch
checkLengthMatch [] (x :: xs) = Nothing
checkLengthMatch (x :: xs) [] = Nothing
checkLengthMatch (x :: xs) (y :: ys)
    = Just (ConsMatch !(checkLengthMatch xs ys))


text:
module Bautzen.Game.Move

import Bautzen.Game.Core
import Bautzen.GameUnit
import Bautzen.Pos
import Bautzen.Terrain
import Bautzen.ZoC

import Data.List.Extra as List
import Data.Nat.Extra

import Data.List
import Data.Maybe
import Data.Nat

public export
updateMovedUnit : (unit : GameUnit) -> Pos -> (mps : Nat) -> { auto prf : LTE mps (currentMP unit) } -> List (GameUnit, Pos) -> List (GameUnit, Pos)
updateMovedUnit unit newPosition mps = foldr updateUnit []
  where
    newMP : Nat
    newMP = currentMP unit - mps

    updateUnit : (GameUnit, Pos) -> List (GameUnit, Pos) -> List (GameUnit, Pos)
    updateUnit (gu, pos) acc =
      if fullName unit == fullName gu
      then (record { currentMP = newMP } unit, newPosition) :: acc
      else (gu, pos) :: acc

public export
movementCost : (unit : GameUnit) -> (units : List (GameUnit, Pos)) -> (gameMap : Map) -> (from : Pos) -> (to : Pos)
             -> Bool
             -> Either GameError (cost : Cost ** LTE (toNat cost) (currentMP unit))
movementCost unit units gameMap from to leavingZoC with (cost (unitType unit) (terrain to gameMap) (connection from to gameMap))
  movementCost unit units _ from to _     | Impossible = Left (ForbiddenTerrain from to)
  movementCost unit units _ from to False | c = case isLTE (toNat c) (currentMP unit) of
                                                           Yes prf => Right (c ** prf)
                                                           No _    => Left (NotEnoughMPs unit from to (toNat c))
  movementCost unit units _ from to True  | c = let cost = One c
                                                in case isLTE (toNat cost) (currentMP unit) of
                                                           Yes prf => Right (cost ** prf)
                                                           No _    => Left (NotEnoughMPs unit from to (toNat cost))

public export
moreMoveTo : (unit : GameUnit) -> (units : List (GameUnit, Pos)) -> (gameMap : Map) -> (from : Pos) -> (to : Pos) -> Either GameError Event
moreMoveTo unit units gameMap from to with (inZoC (side (nation unit)) units from, inZoC (side (nation unit)) units to)
  moreMoveTo unit units gameMap from to | (InZoC _, Free) = do (c ** _) <- movementCost unit units gameMap from to True
                                                               pure (Moved unit from to c)
  moreMoveTo unit units gameMap from to | (Free, _) = do (c ** _) <- movementCost unit units gameMap from to False
                                                         pure (Moved unit from to c)
  moreMoveTo unit units gameMap from to | (_, _) = Left (MoveFromZocToZoc unit to)

public export
sameName : String -> (GameUnit, Pos) -> Bool
sameName unitName (u,_) = fullName u == unitName

public export
samePosition : Pos -> (GameUnit, Pos) -> Bool
samePosition to (_,p) = p == to

public export
moveTo : (side : Side) -> (units : List (GameUnit, Pos)) -> Map -> (unitName : String) -> (to : Pos) -> Either GameError Event
moveTo sideToPlay units gameMap unitName to =
  case find' (sameName unitName) units of
    (Just (unit, b)) => if side (nation unit) /= sideToPlay
                        then Left (NotYourTurn (side (nation unit)))
                        else if not (to `elem` (neighbours b))
                             then Left (InvalidMove b to)
                             else case find' (samePosition to) units of
                                       Nothing => moreMoveTo unit units gameMap b to
                                       (Just (other, _)) => if friendly (nation unit) (nation other)
                                                            then moreMoveTo unit units gameMap b to
                                                            else Left (EnemyInHex other to)
    Nothing => Left (NoSuchUnits [unitName])

-- namespace MoveTest

--   cannot_move_if_unit_does_not_exist : moveTo Allies [ (Bautzen.GameUnit.p13_5dp, Hex 3 4) ] TestMap "foo" (Hex 3 5) = Left (NoSuchUnits [ "foo" ])
--   cannot_move_if_unit_does_not_exist = Refl

--   cannot_move_not_current_side : moveTo Axis [ (Bautzen.GameUnit.p13_5dp, Hex 3 4) ] TestMap "13/5DP" (Hex 3 5) = Left (NotYourTurn Allies)
--   cannot_move_not_current_side = Refl

--   cannot_move_if_target_hex_is_occupied_by_enemy : moveTo Allies [ (Bautzen.GameUnit.p13_5dp, Hex 3 4), (Bautzen.GameUnit.g21_20pz, Hex 3 5) ] TestMap "13/5DP" (Hex 3 5) = Left (EnemyInHex Bautzen.GameUnit.g21_20pz (Hex 3 5))
--   cannot_move_if_target_hex_is_occupied_by_enemy = Refl

--   cannot_move_from_zoc_to_zoc : moveTo Allies [ (Bautzen.GameUnit.p13_5dp, Hex 3 4), (Bautzen.GameUnit.g21_20pz, Hex 3 5) ] TestMap "13/5DP" (Hex 4 5) = Left (MoveFromZocToZoc Bautzen.GameUnit.p13_5dp (Hex 4 5))
--   cannot_move_from_zoc_to_zoc = Refl

--   moving_into_clear_terrain_costs_1 : moveTo Allies [ (Bautzen.GameUnit.p13_5dp, Hex 3 4) ] TestMap "13/5DP" (Hex 4 4) = Right (Moved Bautzen.GameUnit.p13_5dp (Hex 3 4) (Hex 4 4) (One Zero))
--   moving_into_clear_terrain_costs_1 = Refl

--   infantry_moving_into_rough_terrain_costs_1 : moveTo Allies [ (Bautzen.GameUnit.p13_5dp, Hex 3 4) ] TestMap "13/5DP" (Hex 3 3) = Right (Moved Bautzen.GameUnit.p13_5dp (Hex 3 4) (Hex 3 3) (One Zero))
--   infantry_moving_into_rough_terrain_costs_1 = Refl

--   non_infantry_moving_into_rough_terrain_costs_2 : moveTo Axis [ (Bautzen.GameUnit.g21_20pz, Hex 3 4) ] TestMap "21/20Pz" (Hex 3 3) = Right (Moved Bautzen.GameUnit.g21_20pz (Hex 3 4) (Hex 3 3) (Two Zero))
--   non_infantry_moving_into_rough_terrain_costs_2 = Refl

--   cost_for_rough_is_cumulative : moveTo Allies [ (Bautzen.GameUnit.p13_5dp, Hex 3 4) ] TestMap "13/5DP" (Hex 3 5) = Right (Moved Bautzen.GameUnit.p13_5dp (Hex 3 4) (Hex 3 5) (One (One Zero)))
--   cost_for_rough_is_cumulative = Refl

--   armored_cost_for_rough_is_cumulative : moveTo Axis [ (Bautzen.GameUnit.g21_20pz, Hex 3 4) ] TestMap "21/20Pz" (Hex 3 5) = Right (Moved Bautzen.GameUnit.g21_20pz (Hex 3 4) (Hex 3 5) (Two (Two Zero)))
--   armored_cost_for_rough_is_cumulative = Refl

--   moving_across_a_lake_is_forbidden : moveTo Axis [ (Bautzen.GameUnit.g21_20pz, Hex 8 6) ] TestMap "21/20Pz" (Hex 8 7) = Left (ForbiddenTerrain (Hex 8 6) (Hex 8 7))
--   moving_across_a_lake_is_forbidden = Refl

--   armored_moving_on_hill_is_forbidden : moveTo Axis [ (Bautzen.GameUnit.g21_20pz, Hex 3 4) ] TestMap "21/20Pz" (Hex 4 5) = Left (ForbiddenTerrain (Hex 3 4) (Hex 4 5))
--   armored_moving_on_hill_is_forbidden = Refl

--   armored_moving_on_hill_through_road_costs_half : moveTo Axis [ (Bautzen.GameUnit.g21_20pz, Hex 8 7) ] TestMap "21/20Pz" (Hex 7 7) = Right (Moved Bautzen.GameUnit.g21_20pz (Hex 8 7) (Hex 7 7) (Half (Two Zero)))
--   armored_moving_on_hill_through_road_costs_half = Refl

--   armored_moving_through_road_costs_half : moveTo Axis [ (Bautzen.GameUnit.g21_20pz, Hex 4 4) ] TestMap "21/20Pz" (Hex 5 4) = Right (Moved Bautzen.GameUnit.g21_20pz (Hex 4 4) (Hex 5 4) (Half (One Zero)))
--   armored_moving_through_road_costs_half = Refl

--   infantry_moving_through_road_costs_half : moveTo Allies [ (Bautzen.GameUnit.p13_5dp, Hex 8 7) ] TestMap "13/5DP" (Hex 7 7) = Right (Moved Bautzen.GameUnit.p13_5dp (Hex 8 7) (Hex 7 7) (Half (Two (One Zero))))
--   infantry_moving_through_road_costs_half = Refl

--   river_adds_one_PM_to_move : moveTo Allies [ (Bautzen.GameUnit.p13_5dp, Hex 10 3) ] TestMap "13/5DP" (Hex 10 2) = Right (Moved Bautzen.GameUnit.p13_5dp (Hex 10 3) (Hex 10 2) (Half (One (One (One Zero)))))
--   river_adds_one_PM_to_move = Refl

--   moving_out_of_ZoC_adds_one_PM_to_move : moveTo Allies [ (Bautzen.GameUnit.p13_5dp, Hex 3 4), (Bautzen.GameUnit.g21_20pz, Hex 3 5) ] TestMap "13/5DP" (Hex 4 4) = Right (Moved Bautzen.GameUnit.p13_5dp (Hex 3 4) (Hex 4 4) (One (One Zero)))
--   moving_out_of_ZoC_adds_one_PM_to_move = Refl

--   g21_20pz_no_mp : GameUnit
--   g21_20pz_no_mp = record { currentMP = 3 } GameUnit.g21_20pz

--   unit_cannot_move_if_not_enough_MP : moveTo Axis [ (MoveTest.g21_20pz_no_mp, Hex 3 4) ] TestMap "21/20Pz" (Hex 3 5) = Left (NotEnoughMPs MoveTest.g21_20pz_no_mp (Hex 3 4) (Hex 3 5) 4)
--   unit_cannot_move_if_not_enough_MP = Refl

--   cannot_move_more_than_one_hex : moveTo Axis [ (Bautzen.GameUnit.g21_20pz, Hex 3 4) ] TestMap "21/20Pz" (Hex 3 6) = Left (InvalidMove (Hex 3 4) (Hex 3 6))
--   cannot_move_more_than_one_hex = Refl

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
import Data.Vect
import Data.Vect.Elem
import Decidable.Equality

removeElem_v1 : DecEq a => (value : a) -> (xs : Vect (S n) a) -> Vect n a
removeElem_v1 value (x :: xs) = case decEq value x of
                                     Yes prf => xs
                                     No contra => ?removeElem_v1_rhs -- x :: removeElem_v1 value xs

Uninhabited (2 + 2 = 5) where
    uninhabited Refl impossible

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

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

removeElem : {n : _} ->
             (value : a) -> (xs : Vect (S n) a) ->
             {auto prf : Elem value xs} ->
             Vect n a
removeElem value (value :: ys) {prf = Here} = ys
removeElem {n = Z} value (y :: []) {prf = There later} = absurd later
removeElem {n = (S k)} value (y :: ys) {prf = There later}
                                          = y :: removeElem value ys

my_elem : Eq a => (value : a) -> (xs : Vect n a) -> Bool
my_elem value [] = False
my_elem value (x :: xs) = case value == x of
                               False => my_elem value xs
                               True => True

not_in_nil : Elem value [] -> Void
not_in_nil Here impossible
not_in_nil (There _) impossible

not_in_tail : (contra1 : Elem value xs -> Void) -> (contra : (value = x) -> Void) -> Elem value (x :: xs) -> Void
not_in_tail contra1 contra Here = contra Refl
not_in_tail contra1 contra (There later) = contra1 later

my_decElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
my_decElem value [] = No not_in_nil
my_decElem value (x :: xs)
      = case decEq value x of
            (Yes Refl) => Yes Here
            (No contra) => case my_decElem value xs of
                                (Yes prf) => Yes (There prf)
                                (No contra1) => No (not_in_tail contra1 contra)


text:
-- Copyright (c) 2013 Radek Micek

module Main

import D3

main : IO ()
main = do

  -- Prints: 3, 5
  arr <- mkArray [1, 2, 3, 6]
  getNth arr 2 >>= print
  setNth arr 2 5
  getNth arr 2 >>= print

  -- Prints: 0, 1, 17
  arr2 <- emptyA ()
  lengthA arr2 >>= print
  pushA arr2 17
  lengthA arr2 >>= print
  getNth arr2 0 >>= print

  -- Prints: True, False
  anyA (pure . (== 5)) arr >>= print
  anyA (pure . (== 3)) arr >>= print

  -- Prints: [1, 2, 5, 6]
  --         [1, 2]
  arr3 <- filterA (pure . (< 4)) arr
  arrayToList arr >>= print
  arrayToList arr3 >>= print

  return ()

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
import Mod1
import Mod2

main : IO ()
main = printLn foo


text:
module Movement

%default total
%access public

data By =
  ByCharacter
  | ByLine

data Move : By -> Type where
  Backward : {by : By} -> Nat -> Move by
  Forward : {by : By} -> Nat -> Move by

%name Move movement

h : Nat -> Move ByCharacter
h x = Backward x

j : Nat -> Move ByLine
j x = Forward x

l : Nat -> Move ByCharacter
l x = Forward x

k : Nat -> Move ByLine
k x = Backward x


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

import XML.DOM
import XML.Reader
import XML.XPath

import Freyja
import Freyja.Extract
import Freyja.Convert
import Freyja.Convert.Edda

import Edda
import Edda.Writer.Org

import Sif.Types
import Sif.Pattern
import Sif.Pattern.Recover
import Sif.Builder.AbsInterp

import Readability
import Readability.Process.XML

import Frigg.Effs
import Frigg.Options
import Frigg.Error
import Frigg.Eval
import Frigg.Commands

%access export

loadPatternDoc : Maybe String -> Frigg ()
loadPatternDoc Nothing   = Frigg.raise FileExpected
loadPatternDoc (Just fn) = do
  doc <- readXMLDoc fn
  case doc of
    Left err  => printLn $ Frigg.Error.ParseError (show err)
    Right res => do
      putXMLDoc res
      case document res of
        Left err  => printLn $ Frigg.Error.ParseError (show err)
        Right doc => putPatternDoc doc

-- --------------------------------------------------------------- [ Transform ]

doConvertShow : FreyjaOutFormat -> Frigg ()
doConvertShow fmt = do
    doc <- getPatternDoc
    case convShow fmt doc of
      Nothing  => Frigg.raise $ GeneralError "Error"
      Just str => putStrLn str

convertShowDoc : Frigg ()
convertShowDoc = do
    case to !getOptions of
      Nothing  => Frigg.raise NoFormatSpecified
      Just fmt => doConvertShow fmt

-- ---------------------------------------------------------------- [ Sif Eval ]
evalSifRepr : Frigg Sif.EvalResult
evalSifRepr = do
    doc <- getPatternDoc
    let (_ ** sifrep) = fromFreya absInterpBuilder doc
    let res = evalPattern sifrep
    pure res

evalSifAndReport : Frigg ()
evalSifAndReport = do
  res <- evalSifRepr
  case evalResultsToString res of
    Just res => putStrLn res
    Nothing  => putStrLn "oops"

-- ----------------------------------------------------------------- [ Display ]

doDisplay : DisplayPattern -> Frigg ()
doDisplay All       = putStrLn (org    (convertPattern !getPatternDoc))
doDisplay MData     = putStrLn (blocks (convertMetadata (mdata    !getPatternDoc)))
doDisplay Context   = putStrLn (blocks (convertDomain   (context  !getPatternDoc)))
doDisplay Problem   = putStrLn (blocks (convertProblem  (problem  !getPatternDoc)))
doDisplay Solution  = putStrLn (blocks (convertSolution (solution !getPatternDoc)))
doDisplay Evidence  = putStrLn (blocks (convertEvidence (evidence !getPatternDoc)))
doDisplay Studies   = putStrLn (blocks (convertStudies  (studies  !getPatternDoc)))
doDisplay Related   = printLn FeatureNotImpl -- @TODO
doDisplay Summary = do
    doc <- getPatternDoc
    putStrLn $ inlines (name doc)
    putStrLn $ blocks  (summary doc)

-- ------------------------------------------------------------- [ Readability ]

evalReadability : Frigg ReadResult
evalReadability = do
  xdoc <- getXMLDoc
  case calcReadability xdoc of
    Nothing      => Frigg.raise MalformedPattern
    Just readRes => pure readRes

evalReadAndReport : Frigg ()
evalReadAndReport = do
  res <- evalReadability
  putStrLn $ unlines $ map show (Metrics.toList res)

-- ------------------------------------------------------------------- [ Query ]

doQuery : String -> Frigg ()
doQuery qStr = do
  xdoc <- getXMLDoc
  case query qStr xdoc of
    Left err  => printLn err
    Right Nil => putStrLn "Nothing Found"
    Right rs  => putStrLn $ unlines $ map (\r => show @{xml} r) rs

-- ---------------------------------------------------------------- [ Template ]

doEvalAndReport : EvalPattern -> Frigg ()
doEvalAndReport SifModel    = evalSifAndReport
doEvalAndReport TemplateAd  = evalTemplateAndReport
doEvalAndReport Readability = evalReadAndReport
doEvalAndReport EvalAll     = printLn FeatureNotImpl

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

max_stars_repo_name: jfdm/frigg-tool

max_issues_repo_name: jfdm/frigg-tool

max_forks_repo_name: jfdm/frigg-tool


text:
module Java.IO

import IdrisJvm.IO
import Java.Lang

%access public export

namespace File
    fileClass : String
    fileClass = "java/io/File"

    FileClass : JVM_NativeTy
    FileClass = Class fileClass

    File : Type
    File = JVM_Native FileClass

namespace IOException

  IOException : Type
  IOException = JVM_Native (Class "java/io/IOException")

  new : String -> JVM_IO IOException
  new = FFI.new (String -> JVM_IO IOException)

namespace OutputStream

  OutputStream : Type
  OutputStream = JVM_Native (Class "java/io/OutputStream")

  Inherits Closeable OutputStream where {}

  Inherits Flushable OutputStream where {}

namespace BufferedReader
    BufferedReader : Type
    BufferedReader = JVM_Native (Class "java/io/BufferedReader")


text:
module Data.Fin.Extra

import Data.Fin
import Data.Nat

%default total

||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
export
elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
elemSmallerThanBound FZ = LTESucc LTEZero
elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)

||| Proof that application of finToNat the last element of Fin **S n** gives **n**.
export
finToNatLastIsBound : {n : Nat} -> finToNat (Fin.last {n}) = n
finToNatLastIsBound {n=Z} = Refl
finToNatLastIsBound {n=S k} = rewrite finToNatLastIsBound {n=k} in Refl

||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
export
finToNatWeakenNeutral : {m : Nat} -> {n : Fin m} -> finToNat (weaken n) = finToNat n
finToNatWeakenNeutral {n=FZ} = Refl
finToNatWeakenNeutral {m=S (S _)} {n=FS _} = cong S finToNatWeakenNeutral

-- ||| Proof that it's possible to strengthen a weakened element of Fin **m**.
-- export
-- strengthenWeakenNeutral : {m : Nat} -> (n : Fin m) -> strengthen (weaken n) = Right n
-- strengthenWeakenNeutral {m=S _} FZ = Refl
-- strengthenWeakenNeutral {m=S (S _)} (FS k) = rewrite strengthenWeakenNeutral k in Refl

||| Proof that it's not possible to strengthen the last element of Fin **n**.
export
strengthenLastIsLeft : {n : Nat} -> strengthen (Fin.last {n}) = Left (Fin.last {n})
strengthenLastIsLeft {n=Z} = Refl
strengthenLastIsLeft {n=S k} = rewrite strengthenLastIsLeft {n=k} in Refl

||| Enumerate elements of Fin **n** backwards.
export
invFin : {n : Nat} -> Fin n -> Fin n
invFin FZ = last
invFin {n=S (S _)} (FS k) = weaken (invFin k)

||| Proof that an inverse of a weakened element of Fin **n** is a successive of an inverse of an original element.
export
invWeakenIsSucc : {n : Nat} -> (m : Fin n) -> invFin (weaken m) = FS (invFin m)
invWeakenIsSucc FZ = Refl
invWeakenIsSucc {n=S (S _)} (FS k) = rewrite invWeakenIsSucc k in Refl

||| Proof that double inversion of Fin **n** gives the original.
export
doubleInvFinSame : {n : Nat} -> (m : Fin n) -> invFin (invFin m) = m
doubleInvFinSame {n=S Z} FZ = Refl
doubleInvFinSame {n=S (S k)} FZ = rewrite doubleInvFinSame {n=S k} FZ in Refl
doubleInvFinSame {n=S (S _)} (FS x) = trans (invWeakenIsSucc $ invFin x) (cong FS $ doubleInvFinSame x)

||| Proof that an inverse of the last element of Fin (S **n**) in FZ.
export
invLastIsFZ : {n : Nat} -> invFin (Fin.last {n}) = FZ
invLastIsFZ {n=Z} = Refl
invLastIsFZ {n=S k} = rewrite invLastIsFZ {n=k} in Refl

-- ||| Proof that it's possible to strengthen an inverse of a succesive element of Fin **n**.
-- export
-- strengthenNotLastIsRight : (m : Fin (S n)) -> strengthen (invFin (FS m)) = Right (invFin m)
-- strengthenNotLastIsRight m = strengthenWeakenNeutral (invFin m)
--
||| Either tightens the bound on a Fin or proves that it's the last.
export
strengthen' : {n : Nat} -> (m : Fin (S n)) -> Either (m = Fin.last) (m' : Fin n ** finToNat m = finToNat m')
strengthen' {n = Z} FZ = Left Refl
strengthen' {n = S k} FZ = Right (FZ ** Refl)
strengthen' {n = S k} (FS m) = case strengthen' m of
    Left eq => Left $ cong FS eq
    Right (m' ** eq) => Right (FS m' ** cong S eq)

||| A view of Nat as a quotient of some number and a finite remainder.
public export
data FractionView : (n : Nat) -> (d : Nat) -> Type where
    Fraction : (n : Nat) -> (d : Nat) -> {auto ok: GT d Z} ->
                (q : Nat) -> (r : Fin d) ->
                q * d + finToNat r = n -> FractionView n d

||| Converts Nat to the fractional view with a non-zero divisor.
export
divMod : (n, d : Nat) -> {auto ok: GT d Z} -> FractionView n d
divMod Z (S d) = Fraction Z (S d) Z FZ Refl
divMod {ok=_} (S n) (S d) =
    let Fraction {ok=ok} n (S d) q r eq = divMod n (S d) in
    case strengthen' r of
        Left eq' => Fraction {ok=ok} (S n) (S d) (S q) FZ $
            rewrite sym eq in
                rewrite trans (cong finToNat eq') finToNatLastIsBound in
                    cong S $ trans
                        (plusZeroRightNeutral (d + q * S d))
                        (plusCommutative d (q * S d))
        Right (r' ** eq') => Fraction {ok=ok} (S n) (S d) q (FS r') $
            rewrite sym $ plusSuccRightSucc (q * S d) (finToNat r') in
                cong S $ trans (sym $ cong (plus (q * S d)) eq') eq


text:
module ElabImplLambda

import Language.Reflection

%language ElabReflection

derive : {ty : Type} -> Elab ty
derive = check $
           ILam EmptyFC MW ExplicitArg (Just `{x}) `(Nat) $
             ILam EmptyFC MW AutoImplicit Nothing `(List Nat) $
               `(x + 1)

derived : Nat -> List Nat => Nat
derived = %runElab derive

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module NoRegression

import Data.Vect

data Dep : (n : Nat) -> (a : Type) -> Vect n a -> Type where
   MkDep : Dep n a v

dpairParse : (   n : Nat
              ** a : Type
              ** v : Vect n a
              ** Dep n a v
             )
dpairParse = (_ ** _ ** ["a", "b"] ** MkDep)


text:
module Main

import Data.Strings

%default total

%foreign "C:add,libcalc"
add : Int -> Int -> Int

%foreign "C:sub,libcalc"
sub : Int -> Int -> Int

%foreign "C:mul,libcalc"
mul : Int -> Int -> Int

%foreign "C:div,libcalc"
div : Int -> Int -> Int

%foreign "C:op_with_message,libcalc"
prim_opWithMessage : String -> (Int -> Int -> Int) -> Int -> Int -> PrimIO Int

opWithMessage : HasIO io => String -> (Int -> Int -> Int) -> Int -> Int -> io Int
opWithMessage s f x y = primIO $ prim_opWithMessage s f x y

readNum : HasIO io => io (Maybe Int)
readNum = do putStr "Enter number: "
             ns <- getLine
             case all isDigit (unpack ns) of
                  False => pure Nothing
                  True => pure (Just (cast ns))

main : IO ()
main = do Just x <- readNum
            | Nothing => putStrLn "first number is invalid"
          Just y <- readNum
            | Nothing => putStrLn "second number is invalid"
          printLn (add x y)
          printLn (sub x y)
          printLn (mul x y)
          printLn (Main.div x y)
          opWithMessage "sum" add x y
          opWithMessage "diff" sub x y
          opWithMessage "prod" mul x y
          opWithMessage "quot" Main.div x y
          pure ()

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

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

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


text:
module Demo

import Data.Vect

-- %default total

isSingleton : Bool -> Type
isSingleton True = Int
isSingleton False = List Nat

plus' : Nat -> Nat -> Nat
plus' Z j = j
plus' (S k) j = S (plus k j)

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = ?sd

take' : (n : Nat) -> Vect (n + m) a -> Vect n a
take' = ?rhs

total
head' : Vect (S n) a -> a
head' (x :: xs) = x

max_stars_repo_name: tgrospic/dependently-typed-slides

max_issues_repo_name: tgrospic/dependently-typed-slides

max_forks_repo_name: tgrospic/dependently-typed-slides


text:
module AddTwoNumbers

data Digit = D Int

ofIntHelp : Int -> List Digit
ofIntHelp 0 = []
ofIntHelp i = D (i `mod` 10) :: ofIntHelp (i `div` 10)

ofInt : Int -> List Digit
ofInt 0 = [D 0]
ofInt i = ofIntHelp i

addHelp : Bool -> List Digit -> List Digit -> List Digit
addHelp carry [] [] = if carry then [D 1] else []
addHelp False [] ys = ys
addHelp True [] ys = addHelp False [D 1] ys
addHelp False xs [] = xs
addHelp True xs [] = addHelp False [D 1] xs
addHelp carry (D x :: xs) (D y :: ys) =
  let sum = x + y + if carry then 1 else 0 in
  if sum >= 10 then
    D (sum `mod` 10) :: addHelp True xs ys
  else
    D sum :: addHelp False xs ys

add : List Digit -> List Digit -> List Digit
add = addHelp False

test1 : add (ofInt 342) (ofInt 465) = ofInt 807
test1 = Refl
test2 : add [D 0] [D 0] = [D 0]
test2 = Refl
test3 : add (map D [9,9,9,9,9,9,9]) (map D [9,9,9,9]) = map D [8,9,9,9,0,0,0,1]
test3 = Refl


text:
module BinaryRandomAccessList

import RandomAccessList

%default total
%access private

data Tree a = Leaf a | Node Int (Tree a) (Tree a)
data Digit a = Zero | One (Tree a)

export
data BinaryList a = BL (List (Digit a))

size : Tree a -> Int
size (Leaf x) = 1
size (Node w t1 t2) = w

link : Tree a -> Tree a -> Tree a
link t1 t2 = Node (size t1 + size t2) t1 t2

consTree : Tree a -> List (Digit a) -> List (Digit a)
consTree t  []             = [One t]
consTree t  (Zero   :: ts) = One t :: ts
consTree t1 (One t2 :: ts) = Zero  :: consTree (link t1 t2) ts

unconsTree : List (Digit a) -> (Tree a, List (Digit a))
unconsTree [] = idris_crash "empty list"
unconsTree [One t] = (t, [])
unconsTree (One t :: ts) = (t, Zero :: ts)
unconsTree (Zero :: ts) = case unconsTree ts of
  (Node _ t1 t2, ts') => (t1, One t2 :: ts')
  (Leaf _      , _)   => assert_unreachable

export
RandomAccessList BinaryList where
  empty = BL []
  isEmpty (BL ts) = isNil ts

  cons x (BL ts) = BL (consTree (Leaf x) ts)
  head (BL ts) = assert_total $ let (Leaf x, _) = unconsTree ts in x
  tail (BL ts) = let (_, ts') = unconsTree ts in BL ts'

  lookup i (BL ts) = look i ts
   where
    lookTree : Int -> Tree a -> a
    lookTree 0 (Leaf x)       = x
    lookTree i (Leaf x)       = idris_crash "bad subscript"
    lookTree i (Node w t1 t2) = let hw = assert_total $ w `div` 2
      in if i < hw then lookTree i t1 else lookTree (i - hw) t2

    look i []            = idris_crash "bad subscript"
    look i (Zero  :: ts) = look i ts
    look i (One t :: ts) =
      if i < size t then lookTree i t else look (i - size t) ts

  update i y (BL ts) = BL (upd i ts)
   where
    updTree : Int -> Tree a -> Tree a
    updTree 0 (Leaf x)       = Leaf y
    updTree i (Leaf x)       = idris_crash "bad subscript"
    updTree i (Node w t1 t2) = let hw = assert_total $ w `div` 2 in
      if i < hw then Node w (updTree i t1) t2
      else Node w t1 (updTree (i - hw) t2)

    upd i []            = idris_crash "bad subscript"
    upd i (Zero  :: ts) = Zero :: upd i ts
    upd i (One t :: ts) =
      if i < size t then One (updTree i t) :: ts
      else One t :: upd (i - size t) ts


text:
module Program

import CommonTestingStuff

import Data.List

export
beforeString : String
beforeString = "before coop"

s150 : PrintString m => CanSleep m => (offset : Time) => Nat -> m String
s150 no = do
  printTime offset "s150 proc \{show no}, first"
  for 5 $ do
    printTime offset "s150 proc \{show no}, before 1000"
    sleepFor 1.seconds
    printTime offset "s150 proc \{show no}, before 2000"
    sleepFor 2.seconds
  "long" <$ printTime offset "s150 proc \{show no}, last"

s55 : PrintString m => CanSleep m => (offset : Time) => Nat -> m String
s55 no = do
  printTime offset "                         s55 proc \{show no}, first"
  for 5 $ do
    printTime offset "                         s55 proc \{show no}, before 350"
    sleepFor 350.millis
    printTime offset "                         s55 proc \{show no}, before 750"
    sleepFor 750.millis
  "mid 1" <$ printTime offset "                         s55 proc \{show no}, last"

s35 : PrintString m => CanSleep m => (offset : Time) => Nat -> m String
s35 no = do
  printTime offset "                                               s35 proc \{show no}, first"
  for 5 $ do
    printTime offset "                                               s35 proc \{show no}, before 700"
    sleepFor 700.millis
  "short" <$ printTime offset "                                               s35 proc \{show no}, last"

s77 : PrintString m => CanSleep m => (offset : Time) => Nat -> m String
s77 no = do
  printTime offset "                                                                      s77 proc \{show no}, first"
  for 5 $ do
    printTime offset "                                                                      s77 proc \{show no}, before 1350"
    sleepFor 1350.millis
  sleepFor 950.millis
  "mid 2" <$ printTime offset "                                                                      s77 proc \{show no}, last"

export
program : PrintString m => CanSleep m => Zippable m => Alternative m => m Unit
program = do
  offset <- currentTime
  printTime offset "start"

  res <- choiceMap
    ( \(comp, n) => choiceMap (\k => comp k <&> (++ ", var #\{show k}")) $ take n [1..n] )
    [(s150, 1), (s55, 2), (s35, 3), (s77, 0)]
  printTime offset "top: \{res}"

  printTime offset "end"


text:
module Backprop

import public Backprop.CanBack
import public Backprop.Math
import public Backprop.Node
import public Data.List.Quantifiers


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

import Data.Vect

-- check that all functions are total
%default total

createEmptyVector : Num t =>
                    Vect n (Vect 0 t)
createEmptyVector {n} = replicate n []
-- or:
-- createEmptyVector = replicate _ []

transposeHelper : Num t =>
                  Vect n t ->
                  Vect n (Vect k t) ->
                  Vect n (Vect (S k) t)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys

transposeMatrix : Num t =>
                  Vect m (Vect n t) ->
                  Vect n (Vect m t)
transposeMatrix [] = createEmptyVector
transposeMatrix (x :: xs) = let xsTrans = transposeMatrix xs in
                            transposeHelper x xsTrans

transposeMatrixWithZip : Num t =>
                         Vect m (Vect n t) ->
                         Vect n (Vect m t)
transposeMatrixWithZip [] = createEmptyVector
transposeMatrixWithZip (x :: xs) = let xsTrans = transposeMatrixWithZip xs in
                                   zipWith (::) x xsTrans

addVector : Num t =>
            Vect n t ->
            Vect n t ->
            Vect n t
addVector = zipWith (+)
-- or:
-- addVector xs = zipWith (+) xs
-- or:
-- addVector [] [] = []
-- addVector (x :: xs) (y :: ys) = x + y :: addVector xs ys

multVector : Num t =>
             Vect n t ->
             Vect n t ->
             t
multVector xs ys = sum $ zipWith (*) xs ys
-- or:
-- multVector xs ys = foldl (+) 0 $ zipWith (*) xs ys
-- or:
-- multVector [] [] = 0
-- multVector (x :: xs) (y :: ys) = (x * y) + multVector xs ys

addMatrix : Num t =>
           Vect m (Vect n t) ->
           Vect m (Vect n t) ->
           Vect m (Vect n t)
addMatrix = zipWith (addVector)
-- or:
-- addMatrix [] [] = []
-- addMatrix (x :: xs) (y :: ys) = addVector x y :: addMatrix xs ys

multMatrixHelper2 : Num t =>
                    Vect n t ->
                    Vect p (Vect n t) ->
                    Vect p t
multMatrixHelper2 x ys = map (multVector x) ys
-- or:
-- multMatrixHelper2 _ [] = []
-- multMatrixHelper2 x (y :: ys) = multVector x y :: multMatrixHelper2 x ys

multMatrixHelper : Num t =>
                   Vect m (Vect n t) ->
                   Vect p (Vect n t) ->
                   Vect m (Vect p t)
multMatrixHelper xs ys = map (flip multMatrixHelper2 $ ys) xs
-- or:
-- multMatrixHelper xs ys = map (\x => multMatrixHelper2 x ys) xs
-- or:
-- multMatrixHelper [] _ = []
-- multMatrixHelper (x :: xs) ys = multMatrixHelper2 x ys :: multMatrixHelper xs ys

multMatrix : Num t =>
            Vect m (Vect n t) ->
            Vect n (Vect p t) ->
            Vect m (Vect p t)
multMatrix xs ys = multMatrixHelper xs $ transposeMatrixWithZip ys
-- or:
-- multMatrix xs ys = let ysTrans = transposeMatrixWithZip ys in
--                    multMatrixHelper xs ysTrans

v1 : Vect 3 (Vect 2 Nat)
v1 = [[1,2],[3,4],[5,6]]

v2 : Vect 2 (Vect 4 Nat)
v2 = [[7,8,9,10],[11,12,13,14]]

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
%include JavaScript "silly.js"

jscall : (fname : String) -> (ty : Type) ->
          {auto fty : FTy FFI_JS [] ty} -> ty
jscall fname ty = foreign FFI_JS fname ty

-- I don't know what I'm supposed to import to make this work given that the documentation shows this jscall function like it's a given so ???
-- and then when I add this function it looks like some of the other types aren't defined.
-- so what exactly from the documentation already exists and what do you just have to copy over?
counterMaker : JS_IO (() -> JS_IO Int)
counterMaker = jscall "counterMaker" (JS_IO (Js_Fn ( () -> JS_IO Int)))

main : JS_IO ()
main = do
  c <- counterMaker
  i <- jscall "%0()" (Js_Fn ( () -> JS_IO Int) -> JS_IO Int) c
  print i

max_stars_repo_name: clarissalittler/idris-practice

max_issues_repo_name: clarissalittler/idris-practice

max_forks_repo_name: clarissalittler/idris-practice


text:
module Common.Dict

import Common

-- module Data.Linear.Array
-- https://arxiv.org/pdf/1710.09756.pdf

-- How to implement LinDict Felt SomeOtherType?
-- And store the Felt as the address to the value?

record Dict where
  constructor MkDict
  dict_ptr: Felt

export
data LinDict : Type where
  MkLinDict : (1 _:Dict) -> LinDict

%foreign
    "imports:starkware.cairo.common.default_dict default_dict_new"
    "untupled:(_,_)"
    """
    code:
    func Common_Dict_dnew(default_value, world) -> (world, dict):
        let (dict_ptr) = default_dict_new(default_value)
        return (world, cast(dict_ptr, felt))
    end
    """
dnew :  Felt -> PrimCairo Felt

export
%foreign
    "imports:starkware.cairo.common.dict_access DictAccess, starkware.cairo.common.dict dict_read"
    "untupled:(_,_)"
    """
    code:
    func Common_Dict_dread(dict, key) -> (dict, value):
       let dict_end_ptr = cast(dict, DictAccess*)
       let (res) = dict_read{dict_ptr=dict_end_ptr}(key)
       return (cast(dict_end_ptr, felt), res)
    end
    """
dread : (1 d: LinDict) -> (key : Felt) -> (LinDict, Felt) -- The key must be present. Better would be Maybe Felt

export
%foreign
    "imports:starkware.cairo.common.dict_access DictAccess, starkware.cairo.common.dict dict_write"
    """
    code:
    func Common_Dict_dwrite(dict, key, value) -> (dict_ptr):
       let dict_end_ptr = cast(dict, DictAccess*)
       dict_write{dict_ptr=dict_end_ptr}(key, value)
       return (cast(dict_end_ptr, felt))
    end
    """
dwrite : (1 d: LinDict) -> (key : Felt) -> (value : Felt) -> LinDict

%foreign
    "imports:starkware.cairo.common.dict_access DictAccess, starkware.cairo.common.default_dict default_dict_finalize"
    "linear_implicits:range_check_ptr"
    """
    code:
    func Common_Dict_dverify(range_check_ptr, def_value, dict_start, dict_end, world) -> (world,range_check_ptr):
        let (squashed_dict_start, squashed_dict_end) = default_dict_finalize{range_check_ptr=range_check_ptr}(
             cast(dict_start, DictAccess*), cast(dict_end,DictAccess*), def_value)
       return (world, range_check_ptr)
    end
    """
    -- Should we return the squashed dict?
    -- Should we offer Verified Dict and Unverified dict? A write would lead to a linear Unverified dict.
dverify : (def_value:Felt) -> (dict_start:Felt) -> (1 _: LinDict) -> PrimCairoUnit

-- Creates a new dict which is then passed to the continutation k
-- At the end the dict is verified
public export %inline
dict : Felt -> (1 k : (1 d : LinDict ) -> (LinDict, a)) -> Cairo a
dict def k  = fromPrimCairo $ \(out_ptr) =>
       let MkCairoRes out_ptr' dict_start = dnew def out_ptr
           (dict_end, a) = k (MkLinDict $ MkDict dict_start)
           out_ptr'' = dverify def dict_start dict_end out_ptr'
        in MkCairoRes out_ptr'' a


text:
-- Streams

codata Stream : Type -> Type where
  head : Stream a -> a
  tail : Stream a -> Stream a
  constructor (::)

map : (a -> b) -> Stream a -> Stream b
head map f s = f (head s)
tail map f s = map f (tail s)

foldln : Nat -> (a -> b -> a) -> a -> Stream b -> a
foldln Z     f a s = a
foldln (S n) f a s = foldln f (f a (head s)) (tail s)

iterate : (a -> a) -> a -> Stream a
head iterate f a = a
tail iterate f a = iterate f (f a)

nats : Stream Nat
head nats = Z
tail nats = map S nats

repeat : a -> Stream a
head repeat a = a
tail repeat a = repeat a

cycle : Vect (S n) a -> Stream a
cycle xs = cycle' xs xs
  where cycle' : Vect (S n) a -> Vect m a -> Stream a
        head cycle' (x :: xs)       []  = x
        head cycle'       xs  (y :: ys) = y
        tail cycle' (x :: xs)       []  = cycle' (x :: xs) xs
        tail cycle'       xs  (y :: ys) = cycle' xs ys

take : (n : Nat) -> Stream a -> Vect n a
take Z     _ = []
take (S n) s = (head s) :: (take n (tail s))

drop : Nat -> Stream a -> Stream a
drop Z     s = s
drop (S n) s = drop n (tail s)

index : Nat -> Stream a -> a
index    Z  s = head s
index (S n) s = index n (tail s)

zip : Stream a -> Stream b -> Stream (a, b)
head zip s t = (head s, head t)
tail zip s t = zip (tail s) (tail t)

zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c
head zipWith f s t = f (head s) (head t)
tail zipWith f s t = zipWith f (tail s) (tail t)

unzip : Stream (a, b) -> (Stream a, Stream b)
unzip s = (map fst s, map snd s)

intersect : Stream a -> Stream a -> Stream a
head      intersect s t = head s
head tail intersect s t = head t
tail tail intersect s t = intersect (tail s) (tail t)

scanl : (a -> b -> a) -> a -> Stream b -> Stream a
head scanl f a s = a
tail scanl f a s = scanl f (f a (head s)) (tail s)

prepend : Vect n a -> Stream a -> Stream a
head prepend []        s = head s
head prepend (x :: xs) s = x
tail prepend []        s = tail s
tail prepend (x :: xs) s = prepend xs s

cons : a -> Stream a -> Stream a
head cons a s = a
tail cons a s = s

fib : Stream Nat
head      fib = Z
head tail fib = S Z
tail tail fib = zipWith (+) fib (tail fib)

mutual
  evens : Stream a -> Stream a
  head (evens s) = head s
  tail (evens s) = odds (tail s)

  odds : Stream a -> Stream a
  odds s = evens (tail s)

merge : Stream Nat -> Stream Nat
head (merge s t) = if (head s) <= (head t) then head s else head t
tail (merge s t) = if (head s) <= (head t) then
                      if (head t <= head s) then
                        merge (tail s) (tail t)
                      else
                        merge (tail s) t
                   else
                     merge s (tail t)

hamming : Stream Nat
head hamming = 1
tail hamming =
  (merge (map (\x -> 2 * x) hamming)
  (merge (map (\x -> 3 * x) hamming)
         (map (\x -> 5 * x) hamming)))

-- Binary Trees
codata BinTree : Type -> Type where
  value : BinTree a -> a
  left  : BinTree a -> BinTree a
  right : BinTree a -> BinTree a
  constructor _|_|_

map : (a -> b) -> BinTree a -> BinTree b
value f t = f (value t)
left  f t = map f (left t)
right f t = map f (right t)

fact : Nat -> Nat
fact Z   = S Z
fact S n = (S n) * (fact n)

-- This lacks a proof that we are not dividing by 0
choose : Nat -> Nat -> Nat
choose n k = (fact n) / ((fact k) * fact (n - k))

pascal : BinTree Nat
pascal = pascal' Z Z
  where pascal' : Nat -> Nat -> BinTree Nat
        value (pascal' n k) = choose n k
        left  (pascal' n k) = pascal' (S n)    k
        right (pascal' n k) = pascal' (S n) (S k)

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis


text:
module Meh

import public Control.WellFounded

public export
interface Argh (rel : a -> a -> Type) where
  argh : (x : a) -> Accessible rel x

data Meh : Nat -> Nat -> Type where

implementation Argh Meh where
  argh x = ?foo


text:
module Core.SchemeEval

-- Top level interface to the scheme based evaluator
-- Drops back to the default slow evaluator if scheme isn't available

import Core.Context
import Core.Core
import Core.Env
import Core.Normalise
import public Core.SchemeEval.Compile
import public Core.SchemeEval.Evaluate
import public Core.SchemeEval.Quote
import public Core.SchemeEval.ToScheme
import Core.TT

{-

Summary:

SObj vars
   ...is a scheme object with the scheme representation of the result
   of evaluating a term vars

SNF vars
   ...corresponds to NF vars, and is an inspectable version of the above.
   Evaluation is call by value, but there has not yet been any evaluation
   under lambdas

'Evaluate.seval' gets you an SObj from a Term
   - this involves compiling all the relevant definitions to scheme code
   first. We make a note of what we've compiled to scheme so we don't have
   to do it more than once.
`Evaluate.toSNF` gets you an SNF from an SObj
`Quote.quote` gets you back to a Term from an SNF

`snf` gets you directly to an SNF from a Term
`snormalise` packages up the whole process

All of this works only on a back end which can call scheme directly, and
with the relevant support files (currently: Chez)

-}

snormaliseMode : {auto c : Ref Ctxt Defs} ->
                 {vars : _} ->
                 SchemeMode -> Env Term vars -> Term vars -> Core (Term vars)
snormaliseMode mode env tm
    = do defs <- get Ctxt
         True <- initialiseSchemeEval
             | _ => normalise defs env tm
         sval <- seval mode env tm
         quoteObj sval

export
snormalise : {auto c : Ref Ctxt Defs} ->
             {vars : _} ->
             Env Term vars -> Term vars -> Core (Term vars)
snormalise = snormaliseMode BlockExport

export
snormaliseAll : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                Env Term vars -> Term vars -> Core (Term vars)
snormaliseAll = snormaliseMode EvalAll

export
snf : {auto c : Ref Ctxt Defs} ->
      {vars : _} ->
      Env Term vars -> Term vars -> Core (SNF vars)
snf env tm
    = do True <- initialiseSchemeEval
             | _ => throw (InternalError "Scheme evaluator not available")
         sval <- seval BlockExport env tm
         toSNF sval

export
snfAll : {auto c : Ref Ctxt Defs} ->
         {vars : _} ->
         Env Term vars -> Term vars -> Core (SNF vars)
snfAll env tm
    = do True <- initialiseSchemeEval
             | _ => throw (InternalError "Scheme evaluator not available")
         sval <- seval EvalAll env tm
         toSNF sval


text:
module Inigo.Async.SubtleCrypto.Example

import Inigo.Async.Promise
import Inigo.Async.SubtleCrypto.SubtleCrypto

-- Can be tested in a browser with:
-- idris2 SubtleCrypto/Example.idr --cg node -o testcrypto && cat build/exec/testcrypto | pbcopy

signAndVerify : Promise ()
signAndVerify =
  do
    let keyAlgo = (KeyECDSA P256)
    let algo = (ECDSA Sha256)
    (pub, priv) <- generateKey keyAlgo (Sign <&> Verify)
    privEnc <- exportKey priv
    privImp <- importKey keyAlgo Sign privEnc
    signature <- sign algo privImp "hello world"
    pubEnc <- exportKey pub
    pubImp <- importKey keyAlgo Verify pubEnc
    success <- verify algo pubImp signature "hello world"
    log ("Success: " ++ show success)

hashPassword : Promise ()
hashPassword =
  do
    salt <- getRand 8
    let algo = (PBKDF2 Sha256 salt 10000)
    hashed <- hash algo "my password"
    log ("Hashed: " ++ hashed)

main : IO ()
main =
  resolve hashPassword (\_ => pure ()) (\_ => pure ())

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module ContT

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

%access public export

data ContT : (r : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
  ContK : ((a -> m r) -> m r) -> ContT r m a

Cont : Type -> Type -> Type
Cont r a = ContT r Identity a

Functor (ContT r m) where
  map f (ContK c) = ContK (\k => c (\a => k (f a)))

Applicative (ContT r m) where
  pure a = ContK (\k => k a)
  (ContK cf) <*> (ContK c) = ContK (\k => c (\a => cf (\f => k (f a))))

Monad (ContT r m) where
  (ContK c) >>= f = ContK (\k => c (\a => let (ContK k') = f a in k' k))

MonadTrans (ContT r) where
  lift x = ContK (\k => x >>= k)

run : (a -> m r) -> ContT r m a -> m r
run f (ContK c) = c f

reset : Monad m => ContT r m r -> m r
reset (ContK c) = c (\x => pure x)

shift : Monad m => ((a -> m r) -> ContT r m r) -> ContT r m a
shift f = ContK (\k => reset (f k))

callCC : ((a -> ContT r m b) -> ContT r m a) -> ContT r m a
callCC f = ContK (\k => let (ContK c) = f (\a => ContK (\k' => k a)) in c k)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
||| An strict preorder (sometimes known as a quasi-order, or an
||| ordering) is what you get when you remove the diagonal `{(a,b) | a
||| r b , b r a}` from a preorder. For example a < b is an ordering.
||| This module extends base's Decidable.Order with the strict versions.
||| The interface system seems to struggle a bit with some of the constructions,
||| so I hacked them a bit. Sorry.
module Decidable.Order.Strict

import Decidable.Order
import Decidable.Equality

%default total

public export
interface StrictPreorder t (spo : t -> t -> Type) where
  transitive : (a, b, c : t) -> a `spo` b -> b `spo` c -> a `spo` c
  irreflexive : (a : t) -> Not (a `spo` a)

public export
asymmetric : StrictPreorder t spo => (a, b : t) -> a `spo` b -> Not (b `spo` a)
asymmetric a b aLTb bLTa = irreflexive a $
                           Strict.transitive a b a aLTb bLTa

public export
EqOr : (spo : t -> t -> Type) -> StrictPreorder t spo => (a,b : t) -> Type
EqOr spo a b = Either (a = b) (a `spo` b)

-- Can generalise to an arbitrary equivalence, I belive
public export
[MkPreorder] {spo : t -> t -> Type} -> StrictPreorder t spo => Preorder t (EqOr spo) where
  reflexive a = Left Refl
  transitive a _ c (Left  Refl) bLTEc        = bLTEc
  transitive a b _ (Right aLTb) (Left  Refl) = Right aLTb
  transitive a b c (Right aLTb) (Right bLTc) = Right $ Strict.transitive a b c aLTb bLTc

[MkPoset] {antisym : (a,b : t) -> a `leq` b -> b `leq` a -> a = b} -> Preorder t leq => Poset t leq where
  antisymmetric = antisym

%hint
public export
InferPoset : {t : Type} -> {spo : t -> t -> Type} -> StrictPreorder t spo => Poset t (EqOr spo)
InferPoset {t} {spo} = MkPoset @{MkPreorder} {antisym = antisym}
  where
    antisym : (a,b : t) -> EqOr spo a b -> EqOr spo b a -> a = b
    antisym a a (Left  Refl) (Left  Refl) = Refl
    antisym a a (Left  Refl) (Right bLTa) = absurd (irreflexive a bLTa)
    antisym b b (Right aLTb) (Left  Refl) = absurd (irreflexive b aLTb)
    antisym a b (Right aLTb) (Right bLTa) = absurd (asymmetric a b aLTb bLTa)

public export
data DecOrdering : {lt : t -> t -> Type} -> (a,b : t) -> Type where
  DecLT : forall lt . (a `lt` b) -> DecOrdering {lt = lt} a b
  DecEQ : forall lt . (a  =   b) -> DecOrdering {lt = lt} a b
  DecGT : forall lt . (b `lt` a) -> DecOrdering {lt = lt} a b

public export
interface StrictPreorder t spo => StrictOrdered t (spo : t -> t -> Type) where
  order : (a,b : t) -> DecOrdering {lt = spo} a b

[MkOrdered] {ord : (a,b : t) -> Either (a `leq` b) (b `leq` a)} -> Poset t leq => Ordered t leq where
  order = ord

%hint
public export
InferOrder : {t : Type} -> {spo : t -> t -> Type} -> StrictOrdered t spo => Ordered t (EqOr spo)
InferOrder {t} {spo} @{so} = MkOrdered @{InferPoset} {ord = ord}
  where
    ord : (a,b : t) -> Either (EqOr spo a b) (EqOr spo b a)
    ord  a b with (Strict.order @{so} a b)
     ord a _ | DecEQ Refl = Left  (Left  Refl)
     ord a b | DecLT aLTb = Left  (Right aLTb)
     ord a b | DecGT bLTa = Right (Right bLTa)

public export
(tot : StrictOrdered t lt) => (pre : StrictPreorder t lt) => DecEq t where
  decEq x y = case order @{tot} x y of
    DecEQ x_eq_y => Yes x_eq_y
    DecLT xlty => No $ \x_eq_y => absurd $ irreflexive @{pre} y
                                         $ replace {p = \u => u `lt` y} x_eq_y xlty
    -- Similarly
    DecGT yltx => No $ \x_eq_y => absurd $ irreflexive @{pre} y
                                         $ replace {p = \u => y `lt` u} x_eq_y yltx


text:
module Abishekrajan.Odds

import Evens

import Intro

data IsOdd : Nat -> Type where
  OneOdd : IsOdd 1
  SSOdd : (n : Nat) -> IsOdd n -> IsOdd (S (S n))

threeOdd : IsOdd 3
threeOdd = SSOdd 1 OneOdd

twoNotOdd : IsOdd 2 -> Void
twoNotOdd (SSOdd Z OneOdd) impossible
twoNotOdd (SSOdd Z (SSOdd x y)) impossible

nOddSnEven : (n: Nat) -> IsOdd n -> IsEven (S n)
nOddSnEven (S Z) OneOdd = (SSEven Z ZEven)
nOddSnEven (S (S k)) (SSOdd k x) = SSEven (S k) (nOddSnEven k x)

nEvenSnOdd : (n: Nat) -> IsEven n -> IsOdd (S n)
nEvenSnOdd Z ZEven = OneOdd
nEvenSnOdd (S (S k)) (SSEven k x) = SSOdd (S k) (nEvenSnOdd k x)

nEvenOrOdd : (n: Nat) -> Either (IsEven n) (IsOdd n)
nEvenOrOdd Z = Left ZEven
nEvenOrOdd (S k) = case (nEvenOrOdd k) of
                       (Left l) => Right (nEvenSnOdd k l)
                       (Right r) => Left (nOddSnEven k r)

nNotEvenAndOdd : (n: Nat) -> (IsEven n) -> (IsOdd n) -> Void
nNotEvenAndOdd Z ZEven OneOdd impossible
nNotEvenAndOdd Z ZEven (SSOdd p q) impossible
nNotEvenAndOdd (S (S k)) (SSEven k x) (SSOdd k y) = nNotEvenAndOdd k x y

mOddnOddmplusnEven : (m: Nat) -> IsOdd m -> (n: Nat) -> IsOdd n -> IsEven (add m n)
mOddnOddmplusnEven (S Z) OneOdd (S Z) OneOdd = SSEven 0 ZEven
mOddnOddmplusnEven (S Z) OneOdd (S (S k)) (SSOdd k x) = SSEven (S k) (mOddnOddmplusnEven (S Z) OneOdd k x)
mOddnOddmplusnEven (S (S k)) (SSOdd k x) n y = SSEven (add k n) (mOddnOddmplusnEven k x n y)

apNat : (f: Nat -> Nat) -> (n: Nat) -> (m: Nat) -> n = m -> f n = f m
apNat f m m Refl = Refl

oddIsSDouble : (n: Nat) -> IsOdd n -> (k: Nat ** (S (double k)) = n)
oddIsSDouble (S Z) OneOdd = (0 ** Refl)
oddIsSDouble (S (S k)) (SSOdd k x) = case (oddIsSDouble k x) of
            (m ** y) => ((S m) ** apNat (\l => S (S l)) (S (double m)) k y)


text: module PQ.SQL.Query


text:
module EqInterf

import Data.Nat

infix 6 =~=

--------------------------------------------------
--- Interfaces and general functions over them ---
--------------------------------------------------

interface Equ ty where
  data (=~=) : ty -> ty -> Type

  0 fromPropositional : {0 x, y : ty} -> (0 _ : x = y) -> x =~= y

  0 reflexivity  : {0 x : ty} -> x =~= x
  0 symmetry     : {0 x, y : ty} -> (0 _ : x =~= y) -> y =~= x
  0 transitivity : {0 x, y, z : ty} -> (0 _ : x =~= y) -> (0 _ : y =~= z) -> x =~= z

interface Equ ty => Transp ty where
  0 transport : (0 p : ty -> Type) -> {0 x, y : ty} -> (0 _ : x =~= y) -> p x -> p y

0 congruence : Transp ty => Equ tu => (0 f : ty -> tu) -> {0 x, y : ty} -> (0 _ : x =~= y) -> f x =~= f y
congruence f xy = transport (\i => f x =~= f i) xy reflexivity

interface Equ ty => EquProp ty where
  0 equIsProp : (=~=) {ty} = Equal

--interface Equ t => Equ u => Cong t u (0 f : t -> u) where
--  0 congruence : {0 x, y : t} -> (0 _ : x =~= y) -> f x =~= f y

interface Equ t => Equ u => Inj t u (0 f : t -> u) where
  0 injectivity : {0 x, y : t} -> (0 _ : f x =~= f y) -> x =~= y

---------------------------------------------
--- Interfaces' implementations for `Nat` ---
---------------------------------------------

Equ Nat where
  (=~=) = Equal

  fromPropositional Refl = Refl

  reflexivity  = Refl
  symmetry     = sym
  transitivity = trans

Transp Nat where
  transport _ Refl p = p

EquProp Nat where
  equIsProp = Refl

Inj _ _ S where
  injectivity Refl = Refl

0 injPlusL : {n : Nat} -> (n + x = n + y) -> x = y
injPlusL {n=Z}   eq = eq
injPlusL {n=S k} eq = injPlusL $ injectivity {f=S} eq

Inj Nat _ (n+) where
  injectivity eq = injPlusL eq

Inj Nat _ (+n) where
  injectivity eq = injPlusL {n} rewrite plusCommutative n x in rewrite plusCommutative n y in eq

----------------------------------------------------------
--- Equality for functions as functional extensinality ---
----------------------------------------------------------

[WeakFunext] Equ b => Equ (a -> b) where
  f =~= g = (x : a) -> f x =~= g x

  fromPropositional Refl = \_ => reflexivity

  reflexivity      _ = reflexivity
  symmetry p       x = symmetry $ p x
  transitivity p q x = transitivity (p x) (q x)

[WeakFunextTransp] Equ b => Transp (a -> b) using WeakFunext where
  transport {x=f} {y=g} pr fg p = ?foo_transport -- impossible since implies actual functional extensionality

[StrongFunext] Transp a => Equ b => Equ (a -> b) where
  f =~= g = (x, y : a) -> x =~= y -> f x =~= g y

  fromPropositional {y=f} Refl = \_, _, xy => congruence f xy

  reflexivity {x=f} = \_, _, xx => congruence f xx
  symmetry {x=f} {y=g} fg = \x, y, xy => symmetry $ fg y x $ symmetry xy
  transitivity {x=f} {y=g} {z=h} fg gh = \x, y, xy => fg x y xy `transitivity` gh y y reflexivity

[StrongFunextTransp] Transp a => Equ b => Transp (a -> b) using StrongFunext where
  transport {x=f} {y=g} pr fg p = ?foo0 -- impossible since implies actual functional extensionality


text:
import Data.Vect

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

oneInVector : Elem 1 [1, 2, 3]
oneInVector = Here

maryInVector : Elem "Mary" ["Peter", "Paul", "Mary"]
maryInVector = There (There Here)

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


text:
%default total

partial
foo : Nat -> Nat
foo Z = Z

partial
bar : Nat -> Nat
bar n with (0)
 bar n | k = foo n


text:
AdderType : (numargs : Nat) -> Type -> Type
AdderType Z numType = numType
AdderType (S k) numType = (next : numType) -> AdderType k numType

adder : Num numType => (numargs : Nat) -> numType -> AdderType numargs numType
adder Z acc = acc
adder (S k) acc = \next => adder k (next + acc)

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


text:
{-
A 42
-}

module Main

data V a = A a

instance Show a => Show (V a) where
  show (A a) = "A " ++ show a

main : IO ()
main = printLn $ A 42

max_stars_repo_name: Despair/idris-cil

max_issues_repo_name: Despair/idris-cil

max_forks_repo_name: Despair/idris-cil


text:
module D

-- %logging 10
func1 : Applicative f => (a -> f c) -> (b -> f d) -> (a, b) -> f (c, d)
func1 fn g (ma, mb) = MkPair <$> fn ma <*> ?gmb
-- %logging 0

-- %logging 10
mfunc : (a -> Maybe c) -> (b -> Maybe d) -> (a, b) -> Maybe (c, d)
mfunc fn g (ma, mb)
   = let pairapp = MkPair <$> fn ma in
         pairapp <*> g mb
%logging 0

func2 : (a -> c) -> (b -> d) -> a -> b -> (c, d)
func2 f g a b = MkPair (f a) (g b)


text:
module Issue1831_1

export
fooFromInteger : Num x => Integer -> x
fooFromInteger x = fromInteger (x + x)

%integerLit Issue1831_1.fooFromInteger

test : Nat
test = 5 + 6

test2 : Nat -> Bool
test2 1 = True
test2 _ = False


text:
module Mmhelloworld.IdrisSpringBoot.Context.Annotation

import IdrisJvm.IO

%access public export

term syntax "<@Bean>" [attrs] = <@> "org/springframework/context/annotation/Bean" attrs

max_stars_repo_name: mmhelloworld/idris-spring-boot

max_issues_repo_name: mmhelloworld/idris-spring-boot

max_forks_repo_name: mmhelloworld/idris-spring-boot


text:
module IntBits

import IntCasts
import IntEqOrd
import IntNum

import Data.Bits
import Data.DPair

-- This file to be deleted once these interfaces are added to base

public export %inline
Bits Int8 where
  Index       = Subset Nat (`LT` 8)
  (.&.)       = prim__and_Int8
  (.|.)       = prim__or_Int8
  xor         = prim__xor_Int8
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Int8 x . cast . fst
  shiftL x    = prim__shl_Int8 x . cast . fst
  complement  = xor (-1)
  oneBits     = -1

public export %inline
Bits Int16 where
  Index       = Subset Nat (`LT` 16)
  (.&.)       = prim__and_Int16
  (.|.)       = prim__or_Int16
  xor         = prim__xor_Int16
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Int16 x . cast . fst
  shiftL x    = prim__shl_Int16 x . cast . fst
  complement  = xor (-1)
  oneBits     = -1

public export %inline
Bits Int32 where
  Index       = Subset Nat (`LT` 32)
  (.&.)       = prim__and_Int32
  (.|.)       = prim__or_Int32
  xor         = prim__xor_Int32
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Int32 x . cast . fst
  shiftL x    = prim__shl_Int32 x . cast . fst
  complement  = xor (-1)
  oneBits     = -1

public export %inline
Bits Int64 where
  Index       = Subset Nat (`LT` 64)
  (.&.)       = prim__and_Int64
  (.|.)       = prim__or_Int64
  xor         = prim__xor_Int64
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Int64 x . cast . fst
  shiftL x    = prim__shl_Int64 x . cast . fst
  complement  = xor (-1)
  oneBits     = -1

public export %inline
Bits Bits64 where
  Index       = Subset Nat (`LT` 64)
  (.&.)       = prim__and_Bits64
  (.|.)       = prim__or_Bits64
  xor         = prim__xor_Bits64
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Bits64 x . fromInteger . cast . fst
  shiftL x    = prim__shl_Bits64 x . fromInteger . cast . fst
  complement  = xor 0xffffffffffffffff
  oneBits     = 0xffffffffffffffff

public export %inline
Bits Integer where
  Index       = Nat
  (.&.)       = prim__and_Integer
  (.|.)       = prim__or_Integer
  xor         = prim__xor_Integer
  bit         = (1 `shiftL`)
  zeroBits    = 0
  testBit x i = (x .&. bit i) /= 0
  shiftR x    = prim__shr_Integer x . cast
  shiftL x    = prim__shl_Integer x . cast
  complement  = xor (-1)
  oneBits     = (-1)

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Compiler.Identity

import Compiler.CompileExpr
import Core.Context
import Core.Context.Log

getArg : FC -> Nat -> (args : List Name) -> Maybe (CExp args)
getArg _ _ [] = Nothing
getArg fc Z (a :: _) = Just $ CLocal fc First
getArg fc (S k) (_ :: as) = weaken <$> getArg fc k as

idCDef : Nat -> CDef -> Maybe CDef
idCDef idx (MkFun args exp) = MkFun args <$> getArg (getFC exp) idx args
idCDef _ def = Just def

export
setIdentity : Ref Ctxt Defs => Name -> Core ()
setIdentity fn = do
    log "compiler.identity" 10 $ "processing identity flag for: " ++ show fn
    defs <- get Ctxt
    Just gdef <- lookupCtxtExact fn defs.gamma
        | Nothing => pure ()
    log "compiler.identity" 25 $ "flags for " ++ show fn ++ ": " ++ show gdef.flags
    let Just flg@(Identity idx) = find isId gdef.flags
        | _ => pure ()
    log "compiler.identity" 5 $ "found identity flag for: " ++ show fn ++ ", " ++ show idx
                             ++ "\n\told def: " ++ show gdef.compexpr
    let Just cdef = the _ $ gdef.compexpr >>= idCDef idx
        | Nothing => pure ()
    log "compiler.identity" 15 $ "new def: " ++ show cdef
    unsetFlag EmptyFC fn flg -- other optimisations might mess with argument counts
    setCompiled fn cdef
  where
    isId : DefFlag -> Bool
    isId (Identity _) = True
    isId _ = False


text:
module Hedgehog

import public Control.Monad.Either
import public Control.Monad.Writer
import public Hedgehog.Internal.Gen as Hedgehog
import public Hedgehog.Internal.Property as Hedgehog
import public Hedgehog.Internal.Range as Hedgehog
import public Hedgehog.Internal.Runner as Hedgehog
import public Hedgehog.Internal.Seed as Hedgehog
import public Hedgehog.Internal.Shrink as Hedgehog
import public Hedgehog.Internal.Util as Hedgehog