text:
module Main

import Data.Strings

data MyEither a b = MyLeft a | MyRight b

data MyDecEq : Type -> Type where
  MyYes : a           -> MyDecEq a
  MyNo  : (a -> Void) -> MyDecEq a

myDec1 : MyDecEq Char
myDec1 = MyYes 'a'

myDec2 : MyDecEq Char
myDec2 = MyNo ?absurd

test : Int
test = ?test1

test3 : Int -> Int -> Int
test3 x y = x

data MyStream : Type -> Type where
  MkMyStream : Lazy a -> Inf (MyStream a) -> MyStream a

mkStream : a -> MyStream a
mkStream x = MkMyStream x (mkStream x)

headS : MyStream a -> a
headS (MkMyStream x _) = x

tailS : MyStream a -> MyStream a
tailS (MkMyStream _ xs) = xs

data MyStream2 : Type -> Type where
  MkMyStream2 : a -> MyStream2 a -> MyStream2 a
  MkMyStream2N : MyStream2 a

myStream2 : a -> MyStream2 a
myStream2 x = MkMyStream2 x (myStream2 x)

heads2 : MyStream2 a -> Maybe a
heads2 MkMyStream2N = Nothing
heads2 (MkMyStream2 x _) = Just x

%foreign "stg:prim__consoleLog = base:Prelude.putStrLn"
prim__consoleLog : String -> PrimIO ()
export
consoleLog : HasIO io => String -> io ()
consoleLog x = primIO $ prim__consoleLog x

%foreign "stg:prim__applyFnIO = base:Prelude.somewhat"
prim__applyFnIO : String -> Int -> (String -> Int -> PrimIO String) ->
                 PrimIO String
applyFnIO : HasIO io =>
            String -> Int -> (String -> Int -> IO String) -> io String
applyFnIO c i f = primIO $ prim__applyFnIO c i (\s, i => toPrim $ f s i)

data MyBuffer : Type -> Type where [external]

%foreign "stg:prim__myBuffer = base:Prelude.myBuffer"
prim__myBuffer : PrimIO (MyBuffer Int)
myBuffer : HasIO io => io (MyBuffer Int)
myBuffer = primIO prim__myBuffer

data ThreadID1 : Type where [external]

%foreign "stg:prim__fork = base:Something.something"
prim__fork : (1 prog : PrimIO ()) -> PrimIO ThreadID1

fork : (1 prog : IO ()) -> IO ThreadID1
fork act = fromPrim (prim__fork (toPrim act))

partial
main : IO ()
main = do
  name <- getLine
  let nm1 = the (MyEither String String) (MyLeft name)
  let md1 = the (MyDecEq Char) (MyYes 'a')
  putStrLn $ strTail $ "!Hello " ++ name
  case nm1 of
    MyLeft n => printLn $ fastUnpack n
    MyRight n => printLn $ fastUnpack n
  case md1 of
    MyYes a => printLn $ show a
    MyNo _ => printLn $ "Noooo!"
  printLn $ test3 1 test
  consoleLog "BLAH!"
  str <- applyFnIO "hello" 1 (\s, i => do { printLn (s,i); pure s})
  bfr <- myBuffer
  tid <- Main.fork (putStrLn "Hello Fork!")
  printLn $ headS $ tailS $ mkStream 4
  printLn $ heads2 $ myStream2 5
  pure ()

{-
Main.prim__applyFnIO = Foreign call ["stg:prim__applyFnIO = base:Prelude.somewhat"] [String, Int, String -> Int -> %World -> IORes String, %World] -> IORes
Main.{applyFnIO:1} = [0, 1, 2, 3, 4, 5, 6, 7]: %let v8 = (<Main.{applyFnIO:0} underapp 2>(v7, v0, v1, v2, v3, v4, v5, v6)) in (Main.prim__applyFnIO(v4, v5, v8, v7))
Main.applyFnIO = [0, 1, 2, 3, 4]: %case v1 of { %conalt Prelude.IO.HasIO at Prelude/IO.idr:33:1--35:32(v5, v6) => %let v7 = (v6 @ ([__])) in (%let v8 = (<Main.{applyFnIO:1} underapp 1>(v5, v6, v0, v1, v2, v3, v4)) in (v7 @ (v8))) Nothing }
-}

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Data.OrderedVect

import Decidable.Order

%default total

mutual
  public export
  data OrderedVect : Nat -> (constraint : Ordered ty to) -> Type where
    Nil : .{auto constraint : Ordered ty to}
        -> OrderedVect Z constraint
    (::) : .{constraint : Ordered ty to}
        -> (x : ty)
        -> (v : OrderedVect n constraint)
        -> .{auto prf : Fits x v}
        -> OrderedVect (S n) constraint

  public export
  Fits : {constraint : Ordered ty to} -> ty -> OrderedVect n constraint -> Type
  Fits _ Nil = ()
  Fits n (m :: _) = to n m

%name OrderedVect xs,ys,zs

export
head : .{constraint : Ordered ty to} -> OrderedVect (S _) constraint -> ty
head (x :: _) = x

fitsTrans : (Fits {constraint} x ys) -> Fits {constraint} (head ys) zs -> Fits {constraint} x zs
fitsTrans {zs = []} _ _ = ()
fitsTrans {x} {ys = y' :: _} {zs = z' :: _} rel1 rel2 = transitive x y' z' rel1 rel2

mutual
  merge' : .{constraint : Ordered ty to}
        -> {n : Nat}
        -> (v1 : OrderedVect (S n) constraint)
        -> {m : Nat}
        -> (v2 : OrderedVect (S m) constraint)
        -> (ret : OrderedVect ((S n) + (S m)) constraint ** Either (Fits (head v1) ret) (Fits (head v2) ret))
  merge' [] _ impossible
  merge' _ [] impossible
  merge' {to} [x] [y] = case order {to} x y of
                        Left prf => ([x, y] ** Left (reflexive x))
                        Right prf => ([y, x] ** Right (reflexive y))
  merge' {m} [x] (y :: ys) = rewrite sym $ plusZeroRightNeutral m in
                             rewrite plusSuccRightSucc m Z in
                             case assert_total $ merge' (y :: ys) [x] of
                             (ref ** Left prf) => (ref ** Right prf)
                             (ref ** Right prf) => (ref ** Left prf)
  merge' {n = S cntX} (x :: xs) [y]
    = case order {to} x y of
      Left prf => case mergeHelper xs [y] x of
                  (zs ** fitsPrf) => (zs ** Left fitsPrf)
      Right prf => rewrite sym $ plusSuccRightSucc cntX Z in
                   rewrite plusZeroRightNeutral cntX in
                   ((y :: x :: xs) ** Right (reflexive y))
  merge' ((::) {n = S cntX} x (x' :: xs'))
        ((::) {n = S cntY} y (y' :: ys'))
    = case order {to} x y of
      Left prf => case mergeHelper (x' :: xs') (y :: y' :: ys') x of
                  (zs ** fitsPrf) => (zs ** Left fitsPrf)
      Right prf => case mergeHelper (y' :: ys') (x :: x' :: xs') y of
                   (zs ** fitsPrf) => rewrite plusCommutative cntX (S $ S $ cntY) in
                                      rewrite plusSuccRightSucc (S $ S cntY) cntX in
                                      rewrite plusSuccRightSucc (S cntY) (S cntX) in
                                      (zs ** Right fitsPrf)
  mergeHelper : .{constraint : Ordered ty to}
             -> {n : Nat}
             -> (xs : OrderedVect (S n) constraint)
             -> {m : Nat}
             -> (ys : OrderedVect (S m) constraint)
             -> (x : ty)
             -> .{auto prfXs : Fits x xs}
             -> .{auto prfYs : Fits x ys}
             -> (ret : OrderedVect (S $ (S n) + (S m)) constraint ** Fits x ret)
  mergeHelper xs ys x {prfXs} {prfYs}
    = case assert_total $ merge' xs ys of
      (zs ** Left fitsPrf) => let _ = fitsTrans prfXs fitsPrf in
                              (x :: zs ** reflexive x)
      (zs ** Right fitsPrf) => let _ = fitsTrans prfYs fitsPrf in
                               (x :: zs ** reflexive x)

export
merge : {constraint : Ordered ty to}
     -> (n : Nat)
     -> OrderedVect n constraint
     -> (m : Nat)
     -> OrderedVect m constraint
     -> OrderedVect (n + m) constraint
merge Z     [] Z     [] = Nil
merge n     v1 Z     [] = rewrite plusZeroRightNeutral n in v1
merge Z     [] _     v2 = v2
merge (S _) v1 (S _) v2 = fst $ merge' v1 v2

export
tail : OrderedVect (S n) constraint -> OrderedVect n constraint
tail (_ :: v) = v

export
orderedVectToList : .{constraint : Ordered ty _} -> OrderedVect n constraint -> List ty
orderedVectToList [] = []
orderedVectToList {n = S _} (x :: xs) = x :: (orderedVectToList xs)

ext: idr

max_stars_repo_name: jdevuyst/idris-data

max_issues_repo_name: jdevuyst/idris-data

max_forks_repo_name: jdevuyst/idris-data


text:
foo : Int -> Int
foo x = x

bar : Int -> Int
bar x = if x == 95 then 0

baz : Int -> Int
baz x = x


text:
{-
False
foobar
oof
rab
True
foofoo
oof
oof
(Hello)
()
( Idris)
(s)
(s!)
'I'
'd'
'r'
'i'
's'
"foo" < "foo" => False
"foo" <= "foo" => True
"foo" == "foo" => True
"foo" >= "foo" => True
"foo" > "foo" => False
"foo" max "foo" => "foo"
"foo" min "foo" => "foo"
"foo" < "bar" => False
"foo" <= "bar" => False
"foo" == "bar" => False
"foo" >= "bar" => True
"foo" > "bar" => True
"foo" max "bar" => "foo"
"foo" min "bar" => "bar"
"bar" < "foo" => True
"bar" <= "foo" => True
"bar" == "foo" => False
"bar" >= "foo" => False
"bar" > "foo" => False
"bar" max "foo" => "foo"
"bar" min "foo" => "bar"
"bar" < "bar" => False
"bar" <= "bar" => True
"bar" == "bar" => True
"bar" >= "bar" => True
"bar" > "bar" => False
"bar" max "bar" => "bar"
"bar" min "bar" => "bar"
-}
module Main

test : String -> String -> IO ()
test s1 s2 = do printLn $ s1 == s2
                putStrLn $ s1 ++ s2
                for_ [s1, s2] $ putStrLn . reverse

testSubstr : (Nat, Nat) -> IO ()
testSubstr (index, length) = putStrLn $ "(" ++ (substr index length "Hello, Idris!") ++ ")"

testOrd : IO ()
testOrd = traverse_ putStrLn (test strings strings)
  where
    strings = [ "foo", "bar" ]

    op : Show r => String -> (String -> String -> r) -> (String -> String -> String)
    op name o = \x, y => show x ++ " " ++  name ++ " " ++ show y ++ " => " ++ show (x `o` y)

    operators : List (String -> String -> String)
    operators = [ op "<" (<), op "<=" (<=), op "==" (==)
                , op ">=" (>=), op ">" (>)
                , op "max" max, op "min" min ]

    test : List String -> List String -> List String
    test xs ys = do
      x <- xs
      y <- ys
      map (\o => x `o` y) operators

main : IO ()
main = do
  test "foo" "bar"
  test "foo" "foo"
  traverse_ testSubstr [(0, 5), (20, 5), (6, 6), (11, 1), (11, 5)]
  traverse_ (putStrLn . show . strIndex "Idris") [0..4]
  testOrd

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module Part2.Sec6_3b_datastore
import Data.Vect
import Util.MiniParser

%default total

infixr 5 .+.

||| ADT that represents parsed schema
data Schema = SString
            | SInt
            | (.+.) Schema Schema

||| Type level function that maps Schema to actual type, composite schema
||| is mapped to a tuple.
SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

{-
idris repl:
*src/Part2/Sec6_3_datastore> SchemaType (SInt .+. SString .+. SInt)
(Int, String, Int) : Type
-}

{- This needs schema type parameter to cary the schema information around -}
||| Type representing user commands (DSL)
data Command : Schema -> Type where
           -- works in context of old schema, polymorphic in the return type
           SetSchema : (newschema : Schema) -> Command schema
           Add : SchemaType schema -> Command schema
           Get : Integer -> Command schema
           Quit : Command schema

{- This is powerful. Some of this can be mimicked in Haskell, e.g.
`singletons` library could generate type family Schema :: DataStore -> Schema from
something like `data DataStore = DataStore{ schema :: Schema}`
but cross referencing between field values and field types is beyond what I can
do in Haskell, also record 'getters' are not automatically lifted by `DataKinds` -}
record DataStore where
       constructor MkData
       schema : Schema
       size : Nat
       items : Vect size (SchemaType schema)

{-
teststore = MkData (SInt .+. SString .+. SInt) 1 [(2, "Two", 42)]
-}

{- helper methods used with DataStore, note cool use of record getter at type level -}

addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
addToStore (MkData schema size store) newitem
           = MkData schema _ (addToData store)
  where
    addToData : Vect oldsize (SchemaType schema) -> Vect (S oldsize) (SchemaType schema)
    addToData [] = [newitem]
    addToData (item :: items) = item :: addToData items

display : SchemaType schema -> String
display {schema = SString} item = show item
display {schema = SInt} item = show item
display {schema = (x .+. y)} (iteml, itemr)
            = display iteml ++ ", " ++ display itemr

{- Changed from the book version to emphasize type safe retrieval -}
retrieve : (pos : Integer) -> (store : DataStore) -> Maybe (SchemaType (schema store))
retrieve pos store =
      integerToFin pos (size store) >>= (\i => pure (index i (items store)))

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store = case retrieve pos store of
             Nothing => Just ("Out of range\n", store)
             Just rec => Just ((display rec) ++ "\n", store)

setSchema : (store : DataStore) -> Schema -> Maybe DataStore
setSchema store schema = case size store of
       Z => Just (MkData schema _ [])
       S k => Nothing

{- Parsers -}
sstring : Parser Schema
sstring =  string "String" *> pure SString

sint : Parser Schema
sint = string "Int" *> pure SInt

scolumn : Parser Schema
scolumn = sstring <|> sint

covering
schemaBody : Parser Schema
schemaBody = do
     col  <- scolumn
     _    <- optional spaces
     rest <- optional schemaBody
     case rest of
        Nothing =>  pure col
        Just rest => pure (col .+. rest)

{- Note Idris has no problem with this name being overloaded -}
covering
schema : Parser Schema
schema = string "schema" *> spaces *> schemaBody

covering
schemaTypeBody : (sch : Schema) -> Parser (SchemaType sch)
schemaTypeBody SString = between (char '"') (char '"')
schemaTypeBody SInt = decimalInt
schemaTypeBody (schemal .+. schemar) = do
                parsed1 <- schemaTypeBody schemal
                _    <- spaces
                parsed2 <- schemaTypeBody schemar
                pure (parsed1, parsed2)

covering
schemaType : (sch : Schema) -> Parser (SchemaType sch)
schemaType sch = string "add" *> spaces *> schemaTypeBody sch

covering
command : (sc : Schema) -> Parser (Command sc)
command sc = (SetSchema <$> schema) <|>
             (string "quit" *> pure Quit) <|>
             (string "get") *> spaces *> (Get <$> decimalInteger) <|>
             (Add <$> schemaType sc)

{- End Parsers -}

||| replWith implementation method
covering
processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
          = case parseAll (command (schema store)) input of
                 Left msg => Just ("Invalid command: " ++ msg ++ "\n", store)
                 Right (Add item) =>
                    Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
                 Right (Get pos) => getEntry pos store
                 Right (SetSchema schema') => case setSchema store schema' of
                        Nothing => Just ("Can't update schema\n", store)
                        Just store' => Just ("OK\n", store')
                 Right Quit => Nothing

initDs : DataStore
initDs = MkData SString _ []

testDs : DataStore
testDs = MkData (SInt .+. SString) _ []

{- To execute in repl, idrs repl from src folder, :l this file and use :exec sec6_3b -}
export
covering
sec6_3b : IO ()
sec6_3b = replWith initDs "Command: " processInput

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
data Matter = Solid | Liquid | Gas

Eq Matter where
    (==) Solid Solid = True
    (==) Liquid Liquid = True
    (==) Gas Gas = True
    (==) _ _ = False

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Interfaces.VerifiedOrd

import Data.Fin

%default total
%access public export

typeOf : (x : a) -> Type
typeOf {a} x = a

reverseOrd : Ordering -> Ordering
reverseOrd EQ = EQ
reverseOrd LT = GT
reverseOrd GT = LT

orderPair : Ordering -> Ordering -> Ordering
orderPair EQ x = x
orderPair x  _ = x

data DecOrd : Ordering -> Type where
  IsEQ : (o = EQ) -> DecOrd o
  IsLT : (o = LT) -> DecOrd o
  IsGT : (o = GT) -> DecOrd o

decOrd : (o : Ordering) -> DecOrd o
decOrd EQ = IsEQ Refl
decOrd GT = IsGT Refl
decOrd LT = IsLT Refl

decOrdEq : (o : Ordering) -> Dec (o = EQ)
decOrdEq EQ = Yes Refl
decOrdEq LT = No (\Refl impossible)
decOrdEq GT = No (\Refl impossible)

interface VerifiedOrd a where
  order : a -> a -> Ordering
  ordRefl : (x : a) -> order x x = EQ
  reflOrd : (x : a) -> (y : a) -> order x y = EQ -> x = y
  ordSym  : (x : a) -> (y : a) -> order x y = reverseOrd (order y x)
  ordTrans : (left : a) -> (middle : a) -> (right : a) -> order left middle = order middle right -> order left middle = order left right

ordRefl' : VerifiedOrd a => (x : a) -> (y : a) -> (x = y) -> order x y = EQ
ordRefl' x x Refl = ordRefl x

decEqVerifiedOrd : VerifiedOrd a => (x : a) -> (y : a) -> Dec (x = y)
decEqVerifiedOrd x y with (decOrdEq (order x y))
  | Yes p = Yes $ reflOrd x y p
  | No  p = No  $ \xeqy => p $ ordRefl' x y xeqy

implementation VerifiedOrd () where
  order = compare
  ordRefl () = Refl
  reflOrd () () _ = Refl
  ordSym () () = Refl
  ordTrans () () () _ = Refl

implementation VerifiedOrd Bool where
  order = compare
  ordRefl True = Refl
  ordRefl False = Refl
  reflOrd True True _ = Refl
  reflOrd True False Refl impossible
  reflOrd False True Refl impossible
  reflOrd False False _ = Refl
  ordSym True True = Refl
  ordSym True False = Refl
  ordSym False True = Refl
  ordSym False False = Refl
  ordTrans False False False _ = Refl
  ordTrans True True True _ = Refl
  ordTrans False False True Refl impossible
  ordTrans False True False Refl impossible
  ordTrans True False False Refl impossible
  ordTrans False True True Refl impossible
  ordTrans True False True Refl impossible
  ordTrans True True False Refl impossible

pair_ordTrans_lemma1 : (VerifiedOrd a, VerifiedOrd b) =>
                       {l1, m1, r1 : a} ->
                       {l2, m2, r2 : b} ->
                       (order l1 m1 = GT) ->
                       (order m1 r1 = LT) ->
                       (orderPair (order l1 m1) (order l2 m2) = orderPair (order m1 r1) (order m2 r2)) ->
                       Void
pair_ordTrans_lemma1 p1 p2 = rewrite p1 in rewrite p2 in \Refl impossible

pair_ordTrans_lemma2 : (VerifiedOrd a, VerifiedOrd b) =>
                       {l1, m1, r1 : a} ->
                       {l2, m2, r2 : b} ->
                       (order l1 m1 = LT) ->
                       (order m1 r1 = GT) ->
                       (orderPair (order l1 m1) (order l2 m2) = orderPair (order m1 r1) (order m2 r2)) ->
                       Void
pair_ordTrans_lemma2 p1 p2 = rewrite p1 in rewrite p2 in \Refl impossible

pair_ordTrans_lemma3 : (VerifiedOrd a, VerifiedOrd b) =>
                       (l1 : a) ->
                       (m1 : a) ->
                       (r1 : a) ->
                       (l2 : b) ->
                       (m2 : b) ->
                       (r2 : b) ->
                       (order l1 m1 = EQ) ->
                       (order m1 r1 = EQ) ->
                       (orderPair (order l1 m1) (order l2 m2) = orderPair (order m1 r1) (order m2 r2)) ->
                       (order l2 m2 = order m2 r2)
pair_ordTrans_lemma3 _ _ _ _ _ _ p1 p2 = rewrite p1 in rewrite p2 in \x => x

pair_ordTrans_lemma4 : (VerifiedOrd a, VerifiedOrd b) =>
                       (l1 : a) ->
                       (m1 : a) ->
                       (r1 : a) ->
                       (l2 : b) ->
                       (m2 : b) ->
                       (r2 : b) ->
                       (order l1 m1 = EQ) ->
                       (order m1 r1 = LT) ->
                       (orderPair (order l1 m1) (order l2 m2) = orderPair (order m1 r1) (order m2 r2)) ->
                       (order l2 m2 = LT)
pair_ordTrans_lemma4 _ _ _ _ _ _ p1 p2 = rewrite p1 in rewrite p2 in \x => x

pair_ordTrans_lemma5 : (VerifiedOrd a, VerifiedOrd b) =>
                       (l1 : a) ->
                       (m1 : a) ->
                       (r1 : a) ->
                       (l2 : b) ->
                       (m2 : b) ->
                       (r2 : b) ->
                       (order l1 m1 = EQ) ->
                       (order m1 r1 = GT) ->
                       (orderPair (order l1 m1) (order l2 m2) = orderPair (order m1 r1) (order m2 r2)) ->
                       (order l2 m2 = GT)
pair_ordTrans_lemma5 _ _ _ _ _ _ p1 p2 = rewrite p1 in rewrite p2 in \x => x

implementation (VerifiedOrd a, VerifiedOrd b) => VerifiedOrd (a, b) where
  order (x1, x2) (y1, y2) = orderPair (order x1 y1) (order x2 y2)
  ordRefl (x1, x2) = rewrite ordRefl x1 in ordRefl x2
  reflOrd (x1, x2) (y1, y2) p with (decOrdEq (order x1 y1))
    | Yes p2 with (reflOrd x1 y1 p2)
      reflOrd (x1, x2) (x1, y2) p | Yes p2 | Refl with (order x1 x1)
        | EQ = rewrite reflOrd x2 y2 p in Refl
        reflOrd (_, _) (_, _) Refl | Yes _ | Refl | LT impossible
        reflOrd (_, _) (_, _) Refl | Yes _ | Refl | GT impossible
    | No p2 with (order x1 y1)
      reflOrd (_, _) (_, _) Refl | No _ | GT impossible
      reflOrd (_, _) (_, _) Refl | No _ | LT impossible
      | EQ = void $ p2 Refl
  ordSym (x1, x2) (y1, y2) with (decOrd (order y1 x1))
    | IsEQ p = rewrite ordSym x1 y1 in rewrite p in ordSym x2 y2
    | IsLT p = rewrite ordSym x1 y1 in rewrite p in Refl
    | IsGT p = rewrite ordSym x1 y1 in rewrite p in Refl
  ordTrans (l1, l2) (m1, m2) (r1, r2) p with (decOrd (order l1 m1))
    | IsLT p1 with (decOrd (order m1 r1))
      | IsLT p2 = rewrite sym (ordTrans l1 m1 r1 (trans p1 (sym p2))) in rewrite p1 in Refl
      | IsGT p2 = void $ pair_ordTrans_lemma2 {l1=l1} {l2=l2} {m1=m1} {m2=m2} {r1=r1} {r2=r2} p1 p2 p
      | IsEQ p2 with (reflOrd m1 r1 p2)
        ordTrans (l1, l2) (m1, m2) (m1, r2) p | IsLT p1 | IsEQ _ | Refl with (order l1 m1)
          ordTrans (_, _) (_, _) (_, _) _ | IsLT Refl | IsEQ _ | Refl | EQ impossible
          | LT = Refl
          | GT = Refl
    | IsGT p1 with (decOrd (order m1 r1))
      | IsGT p2 = rewrite sym (ordTrans l1 m1 r1 (trans p1 (sym p2))) in rewrite p1 in Refl
      | IsLT p2 = void $ pair_ordTrans_lemma1 {l1=l1} {l2=l2} {m1=m1} {m2=m2} {r1=r1} {r2=r2} p1 p2 p
      | IsEQ p2 with (reflOrd m1 r1 p2)
        ordTrans (l1, l2) (m1, m2) (m1, r2) p | IsGT p1 | IsEQ _ | Refl with (order l1 m1)
          ordTrans (_, _) (_, _) (_, _) _ | IsGT Refl | IsEQ _ | Refl | EQ impossible
          | LT = Refl
          | GT = Refl
    | IsEQ p1 with (decOrd (order m1 r1))
        | IsEQ p2 = rewrite p1 in rewrite sym (ordTrans l1 m1 r1 (trans p1 (sym p2))) in rewrite p1 in ordTrans l2 m2 r2 (pair_ordTrans_lemma3 l1 m1 r1 l2 m2 r2 p1 p2 p)
        | IsLT p2 = rewrite p1 in rewrite reflOrd l1 m1 p1 in rewrite p2 in pair_ordTrans_lemma4 l1 m1 r1 l2 m2 r2 p1 p2 p
        | IsGT p2 = rewrite p1 in rewrite reflOrd l1 m1 p1 in rewrite p2 in pair_ordTrans_lemma5 l1 m1 r1 l2 m2 r2 p1 p2 p

implementation VerifiedOrd a => VerifiedOrd (List a) where
  order []      []      = EQ
  order []      (_::_)  = LT
  order (_::_)  []      = GT
  order (x::xs) (y::ys) = orderPair (order x y) (order xs ys)
  ordRefl [] = Refl
  ordRefl (x::xs) = rewrite ordRefl x in ordRefl xs
  reflOrd [] [] _ = Refl
  reflOrd (x::xs) (y::ys) p with (decOrdEq (order x y))
    | Yes p2 with (reflOrd x y p2)
      reflOrd (x::xs) (x::ys) p | Yes p2 | Refl with (order x x)
        reflOrd (x::xs) (x::ys) p | Yes p2   | Refl | EQ = rewrite reflOrd xs ys p in Refl
        reflOrd (_::_)  (_::_)  _ | Yes Refl | Refl | LT impossible
        reflOrd (_::_)  (_::_)  _ | Yes Refl | Refl | GT impossible
    | No p2 with (order x y)
      | EQ = void $ p2 Refl
      | LT = void $ p2 p
      | GT = void $ p2 p
  reflOrd [] (_::_) Refl impossible
  reflOrd (_::_) [] Refl impossible
  ordSym [] [] = Refl
  ordSym [] (_::_) = Refl
  ordSym (_::_) [] = Refl
  ordSym (x::xs) (y::ys) with (decOrd (order x y))
    | IsLT p = rewrite ordSym y x in rewrite p in Refl
    | IsGT p = rewrite ordSym y x in rewrite p in Refl
    | IsEQ p = rewrite ordSym y x in rewrite p in ordSym xs ys
  ordTrans [] [] zs p = p
  ordTrans [] (y::ys) (z::zs) p = Refl
  ordTrans (x::xs) (y::ys) [] p = p
  ordTrans (x::xs) (y::ys) (z::zs) p with (decOrd (order x y))
    | IsLT p1 with (decOrd (order y z))
      | IsLT p2 = rewrite sym (ordTrans x y z (trans p1 (sym p2))) in rewrite p1 in Refl
      | IsGT p2 = void $ (the (typeOf p -> Void) (rewrite p1 in rewrite p2 in \Refl impossible)) p
      | IsEQ p2 = rewrite (sym (reflOrd y z p2)) in rewrite p1 in Refl
    | IsGT p1 with (decOrd (order y z))
      | IsGT p2 = rewrite sym (ordTrans x y z (trans p1 (sym p2))) in rewrite p1 in Refl
      | IsLT p2 = void $ (the (typeOf p -> Void) (rewrite p1 in rewrite p2 in \Refl impossible)) p
      | IsEQ p2 = rewrite (sym (reflOrd y z p2)) in rewrite p1 in Refl
    | IsEQ p1 with (decOrd (order y z))
      | IsEQ p2 = the (typeOf p -> order (x::xs) (y::ys) = order (x::xs) (z::zs)) (rewrite sym (reflOrd y z p2) in rewrite reflOrd x y p1 in rewrite ordRefl y in ordTrans xs ys zs) p
      | IsGT p2 = rewrite p1 in rewrite (reflOrd x y p1) in rewrite p2 in (the (typeOf p -> order xs ys = GT) (rewrite p1 in rewrite p2 in id)) p
      | IsLT p2 = rewrite p1 in rewrite (reflOrd x y p1) in rewrite p2 in (the (typeOf p -> order xs ys = LT) (rewrite p1 in rewrite p2 in id)) p
  ordTrans [] (_::_) [] Refl impossible
  ordTrans (_::_) [] [] Refl impossible
  ordTrans (_::_) [] (_::_) Refl impossible

implementation VerifiedOrd Nat where
  order = compare
  ordRefl Z = Refl
  ordRefl (S n) = ordRefl n
  reflOrd Z Z _ = Refl
  reflOrd Z (S _) Refl impossible
  reflOrd (S _) Z Refl impossible
  reflOrd (S n) (S m) p = cong (reflOrd n m p)
  ordSym Z Z = Refl
  ordSym Z (S _) = Refl
  ordSym (S _) Z = Refl
  ordSym (S m) (S n) = ordSym m n
  ordTrans Z Z Z _ = Refl
  ordTrans Z (S m) (S r) _ = Refl
  ordTrans (S l) (S m) Z p = p
  ordTrans (S l) (S m) (S r) p = ordTrans l m r p
  ordTrans Z Z (S r) Refl impossible
  ordTrans Z (S m) Z Refl impossible
  ordTrans (S l) Z Z Refl impossible
  ordTrans (S l) Z (S r) Refl impossible

implementation VerifiedOrd (Fin n) where
  order = compare
  ordRefl FZ = Refl
  ordRefl (FS n) = ordRefl n
  reflOrd FZ FZ _ = Refl
  reflOrd (FS n) (FS m) p = cong $ reflOrd n m p
  reflOrd FZ (FS _) Refl impossible
  reflOrd (FS _) FZ Refl impossible
  ordSym FZ FZ = Refl
  ordSym FZ (FS _) = Refl
  ordSym (FS _) FZ = Refl
  ordSym (FS m) (FS n) = ordSym m n
  ordTrans FZ FZ FZ _ = Refl
  ordTrans FZ (FS m) (FS r) _ = Refl
  ordTrans (FS l) (FS m) FZ p = p
  ordTrans (FS l) (FS m) (FS r) p = ordTrans l m r p
  ordTrans FZ FZ (FS r) Refl impossible
  ordTrans FZ (FS m) FZ Refl impossible
  ordTrans (FS l) FZ FZ Refl impossible
  ordTrans (FS l) FZ (FS r) Refl impossible


text:
module ArithCmd

import System
import Arith

%default total

data Command : Type -> Type where
     PutStr : String -> Command ()
     GetLine : Command String

data ConsoleIO : Type -> Type where
     Quit : a -> ConsoleIO a
     Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

data Fuel = Empty | More (Lazy Fuel)

(>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
(>>=) = Do

runCommand : Command a -> IO a
runCommand (PutStr x) = putStr x
runCommand GetLine = getLine

partial
forever : Fuel
forever = More forever

run : Fuel -> ConsoleIO a -> IO (Maybe a)
run Empty y = pure Nothing
run (More x) (Quit y) = pure $ Just y
run (More x) (Do z f) = do res <- runCommand z
                           run x $ f res
mutual
  correct : Stream Int -> (score : Nat) -> ConsoleIO Nat
  correct nums score
    = do PutStr "Correct!\n"
         quiz nums (score + 1)

  wrong : Stream Int -> Int -> (score : Nat) -> ConsoleIO Nat
  wrong nums ans score
    = do PutStr ("Wrong, the answer is " ++ show ans ++ "\n")
         quiz nums score

  quiz : Stream Int -> (score : Nat) -> ConsoleIO Nat
  quiz (n1 :: n2 :: nums) score =
    do PutStr $ "Score so far: " ++ show score ++ "\n"
       PutStr $ show n1 ++ " * " ++ show n2 ++ "? "
       answer <- GetLine
       if toLower answer == "quit" then Quit score else
           if (cast answer == n1 * n2)
             then correct nums score
             else wrong nums (n1 * n2) score

partial
main : IO ()
main = do seed <- time
          Just score <- run forever (quiz (arithInputs (fromInteger seed)) 0)
               | Nothing => putStrLn "Ran out of fuel."
          putStrLn ("Final score: " ++ show score)

max_stars_repo_path: Chapter 11/ArithCmd.idr

max_issues_repo_path: Chapter 11/ArithCmd.idr

max_forks_repo_path: Chapter 11/ArithCmd.idr


text:
module Toolkit.System

import System

%default total

export
tryOrDie : Show err
        => Either err type
        -> IO type
tryOrDie (Left err) =
  do putStrLn "Error Happened"
     printLn err
     exitFailure
tryOrDie (Right res) = pure res

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Parsers
{-
Parsing is the conversion of input, say a list of characters or a string,
to structured data, if the input is of the appropriate form. We implement here
the idea of _combinator parsing_, where we build parsers from basic ones by
combining and transforming parsers.

This allows us to parse relatively complex languages with a small amount of code.
Better still, even the code to enable this is small (at least provided we do not
address issues of efficiency and error messages).
-}

%access public export

{- The result of parsing, either consuming some input and generating a result
with type `a` as well as the rest of the input, or reporting that parsing failed.
-}
data ParseResult : Type -> Type where
  Success : {a: Type} -> (result : a) -> (rest: List Char) -> ParseResult a
  Failed : {a: Type} ->  ParseResult a

-- A parser, which takes input and gives a result (plus unconsumed input)
Parser: Type -> Type
Parser a = (List Char) -> ParseResult a

-- A helper method
parseChars : {a: Type} -> Parser a -> List Char -> ParseResult a
parseChars  p xs = p xs

-- A helper that allows giving a string as method to parse: the most user-friendly method
parse : {a: Type} -> Parser a -> String -> ParseResult a
parse p s = parseChars p (unpack s)

-- A parser that checks if a character satisfies a predicate and returns it.
charPred : (Char -> Bool) -> Parser Char
charPred p l = (case l of
                     [] => Failed
                     (x :: xs) =>
                       if (p x) then (Success x xs) else Failed)

-- A parser matching a specific character
charLit : Char -> Parser Char
charLit c = charPred (\x => x == c)

{- Given a parser `p` for type `a` and a function `f: a -> b` gives a parser for type `b`;
this succeeds if `p` succeeds, and the result for type `b` is obtained by applying `f`
to the result of `p`
-}
map : {a: Type} -> {b: Type} -> Parser a -> (a -> b) -> Parser b
map p f cs = (case (p cs) of
                           (Success  result rest) => Success  (f result) rest
                           Failed => Failed)

{- Given parsers `p` for type `a` and `q` for type `b`, returns a parser which
parses the input on `a`, and if this succeeds parses the rest with `q`. A success
is where both parses succeed, and the result is the pair of results.
-}
(++) : {a : Type} -> {b: Type} -> Parser a -> Parser b -> Parser (Pair a b)
(++) p q l = (case p l of
                       (Success result1 rest1) =>
                          (case (q rest1) of
                              (Success result2 rest2) => Success ((result1, result2)) rest2
                              Failed => Failed)
                       Failed => Failed)

{- A parser that matches a list of characters, e.g. [`l`, `e`, `t`]. This means
the input should begin with this. This could have been reursively implemented
with `charLit` and `(++)` instead.
-}
charsLit: (List Char) -> Parser (List Char)
charsLit []  l = Success [] l
charsLit (x :: xs) [] = Failed
charsLit (x :: xs) (a :: bs) =
                  (case charLit x (a :: bs) of
                        (Success result1 rest) => (case (charsLit xs bs) of
                                (Success result2 rest) => Success (result1 :: result2) rest
                                Failed => Failed)
                        Failed => Failed)

-- A parser matching a string, e.g. "let"
S: String -> Parser String
S s = map (charsLit (unpack s)) pack

{- Given two parsers `p` and `q` for type `a`, tries to parse with `p` and, if this fails,
tries to parse with `q`.
-}
(||) : {a: Type} -> Parser a -> Parser a -> Parser a
(||) p q l = (case (p l) of
                       (Success result rest) => Success result rest
                       Failed => q l)

-- recursive helper for `rep` method.
repParse: {a: Type} -> Parser a -> (inp: List Char) -> (accum: List a) -> ParseResult (List a)
repParse p inp accum = case (p inp) of
                            (Success result rest) => repParse p rest (result :: accum)
                            Failed => Success accum inp

-- helper for `rep` method
repRev : {a: Type} -> Parser a -> Parser (List a)
repRev p l =  repParse p l []

{- Given a parser `p`, returns a new parser that matches 0 or more
matches for `p` and returns a list of successful matches
-}
rep : {a: Type} -> Parser a -> Parser (List a)
rep p = map (repRev p) reverse

{- Given a parser `p`, returns a new parser that matches 1 or more
matches for `p` and returns a list of successful matches
-}
rep1 : {a: Type} -> Parser a -> Parser (List a)
rep1 p = map (p ++ (repRev p)) (\pair => (case pair of
                                            (a, b) => a:: reverse(b)))

-- Helper: given the  digits of a natural number from the list of digits from right to left
natFromRev : List Char -> Nat -> Nat
natFromRev [] n = 0
natFromRev (x :: xs) n =
  let
  d : Nat = n * cast( (ord x) - (ord '0'))
  in
  d + (natFromRev xs (10 * n))

-- Given the digits of a natural number, returns the number.
natFromChars : (List Char) -> Nat
natFromChars l = natFromRev (reverse l) 1

-- Parser to return a (literal) natural number, e.g. "231" -> 231
nat : Parser Nat
nat = map (rep1 (charPred isDigit)) (natFromChars)

-- Parser checking if al input is consumed.
eof : Parser Unit
eof [] = Success () []
eof (x :: xs) = Failed

-- Given a parser `p` for type `a` and a predicate
filter : {a: Type} -> Parser a -> (a -> Bool) -> Parser a
filter p pred l = case p l of
                       (Success result rest) =>
                         if pred result then Success result rest else Failed
                       Failed => Failed

infix 10 +>

-- Like (++) but drops the second matched term
(+>) : {a : Type} -> {b: Type} -> Parser a -> Parser b -> Parser a
(+>) p q l = (case p l of
                       (Success result1 rest1) => (case (q rest1) of
                                      (Success result2 rest2) => Success result1 rest2
                                      Failed => Failed)
                       Failed => Failed)

infix 11 <+

-- Like (++) but drops the first matched term
(<+) : {a : Type} -> {b: Type} -> Parser a -> Parser b -> Parser b
(<+) p q l = (case p l of
                      (Success result1 rest1) => (case (q rest1) of
                                      (Success result2 rest2) => Success result2 rest2
                                      Failed => Failed)
                      Failed => Failed)

{- Given a parser `p` for type `a` and a character `c`, matches for 1 or more
matches for `p` separated by `c`
-}
repSep: {a: Type} -> Parser a -> Char -> Parser (List a)
repSep p c =
  map((p +> (charLit c)) ++ (repSep p c))(
    \pair => (case pair of
          (x, ys) => x :: ys)) || map(p)(\n => n ::[])

{- Given a parser `p`, returns a parser that allows spaces before and after the match
-}
pad : {a: Type} -> Parser a -> Parser a
pad p =  rep(S " ") <+ p +> rep(S " ")

-- Parses a string with spaces allowed before and after
SS : String -> Parser String
SS s = pad (S s)

{- Given a parser `p` for type `a` and a character `c`, matches for 1 or more
matches for `p` separated by `c`, allowing spaces before and after `c`
-}
repSepTrim: {a: Type} -> Parser a -> Char -> Parser (List a)
repSepTrim p c =
  map((p +>  (pad(charLit c))) ++ (repSepTrim p c))(
    \pair => (case pair of
                    (x, ys) => x :: ys)) || map(p)(\n => n ::[])

{- The mutual block is a typical example of parsing: parsers for arithmetic
expressions involving + and * and parenthesis with the usual precedence,
calculating the resulting natural number
-}
mutual
  -- A simple term: a literal natural number or an expression in parenthesis
  simpleTerm : Parser Nat
  simpleTerm = nat || ( (SS "(") <+ expression +> (SS ")") )

  -- A product of simple terms, possibly with just one simple term
  term : Parser Nat
  term = map(repSepTrim simpleTerm '*')(foldl(*)(1))

  -- A sum of terms, possibly with just one term
  expression: Parser Nat
  expression = map(repSepTrim term '+')(foldl(+)(0))

{- Combining parsers to allow dependence on context. Concretely, given
  * A parser `p` for type `a`
  * A function `parsers` from `a` to parsers of type `b`
  We get a parser for type `b`. Namely, the parser `p` is applied to the input.
  If this succeeds with result `x: a`, the parser `q = parsers x` is applied to the
  rest of the input.
-}
flatMapWithNext : {a : Type} -> {b: Type} -> Parser a -> (a -> Parser b) -> Parser b
flatMapWithNext p parsers input =
  case p input of
          (Success result1 rest1) => (case (parsers result1) rest1 of
                    (Success result2 rest) => Success result2 rest
                    Failed => Failed)
          Failed => Failed

{- Given a parser `p` for type `a` and a function `f: a -> Maybe b` gives a parser for type `b`;
if `p` succeeds with result `x` and `f x = Just y`, then the parse is successful with result y;
all other cases fail
-}
mapMaybe : {a : Type} -> {b: Type} -> Parser a -> (a -> Maybe b) -> Parser b
mapMaybe p f s = case p s of
                      (Success result rest) =>
                        (case f result of
                              Nothing => Failed
                              (Just b) => Success b rest)
                      Failed => Failed

-- matches a letter
letter: Parser Char
letter = charPred (\x => 'a' <= x && x <= 'z')


text:
module Pipes.Core

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

||| Main data type for Pipes:
||| * `a` is the type flowing in from the upstream
||| * `b` is the type flowing out to downstream
||| * `m` is the Monad the pipe runs in
||| * `r2` is the returned value of the pipe
||| * `r1` is the returned value of the previous pipe

export
data PipeM : (a, b, r1 : Type) -> (m : Type -> Type) -> (r2 : Type) -> Type where
  Pure    : r2 -> PipeM a b r1 m r2                                       -- Lift a value into the pipe
  Action  : m (Inf (PipeM a b r1 m r2)) -> PipeM a b r1 m r2              -- Interleave an effect
  Yield   : Inf (PipeM a b r1 m r2) -> m () -> b -> PipeM a b r1 m r2     -- Yield a value and next status
  Await   : (Either r1 a -> Inf (PipeM a b r1 m r2)) -> PipeM a b r1 m r2 -- Yield a continuation (expecting a value)

||| `yield` sends a value downstream

export
yield : (Monad m) => b -> PipeM a b r' m ()
yield = Yield (Pure ()) (pure ())

||| `finalizeOr` sends a value downstream, or
||| run the finalizer if the downstream pipe is termination

export
yieldOr : (Monad m) => b -> m () -> PipeM a b r' m ()
yieldOr value finalize = Yield (Pure ()) finalize value

||| `await` waits from an upstream value

export
await : PipeM a b r' m (Maybe a)
await = Await $ \v =>
  case v of Right x => Pure (Just x)
            _ => Pure (the (Maybe a) Nothing)

||| `awaitOr` waits from an upstream value, or result of upstream pipe

export
awaitOr : PipeM a b r1 m (Either r1 a)
awaitOr = Await $ \v => Pure v

||| A `Source` cannot `await` any input

public export
Source : (m: Type -> Type) -> (b: Type) -> Type
Source m b = PipeM Void b Void m ()

||| A `Source` that can return a result of type `r`

public export
SourceM : (b: Type) -> (m: Type -> Type) -> (r: Type) -> Type
SourceM b m r = PipeM Void b Void m r

||| A `Pipe` can `await` and `yield`

public export
Pipe : {r: Type} -> (a: Type) -> (m: Type -> Type) -> (b: Type) -> Type
Pipe {r} a m b = PipeM a b r m r

||| A `Sink` cannot `yield` anything

public export
Sink : {r1: Type} -> (a: Type) -> (m: Type -> Type) -> (r: Type) -> Type
Sink {r1} a m r = PipeM a Void r1 m r

||| A `Sink` with access to the previous pipe return value

public export
SinkM : (a: Type) -> (m: Type -> Type) -> (r1, r2: Type) -> Type
SinkM a m r1 r2 = PipeM a Void r1 m r2

||| An `Effect` cannot `await` or `yield` (pure effect)

public export
Effect : (m: Type -> Type) -> (r: Type) -> Type
Effect m r = PipeM Void Void Void m r

||| Functor implementation: (Recursively replace `r` with `f r`)

export
implementation (Monad m) => Functor (PipeM a b r1 m) where
  map f = assert_total recur where
    recur (Pure r) = Pure (f r)
    recur (Action a) = Action (a >>= \x => pure (recur x))
    recur (Yield next finish b) = Yield (recur next) finish b
    recur (Await cont) = Await (\x => recur (cont x))

||| Applicative implementation (Recursively replace `r` with `map r pa`)

export
implementation (Monad m) => Applicative (PipeM a b r1 m) where
  pure = Pure
  pf <*> pa = assert_total (recur pf) where
    recur (Pure f) = map f pa
    recur (Action a) = Action (a >>= \x => pure (recur x))
    recur (Yield next finish b) = Yield (recur next) finish b
    recur (Await cont) = Await (\x => recur (cont x))

||| Monad implementation (Recursively replace `r` with `f r`)

export
implementation (Monad m) => Monad (PipeM a b r1 m) where
  m >>= f = assert_total (recur m) where
    recur (Pure r) = f r
    recur (Action a) = Action (a >>= \x => pure (recur x))
    recur (Yield next finish b) = Yield (recur next) finish b
    recur (Await cont) = Await (\x => recur (cont x))

||| Monad Transformer implementation
||| * Wrap the monadic action in a `Action` constructor
||| * Wrap the monadic return in a `Pure` constructor

export
implementation MonadTrans (PipeM a b r1) where
  lift m = assert_total $ Action (m >>= \x => pure (Pure x))

infixr 9 .|

||| Assembling pipes: Pull based behavior
||| * Run the actions of the right pipe until it reaches `await`
||| * The run the actions of the left pipe until it reached `yield`

export
(.|) : (Monad m) => PipeM a b r1 m r2 -> PipeM b c r2 m r3 -> PipeM a c r1 m r3
(.|) = pull (pure ()) where
  mutual

    pull : (Monad m) => m () -> PipeM a b r1 m r2 -> PipeM b c r2 m r3 -> PipeM a c r1 m r3
    pull final up (Yield next finish c) =
      let final' = do finish; final
      in Yield (pull final up next) final' c      -- Yielding downstream
    pull final up (Action a) =
      lift a >>= \next => pull final up next      -- Produce effect downstream
    pull final up (Await cont) =
      up `push` \x => cont x                      -- Ask upstream for a value
    pull final up (Pure r) =
      do lift final; Pure r

    push : (Monad m) => PipeM a b r1 m r2 -> (Either r2 b -> PipeM b c r2 m r3) -> PipeM a c r1 m r3
    push (Await cont) down =
      Await (\a => cont a `push` down)            -- Awaiting upstream
    push (Action a) down =
      lift a >>= \next => next `push` down        -- Produce effect upstream
    push (Yield next finish b) down =
      pull finish next (down (Right b))           -- Give control downstream
    push (Pure r) down =
      pull (pure ()) (Pure r) (down (Left r))     -- Termination, send Nothing to next

||| Run an Effect and collect the output
||| * Execute the sequence of effects of the pipe
||| * Return the final value when no effects are remaining

export
runPipe : (Monad m) => Effect m r -> m r
runPipe (Pure r) = pure r                         -- Done executing the pipe, return the result
runPipe (Action a) = a >>= \p => runPipe p        -- Execute the action, run the next of the pipe
runPipe (Yield next finish b) = absurd b
runPipe (Await cont) = runPipe $ Await (either absurd absurd)

||| Run an Effect and discard the output

export
runEffect : (Monad m) => Effect m r -> m ()
runEffect p = runPipe p *> pure ()

||| Run an pure Effect in the Identity Monad

export
runPure : Effect Identity r -> r
runPure = runIdentity . runPipe

||| `foldM` consumes a stream
||| It creates a Sink to fold a set of values into a single output value

export
foldM : (Monad m) => (a -> b -> m b) -> b -> Sink a m b
foldM f = recur where
  recur acc = do
    ma <- await
    case ma of
      Just x => lift (f x acc) >>= recur
      Nothing => pure acc

export
fold : (Monad m) => (a -> b -> b) -> b -> Sink a m b
fold f = foldM (\a, b => pure (f a b))

||| `idP` is the identity Pipe

export
idP : (Monad m) => Pipe a m a
idP = awaitOr >>= either Pure (Yield idP (pure ()))

||| The function `each` lifts a foldable to a Source
||| * The actual type is in fact more general
||| * It allows you to use it to build pipes

export
each : (Monad m, Foldable f) => f a -> PipeM a' a r m ()
each xs = foldr (\x, p => yield x *> p) (pure ()) xs

||| Use `awaitOne` to automatically take care of forwarding the return value
||| of the previous pipe to the next pipe

export
awaitOne : (Monad m) => (i -> PipeM i o r m r) -> PipeM i o r m r
awaitOne f = awaitOr >>= either Pure f

||| Use `awaitForever` to build stateless pipes

export
awaitForever : (Monad m) => (i -> PipeM i o r m r') -> PipeM i o r m r
awaitForever f = recur where
  recur = awaitOr >>= either Pure (\x => do f x; recur)

--

max_stars_repo_name: QuentinDuval/IdrisPipes

max_issues_repo_name: QuentinDuval/IdrisPipes

max_forks_repo_name: QuentinDuval/IdrisPipes


text:
module Crypto.Curve.Weierstrass

import Crypto.Curve
import Data.Bits
import Data.List
import Data.Vect
import Utils.Bytes
import Utils.Misc

-- Weiserstrass curve y^2 = x^3 + ax + b in Jacobian coordinate
public export
interface WeierstrassPoint p where
  a_coefficent : Integer
  b_coefficent : Integer
  prime : Integer -- If this isn't prime the skinwalker will devour you
  to_jacobian : p -> (Integer, Integer, Integer)
  from_jacobian : (Integer, Integer, Integer) -> p
  g : p
  to_from_jacobian : (x : (Integer, Integer, Integer)) -> to_jacobian (from_jacobian x) = x
  bits' : Nat
  curve_n : Integer

j_point_double : WeierstrassPoint p => (Integer, Integer, Integer) -> (Integer, Integer, Integer)
j_point_double (x, y, z) =
  let modulus = prime {p=p}
      s  = (4 * x * y * y) `mod'` modulus
      z4 = pow_mod z 4 modulus
      y4 = pow_mod y 4 modulus
      m  = (3 * x * x + a_coefficent {p} * z4) `mod'` modulus
      x' = (m * m - 2 * s) `mod'` modulus
      y' = (m * (s - x') - 8 * y4) `mod'` modulus
      z' = (2 * y * z) `mod'` modulus
  in (x', y', z')

j_point_add : WeierstrassPoint p => (Integer, Integer, Integer) -> (Integer, Integer, Integer) -> (Integer, Integer, Integer)
j_point_add (x, y, 0) b = b
j_point_add a (x, y, 0) = a
j_point_add a@(xp, yp, zp) b@(xq, yq, zq) =
  let m = prime {p=p}
      zq2 = pow_mod zq 2 m
      zq3 = pow_mod zq 3 m
      zp2 = pow_mod zp 2 m
      zp3 = pow_mod zp 3 m
      u1 = mul_mod xp zq2 m
      u2 = mul_mod xq zp2 m
      s1 = mul_mod yp zq3 m
      s2 = mul_mod yq zp3 m
      h = u2 - u1
      r = s2 - s1
      h2 = pow_mod h 2 m
      h3 = mul_mod h h2 m
      u1h2 = mul_mod u1 h2 m
      nx = ((r * r) - h3 - 2 * u1h2) `mod'` m
      ny = (r * (u1h2 - nx) - s1 * h3) `mod'` m
      nz = (h * zp * zq) `mod'` m
      in if h == 0 then (if r == 0 then j_point_double {p=p} a else (0, 1, 0)) else (nx, ny, nz)

point_double : (Point p, WeierstrassPoint p) => p -> p
point_double b = from_jacobian {p=p} (j_point_double {p=p} (to_jacobian b))

mul' : (Point p, WeierstrassPoint p) => p -> p -> Nat -> Integer -> p
mul' r0 r1 m d =
  let (r0', r1') = if testBit d m then (point_add r0 r1, point_double r1) else (point_double r0, point_add r0 r1)
  in case m of
       S m' => mul' r0' r1' m' d
       Z => r0'

public export
WeierstrassPoint p => Point p where
  infinity = from_jacobian (0, 1, 0)
  generator = g
  bits = bits' {p=p}
  to_affine point =
    let (x, y, z) = to_jacobian point
        m = prime {p=p}
        z' = inv_mul_mod z m
        z2 = z' * z'
        z3 = z2 * z'
    in (mul_mod x z2 m, mul_mod y z3 m)
  modulus = prime {p=p}
  order = curve_n {p=p}
  point_add a b = from_jacobian {p=p} (j_point_add {p=p} (to_jacobian a) (to_jacobian b))
  mul s pt = mul' infinity pt (bits {p=p}) s

  encode point =
    let bytes = (7 + bits {p=p}) `div` 8
        (x', y') = to_affine point
        x = toList $ integer_to_be bytes x'
        y = toList $ integer_to_be bytes y'
    in 4 :: (x <+> y)

  decode (4 :: body) = do
    let bytes = (7 + bits {p=p}) `div` 8
    let (x', y') = splitAt bytes body
    x <- map be_to_integer $ exactLength bytes $ fromList x'
    y <- map be_to_integer $ exactLength bytes $ fromList y'

    -- infinity check
    guard $ not $ (x == 0) && (y == 0)

    -- check on curve
    let pri = modulus {p=p}
    let lhs = pow_mod y 2 pri
    let a   = a_coefficent {p=p}
    let b   = b_coefficent {p=p}
    let rhs = ((pow_mod x 3 pri) + (mul_mod x a pri) + b) `mod'` pri
    guard $ lhs == rhs

    pure $ from_jacobian (x, y, 1)
  decode _ = Nothing

public export
data P256 : Type where
  MkP256 : (Integer, Integer, Integer) -> P256

public export
WeierstrassPoint P256 where
  prime =
    0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff
  a_coefficent =
    0xffffffff00000001000000000000000000000000fffffffffffffffffffffffc
  b_coefficent =
    0x5ac635d8aa3a93e7b3ebbd55769886bc651d06b0cc53b0f63bce3c3e27d2604b
  from_jacobian = MkP256
  to_jacobian (MkP256 p) = p
  g = MkP256
    ( 0x6b17d1f2e12c4247f8bce6e563a440f277037d812deb33a0f4a13945d898c296
    , 0x4fe342e2fe1a7f9b8ee7eb4a7c0f9e162bce33576b315ececbb6406837bf51f5
    , 1 )
  to_from_jacobian x = Refl
  bits' = 256
  curve_n =
    0xffffffff00000000ffffffffffffffffbce6faada7179e84f3b9cac2fc632551

public export
data P384 : Type where
  MkP384 : (Integer, Integer, Integer) -> P384

public export
WeierstrassPoint P384 where
  prime =
    0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff
  a_coefficent =
    0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffc
  b_coefficent =
    0xb3312fa7e23ee7e4988e056be3f82d19181d9c6efe8141120314088f5013875ac656398d8a2ed19d2a85c8edd3ec2aef
  from_jacobian = MkP384
  to_jacobian (MkP384 p) = p
  g = MkP384
    ( 0xaa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7
    , 0x3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f
    , 1 )
  to_from_jacobian x = Refl
  bits' = 384
  curve_n =
    0xffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973

public export
data P521 : Type where
  MkP521 : (Integer, Integer, Integer) -> P521

public export
WeierstrassPoint P521 where
  prime =
    0x01ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
  a_coefficent =
    0x01fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc
  b_coefficent =
    0x0051953eb9618e1c9a1f929a21a0b68540eea2da725b99b315f3b8b489918ef109e156193951ec7e937b1652c0bd3bb1bf073573df883d2c34f1ef451fd46b503f00
  from_jacobian = MkP521
  to_jacobian (MkP521 p) = p
  g = MkP521
    ( 0x00c6858e06b70404e9cd9e3ecb662395b4429c648139053fb521f828af606b4d3dbaa14b5e77efe75928fe1dc127a2ffa8de3348b3c1856a429bf97e7e31c2e5bd66
    , 0x011839296a789a3bc0045c8a5fb42c7d1bd998f54449579b446817afbd17273e662c97ee72995ef42640c550b9013fad0761353c7086a272c24088be94769fd16650
    , 1 )
  to_from_jacobian x = Refl
  bits' = 521
  curve_n =
    0x01fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409


text:
In : (x : a) -> (l : List a) -> Type
In x [] = Void
In x (x' :: xs) = (x' = x) `Either` In x xs

appendEmpty : (xs : List a) -> xs ++ [] = xs
appendEmpty [] = Refl
appendEmpty (x :: xs) = rewrite appendEmpty xs in Refl

in_app_iff : {l : List b} -> {l' : List b} -> In a (l++l') -> (In a l `Either` In a l')
in_app_iff {l = []} {  l' = []} x = Left x
in_app_iff {l = []} {  l' = (y :: xs)} x = Right x
in_app_iff {l = (y::xs)} {  l' = []} x = rewrite sym (appendEmpty xs) in Left x
in_app_iff {l = (y::xs)} {l' = (z::ys)} (Left prf) = Left (Left prf)
in_app_iff {l = (y::xs)} {l' = (z::ys)} (Right prf) =
                                          let induc : Either (In a xs) (Either (z = a) (In a ys))= in_app_iff {l = xs} {l' = z :: ys} prf  in
                                          case induc of
                                                (Left l) => Left $ Right l
                                                (Right r) => Right r


text:
module Js.React.DOM

import Js
import Js.Object
import Js.DOM.Element
import Js.React.Element

%default total

export
%inline
render : (mount : Js.DOM.Element.Element) -> (element : Js.React.Element.Element) -> JS_IO ()
render mount = js "ReactDOM.render(%1, %0)" (Ptr -> Ptr -> JS_IO ()) (ptr mount) . ptr

max_stars_repo_name: jheiling/idris-react

max_issues_repo_name: jheiling/idris-react

max_forks_repo_name: jheiling/idris-react


text:
module Main

%default total

data U : Type where
  BOOL : U
  NAT : U
  PAIR : U -> U -> U

interpU : U -> Type
interpU BOOL = Bool
interpU NAT = Nat
interpU (PAIR x y) = (interpU x, interpU y)

showU : (u : U) -> interpU u -> String
showU BOOL True            = "Yes"
showU BOOL False           = "No"
showU NAT Z                = "Z"
showU NAT (S x)            = "S of " ++ showU NAT x
showU (PAIR tx ty) (x , y) = "(" ++ showU tx x ++ "," ++ showU ty y ++ ")"

main : IO ()
main = putStrLn $ showU NAT 0

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
-- Small (and obsolete) prototype of a cost-based computational
-- eDLS. Each operation has a cost. Functions take a lifted type,
-- FndType, that includes a fund. The output type of each lifted
-- operation contains the remaining fund after the operation.  It is
-- planned to be replaced by function realization described in
-- https://blog.singularitynet.io/ai-dsl-toward-a-general-purpose-description-language-for-ai-agents-21459f691b9e
-- but is kept here for future references.

module FndType

-- Funded type
public export
data FndType : Nat -> Type -> Type where
  FT : {fund : Nat} -> (datum : a) -> (FndType fund a)

-- Overload show for FndType
export
show : (FndType fund Int) -> String
show (FT datum) = "FT " ++ (show fund) ++ " " ++ (show datum)

-- Fund accessor
export
getFund : (FndType fund a) -> Nat
getFund (FT datum) = fund

-- Datum accessor
export
getDatum : (FndType fund a) -> a
getDatum (FT datum) = datum

-- Uplift function as to use FndType, with cost of 1.
export
upliftFun : {fund : Nat} -> {cost : Nat} -> (a -> b) -> (FndType (cost + fund) a) -> (FndType fund b)
upliftFun f = (\x => (FT (f (getDatum x))))

-- Downlift function as to run over datum rather than FndType.
export
downliftFun : {infund : Nat} -> ((FndType infund a) -> (FndType outfund b)) -> a -> b
downliftFun f = (\x => (getDatum (f (FT x))))

-- Lifted composition. Takes 2 filted functions and compose them
export
compose : ((FndType fund_b b) -> (FndType fund_c c))
        -> ((FndType fund_a a) -> (FndType fund_b b))
        -> (FndType fund_a a) -> (FndType fund_c c)
compose f g = (\x => (f (g x)))

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Toolkit.Data.List.View.PairWise

import Data.List

%default total

public export
data PairWise : List a -> Type where
  Empty : PairWise Nil
  One   : (x:a) -> PairWise [x]
  Two   : (x,y : a) -> PairWise [x,y]
  N     : (x,y : a)
       -> PairWise (y::xs)
       -> PairWise (x::y::xs)

export
pairwise : (xs : List a) -> PairWise xs
pairwise [] = Empty
pairwise (x :: []) = One x
pairwise (x :: (y :: xs)) with (pairwise (y::xs))
  pairwise (x :: (y :: [])) | (One y) = Two x y
  pairwise (x :: (y :: [w])) | (Two y w) = N x y (Two y w)
  pairwise (x :: (y :: (w :: xs))) | (N y w v) = N x y (N y w v)

unSafeToList : {xs : List a} -> PairWise xs -> Maybe (List (a,a))
unSafeToList Empty = Just Nil
unSafeToList (One x) = Nothing
unSafeToList (Two x y) = Just [(x,y)]
unSafeToList (N x y z)
  = do rest <- unSafeToList z
       pure (MkPair x y :: rest)

||| Returns a list of pairs if `xs` has even number of elements, Nothing if odd.
export
unSafePairUp : (xs : List a) -> Maybe (List (a,a))
unSafePairUp xs = (unSafeToList (pairwise xs))

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Test.Spec

import Specdris.Spec
import Control.Permutation
import Data.Vect

export
specSuite : IO ()
specSuite =
  spec $ do
    describe "circulate" $ do
      it "should work (1/2)" $ do
        show circ `shouldBe` "(01234)"
      it "should work (2/2)" $ do
        sigma circulate [0, 1, 2, 3, 4] `shouldBe` [1, 2, 3, 4, 0]
    describe "isEven" $ do
      it "should work" $ do
        map isEven ps `shouldBe` [False, True]
      it "should work with exp" $ do
        map (isEven . exp 2) ps `shouldBe` [True, True]
    describe "trivial" $ do
      it "should permute a vector" $
        toVector trivial `shouldBe` [0, 3, 2, 1]
      it "work on reversed" $
        toVector reverse `shouldBe` [3, 2, 1, 0]
    describe "cycle precursor" $ do
      it "should give a fixNat function" $
        fixNat trivial 1 `shouldBe` 3
      it "should give a orbit function" $
        finOrbit trivial 1 `shouldBe` [1, 3]
    describe "show" $ do
      it "should pretty-print for n < 10" $ do
        show trivial `shouldBe` "(13)"
    describe "compose" $ do
      it "should compose nicely (1/2)" $ do
        toVector (trivial <+> disjoint) `shouldBe` [2, 3, 0, 1]
      it "should compose nicely (2/2)" $ do
        show (trivial <+> swap) `shouldBe` "(02)(13)"
    describe "invert" $ do
      it "should invert a permutation" $
        inverse trivial `shouldBe` trivial
      it "should satisfy x⁻¹x=e" $
        inverse trivial <+> trivial `shouldBe` neutral
    describe "issue #2" $ do
      it "should hold" $
        neutral <+> circSmall `shouldBe` circSmall

        -- TODO property test: composing disjoint swaps should commute!
        -- Also associativity. or better yet proofs?
  where trivial : Permutation 4
        trivial = pi (FS 0) (FS 2)
        disjoint : Permutation 4
        disjoint = pi (FZ) (FS 1)
        big : Permutation 11
        big = pi (FS 0) (FS 9)
        swap : Permutation 4
        swap = pi FZ (FS 1)
        ps : Vect 2 (Permutation 2)
        ps = enumerateStrict
        circSmall : Permutation 3
        circSmall = circulate
        x : Permutation 3
        x = pi FZ (FS 1)
        circ : Permutation 5
        circ = circulate

max_stars_repo_name: vmchale/permutations

max_issues_repo_name: marcosh/permutations

max_forks_repo_name: marcosh/permutations


text:
-- test that defs from Strings are available.
import Data.Strings

-- same signature as a function pulled in from above import
sameSig : Char -> String
sameSig = singleton

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
data Tree a = Empty
            | Node (Tree a) a (Tree a)

Eq a => Eq (Tree a) where
    (==) Empty Empty = True
    (==) (Node l e r) (Node l' e' r')
      = l == l' && e == e' && r == r'
    (==) _ _ = False

Foldable Tree where
  foldr func acc Empty = acc
  foldr func acc (Node l e r) =
    let left = foldr func acc l
        right = foldr func left r in
        func e right


text:
module Language.LSP.Message.Cancel

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#cancelRequest
public export
record CancelParams where
  constructor MkCancelParams
  id : OneOf [Int, String]
%runElab deriveJSON defaultOpts `{{CancelParams}}


text:
import System

import System.Concurrency.Pipe

{-- TODO: REWRITE EVERYTHING
data MsgType = Syn
             | Ack
             | Syn_Ack

senderError : (senderID : Int) -> (errMsg : String) -> IO ()
senderError senderID errMsg
  = putStrLn $ "S" ++ (show senderID) ++ ": ERROR: " ++ errMsg

receiverError : (receiverID : Int) -> (errMsg : String) -> IO ()
receiverError receiverID errMsg
  = putStrLn $ "R" ++ (show receiverID) ++ ": ERROR: " ++ errMsg

s1 : (chan : Channel) -> IO ()
s1 chan =
  do putStrLn "S1: Hello"
     sendAndSignal chan (prepare Syn)
     putStrLn "S1: Sent 'Syn'"
     rawResp <- await chan
     putStrLn "S1: Got a response"
     let s1Err = senderError 1
     case rawResp of
          Nothing => s1Err "No reply."

          (Just rawResp) => case unsafeOpen rawResp MsgType of
                                 Syn => s1Err "Received 'Syn' as reply."

                                 Ack => do putStrLn "S1: Received 'Ack'"
                                           sendAndSignal chan (prepare Syn_Ack)
                                           putStrLn "S1: Sent 'Syn_Ack'"
                                           putStrLn "S1: -- Done --"

                                 Syn_Ack => s1Err "Received 'Syn_Ack' as reply."

r1 : (chan : Channel) -> IO ()
r1 chan =
  do putStrLn "R1: Hello"
     let r1Err = receiverError 1
     rawMsg <- await chan
     putStrLn "R1: Got an initial message"
     case rawMsg of
          Nothing => r1Err "No initial message."

          (Just msg) =>
            case unsafeOpen msg MsgType of
                 Syn => do putStrLn "R1: Got 'Syn'"
                           sendAndSignal chan (prepare Ack)
                           putStrLn "R1: Sent 'Ack'"
                           rawMsg' <- await chan
                           putStrLn "R1: Got a second message"
                           case rawMsg' of
                                Nothing => r1Err "No second message."

                                (Just msg') =>
                                  case unsafeOpen msg' MsgType of
                                       Syn => r1Err "Got 'Syn' second"

                                       Ack => r1Err "Got 'Ack' second"

                                       Syn_Ack =>
                                         do putStrLn "R1: Got 'Syn_Ack'"
                                            putStrLn "R1: -- Done --"

                 Ack => r1Err "Got 'Ack' first"

                 Syn_Ack => r1Err "Got 'Syn_Ack' first"

testHandshake1 : IO ()
testHandshake1 = do putStrLn "----- Begin Test 1 -----"
                    cRef <- makeChannel
                    sendChan <- makeSender cRef
                    receiveChan <- makeReceiver cRef
                    senderPID <- fork (s1 sendChan)
                    receiverPID <- fork (r1 receiveChan)
                    sleep 3
                    putStrLn "-----  End Test 1  -----"
                    putStrLn ""

testHandshake2 : IO ()
testHandshake2 = do putStrLn "----- Begin Test 2 -----"
                    cRef <- makeChannel
                    sendChan <- makeSender cRef
                    receiveChan <- makeReceiver cRef
                    senderPID <- fork (s1 sendChan)
                    receiverPID <- fork (r1 receiveChan)
                    sleep 3
                    putStrLn "-----  End Test 2  -----"
                    putStrLn ""

main : IO ()
main = do testHandshake1
          testHandshake2
--}


text:
module Graphics.Rendering.Gl.Buffers

%include C "gl_idris.h"
%link C "gl_idris.o"

%access public export

free : Ptr -> IO ()
free ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr

-- ----------------------------------------------------------------- [ Double Buffers ]
private
setDouble : Ptr -> (idx: Nat) -> Double -> IO ()
setDouble ptr idx d = foreign FFI_C "idr_buffers_set_double" (Ptr -> Int -> Double -> IO ()) ptr (cast idx) d

||| allocates a C-Array for n doubles
||| @n the number of doubles to store
doubleBuffer : (n: Int) -> IO Ptr
doubleBuffer n = foreign FFI_C "idr_buffers_double_buffer" (Int -> IO Ptr) n

||| convert a List of doubles to a C-Array
doublesToBuffer : List Double -> IO Ptr
doublesToBuffer xs =
  do ptr <- doubleBuffer $ toIntNat $ length xs
     writeDoubleBuffer' ptr Z xs
     pure ptr
  where writeDoubleBuffer' : Ptr -> Nat -> List Double -> IO ()
        writeDoubleBuffer' ptr i []        = pure ()
        writeDoubleBuffer' ptr i (d :: ds) = do setDouble ptr i d
                                                writeDoubleBuffer' ptr (S i) ds

||| the size of a C-double
sizeofDouble : IO Int
sizeofDouble = foreign FFI_C "idr_buffers_double_size" (IO Int)

-- ----------------------------------------------------------------- [ Float Buffers ]

private
setFloat : Ptr -> (idx: Nat) -> Double -> IO ()
setFloat ptr idx d = foreign FFI_C "idr_buffers_set_float" (Ptr -> Int -> Double -> IO ()) ptr (cast idx) d

||| allocates a C-Array of floats for n doubles
||| @n the number of doubles to store
floatBuffer : (n: Int) -> IO Ptr
floatBuffer n = foreign FFI_C "idr_buffers_float_buffer" (Int -> IO Ptr) n

||| converts n Doubles to a C-Array containing n floats
floatsToBuffer : List Double -> IO Ptr
floatsToBuffer xs =
  do ptr <- floatBuffer $ toIntNat $ length xs
     writeFloatBuffer' ptr Z xs
     pure ptr
  where writeFloatBuffer' : Ptr -> Nat -> List Double -> IO ()
        writeFloatBuffer' ptr i []        = pure ()
        writeFloatBuffer' ptr i (d :: ds) = do setFloat ptr i d
                                               writeFloatBuffer' ptr (S i) ds

||| the size of a C-float
sizeofFloat : IO Int
sizeofFloat = foreign FFI_C "idr_buffers_float_size" (IO Int)

-- ----------------------------------------------------------------- [ String Buffers ]

private
setString : Ptr -> (idx: Nat) -> String -> IO ()
setString ptr idx str = foreign FFI_C "idr_buffers_set_string" (Ptr -> Int -> String -> IO ()) ptr (cast idx) str

stringBuffer : (n: Int) -> IO Ptr
stringBuffer n = foreign FFI_C "idr_buffers_string_buffer" (Int -> IO Ptr) n

||| convers n Strings to a C-Array
stringsToBuffer : List String -> IO Ptr
stringsToBuffer xs =
  do ptr <- stringBuffer $ toIntNat $ length xs
     writeStringBuffer' ptr Z xs
     pure ptr
  where writeStringBuffer' : Ptr -> Nat -> List String -> IO ()
        writeStringBuffer' ptr i []        = pure ()
        writeStringBuffer' ptr i (d :: ds) = do setString ptr i d
                                                writeStringBuffer' ptr (S i) ds

freeStringBuffer : Ptr -> (n: Int) -> IO ()
freeStringBuffer ptr n = foreign FFI_C "idr_buffers_free_string_buffer" (Ptr -> Int -> IO ()) ptr n

-- ----------------------------------------------------------------- [ Int Buffers ]

private
setInt : Ptr -> (idx: Nat) -> Int -> IO ()
setInt ptr idx i = foreign FFI_C "idr_buffers_set_int" (Ptr -> Int -> Int -> IO ()) ptr (cast idx) i

private
readInt : Ptr -> (idx: Nat) -> IO Int
readInt ptr idx = foreign FFI_C "idr_buffers_read_int" (Ptr -> Int -> IO Int) ptr (cast idx)

||| allocates a C-Array for n ints
||| @n the number of ints to store
intBuffer : (n: Int) -> IO Ptr
intBuffer n = foreign FFI_C "idr_buffers_int_buffer" (Int -> IO Ptr) n

||| convers n Strings to a C-Array
intsToBuffer : List Int -> IO Ptr
intsToBuffer xs =
  do ptr <- intBuffer $ toIntNat $ length xs
     writeIntBuffer' ptr Z xs
     pure ptr
  where writeIntBuffer' : Ptr -> Nat -> List Int -> IO ()
        writeIntBuffer' ptr i []        = pure ()
        writeIntBuffer' ptr i (d :: ds) = do setInt ptr i d
                                             writeIntBuffer' ptr (S i) ds

||| convert a C-Array of ints to a List
||| @ n how many ints to read from the buffer
intBufferToList : Ptr -> (n: Int) -> IO (List Int)
intBufferToList ptr n = readIntBuffer' ptr [] (cast n)
  where readIntBuffer' : Ptr -> List Int -> Nat -> IO (List Int)
        readIntBuffer' ptr xs Z     = pure xs
        readIntBuffer' ptr xs (S k) = do x <- readInt ptr k
                                         readIntBuffer' ptr (x :: xs) k

||| the size of a C-int
sizeofInt : IO Int
sizeofInt = foreign FFI_C "idr_buffers_int_size" (IO Int)

max_stars_repo_name: spearman/gl-idris

max_issues_repo_name: spearman/gl-idris

max_forks_repo_name: spearman/gl-idris


text:
||| Copyright 2016 Google Inc.
|||
||| Licensed under the Apache License, Version 2.0 (the "License");
||| you may not use this file except in compliance with the License.
||| You may obtain a copy of the License at
|||
|||     http://www.apache.org/licenses/LICENSE-2.0
|||
||| Unless required by applicable law or agreed to in writing, software
||| distributed under the License is distributed on an "AS IS" BASIS,
||| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
||| See the License for the specific language governing permissions and
||| limitations under the License.
|||
||| This module defines a generalized algebraic data type, `MessageDescriptor`,
||| which is the strongly typed equivalent of the `Descriptor` protocol buffer.
||| Because types are first class values in Idris, we can construct a function
||| `interpMessage` that maps a `MessageDescriptor` to the *type* of structure
||| that the message describes.  The ability to treat types as first class
||| values, and to create generic functions allows us to do in Idris code much
||| of what is done with generated code for protocol buffer implementations in
||| other languages.
|||
||| We try to follow the naming conventions for protocol buffer descriptors
||| found in [descriptor.proto](https://developers.google.com/protocol-buffers/docs/reference/cpp/google.protobuf.descriptor.pb) with the exception that we use the name
||| `MessageDescriptor` instead of `Descriptor`.

module Protobuf.Core

import public Data.Fin
import public Data.Vect

%default total
%access public export

||| A `Label` is an annotation on a field that describes what kind of data type
||| the field represents.
data Label : Type where
  ||| `Optional` fields are represented as a `Maybe` type.
  Optional : Label
  ||| `Required` fields are represented as a single value.
  Required : Label
  ||| `Repeated` fields are represented as a `List`.
  Repeated : Label

||| A descriptor for a single value in an enum.
record EnumValueDescriptor where
  constructor MkEnumValueDescriptor
  name : String
  number : Int

||| A descriptor for an enum.
|||
||| k is the size of the enum
||| values is the possible values of the enum.  Note that enum values have a
||| numeric value that is possibly different from the index of the value in
||| `values`, e.g. `values` could be `[MkEnumValueDescriptor "five" 5]`.
record EnumDescriptor where
  constructor MkEnumDescriptor
  name : String
  values : Vect k EnumValueDescriptor

mutual
  ||| A descriptor that describes the type of a protocol buffer message.  This
  ||| describes the type of a protocol buffer message, which is a list of
  ||| fields.
  record MessageDescriptor where
    constructor MkMessageDescriptor
    name : String
    fields : Vect k FieldDescriptor

  ||| A descriptor that describes the type of a protocol buffer field. E.g.
  ||| `MkFieldDescriptor Optional PBDouble "temperature"` describes an
  ||| optional field whose name is "temperature" of type PBDouble, which is
  ||| interpreted Idris as a `Maybe double`.
  |||
  ||| label determines whether the field is optional, required or repeated.
  ||| ty is the type of a single value in the field.
  ||| name is the field's name, used in the text format.
  record FieldDescriptor where
    constructor MkFieldDescriptor
    label : Label
    ty : FieldValueDescriptor
    name : String
    number : Int

  ||| This does not correspond to anything in `descriptor.proto`, but is a
  ||| necessary definition here.  It describes the type of the value of a
  ||| protocol buffer required field, i.e. a single value.  This may be a
  ||| message, an enum or a primitive value.
  data FieldValueDescriptor : Type where
    PBDouble : FieldValueDescriptor
    PBFloat : FieldValueDescriptor
    PBInt32 : FieldValueDescriptor
    PBInt64 : FieldValueDescriptor
    PBUInt32 : FieldValueDescriptor
    PBUInt64 : FieldValueDescriptor
    PBSInt32 : FieldValueDescriptor
    PBSInt64 : FieldValueDescriptor
    PBFixed32 : FieldValueDescriptor
    PBFixed64 : FieldValueDescriptor
    PBSFixed32 : FieldValueDescriptor
    PBSFixed64 : FieldValueDescriptor
    PBBool : FieldValueDescriptor
    PBString : FieldValueDescriptor
    PBBytes : FieldValueDescriptor
    ||| A value which is itself a message.
    PBMessage : MessageDescriptor -> FieldValueDescriptor
    PBEnum : EnumDescriptor -> FieldValueDescriptor

interpEnum : EnumDescriptor -> Type
interpEnum (MkEnumDescriptor {k=k} _ _) = Fin k

-- NOTE: we implement Interp* as inductive types rather than as functions,
-- because these allow us to implement type classes such as Eq and Show.
--
-- E.g. if we had a function interpMessage : MessageDescriptor -> Type
-- it would not be possible to define a typeclass implementation
--
-- implementation Eq (interpMessage d) where ...
--
-- but it is possible to define
--
-- implementation Eq (InterpMessage d) where ...
--
-- Type classes also operate differently with respect to unfolding, though
-- that didn't pose any problems while working with functions.

mutual
  ||| Takes a message descriptor and returns the type that that message
  ||| descriptor describes.  This is implemented with the algebraic data type
  ||| `InterpMessage`.
  data InterpMessage : MessageDescriptor -> Type where
    MkMessage : InterpFields fields -> InterpMessage (MkMessageDescriptor name fields)

  ||| `InterpMessage` the algebraic data type used to implement `interpMessage`.
  ||| `InterpMessage fs` is a heterogeneous vector where where the type of each
  ||| element is `interpField` applied to the corresponding element in `fs`.
  ||| While it is possible to construct this type using `Data.HVect`, I haven't
  ||| found a way to satisfy the totality checker when using this approach.
  data InterpFields : (Vect k FieldDescriptor) -> Type where
    Nil  : InterpFields Nil
    (::) : (interpField f) -> (InterpFields m) -> InterpFields (f :: m)

  ||| Takes a field descriptor and returns the type that that field descriptor
  ||| describes.  This is a single value, a `Maybe` or a `List` depending on
  ||| the field's label.
  interpField : FieldDescriptor -> Type
  interpField (MkFieldDescriptor Optional value _ _) = Maybe (interpFieldValue value)
  interpField (MkFieldDescriptor Required value _ _) = interpFieldValue value
  interpField (MkFieldDescriptor Repeated value _ _) = List (interpFieldValue value)

  ||| Interprets a single field value, i.e. the value described by a required
  ||| field.  For primitive types this is a corresponding Idris primitive type.
  ||| For messages this is `interpMessage` for that message.  For enum's it is
  ||| `Fin k` where `k` is the number of values in the enum.
  interpFieldValue : FieldValueDescriptor -> Type
  interpFieldValue PBDouble = Double
  interpFieldValue PBFloat = Double
  interpFieldValue PBInt32 = Integer
  interpFieldValue PBInt64 = Integer
  interpFieldValue PBUInt32 = Integer
  interpFieldValue PBUInt64 = Integer
  interpFieldValue PBSInt32 = Integer
  interpFieldValue PBSInt64 = Integer
  interpFieldValue PBFixed32 = Integer
  interpFieldValue PBFixed64 = Integer
  interpFieldValue PBSFixed32 = Integer
  interpFieldValue PBSFixed64 = Integer
  interpFieldValue PBBool = Bool
  interpFieldValue PBString = String
  interpFieldValue PBBytes = String
  interpFieldValue (PBMessage m) = InterpMessage m
  interpFieldValue (PBEnum e) = interpEnum e

max_stars_repo_name: google/idris-protobuf

max_issues_repo_name: google/idris-protobuf

max_forks_repo_name: google/idris-protobuf


text:
module RhoCalculus

{-
A Reflective Higher-order Calculus
L.G.Meredith MatthiasRadestock
Electronic Notes in Theoretical Computer Science
Volume 141, Issue 5, 22 December 2005, Pages 49-67
http://www.sciencedirect.com/science/article/pii/S1571066105051839
-}

%access export
%default total

mutual
  data Process: Type where
    Zero: Process
    Input: Action -> (P: Process) -> Process
    Lift: (x: Name) -> (P: Process) -> Process
    Drop: (x: Name) -> Process
    Par: (List Process) -> Process

  data Action: Type where
    Act: (x: Name) -> (y: Name) -> Action

  data Name: Type where
    Quote: (P: Process) -> Name

zero: Process
zero = Zero

guard: Name -> Name -> Action
guard nsubj nobj = Act nsubj nobj

input: Name -> Name -> Process -> Process
input nsubj nobj cont = Input (Act nsubj nobj) cont

prefix_: Action -> Process -> Process
prefix_ (Act (Quote proc1) (Quote proc2)) cont = Input (Act (Quote proc1) (Quote proc2)) cont

lift: Name -> Process -> Process
lift nsubj cont = Lift nsubj cont

drop: Name -> Process
drop n = Drop n

par: Process -> Process -> Process
par (Par proclist1) (Par proclist2) = Par (proclist1 ++ proclist2)
par (Par proclist) proc = Par (proclist ++ [proc])
par proc (Par proclist) = Par ([proc] ++ proclist)
par p1 p2 = Par [p1, p2]

parstar: List Process -> Process
parstar [] = Zero
parstar (proclisthd :: proclisttl) = foldl par proclisthd proclisttl

quote : Process -> Name
quote proc = Quote proc

mutual
  processQuoteDepth: Process -> Nat  -- TODO: prove totality
  processQuoteDepth Zero = 0
  processQuoteDepth (Input (Act nsubj nobj) cont) =
    maximum (nameQuoteDepth nsubj) (processQuoteDepth cont)
  processQuoteDepth (Lift nsubj cont) =
    maximum (nameQuoteDepth nsubj) (processQuoteDepth cont)
  processQuoteDepth (Drop n) = nameQuoteDepth n
  processQuoteDepth (Par procs) =
   assert_total $ foldl (\qD, proc => maximum qD (processQuoteDepth proc))
         0
         procs

  nameQuoteDepth: Name -> Nat
  nameQuoteDepth (Quote proc) = assert_total $ 1 + (processQuoteDepth proc)

syntax [x] "[" [y] "]" = output x y
output : Name -> Name -> Process
output x y = Lift x $ Drop y

exampleName: Name
exampleName = Quote Zero

twoNewProcesses: List Process
twoNewProcesses =
  [qz[qz],
   Input (Act qz qz) Zero]
 where
   qz = Quote Zero

moreNames: List Name
moreNames = map Quote twoNewProcesses

max_stars_repo_name: jimscarver/togl

max_issues_repo_name: jimscarver/togl

max_forks_repo_name: jimscarver/togl


text:
module CFT.Containers

record SCont (n : Nat) where
    constructor MkSCont
    shapes : Type
    seq : (x, y : shapes) -> Dec (x = y)
    positions : shapes -> Type

-- SExt : {n : Nat} -> SCont n -> Vect n Type -> Type
-- SExt (MkSCont shapes seq pos) x =
--     DPair shapes (\s => ((i : Fin n) -> (Vect (pos i s) (index i x))))

-- ex : {n : Nat} -> String
-- ex {n} = "hello" ++ show n
--
--
-- main : IO ()
-- main = putStrLn ex

max_stars_repo_name: andrevidela/dev-notes

max_issues_repo_name: andrevidela/dev-notes

max_forks_repo_name: andrevidela/dev-notes


text:
module Extra.Vect

import public Data.Vect
import Data.List1
import Data.List

public export
toList1 : Vect (S n) a -> List1 a
toList1 (x :: xs) = x ::: toList xs


text:
module Client.Action.Archive

import Data.Buffer
import Data.Maybe
import Extra.Buffer
import Inigo.Archive.Archive
import Inigo.Async.Archive
import Inigo.Async.Promise
import Inigo.Package.Package
import Inigo.Async.FS
import Inigo.Async.Package
import System.Path

export
buildArchive : String -> String -> Promise ()
buildArchive packageFile outFile =
  do
    package <- Inigo.Async.Package.readPackage packageFile
    Inigo.Async.Archive.saveArchive package (fromMaybe "" $ parent packageFile) outFile

export
extractArchive : String -> String -> Promise ()
extractArchive archiveFile outPath =
  do
    archive <- fs_readFileBuf archiveFile
    Inigo.Async.Archive.extractArchive archive outPath

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Text.Markup.Edda.Model.Common

%default total
%access public export

data FontTy   = SerifTy | SansTy | ScapTy | MonoTy
data QuoteTy  = SQuote | DQuote
data CiteSty  = ParenSty | TextSty
data ParenTy  = Parents | Brackets | Braces
data LinkTy   = HyperTy | ExposedTy | FnoteTy | RefTy | CiteTy
data MarkupTy = BoldTy | EmphTy | StrikeTy | UlineTy
data RawTy    = VerbTy | CodeTy | MathTy

data TextBlockTy = ParaTy | TheoremTy | CorollaryTy | LemmaTy | PropositionTy | ProofTy | DefinitionTy
               | ExerciseTy | NoteTy | ProblemTy | QuestionTy | RemarkTy
               | SolutionTy | ExampleTy | QuotationTy

data VerbBlockTy = CommentTy | ListingTy | LiteralTy | EquationTy

data ListTy = BulletTy | NumberTy

||| Add different block types but that will require adding predicated lists
data EddaTy = INLINE | BLOCK | SNIPPET | DOC

data ValidSnippet : EddaTy -> Type where
  IsInLine : ValidSnippet INLINE
  IsBlock  : ValidSnippet BLOCK

implementation Eq EddaTy where
    (==) INLINE  INLINE  = True
    (==) BLOCK   BLOCK   = True
    (==) DOC     DOC     = True
    (==) SNIPPET SNIPPET = True
    (==) _      _        = False

implementation Eq FontTy where
    (==) SerifTy SerifTy = True
    (==) SansTy  SansTy  = True
    (==) ScapTy  ScapTy  = True
    (==) MonoTy  MonoTy  = True
    (==) _       _       = False

implementation Eq QuoteTy where
    (==) SQuote SQuote = True
    (==) DQuote DQuote = True
    (==) _      _      = False

implementation Eq CiteSty where
    (==) ParenSty ParenSty = True
    (==) TextSty  TextSty  = True
    (==) _        _        = False

implementation Eq ParenTy where
    (==) Parents  Parents  = True
    (==) Brackets Brackets = True
    (==) Braces   Braces   = True
    (==) _        _        = False

implementation Eq LinkTy where
    (==) HyperTy   HyperTy   = True
    (==) ExposedTy ExposedTy = True
    (==) FnoteTy   FnoteTy   = True
    (==) RefTy     RefTy     = True
    (==) CiteTy    CiteTy    = True
    (==) _         _         = False

implementation Eq MarkupTy where
    (==) BoldTy   BoldTy   = True
    (==) EmphTy   EmphTy   = True
    (==) StrikeTy StrikeTy = True
    (==) UlineTy  UlineTy  = True
    (==) _        _        = False

implementation Eq RawTy where
    (==) VerbTy VerbTy = True
    (==) CodeTy CodeTy = True
    (==) MathTy MathTy = True
    (==) _      _      = False

implementation Eq VerbBlockTy where
    (==) CommentTy  CommentTy  = True
    (==) ListingTy  ListingTy  = True
    (==) LiteralTy  LiteralTy  = True
    (==) EquationTy EquationTy = True
    (==) _          _          = False

implementation Eq TextBlockTy where
    (==) ParaTy         ParaTy        = True
    (==) TheoremTy      TheoremTy     = True
    (==) CorollaryTy    CorollaryTy   = True
    (==) LemmaTy        LemmaTy       = True
    (==) PropositionTy  PropositionTy = True
    (==) ProofTy        ProofTy       = True
    (==) DefinitionTy   DefinitionTy  = True

    (==) ExerciseTy     ExerciseTy    = True
    (==) NoteTy         NoteTy        = True
    (==) ProblemTy      ProblemTy     = True
    (==) QuestionTy     QuestionTy    = True
    (==) RemarkTy       RemarkTy      = True

    (==) SolutionTy     SolutionTy    = True
    (==) ExampleTy      ExampleTy     = True
    (==) QuotationTy    QuotationTy   = True
    (==) _              _             = False

implementation Eq ListTy where
  (==) BulletTy BulletTy = True
  (==) NumberTy NumberTy = True
  (==) _        _        = False

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
{-
  Copyright 2018 Double-oxygeN

  Licensed under the Apache License, Version 2.0 (the "License");
  you may not use this file except in compliance with the License.
  You may obtain a copy of the License at

      http://www.apache.org/licenses/LICENSE-2.0

  Unless required by applicable law or agreed to in writing, software
  distributed under the License is distributed on an "AS IS" BASIS,
  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  See the License for the specific language governing permissions and
  limitations under the License.
-}

module Partition

%default total
%access export

-- define decreasing rule
public export
(>=) : Nat -> Nat -> Type
(>=) = GTE

public export
data IsDecreasing : List Nat -> Type where
  DecEmpty :
    IsDecreasing Nil

  DecSingle :
    (a: Nat) -> a >= 1 ->
    IsDecreasing (a :: Nil)

  DecMany :
    (a1: Nat) -> (a2: Nat) -> (ax: List Nat) ->
    a1 >= a2 -> IsDecreasing (a2 :: ax) ->
    IsDecreasing (a1 :: a2 :: ax)

-- some theorems

succDec : IsDecreasing (x :: xs) -> IsDecreasing ((S x) :: xs)
succDec (DecSingle x proofXIsPositive) = DecSingle (S x) (lteSuccRight proofXIsPositive)
succDec (DecMany x y ys proofXGteY proofYYsIsDec) = DecMany (S x) y ys (lteSuccRight proofXGteY) proofYYsIsDec

-- define partition
namespace Partition
  public export
  data Par : Type where
    MkPar : (ls: List Nat) -> IsDecreasing ls -> Par

  ParNil : Par
  ParNil = MkPar Nil DecEmpty

  -- partition utility functions
  toList : Par -> List Nat
  toList (MkPar ls _) = ls

  index : (n: Nat) -> (l: Par) -> {auto ok: InBounds n (toList l)} -> Nat
  index n l = Prelude.List.index n (Partition.toList l)

  length : Par -> Nat
  length l = length $ toList l

  multiplicity : Nat -> Par -> Nat
  multiplicity e l = length $ elemIndices e (toList l)

  tail : Par -> Par
  tail (MkPar Nil _) = ParNil
  tail (MkPar (x :: Nil) _) = ParNil
  tail (MkPar (x :: y :: ys) (DecMany x y ys _ proofYYsIsDec)) = (MkPar (y :: ys) proofYYsIsDec)

  sizePar : Par -> Nat
  sizePar (MkPar Nil _) = Z
  sizePar (MkPar (x :: Nil) (DecSingle _ _)) = x
  sizePar (MkPar (x :: y :: ys) (DecMany x y ys proofXGteY proofYYsIsDec)) =
    x + sizePar (assert_smaller (MkPar (x :: y :: ys) (DecMany x y ys proofXGteY proofYYsIsDec)) (MkPar (y :: ys) proofYYsIsDec))

Show Par where
  show l = "(" ++ (join "," (toList l)) ++ ")"
  where
    join : (Show a) => String -> List a -> String
    join _ Nil = ""
    join _ (x :: Nil) = show x
    join s (x :: xs) = (show x) ++ s ++ (join s xs)

-- define partition of size N
public export
data ParN : Nat -> Type where
  MkParN : (l: Par) -> sizePar l = n -> ParN n

-- partition with limit
data ParUpper : Nat -> Type where
  MkParUpper : (k: Nat) -> (ls: List Nat) -> IsDecreasing (k :: ls) -> ParUpper k

forgetUpper : ParUpper k -> Par
forgetUpper (MkParUpper k Nil _) = ParNil
forgetUpper (MkParUpper k _ (DecMany _ x xs _ proofXXsIsDec)) = MkPar (x :: xs) proofXXsIsDec

parUpperKIsParUpperSuccK : ParUpper k -> ParUpper (S k)
parUpperKIsParUpperSuccK (MkParUpper k ls proofKLsIsDec) =
  MkParUpper (S k) ls (succDec proofKLsIsDec)

parUpperCons : (k1: Nat) -> k1 >= k2 -> ParUpper k2 -> ParUpper k1
parUpperCons k1 proofK1GteK2 (MkParUpper k2 ls proofK2LsIsDec) =
  case proofK2LsIsDec of
    DecSingle _ proofK2IsPos => MkParUpper k1 [k1] (DecMany k1 k1 [] lteRefl (DecSingle k1 (lteTransitive proofK2IsPos proofK1GteK2)))
    DecMany _ y ys proofK2GteY proofYYsIsDec => MkParUpper k1 (k1 :: y :: ys) (DecMany k1 k1 (y :: ys) lteRefl (DecMany k1 y ys (lteTransitive proofK2GteY proofK1GteK2) proofYYsIsDec))

-- get all Par(N)
naiveAllParNUpper : (k: Nat) -> Nat -> List (ParUpper k)
naiveAllParNUpper Z _ = Nil
naiveAllParNUpper (S k) Z = (MkParUpper (S k) Nil (DecSingle (S k) (LTESucc LTEZero))) :: Nil
naiveAllParNUpper (S k) n with ((S k) <= n)
  | False = parUpperKIsParUpperSuccK <$> naiveAllParNUpper k n
  | True  = ((parUpperCons (S k) lteRefl) <$> naiveAllParNUpper (S k) (assert_smaller n (n `minus` (S k)))) ++ (parUpperKIsParUpperSuccK <$> (naiveAllParNUpper k n))

naiveAllParN : Nat -> List Par
naiveAllParN n = forgetUpper <$> naiveAllParNUpper n n


text:
module SkepticLang.PairUtils

%access public export

||| Compares the second element in two pairs.
|||
||| @x  the first pair
||| @y  the second pair
compareSnd : Ord b => (x : (a, b)) -> (y : (a, b)) -> Ordering
compareSnd (_, x') (_, y') = compare x' y'

max_stars_repo_name: sr-lab/skeptic-lang

max_issues_repo_name: sr-lab/skeptic-lang

max_forks_repo_name: sr-lab/skeptic-lang


text:
module TyTTP.Adapter.Node.URI

import Control.Monad.Maybe
import Node.URI
import TyTTP

export
uri : Alternative m
  => (
    Step me String h1 s h2 a b
    -> m $ Step me' String h1' s' h2' a' b'
  )
  -> Step me String h1 s h2 a b
  -> m $ Step me' String h1' s' h2' a' b'
uri handler step = case decodeURI step.request.url of
  Right str => handler $ { request.url := str } step
  Left _ => empty

export
uri' : Monad m
  => (
    Step me String h1 s h2 a b
    -> m $ Step me' String h1' s' h2' a' b'
  )
  -> (
    Step me String h1 s h2 a b
    -> MaybeT m $ Step me' String h1' s' h2' a' b'
  )
  -> Step me String h1 s h2 a b
  -> m $ Step me' String h1' s' h2' a' b'
uri' defHandler handler step = do
  Just result <- runMaybeT $ uri handler step
    | Nothing => defHandler step
  pure result

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp