text:
-- Copyright (c) 2013 Radek Micek

module Solver

import Algo

partial
hd : List a -> a
hd (x :: _) = x
-- missing case: hd []

partial
tl : List a -> List a
tl (_ :: xs) = xs
-- missing case: tl []

partial
fromJust : Maybe a -> a
fromJust (Just x) = x
-- missing case: fromJust Nothing

groupBy : (a -> a -> Bool) -> List a -> List (List a)
groupBy _ [] = []
groupBy eq (x :: xs) =
  let (ys, zs) = span (eq x) xs in
  (x :: ys) :: groupBy eq zs

Var : Type
Var = String

data Sign = Pos | Neg

instance Eq Sign where
  Pos == Pos = True
  Neg == Neg = True
  _ == _ = False

instance Ord Sign where
  compare Pos Pos = EQ
  compare Neg Neg = EQ
  compare Pos Neg = LT
  compare Neg Pos = GT

data Lit = MkLit Sign Var

instance Eq Lit where
  (MkLit sign var) == (MkLit sign' var') = sign == sign' && var == var'

instance Ord Lit where
  compare (MkLit s v) (MkLit s' v') =
    case compare s s' of
      LT => LT
      GT => GT
      EQ => compare v v'

instance Show Lit where
  show (MkLit Pos lit) = lit
  show (MkLit Neg lit) = strCons '~' lit

data CId = MkCId Nat

instance Eq CId where
  (MkCId x) == (MkCId y) = x == y

-- Must not contain any duplicate literals.
data Clause = MkClause CId (List Lit)

-- Decision level.
Level : Type
Level = Nat

Ante : Type
Ante = CId

Trail : Type
Trail = List (Lit, Maybe Ante, Level)

data Operation
  = OOther
  -- Current conflict clause, original conflict clause, processed variables.
  | OLearn (List Lit) Clause (List Var)
  | OMinimize (List Lit)
  -- Processed clauses, remaining clauses.
  | OPropagate (List Clause) (List Clause)

-- Solver state.
record Sol : Type where
  MkSol : (sClauses : List Clause) ->
          (sLevel : Level) ->
          (sTrail : Trail) ->
          (sOp : Operation) ->
          -- Corresponding clauses contain negations of the literals.
          (sWatched : List (CId, (Lit, Lit))) ->
          (sChosen : Maybe Lit) ->
          (sEnableMinimization : Bool) ->
          (sEnableWatchedLits : Bool) ->
          Sol

data Event
  -- Nonempty list of unassigned variables.
  = EChoose (List Var)
  | EDecide Lit
  | EProp Lit Clause
  | EConfl Clause
  | EWShortClause Lit Clause
  | EWPropLitStart Lit
  -- Watched literal which is being propagated,
  -- other watched literal which is true, clause.
  | EWOtherLitTrue Lit Lit Clause
  -- Watched literal which is being propagated,
  -- not watched literal which is not false, clause.
  | EWReplaceLit Lit Lit Clause
  -- Watched literal which is being propagated,
  -- other watched literal which is false, clause.
  | EWConfl Lit Lit Clause
  -- Watched literal which is being propagated,
  -- other watched literal which is unassigned, clause.
  | EWProp Lit Lit Clause
  | EAnalyzeStart Clause
  -- Variable to be resolved on, current conflict clause,
  -- antecedent clause of the variable, resolvent.
  | EResolve Var (List Lit) Clause (List Lit)
  | ESkip Var (List Lit) Clause
  | EAnalyzeEnd (List Lit)
  -- Candidates for removal, asserting clause.
  | EMinStart (List Lit) (List Lit)
  | ETestRedundant Lit (List Lit)
  | ERedundant Lit (List Lit)
  | ENotRedundant Lit (List Lit)
  -- Redundant literals, original asserting clause,
  -- minimized asserting clause.
  | EMinEnd (List Lit) (List Lit) (List Lit)
  | ELearn Clause
  | EBacktrack Lit (Maybe Clause)

SatAlgo : Type -> Type -> Type
SatAlgo = Algo Sol Event

data LBool = LTrue | LFalse | LUndef

instance Eq LBool where
  LTrue == LTrue = True
  LFalse == LFalse = True
  LUndef == LUndef = True
  _ == _ = False

Assignment : Type
Assignment = Lit -> LBool

emptySol : Sol
emptySol = MkSol [] 0 [] OOther [] Nothing True True

negLit : Lit -> Lit
negLit (MkLit Pos l) = MkLit Neg l
negLit (MkLit Neg l) = MkLit Pos l

getLits : Clause -> List Lit
getLits (MkClause _ lits) = lits

findInTrail : Var -> Trail -> Maybe (Lit, Maybe Ante, Level)
findInTrail var = find (\(MkLit _ v, _, _) => v == var)

findClause : CId -> List Clause -> Clause
findClause cid = fromJust . find (\(MkClause cid' _) => cid == cid')

trailToAssig : Trail -> Assignment
trailToAssig trail l =
  let (MkLit _ var) = l in
  case findInTrail var trail of
    Nothing => LUndef
    Just (l', _, _) => if l == l' then LTrue else LFalse

data Prop = Unit Lit | Conflict

testClause : Assignment -> Clause -> Maybe Prop
testClause assig (MkClause _ lits) =
  if sat then
    Nothing
  else
    -- Note: nub is redundant when clause has no duplicate literals.
    case List.nub $ filter ((== LUndef) . assig) lits of
      [] => Just Conflict
      [l] => Just $ Unit l
      _ => Nothing
  where
    sat = not $ isNil $ filter ((== LTrue) . assig) lits

-- Manages decision level.
assign : Lit -> Maybe Ante -> SatAlgo r ()
assign l ante = do
  s <- get
  let trail = sTrail s
  let lvl : Nat =
    case ante of
      Nothing => sLevel s + 1
      Just _ => sLevel s
  put (record { sTrail = (l, ante, lvl) :: trail, sLevel = lvl } s)

findClauseToProp : Assignment -> List Clause -> Maybe (Clause, Prop)
findClauseToProp _ [] = Nothing
findClauseToProp assig (c::cs) =
  case testClause assig c of
    Just p => Just (c, p)
    Nothing => findClauseToProp assig cs

-- Unit propagation. Returns conflict clause.
propagate : SatAlgo r (Maybe Clause)
propagate = do
  s <- get
  let assig = trailToAssig $ sTrail s
  let clauses = sClauses s
  let clause = findClauseToProp assig clauses
  case clause of
    Just (cl, Unit l) => do
      let MkClause cid _ = cl
      assign l $ Just cid
      interrupt $ EProp l cl
      propagate
    Just (cl, Conflict) => return $ Just cl
    Nothing => return Nothing

wpropagate : SatAlgo r (Maybe Clause)
wpropagate = do
    confl <- propagateShort
    case confl of
      Just _ => return confl
      _ => firstLit >>= propagateWatched
  where
    findShortToProp : Assignment -> List Clause -> Maybe (Clause, Prop)
    findShortToProp _ [] = Nothing
    findShortToProp _ (MkClause cid [] :: _) =
      Just (MkClause cid [], Conflict)
    findShortToProp assig (MkClause cid [l] :: cs) =
      case assig l of
        LTrue => findShortToProp assig cs
        LFalse => Just (MkClause cid [l], Conflict)
        LUndef => Just (MkClause cid [l], Unit l)
    findShortToProp assig (_ :: cs) = findShortToProp assig cs

    propagateShort : SatAlgo r (Maybe Clause)
    propagateShort = do
      s <- get
      if sLevel s == 0 then
        case findShortToProp (trailToAssig $ sTrail s) (sClauses s) of
          Nothing => return Nothing
          -- There should be no empty clause.
          Just (cl, Conflict) => return $ Just cl
          Just (MkClause cid lits, Unit l) => do
            assign l $ Just cid
            interrupt $ EWShortClause l $ MkClause cid lits
            propagateShort
      else
        return Nothing

    -- The first literal in the propagation queue.
    firstLit : SatAlgo r (Maybe Lit)
    firstLit = do
      s <- get
      case dropWhile (\(_, _, lvl) => lvl /= sLevel s) $ reverse (sTrail s) of
        [] => return $ Nothing
        (l, _, _) :: _ => return $ Just l

    -- Next literal in the propagation queue.
    nextLit : Lit -> SatAlgo r (Maybe Lit)
    nextLit lit = do
      s <- get
      case dropWhile (\(l, _, _) => l /= lit) $ reverse (sTrail s) of
        _ :: (l, _, _) :: _ => return $ Just l
        _ => return Nothing

    propagateWatched : Maybe Lit -> SatAlgo r (Maybe Clause)
    -- Propagation queue is empty.
    propagateWatched Nothing = return Nothing
    propagateWatched (Just lit) = do
        s <- get

        -- Find clauses where lit is watched.
        let clauses : List Clause =
          map (\(cid, _) => findClause cid $ sClauses s)
            $ filter (\(cid, (l, l')) => l == lit || l' == lit)
            $ sWatched s

        putOp [] clauses

        interrupt $ EWPropLitStart (negLit lit)

        confl <- propClauses [] clauses
        case confl of
          Nothing => nextLit lit >>= propagateWatched
          confl => return confl
      where
        putOp : List Clause -> List Clause -> SatAlgo r ()
        putOp proc remaining = do
          s <- get
          case remaining of
            [] => put (record { sOp = OOther } s)
            _ :: _ => put (record { sOp = OPropagate proc remaining } s)
        propClauses : List Clause -> List Clause -> SatAlgo r (Maybe Clause)
        propClauses proc [] = return Nothing
        propClauses proc (c :: cs) = do
          putOp (c :: proc) cs
          s <- get

          let (MkClause cid lits) = c
          let (_, (wl, wl')) = fromJust
                                 $ List.find (\(cid', _) => cid == cid')
                                 $ sWatched s
          let lit' = (wl == lit) ? wl' : wl
          let assig = trailToAssig $ sTrail s

          case assig $ negLit lit' of
            LTrue => do
              interrupt $ EWOtherLitTrue (negLit lit) (negLit lit') c
              propClauses (c :: proc) cs
            a =>
              -- Find replacement for lit.
              case
                find (\l => negLit l /= lit &&
                            negLit l /= lit' &&
                            assig l /= LFalse)
                     lits
              of
                Just newLit => do
                  -- Replace watched literal.
                  s2 <- get
                  let (ws, ws') = List.break (\(cid', _) => cid == cid')
                                    $ sWatched s2
                  let watched : List (CId, (Lit, Lit)) =
                    ws ++ ((cid, (negLit newLit, lit')) :: tl ws')
                  put (record { sWatched = watched } s2)

                  interrupt $ EWReplaceLit (negLit lit) newLit c
                  propClauses (c :: proc) cs
                Nothing =>
                  if a == LFalse then do
                    putOp (c :: proc) []
                    interrupt $ EWConfl (negLit lit) (negLit lit') c
                    return $ Just c
                  else do
                    assign (negLit lit') $ Just cid
                    interrupt $ EWProp (negLit lit) (negLit lit') c
                    propClauses (c :: proc) cs

unassignedVars : Assignment -> List Clause -> List Var
unassignedVars assig clauses =
  filter ((== LUndef) . assig . MkLit Pos) vars
  where
    varsInClause : Clause -> List Var
    varsInClause (MkClause _ lits) = nub $ map (\(MkLit _ var) => var) lits
    vars : List Var
    vars = nub $ concatMap varsInClause clauses

choose : SatAlgo r (Maybe Lit)
choose = do
  s <- get
  let vars = unassignedVars (trailToAssig $ sTrail s) (sClauses s)

  case vars of
    [] => return Nothing
    _ :: _ =>
      case sChosen s of
        Nothing => do
          interrupt $ EChoose vars
          choose
        Just (MkLit sign v) => do
          put (record { sChosen = Nothing } s)
          if v `elem` vars then
            return $ Just $ MkLit sign v
          -- Chosen literal isn't among unassigned literals.
          else
            choose

addClause' : List Lit -> Maybe (Lit, Lit) -> SatAlgo r Clause
addClause' lits watch = do
  s <- get
  let clauses = sClauses s
  let cid = MkCId $ length clauses + 1
  let cl = MkClause cid lits
  let watched =
    if sEnableWatchedLits s then
      case watch of
        Just (l, l') => sWatched s ++ [(cid, (negLit l, negLit l'))]
        Nothing =>
          case lits of
            l :: l' :: _ => sWatched s ++ [(cid, (negLit l, negLit l'))]
            _ => sWatched s
    else
      sWatched s
  put (record { sClauses = clauses ++ [cl], sWatched = watched } s)
  return cl

addClause : List Lit -> SatAlgo r Clause
addClause lits = addClause' lits Nothing

-- Literal must be assigned.
litToLevel : Trail -> Lit -> Level
litToLevel trail (MkLit _ v) = level $ fromJust $ findInTrail v trail
  where
    level (_, _, l) = l

litRedundant : List Lit -> Lit -> SatAlgo r Bool
litRedundant assertingCl = \l => get >>= litRedundant' (negLit l)
  where
    -- Literal must be in the trail (i.e. it must be true).
    litRedundant' : Lit -> Sol -> SatAlgo r Bool
    litRedundant' literal s = do
        let (MkLit _ variable) = literal
        let (_, antecedent, _) = fromJust $ findInTrail variable $ sTrail s
        let anteLits = getLits $ findClause (fromJust antecedent) $ sClauses s
        let queue = List.map negLit $ filter (/= literal) anteLits
        let (b, highlight) = bfs queue $ map (\l => (l, Nothing)) queue

        put (record { sOp = OMinimize highlight } s)
        interrupt $ ETestRedundant (negLit literal) assertingCl

        put (record { sOp = OOther } s)
        if b then
          interrupt $ ERedundant (negLit literal) assertingCl
        else
          interrupt $ ENotRedundant (negLit literal) assertingCl

        return b
      where
        Redundant : Type
        Redundant = Bool
        Marked : Type
        Marked = (Lit, Maybe Lit)
        bfs : List Lit -> List Marked -> (Redundant, List Lit)
        bfs [] marked = (True, map fst marked) -- Literal is redundant.
        bfs (q :: qs) marked =
          -- Literal ~q is in asserting clause.
          if negLit q `elem` assertingCl then
            bfs qs marked
          else
            let (MkLit _ var) = q in
            case fromJust $ findInTrail var (sTrail s) of
              -- Literal isn't redundant.
              (_, Nothing, _) => (False, constructPath q)
              (_, Just _, O) => bfs qs marked
              (_, Just cid, _) =>
                let newLits : List Lit =
                  filter (\l => all ((/= l) . fst) marked) -- l is not marked.
                    $ map negLit
                    $ filter (/= q)
                    $ getLits
                    $ findClause cid (sClauses s) in
                -- Add antecedents to the queue and mark them.
                bfs
                  (qs ++ newLits)
                  (marked ++ map (\l => (l, Just q)) newLits)
          where
            constructPath : Lit -> List Lit
            constructPath lit =
              case fromJust $ find (\(l, _) => l == lit) marked of
                (_, Nothing) => [lit]
                (_, Just l) => lit :: constructPath l

-- Common.filterM doesn't work for some reason.
filterM' : (a -> SatAlgo r Bool) -> List a -> SatAlgo r (List a)
filterM' _ [] = return List.Nil
filterM' p (x :: xs) = do
  b <- p x
  ys <- filterM' p xs
  return (b ? List.(::) x ys : ys)

minimize : List Lit -> SatAlgo r (List Lit)
minimize assertingCl = do
    s <- get

    let candidates : List Lit =
      map (negLit . getLit)
        -- Skip decided literals.
        $ filter (\(_, ante, _) => isJust ante)
        -- Skip literal from current decision level.
        $ filter (\(_, _, lvl) => sLevel s /= lvl)
        $ List.map fromJust
        $ List.map (\(MkLit _ var) => findInTrail var $ sTrail s) assertingCl

    interrupt $ EMinStart candidates assertingCl

    redundant <- filterM' (litRedundant assertingCl) candidates
    let newAssertingCl = filter (\l => List.all (/= l) redundant) assertingCl

    interrupt $ EMinEnd redundant assertingCl newAssertingCl

    return newAssertingCl
  where
    getLit : (Lit, Maybe Ante, Level) -> Lit
    getLit (l, _, _) = l

isAsserting : List Lit -> Level -> Trail -> Bool
isAsserting lits level trail = (List.length $ filter (== level) levels) == 1
  where
      levels : List Nat
      levels = map (litToLevel trail) $ nub lits

-- Returns a learned clause.
-- If decision level > 0 then the learned clause is nonempty.
analyzeConflict : Clause -> SatAlgo r (List Lit)
analyzeConflict conflClause = do
    let conflLits = getLits conflClause
    s <- get
    put (record { sOp = OLearn conflLits conflClause [] } s)
    interrupt $ EAnalyzeStart conflClause
    assertingLits <- resolve s (sTrail s) conflLits []
    put (record { sOp = OOther } s)
    interrupt $ EAnalyzeEnd assertingLits
    return assertingLits
  where
    partial
    resolve : Sol -> Trail -> List Lit -> List Var -> SatAlgo r (List Lit)
    resolve s trail lits procVars =
      if isAsserting lits (sLevel s) (sTrail s) then
        return lits
      else
        case trail of
          (MkLit _ var, Just ante, _) :: ts => do
            let procVars' = var :: procVars
            let anteCl = findClause ante $ sClauses s
            if find (\(MkLit _ v) => v == var) lits == Nothing then do
              put (record { sOp = OLearn lits conflClause procVars' } s)
              interrupt $ ESkip var lits anteCl
              resolve s ts lits procVars'
            -- var is among lits, so we resolve it out.
            else do
              let anteLits = getLits anteCl
              let resolvent =
                List.nub
                  $ filter (\(MkLit _ v) => v /= var)
                  $ lits ++ anteLits
              put (record { sOp = OLearn resolvent conflClause procVars' } s)
              interrupt $ EResolve var lits anteCl resolvent
              resolve s ts resolvent procVars'
          -- missing case: []

-- Assumes that every literal in the clause is assigned.
computeBacktrackLevel : List Lit -> Trail -> (Level, Maybe (Lit, Lit))
computeBacktrackLevel lits trail =
  case groupBy sameLevel $ reverse $ sort lits' of
    ((_, l) :: _) :: ((lvl, l') :: _) :: _ => (lvl, Just (l, l'))
    _ => (0, Nothing)
  where
    lits' : List (Level, Lit)
    lits' = map (\l => (litToLevel trail l, l)) lits
    sameLevel : (Level, Lit) -> (Level, Lit) -> Bool
    sameLevel (l, _) (l2, _) = l == l2

backtrack : Level -> SatAlgo r ()
backtrack level = do
  s <- get
  let trail = sTrail s
  case trail of
    (lit, ante, l) :: ts =>
      if l > level then do
        put (record { sTrail = ts } s)
        let cl = [| findClause ante (pure $ sClauses s) |]
        interrupt (EBacktrack lit cl)
        backtrack level
      else
        put $ record { sLevel = level } s
    [] =>
      put $ record { sLevel = level } s

data Result = Sat | Unsat

instance Eq Result where
  Sat == Sat = True
  Unsat == Unsat = True
  _ == _ = False

instance Show Result where
  show Sat = "Sat"
  show Unsat = "Unsat"

solve : SatAlgo r Result
solve = do
  conflCl <- get >>= (\s => (sEnableWatchedLits s) ? wpropagate : propagate)
  case conflCl of
    Nothing => do
      lit <- choose
      case lit of
        -- All variables are assigned.
        Nothing => return Sat
        Just l => do
          assign l Nothing
          interrupt (EDecide l)
          solve
    Just confl => do
      interrupt (EConfl confl)
      s <- get
      if sLevel s == 0 then
        return Unsat
      else do
        assertingCl <- analyzeConflict confl
        assertingCl' <-
          (sEnableMinimization s) ? minimize assertingCl : return assertingCl
        let (blevel, watch) = computeBacktrackLevel assertingCl' (sTrail s)
        learned <- addClause' assertingCl' watch
        interrupt (ELearn learned)
        backtrack blevel
        solve

-- ---------------------------------------------------------------------------
-- Parser

whitespace : Char -> Bool
whitespace c = c == ' ' || c == '\t' || c == '\n' || c == '\r'

asciiIdent : String -> Bool
asciiIdent s with (unpack s)
  asciiIdent _ | [] = False
  asciiIdent _ | (x :: xs) = asciiAlphaUsc x && all asciiAlphaNumUsc xs
  where
    asciiAlphaUsc : Char -> Bool
    asciiAlphaUsc c =
      (c >= 'A' && c <= 'Z') || (c >= 'a' && c <= 'z') || c == '_'
    asciiAlphaNumUsc : Char -> Bool
    asciiAlphaNumUsc c = asciiAlphaUsc c || (c >= '0' && c <= '9')

parseLit' : List Char -> Either String Lit
parseLit' str =
  case lit of
    MkLit _ v =>
      if not $ asciiIdent v then
        Left $ "Invalid identifier: '" ++ v ++ "'"
      else
        Right lit
  where
    str' : List Char
    str' = filter (not . whitespace) str
    lit : Lit
    lit =
      case str' of
        '~' :: var => MkLit Neg (pack var)
        '!' :: var => MkLit Neg (pack var)
        var => MkLit Pos (pack var)

-- Tolerates literal separator after the last literal.
parseLits' : List Char -> Either String (List Lit)
parseLits' str =
  if all whitespace str then
    Right []
  else
    let (litStr, restStr) = break litSep str in
    case (parseLit' litStr, parseLits' $ drop 1 restStr) of
      (Left err, _) => Left err
      (_, Left err) => Left err
      (Right l, Right ls) => Right $ l :: ls
  where
    litSep : Char -> Bool
    litSep c = c == ',' || c == '|' || c == ';'

parseLit : String -> Either String Lit
parseLit = parseLit' . unpack

parseLits : String -> Either String (List Lit)
parseLits = parseLits' . unpack

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
module Fs

%access public export

%inline
jscall : (fname : String) -> (ty : Type) ->
          {auto fty : FTy FFI_JS [] ty} -> ty
jscall fname ty = foreign FFI_JS fname ty

FsModule : Type
FsModule = Ptr

FilePath : Type
FilePath = String

Contents : Type
Contents = String

fsModule : JS_IO FsModule
fsModule = jscall "require('fs')" (JS_IO FsModule)

readFileSync : FilePath -> JS_IO String
readFileSync filename = do
  fsModule' <- fsModule
  jscall "%0.readFileSync(%1, 'utf8')" (FsModule -> String -> JS_IO String) fsModule' filename

writeFileSync : FilePath -> Contents -> JS_IO ()
writeFileSync filename contents = do
  fsModule' <- fsModule
  jscall "%0.writeFileSync(%1, %2, 'utf8')" (FsModule -> String -> String -> JS_IO ()) fsModule' filename contents

ext: idr

max_stars_repo_name: idris-industry/idris-free

max_issues_repo_name: idris-industry/idris-free

max_forks_repo_name: idris-industry/idris-free


text:
module VecSort

import Data.Vect

insertElement : Ord elem => (x : elem) -> (xsSorted : Vect len elem) -> Vect (S len) elem
insertElement x [] = [x]
insertElement x (y :: ys) = case x < y of
                                 False => y :: insertElement x ys
                                 True => x :: y :: ys

insSort : Ord elem => Vect n elem -> Vect n elem
insSort [] = []
insSort (x :: xs) = let xsSorted = insSort xs in
                        insertElement x xsSorted

-- Exercises
my_length : List a -> Nat
my_length [] = 0
my_length (x :: xs) = S (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  -- why doesn't this overload?
my_map2 f [] = []
--my_map2 f (x :: xs) = ?my_map2_rhs_2  -- <leader>o to search and...
my_map2 f (x :: xs) = f x :: my_map2 f xs  -- BOOM!

max_stars_repo_name: neduard/type-driven-development

max_issues_repo_name: neduard/type-driven-development

max_forks_repo_name: neduard/type-driven-development


text:
module Js.Node

{-
import Effects
import public Js.ASync
import public Js.ServiceTypes
import Data.SortedMap

require : String -> JS_IO Ptr
require s = jscall "require(%0)" (String -> JS_IO Ptr) s

export
err2Either : ASync Ptr -> ASync (Either String Ptr)
err2Either x =
  do
    y <- x
    errQ <- liftJS_IO $ jscall "%0[0] ? 1 : 0" (Ptr -> JS_IO Int) y
    if errQ == 1 then
      do
        msg <- liftJS_IO $ jscall "%0[0] + ''" (Ptr -> JS_IO String) y
        pure $ Left msg
      else
        do
          res <- liftJS_IO $ jscall "%0[1]" (Ptr -> JS_IO Ptr) y
          pure $ Right res

export
handleErr : ASync Ptr -> ASync Ptr
handleErr x  =
  do
    z <- err2Either x
    case z of
      Left e => debugError e
      Right res => pure res

export
readFileJS_IO : String -> JS_IO String
readFileJS_IO file =
  do
    fs <- require "fs"
    jscall "%0.readFileSync(%1)" (Ptr -> String -> JS_IO String) fs file

export
readFileASync : String -> ASync String
readFileASync f =
  do
    map (\x => the String (believe_me x)) $ handleErr $ MkASync $ \proc =>
      do
        jscall
          "require('fs').readFile(%0, 'utf8', function(e,c){%1([e,c])} )"
          (String -> JsFn (Ptr -> JS_IO ()) -> JS_IO () )
          f
          (MkJsFn $ proc)

export
data FileIO : Effect where
  ReadFile : String -> sig FileIO String

export
implementation Handler FileIO ASync where
  handle () (ReadFile s) k = do x <- readFileASync s; k x ()

public export
FILEIO : EFFECT
FILEIO = MkEff () FileIO

export
readFile : String -> Eff String [FILEIO]
readFile s = call $ ReadFile s

export
data RequestState = MkRequestState Ptr Ptr

export
data WSState = MkWSState Ptr (List String)

export
data WebSocket : Effect where
  WSSend : String -> sig WebSocket () WSState WSState
  WSReceive : sig WebSocket String WSState WSState

public export
WEBSOCKET : (ty : Type) -> EFFECT
WEBSOCKET t = MkEff t WebSocket

export
data Request : Effect where
  EndRequest : String -> sig Request () RequestState ()

public export
REQUEST : (ty : Type) -> EFFECT
REQUEST t = MkEff t Request

export
implementation Handler Request ASync where
  handle (MkRequestState req resp) (EndRequest s) k = do liftJS_IO $ jscall "%0.end(%1)" (Ptr -> String -> JS_IO ()) resp s ; k () ()

procReqRaw : (RequestState -> ASync ()) -> Ptr -> JS_IO ()
procReqRaw handler x =
  do
    req <- jscall "%0[0]" (Ptr -> JS_IO Ptr) x
    resp <- jscall "%0[1]" (Ptr -> JS_IO Ptr) x
    setASync_ $  handler $ MkRequestState req resp

export
runServer : (XS : List EFFECT) -> Env ASync XS -> Int ->
                EffM ASync () (REQUEST RequestState :: XS) (\_ => REQUEST () :: XS) -> JS_IO ()
runServer xs inits port handler =
  do
    http <- require "http"
    server <- jscall
                "%0.createServer(function(req, res){return %1([req,res])})"
                (Ptr -> (JsFn (Ptr -> JS_IO ())) -> JS_IO Ptr )
                http
                (MkJsFn $ procReqRaw (\x => runInit (x::inits) handler) )
    jscall
      ("%0.listen(%1, function(err){" ++
       " if(err){" ++
       "  console.log('Error starting server',err)" ++
       " }else{" ++
       "  console.log('server is listnening on port', %1)" ++
       "}" ++
       "})")
      (Ptr -> Int -> JS_IO ()) server port

export
endRequest : String -> Eff () [REQUEST RequestState] [REQUEST ()]
endRequest s = call $ EndRequest s
-}

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
occurrences : Eq ty => (item : ty) -> (values : List ty) -> Nat
occurrences item [] = 0
occurrences item (x :: xs) = case x == item of
                                  False => occurrences item xs
                                  True => 1 + occurrences item xs

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Issue893

%default total

foo : (a, b : Nat) -> Bool
foo  Z    b = False
foo (S _) b = False

notFoo : (a, b : Nat) -> Not (foo a b = True)
notFoo  Z    _ = uninhabited
notFoo (S _) _ = uninhabited

bar : (a, b : Nat) -> (foo a b) && c = foo a b
bar a b with (foo a b) proof ab
  bar a b | True  = absurd $ notFoo a b ab
  bar a b | False = Refl

goo : (a, b : Nat) -> Bool -> Bool
goo a b True = True
goo a b False = foo a b || foo a b

bar2 : (a, b : Nat) -> goo a b (foo a b) = foo a b
bar2 a b with (foo a b) proof ab
  bar2 a b | True = Refl
  bar2 a b | False = rewrite ab in Refl


text:
module Replica.Command.Info

import Data.String

import Replica.Help
import Replica.Option.Filter
import Replica.Option.Global
import Replica.Option.Types
import Replica.Other.Decorated

%default total

public export
record InfoCommand' (f : Type -> Type) where
  constructor MkInfo
  showExpectation : f Bool
  filter : Filter' f
  global : Global' f

public export
InfoCommand : Type
InfoCommand = Done InfoCommand'

export
TyMap InfoCommand' where
  tyMap func x = MkInfo
    (func x.showExpectation)
    (tyMap func x.filter) (tyMap func x.global)

export
TyTraversable InfoCommand' where
  tyTraverse func x = [| MkInfo
      (func x.showExpectation)
      (tyTraverse func x.filter) (tyTraverse func x.global)
      |]

export
Show InfoCommand where
  show i = unwords [ "MkInfo"
                   , show i.showExpectation
                   , show i.filter
                   , show i.global]

showExpectationPart : Part (Builder InfoCommand') Bool
showExpectationPart = inj $ MkOption
      ( singleton
        $ MkMod (singleton "expectations") ['e'] (Left True)
          "show expectation for each test")
      False
      go
  where
    go : Bool -> Builder InfoCommand' -> Either String (Builder InfoCommand')
    go = ifSame showExpectation
                (\x => record {showExpectation = Right x})
                (const $ const "Contradictory values for expectations")

optParseInfo : OptParse (Builder InfoCommand') InfoCommand
optParseInfo = [|MkInfo
  (liftAp showExpectationPart)
  (embed filter (\x => record {filter = x}) optParseFilter)
  (embed global (\x => record {global = x}) optParseGlobal)
  |]

defaultInfo : Default InfoCommand'
defaultInfo = MkInfo
  (defaultPart showExpectationPart)
  defaultFilter
  defaultGlobal

export
parseInfo : List1 String -> ParseResult InfoCommand
parseInfo ("info":::xs) = case parse (initBuilder defaultInfo) optParseInfo xs of
  InvalidMix reason => InvalidMix reason
  InvalidOption ys => InvalidMix "Unknown option: \{ys.head}"
  Done x => maybe (InvalidMix "File is not set") Done $ build x
parseInfo xs = InvalidOption xs

export
helpInfo : Help
helpInfo =
  commandHelp {b = Builder InfoCommand'}
    "info" "Display information about test suites"
    optParseInfo
    (Just "JSON_TEST_FILE")

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module Decidable.Decidable

import Data.Rel
import Data.Fun

||| Interface for decidable n-ary Relations
public export
interface Decidable (ts : Vect k Type) (p : Rel ts) where
  total decide : liftRel ts p Dec

||| Given a `Decidable` n-ary relation, provides a decision procedure for
||| this relation.
decision : (ts : Vect k Type) -> (p : Rel ts) -> (Decidable ts p) => liftRel ts p Dec
decision ts p = decide {ts} {p}

using (a : Type, x : a)
  public export
  data Given : Dec a -> Type where
    Always : Given (Yes x)


text:
module GTLC
import Data.Fin
import Data.Vect
import Data.So

%default total

-- The Representation of types
mutual
  data Ty  = TyDyn | TyInt | TyBool | TyFun Ty Ty

mutual
  -- The representation of Dyn values
  data Dyn : Type where
    inj : (t : Ty) -> (x : interpTy t) -> Dyn

  -- Convert Ty to Type in proof land
  data Ty2T : Ty -> Type -> Type where
    d2d : Ty2T TyDyn Dyn
    i2i : Ty2T TyInt Int
    b2b : Ty2T TyBool Bool
    f2f : Ty2T a b -> Ty2T c d -> Ty2T (TyFun a c) (b -> Maybe d)

  -- Compute the real type of interpreted Ty values
  total
  interpTy : Ty -> Type
  interpTy TyDyn       = Dyn
  interpTy TyInt       = Int
  interpTy TyBool      = Bool
  interpTy (TyFun A T) = (interpTy A) -> Maybe (interpTy T)

  -- Proof that two Types are consistent
data consistTy : Ty -> Ty -> Type where
  refl  : consistTy a     a
  dynR  : consistTy a     TyDyn
  dynL  : consistTy TyDyn a
  funC  : consistTy a b -> consistTy c d -> consistTy (TyFun a c) (TyFun b d)

data joinTy : Ty -> Ty -> Ty -> Type where
  const : joinTy a     a     a
  right : joinTy TyDyn a     a
  left  : joinTy a     TyDyn a
  under : joinTy a     b     c -> joinTy d e f ->
            joinTy (TyFun a d) (TyFun b e) (TyFun c f)

-- I am Interested in how this is implemented but it represents a type index
-- that allows variables types to be computed computed while typechecking.
using (G : Vect n Ty)

-- An index for variable types
  data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
    Stop : HasType FZ (t :: G) t
    Pop  : HasType k G t -> HasType (FS k) (u :: G) t

-- The Explicitly Typed Cast Calculus
  data Expr : Vect n Ty -> Ty -> Type where
    Var   : HasType i G t -> Expr G t
    ValI  : (v : Int)  -> Expr G TyInt
    ValB  : (v : Bool) -> Expr G TyBool
    ILam  : Expr (a :: G) t -> Expr G (TyFun a t)
    IApp  : Expr G (TyFun a t) -> Expr G a -> Expr G t
    IOp   : (interpTy a -> interpTy b -> interpTy c) ->
             Expr G a -> Expr G b -> Expr G c
    IIf   : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a
    ICast : Expr G t -> (t : Ty) -> (g : Ty) -> Expr G g

  mkCast : Expr G t1 -> (t1 : Ty) -> (t2 : Ty) -> (p : consistTy t1 t2) -> Expr G t2
  mkCast e s t p = (ICast e s t)
--  mkCast refl s t e = e -- mkCast is really dumb currently

-- Lam is an unannotated lambda
  Lam : Expr (TyDyn :: G) t -> Expr G (TyFun TyDyn t)
  Lam = ILam
-- LamT is a lambda that accecpts a non dynamic type annotation
  LamT : (t : Ty) -> Expr (t :: G) g -> Expr G (TyFun t g)
  LamT t = ILam

-- If is the "smart" constructor for if terms
  If : Expr G tt -> Lazy (Expr G tc) -> Lazy (Expr G ta) ->
        {auto ct : consistTy tt TyBool} ->
        {auto cc : consistTy tc tr} ->
        {auto ca : consistTy ta tr} ->
        Expr G tr
  If {ct=dynL}{cc}{ca} t c a = If {ct=refl}{cc}{ca} (ICast t TyDyn TyBool) c a
  If {ct=refl}{cc=refl}{ca=refl} t c a = IIf t c a
  If {ct=refl}{tc}{ta}{tr} t c a = IIf t (ICast c tc tr) (ICast a ta tr)

-- App is the smart constructor for Application terms
  data AppRule : Ty -> Ty -> Ty -> Type where
   fApp : AppRule (TyFun a b) a     b
   dApp : AppRule TyDyn       TyDyn TyDyn

  App :  Expr G tf -> Expr G ta -> {auto ar : AppRule tf ra rr} ->
     {auto cf : consistTy tf (TyFun ra rr)} -> {auto ca : consistTy ta ra} -> Expr G rr
  App f a {cf} {ca} {tf} {ra} {rr} {ta} = IApp (mkCast f tf (TyFun ra rr) cf)
                                               (mkCast a ta ra ca)

-- Op is the smart constructor for operators

  Op  : (interpTy oa -> interpTy ob -> interpTy c) -> Expr G aa -> Expr G ab ->
           {auto pa : consistTy aa oa} ->
           {auto pb : consistTy ab ob} -> Expr G c
  Op p a b {pa} {aa} {oa} {pb} {ab} {ob}  = IOp p (mkCast a aa oa pa) (mkCast b ab ob pb)

-- The lexical environment of the interpreter
  data Env : Vect n Ty -> Type where
    Nil  : Env Nil
    (::) : interpTy a -> Env G -> Env (a :: G)

-- Lookup of lexical values in the interpreter
  lookup : HasType i G t -> Env G -> interpTy t
  lookup Stop    (x :: xs) = x
  lookup (Pop k) (x :: xs) = lookup k xs

  mutual
-- Cast between types computed in the smart constructors
    rtCast : (t : Ty) -> (g : Ty) -> (x : interpTy t) -> Maybe (interpTy g)
    rtCast TyDyn      TyDyn       x          = return x
    rtCast TyInt      TyInt       x          = return x
    rtCast TyBool     TyBool      x          = return x
    rtCast TyDyn      g           (inj t' x) = rtCast t' g x
    rtCast t'         TyDyn       x          = return (inj t' x)
    rtCast (TyFun a b)(TyFun c d) f          =
             return (\x => rtCast b d !(f !(rtCast c a x)))
    rtCast _          _         _          = Nothing

  -- The GTLC interpreter
    interp : Env G -> Expr G ty -> Maybe (interpTy ty)
    interp env (Var i)         = return (lookup i env)
    interp env (ValI x)        = return x
    interp env (ValB x)        = return x
    interp env (ICast x r1 r2) = ?ICast --rtCast r1 r2 !(interp env x)
    interp env (ILam b)        = return (\x => interp (x :: env) b)
    interp env (IOp op x y)    = return (op !(interp env x) !(interp env y))
    interp env (IApp f s)      = (!(interp env f) !(interp env s))
    interp env (IIf t c a)     = return (if !(interp env t)
                                         then !(interp env c)
                                         else !(interp env a))

-- unit tests
-- unit tests for consist
a2 : consistTy TyInt TyInt
a2 = refl
a0 : consistTy TyDyn TyDyn
a0 = refl
a1 : consistTy TyDyn TyBool
a1 = dynL
a3 : consistTy TyInt TyDyn
a3 = dynR
a4 : consistTy (TyFun TyInt TyBool) (TyFun TyInt TyBool)
a4 = refl
a5 : consistTy (TyFun TyInt TyBool) (TyFun TyInt TyBool)
a5 = funC refl refl
a6 : consistTy (TyFun TyDyn TyBool) (TyFun TyInt TyDyn)
a6 = funC dynL dynR
-- unit tests of coersion calculus forms
c0 : Expr [] TyInt
c0 = ValI 1
c1 : Expr [] TyBool
c1 = ValB True

-- unit tests of gradually typed forms
t0 : Expr [] TyInt
t0 = ValI 1
t0' : Expr [] TyBool
t0' = ValB True
t1 : Expr [] (TyFun TyDyn TyDyn)
t1 = Lam (Var Stop)
t2 : Expr [] (TyFun TyInt TyInt)
t2 = LamT TyInt (Var Stop)
-- unit test on the gradual If smart constructor
t3 : Expr [] TyInt
t3 = (If (ValB True) (ValI 0) (ValI 1))
t4 : Expr [TyDyn] TyInt
t4 = (If (Var Stop) (ValI 0) (ValI 1))
t5 : Expr [TyDyn] TyInt
t5 = (If (Var Stop) (Var Stop) (ValI 1))
t6 : Expr [TyDyn] TyInt
t6 = (If (Var Stop) (Var Stop) (Var Stop))
t7 : Expr [TyDyn] TyDyn
t7 = (If (Var Stop) (ValI 0) (ValB True))
-- unit tests for the gradual App smart constructor
t8 : Expr [] TyInt
t8 = App (LamT TyInt (Var Stop)) (ValI 1)
t9 : Expr [] TyDyn
t9 = App (Lam (Var Stop)) (ValI 1)
t10 : Expr [] TyDyn
t10 = App (Lam (If (Var Stop) (ValI 0) (Var Stop))) (ValI 1)

sub1 : Expr [] (TyFun TyInt TyInt)
sub1 = LamT TyInt (Op (-) (Var Stop) (ValI 1))

zerop : Expr [] (TyFun TyInt TyBool)
zerop = LamT TyInt (Op (==) (ValI 0) (Var Stop))

--zerod : Expr [] (TyFun TyDyn TyBool)
--zerod = Lam (Op (==) (ValI 0) (Var Stop))

{-
fact : Expr [] (TyFun TyDyn TyInt)
fact = (Lam (If (App zerop (Var Stop))
                (ValI 1)
                (Op (*) (Var Stop) (App fact (App sub1 (Var Stop))))))
-}
-- unit tests for the interpreter
i0 : Maybe Int
i0 = (interp [] (ValI 0))
i0p : i0 = Just 0
i0p = Refl
i1 : Maybe Bool
i1 = (interp [] (ValB True))
i1p : i1 = Just True
i1p = Refl

--main : IO ()
--main = putStrLn (show i0)

max_stars_repo_name: akuhlens/metaprogramming

max_issues_repo_name: akuhlens/metaprogramming

max_forks_repo_name: akuhlens/metaprogramming


text:
module JS.Promise

import JS.Marshall

export
data Promise : Type -> Type where [external]

export
ToFFI (Promise a) (Promise a) where toFFI = id

export
FromFFI (Promise a) (Promise a) where fromFFI = Just


text:
import STLC

namespace Example
    nat : Typ
    nat = Arrow (Arrow Base Base) (Arrow Base Base)

    zero : Term
    zero = Abs "s" (Arrow Base Base)
            (Abs "z" Base
                (Var "z"))

    suc : Term
    suc = Abs "n" nat
            (Abs "s" (Arrow Base Base)
                (Abs "z" Base
                    (App (Var "s")
                        (App (App (Var "n")
                                (Var "s"))
                            (Var "z")))))

    one : Term
    one = App suc zero

    plus : Term
    plus =
        Abs "m" nat
            (Abs "n" nat
                (Abs "s" (Arrow Base Base)
                    (Abs "z" Base
                        (App (App  (Var "m")
                                (Var "s"))
                            (App (App (Var "n")
                                    (Var "s"))
                                (Var "z"))))))
    example : Term
    example = App (App plus one) one


text:
module Control.Optics.Types

import public Control.Applicative.Const
import public Control.Monad.Identity
import public Data.Contravariant
import public Data.Functor.Tagged
import public Data.Morphisms
import public Data.Profunctor
import public Data.Profunctor.Choice

public export
Simple : (Type -> Type -> Type -> Type -> Type) -> Type -> Type -> Type
Simple p s a = p s s a a

public export
Optical : (p : Type -> Type -> Type)
       -> (q : Type -> Type -> Type)
       -> (f : Type -> Type)
       -> (s : Type)
       -> (t : Type)
       -> (a : Type)
       -> (b : Type)
       -> Type
Optical p q f s t a b = p a (f b) -> q s (f t)

public export
Optic : (Type -> Type -> Type) -> (Type -> Type) -> Type -> Type -> Type -> Type -> Type
Optic p = Optical p p

public export
LensLike : (Type -> Type) -> Type -> Type -> Type -> Type -> Type
LensLike = Optic Morphism

public export
Lens : Type -> Type -> Type -> Type -> Type
Lens s t a b = {f : Type -> Type} -> Functor f => LensLike f s t a b

public export
Setter : Type -> Type -> Type -> Type -> Type
Setter s t a b = LensLike Identity s t a b

public export
Getter : Type -> Type -> Type
Getter s a = {f : _} -> (Contravariant f, Functor f) => Simple (LensLike f) s a

public export
Getting : Type -> Type -> Type -> Type
Getting r s a = Simple (LensLike (Const r)) s a

public export
Prism : Type -> Type -> Type -> Type -> Type
Prism s t a b = {p, f : _} -> (Choice p, Applicative f) => Optic p f s t a b

public export
Review : Type -> Type -> Type -> Type -> Type
Review s t a b = {p : _} -> (Choice p) => Optic p Identity s t a b

public export
AReview : Type -> Type -> Type
AReview t b = Simple (Optic Tagged Identity) t b


text:
module Counts

import Data.Strings
import System.REPL

showCounts : String -> String
showCounts str = show (length (words str), length str) ++ "\n"

main : IO ()
main = repl "Enter a string: " showCounts

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:
data State : (stateType : Type) -> Type -> Type where
  Get : State stateType stateType
  Put : stateType -> State stateType ()

  Pure : ty -> State stateType ty
  Bind : State stateType a -> (a -> State stateType b) -> State stateType b

get : State stateType stateType
get = Get

put : stateType -> State stateType ()
put = Put

pure : ty -> State stateType ty
pure = Pure

(>>=) : State stateType a -> (a -> State stateType b) -> State stateType b
(>>=) = Bind

data Tree a = Empty
            | Node (Tree a) a (Tree a)

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty) "Fred"
                      (Node Empty "Sheilia" Empty)) "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

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

treeLabelWith : Tree a -> State (Stream labelType) (Tree (labelType, a))
treeLabelWith Empty = Pure Empty
treeLabelWith (Node left val right)
  = do left_labelled <- treeLabelWith left
       (this :: rest) <- get
       put rest
       right_labelled <- treeLabelWith right
       pure (Node left_labelled (this, val) right_labelled)

runState : State stateType a -> (st : stateType) -> (a, stateType)
runState Get st = (st, st)
runState (Put newState) st = ((), newState)
runState (Pure x) st = (x, st)
runState (Bind cmd prog) st = let (val, nextState) = runState cmd st in
                                  runState (prog val) nextState

treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = fst (runState (treeLabelWith tree) [1..])


text:
import Text.ParseTest

main : IO ()
main = do
  res <- test
  case res of
    Left e => do { putStrLn "Failed:" ; putStrLn e }
    Right () => putStrLn "Success"

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
-- like name map, but able to return ambiguous names
module Data.ANameMap

import Core.Name

import Data.List
import Data.NameMap
import Data.StringMap

%default total

export
record ANameMap a where
     constructor MkANameMap
     -- for looking up by exact (completely qualified) names
     exactNames : NameMap a
     -- for looking up by name root or partially qualified (so possibly
     -- ambiguous) names. This doesn't store machine generated names.
     hierarchy : StringMap (List (Name, a))

export
empty : ANameMap a
empty = MkANameMap empty empty

||| Given a Name, and an ANameMap, look up that name exactly
export
lookupExact : Name -> ANameMap a -> Maybe a
lookupExact n dict = lookup n (exactNames dict)

export
lookupName : Name -> ANameMap a -> List (Name, a)
lookupName n dict
    = case userNameRoot n of
           Nothing => case lookupExact n dict of
                           Nothing => []
                           Just res => [(n, res)]
           Just r => case lookup r (hierarchy dict) of
                          Nothing => []
                          Just ns => filter (matches n . fst) ns

addToHier : Name -> a ->
            StringMap (List (Name, a)) -> StringMap (List (Name, a))
addToHier n val hier
     -- Only add user defined names. Machine generated names can only be
		 -- found with the exactNames
     = case userNameRoot n of
            Nothing => hier
            Just root =>
                 case lookup root hier of
                      Nothing => insert root [(n, val)] hier
                      Just ns => insert root (update val ns) hier
  where
    update : a -> List (Name, a) -> List (Name, a)
    update val [] = [(n, val)]
    update val (old :: xs)
		    = if n == fst old
					   then (n, val) :: xs
						 else old :: update val xs

export
addName : Name -> a -> ANameMap a -> ANameMap a
addName n val (MkANameMap dict hier)
     = let dict' = insert n val dict
           hier' = addToHier n val hier in
           MkANameMap dict' hier'

export
toList : ANameMap a -> List (Name, a)
toList dict = toList (exactNames dict)

export
fromList : List (Name, a) -> ANameMap a
fromList = fromList' empty
  where
    fromList' : ANameMap a -> List (Name, a) -> ANameMap a
    fromList' acc [] = acc
    fromList' acc ((k, v) :: ns) = fromList' (addName k v acc) ns

-- Merge two contexts, with entries in the first overriding entries in
-- the second
export
merge : ANameMap a -> ANameMap a -> ANameMap a
merge (MkANameMap exact hier) ctxt
    = insertFrom (toList exact) ctxt
  where
    insertFrom : List (Name, a) -> ANameMap a -> ANameMap a
    insertFrom [] ctxt = ctxt
    insertFrom ((n, val) :: cs) ctxt
        = insertFrom cs (addName n val ctxt)


text:
twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible

equalSuccEqual : S k = S j -> k = j
equalSuccEqual Refl = Refl

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Dec (num1 = num2)
checkEqNat Z Z = Yes Refl
checkEqNat Z (S k) = No (\prf => (case prf of
                                       Refl impossible))

checkEqNat (S k) Z = No (\prf => (case prf of
                                       Refl impossible))

checkEqNat (S k) (S j) = case checkEqNat k j of
                              (Yes prf) => Yes $ cong prf
                              (No contra) => No (contra . equalSuccEqual)

||| Invariant functor
interface Invariant (i : Type -> Type) where
  xmap : (a -> b) -> (b -> a) ->  i a -> i b

Invariant Dec where
  xmap f g (Yes prf) = Yes (f prf)
  xmap f g (No contra) = No (contra . g)

castMap : (Cast a b, Cast b a, Invariant i) => i a -> i b
castMap x = xmap cast cast x

Cast (S k = S j) (k = j) where
  cast Refl = Refl

Cast (k = j) (S k = S j) where
  cast Refl = Refl

checkEqNat2 : (x : Nat) -> (y : Nat) -> Dec (x = y)
checkEqNat2 Z Z = Yes Refl
checkEqNat2 Z (S k) = No (\prf => case prf of
                                       Refl impossible)
checkEqNat2 (S k) Z = No (\prf => case prf of
                                       Refl impossible)
checkEqNat2 (S k) (S j) = castMap (checkEqNat2 k j)

data Vect : Nat -> a -> Type where
  Nil : Vect 0 a
  (::) : a -> Vect n a -> Vect (S n) a

headUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} -> (contra : (x = y) -> Void) -> x :: xs = y :: ys -> Void
headUnequal contra Refl = contra Refl

tailUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} -> (contra : (xs = ys) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
tailUnequal contra Refl = contra Refl

DecEq a => DecEq (Vect n a) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) = case decEq x y of
                                   (Yes Refl) => case decEq xs ys of
                                                    (Yes Refl) => Yes Refl
                                                    (No contra) => No (tailUnequal contra)
                                   (No contra) => No (headUnequal contra)


text:
module Tests

import Main

main : IO ()
main = putStrLn "tests passed"


text:
module Idris.Codegen.ExtSTG.ExternalTopIds

import Data.Strings
import Data.List
import Data.List1
import Data.List.Views
import Core.Context
import Libraries.Data.StringMap
import Idris.Codegen.ExtSTG.Core
import Idris.Codegen.ExtSTG.STG

{-
When referring a function from a different module, a binder must be created for the
name and it this binder must be registered in the ExternalTopIds of the module.

The STGApp needs a BinderId which will be the BinderId locally associated with
the binder in ExternalTopIds. The code generation for the binders in the ExternalTopIds
are special and the 'Unique's are not used.

During the compilation we need to collect the Binders and only use their Ids in the StgApp.

How do we store the Binders already? We associate Names with Uniques and we get the BinderIds
for free. But still we have to collect the externals for this name.
-}

%default total

||| Name for module dependency with fully qualified name.
public export
data ExtName = MkExtName String (List String) String

Show ExtName where
  show (MkExtName p m f) = "MkExtName " ++ show p ++ show m ++ show f

export
data ExternalBinder : Type where

export
ExtBindMap : Type
ExtBindMap = StringMap (ExtName, SBinderSg)

export
mkExternalBinders : Core (Ref ExternalBinder ExtBindMap)
mkExternalBinders = newRef ExternalBinder empty

renderName : ExtName -> String
renderName (MkExtName pkg mdl fn) = pkg ++ "_" ++ concat (intersperse "." mdl) ++ "." ++ fn

||| Parse names that are expected to have the following format:
||| package:namespace.entries.function
export
parseName : String -> Maybe ExtName
parseName str = case break (=='_') $ unpack str of
  ([], something)   => Nothing
  (something, [])   => Nothing
  (package, names)  => parseModuleName package $ toList $ splitOn '.' $ drop 1 names
  where
    parseModuleName : List Char -> List (List Char) -> Maybe ExtName
    parseModuleName pkg xs with (snocList xs)
      parseModuleName pkg []          | Empty      = Nothing
      parseModuleName pkg (ys ++ [y]) | Snoc _ _ _ = Just $ MkExtName (pack pkg) (map pack ys) (pack y)

||| Ask for a BinderId for the given name, if there is, if not create a one Binder and
||| register in the ExtBindMap
export
extName
  :  {auto _ : Ref ExternalBinder ExtBindMap}
  -> {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> ExtName
  -> Core BinderIdSg
extName e@(MkExtName pkg mdl fn) = do
  extBindMap <- get ExternalBinder
  let entryName = renderName e
  case lookup entryName extBindMap of
    Nothing => do
      binder <- map mkSBinderSg $ mkSBinderStr emptyFC fn -- TODO: Fix this HaskellExported etc
      put ExternalBinder $ insert entryName (e,binder) extBindMap
      pure $ getSBinderIdSg binder
    Just (_, b) => pure $ getSBinderIdSg b

export
registerHardcodedExtTopIds
  :  Ref ExternalBinder ExtBindMap
  => UniqueMapRef
  => Ref Counter Int
  => Core ()
registerHardcodedExtTopIds = do
  extBindMap <- get ExternalBinder
  binder <- map mkSBinderSg $ mkSBinderHardcoded hardcodedVoidHash emptyFC
  let (unt,mod,fn,_,_) = hardcodedVoidHash
  let e = MkExtName unt mod fn
  let entryName = renderName e
  put ExternalBinder $ insert entryName (e,binder) extBindMap

||| Generate External Top Ids for an STG module.
export
genExtTopIds
  : {auto _ : Ref ExternalBinder ExtBindMap}
  -> Core (List (UnitId, ModuleName, SBinderSg))
genExtTopIds = do
  map ( map
            (\(key, (MkExtName pck mdl fn, binder)) =>
              (MkUnitId pck, MkModuleName (concat (intersperse "." mdl)), binder))
        . StringMap.toList
        )
      $ get ExternalBinder

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Gamestate

import Effect.State
import Effect.SDL
import Effect.StdIO

import Aliens
import Rnd

record Gamestate : Type where
    MkGamestate : (position : (Int, Int)) ->
                  (xmovement : Int) ->
                  (ymovement : Int) ->
                  (bullets : List (Int, Int)) ->
                  (bombs : List (Int, Int)) ->
                  (aliens : List Alien) ->
                  Gamestate

initState : Gamestate
initState = MkGamestate (320,400) 0 0 [] [] startAliens

---------
-- Game state effect needs access to a random number generator

GS : (Type -> Type) -> Type -> Type
GS m t = { [Gamestate ::: STATE Gamestate, RND] } Eff m t

moveBullets : Gamestate -> Gamestate
moveBullets gs = let bullets' = movebs (bullets gs) in
                     record { bullets = bullets' } gs
    where movebs [] = []
          movebs ((x, y) :: bs)
                 = if y < 0 then movebs bs
                            else ((x, y-5) :: movebs bs)

moveBombs : Gamestate -> Gamestate
moveBombs gs = let bombs' = movebs (bombs gs) in
                   record { bombs = bombs' } gs
    where movebs [] = []
          movebs ((x, y) :: bs)
                 = if y > 480 then movebs bs
                              else ((x, y+5) :: movebs bs)

moveAliens : Gamestate -> Gamestate
moveAliens gs = record { aliens = move (bullets gs) (aliens gs) } gs

removeHit : Gamestate -> Gamestate
removeHit gs = let bs = bullets gs in
               let as = aliens gs in
               let (bs', as') = checkHit bs as in
               record { bullets = bs', aliens = as' } gs

drawBullets : List (Int, Int) -> { [SDL_ON] } Eff IO ()
drawBullets [] = return ()
drawBullets ((x, y) :: bs) = do rectangle red (x-1) (y-4) 2 8
                                drawBullets bs

drawBombs : List (Int, Int) -> { [SDL_ON] } Eff IO ()
drawBombs [] = return ()
drawBombs ((x, y) :: bs) = do rectangle yellow (x-1) (y-4) 2 8
                              drawBombs bs

randomDropBomb : GS m ()
randomDropBomb = randomDrop (map (Alien.position) (aliens !(Gamestate :- get)))
 where
   randomDrop : List (Int, Int) -> GS m ()
   randomDrop [] = return ()
   randomDrop ((x, y) :: as)
        = do if (!(rndInt 1 3000) == 100)
                 then (do s <- Gamestate :- get
                          let bs = bombs s
                          Gamestate :- put (record { bombs = (x, y+10) :: bs } s))
                 else randomDrop as

---------
updateGamestate : GS m ()
updateGamestate = do gs <- Gamestate :- get
                     let (x, y) = Gamestate.position gs
                     let (x', y') = (bounds 10 630 (x + xmovement gs),
                                     bounds 380 460 (y + ymovement gs))

                     let gs' = record { position = (x', y') } gs
                     let gs'' = moveAliens (moveBombs (moveBullets gs'))
                     Gamestate :- put (removeHit gs'')
                     randomDropBomb

    where bounds : Int -> Int -> Int -> Int
          bounds low high v = if v < low then low
                                 else if v > high then high
                                      else v

getPos : GS m (Int, Int)
getPos = do s <- Gamestate :- get
            return (position s)

xmove : Int -> GS m ()
xmove x = do s <- Gamestate :- get
             Gamestate :- put (record { xmovement = x } s)

ymove : Int -> GS m ()
ymove x = do s <- Gamestate :- get
             Gamestate :- put (record { ymovement = x } s)

addBullet : GS m ()
addBullet = do s <- Gamestate :- get
               let bs = bullets s
               (x, y) <- getPos
               Gamestate :- put (record { bullets = (x, y-10) :: bs } s)

-- Deal with keypresses from SDL
process : Maybe Event -> GS m Bool
process (Just AppQuit) = return False
process (Just (KeyDown KeyLeftArrow))  = do xmove (-2); return True
process (Just (KeyUp KeyLeftArrow))    = do xmove 0; return True
process (Just (KeyDown KeyRightArrow)) = do xmove 2; return True
process (Just (KeyUp KeyRightArrow))   = do xmove 0; return True
process (Just (KeyDown KeyUpArrow))    = do ymove (-2); return True
process (Just (KeyUp KeyUpArrow))      = do ymove 0; return True
process (Just (KeyDown KeyDownArrow))  = do ymove 2; return True
process (Just (KeyUp KeyDownArrow))    = do ymove 0; return True
process (Just (KeyDown KeySpace))      = do addBullet; return True
process _ = return True

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module Set

import RedBlack

export
data Set : Type -> Type where
  MkSet : {d : Nat} -> {c : RedBlack.Color} -> (a : Type) ->
          Tree d c a -> Set a

export
empty : Ord a => Set a
empty = MkSet _ RedBlack.empty

export
member : Ord a => a -> Set a -> Bool
member x (MkSet _ t) = RedBlack.member x t

export
add : Ord a => a -> Set a -> Set a
add x (MkSet _ t) = MkSet _ (snd (snd (RedBlack.insert x t)))

export
fromList : Ord a => List a -> Set a
fromList = foldr add empty

max_stars_repo_name: xuanruiqi/dtp

max_issues_repo_name: xuanruiqi/dtp

max_forks_repo_name: xuanruiqi/dtp


text:
module Data.Utils

import Data.Vect

export
enumerateVect : {n : Nat} -> Vect n a -> Vect n (Int, a)
enumerateVect l = enumerate' 0 l where
  enumerate' : {n : Nat} -> Int -> Vect n a -> Vect n (Int, a)
  enumerate' _ [] = []
  enumerate' i (x::xs) = (i, x)::(enumerate' (i+1) xs)

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Shape

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

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

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

export
circle : Double -> Shape
circle = Circle

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

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

area : Shape -> Double
area x with (shapeView x)
  area (triangle  base    height) | STriangle   = 0.5 * base * height
  area (rectangle width   height) | SRectangle  = width * height
  area (circle    radius)         | SCircle     = pi * radius * radius

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
> module Decidable.Predicates

> %default total
> %access public export

> Dec0 : Type -> Type
> Dec0 = Dec

> Dec1 : {A : Type} -> (P : A -> Type) -> Type
> Dec1 {A} P = (a : A) -> Dec0 (P a)

> DecEq0 : Type -> Type
> DecEq0 A = (a1 : A) -> (a2 : A) -> Dec (a1 = a2)

> DecEq1 : {A : Type} -> (P : A -> Type) -> Type
> DecEq1 {A} P = (a : A) -> DecEq0 (P a)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
||| Matrix operations with vector space dimensionalities enforced
||| at the type level. Uses operations from the Num type class.
module Data.Matrix.Numeric

import public Data.Matrix

%default total

infixr 2 <:>  -- vector inner product
infixr 2 ><   -- vector outer product
infixr 2 <<>> -- matrix commutator
infixr 2 >><< -- matrix anticommutator
infixl 3 <\>  -- row times a matrix
infixr 4 </>  -- matrix times a column
infixr 5 <>   -- matrix multiplication
infixl 5 <#>  -- matrix rescale
infixl 5 <#   -- vector rescale
infixr 7 \&\  -- vector tensor product
infixr 7 <&>  -- matrix tensor product

-----------------------------------------------------------------------
--                   Vectors as members of Num
-----------------------------------------------------------------------

instance Num a => Num (Vect n a) where
  (+) = zipWith (+)
  (*) = zipWith (*)
  fromInteger n = replicate _ (fromInteger n)

instance Neg a => Neg (Vect n a) where
  (-) = zipWith (-)
  abs = map abs
  negate = map negate

-----------------------------------------------------------------------
--                        Vector functions
-----------------------------------------------------------------------

||| Inner product of ring vectors
(<:>) : Num a => Vect n a -> Vect n a -> a
(<:>) w v = sum $ zipWith (*) w v

||| Scale a numeric vector by a scalar
(<#) : Num a => a -> Vect n a -> Vect n a
(<#) r = map (r *)

||| Tensor multiply (⊗) numeric vectors
(\&\) : Num a => Vect n a -> Vect m a -> Vect (n * m) a
(\&\) {n} {m} v w = zipWith (*) (oextend m v) (orep n w) where
  orep : (n : Nat) -> Vect m a -> Vect (n * m) a
  orep n v = concat $ replicate n v
  oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
  oextend n w = concat $ map (replicate n) w

||| Standard basis vector with one nonzero entry, numeric data type and vector-length unfixed
basis : Num a => (Fin d) -> Vect d a
basis i = replaceAt i 1 0

-----------------------------------------------------------------------
--                          Matrix functions
-----------------------------------------------------------------------

||| Matrix times a column vector
(</>) : Num a => Matrix n m a -> Vect m a -> Vect n a
(</>) m v = map (v <:>) m

||| Matrix times a row vector
(<\>) : Num a => Vect n a -> Matrix n m a -> Vect m a
(<\>) r m = map (r <:>) $ transpose m

||| Matrix multiplication
(<>) : Num a => Matrix n k a ->
                Matrix k m a ->
                Matrix n m a
(<>) m1 m2 = map (<\> m2) m1

||| Scale matrix by a scalar
(<#>) : Num a => a -> Matrix n m a -> Matrix n m a
(<#>) r = map (r <#)

||| Tensor multiply (⊗) for numeric matrices
(<&>) : Num a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
  stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
  stepOne {h2} m1 m2 = concat $ map (replicate h2) m1
  stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
  stepTwo {h1} m1 m2 = concat $ replicate h1 m2

||| Outer product between numeric vectors
(><) : Num a => Vect n a -> Vect m a -> Matrix n m a
(><) x y = col x <> row y

||| Matrix commutator
(<<>>) : Neg a => Matrix n n a -> Matrix n n a -> Matrix n n a
(<<>>) m1 m2 = (m1 <> m2) - (m2 <> m1)

||| Matrix anti-commutator
(>><<) : Num a => Matrix n n a -> Matrix n n a -> Matrix n n a
(>><<) m1 m2 = (m1 <> m2) + (m2 <> m1)

||| Identity matrix
Id : Num a => Matrix d d a
Id = map (\n => basis n) (fins _)

||| Square matrix from diagonal elements
diag_ : Num a => Vect n a -> Matrix n n a
diag_ = zipWith (\f => \x => replaceAt f x 0) (fins _)

||| Combine two matrices to make a new matrix in block diagonal form
blockDiag : Num a => Matrix n n a -> Matrix m m a -> Matrix (n+m) (n+m) a
blockDiag {n} {m} g h = map (++ replicate m 0) g ++ map ((replicate n 0) ++) h

-----------------------------------------------------------------------
--                           Determinants
-----------------------------------------------------------------------

||| Alternating sum
altSum : Neg a => Vect n a -> a
altSum (x::y::zs) = (x - y) + altSum zs
altSum [x]        = x
altSum []         = 0

||| Determinant of a 2-by-2 matrix
det2 : Neg a => Matrix 2 2 a -> a
det2 [[x1,x2],[y1,y2]] = x1*y2 - x2*y1

||| Determinant of a square matrix
det : Neg a => Matrix (S (S n)) (S (S n)) a -> a
det {n} m = case n of
  Z     => det2 m
  (S k) => altSum . map (\c => indices FZ c m * det (subMatrix FZ c m))
         $ fins (S (S (S k)))

max_stars_repo_name: BlackBrane/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module Web.Internal.WebidlTypes

import JS

%default total

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

export data DOMException : Type where [external]

export
ToFFI DOMException DOMException where toFFI = id

export
FromFFI DOMException DOMException where fromFFI = Just

export
SafeCast DOMException where
  safeCast = unsafeCastOnPrototypeName "DOMException"

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

export data Function : Type where [external]

export
ToFFI Function Function where toFFI = id

export
FromFFI Function Function where fromFFI = Just

export data VoidFunction : Type where [external]

export
ToFFI VoidFunction VoidFunction where toFFI = id

export
FromFFI VoidFunction VoidFunction where fromFFI = Just


text:
module Data.List.Predicates.Unique

import public Data.List.NotElem

%default total
%access public export

data Unique : (prfSame : a -> a -> Type)
            -> (ns : List a)
            -> Type
  where
    Empty : Unique p Nil
    Extend : (node : a)
          -> (prfNotElem : NotElem p node ns)
          -> (rest : Unique p ns)
          -> Unique p (node :: ns)

nodeIsFoundLater : (contra : NotElem prfSame x xs -> Void)
                -> Unique prfSame (x :: xs)
                -> Void
nodeIsFoundLater contra (Extend x prfNotElem rest) = contra prfNotElem

restNotUnique : (contra : Unique prfSame xs -> Void)
             -> (prfX : NotElem prfSame x xs)
             -> Unique prfSame (x :: xs)
             -> Void
restNotUnique contra prfX (Extend x prfNotElem rest) = contra rest

unique : (decEq : (x,y : a) -> Dec (prfSame x y))
     -> (xs    : List a)
     -> Dec (Unique prfSame xs)
unique decEq [] = Yes Empty
unique decEq (x :: xs) with (notElem decEq x xs)
  unique decEq (x :: xs) | (Yes prfX) with (unique decEq xs)
    unique decEq (x :: xs) | (Yes prfX) | (Yes prfXS) = Yes (Extend x prfX prfXS)
    unique decEq (x :: xs) | (Yes prfX) | (No contra) = No (restNotUnique contra prfX)

  unique decEq (x :: xs) | (No contra) = No (nodeIsFoundLater contra)

toList : {ns : List a} -> Unique prfSame ns -> List a
toList Empty = []
toList (Extend node prfNotElem rest) = node :: toList rest

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


text:
module ImplicitQueue

import Queue

%default total
%access private

data Digit a = Zero | One a | Two a a

export
data ImplicitQueue a =
    Shallow (Digit a)
  | Deep (Digit a) (Lazy (ImplicitQueue (a, a))) (Digit a)

export
Queue ImplicitQueue where
  empty = Shallow Zero
  isEmpty (Shallow Zero) = True
  isEmpty x              = False

  snoc (Shallow Zero) y = Shallow (One y)
  snoc (Shallow (One x)) y = Deep (Two x y) empty Zero
  snoc (Deep f m Zero) y = Deep f m (One y)
  snoc (Deep f m (One x)) y = Deep f (snoc m (x, y)) Zero
  snoc (Shallow (Two _ _)) _ = assert_unreachable
  snoc (Deep _ _ (Two _ _)) _ = assert_unreachable

  head (Shallow Zero   ) = idris_crash "empty queue"
  head (Shallow (One x)) = x
  head (Deep (One x)   m r) = x
  head (Deep (Two x y) m r) = x
  head (Shallow (Two _ _)) = assert_unreachable
  head (Deep Zero _ _) = assert_unreachable

  tail (Shallow Zero) = idris_crash "empty queue"
  tail (Shallow (One x)) = empty
  tail (Deep (Two x y) m r) = Deep (One y) m r
  tail (Deep (One x) m r) =
    if isEmpty m then Shallow r
    else let (y, z) = head m in Deep (Two y z) (tail m) r
  tail (Shallow (Two _ _)) = assert_unreachable
  tail (Deep Zero _ _) = assert_unreachable


text:
module Addition.Carry

import Common.Util
import Common.Interfaces
import Specifications.DiscreteOrderedGroup
import Proofs.GroupCancelationLemmas
import Proofs.Interval
import Addition.CarryLemmas

%default total
%access public export

data Carry = M | O | P

implementation Show Carry where
  show M = "M"
  show O = "O"
  show P = "P"

public export
value : Ringops s => Carry -> s
value P = One
value O = Zero
value M = Ng One

||| multiply by Carry
scale : s -> (s -> s) -> s -> Carry -> s
scale zero neg x M = neg x
scale zero neg x O = zero
scale zero neg x P = x

||| u = radix - 1
||| radix = u + 1
||| carry * radix + output = input
||| output in [-v..v] where v = u - 1
data Reduction :
  Binop s -> s -> (s -> s) -> Binrel s -> s -> s -> s -> {input : s} -> Type
  where MkReduction :
    .(input : s) -> (carry : Carry) -> (output : s) ->
    scale zero neg radix carry `add` output = input ->
    InSymRange leq neg (add u (neg unit)) output ->
    Reduction add zero neg leq unit u radix {input}

input : Reduction {s} _ _ _ _ _ _ _ {input = x} -> s
input _ = x

carry : Reduction _ _ _ _ _ _ _ -> Carry
carry (MkReduction _ c _ _ _) = c

output : Reduction {s} _ _ _ _ _ _ _ -> s
output (MkReduction _ _ o _ _) = o

result : Reduction {s} _ _ _ _ _ _ _ -> (Carry, s)
result (MkReduction _ c o _ _) = (c, o)

||| See README for a brief introduction.
||| 1 <= u - 1 means radix >= 3.
computeCarry : (Ringops s, Decidable [s,s] leq) =>
  DiscreteOrderedGroupSpec (+) Zero Ng leq One ->
  (u : s) -> leq One (u + Ng One) ->
  (x : s) -> InSymRange leq Ng (u + u) x ->
  Reduction (+) Zero Ng leq One u (One + u) {input = x}

computeCarry spec u bound x range =
  let pog = partiallyOrderedGroup spec
      grp = group (partiallyOrderedGroup spec)
      abel = abelian spec in
  case decidePartition3 spec (Ng u) u x range of
    Left prf
      => MkReduction x M (One + u + x)
           (groupCancel1bis grp _ x)
           (shiftLeftToSymRange pog u One x bound prf)
    Middle prf
      => MkReduction x O x
           (neutralL (monoid grp) _)
           (toSymRange pog abel prf)
    Right prf
      => MkReduction x P (x + Ng (One + u))
           (groupCancelAbelian grp abel _ x)
           (shiftRightToSymRange pog u One x bound prf)

max_stars_repo_name: jeroennoels/verified-exact-real

max_issues_repo_name: jeroennoels/verified-exact-real

max_forks_repo_name: jeroennoels/verified-exact-real


text:
module Main

import Data.Vect
import System.REPL
import Data.String

infixr 5 .+.

data Schema = SString
            | SInt
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

record DataStore where
  constructor MkData
  schema : Schema
  size : Nat
  items : Vect size (SchemaType schema)

items : (store : DataStore) -> Vect (size store) (SchemaType (schema store))
items (MkData _ _ items') = items'

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

-- data Command = Add String
--              | Get Integer
--              | Quit

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

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

-- getEntry : Integer -> DataStore -> Maybe (String, DataStore)
-- getEntry pos store = let storeItems = items store in
--                          case integerToFin pos (size store) of
--                               Nothing => Just ("Out of range\n", store)
--                               Just id => Just (index id storeItems ++ "\n", store)

-- processCommand : DataStore -> Command -> Maybe (String, DataStore)
-- processCommand store (Add item) = Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
-- processCommand store (Get pos) = getEntry pos store
-- processCommand store Quit = Nothing

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

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

max_stars_repo_name: brunoflores/type-driven-with-idris

max_issues_repo_name: brunoflores/type-driven-with-idris

max_forks_repo_name: brunoflores/type-driven-with-idris


text:
||| Provie `Day` level function.
module Data.Time.Calendar.Days

||| The Modified Julian Day is a standard count of days, with zero being the day 1858-11-17.
public export
data Day = MkModifiedJulianDay Integer

export
Eq Day where
  (MkModifiedJulianDay a) == (MkModifiedJulianDay b) = a == b

export
Ord Day where
  compare (MkModifiedJulianDay a) (MkModifiedJulianDay b) = compare a b

export
toInteger : Day -> Integer
toInteger (MkModifiedJulianDay x) = x

export
Enum Day where
  pred (MkModifiedJulianDay x) = MkModifiedJulianDay (pred x)
  toNat (MkModifiedJulianDay x) = toNat x
  fromNat x = MkModifiedJulianDay (fromNat x)

export
range: (Day, Day) -> List Day
range (MkModifiedJulianDay x, MkModifiedJulianDay y) = map (MkModifiedJulianDay) [x .. y]

export
index: (Day, Day) -> Nat -> Maybe Day
index (a, b) k =
  let (MkModifiedJulianDay a1) = a
      (MkModifiedJulianDay b1) = b
      range_a_b = range (a, b)
      inbounds = inBounds k range_a_b
  in
    case inbounds of
         Yes prf => Just (List.index k range_a_b)
         No  contra => Nothing

export
inRange: (Day, Day) -> Day -> Bool
inRange (a, b) k = elem k (range (a, b))

export
rangeSize: (Day, Day) -> Nat
rangeSize x = List.length (range x)

export
addDays: Integer -> Day -> Day
addDays x (MkModifiedJulianDay y) = MkModifiedJulianDay (x + y)

export
diffDays: Day -> Day -> Integer
diffDays (MkModifiedJulianDay x) (MkModifiedJulianDay y) = x - y

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
-- | Exercises on Equality.
module Koans.Equality

equalityEq : Bool
equalityEq = True == True

equalityNeq : Bool
equalityNeq = 5 /= 3

equalityGeq : Bool
equalityGeq = 5 >= 4

equalityGtr : Bool
equalityGtr = 5 > 4

equalityLeq : Bool
equalityLeq = 5 <= 5

equalityLess : Bool
equalityLess = 5 < 6

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

max_stars_repo_name: harrisi/on-being-better

max_issues_repo_name: harrisi/on-being-better

max_forks_repo_name: harrisi/on-being-better


text:
module Specifications.Order

import public Common.Abbrev

%default total
%access public export

||| specification
isReflexive : Binrel s -> Type
isReflexive rel = (x : _) -> rel x x

||| specification
isTransitive : Binrel s -> Type
isTransitive rel = (x,y,z : _) -> rel x y -> rel y z -> rel x z

||| specification
isAntisymmetric : Binrel s -> Type
isAntisymmetric rel = (x,y : _) -> rel x y -> rel y x -> x = y

||| composed specification
data PartialOrderSpec : Binrel s -> Type where
  MkPartialOrder : isReflexive rel -> isTransitive rel -> isAntisymmetric rel ->
    PartialOrderSpec rel

||| forget
reflexive : PartialOrderSpec rel -> isReflexive rel
reflexive (MkPartialOrder r _ _) = r

||| forget
transitive : PartialOrderSpec rel -> isTransitive rel
transitive (MkPartialOrder _ t _) = t

||| forget
antisymmetric : PartialOrderSpec rel -> isAntisymmetric rel
antisymmetric (MkPartialOrder _ _ a) = a

||| specification
isTotalOrder : Binrel s -> Type
isTotalOrder rel = (x,y : _) -> Either (rel x y) (rel y x)

||| composed specification
data TotalOrderSpec : Binrel s -> Type where
  MkTotalOrder : PartialOrderSpec rel -> isTotalOrder rel -> TotalOrderSpec rel

||| forget
partialOrder : TotalOrderSpec rel -> PartialOrderSpec rel
partialOrder (MkTotalOrder p _) = p

||| forget
totalOrder : TotalOrderSpec rel -> isTotalOrder rel
totalOrder (MkTotalOrder _ t) = t

||| A proof that `x` is between `a` and `b` relative to a certain
||| order relation.
data Between : Binrel s -> (s,s) -> s -> Type where
  MkBetween : rel a x -> rel x b -> Between rel (a,b) x

||| about the left side of the interval
betweenL : Between rel (a,b) x -> rel a x
betweenL (MkBetween l _) = l

||| about the right side of the interval
betweenR : Between rel (a,b) x -> rel x b
betweenR (MkBetween _ r) = r

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Dart.FFI.Constructors

import public System.FFI
import public Data.HVect
import public Data.List.Elem
import public Dart.FFI.Upcast

public export
data Parameter : (tag : Type) -> Type where
  MkParameter : (name : String) -> (ty : Type) -> (0 tag : Type) -> Parameter tag

%inline
public export
mkParameter : {tag : Type} -> String -> Type -> Parameter tag
mkParameter name ty = MkParameter name ty tag

%inline
public export
typeOf : Parameter tag -> Type
typeOf (MkParameter _ ty _) = ty

public export
data Argument : Parameter tag -> Type where
  Assign : {0 tag : Type} -> {ty : Type} -> (name : String) -> (value : ty) -> Argument (MkParameter name ty tag)

%inline
public export
Schema : (tag : Type) -> Type
Schema tag = List (Parameter tag)

public export
data Parameters : Schema tag -> Type where
  Nil : {0 schema : Schema tag} -> Parameters schema
  (::) : {0 p : Parameter tag} -> {0 schema : Schema tag}
      -> Argument p -> Parameters schema -> {auto 0 isValid : Elem p schema} -> Parameters schema

infix 1 @=
infix 1 @=>

%inline
public export
(@=) : {tag : Type} -> (p : Parameter tag) -> typeOf p -> Argument p
(@=) (MkParameter name _ _) value = Assign {tag = tag} name value

||| Upcast assignment.
%inline
public export
(@=>) : {tag : Type} -> (p : Parameter tag) -> ty -> {auto isAssignable : typeOf p `IsAssignableFrom` ty} -> Argument p
(@=>) (MkParameter name _ _) value = Assign {tag = tag} name (upcast value)

public export
%extern prim__dart_new : (ty : Type) -> HVect positional -> Parameters named -> (1 x : %World) -> IORes ty


text:
module Web.Raw.Webidl

import JS
import Web.Internal.WebidlPrim
import Web.Internal.Types

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

namespace DOMException

  public export
  ABORT_ERR : Bits16
  ABORT_ERR = 20

  public export
  DATA_CLONE_ERR : Bits16
  DATA_CLONE_ERR = 25

  public export
  DOMSTRING_SIZE_ERR : Bits16
  DOMSTRING_SIZE_ERR = 2

  public export
  HIERARCHY_REQUEST_ERR : Bits16
  HIERARCHY_REQUEST_ERR = 3

  public export
  INDEX_SIZE_ERR : Bits16
  INDEX_SIZE_ERR = 1

  public export
  INUSE_ATTRIBUTE_ERR : Bits16
  INUSE_ATTRIBUTE_ERR = 10

  public export
  INVALID_ACCESS_ERR : Bits16
  INVALID_ACCESS_ERR = 15

  public export
  INVALID_CHARACTER_ERR : Bits16
  INVALID_CHARACTER_ERR = 5

  public export
  INVALID_MODIFICATION_ERR : Bits16
  INVALID_MODIFICATION_ERR = 13

  public export
  INVALID_NODE_TYPE_ERR : Bits16
  INVALID_NODE_TYPE_ERR = 24

  public export
  INVALID_STATE_ERR : Bits16
  INVALID_STATE_ERR = 11

  public export
  NAMESPACE_ERR : Bits16
  NAMESPACE_ERR = 14

  public export
  NETWORK_ERR : Bits16
  NETWORK_ERR = 19

  public export
  NOT_FOUND_ERR : Bits16
  NOT_FOUND_ERR = 8

  public export
  NOT_SUPPORTED_ERR : Bits16
  NOT_SUPPORTED_ERR = 9

  public export
  NO_DATA_ALLOWED_ERR : Bits16
  NO_DATA_ALLOWED_ERR = 6

  public export
  NO_MODIFICATION_ALLOWED_ERR : Bits16
  NO_MODIFICATION_ALLOWED_ERR = 7

  public export
  QUOTA_EXCEEDED_ERR : Bits16
  QUOTA_EXCEEDED_ERR = 22

  public export
  SECURITY_ERR : Bits16
  SECURITY_ERR = 18

  public export
  SYNTAX_ERR : Bits16
  SYNTAX_ERR = 12

  public export
  TIMEOUT_ERR : Bits16
  TIMEOUT_ERR = 23

  public export
  TYPE_MISMATCH_ERR : Bits16
  TYPE_MISMATCH_ERR = 17

  public export
  URL_MISMATCH_ERR : Bits16
  URL_MISMATCH_ERR = 21

  public export
  VALIDATION_ERR : Bits16
  VALIDATION_ERR = 16

  public export
  WRONG_DOCUMENT_ERR : Bits16
  WRONG_DOCUMENT_ERR = 4

  export
  new :  (message : Optional String)
      -> (name : Optional String)
      -> JSIO DOMException
  new a b = primJS $ DOMException.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO DOMException
  new' = primJS $ DOMException.prim__new undef undef

  export
  code :  (0 _ : JSType t1)
       => {auto 0 _ : Elem DOMException (Types t1)}
       -> (obj : t1)
       -> JSIO Bits16
  code a = primJS $ DOMException.prim__code (up a)

  export
  message :  (0 _ : JSType t1)
          => {auto 0 _ : Elem DOMException (Types t1)}
          -> (obj : t1)
          -> JSIO String
  message a = primJS $ DOMException.prim__message (up a)

  export
  name :  (0 _ : JSType t1)
       => {auto 0 _ : Elem DOMException (Types t1)}
       -> (obj : t1)
       -> JSIO String
  name a = primJS $ DOMException.prim__name (up a)

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

namespace Function

  export
  toFunction : ( IO (Array AnyPtr) -> IO AnyPtr ) -> JSIO Function
  toFunction cb = primJS $ prim__toFunction cb

namespace VoidFunction

  export
  toVoidFunction : (() -> IO ()) -> JSIO VoidFunction
  toVoidFunction cb = primJS $ prim__toVoidFunction cb


text:
module Error.ANSI

namespace Deco
  public export
  reset : String
  reset = "\x1b[0m"

  public export
  dim : String
  dim = "\x1b[2m"

  public export
  bold : String
  bold = "\x1b[1m"

namespace Fg
  public export
  cyan : String
  cyan = "\x1b[34m"

  public export
  red : String
  red = "\x1b[31m"

namespace Bg
  public export
  red : String
  red = "\x1b[41m"

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
module Control.Monad.Free

%access public export
%default total

data Free : (f : Type -> Type) -> (a : Type) -> Type where
  Pure : a -> Free f a
  Bind : f (Free f a) -> Free f a

Functor f => Functor (Free f) where
  map f m = assert_total $ case m of
    Pure x => Pure (f x)
    Bind x => Bind (map (map f) x)

Functor f => Applicative (Free f) where
  pure = Pure

  m <*> x = assert_total $ case m of
    Pure f => map f x
    Bind f => Bind (map (<*> x) f)

Functor f => Monad (Free f) where
  m >>= f = assert_total $ case m of
    Pure x => f x
    Bind x => Bind (map (>>= f) x)

liftFree : Functor f => f a -> Free f a
liftFree = assert_total $ Bind . map Pure

lowerFree : Monad f => Free f a -> f a
lowerFree m = assert_total $ case m of
  Pure x => pure x
  Bind f => join (map lowerFree f)

iterM : (Monad m, Functor f) => (f (m a) -> m a) -> Free f a -> m a
iterM f m = assert_total $ case m of
  Pure x => pure x
  Bind x => f (map (iterM f) x)

hoistFree : Functor g => ({ a : Type } -> f a -> g a) -> Free f b -> Free g b
hoistFree f m = assert_total $ case m of
  Pure x => Pure x
  Bind x => Bind (hoistFree f <$> f x)

foldFree : (Monad m, Functor f) => ({ a : Type } -> f a -> m a) -> Free f b -> m b
foldFree f m = assert_total $ case m of
  Pure x => pure x
  Bind x => f x >>= foldFree f

interface MonadFree (m : Type -> Type) (f : Type -> Type) | m where
  wrap : f (m a) -> m a

MonadFree (Free f) f where
  wrap = assert_total Bind

max_stars_repo_name: ajhamwood/idris-free

max_issues_repo_name: idris-industry/idris-free

max_forks_repo_name: idris-industry/idris-free


text:
module Main

import Parity
import System

data Bit : Nat -> Type where
     b0 : Bit 0
     b1 : Bit 1

instance Show (Bit n) where
     show b0 = "0"
     show b1 = "1"

infixl 5 #

data Binary : (width : Nat) -> (value : Nat) -> Type where
     zero : Binary Z Z
     (#)  : %erase v
            Binary w v -> (p : Bit bit) -> Binary (S w) (bit + 2 * v)

instance Show (Binary w k) where
     show zero = ""
     show (bin # bit) = show bin ++ show bit

pad : Binary w n -> Binary (S w) n
pad zero = zero # b0
pad (num # x) = pad num # x

natToBin : (width : Nat) -> (n : Nat) ->
           Maybe (Binary width n)
natToBin Z (S k) = Nothing
natToBin Z Z = Just zero
natToBin (S w) Z = do x <- natToBin w Z
                      Just (pad x)
natToBin (S w) (S k) with (parity k)
  natToBin (S w) (S (plus j j)) | even = do jbin <- natToBin w j
                                            let value = jbin # b1
                                            ?ntbEven
  natToBin (S w) (S (S (plus j j))) | odd = do jbin <- natToBin w (S j)
                                               let value = jbin # b0
                                               ?ntbOdd

pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
term    syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))

addBit : Bit x -> Bit y -> Bit c ->
          (bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))
addBit b0 b0 b0 = bitpair b0 b0
addBit b0 b0 b1 = bitpair b0 b1
addBit b0 b1 b0 = bitpair b0 b1
addBit b0 b1 b1 = bitpair b1 b0
addBit b1 b0 b0 = bitpair b0 b1
addBit b1 b0 b1 = bitpair b1 b0
addBit b1 b1 b0 = bitpair b1 b0
addBit b1 b1 b1 = bitpair b1 b1

adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)
adc zero        zero        carry ?= zero # carry
adc (numx # bx) (numy # by) carry
   ?= let (bitpair carry0 lsb) = addBit bx by carry in
          adc numx numy carry0 # lsb

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

readNum : IO Nat
readNum = do putStr "Enter a number:"
             return (fromInteger (cast !getLine))

mainLoop : Int -> IO ()
mainLoop i
     = do putStrLn $ "Calc " ++ show i
          let Just bin1 = natToBin 8 !readNum
          print bin1
          let Just bin2 = natToBin 8 !readNum
          print bin2
          print (adc bin1 bin2 b0)
          mainLoop (i + 1)

main : IO ()
main = mainLoop 1

---------- Proofs ----------

Main.ntbOdd = proof {
    intro w,j;
    rewrite sym (plusZeroRightNeutral j);
    rewrite plusSuccRightSucc j j;
    intros;
    refine Just;
    trivial;
}

Main.ntbEven = proof {
    compute;
    intro w,j;
    rewrite sym (plusZeroRightNeutral j);
    intros;
    refine Just;
    trivial;
}

-- There is almost certainly an easier proof. I don't care, for now :)

Main.adc_lemma_2 = proof {
    intro c,w,v,bit0,num0;
    intro b0,v1,bit1,num1,b1;
    intro bc,x,x1,bx,bx1;
    rewrite sym (plusZeroRightNeutral x);
    rewrite sym (plusZeroRightNeutral v1);
    rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));
    rewrite sym (plusZeroRightNeutral v);
    intros;
    rewrite sym (plusAssociative (plus c (plus bit0 (plus v v))) bit1 (plus v1 v1));
    rewrite  (plusAssociative c (plus bit0 (plus v v)) bit1);
    rewrite  (plusAssociative bit0 (plus v v) bit1);
    rewrite plusCommutative bit1 (plus v v);
    rewrite sym (plusAssociative c bit0 (plus bit1 (plus v v)));
    rewrite sym (plusAssociative (plus c bit0) bit1 (plus v v));
    rewrite sym b;
    rewrite plusAssociative x1 (plus x x) (plus v v);
    rewrite plusAssociative x x (plus v v);
    rewrite sym (plusAssociative x v v);
    rewrite plusCommutative v (plus x v);
    rewrite sym (plusAssociative x v (plus x v));
    rewrite (plusAssociative x1 (plus (plus x v) (plus x v)) (plus v1 v1));
    rewrite sym (plusAssociative (plus (plus x v) (plus x v)) v1 v1);
    rewrite  (plusAssociative (plus x v) (plus x v) v1);
    rewrite (plusCommutative v1 (plus x v));
    rewrite sym (plusAssociative (plus x v) v1 (plus x v));
    rewrite (plusAssociative (plus (plus x v) v1) (plus x v) v1);
    trivial;
}

Main.adc_lemma_1 = proof {
    intros;
    rewrite sym (plusZeroRightNeutral c) ;
    trivial;
}