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

||| A alternate version of the GRL with added structural semantics.
module GRL.Lang.GLangPlus

import public GRL.Common
import public GRL.IR
import public GRL.Model
import public GRL.Builder
import public GRL.Pretty

%access public export

-- ------------------------------------------------------------- [ Type System ]

||| Specify valid impacts between elements.
data ValidImpacts : GElemTy -> GElemTy -> Type where
  GIS : ValidImpacts GOALty SOFTty
  SIG : ValidImpacts SOFTty GOALty
  TIG : ValidImpacts TASKty GOALty
  TIS : ValidImpacts TASKty SOFTty
  RIG : ValidImpacts RESty GOALty
  RIS : ValidImpacts RESty GOALty

||| Specify valid decomopositions.
data ValidDecomp : GElemTy -> GElemTy -> Type where
  GHS : ValidDecomp GOALty SOFTty
  THT : ValidDecomp TASKty TASKty

||| New structural types.
data GLangPTy = E GElemTy | L | S

||| The GLang Language with improved structural semantics.
data GLang : GLangPTy -> GTy -> Type where
  ||| Make a Goal node.
  MkGoal : String -> Maybe SValue -> GLang (E GOALty) ELEM
  ||| Make a Soft Goal node.
  MkSoft : String -> Maybe SValue -> GLang (E SOFTty) ELEM
  ||| Make a Task node.
  MkTask : String -> Maybe SValue -> GLang (E TASKty) ELEM
  ||| Make a resource node.
  MkRes  : String -> Maybe SValue -> GLang (E RESty)  ELEM

  ||| Declare an impact relation.
  MkImpact : CValue
          -> GLang (E xty) ELEM
          -> GLang (E yty) ELEM
          -> {auto prf : ValidImpacts xty yty}
          -> GLang L INTENT

  ||| And decomposition relation.
  MkAnd : GLang (E xty) ELEM
       -> GLang (E yty) ELEM
       -> {auto prf : ValidDecomp xty yty}
       -> GLang S STRUCT

-- ----------------------------------------------------------- [ Pretty Syntax ]

syntax [a] "~~>" [b] "|" [c] = MkImpact c a b
syntax [a] "&=" [b]          = MkAnd a b

-- ----------------------------------------------------------- [ Type Synonyms ]

GOAL : Type
GOAL = GLang (E GOALty) ELEM

SOFT : Type
SOFT = GLang (E SOFTty) ELEM

TASK : Type
TASK = GLang (E TASKty) ELEM

RES : Type
RES = GLang (E RESty) ELEM

IMPACT : Type
IMPACT = GLang L INTENT

AND : Type
AND = GLang S STRUCT

-- --------------------------------------------------------------------- [ GRL ]

implementation GRL (\x => GLang ty x) where
    mkElem (MkGoal s e) = Elem GOALty s e
    mkElem (MkSoft s e) = Elem SOFTty s e
    mkElem (MkTask s e) = Elem TASKty s e
    mkElem (MkRes  s e) = Elem RESty  s e

    mkIntent (MkImpact c a b) = ILink IMPACTSty c (mkElem a) (mkElem b)

    mkStruct (MkAnd a b) = SLink ANDty (mkElem a) [(mkElem b)]

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module DepSec.DIO

%access public export

||| Security monad
||| @ l security label of wrapped value
||| @ valueType type of wrapped value
data DIO : l
        -> (valueType : Type)
        -> Type where
  ||| TCB
  MkDIO : IO valueType -> DIO l valueType

||| Unwrap security monad
||| TCB
||| @ dio secure computation
run : (dio : DIO l a) -> IO a
run (MkDIO m) = m

||| Lift arbitrary IO monad into security monad
||| TCB
||| @ io computation
lift : (io : IO a) -> DIO l a
lift = MkDIO

Functor (DIO l) where
  map f (MkDIO io) = MkDIO (map f io)

Applicative (DIO l) where
  pure = MkDIO . pure
  (<*>) (MkDIO f) (MkDIO a) = MkDIO (f <*> a)

Monad (DIO l) where
  (>>=) (MkDIO a) f = MkDIO (a >>= run . f)

ext: idr

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module Algebra.Semiring

import Data.Nat
import Syntax.PreorderReasoning

%default total

||| This interface is a witness that for a
||| numeric type `a` the axioms of a commutative semiring hold:
|||
||| 1. `a` is a commutative monoid under addition:
|||    1. `+` is associative: `k + (m + n) = (k + m) + n` for all `k,m,n : a`.
|||    2. `+` is commutative: `m + n = n + m` for all `m,n : a`.
|||    3. 0 is the additive identity: `n + 0 = n` for all `n : a`.
|||
||| 2. `a` is a commutative monoid under multiplication:
|||    1. `*` is associative: `k * (m * n) = (k * m) * n` for all `k,m,n : a`.
|||    2. `*` is commutative: `m * n = n * m` for all `m,n : a`.
|||    3. 1 is the multiplicative identity: `n * 1 = n` for all `n : a`.
|||
||| 3. Multiplication is distributive with respect to addition:
|||    `k * (m + n) = (k * m) + (k * n)` for all `k,m,n : a`.
|||
public export
interface Num a => Semiring a where
  ||| Addition is associative.
  0 plusAssociative : {k,m,n : a} -> k + (m + n) === (k + m) + n

  ||| Addition is commutative.
  0 plusCommutative : {m,n : a} -> m + n === n + m

  ||| 0 is the additive identity.
  0 plusZeroLeftNeutral : {n : a} -> 0 + n === n

  ||| Multiplication is associative.
  0 multAssociative : {k,m,n : a} -> k * (m * n) === (k * m) * n

  ||| Multiplication is commutative.
  0 multCommutative : {m,n : a} -> m * n === n * m

  ||| 1 is the multiplicative identity.
  0 multOneLeftNeutral : {n : a} -> 1 * n === n

  ||| Multiplication is distributive with respect to addition.
  0 leftDistributive : {k,m,n : a} -> k * (m + n) === (k * m) + (k * n)

  ||| Zero is an absorbing element of multiplication.
  0 multZeroLeftAbsorbs : {n : a} -> 0 * n === 0

--------------------------------------------------------------------------------
--          Proofs on Addition
--------------------------------------------------------------------------------

||| `n + 0 === n` for all `n : a`.
export
0 plusZeroRightNeutral : Semiring a => {n : a} -> n + 0 === n
plusZeroRightNeutral =
  Calc $
    |~ n + 0
    ~~ 0 + n ... plusCommutative
    ~~ n     ... plusZeroLeftNeutral

--------------------------------------------------------------------------------
--          Proofs on Multiplication
--------------------------------------------------------------------------------

||| `n * 1 === n` for all `n : a`.
export
0 multOneRightNeutral : Semiring a => {n : a} -> n * 1 === n
multOneRightNeutral =
  Calc $
    |~ n * 1
    ~~ 1 * n ... multCommutative
    ~~ n     ... multOneLeftNeutral

||| Zero is an absorbing element of multiplication.
export
0 multZeroRightAbsorbs : Semiring a => {n : a} -> n * 0 === 0
multZeroRightAbsorbs =
  Calc $
    |~ n * 0
    ~~ 0 * n ... multCommutative
    ~~ 0     ... multZeroLeftAbsorbs

||| Zero is an absorbing element of multiplication.
export
multZeroAbsorbs :  Semiring a
                => (m,n : a)
                -> Either (m === 0) (n === 0)
                -> m * n === 0
multZeroAbsorbs m n (Left rfl) =
  Calc $
    |~ m * n
    ~~ 0 * n ... cong (*n) rfl
    ~~ 0     ... multZeroLeftAbsorbs

multZeroAbsorbs m n (Right rfl) =
  Calc $
    |~ m * n
    ~~ m * 0 ... cong (m*) rfl
    ~~ 0     ... multZeroRightAbsorbs

||| Multiplication is distributive with respect to addition.
export
0 rightDistributive :  Semiring a
                  => {k,m,n : a}
                  -> (m + n) * k === m * k + n * k
rightDistributive =
  Calc $
    |~ (m + n) * k
    ~~ k * (m + n)       ... multCommutative
    ~~ (k * m) + (k * n) ... leftDistributive
    ~~ m * k + k * n     ... cong (+ k * n) multCommutative
    ~~ m * k + n * k     ... cong (m * k +) multCommutative

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

export
Semiring Nat where
  plusAssociative = Nat.plusAssociative _ _ _
  plusCommutative = Nat.plusCommutative _ _
  plusZeroLeftNeutral = Nat.plusZeroLeftNeutral _
  multAssociative = Nat.multAssociative _ _ _
  multCommutative = Nat.multCommutative _ _
  multOneLeftNeutral = Nat.multOneLeftNeutral _
  leftDistributive = multDistributesOverPlusRight _ _ _
  multZeroLeftAbsorbs = Refl


text:
import Data.Vect
import Data.Vect.Elem

data Typ : Type where
    TLam : Typ -> Typ -> Typ
    TNat : Typ

data Term : Typ -> Vect len Typ -> Type where
    Var : Elem a ctx -> Term a ctx
    Lam : Term b (a :: ctx) -> Term (TLam a b) ctx
    Fix : Term a (a :: ctx) -> Term a ctx

lookup : Vect len Typ -> Fin len -> Typ
lookup (a :: ctx) FZ = a
lookup (_ :: ctx) (FS n) = lookup ctx n

count : {ctx : Vect len Typ} -> (n : Fin len) -> Elem (lookup ctx n) ctx
count {ctx = _ :: ctx} FZ = Here
count {ctx = _ :: ctx} (FS n) = There (count n)

segfaults : {len : _} -> {ctx : Vect len Typ} ->
            Term (TLam TNat TNat) ctx
segfaults = Fix (Lam (Var (count 0)))

cycleDetected : {len : _} -> {ctx : Vect len Typ} ->
                Term (TLam TNat TNat) ctx
cycleDetected = Fix (Var (count 0))


text:
import InfList
import Data.Primitives.Views
import Data.Nat.Views

-- exercise #1
every_other : Stream a -> Stream a
every_other (first :: second :: tail) = second :: every_other tail

-- Exercise #2
Functor InfList where
  map func (value :: tail) = (func value) :: (map func tail)

infListFunctorTest: List Integer
infListFunctorTest = getPrefix 10 (map (*2) (countFrom 1))

-- Exercise #3
data Face = Heads | Tails

getFace : Int -> Face
getFace number with (divides number 2)
  getFace ((2 * div) + rem) | (DivBy prf) = if rem <= 0 then Heads else Tails

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

coinFlips : Nat -> Stream Int -> List Face
coinFlips count stream = map getFace (take count stream)

flipsTest : List Face
flipsTest = coinFlips 6 (randoms 12345)

-- Exercise #4
calcNext: (number: Double) -> (approx: Double) -> Double
calcNext number approx = (approx + (number / approx)) / 2

square_root_approx : (number: Double) -> (approx: Double) -> Stream Double
square_root_approx number approx = approx :: square_root_approx number (calcNext number approx)

sqrtTest1 : List Double
sqrtTest1 = take 3 $ square_root_approx 10 10

sqrtTest2 : List Double
sqrtTest2 = take 10 $ square_root_approx 100 25

-- Exercise #5
square_root_bound : (max: Nat) -> (number: Double) -> (bound : Double) -> (approxs: Stream Double) -> Double
square_root_bound  Z    number bound (value :: xs) = value
square_root_bound (S k) number bound (apprx :: xs) =
  if isBoundReached
  then apprx
  else square_root_bound k number bound xs
  where
    isBoundReached : Bool
    isBoundReached = (apprx * apprx - number) < bound

square_root : Double -> Double
square_root value = square_root_bound 100 value 0.00000000001 (square_root_approx value value)

boundedSqrtTest1: Double
boundedSqrtTest1 = square_root 6

boundedSqrtTest2: Double
boundedSqrtTest2 = square_root 2500

boundedSqrtTest3: Double
boundedSqrtTest3 = square_root 2501

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
import Json

-- pattern-matching-friendly JSON structure (that is, without
-- SortedMap in it)

data PMJsonValue = JsonString String
                 | JsonNumber Float
                 | JsonBool Bool
                 | JsonNull
                 | JsonArray (List PMJsonValue)
                 | JsonObject (List (String, PMJsonValue))

mapSnd : (b -> c) -> List (a, b) -> List (a, c)
mapSnd f [] = []
mapSnd f ((x,y)::xs) = (x, f y) :: mapSnd f xs

toPM : JsonValue -> PMJsonValue
toPM (JsonString s) = (JsonString s)
toPM (JsonNumber n) = (JsonNumber n)
toPM (JsonBool b) = (JsonBool b)
toPM JsonNull = JsonNull
toPM (JsonArray a) = JsonArray $ map toPM a
toPM (JsonObject o) = JsonObject $ mapSnd toPM $ toList o

fromPM : PMJsonValue -> JsonValue
fromPM (JsonString s) = (JsonString s)
fromPM (JsonNumber n) = (JsonNumber n)
fromPM (JsonBool b) = (JsonBool b)
fromPM JsonNull = JsonNull
fromPM (JsonArray a) = JsonArray $ map fromPM a
fromPM (JsonObject o) = JsonObject . fromList $ mapSnd fromPM o

instance Show PMJsonValue where
  show = show . fromPM

-- objects
syntax "j{" [xs] "}" = JsonObject xs
-- (key, value): [f]loat, [b]ool, [s]tring, [a]ny
syntax [x] ".f" [y] = (x, JsonNumber y)
syntax [x] ".b" [y] = (x, JsonBool y)
syntax [x] ".s" [y] = (x, JsonString y)
syntax [x] ".a" [y] = (x, y)

-- arrays
syntax "j[" [xs] "]" = JsonArray xs
syntax [x] ":f" [y] = JsonNumber x :: y
syntax [x] ":b" [y] = JsonBool x :: y
syntax [x] ":s" [y] = JsonString x :: y
syntax [x] ":a" [y] = x :: y

-- j{["num" .f 3, "bool" .b True, "obj" .a j{["num2" .f 2]}, "arr" .a j[1 :f "str" :s (j{["n" .f 3]}) :a []]]}

foo : PMJsonValue -> Float
foo (j{["obj" .a (j{["arr" .a j[n :f m :f []]]})]}) = n + m
foo (j{["obj" .a obj]}) = 1
foo _ = 0 -- coverage check takes forever without it

-- foo j{["obj" .a (j{["arr" .a j[3 :f 4 :f []]]})]}
-- map (foo . toPM) $ parse jsonToplevelValue """{"obj": {"arr": [3, 4]}}"""

max_stars_repo_name: archaeron/idris-json-rpc

max_issues_repo_name: archaeron/idris-json-rpc

max_forks_repo_name: archaeron/idris-json-rpc


text:
StringOrInt : Bool -> Type
StringOrInt x = case x of
                    True => Int
                    False => String

getStringOrInt : (x : Bool) -> StringOrInt x
getStringOrInt x = case x of
                        True => 94
                        False => "Ninety four"

valToString : (x : Bool) -> StringOrInt x -> String
valToString x val = case x of
                        True => cast val
                        False => val

valToStringHoles : (x : Bool) -> StringOrInt x -> String
valToStringHoles x val = case x of
                        True => ?xtrueType
                        False => ?xfalseType

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
module Core.SchemeEval.Quote

import Core.Context
import Core.Core
import Core.Env
import Core.SchemeEval.Compile
import Core.SchemeEval.Evaluate
import Core.TT

mutual
  quoteArgs : {auto c : Ref Ctxt Defs} ->
              {bound, free : _} ->
              Ref Sym Integer -> Bounds bound ->
              Env Term free -> List (Core (SNF free)) ->
              Core (List (Term (bound ++ free)))
  quoteArgs q bound env args
      = traverse (\arg => do arg' <- arg
                             quoteGen q bound env arg') args

  quotePi : {auto c : Ref Ctxt Defs} ->
            {bound, free : _} ->
            Ref Sym Integer -> Bounds bound ->
            Env Term free -> PiInfo (SNF free) ->
            Core (PiInfo (Term (bound ++ free)))
  quotePi q bound env Explicit = pure Explicit
  quotePi q bound env Implicit = pure Implicit
  quotePi q bound env AutoImplicit = pure AutoImplicit
  quotePi q bound env (DefImplicit t)
      = do t' <- quoteGen q bound env t
           pure (DefImplicit t')

  quoteBinder : {auto c : Ref Ctxt Defs} ->
                {bound, free : _} ->
                Ref Sym Integer -> Bounds bound ->
                Env Term free -> Binder (SNF free) ->
                Core (Binder (Term (bound ++ free)))
  quoteBinder q bound env (Lam fc r p ty)
     = do ty' <- quoteGen q bound env ty
          p' <- quotePi q bound env p
          pure (Lam fc r p' ty')
  quoteBinder q bound env (Let fc r val ty)
     = do ty' <- quoteGen q bound env ty
          val' <- quoteGen q bound env val
          pure (Let fc r val' ty')
  quoteBinder q bound env (Pi fc r p ty)
     = do ty' <- quoteGen q bound env ty
          p' <- quotePi q bound env p
          pure (Pi fc r p' ty')
  quoteBinder q bound env (PVar fc r p ty)
     = do ty' <- quoteGen q bound env ty
          p' <- quotePi q bound env p
          pure (PVar fc r p' ty')
  quoteBinder q bound env (PLet fc r val ty)
     = do ty' <- quoteGen q bound env ty
          val' <- quoteGen q bound env val
          pure (PLet fc r val' ty')
  quoteBinder q bound env (PVTy fc r ty)
     = do ty' <- quoteGen q bound env ty
          pure (PVTy fc r ty')

  quoteHead : {auto c : Ref Ctxt Defs} ->
              {bound, free : _} ->
              Ref Sym Integer ->
              FC -> Bounds bound -> Env Term free -> SHead free ->
              Core (Term (bound ++ free))
  quoteHead {bound} q fc bounds env (SLocal idx prf)
      = let MkVar prf' = addLater bound prf in
            pure (Local fc Nothing _ prf')
    where
      addLater : {idx : _} ->
                 (ys : List Name) -> (0 p : IsVar n idx xs) ->
                 Var (ys ++ xs)
      addLater [] isv = MkVar isv
      addLater (x :: xs) isv
          = let MkVar isv' = addLater xs isv in
                MkVar (Later isv')
  quoteHead q fc bounds env (SRef nt n)
      = pure $ case findName bounds of
             Just (MkVar p) => Local fc Nothing _ (varExtend p)
             Nothing => Ref fc nt n
    where
      findName : Bounds bound' -> Maybe (Var bound')
      findName None = Nothing
      findName (Add x n' ns)
          = if n == n'
               then Just (MkVar First)
               else do MkVar p <-findName ns
                       Just (MkVar (Later p))
  quoteHead q fc bounds env (SMeta n i args)
      = do args' <- quoteArgs q bounds env args
           pure $ Meta fc n i args'

  quoteGen : {auto c : Ref Ctxt Defs} ->
             {bound, vars : _} ->
             Ref Sym Integer -> Bounds bound ->
             Env Term vars -> SNF vars -> Core (Term (bound ++ vars))
  quoteGen q bound env (SBind fc n b sc)
      = do i <- get Sym
           put Sym (i + 1)
           let var = UN (Basic ("b-" ++ show (fromInteger i)))
           -- Ref Bound gets turned directly into a symbol by seval, which
           -- we can then read back when quoting the scope
           arg <- seval EvalAll env (Ref fc Bound var)
           sc' <- quoteGen q (Add n var bound) env !(sc arg)
           b' <- quoteBinder q bound env b
           pure (Bind fc n b' sc')
  quoteGen q bound env (SApp fc f args)
      = do f' <- quoteHead q fc bound env f
           args' <- quoteArgs q bound env args
           pure $ apply fc f' args'
  quoteGen q bound env (SDCon fc n t ar args)
      = do args' <- quoteArgs q bound env args
           pure $ apply fc (Ref fc (DataCon t ar) n) args'
  quoteGen q bound env (STCon fc n t ar args)
      = do args' <- quoteArgs q bound env args
           pure $ apply fc (Ref fc (TyCon t ar) n) args'
  quoteGen q bound env (SDelayed fc r arg)
      = do argQ <- quoteGen q bound env arg
           pure (TDelayed fc r argQ)
  quoteGen q bound env (SDelay fc r ty arg)
      = do argQ <- quoteGen q bound env !arg
           tyQ <- quoteGen q bound env !ty
           pure (TDelay fc r tyQ argQ)
  quoteGen q bound env (SForce fc r arg)
      = case arg of
             SDelay fc _ _ arg => quoteGen q bound env !arg
             _ => do arg' <- quoteGen q bound env arg
                     pure $ (TForce fc r arg')
  quoteGen q bound env (SPrimVal fc c) = pure $ PrimVal fc c
  quoteGen q bound env (SErased fc i) = pure $ Erased fc i
  quoteGen q bound env (SType fc u) = pure $ TType fc u

export
quote : {auto c : Ref Ctxt Defs} ->
        {vars : _} ->
        Env Term vars -> SNF vars -> Core (Term vars)
quote env tm
    = do q <- newRef Sym 0
         quoteGen q None env tm


text:
module Web.Internal.UrlTypes

import JS

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

export data URL : Type where [external]

export
ToFFI URL URL where toFFI = id

export
FromFFI URL URL where fromFFI = Just

export
SafeCast URL where
  safeCast = unsafeCastOnPrototypeName "URL"

export data URLSearchParams : Type where [external]

export
ToFFI URLSearchParams URLSearchParams where toFFI = id

export
FromFFI URLSearchParams URLSearchParams where fromFFI = Just

export
SafeCast URLSearchParams where
  safeCast = unsafeCastOnPrototypeName "URLSearchParams"


text:
module Main

lnWord : String -> Nat
lnWord str = length $ words str

max_stars_repo_name: mrLSD/idris-docker

max_issues_repo_name: mrLSD/idris-docker

max_forks_repo_name: mrLSD/idris-docker


text:
{-
foo
bar
-}
import CIL.FFI

||| System.Collections.DictionaryEntry value type.
DictionaryEntry : Type
DictionaryEntry = CIL $ corlibTyVal "System.Collections.DictionaryEntry"

IsA Object DictionaryEntry where {}

newDictionaryEntry : key -> value -> CIL_IO DictionaryEntry
newDictionaryEntry key value = new (Object -> Object -> CIL_IO DictionaryEntry)
                                   (believe_me key)
                                   (believe_me value)

Key : DictionaryEntry -> CIL_IO Object
Key = invoke (CILInstance "get_Key") (DictionaryEntry -> CIL_IO Object)

Value : DictionaryEntry -> CIL_IO Object
Value = invoke (CILInstance "get_Value") (DictionaryEntry -> CIL_IO Object)

main : CIL_IO ()
main = do
  e <- newDictionaryEntry "foo" "bar"
  for_ [Key, Value] $ \p =>
    putStrLn !(p e >>= ToString)

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module Main

main : IO ()
main =
   let s = [1..] in putStrLn $ show $ take 100 s

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:
module Minecraft.Base.PreClassic.Dirt.Block

import public Minecraft.Base.PreClassic.Dirt
import public Minecraft.Core.Block.Export
import public Minecraft.Core.Block.Break.Export
import public Minecraft.Data.Type.Vtbl

%default total

namespace Export
  public export %hint dirtBlock : Block Dirt.Block
  public export %hint breakDirt : Break Dirt.Block
  public export %hint dirtVtbl  : Vtbl  Dirt.Block

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


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

import public Freyja.Common

%access public export
-- ----------------------------------------------- [ Problems and Requirements ]

-- Encoding of CONTROL | CODE | ACTION ??
-- Encoding of Categories => Security, Access Control, HCI...

data STy = ABSTRACT | CONCRETE

data SifTy = TyREQ     | TyTRAIT   | TyPROPERTY | TySOLUTION
           | TyPROBLEM | TyPATTERN | TyAFFECTS

data HasMData : SifTy -> Type where
  HMA : HasMData TyREQ
  HMB : HasMData TyPROPERTY
  HMC : HasMData TySOLUTION
  HMD : HasMData TyPROBLEM
  HME : HasMData TyPATTERN
  HMF : HasMData TyTRAIT

data SifOutFormat = ORG  | LATEX   | CMARK | XML    | DOT
                  | EDDA | COMPACT | IDRIS | STRING | FREYJA

Eq SifOutFormat where
  (==) LATEX   LATEX   = True
  (==) CMARK   CMARK   = True
  (==) ORG     ORG     = True
  (==) XML     XML     = True
  (==) DOT     DOT     = True
  (==) EDDA    EDDA    = True
  (==) COMPACT COMPACT = True
  (==) IDRIS   IDRIS   = True
  (==) STRING  STRING  = True
  (==) FREYJA  FREYJA  = True
  (==) _       _       = False

Show SifOutFormat where
  show LATEX   = "LaTeX"
  show CMARK   = "CommonMark"
  show ORG     = "Org"
  show XML     = "XML"
  show DOT     = "dot"
  show EDDA    = "Edda"
  show COMPACT = "Compact"
  show IDRIS   = "Idris"
  show STRING  = "String"
  show FREYJA  = "Freyja"

export
readOutFMT : String -> Maybe SifOutFormat
readOutFMT s =
  case toLower s of
    "latex"    => Just LATEX
    "markdown" => Just CMARK
    "org"      => Just ORG
    "xml"      => Just XML
    "dot"      => Just DOT
    "compact"  => Just COMPACT
    "string"   => Just STRING
    "freyja"   => Just FREYJA
    "idris"    => Nothing -- @TODO Just IDRIS
    "edda"     => Nothing -- internal
    otherwise  => Nothing

data SifDomain = MkDomain String (Maybe String)

export
defaultDomain : SifDomain
defaultDomain = MkDomain "Default" (Just "Not Specified")

Eq SifDomain where
  (==) (MkDomain x xd) (MkDomain y yd) = x == y && xd == yd

Show SifDomain where
  show (MkDomain x xd) = unwords ["MkDomain", show x, show xd]
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
import TypedContainers.RBTree
import TypedContainers.LawfulOrd.Nat
import TypedContainers.LawfulOrd

mytree : RBTree Nat (\_ => Nat)
mytree = empty

mytree' : RBTree Nat (\_ => Nat)
mytree' =
  insert 5 10 .
  insert 2 4 .
  insert 8 16 $
  mytree

max_stars_repo_name: L-as/idris-rbtree

max_issues_repo_name: L-as/idris-rbtree

max_forks_repo_name: L-as/idris-rbtree


text:
module TwoThreeTree
%access abstract

data TwoThreeTree : Type -> Type where
  Nil  : TwoThreeTree a
  Leaf : a -> TwoThreeTree a
  Node : a -> a -> TwoThreeTree a -> TwoThreeTree a
    -> Maybe (TwoThreeTree a) -> TwoThreeTree a

-- Lookup value
lookup : (Eq a, Ord a) => a -> TwoThreeTree a -> Bool
lookup x Nil = False
lookup x (Leaf r) = (x == r)
lookup x (Node lm mm lc mc rc) =
  if x <= lm then
    lookup x lc
  else
    if (x > lm)  && (x <= mm) then
      lookup x mc
    else
      case rc of
        Nothing => False
        Just tt => lookup x tt

-- Tree2List function
Tree2List : TwoThreeTree a -> List a
Tree2List Nil = []
Tree2List (Leaf x) = [x]
Tree2List (Node x y z w Nothing) = (Tree2List z) ++ (Tree2List w)
Tree2List (Node x y z w (Just s)) = (Tree2List z) ++ (Tree2List w) ++ (Tree2List s)

Show a => Show (TwoThreeTree a) where
  show x = show (Tree2List x)

private
get_max : (Ord a) => TwoThreeTree a -> a -> a
get_max tree val =
  case (head' ll, tail' ll) of
    (Nothing, Nothing) => val
    (Just h, Just t) => foldl max h t
  where
  ll : List a
  ll = Tree2List tree

private
update_lm_mm : Ord a => TwoThreeTree a -> TwoThreeTree a
update_lm_mm Nil = Nil
update_lm_mm (Leaf x) = Leaf x
update_lm_mm (Node _ _ (Leaf u) (Leaf v) y1) =
  Node u v (Leaf u) (Leaf v) y1
update_lm_mm (Node _ mm (Leaf u) mst y1) =
  Node u (get_max mst mm) (Leaf u) mst y1
update_lm_mm (Node lm _ lst (Leaf s1) y1) =
  Node (get_max lst lm) s1 lst (Leaf s1) y1
update_lm_mm (Node lm mm lst mst y1) =
  Node (get_max lst lm) (get_max mst mm) lst mst y1

private
insert : Ord a => a -> TwoThreeTree a
  -> (TwoThreeTree a, Maybe(TwoThreeTree a))
insert x Nil = (Leaf x, Nothing)
insert x (Leaf y) =
  if y <= x then
    (Node y x (Leaf y) (Leaf x) Nothing, Nothing)
  else
    (Node x y (Leaf x) (Leaf y) Nothing, Nothing)

insert x y = insert' x y where
  insert' : a -> TwoThreeTree a
    -> (TwoThreeTree a, Maybe (TwoThreeTree a))
  insert' x (Node y z (Leaf w) (Leaf s) t) =
    insert'' x y z w s t where
    insert'' : a -> a -> a -> a -> a -> Maybe (TwoThreeTree a)
      -> (TwoThreeTree a, Maybe (TwoThreeTree a))
    insert'' x lm mm lsl msl Nothing =
      if x <= lm then
        (Node x lm (Leaf x) (Leaf lsl) (Just (Leaf msl)), Nothing)
      else
        if (x > lm) && (x <= mm) then
          (Node lm x (Leaf lsl) (Leaf x) (Just (Leaf msl)), Nothing)
        else
          (Node lm mm (Leaf lsl) (Leaf msl) (Just (Leaf x)), Nothing)
    insert'' k lm mm lf mf (Just (Leaf rf)) =
      if k <= lm then
        (Node k lm (Leaf k) (Leaf lm) Nothing,   -- This is node n
         Just (Node mm rf (Leaf mm) (Leaf rf) Nothing)) -- This is node m
      else
        if (k > lm) && (k <= mm) then
          (Node lm k (Leaf lm) (Leaf k) Nothing,
           Just (Node mm rf (Leaf mm) (Leaf rf) Nothing))
        else
          if (k > mm) && (k <= rf) then
            (Node lm mm (Leaf lm) (Leaf mm) Nothing,
             Just (Node k rf (Leaf k) (Leaf rf) Nothing))
          else
            (Node lm mm (Leaf lm) (Leaf mm) Nothing,
             Just (Node rf k (Leaf rf) (Leaf k) Nothing))

    -- TODO This should never happen, because all leaves are the same
    -- level!
    -- insert'' x y z x1 y1 (Just (Node u v z1 w1 s1)) = ?b_2

  insert' x (Node y z lst mst t) =
    if x <= y then
      let (n, m) = insert x lst in
          case m of
            Nothing => (Node y z n mst t, Nothing)
            Just m =>
              case t of
                Nothing => (Node y z n m (Just mst), Nothing)
                Just m1 => (Node y z n m (Just mst), Just m1)
    else
      if (x > y) && (x <= z) then
        let (n, m) = insert x mst in
          case m of
            Nothing => (Node y z lst n t, Nothing)
            Just m =>
              case t of
                Nothing => (Node y z lst n (Just m), Nothing)
                Just m1 => (Node y z lst n (Just m), Just m1)
      else
        case t of
          Just u =>
            let (n, m) = insert x u in
              case m of
                Nothing => (Node y z lst mst (Just n), Nothing)
                Just w => (Node y z lst mst (Just n), Just w)
          Nothing =>
            let (n, m) = insert x mst in
            case m of
              Nothing => (Node y z lst n Nothing, Nothing)
              Just w => (Node y z lst n Nothing, m)

private
get : Ord a => TwoThreeTree a -> a
get (Leaf x) = x
get (Node x y z w s) = max x y

-- Insert function XXX: Make this update_lm_mm inlined with insertion
-- itself!
Insert : Ord a => a -> TwoThreeTree a -> TwoThreeTree a
Insert x y =
  if (lookup x y) /= True then
    let (n, m) = insert x y in
      case m of
        Nothing => update_lm_mm n
        Just m => update_lm_mm (Node (get n) (get m) n m Nothing)
  else y

-- Functor on TwoThreeTree
Functor TwoThreeTree where
  map f Nil = Nil
  map f (Leaf x) = Leaf (f x)
  map f (Node x y z w Nothing) = Node (f x) (f y) (map f z) (map f w) Nothing
  map f (Node x y z w (Just s)) = Node (f x) (f y) (map f z) (map f w)
    (Just (assert_total (map f s)))

private
delete' : (Ord a, Eq a) => a -> TwoThreeTree a -> (TwoThreeTree a, Bool)

-- This is the case where there are 3 children
delete' k (Node y z (Leaf w) (Leaf s) (Just t)) =
  -- Remove the left leaf
  if k == w then
    (Node z (get_val t) (Leaf s) t Nothing, False)
  else
    -- Remove the middle leaf
    if k == s then
      (Node y (get_val t) (Leaf w) t Nothing, False)
    -- Remove the right leaf
    else
      (Node y z (Leaf w) (Leaf s) Nothing, False) where
  get_val : TwoThreeTree a -> a
  get_val (Leaf x) = x

-- This is the case where there are only 2 children
delete' k (Node y z (Leaf w) (Leaf s) Nothing) =
  if (k == y) || (k == z) then
    (Node y z (Leaf w) (Leaf s) Nothing, True)
  else
    (Node y z (Leaf w) (Leaf s) Nothing, False)

-- Still need to recurse trying to find the leafs!
delete' k (Node y z lst mst t) =
  if k <= y then
    case delete' k lst of
      (tt, True) =>
        case mst of
          Node _ _ _ _ (Just _) => (delete'' k y z lst mst t, False)
          Node _ _ _ _ Nothing  =>
            case t of
              Just (Node na nb nc nd (Just ne)) =>
                (delete'' k y z lst (Node na nb nc nd (Just ne)) (Just mst), False)
              Just (Node _ _ _ _ Nothing) => (delete''' k y z lst mst t, False)
              -- In this case when lst is deleted only one node mst will
              -- remain and the tree will be unbalanced.
              Nothing => (delete''' k y z lst mst t, False)
      (tt, False) => (Node y z tt mst t, False)
  else
    if (k > y) && (k <= z) then
      case delete' k mst of
        (tt, True) =>
          case lst of
            Node _ _ _ _ (Just _) => (delete'' k y z mst lst t, False)
            Node _ _ _ _ Nothing  =>
              case t of
                Just (Node na nb nc nd (Just ne)) =>
                  (delete'' k y z mst (Node na nb nc nd (Just ne)) (Just lst), False)
                Just (Node _ _ _ _ Nothing) => (delete''' k y z mst lst t, False)
                -- In this case when mst is deleted then there will be a
                -- single node left just lst
                Nothing => (delete''' k y z mst lst t, False)
        (tt, False) => (Node y z lst tt t, False)
    else
      case t of
        Just ttt =>
          case delete' k ttt of
            (tt, True) =>
              case lst of
                Node _ _ _ _ (Just _) => (delete'' k y z ttt lst (Just mst), False)
                Node _ _ _ _ Nothing  =>
                  case mst of
                    Node _ _ _ _ (Just _) => (delete'' k y z ttt mst (Just lst), False)
                    Node _ _ _ _ Nothing => (delete''' k y z ttt lst (Just mst), False)
            (tt, False) => (Node y z lst mst (Just tt), False)
        Nothing => (Node y z lst mst t, False)
  where
  -- The case when the sibling has 3 kids
  delete'' : (k : a) -> (lm : a) -> (mm : a) -> (td : TwoThreeTree a)
             -> (sibling : TwoThreeTree a) -> (xtra: Maybe (TwoThreeTree a))
             -> TwoThreeTree a
  delete'' k lm mm td sibling xtra =
    let (nsibling, sc) = steal_third_child sibling in
      Node lm mm (remove_k_td k td sc) nsibling xtra
    where
    -- This is the only case that should happen here!
    steal_third_child : TwoThreeTree a -> (TwoThreeTree a, TwoThreeTree a)
    steal_third_child (Node x w s u (Just v)) = (Node x w s u Nothing, v)

    -- Here we need to delete "Leaf k" and replace it with sc
    remove_k_td : (Eq a, Ord a) => (k : a) -> (td : TwoThreeTree a)
                  -> (sc : TwoThreeTree a) -> TwoThreeTree a
    remove_k_td k (Node x w (Leaf s) (Leaf u) Nothing) sc =
      let scv = get_val sc in
        if k == s then
          if w <= scv then
            Node w scv (Leaf u) sc Nothing
          else
            Node scv w sc (Leaf u) Nothing
        else
          if x <= scv then
            Node x scv (Leaf s) sc Nothing
          else
            Node scv x sc (Leaf x) Nothing
       where
         get_val : TwoThreeTree a -> a
         get_val (Leaf vv) = vv

  -- The case when the siblings only have 2 kids
  delete''' : (k : a) -> (lm : a) -> (mm : a) -> (td : TwoThreeTree a)
             -> (sibling : TwoThreeTree a) -> (xtra : Maybe (TwoThreeTree a))
             -> TwoThreeTree a
  delete''' k lm mm td sibling xtra =
    let nsibling = Insert (remove_k_from_td k td) sibling in
      return_tree lm mm nsibling xtra
    where
    remove_k_from_td : a -> TwoThreeTree a -> a
    remove_k_from_td k (Node _ _ (Leaf ll) (Leaf rl) Nothing) =
      if k == ll then rl else ll

    return_tree : a -> a -> TwoThreeTree a -> Maybe (TwoThreeTree a)
                  -> TwoThreeTree a
    return_tree lm mm nsibling Nothing = nsibling
    -- XXX: This should be updated later on!
    return_tree lm mm nsibling (Just xxtra) = Node lm mm nsibling xxtra Nothing

-- Delete a key from the TwoThreeTree
Delete : (Eq a, Ord a) => a -> (TwoThreeTree a) -> TwoThreeTree a
Delete x [] = []
Delete x (Leaf y) =
  if x == y then []
  else (Leaf y)
Delete x t =
  if (lookup x t) then
    case (delete' x t) of
      (t, True) => remove_from_root t
      (t, False) => update_lm_mm t
  else
    t where
  remove_from_root : TwoThreeTree a -> TwoThreeTree a
  remove_from_root [] = []
  remove_from_root (Leaf x) = (Leaf x)
  remove_from_root (Node lm mm (Leaf l) (Leaf m) Nothing) =
    if x == l then
      Leaf m
    else Leaf l

-- Examples
aTwoThreeTree : TwoThreeTree Nat
aTwoThreeTree = (Node 10 11 (Node 8 9 (Leaf 8) (Leaf 9) (Just (Leaf 10)))
                           (Leaf 11) Nothing)

-- Example of insert
ct : TwoThreeTree Nat
ct = map (+ 1) (Node 10 14 (Leaf 10) (Leaf 14) (Just (Leaf 15)))

bt : TwoThreeTree Nat
bt = Insert 17 ct

dt : TwoThreeTree Nat
dt = Insert 18 bt

et : TwoThreeTree Nat
et = Insert 19 dt

ft : TwoThreeTree Nat
ft = Insert 14 dt

-- Examples of delete
gt : TwoThreeTree Nat
gt = Delete 18 ft

ht : TwoThreeTree Nat
ht = Delete 11 gt


text:
partial
bar : (n : Nat) -> (m : Nat) -> n = m -> Nat
bar (S m) (S m) (Refl {x = S m}) = m

data Baz : Int -> Type where
     AddThings : (x : Int) -> (y : Int) -> Baz (x + y)

addBaz : (x : Int) -> Baz x -> Int
addBaz (x + y) (AddThings x y) = x + y

-- Not allowed in Idris 2, we use unification rather than matching!
-- addBaz2 : (x : Int) -> Baz x -> Int
-- addBaz2 (_ + _) (AddThings x y) = x + y

-- Also not allowed in Idris 2!
-- addBaz3 : (x : Int) -> Baz x -> Int
-- addBaz3 (x + y) (AddThings _ _) = x + y


text:
module TestDoubles

put : Double -> IO ()
put = putStrLn . show

main : IO ()
main = do
    put $ exp 1
    put $ log 1

    put $ sin 1
    put $ cos 1
    put $ tan 1
    put $ asin 1
    put $ acos 1
    put $ atan 1

    put $ sqrt 2

    put $ floor 1.5
    put $ ceiling 1.5


text:
topten : Ord a => List a -> List a
topten l =
    let rsl = reverse (sort l) in
        take 10 rsl

max_stars_repo_name: curtisalexander/tdd-idris

max_issues_repo_name: curtisalexander/tdd-idris

max_forks_repo_name: curtisalexander/tdd-idris


text:
||| Common types and utility funtions for the LSP server implementation.
|||
||| (C) The Idris Community, 2021
module Server.Utils

import Core.Context
import Core.Core
import Core.FC
import Core.Name
import Core.Metadata
import Data.Bits
import Data.List
import Data.String
import Idris.Pretty
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.Message
import Libraries.Data.PosMap
import Server.Configuration
import System.File

||| Gets a specific component of a reference, using the supplied projection.
export
gets : (l : label) -> Ref l a => (a -> b) -> Core b
gets l f = f <$> get l

export
modify : (l : label) -> Ref l a => (a -> a) -> Core ()
modify l f = put l . f =<< get l

export
foldlM : Foldable t => (a -> b -> Core a) -> a -> t b -> Core a
foldlM f init = foldl (\ma, b => flip f b =<< ma) (pure init)

export
uncons' : List a -> Maybe (a, List a)
uncons' [] = Nothing
uncons' (x :: xs) = Just (x, xs)

||| Reads a single header from an LSP message on the supplied file handle.
||| Headers end with the string "\r\n".
export
fGetHeader : (h : File) -> Core (Either FileError String)
fGetHeader handle = do
  Right l <- coreLift $ fGetLine handle
    | Left err => pure $ Left err
  -- TODO: reading up to a string should probably be handled directly by the FFI primitive
  --       or at least in a more efficient way in Idris2
  if isSuffixOf "\r\n" l
     then pure $ Right l
     else (map (l ++)) <$> fGetHeader handle

-- From Language.JSON.Data
private
b16ToHexString : Bits16 -> String
b16ToHexString n =
  case n of
    0 => "0"
    1 => "1"
    2 => "2"
    3 => "3"
    4 => "4"
    5 => "5"
    6 => "6"
    7 => "7"
    8 => "8"
    9 => "9"
    10 => "A"
    11 => "B"
    12 => "C"
    13 => "D"
    14 => "E"
    15 => "F"
    other => assert_total $
               b16ToHexString (n `shiftR` fromNat 4) ++
               b16ToHexString (n .&. 15)

private
showChar : Char -> String
showChar c
  = case c of
         '\b' => "\\b"
         '\f' => "\\f"
         '\n' => "\\n"
         '\r' => "\\r"
         '\t' => "\\t"
         '\\' => "\\\\"
         '"'  => "\\\""
         c => if isControl c || c >= '\127'
                 then "\\u" ++ b16ToHexString (cast (ord c)) -- quick hack until b16ToHexString is available in Idris2
                 else singleton c

private
showString : String -> String
showString x = "\"" ++ concatMap showChar (unpack x) ++ "\""

export
stringify : JSON -> String
stringify JNull = "null"
stringify (JBoolean x) = if x then "true" else "false"
stringify (JNumber x) = let s = show x in
                            if isSuffixOf ".0" s
                               then substr 0 (length s `minus` 2) s
                               else s
stringify (JString x) = showString x
stringify (JArray xs) = "[" ++ stringifyValues xs ++ "]"
  where
    stringifyValues : List JSON -> String
    stringifyValues [] = ""
    stringifyValues (x :: xs) = stringify x
                             ++ if isNil xs
                                   then ""
                                   else "," ++ stringifyValues xs
stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}"
  where
    stringifyProp : (String, JSON) -> String
    stringifyProp (key, value) = showString key ++ ":" ++ stringify value

    stringifyProps : List (String, JSON) -> String
    stringifyProps [] = ""
    stringifyProps (x :: xs) = stringifyProp x
                            ++ if isNil xs
                                  then ""
                                  else "," ++ stringifyProps xs

export
findInTreeLoc' : FilePos -> FilePos -> PosMap (NonEmptyFC, a) -> List (NonEmptyFC, a)
findInTreeLoc' sp ep m = sortBy (\x, y => cmp (measure x) (measure y)) $ dominators (sp, ep) m
  where
    cmp : FileRange -> FileRange -> Ordering
    cmp ((sr1, sc1), (er1, ec1)) ((sr2, sc2), (er2, ec2)) =
      compare (er1 - sr1, ec1 - sc1) (er2 - sr2, ec2 - sc2)

export
findPointInTreeLoc' : FilePos -> PosMap (NonEmptyFC, a) -> List (NonEmptyFC, a)
findPointInTreeLoc' p = findInTreeLoc' p p

export
findInTreeLoc : FilePos -> FilePos -> PosMap (NonEmptyFC, a) -> Maybe (NonEmptyFC, a)
findInTreeLoc sp ep m = head' $ findInTreeLoc' sp ep m

export
findPointInTreeLoc : FilePos -> PosMap (NonEmptyFC, a) -> Maybe (NonEmptyFC, a)
findPointInTreeLoc p = findInTreeLoc p p

export
findInTree : FilePos -> FilePos -> PosMap (NonEmptyFC, a) -> Maybe a
findInTree sp ep m = snd <$> findInTreeLoc sp ep m

export
findPointInTree : FilePos -> PosMap (NonEmptyFC, a) -> Maybe a
findPointInTree p = findInTree p p

export
anyAt : (a -> Bool) -> a -> b -> Bool
anyAt p loc _ = p loc

export
anyWithName : Name -> (NonEmptyFC -> Bool) -> NonEmptyFC -> (Name, b) -> Bool
anyWithName name p loc (n, _) = p loc && name == n

export
Cast FilePos Position where
  cast (line, col) = MkPosition line col

export
Cast Position FilePos where
  cast (MkPosition line col) = (line, col)

export
Cast FC Range where
  cast (MkFC _ start end) = MkRange { start = cast start, end = cast end }
  cast (MkVirtualFC _ start end) = MkRange { start = cast start, end = cast end }
  cast EmptyFC = MkRange { start = MkPosition 0 0, end = MkPosition 0 0 }

export
Cast NonEmptyFC Range where
  cast (_, start, end) = MkRange { start = cast start, end = cast end }

public export
Measure (Range, a) where
  measure (r, _) = (cast r.start, cast r.end)

export
prettyTerm : PTerm -> Doc IdrisAnn
prettyTerm = reAnnotate Syntax . Pretty.prettyTerm

export
searchCache : Ref LSPConf LSPConfiguration => Range -> IdrisAction -> Core (List CodeAction)
searchCache r type = do
  cache <- gets LSPConf cachedActions
  let inRange = dominators (cast r.start, cast r.end) cache
  pure $ concatMap (snd . snd) $ filter (\(_, t, _) => type == t) inRange

export
pathToURI : String -> URI
pathToURI path =
  MkURI { scheme = "file"
        , authority = Just (MkURIAuthority Nothing "" Nothing)
        , path = path
        , query = ""
        , fragment = ""
        }

export
toStart : FC -> FC
toStart (MkFC f _ _) = MkFC f (0, 0) (0, 0)
toStart (MkVirtualFC f _ _) = MkVirtualFC f (0, 0) (0, 0)
toStart EmptyFC = EmptyFC


text:
module Libgit.Git

import System.FFI

import Libgit.FFI
import Libgit.Types

||| Runs some action within an initialized Git context. Initializes libgit2
||| static memory before running the action and shuts it down after running the
||| action. All managed Git resources must be accessed from within this context.
export
withGit : HasIO io => io b -> io (Either Int b)
withGit act = do
  err <- liftIO (primIO prim_libgit_init)
  case err < 0 of
    True => pure (Left err)
    False => do
      res <- act
      liftIO (primIO prim_libgit_shutdown)
      pure (Right res)

||| Get the last Git error, if present.
|||
||| Returns a tuple of a git error message and an error class code if a Git
||| error is present.
export
lastError : Maybe (String, Int)
lastError =
  let ptr = git_error_last in
    case is_null_ptr (prim__forgetPtr ptr) of
      1 => Nothing
      _ => let giterr = derefGitError ptr
               message = getField giterr "message"
               klass = getField giterr "klass"
               messageStr = getString message in
             Just (messageStr, klass)

max_forks_repo_name: bigs/libgit-idris


text:
-- Test for multiple field declarations on one line with the same type

record Person where
  constructor MkPerson
  firstName, middleName, lastName : String

fred : Person
fred = MkPerson "Fred" "Joe" "Bloggs"

main : IO ()
main = do printLn (firstName fred)
          printLn (middleName fred)
          printLn (lastName fred)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module IdrisJvm.Core.Inference

import IdrisJvm.Core.Asm
import IdrisJvm.Core.Common
import IdrisJvm.Core.Constant
import IdrisJvm.Core.ControlFlow
import IdrisJvm.Core.Foreign
import IdrisJvm.Core.Operator
import IdrisJvm.IR.Types
import Data.SortedMap

%access public export

addType : InferredTypeStore -> Int -> InferredType -> InferredTypeStore
addType types var ty = maybe addNew checkExisting $ lookup var types where
  addNew : InferredTypeStore
  addNew = insert var ty types

  checkExisting : InferredType -> InferredTypeStore
  checkExisting existingTy = insert var (existingTy <+> ty) types

addTypeForVars : InferredType -> List LVar -> InferredTypeStore -> InferredTypeStore
addTypeForVars ty [] acc = acc
addTypeForVars ty ((Loc v) :: args) acc = addTypeForVars ty args (addType acc v ty)

inferBinaryOp : InferredTypeStore -> InferredType -> LVar -> LVar -> InferredTypeStore
inferBinaryOp types ty (Loc op1) (Loc op2) = let typesWithFirstOp = addType types op1 ty
                                             in addType typesWithFirstOp op2 ty

inferUnaryOp : InferredTypeStore -> InferredType  -> LVar -> InferredTypeStore
inferUnaryOp types ty (Loc op) = addType types op ty

inferOp2 : InferredTypeStore -> PrimFn -> List LVar -> (InferredType, InferredTypeStore)
inferOp2 types (LIntStr (ITFixed IT64)) [x] = (inferredStringType, inferUnaryOp types ILong x)
inferOp2 types (LIntStr (ITFixed _)) [x] = (inferredStringType, inferUnaryOp types IInt x)
inferOp2 types (LIntStr ITNative) [x] = (inferredStringType, inferUnaryOp types IInt x)
inferOp2 types (LIntStr ITBig) [x] = (inferredStringType, inferUnaryOp types (inferredBigIntegerType) x)

inferOp2 types LFloatStr [x] = (inferredStringType, inferUnaryOp types IDouble x)

inferOp2 types (LChInt ITBig) [x] = (inferredBigIntegerType, inferUnaryOp types IChar x)

inferOp2 types (LChInt (ITFixed IT64)) [x] = (ILong, inferUnaryOp types IChar x)

inferOp2 types (LChInt _) [x] = (IInt, inferUnaryOp types IChar x)

inferOp2 types (LIntCh ITBig) [x] = (IChar, inferUnaryOp types (inferredBigIntegerType) x)

inferOp2 types (LIntCh (ITFixed IT64)) [x] = (IChar, inferUnaryOp types ILong x)

inferOp2 types (LIntCh _) [x] = (IChar, inferUnaryOp types IInt x)

inferOp2 types (LSExt ITNative ITBig) [x] = (inferredBigIntegerType, inferUnaryOp types IInt x)

inferOp2 types (LSExt (ITFixed IT64) ITBig) [x] = (inferredBigIntegerType, inferUnaryOp types ILong x)

inferOp2 types (LSExt (ITFixed _) ITBig) [x] = (inferredBigIntegerType, inferUnaryOp types IInt x)

inferOp2 types (LTrunc ITNative (ITFixed IT64)) [x] = (ILong, inferUnaryOp types IInt x)

inferOp2 types (LTrunc (ITFixed IT64) (ITFixed IT32)) [x] = (IInt, inferUnaryOp types ILong x)
inferOp2 types (LTrunc (ITFixed IT64) (ITFixed IT16)) [x] = (IInt, inferUnaryOp types ILong x)
inferOp2 types (LTrunc (ITFixed IT64) (ITFixed IT8)) [x] = (IInt, inferUnaryOp types ILong x)

inferOp2 types (LTrunc ITBig (ITFixed IT64)) [x] = (ILong, inferUnaryOp types inferredBigIntegerType x)
inferOp2 types (LTrunc ITBig (ITFixed _)) [x] = (IInt, inferUnaryOp types inferredBigIntegerType x)
inferOp2 types (LTrunc ITBig ITNative) [x] = (IInt, inferUnaryOp types inferredBigIntegerType x)

inferOp2 types (LTrunc (ITFixed _) (ITFixed _)) [x] = (IInt, inferUnaryOp types IInt x)

inferOp2 types LWriteStr [_, s] = (IInt, inferUnaryOp types inferredStringType s)

inferOp2 types LReadStr [_] = (inferredStringType, types)

inferOp2 types LStrConcat [l,r] = (inferredStringType, inferBinaryOp types (inferredStringType) l r)

inferOp2 types LStrCons [l,r] =
    let typesWithLeft =  inferUnaryOp types IChar l
    in  (inferredStringType, inferUnaryOp typesWithLeft (inferredStringType) r)

inferOp2 types LStrSubstr [offset, len, str] =
    let typesWithOffset = inferUnaryOp types IInt offset
        typesWithLen = inferUnaryOp typesWithOffset IInt len
    in (inferredStringType, inferUnaryOp typesWithLen (inferredStringType) str)

inferOp2 types (LStrInt ITBig) [x] = (inferredBigIntegerType, inferUnaryOp types (inferredStringType) x)

inferOp2 types (LStrInt (ITFixed IT8)) [x] = (IInt, inferUnaryOp types (inferredStringType) x)

inferOp2 types (LStrInt _) [x] = (IInt, inferUnaryOp types (inferredStringType) x)

inferOp2 types LStrFloat [x] = (IDouble, inferUnaryOp types (inferredStringType) x)

inferOp2 types (LSHL (ITFixed IT64)) [l, r] = (ILong, inferBinaryOp types ILong l r)

inferOp2 types (LSHL (ITFixed IT8)) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp2 types (LSHL (ITFixed _)) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp2 types (LLSHR (ITFixed IT64)) [l, r] = (ILong, inferBinaryOp types ILong l r)

inferOp2 types (LLSHR (ITFixed _)) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp2 types (LASHR (ITFixed IT64)) [l, r] = (ILong, inferBinaryOp types ILong l r)

inferOp2 types (LASHR (ITFixed _)) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp2 types LFork [x] = (Ref futureClass, types)

inferOp2 types LPar [x] = (Ref objectClass, types)

inferOp2 types (LIntFloat ITBig) [x] = (IDouble, inferUnaryOp types (inferredBigIntegerType) x)

inferOp2 types (LIntFloat ITNative) [x] = (IDouble, inferUnaryOp types IInt x)

inferOp2 types (LFloatInt ITBig) [x] = (inferredBigIntegerType, inferUnaryOp types IDouble x)

inferOp2 types (LFloatInt ITNative) [x] = (IInt, inferUnaryOp types IDouble x)

inferOp2 types LSystemInfo [x] = (inferredStringType, inferUnaryOp types IInt x)

inferOp2 types LCrash [x] = (IUnknown, inferUnaryOp types inferredStringType x)

inferOp2 types op _ = (IUnknown, types)

inferOpLLe : InferredTypeStore -> PrimFn -> List LVar -> (InferredType, InferredTypeStore)
inferOpLLe types (LLe ITBig) [l, r] = (IBool, inferBinaryOp types (inferredBigIntegerType) l r)
inferOpLLe types (LLe ITNative) [l, r] = (IBool, inferBinaryOp types IInt l r)
inferOpLLe types (LLe (ITFixed IT64)) [l, r] = (IBool, inferBinaryOp types ILong l r)
inferOpLLe types (LLe (ITFixed _)) [l, r] = (IBool, inferBinaryOp types IInt l r)

inferOpLLt : InferredTypeStore -> PrimFn -> List LVar -> (InferredType, InferredTypeStore)
inferOpLLt types (LLt ITBig) [l, r] = (IBool, inferBinaryOp types (inferredBigIntegerType) l r)
inferOpLLt types (LLt ITNative) [l, r] = (IBool, inferBinaryOp types IInt l r)
inferOpLLt types (LLt (ITFixed IT64)) [l, r] = (IBool, inferBinaryOp types ILong l r)
inferOpLLt types (LLt (ITFixed _)) [l, r] = (IBool, inferBinaryOp types IInt l r)

inferOpLGt : InferredTypeStore -> PrimFn -> List LVar -> (InferredType, InferredTypeStore)
inferOpLGt types (LGt ITBig) [l, r] = (IBool, inferBinaryOp types (inferredBigIntegerType) l r)
inferOpLGt types (LGt ITNative) [l, r] = (IBool, inferBinaryOp types IInt l r)
inferOpLGt types (LGt (ITFixed IT64)) [l, r] = (IBool, inferBinaryOp types ILong l r)
inferOpLGt types (LGt (ITFixed _)) [l, r] = (IBool, inferBinaryOp types IInt l r)

inferOp : InferredTypeStore -> PrimFn -> List LVar -> (InferredType, InferredTypeStore)
inferOp types (LAnd (ITFixed IT64)) [l, r] = (ILong, inferBinaryOp types ILong l r)
inferOp types (LAnd (ITFixed _)) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LAnd ITNative) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp types (LOr (ITFixed IT64)) [l, r] = (ILong, inferBinaryOp types ILong l r)
inferOp types (LOr (ITFixed _)) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LOr ITNative) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp types (LXOr (ITFixed IT64)) [l, r] = (ILong, inferBinaryOp types ILong l r)
inferOp types (LXOr (ITFixed _)) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LXOr ITNative) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp types (LCompl (ITFixed IT64)) [x] = (ILong, inferUnaryOp types ILong x)
inferOp types (LCompl (ITFixed _)) [x] = (IInt, inferUnaryOp types IInt x)
inferOp types (LCompl ITNative) [x] = (IInt, inferUnaryOp types IInt x)

inferOp types llt@(LLt _) args = inferOpLLt types llt args

inferOp types lle@(LLe _) args = inferOpLLe types lle args

inferOp types lgt@(LGt _) args = inferOpLGt types lgt args

inferOp types (LGe ITBig) [l, r] = inferOp types (LSGe (ATInt ITBig)) [l, r]
inferOp types (LGe ITNative) [l, r] = (IBool, inferBinaryOp types IInt l r)
inferOp types (LGe (ITFixed IT64)) [l, r] = (IBool, inferBinaryOp types ILong l r)
inferOp types (LGe (ITFixed _)) [l, r] = (IBool, inferBinaryOp types IInt l r)

inferOp types (LPlus ATFloat) [l, r] = (IDouble, inferBinaryOp types IDouble l r)
inferOp types (LPlus (ATInt ITBig)) [l, r] =
    (inferredBigIntegerType, inferBinaryOp types (inferredBigIntegerType) l r)

inferOp types (LPlus (ATInt ITNative)) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LPlus (ATInt ITChar)) [l, r] = (IChar, inferBinaryOp types IChar l r)

inferOp types (LPlus (ATInt (ITFixed IT64))) [l, r] = (ILong, inferBinaryOp types ILong l r)
inferOp types (LPlus (ATInt (ITFixed IT8))) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LPlus (ATInt (ITFixed _))) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp types (LMinus ATFloat) [l, r] = (IDouble, inferBinaryOp types IDouble l r)
inferOp types (LMinus (ATInt ITBig)) [l, r] =
    (inferredBigIntegerType, inferBinaryOp types (inferredBigIntegerType) l r)

inferOp types (LMinus (ATInt ITNative)) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LMinus (ATInt (ITFixed IT64))) [l, r] = (ILong, inferBinaryOp types ILong l r)
inferOp types (LMinus (ATInt (ITFixed _))) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp types (LTimes ATFloat) [l, r] = (IDouble, inferBinaryOp types IDouble l r)
inferOp types (LTimes (ATInt ITBig)) [l, r] =
    (inferredBigIntegerType, inferBinaryOp types (inferredBigIntegerType) l r)

inferOp types (LTimes (ATInt ITNative)) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LTimes (ATInt (ITFixed IT64))) [l, r] = (ILong, inferBinaryOp types ILong l r)
inferOp types (LTimes (ATInt (ITFixed IT8))) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LTimes (ATInt (ITFixed _))) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp types (LSDiv ATFloat) [l, r] = (IDouble, inferBinaryOp types IDouble l r)
inferOp types (LSDiv (ATInt ITBig)) [l, r] =
    (inferredBigIntegerType, inferBinaryOp types (inferredBigIntegerType) l r)

inferOp types (LSDiv (ATInt ITNative)) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LSDiv (ATInt (ITFixed IT64))) [l, r] = (ILong, inferBinaryOp types ILong l r)
inferOp types (LSDiv (ATInt (ITFixed _))) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp types (LUDiv ITNative) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LUDiv (ITFixed IT64)) [l, r] = (ILong, inferBinaryOp types ILong l r)

inferOp types (LUDiv ITBig) [l, r] =
    (inferredBigIntegerType, inferBinaryOp types (inferredBigIntegerType) l r)
inferOp types (LUDiv (ITFixed _)) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp types (LSRem ATFloat) [l, r] = (IDouble, inferBinaryOp types IDouble l r)
inferOp types (LSRem (ATInt ITBig)) [l, r] =
    (inferredBigIntegerType, inferBinaryOp types (inferredBigIntegerType) l r)

inferOp types (LSRem (ATInt ITNative)) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LSRem (ATInt (ITFixed IT64))) [l, r] = (ILong, inferBinaryOp types ILong l r)
inferOp types (LSRem (ATInt (ITFixed _))) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp types (LURem (ITFixed IT64)) [l, r] = (ILong, inferBinaryOp types ILong l r)
inferOp types (LURem ITNative) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LURem (ITFixed IT32)) [l, r] = (IInt, inferBinaryOp types IInt l r)
inferOp types (LURem ITBig) [l, r] =
    (inferredBigIntegerType, inferBinaryOp types (inferredBigIntegerType) l r)
inferOp types (LURem (ITFixed _)) [l, r] = (IInt, inferBinaryOp types IInt l r)

inferOp types (LEq ATFloat) [l, r] = (IBool, inferBinaryOp types IDouble l r)
inferOp types (LEq (ATInt ITBig)) [l, r] = (IBool, inferBinaryOp types (inferredBigIntegerType) l r)
inferOp types (LEq (ATInt ITChar)) [l, r] = (IBool, inferBinaryOp types IChar l r)
inferOp types (LEq (ATInt ITNative)) [l, r] = (IBool, inferBinaryOp types IInt l r)
inferOp types (LEq (ATInt (ITFixed IT64))) [l, r] = (IBool, inferBinaryOp types ILong l r)
inferOp types (LEq (ATInt (ITFixed _))) [l, r] = (IBool, inferBinaryOp types IInt l r)

inferOp types (LSLt ATFloat) [l, r] = (IBool, inferBinaryOp types IDouble l r)
inferOp types (LSLt (ATInt ITNative)) [l, r] = (IBool, inferBinaryOp types IInt l r)
inferOp types (LSLt (ATInt ITBig)) [l, r] =
    (IBool, inferBinaryOp types (inferredBigIntegerType) l r)
inferOp types (LSLt (ATInt ITChar)) [l, r] = (IBool, inferBinaryOp types IChar l r)
inferOp types (LSLt (ATInt (ITFixed IT64))) [l, r] = (IBool, inferBinaryOp types ILong l r)
inferOp types (LSLt (ATInt (ITFixed _))) [l, r] = (IBool, inferBinaryOp types IInt l r)

inferOp types (LSLe ATFloat) [l, r] = (IBool, inferBinaryOp types IDouble l r)
inferOp types (LSLe (ATInt ITNative)) [l, r] = (IBool, inferBinaryOp types IInt l r)
inferOp types (LSLe (ATInt ITBig)) [l, r] =
    (IBool, inferBinaryOp types (inferredBigIntegerType) l r)
inferOp types (LSLe (ATInt ITChar)) [l, r] = (IBool, inferBinaryOp types IChar l r)
inferOp types (LSLe (ATInt (ITFixed IT64))) [l, r] = (IBool, inferBinaryOp types ILong l r)
inferOp types (LSLe (ATInt (ITFixed _))) [l, r] = (IBool, inferBinaryOp types IInt l r)

inferOp types (LSGt ATFloat) [l, r] = (IBool, inferBinaryOp types IDouble l r)
inferOp types (LSGt (ATInt ITNative)) [l, r] = (IBool, inferBinaryOp types IInt l r)
inferOp types (LSGt (ATInt ITBig)) [l, r] =
    (IBool, inferBinaryOp types (inferredBigIntegerType) l r)
inferOp types (LSGt (ATInt ITChar)) [l, r] = (IBool, inferBinaryOp types IChar l r)
inferOp types (LSGt (ATInt (ITFixed IT64))) [l, r] = (IBool, inferBinaryOp types ILong l r)
inferOp types (LSGt (ATInt (ITFixed _))) [l, r] = (IBool, inferBinaryOp types IInt l r)

inferOp types (LSGe ATFloat) [l, r] = (IBool, inferBinaryOp types IDouble l r)
inferOp types (LSGe (ATInt ITNative)) [l, r] = (IBool, inferBinaryOp types IInt l r)
inferOp types (LSGe (ATInt ITBig)) [l, r] =
    (IBool, inferBinaryOp types (inferredBigIntegerType) l r)
inferOp types (LSGe (ATInt ITChar)) [l, r] = (IBool, inferBinaryOp types IChar l r)
inferOp types (LSGe (ATInt (ITFixed IT64))) [l, r] = (IBool, inferBinaryOp types ILong l r)
inferOp types (LSGe (ATInt (ITFixed _))) [l, r] = (IBool, inferBinaryOp types IInt l r)

inferOp types LStrEq [l,r] = (IBool, inferBinaryOp types inferredStringType l r)

inferOp types LStrRev [var] = (inferredStringType, inferUnaryOp types inferredStringType var)

inferOp types LStrLen [var] = (IInt, inferUnaryOp types inferredStringType var)

inferOp types LStrLt [l, r] = (IBool, inferBinaryOp types inferredStringType l r)

inferOp types LStrHead [var] = (IChar, inferUnaryOp types inferredStringType var)

inferOp types LStrIndex [string, index] =
    let stringTyped = inferUnaryOp types (inferredStringType) string
        stringAndIndexTyped = inferUnaryOp stringTyped IInt index
    in (IChar, stringAndIndexTyped)

inferOp types LStrTail [var] = (inferredStringType, inferUnaryOp types (inferredStringType) var)

inferOp types (LZExt ITNative ITBig) [var] = (inferredBigIntegerType, inferUnaryOp types IInt var)
inferOp types (LZExt (ITFixed IT64) ITBig) [var] = (inferredBigIntegerType, inferUnaryOp types ILong var)
inferOp types (LZExt (ITFixed from) ITBig) [var] = (inferredBigIntegerType, inferUnaryOp types IInt var)

inferOp types (LZExt ITNative (ITFixed IT64)) [x] = (ILong, inferUnaryOp types IInt x)
inferOp types (LZExt (ITFixed from) (ITFixed IT64)) [x] = (ILong, inferUnaryOp types IInt x)

inferOp types (LZExt ITNative (ITFixed to)) [x] = (IInt, inferUnaryOp types IInt x)
inferOp types (LZExt (ITFixed IT64) ITNative) [x] = (IInt, inferUnaryOp types ILong x)
inferOp types (LZExt (ITFixed from) ITNative) [x] = (IInt, inferUnaryOp types IInt x)
inferOp types (LZExt ITChar ITNative) [x] = (IInt, inferUnaryOp types IChar x)
inferOp types (LZExt ITChar (ITFixed to)) [x] = (IInt, inferUnaryOp types IChar x)

inferOp types (LZExt (ITFixed IT64) ITChar) [x] = (IChar, inferUnaryOp types ILong x)
inferOp types (LZExt (ITFixed to) ITChar) [x] = (IChar, inferUnaryOp types IInt x)

inferOp types op args = inferOp2 types op args

inferForeignArgDescs : InferredTypeStore -> List (FieldTypeDescriptor, LVar) -> InferredTypeStore
inferForeignArgDescs types [] = types
inferForeignArgDescs types ((fieldTyDesc, x) :: rest) =
    let inferredTy = fieldTypeDescriptorToInferredType fieldTyDesc
    in inferForeignArgDescs (inferUnaryOp types inferredTy x) rest

inferConstExp : InferredTypeStore -> Const -> (InferredType, InferredTypeStore)
inferConstExp acc (B8 i) = (IInt, acc)
inferConstExp acc (B16 i) = (IInt, acc)
inferConstExp acc (B32 i) = (IInt, acc)
inferConstExp acc (B64 i) = (ILong, acc)
inferConstExp acc (I i) = (IInt, acc)
inferConstExp acc (Fl d) = (IDouble, acc)
inferConstExp acc (Ch c) = (IChar, acc)
inferConstExp acc (BI i) = (inferredBigIntegerType, acc)
inferConstExp acc (Str s) = (inferredStringType, acc)
inferConstExp acc TheWorld = (IInt, acc)
inferConstExp acc x = if isTypeConst x
              then (IInt, acc)
              else jerror $ "Constant " ++ show x ++ " not compilable yet"

inferFunctionAppArgs : InferredTypeStore -> InferredTypeStore -> List LVar -> InferredTypeStore
inferFunctionAppArgs calledFunctionArgTypes types args =
    let lookupType = \argPos => fromMaybe inferredObjectType $ SortedMap.lookup (cast $ the Nat argPos) calledFunctionArgTypes
        argsLength = length args
        argIndices = if argsLength > 0 then [0 .. (Nat.pred argsLength)] else []
    in foldl
         (\acc, (pos, arg) => addType acc (locIndex arg) (lookupType pos))
         types
         (List.zip argIndices args)

combineTypes : List InferredType -> InferredType
combineTypes [] = IUnknown
combineTypes (ty :: rest) = go ty rest where
  go : InferredType -> List InferredType -> InferredType
  go prevTy [] = prevTy
  go prevTy (currTy :: rest) =
    if prevTy == currTy then
        go currTy rest
    else
        inferredObjectType

mutual
    inferIfElseTy : InferenceConfig -> InferredTypeStore -> LVar -> SExp -> SExp -> (InferredType, InferredTypeStore)
    inferIfElseTy config acc (Loc i) trueAlt falseAlt =
        let ifVarInferred = addType acc i IBool
            (falseRetTy, falseAltTypes) = inferExp config ifVarInferred falseAlt
            (trueRetTy, trueAltTypes) = inferExp config ifVarInferred trueAlt
        in (falseRetTy <+> trueRetTy, merge falseAltTypes trueAltTypes)

    inferNullableIfElseTy : InferenceConfig -> InferredTypeStore -> LVar -> SExp -> SExp -> (InferredType, InferredTypeStore)
    inferNullableIfElseTy config acc (Loc i) trueAlt falseAlt =
        let ifVarInferred = addType acc i inferredObjectType
            (falseRetTy, falseAltTypes) = inferExp config ifVarInferred falseAlt
            (trueRetTy, trueAltTypes) = inferExp config ifVarInferred trueAlt
        in (falseRetTy <+> trueRetTy, merge falseAltTypes trueAltTypes)

    inferAltConCase : InferenceConfig -> InferredTypeStore -> Int -> List String -> SExp -> (InferredType, InferredTypeStore)
    inferAltConCase config types lv args expr = inferExp config typesWithPropTypes expr where
      argsLength : Int
      argsLength = cast $ length args

      typesWithPropTypes : InferredTypeStore
      typesWithPropTypes = if argsLength == 0 then types else go types lv (pred argsLength) where
        go : InferredTypeStore -> Int -> Int -> InferredTypeStore
        go types lv 0 = addType types lv inferredObjectType
        go types lv n = go (addType types (lv + n) inferredObjectType) lv (pred n)

    inferAlt : InferenceConfig -> InferredTypeStore -> SAlt -> (InferredType, InferredTypeStore)
    inferAlt config types (SConstCase _ expr) = inferExp config types expr
    inferAlt config types (SDefaultCase expr) = inferExp config types expr
    inferAlt config types (SConCase lv _ _ args expr) = inferAltConCase config types lv args expr

    inferSwitch : InferenceConfig -> InferredTypeStore -> LVar -> List SAlt -> (InferredType, InferredTypeStore)
    inferSwitch config types (Loc e) alts =
        let switchExprType =
                if isConstructorSwitchCases alts then
                    inferredObjectType
                else if isIntSwitchCases alts then
                    IInt
                else if isCharSwitchCases alts then
                    IChar
                else
                    IUnknown
            altTypes = inferAlt config (addType types e switchExprType) <$> alts

        in (combineTypes $ fst <$> altTypes, concat $ snd <$> altTypes)

    inferExp : InferenceConfig -> InferredTypeStore -> SExp -> (InferredType, InferredTypeStore)
    inferExp config acc (SV (Glob _)) = (inferredObjectType, acc)
    inferExp config acc (SV (Loc i)) = (fromMaybe IUnknown $ lookup i acc, acc)

    inferExp config acc (SApp True f args) =
        let calledFunctionName = jname f
        in
          if calledFunctionName == functionName config then
            (IUnknown, acc)
          else maybe (Ref thunkClass, acc) inferArgs $ lookup calledFunctionName (functionTypes config) where
             inferArgs : InferredFunctionType -> (InferredType, InferredTypeStore)
             inferArgs fty = (Ref thunkClass, inferFunctionAppArgs (locsType fty) acc args)

    inferExp config acc (SApp False f args) =
      maybe (inferredObjectType, acc) inferArgs $ lookup (jname f) (functionTypes config) where
        inferArgs : InferredFunctionType -> (InferredType, InferredTypeStore)
        inferArgs fty = (returnType fty, inferFunctionAppArgs (locsType fty) acc args)

    inferExp config acc (SLet (Loc i) v sc) =
        let (vty, nacc) = inferExp config acc v
            naccWithI = addType nacc i vty
        in inferExp config naccWithI sc

    inferExp config acc (SUpdate _ e) = inferExp config acc e
    inferExp config acc (SProj (Loc v) i) = (inferredObjectType, addType acc v inferredIdrisObjectType)

    inferExp config acc (SCon _ 0 "Prelude.Bool.False" []) = (IBool, acc)
    inferExp config acc (SCon _ 1 "Prelude.Bool.True" []) = (IBool, acc)

    inferExp config acc (SCon _ t _ args) = (inferredIdrisObjectType, addTypeForVars inferredObjectType args acc)
    inferExp config acc (SCase _ e ((SConCase _ 0 "Prelude.Bool.False" [] falseAlt) ::
                             (SConCase _ 1 "Prelude.Bool.True" [] trueAlt) ::
                             _)) = inferIfElseTy config acc e trueAlt falseAlt

    inferExp config acc (SCase _ e ((SConCase _ 1 "Prelude.Bool.True" [] trueAlt) ::
                            (SDefaultCase falseAlt) ::
                            _))
        = inferIfElseTy config acc e trueAlt falseAlt

    inferExp config acc (SCase _ e ((SConCase _ 0 "Prelude.Bool.False" [] falseAlt) ::
                        (SDefaultCase trueAlt) ::
                        _))
        = inferIfElseTy config acc e trueAlt falseAlt

    inferExp config acc (SCase _ e [SDefaultCase defaultExpr]) = inferExp config acc defaultExpr

    inferExp config acc (SCase _ e alts) =
        if any defaultCase alts
            then inferSwitch config acc e alts
            else inferSwitch config acc e (alts ++ [SDefaultCase SNothing])

    inferExp config acc (SChkCase e [SDefaultCase defaultExpr]) = inferExp config acc defaultExpr
    inferExp config acc (SChkCase e alts) = inferSwitch config acc e alts

    inferExp config acc (SConst c) = inferConstExp acc c

    inferExp config acc (SOp op args) = inferOp acc op args

    inferExp config acc SNothing = (inferredObjectType, acc)

    inferExp config acc (SError x) = (inferredObjectType, acc)

    inferExp config acc (SForeign returns fdesc args) = case parseDescriptor returns fdesc args of
        JLambda clazz _ => (Ref clazz, acc)
        _ =>
            let argsWithTypes = (\(fdesc, lvar) => (fdescFieldDescriptor fdesc, lvar)) <$> args
                returnDesc = fdescTypeDescriptor returns
            in (typeDescriptorToInferredType returnDesc, inferForeignArgDescs acc argsWithTypes)

inferFun : SortedMap JMethodName InferredFunctionType -> SDecl -> InferredFunctionType
inferFun types (SFun name args locs def) =
  let jmethodName = jname name
      config = MkInferenceConfig jmethodName types
      initialArgsTypes = fromMaybe SortedMap.empty $ locsType <$> lookup jmethodName types
      (returnType, locsType) = inferExp config initialArgsTypes def
  in MkInferredFunctionType jmethodName returnType locsType (length args)


text:
libsmall : String -> String
libsmall fn = "C:" ++ fn ++ ",libsmallc"

%foreign (libsmall "add")
add : Int -> Int -> Int

%foreign (libsmall "addWithMessage")
prim__addWithMessage : String -> Int -> Int -> PrimIO Int

addWithMessage : String -> Int -> Int -> IO Int
addWithMessage s x y = primIO $ prim__addWithMessage s x y

%foreign (libsmall "applyFn")
prim__applyFn : String -> Int -> (String -> Int -> String) -> PrimIO String

applyFn : String -> Int -> (String -> Int -> String) -> IO String
applyFn c i f = primIO $ prim__applyFn c i f

%foreign (libsmall "applyFn")
prim__applyFnIO : String -> Int -> (String -> Int -> PrimIO String) -> PrimIO String

applyFnIO : String -> Int -> (String -> Int -> IO String) -> IO String
applyFnIO c i f = primIO $ prim__applyFnIO c i (\s, i => toPrim $ f s i)

pluralise : String -> Int -> IO String
pluralise str x
    = do putStrLn "Pluralising"
         pure $ show x ++ " " ++
                if x == 1
                   then str
                   else str ++ "s"

main : IO ()
main
    = do -- printLn (add 70 24)
         -- primIO $ prim__addWithMessage "Sum" 70 24
         str1 <- applyFnIO "Biscuit" 10 pluralise
         putStrLn str1
         str2 <- applyFnIO "Tree" 1 pluralise
         putStrLn str2


text:
module ReadNum

import Data.Strings

%default total

readNumber : HasIO io => io (Maybe Nat)
readNumber = do n <- getLine
                if all isDigit (unpack n)
                   then pure $ Just (stringToNatOrZ n)
                   else pure Nothing

readNumbers : HasIO io => io (Maybe (Nat, Nat))
readNumbers = do m <- readNumber
                 case m of
                      Nothing => pure Nothing
                      Just mm => do n <- readNumber
                                    case n of
                                         Nothing => pure Nothing
                                         Just nn => pure $ Just (mm, nn)

-- pattern-matched destucturing

readNumbersImproved : HasIO io => io (Maybe (Nat, Nat))
readNumbersImproved = do Just m <- readNumber | Nothing => pure Nothing
                         Just n <- readNumber | Nothing => pure Nothing
                         pure $ Just (m, n)

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module CommutativityOfAddition

%default total

sym_eq : x = y -> y = x
sym_eq Refl = Refl

tr_eq : x = y -> y = z -> x = z
tr_eq Refl Refl = Refl

congr : (P : a -> b) -> x = y -> P x = P y
congr f Refl = Refl

-- x = x + 0
sym_plus_z : {m : Nat} -> m = m + 0
sym_plus_z {m=Z} = Refl
-- sym_plus_z {m=(S k)} = congr S (sym_plus_z{m=k})
sym_plus_z {m=(S k)} = rewrite sym_plus_z{m=k} in Refl

-- S x = 1 + x
sym_plus_one_left : {m : Nat} -> S m = 1 + m
sym_plus_one_left = Refl

-- S x = x + 1
sym_plus_one_right : {m : Nat} -> S m = m + 1
sym_plus_one_right {m=Z} = Refl
sym_plus_one_right {m=(S k)} =
    rewrite sym_plus_one_right{m=k} in Refl

proof11 : {m : Nat} -> S m + m = S (m + m)
proof11 {m = Z}     = Refl
proof11 {m = (S k)} = Refl

proof12 : {m : Nat} -> {a : Nat} -> a + (S m) = S (a + m)
-- 0 + (S m) = S (0 + m)
proof12 {m=m} {a=Z} = Refl
proof12 {m=m} {a=(S k)} = rewrite proof12{m=m}{a=k} in Refl

-- S x + S x = S (S (x + x))
export
-- S (S x) + S (S x) = S (S (S S (x + x)))
sumSucc : {m : Nat} -> S m + S m = S (S (m + m))
-- -- S 0 + S 0 = S (S (0 + 0))
sumSucc {m=Z} = Refl
-- S (S k) + S (S k) = S (S ((S k) + (S k)))
sumSucc {m=m} = let rec = proof12{m=m}{a=m} -- (S m) + (S m) = S ((S m) + m)
             in rewrite rec
             in Refl

proof2 : {x: Nat} -> {y: Nat} -> S x + S y = S (S (x + y))
proof2 {x=Z} {y=Z}           = Refl
proof2 {x=Z} {y=(S k)}       = Refl
proof2 {x=(S k)}  {y=Z}      = rewrite proof2{x=k}{y=Z} in Refl
proof2 {x=(S kx)} {y=(S ky)} = rewrite proof2{x=kx}{y=(S ky)} in Refl

proof3 : {x, y: Nat} -> {y: Nat} -> S (x + y) = x + (S y)
proof3 {x=Z}{y=y} = Refl
proof3 {x=(S k)}{y=y} =      -- S (S k + y) = S k + (S y)
    let p = proof3{x=k}{y=y} --   S (k + y) = k + (S y)
    in congr S p
    -- rewrite proof3{x=k}{y=y} --   S (k + y) = k + (S y)
    -- in Refl                  --  (k + (S y) = k + (S y)
                                --  S (S k + y) = S (k + (S y))
    -- replace{P=\w => S (S k + y) = S w} (proof3{x=k}{y=y}) Refl{x=(S k + y)}

sym_plus : {x,y:Nat} -> x + y = y + x
sym_plus {x=Z}{y=Z}           = Refl
sym_plus {x=Z}{y=(S k)}       = sym_plus_z
sym_plus {x=(S k)}{y=Z}       = sym_eq sym_plus_z
-- sym_plus_z = 0 + x = x + 0
sym_plus {x=(S kx)}{y=(S ky)} =       --  S kx + y = y + S kx
    let p1 = sym_plus{x=kx}{y=(S ky)}    -- kx + y = y + kx
        p2 =  proof3{x=(S ky)}{y=kx} -- S (y + kx) = y + (S kx)
    in tr_eq (congr S p1) p2
-- proof3 : S (x + y) = x + (S y)

max_stars_repo_name: GoPavel/idris-proof

max_issues_repo_name: GoPavel/idris-proof

max_forks_repo_name: GoPavel/idris-proof


text:
module FreshPerm

import FreshList
import Data.Fin
import Data.Vect

||| An arrangement is a list of fins of a given length
||| and range.
public export
Arrangement : Nat -> Nat -> Type
Arrangement len range = FreshVect len (Fin range) (/=)

||| A permutation is an arrangement where each fin appears n times
||| and the fins range from 0 to n
public export
Permutation : Nat -> Type
Permutation n = Arrangement n n

weakenInj : (x : Fin k) -> (y : Fin k) -> So (not (x == y)) -> So (not (weaken x == weaken y))
weakenInj FZ FZ z = z
weakenInj FZ (FS x) z = z
weakenInj (FS x) FZ z = z
weakenInj (FS x) (FS y) z = weakenInj x y z

easyNeq : (y : Fin n) -> So ((Fin.last /= (Fin.weaken y)))
easyNeq FZ = Oh
easyNeq (FS x) = easyNeq x

freshWeakend : (fs : Arrangement l r) ->
               So ((Fin.last) ## map Fin.weaken {Bneq=(/=)} weakenInj fs)
freshWeakend [] = Oh
freshWeakend (x :: xs) = andSo (easyNeq _, freshWeakend xs)

reversePermutation : (n : Nat) -> Permutation n
newFresh : (n : Nat) -> So (Fin.last {n}
                           ## map Fin.weaken {Bneq = (/=)} FreshPerm.weakenInj (reversePermutation n))

reversePermutation 0 = []
reversePermutation (S k) =
    (::) (last {n=k})
       (FreshList.map weaken {Bneq = (/=)} weakenInj (reversePermutation k)) {fresh = newFresh k}

newFresh n = freshWeakend (reversePermutation n)

flip : {a, b : Fin n} -> So (a /= b) -> So (b /= a)
flip {a = FZ} {b = FZ} x = x
flip {a = FZ} {b = (FS y)} x = x
flip {a = (FS y)} {b = FZ} x = x
flip {a = (FS y)} {b = (FS z)} x = flip x

export
append : (f : Fin n) -> (fs : Arrangement l n) -> {0 notIn : So (f ## fs)} -> Arrangement (S l) n
freshlyAppend : {x, f : Fin n} ->
                {xs : Arrangement l n} ->
                {fneq : So (f ## xs)} ->
                (notEq : So (x /= f)) ->
                (fresh : So (x ## xs)) ->
                So (x ## append {notIn = fneq} f xs)

append f [] = [f]
append f ((x :: xs) {fresh}) = let 0 p = soAnd notIn in
                                   (::) x (append f {notIn = snd p} xs)
                                   {fresh = freshlyAppend (flip $ fst p) fresh}

freshlyAppend notEq fresh {xs = []} = andSo (notEq, Oh)
freshlyAppend notEq fresh {xs = (y :: xs)} =
  let (a, b) = soAnd fresh in
      andSo (a, freshlyAppend notEq b)

export
reverse : Arrangement l n -> Arrangement l n

0 freshlyReversed : (x, xs : _) -> So (x ## xs) -> So (x ## FreshPerm.reverse xs)

reverse [] = []
reverse ((::) x xs {fresh}) = append x (reverse xs) {notIn = freshlyReversed x xs fresh}

freshlyReversed x [] y = Oh
freshlyReversed x (z :: xs) y with (soAnd y)
  freshlyReversed x (z :: xs) y | (w, v) =
    freshlyAppend {xs= reverse xs} {f=z} w (freshlyReversed ? xs v)

export
identityPermutation : (n : Nat) -> Permutation n
identityPermutation n = reverse (reversePermutation n)

extractVal : (Fin (S n)) -> Vect (S n) a -> (a, Vect n a)
extractVal FZ (x :: xs) = (x, xs)
extractVal (FS FZ) (y :: (x :: xs)) = (x, y :: xs)
extractVal (FS (FS x)) (y :: (z :: xs)) with (extractVal (FS x) (z :: xs))
  extractVal (FS (FS x)) (y :: (z :: xs)) | (k, ks) = (k, y :: ks)

applyPermutation : (1 _ : Permutation n) -> (1 _ : Vect n a) -> Vect n a
applyPermutation [] [] = []
applyPermutation (x :: xs) (y :: ys) =
  let (val, res) = extractVal x (y :: ys) in
      val :: applyPermutation ?kek res

max_stars_repo_name: andrevidela/dev-notes

max_issues_repo_name: andrevidela/dev-notes

max_forks_repo_name: andrevidela/dev-notes


text:
module Sigma

import Basic
import Unit
import Void

infixr 0 #
public export
data Sigma : (a : Type) -> (p : a -> Type) -> Type where
  (#) : (x : a) -> p x -> Sigma a p

public export
Pair : Type -> Type -> Type
Pair a b = Sigma a (const b)

public export
pr1 : Sigma a p -> a
pr1 (x # _) = x

public export
pr2 : (s : Sigma a p) -> p (pr1 s)
pr2 (_ # y) = y

public export
SigmaInduction : (q : Sigma a p -> Type)
              -> ((x : a) -> (y : p x) -> q (x # y))
              -> (s : Sigma a p) -> q s
SigmaInduction _ f (x # y) = f x y

public export
uncurry : (q : Sigma a p -> Type)
       -> ((x : a) -> (y : p x) -> q (x # y))
       -> (s : Sigma a p) -> q s
uncurry = SigmaInduction

public export
curry : (q : Sigma a p -> Type)
     -> ((s : Sigma a p) -> q s)
     -> ((x : a) -> (y : p x) -> q (x # y))
curry _ f x y = f (x # y)


text:
-- --------------------------------------------------------------- [ Paths.idr ]
-- Module    : Test.System.Posix.Paths
-- Copyright : (c) 2017 Josh Filstrup
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

module Paths

import System.Posix.Paths

assertEq : (Show a, Show b, Eq b) => (id : String) -> (fn : a -> b)
           -> (input : a) -> (expected : b) -> IO Bool
assertEq id f input expected = let res = f input in
                                  if res == expected
                                    then do putStrLn ("Test " ++ id ++ " passed!")
                                            pure True
                                    else do putStrLn ("Test " ++ id ++ " failed!")
                                            putStrLn ("\t Expected: " ++ (show expected))
                                            putStrLn ("\t Actual: " ++ (show res))
                                            putStrLn ("\t Input: " ++ (show input))
                                            pure False

concatTestImpl : String -> (Maybe (Path t Directory))
                        -> (Maybe (Path Relative k)) -> String -> IO Bool
concatTestImpl id (Just left) (Just right) expected = let concatFn = Paths.concat left in
                                                        assertEq id (show . concatFn) right expected
concatTestImpl id _ _ _ = do putStrLn ("Test " ++ id ++ " failed! (Invalid args)")
                             pure False

fileExtTestImpl : String -> (Maybe (Path a File)) -> String -> IO Bool
fileExtTestImpl id (Just path) expected = assertEq id (show . Paths.getFileExtension) path expected
fileExtTestImpl id _ _ = do putStrLn ("Test " ++ id ++ " failed! (Invalid args)")
                            pure False

dirNameTestImpl : String -> (Maybe (Path a File)) -> String -> IO Bool
dirNameTestImpl id (Just path) expected = assertEq id (show . Paths.getDirectoryName) path expected
dirNameTestImpl id _ _ = do putStrLn ("Test " ++ id ++ " failed! (Invalid args)")
                            pure False

export
test_DirectoryName : IO ()
test_DirectoryName = do putStrLn "--------------------------------------------"
                        putStrLn "Running test_DirectoryName"
                        putStrLn "--------------------------------------------"

                        (dirNameTestImpl
                          "test_DirectoryName/absoluteFile"
                          (mkAbsoluteFile "/foo/bar/baz.txt")
                          "Just \"/foo/bar\"")

                        (dirNameTestImpl
                          "test_DirectoryName/relativeFile"
                          (mkRelativeFile "./foo/bar/baz.txt")
                          "Just \"foo/bar\"")

                        (dirNameTestImpl
                          "test_DirectoryName/absoluteFileRoot"
                          (mkAbsoluteFile "/")
                          "Nothing")

                        putStrLn ""

export
test_FileExtension : IO ()
test_FileExtension = do putStrLn "--------------------------------------------"
                        putStrLn "Running test_FileExtension"
                        putStrLn "--------------------------------------------"

                        (fileExtTestImpl
                          "test_FileExtension/absolute"
                          (mkAbsoluteFile "/foo/bar/baz.txt")
                          "Just \"txt\"")

                        (fileExtTestImpl
                          "test_FileExtension/relative"
                          (mkRelativeFile "./foo/bar/baz.txt")
                          "Just \"txt\"")

                        (fileExtTestImpl
                          "test_FileExtension/relativeNoExtension"
                          (mkRelativeFile "./foo/bar/baz")
                          "Nothing")

                        (fileExtTestImpl
                          "test_FileExtension/absoluteNoExtension"
                          (mkAbsoluteFile "/foo/bar/baz")
                          "Nothing")

                        putStrLn ""

export
test_Concatenation : IO ()
test_Concatenation = do putStrLn "--------------------------------------------"
                        putStrLn "Running test_Concatenation"
                        putStrLn "--------------------------------------------"

                        (concatTestImpl
                          "test_Concatenation/absRelFile"
                          (mkAbsoluteDirectory "/foo/bar")
                          (mkRelativeFile "temp.txt")
                          "Absolute File: /foo/bar/temp.txt")

                        (concatTestImpl
                          "test_Concatenation/absRelDir"
                          (mkAbsoluteDirectory "/foo/bar")
                          (mkRelativeDirectory "temp")
                          "Absolute Directory: /foo/bar/temp")

                        (concatTestImpl
                          "test_Concatenation/relRelFile"
                          (mkRelativeDirectory "./foo/bar")
                          (mkRelativeFile "temp.txt")
                          "Relative File: foo/bar/temp.txt")

                        (concatTestImpl
                          "test_Concatenation/relRelDir"
                          (mkRelativeDirectory "./foo/bar")
                          (mkRelativeDirectory "temp")
                          "Relative Directory: foo/bar/temp")

                        (concatTestImpl
                          "test_Concatenation/normalize"
                          (mkRelativeDirectory "./foo///bar//baz")
                          (mkRelativeDirectory "temp/")
                          "Relative Directory: foo/bar/baz/temp")

                        putStrLn ""

export
test_MkRelativeFile : IO ()
test_MkRelativeFile = do putStrLn "--------------------------------------------"
                         putStrLn "Running test_MkRelativeFile"
                         putStrLn "--------------------------------------------"

                         (assertEq
                           "test_MkRelativeFile/basic"
                           (show . Paths.mkRelativeFile)
                           "./foo/bar/temp.txt"
                           "Just Relative File: foo/bar/temp.txt")

                         (assertEq
                           "test_MkRelativeFile/absolute"
                           (show . Paths.mkRelativeFile)
                           "/foo/bar/temp.txt"
                           "Nothing")

                         (assertEq
                           "test_MkRelativeFile/normalized"
                           (show . Paths.mkRelativeFile)
                           "foo/bar///baz//temp.txt"
                           "Just Relative File: foo/bar/baz/temp.txt")

                         (assertEq
                           "test_MkRelativeFile/relativeSpecifiers"
                           (show . Paths.mkRelativeFile)
                           "foo/bill/../bar/../baz/temp.txt"
                           "Just Relative File: foo/baz/temp.txt")

                         putStrLn ""

export
test_MkRelativeDirectory : IO ()
test_MkRelativeDirectory = do putStrLn "--------------------------------------------"
                              putStrLn "Running test_MkRelativeDirectory"
                              putStrLn "--------------------------------------------"

                              (assertEq
                                "test_MkRelativeDirectory/basic"
                                (show . Paths.mkRelativeDirectory)
                                "./foo/bar/"
                                "Just Relative Directory: foo/bar")

                              (assertEq
                                "test_MkRelativeDirectory/absolute"
                                (show . Paths.mkRelativeDirectory)
                                "/foo/bar/"
                                "Nothing")

                              (assertEq
                                "test_MkRelativeDirectory/normalized"
                                (show . Paths.mkRelativeDirectory)
                                "foo/bar///baz//"
                                "Just Relative Directory: foo/bar/baz")

                              (assertEq
                                "test_MkRelativeDirectory/relativeSpecifiers"
                                (show . Paths.mkRelativeDirectory)
                                "foo/bill/../bar/../baz/"
                                "Just Relative Directory: foo/baz")

                              putStrLn ""

export
test_MkAbsoluteFile : IO ()
test_MkAbsoluteFile = do putStrLn "--------------------------------------------"
                         putStrLn "Running test_MkAbsoluteFile"
                         putStrLn "--------------------------------------------"

                         (assertEq
                           "test_MkAbsoluteDirectory/basic"
                           (show . Paths.mkAbsoluteFile)
                           "/foo/bar/baz.txt"
                           "Just Absolute File: /foo/bar/baz.txt")

                         (assertEq
                           "test_MkAbsoluteDirectory/normalized"
                           (show . Paths.mkAbsoluteFile)
                           "/foo//bar/////baz.txt"
                           "Just Absolute File: /foo/bar/baz.txt")

                         (assertEq
                           "test_MkAbsoluteDirectory/relative"
                           (show . Paths.mkAbsoluteFile)
                           "./foo/bar/baz.txt"
                           "Nothing")

                         (assertEq
                           "test_MkAbsoluteDirectory/relativeSpecifiers"
                           (show . Paths.mkAbsoluteFile)
                           "/foo/../bar/../baz.txt"
                           "Nothing")

                         putStrLn ""

export
test_MkAbsoluteDirectory : IO ()
test_MkAbsoluteDirectory = do putStrLn "--------------------------------------------"
                              putStrLn "Running test_MkAbsoluteDirectory"
                              putStrLn "--------------------------------------------"

                              (assertEq
                                "test_MkAbsoluteDirectory/basic"
                                (show . Paths.mkAbsoluteDirectory)
                                "/foo/bar/"
                                "Just Absolute Directory: /foo/bar")

                              (assertEq
                                "test_MkAbsoluteDirectory/normalized"
                                (show . Paths.mkAbsoluteDirectory)
                                "/foo/bar///baz/"
                                "Just Absolute Directory: /foo/bar/baz")

                              (assertEq
                                "test_MkAbsoluteDirectory/normalized2"
                                (show . Paths.mkAbsoluteDirectory)
                                "/foo/../bar///baz/"
                                "Nothing")

                              (assertEq
                                "test_MkAbsoluteDirectory/missingFrontSlash"
                                (show . Paths.mkAbsoluteDirectory)
                                "foo/bar/"
                                "Nothing")

                              (assertEq
                                "test_MkAbsoluteDirectory/tildeExists"
                                (show . Paths.mkAbsoluteDirectory)
                                "~/foo/bar/"
                                "Nothing")

                              putStrLn ""

export
test_Normalization : IO ()
test_Normalization = do putStrLn "--------------------------------------------"
                        putStrLn "Running test_Normalization"
                        putStrLn "--------------------------------------------"

                        (assertEq
                          "test_Normalization/tooManySlashes"
                          (Paths.normalize Absolute)
                          "//foo/bar//baz////billy/"
                          "/foo/bar/baz/billy")

                        (assertEq
                          "test_Normalization/dotSlashPrefix"
                          (Paths.normalize Relative)
                          "./hello/there"
                          "hello/there")

                        (assertEq
                          "test_Normalization/doubleDots"
                          (Paths.normalize Relative)
                          "hello/../there"
                          "there")

                        (assertEq
                          "test_Normalization/manyDoubleDots"
                          (Paths.normalize Relative)
                          "hello/../there/billy/../"
                          "there")

                        (assertEq
                          "test_Normalization/rootPath"
                          (Paths.normalize Absolute)
                          "/"
                          "/")

                        putStrLn ""

export
test_Eq : IO ()
test_Eq = do putStrLn "--------------------------------------------"
             putStrLn "Running test_Eq"
             putStrLn "--------------------------------------------"

             (assertEq
                "test_Eq/basic"
                ((==) (mkAbsoluteDirectory "/foo/bar"))
                (mkAbsoluteDirectory "/foo/bar")
                True)

             (assertEq
                "test_Eq/basic2"
                ((==) (mkAbsoluteDirectory "/foo/bar"))
                (mkAbsoluteDirectory "/foo/bar/baz")
                False)

             putStrLn ""

max_stars_repo_name: superfunc/dtp

max_issues_repo_name: superfunc/dtp

max_forks_repo_name: superfunc/dtp


text:
||| Interface to string.h of STDC
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Foreign.Memory.String

%default total

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

%foreign "C,memcpy,libc 6"
export prim__memcpy : (dst:AnyPtr) -> (src:AnyPtr) -> (bytes:Int) -> PrimIO AnyPtr

%foreign "C,memmove,libc 6"
export prim__memmove : (dst:AnyPtr) -> (src:AnyPtr) -> (bytes:Int) -> PrimIO AnyPtr

%foreign "C,memccpy,libc 6"
export prim__memccpy : (dst:AnyPtr) -> (src:AnyPtr) -> (c:Int) -> (bytes:Int) -> PrimIO AnyPtr

%foreign "C,memset,libc 6"
export prim__memset : (p:AnyPtr) -> (c:Int) -> (bytes:Int) -> PrimIO AnyPtr

%foreign "C,memcmp,libc 6"
export prim__memcmp : (lhs:AnyPtr) -> (rhs:AnyPtr) -> (bytes:Int) -> PrimIO Int

%foreign "C,memchr,libc 6"
export prim__memchr : (p:AnyPtr) -> (c:Int) -> (bytes:Int) -> PrimIO AnyPtr

%foreign "C,memchrr,libc 6"
export prim__memchrr : (p:AnyPtr) -> (c:Int) -> (bytes:Int) -> PrimIO AnyPtr

%foreign "C,strcpy,libc 6"
export prim__strcpy : (dst:Ptr Char) -> (src:Ptr Char) -> PrimIO String
%foreign "C,strncpy,libc 6"
export prim__strncpy : (dst:Ptr Char) -> (src:Ptr Char) -> (n:Int) -> PrimIO String

%foreign "C,strcat,libc 6"
export prim__strcat : (dst:Ptr Char) -> (src:Ptr Char) -> PrimIO String
%foreign "C,strncat,libc 6"
export prim__strncat : (dst:Ptr Char) -> (src:Ptr Char) -> (n:Int) -> PrimIO String

-- strcmp, strncmp, strcoll, strxfrm, strcoll_l, strxfrm_l
-- strdup, strndup, strchr, strrchr, strspn, strcspn, strpbrk
-- strstr, strtok, strtok_r, strcasestr, strlen, strerror, strerror_r, strerror_l
-- strsep, strsignal, strpcpy, strpncpy, strtry, memfrob
-- basename

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

-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Main

import Data.Vect

data DataStore : Type where
  MkData : (size : Nat) ->
           (items : Vect size String) ->
           DataStore

size : DataStore -> Nat
size (MkData size' items') = size'

items : (store : DataStore) -> Vect (size store) String
items (MkData size' items') = items'

search : (store : DataStore) -> String -> List String
search (MkData _ items) q = filter (isInfixOf q) (toList items)

search' : (store : DataStore) -> String -> List (Nat, String)
search' (MkData size items) q
  = filter ((isInfixOf q) . snd)
           (zip (enumFromTo 0 size) (toList items))

addToStore : DataStore -> String -> DataStore
addToStore (MkData size items) item = MkData _ (addToData items)
  where
    addToData : Vect old String -> Vect (S old) String
    addToData [] = [item]
    addToData (x :: xs) = x :: addToData xs

sumInputs : Integer -> String -> Maybe (String, Integer)
sumInputs sum input
  = let val = cast input in
        if val < 0
        then Nothing
        else let newVal = sum + val in
                 Just ("Subtotal: " ++ show newVal ++ "\n", newVal)

data Command = Add String
             | Get Integer
             | Search String
             | Size
             | Quit

parseCommand : (cmd : String) -> (args : String) -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" val = case all isDigit (unpack val) of
                              False => Nothing
                              True => Just (Get (cast val))
parseCommand "search" query = Just (Search query)
parseCommand "size" "" = Just Size
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

parse : (input : String) -> Maybe Command
parse input = case span (/= ' ') input of
                   (cmd, args) => parseCommand cmd (ltrim args)

getEntry : (store : DataStore) -> (id : Integer) -> Maybe String
getEntry store id = let items = items store in
                    flip index items <$> integerToFin id (size store)

processCommand : (store : DataStore) -> (cmd : Command) -> Maybe (String, DataStore)
processCommand store (Add item)
  = Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
processCommand store (Get id) = case getEntry store id of
                                     Just item => Just (item ++ "\n", store)
                                     Nothing => Just ("Out of range\n", store)
processCommand store (Search query)
  = let results = search' store query
        results' = map (\(k, v) => show k ++ ": " ++ v) results in
        Just (unlines results' ++ "\n", store)
processCommand store Size = Just ("Size: " ++ show (size store) ++ "\n", store)
processCommand store Quit = Nothing

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
  = case parse input of
         Nothing => Just ("Invalid command\n", store)
         Just cmd => processCommand store cmd

main : IO ()
main = replWith (MkData _ [])  "Command: " processInput

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Ch04.NaturalInduction

-- TODO: Figure out how to implement the function below (if it's at all possible).

--natural_induction_principle : {a,b : Type} ->
--                              (size : a -> Nat) ->
--                              (f : (x : a) -> Either b (x' : a ** LT (size x') (size x))) ->
--                              (g : (a -> b) ** (x : a) -> (case f x of
--                                                                Left y => (g x = y)
--                                                                Right (y ** _) => (g x = g y)))

lemma : {x : Nat} ->
        LTE x 0 ->
        (x = 0)
lemma {x = Z} pf = Refl
lemma {x = (S k)} pf = absurd (succNotLTEzero pf)

public export
inductive_construction : {a,b : Type} ->
                         (size : a -> Nat) ->
                         (f : (x : a) -> Either b (x' : a ** LT (size x') (size x))) ->
                         a -> b
inductive_construction {a} {b} size f x = helper x (size x) lteRefl where
  helper : (x : a) -> (k : Nat) -> LTE (size x) k -> b
  helper x k bound = case f x of
                          Left y => y
                          Right (x' ** pf) => case k of
                                                    Z => let temp = replace (lemma bound) pf in
                                                             absurd (succNotLTEzero temp)
                                                    (S j) => helper x' j (fromLteSucc (lteTransitive pf bound))

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl