text:
module Data.Bool.Algebra

import Control.Algebra
import Data.Bool.Xor

%default total

-- && is Bool -> Lazy Bool -> Bool,
-- but Bool -> Bool -> Bool is required
and : Bool -> Bool -> Bool
and True True = True
and _ _ = False

Semigroup Bool where
  (<+>) = xor

SemigroupV Bool where
  semigroupOpIsAssociative = xorAssociative

Monoid Bool where
  neutral = False

MonoidV Bool where
  monoidNeutralIsNeutralL True = Refl
  monoidNeutralIsNeutralL False = Refl

  monoidNeutralIsNeutralR True = Refl
  monoidNeutralIsNeutralR False = Refl

Group Bool where
  -- Each Bool is its own additive inverse.
  inverse = id

  groupInverseIsInverseR True = Refl
  groupInverseIsInverseR False = Refl

AbelianGroup Bool where
  groupOpIsCommutative = xorCommutative

Ring Bool where
  (<.>) = and

  ringOpIsAssociative True True True = Refl
  ringOpIsAssociative True True False = Refl
  ringOpIsAssociative True False True = Refl
  ringOpIsAssociative True False False = Refl
  ringOpIsAssociative False True True = Refl
  ringOpIsAssociative False False True = Refl
  ringOpIsAssociative False True False = Refl
  ringOpIsAssociative False False False = Refl

  ringOpIsDistributiveL True True True = Refl
  ringOpIsDistributiveL True True False = Refl
  ringOpIsDistributiveL True False True = Refl
  ringOpIsDistributiveL True False False = Refl
  ringOpIsDistributiveL False True True = Refl
  ringOpIsDistributiveL False False True = Refl
  ringOpIsDistributiveL False True False = Refl
  ringOpIsDistributiveL False False False = Refl

  ringOpIsDistributiveR True True True = Refl
  ringOpIsDistributiveR True True False = Refl
  ringOpIsDistributiveR True False True = Refl
  ringOpIsDistributiveR True False False = Refl
  ringOpIsDistributiveR False True True = Refl
  ringOpIsDistributiveR False False True = Refl
  ringOpIsDistributiveR False True False = Refl
  ringOpIsDistributiveR False False False = Refl

RingWithUnity Bool where
  unity = True

  unityIsRingIdL True = Refl
  unityIsRingIdL False = Refl

  unityIsRingIdR True = Refl
  unityIsRingIdR False = Refl


text:
module Node.Free.FileSystem

import Control.Monad.Free

%access public export

FilePath : Type
FilePath = String

Contents : Type
Contents = String

public export
data FileSystemF next
  = WriteFile FilePath Contents next
  | ReadFile FilePath (Contents -> next)

FileSystem : Type -> Type
FileSystem = Free FileSystemF

Functor FileSystemF where
  map f (WriteFile filePath contents next) = WriteFile filePath contents (f next)
  map f (ReadFile filePath nextFn) = ReadFile filePath (f . nextFn)

writeFile : FilePath -> Contents -> FileSystem Unit
writeFile filePath contents = liftFree $ WriteFile filePath contents ()

readFile : FilePath -> FileSystem String
readFile filePath = liftFree $ ReadFile filePath id

ext: idr

max_stars_repo_name: Risto-Stevcev/idris-node-fs

max_issues_repo_name: Risto-Stevcev/idris-node-fs

max_forks_repo_name: Risto-Stevcev/idris-node-fs


text:
module Utils.Shunting

import Core.Core
import Core.FC

%default total

-- The shunting yard algorithm turns a list of tokens with operators into
-- a parse tree expressing the precedence and associativity correctly.
-- We assume that brackets, functions etc are dealt with in a higher level
-- parser, so we're only dealing with operators here.

-- Precedences/associativities
public export
data OpPrec
          = AssocL Nat
          | AssocR Nat
          | NonAssoc Nat
          | Prefix Nat

-- Tokens are either operators or already parsed expressions in some
-- higher level language
public export
data Tok op a = Op FC op OpPrec
              | Expr a

-- The result of shunting is a parse tree with the precedences made explicit
-- in the tree.
-- NOTE: I have been wondering if I can use types to express that the
-- subtrees use lower precedence operators, but my attempts so far have
-- ended up with more complicated types than the function 'higher', below,
-- which is the one that compares precedences. So I've just used simple
-- types instead and will rely on tests. It would be interesting to see if
-- there's a better way though!

public export
data Tree op a = Infix FC op (Tree op a) (Tree op a)
               | Pre FC op (Tree op a)
               | Leaf a

export
(Show op, Show a) => Show (Tree op a) where
  show (Infix _ op l r) = "(" ++ show op ++ " " ++ show l ++ " " ++ show r ++ ")"
  show (Pre _ op l) = "(" ++  show op ++ " " ++ show l ++ ")"
  show (Leaf val) = show val

Show OpPrec where
  show (AssocL p) = "infixl " ++ show p
  show (AssocR p) = "infixr " ++ show p
  show (NonAssoc p) = "infix " ++ show p
  show (Prefix p) = "prefix " ++ show p

export
(Show op, Show a) => Show (Tok op a) where
  show (Op _ op p) = show op ++ " " ++ show p
  show (Expr val) = show val

-- Label for the output queue state
data Out : Type where

output : List (Tree op a) -> Tok op a ->
         Core (List (Tree op a))
output [] (Op _ _ _) = throw (InternalError "Invalid input to shunting")
output (x :: stk) (Op loc str (Prefix _)) = pure $ Pre loc str x :: stk
output (x :: y :: stk) (Op loc str _) = pure $ Infix loc str y x :: stk
output stk (Expr a) = pure $ Leaf a :: stk
output _ _ = throw (InternalError "Invalid input to shunting")

emit : {auto o : Ref Out (List (Tree op a))} ->
       Tok op a -> Core ()
emit t
    = do out <- get Out
         put Out !(output out t)

getPrec : OpPrec -> Nat
getPrec (AssocL k) = k
getPrec (AssocR k) = k
getPrec (NonAssoc k) = k
getPrec (Prefix k) = k

isLAssoc : OpPrec -> Bool
isLAssoc (AssocL _) = True
isLAssoc _ = False

-- Return whether the first operator should be applied before the second,
-- assuming
higher : Show op => FC -> op -> OpPrec -> op -> OpPrec -> Core Bool
higher loc opx op opy (Prefix p) = pure False
higher loc opx (NonAssoc x) opy oy
    = if x == getPrec oy
         then throw (GenericMsg loc ("Operator '" ++ show opx ++
                                     "' is non-associative"))
         else pure (x > getPrec oy)
higher loc opx ox opy (NonAssoc y)
    = if getPrec ox == y
         then throw (GenericMsg loc ("Operator '" ++ show opy ++
                                     "' is non-associative"))
         else pure (getPrec ox > y)
higher loc opl l opr r
    = pure $ (getPrec l > getPrec r) ||
             ((getPrec l == getPrec r) && isLAssoc l)

processStack : Show op => {auto o : Ref Out (List (Tree op a))} ->
               List (FC, op, OpPrec) -> op -> OpPrec ->
               Core (List (FC, op, OpPrec))
processStack [] op prec = pure []
processStack ((loc, opx, sprec) :: xs) opy prec
    = if !(higher loc opx sprec opy prec)
         then do emit (Op loc opx sprec)
                 processStack xs opy prec
         else pure ((loc, opx, sprec) :: xs)

shunt : Show op => {auto o : Ref Out (List (Tree op a))} ->
        (opstk : List (FC, op, OpPrec)) ->
        List (Tok op a) -> Core (Tree op a)
shunt stk (Expr x :: rest)
    = do emit (Expr x)
         shunt stk rest
shunt stk (Op loc op prec :: rest)
    = do stk' <- processStack stk op prec
         shunt ((loc, op, prec) :: stk') rest
shunt stk []
    = do traverse (\s => emit (Op (sloc s) (sop s) (sprec s))) stk
         [out] <- get Out
             | out => throw (InternalError "Invalid input to shunting")
         pure out
  where
    sloc : (annot, b, c) -> annot
    sloc (x, y, z) = x
    sop : (annot, b, c) -> b
    sop (x, y, z) = y
    sprec : (annot, b, c) -> c
    sprec (x, y, z) = z

export
parseOps : Show op => List (Tok op a) -> Core (Tree op a)
parseOps toks
    = do o <- newRef {t = List (Tree op a)} Out []
         shunt [] toks


text:
module ReadVect

import Data.Vect

%default total

-- reading a vector whose length is known ahead of time

readVectLen : HasIO io => (len : Nat) -> io (Vect len String)
readVectLen Z = pure []
readVectLen (S k) = do x <- getLine
                       xs <- readVectLen k
                       pure (x :: xs)

-- reading a vector whose length is not known ahead of time

||| This type represents a vector whose length is encoded as part of its
||| type, and this length is only known when the program is run
data VectUnknown : Type -> Type where
  MkVect : (len : Nat) -> Vect len a -> VectUnknown a

printVect : HasIO io => Show a => VectUnknown a -> io ()
printVect (MkVect len xs) = putStrLn $ show xs ++ "(length = " ++ show len ++ ")"

partial
readVect : IO (VectUnknown String)
readVect = do x <- getLine
              if x == ""
                 then pure $ MkVect _ []
                 else do MkVect _ xs <- readVect
                         pure $ MkVect _ (x :: xs)

-- The problem with the approach above is that we would have to define
-- such wrapper types for each type that may be read in from an external
-- source. A better way of embedding the length (unknown till runtime)
-- or any other dynamic property along with the data is to use "Dependent Pairs"

-- a dependent pair is a pair where the type of the second element can be computed
-- by the value of the first element of the pair

anyVect : (n : Nat ** Vect n String)
anyVect = (2 ** ["Hello", "world"])

anyVect1 : (n ** Vect n String)
anyVect1 = (3 ** ["Hola", "mundo", "hello"])

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
data Shape = ||| A triangle, with its base length and height
             Triangle Double Double
           | ||| A rectangle, with its length and height
              Rectangle Double Double
           | ||| A circle, with its radius
             Circle Double

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture

testPic1 : Picture
testPic1 = Combine (Primitive (Triangle 2 3))
                   (Primitive (Triangle 2 4))

testPic2 : Picture
testPic2 = Combine (Primitive (Rectangle 1 3))
                   (Primitive (Circle 4))

data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)

%name Tree tree, tree1

insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node left val right)
    = case compare x val of
           LT => Node (insert x left) val right
           EQ => orig
           GT => Node left val (insert x right)

-- Exercise 1
listToTree : Ord a => List a -> Tree a
listToTree [] = Empty
listToTree (x :: xs) = insert x (listToTree xs)

-- Exercise 2
-- The function `treeToList` does an in-order traversal of a tree.
treeToList : Ord a => Tree a -> List a
treeToList Empty = []
treeToList (Node left x right) = (treeToList left) ++ x :: treeToList right

-- Exercise 3
data Expr = Val Integer
          | Add Expr Expr
          | Sub Expr Expr
          | Mul Expr Expr
-- Exercise 4
evaluate : Expr -> Integer
evaluate (Val x) = x
evaluate (Add x y) = evaluate x + evaluate y
evaluate (Sub x y) = evaluate x - evaluate y
evaluate (Mul x y) = evaluate x * evaluate y

-- Exercise 5
maybeMax : Ord a => Maybe a -> Maybe a -> Maybe a
maybeMax Nothing Nothing = Nothing
maybeMax Nothing (Just x) = Just x
maybeMax (Just x) Nothing = Just x
maybeMax (Just x) (Just y) = Just $ max x y

-- Exercise 6
biggestTriangle : Picture -> Maybe Double
biggestTriangle (Primitive tri@(Triangle x y)) = Just $ area tri
biggestTriangle (Primitive _) = Nothing
biggestTriangle (Combine pic1 pic2) = maybeMax (biggestTriangle pic1) (biggestTriangle pic2)
biggestTriangle (Rotate x pic) = biggestTriangle pic
biggestTriangle (Translate x y pic) = biggestTriangle pic


text:
module Temp

import Data.List

safeStrHead : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
safeStrHead s with (unpack s)
  safeStrHead s | [] = absurd pr
  safeStrHead s | (c::_) = c

safeStrHead1 : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
safeStrHead1 s with (unpack s)
  safeStrHead1 {pr} s | [] = absurd pr
  safeStrHead1 s | (c::_) = c

safeStrHead2 : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
safeStrHead2 s with (unpack s)
  safeStrHead2 {pr=foo} s | [] = absurd foo
  safeStrHead2 s | (c::_) = c

safeStrHead3 : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
safeStrHead3 {pr=foo} s with (unpack s)
  safeStrHead3 s | [] = absurd foo
  safeStrHead3 s | (c::_) = c

safeStrHead4 : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
safeStrHead4 {pr=foo} s with (unpack s)
  safeStrHead4 {pr=bar} s | [] = absurd bar
  safeStrHead4 s | (c::_) = c


text:
module Quotient_Type

%access public export
%default total

IsRefl : (typ : Type) -> (rel : typ -> typ -> Type) -> Type
IsRefl typ rel = (a : typ) -> (rel a a)

IsSym : (typ : Type) -> (rel : typ -> typ -> Type) -> Type
IsSym typ rel = (a, b : typ) -> (rel a b) -> (rel b a)

IsTrans : (typ : Type) -> (rel : typ -> typ -> Type) -> Type
IsTrans typ rel = (a, b, c : typ) -> (rel a b) -> (rel b c) -> (rel a c)

IsEqRel : (typ : Type) -> (rel : typ -> typ -> Type) -> Type
IsEqRel typ rel = ( (IsRefl typ rel) , ( (IsSym typ rel), (IsTrans typ rel) ) )

data Quotient_Type : (typ : Type) -> (rel : typ -> typ -> Type) -> Type where
    Cons_quotient_Type : (IsEqRel typ rel) -> (Quotient_Type typ rel)

||| Type of proof that a function passes through the relations

Passes_Through : (ty1 : Type) -> (rel_1 : ty1 -> ty1 -> Type) ->
                 (ty2 : Type) -> (rel_2 : ty2 -> ty2 -> Type) ->
                 (f : ty1 -> ty2) -> Type

Passes_Through ty1 rel_1 ty2 rel_2 f =
    (a, b : ty1) -> (rel_1 a b) -> (rel_2 (f a) (f b))

||| Type of function between two quotient types
data Quotient_Function : (ty1 : Type) -> (rel_1 : ty1 -> ty1 -> Type) ->
                         (ty2 : Type) -> (rel_2 : ty2 -> ty2 -> Type) -> Type where

    Cons_quotient_Function : (f : ty1 -> ty2) -> (Passes_Through ty1 rel_1 ty2 rel_2 f)
        -> (Quotient_Function ty1 rel_1 ty2 rel_2)

||| The type of transports of a relation
Transport_of : (ty : Type) -> (rel : ty -> ty -> Type) -> (P : ty -> Type) -> Type
Transport_of ty rel P = (a, b : ty) -> (rel a b) -> (P a) -> (P b)

||| Definition of a family of quotient types
data Quotient_Family : (ty : Type) -> (rel : ty -> ty -> Type) -> Type where
    Cons_quotient_Family : (P : ty -> Type) -> (Transport_of ty rel P) -> (Quotient_Family ty rel)

||| Given a quotient family gets the underlying family.
get_Family : (ty : Type) -> (rel : ty -> ty -> Type) -> (P : (Quotient_Family ty rel)) ->
             (ty -> Type)
get_Family ty rel (Cons_quotient_Family p tr) = p

||| Given a quotient type gets the transport
get_Transport : (ty : Type) -> (rel : ty -> ty -> Type) -> (P : (Quotient_Family ty rel)) ->
                (Transport_of ty rel (get_Family ty rel P))
get_Transport ty rel (Cons_quotient_Family P tr) = tr

||| Type of proofs that a dependent function passes through the corresponding relations
Passes_Through_Dependent : (ty1 : Type) -> (rel_1 : ty1 -> ty1 -> Type) ->
                           (P : (Quotient_Family ty1 rel_1)) ->
                           (relP : (a : ty1) -> ((get_Family ty1 rel_1 P) a) -> ((get_Family ty1 rel_1 P) a) -> Type) ->
                           (f : (a : ty1) -> ((get_Family ty1 rel_1 P) a) ) -> Type

Passes_Through_Dependent ty1 rel_1 P relP f = (a, b : ty1) -> (pt : rel_1 a b) ->
    ( (relP b) ((get_Transport ty1 rel_1 P) a b pt (f a)) (f b))

||| A proof that any equivalence relation factors through equality
EqRel_factors_through_Eq : (ty : Type) -> (rel : ty -> ty -> Type) -> (IsEqRel ty rel) ->
                           (a, b : ty) -> (a = b) -> (rel a b)

EqRel_factors_through_Eq ty rel pfEqRel a a Refl = (fst pfEqRel) a

||| The condition on the function type A -> B to make it the quotient function type (A, relA) -> (B, relB)
Function_rel : (ty1 : Type) -> (rel1 : ty1 -> ty1 -> Type) -> (IsEqRel ty1 rel1) ->
               (ty2 : Type) -> (rel2 : ty2 -> ty2 -> Type) -> (IsEqRel ty2 rel2) ->
               (f, g : (ty1 -> ty2)) ->
               (Passes_Through ty1 rel1 ty2 rel2 f) ->
               (Passes_Through ty1 rel1 ty2 rel2 g) -> Type

Function_rel ty1 rel1 pfEq1 ty2 rel2 pfEq2 f g pf_f pf_g =
      (a, b : ty1) -> (rel1 a b) -> (rel2 (f a) (g b))

IsRefl_Function_rel : (ty1 : Type) -> (rel1 : ty1 -> ty1 -> Type) -> (pf1 : IsEqRel ty1 rel1) ->
                      (ty2 : Type) -> (rel2 : ty2 -> ty2 -> Type) -> (pf2 : IsEqRel ty2 rel2) ->
                      (f : (ty1 -> ty2)) -> (pf_f : Passes_Through ty1 rel1 ty2 rel2 f) ->
                      (Function_rel ty1 rel1 pf1 ty2 rel2 pf2 f f pf_f pf_f)

IsRefl_Function_rel ty1 rel1 pf1 ty2 rel2 pf2 f pf_f = pf_f

IsSym_Function_rel : (ty1 : Type) -> (rel1 : ty1 -> ty1 -> Type) -> (pf1 : IsEqRel ty1 rel1) ->
                     (ty2 : Type) -> (rel2 : ty2 -> ty2 -> Type) -> (pf2 : IsEqRel ty2 rel2) ->
                     (f : (ty1 -> ty2)) -> (pf_f : Passes_Through ty1 rel1 ty2 rel2 f) ->
                     (g : (ty1 -> ty2)) -> (pf_g : Passes_Through ty1 rel1 ty2 rel2 g) ->
                     (Function_rel ty1 rel1 pf1 ty2 rel2 pf2 f g pf_f pf_g) ->
                     (Function_rel ty1 rel1 pf1 ty2 rel2 pf2 g f pf_g pf_f)

IsSym_Function_rel ty1 rel1 pf1 ty2 rel2 pf2 f pf_f g pf_g pf_rel a b pfab = let

    pf_sym_1 : ((a1 : ty1) -> (b1 : ty1) -> (rel1 a1 b1) -> (rel1 b1 a1))
        = (fst (snd pf1))

    pf_sym_2 : ((a1 : ty2) -> (b1 : ty2) -> (rel2 a1 b1) -> (rel2 b1 a1))
        = (fst (snd pf2))

    pf4 : (rel1 b a)
        = pf_sym_1 a b pfab

    pf5 : (rel2 (f b) (g a))
        = pf_rel b a pf4

    pf6 : (rel2 (g a) (f b))
        = pf_sym_2 (f b) (g a) pf5
    in
    pf6

IsTrans_Function_rel : (ty1 : Type) -> (rel1 : ty1 -> ty1 -> Type) -> (pf1 : IsEqRel ty1 rel1) ->
                       (ty2 : Type) -> (rel2 : ty2 -> ty2 -> Type) -> (pf2 : IsEqRel ty2 rel2) ->
                       (f : (ty1 -> ty2)) -> (pf_f : Passes_Through ty1 rel1 ty2 rel2 f) ->
                       (g : (ty1 -> ty2)) -> (pf_g : Passes_Through ty1 rel1 ty2 rel2 g) ->
                       (h : (ty1 -> ty2)) -> (pf_h : Passes_Through ty1 rel1 ty2 rel2 h) ->
                       (Function_rel ty1 rel1 pf1 ty2 rel2 pf2 f g pf_f pf_g) ->
                       (Function_rel ty1 rel1 pf1 ty2 rel2 pf2 g h pf_g pf_h) ->
                       (Function_rel ty1 rel1 pf1 ty2 rel2 pf2 f h pf_f pf_h)

IsTrans_Function_rel ty1 rel1 pf1 ty2 rel2 pf2 f pf_f g pf_g h pf_h pf_fg pf_gh a b pf_ab = let

    pf3 : (rel2 (f a) (g b))
        = pf_fg a b pf_ab

    pf_refl_1 : ((a1 : ty1) -> rel1 a1 a1)
        = (fst pf1)

    pf_refl_2 : ((a1 : ty2) -> rel2 a1 a1)
        = (fst pf2)

    -- pf4 : (rel2 (g b) (g b))
        -- = pf_refl_2 (g b)

    pf5 : (rel2 (g b) (h b))
        = pf_gh b b (pf_refl_1 b)

    pf_trans_2 : ((a1 : ty2) -> (b1 : ty2) -> (c : ty2) ->
                 (rel2 a1 b1) -> (rel2 b1 c) -> (rel2 a1 c))
        = (snd (snd pf2))

    pf6 : (rel2 (f a) (h b))
        = pf_trans_2 (f a) (g b) (h b) pf3 pf5

    in
    pf6

{-
data Quotient_Dependent_Function : (ty : Type) -> (rel : ty -> ty -> Type) ->
                                  (P : (Quotient_Family ty rel)) -> Type where
    quotient_Dependent_Function : (a, b : ty) -> (rel a b) ->
                    -}


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.

module Test.TextFormat

import Test.UnitTest
import Test.Utils
import Protobuf.Core
import Protobuf.TextFormat

%access export
%default total

johnInTextFormat : String
johnInTextFormat = unlines [
  "name: \"John Doe\"",
  "id: 1234",
  "email: \"jdoe@example.com\"",
  "phone: {",
  "  number: \"123-456-7890\"",
  "  type: HOME",
  "}",
  "phone: {",
  "  number: \"987-654-3210\"",
  "}",
  ""
]

-- Implementing Eq (InterpMessage d) is proving difficult so for testing we
-- implement it by serializing to text format and comparing.
implementation Eq (InterpMessage d) where
  x == y = (show x) == (show y)

Jane : InterpMessage Person
Jane = MkMessage [
  "Jane Doe",
  1234,
  Just "jdoe@example.com",
  [
    MkMessage ["123-456-7890", Just 1],
    MkMessage ["987-654-3210", Nothing]
  ]
]

allTests : IO ()
allTests = runTests (MkTestFixture "TextFormat" [
  MkTestCase "PrintJohn" (assertEq (printToTextFormat John) johnInTextFormat),
  MkTestCase "ParseJohn"
    (assertEq (parseFromTextFormat {d=Person} johnInTextFormat) (Right John)),
  MkTestCase "ParseMessageWithBadField"
    (assertEq
      (parseFromTextFormat {d=Person} "not_a_field: 1")
      (Left "at 1:14 expected:\n  An field in the message Person (no field named \"not_a_field\")")),
  MkTestCase "ParseMessageWithMissingRequiredField"
    (assertEq
        (parseFromTextFormat {d=Person} "id: 1234")
        (Left "at 0:0 expected:\n  A valid message (The required field \"name\" was not set.)")),
  MkTestCase "ParseMessageWithOverriddenRequiredField"
    (assertEq (parseFromTextFormat (johnInTextFormat ++ "name: \"Jane Doe\"\n")) (Right Jane)),
  MkTestCase "ParseDouble"
    (assertEq
      (parseFromTextFormat {d=MkMessageDescriptor "test" [
        MkFieldDescriptor Required PBDouble "double_value" 0
      ]} "double_value: -12.34")
      (Right (MkMessage [-12.34]))),
  MkTestCase "ParseBool" (do {
    (assertEq
      (parseFromTextFormat {d=MkMessageDescriptor "test" [
        MkFieldDescriptor Required PBBool "bool_value" 0
      ]} "bool_value: true")
      (Right (MkMessage [True])))
  })
])

max_stars_repo_name: google/idris-protobuf

max_issues_repo_name: google/idris-protobuf

max_forks_repo_name: google/idris-protobuf


text:
module JS.Buffer

import JS.Marshall

export
data UInt8ClampedArray : Type where [external]

export
ToFFI UInt8ClampedArray UInt8ClampedArray where toFFI = id

export
FromFFI UInt8ClampedArray UInt8ClampedArray where fromFFI = Just

export
data UInt8Array : Type where [external]

export
ToFFI UInt8Array UInt8Array where toFFI = id

export
FromFFI UInt8Array UInt8Array where fromFFI = Just

export
data UInt16Array : Type where [external]

export
ToFFI UInt16Array UInt16Array where toFFI = id

export
FromFFI UInt16Array UInt16Array where fromFFI = Just

export
data UInt32Array : Type where [external]

export
ToFFI UInt32Array UInt32Array where toFFI = id

export
FromFFI UInt32Array UInt32Array where fromFFI = Just

export
data Int8Array : Type where [external]

export
ToFFI Int8Array Int8Array where toFFI = id

export
FromFFI Int8Array Int8Array where fromFFI = Just

export
data Int16Array : Type where [external]

export
ToFFI Int16Array Int16Array where toFFI = id

export
FromFFI Int16Array Int16Array where fromFFI = Just

export
data Int32Array : Type where [external]

export
ToFFI Int32Array Int32Array where toFFI = id

export
FromFFI Int32Array Int32Array where fromFFI = Just

export
data Float32Array : Type where [external]

export
ToFFI Float32Array Float32Array where toFFI = id

export
FromFFI Float32Array Float32Array where fromFFI = Just

export
data Float64Array : Type where [external]

export
ToFFI Float64Array Float64Array where toFFI = id

export
FromFFI Float64Array Float64Array where fromFFI = Just

export
data DataView : Type where [external]

export
ToFFI DataView DataView where toFFI = id

export
FromFFI DataView DataView where fromFFI = Just

export
data ArrayBuffer : Type where [external]

export
ToFFI ArrayBuffer ArrayBuffer where toFFI = id

export
FromFFI ArrayBuffer ArrayBuffer where fromFFI = Just


text:
module Proofs.GroupTheory

import Specifications.Group
import Proofs.GroupCancelationLemmas

%default total
%access export

infixl 8 #

groupInverseUnique : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b : s) ->
  a # b = e -> inv a = b
groupInverseUnique {e} spec a b given = o4 @== o3 where
  o1 : inv a # (a # b) = inv a # e
  o1 = cong given
  o2 : inv a # (a # b) = b
  o2 = groupCancel1bis spec a b
  o3 : inv a # e = b
  o3 = o1 @== o2
  o4 : inv a # e = inv a
  o4 = neutralR (monoid spec) _

groupInverseInvolution : GroupSpec _ _ inv -> (a : s) ->
  inv (inv a) = a
groupInverseInvolution spec a =
  groupInverseUnique spec _ a $
  inverseL spec a

groupInverseMutual : GroupSpec _ _ inv -> (a,b : s) ->
  inv a = b -> inv b = a
groupInverseMutual spec a b given =
  cong given @== groupInverseInvolution spec a

groupInverseUniqueBis : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b : s) ->
  a # b = e -> inv b = a
groupInverseUniqueBis spec a b given =
  groupInverseMutual spec a b $
  groupInverseUnique spec a b given

groupInverseNeutral : GroupSpec _ e inv -> inv e = e
groupInverseNeutral {e} spec =
  groupInverseUnique spec e e $
  neutralL (monoid spec) e

groupInverseAnti : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b : s) ->
  inv (a # b) = inv b # inv a
groupInverseAnti spec a b = groupInverseUniqueBis spec _ _ o3 where
  o1 : inv b # inv a # a = inv b
  o1 = groupCancel2bis spec _ a
  o2 : inv b # inv a # a # b = inv b # b
  o2 = cong {f = (# b)} o1
  o3 : inv b # inv a # (a # b) = e
  o3 = associative (monoid spec) _ _ _ === o2 === inverseL spec b

groupInverseAntiInverse : {(#) : Binop s} ->
  GroupSpec (#) e inv -> (a,b : s) ->
    inv (a # inv b) = b # inv a
groupInverseAntiInverse spec a b = o1 === o2 where
  o1 : inv (a # inv b) = inv (inv b) # inv a
  o1 = groupInverseAnti spec a (inv b)
  o2 : inv (inv b) # inv a = b # inv a
  o2 = cong {f = (# inv a)} $ groupInverseInvolution spec b

groupInverseAndEquality : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b : s) ->
  a # inv b = e -> a = b
groupInverseAndEquality {e} spec a b given = o2 @== o1 where
  o1 : a # inv b # b = b
  o1 = cong {f = (# b)} given === neutralL (monoid spec) b
  o2 : a # inv b # b = a
  o2 = groupCancel2bis spec a b

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module VectMonadLaws

import Data.Vect

%default total

mapFuses : (g : b -> c) -> (f : a -> b) -> (xs : Vect n a) -> map g (map f xs) = map (g . f) xs
mapFuses g f []      = Refl
mapFuses g f (_::xs) = rewrite mapFuses g f xs in Refl

bindPureIsMap : (xs : Vect n a) -> (f : a -> b) -> map f xs = xs >>= \x => pure $ f x
bindPureIsMap [] f = Refl
bindPureIsMap {n=S n} (_::xs) f = rewrite bindPureIsMap xs f in
                                  rewrite mapFuses tail (\x => f x :: replicate n (f x)) xs in
                                  Refl

apThruBind' : (fs : Vect n (a -> b)) -> (xs : Vect n a) -> fs <*> xs = fs >>= (`map` xs)
apThruBind' [] [] = Refl
apThruBind' (_::fs) (x::xs) = rewrite mapFuses tail (\f' => f' x :: map f' xs) fs in
                              rewrite apThruBind' fs xs in
                              Refl

0 funext : {f, g : a -> b} -> ((x : a) -> f x = g x) -> f = g
funext _ = believe_me $ the (0 = 0) Refl

apThruBind : (fs : Vect n (a -> b)) -> (xs : Vect n a) -> fs <*> xs = fs >>= \f' => xs >>= \x' => pure (f' x')
apThruBind fs xs = trans (apThruBind' fs xs) $
                     cong diag $ cong (`map` fs) $
                       funext $ bindPureIsMap xs

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
||| Common types and instances for JSON interoperability.
|||
||| (C) The Idris Community, 2021
module Language.LSP.Message.Utils

import Language.JSON
import Language.JSON.Interfaces
import Language.LSP.Message.Derive

%default total

-- TODO: Upstream this implementations.
public export
Foldable (Pair a) where
  foldr f init (_, input) = f input init
  null _ = False

public export
Traversable (Pair a) where
  traverse f (x, y) = (x,) <$> f y

public export
Eq JSON where
  JNull        == JNull        = True
  (JBoolean x) == (JBoolean y) = x == y
  (JNumber x)  == (JNumber y)  = x == y
  (JString x)  == (JString y)  = x == y
  (JArray xs)  == (JArray ys)  = assert_total $ xs == ys
  (JObject xs) == (JObject ys) = assert_total $ xs == ys
  _ == _ = False

||| Singleton type that models `null` in JSON.
public export
data Null = MkNull

public export
Eq Null where
  MkNull == MkNull = True

public export
Ord Null where
  compare MkNull MkNull = EQ

public export
Show Null where
  show MkNull = "null"

export
ToJSON Null where
  toJSON MkNull = JNull

export
FromJSON Null where
  fromJSON JNull = pure MkNull
  fromJSON _ = neutral

||| Data type isomorphic to `Either`, but is translated untagged from and to JSON.
public export
data UntaggedEither a b = Left a | Right b

export
(Eq a, Eq b) => Eq (UntaggedEither a b) where
  (Left x)  == (Left y)  = x == y
  (Right x) == (Right y) = x == y
  _ == _ = False

export
(Ord a, Ord b) => Ord (UntaggedEither a b) where
  compare (Left x)  (Left y)  = compare x y
  compare (Left _)  (Right _) = LT
  compare (Right _) (Left _)  = GT
  compare (Right x) (Right y) = compare x y

export
(Show a, Show b) => Show (UntaggedEither a b) where
  showPrec p (Left x)  = showCon p "Left" $ showArg x
  showPrec p (Right y) = showCon p "Right" $ showArg y

export
Bifunctor UntaggedEither where
  bimap f g (Left x) = Left (f x)
  bimap f g (Right x) = Right (g x)

infixr 0 .+.
||| Operator synonym for `UntaggedEither`.
public export
(.+.) : Type -> Type -> Type
(.+.) = UntaggedEither

||| Converts an `UntaggedEither` value to the isomorphic value in `Either`.
public export
toEither : UntaggedEither a b -> Either a b
toEither (Left x)  = Left x
toEither (Right x) = Right x

||| Converts an `Either` value to the isomorphic value in `UntaggedEither`.
public export
fromEither : Either a b -> UntaggedEither a b
fromEither (Left x)  = Left x
fromEither (Right x) = Right x

public export
toMaybe : UntaggedEither a Null -> Maybe a
toMaybe (Left x) = Just x
toMaybe (Right MkNull) = Nothing

public export
fromMaybe : Maybe a -> UntaggedEither a Null
fromMaybe (Just x) = Left x
fromMaybe Nothing = Right MkNull

export
(ToJSON a, ToJSON b) => ToJSON (UntaggedEither a b) where
  toJSON (Left x)  = toJSON x
  toJSON (Right x) = toJSON x

export
(FromJSON a, FromJSON b) => FromJSON (UntaggedEither a b) where
  -- NOTE: The rightmost type is parsed first, since in the LSP specification
  --       the most specific type appears also rightmost.
  fromJSON v = (Right <$> fromJSON v) <|> (Left <$> fromJSON v)


text:
module AssRecRule

import Data.Fin
import Data.Vect

%default total

||| The recursion function for lists of type `a`. Define this by pattern matching

recList : (a : Type) ->  (x : Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)

recList ty1 ty2 elem fun Nil = elem
recList ty1 ty2 elem fun (x :: xs) = (fun x xs (recList ty1 ty2 elem fun xs))

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

||| Given a list of type `a` and a function `f: a -> b` get a list of type `b` by applying `f` to each element.
||| Note: Define using `recList` and without pattern matching on lists.

mapList : (a : Type) -> (b : Type) -> (f : a -> b) -> List a -> List b

mapList ty1 ty2 f = recList ty1 (List ty2) Nil fun where

    fun : ty1 -> (List ty1) -> (List ty2) -> (List ty2)
    fun x xs ys = (f x) :: ys

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

||| Given a list of type `a`, an initial value `init : a` and an operation `op: a -> a -> a`,
||| get an element of `a` by starting with init and repeatedly applying the elements of the list.
||| e.g. fold Nat 1 (*) ([22] :: [3] :: [])  = 1 * 22 * 3
||| Note: Define using `recList` and without pattern matching on lists.

foldList : (a : Type) ->  (init : a) -> (op : a -> a -> a) -> List a -> a

foldList ty init op = recList ty ty init fun where
    fun : ty -> (List ty) -> ty -> ty
    fun x xs y = (op x y) -- it can be defined as (op y x) also depending on the need

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

||| The induction function on the `Fin` indexed type family.
||| Define this by pattern matching.

inducFin : (xs : (n: Nat) -> Fin n -> Type) ->
  (base : (m: Nat) -> xs (S m) FZ) ->
  (step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))) ->
  (q: Nat) -> (j: Fin q) -> xs q j

inducFin xs base step Z k impossible
inducFin xs base step (S q) FZ = base q
inducFin xs base step (S Z) (FS k) impossible
inducFin xs base step (S (S q)) (FS k) = step (S q) k (inducFin xs base step (S q) k)

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

||| Given a type `a`, a natural number `q`, an element `j : Fin q` and a vector `v` of length q with entries of type `a`,
||| get the element in position `j` of `v`. Note that this is always well defined.
||| Note: Define using `inducFin` and without pattern matching on the `Fin` family. You may pattern match on Vectors.

fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)

fetchElem ty q j = inducFin family base step q j where

    family : (n : Nat) -> (Fin n) -> Type
    family n k = (Vect n ty) -> ty

    base : (m : Nat) -> (family (S m) FZ)
    base m (x :: xs) = x

    step : (p : Nat) -> (k : Fin p) -> (prev : (family p k)) -> (family (S p) (FS k))
    step p k prev (x :: xs) = prev xs


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

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

TupleVect : (length : Nat) -> (ty : Type) -> Type
TupleVect Z _ = ()
TupleVect (S k) x = (x, TupleVect k x)

test : TupleVect 4 Nat
test = (1,2,3,4,())


text:
module Main

import Control.ST
import Data.IORef
import Control.IOExcept
import Control.ST.Exception
import Data.SortedMap
import Util
import DataTypes
import Environment
import Eval
import Repl

%access public export

notVoid : LispVal -> Bool
notVoid LispVoid = False
notVoid _ = True

replEval : String -> JS_IO String
replEval s = ioe_run (run (do envRef <- primitiveBindings
                              lispVals <- evalExprList envRef s
                              let lispValString = unlines $ map show (filter notVoid lispVals)
                              pure lispValString))
                     (\err => pure $ show err)
                     (\ok  => pure ok)

run : String -> JS_IO String
run s = do
    {-#
    Right identity dictates this can be simplified, but
    unfortunately that is not the case right now.
    https://github.com/idris-lang/Idris-dev/issues/4656
    #-}
    out <- replEval s
    pure out

expList : FFI_Export FFI_JS "" []
expList = Fun run "run" $
          End

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module LightClick.Types.Compatibility

import public Toolkit.Decidable.Equality.Indexed

import public Toolkit.Decidable.Informative

import Toolkit.Data.Rig
import Toolkit.Data.Vect.Extra

import LightClick.Types.Meta
import LightClick.Types.Direction
import LightClick.Types.Sensitivity
import LightClick.Types.WireType

import LightClick.Types
import LightClick.Types.Equality

%default total

namespace Data

  mutual
    namespace Fields
      public export
      data Compatible : (kxs : Vect n (Pair String (Ty DATA)))
                     -> (kys : Vect m (Pair String (Ty DATA)))
                                 -> Type
        where
          Empty : Compatible Nil Nil
          Cons : (compatLabels :                     i        =  j)
              -> (compatTypes  : Data.Compatible       a           b)
              -> (rest         : Fields.Compatible         xs          ys)
                              -> Fields.Compatible ((i,a)::xs) ((j,b)::ys)

    public export
    data Compatible : (x,y : Ty DATA) -> Type where
      CompatLogic : Data.Compatible TyLogic TyLogic
      CompatArray : (sameLength : i = j)
                 -> (types      : Data.Compatible a b)
                               -> Data.Compatible (TyArray a i)
                                                  (TyArray b j)
      CompatStruct : (compatFields : Fields.Compatible xs ys)
                                  -> Data.Compatible (TyStruct xs) (TyStruct ys)
      CompatUnion : (compatFields : Fields.Compatible xs ys)
                                 -> Data.Compatible (TyUnion xs) (TyUnion ys)

    export
    posFlip : Data.Compatible l r -> Data.Compatible r l
    posFlip (CompatArray Refl prf) = CompatArray Refl (posFlip prf)
    posFlip (CompatStruct prfs) = CompatStruct (posFlips prfs)
    posFlip (CompatUnion  prfs) = CompatUnion (posFlips prfs)
    posFlip CompatLogic = CompatLogic

    export
    negFlip : (Data.Compatible l r -> Void) -> Data.Compatible r l -> Void
    negFlip f (CompatArray Refl prf) = f (CompatArray Refl (posFlip prf))
    negFlip f (CompatStruct prfs) = f (CompatStruct (posFlips prfs))
    negFlip f (CompatUnion  prfs) = f (CompatUnion (posFlips prfs))
    negFlip f CompatLogic = f CompatLogic

    export
    posFlips : (Fields.Compatible ls rs) -> Fields.Compatible rs ls
    posFlips Empty = Empty
    posFlips (Cons Refl prf rest) = Cons Refl (posFlip prf) (posFlips rest)

namespace Logic
  export
  logicNotCompatWithArray : Data.Compatible TyLogic (TyArray l t) -> Void
  logicNotCompatWithArray (CompatArray _ _) impossible
  logicNotCompatWithArray (CompatStruct _) impossible
  logicNotCompatWithArray (CompatUnion _) impossible
  logicNotCompatWithArray CompatLogic impossible

  export
  logicNotCompatWithStruct : Data.Compatible TyLogic (TyStruct xs) -> Void
  logicNotCompatWithStruct (CompatArray _ _) impossible
  logicNotCompatWithStruct (CompatStruct _) impossible
  logicNotCompatWithStruct (CompatUnion _) impossible
  logicNotCompatWithStruct CompatLogic impossible

  export
  logicNotCompatWithUnion : Data.Compatible TyLogic (TyUnion xs) -> Void
  logicNotCompatWithUnion (CompatArray _ _) impossible
  logicNotCompatWithUnion (CompatStruct _) impossible
  logicNotCompatWithUnion (CompatUnion _) impossible
  logicNotCompatWithUnion CompatLogic impossible

namespace Array

  export
  arraysNotSameLength : (contra : (k = j) -> Void)
                     -> Data.Compatible (TyArray x k) (TyArray y j)
                     -> Void
  arraysNotSameLength contra (CompatArray prf x) = contra prf

  export
  arraysNotSameType : (f : Data.Compatible x y -> Void)
                   -> Data.Compatible (TyArray x j) (TyArray y j)
                   -> Void
  arraysNotSameType f (CompatArray Refl x) = f x

  export
  arrayNotCompatWithStruct : Data.Compatible (TyArray x k) (TyStruct xs) -> Void
  arrayNotCompatWithStruct (CompatArray _ _) impossible
  arrayNotCompatWithStruct (CompatStruct _) impossible
  arrayNotCompatWithStruct (CompatUnion _) impossible
  arrayNotCompatWithStruct CompatLogic impossible

  export
  arrayNotCompatWithUnion : Data.Compatible (TyArray x k) (TyUnion xs) -> Void
  arrayNotCompatWithUnion (CompatArray _ _) impossible
  arrayNotCompatWithUnion (CompatStruct _) impossible
  arrayNotCompatWithUnion (CompatUnion _ ) impossible
  arrayNotCompatWithUnion CompatLogic impossible

namespace Struct

  export
  structNotCompatWithUnion : Data.Compatible (TyStruct xs) (TyUnion ys) -> Void
  structNotCompatWithUnion (CompatArray _ _) impossible
  structNotCompatWithUnion (CompatStruct _) impossible
  structNotCompatWithUnion (CompatUnion _ ) impossible
  structNotCompatWithUnion CompatLogic impossible

  export
  structsAreNotCompat : (Compatible xs ys -> Void) -> Compatible (TyStruct xs) (TyStruct ys) -> Void
  structsAreNotCompat contra (CompatStruct prf) = contra prf

namespace Union

  export
  unionsAreNotCompat : (Compatible xs ys -> Void) -> Compatible (TyUnion xs) (TyUnion ys) -> Void
  unionsAreNotCompat contra (CompatUnion prf) = contra prf

namespace Data
  public export
  data Error : Type where
    Mismatch : Data.Error
    MismatchArrayLength : Data.Error
    MismatchArrayType   : (error : Data.Error) -> Data.Error
    MismatchStructureFieldType  : (position : Nat) -> (error : Data.Error) -> Data.Error
    MismatchStructureFieldLabel  : (position : Nat) -> (x,y : String) -> Data.Error
    MismatchStructureLength : Data.Error

-- [ Function Declaration ]

export
compatible : (x : Ty DATA)
          -> (y : Ty DATA)
                 -> DecInfo Data.Error
                            (Data.Compatible x y)

namespace Fields
  fieldMismatchLabel : (xl = yl -> Void)
                    -> Fields.Compatible ((xl, xt) :: xs) ((yl, yt) :: ys)
                    -> Void
  fieldMismatchLabel contra (Cons Refl prf rest) = contra Refl

  fieldMismatchType : (Compatible xt yt -> Void)
                   -> Compatible ((xl, xt) :: xs) ((xl, yt) :: ys)
                   -> Void
  fieldMismatchType contra (Cons Refl prf rest) = contra prf

  restNotCompatible : (Compatible xs ys -> Void)
                   -> Compatible ((xl, xt) :: xs) ((xl, yt) :: ys)
                   -> Void
  restNotCompatible contra (Cons Refl prf rest) = contra rest

  fieldsLeftIsLarger : Compatible (x :: xs) [] -> Void
  fieldsLeftIsLarger _ impossible

  fieldsRightIsLarger : Compatible [] (y :: ys) -> Void
  fieldsRightIsLarger _ impossible

  export
  compatible : (kxs : Vect n (Pair String (Ty DATA)))
            -> (kys : Vect m (Pair String (Ty DATA)))
                        -> DecInfo Compatibility.Data.Error
                                   (Fields.Compatible kxs kys)

  compatible {n} xs {m} ys with (shape xs ys)
    compatible {n = 0} [] {m = 0} [] | Empty = Yes Empty

    compatible {n = (S len)} (x :: xs) {m = 0} [] | LH = No MismatchStructureLength fieldsLeftIsLarger
    compatible {n = 0} [] {m = (S len)} (y :: ys) | RH = No MismatchStructureLength fieldsRightIsLarger

    compatible {n = (S len)} ((xl, xt) :: xs) {m = (S len)} ((yl, yt) :: ys) | Both with (decEq xl yl)
      compatible {n = (S len)} ((xl, xt) :: xs) {m = (S len)} ((xl, yt) :: ys) | Both | (Yes Refl) with (compatible xt yt)
        compatible {n = (S len)} ((xl, xt) :: xs) {m = (S len)} ((xl, yt) :: ys) | Both | (Yes Refl) | (Yes prf) with (compatible xs ys)
          compatible {n = (S len)} ((xl, xt) :: xs) {m = (S len)} ((xl, yt) :: ys) | Both | (Yes Refl) | (Yes prf) | (Yes rest)
            = Yes (Cons Refl prf rest)
            -- End of happy path

          -- Rest not happy somewhere, and need to update position when it is recorded.
          compatible {n = (S len)} ((xl, xt) :: xs) {m = (S len)} ((xl, yt) :: ys) | Both | (Yes Refl) | (Yes prf) | (No (MismatchStructureFieldType position error) contra)
            = No (MismatchStructureFieldType (S position) error) (restNotCompatible contra)
          compatible {n = (S len)} ((xl, xt) :: xs) {m = (S len)} ((xl, yt) :: ys) | Both | (Yes Refl) | (Yes prf) | (No (MismatchStructureFieldLabel position x y) contra)
            = No (MismatchStructureFieldLabel (S position) x y) (restNotCompatible contra)
          compatible {n = (S len)} ((xl, xt) :: xs) {m = (S len)} ((xl, yt) :: ys) | Both | (Yes Refl) | (Yes prf) | (No msg contra)
            = No msg (restNotCompatible contra)

        -- Type mismatch
        compatible {n = (S len)} ((xl, xt) :: xs) {m = (S len)} ((xl, yt) :: ys) | Both | (Yes Refl) | (No msg contra)
          = No (MismatchStructureFieldType Z msg) (fieldMismatchType contra)
      -- Label mismatch
      compatible {n = (S len)} ((xl, xt) :: xs) {m = (S len)} ((yl, yt) :: ys) | Both | (No contra)
        = No (MismatchStructureFieldLabel Z xl yl) (fieldMismatchLabel contra)

-- [ Definition Starts Here]

-- [ Logic vs X ]

compatible TyLogic TyLogic = Yes CompatLogic
compatible TyLogic (TyArray l t) = No Mismatch logicNotCompatWithArray
compatible TyLogic (TyStruct kvs) = No Mismatch logicNotCompatWithStruct
compatible TyLogic (TyUnion kvs) = No Mismatch logicNotCompatWithUnion

-- [ Array vs X ]

compatible (TyArray type length) TyLogic = No Mismatch (negFlip logicNotCompatWithArray)

compatible (TyArray typeA lengthA) (TyArray typeB lengthB) with (decEq lengthA lengthB)
  compatible (TyArray typeA lengthA) (TyArray typeB lengthA) | Yes Refl with (compatible typeA typeB)
    compatible (TyArray typeA lengthA) (TyArray typeB lengthA) | Yes Refl | Yes prf
      = Yes (CompatArray Refl prf)

    compatible (TyArray typeA lengthA) (TyArray typeB lengthA) | Yes Refl | No msg contra
      = No (MismatchArrayType msg) (arraysNotSameType contra)
  compatible (TyArray typeA lengthA) (TyArray typeB lengthB) | No contra
    = No MismatchArrayLength (arraysNotSameLength contra)

compatible (TyArray type length) (TyStruct kvs) = No Mismatch arrayNotCompatWithStruct
compatible (TyArray type length) (TyUnion kvs) = No Mismatch arrayNotCompatWithUnion

-- [ Struct vs X ]

compatible (TyStruct kvs) TyLogic
  = No Mismatch (negFlip logicNotCompatWithStruct)

compatible (TyStruct kvs) (TyArray type length)
  = No Mismatch (negFlip arrayNotCompatWithStruct)

compatible (TyStruct xs) (TyStruct ys) with (Fields.compatible xs ys)
  compatible (TyStruct xs) (TyStruct ys) | (Yes prf) = Yes (CompatStruct prf)
  compatible (TyStruct xs) (TyStruct ys) | (No msg contra) = No msg (structsAreNotCompat contra)

compatible (TyStruct kvs) (TyUnion xs) = No Mismatch structNotCompatWithUnion

-- [ Union vs X ]

compatible (TyUnion kvs) TyLogic = No Mismatch (negFlip logicNotCompatWithUnion)

compatible (TyUnion kvs) (TyArray type length) = No Mismatch (negFlip arrayNotCompatWithUnion)

compatible (TyUnion xs) (TyStruct ys) = No Mismatch (negFlip structNotCompatWithUnion)

compatible (TyUnion xs) (TyUnion ys) with (Fields.compatible xs ys)
  compatible (TyUnion xs) (TyUnion ys) | (Yes prf) = Yes (CompatUnion prf)
  compatible (TyUnion xs) (TyUnion ys) | (No msg contra) = No msg (unionsAreNotCompat contra)

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Main

import System

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
    then pure (Just (cast input))
    else pure Nothing

guess : (target : Nat) -> (guesses : Nat) -> IO ()
guess target guesses =
    do
        putStr ("Number (attempt #" ++ (show guesses) ++ "): ")
        Just num <- readNumber
            | Nothing =>
                do
                    putStrLn "Invalid input"
                    guess target guesses

        case compare num target of
            LT =>
                do
                    putStrLn "Too low"
                    guess target (S guesses)
            EQ => putStrLn "Correct!"
            GT =>
                do
                    putStrLn "Too high!"
                    guess target (S guesses)

main : IO ()
main =
    do
        randomVal <- time
        let target = randomVal - 1529902000
        guess (cast target) 0


text:
module Main

import Data.Fuel
import Data.Vect
import State
import Editor
import Document
import Cursor
import Terminal
import EditorMode

%default total

error : String -> IO ()
error = putStrLn

--todo: check if this is still needed
makeSt : String -> (n : Nat ** Vect n String) -> State
makeSt fn ((S _) ** lines) = initState $ MkDocument lines (MkCursor Z FZ) fn
makeSt fn (Z ** lines) = initState $ MkDocument [""] (MkCursor Z FZ) fn

makeState : String -> String -> State
makeState fileName content =
  let lines = (_ ** fromList $ lines content)
   in makeSt fileName lines

partial
main : IO ()
main = do
  arguments <- getArgs
  let (Just fileName) = index' 1 arguments | error "usage: p <filename>"
  Right fileContent <- readFile fileName | error ("unable to open file: " ++ fileName)
  setRaw
  run forever $ normalEditor $ makeState fileName fileContent

max_stars_repo_name: PeterHajdu/peti

max_issues_repo_name: PeterHajdu/peti

max_forks_repo_name: PeterHajdu/peti


text:
module Group_property3

import congruence
import Monoid
import Group
import Group_property
import Group_property2

%access public export
%default total

||| Property 9 - If a*b = c then b = Inv(a) * c
total
Group_property_9 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a, b, c : grp) -> (a*b = c) -> (b = (Inv grp (*) pfgrp a)*c)

Group_property_9 grp (*) pfgrp a b c pfEq = let
    a_inv = fst(Inv_with_pf grp (*) pfgrp a)
    pf_inv = snd(Inv_with_pf grp (*) pfgrp a)

    pf1 = Group_property_3 grp (*) pfgrp a_inv (a*b) c pfEq -- a_inv * (a * b) = a_inv * c
    pfAss = fst pfgrp -- proof of associativity
    pf2 = pfAss a_inv a b -- a_inv * (a * b) = (a_inv * a) * b

    pf3 = snd pf_inv -- a_inv * a = e2

    pfid1 = (fst (snd pfgrp))
    e1 = (fst pfid1) -- identity in the IdentityExists
    e1_pf = (snd pfid1) -- proof that e_dom1 is the identity

    pfid2 = (fst (snd (snd pfgrp)))
    e2 = (fst pfid2) -- identity in the InverseExists
    e2_pf = (snd pfid2) -- prood that it is the identity

    pf_eq_e12 = (Group_property_1 grp (*) pfgrp e1 e2 e1_pf e2_pf) -- e1 = e2

    pf4 = trans pf3 (sym pf_eq_e12) -- a_inv * a = e1
    pf5 = Group_property_5 grp (*) pfgrp b (a_inv * a) e1 pf4 -- (a_inv * a) * b = e1 * b
    pf6 = e1_pf b
    pf7 = fst pf6 -- b * e1 = b
    pf8 = snd pf6 -- e1 * b = b
    pf9 = trans pf5 pf8 -- a_inv * a * b = b
    pf10 = trans (sym pf2) pf9 -- a_inv * (a * b) = b
    pf11 = trans (sym pf1) pf10 -- a_inv * c = b
    in
    (sym pf11)


text:
module Main

import Erlang

%cg erlang export exports

printSum : Integer -> Integer -> IO Integer
printSum x y = do
  let result = x + y
  putStrLn ("Sum: " ++ show result)
  pure result

exports : ErlExport
exports =
  Fun "foo" 42
    <+> Fun "print_sum" (MkIOFun2 printSum)


text:
import Data.Fin

%default total

data ZeroOneOmega = Zero | One | Omega

Num ZeroOneOmega where
  Zero + a = a
  a + Zero = a
  One + a = Omega
  a + One = Omega
  Omega + Omega = Omega

  Zero * _ = Zero
  _ * Zero = Zero
  One * a = a
  a * One = a
  Omega * Omega = Omega

  fromInteger 0 = Zero
  fromInteger 1 = One
  fromInteger _ = Omega

test1 : ZeroOneOmega
test1 = 0

test2 : ZeroOneOmega
test2 = 1

test3 : ZeroOneOmega
test3 = 8


text:
-- This code is a copy of gist:
-- https://gist.github.com/david-christiansen/3660d5d45e9287c25a5e

module FizzBuzzC

%default total

-- Dependently typed FizzBuzz, constructively

-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
  ZeroFizzy : Fizzy 0
  Fizz : Fizzy n -> Fizzy (3 + n)

-- Fizzy is a correct specification of divisibility by 3 - that is, if n is
-- fizzy then there exists some k such that n = 3*k.
fizzyCorrect : (n : Nat) -> Fizzy n -> (k : Nat ** n = 3 * k)
fizzyCorrect Z ZeroFizzy = (Z ** Refl)
fizzyCorrect (S (S (S k))) (Fizz x) =
  let (k' ** ih) = fizzyCorrect k x
  in (S k' ** ?fizzyIsAOK)

-- Basic fizziness lemmas
oneNotFizzy : Not (Fizzy 1)
oneNotFizzy (Fizz f) impossible

twoNotFizzy : Not (Fizzy 2)
twoNotFizzy (Fizz f) impossible

fizzyUp : Not (Fizzy n) -> Not (Fizzy (3 + n))
fizzyUp nope ZeroFizzy impossible
fizzyUp nope (Fizz f) = nope f

-- Fizziness is decidable
decFizzy : (n : Nat) -> Dec (Fizzy n)
decFizzy Z = Yes ZeroFizzy
decFizzy (S Z) = No oneNotFizzy
decFizzy (S (S Z)) = No twoNotFizzy
decFizzy (S (S (S k))) with (decFizzy k)
  decFizzy (S (S (S k))) | (Yes prf) = Yes (Fizz prf)
  decFizzy (S (S (S k))) | (No contra) = No $ fizzyUp contra

-- A number is buzzy if it is evenly divisible by 5
data Buzzy : Nat -> Type where
  ZeroBuzzy : Buzzy 0
  Buzz : Buzzy n -> Buzzy (5 + n)

-- Correctness of buzziness spec elided due to verbosity

oneNotBuzzy : Not (Buzzy 1)
oneNotBuzzy (Buzz b) impossible

twoNotBuzzy : Not (Buzzy 2)
twoNotBuzzy (Buzz b) impossible

threeNotBuzzy : Not (Buzzy 3)
threeNotBuzzy (Buzz b) impossible

fourNotBuzzy : Not (Buzzy 4)
fourNotBuzzy (Buzz b) impossible

buzzOff : Not (Buzzy n) -> Not (Buzzy (5 + n))
buzzOff nope ZeroBuzzy impossible
buzzOff nope (Buzz b) = nope b

decBuzzy : (n : Nat) -> Dec (Buzzy n)
decBuzzy Z = Yes ZeroBuzzy
decBuzzy (S Z) = No oneNotBuzzy
decBuzzy (S (S Z)) = No twoNotBuzzy
decBuzzy (S (S (S Z))) = No threeNotBuzzy
decBuzzy (S (S (S (S Z)))) = No fourNotBuzzy
decBuzzy (S (S (S (S (S k))))) with (decBuzzy k)
  decBuzzy (S (S (S (S (S k))))) | (Yes prf) = Yes (Buzz prf)
  decBuzzy (S (S (S (S (S k))))) | (No way) = No (buzzOff way)

-- A version of Dec that tracks two properties - DoubleDec A B is isomorphic
-- to (Dec A, Dec B). This is just for readability.
data DoubleDec : Type -> Type -> Type where
  Neither : Not a -> Not b -> DoubleDec a b
  First : a -> Not b -> DoubleDec a b
  Second : Not a -> b -> DoubleDec a b
  Both : a -> b -> DoubleDec a b

decFizzBuzz : (n : Nat) -> DoubleDec (Fizzy n) (Buzzy n)
decFizzBuzz n with (decFizzy n, decBuzzy n)
  decFizzBuzz n | (Yes f, Yes b) = Both f b
  decFizzBuzz n | (No nf, Yes b) = Second nf b
  decFizzBuzz n | (Yes f, No nb) = First f nb
  decFizzBuzz n | (No nf, No nb) = Neither nf nb

-- Let's show some fizzing and buzzing. Start with all the nats:
nats : Stream Nat
nats = iterate S Z

-- and the fizzed and buzzed nats
fizzBuzz : Stream (n : Nat ** DoubleDec (Fizzy n) (Buzzy n))
fizzBuzz = map (\n => (n ** (decFizzBuzz n))) (tail nats)

instance Show (n : Nat ** DoubleDec (Fizzy n) (Buzzy n)) where
  show (x ** Neither _ _) = show x
  show (x ** First _ _)   = "Fizz"
  show (x ** Second _ _)  = "Buzz"
  show (x ** Both _ _)    = "FizzBuzz"

-- Take the first 100 numbers' FizzBuzzes, then print them to the screen.
namespace Main
  main : IO ()
  main = sequence_ . map (putStrLn . show) . take 100 $ fizzBuzz

---------- Proofs ----------

FizzBuzzC.fizzyIsAOK = proof
  compute
  intros
  rewrite plusSuccRightSucc k' (plus k' 0)
  rewrite plusSuccRightSucc k' (S (plus k' (plus k' 0)))
  rewrite plusSuccRightSucc k' (plus k' (plus k' 0))
  rewrite ih
  trivial


text:
module Main

import SimpleRealizedFunction

-- Realized incrementer
incrementer : Int -> Int
incrementer = (+1)
rlz_incrementer : SimpleRealizedFunction (Int -> Int) 100 1.0
rlz_incrementer = MkSimpleRealizedFunction incrementer

-- Realized twicer
twicer : Int -> Int
twicer = (*2)
rlz_twicer : SimpleRealizedFunction (Int -> Int) 500 0.9
rlz_twicer = MkSimpleRealizedFunction twicer

-- Realized (twicer . incrementer).
rlz_composition : SimpleRealizedFunction (Int -> Int) 600 0.9
-- The following does not work because 601 ≠ 100+500 and 1.0 ≠ (min 1.0 0.9)
-- rlz_composition : SimpleRealizedFunction (Int -> Int) 601 1.0
rlz_composition = compose rlz_twicer rlz_incrementer

-- Simple test, result should be (3+1)*2 = 8
rslt : Int
rslt = apply rlz_composition 3

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 App.User
{-
import Common
Name : Type
Name = String

mutual
  data User : Type where
    U1 : UserId -> Name -> User

  UserId : Type
  UserId = Id User String

-}


text:
module Oyster.Helper

import Data.Strings

%default total

export
listCharToString : List Char -> String
listCharToString [] = ""
listCharToString (c :: cs) = strCons c (listCharToString cs)

export
natToInt : Nat -> Int
natToInt Z = 0
natToInt (S k) = 1 + natToInt k

max_stars_repo_name: timmyjose-compilers/oyster

max_issues_repo_name: timmyjose-compilers/oyster

max_forks_repo_name: timmyjose-compilers/oyster


text:
module Rnd

import Effects

data Random : Effect where
     getRandom : Random Int Int (\v => Int)

using (m : Type -> Type)
  instance Handler Random m where
     handle seed getRandom k
              = let seed' = (1664525 * seed + 1013904223) `prim__sremInt` (pow 2 32) in
                    k seed' seed'

RND : EFFECT
RND = MkEff Int Random

rndInt : Int -> Int -> { [RND] } Eff m Int
rndInt lower upper = do v <- getRandom
                        return (abs (v `prim__sremInt` (upper - lower)) + lower)

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module Network.TLS.Handle

import Control.Linear.LIO
import Control.Monad.Error.Either
import Control.Monad.State
import Crypto.ECDH
import Crypto.Random
import Data.List
import Data.List1
import Data.Vect
import Data.Void
import Network.TLS.Core
import Network.TLS.Magic
import Network.TLS.Parsing
import Network.TLS.Record
import Utils.Bytes
import Utils.Handle
import Utils.Misc
import Utils.Parser

public export
tls_version_to_state_type : TLSVersion -> Type
tls_version_to_state_type TLS12 = TLSState Application2
tls_version_to_state_type TLS13 = TLSState Application3
tls_version_to_state_type _ = Void

export
record TLSHandle (version : TLSVersion) t_ok t_closed where
  constructor MkTLSHandle
  1 handle : Handle t_ok t_closed (Res String $ const t_closed) (Res String $ const t_closed)
  state : tls_version_to_state_type version
  buffer : List Bits8

public export
Uninhabited (TLSHandle TLS10 t_ok t_closed) where
  uninhabited = state

public export
Uninhabited (TLSHandle TLS11 t_ok t_closed) where
  uninhabited = state

OkOrError : TLSVersion -> Type -> Type -> Type
OkOrError tls_version t_ok t_closed = Res Bool $ \ok => if ok then TLSHandle tls_version t_ok t_closed else Res String (const t_closed)

read_record : LinearIO m => (1 _ : Handle' t_ok t_closed) -> L1 m $ Res Bool $ \ok => if ok then Res (List Bits8) (const $ Handle' t_ok t_closed) else Res String (const t_closed)
read_record handle = do
  -- read header
  (True # (b_header # handle)) <- read handle 5
  | (False # (error # handle)) => pure1 (False # ("read (record header / alert) failed: " <+> error # handle))
  let (Pure [] (Right (_, TLS12, len))) =
    feed {i = List (Posed Bits8)} (map (uncurry MkPosed) $ enumerate 0 b_header) (alert <|> record_type_with_version_with_length).decode
  | Pure [] (Left x) => (close handle) >>= (\s => pure1 (False # (("ALERT: " <+> show x) # s)))
  | _ => (close handle) >>= (\s => pure1 (False # (("unable to parse header: " <+> xxd b_header) # s)))

  -- read record content
  (True # (b_body # handle)) <- read handle (cast len)
  | (False # (error # handle)) => pure1 (False # ("read (record body) failed: " <+> error # handle))
  if length b_body == cast len
    then pure1 (True # (b_header <+> b_body # handle))
    else let err = "length does not match header: " <+> xxd b_body
               <+> "\nexpected length: " <+> show len
               <+> "\nactual length: " <+> (show $ length b_body)
         in (close handle) >>= (\s => pure1 (False # (err # s)))

gen_key : MonadRandom m => (g : SupportedGroup) -> m (DPair SupportedGroup (\g => Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g)))
gen_key group = do
  keypair <- generate_key_pair @{snd $ curve_group_to_type group}
  pure (group ** keypair)

tls2_handshake : LinearIO io => TLSState ServerHello2 -> (1 _ : Handle' t_ok t_closed) -> CertificateCheck IO -> L1 io (OkOrError TLS12 t_ok t_closed)
tls2_handshake state handle cert_ok = do
  (True # (b_cert # handle)) <- read_record handle
  | (False # other) => pure1 (False # other)

  let Right state = serverhello2_to_servercert state b_cert
  | Left error => (close handle) >>= (\s => pure1 (False # (error # s)))

  (True # (b_skex # handle)) <- read_record handle
  | (False # other) => pure1 (False # other)

  Right state <- liftIO1 $ servercert_to_serverkex state b_skex cert_ok
  | Left error => (close handle) >>= (\s => pure1 (False # (error # s)))

  (True # (b_s_hello_done # handle)) <- read_record handle
  | (False # other) => pure1 (False # other)

  let Right (state, handshake_data) = serverkex_process_serverhellodone state b_s_hello_done
  | Left error => (close handle) >>= (\s => pure1 (False # (error # s)))

  (True # handle) <- write handle handshake_data
  | (False # (error # handle)) => pure1 (False # ("send_byte (handshake data) failed: " <+> error # handle))

  (True # (b_ccs # handle)) <- read_record handle
  | (False # other) => pure1 (False # other)

  let Right state = serverhellodone_to_applicationready2 state b_ccs
  | Left error => (close handle) >>= (\s => pure1 (False # (error # s)))

  (True # (b_fin # handle)) <- read_record handle
  | (False # other) => pure1 (False # other)

  case applicationready2_to_application2 state b_fin of
    Right state => pure1 (True # MkTLSHandle handle state [])
    Left error => (close handle) >>= (\s => pure1 (False # (error # s)))

tls3_handshake : LinearIO io => TLSState ServerHello3 -> (1 _ : Handle' t_ok t_closed) -> CertificateCheck IO -> L1 io (OkOrError TLS13 t_ok t_closed)
tls3_handshake state handle cert_ok = do
  (True # (b_response # handle)) <- read_record handle
  | (False # other) => pure1 (False # other)
  parsed <- liftIO1 $ tls3_serverhello_to_application state b_response cert_ok
  case parsed of
    Right (Right (client_verify, state)) => do
      (True # handle) <- write handle client_verify
      | (False # (error # handle)) => pure1 (False # ("send_byte (client verify data) failed: " <+> error # handle))
      pure1 (True # MkTLSHandle handle state [])
    Right (Left state) =>
      tls3_handshake state handle cert_ok
    Left error =>
      (close handle) >>= (\s => pure1 (False # (error # s)))

DecryptFunction : Type -> Type
DecryptFunction state = state -> List Bits8 -> Either String (state, List Bits8)

EncryptFunction : Type -> Type
EncryptFunction state = state -> List Bits8 -> (state, List Bits8)

tlshandle_read : {version : _} -> LinearIO io => (wanted : Nat) -> (1 _ : TLSHandle version t_ok t_closed) -> DecryptFunction (tls_version_to_state_type version) -> L1 io (Res Bool $ ReadHack (TLSHandle version t_ok t_closed) (Res String (const t_closed)))
tlshandle_read wanted (MkTLSHandle handle state buffer) decrypt =
  let (a, b) = splitAt wanted buffer
  in if (length a) == wanted
        then pure1 (True # (a # MkTLSHandle handle state b))
        else do
          (True # (b_record # handle)) <- read_record handle
          | (False # other) => pure1 (False # other)
          case decrypt state b_record of
            Right (state, plaintext) => tlshandle_read wanted (MkTLSHandle handle state $ buffer <+> plaintext) decrypt
            Left error => (close handle) >>= (\s => pure1 (False # (error # s)))

tlshandle_write : {tls_version : TLSVersion} -> LinearIO io => List (List Bits8) -> (1 _ : TLSHandle tls_version t_ok t_closed) -> EncryptFunction (tls_version_to_state_type tls_version) -> L1 io (Res Bool $ WriteHack (TLSHandle tls_version t_ok t_closed) (Res String (const t_closed)))
tlshandle_write [] sock encrypt = pure1 (True # sock)
tlshandle_write (x :: xs) (MkTLSHandle handle state buffer) encrypt = do
  let (state, b_record) = encrypt state x
  (True # handle) <- write handle b_record
  | (False # (error # handle)) => pure1 (False # ("write (application data) failed: " <+> error # handle))
  tlshandle_write xs (MkTLSHandle handle state buffer) encrypt

||| Reference: OpenSSL
chunk_size : Nat
chunk_size = 0x2000

tlshandle_to_handle : {version : _} -> (1 _ : TLSHandle version t_ok t_closed) -> Handle' (TLSHandle version t_ok t_closed) t_closed
tlshandle_to_handle {version=TLS10} (MkTLSHandle handle state buffer) = (kill_linear state) handle
tlshandle_to_handle {version=TLS11} (MkTLSHandle handle state buffer) = (kill_linear state) handle
tlshandle_to_handle {version=TLS12} handle = MkHandle
  handle
  ( \sock, len => tlshandle_read len sock decrypt_from_record2 )
  ( \sock, input => tlshandle_write (chunk chunk_size input) sock encrypt_to_record2 )
  ( \(MkTLSHandle handle state buffer) => close handle )
tlshandle_to_handle {version=TLS13} handle = MkHandle
  handle
  ( \sock, len => tlshandle_read len sock decrypt_from_record )
  ( \sock, input => tlshandle_write (chunk chunk_size input) sock encrypt_to_record )
  ( \(MkTLSHandle handle state buffer) => close handle )

TLSHandle' : Type -> Type -> Type
TLSHandle' t_ok t_closed = Res TLSVersion $ \version => TLSHandle version t_ok t_closed

abstract_tlshandle : (1 _ : TLSHandle' t_ok t_closed) -> Handle' (TLSHandle' t_ok t_closed) t_closed
abstract_tlshandle x = MkHandle
  x
  ( \(v # h), wanted => do
      (True # (output # MkHandle h _ _ _)) <- read (tlshandle_to_handle h) wanted
      | (False # (err # x)) => pure1 $ False # (err # x)
      pure1 $ True # (output # (_ # h))
  )
  ( \(v # h), input => do
      (True # MkHandle h _ _ _) <- write (tlshandle_to_handle h) input
      | (False # (err # x)) => pure1 $ False # (err # x)
      pure1 $ True # (_ # h)
  )
  ( \(v # h) => close $ tlshandle_to_handle h
  )

export
tls_handshake : (MonadRandom IO, LinearIO io) =>
                String ->
                List1 SupportedGroup ->
                List1 SignatureAlgorithm ->
                List1 CipherSuite ->
                (1 _ : Handle' t_ok t_closed) ->
                CertificateCheck IO ->
                L1 io (Res Bool $ \ok => if ok then Handle' (TLSHandle' t_ok t_closed) t_closed else Res String (const t_closed))
tls_handshake target_hostname supported_groups signature_algos cipher_suites handle cert_ok = do
  random <- liftIO1 $ random_bytes _
  keypairs <- liftIO1 $ traverse gen_key supported_groups
  let
    (client_hello, state) =
      tls_init_to_clienthello $ TLS_Init $ MkTLSInitialState
        target_hostname
        random
        []
        cipher_suites
        signature_algos
        keypairs

  (True # handle) <- write handle client_hello
  | (False # (error # handle)) => pure1 (False # ("send client_hello failed: " <+> error # handle))

  (True # (b_server_hello # handle)) <- read_record handle
  | (False # other) => pure1 (False # other)

  case tls_clienthello_to_serverhello state b_server_hello of
    Right (Left state) => do
      (True # ok) <- tls2_handshake state handle cert_ok
      | (False # no) => pure1 (False # no)
      pure1 $ True # abstract_tlshandle (_ # ok)
    Right (Right state) => do
      (True # ok) <- tls3_handshake state handle cert_ok
      | (False # no) => pure1 (False # no)
      pure1 $ True # abstract_tlshandle (_ # ok)
    Left error => do
      h <- close handle
      pure1 $ False # (error # h)


text:
module Erlang.System.File

import Data.List
import Data.Strings
import Erlang

%default total

public export
data Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend

public export
data FileError
  = GenericFileError Int -- errno
  | FileReadError
  | FileWriteError
  | FileNotFound
  | PermissionDenied
  | FileExists

export
Show FileError where
  show (GenericFileError errno) = "File error: " ++ show errno
  show FileReadError = "File Read Error"
  show FileWriteError = "File Write Error"
  show FileNotFound = "File Not Found"
  show PermissionDenied = "Permission Denied"
  show FileExists = "File Exists"

export
unknownError : FileError
unknownError = GenericFileError 0

export
reason : ErlDecoder FileError
reason =
  (exact (MkAtom "enoent") *> pure FileNotFound)
    <|> (exact (MkAtom "eacces") *> pure PermissionDenied)
    <|> (exact (MkAtom "eexist") *> pure FileExists)
    <|> pure unknownError

export
error : ErlDecoder FileError
error =
  errorTuple reason

export
data File : Type where
  FHandle : ErlTerm -> File

export
stdin : File
stdin = FHandle (cast (MkAtom "standard_io"))

export
stdout : File
stdout = FHandle (cast (MkAtom "standard_io"))

export
stderr : File
stderr = FHandle (cast (MkAtom "standard_error"))

-- TODO: Match on all cases of Mode?
fileModes : Mode -> ErlTerm
fileModes mode =
  let flags = case mode of
        Read          => [MkAtom "read"]
        WriteTruncate => [MkAtom "write"]
        Append        => [MkAtom "append"]
        ReadWrite     => [MkAtom "read", MkAtom "write"]
        _ => []
  in cast $ the (List ErlAtom) (MkAtom "binary" :: flags)

export
openFile : HasIO io => (filePath : String) -> Mode -> io (Either FileError File)
openFile filePath mode = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "open" [filePath, fileModes mode]
  pure $ erlDecodeDef (Left unknownError)
    (map (\pid => Right (FHandle (cast pid))) (okTuple pid)
      <|> map Left error)
    result

export
closeFile : HasIO io => File -> io ()
closeFile (FHandle f) = do
  pure $ erlUnsafeCall ErlTerm "file" "close" [f]
  pure ()

export
fGetLine : HasIO io => File -> io (Either FileError String)
fGetLine (FHandle f) = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "read_line" [f]
  pure $ erlDecodeDef (Left unknownError)
    (map Right (okTuple string)
      <|> exact (MkAtom "eof") *> pure (Right "")
      <|> map Left error)
    result

export
fGetChar : HasIO io => File -> io (Either FileError Char)
fGetChar (FHandle f) = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "read" [f, 1]
  pure $ erlDecodeDef (Left unknownError)
    (map (\(MkCharlist str) => maybe (Left FileReadError) (Right . fst) (strUncons str)) (okTuple charlist)
      <|> exact (MkAtom "eof") *> pure (Left FileReadError)
      <|> map Left error)
    result

export
fPutStr : HasIO io => File -> String -> io (Either FileError ())
fPutStr (FHandle f) str = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "write" [f, str]
  pure $ erlDecodeDef (Left unknownError)
    (exact (MkAtom "ok") *> pure (Right ())
      <|> map Left error)
    result

export
fPutStrLn : HasIO io => File -> String -> io (Either FileError ())
fPutStrLn f str = fPutStr f (str ++ "\n")

export
fEOF : HasIO io => File -> io Bool
fEOF (FHandle f) = do
  readResult <- pure $ erlUnsafeCall ErlTerm "file" "read" [f, 1]
  erlDecodeDef (pure True)
    (okTuple any *> pure scanBack <|>
      exact (MkAtom "eof") *> pure (pure True) <|>
      errorTuple any *> pure (pure True))
    readResult
  where
    -- If `file:read/2` returns `{ok, _}` we need to scan back to the original position
    scanBack : io Bool
    scanBack = do
      scanResult <- pure $ erlUnsafeCall ErlTerm "file" "position" [f, MkTuple2 (MkAtom "cur") (-1)]
      pure $ erlDecodeDef True
        (okTuple any *> pure False <|>
          errorTuple any *> pure True)
        scanResult

export
readFile : HasIO io => String -> io (Either FileError String)
readFile file = do
  readResult <- pure $ erlUnsafeCall ErlTerm "file" "read_file" [file]
  pure $ erlDecodeDef (Left FileReadError)
    (Right <$> okTuple string <|>
      Left <$> error)
    readResult

export
writeFile : HasIO io => (filepath : String) -> (contents : String) -> io (Either FileError ())
writeFile filePath contents = do
  Right h <- openFile filePath WriteTruncate
    | Left err => pure (Left err)
  Right () <- fPutStr h contents
    | Left err => do
      closeFile h
      pure (Left err)
  closeFile h
  pure (Right ())

-- TODO: Is this necessary? Currently a no-op.
export
fflush : HasIO io => File -> io ()
fflush (FHandle f) = do
  pure ()

fileInfo : HasIO io => (filePath : String) -> (fieldIndex : Nat) -> ErlDecoder a -> io (Either FileError a)
fileInfo filePath fieldIndex decoder = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "read_file_info" [filePath, the (ErlList _) [MkTuple2 (MkAtom "time") (MkAtom "posix")]]
  let Right info = erlDecodeDef
        (Left unknownError)
        (map Right (okTuple any)
          <|> map Left error)
        result
        | Left err => pure (Left err)
  -- Returns an exception if index does not exist
  Right fieldValue <- erlCall "erlang" "element" [cast fieldIndex + 2, info]
    | Left _ => pure (Left unknownError)
  pure $ erlDecodeDef
    (Left unknownError)
    (map Right decoder)
    fieldValue

export
fileSize : HasIO io => (filePath : String) -> io (Either FileError Int)
fileSize filePath =
   fileInfo filePath 0 (map cast integer)

export
fileAccessTime : HasIO io => (filePath : String) -> io (Either FileError Int)
fileAccessTime filePath =
  fileInfo filePath 3 (map cast integer)

export
fileModifiedTime : HasIO io => (filePath : String) -> io (Either FileError Int)
fileModifiedTime filePath =
  fileInfo filePath 4 (map cast integer)

export
fileStatusTime : HasIO io => (filePath : String) -> io (Either FileError Int)
fileStatusTime filePath =
  fileInfo filePath 5 (map cast integer)

export
removeFile : HasIO io => String -> io (Either FileError ())
removeFile filePath = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "delete" [filePath]
  pure $ erlDecodeDef
    (Left unknownError)
    ((exact (MkAtom "ok") *> pure (Right ()))
      <|> map Left error)
    result

-- TODO: Add `fPoll`? It is not used in the project.

namespace FileMode
  public export
  data FileMode = Read | Write | Execute

public export
record Permissions where
  constructor MkPermissions
  user   : List FileMode
  group  : List FileMode
  others : List FileMode

mkMode : Permissions -> Int
mkMode p =
  getMs (user p) * 64 + getMs (group p) * 8 + getMs (others p)
  where
    getM : FileMode -> Int
    getM Read = 4
    getM Write = 2
    getM Execute = 1

    getMs : List FileMode -> Int
    getMs = sum . map getM

export
chmodRaw : HasIO io => (filePath : String) -> Int -> io (Either FileError ())
chmodRaw filePath p = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "change_mode" [filePath, p]
  pure $ erlDecodeDef
    (Left unknownError)
    ((exact (MkAtom "ok") *> pure (Right ()))
      <|> map Left error)
    result

export
chmod : HasIO io => String -> Permissions -> io (Either FileError ())
chmod fname p = chmodRaw fname (mkMode p)


text:
{-
%builtins output pedersen

from starkware.cairo.common.cairo_builtins import HashBuiltin
from starkware.cairo.common.hash import hash2
from starkware.cairo.common.serialize import serialize_word

func main{output_ptr : felt*, pedersen_ptr : HashBuiltin*}():
    let (res) = hash2{hash_ptr=pedersen_ptr}(1,2)
    serialize_word(res + 1)
    return ()
end
-}

module Main

import Cairo

%noinline
main : Cairo ()
main =
    output (1 + (pedersenHash 1 2))

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
-- --------------------------------------------------------------- [ Utils.idr ]
-- Module    : Utils.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Things that should be in Lightyear but are Not.
module Sif.DSL.Parser.Utils

import Lightyear
import Lightyear.Char
import Lightyear.Strings

import Test.Parsing

%default partial
%access private

line : String -> Parser ()
line l = do
    token l <* spaces
    manyTill anyChar endOfLine
    spaces
    pure ()
  <?> "Line comment"

block : String -> String -> Parser ()
block b e = do
    token b <* spaces
    manyTill anyChar (token e)
    spaces
    pure ()
  <?> "Block Comment"

export
comment : String -> String -> String -> Parser ()
comment l b e = (line l)
            <|> (block b e)
            <|> spaces
            <?> "Comment"

nonEmptyDocString : String -> Parser String
nonEmptyDocString m = do
    token m <* spaces
    d <- manyTill anyChar endOfLine
    spaces
    pure $ pack d
  <?> "Text Doc String"

emptyDocString : String -> Parser String
emptyDocString m = do
    string m
    endOfLine
    pure "\n\n"
  <?> "Empty Doc String"

docString : String -> Parser String
docString m = emptyDocString m <|> nonEmptyDocString m

export
doc : String -> Parser String
doc m = do
      ds <- some $ (docString m <* spaces)
      spaces
      pure $ unwords ds
    <?> "Documentation"

export
runTests : IO ()
runTests = do
  putStrLn $ heading "Parsing Utility Tests"
  canParse (Just "Line")    (line "--")       "-- I am a comment\n"
  canParse (Just "Block")   (block "{-" "-}") "{- -- I am a comment -}"
  canParse (Just "Docs")    (doc ">") """> I am doc
> I am doc
> Doc
>
"""
  canParse (Just "Comment") (comment "--" "{-" "-}") """{-
A comment
-}"""

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Client.Action.Check

import Client.Action.Build
import Inigo.Async.Base
import Inigo.Async.Promise
import Inigo.Package.Package
import Inigo.Paths

export
check : Promise ()
check =
  do
    ignore writeIPkgFile
    ignore $ system "idris2" ["--typecheck", inigoIPkgPath] Nothing False False

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import OCaml.IO

front_legss : List (Int, Int)
front_legss = [
        (256, 246), (249, 287), (251, 343), (264, 346), (266, 306), (276, 276),
        (282, 306), (278, 343), (292, 343), (298, 306), (298, 277), (299, 254),
        (255, 246)
    ]

back_legss : List (Int, Int)
back_legss = [
         (432, 243), (441, 289), (430, 334), (445, 334), (462, 275), (469, 328),
         (476, 328), (478, 259), (454, 214), (461, 164), (407, 206)
    ]

set_color : Int -> OCaml_IO ()
set_color = ocamlCall "Graphics.set_color" (Int -> OCaml_IO ())

fe : Int -> Int -> Int -> Int -> Int -> OCaml_IO ()
fe y_max x y w h = let y = y_max - y in
    ocamlCall "Graphics.fill_ellipse" (Int -> Int -> Int -> Int -> OCaml_IO ())
     (x + (w `div` 2)) (y - (h `div` 2)) (w `div` 2) (h `div` 2)

fp : Int -> Ptr -> OCaml_IO ()
fp y_max ar = do
    f <- ocamlCall "Idrisobj.f" (Int -> OCaml_IO Ptr) y_max
    arr <- ocamlCall "Array.map"
        (Ptr -> Ptr -> OCaml_IO Ptr) f ar
    ocamlCall "Graphics.fill_poly" (Ptr -> OCaml_IO ()) arr

loop : () -> OCaml_IO ()
loop _ = do
    ocamlCall "Graphics.wait_next_event" (List Int -> OCaml_IO Ptr)
        [0,1,2,3,4]
    loop ()

main : OCaml_IO  ()
main = do
    ocamlCall "Graphics.open_graph" (String -> OCaml_IO ()) ""
    ocamlCall "Graphics.auto_synchronize" (Bool -> OCaml_IO ()) False
    ocamlCall "Graphics.clear_graph" (() -> OCaml_IO ()) ()
    ocamlCall "Graphics.synchronize" (() -> OCaml_IO ()) ()

    y_max <- ocamlCall "Graphics.size_y" (() -> OCaml_IO Int) ()

    orange <- ocamlCall "Graphics.rgb" (Int -> Int -> Int -> OCaml_IO Int)
        198 141 62
    white <- ocamlCall "Graphics.white" (OCaml_IO Int)
    black <- ocamlCall "Graphics.black" (OCaml_IO Int)

    back_legs <- ocamlCall "Idrisobj.back_legs" (OCaml_IO Ptr)
    front_legs <- ocamlCall "Idrisobj.front_legs" (OCaml_IO Ptr)

    set_color orange
    fe y_max 185 90 250 147
    fe y_max 269 54 68 98
    fe y_max 143 138 127 94

    set_color white
    fe y_max 89 (-79) 195 227

    set_color orange
    fe y_max 134 93 62 122
    fe y_max 97 101 86 47
    fe y_max 354 63 68 118
    fe y_max 367 101 98 109
    fe y_max 247 176 68 94

    fp y_max back_legs
    fp y_max front_legs

    ocamlCall "Graphics.moveto" (Int -> Int -> OCaml_IO ()) 200 40
    set_color black

    ocamlCall "Graphics.draw_string" (String -> OCaml_IO ())
        "Bactrian the Double-Humped OCaml"

    ocamlCall "Graphics.synchronize" (() -> OCaml_IO ()) ()
    loop ()

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
import Data.String

main : IO ()
main = do putStrLn $ fastPack ['a', 'b', 'c', 'π', 'Ω', '2']
          printLn $ fastUnpack "abcπΩ2"
          putStrLn $ fastConcat ["a", "b", "c", "πΩ", "2"]


text:
||| A version of `Dec` that returns a meaningful error message as well as proof of void.
|||
||| When dealing with decidable properties for type-level computations the existing `Dec` data type is useful.
||| However, when using decidable properties interactively one cannot easily tell why a property failed.
||| One can always encode failing cases within the property itself but that is not necessarily a advantageous.
|||
||| `DecInfo` provides a data structure to capture decidable properties together with an informative error message for when the property does not hold.
module Commons.Data.DecInfo

%default total
%access public export

data DecInfo : (errType : Type) -> (prop : Type) -> Type where
   Yes : (prfWhy : prop) -> DecInfo errType prop
   No  : (msgWhyNot : errType) -> (prfWhyNot : prop -> Void) -> DecInfo errType prop

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Data.Prim

import public Data.Prim.Char
import public Data.Prim.Bits8
import public Data.Prim.Bits16
import public Data.Prim.Bits32
import public Data.Prim.Bits64
import public Data.Prim.Int8
import public Data.Prim.Int16
import public Data.Prim.Int32
import public Data.Prim.Int64
import public Data.Prim.String


text:
module NanoParsec.Combinators

import NanoParsec.Parser
import Data.String

%access export

oneOf : List Char -> Parser Char
oneOf st = satisfy (flip elem st)

chainl1 : Parser a -> Parser (a -> a -> a) -> Parser a
chainl1 p op = do { a <- p; rest a }
    where
        rest a = (do f <- op
                     b <- p
                     rest (f a b))
                <|> return a

chainl : Parser a -> Parser (a -> a -> a) -> a -> Parser a
chainl p op a = (chainl1 p op) <|> return a

char : Char -> Parser Char
char ch = satisfy (ch ==)

digit : Parser Char
digit = satisfy isDigit

spaces : Parser String
spaces = pack <$> (many . oneOf . unpack $ " \n\r")

string : String -> Parser String
string st = pack <$> (string' $ unpack st)
    where
        string' : List Char -> Parser (List Char)
        string' [] = return []
        string' (c :: cs) = char c
                          >>= \_ => string' cs
                          >>= \_ => return (c :: cs)

token : Parser a -> Parser a
token p = p >>= \a => spaces >>= \_ => return a

reserved : String -> Parser String
reserved st = token (string st)

maybeNatural : Parser (Maybe Integer)
maybeNatural = parseInteger <$> (pack <$> some digit)

natural : Parser Integer
natural = fromMaybe <$> maybeNatural

maybeNumber : Parser (Maybe Int)
maybeNumber = do
    sign   <- (unpack <$> string "-") <|> return []
    digits <- some digit
    return $ parseInteger $ pack (sign ++ digits)

number : Parser Int
number = fromMaybe <$> maybeNumber

parens : Parser a -> Parser a
parens p = do
    reserved "("
    val <- p
    reserved ")"
    return val

max_stars_repo_name: stallmanifold/idris-nanoparsec

max_issues_repo_name: lambdaxymox/idris-nanoparsec

max_forks_repo_name: lambdaxymox/idris-nanoparsec


text:
main : IO ()
main = do
  printLn $ exp 1.0
  printLn $ log 2.7
  printLn $ sin 3.14
  printLn $ cos 3.14
  printLn $ tan 1.57
  printLn $ asin 0.01
  printLn $ acos 0.01
  printLn $ atan 0.01
  printLn $ sqrt 1000.0
  printLn $ floor 2.7
  printLn $ ceiling 11.1

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Minecraft.Core.Export

import public Minecraft.Core.Block.Export
import public Minecraft.Core.Entity.Export
import public Minecraft.Core.Entity.Pickup.Export
import public Minecraft.Core.Item.Export
import public Minecraft.Core.Item.Put.Export

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
printLength : IO ()
printLength = do putStr "Input string: "
                 input <- getLine
                 let len = length input
                 putStrLn (show len)

printLonger : IO ()
printLonger = do putStr "Input string 1: "
                 firstInput <- getLine
                 putStr "Input string 2: "
                 secondInput <- getLine
                 let longer = max (length firstInput) (length secondInput)
                 putStrLn (show longer)

printLongerAlt : IO ()
printLongerAlt = putStr "Input string 1: " >>= \_ =>
                 getLine >>= \input1 =>
                 putStr "Input string 2: " >>= \_=>
                 getLine >>= \input2 =>
                 let longer = max (length input1) (length input2) in
                     putStrLn (show longer)


text:
module Main

import System

----------------------------------------------------------------------
-- Hilffunktionen

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input) then
    pure (Just (cast input))
  else
    pure Nothing

----------------------------------------------------------------------
-- Projekt

-- Gesucht ist eine zufällige Zahl Z zwischen 1 und 100
-- (Hinweis: `System.time : IO Integer`)
-- Der Spieler hat n Versuche (Vorschlag: n=7)
-- Zunächst gibt das Spiel die Anzahl der verbliebenen Versuche aus
-- Dann wird der Spieler aufgefordert eine Zahl zu nennen
-- Hat er keine Zahl eingegeben wiederholt sich der letzt Schritt
-- (nach Ausgabe einer Warnung)
-- Hat der Spieler Z eraten hat er gewonnen
--    eine entsprechende Meldung wird ausgegeben und das Spiel ist beendet
-- Sonst erhält der Spieler eine Meldung (zu klein/zu groß) und das Spiel
-- geht mit einem Versuch weniger (n-1) oben weiter

-- Implementiere dazu diese Funktionen entsprechend:

rate : (ziel : Nat) -> (versuche : Nat) -> IO ()

zufallsZahl : IO Nat

main : IO ()
main = do
  ziel <- zufallsZahl
  rate ziel 7


text:
module LightClick.Values

import Data.List
import Data.List.Elem

import Data.Vect
import Data.Vect.Elem

import Data.String

import Toolkit.Data.DList
import Toolkit.Data.DVect

import Language.SystemVerilog.Gates
import Language.SystemVerilog.Utilities

import LightClick.Types
import LightClick.Terms
import LightClick.Error

%default total

public export
data TyValue : Type where
  PORT : (name : String) -> TyValue
  UNIT : TyValue
  MODULE : (names : (Vect (S n) String)) -> TyValue
  CONN : TyValue
  DATA : TyValue
  CHAN : TyValue
  GATE : TyValue

public export
data Value : TyValue -> Type where
  VRef  : (name : String)
       -> (type : TyValue)
               -> Value type

  VLet  : {term : TyValue}
       -> (name : String)
       -> (beThis : Value term)
       -> (inThis : Value expr)
                 -> Value expr

  VSeq  : {a,b : TyValue}
       -> (this     : Value a)
       -> (thenThis : Value b)
                   -> Value b

  VEnd : Value UNIT

  VPort : (label : String)
       -> (dir   : Direction)
       -> (type  : Value DATA)
                -> Value (PORT label)

  VModule : {n : Nat}
         -> {names : Vect (S n) String}
         -> DVect String
                  (Value . PORT)
                  (S n)
                  names
         -> Value (MODULE names)

  VDataLogic : Value DATA

  VDataArray : Value DATA
            -> Nat
            -> Value DATA

  VDataStruct : {n : Nat}
             -> Vect (S n) (Pair String (Value DATA))
             -> Value DATA

  VDataUnion  : {n : Nat}
             -> Vect (S n) (Pair String (Value DATA))
             -> Value DATA

  VChan : Value DATA -> Value CHAN

  VIDX : (name : String)
      -> (Value (MODULE names))
      -> (Value (PORT name))
      -> Value (PORT name)

  VConnD : Value CHAN
        -> Value (PORT i)
        -> Value (PORT o)
        -> Value CONN

  VConnFO : {m : Nat}
         -> {outs : Vect (S m) String}
         -> Value CHAN
         -> Value (PORT i)
         -> DVect String (Value . PORT) (S m) outs
         -> Value CONN

  VNot : Value CHAN
      -> Value CHAN
      -> Value GATE

  VGate : {n : Nat}
       -> TyGateComb
       -> Value CHAN
       -> Vect (S (S n)) (Value CHAN)
       -> Value GATE

  VConnG : Value CHAN
        -> Value (PORT p)
        -> Value CONN

export
getType : {type : TyValue} -> Value type -> TyValue
getType {type} _ = type

covering
showV : Value type -> String
showV (VRef name type)
  = "(VRef " <+> show name  <+> ")"

showV (VLet x y z) =
   "(VLet "
     <+> show x <+> " "
     <+> showV y <+> " "
     <+> showV z
     <+> ")"

showV (VSeq x y) =
    "(VSeq "
      <+> showV x <+> " "
      <+> showV y
      <+> ")"
showV VEnd = "(VEnd)"

showV (VPort x y z) =
    "(VPort "
      <+> show x <+> " "
      <+> show y <+> " "
      <+> showV z <+> " "
      <+> ")"

showV (VModule x) =
    "(VModule "
      <+> showDVect showV x
      <+> ")"

showV VDataLogic = "(VTyLogic)"

showV (VDataArray x k) =
  "(VTyArray "
    <+> showV x <+> " "
    <+> show k
    <+> ")"

showV (VDataStruct {n} xs)
  = "(VTyStruct " <+> show ps <+> ")"
    where
      covering
      ps : Vect (S n) String
      ps = map (\(l,c) => "(" <+> show l <+> " " <+> showV c <+> ")") xs

showV (VDataUnion {n} xs) = "(TyUnion " <+> show ps <+> ")"
  where
    covering
    ps : Vect (S n) String
    ps = map (\(l,c) => "(" <+> show l <+> " " <+> showV c <+> ")") xs

showV (VChan x) = "(VChan " <+> showV x <+> ")"

showV (VIDX x y z) =
    "(VIndex "
       <+> show x <+> " "
       <+> showV y <+> " "
       <+> showV z
       <+> ")"

showV (VConnD x y z) =
    "(VDConn "
      <+> showV x <+> " "
      <+> showV y <+> " "
      <+> showV z <+> " "
      <+> ")"

showV (VConnFO x y z) =
    "(VFConn "
      <+> showV x <+> " "
      <+> showV y <+> " "
      <+> showDVect showV z <+> " "
      <+> ")"

showV (VNot o i)
  = unwords ["(VNot", showV o, showV i, ")"]

showV (VGate ty o ins)
    = unwords ["(VGate", show ty, showV o, ins', ")"]

  where
    covering
    ins' : String
    ins' = unwords $ toList $ map (\c => "(" <+> showV c <+> ")") ins

showV (VConnG c idx)
  = unwords ["(VConnG", showV c, showV idx, ")"]

export
Show (Value type) where
  show = assert_total showV -- TODO

public export
interp : MTy -> TyValue
interp (PORT x) = PORT x
interp UNIT = UNIT
interp (MODULE xs) = MODULE xs
interp CONN = CONN
interp DATA = DATA
interp GATE = GATE

export
getData : Value (PORT s) -> Either LightClick.Error (Value DATA)
getData (VRef x (PORT s)) = Left (NotSupposedToHappen (Just "getData"))
getData (VLet x y z)      = Left (NotSupposedToHappen (Just "getData"))
getData (VSeq x y)        = Left (NotSupposedToHappen (Just "getData"))
getData (VPort x y z) = Right z
getData (VIDX x y z) = getData z

export
genNameConn : Value (PORT s) -> Either LightClick.Error String
genNameConn (VRef name (PORT s)) = Left $ NotSupposedToHappen (Just "genNameConn ref")
genNameConn (VLet x y z)         = Left $ NotSupposedToHappen (Just "genNameConn let")
genNameConn (VSeq x y)           = Left $ NotSupposedToHappen (Just "genNameConn seq")
genNameConn (VPort x y z) = Right x
genNameConn (VIDX x (VRef m (MODULE names)) z) = Right (newName [m,x])
genNameConn (VIDX x y z) = Left $ NotSupposedToHappen (Just $ "genNameConn idx non-ref" <+> show y)

export
mkDual : (n : String) -> Value (PORT s) -> Either LightClick.Error (Value (PORT (n <+> s)))
mkDual n (VLet _ _ _)  = Left $ NotSupposedToHappen (Just "mkDual")
mkDual n (VSeq  _ _)   = Left $ NotSupposedToHappen (Just "mkDual")
mkDual n (VRef _ _)    = Left $ NotSupposedToHappen (Just "mkDual")
mkDual n (VIDX x y z)  = mkDual n z
mkDual n (VPort x IN    t) = Right (VPort (n <+> x) OUT t)
mkDual n (VPort x OUT   t) = Right (VPort (n <+> x) IN t)
mkDual n (VPort x INOUT t) = Right (VPort (n <+> x) INOUT t)

export
genNameFan : DVect String (Value . PORT) k names -> Either LightClick.Error String
genNameFan Nil      = Right ""
genNameFan (x::Nil) = genNameConn x
genNameFan (x::xs) =
  do n <- genNameConn x
     rest <- genNameFan xs
     pure $ newName [n,rest]

export
getNameFan : DVect String (Value . PORT) k names
          -> Either LightClick.Error (Vect k String)
getNameFan Nil      = Right Nil
getNameFan (x::Nil) = do n <- genNameConn x
                         pure [n]
getNameFan (x::xs) =
  do n <- genNameConn x
     rest <- getNameFan xs
     pure $ n :: rest

public export
fanPortNames : (p : String)
            -> (n : Nat)
            -> Vect n String
fanPortNames p Z = Nil
fanPortNames p (S k) = (p <+> "fan_" <+> show (S k) <+> "_") :: fanPortNames p k

dualFanG : {k : Nat}
        -> (ps : Vect k String)
        -> {names : Vect k String}
        -> DVect String (Value . PORT) k names
        -> Either LightClick.Error (DVect String (Value . PORT) k (zipWith (<+>) ps names))
dualFanG Nil     Nil     = Right Nil
dualFanG (p::ps) (x::xs) = do
   rest <- dualFanG ps xs
   d <- mkDual p x
   pure (d :: rest)

export
dualFan : {n : Nat}
       -> (ps : Vect (S (S n)) String)
        -> {names : Vect (S (S n)) String}
       -> DVect String (Value . PORT) (S (S n)) names
       -> Either LightClick.Error
                 (DVect String (Value . PORT) (S (S n)) (zipWith (<+>) ps names))
dualFan (p::q::ps) (x::y::xs) = do
  xs' <- dualFanG ps xs
  x' <- mkDual p x
  y' <- mkDual q y

  pure (x'::y'::xs')

export
dualFan' : {n     : Nat}
        -> (p     : String)
        -> {names : Vect (S (S n)) String}
        -> (ports : DVect String (Value . PORT) (S (S n)) names)
        -> Either LightClick.Error
                 (DVect String (Value . PORT) (S (S n)) (zipWith (<+>) (fanPortNames p (S (S n))) names))
dualFan' p (x::y::xs) {n} = dualFan (fanPortNames p (S (S n))) (x::y::xs)

getPort' : DVect String (Value . PORT) n names
        -> Elem nam names
        -> Either LightClick.Error (Value (PORT nam))
getPort' (y :: xs) Here          = Right y
getPort' (y::ys)   (There later) = getPort' ys later

export
getPort : DVect String (Value . PORT) (S n) names
       -> Elem nam names
       -> (Either LightClick.Error $ Value (PORT nam))
getPort (z :: xs) Here = Right z
getPort (z :: xs) (There later) = getPort' xs later

export
getPortFromModule : Value (MODULE names)
                 -> Elem nam names
                 -> Either LightClick.Error $ Value (PORT nam)
getPortFromModule (VLet x w s) z = Left $ NotSupposedToHappen (Just "getPrtFromModule")
getPortFromModule (VSeq x w)   z = Left $ NotSupposedToHappen (Just "getPrtFromModule")
getPortFromModule (VRef _ _)   z = Left $ NotSupposedToHappen (Just "getPrtFromModule")
getPortFromModule {nam} (VModule x)  z = getPort x z

namespace IndexBuilder
   export
   newIDX : {s : String}
         -> (m : Value (MODULE names))
         -> (port  : Value (PORT s))
         -> Value (PORT s)
   newIDX {s} = VIDX s

   export
   recoverRef : {names : Vect (S n) String}
             -> (m : Value (MODULE names))
             -> (label : String)
             -> Value (MODULE names)
   recoverRef {names} _ label = VRef label (MODULE names)

namespace ConnBuilder

  namespace Gate
    export
    newConn : (name : String)
           -> Value (PORT i)
           -> Value CONN
    newConn name i = (VConnG (VRef name CHAN) i)

    namespace FanIn
      helper : (cname : String)
            -> (n     : Nat)
            -> (dTy   : Value DATA)
            -> (iport : Value (PORT i))
                     -> Either LightClick.Error (Value CHAN, Value CONN)
      helper cname n type src
        = let cname' = newName [cname, show n]
          in Right ( VRef cname' CHAN
                   , VLet cname'
                          (VChan type)
                          (Gate.newConn cname' src)
                   )

      newConn' : (c     : Nat)
              -> (cname : String)
              -> (type  : Value DATA)
              -> (is    : DVect String (Value . PORT) (S (S n)) ins)
                       -> Either LightClick.Error
                                 ( Vect (S (S n)) (Value CHAN)
                                 , Value CONN)
      newConn' c name type (i::j::Nil)
        = do (i'', i') <- helper name c     type i
             (j'', j') <- helper name (S c) type j
             pure ([i'', j''], VSeq i' j')

      newConn' c name type (i::j::k::is)
        = do (rest', rest) <- newConn' (S (S c)) name type (j::k::is)
             (i'',   i')   <- helper name c type i
             pure (i''::rest', VSeq i' rest)

      export
      newConn : (cname : String)
             -> (type  : Value DATA)
             -> (is    : DVect String (Value . PORT) (S (S n)) ins)
                      -> Either LightClick.Error
                                ( Vect (S (S n)) (Value CHAN)
                                , Value CONN
                                )
      newConn = newConn' Z

  namespace Direct
    export
    newConn : (name : String)
           -> Value (PORT ins)
           -> Value (PORT outs)
           -> Value CONN
    newConn name x y = (VConnD (VRef name CHAN) x y)
  namespace FanOut
    export
    newConn : {n : Nat}
           -> {outs : Vect (S n) String}
           -> (name : String)
           -> (is   : Value (PORT i))
           -> (os   : DVect String (Value . PORT) (S n) outs)
           -> Value CONN
    newConn name is os = (VConnFO (VRef name CHAN) is os)

  namespace FanIn
    export
    helper :  {o : String}
          -> (cname : String)
           -> (dTy   : Value DATA)
           -> (mod   : Value (MODULE names))
           -> (iport : Value (PORT i))
           -> (oport : Value (PORT o))
           -> Either LightClick.Error (Value CONN)
    helper {o} cname dTy m x y = do
      nX <- genNameConn x
      nY <- genNameConn y
      let cname' = newName [cname, nX, nY]
      pure (VLet cname'
                   (VChan dTy)
                   (Direct.newConn cname' x (VIDX o m y)))

    export
    newConn : (cname : String)
           -> (Value DATA)
           -> (Value (MODULE names))
           -> (is : DVect String (Value . PORT) (S n) ins)
           -> (os : DVect String (Value . PORT) (S n) outs)
                 -> Either LightClick.Error (Value CONN)
    newConn cname type m (i :: []) (o :: []) = helper cname type m i o
    newConn cname type m (i :: i' :: is) (o :: o' :: os)
      = do xy <- helper cname type m i o
           rest <- newConn cname type m (i'::is) (o'::os)
           pure (VSeq xy rest)

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


text:
import Language.JSON

main : IO ()
main = do
    printLn $ JObject [
        ("a", cast ()),
        ("b", cast True),
        ("c", cast 1.0),
        ("d", cast "Hello, world"),
        ("e", cast ["Lorem", "ipsum"])
      ]


text:
module Midlevel
import UserApi
import Control.Monad.Freer

%access public export

data TFops : Type where
  Placeholder : String->TFops

str2tfops : String -> TFops
str2tfops x = Placeholder ""

runFreeGraph : FreeGraph -> IO ()
runFreeGraph (Pure x) = pure ()
runFreeGraph (Bind _ _) = pure ()

max_stars_repo_name: justjoheinz/tensorflow-idris

max_issues_repo_name: doofin/differentiable-idris

max_forks_repo_name: doofin/differentiable-idris


text:
module Crazy

%default total
%access public export

data QVect : (Type -> Type) -> List Type -> Type where
  Nil : QVect q []
  (::) : q x -> QVect q xs -> QVect q (x :: xs)

||| Type representing a query type which encodes a query _request_ (presumably a
||| GADT), paired with a handler for it.
record HandledQry (q : Type -> Type)  (a : Type) where
  constructor HandleQry
  qry : q i
  handle : i -> a

record Qry (q : Type -> Type) (a : Type) where
  constructor Q
  queries : QVect (HandledQry q) ts
  handleN : QVect Basics.id ts -> a

pure : a -> Qry q a
pure x = Q [] (\_ => x)


text:
module Main

main : IO ()
main = printLn "Hello World"