text:
||| Metadata about a data type's constructor and field names.
|||
||| Since for the time being, record syntax is still under discussion,
||| records are not yet treated any differently from other
||| product types. This might well change in the future, once
||| the issues about record syntax are resolved.
|||
||| Also, it seems not yet to be possible to get access to an
||| operator's fixity through elaborator reflection. We try to make
||| this information available as soon as possible.
module Generics.Meta

import Data.List
import Generics.SOP

%default total

||| Name and integer index of constructor arguments
public export
data ArgName : Type where

  ||| Name and index of a named argument
  NamedArg   : (index : Int) -> (name : String) -> ArgName

  ||| Index of an unnamed argument
  UnnamedArg : (index : Int) -> ArgName

||| Tries to extract an argument's name.
public export
getName : ArgName -> Maybe String
getName (NamedArg _ name) = Just name
getName (UnnamedArg _)    = Nothing

||| Namespace, name and arguments of a single data constructor
|||
||| The arguments are wrapped in an n-ary product
||| parameterized by the constant functor, to make them
||| accessible to the SOP combinators.
public export
record ConInfo_ (k : Type) (ks : List k) where
  constructor MkConInfo

  ||| Namespace of the constructor
  conNS   : List String

  ||| Name of the constructor
  conName : String

  ||| Constructor arguments
  args    : NP_ k (K ArgName) ks

||| Alias for `ConInfo_` with the `k` parameter being implicit.
public export
ConInfo : {k : Type} -> (ks : List k) -> Type
ConInfo = ConInfo_ k

||| Tries to extract the set of argument names from
||| a constructor.
public export
argNames : ConInfo ks -> Maybe (NP (K String) ks)
argNames = htraverse getName . args

||| Returns `True` if a constructor's `conName` consists
||| only of non-alphanumeric characters.
public export
isOperator : String -> Bool
isOperator = all (not . isAlphaNum) . unpack

||| Wraps a function name in parentheses if it is an operator
public export
wrapOperator : String -> String
wrapOperator n = if isOperator n then "(" ++ n ++ ")" else n

||| Namespace, name and constructors of a data type.
|||
||| The constructors are wrapped in an n-ary product
||| parameterized by `ConInfo`, to make them
||| accessible to the SOP combinators.
public export
record TypeInfo' (k : Type) (kss : List $ List k) where
  constructor MkTypeInfo

  ||| Namespace of the data type
  typeNS       : List String

  ||| Name of the data type
  typeName     : String

  ||| n-ary product of the data type's constructors
  constructors : NP_ (List k) (ConInfo_ k) kss

||| Alias for `TypeInfo'` with the `k` parameter being implicit.
public export
TypeInfo : {k : Type} -> (kss : List $ List k) -> Type
TypeInfo = TypeInfo' k

--------------------------------------------------------------------------------
--          Meta
--------------------------------------------------------------------------------

||| Interface to make a data type's metadata available at runtime.
|||
||| In order to get access to the meta data, it is often more convenient
||| to use function `metaFor`.
public export
interface Generic t code => Meta t code | t where
  constructor MkMeta
  meta : TypeInfo' Type code

||| Return's the `TypeInfo` of a data type. This is
||| an alias for `meta {t = t}`.
public export
metaFor : (0 t : Type) -> Meta t code => TypeInfo code
metaFor t = meta {t = t}

--------------------------------------------------------------------------------
--          Show Implementations
--------------------------------------------------------------------------------

-- Displays a single applied constructor wrapping it in parens if necessary
showC : NP (Show . f) ks => (p : Prec) -> ConInfo ks -> NP f ks -> String

-- No need to wrap a constant in parens
showC _ info []   = info.conName

-- This uses `showCon` from the Prelude to wrap an applied
-- constructor in parentheses depending on `p`.
showC p info args =
  let con = wrapOperator info.conName
   in maybe (showOther con) (showRecord con) (argNames info)

  where showNamed : Show a => String -> a -> String
        showNamed name v = name ++ " = " ++ show v

        showRecord : (con : String) -> NP (K String) ks -> String
        showRecord con names =
          let applied = hcliftA2 (Show . f) showNamed names args
              inner   = intersperse ", " (collapseNP applied)
           in showCon p con (" { " ++ concat inner ++ " }")

        showOther : (con : String) -> String
        showOther con =
          let argStr = hconcat $ hcmap (Show . f) showArg args
           in showCon p con argStr

showSOP :  (all : POP (Show . f) kss)
        => Prec -> TypeInfo kss -> SOP f kss -> String
showSOP {all = MkPOP _} p (MkTypeInfo _ _ cons) =
  hconcat . hcliftA2 (NP $ Show . f) (showC p) cons . unSOP

||| Generic show function.
|||
||| This is still quite basic. It uses prefix notation for operators
||| and data types with List constructors (`Nil` and `(::)`)
||| are not yet displayed using list syntax ("[a,b,c]").
|||
||| However, constructors with only named arguments are displayed
||| in record syntax style.
public export
genShowPrec : Meta t code => POP Show code => Prec -> t -> String
genShowPrec p = showSOP p (metaFor t) . from


text:
-- ------------------------------------------------------------- [ Char.idr ]
-- Module      : Lightyear.Char
-- Description : Character-related parsers.
--
-- This code is distributed under the BSD 2-clause license.
-- See the file LICENSE in the root directory for its full text.
--
-- This code is (mostly) a port of Daan Leijen's Text.Parsec.Char library.
-- --------------------------------------------------------------------- [ EOH ]
module Lightyear.Char

import        Data.Strings
import public Data.Vect
import public Data.Fin

import public Control.Monad.Identity

import Lightyear.Core
import Lightyear.Combinators

-- Maybe somehow return proof that returned Char is the one passed as arg?
-- `char a <|> char b` should return `Either (c = a) (c = b)`
-- char : (Monad m, Stream Char str) => (c : Char) -> Covers (Subset Char (Equal c)) t => ParserT str m t
||| A parser that matches some particular character
export
char : (Monad m, Stream Char str) => Char -> ParserT str m Char
char c = satisfy (== c) <?> "character '" ++ singleton c ++ "'"

||| oneOf cs succeeds if the current character is in the supplied
||| list of characters @cs@. Returns the parsed character. See also
||| 'satisfy'.
|||
|||   vowel  = oneOf "aeiou"
export
oneOf : (Monad m, Stream Char str) => String -> ParserT str m Char
oneOf cs = satisfy (\c => elem c $ unpack cs)

||| As the dual of 'oneOf', @noneOf cs@ succeeds if the current
||| character /not/ in the supplied list of characters @cs@. Returns the
||| parsed character.
|||
|||  consonant = noneOf "aeiou"
export
noneOf :  (Monad m, Stream Char str) => String -> ParserT str m Char
noneOf cs = satisfy (\c => not $ elem c $ unpack cs)

||| Parses a white space character (any character which satisfies 'isSpace')
||| Returns the parsed character.
export
space : (Monad m, Stream Char s) => ParserT s m Char
space = satisfy isSpace <?> "space"

||| Skips /zero/ or more white space characters. See also 'skipMany'.
export
spaces : (Monad m, Stream Char s) => ParserT s m ()
spaces = skip (many Lightyear.Char.space)  <?> "white space"

||| Parses a newline character (\'\\n\'). Returns a newline character.
export
newline : (Monad m, Stream Char s) => ParserT s m Char
newline = char '\n' <?> "lf new-line"

||| Parses a carriage return character (\'\\r\') followed by a newline character (\'\\n\').
||| Returns a newline character.
export
crlf : (Monad m, Stream Char s) => ParserT s m Char
crlf = char '\r' *> char '\n' <?> "crlf new-line"

||| Parses a CRLF (see 'crlf') or LF (see 'newline') end-of-line.
||| Returns a newline character (\'\\n\').
|||
||| endOfLine = newline <|> crlf
export
endOfLine : (Monad m, Stream Char s) => ParserT s m Char
endOfLine           = newline <|> crlf       <?> "new-line"

||| Parses a tab character (\'\\t\'). Returns a tab character.
export
tab : (Monad m, Stream Char s) => ParserT s m Char
tab = char '\t'             <?> "tab"

||| Parses an upper case letter (a character between \'A\' and \'Z\').
||| Returns the parsed character.
export
upper : (Monad m, Stream Char s) => ParserT s m Char
upper = satisfy isUpper       <?> "uppercase letter"

||| Parses a lower case character (a character between \'a\' and \'z\').
||| Returns the parsed character.
export
lower : (Monad m, Stream Char s) => ParserT s m Char
lower = satisfy isLower       <?> "lowercase letter"

||| Parses a letter or digit (a character between \'0\' and \'9\').
||| Returns the parsed character.
export
alphaNum : (Monad m, Stream Char s) => ParserT s m Char
alphaNum            = satisfy isAlphaNum    <?> "letter or digit"

||| Parses a letter (an upper case or lower case character). Returns the
||| parsed character.
export
letter : (Monad m, Stream Char s) => ParserT s m Char
letter              = satisfy isAlpha       <?> "letter"

||| Matches a single digit
export
digit : (Monad m, Stream Char s) => ParserT s m (Fin 10)
digit = satisfyMaybe fromChar
  where fromChar : Char -> Maybe (Fin 10)
        fromChar '0' = Just FZ
        fromChar '1' = Just (FS (FZ))
        fromChar '2' = Just (FS (FS (FZ)))
        fromChar '3' = Just (FS (FS (FS (FZ))))
        fromChar '4' = Just (FS (FS (FS (FS (FZ)))))
        fromChar '5' = Just (FS (FS (FS (FS (FS (FZ))))))
        fromChar '6' = Just (FS (FS (FS (FS (FS (FS (FZ)))))))
        fromChar '7' = Just (FS (FS (FS (FS (FS (FS (FS (FZ))))))))
        fromChar '8' = Just (FS (FS (FS (FS (FS (FS (FS (FS (FZ)))))))))
        fromChar '9' = Just (FS (FS (FS (FS (FS (FS (FS (FS (FS (FZ))))))))))
        fromChar _   = Nothing

||| Matches an integer literal
export
integer : (Num n, Monad m, Stream Char s) => ParserT s m n
integer = do minus <- opt (char '-')
             ds <- some digit
             let theInt = getInteger ds
             case minus of
               Nothing => pure (fromInteger theInt)
               Just _  => pure (fromInteger ((-1) * theInt))
  where getInteger : List (Fin 10) -> Integer
        getInteger = foldl (\a => \b => 10 * a + cast b) 0

||| Parses a hexadecimal digit (a digit or a letter between \'a\' and
||| \'f\' or \'A\' and \'F\'). Returns the parsed character.
export
hexDigit : (Monad m, Stream Char s) => ParserT s m Char
hexDigit = satisfy isHexDigit <?> "hexadecimal digit"

||| Parses an octal digit (a character between \'0\' and \'7\'). Returns
||| the parsed character.
export
octDigit : (Monad m, Stream Char s) => ParserT s m Char
octDigit = satisfy isOctDigit <?> "octal digit"

||| This parser succeeds for any character. Returns the parsed character.
export
anyChar : (Monad m, Stream Char s) => ParserT s m Char
anyChar  = anyToken <?> "any character"

ext: idr

max_stars_repo_name: Mr-Andersen/lightyear

max_issues_repo_name: Mr-Andersen/lightyear

max_forks_repo_name: Mr-Andersen/lightyear


text:
||| An example Resource Dependent EDSL (based upon Robin Milner's BiGraphs) to specify the physical and behavioural connections for mobile devices.
|||
||| This EDSL encapsulates the following concepts:
|||
||| 1. Messages, an atomic entity of arity zero.
||| 2. Devices, a complex entity (nesting) that contains many messages, and
||| artiy one. Devices have at most one connection to another device.
||| 3. Rooms, a complex entity (merge) of arity zero that contains many devices.
||| 4. Buildings, a complex entity (merge) of arity zero that contains many
||| rooms
||| 5. Regions, a complex entity (parallel) of arity zero that situates buildings in different regions.
|||
||| We define a handler to construct EDSL instances into a pure BiGraph form based upon an algebraic graph representation.
module Examples.BiGraph

import Data.Vect
import Resources

%default total
%access public export

{- [ NOTE ] The types for our Wireless EDSL -}

||| Device Types
data DTy = MOBILE | LAPTOP

||| Node types.
data Ty = ROOM | BUILDING | DEVICE DTy | MESSAGE

||| Mobile devices can support upto two connections, laptops ten.
maxConn : DTy -> Nat
maxConn MOBILE = 2
maxConn LAPTOP = 10

||| An abstract resource to capture device states.
|||
||| As the device is used the number of free connections will decrease until zero.
|||
||| @dtype The devce type.
data StateD : (dtype : DTy) -> Type where
  ||| Capture connection status and max number of connections.
  MkD : (connected : Bool) -> (curr : Nat) -> StateD ty

||| Default status of unconnected and a calculated number of connections.
defState : (type : DTy) -> StateD type
defState type = MkD False (maxConn type)

||| Map node types to an abstract resource.
|||
||| 1. Rooms, and messages, contain placement status.
||| 2. Buildings have no associated abstract state.
||| 3. Devices have type `StateD`
|||
CalcStateType : Ty -> Type
CalcStateType ROOM = Bool
CalcStateType BUILDING = ()
CalcStateType (DEVICE ty) = StateD ty
CalcStateType MESSAGE = Bool

||| A predicate to capture if a node has been unassigned.
|||
||| @value The type of node.
||| @lbl the node's bound name.
||| @item the nodes abstract state.
data Unassigned : (value : Ty)
               -> (lbl : Var Ty value)
               -> (item : StateItem Ty CalcStateType value)
               -> Type where
                     -- Type       | Label | Abstract State
  URoom    : Unassigned ROOM         rm      (MkStateItem ROOM         rm  False)
  UDevice  : Unassigned (DEVICE ty)  dev     (MkStateItem (DEVICE ty)  dev (MkD False c))
  UMessage : Unassigned MESSAGE      msg     (MkStateItem MESSAGE      msg False)

||| Function to update a node's abstract state to indicate node usage.
|||
||| @item the nodes abstract state.
||| @prf  that the node has not been assigned.
Use : (item : StateItem Ty CalcStateType value)
   -> (prf  : Unassigned value lbl item)
   -> StateItem Ty CalcStateType value
Use {value = ROOM} (MkStateItem ROOM lbl False) URoom = MkStateItem ROOM lbl True
Use {value = DEVICE ty} (MkStateItem (DEVICE ty) lbl (MkD False curr)) UDevice = MkStateItem (DEVICE ty) lbl (MkD True curr)
Use {value = MESSAGE} (MkStateItem MESSAGE lbl False) UMessage = MkStateItem MESSAGE lbl True

||| A predicate to capture that a node can be assigned to.
|||
||| @thisValue The type of node.
||| @thisVar the node's bound name.
||| @item the nodes abstract state.
data CanAssign : (thisValue : Ty)
              -> (thisVar   : Var Ty valueThis)
              -> (item  : StateItem Ty CalcStateType valueThis)
              -> Type where
                        -- Type      | Label | Abstract State
   ToABuilding : CanAssign BUILDING    bld     (MkStateItem BUILDING bld ())
   ToARoom     : CanAssign ROOM        rm      (MkStateItem ROOM     rm  True)
   ToADevice   : CanAssign (DEVICE ty) dev     (MkStateItem (DEVICE ty)   dev (MkD True (S n)))

||| A predicate to capture valid nesting of nodes.
data ValidAssign : Ty -> Ty -> Type where
  IsValidAssignBR : ValidAssign BUILDING    ROOM
  IsValidAssignRD : ValidAssign ROOM        (DEVICE ty)
  IsValidAssignDM : ValidAssign (DEVICE ty) MESSAGE

||| A type level function to update the abstract state of a node to indicate it's assignment.
|||
||| @var  the node's label
||| @prfV proof that it is a valid assignment.
||| @item the nodes abstract state.
||| @prf  that the node can be assigned.
Assign : (var  : Var Ty x)
      -> (prfV : ValidAssign value x)
      -> (item : StateItem Ty CalcStateType value)
      -> (prf  : CanAssign value lbl item)
      -> StateItem Ty CalcStateType value
Assign {value = BUILDING} var prfV (MkStateItem BUILDING lbl ()) ToABuilding =
  MkStateItem BUILDING lbl ()
Assign {value = ROOM} var prfV (MkStateItem ROOM lbl True) ToARoom = MkStateItem ROOM lbl True
Assign {value = (DEVICE ty)} var prfV (MkStateItem (DEVICE ty) lbl (MkD True (S n))) ToADevice =
  MkStateItem (DEVICE ty) lbl (MkD True n)

||| A predicate to capture that a device has sufficient space to handle more connections
data CanConnect : (to   : Var Ty (DEVICE type))
               -> (item : StateItem Ty CalcStateType (DEVICE type))
               -> Type where
  HasSpace : CanConnect dev (MkStateItem (DEVICE type) lbl (MkD True (S n)))

||| A type-level function to update the abstract state of a device.
|||
||| This decreases the number of free connections.
|||
||| @item the nodes abstract state.
||| @prf  that the node can be assigned.
Connect : (item : StateItem Ty CalcStateType (DEVICE type))
       -> (prf  : CanConnect to item)
       -> StateItem Ty CalcStateType (DEVICE type)
Connect (MkStateItem (DEVICE type) lbl (MkD True (S n))) HasSpace =
    MkStateItem (DEVICE type) lbl (MkD True n)

{- [ Language Definition ] -}

data Wireless : Lang Ty CalcStateType where
  ||| Create a new building.
  NewBuilding : Wireless (Var Ty BUILDING) old (\lbl => MkStateItem BUILDING lbl () :: old)

  ||| Create a new room.
  NewRoom : Wireless (Var Ty ROOM) old (\lbl => MkStateItem ROOM lbl False :: old)

  ||| Create a new device.
  NewDevice : (type : DTy)
           -> Wireless (Var Ty (DEVICE type)) old (\lbl => MkStateItem (DEVICE type) lbl (defState type) :: old)

  ||| Create a new message.
  NewMessage  : Wireless (Var Ty MESSAGE) old (\lbl => MkStateItem MESSAGE lbl False :: old)

  ||| Insert `varX` into `varY`
  |||
  ||| @varX The child node.
  ||| @varY The parent node.
  ||| @prfValid that it is a valid assignment.
  ||| @prfFree that one can insert into `varX`.
  ||| @prfInsert that one can assign `varY`
  Insert : (varX : Var Ty x)
        -> (varY : Var Ty y)
        -> (prfValid : ValidAssign y x)
        -> (prfFree : InContext x (Unassigned x varX) old)
        -> (prfInsert : InContext y (CanAssign y varY) (update old prfFree Use))
        -> Wireless () old (const $ update (update old prfFree Use) prfInsert (Assign varX prfValid))

  ||| Connect `varX` to `varY`
  |||
  ||| @varX The sending node.
  ||| @varY The receiving node.
  ||| @prfSpaceX that `varX` can be linked.
  ||| @prfSpaceY that `varY` can be linked.
  Link : (varX : Var Ty (DEVICE typeX))
      -> (varY : Var Ty (DEVICE typeY))
      -> (prfSpaceX : InContext (DEVICE typeX) (CanConnect varX) old)
      -> (prfSpaceY : InContext (DEVICE typeY) (CanConnect varY) (update old prfSpaceX Connect))
      -> Wireless () old (const $ update (update old prfSpaceX Connect) prfSpaceY Connect)

  ||| End the specification.
  End : Wireless () old (const Nil)

{- [ NOTE ]

A high-level API to embedd language expressions within `LangM`, and calculate language proofs.

-}

||| An resource dependent EDSL to describe communication networks and state.
WIRELESS : LANG Ty CalcStateType
WIRELESS = MkLang Ty CalcStateType Wireless

||| Create a new building.
newBuilding : LangM m (Var Ty BUILDING) WIRELESS old (\lbl => MkStateItem BUILDING lbl () :: old)
newBuilding = Expr $ NewBuilding

||| Create a new room.
newRoom : LangM m (Var Ty ROOM) WIRELESS old (\lbl => MkStateItem ROOM lbl False :: old)
newRoom = Expr $ NewRoom

||| Create a new device.
|||
||| @type The devices type.
newDevice : (type : DTy)
         -> LangM m (Var Ty (DEVICE type))
                    WIRELESS
                    old
                    (\lbl => MkStateItem (DEVICE type) lbl (defState type) :: old)
newDevice ty = Expr $ NewDevice ty

||| Create a new message
newMessage : LangM m (Var Ty MESSAGE)
                     WIRELESS
                     old
                     (\lbl => MkStateItem MESSAGE lbl False :: old)
newMessage = Expr $ NewMessage

||| Insert `varX` into `varY`.
insert : (varX : Var Ty x)
      -> (varY : Var Ty y)
      -> {auto prfValid : ValidAssign y x}
      -> {auto prfFree : InContext x (Unassigned x varX) old}
      -> {auto prfInsert : InContext y (CanAssign y varY) (update old prfFree Use)}
      -> LangM m () WIRELESS old (const $ update (update old prfFree Use) prfInsert (Assign varX prfValid))
insert x y {prfValid} {prfFree} {prfInsert} = Expr (Insert x y prfValid prfFree prfInsert)

||| Link two devices together.
link : (varX : Var Ty (DEVICE typeX))
    -> (varY : Var Ty (DEVICE typeY))
    -> {auto prfSpaceXY : InContext (DEVICE typeX) (CanConnect varX) old}
    -> {auto prfSpaceYX : InContext (DEVICE typeY) (CanConnect varY) (update old prfSpaceXY Connect)}
    -> LangM m () WIRELESS old (const $ update (update old prfSpaceXY Connect) prfSpaceYX Connect)
link x y {prfSpaceXY} {prfSpaceYX} = Expr (Link x y prfSpaceXY prfSpaceYX)

||| End a specification.
end : LangM m () WIRELESS old (const Nil)
end = Expr End

||| Type given to programs to ensure that they are closed.
|||
WirelessDesc : (m : Type -> Type) -> Type
WirelessDesc m = LangM m () WIRELESS Nil (const Nil)

{- [ NOTE]

Here we given an example before giving the evaluation context.

-}

|||
example : WirelessDesc m
example = do
  buildingA <- newBuilding
  buildingB <- newBuilding

  roomA <- newRoom
  roomB <- newRoom
  roomC <- newRoom

  laptopA <- newDevice LAPTOP
  laptopB <- newDevice LAPTOP
  laptopC <- newDevice LAPTOP
  mobile  <- newDevice MOBILE

  msg <- newMessage

  insert roomA buildingA
  insert laptopA roomA
  insert mobile  roomA
  insert msg mobile

  insert roomB buildingA
  insert laptopB roomB

  insert roomC buildingB
  insert laptopC roomC

  link laptopA laptopC
  link mobile laptopB
  end

{- [ Evaluation context ]
-}

||| An entity has an arity, an identifier, and is typed according to the EDSLs variable type.
data Entity : (type : Type) -> (value : type) -> Type where
  MkEntity : (n : Nat) -> (arity : Nat) -> Entity type value

namespace Algebra

 ||| An algebraic graph view of a Bigraph.
 |||
 ||| The shape of a bigraph follows its algebraic definition.
 ||| The type is indexed by the entity's concrete type.
 data BiGraph : Type -> Type where
   Identity : BiGraph a

   Node : Entity a value -> BiGraph a
   Outside : String -> BiGraph a

   Nesting : (BiGraph a) -> (BiGraph a) -> BiGraph a
   Merge   : (BiGraph a) -> (BiGraph a) -> BiGraph a
   Par     : (BiGraph a) -> (BiGraph a) -> BiGraph a
   Connect : (BiGraph a) -> (BiGraph a) -> BiGraph a
   Overlay : (BiGraph a) -> (BiGraph a) -> BiGraph a

||| We map the EDSL's variable types to concrete entity specifications.
public export
RealVar Ty where
  CalcRealType ROOM       = Entity Ty ROOM
  CalcRealType BUILDING   = Entity Ty BUILDING
  CalcRealType (DEVICE x) = Entity Ty (DEVICE x)
  CalcRealType MESSAGE    = Entity Ty MESSAGE

||| A handler to construct `BiGraph` instances from `WIRELESS` specifications.
|||
||| We run the evaluation in a pure context to enable bigraph construction.
|||
||| **Note** The accumulator in this instance is a counter to generate node identifiers, and the resulting bigraph itself.
public export
Handler Ty CalcStateType Wireless (Nat, BiGraph Ty) (Basics.id) where
  handle env NewBuilding      (ctr,g) cont = cont MkVar (MkTag (MkEntity ctr Z)::env)              (S ctr,g)
  handle env NewRoom          (ctr,g) cont = cont MkVar (MkTag (MkEntity ctr Z)::env)              (S ctr,g)
  handle env (NewDevice type) (ctr,g) cont = cont MkVar (MkTag (MkEntity ctr (maxConn type))::env) (S ctr,g)
  handle env NewMessage       (ctr,g) cont = cont MkVar (MkTag (MkEntity ctr Z)::env)              (S ctr,g)

  handle env (Insert varX varY prfValid prfFree prfInsert) (ctr,g) cont with (prfValid)
    handle env (Insert varX varY prfValid prfFree prfInsert) (ctr,g) cont | IsValidAssignBR = do
        let MkTag rm  = lookup env prfFree
        let env' = (update env prfFree Use)
        let MkTag bld = lookup env' prfInsert
        let env'' = update env' prfInsert (Assign varX IsValidAssignBR)
        cont () env'' (ctr, Overlay (Nesting (Node bld) (Node rm)) g)
    handle env (Insert varX varY prfValid prfFree prfInsert) (ctr,g) cont | IsValidAssignRD = do
        let MkTag dev  = lookup env prfFree
        let env' = (update env prfFree Use)
        let MkTag rm = lookup env' prfInsert
        let env'' = update env' prfInsert (Assign varX IsValidAssignRD)
        cont () env'' (ctr, Overlay (Nesting (Node rm) (Node dev)) g)
    handle env (Insert varX varY prfValid prfFree prfInsert) (ctr,g) cont | IsValidAssignDM = do
        let MkTag msg  = lookup env prfFree
        let env' = (update env prfFree Use)
        let MkTag dev = lookup env' prfInsert
        let env'' = update env' prfInsert (Assign varX IsValidAssignDM)
        cont () env'' (ctr, Overlay (Nesting (Node dev) (Node msg)) g)

  handle env (Link varX varY prfSpaceX prfSpaceY) (ctr,g) cont = do
    let MkTag x = lookup env prfSpaceX
    let env' = update env prfSpaceX Connect
    let MkTag y = lookup env' prfSpaceY
    let env'' = update env' prfSpaceY Connect
    cont () env'' (ctr, Overlay (Connect (Node x) (Node y)) g)

  handle env End (ctr,g) cont = cont () Nil (ctr,g)

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

max_stars_repo_name: border-patrol/resources

max_issues_repo_name: border-patrol/resources

max_forks_repo_name: border-patrol/resources


text:
module Main

import Data.SortedSet
import Data.String

toIntList : List String -> List Integer
toIntList [] = []
toIntList (x :: xs) = maybe (toIntList xs) (\x => x :: (toIntList xs)) (parseInteger x)

firstRepeat : List Integer -> Integer
firstRepeat [] = 0
firstRepeat (x :: xs) = firstRepeatAux 0 infF (insert 0 empty) where
  infF : Stream Integer
  infF = cycle (x :: xs)

  firstRepeatAux : Integer -> Stream Integer -> SortedSet Integer -> Integer
  firstRepeatAux freq (x :: xs) visited =
    let nextFreq = freq + x in
    if (contains nextFreq visited)
    then nextFreq
    else firstRepeatAux nextFreq xs (insert nextFreq visited)

readLine : File -> IO String
readLine f = do l <- fGetLine f
                pure (either (\_ => "") (\x => x) l)

readLines : File -> IO (List String)
readLines f = readLinesAcc [] where
  readLinesAcc : List String -> IO (List String)
  readLinesAcc acc = if (not !(fEOF f))
                     then readLinesAcc (!(readLine f) :: acc)
                     else pure (reverse acc)

main : IO ()
main = case !(openFile "01.input" Read) of
         Left error => putStrLn "Error opening file"
         Right f =>
           let frequencies = toIntList !(readLines f) in
           do putStrLn $ "Part 1: " ++ (show (foldr (+) 0 frequencies))
              putStrLn $ "Part 2: " ++ (show (firstRepeat frequencies))

max_stars_repo_name: jcazevedo/advent-of-code-solutions


text:
module Flexidisc.OrdList.Fresh

import Flexidisc.Dec.IsYes
import Flexidisc.OrdList.Type
import Flexidisc.OrdList.Label

%default total
%access public export

||| Proof that a key is not in an `OrdList`
data Fresh : (l : key) -> (xs : OrdList key o value) -> Type where
  ||| It's always fresh when the `Ordlist` is empty
  Nil  : Fresh l []
  ||| If it's not the head nor in the tail, then it's `Fresh`
  (::) : Not (l = l') -> Fresh l xs -> Fresh l ((l',ty') :: xs)

%name Fresh fresh, prf, new

||| Decide whether a label is fresh or not
decFresh : DecEq key => (l : key) -> (xs : OrdList key o value) -> Dec (Fresh l xs)
decFresh l [] = Yes []
decFresh l ((l', ty) :: xs) with (decEq l l')
  | (Yes prf) = No (\ (freshHead :: _) => freshHead prf)
  | (No freshHere) with (decFresh l xs)
    | (Yes freshThere) = Yes (freshHere :: freshThere)
    | (No f) = No (\ (_ :: freshTail) => f freshTail)

||| Ensure that the result of `decFresh` is a `Yes` for a given label and a
||| given `OrdList`
IsFresh : DecEq key => (l : key) -> (xs : OrdList key o value) -> Type
IsFresh l xs = IsYes (decFresh l xs)

||| Changing a value doesn't impact the freshness of a label
freshOnValueChange : Fresh l xs -> Fresh l (changeValue xs loc new)
freshOnValueChange (f :: fresh) {loc = Here} = f :: fresh
freshOnValueChange (f :: fresh) {loc = (There later)} = f :: freshOnValueChange fresh

||| Changing values doesn't impact the freshness of a label
freshOnMapValues : (p : Fresh l xs) -> Fresh l (f <$> xs)
freshOnMapValues [] = []
freshOnMapValues (prf :: fresh) = prf :: freshOnMapValues fresh

||| We can't find a label that is `Fresh` in an `OrdList`
freshCantBeLabel : Fresh l xs -> Not (OrdLabel l xs)
freshCantBeLabel (f :: _    ) Here = f Refl
freshCantBeLabel (_ :: fresh) (There later) = freshCantBeLabel fresh later

||| If a label is not in a list, is not in this list minus one element.
export
dropPreservesFresh : Fresh l xs -> Fresh l (dropLabel xs e)
dropPreservesFresh (f :: fresh) {e = Here} = fresh
dropPreservesFresh (f :: fresh) {e = (There e)} = f :: dropPreservesFresh fresh

||| If we can exhibit a `Fresh` value, we can build an `IsFresh` proof
isFreshFromEvidence : DecEq key => {l : key} -> (prf : Fresh l xs) -> IsFresh l xs
isFreshFromEvidence prf {l} {xs} with (decFresh l xs)
  | (Yes _) = SoTrue
  | (No contra) = absurd (contra prf)

||| If a label is not in an `OrdList`, it's not in the tail either
tailIsFresh : DecEq key => {l : key} -> IsFresh l (x :: xs) -> IsFresh l xs
tailIsFresh x = case getProof x of (f :: fresh) => isFreshFromEvidence fresh

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
> module SequentialDecisionProblems.examples.Main

> import Decidable.Order

> import Data.List
> import Data.List.Quantifiers
> import Effects
> import Effect.Exception
> import Effect.StdIO

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.FullTheory
> import SequentialDecisionProblems.Utils

> import SequentialDecisionProblems.examples.LeftAheadRight

> import SimpleProb.SimpleProb
> import SimpleProb.BasicOperations
> import SimpleProb.BasicProperties
> import SimpleProb.MonadicOperations
> import SimpleProb.MonadicProperties
> import SimpleProb.Measures
> import BoundedNat.BoundedNat
> import BoundedNat.Operations
> import BoundedNat.Properties
> import Sigma.Sigma
> import Sigma.Operations
> import Sigma.Properties
> import Nat.LTProperties
> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties
> import NonNegRational.Predicates
> import NonNegRational.LTEProperties
> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Void.Properties
> import Unit.Properties
> import Opt.Operations
> import Rel.TotalPreorder
> import LocalEffect.Exception
> import LocalEffect.StdIO

> -- %default total
> %auto_implicits off

> -- %logging 5

We reimplement "Example2.lidr", this time with |M = SimpleProb|.

* The monad M (SimpleProb):

** SimpleProb is a monad:

> SequentialDecisionProblems.CoreTheory.M =
>   SimpleProb

> SequentialDecisionProblems.CoreTheory.fmap =
>   SimpleProb.MonadicOperations.fmap

> SequentialDecisionProblems.Utils.ret =
>   SimpleProb.MonadicOperations.ret

> SequentialDecisionProblems.Utils.bind =
>   SimpleProb.MonadicOperations.bind

** M is a container monad:

> SequentialDecisionProblems.CoreTheory.Elem =
>   SimpleProb.MonadicOperations.Elem

> SequentialDecisionProblems.CoreTheory.NotEmpty =
>   SimpleProb.MonadicOperations.NonEmpty

> SequentialDecisionProblems.CoreTheory.All =
>   SimpleProb.MonadicOperations.All

> SequentialDecisionProblems.CoreTheory.elemNotEmptySpec0 =
>   SimpleProb.MonadicProperties.elemNonEmptySpec0

> SequentialDecisionProblems.CoreTheory.elemNotEmptySpec1 =
>   SimpleProb.MonadicProperties.elemNonEmptySpec1

> SequentialDecisionProblems.CoreTheory.tagElem =
>   SimpleProb.MonadicOperations.tagElem

> SequentialDecisionProblems.CoreTheory.allElemSpec0 =
>   SimpleProb.MonadicProperties.containerMonadSpec3

* The decision process:

> maxColumn : Nat
> maxColumn = 10
> %freeze maxColumn

> nColumns : Nat
> nColumns = S maxColumn

** States:

> SequentialDecisionProblems.CoreTheory.State t = LTB nColumns

** Controls:

> SequentialDecisionProblems.CoreTheory.Ctrl t x = LeftAheadRight

** Transition function:

> SequentialDecisionProblems.CoreTheory.nexts t (MkSigma Z prf) Left =
>   SimpleProb.MonadicOperations.ret (MkSigma maxColumn (ltIdS maxColumn))
> SequentialDecisionProblems.CoreTheory.nexts t (MkSigma (S n) prf) Left =
>   SimpleProb.MonadicOperations.ret (MkSigma n (ltLemma1 n nColumns prf))
> SequentialDecisionProblems.CoreTheory.nexts t x Ahead = SimpleProb.MonadicOperations.ret x
> SequentialDecisionProblems.CoreTheory.nexts t (MkSigma n prf) Right with (decLT n maxColumn)
>   | (Yes p)     = SimpleProb.MonadicOperations.ret (MkSigma (S n) (LTESucc p))
>   | (No contra) = SimpleProb.MonadicOperations.ret (MkSigma  Z    (LTESucc LTEZero))

** |Val| and |LTE|:

> SequentialDecisionProblems.CoreTheory.Val =
>   NonNegRational.NonNegRational

> SequentialDecisionProblems.CoreTheory.plus =
>   NonNegRational.BasicOperations.plus

> SequentialDecisionProblems.CoreTheory.zero =
>   fromInteger 0

> SequentialDecisionProblems.CoreTheory.LTE =
>   NonNegRational.Predicates.LTE

> SequentialDecisionProblems.FullTheory.reflexiveLTE =
>   NonNegRational.LTEProperties.reflexiveLTE

> SequentialDecisionProblems.FullTheory.transitiveLTE =
>   NonNegRational.LTEProperties.transitiveLTE

> SequentialDecisionProblems.FullTheory.monotonePlusLTE =
>   NonNegRational.LTEProperties.monotonePlusLTE

** Reward function:

> SequentialDecisionProblems.CoreTheory.reward t x y (MkSigma c _) =
>   if c == Z
>   then (fromInteger 1)
>   else if (S c) == nColumns
>        then (fromInteger 2)
>        else (fromInteger 0)

** Measure:

> SequentialDecisionProblems.CoreTheory.meas = average
> SequentialDecisionProblems.FullTheory.measMon = monotoneAverage

** |Ctrl| is finite:

> SequentialDecisionProblems.Utils.finiteCtrl _ =
>   finiteLeftAheadRight
> %freeze SequentialDecisionProblems.Utils.finiteCtrl

** Reachability

> SequentialDecisionProblems.CoreTheory.Reachable x' = Unit
> SequentialDecisionProblems.CoreTheory.reachableSpec1 {t} x r y = all (nexts t x y) where
>   all : (sp : SimpleProb  (State (S t))) -> SequentialDecisionProblems.CoreTheory.All (Reachable {t' = S t}) sp
>   all sp = all' (support sp) where
>     all' : (xs : List (State (S t))) -> Data.List.Quantifiers.All (Reachable {t' = S t}) xs
>     all' Nil = Nil
>     all' (x :: xs) = () :: (all' xs)

** Viability:

> SequentialDecisionProblems.CoreTheory.Viable n x = Unit

> SequentialDecisionProblems.CoreTheory.viableSpec1 {t} {n} x _ = MkSigma Ahead (ne, av) where
>   ne : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts t x Ahead)
>   ne = nonEmptyLemma (nexts t x Ahead)
>   av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} n) (nexts t x Ahead)
>   av = [()]

> SequentialDecisionProblems.Utils.finiteViable n x = finiteUnit

> SequentialDecisionProblems.Utils.decidableViable n x = decidableUnit

** |cvalargmax| and |cvalmax|

We want to implement |cvalmax|, |cvalargmax|, |cvalmaxSpec| and
|cvalargmaxSpec|. This can be easily done in terms of |Opt.max| and
|Opt.argmax| if we can show that

1) |LTE| is a *total* preorder

2) |GoodCtrl t x n| is finite and, for every |t : Nat|, |x : State t|
   such that |Viable (S n) x|, its cardinality is not zero.

The first condition trivially holds, see
|NonNegRational.LTEProperties|. Finiteness and non-zero cardinality of
|GoodCtrl t x n|

< finiteGoodCtrl : {t : Nat} -> {n : Nat} ->
<                  (x : State t) ->
<                  Finite (GoodCtrl t x n)

and

< cnzGoodCtrl : {t : Nat} -> {n : Nat} ->
<               (x : State t) -> (v : Viable {t = t} (S n) x) ->
<               CardNotZ (finiteGoodCtrl {t} {n} x)

follow from finiteness of |Viable| (previous section ), finiteness of
|All|

> SequentialDecisionProblems.Utils.finiteAll = SimpleProb.MonadicProperties.finiteAll

, finiteness of |NotEmpty|

> SequentialDecisionProblems.Utils.finiteNotEmpty = SimpleProb.MonadicProperties.finiteNonEmpty

and finiteness of controls (see above). With these results in place, we have

> SequentialDecisionProblems.FullTheory.cvalmax {n} x r v ps =
>   Opt.Operations.max totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (cval x r v ps)

> SequentialDecisionProblems.CoreTheory.cvalargmax {n} x r v ps =
>   Opt.Operations.argmax totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (cval x r v ps)

> SequentialDecisionProblems.FullTheory.cvalmaxSpec {n} x r v ps =
>   Opt.Operations.maxSpec totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (cval x r v ps)

> SequentialDecisionProblems.FullTheory.cvalargmaxSpec {n} x r v ps =
>   Opt.Operations.argmaxSpec totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (cval x r v ps)

* The computation:

> -- showState : {t : Nat} -> State t -> String
> SequentialDecisionProblems.Utils.showState = show

> -- showControl : {t : Nat} -> {x : State t} -> Ctrl t x -> String
> SequentialDecisionProblems.Utils.showCtrl = show

> computation : { [STDIO] } Eff ()
> computation =
>   do putStr ("enter number of steps:\n")
>      nSteps <- getNat
>      putStr ("enter initial column:\n")
>      x0 <- getLTB nColumns
>      case (decidableViable {t = Z} nSteps x0) of
>        (Yes v0) => do putStrLn ("computing optimal policies ...")
>                       ps   <- pure (backwardsInduction Z nSteps)
>                       putStrLn ("computing optimal controls ...")
>                       mxys <- pure (possibleStateCtrlSeqs x0 () v0 ps)
>                       putStrLn (show mxys)
>                       putStrLn ("done!")
>        (No _)   => putStrLn ("initial column non viable for " ++ cast {from = Int} (cast nSteps) ++ " steps")

> main : IO ()
> main = run computation

> {-

> ---}

-- Local Variables:
-- idris-packages: ("effects")
-- End:

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Flutter.Widgets.Painter

import Dart.FFI
import Flutter.FFI

%inline
public export
Painter : Type
Painter = Struct "_Painter,

import 'package:flutter/material.dart' as material;

class _Painter extends material.CustomPainter {

  final void Function(material.Canvas, material.Size) onPaint;

  _Painter({this.onPaint});

  @$.override
  void paint(material.Canvas canvas, material.Size size) {
    onPaint(canvas, size);
  }

  @$.override
  $.bool shouldRepaint(covariant material.CustomPainter oldDelegate) {
    return oldDelegate != this;
  }
}" []

public export
IsAssignableFrom CustomPainter Painter where

namespace Painter
  namespace New
    data Tag : Type where

    %inline
    public export
    onPaint : Parameter Painter.New.Tag
    onPaint = mkParameter "onPaint" (Canvas -> Size -> IO ())

    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [Painter.New.onPaint]

  %inline
  export
  new : Painter.New.NamedParameters -> IO Painter
  new ps = primIO (prim__dart_new Painter [] ps)


text:
module Example.Qtt.One

import Control.Linear.LIO

import Data.Fin

%default total

---------------------------------
--- File remove grant example ---
---------------------------------

namespace FileRemoveGrantExample

  data File : Type where [external]

  data RmGrant : File -> Type where [external]

  wantToRemove : (fl : File) -> IO $ Maybe $ RmGrant fl
  remove : RmGrant fl -> IO Unit

  readFileFromUser : IO File

  whatever : IO Bool
  whatever = do
    fl <- readFileFromUser
    Just rm <- wantToRemove fl
      | Nothing => pure False
    remove rm
    pure True

----------------------
--- Disconnect arm ---
----------------------

namespace DisconnectArmExample

  data Arm = LeftTopArm | RightTopArm

  data DisconnectGrant : Arm -> Type where [external]

  data DisResult = CantDisconnect | Disconnected

  wantDisconnect : (arm : Arm) -> IO $ Maybe $ DisconnectGrant arm
  disconnect : DisconnectGrant arm -> IO Unit

  whatever : IO DisResult
  whatever = do
    Just rm <- wantDisconnect LeftTopArm
      | Nothing => pure CantDisconnect
    disconnect rm
    pure Disconnected

--------------------------------
--- Handle closing liability ---
--------------------------------

namespace HandleClosingLiability

  data File : Type where [external]

  data ClosingLia : File -> Type where [external]

  openFile  : (fl : File) -> IO $ Maybe $ ClosingLia fl
  readChar  : (fl : File) -> (0 _ : ClosingLia fl) => IO Char
  closeFile : ClosingLia h -> IO Unit

  whatever : File -> IO $ Either String Char
  whatever fl = do
    Just cl <- openFile fl
      | Nothing => pure $ Left "Can't open"
    c <- readChar fl
    closeFile cl
    pure $ Right c

----------------------
--- First examples ---
----------------------

namespace AppendList

  data List' : Type -> Type where
    Nil  : List' a
    (::) : (1 _ : a) -> (1 _ : List' a) -> List' a

  (++) : (1 _ : List' a) -> (1 _ : List' a) -> List' a
  []      ++ ys = ys
  (x::xs) ++ ys = x :: xs ++ ys

  null : (_ : List' a) -> Bool
  null []     = True
  null (_::_) = False

-----------------------------------
--- Entering the linear context ---
-----------------------------------

namespace EnterLin

  data Params = MkParams
  data Result = MkResult

  data Resource : Type where
    [noHints]
    MkResource : (1 _ : Nat) -> Resource

  public export
  data LPair' : Type -> Type -> Type where
    (#) : a -> (1 _ : b) -> LPair' a b

  namespace ResultMark

    export
    1 create : Params -> Resource
    create MkParams = MkResource 3

  namespace WrappingFunction

    public export
    data Ur : Type -> Type where
      MkUr : a -> Ur a

    export
    runWithCreated : Params -> (1 _ : (1 _ : Resource) -> Ur a) -> a
    runWithCreated MkParams f = let MkUr x = f $ MkResource 4 in x

  depend : (1 _ : Resource) -> LPair' Result Resource
  depend r = (MkResult # r)

  destroy : (1 _ : Resource) -> Unit -- Result
  destroy $ MkResource Z     = () -- MkResult
  destroy $ MkResource (S n) = () -- MkResult

  --- Usage of this simple linear interface ---

  --x : Nat
  --x = let r = runWithCreated MkParams (\x => x)
  --     in ?foo -- resource leaks if instead of `Ur a` just `a` was used

  f1 : Result
  f1 = runWithCreated MkParams \res =>
         MkUr ?foo_f1

  f2 : Result
  f2 = runWithCreated MkParams \res =>
         let (r # res') = depend res in
         MkUr ?foo_f2

  --f3 : Result
  --f3 = runWithCreated MkParams \res =>
  --       let (r # res') = depend res in
  --       let (s # res'') = depend res in
  --       MkUr ?foo_f3

  f4 : Result
  f4 = runWithCreated MkParams \res =>
         let (r # res') = depend res in
         let (s # res'') = depend res' in
         MkUr ?foo_f4

  f5 : Result
  f5 = runWithCreated MkParams \res =>
         let (r # res') = depend res in
         let _ = destroy res' in
         MkUr ?foo_f5

  --f6 : Result
  --f6 = runWithCreated MkParams \res =>
  --       let (r # res') = depend res in
  --       let _ = destroy res' in
  --       MkUr r

  --f7 : Result
  --f7 = runWithCreated MkParams \res =>
  --       let (r # res') = depend res in
  --       let z = destroy res' in
  --       MkUr r

  f8 : Result
  f8 = runWithCreated MkParams \res =>
         let (r # res') = depend res in
         let () = destroy res' in
         MkUr r

----------------------------------------
--- Pseudo-quantity-polymorphic pair ---
----------------------------------------

namespace PseudoQuantityPolymorphic

  --data Usage = None | Linear | Unrestricted

  namespace Pair

    public export
    data Pair' : {r : Usage} -> Type -> Type -> Type where
      W0 : a -> (0 _ : b) -> Pair' {r=None}   a b
      W1 : a -> (1 _ : b) -> Pair' {r=Linear} a b
      WW : a -> b         -> Pair'            a b
      --WW : a -> b -> {default Unrestricted 0 r : Usage} -> Pair' {r} a b

    relax : Pair' {r=Unrestricted} a b -> Pair' a b
    relax (WW x y) = WW x y
    -- When `WW` is declared with a default.
    --relax : Pair' {r=Unrestricted} a b -> {0 u : Usage} -> Pair' {r=u} a b
    --relax (WW x y) = WW {r=u} x y

    (.fst) : Pair' a b -> a
    (.fst) (W0 x _) = x
    (.fst) (W1 x _) = x
    (.fst) (WW x _) = x

    0 (.snd0) : (0 _ : Pair' {r=0} a b) -> b
    (W0 _ y).snd0 = y
    (WW _ y).snd0 = y

    1 (.snd1) : (1 _ : Pair' {r=1} a b) -> b
    (.snd1) (W1 _ y) = y
    (.snd1) (WW _ y) = y

    (.sndW) : (1 _ : Pair' {r=Unrestricted} a b) -> b
    (.sndW) (WW _ y) = y

  --- Not a pair ---

  namespace SingleValue

    public export
    data V : {r : Usage} -> Type -> Type where
      V0 : (0 _ : a) -> V {r=None}   a
      V1 : (1 _ : a) -> V {r=Linear} a
      VW : a         -> V            a

    relax : V {r=Unrestricted} a -> V a
    relax (VW x) = VW x

    0 (.v0) : (0 _ : V {r=0} a) -> a
    (.v0) (V0 x) = x
    (.v0) (VW x) = x

    1 (.v1) : (1 _ : V {r=1} a) -> a
    (.v1) (V1 x) = x
    (.v1) (VW x) = x

    (.vW) : (1 _ : V {r=Unrestricted} a) -> a
    (.vW) (VW x) = x

  namespace List

    public export
    data LinOrW = Linear | W

    public export
    fromInteger : (0 x : Integer) -> (0 _ : x = 1) => LinOrW
    fromInteger 1 @{Refl} = Linear

    infixr 7 .::, ::., .::.

    data List' : {l, r : LinOrW} -> Type -> Type where
      Nil    : List' a
      (::)   : a -> List' a -> List' {l=W,r=W} a
      (.::)  : (1 _ : a) -> List' a -> List' {l=1,r=W} a
      (::.)  : a -> (1 _ : List' a) -> List' {l=W,r=1} a
      (.::.) : (1 _ : a) -> (1 _ : List' a) -> List' {l=1,r=1} a

    relax : (1 _ : List' a) -> List' {l=1,r=1} a
    relax [] = []
    relax (x  ::  y) = x .::. y
    relax (x .::  y) = x .::. y
    relax (x  ::. y) = x .::. y
    relax (x .::. y) = x .::. y

    null : (1 _ : List' {l=W,r=W} a) -> Bool
    null []     = True
    null (x::y) = False

    (++) : (1 _ : List' {l=1,r=1} a) -> (1 _ : List' {l=1,r=1} a) -> List' {l=1,r=1} a
    [] ++ ys = ys
    (x .::. xs) ++ ys = assert_total $ x .::. (relax xs ++ ys)

    f : List' a -> List' a -> List' {l=1,r=1} a
    f xs ys = relax xs ++ relax ys

  namespace List'

    data List' : {l, r : LinOrW} -> Type -> Type where
      Nil    : List' a
      (::)   : a -> List' a -> List' a
      (.::)  : (1 _ : a) -> List' a -> List' {l=1} a
      (::.)  : a -> (1 _ : List' a) -> List' {r=1} a
      (.::.) : (1 _ : a) -> (1 _ : List' a) -> List' {l=1,r=1} a

    relax : (1 _ : List' a) -> List' {l=1,r=1} a
    relax [] = []
    relax (x  ::  y) = x  ::  y
    relax (x .::  y) = x .::  y
    relax (x  ::. y) = x  ::. y
    relax (x .::. y) = x .::. y

    null : (1 _ : List' {l=W,r=W} a) -> Bool
    null []     = True
    null (x::y) = False

    (++) : (1 _ : List' {l=1,r=1} a) -> (1 _ : List' {l=1,r=1} a) -> List' {l=1,r=1} a
    [] ++ ys = ys
    (x  ::  xs) ++ ys = assert_total $ x .::. (relax xs ++ ys)
    (x .::  xs) ++ ys = assert_total $ x .::. (relax xs ++ ys)
    (x  ::. xs) ++ ys = assert_total $ x .::. (relax xs ++ ys)
    (x .::. xs) ++ ys = assert_total $ x .::. (relax xs ++ ys)

    f : List' a -> List' a -> List' {l=1,r=1} a
    f xs ys = relax xs ++ relax ys

----------------------
--- Linear file IO ---
----------------------

namespace FileIO

  data FileName = MkFileName String

  FromString FileName where
    fromString = MkFileName

  data FileHandler : FileName -> Type where [external]

  namespace ImpureIO_API

    withOpenFile : LinearIO io =>
                   (fn : FileName) ->
                   (success : (1 _ : FileHandler fn) -> L io a) ->
                   (fail : L io a) ->
                   L io a

    closeFile : LinearIO io => (1 _ : FileHandler fn) -> L io Unit

    readLine : LinearIO io =>
               (1 _ : FileHandler fn) ->
               L io {use=1} $ LPair' String $ FileHandler fn

    f : LinearIO io => L io $ Maybe Bool
    f = withOpenFile "foo" success (putStrLn "alas" *> pure Nothing) where
      success : (1 _ : FileHandler _) -> L io $ Maybe Bool
      success fh = do (str # fh) <- readLine fh
                      closeFile fh
                      pure $ Just (str == "x")

  namespace AbstractedAPI

    interface (Monad io, LinearBind io) => FilesAPI io where
      withOpenFile : (fn : FileName) ->
                     (success : (1 _ : FileHandler fn) -> L io a) ->
                     (fail : L io a) ->
                     L io a
      closeFile : (1 _ : FileHandler fn) -> L io Unit
      readLine : (1 _ : FileHandler fn) ->
                 L io {use=1} $ LPair' String $ FileHandler fn

    f : (FilesAPI io, HasLinearIO io) => L io $ Maybe Bool
    f = withOpenFile "foo" success (putStrLn "alas" *> pure Nothing) where
      success : (1 _ : FileHandler _) -> L io $ Maybe Bool
      success fh = do (str # fh) <- AbstractedAPI.readLine fh
                      closeFile fh
                      pure $ Just (str == "x")

-----------------------------
--- Simple login protocol ---
-----------------------------

namespace SimpleLoginProtocol

  data JournalState = NotYetCheckedIn | CheckedIn
  data LoginState = Initial | LoggedIn JournalState | LoggedOut

  prefix 9 @
  data (@) : LoginState -> Type where [external]

  data Key : Type where [external]
  data FailureReason = WrongKey | MalformedKey

  Show FailureReason where
    show WrongKey     = "wrong key"
    show MalformedKey = "malformed key"

  interface (Monad m, LinearBind m) => SimpleProtocol m where
    beginSession : (1 _ : (1 _ : @ Initial) -> L m a) -> L m a
    endSession   : (1 _ : @ LoggedOut) -> L m Unit

    login  : (1 _ : @ Initial) ->
             (name : String) ->
             (key : Key) ->
             L m {use=1} $ Res Bool \case
               True  => @ LoggedIn NotYetCheckedIn
               False => LPair' FailureReason (@ LoggedOut)
    logout : (1 _ : @ LoggedIn CheckedIn) -> L m {use=1} (@ LoggedOut)

    updateKey  : (1 _ : @ LoggedIn x) ->
                 (newKey : Key) ->
                 L m {use=1} $ LPair' (Maybe FailureReason) (@ LoggedIn x)
    readSecret : (1 _ : @ LoggedIn x) -> L m {use=1} $ LPair' String (@ LoggedIn x)

    checkIn : (1 _ : @ LoggedIn NotYetCheckedIn) ->
              (info : String) ->
              L m {use=1} (@ LoggedIn CheckedIn)

  denisKey : Key

  f1 : SimpleProtocol m => L m $ Either String Bool
  f1 = beginSession \p => do
         ?foo_1

  f2 : SimpleProtocol m => L m $ Either String Bool
  f2 = beginSession \p => do
         ans <- login p "Denis" denisKey
         ?foo_2

  f3 : SimpleProtocol m => L m $ Either String Bool
  f3 = beginSession \p => do
         (True # s) <- login p "Denis" denisKey
           | (False # (reason # s)) => ?foo_bad
         ?foo_good

  f4 : SimpleProtocol m => L m $ Either String Bool
  f4 = beginSession \p => do
         (True # p) <- login p "Denis" denisKey
           | (False # (reason # s)) => do
               endSession s
               pure $ Left $ show reason
         ?foo_4

  f5 : SimpleProtocol m => L m $ Either String Bool
  f5 = beginSession \p => do
         (True # p) <- login p "Denis" denisKey
           | (False # (reason # s)) => do
               endSession s
               pure $ Left $ show reason
         sec # p <- readSecret p
         ?foo_5

  --f6 : SimpleProtocol m => L m $ Either String Bool
  --f6 = beginSession \p => do
  --       (True # p) <- login p "Denis" denisKey
  --         | (False # (reason # s)) => do
  --             endSession s
  --             pure $ Left $ show reason
  --       sec # p <- readSecret p
  --       p <- logout p
  --       ?foo_6

  f7 : SimpleProtocol m => L m $ Either String Bool
  f7 = beginSession \p => do
         (True # p) <- login p "Denis" denisKey
           | (False # (reason # s)) => do
               endSession s
               pure $ Left $ show reason
         sec # p <- readSecret p
         p <- checkIn p "read secret"
         p <- logout p
         ?foo_7

  --f8 : SimpleProtocol m => L m $ Either String Bool
  --f8 = beginSession \p => do
  --       (True # p) <- login p "Denis" denisKey
  --         | (False # (reason # s)) => do
  --             endSession s
  --             pure $ Left $ show reason
  --       sec # p <- readSecret p
  --       p <- checkIn p "read secret"
  --       p <- logout p
  --       pure $ Right $ sec == "foo"

  f9 : SimpleProtocol m => L m $ Either String Bool
  f9 = beginSession \p => do
         (True # p) <- login p "Denis" denisKey
           | (False # (reason # s)) => do
               endSession s
               pure $ Left $ show reason
         sec # p <- readSecret p
         p <- checkIn p "read secret"
         p <- logout p
         endSession p
         pure $ Right $ sec == "foo"

---------------------
--- Game protocol ---
---------------------

namespace GameLocalProtocol

  -- Not done yet.

-----------------------------------------
--- Safe pure mutable data structures ---
-----------------------------------------

namespace MonadicMutalbeArrays

  export
  data IArray : Nat -> Type -> Type where [external]

  interface Monad m => MArray (0 ar : Nat -> Type -> Type) m where
    new   : (n : Nat) -> a -> m (ar n a)
    read  : Fin n -> ar n a -> m a
    write : Fin n -> a -> ar n a -> m Unit

    freeze : ar n a -> m (IArray n a) -- unsafe!

  modify : MArray ar m => (a -> a) -> Fin n -> ar n a -> m Unit
  modify f i arr = do
    x <- read i arr
    write i (f x) arr

  modifyAll : MArray ar m => (a -> a) -> ar n a -> m Unit

  f : MArray ar m => Fin n -> ar n Nat -> m Nat
  f i arr = do original <- read i arr
               modify (+1) i arr
               pure original

namespace LinearMutableArrays

  data LArray : Nat -> Type -> Type where [external]

  withNew : (n : Nat) -> a -> (1 _ : (1 _ : LArray n a) -> Ur b) -> b
  read    : Fin n -> (1 _ : LArray n a) -> LPair' a $ LArray n a
  write   : Fin n -> a -> (1 _ : LArray n a) -> LArray n a

  free   : (1 _ : LArray n a) -> Unit
  freeze : (1 _ : LArray n a) -> Ur $ IArray n a

  modify : (a -> a) -> Fin n -> (1 _ : LArray n a) -> LArray n a
  modify f i arr = let x # arr = read i arr
                    in write i (f x) arr

  modifyAll : (a -> a) -> (1 _ : LArray n a) -> LArray n a

  f : Fin n -> (1 _ : LArray n Nat) -> LPair' Nat $ LArray n Nat
  f i arr = let original # arr = read i arr
                arr = modify (+1) i arr
             in original # arr

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
module Network.Curl.Types.Handle

export
data HandlePtr : Type where

export
data FunPtr : Type where

export
data ObjPtr : Type where

public export
data HandleType = Easy | Multi

public export
data CurlHandle : HandleType -> Type where
  MkH : (1 _ : Ptr HandlePtr) -> CurlHandle ty


text:
||| Core features required to perform Golden file testing.
|||
||| We provide the core functionality to run a *single* golden file test, or
||| a whole test tree.
||| This allows the developer freedom to use as is or design the rest of the
||| test harness to their liking.
|||
||| This was originally used as part of Idris2's own test suite and
||| the core functionality is useful for the many and not the few.
||| Please see Idris2 test harness for example usage.
|||
||| # Test Structure
|||
||| This harness works from the assumption that each individual golden test
||| comprises of a directory with the following structure:
|||
||| + `run` a *shell* script that runs the test. We expect it to:
|||   * Use `$1` as the variable standing for the idris executable to be tested
|||   * May use `${IDRIS2_TESTS_CG}` to pick a codegen that ought to work
|||   * Clean up after itself (e.g. by running `rm -rf build/`)
|||
||| + `expected` a file containting the expected output of `run`
|||
||| During testing, the test harness will generate an artefact named `output`
||| and display both outputs if there is a failure.
||| During an interactive session the following command is used to compare them
||| as they are:
|||
||| ```sh
|||  git diff --no-index --exit-code --word-diff=color expected output
||| ```
|||
||| If `git` fails then the runner will simply present the expected and 'given'
||| files side-by-side.
|||
||| Of note, it is helpful to add `output` to a local `.gitignore` instance
||| to ensure that it is not mistakenly versioned.
|||
||| # Options
|||
||| The test harness has several options that may be set:
|||
||| + `idris2`       The path of the executable we are testing.
||| + `codegen`      The backend to use for code generation.
||| + `onlyNames`    The tests to run relative to the generated executable.
||| + `onlyFile`     The file listing the tests to run relative to the generated executable.
||| + `interactive`  Whether to offer to update the expected file or not.
||| + `timing`       Whether to display time taken for each test.
||| + `threads`      The maximum numbers to use (default: number of cores).
||| + `failureFile`  The file in which to write the list of failing tests.
|||
||| We provide an options parser (`options`) that takes the list of command line
||| arguments and constructs this for you.
|||
||| # Usage
|||
||| When compiled to an executable the expected usage is:
|||
|||```sh
||| runtests <path to executable under test>
|||   [--timing]
|||   [--interactive]
|||   [--only-file PATH]
|||   [--failure-file PATH]
|||   [--threads N]
|||   [--cg CODEGEN]
|||   [--only [NAMES]]
|||```
|||
||| assuming that the test runner is compiled to an executable named `runtests`.

module Test.Golden

import Control.ANSI

import Data.Either
import Data.Maybe
import Data.List
import Data.List1
import Data.String

import System
import System.Clock
import System.Directory
import System.File
import System.Future
import System.Info
import System.Path

-- [ Options ]

||| Options for the test driver.
public export
record Options where
  constructor MkOptions
  ||| Name of the idris2 executable
  exeUnderTest : String
  ||| Which codegen should we use?
  codegen      : Maybe String
  ||| Should we only run some specific cases?
  onlyNames    : List String
  ||| Should we run the test suite interactively?
  interactive  : Bool
  ||| Should we use colors?
  color        : Bool
  ||| Should we time and display the tests
  timing       : Bool
  ||| How many threads should we use?
  threads      : Nat
  ||| Should we write the list of failing cases to a file?
  failureFile     : Maybe String

export
initOptions : String -> Bool -> Options
initOptions exe color
  = MkOptions exe
              Nothing
              []
              False
              color
              False
              1
              Nothing

export
usage : String
usage = unwords
  ["Usage:"
  , "runtests <path>"
  , "[--timing]"
  , "[--interactive]"
  , "[--[no-]color, --[no-]colour]"
  , "[--cg CODEGEN]"
  , "[--threads N]"
  , "[--failure-file PATH]"
  , "[--only-file PATH]"
  , "[--only [NAMES]]"
  ]

export
fail : String -> IO a
fail err
    = do putStrLn err
         exitWith (ExitFailure 1)

||| Process the command line options.
export
options : List String -> IO (Maybe Options)
options args = case args of
    (_ :: exe :: rest) => mkOptions exe rest
    _ => pure Nothing

  where

    go : List String -> Maybe String -> Options -> Maybe (Maybe String, Options)
    go rest only opts = case rest of
      []                            => pure (only, opts)
      ("--timing" :: xs)            => go xs only (record { timing = True} opts)
      ("--interactive" :: xs)       => go xs only (record { interactive = True } opts)
      ("--color"  :: xs)            => go xs only (record { color = True } opts)
      ("--colour" :: xs)            => go xs only (record { color = True } opts)
      ("--no-color"  :: xs)         => go xs only (record { color = False } opts)
      ("--no-colour" :: xs)         => go xs only (record { color = False } opts)
      ("--cg" :: cg :: xs)          => go xs only (record { codegen = Just cg } opts)
      ("--threads" :: n :: xs)      => do let pos : Nat = !(parsePositive n)
                                          go xs only (record { threads = pos } opts)
      ("--failure-file" :: p :: xs) => go  xs only (record { failureFile = Just p } opts)
      ("--only" :: xs)              => pure (only, record { onlyNames = xs } opts)
      ("--only-file" :: p :: xs)    => go xs (Just p) opts
      _ => Nothing

    mkOptions : String -> List String -> IO (Maybe Options)
    mkOptions exe rest
      = do color <- (Just "DUMB" /=) <$> getEnv "TERM"
           let Just (mfp, opts) = go rest Nothing (initOptions exe color)
                 | Nothing => pure Nothing
           let Just fp = mfp
                 | Nothing => pure (Just opts)
           Right only <- readFile fp
             | Left err => fail (show err)
           pure $ Just $ record { onlyNames $= ((lines only) ++) } opts

||| Normalise strings between different OS.
|||
||| on Windows, we just ignore backslashes and slashes when comparing,
||| similarity up to that is good enough. Leave errors that depend
||| on the confusion of slashes and backslashes to unix machines.
normalize : String -> String
normalize str =
    if isWindows
      then pack $ filter (\ch => ch /= '/' && ch /= '\\') (unpack str)
      else str

||| The result of a test run
||| `Left` corresponds to a failure, and `Right` to a success
Result : Type
Result = Either String String

guardPath : String -> String
guardPath s = "\"" ++ s ++ "\""

||| Run the specified Golden test with the supplied options.
||| See the module documentation for more information.
||| @testPath the directory that contains the test.
export
runTest : Options -> (testPath : String) -> IO (Future Result)
runTest opts testPath = forkIO $ do
  start <- clockTime UTC
  let cg = maybe "" (" --cg " ++) (codegen opts)
  let exe = "\"" ++ exeUnderTest opts ++ cg ++ "\""
  ignore $ system $ "cd " ++ guardPath testPath ++ " && " ++
    "sh ./run " ++ exe ++ " | tr -d '\\r' > output"
  end <- clockTime UTC

  Right out <- readFile $ testPath ++ "/output"
    | Left err => do putStrLn $ (testPath ++ "/output") ++ ": " ++ show err
                     pure (Left testPath)

  Right exp <- readFile $ testPath ++ "/expected"
    | Left FileNotFound => do
        if interactive opts
          then mayOverwrite Nothing out
          else putStrLn $ (testPath ++ "/expected") ++ ": " ++ show FileNotFound
        pure (Left testPath)
    | Left err => do putStrLn $ (testPath ++ "/expected") ++ ": " ++ show err
                     pure (Left testPath)

  let result = normalize out == normalize exp
  let time = timeDifference end start

  if result
    then printTiming (timing opts) time testPath $
      (if opts.color then show . colored BrightGreen else id) "success"
    else do
      printTiming (timing opts) time testPath $
        (if opts.color then show . colored BrightRed else id) "FAILURE"
      if interactive opts
        then mayOverwrite (Just exp) out
        else putStr . unlines $ expVsOut exp out

  pure $ if result then Right testPath else Left testPath

  where
    getAnswer : IO Bool
    getAnswer = do
      str <- getLine
      case str of
        "y" => pure True
        "n" => pure False
        "N" => pure False
        ""  => pure False
        _   => do putStrLn "Invalid answer."
                  getAnswer

    expVsOut : String -> String -> List String
    expVsOut exp out = ["Expected:", exp, "Given:", out]

    mayOverwrite : Maybe String -> String -> IO ()
    mayOverwrite mexp out = do
      case mexp of
        Nothing => putStr $ unlines
          [ "Golden value missing. I computed the following result:"
          , out
          , "Accept new golden value? [y/N]"
          ]
        Just exp => do
          code <- system $ "git diff --no-index --exit-code " ++
            (if opts.color then  "--word-diff=color " else "") ++
            guardPath testPath ++ "/expected " ++ guardPath testPath ++ "/output"
          putStr . unlines $
            ["Golden value differs from actual value."] ++
            (if (code < 0) then expVsOut exp out else []) ++
            ["Accept actual value as new golden value? [y/N]"]
      b <- getAnswer
      when b $ do Right _ <- writeFile (testPath ++ "/expected") out
                    | Left err => putStrLn $ (testPath ++ "/expected") ++ ": " ++ show err
                  pure ()

    printTiming : Bool -> Clock type -> String -> String -> IO ()
    printTiming False _     path msg = putStrLn $ concat [path, ": ", msg]
    printTiming True  clock path msg =
      let time  = showTime 2 3 clock
          -- We use 9 instead of `String.length msg` because:
          -- 1. ": success" and ": FAILURE" have the same length
          -- 2. ANSI escape codes make the msg look longer than it is
          spent = String.length time + String.length path + 9
          pad   = pack $ replicate (minus 72 spent) ' '
      in putStrLn $ concat [path, ": ", msg, pad, time]

||| Find the first occurrence of an executable on `PATH`.
export
pathLookup : List String -> IO (Maybe String)
pathLookup names = do
  path <- getEnv "PATH"
  let extensions = if isWindows then [".exe", ".cmd", ".bat", ""] else [""]
  let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
  let candidates = [p ++ "/" ++ x ++ y | p <- pathList,
                                         x <- names,
                                         y <- extensions]
  firstExists candidates

||| Some test may involve Idris' backends and have requirements.
||| We define here the ones supported by Idris
public export
data Requirement = C | Chez | Node | Racket | Gambit | Jvm

export
Show Requirement where
  show C = "C"
  show Chez = "Chez"
  show Node = "node"
  show Racket = "racket"
  show Gambit = "gambit"
  show Jvm = "jvm"

export
[CG] Show Requirement where
  show C = "refc"
  show Chez = "chez"
  show Node = "node"
  show Racket = "racket"
  show Gambit = "gambit"
  show Jvm = "jvm"

export
checkRequirement : Requirement -> IO (Maybe String)
checkRequirement req
  = if platformSupport req
      then do let (envvar, paths) = requirement req
              Just exec <- getEnv envvar | Nothing => pathLookup paths
              pure (Just exec)
      else pure Nothing
  where
    requirement : Requirement -> (String, List String)
    requirement C = ("CC", ["cc"])
    requirement Chez = ("CHEZ", ["chez", "chezscheme9.5", "chezscheme", "chez-scheme", "scheme"])
    requirement Node = ("NODE", ["node"])
    requirement Racket = ("RACKET", ["racket"])
    requirement Gambit = ("GAMBIT", ["gsc"])
    requirement Jvm = ("JVM", ["java"])
    platformSupport : Requirement -> Bool
    platformSupport C = not isWindows
    platformSupport Racket = not isWindows
    platformSupport _ = True

export
findCG : IO (Maybe String)
findCG
  = do Nothing <- getEnv "IDRIS2_TESTS_CG" | p => pure p
       Nothing <- checkRequirement Chez    | p => pure (Just "chez")
       Nothing <- checkRequirement Node    | p => pure (Just "node")
       Nothing <- checkRequirement Racket  | p => pure (Just "racket")
       Nothing <- checkRequirement Gambit  | p => pure (Just "gsc")
       Nothing <- checkRequirement C       | p => pure (Just "refc")
       Nothing <- checkRequirement Jvm     | p => pure (Just "jvm")
       pure Nothing

||| A choice of a codegen
public export
data Codegen
  = ||| Do NOT pass a cg argument to the executable being tested
    Nothing
  | ||| Use whatever the test runner was passed at the toplevel,
    ||| and if nothing was passed guess a sensible default using findCG
    Default
  | ||| Use exactly the given requirement
    Just Requirement

export
toList : Codegen -> List Requirement
toList (Just r) = [r]
toList _ = []

||| A test pool is characterised by
|||  + a name
|||  + a list of requirement
|||  + a choice of codegen (overriding the default)
|||  + and a list of directory paths
public export
record TestPool where
  constructor MkTestPool
  poolName : String
  constraints : List Requirement
  codegen : Codegen
  testCases : List String

||| Find all the test in the given directory.
export
testsInDir : (dirName : String) -> (testNameFilter : String -> Bool) -> (poolName : String) -> List Requirement -> Codegen -> IO TestPool
testsInDir dirName testNameFilter poolName reqs cg = do
  Right names <- listDir dirName
    | Left e => do putStrLn ("failed to list " ++ dirName ++ ": " ++ show e)
                   exitFailure
  let names = [n | n <- names, testNameFilter n]
  let testNames = [dirName ++ "/" ++ n | n <- names]
  testNames <- filter testNames
  when (length testNames == 0) $ do
    putStrLn ("no tests found in " ++ dirName)
    exitFailure
  pure $ MkTestPool poolName reqs cg testNames
    where
      -- Directory without `run` file is not a test
      isTest : (path : String) -> IO Bool
      isTest path = exists (path ++ "/run")

      filter : (testPaths : List String) -> IO (List String)
      filter [] = pure []
      filter (p :: ps) =
          do rem <- filter ps
             case !(isTest p) of
               True  => pure $ p :: rem
               False => pure rem

||| Only keep the tests that have been asked for
export
filterTests : Options -> List String -> List String
filterTests opts = case onlyNames opts of
  [] => id
  xs => filter (\ name => any (`isInfixOf` name) xs)

||| The summary of a test pool run
public export
record Summary where
  constructor MkSummary
  success : List String
  failure : List String

export
initSummary : Summary
initSummary = MkSummary [] []

export
updateSummary : List Result -> Summary -> Summary
updateSummary res =
  let (ls, ws) = partitionEithers res in
  { success $= (ws ++)
  , failure $= (ls ++)
  }

export
Semigroup Summary where
  MkSummary ws1 ls1 <+> MkSummary ws2 ls2
    = MkSummary (ws1 ++ ws2) (ls1 ++ ls2)

export
Monoid Summary where
  neutral = initSummary

||| A runner for a test pool
export
poolRunner : Options -> TestPool -> IO Summary
poolRunner opts pool
  = do -- check that we indeed want to run some of these tests
       let tests = filterTests opts (testCases pool)
       let (_ :: _) = tests
             | [] => pure initSummary
       -- if so make sure the constraints are satisfied
       cs <- for (toList (codegen pool) ++ constraints pool) $ \ req => do
          mfp <- checkRequirement req
          let msg = case mfp of
                      Nothing => "✗ " ++ show req ++ " not found"
                      Just fp => "✓ Found " ++ show req ++ " at " ++ fp
          pure (mfp, msg)
       let (cs, msgs) = unzip cs

       putStrLn (banner msgs)

       let Just _ = the (Maybe (List String)) (sequence cs)
             | Nothing => pure initSummary

       -- if the test pool requires a specific codegen then use that
       let opts = case codegen pool of
                    Nothing => { codegen := Nothing } opts
                    Just cg => { codegen := Just (show @{CG} cg) } opts
                    Default => opts
       -- if so run them all!
       loop opts initSummary tests

  where

    separator : String
    separator = fastPack $ replicate 72 '-'

    banner : List String -> String
    banner msgs = fastUnlines
        $ [ "", separator, pool.poolName ]
       ++ msgs
       ++ [ separator ]

    loop : Options -> Summary -> List String -> IO Summary
    loop opts acc [] = pure acc
    loop opts acc tests
      = do let (now, later) = splitAt opts.threads tests
           bs <- map await <$> traverse (runTest opts) now
           loop opts (updateSummary bs acc) later

||| A runner for a whole test suite
export
runner : List TestPool -> IO ()
runner tests
    = do args <- getArgs
         Just opts <- options args
            | _ => do printLn args
                      putStrLn usage
         -- if no CG has been set, find a sensible default based on what is available
         opts <- case codegen opts of
                   Nothing => pure $ record { codegen = !findCG } opts
                   Just _ => pure opts
         -- run the tests
         res <- concat <$> traverse (poolRunner opts) tests

         -- report the result
         let nsucc  = length res.success
         let nfail  = length res.failure
         let ntotal = nsucc + nfail
         putStrLn (show nsucc ++ "/" ++ show ntotal ++ " tests successful")

         -- deal with failures
         let list = fastUnlines res.failure
         when (nfail > 0) $
           do putStrLn "Failing tests:"
              putStr list
         -- always overwrite the failure file, if it is given
         whenJust opts.failureFile $ \ path =>
           do Right _ <- writeFile path list
                | Left err => fail (show err)
              pure ()

         -- exit
         if nfail == 0
           then exitWith ExitSuccess
           else exitWith (ExitFailure 1)


text:
-- Copyright (c) 2013 Radek Micek

module Common

infixr 1 ??, >=>

(??) : a -> (a -> b) -> b
a ?? f = f a

(>=>) : Monad m => (a -> m b) -> (b -> m c) -> a -> m c
f >=> g = \a => f a >>= g

filterM : Monad m => (a -> m Bool) -> List a -> m (List a)
filterM _ [] = return List.Nil
filterM p (x :: xs) = do
  b <- p x
  ys <- filterM p xs
  return (b ? List.(::) x ys : ys)

mapTupleM : Monad m => (a -> m b) -> (a, a) -> m (b, b)
mapTupleM f (x, y) = do
  x' <- f x
  y' <- f y
  return (x', y')

mapM_ : Monad m => (a -> m b) -> List a -> m ()
mapM_ f = sequence_ . map f

boolToInt : Bool -> Int
boolToInt b = b ? 1 : 0

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
module Brainfeck.Util

import Data.Vect

%default total

export
listToVect : List a -> (num_a : Nat ** Vect num_a a)
listToVect []        = (0 ** Nil)
listToVect (a :: as) =
  case listToVect as of
    (_ ** avect) => (_ ** a :: avect)

max_stars_repo_name: jhmcstanton/brainfeck

max_issues_repo_name: jhmcstanton/brainfeck

max_forks_repo_name: jhmcstanton/brainfeck


text:
module extensible_records

import Data.List
import list

-- All functions must be total
%default total

-- All definitions and functions are exported
%access public export

-- *** Labelled Heterogeneous List ***

infixr 4 .=.

data Field : lty -> Type -> Type where
  (.=.) : (l : lty) -> (v : t) -> Field l t

infix 5 :>

data LHList : List (lty, Type) -> Type where
  HNil : LHList []
  (:>) : Field lty t -> LHList ts -> LHList ((lty, t) :: ts)

infixr 3 :++:

-- Appends two labelled hlists
(:++:) : LHList ts -> LHList us -> LHList (ts ++ us)
(:++:) HNil ys      = ys
(:++:) (x :> xs) ys = x :> (xs :++: ys)

-- *** Record ***

data Record : List (lty, Type) -> Type where
  MkRecord : IsSet (labelsOf ts) -> LHList ts ->
                                    Record ts

recToHList : Record ts -> LHList ts
recToHList (MkRecord _ hs) = hs

recLblIsSet : Record ts -> IsSet (labelsOf ts)
recLblIsSet (MkRecord isS _) = isS

emptyRec : Record []
emptyRec = MkRecord IsSetNil {ts=[]} HNil

hListToRec : DecEq lty => {prf : IsSet (labelsOf ts)} -> LHList ts -> Record ts
hListToRec {prf} hs = MkRecord prf hs

-- *** Automatic generation of proofs ***

TypeOrUnit : Dec p -> (p -> Type) -> Type
TypeOrUnit (Yes yes) tyCons = tyCons yes
TypeOrUnit (No _) _         = ()

mkTorU : (d : Dec p) -> (tyCons : p -> Type) ->
          (f : (prf : p) -> tyCons prf) ->
          TypeOrUnit d tyCons
mkTorU (Yes yes) _ f = f yes
mkTorU (No _) _ _    = ()

UnitOrType : Dec p -> (Not p -> Type) -> Type
UnitOrType (Yes _) _ = ()
UnitOrType (No no) tyCons = tyCons no

mkUorT : (d : Dec p) -> (tyCons : Not p -> Type) ->
          (f : (contra : Not p) -> tyCons contra) ->
          UnitOrType d tyCons
mkUorT (Yes _) _ _ = ()
mkUorT (No no) _ f = f no

-- TypeOrUnit with constant return type
TypeOrUnitC : Dec p -> Type -> Type
TypeOrUnitC d ty = TypeOrUnit d (\_ => ty)

mkTorUC : (d : Dec p) -> (f : p -> ty)
                     -> TypeOrUnitC d ty
mkTorUC {ty} d f = mkTorU d (\_ => ty)
                       (\p => f p)

-- UnitOrType with constant return type
UnitOrTypeC : Dec p -> Type -> Type
UnitOrTypeC d ty = UnitOrType d (\_ => ty)

mkUorTC : (d : Dec p) -> (f : Not p -> ty)
                     -> UnitOrTypeC d ty
mkUorTC {ty} d f = mkUorT d (\_ => ty)
                       (\np => f np)

-- *** Extension of record ***

consR : DecEq lty => {l : lty} ->
        Field l t -> Record ts ->
        Not (Elem l (labelsOf ts)) ->
        Record ((l, t) :: ts)
consR {ts} f (MkRecord isS fs) notLInTs =
  MkRecord (IsSetCons notLInTs isS) (f :> fs)

MaybeE : DecEq lty => lty -> List (lty, Type) -> Type -> Type
MaybeE l ts r = UnitOrTypeC (isElem l (labelsOf ts)) r

infixr 6 .*.

(.*.) : DecEq lty => {l : lty} ->
        Field l t -> Record ts ->
        MaybeE l ts (Record ((l, t) :: ts))
(.*.) {l} {ts} f r
   = mkUorTC (isElem l (labelsOf ts))
            (\notp => consR f r notp)

-- *** Lookup ***

getType : (ts : List (lty, Type)) -> Elem l (labelsOf ts) ->
          Type
getType ((l, ty) :: ts) Here      = ty
getType ((l, ty) :: ts)(There th) = getType ts th

lookupH : (l : lty) -> LHList ts ->
          (isE : Elem l (labelsOf ts)) -> getType ts isE
lookupH _ ((_ .=. v) :> _) Here   = v
lookupH l (_ :> hs) (There th)    = lookupH l hs th

lookupR : (l : lty) -> Record ts ->
          (isE : Elem l (labelsOf ts)) -> getType ts isE
lookupR l (MkRecord _ fs) isE = lookupH l fs isE

MaybeLkp : DecEq lty => List (lty, Type) -> lty -> Type
MaybeLkp ts l = TypeOrUnit (isElem l (labelsOf ts))
                            (\isE => getType ts isE)

infixr 7 .!.

(.!.) : DecEq lty => Record ts -> (l : lty) ->
        MaybeLkp ts l
(.!.) {ts} r l = mkTorU (isElem l (labelsOf ts))
                         (\isE => getType ts isE)
                         (\isE => lookupR l r isE)

-- *** Update ***

updateH : DecEq lty => (l : lty) ->
          (isE : Elem l (labelsOf ts)) ->
          getType ts isE -> LHList ts -> LHList ts
updateH l {ts=(l,_)::ts} Here v ( _ :> fs) = (l .=. v) :> fs
updateH l {ts=(_,_)::ts} (There th) v (f :> fs) = f :> updateH l th v fs

updateR : DecEq lty => (l : lty) ->
          (isE : Elem l (labelsOf ts)) ->
          getType ts isE -> Record ts -> Record ts
updateR l isE v (MkRecord isS fs) = MkRecord isS (updateH l isE v fs)

MaybeUpd : DecEq lty => List (lty, Type) -> lty -> Type
MaybeUpd ts l = TypeOrUnit (isElem l (labelsOf ts))
                (\isE => getType ts isE -> Record ts)

updR : DecEq lty => (l : lty) -> Record ts -> MaybeUpd ts l
updR {ts} l r =
     mkTorU (isElem l (labelsOf ts))
            (\isE => getType ts isE -> Record ts)
            (\isE => \v => updateR l isE v r)

-- *** Append ***

appendR : DecEq lty => {ts, us : List (lty, Type)} ->
          Record ts -> Record us ->
          IsSet (labelsOf (ts ++ us)) -> Record (ts ++ us)
appendR (MkRecord _ fs) (MkRecord _ gs) iS = MkRecord iS (fs :++: gs)

MaybeApp : DecEq lty => List (lty, Type) ->
           List (lty, Type) -> Type -> Type
MaybeApp ts us r =
    TypeOrUnitC (isSet (labelsOf (ts ++ us))) r

infixr 7 .++.

(.++.) : DecEq lty => {ts, us : List (lty, Type)} -> Record ts ->
         Record us -> MaybeApp ts us (Record (ts ++ us))
(.++.) {ts} {us} rt ru =
       mkTorUC (isSet (labelsOf (ts ++ us)))
               (\p => appendR rt ru p)

-- *** Delete ***

hDeleteH : DecEq lty => {ts : List (lty, Type)} -> (l : lty) -> LHList ts -> LHList (l ://: ts)
hDeleteH {ts=[]} _ _ = HNil
hDeleteH {ts=(l', ty)::ts} l (f :> fs) with (decEq l l')
  hDeleteH {ts=(l', ty)::ts} l (f :> fs) | Yes _ = fs
  hDeleteH {ts=(l', ty)::ts} l (f :> fs) | No _  = f :> hDeleteH l fs

infixr 7 .//.

(.//.) : DecEq lty => {ts : List (lty, Type)} -> (l : lty) -> Record ts ->
         Record (l ://: ts)
(.//.) l (MkRecord isS fs) =
  let newFs = hDeleteH l fs
      newIsS = ifDeleteThenIsSet l isS
  in MkRecord newIsS newFs

-- *** Delete Labels ***

hDeleteLabelsH : DecEq lty => {ts : List (lty, Type)} -> (ls : List lty ) -> LHList ts -> LHList (ls :///: ts)
hDeleteLabelsH [] fs = fs
hDeleteLabelsH (l :: ls) fs =  hDeleteH l $ hDeleteLabelsH ls fs

infixr 7 .///.

(.///.) : DecEq lty => {ts : List (lty, Type)} -> (ls : List lty) -> Record ts ->
          Record (ls :///: ts)
(.///.) ls (MkRecord isS fs) =
  let newFs = hDeleteLabelsH ls fs
      newIsS = ifDeleteLabelsThenIsSet ls isS
  in MkRecord newIsS newFs

-- *** Left Union ***

hLeftUnionH : DecEq lty => {ts, us : List (lty, Type)} ->
                           LHList ts -> LHList us ->
                           LHList (ts :||: us)
hLeftUnionH {ts} fs gs =  fs :++: (hDeleteLabelsH (labelsOf ts) gs)

infixr 7 .||.

(.||.) : DecEq lty => {ts, us : List (lty, Type)} -> Record ts -> Record us ->
         Record (ts :||: us)
(.||.) (MkRecord isS1 fs) (MkRecord isS2 gs) =
  let newFs = hLeftUnionH fs gs
      newIsS = ifLeftUnionThenisSet isS1 isS2
  in MkRecord newIsS newFs

-- *** Left Projection ***

projectLeftH : DecEq lty => {ts : List (lty, Type)} -> (ls : List lty) ->
               LHList ts -> LHList (ls :<: ts)
projectLeftH {ts=[]} _ HNil = HNil
projectLeftH {ts=(l, _) :: _} ls fs with (isElem l ls)
  projectLeftH {ts=(l, _) :: _} ls (f :> fs) | Yes _ = f :> projectLeftH ls fs
  projectLeftH {ts=(l, _) :: _} ls (_ :> fs) | No _  = projectLeftH ls fs

infixr 7 .<.

(.<.) : DecEq lty => {ts : List (lty, Type)} -> (ls : List lty) ->
        Record ts -> Record (ls :<: ts)
(.<.) ls (MkRecord isS fs) =
  let newFs = projectLeftH ls fs
      newIsS = ifProjectLeftThenIsSet ls isS
  in MkRecord newIsS newFs

-- *** Right Projection ***

projectRightH : DecEq lty => {ts : List (lty, Type)} -> (ls : List lty) ->
               LHList ts -> LHList (ls :>: ts)
projectRightH {ts=[]} _ HNil = HNil
projectRightH {ts=(l, _) :: _} ls fs with (isElem l ls)
  projectRightH {ts=(l, _) :: _} ls (_ :> fs) | Yes _  = projectRightH ls fs
  projectRightH {ts=(l, _) :: _} ls (f :> fs) | No _ = f :> projectRightH ls fs

infixr 7 .>.

(.>.) : DecEq lty => {ts : List (lty, Type)} -> (ls : List lty) ->
        Record ts -> Record (ls :>: ts)
(.>.) ls (MkRecord isS fs) =
  let newFs = projectRightH ls fs
      newIsS = ifProjectRightThenIsSet ls isS
  in MkRecord newIsS newFs

max_stars_repo_name: gonzaw/extensible-records

max_issues_repo_name: gonzaw/extensible-records

max_forks_repo_name: gonzaw/extensible-records


text:
module Compiler.Erlang.Codegen.AbstractFormatToPrimTerm

import Data.Fin
import Data.List

import public Compiler.Erlang.IR.AbstractFormat
import public Compiler.Erlang.Utils.PrimTerm

%default total

-- CODE GENERATION

genLine : Line -> PrimTerm
genLine l = PInteger (cast l)

genLiteral : Literal -> PrimTerm
genLiteral (ALAtom l x) = PTuple [PAtom "atom", genLine l, PAtom x]
genLiteral (ALChar l x) = PTuple [PAtom "char", genLine l, PChar x]
genLiteral (ALFloat l x) = PTuple [PAtom "float", genLine l, PFloat x]
genLiteral (ALInteger l x) = PTuple [PAtom "integer", genLine l, PInteger x]
genLiteral (ALCharlist l x) = PTuple [PAtom "string", genLine l, PCharlist x]

genMapFieldAssoc : (a -> PrimTerm) -> MapFieldAssoc a -> PrimTerm
genMapFieldAssoc toPrimTerm (MkAssoc l key value) =
  PTuple [PAtom "map_field_assoc", genLine l, toPrimTerm key, toPrimTerm value]

genMapFieldExact : (a -> PrimTerm) -> MapFieldExact a -> PrimTerm
genMapFieldExact toPrimTerm (MkExact l key value) =
  PTuple [PAtom "map_field_exact", genLine l, toPrimTerm key, toPrimTerm value]

genBitType : BitType -> PrimTerm
genBitType type =
  PAtom $ case type of
    ABInteger => "integer"
    ABFloat => "float"
    ABBinary => "binary"
    ABBytes => "bytes"
    ABBitstring => "bitstring"
    ABBits => "bits"
    ABUtf8 => "utf8"
    ABUtf16 => "utf16"
    ABUtf32 => "utf32"

genBitSignedness : BitSignedness -> PrimTerm
genBitSignedness signedness =
  PAtom $ case signedness of
    ABUnsigned => "unsigned"
    ABSigned => "signed"

genBitEndianness : BitEndianness -> PrimTerm
genBitEndianness endianness =
  PAtom $ case endianness of
    ABBig => "big"
    ABLittle => "little"
    ABNative => "native"

genBitUnit : BitUnit -> PrimTerm
genBitUnit (MkBitUnit size) =
  PTuple [PAtom "unit", PInteger (cast size + 1)]

genBitSize : BitSize -> PrimTerm
genBitSize ABSDefault = PAtom "default"
genBitSize (ABSInteger l x) = PTuple [PAtom "integer", genLine l, PInteger x]
genBitSize (ABSVar l x) = PTuple [PAtom "var", genLine l, PAtom x]

genTypeSpecifierList : TypeSpecifierList -> PrimTerm
genTypeSpecifierList (MkTSL signedness endianness type unit) =
  PList $ toList (map genBitSignedness signedness) ++
    toList (map genBitEndianness endianness) ++
    toList (map genBitType type) ++
    toList (map genBitUnit unit)

genBitSegment : (a -> PrimTerm) -> BitSegment a -> PrimTerm
genBitSegment genValue (MkBitSegment l value size tsl) =
  PTuple [PAtom "bin_element", genLine l, genValue value, genBitSize size, genTypeSpecifierList tsl]

genBitPattern : BitPattern -> PrimTerm
genBitPattern (ABPInteger l x) = PTuple [PAtom "integer", genLine l, PInteger x]
genBitPattern (ABPFloat l x) = PTuple [PAtom "float", genLine l, PFloat x]
genBitPattern (ABPCharlist l x) = PTuple [PAtom "string", genLine l, PCharlist x]
genBitPattern (ABPUniversal l) = PTuple [PAtom "var", genLine l, PAtom "_"]
genBitPattern (ABPVar l x) = PTuple [PAtom "var", genLine l, PAtom x]

genPattern : Pattern -> PrimTerm
genPattern (APLiteral x) = genLiteral x
genPattern (APBitstring l segments) = PTuple [PAtom "bin", genLine l, PList (map (genBitSegment genBitPattern) segments)]
genPattern (APCons l x y) = PTuple [PAtom "cons", genLine l, genPattern x, genPattern y]
genPattern (APMap l entries) = PTuple [PAtom "map", genLine l, PList (assert_total (map (genMapFieldExact genPattern) entries))]
genPattern (APNil l) = PTuple [PAtom "nil", genLine l]
genPattern (APTuple l patterns) = PTuple [PAtom "tuple", genLine l, PList (assert_total (map genPattern patterns))]
genPattern (APUniversal l) = PTuple [PAtom "var", genLine l, PAtom "_"]
genPattern (APVar l x) = PTuple [PAtom "var", genLine l, PAtom x]

genGuard : Guard -> PrimTerm
genGuard (AGLiteral x) = genLiteral x
genGuard (AGCons l x y) = PTuple [PAtom "cons", genLine l, genGuard x, genGuard y]
genGuard (AGFunCall l fnName args) =
  let remoteRef = PTuple [PAtom "remote", genLine l, genLiteral (ALAtom l "erlang"), genLiteral (ALAtom l fnName)]
  in PTuple [PAtom "call", genLine l, remoteRef, PList (assert_total (map genGuard args))]
genGuard (AGNil l) = PTuple [PAtom "nil", genLine l]
genGuard (AGOp l opName x y) = PTuple [PAtom "op", genLine l, PAtom opName, genGuard x, genGuard y]
genGuard (AGTuple l guards) = PTuple [PAtom "tuple", genLine l, PList (assert_total (map genGuard guards))]
genGuard (AGVar l x) = PTuple [PAtom "var", genLine l, PAtom x]

genGuardAlt : GuardAlt -> PrimTerm
genGuardAlt (MkGuardAlt guards) = PList (assert_total (map genGuard (toList guards)))

mutual
  genExpr : Expr -> PrimTerm
  genExpr (AELiteral x) =
    genLiteral x
  genExpr (AEBitstring l segments) =
    PTuple [PAtom "bin", genLine l, PList (assert_total (map (genBitSegment genExpr) segments))]
  genExpr (AEBlock l body) =
    PTuple [PAtom "block", genLine l, PList (assert_total (map genExpr (toList body)))]
  genExpr (AECase l sc clauses) =
    PTuple [PAtom "case", genLine l, genExpr sc, PList (assert_total (map genCaseClause (toList clauses)))]
  genExpr (AECons l x y) =
    PTuple [PAtom "cons", genLine l, genExpr x, genExpr y]
  genExpr (AEFun l arity clauses) =
    PTuple [PAtom "fun", genLine l, PTuple [PAtom "clauses", PList (assert_total (map genFunClause (toList clauses)))]]
  genExpr (AEFunCall l fn args) =
    PTuple [PAtom "call", genLine l, genExpr fn, PList (assert_total (map genExpr args))]
  genExpr (AERemoteRef l modName fnName) =
    PTuple [PAtom "remote", genLine l, genExpr modName, genExpr fnName]
  genExpr (AEMapNew l entries) =
    PTuple [PAtom "map", genLine l, PList (assert_total (map (genMapFieldAssoc genExpr) entries))]
  genExpr (AEMatch l p x) =
    PTuple [PAtom "match", genLine l, genPattern p, genExpr x]
  genExpr (AENil l) =
    PTuple [PAtom "nil", genLine l]
  genExpr (AEOp l opName x y) =
    PTuple [PAtom "op", genLine l, PAtom opName, genExpr x, genExpr y]
  genExpr (AEReceive l clauses NoTimeout) =
    PTuple [PAtom "receive", genLine l, PList (assert_total (map genCaseClause clauses))]
  genExpr (AEReceive l clauses (TimeoutAfter ms afterBody)) =
    PTuple [PAtom "receive", genLine l, PList (assert_total (map genCaseClause clauses)), genExpr ms, PList (assert_total (map genExpr (toList afterBody)))]
  genExpr (AETuple l exprs) =
    PTuple [PAtom "tuple", genLine l, PList (assert_total (map genExpr exprs))]
  genExpr (AETry l sc caseClauses catchClauses afterBody) =
    PTuple [PAtom "try", genLine l, PList (assert_total (map genExpr (toList sc))), PList (assert_total (map genCaseClause caseClauses)), PList (assert_total (map genCatchClause catchClauses)), PList (assert_total (map genExpr afterBody))]
  genExpr (AEVar l x) =
    PTuple [PAtom "var", genLine l, PAtom x]

  genFunClause : FunClause arity -> PrimTerm
  genFunClause (MkFunClause l patterns guardAlts body) =
    PTuple [PAtom "clause", genLine l, PList (toList (map genPattern patterns)), PList (map genGuardAlt guardAlts), PList (assert_total (map genExpr (toList body)))]

  genCaseClause : CaseClause -> PrimTerm
  genCaseClause (MkCaseClause l pattern guardAlts body) =
    PTuple [PAtom "clause", genLine l, PList [genPattern pattern], PList (map genGuardAlt guardAlts), PList (assert_total (map genExpr (toList body)))]

  genCatchClause : CatchClause -> PrimTerm
  genCatchClause (MkCatchClause l classPat reasonPat stacktracePat guardAlts body) =
    let catchPattern = genPattern (APTuple l [classPat, reasonPat, stacktracePat])
    in PTuple [PAtom "clause", genLine l, PList [catchPattern], PList (map genGuardAlt guardAlts), PList (assert_total (map genExpr (toList body)))]

genExportFun : (String, Nat) -> PrimTerm
genExportFun (name, arity) = PTuple [PAtom name, PInteger (natToInteger arity)]

export
genDecl : Decl -> PrimTerm
genDecl (ADExport l fs) =
  PTuple [PAtom "attribute", genLine l, PAtom "export", PList (map genExportFun fs)]
genDecl (ADModule l name) =
  PTuple [PAtom "attribute", genLine l, PAtom "module", PAtom name]
genDecl (ADFunDef l name arity clauses) =
  PTuple [PAtom "function", genLine l, PAtom name, PInteger (natToInteger arity), PList (map genFunClause (toList clauses))]
genDecl (ADAttribute l attr value) =
  PTuple [PAtom "attribute", genLine l, PAtom attr, value]


text:
module Semacrolon

import Nope

%access public export
%default total

--data SemacrolonToken : Type where
--  STMacro : SemacrolonToken
--  STEq : SemacrolonToken
--  STMacroName : String -> SemacrolonToken
--  STTerm : Term String -> SemacrolonToken

data SemacrolonExpr : Type where
  MacroAppl : String -> List SemacrolonExpr -> SemacrolonExpr
  NopeAppl : Term String -> SemacrolonExpr -> List SemacrolonExpr -> SemacrolonExpr
  SemacrolonTerm : Term String -> SemacrolonExpr

data SemacrolonAst : Type where
  MacroDef : String -> List SemacrolonExpr -> NopeAst -> SemacrolonAst
  MacroExpr : SemacrolonExpr -> SemacrolonAst

mutual
  -- This is necessary for totality
  unwrapQuotedIds_ : List NopeAst -> List NopeAst
  unwrapQuotedIds_ [] = []
  unwrapQuotedIds_ (ast :: asts) = unwrapQuotedIds ast :: unwrapQuotedIds_ asts

  unwrapQuotedIds : NopeAst -> NopeAst
  unwrapQuotedIds (TermAst (Raw '#' y)) = TermAst (Id y)
  unwrapQuotedIds (TermAst term@(Raw _ _)) = TermAst term
  unwrapQuotedIds (TermAst term@(Id _)) = TermAst term
  unwrapQuotedIds (Appl ast ast_ asts) =
    Appl (unwrapQuotedIds ast) (unwrapQuotedIds ast_) (unwrapQuotedIds_ asts)

parseMacroExpr : NopeAst -> Maybe SemacrolonExpr
parseMacroExpr (TermAst term@(Raw _ _)) = Just $ SemacrolonTerm term
parseMacroExpr (TermAst (Id x)) =
  case unpack x of
    ('#' :: _) => Nothing
    (';' :: _) => Just $ MacroAppl x []
    _ =>  Just $ SemacrolonTerm $ Id x
parseMacroExpr (Appl (TermAst x) ast2 xs) = ?parseMacroExpr_rhs_1
parseMacroExpr (Appl (Appl ast ast_ ys) ast2 xs) = ?parseMacroExpr_rhs_3

parseMacro : NopeAst -> Maybe SemacrolonAst

execMacro : SemacrolonAst -> NopeAst
execMacro (MacroDef x xs ast) = ?execMacro_rhs_1
execMacro (MacroExpr x) = ?execMacro_rhs_2

max_stars_repo_name: PolyglotSymposium/nosh

max_issues_repo_name: PolyglotSymposium/nosh

max_forks_repo_name: PolyglotSymposium/nosh


text:
module Minecraft.Core.Tangible

import Minecraft.Core

%default total

public export
interface Tangible (self : Type) where

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
||| Common types and instances for JSON interoperability.
|||
||| (C) The Idris Community, 2021
module Language.LSP.Message.Utils

import public Data.OneOf
import Language.JSON
import Language.JSON.Interfaces
import Language.LSP.Message.Derive

%default total

-- TODO: Upstream this implementations.
public export
Foldable (Pair a) where
  foldr f init (_, input) = f input init
  null _ = False

public export
Traversable (Pair a) where
  traverse f (x, y) = (x,) <$> f y

public export
Eq JSON where
  JNull        == JNull        = True
  (JBoolean x) == (JBoolean y) = x == y
  (JNumber x)  == (JNumber y)  = x == y
  (JString x)  == (JString y)  = x == y
  (JArray xs)  == (JArray ys)  = assert_total $ xs == ys
  (JObject xs) == (JObject ys) = assert_total $ xs == ys
  _ == _ = False

||| Singleton type that models `null` in JSON.
public export
data Null = MkNull

public export
Eq Null where
  MkNull == MkNull = True

public export
Ord Null where
  compare MkNull MkNull = EQ

public export
Show Null where
  show MkNull = "null"

export
ToJSON Null where
  toJSON MkNull = JNull

export
FromJSON Null where
  fromJSON JNull = pure MkNull
  fromJSON _ = neutral

||| Converts an `UntaggedEither` value to the isomorphic value in `Either`.
public export
toEither : OneOf [a, b] -> Either a b
toEither (Here x)  = Left x
toEither (There (Here x)) = Right x

||| Converts an `Either` value to the isomorphic value in `UntaggedEither`.
public export
fromEither : Either a b -> OneOf [a, b]
fromEither (Left x)  = make x
fromEither (Right x) = make x

public export
toMaybe : OneOf [a, Null] -> Maybe a
toMaybe (Here x) = Just x
toMaybe (There (Here MkNull)) = Nothing

public export
fromMaybe : Maybe a -> OneOf [a, Null]
fromMaybe (Just x) = make x
fromMaybe Nothing = make MkNull

public export
ConstraintList : (Type -> Type) -> List Type -> Type
ConstraintList f [] = ()
ConstraintList f (x :: xs) = (f x, ConstraintList f xs)

export
ConstraintList ToJSON as => ToJSON (OneOf as) where
  toJSON (Here x) = toJSON x
  toJSON (There x) = toJSON x

export
{as : _} -> ConstraintList FromJSON as => FromJSON (OneOf as) where
  -- NOTE: The rightmost type is parsed first, since in the LSP specification
  --       the most specific type appears also rightmost.
  fromJSON {as = []} @{()} v = Nothing
  fromJSON {as = (x :: xs)} @{(c, cs)} v = (There <$> fromJSON v) <|> (Here <$> fromJSON v)


text:
-- using Idris as a library to install new backends
-- build with: $ idris2 -p idris2 -p contrib -p network -o lazy-idris2 Lazy.idr
-- run with: $ ./build/exec/lazy-idris2 --cg lazy -o <output-exec> <File.idr>

module Main

import Core.Context
import Compiler.Common
import Idris.Driver -- mainWithCodegens

compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) -> ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs tmpDir outputDir term file = do coreLift $ putStrLn "I'd rather not."
                                             pure Nothing

execute : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
execute defs tmpDir term = do coreLift $ putStrLn "Maybe in an hour!"

lazyCodegen : Codegen
lazyCodegen = MkCG compile execute

main : IO ()
main = mainWithCodegens [("lazy", lazyCodegen)]

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
import Data.Vect

my_length : List a -> Nat
my_length [] = 0
my_length (x :: xs) = 1 + length xs

my_reverse : List a -> List a
my_reverse [] = []
my_reverse (x :: xs) = my_reverse xs ++ [x]

my_map : (a -> b) -> List a -> List b
my_map f [] = []
my_map f (x :: xs) = f x :: my_map f xs

my_vmap : (a -> b) -> Vect n a -> Vect n b
my_vmap f [] = []
my_vmap f (x :: xs) = f x :: my_vmap f xs

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Main

main : IO ()
main = do l <- getLine
          let ll = l ++ l
          putStrLn ll

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin