text:
||| Spec: https://webassembly.github.io/spec/core/valid/types.html#external-types
module WebAssembly.Validation.Types.ExternalTypes

import WebAssembly.Structure.Types
import WebAssembly.Validation.Types.Limits
import WebAssembly.Validation.Types.FunctionTypes
import WebAssembly.Validation.Types.TableTypes
import WebAssembly.Validation.Types.MemoryTypes
import WebAssembly.Validation.Types.GlobalTypes

-------------------------------------------------------------------------------
-- Validation Rules
-------------------------------------------------------------------------------

public export
data ValidExternalType : (externType : ExternType) -> Type where
  MkValidExternFunkType   : (externType : ExternType) -> (externType = Func funcType)     -> (ValidFunctionType funcType) -> ValidExternalType externType
  MkValidExternTableType  : (externType : ExternType) -> (externType = Table tableType)   -> (ValidTableType tableType)   -> ValidExternalType externType
  MkValidExternMemType    : (externType : ExternType) -> (externType = Mem memType)       -> (ValidMemoryType memType)    -> ValidExternalType externType
  MkValidExternGlobalType : (externType : ExternType) -> (externType = Global globalType) -> (ValidGlobalType globalType) -> ValidExternalType externType

-------------------------------------------------------------------------------
-- Lemmas about external-type validation
-------------------------------------------------------------------------------

total ext_invalid_func_type : (contra : ValidFunctionType funcType -> Void) -> ValidExternalType (Func funcType) -> Void
ext_invalid_func_type contra (MkValidExternFunkType (Func funcType) Refl x) = contra x
ext_invalid_func_type _ (MkValidExternTableType (Func _) Refl _) impossible
ext_invalid_func_type _ (MkValidExternMemType (Func _) Refl _) impossible
ext_invalid_func_type _ (MkValidExternGlobalType (Func _) Refl _) impossible

total ext_valid_func_type : (prof : ValidFunctionType funcType) -> ValidExternalType (Func funcType)
ext_valid_func_type (MkValidFunctionType funcType)
  = MkValidExternFunkType (Func funcType) Refl (MkValidFunctionType funcType)

total ext_invalid_table_type : (contra : ValidTableType tableType -> Void) -> ValidExternalType (Table tableType) -> Void
ext_invalid_table_type _ (MkValidExternFunkType (Table _) Refl _) impossible
ext_invalid_table_type contra (MkValidExternTableType (Table tableType) Refl x) = contra x
ext_invalid_table_type _ (MkValidExternMemType (Table _) Refl _) impossible
ext_invalid_table_type _ (MkValidExternGlobalType (Table _) Refl _) impossible

total ext_valid_table_type : (prof : ValidTableType tableType) -> ValidExternalType (Table tableType)
ext_valid_table_type (MkValidTableType limits elementType limits_valid)
  = MkValidExternTableType (Table (limits, elementType)) Refl (MkValidTableType limits elementType limits_valid)

total ext_invalid_mem_type : (contra : ValidMemoryType memType -> Void) -> ValidExternalType (Mem memType) -> Void
ext_invalid_mem_type _ (MkValidExternFunkType (Mem _) Refl _) impossible
ext_invalid_mem_type _ (MkValidExternTableType (Mem _) Refl _) impossible
ext_invalid_mem_type contra (MkValidExternMemType (Mem memType) Refl x) = contra x
ext_invalid_mem_type _ (MkValidExternGlobalType (Mem _) Refl _) impossible

total ext_valid_mem_type : (prof : ValidMemoryType memType) -> ValidExternalType (Mem memType)
ext_valid_mem_type (MkValidMemoryType memType limits_valid) = MkValidExternMemType (Mem memType) Refl (MkValidMemoryType memType limits_valid)

total ext_invalid_global_type : (contra : ValidGlobalType globalType -> Void) -> ValidExternalType (Global globalType) -> Void
ext_invalid_global_type _ (MkValidExternFunkType (Global _) Refl _) impossible
ext_invalid_global_type _ (MkValidExternTableType (Global _) Refl _) impossible
ext_invalid_global_type _ (MkValidExternMemType (Global _) Refl _) impossible
ext_invalid_global_type contra (MkValidExternGlobalType (Global globalType) Refl x) = contra x

total ext_valid_global_type : (prof : ValidGlobalType globalType) -> ValidExternalType (Global globalType)
ext_valid_global_type (MkGlobalValidType globalType) = MkValidExternGlobalType (Global globalType) Refl (MkGlobalValidType globalType)

-------------------------------------------------------------------------------
-- Decidablity of Validation
-------------------------------------------------------------------------------

total public export
isValidExternalType : (externType : ExternType) -> Dec (ValidExternalType externType)
isValidExternalType (Func funcType) = case (isFunctionTypeValid funcType) of
  No contra => No (ext_invalid_func_type contra)
  Yes prof  => Yes (ext_valid_func_type prof)
isValidExternalType (Table tableType) = case (isTableTypeValid tableType) of
  No contra => No (ext_invalid_table_type contra)
  Yes prof  => Yes (ext_valid_table_type prof)
isValidExternalType (Mem memType) =  case (isMemoryTypeValid memType) of
  No contra => No (ext_invalid_mem_type contra)
  Yes prof  => Yes (ext_valid_mem_type prof)
isValidExternalType (Global globalType) =  case (isGlobalTypeValid globalType) of
  No contra => No (ext_invalid_global_type contra)
  Yes prof  => Yes (ext_valid_global_type prof)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Sixel.Library

import Data.Buffer

public export
c : String -> String
c symbol = "C:" ++ symbol ++ ",libc"

public export
sixel : String -> String
sixel symbol = "C:" ++ symbol ++ ",libsixel"

public export
sixelutils : String -> String
sixelutils symbol = "C:" ++ symbol ++ ",libsixelutils"

%foreign (sixelutils "sixel_utils_is_concrete")
sixel_utils_is_concrete : Ptr t -> Int

%foreign (sixelutils "sixel_utils_is_concrete")
sixel_utils_is_concrete_any : AnyPtr -> Int

export
prim__isConcrete : Ptr t -> Bool
prim__isConcrete = intToBool . sixel_utils_is_concrete

export
prim__isConcreteAny : AnyPtr -> Bool
prim__isConcreteAny = intToBool . sixel_utils_is_concrete_any

export
%foreign (sixelutils "sixel_utils_pointer_cast")
prim__toString : Ptr t -> String

export
%foreign (sixelutils "sixel_utils_pointer_cast")
prim__toStringAny : AnyPtr -> String

export
%foreign (sixelutils "sixel_utils_buffer_null")
prim__getNullBuffer : Buffer

ext: idr

max_stars_repo_name: Kaiepi/id-sixel

max_issues_repo_name: Kaiepi/id-sixel

max_forks_repo_name: Kaiepi/id-sixel


text:
module Data.Vect.Extra

import Data.Vect

%access export
%default total

namespace Equality
   vecEq : Eq type => Vect n type -> Vect m type -> Bool
   vecEq [] [] = True
   vecEq [] (x :: xs) = False
   vecEq (x :: xs) [] = False
   vecEq (x :: xs) (y :: ys) = x == y && vecEq xs ys

namespace Decidable
  namespace SameLength
    decEq : DecEq type
          => (n = m)
          -> (xs : Vect n type)
          -> (ys : Vect m type)
          -> Dec (xs = ys)
    decEq Refl xs ys with (decEq xs ys)
      decEq Refl ys ys | (Yes Refl) = Yes Refl
      decEq Refl xs ys | (No contra) = No contra

  namespace DiffLength

    vectorsDiffLength : DecEq type
                      => (contra : (n = m) -> Void)
                      -> {xs : Vect n type}
                      -> {ys : Vect m type}
                      -> (xs = ys) -> Void
    vectorsDiffLength contra Refl = contra Refl

    decEq : DecEq type
         => (xs : Vect n type)
         -> (ys : Vect m type)
         -> Dec (xs = ys)
    decEq xs ys {n} {m} with (decEq n m)
      decEq xs ys {n = m} {m = m} | (Yes Refl) = decEq Refl xs ys
      decEq xs ys {n = n} {m = m} | (No contra) = No (vectorsDiffLength contra)


text:
module Libraries.Data.DList

%default total

-- Do not re-export the type so that it does not get unfolded in goals
-- and error messages!
export
DList : Type -> Type
DList a = List a -> List a

export
Nil : DList a
Nil = id

export
(::) : a -> DList a -> DList a
(::) a as = (a ::) . as

export
snoc : DList a -> a -> DList a
snoc as a = as . (a ::)

export
appendR : DList a -> List a -> DList a
appendR as bs = as . (bs ++)

export
appendL : List a -> DList a -> DList a
appendL as bs = (as ++) . bs

export
(++) : DList a -> DList a -> DList a
(++) = (.)

export
reify : DList a -> List a
reify as = as []

-- NB: No Functor instance because it's too expensive to reify, map, put back
-- Consider using a different data structure if you need mapping (e.g. a rope)


text:
module Client.Client

import Client.Action.Archive
import Client.Action.Build
import Client.Action.BuildDeps
import Client.Action.Clean
import Client.Action.Check
import Client.Action.Exec
import Client.Action.FetchDeps
import Client.Action.Init
import Client.Action.Login
import Client.Action.Pull
import Client.Action.Push
import Client.Action.Register
import Client.Action.Repl
import Client.Action.Test
import Client.Server
import Client.Skeleton.Skeleton
import Client.Util
import Data.List
import Data.Maybe
import Data.String
import Extra.Either
import Extra.String
import Fmt
import Inigo.Account.Account
import Inigo.Async.Promise
import Inigo.Package.CodeGen
import SemVar
import System

||| TODO: Overall, this should be converted to a
|||       better dependently-typed CLI system
fail : String -> IO ()
fail str =
  do
    putStrLn str
    exitFailure

-- Note: not total
requirePrompt : String -> (String -> List String) -> IO String
requirePrompt prompt validator =
  do
    putStr prompt
    x <- map trim $ getLine
    case validator x of
      [] =>
        pure x
      errs =>
        do
          putStrLn (fmt "Invalid: %s\n" (join ", " errs))
          requirePrompt prompt validator

data Action : Type where
  Archive : String -> String -> Action
  Build : CodeGen -> Action
  BuildDeps : Bool -> Action
  Clean : Bool -> Action
  Check : Action
  Exec : CodeGen -> List String -> Action
  Extract : String -> String -> Action
  FetchDeps : Server -> Bool -> Bool -> Action
  Init :
    String -> -- template file
    String -> -- package ns
    String -> -- package name
    Action
  Login : Server -> Action
  Pull : Server -> String -> String -> (Maybe Version) -> Action
  Push : Server -> String -> Action
  Register : Server -> Action
  Repl : Action
  Test : CodeGen -> Action

fetchDepsAction : String -> Bool -> Bool -> Maybe Action
fetchDepsAction serverName includeDevDeps build =
  do
    server <- getServer serverName
    pure $ FetchDeps server includeDevDeps build

getAction : List String -> Maybe Action
getAction ["archive", packageFile, outFile] =
  Just (Archive packageFile outFile)

getAction ["extract", archiveFile, outPath] =
  Just (Extract archiveFile outPath)

getAction ("build-deps" :: args) =
  let
    dev = any (== "--dev") args
  in
    Just (BuildDeps dev)

getAction ["build", codeGen] =
  do
    codeGen <- getCodeGen codeGen
    pure $ Build codeGen

getAction ["build"] =
  Just (Build Node)

getAction ["clean"] =
  Just (Clean False)

getAction ["clean", "deps"] =
  Just (Clean True)

getAction ["check"] =
  Just Check

getAction ("exec" :: args) =
  do
    let (execArgs, progArgs) = splitArgs args
    case execArgs of
      [] => Just (Exec Node progArgs)
      [cg] => Just (Exec !(getCodeGen cg) progArgs)
      _ => Nothing
  where
    splitArgs : List String -> (List String, List String)
    splitArgs [] = ([], [])
    splitArgs ("--" :: args) = ([], args)
    splitArgs (arg :: args) = mapFst (arg ::) (splitArgs args)

getAction ("fetch-deps" :: serverName :: extraArgs) =
  let
    build = not $ any (== "--no-build") extraArgs
    includeDevDeps = any (== "--dev") extraArgs
  in
    fetchDepsAction serverName includeDevDeps build

getAction ["push", serverName, archive] =
  do
    server <- getServer serverName
    pure $ Push server archive

getAction ["pull", serverName, packageNS, packageName] =
  do
    server <- getServer serverName
    pure $ Pull server packageNS packageName Nothing

getAction ["pull", serverName, packageNS, packageName, versionStr] =
  do
    server <- getServer serverName
    version <- parseVersion versionStr
    pure $ Pull server packageNS packageName (Just version)

getAction ["test", codeGen] =
  do
    codeGen <- getCodeGen codeGen
    pure $ Test codeGen

getAction ["test"] =
  pure $ Test Node

getAction ["register", serverName] =
  do
    server <- getServer serverName
    pure $ Register server

getAction ["repl"] =
    pure Repl

getAction ["login", serverName] =
  do
    server <- getServer serverName
    pure $ Login server

getAction ["init", packageNS, packageName, tmplFile] =
  Just (Init tmplFile packageNS packageName)

getAction _ = Nothing

getActionIO : IO (Maybe Action)
getActionIO =
  map (getAction . drop 2) getArgs

runAction : Action -> IO ()
runAction (Archive packageFile outFile) =
  do
    putStrLn ("Archiving " ++ packageFile ++ " to " ++ outFile)
    run (buildArchive packageFile outFile)

runAction (Extract archiveFile outPath) =
  do
    putStrLn ("Extracting " ++ archiveFile ++ " from " ++ outPath)
    run (extractArchive archiveFile outPath)

runAction (BuildDeps dev) =
  run $ buildDeps dev

runAction (Build codeGen) =
  run (build codeGen)

runAction (Clean deps) =
  run (clean deps)

runAction Check =
  run check

runAction (Exec codeGen userArgs) =
  run (exec codeGen True userArgs) -- TODO: Make build a flag

runAction (FetchDeps server includeDevDeps build) =
  do
    putStrLn ("Feching deps from " ++ toString server ++ (if includeDevDeps then " including dev deps" else ""))
    run $ fetchAllDeps server includeDevDeps build

runAction (Push server archive) =
  do
    Just session <- readSessionFile
      | Nothing => fail "Must be logged in to push package."
    putStrLn ("Pushing " ++ archive ++ " to " ++ toString server)
    run (push server session archive)

runAction (Pull server packageNS packageName mVersion) =
  do
    putStrLn (fmt "Pulling %s.%s [%s] from %s" packageNS packageName (show mVersion) (toString server))
    run (pull server packageNS packageName mVersion)

runAction (Register server) =
  do
    putStrLn "Welcome to Inigo. Let's create an account."
    ns <- requirePrompt "Namespace [your username]: " nsValid
    email <- requirePrompt "Email: " emailValid
    passphrase <- requirePrompt "Passphrase: " passphraseValid
    putStrLn (fmt "Creating account %s..." ns)
    run (registerAccount server ns email passphrase)

runAction Repl = run repl

runAction (Login server) =
  do
    putStrLn "Welcome back to Inigo."
    ns <- requirePrompt "Namespace [your username]: " nsValid
    passphrase <- requirePrompt "Passphrase: " (const [])
    putStrLn "Logging in..."
    run (loginAccount server ns passphrase)

runAction (Init tmplFile packageNS packageName) = do
    putStrLn (fmt "Initializing new inigo application %s.%s from template %s" packageNS packageName tmplFile)
    run (init tmplFile packageNS packageName)

runAction (Test codeGen) =
  run (test codeGen)

short : Action -> String
short (Archive _ _)     = "archive <pkg_file> <out_file>: Archive a given package"
short (Build _)         = "build <code-gen=node>: Build program under given code gen"
short (BuildDeps _)     = "build-deps: Build all deps"
short (Clean _)         = "clean <deps?>: Clean package artifacts, optionally including deps"
short Check             = "check: Typecheck the project"
short (Exec _ _)        = "exec <code-gen=node> -- ...args: Execute program with given args"
short (Extract _ _)     = "extract <archive_file> <out_path>: Extract a given archive to directory"
short (FetchDeps _ _ _) = "fetch-deps <server>: Fetch and build all deps (opts: --no-build, --dev)"
short (Init _ _ _)      = "init <namespace> <package> <template.inigo>: Initialize a new project with given namespace and package name"
short (Login _)         = "login <server>: Login to an account"
short (Pull _ _ _ _)    = "pull <server> <package_ns> <package_name> <version?>: Pull a package from remote"
short (Push _ _)        = "push <server> <pkg_file>: Push a package to remote"
short (Register _)      = "register <server>: Register an account namespace"
short Repl              = "repl: Launch idris2 repl"
short (Test _)          = "test: Run tests via IdrTest"

usage : IO ()
usage =
  let
    descs = join "\n\t" $
      map short
        [ (Archive "" "")
        , (Build Node)
        , (BuildDeps False)
        , (Clean False)
        , Check
        , (Exec Node [])
        , (Extract "" "")
        , (FetchDeps Prod False False)
        , (Init "" "" "")
        , (Login Prod)
        , (Pull Prod "" "" Nothing)
        , (Push Prod "")
        , (Register Prod)
        , Repl
        , (Test Node)
        ]
  in
    fail ("usage: Inigo <command> <...args>\n\n\t" ++ descs)

main : IO ()
main =
  do
    Just action <- getActionIO
      | Nothing => usage
    runAction action

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Control.Algebra.ZZGCDOfVectAlg

import Control.Algebra
import Classes.Verified
import Control.Algebra.VectorSpace

import Data.ZZ
import Control.Algebra.NumericInstances
import Control.Algebra.ZZVerifiedInstances

import Data.Matrix
import Data.Matrix.Algebraic
import Data.Matrix.AlgebraicVerified
import Data.Matrix.LinearCombinations -- for (vectVectLScalingCompatibility)

import Data.Vect.Structural

import Control.Algebra.ZZDivisors

import Data.Fin.FinOrdering
import Data.Fin.Structural

{-
(bezQTy) is the only thing actually used from here,
something req.d to potentially generalize to other Bezout domains.
-}
import Control.Algebra.ZZBezoutsIdentity

-- Dependent pattern matching using (do) notation binds improves clarity
import Control.Monad.Identity
import Syntax.PreorderReasoning

import Control.Algebra.DiamondInstances

%default total

{-
Table of contents:
* Lemmas about extending a GCD to more than 2 numbers
* The extension of a GCD of 2 numbers to that of a Vect of numbers
-}

{-
Lemmas about extending a GCD to more than 2 numbers
-}

vectGCDFnExtension : ( t : Fin n -> ZZ )
	-> ( r, r' : ZZ )
	-> Fin (S n) -> ZZ
vectGCDFnExtension _ _ r' FZ = r'
vectGCDFnExtension t r _ (FS prel) = t prel <.> r

vectGCDExtension' : ( t : Fin n -> ZZ )
	-> ( factorizationAtInd : ( j : Fin n )
		-> t j <.> ( vs <:> xs ) = index j xs )
	-> ( factorizationX : r' <.> s = x )
	-> ( factorizationWithin : r <.> s = vs <:> xs )
	-> ( i : Fin (S n) )
	-> vectGCDFnExtension t r r' i <.> s = index i (x :: xs)
vectGCDExtension' t factorizationAtInd factorizationX factorizationWithin FZ
	= factorizationX
vectGCDExtension' t factorizationAtInd factorizationX factorizationWithin (FS prel)
	= trans (sym $ ringOpIsAssociative _ _ _)
	$ trans (cong factorizationWithin)
	$ factorizationAtInd prel

vectGCDExtension : ( factorizationAtInd : ( j : Fin n )
		-> index j xs `quotientOverZZ` ( vs <:> xs ) )
	-> ( factorizationX : x `quotientOverZZ` s )
	-> ( factorizationWithin : (vs <:> xs) `quotientOverZZ` s )
	-> ( i : Fin (S n) )
	-> index i (x :: xs) `quotientOverZZ` s
vectGCDExtension factorizationAtInd (factnXDiv ** factnXPr) (factnWinDiv ** factnWinPr) i
	= let vectGCDOldFn = \j => getWitness $ factorizationAtInd j
	in let vectGCDOldPr = \j => getProof $ factorizationAtInd j
	in ( vectGCDFnExtension vectGCDOldFn factnWinDiv factnXDiv i
		** vectGCDExtension' vectGCDOldFn vectGCDOldPr factnXPr factnWinPr i )

bezoutDotRewrite : {a : ZZ}
	-> (a :: (b <#> vs)) <:> (x :: xs) = a<.>x <+> b<.>(vs <:> xs)
bezoutDotRewrite {a} {b} {x} {xs} {vs} = (
	(a :: (b <#> vs)) <:> (x :: xs)
	) ={ monoidrec1D }= (
	a<.>x <+> ( (b <#> vs)<:>xs )
	) ={ cong vectVectLScalingCompatibility }= (
	a<.>x <+> b<.>(vs <:> xs)
	) QED

{-
The extension of a GCD of 2 numbers to that of a Vect of numbers
-}

{- (gcdToVectGCD) parameters -}
parameters (
	gcdAlg : (c, d : ZZ)
		-> ( zpar : (ZZ, ZZ) ** uncurry (bezQTy c d) zpar )
	) {

gcdToVectGCD :
	(k : Nat)
	-> (x : Vect k ZZ)
	-> ( v : Vect k ZZ **
		( i : Fin k )
		-> (index i x) `quotientOverZZ` (v <:> x) )
gcdToVectGCD Z [] = ( [] ** \i => FinZElim i )
gcdToVectGCD (S predk) (x::xs) with (gcdToVectGCD predk xs)
	| (vs ** recQFn) = runIdentity $ do {
			( (a, b) ** (gcdivA, gcdivB) )
				<- Id $ gcdAlg x (vs <:> xs)
			let vectGCDExtensionFn = vectGCDExtension
				{s=a<.>x <+> b<.>(vs <:> xs)}
				{xs=xs}
				{vs=vs}
				{x=x}
				recQFn gcdivA gcdivB
			return $ ( a::(b<#>vs) **
				\i => let apAtI = vectGCDExtensionFn i
				in (getWitness apAtI
					** trans (cong bezoutDotRewrite) $ getProof apAtI)
				)
		}

} {- (gcdToVectGCD) parameters -}


text:
module MergeSort

data SplitList : List a -> Type where
     SplitNil : SplitList []
     SplitOne : SplitList [x]
     SplitPair : (lefts : List a) -> (rights : List a) -> SplitList (lefts ++ rights)

total
splitList : (l : List a) -> SplitList l
splitList inp = splitListHelp inp inp
  where
    splitListHelp : List a -> (l : List a) -> SplitList l
    splitListHelp _ [] = SplitNil
    splitListHelp _ [x] = SplitOne
    splitListHelp (_ :: _ :: counter) (i :: items) = case splitListHelp counter items of
                                                          SplitNil => SplitOne
                                                          SplitOne {x} => SplitPair [i] [x]
                                                          (SplitPair lefts rights) => SplitPair (i :: lefts) rights
    splitListHelp _ items = SplitPair [] items

mergeSort : Ord a => List a -> List a
mergeSort xs with (splitList xs)
  mergeSort [] | SplitNil = []
  mergeSort [x] | SplitOne = [x]
  mergeSort (lefts ++ rights) | (SplitPair lefts rights) = merge (mergeSort lefts) (mergeSort rights)


text:
module Idris.Codegen.ExtSTG.RepType

import Idris.Codegen.ExtSTG.SemiDecEq

public export
data PrimElemRep
  = Int8ElemRep
  | Int16ElemRep
  | Int32ElemRep
  | Int64ElemRep
  | Word8ElemRep
  | Word16ElemRep
  | Word32ElemRep
  | Word64ElemRep
  | FloatElemRep
  | DoubleElemRep

export
SemiDecEq PrimElemRep where
  semiDecEq Int8ElemRep   Int8ElemRep   = Just Refl
  semiDecEq Int16ElemRep  Int16ElemRep  = Just Refl
  semiDecEq Int32ElemRep  Int32ElemRep  = Just Refl
  semiDecEq Int64ElemRep  Int64ElemRep  = Just Refl
  semiDecEq Word8ElemRep  Word8ElemRep  = Just Refl
  semiDecEq Word16ElemRep Word16ElemRep = Just Refl
  semiDecEq Word32ElemRep Word32ElemRep = Just Refl
  semiDecEq Word64ElemRep Word64ElemRep = Just Refl
  semiDecEq FloatElemRep  FloatElemRep  = Just Refl
  semiDecEq DoubleElemRep DoubleElemRep = Just Refl
  semiDecEq _ _ = Nothing

Show PrimElemRep where
  show Int8ElemRep   = "Int8ElemRep"
  show Int16ElemRep  = "Int16ElemRep"
  show Int32ElemRep  = "Int32ElemRep"
  show Int64ElemRep  = "Int64ElemRep"
  show Word8ElemRep  = "Word8ElemRep"
  show Word16ElemRep = "Word16ElemRep"
  show Word32ElemRep = "Word32ElemRep"
  show Word64ElemRep = "Word64ElemRep"
  show FloatElemRep  = "FloatElemRep"
  show DoubleElemRep = "DoubleElemRep"

public export
data PrimRep
  = VoidRep
  | LiftedRep   -- Boxed, in thunk or WHNF
  | UnliftedRep -- Boxed, in WHNF
  | Int8Rep     -- Unboxed, Signed, 8 bits value
  | Int16Rep    -- Unboxed, Signed, 16 bits value
  | Int32Rep    -- Unboxed, Signed, 32 bits value
  | Int64Rep    -- Unboxed, Signed, 64 bits value (with 32 bits words only)
  | IntRep      -- Unboxed, Signed, word-sized value
  | Word8Rep    -- Unboxed, Unsigned, 8 bits value
  | Word16Rep   -- Unboxed, Unsigned, 16 bits value
  | Word32Rep   -- Unboxed, Unsigned, 32 bits value
  | Word64Rep   -- Unboxed, Unisgned, 64 bits value (with 32 bits words only)
  | WordRep     -- Unboxed, Unisgned, word-sized value
  | AddrRep     -- A pointer, but *not* a Haskell value. Use (Un)liftedRep
  | FloatRep
  | DoubleRep
  | VecRep Nat PrimElemRep -- A vector

export
SemiDecEq PrimRep where
  semiDecEq VoidRep     VoidRep     = Just Refl
  semiDecEq LiftedRep   LiftedRep   = Just Refl
  semiDecEq UnliftedRep UnliftedRep = Just Refl
  semiDecEq Int8Rep     Int8Rep     = Just Refl
  semiDecEq Int16Rep    Int16Rep    = Just Refl
  semiDecEq Int32Rep    Int32Rep    = Just Refl
  semiDecEq Int64Rep    Int64Rep    = Just Refl
  semiDecEq IntRep      IntRep      = Just Refl
  semiDecEq Word8Rep    Word8Rep    = Just Refl
  semiDecEq Word16Rep   Word16Rep   = Just Refl
  semiDecEq Word32Rep   Word32Rep   = Just Refl
  semiDecEq Word64Rep   Word64Rep   = Just Refl
  semiDecEq WordRep     WordRep     = Just Refl
  semiDecEq AddrRep     AddrRep     = Just Refl
  semiDecEq FloatRep    FloatRep    = Just Refl
  semiDecEq DoubleRep   DoubleRep   = Just Refl
  semiDecEq (VecRep n1 p1) (VecRep n2 p2) = do
    Refl <- semiDecEq p1 p2
    Refl <- semiDecEq n1 n2
    Just Refl
  semiDecEq _ _ = Nothing

export
Show PrimRep where
  showPrec d VoidRep      = "VoidRep"
  showPrec d LiftedRep    = "LiftedRep"
  showPrec d UnliftedRep  = "UnliftedRep"
  showPrec d Int8Rep      = "Int8Rep"
  showPrec d Int16Rep     = "Int16Rep"
  showPrec d Int32Rep     = "Int32Rep"
  showPrec d Int64Rep     = "Int64Rep"
  showPrec d IntRep       = "IntRep"
  showPrec d Word8Rep     = "Word8Rep"
  showPrec d Word16Rep    = "Word16Rep"
  showPrec d Word32Rep    = "Word32Rep"
  showPrec d Word64Rep    = "Word64Rep"
  showPrec d WordRep      = "WordRep"
  showPrec d AddrRep      = "AddrRep"
  showPrec d FloatRep     = "FloatRep"
  showPrec d DoubleRep    = "DoubleRep"
  showPrec d (VecRep n p) = showCon d "VecRep" $ showArg n ++ " " ++ showArg p

||| SingeValue LiftedRep = Simple Algebraic value
public export
data RepType
  = SingleValue    PrimRep
  | UnboxedTuple   (List PrimRep)
  | PolymorphicRep

export
Show RepType where
  showPrec d (SingleValue p)   = showCon d "SingleValue" $ showArg p
  showPrec d (UnboxedTuple ps) = showCon d "UnboxedTuple" $ showArg ps
  showPrec d PolymorphicRep    = "PolymorphicRep"

export
SemiDecEq RepType where
  semiDecEq (SingleValue p1) (SingleValue p2) = do
    Refl <- semiDecEq p1 p2
    Just Refl
  semiDecEq (UnboxedTuple p1) (UnboxedTuple p2) = do
    Refl <- semiDecEq p1 p2
    Just Refl
  semiDecEq PolymorphicRep PolymorphicRep = Just Refl
  semiDecEq _ _ = Nothing

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Main

record Timeout where
  constructor MkTimeout
  unTimeout : Ptr

js_apply : (s : String) -> (ty : Type) -> { auto prf : FTy FFI_JS [] ty } -> ty
js_apply s ty = foreign FFI_JS s ty

setTimeout : (() -> JS_IO ()) -> (ms : Int) -> JS_IO Timeout
setTimeout f ms = do
  timeout <- js_apply "setTimeout(%0, %1)"
                      (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)
                      (MkJsFn f)
                      ms
  pure $ MkTimeout timeout

log : String -> JS_IO ()
log = js_apply "console.log(%0)" (String -> JS_IO())

data Component : Type -> Type where
  MkComponent : String -> List Prop -> Component

data ReactElement : Type where
  MkReactElement : (tag : String) ->
                   (props : List ReactProp) ->
                   (children : List Reactelement) ->
                   ReactElement

interface Render a (MkFFI b) where
  render : a -> (MkFFI b)

createElement : String -> JS_IO Ptr
createElement el = js_apply "React.createElement(%0, {}, [\"Hello Wurld\"])"
                            (String -> JS_IO Ptr)
                            el

render : Ptr -> JS_IO ()
render = js_apply "ReactDOM.render(%0, document.getElementById(\"root\"))"
                  (Ptr -> JS_IO ())

main : JS_IO ()
main = do _  <- setTimeout (\x => log "timed") 1000
          el <- createElement "h1"
          render el

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Gspider.Types.AttackFrame

import Data.Vect

import Core
import Types.RestrictedCharString

%access private

||| Represents a probabilistic attack frame.
|||
||| @ n the number of pending guesses at this frame
||| @ m the number of made guesses at this frame
public export
data AttackFrame : (s : System) -> (n : Nat) -> (m : Nat) -> Type where
  -- Included for completeness.
  Empty : (d : Distribution s) ->
          AttackFrame s Z Z
  Initial : (p : Vect (S n) (RestrictedCharString s)) ->
            (d : Distribution s) ->
            AttackFrame s (S n) Z
  Ongoing : (p : Vect (S n) (RestrictedCharString s)) ->
            (g : Vect (S m) (RestrictedCharString s)) ->
            (d : Distribution s) ->
            (q : Double) ->
            AttackFrame s (S n) (S m)
  Terminal : (g : Vect (S m) (RestrictedCharString s)) ->
             (d : Distribution s) ->
             (q : Double) ->
             AttackFrame s Z (S m)

||| Gets the probability of a password in a distribution given that it is not present in a collection.
|||
||| @ p the password
||| @ d the distribution
||| @ g the collection
distinctProb : (p : (RestrictedCharString s)) ->
               (d : Distribution s) ->
               (g : Vect n (RestrictedCharString s)) ->
               Double
distinctProb p d g = if elem p g then 0 else d p

||| Advances an attack to the next frame.
|||
||| @ frame the frame to advance
export
advance : (frame : AttackFrame s (S n) m) -> AttackFrame s n (S m)
advance (Initial [p] d) = Terminal [p] d (d p)
advance (Initial (p :: rest@(p' :: ps)) d) = Ongoing rest [p] d (d p)
advance (Ongoing [p] g d q) = Terminal (p :: g) d (q + (distinctProb p d g))
advance (Ongoing (p :: rest@(p' :: ps)) g d q) = Ongoing rest (p :: g) d (q + (distinctProb p d g))

||| Retreats an attack to the previous frame.
|||
||| @ frame the frame to retreat
export
retreat : (frame : AttackFrame s n (S m)) -> AttackFrame s (S n) m
retreat (Ongoing p [g] d q) = Initial (g :: p) d
retreat (Ongoing p (g :: rest@(g' :: gs)) d q) = Ongoing (g :: p) rest d (q - (distinctProb g d rest))
retreat (Terminal [g] d q) = Initial [g] d
retreat (Terminal (g :: rest@(g' :: gs)) d q) = Ongoing [g] rest d (q - (distinctProb g d rest))

max_stars_repo_name: sr-lab/gspider

max_issues_repo_name: sr-lab/gspider

max_forks_repo_name: sr-lab/gspider


text:
module Lexer

import Lightyear
import Lightyear.Char
import Lightyear.Strings

public export
data Lexeme
  = Numeral Integer
  | Plus
  | Minus
  | Times
  | Divide
  | LParen
  | RParen

-- XXX: deriving Eq?
export
implementation Eq Lexeme where
  (Numeral n1) == (Numeral n2) = n1 == n2
  Plus == Plus = True
  Minus == Minus = True
  Times == Times = True
  Divide == Divide = True
  LParen == LParen = True
  RParen == RParen = True
  _ == _ = False

-- XXX: deriving Show?
export
implementation Show Lexeme where
  show (Numeral n) = "(Numeral " ++ show n ++ ")"
  show Plus = "Plus"
  show Minus = "Minus"
  show Times = "Times"
  show Divide = "Divide"
  show LParen = "LParen"
  show RParen = "RParen"

-- XXX: Data.Fin finToInteger?
getInteger : List (Fin 10) -> Integer
getInteger = foldl (\a => \b => 10 * a + cast b) 0

numeral : Parser Lexeme
numeral = do
  digits <- some digit
  pure $ Numeral (getInteger digits)

tok : Parser Lexeme
tok = numeral
  <|> ((char '+') *> pure Plus)
  <|> ((char '-') *> pure Minus)
  <|> ((char '*') *> pure Times)
  <|> ((char '/') *> pure Divide)
  <|> ((char '(') *> pure LParen)
  <|> ((char ')') *> pure RParen)

export
lexer : Parser (List Lexeme)
lexer = spaces *> (many (tok <* spaces))

max_stars_repo_name: steshaw/idris-calc

max_issues_repo_name: steshaw/idris-calc

max_forks_repo_name: steshaw/idris-calc


text:
module TestStore

import DataStore

testStore : DataStore (SString .+. SString .+. SInt)
testStore = addToStore ("Mercury", "Mariner 10", 1974) $
            addToStore ("Venus", "Venera", 1961) $
            addToStore ("Uranus", "Voyager 2", 1986) $
            addToStore ("Pluto", "New Horizons", 2015) $
            empty

listItems : DataStore schema -> List (SchemaType schema)
listItems x with (storeView x)
  listItems x | SNil = []
  listItems (addToStore value store) | (SAdd rec) = value :: listItems store | rec

filterKeys : (test : SchemaType val_schema -> Bool) -> DataStore (SString .+. val_schema) -> List String
filterKeys test x with (storeView x)
  filterKeys test x | SNil = []
  filterKeys test (addToStore (key, value) store) | (SAdd rec) =
    case test value of
        False => filterKeys test store | rec
        True => key :: filterKeys test store | rec

-- 10.3 Ex. # 1
getValues : DataStore (SString .+. val_schema) -> List (SchemaType val_schema)
getValues x with (storeView x)
  getValues x | SNil = []
  getValues (addToStore (key, value) store) | (SAdd rec) = value :: getValues store | rec

ttestStore : DataStore (SString .+. SInt)
ttestStore = addToStore ("First", 1) $
            addToStore ("Second", 2) $
            empty


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.TOML.Value

import public Data.SortedMap
import Data.List
import Data.Strings

public export
Key : Type
Key = String

mutual
    public export
    data Value
        = VString String
        | VInteger Integer
        | VFloat Double
        | VBoolean Bool
        | VArray (List Value)
        | VTable Table

    public export
    Table : Type
    Table = SortedMap Key Value

export
lookupNested : (key : List String) -> (table : Table) -> Maybe Value
lookupNested [] table = Nothing
lookupNested [x] table = lookup x table
lookupNested (x :: xs) table = do
    VTable t <- lookup x table
        | _ => Nothing
    lookupNested xs t

public export
Eq Value where
    (VString x) == (VString y) = x == y
    (VInteger x) == (VInteger y) = x == y
    (VFloat x) == (VFloat y) = x == y
    (VBoolean x) == (VBoolean y) = x == y
    (VArray xs) == (VArray ys) = xs == ys
    (VTable x) == (VTable y) = SortedMap.toList x == SortedMap.toList y
    _ == _ = False

public export
Show Value where
    show (VString x) = show x
    show (VInteger x) = show x
    show (VFloat x) = show x
    show (VBoolean True) = "true"
    show (VBoolean False) = "false"
    show (VArray xs) = "["
        ++ fastConcat (intersperse ", " $ map show xs)
        ++ "]"
    show (VTable x) =
        let kvs = the (List (Key, Value)) $ toList x in
        "{"
        ++ fastConcat (intersperse ", " $ flip map kvs \(k, v) =>
                            show k ++ " = " ++ show v
                        )
        ++ "}"

max_stars_repo_name: tiatomee/toml-idr

max_issues_repo_name: tiatomee/toml-idr

max_forks_repo_name: tiatomee/toml-idr


text:
||| Properties of factorial functions
module Data.Nat.Fact

import Data.Nat

%default total

||| Recursive definition of factorial.
factRec : Nat -> Nat
factRec Z = 1
factRec (S k) = (S k) * factRec k

||| Tail-recursive accumulator for factItr.
factAcc : Nat -> Nat -> Nat
factAcc Z acc = acc
factAcc (S k) acc = factAcc k $ (S k) * acc

||| Iterative definition of factorial.
factItr : Nat -> Nat
factItr n = factAcc n 1

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

||| Multiplicand-shuffling lemma.
multShuffle : (a, b, c : Nat) -> a * (b * c) = b * (a * c)
multShuffle a b c =
  rewrite multAssociative a b c in
    rewrite multCommutative a b in
      sym $ multAssociative b a c

||| Multiplication of the accumulator.
factAccMult : (a, b, c : Nat) ->
  a * factAcc b c = factAcc b (a * c)
factAccMult _ Z _ = Refl
factAccMult a (S k) c =
  rewrite factAccMult a k (S k * c) in
    rewrite multShuffle a (S k) c in
      Refl

||| Addition of accumulators.
factAccPlus : (a, b, c : Nat) ->
  factAcc a b + factAcc a c = factAcc a (b + c)
factAccPlus Z _ _ = Refl
factAccPlus (S k) b c =
  rewrite factAccPlus k (S k * b) (S k * c) in
    rewrite sym $ multDistributesOverPlusRight (S k) b c in
      Refl

||| The recursive and iterative definitions are the equivalent.
factRecItr : (n : Nat) -> factRec n = factItr n
factRecItr Z = Refl
factRecItr (S k) =
  rewrite factRecItr k in
    rewrite factAccMult k k 1 in
      rewrite multOneRightNeutral k in
        factAccPlus k 1 k


text:
module parser

import lexer
import tipos

%access public export

mutual

--------------------------------- Parser de Expressões Aritmeticas ---------------------------------
  num : List Token -> (Maybe AExp, List Token)
  num ((TokenInt n)::l) = (Just (N n), l)
  num ((TokenVarId id)::xs) = let (exp, r) = parseId ((TokenVarId id)::xs) in case exp of
    Nothing => (Nothing, r)
    Just k => (Just (IdA k), xs)
  num l = (Nothing, l)

  factor : List Token -> (Maybe AExp, List Token)
  factor = orParser num parenExp

  parenExp : List Token -> (Maybe AExp, List Token)
  parenExp ((TokenLParen)::xs) = let (e,r) = arithExp xs in parenExpAux e r where
    parenExpAux : Maybe AExp -> List Token -> (Maybe AExp, List Token)
    parenExpAux Nothing r = (Nothing, (TokenLParen::r))
    parenExpAux (Just e) (TokenRParen::xs) = ((Just e),xs)
    parenExpAux (Just e) l = (Nothing,(TokenLParen::xs))
  parenExp l = (Nothing, l)

  mul : List Token -> (Maybe AExp, List Token)
  mul l = let (exp, r) = factor l in mulAux exp r where
    mulAux : Maybe AExp -> List Token -> (Maybe AExp, List Token)
    mulAux Nothing r = (Nothing, r)
    mulAux (Just e) ((TokenTimes)::xs) = let (exp', r2) = factor xs in case exp' of
      Nothing => (Just e, (TokenTimes::xs))
      Just k => mulAux (Just (Mul e k)) r2
    mulAux (Just e) ((TokenDiv)::xs) = let (exp', r2) = factor xs in case exp' of
      Nothing => (Just e, (TokenDiv::xs))
      Just k => mulAux (Just (Div e k)) r2
    mulAux (Just e) l = ((Just e),l)

  sum : List Token -> (Maybe AExp, List Token)
  sum l = let (exp, r) = mul l in sumAux exp r where
    sumAux : Maybe AExp -> List Token -> (Maybe AExp, List Token)
    sumAux Nothing r = (Nothing, r)
    sumAux (Just e) ((TokenPlus)::xs) = let (exp', r2) = mul xs in case exp' of
      Nothing => (Just e, (TokenPlus::xs))
      Just k => sumAux (Just (Sum e k)) r2
    sumAux (Just e) ((TokenMinus)::xs) = let (exp', r2) = mul xs in case exp' of
      Nothing => (Just e, (TokenMinus::xs))
      Just k => sumAux (Just (Sub e k)) r2
    sumAux (Just e) l = ((Just e),l)

  arithExp : List Token -> (Maybe AExp, List Token)
  arithExp = sum

--------------------------------- Parser de Expressões Booleanas ---------------------------------
  bool : List Token -> (Maybe BExp, List Token)
  bool (TokenTrue::xs) = (Just (Boo True), xs)
  bool (TokenFalse::xs) = (Just (Boo False), xs)
  bool l = (Nothing, l)

  idBExp : List Token -> (Maybe BExp, List Token)
  idBExp ((TokenVarId id)::xs) = let (exp, r) = parseId ((TokenVarId id)::xs) in idAux exp r where
    idAux : Maybe Id -> List Token -> (Maybe BExp, List Token)
    idAux (Just e) (TokenPlus::xs) = (Nothing, (TokenPlus::xs))
    idAux (Just e) (TokenMinus::xs) = (Nothing, (TokenMinus::xs))
    idAux (Just e) (TokenTimes::xs) = (Nothing, (TokenTimes::xs))
    idAux (Just e) (TokenDiv::xs) = (Nothing, (TokenDiv::xs))
    idAux (Just e) l = (Just (IdB e), l)

  factorBExp : List Token -> (Maybe BExp, List Token)
  factorBExp ((TokenVarId id)::xs) = idBExp ((TokenVarId id)::xs)
  factorBExp (TokenNot::xs) = let (exp, r) = conditExp xs in case exp of
    Nothing => (Nothing, (TokenNot::xs))
    Just k => (Just (Not k), r)
  factorBExp l = orParser bool parenBExp l

  parenBExp : List Token -> (Maybe BExp, List Token)
  parenBExp ((TokenLParen)::xs) = let (e,r) = boolExp xs in parenBExpAux e r where
    parenBExpAux : Maybe BExp -> List Token -> (Maybe BExp, List Token)
    parenBExpAux Nothing r = (Nothing, (TokenLParen::r))
    parenBExpAux (Just e) (TokenRParen::xs) = ((Just e),xs)
    parenBExpAux (Just e) l = (Nothing,(TokenLParen::xs))
  parenBExp l = (Nothing, l)

  conditExp : List Token -> (Maybe BExp, List Token)
  conditExp = orParser aux factorBExp

  aux : List Token -> (Maybe BExp, List Token)
  aux l = let (e,r) = arithExp l in conditExpAux e r where
    conditExpAux : Maybe AExp -> List Token -> (Maybe BExp, List Token)
    conditExpAux Nothing r = (Nothing, r)
    conditExpAux (Just e) ((TokenEqual)::xs) = let (exp', r2) = arithExp xs in case exp' of
      Nothing => (Nothing, (TokenEqual::xs))
      Just k => ((Just (Equal e k)), r2)
    conditExpAux (Just e) ((TokenMaior)::xs) = let (exp', r2) = arithExp xs in case exp' of
      Nothing => (Nothing, (TokenMaior::xs))
      Just k => ((Just (GT e k)), r2)
    conditExpAux (Just e) ((TokenMenor)::xs) = let (exp', r2) = arithExp xs in case exp' of
      Nothing => (Nothing, (TokenMenor::xs))
      Just k => ((Just (LT e k)), r2)
    conditExpAux (Just e) ((TokenMaiorIgual)::xs) = let (exp', r2) = arithExp xs in case exp' of
      Nothing => (Nothing, (TokenMaiorIgual::xs))
      Just k => ((Just (GE e k)), r2)
    conditExpAux (Just e) ((TokenMenorIgual)::xs) = let (exp', r2) = arithExp xs in case exp' of
      Nothing => (Nothing, (TokenMenorIgual::xs))
      Just k => ((Just (LE e k)), r2)
    conditExpAux (Just e) l' = (Nothing,l)

  logic : List Token -> (Maybe BExp, List Token)
  logic l = let (exp, r) = conditExp l in logicAux exp r where
    logicAux : Maybe BExp -> List Token -> (Maybe BExp, List Token)
    logicAux Nothing r = (Nothing, r)
    logicAux (Just e) ((TokenOr)::xs) = let (exp', r2) = conditExp xs in case exp' of
      Nothing => (Just e, (TokenOr::xs))
      Just k => logicAux (Just (OR e k)) r2
    logicAux (Just e) ((TokenAnd)::xs) = let (exp', r2) = conditExp xs in case exp' of
      Nothing => (Just e, (TokenAnd::xs))
      Just k => logicAux (Just (And e k)) r2
    logicAux (Just e) l = ((Just e),l)

  boolExp : List Token -> (Maybe BExp, List Token)
  boolExp = logic

--------------------------------- Ajustes para Exp ---------------------------------
  parseBExp : List Token -> (Maybe Exp, List Token)
  parseBExp l = let (exp, r) = logic l in case exp of
    Nothing => (Nothing, l)
    Just k => ((Just (BExpR k)), r)

  parseAExp : List Token -> (Maybe Exp, List Token)
  parseAExp l = let (exp, r) = arithExp l in case exp of
    Nothing => (Nothing, l)
    Just k => ((Just (AExpR k)), r)

  parseExp : List Token -> (Maybe Exp, List Token)
  parseExp (TokenCommercialE::l') = let (exp', r2) = parseId l' in case exp' of
    Nothing => (Nothing, l')
    Just k => (Just (DeRef k), r2)
  parseExp (TokenTimes::l') = let (exp', r2) = parseId l' in case exp' of
    Nothing => (Nothing, l')
    Just k => (Just(ValRef k), r2)
  parseExp l = orParser parseBExp parseAExp l

--------------------------------- Parser de Comandos ---------------------------------
  parseId : List Token -> (Maybe Id, List Token)
  parseId ((TokenVarId id)::xs) = (Just (ValID id), xs)
  parseId l = (Nothing, l)

  assign : List Token -> (Maybe Cmd, List Token)
  assign l = let (exp, r) = parseId l in assignAux exp r where
    assignAux : Maybe Id -> List Token -> (Maybe Cmd, List Token)
    assignAux Nothing r = (Nothing, r)
    assignAux (Just e) (TokenAssign::xs) = let (exp', r2) = parseExp xs in case exp' of
      Nothing => (Nothing, l)
      Just k => ((Just (Assign e k)), r2)
    assignAux (Just e) r = (Nothing, l)

  loop : List Token -> (Maybe Cmd, List Token)
  loop (TokenWhile::xs) = let (exp, r) = boolExp xs in loopAux exp r where
    loopAux : Maybe BExp -> List Token -> (Maybe Cmd, List Token)
    loopAux Nothing l = (Nothing, (TokenWhile::xs))
    loopAux (Just e) (TokenDo::xs) = let (exp', r2) = seq xs in case exp' of
      Nothing => (Nothing, (TokenDo::xs))
      Just k => (Just (Loop e k), r2)
    loopAux (Just e) l = (Nothing, l)
  loop l = (Nothing, l)

  partials : List Token -> (Maybe Cmd, List Token)
  partials (TokenElse::xs) = seq xs
  partials l = (Nothing, l)

  comandCall : List Token -> (Maybe Cmd, List Token)
  comandCall = orParser call bloc

  auxComand : List Token -> (Maybe Cmd, List Token)
  auxComand = orParser loop comandCall

  comandUnityAux : List Token -> (Maybe Cmd, List Token)
  comandUnityAux = orParser assign auxComand

  comandUnity : List Token -> (Maybe Cmd, List Token)
  comandUnity = orParser cond comandUnityAux

  cond : List Token -> (Maybe Cmd, List Token)
  cond (TokenIf::xs) = let (exp, r) = boolExp xs in condAux exp r where
    condAux : Maybe BExp -> List Token -> (Maybe Cmd, List Token)
    condAux Nothing l = (Nothing, (TokenIf::xs))
    condAux (Just e) (TokenThen::xs) = let (c1, r2) = seq xs in case c1 of
      Nothing => (Nothing, (TokenThen::xs))
      Just k => let (c2, r3) = partials r2 in case c2 of
        Nothing => (Just (Cond e k NOP), r3)
        Just p => (Just (Cond e k p), r3)
    condAux (Just e) l = (Nothing, l)
  cond l = (Nothing, l)

  seq : List Token -> (Maybe Cmd, List Token)
  seq l = let (exp, r) = comandUnity l in seqAux exp r where
    seqAux : Maybe Cmd -> List Token -> (Maybe Cmd, List Token)
    seqAux Nothing l' = (Nothing, l')
    seqAux (Just e) (TokenEnd::xs) = ((Just e), xs)
    seqAux (Just e) l' = let (c2, r2) = seq l' in case c2 of
      Nothing => ((Just e), l')
      Just k => (Just (CSeq e k), r2)

  comands : List Token -> (Maybe Cmd, List Token)
  comands = seq

  declaration : List Token -> (Maybe Dec, List Token)
  declaration (TokenCons::xs) = const (TokenCons::xs)
  declaration (TokenVar::xs) = let (exp, r) = parseId xs in declarationAux exp r where
    declarationAux : Maybe Id -> List Token -> (Maybe Dec, List Token)
    declarationAux Nothing l' = (Nothing, l')
    declarationAux (Just e) (TokenAssign::l') = let (exp', r2) = parseExp l' in case exp' of
      Nothing => (Nothing, l')
      Just k => (Just (Bind e (Ref k)), r2)
    declarationAux (Just e) l' = (Nothing, l')
  declaration l = (Nothing, l)

  const :List Token -> (Maybe Dec, List Token)
  const (TokenCons::xs) = let (exp, r) = parseId xs in constAux exp r where
    constAux : Maybe Id -> List Token -> (Maybe Dec, List Token)
    constAux Nothing l' = (Nothing, l')
    constAux (Just e) (TokenAssign::l') = let (exp', r2) = parseExp l' in case exp' of
      Nothing => (Nothing, l')
      Just k => (Just (Bind e k), r2)
    constAux (Just e) l' = (Nothing, l')
  const l = (Nothing, l)

  dec : List Token -> (Maybe Dec, List Token)
  dec = orParser seqDec function

  bloc : List Token -> (Maybe Cmd, List Token)
  bloc (TokenLet::xs) = let (dec, r) = dec xs in blocAux dec r where
    blocAux : Maybe Dec -> List Token -> (Maybe Cmd, List Token)
    blocAux Nothing l' = (Nothing, l')
    blocAux (Just c) (TokenIn::xs) = let (c1, r2) = comands xs in case c1 of
      Nothing => (Nothing, r2)
      Just k => (Just (Blk c k), r2)
    blocAux (Just e) l' = (Nothing, l')
  bloc l = (Nothing, l)

  seqDec : List Token -> (Maybe Dec, List Token)
  seqDec l = let (exp, r) = declaration l in seqDecAux exp r where
    seqDecAux : Maybe Dec -> List Token -> (Maybe Dec, List Token)
    seqDecAux Nothing l' = (Nothing, l')
    seqDecAux (Just e) l' = let (c2, r2) = seqDec l' in case c2 of
      Nothing => ((Just e), l')
      Just k => (Just (DSeq e k), r2)

  ctrlParser : List Token -> (Maybe Ctrl, List Token)
  ctrlParser l = let (exp, r) = bloc l in case exp of
    Nothing => (Nothing, l)
    Just k => ((Just (CtCmd k)), r)

--------------------------------- Parser de Comandos ---------------------------------
  formals : List Token -> (Maybe Formals, List Token)
  formals (TokenLParen::xs) = let (list, r) = listaParam xs in formalsAux list r where
    formalsAux : List Id -> List Token -> (Maybe Formals, List Token)
    formalsAux list (TokenRParen::xs) = (Just (Form list), xs)
    formalsAux list r2 = (Nothing, r2)
  formals l = (Nothing, l)

  listaParam : List Token -> (List Id, List Token)
  listaParam l = let (id, r) = parseId l in listaParamAux id r [] where
    listaParamAux : Maybe Id -> List Token -> List Id -> (List Id, List Token)
    listaParamAux Nothing r2 list = (list, r2)
    listaParamAux (Just k) r2 list = let (id', r3) = parseId r2 in listaParamAux id' r3 (k::list)

  abst : List Token -> (Maybe Abst, List Token)
  abst l =  let (f, r) = formals l in abstAux f r where
    abstAux : Maybe Formals -> List Token -> (Maybe Abst, List Token)
    abstAux Nothing r2 = (Nothing, r2)
    abstAux (Just f) (TokenIgual::xs) = let (cm, r3) = comands xs in case cm of
      Nothing => (Nothing, r3)
      Just c => (Just (Abstr f c), r3)
    abstAux (Just f) r2 = (Nothing, r2)

  function : List Token -> (Maybe Dec, List Token)
  function (TokenRec::TokenFn::xs)=  let (id, r) = parseId xs in case id of
    Nothing => (Nothing, xs)
    Just i => let (f, r2) = abst r in case f of
      Nothing => (Nothing, r2)
      Just abs => (Just (Rbnd i abs), r2)
  function (TokenFn::xs)=  let (id, r) = parseId xs in case id of
    Nothing => (Nothing, xs)
    Just i => let (f, r2) = abst r in case f of
      Nothing => (Nothing, r2)
      Just abs => (Just (BindF i abs), r2)
  function l = (Nothing, l)

  actuals : List Token -> (Maybe Actuals, List Token)
  actuals (TokenLParen::xs) = let (list, r) = listaExps xs in actualsAux list r where
    actualsAux : List Exp -> List Token -> (Maybe Actuals, List Token)
    actualsAux list (TokenRParen::xs) = (Just (Act list), xs)
    actualsAux list r2 = (Nothing, r2)
  actuals l = (Nothing, l)

  listaExps : List Token -> (List Exp, List Token)
  listaExps l = let (exp, r) = parseExp l in listaExpsAux exp r [] where
    listaExpsAux : Maybe Exp -> List Token -> List Exp -> (List Exp, List Token)
    listaExpsAux Nothing r2 list = (list, r2)
    listaExpsAux (Just k) r2 list = let (exp', r3) = parseExp r2 in listaExpsAux exp' r3 (k::list)

  call : List Token -> (Maybe Cmd, List Token)
  call l = let (id, r) = parseId l in case id of
    Nothing => (Nothing, r)
    Just i => let (act, r2) = actuals r in case act of
      Nothing => (Nothing, r2)
      Just k => (Just (Call i k), r2)

-- funçao para tentar parser de AExp e BExp
-- tenta aplicar o parser1 a lista
  orParser : (List Token -> (Maybe a, List Token)) -> (List Token -> (Maybe a, List Token)) -> (List Token -> (Maybe a, List Token))
  orParser parser1 parser2 list = let (exp,r) = parser1 list in orParserAux exp r where
-- orParserAux verifica se o parser1 falhou (Nothing) ou retornou com sucesso um (exp, resto da lista)
    orParserAux : Maybe a -> List Token -> (Maybe a, List Token)
    orParserAux Nothing l = parser2 l
    orParserAux (Just exp') l = (Just exp', l)

max_stars_repo_name: RonaldCamp/ImpCompiler

max_issues_repo_name: RonaldCamp/ImpCompiler

max_forks_repo_name: RonaldCamp/ImpCompiler


text:
-- ----------------------------------------------------------- [ Lightyear.idr ]
-- Module  : Lightyear
--
-- License : This code is distributed under the BSD 2-clause license. See the
--           file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Lightyear

import public Lightyear.Core
import public Lightyear.Errmsg
import public Lightyear.Combinators

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

max_stars_repo_name: david-christiansen/lightyear

max_issues_repo_name: david-christiansen/lightyear

max_forks_repo_name: david-christiansen/lightyear


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

import GRL.Lang.GLang

import Sif.Types
import Sif.Pattern.Model

%access export
-- ----------------------------------------------------------- [ Type Synonyms ]

public export
FUNCTIONAL : (impl : SifTy -> SifDomain -> Type) -> SifDomain -> Type
FUNCTIONAL impl d = SifExpr TyREQ d impl

public export
USABILITY : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
USABILITY impl d = SifExpr TyREQ d impl

public export
RELIABILITY : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
RELIABILITY impl d = SifExpr TyREQ d impl

public export
PERFORMANCE : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
PERFORMANCE impl d = SifExpr TyREQ d impl

public export
SUPPORTABILITY : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
SUPPORTABILITY impl d = SifExpr TyREQ d impl

public export
REQUIREMENT : (impl : SifTy -> SifDomain -> Type) -> SifDomain -> Type
REQUIREMENT impl d = SifExpr TyREQ d impl

public export
REQUIREMENTS : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
REQUIREMENTS impl d = List (REQUIREMENT impl d)

public export
PROBLEM : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
PROBLEM impl d = SifExpr TyPROBLEM d impl

public export
ADVANTAGE : (impl : SifTy -> SifDomain -> Type) -> SifDomain -> Type
ADVANTAGE impl d = SifExpr TyTRAIT d impl

public export
DISADVANTAGE : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
DISADVANTAGE impl d = SifExpr TyTRAIT d impl

public export
TRAIT : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
TRAIT impl d = SifExpr TyTRAIT d impl

public export
TRAITS : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
TRAITS impl d = List (TRAIT impl d)

public export
AFFECT : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
AFFECT impl d = SifExpr TyAFFECTS d impl

public export
AFFECTS : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
AFFECTS impl d = List (AFFECT impl d)

public export
PROPERTY : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
PROPERTY impl d = SifExpr TyPROPERTY d impl

public export
PROPERTIES : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
PROPERTIES impl d = List (PROPERTY impl d)

public export
SOLUTION : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
SOLUTION impl d = SifExpr TySOLUTION d impl

public export
PATTERN : (SifTy -> SifDomain -> Type) -> SifDomain -> Type
PATTERN impl d = SifExpr TyPATTERN d impl

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

mkRequirement : SifBuilder i
             -> (d : SifDomain)
             -> RTy
             -> String
             -> Maybe String
             -> REQUIREMENT i d
mkRequirement impl d ty s desc = (buildReq impl) d ty s desc

mkFunctional : SifBuilder i
            -> (d : SifDomain)
            -> String
            -> Maybe String
            -> FUNCTIONAL i d
mkFunctional impl d s desc = (buildReq impl) d FUNC s desc

mkUsability : SifBuilder i
           -> (d : SifDomain)
           -> String
           -> Maybe String
           -> USABILITY i d
mkUsability impl d s desc = (buildReq impl) d USAB s desc

mkReliability : SifBuilder i
             -> (d : SifDomain)
             -> String
             -> Maybe String
             -> RELIABILITY i d
mkReliability impl d s desc = (buildReq impl) d RELI s desc

mkPerformance : SifBuilder i
             -> (d : SifDomain)
             -> String
             -> Maybe String
             -> PERFORMANCE i d
mkPerformance impl d s desc = (buildReq impl) d PERF s desc

mkSupportability : SifBuilder i
                -> (d : SifDomain)
                -> String
                -> Maybe String
                -> SUPPORTABILITY i d
mkSupportability impl d s desc = (buildReq impl) d SUPP s desc

mkProblem : SifBuilder i
         -> (d : SifDomain)
         -> String
         -> Maybe String
         -> REQUIREMENTS i d
         -> PROBLEM i d
mkProblem impl d t desc rs = (buildProblem impl) d t desc rs

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

mkAffect : SifBuilder i
        -> (d : SifDomain)
        -> CValue
        -> REQUIREMENT i d
        -> Maybe String
        -> AFFECT i d
mkAffect impl d c r desc = (buildAffect impl) d c r desc

mkTrait : SifBuilder i
       -> (d : SifDomain)
       -> TTy
       -> String
       -> Maybe String
       -> SValue
       -> AFFECTS i d
       -> TRAIT i d
mkTrait impl d ty t desc s rs = (buildTrait impl) d ty t desc s' rs
  where
    s' : SValue
    s' = case ty of {GEN => s; ADV => s; DIS => invertEval s}

mkAspect : SifBuilder i
        -> (d : SifDomain)
        -> String
        -> Maybe String
        -> SValue
        -> AFFECTS i d
        -> TRAIT i d
mkAspect impl d t desc s rs = (buildTrait impl) d GEN t desc s rs

mkAdvantage : SifBuilder i
           -> (d : SifDomain)
           -> String
           -> Maybe String
           -> SValue
           -> AFFECTS i d
           -> ADVANTAGE i d
mkAdvantage impl d t desc s rs = (buildTrait impl) d ADV t desc s rs

mkDisadvantage : SifBuilder i
              -> (d : SifDomain)
              -> String
              -> Maybe String
              -> SValue
              -> AFFECTS i d
              -> DISADVANTAGE i d
mkDisadvantage impl d t desc s rs = (buildTrait impl) d DIS t desc (invertEval s) rs

mkProperty : SifBuilder i
          -> (d : SifDomain)
          -> String
          -> Maybe String
          -> TRAITS i d
          -> PROPERTY i d
mkProperty impl d t desc ts = (buildProperty impl) d t desc ts

mkSolution : SifBuilder i
          -> (d : SifDomain)
          -> String
          -> Maybe String
          -> PROPERTIES i d
          -> SOLUTION i d
mkSolution impl d t desc ps = (buildSolution impl) d t desc ps

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

mkPattern : SifBuilder i
         -> (d : SifDomain)
         -> String
         -> Maybe String
         -> PROBLEM i d
         -> SOLUTION i d
         -> PATTERN i d
mkPattern impl d t desc p s = (buildPattern impl) d t desc p s

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
import Language.Reflection

%language ElabReflection

data NatExpr : Nat -> Type where
     Plus : NatExpr x -> NatExpr y -> NatExpr (plus x y)
     Mult : NatExpr x -> NatExpr y -> NatExpr (mult x y)
     Dbl : NatExpr x -> NatExpr (mult 2 x)
     Val : (val : Nat) -> NatExpr val

getNatExpr : TTImp -> Elab (n ** NatExpr n)
getNatExpr `(Prelude.Types.plus ~(x) ~(y))
   = do (_ ** xval) <- getNatExpr x
        (_ ** yval) <- getNatExpr y
        pure (_ ** Plus xval yval)
getNatExpr `(Prelude.Types.mult (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)) ~(y))
   = do (y ** yval) <- getNatExpr y
        pure (_ ** Dbl yval)
getNatExpr `(Prelude.Types.mult ~(x) ~(y))
   = do (_ ** xval) <- getNatExpr x
        (_ ** yval) <- getNatExpr y
        pure (_ ** Mult xval yval)
getNatExpr x = pure (_ ** Val !(check x))

%macro
mkNatExpr : (n : Nat) -> Elab (NatExpr n)
mkNatExpr n
    = do Just `(Main.NatExpr ~(expr)) <- goal
              | _ => fail "Goal is not a NatExpr"
         (n' ** expr') <- getNatExpr expr
         check !(quote expr')

test1 : (x : Nat) -> (y : Nat) -> NatExpr (plus x (plus y x))
test1 x y = mkNatExpr _ -- yes, auto implicits can do this too :)

test2 : (x : Nat) -> (y : Nat) -> NatExpr (plus x (mult y x))
test2 x y = mkNatExpr _

test3 : (x : Nat) -> (y : Nat) -> NatExpr (plus x (mult 2 x))
test3 x y = mkNatExpr _ -- auto implicit search gets something different


text:
module Idris.Codegen.ExtSTG.Core

import Compiler.ANF
import Core.Context
import Core.Core
import Core.TT
import Data.IOArray
import Libraries.Data.IntMap
import Data.List
import Libraries.Data.StringMap
import Data.Strings
import Data.Vect
import Idris.Codegen.ExtSTG.STG
import Prelude

export
logLine : String -> Core ()
logLine msg = coreLift $ putStrLn msg

namespace Counter

  ||| Counter annotation for creating Unique identifiers.
  export
  data Counter : Type where

  export
  mkCounter : Core (Ref Counter Int)
  mkCounter = newRef Counter 0

namespace Uniques

  ||| Uniques annotation for storing unique identifiers associated with names.
  export
  data Uniques : Type where

  export
  UniqueMap : Type
  UniqueMap =
    ( StringMap Unique -- Namespace for types
    , StringMap Unique -- Namespace for terms
    )

  export
  UniqueMapRef : Type
  UniqueMapRef = Ref Uniques UniqueMap

  export
  mkUniques : Core UniqueMapRef
  mkUniques = newRef Uniques (empty, empty)

  export
  mkUnique : {auto _ : Ref Counter Int} -> Char -> Core Unique
  mkUnique c = do
    x <- get Counter
    let u = MkUnique c x
    put Counter (x + 1)
    pure u

  export
  uniqueForType
    :  {auto _ : UniqueMapRef}
    -> {auto _ : Ref Counter Int}
    -> String
    -> Core Unique
  uniqueForType name = do
    (ty,te) <- get Uniques
    case lookup name ty of
      Nothing => do
        u <- mkUnique 'y'
        put Uniques (insert name u ty, te)
        pure u
      Just u => do
        pure u

  export
  uniqueForTerm
    :  {auto _ : UniqueMapRef}
    -> {auto _ : Ref Counter Int}
    -> String
    -> Core Unique
  uniqueForTerm name = do
    (ty,te) <- get Uniques
    case lookup name te of
      Nothing => do
        u <- mkUnique 'e'
        put Uniques (ty,insert name u te)
        pure u
      Just u => do
        pure u

  public export
  HardcodedUnique : Type
  HardcodedUnique = (String, List String, String, Unique, RepType)

  public export
  hardcodedRepType : HardcodedUnique -> RepType
  hardcodedRepType (_,_,_,_,r) = r

  ||| void# in STG
  export
  hardcodedVoidHash : HardcodedUnique
  hardcodedVoidHash = ("ghc-prim", ["GHC", "Prim"], "void#", MkUnique '0' 21, SingleValue VoidRep)

-- TODO: Remove export
public export
stgRepType : RepType
stgRepType = SingleValue LiftedRep

export
mkSrcSpan : FC -> SrcSpan
mkSrcSpan (MkFC file (sl,sc) (el,ec))
  = SsRealSrcSpan (MkRealSrcSpan file (sl + 1) (sc + 1) (el + 1) (ec + 1)) Nothing
mkSrcSpan (MkVirtualFC file (sl,sc) (el,ec))
  = SsRealSrcSpan (MkRealSrcSpan file (sl + 1) (sc + 1) (el + 1) (ec + 1)) Nothing
mkSrcSpan EmptyFC
  = SsUnhelpfulSpan "<no location>"

public export
data BinderKind
  = TermBinder
  | TypeBinder

export
mkSBinderHardcoded
  : UniqueMapRef => Ref Counter Int => (h : HardcodedUnique) -> FC -> Core (SBinder (hardcodedRepType h))
mkSBinderHardcoded (_,_,binderName,unique,repType) fc = do
  let binderId = MkBinderId unique
  let typeSig = "mkSBinder: hardcodedSig"
  let details = VanillaId
  let info = "mkSBinder: IdInfo"
  let defLoc = mkSrcSpan fc
  pure $ MkSBinder
    binderName
    repType
    binderId
    typeSig
    HaskellExported
    details
    info
    defLoc

-- TODO: Remove export
-- TODO: Remove/replace topLevel parameter
export
mkSBinder
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> BinderKind -> Scope -> FC -> String
  -> Core (SBinder Core.stgRepType)
mkSBinder binderKind scope fc binderName = do
  binderId <- MkBinderId <$> case binderKind of
                               TermBinder => uniqueForTerm binderName
                               TypeBinder => uniqueForType binderName
  let typeSig = "mkSBinder: typeSig"
  let details = VanillaId
  let info    = "mkSBinder: IdInfo"
  let defLoc  = mkSrcSpan fc
  pure $ MkSBinder
    binderName
    stgRepType
    binderId
    typeSig
    scope
    details
    info
    defLoc

-- TODO: Remove export
-- TODO: Remove/replace topLevel parameter
export
mkSBinderRep
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> BinderKind -> Scope -> (rep : RepType) -> FC -> String
  -> Core (SBinder rep)
mkSBinderRep binderKind scope rep fc binderName = do
  binderId <- MkBinderId <$> case binderKind of
                               TermBinder => uniqueForTerm binderName
                               TypeBinder => uniqueForType binderName
  let typeSig = "mkSBinder: typeSig"
  let details = VanillaId
  let info    = "mkSBinder: IdInfo"
  let defLoc  = mkSrcSpan fc
  pure $ MkSBinder
    binderName
    rep
    binderId
    typeSig
    scope
    details
    info
    defLoc

-- export
mkSBinderTyCon
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> FC -> String -- TODO : Constant
  -> Core (SBinder Core.stgRepType)
mkSBinderTyCon = mkSBinder TypeBinder GlobalScope

||| Create a top-level binder for a given name. Mainly, used in STG.String module
export
mkSBinderTopLevel
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> String
  -> Core (SBinder Core.stgRepType)
mkSBinderTopLevel = mkSBinder TermBinder GlobalScope emptyFC

||| Create a local binder for a given name. Used in STG.String module
export
mkSBinderLocalStr
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> String
  -> Core (SBinder Core.stgRepType)
mkSBinderLocalStr n = mkSBinder TermBinder LocalScope emptyFC n

||| Create a local binder for a given name. Used in STG.String module
export
mkSBinderRepLocalStr
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> (rep : RepType)
  -> String
  -> Core (SBinder rep)
mkSBinderRepLocalStr r n = mkSBinderRep TermBinder LocalScope r emptyFC n

export
mkSBinderLocal
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> FC -> Core.Name.Name -> Int
  -> Core (SBinder Core.stgRepType)
mkSBinderLocal f n x = mkSBinder TermBinder LocalScope f (show n ++ ":" ++ show x)

export
mkSBinderRepLocal
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> (rep : RepType) -> FC -> Core.Name.Name -> Int
  -> Core (SBinder rep)
mkSBinderRepLocal r f n x = mkSBinderRep TermBinder LocalScope r f (show n ++ ":" ++ show x)

export
mkSBinderName
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> FC -> Core.Name.Name
  -> Core (SBinder Core.stgRepType)
mkSBinderName f n = mkSBinder TermBinder GlobalScope f (show n)

export
mkSBinderStr
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> FC -> String
  -> Core (SBinder Core.stgRepType)
mkSBinderStr = mkSBinder TermBinder GlobalScope

||| Create a binder for a function that is defined in another STG module.
||| Primary use case for this is the STG-FFI, or exported from the module.
export
mkSBinderExtId
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> FC -> String
  -> Core (SBinder Core.stgRepType)
mkSBinderExtId = mkSBinder TermBinder HaskellExported

||| Always return a new binder for the given name adding the counter at the end of the name.
||| Used in defining local variables.
export
mkFreshSBinderStr
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> Scope -> FC -> String
  -> Core (SBinder Core.stgRepType)
mkFreshSBinderStr scope fc binderName = do
  unique@(MkUnique _ c) <- mkUnique 'l'
  binderId <- MkBinderId <$> mkUnique 'l'
  let typeSig = "mkSBinder: typeSig"
  let details = VanillaId
  let info    = "mkSBinder: IdInfo"
  let defLoc  = mkSrcSpan fc
  pure $ MkSBinder
    (binderName ++ ":" ++ show c)
    stgRepType
    binderId
    typeSig
    scope
    details
    info
    defLoc

||| Always return a new binder for the given name adding the counter at the end of the name.
||| Used in defining local variables.
export
mkFreshSBinderRepStr
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> Scope -> (rep : RepType) -> FC -> String
  -> Core (SBinder rep)
mkFreshSBinderRepStr scope rep fc binderName = do
  unique@(MkUnique _ c) <- mkUnique 'l'
  binderId <- MkBinderId <$> mkUnique 'l'
  let typeSig = "mkSBinder: typeSig"
  let details = VanillaId
  let info    = "mkSBinder: IdInfo"
  let defLoc  = mkSrcSpan fc
  pure $ MkSBinder
    (binderName ++ ":" ++ show c)
    rep
    binderId
    typeSig
    scope
    details
    info
    defLoc

export
mkSBinderVar
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> FC -> Core.Name.Name -> AVar
  -> Core (SBinder Core.stgRepType)
mkSBinderVar fc n (ALocal x) = mkSBinder TermBinder LocalScope fc (show n ++ ":" ++ show x)
mkSBinderVar fc n ANull      = coreFail $ InternalError $ "mkSBinderVar " ++ show fc ++ " " ++ show n ++ " ANull"

export
mkBinderIdVar
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> FC -> Core.Name.Name -> (r : RepType) -> AVar
  -> Core (BinderId r)
mkBinderIdVar fc n r (ALocal x) = MkBinderId <$> uniqueForTerm (show n ++ ":" ++ show x)
mkBinderIdVar fc n r ANull      = coreFail $ InternalError $ "mkBinderIdVar " ++ show fc ++ " " ++ show n ++ " ANull"

||| Create a StdVarArg for the Argument of a function application.
|||
||| If the argument is ANull/erased, then it returns a NulAddr literal
export
mkStgArg
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> FC -> Core.Name.Name -> AVar
  -> Core ArgSg
mkStgArg fc n a@(ALocal _) = mkArgSg . StgVarArg <$> (mkBinderIdVar fc n stgRepType a)
mkStgArg _  _ ANull        = pure $ mkArgSg $ StgLitArg $ LitNullAddr
-- Question: Is that a right value for erased argument?
-- Answer: This is not right, this should be Lifted. Make a global erased value, with its binder
--         that is referred here.

||| Lookup a binder based on the name encoded as String
export
mkBinderIdStr
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> String
  -> Core (BinderId Core.stgRepType)
mkBinderIdStr = map MkBinderId . uniqueForTerm -- TODO: Is this right?

export
mkBinderIdName
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> Core.Name.Name
  -> Core (BinderId Core.stgRepType)
mkBinderIdName = map MkBinderId . uniqueForTerm . show -- TODO: Is this right?

export
dataConNameForConstant
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> Constant
  -> Core String
dataConNameForConstant IntType     = pure "I#"
dataConNameForConstant IntegerType = pure "GMPInt" -- TODO: This should be GMP int
dataConNameForConstant Bits8Type   = pure "W8#"
dataConNameForConstant Bits16Type  = pure "W16#"
dataConNameForConstant Bits32Type  = pure "W32#"
dataConNameForConstant Bits64Type  = pure "W64#"
-- dataConNameForConstant StringType  = pure "IdrString" -- TODO: Figure this out.
dataConNameForConstant CharType    = pure "C#"
dataConNameForConstant DoubleType  = pure "D#"
dataConNameForConstant WorldType   = pure "IdrWorld"
dataConNameForConstant other = coreFail $ UserError $ "No data constructor for " ++ show other

export
typeConNameForConstant
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> Constant
  -> Core String
typeConNameForConstant IntType     = pure "Int"
typeConNameForConstant IntegerType = pure "IInt" -- TODO: This should be GMP int
typeConNameForConstant Bits8Type   = pure "Word8"
typeConNameForConstant Bits16Type  = pure "Word16"
typeConNameForConstant Bits32Type  = pure "Word32"
typeConNameForConstant Bits64Type  = pure "Word64"
-- typeConNameForConstant StringType  = pure "IdrString" -- TODO: Figure this out.
typeConNameForConstant CharType    = pure "Char"
typeConNameForConstant DoubleType  = pure "Double"
typeConNameForConstant WorldType   = pure "IdrWorld"
typeConNameForConstant other = coreFail $ UserError $ "No data constructor for " ++ show other

||| Create a TyConId for the given idris primtive type.
export
tyConIdForConstant
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> Constant
  -> Core TyConId
tyConIdForConstant c = pure $ MkTyConId !(uniqueForType !(typeConNameForConstant c))

||| The unit where the Idris STG backend puts every definitions,
||| primitives and used defined codes
export
MAIN_UNIT : String
MAIN_UNIT = "main"

||| The module name where Idris STG backend puts every definitions,
||| primitives and user defined codes
export
MAIN_MODULE : String
MAIN_MODULE = "Main"

namespace DataTypes

  ||| DataType annotation for auto Refs to store the defined STG datatypes during compilation.
  export
  data DataTypes : Type where

  ||| Defined datatypes in STG during the compilation of the module.
  DataTypeMap : Type
  DataTypeMap = StringMap {-UnitId-} (StringMap {-ModuleName-} (List STyCon))

  DataConIdMap : Type
  DataConIdMap = StringMap {-Unique-} (List SDataConSg) -- Should be unique

  TyConIdMap : Type
  TyConIdMap = StringMap {-Unique-} (List STyCon) -- Should be unique

  export
  DataTypeMapRef : Type
  DataTypeMapRef = Ref DataTypes (DataTypeMap, DataConIdMap, TyConIdMap)

  ||| Create the Reference that holds the DataTypeMap
  export
  mkDataTypes : Core DataTypeMapRef
  mkDataTypes = newRef DataTypes (empty, empty, empty)

  addDataType
    : UnitId -> ModuleName -> STyCon
    -> (DataTypeMap, DataConIdMap, TyConIdMap) -> (DataTypeMap, DataConIdMap, TyConIdMap)
  addDataType (MkUnitId u) (MkModuleName m) s (dm,dc,tc) =
    ( merge (singleton u (singleton m [s])) dm
    , foldl merge dc $ map (\d => singleton (show (dataConUnique (ident (snd d)))) [d]) s.DataCons
    , merge (singleton (show (tyConUnique s.Id)) [s]) tc
    )

  export
  checkDefinedDataCon : DataTypeMapRef => Unique -> Core (Maybe SDataConSg)
  checkDefinedDataCon u = do
    (_,dc,_) <- get DataTypes
    case lookup (show u) dc of
      Nothing  => pure Nothing
      Just [d] => pure $ Just d
      Just ds  => coreFail $ InternalError $ "Non unique datatype for DataCon: " ++ show u

  export
  checkDefinedSTyCon : DataTypeMapRef => TyConId -> Core (Maybe STyCon)
  checkDefinedSTyCon (MkTyConId u) = do
    (_,_,tc) <- get DataTypes
    case lookup (show u) tc of
      Nothing  => pure Nothing
      Just [t] => pure $ Just t
      Just ts  => coreFail $ InternalError $ "Non unqiue typecon for TyCon:" ++ show (u,ts)

  dataTypeList : DataTypeMap -> List (UnitId, List (ModuleName, List STyCon))
  dataTypeList = map (mapFst MkUnitId) . Data.StringMap.toList . map (map (mapFst MkModuleName) . Data.StringMap.toList)

  export
  createSTyCon
    :  {auto _ : UniqueMapRef}
    -> {auto _ : Ref Counter Int}
    -> (STG.Name, SrcSpan) -> List (STG.Name, DataConRep, SrcSpan)
    -> Core STyCon
  createSTyCon (tName,tSpan) dCons = do
    ds <- traverse (\(dName, drep, span) => pure $ mkSDataConSg $
                      MkSDataCon
                        dName
                        drep
                        (MkDataConId !(uniqueForTerm dName))
                        !(mkSBinderTopLevel dName)
                        span
                   )
                   dCons
    pure $ MkSTyCon tName (MkTyConId !(uniqueForType tName)) ds tSpan

  ||| Register an STG datatype under the compilation unit and module name.
  export
  defineDataType : {auto _ : DataTypeMapRef} -> UnitId -> ModuleName -> STyCon -> Core ()
  defineDataType u m s = do
    x <- get DataTypes
    put DataTypes (addDataType u m s x)

  ||| Return all the STG data type definition that were registered during the compilation
  export
  getDefinedDataTypes : {auto _ : DataTypeMapRef} -> Core (List (UnitId, List (ModuleName, List STyCon)))
  getDefinedDataTypes = map (dataTypeList . fst) $ get DataTypes

||| Creates a DataConId for the given data constructor name, checks if the name is already have
||| a definition, if not throw an InternalError
export
mkDataConIdStr
  : UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => String
  -> Core DataConIdSg
mkDataConIdStr n = do
  Just (r ** d) <- checkDefinedDataCon !(uniqueForTerm n)
    | Nothing => coreFail $ InternalError $ "DataCon is not defined: " ++ n
  pure $ (r ** ident d)

||| Creates a DataConId for the given data constructor name, checks if the name is already have
||| a definition, if not throw an InternalError
export
mkDataConId
  : UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => Core.Name.Name -- Name of the fully qualified data constructor (not an Idris primitive type)
  -> Core DataConIdSg
mkDataConId n = mkDataConIdStr (show n)

export
mkTyConIdStr
  : UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => String
  -> Core TyConId
mkTyConIdStr n = do
  tyConId <- MkTyConId <$> uniqueForType n
  Just _ <- checkDefinedSTyCon tyConId
    | Nothing => coreFail $ InternalError $ "TyCon is not defined: " ++ n
  pure tyConId

||| Determine the Data constructor for the boxed primitive type.
|||
||| The name of terms should coincide the ones that are defined in GHC's ecosystem. This
||| would make the transition easier, I hope.
export
dataConIdForConstant
  :  UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => Constant
  -> Core DataConIdSg
dataConIdForConstant c = mkDataConIdStr !(dataConNameForConstant c)

||| Determine the Data constructor for the boxed primitive type.
|||
||| The name of terms should coincide the ones that are defined in GHC's ecosystem. This
||| would make the transition easier, I hope.
export
dataConIdRepForConstant
  : UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => (r : PrimRep)
  -> Constant
  -> Core (DataConId (AlgDataCon [r]))
dataConIdRepForConstant r c = do
  ((AlgDataCon [q]) ** d) <- dataConIdForConstant c
    | other => coreFail $ InternalError
                        $ unwords
                          [ "dataConIdRepForConstant:"
                          , show c, "got an unexpectly shaped binder:"
                          , show other, "expected:" -- , show (AlgDataCon [r])
                          ]
  let Just Refl = semiDecEq r q
    | Nothing => coreFail $ InternalError
                          $ unwords
                            [ "dataConIdRepForConstant:"
                            , show c, "doesn't have the expected"
                            , show r, "found"
                            , show q
                            ]
  pure d

||| Always creates a fresh binder, its main purpose to create a binder which won't be used, mainly StgCase
export
nonused : UniqueMapRef => Ref Counter Int => Core (SBinder (SingleValue LiftedRep))
nonused = mkFreshSBinderStr LocalScope emptyFC "nonused"

export
nonusedRep : UniqueMapRef => Ref Counter Int => (rep : RepType) -> Core (SBinder rep)
nonusedRep rep = mkFreshSBinderRepStr LocalScope rep emptyFC "nonused"

export
topLevel : {r : RepType} -> SBinder (SingleValue LiftedRep) -> List SBinderSg -> Expr r -> TopBinding
topLevel n as body
  = StgTopLifted
  $ StgNonRec n
  $ StgRhsClosure ReEntrant as body

||| Create a case expression with one Alt which matches the one data constructor
export
unBox
  :  (v1     : SBinder (SingleValue LiftedRep))
  -> {q      : DataConRep}
  -> (d1     : DataConId q)
  -> (t1     : TyConId)
  -> (cb     : SBinder (SingleValue LiftedRep))
  -> (v2     : (AltBinderType (AltDataCon (q ** d1))))
  -> (e      : Expr Core.stgRepType) -- TODO: Fix
  -> Expr Core.stgRepType -- TODO: Fix
unBox v1 d1 t1 cb v2 e =
  StgCase (AlgAlt t1) (StgApp (binderId v1) [] (SingleValue LiftedRep)) cb
  [ MkAlt (AltDataCon (q ** d1)) v2 e ]

export
checkSemiDecEq : Show a => SemiDecEq a => String -> (x : a) -> (y : a) -> Core (x = y)
checkSemiDecEq ctx x y = case (semiDecEq x y) of
  Nothing   => coreFail $ InternalError $ ctx ++ " different values: " ++ show (x, y)
  Just Refl => pure Refl

export
checkDataCon : String -> (r : DataConRep) -> DataConIdSg -> Core (DataConId r)
checkDataCon loc r c@(q ** d) = do
  Refl <- checkSemiDecEq loc r q
  pure d


text:
import Data.Maybe
import Data.List

data NoParam
  = NPCons1
  | NPCons2 Nat

noParam : NoParam
noParam = ?test1

-- SCENARIO
-- WHEN: Code action on ?test1
-- THEN: Code action result contains:
--       - 'Fill Hole ~ NPCons1'
--       - 'Fill Hole ~ (NDCons2 ?test1_0)'

data WithParam a
  = WPCons1
  | WPCons2 a Nat a

withParam : WithParam Nat
withParam = ?test2

-- SCENARIO
-- WHEN: Code action on ?test2
-- THEN: Code action result contains:
--       - 'Fill Hole ~ WPCons1'
--       - 'Fill Hole ~ (WPCons2 ?test2_2 ?test2_1 ?test2_0)'

similarNames : Bool
similarNames = ?isJ (Just 0)

-- SCENARIO
-- WHEN: Code action on ?isJ
-- THEN: Code action result contains:
--       - 'Fill Hole ~ isJust'
-- NOTE: This is failing now, as we need to improve the polymorphic type unification

record Record a where
  constructor MkRecord
  field1 : a
  field2 : String

someRecord : Record Int
someRecord = ?test3

-- SCENARIO
-- WHEN: Code action on ?test3
-- THEN: Code action result contains:
--       - 'Fill Hole ~ (MkRecord ?field1_1 ?field2_0)'

applied : NoParam
applied = ?test4 (the Nat 0)

-- SCENARIO
-- WHEN: Code action on ?test4
-- THEN: Code action result contains:
--       - 'Fill Hole ~ NPCons2'

not : Bool -> Bool
not True = False
not False = True

-- SCENARIO
-- WHEN: Code action on ?no
-- THEN: Code action result contains:
--       - 'Fill Hole ~ not'

someBool : Bool
someBool = ?no False

namespace Private

  export
  data PrivateData
    = PrivateConstructor

  export
  privateData : PrivateData
  privateData = PrivateConstructor

-- SCENARIO
-- WHEN: Code action on ?pd2
-- THEN: Code action result contains:
--       - 'Fill Hole ~ PrivateDataConstructor'

  export
  privateData2 : PrivateData
  privateData2 = ?pd2

-- SCENARIO
-- WHEN: Code action on ?pd1
-- THEN: Code action result contains:
--       - 'Fill Hole ~ privateData'
--  AND: Code action does not contain:
--       - 'Fill Hole ~ PrivateDataConstructor'

somePrivate : PrivateData
somePrivate = ?pd1

data SomeNamedADT : Type -> Type where
  NamedField1 : (name1 : String) -> (name2 : a) -> SomeNamedADT a
  NamedField2 : (name3 : Int) -> SomeNamedADT Int
  NamedField3 : (name3 : Int) -> String -> SomeNamedADT a

-- SCENARIO
-- WHEN: Code action on ?sna
-- THEN: Code action result contains:
--       - 'Fill Hole ~ (NameField1 ?name1_1 ?name2_0)'
--       - 'Fill Hole ~ (NameField2 ?name3_0)'
--       - 'Fill Hole ~ (NameField1 ?name3_1 ?sna_0)'

someNamedADT : SomeNamedADT Int
someNamedADT = ?sna


text:
module Main

import Effect.State
import Effect.Exception
import Effect.Random
import Effect.StdIO

data Expr = Var String
          | Val Integer
          | Add Expr Expr
          | Random Integer

Env : Type
Env = List (String, Integer)

getRnd : Integer -> { [RND] } Eff IO Integer
getRnd upper = do val <- rndInt 0 upper
--                   putStrLn (show val)
                  return val

eval : Expr -> { [RND, EXCEPTION String, STDIO, STATE Env] } Eff IO Integer
eval (Var x)
   = do vs <- get
        case lookup x vs of
             Nothing => raise ("No such variable " ++ x)
             Just val => return val
eval (Val x) = return x
eval (Add l r) = do l' <- eval l
                    r' <- eval r
                    return (l' + r')
eval (Random upper) = do val <- getRnd upper
                         return val

testExpr : Expr
testExpr = Add (Add (Var "foo") (Val 42)) (Random 100)

runEval : List (String, Integer) -> Expr -> IO Integer
runEval args expr = run (eval' expr)
  where eval' : Expr ->
                { [RND, EXCEPTION String, STDIO, STATE Env] } Eff IO Integer
        eval' e = do put args
                     srand 1234567890
                     eval e
main : IO ()
main = do putStr "Number: "
          x <- getLine
          val <- runEval [("foo", cast x)] testExpr
          putStrLn $ "Answer: " ++ show val

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
-- vim: ft=idris sw= ts=2 et

import Data.Vect

-- vector arithmetics
add : Vect n a -> Vect m a -> Vect (n + m) a
add Nil ys = ys
add (x :: xs) ys = x :: add xs ys

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
||| Helper functions for LSP server responses and notifications.
|||
||| (C) The Idris Community, 2021
module Server.Response

import Core.Context
import Core.Core
import Core.Env
import Core.FC
import Data.OneOf
import Data.String
import Idris.Pretty
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.JSON
import Language.LSP.Message
import Parser.Support
import Server.Configuration
import Server.Diagnostics
import Server.Log
import Server.Utils
import System.File

||| Header for messages on-the-wire.
||| By specification only Content-Length is mandatory.
header : Int -> String
header l = "Content-Length: " ++ show l ++ "\r\n\r\n"

||| Response message for method not found or not implemented yet.
export
methodNotFound : ResponseError
methodNotFound = MkResponseError MethodNotFound "Method not implemented yet" JNull

||| Response message for error while parsing a new message received.
export
parseError : ResponseError
parseError = MkResponseError ParseError "Parse error" JNull

||| Response message for internal server errors.
export
internalError : String -> ResponseError
internalError msg = MkResponseError InternalError msg JNull

||| Response message for invalid requests.
export
invalidRequest : String -> ResponseError
invalidRequest msg = MkResponseError InvalidRequest msg JNull

||| Response message for invalid parameters to an otherwise valid method.
export
invalidParams : String -> ResponseError
invalidParams msg = MkResponseError InvalidParams msg JNull

||| Response message for messages received before initialization.
export
serverNotInitialized : ResponseError
serverNotInitialized = MkResponseError ServerNotInitialized "" JNull

writeResponse : Ref LSPConf LSPConfiguration
             => JSON
             -> Core ()
writeResponse msg = do
  let body = stringify msg
  let header = header (cast $ length body)
  outputHandle <- gets LSPConf outputHandle
  coreLift_ $ fPutStr outputHandle (header ++ body)
  coreLift_ $ fflush outputHandle

||| Sends a new notification from the server to the client.
export
sendNotificationMessage : Ref LSPConf LSPConfiguration
                       => (method : Method Server Notification)
                       -> (params : MessageParams method)
                       -> Core ()
sendNotificationMessage method params = do
  let msg = MkNotificationMessage method params
  writeResponse $ toJSON msg
  logString Info ("Sent notification message for method " ++ stringify (toJSON method))
  logString Debug (stringify (toJSON msg))

||| Sends a request from the server to the client ignoring the result
||| TODO when client sends response we fail to parse it
export
sendRequestMessage_ : Ref LSPConf LSPConfiguration
                       => (method : Method Server Request)
                        -> (params : MessageParams method)
                       -> Core ()
sendRequestMessage_ method params = do
  requestId <- gets LSPConf nextRequestId
  let msg = MkRequestMessage (make $ cast {to=Int} requestId) method params
  modify LSPConf (record {nextRequestId = requestId + 1})
  writeResponse (toJSON msg)
  logString Info ("Sent request message for method " ++ stringify (toJSON method))
  logString Debug (stringify (toJSON msg))

||| Sends a response message to a request received from the client.
export
sendResponseMessage : Ref LSPConf LSPConfiguration
                   => (method : Method Client Request)
                   -> ResponseMessage method
                   -> Core ()
sendResponseMessage method msg = do
  writeResponse (toJSON msg)
  logString Info ("Sent response message for method " ++ stringify (toJSON method))
  logString Debug (stringify (toJSON msg))

||| Sends an error response to an unknown method.
export
sendUnknownResponseMessage : Ref LSPConf LSPConfiguration => ResponseError -> Core ()
sendUnknownResponseMessage err = do
  -- The method type Initialize is irrelevant since the message is unknown, can use any method, the message would be the same.
  writeResponse (toJSON {a = ResponseMessage Initialize} (Failure (make MkNull) err))
  logString Info "Sent response to unknown method"

||| Sends a LSP `Diagnostic` message for a given, potentially versioned, source
||| that produces some errors.
|||
||| @caps The client capabilities related to diagnostics
||| @uri The source URI.
||| @version Optional source version.
||| @errs Errors produced while trying to check the source.
export
sendDiagnostics : Ref LSPConf LSPConfiguration
               => Ref Syn SyntaxInfo
               => Ref Ctxt Defs
               => Ref ROpts REPLOpts
               => (caps : Maybe PublishDiagnosticsClientCapabilities)
               -> (uri : DocumentURI)
               -> (version : Maybe Int)
               -> (errs : List Error)
               -> Core ()
sendDiagnostics caps uri version errs = do
  diagnostics <- traverse (toDiagnostic caps uri) errs
  let params = MkPublishDiagnosticsParams uri version diagnostics
  sendNotificationMessage TextDocumentPublishDiagnostics params


text:
main : IO Int
main = pure $ sum $ [1 .. 100]


text:
{-
0.42
1.68
1.34
0.34
42
0
-}
module Main

testNum : IO ()
testNum =
  traverse_
    (\op => printLn $ 0.84 `op` 0.5)
    [(*), (/), (+), (-)]

testStr : IO ()
testStr =
  for_ ["42.0", "not a double"] $ \s =>
    printLn $ the Double (cast s)

main : IO ()
main = do
  testNum
  testStr

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
{-
Copyright 2020, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module Utils

%access public export
%default total

%include C "print.h"
%include C "FreeRTOS/idris_FreeRTOS.h"

||| FFI wrapper for 'int16_t printInit(uint16_t uart_nr)'
printInit : Int -> IO Int
printInit uart_nr =
    foreign FFI_C "printInit" (Int -> IO Int) uart_nr

||| FFI wrapper for 'void vDirectPrintMsg(const portCHAR* msg)'
vDirectPrintMsg : String -> IO ()
vDirectPrintMsg msg =
    foreign FFI_C "vDirectPrintMsg" (String -> IO ()) msg

max_stars_repo_name: mokshasoft/FreeRTOS-community-ports

max_issues_repo_name: mokshasoft/FreeRTOS-community-ports

max_forks_repo_name: mokshasoft/FreeRTOS-community-ports


text:
module Language.LSP.Definition

import Core.Context
import Core.Core
import Core.Directory
import Core.Env
import Core.Metadata
import Core.Options
import Data.List
import Data.String
import Data.String.Parser
import Data.URI
import Language.LSP.Message
import Libraries.Data.PosMap
import Server.Configuration
import Server.Log
import Server.Utils
import System.File
import System.Path

mkLocation : Ref Ctxt Defs
          => Ref LSPConf LSPConfiguration
          => OriginDesc -> (Int, Int) -> (Int, Int) -> Core (Maybe Location)
mkLocation origin (sline, scol) (eline, ecol) = do
  defs <- get Ctxt
  let PhysicalIdrSrc modIdent = origin
    | _ => do
       logString Debug "gotoDefinition: Origin doesn't have an Idris file attached to it \{show origin}"
       pure Nothing
  let wdir = defs.options.dirs.working_dir
  let pkg_dirs = filter (/= ".") defs.options.dirs.extra_dirs
  let exts = map show listOfExtensions
  Just fname_abs <- catch
      (Just . (wdir </>) <$> nsToSource replFC modIdent) -- Try local source first
      -- if not found, try looking for the file amongst the loaded packages.
      (const $ firstAvailable $ do
        pkg_dir <- pkg_dirs
        -- Assume that if the package dir is relative, then it must be relative to
        -- the working directory of the running Idris2 instance.
        let pkg_dir_abs = ifThenElse (isRelative pkg_dir) (wdir </> pkg_dir) pkg_dir
        ext <- exts
        pure (pkg_dir_abs </> ModuleIdent.toPath modIdent <.> ext))
    | _ => do
      logString Debug "gotoDefinition: Can't find file for module \{show modIdent}"
      pure Nothing

  let fname_abs_uri = "file://" ++ fname_abs

  let Right (uri, _) = parse uriReferenceParser fname_abs_uri
      | Left err => do
          logString Debug "gotoDefinition: URI parse error: \{err} \{show (fname_abs_uri, sline, scol)}"
          pure Nothing

  pure $ Just $ MkLocation uri (MkRange (MkPosition sline scol) (MkPosition eline ecol))

export
gotoDefinition : Ref Ctxt Defs
              => Ref MD Metadata
              => Ref LSPConf LSPConfiguration
              => DefinitionParams -> Core (Maybe Location)
gotoDefinition params = do
  -- Check actual doc
  Just (actualUri, _) <- gets LSPConf openFile
    | Nothing => do
        logString Debug "gotoDefinition: openFile returned Nothing."
        pure Nothing
  let True = actualUri == params.textDocument.uri
      | False => do
          logString Debug "gotoDefinition: different URI than expected \{show (actualUri, params.textDocument.uri)}"
          pure Nothing

  let line = params.position.line
  let col  = params.position.character

  nameLocs <- gets MD nameLocMap
  let Just (_, name) = findPointInTreeLoc (line, col) nameLocs
    | Nothing => do
        logString Debug "gotoDefinition: Couldn't find a name at \{show (line, col)}"
        pure Nothing

  Nothing <- findTypeAt $ anyWithName name $ within (line, col)
    | Just _ => do
        logString Debug "gotoDefinition: \{show name} was a local name."
        pure Nothing

  Just globalDef <- lookupCtxtExact name !(gets Ctxt gamma)
    | Nothing => do
        logString Debug "gotoDefinition: \{show name} didn't have a GlobalDef."
        pure Nothing

  case globalDef.location of
    MkFC f s e => mkLocation f s e
    MkVirtualFC f s e => mkLocation f s e
    _ => do
      logString Debug "gotoDefinition: \{show name} didn't have location information."
      pure Nothing


text:
module Aoc
-- This module defines functions that might be useful every day.

import Data.Nat
import Data.List
import Data.List1
import Data.Stream
import Data.Strings
import Data.Vect

%default total

||| Apply a parser to each line of STDIN until it fails.
||| (`getLine` eventually returns an empty string, which
||| the parser should return Nothing for.)
|||
||| We use assert_total, because Idris doesn't know that our input files are finite.
public export
parseLines : HasIO io => (String -> Maybe a) -> io (List a)
parseLines parser =
  case parser !getLine of
    Just n => (n::) <$> assert_total (parseLines parser)
    Nothing => pure []

||| Read a list of non-empty strings from STDIN.
public export
readLines : HasIO io => io (List String)
readLines = parseLines (\s => if s == "" then Nothing else Just s)

||| Read a list of paragraphs from STDIN.
public export
readParagraphs : HasIO io => io (List1 (List String))
readParagraphs = split (== "") <$> go
  where go : io (List String); go = assert_total $ do
    l <- getLine
    case l of
      "" => do
        m <- getLine
        case m of
          "" => pure []
          _ => (l::) . (m::) <$> go
      _ => (l::) <$> go

||| Read a list of integers from STDIN, each on its own line.
public export
readIntegerLines : (Num a, Neg a, HasIO io) => io (List a)
readIntegerLines = parseLines parseInteger

||| Parse a comma-separated list of integers.
public export
parseCommaSeparatedIntegers : (Num a, Neg a) => String -> Maybe (List a)
parseCommaSeparatedIntegers = traverse parseInteger . toList . split (==',')

||| Count how many times a predicate is true.
public export
count : Foldable t => (a -> Bool) -> t a -> Nat
count f = foldr (\x, acc => if f x then S acc else acc) 0

||| Try to index into a list.
public export
maybeIndex : Nat -> List a -> Maybe a
maybeIndex n xs =
  case inBounds n xs of
    Yes _ => Just (index n xs)
    _ => Nothing

||| Turn a list of lists into an (n x m) matrix, if possible.
public export
toMatrix : (n : Nat) -> (m : Nat) -> List (List a) -> Maybe (Vect n (Vect m a))
toMatrix n m rows =
    sequence (map (toVect m) rows) >>= toVect n

||| Modularly index a non-empty vector.
public export
mindex : {n : Nat} -> (i : Nat) -> Vect (S n) a -> a
mindex i (x::xs) =
  let i' = modNatNZ i (S n) SIsNotZ  -- really just an optimization
  in index i' (cycle (x::toList xs))

public export
isLowerHexDigit : Char -> Bool
isLowerHexDigit c = isDigit c || c >= 'a' && c <= 'f'

public export
takeVect : (n : Nat) -> List a -> Maybe (Vect n a, List a)
takeVect Z xs = Just ([], xs)
takeVect (S n) [] = Nothing
takeVect (S n) (x::xs) = do { (v, l) <- takeVect n xs; pure (x::v, l) }

||| Get all ways to choose n distinct elements from a list.
public export
combinations : (n : Nat) -> List a -> List (Vect n a)
combinations Z _ = [[]]
combinations (S k) [] = []
combinations (S k) (x::xs) =
  [x::c | c <- combinations k xs] ++ combinations (S k) xs

public export
scanl : (f : a -> b -> a) -> a -> List b -> List a
scanl f a [] = [a]
scanl f a (b::bs) = a :: scanl f (f a b) bs

public export
scanl1 : (f : a -> a -> a) -> List a -> List a
scanl1 f [] = []
scanl1 f (x::xs) = scanl f x xs

public export
zipSL : Stream a -> List b -> List (a, b)
zipSL _ [] = []
zipSL (x::xs) (y::ys) = (x,y) :: zipSL xs ys

public export
enumerate : List a -> List (Integer, a)
enumerate xs = zipSL [0..] xs

public export
minBy : Ord b => (a -> b) -> a -> a -> a
minBy f x y = if f x < f y then x else y

public export
minimumBy : Ord b => (a -> b) -> List1 a -> a
minimumBy f xs = foldr1 (minBy f) xs

||| Apply a function n times.
public export
times : Nat -> (a -> a) -> a -> a
times Z f x = x
times (S k) f x = times k f (f x)


text:
module Linear

public export
data Usage = Once | Many

public export
data Use : Usage -> (Type -> Type) -> Type -> Type where
     Pure : (1 x : a) -> Use t m a
     BindOnce : (1 act : Use Once m a) -> (1 k : (1 x : a) -> Use t m b) -> Use t m b
     BindMany : (1 act : Use Many m a) -> (1 k : (x : a) -> Use t m b) -> Use t m b

public export
contType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
contType m Once q a b = ((1 x : a) -> Use q m b)
contType m Many q a b = ((x : a) -> Use q m b)

public export
(>>=) : {p : _} -> (1 f : Use p m a) -> (1 k : contType m p q a b) -> Use q m b
(>>=) {p = Once} = BindOnce
(>>=) {p = Many} = BindMany

public export
pure : (1 x : a) -> Use t m a
pure = Pure

public export
One : (Type -> Type) -> Type -> Type
One = Use Once

public export
Any : (Type -> Type) -> Type -> Type
Any = Use Many


text:
module Shape

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

export
triangle : Double -> Double -> Shape
triangle = Triangle

export
rectangle : Double -> Double -> Shape
rectangle = Rectangle

export
circle : Double -> Shape
circle = Circle

public export
data ShapeView : Shape -> Type where
    STriangle : (base : Double) -> (height : Double) -> ShapeView (triangle base height)
    SRectangle : (width : Double) -> (height : Double) -> ShapeView (rectangle width height)
    SCircle : (radius : Double) -> ShapeView (circle radius)

export
shapeView : (shape : Shape) -> ShapeView shape
shapeView (Triangle x y) = STriangle x y
shapeView (Rectangle x y) = SRectangle x y
shapeView (Circle x) = SCircle x


text:
import Fuel

%default total

data RunIO : Type -> Type where
  Quit : a -> RunIO a
  Do : IO a -> (a -> Inf (RunIO b)) -> RunIO b

(>>=) : IO a -> (a -> Inf (RunIO b)) -> RunIO b
(>>=) = Do

greet : RunIO ()
greet = do
  putStr "Name: "
  name <- getLine
  if name == ""
    then do putStrLn "Bye!"
            Quit ()
    else do
      putStrLn ("Hello " ++ name)
      greet

run : Fuel -> RunIO a -> IO (Maybe a)
run _ (Quit value) = pure (Just value)
run (More fuel) (Do k f) = do
  res <- k
  run fuel (f res)
run Dry _ = pure Nothing

partial
main : IO ()
main = do run forever greet
          pure ()

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development