text:
module Markdown.Data

import Data.String
import Data.List

import Extra.String

-- Note: this is currently infinitely recursive
-- %default total

public export
data Inline
  = Text String
  | Pre String
  | CodeBlock String (Maybe String)
  | Italics (List Inline)
  | Bold (List Inline)
  | Link String String
  | Image String String
  | Html String (List Inline)

public export
data Block
   = Header Nat (List Inline)
   | Paragraph (List Inline)

public export
data Markdown =
  Doc (List Block)

%name Markdown markdown

mutual
  showInlines : List Inline -> String
  showInlines = showList showInline

  showBlocks : List Block -> String
  showBlocks = showList showBlock

  showBlock : Block -> String
  showBlock (Header level inline) = "H" ++ (show level) ++ " " ++ (showInlines inline)
  showBlock (Paragraph inline) = "P " ++ (showInlines inline)

  showInline : Inline -> String
  showInline (Text text) = "Text " ++ (quote text)
  showInline (Pre text) = "Pre " ++ (quote text)
  showInline (CodeBlock text type) = "CodeBlock [" ++ show type ++ "] " ++ (quote text)
  showInline (Italics inline) = "Italics " ++ (showInlines inline)
  showInline (Bold inline) = "Bold " ++ (showInlines inline)
  showInline (Link href desc) = "Link " ++ href ++ " " ++ desc
  showInline (Image alt src) = "Image " ++ alt ++ " " ++ src
  showInline (Html tag inline) = "HTML <" ++ tag ++ "> " ++ (showInlines inline)

export covering
Show Inline where
  show = showInline

export covering
Show Block where
  show = showBlock

export covering
Show Markdown where
  show (Doc blocks) = showBlocks blocks

export covering
Eq Inline where
  (Text text0) == (Text text1) = text0 == text1
  (Pre text0) == (Pre text1) = text0 == text1
  (CodeBlock text0 type0) == (CodeBlock text1 type1) = text0 == text1 && type0 == type1
  (Italics inline0) == (Italics inline1) = inline0 == inline1
  (Bold inline0) == (Bold inline1) = inline0 == inline1
  (Link href0 desc0) == (Link href1 desc1) = href0 == href1 && desc0 == desc1
  (Image href0 desc0) == (Image href1 desc1) = href0 == href1 && desc0 == desc1
  (Html tag0 inline0) == (Html tag1 inline1) = tag0 == tag1 && inline0 == inline1
  _ == _ = False

export covering
Eq Block where
  (Header level0 inline0) == (Header level1 inline1) = level0 == level1 && inline0 == inline1
  (Paragraph inline0) == (Paragraph inline1) = inline0 == inline1
  _ == _ = False

export covering
Eq Markdown where
  (Doc a) == (Doc b) = a == b

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Highlight.Main

import Effects
import Effect.File
import Highlight.Parser
import Highlight.Regions
import Highlight.Formats
import Lightyear.Strings

---------------------
-- Usage Instructions
---------------------

||| Print usage instructions
usage : IO ()
usage = putStrLn "Usage:" *>
        putStrLn "highlight-idris BASENAME" *>
        putStr   "where BASENAME.idr and BASENAME.idh both exist. " *>
        putStrLn "The output will be BASENAME.tex and BASENAME.html."

---------------
-- Highlighting
---------------

||| Extract a sorted list of highlights from a parsed Idris highlight file
||| @ file the filename to which highlights apply
||| @ hls the highlighting information
sortedHighlights : (file : String) ->
                   (hls  : List SExpr) ->
                   List (Region HighlightType)
sortedHighlights file hls =
    let metadata = map getRegionMeta hls
        successfulMetadata = catMaybes metadata
        regs = mkHls successfulMetadata
        forThisFile = filter (sameFile file) regs
    in sort forThisFile
  where
    sameFile : String -> Region HighlightType -> Bool
    sameFile fname reg = (fileName reg) == fname || (fileName reg) == ("./" ++ fname)

||| Highlight `src` in `format` using `highlights` and write to `outputFile`.
||| @ outputFile The file to which to write the formatted highlights.
||| @ format     The output `Format`.
||| @ src        The contents of the Idris source file.
||| @ highlights A list of highlights for `src`.
doHighlight : (outputFile : String) ->
              (format     : Format) ->
              (src        : String) ->
              (highlights : List (Region HighlightType)) ->
              Eff (IO ()) [FILE ()]
doHighlight outputFile format src highlights =
    do Success <- writeFile outputFile (highlight format src highlights)
         | FError err => pure (printLn err)
       pure (pure ())

||| Generate `basename`.tex and `basename`.html via `doHighlight`.
doHighlights : (basename : String) -> Eff (IO ()) [FILE ()]
doHighlights bn =
    do Result info <- readFile (bn ++ ".idh")
         | FError err => pure (printLn err)
       case parse expr info of
         Left err => pure (putStrLn err)
         Right (SList xs) =>
           do let idr = bn ++ ".idr"
              Result src <- readFile idr
                | FError err => pure (printLn err)
              let hls = sortedHighlights idr xs
              doHighlight (bn ++ ".tex")  LaTeX src hls
              doHighlight (bn ++ ".html") HTML  src hls

-------------------------
-- Figuring out filenames
-------------------------

||| Get the file name from the command line arguments.
getFilename : IO (Maybe String)
getFilename = case !getArgs of
                [prog, filename] => pure (Just filename)
                _                => pure Nothing

||| Strip the ".idh" extension from a file's name.
basename : (file : String) -> String
basename file =
    if isSuffixOf ".idh" file
      then pack (reverse (drop 4 (reverse (unpack file))))
      else file

||| Get the base filename from the command line arguments.
getBasename : IO (Maybe String)
getBasename = map (map basename) getFilename

main : IO ()
main =
    do Just basename <- getBasename | _ => usage
       run (doHighlights basename)
       putStrLn ("Processed " ++ basename)

ext: idr


text:
public export
data Fuel = Dry | More (Lazy Fuel)

public export
partial
forever : Fuel
forever = More forever

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
import System

{- 3 -}

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
     then pure (Just (cast input))
     else pure Nothing

guess : (target : Nat) -> (guesses : Nat) -> IO ()
guess target guesses = do
  putStrLn (show guesses ++ " guesses so far")
  putStr ("Guess a number between 1 and 100: ")
  isNum <- readNumber
  case isNum of
       Nothing => do putStrLn "Invalid input"
                     guess target guesses
       Just userguess => if userguess < target
                            then do putStrLn "Too low"
                                    guess target (guesses + 1)
                            else if userguess > target
                                 then do putStrLn "Too high"
                                         guess target  (guesses + 1)
                                 else putStrLn "Well done!"

main : IO ()
main = do t <- time
          guess (cast (t `mod` 101)) 0

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module SQLite3.Constants

import SQLite3.Bindings
import Data.Buffer

public export
data ErrorCode : Type where

||| Result Codes versus Error Codes
|||
||| "Error codes" are a subset of "result codes" that indicate that something has gone wrong.
||| There are only a few non-error result codes: SQLITE_OK, SQLITE_ROW, and SQLITE_DONE.
||| The term "error code" means any result code other than these three.
||| -- from: https://sqlite.org/rescode.html
public export
data ResultCode : Type where
  ||| Value: 0   /* Successful result */
  Ok : ResultCode
  ||| Value: 1   /* Generic error */
  Error : ResultCode
  ||| Value: 2   /* Internal logic error in SQLite */
  Internal : ResultCode
  ||| Value: 3   /* Access permission denied */
  Perm : ResultCode
  ||| Value: 4   /* Callback routine requested an abort */
  Abort : ResultCode
  ||| Value: 5   /* The database file is locked */
  Busy : ResultCode
  ||| Value: 6   /* A table in the database is locked */
  Locked : ResultCode
  ||| Value: 7   /* A malloc() failed */
  NoMem : ResultCode
  ||| Value: 8   /* Attempt to write a readonly database */
  ReadOnly : ResultCode
  ||| Value: 9   /* Operation terminated by sqlite3_interrupt()*/
  Interrupt : ResultCode
  ||| Value: 10   /* Some kind of disk I/O error occurred */
  IoErr : ResultCode
  ||| Value: 11   /* The database disk image is malformed */
  Corrupt : ResultCode
  ||| Value: 12   /* Unknown opcode in sqlite3_file_control() */
  NotFound : ResultCode
  ||| Value: 13   /* Insertion failed because database is full */
  Full : ResultCode
  ||| Value: 14   /* Unable to open the database file */
  CantOpen : ResultCode
  ||| Value: 15   /* Database lock protocol error */
  Protocol : ResultCode
  ||| Value: 16   /* Internal use only */
  Empty : ResultCode
  ||| Value: 17   /* The database schema changed */
  Schema : ResultCode
  ||| Value: 18   /* String or BLOB exceeds size limit */
  TooBig : ResultCode
  ||| Value: 19   /* Abort due to constraint violation */
  Constraint : ResultCode
  ||| Value: 20   /* Data type mismatch */
  Mismatch : ResultCode
  ||| Value: 21   /* Library used incorrectly */
  Misuse : ResultCode
  ||| Value: 22   /* Uses OS features not supported on host */
  NoLFS : ResultCode
  ||| Value: 23   /* Authorization denied */
  Auth : ResultCode
  ||| Value: 24   /* Not used */
  Format : ResultCode
  ||| Value: 25   /* 2nd parameter to sqlite3_bind out of range */
  Range : ResultCode
  ||| Value: 26   /* File opened that is not a database file */
  NotADB : ResultCode
  ||| Value: 27   /* Notifications from sqlite3_log() */
  Notice : ResultCode
  ||| Value: 28   /* Warnings from sqlite3_log() */
  Warning : ResultCode
  ||| Value: 100  /* sqlite3_step() has another row ready */
  Row : ResultCode
  ||| Value: 101  /* sqlite3_step() has finished executing */
  Done : ResultCode

export
Show ResultCode where
  show Ok = "Ok"
  show Error = "Error"
  show Internal = "Internal"
  show Perm = "Perm"
  show Abort = "Abort"
  show Busy = "Busy"
  show Locked = "Locked"
  show NoMem = "NoMem"
  show ReadOnly = "ReadOnly"
  show Interrupt = "Interrupt"
  show IoErr = "IoErr"
  show Corrupt = "Corrupt"
  show NotFound = "NotFound"
  show Full = "Full"
  show CantOpen = "CantOpen"
  show Protocol = "Protocol"
  show Empty = "Empty"
  show Schema = "Schema"
  show TooBig = "TooBig"
  show Constraint = "Constraint"
  show Mismatch = "Mismatch"
  show Misuse = "Misuse"
  show NoLFS = "NoLFS"
  show Auth = "Auth"
  show Format = "Format"
  show Range = "Range"
  show NotADB = "NotADB"
  show Notice = "Notice"
  show Warning = "Warning"
  show Row = "Row"
  show Done = "Done"

namespace ResultCode
  export
  from_raw : Int -> Maybe ResultCode
  from_raw 0   = Just Ok
  from_raw 1   = Just Error
  from_raw 2   = Just Internal
  from_raw 3   = Just Perm
  from_raw 4   = Just Abort
  from_raw 5   = Just Busy
  from_raw 6   = Just Locked
  from_raw 7   = Just NoMem
  from_raw 8   = Just ReadOnly
  from_raw 9   = Just Interrupt
  from_raw 10  = Just IoErr
  from_raw 11  = Just Corrupt
  from_raw 12  = Just NotFound
  from_raw 13  = Just Full
  from_raw 14  = Just CantOpen
  from_raw 15  = Just Protocol
  from_raw 16  = Just Empty
  from_raw 17  = Just Schema
  from_raw 18  = Just TooBig
  from_raw 19  = Just Constraint
  from_raw 20  = Just Mismatch
  from_raw 21  = Just Misuse
  from_raw 22  = Just NoLFS
  from_raw 23  = Just Auth
  from_raw 24  = Just Format
  from_raw 25  = Just Range
  from_raw 26  = Just NotADB
  from_raw 27  = Just Notice
  from_raw 28  = Just Warning
  from_raw 100 = Just Row
  from_raw 101 = Just Done
  from_raw _   = Nothing

public export
data ConcreteType : Type where
  ||| #define SQLITE_INTEGER  1
  AInteger : ConcreteType
  ||| #define SQLITE_FLOAT    2
  AFloat : ConcreteType
  ||| #define SQLITE_TEXT     3
  AText : ConcreteType
  ||| #define SQLITE_BLOB     4
  ABlob : ConcreteType

export
Show ConcreteType where
  show AInteger = "Integer"
  show AFloat = "Float"
  show AText = "Text"
  show ABlob = "Blob"

export
Eq ConcreteType where
  AInteger == AInteger = True
  AFloat == AFloat = True
  AText == AText = True
  ABlob == ABlob = True
  _ == _ = False

public export
data DataType : Type where
  Concrete : ConcreteType -> DataType
  ||| #define SQLITE_NULL     5
  ANull : DataType

export
Show DataType where
  show ANull = "Null"
  show (Concrete t) = show t

export
Eq DataType where
  Concrete x == Concrete x' = x == x'
  ANull == ANull = True
  _ == _ = False

namespace DataType
  export
  from_raw : Int -> Maybe DataType
  from_raw 1 = Just $ Concrete AInteger
  from_raw 2 = Just $ Concrete AFloat
  from_raw 3 = Just $ Concrete AText
  from_raw 4 = Just $ Concrete ABlob
  from_raw 5 = Just ANull
  from_raw _ = Nothing


text:
module Data.Filter

import Data.DList
import Data.List.Predicates.Interleaving

%default total
%access public export

data Filter : (holdsFor : type -> Type)
           -> (input : List type)
           -> Type where
  MkFilter : (kept : List type)
          -> (prfOrdering : Interleaving kept thrown input)
          -> (prfKept     : DList type holdsFor kept)
          -> (prfThrown   : DList type (Not . holdsFor) thrown)
          -> Filter holdsFor input

filter : (test   : (value : type) -> Dec (holds value))
      -> (input  : List type)
      -> Filter holds input
filter test [] = MkFilter [] Empty [] []
filter test (x :: xs) with (filter test xs)
  filter test (x :: xs) | (MkFilter kept prfOrdering prfKept prfThrown) with (test x)
    filter test (x :: xs) | (MkFilter kept prfOrdering prfKept prfThrown) | (Yes prf) =
      MkFilter (x::kept) (LeftAdd x prfOrdering) (prf :: prfKept) prfThrown
    filter test (x :: xs) | (MkFilter kept prfOrdering prfKept prfThrown) | (No contra) =
      MkFilter kept (RightAdd x prfOrdering) prfKept (contra :: prfThrown)

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
-- Prints out some things, tries using color, and asks the user something.
-- compile with `idris -p effects -p curses -o testE testE.idr`

module Main

import Effects
import Effect.Curses

test : { [CURSES Pre] ==> [CURSES Post] } Eff ()
test = do start WaitForever
          addStr "Welcome to testE\nPress any key to continue"
          getCh
          Color <- startColor | NoColor => noColor
          setAttrAndColor [Bold, Underline] $ Just (MkColorPair 1 Red Blue)
          clear
          (lin, _) <- scrSize
          move (lin `div` 2) 0
          addStr "This is colorful text with some attributes."
          getCh
          setAttrAndColor [] Nothing
          loop
          end

   where noColor : { [CURSES $ Active NoColor] ==> [CURSES Post] } Eff ()
         noColor = do addStr "\nYour terminal doesn't support color!"
                      addStr "\nThe program will terminate now!"
                      end
         loop : { [CURSES $ Active Color] } Eff ()
         loop = do clear
                   addStr "Please write \"quit\" and press enter: "
                   when (!(getStr True False) /= "quit") loop

main : IO ()
main = run test

max_stars_repo_name: zenntenn/curses-idris

max_issues_repo_name: zenntenn/curses-idris

max_forks_repo_name: zenntenn/curses-idris


text:
-- An answer to a question by Nicolas Alexander Schmidt in the idris mailing list.

%default total

interface Foo (p : Type -> Type) where
  bar : {0 a : _} -> p a => a

data OnlyInt : Type -> Type where
  NiceCase : OnlyInt Int

Foo OnlyInt where
  bar @{NiceCase} = 0

-- Why can't we remove `BadCase` and its match from `bar` implementation?
-- Compiler claims that match in not exhaustive, however, everything works for `Nat`s:

data X : Nat -> Type where
  X10 : X 10

bbar : {a : _} -> X a -> Int
bbar {a=10} X10 = 1

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Web.Internal.VisibilityPrim

import JS
import Web.Internal.Types

%default total


text:
import Data.Buffer
import System.File

main : IO ()
main
    = do Just buf <- newBuffer 100
              | Nothing => putStrLn "Buffer creation failed"
         s <- rawSize buf
         printLn s

         setInt32 buf 1 94
         setString buf 5 "AAAA"
         val <- getInt32 buf 1
         printLn val

         setDouble buf 10 94.42
         val <- getDouble buf 10
         printLn val

         putStrLn $ "bytes: " ++ show (stringByteLength "Hello there!")
         setString buf 20 "Hello there!"
         val <- getString buf 20 5
         printLn val

         val <- getString buf 26 6
         printLn val

         copyData buf 6 11 buf 60

         ds <- bufferData buf
         printLn ds

         Right _ <- writeBufferToFile "test.buf" buf 100
             | Left err => putStrLn "Buffer write fail"
         Right buf2 <- createBufferFromFile "test.buf"
             | Left err => putStrLn "Buffer read fail"

         ds <- bufferData buf2
         printLn ds

         freeBuffer buf
         freeBuffer buf2

         ignore $ removeFile "test.buf"

-- Put back when the File API is moved to C and these can work again
--          Right f <- openBinaryFile "test.buf" Read
--              | Left err => putStrLn "File error on read"
--          Just buf3 <- newBuffer 99
--               | Nothing => putStrLn "Buffer creation failed"
--          Right _ <- readBufferFromFile f buf3 100
--              | Left err => do putStrLn "Buffer read fail"
--                               closeFile f
--          closeFile f

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Conat

%default total

namespace R

  record Conat where
    constructor C
    pred : Maybe $ Inf Conat

  Z : Conat
  Z = C {pred = Nothing}

  S : Conat -> Conat
  S n = C {pred = Just n}

  -- Infinity value
  I : Conat
  I = C {pred = Just I}

  coind : (p : Conat -> Type) -> p Z -> ({n : Conat} -> p (S n) -> p n) -> (n : Conat) -> Inf (p n)
  coind p base _    (C Nothing)    = base
  coind p base prev n@(C $ Just _) = prev {n} $ coind p base prev $ S n

namespace D

  %hide Prelude.Z
  %hide Prelude.S

  %hide Conat.R.Conat
  %hide Conat.R.Z
  %hide Conat.R.S

  data Conat : Type where
    Z : Conat
    S : Inf Conat -> Conat

  I : Conat
  I = S I

  coind : (p : Conat -> Type) -> p Z -> ({n : Conat} -> p (S n) -> p n) -> (n : Conat) -> Inf (p n)
  coind p base _    Z       = base
  coind p base prev n@(S _) = prev {n} $ coind p base prev $ S n


text:
> module Fraction.Normal

> import Fraction.Fraction
> import Fraction.BasicOperations
> import Nat.Coprime
> import Unique.Predicates
> import Nat.GCD
> import Nat.GCDEuclid
> import PNat.PNat
> import Nat.Positive
> import Pairs.Operations

> %default total

> %access public export

> |||
> data Normal : Fraction -> Type where
>   MkNormal  : {x : Fraction} -> Coprime (num x) (den x) -> Normal x

> |||
> NormalUnique : {x : Fraction} -> Unique (Normal x)
> NormalUnique {x} (MkNormal p) (MkNormal q) = cong (CoprimeUnique p q)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module LightClick.Types.Usage

import Data.List
import Data.Vect

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

import LightClick.Error

import LightClick.Types
import LightClick.Types.Equality

%default total

public export
PortList : (p     : Nat)
        -> (names : Vect p String)
                 -> Type
PortList = DVect String (Ty . PORT)

namespace PortList

  public export
  data Division : (0 pred : (label : String) -> Ty (PORT label) -> Type)

               -> {ps    : Vect p String}
               -> {ns    : Vect n String}
               -> {names : Vect o String}

               -> (pos  : PortList p ps)
               -> (neg  : PortList n ns)
               -> (orig : PortList o names)
                       -> Type
    where
      Empty : Division pred Nil Nil Nil

      Pos : {0 pred : (label : String) -> Ty (PORT label) -> Type}
         -> {pos  : PortList p ps}
         -> {neg  : PortList n ns}
         -> {orig : PortList o os}

         -> {label : String}
         -> {port : Ty (PORT label)}

         -> (prf  : pred label port)
         -> (rest : Division pred        pos  neg        orig)
                 -> Division pred (port::pos) neg (port::orig)

      Neg : {0 pred : (label : String) -> Ty (PORT label) -> Type}
         -> {pos  : PortList p ps}
         -> {neg  : PortList n ns}
         -> {orig : PortList o os}

         -> {label : String}
         -> {port : Ty (PORT label)}

         -> (prf  : Not (pred label port))

         -> (rest : Division pred pos        neg         orig)
                 -> Division pred pos (port::neg) (port::orig)

  public export
  data State : (pred  : (label : String) -> (port : Ty (PORT label)) -> Type)
            -> (ports : PortList p names)
                     -> Type
    where

      MkState : {0 pred : (label : String) -> Ty (PORT label) -> Type}

             -> {os       : Vect     o String}
             -> {orig     : PortList o os}

             -> (ps       : Vect     p String)
             -> (pos      : PortList p ps)

             -> (ns       : Vect     n String)
             -> (neg      : PortList n ns)

             -> (division : Division pred pos neg orig)

                         -> State pred orig

  export
  state : (0 pred  : (label : String) -> (port : Ty (PORT label)) -> Type)

       -> (dec   : (label : String) -> (port : Ty (PORT label)) -> Dec (pred label port))
       -> (ports : PortList p ps)
                -> State pred ports
  state pred _ [] = MkState Nil Nil Nil Nil Empty

  state pred dec ((TyPort l d s w t u) :: ports) with (dec l (TyPort l d s w t u))
    state pred dec ((TyPort l d s w t u) :: ports) | (Yes prf) with (state pred dec ports)
      state pred dec ((TyPort l d s w t u) :: ports) | (Yes prf) | (MkState xs pos ns neg division)
        = MkState (l::xs) ((TyPort l d s w t u)::pos) ns neg (Pos prf division)

    state pred dec ((TyPort l d s w t u) :: ports) | (No contra) with (state pred dec ports)
      state pred dec ((TyPort l d s w t u) :: ports) | (No contra) | (MkState xs pos ns neg division)
        = MkState xs pos (l::ns) ((TyPort l d s w t u)::neg) (Neg contra division)

namespace Free

  namespace Port
    public export
    data Free : (l : String) -> (port : Ty (PORT l)) -> Type where
      FreePort : (label : String)
              -> (use : TyRig)
              -> (contra : Not (use = None))
              -> Free (label) (TyPort label dir sense ety type use)

    used : Free l (TyPort l d s w t None) -> Void
    used (FreePort l None contra) = contra Refl

    export
    free : (label : String)
        -> (type  : Ty (PORT label))
                 -> Dec (Free label type)
    free l (TyPort l d s w t None) = No used
    free l (TyPort l d s w t One) = Yes (FreePort l One (negEqSym noneNotOne))
    free l (TyPort l d s w t Tonne) = Yes (FreePort l Tonne (negEqSym noneNotTonne))

  namespace Types

    export
    free : (type : Ty m) -> List String
    free TyLogic = Nil
    free (TyArray type length) = Nil
    free (TyStruct kvs) = Nil
    free (TyUnion kvs) = Nil
    free TyUnit = Nil
    free TyConn = Nil
    free TyGate = Nil
    free (TyPort label dir sense wty type usage) with (free label (TyPort label dir sense wty type usage))
      free (TyPort label dir sense wty type usage) | Yes (FreePort label usage contra)
        = [label]
      free (TyPort label dir sense wty type usage) | No contra
        = Nil
    free (TyModule ports) with (state Port.Free Port.free ports)
      free (TyModule ports) | (MkState ps pos ns neg division) = toList ps

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

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Compiler.Erlang.Codegen.NamedCExpToErlExpr

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Inline
import Compiler.Erlang.Name
import public Compiler.Erlang.IR.ErlExpr
import Compiler.Erlang.Codegen.NamedCExpToErlExpr.RtsSupport

import Core.Context
import Core.Name
import Core.TT

import Data.List
import Libraries.Data.NameMap
import Data.Stream
import Data.Vect

%default total

-- OPTIONS

public export
record CGOpts where
  constructor MkCGOpts
  useMutableStorage : Bool

-- CONSTANTS

genConstant : Constant -> IdrisConstant
genConstant (I x) = IInt x
genConstant (I8 x) = IInt8 x
genConstant (I16 x) = IInt16 x
genConstant (I32 x) = IInt32 x
genConstant (I64 x) = IInt64 x
genConstant (BI x) = IInteger x
genConstant (B8 x) = IB8 x
genConstant (B16 x) = IB16 x
genConstant (B32 x) = IB32 x
genConstant (B64 x) = IB64 x
genConstant (Str x) = IString x
genConstant (Ch x) = IChar x
genConstant (Db x) = IDouble x
genConstant WorldVal = IWorldVal
genConstant IntType = IIntType
genConstant Int8Type = IInt8Type
genConstant Int16Type = IInt16Type
genConstant Int32Type = IInt32Type
genConstant Int64Type = IInt64Type
genConstant IntegerType = IIntegerType
genConstant Bits8Type = IBits8Type
genConstant Bits16Type = IBits16Type
genConstant Bits32Type = IBits32Type
genConstant Bits64Type = IBits64Type
genConstant StringType = IStringType
genConstant CharType = ICharType
genConstant DoubleType = IDoubleType
genConstant WorldType = IWorldType

-- OPERATORS

precToNat : Int -> Nat
precToNat = integerToNat . cast

genBoundedInt : {auto lv : Ref LV LocalVars} -> Line -> IntKind -> ErlExpr -> Core ErlExpr
genBoundedInt l (Signed Unlimited) x = pure x
genBoundedInt l (Signed $ P n)     x = pure $ genToBoundedSignedInt l (precToNat n) x
genBoundedInt l (Unsigned n)       x = genToBoundedUnsignedInt l (precToNat n) x

genAdd : {auto lv : Ref LV LocalVars} -> Line -> Maybe IntKind -> ErlExpr -> ErlExpr -> Core ErlExpr
genAdd l (Just ty) x y = genBoundedInt l ty (EOp l "+" x y)
genAdd l _         x y = pure $ EOp l "+" x y

genSub : {auto lv : Ref LV LocalVars} -> Line -> Maybe IntKind -> ErlExpr -> ErlExpr -> Core ErlExpr
genSub l (Just ty) x y = genBoundedInt l ty (EOp l "-" x y)
genSub l _         x y = pure $ EOp l "-" x y

genMul : {auto lv : Ref LV LocalVars} -> Line -> Maybe IntKind -> ErlExpr -> ErlExpr -> Core ErlExpr
genMul l (Just ty) x y = genBoundedInt l ty (EOp l "*" x y)
genMul l _         x y = pure $ EOp l "*" x y

genDiv : {auto lv : Ref LV LocalVars} -> Line -> Maybe IntKind -> ErlExpr -> ErlExpr -> Core ErlExpr
genDiv l (Just ty) x y = genBoundedInt l ty (EOp l "div" x y)
genDiv l _         x y = pure $ EOp l "/" x y

genShl : {auto lv : Ref LV LocalVars} -> Line -> Maybe IntKind -> ErlExpr -> ErlExpr -> Core ErlExpr
genShl l (Just ty) x y = genBoundedInt l ty (EOp l "bsl" x y)
genShl l _         x y = pure $ EOp l "bsl" x y

constPrimitives : {auto lv : Ref LV LocalVars} -> Line -> ConstantPrimitives ErlExpr
constPrimitives l = MkConstantPrimitives {
    charToInt    = \k, x => pure $ genCharToInt l x
  , intToChar    = \_, x => pure $ genIntToChar l x
  , stringToInt  = \k, x => do
      int <- genStringToInteger l x
      genBoundedInt l k int
  , intToString  = \_, x => pure $ genFunCall l "erlang" "integer_to_binary" [x]
  , doubleToInt  = \k, x => genBoundedInt l k (genFunCall l "erlang" "trunc" [x])
  , intToDouble  = \_, x => pure $ genFunCall l "erlang" "float" [x]
  , intToInt     = intToInt
  }
  where
    intToInt : IntKind -> IntKind -> ErlExpr -> Core ErlExpr
    intToInt _ (Signed Unlimited) x = pure x
    intToInt (Signed m) (Signed $ P n) x =
      if P n >= m
        then pure x
        else pure $ genToBoundedSignedInt l (precToNat n) x

    -- Only if the precision of the target is greater
    -- than the one of the source, there is no need to cast.
    intToInt (Unsigned m) (Signed $ P n) x =
      if n > m
        then pure $ x
        else pure $ genToBoundedSignedInt l (precToNat n) x

    intToInt (Signed _) (Unsigned n) x = genToBoundedUnsignedInt l (precToNat n) x

    intToInt (Unsigned m) (Unsigned n) x =
      if n >= m
        then pure x
        else genToBoundedUnsignedInt l (precToNat n) x

genOp : forall arity . {auto lv : Ref LV LocalVars} -> Line -> PrimFn arity -> Vect arity ErlExpr -> Core ErlExpr
genOp l (Add ty) [x, y] = genAdd l (intKind ty) x y
genOp l (Sub ty) [x, y] = genSub l (intKind ty) x y
genOp l (Mul ty) [x, y] = genMul l (intKind ty) x y
genOp l (Div ty) [x, y] = genDiv l (intKind ty) x y -- NOTE: Is allowed to be partial
genOp l (Mod ty) [x, y] = pure $ EOp l "rem" x y -- NOTE: Is allowed to be partial
genOp l (Neg ty) [x] = pure $ genFunCall l "erlang" "-" [x]
genOp l (ShiftL ty) [x, y] = genShl l (intKind ty) x y
genOp l (ShiftR ty) [x, y] = pure $ EOp l "bsr" x y
genOp l (BAnd ty) [x, y] = pure $ EOp l "band" x y
genOp l (BOr ty) [x, y] = pure $ EOp l "bor" x y
genOp l (BXOr ty) [x, y] = pure $ EOp l "bxor" x y
genOp l (LT StringType) [x, y] = pure $ genUnicodeStringLT l x y
genOp l (LTE StringType) [x, y] = pure $ genUnicodeStringLTE l x y
genOp l (EQ StringType) [x, y] = pure $ genUnicodeStringEQ l x y
genOp l (GTE StringType) [x, y] = pure $ genUnicodeStringGTE l x y
genOp l (GT StringType) [x, y] = pure $ genUnicodeStringGT l x y
genOp l (LT ty) [x, y] = pure $ genBoolToInt l (EOp l "<" x y)
genOp l (LTE ty) [x, y] = pure $ genBoolToInt l (EOp l "=<" x y)
genOp l (EQ ty) [x, y] = pure $ genBoolToInt l (EOp l "=:=" x y)
genOp l (GTE ty) [x, y] = pure $ genBoolToInt l (EOp l ">=" x y)
genOp l (GT ty) [x, y] = pure $ genBoolToInt l (EOp l ">" x y)
genOp l StrLength [str] = pure $ genUnicodeStringLength l str
genOp l StrHead [str] = pure $ genUnicodeStringHead l str
genOp l StrTail [str] = genUnicodeStringTail l str
genOp l StrIndex [str, index] = pure $ genUnicodeStringIndex l str index
genOp l StrCons [char, str] = pure $ genUnicodeStringCons l char str
genOp l StrAppend [str1, str2] = pure $ genUnicodeStringAppend l str1 str2
genOp l StrReverse [str] = pure $ genUnicodeStringReverse l str
genOp l StrSubstr [start, len, str] = pure $ genUnicodeStringSubstr l start len str

-- `e` is Euler's number, which approximates to: 2.718281828459045
genOp l DoubleExp [x] = pure $ genFunCall l "math" "pow" [EFloat l 2.718281828459045, x] -- Base is `e`
genOp l DoubleLog [x] = pure $ genFunCall l "math" "log" [x] -- Base is `e`
genOp l DoublePow [x, y] = pure $ genFunCall l "math" "pow" [x, y]
genOp l DoubleSin [x] = pure $ genFunCall l "math" "sin" [x]
genOp l DoubleCos [x] = pure $ genFunCall l "math" "cos" [x]
genOp l DoubleTan [x] = pure $ genFunCall l "math" "tan" [x]
genOp l DoubleASin [x] = pure $ genFunCall l "math" "asin" [x]
genOp l DoubleACos [x] = pure $ genFunCall l "math" "acos" [x]
genOp l DoubleATan [x] = pure $ genFunCall l "math" "atan" [x]
genOp l DoubleSqrt [x] = pure $ genFunCall l "math" "sqrt" [x]
genOp l DoubleFloor [x] = pure $ genFunCall l "erlang" "floor" [x]
genOp l DoubleCeiling [x] = pure $ genFunCall l "erlang" "ceil" [x]

genOp l (Cast DoubleType StringType)  [x] = pure $ genDoubleToString l x
genOp l (Cast CharType StringType)    [x] = pure $ genCharToString l x
genOp l (Cast StringType DoubleType)  [x] = genStringToDouble l x

genOp l (Cast from to)                [x] = castInt (constPrimitives l) from to x

genOp l BelieveMe [_, _, x] = pure $ x
genOp l Crash [_, msg] = do
  let crashMsg = EBinaryConcat l (EBinary l "Crash: ") msg
  pure $ genThrowBinary l crashMsg

-- DATA CONSTRUCTORS

genCon : {auto lv : Ref LV LocalVars} -> NamespaceInfo -> Line -> Name -> List ErlExpr -> Core ErlExpr
genCon namespaceInfo l name args = do
  let (NS ns (UN (Basic n))) = name
    | _ => pure $ ECon l (constructorName name) args
  case (unsafeUnfoldNamespace ns, n, args) of
    -- List
    (["Basics", "Prelude"], "Nil", []) =>
      pure $ ENil l
    (["Basics", "Prelude"], "::", [x, xs]) =>
      pure $ ECons l x xs
    -- ErlAtom
    (["Types", "Erlang"], "MkAtom", [x]) =>
      pure $ genUnsafeStringToAtom l x
    -- ErlCharlist
    (["Types", "Erlang"], "MkCharlist", [x]) =>
      pure $ genFunCall l "unicode" "characters_to_list" [x]
    -- ErlNil
    (["MaybeImproperList", "Types", "Erlang"], "Nil", []) =>
      pure $ ENil l
    -- ErlCons
    (["MaybeImproperList", "Types", "Erlang"], "::", [x, y]) =>
      pure $ ECons l x y
    -- ErlList
    (["ProperList", "Types", "Erlang"], "Nil", []) =>
      pure $ ENil l
    (["ProperList", "Types", "Erlang"], "::", [x, xs]) =>
      pure $ ECons l x xs
    -- ErlTuple/A
    (["Types", "Erlang"], "MkTuple0", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple1", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple2", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple3", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple4", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple5", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple6", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple7", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple8", args) => pure $ ETuple l args
    -- ErlFun/A
    (["Types", "Erlang"], "MkFun0", [fun]) => genUncurry l 0 id fun
    (["Types", "Erlang"], "MkFun1", [fun]) => genUncurry l 1 id fun
    (["Types", "Erlang"], "MkFun2", [fun]) => genUncurry l 2 id fun
    (["Types", "Erlang"], "MkFun3", [fun]) => genUncurry l 3 id fun
    (["Types", "Erlang"], "MkFun4", [fun]) => genUncurry l 4 id fun
    (["Types", "Erlang"], "MkFun5", [fun]) => genUncurry l 5 id fun
    (["Types", "Erlang"], "MkFun6", [fun]) => genUncurry l 6 id fun
    (["Types", "Erlang"], "MkFun7", [fun]) => genUncurry l 7 id fun
    (["Types", "Erlang"], "MkFun8", [fun]) => genUncurry l 8 id fun
    -- ErlIOFun/A
    (["Types", "Erlang"], "MkIOFun0", [fun]) => genUncurry l 0 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun1", [fun]) => genUncurry l 1 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun2", [fun]) => genUncurry l 2 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun3", [fun]) => genUncurry l 3 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun4", [fun]) => genUncurry l 4 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun5", [fun]) => genUncurry l 5 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun6", [fun]) => genUncurry l 6 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun7", [fun]) => genUncurry l 7 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun8", [fun]) => genUncurry l 8 (genUnsafePerformIO namespaceInfo l) fun
    -- Default
    _ =>
      pure $ ECon l (constructorName name) args

-- DATA DECONSTRUCTORS

argsToErlMatchers : (args : List LocalVar) -> List (LocalVar, ErlMatcher)
argsToErlMatchers xs = map (\arg => (arg, MAny)) xs

readConAltFun : {auto lv : Ref LV LocalVars} -> Line -> (arity : Nat) -> (funVar : LocalVar) -> ErlExpr -> (transform : ErlExpr -> ErlExpr) -> Core ErlMatcher
readConAltFun l arity funVar body transform = do
  tempVar <- newLocalVar
  let curriedFunMatcher = MTransform MAny tempVar !(genCurry l arity transform (ELocal l tempVar))
  pure $ MTransform curriedFunMatcher funVar body

readConAlt : {auto lv : Ref LV LocalVars} -> {auto cgOpts : CGOpts} -> NamespaceInfo -> Line -> Name -> (args : List LocalVar) -> ErlExpr -> Core ErlMatcher
readConAlt namespaceInfo l name args body = do
  let NS ns (UN (Basic n)) = name
    | _ => pure $ MTaggedTuple (constructorName name) args body
  case (unsafeUnfoldNamespace ns, n, args) of
    -- List
    (["Basics", "Prelude"], "Nil", []) =>
      pure $ MConst MNil body
    (["Basics", "Prelude"], "::", [xVar, xsVar]) =>
      pure $ MCons MAny MAny xVar xsVar body
    -- ErlAtom
    (["Types", "Erlang"], "MkAtom", [xVar]) => do
      tempVar <- newLocalVar
      let convertAtomMatcher = MTransform MAny tempVar (genAtomToString l (ELocal l tempVar))
      pure $ MTransform convertAtomMatcher xVar body
    -- ErlCharlist
    (["Types", "Erlang"], "MkCharlist", [xVar]) => do
      tempVar <- newLocalVar
      let convertCharlistMatcher = MTransform MAny tempVar (genFunCall l "unicode" "characters_to_binary" [ELocal l tempVar])
      pure $ MTransform convertCharlistMatcher xVar body
    -- ErlNil
    (["MaybeImproperList", "Types", "Erlang"], "Nil", []) =>
      pure $ MConst MNil body
    -- ErlCons
    (["MaybeImproperList", "Types", "Erlang"], "::", [xVar, yVar]) =>
      pure $ MCons MAny MAny xVar yVar body
    -- ErlList
    (["ProperList", "Types", "Erlang"], "Nil", []) =>
      pure $ MConst MNil body
    (["ProperList", "Types", "Erlang"], "::", [xVar, xsVar]) =>
      pure $ MCons MAny MAny xVar xsVar body
    -- ErlTuple/A
    (["Types", "Erlang"], "MkTuple0", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple1", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple2", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple3", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple4", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple5", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple6", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple7", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple8", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    -- ErlFun/A
    (["Types", "Erlang"], "MkFun0", [funVar]) =>
      readConAltFun l 0 funVar body id
    (["Types", "Erlang"], "MkFun1", [funVar]) =>
      readConAltFun l 1 funVar body id
    (["Types", "Erlang"], "MkFun2", [funVar]) =>
      readConAltFun l 2 funVar body id
    (["Types", "Erlang"], "MkFun3", [funVar]) =>
      readConAltFun l 3 funVar body id
    (["Types", "Erlang"], "MkFun4", [funVar]) =>
      readConAltFun l 4 funVar body id
    (["Types", "Erlang"], "MkFun5", [funVar]) =>
      readConAltFun l 5 funVar body id
    (["Types", "Erlang"], "MkFun6", [funVar]) =>
      readConAltFun l 6 funVar body id
    (["Types", "Erlang"], "MkFun7", [funVar]) =>
      readConAltFun l 7 funVar body id
    (["Types", "Erlang"], "MkFun8", [funVar]) =>
      readConAltFun l 8 funVar body id
    -- ErlIOFun/A
    (["Types", "Erlang"], "MkIOFun0", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 0 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun1", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 1 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun2", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 2 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun3", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 3 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun4", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 4 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun5", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 5 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun6", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 6 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun7", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 7 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun8", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 8 funVar body (genMkIO l worldVal)
    _ =>
      pure $ MTaggedTuple (constructorName name) args body

-- EXTERNAL PRIMITIVES

genDecode : {auto lv : Ref LV LocalVars} -> Line -> ErlExpr -> ErlMatcher -> Core ErlExpr
genDecode l term matcher = do
  tempVar <- newLocalVar
  pure $ EMatcherCase l
    term
    (singleton $ MTransform matcher tempVar (genJust l (ELocal l tempVar)))
    (Just $ genNothing l)

genDecodeTuple : {auto lv : Ref LV LocalVars} -> Line -> ErlExpr -> (arity : Nat) -> Core ErlExpr
genDecodeTuple l term arity = do
  args <- newLocalVars arity
  genDecode l term $ MTuple (argsToErlMatchers args) (ETuple l (map (ELocal l) args))

genExtPrim : {auto lv : Ref LV LocalVars} -> {auto cgOpts : CGOpts} -> NamespaceInfo -> Line -> Name -> List ErlExpr -> Core ErlExpr
genExtPrim namespaceInfo l (NS _ (UN (Basic "void"))) [_, _] =
  pure $ genThrowMsg l "Error: Executed 'void'"
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__os"))) [] =
  genOsType l
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__codegen"))) [] =
  pure $ EBinary l "erlang"
genExtPrim {cgOpts} namespaceInfo l (NS _ (UN (Basic "prim__newIORef"))) [_, val, world] = do
  expr <- if cgOpts.useMutableStorage
    then pure $ genFunCall l "mutable_storage" "term_new" [val]
    else do
      refVar <- newLocalVar
      pure $ genMkIORes l $ genProcessDictNewIORef l refVar val
  pure $ genMkIORes l expr
genExtPrim {cgOpts} namespaceInfo l (NS _ (UN (Basic "prim__readIORef"))) [_, mutableRef, world] = do
  let expr = if cgOpts.useMutableStorage
        then genFunCall l "mutable_storage" "term_get" [mutableRef]
        else genProcessDictReadIORef l mutableRef
  pure $ genMkIORes l expr
genExtPrim {cgOpts} namespaceInfo l (NS _ (UN (Basic "prim__writeIORef"))) [_, mutableRef, newVal, world] = do
  let expr = if cgOpts.useMutableStorage
        then genFunCall l "mutable_storage" "term_set" [mutableRef, newVal]
        else genProcessDictWriteIORef l mutableRef newVal
  pure $ genMkIORes l expr
genExtPrim {cgOpts} namespaceInfo l (NS _ (UN (Basic "prim__freeIORef"))) [_, mutableRef, world] = do
  let expr = genProcessDictFreeIORef l mutableRef
  pure $ genMkIORes l expr
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlUnsafeCall"))) [_, ret, modName, fnName, args] = do
  pure $ genFunCall l "erlang" "apply" [genUnsafeStringToAtom l modName, genUnsafeStringToAtom l fnName, args]
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlTryCatch"))) [_, action, world] = do
  okVar <- newLocalVar
  errorVar <- newLocalVar
  let actionExpr = genUnsafePerformIO namespaceInfo l action
  let body = ETryCatch l actionExpr okVar (genRight l (ELocal l okVar)) errorVar (genLeft l (ELocal l errorVar))
  pure $ genMkIORes l body
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlReceive"))) [timeout, world] = do
  tempVar <- newLocalVar
  let receive = EReceive l [MTransform MAny tempVar (genJust l (ELocal l tempVar))] timeout (genNothing l)
  pure $ genMkIORes l receive
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlModule"))) [] =
  pure $ EAtom l (currentModuleName namespaceInfo)
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlMatchExact"))) [x, y] =
  pure $ genBoolToInt l (EOp l "=:=" x y)
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeCodepoint"))) [term] =
  genDecode l term MCodepoint
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeInteger"))) [term] =
   genDecode l term MInteger
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeDouble"))) [term] =
  genDecode l term MFloat
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeAtom"))) [term] =
  genDecode l term MAtom
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeBinary"))) [term] =
  genDecode l term MBinary
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodePid"))) [term] =
  genDecode l term MPid
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erldecodeReference"))) [term] =
  genDecode l term MRef
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodePort"))) [term] =
  genDecode l term MPort
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeAnyMap"))) [term] =
  genDecode l term MMap
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeAnyList"))) [term] =
  genDecode l term MAnyList
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeNil"))) [term] =
  genDecode l term MNil
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeCons"))) [term] = do
  hdVar <- newLocalVar
  tlVar <- newLocalVar
  genDecode l term $ MCons MAny MAny hdVar tlVar (ECons l (ELocal l hdVar) (ELocal l tlVar))
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeTuple0"))) [term] =
  genDecodeTuple l term 0
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeTuple1"))) [term] =
  genDecodeTuple l term 1
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeTuple2"))) [term] =
  genDecodeTuple l term 2
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeTuple3"))) [term] =
  genDecodeTuple l term 3
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeTuple4"))) [term] =
  genDecodeTuple l term 4
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeTuple5"))) [term] =
  genDecodeTuple l term 5
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeTuple6"))) [term] =
  genDecodeTuple l term 6
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeTuple7"))) [term] =
  genDecodeTuple l term 7
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeTuple8"))) [term] =
  genDecodeTuple l term 8
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeFun0"))) [term] =
  genDecode l term (MFun 0)
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeFun1"))) [_, term] =
  genDecode l term (MFun 1)
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeFun2"))) [_, _, term] =
  genDecode l term (MFun 2)
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeFun3"))) [_, _, _, term] =
  genDecode l term (MFun 3)
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeFun4"))) [_, _, _, _, term] =
  genDecode l term (MFun 4)
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeFun5"))) [_, _, _, _, _, term] =
  genDecode l term (MFun 5)
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeFun6"))) [_, _, _, _, _, _, term] =
  genDecode l term (MFun 6)
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeFun7"))) [_, _, _, _, _, _, _, term] =
  genDecode l term (MFun 7)
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlDecodeFun8"))) [_, _, _, _, _, _, _, _, term] =
  genDecode l term (MFun 8)
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferNew"))) [size] =
  pure $ EBufferNew l size
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferResize"))) [bin, newSize] =
  pure $ EBufferResize l bin newSize
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferFlatten"))) [bin, maxbytes] =
  pure $ EBufferFlatten l bin maxbytes
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferSetByte"))) [bin, loc, value] =
  pure $ EBufferSetBits8 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferGetByte"))) [bin, loc] =
  pure $ EBufferGetBits8 l bin loc
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferSetBits8"))) [bin, loc, value] =
  pure $ EBufferSetBits8 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferGetBits8"))) [bin, loc] =
  pure $ EBufferGetBits8 l bin loc
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferSetBits16"))) [bin, loc, value] =
  pure $ EBufferSetBits16 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferGetBits16"))) [bin, loc] =
  pure $ EBufferGetBits16 l bin loc
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferSetBits32"))) [bin, loc, value] =
  pure $ EBufferSetBits32 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferGetBits32"))) [bin, loc] =
  pure $ EBufferGetBits32 l bin loc
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferSetBits64"))) [bin, loc, value] =
  pure $ EBufferSetBits64 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferGetBits64"))) [bin, loc] =
  pure $ EBufferGetBits64 l bin loc
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferSetInt32"))) [bin, loc, value] =
  pure $ EBufferSetInt32 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferGetInt32"))) [bin, loc] =
  pure $ EBufferGetInt32 l bin loc
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferSetInt64"))) [bin, loc, value] =
  pure $ EBufferSetInt64 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferGetInt64"))) [bin, loc] =
  pure $ EBufferGetInt64 l bin loc
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferSetDouble"))) [bin, loc, value] =
  pure $ EBufferSetDouble l bin loc value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferGetDouble"))) [bin, loc] =
  pure $ EBufferGetDouble l bin loc
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferSetString"))) [bin, loc, value] =
  pure $ EBufferSetString l bin loc value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__erlBufferGetString"))) [bin, loc, len] =
  pure $ EBufferGetString l bin loc len
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__newBuilder"))) [] =
  pure $ EBinary l ""
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__builderToByteString"))) [builder] =
  pure $ builder
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__byteStringToIterator"))) [str] =
  pure $ str
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__freeIterator"))) [it] =
  pure $ genMkUnit l
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__writeInt8"))) [value, builder] =
  pure $ ESerialiseWriteInt 8 l builder value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__readInt8"))) [it] =
  pure $ ESerialiseReadInt 8 l it
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__writeInt16"))) [value, builder] =
  pure $ ESerialiseWriteInt 16 l builder value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__readInt16"))) [it] =
  pure $ ESerialiseReadInt 16 l it
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__writeInt32"))) [value, builder] =
  pure $ ESerialiseWriteInt 32 l builder value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__readInt32"))) [it] =
  pure $ ESerialiseReadInt 32 l it
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__writeInt64"))) [value, builder] =
  pure $ ESerialiseWriteInt 64 l builder value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__readInt64"))) [it] =
  pure $ ESerialiseReadInt 64 l it
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__writeBits8"))) [value, builder] =
  pure $ ESerialiseWriteBits 8 l builder value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__readBits8"))) [it] =
  pure $ ESerialiseReadBits 8 l it
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__writeBits16"))) [value, builder] =
  pure $ ESerialiseWriteBits 16 l builder value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__readBits16"))) [it] =
  pure $ ESerialiseReadBits 16 l it
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__writeBits32"))) [value, builder] =
  pure $ ESerialiseWriteBits 32 l builder value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__readBits32"))) [it] =
  pure $ ESerialiseReadBits 32 l it
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__writeBits64"))) [value, builder] =
  pure $ ESerialiseWriteBits 64 l builder value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__readBits64"))) [it] =
  pure $ ESerialiseReadBits 64 l it
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__writeString"))) [value, builder] =
  pure $ ESerialiseWriteBinary l builder value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__readString"))) [it] =
  pure $ ESerialiseReadBinary l it
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__writeChar"))) [value, builder] =
  pure $ ESerialiseWriteChar l builder value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__readChar"))) [it] =
  pure $ ESerialiseReadChar l it
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__writeDouble"))) [value, builder] =
  pure $ ESerialiseWriteDouble l builder value
genExtPrim namespaceInfo l (NS _ (UN (Basic "prim__readDouble"))) [it] =
  pure $ ESerialiseReadDouble l it

-- genExtPrim namespaceInfo l name args =
--   throw (InternalError ("Badly formed external primitive " ++ show name))
genExtPrim namespaceInfo l name args =
  pure $ genThrowMsg l ("Error: Badly formed external primitive " ++ show name) -- TODO: Should fail at compile-time instead

-- %FOREIGN PRIMITIVES

genForeign : {auto lv : Ref LV LocalVars} -> NamespaceInfo -> Line -> Name -> List ErlExpr -> Core ErlExpr
genForeign namespaceInfo l (NS _ (UN (Basic "prim__putStr"))) [arg, world] = do
  let putStrCall = genUnicodePutStr l arg
  let retVal = genMkIORes l (genMkUnit l)
  pure $ ESequence l (putStrCall ::: [retVal])
genForeign namespaceInfo l (NS _ (UN (Basic "prim__getStr"))) [world] = do
  let getStrCall = genUnicodeGetStr l (ECharlist l "")
  pure $ genMkIORes l getStrCall
genForeign namespaceInfo l (NS _ (UN (Basic "fastPack"))) [xs] = do
  pure $ genFunCall l "unicode" "characters_to_binary" [xs]
genForeign namespaceInfo l (NS _ (UN (Basic "fastUnpack"))) [str] = do
  pure $ genFunCall l "string" "to_graphemes" [str]
genForeign namespaceInfo l (NS _ (UN (Basic "fastConcat"))) [xs] = do
  pure $ genFunCall l "unicode" "characters_to_binary" [xs] -- TODO: Can this be improved?
-- genForeign namespaceInfo l name args =
--   throw (InternalError ("Unsupported %foreign primitive " ++ show name))
genForeign namespaceInfo l name args =
  pure $ genThrowMsg l ("Error: Unsupported %foreign primitive " ++ show name) -- TODO: Should fail at compile-time instead

-- CODE GENERATION

mutual
  export
  genNmExp : {auto lv : Ref LV LocalVars} -> {auto cgOpts : CGOpts} -> NamespaceInfo -> NameMap LocalVar -> NamedCExp -> Core ErlExpr
  genNmExp namespaceInfo vs (NmLocal fc name) = do
    let l = genFC fc
    let Just var = lookup name vs
      | Nothing => throw (InternalError ("Missing variable name: " ++ show name))
    pure $ ELocal l var
  genNmExp namespaceInfo vs (NmRef fc name) = do
    let l = genFC fc
    pure $ genRef namespaceInfo l name
  genNmExp namespaceInfo vs (NmLam fc x body) = do
    let l = genFC fc
    (vs', vars) <- addLocalVars [x] vs
    body' <- genNmExp namespaceInfo vs' body
    pure $ ELam l vars body'
  genNmExp namespaceInfo vs (NmLet fc x val body) = do
    let l = genFC fc
    val' <- genNmExp namespaceInfo vs val
    (vs', xVar) <- addLocalVar x vs
    body' <- genNmExp namespaceInfo vs' body
    pure $ ELet l xVar val' body'
  genNmExp namespaceInfo vs (NmApp fc x args) = do
    let l = genFC fc
    args' <- assert_total $ traverse (genNmExp namespaceInfo vs) args
    pure $ EApp l !(genNmExp namespaceInfo vs x) args'
  genNmExp namespaceInfo vs (NmCon fc name ci tag args) = do
    let l = genFC fc
    args' <- assert_total $ traverse (genNmExp namespaceInfo vs) args
    genCon namespaceInfo l name args'
  genNmExp namespaceInfo vs (NmOp fc op args) = do
    let l = genFC fc
    args' <- assert_total $ traverseVect namespaceInfo vs args
    genOp l op args'
  genNmExp namespaceInfo vs (NmExtPrim fc name args) = do
    let l = genFC fc
    args' <- assert_total $ traverse (genNmExp namespaceInfo vs) args
    genExtPrim namespaceInfo l name args'
  genNmExp namespaceInfo vs (NmForce fc lr t) = do
    let l = genFC fc
    pure $ EApp l !(genNmExp namespaceInfo vs t) []
  genNmExp namespaceInfo vs (NmDelay fc lr t) = do
    let l = genFC fc
    pure $ ELam l [] !(genNmExp namespaceInfo vs t)
  genNmExp namespaceInfo vs (NmConCase fc sc [] def) =
    throw $ InternalError "ConCase has no clauses"
  genNmExp namespaceInfo vs (NmConCase fc sc (x :: xs) def) = do
    let l = genFC fc
    sc' <- genNmExp namespaceInfo vs sc
    alts' <- assert_total $ traverseList1 (genConAlt namespaceInfo vs l) (x ::: xs)
    def' <- assert_total $ traverseOpt (genNmExp namespaceInfo vs) def
    pure $ EMatcherCase l sc' alts' def'
  genNmExp namespaceInfo vs (NmConstCase fc sc [] def) =
    throw $ InternalError "ConstCase has no clauses"
  genNmExp namespaceInfo vs (NmConstCase fc sc (x :: xs) def) = do
    let l = genFC fc
    sc' <- genNmExp namespaceInfo vs sc
    alts' <- assert_total $ traverseList1 (genConstAlt namespaceInfo vs) (x ::: xs)
    def' <- assert_total $ traverseOpt (genNmExp namespaceInfo vs) def
    pure $ EConstCase l sc' alts' def'
  genNmExp namespaceInfo vs (NmPrimVal fc c) = do
    let l = genFC fc
    pure $ EIdrisConstant l (genConstant c)
  genNmExp namespaceInfo vs (NmErased fc) = do
    let l = genFC fc
    pure $ EAtom l "erased"
  genNmExp namespaceInfo vs (NmCrash fc msg) = do
    let l = genFC fc
    pure $ genThrowMsg l msg

  traverseVect : {auto lv : Ref LV LocalVars} -> {auto cgOpts : CGOpts} -> NamespaceInfo -> NameMap LocalVar -> Vect n NamedCExp -> Core (Vect n ErlExpr)
  traverseVect namespaceInfo vs [] = pure []
  traverseVect namespaceInfo vs (arg :: args) = pure $ !(genNmExp namespaceInfo vs arg) :: !(traverseVect namespaceInfo vs args)

  genConAlt : {auto lv : Ref LV LocalVars} -> {auto cgOpts : CGOpts} -> NamespaceInfo -> NameMap LocalVar -> Line -> NamedConAlt -> Core ErlMatcher
  genConAlt namespaceInfo vs l (MkNConAlt name ci tag args body) = do
    (vs', vars) <- addLocalVars args vs
    readConAlt namespaceInfo l name vars !(genNmExp namespaceInfo vs' body)

  genConstAlt : {auto lv : Ref LV LocalVars} -> {auto cgOpts : CGOpts} -> NamespaceInfo -> NameMap LocalVar -> NamedConstAlt -> Core ErlConstAlt
  genConstAlt namespaceInfo vs (MkNConstAlt constant body) =
    pure $ MkConstAlt (genConstant constant) !(genNmExp namespaceInfo vs body)

-- DEFINITIIONS

export
genDef : {auto cgOpts : CGOpts} -> NamespaceInfo -> Line -> Name -> NamedDef -> Core (Maybe ErlFunDecl)
genDef namespaceInfo l name (MkNmFun args body) = do
  lv <- newRef LV (initLocalVars "V")
  let (modName, fnName) = moduleNameFunctionName namespaceInfo name
  (vs, vars) <- addLocalVars args empty
  let funDecl = MkFunDecl l Public fnName vars !(genNmExp namespaceInfo vs body)
  pure $ Just funDecl
genDef namespaceInfo l name (MkNmCon tag arity nt) =
  pure Nothing
genDef namespaceInfo l name (MkNmForeign cs args ret) = do
  lv <- newRef LV (initLocalVars "V")
  let (modName, fnName) = moduleNameFunctionName namespaceInfo name
  vars <- newLocalVars (length args)
  let funDecl = MkFunDecl l Public fnName vars !(genForeign namespaceInfo l name (map (ELocal l) vars))
  pure $ Just funDecl
genDef namespaceInfo l name (MkNmError body) = do
  lv <- newRef LV (initLocalVars "V")
  let (modName, fnName) = moduleNameFunctionName namespaceInfo name
  let funDecl = MkFunDecl l Private fnName [] !(genNmExp namespaceInfo empty body)
  pure $ Just funDecl

-- EXPORTS

data InternalArity = Value | Arity Nat

internalArity : NamedCExp -> InternalArity
internalArity (NmCon fc (NS ns (UN (Basic n))) _ _ _) =
  if ns == erlangTypesNS
    then case n of
      "ETFun" => Arity 1
      "ETErlFun0" => Arity 0
      "ETErlFun1" => Arity 1
      "ETErlFun2" => Arity 2
      "ETErlFun3" => Arity 3
      "ETErlFun4" => Arity 4
      "ETErlFun5" => Arity 5
      "ETErlFun6" => Arity 6
      "ETErlFun7" => Arity 7
      "ETErlFun8" => Arity 8
      "ETErlIOFun0" => Arity 0
      "ETErlIOFun1" => Arity 1
      "ETErlIOFun2" => Arity 2
      "ETErlIOFun3" => Arity 3
      "ETErlIOFun4" => Arity 4
      "ETErlIOFun5" => Arity 5
      "ETErlIOFun6" => Arity 6
      "ETErlIOFun7" => Arity 7
      "ETErlIOFun8" => Arity 8
      _ => Value
    else Value
internalArity _ = Value

externalArity : InternalArity -> Nat
externalArity Value = 0
externalArity (Arity arity) = arity

-- TODO: Do not require name of exported function to be a static string?
export
readExports : NamespaceInfo -> Line -> NamedCExp -> Core (List ErlFunDecl)
readExports namespaceInfo l tm = do
  case tm of
    NmCon fc (NS ns (UN (Basic "Fun"))) ci tag [exprTy, NmPrimVal _ (Str fnName), expr] => do
      let True = ns == erlangIONS
        | False => throw (InternalError ("Invalid export: " ++ show tm))
      lv <- newRef LV (initLocalVars "V")
      body <- genNmExp namespaceInfo empty expr -- NOTE: Vars are not relevant to `body`
      let intArity = internalArity exprTy
      let extArity = externalArity intArity
      vars <- newLocalVars extArity
      let invokedBody =
          case intArity of
            Value => body
            Arity arity => EApp l body (genArgsToLocals l vars)
      let funDecl = MkFunDecl l Public fnName vars invokedBody
      pure $ [funDecl]
    NmCon fc (NS ns (UN (Basic "Combine"))) ci tag [exports1, exports2] => do
      let True = ns == erlangIONS
        | False => throw (InternalError ("Invalid export: " ++ show tm))
      pure $ !(readExports namespaceInfo l exports1) ++ !(readExports namespaceInfo l exports2)
    _ =>
      throw (InternalError ("Invalid export: " ++ show tm))


text:
import Data.List.Views

-- total
isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1, snocList input2)
  isSuffix _ _ | (Snoc x xs xsrec, Snoc y ys ysrec)
     = (x == y) && (isSuffix _ _ | (xsrec, ysrec))
  isSuffix _ _ | (Empty, s) = True
  isSuffix _ _ | (s, Empty) = False


text:
||| Heap (aka. Priority Queue) data structure.
|||
||| A _Heap_ provides an efficient way to store a bunch of `Ord`ered
||| elements in such a way that it's easy to retrieve the minimum
||| element. It's a basic data structure to implement classical graph
||| algorithms like [A*](https://en.wikipedia.org/wiki/A*_search_algorithm).
|||
||| We provide a single implementation called _Binomial Heaps_ from
||| Okasaki's [Purely Functional Data Structures](https://www.cs.cmu.edu/~rwh/theses/okasaki.pdf)
||| but the interface can of course be easily implemented by other
||| data structures
module Data.Heap

||| Interface to Heap/Priority Queue
public export
interface Heap (heap : Type -> Type) where

  ||| Create a new, empty `Heap`
  empty : heap a

  ||| Test whether or not given `heap` is empty
  isEmpty : (q : heap a) -> Bool

  ||| Insert given element into the heap
  ||| @elem the element to insert. Must implement `Ord` interface
  ||| @q the heap to insert element into
  ||| @return a new heap with element inserted. If `elem` is the
  ||| smallest element in the heap, then it's inserted at its top
  push : (Ord a) => (elem : a) -> (q : heap a) -> heap a

  ||| Try to find the mininal element of the heap
  ||| @q the heap to peek at
  ||| @return Nothing if the heap is empty, or the minimal element
  ||| otherwise.
  peek : (Ord a) => (q : heap a) -> Maybe a

  ||| Try to pop the minimal element off the heap.
  ||| @q the heap to pop from
  ||| @return the updated heap and the minimal element. If the
  ||| second element of the pair is Nothing then the returned
  ||| heap is the unmodified `q`
  pop : (Ord a) => (q : heap a) -> (heap a, Maybe a)

  ||| Merge to heaps, restructuring their elements to respect
  ||| the ordering.
  ||| @q first heap to merge
  ||| @q' second heap to merge
  ||| @return a new heap containing all elements of `q` and `q'`
  ||| in correct order
  merge : (Ord a) => (q : heap a) -> (q' : heap a) -> heap a

  ||| Extract statistics form the `heap` for debugging purpose
  |||
  ||| This interface is kind of uninteresting and is just a stop-gap solution,
  ||| it needs to be refactored to produce some real statistics data, like the
  ||| number of operations done so far on this heap and possibly their timing.
  stats : (Show a) => heap a -> Maybe String

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Main

import Test.Golden

prefixFolder : String -> List String -> List String
prefixFolder pref paths = map ((pref ++ "/") ++) paths

tests : TestPool
tests = MkTestPool "Tests" [] Nothing ["uri"]

main : IO ()
main = runner [ tests ]

max_stars_repo_name: felipegchi/sayURI

max_issues_repo_name: felipegchi/sayURI

max_forks_repo_name: felipegchi/sayURI


text:
module AssRecRule

import Data.Fin
import Data.Vect
%default total
%access public export

{-
 The recursion function for lists of type `a`. Define this by pattern matching
-}
recList : (a: Type) ->  (x: Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)
recList a x base step [] = base
recList a x base step (y :: xs) = (step y xs previous) where
  previous = recList a x base step xs

{-
Given a list of type `a` and a function `f: a -> b` get a list of type `b`
by applying `f` to each element.
Note: Define using `recList` and without pattern matching on lists.
-}
mapList : (a: Type) -> (b: Type) -> (f: a -> b) -> List a -> List b
mapList a b f = recList a (List b) [] step where
  step = \y:a => \xs:(List a)  => \blist:(List b) => (f(y)::blist)

{-
Given a list of type `a`, an initial value `init: a` and an operation `op: a -> a -> a`,
get an element of `a` by starting with init and repeatedly applying the elements of the
list,
e.g. fold Nat 1 (*) ([22] :: [3] :: [])  = 1 * 22 * 3
Note: Define using `recList` and without pattern matching on lists.
-}

|||The way I have defined foldList, if init =p and list is [q,r], it will return
|||op((op(p,r)),q).
foldList : (a: Type) ->  (init: a) -> (op : a -> a -> a) -> List a -> a
foldList a init op = recList a a init step where
  step = \y:a => \xs:(List a) => \previous:a => (op previous y)

{-
The induction function on the `Fin` indexed type family. Define this by pattern matching.
-}
inducFin : (xs : (n: Nat) -> Fin n -> Type) ->
  (base : (m: Nat) -> xs (S m) FZ) ->
  (step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))) ->
  (q: Nat) -> (j: Fin q) -> xs q j
inducFin xs base step (S k) FZ = base  k
inducFin xs base step (S k) (FS x) = step k x (inducFin xs base step k x)

{-
Given a type `a`, a natural number `q`, an element `j : Fin q` and a vector `v` of length q with entries of type `a`,
get the element in position `j` of `v`. Note that this is always well defined.

Note: Define using `inducList` and without pattern matching on the `Fin` family. You may pattern match on Vectors.
The definition should have only one case, and there should be no case splitting on `Fin`.
-}

|||Specifies the output type for fetchelem
outTypeFetchElem: (a:Type) ->(n:Nat) -> Fin n -> Type
outTypeFetchElem a n x = (Vect n a ->a)

baseFetchElem : (m : Nat) -> Vect (S m) a -> a
baseFetchElem m (x :: xs) = x

stepFetchElem : (p : Nat) -> Fin p -> (Vect p a -> a) -> Vect (S p) a -> a
stepFetchElem p x f (y :: xs) = f (xs)

fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)
fetchElem a   = inducFin (outTypeFetchElem a) baseFetchElem stepFetchElem


text:
module Main

import Data.Vect

emptyString : String
emptyString = ""

helloWorld : String
helloWorld = "hello world!"

spaceOnly : String
spaceOnly = " "

tabOnly : String
tabOnly =  "\t"

linebreakOnly : String
linebreakOnly = "\n"

all : Vect 5 String
all =
  [ emptyString
  , helloWorld
  , spaceOnly
  , tabOnly
  , linebreakOnly
  ]

lengthAll : Nat
lengthAll = Strings.length $ foldl (++) (head all) (tail all)

sumOfAllLengths : Nat
sumOfAllLengths = foldl (\ l, s => l + (Strings.length s)) (Strings.length $ head all) (tail all)

main : IO ()
main = do putStrLn $ "length of: '" ++ emptyString ++ "' is: " ++ (show $ length emptyString)
          putStrLn $ "length of: '" ++ helloWorld ++ "' is: " ++ (show $ length helloWorld)
          putStrLn $ "length of: '" ++ spaceOnly ++ "' is: " ++ (show $ length spaceOnly)
          putStrLn $ "length of: '" ++ tabOnly ++ "' is: " ++ (show $ length tabOnly)
          putStrLn $ "length of: '" ++ linebreakOnly ++ "' is: " ++ (show $ length linebreakOnly)
          putStrLn $ "length of all matches sum of all lengths: " ++ (show $ lengthAll == sumOfAllLengths)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Python.Telescope

import public Data.Erased

%default total
%access public export

data Binder : (argTy : Type) -> (depTy : Type) -> (argTy -> depTy) -> Type where
  ||| Relevant, mandatory, positional argument.
  Pi : (a : Type) -> Binder a a Basics.id

  ||| Erased, mandatory, positional argument.
  Forall : (a : Type) -> Binder (Erased a) (Erased a) Basics.id

  ||| An argument with a default value.
  Default : (a : Type) -> (d : a) -> Binder (Maybe a) a (fromMaybe d)

||| Type of sequences where the value of any element may affect
||| the type of the following elements.
|||
||| In other words, a dependent pair generalised to multiple elements.
data Telescope : Type -> Type where

  ||| Empty telescope.
  Return : Type -> Telescope Unit

  ||| Value on which subsequent types may depend.
  Bind :
    (bnd : Binder argTy depTy fromArg)
    -> {b : depTy -> Type}
    -> (tf : (x : depTy) -> Telescope (b x))
    -> Telescope (DPair argTy (b . fromArg))

term syntax "pi" {x} ":" [t] "." [rhs]
  = Bind (Pi t) (\x : t => rhs);

term syntax "forall" {x} ":" [t] "." [rhs]
  = Bind (Forall t) (\ex : Erased t => let x = unerase ex in rhs);

term syntax "default" {x} ":" [t] "=" [dflt] "." [rhs]
  = Bind (Default t dflt) (\x : t => rhs);

namespace DPairSugar
  Nil : Type
  Nil = Unit

  (::) : Type -> Type -> Type
  (::) a b = DPair a (const b)

namespace TupleSugar
  ||| Alternative name for `MkUnit`, useful for the [list, syntax, sugar].
  Nil : Unit
  Nil = ()

  ||| Infix name for `MkDPair`, useful for the [list, syntax, sugar].
  (::) : (x : a) -> (y : b x) -> DPair a b
  (::) = MkDPair

||| Convert a list of types to the corresponding tuple type.
toTuple : (xs : List Type) -> Type
toTuple [] = Unit
toTuple (x :: xs) = DPair x (const $ toTuple xs)

||| Convert a list of types to the corresponding simple telescope.
simple : (xs : List Type) -> (ret : Type) -> Telescope (toTuple xs)
simple []        ret = Return ret
simple (a :: as) ret = Bind (Pi a) (\x => simple as ret)

retTy : (t : Telescope a) -> (args : a) -> Type
retTy (Return x) () = x
retTy (Bind {fromArg = fromArg} bnd tf) (MkDPair x xs) = retTy (tf $ fromArg x) xs

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Parity

{- conversion

plus 3 4
\k => plus k 0
\k => plus Z k
\k,m => plus (S k) m
\k:Nat => 0+k
\k:Nat => k+0
\k => Z + k

-}

data Parity : Nat -> Type where
   Even : Parity (n + n)
   Odd  : Parity (S (n + n))

{-
l1: Parity (S (plus j (S j))) -> Parity (S (S (plus j j)))
....
-}

parity : (n:Nat) -> Parity n
parity Z     = Even {n = Z}
parity (S Z) = Odd {n = Z}
parity (S (S k)) with (parity k)
    parity (S (S (j + j)))     | Even  = ?l1 (Even {n=S j})
    parity (S (S (S (j + j)))) | Odd  ?= (Odd {n=S j})

{-
---------- Proofs ----------
Parity.l1 = proof
  compute
  intros
  rewrite sym (plusSuccRightSucc j j)
  trivial

Parity.parity_lemma_1 = proof
  compute
  intros
  rewrite sym (plusSuccRightSucc j j)
  trivial
-}

{-

parity2 : (n:Nat) -> Parity n
parity2 Z     = Even {n = Z}
parity2 (S k) with (parity2 k)
    parity2 (S (j + j))     | Even ?= Odd {n=j}
    parity2 (S (S (j + j))) | Odd  ?= Even {n=S j}

-}

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


text:
module Compiler.Scheme.Chez

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Inline
import Compiler.Scheme.Common

import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Name
import Core.Options
import Core.TT
import Libraries.Utils.Hex
import Libraries.Utils.Path

import Data.List
import Data.List1
import Data.Maybe
import Data.Strings
import Data.Vect

import Idris.Env

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

import Libraries.Data.NameMap
import Libraries.Data.Version
import Libraries.Utils.String

%default covering

export
findChez : IO String
findChez
    = do Nothing <- idrisGetEnv "CHEZ"
            | Just chez => pure chez
         path <- pathLookup ["chez", "chezscheme", "chezscheme9.5", "scheme"]
         pure $ fromMaybe "/usr/bin/env scheme" path

||| Returns the chez scheme version for given executable
|||
||| This uses `chez --version` which unfortunately writes the version
||| on `stderr` thus requiring suffixing the command which shell redirection
||| which does not seem very portable.
export
chezVersion : String -> IO (Maybe Version)
chezVersion chez = do
    Right fh <- popen cmd Read
        | Left err => pure Nothing
    Right output <- fGetLine fh
        | Left err => pure Nothing
    pclose fh
    pure $ parseVersion output
  where
  cmd : String
  cmd = chez ++ " --version 2>&1"

unsupportedCallingConvention : Maybe Version -> Bool
unsupportedCallingConvention Nothing = True
unsupportedCallingConvention (Just version) = version < MkVersion (9,5,0) Nothing

-- Given the chez compiler directives, return a list of pairs of:
--   - the library file name
--   - the full absolute path of the library file name, if it's in one
--     of the library paths managed by Idris
-- If it can't be found, we'll assume it's a system library and that chez
-- will thus be able to find it.
export
findLibs : {auto c : Ref Ctxt Defs} ->
           List String -> Core (List (String, String))
findLibs ds
    = do let libs = mapMaybe (isLib . trim) ds
         traverse locate (nub libs)
  where
    isLib : String -> Maybe String
    isLib d
        = if isPrefixOf "lib" d
             then Just (trim (substr 3 (length d) d))
             else Nothing

schHeader : String -> List String -> String
schHeader chez libs
  = (if os /= "windows" then "#!" ++ chez ++ " --script\n\n" else "") ++
    "; @generated\n" ++
    "(import (chezscheme))\n" ++
    "(case (machine-type)\n" ++
    "  [(i3fb ti3fb a6fb ta6fb) #f]\n" ++
    "  [(i3le ti3le a6le ta6le) (load-shared-object \"libc.so.6\")]\n" ++
    "  [(i3osx ti3osx a6osx ta6osx) (load-shared-object \"libc.dylib\")]\n" ++
    "  [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")" ++
    "                           (load-shared-object \"ws2_32.dll\")]\n" ++
    "  [else (load-shared-object \"libc.so\")])\n\n" ++
    showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeStringChez x ++ "\")") libs) ++ "\n\n" ++
    "(let ()\n"

schFooter : Bool -> String
schFooter prof
    = "(collect 4)\n(blodwen-run-finalisers)\n" ++
      if prof
         then "(profile-dump-html))\n"
         else ")\n"

showChezChar : Char -> String -> String
showChezChar '\\' = ("\\\\" ++)
showChezChar c
   = if c < chr 32 || c > chr 126
        then (("\\x" ++ asHex (cast c) ++ ";") ++)
        else strCons c

showChezString : List Char -> String -> String
showChezString [] = id
showChezString ('"'::cs) = ("\\\"" ++) . showChezString cs
showChezString (c ::cs) = (showChezChar c) . showChezString cs

export
chezString : String -> String
chezString cs = strCons '"' (showChezString (unpack cs) "\"")

mutual
  tySpec : NamedCExp -> Core String
  -- Primitive types have been converted to names for the purpose of matching
  -- on types
  tySpec (NmCon fc (UN "Int") _ _ []) = pure "int"
  tySpec (NmCon fc (UN "String") _ _ []) = pure "string"
  tySpec (NmCon fc (UN "Double") _ _ []) = pure "double"
  tySpec (NmCon fc (UN "Char") _ _ []) = pure "char"
  tySpec (NmCon fc (NS _ n) _ _ [_])
     = cond [(n == UN "Ptr", pure "void*"),
             (n == UN "GCPtr", pure "void*"),
             (n == UN "Buffer", pure "u8*")]
          (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
  tySpec (NmCon fc (NS _ n) _ _ [])
     = cond [(n == UN "Unit", pure "void"),
             (n == UN "AnyPtr", pure "void*"),
             (n == UN "GCAnyPtr", pure "void*")]
          (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
  tySpec ty = throw (GenericMsg (getFC ty) ("Can't pass argument of type " ++ show ty ++ " to foreign function"))

  handleRet : String -> String -> String
  handleRet "void" op = op ++ " " ++ mkWorld (schConstructor chezString (UN "") (Just 0) [])
  handleRet _ op = mkWorld op

  getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp))
  getFArgs (NmCon fc _ _ (Just 0) _) = pure []
  getFArgs (NmCon fc _ _ (Just 1) [ty, val, rest]) = pure $ (ty, val) :: !(getFArgs rest)
  getFArgs arg = throw (GenericMsg (getFC arg) ("Badly formed c call argument list " ++ show arg))

  export
  chezExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String
  chezExtPrim i GetField [NmPrimVal _ (Str s), _, _, struct,
                          NmPrimVal _ (Str fld), _]
      = do structsc <- schExp chezExtPrim chezString 0 struct
           pure $ "(ftype-ref " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++ ")"
  chezExtPrim i GetField [_,_,_,_,_,_]
      = pure "(error \"bad getField\")"
  chezExtPrim i SetField [NmPrimVal _ (Str s), _, _, struct,
                          NmPrimVal _ (Str fld), _, val, world]
      = do structsc <- schExp chezExtPrim chezString 0 struct
           valsc <- schExp chezExtPrim chezString 0 val
           pure $ mkWorld $
              "(ftype-set! " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++
              " " ++ valsc ++ ")"
  chezExtPrim i SetField [_,_,_,_,_,_,_,_]
      = pure "(error \"bad setField\")"
  chezExtPrim i SysCodegen []
      = pure $ "\"chez\""
  chezExtPrim i OnCollect [_, p, c, world]
      = do p' <- schExp chezExtPrim chezString 0 p
           c' <- schExp chezExtPrim chezString 0 c
           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
  chezExtPrim i OnCollectAny [p, c, world]
      = do p' <- schExp chezExtPrim chezString 0 p
           c' <- schExp chezExtPrim chezString 0 c
           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
  chezExtPrim i MakeFuture [_, work]
      = do work' <- schExp chezExtPrim chezString 0 work
           pure $ "(blodwen-make-future " ++ work' ++ ")"
  chezExtPrim i prim args
      = schExtCommon chezExtPrim chezString i prim args

-- Reference label for keeping track of loaded external libraries
export
data Loaded : Type where

-- Label for noting which struct types are declared
export
data Structs : Type where

cftySpec : FC -> CFType -> Core String
cftySpec fc CFUnit = pure "void"
cftySpec fc CFInt = pure "int"
cftySpec fc CFInt8 = pure "integer-8"
cftySpec fc CFInt16 = pure "integer-16"
cftySpec fc CFInt32 = pure "integer-32"
cftySpec fc CFInt64 = pure "integer-64"
cftySpec fc CFUnsigned8 = pure "unsigned-8"
cftySpec fc CFUnsigned16 = pure "unsigned-16"
cftySpec fc CFUnsigned32 = pure "unsigned-32"
cftySpec fc CFUnsigned64 = pure "unsigned-64"
cftySpec fc CFString = pure "string"
cftySpec fc CFDouble = pure "double"
cftySpec fc CFChar = pure "char"
cftySpec fc CFPtr = pure "void*"
cftySpec fc CFGCPtr = pure "void*"
cftySpec fc CFBuffer = pure "u8*"
cftySpec fc (CFFun s t) = pure "void*"
cftySpec fc (CFIORes t) = cftySpec fc t
cftySpec fc (CFStruct n t) = pure $ "(* " ++ n ++ ")"
cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
                         " to foreign function"))

cCall : {auto c : Ref Ctxt Defs}
     -> {auto l : Ref Loaded (List String)}
     -> String
     -> FC
     -> (cfn : String)
     -> (clib : String)
     -> List (Name, CFType)
     -> CFType
     -> (collectSafe : Bool)
     -> Core (String, String)
cCall appdir fc cfn clib args (CFIORes CFGCPtr) _
    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args CFGCPtr _
    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args (CFIORes CFBuffer) _
    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn clib args CFBuffer _
    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn clib args ret collectSafe
    = do loaded <- get Loaded
         lib <- if clib `elem` loaded
                   then pure ""
                   else do (fname, fullname) <- locate clib
                           copyLib (appdir </> fname, fullname)
                           put Loaded (clib :: loaded)
                           pure $ "(load-shared-object \""
                                    ++ escapeStringChez fname
                                    ++ "\")\n"
         argTypes <- traverse (cftySpec fc . snd) args
         retType <- cftySpec fc ret
         let callConv = if collectSafe then " __collect_safe" else ""
         let call = "((foreign-procedure" ++ callConv ++ " " ++ show cfn ++ " ("
                      ++ showSep " " argTypes ++ ") " ++ retType ++ ") "
                      ++ showSep " " !(traverse buildArg args) ++ ")"

         pure (lib, case ret of
                         CFIORes _ => handleRet retType call
                         _ => call)
  where
    mkNs : Int -> List CFType -> List (Maybe String)
    mkNs i [] = []
    mkNs i (CFWorld :: xs) = Nothing :: mkNs i xs
    mkNs i (x :: xs) = Just ("cb" ++ show i) :: mkNs (i + 1) xs

    applyLams : String -> List (Maybe String) -> String
    applyLams n [] = n
    applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as
    applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as

    getVal : String -> String
    getVal str = "(vector-ref " ++ str ++ "1)"

    mkFun : List CFType -> CFType -> String -> String
    mkFun args ret n
        = let argns = mkNs 0 args in
              "(lambda (" ++ showSep " " (mapMaybe id argns) ++ ") " ++
              (applyLams n argns ++ ")")

    notWorld : CFType -> Bool
    notWorld CFWorld = False
    notWorld _ = True

    callback : String -> List CFType -> CFType -> Core String
    callback n args (CFFun s t) = callback n (s :: args) t
    callback n args_rev retty
        = do let args = reverse args_rev
             argTypes <- traverse (cftySpec fc) (filter notWorld args)
             retType <- cftySpec fc retty
             pure $
                 "(let ([c-code (foreign-callable #f " ++
                       mkFun args retty n ++
                       " (" ++ showSep " " argTypes ++ ") " ++ retType ++ ")])" ++
                       " (lock-object c-code) (foreign-callable-entry-point c-code))"

    buildArg : (Name, CFType) -> Core String
    buildArg (n, CFFun s t) = callback (schName n) [s] t
    buildArg (n, CFGCPtr) = pure $ "(car " ++ schName n ++ ")"
    buildArg (n, _) = pure $ schName n

schemeCall : FC -> (sfn : String) ->
             List Name -> CFType -> Core String
schemeCall fc sfn argns ret
    = let call = "(" ++ sfn ++ " " ++ showSep " " (map schName argns) ++ ")" in
          case ret of
               CFIORes _ => pure $ mkWorld call
               _ => pure call

-- Use a calling convention to compile a foreign def.
-- Returns any preamble needed for loading libraries, and the body of the
-- function call.
useCC : {auto c : Ref Ctxt Defs} ->
        {auto l : Ref Loaded (List String)} ->
        String -> FC -> List String -> List (Name, CFType) -> CFType ->
        Maybe Version -> Core (String, String)
useCC appdir fc ccs args ret version
    = case parseCC ["scheme,chez", "scheme", "C__collect_safe", "C"] ccs of
           Just ("scheme,chez", [sfn]) =>
               do body <- schemeCall fc sfn (map fst args) ret
                  pure ("", body)
           Just ("scheme", [sfn]) =>
               do body <- schemeCall fc sfn (map fst args) ret
                  pure ("", body)
           Just ("C__collect_safe", (cfn :: clib :: _)) => do
             if unsupportedCallingConvention version
               then cCall appdir fc cfn clib args ret False
               else cCall appdir fc cfn clib args ret True
           Just ("C", (cfn :: clib :: _)) =>
             cCall appdir fc cfn clib args ret False
           _ => throw (NoForeignCC fc ccs)

-- For every foreign arg type, return a name, and whether to pass it to the
-- foreign call (we don't pass '%World')
mkArgs : Int -> List CFType -> List (Name, Bool)
mkArgs i [] = []
mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs i cs
mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs

mkStruct : {auto s : Ref Structs (List String)} ->
           CFType -> Core String
mkStruct (CFStruct n flds)
    = do defs <- traverse mkStruct (map snd flds)
         strs <- get Structs
         if n `elem` strs
            then pure (concat defs)
            else do put Structs (n :: strs)
                    pure $ concat defs ++ "(define-ftype " ++ n ++ " (struct\n\t"
                           ++ showSep "\n\t" !(traverse showFld flds) ++ "))\n"
  where
    showFld : (String, CFType) -> Core String
    showFld (n, ty) = pure $ "[" ++ n ++ " " ++ !(cftySpec emptyFC ty) ++ "]"
mkStruct (CFIORes t) = mkStruct t
mkStruct (CFFun a b) = do ignore (mkStruct a); mkStruct b
mkStruct _ = pure ""

schFgnDef : {auto c : Ref Ctxt Defs} ->
            {auto l : Ref Loaded (List String)} ->
            {auto s : Ref Structs (List String)} ->
            String -> FC -> Name -> NamedDef -> Maybe Version -> Core (String, String)
schFgnDef appdir fc n (MkNmForeign cs args ret) version
    = do let argns = mkArgs 0 args
         let allargns = map fst argns
         let useargns = map fst (filter snd argns)
         argStrs <- traverse mkStruct args
         retStr <- mkStruct ret
         (load, body) <- useCC appdir fc cs (zip useargns args) ret version
         defs <- get Ctxt
         pure (load,
                concat argStrs ++ retStr ++
                "(define " ++ schName !(full (gamma defs) n) ++
                " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++
                body ++ "))\n")
schFgnDef _ _ _ _ _ = pure ("", "")

export
getFgnCall : {auto c : Ref Ctxt Defs} ->
             {auto l : Ref Loaded (List String)} ->
             {auto s : Ref Structs (List String)} ->
             String -> Maybe Version -> (Name, FC, NamedDef) -> Core (String, String)
getFgnCall appdir version (n, fc, d) = schFgnDef appdir fc n d version

export
startChezPreamble : String
startChezPreamble = unlines
    [ "#!/bin/sh"
    , ""
    , "set -e # exit on any error"
    , ""
    , "if [ \"$(uname)\" = Darwin ]; then"
    , "  DIR=$(zsh -c 'printf %s \"$0:A:h\"' \"$0\")"
    , "else"
    , "  DIR=$(dirname \"$(readlink -f -- \"$0\")\")"
    , "fi"
    , ""  -- so that the preamble ends with a newline
    ]

startChez : String -> String -> String
startChez appdir target = startChezPreamble ++ unlines
    [ "export LD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ "\":$LD_LIBRARY_PATH"
    , "\"$DIR/" ++ target ++ "\" \"$@\""
    ]

startChezCmd : String -> String -> String -> String
startChezCmd chez appdir target = unlines
    [ "@echo off"
    , "set APPDIR=%~dp0"
    , "set PATH=%APPDIR%\\" ++ appdir ++ ";%PATH%"
    , "\"" ++ chez ++ "\" --script \"%APPDIR%/" ++ target ++ "\" %*"
    ]

startChezWinSh : String -> String -> String -> String
startChezWinSh chez appdir target = unlines
    [ "#!/bin/sh"
    , ""
    , "set -e # exit on any error"
    , ""
    , "DIR=$(dirname \"$(readlink -f -- \"$0\")\")"
    , "CHEZ=$(cygpath \"" ++ chez ++"\")"
    , "export PATH=\"$DIR/" ++ appdir ++ "\":$PATH"
    , "\"$CHEZ\" --script \"$DIR/" ++ target ++ "\" \"$@\""
    ]

||| Compile a TT expression to Chez Scheme
compileToSS : Ref Ctxt Defs ->
              Bool -> String -> ClosedTerm -> (outfile : String) -> Core ()
compileToSS c prof appdir tm outfile
    = do ds <- getDirectives Chez
         libs <- findLibs ds
         traverse_ copyLib libs
         cdata <- getCompileData False Cases tm
         let ndefs = namedDefs cdata
         let ctm = forget (mainExpr cdata)

         defs <- get Ctxt
         l <- newRef {t = List String} Loaded ["libc", "libc 6"]
         s <- newRef {t = List String} Structs []
         chez <- coreLift findChez
         version <- coreLift $ chezVersion chez
         fgndefs <- traverse (getFgnCall appdir version) ndefs
         compdefs <- traverse (getScheme chezExtPrim chezString) ndefs
         let code = fastAppend (map snd fgndefs ++ compdefs)
         main <- schExp chezExtPrim chezString 0 ctm
         support <- readDataFile "chez/support.ss"
         extraRuntime <- getExtraRuntime ds
         let scm = schHeader chez (map snd libs) ++
                   support ++ extraRuntime ++ code ++
                   concat (map fst fgndefs) ++
                   "(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))\n" ++
                   main ++ schFooter prof
         Right () <- coreLift $ writeFile outfile scm
            | Left err => throw (FileErr outfile err)
         coreLift_ $ chmodRaw outfile 0o755
         pure ()

||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off.
compileToSO : {auto c : Ref Ctxt Defs} ->
              Bool -> String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
compileToSO prof chez appDirRel outSsAbs
    = do let tmpFileAbs = appDirRel </> "compileChez"
         let build = "(parameterize ([optimize-level 3] "
                     ++ (if prof then "[compile-profile #t] "
                                else "") ++
                     "[compile-file-message #f]) (compile-program " ++
                    show outSsAbs ++ "))"
         Right () <- coreLift $ writeFile tmpFileAbs build
            | Left err => throw (FileErr tmpFileAbs err)
         coreLift_ $ chmodRaw tmpFileAbs 0o755
         coreLift_ $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"")
         pure ()

makeSh : String -> String -> String -> Core ()
makeSh outShRel appdir outAbs
    = do Right () <- coreLift $ writeFile outShRel (startChez appdir outAbs)
            | Left err => throw (FileErr outShRel err)
         pure ()

||| Make Windows start scripts, one for bash environments and one batch file
makeShWindows : String -> String -> String -> String -> Core ()
makeShWindows chez outShRel appdir outAbs
    = do let cmdFile = outShRel ++ ".cmd"
         Right () <- coreLift $ writeFile cmdFile (startChezCmd chez appdir outAbs)
            | Left err => throw (FileErr cmdFile err)
         Right () <- coreLift $ writeFile outShRel (startChezWinSh chez appdir outAbs)
            | Left err => throw (FileErr outShRel err)
         pure ()

||| Chez Scheme implementation of the `compileExpr` interface.
compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
              ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr makeitso c tmpDir outputDir tm outfile
    = do let appDirRel = outfile ++ "_app" -- relative to build dir
         let appDirGen = outputDir </> appDirRel -- relative to here
         coreLift_ $ mkdirAll appDirGen
         Just cwd <- coreLift currentDir
              | Nothing => throw (InternalError "Can't get current directory")
         let outSsFile = appDirRel </> outfile <.> "ss"
         let outSoFile = appDirRel </> outfile <.> "so"
         let outSsAbs = cwd </> outputDir </> outSsFile
         let outSoAbs = cwd </> outputDir </> outSoFile
         chez <- coreLift $ findChez
         let prof = profile !getSession
         compileToSS c (makeitso && prof) appDirGen tm outSsAbs
         logTime "++ Make SO" $ when makeitso $ compileToSO prof chez appDirGen outSsAbs
         let outShRel = outputDir </> outfile
         if isWindows
            then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile)
            else makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile)
         coreLift_ $ chmodRaw outShRel 0o755
         pure (Just outShRel)

||| Chez Scheme implementation of the `executeExpr` interface.
||| This implementation simply runs the usual compiler, saving it to a temp file, then interpreting it.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm
    = do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpchez"
            | Nothing => throw (InternalError "compileExpr returned Nothing")
         coreLift_ $ system sh
         pure ()

||| Codegen wrapper for Chez scheme implementation.
export
codegenChez : Codegen
codegenChez = MkCG (compileExpr True) executeExpr

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
%default total

fix : Void
fix = case the (Either () Void) (Left ()) of
        Left () => fix
        Right p => absurd p


text:
module System.Clock

import PrimIO

||| The various types of system clock available.
public export
data ClockType
  = UTC       -- The time elapsed since the "epoch:" 00:00:00 UTC, January 1, 1970
  | Monotonic -- The time elapsed since some arbitrary point in the past
  | Duration  -- Representing a time duration.
  | Process   -- The amount of CPU time used by the current process.
  | Thread    -- The amount of CPU time used by the current thread.
  | GCCPU     -- The current process's CPU time consumed by the garbage collector.
  | GCReal    -- The current process's real time consumed by the garbage collector.

export
Show ClockType where
  show UTC       = "UTC"
  show Monotonic = "monotonic"
  show Duration  = "duration"
  show Process   = "process"
  show Thread    = "thread"
  show GCCPU     = "gcCPU"
  show GCReal    = "gcReal"

public export
data Clock : (type : ClockType) -> Type where
  MkClock
    : {type : ClockType}
    -> (seconds : Integer)
    -> (nanoseconds : Integer)
    -> Clock type

public export
Eq (Clock type) where
  (MkClock seconds1 nanoseconds1) == (MkClock seconds2 nanoseconds2) =
    seconds1 == seconds2 && nanoseconds1 == nanoseconds2

public export
Ord (Clock type) where
  compare (MkClock seconds1 nanoseconds1) (MkClock seconds2 nanoseconds2) =
  case compare seconds1 seconds2 of
    LT => LT
    GT => GT
    EQ => compare nanoseconds1 nanoseconds2

public export
Show (Clock type) where
  show (MkClock {type} seconds nanoseconds) =
    show type ++ ": " ++ show seconds ++ "s " ++ show nanoseconds ++ "ns"

||| A helper to deconstruct a Clock.
public export
seconds : Clock type -> Integer
seconds (MkClock s _) = s

||| A helper to deconstruct a Clock.
public export
nanoseconds : Clock type -> Integer
nanoseconds (MkClock _ ns) = ns

||| Make a duration value.
public export
makeDuration : Integer -> Integer -> Clock Duration
makeDuration = MkClock

||| Opaque clock value manipulated by the back-end.
data OSClock : Type where [external]

||| Note: Back-ends are required to implement UTC, monotonic time, CPU time
||| in current process/thread, and time duration; the rest are optional.
export
data ClockTypeMandatory
  = Mandatory
  | Optional

public export
isClockMandatory : ClockType -> ClockTypeMandatory
isClockMandatory GCCPU  = Optional
isClockMandatory GCReal = Optional
isClockMandatory _      = Mandatory

%foreign "scheme:blodwen-clock-time-monotonic"
prim__clockTimeMonotonic : PrimIO OSClock

clockTimeMonotonic : IO OSClock
clockTimeMonotonic = fromPrim prim__clockTimeMonotonic

%foreign "scheme:blodwen-clock-time-utc"
prim__clockTimeUtc : PrimIO OSClock

clockTimeUtc : IO OSClock
clockTimeUtc = fromPrim prim__clockTimeUtc

%foreign "scheme:blodwen-clock-time-process"
prim__clockTimeProcess : PrimIO OSClock

clockTimeProcess : IO OSClock
clockTimeProcess = fromPrim prim__clockTimeProcess

%foreign "scheme:blodwen-clock-time-thread"
prim__clockTimeThread : PrimIO OSClock

clockTimeThread : IO OSClock
clockTimeThread = fromPrim prim__clockTimeThread

%foreign "scheme:blodwen-clock-time-gccpu"
prim__clockTimeGcCpu : PrimIO OSClock

clockTimeGcCpu : IO OSClock
clockTimeGcCpu = fromPrim prim__clockTimeGcCpu

%foreign "scheme:blodwen-clock-time-gcreal"
prim__clockTimeGcReal : PrimIO OSClock

clockTimeGcReal : IO OSClock
clockTimeGcReal = fromPrim prim__clockTimeGcReal

fetchOSClock : ClockType -> IO OSClock
fetchOSClock UTC       = clockTimeUtc
fetchOSClock Monotonic = clockTimeMonotonic
fetchOSClock Process   = clockTimeProcess
fetchOSClock Thread    = clockTimeThread
fetchOSClock GCCPU     = clockTimeGcCpu
fetchOSClock GCReal    = clockTimeGcReal
fetchOSClock Duration  = clockTimeMonotonic

%foreign "scheme:blodwen-is-time?"
prim__osClockValid : OSClock -> PrimIO Int

||| A test to determine the status of optional clocks.
osClockValid : OSClock -> IO Int
osClockValid clk = fromPrim (prim__osClockValid clk)

%foreign "scheme:blodwen-clock-second"
prim__osClockSecond : OSClock -> PrimIO Bits64

osClockSecond : OSClock -> IO Bits64
osClockSecond clk = fromPrim (prim__osClockSecond clk)

%foreign "scheme:blodwen-clock-nanosecond"
prim__osClockNanosecond : OSClock -> PrimIO Bits64

osClockNanosecond : OSClock -> IO Bits64
osClockNanosecond clk = fromPrim (prim__osClockNanosecond clk)

fromOSClock : {type : ClockType} -> OSClock -> IO (Clock type)
fromOSClock clk =
  pure $
    MkClock
      {type}
      (cast !(osClockSecond clk))
      (cast !(osClockNanosecond clk))

public export
clockTimeReturnType : (typ : ClockType) -> Type
clockTimeReturnType typ with (isClockMandatory typ)
  clockTimeReturnType typ | Optional = Maybe (Clock typ)
  clockTimeReturnType typ | Mandatory = Clock typ

||| Fetch the system clock of a given kind. If the clock is mandatory,
||| we return a (Clock type) else (Maybe (Clock type)).
public export
clockTime : (typ : ClockType) -> IO (clockTimeReturnType typ)
clockTime clockType with (isClockMandatory clockType)
  clockTime clockType | Mandatory = fetchOSClock clockType >>= fromOSClock
  clockTime clockType | Optional = do
    clk <- fetchOSClock clockType
    valid <- map (== 1) $ osClockValid clk
    if valid
      then map Just $ fromOSClock clk
      else pure Nothing

toNano : Clock type -> Integer
toNano (MkClock seconds nanoseconds) =
  let scale = 1000000000
   in scale * seconds + nanoseconds

fromNano : {type : ClockType} -> Integer -> Clock type
fromNano n =
  let scale       = 1000000000
      seconds     = n `div` scale
      nanoseconds = n `mod` scale
   in MkClock seconds nanoseconds

||| Compute difference between two clocks of the same type.
public export
timeDifference : Clock type -> Clock type -> Clock Duration
timeDifference clock duration = fromNano $ toNano clock - toNano duration

||| Add a duration to a clock value.
public export
addDuration : {type : ClockType} -> Clock type -> Clock Duration -> Clock type
addDuration clock duration = fromNano $ toNano clock + toNano duration

||| Subtract a duration from a clock value.
public export
subtractDuration : {type : ClockType} -> Clock type -> Clock Duration -> Clock type
subtractDuration clock duration = fromNano $ toNano clock - toNano duration