text:
module Language.JSON.Lexer

import Language.JSON.String
import Text.Lexer
import Text.Token

import public Language.JSON.Tokens

%default total

private
numberLit : Lexer
numberLit
  = let sign  = is '-'
        whole = is '0' <|> range '1' '9' <+> many digit
        frac  = is '.' <+> digits
        exp   = like 'e' <+> opt (oneOf "+-") <+> digits in
        opt sign <+> whole <+> opt frac <+> opt exp

private
jsonTokenMap : TokenMap JSONToken
jsonTokenMap = toTokenMap $
  [ (spaces, JTIgnore)
  , (is ',', JTPunct Comma)
  , (is ':', JTPunct Colon)
  , (is '[', JTPunct $ Square Open)
  , (is ']', JTPunct $ Square Close)
  , (is '{', JTPunct $ Curly Open)
  , (is '}', JTPunct $ Curly Close)
  , (exact "null", JTNull)
  , (exact strTrue <|> exact strFalse, JTBoolean)
  , (numberLit, JTNumber)
  , (permissiveStringLit, JTString)
  ]

export
lexJSON : String -> Maybe (List (WithBounds JSONToken))
lexJSON str
  = case lex jsonTokenMap str of
         (tokens, _, _, "") => Just $ tokens
         _ => Nothing


text:
module ListLast

public export
data ListLast : List a -> Type where
  Empty : ListLast []
  NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])

export
total
listLast : (xs : List a) -> ListLast xs
listLast [] = Empty
listLast (x :: xs) = case listLast xs of
                          Empty => NonEmpty [] x
                          NonEmpty xs y => NonEmpty (x :: xs) y

ext: idr

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
||| WIP: same as Data.List.Quantifiers but for lazy lists

module Data.List.Lazy.Quantifiers

import Data.DPair
import Data.List.Lazy

%default total

namespace Any

  -- Note: it is crucial here that we mark `xs` as `Lazy`, otherwise Idris
  --  will happily use `Delay` in the return index and give us a badly-behaved
  -- family!
  public export
  data Any : (p : a -> Type) -> (xs : LazyList a) -> Type where
    Here : {0 xs : Lazy (LazyList a)} -> p x -> Any p (x :: xs)
    There : {0 xs : Lazy (LazyList a)} -> Any p xs -> Any p (x :: xs)

  public export
  toExists : Any p xs -> Exists p
  toExists (Here prf) = Evidence _ prf
  toExists (There p) = toExists p

  public export
  toDPair : {xs : LazyList a} -> Any p xs -> DPair a p
  toDPair (Here prf) = (_ ** prf)
  toDPair (There p) = toDPair p


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/modules.html#start-function
module WebAssembly.Structure.Modules.StartFunction

import WebAssembly.Structure.Modules.Indices

import Decidable.Equality

-- Definition

public export
record Start where
  constructor MkStart
  func : FuncIdx

-- Equality

total public export
lemma_start__func_injective : ((f1 = f2) -> Void) -> (MkStart f1 = MkStart f2) -> Void
lemma_start__func_injective f1_not_f2 Refl = f1_not_f2 Refl

-- Decidable Equality

public export
implementation DecEq Start where
  decEq (MkStart f1) (MkStart f2) = case decEq f1 f2 of
    No f1_not_f2 => No $ lemma_start__func_injective f1_not_f2
    Yes Refl     => Yes Refl

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module CanEscape

import Language.Reflection

%language ElabReflection

-- Show that actually an erased value can escape through an elaboration script

0 n : Nat
n = 3

elabScript : Elab Nat
elabScript = check !(quote n)

M : Nat
M = %runElab elabScript

mIs3 : M = 3
mIs3 = Refl

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Minecraft.Base.PreClassic.Air.Block.Export

import public Minecraft.Core.Entity
import public Minecraft.Base.PreClassic.Air.Block

%default total

public export
Eq Air.Block where
  x == y = True

public export
Serialize Air.Block where
  identifier = "Air.Block"
  serialize x = JNull

public export
Deserialize Air.Block where
  deserialize _ = Just $ Air.MkBlock

[airBlock']
Block Air.Block where
  id = "minecraft:air"

[airVtbl']
Vtbl Air.Block where
  vtable (Block    Air.Block) = Just airBlock
  vtable (Tangible Air.Block) = Just %search
  vtable _ = Nothing

airBlock = airBlock'
airVtbl  = airVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Types.Inclusion

import Syntax.PreorderReasoning
import Control.Isomorphism

%default total

-- An inclusion from a to b
data Inclusion : (a, b : Type) -> Type where
  Include : (upcast : a -> b) ->
            (downcast : b -> Maybe a) ->
            (upThenDown : (x : a) -> downcast (upcast x) = Just x) ->
            (downThenUp : (y : b) -> maybe () (\x => upcast x = y) (downcast y)) ->
            Inclusion a b

includeRefl : Inclusion a a
includeRefl = Include id Just (\x => Refl) (\y => Refl)

includeTrans : Inclusion a b -> Inclusion b c -> Inclusion a c
includeTrans {a} {b} {c} (Include u d ud du) (Include u' d' ud' du') =
  Include (\x => u' (u x))
          (\y => (d' y) >>= d)
          ok1
          ok2

    where ok1 : (x : a) -> (d' (u' (u x))) >>= d = Just x
          ok1 x = ((d' (u' (u x))) >>= d) ={ cong {f=(>>= d)} (ud' (u x)) }=
                  ((Just (u x)) >>= d)    ={ Refl }=
                  (d (u x))               ={ ud x }=
                  (Just x)                QED

          ok2 : (y : c) -> maybe () (\x => u' (u x) = y) ((d' y) >>= d)
          ok2 y = ok2' (d' y) (du' y) -- Do the first case analysis, but keep the proof
            where ok2' : (z : Maybe b) ->
                         maybe () (\x => u' x = y) z ->
                         maybe () (\x => u' (u x) = y) (z >>= d)
                  ok2' Nothing prf = ()
                  ok2' (Just x) prf = ok2'' (d x) (du x) -- second analysis, keep proof
                    where ok2'' : (z : Maybe a) ->
                                  maybe () (\w => u w = x) z ->
                                  maybe (the Type ()) (\x1 => u' (u x1) = y) z
                          ok2'' Nothing prf2 = ()
                          ok2'' (Just v) prf2 = (u' (u v)) ={ cong prf2 }=
                                                (u' x)     ={ prf       }=
                                                y          QED

-- Enable preorder reasoning syntax over inclusions
qed : (a : Type) -> Inclusion a a
qed a = includeRefl

step : (a : Type) -> Inclusion a b -> Inclusion b c -> Inclusion a c
step a incl1 incl2 = includeTrans incl1 incl2

-- Every isomorphism gives an inclusion mapping
includeIso : Iso a b -> Inclusion a b
includeIso {a} {b} (MkIso to from toFrom fromTo) =
  Include to (\x => Just (from x)) ok1 ok2
    where ok1 : (x : a) -> (Just (from (to x)) = Just x)
          ok1 x = rewrite fromTo x in Refl -- workaround for de Bruijn index bug
          ok2 : (y : b) -> to (from y) = y
          ok2 y = rewrite toFrom y in Refl -- workaround for de Bruijn index bug

castUp : Inclusion a b -> a -> b
castUp (Include up _ _ _) = up

castDown : Inclusion a b -> b -> Maybe a
castDown (Include _ down _ _) = down

max_stars_repo_name: david-christiansen/idris-utils

max_issues_repo_name: david-christiansen/idris-utils

max_forks_repo_name: david-christiansen/idris-utils


text:
||| A binary relation is a function of type (ty -> ty -> Type).
|||
||| A prominent example of a binary relation is LTE over Nat.
|||
||| This module defines some interfaces for describing properties of
||| binary relations. It also proves somes relations among relations.

module Control.Relation

%default total

||| A relation on ty is a type indexed by two ty values
public export
Rel : Type -> Type
Rel ty = ty -> ty -> Type

||| A relation is reflexive if x ~ x for every x.
public export
interface Reflexive ty rel where
  constructor MkReflexive
  reflexive : {x : ty} -> rel x x

||| A relation is transitive if x ~ z when x ~ y and y ~ z.
public export
interface Transitive ty rel where
  constructor MkTransitive
  transitive : {x, y, z : ty} -> rel x y -> rel y z -> rel x z

||| A relation is symmetric if y ~ x when x ~ y.
public export
interface Symmetric ty rel where
  constructor MkSymmetric
  symmetric : {x, y : ty} -> rel x y -> rel y x

||| A relation is antisymmetric if no two distinct elements bear the relation to each other.
public export
interface Antisymmetric ty rel where
  constructor MkAntisymmetric
  antisymmetric : {x, y : ty} -> rel x y -> rel y x -> x = y

||| A relation is dense if when x ~ y there is z such that x ~ z and z ~ y.
public export
interface Dense ty rel where
  constructor MkDense
  dense : {x, y : ty} -> rel x y -> (z : ty ** (rel x z, rel z y))

||| A relation is serial if for all x there is a y such that x ~ y.
public export
interface Serial ty rel where
  constructor MkSerial
  serial : {x : ty} -> (y : ty ** rel x y)

||| A relation is euclidean if y ~ z when x ~ y and x ~ z.
public export
interface Euclidean ty rel where
  constructor MkEuclidean
  euclidean : {x, y, z : ty} -> rel x y -> rel x z -> rel y z

||| A tolerance relation is reflexive and symmetric.
public export
interface (Reflexive ty rel, Symmetric ty rel) => Tolerance ty rel where

||| A partial equivalence is transitive and symmetric.
public export
interface (Transitive ty rel, Symmetric ty rel) => PartialEquivalence ty rel where

||| An equivalence relation is transitive, symmetric, and reflexive.
public export
interface (Reflexive ty rel, Transitive ty rel, Symmetric ty rel) => Equivalence ty rel where

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

||| Every reflexive relation is dense.
public export
Reflexive ty rel => Dense ty rel where
  dense {x} xy = (x ** (reflexive {x}, xy))

||| Every reflexive relation is serial.
public export
Reflexive ty rel => Serial ty rel where
  serial {x} = (x ** reflexive {x})

||| A transitive symmetric serial relation is reflexive.
public export
(Transitive ty rel, Symmetric ty rel, Serial ty rel) => Reflexive ty rel where
  reflexive {x} =
    let (y ** xy) = serial {x} in
      transitive {x} xy $ symmetric {x} xy

||| A reflexive euclidean relation is symmetric.
public export
[RES] (Reflexive ty rel, Euclidean ty rel) => Symmetric ty rel where
  symmetric {x} xy =
    euclidean {x} xy $ reflexive {x}

||| A reflexive euclidean relation is transitive.
public export
[RET] (Reflexive ty rel, Euclidean ty rel) =>
      Transitive ty rel using RES where
  transitive {rel} xy yz =
    symmetric {rel} $ euclidean {rel} yz $ symmetric {rel} xy

||| A transitive symmetrics relation is euclidean.
public export
[TSE] (Transitive ty rel, Symmetric ty rel) => Euclidean ty rel where
  euclidean {rel} xy xz =
    transitive {rel} (symmetric {rel} xy) xz

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

public export
Reflexive ty Equal where
  reflexive = Refl

public export
Symmetric ty Equal where
  symmetric xy = sym xy

public export
Transitive ty Equal where
  transitive xy yz = trans xy yz

public export
Euclidean ty Equal where
  euclidean = euclidean {rel = Equal} @{TSE}

public export
Tolerance ty Equal where

public export
PartialEquivalence ty Equal where

public export
Equivalence ty Equal where


text:
module Isomorphisms

import Linear.Types
import FunExt

-- Isomorphisms in the category of types and linear functions
record Iso a b where
  constructor MkIso
  to : a -<> b
  from : b -<> a
  0 toFrom : (0 y : b) -> to (from y) = y
  0 fromTo : (0 x : a) -> from (to x) = x

-- Identity isomorphism
idIso : Iso a a
idIso = MkIso (\ x => x) (\ x => x) (\ x => Refl) (\ x => Refl)

-- Composition of isomorphisms
transIso : Iso a b -> Iso b c -> Iso a c
transIso f g = MkIso (\ x => to g (to f x))
                     (\ x => from f (from g x))
                     (\ x => rewrite toFrom f (from g x) in toFrom g x)
                     (\ x => rewrite fromTo g (to f x) in fromTo f x)

-- "Dependent pairs are left adjoint to dependent functions" -- true
-- for arbitrary resource annotation ρ, but can only be stated for ρ =
-- 0, 1, ω^< in Idris 2. Here we state it for the most interesting
-- case ρ = ω^<.
curryuncurry : {c : Sigma1 a b -> Type} ->
               Iso ((1 xy : Sigma1 a b) -> c xy) ((1 x : a) -> (1 y : b x) -> c (x # y))
curryuncurry = MkIso (\ f => \ x => \ y => f (x # y))
                     (\ g => \ (x # y) => g x y)
                     (\ f => Refl)
                     (\ g => funext (\ (x # y) => Refl))

pairUnitL : Iso (Sigma1 I b) (b Star)
pairUnitL = MkIso (\ (Star # a) => a)
                  (\ a => Star # a)
                  (\ x => Refl)
                  (\ (Star # a) => Refl)

data Box : Type -> Type where
  Unrestricted : a -> Box x

{-
-- The rules for Top refer to arbitrary contexts, so they
-- cannot be formulated inside Idris 2 itself.

zeroInitial : Iso (Void -<> a) Top
zeroInitial = MkIso (\ f => Star)
                    (\ x => \ y => void1 y)
                    (\ x => ?Refl)
                    (\ x => funext (\ y => void1 y))
-}

trivArgument : Iso (I -<> a) a
trivArgument = MkIso (\ f => f Star)
                     (\ a => \ Star => a)
                     (\ a => Refl)
                     (\ f => funext (\ Star => Refl))

-- With our encoding of With a a, this is almost a tautology
twoArgument : Iso (Bool -<> a) (With a a)
twoArgument = MkIso (\ f => \ b => if b then f True else f False)
                    (\ aa => \ b => if b then aa True else aa False)
                    (\ f => funext (\ b => if b then Refl else Refl))
                    (\ aa => funext (\ b => if b then Refl else Refl))

max_stars_repo_name: g-nakov/quantitative-poly

max_issues_repo_name: g-nakov/quantitative-poly

max_forks_repo_name: g-nakov/quantitative-poly


text:
module Test.Parser

import Test.Assertions
import Idrlisp.Sexp
import Idrlisp.Parser

%default covering

export
test : IO ()
test = describe "Idrlisp.Parser" $ do
  describe "parseToEnd" $ do
    let parseSyn = parseToEnd {ty = SSyn ()}
    parseSyn "123"
      `shouldBe` Right (Num 123)
    parseSyn " \n\t ; comment \n 3.14  "
      `shouldBe` Right (Num 3.14)
    parseSyn "*foo-bar+baz"
      `shouldBe` Right (Sym "*foo-bar+baz")
    parseSyn (show "Hello, World!\n")
      `shouldBe` Right (Str "Hello, World!\n")
    parseSyn "()"
      `shouldBe` Right Nil
    parseSyn "(#t)"
      `shouldBe` Right (App [Bool True])
    parseSyn "(#t #f)"
      `shouldBe` Right (App [Bool True, Bool False])
    parseSyn "(#t #f . 0)"
      `shouldBe` Right ([Bool True, Bool False] :.: Num 0)
    parseSyn "(#t #f . 0 1)"
      `shouldSatisfy` isLeft
    parseSyn "(foo [bar baz])"
      `shouldBe` Right (App [Sym "foo", App [Sym "bar", Sym "baz"]])
    parseSyn "`(foo ,bar ,@(hoge 'fuga))"
      `shouldBe` Right (Quasiquote (App [Sym "foo", Unquote (Sym "bar"), UnquoteSplicing (App [Sym "hoge", Quote (Sym "fuga")])]))
    parseToEnd {ty = List (SSyn ())} "123 () foo ; test \n \"bar\""
      `shouldBe` Right [Num 123.0, Nil, Sym "foo", Str "bar"]

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
import Data.List
import System.Concurrency

consumer : Channel Nat -> IO ()
consumer c =
  do (S k) <- channelGet c
      | Z => pure ()
     consumer c

producer : Channel Nat -> IO ()
producer c = ignore $ traverse (\n => channelPut c n) [1..100]

nConsumers : Nat
nConsumers = 3

nProducers : Nat
nProducers = 5

main : IO ()
main =
  do c <- makeChannel
     cTIDs <- for (replicate nConsumers 0) $ \_ => fork (consumer c)
     pTIDs <- for (replicate nProducers 0) $ \_ => fork (producer c)
     ignore $ traverse (\t => threadWait t) pTIDs
     ignore $ for (replicate nConsumers 0) $ \_ => channelPut c Z
     ignore $ traverse (\t => threadWait t) cTIDs
     putStrLn "SUCCESS!!!"


text:
module SimpleFFI.Renderer

import SimpleFFI.Spec
import Data.Either
import Data.List
import Data.SortedMap
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.String

emptyLine : Doc ()
emptyLine = hardline <+> hardline

stringLit : String -> Doc ()
stringLit = dquotes . pretty

sepByLines : List (Doc ()) -> Doc ()
sepByLines ds@(d::_) = foldl1 (\acc, d => acc <+> emptyLine <+> d) ds
sepByLines [] = emptyDoc

indented : Doc () -> Doc ()
indented d = nest 2 (hardline <+> d) <+> hardline

inline : Doc ()
inline = pretty "%inline"

pubExport : Doc ()
pubExport = pretty "public export"

export_ : Doc ()
export_ = pretty "export" <+> hardline

typeHeader : Doc () -> Doc ()
typeHeader n = vcat [
  inline,
  pubExport,
  n <++> colon <++> pretty "Type"
]

arr : Doc ()
arr = pretty " ->"

funType : List (Doc ()) -> Doc ()
funType = hsep . punctuate arr

namespaced : String -> Doc () -> Doc ()
namespaced n body = pretty ("namespace " ++ n) <+> indented body

prettyType : DartType -> Doc ()
prettyType ty = case ty of
  BoolType => pretty "DartBool"
  IntType => pretty "Int"
  StringType => pretty "String"
  DoubleType => pretty "Double"
  VoidType => pretty "()"
  NamedType n => pretty n
  ListType a => parens (pretty "DartList" <++> prettyType a)
  FunctionType ps ret =>
    let sig = (prettyType <$> ps) ++ [pretty "IO" <++> prettyType ret]
    in parens (funType sig)

structField : (String, DartType) -> Doc ()
structField (n, ty) =
  parens $ hsep $ punctuate comma $ [stringLit n, prettyType ty]

fieldList : List (String, DartType) -> Doc ()
fieldList [] = pretty "[]"
fieldList fs =
  enclose "[" "]"
    (indented . vsep . punctuate comma $ (structField <$> fs))

foreignNameOf : {auto lib : Lib} -> String -> String
foreignNameOf name = name ++ "," ++ lib.package

typeDecl : {auto lib : Lib} -> String -> List (String, DartType) -> Doc ()
typeDecl name fields =
  let
    name' = pretty name
    foreignTypeName = dquotes (pretty (foreignNameOf name))
    struct = pretty "Struct" <++> foreignTypeName <++> fieldList fields
  in
    typeHeader name' <+> hardline <+> name' <++> equals <++> struct

fields : Class -> List Field
fields c = mapMaybe field c.members
  where
    field : Member -> Maybe Field
    field (FieldMember f) = Just f
    field _ = Nothing

nameAndType : Field -> (String, DartType)
nameAndType (Var n ty) = (n, ty)
nameAndType (Final n ty) = (n, ty)

typeDeclFor : {auto lib : Lib} -> Declaration -> Doc ()
typeDeclFor (ClassDecl c) =
  typeDecl c.name (nameAndType <$> fields c)
typeDeclFor (EnumDecl n fs) =
  typeDecl n []

typeDeclsForLib : LibDef -> List (Doc ())
typeDeclsForLib libDef =
  let lib = libDef.lib
  in typeDeclFor <$> libDef.declarations

this : Doc ()
this = pretty "this"

ioUnit : Doc ()
ioUnit = pretty "IO ()"

capitalize : String -> String
capitalize s =
  let cs = unpack s
  in pack ((toUpper <$> take 1 cs) ++ drop 1 cs)

setter : String -> String -> DartType -> Doc ()
setter owner field ty =
  let
    n = pretty ("set" ++ capitalize field)
    field' = pretty field
    ty' = prettyType ty
    val = pretty "value"
  in
    export_
      <+> n <++> colon <++> funType [ty', pretty owner, ioUnit] <+> hardline
      <+> n <++> val <++> this <++> equals
      <++> pretty "setField" <++> this <++> dquotes field' <++> val

getter : String -> String -> DartType -> Doc ()
getter owner field ty =
  let
    field' = pretty field
    ty' = prettyType ty
  in
    export_
      <+> field' <++> colon <++> funType [pretty owner, ty'] <+> hardline
      <+> field' <++> this <++> equals
      <++> pretty "getField" <++> this <++> dquotes field'

foreign' : Doc ()
foreign' = pretty "%foreign"

foreign : String -> Doc ()
foreign n = foreign' <++> dquotes (pretty ("Dart:" ++ n))

prettyParameter : Parameter -> Doc ()
prettyParameter (P n ty) = parens (pretty n <++> colon <++> prettyType ty)
prettyParameter _ = emptyDoc

partitionParameters : List Parameter -> (List (String, DartType), List (String, DartType))
partitionParameters ps = partitionEithers . flip map ps $ \case
  P n ty => Left (n, ty)
  N n ty => Right (n, ty)

parameterNames : List Parameter -> List (Doc ())
parameterNames ps = flip mapMaybe ps $ \case
  P n _ => Just (pretty n)
  _ => Nothing

parameters' : Doc ()
parameters'= pretty "NamedParameters"

namedParameterDeclarationsFor : String -> String -> List (String, DartType) -> Doc ()
namedParameterDeclarationsFor typeName _ [] = emptyDoc
namedParameterDeclarationsFor typeName ns ps = namespaced ns (sepByLines (tag :: (decl <$> ps)) <+> hardline <+> schema)
  where
    qualified : String -> Doc ()
    qualified n = pretty (typeName ++ "." ++ ns ++ "." ++ n)

    tag : Doc ()
    tag = pretty "data Tag : Type where"

    schema : Doc ()
    schema = vcat [
      inline,
      pubExport,
      parameters' <++> colon <++> pretty "Type",
      parameters' <++> equals <++> pretty "Parameters" <++> list ((\(n, _) => qualified n) <$> ps)
    ]

    decl : (String, DartType) -> Doc ()
    decl (n, ty) = vcat [
      inline,
      pubExport,
      pretty n <++> colon <++> pretty "Parameter" <++> qualified "Tag",
      pretty n <++> equals <++> pretty "mkParameter" <++> hsep [stringLit n, prettyType ty]
    ]

ctorPrimsFor : {auto lib : Lib} -> {auto c : Class} -> String -> List Parameter -> Maybe DartType -> Maybe String -> List (Doc ())
ctorPrimsFor n ps ret foreignName =
  let
    funName = if length n == 0 then "new" else n
    namedParameterNS = capitalize funName
    input' = pretty c.name
    ret' = case ret of
              Nothing => input'
              (Just ret) => prettyType ret
    foreignName' = case foreignName of
                        Nothing => ""
                        (Just foreignName) => foreignName
    prim__new =  pretty "  export %extern prim__dart_new : Type -> HVect positional -> Parameters named -> (1 x : %World) -> IORes " <++> ret'
    (positionalPs, namedPs) = partitionParameters ps
    positionalPs' = (\(n, ty) => parens (pretty n <++> colon <++> prettyType ty)) <$> positionalPs
    psNames = pretty . fst <$> positionalPs
    (ps', pTys', args') = if isNil namedPs
      then (
        hsep psNames,
        positionalPs',
        list psNames <++> parens (pretty "the (Parameters {tag = Void} [])" <++> list [])
      ) else (
        hsep psNames <++> pretty "ps",
        positionalPs' ++ [input' <+> dot <+> pretty namedParameterNS <+> dot <+> parameters'],
        list psNames <++> pretty "ps"
      )
    funBody = pretty funName <++> ps' <++> equals <++> pretty "primIO $ prim__dart_new" <++> ret' <++> args'
    funBodyForeign =
        let prim_type = pretty $ "(Struct \"" ++ foreignName' ++ "\" [])"
        in pretty funName <++> ps' <++> equals <++> pretty ("primIO $ " ++ namedParameterNS ++ ".prim__dart_new") <++> prim_type <++> args'
    fun = vcat [
      case foreignName of
        Nothing => pretty ""
        otherwise => prim__new <+> hardline,
      inline,
      pubExport,
      pretty funName <++> colon <++> pretty "HasIO io =>" <++> funType (pTys' ++ [pretty "io" <++> ret']),
      case foreignName of
        Nothing => funBody
        otherwise => funBodyForeign
    ]
  in
    if isNil namedPs
      then [fun]
      else [namedParameterDeclarationsFor c.name namedParameterNS namedPs, fun]

isIdrisKeyword : String -> Bool
isIdrisKeyword s = case s of
  "of" => True
  _ => False

functionPrimsFor : {auto lib : Lib} -> {auto c : Class} -> Function -> String -> Bool -> List (Doc ())
functionPrimsFor (Fun n ps ret) foreignName hasThis =
  let
    ret' = prettyType ret
    ps' = prettyParameter <$> ps
    psNames = parameterNames ps
    primName = pretty ("prim__" ++ n)
    primRet = pretty "PrimIO" <++> ret'
    primParamTys = ps' ++ [primRet]
    proxyParamTys = [pretty "io" <++> ret']
    thisTy = the (Lazy (Doc())) (parens (this <++> colon <++> pretty c.name))
    proxyName = pretty (if isIdrisKeyword n then n ++ "_" else n)
    (positionalPs, namedPs) = partitionParameters ps
    prim =
      foreign foreignName <+> hardline
        <+> primName <++> colon <++> funType (ifHasThis (thisTy :: primParamTys) primParamTys)
    proxy =
      export_ <+> proxyName <++> colon <++> pretty "HasIO io =>"
        <++> funType (ps' ++ ifHasThis (thisTy :: proxyParamTys) proxyParamTys) <+> hardline
        <+> proxyName <++> hsep psNames <++> ifHasThis (this <++> equals) equals
        <++> pretty "primIO $" <++> primName <++> hsep (ifHasThis (this :: psNames) psNames)
  in
    if isNil namedPs
      then [prim, proxy]
      else ctorPrimsFor n ps (Just ret) (Just foreignName)

  where
    ifHasThis : Lazy a -> Lazy a -> a
    ifHasThis ifTrue ifFalse = if hasThis then ifTrue else ifFalse

constPrim : {auto lib : Lib} -> String -> String -> DartType -> Doc ()
constPrim owner field ty =
  export_ <+> foreign ("const " ++ owner ++ "." ++ field ++ "," ++ lib.package) <+> hardline
    <+> pretty field <++> colon <++> prettyType ty

enumPrim : {auto lib : Lib} -> String -> String -> Doc ()
enumPrim n f = constPrim n f (NamedType n)

isAssignableFromInstance : String -> String -> Doc ()
isAssignableFromInstance super sub =
  export_ <+> pretty "IsAssignableFrom" <++> pretty super <++> pretty sub <++> pretty "where"

classMemberPrim : {auto lib : Lib} -> Class -> Member -> List (Doc ())
classMemberPrim c m = case m of
  Constructor n ps => ctorPrimsFor n ps Nothing Nothing
  Method f@(Fun n _ _) => functionPrimsFor f ("." ++ n) True
  Static f@(Fun n _ _) => functionPrimsFor f (foreignNameOf (c.name ++ "." ++ n)) False
  FieldMember (Var n ty) => [getter c.name n ty, setter c.name n ty]
  FieldMember (Final n ty) => [getter c.name n ty]
  Extends ty => [isAssignableFromInstance ty c.name]
  Const n ty => [constPrim c.name n ty]

prettyPrims : {auto lib : Lib} -> Declaration -> Maybe (Doc ())
prettyPrims (ClassDecl c) =
  case concatMap (classMemberPrim c) c.members of
    [] => Nothing
    ms => Just $ namespaced c.name (sepByLines ms)
prettyPrims (EnumDecl n fs) =
  Just $ namespaced n (vcat (enumPrim n <$> fs))

primsForLib : LibDef -> List (Doc ())
primsForLib libDef =
  let lib = libDef.lib
  in mapMaybe prettyPrims libDef.declarations

header : Doc () -> Doc ()
header n =
  pretty "||| FFI definitions for the " <++> n <++> "API." <+> hardline
    <+> pretty "module" <++> n <+> hardline <+> hardline
    <+> pretty "import Dart.Core" <+> hardline
    <+> pretty "import Dart.FFI"

export
renderModule : Module -> IO ()
renderModule ffi = do
  let decls = concatMap typeDeclsForLib ffi.libs
  let mutualDecls = pretty "mutual" <+> indented (sepByLines decls)
  let prims = concatMap primsForLib ffi.libs
  let doc = the (Doc ()) (sepByLines (header (pretty ffi.name) :: mutualDecls :: prims))
  let pageWidth = AvailablePerLine 120 1
  let options = record { layoutPageWidth = pageWidth } defaultLayoutOptions
  renderIO $ layoutPretty options $ doc


text:
module India.Language.Core.Types

%default total

export
data Paragraph : Type where

export
data Content : Type where

public export
interface IndianCore (0 decorator : Type -> Type)
                     (0 indian : Type -> Type) | indian where

    content : decorator String -> indian Content
    paragraph : List (indian Content) -> indian Paragraph

max_stars_repo_name: berewt/india

max_issues_repo_name: berewt/india

max_forks_repo_name: berewt/india


text:
module ClosedInt

import Bits
import Signed
import Data.ZZ

%access export
%default total

||| A value in the closed (integer) interval [n,m]
data ClosedInt : (n: ZZ) -> (m: ZZ) -> Type where
  ||| Built with a ZZ
  CI : {n, m: ZZ} -> (x:ZZ) -> ClosedInt n m

-- Consider adding a proof that n <= x <= m using some ZZ proof types, similar
-- to Nat's LTE type. See
-- https://stackoverflow.com/questions/46066253/lte-for-integers-zz
-- for ideas

||| Show instance for printing `ClosedInt`s
Show (ClosedInt n m) where
  show {n} {m} (CI x) = "CI(" ++ show n ++ "," ++ show m ++ ") " ++ show x

||| Eq instance for equality of `ClosedInt`s
Eq (ClosedInt n m) where
  (==) (CI x) (CI y) = x==y

||| Ord instance for ordering of `ClosedInt`s
Ord (ClosedInt n m) where
  compare (CI x) (CI y) = compare x y

||| MinBound instance for generating extremes of `ClosedInt n m`
MinBound (ClosedInt n m) where
  minBound = CI n

||| MaxBound instance for generating extremes of `ClosedInt n m`
MaxBound (ClosedInt n m) where
  maxBound = CI m

||| Generate a `ClosedInt n m` with zeros. The caller must ensure that `n<=0<=m`
zeros : ClosedInt n m
zeros = CI 0

||| Safely create an `Unsigned n` from an Integer using saturation
saturate : ZZ -> ClosedInt n m
saturate x = let tryCI = CI {n} {m} x
             in if tryCI > maxBound then maxBound else
                if tryCI < minBound then minBound else tryCI

--------------------------------------------------------------------------------
-- ClosedInt arithmetic functions
--------------------------------------------------------------------------------

||| Helper function to find high bound of `ClosedInt` scaled by an integer
||| constant
-- public export
multHi : (n, m, a : ZZ) -> ZZ
multHi n m (Pos  k) = m*(Pos  k)
multHi n m (NegS k) = n*(NegS k)

||| Helper function to find low bound of `ClosedInt` scaled by an integer
||| constant
-- public export
multLo : (n, m, a : ZZ) -> ZZ
multLo n m (Pos  k) = n*(Pos  k)
multLo n m (NegS k) = m*(NegS k)

||| Multiply a `ClosedInt` with an integer constant
multConst : ClosedInt n m -> (a : ZZ) -> ClosedInt (multLo n m a) (multHi n m a)
multConst {n}{m} (CI x) a = CI (x*a) {n=multLo n m a} {m=multHi n m a}

||| Add two `ClosedInt`s
add : ClosedInt n m -> ClosedInt a b -> ClosedInt (n+a) (m+b)
add {n}{m}{a}{b} (CI x) (CI y) = CI (x+y) {n=(n+a)} {m=(m+b)}

-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:


text:
module DndPem

%access export
%default total

--- You need this to get the final submit work
public export
AxiomPEM : Type
AxiomPEM = {a : Type} -> {b : Type} -> (a -> b) -> ((a -> Void) -> b) -> b

public export
AxiomDNE : Type
AxiomDNE = {a : Type} -> ((a -> Void) -> Void) -> a

from : AxiomDNE -> AxiomPEM
from dne ri nri = dne $ \bv => bv . nri $ bv . ri

to : AxiomPEM -> AxiomDNE
to pem = pem id . (absurd .)


text:
module PCF

-- Re-export modules that define expressions and
-- evaluation in the simply-typed lambda calculus.
--
-- Also introduce simplified syntax for lambda calculus
-- expressions and utility functions for converting
-- between Idris' built-in natural numbers and natural
-- numbers in the lambda calculus.

import public BigStep
import public Determinism
import public Equivalence
import public Eval
import public Term
import public Step

%access export

------------------------------------------------------------------
-- Begin: SIMPLIFIED SYNTAX FOR EXPRESSIONS IN THE LAMBDA CALCULUS

-- Simplified syntax for abstraction (viz. "Lambda"):
L : Term (s::ctx) t -> Term ctx (s :->: t)
L = TAbs

-- Simplified syntac for application:
infixl 10 @.
(@.) : Term ctx (s :->: t) -> Term ctx s -> Term ctx t
(@.) = TApp

-- More natural syntax for 'Ifz':
syntax "ifz" [e1] "then" [e2] "else" [e3] = TIfz e1 e2 e3;

-- Constants for the variables with the lowest
-- the de-Bruijn indices (i.e. indices 0--2):
v0 : {ctx : Context (S n)} ->
     {auto p : index 0 ctx = t} -> Term ctx t
v0 = TVar 0

v1 : {ctx : Context (S (S n))} ->
     {auto p : index 1 ctx = t} -> Term ctx t
v1 = TVar 1

v2 : {ctx : Context (S (S (S n)))} ->
     {auto p : index 2 ctx = t} -> Term ctx t
v2 = TVar 2

v3 : {ctx : Context (S (S (S (S n))))} ->
     {auto p : index 3 ctx = t} -> Term ctx t
v3 = TVar 3

-- End: SIMPLIFIED SYNTAX FOR EXPRESSIONS IN THE LAMBDA CALCULUS
----------------------------------------------------------------

---------------------------------
-- Begin: EXAMPLES OF EXPRESSIONS

add : Term ctx (TyNat :->: TyNat :->: TyNat)
add = (L (L (TRec v0
                  v1
                  (TSucc v0) )))

mul : Term ctx (TyNat :->: TyNat :->: TyNat)
mul = (L (L (TRec v0
                  TZero
                  (add @.v0 @.v3 ) )))

fact : Term ctx (TyNat :->: TyNat)
fact = (L (TRec v0
                (TSucc TZero)
                (mul @.v0 @.(TSucc v1)) ))

id : Term ctx (t :->: t)
id = L v0

first : Term ctx (t :->: t :->: t)
first = L (L v1)

second : Term ctx (t :->: t :->: t)
second = L (L v0)

two : Term ctx TyNat
two = TSucc $ TSucc TZero

double : Term ctx (TyNat :->: TyNat)
double = mul @.two

-- End: EXAMPLES OF EXPRESSIONS
-------------------------------

----------------------------------------
-- Begin: CONVERSIONS FOR NATURAL NUMBER

natToTerm : Nat -> Term ctx TyNat
natToTerm Z     = TZero
natToTerm (S n) = TSucc (natToTerm n)

termToNat : Term ctx TyNat -> Nat
termToNat TZero     = Z
termToNat (TSucc n) = S (termToNat n)

-- End: CONVERSIONS FOR NATURAL NUMBER
--------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
||| Spec: https://webassembly.github.io/spec/core/valid/conventions.html#contexts
module WebAssembly.Validation.Conventions.Contexts

import WebAssembly.Structure.Types

import Decidable.Equality

-- Definition

public export
record Context where
  constructor MkContext
  types   : List FuncType
  funcs   : List FuncType
  tables  : List TableType
  mems    : List MemType
  globals : List GlobalType
  locals  : List ValType
  labels  : List ResultType
  return  : Maybe ResultType

total public export
prependTypes : List FuncType -> Context -> Context
prependTypes xs = record {types $= ((++) xs)}

total public export
prependFuncs : List FuncType -> Context -> Context
prependFuncs xs = record {funcs $= ((++) xs)}

total public export
prependTables : List TableType -> Context -> Context
prependTables xs = record {tables $= ((++) xs)}

total public export
prependMems : List MemType -> Context -> Context
prependMems xs = record {mems $= ((++) xs)}

total public export
prependGlobals : List GlobalType -> Context -> Context
prependGlobals xs = record {globals $= ((++) xs)}

total public export
prependLocals : List ValType -> Context -> Context
prependLocals xs = record {locals $= ((++) xs)}

total public export
prependLabels : List ResultType -> Context -> Context
prependLabels xs = record {labels $= ((++) xs)}

-- Equality

total public export
lemma_c__types_injective: ((ty1 = ty2) -> Void)
  -> (MkContext ty1 fu1 ta1 me1 gl1 lo1 la1 re1 = MkContext ty2 fu2 ta2 me2 gl2 lo2 la2 re2)
  -> Void
lemma_c__types_injective ty1_not_ty2 Refl = ty1_not_ty2 Refl

total public export
lemma_c__funcs_injective: ((fu1 = fu2) -> Void)
  -> (MkContext ty1 fu1 ta1 me1 gl1 lo1 la1 re1 = MkContext ty2 fu2 ta2 me2 gl2 lo2 la2 re2)
  -> Void
lemma_c__funcs_injective fu1_not_fu2 Refl = fu1_not_fu2 Refl

total public export
lemma_c__tables_injective: ((ta1 = ta2) -> Void)
  -> (MkContext ty1 fu1 ta1 me1 gl1 lo1 la1 re1 = MkContext ty2 fu2 ta2 me2 gl2 lo2 la2 re2)
  -> Void
lemma_c__tables_injective ta1_not_ta2 Refl = ta1_not_ta2 Refl

total public export
lemma_c__mems_injective: ((me1 = me2) -> Void)
  -> (MkContext ty1 fu1 ta1 me1 gl1 lo1 la1 re1 = MkContext ty2 fu2 ta2 me2 gl2 lo2 la2 re2)
  -> Void
lemma_c__mems_injective me1_not_me2 Refl = me1_not_me2 Refl

total public export
lemma_c__globals_injective: ((gl1 = gl2) -> Void)
  -> (MkContext ty1 fu1 ta1 me1 gl1 lo1 la1 re1 = MkContext ty2 fu2 ta2 me2 gl2 lo2 la2 re2)
  -> Void
lemma_c__globals_injective gl1_not_gl2 Refl = gl1_not_gl2 Refl

total public export
lemma_c__locals_injective: ((lo1 = lo2) -> Void)
  -> (MkContext ty1 fu1 ta1 me1 gl1 lo1 la1 re1 = MkContext ty2 fu2 ta2 me2 gl2 lo2 la2 re2)
  -> Void
lemma_c__locals_injective lo1_not_lo2 Refl = lo1_not_lo2 Refl

total public export
lemma_c__labels_injective: ((la1 = la2) -> Void)
  -> (MkContext ty1 fu1 ta1 me1 gl1 lo1 la1 re1 = MkContext ty2 fu2 ta2 me2 gl2 lo2 la2 re2)
  -> Void
lemma_c__labels_injective la1_not_la2 Refl = la1_not_la2 Refl

total public export
lemma_c__return_injective: ((re1 = re2) -> Void)
  -> (MkContext ty1 fu1 ta1 me1 gl1 lo1 la1 re1 = MkContext ty2 fu2 ta2 me2 gl2 lo2 la2 re2)
  -> Void
lemma_c__return_injective re1_not_re2 Refl = re1_not_re2 Refl

-- Decidable Equality

public export
implementation DecEq Context where
  decEq (MkContext ty1 fu1 ta1 me1 gl1 lo1 la1 re1) (MkContext ty2 fu2 ta2 me2 gl2 lo2 la2 re2)
    = case decEq ty1 ty2 of
        No ty1_not_ty2 => No $ lemma_c__types_injective ty1_not_ty2
        Yes Refl       => case decEq fu1 fu2 of
          No fu1_not_fu2 => No $ lemma_c__funcs_injective fu1_not_fu2
          Yes Refl       => case decEq ta1 ta2 of
            No ta1_not_ta2 => No $ lemma_c__tables_injective ta1_not_ta2
            Yes Refl       => case decEq me1 me2 of
              No me1_not_me2 => No $ lemma_c__mems_injective me1_not_me2
              Yes Refl       => case decEq gl1 gl2 of
                No gl1_not_gl2 => No $ lemma_c__globals_injective gl1_not_gl2
                Yes Refl       => case decEq lo1 lo2 of
                  No lo1_not_lo2 => No $ lemma_c__locals_injective lo1_not_lo2
                  Yes Refl       => case decEq la1 la2 of
                    No la1_not_la2 => No $ lemma_c__labels_injective la1_not_la2
                    Yes Refl       => case decEq re1 re2 of
                      No re1_not_re2 => No $ lemma_c__return_injective re1_not_re2
                      Yes Refl       => Yes Refl


text:
-- module Main

data N = Zero | Suc N

-- data Q : N -> N -> Type where

addOne : N -> N
addOne Zero = Suc Zero
addOne (Suc n) = Suc (Suc n)

One : N
One = Suc Zero
Two : N
Two = (Suc (Suc Zero))
Three : N
Three = addOne Two
Four : N
Four = addOne Three
Five : N
Five = addOne Four

add : N -> N -> N
add Zero s = s
add (Suc a) b = add a (Suc b)

test : (n : N) -> Type
test Zero  = N
test (Suc n) = N -> N

foo : (n : N) -> test n
foo Zero  = Three
foo (Suc n) = add n

hej : Char
hej = 'h'

bar : {n : N} -> test n
bar = ?haj

max_stars_repo_name: hjorthjort/IdrisToAgda

max_issues_repo_name: hjorthjort/IdrisToAgda

max_forks_repo_name: hjorthjort/IdrisToAgda


text:
module lib.Library2

export
salute2 : String
salute2 = "Hello, from another Idris library"


text:
module xquant

import public xquant.Core.Types
import public xquant.Core.NonZero
import public xquant.Core.Spectrum
import public xquant.Core.Interpretation
import public xquant.Core.Helicity
import public xquant.Core.Epsilon

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module Main
import Data.Vect
%hide natToFin
%hide cmp
%hide index
%default total

public export
interface Indexable c i where
    eltype : Type
    index' : i -> c -> eltype

implementation Indexable (Vect k t) (Fin k) where
    eltype = t
    index' FZ (x :: xs) = x
    index' (FS k) (x :: xs) = index' k xs

int_vec : Vect 2 Int
int_vec = [2, 3]

cmp : Nat -> Nat -> Ordering
cmp Z Z = EQ
cmp Z _ = LT
cmp _ Z = GT
cmp (S k1) (S k2) = cmp k1 k2

-- -> {auto p: cmp m n = LT}

filter' : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter' p [] = ( 0 ** [] )
filter' p (x :: xs) with (filter' p xs)
   | ( a ** xs' ) = if (p x) then ( (S a) ** x :: xs' ) else ( a ** xs' )


text:
{- Preamble, solution below -}

import Data.Primitives.Views
import System

%default total

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

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

data Fuel = Dry | More (Lazy Fuel)

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

randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                   (seed' `shiftR` 2) :: randoms seed'

arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
  where
    bound : Int -> Int
    bound x with (divides x 12)
      bound ((12 * div) + rem) | (DivBy prf) = abs rem + 1

partial
forever : Fuel
forever = More forever

{- Solution -}

totalREPL : (prompt : String) -> (action : String -> String) -> InfIO
totalREPL prompt action =
   do putStr prompt
      inp <- getLine
      putStr (action inp)
      totalREPL prompt action

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Main

import Effects
import Effect.StdIO
import Effect.Default
import Effect.Msg

import System.Protocol

import Greeter.Example

usage : String
usage = unwords $ intersperse "\n" ["Usage:",
          "\t greeter-app <num>"]

processArgs : (List String) -> Maybe Int
processArgs [x]         = Nothing
processArgs (x::y::Nil) = Just $ cast y
processArgs _           = Nothing

main : IO ()
main = do
    args <- getArgs
    case processArgs args of
      Just i  => doGreeterProcess i
      Nothing => do
        putStrLn "Greeter takes a number"
        putStrLn usage

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

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples