text:
module LuaCommon

import Core.Core
import Core.Context.Context
import Core.Name
import Data.Buffer
import Data.Buffer
import Data.List
import Data.List
import Data.List1
import Data.String.Extra
import Data.String
import Data.Vect
import Data.Zippable

import Libraries.Utils.Hex

infixl 100 |>

||| Flipped tightly bound function application
public export %inline
(|>) : a -> (a -> b) -> b
x |> f = f x

namespace Strings
  FromString (List Char) where
    fromString = fastUnpack

  public export
  record String1 where
    constructor MkString1
    head : Char
    tail : String

  public export
  data NonEmptyString : String -> Type where
    ItIsNonEmptyString : (0 prf : IsJust (strUncons str)) -> NonEmptyString str

  public export
  toString1 : (str : String) -> {auto 0 prf : NonEmptyString str} -> String1
  toString1 str @{ItIsNonEmptyString itIs} with (strUncons str)
   toString1 str @{ItIsNonEmptyString ItIsJust} | Just (x, xs) = MkString1 x xs

  public export
  toList1 : (str : String) -> {auto 0 prf : NonEmptyString str} -> List1 Char
  toList1 str @{ItIsNonEmptyString itIs} with (strUncons str)
   toList1 str @{ItIsNonEmptyString ItIsJust} | Just (x, xs) = x ::: fastUnpack xs

  public export
  ||| Removes all occurances of the literal @lit
  ||| in the string @str
  removeAll :
        (lit : String)
     -> (str : String)
     -> String
  removeAll lit str with (str == "")
     removeAll lit str | False =
        if isPrefixOf lit str
           then removeAll lit (substr (length lit) (length str `minus` length lit) str)
           else case strUncons str of
                     Just (head, rest) => strCons head (removeAll lit rest)
                     Nothing => ""
     removeAll lit str | True = ""

  -- TODO Useful function to add to `base` ?
  ||| Splits the subject string into parts by the delimiter.
  public export
  split : (delim : List1 Char) -> (subject : List Char) -> List1 (List Char)
  split delim subject =
    reverse $ splitHelper delim subject [] []
    where
      splitHelper : List1 Char -> List Char -> List Char -> List (List Char) -> List1 (List Char)
      splitHelper delim [] acc store = (reverse acc) ::: store
      splitHelper delim str@(x :: xs) acc store =
        case isPrefixOf (forget delim) str of
          -- Dropping a non-zero sequence of characters from `str` ensures that `str` is structurally smaller with each successive call
          True => splitHelper delim (assert_smaller str $ drop (length $ forget delim) str) [] (reverse acc :: store)
          False => splitHelper delim xs (x :: acc) store

  public export %inline
  indent : Nat -> String
  indent n = replicate (2 * n) ' '

  public export
  trimLeft : List Char -> List Char
  trimLeft (' ' :: xs) = trimLeft xs
  trimLeft xs = xs

  public export %inline
  trim : List Char -> List Char
  trim = reverse . trimLeft . reverse . trimLeft

public export
data LuaVersion = Lua51 | Lua52 | Lua53 | Lua54

namespace LuaVersion

  export
  index : LuaVersion -> Int
  index Lua51 = 51
  index Lua52 = 52
  index Lua53 = 53
  index Lua54 = 54

  export
  fromIndex : Int -> Maybe LuaVersion
  fromIndex 51 = Just Lua51
  fromIndex 52 = Just Lua52
  fromIndex 53 = Just Lua53
  fromIndex 54 = Just Lua54
  fromIndex _  = Nothing

  export
  Eq LuaVersion where
     Lua51 == Lua51 = True
     Lua52 == Lua52 = True
     Lua53 == Lua53 = True
     Lua54 == Lua54 = True
     _     ==     _ = False

  export
  Show LuaVersion where
     show ver =
      let index = index ver
          major = index `div` 10
          minor = index `mod` 10
      in
          "Lua" ++ show major ++ "." ++ show minor

  export
  Ord LuaVersion where
     compare v v' = compare (index v) (index v')

  export
  parseLuaVersion : String -> Maybe LuaVersion
  parseLuaVersion str = helper ((trim . toLower) str)
  where
    helper : String -> Maybe LuaVersion
    helper x =
       let noprefix =
              if isPrefixOf "lua" x
                then drop 3 x
                else x
           nodots = removeAll "." noprefix
           nodashes = removeAll "-" nodots
           firstTwo = take 2 nodashes
       in
           do int <- parseInteger {a = Int} firstTwo
              fromIndex int

namespace Data.List
  public export
  contains : Eq a => List a -> a -> Bool
  contains [] _ = False
  contains (x :: xs) x' = x == x' || contains xs x

  public export
  group : {n : _} -> List a -> Vect n (a -> Bool) -> Vect n (List a)
  group [] _ = replicate _ []
  group (x :: xs) fs
   = zipWith List.(++) (map (\f => fromMaybe [] (toMaybe (f x) [x])) fs) (group xs fs)

namespace Data.Maybe
  public export %inline
  orElse : (maybe : Maybe a) -> (def : Lazy a) -> a
  orElse = flip fromMaybe

public export
luaKeywords : List String
luaKeywords = ["and", "break", "do", "else", "elseif", "end",
               "false", "for", "function", "goto", "if", "in",
               "local", "nil", "not", "or", "repeat", "return",
               "then", "true", "until", "while"]

--lua's set of chars that form a valid identifier is restricted to alphanumeric characters and underscore
--in order to resemble at least some level of readability of generated names below 'pseudotranslation' is utilized
--this is not failproof, i.e. you can find 2 different identifiers such that after running both of them though this function
--you will get same output. But that is highly unlikely and would be a result of using bad naming conventions
public export
validateIdentifier : String -> String
validateIdentifier str = fastConcat $ validate <$> unpack (validateKeyword str)
  where
    validate : Char -> String
    validate ':' = "_col_"
    validate ';' = "_semicol_"
    validate ',' = "_comma_"
    validate '+' = "_plus_"
    validate '-' = "_minus_"
    validate '*' = "_mult_"
    validate '\\' = "_bslash_"
    validate '/' = "_fslash_"
    validate '=' = "_eq_"
    validate '.' = "_dot_"
    validate '?' = "_what_"
    validate '|' = "_pipe_"
    validate '&' = "_and_"
    validate '>' = "_gt_"
    validate '<' = "_lt_"
    validate '!' = "_exclam_"
    validate '@' = "_at_"
    validate '$' = "_dollar_"
    validate '%' = "_percent_"
    validate '^' = "_arrow_"
    validate '~' = "_tilde_"
    validate '#' = "_hash_"
    validate ' ' = "_space_"
    validate '(' = "_lpar_"
    validate ')' = "_rpar_"
    validate '[' = "_lbrack_"
    validate ']' = "_rbrack_"
    validate '{' = "_lbrace_"
    validate '}' = "_rbrace_"
    validate '\'' = "_prime_"
    validate '"' = "_quote_"
    validate s with (ord s > 160) --unicode codepoints are above 160
      validate s | False = cast s
      validate s | True = "_uni_" ++ cast (ord s) ++ "_"

    validateKeyword : String -> String
    validateKeyword mbkw =
      case find (== mbkw) luaKeywords of
        Just kw => "_kw_" ++ kw ++ "_"
        Nothing => mbkw

public export
parseEnvBool : String -> Maybe Bool
parseEnvBool str =
  case toLower str of
    "true" => Just True
    "1" => Just True
    "on" => Just True
    "false" => Just False
    "0" => Just False
    "off" => Just False
    _ => Nothing

||| Escape some of the ascii codes, fail on unicode, as
||| not all supported lua versions have unicode escape sequences
public export
escapeStringLua : String -> Maybe String
escapeStringLua s = concat <$> traverse okchar (fastUnpack s)
  where
    okchar : Char -> Maybe String
    okchar c = if (c >= ' ') && (c /= '\\') && (c /= '"') && (c <= '~')
                  then Just (cast c)
                  else case c of
                            '\0' => Just "\\0"
                            '"' => Just "\\\""
                            '\\' => Just "\\\\"
                            '\r' => Just "\\r"
                            '\n' => Just "\\n"
                            _ => Nothing

||| Transforms `x, y, ... w => body` into `function(x) return function(y) ... return function(w) return body end ... end end
public export
curryTransform : (vars : List (List Char)) -> (body : List Char) -> List Char
curryTransform [] body = body
curryTransform (x :: xs) body = "function(" ++ x ++ ") return " ++ curryTransform xs body ++ " end"

export %inline
sequenceMaybe : Maybe (Core a) -> Core (Maybe a)
sequenceMaybe Nothing = pure Nothing
sequenceMaybe (Just x) = x >>= pure . Just

public export
record StrBuffer where
  constructor MkStrBuffer
  get : Buffer
  offset : Int

namespace StrBuffer

  export
  allocStrBuffer : Int -> Core StrBuffer
  allocStrBuffer initialSize =
    do
       (Just buf) <- coreLift $ newBuffer initialSize
          | _ => throw (UserError "Could not allocate buffer")
       pure (MkStrBuffer buf 0)

  export
  writeStr :
        (marker : Type)
     -> {auto buf : Ref marker StrBuffer}
     -> String
     -> Core ()
  writeStr marker str =
    do
       let strlen = stringByteLength str
       strbuf <- get marker
       raw <- ensureSize strbuf.get strbuf.offset strlen
       coreLift $ setString raw strbuf.offset str
       put marker (MkStrBuffer raw (strbuf.offset + strlen))
       pure ()

     where
       ensureSize : Buffer -> Int -> Int -> Core Buffer
       ensureSize buf offset strlen =
          let bufLen = !(coreLift $ rawSize buf) in
              if offset + strlen > bufLen
                 then do
                    (Just buf) <- coreLift $ resizeBuffer buf (max (2 * bufLen) (offset + strlen))
                      | _ => throw (UserError "Could not allocate buffer")
                    pure buf
              else
                 pure buf

public export
data DeferredStr : Type where
  Nil : DeferredStr
  (::) : Lazy a
      -> {auto prf : Either (a = String) (a = DeferredStr)}
      -> Lazy DeferredStr
      -> DeferredStr

namespace DeferredStr

  export
  pure : String -> DeferredStr
  pure x = [delay x]

  export
  traverse_ : (String -> Core b) -> DeferredStr -> Core ()
  traverse_ f ((::) x xs {prf = Left Refl}) = do ignore (f x); traverse_ f xs
  traverse_ f ((::) x xs {prf = Right Refl}) = do traverse_ f x; traverse_ f xs
  traverse_ _ [] = pure ()

  export
  sepBy : Lazy (List (DeferredStr)) -> String -> DeferredStr
  sepBy (x :: xs@(_ :: _)) sep = x :: sep :: sepBy xs sep
  sepBy (x :: []) _ = [x]
  sepBy [] _ = []

  export
  (++) : Lazy DeferredStr -> Lazy DeferredStr -> DeferredStr
  [] ++ rhs = rhs
  (x :: xs) ++ rhs = x :: xs ++ rhs

--it is actually more general than that, but whatever
export
trimQuotes : String -> String
trimQuotes x = substr 1 (length x `minus` 2) x

public export %inline
forAll : (a -> Bool) -> List a -> Bool
forAll f xs = foldl (\ac, x => ac && f x) True xs


text:
||| Game server for Bautzen 1945
module Bautzen.Server

import Bautzen.Options

import Bautzen.Game
import Bautzen.Network
import Bautzen.REPL

import Data.Strings.Extra

import Builtin
import Prelude
import Data.Nat
import Data.List
import Network.Socket
import Network.Socket.Data
import Network.Socket.Raw
import System

handleClient : Socket -> SocketAddress -> Game -> IO ()
handleClient socket addr game = do
  putStrLn $ "waiting for input"
  Right (str, _) <- recv socket 6 -- receive 6 characters representing the length of message to read
    | Left err => do
        putStrLn ("failed to receive length of message " ++ show err)
        close socket -- TODO: Error handling.
  putStrLn ("received  " ++ str)
  case parseInteger (unpack str) 0 of
    Nothing => do
      putStrLn ("fail to parse '" ++ str ++ "' to expected number of characters, ignoring")
      close socket -- TODO: Error handling.
    Just len => do Right (msg, _) <- recv socket (fromInteger len)
                     | Left err => do
                         putStrLn ("failed to read message " ++ show err)
                         --handleClient socket addr game
                         close socket -- TODO: Error handling.
                   putStrLn $ "received  " ++ msg
                   let (res, game') = commandHandler game msg
                   putStrLn $ "result is " ++ show res
                   let lens = padWith0 (cast $ length res)
                   putStrLn $ "sending " ++ lens ++ " chars"
                   Right l <- send socket (lens ++ res)
                     | Left err => do
                         putStrLn ("failed to send message " ++ show err)
                         close socket -- TODO: Error handling.
                   putStrLn $ "sent result"
                   handleClient socket addr game'

serve : Socket -> IO (Either String ())
serve sock = do
  putStrLn "awaiting clients"
  Right (s, addr) <- accept sock
    | Left err => pure (Left $ "Failed to accept on socket with error: " ++ show err)
  putStrLn $ "client connecting " ++ show addr
  putStrLn $ "before fork s = " ++ show (protocolNumber s, descriptor s)
  pid <- fork (handleClient s addr initialGame)
  putStrLn "after fork"
  serve sock

export
server : Options -> IO (Either String ())
server (MkOptions port host _) = do
  Right sock <- socket AF_INET Stream 0
        | Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
  res <- bind sock (Just (Hostname host)) port
  if res /= 0
    then pure (Left $ "Failed to bind socket with error: " ++ show res)
    else do
      res <- listen sock
      if res /= 0
        then pure (Left $ "Failed to listen on socket with error: " ++ show res)
        else serve sock

ext: idr

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text: module PQ.Schema.Type


text:
module LightClick.Types

import public Data.Vect

import public Toolkit.Data.DVect
import public Toolkit.Data.Rig

import public LightClick.Types.Meta
import public LightClick.Types.Direction
import public LightClick.Types.Sensitivity
import public LightClick.Types.WireType

%default total

public export
data Ty : MTy -> Type where
  TyLogic : Ty DATA
  TyArray : (type : Ty DATA) -> (length : Nat) -> Ty DATA
  TyStruct : {n : Nat} -> (kvs : Vect (S n) (Pair String (Ty DATA))) -> Ty DATA
  TyUnion  : {n : Nat} -> (kvs : Vect (S n) (Pair String (Ty DATA))) -> Ty DATA

  TyUnit : Ty UNIT
  TyConn : Ty CONN
  TyGate : Ty GATE

  TyPort : (label : String)
        -> (dir : Direction)
        -> (sense: Sensitivity)
        -> (wty : Wire)
        -> (type : Ty DATA)
        -> (usage : TyRig)
        -> Ty (PORT label)

  TyModule : {n : Nat}
          -> {names : Vect (S n) String}
          -> DVect String (Ty . PORT) (S n) names
          -> Ty (MODULE names)

-- [ Accessors and ]
public export
mkDual : Ty (PORT label) -> Ty (PORT label)
mkDual (TyPort l d s w t u) with (d)
  mkDual (TyPort l d s w t u) | IN = TyPort l OUT s w t u
  mkDual (TyPort l d s w t u) | OUT = TyPort l IN s w t u
  mkDual (TyPort l d s w t u) | INOUT = TyPort l INOUT s w t u

namespace Control
  public export
  mkDual : Ty (PORT label) -> Ty (PORT label)
  mkDual (TyPort l d s w t u) with (d)
    mkDual (TyPort l d s w t u) | IN = TyPort l OUT s Control t u
    mkDual (TyPort l d s w t u) | OUT = TyPort l IN s Control t u
    mkDual (TyPort l d s w t u) | INOUT = TyPort l INOUT s Control t u

getPortLabel : {label : String} -> Ty (PORT label) -> String
getPortLabel {label} p = label

export
getUsage : Ty (PORT s) -> TyRig
getUsage (TyPort label dir sense wty type usage) = usage

export
setUsage : Ty (PORT s) -> TyRig -> Ty (PORT s)
setUsage (TyPort label dir sense wty type _) = TyPort label dir sense wty type

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Minecraft.Core.Item.Export

import public Minecraft.Core.Item

%default total

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text: (a, b) = (1, 2)


text:
module IdrisScript.JSON

import IdrisScript

%access public export

||| Converts an object into a JSON string
stringfy : JSValue (JSObject c) -> JS_IO String
stringfy obj = jscall "JSON.stringfy(%0)" (Ptr -> JS_IO String) (unpack obj)

||| Parses a JSON string
parse : String -> JS_IO (Maybe (c ** JSValue (JSObject c)))
parse str = do
  res <- jscall "JSON.parse(%0)" (String -> JS_IO Ptr) str
  case !(pack res) of
       (JSObject "Object" ** obj) => pure $ Just ("Object" ** obj)
       (JSObject "Array"  ** obj) => pure $ Just ("Array" ** obj)
       _                          => pure Nothing

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module Core.Reflect

import Data.List1

import Core.Context
import Core.Env
import Core.Normalise
import Core.TT
import Core.Value

%default covering

public export
interface Reify a where
  reify : {auto c : Ref Ctxt Defs} ->
          {vars : _} ->
          Defs -> NF vars -> Core a

public export
interface Reflect a where
  reflect : {vars : _} ->
            FC -> Defs -> (onLHS : Bool) ->
            Env Term vars -> a -> Core (Term vars)

export
getCon : {vars : _} ->
         FC -> Defs -> Name -> Core (Term vars)
getCon fc defs n
    = case !(lookupDefExact n (gamma defs)) of
           Just (DCon t a _) => resolved (gamma defs) (Ref fc (DataCon t a) n)
           Just (TCon t a _ _ _ _ _ _) => resolved (gamma defs) (Ref fc (TyCon t a) n)
           Just _ => resolved (gamma defs) (Ref fc Func n)
           _ => throw (UndefinedName fc n)

export
appCon : {vars : _} ->
         FC -> Defs -> Name -> List (Term vars) -> Core (Term vars)
appCon fc defs n args
    = do fn <- getCon fc defs n
         resolved (gamma defs) (apply fc fn args)

export
preludetypes : String -> Name
preludetypes n = NS typesNS (UN $ Basic n)

export
basics : String -> Name
basics n = NS basicsNS (UN $ Basic n)

export
builtin : String -> Name
builtin n = NS builtinNS (UN $ Basic n)

export
primio : String -> Name
primio n = NS primIONS (UN $ Basic n)

export
reflection : String -> Name
reflection n = NS reflectionNS (UN $ Basic n)

export
reflectiontt : String -> Name
reflectiontt n = NS reflectionTTNS (UN $ Basic n)

export
reflectionttimp : String -> Name
reflectionttimp n = NS reflectionTTImpNS (UN $ Basic n)

export
cantReify : NF vars -> String -> Core a
cantReify val ty
    = throw (GenericMsg (getLoc val) ("Can't reify as " ++ ty))

export
cantReflect : FC -> String -> Core a
cantReflect fc ty
    = throw (GenericMsg fc ("Can't reflect as " ++ ty))

export
Reify () where
  reify defs _ = pure ()

export
Reflect () where
  reflect fc defs lhs env _ = getCon fc defs (builtin "MkUnit")

export
Reify String where
  reify defs (NPrimVal _ (Str str)) = pure str
  reify defs val = cantReify val "String"

export
Reflect String where
  reflect fc defs lhs env x = pure (PrimVal fc (Str x))

export
Reify Int where
  reify defs (NPrimVal _ (I v)) = pure v
  reify defs val = cantReify val "Int"

export
Reflect Int where
  reflect fc defs lhs env x = pure (PrimVal fc (I x))

export
Reify Integer where
  reify defs (NPrimVal _ (BI v)) = pure v
  reify defs val = cantReify val "Integer"

export
Reflect Integer where
  reflect fc defs lhs env x = pure (PrimVal fc (BI x))

export
Reify Char where
  reify defs (NPrimVal _ (Ch v)) = pure v
  reify defs val = cantReify val "Char"

export
Reflect Char where
  reflect fc defs lhs env x = pure (PrimVal fc (Ch x))

export
Reify Double where
  reify defs (NPrimVal _ (Db v)) = pure v
  reify defs val = cantReify val "Double"

export
Reflect Double where
  reflect fc defs lhs env x = pure (PrimVal fc (Db x))

export
Reify Bool where
  reify defs val@(NDCon _ n _ _ _)
      = case dropAllNS !(full (gamma defs) n) of
            UN (Basic "True") => pure True
            UN (Basic "False") => pure False
            _ => cantReify val "Bool"
  reify defs val = cantReify val "Bool"

export
Reflect Bool where
  reflect fc defs lhs env True = getCon fc defs (basics "True")
  reflect fc defs lhs env False = getCon fc defs (basics "False")

export
Reify Nat where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "Z"), _) => pure Z
             (UN (Basic "S"), [(_, k)])
                 => do k' <- reify defs !(evalClosure defs k)
                       pure (S k')
             _ => cantReify val "Nat"
  reify defs val = cantReify val "Nat"

export
Reflect Nat where
  reflect fc defs lhs env Z = getCon fc defs (preludetypes "Z")
  reflect fc defs lhs env (S k)
      = do k' <- reflect fc defs lhs env k
           appCon fc defs (preludetypes "S") [k']

export
Reify a => Reify (List a) where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "Nil"), _) => pure []
             (UN (Basic "::"), [_, (_, x), (_, xs)])
                  => do x' <- reify defs !(evalClosure defs x)
                        xs' <- reify defs !(evalClosure defs xs)
                        pure (x' :: xs')
             _ => cantReify val "List"
  reify defs val = cantReify val "List"

export
Reflect a => Reflect (List a) where
  reflect fc defs lhs env [] = appCon fc defs (basics "Nil") [Erased fc False]
  reflect fc defs lhs env (x :: xs)
      = do x' <- reflect fc defs lhs env x
           xs' <- reflect fc defs lhs env xs
           appCon fc defs (basics "::") [Erased fc False, x', xs']

export
Reify a => Reify (List1 a) where
  reify defs val@(NDCon _ n _ _ [_, (_, x), (_, xs)])
      = case dropAllNS !(full (gamma defs) n) of
             UN (Basic ":::")
                  => do x' <- reify defs !(evalClosure defs x)
                        xs' <- reify defs !(evalClosure defs xs)
                        pure (x' ::: xs')
             _ => cantReify val "List1"
  reify defs val = cantReify val "List1"

export
Reflect a => Reflect (List1 a) where
  reflect fc defs lhs env xxs
      = do x' <- reflect fc defs lhs env (head xxs)
           xs' <- reflect fc defs lhs env (tail xxs)
           appCon fc defs (NS (mkNamespace "Data.List1")
                  (UN $ Basic ":::")) [Erased fc False, x', xs']

export
Reify a => Reify (Maybe a) where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "Nothing"), _) => pure Nothing
             (UN (Basic "Just"), [_, (_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (Just x')
             _ => cantReify val "Maybe"
  reify defs val = cantReify val "Maybe"

export
Reflect a => Reflect (Maybe a) where
  reflect fc defs lhs env Nothing = appCon fc defs (preludetypes "Nothing") [Erased fc False]
  reflect fc defs lhs env (Just x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (preludetypes "Just") [Erased fc False, x']

export
(Reify a, Reify b) => Reify (a, b) where
  reify defs val@(NDCon _ n _ _ [_, _, (_, x), (_, y)])
      = case dropAllNS !(full (gamma defs) n) of
             UN (Basic "MkPair")
                 => do x' <- reify defs !(evalClosure defs x)
                       y' <- reify defs !(evalClosure defs y)
                       pure (x', y')
             _ => cantReify val "Pair"
  reify defs val = cantReify val "Pair"

export
(Reflect a, Reflect b) => Reflect (a, b) where
  reflect fc defs lhs env (x, y)
      = do x' <- reflect fc defs lhs env x
           y' <- reflect fc defs lhs env y
           appCon fc defs (builtin "MkPair") [Erased fc False, Erased fc False, x', y']

export
Reify Namespace where
  reify defs val@(NDCon _ n _ _ [(_, ns)])
    = case dropAllNS !(full (gamma defs) n) of
        UN (Basic "MkNS")
          => do ns' <- reify defs !(evalClosure defs ns)
                pure (unsafeFoldNamespace ns')
        _ => cantReify val "Namespace"
  reify defs val = cantReify val "Namespace"

export
Reflect Namespace where
  reflect fc defs lhs env ns
    = do ns' <- reflect fc defs lhs env (unsafeUnfoldNamespace ns)
         appCon fc defs (reflectiontt "MkNS") [ns']

export
Reify ModuleIdent where
  reify defs val@(NDCon _ n _ _ [(_, ns)])
    = case dropAllNS !(full (gamma defs) n) of
        UN (Basic "MkMI")
          => do ns' <- reify defs !(evalClosure defs ns)
                pure (unsafeFoldModuleIdent ns')
        _ => cantReify val "ModuleIdent"
  reify defs val = cantReify val "ModuleIdent"

export
Reflect ModuleIdent where
  reflect fc defs lhs env ns
    = do ns' <- reflect fc defs lhs env (unsafeUnfoldModuleIdent ns)
         appCon fc defs (reflectiontt "MkMI") [ns']

export
Reify UserName where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "Basic"), [(_, str)])
                 => do str' <- reify defs !(evalClosure defs str)
                       pure (Basic str')
             (UN (Basic "Field"), [(_, str)])
                 => do str' <- reify defs !(evalClosure defs str)
                       pure (Field str')
             (UN (Basic "Underscore"), [])
                 => pure Underscore
             (NS _ (UN _), _)
                 => cantReify val "Name, reifying it is unimplemented or intentionally internal"
             _ => cantReify val "Name, the name was not found in context"
  reify defs val = cantReify val "Name, value is not an NDCon interally"

export
Reflect UserName where
  reflect fc defs lhs env (Basic x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "Basic") [x']
  reflect fc defs lhs env (Field x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "Field") [x']
  reflect fc defs lhs env Underscore
      = do appCon fc defs (reflectiontt "Underscore") []

export
Reify Name where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "UN"), [(_, str)])
                 => do str' <- reify defs !(evalClosure defs str)
                       pure (UN str')
             (UN (Basic "MN"), [(_, str), (_, i)])
                 => do str' <- reify defs !(evalClosure defs str)
                       i' <- reify defs !(evalClosure defs i)
                       pure (MN str' i')
             (UN (Basic "NS"), [(_, ns), (_, n)])
                 => do ns' <- reify defs !(evalClosure defs ns)
                       n' <- reify defs !(evalClosure defs n)
                       pure (NS ns' n')
             (UN (Basic "DN"), [(_, str), (_, n)])
                 => do str' <- reify defs !(evalClosure defs str)
                       n' <- reify defs !(evalClosure defs n)
                       pure (DN str' n')
             (UN (Basic "Nested"), [(_, ix), (_, n)])
                 => do ix' <- reify defs !(evalClosure defs ix)
                       n' <- reify defs !(evalClosure defs n)
                       pure (Nested ix' n')
             (UN (Basic "CaseBlock"), [(_, outer), (_, i)])
                 => do outer' <- reify defs !(evalClosure defs outer)
                       i' <- reify defs !(evalClosure defs i)
                       pure (CaseBlock outer' i')
             (UN (Basic "WithBlock"), [(_, outer), (_, i)])
                 => do outer' <- reify defs !(evalClosure defs outer)
                       i' <- reify defs !(evalClosure defs i)
                       pure (WithBlock outer' i')
             (NS _ (UN _), _)
                 => cantReify val "Name, reifying it is unimplemented or intentionally internal"
             _ => cantReify val "Name, the name was not found in context"
  reify defs val = cantReify val "Name, value is not an NDCon interally"

export
Reflect Name where
  reflect fc defs lhs env (UN x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "UN") [x']
  reflect fc defs lhs env (MN x i)
      = do x' <- reflect fc defs lhs env x
           i' <- reflect fc defs lhs env i
           appCon fc defs (reflectiontt "MN") [x', i']
  reflect fc defs lhs env (NS ns n)
      = do ns' <- reflect fc defs lhs env ns
           n' <- reflect fc defs lhs env n
           appCon fc defs (reflectiontt "NS") [ns', n']
  reflect fc defs lhs env (DN str n)
      = do str' <- reflect fc defs lhs env str
           n' <- reflect fc defs lhs env n
           appCon fc defs (reflectiontt "DN") [str', n']
  reflect fc defs lhs env (Nested ix n)
      = do ix' <- reflect fc defs lhs env ix
           n'  <- reflect fc defs lhs env n
           appCon fc defs (reflectiontt "Nested") [ix',n']
  reflect fc defs lhs env (CaseBlock outer i)
      = do outer' <- reflect fc defs lhs env outer
           i' <- reflect fc defs lhs env i
           appCon fc defs (reflectiontt "CaseBlock") [outer',i']
  reflect fc defs lhs env (WithBlock outer i)
      = do outer' <- reflect fc defs lhs env outer
           i' <- reflect fc defs lhs env i
           appCon fc defs (reflectiontt "WithBlock") [outer',i']
  reflect fc defs lhs env (Resolved i)
      = case !(full (gamma defs) (Resolved i)) of
             Resolved _ => cantReflect fc
                      "Name directly, Resolved is intentionally internal"
             n => reflect fc defs lhs env n
  reflect fc defs lhs env n = cantReflect fc
    "Name, reflecting it is unimplemented or intentionally internal"

export
Reify NameType where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "Bound"), _) => pure Bound
             (UN (Basic "Func"), _) => pure Func
             (UN (Basic "DataCon"), [(_, t), (_, i)])
                  => do t' <- reify defs !(evalClosure defs t)
                        i' <- reify defs !(evalClosure defs i)
                        pure (DataCon t' i')
             (UN (Basic "TyCon"), [(_, t),(_, i)])
                  => do t' <- reify defs !(evalClosure defs t)
                        i' <- reify defs !(evalClosure defs i)
                        pure (TyCon t' i')
             _ => cantReify val "NameType"
  reify defs val = cantReify val "NameType"

export
Reflect NameType where
  reflect fc defs lhs env Bound = getCon fc defs (reflectiontt "Bound")
  reflect fc defs lhs env Func = getCon fc defs (reflectiontt "Func")
  reflect fc defs lhs env (DataCon t i)
      = do t' <- reflect fc defs lhs env t
           i' <- reflect fc defs lhs env i
           appCon fc defs (reflectiontt "DataCon") [t', i']
  reflect fc defs lhs env (TyCon t i)
      = do t' <- reflect fc defs lhs env t
           i' <- reflect fc defs lhs env i
           appCon fc defs (reflectiontt "TyCon") [t', i']

export
Reify Constant where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "I"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (I x')
             (UN (Basic "I8"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (I8 x')
             (UN (Basic "I16"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (I16 x')
             (UN (Basic "I32"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (I32 x')
             (UN (Basic "I64"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (I64 x')
             (UN (Basic "BI"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (BI x')
             (UN (Basic "B8"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (B8 x')
             (UN (Basic "B16"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (B16 x')
             (UN (Basic "B32"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (B32 x')
             (UN (Basic "B64"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (B64 x')
             (UN (Basic "Str"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (Str x')
             (UN (Basic "Ch"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (Ch x')
             (UN (Basic "Db"), [(_, x)])
                  => do x' <- reify defs !(evalClosure defs x)
                        pure (Db x')
             (UN (Basic "WorldVal"), [])
                  => pure WorldVal
             (UN (Basic "IntType"), [])
                  => pure IntType
             (UN (Basic "Int8Type"), [])
                  => pure Int8Type
             (UN (Basic "Int16Type"), [])
                  => pure Int16Type
             (UN (Basic "Int32Type"), [])
                  => pure Int32Type
             (UN (Basic "Int64Type"), [])
                  => pure Int64Type
             (UN (Basic "IntegerType"), [])
                  => pure IntegerType
             (UN (Basic "Bits8Type"), [])
                  => pure Bits8Type
             (UN (Basic "Bits16Type"), [])
                  => pure Bits16Type
             (UN (Basic "Bits32Type"), [])
                  => pure Bits32Type
             (UN (Basic "Bits64Type"), [])
                  => pure Bits64Type
             (UN (Basic "StringType"), [])
                  => pure StringType
             (UN (Basic "CharType"), [])
                  => pure CharType
             (UN (Basic "DoubleType"), [])
                  => pure DoubleType
             (UN (Basic "WorldType"), [])
                  => pure WorldType
             _ => cantReify val "Constant"
  reify defs val = cantReify val "Constant"

export
Reflect Constant where
  reflect fc defs lhs env (I x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "I") [x']
  reflect fc defs lhs env (I8 x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "I8") [x']
  reflect fc defs lhs env (I16 x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "I16") [x']
  reflect fc defs lhs env (I32 x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "I32") [x']
  reflect fc defs lhs env (I64 x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "I64") [x']
  reflect fc defs lhs env (BI x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "BI") [x']
  reflect fc defs lhs env (B8 x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "B8") [x']
  reflect fc defs lhs env (B16 x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "B16") [x']
  reflect fc defs lhs env (B32 x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "B32") [x']
  reflect fc defs lhs env (B64 x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "B64") [x']
  reflect fc defs lhs env (Str x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "Str") [x']
  reflect fc defs lhs env (Ch x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "Ch") [x']
  reflect fc defs lhs env (Db x)
      = do x' <- reflect fc defs lhs env x
           appCon fc defs (reflectiontt "Db") [x']
  reflect fc defs lhs env WorldVal
      = getCon fc defs (reflectiontt "WorldVal")
  reflect fc defs lhs env IntType
      = getCon fc defs (reflectiontt "IntType")
  reflect fc defs lhs env Int8Type
      = getCon fc defs (reflectiontt "Int8Type")
  reflect fc defs lhs env Int16Type
      = getCon fc defs (reflectiontt "Int16Type")
  reflect fc defs lhs env Int32Type
      = getCon fc defs (reflectiontt "Int32Type")
  reflect fc defs lhs env Int64Type
      = getCon fc defs (reflectiontt "Int64Type")
  reflect fc defs lhs env IntegerType
      = getCon fc defs (reflectiontt "IntegerType")
  reflect fc defs lhs env Bits8Type
      = getCon fc defs (reflectiontt "Bits8Type")
  reflect fc defs lhs env Bits16Type
      = getCon fc defs (reflectiontt "Bits16Type")
  reflect fc defs lhs env Bits32Type
      = getCon fc defs (reflectiontt "Bits32Type")
  reflect fc defs lhs env Bits64Type
      = getCon fc defs (reflectiontt "Bits64Type")
  reflect fc defs lhs env StringType
      = getCon fc defs (reflectiontt "StringType")
  reflect fc defs lhs env CharType
      = getCon fc defs (reflectiontt "CharType")
  reflect fc defs lhs env DoubleType
      = getCon fc defs (reflectiontt "DoubleType")
  reflect fc defs lhs env WorldType
      = getCon fc defs (reflectiontt "WorldType")

export
Reify Visibility where
  reify defs val@(NDCon _ n _ _ _)
      = case dropAllNS !(full (gamma defs) n) of
             UN (Basic "Private") => pure Private
             UN (Basic "Export") => pure Export
             UN (Basic "Public") => pure Public
             _ => cantReify val "Visibility"
  reify defs val = cantReify val "Visibility"

export
Reflect Visibility where
  reflect fc defs lhs env Private = getCon fc defs (reflectiontt "Private")
  reflect fc defs lhs env Export = getCon fc defs (reflectiontt "Export")
  reflect fc defs lhs env Public = getCon fc defs (reflectiontt "Public")

export
Reify TotalReq where
  reify defs val@(NDCon _ n _ _ _)
      = case dropAllNS !(full (gamma defs) n) of
             UN (Basic "Total") => pure Total
             UN (Basic "CoveringOnly") => pure CoveringOnly
             UN (Basic "PartialOK") => pure PartialOK
             _ => cantReify val "TotalReq"
  reify defs val = cantReify val "TotalReq"

export
Reflect TotalReq where
  reflect fc defs lhs env Total = getCon fc defs (reflectiontt "Total")
  reflect fc defs lhs env CoveringOnly = getCon fc defs (reflectiontt "CoveringOnly")
  reflect fc defs lhs env PartialOK = getCon fc defs (reflectiontt "PartialOK")

export
Reify RigCount where
  reify defs val@(NDCon _ n _ _ _)
      = case dropAllNS !(full (gamma defs) n) of
             UN (Basic "M0") => pure erased
             UN (Basic "M1") => pure linear
             UN (Basic "MW") => pure top
             _ => cantReify val "Count"
  reify defs val = cantReify val "Count"

export
Reflect RigCount where
  reflect fc defs lhs env r
      = elimSemi (getCon fc defs (reflectiontt "M0"))
                 (getCon fc defs (reflectiontt "M1"))
                 (const (getCon fc defs (reflectiontt "MW")))
                 r

export
Reify t => Reify (PiInfo t) where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "ImplicitArg"), _) => pure Implicit
             (UN (Basic "ExplicitArg"), _) => pure Explicit
             (UN (Basic "AutoImplicit"), _) => pure AutoImplicit
             (UN (Basic "DefImplicit"), [_, (_, t)])
                 => do t' <- reify defs !(evalClosure defs t)
                       pure (DefImplicit t')
             _ => cantReify val "PiInfo"
  reify defs val = cantReify val "PiInfo"

export
Reflect t => Reflect (PiInfo t) where
  reflect fc defs lhs env Implicit
      = appCon fc defs (reflectiontt "ImplicitArg") [Erased fc False]
  reflect fc defs lhs env Explicit
      = appCon fc defs (reflectiontt "ExplicitArg") [Erased fc False]
  reflect fc defs lhs env AutoImplicit
      = appCon fc defs (reflectiontt "AutoImplicit") [Erased fc False]
  reflect fc defs lhs env (DefImplicit t)
      = do t' <- reflect fc defs lhs env t
           appCon fc defs (reflectiontt "DefImplicit") [Erased fc False, t']

export
Reify LazyReason where
  reify defs val@(NDCon _ n _ _ _)
      = case dropAllNS !(full (gamma defs) n) of
             UN (Basic "LInf") => pure LInf
             UN (Basic "LLazy") => pure LLazy
             UN (Basic "LUnknown") => pure LUnknown
             _ => cantReify val "LazyReason"
  reify defs val = cantReify val "LazyReason"

export
Reflect LazyReason where
  reflect fc defs lhs env LInf = getCon fc defs (reflectiontt "LInf")
  reflect fc defs lhs env LLazy = getCon fc defs (reflectiontt "LLazy")
  reflect fc defs lhs env LUnknown = getCon fc defs (reflectiontt "LUnknown")

export
Reify VirtualIdent where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "Interactive"), [])
                   => pure Interactive
             _ => cantReify val "VirtualIdent"
  reify defs val = cantReify val "VirtualIdent"

export
Reflect BuiltinType where
  reflect fc defs lhs env BuiltinNatural
      = getCon fc defs (reflectiontt "BuiltinNatural")
  reflect fc defs lhs env NaturalToInteger
      = getCon fc defs (reflectiontt "NaturalToInteger")
  reflect fc defs lhs env IntegerToNatural
      = getCon fc defs (reflectiontt "IntegerToNatural")

export
Reify BuiltinType where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "BuiltinNatural"), [])
                   => pure BuiltinNatural
             (UN (Basic "NaturalToInteger"), [])
                   => pure NaturalToInteger
             (UN (Basic "IntegerToNatural"), [])
                   => pure IntegerToNatural
             _ => cantReify val "BuiltinType"
  reify defs val = cantReify val "BuiltinType"

export
Reflect VirtualIdent where
  reflect fc defs lhs env Interactive
      = getCon fc defs (reflectiontt "Interactive")

export
Reify OriginDesc where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "PhysicalIdrSrc"), [(_, ident)])
                   => do ident' <- reify defs !(evalClosure defs ident)
                         pure (PhysicalIdrSrc ident')
             (UN (Basic "PhysicalPkgSrc"), [(_, fname)])
                   => do fname' <- reify defs !(evalClosure defs fname)
                         pure (PhysicalPkgSrc fname')
             (UN (Basic "Virtual"), [(_, ident)])
                   => do ident' <- reify defs !(evalClosure defs ident)
                         pure (Virtual ident')
             _ => cantReify val "OriginDesc"
  reify defs val = cantReify val "OriginDesc"

export
Reflect OriginDesc where
  reflect fc defs lhs env (PhysicalIdrSrc ident)
      = do ident' <- reflect fc defs lhs env ident
           appCon fc defs (reflectiontt "PhysicalIdrSrc") [ident']
  reflect fc defs lhs env (PhysicalPkgSrc fname)
      = do fname' <- reflect fc defs lhs env fname
           appCon fc defs (reflectiontt "PhysicalPkgSrc") [fname']
  reflect fc defs lhs env (Virtual ident)
      = do ident' <- reflect fc defs lhs env ident
           appCon fc defs (reflectiontt "Virtual") [ident']

export
Reify FC where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "MkFC"), [(_, fn), (_, start), (_, end)])
                   => do fn' <- reify defs !(evalClosure defs fn)
                         start' <- reify defs !(evalClosure defs start)
                         end' <- reify defs !(evalClosure defs end)
                         pure (MkFC fn' start' end')
             (UN (Basic "EmptyFC"), _) => pure EmptyFC
             _ => cantReify val "FC"
  reify defs val = cantReify val "FC"

export
Reflect FC where
  reflect fc defs True env _ = pure $ Erased fc False
  reflect fc defs lhs env (MkFC fn start end)
      = do fn' <- reflect fc defs lhs env fn
           start' <- reflect fc defs lhs env start
           end' <- reflect fc defs lhs env end
           appCon fc defs (reflectiontt "MkFC") [fn', start', end']
  reflect fc defs lhs env (MkVirtualFC fn start end)
      = do fn' <- reflect fc defs lhs env fn
           start' <- reflect fc defs lhs env start
           end' <- reflect fc defs lhs env end
           appCon fc defs (reflectiontt "MkFC") [fn', start', end']
  reflect fc defs lhs env EmptyFC = getCon fc defs (reflectiontt "EmptyFC")

{-
-- Reflection of well typed terms: We don't reify terms because that involves
-- type checking, but we can reflect them

-- TODO: Do we need this? Fix reify if we do.

export
Reflect (IsVar name idx vs) where
  reflect fc defs lhs env First
      = appCon fc defs (reflectiontt "First") [Erased fc False, Erased fc False]
  reflect fc defs lhs env (Later p)
      = do p' <- reflect fc defs lhs env p
           appCon fc defs (reflectiontt "Later")
                  [Erased fc False, Erased fc False,
                   Erased fc False, Erased fc False, p']

-- Assume terms are normalised so there's not Let bindings in particular
export
Reflect (Term vs) where
  reflect fc defs lhs env (Local {name} lfc _ idx prf)
      = do lfc' <- reflect fc defs lhs env lfc
           idx' <- reflect fc defs lhs env idx
           appCon fc defs (reflectiontt "Local")
                  [Erased fc False, Erased fc False, lfc', idx', Erased fc False]
  reflect fc defs lhs env (Ref rfc nt n)
      = do rfc' <- reflect fc defs lhs env rfc
           nt' <- reflect fc defs lhs env nt
           n' <- reflect fc defs lhs env n
           appCon fc defs (reflectiontt "Ref")
                  [Erased fc False, rfc', nt', n']
  reflect fc defs lhs env (Bind bfc x (Pi c p ty) sc)
      = do bfc' <- reflect fc defs lhs env bfc
           x' <- reflect fc defs lhs env x
           c' <- reflect fc defs lhs env c
           p' <- reflect fc defs lhs env p
           ty' <- reflect fc defs lhs env ty
           sc' <- reflect fc defs lhs env sc
           appCon fc defs (reflectiontt "Pi")
                  [Erased fc False, bfc', c', p', x', ty', sc']
  reflect fc defs lhs env (Bind bfc x (Lam c p ty) sc)
      = do bfc' <- reflect fc defs lhs env bfc
           x' <- reflect fc defs lhs env x
           c' <- reflect fc defs lhs env c
           p' <- reflect fc defs lhs env p
           ty' <- reflect fc defs lhs env ty
           sc' <- reflect fc defs lhs env sc
           appCon fc defs (reflectiontt "Lam")
                  [Erased fc False, bfc', c', p', x', ty', sc']
  reflect fc defs lhs env (App afc fn arg)
      = do afc' <- reflect fc defs lhs env afc
           fn' <- reflect fc defs lhs env fn
           arg' <- reflect fc defs lhs env arg
           appCon fc defs (reflectiontt "App")
                  [Erased fc False, afc', fn', arg']
  reflect fc defs lhs env (TDelayed dfc r tm)
      = do dfc' <- reflect fc defs lhs env dfc
           r' <- reflect fc defs lhs env r
           tm' <- reflect fc defs lhs env tm
           appCon fc defs (reflectiontt "TDelayed")
                  [Erased fc False, dfc', r', tm']
  reflect fc defs lhs env (TDelay dfc r ty tm)
      = do dfc' <- reflect fc defs lhs env dfc
           r' <- reflect fc defs lhs env r
           ty' <- reflect fc defs lhs env ty
           tm' <- reflect fc defs lhs env tm
           appCon fc defs (reflectiontt "TDelay")
                  [Erased fc False, dfc', r', ty', tm']
  reflect fc defs lhs env (TForce dfc r tm)
      = do dfc' <- reflect fc defs lhs env dfc
           r' <- reflect fc defs lhs env r
           tm' <- reflect fc defs lhs env tm
           appCon fc defs (reflectiontt "TForce")
                  [Erased fc False, r', dfc', tm']
  reflect fc defs lhs env (PrimVal pfc c)
      = do pfc' <- reflect fc defs lhs env pfc
           c' <- reflect fc defs lhs env c
           appCon fc defs (reflectiontt "PrimVal")
                  [Erased fc False, pfc', c']
  reflect fc defs lhs env (Erased efc _)
      = do efc' <- reflect fc defs lhs env efc
           appCon fc defs (reflectiontt "Erased")
                  [Erased fc False, efc']
  reflect fc defs lhs env (TType tfc)
      = do tfc' <- reflect fc defs lhs env tfc
           appCon fc defs (reflectiontt "TType")
                  [Erased fc False, tfc']
  reflect fc defs lhs env val = cantReflect fc "Term"
  -}


text:
module Linear.Vect

import Data.List
import Data.Vect

infixl 6 ^+^, ^-^
infixl 7 ^*, *^, ^/

public export
V2 : a -> a -> Vect 2 a
V2 x y = x :: y :: Nil

public export
V3 : a -> a -> a -> Vect 3 a
V3 x y z = x :: y :: z :: Nil

public export
V4 : a -> a -> a -> a -> Vect 4 a
V4 a b c d = a :: b :: c :: d :: Nil

public export
implementation Semigroup a => Semigroup (Vect n a) where
  (<+>) = zipWith (<+>)

public export
implementation {n : Nat} -> Monoid a => Monoid (Vect n a) where
  neutral = pure neutral

public export
implementation {n : Nat} -> Num a => Num (Vect n a) where
  (+) = zipWith (+)
  (*) = zipWith (*)
  fromInteger = pure . fromInteger

||| Compute the negation of a vector
|||
||| ```idris example
||| negated (V2 2 4)
||| ```
export
negated : (Functor f, Neg a) => f a -> f a
negated = map negate

||| Compute the left scalar product
|||
||| ```idris example
||| 2 *^ V2 3 4
||| ```
export
(*^) : (Functor f, Neg a) => a -> f a -> f a
(*^) a = map (a *)

||| Compute the right scalar product
|||
||| ```idris example
||| the (Vect ? ?) [3, 4] ^* 2
||| ```
export
(^*) : (Functor f, Neg a) => f a -> a -> f a
f ^* a = map (* a) f

||| Compute division by a scalar on the right.
export
(^/) : (Functor f, Fractional a) => f a -> a -> f a
f ^/ a = map (/a) f

public export
interface Functor f => Additive f where
  ||| The zero vector
  zero : Num a => f a

  ||| Compute the sum of two vectors
  |||
  ||| ```idris example
  ||| V2 1 2 ^+^ V2 3 4
  (^+^) : Num a => f a -> f a -> f a
  (^+^) = liftU2 (+)

  ||| Compute the difference between two vectors
  |||
  ||| ```idris example
  ||| V2 4 5 ^-^ V2 3 1
  ||| ```
  (^-^) : Neg a => f a -> f a -> f a
  x ^-^ y = x ^+^ negated y

  ||| Linearly interpolate between two vectors.
  lerp : Neg a => a -> f a -> f a -> f a
  lerp alpha u v = alpha *^ u ^+^ (1 - alpha) *^ v

  ||| Apply a function to merge the 'non-zero' components of two vectors, unioning the rest of the values.
  |||
  ||| * For a dense vector this is equivalent to 'liftA2'.
  |||
  ||| * For a sparse vector this is equivalent to 'unionWith'.
  liftU2 : (a -> a -> a) -> f a -> f a -> f a

  ||| Apply a function to the components of two vectors.
  |||
  ||| * For a dense vector this is equivalent to 'liftA2'.
  |||
  ||| * For a sparse vector this is equivalent to 'intersectionWith'.
  liftI2 : (a -> b -> c) -> f a -> f b -> f c

||| Sum over multiple vectors
|||
||| ```idris example
||| sumV [V2 1 1, V2 3 4]
||| ```
export
sumV : (Foldable f, Additive v, Num a) => f (v a) -> v a
sumV = foldl (^+^) zero

public export
interface (Num a, Fractional a, Cast a Double, Cast Double a) => Floating a where

liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c
liftA2 f x = (<*>) (map f x)

public export
implementation Applicative f => Additive f where
  zero = pure 0
  liftU2 = liftA2
  liftI2 = liftA2

public export
implementation Additive Maybe where
  zero = Nothing
  liftU2 f (Just a) (Just b) = Just (f a b)
  liftU2 _ Nothing ys = ys
  liftU2 _ xs Nothing = xs
  liftI2 = liftA2

{-
||| Produce a default basis for a vector space from which the
||| argument is drawn.
basisFor : (Traversable t, Num a) => t b -> List (t a)
-- basisFor = \t ->
--    ifoldMapOf traversed ?? t $ \i _ ->
--      return                  $
--        iover  traversed ?? t $ \j _ ->
--          if i == j then 1 else 0

basis : (Additive t, Traversable t, Num a) => List (t a)
basis = basisFor zero'
  where
    zero' : Additive v => v Int
    zero' = zero

scaled : (Traversable t, Num a) => t a -> t (t a)

unit : (Additive t, Num a) => ASetter' (t a) a -> t a
-}

||| Outer (tensor) product of two vectors
export
outer : (Functor f, Functor g, Num a) => f a -> g a -> f (g a)
outer a b = map (\x => map (*x) b) a

max_stars_repo_name: yurrriq/idris-linear

max_issues_repo_name: yurrriq/idris-linear

max_forks_repo_name: yurrriq/idris-linear


text:
||| Interfaces for marshalling Idris2 values from and to JSON
||| by using the functionality from JS.Object and Javascript's
||| internal JSON parser and stringifier.
|||
||| For regular algebraic data types, implementations can automatically
||| be derived using elaborator reflection.
module JS.JSON

import public JS.JSON.ToJSON
import public JS.JSON.FromJSON


text:
-- ---------------------------------------------------------------- [ Tree.idr ]
-- Module    : Tree.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A Dependently Typed Implementation of an AVL Tree optimised for
||| Dictionaries.
|||
||| This code is dervied from an original design by David
||| Christiansen.
|||
||| *Note* When using this Data Structure, the design is such that the
||| tree does not factor in unbalanced trees and so removal of items
||| is not permited.
module Data.AVL

import public Data.Tree
import public Data.AVL.Core
import public Data.AVL.Core.API
import public Data.AVL.Core.Quantifiers


text:
g1 : Nat -> Nat
g1 x = 5
--g1 _ = 6

g2 : (Nat, Nat) -> Nat
g2 (x, y) = x
--g2 (a, b) = 6

g3 : (Nat, Nat) -> Nat
g3 (x, y) = x
g3 _ = 6

f : Monad m => m (Nat, Nat)

h2 : Monad m => m Nat
h2 = do
  (x, y) <- f
  --  | (a, b) => pure 5
  pure x

h3 : Monad m => m Nat
h3 = do
  (x, y) <- f
    | _ => pure 5
  pure x

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


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

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

greet : RunIO ()
greet = do putStrLn "Enter your name: "
           name <- getLine
           if name == ""
              then do putStrLn "Bye bye!"
                      Quit()
              else do putStrLn ("Hello" ++ name)
                      greet
data Fuel = Dry | More (Lazy Fuel)

forever : Fuel
forever = More forever

tank : Nat -> Fuel
tank Z = Dry
tank (S k) = More (tank k)

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

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


text:
count : Nat -> Stream Nat
count n = n :: count (S n)

badCount : Nat -> Stream Nat
badCount n = n :: map S (badCount n)

data SP : Type -> Type -> Type where
  Get : (a -> SP a b) -> SP a b
  Put : b -> Inf (SP a b) -> SP a b

copy : SP a a
copy = Get (\x => Put x copy)

process : SP a b -> Stream a -> Stream b
process (Get f) (x :: xs) = process (f x) xs
process (Put b sp) xs = b :: process sp xs

badProcess : SP a b -> Stream a -> Stream b
badProcess (Get f) (x :: xs) = badProcess (f x) xs
badProcess (Put b sp) xs = badProcess sp xs

doubleInt : SP Nat Integer
doubleInt = Get (\x => Put (the Integer (cast x))
                        (Put (the Integer (cast x) * 2) doubleInt))

countStream : Nat -> Stream Nat
countStream x = x :: countStream (x + 1)

main : IO ()
main = printLn (take 10 (process doubleInt (countStream 1)))

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


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

import Data.Bitraversable

%default total

--
-- Note: Tuples in Idris are nested `Pair`s, so these don't currently act like
-- their haskell counterparts, e.g., `_2` on `(1,2,3)` will focus on `(2,3)`.
--

public export
fst_ : Lens (a,c) (b,c) a b
fst_ = lens (\(a,_) => a)
          (\(_,c),b => (b,c))

public export
snd_ : Lens (c,a) (c,b) a b
snd_ = lens (\(_,a) => a)
          (\(c,_),b => (c,b))

public export
both : Bitraversable r => Traversal (r a a) (r b b) a b
both (Mor f) = Mor (bitraverse f f)

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


text:
module Linear.Optics

import Control.Optics
import Linear.V

export
as_column : Iso (T [n] a) (T [n] b) (T [n, 1] a) (T [n, 1] b)
as_column = iso (map pure) (map (\[x] => x))

export
as_row : Iso (T [n] a) (T [n] b) (T [1, n] a) (T [1, n] b)
as_row = iso pure (\[x] => x)

export
reshaped : (size : List Nat) -> {auto ns : _} -> {auto prf : prod ns = prod size} -> Iso (T ns a) (T ns b) (T size a) (T size b)
reshaped size = iso (reshape size {ns}) (reshape ns {ns=size} {prf = sym prf})


text:
||| Date difference
|||
||| Copyright 2021. HIROKI, Hattori
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Time.Calendar.CalendarDiffDays

import Generics.Derive

%default total
%language ElabReflection

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

public export
record CalendarDiffDays where
  constructor MkCalendarDiffDays
  month : Integer
  day : Integer

%runElab derive "CalendarDiffDays" [Generic, Meta, Eq, DecEq]

public export
Show CalendarDiffDays where
  show x = "P" ++ show x.month ++ "M" ++ show x.day ++ "D"

public export
Semigroup CalendarDiffDays where
  x <+> y = MkCalendarDiffDays (x.month + y.month) (x.day + y.day)

public export
Monoid CalendarDiffDays where
  neutral = MkCalendarDiffDays 0 0

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

export calendarDay : CalendarDiffDays
calendarDay = MkCalendarDiffDays 0 1

export calendarWeek : CalendarDiffDays
calendarWeek = MkCalendarDiffDays 0 7

export calendarMonth : CalendarDiffDays
calendarMonth = MkCalendarDiffDays 1 0

export calendarYear : CalendarDiffDays
calendarYear = MkCalendarDiffDays 12 0

||| Scale by a factor. Note that @scaleCalendarDiffDays (-1)@ will not perfectly invert a duration, due to variable month lengths.
scaleCalendarDiffDays : Integer -> CalendarDiffDays -> CalendarDiffDays
scaleCalendarDiffDays k (MkCalendarDiffDays m d) =
  MkCalendarDiffDays (k * m) (k * d)

-- vim: tw=80 sw=2 expandtab :


text:
--   Copyright 2017-2018 The Lathe Authors
--
--   Licensed under the Apache License, Version 2.0 (the "License");
--   you may not use this file except in compliance with the License.
--   You may obtain a copy of the License at
--
--       http://www.apache.org/licenses/LICENSE-2.0
--
--   Unless required by applicable law or agreed to in writing,
--   software distributed under the License is distributed on an
--   "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND,
--   either express or implied. See the License for the specific
--   language governing permissions and limitations under the License.

nullMedium :
  (d : Nat) ->
  (is : mediumEdgeType d) ->
  (ts : towerEdgeType d is) ->
  Medium d is ts ->
  Medium d is ts
nullMedium d is ts (medium d' is' ts' contentType) =
  medium d' is' ts' ()

mediumEdgeType : (d : Nat) -> Type
mediumEdgeType d = case d of
  0 => () * () * ()
  1 + d' =>
    (is : mediumEdgeType d') *
    (ts : towerEdgeType d' is) *
    Medium d' is ts

towerEdgeType : (d : Nat) -> mediumEdgeType d -> Type
towerEdgeType d (is * ts * i) = case d of
  0 => ()
  1 + d' => Tower d' is ts i (nullMedium d' is ts i)

mediumContentType :
  (d : Nat) ->
  (is : mediumEdgeType d) ->
  (ts : towerEdgeType d is) ->
  Medium d is ts ->
  Type
mediumContentType d is ts (medium d' is' ts' contentType') =
  contentType'

type Medium (d : Nat) (is : mediumEdgeType d) (towerEdgeType d is)
where
  medium :
    (d : Nat) ->
    (is : mediumEdgeType d) ->
    (ts : towerEdgeType d is) ->
    Type ->
    Medium d is ts

type Tower
  (d : Nat)
  (is : mediumEdgeType d)
  (ts : towerEdgeType d is)
  (Medium d is ts)
  (Medium d is ts)
where
  towerZero :
    (d : Nat) ->
    (is : mediumEdgeType d) ->
    (ts : towerEdgeType d is) ->
    (i : Medium d is ts) ->
    (l : Medium d is ts) ->
    mediumContentType d is ts i ->
    Tower d is ts i l
  towerSucc :
    (d : Nat) ->
    let d' = 1 + d in
    (is' : mediumEdgeType d') ->
    (ts' : towerEdgeType d' is') ->
    (i' : Medium d' is' ts') ->
    (l' : Medium d' is' ts') ->
    let is * ts * i = is' in
    Tower d is ts i (medium d is ts (Tower d' is' ts' l' i')) ->
    mediumContentType d' is' ts' i' ->
    Tower d' is' ts' i' l'

nullMedium :
  (d : Nat) -> (e : mediumEdgeType d) -> Medium d e -> Medium d e
nullMedium d e m = case m of
  mediumZero contentType => mediumZero ()
  mediumSucc d' e' i t contentTypes => mediumSucc d' e' i t (\_ -> ())

towerEdgeType : (d : Nat) -> Type
towerEdgeType d = case d of
  0 => (() * ()) * ()
  1 + d' =>
    ((e * t) * l : mediumEdgeType d) *
    Tower d' (e * t) (nullMedium d' e l) l

mediumEdgeType : (d : Nat) -> Type
mediumEdgeType d = case d of
  0 => () * ()
  1 + d' => (me * t : towerEdgeType d') * Medium d' me

type Medium (d : Nat) (mediumEdgeType d) where
  mediumZero : Type -> Medium 0 ((() * ()) * ())
  mediumSucc :
    (d : Nat) ->
    (me * t : towerEdgeType d) ->
    (i : Medium d me) ->
    (Tower d (me * t) i (nullMedium d me i) -> Type) ->
    Medium (1 + d) ((me * t) * i)

type Tower
  (d : Nat)
  (me * t : towerEdgeType d)
  (Medium d me)
  (Medium d me)
where
  towerZero :
    (d : Nat) ->
    (me * t : towerEdgeType d) ->
    (i : Medium d me) ->
    (l : Medium d me) ->
    (case i of
      mediumZero contentType => contentType
      mediumSucc d' e' i' contentTypes =>
        -- note that e' * i' = me
        -- let (meme * met) * mel = me in
        -- t : Tower d' (meme * met) (nullMedium d' meme mel) mel
        -- contentTypes : Tower d' (meme * met) mel (nullMedium d' meme mel) -> Type
        (contentEdge : Tower d' e' i' (nullMedium d' e' l')) *
        contentTypes contentEdge) ->
    Tower d e i l

nullMedium :
  (d : Nat) -> (e : towerEdgeType d) -> Medium d e -> Medium d e
nullMedium d e m = case m of
  mediumZero c = mediumZero ()
  mediumSucc d' e' m' c = mediumSucc d' e' m' (\_ -> ())

towerEdgeType : (d : Nat) -> Type
towerEdgeType d = case d of
  0 => () * () * ()
  1 + d' =>
    (e : towerEdgeType d') *
    (l : Medium d' e) *
    Tower d' e (nullMedium l) l

-- TODO: mediumZero, mediumSucc, subtowerMedium, towerNullify

type Tower (d : Nat) (e : towerEdgeType d) (Medium d e) (Medium d e)
where
  nil :
    (d : Nat) ->
    (e : towerEdgeType d) ->
    (i : Medium d e) ->
    (l : Medium d e) ->
    (case i of
      mediumZero contentType => contentType
      mediumSucc d' e' contentTypes => contentTypes e) ->
    Tower d e i l
  cons
    (d : Nat) ->
    let d' = 1 + d in
    (e : towerEdgeType d') ->
    let ee * el * et = e in
    (i : Medium d' e) ->
    (l : Medium d' e) ->
    (subtowers : Tower d TODO el (subtowerMedium d e l i)) ->
    (case i of
      mediumSucc d'' e' contentTypes =>
        contentTypes
          (towerNullify d TODO e (subtowerMedium d e l i)
            subtowers) ->
        Tower d' e i l)

edgeLakeMedium :
  (d : Nat) -> (e : towerEdgeType d) -> Medium d e -> Medium d e
edgeLakeMedium d e i = case d of
  0 => mediumZero ()
  1 + d' => mediumSucc d' e i (\_ -> ())

edgeType : (d : Nat) -> (e : towerEdgeType d) -> Medium d e -> Type
edgeType d e i = Tower d e i (edgeLakeMedium d e i)

type Medium (d : Nat) (towerEdgeType d) where
  mediumZero : Type -> Medium 0 (() * () * ())
  mediumSucc :
    (d : Nat) ->
    (e : towerEdgeType (1 + d)) ->
    (m : Medium (1 + d) e) ->
    (edgeType (1 + d) e m -> Type) ->
    Medium (1 + d) e

max_stars_repo_name: rocketnia/lexmeta

max_issues_repo_name: rocketnia/lexmeta

max_forks_repo_name: lathe/punctaffy-for-racket


text:
module IntegerThruNat

%default total

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

namespace Bad1

  -- One example of bad integer definition
  public export
  data Intege = MkInteger (Bool, Nat)

  -- `MkInteger (True, 0)` effectively equal to `MkInteger (False, 0)`
  -- but functions need to match both

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

namespace Bad2

  public export
  data Intege = Zero
              | Pos Nat
              | Neg Nat

  -- `Pos 0` meaning zero is bad by the same reason as the example above.

  -- But we can say that `Pos n` means effectively `n + 1` and `Neg n` means effectively `n - 1`.

  export
  div : Intege -> Intege -> Maybe Intege
  div _ Zero = Nothing
  div Zero _ = Just Zero
  div (Pos x) (Pos y) = Just $ Pos ?pospos
  div (Neg x) (Neg y) = Just $ Pos ?negneg
  div (Pos x) (Neg y) = Just $ Pos ?posneg
  div (Neg x) (Pos y) = Just $ Pos ?negpos

  -- Then everything is okay during the match except it's inconvenient:

  export
  abs : Intege -> Nat
  abs Zero = Z
  abs (Pos x) = S x
  abs (Neg x) = x -- F*CK! It's tempting to forget to add `S` when using matched `Nat`

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

namespace AsIf

  -- What we can do (at least, as I thought) in Arend (shown with non-existent Idris syntax) --

--  data Intege = Zero
--              | Pos Nat with | Pos 0 => Zero
--              | Neg Nat with | Neg 0 => Zero

  -- Here `Pos 0` means zero and is literally equal to `Zero`. And to the `Neg 0` too.
  -- During the pattern match we can match on `Zero`, `Pos x` (including x=0) or both as we want.

--  div : Intege -> Intege -> Maybe Intege
--  div _ Zero = Nothing
--  div Zero _ = Just Zero
--  div (Pos (S x)) (Pos (S y)) = ...
--  ... etc ...
    -- Here ^^^^^^^ we can match `Pos x`, but since the case of `Zero` is already matched, we can match just `Pos (S x)`.

--  abs : Intege -> Nat
--  abs (Pos x) = x
--  abs (Neg x) = x
    -- Here ^^^ we even don't match `Zero` because it's covered by both cases.
    -- And compiler would check that `Pos 0` and `Neg 0` cases would give the same result.
    -- So `abs (Neg x) = S x` won't typecheck.

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

namespace Ersatz

  -- Let's have the same meaning as we wanted (i.e. `Pos 0` and `Neg 0` are effectively `Zero`)

  public export
  data Intege = Zero
              | Pos Nat
              | Neg Nat

  -- But let's define equivalences as a separate function!

  public export
  0 intege : Intege -> Intege
  intege (Pos 0) = Zero
  intege (Neg 0) = Zero
  intege x = x

  public export
  abs : Intege -> Nat
  abs (Pos x) = x
  abs (Neg x) = x
  abs Zero = 0 -- still need to match it

  export
  0 abs_holds_equiv : (n : Intege) -> abs n = abs (intege n)
  abs_holds_equiv Zero        = Refl
  abs_holds_equiv (Pos Z)     = Refl
  abs_holds_equiv (Pos $ S _) = Refl
  abs_holds_equiv (Neg Z)     = Refl
  abs_holds_equiv (Neg $ S _) = Refl

  -- But this should be repeated for each function (and matching should go for each argument). It could be done automatically.
  -- In the automatic variant, equivalence function could be partial meaning that it's identity on those inputs that it's not defined on.

  -- Also, covering check needs to be modified in this case to make able to not to write redundant cases.

  -- Well, can this mechanism we implemented with Idris elaborations?


text:
module Control.Monad.Either

import public Control.Monad.Error.Either as Control.Monad.Either
import public Control.Monad.Error.Interface as Control.Monad.Either


text:
module Utils.Accomodation

import Data.Vect
%hide Data.Vect.(::)
%default total
%access public export

accomod : String -> Nat -> List String
accomod x k = helper (sort (map (pack . (\x => [x])) (unpack x))) k where
  helper : List String -> Nat -> List String
  helper alph Z = []
  helper alph (S Z) = alph
  helper alph (S (S k)) = [| alph ++ helper alph (S k) |]

degree : Nat -> Nat -> Nat
degree x k = helper x k 0 1 where
  helper : Nat -> Nat -> Nat -> Nat -> Nat
  helper x k r acc = case x < acc of
                        False => assert_total (helper x k (S r) (acc * k))
                        True => r

max_stars_repo_name: GrandArchTemplar/QuantumProgramming

max_issues_repo_name: GrandArchTemplar/QuantumProgramming

max_forks_repo_name: GrandArchTemplar/QuantumProgramming


text:
module Data.Tagged

import Data.Bifunctor
import Data.Profunctor

%default total

public export
data Tagged : (a : Type) -> (b : Type) -> Type where
  MkTagged: b -> Tagged a b

public export
retag : Tagged s b -> Tagged t b
retag (MkTagged b) = MkTagged b

||| Alias for 'unTagged'
public export
untag : Tagged s b -> b
untag (MkTagged x) = x

||| Tag a value with its own type.
public export
tagSelf : a -> Tagged a a
tagSelf = MkTagged

||| 'asTaggedTypeOf' is a type-restricted version of 'const'. It is usually used as an infix operator, and its typing forces its first argument (which is usually overloaded) to have the same type as the tag of the second.
public export
asTaggedTypeOf : s -> Tagged s b -> s
asTaggedTypeOf = const

||| 'untagSelf' is a type-restricted version of 'untag'.
public export
untagSelf : Tagged a a -> a
untagSelf (MkTagged x) = x

public export
Semigroup a => Semigroup (Tagged s a) where
  (MkTagged a) <+> (MkTagged b) = MkTagged (a <+> b)

public export
Monoid a => Monoid (Tagged s a) where
  neutral = MkTagged neutral

public export
Functor (Tagged s) where
  map f (MkTagged x) = MkTagged (f x)

public export
implementation Applicative (Tagged s) where
  pure = MkTagged
  (MkTagged f) <*> (MkTagged x) = MkTagged (f x)

public export
implementation Monad (Tagged s) where
  (MkTagged m) >>= k = k m

public export
implementation Bifunctor Tagged where
  bimap _ g (MkTagged b) = MkTagged (g b)

public export
implementation Profunctor Tagged where
  dimap _ f (MkTagged s) = MkTagged (f s)
  lmap _ = retag
  rmap = map

public export
implementation Choice Tagged where
  left' (MkTagged b) = MkTagged (Left b)
  right' (MkTagged b) = MkTagged (Right b)


text:
||| Types for representing a DOT file/graph in Idris
module Graphics.DOT.AST

import Data.Vect

||| The stuff in the AST of a DOT graph
public export
data DOT : Type where
  -- Graphs - The bit where everything starts
  Graph :  (strict : Bool)
        -> (type : DOT)
        -> (id_ : Maybe DOT)
        -> (stmtList : DOT)
        -> DOT

  -- Statements
  StmtList : List DOT -> DOT
  Stmt : (stmt : DOT) -> DOT

  -- Keywords
  Node : DOT
  Edge : DOT
  GraphKW : DOT
  DiGraph : DOT
  SubGraph : DOT
  Strict : DOT

  -- Identifiers
  NameID : (name : String) -> DOT
  NumeralID : (numeral : String) -> DOT
  StringID : (str : String) -> DOT
  HTML_ID : (html : String) -> DOT

  -- Attributes
  -- a_list AST node, takes list of stuff
  AList : List DOT -> DOT   -- non-empty?
  AttrList : List DOT -> DOT
  AttrStmt : (kw : DOT) -> (attrList : DOT) -> DOT

  -- Operators
  Assign : (ids : Vect 2 DOT) -> DOT
  StrConcat : Vect (S (S k)) DOT -> DOT   -- must have at least 2 strings
  -- unsure if this is would be better: Vect 2 DOT -> DOT
  DiGrEdgeOp : DOT
  GrEdgeOp : DOT

  -- Edges
  -- unsure about this one...
  -- EdgeRHS : (edgeOp : DOT) -> DOT -> (moreRHS : List DOT) -> DOT
  -- EdgeRHS : List (DOT, DOT) -> DOT   -- this might be better?
  EdgeRHS : List DOT -> DOT
  EdgeStmt : DOT -> (rhs : DOT) -> (attrList : Maybe DOT) -> DOT

  -- Nodes
  NodeID : (id_ : DOT) -> (port : Maybe DOT) -> DOT
  NodeStmt : (nID : DOT) -> (attrList : Maybe DOT) -> DOT

  -- Ports
  IDPort  : (id_ : DOT) -> (c_pt : Maybe DOT) -> DOT
  CPTPort : (c_pt : DOT) -> DOT

  -- Subgraphs
  SubgraphID : (id_ : Maybe DOT) -> DOT
  Subgraph : (sID : Maybe DOT) -> (stmtList : DOT) -> DOT

  -- Compass points
  North : DOT
  NorthEast : DOT
  East : DOT
  SouthEast : DOT
  South : DOT
  SouthWest : DOT
  West : DOT
  NorthWest : DOT
  CenterCPt : DOT
  UnderCPt : DOT

export
Show DOT where
  show (Graph strict type id_ stmtList) =
    "(Gr " ++ show strict ++ show type ++ show id_ ++ show stmtList
  show (StmtList xs) = show xs
  show (Stmt stmt) = show stmt
  show Node = "Node"
  show Edge = "Edge"
  show GraphKW = "GrKW"
  show DiGraph = "DiGr"
  show SubGraph = "SuGr"
  show Strict = "Strict"
  show (NameID name) = "(Name " ++ name ++ ")"
  show (NumeralID numeral) = "(Nume " ++ numeral ++ ")"
  show (StringID str) = "(StrI " ++ str ++ ")"
  show (HTML_ID html) = "(HTML " ++ html ++ ")"
  show (AList xs) = "(AList:=" ++ show xs ++ ")"
  show (AttrList xs) = "(AttrList:=" ++ show xs ++ ")"
  show (AttrStmt kw attrList) = "(AttrStmt " ++ show kw ++ show attrList ++ ")"
  show (Assign [a, b]) = "(Assign " ++ show a ++ show b ++ ")"
  show (StrConcat xs) = "(StrConc " ++ show xs ++ ")"
  show DiGrEdgeOp = "-->"
  show GrEdgeOp = "---"
  show (EdgeRHS xs) = "(ERhs " ++ show xs ++ ")"
  show (EdgeStmt x rhs attrList) =
    "(EStmt " ++ show x ++ show rhs ++ show attrList ++ ")"
  show (NodeID id_ port) =
    "(NodeID " ++ show id_ ++ (case port of Nothing => ""; Just p => ":" ++ show p) ++ ")"
  show (NodeStmt nID attrList) = "(NodeStmt " ++ show nID ++ show attrList ++ ")"
  show (IDPort id_ c_pt) =
    "(IDPort " ++ show id_ ++ (case c_pt of Nothing => ""; Just pt => ":" ++ show pt) ++ ")"
  show (CPTPort c_pt) = show c_pt
  show (SubgraphID id_) = show id_
  show (Subgraph sID stmtList) = "(Subgraph " ++ show sID ++ show stmtList ++ ")"
  show North = "North"
  show NorthEast = "NorthEast"
  show East = "East"
  show SouthEast = "SouthEast"
  show South = "South"
  show SouthWest = "SouthWest"
  show West = "West"
  show NorthWest = "NorthWest"
  show CenterCPt = "Center"
  show UnderCPt = "_DEF_"


text:
module Language.LSP.Message.DocumentSymbols

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

%language ElabReflection
%default total

namespace SymbolKind
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
  public export
  data SymbolKind
    = File
    | Module
    | Namespace
    | Package
    | Class
    | Method
    | Property
    | Field
    | Constructor
    | Enum
    | Interface
    | Function
    | Variable
    | Constant
    | String_
    | Number
    | Boolean
    | Array
    | Object
    | Key
    | Null
    | EnumMember
    | Struct
    | Event
    | Operator
    | TypeParameter

export
ToJSON SymbolKind where
  toJSON File          = JNumber 1
  toJSON Module        = JNumber 2
  toJSON Namespace     = JNumber 3
  toJSON Package       = JNumber 4
  toJSON Class         = JNumber 5
  toJSON Method        = JNumber 6
  toJSON Property      = JNumber 7
  toJSON Field         = JNumber 8
  toJSON Constructor   = JNumber 9
  toJSON Enum          = JNumber 10
  toJSON Interface     = JNumber 11
  toJSON Function      = JNumber 12
  toJSON Variable      = JNumber 13
  toJSON Constant      = JNumber 14
  toJSON String_       = JNumber 15
  toJSON Number        = JNumber 16
  toJSON Boolean       = JNumber 17
  toJSON Array         = JNumber 18
  toJSON Object        = JNumber 19
  toJSON Key           = JNumber 20
  toJSON Null          = JNumber 21
  toJSON EnumMember    = JNumber 22
  toJSON Struct        = JNumber 23
  toJSON Event         = JNumber 24
  toJSON Operator      = JNumber 25
  toJSON TypeParameter = JNumber 26

export
FromJSON SymbolKind where
  fromJSON (JNumber 1)  = pure File
  fromJSON (JNumber 2)  = pure Module
  fromJSON (JNumber 3)  = pure Namespace
  fromJSON (JNumber 4)  = pure Package
  fromJSON (JNumber 5)  = pure Class
  fromJSON (JNumber 6)  = pure Method
  fromJSON (JNumber 7)  = pure Property
  fromJSON (JNumber 8)  = pure Field
  fromJSON (JNumber 9)  = pure Constructor
  fromJSON (JNumber 10) = pure Enum
  fromJSON (JNumber 11) = pure Interface
  fromJSON (JNumber 12) = pure Function
  fromJSON (JNumber 13) = pure Variable
  fromJSON (JNumber 14) = pure Constant
  fromJSON (JNumber 15) = pure String_
  fromJSON (JNumber 16) = pure Number
  fromJSON (JNumber 17) = pure Boolean
  fromJSON (JNumber 18) = pure Array
  fromJSON (JNumber 19) = pure Object
  fromJSON (JNumber 20) = pure Key
  fromJSON (JNumber 21) = pure Null
  fromJSON (JNumber 22) = pure EnumMember
  fromJSON (JNumber 23) = pure Struct
  fromJSON (JNumber 24) = pure Event
  fromJSON (JNumber 25) = pure Operator
  fromJSON (JNumber 26) = pure TypeParameter
  fromJSON _ = Nothing

namespace SymbolTag
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
  public export
  data SymbolTag = Deprecated

export
ToJSON SymbolTag where
  toJSON Deprecated = JNumber 1

export
FromJSON SymbolTag where
  fromJSON (JNumber 1) = pure Deprecated
  fromJSON _ = Nothing

namespace DocumentSymbolClientCapabilities
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
  public export
  record DocumentSymbolKind where
    constructor MkDocumentSymbolKind
    valueSet : Maybe (List SymbolKind)
  %runElab deriveJSON defaultOpts `{{DocumentSymbolKind}}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
  public export
  record DocumentSymbolTag where
    constructor MkDocumentSymbolTag
    valueSet : Maybe (List SymbolTag)
  %runElab deriveJSON defaultOpts `{{DocumentSymbolTag}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
public export
record DocumentSymbolClientCapabilities where
  constructor MkDocumentSymbolClientCapabilities
  dynamicRegistration               : Maybe Bool
  symbolKind                        : Maybe DocumentSymbolKind
  hierarchicalDocumentSymbolSupport : Maybe Bool
  tagSupport                        : Maybe DocumentSymbolTag
  labelSupport                      : Maybe Bool
%runElab deriveJSON defaultOpts `{{DocumentSymbolClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
public export
record DocumentSymbolOptions where
  constructor MkDocumentSymbolOptions
  workDoneProgress : Maybe Bool
  label            : Maybe String
%runElab deriveJSON defaultOpts `{{DocumentSymbolOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
public export
record DocumentSymbolRegistrationOptions where
  constructor MkDocumentSymbolRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
  label            : Maybe String
%runElab deriveJSON defaultOpts `{{DocumentSymbolRegistrationOptions}}

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

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
public export
record DocumentSymbol where
  constructor MkDocumentSymbol
  name           : String
  detail         : Maybe String
  kind           : SymbolKind
  tags           : Maybe (List SymbolTag)
  deprecated     : Maybe Bool
  range          : Range
  selectionRange : Range
  children       : Maybe (List (Inf DocumentSymbol))

export -- FIXME?: Can I Avoid assert_total? Try indexing it with the depth
ToJSON DocumentSymbol where
  toJSON (MkDocumentSymbol name detail kind tags deprecated range selectionRange children) = assert_total $
    JObject (catMaybes [ Just ("name", toJSON name)
                       , (MkPair "detail" . toJSON) <$> detail
                       , Just ("kind", toJSON kind)
                       , (MkPair "tags" . toJSON) <$> tags
                       , Just ("deprecated", toJSON deprecated)
                       , Just ("range", toJSON range)
                       , Just ("selectionRange", toJSON selectionRange)
                       , (MkPair "children" . toJSON) <$> children
                       ])

export covering
FromJSON DocumentSymbol where
  fromJSON (JObject arg) =
    pure MkDocumentSymbol <*> (lookup "name" arg >>= fromJSON)
                          <*> (pure $ lookup "detail" arg >>= fromJSON)
                          <*> (lookup "kind" arg >>= fromJSON)
                          <*> (pure $ lookup "tags" arg >>= fromJSON)
                          <*> (pure $ lookup "deprecated" arg >>= fromJSON)
                          <*> (lookup "range" arg >>= fromJSON)
                          <*> (lookup "selectionRange" arg >>= fromJSON)
                          <*> (pure $ lookup "children" arg >>= fromJSON)
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
public export
record SymbolInformation where
  constructor MkSymbolInformation
  name          : String
  kind          : SymbolKind
  tags          : Maybe (List SymbolTag)
  deprecated    : Maybe Bool
  location      : Location
  containerName : Maybe String
%runElab deriveJSON defaultOpts `{{SymbolInformation}}


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

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

{-
  ported from file kernel/libsel4/include/sel4/shared_types.h
-}

module seL4.SharedTypes

import seL4.Types

%access public export
%default total

SeL4_IPCBufferP : Type
SeL4_IPCBufferP = Int -- dummy definition at the moment

SeL4_MessageInfo : Type
SeL4_MessageInfo = SeL4_Word


text:
module Control.Monad.TransitionIndexed

infixl 1 >>>=, =<<<, >>>

%hide Prelude.pure

||| A TransitionIndexed pointed type defines purity but is not necessarily
||| Applicative.
public export
interface TransitionIndexedPointed z (0 m : (ty : Type) -> z -> (ty -> z) -> Type) | m where
  pure : {0 a : Type} -> {0 f : a -> z} -> (x : a) -> m a (f x) f

||| A TransitionIndexed monad is like an indexed monad but the third
||| index is determined by a function that takes the first index as input.
|||
||| One readily available example of a type that fits this interface is
||| a type representing stateful transitions and the values that fall
||| out of them.
|||
||| For example, take the final Door example from "Type-Driven Development with Idris."
|||
|||    data DoorCmd : (ty : Type) ->
|||                   DoorState ->
|||                   (ty -> DoorState) ->
|||                   Type
public export
interface TransitionIndexedMonad z (0 m : (ty : Type) -> z -> (ty -> z) -> Type) | m where
  bind : {0 x : z} -> {0 f : a -> z} -> {0 g : b -> z} -> m a x f -> ((res : a) -> m b (f res) g) -> m b x g

public export
(>>>=) : TransitionIndexedMonad z m => m a x f -> ((res : a) -> m b (f res) g) -> m b x g
(>>>=) = bind

||| Flipped version of `>>>=
public export
(=<<<) : TransitionIndexedMonad z m => {0 a : Type} -> {0 f : a -> z} -> ((res : a) -> m b (f res) g) -> m a x f -> m b x g
(=<<<) = flip (>>>=)

public export
(>>>) : TransitionIndexedMonad z m => m () x f -> Lazy (m b (f ()) g) -> m b x g
(>>>) y w = y >>>= \() => w

||| Conditionally execute an expression when the boolean is true.
export
when : TransitionIndexedPointed z m => Bool -> Lazy (m () (f ()) f) -> m () (f ()) f
when True w  = w
when False w = pure ()

||| Execute an expression unless the boolean is true.
export
unless : TransitionIndexedPointed z m => Bool -> Lazy (m () (f ()) f) -> m () (f ()) f
unless = when . not

||| Map each element of a structure to a computation, evaluate those
||| computations and discard the results.
public export
traverse_ : (Foldable t, TransitionIndexedPointed z m, TransitionIndexedMonad z m) => (a -> m b x (const x)) -> t a -> m () x (const x)
traverse_ f = foldr (\x,acc => (f x) >>>= (const acc)) (pure ())

||| Evaluate each computation in a structure and discard the results.
public export
sequence_ : (Foldable t, TransitionIndexedPointed z m, TransitionIndexedMonad z m) => t (m a x (const x)) -> m () x (const x)
sequence_ = foldr (\x, acc => x >>>= (const acc)) (pure ())

||| Like `traverse_` but with the arguments flipped.
public export
for_ : (Foldable t, TransitionIndexedPointed z m, TransitionIndexedMonad z m) => t a -> (a -> m b x (const x)) -> m () x (const x)
for_ = flip traverse_

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
-- by Tojans

-- to run this:
-- idris 99bottles.idr
-- > beerSong 1
-- > beerSong 99
-- > beerSong 100 -- throws

beerSong : Fin 100 -> String
beerSong x = verses x where

    -- invoke this in the CLI using `bottlesOfBeer (the (Fin 10) 4)`
    bottlesOfBeer : Fin n -> String
    bottlesOfBeer fZ      = "No more bottles of beer"
    bottlesOfBeer (fS fZ) = "1 bottle of beer"
    bottlesOfBeer k       = (show (finToInteger k)) ++ " bottles of beer"

    verse : Fin n -> String
    verse fZ     = ""
    verse (fS n) =
        (bottlesOfBeer (fS n)) ++ " on the wall,\n" ++
        (bottlesOfBeer (fS n)) ++ "\n" ++
        "Take one down, pass it around\n" ++
        (bottlesOfBeer n) ++ " on the wall\n"

    verses : Fin n -> String
    verses fZ     = ""
    verses (fS n) = (verse (fS n)) ++ (verses n)


text:
module Dom

import Control.ST
import public Js.Html
import public Js.VirtualDom
import public Js.ASync

data GuiRefData : (a : Type) -> (f : a -> Type) -> (g : a -> Type) -> a -> Type where
  MkGuiRefData : ((z:a) -> f z -> Html (g z)) -> JSIORef (y:a ** JSIOFifoQueue (g y)) -> JSIOFifoQueue (g x) -> f x -> Html (g x) -> GuiRefData a f g x

export
data DomOption : (a:Type) -> (a->Type) -> (a->Type) -> Type where
  OnResize : ((x:a) -> g x) -> DomOption a f g

export
onresize : b -> DomOption () (const a) (const b)
onresize x = OnResize $ \() => x

record DomOptionRec (a : Type) (f:a->Type) (g:a->Type) where
  constructor MkDomOptionRec
  onresizeOption : Maybe ((x:a) -> g x)

domOptionsToRec : List (DomOption a f g) -> DomOptionRec a f g
domOptionsToRec [] = MkDomOptionRec Nothing
domOptionsToRec (OnResize x :: r) = record {onresizeOption = Just x} $ domOptionsToRec r

public export
interface Dom  (m : Type -> Type) where
  DomRef : (a:Type) -> (f : a -> Type) -> (g : a -> Type) -> a -> Type

  initBody : List (DomOption a f g) -> ((x:a) -> f x -> Html (g x)) -> (z:a) -> f z -> ST m Var [add (DomRef a f g z)]
  clearDom : (dom : Var) -> ST m () [remove dom (DomRef a f g z)]
  domPut : (dom : Var) -> {x:a} -> f x -> ST m () [dom ::: (DomRef a f g x)]
  domPutAnimated : (dom : Var) -> {x:a} -> List AnimationOption -> f x -> ST m () [dom ::: (DomRef a f g x)]
  domPutM : (dom : Var) -> (y:a) -> f y -> ST m () [dom ::: (DomRef a f g x) :-> (DomRef a f g y)]
  domGet : (dom : Var) -> {x:a} -> ST m (f x) [dom ::: DomRef a f g x]
  getInput : (dom : Var) -> {x:a} -> ST m (g x) [dom ::: DomRef a f g x]

export
domUpdate : Dom m => (dom : Var) -> {x:a} -> (f x -> f x) -> ST m () [dom ::: (DomRef {m} a f g x)]
domUpdate v h =
  do
    s <- domGet v
    domPut v (h s)

export
domUpdateAnimated : Dom m => (dom : Var) -> {x:a} -> List AnimationOption -> (f x -> f x) -> ST m () [dom ::: (DomRef {m} a f g x)]
domUpdateAnimated v opts h =
  do
    s <- domGet v
    domPutAnimated v opts (h s)

export
domUpdateM : Dom m => (dom : Var) -> (x:a) -> (y:a) -> (f x -> f y) -> ST m () [dom ::: (DomRef {m} a f g x) :-> (DomRef {m} a f g y)]
domUpdateM v x y h =
  do
    s <- domGet v
    domPutM v y (h s)

setOnResizeOpt : (g : a -> Type) -> Maybe ((x:a) -> g x) -> JSIORef (y:a ** JSIOFifoQueue (g y)) -> JS_IO ()
setOnResizeOpt g Nothing ref =
  jscall
    "window.onresize = undefined"
    (JS_IO ())
setOnResizeOpt g (Just h) ref =
  jscall
    "window.onresize = %0"
    (JsFn (() -> JS_IO ()) -> JS_IO ())
    (MkJsFn $ \() =>
      do
        (x ** q) <- readJSIORef ref
        let z = h x
        putInQueue z q
    )

setOpts : DomOptionRec a f g -> JSIORef (y:a ** JSIOFifoQueue (g y)) -> JS_IO ()
setOpts {g} x q = setOnResizeOpt g (onresizeOption x) q

initBodyRaw : List (DomOption a f g) -> ((x:a) -> f x -> Html (g x) ) -> f z -> JS_IO (GuiRefData a f g z)
initBodyRaw {a} {f} {g} {z} opts render st0 =
  do
    let n0 = render z st0
    let opts' = domOptionsToRec opts
    queue <- newJSIOFifoQueue (g z)
    ref <- newJSIORef (z ** queue)
    setOpts opts' ref
    initialyzeBody queue n0
    pure $ MkGuiRefData render ref queue st0 n0

export
implementation Dom ASync where
  DomRef a f g z =
    State (GuiRefData a f g z)
  initBody opts render a0 start =
    do
      guiR <- lift $ liftJS_IO $ initBodyRaw opts render start
      r <- new guiR
      pure r
  clearDom v =
    do
      (MkGuiRefData _ _ _ _ n) <- read v
      lift $ liftJS_IO $ clearNode n
      delete v

  domPut v {x} newSt =
    do
      (MkGuiRefData render ref queue st n) <- read v
      lift $ liftJS_IO $ updateNode n (render x newSt)
      write v $ MkGuiRefData render ref queue newSt n
      pure ()
  domPutAnimated v {x} opts newSt =
    do
      (MkGuiRefData render ref queue st n) <- read v
      lift $ liftJS_IO $ animateNode opts n (render x newSt)
      write v $ MkGuiRefData render ref queue newSt n
      pure ()
  domPutM {g} v x newSt =
    do
      (MkGuiRefData render ref queue st n) <- read v
      queue <- lift $ liftJS_IO $ newJSIOFifoQueue (g x)
      lift $ liftJS_IO $ writeJSIORef ref (x**queue)
      n' <- lift $ liftJS_IO $ updateNodeM queue n (render x newSt)
      write v $ MkGuiRefData render ref queue newSt n'
      pure ()
  domGet v =
    do
      (MkGuiRefData render ref queue st n) <- read v
      pure st
  getInput v =
    do
      (MkGuiRefData render ref queue st n) <- read v
      r <- lift $ getFromQueue queue
      pure r

public export
interface Window (m:Type -> Type) where
  getLocationSearch : STrans m String xs (const xs)
  innerWidth : STrans m Double xs (const xs)
  innerHeight : STrans m Double xs (const xs)
  availableWidth : STrans m Double xs (const xs)
  availableHeight : STrans m Double xs (const xs)

export
implementation Window ASync where
  getLocationSearch = lift $ liftJS_IO $ jscall "decodeURI(window.location.search)" (JS_IO String)
  innerWidth = lift $ liftJS_IO (jscall "window.innerWidth" (JS_IO Double))
  innerHeight = lift $ liftJS_IO (jscall "window.innerHeight" (JS_IO Double))
  availableWidth = lift $ liftJS_IO $ availableWidth_
  availableHeight = lift $ liftJS_IO $ availableHeight_

max_stars_repo_name: banyan-infrastructure/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs