text:
main : IO ()
main = do
  printLn $ cast {to = Integer} "end"
  printLn $ cast {to = Nat} "end"
  printLn $ cast {to = Double} "end"
  printLn $ cast {to = Bits8} "end"
  printLn $ cast {to = Bits16} "end"
  printLn $ cast {to = Bits32} "end"
  printLn $ cast {to = Bits64} "end"
  printLn $ cast {to = Int8} "end"
  printLn $ cast {to = Int16} "end"
  printLn $ cast {to = Int32} "end"
  printLn $ cast {to = Int64} "end"
  printLn $ cast {to = Int} "end"

ext: idr


text:
module QueryDoc

import System

import Effects
import Effect.System
import Effect.File
import Effect.StdIO
import Effect.Exception

import XML.DOM
import XML.Reader
import XML.XPath

%default partial

XEffs : List EFFECT
XEffs = [SYSTEM, FILE_IO (), STDIO, EXCEPTION String]

printRes : List XMLNode -> Eff () XEffs
printRes Nil     = pure ()
printRes (x::xs) = do
  putStrLn $ show @{xml} x
  printRes xs

eMain : Eff () XEffs
eMain = do
    [prog, fn, qstr] <- getArgs | Nil   => raise "Cannot happen!"
                                | [x]   => raise "Need doc and query"
                                | [x,y] => raise "Need Query"
                                | _     => raise "To manny arguments"

    case !(readXMLDoc fn) of
      Left err  => raise $ show err
      Right doc => do
        case query qstr doc of
          Left err  => raise $ show err
          Right Nil => raise "Nothing Found"
          Right xs  => printRes xs

namespace Main
  main : IO ()
  main = do
    run eMain
    exit 0
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


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

import Data.AVL.Dict
import Data.GraphViz.SimpleDot

import GRL.Lang.GLang
import GRL.Eval

import Edda
import Edda.Reader.Org
import XML.DOM

import Sif.Types
import Sif.Pattern.Model
import Sif.Pattern
import Sif.Builder.Utils

-- -------------------------------------------------------------- [ Directives ]

%access private
%default partial

-- ----------------------------------------- [ Private Internal Data Structure ]
export
data DirectRep : SifTy -> SifDomain -> Type where
  DirectMkReq : (ty   : RTy)
             -> (t    : String)
             -> (desc : Maybe String)
             -> DirectRep TyREQ d

  DirectMkProb : (title : String)
              -> (desc  : Maybe String)
              -> List (DirectRep TyREQ d)
              -> DirectRep TyPROBLEM d

  DirectMkAffect : (cval : CValue)
               -> (req : DirectRep TyREQ d)
               -> (desc : Maybe String)
               -> DirectRep TyAFFECTS d

  DirectMkTrait : (ty : TTy)
               -> (title : String)
               -> (desc  : Maybe String)
               -> (sval  : SValue)
               -> List (DirectRep TyAFFECTS d)
               -> DirectRep TyTRAIT d

  DirectMkProp : (title : String)
              -> (desc : Maybe String)
              -> List (DirectRep TyTRAIT d)
              -> DirectRep TyPROPERTY d

  DirectMkSolt : (title : String)
              -> (desc : Maybe String)
              -> List (DirectRep TyPROPERTY d)
              -> DirectRep TySOLUTION d

  DirectMkPatt : (title : String)
              -> (desc : Maybe String)
              -> DirectRep TyPROBLEM  d
              -> DirectRep TySOLUTION d
              -> DirectRep TyPATTERN  d

getDirectTitle : DirectRep ty d -> String
getDirectTitle (DirectMkReq _ t _)       = t
getDirectTitle (DirectMkProb t _ _)      = t
getDirectTitle (DirectMkTrait _ t _ _ _) = t
getDirectTitle (DirectMkProp t _ _)      = t
getDirectTitle (DirectMkSolt t _ _)      = t
getDirectTitle (DirectMkPatt t _ _ _)    = t

getDirectDesc : DirectRep ty d -> Maybe String
getDirectDesc (DirectMkReq _ _ d)       = d
getDirectDesc (DirectMkProb _ d rs)     = d
getDirectDesc (DirectMkAffect _ _ d)    = d
getDirectDesc (DirectMkTrait _ _ d _ _) = d
getDirectDesc (DirectMkProp _ d _)      = d
getDirectDesc (DirectMkSolt _ d _)      = d
getDirectDesc (DirectMkPatt _ d _ _)    = d

getDirectRTy : DirectRep TyREQ d -> RTy
getDirectRTy (DirectMkReq ty _ _) = ty

getDirectTTy : DirectRep TyTRAIT d -> TTy
getDirectTTy (DirectMkTrait ty _ _ _ _) = ty

getDirectSValue : DirectRep TyTRAIT d -> SValue
getDirectSValue (DirectMkTrait _ _ _ sval _) = sval

getDirectCValue : DirectRep TyAFFECTS d -> CValue
getDirectCValue (DirectMkAffect cval _ _) = cval

getDirectProblem : DirectRep TyPATTERN d -> (DirectRep TyPROBLEM d)
getDirectProblem (DirectMkPatt _ _ p _) = p

getDirectSolution : DirectRep TyPATTERN d -> DirectRep TySOLUTION d
getDirectSolution (DirectMkPatt _ _ _ s) = s

getDirectReqs : DirectRep TyPROBLEM d -> List $ DirectRep TyREQ d
getDirectReqs (DirectMkProb _ _ rs) = rs

getDirectProperties : DirectRep TySOLUTION d -> List $ DirectRep TyPROPERTY d
getDirectProperties (DirectMkSolt _ _ ps) = ps

getDirectTraits : DirectRep TyPROPERTY d -> List $ DirectRep TyTRAIT d
getDirectTraits (DirectMkProp _ _ ts) = ts

getDirectAffects : DirectRep TyTRAIT d -> List $ DirectRep TyAFFECTS d
getDirectAffects (DirectMkTrait _ _ _ _ as) = as

getDirectReq : DirectRep TyAFFECTS d -> DirectRep TyREQ d
getDirectReq (DirectMkAffect _ r _) = r

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

covering
toGRL : DirectRep ty d -> InterpRes ty
toGRL (DirectMkReq ty t d)        = interpReq t
toGRL (DirectMkProb t d rs)       = interpProb t (map toGRL rs)
toGRL (DirectMkAffect cval r d)   = interpAffect cval (toGRL r)
toGRL (DirectMkTrait ty t d s rs) = interpTrait t s (map toGRL rs) ty
toGRL (DirectMkProp t d ts)       = interpProp t (map toGRL ts)
toGRL (DirectMkSolt t d ps)       = interpSolt t (map toGRL ps)
toGRL (DirectMkPatt t d p s)      = interpPatt (toGRL p) (toGRL s)

-- ----------------------------------------------------- [ Instances and Stuff ]

getGModel : DirectRep TyPATTERN d -> GModel
getGModel p = extract (toGRL p)
  where
    extract : InterpRes TyPATTERN -> GModel
    extract (IPatt m) = m

-- ------------------------------------------------------ [ Builder Definition ]

SifRepAPI DirectRep where
  getTitle  x = getDirectTitle x
  getDesc     = getDirectDesc
  getTTy      = getDirectTTy
  getRTy      = getDirectRTy
  getSValue   = getDirectSValue
  getCValue   = getDirectCValue

  getProblem    = getDirectProblem
  getSolution   = getDirectSolution
  getReqs       = getDirectReqs
  getProperties = getDirectProperties
  getTraits     = getDirectTraits
  getAffects    = getDirectAffects
  getReq        = getDirectReq

  evalPattern p =
      case evalModel (getGModel p) Nothing of
        BadModel  => Bad
        Result gs => Good $ map (\x => (getNodeTitle x, getSValue x)) (getGNodes gs)

  fetchMetaModel p = mkMetaModel $ getGModel p

-- ------------------------------------------------------------- [ The Builder ]

%inline
conv : SifExpr ty d DirectRep -> DirectRep ty d
conv (MkExpr x) = x

buildReqDir : (d : SifDomain)
           -> RTy
           -> String
           -> Maybe String
           -> REQUIREMENT DirectRep d
buildReqDir _ ty s d = MkExpr $ DirectMkReq ty s d

buildProblemDir : (d : SifDomain)
               -> String
               -> Maybe String
               -> REQUIREMENTS DirectRep d
               -> PROBLEM DirectRep d
buildProblemDir _ t d rs =
    MkExpr $ DirectMkProb t d (map conv rs)

buildAffectDir : (d : SifDomain)
              -> CValue
              -> REQUIREMENT DirectRep d
              -> Maybe String
              -> AFFECT DirectRep d
buildAffectDir _ c r d = MkExpr $ DirectMkAffect c (conv r) d

buildTraitDir : (d : SifDomain)
             -> TTy
             -> String
             -> Maybe String
             -> SValue
             -> AFFECTS DirectRep d
             -> TRAIT DirectRep d
buildTraitDir _ ty t d s rs =
    MkExpr $ DirectMkTrait ty t d s (map conv rs)

buildPropertyDir : (d : SifDomain)
                -> String
                -> Maybe String
                -> TRAITS DirectRep d
                -> PROPERTY DirectRep d
buildPropertyDir _ t d ts =
    MkExpr $ DirectMkProp t d (map conv ts)

buildSolutionDir : (d : SifDomain)
                -> String
                -> Maybe String
                -> PROPERTIES DirectRep d
                -> SOLUTION DirectRep d
buildSolutionDir _ s d ps =
    MkExpr $ DirectMkSolt s d (map conv ps)

buildPatternDir : (d : SifDomain)
               -> String
               -> Maybe String
               -> PROBLEM DirectRep d
               -> SOLUTION DirectRep d
               -> PATTERN DirectRep d
buildPatternDir _ t d p s = MkExpr $ DirectMkPatt t d (conv p) (conv s)

export
directBuilder : SifBuilder DirectRep
directBuilder = MkSifBuilder
    buildReqDir
    buildProblemDir
    buildAffectDir
    buildTraitDir
    buildPropertyDir
    buildSolutionDir
    buildPatternDir

export
backendDirectRep : SifBackend
backendDirectRep = MkBackend "direct" directBuilder

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Control.Algebra

infixl 6 <->
infixl 7 <.>

public export
interface Semigroup ty => SemigroupV ty where
  semigroupOpIsAssociative : (l, c, r : ty) ->
    l <+> (c <+> r) = (l <+> c) <+> r

public export
interface (Monoid ty, SemigroupV ty) => MonoidV ty where
  monoidNeutralIsNeutralL : (l : ty) -> l <+> neutral {ty} = l
  monoidNeutralIsNeutralR : (r : ty) -> neutral {ty} <+> r = r

||| Sets equipped with a single binary operation that is associative,
||| along with a neutral element for that binary operation and
||| inverses for all elements. Satisfies the following laws:
|||
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Neutral for `<+>`:
|||     forall a,     a <+> neutral   == a
|||     forall a,     neutral <+> a   == a
||| + Inverse for `<+>`:
|||     forall a,     a <+> inverse a == neutral
|||     forall a,     inverse a <+> a == neutral
public export
interface MonoidV ty => Group ty where
  inverse : ty -> ty

  groupInverseIsInverseR : (r : ty) -> inverse r <+> r = neutral {ty}

(<->) : Group ty => ty -> ty -> ty
(<->) left right = left <+> (inverse right)

||| Sets equipped with a single binary operation that is associative
||| and commutative, along with a neutral element for that binary
||| operation and inverses for all elements. Satisfies the following
||| laws:
|||
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Commutativity of `<+>`:
|||     forall a b,   a <+> b         == b <+> a
||| + Neutral for `<+>`:
|||     forall a,     a <+> neutral   == a
|||     forall a,     neutral <+> a   == a
||| + Inverse for `<+>`:
|||     forall a,     a <+> inverse a == neutral
|||     forall a,     inverse a <+> a == neutral
public export
interface Group ty => AbelianGroup ty where
  groupOpIsCommutative : (l, r : ty) -> l <+> r = r <+> l

||| A homomorphism is a mapping that preserves group structure.
public export
interface (Group a, Group b) => GroupHomomorphism a b where
  to : a -> b

  toGroup : (x, y : a) ->
    to (x <+> y) = (to x) <+> (to y)

||| Sets equipped with two binary operations, one associative and
||| commutative supplied with a neutral element, and the other
||| associative, with distributivity laws relating the two operations.
||| Satisfies the following laws:
|||
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Commutativity of `<+>`:
|||     forall a b,   a <+> b         == b <+> a
||| + Neutral for `<+>`:
|||     forall a,     a <+> neutral   == a
|||     forall a,     neutral <+> a   == a
||| + Inverse for `<+>`:
|||     forall a,     a <+> inverse a == neutral
|||     forall a,     inverse a <+> a == neutral
||| + Associativity of `<.>`:
|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
||| + Distributivity of `<.>` and `<+>`:
|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
public export
interface Group ty => Ring ty where
  (<.>) : ty -> ty -> ty

  ringOpIsAssociative   : (l, c, r : ty) ->
    l <.> (c <.> r) = (l <.> c) <.> r
  ringOpIsDistributiveL : (l, c, r : ty) ->
    l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
  ringOpIsDistributiveR : (l, c, r : ty) ->
    (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

||| Sets equipped with two binary operations, one associative and
||| commutative supplied with a neutral element, and the other
||| associative supplied with a neutral element, with distributivity
||| laws relating the two operations. Satisfies the following laws:
|||
||| +  Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Commutativity of `<+>`:
|||     forall a b,   a <+> b         == b <+> a
||| + Neutral for `<+>`:
|||     forall a,     a <+> neutral   == a
|||     forall a,     neutral <+> a   == a
||| + Inverse for `<+>`:
|||     forall a,     a <+> inverse a == neutral
|||     forall a,     inverse a <+> a == neutral
||| + Associativity of `<.>`:
|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
||| + Neutral for `<.>`:
|||     forall a,     a <.> unity     == a
|||     forall a,     unity <.> a     == a
||| + Distributivity of `<.>` and `<+>`:
|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
public export
interface Ring ty => RingWithUnity ty where
  unity : ty

  unityIsRingIdL : (l : ty) -> l <.> unity = l
  unityIsRingIdR : (r : ty) -> unity <.> r = r

||| Sets equipped with two binary operations – both associative,
||| commutative and possessing a neutral element – and distributivity
||| laws relating the two operations. All elements except the additive
||| identity should have a multiplicative inverse. Should (but may
||| not) satisfy the following laws:
|||
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Commutativity of `<+>`:
|||     forall a b,   a <+> b         == b <+> a
||| + Neutral for `<+>`:
|||     forall a,     a <+> neutral   == a
|||     forall a,     neutral <+> a   == a
||| + Inverse for `<+>`:
|||     forall a,     a <+> inverse a == neutral
|||     forall a,     inverse a <+> a == neutral
||| + Associativity of `<.>`:
|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
||| + Unity for `<.>`:
|||     forall a,     a <.> unity     == a
|||     forall a,     unity <.> a     == a
||| + InverseM of `<.>`, except for neutral
|||     forall a /= neutral,  a <.> inverseM a == unity
|||     forall a /= neutral,  inverseM a <.> a == unity
||| + Distributivity of `<.>` and `<+>`:
|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
public export
interface RingWithUnity ty => Field ty where
  inverseM : (x : ty) -> Not (x = neutral {ty}) -> ty


text:
import System.File

main : IO ()
main
    = do Right ok <- readFile "test.txt"
               | Left err => printLn err
         putStr ok
         writeFile "testout.txt" "abc\ndef\n"
         Right ok <- readFile "testout.txt"
               | Left err => printLn err
         putStr ok
         Right ok <- readFile "notfound"
               | Left err => printLn err
         putStr ok

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
-- --------------------------------------------------------------- [ State.idr ]
-- Module      : Exercises.State
-- Description : Solutions to the Chapter 12 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.State

import public Chapter.State

%access export

-- -------------------------------------------------------- [ 12.1.5 Exercises ]

update : (stateType -> stateType) -> State stateType ()
update = (get >>=) . (put .)

increase : Nat -> State Nat ()
increase = update . (+)

%hide Chapter.State.increase

countEmpty : Tree a -> State Nat ()
countEmpty  Empty              = increase 1
countEmpty (Node left _ right) = countEmpty left *> countEmpty right

-- Like Bifunctor.first for Pair.
private
first : (a -> c) -> (a, b) -> (c, b)
first f (a, b) = (f a, b)

-- Like Bifunctor.second for Pair.
private
second : (b -> d) -> (a, b) -> (a, d)
second g (a, b) = (a, g b)

countEmptyNode : Tree a -> State (Nat, Nat) ()
countEmptyNode Empty               = update (first S)
countEmptyNode (Node left _ right) = countEmptyNode left  *>
                                     countEmptyNode right *>
                                     update (second S)

-- -------------------------------------------------------- [ 12.3.7 Exercises ]

export
updateGameState : (GameState -> GameState) -> Command ()
updateGameState f = GetGameState >>= PutGameState . f

public export
implementation Functor Command where
  map f x = Bind x (Pure . f)

public export
implementation Applicative Command where
  pure = Pure
  f <*> m = Bind f $ (Bind m) . (Pure .)

public export
implementation Monad Command where
  (>>=) = Bind

public export
record Votes where
  constructor MkVotes
  upvotes, downvotes : Integer

public export
record Article where
  constructor MkArticle
  title, url : String
  score : Votes

export
initPage : (title, url : String) -> Article
initPage title url = MkArticle title url (MkVotes 0 0)

export
getScore : Article -> Integer
getScore = (\(MkVotes up down) => up - down) . score

export
addUpvote : Article -> Article
addUpvote = record { score->upvotes $= (+1) }

export
addDownvote : Article -> Article
addDownvote = record { score->downvotes $= (+1) }

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Main

import tipos
import lexer
import parser
import piAutomata
import Data.SortedMap

verificaList : List Token -> Bool
verificaList [] = True
verificaList l = False

removeParam : String -> String -> String
removeParam str p = let list = words str in removeAux list p where
  removeAux : List String -> String -> String
  removeAux x p' = unwords (filter ((/=) p') x)

printPi: (List Ctrl, List Val, SortedMap Id Bindable , SortedMap Loc Val, List Loc) -> String
printPi (c, v, e, s, l) = "\n##############################################################\n\nPilha de Controle: " ++ show c ++ "\n\n" ++ "Pilha de Valores: " ++ show v ++ "\n\n" ++ "Enviroment: " ++ show (toList e) ++ "\n\n" ++ "Stored: " ++ show (toList s) ++ "\n\n" ++ "Lista de Locations: " ++ show l ++ "\n"

read_input : String -> String -> String
read_input x "" = let (e, l) = (ctrlParser (read_token (unpack x) "" [])) in case e of
  Nothing  => "Parser Error! \n" ++ show l ++ "\n"
  Just k => if (verificaList l) then let (resp, (x1::x2::xs)) = process ([k], [], empty, empty, []) []
     in unwords(map printPi (x1::[x2])) else "Parser Error! \n" ++ show l ++ "\n"
read_input x "--all" = let (e, l) = (ctrlParser (read_token (unpack x) "" [])) in case e of
 Nothing  => "Parser Error! \n" ++ show l ++ "\n"
 Just k => if (verificaList l) then let (resp, (x::xs)) = process ([k], [], empty, empty, []) []
    in unwords(map printPi (x::xs)) else "Parser Error! \n" ++ show l ++ "\n"
read_input x "--a" = let (e, l) = (ctrlParser (read_token (unpack x) "" [])) in case e of
 Nothing  => "Parser Error! \n" ++ show l ++ "\n"
 Just k => if (verificaList l) then let (resp, (x1::x2::xs)) = process ([k], [], empty, empty, []) []
    in "\n" ++ show e ++ "\n" ++ unwords(map printPi (x1::[x2])) else "Parser Error! \n" ++ show l ++ "\n"

leParametro : String -> String
leParametro str = let palavras = words str in case palavras of
  [] => ""
  (x::xs) => let p = (last (x::xs)) in case p of
    "--all" => read_input (removeParam str "--all") "--all"
    "--a" => read_input (removeParam str "--a") "--a"
    x => read_input str ""

main : IO ()
main = repl "Enter a program: " leParametro

max_stars_repo_name: RonaldCamp/ImpCompiler

max_issues_repo_name: RonaldCamp/ImpCompiler

max_forks_repo_name: RonaldCamp/ImpCompiler


text:
module Main

main : IO ()
main = do putStr "Enter your name: "
          name <- getLine
          putStrLn $ "Nice to meet you, " ++ name ++ "!"

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Text.Markdown

import Text.Markdown.Definition
import Text.Markdown.Options

%link    C "cmark.o"
%include C "commonmark.c"
%include C "scanners.c"

-- Direct foreign function calls -----------------------------------

-- void free(void* ptr);
cFree : Ptr -> IO ()
cFree ptr = foreign FFI_C "free" (Ptr -> IO Unit) ptr

-- void cmark_free_nodes(node_block* e);
cFreeNodes : Ptr -> IO ()
cFreeNodes ptr = foreign FFI_C "cmark_free_nodes" (Ptr -> IO Unit) ptr

-- void cmark_debug_print(node_block* b, int indent);
cPrintBlocks : Ptr -> IO ()
cPrintBlocks ptr = foreign FFI_C "cmark_debug_print" (Ptr -> IO Unit) ptr

-- node_block *readMarkdown(char *str);
cReadMarkdown : String -> IO Ptr
cReadMarkdown str = foreign FFI_C "readMarkdown" (String -> IO Ptr) str

-- char *writeHtml(node_block *cur);
cWriteHtml : Ptr -> IO String
cWriteHtml ptr = foreign FFI_C "writeHtml" (Ptr -> IO String) ptr

-- void printHtml(node_block *cur);
cPrintHtml : Ptr -> IO ()
cPrintHtml ptr = foreign FFI_C "printHtml" (Ptr -> IO Unit) ptr

-- High-level binding: struct Inline* => data Inline ---------------

-- const char *getInlineTag(node_inl *i);
cGetInlineTag : Ptr -> IO InlineTag
cGetInlineTag ptr = return $ case !(foreign FFI_C "getInlineTag" (Ptr -> IO String) ptr) of
                                  "str"       => Str
                                  "softbreak" => SoftBreak
                                  "linebreak" => LineBreak
                                  "code"      => Code
                                  "raw_html"  => RawHtml
                                  "entity"    => Entity
                                  "emph"      => Emph
                                  "strong"    => Strong
                                  "link"      => Link
                                  "image"     => Image

-- const char *getInlineContent_Literal(node_inl *i);
cGetInlineContent_Literal : Ptr -> IO Literal
cGetInlineContent_Literal ptr = foreign FFI_C "getInlineContent_Literal" (Ptr -> IO String) ptr >>= return . MkLiteral

-- node_inl *getInlineContent_Inlines(node_inl *i);
cGetInlineContent_Inlines : Ptr -> IO Ptr
cGetInlineContent_Inlines ptr = foreign FFI_C "getInlineContent_Inlines" (Ptr -> IO Ptr) ptr

-- node_inl *getInlineContent_Linkable_Label(node_inl *i);
cGetInlineContent_Linkable_Label : Ptr -> IO Ptr
cGetInlineContent_Linkable_Label ptr = foreign FFI_C "getInlineContent_Linkable_Label" (Ptr -> IO Ptr) ptr

-- const char *getInlineContent_Linkable_Url(node_inl *i);
cGetInlineContent_Linkable_Url : Ptr -> IO String
cGetInlineContent_Linkable_Url ptr = foreign FFI_C "getInlineContent_Linkable_Url" (Ptr -> IO String) ptr

-- const char *getInlineContent_Linkable_Title(inl *i);
cGetInlineContent_Linkable_Title : Ptr -> IO String
cGetInlineContent_Linkable_Title ptr = foreign FFI_C "getInlineContent_Linkable_Title" (Ptr -> IO String) ptr

-- node_inl *getInlineNext(node_inl *i);
cGetInlineNext : Ptr -> IO Ptr
cGetInlineNext ptr = foreign FFI_C "getInlineNext" (Ptr -> IO Ptr) ptr

-- High-level binding: struct Block* => data Block -----------------

-- const char *getBlockTag(node_block *cur);
cGetBlockTag : Ptr -> IO BlockTag
cGetBlockTag ptr = return $ case !(foreign FFI_C "getBlockTag" (Ptr -> IO String) ptr) of
                                 "document"      => Document
                                 "bquote"        => BlockQuote
                                 "list"          => GenericList
                                 "list_item"     => GenericListItem
                                 "fenced_code"   => FencedCode
                                 "indented_code" => IndentedCode
                                 "html"          => HtmlBlock
                                 "paragraph"     => Paragraph
                                 "atx_header"    => AtxHeader
                                 "setext_header" => SetExtHeader
                                 "hrule"         => HRule
                                 "reference_def" => ReferenceDef

-- int getBlockStartLine(node_block *cur);
cGetBlockStartLine : Ptr -> IO Int
cGetBlockStartLine ptr = foreign FFI_C "getBlockStartLine" (Ptr -> IO Int) ptr

-- int getBlockStartColumn(node_block *cur);
cGetBlockStartColumn : Ptr -> IO Int
cGetBlockStartColumn ptr = foreign FFI_C "getBlockStartColumn" (Ptr -> IO Int) ptr

-- int getBlockEndLine(node_block *cur);
cGetBlockEndLine : Ptr -> IO Int
cGetBlockEndLine ptr = foreign FFI_C "getBlockEndLine" (Ptr -> IO Int) ptr

-- bool getBlockOpen(node_block *cur);
cGetBlockOpen : Ptr -> IO Bool
cGetBlockOpen ptr = foreign FFI_C "getBlockOpen" (Ptr -> IO Int) ptr >>= return . (/= 0)

-- bool getBlockLastLineBlank(node_block *cur);
cGetBlockLastLineBlank : Ptr -> IO Bool
cGetBlockLastLineBlank ptr = foreign FFI_C "getBlockLastLineBlank" (Ptr -> IO Int) ptr >>= return . (/= 0)

-- struct Block *getBlockChildren(node_block *cur);
cGetBlockChildren : Ptr -> IO Ptr
cGetBlockChildren ptr = foreign FFI_C "getBlockChildren" (Ptr -> IO Ptr) ptr

-- const char *getBlockStringContent(node_block *cur);
cGetBlockStringContent : Ptr -> IO String
cGetBlockStringContent ptr = foreign FFI_C "getBlockStringContent" (Ptr -> IO String) ptr

-- inl *getBlockInlineContent(node_block *cur);
cGetBlockInlineContent : Ptr -> IO Ptr
cGetBlockInlineContent ptr = foreign FFI_C "getBlockInlineContent" (Ptr -> IO Ptr) ptr

-- const char *getBlockAttributes_ListData_ListType(node_block *cur);
cGetBlockAttributes_ListData_ListType : Ptr -> IO ListType
cGetBlockAttributes_ListData_ListType ptr = return $ case !(foreign FFI_C "getBlockAttributes_ListData_ListType" (Ptr -> IO String) ptr) of
                                                          "bullet" => Bullet
                                                          "ordered" => Ordered

-- int getBlockAttributes_ListData_MarkerOffset(node_block *cur);
cGetBlockAttributes_ListData_MarkerOffset : Ptr -> IO Int
cGetBlockAttributes_ListData_MarkerOffset ptr = foreign FFI_C "getBlockAttributes_ListData_MarkerOffset" (Ptr -> IO Int) ptr

-- int getBlockAttributes_ListData_Padding(node_block *cur);
cGetBlockAttributes_ListData_Padding : Ptr -> IO Int
cGetBlockAttributes_ListData_Padding ptr = foreign FFI_C "getBlockAttributes_ListData_Padding" (Ptr -> IO Int) ptr

-- int getBlockAttributes_ListData_Start(node_block *cur);
cGetBlockAttributes_ListData_Start : Ptr -> IO Int
cGetBlockAttributes_ListData_Start ptr = foreign FFI_C "getBlockAttributes_ListData_Start" (Ptr -> IO Int) ptr

-- const char *getBlockAttributes_ListData_Delimiter(node_block *cur);
cGetBlockAttributes_ListData_Delimiter : Ptr -> IO Delimiter
cGetBlockAttributes_ListData_Delimiter ptr = return $ case !(foreign FFI_C "getBlockAttributes_ListData_Delimiter" (Ptr -> IO String) ptr) of
                                                           "period" => Period
                                                           "parens" => Parens

-- char getBlockAttributes_ListData_BulletChar(node_block *cur);
cGetBlockAttributes_ListData_BulletChar : Ptr -> IO Char
cGetBlockAttributes_ListData_BulletChar ptr = foreign FFI_C "getBlockAttributes_ListData_BulletChar" (Ptr -> IO Char) ptr

-- bool getBlockAttributes_ListData_Tight(node_block *cur);
cGetBlockAttributes_ListData_Tight : Ptr -> IO Bool
cGetBlockAttributes_ListData_Tight ptr = foreign FFI_C "getBlockAttributes_ListData_Tight" (Ptr -> IO Int) ptr >>= return . (/= 0)

-- int getBlockAttributes_FencedCodeData_FenceLength(node_block *cur);
cGetBlockAttributes_FencedCodeData_FenceLength : Ptr -> IO Int
cGetBlockAttributes_FencedCodeData_FenceLength ptr = foreign FFI_C "getBlockAttributes_FencedCodeData_FenceLength" (Ptr -> IO Int) ptr

-- int getBlockAttributes_FencedCodeData_FenceOffset(node_block *cur);
cGetBlockAttributes_FencedCodeData_FenceOffset : Ptr -> IO Int
cGetBlockAttributes_FencedCodeData_FenceOffset ptr = foreign FFI_C "getBlockAttributes_FencedCodeData_FenceOffset" (Ptr -> IO Int) ptr

-- char getBlockAttributes_FencedCodeData_FenceChar(node_block *cur);
cGetBlockAttributes_FencedCodeData_FenceChar : Ptr -> IO Char
cGetBlockAttributes_FencedCodeData_FenceChar ptr = foreign FFI_C "getBlockAttributes_FencedCodeData_FenceChar" (Ptr -> IO Char) ptr

-- const char *getBlockAttributes_FencedCodeData_Info(node_block *cur);
cGetBlockAttributes_FencedCodeData_Info : Ptr -> IO String
cGetBlockAttributes_FencedCodeData_Info ptr = foreign FFI_C "getBlockAttributes_FencedCodeData_Info" (Ptr -> IO String) ptr

-- int getBlockAttributes_HeaderLevel(node_block *cur);
cGetBlockAttributes_HeaderLevel : Ptr -> IO HeaderLevel
cGetBlockAttributes_HeaderLevel ptr = foreign FFI_C "getBlockAttributes_HeaderLevel" (Ptr -> IO Int) ptr >>= return . MkHeaderLevel

-- node_block *getBlockNext(node_block *cur);
cGetBlockNext : Ptr -> IO Ptr
cGetBlockNext ptr = foreign FFI_C "getBlockNext" (Ptr -> IO Ptr) ptr

-- High-level binding: cGetInline ----------------------------------

mutual
  cGetInlineContent_Linkable: Ptr -> IO Linkable
  cGetInlineContent_Linkable cur = return $ MkLinkable !(cGetInline !(cGetInlineContent_Linkable_Label cur))
                                                       !(cGetInlineContent_Linkable_Url cur)
                                                       !(cGetInlineContent_Linkable_Title cur)

  cGetInlineContent : Ptr -> InlineTag -> IO Content
  cGetInlineContent cur tag = case tag of
                                   Str       => cGetInlineContent_Literal cur >>= return . MkLiteralContent
                                   SoftBreak => return NullContent
                                   LineBreak => return NullContent
                                   Code      => cGetInlineContent_Literal cur >>= return . MkLiteralContent
                                   RawHtml   => cGetInlineContent_Literal cur >>= return . MkLiteralContent
                                   Entity    => cGetInlineContent_Literal cur >>= return . MkLiteralContent
                                   Emph      => cGetInlineContent_Linkable cur >>= return . MkLinkableContent
                                   Strong    => cGetInlineContent_Linkable cur >>= return . MkLinkableContent
                                   Link      => cGetInlineContent_Linkable cur >>= return . MkLinkableContent
                                   Image     => cGetInlineContent_Linkable cur >>= return . MkLinkableContent

  cGetInline : Ptr -> IO Inline
  cGetInline cur = if !(nullPtr cur)
                      then return NullInline
                      else do
                           tag <- cGetInlineTag cur
                           return $ MkInline
                                  $ MkInline' tag
                                              !(cGetInlineContent cur tag)
                                              !(cGetInline !(cGetInlineNext cur))

-- High-level binding: cGetBlock -----------------------------------

cGetBlockAttributes_ListData : Ptr -> IO ListData
cGetBlockAttributes_ListData cur = return $ MkListData !(cGetBlockAttributes_ListData_ListType cur)
                                                       !(cGetBlockAttributes_ListData_MarkerOffset cur)
                                                       !(cGetBlockAttributes_ListData_Padding cur)
                                                       !(cGetBlockAttributes_ListData_Start cur)
                                                       !(cGetBlockAttributes_ListData_Delimiter cur)
                                                       !(cGetBlockAttributes_ListData_BulletChar cur)
                                                       !(cGetBlockAttributes_ListData_Tight cur)

cGetBlockAttributes_FencedCodeData : Ptr -> IO FencedCodeData
cGetBlockAttributes_FencedCodeData cur = return $ MkFencedCodeData !(cGetBlockAttributes_FencedCodeData_FenceLength cur)
                                                                   !(cGetBlockAttributes_FencedCodeData_FenceOffset cur)
                                                                   !(cGetBlockAttributes_FencedCodeData_FenceChar cur)
                                                                   !(cGetBlockAttributes_FencedCodeData_Info cur)

cGetBlockAttributes : Ptr -> BlockTag -> IO Attributes
cGetBlockAttributes cur tag = case tag of
                                   Document        => return NullAttributes
                                   BlockQuote      => return NullAttributes
                                   GenericList     => cGetBlockAttributes_ListData cur >>= return . MkListDataAttributes
                                   GenericListItem => cGetBlockAttributes_ListData cur >>= return . MkListDataAttributes
                                   FencedCode      => cGetBlockAttributes_FencedCodeData cur >>= return . MkFencedCodeDataAttributes
                                   IndentedCode    => return NullAttributes
                                   HtmlBlock       => return NullAttributes
                                   Paragraph       => return NullAttributes
                                   AtxHeader       => cGetBlockAttributes_HeaderLevel cur >>= return . MkHeaderLevelAttributes
                                   SetExtHeader    => cGetBlockAttributes_HeaderLevel cur >>= return . MkHeaderLevelAttributes
                                   HRule           => return NullAttributes
                                   ReferenceDef    => return NullAttributes --FIXME!

cGetBlock : Ptr -> IO Block
cGetBlock cur = if !(nullPtr cur)
                   then return NullBlock
                   else do
                        tag <- cGetBlockTag cur
                        return $ MkBlock
                               $ MkBlock' tag
                                          !(cGetBlockStartLine cur)
                                          !(cGetBlockStartColumn cur)
                                          !(cGetBlockEndLine cur)
                                          !(cGetBlockOpen cur)
                                          !(cGetBlockLastLineBlank cur)
                                          !(cGetBlock !(cGetBlockChildren cur))
                                          !(cGetBlockStringContent cur)
                                          !(cGetInline !(cGetBlockInlineContent cur))
                                          !(cGetBlockAttributes cur tag)
                                          !(cGetBlock !(cGetBlockNext cur))

-- Idris API -------------------------------------------------------

readMarkdown : ReaderOptions -> String -> Markdown
readMarkdown opts s = unsafePerformIO $
                      do
                      cur <- cReadMarkdown s
                      block <- cGetBlock cur
                      cFreeNodes cur
                      return $ MkMarkdown (MkMeta s)
                                          [block]

readMarkdown' : String -> Markdown
readMarkdown' = readMarkdown def

writeMarkdown : WriterOptions -> Markdown -> String
writeMarkdown _ = source . meta

writeMarkdown' : Markdown -> String
writeMarkdown' = writeMarkdown def

writeHtml : WriterOptions -> Markdown -> String
writeHtml opts m = unsafePerformIO $
                   do
                   let s = source (meta m)
                   cur <- cReadMarkdown s
                   html <- cWriteHtml cur
                   cFreeNodes cur
                   return html

writeHtml' : Markdown -> String
writeHtml' = writeHtml def

printMarkdown : WriterOptions -> Markdown -> IO ()
printMarkdown opts m = putStrLn $ writeMarkdown opts m

printMarkdown' : Markdown -> IO ()
printMarkdown' = printMarkdown def

printHtml : WriterOptions -> Markdown -> IO ()
printHtml opts m = putStrLn $ writeHtml opts m

printHtml' : Markdown -> IO ()
printHtml' = printHtml def

printAST : WriterOptions -> Markdown -> IO ()
printAST opts m = do
                  let s = source (meta m)
                  cur <- cReadMarkdown s
                  cPrintBlocks cur
                  cFreeNodes cur

printAST' : Markdown -> IO ()
printAST' = printAST def

max_stars_repo_name: soimort/idris-commonmark

max_issues_repo_name: soimort/idris-commonmark

max_forks_repo_name: soimort/idris-commonmark


text:
import Data.Primitives.Views
import System

%default total

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

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

data Fuel = Dry | More (Lazy Fuel)

partial
forever: Fuel
forever = More forever

run: Fuel -> InfIO -> IO()
run Dry         y                = putStrLn "Out of fuel"
run (More fuel) (Do action cont) =
  do
    res <- action
    run fuel (cont res)

quiz : Stream Int -> (score: Nat) -> InfIO
quiz (num1 :: num2 :: nums) score =
  do
    putStrLn ("Score so far: " ++ show score)
    putStr   (show num1 ++ " * " ++ show num2 ++ "? ")
    answer <- getLine
    if cast answer == num1 * num2
      then do putStrLn "Correct!"
              quiz nums (score + 1)
      else do putStrLn ("Wrong, the answer is " ++ show (num1 * num2))
              quiz nums score

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

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

partial
main : IO()
main =
  do
    seed <- time
    run forever (quiz (arithInputs (fromInteger seed)) 0)

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.Message.SemanticTokens

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

namespace SemanticTokenClientCapabilities
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
  public export
  record SemanticTokenRequestsFull where
    constructor MkSemanticTokenRequestsFull
    delta : Maybe Bool
  %runElab deriveJSON defaultOpts `{{SemanticTokenRequestsFull}}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
  public export
  record SemanticTokenRequests where
    constructor MkSemanticTokenRequests
    range : Maybe (OneOf [Bool, ()])
    full  : Maybe (OneOf [Bool, SemanticTokenRequestsFull])
  %runElab deriveJSON defaultOpts `{{SemanticTokenRequests}}

namespace TokenFormat
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
  public export
  data TokenFormat = Relative

export
ToJSON TokenFormat where
  toJSON Relative = JString "relative"

export
FromJSON TokenFormat where
  fromJSON (JString "relative") = pure Relative
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensLegend where
  constructor MkSemanticTokensLenged
  tokenTypes     : List String
  tokenModifiers : List String
%runElab deriveJSON defaultOpts `{{SemanticTokensLegend}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensClientCapabilities where
  constructor MkSemanticTokensClientCapabilities
  dynamicRegistration     : Maybe Bool
  requests                : SemanticTokenRequests
  tokenTypes              : List String
  tokenModifiers          : List String
  formats                 : List TokenFormat
  overlappingTokenSupport : Maybe Bool
  multilineTokenSupport   : Maybe Bool
%runElab deriveJSON defaultOpts `{{SemanticTokensClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensOptions where
  constructor MkSemanticTokensOptions
  legend : SemanticTokensLegend
  range  : Maybe (OneOf [Bool, ()])
  full   : Maybe (OneOf [Bool, SemanticTokenRequestsFull])
%runElab deriveJSON defaultOpts `{{SemanticTokensOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensRegistrationOptions where
  constructor MkSemanticTokensRegistrationOptions
  legend           : SemanticTokensLegend
  range            : Maybe (OneOf [Bool, ()])
  full             : Maybe (OneOf [Bool, SemanticTokenRequestsFull])
  documentSelector : OneOf [DocumentSelector, Null]
  id               : Maybe Bool
%runElab deriveJSON defaultOpts `{{SemanticTokensRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensParams where
  constructor MkSemanticTokensParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
%runElab deriveJSON defaultOpts `{{SemanticTokensParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokens where
  constructor MkSemanticTokens
  resultId : Maybe String
  data_    : List Int
%runElab deriveJSON (record {renames = [("data_", "data")]} defaultOpts) `{{SemanticTokens}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensPartialResult where
  constructor MkSemanticTokensPartialResult
  data_ : List Int
%runElab deriveJSON (record {renames = [("data_", "data")]} defaultOpts) `{{SemanticTokensPartialResult}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensDeltaParams where
  constructor MkSemanticTokensDeltaParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
  previousResultId   : String
%runElab deriveJSON defaultOpts `{{SemanticTokensDeltaParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensEdit where
  constructor MkSemanticTokensEdit
  start       : Int
  deleteCount : Int
  data_       : Maybe (List Int)
%runElab deriveJSON (record {renames = [("data_", "data")]} defaultOpts) `{{SemanticTokensEdit}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensDelta where
  constructor MkSemanticTokensDelta
  resultId : Maybe String
  edits    : List SemanticTokensEdit
%runElab deriveJSON defaultOpts `{{SemanticTokensDelta}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensDeltaPartialResult where
  constructor MkSemanticTokensDeltaPartialResult
  edits : List SemanticTokensEdit
%runElab deriveJSON defaultOpts `{{SemanticTokensDeltaPartialResult}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensRangeParams where
  constructor MkSemanticTokensRangeParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
  range              : Range
%runElab deriveJSON defaultOpts `{{SemanticTokensRangeParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens
public export
record SemanticTokensWorkspaceClientCapabilities where
  constructor MkSemanticTokensWorkspaceClientCapabilities
  refreshSupport : Maybe Bool
%runElab deriveJSON defaultOpts `{{SemanticTokensWorkspaceClientCapabilities}}


text:
Ty : Type
Ty = (Ty   : Type)
 ->  (nat  : Ty)
 ->  (top  : Ty)
 ->  (bot  : Ty)
 ->  (arr  : Ty -> Ty -> Ty)
 ->  (prod : Ty -> Ty -> Ty)
 ->  (sum  : Ty -> Ty -> Ty)
 ->  Ty

nat : Ty
nat = \ _, nat, _, _, _, _, _ => nat
top : Ty
top = \ _, _, top, _, _, _, _ => top
bot : Ty
bot = \ _, _, _, bot, _, _, _ => bot

arr : Ty-> Ty-> Ty
arr = \ a, b, ty, nat, top, bot, arr, prod, sum =>
     arr (a ty nat top bot arr prod sum) (b ty nat top bot arr prod sum)

prod : Ty-> Ty-> Ty
prod = \ a, b, ty, nat, top, bot, arr, prod, sum =>
     prod (a ty nat top bot arr prod sum) (b ty nat top bot arr prod sum)

sum : Ty-> Ty-> Ty
sum = \ a, b, ty, nat, top, bot, arr, prod, sum =>
     sum (a ty nat top bot arr prod sum) (b ty nat top bot arr prod sum)

Con : Type
Con = (Con : Type)
 -> (nil  : Con)
 -> (snoc : Con -> Ty-> Con)
 -> Con

nil : Con
nil = \ con, nil, snoc => nil

snoc : Con -> Ty-> Con
snoc = \ g, a, con, nil, snoc => snoc (g con nil snoc) a

Var : Con -> Ty-> Type
Var = \ g, a =>
    (Var : Con -> Ty-> Type)
 -> (vz  : {g:_}->{a:_} -> Var (snoc g a) a)
 -> (vs  : {g:_}->{b:_}->{a:_} -> Var g a -> Var (snoc g b) a)
 -> Var g a

vz : {g:_}->{a:_} -> Var (snoc g a) a
vz = \ var, vz, vs => vz

vs : {g:_}->{b:_}->{a:_} -> Var g a -> Var (snoc g b) a
vs = \ x, var, vz, vs => vs (x var vz vs)

Tm : Con -> Ty-> Type
Tm = \ g, a =>
    (Tm    : Con -> Ty-> Type)
 -> (var   : {g:_}->{a:_}-> Var g a -> Tm g a)
 -> (lam   : {g:_}->{a:_}->{b:_} -> Tm (snoc g a) b -> Tm g (arr a b))
 -> (app   : {g:_}->{a:_}->{b:_} -> Tm g (arr a b) -> Tm g a -> Tm g b)
 -> (tt    : {g:_}-> Tm g top)
 -> (pair  : {g:_}->{a:_}->{b:_} -> Tm g a -> Tm g b -> Tm g (prod a b))
 -> (fst   : {g:_}->{a:_}->{b:_} -> Tm g (prod a b) -> Tm g a)
 -> (snd   : {g:_}->{a:_}->{b:_} -> Tm g (prod a b) -> Tm g b)
 -> (left  : {g:_}->{a:_}->{b:_} -> Tm g a -> Tm g (sum a b))
 -> (right : {g:_}->{a:_}->{b:_} -> Tm g b -> Tm g (sum a b))
 -> (split : {g:_}->{a:_}->{b:_}-> {c:_} -> Tm g (sum a b) -> Tm g (arr a c) -> Tm g (arr b c) -> Tm g c)
 -> (zero  : {g:_}-> Tm g nat)
 -> (suc   : {g:_}-> Tm g nat -> Tm g nat)
 -> (rec   : {g:_}->{a:_} -> Tm g nat -> Tm g (arr nat (arr a a)) -> Tm g a -> Tm g a)
 -> Tm g a

var : {g:_}->{a:_} -> Var g a -> Tm g a
var = \ x, tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec => var x

lam : {g:_}->{a:_}->{b:_}-> Tm (snoc g a) b -> Tm g (arr a b)
lam = \ t, tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>
     lam (t tm var lam app tt pair fst snd left right split zero suc rec)

app : {g:_}->{a:_}->{b:_} -> Tm g (arr a b) -> Tm g a -> Tm g b
app = \ t, u, tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>
     app (t tm var lam app tt pair fst snd left right split zero suc rec)
         (u tm var lam app tt pair fst snd left right split zero suc rec)

tt : {g:_} -> Tm g Main.top
tt = \ tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec => tt

pair : {g:_}->{a:_}->{b:_} -> Tm g a -> Tm g b -> Tm g (prod a b)
pair = \ t, u, tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>
     pair (t tm var lam app tt pair fst snd left right split zero suc rec)
          (u tm var lam app tt pair fst snd left right split zero suc rec)

fst : {g:_}->{a:_}->{b:_}-> Tm g (prod a b) -> Tm g a
fst = \ t, tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>
     fst (t tm var lam app tt pair fst snd left right split zero suc rec)

snd : {g:_}->{a:_}->{b:_} -> Tm g (prod a b) -> Tm g b
snd = \ t, tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>
     snd (t tm var lam app tt pair fst snd left right split zero suc rec)

left : {g:_}->{a:_}->{b:_} -> Tm g a -> Tm g (sum a b)
left = \ t, tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>
     left (t tm var lam app tt pair fst snd left right split zero suc rec)

right : {g:_}->{a:_}->{b:_} -> Tm g b -> Tm g (sum a b)
right = \ t, tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>
     right (t tm var lam app tt pair fst snd left right split zero suc rec)

split : {g:_}->{a:_}->{b:_}->{c:_} -> Tm g (sum a b) -> Tm g (arr a c) -> Tm g (arr b c) -> Tm g c
split = \ t, u, v, tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>
     split (t tm var lam app tt pair fst snd left right split zero suc rec)
          (u tm var lam app tt pair fst snd left right split zero suc rec)
          (v tm var lam app tt pair fst snd left right split zero suc rec)

zero : {g:_} -> Tm g Main.nat
zero = \ tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec => zero

suc : {g:_} -> Tm g Main.nat -> Tm g Main.nat
suc = \ t, tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>
   suc (t tm var lam app tt pair fst snd left right split zero suc rec)

rec : {g:_}->{a:_} -> Tm g Main.nat -> Tm g (arr Main.nat (arr a a)) -> Tm g a -> Tm g a
rec = \ t, u, v, tm, var, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>
     rec (t tm var lam app tt pair fst snd left right split zero suc rec)
         (u tm var lam app tt pair fst snd left right split zero suc rec)
         (v tm var lam app tt pair fst snd left right split zero suc rec)

v0 : {g:_}->{a:_} -> Tm (snoc g a) a
v0 = var vz

v1 : {g:_}->{a:_}->{b:_} -> Tm (snoc (snoc g a) b) a
v1 = var (vs vz)

v2 : {g:_}->{a:_}->{b:_}->{c:_} -> Tm (snoc (snoc (snoc g a) b) c) a
v2 = var (vs (vs vz))

v3 : {g:_}->{a:_}->{b:_}->{c:_}->{d:_} -> Tm (snoc (snoc (snoc (snoc g a) b) c) d) a
v3 = var (vs (vs (vs vz)))

tbool : Ty
tbool = sum top top

ttrue : {g:_} -> Tm g Main.tbool
ttrue = left tt

tfalse : {g:_} -> Tm g Main.tbool
tfalse = right tt

ifthenelse : {g:_}->{a:_} -> Tm g (arr Main.tbool (arr a (arr a a)))
ifthenelse = lam (lam (lam (split v2 (lam v2) (lam v1))))

times4 : {g:_}->{a:_} -> Tm g (arr (arr a a) (arr a a))
times4  = lam (lam (app v1 (app v1 (app v1 (app v1 v0)))))

add : {g:_} -> Tm g (arr Main.nat (arr Main.nat Main.nat))
add = lam (rec v0
       (lam (lam (lam (suc (app v1 v0)))))
       (lam v0))

mul : {g:_} -> Tm g (arr Main.nat (arr Main.nat Main.nat))
mul = lam (rec v0
       (lam (lam (lam (app (app add (app v1 v0)) v0))))
       (lam zero))

fact : {g:_} -> Tm g (arr Main.nat Main.nat)
fact = lam (rec v0 (lam (lam (app (app mul (suc v1)) v0)))
                 (suc zero))

max_stars_repo_name: Kha/smalltt

max_issues_repo_name: Kha/smalltt

max_forks_repo_name: Kha/smalltt


text:
module Idris.IDEMode.CaseSplit

import Core.Context
import Core.Context.Log
import Core.Env
import Core.Metadata
import Core.TT
import Core.Value

import Parser.Lexer.Source
import Parser.Unlit

import TTImp.Interactive.CaseSplit
import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Utils

import Idris.IDEMode.TokenLine
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax

import Data.List
import Data.List1
import Data.List.Views
import Data.SnocList
import Libraries.Data.List.Extra
import Libraries.Data.String.Extra
import Data.String
import System.File
import Data.Fin

%hide Data.String.lines
%hide Data.String.lines'
%hide Data.String.unlines
%hide Data.String.unlines'

%default covering

||| A series of updates is a mapping from `RawName` to `String`
||| `RawName` is currently just an alias for `String`
||| `String` is a rendered `List SourcePart`
Updates : Type
Updates = List (RawName, String)

||| Convert a RawImp update to a SourcePart one
toStrUpdate : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              (Name, RawImp) -> Core Updates
toStrUpdate (UN (Basic n), term)
    = do clause <- pterm (map defaultKindedName term) -- hack
         pure [(n, show (bracket clause))]
  where
    bracket : PTerm' nm -> PTerm' nm
    bracket tm@(PRef _ _) = tm
    bracket tm@(PList _ _ _) = tm
    bracket tm@(PSnocList _ _ _) = tm
    bracket tm@(PPair _ _ _) = tm
    bracket tm@(PUnit _) = tm
    bracket tm@(PComprehension _ _ _) = tm
    bracket tm@(PPrimVal _ _) = tm
    bracket tm = PBracketed emptyFC tm
toStrUpdate _ = pure [] -- can't replace non user names

data UPD : Type where

||| Returns True if the SourcePart is a `Whitespace _` and False if not. Useful
||| for filtering or spanning a `List SourcPart`
isWhitespace : SourcePart -> Bool
isWhitespace (Whitespace _) = True
isWhitespace _              = False

||| Given a list of definitions, a list of mappings from `RawName` to `String`,
||| and a list of tokens to update, work out the updates to do, apply them, and
||| return the result.
doUpdates : {auto s : Ref Syn SyntaxInfo} ->
            {auto u : Ref UPD (List String)} ->
            Defs -> Updates -> List SourcePart ->
            Core (List SourcePart)
doUpdates defs ups [] = pure []   -- no more tokens to update, so we are done
-- if we have an LBrace (i.e. `{`), handle its contents
doUpdates defs ups (LBrace :: xs)
    -- the cases we care about are easy to detect w/o whitespace, so separate it
    = let (ws, nws) = span isWhitespace xs in
        case nws of
          -- handle potential whitespace in the other parts
          Name n :: rest =>
             let (ws', nws') = span isWhitespace rest in
               case nws' of
                  -- brace is immediately closed, so generate a new
                  -- pattern-match on the values the name can have, e.g.
                  -- { x}  where x : Nat would become { x = Z}
                  --                       (and later { x = (S k)})
                  RBrace :: rest' =>
                    pure (LBrace :: ws ++
                          Name n :: Whitespace " " :: Equal :: Whitespace " " ::
                          !(doUpdates defs ups (Name n :: ws' ++ RBrace :: rest'))
                          )
                  -- preserve whitespace before (and after) the Equal
                  Equal :: rest' =>
                    let (ws'', nws'') = span isWhitespace rest' in
                    pure (LBrace :: ws ++
                          Name n :: ws' ++ Equal :: ws'' ++
                          !(doUpdates defs ups nws'')
                          )
                  -- handle everything else as usual, preserving whitespace
                  _ => pure (LBrace :: ws ++ Name n :: ws' ++
                             !(doUpdates defs ups rest)
                             )
          -- not a special case: proceed as normal
          _ => pure (LBrace :: [] ++ !(doUpdates defs ups xs))
-- if we have a name that acts as an as-pattern then do not update it
doUpdates defs ups (Name n :: AsPattern :: xs)
    = pure $ Name n :: AsPattern :: !(doUpdates defs ups xs)
-- if we have a name, look up if it's a name we're updating. If it isn't, keep
-- the old name, otherwise update the name, i.e. replace with the new name
doUpdates defs ups (Name n :: xs)
    = case lookup n ups of
           Nothing => pure (Name n :: !(doUpdates defs ups xs))
           Just up => pure (Other up :: !(doUpdates defs ups xs))
-- if we have a hole, get the used names, generate+register a new unique name,
-- and change the hole's name to the new one
doUpdates defs ups (HoleName n :: xs)
    = do used <- get UPD
         n' <- uniqueHoleName defs used n
         put UPD (n' :: used)
         pure $ HoleName n' :: !(doUpdates defs ups xs)
-- if it's not a thing we update, leave it and continue working on the rest
doUpdates defs ups (x :: xs)
    = pure $ x :: !(doUpdates defs ups xs)

-- State here is a list of new hole names we generated (so as not to reuse any).
-- Update the token list with the string replacements for each match, and return
-- the newly generated strings.
updateAll : {auto s : Ref Syn SyntaxInfo} ->
            {auto u : Ref UPD (List String)} ->
            Defs -> List SourcePart -> List Updates ->
            Core (List String)
updateAll defs l [] = pure []
updateAll defs l (rs :: rss)
    = do l' <- doUpdates defs rs l
         rss' <- updateAll defs l rss
         pure (concatMap toString l' :: rss')

-- Turn the replacements we got from 'getSplits' into a list of actual string
-- replacements
getReplaces : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto o : Ref ROpts REPLOpts} ->
              List (Name, RawImp) -> Core Updates
getReplaces updates
    = do strups <- traverse toStrUpdate updates
         pure (concat strups)

showImpossible : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 {auto o : Ref ROpts REPLOpts} ->
                 (indent : Nat) -> RawImp -> Core String
showImpossible indent lhs
    = do clause <- pterm (map defaultKindedName lhs) -- hack
         pure (fastPack (replicate indent ' ') ++ show clause ++ " impossible")

||| What type of `case` block we're splitting:
||| - OneLine Nat
|||   ```
|||   f n = (case n of case_val => ?f_rhs)
|||   ```
|||   The `Nat` is the index of the "of" keyword
||| - HoleNameParen
|||   ```
|||   g n = (case n of
|||               case_val => ?g_rhs)
|||   ```
data CaseStmtType = Oneline Nat
                  | OnelineParen Nat
                  | HoleNameParen

||| Inspect the token list to see if it contains an interesting `case` block for
||| splitting, and if it does, determine the type of interesting `case` block
getCaseStmtType : (toks : List SourcePart) -> Maybe CaseStmtType
getCaseStmtType toks
  = let nws = filter (not . isWhitespace) toks in
        -- use SnocList of nws so we can express the pattern we're looking for
        -- as it would appear
        case Lin <>< nws of
             -- If the line ends with a right parenthesis followed by a
             -- `HoleName`, we're interested in what kind of `case` block it is
             start :< HoleName _ :< Other ")" =>
                  -- try to find the index of a `Name "of"` in the SnocList of
                  -- all tokens, including whitespace; if we don't find one, the
                  -- line must be a case hole on a new line, otherwise, it must
                  -- be a oneline case statement and the index let's us
                  -- calculate the indentation required!
                  case findIndex isNameOf (Lin <>< toks) of
                       Nothing => Just HoleNameParen
                       (Just skotOfIndex) =>
                            -- calculate the indentation, remembering that we
                            -- constructed a SnocList so the index is backwards
                            let ofIndex = minus (length toks) (finToNat skotOfIndex) in
                                Just $ OnelineParen (calcIndent ofIndex toks)
             -- If the line ends with a `HoleName`, check if its a oneline `case` block
             start :< HoleName _ =>
                  case findIndex isNameOf (Lin <>< toks) of
                       Nothing => Nothing
                       (Just skotOfIndex) =>
                            let ofIndex = minus (length toks) (finToNat skotOfIndex) in
                                Just $ Oneline (calcIndent ofIndex toks)
             -- If it doesn't, it's not a statement we're interested in
             _ => Nothing
    where
      isNameOf : SourcePart -> Bool
      isNameOf (Name "of") = True
      isNameOf _ = False

      calcIndent : Nat -> List SourcePart -> Nat
      calcIndent ofIndex toks
        = let (preOf, _) = splitAt ofIndex toks in
              foldr (\e,a => a + (length . toString) e) 0 preOf

||| Given a list of characters reprsenting an update string, drop its last
||| element.
dropLast : (updChars : List Char) -> List Char
dropLast updChars with (snocList updChars)
  dropLast [] | Empty = []
  dropLast (xs ++ [x]) | (Snoc x xs rec) = xs

||| Trim whitespace to the right of the string
rtrim : String -> String
rtrim = reverse . ltrim . reverse

||| Drop the closing parenthesis and any indentation preceding it.
parenTrim : String -> String
parenTrim = Idris.IDEMode.CaseSplit.rtrim . fastPack . dropLast . fastUnpack

||| Drop the number of letters equal to the indentation level to align
||| just after the `of`.
onelineIndent : Nat -> String -> String
onelineIndent indentation
  = (Data.String.indent indentation) . fastPack . (drop indentation) . fastUnpack

||| An unbracketed, oneline `case` block just needs to have the last updates
||| indented to lign up with the statement after the `of`.
handleOneline : (indentation : Nat) -> (upds : List String) -> List String
handleOneline indentation [] = []
handleOneline indentation (u :: us) = u :: ((onelineIndent indentation) <$> us)

||| A bracketed, oneline `case` block needs to have the parenthesis cut off the
||| first update; all the following updates, apart from the last, need to have
||| the parenthesis cut off and be indented rather than having the line
||| repeated; the final update only needs to be indented, but must preserve the
||| parenthesis from the original line that was split.
handleOnelineParen : (indentation : Nat) -> (upds : List String) -> List String
handleOnelineParen indentation upds with (snocList upds)
  handleOnelineParen indentation [] | Empty = []
  handleOnelineParen indentation (xs ++ [x]) | (Snoc x xs rec)
    = handleMiddle xs ++ [onelineIndent indentation x]
  where
    handleMiddle : (us : List String) -> List String
    handleMiddle [] = []
    handleMiddle (u :: us)
      = (parenTrim $ onelineIndent indentation u) :: handleMiddle us

||| A `HoleName` folled by a parenthesis needs to have the parenthesis removed
||| from every update apart from the final one.
handleHoleNameParen : (upds : List String) -> List String
handleHoleNameParen upds with (snocList upds)
  handleHoleNameParen [] | Empty = []
  handleHoleNameParen (xs ++ [x]) | (Snoc x xs rec) = map parenTrim xs ++ [x]

||| Given a list of updates and some information as to what kind of `case` block
||| needs handling, change the updates such that the result is syntactically
||| correct Idris.
handleCaseStmtType : (upds : List String) ->
                     (cst : CaseStmtType) ->
                     List String
handleCaseStmtType [] _ = []
handleCaseStmtType (u :: us) (Oneline indentation) = handleOneline indentation (u :: us)
handleCaseStmtType (u :: us) (OnelineParen indentation)
  = (parenTrim u) :: handleOnelineParen indentation us
handleCaseStmtType upds HoleNameParen = handleHoleNameParen upds

||| Given a list of updates and a line and column, find the relevant line in
||| the source file and return the lines to replace it with.
export
updateCase : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
             {auto o : Ref ROpts REPLOpts} ->
             List ClauseUpdate -> Int -> Int ->
             Core (List String)
updateCase splits line col
    = do opts <- get ROpts
         case mainfile opts of
              Nothing => throw (InternalError "No file loaded")
              Just f =>
                do Right file <- coreLift $ readFile f
                       | Left err => throw (FileErr f err)
                   let thisline = elemAt (forget $ lines file) (integerToNat (cast line))
                   case thisline of
                        Nothing => throw (InternalError "File too short!")
                        Just l =>
                            do let valid = mapMaybe getValid splits
                               let bad = mapMaybe getBad splits
                               log "interaction.casesplit" 3 $ "Valid: " ++ show valid
                               log "interaction.casesplit" 3 $ "Bad: " ++ show bad
                               if isNil valid
                                  then do let indent = getIndent 0 $ fastUnpack l
                                          traverse (showImpossible indent) bad
                                  else do rs <- traverse getReplaces valid
                                          let stok = tokens l
                                          defs <- get Ctxt
                                          u <- newRef UPD []
                                          upds <- updateAll defs stok rs
                                          pure $ case getCaseStmtType stok of
                                                      Nothing => upds
                                                      (Just cst) =>
                                                          handleCaseStmtType upds cst
  where
    getValid : ClauseUpdate -> Maybe (List (Name, RawImp))
    getValid (Valid _ ups) = Just ups
    getValid _ = Nothing

    getBad : ClauseUpdate -> Maybe RawImp
    getBad (Impossible lhs) = Just lhs
    getBad _ = Nothing

    getIndent : (acc : Nat) -> List Char -> Nat
    getIndent acc [] = acc
    getIndent acc (' ' :: xs) = getIndent (acc + 1) xs
    getIndent acc _ = acc

fnName : Bool -> Name -> String
fnName lhs (UN (Basic n))
    = if isIdentNormal n then n
      else if lhs then "(" ++ n ++ ")"
      else "op"
fnName lhs (NS _ n) = fnName lhs n
fnName lhs (DN s _) = s
fnName lhs n = nameRoot n

export
getClause : {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto o : Ref ROpts REPLOpts} ->
            Int -> Name -> Core (Maybe String)
getClause l n
    = do defs <- get Ctxt
         Just (loc, nidx, envlen, ty) <- findTyDeclAt (\p, n => onLine (l-1) p)
             | Nothing => pure Nothing
         n <- getFullName nidx
         argns <- getEnvArgNames defs envlen !(nf defs [] ty)
         Just srcLine <- getSourceLine l
           | Nothing => pure Nothing
         let (mark, src) = isLitLine srcLine
         pure (Just (indent mark loc ++ fnName True n ++ concat (map (" " ++) argns) ++
                  " = ?" ++ fnName False n ++ "_rhs"))
  where
    indent : Maybe String -> NonEmptyFC -> String
    indent (Just mark) fc
        = relit (Just mark) $ pack (replicate (integerToNat (cast (max 0 (snd (startPos fc) - 1)))) ' ')
    indent Nothing fc = pack (replicate (integerToNat (cast (snd (startPos fc)))) ' ')


text:
module Data.Prim.Bits8

import public Control.WellFounded
import public Data.DPair
import public Data.Prim.Ord
import public Algebra.Solver.Ring
import Syntax.PreorderReasoning

%default total

unsafeRefl : a === b
unsafeRefl = believe_me (Refl {x = a})

--------------------------------------------------------------------------------
--          (<)
--------------------------------------------------------------------------------

||| Witness that `m < n === True`.
export
data (<) : (m,n : Bits8) -> Type where
  LT : {0 m,n : Bits8} -> (0 prf : (m < n) === True) -> m < n

||| Contructor for `(<)`.
|||
||| This can only be used in an erased context.
export %hint
0 mkLT : (0 prf : (m < n) === True) -> m < n
mkLT = LT

||| Extractor for `(<)`.
|||
||| This can only be used in an erased context.
export
0 runLT : m < n -> (m < n) === True
runLT (LT prf) = prf

||| We don't trust values of type `(<)` too much,
||| so we use this when creating magical results.
export
strictLT : (0 p : m < n) -> Lazy c -> c
strictLT (LT prf) x = x

--------------------------------------------------------------------------------
--          Aliases
--------------------------------------------------------------------------------

||| Flipped version of `(<)`.
public export
0 (>) : (m,n : Bits8) -> Type
m > n = n < m

||| `m <= n` mean that either `m < n` or `m === n` holds.
public export
0 (<=) : (m,n : Bits8) -> Type
m <= n = Either (m < n) (m === n)

||| Flipped version of `(<=)`.
public export
0 (>=) : (m,n : Bits8) -> Type
m >= n = n <= m

||| `m /= n` mean that either `m < n` or `m > n` holds.
public export
0 (/=) : (m,n : Bits8) -> Type
m /= n = Either (m < n) (m > n)

--------------------------------------------------------------------------------
--          Order
--------------------------------------------------------------------------------

0 ltNotEQ : m < n -> Not (m === n)
ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")

0 ltNotGT : m < n -> Not (n < m)
ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")

0 eqNotLT : m === n -> Not (m < n)
eqNotLT = flip ltNotEQ

export
comp : (m,n : Bits8) -> Trichotomy (<) m n
comp m n = case prim__lt_Bits8 m n of
  0 => case prim__eq_Bits8 m n of
    0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
    x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)

export
Total Bits8 (<) where
  trichotomy   = comp
  transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl

--------------------------------------------------------------------------------
--          Bounds and Well-Foundedness
--------------------------------------------------------------------------------

||| Lower bound of `Bits8`
public export
MinBits8 : Bits8
MinBits8 = 0

||| Upper bound of `Bits8`
public export
MaxBits8 : Bits8
MaxBits8 = 0xff

||| `m >= 0` for all `m` of type `Bits8`.
export
0 GTE_MinBits8 : (m : Bits8) -> m >= MinBits8
GTE_MinBits8 m = case comp MinBits8 m of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total $ idris_crash "IMPOSSIBLE: Bits8 smaller than 0"

||| Not value of type `Bits8` is less than zero.
export
0 Not_LT_MinBits8 : m < 0 -> Void
Not_LT_MinBits8 = GTE_not_LT (GTE_MinBits8 m)

||| `m <= MaxBits8` for all `m` of type `Bits8`.
export
0 LTE_MaxBits8 : (m : Bits8) -> m <= MaxBits8
LTE_MaxBits8 m = case comp m MaxBits8 of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total
            $ idris_crash "IMPOSSIBLE: Bits8 greater than \{show MaxBits8}"

||| Not value of type `Bits8` is greater than `MaxBits8`.
export
0 Not_GT_MaxBits8 : m > MaxBits8 -> Void
Not_GT_MaxBits8 = LTE_not_GT (LTE_MaxBits8 m)

||| Every value of type `Bits8` is accessible with relation
||| to `(<)`.
export
accessLT : (m : Bits8) -> Accessible (<) m
accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)

||| `(<)` is well founded.
export %inline
WellFounded Bits8 (<) where
  wellFounded = accessLT

||| Every value of type `Bits8` is accessible with relation
||| to `(>)`.
export
accessGT : (m : Bits8) -> Accessible (>) m
accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)

||| `(>)` is well founded.
export %inline
[GT] WellFounded Bits8 (>) where
  wellFounded = accessGT

--------------------------------------------------------------------------------
--          Arithmetics
--------------------------------------------------------------------------------

||| Safe division.
|||
||| This uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
export %inline
sdiv : (n,d : Bits8) -> (0 prf : 0 < d) => Bits8
sdiv n d = n `div` d

||| Refined division.
|||
||| This comes with a proof that the result is
||| strictly smaller than `n`.
|||
||| This uses `0 < n` as a constraint instead
||| of `0 /= n`, because in my experience, the former
||| is much more useful.
export %inline
rdiv :  (n,d : Bits8)
     -> (0 dgt1 : 1 < d)
     => (0 ngt0 : 0 < n)
     => Subset Bits8 (< n)
rdiv n d = Element (n `div` d) (LT unsafeRefl)

||| Safe modulo.
|||
||| This uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
|||
||| If you need the postcondition that the result is strictly
||| smaller than `d`, use `rmod` instead.
export %inline
smod : (n,d : Bits8) -> (0 prf : 0 < d) => Bits8
smod n d = n `mod` d

||| Refined modulo.
|||
||| This comes with a proof that the result is strictly smaller
||| than `d`.
|||
||| It uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
export %inline
rmod : (n,d : Bits8) -> (0 prf : 0 < d) => Subset Bits8 (< d)
rmod n d = Element (n `mod` d) (LT unsafeRefl)


text:
module BoundedNat
import Data.Fin
import NatHelpers
-- Bounded Nats, Nats which are LTE than the upper bound

%default total

public export
data BoundedNat : (bound : Nat) -> Type where
  Val : (n : Nat) -> (ok : LTE n bound) -> BoundedNat bound

export
MkUpperBound : (b : Nat) -> BoundedNat b
MkUpperBound Z = Val Z LTEZero
MkUpperBound (S k) = Val (S k) (LTESucc lteRefl)

export
weakenBound : BoundedNat b -> BoundedNat (S b)
weakenBound (Val n ok) = Val n (lteRightSucc ok)

export
weakenBoundN : (n : Nat) -> BoundedNat b -> BoundedNat (b + n)
weakenBoundN k (Val n ok) = Val n (lteRightPlus ok)

||| Add a nat to a boundednat, either the sum it out of bound and the excess is returned as Left. Or the new bounded value is returned as right
export boundedAdd : BoundedNat b -> Nat -> Either Nat (BoundedNat b)
boundedAdd bounded Z = Right bounded
boundedAdd bounded (S k) {b = Z} = Left (S k)
boundedAdd (Val n ok) (S j) {b = (S k)} with (isLTE n k)
  boundedAdd (Val n ok) (S j) {b = (S k)} | (Yes prf) = let p = LTESucc prf in
                                                            boundedAdd (Val (S n) p) j
  boundedAdd (Val n ok) (S j) {b = (S k)} | (No contra) = Left (S j)

||| the predecessor of l in l <= r is also smaller than r
export lteLeftSucc : LTE (S j) k -> LTE j k
lteLeftSucc (LTESucc LTEZero) = LTEZero
lteLeftSucc (LTESucc (LTESucc x)) = LTESucc (lteLeftSucc (LTESucc x))

||| subtract a bounded nat by a Nat, the result is within bounds,
export subtractBounded : BoundedNat k -> Nat -> BoundedNat k
subtractBounded x Z = x
subtractBounded (Val Z ok) (S k) = Val Z ok
subtractBounded (Val (S j) ok) (S k) = subtractBounded (Val j (lteLeftSucc ok)) k

export
boundPlusRight : (value : Nat) -> BoundedNat (value + more)
boundPlusRight value = Val value (lteRightPlusNat value)

export
addBounded : BoundedNat b -> Nat -> BoundedNat b
addBounded x k with (boundedAdd x k)
  addBounded x k | (Left l) {b} = MkUpperBound b
  addBounded x k | (Right r) = r


text:
module Diff

sub: (n: Nat) -> (m: Nat) -> (LTE m n) -> Nat
sub n Z LTEZero = n
sub (S right) (S left) (LTESucc x) = sub right left x

rl: (n: Nat) -> LTE n n
rl Z = LTEZero
rl (S k) = LTESucc (rl k)

rs: (n: Nat) -> LTE n (S n)
rs Z = LTEZero
rs (S k) = LTESucc (rs k)

zm : (n: Nat) -> LTE n 0 -> n = 0
zm Z LTEZero = ?zm_rhs_1

es: (n: Nat) -> (m: Nat) -> (n = m) -> S n = S m
es m m Refl = Refl

ans : (n: Nat) -> (m: Nat) -> (LTE n m) -> (LTE m n) -> n = m
ans Z Z LTEZero LTEZero = Refl
ans (S a) (S b) (LTESucc x) (LTESucc y) = es a b (ans a b x y)

contra: (1 = 2) -> Void
contra Refl impossible

data IsEven : Nat -> Type where
  ZeroEven : IsEven 0
  PlusTwo : (n: Nat) -> IsEven n -> IsEven (S (S n))

twoEven : IsEven 2
twoEven = PlusTwo 0 ZeroEven

oneOdd : (IsEven 1) -> Void
oneOdd ZeroEven impossible
oneOdd (PlusTwo _ _) impossible

one: Nat
one = 1

threeOdd : (IsEven 3) -> Void
threeOdd (PlusTwo (S Z) ZeroEven) impossible
threeOdd (PlusTwo (S Z) (PlusTwo _ _)) impossible

thmEven : (n: Nat) -> Either (IsEven n) (IsEven (S n))
thmEven Z = Left ZeroEven
thmEven (S k) = case thmEven k of
                     (Left l) => Right (PlusTwo k l)
                     (Right r) => Left r

divTwo: (n: Nat) -> IsEven n -> Nat
divTwo Z ZeroEven = 0
divTwo (S (S k)) (PlusTwo k x) = S (divTwo k x)


text:
-- DepPairs.idr

-- Demonstrates dependendent pairs by reading
-- 2 Vect of variable length
-- and zip them together

import Data.Vect

||| Reads a Vect of unknown length
readVect : IO (len ** Vect len String)
readVect = do
  x <- getLine
  if x == ""
     then pure (_ ** [])
     else do (_ ** xs) <- readVect
             pure (_ ** x :: xs)

||| Zip to Vect of unknown length
zipInputs : IO ()
zipInputs = do putStrLn "Enter first vector (blank line to end):"
               (len1 ** vec1) <- readVect
               putStrLn "Enter second vector (blank line to end):"
               (len2 ** vec2) <- readVect
               case exactLength len1 vec2 of
                    Nothing => putStrLn "Vectors have different length"
                    Just vec2' => printLn (zip vec1 vec2')

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Main

import Cairo

data Clist a = Nil | (::) a (Clist a)

clength : Clist a -> Felt
clength Nil = 0
clength (_::as) = 1 + clength as

cfoldl : (a -> e -> a) -> a -> Clist e -> a
cfoldl _ acc Nil = acc
cfoldl f acc (e::es) = cfoldl f (f acc e) es

export
hashChain' : (l: Clist Felt) -> Felt
hashChain' l = cfoldl pedersenHash (clength l) l

%noinline
main : Cairo ()
main = output (hashChain' [1,2,3,4,5,6,7,8,9,10])

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module OfficialCrashCourse.VTypes

import Data.Vect

-- Shows use of view types
%hide Data.Vect.filter
%hide Data.Maybe.filter

filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter p Nil = ?somethings
filter p (x :: xs) with (filter p xs)
    filter p (x :: xs) | (_ ** xs') = if (p x) then (_ ** x :: xs') else (_ ** xs')

max_stars_repo_name: umbrela-academy/idrusti

max_issues_repo_name: umbrela-academy/idrusti

max_forks_repo_name: umbrela-academy/idrusti


text:
-- %language FirstClassReflection
-- %default total
%reflection

ups : Nat -> Nat
ups (S k) = k


text:
module Map

import Data.List
import Data.Maybe
import Data.Nat

%default total

iff : (p, q : Type) -> Type
iff p q = (p -> q, q -> p)

iff_sym : iff p q -> iff q p
iff_sym (x, y) = (y, x)

functional_extensionality : ((x : a) -> f x = g x) -> f = g
functional_extensionality = believe_me

public export
data Reflect : (p: Type) -> (b: Bool) -> Type where
    ReflectT : p -> (b=True) -> Reflect p b
    ReflectF : (Not p) -> (b=False) -> Reflect p b

iff_reflect : (b : Bool) -> iff p (b = True) -> Reflect p b
iff_reflect False (x, y) = ReflectF (uninhabited . x) Refl
iff_reflect True (x, y) = ReflectT (y Refl) Refl

reflect_iff : (b : Bool) -> Reflect p b -> iff p (b = True)
reflect_iff False (ReflectT _ Refl) impossible
reflect_iff False (ReflectF f prf) = (\p => void (f p), \p => void (uninhabited p))
reflect_iff True (ReflectT x prf) = (\p => prf, \Refl => x)
reflect_iff True (ReflectF _ Refl) impossible

public export
beq_bool : (b : Bool) -> b == b = True
beq_bool False = Refl
beq_bool True = Refl

public export
eq_bool : (b1, b2 : Bool) -> b1 == b2 = True -> b1 = b2
eq_bool False False _ = Refl
eq_bool False True Refl impossible
eq_bool True False Refl impossible
eq_bool True True _ = Refl

public export
neq_bool : (b1, b2 : Bool) -> b1 == b2 = False -> Not (b1 = b2)
neq_bool False False prf = absurd $ prf
neq_bool False True prf = uninhabited
neq_bool True False prf = uninhabited
neq_bool True True prf = absurd $ prf

public export
inv_bool : (b1, b2 : Bool) -> b1 = (not b2) -> b2 = (not b1)
inv_bool False False Refl impossible
inv_bool False True _ = Refl
inv_bool True False _ = Refl
inv_bool True True Refl impossible

public export
and_split : (a : Bool) -> (b : Lazy Bool) -> a && b = True -> (a = True, b = True)
and_split False (Delay b) prf = absurd prf
and_split True (Delay b) prf = (Refl, prf)

public export
and_join : (a = True, b = True) -> a && b = True
and_join (x, y) = rewrite x in rewrite y in Refl

public export
and_join2 : a = False -> a && _ = False
and_join2 prf = rewrite prf in Refl

public export
tuple_eq : (a, b) = (c, d) -> Not (c = d) -> Not (a = b)
tuple_eq prf f prf1 =
    let
        ac = cong fst prf
        bd = cong snd prf
    in f (rewrite sym ac in rewrite sym bd in prf1)

-- Maybe utils
public export
it_is_just : (a : Maybe b) -> (a = Just c) -> IsJust a
it_is_just Nothing Refl impossible
it_is_just (Just x) prf = ItIsJust

public export
contra : IsJust a -> a = Nothing -> Void
contra ItIsJust Refl impossible

-- Nat utils
public export
beq_nat : (n : Nat) -> n == n = True
beq_nat 0 = Refl
beq_nat (S k) = beq_nat k

public export
eq_nat : (n1, n2 : Nat) -> n1 == n2 = True -> n1 = n2
eq_nat 0 0 prf = Refl
eq_nat 0 (S _) Refl impossible
eq_nat (S _) 0 Refl impossible
eq_nat (S k) (S j) prf =
    let ind = eq_nat k j prf in
        rewrite ind in Refl

public export
neq_nat : (n1, n2 : Nat) -> n1 == n2 = False -> Not (n1 = n2)
neq_nat 0 0 prf = absurd prf
neq_nat 0 (S k) Refl = uninhabited
neq_nat (S k) 0 Refl = uninhabited
neq_nat (S k) (S j) prf =
    let ind = neq_nat k j prf in
        \p => ind $ cong pred p

beq_natP : (n, m : Nat) -> Reflect (n = m) (n == m)
beq_natP n m with (n == m) proof h
    beq_natP n m | False = ReflectF (neq_nat n m h) Refl
    beq_natP n m | True = ReflectT (eq_nat n m h) Refl

-- String utils
public export
beq_str : (s : List Char) -> s == s = True
beq_str s = believe_me s

public export
eq_str : (s1, s2 : List Char) -> s1 == s2 = True -> s1 = s2
eq_str s1 s2 prf = believe_me prf

public export
neq_str : (s1, s2 : List Char) -> s1 == s2 = False -> Not (s1 = s2)
neq_str s1 s2 prf = believe_me prf

-- Key
public export
data Key : Type where
    MkKey : Nat -> Key

%name Key k, k1, k2

key_to_nat : Key -> Nat
key_to_nat (MkKey n) = n

public export
Eq Key where
    MkKey a == MkKey b = a == b

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

public export
beq_key : (k: Key) -> k == k = True
beq_key (MkKey n) = beq_nat n

public export
bne_key : (k1, k2 : Key) -> k1 == k2 = False -> Not (k1 = k2)
bne_key (MkKey k) (MkKey j) prf prf1 =
    neq_nat k j prf (cong key_to_nat prf1)

public export
ne_key : (k1, k2 : Key) -> Not (k1 = k2) -> k1 == k2 = False
ne_key (MkKey k) (MkKey j) with (beq_natP k j)
    ne_key (MkKey k) (MkKey j) | (ReflectT x prf) = \a => void $ a $ cong MkKey x
    ne_key (MkKey k) (MkKey j) | (ReflectF f prf) = \a => prf

public export
beq_keyP : (n, m : Key) -> Reflect (n = m) (n == m)
beq_keyP (MkKey k) (MkKey j) with (beq_natP k j)
    beq_keyP (MkKey k) (MkKey j) | (ReflectT x prf) = ReflectT (cong MkKey x) prf
    beq_keyP (MkKey k) (MkKey j) | (ReflectF f prf) = ReflectF (\p => f (cong key_to_nat p)) prf

public export
data Map : Type -> Type where
    Empty : Map a
    Update : Key -> Maybe a -> Map a -> Map a

%name Map m, m1, m2

public export
Uninhabited (Empty = Update k v m) where
    uninhabited Refl impossible

public export
Uninhabited (Update k v m = Empty) where
    uninhabited Refl impossible

public export
empty : Map a
empty = Empty

public export
update : Key -> Maybe a -> Map a -> Map a
update k v m = Update k v m

public export
insert : Key -> a -> Map a -> Map a
insert k v m = update k (Just v) m

public export
remove : Key -> Map a -> Map a
remove k m = update k Nothing m

public export
get : Key -> Map a -> Maybe a
get k Empty = Nothing
get k (Update k' v' m') = if k == k' then v' else get k m'

public export
contains : Key -> Map a -> Bool
contains k m = isJust $ get k m

public export
half_eq : Eq a => Map a -> Map a -> Bool
half_eq Empty _ = True
half_eq (Update k v m') m2 = get k m2 == v

public export
Eq a => Eq (Map a) where
    x == y = half_eq x y && half_eq y x

public export
keys : Map a -> List Key
keys m = filter (\k => contains k m) (all_keys m) where
    all_keys : Map a  -> List Key
    all_keys Empty = []
    all_keys (Update k _ m) = k :: all_keys m

public export
contains_all : List Key -> Map a -> Bool
contains_all [] m = True
contains_all (x :: xs) m = contains x m && contains_all xs m

public export
half_keys_eq : Map a -> Map b -> Bool
half_keys_eq m1 m2 = contains_all (keys m1) m2

public export
keys_eq : Map a -> Map b -> Bool
keys_eq m1 m2 = half_keys_eq m1 m2 && half_keys_eq m2 m1

-- Contains theorems
public export
get_just_contains : get k m = Just _ -> contains k m = True
get_just_contains prf = rewrite prf in Refl

public export
get_nothing_contains : get k m = Nothing -> contains k m = False
get_nothing_contains prf = rewrite prf in Refl

-- Get theorems
public export
get_neq : Not (get a m = get b m) -> Not (a = b)
get_neq f prf = f (cong (\k => get k m) prf)

-- Update theorems
public export
map_extensionality : (m1, m2 : Map a) -> ((k : Key) -> get k m1 = get k m2) -> m1 = m2
map_extensionality = \m1, m2, f => believe_me (Refl {x = MkUnit})

public export
update_eq : (m : Map a) -> (k : Key) -> (v : Maybe a) -> get k (update k v m) = v
update_eq m k v = rewrite beq_key k in Refl

public export
update_neq : (m : Map a) -> (k1, k2 : Key) -> (v : Maybe a) -> Not (k1 = k2) -> (get k2 $ update k1 v m) = get k2 m
update_neq m k1 k2 v f with (beq_keyP k2 k1)
    update_neq m k1 k2 v f | (ReflectT x prf) = void $ f $ sym x
    update_neq m k1 k2 v f | (ReflectF g prf) = rewrite prf in Refl

public export
update_shadow : (m : Map a) -> (k : Key) -> (v1, v2 : Maybe a) -> (update k v2 $ update k v1 m) = update k v2 m
update_shadow m k v1 v2 = map_extensionality (update k v2 $ update k v1 m) (update k v2 m) $ \k' =>
    case beq_keyP k' k of
        ReflectT t prf => rewrite prf in Refl
        ReflectF f prf => rewrite prf in rewrite prf in Refl

public export
update_same : (m : Map a) -> (k : Key) -> (v : Maybe a) -> (get k m = v) -> update k v m = m
update_same m k v prf = map_extensionality (update k v m) m  $ \k' =>
    case beq_keyP k' k of
        ReflectT t prf1 => rewrite prf1 in rewrite t in rewrite prf in Refl
        ReflectF f prf1 => rewrite prf1 in Refl

public export
update_permute : (m : Map a) -> (k1, k2 : Key) -> (v1, v2 : Maybe a) -> Not (k1 = k2) ->
    (update k1 v1 $ update k2 v2 m) = (update k2 v2 $ update k1 v1 m)
update_permute m k1 k2 v1 v2 prf = map_extensionality
    (update k1 v1 $ update k2 v2 m) (update k2 v2 $ update k1 v1 m) $ \k' =>
    case (beq_keyP k' k1, beq_keyP k' k2) of
        (ReflectT x _, ReflectT y _) =>
                void $ prf $ rewrite sym x in rewrite sym y in Refl
        (ReflectT _ prf1, ReflectF _ prf2) =>
            rewrite prf1 in rewrite prf2 in rewrite prf1 in Refl
        (ReflectF _ prf1, ReflectT _ prf2) =>
            rewrite prf1 in rewrite prf2 in Refl
        (ReflectF _ prf1, ReflectF _ prf2) =>
            rewrite prf1 in rewrite prf2 in rewrite prf1 in Refl

-- Half keys equality theorems
InMap : (k : Key) -> (m : Map a) -> Type
InMap k Empty = Void
InMap k (Update k' v' m') = Either (k = k', IsJust v') (Not (k = k'), InMap k m')

containsP : (k : Key) -> (m : Map a) -> Reflect (InMap k m) (contains k m)
containsP k Empty = ReflectF id Refl
containsP k (Update k' v' m') with (beq_keyP k k')
    containsP k (Update k' Nothing m') | ReflectT keq prf =
        rewrite prf in ReflectF (\f => case f of
            Left (_, f) => absurd f
            Right (f, _) => f keq) Refl
    containsP k (Update k' (Just v) m') | ReflectT keq prf =
        rewrite prf in ReflectT (Left (keq, ItIsJust)) Refl
    containsP k (Update k' v' m') | ReflectF f prf with (containsP k m')
        containsP k (Update k' v' m') | ReflectF f prf | ReflectT t prf1 =
            rewrite prf in ReflectT (Right (f, t)) prf1
        containsP k (Update k' v' m') | ReflectF f prf | ReflectF f' prf1 =
            rewrite prf in ReflectF (\p => case p of
                Left (p, _) => f p
                Right (_, p) => f' p) prf1

insert_contains : (k : Key) -> (v : a) -> (m : Map a) -> contains k (insert k v m) = True
insert_contains k v m = rewrite beq_key k in Refl

remove_contains : (k : Key) -> (m : Map a) -> contains k (remove k m) = False
remove_contains k m = rewrite beq_key k in Refl

contains_all_insert : (ks : List Key) -> (m : Map a) -> (k : Key) -> (v : a) ->
    contains_all ks m = True -> contains_all ks (insert k v m) = True
contains_all_insert [] _ _ _ _ = Refl
contains_all_insert (k :: ks) m k' v prf with (k == k')
    contains_all_insert (k :: ks) m k' v prf | False =
        let split = and_split (contains k m) (contains_all ks m) prf
            ind = contains_all_insert ks m k' v (snd split)
        in rewrite ind in rewrite fst split in Refl
    contains_all_insert (k :: ks) m k' v prf | True =
        let split = and_split (contains k m) (contains_all ks m) prf
            ind = contains_all_insert ks m k' v (snd split)
        in rewrite ind in Refl

contains_all_key : (ks : List Key) -> (m : Map a) -> (k : Key) -> contains k m = True ->
    contains_all ks m = True -> contains_all (k :: ks) m = True
contains_all_key ks m k prf prf1 = rewrite prf in rewrite prf1 in Refl

contains_all_key_insert : (ks : List Key) -> (m : Map a) -> (k : Key) -> (v : a) ->
    contains_all ks m = True -> contains_all (k :: ks) (insert k v m) = True
contains_all_key_insert ks m k v prf =
    let p = contains_all_insert ks m k v prf
        p' = contains_all_key ks (insert k v m) k (insert_contains k v m) p
    in p'

-- actually not true
keys_insert : (ks : List Key) -> (m : Map a) -> (k : Key) -> (v : a) ->
    keys m = ks -> keys (insert k v m) = k :: ks

public export
half_keys_eq_insert : (am : Map a) -> (bm : Map b) ->
    (k : Key) -> (av : a) -> (bv : b) ->
    half_keys_eq am bm = True -> half_keys_eq (insert k av am) (insert k bv bm) = True
half_keys_eq_insert am bm k av bv prf =
    let ki = keys_insert (keys am) am k av Refl
        p = contains_all_key_insert (keys am) bm k bv prf
    in rewrite ki in p

{-half_keys_eq_remove_right : (am : Map a) -> (bm : Map b) -> (k : Key) ->
    NotInMap k am -> half_keys_eq am bm = True -> half_keys_eq am (remove k bm) = True

half_keys_eq_remove_left : (am : Map a) -> (bm : Map b) -> (k : Key) ->
    half_keys_eq am bm = True -> half_keys_eq (remove k am) bm = True-}

public export
half_keys_eq_remove : (am : Map a) -> (bm : Map b) -> (k : Key) ->
    half_keys_eq am bm = True -> half_keys_eq (remove k am) (remove k bm) = True
{-half_keys_eq_remove am bm k prf =
    let left = half_keys_eq_remove_left am bm k prf
        right = half_keys_eq_remove_right (remove k am) bm k (remove_contains k am) left
    in right-}

public export
not_half_keys_eq : (am : Map a) -> (bm : Map b) -> (k : Key) ->
    contains k am = True -> contains k bm = False -> half_keys_eq am bm = False

max_stars_repo_name: Actyx/cambria

max_issues_repo_name: Actyx/cambria

max_forks_repo_name: Actyx/cambria


text:
module Libraries.Data.List.Extra

import public Data.List
import Data.List1

%default total

export
minimum : Ord a => (xs : List a) -> {auto 0 _ : NonEmpty xs} -> a
minimum (x :: xs) = foldl min x xs

||| Fetches the element at a given position.
||| Returns `Nothing` if the position beyond the list's end.
public export
elemAt : List a -> Nat -> Maybe a
elemAt []        _     = Nothing
elemAt (l :: _)  Z     = Just l
elemAt (_ :: ls) (S n) = elemAt ls n

export
findBy : (a -> Maybe b) -> List a -> Maybe b
findBy p [] = Nothing
findBy p (x :: xs)
  = case p x of
      Nothing => findBy p xs
      Just win => pure win

export
breakAfter : (a -> Bool) -> List a -> (List a, List a)
breakAfter p [] = ([], [])
breakAfter p (x::xs)
    = if p x
         then ([x], xs)
         else let (ys, zs) = breakAfter p xs in (x::ys, zs)

export
splitAfter : (a -> Bool) -> List a -> List1 (List a)
splitAfter p xs
    = case breakAfter p xs of
           (chunk, []) => singleton chunk
           (chunk, rest@(_::_)) => cons chunk (splitAfter p (assert_smaller xs rest))

export
zipMaybe : List a -> List b -> Maybe (List (a, b))
zipMaybe [] [] = pure []
zipMaybe (a::as) (b::bs) = ((a, b) ::) <$> zipMaybe as bs
zipMaybe _ _ = Nothing

export
findBy' : (a -> Bool) -> List a -> (List a, Maybe a, List a)
findBy' f [] = ([], Nothing, [])
findBy' f (x :: xs) =
  case f x of
    True  => ([], Just x, xs)
    False =>
      let (pre, mb, post) = findBy' f xs in
      (x :: pre, mb, post)

||| Compute the difference of two lists by the given predicate.
||| Lists are treated as bags.
export
diffBy : (a -> a -> Bool)
      -> List a
      -> List a
      -> List a
diffBy f [] ys = []
diffBy f (x :: xs) ys =
  let whole@(pre, mb, post) = findBy' (f x) ys
      ys' = pre ++ post in
  case mb of
    Just _  =>      diffBy f xs ys'
    Nothing => x :: diffBy f xs ys'

||| Remove adjacent duplicates
export
dedup : Eq a => List a -> List a
dedup (a :: xs@(b :: _)) = if a == b then dedup xs else a :: dedup xs
dedup xs                = xs

||| O(n * log(n)). Sort a list and remove duplicates
export
sortedNub : Ord a => List a -> List a
sortedNub = dedup . sort

||| TODO: use the version in `Data.List1` in base after the next release.
export
groupBy : (a -> a -> Bool) -> List a -> List (List1 a)
groupBy _ [] = []
groupBy eq (h :: t) = let (ys,zs) = go h t
                       in ys :: zs

  where go : a -> List a -> (List1 a, List (List1 a))
        go v [] = (singleton v,[])
        go v (x :: xs) = let (ys,zs) = go x xs
                          in if eq v x
                                then (cons v ys, zs)
                                else (singleton v, ys :: zs)

||| TODO: use the version in `Data.List1` in base after the next release.
export
group : Eq a => List a -> List (List1 a)
group = Libraries.Data.List.Extra.groupBy (==)

||| TODO: use the version in `Data.List1` in base after the next release.
export
groupWith : Eq b => (a -> b) -> List a -> List (List1 a)
groupWith f = Libraries.Data.List.Extra.groupBy (\x,y => f x == f y)

||| TODO: use the version in `Data.List1` in base after the next release.
export
groupAllWith : Ord b => (a -> b) -> List a -> List (List1 a)
groupAllWith f = Libraries.Data.List.Extra.groupWith f . sortBy (comparing f)


text:
module TyTTP.HTTP.Combinators

import Control.Monad.Trans
import Data.Buffer
import Data.Buffer.Ext
import Data.Maybe
import Data.SnocList
import Data.IORef
import TyTTP
import TyTTP.HTTP

||| This function consumes the stream from the underlying server, thus the original stream cannot be used twice.
||| If you make sure that the original stream is not used twice, then this function can be used.
export
unsafeConsumeBody : Error e
  => HasIO m
  => (
    Step Method u h1 s h2 Buffer b
    -> Promise e m $ Step Method u' h1' s' h2' a' b'
  )
  -> Step Method u h1 s h2 (Publisher m e Buffer) b
  -> Promise e m $ Step Method u' h1' s' h2' a' b'
unsafeConsumeBody handler step = MkPromise $ \cb => do
  acc <- newIORef Lin
  let handlerCallbacks = MkCallbacks
        { onSucceded = cb.onSucceded
        , onFailed = cb.onFailed
        }
      subscriber : Subscriber m e Buffer = MkSubscriber
        { onNext = \a => modifyIORef acc (:< a)
        , onSucceded = \_ => do
            all <- concatBuffers =<< asList <$> readIORef acc
            emptyBuffer <- Ext.newBuffer 0
            let result = handler $ { request.body := fromMaybe emptyBuffer all } step
            result.continuation handlerCallbacks
        , onFailed = cb.onFailed
        }
  step.request.body.subscribe subscriber

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Main

data TestData = Con1 (List TestData) String (List (List Int))
    | Con2 ((Int, Int), String)

func : TestData -> Bool -> String
func (Con1 [] x []) False = x ++ "p1"
func (Con1 [] x ([] :: xs)) False = x ++ "p2"
func (Con1 [] x ((y :: ys) :: [])) False = x ++ "p3"
func (Con1 [] x ((y :: ys) :: (z :: xs))) False = x ++ "p4"
func (Con1 ((Con1 zs y ws) :: xs) x ys) False = x ++ "p5"
func (Con1 ((Con2 y) :: xs) x ys) False = x ++ "p6"
func (Con2 ((a,c), b)) False = b ++ "p7"
func (Con1 (x :: xs) y _) True = "super"
func (Con1 [] y _) True = "supertare"
func _ True = "defacto"

t1 : TestData
t1 = Con1 [] "t1" [[]]

ptrStr : Bool -> String -> String
ptrStr False "asd" = reverse "asd"
ptrStr x "2"   = "22"
ptrStr _ _     = reverse "asdauysgdansd"

ptrFlt : Bool -> Double -> String
ptrFlt False 3.14 = reverse "asd"
ptrFlt x 2.11   = "22"
ptrFlt _ _     = reverse "asdauysgdansd"

abcd : Integer -> String
abcd 300040000200 = "WOW"
abcd _      = "NOWOW"

main : IO ()
main = do
     putStrLn $ func t1 False
     putStrLn $ func (Con1 [] "t2" []) False
     putStrLn $ func t1 True
     x <- getLine
     putStrLn $ ptrStr False x
     putStrLn $ ptrFlt False 3.14
     putStrLn $ ptrFlt False 2.11
     if (2.11 == (cast x)) then putStrLn "hey" else putStrLn "x"
    --  putStrLn $ ptrFlt True (cast x - 0.01)
     y <- getLine
     putStrLn $ abcd (cast y)
     putStrLn $ abcd (cast y)

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module Minecraft.Data.Type.Ctx

%default total

public export
record Ctx kind where
  constructor (#)
  type : Type
  {auto impl : kind type}

public export
record Impl kind (type : Type) where
  constructor Inst
  {auto impl : kind type}

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
-- https://www.codewars.com/kata/50654ddff44f800200000004

module Multiply

%access export
%default total

multiply : Int -> Int -> Int
multiply a b = a * b

max_stars_repo_name: hiljusti/codewars-solutions

max_issues_repo_name: hiljusti/codewars-solutions

max_forks_repo_name: hiljusti/codewars-solutions


text:
module Main

import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.String

data Point = P Int Int

Pretty Point where
  pretty (P x y) = parens (pretty "Point" <++> pretty x <++> pretty y)

export
makePoint : Int -> Int -> Point
makePoint = P

main : IO ()
main = do
  putStrLn "makePoint 0 $ 0 =>"
  let options = record { layoutPageWidth = AvailablePerLine 7 1 } defaultLayoutOptions
  let doc = the (Doc ()) (pretty points)
  renderIO (layoutPretty options doc)
  where
    origin : Point
    origin = makePoint 0 $ 0
    points : List Point
    points = [origin, origin]


text:
module Door

import Linear

data DoorState = Closed | Open

data Door : DoorState -> Type where
     MkDoor : (isOpen : Bool) -> Door (if isOpen then Open else Closed)

newDoor    : One m (Door Closed)
knock      : (1 d : Door t) -> One m (Door t)
openDoor   : (1 d : Door Closed) -> One m (Res Bool (\r => Door (if r then Open else Closed)))
closeDoor  : (1 d : Door Open) -> One m (Door Closed)
deleteDoor : (1 d : Door Closed) -> Any m ()

doorProg : Any m ()
doorProg
    = do d <- newDoor
         d <- knock d
         let x = the Int ?something
         ?bar

doorProg2 : Any m ()
doorProg2
    = do d <- newDoor
         d <- knock d
         let x = the Int ?something2
         d' <- knock d
         ?bar2