text:
module TTImp.ProcessTransform

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.UnifyState

import TTImp.Elab
import TTImp.Elab.Check
import TTImp.ProcessDef -- for checking LHS
import TTImp.TTImp

%default covering

export
processTransform : {vars : _} ->
                   {auto c : Ref Ctxt Defs} ->
                   {auto m : Ref MD Metadata} ->
                   {auto u : Ref UST UState} ->
                   List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->
                   Name -> RawImp -> RawImp -> Core ()
processTransform eopts nest env fc tn_in lhs rhs
    = do tn <- inCurrentNS tn_in
         tidx <- resolveName tn
         (_, (vars'  ** (sub', env', nest', lhstm, lhsty))) <-
             checkLHS True top True tidx eopts nest env fc lhs
         logTerm "" 3 "Transform LHS" lhstm
         rhstm <- wrapError (InRHS fc tn_in) $
                       checkTermSub tidx InExpr (InTrans :: eopts) nest' env' env sub' rhs (gnf env' lhsty)
         clearHoleLHS
         logTerm "" 3 "Transform RHS" rhstm
         addTransform fc (MkTransform tn env' lhstm rhstm)

ext: idr


text:
module Main

import Vimscript.Builtins
import Vimscript.FFI
import Vimscript.List

||| Make a bunch of splits, alternating between
||| horizontal and vertical.
mkSplits : (n : Int) -> VIM_IO ()
mkSplits n = go n True
  where
    go 0 _ = pure ()
    go n c =
      (if c then split else vsplit) *> go (n - 1) (not c)

-- function! StripTrailingWhitespaces()
--     " save last search & cursor position
--     let _s=@/
--     let l = line(".")
--     let c = col(".")
--     %s/\s\+$//e
--     let @/=_s
--     call cursor(l, c)
-- endfunction
stripTrailingWhitespace : VIM_IO ()
stripTrailingWhitespace = do
  l <- line "."
  c <- col "."
  sub "%" "\\s\\+$" "" "e"
  cursor l c

%inline
echoStr : String -> VIM_IO ()
echoStr = echo

main : VIM_IO ()
main = do
  echo ("Readonly flag is set to " ++ !(readOption "readonly"))
  writeOption "readonly" 1
  echo ("Readonly flag is set to " ++ !(readOption "readonly"))
  writeRegister "q" "ggVGy"

  echo "Registers:"
  map concat (traverse (readRegister . singleton) ['a','q']) >>= echoStr

max_stars_repo_name: owickstrom/idris-vimscript

max_issues_repo_name: owickstrom/idris-vimscript

max_forks_repo_name: owickstrom/idris-vimscript


text:
module Specifications.TranslationInvariance

import public Specifications.Group
import public Specifications.Order

%default total
%access public export

infixl 8 #

||| specification
isTranslationInvariantL : Binop s -> Binrel s -> Type
isTranslationInvariantL (#) rel = (x,y,a : _) -> rel x y -> rel (a # x) (a # y)

||| specification
isTranslationInvariantR : Binop s -> Binrel s -> Type
isTranslationInvariantR (#) rel = (x,y,a : _) -> rel x y -> rel (x # a) (y # a)

||| composed specification
data PartiallyOrderedMagmaSpec : Binop s -> Binrel s -> Type where
  MkPartiallyOrderedMagma :
    PartialOrderSpec leq ->
    isTranslationInvariantL op leq ->
    isTranslationInvariantR op leq ->
    PartiallyOrderedMagmaSpec op leq

||| forget
order : PartiallyOrderedMagmaSpec _ leq -> PartialOrderSpec leq
order (MkPartiallyOrderedMagma o _ _) = o

||| forget
translationInvariantL : PartiallyOrderedMagmaSpec op leq ->
  isTranslationInvariantL op leq
translationInvariantL (MkPartiallyOrderedMagma _ l _) = l

||| forget
translationInvariantR : PartiallyOrderedMagmaSpec op leq ->
  isTranslationInvariantR op leq
translationInvariantR (MkPartiallyOrderedMagma _ _ r) = r

||| composed specification
data PartiallyOrderedGroupSpec :
       Binop s -> s -> (s -> s) -> Binrel s -> Type where
  MkPartiallyOrderedGroup :
    GroupSpec op e inv ->
    PartiallyOrderedMagmaSpec op leq ->
    PartiallyOrderedGroupSpec op e inv leq

||| forget
invariantOrder : PartiallyOrderedGroupSpec op _ _ leq ->
  PartiallyOrderedMagmaSpec op leq
invariantOrder (MkPartiallyOrderedGroup _ m) = m

||| forget
group : PartiallyOrderedGroupSpec op e inv _ -> GroupSpec op e inv
group (MkPartiallyOrderedGroup g _) = g

namespace ForgetGroup
  order : PartiallyOrderedGroupSpec _ _ _ leq -> PartialOrderSpec leq
  order = order . invariantOrder

||| A symmetric interval [-u, u]
InSymRange : Binrel s -> (s -> s) -> s -> s -> Type
InSymRange rel inv u = Between rel (inv u, u)

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Text.WebIDL.Types.Numbers

import Generics.Derive

%default total

%language ElabReflection

||| The default Eq for Nat runs in O(n), which is too slow
||| if we want to support large natlits in our tests.
export
[FastNatEq] Eq Nat where
  (==) = (==) `on` natToInteger

--------------------------------------------------------------------------------
--          IntLit
--------------------------------------------------------------------------------

||| An integer literal in hexadecimal, octal, or decimal representation.
||| The code generator will use the same representation when
||| generating code for constants and default values.
public export
data IntLit = Hex Nat | Oct Nat | I Integer

%runElab derive "IntLit" [Generic,Meta,Show]

export
Eq IntLit using FastNatEq where (==) = genEq

--------------------------------------------------------------------------------
--          Parsing Integers
--------------------------------------------------------------------------------

digitToInt : Char -> Integer
digitToInt c = cast $ if isDigit c
                         then ord c - ord '0'
                         else ord (toUpper c) - ord 'A' + 10

charsToPosInt : (base : Integer) -> List Char -> Maybe Integer
charsToPosInt base t = calc <$> traverse readDigit t
  where readDigit : Char -> Maybe Integer
        readDigit c = let d = digitToInt c
                       in if d >= 0 && d < base then Just d else Nothing

        calc : List Integer -> Integer
        calc = foldl (\a,e => a * base + e) 0

||| Tries to read an integer literal from a `String`.
export
readInt : String -> Maybe IntLit
readInt s = case fastUnpack s of
                 '0'::'x'::t => map (Hex . fromInteger) $ charsToPosInt 16 t
                 '0'::'X'::t => map (Hex . fromInteger) $ charsToPosInt 16 t
                 '0'::t      => map (Oct . fromInteger) $ charsToPosInt 8  t
                 '-'::t      => I . negate <$> charsToPosInt 10 t
                 t           => map I $ charsToPosInt 10 t

--------------------------------------------------------------------------------
--          Floating Point Literals
--------------------------------------------------------------------------------

||| The sign of a floating point literal.
public export
data Signum = Plus | Minus

%runElab derive "Signum" [Generic,Meta,Eq,Show]

||| A parsed floating point literal.
|||
||| A floating point literal is either one of three
||| special values (`NaN`, `Infinity`, or `-Infinity`)
||| or a decimal floating point number (`NoExp`: dot is
||| mandatory), or a float in scientific notation (`Exp`:
||| dot is optional).
|||
||| The main focus of this data type is one of
||| preserving information. Encoding a `FloatLit` should
||| yield (almost) exactly the same literal as the one
||| encountered during parsin with two minor exceptions:
||| a) The encoded literal will always use a lowercase 'e' as
||| the delimiter for the exponent and b) in case of a
||| positive exponent, there will not be a '+' in the
||| encoded literal.
public export
data FloatLit : Type where
  ||| Floating point number in scientific notation.
  |||
  ||| Example: `-12.10e10`
  Exp :  (signum    : Signum)
      -> (beforeDot : Nat)
      -> (afterDot  : Maybe Nat)
      -> (exp       : Integer)
      -> FloatLit

  ||| Floating point number without exponent.
  |||
  ||| Example: `-12.1002`
  NoExp :  (signum    : Signum)
        -> (beforeDot : Nat)
        -> (afterDot  : Nat)
        -> FloatLit

  ||| Corresponds to the WebIDL keyword `Infinity`
  Infinity         : FloatLit

  ||| Corresponds to the WebIDL keyword `-Infinity`
  NegativeInfinity : FloatLit

  ||| Corresponds to the WebIDL keyword `NaN`
  NaN              : FloatLit

%runElab derive "FloatLit" [Generic,Meta,Show]

export
Eq FloatLit using FastNatEq where (==) = genEq

--------------------------------------------------------------------------------
--          Parsing Floats
--------------------------------------------------------------------------------

charsToNat : List Char -> Maybe Nat
charsToNat = map fromInteger . charsToPosInt 10

beforeDot : List Char -> (Signum,Maybe Nat)
beforeDot ('-'::cs) = (Minus,charsToNat cs)
beforeDot cs        = (Plus, charsToNat cs)

exp : String -> Maybe String -> String -> Maybe FloatLit
exp bds ads es =
  let (s,bdNat) = beforeDot (fastUnpack bds)
   in do bd <- bdNat
         ad <- maybe (Just Nothing) (map Just . charsToNat . fastUnpack) ads
         e  <- afterExp (fastUnpack es)
         pure $ Exp s bd ad e

  where afterExp : List Char -> Maybe Integer
        afterExp ('-'::cs) = negate <$> charsToPosInt 10 cs
        afterExp ('+'::cs) = charsToPosInt 10 cs
        afterExp cs        = charsToPosInt 10 cs

noExp : String -> String -> Maybe FloatLit
noExp bds ads =
  let (s,bdNat) = beforeDot $ fastUnpack bds
   in do bd <- bdNat
         ad <- charsToNat $ fastUnpack ads
         pure $ NoExp s bd ad

||| Tries to read a floating point literal
||| from a `String`.
export
readFloat : String -> Maybe FloatLit
readFloat s =
  case split (('E' ==) . toUpper) s of
    -- with exponent, dot is optional
    h ::: [e] => case split ('.' ==) h of
      h2 ::: [t2] => exp h2 (Just t2) e
      h2 ::: []   => exp h2 Nothing e
      _  ::: _    => Nothing

    -- without exponent, dot is mandatory
    -- (otherwise it is an integer)
    h ::: [] => case split ('.' ==) h of
      h2 ::: [t2] => noExp h2 t2
      _  ::: _    => Nothing

    -- more than one E in string
    _ ::: _  => Nothing


text:
module Libraries.Control.ANSI.CSI

%default total

||| Moves the cursor n columns up.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorUp : Nat -> String
cursorUp n = "\x1B[" ++ show n ++ "A"

export
cursorUp1 : String
cursorUp1 = cursorUp 1

||| Moves the cursor n columns down.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorDown : Nat -> String
cursorDown n = "\x1B[" ++ show n ++ "B"

export
cursorDown1 : String
cursorDown1 = cursorDown 1

||| Moves the cursor n columns forward.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorForward : Nat -> String
cursorForward n = "\x1B[" ++ show n ++ "C"

export
cursorForward1 : String
cursorForward1 = cursorForward 1

||| Moves the cursor n columns back.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorBack : Nat -> String
cursorBack n = "\x1B[" ++ show n ++ "D"

export
cursorBack1 : String
cursorBack1 = cursorBack 1

||| Moves the cursor at the beginning of n lines down.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorNextLine : Nat -> String
cursorNextLine n = "\x1B[" ++ show n ++ "E"

export
cursorNextLine1 : String
cursorNextLine1 = cursorNextLine 1

||| Moves the cursor at the beginning of n lines up.
||| If the cursor is at the edge of the screen it has no effect.
export
cursorPrevLine : Nat -> String
cursorPrevLine n = "\x1B[" ++ show n ++ "F"

export
cursorPrevLine1 : String
cursorPrevLine1 = cursorPrevLine 1

||| Moves the cursor at an arbitrary line and column.
||| Both lines and columns start at 1.
export
cursorMove : (row : Nat) -> (col : Nat) -> String
cursorMove row col = "\x1B[" ++ show row ++ ";" ++ show col ++ "H"

public export
data EraseDirection = Start | End | All

Cast EraseDirection String where
  cast Start = "1"
  cast End = "0"
  cast All = "2"

||| Clears part of the screen.
export
eraseScreen : EraseDirection -> String
eraseScreen to = "\x1B[" ++ cast to ++ "J"

||| Clears part of the line.
export
eraseLine : EraseDirection -> String
eraseLine to = "\x1B[" ++ cast to ++ "K"

||| Scrolls the whole screen up by n lines.
export
scrollUp : Nat -> String
scrollUp n = "\x1B[" ++ show n ++ "S"

export
scrollUp1 : String
scrollUp1 = scrollUp 1

||| Scrolls the whole screen down by n lines.
export
scrollDown : Nat -> String
scrollDown n = "\x1B[" ++ show n ++ "T"

export
scrollDown1 : String
scrollDown1 = scrollDown 1


text:
module As

-- Test @
isS : Nat -> Maybe Nat
isS Z = Nothing
isS n@(S _) = Just n

-- Test @ under a constructor
hasS : List Nat -> Maybe Nat
hasS (Z::xs) = hasS xs
hasS (n@(S _)::xs) = Just n
hasS _ = Nothing

-- Test nested @s
isSS : Nat -> Maybe (Nat, Nat)
isSS n@(S m@(S _)) = Just (n,m)
isSS _ = Nothing

-- Test two @-patterns
same : Nat -> Nat -> Maybe Nat
same x@(S _) y@(S _) = Just $ x + y
same Z Z = Just 42
same _ _ = Nothing

namespace Main
  main : IO ()
  main = do printLn $ isS 0
            printLn $ isS 1
            printLn $ hasS [0,0,0]
            printLn $ hasS [0,1,2]
            printLn $ isSS 5
            printLn $ isSS 0
            printLn $ same 1 1
            printLn $ same 0 0
            printLn $ same 1 0

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Optimisation.StaticProcessing.IterativeBaseTransformer

import Data.List
import Data.SortedSet
import Data.SortedMap
import Core.Context
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import Optimisation.StaticProcessing.StaticTransformer
import Optimisation.StaticProcessing.StaticTracker
import Optimisation.OrderAndEliminateDefinitions
import CairoCode.Traversal.Base
import Utils.Helpers
import CommonDef
import Utils.Lens

import Debug.Trace

%hide Prelude.toList

record GlobalTransformerState where
    constructor MkGlobalTransformerState
    -- Global Context
    allDefs : SortedMap Name CairoDef
    retBind : SortedMap Name (List StaticInfo)
    -- Per iter Context
    regGen : RegisterGen
    return : Maybe (List StaticInfo)
    hot : Bool

regGenLens : Lens GlobalTransformerState RegisterGen
regGenLens = MkLens regGen (\ts,fn => {regGen $= fn} ts)

returnLens : Lens GlobalTransformerState (Maybe (List StaticInfo))
returnLens = MkLens return (\ts,fn => {return $= fn} ts)

recordRet : List StaticInfo -> GlobalTransformerState -> GlobalTransformerState
recordRet ret (MkGlobalTransformerState allDefs retBind regGen (Just oldRet) hot) = MkGlobalTransformerState allDefs retBind regGen (Just (zipWith mergeStaticInfo ret oldRet)) hot
recordRet ret (MkGlobalTransformerState allDefs retBind regGen Nothing hot) = MkGlobalTransformerState allDefs retBind regGen (Just ret) hot

markHot : GlobalTransformerState -> GlobalTransformerState
markHot (MkGlobalTransformerState allDefs retBind regGen ret hot) = MkGlobalTransformerState allDefs retBind regGen ret True

integrateRet : Name -> List StaticInfo -> GlobalTransformerState -> GlobalTransformerState
integrateRet name ret (MkGlobalTransformerState allDefs retBind regGen rets hot) = MkGlobalTransformerState allDefs (insert name ret retBind) regGen rets hot

integrateDef : (Name, CairoDef) -> GlobalTransformerState -> GlobalTransformerState
integrateDef (name, def) (MkGlobalTransformerState allDefs retBind regGen rets hot) = MkGlobalTransformerState (insert name def allDefs) retBind regGen rets hot

resetState : GlobalTransformerState -> GlobalTransformerState
resetState (MkGlobalTransformerState allDefs retBind regGen _ _) = MkGlobalTransformerState allDefs retBind regGen Nothing False

finishDef : (Name, CairoDef) -> GlobalTransformerState -> GlobalTransformerState
finishDef def state = resetState $ integrateDef def (integrateRet (fst def) (fromMaybe (assert_total $ idris_crash "Missing return to record") state.return) state)

-- todo: not necessary but would lead to a cleaner ret map : REENABLE THIS --
{-
mutual
    cleanStaticValue : SortedSet CairoReg  -> StaticValue -> StaticValue
    cleanStaticValue argKeep (Constructed ctrs) = Constructed (mapValueMap (map (cleanStaticInfo argKeep)) ctrs)
    cleanStaticValue argKeep (Closure name args) = Closure name (map (cleanStaticInfo argKeep) args)
    cleanStaticValue argKeep (Field src tag no) = Field (cleanStaticInfo argKeep) tag no
    cleanStaticValue _ val = val

    cleanStaticInfo : SortedSet CairoReg -> StaticInfo -> StaticInfo
    cleanStaticInfo args (MKStaticInfo src val) = MKStaticInfo (intersection src args) (cleanStaticValue val)

cleanStaticInfos : (args: List CairoReg) -> (rets: List StaticInfo) -> List StaticInfo
cleanStaticInfos args rets = map (cleanStaticInfo (fromList args)) rets
-}

mutual
    substituteStaticValue : SortedMap CairoReg StaticInfo -> StaticValue -> StaticInfo
    substituteStaticValue argSubs (Constructed ctrs) = MKStaticInfo empty (Constructed (mapValueMap (map (substituteStaticInfo argSubs)) ctrs))
    substituteStaticValue argSubs (Closure name args) = MKStaticInfo empty (Closure name (map (substituteStaticInfo argSubs) args))
    substituteStaticValue argSubs (Field src Nothing no) = MKStaticInfo empty (Field (substituteStaticInfo argSubs src) Nothing no)
    substituteStaticValue argSubs (Field src (Just tag) no) = simplify $ substituteStaticInfo argSubs src
        where tryExtractField : Nat -> List StaticInfo -> StaticInfo
              tryExtractField _ Nil = MKStaticInfo empty (Field src (Just tag) no)
              tryExtractField Z (x::_) = substituteStaticInfo argSubs x
              tryExtractField (S n) (_::xs) = tryExtractField n xs
              simplify : StaticInfo -> StaticInfo
              simplify inner@(MKStaticInfo _ (Constructed ctrs)) = case (lookup tag ctrs) of
                Nothing => MKStaticInfo empty (Field src (Just tag) no)
                (Just ctr) => tryExtractField no ctr
              simplify inner = MKStaticInfo empty (Field src (Just tag) no)
    substituteStaticValue _ val = MKStaticInfo empty val

    substituteStaticInfo : SortedMap CairoReg StaticInfo -> StaticInfo -> StaticInfo
    substituteStaticInfo args (MKStaticInfo src val) = case usedParamRegs of
        Nil => substituteStaticValue args val
        reg::_ => fromMaybe (MKStaticInfo empty Unknown) (lookup reg args)
        where usedParamRegs : List CairoReg
              usedParamRegs = toList $ intersection src (fromList $ keys args)

substituteStaticInfos : (args: List (CairoReg, StaticInfo)) -> (rets: List (CairoReg, StaticInfo)) -> List StaticInfo
substituteStaticInfos args rets = map (\(reg,ret) => addBinding (substituteStaticInfo (fromList args) ret) reg) rets

bindArgs : Maybe CairoDef -> List StaticInfo ->  List (CairoReg, StaticInfo)
bindArgs (Just (FunDef params _ _ _)) vals = zip params vals
bindArgs (Just (ForeignDef _ args _)) vals = zip (map Param (fromZeroTo ((cast args)-1))) vals -- just gen the default ones
bindArgs _ _ = trace "Def to bind args not available" []

public export
record FunData where
    constructor MKFunData
    function: Name
    target: CairoDef
    -- StaticInfo is input (stores a reg internally) & CairoReg is output
    implicitsIn: SortedMap LinearImplicit StaticInfo
    -- StaticInfo is static result & CairoReg is target reg to store it in
    implicitsOut: SortedMap LinearImplicit (CairoReg, StaticInfo)
    -- StaticInfo is input (stores a reg internally)
    arguments : List StaticInfo
    -- StaticInfo is static result & CairoReg is target reg to store it in
    returns: List (CairoReg, StaticInfo)

export
genFunCall : FunData -> List (InstVisit CairoReg)
genFunCall (MKFunData name _ implIn implsOut args rs) = [VisitCall (map fst rs) (resolveLinearImplicits reconstructedImpls) name (map resolveInfToReg args)]
    where  reconstructedImpls : SortedMap LinearImplicit (StaticInfo, CairoReg)
           reconstructedImpls = fromList $ map (\(k,v) => (k, (v, fromMaybe Eliminated (maybeMap fst (lookup k implsOut))))) (toList implIn)

iterativeProcessing : (RegisterGen -> Name -> FunData -> (RegisterGen, Maybe (List (InstVisit CairoReg)))) -> ((Name, CairoDef) -> (Name, CairoDef)) -> List Name -> GlobalTransformerState -> GlobalTransformerState
iterativeProcessing funTransformer cleanUp Nil state = state
iterativeProcessing funTransformer cleanUp (name::xs) state = case lookup name state.allDefs of
        Nothing => iterativeProcessing funTransformer cleanUp (trace ("Function "++(show name)++" is missing") xs) state
        (Just def) => case processFunction (name,def) state of
            (True, state) => iterativeProcessing funTransformer cleanUp (name::xs) state
            (False, state) => iterativeProcessing funTransformer cleanUp xs state
    where processFunction : (Name, CairoDef) -> GlobalTransformerState -> (Bool, GlobalTransformerState)
          processFunction curDef@(curName, (ForeignDef _ _ rets)) state = (False, finishDef curDef (recordRet (replicate rets (MKStaticInfo empty  Unknown)) state))
          -- todo: Shall we have a track only version now that we have cleanup??
          processFunction curDef state = finish $ globalStaticOptimizeDef @{handler} state.allDefs state curDef
            where finish : ((Name, CairoDef), GlobalTransformerState) -> (Bool, GlobalTransformerState)
                  finish (def, nState) = (nState.hot, finishDef (cleanUp def) nState)
                  trackRet : Name -> List StaticInfo -> List CairoReg -> GlobalTransformerState -> List StaticInfo
                  trackRet name args rs state = produceRet $ lookup name state.retBind
                    where produceRet : Maybe (List StaticInfo) ->  List StaticInfo
                          produceRet (Just statRet) = substituteStaticInfos (bindArgs (lookup name state.allDefs) args) (zip rs statRet)
                          produceRet Nothing = map (\r => MKStaticInfo (singleton r) Unknown) rs
                  [handler] CallHandler GlobalTransformerState where
                    return rets _ = updateState (recordRet rets)
                    track (MKCallData name impls args rs) = map (\state => (trackRet name args rs state, staticImplTracker impls)) readState
                    transform (MKCallData name impls args rs) = readState >>= (\state => writeStateBack $ withState state)
                        where writeStateBack : (GlobalTransformerState, List (InstVisit CairoReg)) -> Traversal GlobalTransformerState (List (InstVisit CairoReg))
                              writeStateBack (state, res) = map (\_ => res) (writeState state)
                              withState : GlobalTransformerState -> (GlobalTransformerState, List (InstVisit CairoReg))
                              withState state = processRet $ funTransformer state.regGen (fst curDef) funData
                                where nImpls : SortedMap LinearImplicit StaticInfo
                                      nImpls = staticImplTracker impls
                                      rets : List (CairoReg, StaticInfo)
                                      rets = zip rs (trackRet name args rs state)
                                      buildLinOut: LinearImplicit -> (LinearImplicit, (CairoReg, StaticInfo))
                                      buildLinOut k = (k, (fromMaybe Eliminated (maybeMap snd (lookup k impls)), fromMaybe (MKStaticInfo empty Unknown) (lookup k nImpls)))
                                      implOut : SortedMap LinearImplicit (CairoReg, StaticInfo)
                                      implOut = fromList $ map buildLinOut (keys impls)
                                      def : CairoDef
                                      def = fromMaybe (assert_total $ idris_crash "Unknown function is called") (lookup name state.allDefs)
                                      funData : FunData
                                      funData = (MKFunData name def (mapValueMap fst impls) implOut args rets)
                                      processRet : (RegisterGen, Maybe (List (InstVisit CairoReg))) -> (GlobalTransformerState, List (InstVisit CairoReg))
                                      processRet (regGen, Nothing) = (regGenLens.set state regGen, genFunCall funData)
                                      processRet (regGen, Just res) = (markHot $ regGenLens.set state regGen, res)

export
iterativeCallTransform : RegisterGen -> (RegisterGen -> Name -> FunData -> (RegisterGen, Maybe (List (InstVisit CairoReg)))) -> ((Name, CairoDef)  -> (Name, CairoDef))  -> Name -> List (Name, CairoDef) -> List (Name, CairoDef)
iterativeCallTransform regGen transformer cleaner entryPoint defs = reconstruct $ iterativeProcessing transformer cleaner orderedNames (MkGlobalTransformerState defLookup empty regGen Nothing False)
    where defLookup : SortedMap Name CairoDef
          defLookup = fromList defs
          orderedNames : List Name
          orderedNames = map fst (orderUsedDefs entryPoint defs)
          reconstruct : GlobalTransformerState -> List (Name, CairoDef)
          reconstruct (MkGlobalTransformerState newDefs _ _ _ _ ) = orderUsedDefs entryPoint (toList newDefs)

export
noTransform : RegisterGen -> Name -> FunData -> (RegisterGen, Maybe (List (InstVisit CairoReg)))
noTransform regGen _ funData = (regGen, Nothing)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Main

palindrome : String -> Bool
palindrome str = let strLower = toLower str in
                     strLower == reverse strLower

main : IO ()
main = repl "Enter a string: " show_palindrome
  where
    show_palindrome : String -> String
    show_palindrome x = show (palindrome x) ++ "\n"


text:
module HEffCont

import Data.HVect

Effect : Type -> Type
Effect r = r -> (a : Type) -> (a -> r) -> Type

Effects : (Type -> Type) -> Vect n Type -> Vect n Type
Effects f [] = []
Effects f (x :: xs) = f x :: Effects f xs

data Exists' : {t : Type} -> {rs : Vect n Type} ->
               HVect rs -> t -> HVect (Effects Effect rs) -> Effect t -> Type where
  Here : Exists' (x :: xs) x (y :: ys) y
  There : Exists' xs x ys y -> Exists' (_ :: xs) x (_ :: ys) y

update' : {t : Type} -> (r : HVect rs) -> (e : Exists' {t = t} r s effs eff) -> t -> HVect rs
update' [] Here _ impossible
update' [] (There _) _ impossible
update' (x :: xs) Here v = v :: xs
update' (x :: xs) (There e) v = x :: update' xs e v

data HEffect : {n : Nat} -> (rs : Vect n Type) -> HVect (Effects Effect rs) -> Effect (HVect rs) where
  Pure : (x : a) -> HEffect rs effs (r' x) a r'
  EffectC : (e : Exists' r s effs eff) -> eff s a s' -> HEffect rs effs r a (\x => update' r e (s' x))

data HEff : {n : Nat} -> (rs : Vect n Type) -> HVect (Effects Effect rs) -> Effect (HVect rs) where
  Cont : {rs : Vect n Type} -> ({res : Type} -> (a -> res) -> ({x : Type} -> {r : HVect rs} -> {r' : x -> HVect rs} -> HEffect rs effs r x r' -> (x -> res) -> res) -> res) -> HEff rs effs r a r'

pure : (x : a) -> HEff rs effs (r' x) a r'
pure {r'} x = Cont (\k, imp => imp (Pure {r' = r'} x) k)

(>>=) : HEff rs effs r a r' -> ((x : a) -> HEff rs effs (r' x) b r'') -> HEff rs effs r b r''
(>>=) (Cont g) f = Cont (\k, imp => g (\x => let (Cont g') = f x in g' k imp) imp)

data Access = LoggedOut | LoggedIn
data Store : Access -> (ty : Type) -> (ty -> Access) -> Type where
  Login : Store LoggedOut () (const LoggedIn)
  Logout : Store LoggedIn () (const LoggedOut)

login : {auto e : Exists' r LoggedOut effs Store} ->
         HEff rs effs r () (\_ => update' r e LoggedIn)
login {e} = Cont (\k, imp => imp (EffectC e Login) k)

logout : {auto e : Exists' r LoggedIn effs Store} ->
         HEff rs effs r () (\_ => update' r e LoggedOut)
logout {e} = Cont (\k, imp => imp (EffectC e Logout) k)

runPure : HEffect [] [] r a r' -> (a -> res) -> res
runPure (Pure x) k = k x
runPure (EffectC Here _) _ impossible
runPure (EffectC (There _) _) _ impossible

head' : HVect xs -> head xs
head' (x :: _) = x
tail' : HVect xs -> HVect (tail xs)
tail' (x :: xs) = xs

runStore : {rs : Vect n Type} -> (HEffect rs effs (tail' {xs = (Access :: rs)} r) a (\x => tail' {xs = (Access :: rs)} $ r' x) -> (a -> res) -> res) -> HEffect (Access :: rs) (Store :: effs) r a r' -> (a -> res) -> res
runStore k (Pure x) k' = k' x
runStore k (EffectC Here Login) k' = k' ()
runStore k (EffectC Here Logout) k' = k' ()
runStore k (EffectC (There effs) eff) k' = k (EffectC effs eff) k'

run : {rs : Vect n Type} -> HEff rs effs r a r' -> (a -> res) -> ({x : Type} -> {r : HVect rs} -> {r' : x -> HVect rs} -> HEffect rs effs r x r' -> (x -> res) -> res) -> res
run (Cont f) k imp = f k imp

example : HEff [Access] [Store] [LoggedOut] () (\_ => [LoggedOut])
example = do login
             logout

test : ()
test = run example (\_ => ()) (\eff, k => runStore runPure eff k)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
import Data.List

mkList : a -> Nat -> List a
mkList x Z = ?help
mkList x (S k) = x :: mkList x k

-- For a performance test: make sure we evaluate the full list, and get
-- a result that we don't have to work hard to render
isEven : Nat -> Bool
isEven Z = True
isEven (S k) = not (isEven k)


text:
module Erlang.Types.Atom

import Language.Reflection

%default total

||| Generate atom functions from a list of strings.
|||
||| Usage:
||| ```
||| import Erlang
||| import Language.Reflection
|||
||| %language ElabReflection
|||
||| %runElab generateAtomHelpers ["ok", "error"]
||| ```
|||
||| Will generate the following functions:
||| ```
||| private %inline
||| A_ok : ErlAtom
||| A_ok = MkAtom "ok"
|||
||| private %inline
||| A_error : ErlAtom
||| A_error = MkAtom "error"
||| ```
export
generateAtomHelpers : List String -> Elab ()
generateAtomHelpers atoms =
  declare (atoms >>= atomToDecls)
  where
    atomToDecls : String -> List Decl
    atomToDecls atom =
      let fnName = UN (Basic ("A_" ++ atom))
      in
        [ IClaim EmptyFC MW Private [Inline] (MkTy EmptyFC EmptyFC fnName `(ErlAtom))
        , IDef EmptyFC fnName
            [ PatClause EmptyFC
                (IVar EmptyFC fnName)
                `(MkAtom ~(IPrimVal EmptyFC (Str atom)))
            ]
        ]


text:
[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[MultNatSemi] Semigroup Nat where
  (<+>) x y = x * y

[PlusNatMonoid] Monoid Nat using PlusNatSemi where
  neutral = 0

[MultNatMonoid] Monoid Nat using MultNatSemi where
  neutral = 1


text:
import Data.Vect

my_length : List a -> Nat
my_length [] = 0
my_length (x :: xs) = 1 + my_length xs

my_reverse : List a -> List a
my_reverse [] = []
my_reverse (x :: xs) = (my_reverse xs) ++ [x]

my_map : (a -> b) -> List a -> List b
my_map f [] = []
my_map f (x :: xs) = f x :: my_map f xs

my_map2 : (a -> b) -> Vect n a -> Vect n b
my_map2 f [] = []
my_map2 f (x :: xs) = f x :: my_map2 f xs


text:
module Quantities.ImperialUnits

import Quantities.Core
import Quantities.SIBaseQuantities
import Quantities.SIPrefixes
import Quantities.SIBaseUnits
import Quantities.SIDerivedQuantities
import Quantities.NonSIUnits

%default total
%access public export

-- Based on http://en.wikipedia.org/wiki/Imperial_units

-- Length

Thou : ElemUnit Length
Thou = < one "th" equals 25.4 (micro Metre) >
Th : ElemUnit Length
Th = Thou

Inch : ElemUnit Length
Inch = < one "in" equals 2.54 Centimetre >
In_ : ElemUnit Length
In_ = Inch

Foot : ElemUnit Length
Foot = < one "ft" equals 12 Inch >
Ft : ElemUnit Length
Ft = Foot

Yard : ElemUnit Length
Yard = < one "yd" equals 3 Foot >
Yd : ElemUnit Length
Yd = Yard

Chain : ElemUnit Length
Chain = < one "ch" equals 22 Yard >
Ch : ElemUnit Length
Ch = Chain

Furlong : ElemUnit Length
Furlong = < one "fur" equals 10 Chain >
Fur : ElemUnit Length
Fur = Furlong

Mile : ElemUnit Length
Mile = < one "mi" equals 1760 Yard >
Mi : ElemUnit Length
Mi = Mile

League : ElemUnit Length
League = < one "lea" equals 3 Mile >
Lea : ElemUnit Length
Lea = League

-- Maritime units

Fathom : ElemUnit Length
Fathom = < one "ftm" equals 6.08 Foot >
Ftm : ElemUnit Length
Ftm = Fathom

Cable : ElemUnit Length
Cable = < one "cable" equals 608 Foot >

NauticalMile : ElemUnit Length
NauticalMile = < one "nmi" equals 1852 Metre >
Nmi : ElemUnit Length
Nmi = NauticalMile

-- Gunter's survey units

Link : ElemUnit Length
Link = < one "link" equals (1/100) Chain >

Rod : ElemUnit Length
Rod = < one "rod" equals (1/4) Chain >

-- Speed

Knot : ElemUnit Speed
Knot = < one "kn" equals 1 (NauticalMile <//> Hour) >
Kn : ElemUnit Speed
Kn = Knot

-- Area

Perch : ElemUnit Area
Perch = < one "perch" equals 1 (Rod ^^ 2) >

Rood : ElemUnit Area
Rood = < one "rood" equals 1 (Furlong <**> Rod) >

Acre : ElemUnit Area
Acre = < one "acre" equals 1 (Furlong <**> Chain) >

-- Volume

FluidOunce : ElemUnit Volume
FluidOunce = < one "floz" equals 28.4130625 (milli $ (deci Metre) ^^ 3) >
Floz : ElemUnit Volume
Floz = FluidOunce

Gill : ElemUnit Volume
Gill = < one "gi" equals 5 FluidOunce >
Gi : ElemUnit Volume
Gi = Gill

Pint : ElemUnit Volume
Pint = < one "pt" equals 20 FluidOunce >
Pt : ElemUnit Volume
Pt = Pint

Quart : ElemUnit Volume
Quart = < one "qt" equals 40 FluidOunce >
Qt : ElemUnit Volume
Qt = Quart

Gallon : ElemUnit Volume
Gallon = < one "gal" equals 160 FluidOunce >
Gal : ElemUnit Volume
Gal = Gallon

-- British apothecaries' volume measures

Minim : ElemUnit Volume
Minim = < one "min" equals 59.1938802083 (micro $ (deci Metre) ^^ 3) >
Min : ElemUnit Volume
Min = Minim

FluidScruple : ElemUnit Volume
FluidScruple = < one "fls" equals 20 Minim >
Fls : ElemUnit Volume
Fls = FluidScruple

FluidDrachm : ElemUnit Volume
FluidDrachm = < one "fldr" equals 3 FluidScruple >
Fldr : ElemUnit Volume
Fldr = FluidDrachm

-- Mass

Pound : ElemUnit Mass
Pound = < one "lb" equals 453.59237 Gram >
Lb : ElemUnit Mass
Lb = Pound

Grain : ElemUnit Mass
Grain = < one "gr" equals (1/7000) Pound >
Gr : ElemUnit Mass
Gr = Grain

Drachm : ElemUnit Mass
Drachm = < one "dr" equals (1/256) Pound >
Dr : ElemUnit Mass
Dr = Drachm

Ounce : ElemUnit Mass
Ounce = < one "oz" equals (1/16) Pound >
Oz : ElemUnit Mass
Oz = Ounce

Stone : ElemUnit Mass
Stone = < one "st" equals 14 Pound >
St : ElemUnit Mass
St = Stone

Quarter : ElemUnit Mass
Quarter = < one "qtr" equals 28 Pound >
Qtr : ElemUnit Mass
Qtr = Quarter

Hundredweight : ElemUnit Mass
Hundredweight = < one "cwt" equals 112 Pound >
Cwt : ElemUnit Mass
Cwt = Hundredweight

Ton : ElemUnit Mass
Ton = < one "ton" equals 2240 Pound >

-- Energy

FootPound : ElemUnit Energy
FootPound = < one "ftlb" equals 1 (Foot <**> Pound <**> G_0) >
Ftlb : ElemUnit Energy
Ftlb = FootPound

-- Power

MechanicalHorsepower : ElemUnit Power
MechanicalHorsepower = < one "hp" equals 550 (FootPound <//> Second) >
ImperialHorsepower : ElemUnit Power
ImperialHorsepower = MechanicalHorsepower
Horsepower : ElemUnit Power
Horsepower = MechanicalHorsepower
Hp : ElemUnit Power
Hp = MechanicalHorsepower

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
module Matrix

import Data.Vect

%default total

transposeHelper : Vect n elem -> Vect n (Vect len elem) -> Vect n (Vect (S len) elem)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys

transposeMatrix : { n, m : _ } -> Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMatrix [] = replicate n []
transposeMatrix (x :: xs) = let xsTrans = transposeMatrix xs in
                                transposeHelper x xsTrans

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:
-- ------------------------------------------------------- [ Specification.idr ]
-- Module    : Specification.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A language to build abstract interface specifications.
module Cordial.EDSL.Specification

import public Data.Vect
import public Data.List.Quantifiers
import public Data.Ranged

import public Text.Markup.Edda

import public Language.EDSL.SingleStateVar

import public Cordial.Model.Specification

import public Cordial.EDSL.Specification.Lang

import public Cordial.EDSL.Specification.API

%default total
%access public export

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module TypedContainers.RBTree.Balance

import Data.DPair
import Data.List
import TypedContainers.In
import TypedContainers.LawfulOrd
import TypedContainers.RBTree.Base
import TypedContainers.Util.Filter

%default total

0 lemma0 : LawfulOrd kt => {keys : List kt} -> (xk : kt) -> (yk : kt) -> In (yk ==) (filter (xk <) keys) -> (compare xk yk = LT)
lemma0 xk yk p0 =
  let MkDPair v (p3, p4) = extractIn p0 in
  let p5 = equality2 _ _ xk (convEQ _ _ p3) in
  let p6 = convLT xk v p4 in
  trans p5 p6

0 lemma1 : LawfulOrd kt => {keys : List kt} -> (xk : kt) -> (yk : kt) -> In (yk ==) (filter (xk >) keys) -> (compare xk yk = GT)
lemma1 xk yk p0 =
  let MkDPair v (p3, p4) = extractIn p0 in
  let p5 = equality2 _ _ xk (convEQ _ _ p3) in
  let p6 = convGT xk v p4 in
  trans p5 p6

public export
balanceLeft :
  (kord : LawfulOrd kt) =>
  (zk : kt) ->
  {0 zkp : In (zk ==) keys} ->
  vt zk ->
  BadTree {height, kt, kord, keys = filter (zk >) keys, vt} ->
  GoodTree {height, color = colorRight, kt, kord, keys = filter (zk <) keys, vt} ->
  Exists \color : Color => GoodTree {height = S height, color, kt, kord, keys = keys, vt}
balanceLeft zk zv (BadRedNode {kp = xkp} xk xv a (RedNode yk yv b c {kp = ykp})) d =
  let
    0 p0 : (arg : kt) -> (xk == arg = True) -> (yk > arg = True)
    p0 arg prr =
      let pp0 = reversion1 xk yk $ lemma0 xk yk ykp in
      let pp1 = equality2 xk arg yk (convEQ xk arg prr) in
      let pp2 = trans (sym pp1) pp0 in
      cong (\case { GT => True; _ => False }) pp2

    0 p0' : (arg : kt) -> (zk == arg = True) -> (yk < arg = True)
    p0' arg prr =
      let pp0 = lemma1 zk yk (outFilter ykp) in
      let pp1 = equality1 zk arg yk (convEQ zk arg prr) in
      let pp2 = trans (sym pp1) pp0 in
      cong (\case { LT => True; _ => False }) $ reversion2 arg yk pp2

    0 p1 : (arg : kt) -> (xk > arg = True) -> (yk > arg = True)
    p1 arg pp0 =
      let pp1 : (compare arg xk = LT) = reversion2 xk arg $ convGT _ _ pp0 in
      let pp2 : (compare xk yk = LT) = lemma0 xk yk ykp in
      let pp3 : (compare arg yk = LT) = transitivity arg xk yk pp1 pp2 in
      cong (\case { GT => True; _ => False }) $ reversion1 arg yk pp3

    0 p1' : (arg : kt) -> (yk < arg = True) -> (xk < arg = True)
    p1' arg pp0 =
      let pp1 : (compare yk arg = LT) = convLT _ _ pp0 in
      let pp2 : (compare xk arg = LT) = transitivity xk yk arg (lemma0 xk yk ykp) pp1 in
      cong (\case { LT => True; _ => False }) pp2

    0 p2 : (arg : kt) -> (yk > arg = True) -> (zk > arg = True)
    p2 arg pp0 =
      let pp1 : (compare arg yk = LT) = reversion2 yk arg $ convGT _ _ pp0 in
      let pp2 : (compare yk zk = LT) = reversion2 zk yk $ lemma1 zk yk (outFilter ykp) in
      let pp3 : (compare arg zk = LT) = transitivity arg yk zk pp1 pp2 in
      cong (\case { GT => True; _ => False }) $ reversion1 arg zk pp3

    0 p2' : (arg : kt) -> (zk < arg = True) -> (yk < arg = True)
    p2' arg pp0 =
      let pp1 : (compare zk arg = LT) = convLT _ _ pp0 in
      let pp2 : (compare yk arg = LT) = transitivity yk zk arg (reversion2 zk yk $ lemma1 zk yk (outFilter ykp)) pp1 in
      cong (\case { LT => True; _ => False }) pp2

    0 p3 : ((filter (xk >) $ filter (zk >) keys) === (filter (xk >) $ filter (yk >) keys))
    p3 =
      let pp0 : ((filter (yk >) $ filter (xk >) $ filter (zk >) keys) === (filter (xk >) $ filter (zk >) keys))
          = filterImplication {g = (xk >), f = (yk >)} p1
      in
      let pp1 : ((filter (xk >) $ filter (yk >) $ filter (zk >) keys) === (filter (yk >) $ filter (xk >) $ filter (zk >) keys))
          = filterCommutative
      in
      let pp2 : ((filter (xk >) $ filter (zk >) $ filter (yk >) keys) === (filter (xk >) $ filter (yk >) $ filter (zk >) keys))
          = cong (filter (xk >)) filterCommutative
      in
      let pp3 : ((filter (xk >) $ filter (yk >) keys) === (filter (xk >) $ filter (zk >) $ filter (yk >) keys))
          = cong (filter (xk >)) $ sym $ filterImplication p2
      in
      sym $ trans pp3 $ trans pp2 $ trans pp1 pp0

    0 p4 : ((filter (yk >) $ filter (xk <) $ filter (zk >) keys) === (filter (xk <) $ filter (yk >) keys))
    p4 =
      let pp0 : ((filter (xk <) $ filter (yk >) $ filter (zk >) keys) === (filter (yk >) $ filter (xk <) $ filter (zk >) keys))
          = filterCommutative
      in
      let pp1 : ((filter (xk <) $ filter (zk >) $ filter (yk >) keys) === (filter (xk <) $ filter (yk >) $ filter (zk >) keys))
          = cong (filter (xk <)) filterCommutative
      in
      let pp2 : ((filter (xk <) $ filter (yk >) keys) === (filter (xk <) $ filter (zk >) $ filter (yk >) keys))
          = cong (filter (xk <)) $ sym $ filterImplication p2
      in
      sym $ trans pp2 $ trans pp1 pp0

    0 p5 : ((filter (yk <) $ filter (xk <) $ filter (zk >) keys) === (filter (zk >) $ filter (yk <) keys))
    p5 =
      let pp0 : ((filter (xk <) $ filter (yk <) $ filter (zk >) keys) === (filter (yk <) $ filter (xk <) $ filter (zk >) keys))
          = filterCommutative
      in
      let pp1 : ((filter (yk <) $ filter (zk >) keys) === (filter (xk <) $ filter (yk <) $ filter (zk >) keys))
          = sym $ filterImplication p1'
      in
      let pp2 : ((filter (zk >) $ filter (yk <) keys) === (filter (yk <) $ filter (zk >) keys))
          = filterCommutative
      in
      sym $ trans pp2 $ trans pp1 pp0

    0 p6 : (filter (zk <) keys) === (filter (zk <) $ filter (yk <) keys)
    p6 =
      let pp0 : ((filter (yk <) $ filter (zk <) keys) === (filter (zk <) keys))
          = filterImplication p2'
      in
      let pp1 : ((filter (zk <) $ filter (yk <) keys) === (filter (yk <) $ filter (zk <) keys))
          = filterCommutative
      in
      sym $ trans pp1 pp0
  in
  let a' : GoodTree {keys = filter (xk >) $ filter (yk >) keys} = rewrite sym p3 in a in
  let b' : GoodTree {keys = filter (xk <) $ filter (yk >) keys} = rewrite sym p4 in b in
  let c' : GoodTree {keys = filter (zk >) $ filter (yk <) keys} = rewrite sym p5 in c in
  let d' : GoodTree {keys = filter (zk <) $ filter (yk <) keys} = rewrite sym p6 in d in
  let l' = BlackNode xk xv a' b' {kp = inFilter (yk >) (xk ==) p0 _ (outFilter xkp)} in
  let r' = BlackNode zk zv c' d' {kp = inFilter (yk <) (zk ==) p0' _ zkp} in
  Evidence Red $ RedNode yk yv l' r' {kp = outFilter $ outFilter ykp}
balanceLeft zk zv (BadRedNode {kp = ykp} yk yv (RedNode xk xv a b {kp = xkp}) c) d =
  let
    0 p0 : (arg : kt) -> (zk == arg = True) -> (yk < arg = True)
    p0 arg prr =
      let pp0 = lemma1 zk yk ykp in
      let pp1 = equality1 zk arg yk (convEQ zk arg prr) in
      let pp2 = trans (sym pp1) pp0 in
      cong (\case { LT => True; _ => False }) $ reversion2 arg yk pp2

    0 p1 : (In (xk ==) (filter (yk >) keys))
    p1 = outFilter $ replace {p = In (xk ==)} filterCommutative xkp

    0 p2 : (arg : kt) -> (yk > arg = True) -> (zk > arg = True)
    p2 arg pp0 =
      let pp1 : (compare arg yk = LT) = reversion2 yk arg $ convGT _ _ pp0 in
      let pp2 : (compare yk zk = LT) = reversion2 zk yk $ lemma1 zk yk ykp in
      let pp3 : (compare arg zk = LT) = transitivity arg yk zk pp1 pp2 in
      cong (\case { GT => True; _ => False }) $ reversion1 arg zk pp3

    0 p2' : (arg : kt) -> (zk < arg = True) -> (yk < arg = True)
    p2' arg pp0 =
      let pp1 : (compare zk arg = LT) = convLT _ _ pp0 in
      let pp2 : (compare yk arg = LT) = transitivity yk zk arg (reversion2 zk yk $ lemma1 zk yk ykp) pp1 in
      cong (\case { LT => True; _ => False }) pp2

    0 p3 : ((filter (xk >) $ filter (yk >) $ filter (zk >) keys) === (filter (xk >) $ filter (yk >) keys))
    p3 =
      let pp2 : ((filter (xk >) $ filter (zk >) $ filter (yk >) keys) === (filter (xk >) $ filter (yk >) $ filter (zk >) keys))
          = cong (filter (xk >)) filterCommutative
      in
      let pp3 : ((filter (xk >) $ filter (yk >) keys) === (filter (xk >) $ filter (zk >) $ filter (yk >) keys))
          = cong (filter (xk >)) $ sym $ filterImplication p2
      in
      sym $ trans pp3 pp2

    0 p4 : ((filter (xk <) $ filter (yk >) $ filter (zk >) keys) === (filter (xk <) $ filter (yk >) keys))
    p4 =
      let pp1 : ((filter (xk <) $ filter (zk >) $ filter (yk >) keys) === (filter (xk <) $ filter (yk >) $ filter (zk >) keys))
          = cong (filter (xk <)) filterCommutative
      in
      let pp2 : ((filter (xk <) $ filter (yk >) keys) === (filter (xk <) $ filter (zk >) $ filter (yk >) keys))
          = cong (filter (xk <)) $ sym $ filterImplication p2
      in
      sym $ trans pp2 pp1

    0 p5 : ((filter (yk <) $ filter (zk >) keys) === (filter (zk >) $ filter (yk <) keys))
    p5 = filterCommutative

    0 p6 : (filter (zk <) keys) === (filter (zk <) $ filter (yk <) keys)
    p6 =
      let pp0 : ((filter (yk <) $ filter (zk <) keys) === (filter (zk <) keys))
          = filterImplication p2'
      in
      let pp1 : ((filter (zk <) $ filter (yk <) keys) === (filter (yk <) $ filter (zk <) keys))
          = filterCommutative
      in
      sym $ trans pp1 pp0
  in
  let a' : GoodTree {keys = filter (xk >) $ filter (yk >) keys} = rewrite sym p3 in a in
  let b' : GoodTree {keys = filter (xk <) $ filter (yk >) keys} = rewrite sym p4 in b in
  let c' : GoodTree {keys = filter (zk >) $ filter (yk <) keys} = rewrite sym p5 in c in
  let d' : GoodTree {keys = filter (zk <) $ filter (yk <) keys} = rewrite sym p6 in d in
  let l' = BlackNode xk xv a' b' {kp = p1} in
  let r' = BlackNode zk zv c' d' {kp = inFilter (yk <) (zk ==) p0 _ zkp} in
  Evidence Red $ RedNode yk yv l' r' {kp = outFilter ykp}
balanceLeft zk zv (BadRedNode {kp = ykp} yk yv a@(BlackNode _ _ _ _) b@(BlackNode _ _ _ _)) c =
  Evidence Black $ BlackNode {kp = zkp} zk zv (RedNode {kp = ykp} yk yv a b) c
balanceLeft zk zv (BadRedNode {kp = ykp} yk yv a@(BlackNode _ _ _ _) b@(Empty _)) c impossible
balanceLeft zk zv (BadRedNode {kp = ykp} yk yv a@(Empty _) b@(BlackNode _ _ _ _)) c impossible
balanceLeft zk zv (BadRedNode {kp = ykp} yk yv a@(Empty _) b@(Empty _)) c =
  Evidence Black $ BlackNode {kp = zkp} zk zv (RedNode {kp = ykp} yk yv a b) c

public export
balanceRight :
  (kord : LawfulOrd kt) =>
  (xk : kt) ->
  {0 xkp : In (xk ==) keys} ->
  vt xk ->
  GoodTree {height, color = colorLeft, kt, kord, keys = filter (xk >) keys, vt} ->
  BadTree {height, kt, kord, keys = filter (xk <) keys, vt} ->
  Exists \color : Color => GoodTree {height = S height, color, kt, kord, keys, vt}
balanceRight xk xv a (BadRedNode {kp = zkp} zk zv (RedNode yk yv b c {kp = ykp}) d) =
  let
    0 p0 : (arg : kt) -> (yk < arg = True) -> (xk < arg = True)
    p0 arg pp0 =
      let pp1 : (compare yk arg = LT) = convLT _ _ pp0 in
      let pp2 : (compare xk arg = LT) = transitivity xk yk arg (lemma0 xk yk (outFilter ykp)) pp1 in
      cong (\case { LT => True; _ => False }) pp2

    0 p0' : (arg : kt) -> (zk < arg = True) -> (yk < arg = True)
    p0' arg pp0 =
      let pp1 : (compare zk arg = LT) = convLT _ _ pp0 in
      let pp2 : (compare yk arg = LT) = transitivity yk zk arg (reversion2 zk yk $ lemma1 zk yk ykp) pp1 in
      cong (\case { LT => True; _ => False }) pp2

    0 p1 : (arg : kt) -> (yk > arg = True) -> (zk > arg = True)
    p1 arg pp0 =
      let pp1 : (compare arg yk = LT) = reversion2 yk arg $ convGT _ _ pp0 in
      let pp2 : (compare yk zk = LT) = reversion2 zk yk $ lemma1 zk yk ykp in
      let pp3 : (compare arg zk = LT) = transitivity arg yk zk pp1 pp2 in
      cong (\case { GT => True; _ => False }) $ reversion1 arg zk pp3

    0 p2 : (arg : kt) -> (xk > arg = True) -> (yk > arg = True)
    p2 arg pp0 =
      let pp1 : (compare arg xk = LT) = reversion2 xk arg $ convGT _ _ pp0 in
      let pp2 : (compare xk yk = LT) = lemma0 xk yk (outFilter ykp) in
      let pp3 : (compare arg yk = LT) = transitivity arg xk yk pp1 pp2 in
      cong (\case { GT => True; _ => False }) $ reversion1 arg yk pp3

    0 p3 : (filter (xk >) $ filter (yk >) keys) === (filter (xk >) keys)
    p3 = trans filterCommutative $ filterImplication p2

    0 p4 : (filter (xk <) $ filter (yk >) keys) === (filter (yk >) $ filter (zk >) $ filter (xk <) keys)
    p4 = trans filterCommutative $ trans (sym $ filterImplication p1) filterCommutative

    0 p5 : (filter (zk >) $ filter (yk <) keys) === (filter (yk <) $ filter (zk >) $ filter (xk <) keys)
    p5 = trans (cong (filter (zk >))
      $ sym $ filterImplication p0)
      $ trans (cong (filter (zk >)) filterCommutative) filterCommutative

    0 p6 : (filter (zk <) $ filter (yk <) keys) === (filter (zk <) $ filter (xk <) keys)
    p6 =
      let
        pp0 : (filter (yk <) $ filter (zk <) $ filter (xk <) keys) === (filter (zk <) $ filter (xk <) keys)
        pp0 = filterImplication p0'
        pp1 : (filter (yk <) $ filter (xk <) $ filter (zk <) keys) === (filter (yk <) $ filter (zk <) $ filter (xk <) keys)
        pp1 = cong (filter (yk <)) filterCommutative
        pp2 : (filter (xk <) $ filter (yk <) $ filter (zk <) keys) === (filter (yk <) $ filter (xk <) $ filter (zk <) keys)
        pp2 = filterCommutative
        pp3 : (filter (yk <) $ filter (zk <) keys) === (filter (xk <) $ filter (yk <) $ filter (zk <) keys)
        pp3 = sym $ filterImplication p0
        pp4 : (filter (zk <) $ filter (yk <) keys) === (filter (yk <) $ filter (zk <) keys)
        pp4 = filterCommutative
      in
      trans pp4 $ trans pp3 $ trans pp2 $ trans pp1 pp0

    0 p7 : (arg : kt) -> (xk == arg = True) -> (yk > arg = True)
    p7 arg pp0 =
      let pp1 = lemma0 xk yk (outFilter ykp) in
      let pp2 = trans (sym pp1) $ equality1 xk arg yk (convEQ xk arg pp0) in
      cong (\case { GT => True; _ => False }) $ reversion1 arg yk $ sym pp2

    0 p8 : (arg : kt) -> (zk == arg = True) -> (yk < arg = True)
    p8 arg pp0 =
      let pp1 = lemma1 zk yk ykp in
      let pp2 = trans (sym pp1) $ equality1 zk arg yk (convEQ zk arg pp0) in
      cong (\case { LT => True; _ => False }) $ reversion2 arg yk $ sym pp2
  in
  let a' : GoodTree {keys = filter (xk >) $ filter (yk >) keys} = rewrite p3 in a in
  let b' : GoodTree {keys = filter (xk <) $ filter (yk >) keys} = rewrite p4 in b in
  let c' : GoodTree {keys = filter (zk >) $ filter (yk <) keys} = rewrite p5 in c in
  let d' : GoodTree {keys = filter (zk <) $ filter (yk <) keys} = rewrite p6 in d in
  let l' = BlackNode xk xv a' b' {kp = inFilter (yk >) (xk ==) p7 _ xkp} in
  let r' = BlackNode zk zv c' d' {kp = inFilter (yk <) (zk ==) p8 _ (outFilter zkp)} in
  Evidence Red $ RedNode yk yv l' r' {kp = outFilter $ outFilter ykp}
balanceRight xk xv a (BadRedNode {kp = ykp} yk yv b (RedNode zk zv c d {kp = zkp})) =
  let
    0 p1 : (arg : kt) -> (yk < arg = True) -> (xk < arg = True)
    p1 arg pp0 =
      let pp1 : (compare yk arg = LT) = convLT _ _ pp0 in
      let pp2 : (compare xk yk = LT) = lemma0 xk yk ykp in
      let pp3 : (compare xk arg = LT) = transitivity xk yk arg pp2 pp1 in
      cong (\case { LT => True; _ => False }) pp3

    0 p2 : (arg : kt) -> (xk > arg = True) -> (yk > arg = True)
    p2 arg pp0 =
      let pp1 : (compare arg xk = LT) = reversion2 xk arg $ convGT _ _ pp0 in
      let pp2 : (compare xk yk = LT) = lemma0 xk yk ykp in
      let pp3 : (compare arg yk = LT) = transitivity arg xk yk pp1 pp2 in
      cong (\case { GT => True; _ => False }) $ reversion1 arg yk pp3

    0 p3 : (filter (xk >) $ filter (yk >) keys) === (filter (xk >) keys)
    p3 = trans filterCommutative $ filterImplication p2

    0 p4 : (filter (xk <) $ filter (yk >) keys) === (filter (yk >) $ filter (xk <) keys)
    p4 = filterCommutative

    0 p5 : (filter (zk >) $ filter (yk <) keys) === (filter (zk >) $ filter (yk <) $ filter (xk <) keys)
    p5 =
      let
        pp0 : (filter (zk >) $ filter (xk <) $ filter (yk <) keys) === (filter (zk >) $ filter (yk <) $ filter (xk <) keys)
        pp0 = cong (filter (zk >)) filterCommutative
        pp1 : (filter (zk >) $ filter (yk <) keys) === (filter (zk >) $ filter (xk <) $ filter (yk <) keys)
        pp1 = cong (filter (zk >)) $ sym $ filterImplication p1
      in
      trans pp1 pp0

    0 p6 : (filter (zk <) $ filter (yk <) keys) === (filter (zk <) $ filter (yk <) $ filter (xk <) keys)
    p6 =
      let
        pp0 : (filter (zk <) $ filter (xk <) $ filter (yk <) keys) === (filter (zk <) $ filter (yk <) $ filter (xk <) keys)
        pp0 = cong (filter (zk <)) filterCommutative
        pp1 : (filter (zk <) $ filter (yk <) keys) === (filter (zk <) $ filter (xk <) $ filter (yk <) keys)
        pp1 = cong (filter (zk <)) $ sym $ filterImplication p1
      in
      trans pp1 pp0

    0 p7 : (arg : kt) -> (xk == arg = True) -> (yk > arg = True)
    p7 arg pp0 =
      let pp1 = lemma0 xk yk ykp in
      let pp2 = trans (sym pp1) $ equality1 xk arg yk (convEQ xk arg pp0) in
      cong (\case { GT => True; _ => False }) $ reversion1 arg yk $ sym pp2
  in
  let a' : GoodTree {keys = filter (xk >) $ filter (yk >) keys} = rewrite p3 in a in
  let b' : GoodTree {keys = filter (xk <) $ filter (yk >) keys} = rewrite p4 in b in
  let c' : GoodTree {keys = filter (zk >) $ filter (yk <) keys} = rewrite p5 in c in
  let d' : GoodTree {keys = filter (zk <) $ filter (yk <) keys} = rewrite p6 in d in
  let l' = BlackNode xk xv a' b' {kp = inFilter (yk >) (xk ==) p7 _ xkp} in
  let r' = BlackNode zk zv c' d' {kp = replace {p = In (zk ==)} (trans filterCommutative $ filterImplication p1) zkp} in
  Evidence Red $ RedNode yk yv l' r' {kp = outFilter ykp}
balanceRight _ _ _ (BadRedNode _ _ (Empty _) (BlackNode _ _ _ _)) impossible
balanceRight _ _ _ (BadRedNode _ _ (BlackNode _ _ _ _) (Empty _)) impossible
balanceRight xk xv a (BadRedNode {kp = ykp} yk yv b@(BlackNode _ _ _ _) c@(BlackNode _ _ _ _)) =
  Evidence Black $ BlackNode {kp = xkp} xk xv a (RedNode {kp = ykp} yk yv b c)
balanceRight xk xv a (BadRedNode {kp = ykp} yk yv b@(Empty _) c@(Empty _)) =
  Evidence Black $ BlackNode {kp = xkp} xk xv a (RedNode {kp = ykp} yk yv b c)

max_stars_repo_name: L-as/idris-rbtree

max_issues_repo_name: L-as/idris-rbtree

max_forks_repo_name: L-as/idris-rbtree


text:
module Http

import public Http.Uri
import public Http.Error
import public Http.RawResponse
import public Http.Request
import public Http.Response
import public Data.SortedMap
import public Data.Vect
import public Network.Socket

%access export

||| Loop until EOF.
||| TODO: Actually check for EOF instead of "all errors"
private
readResp : Socket -> String -> IO String
readResp sock buf = do
  Right (str, t) <- recv sock 65536 | Left err => pure buf
  readResp sock (buf ++ str)

private
sendRequest : Request String -> IO (Either HttpError (RawResponse String))
sendRequest req = do
    Right sock <- socket AF_INET Stream 0 | Left err => pure (Left $ HttpSocketError err)
    0 <- connect sock (Hostname host) port | err => pure (Left $ HttpSocketError err)
    Right _ <- send sock (resolveRequest fullRequest) | Left err => pure (Left $ HttpSocketError err)
    Right _ <- send sock (requestBody fullRequest) | Left err => pure (Left $ HttpSocketError err)
    str <- readResp sock ""
    pure (Right (MkRawResponse str))
  where
    host : String
    host = uriHost . uriAuth . uri $ req

    port : Int
    port = uriPort . uriAuth . uri $ req

    portHostHeader : String
    portHostHeader =
      if port `List.elem` [80, 443]
        then ""
        else ":" ++ show port

    extraHeaders : List (String, String)
    extraHeaders = let standard = [("Host", host ++ portHostHeader), ("Connection", "close")]
                       length = case length $ requestBody req of
                         Z => []
                         n => [("Content-Length", show n)]
                   in standard ++ length

    fullRequest : Request String
    fullRequest = record { headers $= insertFrom extraHeaders } req

httpRequest : Request String -> IO (Either HttpError (Response String))
httpRequest req = pure $ !(sendRequest req) >>= parseResponse

simpleHttp : Host -> Port -> (path : String) -> IO (Either HttpError (Response String))
simpleHttp host port path = do
  repl <- sendRequest (MkRequest GET (MkURI "http" (MkURIAuth Nothing Nothing host port) path [] "") "" empty)
  pure (repl >>= parseResponse)

max_stars_repo_name: uwap/idris-http

max_issues_repo_name: uwap/idris-http

max_forks_repo_name: uwap/idris-http


text:
module Test

data A = A0

giveA : HasIO io => io A
giveA = pure A0

please : HasIO io => io ()
please = do
     value_a <- giveA

     let a : A
         a = value_a

     pure ()

interface Cool a where cool : a -> a
implementation Cool A where cool x = x

help : A
help = cool (let x : String; x = "hello" in A0)


text:
import System.File

main : IO ()
main = do
    Right () <- copyFile "source.bin" "dest.bin"
        | Left err => printLn err
    pure ()


text:
module Graph_alt

import Data.Fin
import Data.Vect
import fn_to_vect
import Matrix

||| Definition of a graph as it's adacency matrix
total
Graph : (n : Nat) -> Type
Graph n = Mat_Vect n n Bool

total
self_loops : (n : Nat) -> (Graph n)
self_loops n = Identity_Bool n

total
or : Bool -> Bool -> Bool
or False False = False
or _ _ = True

total
and : Bool -> Bool -> Bool
and True True = True
and _ _ = False

total
add_self_loops : (n : Nat) -> (Graph n) -> (Graph n)
add_self_loops n adj = addMat n n Bool or adj (self_loops n)

total
mulGraphs : (n : Nat) -> (Graph n) -> (Graph n) -> (Graph n)
mulGraphs n u v = ( mulMat n n n Bool and or False u v )

total
nth_power_of_adj : (n : Nat) -> (siz : Nat) -> (Graph siz) -> (Graph siz)
nth_power_of_adj Z siz adj = self_loops siz
nth_power_of_adj (S k) siz adj =
      mulGraphs siz adj (nth_power_of_adj k siz adj)

total
Is_path_of_length : (length : Nat) -> (siz : Nat) -> (Graph siz) ->
                    (i : Fin siz) -> (j : Fin siz) -> Bool
Is_path_of_length l siz adj i j =
      index j (index i (nth_power_of_adj l siz adj ))


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

import Data.AVL.Dict

import Readability
import Readability.Process.XML

import Config.INI

import XML.DOM
import XML.XPath

import Frigg.Options
import Frigg.Error
import Frigg.Effs

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

%default partial
%access export

-- ------------------------------------------------------------------- [ Begin ]

getMappings : INIElem -> Dict String Double
getMappings (INIFile is) =
    Dict.fromList $ catMaybes $ map getMap is
  where
    getMap : INIElem -> Maybe (String, Double)
    getMap (INIFile is)       = Nothing
    getMap (INISection t kvs) = Nothing
    getMap (INIEntry k v)     =
      let val = (the (Double) (cast v)) in
        case val < 0 of
          True  => Nothing
          False => Just (toLower k, val)

getConfig : Maybe String -> Frigg (Dict String Double)
getConfig Nothing   = pure empty
getConfig (Just fn) =
  case !(readINIConfig fn) of
    Left  err => pure empty
    Right res => pure $ getMappings res

getTemplateWeightings : Frigg (Dict String Double)
getTemplateWeightings = getConfig $ weights !getOptions

getGradingScale : Eff (Dict String Double) FriggEffs
getGradingScale = getConfig $ gscale !getOptions

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

max_stars_repo_name: jfdm/frigg-tool

max_issues_repo_name: jfdm/frigg-tool

max_forks_repo_name: jfdm/frigg-tool


text:
module Graph

import Data.Vect
import Lemmas

%default total

||| 'Graph n' is the type of undirected graphs with no parallel edges and no self-loops with 'n' vertices.
||| Vertex '0' corresponds to the innermost AddVertex call in the graph expression.
||| Vertex '1' corresponds to the penultimate AddVertex call in the graph expression.
||| ...
||| Vertex 'n-1' corresponds to the outermost AddVertex call in the graph expression.
||| The second argument of AddVertex is a Vect of Bools, where the 'i'-th entry indicates whether
|||   the current vertex should be connected to the 'i'-th vertex of the graph.
public export
data Graph : Nat -> Type where
  Empty     : Graph 0
  AddVertex : Graph n -> Vect n Bool -> Graph (S n)

||| The complete graph on 'n' vertices.
export
completeGraph : (n : Nat) -> Graph n
completeGraph 0 = Empty
completeGraph (S k) = AddVertex (completeGraph k) (replicate k True)

||| The graph with one vertex. Same as 'completeGraph 1'.
export
singletonGraph : Graph 1
singletonGraph = AddVertex Empty []

||| A convenient representation of a graph cut.
||| The 'i'-th entry indicates the color of the 'i'-th vertex in the cut.
public export
Cut : Nat -> Type
Cut n = Vect n Bool

||| Helper function fot sizeCut
|||
||| color  -- Color of the current vertex
||| cut    -- Colors of the other vertices
||| edges  -- Vect of edges between the current vertex and the others
||| output -- Number of edges between the current vertex and the other vertices of a different color
sizeCut' : (color : Bool) -> (cut : Vect n Bool) -> (edges : Vect n Bool) -> Nat
sizeCut' _ [] [] = 0
sizeCut' True (False :: cut) (True :: edges) = S (sizeCut' True cut edges)
sizeCut' False (True :: cut) (True :: edges) = S (sizeCut' False cut edges)
sizeCut' color (_::cut) (_::edges) = sizeCut' color cut edges

||| Compute the size of a cut of a graph.
|||
||| graph  -- The input graph of the problem
||| cut    -- The given cut
||| output -- The size of the cut
export
sizeCut : (graph : Graph n) -> (cut : Cut n) -> Nat
sizeCut Empty [] = 0
sizeCut (AddVertex graph edges) cut =
  let x = last cut
      smaller_cut = init cut
  in sizeCut' x smaller_cut edges + sizeCut graph smaller_cut

||| Find the best cut of a graph among a vector of cuts (or the trivial cut if the vector is []).
|||
||| n      -- The size of the input graph of the problem
||| graph  -- The input graph of the problem
||| cuts   -- Vector of cuts
||| output -- The best cut from the vector and its size
export
bestCut : {n : Nat} -> (graph : Graph n) -> (cuts : Vect k (Cut n)) -> (Cut n, Nat)
bestCut graph [] = (replicate n True, 0)
bestCut graph (cut::cuts) =
  let (best, size) = bestCut graph cuts
      s = sizeCut graph cut
  in if s >= size then (cut, s) else (best,size)

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module Examples.Fractals

import Control.Applicative.Syntax
import Data.DPair
import Data.Either
import Data.IORef
import Data.MSF.Switch
import Data.Nat
import Data.So
import Examples.CSS.Fractals
import Examples.Fractals.Dragon
import Examples.Util
import Generics.Derive
import Rhone.JS

%language ElabReflection
%default total

--------------------------------------------------------------------------------
--          Model
--------------------------------------------------------------------------------

data Fractal = Dragon

%runElab derive "Fractal" [Generic,Meta,Show,Eq]

data Ev = Fract Fractal | Iter | Redraw | Run | Inc

%runElab derive "Ev" [Generic,Meta,Show,Eq]

MaxIter : Nat
MaxIter = 18

record Iterations where
  constructor MkIterations
  value : Nat
  0 prf : LTE value MaxIter

namespace Iterations
  export
  fromInteger :  (n : Integer)
              -> {auto 0 prf : LTE (fromInteger n) MaxIter}
              -> Iterations
  fromInteger n = MkIterations (cast n) prf

  export
  read : String -> Either String Iterations
  read "0" = Right $ MkIterations 0 LTEZero
  read s = case cast {to = Nat} s of
    0 => Left "Not a natural number: \{s}"
    n => case isLTE n MaxIter of
      Yes prf   => Right $ MkIterations n prf
      No contra => Left "Value must be <= \{show MaxIter}"

isDelay : Bits32 -> Bool
isDelay v = 100 <= v && v <= 10000

record RedrawAfter where
  constructor RA
  value : Bits32
  0 prf : So (isDelay value)

namespace RedrawAfter
  export
  read : String -> Either String RedrawAfter
  read s =
    let v = cast {to = Bits32} s
     in case choose (isDelay v) of
          Left oh => Right $ RA v oh
          Right _ => Left $ "Enter a value between 100 and 10'000"

record Config where
  constructor MkConfig
  fractal    : Fractal
  iterations : Iterations
  redraw     : RedrawAfter

--------------------------------------------------------------------------------
--          Controller
--------------------------------------------------------------------------------

public export
M : Type -> Type
M = DomIO Ev JSIO

msf : (timer : RedrawAfter -> JSIO ()) -> MSF M Ev ()
msf timer = drswitchWhen neutral config fractal
  where fractal : Config -> MSF M Ev ()
        fractal c =
          let Element dragons prf = mkDragons c.iterations.value
           in ifIs Inc $ cycle dragons >>> innerHtml out

        readAll : MSF M Ev (Either String Config)
        readAll =    MkConfig Dragon
                <$$> getInput Iter   read txtIter
                <**> getInput Redraw read txtRedraw
                >>>  observeWith (isLeft ^>> disabledAt btnRun)

        config : MSF M Ev (MSFEvent Config)
        config =   fan [readAll, is Run]
               >>> rightOnEvent
               >>> observeWith (ifEvent $ arrM (liftJSIO . timer . redraw))

--------------------------------------------------------------------------------
--          View
--------------------------------------------------------------------------------

content : Node Ev
content =
  div [ class fractalContent ]
    [ lbl "Number of iterations:" lblIter
    , input [ ref txtIter
            , onInput (const Iter)
            , onEnterDown Run
            , class widget
            , placeholder "Range: [0, \{show MaxIter}]"
            ] []
    , lbl "Iteration delay [ms]:" lblDelay
    , input [ ref txtRedraw
            , onInput (const Redraw)
            , onEnterDown Run
            , class widget
            , placeholder "Range: [100,10'000]"
            ] []
    , button [ref btnRun, onClick Run, classes [widget,btn]] ["Run"]
    , div [ref out] []
    ]

--------------------------------------------------------------------------------
--          UI
--------------------------------------------------------------------------------

export
ui : M (MSF M Ev (), JSIO ())
ui = do
  innerHtmlAt exampleDiv content
  ref  <- newIORef {a = Maybe IntervalID} Nothing
  h    <- handler <$> env

  let cleanup : JSIO ()
      cleanup = readIORef ref >>= traverse_ clearInterval

      timer   : RedrawAfter -> JSIO ()
      timer ra = do
        cleanup
        newID <- setInterval ra.value (h Inc)
        writeIORef ref (Just newID)

  pure (msf timer, cleanup)


text:
data MyShow : Type -> Type where
     ShowImplementation : (show : a -> String) -> MyShow a

myshow : {auto inst : MyShow a} -> a -> String
myshow {inst = ShowImplementation show} x1 = show x1

%hint
showNat : MyShow Nat
showNat = ShowImplementation show

%hint
showFn : MyShow (a -> b)
showFn = ShowImplementation (\x => "<< function >>")

%hint
showBools : MyShow (Bool, Bool)
showBools = ShowImplementation (\x => "some bools")

%hint
showStuff : MyShow a -> MyShow b -> MyShow (a, b)
showStuff sa sb = ShowImplementation showPair
  where
    showPair : (a, b) -> String
    showPair (x, y) = myshow x ++ ", " ++ myshow y

testShow : List (Bool, Bool) -> String
testShow [] = ""
testShow (x :: xs) = myshow x ++ "\n" ++ testShow xs

testShow2 : List (Nat, Int -> Int) -> String
testShow2 [] = ""
testShow2 (x :: xs) = myshow x ++ "\n" ++ testShow2 xs

main : IO ()
main = do putStrLn $ testShow2 [(2, (+1)), (3, abs)]
          putStrLn $ testShow [(True, False), (False, True)]


text:
module Toolkit.Data.DList.DeBruijn

import public Decidable.Equality

import public Data.List.Elem

import public Toolkit.Data.List.DeBruijn

import public Toolkit.Data.DList
import public Toolkit.Data.DList.Elem

%default total

namespace DList

  public export
  Context : (idx      : Type)
         -> (type     : idx -> Type)
         -> (indicies : List idx)
                     -> Type
  Context = DList

  public export
  Contains : (idxType  : Type)
          -> (typeType : idxType -> Type)

          -> {indicies : List idxType}

          -> (ctxt : Context idxType typeType indicies)
          -> {idx  : idxType}
          -> (type : typeType idx)
                  -> Type
  Contains idxType typeType xs x = Elem idxType typeType x xs

  ||| Append `x` to the head of `xs`.
  public export
  (+=) : {v : a}
      -> (xs : DList a e vs)
      -> (x  : e v)
            -> DList a e (v::vs)
  (+=) xs x = x :: xs

{- A nice to have below, work in progress.

namespace Renaming

  public export
  weaken : {idx : typeIdx}
        -> {type' : typeType idx}
        -> (func : Contains typeIdx typeType old type
                -> Contains typeIdx typeType new type)
        -> (Contains typeIdx typeType (old += type') type
         -> Contains typeIdx typeType (new += type') type)

  weaken func (H (Same Refl Refl)) = H (Same Refl Refl)
  weaken func (T rest)             = T (func rest)

  public export
  interface Rename (idxType  : Type)
                   (typeType : idxType -> Type)
                   (term     : {indicies : List idxType}
                            -> {idx      : idxType}
                            -> (context  : DList idxType typeType indicies)
                            -> (type     : typeType idx)
                                        -> Type)
      | term
    where

      rename : {indiciesOld : List idxType}
            -> {indiciesNew : List idxType}
            -> {old : DList idxType typeType indiciesOld}
            -> {new : DList idxType typeType indiciesNew}
            -> (f : {level : idxType}
                 -> {type  : typeType level}
                          -> Contains idxType typeType old type
                          -> Contains idxType typeType new type)
           -> ({level : idxType}
            -> {type  : typeType level}
                     -> term old type
                     -> term new type)

      var : {indicies : List idxType}
         -> {ctxt     : DList idxType typeType indicies}
         -> {idx      : idxType}
         -> {type     : typeType idx}
                     -> Elem idxType typeType type ctxt
                     -> term ctxt type

--  weakens : {idxType  : Type}
--         -> {typeType : idxType -> Type}
--         -> {term     : {indicies : List idxType}
--                     -> {idx      : idxType}
--                     -> (context  : DList idxType typeType indicies)
--                     -> (type     : typeType idx)
--                                 -> Type}
--         -> Rename idxType typeType term
--         => {indiciesOld : List idxType}
--         -> {indiciesNew : List idxType}
--         -> {old : DList idxType typeType indiciesOld}
--         -> {new : DList idxType typeType indiciesNew}
--         -> {level' : idxType}
--         -> {type' : typeType level'}
--         -> (f : {level : idxType}
--              -> {type  : typeType level}
--                       -> Contains idxType typeType old type
--                       -> term                      new type)
--         -> ({level : idxType}
--          -> {type  : typeType level}
--                   -> Contains idxType typeType (type' :: old) type
--                   -> term                      (type' :: new) type)
--  weakens f (H (Same Refl Refl)) = var (H (Same Refl Refl))
--  weakens f (T rest)             = rename T (f rest)

namespace Substitution

  namespace General
    public export
    interface Rename idx type term
           => Substitute (idxType  : Type)
                         (typeType : idxType -> Type)
                         (term     : {indicies : List idxType}
                                  -> {idx      : idxType}
                                  -> (context  : DList idxType typeType indicies)
                                  -> (type     : typeType idx)
                                              -> Type)
         | term
       where

         subst : {old, new : List type}
              -> (f : {ty  : type}
                          -> Contains old ty
                          -> term     new ty)
              -> ({ty : type}
                     -> term old ty
                     -> term new ty)
(f : {level : Universe}
            -> {type  : MTy level}
                     -> Types.Contains old type
                     -> SystemV new type)
       -> ({level : Universe}
        -> {type  : MTy level}
                 -> SystemV old type
                 -> SystemV new type)

--  namespace Single
--
--    apply : {type : Type}
--         -> {term : List type -> type -> Type}
--         -> Rename type term
--         => {ctxt   : List type}
--         -> {typeA  : type}
--         -> {typeB  : type}
--         -> (this   : term      ctxt    typeB)
--         -> (idx    : Contains (ctxt += typeB) typeA)
--                   -> term      ctxt           typeA
--    apply this Here = this
--    apply this (There rest) = var rest
--
--    export
--    subst : {type : Type}
--         -> {term : List type -> type -> Type}
--         -> Rename type term
--         => Substitute type term
--         => {ctxt          : List type}
--         -> {typeA         : type}
--         -> {typeB         : type}
--         -> (this          : term  ctxt           typeB)
--         -> (inThis        : term (ctxt += typeB) typeA)
--                          -> term  ctxt           typeA
--    subst {ctxt} {typeA} {typeB} this inThis
--      = subst (apply this) inThis

-}
-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Main

ok : String -> String
ok s = if length s `mod` 2 == 0 then reverse s else s

main : IO ()
main = putStrLn $ substr 3 2 ( ok "abcdefghjklmnopqrstuvw")

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 Main

data InfList : Type -> Type where
  (::) : (value : elem) -> Inf (InfList elem) -> InfList elem

%name InfList xs, ys, zs

total
countFrom : Integer -> InfList Integer
countFrom x = x :: countFrom (x + 1)

total
getPrefix : (count : Nat) -> InfList ty -> List ty
getPrefix Z xs = []
getPrefix (S k) (value :: xs) = value :: getPrefix k xs

labelWith : Stream labelType -> List a -> List (labelType, a)
labelWith xs [] = []
labelWith (x :: xs) (y :: ys) = (x, y) :: labelWith xs ys

label : List a -> List (Int, a)
label = labelWith (iterate (+1) 0)

main : IO ()
main = do
  printLn $ getPrefix 10 $ countFrom 2 -- [2,3,4,5,6,7,8,9,10,11]
  printLn $ label [1..7] -- [(0,1) .. (6, 7)]
  printLn $ labelWith (cycle ["a", "b", "c"]) [1..5] -- [("a",1), ("b".2), ("c",3), ("a",4), ("b",5)]

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module InsertInput

import State
import Cursor
import Document

%default total

public export
data InsertInput : Type where
  InsertChar : Char -> InsertInput
  InsertNormal : InsertInput
  InsertNewLine : InsertInput
  InsertBackspace : InsertInput

parseChar : Char -> InsertInput
parseChar c =
  case (ord c) of
    127 => InsertBackspace
    13 => InsertNewLine
    27 => InsertNormal
    _ => InsertChar c

export
getInsertInput : IO InsertInput
getInsertInput = parseChar <$> getChar

max_stars_repo_name: PeterHajdu/peti

max_issues_repo_name: PeterHajdu/peti

max_forks_repo_name: PeterHajdu/peti


text:
module Replica.TestConfig

import public Replica.TestConfig.Core
import public Replica.TestConfig.Lexer
import public Replica.TestConfig.Parser

max_stars_repo_name: xvw/REPLica

max_issues_repo_name: xvw/REPLica

max_forks_repo_name: xvw/REPLica


text:
data DumbNumber = Naught | One | Two |Three

data Natural = Zero | After Natural

-- A polymorphic list
data MyList a = Blank | (::) a (MyList a)

first : MyList a -> Maybe a
first Blank = Nothing
first (x :: xs) = Just x

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 DataStore


text:
module RedBlackSet

import Set

%default total
%access private

data Color = R | B

export
data RedBlackSet a = E | T Color (RedBlackSet a) a (RedBlackSet a)

balance : Color -> RedBlackSet a -> a -> RedBlackSet a -> RedBlackSet a
balance B (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)
balance B (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)
balance B a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)
balance B a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)
balance color a x b = T color a x b

export
Ord a => Set RedBlackSet a where
  empty = E

  member x E = False
  member x (T _ a y b) = case compare x y of
    LT => member x a
    GT => member x b
    EQ => True

  insert x s = assert_total $ let T _ a y b = ins s in T B a y b
   where
    ins : Ord a => RedBlackSet a -> RedBlackSet a
    ins E = T R E x E
    ins s'@(T color a y b) = case compare x y of
      LT => balance color (ins a) y b
      GT => balance color a y (ins b)
      EQ => s'


text:
||| Provide a prompt and apply function to user input
||| ex. myRepl "Enter a string: " reverse
repl : (prompt : String) -> (String -> String) -> IO ()
repl prompt f = do putStrLn prompt
                   input <- getLine
                   putStrLn (f input)
                   repl prompt f

-- dummy helper for testing
processInput : List String -> String -> Maybe (String, List String)
processInput xs input = Just ("Added item, count = " ++ show (length xs + 1), input :: xs )

||| Given a state and prompt,  apply a function to the state and user input
||| ex. replWith [] "Enter a string: " processInput
replWith : (state: a) -> (prompt : String) -> (a -> String -> Maybe (String, a)) -> IO ()
replWith state prompt f = do putStrLn prompt
                             input <- getLine
                             let Just (output, newState) = f state input
                               | Nothing => replWith state prompt f
                             putStrLn output
                             replWith newState prompt f


text:
module DB.SQLite.SQLiteTest

import Effects
import DB.SQLite.Effect
import DB.SQLite.SQLiteCodes

testInsert : String -> Int -> Eff (Either QueryError ()) [SQLITE ()]
testInsert name age =
  do open_db <- openDB "test.db"
     case open_db of
       Left err => return $ Left err
       Right () =>
         do let sql = "INSERT INTO `test` (`name`, `age`) VALUES (?, ?);"
            prep_res <- prepareStatement sql
            case prep_res of
              Left err => do cleanupPSFail ; return $ Left err
              Right () =>
                do bindText 1 name
                   bindInt 2 age
                   bind_res <- finishBind
                   case bind_res of
                     Just err => do cleanupBindFail ; return $ Left err
                     Nothing =>
                       case !executeStatement of
                         Unstarted => do finalise
                                         closeDB
                                         pure (Right ())
                         StepFail => do finalise
                                        closeDB
                                        pure (Right ())
                         StepComplete => do finalise
                                            closeDB
                                            pure (Right ())
                         NoMoreRows => do finalise
                                          closeDB
                                          pure (Right ())

testSelect : Eff (Either QueryError ResultSet) [SQLITE ()]
testSelect =
  executeSelect "test.db" "SELECT `name`, `sql` FROM `sqlite_master`;" [] $
  do name <- getColumnText 0
     sql <- getColumnText 1
     return [DBText name, DBText sql]

namespace Main
  main : IO ()
  main = do select_res <- run $ testInsert "foo" 29
            case select_res of
                 Left err => putStrLn $ "Error: " ++ (show err)
                 Right () => putStrLn $ "Done"
            select_res <- run $ testSelect
            case select_res of
              Left err => putStrLn $ "Error reading: " ++ show err
              Right res => putStrLn (show res)

-- -}
-- -}
-- -}

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
module ReverseVec

import Data.Vect

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse (x :: xs) = reverseProof (myReverse xs ++ [x])
  where
    reverseProof : Vect (k + 1) elem -> Vect (S k) elem
    reverseProof {k} res = rewrite sym (plusCommutative k 1) in res
    -- Used sym for fun to get the hang of reversing direction of rewrites


text:
module Control.Validation

-- Main purpose of this module is verifying programmer's assumptions about
-- user input. On one hand we want to write precisely typed programs, including
-- assumptions about input expressed in types and prove correctness of these
-- programs. On the other we get an unstructured user input as a string or even
-- a raw sequence of bytes.

-- This module intends to provide a framework for verifying our assumptions
-- about user input and constructing proofs that input is indeed valid or
-- failing early with a nice error message if it isn't.

import Control.Monad.Identity
import Control.Monad.Error.Either
import Data.Nat
import Data.String
import Data.Vect
import Decidable.Equality

%default total

public export
Result : (Type -> Type) -> Type -> Type
Result m = EitherT String m

||| Validators in this module come in two flavours: Structural Validators and
||| Property Validators. They are both wrappers around functions which take
||| some input and confirm that it's valid (returning some witness of its
||| validity) or fail with an error described by a string.
export
data ValidatorT : (Type -> Type) -> Type -> Type -> Type where
    MkValidator : (a -> Result m b) -> ValidatorT m a b

||| A type of validator trying to prove properties of values. It's type is
||| significantly different than that of an ordinary validator and cannot be
||| made an instance of Monad interface, because it's last parameter is
||| (t -> Type) instead of just Type. Therefore it must be explicitly turned
||| into an ordinary validator using the prop function below.
data PropValidator : (Type -> Type) -> (t : Type) -> (t -> Type) -> Type where
    MkPropValidator : ((x : t) -> Result m (p x)) -> PropValidator m t p

public export
Validator : Type -> Type -> Type
Validator = ValidatorT Identity

||| Run validation on given input, returning (Right refinedInput) if everything
||| is all right or (Left errorMessage) if it's not.
export
validateT : ValidatorT m a b -> a -> Result m b
validateT (MkValidator v) = v

||| Run validation within the Identity monad and unwrap result immediately.
export
validate : Validator a b -> a -> Either String b
validate v = runIdentity . runEitherT . validateT v

||| Given a function from input to Either String output, make a validator.
export
validator : (a -> Result m b) -> ValidatorT m a b
validator = MkValidator

export
Functor m => Functor (ValidatorT m a) where
    map f v = MkValidator (map f . validateT v)

export
Monad m => Applicative (ValidatorT m a) where
    pure a = MkValidator (const $ pure a)
    f <*> a = MkValidator (\x => validateT f x <*> validateT a x)

export
Monad m => Monad (ValidatorT m a) where
    v >>= f = MkValidator $ \x => do
        r <- validateT v x
        validateT (f r) x

||| Plug a property validator into the chain of other validators. The value
||| under validation will be ignored and the value whose property is going to
||| be checked must be supplied manually. Otherwise Idris won;t be able to
||| unify.
prop : PropValidator m t p -> (x : t) -> ValidatorT m a (p x)
prop (MkPropValidator v) x = MkValidator (const $ v x)

replaceError : Monad m => String -> Result m a -> Result m a
replaceError e = bimapEitherT (const e) id

||| Replace validator's default error message.
export
withError : Monad m => String -> ValidatorT m a b -> ValidatorT m a b
withError e (MkValidator f) = MkValidator (replaceError e . f)

||| A validator which always fails with a given message.
export
fail : Applicative m => String -> ValidatorT m a b
fail s = MkValidator $ \_ => left s

infixl 2 >>>

||| Compose two validators so that the second validates the output of the first.
export
(>>>) : Monad m => ValidatorT m a b -> ValidatorT m b c -> ValidatorT m a c
left >>> right = MkValidator (validateT left >=> validateT right)

Monad m => Alternative (ValidatorT m a) where
    left <|> right = MkValidator $ \x => MkEitherT $ do
        case !(runEitherT $ validateT left x) of
            (Right r) => pure $ Right r
            (Left e) => case !(runEitherT $ validateT right x) of
                (Right r) => pure $ Right r
                (Left e') => pure $ Left (e <+> " / " <+> e')

    empty = MkValidator $ \x => MkEitherT $ pure (Left "invalid")

||| Alter the input before validation using given function.
export
contramap : (a -> b) -> ValidatorT m b c -> ValidatorT m a c
contramap f v = MkValidator (validateT v . f)

||| Given a value x and a decision procedure for property p, validateT if p x
||| holds, returning a proof if it does. The procedure also has access to the
||| raw input in case it was helpful.
export
decide : Monad m => (t -> String) -> ((x : t) -> Dec (p x)) -> PropValidator m t p
decide msg dec = MkPropValidator $ \x => case dec x of
    Yes prf => pure prf
    No _ => left (msg x)

||| Given a function converting a into Maybe b, build a Validator of a
||| converting it into b.
export
fromMaybe : Monad m => (a -> String) -> (a -> Maybe b) -> ValidatorT m a b
fromMaybe e f = MkValidator $ \a => case f a of
    Nothing => left $ e a
    Just b => pure b

||| Verify whether a String represents a natural number.
export
natural : Monad m => ValidatorT m String Nat
natural = fromMaybe mkError parsePositive
    where
    mkError : String -> String
    mkError s = "'" <+> s <+> "' is not a natural number."

||| Verify whether a String represents an Integer
export
integral : (Num a, Neg a, Monad m) => ValidatorT m String a
integral = fromMaybe mkError parseInteger
    where
    mkError : String -> String
    mkError s = "'" <+> s <+> "' is not an integer."

||| Verify that a string represents a decimal fraction.
export
double : Monad m => ValidatorT m String Double
double = fromMaybe mkError parseDouble
    where
    mkError : String -> String
    mkError s = "'" <+> s <+> "is not a decimal."

||| Verify whether a list has a desired length.
export
length : Monad m => (l : Nat) -> ValidatorT m (List a) (Vect l a)
length l = MkValidator (validateVector l)
    where
    validateVector : (l : Nat) -> List a -> Result m (Vect l a)
    validateVector Z [] = pure []
    validateVector (S _) [] = left "Missing list element."
    validateVector Z (_ :: _) = left "Excessive list element."
    validateVector (S k) (x :: xs) = do
        ys <- validateVector k xs
        pure (x :: ys)

||| Verify that certain values are equal.
export
equal : (DecEq t, Monad m) => (a : t) -> PropValidator m t (\b => a = b)
equal a = MkPropValidator $ \b => case decEq a b of
    Yes prf => pure prf
    No _ => left "Values are not equal."

||| Verify that a Nat is less than or equal to  certain bound.
export
lteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LTE bound)
lteNat bound = decide
    (\n => show n <+> " is not lower or equal to " <+> show bound)
    (\n => isLTE n bound)

||| Verify that a Nat is greater than or equal to certain bound.
export
gteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GTE bound)
gteNat bound = decide
    (\n => show n <+> " is not greater or equal to " <+> show bound)
    (isLTE bound)

||| Verify that a Nat is strictly less than a certain bound.
export
ltNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LT bound)
ltNat bound = decide
    (\n => show n <+> " is not strictly lower than " <+> show bound)
    (\n => isLTE (S n) bound)

||| Verify that a Nat is strictly greate than a certain bound.
export
gtNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GT bound)
gtNat bound = decide
    (\n => show n <+> " is not strictly greater than " <+> show bound)
    (isLTE (S bound))


text:
module Verified.Monad

import Verified.Applicative

%default total

class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
  monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
                     mf <*> mx = mf >>= \f =>
                                 mx >>= \x =>
                                        pure (f x)
  monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x
  monadRightIdentity : (mx : m a) -> mx >>= return = mx
  monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
                       (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
module Compiler.Codegen.VmcodeSexp

import Data.List
import Data.String
import System
import System.File

import Core.Directory
import Core.CompileExpr
import Core.Context
import Compiler.Common
import Compiler.VMCode
import Libraries.Utils.Path

import Data.Sexp
import Compiler.VMCodeSexp

dumpFgn : (Name, FC, NamedDef) -> String
dumpFgn (n, _, def@(MkNmForeign cs args ret)) = show (toSexp (n, def)) ++ "\n"
dumpFgn _ = "" -- not a foreign function

dumpDef : (Name, VMDef) -> String
dumpDef d = (show $ toSexp d) ++ "\n\n"

compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
        ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs tmpDir outputDir term outfile = do
  let appDirRel = outfile ++ "_rapid" -- relative to build dir
  let appDirGen = outputDir </> appDirRel -- relative to here
  let outputFileName = appDirGen </> (outfile ++ ".sexp") -- VMCode S-exp
  Right () <- coreLift $ mkdirAll appDirGen
    | Left err => do coreLift_ $ putStrLn $ "ERROR" ++ show err
                     pure Nothing

  cd <- getCompileData False VMCode term
  let foreignDecls = map dumpFgn (namedDefs cd)
  let compiledFunctions = map dumpDef (vmcode cd)

  coreLift $ do
    (Right outFile) <- openFile outputFileName WriteTruncate
    | Left err => putStrLn $ "error opening output file: " ++ show err
    ignore $ fPutStr outFile $ fastAppend foreignDecls
    for_ compiledFunctions (fPutStr outFile)
    ignore $ closeFile outFile
    pure ()

  pure $ Nothing

execute : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
execute defs tmpDir term = do coreLift $ putStrLn "Can't execute VMCode directly"

export
vmcodeSexp : Codegen
vmcodeSexp = MkCG compile execute

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Libgit.Examples

import Control.Monad.Managed

import Libgit

-- Clone a repository and print some information about the success of the
-- operation.
export
testClone : String -> String -> String -> IO ()
testClone url localPath branch = do
  res <- withGit $ runManaged $ do
    eRes <- repository (GitRepositoryClone (MkCloneOpts False branch) url localPath)
    let result = case eRes of
                   Left res => "Error: " ++ show res
                   Right _ => "Cloned repository"
    liftIO $ putStrLn result
  case res of
    Left err => putStrLn ("Error initializing: " ++ show err)
    Right _ => putStrLn "Success"

-- Open a repository and reset its head to a given commit/tag
export
resetRepo : (path : String) -> (rev : String) -> IO ()
resetRepo path rev = do
  withGit $ runManaged $ do
    Right repo <- repository (GitRepositoryOpen path)
      | Left err => putStrLn ("Error opening repo: " ++ show err)
    Right (objTyp ** obj) <- revParse repo rev
      | Left err => putStrLn ("Error parsing revision: " ++ show err)
    case objTyp of
      GitObjectCommit => liftIO resetRepo
      GitObjectTag => liftIO resetRepo
      _ => liftIO (putStrLn "Wrong object type")
  pure ()
  where
    resetRepo : {auto repo : GitRepository}
             -> {auto typ : GitObjectType}
             -> {auto obj : GitObject typ}
             -> {auto 0 prf : IsCommitish typ}
             -> IO ()
    resetRepo {repo} {obj} = do
      0 <- liftIO (resetRepository repo obj GitResetHard)
        | err => putStrLn ("Error resetting repo: " ++ show err)
      putStrLn "Successfully reset repo"

-- Open a repository and fetch a remote
export
fetchRemote : (path : String) -> (remote : String) -> IO ()
fetchRemote path rev = do
  withGit $ runManaged $ do
    Right repo <- repository (GitRepositoryOpen path)
      | Left err => putError ("Error opening repo: " ++ show err)
    Right remote <- remote repo "origin"
      | Left err => putError ("Error looking up remote: " ++ show err)
    0 <- liftIO (remoteFetch' remote "Fetched from Idris")
      | err => putError ("Error fetching remote: " ++ show err)
    putStrLn "Fetch successful."
  pure ()
  where
    putError : HasIO io => String -> io ()
    putError msg = liftIO $ do
      putStrLn msg
      case lastError of
        Just (msg, _) => putStrLn msg
        Nothing => putStrLn "No git error present"

max_forks_repo_name: bigs/libgit-idris


text:
module LightClick.IR.Channel.Normalise.Merge

import Data.List
import Data.Vect

import Toolkit.Data.DList
import Toolkit.Data.DVect

import LightClick.Types
import LightClick.Terms

import LightClick.IR.ModuleCentric
import LightClick.IR.ChannelCentric
import LightClick.IR.Channel.Normalise.Error

%default total

data State = Empty | RepeatedName | UniqueNames (List String) | InlineModule

||| If the name has been seen return nothing, otherwise extend the state.
updateState : State -> String -> State
updateState Empty y = UniqueNames [y]
updateState RepeatedName y = RepeatedName
updateState (UniqueNames xs) y with (isElem y xs)
  updateState (UniqueNames xs) y | (Yes prf) = RepeatedName
  updateState (UniqueNames xs) y | (No contra) = UniqueNames (y::xs)

updateState InlineModule y = InlineModule

||| A ChannelIR specification is in module normal form if each CModuleInst has a unique type.
|||
||| Returns nothing if a name is repeated, other wise a list of unique names.
isModuleNF : (state : State)
          -> (expr  : ChannelIR type)
                   -> State
isModuleNF state (CLet n beThis inThis)
  = isModuleNF (isModuleNF state beThis) inThis

isModuleNF state (CSeq this thenThis)
  = isModuleNF (isModuleNF state this) thenThis

isModuleNF state (CModuleInst (CRef mname MODULE) xs)
  = updateState state mname

isModuleNF state (CModuleInst mname xs)  = InlineModule
isModuleNF state expr = state

||| Remove all instances of CModuleInst and merge them together.
mergeModules : (state : List (String, (ChannelIR MODULE, List (String, ChannelIR CHAN))))
            -> (expr  : ChannelIR type)
                     -> ChannelIR type
mergeModules state (CLet x y z)
  = CLet x (mergeModules state y) (mergeModules state z)
mergeModules state (CSeq (CModuleInst m@(CRef name MODULE) cs) y)
  = mergeModules ((name, (m,toList cs))::state) y

mergeModules state (CSeq x y) = CSeq x (mergeModules state y)

mergeModules state CEnd = rebuild CEnd (reduce Nil state)
  where
    rebuild : ChannelIR UNIT
           -> List (String, (ChannelIR MODULE, List (String, ChannelIR CHAN)))
           -> ChannelIR UNIT
    rebuild u Nil     = u
    rebuild u ((_,(m,Nil))::xs) = (rebuild u xs) -- shouldn't happen
    rebuild u ((_,(m,c::cs))::xs) = CSeq (CModuleInst m (c::(fromList cs))) (rebuild u xs)

    action : String
          -> ChannelIR MODULE
          -> List (String, ChannelIR CHAN)
          -> List (String, (ChannelIR MODULE, List (String, ChannelIR CHAN)))
          -> List (String, (ChannelIR MODULE, List (String, ChannelIR CHAN)))
    action k inst cs Nil                          = [(k,(inst,cs))]
    action k inst cs ((name, (inst', cs')) :: rest) with (decEq k name)
      action k inst cs ((k, (inst', cs')) :: rest) | (Yes Refl)
        = (k, (inst', cs ++ cs')) :: rest
      action k inst cs ((name, (inst', cs')) :: rest) | (No contra)
        = (name, (inst', cs')) :: (action k inst cs rest)

    reduce : List (String, (ChannelIR MODULE, List (String, ChannelIR CHAN))) -- turn into map
          -> List (String, (ChannelIR MODULE, List (String, ChannelIR CHAN)))
          -> List (String, (ChannelIR MODULE, List (String, ChannelIR CHAN)))
    reduce new Nil = new
    reduce new ((k,(inst, cs))::xs) = reduce (action k inst cs new) xs

mergeModules state expr = expr

export
covering
runMerge : ChannelIR type -> Either Normalise.Error (ChannelIR type)
runMerge expr =
  case isModuleNF Empty expr of
    Empty => Left (NoModuleInstances)
    InlineModule => Left (ModuleInlined)
    RepeatedName => runMerge (mergeModules Nil expr)
    UniqueNames _ => Right expr

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

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module G4LowerFormalPSpring

%access public export
%default total

-- 形式的体系P
-- 数項化された自然数
GNat : Type
GNat = Nat

-- 10.6.1 基本記号のゲーデル数
左かっこ : GNat
左かっこ = 11
右かっこ : GNat
右かっこ = 13