text:
module Language.APIDef

import Data.Maybe
import Data.List as L
import Data.Strings
--import Data.Vect

import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Util

{-
As source AST of Idris2 is too big to describe API.
To minimize efforts, reduced version of AST is defined.
Because of its reduction, if we just remove unnecessary definition, some functions becomes partial,
we choose to define NotImplemented definition for such reduced definitions.

The idea behind this is to use restricted Idris2's source language as a API definition language.
That provides automatic type check for API definition language and an ability to use Idris2's dependent type
for API definitions.

-}

public export
data Const
    = CI Int
    | CBI Integer
    | CB8 Int -- For now, since we don't have Bits types. We need to
                -- make sure the Integer remains in range
    | CB16 Int
    | CB32 Int
    | CB64 Integer
    | CStr String
    | CCh Char
    | CDb Double
    | CWorldVal

    | CIntType
    | CIntegerType
    | CBits8Type
    | CBits16Type
    | CBits32Type
    | CBits64Type
    | CStringType
    | CCharType
    | CDoubleType
    | CWorldType

pshow : Show a => a -> Doc ann
pshow = pretty . show

Pretty Const where
  pretty (CI x) = "CT" <++> pshow x
  pretty (CBI x) = "CBI" <++> pshow x
  pretty (CB8 x) = "CB8" <++> pshow x
  pretty (CB16 x) = "CB16" <++> pshow x
  pretty (CB32 x) = "CB32" <++> pshow x
  pretty (CB64 x) = "CB64" <++> pshow x
  pretty (CStr x) = "CStr" <++> pshow x
  pretty (CCh x) = "CCh" <++> pshow x
  pretty (CDb x) = "CDb" <++> pshow x
  pretty CWorldVal = "WorldVal"
  pretty CIntType = "CIntType"
  pretty CIntegerType = "CIntegerType"
  pretty CBits8Type = "CBitsType"
  pretty CBits16Type = "CBits16Type"
  pretty CBits32Type ="CBits32Type"
  pretty CBits64Type = "CBits64Type"
  pretty CStringType = "CStringType"
  pretty CCharType = "CCharType"
  pretty CDoubleType = "CDoubleType"
  pretty CWorldType = "CWorldType"

parens: String -> String
parens s = "("++ s ++ ")"

export
sconcat : String -> List String -> String
sconcat sep xs = concat $ L.intersperse sep xs

-- Restricted version of Source syntax
public export
data Namespace : Type where
  DMkNS : List String -> Namespace

public export
data ModuleIdent : Type where
  DMkMI : List String -> ModuleIdent

mutual
  public export
  Name : Type
  Name = String

  ||| DModule corresond to Module in Idris/Syntax.idr
  data DModule : Type where
    MkModule : String -> Namespace -> List DDecl -> DModule
  ||| DDecl is a reduced version of PDecl.
  ||| Anything ommited becomes DDeclNotIMplemented.
  public export
  data DDecl : Type where
    DClaim : DTypeDecl -> DDecl
    DDef : List DClause -> DDecl
    DData : (doc : String) -> DDataDecl -> DDecl
    DRecord : (doc : String) -> Name -> (conName : Maybe Name) -> List DField -> DDecl
    DNamespace : Namespace -> (List DDecl) -> DDecl
    DDeclNotImplemented: String -> DDecl

  ||| DField is a reduced version of PDField.
  public export
  data DField : Type where
    MkDField : (doc : String) -> APIDef.Name -> (ty : DTerm) -> DField

  ||| DTerm is a reduced version of PTerm.
  ||| This is one of the most central pert of APIDef.
  ||| Selected terms are all necessary to define data type, record, muti-argument function definitions and etc.
  public export
  data DTerm: Type where
    DRef : APIDef.Name -> DTerm
    DPi : Maybe APIDef.Name -> (argTy : DTerm) -> (retTy : DTerm) -> DTerm
    DLam : DTerm -> (argTy : DTerm) -> (scope: DTerm) -> DTerm
    DApp : DTerm -> DTerm -> DTerm
    DNamedApp : DTerm -> Name -> DTerm -> DTerm
    DPrimVal : Const -> DTerm
    DImplicit : DTerm
    DInfer : DTerm
    DHole : String -> DTerm
    DType : DTerm

    DList : List DTerm -> DTerm
    DPair : DTerm -> DTerm -> DTerm
    DUnit : DTerm

    DBracketed :  DTerm -> DTerm
    DTermNotImplemented : String -> DTerm

  ||| DClause is a reduced version of PClause.
  public export
  data DClause : Type where
    MkDPatClause : (lhs : DTerm) -> (rhs : DTerm) -> DClause
    MkDClauseNotImplemented : String -> DClause

  ||| Reduced vaersion of DTypeDecl
  public export
  data DTypeDecl : Type where
    MkDTy : (n : APIDef.Name) -> (doc : String) -> (type : DTerm) -> DTypeDecl

  ||| Reduced vaersion of DDataDecl
  public export
  data DDataDecl : Type where
    MkDData : (tyname : APIDef.Name) -> (tycon : DTerm) -> (datacons : List DTypeDecl) -> DDataDecl
--    MkDLater : (tyname : APIDef.Name) -> (tycon : DTerm) -> DDataDecl
    MkDDataNotImplemented : String -> DDataDecl

Show Namespace where
  show (DMkNS xs) = ("DMkNS:" ++ show xs)

Show ModuleIdent where
  show (DMkMI xs) = ("DMkMI:" ++ show xs)

mutual
  export
  Show DTerm where
    show (DRef x) = x
    show (DPi Nothing argTy retTy) = show argTy ++ "->" ++ show retTy
    show (DPi (Just x) argTy retTy) = "Π" ++ x ++ ":" ++ show argTy ++ "->" ++ show retTy
    show (DLam x argTy scope) = parens("λ" ++ show x ++ "." ++ show argTy ++ "-->" ++ show scope)
    show (DApp x y) = show x ++ parens( show y)
    show (DNamedApp x name y) = show x ++ show name ++ show y
    show (DPrimVal (CI x)) = show x
    show (DPrimVal (CBI x)) = show x
    show (DPrimVal (CB8 x)) = show x
    show (DPrimVal (CB16 x)) = show x
    show (DPrimVal (CB32 x)) = show x
    show (DPrimVal (CB64 x)) = show x
    show (DPrimVal (CStr x)) = show x
    show (DPrimVal (CCh x)) = show x
    show (DPrimVal (CDb x)) = show x
    show (DPrimVal CWorldVal) = "World"
    show (DPrimVal CIntType) = "Int"
    show (DPrimVal CIntegerType) = "Integer"
    show (DPrimVal CBits8Type) = "B8"
    show (DPrimVal CBits16Type) = "B16"
    show (DPrimVal CBits32Type) = "B32"
    show (DPrimVal CBits64Type) = "B64"
    show (DPrimVal CStringType) = "String"
    show (DPrimVal CCharType) = "Char"
    show (DPrimVal CDoubleType) = "Double"
    show (DPrimVal CWorldType) = "#World"
    show DImplicit = "IMPLICIT"
    show DInfer = "INFER"
    show (DHole x) = "?" ++ x
    show DType = "Type"
    show (DList xs) = "List "
    show (DPair x y) = "(" ++ show x ++ "," ++ show y ++ ")"
    show DUnit = "()"
    show (DBracketed x) = show x
    show (DTermNotImplemented msg) = "Not supported Term:" ++ msg

  ||| Data field of record.
  export
  Show DField where
    show (MkDField d x ty) = x ++ ":" ++ (show ty)

  export
  Show DClause where
    show (MkDPatClause lhs rhs) = show lhs ++ ":=" ++ show rhs
    show (MkDClauseNotImplemented x) = "Not supported"

  export
  Show DTypeDecl where
    show (MkDTy n doc type) = n ++ ":" ++ show type

  export
  Show DDataDecl where
    show (MkDData tyname tycon datacons) = tyname ++ ":" ++ show tycon ++ " " ++ (sconcat " " $ map show datacons)
--    show (MkDLater tyname tycon) = tyname ++ ":" ++ show tycon
    show (MkDDataNotImplemented x) = "MkDDataNotImplemented:" ++ x

  public export
  Show DDecl where
    show (DClaim x) = "DClaim:" ++ show x
    show (DDef xs) = "DDef:" ++ (sconcat " " $ map show xs)
    show (DData doc x) = "DData:" ++ show x
    show (DRecord doc n con fs) = "DRecord:" ++ show n ++ " " ++ show con ++ " " ++  show fs
    show (DNamespace n ds) = "DNamespace:" ++ show n ++ " " ++ show ds
    show (DDeclNotImplemented msg) = "DDeclNotImplemented:" ++ "Not implemented:" ++ msg

prettyMaybe : (a -> Doc ann) -> Maybe a -> Doc ann
prettyMaybe _ Nothing = pretty "Nothing"
prettyMaybe f (Just a) = pretty "Just" <++> f a

p : Doc ann -> Doc ann
p = parenthesise True
q : String -> Doc ann
q = dquotes . pretty

escape : Char -> String -> String
escape _ a = a

qq : String -> Doc ann
qq = dquotes . pretty . escape '\''

ms : Maybe String -> Doc ann
ms = prettyMaybe q

public export
Pretty Namespace where
  pretty (DMkNS xs) = p("DMkNS" <++>  (encloseSep lbracket rbracket comma . reverse $ map q xs))
public export
Pretty ModuleIdent where
  pretty (DMkMI xs) = p("DMkMI" <++>  (encloseSep lbracket rbracket comma . reverse $ map q xs))

export
ppPair : (Pretty a, Pretty b) => (a, b) -> Doc ann
ppPair (a, b) = p(pretty a <+> comma <+>pretty b)

(Pretty a, Pretty b) => Pretty (List (Pair a b)) where
  pretty xs = vcat $ map pretty xs

--export
--Pretty a => Pretty (List a) where
--  pretty xs = vsep $ intersperse comma $ map pretty xs

mutual
  public export
  Pretty DDecl where
    pretty (DClaim x) = p ("DClaim" <++> pretty x)
    pretty (DDef xs) = p ("DDef" <++> pretty xs)
    pretty (DData doc x) = p ("DData" <++> qq doc <++> pretty x)
    pretty (DRecord doc n con fs) = p ("DRecord" <++> qq doc <++> q n <++> ms con <++> pretty fs)
    pretty (DNamespace ns ds) = p ("DNamespace" <++> pretty ns <++> pretty ds)

    pretty (DDeclNotImplemented x) = p ("DDeclNotImplemented" <++> qq x)
  export
  Pretty DDataDecl where
    pretty (MkDData tyname tycon datacons) = p ("MkDData" <++> q tyname <++> pretty tycon <++> pretty datacons)
--    pretty (MkDLater tyname tycon) = p ("MkDLater" <++> q tyname <++> pretty tycon)
    pretty (MkDDataNotImplemented x) = p ("MkDDataNotImplemented" <++> qq x)
  export
  Pretty DTypeDecl where
    pretty (MkDTy n doc type) = p ("MkDTy" <++> q n <++> qq doc <++> pretty type)
  export
  Pretty DClause where
    pretty (MkDPatClause lhs rhs) = p ("MkDPatClause" <++> pretty lhs <++> pretty rhs)
    pretty (MkDClauseNotImplemented x) = p ("MkDClauseNotImplemented" <++> qq x)
  export
  Pretty DField where
    pretty (MkDField doc x ty) = p ("MkDField" <++> qq doc <++> q x <++> pretty ty)
  export
  Pretty DTerm where
    pretty (DRef x) = p ("DRef" <++> q x)
    pretty (DPi x argTy retTy)
      = p ("DPi" <++> p (ms x) <++> pretty argTy <++> pretty retTy)
    pretty (DLam x argTy scope) = p ("DLam" <++> pretty x <++> pretty argTy <++> pretty scope)
    pretty (DApp x y) = p ("DApp" <++> pretty x <++> pretty y)
    pretty (DNamedApp x n y) = p ("DNamedApp" <++> pretty x <++> q n <++> pretty y)
    pretty (DPrimVal x) = p ("DPrimVal" <++> pretty x)
    pretty DImplicit = pretty "DImplicit"
    pretty DInfer = pretty "DInfoer"
    pretty (DHole x) = p ("DHole" <++> pretty x)
    pretty DType = pretty "DType"
    pretty (DPair x y) = p ("DPair" <++> p(pretty x) <++> p(pretty y))
    pretty (DList xs) = p ("DList" <++> encloseSep lbracket rbracket comma (map pretty xs))
    pretty DUnit = pretty "DUnit"
    pretty (DBracketed x) = p ("DBracketed" <++> pretty x)
    pretty (DTermNotImplemented x) = p ("DTermNotImplemented" <++> qq x)

Pretty DModule where
  pretty (MkModule doc n decls) = p (pretty (show n) <++> comma <++> pretty decls)


text:
module Crayon

%access public export

data Crayon
  = FgBlack | FgRed | FgGreen | FgYellow | FgBlue | FgMagenta | FgCyan | FgWhite
  | BgBlack | BgRed | BgGreen | BgYellow | BgBlue | BgMagenta | BgCyan | BgWhite
  | Reset | Bright | Dim | Underscore | Blink | Reverse | Hidden

--------------------------------------------------------------------------------
-- Implementations
--------------------------------------------------------------------------------

Cast Crayon Nat where
  cast Reset      = 0
  cast Bright     = 1
  cast Dim        = 2
  cast Underscore = 4
  cast Blink      = 5
  cast Reverse    = 7
  cast Hidden     = 8
  cast FgBlack    = 30
  cast FgRed      = 31
  cast FgGreen    = 32
  cast FgYellow   = 33
  cast FgBlue     = 34
  cast FgMagenta  = 35
  cast FgCyan     = 36
  cast FgWhite    = 37
  cast BgBlack    = 40
  cast BgRed      = 41
  cast BgGreen    = 42
  cast BgYellow   = 43
  cast BgBlue     = 44
  cast BgMagenta  = 45
  cast BgCyan     = 46
  cast BgWhite    = 47

Show Crayon where
  show x = "\x1b[" <+> show (the Nat (cast x)) <+> "m"

--------------------------------------------------------------------------------
-- Helpers
--------------------------------------------------------------------------------

colorize : Crayon -> String -> String
colorize crayon string = (show crayon) <+> string <+> (show Reset)

bright : String -> String
bright = colorize Bright

dim : String -> String
dim = colorize Dim

underscore : String -> String
underscore = colorize Underscore

blink : String -> String
blink = colorize Blink

black : String -> String
black = colorize FgBlack

red : String -> String
red = colorize FgRed

green : String -> String
green = colorize FgGreen

yellow : String -> String
yellow = colorize FgYellow

blue : String -> String
blue = colorize FgBlue

magenta : String -> String
magenta = colorize FgMagenta

cyan : String -> String
cyan = colorize FgCyan

white : String -> String
white = colorize FgWhite

bgBlack : String -> String
bgBlack = colorize BgBlack

bgRed : String -> String
bgRed = colorize BgRed

bgGreen : String -> String
bgGreen = colorize BgGreen

bgYellow : String -> String
bgYellow = colorize BgYellow

bgBlue : String -> String
bgBlue = colorize BgBlue

bgMagenta : String -> String
bgMagenta = colorize BgMagenta

bgCyan : String -> String
bgCyan = colorize BgCyan

bgWhite : String -> String
bgWhite = colorize BgWhite

{-
code : Crayon -> String
code (Foreground FgBlack) = "\x1b[" <+> (show . cast $ FgBlack) <+> "m"
code (Foreground FgRed) = ?code_rhs_5
code _ = ""
-}

{-
code : Color -> Nat
code NoColor = 0
code White = 37
code Black = 30
-}

{-
Reset = "\x1b[0m"
Bright = "\x1b[1m"
Dim = "\x1b[2m"
Underscore = "\x1b[4m"
Blink = "\x1b[5m"
Reverse = "\x1b[7m"
Hidden = "\x1b[8m"

FgBlack = "\x1b[30m"
FgRed = "\x1b[31m"
FgGreen = "\x1b[32m"
FgYellow = "\x1b[33m"
FgBlue = "\x1b[34m"
FgMagenta = "\x1b[35m"
FgCyan = "\x1b[36m"
FgWhite = "\x1b[37m"

BgBlack = "\x1b[40m"
BgRed = "\x1b[41m"
BgGreen = "\x1b[42m"
BgYellow = "\x1b[43m"
BgBlue = "\x1b[44m"
BgMagenta = "\x1b[45m"
BgCyan = "\x1b[46m"
BgWhite = "\x1b[47m"
               -}

ext: idr

max_stars_repo_name: Risto-Stevcev/idris-crayons

max_issues_repo_name: Risto-Stevcev/idris-crayons

max_forks_repo_name: Risto-Stevcev/idris-crayons


text:
||| This module is responsible for compiling an
||| Idris2 `ClosedTerm` to a pair of `ImperativeStatement`s,
||| one of which corresponds to a sequence of toplevel
||| definitions, the other being the program's main entry
||| point.
module Compiler.ES.Imperative

import public Compiler.ES.ImperativeAst

import Data.List

import Compiler.Common
import Compiler.CompileExpr

import public Core.Context

import Compiler.ES.TailRec

%default covering

mutual
  isNameUsed : Name -> NamedCExp -> Bool
  isNameUsed name (NmLocal fc n) = n == name
  isNameUsed name (NmRef fc n) = n == name
  isNameUsed name (NmLam fc n e) = isNameUsed name e
  isNameUsed name (NmApp fc x args)
    = isNameUsed name x || any (isNameUsed name) args
  isNameUsed name (NmPrimVal fc c) = False
  isNameUsed name (NmOp fc op args) = any (isNameUsed name) args
  isNameUsed name (NmConCase fc sc alts def)
    = isNameUsed name sc
    || any (isNameUsedConAlt name) alts
    || maybe False (isNameUsed name) def
  isNameUsed name (NmConstCase fc sc alts def)
    = isNameUsed name sc
    || any (isNameUsedConstAlt name) alts
    || maybe False (isNameUsed name) def
  isNameUsed name (NmExtPrim fc p args) = any (isNameUsed name) args
  isNameUsed name (NmCon fc x _ t args) = any (isNameUsed name) args
  isNameUsed name (NmDelay fc _ t) = isNameUsed name t
  isNameUsed name (NmForce fc _ t) = isNameUsed name t
  isNameUsed name (NmLet fc x val sc) =
    if x == name then isNameUsed name val
      else isNameUsed name val || isNameUsed name sc
  isNameUsed name (NmErased fc) = False
  isNameUsed name (NmCrash fc msg) = False

  isNameUsedConAlt : Name -> NamedConAlt -> Bool
  isNameUsedConAlt name (MkNConAlt n _ t args exp) = isNameUsed name exp

  isNameUsedConstAlt : Name -> NamedConstAlt -> Bool
  isNameUsedConstAlt name (MkNConstAlt c exp) = isNameUsed name exp

data Imps : Type where

record ImpSt where
  constructor MkImpSt
  nextName : Int

genName : {auto c : Ref Imps ImpSt} -> Core Name
genName =
  do s <- get Imps
     let i = nextName s
     put Imps (record { nextName = i + 1 } s)
     pure $ MN "imp_gen" i

-- Processing an Idris2 expression results in
-- an `ImperativeStatement` (since this is a monoid,
-- this might actually be many statements) of utility
-- functions and intermediary vars and results, and
-- a final imperative expression, calculating a result
-- from the related statement(s). These
-- are then converted to JS code.
--
-- The boolean flag indicates, whether the two parts
-- should be returned as a pair for further
-- processing, or should be converted
-- to a single statement (in which case, the final
-- expression is converted to a `return` statement).
ImperativeResult : (toReturn : Bool) -> Type
ImperativeResult True  = ImperativeStatement
ImperativeResult False = (ImperativeStatement, ImperativeExp)

-- when invoking `impExp`, in some cases we always
-- generate a pair (statements plus related final
-- expression). In such a case, this function converts
-- the statement to the correct result type as indicated
-- by `toReturn`.
pairToReturn :  (toReturn : Bool)
             -> (ImperativeStatement, ImperativeExp)
             -> (ImperativeResult toReturn)
pairToReturn False (s, e) = (s, e)
pairToReturn True (s, e)  = s <+> ReturnStatement e

-- when invoking `impExp`, in some cases we
-- generate just an expression.
-- In such a case, this function converts
-- the expression to the correct result type as indicated
-- by `toReturn`.
expToReturn :  (toReturn : Bool)
            -> ImperativeExp
            -> (ImperativeResult toReturn)
expToReturn False e = (DoNothing, e)
expToReturn True e  = ReturnStatement e

impTag : Name -> Maybe Int -> Either Int String
impTag n Nothing = Right $ show n
impTag n (Just i) = Left i

-- memoize an intermediary result in a `let` binding.
-- doesn't do anything if `exp` is a variable, constant
-- or undefined.
memoExp : {auto c : Ref Imps ImpSt}
        -> (exp : ImperativeExp)
        -> Core (ImperativeStatement, ImperativeExp)
memoExp e@(IEVar _)      = pure (neutral, e)
memoExp e@(IEConstant _) = pure (neutral, e)
memoExp IENull           = pure (neutral, IENull)
memoExp e                = map (\n =>(LetDecl n $ Just e, IEVar n)) genName

mutual
  -- converts primOps arguments to a set of
  -- statements plus a corresponding vect of expressions
  impVectExp :  {auto c : Ref Imps ImpSt}
             -> Vect n NamedCExp
             -> Core (ImperativeStatement, Vect n ImperativeExp)
  impVectExp args =
    do a <- traverseVect (impExp False) args
       pure (concatMap fst a, map snd a)

  -- converts function arguments to a set of
  -- statements plus a corresponding list of expressions
  impListExp :  {auto c : Ref Imps ImpSt}
             -> List NamedCExp
             -> Core (ImperativeStatement, List ImperativeExp)
  impListExp args =
    do a <- traverse (impExp False) args
       pure (concatMap fst a, map snd a)

  impExp :  {auto c : Ref Imps ImpSt}
         -> (toReturn : Bool)
         -> NamedCExp
         -> Core (ImperativeResult toReturn)
  -- convert local names to vars
  impExp toReturn (NmLocal fc n) =
    pure . expToReturn toReturn $ IEVar n

  impExp toReturn (NmRef fc n) =
    pure . expToReturn toReturn $ IEVar n

  -- TODO: right now, nested lambda expressions are curried
  -- (or are they?).
  -- It might be more efficient (and more readable!) to uncurry
  -- these, at least in the most simple cases.
  impExp toReturn (NmLam fc n e) =
    pure . expToReturn toReturn $ IELambda [n] !(impExp True e)

  -- Function application: Statements for the
  -- implementation of the function and the arguments are
  -- generated separately and concatenated.
  impExp toReturn (NmApp fc x args) =
    do (s1, f) <- impExp False x
       (s2, a) <- impListExp args
       pure $ pairToReturn toReturn (s1 <+> s2, IEApp f a)

  -- primitive values
  impExp toReturn (NmPrimVal fc c) =
    pure . expToReturn toReturn $ IEConstant c

  -- primitive operations
  impExp toReturn (NmOp fc op args) =
    do (s, a) <- impVectExp args
       pure $ pairToReturn toReturn (s, IEPrimFn op a)

  -- a pattern match on a constructor
  -- is converted to a switch statement in JS.
  --
  -- TODO: We should treat record constructors
  --       separately, to avoid the unnecessary
  --       switch
  --
  -- ```
  -- s1
  -- let res;
  -- switch(exp.h) {
  --   alternatives
  --   default (if any)
  -- }
  -- res;
  -- ```
  impExp False (NmConCase fc sc alts def) =
    do (s1, exp)  <- impExp False sc
       (s2, exp2) <- memoExp exp
       res    <- genName
       swalts <- traverse (impConAltFalse res exp2) alts
       swdef  <- case def of
                   Nothing => pure $ ErrorStatement $ "unhandled con case on " ++ show fc
                   Just x =>
                    do (sd, r) <- impExp False x
                       pure $ sd <+> MutateStatement res r
       let switch = SwitchStatement (IEConstructorHead exp2) swalts (Just swdef)
       pure (s1 <+> s2 <+> LetDecl res Nothing <+> switch, IEVar res)

  -- like `impExp False NmConCase`, but we return directly without
  -- a local let binding
  impExp True (NmConCase fc sc alts def) =
    do (s1, exp) <- impExp False sc
       (s2, exp2) <- memoExp exp
       swalts <- traverse (impConAltTrue exp2) alts
       swdef <- case def of
                 Nothing => pure $ ErrorStatement $ "unhandled con case on " ++ show fc
                 Just x => impExp True x
       let switch = SwitchStatement (IEConstructorHead exp2) swalts (Just swdef)
       pure (s1 <+> s2 <+> switch)

  -- a case statement (pattern match on a constant)
  -- is converted to a switch statement in JS.
  -- the distinction between `impExp False` and
  -- `impExp True` is the same as for constructor matches
  impExp False (NmConstCase fc sc alts def) =
    do (s1, exp) <- impExp False sc
       res <- genName
       swalts <- traverse (impConstAltFalse res) alts
       swdef <- case def of
                  Nothing => pure $ ErrorStatement $ "unhandled const case on " ++ show fc
                  Just x =>
                    do
                      (sd, r) <- impExp False x
                      pure $ sd <+> MutateStatement res r
       let switch = SwitchStatement exp swalts (Just swdef)
       pure (s1 <+> LetDecl res Nothing <+> switch, IEVar res)

  impExp True (NmConstCase fc sc alts def) =
    do (s1, exp) <- impExp False sc
       swalts <- traverse impConstAltTrue alts
       swdef <- case def of
                 Nothing => pure $ ErrorStatement $ "unhandled const case on " ++ show fc
                 Just x => impExp True x
       let switch = SwitchStatement exp swalts (Just swdef)
       pure $ s1 <+> switch

  -- coversion of primitive external functions like
  -- `prim__newIORef`
  impExp toReturn (NmExtPrim fc p args) =
    do (s, a) <- impListExp args
       pure $ pairToReturn toReturn (s, IEPrimFnExt p a)

  -- A saturated constructor
  -- TODO: Use ConInfo
  impExp toReturn (NmCon fc x _ tag args) =
    do (s, a) <- impListExp args
       pure $ pairToReturn toReturn
         (s, IEConstructor (impTag x tag) a)

  -- a delayed computation
  impExp toReturn (NmDelay fc _ t) =
    do (s, x) <- impExp False t
       pure $ pairToReturn toReturn (s, IEDelay x)

  -- a forced computation
  impExp toReturn (NmForce fc _ t) =
    do (s, x) <- impExp False t
       pure $ pairToReturn toReturn (s, IEForce x)

  -- a let statement of the form
  -- ```idris
  -- let name = expr1
  --  in expr2
  --
  -- ```
  -- is converted to
  --
  -- ```javascript
  -- expr1_statements;
  -- const name_ = expr1_expr;
  -- expr2_statements;
  -- expr2_expr;
  -- ```
  -- where `name_` is a newly generated name, which
  -- is replaced in `expr2`.
  --
  -- if `name` is not used in `expr2`, this is
  -- simplified to
  --
  -- ```javascript
  -- expr1_statements;
  -- expr1_expr; -- evaluation of expr1!
  -- expr2_statements;
  -- expr2_expr;
  -- ```
  -- TODO: Is it necessary to generate a new name
  -- here, or is this already handled by Idris itself?
  impExp toReturn (NmLet fc x val sc) =
    do (s1, v)   <- impExp False val
       (s2, sc_) <- impExp False sc
       if isNameUsed x sc
         then do
           x_ <- genName
           let reps = [(x, IEVar x_)]
           let s2_  = replaceNamesExpS reps s2
           let sc__ = replaceNamesExp reps sc_
           let decl = ConstDecl x_ v
           pure $ pairToReturn toReturn (s1 <+> decl <+> s2_, sc__)
         else do
           let decl = EvalExpStatement v
           pure $ pairToReturn toReturn (s1 <+> decl <+> s2, sc_)

  -- an erased argument is converted to `undefined`
  impExp toReturn (NmErased fc) =
    pure . expToReturn toReturn $ IENull

  -- an error is converted to a `throw new Error`
  -- statement. It's result is `undefined` (`IENull`).
  impExp toReturn (NmCrash fc msg) =
    pure $ pairToReturn toReturn (ErrorStatement msg, IENull)

  -- a single alternative in a case statement.
  -- In JS, this will be a single alternative of
  -- a switch statement.
  -- TODO: Use ConInfo
  --
  -- @ res : name of the local var (from a `let` statement)
  --         to which the result should be assigned (if any)
  -- @ target : The value against which to match
  -- @ con : The constructor to use
  impConAltFalse :  {auto c : Ref Imps ImpSt}
                 -> (res : Name)
                 -> (target : ImperativeExp)
                 -> (con : NamedConAlt)
                 -> Core (ImperativeExp, ImperativeStatement)
  impConAltFalse res target (MkNConAlt n _ tag args exp) =
    do (s, r) <- impExp False exp
       (tgts,tgte) <- memoExp target
       let nargs = length args
       let reps = zipWith (\i, n => (n, IEConstructorArg (cast i) tgte))
                          [1..nargs]
                          args
       pure ( IEConstructorTag (impTag n tag)
            , tgts <+> (replaceNamesExpS reps $ s <+> MutateStatement res r)
            )

  impConAltTrue :  {auto c : Ref Imps ImpSt}
                -> (target : ImperativeExp)
                -> (con : NamedConAlt)
                -> Core (ImperativeExp, ImperativeStatement)
  impConAltTrue target (MkNConAlt n _ tag args exp) =
    do s <- impExp True exp
       (tgts,tgte) <- memoExp target
       let nargs = length args
       let reps = zipWith (\i, n => (n, IEConstructorArg (cast i) tgte))
                          [1..nargs]
                          args
       pure ( IEConstructorTag (impTag n tag), tgts <+> replaceNamesExpS reps s)

  impConstAltFalse :  {auto c : Ref Imps ImpSt}
                   -> Name
                   -> NamedConstAlt
                   -> Core (ImperativeExp, ImperativeStatement)
  impConstAltFalse res (MkNConstAlt c exp) =
    do (s, r) <- impExp False exp
       pure (IEConstant c, s <+> MutateStatement res r)

  impConstAltTrue :  {auto c : Ref Imps ImpSt}
                  -> NamedConstAlt
                  -> Core (ImperativeExp, ImperativeStatement)
  impConstAltTrue (MkNConstAlt c exp) =
    do s <- impExp True exp
       pure (IEConstant c, s)

-- generate an `ImperativeStatement` from the
-- given named definition
getImp :  {auto c : Ref Imps ImpSt}
       -> (Name, FC, NamedDef)
       -> Core ImperativeStatement
getImp (n, fc, MkNmFun args exp) =
  pure $ FunDecl fc n args !(impExp True exp)
getImp (n, fc, MkNmError exp) =
  throw $ (InternalError $ show exp)
getImp (n, fc, MkNmForeign cs args ret) =
  pure $ ForeignDecl fc n cs args ret
getImp (n, fc, MkNmCon _ _ _) =
  pure DoNothing

||| Compiles a `ClosedTerm` to a pair of statements,
||| the first corresponding to a list of toplevel definitions
||| the other being the program's main entry point.
|||
||| Toplevel definitions defined in the given `ClosedTerm`
||| are only included if they are (transitively) being
||| invoked by the main function.
|||
||| In addition, toplevel definitions are tail call optimized
||| (see module `Compiler.ES.TailRec`).
export
compileToImperative :  Ref Ctxt Defs
                    -> ClosedTerm
                    -> Core (ImperativeStatement, ImperativeStatement)
compileToImperative c tm =
  do -- generate the named definitions and main expression
     -- from the `ClosedTerm`
     cdata <- getCompileData False Cases tm

     -- list of named definitions
     let ndefs = namedDefs cdata

     -- main expression
     let ctm = forget (mainExpr cdata)

     ref <- newRef Imps (MkImpSt 0)

     -- list of toplevel definitions (only those necessary
     -- to implement the main expression)
     lst_defs <- traverse getImp ndefs

     let defs = concat lst_defs

     -- tail rec optimited definitions
     defs_optim <- tailRecOptim defs

     -- main expression and statements necessary to
     -- implement main's body
     (s, main) <- impExp False ctm
     pure $ (defs_optim, s <+> EvalExpStatement main)

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Flexidisc.Transformation.Type

import Flexidisc.OrdList
import Flexidisc.RecordContent
import Flexidisc.TaggedValue

import Control.Monad.Identity

%default total
%access export

infixr 9 :->

public export
data MapValue = (:->) Type Type

public export
data MapValuesM : (m : Type -> Type) -> (k : Type) -> (o : Ord k) ->
                  (header : OrdList k o MapValue) -> Type where
    Nil  : (o : Ord k) => MapValuesM m k o []
    (::) : TaggedValue l (s -> m t) -> MapValuesM m k o header ->
           MapValuesM m k o ((l, s :-> t) :: header)

public export
MapValues :  (k : Type) -> (o : Ord k) -> OrdList k o MapValue -> Type
MapValues = MapValuesM id

insert : TaggedValue k' (s -> m t) -> MapValuesM m k o header ->
         MapValuesM m k o (insert (k', s :-> t) header)
insert x [] = [x]
insert (k' := v) ((kx := vx) :: xs') with (k' < kx)
  | False = (kx := vx) :: (insert (k' := v) xs')
  | True  = (k' := v) :: (kx := vx) :: xs'

public export
toLabels : OrdList k o MapValue -> List k
toLabels [] = []
toLabels ((k, s :-> t) :: xs) = k :: toLabels xs

public export
toSource : OrdList k o MapValue -> OrdList k o Type
toSource [] = []
toSource ((k, s :-> t) :: xs) = (k, s) :: toSource xs

public export
toTarget : OrdList k o MapValue -> OrdList k o Type
toTarget [] = []
toTarget ((k, s :-> t) :: xs) = (k, t) :: toTarget xs

mapRecord : (o : Ord k) =>
            (trans : MapValuesM m k o mapper) ->
            (xs : RecordContent k o (toSource mapper)) ->
            RecordContentM m k o (toTarget mapper)
mapRecord [] [] = []
mapRecord (k := f :: fs) (k := x :: xs) = k := f x :: mapRecord fs xs

traverseRecord : (o : Ord k, Applicative m) =>
                 (trans : MapValuesM m k o mapper) ->
                 (xs : RecordContent k o (toSource mapper)) ->
                 m (RecordContent k o (toTarget mapper))
traverseRecord [] [] = pure []
traverseRecord ((k := f) :: fs) ((k := x) :: xs) =
  mapHead k <$> f x <*> traverseRecord fs xs
    where
      mapHead k' x' xs' = k' := x' :: xs'

patchRecord : (DecEq k, Applicative m) =>
              (trans : MapValuesM m k o mapper) ->
              (xs : RecordContent k o header) ->
              (prf : Sub (toSource mapper) header) ->
              m (RecordContent k o (patch (toTarget mapper) header))
patchRecord trans xs {prf} =
  (\p => p |> xs) <$> traverseRecord trans (project xs prf)

patchRecord' : DecEq k =>
               (trans : MapValues k o mapper) ->
               (xs : RecordContent k o header) ->
               (prf : Sub (toSource mapper) header) ->
               RecordContent k o (patch (toTarget mapper) header)
patchRecord' trans xs {prf} =
  mapRecord trans (project xs prf) |> xs

public export
endoM : (f, g : Type -> Type) -> Type -> Type
endoM f g a = f a -> g a

infixl 4 <**>

(<**>) : RecordContentM (endoM m n) k o header ->
         RecordContentM m k o header ->
         RecordContentM n k o header
(<**>) [] [] = []
(<**>) (k' := f :: fs) (k' := x :: xs) = k' := f x :: (fs <**> xs)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 13, section 2

-- check that all functions are total
%default total

--
-- see Stack.idr
-- see StackIO.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Main

corecord Str a where -- Current stream is codata, not a corecord
  constructor (::)
  head : a
  tail : Str a

implementation Functor Str where
  map f (x :: xs) = (f x) :: (map f xs)

total -- marked total to check that corecords are indeed treated as coinductive types
zeros : Str Int
zeros = 0 :: zeros

ones : Str Int
ones = map (1+) zeros

main : IO ()
main = do let x = record { head = 1 } zeros
          printLn $ head zeros
          printLn $ head x
          printLn $ head (record { head = 3 } x)
          printLn $ head (tail ones)
          printLn $ head (tail (record { tail = zeros } ones))

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 Main

import Parity
import System

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

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

infixl 5 #

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

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

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

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

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

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
||| Union types (= sum types) in the FFI.
module JS.Union

import Data.SOP
import JS.Inheritance
import JS.Marshall

public export
data NPP :  (f : Type -> Type -> Type)
         -> (ps1 : List Type)
         -> (ps2 : List Type)
         -> Type where
  Nil  : NPP f Nil Nil
  (::) : f a b -> NPP f ps1 ps2 -> NPP f (a :: ps1) (b :: ps2)

appToFFI : NPP ToFFI ps1 ps2 -> NS I ps1 -> NS I ps2
appToFFI [] (Z v) impossible
appToFFI [] (S x) impossible
appToFFI (_ :: _) (Z v) = Z $ toFFI v
appToFFI (_ :: t) (S y) = S $ appToFFI t y

appFromFFI : NPP FromFFI ps1 ps2 -> NS I ps2 -> Maybe $ NS I ps1
appFromFFI [] (Z v) impossible
appFromFFI [] (S x) impossible
appFromFFI (_ :: _) (Z v) = Z <$> fromFFI v
appFromFFI (_ :: t) (S y) = S <$> appFromFFI t y

--------------------------------------------------------------------------------
--          Union2
--------------------------------------------------------------------------------

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

export
toUnion2 : NS I [a,b] -> Union2 a b
toUnion2 = collapseNS . mapNS believe_me

export
fromUnion2 : NP SafeCast [a,b] => Union2 a b -> Maybe $ NS I [a,b]
fromUnion2 = safeCastNS

export
(npp : NPP ToFFI [a,b] [m,n]) =>
  ToFFI (NS I [a,b]) (Union2 m n) where
    toFFI ns = toUnion2 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b] [m,n]) => NP SafeCast [m,n] =>
  FromFFI (NS I [a,b]) (Union2 m n) where
    fromFFI ns = fromUnion2 ns >>= appFromFFI npp

export
FromFFI (Union2 a b) (Union2 a b) where
  fromFFI = Just

export
ToFFI (Union2 a b) (Union2 a b) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union3
--------------------------------------------------------------------------------

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

export
toUnion3 : NS I [a,b,c] -> Union3 a b c
toUnion3 = collapseNS . mapNS believe_me

export
fromUnion3 : NP SafeCast [a,b,c] => Union3 a b c -> Maybe $ NS I [a,b,c]
fromUnion3 = safeCastNS

export
(npp : NPP ToFFI [a,b,c] [m,n,o]) =>
  ToFFI (NS I [a,b,c]) (Union3 m n o) where
    toFFI ns = toUnion3 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c] [m,n,o]) => NP SafeCast [m,n,o] =>
  FromFFI (NS I [a,b,c]) (Union3 m n o) where
    fromFFI ns = fromUnion3 ns >>= appFromFFI npp

export
FromFFI (Union3 a b c) (Union3 a b c) where
  fromFFI = Just

export
ToFFI (Union3 a b c) (Union3 a b c) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union4
--------------------------------------------------------------------------------

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

export
toUnion4 : NS I [a,b,c,d] -> Union4 a b c d
toUnion4 = collapseNS . mapNS believe_me

export
fromUnion4 : NP SafeCast [a,b,c,d] => Union4 a b c d -> Maybe $ NS I [a,b,c,d]
fromUnion4 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d] [m,n,o,p]) =>
  ToFFI (NS I [a,b,c,d]) (Union4 m n o p) where
    toFFI ns = toUnion4 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d] [m,n,o,p]) => NP SafeCast [m,n,o,p] =>
  FromFFI (NS I [a,b,c,d]) (Union4 m n o p) where
    fromFFI ns = fromUnion4 ns >>= appFromFFI npp

export
FromFFI (Union4 a b c d) (Union4 a b c d) where
  fromFFI = Just

export
ToFFI (Union4 a b c d) (Union4 a b c d) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union5
--------------------------------------------------------------------------------

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

export
toUnion5 : NS I [a,b,c,d,e] -> Union5 a b c d e
toUnion5 = collapseNS . mapNS believe_me

export
fromUnion5 : NP SafeCast [a,b,c,d,e] =>
             Union5 a b c d e -> Maybe $ NS I [a,b,c,d,e]
fromUnion5 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e] [m,n,o,p,q]) =>
  ToFFI (NS I [a,b,c,d,e]) (Union5 m n o p q) where
    toFFI ns = toUnion5 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e] [m,n,o,p,r]) => NP SafeCast [m,n,o,p,r] =>
  FromFFI (NS I [a,b,c,d,e]) (Union5 m n o p r) where
    fromFFI ns = fromUnion5 ns >>= appFromFFI npp

export
FromFFI (Union5 a b c d e) (Union5 a b c d e) where
  fromFFI = Just

export
ToFFI (Union5 a b c d e) (Union5 a b c d e) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union6
--------------------------------------------------------------------------------

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

export
toUnion6 : NS I [a,b,c,d,e,f] -> Union6 a b c d e f
toUnion6 = collapseNS . mapNS believe_me

export
fromUnion6 : NP SafeCast [a,b,c,d,e,f] =>
             Union6 a b c d e f -> Maybe $ NS I [a,b,c,d,e,f]
fromUnion6 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e,f] [m,n,o,p,q,r]) =>
  ToFFI (NS I [a,b,c,d,e,f]) (Union6 m n o p q r) where
    toFFI ns = toUnion6 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e,f] [m,n,o,p,r,s]) =>
NP SafeCast [m,n,o,p,r,s] =>
  FromFFI (NS I [a,b,c,d,e,f]) (Union6 m n o p r s) where
    fromFFI ns = fromUnion6 ns >>= appFromFFI npp

export
FromFFI (Union6 a b c d e f) (Union6 a b c d e f) where
  fromFFI = Just

export
ToFFI (Union6 a b c d e f) (Union6 a b c d e f) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union7
--------------------------------------------------------------------------------

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

export
toUnion7 : NS I [a,b,c,d,e,f,g] -> Union7 a b c d e f g
toUnion7 = collapseNS . mapNS believe_me

export
fromUnion7 : NP SafeCast [a,b,c,d,e,f,g] =>
             Union7 a b c d e f g -> Maybe $ NS I [a,b,c,d,e,f,g]
fromUnion7 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e,f,g] [m,n,o,p,q,r,s]) =>
  ToFFI (NS I [a,b,c,d,e,f,g]) (Union7 m n o p q r s) where
    toFFI ns = toUnion7 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e,f,g] [m,n,o,p,r,s,t]) =>
NP SafeCast [m,n,o,p,r,s,t] =>
  FromFFI (NS I [a,b,c,d,e,f,g]) (Union7 m n o p r s t) where
    fromFFI ns = fromUnion7 ns >>= appFromFFI npp

export
FromFFI (Union7 a b c d e f g) (Union7 a b c d e f g) where
  fromFFI = Just

export
ToFFI (Union7 a b c d e f g) (Union7 a b c d e f g) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union8
--------------------------------------------------------------------------------

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

export
toUnion8 : NS I [a,b,c,d,e,f,g,h] -> Union8 a b c d e f g h
toUnion8 = collapseNS . mapNS believe_me

export
fromUnion8 : NP SafeCast [a,b,c,d,e,f,g,h] =>
             Union8 a b c d e f g h -> Maybe $ NS I [a,b,c,d,e,f,g,h]
fromUnion8 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e,f,g,h] [m,n,o,p,q,r,s,t]) =>
  ToFFI (NS I [a,b,c,d,e,f,g,h]) (Union8 m n o p q r s t) where
    toFFI ns = toUnion8 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e,f,g,h] [m,n,o,p,r,s,t,u]) =>
NP SafeCast [m,n,o,p,r,s,t,u] =>
  FromFFI (NS I [a,b,c,d,e,f,g,h]) (Union8 m n o p r s t u) where
    fromFFI ns = fromUnion8 ns >>= appFromFFI npp

export
FromFFI (Union8 a b c d e f g h) (Union8 a b c d e f g h) where
  fromFFI = Just

export
ToFFI (Union8 a b c d e f g h) (Union8 a b c d e f g h) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union9
--------------------------------------------------------------------------------

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

export
toUnion9 : NS I [a,b,c,d,e,f,g,h,i] -> Union9 a b c d e f g h i
toUnion9 = collapseNS . mapNS believe_me

export
fromUnion9 : NP SafeCast [a,b,c,d,e,f,g,h,i] =>
             Union9 a b c d e f g h i -> Maybe $ NS I [a,b,c,d,e,f,g,h,i]
fromUnion9 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e,f,g,h,i] [m,n,o,p,q,r,s,t,u]) =>
  ToFFI (NS I [a,b,c,d,e,f,g,h,i]) (Union9 m n o p q r s t u) where
    toFFI ns = toUnion9 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e,f,g,h,i] [m,n,o,p,r,s,t,u,v]) =>
NP SafeCast [m,n,o,p,r,s,t,u,v] =>
  FromFFI (NS I [a,b,c,d,e,f,g,h,i]) (Union9 m n o p r s t u v) where
    fromFFI ns = fromUnion9 ns >>= appFromFFI npp

export
FromFFI (Union9 a b c d e f g h i) (Union9 a b c d e f g h i) where
  fromFFI = Just

export
ToFFI (Union9 a b c d e f g h i) (Union9 a b c d e f g h i) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union10
--------------------------------------------------------------------------------

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

export
toUnion10 : NS I [a,b,c,d,e,f,g,h,i,j] -> Union10 a b c d e f g h i j
toUnion10 = collapseNS . mapNS believe_me

export
fromUnion10 : NP SafeCast [a,b,c,d,e,f,g,h,i,j] =>
             Union10 a b c d e f g h i j -> Maybe $ NS I [a,b,c,d,e,f,g,h,i,j]
fromUnion10 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j] [m,n,o,p,q,r,s,t,u,v]) =>
  ToFFI (NS I [a,b,c,d,e,f,g,h,i,j]) (Union10 m n o p q r s t u v) where
    toFFI ns = toUnion10 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j] [m,n,o,p,r,s,t,u,v,w]) =>
NP SafeCast [m,n,o,p,r,s,t,u,v,w] =>
  FromFFI (NS I [a,b,c,d,e,f,g,h,i,j]) (Union10 m n o p r s t u v w) where
    fromFFI ns = fromUnion10 ns >>= appFromFFI npp

export
FromFFI (Union10 a b c d e f g h i j) (Union10 a b c d e f g h i j) where
  fromFFI = Just

export
ToFFI (Union10 a b c d e f g h i j) (Union10 a b c d e f g h i j) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union11
--------------------------------------------------------------------------------

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

export
toUnion11 : NS I [a,b,c,d,e,f,g,h,i,j,k] -> Union11 a b c d e f g h i j k
toUnion11 = collapseNS . mapNS believe_me

export
fromUnion11 : NP SafeCast [a,b,c,d,e,f,g,h,i,j,k] =>
             Union11 a b c d e f g h i j k -> Maybe $ NS I [a,b,c,d,e,f,g,h,i,j,k]
fromUnion11 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k] [m,n,o,p,q,r,s,t,u,v,w]) =>
  ToFFI (NS I [a,b,c,d,e,f,g,h,i,j,k]) (Union11 m n o p q r s t u v w) where
    toFFI ns = toUnion11 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k] [m,n,o,p,q,r,s,t,u,v,w]) =>
NP SafeCast [m,n,o,p,q,r,s,t,u,v,w] =>
  FromFFI (NS I [a,b,c,d,e,f,g,h,i,j,k]) (Union11 m n o p q r s t u v w) where
    fromFFI ns = fromUnion11 ns >>= appFromFFI npp

export
FromFFI (Union11 a b c d e f g h i j k) (Union11 a b c d e f g h i j k) where
  fromFFI = Just

export
ToFFI (Union11 a b c d e f g h i j k) (Union11 a b c d e f g h i j k) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union12
--------------------------------------------------------------------------------

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

export
toUnion12 : NS I [a,b,c,d,e,f,g,h,i,j,k,l] -> Union12 a b c d e f g h i j k l
toUnion12 = collapseNS . mapNS believe_me

export
fromUnion12 : NP SafeCast [a,b,c,d,e,f,g,h,i,j,k,l] =>
             Union12 a b c d e f g h i j k l -> Maybe $ NS I [a,b,c,d,e,f,g,h,i,j,k,l]
fromUnion12 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k,l] [m,n,o,p,q,r,s,t,u,v,w,x]) =>
  ToFFI (NS I [a,b,c,d,e,f,g,h,i,j,k,l]) (Union12 m n o p q r s t u v w x) where
    toFFI ns = toUnion12 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k,l] [m,n,o,p,q,r,s,t,u,v,w,x]) =>
NP SafeCast [m,n,o,p,q,r,s,t,u,v,w,x] =>
  FromFFI (NS I [a,b,c,d,e,f,g,h,i,j,k,l]) (Union12 m n o p q r s t u v w x) where
    fromFFI ns = fromUnion12 ns >>= appFromFFI npp

export
FromFFI (Union12 a b c d e f g h i j k l) (Union12 a b c d e f g h i j k l) where
  fromFFI = Just

export
ToFFI (Union12 a b c d e f g h i j k l) (Union12 a b c d e f g h i j k l) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union13
--------------------------------------------------------------------------------

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

export
toUnion13 : NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1] -> Union13 a b c d e f g h i j k l a1
toUnion13 = collapseNS . mapNS believe_me

export
fromUnion13 : NP SafeCast [a,b,c,d,e,f,g,h,i,j,k,l,a1] =>
             Union13 a b c d e f g h i j k l a1 -> Maybe $ NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1]
fromUnion13 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1] [m,n,o,p,q,r,s,t,u,v,w,x,y]) =>
  ToFFI (NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1]) (Union13 m n o p q r s t u v w x y) where
    toFFI ns = toUnion13 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1] [m,n,o,p,q,r,s,t,u,v,w,x,y]) =>
NP SafeCast [m,n,o,p,q,r,s,t,u,v,w,x,y] =>
  FromFFI (NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1]) (Union13 m n o p q r s t u v w x y) where
    fromFFI ns = fromUnion13 ns >>= appFromFFI npp

export
FromFFI (Union13 a b c d e f g h i j k l m) (Union13 a b c d e f g h i j k l m) where
  fromFFI = Just

export
ToFFI (Union13 a b c d e f g h i j k l m) (Union13 a b c d e f g h i j k l m) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union14
--------------------------------------------------------------------------------

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

export
toUnion14 : NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2] -> Union14 a b c d e f g h i j k l a1 a2
toUnion14 = collapseNS . mapNS believe_me

export
fromUnion14 : NP SafeCast [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2] =>
             Union14 a b c d e f g h i j k l a1 a2 -> Maybe $ NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2]
fromUnion14 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2] [m,n,o,p,q,r,s,t,u,v,w,x,y,z]) =>
  ToFFI (NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2]) (Union14 m n o p q r s t u v w x y z) where
    toFFI ns = toUnion14 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2] [m,n,o,p,q,r,s,t,u,v,w,x,y,z]) =>
NP SafeCast [m,n,o,p,q,r,s,t,u,v,w,x,y,z] =>
  FromFFI (NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2]) (Union14 m n o p q r s t u v w x y z) where
    fromFFI ns = fromUnion14 ns >>= appFromFFI npp

export
FromFFI (Union14 a b c d e f g h i j k l m n) (Union14 a b c d e f g h i j k l m n) where
  fromFFI = Just

export
ToFFI (Union14 a b c d e f g h i j k l m n) (Union14 a b c d e f g h i j k l m n) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union15
--------------------------------------------------------------------------------

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

export
toUnion15 : NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3] -> Union15 a b c d e f g h i j k l a1 a2 a3
toUnion15 = collapseNS . mapNS believe_me

export
fromUnion15 : NP SafeCast [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3] =>
             Union15 a b c d e f g h i j k l a1 a2 a3 -> Maybe $ NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3]
fromUnion15 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3] [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1]) =>
  ToFFI (NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3]) (Union15 m n o p q r s t u v w x y z z1) where
    toFFI ns = toUnion15 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3] [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1]) =>
NP SafeCast [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1] =>
  FromFFI (NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3]) (Union15 m n o p q r s t u v w x y z z1) where
    fromFFI ns = fromUnion15 ns >>= appFromFFI npp

export
FromFFI (Union15 a b c d e f g h i j k l m n o) (Union15 a b c d e f g h i j k l m n o) where
  fromFFI = Just

export
ToFFI (Union15 a b c d e f g h i j k l m n o) (Union15 a b c d e f g h i j k l m n o) where
  toFFI = id

--------------------------------------------------------------------------------
--          Union16
--------------------------------------------------------------------------------

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

export
toUnion16 : NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4] -> Union16 a b c d e f g h i j k l a1 a2 a3 a4
toUnion16 = collapseNS . mapNS believe_me

export
fromUnion16 : NP SafeCast [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4] =>
             Union16 a b c d e f g h i j k l a1 a2 a3 a4 -> Maybe $ NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4]
fromUnion16 = safeCastNS

export
(npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4] [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1,z2]) =>
  ToFFI (NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4]) (Union16 m n o p q r s t u v w x y z z1 z2) where
    toFFI ns = toUnion16 $ appToFFI npp ns

export
(npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4] [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1,z2]) =>
NP SafeCast [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1,z2] =>
  FromFFI (NS I [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4]) (Union16 m n o p q r s t u v w x y z z1 z2) where
    fromFFI ns = fromUnion16 ns >>= appFromFFI npp

export
FromFFI (Union16 a b c d e f g h i j k l m n o p) (Union16 a b c d e f g h i j k l m n o p) where
  fromFFI = Just

export
ToFFI (Union16 a b c d e f g h i j k l m n o p) (Union16 a b c d e f g h i j k l m n o p) where
  toFFI = id


text:
module Extra.C.CPtr

import Data.Nat
import Data.Vect
import Extra.String
import Extra.Proof
import Extra.C.Ptr
import Extra.C.Storable
import public Control.Linear.LIO
import public Extra.C.Types

public export
data Content : Type where
  NullTerminated : (can_free : Bool) -> Content
  Bytes : (can_free, can_read, can_write : Bool) -> Nat -> Content
  Opaque : (can_free : Bool) -> (ty : Type) -> Content

public export
isFreeable : Content -> Bool
isFreeable (NullTerminated can_free) = can_free
isFreeable (Bytes can_free _ _ _) = can_free
isFreeable (Opaque can_free _) = can_free

public export
typeOf : Content -> Type
typeOf (NullTerminated _) = CChar
typeOf (Bytes _ _ _ _) = CUInt8
typeOf (Opaque _ ty) = ty

public export
data CPtr : Content -> Type where
  MkCPtr : Ptr (typeOf content) -> CPtr content

export
malloc
  : LinearIO io
  => (length : Nat)
  -> {default True can_free : Bool}
  -> {default True can_read : Bool}
  -> {default True can_write : Bool}
  -> L io {use=1} (CPtr (Bytes can_free can_read can_write length))
malloc length = do
  ptr <- primIO $ prim__malloc $ cast $ natToInteger length
  pure1 $ MkCPtr (castPtr ptr)

export
calloc
  : LinearIO io
  => (length : Nat)
  -> {default True can_free : Bool}
  -> {default True can_read : Bool}
  -> {default True can_write : Bool}
  -> L io {use=1} (CPtr (Bytes can_free can_read can_write length))
calloc length = do
  ptr <- primIO $ prim__calloc $ cast $ natToInteger length
  pure1 $ MkCPtr (castPtr ptr)

export
free
  : LinearIO io
  => (1 _ : CPtr content)
  -> {auto okay : isFreeable content = True}
  -> L io ()
free (MkCPtr ptr) = primIO $ prim__free (forgetPtr ptr)

export
pokeByte
  : LinearIO io
  => (1 _ : CPtr (Bytes can_free can_read True length))
  -> (index : Nat)
  -> {auto 0 okay : LT index length}
  -> (byte : CUInt8)
  -> L io {use=1} (CPtr (Bytes can_free can_read True length))
pokeByte (MkCPtr ptr) index byte = do
  poke (plusPtr ptr (cast $ natToInteger index)) byte
  pure1 $ MkCPtr ptr

export
peekByte
  : LinearIO io
  => (1 _ : CPtr (Bytes can_free True can_write length))
  -> (index : Nat)
  -> {auto 0 okay : LT index length}
  -> L io {use=1} (Res CUInt8 (\_ => CPtr (Bytes can_free True can_write length)))
peekByte (MkCPtr ptr) index = do
  byte <- peek (plusPtr ptr (cast $ natToInteger index))
  pure1 $ (byte # MkCPtr ptr)

export
peekBytes
  : LinearIO io
  => (1 _ : CPtr (Bytes can_free True can_write length))
  -> (offset : Nat)
  -> (count : Nat)
  -> {auto okay : LTE (offset + count) length}
  -> L io {use=1} (Res (Vect count CUInt8) (\_ => CPtr (Bytes can_free True can_write length)))
peekBytes cptr ofs Z = pure1 $ Nil # cptr
peekBytes cptr ofs (S cnt) = do
  let m = lteAddRight (S ofs) {m = cnt}
  let m = replace {p = LTE (S ofs)} (plusSuccRightSucc ofs cnt) m
  byte # cptr <- peekByte {okay = lteTransitive m okay} cptr ofs
  let n = okay
  let n = replace {p = \a => LTE a length} (sym $ plusSuccRightSucc ofs cnt) n
  bytes # cptr <- peekBytes cptr (S ofs) cnt {okay = n}
  pure1 $ (byte :: bytes) # cptr

export
pokeBytes
  : LinearIO io
  => (1 _ : CPtr (Bytes can_free can_read True length))
  -> (offset : Nat)
  -> {count : Nat}
  -> (bytes : Vect count CUInt8)
  -> {auto okay : LTE (offset + count) length}
  -> L io {use=1} (CPtr (Bytes can_free can_read True length))
pokeBytes {count = Z} cptr ofs Nil             = pure1 $ cptr
pokeBytes {count = S cnt} cptr ofs (byte :: bytes) = do
  let m = lteAddRight (S ofs) {m = cnt}
  let m = replace {p = LTE (S ofs)} (plusSuccRightSucc ofs cnt) m
  cptr <- pokeByte {okay = lteTransitive m okay} cptr ofs byte
  let n = okay
  let n = replace {p = \a => LTE a length} (sym $ plusSuccRightSucc ofs cnt) n
  pokeBytes {okay = n} cptr (S ofs) bytes

export
unsafeToNullTerminated
  : LinearIO io
  => (1 _ : CPtr (Bytes can_free can_read can_write length))
  -> L io {use=1} (CPtr (NullTerminated can_free))
unsafeToNullTerminated (MkCPtr ptr) = pure1 $ MkCPtr ptr

export
unsafeToBytes
  : LinearIO io
  => (1 _ : CPtr (NullTerminated can_free))
  -> (0 length : Nat)
  -> {default True can_read  : Bool}
  -> {default True can_write : Bool}
  -> L io {use=1} (CPtr (Bytes can_free can_read can_write length))
unsafeToBytes (MkCPtr ptr) _ = pure1 $ MkCPtr ptr

-- TODO: behavior of length on strings containing '\0' is weird (?
export
packString
  : LinearIO io
  => String
  -> {default True can_free : Bool}
  -> L io {use=1} (CPtr (NullTerminated can_free))
packString str = do
  cptr <- malloc (S (length str))
  cptr <- pokeBytes {okay = believe_me ()} cptr 0 ((map (cast . ord) $ unpackVect str) `snoc` 0)
  let (MkCPtr ptr) = cptr
  pure1 $ MkCPtr ptr

export
packBytes
  : LinearIO io
  => {length : Nat}
  -> Vect length CUInt8
  -> {default True can_read  : Bool}
  -> {default True can_write : Bool}
  -> L io {use=1} (CPtr (Bytes True can_read can_write length))
packBytes bytes = do
  cptr <- malloc length
  cptr <- pokeBytes {okay = lteRefl} cptr 0 bytes
  let (MkCPtr ptr) = cptr
  pure1 $ MkCPtr ptr

export
unpackBytes
  : LinearIO io
  => {length : Nat}
  -> (1 _ : CPtr (Bytes can_free True can_write length))
  -> L io {use=1} (Res (Vect length CUInt8) (\_ => CPtr (Bytes can_free True can_write length)))
unpackBytes cptr = do
  bytes # cptr <- peekBytes {okay = lteRefl} cptr 0 length
  pure1 $ bytes # cptr


text:
import Aoc
import Data.String.Parser

pfoldl1 : Parser (a -> a -> a) -> Parser a -> Parser a
pfoldl1 o t = hchainl t o t

pPlus : Parser (Integer -> Integer -> Integer)
pPlus = (+) <$ string " + "
pTimes : Parser (Integer -> Integer -> Integer)
pTimes = (*) <$ string " * "
pExpr1 : Parser Integer
pExpr1 = pfoldl1 (pPlus <|> pTimes) $ integer <|> parens pExpr1
pExpr2 : Parser Integer
pExpr2 = pfoldl1 pTimes $ pfoldl1 pPlus $ integer <|> parens pExpr2

main : IO ()
main = do
  lines <- readLines
  putStr "*   "; printLn $ sum <$> traverse (map fst . parse pExpr1) lines
  putStr "**  "; printLn $ sum <$> traverse (map fst . parse pExpr2) lines


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

module API.Web.HTML.Window

import API.Web.HTML.Document
import API.Web.Time.HighResolution
import IdrisScript

%access public export
%default total

||| An HTML Window as of
||| https://html.spec.whatwg.org/multipage/browsers.html#window
record Window where
  constructor New
  ||| The `Document` associated with `window`.
  document : API.Web.HTML.Document.Document
  self     : Ptr

||| A FrameRequestCallback is the function to call when it's time to update an
||| animation for the next repaint. The callback has one single argument, a
||| DOMHighResTimeStamp, which indicates the current time for when
||| requestAnimationFrame starts to fire callbacks.
FrameRequestCallback : Type
FrameRequestCallback = DOMHighResTimeStamp -> JS_IO ()

||| RequestAnimationFrame tells the browser that you wish to perform an
||| animation and requests that the browser call a specified function to update
||| an animation before the next repaint. The method takes as an argument a
||| callback to be invoked before the repaint.
-- I would love to have this as a Nat instead of an Int. It is specified that
-- this method returns an unsigned long, but Javascript has a weird concept
-- of numbers, so we somehow ended up using Ints.
partial
requestAnimationFrame : Window -> FrameRequestCallback -> JS_IO $ Maybe Int
requestAnimationFrame (New _ self) callback = let
    id = jscall "%0.requestAnimationFrame(%1)"
                (JSRef -> JsFn FrameRequestCallback -> JS_IO JSRef)
                self (MkJsFn callback)
  in
    case !(IdrisScript.pack !id) of
         (JSNumber ** n) => pure $ Just $ fromJS n
         _               => pure Nothing

||| defaultWindow is a default implementation of Window, intended to be used in
||| in a browser.
defaultWindow : JS_IO $ Maybe Window
defaultWindow = case !maybeDocument of
    Nothing         => pure Nothing
    (Just document) => map Just $
                       API.Web.HTML.Window.New <$> pure document <*> self
  where
    self : JS_IO JSRef
    self = jscall "window" (JS_IO JSRef)

    maybeDocument : JS_IO $ Maybe API.Web.HTML.Document.Document
    maybeDocument = let
        docRef = join $ jscall "%0.document" (JSRef -> JS_IO JSRef) <$> self
      in
        -- right now, this will never fail, because an HTML Document is pretty
        -- much an empty type.
        Just <$> map API.Web.HTML.Document.New docRef

max_stars_repo_name: blau-io/idris-html

max_issues_repo_name: blau-io/idris-html

max_forks_repo_name: blau-io/idris-html


text:
import ListLast

my_reverse : List a -> List a
my_reverse xs with (listLast xs)
  my_reverse [] | Empty = []
  my_reverse (xs' ++ [x]) | (NonEmpty xs' x) = x :: my_reverse xs'

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
||| We need at least three different code generators for
||| WebIDL types and arguments. When used in the FFI, they should
||| be mapped to external types and primitives. In API functions,
||| however, they should be mapped to types convenient for
||| users of the API. Same for return types, but there, the rules
||| about what is possible are different.
|||
||| Finally, types affect how we adjust values and return values
||| in function implementations.
module Text.WebIDL.Codegen.Args

import Data.List
import Data.List1
import Text.WebIDL.Codegen.Util
import Text.WebIDL.Encoder as E

public export
record PrettyArg where
  constructor MkPrettyArg
  name : ArgumentName
  doc  : Doc ()

export
argIdent : PrettyArg -> IdrisIdent
argIdent = fromString . value . name

public export
PrettyArgs : Type
PrettyArgs = List PrettyArg

--------------------------------------------------------------------------------
--          FFI
--------------------------------------------------------------------------------

nullableFFI :  (Prec -> a -> Doc ()) -> Prec -> Nullable a -> Doc ()
nullableFFI f p (MaybeNull x) = prettyCon p "Nullable" [f App x]
nullableFFI f p (NotNull x)   = f p x

mutual
  simpleFFI : Prec -> SimpleType -> Doc ()
  simpleFFI p Undef            = "Undefined"
  simpleFFI p Boolean          = "Boolean"
  simpleFFI p (Interface _ x)  = pretty x.value
  simpleFFI p (Dictionary x)   = pretty x.value
  simpleFFI p (Mixin x)        = pretty x.value
  simpleFFI p (Primitive x)    = pretty x
  simpleFFI p (Unchangeable x) = pretty x
  simpleFFI p (Enum x)         = "String"
  simpleFFI p (Array x)        = prettyCon p "Array" [ffi App x]
  simpleFFI p (Record x y)     = prettyCon p "Record" [pretty x, ffi App y]

  unionFFI : Prec -> List1 SimpleType -> Doc ()
  unionFFI p ts = prettyCon p ("Union" <+> pretty (length $ forget ts))
                              (map (simpleFFI App) $ forget ts)
  export
  ffi : Prec -> CGType -> Doc ()
  ffi p Any         = "AnyPtr"
  ffi p (Promise x) = prettyCon p "Promise" [ffi App x]
  ffi p (Simple x)  = nullableFFI simpleFFI p x
  ffi p (Union x)   = nullableFFI unionFFI p x

--------------------------------------------------------------------------------
--          API
--------------------------------------------------------------------------------

nullableAPI :  (Prec -> a -> Doc ()) -> Prec -> Nullable a -> Doc ()
nullableAPI f p (MaybeNull x) = prettyCon p "Maybe" [f App x]
nullableAPI f p (NotNull x)   = f p x

mutual
  simpleAPI : Maybe Nat -> Prec -> SimpleType -> Doc ()
  simpleAPI (Just k) _ (Dictionary _)     = pretty "t" <+> pretty k
  simpleAPI (Just k) _ (Mixin _)          = pretty "t" <+> pretty k
  simpleAPI (Just k) _ (Interface True _) = pretty "t" <+> pretty k
  simpleAPI Nothing _ (Dictionary x)      = pretty x.value
  simpleAPI Nothing _ (Mixin x)           = pretty x.value
  simpleAPI _ _        (Interface _ x)    = pretty x.value
  simpleAPI _ _ Undef                     = "Undefined"
  simpleAPI _ _ Boolean                   = "Bool"
  simpleAPI _ _ (Primitive x)             = pretty x
  simpleAPI _ _ (Unchangeable x)          = pretty x
  simpleAPI _ _ (Enum x)                  = pretty x.value
  simpleAPI _ p (Array x)                 = prettyCon p "Array" [ffi App x]
  simpleAPI _ p (Record x y)              = prettyCon p "Record" [pretty x, ffi App y]

  unionAPI : Prec -> List1 SimpleType -> Doc ()
  unionAPI p (h ::: t) =
    let simple = simpleAPI Nothing Open
        brkt   = align . sep $  ["[" <++> simple h]
                             ++ map ("," <++>) (map simple t)
                             ++ ["]"]
     in prettyCon p "NS I" [brkt]

  api : Maybe Nat -> Prec -> CGType -> Doc ()
  api _ p Any         = "Any"
  api _ p (Promise x) = prettyCon p "Promise" [ffi App x]
  api k p (Simple x)  = nullableAPI (simpleAPI k) p x
  api _ p (Union x)   = nullableAPI unionAPI p x

--------------------------------------------------------------------------------
--          Return Types
--------------------------------------------------------------------------------

export
ret : Prec -> CGType -> Doc ()
ret p (Union $ MaybeNull xs) =
  let u = if all SimpleType.safeCast xs
             then unionAPI App xs
             else unionFFI App xs

   in prettyCon p "Maybe" [u]

ret p t@(Union $ NotNull xs) =
  if all SimpleType.safeCast xs then api Nothing p t else ffi p t

ret p t             = api Nothing p t

returnTypeFFI' : (io : Doc ()) -> ReturnType -> Doc ()
returnTypeFFI' io Undefined     = io <++> "()"
returnTypeFFI' io (Def t)       = prettyCon Open io [ffi App t]
returnTypeFFI' io (UndefOr t _) =
  prettyCon Open io [prettyCon App "UndefOr" [ffi App t]]

returnTypeFFI : ReturnType -> Doc ()
returnTypeFFI = returnTypeFFI' "PrimIO"

returnTypeAPI : ReturnType -> Doc ()
returnTypeAPI Undefined     = "JSIO ()"
returnTypeAPI (Def t)       = prettyCon Open "JSIO" [ret App t]
returnTypeAPI (UndefOr t _) =
  prettyCon Open "JSIO" [prettyCon App "Optional" [ret App t]]

export
constTpe : CGConstType -> Doc ()
constTpe = pretty . primitive

--------------------------------------------------------------------------------
--          Default Arg
--------------------------------------------------------------------------------

export
Pretty StringLit where
  pretty v = pretty v.value

export
Pretty FloatLit where
  pretty v = pretty $ E.floatLit v

export
Pretty IntLit where
  pretty (Hex k) = pretty $ E.toDigits "0x" 16 k
  pretty (Oct 0) = pretty "0"
  pretty (Oct k) = pretty $ E.toDigits "0o" 8 k
  pretty (I x)   = pretty x

export
Pretty ConstValue where
  pretty (B x) = pretty x
  pretty (F x) = pretty x
  pretty (I x) = pretty x

defltS : SimpleType -> Default -> Maybe (Doc ())
defltS Boolean (C $ B x)   = Just $ pretty x
defltS (Primitive _) (S x) = Just $ pretty x
defltS (Primitive _) (C x) = Just $ pretty x
defltS _ _                 = Nothing

unionD : Prec -> List1 SimpleType -> Default -> Maybe (Doc ())
unionD p ts d =
  let m = choiceMap (`defltS` d) ts
   in map (\x => prettyCon p "inject" [x]) m

export
deflt : Bool -> Prec -> CGType -> Default -> Maybe (Doc ())
deflt _ p Any Null  = Just $ prettyCon p "MkAny" ["$ null {a = ()}"]
deflt _ p Any (S x) = Just $ prettyCon p "MkAny" [pretty x]
deflt _ p Any (C x) = Just $ prettyCon p "MkAny" [pretty x]
deflt _ _ (Simple $ MaybeNull x) Null = Just "Nothing"

deflt _ p (Simple $ MaybeNull x) d =
  map (\v => prettyCon p "Just" [v]) (defltS x d)

deflt _ _ (Simple $ NotNull x) d = defltS x d

deflt _ p (Union $ MaybeNull x) Null = Just "Nothing"

deflt True p (Union $ MaybeNull x) d =
  map (\v => prettyCon p "Just" [v]) (unionD App x d)

deflt True p (Union $ NotNull x) d = unionD p x d
deflt _ _ _ _ = Nothing

--------------------------------------------------------------------------------
--          Arguments
--------------------------------------------------------------------------------

argTypeFFI : Prec -> CGArg -> Doc ()
argTypeFFI p (Mandatory _ t)  = ffi p t
argTypeFFI p (VarArg _ t)     =
  prettyCon p "IO" [prettyCon App "Array" [ffi App t]]
argTypeFFI p (Optional _ t _) = prettyCon p "UndefOr" [ffi App t]

argTypeAPI : Nat -> Prec -> CGArg -> Doc ()
argTypeAPI k p (Mandatory _ t)  = api (Just k) p t
argTypeAPI _ p (VarArg _ t)     = prettyCon p "List" [api Nothing App t]
argTypeAPI k p (Optional _ t _) = prettyCon p "Optional" [api (Just k) App t]

arg : PrettyArg -> Doc ()
arg a = parens $ hsep [pretty (argIdent a), ":", a.doc]

prettyArgFFI : CGArg -> Doc ()
prettyArgFFI = argTypeFFI Open

prettyArgAPI : Nat -> CGArg -> PrettyArg
prettyArgAPI k a = let doc = argTypeAPI k Open a
                    in MkPrettyArg (argName a) doc

--------------------------------------------------------------------------------
--          Functions
--------------------------------------------------------------------------------

funTypeFFI : (name : IdrisIdent) -> ReturnType -> Args -> Doc ()
funTypeFFI n t as = typeDecl n (returnTypeFFI t) (map prettyArgFFI as)

funType : (name : IdrisIdent) -> ReturnType -> Args -> Doc ()
funType n t as =
  let (implicits,autos,explicits) = run 0 as
   in typeDeclWithImplicits n (returnTypeAPI t) implicits (autos ++ explicits)
  where run : Nat -> Args -> (List $ Doc(), List $ Doc (), List $ Doc ())
        run _ []        = ([],[],[])
        run k (a :: as) =
          case CGArg.inheritance a of
               Just (n,_) =>
                 let k2  = S k
                     pk2 = "t" <+> pretty' k2
                     (implicits,autos,explicits) = run k2 as
                     impl = "(0 _ : JSType" <++> pk2 <+> ")"
                     aut = hsep ["{auto 0 _ : Elem"
                                , pretty n.value
                                ,"(Types" <++> pk2 <+> ")}"
                                ]
                     expl = arg (prettyArgAPI k2 a)
                  in (impl :: implicits, aut :: autos, expl :: explicits)
               Nothing =>
                 let (implicits,autos,explicits) = run k as
                     expl = arg (prettyArgAPI k a)
                  in (implicits, autos, expl :: explicits)

export
callbackFFI :  (obj  : Identifier)
            -> (name : IdrisIdent)
            -> (impl : String)
            -> (args : Args)
            -> (tpe  : ReturnType)
            -> String
callbackFFI o n impl as t =
  let cbTpe  = functionTypeOnly (returnTypeFFI' "IO" t)
                                (map prettyArgFFI as)

      retTpe = "PrimIO" <++> pretty' (o.value)

   in show . indent 2 $ vsep [ ""
                             , "export"
                             , pretty' impl
                             , typeDecl n retTpe [cbTpe]
                             ]

export
callbackAPI :  (obj  : Identifier)
            -> (name : IdrisIdent)
            -> (prim : IdrisIdent)
            -> (args : Args)
            -> (tpe  : ReturnType)
            -> String
callbackAPI o n prim as t =
  let cbTpe  = functionTypeOnly (returnTypeFFI' "IO" t)
                                (map prettyArgFFI as)

      retTpe = "JSIO" <++> pretty' (o.value)
      impl   = pretty' n <++> "cb = primJS $" <++> pretty prim <++> "cb"

   in show . indent 2 $ vsep [ ""
                             , "export"
                             , typeDecl n retTpe [cbTpe]
                             , impl
                             ]

export
funFFI :  (name : IdrisIdent)
       -> (impl : String)
       -> (args : Args)
       -> (tpe  : ReturnType)
       -> String
funFFI n impl as t =
   show . indent 2 $ vsep ["", "export", pretty impl, funTypeFFI n t as ]

export
namespacedIdent : (ns : Kind) -> (name : IdrisIdent) -> String
namespacedIdent ns n = fastConcat ["\"",kindToString ns,".",show n,"\""]

fun' :  (ns         : Kind)
     -> (name       : IdrisIdent)
     -> (prim       : IdrisIdent)
     -> (args       : Args)
     -> (undefs     : List String)
     -> (returnType : ReturnType)
     -> List (Doc ())
fun' ns name prim as us rt =
  let vs      = take (length as) (unShadowingArgNames name)

      appVs   = align . sep $ zipWith adjVal vs as ++ map pretty' us

      primNS  = kindToString ns ++ "." ++ show prim

      primCall = if sameType rt
                    then "primJS"
                    else "tryJS " ++ namespacedIdent ns name

      lhs     = pretty' . fastConcat . intersperse " " $ show name :: vs

      impl    = lhs <++> (align . sep) [ "=" <++> pretty primCall
                                       , "$" <++> pretty primNS <++> appVs
                                       ]
   in ["", "export", funType name rt as, impl]

  where adjVal : String -> CGArg -> Doc ()
        adjVal v a =
          -- If the same type is used at the FFI and the API,
          -- there is no need to convert the value.
          -- If the value should be upcast to a parent type (`inheritance` returns
          -- a `Just`), we upcast the value using a number of nested `map`s,
          -- corresponding to the number of functors around
          -- the type (at most two layers: `Optional` and `Maybe`),
          -- otherwise, we just use `toFFI` to convert it.
          case (sameType a, snd <$> inheritance a) of
            (True,_)            => pretty v
            (False,Nothing)     => parens ("toFFI" <++> pretty v)
            (False,Just Direct) => parens ("up" <++> pretty v)
            (False,Just May)    => parens ("mayUp" <++> pretty v)
            (False,Just Opt)    => parens ("optUp" <++> pretty v)
            (False,Just OptMay) => parens ("omyUp" <++> pretty v)

export
fun :  (ns   : Kind)
    -> (name : IdrisIdent)
    -> (prim : IdrisIdent)
    -> Args
    -> ReturnType
    -> String
fun ns name prim as t =
  let funImpl       = fun' ns name prim as [] t

      -- function without optional args
      as2      = filter (not . isOptional) as
      undefs   = List.replicate (length as `minus` length as2) "undef"
      funImpl2 = if null undefs then []
                 else fun' ns name2 prim as2 undefs t

   in show . indent 2 $ vsep (funImpl ++ funImpl2)

  where name2 : IdrisIdent
        name2 = case name of
                     II v prf     => fromString $ v ++ "'"
                     Prim v       => Prim (v ++ "'")
                     Underscore v => fromString $ v ++ "'"


text:
module Main
--module IdrisWeb.Form.FormTest
import Cgi
import Effects
--import Debug.Trace

total
outputCommaList : List String -> String
outputCommaList [] = ""
outputCommaList [x] = x ++ "."
outputCommaList (x :: y :: []) = x ++ " and " ++ y ++ "."
outputCommaList (x :: xs) = x ++ ", " ++ outputCommaList xs

sampleHandler : Maybe String ->
                Maybe Int ->
                FormHandler [CGI (InitialisedCGI TaskRunning), SQLITE ()]
sampleHandler (Just name) (Just age) = do (output ("Your name is: " ++ name ++
                                            ", and you are " ++ (show age) ++ " years old!"))
                                          pure ()
sampleHandler _ _ = do output "There was an error processing form data."
                       pure ()

sampleHandler2 : Maybe String ->
                Maybe Int ->
                FormHandler [CGI (InitialisedCGI TaskRunning), SQLITE ()]
sampleHandler2 (Just name) (Just age) = do (output ("Your name is: " ++ name ++
                                             ", and you are " ++ (show age) ++ " years old!"))
                                           pure ()
sampleHandler2 _ _ = do output "There was an error processing form data."
                        pure ()

-- Some syntax macro magic might be nice here
handlers : HandlerList
handlers = [(([FormString, FormInt], [CgiEffect, SqliteEffect]) ** (sampleHandler, "sampleHandler")),
            (([FormString, FormInt], [CgiEffect, SqliteEffect]) ** (sampleHandler2, "sampleHandler2"))]

sampleForm : UserForm --UserForm
sampleForm = do addTextBox "Name: " FormString (Just "Simon")
                addTextBox "Age: " FormInt Nothing-- 21
                useEffects [CgiEffect, SqliteEffect]
                addSubmit sampleHandler handlers

cgiAction : CGIProg [] ()
cgiAction = do output "
Simon's awesome sauce form stuff!
\n"
               handlervar <- queryPostVar "handler"
               post_vars <- getPOSTVars
               let post_vars_str = foldr (\(k, v), str => str ++ k ++ " :-> " ++ v ++ "
") "" post_vars
               output "Post vars:
"
               output post_vars_str
               --sequence (map (\(name, val) => output $ "Name: " ++ name ++ ", " ++ val ++ "
") post_vars)
               case handlervar of
                    -- If at all poss, this needs to be cleaner. Users shouldn't have to type this
                    Just _ => do res <- handleForm handlers
                                 pure ()
                    Nothing => do addForm "sampleForm" "formtest" sampleForm
                                  pure ()
main : IO ()
main = do runCGI [initCGIState] cgiAction
          pure ()

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
import Data.List.Views

palindrome : Eq a => List a -> Bool
palindrome xs with (vList xs)
  palindrome [] | VNil = True
  palindrome [x] | VOne = True
  palindrome (x :: (ys ++ [y])) | (VCons rec)
    = if x == y
      then palindrome ys | rec
      else False


text:
module Quantities.SIPrefixes

import Quantities.Core

%default total
%access public export

makePrefix : Integer -> Unit q -> Unit q
makePrefix i (MkUnit e us) = MkUnit (e+i) us

-- List of prefixes from
-- http://en.wikipedia.org/wiki/Metric_prefix

yotta : Unit q -> Unit q
yotta = makePrefix 24

zetta : Unit q -> Unit q
zetta = makePrefix 21

exa : Unit q -> Unit q
exa = makePrefix 18

peta : Unit q -> Unit q
peta = makePrefix 15

tera : Unit q -> Unit q
tera = makePrefix 12

giga : Unit q -> Unit q
giga = makePrefix 9
G : Unit q -> Unit q
G = giga

mega : Unit q -> Unit q
mega = makePrefix 6
M : Unit q -> Unit q
M = mega

kilo : Unit q -> Unit q
kilo = makePrefix 3
k : Unit q -> Unit q
k = kilo

hecto : Unit q -> Unit q
hecto = makePrefix 2

deca : Unit q -> Unit q
deca = makePrefix 1
da : Unit q -> Unit q
da = deca

-- ################## --

deci : Unit q -> Unit q
deci = makePrefix (-1)

centi : Unit q -> Unit q
centi = makePrefix (-2)

milli : Unit q -> Unit q
milli = makePrefix (-3)

micro : Unit q -> Unit q
micro = makePrefix (-6)

nano : Unit q -> Unit q
nano = makePrefix (-9)

pico : Unit q -> Unit q
pico = makePrefix (-12)

femto : Unit q -> Unit q
femto = makePrefix (-15)

atto : Unit q -> Unit q
atto = makePrefix (-18)

zepto : Unit q -> Unit q
zepto = makePrefix (-21)

yocto : Unit q -> Unit q
yocto = makePrefix (-24)

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities