text:
module Main

import GTK
import GTK.Utils

-- reference: https://zetcode.com/gui/gtk2/

tooltip_test : IO ()
tooltip_test = do
  primIO $ gtk_init nullptr nullptr
  -- make window
  window <- primIO $ gtk_window_new GTK_WINDOW_TOPLEVEL
  primIO $ gtk_window_set_title window "Tooltip Test"
  primIO $ gtk_container_set_border_width window 15
  primIO $ gtk_window_set_default_size window 300 200
  _ <- primIO $ g_signal_connect_data (to_object window) "destroy" gtk_main_quit nullanyptr 0 (\_, _ => prim__io_pure ())
  -- make button
  button <- primIO $ gtk_button_new_with_mnemonic "B_utton"
  primIO $ gtk_widget_set_halign button GTK_ALIGN_START
  primIO $ gtk_widget_set_valign button GTK_ALIGN_START
  primIO $ gtk_widget_set_tooltip_text button "why"
  primIO $ gtk_container_add window button
  -- main
  primIO $ gtk_widget_show_all window
  primIO $ gtk_main

simple_menu : IO ()
simple_menu = do
  primIO $ gtk_init nullptr nullptr
  -- make window
  window <- primIO $ gtk_window_new GTK_WINDOW_TOPLEVEL
  primIO $ gtk_window_set_title window "Simple Menu"
  primIO $ gtk_window_set_position window GTK_WIN_POS_CENTER -- must be before set_default_size or else the size will shrink
  primIO $ gtk_window_set_default_size window 300 200
  _ <- primIO $ g_signal_connect_data (to_object window) "destroy" gtk_main_quit nullanyptr 0 (\_, _ => prim__io_pure ())
  -- make vbox
  vbox <- primIO $ gtk_vbox_new false 0
  primIO $ gtk_container_add window vbox
  -- create objects
  menu_bar <- primIO $ gtk_menu_bar_new
  file_menu <- primIO $ gtk_menu_new
  file_menu_item <- primIO $ gtk_menu_item_new_with_label "File"
  quit_menu_item <- primIO $ gtk_menu_item_new_with_label "Quit"
  -- construct menu
  primIO $ gtk_menu_item_set_submenu file_menu_item file_menu
  primIO $ gtk_menu_shell_append file_menu quit_menu_item
  primIO $ gtk_menu_shell_append menu_bar file_menu_item
  primIO $ gtk_box_pack_start vbox menu_bar false false 0
  _ <- primIO $ g_signal_connect_data (to_object window) "destroy" gtk_main_quit nullanyptr 0 (\_, _ => prim__io_pure ())
  _ <- primIO $ g_signal_connect_data (to_object quit_menu_item) "activate" gtk_main_quit nullanyptr 0 (\_, _ => prim__io_pure ())
  -- main
  primIO $ gtk_widget_show_all window
  primIO $ gtk_main

submenu : IO ()
submenu = do
  primIO $ gtk_init nullptr nullptr
  -- make window
  window <- primIO $ gtk_window_new GTK_WINDOW_TOPLEVEL
  primIO $ gtk_window_set_title window "Submenu"
  primIO $ gtk_window_set_position window GTK_WIN_POS_CENTER -- must be before set_default_size or else the size will shrink
  primIO $ gtk_window_set_default_size window 300 200
  _ <- primIO $ g_signal_connect_data (to_object window) "destroy" gtk_main_quit nullanyptr 0 (\_, _ => prim__io_pure ())
  -- make vbox
  vbox <- primIO $ gtk_vbox_new false 0
  -- create objects
  menu_bar <- primIO $ gtk_menu_bar_new
  file_menu <- primIO $ gtk_menu_new
  file_menu_item <- primIO $ gtk_menu_item_new_with_label "File"
  quit_menu_item <- primIO $ gtk_menu_item_new_with_label "Quit"
  import_menu <- primIO $ gtk_menu_new
  import_menu_item <- primIO $ gtk_menu_item_new_with_label "Import"
  import_feed_menu_item <- primIO $ gtk_menu_item_new_with_label "Import News Feed..."
  import_book_menu_item <- primIO $ gtk_menu_item_new_with_label "Import Bookmarks..."
  import_mail_menu_item <- primIO $ gtk_menu_item_new_with_label "Import Mail..."
  sep <- primIO $ gtk_separator_menu_item_new
  -- construct menu
  primIO $ gtk_menu_item_set_submenu import_menu_item import_menu
  primIO $ gtk_menu_shell_append import_menu import_feed_menu_item
  primIO $ gtk_menu_shell_append import_menu import_book_menu_item
  primIO $ gtk_menu_shell_append import_menu import_mail_menu_item
  primIO $ gtk_menu_item_set_submenu file_menu_item file_menu
  primIO $ gtk_menu_shell_append file_menu import_menu_item
  primIO $ gtk_menu_shell_append file_menu sep
  primIO $ gtk_menu_shell_append file_menu quit_menu_item
  primIO $ gtk_menu_shell_append menu_bar file_menu_item
  primIO $ gtk_box_pack_start vbox menu_bar false false 0
  primIO $ gtk_container_add window vbox
  _ <- primIO $ g_signal_connect_data (to_object window) "destroy" gtk_main_quit nullanyptr 0 (\_, _ => prim__io_pure ())
  _ <- primIO $ g_signal_connect_data (to_object quit_menu_item) "activate" gtk_main_quit nullanyptr 0 (\_, _ => prim__io_pure ())
  -- main
  primIO $ gtk_widget_show_all window
  primIO $ gtk_main


text:
module CT

import Control.Monad.Trans

%default total

-- United container's transformer
-- In fact, it is a `newtype` for `m . c`
-- In fact, all these instances are called `*.Compose` in the standard lib.

public export
record CT (c : Type -> Type) m a where
  constructor MkCT
  runCT : m (c a)

export
Functor c => Functor m => Functor (CT c m) where
  map f (MkCT ml) = MkCT $ map f <$> ml

export
Applicative c => Applicative m => Applicative (CT c m) where
  pure = MkCT . pure . pure
  MkCT ml1 <*> MkCT ml2 = MkCT [| ml1 <*> ml2 |]

export
Applicative c => Alternative m => Alternative (CT c m) where
  empty = MkCT empty
  MkCT ml1 <|> MkCT ml2 = MkCT $ ml1 <|> ml2

export
Monad c => Traversable c => Monad m => Monad (CT c m) where
  MkCT ml >>= mf = MkCT $ ml >>= \xs => join <$> traverse (runCT . mf) xs

export
Foldable c => Foldable m => Foldable (CT c m) where
  foldr f i (MkCT ml) = foldr (flip $ foldr f) i ml

export
Traversable c => Traversable m => Traversable (CT c m) where
  traverse f (MkCT ml) = MkCT <$> traverse (traverse f) ml

export
Applicative c => MonadTrans (CT c) where
  lift = MkCT . map pure

ext: idr

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Main
import Cairo

-- Example data from https://www.cairo-lang.org/docs/hello_starknet/signature_verification.html
publicKey : Felt
publicKey = 1628448741648245036800002906075225705100596136133912895015035902954123957052

messageHash : TaintedMessage
messageHash = tainted $ pedersenHash 4321 0

signature : (Felt, Felt)
signature = (1225578735933442828068102633747590437426782890965066746429241472187377583468, 3568809569741913715045370357918125425757114920266578211811626257903121825123)

%noinline
main : Cairo ()
main =
  output (verifySignature messageHash publicKey (fst signature) (snd signature))

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Test.Optics

import UnitTest
import Data.Optics
import Control.Category

PLZ : Type
PLZ = Integer

mutual
  record Person where
    constructor MkPerson
    name : String
    address : Address
    second : Maybe Address

  record Address where
    constructor MkAddress
    street: String
    plz : PLZ
    city : String

  instance Eq Person where
    (==) (MkPerson name address second) (MkPerson x y z) = (name == x) && (address == y) && (second == z)

  instance Eq Address where
    (==) (MkAddress street plz city) (MkAddress x y z) = (street == x) && (plz == y) && (city == z)

  instance Show Person where
    show p = "Person(" ++ name p ++ ")"

  instance Show Address where
    show a = "Address(" ++ street a ++ ")"

hamburg: Address
hamburg = MkAddress "Elbchaussee" 2000 "Hamburg"

p: Person
p = MkPerson "Holmes" hamburg (Just hamburg)

_name : Lens Person String
_name = MkLens (\p => name p) (\p,n => record { name = n} p)

_address : Lens Person Address
_address = MkLens (\p => address p) (\p, a => record { address = a} p)

_secondary_address : Optional Person Address
_secondary_address = MkOptional (\p => second p) (\p, a => record { second = Just a} p )

_street : Lens Address String
_street = MkLens (\a => street a) (\a, s => record { street = s} a)

_person_street : Lens Person String
_person_street =  _address >>> _street

_secondary_street : Optional Person String
_secondary_street = _secondary_address +:? lensAsOptional _street

testPersonNameGet : IO ()
testPersonNameGet = assertEq "the _name lens can get the name of a person" (get _name p) ("Holmes")

testPersonNameSet : IO ()
testPersonNameSet = assertEq "the _name lens can set the name of a person" (set _name p "Watson") ( record { name = "Watson"} p)

testPersonAddressStreetGet : IO ()
testPersonAddressStreetGet = assertEq "the composed _person_street lens can get the name of the street" (get _person_street p) ("Elbchaussee")

testModifyF : IO ()
testModifyF = assertEq "modifyF can modify a value using a functor"(modifyF (\n => Just n) _name p) (Just p)

runall : IO()
runall = do testPersonNameGet
            testPersonNameSet
            testPersonAddressStreetGet
            testModifyF

max_stars_repo_name: justjoheinz/idris-optics

max_issues_repo_name: justjoheinz/idris-optics

max_forks_repo_name: justjoheinz/idris-optics


text:
import Extra.Prelude
import Extra.Language.Derive
import Language.Reflection
import Decidable.Equality

%language ElabReflection

data BalancedTree : Nat -> Type -> Type where
  Leaf : BalancedTree 0 a
  Branch : {n : Nat}
    -> (1 l : BalancedTree n a)
    -> (1 x : a)
    -> (1 r : BalancedTree n a)
    -> BalancedTree (S n) a

-- This works fine
mutual
  eqBalancedTree : Eq a
    => BalancedTree n a
    -> BalancedTree n a
    -> Bool
  %runElab deriveEq `{{ eqBalancedTree }} `{{ BalancedTree }}

  Eq a => Eq (BalancedTree n a) where
    (==) = eqBalancedTree

-- This fails since the clause `decEq Leaf (Branch _ _ _)` fails to typecheck
mutual
  decEqBalancedTree : DecEq a
    => (x : BalancedTree n a)
    -> (y : BalancedTree n a)
    -> Dec (x = y)
  %runElab deriveDecEq `{{ decEqBalancedTree }} `{{ BalancedTree }}

  DecEq a => DecEq (BalancedTree n a) where
    decEq = decEqBalancedTree

main : IO ()
main = putStrLn "Hi!"


text:
{- Tests for typed native Dart lists -}
module Main

import Dart.Core
import Dart.FFI
import Data.String

%inline
Box : Type -> Type
Box a = GenericType """
Box,
// A Dart generic type.
class Box<T> {
  final T value;
  Box(this.value);
  // A Dart generic member function.
  Box<U> map<U>(U Function(T) f) => Box<U>(f(value));
}
""" [a]

namespace Box

  %inline
  export
  new : HasIO io => {a : Type} -> a -> io (Box a)
  new value = primIO $ prim__dart_new (Box a) "" [value] none

  %inline
  export
  get : {a : Type} -> Box a -> a
  get box = prim__dart_get_pure ".value" box

  %inline
  export
  map : {a : Type} -> {b : Type} -> (a -> b) -> Box a -> Box b
  map f this = prim__dart_invoke_pure ".map" [b] [this, f] none

main : IO ()
main = do
  box <- Box.new "foo"
  Core.print box
  Core.print (box @. map String.toUpper @. get)


text:
data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)
%name Tree left, val, right

Eq elem => Eq (Tree elem) where
    (==) Empty Empty = ?Eq_rhs1_2
    (==) (Node left e right) (Node left' e' right') = left == left' && e == e' && right == right'
    (==) _ _ = False

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

listToTree : Ord a => List a -> Tree a
listToTree [] = Empty
listToTree (x :: xs) = let tree = listToTree xs in insert x tree

treeToList : Tree a -> List a
treeToList Empty = []
treeToList (Node left val right) = treeToList left ++ [val] ++ treeToList right


text:
module Data.Buffer.Ext

import public Data.Buffer

%foreign "scheme:blodwen-new-buffer"
         "RefC:newBuffer"
         "node:lambda:s=>Buffer.alloc(s)"
prim__newBuffer : Int -> PrimIO Buffer

export
newBuffer : HasIO io => Nat -> io Buffer
newBuffer size = primIO (Ext.prim__newBuffer $ cast size)

%foreign "scheme:string->utf8"
         "node:lambda: s=>Buffer.from(s, 'utf8')"
ffi_BufferFromStringUTF8 : String -> Buffer

export
implementation FromString Buffer where
  fromString = ffi_BufferFromStringUTF8

%foreign "scheme:utf8->string"
         "node:lambda: b=>b.toString('utf8')"
ffi_BufferToStringUTF8 : Buffer -> String

export
implementation Show Buffer where
  show = ffi_BufferToStringUTF8

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Main

data Ty = TyInt | TyBool | TyFun Ty Ty

interpTy : Ty -> Type
interpTy TyInt       = Int
interpTy TyBool      = Bool
interpTy (TyFun s t) = interpTy s -> interpTy t

using (G : Vect n Ty)

  data Env : Vect n Ty -> Type where
      Nil  : Env Nil
      (::) : interpTy a -> Env G -> Env (a :: G)

  data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
      stop : HasType fZ (t :: G) t
      pop  : HasType k G t -> HasType (fS k) (u :: G) t

  lookup : HasType i G t -> Env G -> interpTy t
  lookup stop    (x :: xs) = x
  lookup (pop k) (x :: xs) = lookup k xs

  data Expr : Vect n Ty -> Ty -> Type where
      Var : HasType i G t -> Expr G t
      Val : (x : Int) -> Expr G TyInt
      Lam : Expr (a :: G) t -> Expr G (TyFun a t)
      App : Expr G (TyFun a t) -> Expr G a -> Expr G t
      Op  : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
            Expr G c
      If  : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
      Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b

  dsl expr
      lambda      = Lam
      variable    = Var
      index_first = stop
      index_next  = pop

  (<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
  (<$>) = \f, a => App f a

  pure : Expr G a -> Expr G a
  pure = id

  syntax IF [x] THEN [t] ELSE [e] = If x t e

  (==) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool
  (==) = Op (==)

  (<) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool
  (<) = Op (<)

  instance Num (Expr G TyInt) where
    (+) x y = Op (+) x y
    (-) x y = Op (-) x y
    (*) x y = Op (*) x y

    abs x = IF (x < 0) THEN (-x) ELSE x

    fromInteger = Val . fromInteger

  interp : Env G -> {static} Expr G t -> interpTy t
  interp env (Var i)     = lookup i env
  interp env (Val x)     = x
  interp env (Lam sc)    = \x => interp (x :: env) sc
  interp env (App f s)   = (interp env f) (interp env s)
  interp env (Op op x y) = op (interp env x) (interp env y)
  interp env (If x t e)  = if (interp env x) then (interp env t) else (interp env e)
  interp env (Bind v f)  = interp env (f (interp env v))

  eId : Expr G (TyFun TyInt TyInt)
  eId = expr (\x => x)

  eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
  eTEST = expr (\x, y => y)

  eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
  eAdd = expr (\x, y => Op (+) x y)

  eDouble : Expr G (TyFun TyInt TyInt)
  eDouble = expr (\x => App (App eAdd x) (Var stop))

  eFac : Expr G (TyFun TyInt TyInt)
  eFac = expr (\x => IF x == 0 THEN 1 ELSE [| eFac (x - 1) |] * x)

testFac : Int
testFac = interp [] eFac 4

main : IO ()
main = print testFac


text:
module Compiler.RefC

import public Compiler.RefC.CC
import public Compiler.RefC.RefC


text:
import CommonTestingStuff

par : Applicative m => Coop m Unit -> Coop m Unit -> Coop m Unit
par = ignore .: zip

export
main : IO Unit
main = do putStrLn "before coop"
          runCoop $ do
  offset <- currentTime
  printTime offset "start"
  par
    (forever $ do
      printTime offset "proc 1, before 1000"
      sleepFor 1.seconds
      printTime offset "proc 1, before 2000"
      sleepFor 2.seconds)
    (forever $ do
      printTime offset "                     proc 2, before 350"
      sleepFor 350.millis
      printTime offset "                     proc 2, before 750"
      sleepFor 750.millis)
  printTime offset "end"


text:
module Dec

import Basic
import Unit
import Void
import Coproduct

import Path
import General

public export
Dec : Type -> Type
Dec a = a + Neg a

public export
DecEq : Type -> Type
DecEq a = (x, y : a) -> Dec (x == y)


text:
module Blockchain

import Data.Hash

%default total
-- TODO public export is temporary
%access public export

{-
   Conceptual, dependently typed implementation of a blockchain using
   (not cryptographic) Data.Hash.
   I plan on trying to covert this to use
     https://github.com/idris-hackers/idris-crypto

   This module implements blockchain (cryptographic linked list) that provides
   type level guarantee of cryptographic correctness of hashes.
   It does not implement anything else (P2P networking, payloads stored in chain,
   consensus protocol, etc).
-}

------------------------------
--- HList and other utilitities
------------------------------
namespace HList
  infixr 7 ::
  data HList : List Type -> Type where
    HNil : HList []
    (::) : t -> HList ts -> HList (t :: ts)

  ||| Show instance is used for testing
  Show (HList []) where
     show x = "HNil"
  (Show a, Show (HList xs)) => Show (HList (a :: xs)) where
     show (t :: xt) = (show t) ++ "::" ++ (show xt)

||| Testing convenience class
||| ```idris example
|||  the (List String) (asList ("2" :: 1 :: HNil))
||| ```
||| Interstingly doing something similar with Monoids
||| does not seem to go far
interface AsList a b where
   asList : a -> List b
AsList (HList []) b where
   asList = const []
(AsList (HList xs) b, Cast a b) => AsList (HList (a :: xs)) b where
   asList (t :: xt) = (cast t) :: (asList xt)
||| Idris does not have this
||| https://github.com/idris-lang/Idris-dev/issues/3479
Cast a a where
   cast = id

-----------------------------------------------
-- Temporary non-crypto hashing abstracted out
-----------------------------------------------

BlockHash : Type
BlockHash = Bits64

GenesisHash : BlockHash
GenesisHash = hash ()

GenesisFn : () -> BlockHash
GenesisFn = hash -- (const (hash ()))

strHash : String -> BlockHash
strHash = hash

--------------------
-- DSLs
--------------------

||| Conceptual code does not want to concern itself with particulars
||| of how this is done. The implementation of this interface is assumed
||| to correctly compute hashes.
||| TODO think about it more - move to a more explicit hashing?
interface BlockData a where
    serialize : a -> String
    blockHash : a -> BlockHash
    blockHash = strHash . serialize
    prevHash : a -> BlockHash

-- Interestingly things stop compiling if blockHash method is moved out from
-- the interface!
-- blockHash : BlockData a => a -> BlockHash
-- blockHash = strHash . serialize

--------------------------------
-- Simple homogenious blockchain
--------------------------------

namespace SimpleBlockchain
  ||| See Test.Blockchain for example
  data SimpleBlockchain : (payload : Type) -> (hash : BlockHash) -> Type where
     Genesis : SimpleBlockchain a GenesisHash
     (::) : BlockData a => (payload : a) -> SimpleBlockchain a (prevHash payload) -> SimpleBlockchain a (blockHash payload)

--------------------------------------------------
-- Heterogenous blockchain with varying payloads
-- Can blockchain be general purpose and store various types of payloads?
--------------------------------------------------

-- TODO this is getting better but still needs more thinking

namespace Block
  ||| `Block payload hash hash_fn` looks like standard dependently typed
  |||  indexed monad (or state machine).
  |||  @ payload that contains previous hash and can be hashed (satisfies BlockData contraint)
  |||  @ hash links previous block
  |||  @ hash_fn hash function that knows how to sign the payload
  data Block : (payload : Type) -> (hash: BlockHash) -> (hash_fn : payload -> BlockHash) -> Type where
      MkBlock : BlockData a => (payload : a) -> Block a (prevHash payload) blockHash

      Genesis : Block () 0 GenesisFn
      ||| This is currently not used,
      ||| monadic function verifies (on type level) previous payload hash (payload : a) and
      ||| exposes proof of that verification (hash2_fn payload)
      ||| as well as provides hash function that works on its own payload.
      (>>=) : Block a hash1 hash2_fn ->
              ((payload : a) -> Block b (hash2_fn payload) hash3_fn) ->
              Block b (hash2_fn payload) hash3_fn

extractPayload : Block a h hash_fn -> a
extractPayload (MkBlock p) = p
extractPayload Genesis = ()
extractPayload (block1 >>= fn) = extractPayload (fn (extractPayload block1))

extractPrevHash : Block a h hash_fn -> BlockHash
extractPrevHash (MkBlock p) = prevHash p
extractPrevHash Genesis = 0
extractPrevHash (block1 >>= fn) = extractPrevHash (fn (extractPayload block1))

computeHash : Block a h hash_fn -> BlockHash
computeHash (MkBlock p) = blockHash p
computeHash Genesis = GenesisFn ()
computeHash (block1 >>= fn) = computeHash (fn (extractPayload block1))

namespace HBlockchain
  ||| This blockchain allows heterogeneous blocks with different payloads and different
  ||| (payload dependent) hashing algorithms.
  ||| The crypto-correctness of the chain is guaranteed by the type.
  |||
  ||| This blockchain maintains the 'running' last block hash
  ||| @ payloads the type level list of payload types does not buy me much except for
  ||| having a simple extractPayloads function
  data HBlockchain : (payloads : List Type) -> BlockHash -> Type where
       Single : Block () 0 GenesisFn -> HBlockchain [] GenesisHash
       (::) : (block : Block a h1 hash_fn) -> HBlockchain ax h1 -> HBlockchain (a::ax) (hash_fn (extractPayload block))

extractPayloads : HBlockchain payloads hs -> HList payloads
extractPayloads (Single g) = HNil
extractPayloads (block :: chain) =  (extractPayload block) :: extractPayloads chain

||| Untyping convenient for testing
AsList (HList payloads) b => AsList (HBlockchain payloads hs) b where
   asList = asList . extractPayloads

extractPrevHashes : HBlockchain payloads hs -> List BlockHash
extractPrevHashes (Single g) = [0]
extractPrevHashes (block :: chain) = (extractPrevHash block) :: extractPrevHashes chain

computeHashes : HBlockchain payloads hs -> List BlockHash
computeHashes (Single g) = [GenesisFn ()]
computeHashes (block :: chain) = (computeHash block) :: computeHashes chain

-------------------------------
-- Examples
-- for example usage see `Test.Blockchain` module
-------------------------------
exampleMiner : BlockData a => (payload : a) -> HBlockchain ax (prevHash payload) -> HBlockchain (a :: ax) (blockHash payload)
exampleMiner payload chain =  (MkBlock payload) :: chain

max_stars_repo_name: rpeszek/idris-chain

max_issues_repo_name: rpeszek/idris-chain

max_forks_repo_name: rpeszek/idris-chain


text:
||| Logging utilities for the LSP server implementation.
|||
||| (C) The Idris Community, 2021
module Server.Log

import Core.Core
import Server.Configuration
import Server.Utils
import System.File

%default total

-- TODO: Very crude logging, we should probably adopt a more flexible logging mechanism.
--       Maybe comonads, à la Haskell co-log package?

||| Type for the severity of logging messages.
public export
data Severity = Debug | Info | Warning | Error | Critical

Cast Severity Integer where
  cast Debug    = 0
  cast Info     = 1
  cast Warning  = 2
  cast Error    = 3
  cast Critical = 4

export
Eq Severity where
  Debug    == Debug    = True
  Info     == Info     = True
  Warning  == Warning  = True
  Error    == Error    = True
  Critical == Critical = True
  _ == _ = False

export
Show Severity where
  show Debug    = "DEBUG"
  show Info     = "INFO"
  show Warning  = "WARNING"
  show Error    = "ERROR"
  show Critical = "CRITICAL"

export
Ord Severity where
  compare x y = compare (cast {to = Integer} x) (cast y)

||| Logs a string with the provided severity level.
export
logString : Ref LSPConf LSPConfiguration => Severity -> String -> Core ()
logString severity msg = do
  logHandle <- gets LSPConf logHandle
  coreLift_ $ fPutStrLn logHandle ("LOG " ++ show severity ++ ": " ++ msg)
  coreLift_ $ fflush logHandle
--   fPutStrLn stderr ("LOG " ++ show severity ++ ": " ++ msg) *> pure ()
||| Logs a showable value with the provided severity level.
export
logShow : Ref LSPConf LSPConfiguration => Show a => Severity -> a -> Core ()
logShow severity = logString severity . show


text:
module Effekt.CpsUnstaged

public export
Cps : Type -> Type -> Type
Cps r a = (a -> r) -> r

shift0 : ((a -> r) -> r) -> Cps r a
shift0 = id

runIn0 : Cps r a -> (a -> r) -> r
runIn0 = id

reset0 : Cps r r -> r
reset0 m = runIn0 m id

pure : a -> Cps r a
pure a = \k => k a

push : (a -> Cps r b) -> (b -> r) -> (a -> r)
push f k = \a => f a k

bind : Cps r a -> (a -> Cps r b) -> Cps r b
bind m f = \k => m (push f k)

(>>=) : Cps r a -> (a -> Cps r b) -> Cps r b
m >>= f = bind m f

example : Int
example = 1 + reset0 (do
  x <- shift0 (\k => k (k 100))
  pure (10 + x))

max_stars_repo_name: b-studios/idris-effekt

max_issues_repo_name: b-studios/idris-effekt

max_forks_repo_name: b-studios/idris-effekt


text:
module Data.Either

import public Control.Function
import Data.List1

%default total

--------------------------------------------------------------------------------
-- Checking for a specific constructor

||| Extract the Left value, if possible
public export
getLeft : Either a b -> Maybe a
getLeft (Left a) = Just a
getLeft _ = Nothing

||| Extract the Right value, if possible
public export
getRight : Either a b -> Maybe b
getRight (Right b) = Just b
getRight _ = Nothing

||| True if the argument is Left, False otherwise
public export
isLeft : Either a b -> Bool
isLeft (Left _)  = True
isLeft (Right _) = False

||| True if the argument is Right, False otherwise
public export
isRight : Either a b -> Bool
isRight (Left _)  = False
isRight (Right _) = True

||| Proof that an `Either` is actually a Right value
public export
data IsRight : Either a b -> Type where
  ItIsRight : IsRight (Right x)

export
Uninhabited (IsRight (Left x)) where
  uninhabited ItIsRight impossible

||| Proof that an `Either` is actually a Left value
public export
data IsLeft : Either a b -> Type where
  ItIsLeft : IsLeft (Left x)

export
Uninhabited (IsLeft (Right x)) where
  uninhabited ItIsLeft impossible

--------------------------------------------------------------------------------
-- Grouping values

||| Compress the list of Lefts and Rights by accumulating
||| all of the lefts and rights into non-empty blocks.
export
compress : List (Either a b) -> List (Either (List1 a) (List1 b))
compress [] = []
compress (Left x :: abs) = compressLefts (singleton x) abs where
  compressLefts : List1 a -> List (Either a b) -> List (Either (List1 a) (List1 b))
  compressLefts acc (Left a :: abs) = compressLefts (cons a acc) abs
  compressLefts acc abs = Left (reverse acc) :: compress abs
compress (Right y :: abs) = compressRights (singleton y) abs where
  compressRights : List1 b -> List (Either a b) -> List (Either (List1 a) (List1 b))
  compressRights acc (Right b :: abs) = compressRights (cons b acc) abs
  compressRights acc abs = Right (reverse acc) :: compress abs

||| Decompress a compressed list. This is the left inverse of `compress` but not its
||| right inverse because nothing forces the input to be maximally compressed!
export
decompress : List (Either (List1 a) (List1 b)) -> List (Either a b)
decompress = concatMap $ \case
  Left  as => map Left  $ forget as
  Right bs => map Right $ forget bs

||| Keep the payloads of all Left constructors in a list of Eithers
public export
lefts : List (Either a b) -> List a
lefts []              = []
lefts (Left  l :: xs) = l :: lefts xs
lefts (Right _ :: xs) = lefts xs

||| Keep the payloads of all Right constructors in a list of Eithers
public export
rights : List (Either a b) -> List b
rights []              = []
rights (Left  _ :: xs) = rights xs
rights (Right r :: xs) = r :: rights xs

||| Split a list of Eithers into a list of the left elements and a list of the right elements
public export
partitionEithers : List (Either a b) -> (List a, List b)
partitionEithers l = (lefts l, rights l)

||| Remove a "useless" Either by collapsing the case distinction
public export
fromEither : Either a a -> a
fromEither (Left l)  = l
fromEither (Right r) = r

||| Right becomes left and left becomes right
public export
mirror : Either a b -> Either b a
mirror (Left  x) = Right x
mirror (Right x) = Left x

--------------------------------------------------------------------------------
-- Bifunctor

export
pushInto : c -> Either a b -> Either (c, a) (c, b)
pushInto c = bimap (\ a => (c, a)) (\ b => (c, b))
  -- ^ not using sections to keep it backwards compatible

--------------------------------------------------------------------------------
-- Conversions
--------------------------------------------------------------------------------

||| Convert a Maybe to an Either by using a default value in case of Nothing
||| @ e the default value
public export
maybeToEither : (def : Lazy e) -> Maybe a -> Either e a
maybeToEither def (Just j) = Right j
maybeToEither def Nothing  = Left  def

||| Convert an Either to a Maybe from Right injection
public export
eitherToMaybe : Either e a -> Maybe a
eitherToMaybe (Left _) = Nothing
eitherToMaybe (Right x) = Just x

export
eitherMapFusion : (f : _) -> (g : _) -> (p : _) -> (e : Either a b) -> either f g (map p e) = either f (g . p) e
eitherMapFusion f g p $ Left x  = Refl
eitherMapFusion f g p $ Right x = Refl

export
eitherBimapFusion : (f : _) -> (g : _) -> (p : _) -> (q : _) -> (e : _) -> either f g (bimap p q e) = either (f . p) (g . q) e
eitherBimapFusion f g p q $ Left z  = Refl
eitherBimapFusion f g p q $ Right z = Refl

-- Injectivity of constructors

||| Left is injective
export
Injective Left where
  injective Refl = Refl

||| Right is injective
export
Injective Right where
  injective Refl = Refl


text:
module Main

main : IO ()
main = putStrLn "Hello, binary example of idris ;)"


text:
module Main

main : IO ()
main = putStrLn ?greeting

even : Nat -> Bool
even Z = True
even (S k) = ?even_rhs

isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

sum2 : (single : Bool) -> isSingleton single -> Nat
sum2 True x = x
sum2 False [] = 0
sum2 False (x :: xs) = x + sum2 False xs

data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : a -> Vect h a -> Vect (S h) a

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

data Fin : Nat -> Type where
  FZ : Fin (S k)
  FS : Fin k -> Fin (S k)

max_stars_repo_name: nunet-io/snet-ai-dsl

max_issues_repo_name: nunet-io/snet-ai-dsl

max_forks_repo_name: nunet-io/snet-ai-dsl


text:
data MyNat
    = S (Inf MyNat)
    | Z

%builtin Natural MyNat


text:
module Raytracer
import Units
import Vector
import PPM

%default total

data Point = P (Dim Meters) (Dim Meters) (Dim Meters)

data Ray = R Point Vector

(+) : Point -> Vector -> Point
(P (M x) (M y) (M z)) + (V a b c) = P (M (x + a)) (M (y + b)) (M (z + c))

data Object : Type where
  Sphere : (center : Point) -> (radius : Dim Meters) -> Object

toRad : Dim Degrees -> Dim Radians
toRad (Deg d) = Rad $ d * (pi / 180)

tan : Dim Radians -> Float
tan (Rad r) = tan r

record Scene : Type where
  MkScene : (objects : List Object) ->
            (lights : List Point) -> -- light sources
            (camera : Point) -> -- camera location
            (lookingAt : Point) ->
            (fieldOfView : Dim Degrees) ->
            (background : Color) ->
            Scene

width : Scene -> Float
width s = tan (toRad (fieldOfView s)) * 2

height : Scene -> Float
height = width

--trace : Ray -> Scene -> Color
--

max_stars_repo_name: david-christiansen/idris-raytracer

max_issues_repo_name: david-christiansen/idris-raytracer

max_forks_repo_name: david-christiansen/idris-raytracer


text:
module Control.Comonad.Traced.Interface

import Data.Morphisms

import Control.Comonad
import Control.Comonad.Env.Env
import Control.Comonad.Store.Store
import Control.Comonad.Traced.Traced
import Control.Comonad.Trans

%default total

public export
interface Comonad w => ComonadTraced m w | w where
  trace : m -> w a -> a

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

public export %inline
traces : ComonadTraced m w => (a -> m) -> w a -> a
traces f wa = trace (f $ extract wa) wa

public export %inline
lowerTrace : (ComonadTrans t, ComonadTraced m w) => m -> t w a -> a
lowerTrace m = trace m . lower

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

public export %inline
Monoid m => ComonadTraced m (Morphism m) where
  trace m (Mor f) = f m

public export %inline
ComonadTraced m w => ComonadTraced m (EnvT e w) where
  trace = lowerTrace

public export %inline
ComonadTraced m w => ComonadTraced m (StoreT s w) where
  trace = lowerTrace

public export %inline
(Comonad w, Monoid m) => ComonadTraced m (TracedT m w) where
  trace m (MkTracedT wf) = extract wf m


text:
{-
Copyright 2019, 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 StwfFFI.GPIO

%access public export
%default total

%include C "beaglebone.h"
%include C "gpio_v2.h"

{- FFI to
    void GPIO1ModuleClkConfig(void)
-}
gpio1ModuleClkConfig : IO ()
gpio1ModuleClkConfig =
    foreign FFI_C "GPIO1ModuleClkConfig" (IO ())

{- FFI to
    void GPIO1Pin23PinMuxSetup(void)
-}
gpio1Pin23PinMuxSetup : IO ()
gpio1Pin23PinMuxSetup =
    foreign FFI_C "GPIO1Pin23PinMuxSetup" (IO ())

{- FFI to
    void GPIOModuleEnable(unsigned int baseAdd)
-}
gpioModuleEnable : Bits32 -> IO ()
gpioModuleEnable base =
    foreign FFI_C "GPIOModuleEnable" (Bits32 -> IO ()) base

{- FFI to
    void GPIOModuleReset(unsigned int baseAdd)
-}
gpioModuleReset : Bits32 -> IO ()
gpioModuleReset base =
    foreign FFI_C "GPIOModuleReset" (Bits32 -> IO ()) base

{- FFI to
    void GPIODirModeSet(
        unsigned int baseAdd,
        unsigned int pinNumber,
        unsigned int pinDirection)
-}
gpioDirModeSet : Bits32 -> Int -> Int -> IO ()
gpioDirModeSet base pin dir =
    foreign FFI_C "GPIODirModeSet" (Bits32 -> Int -> Int -> IO ()) base pin dir

{- FFI to
    void GPIOPinWrite(
        unsigned int baseAdd,
        unsigned int pinNumber,
        unsigned int pinValue)
-}
gpioPinWrite : Bits32 -> Int -> Bool -> IO ()
gpioPinWrite base pin val =
    foreign FFI_C "GPIOPinWrite" (Bits32 -> Int -> Int -> IO ()) base pin (if val then 1 else 0)

max_stars_repo_name: mokshasoft/bare-metal-idris-drivers

max_issues_repo_name: mokshasoft/bare-metal-idris-drivers

max_forks_repo_name: mokshasoft/bare-metal-idris-drivers


text:
import ProcessLib

data ListAction : Type where
     Length : List elem -> ListAction
     Append : List elem -> List elem -> ListAction

ListType : ListAction -> Type
ListType (Length xs) = Nat
ListType (Append {elem} xs ys) = List elem

total
procList : Service ListType ()
procList = do Respond (\msg => case msg of
                                    Length xs => Pure (length xs)
                                    Append xs ys => Pure (xs ++ ys))
              Loop procList

procMain : Client ()
procMain = do Just list <- Spawn procList
                      | Nothing => Action (putStrLn "Spawn failed")
              len <- Request list (Length [1,2,3])
              Action (printLn len)

              app <- Request list (Append [1,2,3] [4,5,6])
              Action (printLn app)

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Data.Profunctor.Choice

import Data.Profunctor.Class
import Data.Morphisms

public export
interface Profunctor p => Choice (0 p : Type -> Type -> Type) where
  left' : p a b -> p (Either a c) (Either b c)
  left' = dimap (either Right Left) (either Right Left) . right'

  right' : p a b -> p (Either c a) (Either c b)
  right' = dimap (either Right Left) (either Right Left) . left'

public export
Choice Morphism where
  left' (Mor f) = Mor g
    where g : Either a c -> Either b c
          g (Left a) = Left (f a)
          g (Right c) = Right c

  right' (Mor f) = Mor g
    where g : Either c a -> Either c b
          g (Left c) = Left c
          g (Right a) = Right (f a)


text:
module Finmath.Vector

import Finite

--------------------------------------------------------------------------------
-- Equivalence of vectors and maps on finite sets
--------------------------------------------------------------------------------

||| Map from a vector to a function on a finite set
||| Note that this is the Prelude.Vect.index with the arguments reversed.
vectToMap : Vect n a -> Fin n -> a
vectToMap (x :: xs) fZ     = x
vectToMap (x :: xs) (fS k) = vectToMap xs k

||| The inverse of vectToMap
mapToVect : (Fin n -> a) -> Vect n a
mapToVect {n=Z} f     = []
mapToVect {n=(S k)} f = (f fZ) :: (mapToVect (f . fS))

--------------------------------------------------------------------------------
-- Operations on vectors derived from operations on finite sets by duality
--------------------------------------------------------------------------------

||| Concatenates two vectors
concat : Vect n a -> Vect m a -> Vect (n + m) a
concat v w = mapToVect ((either (vectToMap v) (vectToMap w)) . fSetSumInv)

||| Splits a vector
split : Vect (n + m) a -> (Vect n a, Vect m a)
split {n}{m} v = let f = (vectToMap v) . (fSetSum {m=m}{n=n}) in
  (mapToVect (f . Left), mapToVect (f . Right))

||| Unflattens a vector
unFlatten : Vect (n * m) a -> Vect n (Vect m a)
unFlatten v = let f = \x => \y => (vectToMap v) (fSetProduct (x,y)) in
  mapToVect (mapToVect . f)

--------------------------------------------------------------------------------
-- Misc vector operations
--------------------------------------------------------------------------------

||| like Prelude.Vect.findIndices but using Fin, not Nat
findIndices' : (a -> Bool) -> Vect m a -> (p ** Vect p (Fin m))
findIndices' p [] = (_ ** [])
findIndices' p (x::xs) with (findIndices' p xs)
      | (_ ** tail) =
       if p x then
        (_ ** fZ::(map fS tail))
       else
        (_ ** (map fS tail))

-- Heterogeneous (Mixed) Tuples

--Mixed tuple of order k
MixedTuple : (Fin k -> Type) -> Type
MixedTuple sig = (i : Fin _) -> sig i

--Pullback of dependent function
pullback : (a -> b) -> (b -> c) -> (a -> c)
pullback f = \g => g . f

pullback' : (s : a -> Type) -> (s' : b -> Type) -> (f : a -> b) -> s = s' . f -> ((y : b) -> s' y) -> ((x : a) -> s x)
pullback' s s' f p = \g => \x => rewrite p in (g (f x))

--(Unknown name) mapping from mixed tuples induced by mapping on signatures
myMap : (s : Fin k -> Type) -> (s' : Fin k' -> Type) -> (f : Fin k -> Fin k') -> s = s' . f -> MixedTuple s' -> MixedTuple s
myMap s s' f p g = pullback' s s' f p g

NDVector : (Fin k -> Nat) -> Type -> Type
NDVector s a = (MixedTuple (Fin . s)) -> a

max_stars_repo_name: KesterTong/idris-finite-math

max_issues_repo_name: silky/idris-finite-math

max_forks_repo_name: silky/idris-finite-math


text:
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
    putStrLn "Enter your name: "
    name <- getLine
    if name == ""
      then Quit ()
      else
        do
          putStrLn ("Your name is " ++ name)
          greet

data Fuel = Dry | More (Lazy Fuel)

forever : Fuel
forever = More forever

run: Fuel -> RunIO a -> IO (Maybe a)
run Dry         y             = pure Nothing
run (More fuel) (Quit result) = pure (Just result)
run (More fuel) (Do io func)  =
  do
    result <- io
    run fuel (func result)

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

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Language.LSP.Metavars

import Core.Context
import Core.Core
import Core.Directory
import Core.Env
import Core.TT
import Core.Name
import Idris.IDEMode.Holes
import Idris.Pretty
import Idris.Pretty.Render
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.JSON
import Language.LSP.Message
import Language.LSP.Definition
import Server.Configuration
import Server.Log
import Server.Utils
import System.File
import System.Path
import Language.Reflection
import Libraries.Text.PrettyPrint.Prettyprinter.Symbols

%language ElabReflection
%hide Language.Reflection.TT.FC
%hide Language.Reflection.TT.Name

-- Non-exported functions are temporary changes to functions in the module Idris.IDEMode.Holes.
-- TODO: upstream changes to the compiler when stability is reached.

public export
record Premise where
  constructor MkPremise
  name : String
  location : Maybe Location
  type : String
  multiplicity : String
  isImplicit : Bool
%runElab deriveJSON defaultOpts `{Metavars.Premise}

public export
record Metavar where
  constructor MkMetavar
  name : String
  location : Maybe Location
  type : String
  premises : List Metavars.Premise
%runElab deriveJSON defaultOpts `{Metavars.Metavar}

showName : Name -> Bool
showName (UN Underscore) = False
showName (MN _ _) = False
showName _ = True

getUserHolesData : Ref Ctxt Defs
                => Ref Syn SyntaxInfo
                => Core (List (Holes.Data, FC))
getUserHolesData = do
  defs <- get Ctxt
  ms <- getUserHoles
  globs <- concat <$> traverse (flip lookupCtxtName defs.gamma) ms
  let holesWithArgs = mapMaybe (\(n, i, gdef) => pure (n, gdef, !(isHole gdef))) globs
  traverse (\(n, gdef, args) => (, gdef.location) <$> holeData defs [] n args gdef.type) holesWithArgs

||| Returns the list of metavariables visible in the current context with their location.
||| JSON schema for a single metavariable:
||| {
|||   location: Location | null;
|||   name: string;
|||   type: string;
|||   premises: Premise[]
||| }
||| JSON schema for a single premise:
||| {
|||   location: Location | null;
|||   name: string;
|||   type: string;
|||   multiplicity: string;
|||   isImplicit: bool;
||| }
export
metavarsCmd : Ref Ctxt Defs
           => Ref Syn SyntaxInfo
           => Ref ROpts REPLOpts
           => Ref LSPConf LSPConfiguration
           => Core (List Metavar)
metavarsCmd = do
  logI Metavars "Fetching metavars"
  c <- getColor
  setColor False
  holes <- Metavars.getUserHolesData
  logI Metavars "Metavars fetched, found \{show $ length holes}"
  res <- for holes $ \(h, fc) => do
    loc <- mkLocation fc
    let name = show h.name
    type <- render (reAnnotate Syntax $ prettyTerm h.type)
    premises <- for h.context $ \p => do
      loc <- mkLocation replFC
      let name = show p.name
      type <- render (reAnnotate Syntax $ prettyTerm p.type)
      pure $ MkPremise { location = loc, name = name, type = type, isImplicit = p.isImplicit, multiplicity = show p.multiplicity }
    pure $ MkMetavar { location = loc, name = name, type = type, premises = premises }
  setColor c
  pure res


text:
-- Exercise_4_2.idr
--

import Data.Vect

||| Take the first n elements of given Vect xs
vectTake : (n : Nat) -> (xs : Vect (n + m) a) -> Vect n a
vectTake Z [] = []
vectTake Z (x :: xs) = []
vectTake (S k) (x :: xs) = x :: vectTake k xs

||| Calculate sum of selected entries, return Nothing if index
||| is out of bounds
sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a ->
             Maybe a
sumEntries {n} pos xs ys = case integerToFin pos n of
                                Nothing => Nothing
                                (Just x) => Just ((index x xs) + (index x ys))

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Himp

import Assn
import Expr
import Logic
import Maps

%access public export

%default total

data HCom : Type where
  HCSkip : HCom
  HCAss : (x : Id) -> (a : AExp) -> HCom
  HCSeq : (c1 : HCom) -> (c2 : HCom) -> HCom
  HCIf : (b : BExp) -> (ct : HCom) -> (cf : HCom) -> HCom
  HCWhile : (b : BExp) -> (c : HCom) -> HCom
  HCHavoc : (x : Id) -> HCom

SKIP : HCom
SKIP = HCSkip

infix 5 ::=

(::=) : Id -> AExp -> HCom
(::=) = HCAss

(>>=) : HCom -> (() -> HCom) -> HCom
(>>=) c f = HCSeq c (f ())

WHILE : BExp -> HCom -> HCom
WHILE = HCWhile

syntax IFB [b] THEN [ct] ELSE [cf] FI = HCIf b ct cf

HAVOC : Id -> HCom
HAVOC = HCHavoc

data HCEval : HCom -> State -> State -> Type where
  E_Skip : HCEval HCSkip st st
  E_Ass : aeval st a1 = n -> HCEval (HCAss x a1) st (t_update x n st)
  E_Seq : HCEval c1 st1 st2 -> HCEval c2 st2 st3 ->
          HCEval (HCSeq c1 c2) st1 st3
  E_IfTrue : beval st b = True -> HCEval c1 st st1 ->
             HCEval (HCIf b c1 c2) st st1
  E_IfFalse : beval st b = False -> HCEval c2 st st1 ->
              HCEval (HCIf b c1 c2) st st1
  E_WhileEnd : beval st b = False -> HCEval (HCWhile b c) st st
  E_WhileLoop : beval st b = True ->
                HCEval c st st1 -> HCEval (HCWhile b c) st1 st2 ->
                HCEval (HCWhile b c) st st2
  E_Havoc : (n : Nat) -> HCEval (HCHavoc x) st (t_update x n st)

syntax [c1] "/" [st1] "\\\\" [st2] = HCEval c1 st1 st2

havoc_example_1 : (HAVOC X) / Expr.empty_state \\ (t_update X 0 Expr.empty_state)
havoc_example_1 = E_Havoc 0

havoc_example_2 : (do SKIP; HAVOC Z)
                  / Expr.empty_state \\ (t_update Z 42 Expr.empty_state)
havoc_example_2 = E_Seq E_Skip (E_Havoc 42)

HCEquiv : (c1, c2 : HCom) -> Type
HCEquiv c1 c2 = (st, st' : State) -> ((c1 / st \\ st') ↔ (c2 / st \\ st'))

havoc_property : Not (x = y) -> st x = n -> ((HAVOC y) / st \\ st') -> st' x = n
havoc_property contra prf (E_Havoc _) =
  rewrite snd beq_id_false_iff $ neqSym contra
  in prf

pXY : HCom
pXY = do HAVOC X
         HAVOC Y

pYX : HCom
pYX = do HAVOC Y
         HAVOC X

x_neq_y : Not (Expr.X = Expr.Y)
x_neq_y Refl impossible

pXY_equiv_pYX : Either (HCEquiv Himp.pXY Himp.pYX)
                       (Not (HCEquiv Himp.pXY Himp.pYX))
pXY_equiv_pYX = Left $ \st, st' =>
  (forward st st', backward st st')
where forward : (st, st' : State) ->
                (Himp.pXY / st \\ st') -> (Himp.pYX / st \\ st')
      forward st _ (E_Seq (E_Havoc n) (E_Havoc m)) =
        rewrite t_update_permute {x1=Y} {v1=m} {x2=X} {v2=n} {m=st}
                                 x_neq_y
        in E_Seq (E_Havoc m) (E_Havoc n)
      backward : (st, st' : State) ->
                 (Himp.pYX / st \\ st') -> (Himp.pXY / st \\ st')
      backward st _ (E_Seq (E_Havoc n) (E_Havoc m)) =
        rewrite t_update_permute {x1=X} {v1=m} {x2=Y} {v2=n} {m=st}
                                 (neqSym x_neq_y)
        in E_Seq (E_Havoc m) (E_Havoc n)

ptwice : HCom
ptwice = do HAVOC X
            HAVOC Y

pcopy : HCom
pcopy = do HAVOC X
           Y ::= X

ptwice_inequiv_pcopy : Either (HCEquiv Himp.ptwice Himp.pcopy)
                              (Not (HCEquiv Himp.ptwice Himp.pcopy))
ptwice_inequiv_pcopy = Right $ \equiv =>
  let st' = t_update Y 1 $ t_update X 0 empty_state
  in case fst (equiv empty_state st') (E_Seq (E_Havoc 0) (E_Havoc 1)) of
       E_Seq _ E_Skip impossible
       E_Seq _ (E_Ass _) impossible
       E_Seq _ (E_Seq _ _) impossible
       E_Seq _ (E_IfTrue _ _) impossible
       E_Seq _ (E_IfFalse _ _) impossible
       E_Seq _ (E_WhileEnd _) impossible
       E_Seq _ (E_WhileLoop _ _ _) impossible
       E_Seq _ (E_Havoc _) impossible

p1 : HCom
p1 = WHILE (not (X == 0)) $ do
       HAVOC Y
       X ::= X + 1

p2 : HCom
p2 = WHILE (not (X == 0)) $
       SKIP

p1_may_diverge : Not (st X = 0) -> Not (Himp.p1 / st \\ st')
p1_may_diverge {st'} contra (E_WhileEnd prf) with (st' X)
  p1_may_diverge {st'} contra (E_WhileEnd prf) | Z = contra Refl
  p1_may_diverge {st'} contra (E_WhileEnd prf) | S _ = absurd prf
p1_may_diverge contra (E_WhileLoop _ (E_Seq {st2} _ (E_Ass prf)) next) =
  let h_prf = sym $ trans (plusCommutative 1 (st2 X)) prf
  in p1_may_diverge {st=t_update X _ _}
                    (n_eq_succ__n_neq_0 {k=st2 X} h_prf) next

p2_may_diverge : Not (st X = 0) -> Not (Himp.p2 / st \\ st')
p2_may_diverge {st'} contra (E_WhileEnd prf) =
  let st_X_beq_0 = trans (sym (notInvolutive (st' X == 0)))
                         (cong {f=Bool.not} prf)
  in contra (fst (nat_beq_iff (st' X) 0) st_X_beq_0)
p2_may_diverge contra (E_WhileLoop _ E_Skip next) = p2_may_diverge contra next

p1_p2_equiv : HCEquiv Himp.p1 Himp.p2
p1_p2_equiv st st' = (forward, backward)
where forward : (Himp.p1 / st \\ st') -> (Himp.p2 / st \\ st')
      forward rel = case rel of
        E_WhileEnd prf => E_WhileEnd prf
        E_WhileLoop prf _ _ =>
          let st_X_neq_0 = fst (nat_nbeq_iff (st X) 0)
                               (trans (sym (notInvolutive (st X == 0)))
                                      (cong {f=Bool.not} prf))
          in absurd $ p1_may_diverge st_X_neq_0 rel
      backward : (Himp.p2 / st \\ st') -> (Himp.p1 / st \\ st')
      backward rel = case rel of
        E_WhileEnd prf => E_WhileEnd prf
        E_WhileLoop prf _ _ =>
          let st_X_neq_0 = fst (nat_nbeq_iff (st X) 0)
                               (trans (sym (notInvolutive (st X == 0)))
                                      (cong {f=Bool.not} prf))
          in absurd $ p2_may_diverge st_X_neq_0 rel

p3 : HCom
p3 = do Z ::= 1
        WHILE (not (X == 0)) $ do
          HAVOC X
          HAVOC Z

p4 : HCom
p4 = do X ::= 0
        Z ::= 1

p3_p4_inequiv : Not (HCEquiv Himp.p3 Himp.p4)
p3_p4_inequiv equiv =
  let st = t_update X 1 empty_state
      st' = t_update Z 2 $ t_update X 0 $ t_update Z 1 st
  in case fst (equiv st st')
              (E_Seq (E_Ass Refl)
                     (E_WhileLoop Refl
                                  (E_Seq (E_Havoc 0) (E_Havoc 2))
                                  (E_WhileEnd Refl))) of
       (E_Seq (E_Ass _) E_Skip) impossible
       (E_Seq (E_Ass _) (E_Ass _)) impossible
       (E_Seq (E_Ass _) (E_Seq _ _)) impossible
       (E_Seq (E_Ass _) (E_IfTrue _ _)) impossible
       (E_Seq (E_Ass _) (E_IfFalse _ _)) impossible
       (E_Seq (E_Ass _) (E_WhileEnd _)) impossible
       (E_Seq (E_Ass _) (E_WhileLoop _ _ _)) impossible
       (E_Seq (E_Ass _) (E_Havoc _)) impossible

p5 : HCom
p5 = WHILE (not (X == 1)) $
       HAVOC X

p6 : HCom
p6 = X ::= 1

overwriting_write : ((x ::= ANum n) / (t_update x v st) \\ st') ->
                    ((x ::= ANum n) / st \\ st')
overwriting_write {x} {n} {v} {st} (E_Ass prf) =
  rewrite sym prf
  in rewrite t_update_shadow {x=x} {v2=n} {v1=v} {m=st}
  in E_Ass {n=n} Refl

p5_p6_equiv : HCEquiv Himp.p5 Himp.p6
p5_p6_equiv st st' = (forward st st', backward st st')
where forward : (st, st' : State) ->
                (Himp.p5 / st \\ st') -> (Himp.p6 / st \\ st')
      forward st st' rel = case rel of
        E_WhileEnd prf =>
          let st_X_eq_1 = fst (nat_beq_iff (st X) 1)
                              (trans (sym (notInvolutive (st X == 1)))
                                     (cong {f=Bool.not} prf))
              st_prf = replace {P=\v => t_update X v st = st}
                               st_X_eq_1 (t_update_same {m=st} {x=X})
          in replace {P=\x => HCEval (HCAss X 1) st x}
                     st_prf (Himp.E_Ass Refl)
        E_WhileLoop {st1 = (t_update Expr.X n st)} _ (E_Havoc n) next =>
          overwriting_write $ forward (t_update X n st) st' next
      backward : (st, st' : State) ->
                 (Himp.p6 / st \\ st') -> (Himp.p5 / st \\ st')
      backward st st' rel with (st X) proof st_X_prf
        backward st st' rel | Z = case rel of
          E_Ass prf => let pf = cong {f=Bool.not . (==1)} $ sym st_X_prf
                       in rewrite sym prf
                       in E_WhileLoop pf (E_Havoc 1) (E_WhileEnd Refl)
        backward st st' rel | S Z = case rel of
          E_Ass prf => let pf = cong {f=Bool.not . (==1)} $ sym st_X_prf
                       in rewrite sym prf
                       in rewrite st_X_prf
                       in rewrite t_update_same {m=st} {x=X}
                       in rewrite sym st_X_prf
                       in E_WhileEnd pf
        backward st st' rel | S (S k) = case rel of
          E_Ass prf => let pf = cong {f=Bool.not . (== 1)} $ sym st_X_prf
                       in rewrite sym prf
                       in E_WhileLoop pf (E_Havoc 1) (E_WhileEnd Refl)

HoareTriple : (p : Assertion) -> (c : HCom) -> (q : Assertion) -> Type
HoareTriple p c q = (st, st' : State) -> (c / st \\ st') -> p st -> q st'

HavocPre : (x : Id) -> (q : Assertion) -> Assertion
HavocPre x q = \st => (n : Nat) -> q (t_update x n st)

hoare_havoc : (q : Assertion) -> (x : Id) ->
              HoareTriple (HavocPre x q) (HAVOC x) q
hoare_havoc q x st _ (E_Havoc n) p_st = p_st n

IsWP : (p : Assertion) -> (c : HCom) -> (q : Assertion) -> Type
IsWP p c q = ( HoareTriple p c q
             , (p' : Assertion) -> HoareTriple p' c q -> p' ->> p )

hoare_havoc_weakest : IsWP (HavocPre x q) (HAVOC x) q
hoare_havoc_weakest {x} {q} = (hoare_havoc q x, imp)
where imp : (p' : Assertion) -> HoareTriple p' (HAVOC x) q -> p' ->> HavocPre x q
      imp p' ht st p'_st n = ht st _ (E_Havoc n) p'_st


text:
data PosNat : type
mkPosNat : (S k:Nat) -> PosNat

max_stars_repo_name: algeboy/FormalAlgebra

max_issues_repo_name: algeboy/FormalAlgebra

max_forks_repo_name: algeboy/FormalAlgebra


text:
module Main

import System

countdown : (secs : Nat) -> IO ()
countdown Z = putStrLn "Lift off!"
countdown (S secs) = do putStrLn (show (S secs))
                        usleep 1000000
                        countdown secs

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
module Foo

main : IO ()
main = printLn "Foo"


text:
module WebAssembly.Validation

import public WebAssembly.Validation.Conventions
import public WebAssembly.Validation.Types
import public WebAssembly.Validation.Instructions
import public WebAssembly.Validation.Modules

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Elab.Elaboration

import Elab.Common
import Typing.TypeChecking
import Typing.Util

-- 8YYYY 8o  0 oYYYo 0   0 8YYYo 8YYYY      _YYY_ oYYYo    0   0  o8o  0    Y8Y 8888_
-- 8___  8Yo 8 %___  0   0 8___P 8___  ____ 0   0 %___     0   0 8   8 0     0  0   0
-- 8"""  8 Yo8 `"""p 0   0 8""Yo 8"""  """" 0   0 `"""p    "o o" 8YYY8 0     0  0   0
-- 8oooo 0   8 YoooY "ooo" 0   0 8oooo      "ooo" YoooY     "8"  0   0 8ooo o8o 8oooY

ensureOpenSettingsAreValid : List OpenSettings -> Elaborator ()
ensureOpenSettingsAreValid oss = for_ oss ensure
where
	ensureModuleExists : String -> Elaborator ()
	ensureModuleExists m = do
		ms <- moduleNames
		unless (m `elem` ms)
			$ throw $ "The module " ++ m ++ " is not a known module."

	openAsIsValid : Maybe String -> Elaborator ()
	openAsIsValid Nothing = pure ()
	openAsIsValid (Just m') = do
		ms <- moduleNames
		unless (not (m' `elem` ms))
			$ throw $ "The module name " ++ m' ++ " is already in use."

	hidingUsingIsValid : String -> Maybe HidingUsing -> Elaborator ()
	hidingUsingIsValid _ Nothing = pure ()
	hidingUsingIsValid m (Just hu') = do
		defs <- definitions
		sig <- signature
		let ns = nub (case hu' of { Hiding ns' => ns' ; Using ns' => ns' })
		let known = nub ([ n | ((_,n),_,_) <- toList defs ] ++ [ n | ((_,n),_) <- toList sig ])
		let missing = ns \\ known
		unless (isNil missing)
			$ throw $ "The module " ++ m ++ " does not declare these symbols: "
							++ unwords missing

	showLR : String \/ FullName -> String
	showLR (Left n0) = n0
	showLR (Right (m0,n0)) = m0 ++ "." ++ n0

	renamingIsValid : String -> Maybe String -> Maybe HidingUsing -> List FullName -> Elaborator ()
	renamingIsValid m a hu r = do
		defs <- definitions
		sig <- signature
		let ns = nub [ n | (n,_) <- r ]
		let known = nub ([ n | ((m',n),_,_) <- toList defs, m' == m ]
					++ [ n | ((m',n),_) <- toList sig, m' == m ])
		let missing = ns \\ known
		unless (isNil missing) $ throw $ "The module " ++ m ++ " does not declare these symbols: "
			++ unwords ns
		let knownBeingUsed = case hu of
			Nothing => known
			Just (Using used) => used
			Just (Hiding hidden) => known \\ hidden
		let missingUsed = ns \\ knownBeingUsed
		unless (isNil missingUsed)
			$ throw $ "The following symbols are not being opened: " ++ unwords missingUsed
		let ns' = [ n' | (_,n') <- r ]
		let preserved = known \\ ns
		let overlappingNames = [ x | (x :: xs) <- groupBy (==) (sort (ns' ++ preserved)), length xs /= 0 ]
		unless (isNil overlappingNames)
			$ throw $ "These symbols will be overlapping when the module " ++ m
				++ " is opened: " ++ unwords overlappingNames
		als <- aliases
		let combine = the (String -> String \/ FullName) $ case a of
			Nothing => Left
			Just m' => \n' => Right (m', n')
		let mns' = nub [ combine n' | (_,n') <- r ]
		let knownAls = nub [ al | (al,_) <- als ]
		let overlap = intersect mns' knownAls

		unless (isNil overlap) $ throw $ "These symbols are already in scope: "
			++ unwords (map showLR overlap)

	ensure : OpenSettings -> Elaborator ()
	ensure (NewOpenSettings m a hu r) = do
		ensureModuleExists m
		openAsIsValid a
		hidingUsingIsValid m hu
		renamingIsValid m a hu r

-- 8o  0 8YYYY 0     0  o8o  0    Y8Y  o8o  oYYYo 8YYYY oYYYo
-- 8Yo 8 8___  0  0  0 8   8 0     0  8   8 %___  8___  %___
-- 8 Yo8 8"""  8 _8_ 8 8YYY8 0     0  8YYY8 `"""p 8"""  `"""p
-- 0   8 8oooo "8* *8" 0   0 8ooo o8o 0   0 YoooY 8oooo YoooY

newAliases : Signature Term -> Definitions -> List OpenSettings -> ModuleAliases
newAliases _ _ [] = []
newAliases sig defs (os::oss) = do
	let als  = newAliasesFromSettings os
	let als' = newAliases sig defs oss
	als' ++ als
where
	used : Maybe HidingUsing -> List FullName -> List FullName
	used Nothing            = id
	used (Just (Hiding ns)) = filter (\(_,n) => not (n `elem` ns))
	used (Just (Using ns))  = filter (\(_,n) => (n `elem` ns))

	renamed : List FullName -> List FullName -> List (String >< FullName)
	renamed r mns = [ (maybe n id (lookup n r), (m,n)) | (m,n) <- mns ]

	ased : Maybe String -> List (String >< FullName) ->
		List ((String \/ FullName) >< FullName)
	ased Nothing   ns = [ (Left x, (m,n)) | (x,(m,n)) <- ns ]
	ased (Just m') ns = [ (Right (m',x), (m,n)) | (x,(m,n)) <- ns ]

	newAliasesFromSettings : OpenSettings -> ModuleAliases
	newAliasesFromSettings (NewOpenSettings m a hu r) = do
		let openedSymbols = [ (m',c) | ((m',c),_) <- toList sig, m' == m ]
							++ [ (m',x) | ((m',x),_,_) <- toList defs, m' == m ]
		let usedSymbols = used hu openedSymbols
		let renamedSymbols = renamed r usedSymbols
		ased a renamedSymbols

extendAliases : List OpenSettings -> Elaborator a -> Elaborator a
extendAliases settings tc = do
	ensureOpenSettingsAreValid settings
	als <- aliases
	sig <- signature
	defs <- definitions
	let newAls = newAliases sig defs settings ++ als
	putAliases newAls
	x <- tc
	putAliases als
	pure x

-- 8888. 0   0 Y8Y 0    8888_ 0     o8o  8_   _8 8888. 8888_  o8o
-- 8___Y 0   0  0  0    0   0 0    8   8 8"o_o"8 8___Y 0   0 8   8
-- 8"""o 0   0  0  0    0   0 0    8YYY8 0  8  0 8"""o 0   0 8YYY8
-- 8ooo" "ooo" o8o 8ooo 8oooY 8ooo 0   0 0     0 8ooo" 8oooY 0   0

buildLambda : (List Term -> Term) -> List Plict -> Term
buildLambda f [] = f []
buildLambda f (plic :: plics) = Lam plic $
	NewScope ["_" ++ show (length plics)] $ \[x] => buildLambda (f . (x ::)) plics

-- 8YYYY 0     o8o  8888. YY8YY 8YYYY 8YYYo 8_   _8 8888_ 8YYYY  oYYo 0
-- 8___  0    8   8 8___Y   0   8___  8___P 8"o_o"8 0   0 8___  0   " 0
-- 8"""  0    8YYY8 8"""o   0   8"""  8""Yo 0  8  0 0   0 8"""  0   , 0
-- 8oooo 8ooo 0   0 8ooo"   0   8oooo 0   0 0     0 8oooY 8oooo  YooY 8ooo

export elabTermDecl : TermDeclaration -> Elaborator ()

--         oYYYo Y8Y 8_   _8 8YYYo 0    8YYYY
-- ____    %___   0  8"o_o"8 8___P 0    8___
-- """"    `"""p  0  0  8  0 8"""  0    8"""
--         YoooY o8o 0     0 0     8ooo 8oooo

elabTermDecl (SimpleTermDef n ty def) = do
	when' (typeInDefinitions n) $ throw ("Term already defined: " ++ n)
	ty' <- liftTC (check ty Star)
	m <- moduleName
	addAlias n
	def' <- liftTC (extendDefinitions (insert (m,n) (def,ty') empty) (check def ty'))
	addDeclaration n def' ty'

--         8YYYo  o8o  YY8YY YY8YY 8YYYY 8YYYo 8o  0
-- ____    8___P 8   8   0     0   8___  8___P 8Yo 8
-- """"    8"""  8YYY8   0     0   8"""  8""Yo 8 Yo8
--         0     0   0   0     0   8oooo 0   0 0   8

elabTermDecl decl@(PatternTermDef n ty preclauses) = go n ty preclauses
where
	isVarPat : Pattern -> Bool
	isVarPat (VarPat _) = True
	isVarPat _ = False

	truePlicities : List Plict -> Term -> Maybe (List (Plict \/ Plict))
	truePlicities [] _ = Just []
	truePlicities (Expl::plics) (Pi Expl _ sc) = do
		rest <- truePlicities plics (descope (Var . Name) sc)
		pure $ Right Expl :: rest
	truePlicities (Expl::plics) (Pi Impl _ sc) = do
		rest <- truePlicities (Expl :: plics) (descope (Var . Name) sc)
		pure $ Left Impl :: rest
	truePlicities (Impl :: _) (Pi Expl _ _) = Nothing
	truePlicities (Impl :: plics) (Pi Impl _ sc) = do
		rest <- truePlicities plics (descope (Var . Name) sc)
		pure $ Right Impl :: rest

	motiveAux : Int -> Term -> CaseMotive
	motiveAux 0 t = CaseMotiveNil t
	motiveAux i (Pi _ a (NewScope ns b)) = CaseMotiveCons a $ NewScope ns (motiveAux (i - 1) . b)

	truePatterns : List (Plict \/ Plict) -> List Pattern -> List Pattern
	truePatterns [] [] = []
	truePatterns (Right _ :: plics) (p :: ps) = p :: truePatterns plics ps
	truePatterns (Left _ :: plics) ps = MakeMeta :: truePatterns plics ps

	go : String -> Term -> (List ClauseDeclT) -> Elaborator ()
	go n ty [] = throw "Cannot create an empty let-where definition."
	go n ty [(plics,(ps,xs,b))] with (all isVarPat ps)
		| True = elabTermDecl $ SimpleTermDef n ty (helperFold (uncurry lamHelper) (zip plics xs) b)
	go n ty preclauses@((_,(ps0,_,_)) :: _) = do
		let lps0 = length ps0
		unless (all (\(_,(ps,_,_)) => length ps == lps0) preclauses)
			$ throw "Mismatching number of patterns in different clauses of a pattern matching function."
		let (plics :: plicss) = map fst preclauses
		unless (all (plics ==) plicss)
			$ throw "Mismatching plicities in different clauses of a pattern matching function"
		case truePlicities plics ty of
			Nothing => throw $ "Cannot build a case expression motive from the type " ++ show ty
			Just truePlics => do
				let mot = motiveAux (cast $ length truePlics) ty
				let clauses = [ clauseHelper (truePatterns truePlics ps) xs b | (_,(ps,xs,b)) <- preclauses ]
				let plicsForLambdaAux = map (either id id) truePlics
				elabTermDecl $ SimpleTermDef n ty $
					buildLambda (\as => Case as mot clauses) plicsForLambdaAux

--         _YYY_ 8YYYo 8YYYY 8o  0
-- ____    0   0 8___P 8___  8Yo 8
-- """"    0   0 8"""  8"""  8 Yo8
--         "ooo" 0     8oooo 0   8

elabTermDecl (OpenTermDef n args ty) = do
	when' (typeInDefinitions n) $ throw ("Term already defined: " ++ n)
	let (ty,plics,mot) = convertArgs args
	ty' <- liftTC (checkify ty Star)
	mot' <- liftTC (checkifyCaseMotive mot)
	m <- moduleName
	fs <- openFunctions
	case lookup (m,n) fs of
		Nothing => do
				putOpenFunctions $ insert (m,n) (ty',plics,mot',[]) $ fs
				let initialDef = buildLambda (\xs => Case xs mot' []) plics
				addAlias n
				initialDef' <- liftTC $
					extendDefinitions (insert (m,n) (initialDef,ty') empty) (check initialDef ty')
				addDeclaration n initialDef' ty
		Just _ => throw $ "The open function " ++ show (DottedVar m n) ++ " has already been declared."
where
	convertArgs : List DeclArg -> (Term >< List Plict >< CaseMotive)
	convertArgs [] = (ty, [], CaseMotiveNil ty)
	convertArgs (NewDeclArg plic x t :: as) = do
		let (b, plics, mot) = convertArgs as
		(piHelper plic x t b, plic :: plics, consMotiveHelper x t mot)

--         Y8Y 8o  0 oYYYo YY8YY 8o  0  o8o   oYYo 8YYYY
-- ____     0  8Yo 8 %___    0   8Yo 8 8   8 0   " 8___
-- """"     0  8 Yo8 `"""p   0   8 Yo8 8YYY8 0   , 8"""
--         o8o 0   8 YoooY   0   0   8 0   0  YooY 8oooo

elabTermDecl (InstTermDef n preclauses) = do
	let aliasedName = the Term $ case n of
		Left n0 => Var (Name n0)
		Right (m0,n0) => DottedVar m0 n0
	(m',n') <- liftTC $ unalias n
	fs <- openFunctions
	Just (ty,plics,mot,clauses) <- pure $ lookup (m',n') fs
		| _ => throw ("No open function named " ++ show aliasedName ++ " has been declared.")

	clauses' <- Traversable.for preclauses $ \(plics',(ps,xs,b)) => do
		case insertMetas plics plics' of
			Nothing => throw $ "Instance for open function " ++ show aliasedName ++
				" has invalid argument plicities."
			Just bs => pure $ clauseHelper (truePatterns bs ps) xs b
	let newClauses = clauses ++ clauses'
	let newDef = buildLambda (\xs => Case xs mot newClauses) plics
	let newOpenFunctions = insert (m',n') (ty,plics,mot,newClauses) $
		fromList $ filter (\(p,_) => p /= (m',n')) $ toList fs
	newDef' <- liftTC $ extendDefinitions (insert (m',n') (newDef, ty) empty) (check newDef ty)
	putOpenFunctions newOpenFunctions
	defs <- definitions
	putDefinitions $ insert (m', n') (newDef', ty) $
		fromList $ filter (\(p,_,_) => p /= (m',n')) (toList defs)
where
	insertMetas : List Plict -> List Plict -> Maybe (List Bool)
	insertMetas [] [] = Just []
	insertMetas (Expl :: args) (Expl :: plics) = do
		rest <- insertMetas args plics
		pure $ False :: rest
	insertMetas (Expl :: _) (Impl :: _) = Nothing
	insertMetas (Impl :: args) (Expl :: plics) = do
		rest <- insertMetas args plics
		pure $ True :: rest
	insertMetas (Impl :: args) (Impl :: plics) = do
		rest <- insertMetas args plics
		pure $ False :: rest
	insertMetas _ _ = Nothing

	truePatterns : List Bool -> List Pattern -> List Pattern
	truePatterns [] [] = []
	truePatterns (False :: plics) (p :: ps) = p :: truePatterns plics ps
	truePatterns (True :: plics) ps = MakeMeta :: truePatterns plics ps

--          oYYo 0    _YYY_ oYYYo 8YYYY
-- ____    0   " 0    0   0 %___  8___
-- """"    0   , 0    0   0 `"""p 8"""
--          YooY 8ooo "ooo" YoooY 8oooo

elabTermDecl (CloseTermDef n) = do
	let aliasedName = the Term $ case n of
		Left n0 => Var (Name n0)
		Right (m0,n0) => DottedVar m0 n0
	(m',n') <- liftTC $ unalias n
	fs <- openFunctions
	Just (ty,plics,mot,clauses) <- pure $ lookup (m',n') fs
		| _ => throw ("Open function " ++ show aliasedName ++ " is not defined.")
	putOpenFunctions $ fromList $ filter (\(p,_) => p /= (m',n')) $ toList fs

-- 0   0  o8o  0    Y8Y 8888_  oYYo _YYY_ 8o  0 oYYYo Y8Y  oYYo
-- 0   0 8   8 0     0  0   0 0   " 0   0 8Yo 8 %___   0  0  __
-- "o o" 8YYY8 0     0  0   0 0   , 0   0 8 Yo8 `"""p  0  0  "8
--  "8"  0   0 8ooo o8o 8oooY  YooY "ooo" 0   8 YoooY o8o  YooY

validConSig : Constructor -> Constructor -> ConSig Term -> Elaborator ()
validConSig tycon c (ConSigNil (Con tc _)) = unless (tc == tycon) $
	throw $ "The constructor " ++ show c ++ " should constructor a value of the type " ++ show tycon
		++ " but instead produces a " ++ show tc
validConSig tycon c (ConSigNil a) = throw $
	"The constructor " ++ show c ++ " should constructor a value of the type " ++ show tycon
			++ " but instead produces " ++ show a
validConSig tycon c (ConSigCons _ _ sc) = validConSig tycon c (descope (Var . Name) sc)

-- 8YYYY 0     o8o  8888.  o8o  0    YY8YY
-- 8___  0    8   8 8___Y 8   8 0      0
-- 8"""  0    8YYY8 8"""o 8YYY8 0      0
-- 8oooo 8ooo 0   0 8ooo" 0   0 8ooo   0

elabAlt : String -> String -> ConSig Term -> Elaborator ()
elabAlt tycon c consig = do
	validConSig (BareCon tycon) (BareCon c) consig
	when' (typeInSignature (BareCon c))
		$ throw ("Constructor already declared: " ++ c)
	addAlias c
	consig' <- liftTC (checkifyConSig consig)
	addConstructor c consig'

-- 8YYYY 0     o8o  8888. Y8Y 8o  0 oYYYo YY8YY  o8o  8o  0  oYYo 8YYYY  o8o  0    YY8YY
-- 8___  0    8   8 8___Y  0  8Yo 8 %___    0   8   8 8Yo 8 0   " 8___  8   8 0      0
-- 8"""  0    8YYY8 8"""o  0  8 Yo8 `"""p   0   8YYY8 8 Yo8 0   , 8"""  8YYY8 0      0
-- 8oooo 8ooo 0   0 8ooo" o8o 0   8 YoooY   0   0   0 0   8  YooY 8oooo 0   0 8ooo   0

elabInstanceAlt : String -> Constructor -> String -> ConSig Term -> Elaborator ()
elabInstanceAlt m localTycon c consig = do
	validConSig localTycon (BareCon c) consig
	sig <- signature
	case lookup (m,c) sig of
		Just _ => throw ("Constructor already declared: " ++ c)
		Nothing => do
			addAliasFor (Left c) (m,c)
			consig' <- liftTC (checkifyConSig consig)
			addConstructorToModule m c consig'

-- 8YYYY 0     o8o  8888. YY8YY 0   0 8YYYo 8YYYY 8888_ 8YYYY  oYYo 0
-- 8___  0    8   8 8___Y   0   "o o" 8___P 8___  0   0 8___  0   " 0
-- 8"""  0    8YYY8 8"""o   0     0   8"""  8"""  0   0 8"""  0   , 0
-- 8oooo 8ooo 0   0 8ooo"   0     0   0     8oooo 8oooY 8oooo  YooY 8ooo

export elabTypeDecl : TypeDeclaration -> Elaborator ()

--         Y8Y 8o  0 8888_ 0   0  oYYo YY8YY Y8Y 0   0 8YYYY
-- ____     0  8Yo 8 0   0 0   0 0   "   0    0  0   0 8___
-- """"     0  8 Yo8 0   0 0   0 0   ,   0    0  "o o" 8"""
--         o8o 0   8 8oooY "ooo"  YooY   0   o8o  "8"  8oooo

elabTypeDecl (Inductive tycon tyconargs alts) = do
	let tyconSig = conSigHelper tyconargs Star
	when' (typeInSignature (BareCon tycon))
		$ throw ("Type constructor already declared: " ++ tycon)
	addAlias tycon
	tyconSig' <- liftTC (checkifyConSig tyconSig)
	addConstructor tycon tyconSig'
	traverse_ (uncurry (elabAlt tycon)) alts

--         8888_  o8o  YY8YY  o8o  8YYYY  o8o  8_   _8 Y8Y 0    0   0
-- ____    0   0 8   8   0   8   8 8___  8   8 8"o_o"8  0  0    "o o"
-- """"    0   0 8YYY8   0   8YYY8 8"""  8YYY8 0  8  0  0  0      0
--         8oooY 0   0   0   0   0 0     0   0 0     0 o8o 8ooo   0

elabTypeDecl (DataFamily tycon tyconargs) = do
	let tyconSig = conSigHelper tyconargs Star
	when' (typeInSignature (BareCon tycon))
		$ throw ("Type constructor already declared: " ++ tycon)
	addAlias tycon
	tyconSig' <- liftTC (checkifyConSig tyconSig)
	addConstructor tycon tyconSig'
	m <- moduleName
	od <- openData
	putOpenData ((m,tycon) :: od)

--         8888_  o8o  YY8YY  o8o  Y8Y 8o  0 oYYYo YY8YY  o8o  8o  0  oYYo 8YYYY
-- ____    0   0 8   8   0   8   8  0  8Yo 8 %___    0   8   8 8Yo 8 0   " 8___
-- """"    0   0 8YYY8   0   8YYY8  0  8 Yo8 `"""p   0   8YYY8 8 Yo8 0   , 8"""
--         8oooY 0   0   0   0   0 o8o 0   8 YoooY   0   0   0 0   8  YooY 8oooo

elabTypeDecl (DataInstance tycon alts) = do
	let aliasedName = case tycon of
						BareCon c => Left c
						DottedCon m c => Right (m,c)
	(m',c') <- liftTC $ unalias aliasedName
	od <- openData
	unless ((m',c') `elem` od)
		$ throw $ "The constructor " ++ show tycon ++ " is not an open data type."
	traverse_ (uncurry (elabInstanceAlt m' tycon)) alts

-- 8YYYY 0     o8o  8888. 8_   _8 _YYY_ 8888_ 0   0 0    8YYYY
-- 8___  0    8   8 8___Y 8"o_o"8 0   0 0   0 0   0 0    8___
-- 8"""  0    8YYY8 8"""o 0  8  0 0   0 0   0 0   0 0    8"""
-- 8oooo 8ooo 0   0 8ooo" 0     0 "ooo" 8oooY "ooo" 8ooo 8oooo

export elabModule : Module -> Elaborator ()
elabModule (NewModule m settings stmts0) = do
	addModuleName m
	putModuleName m
	ensureOpenSettingsAreValid settings
	als <- aliases
	sig <- signature
	defs <- definitions
	let newAls = newAliases sig defs settings ++ als
	putAliases newAls
	go stmts0
	putAliases als
where
	go : List Statement -> Elaborator ()
	go [] = pure ()
	go (TyDecl td :: stmts) = do
		elabTypeDecl td
		go stmts
	go (TmDecl td :: stmts) = do
		elabTermDecl td
		go stmts

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
||| FFI binding to the low-Level C Sockets bindings for Idris.
|||
||| Modified (C) The Idris Community, 2020
module Network.FFI

import Network.Socket.Data

-- From sys/socket.h

%foreign "C:close,libidris2_support"
export
prim__socket_close : (sockdes : SocketDescriptor) -> PrimIO Int

%foreign "C:listen,libc 6"
export
prim__socket_listen : (sockfd : SocketDescriptor) -> (backlog : Int) -> PrimIO Int

-- From idris_net.h

%foreign "C:idrnet_socket,libidris2_support"
export
prim__idrnet_socket : (domain, type, protocol : Int) -> PrimIO Int

%foreign "C:idrnet_bind,libidris2_support"
export
prim__idrnet_bind : (sockfd : SocketDescriptor) -> (family, socket_type : Int) ->
                    (host : String) -> (port : Port) -> PrimIO Int

%foreign "C:idrnet_connect,libidris2_support"
export
prim__idrnet_connect : (sockfd : SocketDescriptor) -> (family, socket_type : Int) ->
                       (host : String) -> (port : Port) -> PrimIO Int

%foreign "C:idrnet_sockaddr_family,libidris2_support"
export
prim__idrnet_sockaddr_family : (sockaddr : AnyPtr) -> PrimIO Int

%foreign "C:idrnet_sockaddr_ipv4,libidris2_support"
export
prim__idrnet_sockaddr_ipv4 : (sockaddr : AnyPtr) -> PrimIO String

%foreign "C:idrnet_sockaddr_ipv4_port,libidris2_support"
export
prim__idrnet_sockaddr_ipv4_port : (sockaddr : AnyPtr) -> PrimIO Int

%foreign "C:idrnet_sockaddr_port,libidris2_support"
export
prim__idrnet_sockaddr_port : (sockfd : SocketDescriptor) -> PrimIO Int

%foreign "C:idrnet_create_sockaddr,libidris2_support"
export
prim__idrnet_create_sockaddr : PrimIO AnyPtr

%foreign "C:idrnet_accept,libidris2_support"
export
prim__idrnet_accept : (sockfd : SocketDescriptor) -> (sockaddr : AnyPtr) -> PrimIO Int

%foreign "C:idrnet_send,libidris2_support"
export
prim__idrnet_send : (sockfd : SocketDescriptor) -> (dataString : String) -> PrimIO Int

%foreign "C:idrnet_send_buf,libidris2_support"
export
prim__idrnet_send_buf : (sockfd : SocketDescriptor) -> (dataBuffer : AnyPtr) -> (len : Int) -> PrimIO Int

%foreign "C:idrnet_recv,libidris2_support"
export
prim__idrnet_recv : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr

%foreign "C:idrnet_recv_buf,libidris2_support"
export
prim__idrnet_recv_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO Int

%foreign "C:idrnet_sendto,libidris2_support"
export
prim__idrnet_sendto : (sockfd : SocketDescriptor) -> (dataString,host : String) ->
                      (port : Port) -> (family : Int) -> PrimIO Int

%foreign "C:idrnet_sendto_buf,libidris2_support"
export
prim__idrnet_sendto_buf : (sockfd : SocketDescriptor) -> (dataBuf : AnyPtr) ->
                          (buf_len : Int) -> (host : String) -> (port : Port) ->
                          (family : Int) -> PrimIO Int

%foreign "C:idrnet_recvfrom,libidris2_support"
export
prim__idrnet_recvfrom : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr

%foreign "C:idrnet_recvfrom_buf,libidris2_support"
export
prim__idrnet_recvfrom_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO AnyPtr

%foreign "C:idrnet_get_recv_res,libidris2_support"
export
prim__idrnet_get_recv_res : (res_struct : AnyPtr) -> PrimIO Int

%foreign "C:idrnet_get_recv_payload,libidris2_support"
export
prim__idrnet_get_recv_payload : (res_struct : AnyPtr) -> PrimIO String

%foreign "C:idrnet_free_recv_struct,libidris2_support"
export
prim__idrnet_free_recv_struct : (res_struct : AnyPtr) -> PrimIO ()

%foreign "C:idrnet_get_recvfrom_res,libidris2_support"
export
prim__idrnet_get_recvfrom_res : (res_struct : AnyPtr) -> PrimIO Int

%foreign "C:idrnet_get_recvfrom_payload,libidris2_support"
export
prim__idrnet_get_recvfrom_payload : (res_struct : AnyPtr) -> PrimIO String

%foreign "C:idrnet_get_recvfrom_sockaddr,libidris2_support"
export
prim__idrnet_get_recvfrom_sockaddr : (res_struct : AnyPtr) -> PrimIO AnyPtr

%foreign "C:idrnet_free_recvfrom_struct,libidris2_support"
export
prim__idrnet_free_recvfrom_struct : (res_struct : AnyPtr) -> PrimIO ()

%foreign "C:idrnet_geteagain,libidris2_support"
export
prim__idrnet_geteagain : PrimIO Int

%foreign "C:idrnet_errno,libidris2_support"
export
prim__idrnet_errno : PrimIO Int

%foreign "C:idrnet_malloc,libidris2_support"
export
prim__idrnet_malloc : (size : Int) -> PrimIO AnyPtr

%foreign "C:idrnet_free,libidris2_support"
export
prim__idrnet_free : (ptr : AnyPtr) -> PrimIO ()

%foreign "C:idrnet_peek,libidris2_support"
export
prim__idrnet_peek : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) -> PrimIO {-Unsigned-} Int

%foreign "C:idrnet_poke,libidris2_support"
export
prim__idrnet_poke : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) ->
                    (val : Int {- should be Char? -}) -> PrimIO ()


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Lens
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Control.Lens.Maths
import Control.Lens.Types
import Control.Lens.Setter

%default total

infixr 4 +~
public export
(+~) : Num a => Setter s t a a -> a -> s -> t
l +~ n = over l (+ n)

infixr 4 *~
public export
(*~) : Num a => Setter s t a a -> a -> s -> t
l *~ n = over l (* n)

infixr 4 -~
public export
(-~) : (Neg a, Num a) => Setter s t a a -> a -> s -> t
l -~ n = over l (\x => x - n)

infixr 4 //~
public export
(//~) : Fractional a => Setter s t a a -> a -> s -> t
l //~ n = over l (/ n)

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


text:
module ArithExp.AST
%default total

||| Desugaring levels for the language.
data Sugar = Core | Surface

||| ADT for the language itself + syntactic sugar
|||
||| This is all done in "Curry style". To do this in Church style, the type of
||| AST could be `AST : Sugar -> SimpleType -> Type` where each variant has the
||| type per the typing rules in `Types.idr`. This could make some of the type
||| soundness proof easier to write.
data AST : Sugar -> Type where
  Zero   : AST a
  Tru    : AST a
  Fals   : AST a
  IF     : AST a -> AST a -> AST a -> AST a
  Succ   : AST a -> AST a
  Pred   : AST a -> AST a
  IsZero : AST a -> AST a
  Num    : Nat   -> AST Surface
  AND    : AST a -> AST a -> AST Surface
  OR     : AST a -> AST a -> AST Surface

ArithBool : Type
ArithBool = AST Core

||| desguar away 'Num' 'And' and 'OR', could add extra operators too!
desugar : AST a -> AST Core
desugar Zero        = Zero
desugar Tru         = Tru
desugar Fals        = Fals
desugar (IF x y z)  = IF (desugar x) (desugar y) (desugar z)
desugar (Succ x)    = Succ (desugar x)
desugar (Pred x)    = Pred (desugar x)
desugar (IsZero x)  = IsZero (desugar x)
desugar (AND a b)   = IF (desugar a) (desugar b) Fals
desugar (OR a b)    = IF (desugar a) Tru (desugar b)
desugar (Num r)     = unroll r
  where unroll : Nat -> AST Core
        unroll Z     = Zero
        unroll (S k) = Succ (unroll k)

||| Type-level predicate describing fully-reduced numeric values
data NV : ArithBool -> Type where
  NvZero : NV Zero
  NvSucc : NV n -> NV (Succ n)

max_stars_repo_name: ezrosent/TAPL-idris

max_issues_repo_name: ezrosent/TAPL-idris

max_forks_repo_name: ezrosent/TAPL-idris


text:
module Libgit.Clone

import Prelude
import Control.Monad.Managed
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Syntax
import Control.Monad.Trans
import System.FFI

import Libgit.FFI
import Libgit.Git
import Libgit.Types

||| A set of options that dictate how a repository should be cloned from a
||| remote.
public export
record CloneOpts where
  constructor MkCloneOpts
  ||| Make a bare Git repository. When enabled, the localPath provided to clone
  ||| will contain the administrative files usually contained within .git and
  ||| files won't actually be checked out.
  bare : Bool
  ||| Which branch to checkout after cloning.
  checkoutBranch : String

||| Sensible defaults for CloneOpts.
||| + bare = False
||| + checkoutBranch = master
export
defaultOpts : CloneOpts
defaultOpts = MkCloneOpts False "master"

applyOpts : CloneOpts -> AnyPtr -> IO ()
applyOpts cloneOpts cCloneOpts = do
  let bare' = cBool cloneOpts.bare
  primIO $ prim_apply_clone_options cCloneOpts cloneOpts.checkoutBranch bare'

withCloneOptions : CloneOpts -> (GitResult AnyPtr -> IO a) -> IO a
withCloneOptions opts act = do
  optsPtr <- primIO prim_init_clone_options
  err <- primIO (prim_git_clone_init_options optsPtr git_clone_options_version)
  applyOpts opts optsPtr
  res <- act (toGitResult err optsPtr)
  primIO (prim_free optsPtr)
  pure res

cloneOptions : CloneOpts -> Managed (GitResult AnyPtr)
cloneOptions opts = managed (withCloneOptions opts)

withClonedRepository : (url : String)
                    -> (localPath : String)
                    -> (options : AnyPtr)
                    -> (GitResult GitRepository -> IO a)
                    -> IO a
withClonedRepository url localPath options act = do
  cresult <- primIO (prim_git_clone_repository url localPath options)
  repoResult <- getGitResult cresult
  result <- act (MkGitRepository <$> repoResult)
  case repoResult of
    Right ptr => pure result <* primIO (prim_git_repository_free ptr)
    _ => pure result

||| Accepts clone options, a Git remote URL, and a local path, and clones the
||| Git repository at that remote to the specified local path.
|||
||| Returns a Managed reference to a GitRepository object which can be used to
||| interact with the repository.
|||
||| @opts      A CloneOpts specifying additional details about how the
|||            repository should be cloned.
||| @url       A reference to the
||| @localPath The local path to clone the repository to.
export
clonedRepository : (opts : CloneOpts)
                -> (url : String)
                -> (localPath : String)
                -> Managed (GitResult GitRepository)
clonedRepository opts url localPath = do
  Right options <- cloneOptions opts
    | Left res => pure (Left res)
  managed (withClonedRepository url localPath options)

max_forks_repo_name: bigs/libgit-idris


text:
module SimpleLang

data Ty = TyInt | TyBool

interp : Ty -> Type
interp TyInt  = Int
interp TyBool = Bool

data Expr : Ty -> Type where
  CInt  : Int -> Expr TyInt
  CBool : Bool -> Expr TyBool
  Add   : Expr TyInt -> Expr TyInt -> Expr TyInt
  LT    : Expr TyInt -> Expr TyInt -> Expr TyBool

eval : Expr t -> interp t
eval (CInt x) = x
eval (CBool x) = x
eval (Add x y) = eval x + eval y
eval (LT x y) = eval x < eval y

max_stars_repo_name: tgrospic/dependently-typed-slides

max_issues_repo_name: tgrospic/dependently-typed-slides

max_forks_repo_name: tgrospic/dependently-typed-slides


text:
import Data.Either
import Data.List
import Data.Maybe
import Data.String

import System.File

data LowPoint = L Nat | N Nat

Show LowPoint where
  show (L k) = "L " ++ show k
  show (N k) = "N " ++ show k

get : LowPoint -> Nat
get (L k) = k
get (N k) = k

isLow : LowPoint -> Bool
isLow (L k) = True
isLow (N k) = False

parseLines : (String -> Maybe a) -> String -> List a
parseLines f s = catMaybes $ f <$> lines s

lowPointsRow : Nat -> List Nat -> List LowPoint
lowPointsRow n [] = []
lowPointsRow n (x :: []) = if x < n then [L x] else [N x]
lowPointsRow n (x :: (y :: xs)) = (if x < n && x < y then L x else N x) :: lowPointsRow x (y :: xs)

comp : Nat -> LowPoint -> LowPoint
comp p (L k) = if k < p then L k else N k
comp _ (N k) = N k

comp3 : Nat -> LowPoint -> Nat -> LowPoint
comp3 p (L k) n = if k < n && k < p then L k else N k
comp3 _ (N k) _ = N k

lowPointsCol : List Nat -> List (List LowPoint) -> List (List LowPoint)
lowPointsCol prev [] = []
lowPointsCol prev (row :: []) = [ (\(p, r) => comp p r) <$> zip prev row ]
lowPointsCol prev (row :: (next :: rows)) = ((\(p, r, n) => comp3 p r (get n)) <$> zip3 prev row next) :: lowPointsCol (get <$> row) (next :: rows)

run : String -> IO ()
run s = do let l = (\l => catMaybes $ parsePositive {a=Nat} . singleton <$> unpack l) <$> lines s
           let r = lowPointsCol (replicate 100 10) $ lowPointsRow 10 <$> l
           let s = sum $ S . get <$> (filter isLow $ (join r))
           putStrLn $ show $ s

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s


text:
module Exercise_5_2_10

import Ch05.LambdaCalculusWithArith

%default total

||| Terms representing a function converting primitive natural numbers
||| into Church numerals.
churchnat : Term
churchnat = fix . g where
  g : Term
  g = lambda 0
             (\f => lambda 1
                           (\n => IfThenElse (IsZero n)
                                             church_zero
                                             (scc . (f . (Pred n)))))

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module Lens.Uninhabited

import Lens
import Map

%default total

public export
Uninhabited (a = b) => Uninhabited (Boolean a = Boolean b) where
    uninhabited Refl @{ab} = uninhabited @{ab} Refl

public export
Uninhabited (Boolean a = Number b) where
    uninhabited Refl impossible

public export
Uninhabited (Boolean a = Text b) where
    uninhabited Refl impossible

public export
Uninhabited (a = b) => Uninhabited (Number a = Number b) where
    uninhabited Refl @{ab} = uninhabited @{ab} Refl

public export
Uninhabited (Number a = Boolean b) where
    uninhabited Refl impossible

public export
Uninhabited (Number a = Text b) where
    uninhabited Refl impossible

public export
Uninhabited (a = b) => Uninhabited (Text a = Text b) where
    uninhabited Refl @{ab} = uninhabited @{ab} Refl

public export
Uninhabited (Text a = Boolean b) where
    uninhabited Refl impossible

public export
Uninhabited (Text a = Number b) where
    uninhabited Refl impossible

public export
Uninhabited (KBoolean = KNumber) where
    uninhabited Refl impossible

public export
Uninhabited (KBoolean = KText) where
    uninhabited Refl impossible

public export
Uninhabited (KNumber = KBoolean) where
    uninhabited Refl impossible

public export
Uninhabited (KNumber = KText) where
    uninhabited Refl impossible

public export
Uninhabited (KText = KBoolean) where
    uninhabited Refl impossible

public export
Uninhabited (KText = KNumber) where
    uninhabited Refl impossible

public export
Uninhabited (Null = Primitive _) where
    uninhabited Refl impossible

public export
Uninhabited (Null = Array _) where
    uninhabited Refl impossible

public export
Uninhabited (Null = Object _) where
    uninhabited Refl impossible

public export
Uninhabited (Primitive _ = Null) where
    uninhabited Refl impossible

public export
Uninhabited (a = b) => Uninhabited (Primitive a = Primitive b) where
    uninhabited Refl @{ab} = uninhabited @{ab} Refl

public export
Uninhabited (Primitive _ = Array _) where
    uninhabited Refl impossible

public export
Uninhabited (Primitive _ = Object _) where
    uninhabited Refl impossible

public export
Uninhabited (Array _ = Null) where
    uninhabited Refl impossible

public export
Uninhabited (Array _ = Primitive _) where
    uninhabited Refl impossible

public export
Uninhabited (a = b) => Uninhabited (Array a = Array b) where
    uninhabited Refl @{ab} = uninhabited @{ab} Refl

public export
Uninhabited (Array _ = Object _) where
    uninhabited Refl impossible

public export
Uninhabited (Object _ = Null) where
    uninhabited Refl impossible

public export
Uninhabited (Object _ = Primitive _) where
    uninhabited Refl impossible

public export
Uninhabited (Object _ = Array _) where
    uninhabited Refl impossible

public export
Uninhabited (a = b) => Uninhabited (Object a = Object b) where
    uninhabited Refl @{ab} = uninhabited @{ab} Refl

public export
Uninhabited (SNull = SBoolean) where
    uninhabited Refl impossible

public export
Uninhabited (SNull = SNumber) where
    uninhabited Refl impossible

public export
Uninhabited (SNull = SText) where
    uninhabited Refl impossible

public export
Uninhabited (SNull = SArray _ _) where
    uninhabited Refl impossible

public export
Uninhabited (SNull = SObject _) where
    uninhabited Refl impossible

public export
Uninhabited (SBoolean = SNull) where
    uninhabited Refl impossible

public export
Uninhabited (SBoolean = SNumber) where
    uninhabited Refl impossible

public export
Uninhabited (SBoolean = SText) where
    uninhabited Refl impossible

public export
Uninhabited (SBoolean = SArray _ _) where
    uninhabited Refl impossible

public export
Uninhabited (SBoolean = SObject _) where
    uninhabited Refl impossible

public export
Uninhabited (SNumber = SNull) where
    uninhabited Refl impossible

public export
Uninhabited (SNumber = SBoolean) where
    uninhabited Refl impossible

public export
Uninhabited (SNumber = SText) where
    uninhabited Refl impossible

public export
Uninhabited (SNumber = SArray _ _) where
    uninhabited Refl impossible

public export
Uninhabited (SNumber = SObject _) where
    uninhabited Refl impossible

public export
Uninhabited (SText = SNull) where
    uninhabited Refl impossible

public export
Uninhabited (SText = SBoolean) where
    uninhabited Refl impossible

public export
Uninhabited (SText = SNumber) where
    uninhabited Refl impossible

public export
Uninhabited (SText = SArray _ _) where
    uninhabited Refl impossible

public export
Uninhabited (SText = SObject _) where
    uninhabited Refl impossible

public export
Uninhabited (SArray _ _ = SNull) where
    uninhabited Refl impossible

public export
Uninhabited (SArray _ _ = SBoolean) where
    uninhabited Refl impossible

public export
Uninhabited (SArray _ _ = SNumber) where
    uninhabited Refl impossible

public export
Uninhabited (SArray _ _ = SText) where
    uninhabited Refl impossible

public export
Uninhabited (a = b) => Uninhabited (SArray a _ = SArray b _) where
    uninhabited Refl @{ab} = uninhabited @{ab} Refl

public export
Uninhabited (a = b) => Uninhabited (SArray _ a = SArray _ b) where
    uninhabited Refl @{ab} = uninhabited @{ab} Refl

public export
Uninhabited (SArray _ _ = SObject _) where
    uninhabited Refl impossible

public export
Uninhabited (SObject _ = SNull) where
    uninhabited Refl impossible

public export
Uninhabited (SObject _ = SBoolean) where
    uninhabited Refl impossible

public export
Uninhabited (SObject _ = SNumber) where
    uninhabited Refl impossible

public export
Uninhabited (SObject _ = SText) where
    uninhabited Refl impossible

public export
Uninhabited (SObject _ = SArray _ _) where
    uninhabited Refl impossible

public export
Uninhabited (a = b) => Uninhabited (SObject a = SObject b) where
    uninhabited Refl @{ab} = uninhabited @{ab} Refl

max_stars_repo_name: Actyx/cambria

max_issues_repo_name: Actyx/cambria

max_forks_repo_name: Actyx/cambria


text:
module Effect.Gl

import Effects
import public Graphics.Util.Color
import public Graphics.Rendering.Gl.Types
import public Graphics.Rendering.Gl.Gl41
import public Graphics.Rendering.Gl

%access public export

data GlState : Type where
  GlOn : GlState

data Gl : Effect where
  Initialise : sig Gl () () (\v => GlState)
  WithGl : (GlState -> IO a) -> sig Gl a GlState (\w => GlState)
  Terminate : sig Gl () GlState (\_ => ())

instance Handler Gl IO where
  handle () Initialise  k = k () GlOn
  handle GlOn (WithGl f)  k = do r <- f GlOn; k r GlOn
  handle GlOn Terminate   k = k () ()

GL : Type -> EFFECT
GL res = MkEff res Gl

GL_ON : EFFECT
GL_ON = GL GlState

GL_OFF : EFFECT
GL_OFF = GL ()

startGl : { [GL_OFF] ==> [GL_ON] } Eff ()
startGl = call Initialise

stopGl : { [GL_ON] ==> [GL_OFF] } Eff ()
stopGl = call Terminate

clear' : Color -> List ClearBufferMask -> IO ()
clear' (RGBA r g b a) masks = do glClearColor r g b a
                                 traverse glClear masks
                                 pure ()

clear : Color -> List ClearBufferMask -> { [GL_ON] } Eff ()
clear color masks = call $ WithGl (\_ => clear' color masks)

max_stars_repo_name: xiphiness/gl-idris

max_issues_repo_name: xiphiness/gl-idris

max_forks_repo_name: xiphiness/gl-idris


text:
module Core.Context.Log

import Core.Context
import Core.Options
import Data.String

import Libraries.Data.StringMap

import System.Clock

%default covering

-- if this function is called, then logging must be enabled.
%inline
export
logString : String -> Nat -> String -> Core ()
logString "" n msg = coreLift $ putStrLn
    $ "LOG " ++ show n ++ ": " ++ msg
logString str n msg = coreLift $ putStrLn
    $ "LOG " ++ str ++ ":" ++ show n ++ ": " ++ msg

%inline
export
logString' : LogLevel -> String -> Core ()
logString' lvl =
  logString (fastAppend (intersperse "." (topics lvl)) ++ ":")
            (verbosity lvl)

export
logging' : {auto c : Ref Ctxt Defs} ->
           LogLevel -> Core Bool
logging' lvl = do
    opts <- getSession
    pure $ verbosity lvl == 0 || (logEnabled opts && keepLog lvl (logLevel opts))

export
unverifiedLogging : {auto c : Ref Ctxt Defs} ->
                    String -> Nat -> Core Bool
unverifiedLogging str Z = pure True
unverifiedLogging str n = do
    opts <- getSession
    pure $ logEnabled opts && keepLog (mkUnverifiedLogLevel str n) (logLevel opts)

%inline
export
logging : {auto c : Ref Ctxt Defs} ->
          (s : String) -> {auto 0 _ : KnownTopic s} ->
          Nat -> Core Bool
logging str n = unverifiedLogging str n

||| Log message with a term, translating back to human readable names first.
export
logTerm : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          (s : String) ->
          {auto 0 _ : KnownTopic s} ->
          Nat -> Lazy String -> Term vars -> Core ()
logTerm str n msg tm
    = when !(logging str n)
        $ do tm' <- toFullNames tm
             logString str n $ msg ++ ": " ++ show tm'

export
log' : {auto c : Ref Ctxt Defs} ->
       LogLevel -> Lazy String -> Core ()
log' lvl msg
    = when !(logging' lvl)
        $ logString' lvl msg

||| Log a message with the given log level. Use increasingly
||| high log level numbers for more granular logging.
export
log : {auto c : Ref Ctxt Defs} ->
      (s : String) ->
      {auto 0 _ : KnownTopic s} ->
      Nat -> Lazy String -> Core ()
log str n msg
    = when !(logging str n)
        $ logString str n msg

export
unverifiedLogC : {auto c : Ref Ctxt Defs} ->
                 (s : String) ->
                 Nat -> Core String -> Core ()
unverifiedLogC str n cmsg
    = when !(unverifiedLogging str n)
        $ do msg <- cmsg
             logString str n msg

%inline
export
logC : {auto c : Ref Ctxt Defs} ->
       (s : String) ->
       {auto 0 _ : KnownTopic s} ->
       Nat -> Core String -> Core ()
logC str = unverifiedLogC str

nano : Integer
nano = 1000000000

micro : Integer
micro = 1000000

export
logTimeOver : Integer -> Core String -> Core a -> Core a
logTimeOver nsecs str act
    = do clock <- coreLift (clockTime Process)
         let t = seconds clock * nano + nanoseconds clock
         res <- act
         clock <- coreLift (clockTime Process)
         let t' = seconds clock * nano + nanoseconds clock
         let time = t' - t
         when (time > nsecs) $
           assert_total $ -- We're not dividing by 0
              do str' <- str
                 coreLift $ putStrLn $ "TIMING " ++ str' ++ ": " ++
                          show (time `div` nano) ++ "." ++
                          addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
                          "s"
         pure res
  where
    addZeros : List Char -> String
    addZeros [] = "000"
    addZeros [x] = "00" ++ cast x
    addZeros [x,y] = "0" ++ cast x ++ cast y
    addZeros str = pack str

export
logTimeWhen : {auto c : Ref Ctxt Defs} ->
              Bool -> Lazy String -> Core a -> Core a
logTimeWhen p str act
    = if p
         then do clock <- coreLift (clockTime Process)
                 let t = seconds clock * nano + nanoseconds clock
                 res <- act
                 clock <- coreLift (clockTime Process)
                 let t' = seconds clock * nano + nanoseconds clock
                 let time = t' - t
                 assert_total $ -- We're not dividing by 0
                    coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++
                             show (time `div` nano) ++ "." ++
                             addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
                             "s"
                 pure res
         else act
  where
    addZeros : List Char -> String
    addZeros [] = "000"
    addZeros [x] = "00" ++ cast x
    addZeros [x,y] = "0" ++ cast x ++ cast y
    addZeros str = pack str

logTimeRecord' : {auto c : Ref Ctxt Defs} ->
                 String -> Core a -> Core a
logTimeRecord' key act
    = do clock <- coreLift (clockTime Process)
         let t = seconds clock * nano + nanoseconds clock
         res <- act
         clock <- coreLift (clockTime Process)
         let t' = seconds clock * nano + nanoseconds clock
         let time = t' - t
         defs <- get Ctxt
         let tot = case lookup key (timings defs) of
                        Nothing => 0
                        Just (_, t) => t
         put Ctxt (record { timings $= insert key (False, tot + time) } defs)
         pure res

-- for ad-hoc profiling, record the time the action takes and add it
-- to the time for the given category
export
logTimeRecord : {auto c : Ref Ctxt Defs} ->
                String -> Core a -> Core a
logTimeRecord key act
    = do defs <- get Ctxt
         -- Only record if we're not currently recording that key
         case lookup key (timings defs) of
              Just (True, t) => act
              Just (False, t)
                => do put Ctxt (record { timings $= insert key (True, t) } defs)
                      logTimeRecord' key act
              Nothing
                => logTimeRecord' key act

export
showTimeRecord : {auto c : Ref Ctxt Defs} ->
                 Core ()
showTimeRecord
    = do defs <- get Ctxt
         traverse_ showTimeLog (toList (timings defs))
  where
    addZeros : List Char -> String
    addZeros [] = "000"
    addZeros [x] = "00" ++ cast x
    addZeros [x,y] = "0" ++ cast x ++ cast y
    addZeros str = pack str

    showTimeLog : (String, (Bool, Integer)) -> Core ()
    showTimeLog (key, (_, time))
        = do coreLift $ putStr (key ++ ": ")
             assert_total $ -- We're not dividing by 0
                    coreLift $ putStrLn $ show (time `div` nano) ++ "." ++
                               addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
                               "s"

export
logTime : {auto c : Ref Ctxt Defs} ->
          Lazy String -> Core a -> Core a
logTime str act
    = do opts <- getSession
         logTimeWhen (logTimings opts) str act