text:
module Compiler.Common

import Compiler.ANF
import Compiler.CompileExpr
import Compiler.Inline
import Compiler.LambdaLift
import Compiler.Opts.CSE
import Compiler.VMCode

import Core.Binary.Prims
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Options
import Core.Ord
import Core.TT
import Core.TTC
import Libraries.Data.IOArray
import Libraries.Data.SortedMap
import Libraries.Utils.Path

import Data.List
import Data.List1
import Libraries.Data.NameMap
import Data.String as String

import Idris.Env

import System.Directory
import System.Info
import System.File

%default covering

||| Generic interface to some code generator
public export
record Codegen where
  constructor MkCG
  ||| Compile an Idris 2 expression, saving it to a file.
  compileExpr : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
                ClosedTerm -> (outfile : String) -> Core (Maybe String)
  ||| Execute an Idris 2 expression directly.
  executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
  ||| Incrementally compile definitions in the current module (toIR defs)
  ||| if supported
  ||| Takes a source file name, returns the name of the generated object
  ||| file, if successful, plus any other backend specific data in a list
  ||| of strings. The generated object file should be placed in the same
  ||| directory as the associated TTC.
  incCompileFile : Maybe (Ref Ctxt Defs ->
                          (sourcefile : String) ->
                          Core (Maybe (String, List String)))
  ||| If incremental compilation is supported, get the output file extension
  incExt : Maybe String

-- Say which phase of compilation is the last one to use - it saves time if
-- you only ask for what you need.
public export
data UsePhase = Cases | Lifted | ANF | VMCode

Eq UsePhase where
  (==) Cases Cases = True
  (==) Lifted Lifted = True
  (==) ANF ANF = True
  (==) VMCode VMCode = True
  (==) _ _ = False

Ord UsePhase where
  compare x y = compare (tag x) (tag y)
    where
      tag : UsePhase -> Int
      tag Cases = 0
      tag Lifted = 1
      tag ANF = 2
      tag VMCode = 3

public export
record CompileData where
  constructor MkCompileData
  mainExpr : CExp [] -- main expression to execute. This also appears in
                     -- the definitions below as MN "__mainExpression" 0
  namedDefs : List (Name, FC, NamedDef)
  lambdaLifted : List (Name, LiftedDef)
       -- ^ lambda lifted definitions, if required. Only the top level names
       -- will be in the context, and (for the moment...) I don't expect to
       -- need to look anything up, so it's just an alist.
  anf : List (Name, ANFDef)
       -- ^ lambda lifted and converted to ANF (all arguments to functions
       -- and constructors transformed to either variables or Null if erased)
  vmcode : List (Name, VMDef)
       -- ^ A much simplified virtual machine code, suitable for passing
       -- to a more low level target such as C

||| compile
||| Given a value of type Codegen, produce a standalone function
||| that executes the `compileExpr` method of the Codegen
export
compile : {auto c : Ref Ctxt Defs} ->
          Codegen ->
          ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile {c} cg tm out
    = do d <- getDirs
         let tmpDir = execBuildDir d
         let outputDir = outputDirWithDefault d
         ensureDirectoryExists tmpDir
         ensureDirectoryExists outputDir
         logTime "+ Code generation overall" $
             compileExpr cg c tmpDir outputDir tm out

||| execute
||| As with `compile`, produce a functon that executes
||| the `executeExpr` method of the given Codegen
export
execute : {auto c : Ref Ctxt Defs} ->
          Codegen -> ClosedTerm -> Core ()
execute {c} cg tm
    = do d <- getDirs
         let tmpDir = execBuildDir d
         ensureDirectoryExists tmpDir
         executeExpr cg c tmpDir tm
         pure ()

export
incCompile : {auto c : Ref Ctxt Defs} ->
             Codegen -> String -> Core (Maybe (String, List String))
incCompile {c} cg src
    = do let Just inc = incCompileFile cg
             | Nothing => pure Nothing
         inc c src

-- If an entry isn't already decoded, get the minimal entry we need for
-- compilation, and record the Binary so that we can put it back when we're
-- done (so that we don't obliterate the definition)
getMinimalDef : ContextEntry -> Core (GlobalDef, Maybe (Namespace, Binary))
getMinimalDef (Decoded def) = pure (def, Nothing)
getMinimalDef (Coded ns bin)
    = do b <- newRef Bin bin
         cdef <- fromBuf b
         refsRList <- fromBuf b
         let refsR = map fromList refsRList
         fc <- fromBuf b
         mul <- fromBuf b
         name <- fromBuf b
         let def
             = MkGlobalDef fc name (Erased fc False) [] [] [] [] mul
                           [] Public (MkTotality Unchecked IsCovering)
                           [] Nothing refsR False False True
                           None cdef []
         pure (def, Just (ns, bin))

-- ||| Recursively get all calls in a function definition
getAllDesc : {auto c : Ref Ctxt Defs} ->
             List Name -> -- calls to check
             IOArray (Int, Maybe (Namespace, Binary)) ->
                            -- which nodes have been visited. If the entry is
                            -- present, it's visited. Keep the binary entry, if
                            -- we partially decoded it, so that we can put back
                            -- the full definition later.
                            -- (We only need to decode the case tree IR, and
                            -- it's expensive to decode the whole thing)
             Defs -> Core ()
getAllDesc [] arr defs = pure ()
getAllDesc (n@(Resolved i) :: rest) arr defs
  = do Nothing <- coreLift $ readArray arr i
           | Just _ => getAllDesc rest arr defs
       case !(lookupContextEntry n (gamma defs)) of
            Nothing => getAllDesc rest arr defs
            Just (_, entry) =>
              do (def, bin) <- getMinimalDef entry
                 ignore $ addDef n def
                 let refs = refersToRuntime def
                 if multiplicity def /= erased
                    then do coreLift $ writeArray arr i (i, bin)
                            let refs = refersToRuntime def
                            refs' <- traverse toResolvedNames (keys refs)
                            getAllDesc (refs' ++ rest) arr defs
                    else getAllDesc rest arr defs
getAllDesc (n :: rest) arr defs
  = getAllDesc rest arr defs

warnIfHole : Name -> NamedDef -> Core ()
warnIfHole n (MkNmError _)
    = coreLift $ putStrLn $ "Warning: compiling hole " ++ show n
warnIfHole n _ = pure ()

getNamedDef :  {auto c : Ref Ctxt Defs}
            -> (Name,FC,CDef)
            -> Core (Name, FC, NamedDef)
getNamedDef (n,fc,cdef) =
  let ndef = forgetDef cdef
   in warnIfHole n ndef >> pure (n,fc,ndef)

replaceEntry : {auto c : Ref Ctxt Defs} ->
               (Int, Maybe (Namespace, Binary)) -> Core ()
replaceEntry (i, Nothing) = pure ()
replaceEntry (i, Just (ns, b))
    = ignore $ addContextEntry ns (Resolved i) b

natHackNames : List Name
natHackNames
    = [UN (Basic "prim__add_Integer"),
       UN (Basic "prim__sub_Integer"),
       UN (Basic "prim__mul_Integer"),
       NS typesNS (UN $ Basic "prim__integerToNat")]

-- Hmm, these dump functions are all very similar aren't they...
dumpCases : String -> List (Name,FC,NamedDef) -> Core ()
dumpCases fn defs
    = do Right () <- coreLift $ writeFile fn
                     (fastAppend $ map dumpCase defs)
               | Left err => throw (FileErr fn err)
         pure ()
  where
    fullShow : Name -> String
    fullShow (DN _ n) = show n
    fullShow n = show n

    dumpCase : (Name,FC,NamedDef) -> String
    dumpCase (n,_,def)
        = fullShow n ++ " = " ++ show def ++ "\n"

dumpLifted : String -> List (Name, LiftedDef) -> Core ()
dumpLifted fn lns
    = do let cstrs = map dumpDef lns
         Right () <- coreLift $ writeFile fn (fastAppend cstrs)
               | Left err => throw (FileErr fn err)
         pure ()
  where
    fullShow : Name -> String
    fullShow (DN _ n) = show n
    fullShow n = show n

    dumpDef : (Name, LiftedDef) -> String
    dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n"

dumpANF : String -> List (Name, ANFDef) -> Core ()
dumpANF fn lns
    = do let cstrs = map dumpDef lns
         Right () <- coreLift $ writeFile fn (fastAppend cstrs)
               | Left err => throw (FileErr fn err)
         pure ()
  where
    fullShow : Name -> String
    fullShow (DN _ n) = show n
    fullShow n = show n

    dumpDef : (Name, ANFDef) -> String
    dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n"

dumpVMCode : String -> List (Name, VMDef) -> Core ()
dumpVMCode fn lns
    = do let cstrs = map dumpDef lns
         Right () <- coreLift $ writeFile fn (fastAppend cstrs)
               | Left err => throw (FileErr fn err)
         pure ()
  where
    fullShow : Name -> String
    fullShow (DN _ n) = show n
    fullShow n = show n

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

export
nonErased : {auto c : Ref Ctxt Defs} ->
            Name -> Core Bool
nonErased n
    = do defs <- get Ctxt
         Just gdef <- lookupCtxtExact n (gamma defs)
              | Nothing => pure True
         pure (multiplicity gdef /= erased)

-- Find all the names which need compiling, from a given expression, and compile
-- them to CExp form (and update that in the Defs).
-- Return the names, the type tags, and a compiled version of the expression
export
getCompileData : {auto c : Ref Ctxt Defs} -> (doLazyAnnots : Bool) ->
                 UsePhase -> ClosedTerm -> Core CompileData
getCompileData doLazyAnnots phase_in tm_in
    = do defs <- get Ctxt
         sopts <- getSession
         let phase = foldl {t=List} (flip $ maybe id max) phase_in $
                         [Cases <$ dumpcases sopts, Lifted <$ dumplifted sopts, ANF <$ dumpanf sopts, VMCode <$ dumpvmcode sopts]
         let ns = getRefs (Resolved (-1)) tm_in
         tm <- toFullNames tm_in
         natHackNames' <- traverse toResolvedNames natHackNames
         -- make an array of Bools to hold which names we've found (quicker
         -- to check than a NameMap!)
         asize <- getNextEntry
         arr <- coreLift $ newArray asize
         logTime "++ Get names" $ getAllDesc (natHackNames' ++ keys ns) arr defs

         let entries = catMaybes !(coreLift (toList arr))
         let allNs = map (Resolved . fst) entries
         cns <- traverse toFullNames allNs

         -- Do a round of merging/arity fixing for any names which were
         -- unknown due to cyclic modules (i.e. declared in one, defined in
         -- another)
         rcns <- filterM nonErased cns
         logTime "++ Merge lambda" $ traverse_ mergeLamDef rcns
         logTime "++ Fix arity" $ traverse_ fixArityDef rcns
         compiledtm <- fixArityExp !(compileExp tm)

         (cseDefs, csetm) <- logTime "++ CSE" $ do
           um      <- analyzeNames rcns
           defs    <- catMaybes <$> traverse (cseDef um) rcns
           pure $ (cseNewToplevelDefs um ++ defs, adjust um compiledtm)

         namedDefs <- logTime "++ Forget names" $
           traverse getNamedDef cseDefs

         let mainname = MN "__mainExpression" 0
         (liftedtm, ldefs) <- liftBody {doLazyAnnots} mainname csetm

         lifted_in <- if phase >= Lifted
                         then logTime "++ Lambda lift" $
                              traverse (lambdaLift doLazyAnnots) cseDefs
                         else pure []

         let lifted = (mainname, MkLFun [] [] liftedtm) ::
                      ldefs ++ concat lifted_in

         anf <- if phase >= ANF
                   then logTime "++ Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
                   else pure []
         vmcode <- if phase >= VMCode
                      then logTime "++ Get VM Code" $ pure (allDefs anf)
                      else pure []

         defs <- get Ctxt
         whenJust (dumpcases sopts) $ \ f =>
            do coreLift $ putStrLn $ "Dumping case trees to " ++ f
               dumpCases f namedDefs

         whenJust (dumplifted sopts) $ \ f =>
            do coreLift $ putStrLn $ "Dumping lambda lifted defs to " ++ f
               dumpLifted f lifted

         whenJust (dumpanf sopts) $ \ f =>
            do coreLift $ putStrLn $ "Dumping ANF defs to " ++ f
               dumpANF f anf

         whenJust (dumpvmcode sopts) $ \ f =>
            do coreLift $ putStrLn $ "Dumping VM defs to " ++ f
               dumpVMCode f vmcode

         -- We're done with our minimal context now, so put it back the way
         -- it was. Back ends shouldn't look at the global context, because
         -- it'll have to decode the definitions again.
         traverse_ replaceEntry entries
         pure (MkCompileData csetm namedDefs lifted anf vmcode)

export
compileTerm : {auto c : Ref Ctxt Defs} ->
              ClosedTerm -> Core (CExp [])
compileTerm tm_in
    = do tm <- toFullNames tm_in
         fixArityExp !(compileExp tm)

export
getIncCompileData : {auto c : Ref Ctxt Defs} -> (doLazyAnnots : Bool) ->
                    UsePhase -> Core CompileData
getIncCompileData doLazyAnnots phase
    = do defs <- get Ctxt
         -- Compile all the names in 'toIR', since those are the ones defined
         -- in the current source file
         let ns = keys (toIR defs)
         cns <- traverse toFullNames ns
         rcns <- filterM nonErased cns
         cseDefs <- catMaybes <$> traverse (cseDef empty) rcns

         namedDefs <- traverse getNamedDef cseDefs

         lifted_in <- if phase >= Lifted
                         then logTime "++ Lambda lift" $
                              traverse (lambdaLift doLazyAnnots) cseDefs
                         else pure []
         let lifted = concat lifted_in
         anf <- if phase >= ANF
                   then logTime "++ Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
                   else pure []
         vmcode <- if phase >= VMCode
                      then logTime "++ Get VM Code" $ pure (allDefs anf)
                      else pure []
         pure (MkCompileData (CErased emptyFC) namedDefs lifted anf vmcode)

-- Some things missing from Prelude.File

||| check to see if a given file exists
export
exists : String -> IO Bool
exists f
    = do Right ok <- openFile f Read
             | Left err => pure False
         closeFile ok
         pure True
-- Select the most preferred target from an ordered list of choices and
-- parse the calling convention into a backend/target for the call, and
-- a comma separated list of any other location data. For example
-- the chez backend would supply ["scheme,chez", "scheme", "C"]. For a function with
-- more than one string, a string with "scheme" would be preferred over one
-- with "C" and "scheme,chez" would be preferred to both.
-- e.g. "scheme:display" - call the scheme function 'display'
--      "C:puts,libc,stdio.h" - call the C function 'puts' which is in
--      the library libc and the header stdio.h
-- Returns Nothing if there is no match.
export
parseCC : List String -> List String -> Maybe (String, List String)
parseCC [] _ = Nothing
parseCC (target::ts) strs = findTarget target strs <|> parseCC ts strs
  where
    getOpts : String -> List String
    getOpts "" = []
    getOpts str
        = case span (/= ',') str of
               (opt, "") => [opt]
               (opt, rest) => opt :: getOpts (assert_total (strTail rest))
    hasTarget : String -> String -> Bool
    hasTarget target str = case span (/= ':') str of
                            (targetSpec, _) => targetSpec == target
    findTarget : String -> List String -> Maybe (String, List String)
    findTarget target [] = Nothing
    findTarget target (s::xs) = if hasTarget target s
                                  then case span (/= ':') s of
                                        (t, "") => Just (trim t, [])
                                        (t, opts) => Just (trim t, map trim (getOpts
                                                                  (assert_total (strTail opts))))
                                  else findTarget target xs

export
dylib_suffix : String
dylib_suffix
    = cond [(os `elem` ["windows", "mingw32", "cygwin32"], "dll"),
            (os == "darwin", "dylib")]
           "so"

export
locate : {auto c : Ref Ctxt Defs} ->
         String -> Core (String, String)
locate libspec
    = do -- Attempt to turn libspec into an appropriate filename for the system
         let fname
              = case words libspec of
                     [] => ""
                     [fn] => if '.' `elem` unpack fn
                                then fn -- full filename given
                                else -- add system extension
                                     fn ++ "." ++ dylib_suffix
                     (fn :: ver :: _) =>
                          -- library and version given, build path name as
                          -- appropriate for the system
                          cond [(dylib_suffix == "dll",
                                      fn ++ "-" ++ ver ++ ".dll"),
                                (dylib_suffix == "dylib",
                                      fn ++ "." ++ ver ++ ".dylib")]
                                (fn ++ "." ++ dylib_suffix ++ "." ++ ver)

         fullname <- catch (findLibraryFile fname)
                           (\err => -- assume a system library so not
                                    -- in our library path
                                    pure fname)
         pure (fname, fullname)

export
copyLib : (String, String) -> Core ()
copyLib (lib, fullname)
    = if lib == fullname
         then pure ()
         else do Right bin <- coreLift $ readFromFile fullname
                    | Left err => pure () -- assume a system library installed globally
                 Right _ <- coreLift $ writeToFile lib bin
                    | Left err => throw (FileErr lib err)
                 pure ()

-- parses `--directive extraRuntime=/path/to/defs.scm` options for textual inclusion in generated
-- source. Use with `%foreign "scheme:..."` declarations to write runtime-specific scheme calls.
export
getExtraRuntime : List String -> Core String
getExtraRuntime directives
    = do fileContents <- traverse readPath paths
         pure $ concat $ intersperse "\n" fileContents
  where
    getArg : String -> Maybe String
    getArg directive =
      let (k,v) = break (== '=') directive
      in
        if (trim k) == "extraRuntime"
          then Just $ trim $ substr 1 (length v) v
          else Nothing

    paths : List String
    paths = nub $ mapMaybe getArg $ reverse directives

    readPath : String -> Core String
    readPath p = do
      Right contents <- coreLift $ readFile p
        | Left err => throw (FileErr p err)
      pure contents

||| Cast implementations. Values of `ConstantPrimitives` can
||| be used in a call to `castInt`, which then determines
||| the cast implementation based on the given pair of
||| constants.
public export
record ConstantPrimitives where
  constructor MkConstantPrimitives
  charToInt    : IntKind -> String -> Core String
  intToChar    : IntKind -> String -> Core String
  stringToInt  : IntKind -> String -> Core String
  intToString  : IntKind -> String -> Core String
  doubleToInt  : IntKind -> String -> Core String
  intToDouble  : IntKind -> String -> Core String
  intToInt     : IntKind -> IntKind -> String -> Core String

||| Implements casts from and to integral types by using
||| the implementations from the provided `ConstantPrimitives`.
export
castInt :  ConstantPrimitives
        -> Constant
        -> Constant
        -> String
        -> Core String
castInt p from to x =
  case ((from, intKind from), (to, intKind to)) of
       ((CharType, _)  , (_, Just k)) => p.charToInt k x
       ((StringType, _), (_, Just k)) => p.stringToInt k x
       ((DoubleType, _), (_, Just k)) => p.doubleToInt k x
       ((_, Just k), (CharType, _))   => p.intToChar k x
       ((_, Just k), (StringType, _)) => p.intToString k x
       ((_, Just k), (DoubleType, _)) => p.intToDouble k x
       ((_, Just k1), (_, Just k2))   => p.intToInt k1 k2 x
       _ => throw $ InternalError $ "invalid cast: + " ++ show from ++ " + ' -> ' + " ++ show to


text:
--    Copyright 2017, the blau.io contributors
--
--    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.

module API.Web.DOM.Node

import API.Web.DOM.Document
import API.Web.DOM.DocumentType
import API.Web.DOM.Element

%access public export
%default total

||| The original interface specification can be found at
||| https://dom.spec.whatwg.org/#interface-node
data Node : Type where
  FromDocument     : Document _   -> Node
  FromDocumentType : DocumentType -> Node
  FromElement      : Element      -> Node

ext: idr

max_stars_repo_name: blau-io/idris-web

max_issues_repo_name: pierrebeaucamp/idris-dom

max_forks_repo_name: pierrebeaucamp/idris-dom


text:
module DeepFund

tranche: Double -> Double
tranche t =  init * pow (1-incr) t where
  init : Double; init = 15000000
  incr: Double;  incr = 1.5/100

deepAGI: Double -> Double
deepAGI t = tranche t * frac where
  frac: Double; frac = 0.30

deepLockAGI: Double -> Double
deepSNetAGI t = deepAGI t * frac where
  frac: Double; frac = 0.25

deepUSD: (t: Double) -> (p: Double) -> Double
deepUSD t p = deepAGI t * p

max_stars_repo_name: nunet-io/snet-ai-dsl

max_issues_repo_name: nunet-io/snet-ai-dsl

max_forks_repo_name: nunet-io/snet-ai-dsl


text:
-- Perl-style pack/unpack

module Pack

-- core

-- inp - a parsing-oriented type, i.e. including bits count or similar
-- information; it's constructors should accept a final argument of
-- type out
-- out - a user-friendly type, e.g. Nat or String
class Packable inp out where
  total ppack : inp -> Maybe (List Bool)
  total punpack : List Bool -> Maybe (out, List Bool)

-- Verified Packable
data T = tt
class Packable i o => VerifiedPackable i o (f : o -> i) where
  total v1 : (outv : o) -> maybe T (\x => x = (outv, List.Nil {a=Bool})) (ppack (f outv) >>= punpack {inp=i} {out=o})

-- collecting all the types, user should only provide functions of
-- type (out -> inp), e.g. (mkpNat 3)
data Pack : Type -> Type -> Type where
  p : Packable i o => (o -> i) -> Pack i o
  (..) : Packable i o => (o -> i) -> Pack a b -> Pack (i, a) (o, b)

infixr 3 ..

-- actual pack
total mpack : Pack t1 t2 -> t2 -> Maybe (List Bool)
mpack (p tc) o = ppack (tc o)
mpack (tc .. pl) (v, vl) = do
  this <- ppack (tc v)
  rest <- mpack pl vl
  return $ this ++ rest

-- and unpack
total munpack : Pack t1 t2 -> List Bool -> Maybe t2
munpack (p tc) l = (punpack l) >>= Just . fst
munpack (tc .. pl) l = do
  (r, rest) <- punpack l
  next <- munpack pl rest
  return (r, next)

-- extensions

natToBits : Nat -> Nat -> List Bool
natToBits n Z = []
natToBits Z bits = replicate bits False
natToBits n (S bits) = natToBits (div n 2) bits ++ [ (mod n 2 /= Z) ]

bitsToNat : List Bool -> Nat -> Nat
bitsToNat l b = bitsToNat' (reverse l) b
  where bitsToNat' [] b = Z
        bitsToNat' l Z = Z
        bitsToNat' (v :: l) (S b) = (if v then 1 else 0) + 2 * bitsToNat' l b

-- Nat, BE

data pNat : Nat -> Type where
  mkpNat : (bits : Nat) -> Nat -> pNat bits

instance Packable (pNat n) Nat where
  ppack mn = case mn of
    (mkpNat n v) => if S (log2 v) <= n
                    then Just $ natToBits v n
                    else Nothing
  punpack l = if n <= length l
              then Just (bitsToNat (take n l) n, drop n l)
              else Nothing

-- Nat, LE

data pNatLe : Nat -> Type where
  mkpNatLe : (bits : Nat) -> Nat -> pNatLe bits

instance Packable (pNatLe n) Nat where
  ppack mn = case mn of
    (mkpNatLe n v) => if S (log2 v) <= n
                      then Just $ reverse $ natToBits v n
                      else Nothing
  punpack l = if n <= length l
              then Just (bitsToNat (reverse $ take n l) n, drop n l)
              else Nothing

-- Raw bits

data pBits : Nat -> Type where
  mkpBits : (bits : Nat) -> List Bool -> pBits bits

instance Packable (pBits n) (List Bool) where
  ppack bl = case bl of
    (mkpBits n l) => if length l == n
                     then Just $ l
                     else Nothing
  punpack l = if (length l == n) || (length l > n)
              then Just (take n l, drop n l)
              else Nothing

-- Verified pBits

total nat_eqb_eq : (x : Nat) -> (y : Nat) -> (x == y = True) -> (x = y)
nat_eqb_eq Z Z p = refl
nat_eqb_eq Z (S y) p = FalseElim (trueNotFalse (sym p))
nat_eqb_eq (S x) Z p = FalseElim (trueNotFalse (sym p))
nat_eqb_eq (S x) (S y) p = cong {f=S} (nat_eqb_eq x y p)

total take_len : (n : Nat) -> (l : List a) -> n = length l -> take n l = l
take_len Z [] p = refl
take_len Z (x :: xs) p = FalseElim (OnotS p)
take_len (S k) [] p = refl
take_len (S k) (x :: xs) p = cong {f=(x ::)} $ take_len k xs $ succInjective k (length xs) p

total drop_len : (n : Nat) -> (l : List a) -> n = length l -> drop n l = List.Nil {a=a}
drop_len Z [] p = refl
drop_len Z (x :: xs) p = FalseElim (OnotS p)
drop_len (S k) [] p = FalseElim (OnotS (sym p))
drop_len (S k) (x :: xs) p = drop_len k xs $ succInjective k (length xs) p

total pair : {A : Type} -> {B : Type} -> {a : A} -> {b : B} -> {c : A} -> {d : B} ->
  (a = c) -> (b = d) -> (a, b) = (c, d)
pair ac bd = rewrite ac in cong bd

data Inspect : a -> Type where
  wi : {A : Type} -> (x : A) -> (y : A) -> (eq: x = y) -> Inspect x

inspect : {A : Type} -> (x : A) -> Inspect x
inspect x = wi x _ refl

match : {A : Type} -> {x : A} -> (y : A) -> {eq : x = y} -> Inspect x
match y {eq} = wi _ y eq

instance VerifiedPackable (pBits n) (List Bool) (mkpBits n) where
  v1 [] = case n of
    Z => refl
    (S m) => tt
  v1 (x :: xs) with (inspect n)
    | match Z {eq} = rewrite eq in tt
    | match (S m) {eq} with (inspect (length xs == m))
      | match True {eq=eq1} = rewrite eq in (rewrite eq1 in cst_lemma)
        where sml : S m = length (x :: xs)
              sml = cong {f=S} $ sym (nat_eqb_eq (length xs) m eq1)
              cst_lemma2 : maybe T (\x2 => x2 = (x :: xs, List.Nil {a=Bool})) (Just (x :: (take m xs), drop m xs))
              cst_lemma2 = pair (take_len (S m) (x :: xs) sml)
                                (drop_len (S m) (x :: xs) sml)
              cst_lemma = rewrite eq1 in cst_lemma2
      | match False {eq=eq1} = rewrite eq in (rewrite eq1 in tt)

max_stars_repo_name: defanor/parcomb

max_issues_repo_name: defanor/parcomb

max_forks_repo_name: defanor/parcomb


text:
namespace Hoo

  f : Either a b -> Either b a
  f (Left a) = Right a
  f (Right b) = Left b

  natural : (xs : Either a b) -> ((f . f) . map g) xs === (map g . (f . f)) xs
  natural = ?l

mutual

  g : h === h
  g = Refl

  h : g === g
  h = Refl


text:
import System.File
import Data.String
import Data.List

main : IO ()
main = do
    putStrLn "input file: "
    file<-getLine
    Right tocheck<-readFile file
     | Left err => putStrLn $show err
    Right dict<-readFile "words"
     | Left err => putStrLn $show err
    let diff = filter (\s=>not $ s `elem` words dict) $ words tocheck
    putStrLn $ show diff


text:
import OCaml.IO
import OCaml.Lwt

%lib malfunction "duration"

Int64 : Type
Int64 = Ptr

of_sec : Int -> Int64
of_sec n =
  unsafePerformIO $ ocamlCall "Duration.of_sec" (Int -> OCaml_IO Int64) n

Hello : Module [val "sleep" (Int64 -> OCaml_IO (Lwt ()))] ->
        Module [val "start" (() -> OCaml_IO (Lwt ()))]
Hello time =
  struct [ Let "start" $ \() => loop 4 ]
  where
     loop : Int -> OCaml_IO (Lwt ())
     loop 0 = lwtReturn ()
     loop n = do
       print_endline "Idris Unikernel Hello!"
       lwtThread <- (time#"sleep") (of_sec 1)
       lwtThread `lwtBind` (\ () => loop $ n - 1)

exports : FFI_Export FFI_OCaml "idrikernel.mli" []
exports = Fun Hello "Hello" End

main : OCaml_IO ()
main = pure ()

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module Main

import Data.Vect

withFile : String -> (File -> IO (Either FileError a)) -> IO (Either FileError a)
withFile p cb = do
    Right f <- openFile p Read | Left e => pure (Left e)
    result <- cb f
    closeFile f
    pure result

parseLine : String -> List Int
parseLine = map cast . words

toVect : List a -> (n ** Vect n a)
toVect [] = (_ ** [])
toVect (x :: xs) =
    let (_ ** xsVect) = toVect xs
    in (_ ** x :: xsVect)

main : IO ()
main = do
    Right (xs, ys) <- withFile {a = (List Int, List Int)} "data.txt" $ \f => do
        Right xLine <- fGetLine f | Left e => pure (Left e)
        Right yLine <- fGetLine f | Left e => pure (Left e)
        pure (Right (parseLine xLine, parseLine yLine))
    | Left e => putStrLn ("FAILED: " ++ show e)

    let (xsLength ** xsVect) = toVect xs
    let (ysLength ** ysVect) = toVect ys

    case exactLength xsLength ysVect of
        Nothing => putStrLn "Vector lengths do not match"
        Just ysVect' => printLn (zipWith (+) xsVect ysVect')

max_stars_repo_name: rcook/read-vector

max_issues_repo_name: rcook/read-vector

max_forks_repo_name: rcook/read-vector


text:
module Test4

import TTUtils as T

%language ElabReflection

%default total

data In : (f : Type -> Type) -> Type where
  MkIn : In f

-- This step requires definitional type constructor injectivity and is
-- the source of the problem.
injIn : In z = In y -> z = y
injIn (Refl {A=Type} {x=_}) = Refl

injInTT : FnDesc
injInTT = %runElab (getTTForFn `{injIn})

-- P : Type -> Type
-- P v = (a : (Type -> Type) ** (In a = v, a v -> Void))

-- func1 : P (In P) -> Void
-- func1 (a ** (InAEqInP, AAppInPImpVoid)) =
--   let lem2 : (P (In P) -> Void) = -- replace {P=\ x => x (In P) -> Void} (injIn InAEqX) AXImpVoid
--     let e1 = (injIn InAEqInP)
--         lem3 = replace {P=\ x => x (In P) -> Void} (injIn InAEqInP) AAppInPImpVoid
--     in
--       ?xxx
--   in lem2 (P ** (Refl, lem2))

-- total -- for extra oumph!
-- lem2 : Void
-- lem2 =
--   let foo : P (In P) = (P ** (Refl, func1))
--   in func1 foo

-- bla : x = y -> y = x
-- bla Refl = Refl

-- -- lookupFunDefnExact
-- -- let z : FunDefn TT = DefineFun (NS (UN "injIn") ["ProveVoid"])
-- --              [MkFunClause (Bind (UN "x")
-- --               (PVar (Bind (UN "__pi_arg")
-- --                     (Pi (TType (UVar "./Learn/ProveVoid.idr" 84)) (TType (UVar "./Learn/ProveVoid.idr" 86)))
-- --                     (TType (UVar "./Learn/ProveVoid.idr" 87))))
-- --               (App (App (App (P Ref (NS (UN "injIn") ["ProveVoid"]) Erased) (P Bound (UN "x") Erased)) (P Bound (UN "x") Erased))
-- --                    (App (App (P (DCon 0 2) (UN "Refl") Erased) Erased) Erased)))
-- --               (Bind (UN "x")
-- --               (PVar (Bind (UN "__pi_arg")
-- --                     (Pi (TType (UVar "./Learn/ProveVoid.idr" 84)) (TType (UVar "./Learn/ProveVoid.idr" 86)))
-- --                     (TType (UVar "./Learn/ProveVoid.idr" 87))))
-- --               (App (App (P (DCon 0 2) (UN "Refl") Erased)
-- --                   (Bind (UN "__pi_arg1")
-- --                   (Pi (TType (UVar "./Learn/ProveVoid.idr" 97)) (TType (UVar "./Learn/ProveVoid.idr" 99)))
-- --                   (TType (UVar "./Learn/ProveVoid.idr" 100))))
-- --                    (P Bound (UN "x") Erased)))]

-- -- lookupTyExact
-- -- let z : (TTName, NameType, TT) = (NS (UN "injIn") ["ProveVoid"],
-- --           Ref,
-- --           Bind (UN "y")
-- --                (Pi (Bind (UN "__pi_arg") (Pi (TType (UVar "./ProveVoid.idr" 59)) (TType (UVar "./ProveVoid.idr" 61))) (TType (UVar "./ProveVoid.idr" 62)))
-- --              (TType (UVar "./ProveVoid.idr" 64)))
-- --                (Bind (UN "x")
-- --                (Pi (Bind (UN "__pi_arg") (Pi (TType (UVar "./ProveVoid.idr" 65)) (TType (UVar "./ProveVoid.idr" 67))) (TType (UVar "./ProveVoid.idr" 68)))
-- --              (TType (UVar "./ProveVoid.idr" 70)))
-- --                (Bind (UN "__pi_arg")
-- --                (Pi (App (App (App (App (P (TCon 7 4) (UN "=") Erased) (TType (UVar "./ProveVoid.idr" 71))) (TType (UVar "./ProveVoid.idr" 72)))
-- --                  (App (P (TCon 8 1) (NS (UN "In") ["ProveVoid"]) Erased) (V 0)))
-- --                   (App (P (TCon 8 1) (NS (UN "In") ["ProveVoid"]) Erased) (V 1)))
-- --                    (TType (UVar "./ProveVoid.idr" 73)))
-- --                (App (App (App (App (P (TCon 7 4) (UN "=") Erased)
-- --                        (Bind (UN "__pi_arg1")
-- --                        (Pi (TType (UVar "./ProveVoid.idr" 74)) (TType (UVar "./ProveVoid.idr" 76)))
-- --                        (TType (UVar "./ProveVoid.idr" 77))))
-- --                   (Bind (UN "__pi_arg1")
-- --                   (Pi (TType (UVar "./ProveVoid.idr" 79)) (TType (UVar "./ProveVoid.idr" 81)))
-- --                   (TType (UVar "./ProveVoid.idr" 82))))
-- --                    (V 1))
-- --               (V 2)))))

-- -- lookupFunDefnExact
-- -- let z : FunDefn TT = DefineFun (NS (UN "bla") ["ProveVoid"])
-- --              [MkFunClause (Bind (MN 504 "phTy")
-- --               (PVar (TType (UVar "./ProveVoid.idr" 268)))
-- --               (Bind (MN 505 "x")
-- --               (PVar (P Bound (MN 504 "phTy") Erased))
-- --               (App (App (App (App (P Ref (NS (UN "bla") ["ProveVoid"]) Erased) (P Bound (MN 504 "phTy") Erased)) (P Bound (MN 505 "x") Erased))
-- --                   (P Bound (MN 505 "x") Erased))
-- --                    (App (App (P (DCon 0 2) (UN "Refl") Erased) Erased) Erased))))
-- --               (Bind (MN 504 "phTy")
-- --               (PVar (TType (UVar "./ProveVoid.idr" 268)))
-- --               (Bind (MN 505 "x")
-- --               (PVar (P Bound (MN 504 "phTy") Erased))
-- --               (App (App (P (DCon 0 2) (UN "Refl") Erased) (P Bound (MN 504 "phTy") Erased)) (P Bound (MN 505 "x") Erased))))]

-- -- lookupTyExact
-- blaTyExact : (TTName, NameType, TT)
-- blaTyExact =
--   (NS (UN "bla") ["ProveVoid"],
--     Ref,
--     Bind (UN "phTy")
--       (Pi (TType (UVar "./ProveVoid.idr" 262)) (TType (UVar "./ProveVoid.idr" 264)))
--       (Bind (UN "x")
--         (Pi (V 0) (TType (UVar "./ProveVoid.idr" 265)))
--         (Bind (UN "y")
--           (Pi (V 1) (TType (UVar "./ProveVoid.idr" 266)))
--           (Bind (UN "__pi_arg")
--              (Pi (App (App (App (App (P (TCon 7 4) (UN "=") Erased) (V 2)) (V 2)) (V 1)) (V 0)) (TType (UVar "./ProveVoid.idr" 267)))
--              (App (App (App (App (P (TCon 7 4) (UN "=") Erased) (V 3)) (V 3)) (V 1)) (V 2))))))

-- fazoo : 3 = 4 -> Void
-- fazoo Refl impossible


text:
castRating : String -> List Double
castRating = map cast . words

getRatings : Nat -> IO (List String)
getRatings n = traverse id $ replicate n getLine

averageRating : List Double -> Double
averageRating xs = (sum xs) / (the Double $ cast $ List.length xs)

ratingQty : IO Nat
ratingQty = cast <$> getLine

selectRating : List Double -> Integer
selectRating = the Integer . cast . ceiling . foldl1 max

main : IO ()
main = do
  qty <- ratingQty
  ratings <- getRatings qty
  let bestRating = selectRating $ map (averageRating . castRating) ratings
  print bestRating


text:
module Bezout

import Data.Vect
import Data.Fin

{-Copied from Chinmaya's code. Gives quotient and remainder on divison-}
{-This just computes the qoutient and the remainder, but it doesn't prove that they indeed satisfy the conditions a = b*q + r and r < b -}
Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat)
Eucl Z b = (Z,Z)
Eucl (S k) b = case (lte (S (S k)) b) of
                    False => (S(fst(Eucl (minus (S k) b) b)), snd(Eucl (minus (S k) b) b))
                    True => (Z, S k)
{-Just a slight modification of the Euclid's division function to give the remainder -}
rem : (a : Nat) -> (b : Nat) -> Nat
rem Z b = Z
rem (S k) b = case (lte (S (S k)) b) of
                    False => (rem (minus (S k) b) b)
                    True => (S k)
{-Let rk be the remainder in the Euclidean algorithm at the k-2th step.
Let rk = ak*r0 + bk*r1 where r0 and r1 are the original inputs.Correspondingly  rsk = ask*r0 + bsk*r1 where sk = k+1
Then the I am going to the next step in the Euclid algorithm and changing the coefficients.
These formulas can be easily derived.-}
Euclnos: (Int,Int,Int,Int,Int,Int)->(Int,Int,Int,Int,Int,Int)
Euclnos (rk, rsk ,ak ,ask, bk ,bsk) = (rsk,rssk,ask,assk,bsk,bssk) where
  rssk = cast(snd (Eucl (cast rk) (cast rsk)))
  bssk =bk-bsk* (cast(fst (Eucl (cast rk) (cast rsk))))
  assk =ak-ask* (cast(fst (Eucl (cast rk) (cast rsk))))
{-Does the Euclnos repeatedy until the remainder is zero. Then the previous remainder is the GCD.-}
Bezouttuple: (Int,Int,Int,Int,Int,Int)->(Int,Int,Int,Int,Int,Int)
Bezouttuple (rk, rsk ,ak ,ask, bk, bsk) = case rsk of
                                        0 => (rk, rsk, ak, ask, bk, bsk)
                                        _ => (Bezouttuple (Euclnos (rk ,rsk, ak ,ask ,bk ,bsk)))
{-Returns 2 particular integers out of a 6 tuple-}
returnab: (Int,Int,Int,Int,Int,Int)->(Int,Int)
returnab (a ,b ,c ,d, e ,f)  = (c,e)
{-Returns the Bezout coefficients-}
Bezout : Nat ->Nat ->(Int, Int)
Bezout k j =  (returnab(Bezouttuple((cast k) , (cast j),1, 0 ,0 ,1)))

{-}
just the functions to compute the GCD in two different ways.
{-}

gcd2 : Nat -> Nat -> Nat
gcd2 a b = (cast (((cast a)*(snd (Bezout a b))) + ((cast b)*(fst (Bezout a b)))))

gcdab : Nat -> Nat -> Nat
gcdab b Z = b
gcdab a b = gcdab b (snd (Eucl a b))

{-}
given below are the auxilary functions to the proof that given a and b, there exist q and r such that a = b*q + r.
The algorithm above just computes these two numbers, but it doesn't prove that (a = b*q + r and r < b)

f1 is the proof that a + 1 = b*q + (r + 1) given that a = b*q + r

aux1f2 is the proof that given a + 1 <= b, a <= b
aux2f2 is the proof that given a and b, either a <= b or a >= b + 1

aux1f3 is the proof that given a <= b and b <= a, a = b
aux2f3 proves that a = b + c and c = d together imply a = b + d
aux3f3 is the proof that given a = b*c + b, a = b*(c + 1) + 0

All these proofs (except maybe aux2f3) were necessary to avoid various type mismatch errors.
{-}

apNat2 : (a : Nat) -> (b : Nat) -> (a = b) -> (S a = S b)
apNat2 a a Refl = Refl

aux1f2 : (a : Nat) -> (b : Nat) -> (LTE (S a) b) -> (LTE a b)
aux1f2 Z Z LTEZero impossible
aux1f2 Z Z (LTESucc _) impossible
aux1f2 Z (S k) x = LTEZero
aux1f2 (S a) (S k) (LTESucc x) = (LTESucc (aux1f2 a k x))

aux2f2 : (a : Nat) -> (b : Nat) -> (Either (LTE a b) (LTE (S b) a))
aux2f2 Z Z  = Left LTEZero
aux2f2 Z (S b) = Left LTEZero
aux2f2 (S k) Z = Right (LTESucc LTEZero)
aux2f2 (S k) (S b) = step where
                  step = case (aux2f2 k b) of
                    (Left l) => (Left (LTESucc l))
                    (Right r) => (Right (LTESucc r))

f1 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (a = b + c) -> ((S a) = b + (S c))
f1 a c k pf = (trans (apNat2 a (c + k) pf) (plusSuccRightSucc c k))

aux1f3 : (a : Nat) -> (b : Nat) -> (LTE a b) -> (LTE b a) -> (a = b)
aux1f3 Z Z LTEZero LTEZero = Refl
aux1f3 Z (S _) LTEZero LTEZero impossible
aux1f3 Z (S _) LTEZero (LTESucc _) impossible
aux1f3 (S _) Z LTEZero LTEZero impossible
aux1f3 (S _) Z (LTESucc _) LTEZero impossible
aux1f3 (S k) (S j) (LTESucc x) (LTESucc y) = (apNat2 k j (aux1f3 k j x y))

aux2f3 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (a = b + c) -> (c = d) -> (a = b + d)
aux2f3 a b Z Z prf Refl = prf
aux2f3 _ _ Z (S _) _ Refl impossible
aux2f3 _ _ (S _) Z _ Refl impossible
aux2f3 (b + (S j)) b (S j) (S j) Refl Refl = Refl

aux3f3 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (a = (b*c) + b) -> (a = b*(S c) + Z)
aux3f3 a b k prf = (trans (trans (trans (prf) (plusCommutative (b*k) b)) (sym (multRightSuccPlus b k))) (sym (plusZeroRightNeutral (b*(S k)))))

{-Caveat : the function elemproof hasn't been programmed for the divisor b being equal to zero -}
{-replacig b with (S b) everywhere in the proof has been done to avoid the case b = 0-}

elemproof1 : (a : Nat) -> (b : Nat) -> (x : (Nat, Nat) ** ((a = (b*(fst x)) + (snd x)) , (LTE (S (snd x)) b)))
elemproof1 Z (S b) = ((0,0) ** ((sym (trans (trans (plusCommutative ((S b)*Z) Z) (sym (multLeftSuccPlus (S b) Z))) (multZeroRightZero (S (S b))))), (LTESucc LTEZero)))
elemproof1 (S k) (S b) = step where
                     step = case (elemproof1 k (S b)) of
                       ((q,r) ** (pf , pff)) => case (aux2f2 (S (S r)) (S b)) of
                                                  Left l => ((q , (S r)) ** ((f1 k ((S b)*q) r pf) , l))
                                                  Right (LTESucc ri) => (((S q) , Z) ** ((aux3f3 (S k) (S b) q (aux2f3 (S k) ((S b)*q) (S r) (S b) (f1 k ((S b)*q) r pf) (aux1f3 (S r) (S b) pff ri))) , (LTESucc LTEZero)))

{-proof of existence of remainders and quotients is necessary to define the concept of divisibilty -}
{-The next step ahead might be to proof the uniqueness of these remainders and quotients probably -}

-- defining divisibilty as b | a if there exists q such that a = b*q + Z
-- if b | a and c | b, then c | a.
-- if c | a and c | b, then c | (a + b)

-- auxplusDiv 1 to 4 are just auxilary proofs.
auxtransDiv : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (b = c*q)
auxtransDiv a b c d = ?auxtransDiv_rhs

auxplusDiv1 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (a = b) -> (c = d) -> (a + c = b + d)
auxplusDiv1 b b d d Refl Refl = Refl

auxplusDiv2 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat) -> (p : Nat) -> (a = c*q) -> (b = c*p) -> (a + b = c*(q + p))
auxplusDiv2 a b c q p pf1 pf2 = (trans (auxplusDiv1 a (c*q) b (c*p) pf1 pf2) (sym(multDistributesOverPlusRight c q p)))

auxplusDiv3 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (a = c) -> (b = d) -> ((minus a b) = (minus c d))
auxplusDiv3 c d c d Refl Refl = Refl

-- Holes !!
auxplusDiv4 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat) -> (p : Nat) -> (a + b = c*q) -> (b = c*p) -> (a = c*(minus q p))
auxplusDiv4 a b c q p pf1 pf2 = ?auxplusDiv3_rhs

--These statements are the two main facts we might be interested in.
plusDiv1 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat ** a = c*q) -> (p : Nat ** b = c*p) -> (f : Nat ** a + b = c*f)
plusDiv1 a b c (q ** pf1) (p ** pf2) = ((q + p) ** (auxplusDiv2 a b c q p pf1 pf2))

plusDiv2 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat ** a + b = c*q) -> (p : Nat ** b = c*p) -> (f : Nat ** a = c*f)
plusDiv2 a b c (q ** pf1) (p ** pf2) = ((minus q p) ** (auxplusDiv4 a b c q p pf1 pf2))

-- I'll try and prove some (possibly useful) facts about the gcd.
-- weak definition of the gcd : d | a, d | b and if c | a and c | b, then c <= d.
--This is the common Factor Type

isCommonFactor : Nat -> Nat -> Nat -> Type
isCommonFactor a b c = ((q : Nat ** a = c*q),(p : Nat ** b = c*p))

--This is the GCD type
-- d is "a" gcd of a and b if isGCD a b d type is inhabited.
-- Uniqueness of GCD not assumed !!
-- the gcd is just assumed to be bigger than any other common divisor, not a multiple of it.

isGCD : Nat -> Nat -> Nat -> Type
isGCD a b d = ((isCommonFactor a b d) , ((c : Nat) -> (isCommonFactor a b c) -> (LTE c d)))

-- try to prove that if d is "a" gcd of (a,b) then it is "a" gcd of (a+b,a)

gcdfact1 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (isCommonFactor (a + b) b d)
gcdfact1 a b d (((q ** pf1),(p ** pf2)),f) = ((plusDiv1 a b d (q ** pf1) (p ** pf2)),(p ** pf2))

gcdfact2 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (c : Nat) -> (isCommonFactor (a + b) b c) -> (LTE c d)
gcdfact2 a b d (pf , f) c ((q ** pf1),(p ** pf2)) = (f c ((plusDiv2 a b c (q ** pf1) (p ** pf2)),(p ** pf2)))

maingcdfact1 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (isGCD (a + b) b d)
maingcdfact1 a b d pf = ((gcdfact1 a b d pf),(gcdfact2 a b d pf))

-- now the proof that if d is "a" gcd of (a+b,b), then it is "a" gcd of (a,b)

gcdfact3 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD (a + b) b d) -> (isCommonFactor a b d)
gcdfact3 a b d (((q ** pf1),(p ** pf2)),f) = ((plusDiv2 a b d (q ** pf1) (p ** pf2)),(p ** pf2))

gcdfact4 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD (a + b) b d) -> (c : Nat) -> (isCommonFactor a b c) -> (LTE c d)
gcdfact4 a b d (pf, f) c ((q ** pf1),(p ** pf2)) = (f c ((plusDiv1 a b c (q ** pf1) (p ** pf2)),(p ** pf2)))

maingcdFact2 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD (a + b) b d) -> (isGCD a b d)
maingcdFact2 a b d pf = ((gcdfact3 a b d pf),(gcdfact4 a b d pf))

-- now the proof that if d is "a" gcd of (a,b), it is also "a" gcd of (b,a)

symCommonFactor : (a : Nat) -> (b : Nat) -> (c : Nat) -> (isCommonFactor a b c) -> (isCommonFactor b a c)
symCommonFactor a b c ((p ** pf1),(q ** pf2)) = ((q ** pf2),(p ** pf1))

symGCD1 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> ((c : Nat) -> (isCommonFactor b a c) -> (LTE c d))
symGCD1 a b d (pf, f) = g where
                          g c ((p ** pf1),(q ** pf2)) = f c ((q ** pf2),(p ** pf1))

symGCD : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (isGCD b a d)
symGCD a b d (pf , f) = ((symCommonFactor a b d pf) , (symGCD1 a b d (pf , f)))

-- I'll list the types and functions that might be useful
-- The GCD type : isGCD : Nat -> Nat -> Nat -> Type
--                isGCD a b d = ((isCommonFactor a b d) , ((c : Nat) -> (isCommonFactor a b c) -> (LTE c d)))
-- maingcdfact1 , maingcdfact2 , symGCD.

-- The next step might be to show that the natural number that the euclidian algorithm gives us is indeed a gcd
-- also uniqueness of gcd.


text:
||| Implementing `Decidable.Order.Strict` for `Data.Nat.LT`
module Data.Nat.Order.Strict

import Decidable.Order
import Decidable.Order.Strict
import Decidable.Equality
import Data.Nat
import Data.Nat.Order

export
irreflexiveLTE : (a : Nat) -> Not (a `LT` a)
irreflexiveLTE 0     z_lt_z impossible
irreflexiveLTE (S a) (LTESucc a_lt_a) = irreflexiveLTE a a_lt_a

export
StrictPreorder Nat LT where
  irreflexive = irreflexiveLTE
  transitive a b c a_lt_b b_lt_c = transitive {po = LTE} (S a) b c
                                             a_lt_b
                                             (transitive {po = LTE} b (S b) c
                                                (lteSuccRight (reflexive b))
                                                b_lt_c)

public export
decLT : (a, b : Nat) -> DecOrdering {lt = LT} a b
decLT 0       0   = DecEQ Refl
decLT 0     (S b) = DecLT (LTESucc LTEZero)
decLT (S a)  0    = DecGT (LTESucc LTEZero)
decLT (S a) (S b) = case decLT a b of
  DecLT a_lt_b => DecLT (LTESucc a_lt_b)
  DecEQ Refl   => DecEQ Refl
  DecGT b_lt_a => DecGT (LTESucc b_lt_a)

public export
StrictOrdered Nat LT where
  order = decLT

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
--    Copyright 2017, the blau.io contributors
--
--    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.

module API.Web.HTML.HTMLCanvasElement

import API.WebGL.Context
import IdrisScript

%access public export
%default total

data RenderingContext : Type where
  FromWebGLRenderingContext : WebGLRenderingContext -> RenderingContext

||| The HTMLCanvasElement provides scripts with a resolution-dependent bitmap
||| canvas, which can be used for rendering graphs, game graphics, art, or other
||| visual images on the fly.
|||
||| The original specification can be found at
||| https://html.spec.whatwg.org/#the-canvas-element
record HTMLCanvasElement where
  constructor New
  width, height : Int
  localName     : String
  ||| self is a non standard field which is used to facilitate integration with
  ||| JavaScript
  self : Ptr

getContext : HTMLCanvasElement -> String -> JS_IO $ Maybe RenderingContext
getContext (New _ _ _ self) ctxId = let
    ref = jscall "%0.getContext(%1)" (JSRef -> String -> JS_IO JSRef) self ctxId
  in
    -- TODO: This would be a good use for dependent types
    case ctxId of
      "webgl" => case !(webGlRenderingContextFromPointer !ref) of
        Nothing        => pure Nothing
        (Just context) => pure $ Just $ FromWebGLRenderingContext context
      _       => pure Nothing

||| htmlCanvasElementFromPointer is a helper function for easily creating
||| HTMLCanvasElements from JavaScript references.
|||
||| @ ref A pointer to an HTMLCanvasElement.
htmlCanvasElementFromPointer : (ref : JSRef) -> JS_IO $ Maybe HTMLCanvasElement
htmlCanvasElementFromPointer ref = case !maybeLocalName of
    Nothing          => pure Nothing
    (Just localName) => case !maybeWidth of
      Nothing      => pure Nothing
      (Just width) => case !maybeHeight of
        Nothing       => pure Nothing
        (Just height) => pure $ Just $ New width height localName ref
  where
    maybeLocalName : JS_IO $ Maybe String
    maybeLocalName = let
        getLocalName = jscall "%0.localName" (JSRef -> JS_IO JSRef) ref
      in
        case !(IdrisScript.pack !getLocalName) of
             (JSString ** str) => pure $ Just $ fromJS str
             _                 => pure Nothing

    maybeWidth : JS_IO $ Maybe Int
    maybeWidth = let
        getWidth = jscall "%0.width" (JSRef -> JS_IO JSRef) ref
      in
        case !(IdrisScript.pack !getWidth) of
             (JSNumber ** num) => pure $ Just $ fromJS num
             _                 => pure Nothing

    maybeHeight : JS_IO $ Maybe Int
    maybeHeight = let
        getHeight = jscall "%0.height" (JSRef -> JS_IO JSRef) ref
      in
        case !(IdrisScript.pack !getHeight) of
             (JSNumber ** num) => pure $ Just $ fromJS num
             _                 => pure Nothing

max_stars_repo_name: blau-io/idris-html

max_issues_repo_name: blau-io/idris-html

max_forks_repo_name: blau-io/idris-html


text:
module Flutter

import public Dart.FFI.Constructors
import public Dart.FFI.Types
import public Flutter.FFI
import public Flutter.Widgets.Functions
import public Flutter.Widgets.Stateful
import public Flutter.Widgets.Stateless
import public Flutter.Widgets.Painter


text:
-- Local Variables:
-- idris-load-packages: ("prelude" "effects" "contrib" "base")
-- End:

import Data.Vect
import Data.Fin

-- https://en.wikipedia.org/wiki/Netpbm_format
-- A little file for writing PPM format. Why? Because I want to do some little image things
-- in Idris like the ones in the class I helped with using that Haskell library

preamble : Nat -> Nat -> String
preamble x y = unlines ["P3",show x ++ " " ++ show y]

PPM : Nat -> Nat -> Type
PPM x y = Vect y (Vect x (Int,Int,Int))

auxFun : (Int,Int,Int) -> String
auxFun (r,g,b) = (show r) ++ " " ++ (show g) ++ " " ++ (show b)

unwordsV : Vect x String -> String
unwordsV [] = ""
unwordsV (x :: xs) = x ++ " " ++ (unwordsV xs)

unlinesV : Vect x String -> String
unlinesV [] = ""
unlinesV (x :: xs) = x ++ "\n" ++ (unlinesV xs)

ppmToString : PPM x y -> String
ppmToString p = unlinesV $ map (unwordsV . map auxFun) p

ppmToFile : PPM x y -> String -> IO (Either FileError ())
ppmToFile p file = writeFile file (ppmToString p)

-- so we'll do the same thing as the original Haskell code I saw and have a function from doubles
-- to colors and then, being given dimensions to render, create an actual PPM type
coords : Double -> Double -> Double -> Double -> (xsample : Nat) -> (ysample : Nat) -> Vect ysample (Vect xsample (Double, Double))
coords x y delx dely xsample Z = []
coords x y delx dely xsample (S k) = (?createRow (S k))

funToVector : (Double -> Double -> (Int,Int,Int)) -> Double -> Double -> Double -> Double -> (xsample : Nat) -> (ysample : Nat) -> PPM xsample ysample
funToVector f startx starty delx dely xsample ysample = map (map (uncurry f)) (coords startx starty delx dely xsample ysample)

max_stars_repo_name: clarissalittler/idris-practice

max_issues_repo_name: clarissalittler/idris-practice

max_forks_repo_name: clarissalittler/idris-practice


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

%name Vect xs, ys, zs

data Elem : a -> Vect k a -> Type where
  Here : Elem x (x :: xs)
  There : (later : Elem x xs) -> Elem x (y :: xs)

notInNil : Elem value [] -> Void
notInNil Here impossible
notInNil (There _) impossible

notInTail : (notHere : (value = x) -> Void) -> (notThere : Elem value xs -> Void) -> Elem value (x :: xs) -> Void
notInTail notHere notThere Here = notHere Refl
notInTail notHere notThere (There later) = notThere later

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = No notInNil
isElem value (x :: xs) = case decEq value x of
                              (Yes Refl) => Yes Here
                              (No notHere) => (case isElem value xs of
                                                    (Yes prf) => Yes (There prf)
                                                    (No notThere) => No (notInTail notHere notThere))

elem : Eq ty => (value : ty) -> (xs : Vect n ty) -> Bool
elem value [] = False
elem value (x :: xs) = case value == x of
                            False => elem value xs
                            True => True


text:
module Main

import Effects
import Effect.StdIO
import Effect.Exception
import Effect.State

import Light
import Types

until_ : (pred : String -> Bool)
         -> (prompt : Eff String [STDIO])
         -> (action : String -> Eff () [STATE Env, STDIO, EXCEPTION Error])
         -> (Eff () [STATE Env, STDIO, EXCEPTION Error])
until_ pred prompt action = do
                              result <- prompt
                              if pred result
                                then pure ()
                                else do action result
                                        until_ pred prompt action

-- prints out a prompt and reads in a line of input
readPrompt : String -> Eff String [STDIO]
readPrompt prompt = do putStr prompt
                       getStr

-- todo: catch errors
evalString : String -> Eff String [STATE Env, EXCEPTION Error]
evalString expr = pure $ show !(evaluate expr)

-- lose states
-- evalAndPrint : String -> Eff () [STATE Env, STDIO, EXCEPTION Error]
-- evalAndPrint expr =  do case run (evalString expr) of
--                              Left e => putStrLn $ show e
--                              Right s => putStrLn s

evalAndPrint : String -> Eff () [STATE Env, STDIO, EXCEPTION Error]
evalAndPrint expr =  do s <- evalString expr
                        putStrLn s

runRepl : Eff () [STATE Env, STDIO, EXCEPTION Error]
runRepl = until_ (== "quit") (readPrompt "Lisp>>> ") evalAndPrint

go : List String -> IO ()
go [_] = run runRepl
go [_, expr] = run $ evalAndPrint expr
go _ = do putStrLn "Program takes only 0 or 1 argument"

main : IO ()
main = do args <- getArgs
          go args


text:
> module Subset.Operations

> import Data.Fin
> import Data.Vect
> import Control.Isomorphism

> import Sigma.Sigma
> import Pairs.Operations
> import Finite.Predicates
> import Decidable.Predicates
> import Finite.Operations
> import Vect.Operations

> %default total

> %access public export

> |||
> outl : {A : Type} -> {P : A -> Type} -> Subset A P -> A
> outl = getWitness

> |||
> outr : {A : Type} -> {P : A -> Type} -> (s : Subset A P) -> P (outl s)
> outr = getProof

> ||| Maps a finite type |A| and a decidable predicate |P| to a vector |Subset A P| values
> toVectSubset : {A : Type} ->
>                {P : A -> Type} ->
>                Finite A ->
>                Dec1 P ->
>                Sigma Nat (\ n => Vect n (Subset A P))
> toVectSubset fA d1P = filterTagSubset d1P (toVect fA)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
{- Process-based concurrency effect. -}
module Effect.Process
import System.Concurrency.Raw
import Effects
import Effect.State
import Effect.StdIO

%access public

-- Type of a channel, parameterised over message type. Ptr is the VM Ptr
data ProcPID msg = MkPPid Ptr

mutual
  data Running : Type -> Type where
    MkProc : Running mty

  {- Type of a running process, including message type, execution context,
     input and output effects. -}
  RunningProcessM : (mTy : Type) ->
                   List EFFECT ->
                   List EFFECT ->
                   Type
  RunningProcessM mty effs effs' =
    Eff () ((PROCESS (Running mty)) :: effs)
             (\_ => (PROCESS (Running mty)) :: effs')

  {- RunningProcessM but with the same input and output effects -}
  RunningProcess : (mTy : Type) ->
                   List EFFECT ->
                   Type
  RunningProcess mty effs = RunningProcessM mty effs effs

  data Process : Effect where
    Spawn : (mty : Type) ->
            RunningProcessM mty effs effs' ->
            Env IO effs ->
            { (Running mty') } Process (ProcPID mty)

    -- Returns true if there's a message waiting in this process' mailbox,
    -- false if not
    HasMessageWaiting : { (Running mty) } Process Bool

    -- Sends a message to a given process
    SendMessage : ProcPID mty -> mty -> { (Running mty) } Process ()

    -- Receives a message from a given process
    RecvMessage : { (Running mty) } Process mty

    RecvMessageAddr : { (Running mty) } Process (ProcPID mty, mty)

    -- Gets local PID
    GetID : { (Running mty) } Process (ProcPID mty)

   PROCESS : Type -> EFFECT
   PROCESS t = MkEff t Process

-- Spawns a new thread using the given message type, thread, and environment
spawn : (mty : Type) ->
        RunningProcessM mty effs effs' ->
        Env IO effs ->
        { [PROCESS (Running mty')] } Eff (ProcPID mty)
spawn ty proc env = call $ Spawn ty proc env

-- Checks whether a message has been received
hasMessage : { [PROCESS (Running mty)] } Eff Bool
hasMessage = call HasMessageWaiting

-- Sends a message
sendMessage : ProcPID mty -> mty -> { [PROCESS (Running mty)] } Eff ()
sendMessage pid msg = call $ SendMessage pid msg

-- Receives a message
recvMessage : { [PROCESS (Running mty)] } Eff mty
recvMessage = call RecvMessage

-- Receives a message, returning the PID of the sending process
recvMessageAddr : { [PROCESS (Running mty)] } Eff (ProcPID mty, mty)
recvMessageAddr = call RecvMessageAddr

-- Returns the local PID
getPID : { [PROCESS (Running mty)] } Eff (ProcPID mty)
getPID = call GetID

-- Type synonym for constructing instances
initProcess : Running mty
initProcess = MkProc

private
getInternal : Running mty -> IO (Ptr, mty)
getInternal x = getMsg

instance Handler Process IO where
  handle MkProc (Spawn ty proc env) k = do
    ptr <- fork (runInit (MkProc :: env) proc)
    k (MkPPid ptr) MkProc

  handle MkProc GetID k =
    k (MkPPid prim__vm) MkProc

  handle MkProc HasMessageWaiting k = do
    res <- checkMsgs
    k res MkProc

  handle MkProg (SendMessage (MkPPid pid) msg) k = do
    sendToThread pid (prim__vm, msg)
    k () MkProc

  handle x RecvMessage k = do
    (_, msg) <- getInternal x
    k msg x

  handle x RecvMessageAddr k = do
    (pid, msg) <- getInternal x
    k (MkPPid pid, msg) x


text:
module DepSec.File

import public DepSec.DIO
import public DepSec.Labeled

%access export

||| Secure file
data SecFile : {label : Type} -> (l : label) -> Type where
  ||| TCB
  MkSecFile : (path : String) -> SecFile l

||| Make a secure file from string
||| TCB
||| @ path path to file
makeFile : (path : String) -> SecFile l
makeFile = MkSecFile

||| Read a secure file
||| @ flow evidence that l may flow to l'
||| @ file secure file to read
readFile : Poset labelType
        => {l,l' : labelType}
        -> {auto flow : l `leq` l'}
        -> (file : SecFile l')
        -> DIO l (Labeled l' (Either FileError String))
readFile (MkSecFile path) = lift $ map MkLabeled $ readFile path

||| Write to a secure file
||| @ file secure file to write to
||| @ flow evidence that l may flow to l'
||| @ flow' evidence that l' may flow to l''
||| @ content labeled content to write
writeFile : Poset labelType
         => {l,l',l'' : labelType}
         -> {auto flow : l `leq` l'}
         -> (file : SecFile l'')
         -> {auto flow' : l' `leq` l''}
         -> (content : Labeled l' String)
         -> DIO l (Labeled l'' (Either FileError ()))
writeFile (MkSecFile path) (MkLabeled content)
  = lift $ map MkLabeled $ writeFile path content

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module IdrisScript.Date.Months

%access public export

data Month = January
           | February
           | March
           | April
           | May
           | June
           | July
           | August
           | September
           | October
           | November
           | December

implementation Eq Month where
  January   == January   = True
  February  == February  = True
  March     == March     = True
  April     == April     = True
  May       == May       = True
  June      == June      = True
  July      == July      = True
  August    == August    = True
  September == September = True
  October   == October   = True
  November  == November  = True
  December  == December  = True
  _         == _         = False

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module LastSeen

public export
record LastSeen where
  constructor CreateLastSeen
  time : Integer
  platform : Integer

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
module ExactLengthDec

import Data.Vect
import Decidable.Equality

%default total

{-
  interface DecEq ty where
    decEq : (val1 : ty) -> (val2 : ty) -> Dec (val1 = val2)

  data Dec: (prop : Type) -> Type where
    Yes : (prf : prop) -> Dec prop
    No : (contra : prop -> Void) -> Dec prop
-}

exactLength : { m : _ } -> (len : Nat) -> Vect m a -> Maybe (Vect len a)
exactLength len input = case decEq m len of
                          Yes Refl => Just input
                          No contra => Nothing

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Salo

import Salo.Language.Lexer
import Salo.Language.Parser

import Text.Lexer

main : IO ()
main = do putStrLn "Hello, world!"
          putStrLn "(You were probably looking for `nix run .#test`)"

max_stars_repo_name: semissioncontrol/semcos

max_issues_repo_name: semissioncontrol/semcos

max_forks_repo_name: semissioncontrol/semcos


text:
import Channel
import System.Concurrency.Channels

otherThreadProg : Channel (List String) -> IO ()
otherThreadProg chan = do Just state <- read chan | Nothing => putStrLn "Something went wrong 3"
                          write chan ("1234" :: state)
                          Just updatedState <- readOnly chan | Nothing => putStrLn "Something went wrong2"
                          putStrLn $ "Other thread : " ++ (show updatedState)

main : IO ()
main = do chan <- makeChan
          spawn (otherThreadProg chan)
          Just state <- read chan | Nothing => putStrLn "Something went wrong"
        --   input <- getLine
          write chan ("123" :: state)
          Just updatedState <- readOnly chan | Nothing => putStrLn "Something went wrong2"
          putStrLn $ "Main thread : " ++ (show updatedState)

max_stars_repo_name: AsmusAB/Idris-peer-to-peer-network

max_issues_repo_name: AsmusAB/Idris-peer-to-peer-network

max_forks_repo_name: AsmusAB/Idris-peer-to-peer-network


text:
module LightClick.DSL.Lexer

import Text.Lexer

import Toolkit.Text.Lexer.Run

%default total

symbols : List String
symbols = ["->", "-", "[", "]", ";", "{", "}", ":", ",", "=", "?", "(", ")", ".", "#", "!", "&", "|", "+"]

keywords : List String
keywords = [ "input", "output", "inout"
           , "high", "low", "rising", "falling", "insensitive"
           , "control", "clock", "data", "address", "reset", "info", "interrupt", "general"
           , "types", "modules", "connections", "module"
           , "logic", "typedef", "struct", "union", "lightclick", "model", "verilog"
           ]

public export
data Identifier = MkIdentifier String

export
Eq Identifier where
  (==) (MkIdentifier x) (MkIdentifier y) = x == y

namespace LightClick
  public export
  data Token = ID String
               | Keyword String
               | LineComment String
               | BlockComment String
               | Documentation String
               | LitNat Nat
               | LitStr String
               | Symbol String
               | WS String
               | NotRecognised String
               | EndInput

  export
  Eq Token where
    (==) (ID x) (ID y) = x == y
    (==) (LineComment x) (LineComment y) = x == y
    (==) (BlockComment x) (BlockComment y) = x == y
    (==) (Keyword x) (Keyword y) = x == y
    (==) (LitNat x) (LitNat y) = x == y
    (==) (LitStr x) (LitStr y) = x == y
    (==) (Symbol x) (Symbol y) = x == y
    (==) (WS x) (WS y) = x == y
    (==) (NotRecognised x) (NotRecognised y) = x == y
    (==) EndInput EndInput = True
    (==) _ _ = False

  showToken : Show a => String -> a -> String
  showToken n a = "(" <+> n <+> " " <+> show a <+> ")"

  export
  Show Token where
    show (ID id)             = showToken "ID" id
    show (Keyword str)       = showToken "Keyword" str
    show (LineComment str)   = showToken "LineComment" str
    show (BlockComment str)  = showToken "BlockComment" str
    show (Documentation str) = showToken "Documentation" str

    show (LitNat n) = showToken "Nat" n
    show (LitStr s) = showToken "Str" s

    show (Symbol s) = showToken "Symbol" s
    show (WS ws) = "WS"
    show (NotRecognised s) = showToken "Urgh" s
    show EndInput          = "EndInput"

  identifier : Lexer
  identifier = pred startIdent <+> many (pred validIdent)
    where
      startIdent : Char -> Bool
      startIdent x = isAlpha x

      validIdent : Char -> Bool
      validIdent '_' = True
      validIdent x = isAlphaNum x

  export
  tokenMap : TokenMap LightClick.Token
  tokenMap = with List
    [
      (space, WS)
    , (lineComment (exact "//"), LineComment)
    , (blockComment (exact "/*") (exact "*/"), BlockComment)
    , (lineComment (exact "\\\\"), Documentation)
    , (digits, \x => LitNat (integerToNat $ cast {to=Integer} x))
    , (stringLit, LitStr)
    ]
    ++
       map (\x => (exact x, Symbol)) symbols
    ++
    [
      (identifier, (\x => if elem x keywords then Keyword x else ID x))
    , (any, NotRecognised)
    ]

keep : WithBounds LightClick.Token -> Bool
keep (MkBounded t _ _)
  = case t of
      BlockComment _ => False
      LineComment  _ => False
      WS           _ => False
      _              => True

export
LightClickLexer : Lexer Token
LightClickLexer = MkLexer LightClick.tokenMap (keep) EndInput

export
lexClickStr : String -> Either LexError (List (WithBounds Token))
lexClickStr = lexString LightClickLexer

export
lexClickFile : String -> IO $ Either LexFail (List (WithBounds Token))
lexClickFile = lexFile LightClickLexer

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Main

import System
import System.Concurrency

main : IO ()
main = do
    chan <- makeChannel
    threadID <- fork $ do
        channelPut chan "Hello"
        channelPut chan "Goodbye"
    val <- channelGet chan
    putStrLn val
    val <- channelGet chan
    putStrLn val
    sleep 1


text:
module Main

import Erlang

erlPrintLn : ErlType a => a -> IO ()
erlPrintLn x = do
  pure $ erlUnsafeCall ErlTerm "io" "format" ["~p~n", the (List _) [x]]
  pure ()

intTest : IO ()
intTest = do
  putStrLn "intTest"
  erlPrintLn (the Int 0)
  erlPrintLn (the Int (-42))
  erlPrintLn (the Int 42)

integerTest : IO ()
integerTest = do
  putStrLn "integerTest"
  erlPrintLn (the Integer 0)
  erlPrintLn (the Integer (-42))
  erlPrintLn (the Integer 42)

stringTest : IO ()
stringTest = do
  putStrLn "stringTest"
  erlPrintLn ""
  erlPrintLn "test"
  erlPrintLn ("a" ++ "b")

charTest : IO ()
charTest = do
  putStrLn "charTest"
  erlPrintLn 'a'
  erlPrintLn '\n'

doubleTest : IO ()
doubleTest = do
  putStrLn "doubleTest"
  erlPrintLn 0.1
  erlPrintLn (-42.2)
  erlPrintLn 42.3

listTest : IO ()
listTest = do
  putStrLn "listTest"
  erlPrintLn (the (List String) [])
  erlPrintLn (the (List _) ["a", "b", "c"])

-- Skips function calls, (Raw a), ErlTerm for now

erlAtomTest : IO ()
erlAtomTest = do
  putStrLn "erlAtomTest"
  erlPrintLn (MkAtom "") -- Surprisingly, this is allowed
  erlPrintLn (MkAtom "ok")
  erlPrintLn (MkAtom ("a" ++ show 42))

erlCharlistTest : IO ()
erlCharlistTest = do
  putStrLn "erlCharlistTest"
  erlPrintLn (MkCharlist "")
  erlPrintLn (MkCharlist "ok")
  erlPrintLn (MkCharlist ("a" ++ show 42))

erlNilTest : IO ()
erlNilTest = do
  putStrLn "erlNilTest"
  erlPrintLn (the ErlNil [])

erlConsTest : IO ()
erlConsTest = do
  putStrLn "erlConsTest"
  erlPrintLn (the (ErlCons Integer Integer) (1 :: 2))
  erlPrintLn (the (ErlCons Integer String) (1 :: "a"))
  erlPrintLn (the (ErlCons Integer ErlNil) [1])
  erlPrintLn (the (ErlCons Integer (ErlCons Integer ErlNil)) [1, 2])

erlListTest : IO ()
erlListTest = do
  putStrLn "erlListTest"
  erlPrintLn (the (ErlList []) [])
  erlPrintLn (the (ErlList _) ["a", the Int 10, 'c'])

erlTuplesTest : IO ()
erlTuplesTest = do
  putStrLn "erlTuplesTest"
  erlPrintLn MkTuple0
  erlPrintLn (MkTuple1 "a")
  erlPrintLn (MkTuple2 "a" "b")
  erlPrintLn (MkTuple3 "a" "b" "c")
  erlPrintLn (MkTuple4 "a" "b" "c" "d")
  erlPrintLn (MkTuple5 "a" "b" "c" "d" "e")

main : IO ()
main = do
  intTest
  integerTest
  stringTest
  charTest
  doubleTest
  listTest
  erlAtomTest
  erlCharlistTest
  erlNilTest
  erlConsTest
  erlListTest
  erlTuplesTest


text:
module Gspider.Core

import Types.RestrictedCharString

%access private

||| Represents a system as a list of supported password characters.
public export
System : Type -- System is a type alias for a character list.
System = List Char

||| Represents a password probability distribution for a system.
|||
||| @s the system
public export
Distribution : (s : System) -> Type
Distribution s = (RestrictedCharString s) -> Double

max_stars_repo_name: sr-lab/gspider

max_issues_repo_name: sr-lab/gspider

max_forks_repo_name: sr-lab/gspider


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: CC0-1.0

module Parser

import Tester
import Control.ANSI

import Text.Lexer

import Language.TOML
import Language.TOML.Tokens
import Language.TOML.Parser as P
import Language.TOML.Lexer as L
import Language.TOML.ConcreteSyntax
import Language.TOML.Value

parseToItems : String -> TestFunc (List Item)
parseToItems src = do
    Just toks <- pure $ L.lexTOML src
        | Nothing => throw "lexing failed"
    Right items <- pure $ P.parseItems toks
        | Left err => throw (show (colored Red "parsing failed: ") ++ err)
    pure items

parse : String -> TestFunc Table
parse src = do
    Right table <- pure $ parseTOML src
        | Left err => throw (show err)
    pure table

namespace Concrete
    export
    kvNoNewline : Test
    kvNoNewline = test "parse key-value no newline" $ do
        items <- parseToItems "x = 12"
        assertEq (show items) "[keyval: x = 12]"

    export
    kvComment : Test
    kvComment = test "parse key-value with comment" $ do
        items <- parseToItems "x = 12 # this is a key value pair"
        assertEq (show items) "[keyval: x = 12]"

    export
    kvNewline : Test
    kvNewline = test "parse key-value with newline" $ do
        items <- parseToItems "x = 12\n"
        assertEq (show items) "[keyval: x = 12]"

    export
    tableHeader : Test
    tableHeader = test "parse table header" $ do
        items <- parseToItems "[package]"
        assertEq (show items) "[table: package]"

    export
    tableHeaderDotted : Test
    tableHeaderDotted = test "parse table header with dotted key" $ do
        items <- parseToItems "[dependencies.test]"
        assertEq (show items) "[table: dependencies.test]"

    export
    tableArray : Test
    tableArray = test "parse table array header" $ do
        items <- parseToItems "[[bin]]"
        assertEq (show items) "[tablearr: bin]"

    export
    tableArrayDotted : Test
    tableArrayDotted = test "parse table array header with dotted key" $ do
        items <- parseToItems "[[bin.tags]]"
        assertEq (show items) "[tablearr: bin.tags]"

    export
    emptyFile : Test
    emptyFile = test "parse empty file" $ do
        items <- parseToItems ""
        assertEq (show items) "[]"

    export
    kvArrayNewLine : Test
    kvArrayNewLine = test "key-val with array with newlines" $ do
        items <- parseToItems "x = [\n\t1,\n\t2,\n\t3\n]"
        assertEq (show items) "[keyval: x = [1, 2, 3]]"

    export
    kvInlineTable : Test
    kvInlineTable = test "key-val with inline table" $ do
        items <- parseToItems "test = { path = \"../test-idr\" }"
        -- TODO strings are not interspreted *and* are `show`n
        assertEq (show items) "[keyval: test = {path = \"../test-idr\"}]"

namespace Abstract
    export
    kvGlobal : Test
    kvGlobal = test "global key-val" $ do
        table <- parse "x = 12"
        assertEq [("x", VInteger 12)] (toList table)

    export
    kvNested : Test
    kvNested = test "global nested key-val" $ do
        table <- parse "x.y = 12"
        assertEq (lookupNested ["x", "y"] table) (Just $ VInteger 12)

    export
    tableSectionKv : Test
    tableSectionKv = test "table section key-val" $ do
        table <- parse "[table-name]\nx = 12"
        assertEq (lookupNested ["table-name", "x"] table) (Just $ VInteger 12)

    export
    tableSectionNestedKv : Test
    tableSectionNestedKv = test "table section nested key-val" $ do
        table <- parse "[table-name]\nx.y = 12"
        assertEq (lookupNested ["table-name", "x", "y"] table) (Just $ VInteger 12)

    export
    inlineTable : Test
    inlineTable = test "inline table" $ do
        table <- parse "test = { x = 12, y = 21 }"
        assertEq (lookupNested ["test", "x"] table) (Just $ VInteger 12)

    export
    array : Test
    array = test "array" $ do
        table <- parse "x = [1, 3, 7]"
        assertEq (lookup "x" table) (Just $ VArray [VInteger 1, VInteger 3, VInteger 7])

public export
tests : List Test
tests = [
    Concrete.kvNoNewline,
    Concrete.kvComment,
    Concrete.kvNewline,
    Concrete.tableHeader,
    Concrete.tableHeaderDotted,
    Concrete.tableArray,
    Concrete.tableArrayDotted,
    Concrete.emptyFile,
    Concrete.kvArrayNewLine,
    Concrete.kvInlineTable,

    Abstract.kvGlobal,
    Abstract.kvNested,
    Abstract.tableSectionKv,
    Abstract.tableSectionNestedKv,
    Abstract.inlineTable,
    Abstract.array
]

max_stars_repo_name: tiatomee/toml-idr

max_issues_repo_name: tiatomee/toml-idr

max_forks_repo_name: tiatomee/toml-idr


text:
module Shaders

import Types
import GLCore

-- Return the enum value for the shader type for the given GL context
shaderType : Shader -> GLCxt -> IO Int
shaderType (Vertex _) cxt = getGLProp "VERTEX_SHADER" cxt
shaderType (Fragment _) cxt = getGLProp "FRAGMENT_SHADER" cxt

-- This could be better.. so much better
-- Takes a shader, a GL context and the enum value for the shader type
-- and creates a shader program, inserts the source into the program
-- and then compiles it.
-- This should possibly return an Either ShaderProg Error but then again you want
-- to know to explode if your shader doesn't compile sooooo yeah.
compileShader : Shader -> GLCxt -> Int -> IO ShaderProg
compileShader shdr (MkCxt c) type = compileIt
  where
    -- This is horrible, good grief Charlie Brown!!
    code : Shader -> String
    code (Vertex x) = x
    code (Fragment x) = x

    compileIt : IO ShaderProg
    compileIt = do
      s <- mkForeign (FFun "%0.createShader(%1)" [FPtr,FInt] FPtr) c type
      mkForeign (FFun "%0.shaderSource(%1,%2)" [FPtr,FPtr,FString] FUnit) c s (code shdr)
      mkForeign (FFun "%0.compileShader(%1)" [FPtr,FPtr] FUnit) c s
      return (MkShdrPrg s)

-- Build some shader goodness
buildShader : Shader -> GLCxt -> IO ShaderProg
buildShader shdr cxt = do
  typeInt <- shaderType shdr cxt
  compileShader shdr cxt typeInt

-- Attach a Shader Program to the given GL program and context
attachShader : GLProgram -> GLCxt -> ShaderProg -> IO (GLProgram, GLCxt)
attachShader (MkGLProg prog) (MkCxt cxt) (MkShdrPrg shdr) = do
  mkForeign (FFun "%0.attachShader(%1,%2)" [FPtr,FPtr,FPtr] FUnit) cxt prog shdr
  return ((MkGLProg prog), (MkCxt cxt))

-- Build,Compile,Link all given shaders with the given program and context.
compileAndLinkShaders : List Shader -> (GLProgram,GLCxt) -> IO (GLProgram, GLCxt)
compileAndLinkShaders [] ((MkGLProg x),(MkCxt y)) = do
  mkForeign (FFun "%0.linkProgram(%1)" [FPtr,FPtr] FUnit) y x
  return ((MkGLProg x), (MkCxt y))
compileAndLinkShaders (y :: xs) (prog,cxt) = do
  nPrgCxt <- buildShader y cxt >>= attachShader prog cxt
  compileAndLinkShaders xs nPrgCxt

-- Setting attribute locations for shader variables.
getAttribLocation : String -> (GLProgram,GLCxt) -> IO Int
getAttribLocation attr ((MkGLProg p), (MkCxt c)) =
  mkForeign (FFun "%0.getAttribLocation(%1,%2)" [FPtr,FPtr,FString] FInt) c p attr

-- Enable the Vertex Attribute Array for the current vertexPosAttrib
enableVertexAttribArray : (GLProgram,GLCxt) -> Int -> IO (GLProgram,GLCxt)
enableVertexAttribArray ((MkGLProg p),(MkCxt c)) loc = do
  mkForeign (FFun "%0.enableVertexAttribArray(%1)" [FPtr,FInt] FUnit) c loc
  return ((MkGLProg p),(MkCxt c))

-- Set the array pointer for the GL program so it knows where to find some vertices.
setVertexAttribPointer : Int -> Int -> (GLProgram,GLCxt) -> IO (GLProgram,GLCxt)
setVertexAttribPointer n loc ((MkGLProg p),(MkCxt c)) = do
  mkForeign (FFun
             "%0.vertexAttribPointer(%1, %2, %0.FLOAT, false, 0, 0)"
             [FPtr,FInt,FInt] FUnit
            ) c loc n
  return ((MkGLProg p),(MkCxt c))

max_stars_repo_name: mankyKitty/idris-webgl

max_issues_repo_name: mankyKitty/idris-webgl

max_forks_repo_name: mankyKitty/idris-webgl


text:
module Data.Time.Calendar

import public Data.Time.Calendar.Days
import public Data.Time.Calendar.CalendarDiffDays
import public Data.Time.Calendar.Gregorian
import public Data.Time.Calendar.WeekDate

%default total

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


text:
module Idris.IDEMode.REPL

import Core.Context
import Core.Directory
import Core.Metadata
import Core.Options
import Core.Unify

import Idris.Error
import Idris.Package
import Idris.Parser
import Idris.Pretty
import Idris.REPL
import Idris.Syntax
import Idris.Version
import Idris.Doc.String

import Idris.IDEMode.Commands
import Idris.IDEMode.Holes
import Idris.IDEMode.Parser
import Idris.IDEMode.SyntaxHighlight
import Idris.IDEMode.Pretty

import Protocol.Hex
import Libraries.Utils.Path

import Data.List
import System
import System.File

import Network.Socket
import Network.Socket.Data

%default covering

||| TODO: use the version in `Network.FFI` in network after the next release.
%foreign "C:idrnet_fdopen, libidris2_support, idris_net.h"
prim__idrnet_fdopen : Int -> String -> PrimIO AnyPtr

export
socketToFile : Socket -> IO (Either String File)
socketToFile (MkSocket f _ _ _) = do
  file <- FHandle <$> primIO (prim__idrnet_fdopen f "r+")
  if !(fileError file)
    then pure (Left "Failed to fdopen socket file descriptor")
    else pure (Right file)

export
initIDESocketFile : String -> Int -> IO (Either String File)
initIDESocketFile h p = do
  osock <- socket AF_INET Stream 0
  case osock of
    Left fail => do
      putStrLn (show fail)
      putStrLn "Failed to open socket"
      exitWith (ExitFailure 1)
    Right sock => do
      res <- bind sock (Just (Hostname h)) p
      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
                 do putStrLn (show p)
                    fflush stdout
                    res <- accept sock
                    case res of
                      Left err =>
                         pure (Left ("Failed to accept on socket with error: " ++ show err))
                      Right (s, _) =>
                         socketToFile s

getChar : File -> IO Char
getChar h = do
  if !(fEOF h)
     then do
       putStrLn "Alas the file is done, aborting"
       exitWith (ExitFailure 1)
     else do
       Right chr <- fGetChar h
           | Left err => do putStrLn "Failed to read a character"
                            exitWith (ExitFailure 1)
       pure chr

getFLine : File -> IO String
getFLine h
    = do Right str <- fGetLine h
               | Left err =>
                   do putStrLn "Failed to read a line"
                      exitWith (ExitFailure 1)
         pure str

getNChars : File -> Nat -> IO (List Char)
getNChars i Z = pure []
getNChars i (S k)
    = do x <- getChar i
         xs <- getNChars i k
         pure (x :: xs)

-- Read 6 characters. If they're a hex number, read that many characters.
-- Otherwise, just read to newline
getInput : File -> IO String
getInput f
    = do x <- getNChars f 6
         case fromHexChars (reverse x) of
              Nothing =>
                do rest <- getFLine f
                   pure (pack x ++ rest)
              Just num =>
                do inp <- getNChars f (integerToNat num)
                   pure (pack inp)

||| Do nothing and tell the user to wait for us to implmement this (or join the effort!)
todoCmd : {auto c : Ref Ctxt Defs} ->
          {auto o : Ref ROpts REPLOpts} ->
          String -> Core ()
todoCmd cmdName = iputStrLn $ reflow $ cmdName ++ ": command not yet implemented. Hopefully soon!"

data IDEResult
  = REPL REPLResult
  | NameList (List Name)
  | FoundHoles (List Holes.Data)
  | Term String   -- should be a PTerm + metadata, or SExp.
  | TTTerm String -- should be a TT Term + metadata, or perhaps SExp
  | NameLocList (List (Name, FC))

replWrap : Core REPLResult -> Core IDEResult
replWrap m = pure $ REPL !m

process : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto m : Ref MD Metadata} ->
          {auto o : Ref ROpts REPLOpts} ->
          IDECommand -> Core IDEResult
process (Interpret cmd)
    = replWrap $ interpret cmd
process (LoadFile fname_in _)
    = do let fname = case !(findIpkg (Just fname_in)) of
                          Nothing => fname_in
                          Just f' => f'
         replWrap $ Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname
process (NameAt name Nothing)
    = do defs <- get Ctxt
         glob <- lookupCtxtName (UN (mkUserName name)) (gamma defs)
         let dat = map (\(name, _, gdef) => (name, gdef.location)) glob
         pure (NameLocList dat)
process (NameAt n (Just _))
    = do todoCmd "name-at <name> <line> <column>"
         pure $ REPL $ Edited $ DisplayEdit emptyDoc
process (TypeOf n Nothing)
    = replWrap $ Idris.REPL.process (Check (PRef replFC (UN $ mkUserName n)))
process (TypeOf n (Just (l, c)))
    = replWrap $ Idris.REPL.process
               $ Editing (TypeAt (fromInteger l) (fromInteger c) (UN $ mkUserName n))
process (CaseSplit l c n)
    = replWrap $ Idris.REPL.process
    $ Editing $ CaseSplit False (fromInteger l) (fromInteger c)
    $ UN $ mkUserName n
process (AddClause l n)
    = replWrap $ Idris.REPL.process
    $ Editing $ AddClause False (fromInteger l)
    $ UN $ mkUserName n
process (AddMissing l n)
    = do todoCmd "add-missing"
         pure $ REPL $ Edited $ DisplayEdit emptyDoc
process (ExprSearch l n hs all)
    = replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l)
                     (UN $ Basic n) (map (UN . Basic) hs.list)))
process ExprSearchNext
    = replWrap $ Idris.REPL.process (Editing ExprSearchNext)
process (GenerateDef l n)
    = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN $ Basic n) 0))
process GenerateDefNext
    = replWrap $ Idris.REPL.process (Editing GenerateDefNext)
process (MakeLemma l n)
    = replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN $ mkUserName n)))
process (MakeCase l n)
    = replWrap $ Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN $ mkUserName n)))
process (MakeWith l n)
    = replWrap $ Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN $ mkUserName n)))
process (DocsFor n modeOpt)
    = replWrap $ Idris.REPL.process (Doc $ APTerm (PRef EmptyFC (UN $ mkUserName n)))
process (Apropos n)
    = do todoCmd "apropros"
         pure $ REPL $ Printed emptyDoc
process (Directive n)
    = do todoCmd "directive"
         pure $ REPL $ Printed emptyDoc
process (WhoCalls n)
    = do todoCmd "who-calls"
         pure $ NameList []
process (CallsWho n)
    = do todoCmd "calls-who"
         pure $ NameList []
process (BrowseNamespace ns)
    = replWrap $ Idris.REPL.process (Browse (mkNamespace ns))
process (NormaliseTerm tm)
    = do todoCmd "normalise-term"
         pure $ Term tm
process (ShowTermImplicits tm)
    = do todoCmd "show-term-implicits"
         pure $ Term tm
process (HideTermImplicits tm)
    = do todoCmd "hide-term-implicits"
         pure $ Term tm
process (ElaborateTerm tm)
    = do todoCmd "elaborate-term"
         pure $ TTTerm tm
process (PrintDefinition n)
    = do todoCmd "print-definition"
         pure $ REPL $ Printed (pretty n)
process (ReplCompletions n)
    = do todoCmd "repl-completions"
         pure $ NameList []
process (EnableSyntax b)
    = do setSynHighlightOn b
         pure $ REPL $ Printed (reflow "Syntax highlight option changed to" <++> pretty b)
process Version
    = replWrap $ Idris.REPL.process ShowVersion
process (Metavariables _)
    = FoundHoles <$> getUserHolesData
process GetOptions
    = replWrap $ Idris.REPL.process GetOpts

processCatch : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto m : Ref MD Metadata} ->
               {auto o : Ref ROpts REPLOpts} ->
               IDECommand -> Core IDEResult
processCatch cmd
    = do c' <- branch
         u' <- get UST
         s' <- get Syn
         o' <- get ROpts
         catch (do res <- process cmd
                   commit
                   pure res)
               (\err => do put Ctxt c'
                           put UST u'
                           put Syn s'
                           put ROpts o'
                           msg <- perror err
                           pure $ REPL $ REPLError msg)

idePutStrLn : {auto c : Ref Ctxt Defs} -> File -> Integer -> String -> Core ()
idePutStrLn outf i msg
    = send outf $ WriteString msg i

returnFromIDE : {auto c : Ref Ctxt Defs} -> File -> Integer -> IDE.ReplyPayload -> Core ()
returnFromIDE outf i payload
    = do send outf (Immediate payload i)

printIDEResult : {auto c : Ref Ctxt Defs} -> File -> Integer -> IDE.Result -> Core ()
printIDEResult outf i result
  = returnFromIDE outf i $ OK result []

printIDEResultWithHighlight :
  {auto c : Ref Ctxt Defs} ->
  File -> Integer -> (Result, List (Span Properties)) ->
  Core ()
printIDEResultWithHighlight outf i (result, spans) = do
--  log "ide-mode.highlight" 10 $ show spans
  returnFromIDE outf i
    $ OK result spans

-- TODO: refactor to construct an error response
printIDEError : Ref ROpts REPLOpts => {auto c : Ref Ctxt Defs} -> File -> Integer -> Doc IdrisAnn -> Core ()
printIDEError outf i msg = returnFromIDE outf i $
  uncurry IDE.Error !(renderWithDecorations annToProperties msg)

Cast REPLEval String where
  cast EvalTC = "typecheck"
  cast NormaliseAll = "normalise"
  cast Execute = "execute"
  cast Scheme = "scheme"

Cast REPLOpt REPLOption where
  cast (ShowImplicits impl) = MkOption "show-implicits" BOOL impl
  cast (ShowNamespace ns)   = MkOption "show-namespace" BOOL ns
  cast (ShowTypes typs)     = MkOption "show-types"     BOOL typs
  cast (EvalMode mod)       = MkOption "eval"           ATOM $ cast mod
  cast (Editor editor)      = MkOption "editor"         STRING editor
  cast (CG str)             = MkOption "cg"             STRING str
  cast (Profile p)          = MkOption "profile"        BOOL p
  cast (EvalTiming p)       = MkOption "evaltiming"     BOOL p

displayIDEResult : {auto c : Ref Ctxt Defs} ->
       {auto u : Ref UST UState} ->
       {auto s : Ref Syn SyntaxInfo} ->
       {auto m : Ref MD Metadata} ->
       {auto o : Ref ROpts REPLOpts} ->
       File -> Integer -> IDEResult -> Core ()
displayIDEResult outf i  (REPL $ REPLError err)
  = printIDEError outf i err
displayIDEResult outf i  (REPL RequestedHelp  )
  = printIDEResult outf i $ AString displayHelp
displayIDEResult outf i  (REPL $ Evaluated x Nothing)
  = printIDEResultWithHighlight outf i
  $ mapFst AString
   !(renderWithDecorations syntaxToProperties $ prettyTerm x)
displayIDEResult outf i  (REPL $ Evaluated x (Just y))
  = printIDEResultWithHighlight outf i
  $ mapFst AString
   !(renderWithDecorations syntaxToProperties
     $ prettyTerm x <++> ":" <++> prettyTerm y)
displayIDEResult outf i  (REPL $ Printed xs)
  = printIDEResultWithHighlight outf i
  $ mapFst AString
  $ !(renderWithDecorations annToProperties xs)
displayIDEResult outf i (REPL (PrintedDoc xs))
  = printIDEResultWithHighlight outf i
  $ mapFst AString
  $ !(renderWithDecorations docToProperties xs)
displayIDEResult outf i  (REPL $ TermChecked x y)
  = printIDEResultWithHighlight outf i
  $ mapFst AString
   !(renderWithDecorations syntaxToProperties
     $ prettyTerm x <++> ":" <++> prettyTerm y)
displayIDEResult outf i  (REPL $ FileLoaded x)
  = printIDEResult outf i $ AUnit
displayIDEResult outf i  (REPL $ ErrorLoadingFile x err)
  = printIDEError outf i $ reflow "Error loading file" <++> pretty x <+> colon <++> pretty (show err)
displayIDEResult outf i  (REPL $ ErrorsBuildingFile x errs)
  = do errs' <- traverse perror errs
       printIDEError outf i $ reflow "Error(s) building file" <++> pretty x <+> colon <++> vsep errs'
displayIDEResult outf i  (REPL $ NoFileLoaded)
  = printIDEError outf i $ reflow "No file can be reloaded"
displayIDEResult outf i  (REPL $ CurrentDirectory dir)
  = printIDEResult outf i $ AString $ "Current working directory is \"\{dir}\""
displayIDEResult outf i  (REPL CompilationFailed)
  = printIDEError outf i $ reflow "Compilation failed"
displayIDEResult outf i  (REPL $ Compiled f)
  = printIDEResult outf i $ AString "File \{f} written"
displayIDEResult outf i  (REPL $ ProofFound x)
  = printIDEResult outf i $ AString $ show x
displayIDEResult outf i  (REPL $ Missed cases)
  = printIDEResult outf i
  $ AString $ showSep "\n"
  $ map handleMissing' cases
displayIDEResult outf i  (REPL $ CheckedTotal xs)
  = printIDEResult outf i
  $ AString $ showSep "\n"
  $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs
displayIDEResult outf i  (REPL $ LogLevelSet k)
  = printIDEResult outf i
  $ AString $ "Set loglevel to " ++ show k
displayIDEResult outf i  (REPL $ OptionsSet opts)
  = printIDEResult outf i $ AnOptionList $ map cast opts
displayIDEResult outf i  (REPL $ VersionIs x)
  = let (major, minor, patch) = semVer x
    in printIDEResult outf i $ AVersion $ MkIdrisVersion
      {major, minor, patch, tag = versionTag x}
displayIDEResult outf i (REPL $ Edited (DisplayEdit xs))
  = printIDEResult outf i $ AString $ show xs
displayIDEResult outf i (REPL $ Edited (EditError x))
  = printIDEError outf i x
displayIDEResult outf i (REPL $ Edited (MadeLemma lit name pty pappstr))
  = printIDEResult outf i $ AMetaVarLemma $ MkMetaVarLemma
      { application = pappstr
      , lemma = relit lit $ show name ++ " : " ++ show pty
      }
displayIDEResult outf i (REPL $ Edited (MadeWith lit wapp))
  = printIDEResult outf i
  $ AString $ showSep "\n" (map (relit lit) wapp)
displayIDEResult outf i (REPL $ (Edited (MadeCase lit cstr)))
  = printIDEResult outf i
  $ AString $ showSep "\n" (map (relit lit) cstr)
displayIDEResult outf i (FoundHoles holes)
  = printIDEResult outf i $ AHoleList $ map holeIDE holes
displayIDEResult outf i (NameList ns)
  = printIDEResult outf i $ ANameList $ map show ns
displayIDEResult outf i (Term t)
  = printIDEResult outf i $ AString t
displayIDEResult outf i (TTTerm t)
  = printIDEResult outf i $ AString t
displayIDEResult outf i (REPL $ ConsoleWidthSet mn)
  = let width = case mn of
                    Just k  => show k
                    Nothing => "auto"
    in printIDEResult outf i $ AString $ "Set consolewidth to " ++ width
displayIDEResult outf i (NameLocList dat)
  = printIDEResult outf i $ ANameLocList $
       !(traverse (constructFileContext . map toNonEmptyFC) dat)
  where
    -- In order to recover the full path to the module referenced by FC,
    -- which stores a module identifier as opposed to a full path,
    -- we need to check the project's source folder and all the library directories
    -- for the relevant source file.
    -- (!) Always returns the *absolute* path.
    sexpOriginDesc : OriginDesc -> Core String
    sexpOriginDesc (PhysicalIdrSrc modIdent) = do
      defs <- get Ctxt
      let wdir = defs.options.dirs.working_dir
      let pkg_dirs = filter (/= ".") defs.options.dirs.extra_dirs
      let exts = map show listOfExtensions
      Just fname <- catch
          (Just . (wdir </>) <$> nsToSource replFC modIdent) -- Try local source first
          -- if not found, try looking for the file amongst the loaded packages.
          (const $ firstAvailable $ do
            pkg_dir <- pkg_dirs
            let pkg_dir_abs = ifThenElse (isRelative pkg_dir) (wdir </> pkg_dir) pkg_dir
            ext <- exts
            pure (pkg_dir_abs </> ModuleIdent.toPath modIdent <.> ext))
        | _ => pure "(File-Not-Found)"
      pure fname
    sexpOriginDesc (PhysicalPkgSrc fname) = pure fname
    sexpOriginDesc (Virtual Interactive) = pure "(Interactive)"

    constructFileContext : (Name, NonEmptyFC) -> Core (String, FileContext)
    constructFileContext (name, origin, (startLine, startCol), (endLine, endCol)) = pure $
        -- TODO: fix the emacs mode to use the more structured SExpr representation
        (!(render $ pretty name)
        , MkFileContext
          { file  = !(sexpOriginDesc origin)
          , range = MkBounds {startCol, startLine, endCol, endLine}
          })

-- do not use a catchall so that we are warned about missing cases when adding a
-- new construtor to the enumeration.
displayIDEResult _ _ (REPL Done) = pure ()
displayIDEResult _ _ (REPL (Executed _)) = pure ()
displayIDEResult _ _ (REPL (ModuleLoaded _)) = pure ()
displayIDEResult _ _ (REPL (ErrorLoadingModule _ _)) = pure ()
displayIDEResult _ _ (REPL (CompiledLibrary _)) = pure ()
displayIDEResult _ _ (REPL (ColorSet _)) = pure ()
displayIDEResult _ _ (REPL DefDeclared) = pure ()
displayIDEResult _ _ (REPL Exited) = pure ()

handleIDEResult : {auto c : Ref Ctxt Defs} ->
       {auto u : Ref UST UState} ->
       {auto s : Ref Syn SyntaxInfo} ->
       {auto m : Ref MD Metadata} ->
       {auto o : Ref ROpts REPLOpts} ->
       File -> Integer -> IDEResult -> Core ()
handleIDEResult outf i (REPL Exited) = idePutStrLn outf i "Bye for now!"
handleIDEResult outf i other = displayIDEResult outf i other

loop : {auto c : Ref Ctxt Defs} ->
       {auto u : Ref UST UState} ->
       {auto s : Ref Syn SyntaxInfo} ->
       {auto m : Ref MD Metadata} ->
       {auto o : Ref ROpts REPLOpts} ->
       Core ()
loop
    = do res <- getOutput
         case res of
              REPL _ => printError $ reflow "Running idemode but output isn't"
              IDEMode idx inf outf => do
                inp <- coreLift $ getInput inf
                end <- coreLift $ fEOF inf
                if end
                   then pure ()
                   else case parseSExp inp of
                      Left err =>
                        do printIDEError outf idx (reflow "Parse error:" <++> !(perror err))
                           loop
                      Right sexp =>
                        case getMsg sexp of
                          Just (cmd, i) =>
                            do updateOutput i
                               res <- processCatch cmd
                               handleIDEResult outf i res
                               loop
                          Nothing =>
                            do printIDEError outf idx (reflow "Unrecognised command:" <++> pretty (show sexp))
                               loop
  where
    updateOutput : Integer -> Core ()
    updateOutput idx
        = do IDEMode _ i o <- getOutput
                 | _ => pure ()
             setOutput (IDEMode idx i o)

export
replIDE : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto m : Ref MD Metadata} ->
          {auto o : Ref ROpts REPLOpts} ->
          Core ()
replIDE
    = do res <- getOutput
         case res of
              REPL _ => printError $ reflow "Running idemode but output isn't"
              IDEMode _ inf outf => do
                send outf (ProtocolVersion 2 1) -- TODO: Move this info somewhere more central
                loop