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

import Data.AVL.Dict
import Data.DList
import GRL.Lang.GLang

import XML.DOM

import Edda
import Edda.Writer.Org

import Freyja

import Sif.Types
import Sif.Pattern.Model
import Sif.Pattern.API

%access private

blocks : Maybe EddaBody -> Maybe String
blocks Nothing  = Nothing
blocks (Just b) = Just $ concatMap block b

-- -------------------------------------------------------------------- [ Reqs ]

recoverReq : SifBuilder impl
           -> (d : SifDomain)
           -> Requirement ty
           -> REQUIREMENT impl d
recoverReq bob c r {ty} =
    mkRequirement bob c ty (inlines $ name r) (blocks $ Just (desc r))

-- ----------------------------------------------------------------- [ Problem ]

recoverProblem : SifBuilder impl
              -> (d : SifDomain)
              -> Problem
              -> PROBLEM impl d
recoverProblem bob c p = mkProblem bob c t d rs
  where
    t : String
    t = inlines (name p)

    d : Maybe String
    d = blocks (Just (desc p))

    rs : REQUIREMENTS impl c
    rs = mapDList (\r => recoverReq bob c r) (reqs p)

-- ------------------------------------------------------------------ [ Affect ]

recoverAffect : SifBuilder impl
             -> (d : SifDomain)
             -> Affect
             -> AFFECT impl d
recoverAffect bob c a = mkAffect bob c (cval a) r d
  where
    r : REQUIREMENT impl c
    r = recoverReq bob c (req a)

    d : Maybe String
    d = blocks (desc a)

-- ------------------------------------------------------------------- [ Trait ]

recoverTrait : SifBuilder impl
            -> (d : SifDomain)
            -> Trait ty
            -> TRAIT impl d
recoverTrait bob c t {ty} = mkTrait bob c ty n d (sval t) as
  where
    n : String
    n = inlines (name t)

    d : Maybe String
    d = blocks (Just (desc t))

    as : AFFECTS impl c
    as = map (\a => recoverAffect bob c a) (affects t)

-- ---------------------------------------------------------------- [ Property ]

recoverProperty : SifBuilder impl
               -> (d : SifDomain)
               -> Property
               -> PROPERTY impl d
recoverProperty bob c p = mkProperty bob c n d ts
  where
    n : String
    n = inlines (name p)

    d : Maybe String
    d = blocks (Just (desc p))

    ts : TRAITS impl c
    ts = mapDList (\t => recoverTrait bob c t) (traits p)

-- ---------------------------------------------------------------- [ Solution ]

recoverSolution : SifBuilder impl
               -> (d : SifDomain)
               -> Solution
               -> SOLUTION impl d
recoverSolution bob c s = mkSolution bob c n d ps
  where
    n : String
    n = inlines (name s)

    d : Maybe String
    d = blocks (Just (desc s))

    ps : PROPERTIES impl c
    ps = map (\p => recoverProperty bob c p) (properties s)

-- -------------------------------------------------------------------- [ Main ]

export
fromFreya : SifBuilder impl
         -> PatternDoc
         -> (d ** PATTERN impl d)
fromFreya bob doc {impl} =
    (c ** mkPattern bob c t d p s)
  where
    t : String
    t = inlines (name doc)

    d : Maybe String
    d = blocks (Just (summary doc))

    c' : Context
    c' = (context doc)

    c : SifDomain
    c = MkDomain (inlines $ name c') (blocks (Just (desc c')))

    p : PROBLEM impl c
    p = recoverProblem bob c (problem doc)

    s : SOLUTION impl c
    s = recoverSolution bob c (solution doc)

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


text:
module VNode

import Attributes

public export
NodeRef : Type
NodeRef = AnyPtr

public export
data DOMState = L | V

public export
data NodeType = TagNode | VoidNode | TextNode

public export
record Metadata where
  constructor MkMetadata

initMetadata : Metadata
initMetadata = MkMetadata

mutual
  public export
  data Node : (life:DOMState) -> NodeType -> Type where
    Tag  : String -> List Attribute -> List (DOM life) -> Node life TagNode
    Void : String -> List Attribute                    -> Node life VoidNode
    Text : String                                      -> Node life TextNode

  public export
  data DOM : (life:DOMState) -> Type where
    LiveDOM : Metadata -> Node L nodeType -> NodeRef -> DOM L
    VDOM    : Metadata -> Node V nodeType ->            DOM V

export
defineTag : String -> List Attribute -> List (DOM V) -> DOM V
defineTag name attrs children = VDOM initMetadata (Tag name attrs children)

export
defineVoidTag : String -> List Attribute -> DOM V
defineVoidTag name attrs = VDOM initMetadata (Void name attrs)

export
text : Show a => a -> DOM V
text string = VDOM initMetadata (Text (show string))

ext: idr

max_stars_repo_name: Stinners/alder

max_issues_repo_name: Stinners/alder

max_forks_repo_name: Stinners/alder


text:
module Text.WebIDL.Codegen

import public Data.SortedMap
import public Text.WebIDL.Codegen.Rules as Codegen
import public Text.WebIDL.Codegen.Definitions as Codegen


text:
module Data.Review

import Data.Date
import Data.Either
import Language.JSON
import Language.JSON.Accessors
import Data.Vect

%default total

public export
data State = Approved | Commented | ChangesRequested | Dismissed

public export
record Review where
  constructor MkReview
  submittedAt : Date
  author      : String
  state       : State

export
isAuthor : String -> Review -> Bool
isAuthor login = (== login) . author

parseState : String -> Either String State
parseState "APPROVED"          = Right Approved
parseState "COMMENTED"         = Right Commented
parseState "CHANGES_REQUESTED" = Right Approved
parseState "DISMISSED"         = Right Approved
parseState _ = Left "Failed to parse Review State."

parseDateTime : String -> Either String Date
parseDateTime = maybeToEither "Failed to parse Date" . parseDateTimeString

export
parseReview : JSON -> Either String Review
parseReview json =
 do review <- object json
    [authorLogin, stateStr, submittedAtStr] <- lookupAll ["author", "state", "submitted_at"] review
    author      <- string authorLogin
    state       <- parseState    =<< string stateStr
    submittedAt <- parseDateTime =<< string submittedAtStr
    pure $ MkReview {
        submittedAt
      , author
      , state
      }

||| Parse a single review from a JSON String
export
parseReviewString : String -> Either String Review
parseReviewString =
  (maybeToEither "Failed to parse JSON" . JSON.parse) >=> parseReview

||| Parse a list of reviews from a JSON String
export
parseReviewsString : String -> Either String (List Review)
parseReviewsString =
  (maybeToEither "Failed to parse JSON" . JSON.parse) >=> array parseReview

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
module Control.Lens.Market

import Data.Profunctor

%default total

||| This type is used internally by the 'Control.Lens.Prism' code to
||| provide efficient access to the two parts of a 'Prism'.
public export
data Market a b s t = MkMarket (b -> t) (s -> Either t a)

public export
Market' : Type -> Type -> Type -> Type
Market' a = Market a a

public export
Functor (Market a b s) where
  map f (MkMarket bt seta) = MkMarket (f . bt) (either (Left . f) Right . seta)

public export
Profunctor (Market a b) where
  dimap f g (MkMarket bt seta) = MkMarket (g . bt) (either (Left . g) Right . seta . f)

  lmap f (MkMarket bt seta) = MkMarket bt (seta . f)

  rmap f (MkMarket bt seta) = MkMarket (f . bt) (either (Left . f) Right . seta)

public export
Choice (Market a b) where
  left' (MkMarket bt seta) = MkMarket (Left . bt) $ \sc => case sc of
    Left s => case seta s of
      Left t => Left (Left t)
      Right a => Right a
    Right c => Left (Right c)

  right' (MkMarket bt seta) = MkMarket (Right . bt) $ \cs => case cs of
    Left c => Left (Left c)
    Right s => case seta s of
      Left t => Left (Right t)
      Right a => Right a


text:
describeList : List Int -> String
describeList [] = "Empty"
describeList (x :: xs) = "Non-empty, tail = " ++ show xs

{-describeListEnd : List Int -> String
describeListEnd [] = "Empty"
describeListEnd (xs ++ [x]) = "Non-empty, initial portion" ++ show xs-}

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

describeHelper : (input : List Int) -> (form : ListLast input) -> String
describeHelper [] Empty = "Empty"
describeHelper (xs ++ [x]) (NonEmpty xs x)
  = "Non-empty, initial portion = " ++ show xs

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

{-describeListEnd : List Int -> String
describeListEnd xs = describeHelper xs (listLast xs)-}

describeListEnd : List Int -> String
describeListEnd input with (listLast input)
  describeListEnd [] | Empty = "Empty"
  describeListEnd (xs ++ [x]) | (NonEmpty xs x)
    = "Non-empty, initial portion =" ++ show xs

myReverse : List a -> List a
myReverse input with (listLast input)
  myReverse [] | Empty = []
  myReverse (xs ++ [x]) | (NonEmpty xs x) = x :: myReverse xs


text:
module Meriv.Core.Ast

import Data.List
import Meriv.Core.Util

-- Schema definition

||| Data needed to define an entity
||| of a particular type.
data EntityDec : (ts : List Nat) -> Type where
  MkEntityDec : Nat -> ( t : Nat ) -> { auto p: t `elem` ts = True } -> EntityDec ts

identifier : EntityDec ts -> Nat
identifier (MkEntityDec i _) = i

type : EntityDec ts -> Nat
type (MkEntityDec _ t) = t

Eq (EntityDec ts) where
  (MkEntityDec x y) == (MkEntityDec z w) =
    x == z && y == w

||| Data needed to declare that a type is a
||| subtype of some other type.
data SubtypeDec : (ts : List Nat) -> Type where
  MkSubtypeDec :
      (subtype : Nat)
   -> { auto p1: subtype `elem` ts = True }
   -> (supertype : Nat)
   -> { auto p2: supertype `elem` ts = True }
   -> SubtypeDec ts

Eq (SubtypeDec ts) where
  (MkSubtypeDec x y) == (MkSubtypeDec z w) =
    x == z && y == w

||| Modes for Meriv relational arguments.
data ModeDecl =
    InM
  | OutM
  | BothM

Eq ModeDecl where
  InM   == InM   = True
  OutM  == OutM  = True
  BothM == BothM = True
  _ == _         = False

mutual
  ||| Part of a Meriv Schema needed for typechecking.
  record MvBaseSchema where
    constructor MkBaseSchema
    extends     : Maybe MvBaseSchema
    types'       : List Nat
    subtypes'    : List (SubtypeDec types')
    entities'    : List (EntityDec types')
    relations'   : case extends of
      Just base => List (RelDecl base)
      Nothing   => ()
    rules'       : case extends of
      Just base => List (RuleDecl base)
      Nothing   => ()

    ||| Data needed to declare a Meriv relation.
  record RelDecl (s : MvBaseSchema) where
    constructor MkRelDecl
    name  : String
    argTypes : List (ModeDecl, MvType s)

  Eq (RelDecl s) where
    (MkRelDecl n xs) == (MkRelDecl m ys) =
      xs == ys && n == m

  ||| Data needed to declare a Meriv rule.
  record RuleDecl (s : MvBaseSchema) where
    constructor MkRuleDecl
    -- TODO: Fix this after implementing terms
    clauses : ()

  Eq (RuleDecl s) where
    (MkRuleDecl _) == (MkRuleDecl _) =
      True

  types : (base: MvBaseSchema) -> List Nat
  types base = base.types' ++ maybe [] types base.extends

  -- TODO: I think I need to use a lemma here to supply the proof manually
  subtypes : (base: MvBaseSchema) -> List (SubtypeDec (types base))
  subtypes base = base.subtypes' ++ maybe [] subtypes base.extends

  lemma_extendSubtypes : (p : subsetList xs ys) -> SubtypeDec xs -> SubtypeDec ys
  lemma_extendSubtypes = _

  entities : (base: MvBaseSchema) -> List (EntityDec (types base))
  entities base = base.entities' ++ maybe [] entities base.extends

  relations : (base: MvBaseSchema) -> List (RelDecl base)
  relations base = case base.extends of
    Just parent => parent.relations' ++ maybe [] relations parent.extends
    Nothing     => []

  rules : (base: MvBaseSchema) -> List (RelDecl base)
  rules base = case base.extends of
    Just parent => parent.rules' ++ maybe [] rules parent.extends
    Nothing     => []

  ||| Type of meriv types, given a particular schema.
  data MvType : MvBaseSchema -> Type where
    IntT    : MvType s
    StringT : MvType s
    DoubleT : MvType s
    EntityT :
        (s : MvBaseSchema)
     -> (t : Nat)
     -> { auto p: t `elem` (types s) = True }
     -> MvType s
    RelT :
        (s : MvBaseSchema)
     -> List (ModeDecl, MvType s)
     -> MvType s
    FuncT    :
        MvType s
     -> MvType s
     -> MvType s
    -- RuleT :
    RecordT :
        Set (String, MvType s)
     -> MvType s
    UnionT :
        Set (String, MvType s)
     -> MvType s

  Eq (MvType s) where
    IntT    == IntT    = True
    StringT == StringT = True
    DoubleT == DoubleT = True
    -- (EntityT x y) == (EntityT z w)
    --   = x == z && y == w
    _ == _ = False

  Ord (MvType s) where
    compare x y = EQ

||| Idris type corresponding to a Meriv entity type
||| in a schema.
data Entity : MvBaseSchema -> Nat -> Type where
  MkEntity  :
      (s : MvBaseSchema)
   -> (t : Nat)
   -> { auto p: ((t `elem` types s) = True) }
   -> Entity s t

mutual
  ||| Implementation of a simple record type for Meriv
  data Record : (f : Type -> Type) -> (s : MvBaseSchema) -> (ts: Set (String, MvType s)) -> Type where
    RNil  : Record f s (mkSet [])
    RCons : (label : String) -> MvExpr f s t -> Record f s ts -> Record f s (ts `add` (label,t))

  ||| Implementation of a simple union type.
  data Union : (f : Type -> Type) -> (s : MvBaseSchema) -> (ts: Set (String, MvType s)) -> Type where
    UEmpty  : Union f s (mkSet [])
    UInj : (label : String) -> MvExpr f s t -> { auto p: (label,t) `elem` ts = True } -> Union f s ts

  data VarF : Type -> Type where
    Var    : Nat -> VarF a
    Ground : a   -> VarF a

  data IdF : Type -> Type where
    Id : a -> IdF a

  ||| A Meriv term is a relation with arguments of types ts,
  ||| applied to a list of expressions in order, correpsonding to
  ||| the types ts.
  |||
  ||| Example:
  |||   rel likes: person, food.
  |||   nate: person.
  |||
  |||   likes(nate, X) is a MvTerm.
  |||
  data MvTerm : (f : Type -> Type) -> (s : MvBaseSchema) -> Type where
    MkTerm    :
        { s : MvBaseSchema }
     -> { ts : List (ModeDecl, MvType s) }
     -> MvExpr f s (RelT s ts)
     -> MvExprs f s (map (\(x,y) => y) ts)
     -> MvTerm f s

  record MvClause (s : MvBaseSchema) where
    constructor MkClause
    head : MvTerm VarF s
    body : List (MvTerm VarF s)

  data MvExprs : (f : Type -> Type) -> (s : MvBaseSchema) -> List (MvType s) -> Type where
    NilExprs : MvExprs f s []
    ConsExpr : MvExpr f s t -> MvExprs f s ts -> MvExprs f s (t :: ts)

  data MvExpr : (f : Type -> Type) -> (s : MvBaseSchema) -> MvType s -> Type where
    AppExp    : MvExpr f s (FuncT a b) -> MvExpr f s a -> MvExpr f s b
    -- QueryExp  : (q : Query s rs) -> (MvExprs IdF s rs -> MvExpr IdF s r) -> MvExpr IdF s r
    BaseExp   : f (MvBaseExpr s a) -> MvExpr f s a

  ||| Type of expressions in the Meriv language
  data MvBaseExpr : (s : MvBaseSchema) -> MvType s -> Type where
    IntExp    : Int         -> MvBaseExpr s IntT
    StringExp : String      -> MvBaseExpr s StringT
    DoubleExp : Double      -> MvBaseExpr s DoubleT
    FuncExp   : (MvBaseExpr s a -> MvBaseExpr s b) -> MvBaseExpr s (FuncT a b)
    RelExp    :
          (s : MvBaseSchema)
       -> (identifier: String)
       -> (ts : List (ModeDecl, MvType s))
       -> { auto p: (MkRelDecl identifier ts) `elem` (relations s) = True }
       -> MvBaseExpr s (RelT s ts)
    -- SchemaExp :
    -- RuleExp   :
    --     (s : MvBaseSchema)
    --   ->
    RecordExp : Record s ts -> MvBaseExpr s (RecordT ts)
    UnionExp  : Union s ts  -> MvBaseExpr s (UnionT ts)
    EntityExp :
         (s : MvBaseSchema)
      -> (e : Nat)
      -> (t : Nat)
      -> { auto p1: t `elem` (types s) = True }
      -> { auto p2: MkEntityDec e t `elem` entities s = True }
      -> MvBaseExpr s (EntityT s t)
    InjectEntitySub :
         (s : MvBaseSchema)
      -> (x : Nat) -> { auto p1: x `elem` (types s) = True }
      -> (y : Nat) -> { auto p2: y `elem` (types s) = True }
      -> MvBaseExpr s (EntityT s x)
      -> MvBaseExpr s (EntityT s y)

evaluate : {s : MvBaseSchema} -> {a : MvType s} -> MvExpr IdF s a -> MvExpr IdF s a
evaluate (AppExp (FuncExp f) x) = evaluate $ f x
evaluate x = x

||| Information needed to declare an implcit conversion
||| of Meriv types.
record ConversionDec (s : MvBaseSchema) where
  constructor MkConversionDec
  fromType   : MvType s
  toType     : MvType s
  conversion : MvBaseExpr s fromType -> MvBaseExpr s toType

Eq (ConversionDec s) where
  (MkConversionDec x y _) == (MkConversionDec z w _) =
    x == z && y == w

||| A full schema for the meriv language.
record MvSchema where
  constructor MkSchema
  base  : MvBaseSchema
  conversions : List (ConversionDec base)

||| Evidential subtype relation for Meriv types.
data Subtype : (s : MvSchema) -> MvType (base s) -> MvType (base s) -> Type where
  -- Any type is a sub-type of itself.
  ReflSub  : Subtype s t t
  -- Subtyping is a transitive relation.
  TransSub : {x,y,z : _ } -> Subtype s x y -> Subtype s y z -> Subtype s x z
  -- Subtyping can be preformed by an implicit conversion.
  Inject   :
      (s : MvSchema)
   -> (x : MvType (base s))
   -> (y : MvType (base s))
   -> (z : MvBaseExpr (base s) x -> MvBaseExpr (base s) y)
   -> { auto p: (MkConversionDec x y z) `elem` conversions s = True }
   -> Subtype s x y
  -- Subtyping can be preformed by specifyin a subtype for
  -- an entity type.
  EntitySub :
      (s : MvSchema)
   -> (x : Nat)
   -> (y : Nat)
   -> { auto p1: x `elem` types (base s) = True }
   -> { auto p2: y `elem` types (base s) = True }
   -> { auto p3: MkSubtypeDec x y `elem` subtypes (base s) = True }
   -> Subtype s (EntityT (base s) x {p=p1}) (EntityT (base s) y {p=p2})

||| Helper function to preform a conversion from a subtype to it's supertype,
||| given evidence (Subtype s x y) that a term is a subtype of another term
||| according to the given schema.
convertTerm :
      { s: MvSchema }
   -> { x, y: _ }
   -> Subtype s x y
   -> MvBaseExpr (base s) x
   -> MvBaseExpr (base s) y
convertTerm ReflSub
  = \t => t
convertTerm (TransSub t1 t2)
  = convertTerm t2 . convertTerm t1
convertTerm (Inject s x y f)
  = f
convertTerm (EntitySub s x y)
  = InjectEntitySub (base s) x y

-- Examples

-- myType : Nat
-- myType = 0

-- schema : MvBaseSchema
-- schema = MkBaseSchema Nothing [myType] [] [MkEntityDec 0 myType, MkEntityDec 1 myType] () []

-- Note: For some reason, idris2 doesn't like it when I put variables in types -- it treats them like a hole.
-- exampleTerm : MvExpr (MkBaseSchema Nothing [myType] [] [MkEntityDec 0 myType, MkEntityDec 1 myType] () []) (MkBaseSchema Nothing [myType] [] [MkEntityDec 0 myType, MkEntityDec 1 myType] () [])
-- exampleTerm = EntityExp schema 1 0

(+) : MvExpr s (FuncT IntT (FuncT IntT IntT))
(+) = FuncExp (\(IntExp x) => FuncExp $ \(IntExp y) => IntExp $ x + y)

main : IO ()
main = do
  let (IntExp x) = the (MvExpr (MkBaseSchema [] [] []) IntT) $
     evaluate $ AppExp (AppExp (+) (IntExp 2)) (IntExp 2)
  printLn x

max_stars_repo_name: Sintrastes/meriv-idr-prototype

max_issues_repo_name: Sintrastes/meriv-idr-prototype

max_forks_repo_name: Sintrastes/meriv-idr-prototype


text:
import Data.Vect

-- Page 160

-- Exercise 1
Matrix : Nat -> Nat -> Type
Matrix n m = Vect n (Vect m Double)

-- Exercise 2
data Format = Number Format
            | Str Format
            | Lit String Format
            | Ch Format
            | Dbl Format
            | End

PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Str fmt) = (str : String) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType (Ch fmt) = (c : Char) -> PrintfType fmt
PrintfType (Dbl fmt) = (d : Double) -> PrintfType fmt
PrintfType End = String

printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
printfFmt (Ch fmt) acc = \c => printfFmt fmt (acc ++ show c)
printfFmt (Dbl fmt) acc = \d => printfFmt fmt (acc ++ show d)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt End acc = acc

toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: 'c' :: chars) = Ch (toFormat chars)
toFormat ('%' :: 'f' :: chars) = Dbl (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
                             Lit lit chars' => Lit (strCons c lit) chars'
                             fmt => Lit (strCons c "") fmt
printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""

-- Exercise 3
TupleVect : Nat -> Type -> Type
TupleVect Z e = ()
TupleVect (S k) e = (e, TupleVect k e)

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

-- Page 180
-- See file `week7_1_p_180.idr`

-- Page 193

data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

-- Exercise 1

Eq Shape where
  (==) (Triangle a b) (Triangle a' b') = (a == a' && b == b')
  (==) (Rectangle a b) (Rectangle a' b') = (a == a' && b == b')
  (==) (Circle r) (Circle r') = (r == r')
  (==) _ _ = False

-- Exercise 2

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

Ord Shape where
  compare s1 s2 = compare (area s1) (area s2)

-- testShapes : List Shape
-- testShapes = [Circle 3, Triangle 3 9, Rectangle 2 6, Circle 4,
--               Rectangle 2 7]

-- Page 199

-- Exercise 1
data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)

eval : (Neg num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y

Num ty => Num (Expr ty) where
    (+) = Add
    (*) = Mul
    fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
    negate x = 0 - x
    (-) = Sub

Show t => Show (Expr t) where
  show (Val x) = show x
  show (Add x y) = "(" ++ (show x) ++ " + " ++ (show y) ++ ")"
  show (Sub x y) = "(" ++ (show x) ++ " - " ++ (show y) ++ ")"
  show (Mul x y) = "(" ++ (show x) ++ " * " ++ (show y) ++ ")"
  show (Div x y) = "(" ++ (show x) ++ " / " ++ (show y) ++ ")"

-- show (the (Expr _) (6 + 3 * 12))
-- show (the (Expr _) (6 * 3 + 12))

-- Exercise 2
(Eq num, Integral num, Neg num) => Eq (Expr num) where
    (==) x y = eval x == eval y

-- Exercise 3
(Integral num, Neg num) => Cast (Expr num) num where
  cast x = eval (x)

-- Page 206

-- Exercise 1
Functor Expr where
  map f (Val x) = Val (f x)
  map f (Add x y) = Add (map f x) (map f y)
  map f (Sub x y) = Sub (map f x) (map f y)
  map f (Mul x y) = Mul (map f x) (map f y)
  map f (Div x y) = Div (map f x) (map f y)

-- Exercise 2
-- See file `week7_1_p_206_ex_2.idr`

max_stars_repo_name: JnxF/advanced-software-analysis

max_issues_repo_name: JnxF/advanced-software-analysis

max_forks_repo_name: JnxF/advanced-software-analysis


text:
module OCaml.Lwt

import OCaml.IO

%default total
%access public export

%lib malfunction "lwt"

Lwt : Type -> Type
Lwt = Abstr1

lwtReturn : {auto ta : OCaml_Types a} -> a -> OCaml_IO (Lwt a)
lwtReturn {a} x = ocamlCall "Lwt.return" (a -> OCaml_IO (Lwt a)) x

lwtBind : {auto ta : OCaml_Types a} ->
          Lwt a ->
          (a -> OCaml_IO (Lwt b)) ->
          OCaml_IO (Lwt b)
lwtBind {a}{b} p f =
  ocamlCall "Lwt.bind" (Lwt a -> (a -> OCaml_IO (Lwt b)) -> OCaml_IO (Lwt b)) p f

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:
-- ------------------------------------------------------------- [ Daytime.idr ]
--
-- This RFC specifies a standard for the ARPA Internet community.
-- Hosts on the ARPA Internet that choose to implement a Daytime
-- Protocol are expected to adopt and implement this standard.
--
-- A useful debugging and measurement tool is a daytime service. A
-- daytime service simply sends a the current date and time as a
-- character string without regard to the input.
--
-- There is no specific syntax for the daytime.  It is recommended
-- that it be limited to the ASCII printing characters, space,
-- carriage return, and line feed.  The daytime should be just one
-- line. One popular syntax is:
--
-- ```
-- Weekday, Month Day, Year Time-Zone
-- ```
--
-- Example:
---
--- ```
--- Tuesday, February 22, 1982 17:37:43-PST
--- ```
--
-- --------------------------------------------------------------------- [ EOH ]
module RFC.Daytime

import Effects

import Effect.Default
import Effect.StdIO

import System.Protocol

import RFC.Utils

||| A daytime service simply sends a the current date and time as a
||| character string without regard to the input.
daytime : Protocol ['Client, 'Server] ()
daytime = do
    'Client ==> 'Server | Maybe String
    'Server ==> 'Client | Either String DayTime
    Done

-- --------------------------------------------------------------------- [ 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


text:
module Main

import Effects
import Effect.StdIO
sayHello : Eff () [STDIO]
sayHello =putStrLn "Hello World"

main : IO()
main = run sayHello

max_stars_repo_name: dannypsnl/languages-learn

max_issues_repo_name: dannypsnl/languages-learn

max_forks_repo_name: dannypsnl/languages-learn


text:
module Data.Bounded

%default total

public export
interface Ord b => MinBound b where
  ||| The lower bound for the type
  minBound : b

public export
interface Ord b => MaxBound b where
  ||| The upper bound for the type
  maxBound : b

public export %inline
MinBound Bits8 where
  minBound = 0x0

public export %inline
MaxBound Bits8 where
  maxBound = 0xff

public export %inline
MinBound Bits16 where
  minBound = 0x0

public export %inline
MaxBound Bits16 where
  maxBound = 0xffff

public export %inline
MinBound Bits32 where
  minBound = 0x0

public export %inline
MaxBound Bits32 where
  maxBound = 0xffffffff

public export %inline
MinBound Bits64 where
  minBound = 0x0

public export %inline
MaxBound Bits64 where
  maxBound = 0xffffffffffffffff

public export %inline
MinBound Int8 where
  minBound = (- 0x80)

public export %inline
MaxBound Int8 where
  maxBound = 0x7f

public export %inline
MinBound Int16 where
  minBound = (- 0x8000)

public export %inline
MaxBound Int16 where
  maxBound = 0x7fff

public export %inline
MinBound Int32 where
  minBound = (- 0x80000000)

public export %inline
MaxBound Int32 where
  maxBound = 0x7fffffff

public export %inline
MinBound Int64 where
  minBound = (- 0x8000000000000000)

public export %inline
MaxBound Int64 where
  maxBound = 0x7fffffffffffffff

public export %inline
MinBound Int where
  minBound = (- 0x8000000000000000)

public export %inline
MaxBound Int where
  maxBound = 0x7fffffffffffffff


text:
module Minecraft.Core.Block.Break

import Minecraft.Core
import public Minecraft.Core.Block
import public Minecraft.Data.Type.As

%default total

public export
interface Block self => Break (self : Type) where
  breakBlk : self -> List (As Entity)

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Sixel.Helpers

import Data.Buffer

import Sixel.Library
import Sixel.Symbols
import Sixel.Allocator

%foreign (sixel "sixel_helper_get_additional_message")
sixel_helper_get_additional_message : String

%foreign (sixel "sixel_helper_set_additional_message")
sixel_helper_set_additional_message : String -> ()

%foreign (sixel "sixel_helper_format_error")
sixel_helper_format_error : Int -> String

export %inline
getAdditionalMessage : String
getAdditionalMessage = sixel_helper_get_additional_message

export %inline
setAdditionalMessage : String -> IO ()
setAdditionalMessage = pure . sixel_helper_set_additional_message

export %inline
format : Status -> String
format (MkStatus s) = sixel_helper_format_error s

max_stars_repo_name: Kaiepi/id-sixel

max_issues_repo_name: Kaiepi/id-sixel

max_forks_repo_name: Kaiepi/id-sixel


text:
module WebAssembly.Validation.Modules.StartFunction

import WebAssembly.Structure
import WebAssembly.Validation.Conventions
import WebAssembly.Validation.Types

||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#start-function)
|||
||| ```
||| C.funcs[x] = [] -> []
||| ---------------------
||| C ⊢ {func x} ok
||| ```
public export
data ValidStart : Context -> Start -> Type where
  MkValidStart : (c : Context)
              -> (x : FuncIdx)
              -> {auto in_bounds: InBounds x (funcs c)}
              -> (index x (funcs c) = ([] ->> []))
              -> ValidStart c (MkStart x)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
import Text.Readline

testComplete : String -> Int -> IO (Maybe String)
testComplete text 0 = pure $ Just "hamster"
testComplete text 1 = pure $ Just "bar"
testComplete text st = pure Nothing

loop : IO ()
loop = do Just x <- readline "> "
               | Nothing => putStrLn "EOF"
          putStrLn x
          when (x /= "") $ addHistory x
          if x /= "quit"
             then loop
             else putStrLn "Done"

main : IO ()
main = do setCompletionFn testComplete
          loop


text:
h : Monad m => Int -> m (Maybe Int)

f : Int -> Maybe Int

g : Monad m => m Int
g = do
  Just y <- h 5
    | Nothing => pure 0
  let Just x = f 4
    | Nothing => pure 4
  pure $ x + y

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
> module Functor.Properties

> import Functor.Predicates

> %default total
> %access public export
> %auto_implicits off

* Monotonicity and naturality:

> ||| Composing a monotone measure with a natural transformation
> ||| yields a monotone measure
> monotoneNaturalLemma: {B, C : Type} -> {F : Type -> Type} -> (Functor F) =>
>                       (LTE_B : B -> B -> Type) ->
>                       (LTE_C : C -> C -> Type) ->
>                       (measure : F B -> C) ->
>                       Monotone LTE_B LTE_C measure ->
>                       (t : {A : Type} -> F A -> F A) ->
>                       Natural t ->
>                       Monotone LTE_B LTE_C (measure . t)
> monotoneNaturalLemma LTE_B LTE_C m mm t nt = mmt where
>   mmt f g p x = let s1 = mm f g p (t x) in
>                 let s2 = replace {P = \ X => m X `LTE_C` m (map g (t x))} (sym (nt f x)) s1 in
>                 let s3 = replace {P = \ X => m (t (map f x)) `LTE_C` m X} (sym (nt g x)) s2 in
>                 s3

> {-
> monotoneNaturalLemma {B} {C} {F} LTE_B LTE_C m mm t nt = mmt where
>   mmt : Monotone {B} {C} {F} LTE_B LTE_C (m . (t {A = B}))
>   mmt = ?lala
>   mmt A f g p x = s3 where
>     s1 : m (map f (t A x)) `LTE_C` m (map g (t A x))
>     s1 = mm A f g p (t A x)
>     s2 : m ((t B) (map f x)) `LTE_C` m (map g (t A x))
>     s2 = replace {P = \ X => m X `LTE_C` m (map g (t A x))} (sym (nt f x)) s1
>     s3 : m ((t B) (map f x)) `LTE_C` m ((t B) (map g x))
>     s3 = replace {P = \ X => m ((t B) (map f x)) `LTE_C` m X} (sym (nt g x)) s2
> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
-- Additional FFI help for more interesting C types
-- Some assumptions are made about the existence of this module in
-- Compiler.CompileExpr

module System.FFI

export
data Struct : String -> -- C struct name
              List (String, Type) -> -- field names and types
              Type where

public export
data FieldType : String -> Type -> List (String, Type) -> Type where
     First : FieldType n t ((n, t) :: ts)
     Later : FieldType n t ts -> FieldType n t (f :: ts)

%extern
prim__getField : {s : _} -> forall fs, ty .
                         Struct s fs -> (n : String) ->
                         FieldType n ty fs -> ty
%extern
prim__setField : {s : _} -> forall fs, ty .
                         Struct s fs -> (n : String) ->
                         FieldType n ty fs -> ty -> PrimIO ()

public export %inline
getField : {s : _} -> Struct s fs -> (n : String) ->
           {auto fieldok : FieldType n ty fs} -> ty
getField s n = prim__getField s n fieldok

public export %inline
setField : {s : _} -> Struct s fs -> (n : String) ->
           {auto fieldok : FieldType n ty fs} -> ty -> IO ()
setField s n val = primIO (prim__setField s n fieldok val)


text:
module Client.Action.CacheDeps

import Data.List
import Inigo.Async.Base
import Inigo.Async.FS
import Inigo.Async.Promise
import Inigo.Package.Package
import Inigo.Package.JSON
import Inigo.Paths
import Language.JSON
import SemVar

export
writeDepCache : List (String, Package) -> Promise ()
writeDepCache pkgWithSrcs = do
    fs_mkdir True inigoDepDir
    fs_writeFile inigoDepPkgCache json
  where
    encodeWithSrc : (String, Package) -> JSON
    encodeWithSrc (src, pkg) = JObject
        [ ("src", JString src)
        , ("package", encodePackage pkg)
        ]
    json : String
    json = show $ JArray $ encodeWithSrc <$> pkgWithSrcs

export
readDepCache : Promise (List (String, Package))
readDepCache = do
    inp <- fs_readFile inigoDepPkgCache
    let Just (JArray json) = parse inp
        | _ => reject "Corrupt dependency cache (\{inigoDepPkgCache}) (not an array)"
    let Just pkgWithSrc = the (Maybe (List (String, Package))) $ traverse decodeWithSrc json
        | _ => reject "Corrupt dependency cache (\{inigoDepPkgCache}) (couldn't parse packages)"
    pure pkgWithSrc
  where
    decodeWithSrc : JSON -> Maybe (String, Package)
    decodeWithSrc (JObject kvs) = do
        JString src <- lookup "src" kvs
            | _ => Nothing
        pkg <- lookup "package" kvs >>= parsePackage
        pure (src, pkg)
    decodeWithSrc _ = Nothing

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Idrlisp.Lexer

import Text.Lexer

%default total

escapeChars : List (Char, Char)
escapeChars =
  [ ('\\', '\\')
  , ('t', '\t')
  , ('n', '\n')
  , ('"', '"')
  ]

public export
data Token
  = AMB
  | LPAREN
  | RPAREN
  | LBRACK
  | RBRACK
  | DOT
  | TRUE
  | FALSE
  | QUOTE
  | QUASIQUOTE
  | UNQUOTE
  | UNQUOTE_SPLICING
  | NUM Double
  | SYM String
  | STR String

export
Eq Token where
  (==) AMB AMB = True
  (==) LPAREN LPAREN = True
  (==) RPAREN RPAREN = True
  (==) LBRACK LBRACK = True
  (==) RBRACK RBRACK = True
  (==) DOT DOT = True
  (==) TRUE TRUE = True
  (==) FALSE FALSE = True
  (==) QUOTE QUOTE = True
  (==) QUASIQUOTE QUASIQUOTE = True
  (==) UNQUOTE UNQUOTE = True
  (==) UNQUOTE_SPLICING UNQUOTE_SPLICING = True
  (==) (NUM x) (NUM y) = x == y
  (==) (SYM x) (SYM y) = x == y
  (==) (STR x) (STR y) = x == y
  (==) _ _ = False

export
Show Token where
  show AMB = "AMB"
  show LPAREN = "LPAREN"
  show RPAREN = "RPAREN"
  show LBRACK = "LBRACK"
  show RBRACK = "RBRACK"
  show DOT = "DOT"
  show TRUE = "TRUE"
  show FALSE = "FALSE"
  show QUOTE = "QUOTE"
  show QUASIQUOTE = "QUASIQUOTE"
  show UNQUOTE = "UNQUOTE"
  show UNQUOTE_SPLICING = "UNQUOTE_SPLICING"
  show (NUM x) = "NUM " ++ show x
  show (SYM x) = "SYM " ++ x
  show (STR x) = "STR " ++ show x

tokenMap : TokenMap Token
tokenMap =
  [ (amb, const AMB)
  , (is '(', const LPAREN)
  , (is ')', const RPAREN)
  , (is '[', const LBRACK)
  , (is ']', const RBRACK)
  , (is '.', const DOT)
  , (exact "#t", const TRUE)
  , (exact "#f", const FALSE)
  , (is '\'', const QUOTE)
  , (is '`', const QUASIQUOTE)
  , (exact ",@", const UNQUOTE_SPLICING)
  , (is ',', const UNQUOTE)
  , (num, NUM . cast)
  , (sym, SYM)
  , (str, STR . unstr)
  ]
  where
    amb : Lexer
    amb = some (spaces <|> lineComment (is ';'))

    num : Lexer
    num = opt (oneOf "-+") <+> digits <+> opt frac <+> opt exp
      where
        frac = is '.' <+> opt digits
        exp = oneOf "eE" <+> opt (oneOf "-+") <+> digits

    sym : Lexer
    sym = (alpha <|> special) <+> many (alpha <|> digit <|> special)
      where
        special : Lexer
        special = some $ oneOf "!$%&*+-/:<=>?@^_~"

    str : Lexer
    str = is '"' <+> many (escapeSequence <|> isNot '"') <+> is '"'
      where
        escapeSequence : Lexer
        escapeSequence = escape '\\' $ oneOf $ pack $ map fst escapeChars

    unstr : String -> String
    unstr = pack . unescape . unquote . unpack
      where
        unquote : List Char -> List Char
        unquote ('"' :: s@(_ :: _)) = init s
        unquote s = s

        unescape : List Char -> List Char
        unescape ('\\' :: c :: s) = fromMaybe c (lookup c escapeChars) :: unescape s
        unescape (c :: s) = c :: unescape s
        unescape [] = []

export
lex : String -> Either (Int, Int, String) (List Token)
lex str =
  case lex tokenMap str of
    (tokens, (l, c, "")) => Right (mapMaybe dropAmb tokens)
    (_, fail) => Left fail
  where
    dropAmb : TokenData Token -> Maybe Token
    dropAmb t =
      case tok t of
        AMB => Nothing
        x => Just x

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
redDim : Vector (x1::x2::xs) t ->
         Vector (x1*x2::xs) t
redDim [] = []
redDim (v::vs) = v ++ redDim vs

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
module Main

import TestLib
import Test.Golden
import System
import Postgres

tests : TestPool
tests = MkTestPool "postgres" [] Nothing [
  "expected_type_query"
]

exitError : String -> IO ()
exitError err = do
  putStrLn err
  exitFailure

main : IO ()
main = do
  Right config <- getTestConfig
    | Left err => exitError err
  True <- withTestDB {setup=True} $ do
            liftIO' . putStrLn $ "Testing against " ++ config.databaseUrl
            dbSetup
    | False => exitError "Cannot run tests without test database."
  runner [tests]

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: CC0-1.0

module Lexer

import Text.Lexer

import Tester

import Language.TOML.Lexer
import Language.TOML.Tokens

tokenize : Test
tokenize = test "tokenize" $ do
    Just res <- pure $ lexTOML "hello world\n"
        | Nothing => throwE "lexer error"
    assertEq (length res) 4

export
tests : List Test
tests = [tokenize]

max_stars_repo_name: tiatomee/toml-idr

max_issues_repo_name: tiatomee/toml-idr

max_forks_repo_name: tiatomee/toml-idr


text:
import DataStore
import DescribeList
import DescribeList2
import IsSuffix
import MergeSort
import MergeSortView
import Reverse
import ReverseSnoc
import Shape
import Shape_abs
import SnocList
import TestStore


text:
module Lists

%default total

data NatProd : Type where
    Pair : Nat -> Nat -> NatProd

syntax "(" [x] "," [y] ")" = Pair x y

fst : (p : NatProd) -> Nat
fst (Pair x y) = x

snd : (p : NatProd) -> Nat
snd (Pair x y) = y

swap : (p : NatProd) -> NatProd
swap (x, y) = (y, x)

surjective_pairing : (n, m : Nat) -> (n, m) = (fst (n, m), snd(n, m))
surjective_pairing n m = Refl

surjective_pairing_stuck : (p : NatProd) -> p = (fst p, snd p)
surjective_pairing_stuck (Pair k j) = Refl

snd_fst_is_swap : (p : NatProd) -> (snd p, fst p) = swap p
snd_fst_is_swap (Pair k j) = Refl

fst_swap_is_snd : (p : NatProd) -> fst (swap p) = snd p
fst_swap_is_snd (Pair k j) = Refl

data NatList : Type where
    Nil : NatList
    Cons : Nat -> NatList -> NatList

(::) : Nat -> NatList -> NatList
(::) n l = Cons n l

mylist : NatList
mylist = [1, 2, 3]

repeat : (n, count : Nat) -> NatList
repeat n Z = Nil
repeat n (S k) = n :: repeat n k

length : (l : NatList) -> Nat
length [] = Z
length (Cons k x) = S (length x)

append : (l1, l2 : NatList) -> NatList
append Nil l2 = l2
append (Cons h t) l2 = h :: append t l2

(++) : NatList -> NatList -> NatList
(++) = append

test_append1 : ([1, 2, 3] ++ [4, 5]) = [1, 2, 3, 4, 5]
test_append1 = Refl

test_append2 : (Nil ++ [4, 5]) = [4, 5]
test_append2 = Refl

test_append3 : [1, 2, 3] ++ [] = [1, 2, 3]
test_append3 = Refl

hd : (default : Nat) -> (l : NatList) -> Nat
hd default Nil = default
hd default (Cons h t) = h

tl : (l : NatList) -> NatList
tl Nil = Nil
tl (Cons h t) = t

test_hd1 : hd 0 [1, 2, 3] = 1
test_hd1 = Refl

test_hd2 : hd 0 [] = 0
test_hd2 = Refl

test_tl : tl [1, 2, 3] = [2, 3]
test_tl = Refl

non_zeros : (l : NatList) -> NatList
non_zeros [] = Nil
non_zeros (Cons Z x) = non_zeros x
non_zeros (Cons k x) = k :: non_zeros x

test_nonzeros : non_zeros [0, 1, 0, 2, 3, 0, 0] = [1, 2, 3]
test_nonzeros = Refl

oddmembers : (l : NatList) -> NatList
oddmembers [] = Nil
oddmembers (Cons k x) =
    if modNatNZ k 2 SIsNotZ == 0
        then oddmembers x
        else k :: oddmembers x

test_oddmembers : oddmembers [0, 1, 0, 2, 3, 0, 0] = [1, 3]
test_oddmembers = Refl

count_oddmembers : (l : NatList) -> Nat
count_oddmembers = length . oddmembers

test_count_oddmembers : count_oddmembers [1, 0, 3, 1, 4, 5] = 4
test_count_oddmembers = Refl

alternate : (l1, l2 : NatList) -> NatList
alternate [] l2 = l2
alternate l1 [] = l1
alternate (Cons k x) (Cons j y) = k :: j :: alternate x y

test_alternate1 : alternate [1, 2, 3] [4, 5, 6] = [1, 4, 2, 5, 3, 6]
test_alternate1 = Refl
test_alternate2 : alternate [1] [4, 5, 6] = [1, 4, 5, 6]
test_alternate2 = Refl
test_alternate3 : alternate [1, 2, 3] [4] = [1, 4, 2, 3]
test_alternate3 = Refl
test_alternate4 : alternate [] [20, 30] = [20, 30]
test_alternate4 = Refl

Bag : Type
Bag = NatList

count : (v : Nat) -> (s : Bag) -> Nat
count v [] = Z
count Z (Cons Z x) = S (count Z x)
count v@(S k) (Cons (S j) x) = count k [j] + count v x
count v (Cons k x) = count v x

test_count : count 1 [1, 2, 3, 1, 4, 1] = 3
test_count = Refl
test_count2 : count 6 [1, 2, 3, 1, 4, 1] = 0
test_count2 = Refl

sum : Bag -> Bag -> Bag
sum = append

test_sum1 : count 1 (sum [1, 2, 3] [1, 4, 1]) = 3
test_sum1 = Refl

add : (v : Nat) -> (s : Bag) -> Bag
add = (::)

test_add1 : count 1 (add 1 [1, 4, 1]) = 3
test_add1 = Refl
test_add2 : count 5 (add 1 [1, 4, 1]) = 0
test_add2 = Refl

member : (v : Nat) -> (s : Bag) -> Bool
member v [] = False
member v (Cons k x) =
    if k == v
        then True
        else member v x

test_member1 : member 1 [1, 4, 1] = True
test_member1 = Refl
test_member2 : member 2 [1, 4, 1] = False
test_member2 = Refl

remove_one : (v : Nat) -> (s : Bag) -> Bag
remove_one v [] = []
remove_one v (Cons k x) =
    if k == v
        then x
        else k :: remove_one v x

test_remove_one1 : count 5 (remove_one 5 [2, 1, 5, 4, 1]) = 0
test_remove_one1 = Refl
test_remove_one2 : count 5 (remove_one 5 [2, 1, 4, 1]) = 0
test_remove_one2 = Refl
test_remove_one3 : count 4 (remove_one 5 [2, 1, 5, 4, 1, 4]) = 2
test_remove_one3 = Refl
test_remove_one4 : count 5 (remove_one 5 [2, 1, 5, 4, 5, 1, 4]) = 1
test_remove_one4 = Refl

remove_all : (v : Nat) -> (s : Bag) -> Bag
remove_all v [] = []
remove_all v (Cons k x) =
    if k == v
        then remove_all v x
        else k :: remove_all v x

test_remove_all1 : count 5 (remove_all 5 [2, 1, 5, 4, 1]) = 0
test_remove_all1 = Refl
test_remove_all2 : count 5 (remove_all 5 [2, 1, 4, 1]) = 0
test_remove_all2 = Refl
test_remove_all3 : count 4 (remove_all 5 [2, 1, 5, 4, 1, 4]) = 2
test_remove_all3 = Refl
test_remove_all4 : count 5 (remove_all 5 [2, 1, 5, 4, 5, 1, 4, 5, 1, 4]) = 0
test_remove_all4 = Refl

subset : (s1 : Bag) -> (s2 : Bag) -> Bool
subset [] s2 = True
subset (Cons k x) s2 =
    let
        contains_elem_of_s1 = member k s2
        s2' = remove_one k s2
    in
        contains_elem_of_s1 && subset x s2'

test_subset1 : subset [1, 2] [2, 1, 4, 1] = True
test_subset1 = Refl

test_subset2 : subset [1, 2, 2] [2, 1, 4, 1] = False
test_subset2 = Refl

add_succ_count : (v : Nat) -> (s : Bag) -> count v (add v s) = S (count v s)
add_succ_count Z s = Refl
add_succ_count (S k) [] = rewrite add_succ_count k [] in Refl
add_succ_count (S k) (Cons j x) = rewrite add_succ_count k [] in Refl

ble_n_Sn : (n : Nat) -> n `lte` (S n) = True
ble_n_Sn Z = Refl
ble_n_Sn (S k) = rewrite ble_n_Sn k in Refl

count_member_nonzero : (s : Bag) -> 1 `lte` count 1 (1 :: s) = True
count_member_nonzero s = Refl

remove_decreases_count : (s : Bag) -> lte (count 0 (remove_one 0 s)) (count 0 s) = True
remove_decreases_count [] = Refl
remove_decreases_count (Cons Z x) = rewrite ble_n_Sn (count 0 x) in Refl
remove_decreases_count (Cons (S k) x) = rewrite remove_decreases_count x in Refl

bag_count_sum : (s1, s2 : Bag) -> count 0 (sum s1 s2) = (count 0 s1) + (count 0 s2)
bag_count_sum [] s2 = Refl
bag_count_sum (Cons Z x) s2 = rewrite bag_count_sum x s2 in Refl
bag_count_sum (Cons (S k) x) s2 = rewrite bag_count_sum x s2 in Refl


text:
foo : {p,q  : Nat -> Type} -> p x
foo = ?a

  where

    helper : {p2 : Nat -> Nat -> Type} -> p2 y 0
    helper = ?b

    helper1 : {p2 : Nat -> Nat -> Type} -> (y : Nat) -> p2 y 0
    helper1 = ?c

    helper2 : (y : Nat) -> {p2 : Nat -> Nat -> Type} -> p2 y 0
    helper2 = ?d

    -- introduce the ones after explicitly bound variables though
    helper3 : (y : Nat) -> {p2 : Nat -> Nat -> Type} -> p2 y 0
    helper3 y = ?e


text:
transport : (0 eq : a === b) -> a -> b
transport eq x = rewrite sym eq in x

nested : (0 _ : a === b) -> (0 _ : b === c) -> a === c
nested eq1 eq2 =
  rewrite eq1 in
    rewrite eq2 in
      let prf : c === c := Refl in
      prf


text:
module AlterningBitsOracle

import Data.Nat
import Unitary
import Lemmas

%default total

|||Alternating bits oracle : checks if the input alternates, i-e does not have a pair of adjacent qubits in stae 00 or 11

lemmaFlip : (i : Nat) -> (k : Nat) -> (p : S (S i) < k = True) -> i < k = True
lemmaFlip 0 k p = lemmaCompLT0 k 2
lemmaFlip (S i) (S k) p = lemmaFlip i k p

lemmaSolve : (n : Nat) -> n < S (S n) = True
lemmaSolve 0 = Refl
lemmaSolve (S k) = lemmaSolve k

flip : (n : Nat) -> (i : Nat) -> {auto prf : i < S (S n) = True} -> Unitary (S (S n))
flip n 0 = X 0 IdGate
flip n 1 = X 1 IdGate
flip n (S (S i)) = X (S (S i)) (flip n i {prf = lemmaFlip i (S (S n)) prf})

export
solve : (n : Nat) -> Unitary ((S (S n)) + 1)
solve n =
  let circ1 = (flip n (S n) {prf = lemmaLTSucc n}) # IdGate {n=1}
      circ2 = flip n n {prf = lemmaSolve n} # IdGate {n = 1}
      circ1' = circ1 . multipleQubitControlledNOT ((S (S n)) + 1) . circ1
      circ2' = circ2 . multipleQubitControlledNOT ((S (S n)) + 1) . circ2
  in circ1' . circ2'

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
import Data.Vect

readToBlank : IO (List String)
readToBlank = do putStrLn "Enter text (end with a blank line):"
                 line <- getLine
                 if line == ""
                    then pure []
                    else do lines <- readToBlank
                            pure (line :: lines)

readAndSave : IO ()
readAndSave = do contents <- readToBlank
                 putStrLn "Enter a filename:"
                 fileName <- getLine
                 Right () <- writeFile fileName (unlines contents)
                 | Left err => putStrLn (show err)
                 pure ()

readVectFileHelper : (file: File) -> IO (Maybe (n ** Vect n String))
readVectFileHelper file = do
  False <- fEOF file
  | True => pure (Just (_ ** []))
  Right line <- fGetLine file
  | Left err => pure Nothing
  Just (_ ** lines)<- readVectFileHelper file
  | Nothing => pure Nothing
  pure (Just (_ ** (line :: lines)))

readVectFile : (fileName : String) -> IO (n ** Vect n String)
readVectFile fileName = do
  Right file <- openFile fileName Read
  | Left err => pure (_ ** [])
  Just vec <- readVectFileHelper file
  | Nothing => pure (_ ** [])
  closeFile file
  pure vec


text:
module SignedInt

%default total
%access public export

record SignedInt where
    constructor SInt
    p : Nat
    n : Nat

implementation Num SignedInt where
    (SInt p1 n1) + (SInt p2 n2) = SInt (p1 + p2) (n1 + n2)
    (SInt p1 n1) * (SInt p2 n2) = SInt (p1 * p2 + n1 * n2) (p1 * n2 + p2 * n1)
    fromInteger i = if (i > 0)
      then SInt (fromIntegerNat i) 0
      else SInt 0 (fromIntegerNat (abs i))

implementation Neg SignedInt where
    negate (SInt p n) = SInt n p
    s1 - s2 = s1 + (negate s2)

infix 9 $*
($*) : SignedInt -> Nat -> SignedInt
(SInt p n) $* k = SInt (p * k) (n * k)

data SignedEq : SignedInt -> SignedInt -> Type where
    SignedRefl : (eq : (p1 + n2) = (p2 + n1)) -> SignedEq (SInt p1 n1) (SInt p2 n2)


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Lens
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Data.Contravariant

public export
interface Contravariant (0 f : Type -> Type) where
  contramap : (b -> a) -> f a -> f b

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


text:
module TestImpl

import Test

export
record Test.Main where
  constructor MkMain


text:
data Elem : Type -> List Type -> Type where

Types : (0 a : Type) -> Eq a => List Type

export
body :  (0 _ : Eq t1)
     => {auto 0 _ : Elem Bool (Types t1)}
     -> (obj : t1)
     -> (obj == obj) === maybe True (const False) (guard (obj == obj))


text:
-- ---------------------------------------------------------------- [ Main.idr ]
-- Module      : Main
-- Description : Test runner for solutions to exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]

module Main

import Exercises.Test.GettingStarted
import Exercises.Test.Interactive
import Exercises.Test.DataTypes
import Exercises.Test.State

import Test.Helpers
import Test.Utils

import Data.Vect
import System

main : IO ()
main = do resCh2  <- GettingStarted.runTests
          resCh3  <- Interactive.runTests
          resCh4  <- DataTypes.runTests
          resCh12 <- State.runTests
          let results = resCh2 ++ resCh3 ++ resCh4 ++ resCh12
          printSummary results
          when (any not results) (exit 1)

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


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

||| This section details the combinator for intentional link insertion.
|||
||| Correctness/Soundness Properties of an Intentional Link
|||
||| 1. The link should use elements that are in the model.
||| 2. The destination cannot have type: Resource
||| 3. The src and destination must not be the same.
|||
module GRL.Property.Intention

import public Decidable.Equality

import public Data.AVL.Graph
import public Data.List

import GRL.Model
import GRL.IR
import GRL.Common

%access export

-- ---------------------------------------------- [ Intentional Link Insertion ]
examineLink : GExpr INTENT -> Bool
examineLink (ILink cTy c x (Elem RESty n s)) = False
examineLink (ILink cTy c x y)                = not $ eqGExpr x y

inModel : GExpr ELEM -> GModel -> Bool
inModel (Elem ty n s) m = hasGoal n m

validLink : GExpr INTENT -> GModel -> Bool
validLink (ILink cTy ty x y) m = (inModel x m) && (inModel y m)

%hint
checkIntentBool : GExpr INTENT -> GModel -> Bool
checkIntentBool l m = validLink l m && examineLink l

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
labelWith : Stream labelType -> List a -> List (labelType, a)
labelWith lbs [] = []
labelWith (lbl :: lbs) (val :: vals) = (lbl, val) :: labelWith lbs vals
label : List a -> List (Integer, a)
label = labelWith (iterate (+1) 0)


text:
||| This modules presents an exemplar specification 'Mungo'
||| demonstrating salient features of the abstract interfact
||| description language.
module Example.Specification.Mungo

import Text.Markup.Edda
import Text.Markup.Edda.Org

import Cordial.EDSL.Specification

%access public export
%default total

||| Concrete labels for port descriptions.
data MTy = CLOCK
         | WRITE
         | READ
         | ADDRESS
         | DATA
         | ERROR_MODE
         | ERROR_INFO

||| Equality type is required to differentiate labels.
Eq MTy where
  (==) CLOCK      CLOCK      = True
  (==) WRITE      WRITE      = True
  (==) READ       READ       = True
  (==) ADDRESS    ADDRESS    = True
  (==) DATA       DATA       = True
  (==) ERROR_MODE ERROR_MODE = True
  (==) ERROR_INFO ERROR_INFO = True
  (==) _ _ = False

||| This function represents the 'generic' specification for Mungo.
|||
||| @dWidth The width of the data bus.
||| @aWidth The width of addresses
Mungo_Gen : (dWidth : Nat)
         -> (aWidth : Nat)
         -> (prfD  : ValidArraySpec dWidth [32,16])
         -> (prfA  : ValidArraySpec aWidth [8,4])
         -> IDL MTy
Mungo_Gen dWidth aWidth prfD prfA = do
  setVendor "cs.glasgow.ac.uk"
  setLibrary "examples"
  setName ("Mungo"
    <+> "_"
    <+> show dWidth
    <+> "_"
    <+> show aWidth
    <+> "_Description")
  setVersion "0.1"
  setCommunicationStyle Unicast

  c <- label CLOCK
  w <- label WRITE
  r <- label READ
  e <- label ERROR_MODE
  i <- label ERROR_INFO
  a <- label ADDRESS
  d <- label DATA

  clock c Nothing Nothing Nothing
    # system "SYS"
    # fromTargetAlways

  control w # fromInitiator

  control r # fromInitiator

  info e (fromNat 2)  # fromTarget
                      # targetOpt

  info i # fromTarget
         # targetOpt

  address a (fromNat aWidth prfA) # fromInitiator

  bus d (fromNat dWidth prfD) # fromEither

  stop

||| Transform the specification into a model.
Mungo : (dWidth, aWidth : Nat)
     -> {auto prfD : ValidArraySpec dWidth [32,16]}
     -> {auto prfA : ValidArraySpec aWidth [8,4]}
     -> InterfaceTy () MTy
Mungo dWidth aWidth {prfD} {prfA} =
  buildSpec (Mungo_Gen dWidth aWidth prfD prfA)

-- Some sample instances.

Mungo_32_4 : InterfaceTy () MTy
Mungo_32_4 = Mungo 32 4

Mungo_16_8 : InterfaceTy () MTy
Mungo_16_8 = Mungo 16 8

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
-- --------------------------------------------------------------- [ BTree.idr ]
-- Module    : BTree.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Implementation of a Binary Tree an AVL Binary Search Tree.
|||
||| The underlying AVL Tree is a Key-Value Tree, this library just
||| wraps this up as a simple Binary tree for values i.e. keys.
module Data.AVL.BTree

import Data.AVL

%access export

-- ------------------------------------------------------------- [ Definitions ]

||| A Binary Search Tree.
|||
||| @ty The type of the elements in the tree.
data BTree : (ty : Type) -> Type
    where
      MkTree : {a : Type } -> AVLTree n a Unit -> BTree a

-- --------------------------------------------------------------------- [ API ]

||| Return an empty BTree.
empty : Ord a => BTree a
empty = MkTree (Element Empty AVLEmpty)

||| Insert an element into the Tree.
insert : (Ord a) => a -> BTree a -> BTree a
insert a (MkTree t) = MkTree (snd $ AVL.API.insert a () t)

||| Does the tree contain the given element?
contains : (Ord a) => a -> BTree a -> Bool
contains a (MkTree t) = isJust (AVL.API.lookup a t)

||| How many nodes are in the tree?
size : BTree a -> Nat
size (MkTree t) = AVL.API.size t

||| Construct an ordered list containing the elements of the tree.
toList : BTree a -> List a
toList (MkTree t) = map fst $ AVL.API.toList t

||| Construct a tree from a list of elements.
fromList : (Ord a) => List a -> BTree a
fromList xs = (foldl (\t,k => BTree.insert k t) empty xs)

-- --------------------------------------------------------------- [ Instances ]

Foldable BTree where
  foldr f i (MkTree t) = foldr (\x,_,p => f x p) i t

Eq a => Eq (BTree a) where
  (==) (MkTree (Element t _)) (MkTree (Element t' _)) = t == t'

Show a => Show (BTree a) where
  show s = "{ " ++ (unwords . intersperse "," . map show . BTree.toList $ s) ++ " }"

namespace Quantifier

  data All : (predicate : type -> Type) -> (set : BTree type) -> Type where
    Satisfies : (prf : AllKeys p tree) -> All p (MkTree tree)

namespace Predicate

  data Elem : (value : type) -> (tree : BTree type) -> Type where
    IsElem : (prf : HasKey value tree)
          -> Elem value (MkTree tree)

  private
  elemNotInTree : (prfIsNotElem : HasKey value tree -> Void) -> Elem value (MkTree tree) -> Void
  elemNotInTree prfIsNotElem (IsElem prf) = prfIsNotElem prf

  isElem : DecEq type
        => (value : type)
        -> (tree  : BTree type)
        -> Dec (Elem value tree)
  isElem value (MkTree tree) with (isKey value tree)
    isElem value (MkTree tree) | (Yes prf) = Yes (IsElem prf)
    isElem value (MkTree tree) | (No prfIsNotElem) = No (elemNotInTree prfIsNotElem)

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

max_stars_repo_name: elba/idris-containers

max_issues_repo_name: elba/idris-containers

max_forks_repo_name: elba/idris-containers


text:
module TyTTP.HTTP

import Data.List
import public TyTTP

public export
data Method
  = OPTIONS
  | GET
  | HEAD
  | POST
  | PUT
  | DELETE
  | TRACE
  | CONNECT
  | OtherMethod String

export
Eq Method where
  (==) OPTIONS OPTIONS = True
  (==) GET     GET = True
  (==) HEAD    HEAD = True
  (==) POST    POST = True
  (==) PUT     PUT = True
  (==) DELETE  DELETE = True
  (==) TRACE   TRACE = True
  (==) CONNECT CONNECT = True
  (==) (OtherMethod a) (OtherMethod b) = a == b
  (==) _ _ = False

export
Show Method where
  show m = case m of
    OPTIONS => "OPTIONS"
    GET => "GET"
    HEAD => "HEAD"
    POST => "POST"
    PUT => "PUT"
    DELETE => "DELETE"
    TRACE => "TRACE"
    CONNECT => "CONNECT"
    OtherMethod str => str

export
parseMethod : String -> Method
parseMethod str = case str of
  "OPTIONS" => OPTIONS
  "GET" => GET
  "HEAD" => HEAD
  "POST" => POST
  "PUT" => PUT
  "DELETE" => DELETE
  "TRACE" => TRACE
  "CONNECT" => CONNECT
  s => OtherMethod s

public export
StringHeaders : Type
StringHeaders = List (String, String)

public export
interface HasContentType a where
  getContentType : a -> Maybe String

export
implementation HasContentType StringHeaders where
  getContentType headers = lookup "content-type" headers

public export
HttpRequest : Type -> Type -> Type -> Type
HttpRequest p h a = Request Method p h a

export
mkRequest : (m : Method) -> p -> h -> a -> HttpRequest p h a
mkRequest m p h a = MkRequest m p h a

public export
data Status
  = CONTINUE
  | SWITCHING_PROTOCOLS
  | PROCESSING
  | EARLY_HINTS
  | OK
  | CREATED
  | ACCEPTED
  | NON_AUTHORITATIVE_INFORMATION
  | NO_CONTENT
  | RESET_CONTENT
  | PARTIAL_CONTENT
  | MULTI_STATUS
  | ALREADY_REPORTED
  | IM_USED
  | MULTIPLE_CHOICES
  | MOVED_PERMANENTLY
  | FOUND
  | SEE_OTHER
  | NOT_MODIFIED
  | USE_PROXY
  | TEMPORARY_REDIRECT
  | PERMANENT_REDIRECT
  | BAD_REQUEST
  | UNAUTHORIZED
  | PAYMENT_REQUIRED
  | FORBIDDEN
  | NOT_FOUND
  | METHOD_NOT_ALLOWED
  | NOT_ACCEPTABLE
  | PROXY_AUTHENTICATION_REQUIRED
  | REQUEST_TIMEOUT
  | CONFLICT
  | GONE
  | LENGTH_REQUIRED
  | PRECONDITION_FAILED
  | PAYLOAD_TOO_LARGE
  | URI_TOO_LONG
  | UNSUPPORTED_MEDIA_TYPE
  | RANGE_NOT_SATISFIABLE
  | EXPECTATION_FAILED
  | TEAPOT
  | MISDIRECTED_REQUEST
  | UNPROCESSABLE_ENTITY
  | LOCKED
  | FAILED_DEPENDENCY
  | TOO_EARLY
  | UPGRADE_REQUIRED
  | PRECONDITION_REQUIRED
  | TOO_MANY_REQUESTS
  | REQUEST_HEADER_FIELDS_TOO_LARGE
  | UNAVAILABLE_FOR_LEGAL_REASONS
  | INTERNAL_SERVER_ERROR
  | NOT_IMPLEMENTED
  | BAD_GATEWAY
  | SERVICE_UNAVAILABLE
  | GATEWAY_TIMEOUT
  | HTTP_VERSION_NOT_SUPPORTED
  | VARIANT_ALSO_NEGOTIATES
  | INSUFFICIENT_STORAGE
  | LOOP_DETECTED
  | BANDWIDTH_LIMIT_EXCEEDED
  | NOT_EXTENDED
  | NETWORK_AUTHENTICATION_REQUIRED

export
(.code) : Status -> Int
(.code) status = case status of
  CONTINUE => 100
  SWITCHING_PROTOCOLS => 101
  PROCESSING => 102
  EARLY_HINTS => 103
  OK => 200
  CREATED => 201
  ACCEPTED => 202
  NON_AUTHORITATIVE_INFORMATION => 203
  NO_CONTENT => 204
  RESET_CONTENT => 205
  PARTIAL_CONTENT => 206
  MULTI_STATUS => 207
  ALREADY_REPORTED => 208
  IM_USED => 226
  MULTIPLE_CHOICES => 300
  MOVED_PERMANENTLY => 301
  FOUND => 302
  SEE_OTHER => 303
  NOT_MODIFIED => 304
  USE_PROXY => 305
  TEMPORARY_REDIRECT => 307
  PERMANENT_REDIRECT => 308
  BAD_REQUEST => 400
  UNAUTHORIZED => 401
  PAYMENT_REQUIRED => 402
  FORBIDDEN => 403
  NOT_FOUND => 404
  METHOD_NOT_ALLOWED => 405
  NOT_ACCEPTABLE => 406
  PROXY_AUTHENTICATION_REQUIRED => 407
  REQUEST_TIMEOUT => 408
  CONFLICT => 409
  GONE => 410
  LENGTH_REQUIRED => 411
  PRECONDITION_FAILED => 412
  PAYLOAD_TOO_LARGE => 413
  URI_TOO_LONG => 414
  UNSUPPORTED_MEDIA_TYPE => 415
  RANGE_NOT_SATISFIABLE => 416
  EXPECTATION_FAILED => 417
  TEAPOT => 418
  MISDIRECTED_REQUEST => 421
  UNPROCESSABLE_ENTITY => 422
  LOCKED => 423
  FAILED_DEPENDENCY => 424
  TOO_EARLY => 425
  UPGRADE_REQUIRED => 426
  PRECONDITION_REQUIRED => 428
  TOO_MANY_REQUESTS => 429
  REQUEST_HEADER_FIELDS_TOO_LARGE => 431
  UNAVAILABLE_FOR_LEGAL_REASONS => 451
  INTERNAL_SERVER_ERROR => 500
  NOT_IMPLEMENTED => 501
  BAD_GATEWAY => 502
  SERVICE_UNAVAILABLE => 503
  GATEWAY_TIMEOUT => 504
  HTTP_VERSION_NOT_SUPPORTED => 505
  VARIANT_ALSO_NEGOTIATES => 506
  INSUFFICIENT_STORAGE => 507
  LOOP_DETECTED => 508
  BANDWIDTH_LIMIT_EXCEEDED => 509
  NOT_EXTENDED => 510
  NETWORK_AUTHENTICATION_REQUIRED => 511

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Control.Cont.Void

import Control.EffectAlgebra
import Control.HigherOrder

import Control.Monad.Free

public export
data VoidC1 : Type -> Type where

public export
VoidC : (Type -> Type) -> (Type -> Type)
VoidC = Lift VoidC1

public export
VoidE : (Type -> Type) -> (Type -> Type)
VoidE = Lift VoidC1

public export
Uninhabited (VoidC1 a) where
  uninhabited x impossible

public export
Functor VoidC1 where
  map f x impossible

public export
runVoidC : Free VoidC a -> a
runVoidC (Return x) = x
runVoidC (Op (MkLift x)) = absurd x

namespace Algebra
  public export
  [Void] (mon : Monad m) => Algebra VoidE m where
    alg ctx hdl (MkLift x) = absurd x

  %hint
  public export
  AlgebraVoid : (mon : Monad m) => Algebra VoidE m
  AlgebraVoid = Algebra.Void


text:
{-

Test that some library functions don't cause "Maximum call stack size exceeded"
errors.

So far, only Prelude.List.++ is tested.

-}

module Main

-- Until length and replicate are tail recursive, we roll our own for this test.

lengthPlus : Nat -> List a -> Nat
lengthPlus n [] = n
lengthPlus n (x::xs) = lengthPlus (S n) xs

tailRecLength : List a -> Nat
tailRecLength = lengthPlus Z

replicateOnto : List a -> Nat -> a -> List a
replicateOnto acc Z x = acc
replicateOnto acc (S n) x = replicateOnto (x :: acc) n x

tailRecReplicate : Nat -> a -> List a
tailRecReplicate = replicateOnto []

main : IO ()
main = putStrLn $ show $ tailRecLength $ tailRecReplicate 10000 () ++ [()]


text:
module sample

import extensible_records
import Data.List

-- All functions must be total
%default total

-- *** Initial records ***

r1 : Record [("surname", String), ("age", Int)]
r1 = ("surname" .=. "Bond") .*.
     ("age" .=. 30) .*.
     emptyRec

r2 : Record [("surname", String), ("name", String)]
r2 = ("surname" .=. "Bond") .*.
     ("name" .=. "James") .*.
     emptyRec

r3 : Record [("name", String), ("code", String)]
r3 = ("name" .=. "James") .*.
     ("code" .=. "007") .*.
     emptyRec

-- *** Record Extension ***

rExtended : Record [("name", String), ("surname", String), ("age", Int)]
rExtended = ("name" .=. "James") .*. r1

-- *** Lookup ***

r1Surname : String
r1Surname = r1 .!. "surname"
-- "Bond"

r1Age : Int
r1Age = r1 .!. "age"
-- 30

-- *** Append ***

rAppend : Record [("surname", String), ("age", Int), ("name", String), ("code", String)]
rAppend = r1 .++. r3
-- { "surname" = "Bond", "age" = 30, "name" = "James", "code" = "007" }

-- *** Update ***

rUpdate : Record [("surname", String), ("age", Int)]
rUpdate = updR "surname" r1 "Dean"
-- { "surname" = "Dean", "age" = 30 }

-- *** Delete ***

rDelete : Record [("age", Int)]
rDelete = "surname" .//. r1
-- { "age" = 30 }

-- *** Delete Labels ***

rDeleteLabels1 : Record [("age", Int), ("name", String)]
rDeleteLabels1 = ["surname", "code"] .///. rAppend
-- { "age" = 30, "name" = "James" }

rDeleteLabels2 : Record [("age", Int), ("name", String)]
rDeleteLabels2 = ["code", "surname"] .///. rAppend
-- { "age" = 30, "name" = "James" }

-- *** Left Union ***

rLeftUnion1 : Record [("surname", String), ("age", Int), ("name", String), ("code", String)]
rLeftUnion1 = r1 .||. r3
-- { "surname" = "Bond", "age" = 30, "name" = "James", "code" = "007" }

r4 : Record [("name", String), ("code", String)]
r4 = ("name" .=. "Ronald") .*.
     ("code" .=. "007") .*.
     emptyRec

rLeftUnion2 : Record [("surname", String), ("name", String), ("code", String)]
rLeftUnion2 = r2 .||. r4
-- { "surname" = "Bond", "name" = "James", "code" = "007" }

rLeftUnion3 : Record [("name", String), ("code", String), ("surname", String)]
rLeftUnion3 = r4 .||. r2
-- { "name" = "Ronald", "code" = "007", "surname" = "Bond" }

-- *** Projection ***

r5 : Record [("name", String), ("surname", String), ("age", Int), ("code", String), ("supervisor", String)]
r5 = ("name" .=. "James") .*.
     ("surname" .=. "Bond") .*.
     ("age" .=. 30) .*.
     ("code" .=. "007") .*.
     ("supervisor" .=. "M") .*.
     emptyRec

rProjectLeft : Record [("name", String), ("age", Int), ("supervisor", String)]
rProjectLeft = ["name", "supervisor", "age"] .<. r5
-- { "name" = "James", "age" = 30, "supervisor" = "M" }

rProjectRight : Record [("surname", String), ("code", String)]
rProjectRight = ["name", "supervisor", "age"] .>. r5
-- { "surname" = "Bond", "code" = "007" }

max_stars_repo_name: gonzaw/extensible-records

max_issues_repo_name: gonzaw/extensible-records

max_forks_repo_name: gonzaw/extensible-records


text:
module Python

import public Python.Telescope
import public Python.Objects
import public Python.IO
import public Python.Fields
import public Python.Functions
import public Python.Exceptions

%default total
%access public export

||| Import a Python module. This is a low-level function
||| since the correctness of signatures cannot be checked.
|||
||| Libraries are encouraged to provide an ``import_`` function in their namespaces.
|||
||| @ sig     Signature of the returned object. Not checked.
||| @ modName Name of the module, as given to ``__import__``.
export
importModule : (modName : String) -> PIO (Obj sig)
importModule {sig = sig} modName =
  foreign FFI_Py "_idris_pymodule" (String -> PIO (Obj sig)) modName

||| Turn a PIO action into a Python function.
||| The function can then be used as a target for threading.Thread etc.
export
marshalPIO : PIO a -> [] ~> a
marshalPIO {a = a} action =
  unsafePerformIO $
    foreign FFI_Py "_idris_marshal_PIO" (Raw (PIO a) -> PIO ([] ~> a)) (MkRaw action)

export
getGlobal : (name : String) -> Obj sig
getGlobal {sig=sig} name =
  unsafePerformIO $
    foreign FFI_Py "_idris_get_global" (String -> PIO (Obj sig)) name

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module System.Directory

import public System.File

public export
DirPtr : Type
DirPtr = AnyPtr

support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support"

%foreign support "idris2_fileErrno"
         "node:support:fileErrno,support_system_directory"
prim__fileErrno : PrimIO Int

returnError : HasIO io => io (Either FileError a)
returnError
    = do err <- primIO prim__fileErrno
         case err of
              0 => pure $ Left FileReadError
              1 => pure $ Left FileWriteError
              2 => pure $ Left FileNotFound
              3 => pure $ Left PermissionDenied
              4 => pure $ Left FileExists
              _ => pure $ Left (GenericFileError (err-5))

ok : HasIO io => a -> io (Either FileError a)
ok x = pure (Right x)

%foreign support "idris2_currentDirectory"
         "node:lambda:()=>process.cwd()"
prim__currentDir : PrimIO (Ptr String)

%foreign support "idris2_changeDir"
         "node:support:changeDir,support_system_directory"
prim__changeDir : String -> PrimIO Int

%foreign support "idris2_createDir"
         "node:support:createDir,support_system_directory"
prim__createDir : String -> PrimIO Int

%foreign support "idris2_openDir"
prim__openDir : String -> PrimIO DirPtr

%foreign support "idris2_closeDir"
prim__closeDir : DirPtr -> PrimIO ()

%foreign support "idris2_removeDir"
prim__removeDir : String -> PrimIO ()

%foreign support "idris2_nextDirEntry"
prim__dirEntry : DirPtr -> PrimIO (Ptr String)

export
data Directory : Type where
     MkDir : DirPtr -> Directory

export
createDir : HasIO io => String -> io (Either FileError ())
createDir dir
    = do res <- primIO (prim__createDir dir)
         if res == 0
            then ok ()
            else returnError

export
changeDir : HasIO io => String -> io Bool
changeDir dir
    = do ok <- primIO (prim__changeDir dir)
         pure (ok == 0)

export
currentDir : HasIO io => io (Maybe String)
currentDir
    = do res <- primIO prim__currentDir
         if prim__nullPtr res /= 0
            then pure Nothing
            else pure (Just (prim__getString res))

export
openDir : HasIO io => String -> io (Either FileError Directory)
openDir d
    = do res <- primIO (prim__openDir d)
         if prim__nullAnyPtr res /= 0
            then returnError
            else ok (MkDir res)

export
closeDir : HasIO io => Directory -> io ()
closeDir (MkDir d) = primIO (prim__closeDir d)

export
removeDir : HasIO io => String -> io ()
removeDir dirName = primIO (prim__removeDir dirName)

export
dirEntry : HasIO io => Directory -> io (Either FileError String)
dirEntry (MkDir d)
    = do res <- primIO (prim__dirEntry d)
         if prim__nullPtr res /= 0
            then returnError
            else ok (prim__getString res)


text:
module Quotient_Group

import Monoid
import Group

%access public export

||| Given a map f : g -> h, the image of f along with the proofs
total
ImageOf : (x : Type) -> (y : Type) -> (f : x -> y) -> Type
ImageOf x y f = (b : y ** (a : x ** ( (f a) = b)))

||| Generates the coset over h of a given element in g
total
Coset: (h : Type) -> ((+) : h -> h -> h) -> (pf1 : IsGroup h (+)) ->
       (g : Type) -> ((*) : g -> g -> g) -> (pf2 : IsGroup g (*)) ->
       (Subgroup h (+) pf1 g (*) pf2) -> (a : g) -> Type
Coset h (+) pf1 g (*) pf2 (f ** pfSub) a = (y : g ** (y1 : ImageOf h g f ** ((fst y1)*a = y)))
--Imgfn h g (\r => a*(fst(sbgrp) r))

||| The property that a particular element is in the coset
total
Is_in_Coset : (h : Type) -> ((+) : h -> h -> h) -> (pf1 : IsGroup h (+)) ->
              (g : Type) -> ((*) : g -> g -> g) -> (pf2 : IsGroup g (*)) ->
              (Subgroup h (+) pf1 g (*) pf2) -> (a : g) -> (b : g) -> Type

Is_in_Coset h (+) pf1 g (*) pf2 (f ** pfSub) a b = (y1 : ImageOf h g f ** ((fst y1)*a = b))

||| If b is in the coset of a, then a is in the coset of b
total
Coset_property_1 : (h : Type) -> ((+) : h -> h -> h) -> (pf1 : IsGroup h (+)) ->
                   (g : Type) -> ((*) : g -> g -> g) -> (pf2 : IsGroup g (*)) ->
                   (Subgroup h (+) pf1 g (*) pf2) -> (a : g) -> (b : g) ->
                   (Is_in_Coset  h (+) pf1 g (*) pf2 (f ** pfSub) a b) ->
                   (Is_in_Coset  h (+) pf1 g (*) pf2 (f ** pfSub) b a)

||| Property 2 - A proof that C(a) * C(b) and C(a*b) are equal as sets
total
Coset_property_2 : (h : Type) -> ((+) : h -> h -> h) -> (pf1 : IsGroup h (+)) ->
                   (g : Type) -> ((*) : g -> g -> g) -> (pf2 : IsGroup g (*)) ->
                   (Subgroup h (+) pf1 g (*) pf2) -> Type


text:
module Photo

import Objects.Size

public export
record Photo where
  constructor CreatePhoto
  id : Integer
  albumID : Integer
  ownerID : Integer
  userID : Integer
  text : String
  date : Integer
  size : Maybe $ List Size.Size
  photo75 : String
  photo130 : String
  photo604 : String
  photo807 : String
  photo1280 : String
  photo2560 : String
  width : Integer
  heoght : Integer

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI